:: PBOOLE semantic presentation begin theorem :: PBOOLE:1 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "f")) "is" ($#v2_relat_1 :::"non-empty"::: ) )) "holds" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f"))) "is" ($#v1_setfam_1 :::"with_non-empty_elements"::: ) )) ; theorem :: PBOOLE:2 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v3_relat_1 :::"empty-yielding"::: ) ) "iff" (Bool "(" (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) "or" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) )) ")" ) ")" )) ; registrationlet "I" be ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) "I" ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_partfun1 :::"total"::: ) for ($#m1_hidden :::"set"::: ) ; end; definitionlet "I" be ($#m1_hidden :::"set"::: ) ; mode ManySortedSet of "I" is "I" ($#v4_relat_1 :::"-defined"::: ) ($#v1_partfun1 :::"total"::: ) ($#m1_hidden :::"Function":::); end; scheme :: PBOOLE:sch 1 KuratowskiFunction{ F1() -> ($#m1_hidden :::"set"::: ) , F2( ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) } : (Bool "ex" (Set (Var "f")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set F1 "(" ")" ) "st" (Bool "for" (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" ))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "e"))) ($#r2_hidden :::"in"::: ) (Set F2 "(" (Set (Var "e")) ")" )))) provided (Bool "for" (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" ))) "holds" (Bool (Set F2 "(" (Set (Var "e")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) proof end; definitionlet "I" be ($#m1_hidden :::"set"::: ) ; let "X", "Y" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); pred "X" :::"in"::: "Y" means :: PBOOLE:def 1 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) "I")) "holds" (Bool (Set "X" ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r2_hidden :::"in"::: ) (Set "Y" ($#k1_funct_1 :::"."::: ) (Set (Var "i"))))); pred "X" :::"c="::: "Y" means :: PBOOLE:def 2 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) "I")) "holds" (Bool (Set "X" ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_tarski :::"c="::: ) (Set "Y" ($#k1_funct_1 :::"."::: ) (Set (Var "i"))))); reflexivity (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Const "I")))) "holds" (Bool (Set (Set (Var "X")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "X")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))))) ; end; :: deftheorem defines :::"in"::: PBOOLE:def 1 : (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool "(" (Bool (Set (Var "X")) ($#r1_pboole :::"in"::: ) (Set (Var "Y"))) "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 "X")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r2_hidden :::"in"::: ) (Set (Set (Var "Y")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))))) ")" ))); :: deftheorem defines :::"c="::: PBOOLE:def 2 : (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool "(" (Bool (Set (Var "X")) ($#r2_pboole :::"c="::: ) (Set (Var "Y"))) "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 "X")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "Y")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))))) ")" ))); definitionlet "I" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "X", "Y" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); :: original: :::"in"::: redefine pred "X" :::"in"::: "Y"; asymmetry (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")) "st" (Bool (Bool ((Set (Const "I")) "," (Set (Var "b1")) "," (Set (Var "b2"))))) "holds" (Bool "not" (Bool ((Set (Const "I")) "," (Set (Var "b2")) "," (Set (Var "b1")))))) ; end; scheme :: PBOOLE:sch 2 PSeparation{ F1() -> ($#m1_hidden :::"set"::: ) , F2() -> ($#m1_hidden :::"ManySortedSet":::) "of" (Set F1 "(" ")" ), P1[ ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ] } : (Bool "ex" (Set (Var "X")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set F1 "(" ")" ) "st" (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" ))) "holds" (Bool "for" (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "X")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) "iff" (Bool "(" (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set (Set F2 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) & (Bool P1[(Set (Var "i")) "," (Set (Var "e"))]) ")" ) ")" )))) proof end; theorem :: PBOOLE:3 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (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 "X")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "Y")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) ")" )) "holds" (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set (Var "Y"))))) ; definitionlet "I" be ($#m1_hidden :::"set"::: ) ; func :::"[[0]]"::: "I" -> ($#m1_hidden :::"ManySortedSet":::) "of" "I" equals :: PBOOLE:def 3 (Set "I" ($#k7_funcop_1 :::"-->"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )); let "X", "Y" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); func "X" :::"\/"::: "Y" -> ($#m1_hidden :::"ManySortedSet":::) "of" "I" means :: PBOOLE:def 4 (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 (Set "(" "X" ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" "Y" ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" )))); commutativity (Bool "for" (Set (Var "b1")) "," (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")) "st" (Bool (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Const "I")))) "holds" (Bool (Set (Set (Var "b1")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "X")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" (Set (Var "Y")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ))) ")" )) "holds" (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Const "I")))) "holds" (Bool (Set (Set (Var "b1")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "Y")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" (Set (Var "X")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ))))) ; idempotence (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Const "I")))) "holds" (Bool (Set (Set (Var "X")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "X")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" (Set (Var "X")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ))))) ; func "X" :::"/\"::: "Y" -> ($#m1_hidden :::"ManySortedSet":::) "of" "I" means :: PBOOLE:def 5 (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 (Set "(" "X" ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" "Y" ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" )))); commutativity (Bool "for" (Set (Var "b1")) "," (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")) "st" (Bool (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Const "I")))) "holds" (Bool (Set (Set (Var "b1")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "X")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" (Set (Var "Y")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ))) ")" )) "holds" (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Const "I")))) "holds" (Bool (Set (Set (Var "b1")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "Y")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" (Set (Var "X")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ))))) ; idempotence (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Const "I")))) "holds" (Bool (Set (Set (Var "X")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "X")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" (Set (Var "X")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ))))) ; func "X" :::"\"::: "Y" -> ($#m1_hidden :::"ManySortedSet":::) "of" "I" means :: PBOOLE:def 6 (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 (Set "(" "X" ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k6_subset_1 :::"\"::: ) (Set "(" "Y" ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" )))); pred "X" :::"overlaps"::: "Y" means :: PBOOLE:def 7 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) "I")) "holds" (Bool (Set "X" ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_xboole_0 :::"meets"::: ) (Set "Y" ($#k1_funct_1 :::"."::: ) (Set (Var "i"))))); symmetry (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")) "st" (Bool (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Const "I")))) "holds" (Bool (Set (Set (Var "X")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_xboole_0 :::"meets"::: ) (Set (Set (Var "Y")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) ")" )) "holds" (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Const "I")))) "holds" (Bool (Set (Set (Var "Y")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_xboole_0 :::"meets"::: ) (Set (Set (Var "X")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))))) ; pred "X" :::"misses"::: "Y" means :: PBOOLE:def 8 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) "I")) "holds" (Bool (Set "X" ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_xboole_0 :::"misses"::: ) (Set "Y" ($#k1_funct_1 :::"."::: ) (Set (Var "i"))))); symmetry (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")) "st" (Bool (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Const "I")))) "holds" (Bool (Set (Set (Var "X")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_xboole_0 :::"misses"::: ) (Set (Set (Var "Y")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) ")" )) "holds" (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Const "I")))) "holds" (Bool (Set (Set (Var "Y")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_xboole_0 :::"misses"::: ) (Set (Set (Var "X")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))))) ; end; :: deftheorem defines :::"[[0]]"::: PBOOLE:def 3 : (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k1_pboole :::"[[0]]"::: ) (Set (Var "I"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "I")) ($#k7_funcop_1 :::"-->"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))); :: deftheorem defines :::"\/"::: PBOOLE:def 4 : (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "b4")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "X")) ($#k2_pboole :::"\/"::: ) (Set (Var "Y")))) "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 (Set "(" (Set (Var "X")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" (Set (Var "Y")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" )))) ")" ))); :: deftheorem defines :::"/\"::: PBOOLE:def 5 : (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "b4")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "X")) ($#k3_pboole :::"/\"::: ) (Set (Var "Y")))) "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 (Set "(" (Set (Var "X")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" (Set (Var "Y")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" )))) ")" ))); :: deftheorem defines :::"\"::: PBOOLE:def 6 : (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "b4")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "X")) ($#k4_pboole :::"\"::: ) (Set (Var "Y")))) "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 (Set "(" (Set (Var "X")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k6_subset_1 :::"\"::: ) (Set "(" (Set (Var "Y")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" )))) ")" ))); :: deftheorem defines :::"overlaps"::: PBOOLE:def 7 : (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool "(" (Bool (Set (Var "X")) ($#r4_pboole :::"overlaps"::: ) (Set (Var "Y"))) "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 "X")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_xboole_0 :::"meets"::: ) (Set (Set (Var "Y")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))))) ")" ))); :: deftheorem defines :::"misses"::: PBOOLE:def 8 : (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool "(" (Bool (Set (Var "X")) ($#r5_pboole :::"misses"::: ) (Set (Var "Y"))) "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 "X")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_xboole_0 :::"misses"::: ) (Set (Set (Var "Y")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))))) ")" ))); notationlet "I" be ($#m1_hidden :::"set"::: ) ; let "X", "Y" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); antonym "X" :::"meets"::: "Y" for "X" :::"misses"::: "Y"; end; definitionlet "I" be ($#m1_hidden :::"set"::: ) ; let "X", "Y" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); func "X" :::"\+\"::: "Y" -> ($#m1_hidden :::"ManySortedSet":::) "of" "I" equals :: PBOOLE:def 9 (Set (Set "(" "X" ($#k4_pboole :::"\"::: ) "Y" ")" ) ($#k2_pboole :::"\/"::: ) (Set "(" "Y" ($#k4_pboole :::"\"::: ) "X" ")" )); commutativity (Bool "for" (Set (Var "b1")) "," (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")) "st" (Bool (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "X")) ($#k4_pboole :::"\"::: ) (Set (Var "Y")) ")" ) ($#k2_pboole :::"\/"::: ) (Set "(" (Set (Var "Y")) ($#k4_pboole :::"\"::: ) (Set (Var "X")) ")" )))) "holds" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "Y")) ($#k4_pboole :::"\"::: ) (Set (Var "X")) ")" ) ($#k2_pboole :::"\/"::: ) (Set "(" (Set (Var "X")) ($#k4_pboole :::"\"::: ) (Set (Var "Y")) ")" )))) ; end; :: deftheorem defines :::"\+\"::: PBOOLE:def 9 : (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool (Set (Set (Var "X")) ($#k5_pboole :::"\+\"::: ) (Set (Var "Y"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "X")) ($#k4_pboole :::"\"::: ) (Set (Var "Y")) ")" ) ($#k2_pboole :::"\/"::: ) (Set "(" (Set (Var "Y")) ($#k4_pboole :::"\"::: ) (Set (Var "X")) ")" ))))); theorem :: PBOOLE:4 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (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 "(" (Set (Var "X")) ($#k5_pboole :::"\+\"::: ) (Set (Var "Y")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "X")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k5_xboole_0 :::"\+\"::: ) (Set "(" (Set (Var "Y")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" )))))) ; theorem :: PBOOLE:5 (Bool "for" (Set (Var "i")) "," (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set "(" ($#k1_pboole :::"[[0]]"::: ) (Set (Var "I")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ; theorem :: PBOOLE:6 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (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 "X")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" )) "holds" (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set ($#k1_pboole :::"[[0]]"::: ) (Set (Var "I")))))) ; theorem :: PBOOLE:7 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool "(" (Bool (Set (Var "x")) ($#r1_pboole :::"in"::: ) (Set (Var "X"))) "or" (Bool (Set (Var "x")) ($#r1_pboole :::"in"::: ) (Set (Var "Y"))) ")" )) "holds" (Bool (Set (Var "x")) ($#r1_pboole :::"in"::: ) (Set (Set (Var "X")) ($#k2_pboole :::"\/"::: ) (Set (Var "Y")))))) ; theorem :: PBOOLE:8 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_pboole :::"in"::: ) (Set (Set (Var "X")) ($#k3_pboole :::"/\"::: ) (Set (Var "Y")))) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r1_pboole :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "x")) ($#r1_pboole :::"in"::: ) (Set (Var "Y"))) ")" ) ")" ))) ; theorem :: PBOOLE:9 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "x")) ($#r1_pboole :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "X")) ($#r2_pboole :::"c="::: ) (Set (Var "Y")))) "holds" (Bool (Set (Var "x")) ($#r1_pboole :::"in"::: ) (Set (Var "Y"))))) ; theorem :: PBOOLE:10 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "x")) ($#r1_pboole :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "x")) ($#r1_pboole :::"in"::: ) (Set (Var "Y")))) "holds" (Bool (Set (Var "X")) ($#r4_pboole :::"overlaps"::: ) (Set (Var "Y"))))) ; theorem :: PBOOLE:11 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "X")) ($#r4_pboole :::"overlaps"::: ) (Set (Var "Y")))) "holds" (Bool "ex" (Set (Var "x")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_pboole :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "x")) ($#r1_pboole :::"in"::: ) (Set (Var "Y"))) ")" )))) ; theorem :: PBOOLE:12 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "x")) ($#r1_pboole :::"in"::: ) (Set (Set (Var "X")) ($#k4_pboole :::"\"::: ) (Set (Var "Y"))))) "holds" (Bool (Set (Var "x")) ($#r1_pboole :::"in"::: ) (Set (Var "X"))))) ; begin definitionlet "I" be ($#m1_hidden :::"set"::: ) ; let "X", "Y" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); :: original: :::"="::: redefine pred "X" :::"="::: "Y" means :: PBOOLE:def 10 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) "I")) "holds" (Bool (Set "X" ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set "Y" ($#k1_funct_1 :::"."::: ) (Set (Var "i"))))); end; :: deftheorem defines :::"="::: PBOOLE:def 10 : (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool "(" (Bool (Set (Var "X")) ($#r6_pboole :::"="::: ) (Set (Var "Y"))) "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 "X")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "Y")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))))) ")" ))); theorem :: PBOOLE:13 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "X")) ($#r2_pboole :::"c="::: ) (Set (Var "Y"))) & (Bool (Set (Var "Y")) ($#r2_pboole :::"c="::: ) (Set (Var "Z")))) "holds" (Bool (Set (Var "X")) ($#r2_pboole :::"c="::: ) (Set (Var "Z"))))) ; theorem :: PBOOLE:14 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool (Set (Var "X")) ($#r2_pboole :::"c="::: ) (Set (Set (Var "X")) ($#k2_pboole :::"\/"::: ) (Set (Var "Y")))))) ; theorem :: PBOOLE:15 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool (Set (Set (Var "X")) ($#k3_pboole :::"/\"::: ) (Set (Var "Y"))) ($#r2_pboole :::"c="::: ) (Set (Var "X"))))) ; theorem :: PBOOLE:16 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Z")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "X")) ($#r2_pboole :::"c="::: ) (Set (Var "Z"))) & (Bool (Set (Var "Y")) ($#r2_pboole :::"c="::: ) (Set (Var "Z")))) "holds" (Bool (Set (Set (Var "X")) ($#k2_pboole :::"\/"::: ) (Set (Var "Y"))) ($#r2_pboole :::"c="::: ) (Set (Var "Z"))))) ; theorem :: PBOOLE:17 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Z")) "," (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "Z")) ($#r2_pboole :::"c="::: ) (Set (Var "X"))) & (Bool (Set (Var "Z")) ($#r2_pboole :::"c="::: ) (Set (Var "Y")))) "holds" (Bool (Set (Var "Z")) ($#r2_pboole :::"c="::: ) (Set (Set (Var "X")) ($#k3_pboole :::"/\"::: ) (Set (Var "Y")))))) ; theorem :: PBOOLE:18 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "X")) ($#r2_pboole :::"c="::: ) (Set (Var "Y")))) "holds" (Bool (Set (Set (Var "X")) ($#k2_pboole :::"\/"::: ) (Set (Var "Z"))) ($#r2_pboole :::"c="::: ) (Set (Set (Var "Y")) ($#k2_pboole :::"\/"::: ) (Set (Var "Z")))))) ; theorem :: PBOOLE:19 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "X")) ($#r2_pboole :::"c="::: ) (Set (Var "Y")))) "holds" (Bool (Set (Set (Var "X")) ($#k3_pboole :::"/\"::: ) (Set (Var "Z"))) ($#r2_pboole :::"c="::: ) (Set (Set (Var "Y")) ($#k3_pboole :::"/\"::: ) (Set (Var "Z")))))) ; theorem :: PBOOLE:20 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "," (Set (Var "V")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "X")) ($#r2_pboole :::"c="::: ) (Set (Var "Y"))) & (Bool (Set (Var "Z")) ($#r2_pboole :::"c="::: ) (Set (Var "V")))) "holds" (Bool (Set (Set (Var "X")) ($#k2_pboole :::"\/"::: ) (Set (Var "Z"))) ($#r2_pboole :::"c="::: ) (Set (Set (Var "Y")) ($#k2_pboole :::"\/"::: ) (Set (Var "V")))))) ; theorem :: PBOOLE:21 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "," (Set (Var "V")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "X")) ($#r2_pboole :::"c="::: ) (Set (Var "Y"))) & (Bool (Set (Var "Z")) ($#r2_pboole :::"c="::: ) (Set (Var "V")))) "holds" (Bool (Set (Set (Var "X")) ($#k3_pboole :::"/\"::: ) (Set (Var "Z"))) ($#r2_pboole :::"c="::: ) (Set (Set (Var "Y")) ($#k3_pboole :::"/\"::: ) (Set (Var "V")))))) ; theorem :: PBOOLE:22 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "X")) ($#r2_pboole :::"c="::: ) (Set (Var "Y")))) "holds" (Bool (Set (Set (Var "X")) ($#k2_pboole :::"\/"::: ) (Set (Var "Y"))) ($#r6_pboole :::"="::: ) (Set (Var "Y"))))) ; theorem :: PBOOLE:23 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "X")) ($#r2_pboole :::"c="::: ) (Set (Var "Y")))) "holds" (Bool (Set (Set (Var "X")) ($#k3_pboole :::"/\"::: ) (Set (Var "Y"))) ($#r6_pboole :::"="::: ) (Set (Var "X"))))) ; theorem :: PBOOLE:24 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool (Set (Set (Var "X")) ($#k3_pboole :::"/\"::: ) (Set (Var "Y"))) ($#r2_pboole :::"c="::: ) (Set (Set (Var "X")) ($#k2_pboole :::"\/"::: ) (Set (Var "Z")))))) ; theorem :: PBOOLE:25 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Z")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "X")) ($#r2_pboole :::"c="::: ) (Set (Var "Z")))) "holds" (Bool (Set (Set (Var "X")) ($#k2_pboole :::"\/"::: ) (Set "(" (Set (Var "Y")) ($#k3_pboole :::"/\"::: ) (Set (Var "Z")) ")" )) ($#r6_pboole :::"="::: ) (Set (Set "(" (Set (Var "X")) ($#k2_pboole :::"\/"::: ) (Set (Var "Y")) ")" ) ($#k3_pboole :::"/\"::: ) (Set (Var "Z")))))) ; theorem :: PBOOLE:26 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool "(" (Bool (Set (Var "X")) ($#r6_pboole :::"="::: ) (Set (Set (Var "Y")) ($#k2_pboole :::"\/"::: ) (Set (Var "Z")))) "iff" (Bool "(" (Bool (Set (Var "Y")) ($#r2_pboole :::"c="::: ) (Set (Var "X"))) & (Bool (Set (Var "Z")) ($#r2_pboole :::"c="::: ) (Set (Var "X"))) & (Bool "(" "for" (Set (Var "V")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "Y")) ($#r2_pboole :::"c="::: ) (Set (Var "V"))) & (Bool (Set (Var "Z")) ($#r2_pboole :::"c="::: ) (Set (Var "V")))) "holds" (Bool (Set (Var "X")) ($#r2_pboole :::"c="::: ) (Set (Var "V"))) ")" ) ")" ) ")" ))) ; theorem :: PBOOLE:27 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool "(" (Bool (Set (Var "X")) ($#r6_pboole :::"="::: ) (Set (Set (Var "Y")) ($#k3_pboole :::"/\"::: ) (Set (Var "Z")))) "iff" (Bool "(" (Bool (Set (Var "X")) ($#r2_pboole :::"c="::: ) (Set (Var "Y"))) & (Bool (Set (Var "X")) ($#r2_pboole :::"c="::: ) (Set (Var "Z"))) & (Bool "(" "for" (Set (Var "V")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "V")) ($#r2_pboole :::"c="::: ) (Set (Var "Y"))) & (Bool (Set (Var "V")) ($#r2_pboole :::"c="::: ) (Set (Var "Z")))) "holds" (Bool (Set (Var "V")) ($#r2_pboole :::"c="::: ) (Set (Var "X"))) ")" ) ")" ) ")" ))) ; theorem :: PBOOLE:28 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool (Set (Set "(" (Set (Var "X")) ($#k2_pboole :::"\/"::: ) (Set (Var "Y")) ")" ) ($#k2_pboole :::"\/"::: ) (Set (Var "Z"))) ($#r6_pboole :::"="::: ) (Set (Set (Var "X")) ($#k2_pboole :::"\/"::: ) (Set "(" (Set (Var "Y")) ($#k2_pboole :::"\/"::: ) (Set (Var "Z")) ")" ))))) ; theorem :: PBOOLE:29 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool (Set (Set "(" (Set (Var "X")) ($#k3_pboole :::"/\"::: ) (Set (Var "Y")) ")" ) ($#k3_pboole :::"/\"::: ) (Set (Var "Z"))) ($#r6_pboole :::"="::: ) (Set (Set (Var "X")) ($#k3_pboole :::"/\"::: ) (Set "(" (Set (Var "Y")) ($#k3_pboole :::"/\"::: ) (Set (Var "Z")) ")" ))))) ; theorem :: PBOOLE:30 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool (Set (Set (Var "X")) ($#k3_pboole :::"/\"::: ) (Set "(" (Set (Var "X")) ($#k2_pboole :::"\/"::: ) (Set (Var "Y")) ")" )) ($#r6_pboole :::"="::: ) (Set (Var "X"))))) ; theorem :: PBOOLE:31 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool (Set (Set (Var "X")) ($#k2_pboole :::"\/"::: ) (Set "(" (Set (Var "X")) ($#k3_pboole :::"/\"::: ) (Set (Var "Y")) ")" )) ($#r6_pboole :::"="::: ) (Set (Var "X"))))) ; theorem :: PBOOLE:32 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool (Set (Set (Var "X")) ($#k3_pboole :::"/\"::: ) (Set "(" (Set (Var "Y")) ($#k2_pboole :::"\/"::: ) (Set (Var "Z")) ")" )) ($#r6_pboole :::"="::: ) (Set (Set "(" (Set (Var "X")) ($#k3_pboole :::"/\"::: ) (Set (Var "Y")) ")" ) ($#k2_pboole :::"\/"::: ) (Set "(" (Set (Var "X")) ($#k3_pboole :::"/\"::: ) (Set (Var "Z")) ")" ))))) ; theorem :: PBOOLE:33 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool (Set (Set (Var "X")) ($#k2_pboole :::"\/"::: ) (Set "(" (Set (Var "Y")) ($#k3_pboole :::"/\"::: ) (Set (Var "Z")) ")" )) ($#r6_pboole :::"="::: ) (Set (Set "(" (Set (Var "X")) ($#k2_pboole :::"\/"::: ) (Set (Var "Y")) ")" ) ($#k3_pboole :::"/\"::: ) (Set "(" (Set (Var "X")) ($#k2_pboole :::"\/"::: ) (Set (Var "Z")) ")" ))))) ; theorem :: PBOOLE:34 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Set "(" (Set (Var "X")) ($#k3_pboole :::"/\"::: ) (Set (Var "Y")) ")" ) ($#k2_pboole :::"\/"::: ) (Set "(" (Set (Var "X")) ($#k3_pboole :::"/\"::: ) (Set (Var "Z")) ")" )) ($#r6_pboole :::"="::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "X")) ($#r2_pboole :::"c="::: ) (Set (Set (Var "Y")) ($#k2_pboole :::"\/"::: ) (Set (Var "Z")))))) ; theorem :: PBOOLE:35 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Set "(" (Set (Var "X")) ($#k2_pboole :::"\/"::: ) (Set (Var "Y")) ")" ) ($#k3_pboole :::"/\"::: ) (Set "(" (Set (Var "X")) ($#k2_pboole :::"\/"::: ) (Set (Var "Z")) ")" )) ($#r6_pboole :::"="::: ) (Set (Var "X")))) "holds" (Bool (Set (Set (Var "Y")) ($#k3_pboole :::"/\"::: ) (Set (Var "Z"))) ($#r2_pboole :::"c="::: ) (Set (Var "X"))))) ; theorem :: PBOOLE:36 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "X")) ($#k3_pboole :::"/\"::: ) (Set (Var "Y")) ")" ) ($#k2_pboole :::"\/"::: ) (Set "(" (Set (Var "Y")) ($#k3_pboole :::"/\"::: ) (Set (Var "Z")) ")" ) ")" ) ($#k2_pboole :::"\/"::: ) (Set "(" (Set (Var "Z")) ($#k3_pboole :::"/\"::: ) (Set (Var "X")) ")" )) ($#r6_pboole :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "X")) ($#k2_pboole :::"\/"::: ) (Set (Var "Y")) ")" ) ($#k3_pboole :::"/\"::: ) (Set "(" (Set (Var "Y")) ($#k2_pboole :::"\/"::: ) (Set (Var "Z")) ")" ) ")" ) ($#k3_pboole :::"/\"::: ) (Set "(" (Set (Var "Z")) ($#k2_pboole :::"\/"::: ) (Set (Var "X")) ")" ))))) ; theorem :: PBOOLE:37 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Set (Var "X")) ($#k2_pboole :::"\/"::: ) (Set (Var "Y"))) ($#r2_pboole :::"c="::: ) (Set (Var "Z")))) "holds" (Bool (Set (Var "X")) ($#r2_pboole :::"c="::: ) (Set (Var "Z"))))) ; theorem :: PBOOLE:38 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "X")) ($#r2_pboole :::"c="::: ) (Set (Set (Var "Y")) ($#k3_pboole :::"/\"::: ) (Set (Var "Z"))))) "holds" (Bool (Set (Var "X")) ($#r2_pboole :::"c="::: ) (Set (Var "Y"))))) ; theorem :: PBOOLE:39 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool (Set (Set "(" (Set (Var "X")) ($#k2_pboole :::"\/"::: ) (Set (Var "Y")) ")" ) ($#k2_pboole :::"\/"::: ) (Set (Var "Z"))) ($#r6_pboole :::"="::: ) (Set (Set "(" (Set (Var "X")) ($#k2_pboole :::"\/"::: ) (Set (Var "Z")) ")" ) ($#k2_pboole :::"\/"::: ) (Set "(" (Set (Var "Y")) ($#k2_pboole :::"\/"::: ) (Set (Var "Z")) ")" ))))) ; theorem :: PBOOLE:40 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool (Set (Set "(" (Set (Var "X")) ($#k3_pboole :::"/\"::: ) (Set (Var "Y")) ")" ) ($#k3_pboole :::"/\"::: ) (Set (Var "Z"))) ($#r6_pboole :::"="::: ) (Set (Set "(" (Set (Var "X")) ($#k3_pboole :::"/\"::: ) (Set (Var "Z")) ")" ) ($#k3_pboole :::"/\"::: ) (Set "(" (Set (Var "Y")) ($#k3_pboole :::"/\"::: ) (Set (Var "Z")) ")" ))))) ; theorem :: PBOOLE:41 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool (Set (Set (Var "X")) ($#k2_pboole :::"\/"::: ) (Set "(" (Set (Var "X")) ($#k2_pboole :::"\/"::: ) (Set (Var "Y")) ")" )) ($#r6_pboole :::"="::: ) (Set (Set (Var "X")) ($#k2_pboole :::"\/"::: ) (Set (Var "Y")))))) ; theorem :: PBOOLE:42 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool (Set (Set (Var "X")) ($#k3_pboole :::"/\"::: ) (Set "(" (Set (Var "X")) ($#k3_pboole :::"/\"::: ) (Set (Var "Y")) ")" )) ($#r6_pboole :::"="::: ) (Set (Set (Var "X")) ($#k3_pboole :::"/\"::: ) (Set (Var "Y")))))) ; begin theorem :: PBOOLE:43 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool (Set ($#k1_pboole :::"[[0]]"::: ) (Set (Var "I"))) ($#r2_pboole :::"c="::: ) (Set (Var "X"))))) ; theorem :: PBOOLE:44 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "X")) ($#r2_pboole :::"c="::: ) (Set ($#k1_pboole :::"[[0]]"::: ) (Set (Var "I"))))) "holds" (Bool (Set (Var "X")) ($#r6_pboole :::"="::: ) (Set ($#k1_pboole :::"[[0]]"::: ) (Set (Var "I")))))) ; theorem :: PBOOLE:45 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "X")) ($#r2_pboole :::"c="::: ) (Set (Var "Y"))) & (Bool (Set (Var "X")) ($#r2_pboole :::"c="::: ) (Set (Var "Z"))) & (Bool (Set (Set (Var "Y")) ($#k3_pboole :::"/\"::: ) (Set (Var "Z"))) ($#r6_pboole :::"="::: ) (Set ($#k1_pboole :::"[[0]]"::: ) (Set (Var "I"))))) "holds" (Bool (Set (Var "X")) ($#r6_pboole :::"="::: ) (Set ($#k1_pboole :::"[[0]]"::: ) (Set (Var "I")))))) ; theorem :: PBOOLE:46 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "X")) ($#r2_pboole :::"c="::: ) (Set (Var "Y"))) & (Bool (Set (Set (Var "Y")) ($#k3_pboole :::"/\"::: ) (Set (Var "Z"))) ($#r6_pboole :::"="::: ) (Set ($#k1_pboole :::"[[0]]"::: ) (Set (Var "I"))))) "holds" (Bool (Set (Set (Var "X")) ($#k3_pboole :::"/\"::: ) (Set (Var "Z"))) ($#r6_pboole :::"="::: ) (Set ($#k1_pboole :::"[[0]]"::: ) (Set (Var "I")))))) ; theorem :: PBOOLE:47 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool "(" (Bool (Set (Set (Var "X")) ($#k2_pboole :::"\/"::: ) (Set "(" ($#k1_pboole :::"[[0]]"::: ) (Set (Var "I")) ")" )) ($#r6_pboole :::"="::: ) (Set (Var "X"))) & (Bool (Set (Set "(" ($#k1_pboole :::"[[0]]"::: ) (Set (Var "I")) ")" ) ($#k2_pboole :::"\/"::: ) (Set (Var "X"))) ($#r6_pboole :::"="::: ) (Set (Var "X"))) ")" ))) ; theorem :: PBOOLE:48 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Set (Var "X")) ($#k2_pboole :::"\/"::: ) (Set (Var "Y"))) ($#r6_pboole :::"="::: ) (Set ($#k1_pboole :::"[[0]]"::: ) (Set (Var "I"))))) "holds" (Bool (Set (Var "X")) ($#r6_pboole :::"="::: ) (Set ($#k1_pboole :::"[[0]]"::: ) (Set (Var "I")))))) ; theorem :: PBOOLE:49 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool (Set (Set (Var "X")) ($#k3_pboole :::"/\"::: ) (Set "(" ($#k1_pboole :::"[[0]]"::: ) (Set (Var "I")) ")" )) ($#r6_pboole :::"="::: ) (Set ($#k1_pboole :::"[[0]]"::: ) (Set (Var "I")))))) ; theorem :: PBOOLE:50 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "X")) ($#r2_pboole :::"c="::: ) (Set (Set (Var "Y")) ($#k2_pboole :::"\/"::: ) (Set (Var "Z")))) & (Bool (Set (Set (Var "X")) ($#k3_pboole :::"/\"::: ) (Set (Var "Z"))) ($#r6_pboole :::"="::: ) (Set ($#k1_pboole :::"[[0]]"::: ) (Set (Var "I"))))) "holds" (Bool (Set (Var "X")) ($#r2_pboole :::"c="::: ) (Set (Var "Y"))))) ; theorem :: PBOOLE:51 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "," (Set (Var "X")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "Y")) ($#r2_pboole :::"c="::: ) (Set (Var "X"))) & (Bool (Set (Set (Var "X")) ($#k3_pboole :::"/\"::: ) (Set (Var "Y"))) ($#r6_pboole :::"="::: ) (Set ($#k1_pboole :::"[[0]]"::: ) (Set (Var "I"))))) "holds" (Bool (Set (Var "Y")) ($#r6_pboole :::"="::: ) (Set ($#k1_pboole :::"[[0]]"::: ) (Set (Var "I")))))) ; begin theorem :: PBOOLE:52 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool "(" (Bool (Set (Set (Var "X")) ($#k4_pboole :::"\"::: ) (Set (Var "Y"))) ($#r6_pboole :::"="::: ) (Set ($#k1_pboole :::"[[0]]"::: ) (Set (Var "I")))) "iff" (Bool (Set (Var "X")) ($#r2_pboole :::"c="::: ) (Set (Var "Y"))) ")" ))) ; theorem :: PBOOLE:53 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "X")) ($#r2_pboole :::"c="::: ) (Set (Var "Y")))) "holds" (Bool (Set (Set (Var "X")) ($#k4_pboole :::"\"::: ) (Set (Var "Z"))) ($#r2_pboole :::"c="::: ) (Set (Set (Var "Y")) ($#k4_pboole :::"\"::: ) (Set (Var "Z")))))) ; theorem :: PBOOLE:54 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "X")) ($#r2_pboole :::"c="::: ) (Set (Var "Y")))) "holds" (Bool (Set (Set (Var "Z")) ($#k4_pboole :::"\"::: ) (Set (Var "Y"))) ($#r2_pboole :::"c="::: ) (Set (Set (Var "Z")) ($#k4_pboole :::"\"::: ) (Set (Var "X")))))) ; theorem :: PBOOLE:55 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "," (Set (Var "V")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "X")) ($#r2_pboole :::"c="::: ) (Set (Var "Y"))) & (Bool (Set (Var "Z")) ($#r2_pboole :::"c="::: ) (Set (Var "V")))) "holds" (Bool (Set (Set (Var "X")) ($#k4_pboole :::"\"::: ) (Set (Var "V"))) ($#r2_pboole :::"c="::: ) (Set (Set (Var "Y")) ($#k4_pboole :::"\"::: ) (Set (Var "Z")))))) ; theorem :: PBOOLE:56 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool (Set (Set (Var "X")) ($#k4_pboole :::"\"::: ) (Set (Var "Y"))) ($#r2_pboole :::"c="::: ) (Set (Var "X"))))) ; theorem :: PBOOLE:57 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "X")) ($#r2_pboole :::"c="::: ) (Set (Set (Var "Y")) ($#k4_pboole :::"\"::: ) (Set (Var "X"))))) "holds" (Bool (Set (Var "X")) ($#r6_pboole :::"="::: ) (Set ($#k1_pboole :::"[[0]]"::: ) (Set (Var "I")))))) ; theorem :: PBOOLE:58 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool (Set (Set (Var "X")) ($#k4_pboole :::"\"::: ) (Set (Var "X"))) ($#r6_pboole :::"="::: ) (Set ($#k1_pboole :::"[[0]]"::: ) (Set (Var "I")))))) ; theorem :: PBOOLE:59 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool (Set (Set (Var "X")) ($#k4_pboole :::"\"::: ) (Set "(" ($#k1_pboole :::"[[0]]"::: ) (Set (Var "I")) ")" )) ($#r6_pboole :::"="::: ) (Set (Var "X"))))) ; theorem :: PBOOLE:60 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool (Set (Set "(" ($#k1_pboole :::"[[0]]"::: ) (Set (Var "I")) ")" ) ($#k4_pboole :::"\"::: ) (Set (Var "X"))) ($#r6_pboole :::"="::: ) (Set ($#k1_pboole :::"[[0]]"::: ) (Set (Var "I")))))) ; theorem :: PBOOLE:61 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool (Set (Set (Var "X")) ($#k4_pboole :::"\"::: ) (Set "(" (Set (Var "X")) ($#k2_pboole :::"\/"::: ) (Set (Var "Y")) ")" )) ($#r6_pboole :::"="::: ) (Set ($#k1_pboole :::"[[0]]"::: ) (Set (Var "I")))))) ; theorem :: PBOOLE:62 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool (Set (Set (Var "X")) ($#k3_pboole :::"/\"::: ) (Set "(" (Set (Var "Y")) ($#k4_pboole :::"\"::: ) (Set (Var "Z")) ")" )) ($#r6_pboole :::"="::: ) (Set (Set "(" (Set (Var "X")) ($#k3_pboole :::"/\"::: ) (Set (Var "Y")) ")" ) ($#k4_pboole :::"\"::: ) (Set (Var "Z")))))) ; theorem :: PBOOLE:63 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool (Set (Set "(" (Set (Var "X")) ($#k4_pboole :::"\"::: ) (Set (Var "Y")) ")" ) ($#k3_pboole :::"/\"::: ) (Set (Var "Y"))) ($#r6_pboole :::"="::: ) (Set ($#k1_pboole :::"[[0]]"::: ) (Set (Var "I")))))) ; theorem :: PBOOLE:64 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool (Set (Set (Var "X")) ($#k4_pboole :::"\"::: ) (Set "(" (Set (Var "Y")) ($#k4_pboole :::"\"::: ) (Set (Var "Z")) ")" )) ($#r6_pboole :::"="::: ) (Set (Set "(" (Set (Var "X")) ($#k4_pboole :::"\"::: ) (Set (Var "Y")) ")" ) ($#k2_pboole :::"\/"::: ) (Set "(" (Set (Var "X")) ($#k3_pboole :::"/\"::: ) (Set (Var "Z")) ")" ))))) ; theorem :: PBOOLE:65 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool (Set (Set "(" (Set (Var "X")) ($#k4_pboole :::"\"::: ) (Set (Var "Y")) ")" ) ($#k2_pboole :::"\/"::: ) (Set "(" (Set (Var "X")) ($#k3_pboole :::"/\"::: ) (Set (Var "Y")) ")" )) ($#r6_pboole :::"="::: ) (Set (Var "X"))))) ; theorem :: PBOOLE:66 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "X")) ($#r2_pboole :::"c="::: ) (Set (Var "Y")))) "holds" (Bool (Set (Var "Y")) ($#r6_pboole :::"="::: ) (Set (Set (Var "X")) ($#k2_pboole :::"\/"::: ) (Set "(" (Set (Var "Y")) ($#k4_pboole :::"\"::: ) (Set (Var "X")) ")" ))))) ; theorem :: PBOOLE:67 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool (Set (Set (Var "X")) ($#k2_pboole :::"\/"::: ) (Set "(" (Set (Var "Y")) ($#k4_pboole :::"\"::: ) (Set (Var "X")) ")" )) ($#r6_pboole :::"="::: ) (Set (Set (Var "X")) ($#k2_pboole :::"\/"::: ) (Set (Var "Y")))))) ; theorem :: PBOOLE:68 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool (Set (Set (Var "X")) ($#k4_pboole :::"\"::: ) (Set "(" (Set (Var "X")) ($#k4_pboole :::"\"::: ) (Set (Var "Y")) ")" )) ($#r6_pboole :::"="::: ) (Set (Set (Var "X")) ($#k3_pboole :::"/\"::: ) (Set (Var "Y")))))) ; theorem :: PBOOLE:69 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool (Set (Set (Var "X")) ($#k4_pboole :::"\"::: ) (Set "(" (Set (Var "Y")) ($#k3_pboole :::"/\"::: ) (Set (Var "Z")) ")" )) ($#r6_pboole :::"="::: ) (Set (Set "(" (Set (Var "X")) ($#k4_pboole :::"\"::: ) (Set (Var "Y")) ")" ) ($#k2_pboole :::"\/"::: ) (Set "(" (Set (Var "X")) ($#k4_pboole :::"\"::: ) (Set (Var "Z")) ")" ))))) ; theorem :: PBOOLE:70 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool (Set (Set (Var "X")) ($#k4_pboole :::"\"::: ) (Set "(" (Set (Var "X")) ($#k3_pboole :::"/\"::: ) (Set (Var "Y")) ")" )) ($#r6_pboole :::"="::: ) (Set (Set (Var "X")) ($#k4_pboole :::"\"::: ) (Set (Var "Y")))))) ; theorem :: PBOOLE:71 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool "(" (Bool (Set (Set (Var "X")) ($#k3_pboole :::"/\"::: ) (Set (Var "Y"))) ($#r6_pboole :::"="::: ) (Set ($#k1_pboole :::"[[0]]"::: ) (Set (Var "I")))) "iff" (Bool (Set (Set (Var "X")) ($#k4_pboole :::"\"::: ) (Set (Var "Y"))) ($#r6_pboole :::"="::: ) (Set (Var "X"))) ")" ))) ; theorem :: PBOOLE:72 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool (Set (Set "(" (Set (Var "X")) ($#k2_pboole :::"\/"::: ) (Set (Var "Y")) ")" ) ($#k4_pboole :::"\"::: ) (Set (Var "Z"))) ($#r6_pboole :::"="::: ) (Set (Set "(" (Set (Var "X")) ($#k4_pboole :::"\"::: ) (Set (Var "Z")) ")" ) ($#k2_pboole :::"\/"::: ) (Set "(" (Set (Var "Y")) ($#k4_pboole :::"\"::: ) (Set (Var "Z")) ")" ))))) ; theorem :: PBOOLE:73 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool (Set (Set "(" (Set (Var "X")) ($#k4_pboole :::"\"::: ) (Set (Var "Y")) ")" ) ($#k4_pboole :::"\"::: ) (Set (Var "Z"))) ($#r6_pboole :::"="::: ) (Set (Set (Var "X")) ($#k4_pboole :::"\"::: ) (Set "(" (Set (Var "Y")) ($#k2_pboole :::"\/"::: ) (Set (Var "Z")) ")" ))))) ; theorem :: PBOOLE:74 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool (Set (Set "(" (Set (Var "X")) ($#k3_pboole :::"/\"::: ) (Set (Var "Y")) ")" ) ($#k4_pboole :::"\"::: ) (Set (Var "Z"))) ($#r6_pboole :::"="::: ) (Set (Set "(" (Set (Var "X")) ($#k4_pboole :::"\"::: ) (Set (Var "Z")) ")" ) ($#k3_pboole :::"/\"::: ) (Set "(" (Set (Var "Y")) ($#k4_pboole :::"\"::: ) (Set (Var "Z")) ")" ))))) ; theorem :: PBOOLE:75 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool (Set (Set "(" (Set (Var "X")) ($#k2_pboole :::"\/"::: ) (Set (Var "Y")) ")" ) ($#k4_pboole :::"\"::: ) (Set (Var "Y"))) ($#r6_pboole :::"="::: ) (Set (Set (Var "X")) ($#k4_pboole :::"\"::: ) (Set (Var "Y")))))) ; theorem :: PBOOLE:76 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "X")) ($#r2_pboole :::"c="::: ) (Set (Set (Var "Y")) ($#k2_pboole :::"\/"::: ) (Set (Var "Z"))))) "holds" (Bool "(" (Bool (Set (Set (Var "X")) ($#k4_pboole :::"\"::: ) (Set (Var "Y"))) ($#r2_pboole :::"c="::: ) (Set (Var "Z"))) & (Bool (Set (Set (Var "X")) ($#k4_pboole :::"\"::: ) (Set (Var "Z"))) ($#r2_pboole :::"c="::: ) (Set (Var "Y"))) ")" ))) ; theorem :: PBOOLE:77 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool (Set (Set "(" (Set (Var "X")) ($#k2_pboole :::"\/"::: ) (Set (Var "Y")) ")" ) ($#k4_pboole :::"\"::: ) (Set "(" (Set (Var "X")) ($#k3_pboole :::"/\"::: ) (Set (Var "Y")) ")" )) ($#r6_pboole :::"="::: ) (Set (Set "(" (Set (Var "X")) ($#k4_pboole :::"\"::: ) (Set (Var "Y")) ")" ) ($#k2_pboole :::"\/"::: ) (Set "(" (Set (Var "Y")) ($#k4_pboole :::"\"::: ) (Set (Var "X")) ")" ))))) ; theorem :: PBOOLE:78 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool (Set (Set "(" (Set (Var "X")) ($#k4_pboole :::"\"::: ) (Set (Var "Y")) ")" ) ($#k4_pboole :::"\"::: ) (Set (Var "Y"))) ($#r6_pboole :::"="::: ) (Set (Set (Var "X")) ($#k4_pboole :::"\"::: ) (Set (Var "Y")))))) ; theorem :: PBOOLE:79 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool (Set (Set (Var "X")) ($#k4_pboole :::"\"::: ) (Set "(" (Set (Var "Y")) ($#k2_pboole :::"\/"::: ) (Set (Var "Z")) ")" )) ($#r6_pboole :::"="::: ) (Set (Set "(" (Set (Var "X")) ($#k4_pboole :::"\"::: ) (Set (Var "Y")) ")" ) ($#k3_pboole :::"/\"::: ) (Set "(" (Set (Var "X")) ($#k4_pboole :::"\"::: ) (Set (Var "Z")) ")" ))))) ; theorem :: PBOOLE:80 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Set (Var "X")) ($#k4_pboole :::"\"::: ) (Set (Var "Y"))) ($#r6_pboole :::"="::: ) (Set (Set (Var "Y")) ($#k4_pboole :::"\"::: ) (Set (Var "X"))))) "holds" (Bool (Set (Var "X")) ($#r6_pboole :::"="::: ) (Set (Var "Y"))))) ; theorem :: PBOOLE:81 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool (Set (Set (Var "X")) ($#k3_pboole :::"/\"::: ) (Set "(" (Set (Var "Y")) ($#k4_pboole :::"\"::: ) (Set (Var "Z")) ")" )) ($#r6_pboole :::"="::: ) (Set (Set "(" (Set (Var "X")) ($#k3_pboole :::"/\"::: ) (Set (Var "Y")) ")" ) ($#k4_pboole :::"\"::: ) (Set "(" (Set (Var "X")) ($#k3_pboole :::"/\"::: ) (Set (Var "Z")) ")" ))))) ; theorem :: PBOOLE:82 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Set (Var "X")) ($#k4_pboole :::"\"::: ) (Set (Var "Y"))) ($#r2_pboole :::"c="::: ) (Set (Var "Z")))) "holds" (Bool (Set (Var "X")) ($#r2_pboole :::"c="::: ) (Set (Set (Var "Y")) ($#k2_pboole :::"\/"::: ) (Set (Var "Z")))))) ; theorem :: PBOOLE:83 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool (Set (Set (Var "X")) ($#k4_pboole :::"\"::: ) (Set (Var "Y"))) ($#r2_pboole :::"c="::: ) (Set (Set (Var "X")) ($#k5_pboole :::"\+\"::: ) (Set (Var "Y")))))) ; theorem :: PBOOLE:84 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool (Set (Set (Var "X")) ($#k5_pboole :::"\+\"::: ) (Set "(" ($#k1_pboole :::"[[0]]"::: ) (Set (Var "I")) ")" )) ($#r6_pboole :::"="::: ) (Set (Var "X"))))) ; theorem :: PBOOLE:85 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool (Set (Set (Var "X")) ($#k5_pboole :::"\+\"::: ) (Set (Var "X"))) ($#r6_pboole :::"="::: ) (Set ($#k1_pboole :::"[[0]]"::: ) (Set (Var "I")))))) ; theorem :: PBOOLE:86 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool (Set (Set (Var "X")) ($#k2_pboole :::"\/"::: ) (Set (Var "Y"))) ($#r6_pboole :::"="::: ) (Set (Set "(" (Set (Var "X")) ($#k5_pboole :::"\+\"::: ) (Set (Var "Y")) ")" ) ($#k2_pboole :::"\/"::: ) (Set "(" (Set (Var "X")) ($#k3_pboole :::"/\"::: ) (Set (Var "Y")) ")" ))))) ; theorem :: PBOOLE:87 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool (Set (Set (Var "X")) ($#k5_pboole :::"\+\"::: ) (Set (Var "Y"))) ($#r6_pboole :::"="::: ) (Set (Set "(" (Set (Var "X")) ($#k2_pboole :::"\/"::: ) (Set (Var "Y")) ")" ) ($#k4_pboole :::"\"::: ) (Set "(" (Set (Var "X")) ($#k3_pboole :::"/\"::: ) (Set (Var "Y")) ")" ))))) ; theorem :: PBOOLE:88 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool (Set (Set "(" (Set (Var "X")) ($#k5_pboole :::"\+\"::: ) (Set (Var "Y")) ")" ) ($#k4_pboole :::"\"::: ) (Set (Var "Z"))) ($#r6_pboole :::"="::: ) (Set (Set "(" (Set (Var "X")) ($#k4_pboole :::"\"::: ) (Set "(" (Set (Var "Y")) ($#k2_pboole :::"\/"::: ) (Set (Var "Z")) ")" ) ")" ) ($#k2_pboole :::"\/"::: ) (Set "(" (Set (Var "Y")) ($#k4_pboole :::"\"::: ) (Set "(" (Set (Var "X")) ($#k2_pboole :::"\/"::: ) (Set (Var "Z")) ")" ) ")" ))))) ; theorem :: PBOOLE:89 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool (Set (Set (Var "X")) ($#k4_pboole :::"\"::: ) (Set "(" (Set (Var "Y")) ($#k5_pboole :::"\+\"::: ) (Set (Var "Z")) ")" )) ($#r6_pboole :::"="::: ) (Set (Set "(" (Set (Var "X")) ($#k4_pboole :::"\"::: ) (Set "(" (Set (Var "Y")) ($#k2_pboole :::"\/"::: ) (Set (Var "Z")) ")" ) ")" ) ($#k2_pboole :::"\/"::: ) (Set "(" (Set "(" (Set (Var "X")) ($#k3_pboole :::"/\"::: ) (Set (Var "Y")) ")" ) ($#k3_pboole :::"/\"::: ) (Set (Var "Z")) ")" ))))) ; theorem :: PBOOLE:90 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool (Set (Set "(" (Set (Var "X")) ($#k5_pboole :::"\+\"::: ) (Set (Var "Y")) ")" ) ($#k5_pboole :::"\+\"::: ) (Set (Var "Z"))) ($#r6_pboole :::"="::: ) (Set (Set (Var "X")) ($#k5_pboole :::"\+\"::: ) (Set "(" (Set (Var "Y")) ($#k5_pboole :::"\+\"::: ) (Set (Var "Z")) ")" ))))) ; theorem :: PBOOLE:91 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Set (Var "X")) ($#k4_pboole :::"\"::: ) (Set (Var "Y"))) ($#r2_pboole :::"c="::: ) (Set (Var "Z"))) & (Bool (Set (Set (Var "Y")) ($#k4_pboole :::"\"::: ) (Set (Var "X"))) ($#r2_pboole :::"c="::: ) (Set (Var "Z")))) "holds" (Bool (Set (Set (Var "X")) ($#k5_pboole :::"\+\"::: ) (Set (Var "Y"))) ($#r2_pboole :::"c="::: ) (Set (Var "Z"))))) ; theorem :: PBOOLE:92 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool (Set (Set (Var "X")) ($#k2_pboole :::"\/"::: ) (Set (Var "Y"))) ($#r6_pboole :::"="::: ) (Set (Set (Var "X")) ($#k5_pboole :::"\+\"::: ) (Set "(" (Set (Var "Y")) ($#k4_pboole :::"\"::: ) (Set (Var "X")) ")" ))))) ; theorem :: PBOOLE:93 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool (Set (Set (Var "X")) ($#k3_pboole :::"/\"::: ) (Set (Var "Y"))) ($#r6_pboole :::"="::: ) (Set (Set (Var "X")) ($#k5_pboole :::"\+\"::: ) (Set "(" (Set (Var "X")) ($#k4_pboole :::"\"::: ) (Set (Var "Y")) ")" ))))) ; theorem :: PBOOLE:94 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool (Set (Set (Var "X")) ($#k4_pboole :::"\"::: ) (Set (Var "Y"))) ($#r6_pboole :::"="::: ) (Set (Set (Var "X")) ($#k5_pboole :::"\+\"::: ) (Set "(" (Set (Var "X")) ($#k3_pboole :::"/\"::: ) (Set (Var "Y")) ")" ))))) ; theorem :: PBOOLE:95 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "," (Set (Var "X")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool (Set (Set (Var "Y")) ($#k4_pboole :::"\"::: ) (Set (Var "X"))) ($#r6_pboole :::"="::: ) (Set (Set (Var "X")) ($#k5_pboole :::"\+\"::: ) (Set "(" (Set (Var "X")) ($#k2_pboole :::"\/"::: ) (Set (Var "Y")) ")" ))))) ; theorem :: PBOOLE:96 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool (Set (Set (Var "X")) ($#k2_pboole :::"\/"::: ) (Set (Var "Y"))) ($#r6_pboole :::"="::: ) (Set (Set "(" (Set (Var "X")) ($#k5_pboole :::"\+\"::: ) (Set (Var "Y")) ")" ) ($#k5_pboole :::"\+\"::: ) (Set "(" (Set (Var "X")) ($#k3_pboole :::"/\"::: ) (Set (Var "Y")) ")" ))))) ; theorem :: PBOOLE:97 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool (Set (Set (Var "X")) ($#k3_pboole :::"/\"::: ) (Set (Var "Y"))) ($#r6_pboole :::"="::: ) (Set (Set "(" (Set (Var "X")) ($#k5_pboole :::"\+\"::: ) (Set (Var "Y")) ")" ) ($#k5_pboole :::"\+\"::: ) (Set "(" (Set (Var "X")) ($#k2_pboole :::"\/"::: ) (Set (Var "Y")) ")" ))))) ; begin theorem :: PBOOLE:98 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool "(" (Bool (Set (Var "X")) ($#r4_pboole :::"overlaps"::: ) (Set (Var "Y"))) "or" (Bool (Set (Var "X")) ($#r4_pboole :::"overlaps"::: ) (Set (Var "Z"))) ")" )) "holds" (Bool (Set (Var "X")) ($#r4_pboole :::"overlaps"::: ) (Set (Set (Var "Y")) ($#k2_pboole :::"\/"::: ) (Set (Var "Z")))))) ; theorem :: PBOOLE:99 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "X")) ($#r4_pboole :::"overlaps"::: ) (Set (Var "Y"))) & (Bool (Set (Var "Y")) ($#r2_pboole :::"c="::: ) (Set (Var "Z")))) "holds" (Bool (Set (Var "X")) ($#r4_pboole :::"overlaps"::: ) (Set (Var "Z"))))) ; theorem :: PBOOLE:100 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "X")) ($#r4_pboole :::"overlaps"::: ) (Set (Var "Y"))) & (Bool (Set (Var "X")) ($#r2_pboole :::"c="::: ) (Set (Var "Z")))) "holds" (Bool (Set (Var "Z")) ($#r4_pboole :::"overlaps"::: ) (Set (Var "Y"))))) ; theorem :: PBOOLE:101 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "," (Set (Var "V")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "X")) ($#r2_pboole :::"c="::: ) (Set (Var "Y"))) & (Bool (Set (Var "Z")) ($#r2_pboole :::"c="::: ) (Set (Var "V"))) & (Bool (Set (Var "X")) ($#r4_pboole :::"overlaps"::: ) (Set (Var "Z")))) "holds" (Bool (Set (Var "Y")) ($#r4_pboole :::"overlaps"::: ) (Set (Var "V"))))) ; theorem :: PBOOLE:102 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "X")) ($#r4_pboole :::"overlaps"::: ) (Set (Set (Var "Y")) ($#k3_pboole :::"/\"::: ) (Set (Var "Z"))))) "holds" (Bool "(" (Bool (Set (Var "X")) ($#r4_pboole :::"overlaps"::: ) (Set (Var "Y"))) & (Bool (Set (Var "X")) ($#r4_pboole :::"overlaps"::: ) (Set (Var "Z"))) ")" ))) ; theorem :: PBOOLE:103 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Z")) "," (Set (Var "V")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "X")) ($#r4_pboole :::"overlaps"::: ) (Set (Var "Z"))) & (Bool (Set (Var "X")) ($#r2_pboole :::"c="::: ) (Set (Var "V")))) "holds" (Bool (Set (Var "X")) ($#r4_pboole :::"overlaps"::: ) (Set (Set (Var "Z")) ($#k3_pboole :::"/\"::: ) (Set (Var "V")))))) ; theorem :: PBOOLE:104 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "X")) ($#r4_pboole :::"overlaps"::: ) (Set (Set (Var "Y")) ($#k4_pboole :::"\"::: ) (Set (Var "Z"))))) "holds" (Bool (Set (Var "X")) ($#r4_pboole :::"overlaps"::: ) (Set (Var "Y"))))) ; theorem :: PBOOLE:105 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "," (Set (Var "Z")) "," (Set (Var "X")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Bool "not" (Set (Var "Y")) ($#r4_pboole :::"overlaps"::: ) (Set (Var "Z"))))) "holds" (Bool "not" (Bool (Set (Set (Var "X")) ($#k3_pboole :::"/\"::: ) (Set (Var "Y"))) ($#r4_pboole :::"overlaps"::: ) (Set (Set (Var "X")) ($#k3_pboole :::"/\"::: ) (Set (Var "Z"))))))) ; theorem :: PBOOLE:106 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "X")) ($#r4_pboole :::"overlaps"::: ) (Set (Set (Var "Y")) ($#k4_pboole :::"\"::: ) (Set (Var "Z"))))) "holds" (Bool (Set (Var "Y")) ($#r4_pboole :::"overlaps"::: ) (Set (Set (Var "X")) ($#k4_pboole :::"\"::: ) (Set (Var "Z")))))) ; theorem :: PBOOLE:107 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "X")) ($#r5_pboole :::"meets"::: ) (Set (Var "Y"))) & (Bool (Set (Var "Y")) ($#r2_pboole :::"c="::: ) (Set (Var "Z")))) "holds" (Bool (Set (Var "X")) ($#r5_pboole :::"meets"::: ) (Set (Var "Z"))))) ; theorem :: PBOOLE:108 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "," (Set (Var "X")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool (Set (Var "Y")) ($#r5_pboole :::"misses"::: ) (Set (Set (Var "X")) ($#k4_pboole :::"\"::: ) (Set (Var "Y")))))) ; theorem :: PBOOLE:109 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool (Set (Set (Var "X")) ($#k3_pboole :::"/\"::: ) (Set (Var "Y"))) ($#r5_pboole :::"misses"::: ) (Set (Set (Var "X")) ($#k4_pboole :::"\"::: ) (Set (Var "Y")))))) ; theorem :: PBOOLE:110 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool (Set (Set (Var "X")) ($#k3_pboole :::"/\"::: ) (Set (Var "Y"))) ($#r5_pboole :::"misses"::: ) (Set (Set (Var "X")) ($#k5_pboole :::"\+\"::: ) (Set (Var "Y")))))) ; theorem :: PBOOLE:111 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "X")) ($#r5_pboole :::"misses"::: ) (Set (Var "Y")))) "holds" (Bool (Set (Set (Var "X")) ($#k3_pboole :::"/\"::: ) (Set (Var "Y"))) ($#r6_pboole :::"="::: ) (Set ($#k1_pboole :::"[[0]]"::: ) (Set (Var "I")))))) ; theorem :: PBOOLE:112 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_pboole :::"[[0]]"::: ) (Set (Var "I"))))) "holds" (Bool (Set (Var "X")) ($#r5_pboole :::"meets"::: ) (Set (Var "X"))))) ; theorem :: PBOOLE:113 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "X")) ($#r2_pboole :::"c="::: ) (Set (Var "Y"))) & (Bool (Set (Var "X")) ($#r2_pboole :::"c="::: ) (Set (Var "Z"))) & (Bool (Set (Var "Y")) ($#r5_pboole :::"misses"::: ) (Set (Var "Z")))) "holds" (Bool (Set (Var "X")) ($#r6_pboole :::"="::: ) (Set ($#k1_pboole :::"[[0]]"::: ) (Set (Var "I")))))) ; theorem :: PBOOLE:114 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Z")) "," (Set (Var "V")) "," (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Set (Var "Z")) ($#k2_pboole :::"\/"::: ) (Set (Var "V"))) ($#r6_pboole :::"="::: ) (Set (Set (Var "X")) ($#k2_pboole :::"\/"::: ) (Set (Var "Y")))) & (Bool (Set (Var "X")) ($#r5_pboole :::"misses"::: ) (Set (Var "Z"))) & (Bool (Set (Var "Y")) ($#r5_pboole :::"misses"::: ) (Set (Var "V")))) "holds" (Bool "(" (Bool (Set (Var "X")) ($#r6_pboole :::"="::: ) (Set (Var "V"))) & (Bool (Set (Var "Y")) ($#r6_pboole :::"="::: ) (Set (Var "Z"))) ")" ))) ; theorem :: PBOOLE:115 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "X")) ($#r5_pboole :::"misses"::: ) (Set (Var "Y")))) "holds" (Bool (Set (Set (Var "X")) ($#k4_pboole :::"\"::: ) (Set (Var "Y"))) ($#r6_pboole :::"="::: ) (Set (Var "X"))))) ; theorem :: PBOOLE:116 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "X")) ($#r5_pboole :::"misses"::: ) (Set (Var "Y")))) "holds" (Bool (Set (Set "(" (Set (Var "X")) ($#k2_pboole :::"\/"::: ) (Set (Var "Y")) ")" ) ($#k4_pboole :::"\"::: ) (Set (Var "Y"))) ($#r6_pboole :::"="::: ) (Set (Var "X"))))) ; theorem :: PBOOLE:117 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Set (Var "X")) ($#k4_pboole :::"\"::: ) (Set (Var "Y"))) ($#r6_pboole :::"="::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "X")) ($#r5_pboole :::"misses"::: ) (Set (Var "Y"))))) ; theorem :: PBOOLE:118 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool (Set (Set (Var "X")) ($#k4_pboole :::"\"::: ) (Set (Var "Y"))) ($#r5_pboole :::"misses"::: ) (Set (Set (Var "Y")) ($#k4_pboole :::"\"::: ) (Set (Var "X")))))) ; begin definitionlet "I" be ($#m1_hidden :::"set"::: ) ; let "X", "Y" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); pred "X" :::"[="::: "Y" means :: PBOOLE:def 11 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" "I" "st" (Bool (Bool (Set (Var "x")) ($#r1_pboole :::"in"::: ) "X")) "holds" (Bool (Set (Var "x")) ($#r1_pboole :::"in"::: ) "Y")); reflexivity (Bool "for" (Set (Var "X")) "," (Set (Var "x")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")) "st" (Bool (Bool (Set (Var "x")) ($#r1_pboole :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "x")) ($#r1_pboole :::"in"::: ) (Set (Var "X")))) ; end; :: deftheorem defines :::"[="::: PBOOLE:def 11 : (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool "(" (Bool (Set (Var "X")) ($#r7_pboole :::"[="::: ) (Set (Var "Y"))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "x")) ($#r1_pboole :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "x")) ($#r1_pboole :::"in"::: ) (Set (Var "Y")))) ")" ))); theorem :: PBOOLE:119 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "X")) ($#r2_pboole :::"c="::: ) (Set (Var "Y")))) "holds" (Bool (Set (Var "X")) ($#r7_pboole :::"[="::: ) (Set (Var "Y"))))) ; theorem :: PBOOLE:120 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "X")) ($#r7_pboole :::"[="::: ) (Set (Var "Y"))) & (Bool (Set (Var "Y")) ($#r7_pboole :::"[="::: ) (Set (Var "Z")))) "holds" (Bool (Set (Var "X")) ($#r7_pboole :::"[="::: ) (Set (Var "Z"))))) ; begin theorem :: PBOOLE:121 (Bool (Set ($#k1_pboole :::"[[0]]"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ($#r1_pboole :::"in"::: ) (Set ($#k1_pboole :::"[[0]]"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ; theorem :: PBOOLE:122 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k1_xboole_0 :::"{}"::: ) ) "holds" (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ; theorem :: PBOOLE:123 (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "X")) ($#r4_pboole :::"overlaps"::: ) (Set (Var "Y")))) "holds" (Bool (Set (Var "X")) ($#r5_pboole :::"meets"::: ) (Set (Var "Y"))))) ; theorem :: PBOOLE:124 (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool (Bool "not" (Set (Var "x")) ($#r3_pboole :::"in"::: ) (Set ($#k1_pboole :::"[[0]]"::: ) (Set (Var "I"))))))) ; theorem :: PBOOLE:125 (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "x")) ($#r3_pboole :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "x")) ($#r3_pboole :::"in"::: ) (Set (Var "Y")))) "holds" (Bool (Set (Set (Var "X")) ($#k3_pboole :::"/\"::: ) (Set (Var "Y"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_pboole :::"[[0]]"::: ) (Set (Var "I")))))) ; theorem :: PBOOLE:126 (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool (Bool "not" (Set (Var "X")) ($#r4_pboole :::"overlaps"::: ) (Set ($#k1_pboole :::"[[0]]"::: ) (Set (Var "I"))))))) ; theorem :: PBOOLE:127 (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Set (Var "X")) ($#k3_pboole :::"/\"::: ) (Set (Var "Y"))) ($#r6_pboole :::"="::: ) (Set ($#k1_pboole :::"[[0]]"::: ) (Set (Var "I"))))) "holds" (Bool "not" (Bool (Set (Var "X")) ($#r4_pboole :::"overlaps"::: ) (Set (Var "Y")))))) ; theorem :: PBOOLE:128 (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "X")) ($#r4_pboole :::"overlaps"::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "X")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_pboole :::"[[0]]"::: ) (Set (Var "I")))))) ; begin definitionlet "I" be ($#m1_hidden :::"set"::: ) ; let "X" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); :: original: :::"empty-yielding"::: redefine attr "X" is :::"empty-yielding"::: means :: PBOOLE:def 12 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) "I")) "holds" (Bool (Set "X" ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) "is" ($#v1_xboole_0 :::"empty"::: ) )); :: original: :::"non-empty"::: redefine attr "X" is :::"non-empty"::: means :: PBOOLE:def 13 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) "I")) "holds" (Bool "not" (Bool (Set "X" ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) "is" ($#v1_xboole_0 :::"empty"::: ) ))); end; :: deftheorem defines :::"empty-yielding"::: PBOOLE:def 12 : (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v3_relat_1 :::"empty-yielding"::: ) ) "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 "X")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" ))); :: deftheorem defines :::"non-empty"::: PBOOLE:def 13 : (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v2_relat_1 :::"non-empty"::: ) ) "iff" (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Var "I")))) "holds" (Bool "not" (Bool (Set (Set (Var "X")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) "is" ($#v1_xboole_0 :::"empty"::: ) ))) ")" ))); registrationlet "I" be ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) bbbadV3_RELAT_1() "I" ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_partfun1 :::"total"::: ) for ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) bbbadV2_RELAT_1() "I" ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_partfun1 :::"total"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "I" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) bbbadV2_RELAT_1() "I" ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_partfun1 :::"total"::: ) -> bbbadV3_RELAT_1() for ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) bbbadV3_RELAT_1() "I" ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_partfun1 :::"total"::: ) -> bbbadV2_RELAT_1() for ($#m1_hidden :::"set"::: ) ; end; theorem :: PBOOLE:129 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool "(" (Bool (Set (Var "X")) "is" bbbadV3_RELAT_1()) "iff" (Bool (Set (Var "X")) ($#r6_pboole :::"="::: ) (Set ($#k1_pboole :::"[[0]]"::: ) (Set (Var "I")))) ")" ))) ; theorem :: PBOOLE:130 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "," (Set (Var "X")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "Y")) "is" bbbadV3_RELAT_1()) & (Bool (Set (Var "X")) ($#r2_pboole :::"c="::: ) (Set (Var "Y")))) "holds" (Bool (Set (Var "X")) "is" bbbadV3_RELAT_1()))) ; theorem :: PBOOLE:131 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "X")) "is" bbbadV2_RELAT_1()) & (Bool (Set (Var "X")) ($#r2_pboole :::"c="::: ) (Set (Var "Y")))) "holds" (Bool (Set (Var "Y")) "is" bbbadV2_RELAT_1()))) ; theorem :: PBOOLE:132 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "X")) "is" bbbadV2_RELAT_1()) & (Bool (Set (Var "X")) ($#r7_pboole :::"[="::: ) (Set (Var "Y")))) "holds" (Bool (Set (Var "X")) ($#r2_pboole :::"c="::: ) (Set (Var "Y"))))) ; theorem :: PBOOLE:133 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "X")) "is" bbbadV2_RELAT_1()) & (Bool (Set (Var "X")) ($#r7_pboole :::"[="::: ) (Set (Var "Y")))) "holds" (Bool (Set (Var "Y")) "is" bbbadV2_RELAT_1()))) ; theorem :: PBOOLE:134 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "ex" (Set (Var "x")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Set (Var "x")) ($#r1_pboole :::"in"::: ) (Set (Var "X")))))) ; theorem :: PBOOLE:135 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "X")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_pboole :::"in"::: ) (Set (Var "X"))) "iff" (Bool (Set (Var "x")) ($#r1_pboole :::"in"::: ) (Set (Var "Y"))) ")" ) ")" )) "holds" (Bool (Set (Var "X")) ($#r6_pboole :::"="::: ) (Set (Var "Y")))))) ; theorem :: PBOOLE:136 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "X")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_pboole :::"in"::: ) (Set (Var "X"))) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r1_pboole :::"in"::: ) (Set (Var "Y"))) & (Bool (Set (Var "x")) ($#r1_pboole :::"in"::: ) (Set (Var "Z"))) ")" ) ")" ) ")" )) "holds" (Bool (Set (Var "X")) ($#r6_pboole :::"="::: ) (Set (Set (Var "Y")) ($#k3_pboole :::"/\"::: ) (Set (Var "Z"))))))) ; begin scheme :: PBOOLE:sch 3 MSSEx{ F1() -> ($#m1_hidden :::"set"::: ) , P1[ ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ] } : (Bool "ex" (Set (Var "f")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set F1 "(" ")" ) "st" (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" ))) "holds" (Bool P1[(Set (Var "i")) "," (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))]))) provided (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" ))) "holds" (Bool "ex" (Set (Var "j")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool P1[(Set (Var "i")) "," (Set (Var "j"))]))) proof end; scheme :: PBOOLE:sch 4 MSSLambda{ F1() -> ($#m1_hidden :::"set"::: ) , F2( ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) } : (Bool "ex" (Set (Var "f")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set F1 "(" ")" ) "st" (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" ))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set F2 "(" (Set (Var "i")) ")" )))) proof end; registrationlet "I" be ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) "I" ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_partfun1 :::"total"::: ) ($#v1_funcop_1 :::"Function-yielding"::: ) for ($#m1_hidden :::"set"::: ) ; end; definitionlet "I" be ($#m1_hidden :::"set"::: ) ; mode ManySortedFunction of "I" is ($#v1_funcop_1 :::"Function-yielding"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" "I"; end; theorem :: PBOOLE:137 (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")) "holds" (Bool (Bool "not" (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "M"))))))) ; definitionlet "I" be ($#m1_hidden :::"set"::: ) ; let "M" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); mode Component of "M" is ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k10_xtuple_0 :::"rng"::: ) "M"); end; theorem :: PBOOLE:138 (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 "A")) "being" ($#m1_subset_1 :::"Component":::) "of" (Set (Var "M")) (Bool "ex" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Var "I"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set (Var "M")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) ")" ))))) ; theorem :: PBOOLE:139 (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 "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Var "I")))) "holds" (Bool (Set (Set (Var "M")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) "is" ($#m1_subset_1 :::"Component":::) "of" (Set (Var "M")))))) ; definitionlet "I" be ($#m1_hidden :::"set"::: ) ; let "B" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); mode :::"Element"::: "of" "B" -> ($#m1_hidden :::"ManySortedSet":::) "of" "I" means :: PBOOLE:def 14 (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"))) "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set "B" ($#k1_funct_1 :::"."::: ) (Set (Var "i"))))); end; :: deftheorem defines :::"Element"::: PBOOLE:def 14 : (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B")) "," (Set (Var "b3")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool "(" (Bool (Set (Var "b3")) "is" ($#m1_pboole :::"Element"::: ) "of" (Set (Var "B"))) "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 "b3")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "B")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))))) ")" ))); begin definitionlet "I" be ($#m1_hidden :::"set"::: ) ; let "A", "B" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); mode :::"ManySortedFunction"::: "of" "A" "," "B" -> ($#m1_hidden :::"ManySortedSet":::) "of" "I" means :: PBOOLE:def 15 (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"))) "is" ($#m1_subset_1 :::"Function":::) "of" (Set "(" "A" ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) "," (Set "(" "B" ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ))); end; :: deftheorem defines :::"ManySortedFunction"::: PBOOLE:def 15 : (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "b4")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool "(" (Bool (Set (Var "b4")) "is" ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set (Var "A")) "," (Set (Var "B"))) "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"))) "is" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set (Var "A")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) "," (Set "(" (Set (Var "B")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ))) ")" ))); registrationlet "I" be ($#m1_hidden :::"set"::: ) ; let "A", "B" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); cluster -> ($#v1_funcop_1 :::"Function-yielding"::: ) for ($#m2_pboole :::"ManySortedFunction"::: ) "of" "A" "," "B"; end; registrationlet "I" be ($#m1_hidden :::"set"::: ) ; let "J" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "O" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "I")) "," (Set (Const "J")); let "F" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "J")); cluster (Set "O" ($#k3_relat_1 :::"*"::: ) "F") -> "I" ($#v4_relat_1 :::"-defined"::: ) ($#v1_partfun1 :::"total"::: ) for"I" ($#v4_relat_1 :::"-defined"::: ) ($#m1_hidden :::"Function":::); end; scheme :: PBOOLE:sch 5 LambdaDMS{ F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F2( ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) } : (Bool "ex" (Set (Var "X")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set F1 "(" ")" ) "st" (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "holds" (Bool (Set (Set (Var "X")) ($#k1_funct_1 :::"."::: ) (Set (Var "d"))) ($#r1_hidden :::"="::: ) (Set F2 "(" (Set (Var "d")) ")" )))) proof end; registrationlet "J" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "B" be bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "J")); let "j" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "J")); cluster (Set "B" ($#k1_funct_1 :::"."::: ) "j") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; definitionlet "I" be ($#m1_hidden :::"set"::: ) ; let "X", "Y" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); func :::"[|":::"X" "," "Y":::"|]"::: -> ($#m1_hidden :::"ManySortedSet":::) "of" "I" means :: PBOOLE:def 16 (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 ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" "X" ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) "," (Set "(" "Y" ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ))); end; :: deftheorem defines :::"[|"::: PBOOLE:def 16 : (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "b4")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k6_pboole :::"[|"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k6_pboole :::"|]"::: ) )) "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 ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" (Set (Var "X")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) "," (Set "(" (Set (Var "Y")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ))) ")" ))); definitionlet "I" be ($#m1_hidden :::"set"::: ) ; let "X", "Y" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); func :::"(Funcs)"::: "(" "X" "," "Y" ")" -> ($#m1_hidden :::"ManySortedSet":::) "of" "I" means :: PBOOLE:def 17 (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 ($#k1_funct_2 :::"Funcs"::: ) "(" (Set "(" "X" ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) "," (Set "(" "Y" ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) ")" ))); end; :: deftheorem defines :::"(Funcs)"::: PBOOLE:def 17 : (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "b4")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k7_pboole :::"(Funcs)"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) ")" )) "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 ($#k1_funct_2 :::"Funcs"::: ) "(" (Set "(" (Set (Var "X")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) "," (Set "(" (Set (Var "Y")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) ")" ))) ")" ))); definitionlet "I" be ($#m1_hidden :::"set"::: ) ; let "M" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); mode :::"ManySortedSubset"::: "of" "M" -> ($#m1_hidden :::"ManySortedSet":::) "of" "I" means :: PBOOLE:def 18 (Bool it ($#r2_pboole :::"c="::: ) "M"); end; :: deftheorem defines :::"ManySortedSubset"::: PBOOLE:def 18 : (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "," (Set (Var "b3")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool "(" (Bool (Set (Var "b3")) "is" ($#m3_pboole :::"ManySortedSubset"::: ) "of" (Set (Var "M"))) "iff" (Bool (Set (Var "b3")) ($#r2_pboole :::"c="::: ) (Set (Var "M"))) ")" ))); registrationlet "I" be ($#m1_hidden :::"set"::: ) ; let "M" be bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); cluster ($#v1_relat_1 :::"Relation-like"::: ) bbbadV2_RELAT_1() "I" ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_partfun1 :::"total"::: ) for ($#m3_pboole :::"ManySortedSubset"::: ) "of" "M"; end; definitionlet "F", "G" be ($#v1_funcop_1 :::"Function-yielding"::: ) ($#m1_hidden :::"Function":::); func "G" :::"**"::: "F" -> ($#m1_hidden :::"Function":::) means :: PBOOLE:def 19 (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_xtuple_0 :::"dom"::: ) "F" ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) "G" ")" ))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) it))) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" "G" ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" "F" ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"**"::: PBOOLE:def 19 : (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#v1_funcop_1 :::"Function-yielding"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "b3")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k8_pboole :::"**"::: ) (Set (Var "F")))) "iff" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "F")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "G")) ")" ))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b3"))))) "holds" (Bool (Set (Set (Var "b3")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "G")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ))) ")" ) ")" ) ")" ))); registrationlet "F", "G" be ($#v1_funcop_1 :::"Function-yielding"::: ) ($#m1_hidden :::"Function":::); cluster (Set "G" ($#k8_pboole :::"**"::: ) "F") -> ($#v1_funcop_1 :::"Function-yielding"::: ) ; end; definitionlet "I" be ($#m1_hidden :::"set"::: ) ; let "A" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); let "F" be ($#m1_hidden :::"ManySortedFunction":::) "of" (Set (Const "I")); func "F" :::".:.:"::: "A" -> ($#m1_hidden :::"ManySortedSet":::) "of" "I" means :: PBOOLE:def 20 (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 (Set "(" "F" ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k7_relat_1 :::".:"::: ) (Set "(" "A" ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" )))); end; :: deftheorem defines :::".:.:"::: PBOOLE:def 20 : (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"ManySortedFunction":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "b4")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k9_pboole :::".:.:"::: ) (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 (Set "(" (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k7_relat_1 :::".:"::: ) (Set "(" (Set (Var "A")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" )))) ")" ))))); registrationlet "I" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k1_pboole :::"[[0]]"::: ) "I") -> bbbadV3_RELAT_1() ; end; scheme :: PBOOLE:sch 6 MSSExD{ F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , P1[ ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ] } : (Bool "ex" (Set (Var "f")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set F1 "(" ")" ) "st" (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "holds" (Bool P1[(Set (Var "i")) "," (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))]))) provided (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) (Bool "ex" (Set (Var "j")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool P1[(Set (Var "i")) "," (Set (Var "j"))]))) proof end; registrationlet "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) bbbadV2_RELAT_1() "A" ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_partfun1 :::"total"::: ) -> bbbadV3_RELAT_1() for ($#m1_hidden :::"set"::: ) ; end; registrationlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) "X" ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_partfun1 :::"total"::: ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) for ($#m1_hidden :::"set"::: ) ; end; theorem :: PBOOLE:140 (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "," (Set (Var "H")) "being" ($#v1_funcop_1 :::"Function-yielding"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool (Set (Set "(" (Set (Var "H")) ($#k8_pboole :::"**"::: ) (Set (Var "G")) ")" ) ($#k8_pboole :::"**"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "H")) ($#k8_pboole :::"**"::: ) (Set "(" (Set (Var "G")) ($#k8_pboole :::"**"::: ) (Set (Var "F")) ")" )))) ; registrationlet "I" be ($#m1_hidden :::"set"::: ) ; let "f" be bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); cluster ($#v1_relat_1 :::"Relation-like"::: ) "I" ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) "f" ($#v5_funct_1 :::"-compatible"::: ) ($#v1_partfun1 :::"total"::: ) for ($#m1_hidden :::"set"::: ) ; end; theorem :: PBOOLE:141 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "p")) "being" (Set (Var "b1")) ($#v4_relat_1 :::"-defined"::: ) (Set (Var "b2")) ($#v5_funct_1 :::"-compatible"::: ) ($#m1_hidden :::"Function":::) (Bool "ex" (Set (Var "s")) "being" (Set (Var "b2")) ($#v5_funct_1 :::"-compatible"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Set (Var "p")) ($#r1_tarski :::"c="::: ) (Set (Var "s"))))))) ; theorem :: PBOOLE:142 (Bool "for" (Set (Var "I")) "," (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "s")) "," (Set (Var "ss")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool (Set (Set "(" (Set (Var "ss")) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "s")) ($#k5_relat_1 :::"|"::: ) (Set (Var "A")) ")" ) ")" ) ($#k5_relat_1 :::"|"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k5_relat_1 :::"|"::: ) (Set (Var "A")))))) ; registrationlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "Y" be ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) "Y" ($#v4_relat_1 :::"-defined"::: ) "X" ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_partfun1 :::"total"::: ) for ($#m1_hidden :::"set"::: ) ; end; theorem :: PBOOLE:143 (Bool "for" (Set (Var "I")) "," (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "being" (Set (Var "b2")) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "I")) "holds" (Bool (Set (Set (Var "M")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "M")) ($#k7_partfun1 :::"/."::: ) (Set (Var "x"))))))) ; theorem :: PBOOLE:144 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "M")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "M")) ")" ) ($#k5_relat_1 :::"|"::: ) (Set (Var "I"))) ($#r1_hidden :::"="::: ) (Set (Var "M")))))) ; theorem :: PBOOLE:145 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "being" (Set (Var "b1")) ($#v4_relat_1 :::"-defined"::: ) (Set (Var "b2")) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::) (Bool "ex" (Set (Var "s")) "being" (Set (Var "b2")) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Set (Var "p")) ($#r1_tarski :::"c="::: ) (Set (Var "s"))))))) ; theorem :: PBOOLE:146 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "X")) ($#r2_pboole :::"c="::: ) (Set (Var "Y"))) & (Bool (Set (Var "Y")) ($#r2_pboole :::"c="::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "X")) ($#r6_pboole :::"="::: ) (Set (Var "Y"))))) ; definitionlet "I" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "A", "B" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); :: original: :::"="::: redefine pred "A" :::"="::: "B" means :: PBOOLE:def 21 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "I" "holds" (Bool (Set "A" ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set "B" ($#k1_funct_1 :::"."::: ) (Set (Var "i"))))); end; :: deftheorem defines :::"="::: PBOOLE:def 21 : (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool "(" (Bool (Set (Var "A")) ($#r8_pboole :::"="::: ) (Set (Var "B"))) "iff" (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "I")) "holds" (Bool (Set (Set (Var "A")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "B")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))))) ")" )));