:: COH_SP semantic presentation begin definitionlet "IT" be ($#m1_hidden :::"set"::: ) ; attr "IT" is :::"binary_complete"::: means :: COH_SP:def 1 (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) "IT") & (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"::: ) "IT") ")" )) "holds" (Bool (Set ($#k3_tarski :::"union"::: ) (Set (Var "A"))) ($#r2_hidden :::"in"::: ) "IT")); end; :: deftheorem defines :::"binary_complete"::: COH_SP:def 1 : (Bool "for" (Set (Var "IT")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v1_coh_sp :::"binary_complete"::: ) ) "iff" (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "IT"))) & (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 "IT"))) ")" )) "holds" (Bool (Set ($#k3_tarski :::"union"::: ) (Set (Var "A"))) ($#r2_hidden :::"in"::: ) (Set (Var "IT")))) ")" )); registration cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_classes1 :::"subset-closed"::: ) ($#v1_coh_sp :::"binary_complete"::: ) for ($#m1_hidden :::"set"::: ) ; end; definitionmode Coherence_Space is ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_classes1 :::"subset-closed"::: ) ($#v1_coh_sp :::"binary_complete"::: ) ($#m1_hidden :::"set"::: ) ; end; theorem :: COH_SP:1 (Bool "for" (Set (Var "C")) "being" ($#m1_hidden :::"Coherence_Space":::) "holds" (Bool (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "C")))) ; theorem :: COH_SP:2 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k9_setfam_1 :::"bool"::: ) (Set (Var "X"))) "is" ($#m1_hidden :::"Coherence_Space":::))) ; theorem :: COH_SP:3 (Bool (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) ) "is" ($#m1_hidden :::"Coherence_Space":::)) ; theorem :: COH_SP:4 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#m1_hidden :::"Coherence_Space":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k3_tarski :::"union"::: ) (Set (Var "C"))))) "holds" (Bool (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "C"))))) ; definitionlet "C" be ($#m1_hidden :::"Coherence_Space":::); func :::"Web"::: "C" -> ($#m1_subset_1 :::"Tolerance":::) "of" (Set "(" ($#k3_tarski :::"union"::: ) "C" ")" ) means :: COH_SP:def 2 (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"::: ) it) "iff" (Bool "ex" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) "C") & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) ")" )) ")" )); end; :: deftheorem defines :::"Web"::: COH_SP:def 2 : (Bool "for" (Set (Var "C")) "being" ($#m1_hidden :::"Coherence_Space":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Tolerance":::) "of" (Set "(" ($#k3_tarski :::"union"::: ) (Set (Var "C")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k1_coh_sp :::"Web"::: ) (Set (Var "C")))) "iff" (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 (Var "b2"))) "iff" (Bool "ex" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set (Var "C"))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) ")" )) ")" )) ")" ))); theorem :: COH_SP:5 (Bool "for" (Set (Var "C")) "being" ($#m1_hidden :::"Coherence_Space":::) (Bool "for" (Set (Var "T")) "being" ($#m1_subset_1 :::"Tolerance":::) "of" (Set "(" ($#k3_tarski :::"union"::: ) (Set (Var "C")) ")" ) "holds" (Bool "(" (Bool (Set (Var "T")) ($#r2_relset_1 :::"="::: ) (Set ($#k1_coh_sp :::"Web"::: ) (Set (Var "C")))) "iff" (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 (Var "T"))) "iff" (Bool (Set ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "C"))) ")" )) ")" ))) ; theorem :: COH_SP:6 (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#m1_hidden :::"Coherence_Space":::) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "C"))) "iff" (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 (Set ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "C")))) ")" ))) ; theorem :: COH_SP:7 (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#m1_hidden :::"Coherence_Space":::) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "C"))) "iff" (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 (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_coh_sp :::"Web"::: ) (Set (Var "C"))))) ")" ))) ; theorem :: COH_SP:8 (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#m1_hidden :::"Coherence_Space":::) "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 (Set ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "C"))) ")" )) "holds" (Bool (Set (Var "a")) ($#r1_tarski :::"c="::: ) (Set ($#k3_tarski :::"union"::: ) (Set (Var "C")))))) ; theorem :: COH_SP:9 (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "being" ($#m1_hidden :::"Coherence_Space":::) "st" (Bool (Bool (Set ($#k1_coh_sp :::"Web"::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set ($#k1_coh_sp :::"Web"::: ) (Set (Var "D"))))) "holds" (Bool (Set (Var "C")) ($#r1_hidden :::"="::: ) (Set (Var "D")))) ; theorem :: COH_SP:10 (Bool "for" (Set (Var "C")) "being" ($#m1_hidden :::"Coherence_Space":::) "st" (Bool (Bool (Set ($#k3_tarski :::"union"::: ) (Set (Var "C"))) ($#r2_hidden :::"in"::: ) (Set (Var "C")))) "holds" (Bool (Set (Var "C")) ($#r1_hidden :::"="::: ) (Set ($#k9_setfam_1 :::"bool"::: ) (Set "(" ($#k3_tarski :::"union"::: ) (Set (Var "C")) ")" )))) ; theorem :: COH_SP:11 (Bool "for" (Set (Var "C")) "being" ($#m1_hidden :::"Coherence_Space":::) "st" (Bool (Bool (Set (Var "C")) ($#r1_hidden :::"="::: ) (Set ($#k9_setfam_1 :::"bool"::: ) (Set "(" ($#k3_tarski :::"union"::: ) (Set (Var "C")) ")" )))) "holds" (Bool (Set ($#k1_coh_sp :::"Web"::: ) (Set (Var "C"))) ($#r2_relset_1 :::"="::: ) (Set ($#k1_eqrel_1 :::"Total"::: ) (Set "(" ($#k3_tarski :::"union"::: ) (Set (Var "C")) ")" )))) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "E" be ($#m1_subset_1 :::"Tolerance":::) "of" (Set (Const "X")); func :::"CohSp"::: "E" -> ($#m1_hidden :::"Coherence_Space":::) means :: COH_SP:def 3 (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) it) "iff" (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 (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "E")) ")" )); end; :: deftheorem defines :::"CohSp"::: COH_SP:def 3 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "E")) "being" ($#m1_subset_1 :::"Tolerance":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "b3")) "being" ($#m1_hidden :::"Coherence_Space":::) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k2_coh_sp :::"CohSp"::: ) (Set (Var "E")))) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "b3"))) "iff" (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 (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "E")))) ")" )) ")" )))); theorem :: COH_SP:12 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "E")) "being" ($#m1_subset_1 :::"Tolerance":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k1_coh_sp :::"Web"::: ) (Set "(" ($#k2_coh_sp :::"CohSp"::: ) (Set (Var "E")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "E"))))) ; theorem :: COH_SP:13 (Bool "for" (Set (Var "C")) "being" ($#m1_hidden :::"Coherence_Space":::) "holds" (Bool (Set ($#k2_coh_sp :::"CohSp"::: ) (Set "(" ($#k1_coh_sp :::"Web"::: ) (Set (Var "C")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "C")))) ; theorem :: COH_SP:14 (Bool "for" (Set (Var "X")) "," (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "E")) "being" ($#m1_subset_1 :::"Tolerance":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k2_coh_sp :::"CohSp"::: ) (Set (Var "E")))) "iff" (Bool (Set (Var "a")) "is" ($#m1_toler_1 :::"TolSet"::: ) "of" (Set (Var "E"))) ")" ))) ; theorem :: COH_SP:15 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "E")) "being" ($#m1_subset_1 :::"Tolerance":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k2_coh_sp :::"CohSp"::: ) (Set (Var "E"))) ($#r1_hidden :::"="::: ) (Set ($#k3_toler_1 :::"TolSets"::: ) (Set (Var "E")))))) ; begin definitionlet "X" be ($#m1_hidden :::"set"::: ) ; func :::"CSp"::: "X" -> ($#m1_hidden :::"set"::: ) equals :: COH_SP:def 4 "{" (Set (Var "x")) where x "is" ($#m1_subset_1 :::"Subset-Family":::) "of" "X" : (Bool (Set (Var "x")) "is" ($#m1_hidden :::"Coherence_Space":::)) "}" ; end; :: deftheorem defines :::"CSp"::: COH_SP:def 4 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k3_coh_sp :::"CSp"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "x")) where x "is" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) : (Bool (Set (Var "x")) "is" ($#m1_hidden :::"Coherence_Space":::)) "}" )); registrationlet "X" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k3_coh_sp :::"CSp"::: ) "X") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; cluster -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_classes1 :::"subset-closed"::: ) ($#v1_coh_sp :::"binary_complete"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_coh_sp :::"CSp"::: ) "X"); end; theorem :: COH_SP:16 (Bool "for" (Set (Var "X")) "," (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_coh_sp :::"CSp"::: ) (Set (Var "X"))) "st" (Bool (Bool (Set ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "C")))) "holds" (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")))) ")" ))) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; func :::"FuncsC"::: "X" -> ($#m1_hidden :::"set"::: ) equals :: COH_SP:def 5 (Set ($#k3_tarski :::"union"::: ) "{" (Set "(" ($#k1_funct_2 :::"Funcs"::: ) "(" (Set "(" ($#k3_tarski :::"union"::: ) (Set (Var "x")) ")" ) "," (Set "(" ($#k3_tarski :::"union"::: ) (Set (Var "y")) ")" ) ")" ")" ) where x, y "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_coh_sp :::"CSp"::: ) "X") : (Bool verum) "}" ); end; :: deftheorem defines :::"FuncsC"::: COH_SP:def 5 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k4_coh_sp :::"FuncsC"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) "{" (Set "(" ($#k1_funct_2 :::"Funcs"::: ) "(" (Set "(" ($#k3_tarski :::"union"::: ) (Set (Var "x")) ")" ) "," (Set "(" ($#k3_tarski :::"union"::: ) (Set (Var "y")) ")" ) ")" ")" ) where x, y "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_coh_sp :::"CSp"::: ) (Set (Var "X"))) : (Bool verum) "}" ))); registrationlet "X" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k4_coh_sp :::"FuncsC"::: ) "X") -> ($#v4_funct_1 :::"functional"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; theorem :: COH_SP:17 (Bool "for" (Set (Var "x")) "," (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k4_coh_sp :::"FuncsC"::: ) (Set (Var "X")))) "iff" (Bool "ex" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_coh_sp :::"CSp"::: ) (Set (Var "X"))) "st" (Bool "(" "(" (Bool (Bool (Set ($#k3_tarski :::"union"::: ) (Set (Var "C2"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "implies" (Bool (Set ($#k3_tarski :::"union"::: ) (Set (Var "C1"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" & (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k3_tarski :::"union"::: ) (Set (Var "C1")) ")" ) "," (Set "(" ($#k3_tarski :::"union"::: ) (Set (Var "C2")) ")" )) ")" )) ")" )) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; func :::"MapsC"::: "X" -> ($#m1_hidden :::"set"::: ) equals :: COH_SP:def 6 "{" (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "C")) "," (Set (Var "CC")) ($#k4_tarski :::"]"::: ) ) "," (Set (Var "f")) ($#k4_tarski :::"]"::: ) ) where C, CC "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_coh_sp :::"CSp"::: ) "X"), f "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_coh_sp :::"FuncsC"::: ) "X") : (Bool "(" "(" (Bool (Bool (Set ($#k3_tarski :::"union"::: ) (Set (Var "CC"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "implies" (Bool (Set ($#k3_tarski :::"union"::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" & (Bool (Set (Var "f")) "is" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k3_tarski :::"union"::: ) (Set (Var "C")) ")" ) "," (Set "(" ($#k3_tarski :::"union"::: ) (Set (Var "CC")) ")" )) & (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 :::"}"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "C")))) "holds" (Bool (Set ($#k2_tarski :::"{"::: ) (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) "," (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "y")) ")" ) ($#k2_tarski :::"}"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "CC"))) ")" ) ")" ) "}" ; end; :: deftheorem defines :::"MapsC"::: COH_SP:def 6 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k5_coh_sp :::"MapsC"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) "{" (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "C")) "," (Set (Var "CC")) ($#k4_tarski :::"]"::: ) ) "," (Set (Var "f")) ($#k4_tarski :::"]"::: ) ) where C, CC "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_coh_sp :::"CSp"::: ) (Set (Var "X"))), f "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_coh_sp :::"FuncsC"::: ) (Set (Var "X"))) : (Bool "(" "(" (Bool (Bool (Set ($#k3_tarski :::"union"::: ) (Set (Var "CC"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "implies" (Bool (Set ($#k3_tarski :::"union"::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" & (Bool (Set (Var "f")) "is" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k3_tarski :::"union"::: ) (Set (Var "C")) ")" ) "," (Set "(" ($#k3_tarski :::"union"::: ) (Set (Var "CC")) ")" )) & (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 :::"}"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "C")))) "holds" (Bool (Set ($#k2_tarski :::"{"::: ) (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) "," (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "y")) ")" ) ($#k2_tarski :::"}"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "CC"))) ")" ) ")" ) "}" )); registrationlet "X" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k5_coh_sp :::"MapsC"::: ) "X") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; theorem :: COH_SP:18 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "l")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_coh_sp :::"MapsC"::: ) (Set (Var "X"))) (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_coh_sp :::"FuncsC"::: ) (Set (Var "X")))(Bool "ex" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_coh_sp :::"CSp"::: ) (Set (Var "X"))) "st" (Bool "(" (Bool (Set (Var "l")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "C1")) "," (Set (Var "C2")) ($#k4_tarski :::"]"::: ) ) "," (Set (Var "g")) ($#k4_tarski :::"]"::: ) )) & "(" (Bool (Bool (Set ($#k3_tarski :::"union"::: ) (Set (Var "C2"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "implies" (Bool (Set ($#k3_tarski :::"union"::: ) (Set (Var "C1"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" & (Bool (Set (Var "g")) "is" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k3_tarski :::"union"::: ) (Set (Var "C1")) ")" ) "," (Set "(" ($#k3_tarski :::"union"::: ) (Set (Var "C2")) ")" )) & (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 :::"}"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "C1")))) "holds" (Bool (Set ($#k2_tarski :::"{"::: ) (Set "(" (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) "," (Set "(" (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "y")) ")" ) ($#k2_tarski :::"}"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "C2"))) ")" ) ")" ))))) ; theorem :: COH_SP:19 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_coh_sp :::"CSp"::: ) (Set (Var "X"))) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k3_tarski :::"union"::: ) (Set (Var "C1")) ")" ) "," (Set "(" ($#k3_tarski :::"union"::: ) (Set (Var "C2")) ")" ) "st" (Bool "(" (Bool (Bool (Set ($#k3_tarski :::"union"::: ) (Set (Var "C2"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "implies" (Bool (Set ($#k3_tarski :::"union"::: ) (Set (Var "C1"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" & (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 :::"}"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "C1")))) "holds" (Bool (Set ($#k2_tarski :::"{"::: ) (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) "," (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "y")) ")" ) ($#k2_tarski :::"}"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "C2"))) ")" )) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "C1")) "," (Set (Var "C2")) ($#k4_tarski :::"]"::: ) ) "," (Set (Var "f")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k5_coh_sp :::"MapsC"::: ) (Set (Var "X"))))))) ; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "l" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_coh_sp :::"MapsC"::: ) (Set (Const "X"))); cluster (Set "l" ($#k2_xtuple_0 :::"`2"::: ) ) -> ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ; end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "l" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_coh_sp :::"MapsC"::: ) (Set (Const "X"))); func :::"dom"::: "l" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_coh_sp :::"CSp"::: ) "X") equals :: COH_SP:def 7 (Set (Set "(" "l" ($#k1_xtuple_0 :::"`1"::: ) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ); func :::"cod"::: "l" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_coh_sp :::"CSp"::: ) "X") equals :: COH_SP:def 8 (Set (Set "(" "l" ($#k1_xtuple_0 :::"`1"::: ) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ); end; :: deftheorem defines :::"dom"::: COH_SP:def 7 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "l")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_coh_sp :::"MapsC"::: ) (Set (Var "X"))) "holds" (Bool (Set ($#k6_coh_sp :::"dom"::: ) (Set (Var "l"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "l")) ($#k1_xtuple_0 :::"`1"::: ) ")" ) ($#k1_xtuple_0 :::"`1"::: ) )))); :: deftheorem defines :::"cod"::: COH_SP:def 8 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "l")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_coh_sp :::"MapsC"::: ) (Set (Var "X"))) "holds" (Bool (Set ($#k7_coh_sp :::"cod"::: ) (Set (Var "l"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "l")) ($#k1_xtuple_0 :::"`1"::: ) ")" ) ($#k2_xtuple_0 :::"`2"::: ) )))); theorem :: COH_SP:20 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "l")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_coh_sp :::"MapsC"::: ) (Set (Var "X"))) "holds" (Bool (Set (Var "l")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set "(" ($#k6_coh_sp :::"dom"::: ) (Set (Var "l")) ")" ) "," (Set "(" ($#k7_coh_sp :::"cod"::: ) (Set (Var "l")) ")" ) ($#k4_tarski :::"]"::: ) ) "," (Set "(" (Set (Var "l")) ($#k2_xtuple_0 :::"`2"::: ) ")" ) ($#k4_tarski :::"]"::: ) )))) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "C" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_coh_sp :::"CSp"::: ) (Set (Const "X"))); func :::"id$"::: "C" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_coh_sp :::"MapsC"::: ) "X") equals :: COH_SP:def 9 (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) "C" "," "C" ($#k4_tarski :::"]"::: ) ) "," (Set "(" ($#k6_partfun1 :::"id"::: ) (Set "(" ($#k3_tarski :::"union"::: ) "C" ")" ) ")" ) ($#k4_tarski :::"]"::: ) ); end; :: deftheorem defines :::"id$"::: COH_SP:def 9 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_coh_sp :::"CSp"::: ) (Set (Var "X"))) "holds" (Bool (Set ($#k8_coh_sp :::"id$"::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "C")) "," (Set (Var "C")) ($#k4_tarski :::"]"::: ) ) "," (Set "(" ($#k6_partfun1 :::"id"::: ) (Set "(" ($#k3_tarski :::"union"::: ) (Set (Var "C")) ")" ) ")" ) ($#k4_tarski :::"]"::: ) )))); theorem :: COH_SP:21 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "l")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_coh_sp :::"MapsC"::: ) (Set (Var "X"))) "holds" (Bool "(" (Bool "(" (Bool (Set ($#k3_tarski :::"union"::: ) (Set "(" ($#k7_coh_sp :::"cod"::: ) (Set (Var "l")) ")" )) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) "or" (Bool (Set ($#k3_tarski :::"union"::: ) (Set "(" ($#k6_coh_sp :::"dom"::: ) (Set (Var "l")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ) & (Bool (Set (Set (Var "l")) ($#k2_xtuple_0 :::"`2"::: ) ) "is" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k3_tarski :::"union"::: ) (Set "(" ($#k6_coh_sp :::"dom"::: ) (Set (Var "l")) ")" ) ")" ) "," (Set "(" ($#k3_tarski :::"union"::: ) (Set "(" ($#k7_coh_sp :::"cod"::: ) (Set (Var "l")) ")" ) ")" )) & (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 :::"}"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k6_coh_sp :::"dom"::: ) (Set (Var "l"))))) "holds" (Bool (Set ($#k2_tarski :::"{"::: ) (Set "(" (Set "(" (Set (Var "l")) ($#k2_xtuple_0 :::"`2"::: ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) "," (Set "(" (Set "(" (Set (Var "l")) ($#k2_xtuple_0 :::"`2"::: ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "y")) ")" ) ($#k2_tarski :::"}"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k7_coh_sp :::"cod"::: ) (Set (Var "l")))) ")" ) ")" ))) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "l1", "l2" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_coh_sp :::"MapsC"::: ) (Set (Const "X"))); assume (Bool (Set ($#k7_coh_sp :::"cod"::: ) (Set (Const "l1"))) ($#r1_hidden :::"="::: ) (Set ($#k6_coh_sp :::"dom"::: ) (Set (Const "l2")))) ; func "l2" :::"*"::: "l1" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_coh_sp :::"MapsC"::: ) "X") equals :: COH_SP:def 10 (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set "(" ($#k6_coh_sp :::"dom"::: ) "l1" ")" ) "," (Set "(" ($#k7_coh_sp :::"cod"::: ) "l2" ")" ) ($#k4_tarski :::"]"::: ) ) "," (Set "(" (Set "(" "l2" ($#k2_xtuple_0 :::"`2"::: ) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" "l1" ($#k2_xtuple_0 :::"`2"::: ) ")" ) ")" ) ($#k4_tarski :::"]"::: ) ); end; :: deftheorem defines :::"*"::: COH_SP:def 10 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "l1")) "," (Set (Var "l2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_coh_sp :::"MapsC"::: ) (Set (Var "X"))) "st" (Bool (Bool (Set ($#k7_coh_sp :::"cod"::: ) (Set (Var "l1"))) ($#r1_hidden :::"="::: ) (Set ($#k6_coh_sp :::"dom"::: ) (Set (Var "l2"))))) "holds" (Bool (Set (Set (Var "l2")) ($#k9_coh_sp :::"*"::: ) (Set (Var "l1"))) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set "(" ($#k6_coh_sp :::"dom"::: ) (Set (Var "l1")) ")" ) "," (Set "(" ($#k7_coh_sp :::"cod"::: ) (Set (Var "l2")) ")" ) ($#k4_tarski :::"]"::: ) ) "," (Set "(" (Set "(" (Set (Var "l2")) ($#k2_xtuple_0 :::"`2"::: ) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set (Var "l1")) ($#k2_xtuple_0 :::"`2"::: ) ")" ) ")" ) ($#k4_tarski :::"]"::: ) )))); theorem :: COH_SP:22 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "l2")) "," (Set (Var "l1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_coh_sp :::"MapsC"::: ) (Set (Var "X"))) "st" (Bool (Bool (Set ($#k6_coh_sp :::"dom"::: ) (Set (Var "l2"))) ($#r1_hidden :::"="::: ) (Set ($#k7_coh_sp :::"cod"::: ) (Set (Var "l1"))))) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "l2")) ($#k9_coh_sp :::"*"::: ) (Set (Var "l1")) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "l2")) ($#k2_xtuple_0 :::"`2"::: ) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set (Var "l1")) ($#k2_xtuple_0 :::"`2"::: ) ")" ))) & (Bool (Set ($#k6_coh_sp :::"dom"::: ) (Set "(" (Set (Var "l2")) ($#k9_coh_sp :::"*"::: ) (Set (Var "l1")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_coh_sp :::"dom"::: ) (Set (Var "l1")))) & (Bool (Set ($#k7_coh_sp :::"cod"::: ) (Set "(" (Set (Var "l2")) ($#k9_coh_sp :::"*"::: ) (Set (Var "l1")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k7_coh_sp :::"cod"::: ) (Set (Var "l2")))) ")" ))) ; theorem :: COH_SP:23 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "l2")) "," (Set (Var "l1")) "," (Set (Var "l3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_coh_sp :::"MapsC"::: ) (Set (Var "X"))) "st" (Bool (Bool (Set ($#k6_coh_sp :::"dom"::: ) (Set (Var "l2"))) ($#r1_hidden :::"="::: ) (Set ($#k7_coh_sp :::"cod"::: ) (Set (Var "l1")))) & (Bool (Set ($#k6_coh_sp :::"dom"::: ) (Set (Var "l3"))) ($#r1_hidden :::"="::: ) (Set ($#k7_coh_sp :::"cod"::: ) (Set (Var "l2"))))) "holds" (Bool (Set (Set (Var "l3")) ($#k9_coh_sp :::"*"::: ) (Set "(" (Set (Var "l2")) ($#k9_coh_sp :::"*"::: ) (Set (Var "l1")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "l3")) ($#k9_coh_sp :::"*"::: ) (Set (Var "l2")) ")" ) ($#k9_coh_sp :::"*"::: ) (Set (Var "l1")))))) ; theorem :: COH_SP:24 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_coh_sp :::"CSp"::: ) (Set (Var "X"))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k8_coh_sp :::"id$"::: ) (Set (Var "C")) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_partfun1 :::"id"::: ) (Set "(" ($#k3_tarski :::"union"::: ) (Set (Var "C")) ")" ))) & (Bool (Set ($#k6_coh_sp :::"dom"::: ) (Set "(" ($#k8_coh_sp :::"id$"::: ) (Set (Var "C")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "C"))) & (Bool (Set ($#k7_coh_sp :::"cod"::: ) (Set "(" ($#k8_coh_sp :::"id$"::: ) (Set (Var "C")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "C"))) ")" ))) ; theorem :: COH_SP:25 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "l")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_coh_sp :::"MapsC"::: ) (Set (Var "X"))) "holds" (Bool "(" (Bool (Set (Set (Var "l")) ($#k9_coh_sp :::"*"::: ) (Set "(" ($#k8_coh_sp :::"id$"::: ) (Set "(" ($#k6_coh_sp :::"dom"::: ) (Set (Var "l")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "l"))) & (Bool (Set (Set "(" ($#k8_coh_sp :::"id$"::: ) (Set "(" ($#k7_coh_sp :::"cod"::: ) (Set (Var "l")) ")" ) ")" ) ($#k9_coh_sp :::"*"::: ) (Set (Var "l"))) ($#r1_hidden :::"="::: ) (Set (Var "l"))) ")" ))) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; func :::"CDom"::: "X" -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k5_coh_sp :::"MapsC"::: ) "X" ")" ) "," (Set "(" ($#k3_coh_sp :::"CSp"::: ) "X" ")" ) means :: COH_SP:def 11 (Bool "for" (Set (Var "l")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_coh_sp :::"MapsC"::: ) "X") "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "l"))) ($#r1_hidden :::"="::: ) (Set ($#k6_coh_sp :::"dom"::: ) (Set (Var "l"))))); func :::"CCod"::: "X" -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k5_coh_sp :::"MapsC"::: ) "X" ")" ) "," (Set "(" ($#k3_coh_sp :::"CSp"::: ) "X" ")" ) means :: COH_SP:def 12 (Bool "for" (Set (Var "l")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_coh_sp :::"MapsC"::: ) "X") "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "l"))) ($#r1_hidden :::"="::: ) (Set ($#k7_coh_sp :::"cod"::: ) (Set (Var "l"))))); func :::"CComp"::: "X" -> ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k5_coh_sp :::"MapsC"::: ) "X" ")" ) "," (Set "(" ($#k5_coh_sp :::"MapsC"::: ) "X" ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "(" ($#k5_coh_sp :::"MapsC"::: ) "X" ")" ) means :: COH_SP:def 13 (Bool "(" (Bool "(" "for" (Set (Var "l2")) "," (Set (Var "l1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_coh_sp :::"MapsC"::: ) "X") "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "l2")) "," (Set (Var "l1")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) it)) "iff" (Bool (Set ($#k6_coh_sp :::"dom"::: ) (Set (Var "l2"))) ($#r1_hidden :::"="::: ) (Set ($#k7_coh_sp :::"cod"::: ) (Set (Var "l1")))) ")" ) ")" ) & (Bool "(" "for" (Set (Var "l2")) "," (Set (Var "l1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_coh_sp :::"MapsC"::: ) "X") "st" (Bool (Bool (Set ($#k6_coh_sp :::"dom"::: ) (Set (Var "l2"))) ($#r1_hidden :::"="::: ) (Set ($#k7_coh_sp :::"cod"::: ) (Set (Var "l1"))))) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "l2")) "," (Set (Var "l1")) ($#k4_tarski :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "l2")) ($#k9_coh_sp :::"*"::: ) (Set (Var "l1")))) ")" ) ")" ); end; :: deftheorem defines :::"CDom"::: COH_SP:def 11 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k5_coh_sp :::"MapsC"::: ) (Set (Var "X")) ")" ) "," (Set "(" ($#k3_coh_sp :::"CSp"::: ) (Set (Var "X")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k10_coh_sp :::"CDom"::: ) (Set (Var "X")))) "iff" (Bool "for" (Set (Var "l")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_coh_sp :::"MapsC"::: ) (Set (Var "X"))) "holds" (Bool (Set (Set (Var "b2")) ($#k3_funct_2 :::"."::: ) (Set (Var "l"))) ($#r1_hidden :::"="::: ) (Set ($#k6_coh_sp :::"dom"::: ) (Set (Var "l"))))) ")" ))); :: deftheorem defines :::"CCod"::: COH_SP:def 12 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k5_coh_sp :::"MapsC"::: ) (Set (Var "X")) ")" ) "," (Set "(" ($#k3_coh_sp :::"CSp"::: ) (Set (Var "X")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k11_coh_sp :::"CCod"::: ) (Set (Var "X")))) "iff" (Bool "for" (Set (Var "l")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_coh_sp :::"MapsC"::: ) (Set (Var "X"))) "holds" (Bool (Set (Set (Var "b2")) ($#k3_funct_2 :::"."::: ) (Set (Var "l"))) ($#r1_hidden :::"="::: ) (Set ($#k7_coh_sp :::"cod"::: ) (Set (Var "l"))))) ")" ))); :: deftheorem defines :::"CComp"::: COH_SP:def 13 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k5_coh_sp :::"MapsC"::: ) (Set (Var "X")) ")" ) "," (Set "(" ($#k5_coh_sp :::"MapsC"::: ) (Set (Var "X")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "(" ($#k5_coh_sp :::"MapsC"::: ) (Set (Var "X")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k12_coh_sp :::"CComp"::: ) (Set (Var "X")))) "iff" (Bool "(" (Bool "(" "for" (Set (Var "l2")) "," (Set (Var "l1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_coh_sp :::"MapsC"::: ) (Set (Var "X"))) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "l2")) "," (Set (Var "l1")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "b2")))) "iff" (Bool (Set ($#k6_coh_sp :::"dom"::: ) (Set (Var "l2"))) ($#r1_hidden :::"="::: ) (Set ($#k7_coh_sp :::"cod"::: ) (Set (Var "l1")))) ")" ) ")" ) & (Bool "(" "for" (Set (Var "l2")) "," (Set (Var "l1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_coh_sp :::"MapsC"::: ) (Set (Var "X"))) "st" (Bool (Bool (Set ($#k6_coh_sp :::"dom"::: ) (Set (Var "l2"))) ($#r1_hidden :::"="::: ) (Set ($#k7_coh_sp :::"cod"::: ) (Set (Var "l1"))))) "holds" (Bool (Set (Set (Var "b2")) ($#k1_funct_1 :::"."::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "l2")) "," (Set (Var "l1")) ($#k4_tarski :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "l2")) ($#k9_coh_sp :::"*"::: ) (Set (Var "l1")))) ")" ) ")" ) ")" ))); theorem :: COH_SP:26 canceled; definitioncanceled; let "X" be ($#m1_hidden :::"set"::: ) ; func :::"CohCat"::: "X" -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v1_cat_1 :::"strict"::: ) ($#l1_cat_1 :::"CatStr"::: ) equals :: COH_SP:def 15 (Set ($#g1_cat_1 :::"CatStr"::: ) "(#" (Set "(" ($#k3_coh_sp :::"CSp"::: ) "X" ")" ) "," (Set "(" ($#k5_coh_sp :::"MapsC"::: ) "X" ")" ) "," (Set "(" ($#k10_coh_sp :::"CDom"::: ) "X" ")" ) "," (Set "(" ($#k11_coh_sp :::"CCod"::: ) "X" ")" ) "," (Set "(" ($#k12_coh_sp :::"CComp"::: ) "X" ")" ) "#)" ); end; :: deftheorem COH_SP:def 14 : canceled; :: deftheorem defines :::"CohCat"::: COH_SP:def 15 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k13_coh_sp :::"CohCat"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#g1_cat_1 :::"CatStr"::: ) "(#" (Set "(" ($#k3_coh_sp :::"CSp"::: ) (Set (Var "X")) ")" ) "," (Set "(" ($#k5_coh_sp :::"MapsC"::: ) (Set (Var "X")) ")" ) "," (Set "(" ($#k10_coh_sp :::"CDom"::: ) (Set (Var "X")) ")" ) "," (Set "(" ($#k11_coh_sp :::"CCod"::: ) (Set (Var "X")) ")" ) "," (Set "(" ($#k12_coh_sp :::"CComp"::: ) (Set (Var "X")) ")" ) "#)" ))); registrationlet "X" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k13_coh_sp :::"CohCat"::: ) "X") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v1_cat_1 :::"strict"::: ) ($#v2_cat_1 :::"Category-like"::: ) ($#v3_cat_1 :::"transitive"::: ) ($#v4_cat_1 :::"associative"::: ) ($#v5_cat_1 :::"reflexive"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k13_coh_sp :::"CohCat"::: ) "X") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v1_cat_1 :::"strict"::: ) ($#v6_cat_1 :::"with_identities"::: ) ; end; begin definitionlet "X" be ($#m1_hidden :::"set"::: ) ; func :::"Toler"::: "X" -> ($#m1_hidden :::"set"::: ) means :: COH_SP:def 16 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"Tolerance":::) "of" "X") ")" )); end; :: deftheorem defines :::"Toler"::: COH_SP:def 16 : (Bool "for" (Set (Var "X")) "," (Set (Var "b2")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k14_coh_sp :::"Toler"::: ) (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 (Set (Var "x")) "is" ($#m1_subset_1 :::"Tolerance":::) "of" (Set (Var "X"))) ")" )) ")" )); registrationlet "X" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k14_coh_sp :::"Toler"::: ) "X") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; func :::"Toler_on_subsets"::: "X" -> ($#m1_hidden :::"set"::: ) equals :: COH_SP:def 17 (Set ($#k3_tarski :::"union"::: ) "{" (Set "(" ($#k14_coh_sp :::"Toler"::: ) (Set (Var "Y")) ")" ) where Y "is" ($#m1_subset_1 :::"Subset":::) "of" "X" : (Bool verum) "}" ); end; :: deftheorem defines :::"Toler_on_subsets"::: COH_SP:def 17 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k15_coh_sp :::"Toler_on_subsets"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) "{" (Set "(" ($#k14_coh_sp :::"Toler"::: ) (Set (Var "Y")) ")" ) where Y "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) : (Bool verum) "}" ))); registrationlet "X" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k15_coh_sp :::"Toler_on_subsets"::: ) "X") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; theorem :: COH_SP:27 (Bool "for" (Set (Var "x")) "," (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k15_coh_sp :::"Toler_on_subsets"::: ) (Set (Var "X")))) "iff" (Bool "ex" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "X"))) & (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"Tolerance":::) "of" (Set (Var "A"))) ")" )) ")" )) ; theorem :: COH_SP:28 (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k1_eqrel_1 :::"Total"::: ) (Set (Var "a"))) ($#r2_hidden :::"in"::: ) (Set ($#k14_coh_sp :::"Toler"::: ) (Set (Var "a"))))) ; theorem :: COH_SP:29 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k15_coh_sp :::"Toler_on_subsets"::: ) (Set (Var "X"))))) ; theorem :: COH_SP:30 (Bool "for" (Set (Var "a")) "," (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r1_tarski :::"c="::: ) (Set (Var "X")))) "holds" (Bool (Set ($#k1_eqrel_1 :::"Total"::: ) (Set (Var "a"))) ($#r2_hidden :::"in"::: ) (Set ($#k15_coh_sp :::"Toler_on_subsets"::: ) (Set (Var "X"))))) ; theorem :: COH_SP:31 (Bool "for" (Set (Var "a")) "," (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r1_tarski :::"c="::: ) (Set (Var "X")))) "holds" (Bool (Set ($#k6_partfun1 :::"id"::: ) (Set (Var "a"))) ($#r2_hidden :::"in"::: ) (Set ($#k15_coh_sp :::"Toler_on_subsets"::: ) (Set (Var "X"))))) ; theorem :: COH_SP:32 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k1_eqrel_1 :::"Total"::: ) (Set (Var "X"))) ($#r2_hidden :::"in"::: ) (Set ($#k15_coh_sp :::"Toler_on_subsets"::: ) (Set (Var "X"))))) ; theorem :: COH_SP:33 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k6_partfun1 :::"id"::: ) (Set (Var "X"))) ($#r2_hidden :::"in"::: ) (Set ($#k15_coh_sp :::"Toler_on_subsets"::: ) (Set (Var "X"))))) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; func :::"TOL"::: "X" -> ($#m1_hidden :::"set"::: ) equals :: COH_SP:def 18 "{" (Set ($#k4_tarski :::"["::: ) (Set (Var "t")) "," (Set (Var "Y")) ($#k4_tarski :::"]"::: ) ) where t "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k15_coh_sp :::"Toler_on_subsets"::: ) "X"), Y "is" ($#m1_subset_1 :::"Subset":::) "of" "X" : (Bool (Set (Var "t")) "is" ($#m1_subset_1 :::"Tolerance":::) "of" (Set (Var "Y"))) "}" ; end; :: deftheorem defines :::"TOL"::: COH_SP:def 18 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k16_coh_sp :::"TOL"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) "{" (Set ($#k4_tarski :::"["::: ) (Set (Var "t")) "," (Set (Var "Y")) ($#k4_tarski :::"]"::: ) ) where t "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k15_coh_sp :::"Toler_on_subsets"::: ) (Set (Var "X"))), Y "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) : (Bool (Set (Var "t")) "is" ($#m1_subset_1 :::"Tolerance":::) "of" (Set (Var "Y"))) "}" )); registrationlet "X" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k16_coh_sp :::"TOL"::: ) "X") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; theorem :: COH_SP:34 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k16_coh_sp :::"TOL"::: ) (Set (Var "X"))))) ; theorem :: COH_SP:35 (Bool "for" (Set (Var "a")) "," (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r1_tarski :::"c="::: ) (Set (Var "X")))) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" ($#k6_partfun1 :::"id"::: ) (Set (Var "a")) ")" ) "," (Set (Var "a")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k16_coh_sp :::"TOL"::: ) (Set (Var "X"))))) ; theorem :: COH_SP:36 (Bool "for" (Set (Var "a")) "," (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r1_tarski :::"c="::: ) (Set (Var "X")))) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" ($#k1_eqrel_1 :::"Total"::: ) (Set (Var "a")) ")" ) "," (Set (Var "a")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k16_coh_sp :::"TOL"::: ) (Set (Var "X"))))) ; theorem :: COH_SP:37 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" ($#k6_partfun1 :::"id"::: ) (Set (Var "X")) ")" ) "," (Set (Var "X")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k16_coh_sp :::"TOL"::: ) (Set (Var "X"))))) ; theorem :: COH_SP:38 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" ($#k1_eqrel_1 :::"Total"::: ) (Set (Var "X")) ")" ) "," (Set (Var "X")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k16_coh_sp :::"TOL"::: ) (Set (Var "X"))))) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "T" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k16_coh_sp :::"TOL"::: ) (Set (Const "X"))); :: original: :::"`2"::: redefine func "T" :::"`2"::: -> ($#m1_subset_1 :::"Subset":::) "of" "X"; :: original: :::"`1"::: redefine func "T" :::"`1"::: -> ($#m1_subset_1 :::"Tolerance":::) "of" (Set "(" "T" ($#k2_xtuple_0 :::"`2"::: ) ")" ); end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; func :::"FuncsT"::: "X" -> ($#m1_hidden :::"set"::: ) equals :: COH_SP:def 19 (Set ($#k3_tarski :::"union"::: ) "{" (Set "(" ($#k1_funct_2 :::"Funcs"::: ) "(" (Set "(" (Set (Var "T")) ($#k17_coh_sp :::"`2"::: ) ")" ) "," (Set "(" (Set (Var "TT")) ($#k17_coh_sp :::"`2"::: ) ")" ) ")" ")" ) where T, TT "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k16_coh_sp :::"TOL"::: ) "X") : (Bool verum) "}" ); end; :: deftheorem defines :::"FuncsT"::: COH_SP:def 19 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k19_coh_sp :::"FuncsT"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) "{" (Set "(" ($#k1_funct_2 :::"Funcs"::: ) "(" (Set "(" (Set (Var "T")) ($#k17_coh_sp :::"`2"::: ) ")" ) "," (Set "(" (Set (Var "TT")) ($#k17_coh_sp :::"`2"::: ) ")" ) ")" ")" ) where T, TT "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k16_coh_sp :::"TOL"::: ) (Set (Var "X"))) : (Bool verum) "}" ))); registrationlet "X" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k19_coh_sp :::"FuncsT"::: ) "X") -> ($#v4_funct_1 :::"functional"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; theorem :: COH_SP:39 (Bool "for" (Set (Var "x")) "," (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k19_coh_sp :::"FuncsT"::: ) (Set (Var "X")))) "iff" (Bool "ex" (Set (Var "T1")) "," (Set (Var "T2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k16_coh_sp :::"TOL"::: ) (Set (Var "X"))) "st" (Bool "(" "(" (Bool (Bool (Set (Set (Var "T2")) ($#k17_coh_sp :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "implies" (Bool (Set (Set (Var "T1")) ($#k17_coh_sp :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" & (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set (Var "T1")) ($#k17_coh_sp :::"`2"::: ) ")" ) "," (Set "(" (Set (Var "T2")) ($#k17_coh_sp :::"`2"::: ) ")" )) ")" )) ")" )) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; func :::"MapsT"::: "X" -> ($#m1_hidden :::"set"::: ) equals :: COH_SP:def 20 "{" (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "T")) "," (Set (Var "TT")) ($#k4_tarski :::"]"::: ) ) "," (Set (Var "f")) ($#k4_tarski :::"]"::: ) ) where T, TT "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k16_coh_sp :::"TOL"::: ) "X"), f "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k19_coh_sp :::"FuncsT"::: ) "X") : (Bool "(" "(" (Bool (Bool (Set (Set (Var "TT")) ($#k17_coh_sp :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "implies" (Bool (Set (Set (Var "T")) ($#k17_coh_sp :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" & (Bool (Set (Var "f")) "is" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set (Var "T")) ($#k17_coh_sp :::"`2"::: ) ")" ) "," (Set "(" (Set (Var "TT")) ($#k17_coh_sp :::"`2"::: ) ")" )) & (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 (Set (Var "T")) ($#k18_coh_sp :::"`1"::: ) ))) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) "," (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "y")) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Set (Var "TT")) ($#k18_coh_sp :::"`1"::: ) )) ")" ) ")" ) "}" ; end; :: deftheorem defines :::"MapsT"::: COH_SP:def 20 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k20_coh_sp :::"MapsT"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) "{" (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "T")) "," (Set (Var "TT")) ($#k4_tarski :::"]"::: ) ) "," (Set (Var "f")) ($#k4_tarski :::"]"::: ) ) where T, TT "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k16_coh_sp :::"TOL"::: ) (Set (Var "X"))), f "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k19_coh_sp :::"FuncsT"::: ) (Set (Var "X"))) : (Bool "(" "(" (Bool (Bool (Set (Set (Var "TT")) ($#k17_coh_sp :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "implies" (Bool (Set (Set (Var "T")) ($#k17_coh_sp :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" & (Bool (Set (Var "f")) "is" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set (Var "T")) ($#k17_coh_sp :::"`2"::: ) ")" ) "," (Set "(" (Set (Var "TT")) ($#k17_coh_sp :::"`2"::: ) ")" )) & (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 (Set (Var "T")) ($#k18_coh_sp :::"`1"::: ) ))) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) "," (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "y")) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Set (Var "TT")) ($#k18_coh_sp :::"`1"::: ) )) ")" ) ")" ) "}" )); registrationlet "X" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k20_coh_sp :::"MapsT"::: ) "X") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; theorem :: COH_SP:40 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k20_coh_sp :::"MapsT"::: ) (Set (Var "X"))) (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k19_coh_sp :::"FuncsT"::: ) (Set (Var "X")))(Bool "ex" (Set (Var "T1")) "," (Set (Var "T2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k16_coh_sp :::"TOL"::: ) (Set (Var "X"))) "st" (Bool "(" (Bool (Set (Var "m")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "T1")) "," (Set (Var "T2")) ($#k4_tarski :::"]"::: ) ) "," (Set (Var "f")) ($#k4_tarski :::"]"::: ) )) & "(" (Bool (Bool (Set (Set (Var "T2")) ($#k17_coh_sp :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "implies" (Bool (Set (Set (Var "T1")) ($#k17_coh_sp :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" & (Bool (Set (Var "f")) "is" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set (Var "T1")) ($#k17_coh_sp :::"`2"::: ) ")" ) "," (Set "(" (Set (Var "T2")) ($#k17_coh_sp :::"`2"::: ) ")" )) & (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 (Set (Var "T1")) ($#k18_coh_sp :::"`1"::: ) ))) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) "," (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "y")) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Set (Var "T2")) ($#k18_coh_sp :::"`1"::: ) )) ")" ) ")" ))))) ; theorem :: COH_SP:41 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "T1")) "," (Set (Var "T2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k16_coh_sp :::"TOL"::: ) (Set (Var "X"))) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set (Var "T1")) ($#k17_coh_sp :::"`2"::: ) ")" ) "," (Set "(" (Set (Var "T2")) ($#k17_coh_sp :::"`2"::: ) ")" ) "st" (Bool "(" (Bool (Bool (Set (Set (Var "T2")) ($#k17_coh_sp :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "implies" (Bool (Set (Set (Var "T1")) ($#k17_coh_sp :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" & (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 (Set (Var "T1")) ($#k18_coh_sp :::"`1"::: ) ))) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) "," (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "y")) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Set (Var "T2")) ($#k18_coh_sp :::"`1"::: ) )) ")" )) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "T1")) "," (Set (Var "T2")) ($#k4_tarski :::"]"::: ) ) "," (Set (Var "f")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k20_coh_sp :::"MapsT"::: ) (Set (Var "X"))))))) ; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "m" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k20_coh_sp :::"MapsT"::: ) (Set (Const "X"))); cluster (Set "m" ($#k2_xtuple_0 :::"`2"::: ) ) -> ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ; end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "m" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k20_coh_sp :::"MapsT"::: ) (Set (Const "X"))); func :::"dom"::: "m" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k16_coh_sp :::"TOL"::: ) "X") equals :: COH_SP:def 21 (Set (Set "(" "m" ($#k1_xtuple_0 :::"`1"::: ) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ); func :::"cod"::: "m" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k16_coh_sp :::"TOL"::: ) "X") equals :: COH_SP:def 22 (Set (Set "(" "m" ($#k1_xtuple_0 :::"`1"::: ) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ); end; :: deftheorem defines :::"dom"::: COH_SP:def 21 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k20_coh_sp :::"MapsT"::: ) (Set (Var "X"))) "holds" (Bool (Set ($#k21_coh_sp :::"dom"::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "m")) ($#k1_xtuple_0 :::"`1"::: ) ")" ) ($#k1_xtuple_0 :::"`1"::: ) )))); :: deftheorem defines :::"cod"::: COH_SP:def 22 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k20_coh_sp :::"MapsT"::: ) (Set (Var "X"))) "holds" (Bool (Set ($#k22_coh_sp :::"cod"::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "m")) ($#k1_xtuple_0 :::"`1"::: ) ")" ) ($#k2_xtuple_0 :::"`2"::: ) )))); theorem :: COH_SP:42 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k20_coh_sp :::"MapsT"::: ) (Set (Var "X"))) "holds" (Bool (Set (Var "m")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set "(" ($#k21_coh_sp :::"dom"::: ) (Set (Var "m")) ")" ) "," (Set "(" ($#k22_coh_sp :::"cod"::: ) (Set (Var "m")) ")" ) ($#k4_tarski :::"]"::: ) ) "," (Set "(" (Set (Var "m")) ($#k2_xtuple_0 :::"`2"::: ) ")" ) ($#k4_tarski :::"]"::: ) )))) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "T" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k16_coh_sp :::"TOL"::: ) (Set (Const "X"))); func :::"id$"::: "T" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k20_coh_sp :::"MapsT"::: ) "X") equals :: COH_SP:def 23 (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) "T" "," "T" ($#k4_tarski :::"]"::: ) ) "," (Set "(" ($#k6_partfun1 :::"id"::: ) (Set "(" "T" ($#k17_coh_sp :::"`2"::: ) ")" ) ")" ) ($#k4_tarski :::"]"::: ) ); end; :: deftheorem defines :::"id$"::: COH_SP:def 23 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "T")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k16_coh_sp :::"TOL"::: ) (Set (Var "X"))) "holds" (Bool (Set ($#k23_coh_sp :::"id$"::: ) (Set (Var "T"))) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "T")) "," (Set (Var "T")) ($#k4_tarski :::"]"::: ) ) "," (Set "(" ($#k6_partfun1 :::"id"::: ) (Set "(" (Set (Var "T")) ($#k17_coh_sp :::"`2"::: ) ")" ) ")" ) ($#k4_tarski :::"]"::: ) )))); theorem :: COH_SP:43 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k20_coh_sp :::"MapsT"::: ) (Set (Var "X"))) "holds" (Bool "(" (Bool "(" (Bool (Set (Set "(" ($#k22_coh_sp :::"cod"::: ) (Set (Var "m")) ")" ) ($#k17_coh_sp :::"`2"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) "or" (Bool (Set (Set "(" ($#k21_coh_sp :::"dom"::: ) (Set (Var "m")) ")" ) ($#k17_coh_sp :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ) & (Bool (Set (Set (Var "m")) ($#k2_xtuple_0 :::"`2"::: ) ) "is" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set "(" ($#k21_coh_sp :::"dom"::: ) (Set (Var "m")) ")" ) ($#k17_coh_sp :::"`2"::: ) ")" ) "," (Set "(" (Set "(" ($#k22_coh_sp :::"cod"::: ) (Set (Var "m")) ")" ) ($#k17_coh_sp :::"`2"::: ) ")" )) & (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 (Set "(" ($#k21_coh_sp :::"dom"::: ) (Set (Var "m")) ")" ) ($#k18_coh_sp :::"`1"::: ) ))) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" (Set "(" (Set (Var "m")) ($#k2_xtuple_0 :::"`2"::: ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) "," (Set "(" (Set "(" (Set (Var "m")) ($#k2_xtuple_0 :::"`2"::: ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "y")) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k22_coh_sp :::"cod"::: ) (Set (Var "m")) ")" ) ($#k18_coh_sp :::"`1"::: ) )) ")" ) ")" ))) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "m1", "m2" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k20_coh_sp :::"MapsT"::: ) (Set (Const "X"))); assume (Bool (Set ($#k22_coh_sp :::"cod"::: ) (Set (Const "m1"))) ($#r1_hidden :::"="::: ) (Set ($#k21_coh_sp :::"dom"::: ) (Set (Const "m2")))) ; func "m2" :::"*"::: "m1" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k20_coh_sp :::"MapsT"::: ) "X") equals :: COH_SP:def 24 (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set "(" ($#k21_coh_sp :::"dom"::: ) "m1" ")" ) "," (Set "(" ($#k22_coh_sp :::"cod"::: ) "m2" ")" ) ($#k4_tarski :::"]"::: ) ) "," (Set "(" (Set "(" "m2" ($#k2_xtuple_0 :::"`2"::: ) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" "m1" ($#k2_xtuple_0 :::"`2"::: ) ")" ) ")" ) ($#k4_tarski :::"]"::: ) ); end; :: deftheorem defines :::"*"::: COH_SP:def 24 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "m1")) "," (Set (Var "m2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k20_coh_sp :::"MapsT"::: ) (Set (Var "X"))) "st" (Bool (Bool (Set ($#k22_coh_sp :::"cod"::: ) (Set (Var "m1"))) ($#r1_hidden :::"="::: ) (Set ($#k21_coh_sp :::"dom"::: ) (Set (Var "m2"))))) "holds" (Bool (Set (Set (Var "m2")) ($#k24_coh_sp :::"*"::: ) (Set (Var "m1"))) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set "(" ($#k21_coh_sp :::"dom"::: ) (Set (Var "m1")) ")" ) "," (Set "(" ($#k22_coh_sp :::"cod"::: ) (Set (Var "m2")) ")" ) ($#k4_tarski :::"]"::: ) ) "," (Set "(" (Set "(" (Set (Var "m2")) ($#k2_xtuple_0 :::"`2"::: ) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set (Var "m1")) ($#k2_xtuple_0 :::"`2"::: ) ")" ) ")" ) ($#k4_tarski :::"]"::: ) )))); theorem :: COH_SP:44 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "m2")) "," (Set (Var "m1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k20_coh_sp :::"MapsT"::: ) (Set (Var "X"))) "st" (Bool (Bool (Set ($#k21_coh_sp :::"dom"::: ) (Set (Var "m2"))) ($#r1_hidden :::"="::: ) (Set ($#k22_coh_sp :::"cod"::: ) (Set (Var "m1"))))) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "m2")) ($#k24_coh_sp :::"*"::: ) (Set (Var "m1")) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "m2")) ($#k2_xtuple_0 :::"`2"::: ) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set (Var "m1")) ($#k2_xtuple_0 :::"`2"::: ) ")" ))) & (Bool (Set ($#k21_coh_sp :::"dom"::: ) (Set "(" (Set (Var "m2")) ($#k24_coh_sp :::"*"::: ) (Set (Var "m1")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k21_coh_sp :::"dom"::: ) (Set (Var "m1")))) & (Bool (Set ($#k22_coh_sp :::"cod"::: ) (Set "(" (Set (Var "m2")) ($#k24_coh_sp :::"*"::: ) (Set (Var "m1")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k22_coh_sp :::"cod"::: ) (Set (Var "m2")))) ")" ))) ; theorem :: COH_SP:45 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "m2")) "," (Set (Var "m1")) "," (Set (Var "m3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k20_coh_sp :::"MapsT"::: ) (Set (Var "X"))) "st" (Bool (Bool (Set ($#k21_coh_sp :::"dom"::: ) (Set (Var "m2"))) ($#r1_hidden :::"="::: ) (Set ($#k22_coh_sp :::"cod"::: ) (Set (Var "m1")))) & (Bool (Set ($#k21_coh_sp :::"dom"::: ) (Set (Var "m3"))) ($#r1_hidden :::"="::: ) (Set ($#k22_coh_sp :::"cod"::: ) (Set (Var "m2"))))) "holds" (Bool (Set (Set (Var "m3")) ($#k24_coh_sp :::"*"::: ) (Set "(" (Set (Var "m2")) ($#k24_coh_sp :::"*"::: ) (Set (Var "m1")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "m3")) ($#k24_coh_sp :::"*"::: ) (Set (Var "m2")) ")" ) ($#k24_coh_sp :::"*"::: ) (Set (Var "m1")))))) ; theorem :: COH_SP:46 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "T")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k16_coh_sp :::"TOL"::: ) (Set (Var "X"))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k23_coh_sp :::"id$"::: ) (Set (Var "T")) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_partfun1 :::"id"::: ) (Set "(" (Set (Var "T")) ($#k17_coh_sp :::"`2"::: ) ")" ))) & (Bool (Set ($#k21_coh_sp :::"dom"::: ) (Set "(" ($#k23_coh_sp :::"id$"::: ) (Set (Var "T")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "T"))) & (Bool (Set ($#k22_coh_sp :::"cod"::: ) (Set "(" ($#k23_coh_sp :::"id$"::: ) (Set (Var "T")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "T"))) ")" ))) ; theorem :: COH_SP:47 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k20_coh_sp :::"MapsT"::: ) (Set (Var "X"))) "holds" (Bool "(" (Bool (Set (Set (Var "m")) ($#k24_coh_sp :::"*"::: ) (Set "(" ($#k23_coh_sp :::"id$"::: ) (Set "(" ($#k21_coh_sp :::"dom"::: ) (Set (Var "m")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "m"))) & (Bool (Set (Set "(" ($#k23_coh_sp :::"id$"::: ) (Set "(" ($#k22_coh_sp :::"cod"::: ) (Set (Var "m")) ")" ) ")" ) ($#k24_coh_sp :::"*"::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set (Var "m"))) ")" ))) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; func :::"fDom"::: "X" -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k20_coh_sp :::"MapsT"::: ) "X" ")" ) "," (Set "(" ($#k16_coh_sp :::"TOL"::: ) "X" ")" ) means :: COH_SP:def 25 (Bool "for" (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k20_coh_sp :::"MapsT"::: ) "X") "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set ($#k21_coh_sp :::"dom"::: ) (Set (Var "m"))))); func :::"fCod"::: "X" -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k20_coh_sp :::"MapsT"::: ) "X" ")" ) "," (Set "(" ($#k16_coh_sp :::"TOL"::: ) "X" ")" ) means :: COH_SP:def 26 (Bool "for" (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k20_coh_sp :::"MapsT"::: ) "X") "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set ($#k22_coh_sp :::"cod"::: ) (Set (Var "m"))))); func :::"fComp"::: "X" -> ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k20_coh_sp :::"MapsT"::: ) "X" ")" ) "," (Set "(" ($#k20_coh_sp :::"MapsT"::: ) "X" ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "(" ($#k20_coh_sp :::"MapsT"::: ) "X" ")" ) means :: COH_SP:def 27 (Bool "(" (Bool "(" "for" (Set (Var "m2")) "," (Set (Var "m1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k20_coh_sp :::"MapsT"::: ) "X") "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "m2")) "," (Set (Var "m1")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) it)) "iff" (Bool (Set ($#k21_coh_sp :::"dom"::: ) (Set (Var "m2"))) ($#r1_hidden :::"="::: ) (Set ($#k22_coh_sp :::"cod"::: ) (Set (Var "m1")))) ")" ) ")" ) & (Bool "(" "for" (Set (Var "m2")) "," (Set (Var "m1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k20_coh_sp :::"MapsT"::: ) "X") "st" (Bool (Bool (Set ($#k21_coh_sp :::"dom"::: ) (Set (Var "m2"))) ($#r1_hidden :::"="::: ) (Set ($#k22_coh_sp :::"cod"::: ) (Set (Var "m1"))))) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "m2")) "," (Set (Var "m1")) ($#k4_tarski :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "m2")) ($#k24_coh_sp :::"*"::: ) (Set (Var "m1")))) ")" ) ")" ); end; :: deftheorem defines :::"fDom"::: COH_SP:def 25 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k20_coh_sp :::"MapsT"::: ) (Set (Var "X")) ")" ) "," (Set "(" ($#k16_coh_sp :::"TOL"::: ) (Set (Var "X")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k25_coh_sp :::"fDom"::: ) (Set (Var "X")))) "iff" (Bool "for" (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k20_coh_sp :::"MapsT"::: ) (Set (Var "X"))) "holds" (Bool (Set (Set (Var "b2")) ($#k3_funct_2 :::"."::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set ($#k21_coh_sp :::"dom"::: ) (Set (Var "m"))))) ")" ))); :: deftheorem defines :::"fCod"::: COH_SP:def 26 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k20_coh_sp :::"MapsT"::: ) (Set (Var "X")) ")" ) "," (Set "(" ($#k16_coh_sp :::"TOL"::: ) (Set (Var "X")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k26_coh_sp :::"fCod"::: ) (Set (Var "X")))) "iff" (Bool "for" (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k20_coh_sp :::"MapsT"::: ) (Set (Var "X"))) "holds" (Bool (Set (Set (Var "b2")) ($#k3_funct_2 :::"."::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set ($#k22_coh_sp :::"cod"::: ) (Set (Var "m"))))) ")" ))); :: deftheorem defines :::"fComp"::: COH_SP:def 27 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k20_coh_sp :::"MapsT"::: ) (Set (Var "X")) ")" ) "," (Set "(" ($#k20_coh_sp :::"MapsT"::: ) (Set (Var "X")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "(" ($#k20_coh_sp :::"MapsT"::: ) (Set (Var "X")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k27_coh_sp :::"fComp"::: ) (Set (Var "X")))) "iff" (Bool "(" (Bool "(" "for" (Set (Var "m2")) "," (Set (Var "m1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k20_coh_sp :::"MapsT"::: ) (Set (Var "X"))) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "m2")) "," (Set (Var "m1")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "b2")))) "iff" (Bool (Set ($#k21_coh_sp :::"dom"::: ) (Set (Var "m2"))) ($#r1_hidden :::"="::: ) (Set ($#k22_coh_sp :::"cod"::: ) (Set (Var "m1")))) ")" ) ")" ) & (Bool "(" "for" (Set (Var "m2")) "," (Set (Var "m1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k20_coh_sp :::"MapsT"::: ) (Set (Var "X"))) "st" (Bool (Bool (Set ($#k21_coh_sp :::"dom"::: ) (Set (Var "m2"))) ($#r1_hidden :::"="::: ) (Set ($#k22_coh_sp :::"cod"::: ) (Set (Var "m1"))))) "holds" (Bool (Set (Set (Var "b2")) ($#k1_funct_1 :::"."::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "m2")) "," (Set (Var "m1")) ($#k4_tarski :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "m2")) ($#k24_coh_sp :::"*"::: ) (Set (Var "m1")))) ")" ) ")" ) ")" ))); definitioncanceled; let "X" be ($#m1_hidden :::"set"::: ) ; func :::"TolCat"::: "X" -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v1_cat_1 :::"strict"::: ) ($#l1_cat_1 :::"CatStr"::: ) equals :: COH_SP:def 29 (Set ($#g1_cat_1 :::"CatStr"::: ) "(#" (Set "(" ($#k16_coh_sp :::"TOL"::: ) "X" ")" ) "," (Set "(" ($#k20_coh_sp :::"MapsT"::: ) "X" ")" ) "," (Set "(" ($#k25_coh_sp :::"fDom"::: ) "X" ")" ) "," (Set "(" ($#k26_coh_sp :::"fCod"::: ) "X" ")" ) "," (Set "(" ($#k27_coh_sp :::"fComp"::: ) "X" ")" ) "#)" ); end; :: deftheorem COH_SP:def 28 : canceled; :: deftheorem defines :::"TolCat"::: COH_SP:def 29 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k28_coh_sp :::"TolCat"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#g1_cat_1 :::"CatStr"::: ) "(#" (Set "(" ($#k16_coh_sp :::"TOL"::: ) (Set (Var "X")) ")" ) "," (Set "(" ($#k20_coh_sp :::"MapsT"::: ) (Set (Var "X")) ")" ) "," (Set "(" ($#k25_coh_sp :::"fDom"::: ) (Set (Var "X")) ")" ) "," (Set "(" ($#k26_coh_sp :::"fCod"::: ) (Set (Var "X")) ")" ) "," (Set "(" ($#k27_coh_sp :::"fComp"::: ) (Set (Var "X")) ")" ) "#)" ))); registrationlet "X" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k28_coh_sp :::"TolCat"::: ) "X") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v1_cat_1 :::"strict"::: ) ($#v2_cat_1 :::"Category-like"::: ) ($#v3_cat_1 :::"transitive"::: ) ($#v4_cat_1 :::"associative"::: ) ($#v5_cat_1 :::"reflexive"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k28_coh_sp :::"TolCat"::: ) "X") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v1_cat_1 :::"strict"::: ) ($#v6_cat_1 :::"with_identities"::: ) ; end;