:: MSSUBLAT semantic presentation begin theorem :: MSSUBLAT:1 (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set "(" ($#k7_finseq_2 :::"*-->"::: ) (Set (Var "a")) ")" ) ($#k3_funct_2 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ; theorem :: MSSUBLAT:2 (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set "(" ($#k7_finseq_2 :::"*-->"::: ) (Set (Var "a")) ")" ) ($#k3_funct_2 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "a")) ($#k9_finseq_1 :::"*>"::: ) ))) ; theorem :: MSSUBLAT:3 (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set "(" ($#k7_finseq_2 :::"*-->"::: ) (Set (Var "a")) ")" ) ($#k3_funct_2 :::"."::: ) (Num 2)) ($#r1_hidden :::"="::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "a")) "," (Set (Var "a")) ($#k10_finseq_1 :::"*>"::: ) ))) ; theorem :: MSSUBLAT:4 (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set "(" ($#k7_finseq_2 :::"*-->"::: ) (Set (Var "a")) ")" ) ($#k3_funct_2 :::"."::: ) (Num 3)) ($#r1_hidden :::"="::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "a")) "," (Set (Var "a")) "," (Set (Var "a")) ($#k11_finseq_1 :::"*>"::: ) ))) ; theorem :: MSSUBLAT:5 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_tarski :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) ) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Set (Var "i")) ($#k5_finseq_2 :::"|->"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "iff" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "i"))) ")" ))) ; theorem :: MSSUBLAT:6 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_finseq_2 :::"*-->"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))))) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "i"))))) ; begin theorem :: MSSUBLAT:7 (Bool "for" (Set (Var "U1")) "," (Set (Var "U2")) "being" ($#l1_unialg_1 :::"Universal_Algebra":::) "st" (Bool (Bool (Set (Var "U1")) "is" ($#m1_unialg_2 :::"SubAlgebra"::: ) "of" (Set (Var "U2")))) "holds" (Bool (Set ($#k6_msualg_1 :::"MSSign"::: ) (Set (Var "U1"))) ($#r1_hidden :::"="::: ) (Set ($#k6_msualg_1 :::"MSSign"::: ) (Set (Var "U2"))))) ; theorem :: MSSUBLAT:8 (Bool "for" (Set (Var "U1")) "," (Set (Var "U2")) "being" ($#l1_unialg_1 :::"Universal_Algebra":::) "st" (Bool (Bool (Set (Var "U1")) "is" ($#m1_unialg_2 :::"SubAlgebra"::: ) "of" (Set (Var "U2")))) "holds" (Bool "for" (Set (Var "B")) "being" ($#m3_pboole :::"MSSubset":::) "of" (Set "(" ($#k9_msualg_1 :::"MSAlg"::: ) (Set (Var "U2")) ")" ) "st" (Bool (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set "(" ($#k9_msualg_1 :::"MSAlg"::: ) (Set (Var "U1")) ")" )))) "holds" (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set "(" ($#k6_msualg_1 :::"MSSign"::: ) (Set (Var "U2")) ")" ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set "(" ($#k6_msualg_1 :::"MSSign"::: ) (Set (Var "U1")) ")" ) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "o")))) "holds" (Bool (Set ($#k5_msualg_1 :::"Den"::: ) "(" (Set (Var "a")) "," (Set "(" ($#k9_msualg_1 :::"MSAlg"::: ) (Set (Var "U1")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_msualg_1 :::"Den"::: ) "(" (Set (Var "o")) "," (Set "(" ($#k9_msualg_1 :::"MSAlg"::: ) (Set (Var "U2")) ")" ) ")" ")" ) ($#k2_partfun1 :::"|"::: ) (Set "(" ($#k3_msualg_1 :::"Args"::: ) "(" (Set (Var "a")) "," (Set "(" ($#k9_msualg_1 :::"MSAlg"::: ) (Set (Var "U1")) ")" ) ")" ")" ))))))) ; theorem :: MSSUBLAT:9 (Bool "for" (Set (Var "U1")) "," (Set (Var "U2")) "being" ($#l1_unialg_1 :::"Universal_Algebra":::) "st" (Bool (Bool (Set (Var "U1")) "is" ($#m1_unialg_2 :::"SubAlgebra"::: ) "of" (Set (Var "U2")))) "holds" (Bool (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set "(" ($#k9_msualg_1 :::"MSAlg"::: ) (Set (Var "U1")) ")" )) "is" ($#m3_pboole :::"MSSubset":::) "of" (Set "(" ($#k9_msualg_1 :::"MSAlg"::: ) (Set (Var "U2")) ")" ))) ; theorem :: MSSUBLAT:10 (Bool "for" (Set (Var "U1")) "," (Set (Var "U2")) "being" ($#l1_unialg_1 :::"Universal_Algebra":::) "st" (Bool (Bool (Set (Var "U1")) "is" ($#m1_unialg_2 :::"SubAlgebra"::: ) "of" (Set (Var "U2")))) "holds" (Bool "for" (Set (Var "B")) "being" ($#m3_pboole :::"MSSubset":::) "of" (Set "(" ($#k9_msualg_1 :::"MSAlg"::: ) (Set (Var "U2")) ")" ) "st" (Bool (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set "(" ($#k9_msualg_1 :::"MSAlg"::: ) (Set (Var "U1")) ")" )))) "holds" (Bool (Set (Var "B")) "is" ($#v3_msualg_2 :::"opers_closed"::: ) ))) ; theorem :: MSSUBLAT:11 (Bool "for" (Set (Var "U1")) "," (Set (Var "U2")) "being" ($#l1_unialg_1 :::"Universal_Algebra":::) "st" (Bool (Bool (Set (Var "U1")) "is" ($#m1_unialg_2 :::"SubAlgebra"::: ) "of" (Set (Var "U2")))) "holds" (Bool "for" (Set (Var "B")) "being" ($#m3_pboole :::"MSSubset":::) "of" (Set "(" ($#k9_msualg_1 :::"MSAlg"::: ) (Set (Var "U2")) ")" ) "st" (Bool (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set "(" ($#k9_msualg_1 :::"MSAlg"::: ) (Set (Var "U1")) ")" )))) "holds" (Bool (Set "the" ($#u4_msualg_1 :::"Charact"::: ) "of" (Set "(" ($#k9_msualg_1 :::"MSAlg"::: ) (Set (Var "U1")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_msualg_2 :::"Opers"::: ) "(" (Set "(" ($#k9_msualg_1 :::"MSAlg"::: ) (Set (Var "U2")) ")" ) "," (Set (Var "B")) ")" )))) ; theorem :: MSSUBLAT:12 (Bool "for" (Set (Var "U1")) "," (Set (Var "U2")) "being" ($#l1_unialg_1 :::"Universal_Algebra":::) "st" (Bool (Bool (Set (Var "U1")) "is" ($#m1_unialg_2 :::"SubAlgebra"::: ) "of" (Set (Var "U2")))) "holds" (Bool (Set ($#k9_msualg_1 :::"MSAlg"::: ) (Set (Var "U1"))) "is" ($#m1_msualg_2 :::"MSSubAlgebra"::: ) "of" (Set ($#k9_msualg_1 :::"MSAlg"::: ) (Set (Var "U2"))))) ; theorem :: MSSUBLAT:13 (Bool "for" (Set (Var "U1")) "," (Set (Var "U2")) "being" ($#l1_unialg_1 :::"Universal_Algebra":::) "st" (Bool (Bool (Set ($#k9_msualg_1 :::"MSAlg"::: ) (Set (Var "U1"))) "is" ($#m1_msualg_2 :::"MSSubAlgebra"::: ) "of" (Set ($#k9_msualg_1 :::"MSAlg"::: ) (Set (Var "U2"))))) "holds" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "U1"))) "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "U2")))) ; theorem :: MSSUBLAT:14 (Bool "for" (Set (Var "U1")) "," (Set (Var "U2")) "being" ($#l1_unialg_1 :::"Universal_Algebra":::) "st" (Bool (Bool (Set ($#k9_msualg_1 :::"MSAlg"::: ) (Set (Var "U1"))) "is" ($#m1_msualg_2 :::"MSSubAlgebra"::: ) "of" (Set ($#k9_msualg_1 :::"MSAlg"::: ) (Set (Var "U2"))))) "holds" (Bool "for" (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "U2")) "st" (Bool (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "U1"))))) "holds" (Bool (Set (Var "B")) "is" ($#v1_unialg_2 :::"opers_closed"::: ) ))) ; theorem :: MSSUBLAT:15 (Bool "for" (Set (Var "U1")) "," (Set (Var "U2")) "being" ($#l1_unialg_1 :::"Universal_Algebra":::) "st" (Bool (Bool (Set ($#k9_msualg_1 :::"MSAlg"::: ) (Set (Var "U1"))) "is" ($#m1_msualg_2 :::"MSSubAlgebra"::: ) "of" (Set ($#k9_msualg_1 :::"MSAlg"::: ) (Set (Var "U2"))))) "holds" (Bool "for" (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "U2")) "st" (Bool (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "U1"))))) "holds" (Bool (Set "the" ($#u1_unialg_1 :::"charact"::: ) "of" (Set (Var "U1"))) ($#r1_hidden :::"="::: ) (Set ($#k3_unialg_2 :::"Opers"::: ) "(" (Set (Var "U2")) "," (Set (Var "B")) ")" )))) ; theorem :: MSSUBLAT:16 (Bool "for" (Set (Var "U1")) "," (Set (Var "U2")) "being" ($#l1_unialg_1 :::"Universal_Algebra":::) "st" (Bool (Bool (Set ($#k9_msualg_1 :::"MSAlg"::: ) (Set (Var "U1"))) "is" ($#m1_msualg_2 :::"MSSubAlgebra"::: ) "of" (Set ($#k9_msualg_1 :::"MSAlg"::: ) (Set (Var "U2"))))) "holds" (Bool (Set (Var "U1")) "is" ($#m1_unialg_2 :::"SubAlgebra"::: ) "of" (Set (Var "U2")))) ; theorem :: MSSUBLAT:17 (Bool "for" (Set (Var "MS")) "being" ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) (Num 1) ($#v13_struct_0 :::"-element"::: ) ($#v5_msualg_1 :::"segmental"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "MS")) (Bool "for" (Set (Var "B")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#m1_msualg_2 :::"MSSubAlgebra"::: ) "of" (Set (Var "A")) "holds" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k12_msualg_1 :::"1-Alg"::: ) (Set (Var "B")) ")" )) "is" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k12_msualg_1 :::"1-Alg"::: ) (Set (Var "A")) ")" ))))) ; theorem :: MSSUBLAT:18 (Bool "for" (Set (Var "MS")) "being" ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) (Num 1) ($#v13_struct_0 :::"-element"::: ) ($#v5_msualg_1 :::"segmental"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "MS")) (Bool "for" (Set (Var "B")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#m1_msualg_2 :::"MSSubAlgebra"::: ) "of" (Set (Var "A")) (Bool "for" (Set (Var "S")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k12_msualg_1 :::"1-Alg"::: ) (Set (Var "A")) ")" ) "st" (Bool (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k12_msualg_1 :::"1-Alg"::: ) (Set (Var "B")) ")" )))) "holds" (Bool (Set (Var "S")) "is" ($#v1_unialg_2 :::"opers_closed"::: ) ))))) ; theorem :: MSSUBLAT:19 (Bool "for" (Set (Var "MS")) "being" ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) (Num 1) ($#v13_struct_0 :::"-element"::: ) ($#v5_msualg_1 :::"segmental"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "MS")) (Bool "for" (Set (Var "B")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#m1_msualg_2 :::"MSSubAlgebra"::: ) "of" (Set (Var "A")) (Bool "for" (Set (Var "S")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k12_msualg_1 :::"1-Alg"::: ) (Set (Var "A")) ")" ) "st" (Bool (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k12_msualg_1 :::"1-Alg"::: ) (Set (Var "B")) ")" )))) "holds" (Bool (Set "the" ($#u1_unialg_1 :::"charact"::: ) "of" (Set "(" ($#k12_msualg_1 :::"1-Alg"::: ) (Set (Var "B")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_unialg_2 :::"Opers"::: ) "(" (Set "(" ($#k12_msualg_1 :::"1-Alg"::: ) (Set (Var "A")) ")" ) "," (Set (Var "S")) ")" )))))) ; theorem :: MSSUBLAT:20 (Bool "for" (Set (Var "MS")) "being" ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) (Num 1) ($#v13_struct_0 :::"-element"::: ) ($#v5_msualg_1 :::"segmental"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "MS")) (Bool "for" (Set (Var "B")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#m1_msualg_2 :::"MSSubAlgebra"::: ) "of" (Set (Var "A")) "holds" (Bool (Set ($#k12_msualg_1 :::"1-Alg"::: ) (Set (Var "B"))) "is" ($#m1_unialg_2 :::"SubAlgebra"::: ) "of" (Set ($#k12_msualg_1 :::"1-Alg"::: ) (Set (Var "A"))))))) ; theorem :: MSSUBLAT:21 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#m1_msualg_2 :::"MSSubAlgebra"::: ) "of" (Set (Var "B"))) "iff" (Bool (Set (Var "A")) "is" ($#m1_msualg_2 :::"MSSubAlgebra"::: ) "of" (Set ($#g3_msualg_1 :::"MSAlgebra"::: ) "(#" (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "B"))) "," (Set "the" ($#u4_msualg_1 :::"Charact"::: ) "of" (Set (Var "B"))) "#)" )) ")" ))) ; theorem :: MSSUBLAT:22 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l1_unialg_1 :::"Universal_Algebra":::) "holds" (Bool "(" (Bool (Set ($#k1_unialg_1 :::"signature"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k1_unialg_1 :::"signature"::: ) (Set (Var "B")))) "iff" (Bool (Set ($#k6_msualg_1 :::"MSSign"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k6_msualg_1 :::"MSSign"::: ) (Set (Var "B")))) ")" )) ; theorem :: MSSUBLAT:23 (Bool "for" (Set (Var "MS")) "being" ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) (Num 1) ($#v13_struct_0 :::"-element"::: ) ($#v5_msualg_1 :::"segmental"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "MS")) "st" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "MS"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) ))) "holds" (Bool (Set ($#k6_msualg_1 :::"MSSign"::: ) (Set "(" ($#k12_msualg_1 :::"1-Alg"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#g1_msualg_1 :::"ManySortedSign"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "MS"))) "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "MS"))) "," (Set "the" ($#u1_msualg_1 :::"Arity"::: ) "of" (Set (Var "MS"))) "," (Set "the" ($#u2_msualg_1 :::"ResultSort"::: ) "of" (Set (Var "MS"))) "#)" )))) ; theorem :: MSSUBLAT:24 (Bool "for" (Set (Var "MS")) "being" ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) (Num 1) ($#v13_struct_0 :::"-element"::: ) ($#v5_msualg_1 :::"segmental"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "MS")) "st" (Bool (Bool (Set ($#k12_msualg_1 :::"1-Alg"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k12_msualg_1 :::"1-Alg"::: ) (Set (Var "B"))))) "holds" (Bool (Set ($#g3_msualg_1 :::"MSAlgebra"::: ) "(#" (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A"))) "," (Set "the" ($#u4_msualg_1 :::"Charact"::: ) "of" (Set (Var "A"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g3_msualg_1 :::"MSAlgebra"::: ) "(#" (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "B"))) "," (Set "the" ($#u4_msualg_1 :::"Charact"::: ) "of" (Set (Var "B"))) "#)" )))) ; theorem :: MSSUBLAT:25 (Bool "for" (Set (Var "MS")) "being" ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) (Num 1) ($#v13_struct_0 :::"-element"::: ) ($#v5_msualg_1 :::"segmental"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "MS")) "st" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "MS"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) ))) "holds" (Bool (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set "(" ($#k9_msualg_1 :::"MSAlg"::: ) (Set "(" ($#k12_msualg_1 :::"1-Alg"::: ) (Set (Var "A")) ")" ) ")" ))))) ; theorem :: MSSUBLAT:26 (Bool "for" (Set (Var "MS")) "being" ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) (Num 1) ($#v13_struct_0 :::"-element"::: ) ($#v5_msualg_1 :::"segmental"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "MS")) "st" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "MS"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) ))) "holds" (Bool (Set ($#k9_msualg_1 :::"MSAlg"::: ) (Set "(" ($#k12_msualg_1 :::"1-Alg"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#g3_msualg_1 :::"MSAlgebra"::: ) "(#" (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A"))) "," (Set "the" ($#u4_msualg_1 :::"Charact"::: ) "of" (Set (Var "A"))) "#)" )))) ; theorem :: MSSUBLAT:27 (Bool "for" (Set (Var "A")) "being" ($#l1_unialg_1 :::"Universal_Algebra":::) (Bool "for" (Set (Var "B")) "being" ($#v3_msualg_1 :::"strict"::: ) ($#v4_msualg_1 :::"non-empty"::: ) ($#m1_msualg_2 :::"MSSubAlgebra"::: ) "of" (Set ($#k9_msualg_1 :::"MSAlg"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k6_msualg_1 :::"MSSign"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) ))) "holds" (Bool (Set ($#k12_msualg_1 :::"1-Alg"::: ) (Set (Var "B"))) "is" ($#m1_unialg_2 :::"SubAlgebra"::: ) "of" (Set (Var "A"))))) ; begin theorem :: MSSUBLAT:28 (Bool "for" (Set (Var "A")) "being" ($#l1_unialg_1 :::"Universal_Algebra":::) (Bool "for" (Set (Var "a1")) "," (Set (Var "b1")) "being" ($#v1_unialg_1 :::"strict"::: ) ($#m1_unialg_2 :::"SubAlgebra"::: ) "of" (Set (Var "A")) (Bool "for" (Set (Var "a2")) "," (Set (Var "b2")) "being" ($#v3_msualg_1 :::"strict"::: ) ($#v4_msualg_1 :::"non-empty"::: ) ($#m1_msualg_2 :::"MSSubAlgebra"::: ) "of" (Set ($#k9_msualg_1 :::"MSAlg"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Var "a2")) ($#r1_hidden :::"="::: ) (Set ($#k9_msualg_1 :::"MSAlg"::: ) (Set (Var "a1")))) & (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k9_msualg_1 :::"MSAlg"::: ) (Set (Var "b1"))))) "holds" (Bool (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "a2"))) ($#k2_pboole :::"\/"::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "b2")))) ($#r1_hidden :::"="::: ) (Set (Set ($#k6_numbers :::"0"::: ) ) ($#k16_funcop_1 :::".-->"::: ) (Set "(" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "a1"))) ($#k2_xboole_0 :::"\/"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b1"))) ")" )))))) ; theorem :: MSSUBLAT:29 (Bool "for" (Set (Var "A")) "being" ($#l1_unialg_1 :::"Universal_Algebra":::) (Bool "for" (Set (Var "a1")) "," (Set (Var "b1")) "being" ($#v1_unialg_1 :::"strict"::: ) ($#v4_unialg_1 :::"non-empty"::: ) ($#m1_unialg_2 :::"SubAlgebra"::: ) "of" (Set (Var "A")) (Bool "for" (Set (Var "a2")) "," (Set (Var "b2")) "being" ($#v3_msualg_1 :::"strict"::: ) ($#v4_msualg_1 :::"non-empty"::: ) ($#m1_msualg_2 :::"MSSubAlgebra"::: ) "of" (Set ($#k9_msualg_1 :::"MSAlg"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Var "a2")) ($#r1_hidden :::"="::: ) (Set ($#k9_msualg_1 :::"MSAlg"::: ) (Set (Var "a1")))) & (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k9_msualg_1 :::"MSAlg"::: ) (Set (Var "b1"))))) "holds" (Bool (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "a2"))) ($#k3_pboole :::"/\"::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "b2")))) ($#r1_hidden :::"="::: ) (Set (Set ($#k6_numbers :::"0"::: ) ) ($#k16_funcop_1 :::".-->"::: ) (Set "(" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "a1"))) ($#k3_xboole_0 :::"/\"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b1"))) ")" )))))) ; theorem :: MSSUBLAT:30 (Bool "for" (Set (Var "A")) "being" ($#v1_unialg_1 :::"strict"::: ) ($#l1_unialg_1 :::"Universal_Algebra":::) (Bool "for" (Set (Var "a1")) "," (Set (Var "b1")) "being" ($#v1_unialg_1 :::"strict"::: ) ($#v4_unialg_1 :::"non-empty"::: ) ($#m1_unialg_2 :::"SubAlgebra"::: ) "of" (Set (Var "A")) (Bool "for" (Set (Var "a2")) "," (Set (Var "b2")) "being" ($#v3_msualg_1 :::"strict"::: ) ($#v4_msualg_1 :::"non-empty"::: ) ($#m1_msualg_2 :::"MSSubAlgebra"::: ) "of" (Set ($#k9_msualg_1 :::"MSAlg"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Var "a2")) ($#r1_hidden :::"="::: ) (Set ($#k9_msualg_1 :::"MSAlg"::: ) (Set (Var "a1")))) & (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k9_msualg_1 :::"MSAlg"::: ) (Set (Var "b1"))))) "holds" (Bool (Set ($#k9_msualg_1 :::"MSAlg"::: ) (Set "(" (Set (Var "a1")) ($#k8_unialg_2 :::""\/""::: ) (Set (Var "b1")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "a2")) ($#k13_msualg_2 :::""\/""::: ) (Set (Var "b2"))))))) ; registrationlet "A" be ($#v2_unialg_2 :::"with_const_op"::: ) ($#l1_unialg_1 :::"Universal_Algebra":::); cluster (Set ($#k6_msualg_1 :::"MSSign"::: ) "A") -> ($#v2_msualg_2 :::"all-with_const_op"::: ) ; end; theorem :: MSSUBLAT:31 (Bool "for" (Set (Var "A")) "being" ($#v2_unialg_2 :::"with_const_op"::: ) ($#l1_unialg_1 :::"Universal_Algebra":::) (Bool "for" (Set (Var "a1")) "," (Set (Var "b1")) "being" ($#v1_unialg_1 :::"strict"::: ) ($#v4_unialg_1 :::"non-empty"::: ) ($#m1_unialg_2 :::"SubAlgebra"::: ) "of" (Set (Var "A")) (Bool "for" (Set (Var "a2")) "," (Set (Var "b2")) "being" ($#v3_msualg_1 :::"strict"::: ) ($#v4_msualg_1 :::"non-empty"::: ) ($#m1_msualg_2 :::"MSSubAlgebra"::: ) "of" (Set ($#k9_msualg_1 :::"MSAlg"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Var "a2")) ($#r1_hidden :::"="::: ) (Set ($#k9_msualg_1 :::"MSAlg"::: ) (Set (Var "a1")))) & (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k9_msualg_1 :::"MSAlg"::: ) (Set (Var "b1"))))) "holds" (Bool (Set ($#k9_msualg_1 :::"MSAlg"::: ) (Set "(" (Set (Var "a1")) ($#k5_unialg_2 :::"/\"::: ) (Set (Var "b1")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "a2")) ($#k11_msualg_2 :::"/\"::: ) (Set (Var "b2"))))))) ; registrationlet "A" be ($#v3_unialg_1 :::"quasi_total"::: ) ($#l1_unialg_1 :::"UAStr"::: ) ; cluster (Set ($#g1_unialg_1 :::"UAStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "A") "," (Set "the" ($#u1_unialg_1 :::"charact"::: ) "of" "A") "#)" ) -> ($#v3_unialg_1 :::"quasi_total"::: ) ; end; registrationlet "A" be ($#v2_unialg_1 :::"partial"::: ) ($#l1_unialg_1 :::"UAStr"::: ) ; cluster (Set ($#g1_unialg_1 :::"UAStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "A") "," (Set "the" ($#u1_unialg_1 :::"charact"::: ) "of" "A") "#)" ) -> ($#v2_unialg_1 :::"partial"::: ) ; end; registrationlet "A" be ($#v4_unialg_1 :::"non-empty"::: ) ($#l1_unialg_1 :::"UAStr"::: ) ; cluster (Set ($#g1_unialg_1 :::"UAStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "A") "," (Set "the" ($#u1_unialg_1 :::"charact"::: ) "of" "A") "#)" ) -> ($#v4_unialg_1 :::"non-empty"::: ) ; end; registrationlet "A" be ($#v2_unialg_2 :::"with_const_op"::: ) ($#l1_unialg_1 :::"Universal_Algebra":::); cluster (Set ($#g1_unialg_1 :::"UAStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "A") "," (Set "the" ($#u1_unialg_1 :::"charact"::: ) "of" "A") "#)" ) -> ($#v2_unialg_2 :::"with_const_op"::: ) ; end; theorem :: MSSUBLAT:32 (Bool "for" (Set (Var "A")) "being" ($#v2_unialg_2 :::"with_const_op"::: ) ($#l1_unialg_1 :::"Universal_Algebra":::) "holds" (Bool (Set ($#k12_unialg_2 :::"UnSubAlLattice"::: ) (Set ($#g1_unialg_1 :::"UAStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "A"))) "," (Set "the" ($#u1_unialg_1 :::"charact"::: ) "of" (Set (Var "A"))) "#)" )) "," (Set ($#k17_msualg_2 :::"MSSubAlLattice"::: ) (Set "(" ($#k9_msualg_1 :::"MSAlg"::: ) (Set ($#g1_unialg_1 :::"UAStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "A"))) "," (Set "the" ($#u1_unialg_1 :::"charact"::: ) "of" (Set (Var "A"))) "#)" ) ")" )) ($#r1_filter_1 :::"are_isomorphic"::: ) )) ;