:: CLOSURE1 semantic presentation begin scheme :: CLOSURE1:sch 1 MSSUBSET{ F1() -> ($#m1_hidden :::"set"::: ) , F2() -> bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set F1 "(" ")" ), F3() -> ($#m1_hidden :::"ManySortedSet":::) "of" (Set F1 "(" ")" ), P1[ ($#m1_hidden :::"set"::: ) ] } : "(" (Bool (Bool "(" "for" (Set (Var "X")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set F1 "(" ")" ) "holds" (Bool "(" (Bool (Set (Var "X")) ($#r1_pboole :::"in"::: ) (Set F2 "(" ")" )) "iff" (Bool "(" (Bool (Set (Var "X")) ($#r1_pboole :::"in"::: ) (Set F3 "(" ")" )) & (Bool P1[(Set (Var "X"))]) ")" ) ")" ) ")" )) "implies" (Bool (Set F2 "(" ")" ) ($#r2_pboole :::"c="::: ) (Set F3 "(" ")" )) ")" proof end; theorem :: CLOSURE1:1 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r1_tarski :::"c="::: ) (Set (Var "y")))) "holds" (Bool "{" (Set (Var "t")) where t "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) : (Bool (Set (Var "y")) ($#r1_tarski :::"c="::: ) (Set (Var "t"))) "}" ($#r1_tarski :::"c="::: ) "{" (Set (Var "z")) where z "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) : (Bool (Set (Var "x")) ($#r1_tarski :::"c="::: ) (Set (Var "z"))) "}" ))) ; theorem :: CLOSURE1:2 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool "ex" (Set (Var "A")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Set (Var "A")) ($#r1_pboole :::"in"::: ) (Set (Var "M"))))) "holds" (Bool (Set (Var "M")) "is" bbbadV2_RELAT_1()))) ; registrationlet "I" be ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_hidden :::"ManySortedFunction":::) "of" (Set (Const "I")); let "A" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); cluster (Set "F" ($#k15_pralg_1 :::".."::: ) "A") -> "I" ($#v4_relat_1 :::"-defined"::: ) ($#v1_partfun1 :::"total"::: ) for"I" ($#v4_relat_1 :::"-defined"::: ) ($#m1_hidden :::"Function":::); end; definitionlet "I" be ($#m1_hidden :::"set"::: ) ; let "A", "B" be bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); let "F" be ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set (Const "A")) "," (Set (Const "B")); let "X" be ($#m1_pboole :::"Element"::: ) "of" (Set (Const "A")); :: original: :::".."::: redefine func "F" :::".."::: "X" -> ($#m1_pboole :::"Element"::: ) "of" "B"; end; theorem :: CLOSURE1:3 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "X")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "B")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "F")) "being" ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) "st" (Bool (Bool (Set (Var "X")) ($#r1_pboole :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set (Set (Var "F")) ($#k16_pralg_1 :::".."::: ) (Set (Var "X"))) ($#r1_pboole :::"in"::: ) (Set (Var "B"))))))) ; theorem :: CLOSURE1:4 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_hidden :::"ManySortedFunction":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "A")) ($#r1_pboole :::"in"::: ) (Set ($#k2_funct_6 :::"doms"::: ) (Set (Var "G"))))) "holds" (Bool (Set (Set (Var "F")) ($#k16_pralg_1 :::".."::: ) (Set "(" (Set (Var "G")) ($#k16_pralg_1 :::".."::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "F")) ($#k8_pboole :::"**"::: ) (Set (Var "G")) ")" ) ($#k15_pralg_1 :::".."::: ) (Set (Var "A"))))))) ; theorem :: CLOSURE1:5 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"ManySortedFunction":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_msualg_3 :::""1-1""::: ) )) "holds" (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "A")) ($#r1_pboole :::"in"::: ) (Set ($#k2_funct_6 :::"doms"::: ) (Set (Var "F")))) & (Bool (Set (Var "B")) ($#r1_pboole :::"in"::: ) (Set ($#k2_funct_6 :::"doms"::: ) (Set (Var "F")))) & (Bool (Set (Set (Var "F")) ($#k16_pralg_1 :::".."::: ) (Set (Var "A"))) ($#r6_pboole :::"="::: ) (Set (Set (Var "F")) ($#k16_pralg_1 :::".."::: ) (Set (Var "B"))))) "holds" (Bool (Set (Var "A")) ($#r6_pboole :::"="::: ) (Set (Var "B")))))) ; theorem :: CLOSURE1:6 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"ManySortedFunction":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set ($#k2_funct_6 :::"doms"::: ) (Set (Var "F"))) "is" bbbadV2_RELAT_1()) & (Bool "(" "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "A")) ($#r1_pboole :::"in"::: ) (Set ($#k2_funct_6 :::"doms"::: ) (Set (Var "F")))) & (Bool (Set (Var "B")) ($#r1_pboole :::"in"::: ) (Set ($#k2_funct_6 :::"doms"::: ) (Set (Var "F")))) & (Bool (Set (Set (Var "F")) ($#k16_pralg_1 :::".."::: ) (Set (Var "A"))) ($#r6_pboole :::"="::: ) (Set (Set (Var "F")) ($#k16_pralg_1 :::".."::: ) (Set (Var "B"))))) "holds" (Bool (Set (Var "A")) ($#r6_pboole :::"="::: ) (Set (Var "B"))) ")" )) "holds" (Bool (Set (Var "F")) "is" ($#v1_msualg_3 :::""1-1""::: ) ))) ; theorem :: CLOSURE1:7 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) "st" (Bool (Bool "(" "for" (Set (Var "M")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "M")) ($#r1_pboole :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set (Set (Var "F")) ($#k16_pralg_1 :::".."::: ) (Set (Var "M"))) ($#r6_pboole :::"="::: ) (Set (Set (Var "G")) ($#k16_pralg_1 :::".."::: ) (Set (Var "M")))) ")" )) "holds" (Bool (Set (Var "F")) ($#r6_pboole :::"="::: ) (Set (Var "G")))))) ; registrationlet "I" be ($#m1_hidden :::"set"::: ) ; let "M" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); cluster ($#v1_relat_1 :::"Relation-like"::: ) bbbadV3_RELAT_1() "I" ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_partfun1 :::"total"::: ) bbbadV2_FINSET_1() for ($#m1_pboole :::"Element"::: ) "of" (Set ($#k5_mssubfam :::"bool"::: ) "M"); end; begin definitionlet "I" be ($#m1_hidden :::"set"::: ) ; let "M" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); mode MSSetOp of "M" is ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set ($#k5_mssubfam :::"bool"::: ) "M") "," (Set ($#k5_mssubfam :::"bool"::: ) "M"); end; definitionlet "I" be ($#m1_hidden :::"set"::: ) ; let "M" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); let "O" be ($#m2_pboole :::"MSSetOp":::) "of" (Set (Const "M")); let "X" be ($#m1_pboole :::"Element"::: ) "of" (Set ($#k5_mssubfam :::"bool"::: ) (Set (Const "M"))); :: original: :::".."::: redefine func "O" :::".."::: "X" -> ($#m1_pboole :::"Element"::: ) "of" (Set ($#k5_mssubfam :::"bool"::: ) "M"); end; definitionlet "I" be ($#m1_hidden :::"set"::: ) ; let "M" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); let "IT" be ($#m2_pboole :::"MSSetOp":::) "of" (Set (Const "M")); attr "IT" is :::"reflexive"::: means :: CLOSURE1:def 1 (Bool "for" (Set (Var "X")) "being" ($#m1_pboole :::"Element"::: ) "of" (Set ($#k5_mssubfam :::"bool"::: ) "M") "holds" (Bool (Set (Var "X")) ($#r2_pboole :::"c="::: ) (Set "IT" ($#k2_closure1 :::".."::: ) (Set (Var "X"))))); attr "IT" is :::"monotonic"::: means :: CLOSURE1:def 2 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_pboole :::"Element"::: ) "of" (Set ($#k5_mssubfam :::"bool"::: ) "M") "st" (Bool (Bool (Set (Var "X")) ($#r2_pboole :::"c="::: ) (Set (Var "Y")))) "holds" (Bool (Set "IT" ($#k2_closure1 :::".."::: ) (Set (Var "X"))) ($#r2_pboole :::"c="::: ) (Set "IT" ($#k2_closure1 :::".."::: ) (Set (Var "Y"))))); attr "IT" is :::"idempotent"::: means :: CLOSURE1:def 3 (Bool "for" (Set (Var "X")) "being" ($#m1_pboole :::"Element"::: ) "of" (Set ($#k5_mssubfam :::"bool"::: ) "M") "holds" (Bool (Set "IT" ($#k2_closure1 :::".."::: ) (Set (Var "X"))) ($#r6_pboole :::"="::: ) (Set "IT" ($#k2_closure1 :::".."::: ) (Set "(" "IT" ($#k2_closure1 :::".."::: ) (Set (Var "X")) ")" )))); attr "IT" is :::"topological"::: means :: CLOSURE1:def 4 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_pboole :::"Element"::: ) "of" (Set ($#k5_mssubfam :::"bool"::: ) "M") "holds" (Bool (Set "IT" ($#k16_pralg_1 :::".."::: ) (Set "(" (Set (Var "X")) ($#k2_pboole :::"\/"::: ) (Set (Var "Y")) ")" )) ($#r6_pboole :::"="::: ) (Set (Set "(" "IT" ($#k2_closure1 :::".."::: ) (Set (Var "X")) ")" ) ($#k2_pboole :::"\/"::: ) (Set "(" "IT" ($#k2_closure1 :::".."::: ) (Set (Var "Y")) ")" )))); end; :: deftheorem defines :::"reflexive"::: CLOSURE1:def 1 : (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 "IT")) "being" ($#m2_pboole :::"MSSetOp":::) "of" (Set (Var "M")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v1_closure1 :::"reflexive"::: ) ) "iff" (Bool "for" (Set (Var "X")) "being" ($#m1_pboole :::"Element"::: ) "of" (Set ($#k5_mssubfam :::"bool"::: ) (Set (Var "M"))) "holds" (Bool (Set (Var "X")) ($#r2_pboole :::"c="::: ) (Set (Set (Var "IT")) ($#k2_closure1 :::".."::: ) (Set (Var "X"))))) ")" )))); :: deftheorem defines :::"monotonic"::: CLOSURE1: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 "IT")) "being" ($#m2_pboole :::"MSSetOp":::) "of" (Set (Var "M")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v2_closure1 :::"monotonic"::: ) ) "iff" (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_pboole :::"Element"::: ) "of" (Set ($#k5_mssubfam :::"bool"::: ) (Set (Var "M"))) "st" (Bool (Bool (Set (Var "X")) ($#r2_pboole :::"c="::: ) (Set (Var "Y")))) "holds" (Bool (Set (Set (Var "IT")) ($#k2_closure1 :::".."::: ) (Set (Var "X"))) ($#r2_pboole :::"c="::: ) (Set (Set (Var "IT")) ($#k2_closure1 :::".."::: ) (Set (Var "Y"))))) ")" )))); :: deftheorem defines :::"idempotent"::: CLOSURE1:def 3 : (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 "IT")) "being" ($#m2_pboole :::"MSSetOp":::) "of" (Set (Var "M")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v3_closure1 :::"idempotent"::: ) ) "iff" (Bool "for" (Set (Var "X")) "being" ($#m1_pboole :::"Element"::: ) "of" (Set ($#k5_mssubfam :::"bool"::: ) (Set (Var "M"))) "holds" (Bool (Set (Set (Var "IT")) ($#k2_closure1 :::".."::: ) (Set (Var "X"))) ($#r6_pboole :::"="::: ) (Set (Set (Var "IT")) ($#k2_closure1 :::".."::: ) (Set "(" (Set (Var "IT")) ($#k2_closure1 :::".."::: ) (Set (Var "X")) ")" )))) ")" )))); :: deftheorem defines :::"topological"::: CLOSURE1:def 4 : (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 "IT")) "being" ($#m2_pboole :::"MSSetOp":::) "of" (Set (Var "M")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v4_closure1 :::"topological"::: ) ) "iff" (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_pboole :::"Element"::: ) "of" (Set ($#k5_mssubfam :::"bool"::: ) (Set (Var "M"))) "holds" (Bool (Set (Set (Var "IT")) ($#k16_pralg_1 :::".."::: ) (Set "(" (Set (Var "X")) ($#k2_pboole :::"\/"::: ) (Set (Var "Y")) ")" )) ($#r6_pboole :::"="::: ) (Set (Set "(" (Set (Var "IT")) ($#k2_closure1 :::".."::: ) (Set (Var "X")) ")" ) ($#k2_pboole :::"\/"::: ) (Set "(" (Set (Var "IT")) ($#k2_closure1 :::".."::: ) (Set (Var "Y")) ")" )))) ")" )))); theorem :: CLOSURE1:8 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "X")) "being" ($#m1_pboole :::"Element"::: ) "of" (Set (Var "M")) "holds" (Bool (Set (Var "X")) ($#r6_pboole :::"="::: ) (Set (Set "(" ($#k2_msualg_3 :::"id"::: ) (Set (Var "M")) ")" ) ($#k1_closure1 :::".."::: ) (Set (Var "X"))))))) ; theorem :: CLOSURE1:9 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_pboole :::"Element"::: ) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "X")) ($#r2_pboole :::"c="::: ) (Set (Var "Y")))) "holds" (Bool (Set (Set "(" ($#k2_msualg_3 :::"id"::: ) (Set (Var "M")) ")" ) ($#k1_closure1 :::".."::: ) (Set (Var "X"))) ($#r2_pboole :::"c="::: ) (Set (Set "(" ($#k2_msualg_3 :::"id"::: ) (Set (Var "M")) ")" ) ($#k1_closure1 :::".."::: ) (Set (Var "Y"))))))) ; theorem :: CLOSURE1:10 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_pboole :::"Element"::: ) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Set (Var "X")) ($#k2_pboole :::"\/"::: ) (Set (Var "Y"))) "is" ($#m1_pboole :::"Element"::: ) "of" (Set (Var "M")))) "holds" (Bool (Set (Set "(" ($#k2_msualg_3 :::"id"::: ) (Set (Var "M")) ")" ) ($#k16_pralg_1 :::".."::: ) (Set "(" (Set (Var "X")) ($#k2_pboole :::"\/"::: ) (Set (Var "Y")) ")" )) ($#r6_pboole :::"="::: ) (Set (Set "(" (Set "(" ($#k2_msualg_3 :::"id"::: ) (Set (Var "M")) ")" ) ($#k1_closure1 :::".."::: ) (Set (Var "X")) ")" ) ($#k2_pboole :::"\/"::: ) (Set "(" (Set "(" ($#k2_msualg_3 :::"id"::: ) (Set (Var "M")) ")" ) ($#k1_closure1 :::".."::: ) (Set (Var "Y")) ")" )))))) ; theorem :: CLOSURE1: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 "X")) "being" ($#m1_pboole :::"Element"::: ) "of" (Set ($#k5_mssubfam :::"bool"::: ) (Set (Var "M"))) (Bool "for" (Set (Var "i")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Var "I"))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set "(" (Set "(" ($#k2_msualg_3 :::"id"::: ) (Set "(" ($#k5_mssubfam :::"bool"::: ) (Set (Var "M")) ")" ) ")" ) ($#k2_closure1 :::".."::: ) (Set (Var "X")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))))) "holds" (Bool "ex" (Set (Var "Y")) "being" bbbadV2_FINSET_1() ($#m1_pboole :::"Element"::: ) "of" (Set ($#k5_mssubfam :::"bool"::: ) (Set (Var "M"))) "st" (Bool "(" (Bool (Set (Var "Y")) ($#r2_pboole :::"c="::: ) (Set (Var "X"))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set "(" (Set "(" ($#k2_msualg_3 :::"id"::: ) (Set "(" ($#k5_mssubfam :::"bool"::: ) (Set (Var "M")) ")" ) ")" ) ($#k2_closure1 :::".."::: ) (Set (Var "Y")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) ")" )))))) ; registrationlet "I" be ($#m1_hidden :::"set"::: ) ; let "M" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); cluster ($#v1_relat_1 :::"Relation-like"::: ) "I" ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_partfun1 :::"total"::: ) ($#v1_funcop_1 :::"Function-yielding"::: ) bbbadV2_FUNCOP_1() ($#v1_closure1 :::"reflexive"::: ) ($#v2_closure1 :::"monotonic"::: ) ($#v3_closure1 :::"idempotent"::: ) ($#v4_closure1 :::"topological"::: ) for ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set ($#k5_mssubfam :::"bool"::: ) "M") "," (Set ($#k5_mssubfam :::"bool"::: ) "M"); end; theorem :: CLOSURE1:12 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool (Set ($#k2_msualg_3 :::"id"::: ) (Set "(" ($#k5_mssubfam :::"bool"::: ) (Set (Var "A")) ")" )) "is" ($#v1_closure1 :::"reflexive"::: ) ($#m2_pboole :::"MSSetOp":::) "of" (Set (Var "A"))))) ; theorem :: CLOSURE1:13 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool (Set ($#k2_msualg_3 :::"id"::: ) (Set "(" ($#k5_mssubfam :::"bool"::: ) (Set (Var "A")) ")" )) "is" ($#v2_closure1 :::"monotonic"::: ) ($#m2_pboole :::"MSSetOp":::) "of" (Set (Var "A"))))) ; theorem :: CLOSURE1:14 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool (Set ($#k2_msualg_3 :::"id"::: ) (Set "(" ($#k5_mssubfam :::"bool"::: ) (Set (Var "A")) ")" )) "is" ($#v3_closure1 :::"idempotent"::: ) ($#m2_pboole :::"MSSetOp":::) "of" (Set (Var "A"))))) ; theorem :: CLOSURE1:15 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool (Set ($#k2_msualg_3 :::"id"::: ) (Set "(" ($#k5_mssubfam :::"bool"::: ) (Set (Var "A")) ")" )) "is" ($#v4_closure1 :::"topological"::: ) ($#m2_pboole :::"MSSetOp":::) "of" (Set (Var "A"))))) ; theorem :: CLOSURE1:16 (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 "P")) "being" ($#m2_pboole :::"MSSetOp":::) "of" (Set (Var "M")) (Bool "for" (Set (Var "E")) "being" ($#m1_pboole :::"Element"::: ) "of" (Set ($#k5_mssubfam :::"bool"::: ) (Set (Var "M"))) "st" (Bool (Bool (Set (Var "E")) ($#r6_pboole :::"="::: ) (Set (Var "M"))) & (Bool (Set (Var "P")) "is" ($#v1_closure1 :::"reflexive"::: ) )) "holds" (Bool (Set (Var "E")) ($#r6_pboole :::"="::: ) (Set (Set (Var "P")) ($#k2_closure1 :::".."::: ) (Set (Var "E")))))))) ; theorem :: CLOSURE1:17 (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 "P")) "being" ($#m2_pboole :::"MSSetOp":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "P")) "is" ($#v1_closure1 :::"reflexive"::: ) ) & (Bool "(" "for" (Set (Var "X")) "being" ($#m1_pboole :::"Element"::: ) "of" (Set ($#k5_mssubfam :::"bool"::: ) (Set (Var "M"))) "holds" (Bool (Set (Set (Var "P")) ($#k2_closure1 :::".."::: ) (Set (Var "X"))) ($#r2_pboole :::"c="::: ) (Set (Var "X"))) ")" )) "holds" (Bool (Set (Var "P")) "is" ($#v3_closure1 :::"idempotent"::: ) )))) ; theorem :: CLOSURE1:18 (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 "P")) "being" ($#m2_pboole :::"MSSetOp":::) "of" (Set (Var "M")) (Bool "for" (Set (Var "E")) "," (Set (Var "T")) "being" ($#m1_pboole :::"Element"::: ) "of" (Set ($#k5_mssubfam :::"bool"::: ) (Set (Var "M"))) "st" (Bool (Bool (Set (Var "P")) "is" ($#v2_closure1 :::"monotonic"::: ) )) "holds" (Bool (Set (Set (Var "P")) ($#k16_pralg_1 :::".."::: ) (Set "(" (Set (Var "E")) ($#k3_pboole :::"/\"::: ) (Set (Var "T")) ")" )) ($#r2_pboole :::"c="::: ) (Set (Set "(" (Set (Var "P")) ($#k2_closure1 :::".."::: ) (Set (Var "E")) ")" ) ($#k3_pboole :::"/\"::: ) (Set "(" (Set (Var "P")) ($#k2_closure1 :::".."::: ) (Set (Var "T")) ")" ))))))) ; registrationlet "I" be ($#m1_hidden :::"set"::: ) ; let "M" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); cluster ($#v4_closure1 :::"topological"::: ) -> ($#v2_closure1 :::"monotonic"::: ) for ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set ($#k5_mssubfam :::"bool"::: ) "M") "," (Set ($#k5_mssubfam :::"bool"::: ) "M"); end; theorem :: CLOSURE1:19 (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 "P")) "being" ($#m2_pboole :::"MSSetOp":::) "of" (Set (Var "M")) (Bool "for" (Set (Var "E")) "," (Set (Var "T")) "being" ($#m1_pboole :::"Element"::: ) "of" (Set ($#k5_mssubfam :::"bool"::: ) (Set (Var "M"))) "st" (Bool (Bool (Set (Var "P")) "is" ($#v4_closure1 :::"topological"::: ) )) "holds" (Bool (Set (Set "(" (Set (Var "P")) ($#k2_closure1 :::".."::: ) (Set (Var "E")) ")" ) ($#k4_pboole :::"\"::: ) (Set "(" (Set (Var "P")) ($#k2_closure1 :::".."::: ) (Set (Var "T")) ")" )) ($#r2_pboole :::"c="::: ) (Set (Set (Var "P")) ($#k16_pralg_1 :::".."::: ) (Set "(" (Set (Var "E")) ($#k4_pboole :::"\"::: ) (Set (Var "T")) ")" ))))))) ; definitionlet "I" be ($#m1_hidden :::"set"::: ) ; let "M" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); let "R", "P" be ($#m2_pboole :::"MSSetOp":::) "of" (Set (Const "M")); :: original: :::"**"::: redefine func "P" :::"**"::: "R" -> ($#m2_pboole :::"MSSetOp":::) "of" "M"; end; theorem :: CLOSURE1:20 (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 "P")) "," (Set (Var "R")) "being" ($#m2_pboole :::"MSSetOp":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "P")) "is" ($#v1_closure1 :::"reflexive"::: ) ) & (Bool (Set (Var "R")) "is" ($#v1_closure1 :::"reflexive"::: ) )) "holds" (Bool (Set (Set (Var "P")) ($#k3_closure1 :::"**"::: ) (Set (Var "R"))) "is" ($#v1_closure1 :::"reflexive"::: ) )))) ; theorem :: CLOSURE1:21 (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 "P")) "," (Set (Var "R")) "being" ($#m2_pboole :::"MSSetOp":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "P")) "is" ($#v2_closure1 :::"monotonic"::: ) ) & (Bool (Set (Var "R")) "is" ($#v2_closure1 :::"monotonic"::: ) )) "holds" (Bool (Set (Set (Var "P")) ($#k3_closure1 :::"**"::: ) (Set (Var "R"))) "is" ($#v2_closure1 :::"monotonic"::: ) )))) ; theorem :: CLOSURE1:22 (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 "P")) "," (Set (Var "R")) "being" ($#m2_pboole :::"MSSetOp":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "P")) "is" ($#v3_closure1 :::"idempotent"::: ) ) & (Bool (Set (Var "R")) "is" ($#v3_closure1 :::"idempotent"::: ) ) & (Bool (Set (Set (Var "P")) ($#k3_closure1 :::"**"::: ) (Set (Var "R"))) ($#r6_pboole :::"="::: ) (Set (Set (Var "R")) ($#k3_closure1 :::"**"::: ) (Set (Var "P"))))) "holds" (Bool (Set (Set (Var "P")) ($#k3_closure1 :::"**"::: ) (Set (Var "R"))) "is" ($#v3_closure1 :::"idempotent"::: ) )))) ; theorem :: CLOSURE1:23 (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 "P")) "," (Set (Var "R")) "being" ($#m2_pboole :::"MSSetOp":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "P")) "is" ($#v4_closure1 :::"topological"::: ) ) & (Bool (Set (Var "R")) "is" ($#v4_closure1 :::"topological"::: ) )) "holds" (Bool (Set (Set (Var "P")) ($#k3_closure1 :::"**"::: ) (Set (Var "R"))) "is" ($#v4_closure1 :::"topological"::: ) )))) ; theorem :: CLOSURE1:24 (Bool "for" (Set (Var "i")) "," (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "P")) "being" ($#m2_pboole :::"MSSetOp":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "P")) "is" ($#v1_closure1 :::"reflexive"::: ) ) & (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Var "I"))) & (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))))) "holds" (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k9_setfam_1 :::"bool"::: ) (Set "(" (Set (Var "M")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" )) "holds" (Bool (Set (Var "x")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))))))))) ; theorem :: CLOSURE1:25 (Bool "for" (Set (Var "i")) "," (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "P")) "being" ($#m2_pboole :::"MSSetOp":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "P")) "is" ($#v2_closure1 :::"monotonic"::: ) ) & (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Var "I"))) & (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))))) "holds" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k9_setfam_1 :::"bool"::: ) (Set "(" (Set (Var "M")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" )) "st" (Bool (Bool (Set (Var "x")) ($#r1_tarski :::"c="::: ) (Set (Var "y")))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "y"))))))))) ; theorem :: CLOSURE1:26 (Bool "for" (Set (Var "i")) "," (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "P")) "being" ($#m2_pboole :::"MSSetOp":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "P")) "is" ($#v3_closure1 :::"idempotent"::: ) ) & (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Var "I"))) & (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))))) "holds" (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k9_setfam_1 :::"bool"::: ) (Set "(" (Set (Var "M")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" )) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" )))))))) ; theorem :: CLOSURE1:27 (Bool "for" (Set (Var "i")) "," (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "P")) "being" ($#m2_pboole :::"MSSetOp":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "P")) "is" ($#v4_closure1 :::"topological"::: ) ) & (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Var "I"))) & (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))))) "holds" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k9_setfam_1 :::"bool"::: ) (Set "(" (Set (Var "M")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" )) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "y")) ")" )))))))) ; begin definitionlet "S" be ($#l1_struct_0 :::"1-sorted"::: ) ; attr "c2" is :::"strict"::: ; struct :::"MSClosureStr"::: "over" "S" -> ($#l2_msualg_1 :::"many-sorted"::: ) "over" "S"; aggr :::"MSClosureStr":::(# :::"Sorts":::, :::"Family"::: #) -> ($#l1_closure1 :::"MSClosureStr"::: ) "over" "S"; sel :::"Family"::: "c2" -> ($#m3_pboole :::"MSSubsetFamily":::) "of" (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" "c2"); end; definitionlet "S" be ($#l1_struct_0 :::"1-sorted"::: ) ; let "IT" be ($#l1_closure1 :::"MSClosureStr"::: ) "over" (Set (Const "S")); attr "IT" is :::"additive"::: means :: CLOSURE1:def 5 (Bool (Set "the" ($#u1_closure1 :::"Family"::: ) "of" "IT") "is" ($#v1_mssubfam :::"additive"::: ) ); attr "IT" is :::"absolutely-additive"::: means :: CLOSURE1:def 6 (Bool (Set "the" ($#u1_closure1 :::"Family"::: ) "of" "IT") "is" ($#v2_mssubfam :::"absolutely-additive"::: ) ); attr "IT" is :::"multiplicative"::: means :: CLOSURE1:def 7 (Bool (Set "the" ($#u1_closure1 :::"Family"::: ) "of" "IT") "is" ($#v3_mssubfam :::"multiplicative"::: ) ); attr "IT" is :::"absolutely-multiplicative"::: means :: CLOSURE1:def 8 (Bool (Set "the" ($#u1_closure1 :::"Family"::: ) "of" "IT") "is" ($#v4_mssubfam :::"absolutely-multiplicative"::: ) ); attr "IT" is :::"properly-upper-bound"::: means :: CLOSURE1:def 9 (Bool (Set "the" ($#u1_closure1 :::"Family"::: ) "of" "IT") "is" ($#v5_mssubfam :::"properly-upper-bound"::: ) ); attr "IT" is :::"properly-lower-bound"::: means :: CLOSURE1:def 10 (Bool (Set "the" ($#u1_closure1 :::"Family"::: ) "of" "IT") "is" ($#v6_mssubfam :::"properly-lower-bound"::: ) ); end; :: deftheorem defines :::"additive"::: CLOSURE1:def 5 : (Bool "for" (Set (Var "S")) "being" ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "IT")) "being" ($#l1_closure1 :::"MSClosureStr"::: ) "over" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v6_closure1 :::"additive"::: ) ) "iff" (Bool (Set "the" ($#u1_closure1 :::"Family"::: ) "of" (Set (Var "IT"))) "is" ($#v1_mssubfam :::"additive"::: ) ) ")" ))); :: deftheorem defines :::"absolutely-additive"::: CLOSURE1:def 6 : (Bool "for" (Set (Var "S")) "being" ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "IT")) "being" ($#l1_closure1 :::"MSClosureStr"::: ) "over" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v7_closure1 :::"absolutely-additive"::: ) ) "iff" (Bool (Set "the" ($#u1_closure1 :::"Family"::: ) "of" (Set (Var "IT"))) "is" ($#v2_mssubfam :::"absolutely-additive"::: ) ) ")" ))); :: deftheorem defines :::"multiplicative"::: CLOSURE1:def 7 : (Bool "for" (Set (Var "S")) "being" ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "IT")) "being" ($#l1_closure1 :::"MSClosureStr"::: ) "over" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v8_closure1 :::"multiplicative"::: ) ) "iff" (Bool (Set "the" ($#u1_closure1 :::"Family"::: ) "of" (Set (Var "IT"))) "is" ($#v3_mssubfam :::"multiplicative"::: ) ) ")" ))); :: deftheorem defines :::"absolutely-multiplicative"::: CLOSURE1:def 8 : (Bool "for" (Set (Var "S")) "being" ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "IT")) "being" ($#l1_closure1 :::"MSClosureStr"::: ) "over" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v9_closure1 :::"absolutely-multiplicative"::: ) ) "iff" (Bool (Set "the" ($#u1_closure1 :::"Family"::: ) "of" (Set (Var "IT"))) "is" ($#v4_mssubfam :::"absolutely-multiplicative"::: ) ) ")" ))); :: deftheorem defines :::"properly-upper-bound"::: CLOSURE1:def 9 : (Bool "for" (Set (Var "S")) "being" ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "IT")) "being" ($#l1_closure1 :::"MSClosureStr"::: ) "over" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v10_closure1 :::"properly-upper-bound"::: ) ) "iff" (Bool (Set "the" ($#u1_closure1 :::"Family"::: ) "of" (Set (Var "IT"))) "is" ($#v5_mssubfam :::"properly-upper-bound"::: ) ) ")" ))); :: deftheorem defines :::"properly-lower-bound"::: CLOSURE1:def 10 : (Bool "for" (Set (Var "S")) "being" ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "IT")) "being" ($#l1_closure1 :::"MSClosureStr"::: ) "over" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v11_closure1 :::"properly-lower-bound"::: ) ) "iff" (Bool (Set "the" ($#u1_closure1 :::"Family"::: ) "of" (Set (Var "IT"))) "is" ($#v6_mssubfam :::"properly-lower-bound"::: ) ) ")" ))); definitionlet "S" be ($#l1_struct_0 :::"1-sorted"::: ) ; let "MS" be ($#l2_msualg_1 :::"many-sorted"::: ) "over" (Set (Const "S")); func :::"MSFull"::: "MS" -> ($#l1_closure1 :::"MSClosureStr"::: ) "over" "S" equals :: CLOSURE1:def 11 (Set ($#g1_closure1 :::"MSClosureStr"::: ) "(#" (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" "MS") "," (Set "(" ($#k5_mssubfam :::"bool"::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" "MS") ")" ) "#)" ); end; :: deftheorem defines :::"MSFull"::: CLOSURE1:def 11 : (Bool "for" (Set (Var "S")) "being" ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "MS")) "being" ($#l2_msualg_1 :::"many-sorted"::: ) "over" (Set (Var "S")) "holds" (Bool (Set ($#k4_closure1 :::"MSFull"::: ) (Set (Var "MS"))) ($#r1_hidden :::"="::: ) (Set ($#g1_closure1 :::"MSClosureStr"::: ) "(#" (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "MS"))) "," (Set "(" ($#k5_mssubfam :::"bool"::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "MS"))) ")" ) "#)" )))); registrationlet "S" be ($#l1_struct_0 :::"1-sorted"::: ) ; let "MS" be ($#l2_msualg_1 :::"many-sorted"::: ) "over" (Set (Const "S")); cluster (Set ($#k4_closure1 :::"MSFull"::: ) "MS") -> ($#v5_closure1 :::"strict"::: ) ($#v6_closure1 :::"additive"::: ) ($#v7_closure1 :::"absolutely-additive"::: ) ($#v8_closure1 :::"multiplicative"::: ) ($#v9_closure1 :::"absolutely-multiplicative"::: ) ($#v10_closure1 :::"properly-upper-bound"::: ) ($#v11_closure1 :::"properly-lower-bound"::: ) ; end; registrationlet "S" be ($#l1_struct_0 :::"1-sorted"::: ) ; let "MS" be ($#v4_msualg_1 :::"non-empty"::: ) ($#l2_msualg_1 :::"many-sorted"::: ) "over" (Set (Const "S")); cluster (Set ($#k4_closure1 :::"MSFull"::: ) "MS") -> ($#v4_msualg_1 :::"non-empty"::: ) ; end; registrationlet "S" be ($#l1_struct_0 :::"1-sorted"::: ) ; cluster ($#v4_msualg_1 :::"non-empty"::: ) ($#v5_closure1 :::"strict"::: ) ($#v6_closure1 :::"additive"::: ) ($#v7_closure1 :::"absolutely-additive"::: ) ($#v8_closure1 :::"multiplicative"::: ) ($#v9_closure1 :::"absolutely-multiplicative"::: ) ($#v10_closure1 :::"properly-upper-bound"::: ) ($#v11_closure1 :::"properly-lower-bound"::: ) for ($#l1_closure1 :::"MSClosureStr"::: ) "over" "S"; end; registrationlet "S" be ($#l1_struct_0 :::"1-sorted"::: ) ; let "CS" be ($#v6_closure1 :::"additive"::: ) ($#l1_closure1 :::"MSClosureStr"::: ) "over" (Set (Const "S")); cluster (Set "the" ($#u1_closure1 :::"Family"::: ) "of" "CS") -> ($#v1_mssubfam :::"additive"::: ) ; end; registrationlet "S" be ($#l1_struct_0 :::"1-sorted"::: ) ; let "CS" be ($#v7_closure1 :::"absolutely-additive"::: ) ($#l1_closure1 :::"MSClosureStr"::: ) "over" (Set (Const "S")); cluster (Set "the" ($#u1_closure1 :::"Family"::: ) "of" "CS") -> ($#v2_mssubfam :::"absolutely-additive"::: ) ; end; registrationlet "S" be ($#l1_struct_0 :::"1-sorted"::: ) ; let "CS" be ($#v8_closure1 :::"multiplicative"::: ) ($#l1_closure1 :::"MSClosureStr"::: ) "over" (Set (Const "S")); cluster (Set "the" ($#u1_closure1 :::"Family"::: ) "of" "CS") -> ($#v3_mssubfam :::"multiplicative"::: ) ; end; registrationlet "S" be ($#l1_struct_0 :::"1-sorted"::: ) ; let "CS" be ($#v9_closure1 :::"absolutely-multiplicative"::: ) ($#l1_closure1 :::"MSClosureStr"::: ) "over" (Set (Const "S")); cluster (Set "the" ($#u1_closure1 :::"Family"::: ) "of" "CS") -> ($#v4_mssubfam :::"absolutely-multiplicative"::: ) ; end; registrationlet "S" be ($#l1_struct_0 :::"1-sorted"::: ) ; let "CS" be ($#v10_closure1 :::"properly-upper-bound"::: ) ($#l1_closure1 :::"MSClosureStr"::: ) "over" (Set (Const "S")); cluster (Set "the" ($#u1_closure1 :::"Family"::: ) "of" "CS") -> ($#v5_mssubfam :::"properly-upper-bound"::: ) ; end; registrationlet "S" be ($#l1_struct_0 :::"1-sorted"::: ) ; let "CS" be ($#v11_closure1 :::"properly-lower-bound"::: ) ($#l1_closure1 :::"MSClosureStr"::: ) "over" (Set (Const "S")); cluster (Set "the" ($#u1_closure1 :::"Family"::: ) "of" "CS") -> ($#v6_mssubfam :::"properly-lower-bound"::: ) ; end; registrationlet "S" be ($#l1_struct_0 :::"1-sorted"::: ) ; let "M" be bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "S"))); let "F" be ($#m3_pboole :::"MSSubsetFamily":::) "of" (Set (Const "M")); cluster (Set ($#g1_closure1 :::"MSClosureStr"::: ) "(#" "M" "," "F" "#)" ) -> ($#v4_msualg_1 :::"non-empty"::: ) ; end; registrationlet "S" be ($#l1_struct_0 :::"1-sorted"::: ) ; let "MS" be ($#l2_msualg_1 :::"many-sorted"::: ) "over" (Set (Const "S")); let "F" be ($#v1_mssubfam :::"additive"::: ) ($#m3_pboole :::"MSSubsetFamily":::) "of" (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Const "MS"))); cluster (Set ($#g1_closure1 :::"MSClosureStr"::: ) "(#" (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" "MS") "," "F" "#)" ) -> ($#v6_closure1 :::"additive"::: ) ; end; registrationlet "S" be ($#l1_struct_0 :::"1-sorted"::: ) ; let "MS" be ($#l2_msualg_1 :::"many-sorted"::: ) "over" (Set (Const "S")); let "F" be ($#v2_mssubfam :::"absolutely-additive"::: ) ($#m3_pboole :::"MSSubsetFamily":::) "of" (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Const "MS"))); cluster (Set ($#g1_closure1 :::"MSClosureStr"::: ) "(#" (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" "MS") "," "F" "#)" ) -> ($#v7_closure1 :::"absolutely-additive"::: ) ; end; registrationlet "S" be ($#l1_struct_0 :::"1-sorted"::: ) ; let "MS" be ($#l2_msualg_1 :::"many-sorted"::: ) "over" (Set (Const "S")); let "F" be ($#v3_mssubfam :::"multiplicative"::: ) ($#m3_pboole :::"MSSubsetFamily":::) "of" (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Const "MS"))); cluster (Set ($#g1_closure1 :::"MSClosureStr"::: ) "(#" (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" "MS") "," "F" "#)" ) -> ($#v8_closure1 :::"multiplicative"::: ) ; end; registrationlet "S" be ($#l1_struct_0 :::"1-sorted"::: ) ; let "MS" be ($#l2_msualg_1 :::"many-sorted"::: ) "over" (Set (Const "S")); let "F" be ($#v4_mssubfam :::"absolutely-multiplicative"::: ) ($#m3_pboole :::"MSSubsetFamily":::) "of" (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Const "MS"))); cluster (Set ($#g1_closure1 :::"MSClosureStr"::: ) "(#" (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" "MS") "," "F" "#)" ) -> ($#v9_closure1 :::"absolutely-multiplicative"::: ) ; end; registrationlet "S" be ($#l1_struct_0 :::"1-sorted"::: ) ; let "MS" be ($#l2_msualg_1 :::"many-sorted"::: ) "over" (Set (Const "S")); let "F" be ($#v5_mssubfam :::"properly-upper-bound"::: ) ($#m3_pboole :::"MSSubsetFamily":::) "of" (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Const "MS"))); cluster (Set ($#g1_closure1 :::"MSClosureStr"::: ) "(#" (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" "MS") "," "F" "#)" ) -> ($#v10_closure1 :::"properly-upper-bound"::: ) ; end; registrationlet "S" be ($#l1_struct_0 :::"1-sorted"::: ) ; let "MS" be ($#l2_msualg_1 :::"many-sorted"::: ) "over" (Set (Const "S")); let "F" be ($#v6_mssubfam :::"properly-lower-bound"::: ) ($#m3_pboole :::"MSSubsetFamily":::) "of" (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Const "MS"))); cluster (Set ($#g1_closure1 :::"MSClosureStr"::: ) "(#" (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" "MS") "," "F" "#)" ) -> ($#v11_closure1 :::"properly-lower-bound"::: ) ; end; registrationlet "S" be ($#l1_struct_0 :::"1-sorted"::: ) ; cluster ($#v7_closure1 :::"absolutely-additive"::: ) -> ($#v6_closure1 :::"additive"::: ) for ($#l1_closure1 :::"MSClosureStr"::: ) "over" "S"; end; registrationlet "S" be ($#l1_struct_0 :::"1-sorted"::: ) ; cluster ($#v9_closure1 :::"absolutely-multiplicative"::: ) -> ($#v8_closure1 :::"multiplicative"::: ) for ($#l1_closure1 :::"MSClosureStr"::: ) "over" "S"; end; registrationlet "S" be ($#l1_struct_0 :::"1-sorted"::: ) ; cluster ($#v9_closure1 :::"absolutely-multiplicative"::: ) -> ($#v10_closure1 :::"properly-upper-bound"::: ) for ($#l1_closure1 :::"MSClosureStr"::: ) "over" "S"; end; registrationlet "S" be ($#l1_struct_0 :::"1-sorted"::: ) ; cluster ($#v7_closure1 :::"absolutely-additive"::: ) -> ($#v11_closure1 :::"properly-lower-bound"::: ) for ($#l1_closure1 :::"MSClosureStr"::: ) "over" "S"; end; definitionlet "S" be ($#l1_struct_0 :::"1-sorted"::: ) ; mode MSClosureSystem of "S" is ($#v9_closure1 :::"absolutely-multiplicative"::: ) ($#l1_closure1 :::"MSClosureStr"::: ) "over" "S"; end; definitionlet "I" be ($#m1_hidden :::"set"::: ) ; let "M" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); mode MSClosureOperator of "M" is ($#v1_closure1 :::"reflexive"::: ) ($#v2_closure1 :::"monotonic"::: ) ($#v3_closure1 :::"idempotent"::: ) ($#m2_pboole :::"MSSetOp":::) "of" "M"; end; definitionlet "I" be ($#m1_hidden :::"set"::: ) ; let "M" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); let "F" be ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set (Const "M")) "," (Set (Const "M")); func :::"MSFixPoints"::: "F" -> ($#m3_pboole :::"ManySortedSubset"::: ) "of" "M" means :: CLOSURE1:def 12 (Bool "for" (Set (Var "x")) "," (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) "I")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) "iff" (Bool "ex" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool "(" (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set "F" ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "x"))) ")" )) ")" )); end; :: deftheorem defines :::"MSFixPoints"::: CLOSURE1:def 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 "F")) "being" ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set (Var "M")) "," (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 ($#k5_closure1 :::"MSFixPoints"::: ) (Set (Var "F")))) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Var "I")))) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "b4")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) "iff" (Bool "ex" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool "(" (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "x"))) ")" )) ")" )) ")" ))))); registrationlet "I" be ($#m1_hidden :::"set"::: ) ; let "M" be bbbadV3_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); let "F" be ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set (Const "M")) "," (Set (Const "M")); cluster (Set ($#k5_closure1 :::"MSFixPoints"::: ) "F") -> bbbadV3_RELAT_1() ; end; theorem :: CLOSURE1:28 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "," (Set (Var "A")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "F")) "being" ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set (Var "M")) "," (Set (Var "M")) "holds" (Bool "(" (Bool "(" (Bool (Set (Var "A")) ($#r1_pboole :::"in"::: ) (Set (Var "M"))) & (Bool (Set (Set (Var "F")) ($#k16_pralg_1 :::".."::: ) (Set (Var "A"))) ($#r6_pboole :::"="::: ) (Set (Var "A"))) ")" ) "iff" (Bool (Set (Var "A")) ($#r1_pboole :::"in"::: ) (Set ($#k5_closure1 :::"MSFixPoints"::: ) (Set (Var "F")))) ")" )))) ; theorem :: CLOSURE1:29 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool (Set ($#k5_closure1 :::"MSFixPoints"::: ) (Set "(" ($#k2_msualg_3 :::"id"::: ) (Set (Var "A")) ")" )) ($#r6_pboole :::"="::: ) (Set (Var "A"))))) ; theorem :: CLOSURE1:30 (Bool "for" (Set (Var "S")) "being" ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) (Bool "for" (Set (Var "J")) "being" ($#v1_closure1 :::"reflexive"::: ) ($#v2_closure1 :::"monotonic"::: ) ($#m2_pboole :::"MSSetOp":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "D")) "being" ($#m3_pboole :::"MSSubsetFamily":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "D")) ($#r6_pboole :::"="::: ) (Set ($#k5_closure1 :::"MSFixPoints"::: ) (Set (Var "J"))))) "holds" (Bool (Set ($#g1_closure1 :::"MSClosureStr"::: ) "(#" (Set (Var "A")) "," (Set (Var "D")) "#)" ) "is" ($#l1_closure1 :::"MSClosureSystem":::) "of" (Set (Var "S"))))))) ; theorem :: CLOSURE1:31 (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 "D")) "being" ($#v5_mssubfam :::"properly-upper-bound"::: ) ($#m3_pboole :::"MSSubsetFamily":::) "of" (Set (Var "M")) (Bool "for" (Set (Var "X")) "being" ($#m1_pboole :::"Element"::: ) "of" (Set ($#k5_mssubfam :::"bool"::: ) (Set (Var "M"))) (Bool "ex" (Set (Var "SF")) "being" bbbadV2_RELAT_1() ($#m3_pboole :::"MSSubsetFamily":::) "of" (Set (Var "M")) "st" (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool "(" (Bool (Set (Var "Y")) ($#r1_pboole :::"in"::: ) (Set (Var "SF"))) "iff" (Bool "(" (Bool (Set (Var "Y")) ($#r1_pboole :::"in"::: ) (Set (Var "D"))) & (Bool (Set (Var "X")) ($#r2_pboole :::"c="::: ) (Set (Var "Y"))) ")" ) ")" ))))))) ; theorem :: CLOSURE1:32 (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 "D")) "being" ($#v5_mssubfam :::"properly-upper-bound"::: ) ($#m3_pboole :::"MSSubsetFamily":::) "of" (Set (Var "M")) (Bool "for" (Set (Var "X")) "being" ($#m1_pboole :::"Element"::: ) "of" (Set ($#k5_mssubfam :::"bool"::: ) (Set (Var "M"))) (Bool "for" (Set (Var "SF")) "being" bbbadV2_RELAT_1() ($#m3_pboole :::"MSSubsetFamily":::) "of" (Set (Var "M")) "st" (Bool (Bool "(" "for" (Set (Var "Y")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool "(" (Bool (Set (Var "Y")) ($#r1_pboole :::"in"::: ) (Set (Var "SF"))) "iff" (Bool "(" (Bool (Set (Var "Y")) ($#r1_pboole :::"in"::: ) (Set (Var "D"))) & (Bool (Set (Var "X")) ($#r2_pboole :::"c="::: ) (Set (Var "Y"))) ")" ) ")" ) ")" )) "holds" (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Di")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Var "I"))) & (Bool (Set (Var "Di")) ($#r1_hidden :::"="::: ) (Set (Set (Var "D")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))))) "holds" (Bool (Set (Set (Var "SF")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "z")) where z "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "Di")) : (Bool (Set (Set (Var "X")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_tarski :::"c="::: ) (Set (Var "z"))) "}" )))))))) ; theorem :: CLOSURE1:33 (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 "D")) "being" ($#v5_mssubfam :::"properly-upper-bound"::: ) ($#m3_pboole :::"MSSubsetFamily":::) "of" (Set (Var "M")) (Bool "ex" (Set (Var "J")) "being" ($#m2_pboole :::"MSSetOp":::) "of" (Set (Var "M")) "st" (Bool "for" (Set (Var "X")) "being" ($#m1_pboole :::"Element"::: ) "of" (Set ($#k5_mssubfam :::"bool"::: ) (Set (Var "M"))) (Bool "for" (Set (Var "SF")) "being" bbbadV2_RELAT_1() ($#m3_pboole :::"MSSubsetFamily":::) "of" (Set (Var "M")) "st" (Bool (Bool "(" "for" (Set (Var "Y")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool "(" (Bool (Set (Var "Y")) ($#r1_pboole :::"in"::: ) (Set (Var "SF"))) "iff" (Bool "(" (Bool (Set (Var "Y")) ($#r1_pboole :::"in"::: ) (Set (Var "D"))) & (Bool (Set (Var "X")) ($#r2_pboole :::"c="::: ) (Set (Var "Y"))) ")" ) ")" ) ")" )) "holds" (Bool (Set (Set (Var "J")) ($#k2_closure1 :::".."::: ) (Set (Var "X"))) ($#r6_pboole :::"="::: ) (Set ($#k4_mssubfam :::"meet"::: ) (Set (Var "SF")))))))))) ; theorem :: CLOSURE1:34 (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 "D")) "being" ($#v5_mssubfam :::"properly-upper-bound"::: ) ($#m3_pboole :::"MSSubsetFamily":::) "of" (Set (Var "M")) (Bool "for" (Set (Var "A")) "being" ($#m1_pboole :::"Element"::: ) "of" (Set ($#k5_mssubfam :::"bool"::: ) (Set (Var "M"))) (Bool "for" (Set (Var "J")) "being" ($#m2_pboole :::"MSSetOp":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "A")) ($#r1_pboole :::"in"::: ) (Set (Var "D"))) & (Bool "(" "for" (Set (Var "X")) "being" ($#m1_pboole :::"Element"::: ) "of" (Set ($#k5_mssubfam :::"bool"::: ) (Set (Var "M"))) (Bool "for" (Set (Var "SF")) "being" bbbadV2_RELAT_1() ($#m3_pboole :::"MSSubsetFamily":::) "of" (Set (Var "M")) "st" (Bool (Bool "(" "for" (Set (Var "Y")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool "(" (Bool (Set (Var "Y")) ($#r1_pboole :::"in"::: ) (Set (Var "SF"))) "iff" (Bool "(" (Bool (Set (Var "Y")) ($#r1_pboole :::"in"::: ) (Set (Var "D"))) & (Bool (Set (Var "X")) ($#r2_pboole :::"c="::: ) (Set (Var "Y"))) ")" ) ")" ) ")" )) "holds" (Bool (Set (Set (Var "J")) ($#k2_closure1 :::".."::: ) (Set (Var "X"))) ($#r6_pboole :::"="::: ) (Set ($#k4_mssubfam :::"meet"::: ) (Set (Var "SF"))))) ")" )) "holds" (Bool (Set (Set (Var "J")) ($#k2_closure1 :::".."::: ) (Set (Var "A"))) ($#r6_pboole :::"="::: ) (Set (Var "A")))))))) ; theorem :: CLOSURE1:35 (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 "D")) "being" ($#v4_mssubfam :::"absolutely-multiplicative"::: ) ($#m3_pboole :::"MSSubsetFamily":::) "of" (Set (Var "M")) (Bool "for" (Set (Var "A")) "being" ($#m1_pboole :::"Element"::: ) "of" (Set ($#k5_mssubfam :::"bool"::: ) (Set (Var "M"))) (Bool "for" (Set (Var "J")) "being" ($#m2_pboole :::"MSSetOp":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Set (Var "J")) ($#k2_closure1 :::".."::: ) (Set (Var "A"))) ($#r6_pboole :::"="::: ) (Set (Var "A"))) & (Bool "(" "for" (Set (Var "X")) "being" ($#m1_pboole :::"Element"::: ) "of" (Set ($#k5_mssubfam :::"bool"::: ) (Set (Var "M"))) (Bool "for" (Set (Var "SF")) "being" bbbadV2_RELAT_1() ($#m3_pboole :::"MSSubsetFamily":::) "of" (Set (Var "M")) "st" (Bool (Bool "(" "for" (Set (Var "Y")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool "(" (Bool (Set (Var "Y")) ($#r1_pboole :::"in"::: ) (Set (Var "SF"))) "iff" (Bool "(" (Bool (Set (Var "Y")) ($#r1_pboole :::"in"::: ) (Set (Var "D"))) & (Bool (Set (Var "X")) ($#r2_pboole :::"c="::: ) (Set (Var "Y"))) ")" ) ")" ) ")" )) "holds" (Bool (Set (Set (Var "J")) ($#k2_closure1 :::".."::: ) (Set (Var "X"))) ($#r6_pboole :::"="::: ) (Set ($#k4_mssubfam :::"meet"::: ) (Set (Var "SF"))))) ")" )) "holds" (Bool (Set (Var "A")) ($#r1_pboole :::"in"::: ) (Set (Var "D")))))))) ; theorem :: CLOSURE1:36 (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 "D")) "being" ($#v5_mssubfam :::"properly-upper-bound"::: ) ($#m3_pboole :::"MSSubsetFamily":::) "of" (Set (Var "M")) (Bool "for" (Set (Var "J")) "being" ($#m2_pboole :::"MSSetOp":::) "of" (Set (Var "M")) "st" (Bool (Bool "(" "for" (Set (Var "X")) "being" ($#m1_pboole :::"Element"::: ) "of" (Set ($#k5_mssubfam :::"bool"::: ) (Set (Var "M"))) (Bool "for" (Set (Var "SF")) "being" bbbadV2_RELAT_1() ($#m3_pboole :::"MSSubsetFamily":::) "of" (Set (Var "M")) "st" (Bool (Bool "(" "for" (Set (Var "Y")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool "(" (Bool (Set (Var "Y")) ($#r1_pboole :::"in"::: ) (Set (Var "SF"))) "iff" (Bool "(" (Bool (Set (Var "Y")) ($#r1_pboole :::"in"::: ) (Set (Var "D"))) & (Bool (Set (Var "X")) ($#r2_pboole :::"c="::: ) (Set (Var "Y"))) ")" ) ")" ) ")" )) "holds" (Bool (Set (Set (Var "J")) ($#k2_closure1 :::".."::: ) (Set (Var "X"))) ($#r6_pboole :::"="::: ) (Set ($#k4_mssubfam :::"meet"::: ) (Set (Var "SF"))))) ")" )) "holds" (Bool "(" (Bool (Set (Var "J")) "is" ($#v1_closure1 :::"reflexive"::: ) ) & (Bool (Set (Var "J")) "is" ($#v2_closure1 :::"monotonic"::: ) ) ")" ))))) ; theorem :: CLOSURE1:37 (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 "D")) "being" ($#v4_mssubfam :::"absolutely-multiplicative"::: ) ($#m3_pboole :::"MSSubsetFamily":::) "of" (Set (Var "M")) (Bool "for" (Set (Var "J")) "being" ($#m2_pboole :::"MSSetOp":::) "of" (Set (Var "M")) "st" (Bool (Bool "(" "for" (Set (Var "X")) "being" ($#m1_pboole :::"Element"::: ) "of" (Set ($#k5_mssubfam :::"bool"::: ) (Set (Var "M"))) (Bool "for" (Set (Var "SF")) "being" bbbadV2_RELAT_1() ($#m3_pboole :::"MSSubsetFamily":::) "of" (Set (Var "M")) "st" (Bool (Bool "(" "for" (Set (Var "Y")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool "(" (Bool (Set (Var "Y")) ($#r1_pboole :::"in"::: ) (Set (Var "SF"))) "iff" (Bool "(" (Bool (Set (Var "Y")) ($#r1_pboole :::"in"::: ) (Set (Var "D"))) & (Bool (Set (Var "X")) ($#r2_pboole :::"c="::: ) (Set (Var "Y"))) ")" ) ")" ) ")" )) "holds" (Bool (Set (Set (Var "J")) ($#k2_closure1 :::".."::: ) (Set (Var "X"))) ($#r6_pboole :::"="::: ) (Set ($#k4_mssubfam :::"meet"::: ) (Set (Var "SF"))))) ")" )) "holds" (Bool (Set (Var "J")) "is" ($#v3_closure1 :::"idempotent"::: ) ))))) ; theorem :: CLOSURE1:38 (Bool "for" (Set (Var "S")) "being" ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "D")) "being" ($#l1_closure1 :::"MSClosureSystem":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "J")) "being" ($#m2_pboole :::"MSSetOp":::) "of" (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "D"))) "st" (Bool (Bool "(" "for" (Set (Var "X")) "being" ($#m1_pboole :::"Element"::: ) "of" (Set ($#k5_mssubfam :::"bool"::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "D")))) (Bool "for" (Set (Var "SF")) "being" bbbadV2_RELAT_1() ($#m3_pboole :::"MSSubsetFamily":::) "of" (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "D"))) "st" (Bool (Bool "(" "for" (Set (Var "Y")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) "holds" (Bool "(" (Bool (Set (Var "Y")) ($#r1_pboole :::"in"::: ) (Set (Var "SF"))) "iff" (Bool "(" (Bool (Set (Var "Y")) ($#r1_pboole :::"in"::: ) (Set "the" ($#u1_closure1 :::"Family"::: ) "of" (Set (Var "D")))) & (Bool (Set (Var "X")) ($#r2_pboole :::"c="::: ) (Set (Var "Y"))) ")" ) ")" ) ")" )) "holds" (Bool (Set (Set (Var "J")) ($#k2_closure1 :::".."::: ) (Set (Var "X"))) ($#r6_pboole :::"="::: ) (Set ($#k4_mssubfam :::"meet"::: ) (Set (Var "SF"))))) ")" )) "holds" (Bool (Set (Var "J")) "is" ($#m2_pboole :::"MSClosureOperator":::) "of" (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "D"))))))) ; definitionlet "S" be ($#l1_struct_0 :::"1-sorted"::: ) ; let "A" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "S"))); let "C" be ($#m2_pboole :::"MSClosureOperator":::) "of" (Set (Const "A")); func :::"ClOp->ClSys"::: "C" -> ($#l1_closure1 :::"MSClosureSystem":::) "of" "S" means :: CLOSURE1:def 13 (Bool "ex" (Set (Var "D")) "being" ($#m3_pboole :::"MSSubsetFamily":::) "of" "A" "st" (Bool "(" (Bool (Set (Var "D")) ($#r6_pboole :::"="::: ) (Set ($#k5_closure1 :::"MSFixPoints"::: ) "C")) & (Bool it ($#r1_hidden :::"="::: ) (Set ($#g1_closure1 :::"MSClosureStr"::: ) "(#" "A" "," (Set (Var "D")) "#)" )) ")" )); end; :: deftheorem defines :::"ClOp->ClSys"::: CLOSURE1:def 13 : (Bool "for" (Set (Var "S")) "being" ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) (Bool "for" (Set (Var "C")) "being" ($#m2_pboole :::"MSClosureOperator":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "b4")) "being" ($#l1_closure1 :::"MSClosureSystem":::) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k6_closure1 :::"ClOp->ClSys"::: ) (Set (Var "C")))) "iff" (Bool "ex" (Set (Var "D")) "being" ($#m3_pboole :::"MSSubsetFamily":::) "of" (Set (Var "A")) "st" (Bool "(" (Bool (Set (Var "D")) ($#r6_pboole :::"="::: ) (Set ($#k5_closure1 :::"MSFixPoints"::: ) (Set (Var "C")))) & (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#g1_closure1 :::"MSClosureStr"::: ) "(#" (Set (Var "A")) "," (Set (Var "D")) "#)" )) ")" )) ")" ))))); registrationlet "S" be ($#l1_struct_0 :::"1-sorted"::: ) ; let "A" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "S"))); let "C" be ($#m2_pboole :::"MSClosureOperator":::) "of" (Set (Const "A")); cluster (Set ($#k6_closure1 :::"ClOp->ClSys"::: ) "C") -> ($#v5_closure1 :::"strict"::: ) ; end; registrationlet "S" be ($#l1_struct_0 :::"1-sorted"::: ) ; let "A" be bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "S"))); let "C" be ($#m2_pboole :::"MSClosureOperator":::) "of" (Set (Const "A")); cluster (Set ($#k6_closure1 :::"ClOp->ClSys"::: ) "C") -> ($#v4_msualg_1 :::"non-empty"::: ) ; end; definitionlet "S" be ($#l1_struct_0 :::"1-sorted"::: ) ; let "D" be ($#l1_closure1 :::"MSClosureSystem":::) "of" (Set (Const "S")); func :::"ClSys->ClOp"::: "D" -> ($#m2_pboole :::"MSClosureOperator":::) "of" (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" "D") means :: CLOSURE1:def 14 (Bool "for" (Set (Var "X")) "being" ($#m1_pboole :::"Element"::: ) "of" (Set ($#k5_mssubfam :::"bool"::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" "D")) (Bool "for" (Set (Var "SF")) "being" bbbadV2_RELAT_1() ($#m3_pboole :::"MSSubsetFamily":::) "of" (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" "D") "st" (Bool (Bool "(" "for" (Set (Var "Y")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S") "holds" (Bool "(" (Bool (Set (Var "Y")) ($#r1_pboole :::"in"::: ) (Set (Var "SF"))) "iff" (Bool "(" (Bool (Set (Var "Y")) ($#r1_pboole :::"in"::: ) (Set "the" ($#u1_closure1 :::"Family"::: ) "of" "D")) & (Bool (Set (Var "X")) ($#r2_pboole :::"c="::: ) (Set (Var "Y"))) ")" ) ")" ) ")" )) "holds" (Bool (Set it ($#k2_closure1 :::".."::: ) (Set (Var "X"))) ($#r6_pboole :::"="::: ) (Set ($#k4_mssubfam :::"meet"::: ) (Set (Var "SF")))))); end; :: deftheorem defines :::"ClSys->ClOp"::: CLOSURE1:def 14 : (Bool "for" (Set (Var "S")) "being" ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "D")) "being" ($#l1_closure1 :::"MSClosureSystem":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "b3")) "being" ($#m2_pboole :::"MSClosureOperator":::) "of" (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "D"))) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k7_closure1 :::"ClSys->ClOp"::: ) (Set (Var "D")))) "iff" (Bool "for" (Set (Var "X")) "being" ($#m1_pboole :::"Element"::: ) "of" (Set ($#k5_mssubfam :::"bool"::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "D")))) (Bool "for" (Set (Var "SF")) "being" bbbadV2_RELAT_1() ($#m3_pboole :::"MSSubsetFamily":::) "of" (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "D"))) "st" (Bool (Bool "(" "for" (Set (Var "Y")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) "holds" (Bool "(" (Bool (Set (Var "Y")) ($#r1_pboole :::"in"::: ) (Set (Var "SF"))) "iff" (Bool "(" (Bool (Set (Var "Y")) ($#r1_pboole :::"in"::: ) (Set "the" ($#u1_closure1 :::"Family"::: ) "of" (Set (Var "D")))) & (Bool (Set (Var "X")) ($#r2_pboole :::"c="::: ) (Set (Var "Y"))) ")" ) ")" ) ")" )) "holds" (Bool (Set (Set (Var "b3")) ($#k2_closure1 :::".."::: ) (Set (Var "X"))) ($#r6_pboole :::"="::: ) (Set ($#k4_mssubfam :::"meet"::: ) (Set (Var "SF")))))) ")" )))); theorem :: CLOSURE1:39 (Bool "for" (Set (Var "S")) "being" ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) (Bool "for" (Set (Var "J")) "being" ($#m2_pboole :::"MSClosureOperator":::) "of" (Set (Var "A")) "holds" (Bool (Set ($#k7_closure1 :::"ClSys->ClOp"::: ) (Set "(" ($#k6_closure1 :::"ClOp->ClSys"::: ) (Set (Var "J")) ")" )) ($#r6_pboole :::"="::: ) (Set (Var "J")))))) ; theorem :: CLOSURE1:40 (Bool "for" (Set (Var "S")) "being" ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "D")) "being" ($#l1_closure1 :::"MSClosureSystem":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k6_closure1 :::"ClOp->ClSys"::: ) (Set "(" ($#k7_closure1 :::"ClSys->ClOp"::: ) (Set (Var "D")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#g1_closure1 :::"MSClosureStr"::: ) "(#" (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "D"))) "," (Set "the" ($#u1_closure1 :::"Family"::: ) "of" (Set (Var "D"))) "#)" )))) ;