:: COHSP_1 semantic presentation begin definitionlet "X" be ($#m1_hidden :::"set"::: ) ; redefine attr "X" is :::"binary_complete"::: means :: COHSP_1:def 1 (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set (Set (Var "a")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "b"))) ($#r2_hidden :::"in"::: ) "X") ")" )) "holds" (Bool (Set ($#k3_tarski :::"union"::: ) (Set (Var "A"))) ($#r2_hidden :::"in"::: ) "X")); end; :: deftheorem defines :::"binary_complete"::: COHSP_1:def 1 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v1_coh_sp :::"binary_complete"::: ) ) "iff" (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set (Set (Var "a")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "b"))) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) ")" )) "holds" (Bool (Set ($#k3_tarski :::"union"::: ) (Set (Var "A"))) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) ")" )); registration cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#v1_classes1 :::"subset-closed"::: ) ($#v1_coh_sp :::"binary_complete"::: ) for ($#m1_hidden :::"set"::: ) ; end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; func :::"FlatCoh"::: "X" -> ($#m1_hidden :::"set"::: ) equals :: COHSP_1:def 2 (Set ($#k2_coh_sp :::"CohSp"::: ) (Set "(" ($#k6_partfun1 :::"id"::: ) "X" ")" )); func :::"Sub_of_Fin"::: "X" -> ($#m1_subset_1 :::"Subset":::) "of" "X" means :: COHSP_1:def 3 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "X") & (Bool (Set (Var "x")) "is" ($#v1_finset_1 :::"finite"::: ) ) ")" ) ")" )); end; :: deftheorem defines :::"FlatCoh"::: COHSP_1:def 2 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k1_cohsp_1 :::"FlatCoh"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#k2_coh_sp :::"CohSp"::: ) (Set "(" ($#k6_partfun1 :::"id"::: ) (Set (Var "X")) ")" )))); :: deftheorem defines :::"Sub_of_Fin"::: COHSP_1:def 3 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k2_cohsp_1 :::"Sub_of_Fin"::: ) (Set (Var "X")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "x")) "is" ($#v1_finset_1 :::"finite"::: ) ) ")" ) ")" )) ")" ))); theorem :: COHSP_1:1 (Bool "for" (Set (Var "X")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_cohsp_1 :::"FlatCoh"::: ) (Set (Var "X")))) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) "or" (Bool "ex" (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "y")) ($#k1_tarski :::"}"::: ) )) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) ")" )) ")" ) ")" )) ; theorem :: COHSP_1:2 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k3_tarski :::"union"::: ) (Set "(" ($#k1_cohsp_1 :::"FlatCoh"::: ) (Set (Var "X")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "X")))) ; theorem :: COHSP_1:3 (Bool "for" (Set (Var "X")) "being" ($#v1_finset_1 :::"finite"::: ) ($#v1_classes1 :::"subset-closed"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k2_cohsp_1 :::"Sub_of_Fin"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set (Var "X")))) ; registration cluster (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) ) -> ($#v1_classes1 :::"subset-closed"::: ) ($#v1_coh_sp :::"binary_complete"::: ) ; let "X" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k1_zfmisc_1 :::"bool"::: ) "X") -> ($#v1_classes1 :::"subset-closed"::: ) ($#v1_coh_sp :::"binary_complete"::: ) ; cluster (Set ($#k1_cohsp_1 :::"FlatCoh"::: ) "X") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_classes1 :::"subset-closed"::: ) ($#v1_coh_sp :::"binary_complete"::: ) ; end; registrationlet "C" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_classes1 :::"subset-closed"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k2_cohsp_1 :::"Sub_of_Fin"::: ) "C") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_classes1 :::"subset-closed"::: ) ; end; theorem :: COHSP_1:4 (Bool (Set ($#k1_coh_sp :::"Web"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ; scheme :: COHSP_1:sch 1 MinimalElementwrtIncl{ F1() -> ($#m1_hidden :::"set"::: ) , F2() -> ($#m1_hidden :::"set"::: ) , P1[ ($#m1_hidden :::"set"::: ) ] } : (Bool "ex" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set F2 "(" ")" )) & (Bool P1[(Set (Var "a"))]) & (Bool "(" "for" (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set F2 "(" ")" )) & (Bool P1[(Set (Var "b"))]) & (Bool (Set (Var "b")) ($#r1_tarski :::"c="::: ) (Set (Var "a")))) "holds" (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Var "a"))) ")" ) ")" )) provided (Bool "(" (Bool (Set F1 "(" ")" ) ($#r2_hidden :::"in"::: ) (Set F2 "(" ")" )) & (Bool P1[(Set F1 "(" ")" )]) ")" ) and (Bool (Set F1 "(" ")" ) "is" ($#v1_finset_1 :::"finite"::: ) ) proof end; registrationlet "C" be ($#m1_hidden :::"Coherence_Space":::); cluster ($#v1_finset_1 :::"finite"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" "C"; end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; attr "X" is :::"c=directed"::: means :: COHSP_1:def 4 (Bool "for" (Set (Var "Y")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" "X" (Bool "ex" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set ($#k3_tarski :::"union"::: ) (Set (Var "Y"))) ($#r1_tarski :::"c="::: ) (Set (Var "a"))) & (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) "X") ")" ))); attr "X" is :::"c=filtered"::: means :: COHSP_1:def 5 (Bool "for" (Set (Var "Y")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" "X" (Bool "ex" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool "(" "for" (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "Y")))) "holds" (Bool (Set (Var "a")) ($#r1_tarski :::"c="::: ) (Set (Var "y"))) ")" ) & (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) "X") ")" ))); end; :: deftheorem defines :::"c=directed"::: COHSP_1:def 4 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v1_cohsp_1 :::"c=directed"::: ) ) "iff" (Bool "for" (Set (Var "Y")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "ex" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set ($#k3_tarski :::"union"::: ) (Set (Var "Y"))) ($#r1_tarski :::"c="::: ) (Set (Var "a"))) & (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) ")" ))) ")" )); :: deftheorem defines :::"c=filtered"::: COHSP_1:def 5 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v2_cohsp_1 :::"c=filtered"::: ) ) "iff" (Bool "for" (Set (Var "Y")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "ex" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool "(" "for" (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "Y")))) "holds" (Bool (Set (Var "a")) ($#r1_tarski :::"c="::: ) (Set (Var "y"))) ")" ) & (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) ")" ))) ")" )); registration cluster ($#v1_cohsp_1 :::"c=directed"::: ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) for ($#m1_hidden :::"set"::: ) ; cluster ($#v2_cohsp_1 :::"c=filtered"::: ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) for ($#m1_hidden :::"set"::: ) ; end; theorem :: COHSP_1:5 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) "is" ($#v1_cohsp_1 :::"c=directed"::: ) )) "holds" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool "ex" (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Set (Var "a")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "b"))) ($#r1_tarski :::"c="::: ) (Set (Var "c"))) & (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) ")" )))) ; theorem :: COHSP_1:6 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool "ex" (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Set (Var "a")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "b"))) ($#r1_tarski :::"c="::: ) (Set (Var "c"))) & (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) ")" )) ")" )) "holds" (Bool (Set (Var "X")) "is" ($#v1_cohsp_1 :::"c=directed"::: ) )) ; theorem :: COHSP_1:7 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) "is" ($#v2_cohsp_1 :::"c=filtered"::: ) )) "holds" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool "ex" (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "c")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "a")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "b")))) & (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) ")" )))) ; theorem :: COHSP_1:8 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool "ex" (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "c")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "a")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "b")))) & (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) ")" )) ")" )) "holds" (Bool (Set (Var "X")) "is" ($#v2_cohsp_1 :::"c=filtered"::: ) )) ; theorem :: COHSP_1:9 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) "is" ($#v1_cohsp_1 :::"c=directed"::: ) ) & (Bool (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) "is" ($#v2_cohsp_1 :::"c=filtered"::: ) ) ")" )) ; theorem :: COHSP_1:10 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k1_enumset1 :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set "(" (Set (Var "x")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "y")) ")" ) ($#k1_enumset1 :::"}"::: ) ) "is" ($#v1_cohsp_1 :::"c=directed"::: ) )) ; theorem :: COHSP_1:11 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k1_enumset1 :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set "(" (Set (Var "x")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "y")) ")" ) ($#k1_enumset1 :::"}"::: ) ) "is" ($#v2_cohsp_1 :::"c=filtered"::: ) )) ; registration cluster ($#v1_finset_1 :::"finite"::: ) ($#v1_cohsp_1 :::"c=directed"::: ) ($#v2_cohsp_1 :::"c=filtered"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "C" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster ($#v1_finset_1 :::"finite"::: ) ($#v1_cohsp_1 :::"c=directed"::: ) ($#v2_cohsp_1 :::"c=filtered"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) "C"); end; theorem :: COHSP_1:12 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k5_finsub_1 :::"Fin"::: ) (Set (Var "X"))) "is" ($#v1_cohsp_1 :::"c=directed"::: ) ) & (Bool (Set ($#k5_finsub_1 :::"Fin"::: ) (Set (Var "X"))) "is" ($#v2_cohsp_1 :::"c=filtered"::: ) ) ")" )) ; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k5_finsub_1 :::"Fin"::: ) "X") -> ($#v1_cohsp_1 :::"c=directed"::: ) ($#v2_cohsp_1 :::"c=filtered"::: ) ; end; registrationlet "C" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_classes1 :::"subset-closed"::: ) ($#m1_hidden :::"set"::: ) ; cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v4_finsub_1 :::"preBoolean"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) "C"); end; definitionlet "C" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_classes1 :::"subset-closed"::: ) ($#m1_hidden :::"set"::: ) ; let "a" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "C")); :: original: :::"Fin"::: redefine func :::"Fin"::: "a" -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v4_finsub_1 :::"preBoolean"::: ) ($#m1_subset_1 :::"Subset":::) "of" "C"; end; theorem :: COHSP_1:13 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) "is" ($#v1_cohsp_1 :::"c=directed"::: ) ) & (Bool (Set (Var "Y")) ($#r1_tarski :::"c="::: ) (Set ($#k3_tarski :::"union"::: ) (Set (Var "X")))) & (Bool (Set (Var "Y")) "is" ($#v1_finset_1 :::"finite"::: ) )) "holds" (Bool "ex" (Set (Var "Z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "Z")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "Y")) ($#r1_tarski :::"c="::: ) (Set (Var "Z"))) ")" )))) ; notationlet "X" be ($#m1_hidden :::"set"::: ) ; synonym :::"multiplicative"::: "X" for :::"cap-closed"::: ; end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; attr "X" is :::"d.union-closed"::: means :: COHSP_1:def 6 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" "X" "st" (Bool (Bool (Set (Var "A")) "is" ($#v1_cohsp_1 :::"c=directed"::: ) )) "holds" (Bool (Set ($#k3_tarski :::"union"::: ) (Set (Var "A"))) ($#r2_hidden :::"in"::: ) "X")); end; :: deftheorem defines :::"d.union-closed"::: COHSP_1:def 6 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v3_cohsp_1 :::"d.union-closed"::: ) ) "iff" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v1_cohsp_1 :::"c=directed"::: ) )) "holds" (Bool (Set ($#k3_tarski :::"union"::: ) (Set (Var "A"))) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) ")" )); registration cluster ($#v1_classes1 :::"subset-closed"::: ) -> ($#v2_finsub_1 :::"multiplicative"::: ) for ($#m1_hidden :::"set"::: ) ; end; theorem :: COHSP_1:14 (Bool "for" (Set (Var "C")) "being" ($#m1_hidden :::"Coherence_Space":::) (Bool "for" (Set (Var "A")) "being" ($#v1_cohsp_1 :::"c=directed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "C")) "holds" (Bool (Set ($#k3_tarski :::"union"::: ) (Set (Var "A"))) ($#r2_hidden :::"in"::: ) (Set (Var "C"))))) ; registration cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_classes1 :::"subset-closed"::: ) ($#v1_coh_sp :::"binary_complete"::: ) -> ($#v3_cohsp_1 :::"d.union-closed"::: ) for ($#m1_hidden :::"set"::: ) ; end; registration cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_finsub_1 :::"multiplicative"::: ) ($#v1_classes1 :::"subset-closed"::: ) ($#v1_coh_sp :::"binary_complete"::: ) ($#v3_cohsp_1 :::"d.union-closed"::: ) for ($#m1_hidden :::"set"::: ) ; end; definitionlet "C" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v3_cohsp_1 :::"d.union-closed"::: ) ($#m1_hidden :::"set"::: ) ; let "A" be ($#v1_cohsp_1 :::"c=directed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "C")); :: original: :::"union"::: redefine func :::"union"::: "A" -> ($#m1_subset_1 :::"Element"::: ) "of" "C"; end; definitionlet "X", "Y" be ($#m1_hidden :::"set"::: ) ; pred "X" :::"includes_lattice_of"::: "Y" means :: COHSP_1:def 7 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) "Y") & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) "Y")) "holds" (Bool "(" (Bool (Set (Set (Var "a")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "b"))) ($#r2_hidden :::"in"::: ) "X") & (Bool (Set (Set (Var "a")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "b"))) ($#r2_hidden :::"in"::: ) "X") ")" )); end; :: deftheorem defines :::"includes_lattice_of"::: COHSP_1:def 7 : (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "X")) ($#r1_cohsp_1 :::"includes_lattice_of"::: ) (Set (Var "Y"))) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "Y"))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "Y")))) "holds" (Bool "(" (Bool (Set (Set (Var "a")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "b"))) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Set (Var "a")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "b"))) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) ")" )) ")" )); theorem :: COHSP_1:15 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r1_cohsp_1 :::"includes_lattice_of"::: ) (Set (Var "X")))) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v1_cohsp_1 :::"c=directed"::: ) ) & (Bool (Set (Var "X")) "is" ($#v2_cohsp_1 :::"c=filtered"::: ) ) ")" )) ; definitionlet "X", "x", "y" be ($#m1_hidden :::"set"::: ) ; pred "X" :::"includes_lattice_of"::: "x" "," "y" means :: COHSP_1:def 8 (Bool "X" ($#r1_cohsp_1 :::"includes_lattice_of"::: ) (Set ($#k2_tarski :::"{"::: ) "x" "," "y" ($#k2_tarski :::"}"::: ) )); end; :: deftheorem defines :::"includes_lattice_of"::: COHSP_1:def 8 : (Bool "for" (Set (Var "X")) "," (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "X")) ($#r2_cohsp_1 :::"includes_lattice_of"::: ) (Set (Var "x")) "," (Set (Var "y"))) "iff" (Bool (Set (Var "X")) ($#r1_cohsp_1 :::"includes_lattice_of"::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) )) ")" )); theorem :: COHSP_1:16 (Bool "for" (Set (Var "X")) "," (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "X")) ($#r2_cohsp_1 :::"includes_lattice_of"::: ) (Set (Var "x")) "," (Set (Var "y"))) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Set (Var "x")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "y"))) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Set (Var "x")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "y"))) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) ")" ) ")" )) ; begin definitionlet "f" be ($#m1_hidden :::"Function":::); attr "f" is :::"union-distributive"::: means :: COHSP_1:def 9 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k9_xtuple_0 :::"dom"::: ) "f" ")" ) "st" (Bool (Bool (Set ($#k3_tarski :::"union"::: ) (Set (Var "A"))) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "f"))) "holds" (Bool (Set "f" ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_tarski :::"union"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) (Set "(" "f" ($#k7_relat_1 :::".:"::: ) (Set (Var "A")) ")" )))); attr "f" is :::"d.union-distributive"::: means :: COHSP_1:def 10 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k9_xtuple_0 :::"dom"::: ) "f" ")" ) "st" (Bool (Bool (Set (Var "A")) "is" ($#v1_cohsp_1 :::"c=directed"::: ) ) & (Bool (Set ($#k3_tarski :::"union"::: ) (Set (Var "A"))) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "f"))) "holds" (Bool (Set "f" ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_tarski :::"union"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) (Set "(" "f" ($#k7_relat_1 :::".:"::: ) (Set (Var "A")) ")" )))); end; :: deftheorem defines :::"union-distributive"::: COHSP_1:def 9 : (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v4_cohsp_1 :::"union-distributive"::: ) ) "iff" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")) ")" ) "st" (Bool (Bool (Set ($#k3_tarski :::"union"::: ) (Set (Var "A"))) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_tarski :::"union"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) (Set "(" (Set (Var "f")) ($#k7_relat_1 :::".:"::: ) (Set (Var "A")) ")" )))) ")" )); :: deftheorem defines :::"d.union-distributive"::: COHSP_1:def 10 : (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v5_cohsp_1 :::"d.union-distributive"::: ) ) "iff" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")) ")" ) "st" (Bool (Bool (Set (Var "A")) "is" ($#v1_cohsp_1 :::"c=directed"::: ) ) & (Bool (Set ($#k3_tarski :::"union"::: ) (Set (Var "A"))) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_tarski :::"union"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) (Set "(" (Set (Var "f")) ($#k7_relat_1 :::".:"::: ) (Set (Var "A")) ")" )))) ")" )); definitionlet "f" be ($#m1_hidden :::"Function":::); attr "f" is :::"c=-monotone"::: means :: COHSP_1:def 11 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "f")) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "f")) & (Bool (Set (Var "a")) ($#r1_tarski :::"c="::: ) (Set (Var "b")))) "holds" (Bool (Set "f" ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_tarski :::"c="::: ) (Set "f" ($#k1_funct_1 :::"."::: ) (Set (Var "b"))))); attr "f" is :::"cap-distributive"::: means :: COHSP_1:def 12 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) "f") ($#r2_cohsp_1 :::"includes_lattice_of"::: ) (Set (Var "a")) "," (Set (Var "b")))) "holds" (Bool (Set "f" ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "a")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "b")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" "f" ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" "f" ($#k1_funct_1 :::"."::: ) (Set (Var "b")) ")" )))); end; :: deftheorem defines :::"c=-monotone"::: COHSP_1:def 11 : (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v6_cohsp_1 :::"c=-monotone"::: ) ) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "a")) ($#r1_tarski :::"c="::: ) (Set (Var "b")))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "b"))))) ")" )); :: deftheorem defines :::"cap-distributive"::: COHSP_1:def 12 : (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v7_cohsp_1 :::"cap-distributive"::: ) ) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) ($#r2_cohsp_1 :::"includes_lattice_of"::: ) (Set (Var "a")) "," (Set (Var "b")))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "a")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "b")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "b")) ")" )))) ")" )); registration cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v5_cohsp_1 :::"d.union-distributive"::: ) -> ($#v6_cohsp_1 :::"c=-monotone"::: ) for ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v4_cohsp_1 :::"union-distributive"::: ) -> ($#v5_cohsp_1 :::"d.union-distributive"::: ) for ($#m1_hidden :::"set"::: ) ; end; theorem :: COHSP_1:17 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "f")) "is" ($#v4_cohsp_1 :::"union-distributive"::: ) )) "holds" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Set (Var "x")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "y"))) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "y")) ")" ))))) ; theorem :: COHSP_1:18 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "f")) "is" ($#v4_cohsp_1 :::"union-distributive"::: ) )) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ; registrationlet "C1", "C2" be ($#m1_hidden :::"Coherence_Space":::); cluster ($#v1_relat_1 :::"Relation-like"::: ) "C1" ($#v4_relat_1 :::"-defined"::: ) "C2" ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) bbbadV1_FUNCT_2("C1" "," "C2") ($#v4_cohsp_1 :::"union-distributive"::: ) ($#v7_cohsp_1 :::"cap-distributive"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) "C1" "," "C2" ($#k2_zfmisc_1 :::":]"::: ) )); end; registrationlet "C" be ($#m1_hidden :::"Coherence_Space":::); cluster ($#v1_relat_1 :::"Relation-like"::: ) "C" ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) bbbadV1_PARTFUN1("C") ($#v4_cohsp_1 :::"union-distributive"::: ) ($#v7_cohsp_1 :::"cap-distributive"::: ) for ($#m1_hidden :::"set"::: ) ; end; definitionlet "f" be ($#m1_hidden :::"Function":::); attr "f" is :::"U-continuous"::: means :: COHSP_1:def 13 (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) "f") "is" ($#v3_cohsp_1 :::"d.union-closed"::: ) ) & (Bool "f" "is" ($#v5_cohsp_1 :::"d.union-distributive"::: ) ) ")" ); end; :: deftheorem defines :::"U-continuous"::: COHSP_1:def 13 : (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v8_cohsp_1 :::"U-continuous"::: ) ) "iff" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) "is" ($#v3_cohsp_1 :::"d.union-closed"::: ) ) & (Bool (Set (Var "f")) "is" ($#v5_cohsp_1 :::"d.union-distributive"::: ) ) ")" ) ")" )); definitionlet "f" be ($#m1_hidden :::"Function":::); attr "f" is :::"U-stable"::: means :: COHSP_1:def 14 (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) "f") "is" ($#v2_finsub_1 :::"multiplicative"::: ) ) & (Bool "f" "is" ($#v8_cohsp_1 :::"U-continuous"::: ) ) & (Bool "f" "is" ($#v7_cohsp_1 :::"cap-distributive"::: ) ) ")" ); end; :: deftheorem defines :::"U-stable"::: COHSP_1:def 14 : (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v9_cohsp_1 :::"U-stable"::: ) ) "iff" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) "is" ($#v2_finsub_1 :::"multiplicative"::: ) ) & (Bool (Set (Var "f")) "is" ($#v8_cohsp_1 :::"U-continuous"::: ) ) & (Bool (Set (Var "f")) "is" ($#v7_cohsp_1 :::"cap-distributive"::: ) ) ")" ) ")" )); definitionlet "f" be ($#m1_hidden :::"Function":::); attr "f" is :::"U-linear"::: means :: COHSP_1:def 15 (Bool "(" (Bool "f" "is" ($#v9_cohsp_1 :::"U-stable"::: ) ) & (Bool "f" "is" ($#v4_cohsp_1 :::"union-distributive"::: ) ) ")" ); end; :: deftheorem defines :::"U-linear"::: COHSP_1:def 15 : (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v10_cohsp_1 :::"U-linear"::: ) ) "iff" (Bool "(" (Bool (Set (Var "f")) "is" ($#v9_cohsp_1 :::"U-stable"::: ) ) & (Bool (Set (Var "f")) "is" ($#v4_cohsp_1 :::"union-distributive"::: ) ) ")" ) ")" )); registration cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v8_cohsp_1 :::"U-continuous"::: ) -> ($#v5_cohsp_1 :::"d.union-distributive"::: ) for ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v9_cohsp_1 :::"U-stable"::: ) -> ($#v7_cohsp_1 :::"cap-distributive"::: ) ($#v8_cohsp_1 :::"U-continuous"::: ) for ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v10_cohsp_1 :::"U-linear"::: ) -> ($#v4_cohsp_1 :::"union-distributive"::: ) ($#v9_cohsp_1 :::"U-stable"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "X" be ($#v3_cohsp_1 :::"d.union-closed"::: ) ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) "X" ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) bbbadV1_PARTFUN1("X") ($#v5_cohsp_1 :::"d.union-distributive"::: ) -> ($#v8_cohsp_1 :::"U-continuous"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "X" be ($#v2_finsub_1 :::"multiplicative"::: ) ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) "X" ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) bbbadV1_PARTFUN1("X") ($#v7_cohsp_1 :::"cap-distributive"::: ) ($#v8_cohsp_1 :::"U-continuous"::: ) -> ($#v9_cohsp_1 :::"U-stable"::: ) for ($#m1_hidden :::"set"::: ) ; end; registration cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v4_cohsp_1 :::"union-distributive"::: ) ($#v9_cohsp_1 :::"U-stable"::: ) -> ($#v10_cohsp_1 :::"U-linear"::: ) for ($#m1_hidden :::"set"::: ) ; end; registration cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v10_cohsp_1 :::"U-linear"::: ) for ($#m1_hidden :::"set"::: ) ; let "C" be ($#m1_hidden :::"Coherence_Space":::); cluster ($#v1_relat_1 :::"Relation-like"::: ) "C" ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) bbbadV1_PARTFUN1("C") ($#v10_cohsp_1 :::"U-linear"::: ) for ($#m1_hidden :::"set"::: ) ; let "B" be ($#m1_hidden :::"Coherence_Space":::); cluster ($#v1_relat_1 :::"Relation-like"::: ) "B" ($#v4_relat_1 :::"-defined"::: ) "C" ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) bbbadV1_FUNCT_2("B" "," "C") ($#v10_cohsp_1 :::"U-linear"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) "B" "," "C" ($#k2_zfmisc_1 :::":]"::: ) )); end; registrationlet "f" be ($#v8_cohsp_1 :::"U-continuous"::: ) ($#m1_hidden :::"Function":::); cluster (Set ($#k9_xtuple_0 :::"proj1"::: ) "f") -> ($#v3_cohsp_1 :::"d.union-closed"::: ) ; end; registrationlet "f" be ($#v9_cohsp_1 :::"U-stable"::: ) ($#m1_hidden :::"Function":::); cluster (Set ($#k9_xtuple_0 :::"proj1"::: ) "f") -> ($#v2_finsub_1 :::"multiplicative"::: ) ; end; theorem :: COHSP_1:19 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k3_tarski :::"union"::: ) (Set "(" ($#k5_finsub_1 :::"Fin"::: ) (Set (Var "X")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "X")))) ; theorem :: COHSP_1:20 (Bool "for" (Set (Var "f")) "being" ($#v8_cohsp_1 :::"U-continuous"::: ) ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) "is" ($#v1_classes1 :::"subset-closed"::: ) )) "holds" (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) (Set "(" (Set (Var "f")) ($#k7_relat_1 :::".:"::: ) (Set "(" ($#k5_finsub_1 :::"Fin"::: ) (Set (Var "a")) ")" ) ")" ))))) ; theorem :: COHSP_1:21 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) "is" ($#v1_classes1 :::"subset-closed"::: ) )) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v8_cohsp_1 :::"U-continuous"::: ) ) "iff" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) "is" ($#v3_cohsp_1 :::"d.union-closed"::: ) ) & (Bool (Set (Var "f")) "is" ($#v6_cohsp_1 :::"c=-monotone"::: ) ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))))) "holds" (Bool "ex" (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "b")) "is" ($#v1_finset_1 :::"finite"::: ) ) & (Bool (Set (Var "b")) ($#r1_tarski :::"c="::: ) (Set (Var "a"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "b")))) ")" )) ")" ) ")" ) ")" )) ; theorem :: COHSP_1:22 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) "is" ($#v1_classes1 :::"subset-closed"::: ) ) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) "is" ($#v3_cohsp_1 :::"d.union-closed"::: ) )) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v9_cohsp_1 :::"U-stable"::: ) ) "iff" (Bool "(" (Bool (Set (Var "f")) "is" ($#v6_cohsp_1 :::"c=-monotone"::: ) ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))))) "holds" (Bool "ex" (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "b")) "is" ($#v1_finset_1 :::"finite"::: ) ) & (Bool (Set (Var "b")) ($#r1_tarski :::"c="::: ) (Set (Var "a"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "b")))) & (Bool "(" "for" (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "c")) ($#r1_tarski :::"c="::: ) (Set (Var "a"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))))) "holds" (Bool (Set (Var "b")) ($#r1_tarski :::"c="::: ) (Set (Var "c"))) ")" ) ")" )) ")" ) ")" ) ")" )) ; theorem :: COHSP_1:23 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) "is" ($#v1_classes1 :::"subset-closed"::: ) ) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) "is" ($#v3_cohsp_1 :::"d.union-closed"::: ) )) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v10_cohsp_1 :::"U-linear"::: ) ) "iff" (Bool "(" (Bool (Set (Var "f")) "is" ($#v6_cohsp_1 :::"c=-monotone"::: ) ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))))) "holds" (Bool "ex" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "a"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ))) & (Bool "(" "for" (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "b")) ($#r1_tarski :::"c="::: ) (Set (Var "a"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "b"))))) "holds" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b"))) ")" ) ")" )) ")" ) ")" ) ")" )) ; begin definitionlet "f" be ($#m1_hidden :::"Function":::); func :::"graph"::: "f" -> ($#m1_hidden :::"set"::: ) means :: COHSP_1:def 16 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "ex" (Set (Var "y")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "ex" (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "z")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "f")) & (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set "f" ($#k1_funct_1 :::"."::: ) (Set (Var "y")))) ")" ))) ")" )); end; :: deftheorem defines :::"graph"::: COHSP_1:def 16 : (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k5_cohsp_1 :::"graph"::: ) (Set (Var "f")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) "iff" (Bool "ex" (Set (Var "y")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "ex" (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "z")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "y")))) ")" ))) ")" )) ")" ))); definitionlet "C1", "C2" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "C1")) "," (Set (Const "C2")); :: original: :::"graph"::: redefine func :::"graph"::: "f" -> ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) "C1" "," (Set "(" ($#k3_tarski :::"union"::: ) "C2" ")" ) ($#k2_zfmisc_1 :::":]"::: ) ); end; registrationlet "f" be ($#m1_hidden :::"Function":::); cluster (Set ($#k5_cohsp_1 :::"graph"::: ) "f") -> ($#v1_relat_1 :::"Relation-like"::: ) ; end; theorem :: COHSP_1:24 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k5_cohsp_1 :::"graph"::: ) (Set (Var "f")))) "iff" (Bool "(" (Bool (Set (Var "x")) "is" ($#v1_finset_1 :::"finite"::: ) ) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))) ")" ) ")" ))) ; theorem :: COHSP_1:25 (Bool "for" (Set (Var "f")) "being" ($#v6_cohsp_1 :::"c=-monotone"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "a")) ($#r1_tarski :::"c="::: ) (Set (Var "b"))) & (Bool (Set (Var "b")) "is" ($#v1_finset_1 :::"finite"::: ) )) "holds" (Bool "for" (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k5_cohsp_1 :::"graph"::: ) (Set (Var "f"))))) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "b")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k5_cohsp_1 :::"graph"::: ) (Set (Var "f"))))))) ; theorem :: COHSP_1:26 (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#m1_hidden :::"Coherence_Space":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "C1")) "," (Set (Var "C2")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "C1")) (Bool "for" (Set (Var "y1")) "," (Set (Var "y2")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "y1")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k6_cohsp_1 :::"graph"::: ) (Set (Var "f")))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "y2")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k6_cohsp_1 :::"graph"::: ) (Set (Var "f"))))) "holds" (Bool (Set ($#k2_tarski :::"{"::: ) (Set (Var "y1")) "," (Set (Var "y2")) ($#k2_tarski :::"}"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "C2"))))))) ; theorem :: COHSP_1:27 (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#m1_hidden :::"Coherence_Space":::) (Bool "for" (Set (Var "f")) "being" ($#v6_cohsp_1 :::"c=-monotone"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "C1")) "," (Set (Var "C2")) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "C1")) "st" (Bool (Bool (Set (Set (Var "a")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "b"))) ($#r2_hidden :::"in"::: ) (Set (Var "C1")))) "holds" (Bool "for" (Set (Var "y1")) "," (Set (Var "y2")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "y1")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k6_cohsp_1 :::"graph"::: ) (Set (Var "f")))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "b")) "," (Set (Var "y2")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k6_cohsp_1 :::"graph"::: ) (Set (Var "f"))))) "holds" (Bool (Set ($#k2_tarski :::"{"::: ) (Set (Var "y1")) "," (Set (Var "y2")) ($#k2_tarski :::"}"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "C2"))))))) ; theorem :: COHSP_1:28 (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#m1_hidden :::"Coherence_Space":::) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#v8_cohsp_1 :::"U-continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "C1")) "," (Set (Var "C2")) "st" (Bool (Bool (Set ($#k6_cohsp_1 :::"graph"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k6_cohsp_1 :::"graph"::: ) (Set (Var "g"))))) "holds" (Bool (Set (Var "f")) ($#r2_funct_2 :::"="::: ) (Set (Var "g"))))) ; theorem :: COHSP_1:29 (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#m1_hidden :::"Coherence_Space":::) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "C1")) "," (Set "(" ($#k3_tarski :::"union"::: ) (Set (Var "C2")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Set (Var "x")) ($#k1_xtuple_0 :::"`1"::: ) ) "is" ($#v1_finset_1 :::"finite"::: ) ) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "C1")) "st" (Bool (Bool (Set (Var "a")) ($#r1_tarski :::"c="::: ) (Set (Var "b")))) "holds" (Bool "for" (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "b")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) ")" ) & (Bool "(" "for" (Set (Var "a")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "C1")) (Bool "for" (Set (Var "y1")) "," (Set (Var "y2")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "y1")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "y2")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set ($#k2_tarski :::"{"::: ) (Set (Var "y1")) "," (Set (Var "y2")) ($#k2_tarski :::"}"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "C2")))) ")" )) "holds" (Bool "ex" (Set (Var "f")) "being" ($#v8_cohsp_1 :::"U-continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "C1")) "," (Set (Var "C2")) "st" (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set ($#k6_cohsp_1 :::"graph"::: ) (Set (Var "f"))))))) ; theorem :: COHSP_1:30 (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#m1_hidden :::"Coherence_Space":::) (Bool "for" (Set (Var "f")) "being" ($#v8_cohsp_1 :::"U-continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "C1")) "," (Set (Var "C2")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "C1")) "holds" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_cohsp_1 :::"graph"::: ) (Set (Var "f")) ")" ) ($#k7_relat_1 :::".:"::: ) (Set "(" ($#k3_cohsp_1 :::"Fin"::: ) (Set (Var "a")) ")" )))))) ; begin definitionlet "f" be ($#m1_hidden :::"Function":::); func :::"Trace"::: "f" -> ($#m1_hidden :::"set"::: ) means :: COHSP_1:def 17 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "ex" (Set (Var "a")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "f")) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set "f" ($#k1_funct_1 :::"."::: ) (Set (Var "a")))) & (Bool "(" "for" (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "f")) & (Bool (Set (Var "b")) ($#r1_tarski :::"c="::: ) (Set (Var "a"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set "f" ($#k1_funct_1 :::"."::: ) (Set (Var "b"))))) "holds" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b"))) ")" ) ")" )) ")" )); end; :: deftheorem defines :::"Trace"::: COHSP_1:def 17 : (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k7_cohsp_1 :::"Trace"::: ) (Set (Var "f")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) "iff" (Bool "ex" (Set (Var "a")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")))) & (Bool "(" "for" (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "b")) ($#r1_tarski :::"c="::: ) (Set (Var "a"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "b"))))) "holds" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b"))) ")" ) ")" )) ")" )) ")" ))); theorem :: COHSP_1:31 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "a")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k7_cohsp_1 :::"Trace"::: ) (Set (Var "f")))) "iff" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")))) & (Bool "(" "for" (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "b")) ($#r1_tarski :::"c="::: ) (Set (Var "a"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "b"))))) "holds" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b"))) ")" ) ")" ) ")" ))) ; definitionlet "C1", "C2" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "C1")) "," (Set (Const "C2")); :: original: :::"Trace"::: redefine func :::"Trace"::: "f" -> ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) "C1" "," (Set "(" ($#k3_tarski :::"union"::: ) "C2" ")" ) ($#k2_zfmisc_1 :::":]"::: ) ); end; registrationlet "f" be ($#m1_hidden :::"Function":::); cluster (Set ($#k7_cohsp_1 :::"Trace"::: ) "f") -> ($#v1_relat_1 :::"Relation-like"::: ) ; end; theorem :: COHSP_1:32 (Bool "for" (Set (Var "f")) "being" ($#v8_cohsp_1 :::"U-continuous"::: ) ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) "is" ($#v1_classes1 :::"subset-closed"::: ) )) "holds" (Bool (Set ($#k7_cohsp_1 :::"Trace"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set ($#k5_cohsp_1 :::"graph"::: ) (Set (Var "f"))))) ; theorem :: COHSP_1:33 (Bool "for" (Set (Var "f")) "being" ($#v8_cohsp_1 :::"U-continuous"::: ) ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) "is" ($#v1_classes1 :::"subset-closed"::: ) )) "holds" (Bool "for" (Set (Var "a")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k7_cohsp_1 :::"Trace"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Var "a")) "is" ($#v1_finset_1 :::"finite"::: ) ))) ; theorem :: COHSP_1:34 (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#m1_hidden :::"Coherence_Space":::) (Bool "for" (Set (Var "f")) "being" ($#v6_cohsp_1 :::"c=-monotone"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "C1")) "," (Set (Var "C2")) (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Set (Var "a1")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "a2"))) ($#r2_hidden :::"in"::: ) (Set (Var "C1")))) "holds" (Bool "for" (Set (Var "y1")) "," (Set (Var "y2")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "a1")) "," (Set (Var "y1")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k8_cohsp_1 :::"Trace"::: ) (Set (Var "f")))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "a2")) "," (Set (Var "y2")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k8_cohsp_1 :::"Trace"::: ) (Set (Var "f"))))) "holds" (Bool (Set ($#k2_tarski :::"{"::: ) (Set (Var "y1")) "," (Set (Var "y2")) ($#k2_tarski :::"}"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "C2"))))))) ; theorem :: COHSP_1:35 (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#m1_hidden :::"Coherence_Space":::) (Bool "for" (Set (Var "f")) "being" ($#v7_cohsp_1 :::"cap-distributive"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "C1")) "," (Set (Var "C2")) (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Set (Var "a1")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "a2"))) ($#r2_hidden :::"in"::: ) (Set (Var "C1")))) "holds" (Bool "for" (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "a1")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k8_cohsp_1 :::"Trace"::: ) (Set (Var "f")))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "a2")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k8_cohsp_1 :::"Trace"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Var "a1")) ($#r1_hidden :::"="::: ) (Set (Var "a2"))))))) ; theorem :: COHSP_1:36 (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#m1_hidden :::"Coherence_Space":::) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#v9_cohsp_1 :::"U-stable"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "C1")) "," (Set (Var "C2")) "st" (Bool (Bool (Set ($#k8_cohsp_1 :::"Trace"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set ($#k8_cohsp_1 :::"Trace"::: ) (Set (Var "g"))))) "holds" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "C1")) "holds" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "a"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "a"))))))) ; theorem :: COHSP_1:37 (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#m1_hidden :::"Coherence_Space":::) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#v9_cohsp_1 :::"U-stable"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "C1")) "," (Set (Var "C2")) "st" (Bool (Bool (Set ($#k8_cohsp_1 :::"Trace"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k8_cohsp_1 :::"Trace"::: ) (Set (Var "g"))))) "holds" (Bool (Set (Var "f")) ($#r2_funct_2 :::"="::: ) (Set (Var "g"))))) ; theorem :: COHSP_1:38 (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#m1_hidden :::"Coherence_Space":::) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "C1")) "," (Set "(" ($#k3_tarski :::"union"::: ) (Set (Var "C2")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Set (Var "x")) ($#k1_xtuple_0 :::"`1"::: ) ) "is" ($#v1_finset_1 :::"finite"::: ) ) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "C1")) "st" (Bool (Bool (Set (Set (Var "a")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "b"))) ($#r2_hidden :::"in"::: ) (Set (Var "C1")))) "holds" (Bool "for" (Set (Var "y1")) "," (Set (Var "y2")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "y1")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "b")) "," (Set (Var "y2")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set ($#k2_tarski :::"{"::: ) (Set (Var "y1")) "," (Set (Var "y2")) ($#k2_tarski :::"}"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "C2")))) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "C1")) "st" (Bool (Bool (Set (Set (Var "a")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "b"))) ($#r2_hidden :::"in"::: ) (Set (Var "C1")))) "holds" (Bool "for" (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "b")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b")))) ")" )) "holds" (Bool "ex" (Set (Var "f")) "being" ($#v9_cohsp_1 :::"U-stable"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "C1")) "," (Set (Var "C2")) "st" (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set ($#k8_cohsp_1 :::"Trace"::: ) (Set (Var "f"))))))) ; theorem :: COHSP_1:39 (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#m1_hidden :::"Coherence_Space":::) (Bool "for" (Set (Var "f")) "being" ($#v9_cohsp_1 :::"U-stable"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "C1")) "," (Set (Var "C2")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "C1")) "holds" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k8_cohsp_1 :::"Trace"::: ) (Set (Var "f")) ")" ) ($#k7_relat_1 :::".:"::: ) (Set "(" ($#k3_cohsp_1 :::"Fin"::: ) (Set (Var "a")) ")" )))))) ; theorem :: COHSP_1:40 (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#m1_hidden :::"Coherence_Space":::) (Bool "for" (Set (Var "f")) "being" ($#v9_cohsp_1 :::"U-stable"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "C1")) "," (Set (Var "C2")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "C1")) (Bool "for" (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "a")))) "iff" (Bool "ex" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "C1")) "st" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "b")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k8_cohsp_1 :::"Trace"::: ) (Set (Var "f")))) & (Bool (Set (Var "b")) ($#r1_tarski :::"c="::: ) (Set (Var "a"))) ")" )) ")" ))))) ; theorem :: COHSP_1:41 (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#m1_hidden :::"Coherence_Space":::) (Bool "ex" (Set (Var "f")) "being" ($#v9_cohsp_1 :::"U-stable"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "C1")) "," (Set (Var "C2")) "st" (Bool (Set ($#k8_cohsp_1 :::"Trace"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))) ; theorem :: COHSP_1:42 (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#m1_hidden :::"Coherence_Space":::) (Bool "for" (Set (Var "a")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "C1")) (Bool "for" (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k3_tarski :::"union"::: ) (Set (Var "C2"))))) "holds" (Bool "ex" (Set (Var "f")) "being" ($#v9_cohsp_1 :::"U-stable"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "C1")) "," (Set (Var "C2")) "st" (Bool (Set ($#k8_cohsp_1 :::"Trace"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#k1_tarski :::"}"::: ) )))))) ; theorem :: COHSP_1:43 (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#m1_hidden :::"Coherence_Space":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "C1")) (Bool "for" (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#v9_cohsp_1 :::"U-stable"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "C1")) "," (Set (Var "C2")) "st" (Bool (Bool (Set ($#k8_cohsp_1 :::"Trace"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#k1_tarski :::"}"::: ) ))) "holds" (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "C1")) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "a")) ($#r1_tarski :::"c="::: ) (Set (Var "b")))) "implies" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "y")) ($#k1_tarski :::"}"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "a")) ($#r1_tarski :::"c="::: ) (Set (Var "b"))))) "implies" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ")" )))))) ; theorem :: COHSP_1:44 (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#m1_hidden :::"Coherence_Space":::) (Bool "for" (Set (Var "f")) "being" ($#v9_cohsp_1 :::"U-stable"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "C1")) "," (Set (Var "C2")) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k8_cohsp_1 :::"Trace"::: ) (Set (Var "f")) ")" ) (Bool "ex" (Set (Var "g")) "being" ($#v9_cohsp_1 :::"U-stable"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "C1")) "," (Set (Var "C2")) "st" (Bool (Set ($#k8_cohsp_1 :::"Trace"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set (Var "X"))))))) ; theorem :: COHSP_1:45 (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#m1_hidden :::"Coherence_Space":::) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool "ex" (Set (Var "f")) "being" ($#v9_cohsp_1 :::"U-stable"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "C1")) "," (Set (Var "C2")) "st" (Bool (Set (Set (Var "x")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set ($#k8_cohsp_1 :::"Trace"::: ) (Set (Var "f"))))) ")" )) "holds" (Bool "ex" (Set (Var "f")) "being" ($#v9_cohsp_1 :::"U-stable"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "C1")) "," (Set (Var "C2")) "st" (Bool (Set ($#k3_tarski :::"union"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k8_cohsp_1 :::"Trace"::: ) (Set (Var "f"))))))) ; definitionlet "C1", "C2" be ($#m1_hidden :::"Coherence_Space":::); func :::"StabCoh"::: "(" "C1" "," "C2" ")" -> ($#m1_hidden :::"set"::: ) means :: COHSP_1:def 18 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "ex" (Set (Var "f")) "being" ($#v9_cohsp_1 :::"U-stable"::: ) ($#m1_subset_1 :::"Function":::) "of" "C1" "," "C2" "st" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k8_cohsp_1 :::"Trace"::: ) (Set (Var "f"))))) ")" )); end; :: deftheorem defines :::"StabCoh"::: COHSP_1:def 18 : (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#m1_hidden :::"Coherence_Space":::) (Bool "for" (Set (Var "b3")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k9_cohsp_1 :::"StabCoh"::: ) "(" (Set (Var "C1")) "," (Set (Var "C2")) ")" )) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b3"))) "iff" (Bool "ex" (Set (Var "f")) "being" ($#v9_cohsp_1 :::"U-stable"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "C1")) "," (Set (Var "C2")) "st" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k8_cohsp_1 :::"Trace"::: ) (Set (Var "f"))))) ")" )) ")" ))); registrationlet "C1", "C2" be ($#m1_hidden :::"Coherence_Space":::); cluster (Set ($#k9_cohsp_1 :::"StabCoh"::: ) "(" "C1" "," "C2" ")" ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_classes1 :::"subset-closed"::: ) ($#v1_coh_sp :::"binary_complete"::: ) ; end; theorem :: COHSP_1:46 (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#m1_hidden :::"Coherence_Space":::) (Bool "for" (Set (Var "f")) "being" ($#v9_cohsp_1 :::"U-stable"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "C1")) "," (Set (Var "C2")) "holds" (Bool (Set ($#k8_cohsp_1 :::"Trace"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k2_cohsp_1 :::"Sub_of_Fin"::: ) (Set (Var "C1")) ")" ) "," (Set "(" ($#k3_tarski :::"union"::: ) (Set (Var "C2")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) )))) ; theorem :: COHSP_1:47 (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#m1_hidden :::"Coherence_Space":::) "holds" (Bool (Set ($#k3_tarski :::"union"::: ) (Set "(" ($#k9_cohsp_1 :::"StabCoh"::: ) "(" (Set (Var "C1")) "," (Set (Var "C2")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k2_cohsp_1 :::"Sub_of_Fin"::: ) (Set (Var "C1")) ")" ) "," (Set "(" ($#k3_tarski :::"union"::: ) (Set (Var "C2")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ))) ; theorem :: COHSP_1:48 (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#m1_hidden :::"Coherence_Space":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "C1")) (Bool "for" (Set (Var "y1")) "," (Set (Var "y2")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "y1")) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set (Var "b")) "," (Set (Var "y2")) ($#k4_tarski :::"]"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_coh_sp :::"Web"::: ) (Set "(" ($#k9_cohsp_1 :::"StabCoh"::: ) "(" (Set (Var "C1")) "," (Set (Var "C2")) ")" ")" ))) "iff" (Bool "(" (Bool "(" (Bool (Bool "not" (Set (Set (Var "a")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "b"))) ($#r2_hidden :::"in"::: ) (Set (Var "C1")))) & (Bool (Set (Var "y1")) ($#r2_hidden :::"in"::: ) (Set ($#k3_tarski :::"union"::: ) (Set (Var "C2")))) & (Bool (Set (Var "y2")) ($#r2_hidden :::"in"::: ) (Set ($#k3_tarski :::"union"::: ) (Set (Var "C2")))) ")" ) "or" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "y1")) "," (Set (Var "y2")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_coh_sp :::"Web"::: ) (Set (Var "C2")))) & "(" (Bool (Bool (Set (Var "y1")) ($#r1_hidden :::"="::: ) (Set (Var "y2")))) "implies" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b"))) ")" ")" ) ")" ) ")" )))) ; begin theorem :: COHSP_1:49 (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#m1_hidden :::"Coherence_Space":::) (Bool "for" (Set (Var "f")) "being" ($#v9_cohsp_1 :::"U-stable"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "C1")) "," (Set (Var "C2")) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v10_cohsp_1 :::"U-linear"::: ) ) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k8_cohsp_1 :::"Trace"::: ) (Set (Var "f"))))) "holds" (Bool "ex" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )))) ")" ))) ; definitionlet "f" be ($#m1_hidden :::"Function":::); func :::"LinTrace"::: "f" -> ($#m1_hidden :::"set"::: ) means :: COHSP_1:def 19 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "ex" (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "z")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "y")) ($#k1_tarski :::"}"::: ) ) "," (Set (Var "z")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k7_cohsp_1 :::"Trace"::: ) "f")) ")" )) ")" )); end; :: deftheorem defines :::"LinTrace"::: COHSP_1:def 19 : (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k10_cohsp_1 :::"LinTrace"::: ) (Set (Var "f")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) "iff" (Bool "ex" (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "z")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "y")) ($#k1_tarski :::"}"::: ) ) "," (Set (Var "z")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k7_cohsp_1 :::"Trace"::: ) (Set (Var "f")))) ")" )) ")" )) ")" ))); theorem :: COHSP_1:50 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k10_cohsp_1 :::"LinTrace"::: ) (Set (Var "f")))) "iff" (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k7_cohsp_1 :::"Trace"::: ) (Set (Var "f")))) ")" ))) ; theorem :: COHSP_1:51 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )))) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k10_cohsp_1 :::"LinTrace"::: ) (Set (Var "f")))))) ; theorem :: COHSP_1:52 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k10_cohsp_1 :::"LinTrace"::: ) (Set (Var "f"))))) "holds" (Bool "(" (Bool (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ))) ")" ))) ; definitionlet "C1", "C2" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "C1")) "," (Set (Const "C2")); :: original: :::"LinTrace"::: redefine func :::"LinTrace"::: "f" -> ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k3_tarski :::"union"::: ) "C1" ")" ) "," (Set "(" ($#k3_tarski :::"union"::: ) "C2" ")" ) ($#k2_zfmisc_1 :::":]"::: ) ); end; registrationlet "f" be ($#m1_hidden :::"Function":::); cluster (Set ($#k10_cohsp_1 :::"LinTrace"::: ) "f") -> ($#v1_relat_1 :::"Relation-like"::: ) ; end; definitionlet "C1", "C2" be ($#m1_hidden :::"Coherence_Space":::); func :::"LinCoh"::: "(" "C1" "," "C2" ")" -> ($#m1_hidden :::"set"::: ) means :: COHSP_1:def 20 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "ex" (Set (Var "f")) "being" ($#v10_cohsp_1 :::"U-linear"::: ) ($#m1_subset_1 :::"Function":::) "of" "C1" "," "C2" "st" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k11_cohsp_1 :::"LinTrace"::: ) (Set (Var "f"))))) ")" )); end; :: deftheorem defines :::"LinCoh"::: COHSP_1:def 20 : (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#m1_hidden :::"Coherence_Space":::) (Bool "for" (Set (Var "b3")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k12_cohsp_1 :::"LinCoh"::: ) "(" (Set (Var "C1")) "," (Set (Var "C2")) ")" )) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b3"))) "iff" (Bool "ex" (Set (Var "f")) "being" ($#v10_cohsp_1 :::"U-linear"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "C1")) "," (Set (Var "C2")) "st" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k11_cohsp_1 :::"LinTrace"::: ) (Set (Var "f"))))) ")" )) ")" ))); theorem :: COHSP_1:53 (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#m1_hidden :::"Coherence_Space":::) (Bool "for" (Set (Var "f")) "being" ($#v6_cohsp_1 :::"c=-monotone"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "C1")) "," (Set (Var "C2")) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k2_tarski :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k2_tarski :::"}"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "C1")))) "holds" (Bool "for" (Set (Var "y1")) "," (Set (Var "y2")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x1")) "," (Set (Var "y1")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k11_cohsp_1 :::"LinTrace"::: ) (Set (Var "f")))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x2")) "," (Set (Var "y2")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k11_cohsp_1 :::"LinTrace"::: ) (Set (Var "f"))))) "holds" (Bool (Set ($#k2_tarski :::"{"::: ) (Set (Var "y1")) "," (Set (Var "y2")) ($#k2_tarski :::"}"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "C2"))))))) ; theorem :: COHSP_1:54 (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#m1_hidden :::"Coherence_Space":::) (Bool "for" (Set (Var "f")) "being" ($#v7_cohsp_1 :::"cap-distributive"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "C1")) "," (Set (Var "C2")) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k2_tarski :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k2_tarski :::"}"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "C1")))) "holds" (Bool "for" (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x1")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k11_cohsp_1 :::"LinTrace"::: ) (Set (Var "f")))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x2")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k11_cohsp_1 :::"LinTrace"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Var "x1")) ($#r1_hidden :::"="::: ) (Set (Var "x2"))))))) ; theorem :: COHSP_1:55 (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#m1_hidden :::"Coherence_Space":::) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#v10_cohsp_1 :::"U-linear"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "C1")) "," (Set (Var "C2")) "st" (Bool (Bool (Set ($#k11_cohsp_1 :::"LinTrace"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k11_cohsp_1 :::"LinTrace"::: ) (Set (Var "g"))))) "holds" (Bool (Set (Var "f")) ($#r2_funct_2 :::"="::: ) (Set (Var "g"))))) ; theorem :: COHSP_1:56 (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#m1_hidden :::"Coherence_Space":::) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k3_tarski :::"union"::: ) (Set (Var "C1")) ")" ) "," (Set "(" ($#k3_tarski :::"union"::: ) (Set (Var "C2")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k2_tarski :::"{"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_tarski :::"}"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "C1")))) "holds" (Bool "for" (Set (Var "y1")) "," (Set (Var "y2")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "y1")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "b")) "," (Set (Var "y2")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set ($#k2_tarski :::"{"::: ) (Set (Var "y1")) "," (Set (Var "y2")) ($#k2_tarski :::"}"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "C2")))) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k2_tarski :::"{"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_tarski :::"}"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "C1")))) "holds" (Bool "for" (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "b")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b")))) ")" )) "holds" (Bool "ex" (Set (Var "f")) "being" ($#v10_cohsp_1 :::"U-linear"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "C1")) "," (Set (Var "C2")) "st" (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set ($#k11_cohsp_1 :::"LinTrace"::: ) (Set (Var "f"))))))) ; theorem :: COHSP_1:57 (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#m1_hidden :::"Coherence_Space":::) (Bool "for" (Set (Var "f")) "being" ($#v10_cohsp_1 :::"U-linear"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "C1")) "," (Set (Var "C2")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "C1")) "holds" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k11_cohsp_1 :::"LinTrace"::: ) (Set (Var "f")) ")" ) ($#k7_relat_1 :::".:"::: ) (Set (Var "a"))))))) ; theorem :: COHSP_1:58 (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#m1_hidden :::"Coherence_Space":::) (Bool "ex" (Set (Var "f")) "being" ($#v10_cohsp_1 :::"U-linear"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "C1")) "," (Set (Var "C2")) "st" (Bool (Set ($#k11_cohsp_1 :::"LinTrace"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))) ; theorem :: COHSP_1:59 (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#m1_hidden :::"Coherence_Space":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k3_tarski :::"union"::: ) (Set (Var "C1")))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k3_tarski :::"union"::: ) (Set (Var "C2"))))) "holds" (Bool "ex" (Set (Var "f")) "being" ($#v10_cohsp_1 :::"U-linear"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "C1")) "," (Set (Var "C2")) "st" (Bool (Set ($#k11_cohsp_1 :::"LinTrace"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#k1_tarski :::"}"::: ) ))))) ; theorem :: COHSP_1:60 (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#m1_hidden :::"Coherence_Space":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k3_tarski :::"union"::: ) (Set (Var "C1"))))) "holds" (Bool "for" (Set (Var "f")) "being" ($#v10_cohsp_1 :::"U-linear"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "C1")) "," (Set (Var "C2")) "st" (Bool (Bool (Set ($#k11_cohsp_1 :::"LinTrace"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#k1_tarski :::"}"::: ) ))) "holds" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "C1")) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "a")))) "implies" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "y")) ($#k1_tarski :::"}"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "a"))))) "implies" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ")" ))))) ; theorem :: COHSP_1:61 (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#m1_hidden :::"Coherence_Space":::) (Bool "for" (Set (Var "f")) "being" ($#v10_cohsp_1 :::"U-linear"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "C1")) "," (Set (Var "C2")) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k11_cohsp_1 :::"LinTrace"::: ) (Set (Var "f")) ")" ) (Bool "ex" (Set (Var "g")) "being" ($#v10_cohsp_1 :::"U-linear"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "C1")) "," (Set (Var "C2")) "st" (Bool (Set ($#k11_cohsp_1 :::"LinTrace"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set (Var "X"))))))) ; theorem :: COHSP_1:62 (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#m1_hidden :::"Coherence_Space":::) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool "ex" (Set (Var "f")) "being" ($#v10_cohsp_1 :::"U-linear"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "C1")) "," (Set (Var "C2")) "st" (Bool (Set (Set (Var "x")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set ($#k11_cohsp_1 :::"LinTrace"::: ) (Set (Var "f"))))) ")" )) "holds" (Bool "ex" (Set (Var "f")) "being" ($#v10_cohsp_1 :::"U-linear"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "C1")) "," (Set (Var "C2")) "st" (Bool (Set ($#k3_tarski :::"union"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k11_cohsp_1 :::"LinTrace"::: ) (Set (Var "f"))))))) ; registrationlet "C1", "C2" be ($#m1_hidden :::"Coherence_Space":::); cluster (Set ($#k12_cohsp_1 :::"LinCoh"::: ) "(" "C1" "," "C2" ")" ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_classes1 :::"subset-closed"::: ) ($#v1_coh_sp :::"binary_complete"::: ) ; end; theorem :: COHSP_1:63 (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#m1_hidden :::"Coherence_Space":::) "holds" (Bool (Set ($#k3_tarski :::"union"::: ) (Set "(" ($#k12_cohsp_1 :::"LinCoh"::: ) "(" (Set (Var "C1")) "," (Set (Var "C2")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k3_tarski :::"union"::: ) (Set (Var "C1")) ")" ) "," (Set "(" ($#k3_tarski :::"union"::: ) (Set (Var "C2")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ))) ; theorem :: COHSP_1:64 (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#m1_hidden :::"Coherence_Space":::) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "y1")) "," (Set (Var "y2")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x1")) "," (Set (Var "y1")) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set (Var "x2")) "," (Set (Var "y2")) ($#k4_tarski :::"]"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_coh_sp :::"Web"::: ) (Set "(" ($#k12_cohsp_1 :::"LinCoh"::: ) "(" (Set (Var "C1")) "," (Set (Var "C2")) ")" ")" ))) "iff" (Bool "(" (Bool (Set (Var "x1")) ($#r2_hidden :::"in"::: ) (Set ($#k3_tarski :::"union"::: ) (Set (Var "C1")))) & (Bool (Set (Var "x2")) ($#r2_hidden :::"in"::: ) (Set ($#k3_tarski :::"union"::: ) (Set (Var "C1")))) & (Bool "(" (Bool "(" (Bool (Bool "not" (Set ($#k4_tarski :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_coh_sp :::"Web"::: ) (Set (Var "C1"))))) & (Bool (Set (Var "y1")) ($#r2_hidden :::"in"::: ) (Set ($#k3_tarski :::"union"::: ) (Set (Var "C2")))) & (Bool (Set (Var "y2")) ($#r2_hidden :::"in"::: ) (Set ($#k3_tarski :::"union"::: ) (Set (Var "C2")))) ")" ) "or" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "y1")) "," (Set (Var "y2")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_coh_sp :::"Web"::: ) (Set (Var "C2")))) & "(" (Bool (Bool (Set (Var "y1")) ($#r1_hidden :::"="::: ) (Set (Var "y2")))) "implies" (Bool (Set (Var "x1")) ($#r1_hidden :::"="::: ) (Set (Var "x2"))) ")" ")" ) ")" ) ")" ) ")" ))) ; begin definitionlet "C" be ($#m1_hidden :::"Coherence_Space":::); func :::"'not'"::: "C" -> ($#m1_hidden :::"set"::: ) equals :: COHSP_1:def 21 "{" (Set (Var "a")) where a "is" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_tarski :::"union"::: ) "C" ")" ) : (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "C" (Bool "ex" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Set (Set (Var "a")) ($#k8_subset_1 :::"/\"::: ) (Set (Var "b"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )))) "}" ; end; :: deftheorem defines :::"'not'"::: COHSP_1:def 21 : (Bool "for" (Set (Var "C")) "being" ($#m1_hidden :::"Coherence_Space":::) "holds" (Bool (Set ($#k13_cohsp_1 :::"'not'"::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "a")) where a "is" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_tarski :::"union"::: ) (Set (Var "C")) ")" ) : (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "C")) (Bool "ex" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Set (Set (Var "a")) ($#k8_subset_1 :::"/\"::: ) (Set (Var "b"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )))) "}" )); theorem :: COHSP_1:65 (Bool "for" (Set (Var "C")) "being" ($#m1_hidden :::"Coherence_Space":::) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k13_cohsp_1 :::"'not'"::: ) (Set (Var "C")))) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r1_tarski :::"c="::: ) (Set ($#k3_tarski :::"union"::: ) (Set (Var "C")))) & (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "C")) (Bool "ex" (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Set (Set (Var "x")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "a"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "z")) ($#k1_tarski :::"}"::: ) ))) ")" ) ")" ) ")" ))) ; registrationlet "C" be ($#m1_hidden :::"Coherence_Space":::); cluster (Set ($#k13_cohsp_1 :::"'not'"::: ) "C") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_classes1 :::"subset-closed"::: ) ($#v1_coh_sp :::"binary_complete"::: ) ; end; theorem :: COHSP_1:66 (Bool "for" (Set (Var "C")) "being" ($#m1_hidden :::"Coherence_Space":::) "holds" (Bool (Set ($#k3_tarski :::"union"::: ) (Set "(" ($#k13_cohsp_1 :::"'not'"::: ) (Set (Var "C")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) (Set (Var "C"))))) ; theorem :: COHSP_1:67 (Bool "for" (Set (Var "C")) "being" ($#m1_hidden :::"Coherence_Space":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y"))) & (Bool (Set ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "C")))) "holds" (Bool "not" (Bool (Set ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k13_cohsp_1 :::"'not'"::: ) (Set (Var "C"))))))) ; theorem :: COHSP_1:68 (Bool "for" (Set (Var "C")) "being" ($#m1_hidden :::"Coherence_Space":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) ) ($#r1_tarski :::"c="::: ) (Set ($#k3_tarski :::"union"::: ) (Set (Var "C")))) & (Bool (Bool "not" (Set ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "C"))))) "holds" (Bool (Set ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k13_cohsp_1 :::"'not'"::: ) (Set (Var "C")))))) ; theorem :: COHSP_1:69 (Bool "for" (Set (Var "C")) "being" ($#m1_hidden :::"Coherence_Space":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_coh_sp :::"Web"::: ) (Set "(" ($#k13_cohsp_1 :::"'not'"::: ) (Set (Var "C")) ")" ))) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k3_tarski :::"union"::: ) (Set (Var "C")))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k3_tarski :::"union"::: ) (Set (Var "C")))) & (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y"))) "or" "not" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_coh_sp :::"Web"::: ) (Set (Var "C")))) ")" ) ")" ) ")" ))) ; theorem :: COHSP_1:70 (Bool "for" (Set (Var "C")) "being" ($#m1_hidden :::"Coherence_Space":::) "holds" (Bool (Set ($#k13_cohsp_1 :::"'not'"::: ) (Set "(" ($#k13_cohsp_1 :::"'not'"::: ) (Set (Var "C")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "C")))) ; theorem :: COHSP_1:71 (Bool (Set ($#k13_cohsp_1 :::"'not'"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) )) ; theorem :: COHSP_1:72 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k13_cohsp_1 :::"'not'"::: ) (Set "(" ($#k1_cohsp_1 :::"FlatCoh"::: ) (Set (Var "X")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set (Var "X")))) & (Bool (Set ($#k13_cohsp_1 :::"'not'"::: ) (Set "(" ($#k1_zfmisc_1 :::"bool"::: ) (Set (Var "X")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_cohsp_1 :::"FlatCoh"::: ) (Set (Var "X")))) ")" )) ; begin definitionlet "x", "y" be ($#m1_hidden :::"set"::: ) ; func "x" :::"U+"::: "y" -> ($#m1_hidden :::"set"::: ) equals :: COHSP_1:def 22 (Set ($#k3_card_3 :::"Union"::: ) (Set "(" ($#k2_card_3 :::"disjoin"::: ) (Set ($#k10_finseq_1 :::"<*"::: ) "x" "," "y" ($#k10_finseq_1 :::"*>"::: ) ) ")" )); end; :: deftheorem defines :::"U+"::: COHSP_1:def 22 : (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "x")) ($#k14_cohsp_1 :::"U+"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set ($#k3_card_3 :::"Union"::: ) (Set "(" ($#k2_card_3 :::"disjoin"::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) ) ")" )))); theorem :: COHSP_1:73 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "x")) ($#k14_cohsp_1 :::"U+"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "x")) "," (Set ($#k1_tarski :::"{"::: ) (Num 1) ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "y")) "," (Set ($#k1_tarski :::"{"::: ) (Num 2) ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )))) ; theorem :: COHSP_1:74 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Set (Var "x")) ($#k14_cohsp_1 :::"U+"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "x")) "," (Set ($#k1_tarski :::"{"::: ) (Num 1) ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )) & (Bool (Set (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k14_cohsp_1 :::"U+"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "x")) "," (Set ($#k1_tarski :::"{"::: ) (Num 2) ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )) ")" )) ; theorem :: COHSP_1:75 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "x")) ($#k14_cohsp_1 :::"U+"::: ) (Set (Var "y"))))) "holds" (Bool "(" (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "z")) ($#k1_xtuple_0 :::"`1"::: ) ")" ) "," (Set "(" (Set (Var "z")) ($#k2_xtuple_0 :::"`2"::: ) ")" ) ($#k4_tarski :::"]"::: ) )) & (Bool "(" (Bool "(" (Bool (Set (Set (Var "z")) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Set (Var "z")) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "x"))) ")" ) "or" (Bool "(" (Bool (Set (Set (Var "z")) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Num 2)) & (Bool (Set (Set (Var "z")) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "y"))) ")" ) ")" ) ")" )) ; theorem :: COHSP_1:76 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "z")) "," (Num 1) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Set (Var "x")) ($#k14_cohsp_1 :::"U+"::: ) (Set (Var "y")))) "iff" (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set (Var "x"))) ")" )) ; theorem :: COHSP_1:77 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "z")) "," (Num 2) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Set (Var "x")) ($#k14_cohsp_1 :::"U+"::: ) (Set (Var "y")))) "iff" (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set (Var "y"))) ")" )) ; theorem :: COHSP_1:78 (Bool "for" (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "x2")) "," (Set (Var "y2")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Set (Var "x1")) ($#k14_cohsp_1 :::"U+"::: ) (Set (Var "y1"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "x2")) ($#k14_cohsp_1 :::"U+"::: ) (Set (Var "y2")))) "iff" (Bool "(" (Bool (Set (Var "x1")) ($#r1_tarski :::"c="::: ) (Set (Var "x2"))) & (Bool (Set (Var "y1")) ($#r1_tarski :::"c="::: ) (Set (Var "y2"))) ")" ) ")" )) ; theorem :: COHSP_1:79 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "z")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "x")) ($#k14_cohsp_1 :::"U+"::: ) (Set (Var "y"))))) "holds" (Bool "ex" (Set (Var "x1")) "," (Set (Var "y1")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x1")) ($#k14_cohsp_1 :::"U+"::: ) (Set (Var "y1")))) & (Bool (Set (Var "x1")) ($#r1_tarski :::"c="::: ) (Set (Var "x"))) & (Bool (Set (Var "y1")) ($#r1_tarski :::"c="::: ) (Set (Var "y"))) ")" ))) ; theorem :: COHSP_1:80 (Bool "for" (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "x2")) "," (Set (Var "y2")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Set (Var "x1")) ($#k14_cohsp_1 :::"U+"::: ) (Set (Var "y1"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x2")) ($#k14_cohsp_1 :::"U+"::: ) (Set (Var "y2")))) "iff" (Bool "(" (Bool (Set (Var "x1")) ($#r1_hidden :::"="::: ) (Set (Var "x2"))) & (Bool (Set (Var "y1")) ($#r1_hidden :::"="::: ) (Set (Var "y2"))) ")" ) ")" )) ; theorem :: COHSP_1:81 (Bool "for" (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "x2")) "," (Set (Var "y2")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set "(" (Set (Var "x1")) ($#k14_cohsp_1 :::"U+"::: ) (Set (Var "y1")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" (Set (Var "x2")) ($#k14_cohsp_1 :::"U+"::: ) (Set (Var "y2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x1")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "x2")) ")" ) ($#k14_cohsp_1 :::"U+"::: ) (Set "(" (Set (Var "y1")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "y2")) ")" )))) ; theorem :: COHSP_1:82 (Bool "for" (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "x2")) "," (Set (Var "y2")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set "(" (Set (Var "x1")) ($#k14_cohsp_1 :::"U+"::: ) (Set (Var "y1")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" (Set (Var "x2")) ($#k14_cohsp_1 :::"U+"::: ) (Set (Var "y2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x1")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "x2")) ")" ) ($#k14_cohsp_1 :::"U+"::: ) (Set "(" (Set (Var "y1")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "y2")) ")" )))) ; definitionlet "C1", "C2" be ($#m1_hidden :::"Coherence_Space":::); func "C1" :::""/\""::: "C2" -> ($#m1_hidden :::"set"::: ) equals :: COHSP_1:def 23 "{" (Set "(" (Set (Var "a")) ($#k14_cohsp_1 :::"U+"::: ) (Set (Var "b")) ")" ) where a "is" ($#m1_subset_1 :::"Element"::: ) "of" "C1", b "is" ($#m1_subset_1 :::"Element"::: ) "of" "C2" : (Bool verum) "}" ; func "C1" :::""\/""::: "C2" -> ($#m1_hidden :::"set"::: ) equals :: COHSP_1:def 24 (Set "{" (Set "(" (Set (Var "a")) ($#k14_cohsp_1 :::"U+"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ) where a "is" ($#m1_subset_1 :::"Element"::: ) "of" "C1" : (Bool verum) "}" ($#k2_xboole_0 :::"\/"::: ) "{" (Set "(" (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k14_cohsp_1 :::"U+"::: ) (Set (Var "b")) ")" ) where b "is" ($#m1_subset_1 :::"Element"::: ) "of" "C2" : (Bool verum) "}" ); end; :: deftheorem defines :::""/\""::: COHSP_1:def 23 : (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#m1_hidden :::"Coherence_Space":::) "holds" (Bool (Set (Set (Var "C1")) ($#k15_cohsp_1 :::""/\""::: ) (Set (Var "C2"))) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set (Var "a")) ($#k14_cohsp_1 :::"U+"::: ) (Set (Var "b")) ")" ) where a "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "C1")), b "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "C2")) : (Bool verum) "}" )); :: deftheorem defines :::""\/""::: COHSP_1:def 24 : (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#m1_hidden :::"Coherence_Space":::) "holds" (Bool (Set (Set (Var "C1")) ($#k16_cohsp_1 :::""\/""::: ) (Set (Var "C2"))) ($#r1_hidden :::"="::: ) (Set "{" (Set "(" (Set (Var "a")) ($#k14_cohsp_1 :::"U+"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ) where a "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "C1")) : (Bool verum) "}" ($#k2_xboole_0 :::"\/"::: ) "{" (Set "(" (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k14_cohsp_1 :::"U+"::: ) (Set (Var "b")) ")" ) where b "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "C2")) : (Bool verum) "}" ))); theorem :: COHSP_1:83 (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#m1_hidden :::"Coherence_Space":::) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "C1")) ($#k15_cohsp_1 :::""/\""::: ) (Set (Var "C2")))) "iff" (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "C1"))(Bool "ex" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "C2")) "st" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k14_cohsp_1 :::"U+"::: ) (Set (Var "b")))))) ")" ))) ; theorem :: COHSP_1:84 (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#m1_hidden :::"Coherence_Space":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Set (Var "x")) ($#k14_cohsp_1 :::"U+"::: ) (Set (Var "y"))) ($#r2_hidden :::"in"::: ) (Set (Set (Var "C1")) ($#k15_cohsp_1 :::""/\""::: ) (Set (Var "C2")))) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "C1"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "C2"))) ")" ) ")" ))) ; theorem :: COHSP_1:85 (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#m1_hidden :::"Coherence_Space":::) "holds" (Bool (Set ($#k3_tarski :::"union"::: ) (Set "(" (Set (Var "C1")) ($#k15_cohsp_1 :::""/\""::: ) (Set (Var "C2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_tarski :::"union"::: ) (Set (Var "C1")) ")" ) ($#k14_cohsp_1 :::"U+"::: ) (Set "(" ($#k3_tarski :::"union"::: ) (Set (Var "C2")) ")" )))) ; theorem :: COHSP_1:86 (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#m1_hidden :::"Coherence_Space":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Set (Var "x")) ($#k14_cohsp_1 :::"U+"::: ) (Set (Var "y"))) ($#r2_hidden :::"in"::: ) (Set (Set (Var "C1")) ($#k16_cohsp_1 :::""\/""::: ) (Set (Var "C2")))) "iff" (Bool "(" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "C1"))) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ) "or" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "C2"))) ")" ) ")" ) ")" ))) ; theorem :: COHSP_1:87 (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#m1_hidden :::"Coherence_Space":::) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "C1")) ($#k16_cohsp_1 :::""\/""::: ) (Set (Var "C2"))))) "holds" (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "C1"))(Bool "ex" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "C2")) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k14_cohsp_1 :::"U+"::: ) (Set (Var "b")))) & (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) "or" (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ) ")" ))))) ; theorem :: COHSP_1:88 (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#m1_hidden :::"Coherence_Space":::) "holds" (Bool (Set ($#k3_tarski :::"union"::: ) (Set "(" (Set (Var "C1")) ($#k16_cohsp_1 :::""\/""::: ) (Set (Var "C2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_tarski :::"union"::: ) (Set (Var "C1")) ")" ) ($#k14_cohsp_1 :::"U+"::: ) (Set "(" ($#k3_tarski :::"union"::: ) (Set (Var "C2")) ")" )))) ; registrationlet "C1", "C2" be ($#m1_hidden :::"Coherence_Space":::); cluster (Set "C1" ($#k15_cohsp_1 :::""/\""::: ) "C2") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_classes1 :::"subset-closed"::: ) ($#v1_coh_sp :::"binary_complete"::: ) ; cluster (Set "C1" ($#k16_cohsp_1 :::""\/""::: ) "C2") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_classes1 :::"subset-closed"::: ) ($#v1_coh_sp :::"binary_complete"::: ) ; end; theorem :: COHSP_1:89 (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#m1_hidden :::"Coherence_Space":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Num 1) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Num 1) ($#k4_tarski :::"]"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_coh_sp :::"Web"::: ) (Set "(" (Set (Var "C1")) ($#k15_cohsp_1 :::""/\""::: ) (Set (Var "C2")) ")" ))) "iff" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_coh_sp :::"Web"::: ) (Set (Var "C1")))) ")" ))) ; theorem :: COHSP_1:90 (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#m1_hidden :::"Coherence_Space":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Num 2) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Num 2) ($#k4_tarski :::"]"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_coh_sp :::"Web"::: ) (Set "(" (Set (Var "C1")) ($#k15_cohsp_1 :::""/\""::: ) (Set (Var "C2")) ")" ))) "iff" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_coh_sp :::"Web"::: ) (Set (Var "C2")))) ")" ))) ; theorem :: COHSP_1:91 (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#m1_hidden :::"Coherence_Space":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k3_tarski :::"union"::: ) (Set (Var "C1")))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k3_tarski :::"union"::: ) (Set (Var "C2"))))) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Num 1) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Num 2) ($#k4_tarski :::"]"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_coh_sp :::"Web"::: ) (Set "(" (Set (Var "C1")) ($#k15_cohsp_1 :::""/\""::: ) (Set (Var "C2")) ")" ))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Num 2) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Num 1) ($#k4_tarski :::"]"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_coh_sp :::"Web"::: ) (Set "(" (Set (Var "C1")) ($#k15_cohsp_1 :::""/\""::: ) (Set (Var "C2")) ")" ))) ")" ))) ; theorem :: COHSP_1:92 (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#m1_hidden :::"Coherence_Space":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Num 1) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Num 1) ($#k4_tarski :::"]"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_coh_sp :::"Web"::: ) (Set "(" (Set (Var "C1")) ($#k16_cohsp_1 :::""\/""::: ) (Set (Var "C2")) ")" ))) "iff" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_coh_sp :::"Web"::: ) (Set (Var "C1")))) ")" ))) ; theorem :: COHSP_1:93 (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#m1_hidden :::"Coherence_Space":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Num 2) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Num 2) ($#k4_tarski :::"]"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_coh_sp :::"Web"::: ) (Set "(" (Set (Var "C1")) ($#k16_cohsp_1 :::""\/""::: ) (Set (Var "C2")) ")" ))) "iff" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_coh_sp :::"Web"::: ) (Set (Var "C2")))) ")" ))) ; theorem :: COHSP_1:94 (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#m1_hidden :::"Coherence_Space":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Bool "not" (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Num 1) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Num 2) ($#k4_tarski :::"]"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_coh_sp :::"Web"::: ) (Set "(" (Set (Var "C1")) ($#k16_cohsp_1 :::""\/""::: ) (Set (Var "C2")) ")" )))) & (Bool (Bool "not" (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Num 2) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Num 1) ($#k4_tarski :::"]"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_coh_sp :::"Web"::: ) (Set "(" (Set (Var "C1")) ($#k16_cohsp_1 :::""\/""::: ) (Set (Var "C2")) ")" )))) ")" ))) ; theorem :: COHSP_1:95 (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#m1_hidden :::"Coherence_Space":::) "holds" (Bool (Set ($#k13_cohsp_1 :::"'not'"::: ) (Set "(" (Set (Var "C1")) ($#k15_cohsp_1 :::""/\""::: ) (Set (Var "C2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k13_cohsp_1 :::"'not'"::: ) (Set (Var "C1")) ")" ) ($#k16_cohsp_1 :::""\/""::: ) (Set "(" ($#k13_cohsp_1 :::"'not'"::: ) (Set (Var "C2")) ")" )))) ; definitionlet "C1", "C2" be ($#m1_hidden :::"Coherence_Space":::); func "C1" :::"[*]"::: "C2" -> ($#m1_hidden :::"set"::: ) equals :: COHSP_1:def 25 (Set ($#k3_tarski :::"union"::: ) "{" (Set "(" ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_zfmisc_1 :::":]"::: ) ) ")" ) where a "is" ($#m1_subset_1 :::"Element"::: ) "of" "C1", b "is" ($#m1_subset_1 :::"Element"::: ) "of" "C2" : (Bool verum) "}" ); end; :: deftheorem defines :::"[*]"::: COHSP_1:def 25 : (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#m1_hidden :::"Coherence_Space":::) "holds" (Bool (Set (Set (Var "C1")) ($#k17_cohsp_1 :::"[*]"::: ) (Set (Var "C2"))) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) "{" (Set "(" ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_zfmisc_1 :::":]"::: ) ) ")" ) where a "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "C1")), b "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "C2")) : (Bool verum) "}" ))); theorem :: COHSP_1:96 (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#m1_hidden :::"Coherence_Space":::) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "C1")) ($#k17_cohsp_1 :::"[*]"::: ) (Set (Var "C2")))) "iff" (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "C1"))(Bool "ex" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "C2")) "st" (Bool (Set (Var "x")) ($#r1_tarski :::"c="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_zfmisc_1 :::":]"::: ) )))) ")" ))) ; registrationlet "C1", "C2" be ($#m1_hidden :::"Coherence_Space":::); cluster (Set "C1" ($#k17_cohsp_1 :::"[*]"::: ) "C2") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; theorem :: COHSP_1:97 (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#m1_hidden :::"Coherence_Space":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "C1")) ($#k17_cohsp_1 :::"[*]"::: ) (Set (Var "C2"))) "holds" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"proj1"::: ) (Set (Var "a"))) ($#r2_hidden :::"in"::: ) (Set (Var "C1"))) & (Bool (Set ($#k10_xtuple_0 :::"proj2"::: ) (Set (Var "a"))) ($#r2_hidden :::"in"::: ) (Set (Var "C2"))) & (Bool (Set (Var "a")) ($#r1_tarski :::"c="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k9_xtuple_0 :::"proj1"::: ) (Set (Var "a")) ")" ) "," (Set "(" ($#k10_xtuple_0 :::"proj2"::: ) (Set (Var "a")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) )) ")" ))) ; registrationlet "C1", "C2" be ($#m1_hidden :::"Coherence_Space":::); cluster (Set "C1" ($#k17_cohsp_1 :::"[*]"::: ) "C2") -> ($#v1_classes1 :::"subset-closed"::: ) ($#v1_coh_sp :::"binary_complete"::: ) ; end; theorem :: COHSP_1:98 (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#m1_hidden :::"Coherence_Space":::) "holds" (Bool (Set ($#k3_tarski :::"union"::: ) (Set "(" (Set (Var "C1")) ($#k17_cohsp_1 :::"[*]"::: ) (Set (Var "C2")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k3_tarski :::"union"::: ) (Set (Var "C1")) ")" ) "," (Set "(" ($#k3_tarski :::"union"::: ) (Set (Var "C2")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ))) ; theorem :: COHSP_1:99 (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#m1_hidden :::"Coherence_Space":::) (Bool "for" (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "x2")) "," (Set (Var "y2")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set (Var "y1")) "," (Set (Var "y2")) ($#k4_tarski :::"]"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_coh_sp :::"Web"::: ) (Set "(" (Set (Var "C1")) ($#k17_cohsp_1 :::"[*]"::: ) (Set (Var "C2")) ")" ))) "iff" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x1")) "," (Set (Var "y1")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_coh_sp :::"Web"::: ) (Set (Var "C1")))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x2")) "," (Set (Var "y2")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_coh_sp :::"Web"::: ) (Set (Var "C2")))) ")" ) ")" ))) ;