:: CLOSURE3 semantic presentation begin registrationlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) ; cluster (Set ($#g1_struct_0 :::"1-sorted"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S") "#)" ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ; end; theorem :: CLOSURE3:1 (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "," (Set (Var "N")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool (Set (Set (Var "M")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "N"))) ($#r1_hidden :::"="::: ) (Set (Var "N"))))) ; theorem :: CLOSURE3:2 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "," (Set (Var "N")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"SubsetFamily":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "N")) ($#r2_hidden :::"in"::: ) (Set (Var "F")))) "holds" (Bool (Set ($#k4_mssubfam :::"meet"::: ) (Set ($#k5_closure2 :::"|:"::: ) (Set (Var "F")) ($#k5_closure2 :::":|"::: ) )) ($#r2_pboole :::"c='"::: ) (Set (Var "N")))))) ; theorem :: CLOSURE3:3 (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 "MA")) "being" ($#v3_msualg_1 :::"strict"::: ) ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"SubsetFamily":::) "of" (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "MA"))) "st" (Bool (Bool (Set (Var "F")) ($#r1_tarski :::"c="::: ) (Set ($#k6_msualg_2 :::"SubSort"::: ) (Set (Var "MA"))))) "holds" (Bool "for" (Set (Var "B")) "being" ($#m3_pboole :::"MSSubset":::) "of" (Set (Var "MA")) "st" (Bool (Bool (Set (Var "B")) ($#r8_pboole :::"="::: ) (Set ($#k4_mssubfam :::"meet"::: ) (Set ($#k5_closure2 :::"|:"::: ) (Set (Var "F")) ($#k5_closure2 :::":|"::: ) )))) "holds" (Bool (Set (Var "B")) "is" ($#v3_msualg_2 :::"opers_closed"::: ) ))))) ; begin theorem :: CLOSURE3:4 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "A")) ($#r2_setfam_1 :::"is_coarser_than"::: ) (Set (Var "B"))) & (Bool (Set (Var "B")) ($#r2_setfam_1 :::"is_coarser_than"::: ) (Set (Var "C")))) "holds" (Bool (Set (Var "A")) ($#r2_setfam_1 :::"is_coarser_than"::: ) (Set (Var "C")))) ; definitionlet "I" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "M" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); :: original: :::"support"::: redefine func :::"support"::: "M" -> ($#m1_hidden :::"set"::: ) equals :: CLOSURE3:def 1 "{" (Set (Var "x")) where x "is" ($#m1_subset_1 :::"Element"::: ) "of" "I" : (Bool (Set "M" ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) "}" ; end; :: deftheorem defines :::"support"::: CLOSURE3:def 1 : (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool (Set ($#k1_closure3 :::"support"::: ) (Set (Var "M"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "x")) where x "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "I")) : (Bool (Set (Set (Var "M")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) "}" ))); theorem :: CLOSURE3:5 (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool (Set (Var "M")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_pboole :::"[[0]]"::: ) (Set (Var "I")) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "M")) ($#k5_relat_1 :::"|"::: ) (Set "(" ($#k1_closure3 :::"support"::: ) (Set (Var "M")) ")" ) ")" ))))) ; theorem :: CLOSURE3:6 (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Set (Var "M1")) ($#k5_relat_1 :::"|"::: ) (Set "(" ($#k1_closure3 :::"support"::: ) (Set (Var "M1")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "M2")) ($#k5_relat_1 :::"|"::: ) (Set "(" ($#k1_closure3 :::"support"::: ) (Set (Var "M2")) ")" )))) "holds" (Bool (Set (Var "M1")) ($#r8_pboole :::"="::: ) (Set (Var "M2"))))) ; theorem :: CLOSURE3:7 canceled; theorem :: CLOSURE3:8 (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "x")) "being" ($#m1_closure2 :::"Element"::: ) "of" (Set ($#k6_closure2 :::"Bool"::: ) (Set (Var "M"))) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "I")) (Bool "for" (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "x")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))))) "holds" (Bool "ex" (Set (Var "a")) "being" ($#m1_closure2 :::"Element"::: ) "of" (Set ($#k6_closure2 :::"Bool"::: ) (Set (Var "M"))) "st" (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "a")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Var "a")) "is" bbbadV2_FINSET_1()) & (Bool (Set ($#k1_closure3 :::"support"::: ) (Set (Var "a"))) "is" ($#v1_finset_1 :::"finite"::: ) ) & (Bool (Set (Var "a")) ($#r2_pboole :::"c="::: ) (Set (Var "x"))) ")" ))))))) ; definitionlet "I" be ($#m1_hidden :::"set"::: ) ; let "M" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); let "A" be ($#m1_subset_1 :::"SubsetFamily":::) "of" (Set (Const "M")); func :::"MSUnion"::: "A" -> ($#m3_pboole :::"ManySortedSubset"::: ) "of" "M" means :: CLOSURE3:def 2 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) "I")) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) "{" (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) where f "is" ($#m1_closure2 :::"Element"::: ) "of" (Set ($#k6_closure2 :::"Bool"::: ) "M") : (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) "A") "}" ))); end; :: deftheorem defines :::"MSUnion"::: CLOSURE3:def 2 : (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"SubsetFamily":::) "of" (Set (Var "M")) (Bool "for" (Set (Var "b4")) "being" ($#m3_pboole :::"ManySortedSubset"::: ) "of" (Set (Var "M")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k2_closure3 :::"MSUnion"::: ) (Set (Var "A")))) "iff" (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Var "I")))) "holds" (Bool (Set (Set (Var "b4")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) "{" (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) where f "is" ($#m1_closure2 :::"Element"::: ) "of" (Set ($#k6_closure2 :::"Bool"::: ) (Set (Var "M"))) : (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) "}" ))) ")" ))))); registrationlet "I" be ($#m1_hidden :::"set"::: ) ; let "M" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); let "A" be ($#v1_xboole_0 :::"empty"::: ) ($#m1_subset_1 :::"SubsetFamily":::) "of" (Set (Const "M")); cluster (Set ($#k2_closure3 :::"MSUnion"::: ) "A") -> bbbadV3_RELAT_1() ; end; theorem :: CLOSURE3:9 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"SubsetFamily":::) "of" (Set (Var "M")) "holds" (Bool (Set ($#k2_closure3 :::"MSUnion"::: ) (Set (Var "A"))) ($#r6_pboole :::"="::: ) (Set ($#k2_mboolean :::"union"::: ) (Set ($#k5_closure2 :::"|:"::: ) (Set (Var "A")) ($#k5_closure2 :::":|"::: ) )))))) ; definitionlet "I" be ($#m1_hidden :::"set"::: ) ; let "M" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); let "A", "B" be ($#m1_subset_1 :::"SubsetFamily":::) "of" (Set (Const "M")); :: original: :::"\/"::: redefine func "A" :::"\/"::: "B" -> ($#m1_subset_1 :::"SubsetFamily":::) "of" "M"; end; theorem :: CLOSURE3:10 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"SubsetFamily":::) "of" (Set (Var "M")) "holds" (Bool (Set ($#k2_closure3 :::"MSUnion"::: ) (Set "(" (Set (Var "A")) ($#k3_closure3 :::"\/"::: ) (Set (Var "B")) ")" )) ($#r6_pboole :::"="::: ) (Set (Set "(" ($#k2_closure3 :::"MSUnion"::: ) (Set (Var "A")) ")" ) ($#k2_pboole :::"\/"::: ) (Set "(" ($#k2_closure3 :::"MSUnion"::: ) (Set (Var "B")) ")" )))))) ; theorem :: CLOSURE3:11 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"SubsetFamily":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "B")))) "holds" (Bool (Set ($#k2_closure3 :::"MSUnion"::: ) (Set (Var "A"))) ($#r2_pboole :::"c="::: ) (Set ($#k2_closure3 :::"MSUnion"::: ) (Set (Var "B"))))))) ; definitionlet "I" be ($#m1_hidden :::"set"::: ) ; let "M" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); let "A", "B" be ($#m1_subset_1 :::"SubsetFamily":::) "of" (Set (Const "M")); :: original: :::"/\"::: redefine func "A" :::"/\"::: "B" -> ($#m1_subset_1 :::"SubsetFamily":::) "of" "M"; end; theorem :: CLOSURE3:12 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"SubsetFamily":::) "of" (Set (Var "M")) "holds" (Bool (Set ($#k2_closure3 :::"MSUnion"::: ) (Set "(" (Set (Var "A")) ($#k4_closure3 :::"/\"::: ) (Set (Var "B")) ")" )) ($#r2_pboole :::"c="::: ) (Set (Set "(" ($#k2_closure3 :::"MSUnion"::: ) (Set (Var "A")) ")" ) ($#k3_pboole :::"/\"::: ) (Set "(" ($#k2_closure3 :::"MSUnion"::: ) (Set (Var "B")) ")" )))))) ; theorem :: CLOSURE3:13 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "AA")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "AA")))) "holds" (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"SubsetFamily":::) "of" (Set (Var "M"))) ")" )) "holds" (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"SubsetFamily":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) "{" (Set "(" ($#k2_closure3 :::"MSUnion"::: ) (Set (Var "X")) ")" ) where X "is" ($#m1_subset_1 :::"SubsetFamily":::) "of" (Set (Var "M")) : (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set (Var "AA"))) "}" ) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) (Set (Var "AA"))))) "holds" (Bool (Set ($#k2_closure3 :::"MSUnion"::: ) (Set (Var "B"))) ($#r6_pboole :::"="::: ) (Set ($#k2_closure3 :::"MSUnion"::: ) (Set (Var "A")))))))) ; begin definitionlet "I" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "M" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); let "S" be ($#m1_subset_1 :::"SetOp":::) "of" (Set (Const "M")); attr "S" is :::"algebraic"::: means :: CLOSURE3:def 3 (Bool "for" (Set (Var "x")) "being" ($#m1_closure2 :::"Element"::: ) "of" (Set ($#k6_closure2 :::"Bool"::: ) "M") "st" (Bool (Bool (Set (Var "x")) ($#r8_pboole :::"="::: ) (Set "S" ($#k7_closure2 :::"."::: ) (Set (Var "x"))))) "holds" (Bool "ex" (Set (Var "A")) "being" ($#m1_subset_1 :::"SubsetFamily":::) "of" "M" "st" (Bool "(" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) "{" (Set "(" "S" ($#k7_closure2 :::"."::: ) (Set (Var "a")) ")" ) where a "is" ($#m1_closure2 :::"Element"::: ) "of" (Set ($#k6_closure2 :::"Bool"::: ) "M") : (Bool "(" (Bool (Set (Var "a")) "is" bbbadV2_FINSET_1()) & (Bool (Set ($#k1_closure3 :::"support"::: ) (Set (Var "a"))) "is" ($#v1_finset_1 :::"finite"::: ) ) & (Bool (Set (Var "a")) ($#r2_pboole :::"c="::: ) (Set (Var "x"))) ")" ) "}" ) & (Bool (Set (Var "x")) ($#r8_pboole :::"="::: ) (Set ($#k2_closure3 :::"MSUnion"::: ) (Set (Var "A")))) ")" ))); end; :: deftheorem defines :::"algebraic"::: CLOSURE3:def 3 : (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SetOp":::) "of" (Set (Var "M")) "holds" (Bool "(" (Bool (Set (Var "S")) "is" ($#v1_closure3 :::"algebraic"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_closure2 :::"Element"::: ) "of" (Set ($#k6_closure2 :::"Bool"::: ) (Set (Var "M"))) "st" (Bool (Bool (Set (Var "x")) ($#r8_pboole :::"="::: ) (Set (Set (Var "S")) ($#k7_closure2 :::"."::: ) (Set (Var "x"))))) "holds" (Bool "ex" (Set (Var "A")) "being" ($#m1_subset_1 :::"SubsetFamily":::) "of" (Set (Var "M")) "st" (Bool "(" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set (Var "S")) ($#k7_closure2 :::"."::: ) (Set (Var "a")) ")" ) where a "is" ($#m1_closure2 :::"Element"::: ) "of" (Set ($#k6_closure2 :::"Bool"::: ) (Set (Var "M"))) : (Bool "(" (Bool (Set (Var "a")) "is" bbbadV2_FINSET_1()) & (Bool (Set ($#k1_closure3 :::"support"::: ) (Set (Var "a"))) "is" ($#v1_finset_1 :::"finite"::: ) ) & (Bool (Set (Var "a")) ($#r2_pboole :::"c="::: ) (Set (Var "x"))) ")" ) "}" ) & (Bool (Set (Var "x")) ($#r8_pboole :::"="::: ) (Set ($#k2_closure3 :::"MSUnion"::: ) (Set (Var "A")))) ")" ))) ")" )))); registrationlet "I" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "M" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k6_closure2 :::"Bool"::: ) "M") ($#v4_relat_1 :::"-defined"::: ) (Set ($#k6_closure2 :::"Bool"::: ) "M") ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) bbbadV1_PARTFUN1((Set ($#k6_closure2 :::"Bool"::: ) "M")) ($#v1_funct_2 :::"quasi_total"::: ) ($#v7_closure2 :::"reflexive"::: ) ($#v8_closure2 :::"monotonic"::: ) ($#v9_closure2 :::"idempotent"::: ) ($#v1_closure3 :::"algebraic"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k6_closure2 :::"Bool"::: ) "M" ")" ) "," (Set "(" ($#k6_closure2 :::"Bool"::: ) "M" ")" ) ($#k2_zfmisc_1 :::":]"::: ) )); end; definitionlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) ; let "IT" be ($#l1_closure2 :::"ClosureSystem":::) "of" (Set (Const "S")); attr "IT" is :::"algebraic"::: means :: CLOSURE3:def 4 (Bool (Set ($#k12_closure2 :::"ClSys->ClOp"::: ) "IT") "is" ($#v1_closure3 :::"algebraic"::: ) ); end; :: deftheorem defines :::"algebraic"::: CLOSURE3:def 4 : (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "IT")) "being" ($#l1_closure2 :::"ClosureSystem":::) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v2_closure3 :::"algebraic"::: ) ) "iff" (Bool (Set ($#k12_closure2 :::"ClSys->ClOp"::: ) (Set (Var "IT"))) "is" ($#v1_closure3 :::"algebraic"::: ) ) ")" ))); definitionlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "MA" be ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Const "S")); func :::"SubAlgCl"::: "MA" -> ($#v11_closure2 :::"strict"::: ) ($#l1_closure2 :::"ClosureStr"::: ) "over" (Set ($#g1_struct_0 :::"1-sorted"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S") "#)" ) means :: CLOSURE3:def 5 (Bool "(" (Bool (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" "MA")) & (Bool (Set "the" ($#u1_closure2 :::"Family"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set ($#k6_msualg_2 :::"SubSort"::: ) "MA")) ")" ); end; :: deftheorem defines :::"SubAlgCl"::: CLOSURE3:def 5 : (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 "MA")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "b3")) "being" ($#v11_closure2 :::"strict"::: ) ($#l1_closure2 :::"ClosureStr"::: ) "over" (Set ($#g1_struct_0 :::"1-sorted"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) "#)" ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k5_closure3 :::"SubAlgCl"::: ) (Set (Var "MA")))) "iff" (Bool "(" (Bool (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "MA")))) & (Bool (Set "the" ($#u1_closure2 :::"Family"::: ) "of" (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set ($#k6_msualg_2 :::"SubSort"::: ) (Set (Var "MA")))) ")" ) ")" )))); theorem :: CLOSURE3:14 (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 "MA")) "being" ($#v3_msualg_1 :::"strict"::: ) ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) "holds" (Bool (Set ($#k6_msualg_2 :::"SubSort"::: ) (Set (Var "MA"))) "is" ($#v4_closure2 :::"absolutely-multiplicative"::: ) ($#m1_subset_1 :::"SubsetFamily":::) "of" (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "MA")))))) ; registrationlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "MA" be ($#v3_msualg_1 :::"strict"::: ) ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Const "S")); cluster (Set ($#k5_closure3 :::"SubAlgCl"::: ) "MA") -> ($#v11_closure2 :::"strict"::: ) ($#v15_closure2 :::"absolutely-multiplicative"::: ) ; end; registrationlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "MA" be ($#v3_msualg_1 :::"strict"::: ) ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Const "S")); cluster (Set ($#k5_closure3 :::"SubAlgCl"::: ) "MA") -> ($#v11_closure2 :::"strict"::: ) ($#v2_closure3 :::"algebraic"::: ) ; end;