:: PCS_0 semantic presentation begin definitionlet "R1", "R2" be ($#m1_hidden :::"set"::: ) ; let "R" be ($#m1_subset_1 :::"Relation":::) "of" (Set (Const "R1")) "," (Set (Const "R2")); :: original: :::"field"::: redefine func :::"field"::: "R" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" "R1" ($#k2_xboole_0 :::"\/"::: ) "R2" ")" ); end; definitionlet "R1", "R2", "S1", "S2" be ($#m1_hidden :::"set"::: ) ; let "R" be ($#m1_subset_1 :::"Relation":::) "of" (Set (Const "R1")) "," (Set (Const "R2")); let "S" be ($#m1_subset_1 :::"Relation":::) "of" (Set (Const "S1")) "," (Set (Const "S2")); :: original: :::"\/"::: redefine func "R" :::"\/"::: "S" -> ($#m1_subset_1 :::"Relation":::) "of" (Set "(" "R1" ($#k2_xboole_0 :::"\/"::: ) "S1" ")" ) "," (Set "(" "R2" ($#k2_xboole_0 :::"\/"::: ) "S2" ")" ); end; registrationlet "R1", "S1" be ($#m1_hidden :::"set"::: ) ; let "R" be ($#v1_partfun1 :::"total"::: ) ($#m1_subset_1 :::"Relation":::) "of" (Set (Const "R1")); let "S" be ($#v1_partfun1 :::"total"::: ) ($#m1_subset_1 :::"Relation":::) "of" (Set (Const "S1")); cluster (Set "R" ($#k2_xboole_0 :::"\/"::: ) "S") -> ($#v1_partfun1 :::"total"::: ) for ($#m1_subset_1 :::"Relation":::) "of" (Set "(" "R1" ($#k2_xboole_0 :::"\/"::: ) "S1" ")" ); end; registrationlet "R1", "S1" be ($#m1_hidden :::"set"::: ) ; let "R" be ($#v1_relat_2 :::"reflexive"::: ) ($#m1_subset_1 :::"Relation":::) "of" (Set (Const "R1")); let "S" be ($#v1_relat_2 :::"reflexive"::: ) ($#m1_subset_1 :::"Relation":::) "of" (Set (Const "S1")); cluster (Set "R" ($#k2_xboole_0 :::"\/"::: ) "S") -> ($#v1_relat_2 :::"reflexive"::: ) for ($#m1_subset_1 :::"Relation":::) "of" (Set "(" "R1" ($#k2_xboole_0 :::"\/"::: ) "S1" ")" ); end; registrationlet "R1", "S1" be ($#m1_hidden :::"set"::: ) ; let "R" be ($#v3_relat_2 :::"symmetric"::: ) ($#m1_subset_1 :::"Relation":::) "of" (Set (Const "R1")); let "S" be ($#v3_relat_2 :::"symmetric"::: ) ($#m1_subset_1 :::"Relation":::) "of" (Set (Const "S1")); cluster (Set "R" ($#k2_xboole_0 :::"\/"::: ) "S") -> ($#v3_relat_2 :::"symmetric"::: ) for ($#m1_subset_1 :::"Relation":::) "of" (Set "(" "R1" ($#k2_xboole_0 :::"\/"::: ) "S1" ")" ); end; theorem :: PCS_0:1 (Bool "for" (Set (Var "R1")) "," (Set (Var "S1")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#v8_relat_2 :::"transitive"::: ) ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "R1")) (Bool "for" (Set (Var "S")) "being" ($#v8_relat_2 :::"transitive"::: ) ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "S1")) "st" (Bool (Bool (Set (Var "R1")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "S1")))) "holds" (Bool (Set (Set (Var "R")) ($#k2_pcs_0 :::"\/"::: ) (Set (Var "S"))) "is" ($#v8_relat_2 :::"transitive"::: ) )))) ; definitionlet "I" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "C" be ($#v2_pralg_1 :::"1-sorted-yielding"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); redefine func :::"Carrier"::: "C" means :: PCS_0:def 1 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "I" "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" "C" ($#k10_pralg_1 :::"."::: ) (Set (Var "i")) ")" )))); end; :: deftheorem defines :::"Carrier"::: PCS_0:def 1 : (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#v2_pralg_1 :::"1-sorted-yielding"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "b3")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k12_pralg_1 :::"Carrier"::: ) (Set (Var "C")))) "iff" (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "I")) "holds" (Bool (Set (Set (Var "b3")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" (Set (Var "C")) ($#k10_pralg_1 :::"."::: ) (Set (Var "i")) ")" )))) ")" )))); definitionlet "R1", "R2", "S1", "S2" be ($#m1_hidden :::"set"::: ) ; let "R" be ($#m1_subset_1 :::"Relation":::) "of" (Set (Const "R1")) "," (Set (Const "R2")); let "S" be ($#m1_subset_1 :::"Relation":::) "of" (Set (Const "S1")) "," (Set (Const "S2")); func :::"[^":::"R" "," "S":::"^]"::: -> ($#m1_subset_1 :::"Relation":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) "R1" "," "S1" ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k2_zfmisc_1 :::"[:"::: ) "R2" "," "S2" ($#k2_zfmisc_1 :::":]"::: ) ) means :: PCS_0: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 "r1")) "," (Set (Var "s1")) "," (Set (Var "r2")) "," (Set (Var "s2")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "r1")) "," (Set (Var "s1")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "r2")) "," (Set (Var "s2")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Var "r1")) ($#r2_hidden :::"in"::: ) "R1") & (Bool (Set (Var "s1")) ($#r2_hidden :::"in"::: ) "S1") & (Bool (Set (Var "r2")) ($#r2_hidden :::"in"::: ) "R2") & (Bool (Set (Var "s2")) ($#r2_hidden :::"in"::: ) "S2") & (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "r1")) "," (Set (Var "r2")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "R") "or" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "s1")) "," (Set (Var "s2")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "S") ")" ) ")" )) ")" )); end; :: deftheorem defines :::"[^"::: PCS_0:def 2 : (Bool "for" (Set (Var "R1")) "," (Set (Var "R2")) "," (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "R1")) "," (Set (Var "R2")) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "S1")) "," (Set (Var "S2")) (Bool "for" (Set (Var "b7")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "R1")) "," (Set (Var "S1")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "R2")) "," (Set (Var "S2")) ($#k2_zfmisc_1 :::":]"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b7")) ($#r1_hidden :::"="::: ) (Set ($#k3_pcs_0 :::"[^"::: ) (Set (Var "R")) "," (Set (Var "S")) ($#k3_pcs_0 :::"^]"::: ) )) "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 "b7"))) "iff" (Bool "ex" (Set (Var "r1")) "," (Set (Var "s1")) "," (Set (Var "r2")) "," (Set (Var "s2")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "r1")) "," (Set (Var "s1")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "r2")) "," (Set (Var "s2")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Var "r1")) ($#r2_hidden :::"in"::: ) (Set (Var "R1"))) & (Bool (Set (Var "s1")) ($#r2_hidden :::"in"::: ) (Set (Var "S1"))) & (Bool (Set (Var "r2")) ($#r2_hidden :::"in"::: ) (Set (Var "R2"))) & (Bool (Set (Var "s2")) ($#r2_hidden :::"in"::: ) (Set (Var "S2"))) & (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "r1")) "," (Set (Var "r2")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R"))) "or" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "s1")) "," (Set (Var "s2")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "S"))) ")" ) ")" )) ")" )) ")" ))))); definitionlet "R1", "R2", "S1", "S2" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "R" be ($#m1_subset_1 :::"Relation":::) "of" (Set (Const "R1")) "," (Set (Const "R2")); let "S" be ($#m1_subset_1 :::"Relation":::) "of" (Set (Const "S1")) "," (Set (Const "S2")); redefine func :::"[^":::"R" "," "S":::"^]"::: means :: PCS_0:def 3 (Bool "for" (Set (Var "r1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "R1" (Bool "for" (Set (Var "r2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "R2" (Bool "for" (Set (Var "s1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "S1" (Bool "for" (Set (Var "s2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "S2" "holds" (Bool "(" (Bool (Set ($#k1_domain_1 :::"["::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "r1")) "," (Set (Var "s1")) ($#k1_domain_1 :::"]"::: ) ) "," (Set ($#k1_domain_1 :::"["::: ) (Set (Var "r2")) "," (Set (Var "s2")) ($#k1_domain_1 :::"]"::: ) ) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "(" (Bool (Set ($#k1_domain_1 :::"["::: ) (Set (Var "r1")) "," (Set (Var "r2")) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "R") "or" (Bool (Set ($#k1_domain_1 :::"["::: ) (Set (Var "s1")) "," (Set (Var "s2")) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "S") ")" ) ")" ))))); end; :: deftheorem defines :::"[^"::: PCS_0:def 3 : (Bool "for" (Set (Var "R1")) "," (Set (Var "R2")) "," (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "R1")) "," (Set (Var "R2")) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "S1")) "," (Set (Var "S2")) (Bool "for" (Set (Var "b7")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "R1")) "," (Set (Var "S1")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "R2")) "," (Set (Var "S2")) ($#k2_zfmisc_1 :::":]"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b7")) ($#r1_hidden :::"="::: ) (Set ($#k3_pcs_0 :::"[^"::: ) (Set (Var "R")) "," (Set (Var "S")) ($#k3_pcs_0 :::"^]"::: ) )) "iff" (Bool "for" (Set (Var "r1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "R1")) (Bool "for" (Set (Var "r2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "R2")) (Bool "for" (Set (Var "s1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "S1")) (Bool "for" (Set (Var "s2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "S2")) "holds" (Bool "(" (Bool (Set ($#k1_domain_1 :::"["::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "r1")) "," (Set (Var "s1")) ($#k1_domain_1 :::"]"::: ) ) "," (Set ($#k1_domain_1 :::"["::: ) (Set (Var "r2")) "," (Set (Var "s2")) ($#k1_domain_1 :::"]"::: ) ) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "b7"))) "iff" (Bool "(" (Bool (Set ($#k1_domain_1 :::"["::: ) (Set (Var "r1")) "," (Set (Var "r2")) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R"))) "or" (Bool (Set ($#k1_domain_1 :::"["::: ) (Set (Var "s1")) "," (Set (Var "s2")) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "S"))) ")" ) ")" ))))) ")" ))))); registrationlet "R1", "S1" be ($#m1_hidden :::"set"::: ) ; let "R" be ($#v1_partfun1 :::"total"::: ) ($#m1_subset_1 :::"Relation":::) "of" (Set (Const "R1")); let "S" be ($#v1_partfun1 :::"total"::: ) ($#m1_subset_1 :::"Relation":::) "of" (Set (Const "S1")); cluster (Set ($#k3_pcs_0 :::"[^"::: ) "R" "," "S" ($#k3_pcs_0 :::"^]"::: ) ) -> ($#v1_partfun1 :::"total"::: ) ; end; registrationlet "R1", "S1" be ($#m1_hidden :::"set"::: ) ; let "R" be ($#v1_relat_2 :::"reflexive"::: ) ($#m1_subset_1 :::"Relation":::) "of" (Set (Const "R1")); let "S" be ($#v1_relat_2 :::"reflexive"::: ) ($#m1_subset_1 :::"Relation":::) "of" (Set (Const "S1")); cluster (Set ($#k3_pcs_0 :::"[^"::: ) "R" "," "S" ($#k3_pcs_0 :::"^]"::: ) ) -> ($#v1_relat_2 :::"reflexive"::: ) ; end; registrationlet "R1", "S1" be ($#m1_hidden :::"set"::: ) ; let "R" be ($#m1_subset_1 :::"Relation":::) "of" (Set (Const "R1")); let "S" be ($#v1_partfun1 :::"total"::: ) ($#v1_relat_2 :::"reflexive"::: ) ($#m1_subset_1 :::"Relation":::) "of" (Set (Const "S1")); cluster (Set ($#k3_pcs_0 :::"[^"::: ) "R" "," "S" ($#k3_pcs_0 :::"^]"::: ) ) -> ($#v1_relat_2 :::"reflexive"::: ) ; end; registrationlet "R1", "S1" be ($#m1_hidden :::"set"::: ) ; let "R" be ($#v1_partfun1 :::"total"::: ) ($#v1_relat_2 :::"reflexive"::: ) ($#m1_subset_1 :::"Relation":::) "of" (Set (Const "R1")); let "S" be ($#m1_subset_1 :::"Relation":::) "of" (Set (Const "S1")); cluster (Set ($#k3_pcs_0 :::"[^"::: ) "R" "," "S" ($#k3_pcs_0 :::"^]"::: ) ) -> ($#v1_relat_2 :::"reflexive"::: ) ; end; registrationlet "R1", "S1" be ($#m1_hidden :::"set"::: ) ; let "R" be ($#v3_relat_2 :::"symmetric"::: ) ($#m1_subset_1 :::"Relation":::) "of" (Set (Const "R1")); let "S" be ($#v3_relat_2 :::"symmetric"::: ) ($#m1_subset_1 :::"Relation":::) "of" (Set (Const "S1")); cluster (Set ($#k3_pcs_0 :::"[^"::: ) "R" "," "S" ($#k3_pcs_0 :::"^]"::: ) ) -> ($#v3_relat_2 :::"symmetric"::: ) ; end; begin registration cluster ($#v2_struct_0 :::"empty"::: ) -> ($#v2_orders_2 :::"total"::: ) for ($#l1_orders_2 :::"RelStr"::: ) ; end; definitionlet "R" be ($#m1_hidden :::"Relation":::); attr "R" is :::"transitive-yielding"::: means :: PCS_0:def 4 (Bool "for" (Set (Var "S")) "being" ($#l1_orders_2 :::"RelStr"::: ) "st" (Bool (Bool (Set (Var "S")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) "R"))) "holds" (Bool (Set (Var "S")) "is" ($#v4_orders_2 :::"transitive"::: ) )); end; :: deftheorem defines :::"transitive-yielding"::: PCS_0:def 4 : (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" (Bool (Set (Var "R")) "is" ($#v1_pcs_0 :::"transitive-yielding"::: ) ) "iff" (Bool "for" (Set (Var "S")) "being" ($#l1_orders_2 :::"RelStr"::: ) "st" (Bool (Bool (Set (Var "S")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "R"))))) "holds" (Bool (Set (Var "S")) "is" ($#v4_orders_2 :::"transitive"::: ) )) ")" )); registration cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_yellow16 :::"Poset-yielding"::: ) -> ($#v1_pcs_0 :::"transitive-yielding"::: ) for ($#m1_hidden :::"set"::: ) ; end; registration cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_yellow16 :::"Poset-yielding"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "I" be ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) "I" ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_partfun1 :::"total"::: ) ($#v1_yellow16 :::"Poset-yielding"::: ) for ($#m1_hidden :::"set"::: ) ; end; definitionlet "I" be ($#m1_hidden :::"set"::: ) ; let "C" be ($#v1_yellow_1 :::"RelStr-yielding"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); func :::"pcs-InternalRels"::: "C" -> ($#m1_hidden :::"ManySortedSet":::) "of" "I" means :: PCS_0:def 5 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) "I")) "holds" (Bool "ex" (Set (Var "P")) "being" ($#l1_orders_2 :::"RelStr"::: ) "st" (Bool "(" (Bool (Set (Var "P")) ($#r1_hidden :::"="::: ) (Set "C" ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "P")))) ")" ))); end; :: deftheorem defines :::"pcs-InternalRels"::: PCS_0:def 5 : (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#v1_yellow_1 :::"RelStr-yielding"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "b3")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k4_pcs_0 :::"pcs-InternalRels"::: ) (Set (Var "C")))) "iff" (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Var "I")))) "holds" (Bool "ex" (Set (Var "P")) "being" ($#l1_orders_2 :::"RelStr"::: ) "st" (Bool "(" (Bool (Set (Var "P")) ($#r1_hidden :::"="::: ) (Set (Set (Var "C")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Set (Var "b3")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "P")))) ")" ))) ")" )))); definitionlet "I" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "C" be ($#v1_yellow_1 :::"RelStr-yielding"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); redefine func :::"pcs-InternalRels"::: "C" means :: PCS_0:def 6 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "I" "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set "(" "C" ($#k3_waybel_3 :::"."::: ) (Set (Var "i")) ")" )))); end; :: deftheorem defines :::"pcs-InternalRels"::: PCS_0:def 6 : (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#v1_yellow_1 :::"RelStr-yielding"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "b3")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k4_pcs_0 :::"pcs-InternalRels"::: ) (Set (Var "C")))) "iff" (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "I")) "holds" (Bool (Set (Set (Var "b3")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set "(" (Set (Var "C")) ($#k3_waybel_3 :::"."::: ) (Set (Var "i")) ")" )))) ")" )))); registrationlet "I" be ($#m1_hidden :::"set"::: ) ; let "C" be ($#v1_yellow_1 :::"RelStr-yielding"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); cluster (Set ($#k4_pcs_0 :::"pcs-InternalRels"::: ) "C") -> ($#v2_funcop_1 :::"Relation-yielding"::: ) ; end; registrationlet "I" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "C" be ($#v1_yellow_1 :::"RelStr-yielding"::: ) ($#v1_pcs_0 :::"transitive-yielding"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); let "i" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "I")); cluster (Set "C" ($#k1_funct_1 :::"."::: ) "i") -> ($#v4_orders_2 :::"transitive"::: ) for ($#l1_orders_2 :::"RelStr"::: ) ; end; begin definitionattr "c1" is :::"strict"::: ; struct :::"TolStr"::: -> ($#l1_struct_0 :::"1-sorted"::: ) ; aggr :::"TolStr":::(# :::"carrier":::, :::"ToleranceRel"::: #) -> ($#l1_pcs_0 :::"TolStr"::: ) ; sel :::"ToleranceRel"::: "c1" -> ($#m1_subset_1 :::"Relation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "c1"); end; definitionlet "P" be ($#l1_pcs_0 :::"TolStr"::: ) ; let "p", "q" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "P")); pred "p" :::"(--)"::: "q" means :: PCS_0:def 7 (Bool (Set ($#k4_tarski :::"["::: ) "p" "," "q" ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_pcs_0 :::"ToleranceRel"::: ) "of" "P")); end; :: deftheorem defines :::"(--)"::: PCS_0:def 7 : (Bool "for" (Set (Var "P")) "being" ($#l1_pcs_0 :::"TolStr"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "P")) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r1_pcs_0 :::"(--)"::: ) (Set (Var "q"))) "iff" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "p")) "," (Set (Var "q")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_pcs_0 :::"ToleranceRel"::: ) "of" (Set (Var "P")))) ")" ))); definitionlet "P" be ($#l1_pcs_0 :::"TolStr"::: ) ; attr "P" is :::"pcs-tol-total"::: means :: PCS_0:def 8 (Bool (Set "the" ($#u1_pcs_0 :::"ToleranceRel"::: ) "of" "P") "is" ($#v1_partfun1 :::"total"::: ) ); attr "P" is :::"pcs-tol-reflexive"::: means :: PCS_0:def 9 (Bool (Set "the" ($#u1_pcs_0 :::"ToleranceRel"::: ) "of" "P") ($#r1_relat_2 :::"is_reflexive_in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "P")); attr "P" is :::"pcs-tol-irreflexive"::: means :: PCS_0:def 10 (Bool (Set "the" ($#u1_pcs_0 :::"ToleranceRel"::: ) "of" "P") ($#r2_relat_2 :::"is_irreflexive_in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "P")); attr "P" is :::"pcs-tol-symmetric"::: means :: PCS_0:def 11 (Bool (Set "the" ($#u1_pcs_0 :::"ToleranceRel"::: ) "of" "P") ($#r3_relat_2 :::"is_symmetric_in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "P")); end; :: deftheorem defines :::"pcs-tol-total"::: PCS_0:def 8 : (Bool "for" (Set (Var "P")) "being" ($#l1_pcs_0 :::"TolStr"::: ) "holds" (Bool "(" (Bool (Set (Var "P")) "is" ($#v3_pcs_0 :::"pcs-tol-total"::: ) ) "iff" (Bool (Set "the" ($#u1_pcs_0 :::"ToleranceRel"::: ) "of" (Set (Var "P"))) "is" ($#v1_partfun1 :::"total"::: ) ) ")" )); :: deftheorem defines :::"pcs-tol-reflexive"::: PCS_0:def 9 : (Bool "for" (Set (Var "P")) "being" ($#l1_pcs_0 :::"TolStr"::: ) "holds" (Bool "(" (Bool (Set (Var "P")) "is" ($#v4_pcs_0 :::"pcs-tol-reflexive"::: ) ) "iff" (Bool (Set "the" ($#u1_pcs_0 :::"ToleranceRel"::: ) "of" (Set (Var "P"))) ($#r1_relat_2 :::"is_reflexive_in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "P")))) ")" )); :: deftheorem defines :::"pcs-tol-irreflexive"::: PCS_0:def 10 : (Bool "for" (Set (Var "P")) "being" ($#l1_pcs_0 :::"TolStr"::: ) "holds" (Bool "(" (Bool (Set (Var "P")) "is" ($#v5_pcs_0 :::"pcs-tol-irreflexive"::: ) ) "iff" (Bool (Set "the" ($#u1_pcs_0 :::"ToleranceRel"::: ) "of" (Set (Var "P"))) ($#r2_relat_2 :::"is_irreflexive_in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "P")))) ")" )); :: deftheorem defines :::"pcs-tol-symmetric"::: PCS_0:def 11 : (Bool "for" (Set (Var "P")) "being" ($#l1_pcs_0 :::"TolStr"::: ) "holds" (Bool "(" (Bool (Set (Var "P")) "is" ($#v6_pcs_0 :::"pcs-tol-symmetric"::: ) ) "iff" (Bool (Set "the" ($#u1_pcs_0 :::"ToleranceRel"::: ) "of" (Set (Var "P"))) ($#r3_relat_2 :::"is_symmetric_in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "P")))) ")" )); definitionfunc :::"emptyTolStr"::: -> ($#l1_pcs_0 :::"TolStr"::: ) equals :: PCS_0:def 12 (Set ($#g1_pcs_0 :::"TolStr"::: ) "(#" (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set "(" ($#k1_partit_2 :::"{}"::: ) "(" (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ")" ) "#)" ); end; :: deftheorem defines :::"emptyTolStr"::: PCS_0:def 12 : (Bool (Set ($#k5_pcs_0 :::"emptyTolStr"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#g1_pcs_0 :::"TolStr"::: ) "(#" (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set "(" ($#k1_partit_2 :::"{}"::: ) "(" (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ")" ) "#)" )); registration cluster (Set ($#k5_pcs_0 :::"emptyTolStr"::: ) ) -> ($#v2_struct_0 :::"empty"::: ) ($#v2_pcs_0 :::"strict"::: ) ; end; theorem :: PCS_0:2 (Bool "for" (Set (Var "P")) "being" ($#l1_pcs_0 :::"TolStr"::: ) "st" (Bool (Bool (Set (Var "P")) "is" ($#v2_struct_0 :::"empty"::: ) )) "holds" (Bool (Set ($#g1_pcs_0 :::"TolStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "P"))) "," (Set "the" ($#u1_pcs_0 :::"ToleranceRel"::: ) "of" (Set (Var "P"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#k5_pcs_0 :::"emptyTolStr"::: ) ))) ; registration cluster ($#v4_pcs_0 :::"pcs-tol-reflexive"::: ) -> ($#v3_pcs_0 :::"pcs-tol-total"::: ) for ($#l1_pcs_0 :::"TolStr"::: ) ; end; registration cluster ($#v2_struct_0 :::"empty"::: ) -> ($#v4_pcs_0 :::"pcs-tol-reflexive"::: ) ($#v5_pcs_0 :::"pcs-tol-irreflexive"::: ) ($#v6_pcs_0 :::"pcs-tol-symmetric"::: ) for ($#l1_pcs_0 :::"TolStr"::: ) ; end; registration cluster ($#v2_struct_0 :::"empty"::: ) ($#v2_pcs_0 :::"strict"::: ) for ($#l1_pcs_0 :::"TolStr"::: ) ; end; registrationlet "P" be ($#v3_pcs_0 :::"pcs-tol-total"::: ) ($#l1_pcs_0 :::"TolStr"::: ) ; cluster (Set "the" ($#u1_pcs_0 :::"ToleranceRel"::: ) "of" "P") -> ($#v1_partfun1 :::"total"::: ) ; end; registrationlet "P" be ($#v4_pcs_0 :::"pcs-tol-reflexive"::: ) ($#l1_pcs_0 :::"TolStr"::: ) ; cluster (Set "the" ($#u1_pcs_0 :::"ToleranceRel"::: ) "of" "P") -> ($#v1_relat_2 :::"reflexive"::: ) ; end; registrationlet "P" be ($#v5_pcs_0 :::"pcs-tol-irreflexive"::: ) ($#l1_pcs_0 :::"TolStr"::: ) ; cluster (Set "the" ($#u1_pcs_0 :::"ToleranceRel"::: ) "of" "P") -> ($#v2_relat_2 :::"irreflexive"::: ) ; end; registrationlet "P" be ($#v6_pcs_0 :::"pcs-tol-symmetric"::: ) ($#l1_pcs_0 :::"TolStr"::: ) ; cluster (Set "the" ($#u1_pcs_0 :::"ToleranceRel"::: ) "of" "P") -> ($#v3_relat_2 :::"symmetric"::: ) ; end; registrationlet "L" be ($#v3_pcs_0 :::"pcs-tol-total"::: ) ($#l1_pcs_0 :::"TolStr"::: ) ; cluster (Set ($#g1_pcs_0 :::"TolStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L") "," (Set "the" ($#u1_pcs_0 :::"ToleranceRel"::: ) "of" "L") "#)" ) -> ($#v3_pcs_0 :::"pcs-tol-total"::: ) ; end; definitionlet "P" be ($#v6_pcs_0 :::"pcs-tol-symmetric"::: ) ($#l1_pcs_0 :::"TolStr"::: ) ; let "p", "q" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "P")); :: original: :::"(--)"::: redefine pred "p" :::"(--)"::: "q"; symmetry (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Const "P")) "st" (Bool (Bool ((Set (Const "P")) "," (Set (Var "b1")) "," (Set (Var "b2"))))) "holds" (Bool ((Set (Const "P")) "," (Set (Var "b2")) "," (Set (Var "b1"))))) ; end; registrationlet "D" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#g1_pcs_0 :::"TolStr"::: ) "(#" "D" "," (Set "(" ($#k1_eqrel_1 :::"nabla"::: ) "D" ")" ) "#)" ) -> ($#v4_pcs_0 :::"pcs-tol-reflexive"::: ) ($#v6_pcs_0 :::"pcs-tol-symmetric"::: ) ; end; registrationlet "D" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#g1_pcs_0 :::"TolStr"::: ) "(#" "D" "," (Set "(" ($#k1_partit_2 :::"{}"::: ) "(" "D" "," "D" ")" ")" ) "#)" ) -> ($#v5_pcs_0 :::"pcs-tol-irreflexive"::: ) ($#v6_pcs_0 :::"pcs-tol-symmetric"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_pcs_0 :::"strict"::: ) ($#v4_pcs_0 :::"pcs-tol-reflexive"::: ) ($#v6_pcs_0 :::"pcs-tol-symmetric"::: ) for ($#l1_pcs_0 :::"TolStr"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_pcs_0 :::"strict"::: ) ($#v5_pcs_0 :::"pcs-tol-irreflexive"::: ) ($#v6_pcs_0 :::"pcs-tol-symmetric"::: ) for ($#l1_pcs_0 :::"TolStr"::: ) ; end; definitionlet "R" be ($#m1_hidden :::"Relation":::); attr "R" is :::"TolStr-yielding"::: means :: PCS_0:def 13 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "P")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) "R"))) "holds" (Bool (Set (Var "P")) "is" ($#l1_pcs_0 :::"TolStr"::: ) )); end; :: deftheorem defines :::"TolStr-yielding"::: PCS_0:def 13 : (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" (Bool (Set (Var "R")) "is" ($#v7_pcs_0 :::"TolStr-yielding"::: ) ) "iff" (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "P")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "R"))))) "holds" (Bool (Set (Var "P")) "is" ($#l1_pcs_0 :::"TolStr"::: ) )) ")" )); definitionlet "f" be ($#m1_hidden :::"Function":::); redefine attr "f" is :::"TolStr-yielding"::: means :: PCS_0:def 14 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "f"))) "holds" (Bool (Set "f" ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) "is" ($#l1_pcs_0 :::"TolStr"::: ) )); end; :: deftheorem defines :::"TolStr-yielding"::: PCS_0:def 14 : (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v7_pcs_0 :::"TolStr-yielding"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) "is" ($#l1_pcs_0 :::"TolStr"::: ) )) ")" )); definitionlet "I" be ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); :: original: :::"TolStr-yielding"::: redefine attr "f" is :::"TolStr-yielding"::: means :: PCS_0:def 15 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "I")) "holds" (Bool (Set "f" ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) "is" ($#l1_pcs_0 :::"TolStr"::: ) )); end; :: deftheorem defines :::"TolStr-yielding"::: PCS_0:def 15 : (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v7_pcs_0 :::"TolStr-yielding"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "I")))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) "is" ($#l1_pcs_0 :::"TolStr"::: ) )) ")" ))); definitionlet "R" be ($#m1_hidden :::"Relation":::); attr "R" is :::"pcs-tol-reflexive-yielding"::: means :: PCS_0:def 16 (Bool "for" (Set (Var "S")) "being" ($#l1_pcs_0 :::"TolStr"::: ) "st" (Bool (Bool (Set (Var "S")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) "R"))) "holds" (Bool (Set (Var "S")) "is" ($#v4_pcs_0 :::"pcs-tol-reflexive"::: ) )); attr "R" is :::"pcs-tol-irreflexive-yielding"::: means :: PCS_0:def 17 (Bool "for" (Set (Var "S")) "being" ($#l1_pcs_0 :::"TolStr"::: ) "st" (Bool (Bool (Set (Var "S")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) "R"))) "holds" (Bool (Set (Var "S")) "is" ($#v5_pcs_0 :::"pcs-tol-irreflexive"::: ) )); attr "R" is :::"pcs-tol-symmetric-yielding"::: means :: PCS_0:def 18 (Bool "for" (Set (Var "S")) "being" ($#l1_pcs_0 :::"TolStr"::: ) "st" (Bool (Bool (Set (Var "S")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) "R"))) "holds" (Bool (Set (Var "S")) "is" ($#v6_pcs_0 :::"pcs-tol-symmetric"::: ) )); end; :: deftheorem defines :::"pcs-tol-reflexive-yielding"::: PCS_0:def 16 : (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" (Bool (Set (Var "R")) "is" ($#v9_pcs_0 :::"pcs-tol-reflexive-yielding"::: ) ) "iff" (Bool "for" (Set (Var "S")) "being" ($#l1_pcs_0 :::"TolStr"::: ) "st" (Bool (Bool (Set (Var "S")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "R"))))) "holds" (Bool (Set (Var "S")) "is" ($#v4_pcs_0 :::"pcs-tol-reflexive"::: ) )) ")" )); :: deftheorem defines :::"pcs-tol-irreflexive-yielding"::: PCS_0:def 17 : (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" (Bool (Set (Var "R")) "is" ($#v10_pcs_0 :::"pcs-tol-irreflexive-yielding"::: ) ) "iff" (Bool "for" (Set (Var "S")) "being" ($#l1_pcs_0 :::"TolStr"::: ) "st" (Bool (Bool (Set (Var "S")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "R"))))) "holds" (Bool (Set (Var "S")) "is" ($#v5_pcs_0 :::"pcs-tol-irreflexive"::: ) )) ")" )); :: deftheorem defines :::"pcs-tol-symmetric-yielding"::: PCS_0:def 18 : (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" (Bool (Set (Var "R")) "is" ($#v11_pcs_0 :::"pcs-tol-symmetric-yielding"::: ) ) "iff" (Bool "for" (Set (Var "S")) "being" ($#l1_pcs_0 :::"TolStr"::: ) "st" (Bool (Bool (Set (Var "S")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "R"))))) "holds" (Bool (Set (Var "S")) "is" ($#v6_pcs_0 :::"pcs-tol-symmetric"::: ) )) ")" )); registration cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_xboole_0 :::"empty"::: ) -> ($#v9_pcs_0 :::"pcs-tol-reflexive-yielding"::: ) ($#v10_pcs_0 :::"pcs-tol-irreflexive-yielding"::: ) ($#v11_pcs_0 :::"pcs-tol-symmetric-yielding"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "I" be ($#m1_hidden :::"set"::: ) ; let "P" be ($#l1_pcs_0 :::"TolStr"::: ) ; cluster (Set "I" ($#k2_funcop_1 :::"-->"::: ) "P") -> () for ($#m1_hidden :::"ManySortedSet":::) "of" "I"; end; registrationlet "I" be ($#m1_hidden :::"set"::: ) ; let "P" be ($#v4_pcs_0 :::"pcs-tol-reflexive"::: ) ($#l1_pcs_0 :::"TolStr"::: ) ; cluster (Set "I" ($#k2_funcop_1 :::"-->"::: ) "P") -> ($#v9_pcs_0 :::"pcs-tol-reflexive-yielding"::: ) for ($#m1_hidden :::"ManySortedSet":::) "of" "I"; end; registrationlet "I" be ($#m1_hidden :::"set"::: ) ; let "P" be ($#v5_pcs_0 :::"pcs-tol-irreflexive"::: ) ($#l1_pcs_0 :::"TolStr"::: ) ; cluster (Set "I" ($#k2_funcop_1 :::"-->"::: ) "P") -> ($#v10_pcs_0 :::"pcs-tol-irreflexive-yielding"::: ) for ($#m1_hidden :::"ManySortedSet":::) "of" "I"; end; registrationlet "I" be ($#m1_hidden :::"set"::: ) ; let "P" be ($#v6_pcs_0 :::"pcs-tol-symmetric"::: ) ($#l1_pcs_0 :::"TolStr"::: ) ; cluster (Set "I" ($#k2_funcop_1 :::"-->"::: ) "P") -> ($#v11_pcs_0 :::"pcs-tol-symmetric-yielding"::: ) for ($#m1_hidden :::"ManySortedSet":::) "of" "I"; end; registration cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v7_pcs_0 :::"TolStr-yielding"::: ) -> ($#v2_pralg_1 :::"1-sorted-yielding"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "I" be ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) "I" ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_partfun1 :::"total"::: ) () ($#v9_pcs_0 :::"pcs-tol-reflexive-yielding"::: ) ($#v11_pcs_0 :::"pcs-tol-symmetric-yielding"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "I" be ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) "I" ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_partfun1 :::"total"::: ) () ($#v10_pcs_0 :::"pcs-tol-irreflexive-yielding"::: ) ($#v11_pcs_0 :::"pcs-tol-symmetric-yielding"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "I" be ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) "I" ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_partfun1 :::"total"::: ) () for ($#m1_hidden :::"set"::: ) ; end; definitionlet "I" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "C" be () ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); let "i" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "I")); :: original: :::"."::: redefine func "C" :::"."::: "i" -> ($#l1_pcs_0 :::"TolStr"::: ) ; end; definitionlet "I" be ($#m1_hidden :::"set"::: ) ; let "C" be () ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); func :::"pcs-ToleranceRels"::: "C" -> ($#m1_hidden :::"ManySortedSet":::) "of" "I" means :: PCS_0:def 19 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) "I")) "holds" (Bool "ex" (Set (Var "P")) "being" ($#l1_pcs_0 :::"TolStr"::: ) "st" (Bool "(" (Bool (Set (Var "P")) ($#r1_hidden :::"="::: ) (Set "C" ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_pcs_0 :::"ToleranceRel"::: ) "of" (Set (Var "P")))) ")" ))); end; :: deftheorem defines :::"pcs-ToleranceRels"::: PCS_0:def 19 : (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" () ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "b3")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k7_pcs_0 :::"pcs-ToleranceRels"::: ) (Set (Var "C")))) "iff" (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Var "I")))) "holds" (Bool "ex" (Set (Var "P")) "being" ($#l1_pcs_0 :::"TolStr"::: ) "st" (Bool "(" (Bool (Set (Var "P")) ($#r1_hidden :::"="::: ) (Set (Set (Var "C")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Set (Var "b3")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_pcs_0 :::"ToleranceRel"::: ) "of" (Set (Var "P")))) ")" ))) ")" )))); definitionlet "I" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "C" be () ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); redefine func :::"pcs-ToleranceRels"::: "C" means :: PCS_0:def 20 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "I" "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_pcs_0 :::"ToleranceRel"::: ) "of" (Set "(" "C" ($#k6_pcs_0 :::"."::: ) (Set (Var "i")) ")" )))); end; :: deftheorem defines :::"pcs-ToleranceRels"::: PCS_0:def 20 : (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" () ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "b3")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k7_pcs_0 :::"pcs-ToleranceRels"::: ) (Set (Var "C")))) "iff" (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "I")) "holds" (Bool (Set (Set (Var "b3")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_pcs_0 :::"ToleranceRel"::: ) "of" (Set "(" (Set (Var "C")) ($#k6_pcs_0 :::"."::: ) (Set (Var "i")) ")" )))) ")" )))); registrationlet "I" be ($#m1_hidden :::"set"::: ) ; let "C" be () ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); cluster (Set ($#k7_pcs_0 :::"pcs-ToleranceRels"::: ) "C") -> ($#v2_funcop_1 :::"Relation-yielding"::: ) ; end; registrationlet "I" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "C" be () ($#v9_pcs_0 :::"pcs-tol-reflexive-yielding"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); let "i" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "I")); cluster (Set "C" ($#k1_funct_1 :::"."::: ) "i") -> ($#v4_pcs_0 :::"pcs-tol-reflexive"::: ) for ($#l1_pcs_0 :::"TolStr"::: ) ; end; registrationlet "I" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "C" be () ($#v10_pcs_0 :::"pcs-tol-irreflexive-yielding"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); let "i" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "I")); cluster (Set "C" ($#k1_funct_1 :::"."::: ) "i") -> ($#v5_pcs_0 :::"pcs-tol-irreflexive"::: ) for ($#l1_pcs_0 :::"TolStr"::: ) ; end; registrationlet "I" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "C" be () ($#v11_pcs_0 :::"pcs-tol-symmetric-yielding"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); let "i" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "I")); cluster (Set "C" ($#k1_funct_1 :::"."::: ) "i") -> ($#v6_pcs_0 :::"pcs-tol-symmetric"::: ) for ($#l1_pcs_0 :::"TolStr"::: ) ; end; theorem :: PCS_0:3 (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#l1_pcs_0 :::"TolStr"::: ) "st" (Bool (Bool (Set ($#g1_pcs_0 :::"TolStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "P"))) "," (Set "the" ($#u1_pcs_0 :::"ToleranceRel"::: ) "of" (Set (Var "P"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g1_pcs_0 :::"TolStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Q"))) "," (Set "the" ($#u1_pcs_0 :::"ToleranceRel"::: ) "of" (Set (Var "Q"))) "#)" )) & (Bool (Set (Var "P")) "is" ($#v4_pcs_0 :::"pcs-tol-reflexive"::: ) )) "holds" (Bool (Set (Var "Q")) "is" ($#v4_pcs_0 :::"pcs-tol-reflexive"::: ) )) ; theorem :: PCS_0:4 (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#l1_pcs_0 :::"TolStr"::: ) "st" (Bool (Bool (Set ($#g1_pcs_0 :::"TolStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "P"))) "," (Set "the" ($#u1_pcs_0 :::"ToleranceRel"::: ) "of" (Set (Var "P"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g1_pcs_0 :::"TolStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Q"))) "," (Set "the" ($#u1_pcs_0 :::"ToleranceRel"::: ) "of" (Set (Var "Q"))) "#)" )) & (Bool (Set (Var "P")) "is" ($#v5_pcs_0 :::"pcs-tol-irreflexive"::: ) )) "holds" (Bool (Set (Var "Q")) "is" ($#v5_pcs_0 :::"pcs-tol-irreflexive"::: ) )) ; theorem :: PCS_0:5 (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#l1_pcs_0 :::"TolStr"::: ) "st" (Bool (Bool (Set ($#g1_pcs_0 :::"TolStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "P"))) "," (Set "the" ($#u1_pcs_0 :::"ToleranceRel"::: ) "of" (Set (Var "P"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g1_pcs_0 :::"TolStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Q"))) "," (Set "the" ($#u1_pcs_0 :::"ToleranceRel"::: ) "of" (Set (Var "Q"))) "#)" )) & (Bool (Set (Var "P")) "is" ($#v6_pcs_0 :::"pcs-tol-symmetric"::: ) )) "holds" (Bool (Set (Var "Q")) "is" ($#v6_pcs_0 :::"pcs-tol-symmetric"::: ) )) ; definitionlet "P", "Q" be ($#l1_pcs_0 :::"TolStr"::: ) ; func :::"[^":::"P" "," "Q":::"^]"::: -> ($#l1_pcs_0 :::"TolStr"::: ) equals :: PCS_0:def 21 (Set ($#g1_pcs_0 :::"TolStr"::: ) "(#" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "P") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "Q") ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k3_pcs_0 :::"[^"::: ) (Set "the" ($#u1_pcs_0 :::"ToleranceRel"::: ) "of" "P") "," (Set "the" ($#u1_pcs_0 :::"ToleranceRel"::: ) "of" "Q") ($#k3_pcs_0 :::"^]"::: ) ) "#)" ); end; :: deftheorem defines :::"[^"::: PCS_0:def 21 : (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#l1_pcs_0 :::"TolStr"::: ) "holds" (Bool (Set ($#k8_pcs_0 :::"[^"::: ) (Set (Var "P")) "," (Set (Var "Q")) ($#k8_pcs_0 :::"^]"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#g1_pcs_0 :::"TolStr"::: ) "(#" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "P"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Q"))) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k3_pcs_0 :::"[^"::: ) (Set "the" ($#u1_pcs_0 :::"ToleranceRel"::: ) "of" (Set (Var "P"))) "," (Set "the" ($#u1_pcs_0 :::"ToleranceRel"::: ) "of" (Set (Var "Q"))) ($#k3_pcs_0 :::"^]"::: ) ) "#)" ))); notationlet "P", "Q" be ($#l1_pcs_0 :::"TolStr"::: ) ; let "p" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "P")); let "q" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "Q")); synonym :::"[^":::"p" "," "q":::"^]"::: for :::"[":::"P" "," "Q":::"]":::; end; definitionlet "P", "Q" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pcs_0 :::"TolStr"::: ) ; let "p" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "P")); let "q" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "Q")); :: original: :::"[^"::: redefine func :::"[^":::"p" "," "q":::"^]"::: -> ($#m1_subset_1 :::"Element":::) "of" (Set ($#k8_pcs_0 :::"[^"::: ) "P" "," "Q" ($#k8_pcs_0 :::"^]"::: ) ); end; notationlet "P", "Q" be ($#l1_pcs_0 :::"TolStr"::: ) ; let "p" be ($#m1_subset_1 :::"Element":::) "of" (Set ($#k8_pcs_0 :::"[^"::: ) (Set (Const "P")) "," (Set (Const "Q")) ($#k8_pcs_0 :::"^]"::: ) ); synonym "p" :::"^`1"::: for "P" :::"`1"::: ; synonym "p" :::"^`2"::: for "P" :::"`2"::: ; end; definitionlet "P", "Q" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pcs_0 :::"TolStr"::: ) ; let "p" be ($#m1_subset_1 :::"Element":::) "of" (Set ($#k8_pcs_0 :::"[^"::: ) (Set (Const "P")) "," (Set (Const "Q")) ($#k8_pcs_0 :::"^]"::: ) ); :: original: :::"^`1"::: redefine func "p" :::"^`1"::: -> ($#m1_subset_1 :::"Element":::) "of" "P"; :: original: :::"^`2"::: redefine func "p" :::"^`2"::: -> ($#m1_subset_1 :::"Element":::) "of" "Q"; end; theorem :: PCS_0:6 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pcs_0 :::"TolStr"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S1")) (Bool "for" (Set (Var "b")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S2")) "holds" (Bool "(" (Bool (Set ($#k9_pcs_0 :::"[^"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k9_pcs_0 :::"^]"::: ) ) ($#r1_pcs_0 :::"(--)"::: ) (Set ($#k9_pcs_0 :::"[^"::: ) (Set (Var "c")) "," (Set (Var "d")) ($#k9_pcs_0 :::"^]"::: ) )) "iff" (Bool "(" (Bool (Set (Var "a")) ($#r1_pcs_0 :::"(--)"::: ) (Set (Var "c"))) "or" (Bool (Set (Var "b")) ($#r1_pcs_0 :::"(--)"::: ) (Set (Var "d"))) ")" ) ")" )))) ; theorem :: PCS_0:7 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pcs_0 :::"TolStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k8_pcs_0 :::"[^"::: ) (Set (Var "S1")) "," (Set (Var "S2")) ($#k8_pcs_0 :::"^]"::: ) ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_pcs_0 :::"(--)"::: ) (Set (Var "y"))) "iff" (Bool "(" (Bool (Set (Set (Var "x")) ($#k10_pcs_0 :::"^`1"::: ) ) ($#r1_pcs_0 :::"(--)"::: ) (Set (Set (Var "y")) ($#k10_pcs_0 :::"^`1"::: ) )) "or" (Bool (Set (Set (Var "x")) ($#k11_pcs_0 :::"^`2"::: ) ) ($#r1_pcs_0 :::"(--)"::: ) (Set (Set (Var "y")) ($#k11_pcs_0 :::"^`2"::: ) )) ")" ) ")" ))) ; registrationlet "P" be ($#l1_pcs_0 :::"TolStr"::: ) ; let "Q" be ($#v4_pcs_0 :::"pcs-tol-reflexive"::: ) ($#l1_pcs_0 :::"TolStr"::: ) ; cluster (Set ($#k8_pcs_0 :::"[^"::: ) "P" "," "Q" ($#k8_pcs_0 :::"^]"::: ) ) -> ($#v4_pcs_0 :::"pcs-tol-reflexive"::: ) ; end; registrationlet "P" be ($#v4_pcs_0 :::"pcs-tol-reflexive"::: ) ($#l1_pcs_0 :::"TolStr"::: ) ; let "Q" be ($#l1_pcs_0 :::"TolStr"::: ) ; cluster (Set ($#k8_pcs_0 :::"[^"::: ) "P" "," "Q" ($#k8_pcs_0 :::"^]"::: ) ) -> ($#v4_pcs_0 :::"pcs-tol-reflexive"::: ) ; end; registrationlet "P", "Q" be ($#v6_pcs_0 :::"pcs-tol-symmetric"::: ) ($#l1_pcs_0 :::"TolStr"::: ) ; cluster (Set ($#k8_pcs_0 :::"[^"::: ) "P" "," "Q" ($#k8_pcs_0 :::"^]"::: ) ) -> ($#v6_pcs_0 :::"pcs-tol-symmetric"::: ) ; end; begin definitionattr "c1" is :::"strict"::: ; struct :::"pcs-Str"::: -> ($#l1_orders_2 :::"RelStr"::: ) "," ($#l1_pcs_0 :::"TolStr"::: ) ; aggr :::"pcs-Str":::(# :::"carrier":::, :::"InternalRel":::, :::"ToleranceRel"::: #) -> ($#l2_pcs_0 :::"pcs-Str"::: ) ; end; definitionlet "P" be ($#l2_pcs_0 :::"pcs-Str"::: ) ; attr "P" is :::"pcs-compatible"::: means :: PCS_0:def 22 (Bool "for" (Set (Var "p")) "," (Set (Var "p9")) "," (Set (Var "q")) "," (Set (Var "q9")) "being" ($#m1_subset_1 :::"Element":::) "of" "P" "st" (Bool (Bool (Set (Var "p")) ($#r1_pcs_0 :::"(--)"::: ) (Set (Var "q"))) & (Bool (Set (Var "p9")) ($#r1_orders_2 :::"<="::: ) (Set (Var "p"))) & (Bool (Set (Var "q9")) ($#r1_orders_2 :::"<="::: ) (Set (Var "q")))) "holds" (Bool (Set (Var "p9")) ($#r1_pcs_0 :::"(--)"::: ) (Set (Var "q9")))); end; :: deftheorem defines :::"pcs-compatible"::: PCS_0:def 22 : (Bool "for" (Set (Var "P")) "being" ($#l2_pcs_0 :::"pcs-Str"::: ) "holds" (Bool "(" (Bool (Set (Var "P")) "is" ($#v13_pcs_0 :::"pcs-compatible"::: ) ) "iff" (Bool "for" (Set (Var "p")) "," (Set (Var "p9")) "," (Set (Var "q")) "," (Set (Var "q9")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "P")) "st" (Bool (Bool (Set (Var "p")) ($#r1_pcs_0 :::"(--)"::: ) (Set (Var "q"))) & (Bool (Set (Var "p9")) ($#r1_orders_2 :::"<="::: ) (Set (Var "p"))) & (Bool (Set (Var "q9")) ($#r1_orders_2 :::"<="::: ) (Set (Var "q")))) "holds" (Bool (Set (Var "p9")) ($#r1_pcs_0 :::"(--)"::: ) (Set (Var "q9")))) ")" )); definitionlet "P" be ($#l2_pcs_0 :::"pcs-Str"::: ) ; attr "P" is :::"pcs-like"::: means :: PCS_0:def 23 (Bool "(" (Bool "P" "is" ($#v3_orders_2 :::"reflexive"::: ) ) & (Bool "P" "is" ($#v4_orders_2 :::"transitive"::: ) ) & (Bool "P" "is" ($#v4_pcs_0 :::"pcs-tol-reflexive"::: ) ) & (Bool "P" "is" ($#v6_pcs_0 :::"pcs-tol-symmetric"::: ) ) & (Bool "P" "is" ($#v13_pcs_0 :::"pcs-compatible"::: ) ) ")" ); attr "P" is :::"anti-pcs-like"::: means :: PCS_0:def 24 (Bool "(" (Bool "P" "is" ($#v3_orders_2 :::"reflexive"::: ) ) & (Bool "P" "is" ($#v4_orders_2 :::"transitive"::: ) ) & (Bool "P" "is" ($#v5_pcs_0 :::"pcs-tol-irreflexive"::: ) ) & (Bool "P" "is" ($#v6_pcs_0 :::"pcs-tol-symmetric"::: ) ) & (Bool "P" "is" ($#v13_pcs_0 :::"pcs-compatible"::: ) ) ")" ); end; :: deftheorem defines :::"pcs-like"::: PCS_0:def 23 : (Bool "for" (Set (Var "P")) "being" ($#l2_pcs_0 :::"pcs-Str"::: ) "holds" (Bool "(" (Bool (Set (Var "P")) "is" ($#v14_pcs_0 :::"pcs-like"::: ) ) "iff" (Bool "(" (Bool (Set (Var "P")) "is" ($#v3_orders_2 :::"reflexive"::: ) ) & (Bool (Set (Var "P")) "is" ($#v4_orders_2 :::"transitive"::: ) ) & (Bool (Set (Var "P")) "is" ($#v4_pcs_0 :::"pcs-tol-reflexive"::: ) ) & (Bool (Set (Var "P")) "is" ($#v6_pcs_0 :::"pcs-tol-symmetric"::: ) ) & (Bool (Set (Var "P")) "is" ($#v13_pcs_0 :::"pcs-compatible"::: ) ) ")" ) ")" )); :: deftheorem defines :::"anti-pcs-like"::: PCS_0:def 24 : (Bool "for" (Set (Var "P")) "being" ($#l2_pcs_0 :::"pcs-Str"::: ) "holds" (Bool "(" (Bool (Set (Var "P")) "is" ($#v15_pcs_0 :::"anti-pcs-like"::: ) ) "iff" (Bool "(" (Bool (Set (Var "P")) "is" ($#v3_orders_2 :::"reflexive"::: ) ) & (Bool (Set (Var "P")) "is" ($#v4_orders_2 :::"transitive"::: ) ) & (Bool (Set (Var "P")) "is" ($#v5_pcs_0 :::"pcs-tol-irreflexive"::: ) ) & (Bool (Set (Var "P")) "is" ($#v6_pcs_0 :::"pcs-tol-symmetric"::: ) ) & (Bool (Set (Var "P")) "is" ($#v13_pcs_0 :::"pcs-compatible"::: ) ) ")" ) ")" )); registration cluster ($#v14_pcs_0 :::"pcs-like"::: ) -> ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#v4_pcs_0 :::"pcs-tol-reflexive"::: ) ($#v6_pcs_0 :::"pcs-tol-symmetric"::: ) ($#v13_pcs_0 :::"pcs-compatible"::: ) for ($#l2_pcs_0 :::"pcs-Str"::: ) ; cluster ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#v4_pcs_0 :::"pcs-tol-reflexive"::: ) ($#v6_pcs_0 :::"pcs-tol-symmetric"::: ) ($#v13_pcs_0 :::"pcs-compatible"::: ) -> ($#v14_pcs_0 :::"pcs-like"::: ) for ($#l2_pcs_0 :::"pcs-Str"::: ) ; cluster ($#v15_pcs_0 :::"anti-pcs-like"::: ) -> ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#v5_pcs_0 :::"pcs-tol-irreflexive"::: ) ($#v6_pcs_0 :::"pcs-tol-symmetric"::: ) ($#v13_pcs_0 :::"pcs-compatible"::: ) for ($#l2_pcs_0 :::"pcs-Str"::: ) ; cluster ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#v5_pcs_0 :::"pcs-tol-irreflexive"::: ) ($#v6_pcs_0 :::"pcs-tol-symmetric"::: ) ($#v13_pcs_0 :::"pcs-compatible"::: ) -> ($#v15_pcs_0 :::"anti-pcs-like"::: ) for ($#l2_pcs_0 :::"pcs-Str"::: ) ; end; definitionlet "D" be ($#m1_hidden :::"set"::: ) ; func :::"pcs-total"::: "D" -> ($#l2_pcs_0 :::"pcs-Str"::: ) equals :: PCS_0:def 25 (Set ($#g2_pcs_0 :::"pcs-Str"::: ) "(#" "D" "," (Set "(" ($#k1_eqrel_1 :::"nabla"::: ) "D" ")" ) "," (Set "(" ($#k1_eqrel_1 :::"nabla"::: ) "D" ")" ) "#)" ); end; :: deftheorem defines :::"pcs-total"::: PCS_0:def 25 : (Bool "for" (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k12_pcs_0 :::"pcs-total"::: ) (Set (Var "D"))) ($#r1_hidden :::"="::: ) (Set ($#g2_pcs_0 :::"pcs-Str"::: ) "(#" (Set (Var "D")) "," (Set "(" ($#k1_eqrel_1 :::"nabla"::: ) (Set (Var "D")) ")" ) "," (Set "(" ($#k1_eqrel_1 :::"nabla"::: ) (Set (Var "D")) ")" ) "#)" ))); registrationlet "D" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k12_pcs_0 :::"pcs-total"::: ) "D") -> ($#v12_pcs_0 :::"strict"::: ) ; end; registrationlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k12_pcs_0 :::"pcs-total"::: ) "D") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ; end; registrationlet "D" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k12_pcs_0 :::"pcs-total"::: ) "D") -> ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#v4_pcs_0 :::"pcs-tol-reflexive"::: ) ($#v6_pcs_0 :::"pcs-tol-symmetric"::: ) ; end; registrationlet "D" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k12_pcs_0 :::"pcs-total"::: ) "D") -> ($#v14_pcs_0 :::"pcs-like"::: ) ; end; registrationlet "D" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#g2_pcs_0 :::"pcs-Str"::: ) "(#" "D" "," (Set "(" ($#k1_eqrel_1 :::"nabla"::: ) "D" ")" ) "," (Set "(" ($#k1_partit_2 :::"{}"::: ) "(" "D" "," "D" ")" ")" ) "#)" ) -> ($#v15_pcs_0 :::"anti-pcs-like"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v12_pcs_0 :::"strict"::: ) ($#v14_pcs_0 :::"pcs-like"::: ) for ($#l2_pcs_0 :::"pcs-Str"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v12_pcs_0 :::"strict"::: ) ($#v15_pcs_0 :::"anti-pcs-like"::: ) for ($#l2_pcs_0 :::"pcs-Str"::: ) ; end; definitionmode pcs is ($#v14_pcs_0 :::"pcs-like"::: ) ($#l2_pcs_0 :::"pcs-Str"::: ) ; mode anti-pcs is ($#v15_pcs_0 :::"anti-pcs-like"::: ) ($#l2_pcs_0 :::"pcs-Str"::: ) ; end; definitionfunc :::"pcs-empty"::: -> ($#l2_pcs_0 :::"pcs-Str"::: ) equals :: PCS_0:def 26 (Set ($#k12_pcs_0 :::"pcs-total"::: ) (Set ($#k6_numbers :::"0"::: ) )); end; :: deftheorem defines :::"pcs-empty"::: PCS_0:def 26 : (Bool (Set ($#k13_pcs_0 :::"pcs-empty"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k12_pcs_0 :::"pcs-total"::: ) (Set ($#k6_numbers :::"0"::: ) ))); registration cluster (Set ($#k13_pcs_0 :::"pcs-empty"::: ) ) -> ($#v2_struct_0 :::"empty"::: ) ($#v12_pcs_0 :::"strict"::: ) ($#v14_pcs_0 :::"pcs-like"::: ) ; end; definitionlet "p" be ($#m1_hidden :::"set"::: ) ; func :::"pcs-singleton"::: "p" -> ($#l2_pcs_0 :::"pcs-Str"::: ) equals :: PCS_0:def 27 (Set ($#k12_pcs_0 :::"pcs-total"::: ) (Set ($#k1_tarski :::"{"::: ) "p" ($#k1_tarski :::"}"::: ) )); end; :: deftheorem defines :::"pcs-singleton"::: PCS_0:def 27 : (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k14_pcs_0 :::"pcs-singleton"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k12_pcs_0 :::"pcs-total"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "p")) ($#k1_tarski :::"}"::: ) )))); registrationlet "p" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k14_pcs_0 :::"pcs-singleton"::: ) "p") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v12_pcs_0 :::"strict"::: ) ($#v14_pcs_0 :::"pcs-like"::: ) ; end; definitionlet "R" be ($#m1_hidden :::"Relation":::); attr "R" is :::"pcs-Str-yielding"::: means :: PCS_0:def 28 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "P")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) "R"))) "holds" (Bool (Set (Var "P")) "is" ($#l2_pcs_0 :::"pcs-Str"::: ) )); attr "R" is :::"pcs-yielding"::: means :: PCS_0:def 29 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "P")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) "R"))) "holds" (Bool (Set (Var "P")) "is" ($#l2_pcs_0 :::"pcs":::))); end; :: deftheorem defines :::"pcs-Str-yielding"::: PCS_0:def 28 : (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" (Bool (Set (Var "R")) "is" ($#v16_pcs_0 :::"pcs-Str-yielding"::: ) ) "iff" (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "P")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "R"))))) "holds" (Bool (Set (Var "P")) "is" ($#l2_pcs_0 :::"pcs-Str"::: ) )) ")" )); :: deftheorem defines :::"pcs-yielding"::: PCS_0:def 29 : (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" (Bool (Set (Var "R")) "is" ($#v17_pcs_0 :::"pcs-yielding"::: ) ) "iff" (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "P")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "R"))))) "holds" (Bool (Set (Var "P")) "is" ($#l2_pcs_0 :::"pcs":::))) ")" )); definitionlet "f" be ($#m1_hidden :::"Function":::); redefine attr "f" is :::"pcs-Str-yielding"::: means :: PCS_0:def 30 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "f"))) "holds" (Bool (Set "f" ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) "is" ($#l2_pcs_0 :::"pcs-Str"::: ) )); redefine attr "f" is :::"pcs-yielding"::: means :: PCS_0:def 31 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "f"))) "holds" (Bool (Set "f" ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) "is" ($#l2_pcs_0 :::"pcs":::))); end; :: deftheorem defines :::"pcs-Str-yielding"::: PCS_0:def 30 : (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v16_pcs_0 :::"pcs-Str-yielding"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) "is" ($#l2_pcs_0 :::"pcs-Str"::: ) )) ")" )); :: deftheorem defines :::"pcs-yielding"::: PCS_0:def 31 : (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v17_pcs_0 :::"pcs-yielding"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) "is" ($#l2_pcs_0 :::"pcs":::))) ")" )); definitionlet "I" be ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); :: original: :::"pcs-Str-yielding"::: redefine attr "f" is :::"pcs-Str-yielding"::: means :: PCS_0:def 32 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "I")) "holds" (Bool (Set "f" ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) "is" ($#l2_pcs_0 :::"pcs-Str"::: ) )); :: original: :::"pcs-yielding"::: redefine attr "f" is :::"pcs-yielding"::: means :: PCS_0:def 33 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "I")) "holds" (Bool (Set "f" ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) "is" ($#l2_pcs_0 :::"pcs":::))); end; :: deftheorem defines :::"pcs-Str-yielding"::: PCS_0:def 32 : (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v16_pcs_0 :::"pcs-Str-yielding"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "I")))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) "is" ($#l2_pcs_0 :::"pcs-Str"::: ) )) ")" ))); :: deftheorem defines :::"pcs-yielding"::: PCS_0:def 33 : (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v17_pcs_0 :::"pcs-yielding"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "I")))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) "is" ($#l2_pcs_0 :::"pcs":::))) ")" ))); registration cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v16_pcs_0 :::"pcs-Str-yielding"::: ) -> ($#v1_yellow_1 :::"RelStr-yielding"::: ) ($#v7_pcs_0 :::"TolStr-yielding"::: ) for ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v17_pcs_0 :::"pcs-yielding"::: ) -> ($#v16_pcs_0 :::"pcs-Str-yielding"::: ) for ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v17_pcs_0 :::"pcs-yielding"::: ) -> ($#v5_waybel_3 :::"reflexive-yielding"::: ) ($#v1_pcs_0 :::"transitive-yielding"::: ) ($#v9_pcs_0 :::"pcs-tol-reflexive-yielding"::: ) ($#v11_pcs_0 :::"pcs-tol-symmetric-yielding"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "I" be ($#m1_hidden :::"set"::: ) ; let "P" be ($#l2_pcs_0 :::"pcs":::); cluster (Set "I" ($#k2_funcop_1 :::"-->"::: ) "P") -> () for ($#m1_hidden :::"ManySortedSet":::) "of" "I"; end; registrationlet "I" be ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) "I" ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_partfun1 :::"total"::: ) () for ($#m1_hidden :::"set"::: ) ; end; definitionlet "I" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "C" be () ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); let "i" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "I")); :: original: :::"."::: redefine func "C" :::"."::: "i" -> ($#l2_pcs_0 :::"pcs-Str"::: ) ; end; definitionlet "I" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "C" be () ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); let "i" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "I")); :: original: :::"."::: redefine func "C" :::"."::: "i" -> ($#l2_pcs_0 :::"pcs":::); end; definitionlet "P", "Q" be ($#l2_pcs_0 :::"pcs-Str"::: ) ; pred "P" :::"c="::: "Q" means :: PCS_0:def 34 (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "P") ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "Q")) & (Bool (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" "P") ($#r1_relset_1 :::"c="::: ) (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" "Q")) & (Bool (Set "the" ($#u1_pcs_0 :::"ToleranceRel"::: ) "of" "P") ($#r1_relset_1 :::"c="::: ) (Set "the" ($#u1_pcs_0 :::"ToleranceRel"::: ) "of" "Q")) ")" ); reflexivity (Bool "for" (Set (Var "P")) "being" ($#l2_pcs_0 :::"pcs-Str"::: ) "holds" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "P"))) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "P")))) & (Bool (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "P"))) ($#r1_relset_1 :::"c="::: ) (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "P")))) & (Bool (Set "the" ($#u1_pcs_0 :::"ToleranceRel"::: ) "of" (Set (Var "P"))) ($#r1_relset_1 :::"c="::: ) (Set "the" ($#u1_pcs_0 :::"ToleranceRel"::: ) "of" (Set (Var "P")))) ")" )) ; end; :: deftheorem defines :::"c="::: PCS_0:def 34 : (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#l2_pcs_0 :::"pcs-Str"::: ) "holds" (Bool "(" (Bool (Set (Var "P")) ($#r3_pcs_0 :::"c="::: ) (Set (Var "Q"))) "iff" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "P"))) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Q")))) & (Bool (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "P"))) ($#r1_relset_1 :::"c="::: ) (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "Q")))) & (Bool (Set "the" ($#u1_pcs_0 :::"ToleranceRel"::: ) "of" (Set (Var "P"))) ($#r1_relset_1 :::"c="::: ) (Set "the" ($#u1_pcs_0 :::"ToleranceRel"::: ) "of" (Set (Var "Q")))) ")" ) ")" )); theorem :: PCS_0:8 (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "P")) (Bool "for" (Set (Var "p1")) "," (Set (Var "q1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "Q")) "st" (Bool (Bool (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "P"))) ($#r1_relset_1 :::"c="::: ) (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "Q")))) & (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Var "p1"))) & (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set (Var "q1"))) & (Bool (Set (Var "p")) ($#r1_orders_2 :::"<="::: ) (Set (Var "q")))) "holds" (Bool (Set (Var "p1")) ($#r1_orders_2 :::"<="::: ) (Set (Var "q1")))))) ; theorem :: PCS_0:9 (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#l1_pcs_0 :::"TolStr"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "P")) (Bool "for" (Set (Var "p1")) "," (Set (Var "q1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "Q")) "st" (Bool (Bool (Set "the" ($#u1_pcs_0 :::"ToleranceRel"::: ) "of" (Set (Var "P"))) ($#r1_relset_1 :::"c="::: ) (Set "the" ($#u1_pcs_0 :::"ToleranceRel"::: ) "of" (Set (Var "Q")))) & (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Var "p1"))) & (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set (Var "q1"))) & (Bool (Set (Var "p")) ($#r1_pcs_0 :::"(--)"::: ) (Set (Var "q")))) "holds" (Bool (Set (Var "p1")) ($#r1_pcs_0 :::"(--)"::: ) (Set (Var "q1")))))) ; definitionlet "C" be ($#m1_hidden :::"Relation":::); attr "C" is :::"pcs-chain-like"::: means :: PCS_0:def 35 (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#l2_pcs_0 :::"pcs-Str"::: ) "st" (Bool (Bool (Set (Var "P")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) "C")) & (Bool (Set (Var "Q")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) "C")) & (Bool (Bool "not" (Set (Var "P")) ($#r3_pcs_0 :::"c="::: ) (Set (Var "Q"))))) "holds" (Bool (Set (Var "Q")) ($#r3_pcs_0 :::"c="::: ) (Set (Var "P")))); end; :: deftheorem defines :::"pcs-chain-like"::: PCS_0:def 35 : (Bool "for" (Set (Var "C")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" (Bool (Set (Var "C")) "is" ($#v20_pcs_0 :::"pcs-chain-like"::: ) ) "iff" (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#l2_pcs_0 :::"pcs-Str"::: ) "st" (Bool (Bool (Set (Var "P")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "C")))) & (Bool (Set (Var "Q")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "C")))) & (Bool (Bool "not" (Set (Var "P")) ($#r3_pcs_0 :::"c="::: ) (Set (Var "Q"))))) "holds" (Bool (Set (Var "Q")) ($#r3_pcs_0 :::"c="::: ) (Set (Var "P")))) ")" )); registrationlet "I" be ($#m1_hidden :::"set"::: ) ; let "P" be ($#l2_pcs_0 :::"pcs-Str"::: ) ; cluster (Set "I" ($#k2_funcop_1 :::"-->"::: ) "P") -> ($#v20_pcs_0 :::"pcs-chain-like"::: ) for ($#m1_hidden :::"ManySortedSet":::) "of" "I"; end; registration cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v17_pcs_0 :::"pcs-yielding"::: ) ($#v20_pcs_0 :::"pcs-chain-like"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "I" be ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) "I" ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_partfun1 :::"total"::: ) () ($#v20_pcs_0 :::"pcs-chain-like"::: ) for ($#m1_hidden :::"set"::: ) ; end; definitionlet "I" be ($#m1_hidden :::"set"::: ) ; mode pcs-Chain of "I" is () ($#v20_pcs_0 :::"pcs-chain-like"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" "I"; end; definitionlet "I" be ($#m1_hidden :::"set"::: ) ; let "C" be () ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); func :::"pcs-union"::: "C" -> ($#v12_pcs_0 :::"strict"::: ) ($#l2_pcs_0 :::"pcs-Str"::: ) means :: PCS_0:def 36 (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set ($#k3_card_3 :::"Union"::: ) (Set "(" ($#k12_pralg_1 :::"Carrier"::: ) "C" ")" ))) & (Bool (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set ($#k3_card_3 :::"Union"::: ) (Set "(" ($#k4_pcs_0 :::"pcs-InternalRels"::: ) "C" ")" ))) & (Bool (Set "the" ($#u1_pcs_0 :::"ToleranceRel"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set ($#k3_card_3 :::"Union"::: ) (Set "(" ($#k7_pcs_0 :::"pcs-ToleranceRels"::: ) "C" ")" ))) ")" ); end; :: deftheorem defines :::"pcs-union"::: PCS_0:def 36 : (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" () ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "b3")) "being" ($#v12_pcs_0 :::"strict"::: ) ($#l2_pcs_0 :::"pcs-Str"::: ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k17_pcs_0 :::"pcs-union"::: ) (Set (Var "C")))) "iff" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set ($#k3_card_3 :::"Union"::: ) (Set "(" ($#k12_pralg_1 :::"Carrier"::: ) (Set (Var "C")) ")" ))) & (Bool (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set ($#k3_card_3 :::"Union"::: ) (Set "(" ($#k4_pcs_0 :::"pcs-InternalRels"::: ) (Set (Var "C")) ")" ))) & (Bool (Set "the" ($#u1_pcs_0 :::"ToleranceRel"::: ) "of" (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set ($#k3_card_3 :::"Union"::: ) (Set "(" ($#k7_pcs_0 :::"pcs-ToleranceRels"::: ) (Set (Var "C")) ")" ))) ")" ) ")" )))); theorem :: PCS_0:10 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" () ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k17_pcs_0 :::"pcs-union"::: ) (Set (Var "C")) ")" ) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r1_orders_2 :::"<="::: ) (Set (Var "q"))) "iff" (Bool "ex" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) (Bool "ex" (Set (Var "P")) "being" ($#l2_pcs_0 :::"pcs-Str"::: ) (Bool "ex" (Set (Var "p9")) "," (Set (Var "q9")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "P")) "st" (Bool "(" (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Var "I"))) & (Bool (Set (Var "P")) ($#r1_hidden :::"="::: ) (Set (Set (Var "C")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Var "p9")) ($#r1_hidden :::"="::: ) (Set (Var "p"))) & (Bool (Set (Var "q9")) ($#r1_hidden :::"="::: ) (Set (Var "q"))) & (Bool (Set (Var "p9")) ($#r1_orders_2 :::"<="::: ) (Set (Var "q9"))) ")" )))) ")" )))) ; theorem :: PCS_0:11 (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" () ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k17_pcs_0 :::"pcs-union"::: ) (Set (Var "C")) ")" ) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r1_orders_2 :::"<="::: ) (Set (Var "q"))) "iff" (Bool "ex" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "I"))(Bool "ex" (Set (Var "p9")) "," (Set (Var "q9")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" (Set (Var "C")) ($#k15_pcs_0 :::"."::: ) (Set (Var "i")) ")" ) "st" (Bool "(" (Bool (Set (Var "p9")) ($#r1_hidden :::"="::: ) (Set (Var "p"))) & (Bool (Set (Var "q9")) ($#r1_hidden :::"="::: ) (Set (Var "q"))) & (Bool (Set (Var "p9")) ($#r1_orders_2 :::"<="::: ) (Set (Var "q9"))) ")" ))) ")" )))) ; theorem :: PCS_0:12 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" () ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k17_pcs_0 :::"pcs-union"::: ) (Set (Var "C")) ")" ) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r1_pcs_0 :::"(--)"::: ) (Set (Var "q"))) "iff" (Bool "ex" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) (Bool "ex" (Set (Var "P")) "being" ($#l2_pcs_0 :::"pcs-Str"::: ) (Bool "ex" (Set (Var "p9")) "," (Set (Var "q9")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "P")) "st" (Bool "(" (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Var "I"))) & (Bool (Set (Var "P")) ($#r1_hidden :::"="::: ) (Set (Set (Var "C")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Var "p9")) ($#r1_hidden :::"="::: ) (Set (Var "p"))) & (Bool (Set (Var "q9")) ($#r1_hidden :::"="::: ) (Set (Var "q"))) & (Bool (Set (Var "p9")) ($#r1_pcs_0 :::"(--)"::: ) (Set (Var "q9"))) ")" )))) ")" )))) ; theorem :: PCS_0:13 (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" () ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k17_pcs_0 :::"pcs-union"::: ) (Set (Var "C")) ")" ) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r1_pcs_0 :::"(--)"::: ) (Set (Var "q"))) "iff" (Bool "ex" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "I"))(Bool "ex" (Set (Var "p9")) "," (Set (Var "q9")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" (Set (Var "C")) ($#k15_pcs_0 :::"."::: ) (Set (Var "i")) ")" ) "st" (Bool "(" (Bool (Set (Var "p9")) ($#r1_hidden :::"="::: ) (Set (Var "p"))) & (Bool (Set (Var "q9")) ($#r1_hidden :::"="::: ) (Set (Var "q"))) & (Bool (Set (Var "p9")) ($#r1_pcs_0 :::"(--)"::: ) (Set (Var "q9"))) ")" ))) ")" )))) ; registrationlet "I" be ($#m1_hidden :::"set"::: ) ; let "C" be ($#v5_waybel_3 :::"reflexive-yielding"::: ) () ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); cluster (Set ($#k17_pcs_0 :::"pcs-union"::: ) "C") -> ($#v3_orders_2 :::"reflexive"::: ) ($#v12_pcs_0 :::"strict"::: ) ; end; registrationlet "I" be ($#m1_hidden :::"set"::: ) ; let "C" be ($#v9_pcs_0 :::"pcs-tol-reflexive-yielding"::: ) () ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); cluster (Set ($#k17_pcs_0 :::"pcs-union"::: ) "C") -> ($#v4_pcs_0 :::"pcs-tol-reflexive"::: ) ($#v12_pcs_0 :::"strict"::: ) ; end; registrationlet "I" be ($#m1_hidden :::"set"::: ) ; let "C" be ($#v11_pcs_0 :::"pcs-tol-symmetric-yielding"::: ) () ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); cluster (Set ($#k17_pcs_0 :::"pcs-union"::: ) "C") -> ($#v6_pcs_0 :::"pcs-tol-symmetric"::: ) ($#v12_pcs_0 :::"strict"::: ) ; end; registrationlet "I" be ($#m1_hidden :::"set"::: ) ; let "C" be ($#m1_hidden :::"pcs-Chain":::) "of" (Set (Const "I")); cluster (Set ($#k17_pcs_0 :::"pcs-union"::: ) "C") -> ($#v4_orders_2 :::"transitive"::: ) ($#v12_pcs_0 :::"strict"::: ) ($#v13_pcs_0 :::"pcs-compatible"::: ) ; end; registrationlet "p", "q" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k6_afinsq_1 :::"<%"::: ) "p" "," "q" ($#k6_afinsq_1 :::"%>"::: ) ) -> (Set ($#k2_tarski :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k2_tarski :::"}"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ; cluster (Set ($#k6_afinsq_1 :::"<%"::: ) "p" "," "q" ($#k6_afinsq_1 :::"%>"::: ) ) -> ($#v1_partfun1 :::"total"::: ) ; end; registrationlet "P", "Q" be ($#l1_struct_0 :::"1-sorted"::: ) ; cluster (Set ($#k6_afinsq_1 :::"<%"::: ) "P" "," "Q" ($#k6_afinsq_1 :::"%>"::: ) ) -> ($#v2_pralg_1 :::"1-sorted-yielding"::: ) ; end; registrationlet "P", "Q" be ($#l1_orders_2 :::"RelStr"::: ) ; cluster (Set ($#k6_afinsq_1 :::"<%"::: ) "P" "," "Q" ($#k6_afinsq_1 :::"%>"::: ) ) -> ($#v1_yellow_1 :::"RelStr-yielding"::: ) ; end; registrationlet "P", "Q" be ($#l1_pcs_0 :::"TolStr"::: ) ; cluster (Set ($#k6_afinsq_1 :::"<%"::: ) "P" "," "Q" ($#k6_afinsq_1 :::"%>"::: ) ) -> () ; end; registrationlet "P", "Q" be ($#l2_pcs_0 :::"pcs-Str"::: ) ; cluster (Set ($#k6_afinsq_1 :::"<%"::: ) "P" "," "Q" ($#k6_afinsq_1 :::"%>"::: ) ) -> () ; end; registrationlet "P", "Q" be ($#v3_orders_2 :::"reflexive"::: ) ($#l2_pcs_0 :::"pcs-Str"::: ) ; cluster (Set ($#k6_afinsq_1 :::"<%"::: ) "P" "," "Q" ($#k6_afinsq_1 :::"%>"::: ) ) -> ($#v5_waybel_3 :::"reflexive-yielding"::: ) ; end; registrationlet "P", "Q" be ($#v4_orders_2 :::"transitive"::: ) ($#l2_pcs_0 :::"pcs-Str"::: ) ; cluster (Set ($#k6_afinsq_1 :::"<%"::: ) "P" "," "Q" ($#k6_afinsq_1 :::"%>"::: ) ) -> ($#v1_pcs_0 :::"transitive-yielding"::: ) ; end; registrationlet "P", "Q" be ($#v4_pcs_0 :::"pcs-tol-reflexive"::: ) ($#l2_pcs_0 :::"pcs-Str"::: ) ; cluster (Set ($#k6_afinsq_1 :::"<%"::: ) "P" "," "Q" ($#k6_afinsq_1 :::"%>"::: ) ) -> ($#v9_pcs_0 :::"pcs-tol-reflexive-yielding"::: ) ; end; registrationlet "P", "Q" be ($#v6_pcs_0 :::"pcs-tol-symmetric"::: ) ($#l2_pcs_0 :::"pcs-Str"::: ) ; cluster (Set ($#k6_afinsq_1 :::"<%"::: ) "P" "," "Q" ($#k6_afinsq_1 :::"%>"::: ) ) -> ($#v11_pcs_0 :::"pcs-tol-symmetric-yielding"::: ) ; end; registrationlet "P", "Q" be ($#l2_pcs_0 :::"pcs":::); cluster (Set ($#k6_afinsq_1 :::"<%"::: ) "P" "," "Q" ($#k6_afinsq_1 :::"%>"::: ) ) -> () ; end; definitioncanceled; let "P", "Q" be ($#l2_pcs_0 :::"pcs-Str"::: ) ; func :::"pcs-sum"::: "(" "P" "," "Q" ")" -> ($#l2_pcs_0 :::"pcs-Str"::: ) equals :: PCS_0:def 38 (Set ($#k17_pcs_0 :::"pcs-union"::: ) (Set ($#k6_afinsq_1 :::"<%"::: ) "P" "," "Q" ($#k6_afinsq_1 :::"%>"::: ) )); end; :: deftheorem PCS_0:def 37 : canceled; :: deftheorem defines :::"pcs-sum"::: PCS_0:def 38 : (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#l2_pcs_0 :::"pcs-Str"::: ) "holds" (Bool (Set ($#k18_pcs_0 :::"pcs-sum"::: ) "(" (Set (Var "P")) "," (Set (Var "Q")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k17_pcs_0 :::"pcs-union"::: ) (Set ($#k6_afinsq_1 :::"<%"::: ) (Set (Var "P")) "," (Set (Var "Q")) ($#k6_afinsq_1 :::"%>"::: ) )))); theorem :: PCS_0:14 (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#l2_pcs_0 :::"pcs-Str"::: ) "holds" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k18_pcs_0 :::"pcs-sum"::: ) "(" (Set (Var "P")) "," (Set (Var "Q")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "P"))) ($#k2_xboole_0 :::"\/"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Q"))))) & (Bool (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set "(" ($#k18_pcs_0 :::"pcs-sum"::: ) "(" (Set (Var "P")) "," (Set (Var "Q")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "P"))) ($#k2_pcs_0 :::"\/"::: ) (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "Q"))))) & (Bool (Set "the" ($#u1_pcs_0 :::"ToleranceRel"::: ) "of" (Set "(" ($#k18_pcs_0 :::"pcs-sum"::: ) "(" (Set (Var "P")) "," (Set (Var "Q")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_pcs_0 :::"ToleranceRel"::: ) "of" (Set (Var "P"))) ($#k2_pcs_0 :::"\/"::: ) (Set "the" ($#u1_pcs_0 :::"ToleranceRel"::: ) "of" (Set (Var "Q"))))) ")" )) ; theorem :: PCS_0:15 (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#l2_pcs_0 :::"pcs-Str"::: ) "holds" (Bool (Set ($#k18_pcs_0 :::"pcs-sum"::: ) "(" (Set (Var "P")) "," (Set (Var "Q")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#g2_pcs_0 :::"pcs-Str"::: ) "(#" (Set "(" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "P"))) ($#k2_xboole_0 :::"\/"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Q"))) ")" ) "," (Set "(" (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "P"))) ($#k2_pcs_0 :::"\/"::: ) (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "Q"))) ")" ) "," (Set "(" (Set "the" ($#u1_pcs_0 :::"ToleranceRel"::: ) "of" (Set (Var "P"))) ($#k2_pcs_0 :::"\/"::: ) (Set "the" ($#u1_pcs_0 :::"ToleranceRel"::: ) "of" (Set (Var "Q"))) ")" ) "#)" ))) ; theorem :: PCS_0:16 (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#l2_pcs_0 :::"pcs-Str"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k18_pcs_0 :::"pcs-sum"::: ) "(" (Set (Var "P")) "," (Set (Var "Q")) ")" ")" ) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r1_orders_2 :::"<="::: ) (Set (Var "q"))) "iff" (Bool "(" (Bool "ex" (Set (Var "p9")) "," (Set (Var "q9")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "P")) "st" (Bool "(" (Bool (Set (Var "p9")) ($#r1_hidden :::"="::: ) (Set (Var "p"))) & (Bool (Set (Var "q9")) ($#r1_hidden :::"="::: ) (Set (Var "q"))) & (Bool (Set (Var "p9")) ($#r1_orders_2 :::"<="::: ) (Set (Var "q9"))) ")" )) "or" (Bool "ex" (Set (Var "p9")) "," (Set (Var "q9")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "Q")) "st" (Bool "(" (Bool (Set (Var "p9")) ($#r1_hidden :::"="::: ) (Set (Var "p"))) & (Bool (Set (Var "q9")) ($#r1_hidden :::"="::: ) (Set (Var "q"))) & (Bool (Set (Var "p9")) ($#r1_orders_2 :::"<="::: ) (Set (Var "q9"))) ")" )) ")" ) ")" ))) ; theorem :: PCS_0:17 (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#l2_pcs_0 :::"pcs-Str"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k18_pcs_0 :::"pcs-sum"::: ) "(" (Set (Var "P")) "," (Set (Var "Q")) ")" ")" ) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r1_pcs_0 :::"(--)"::: ) (Set (Var "q"))) "iff" (Bool "(" (Bool "ex" (Set (Var "p9")) "," (Set (Var "q9")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "P")) "st" (Bool "(" (Bool (Set (Var "p9")) ($#r1_hidden :::"="::: ) (Set (Var "p"))) & (Bool (Set (Var "q9")) ($#r1_hidden :::"="::: ) (Set (Var "q"))) & (Bool (Set (Var "p9")) ($#r1_pcs_0 :::"(--)"::: ) (Set (Var "q9"))) ")" )) "or" (Bool "ex" (Set (Var "p9")) "," (Set (Var "q9")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "Q")) "st" (Bool "(" (Bool (Set (Var "p9")) ($#r1_hidden :::"="::: ) (Set (Var "p"))) & (Bool (Set (Var "q9")) ($#r1_hidden :::"="::: ) (Set (Var "q"))) & (Bool (Set (Var "p9")) ($#r1_pcs_0 :::"(--)"::: ) (Set (Var "q9"))) ")" )) ")" ) ")" ))) ; registrationlet "P", "Q" be ($#v3_orders_2 :::"reflexive"::: ) ($#l2_pcs_0 :::"pcs-Str"::: ) ; cluster (Set ($#k18_pcs_0 :::"pcs-sum"::: ) "(" "P" "," "Q" ")" ) -> ($#v3_orders_2 :::"reflexive"::: ) ; end; registrationlet "P", "Q" be ($#v4_pcs_0 :::"pcs-tol-reflexive"::: ) ($#l2_pcs_0 :::"pcs-Str"::: ) ; cluster (Set ($#k18_pcs_0 :::"pcs-sum"::: ) "(" "P" "," "Q" ")" ) -> ($#v4_pcs_0 :::"pcs-tol-reflexive"::: ) ; end; registrationlet "P", "Q" be ($#v6_pcs_0 :::"pcs-tol-symmetric"::: ) ($#l2_pcs_0 :::"pcs-Str"::: ) ; cluster (Set ($#k18_pcs_0 :::"pcs-sum"::: ) "(" "P" "," "Q" ")" ) -> ($#v6_pcs_0 :::"pcs-tol-symmetric"::: ) ; end; theorem :: PCS_0:18 (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#l2_pcs_0 :::"pcs":::) "st" (Bool (Bool (Set (Var "P")) ($#r1_tsep_1 :::"misses"::: ) (Set (Var "Q")))) "holds" (Bool (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set "(" ($#k18_pcs_0 :::"pcs-sum"::: ) "(" (Set (Var "P")) "," (Set (Var "Q")) ")" ")" )) "is" ($#v8_relat_2 :::"transitive"::: ) )) ; theorem :: PCS_0:19 (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#l2_pcs_0 :::"pcs":::) "st" (Bool (Bool (Set (Var "P")) ($#r1_tsep_1 :::"misses"::: ) (Set (Var "Q")))) "holds" (Bool (Set ($#k18_pcs_0 :::"pcs-sum"::: ) "(" (Set (Var "P")) "," (Set (Var "Q")) ")" ) "is" ($#v13_pcs_0 :::"pcs-compatible"::: ) )) ; theorem :: PCS_0:20 (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#l2_pcs_0 :::"pcs":::) "st" (Bool (Bool (Set (Var "P")) ($#r1_tsep_1 :::"misses"::: ) (Set (Var "Q")))) "holds" (Bool (Set ($#k18_pcs_0 :::"pcs-sum"::: ) "(" (Set (Var "P")) "," (Set (Var "Q")) ")" ) "is" ($#l2_pcs_0 :::"pcs":::))) ; definitionlet "P" be ($#l2_pcs_0 :::"pcs-Str"::: ) ; let "a" be ($#m1_hidden :::"set"::: ) ; func :::"pcs-extension"::: "(" "P" "," "a" ")" -> ($#v12_pcs_0 :::"strict"::: ) ($#l2_pcs_0 :::"pcs-Str"::: ) means :: PCS_0:def 39 (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set (Set ($#k1_tarski :::"{"::: ) "a" ($#k1_tarski :::"}"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "P"))) & (Bool (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_tarski :::"{"::: ) "a" ($#k1_tarski :::"}"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#k2_zfmisc_1 :::":]"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" "P"))) & (Bool (Set "the" ($#u1_pcs_0 :::"ToleranceRel"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_tarski :::"{"::: ) "a" ($#k1_tarski :::"}"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#k2_zfmisc_1 :::":]"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) "," (Set ($#k1_tarski :::"{"::: ) "a" ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "the" ($#u1_pcs_0 :::"ToleranceRel"::: ) "of" "P"))) ")" ); end; :: deftheorem defines :::"pcs-extension"::: PCS_0:def 39 : (Bool "for" (Set (Var "P")) "being" ($#l2_pcs_0 :::"pcs-Str"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b3")) "being" ($#v12_pcs_0 :::"strict"::: ) ($#l2_pcs_0 :::"pcs-Str"::: ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k19_pcs_0 :::"pcs-extension"::: ) "(" (Set (Var "P")) "," (Set (Var "a")) ")" )) "iff" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k1_tarski :::"{"::: ) (Set (Var "a")) ($#k1_tarski :::"}"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "P"))))) & (Bool (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "a")) ($#k1_tarski :::"}"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b3"))) ($#k2_zfmisc_1 :::":]"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "P"))))) & (Bool (Set "the" ($#u1_pcs_0 :::"ToleranceRel"::: ) "of" (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "a")) ($#k1_tarski :::"}"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b3"))) ($#k2_zfmisc_1 :::":]"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b3"))) "," (Set ($#k1_tarski :::"{"::: ) (Set (Var "a")) ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "the" ($#u1_pcs_0 :::"ToleranceRel"::: ) "of" (Set (Var "P"))))) ")" ) ")" )))); registrationlet "P" be ($#l2_pcs_0 :::"pcs-Str"::: ) ; let "a" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k19_pcs_0 :::"pcs-extension"::: ) "(" "P" "," "a" ")" ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v12_pcs_0 :::"strict"::: ) ; end; theorem :: PCS_0:21 (Bool "for" (Set (Var "P")) "being" ($#l2_pcs_0 :::"pcs-Str"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "P"))) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k19_pcs_0 :::"pcs-extension"::: ) "(" (Set (Var "P")) "," (Set (Var "a")) ")" ")" ))) & (Bool (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "P"))) ($#r1_relset_1 :::"c="::: ) (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set "(" ($#k19_pcs_0 :::"pcs-extension"::: ) "(" (Set (Var "P")) "," (Set (Var "a")) ")" ")" ))) & (Bool (Set "the" ($#u1_pcs_0 :::"ToleranceRel"::: ) "of" (Set (Var "P"))) ($#r1_relset_1 :::"c="::: ) (Set "the" ($#u1_pcs_0 :::"ToleranceRel"::: ) "of" (Set "(" ($#k19_pcs_0 :::"pcs-extension"::: ) "(" (Set (Var "P")) "," (Set (Var "a")) ")" ")" ))) ")" ))) ; theorem :: PCS_0:22 (Bool "for" (Set (Var "P")) "being" ($#l2_pcs_0 :::"pcs-Str"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k19_pcs_0 :::"pcs-extension"::: ) "(" (Set (Var "P")) "," (Set (Var "a")) ")" ")" ) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Var "a")))) "holds" (Bool (Set (Var "p")) ($#r1_orders_2 :::"<="::: ) (Set (Var "q")))))) ; theorem :: PCS_0:23 (Bool "for" (Set (Var "P")) "being" ($#l2_pcs_0 :::"pcs-Str"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "P")) (Bool "for" (Set (Var "p1")) "," (Set (Var "q1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k19_pcs_0 :::"pcs-extension"::: ) "(" (Set (Var "P")) "," (Set (Var "a")) ")" ")" ) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Var "p1"))) & (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set (Var "q1"))) & (Bool (Set (Var "p")) ($#r1_orders_2 :::"<="::: ) (Set (Var "q")))) "holds" (Bool (Set (Var "p1")) ($#r1_orders_2 :::"<="::: ) (Set (Var "q1"))))))) ; theorem :: PCS_0:24 (Bool "for" (Set (Var "P")) "being" ($#l2_pcs_0 :::"pcs-Str"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "P")) (Bool "for" (Set (Var "p1")) "," (Set (Var "q1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k19_pcs_0 :::"pcs-extension"::: ) "(" (Set (Var "P")) "," (Set (Var "a")) ")" ")" ) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Var "p1"))) & (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set (Var "a"))) & (Bool (Set (Var "p1")) ($#r1_orders_2 :::"<="::: ) (Set (Var "q1"))) & (Bool (Bool "not" (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "P")))))) "holds" (Bool "(" (Bool (Set (Var "q1")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "P")))) & (Bool (Set (Var "q1")) ($#r1_hidden :::"<>"::: ) (Set (Var "a"))) ")" ))))) ; theorem :: PCS_0:25 (Bool "for" (Set (Var "P")) "being" ($#l2_pcs_0 :::"pcs-Str"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k19_pcs_0 :::"pcs-extension"::: ) "(" (Set (Var "P")) "," (Set (Var "a")) ")" ")" ) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set (Var "a")))) "holds" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "P"))))))) ; theorem :: PCS_0:26 (Bool "for" (Set (Var "P")) "being" ($#l2_pcs_0 :::"pcs-Str"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "P")) (Bool "for" (Set (Var "p1")) "," (Set (Var "q1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k19_pcs_0 :::"pcs-extension"::: ) "(" (Set (Var "P")) "," (Set (Var "a")) ")" ")" ) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Var "p1"))) & (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set (Var "q1"))) & (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set (Var "a"))) & (Bool (Set (Var "p1")) ($#r1_orders_2 :::"<="::: ) (Set (Var "q1")))) "holds" (Bool (Set (Var "p")) ($#r1_orders_2 :::"<="::: ) (Set (Var "q"))))))) ; theorem :: PCS_0:27 (Bool "for" (Set (Var "P")) "being" ($#l2_pcs_0 :::"pcs-Str"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k19_pcs_0 :::"pcs-extension"::: ) "(" (Set (Var "P")) "," (Set (Var "a")) ")" ")" ) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Var "a")))) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r1_pcs_0 :::"(--)"::: ) (Set (Var "q"))) & (Bool (Set (Var "q")) ($#r1_pcs_0 :::"(--)"::: ) (Set (Var "p"))) ")" )))) ; theorem :: PCS_0:28 (Bool "for" (Set (Var "P")) "being" ($#l2_pcs_0 :::"pcs-Str"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "P")) (Bool "for" (Set (Var "p1")) "," (Set (Var "q1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k19_pcs_0 :::"pcs-extension"::: ) "(" (Set (Var "P")) "," (Set (Var "a")) ")" ")" ) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Var "p1"))) & (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set (Var "q1"))) & (Bool (Set (Var "p")) ($#r1_pcs_0 :::"(--)"::: ) (Set (Var "q")))) "holds" (Bool (Set (Var "p1")) ($#r1_pcs_0 :::"(--)"::: ) (Set (Var "q1"))))))) ; theorem :: PCS_0:29 (Bool "for" (Set (Var "P")) "being" ($#l2_pcs_0 :::"pcs-Str"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "P")) (Bool "for" (Set (Var "p1")) "," (Set (Var "q1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k19_pcs_0 :::"pcs-extension"::: ) "(" (Set (Var "P")) "," (Set (Var "a")) ")" ")" ) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Var "p1"))) & (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set (Var "q1"))) & (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set (Var "a"))) & (Bool (Set (Var "q")) ($#r1_hidden :::"<>"::: ) (Set (Var "a"))) & (Bool (Set (Var "p1")) ($#r1_pcs_0 :::"(--)"::: ) (Set (Var "q1")))) "holds" (Bool (Set (Var "p")) ($#r1_pcs_0 :::"(--)"::: ) (Set (Var "q"))))))) ; registrationlet "P" be ($#v3_orders_2 :::"reflexive"::: ) ($#l2_pcs_0 :::"pcs-Str"::: ) ; let "a" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k19_pcs_0 :::"pcs-extension"::: ) "(" "P" "," "a" ")" ) -> ($#v3_orders_2 :::"reflexive"::: ) ($#v12_pcs_0 :::"strict"::: ) ; end; theorem :: PCS_0:30 (Bool "for" (Set (Var "P")) "being" ($#v4_orders_2 :::"transitive"::: ) ($#l2_pcs_0 :::"pcs-Str"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Bool "not" (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "P")))))) "holds" (Bool (Set ($#k19_pcs_0 :::"pcs-extension"::: ) "(" (Set (Var "P")) "," (Set (Var "a")) ")" ) "is" ($#v4_orders_2 :::"transitive"::: ) ))) ; registrationlet "P" be ($#v4_pcs_0 :::"pcs-tol-reflexive"::: ) ($#l2_pcs_0 :::"pcs-Str"::: ) ; let "a" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k19_pcs_0 :::"pcs-extension"::: ) "(" "P" "," "a" ")" ) -> ($#v4_pcs_0 :::"pcs-tol-reflexive"::: ) ($#v12_pcs_0 :::"strict"::: ) ; end; registrationlet "P" be ($#v6_pcs_0 :::"pcs-tol-symmetric"::: ) ($#l2_pcs_0 :::"pcs-Str"::: ) ; let "a" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k19_pcs_0 :::"pcs-extension"::: ) "(" "P" "," "a" ")" ) -> ($#v6_pcs_0 :::"pcs-tol-symmetric"::: ) ($#v12_pcs_0 :::"strict"::: ) ; end; theorem :: PCS_0:31 (Bool "for" (Set (Var "P")) "being" ($#v13_pcs_0 :::"pcs-compatible"::: ) ($#l2_pcs_0 :::"pcs-Str"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Bool "not" (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "P")))))) "holds" (Bool (Set ($#k19_pcs_0 :::"pcs-extension"::: ) "(" (Set (Var "P")) "," (Set (Var "a")) ")" ) "is" ($#v13_pcs_0 :::"pcs-compatible"::: ) ))) ; theorem :: PCS_0:32 (Bool "for" (Set (Var "P")) "being" ($#l2_pcs_0 :::"pcs":::) (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Bool "not" (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "P")))))) "holds" (Bool (Set ($#k19_pcs_0 :::"pcs-extension"::: ) "(" (Set (Var "P")) "," (Set (Var "a")) ")" ) "is" ($#l2_pcs_0 :::"pcs":::)))) ; definitionlet "P" be ($#l2_pcs_0 :::"pcs-Str"::: ) ; func :::"pcs-reverse"::: "P" -> ($#v12_pcs_0 :::"strict"::: ) ($#l2_pcs_0 :::"pcs-Str"::: ) means :: PCS_0:def 40 (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "P")) & (Bool (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" "P") ($#k3_relset_1 :::"~"::: ) )) & (Bool (Set "the" ($#u1_pcs_0 :::"ToleranceRel"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_pcs_0 :::"ToleranceRel"::: ) "of" "P") ($#k3_subset_1 :::"`"::: ) )) ")" ); end; :: deftheorem defines :::"pcs-reverse"::: PCS_0:def 40 : (Bool "for" (Set (Var "P")) "being" ($#l2_pcs_0 :::"pcs-Str"::: ) (Bool "for" (Set (Var "b2")) "being" ($#v12_pcs_0 :::"strict"::: ) ($#l2_pcs_0 :::"pcs-Str"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k20_pcs_0 :::"pcs-reverse"::: ) (Set (Var "P")))) "iff" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "P")))) & (Bool (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "P"))) ($#k3_relset_1 :::"~"::: ) )) & (Bool (Set "the" ($#u1_pcs_0 :::"ToleranceRel"::: ) "of" (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_pcs_0 :::"ToleranceRel"::: ) "of" (Set (Var "P"))) ($#k3_subset_1 :::"`"::: ) )) ")" ) ")" ))); registrationlet "P" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_pcs_0 :::"pcs-Str"::: ) ; cluster (Set ($#k20_pcs_0 :::"pcs-reverse"::: ) "P") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v12_pcs_0 :::"strict"::: ) ; end; theorem :: PCS_0:33 (Bool "for" (Set (Var "P")) "being" ($#l2_pcs_0 :::"pcs-Str"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "P")) (Bool "for" (Set (Var "p9")) "," (Set (Var "q9")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k20_pcs_0 :::"pcs-reverse"::: ) (Set (Var "P")) ")" ) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Var "p9"))) & (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set (Var "q9")))) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r1_orders_2 :::"<="::: ) (Set (Var "q"))) "iff" (Bool (Set (Var "q9")) ($#r1_orders_2 :::"<="::: ) (Set (Var "p9"))) ")" )))) ; theorem :: PCS_0:34 (Bool "for" (Set (Var "P")) "being" ($#l2_pcs_0 :::"pcs-Str"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "P")) (Bool "for" (Set (Var "p9")) "," (Set (Var "q9")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k20_pcs_0 :::"pcs-reverse"::: ) (Set (Var "P")) ")" ) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Var "p9"))) & (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set (Var "q9"))) & (Bool (Set (Var "p")) ($#r1_pcs_0 :::"(--)"::: ) (Set (Var "q")))) "holds" (Bool "not" (Bool (Set (Var "p9")) ($#r1_pcs_0 :::"(--)"::: ) (Set (Var "q9"))))))) ; theorem :: PCS_0:35 (Bool "for" (Set (Var "P")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_pcs_0 :::"pcs-Str"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "P")) (Bool "for" (Set (Var "p9")) "," (Set (Var "q9")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k20_pcs_0 :::"pcs-reverse"::: ) (Set (Var "P")) ")" ) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Var "p9"))) & (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set (Var "q9"))) & (Bool (Bool "not" (Set (Var "p9")) ($#r1_pcs_0 :::"(--)"::: ) (Set (Var "q9"))))) "holds" (Bool (Set (Var "p")) ($#r1_pcs_0 :::"(--)"::: ) (Set (Var "q")))))) ; registrationlet "P" be ($#v3_orders_2 :::"reflexive"::: ) ($#l2_pcs_0 :::"pcs-Str"::: ) ; cluster (Set ($#k20_pcs_0 :::"pcs-reverse"::: ) "P") -> ($#v3_orders_2 :::"reflexive"::: ) ($#v12_pcs_0 :::"strict"::: ) ; end; registrationlet "P" be ($#v4_orders_2 :::"transitive"::: ) ($#l2_pcs_0 :::"pcs-Str"::: ) ; cluster (Set ($#k20_pcs_0 :::"pcs-reverse"::: ) "P") -> ($#v4_orders_2 :::"transitive"::: ) ($#v12_pcs_0 :::"strict"::: ) ; end; registrationlet "P" be ($#v4_pcs_0 :::"pcs-tol-reflexive"::: ) ($#l2_pcs_0 :::"pcs-Str"::: ) ; cluster (Set ($#k20_pcs_0 :::"pcs-reverse"::: ) "P") -> ($#v5_pcs_0 :::"pcs-tol-irreflexive"::: ) ($#v12_pcs_0 :::"strict"::: ) ; end; registrationlet "P" be ($#v5_pcs_0 :::"pcs-tol-irreflexive"::: ) ($#l2_pcs_0 :::"pcs-Str"::: ) ; cluster (Set ($#k20_pcs_0 :::"pcs-reverse"::: ) "P") -> ($#v4_pcs_0 :::"pcs-tol-reflexive"::: ) ($#v12_pcs_0 :::"strict"::: ) ; end; registrationlet "P" be ($#v6_pcs_0 :::"pcs-tol-symmetric"::: ) ($#l2_pcs_0 :::"pcs-Str"::: ) ; cluster (Set ($#k20_pcs_0 :::"pcs-reverse"::: ) "P") -> ($#v6_pcs_0 :::"pcs-tol-symmetric"::: ) ($#v12_pcs_0 :::"strict"::: ) ; end; registrationlet "P" be ($#v13_pcs_0 :::"pcs-compatible"::: ) ($#l2_pcs_0 :::"pcs-Str"::: ) ; cluster (Set ($#k20_pcs_0 :::"pcs-reverse"::: ) "P") -> ($#v12_pcs_0 :::"strict"::: ) ($#v13_pcs_0 :::"pcs-compatible"::: ) ; end; definitionlet "P", "Q" be ($#l2_pcs_0 :::"pcs-Str"::: ) ; func "P" :::"pcs-times"::: "Q" -> ($#l2_pcs_0 :::"pcs-Str"::: ) equals :: PCS_0:def 41 (Set ($#g2_pcs_0 :::"pcs-Str"::: ) "(#" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "P") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "Q") ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k2_yellow_3 :::"[""::: ) (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" "P") "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" "Q") ($#k2_yellow_3 :::""]"::: ) ) "," (Set ($#k3_pcs_0 :::"[^"::: ) (Set "the" ($#u1_pcs_0 :::"ToleranceRel"::: ) "of" "P") "," (Set "the" ($#u1_pcs_0 :::"ToleranceRel"::: ) "of" "Q") ($#k3_pcs_0 :::"^]"::: ) ) "#)" ); end; :: deftheorem defines :::"pcs-times"::: PCS_0:def 41 : (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#l2_pcs_0 :::"pcs-Str"::: ) "holds" (Bool (Set (Set (Var "P")) ($#k21_pcs_0 :::"pcs-times"::: ) (Set (Var "Q"))) ($#r1_hidden :::"="::: ) (Set ($#g2_pcs_0 :::"pcs-Str"::: ) "(#" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "P"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Q"))) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k2_yellow_3 :::"[""::: ) (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "P"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "Q"))) ($#k2_yellow_3 :::""]"::: ) ) "," (Set ($#k3_pcs_0 :::"[^"::: ) (Set "the" ($#u1_pcs_0 :::"ToleranceRel"::: ) "of" (Set (Var "P"))) "," (Set "the" ($#u1_pcs_0 :::"ToleranceRel"::: ) "of" (Set (Var "Q"))) ($#k3_pcs_0 :::"^]"::: ) ) "#)" ))); registrationlet "P", "Q" be ($#l2_pcs_0 :::"pcs-Str"::: ) ; cluster (Set "P" ($#k21_pcs_0 :::"pcs-times"::: ) "Q") -> ($#v12_pcs_0 :::"strict"::: ) ; end; registrationlet "P", "Q" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_pcs_0 :::"pcs-Str"::: ) ; cluster (Set "P" ($#k21_pcs_0 :::"pcs-times"::: ) "Q") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ; end; theorem :: PCS_0:36 (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#l2_pcs_0 :::"pcs-Str"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" (Set (Var "P")) ($#k21_pcs_0 :::"pcs-times"::: ) (Set (Var "Q")) ")" ) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "P")) (Bool "for" (Set (Var "q1")) "," (Set (Var "q2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "Q")) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "p1")) "," (Set (Var "q1")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "p2")) "," (Set (Var "q2")) ($#k4_tarski :::"]"::: ) ))) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r1_orders_2 :::"<="::: ) (Set (Var "q"))) "iff" (Bool "(" (Bool (Set (Var "p1")) ($#r1_orders_2 :::"<="::: ) (Set (Var "p2"))) & (Bool (Set (Var "q1")) ($#r1_orders_2 :::"<="::: ) (Set (Var "q2"))) ")" ) ")" ))))) ; theorem :: PCS_0:37 (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#l2_pcs_0 :::"pcs-Str"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" (Set (Var "P")) ($#k21_pcs_0 :::"pcs-times"::: ) (Set (Var "Q")) ")" ) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "P")) (Bool "for" (Set (Var "q1")) "," (Set (Var "q2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "Q")) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "p1")) "," (Set (Var "q1")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "p2")) "," (Set (Var "q2")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Var "p")) ($#r1_pcs_0 :::"(--)"::: ) (Set (Var "q"))) & (Bool (Bool "not" (Set (Var "p1")) ($#r1_pcs_0 :::"(--)"::: ) (Set (Var "p2"))))) "holds" (Bool (Set (Var "q1")) ($#r1_pcs_0 :::"(--)"::: ) (Set (Var "q2"))))))) ; theorem :: PCS_0:38 (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_pcs_0 :::"pcs-Str"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" (Set (Var "P")) ($#k21_pcs_0 :::"pcs-times"::: ) (Set (Var "Q")) ")" ) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "P")) (Bool "for" (Set (Var "q1")) "," (Set (Var "q2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "Q")) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set ($#k7_yellow_3 :::"["::: ) (Set (Var "p1")) "," (Set (Var "q1")) ($#k7_yellow_3 :::"]"::: ) )) & (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set ($#k7_yellow_3 :::"["::: ) (Set (Var "p2")) "," (Set (Var "q2")) ($#k7_yellow_3 :::"]"::: ) )) & (Bool "(" (Bool (Set (Var "p1")) ($#r1_pcs_0 :::"(--)"::: ) (Set (Var "p2"))) "or" (Bool (Set (Var "q1")) ($#r1_pcs_0 :::"(--)"::: ) (Set (Var "q2"))) ")" )) "holds" (Bool (Set (Var "p")) ($#r1_pcs_0 :::"(--)"::: ) (Set (Var "q"))))))) ; registrationlet "P", "Q" be ($#v3_orders_2 :::"reflexive"::: ) ($#l2_pcs_0 :::"pcs-Str"::: ) ; cluster (Set "P" ($#k21_pcs_0 :::"pcs-times"::: ) "Q") -> ($#v3_orders_2 :::"reflexive"::: ) ; end; registrationlet "P", "Q" be ($#v4_orders_2 :::"transitive"::: ) ($#l2_pcs_0 :::"pcs-Str"::: ) ; cluster (Set "P" ($#k21_pcs_0 :::"pcs-times"::: ) "Q") -> ($#v4_orders_2 :::"transitive"::: ) ; end; registrationlet "P" be ($#l2_pcs_0 :::"pcs-Str"::: ) ; let "Q" be ($#v4_pcs_0 :::"pcs-tol-reflexive"::: ) ($#l2_pcs_0 :::"pcs-Str"::: ) ; cluster (Set "P" ($#k21_pcs_0 :::"pcs-times"::: ) "Q") -> ($#v4_pcs_0 :::"pcs-tol-reflexive"::: ) ; end; registrationlet "P" be ($#v4_pcs_0 :::"pcs-tol-reflexive"::: ) ($#l2_pcs_0 :::"pcs-Str"::: ) ; let "Q" be ($#l2_pcs_0 :::"pcs-Str"::: ) ; cluster (Set "P" ($#k21_pcs_0 :::"pcs-times"::: ) "Q") -> ($#v4_pcs_0 :::"pcs-tol-reflexive"::: ) ; end; registrationlet "P", "Q" be ($#v6_pcs_0 :::"pcs-tol-symmetric"::: ) ($#l2_pcs_0 :::"pcs-Str"::: ) ; cluster (Set "P" ($#k21_pcs_0 :::"pcs-times"::: ) "Q") -> ($#v6_pcs_0 :::"pcs-tol-symmetric"::: ) ; end; registrationlet "P", "Q" be ($#v13_pcs_0 :::"pcs-compatible"::: ) ($#l2_pcs_0 :::"pcs-Str"::: ) ; cluster (Set "P" ($#k21_pcs_0 :::"pcs-times"::: ) "Q") -> ($#v13_pcs_0 :::"pcs-compatible"::: ) ; end; definitionlet "P", "Q" be ($#l2_pcs_0 :::"pcs-Str"::: ) ; func "P" :::"-->"::: "Q" -> ($#l2_pcs_0 :::"pcs-Str"::: ) equals :: PCS_0:def 42 (Set (Set "(" ($#k20_pcs_0 :::"pcs-reverse"::: ) "P" ")" ) ($#k21_pcs_0 :::"pcs-times"::: ) "Q"); end; :: deftheorem defines :::"-->"::: PCS_0:def 42 : (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#l2_pcs_0 :::"pcs-Str"::: ) "holds" (Bool (Set (Set (Var "P")) ($#k22_pcs_0 :::"-->"::: ) (Set (Var "Q"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k20_pcs_0 :::"pcs-reverse"::: ) (Set (Var "P")) ")" ) ($#k21_pcs_0 :::"pcs-times"::: ) (Set (Var "Q"))))); registrationlet "P", "Q" be ($#l2_pcs_0 :::"pcs-Str"::: ) ; cluster (Set "P" ($#k22_pcs_0 :::"-->"::: ) "Q") -> ($#v12_pcs_0 :::"strict"::: ) ; end; registrationlet "P", "Q" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_pcs_0 :::"pcs-Str"::: ) ; cluster (Set "P" ($#k22_pcs_0 :::"-->"::: ) "Q") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ; end; theorem :: PCS_0:39 (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#l2_pcs_0 :::"pcs-Str"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" (Set (Var "P")) ($#k22_pcs_0 :::"-->"::: ) (Set (Var "Q")) ")" ) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "P")) (Bool "for" (Set (Var "q1")) "," (Set (Var "q2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "Q")) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "p1")) "," (Set (Var "q1")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "p2")) "," (Set (Var "q2")) ($#k4_tarski :::"]"::: ) ))) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r1_orders_2 :::"<="::: ) (Set (Var "q"))) "iff" (Bool "(" (Bool (Set (Var "p2")) ($#r1_orders_2 :::"<="::: ) (Set (Var "p1"))) & (Bool (Set (Var "q1")) ($#r1_orders_2 :::"<="::: ) (Set (Var "q2"))) ")" ) ")" ))))) ; theorem :: PCS_0:40 (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#l2_pcs_0 :::"pcs-Str"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" (Set (Var "P")) ($#k22_pcs_0 :::"-->"::: ) (Set (Var "Q")) ")" ) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "P")) (Bool "for" (Set (Var "q1")) "," (Set (Var "q2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "Q")) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "p1")) "," (Set (Var "q1")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "p2")) "," (Set (Var "q2")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Var "p")) ($#r1_pcs_0 :::"(--)"::: ) (Set (Var "q"))) & (Bool (Set (Var "p1")) ($#r1_pcs_0 :::"(--)"::: ) (Set (Var "p2")))) "holds" (Bool (Set (Var "q1")) ($#r1_pcs_0 :::"(--)"::: ) (Set (Var "q2"))))))) ; theorem :: PCS_0:41 (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_pcs_0 :::"pcs-Str"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" (Set (Var "P")) ($#k22_pcs_0 :::"-->"::: ) (Set (Var "Q")) ")" ) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "P")) (Bool "for" (Set (Var "q1")) "," (Set (Var "q2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "Q")) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set ($#k7_yellow_3 :::"["::: ) (Set (Var "p1")) "," (Set (Var "q1")) ($#k7_yellow_3 :::"]"::: ) )) & (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set ($#k7_yellow_3 :::"["::: ) (Set (Var "p2")) "," (Set (Var "q2")) ($#k7_yellow_3 :::"]"::: ) )) & (Bool "(" "not" (Bool (Set (Var "p1")) ($#r1_pcs_0 :::"(--)"::: ) (Set (Var "p2"))) "or" (Bool (Set (Var "q1")) ($#r1_pcs_0 :::"(--)"::: ) (Set (Var "q2"))) ")" )) "holds" (Bool (Set (Var "p")) ($#r1_pcs_0 :::"(--)"::: ) (Set (Var "q"))))))) ; registrationlet "P", "Q" be ($#v3_orders_2 :::"reflexive"::: ) ($#l2_pcs_0 :::"pcs-Str"::: ) ; cluster (Set "P" ($#k22_pcs_0 :::"-->"::: ) "Q") -> ($#v3_orders_2 :::"reflexive"::: ) ; end; registrationlet "P", "Q" be ($#v4_orders_2 :::"transitive"::: ) ($#l2_pcs_0 :::"pcs-Str"::: ) ; cluster (Set "P" ($#k22_pcs_0 :::"-->"::: ) "Q") -> ($#v4_orders_2 :::"transitive"::: ) ; end; registrationlet "P" be ($#l2_pcs_0 :::"pcs-Str"::: ) ; let "Q" be ($#v4_pcs_0 :::"pcs-tol-reflexive"::: ) ($#l2_pcs_0 :::"pcs-Str"::: ) ; cluster (Set "P" ($#k22_pcs_0 :::"-->"::: ) "Q") -> ($#v4_pcs_0 :::"pcs-tol-reflexive"::: ) ; end; registrationlet "P" be ($#v5_pcs_0 :::"pcs-tol-irreflexive"::: ) ($#l2_pcs_0 :::"pcs-Str"::: ) ; let "Q" be ($#l2_pcs_0 :::"pcs-Str"::: ) ; cluster (Set "P" ($#k22_pcs_0 :::"-->"::: ) "Q") -> ($#v4_pcs_0 :::"pcs-tol-reflexive"::: ) ; end; registrationlet "P", "Q" be ($#v6_pcs_0 :::"pcs-tol-symmetric"::: ) ($#l2_pcs_0 :::"pcs-Str"::: ) ; cluster (Set "P" ($#k22_pcs_0 :::"-->"::: ) "Q") -> ($#v6_pcs_0 :::"pcs-tol-symmetric"::: ) ; end; registrationlet "P", "Q" be ($#v13_pcs_0 :::"pcs-compatible"::: ) ($#l2_pcs_0 :::"pcs-Str"::: ) ; cluster (Set "P" ($#k22_pcs_0 :::"-->"::: ) "Q") -> ($#v13_pcs_0 :::"pcs-compatible"::: ) ; end; registrationlet "P", "Q" be ($#l2_pcs_0 :::"pcs":::); cluster (Set "P" ($#k22_pcs_0 :::"-->"::: ) "Q") -> ($#v14_pcs_0 :::"pcs-like"::: ) ; end; definitionlet "P" be ($#l1_pcs_0 :::"TolStr"::: ) ; let "S" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "P")); attr "S" is :::"pcs-self-coherent"::: means :: PCS_0:def 43 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" "P" "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "S") & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) "S")) "holds" (Bool (Set (Var "x")) ($#r1_pcs_0 :::"(--)"::: ) (Set (Var "y")))); end; :: deftheorem defines :::"pcs-self-coherent"::: PCS_0:def 43 : (Bool "for" (Set (Var "P")) "being" ($#l1_pcs_0 :::"TolStr"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "P")) "holds" (Bool "(" (Bool (Set (Var "S")) "is" ($#v21_pcs_0 :::"pcs-self-coherent"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "P")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "S"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "S")))) "holds" (Bool (Set (Var "x")) ($#r1_pcs_0 :::"(--)"::: ) (Set (Var "y")))) ")" ))); registrationlet "P" be ($#l1_pcs_0 :::"TolStr"::: ) ; cluster ($#v1_xboole_0 :::"empty"::: ) -> ($#v21_pcs_0 :::"pcs-self-coherent"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "P")); end; definitionlet "P" be ($#l1_pcs_0 :::"TolStr"::: ) ; let "F" be ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Const "P")); attr "F" is :::"pcs-self-coherent-membered"::: means :: PCS_0:def 44 (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" "P" "st" (Bool (Bool (Set (Var "S")) ($#r2_hidden :::"in"::: ) "F")) "holds" (Bool (Set (Var "S")) "is" ($#v21_pcs_0 :::"pcs-self-coherent"::: ) )); end; :: deftheorem defines :::"pcs-self-coherent-membered"::: PCS_0:def 44 : (Bool "for" (Set (Var "P")) "being" ($#l1_pcs_0 :::"TolStr"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "P")) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v22_pcs_0 :::"pcs-self-coherent-membered"::: ) ) "iff" (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "P")) "st" (Bool (Bool (Set (Var "S")) ($#r2_hidden :::"in"::: ) (Set (Var "F")))) "holds" (Bool (Set (Var "S")) "is" ($#v21_pcs_0 :::"pcs-self-coherent"::: ) )) ")" ))); registrationlet "P" be ($#l1_pcs_0 :::"TolStr"::: ) ; cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v22_pcs_0 :::"pcs-self-coherent-membered"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "(" ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "P") ")" )); end; definitionlet "P" be ($#l1_orders_2 :::"RelStr"::: ) ; let "D" be ($#m1_hidden :::"set"::: ) ; func :::"pcs-general-power-IR"::: "(" "P" "," "D" ")" -> ($#m1_subset_1 :::"Relation":::) "of" "D" means :: PCS_0:def 45 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "(" (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) "D") & (Bool (Set (Var "B")) ($#r2_hidden :::"in"::: ) "D") & (Bool "(" "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool "ex" (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" "P")) ")" )) ")" ) ")" ) ")" )); end; :: deftheorem defines :::"pcs-general-power-IR"::: PCS_0:def 45 : (Bool "for" (Set (Var "P")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "D")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k23_pcs_0 :::"pcs-general-power-IR"::: ) "(" (Set (Var "P")) "," (Set (Var "D")) ")" )) "iff" (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "b3"))) "iff" (Bool "(" (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set (Var "D"))) & (Bool (Set (Var "B")) ($#r2_hidden :::"in"::: ) (Set (Var "D"))) & (Bool "(" "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool "ex" (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "P")))) ")" )) ")" ) ")" ) ")" )) ")" )))); definitionlet "P" be ($#l1_pcs_0 :::"TolStr"::: ) ; let "D" be ($#m1_hidden :::"set"::: ) ; func :::"pcs-general-power-TR"::: "(" "P" "," "D" ")" -> ($#m1_subset_1 :::"Relation":::) "of" "D" means :: PCS_0:def 46 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "(" (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) "D") & (Bool (Set (Var "B")) ($#r2_hidden :::"in"::: ) "D") & (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 "B")))) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_pcs_0 :::"ToleranceRel"::: ) "of" "P")) ")" ) ")" ) ")" )); end; :: deftheorem defines :::"pcs-general-power-TR"::: PCS_0:def 46 : (Bool "for" (Set (Var "P")) "being" ($#l1_pcs_0 :::"TolStr"::: ) (Bool "for" (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "D")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k24_pcs_0 :::"pcs-general-power-TR"::: ) "(" (Set (Var "P")) "," (Set (Var "D")) ")" )) "iff" (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "b3"))) "iff" (Bool "(" (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set (Var "D"))) & (Bool (Set (Var "B")) ($#r2_hidden :::"in"::: ) (Set (Var "D"))) & (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 "B")))) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_pcs_0 :::"ToleranceRel"::: ) "of" (Set (Var "P")))) ")" ) ")" ) ")" )) ")" )))); theorem :: PCS_0:42 (Bool "for" (Set (Var "P")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "D")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "P")) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k23_pcs_0 :::"pcs-general-power-IR"::: ) "(" (Set (Var "P")) "," (Set (Var "D")) ")" )) "iff" (Bool "(" (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set (Var "D"))) & (Bool (Set (Var "B")) ($#r2_hidden :::"in"::: ) (Set (Var "D"))) & (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "P")) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool "ex" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "P")) "st" (Bool "(" (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) & (Bool (Set (Var "a")) ($#r1_orders_2 :::"<="::: ) (Set (Var "b"))) ")" )) ")" ) ")" ) ")" )))) ; theorem :: PCS_0:43 (Bool "for" (Set (Var "P")) "being" ($#l1_pcs_0 :::"TolStr"::: ) (Bool "for" (Set (Var "D")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "P")) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k24_pcs_0 :::"pcs-general-power-TR"::: ) "(" (Set (Var "P")) "," (Set (Var "D")) ")" )) "iff" (Bool "(" (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set (Var "D"))) & (Bool (Set (Var "B")) ($#r2_hidden :::"in"::: ) (Set (Var "D"))) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "P")) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "B")))) "holds" (Bool (Set (Var "a")) ($#r1_pcs_0 :::"(--)"::: ) (Set (Var "b"))) ")" ) ")" ) ")" )))) ; definitionlet "P" be ($#l2_pcs_0 :::"pcs-Str"::: ) ; let "D" be ($#m1_hidden :::"set"::: ) ; func :::"pcs-general-power"::: "(" "P" "," "D" ")" -> ($#l2_pcs_0 :::"pcs-Str"::: ) equals :: PCS_0:def 47 (Set ($#g2_pcs_0 :::"pcs-Str"::: ) "(#" "D" "," (Set "(" ($#k23_pcs_0 :::"pcs-general-power-IR"::: ) "(" "P" "," "D" ")" ")" ) "," (Set "(" ($#k24_pcs_0 :::"pcs-general-power-TR"::: ) "(" "P" "," "D" ")" ")" ) "#)" ); end; :: deftheorem defines :::"pcs-general-power"::: PCS_0:def 47 : (Bool "for" (Set (Var "P")) "being" ($#l2_pcs_0 :::"pcs-Str"::: ) (Bool "for" (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k25_pcs_0 :::"pcs-general-power"::: ) "(" (Set (Var "P")) "," (Set (Var "D")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#g2_pcs_0 :::"pcs-Str"::: ) "(#" (Set (Var "D")) "," (Set "(" ($#k23_pcs_0 :::"pcs-general-power-IR"::: ) "(" (Set (Var "P")) "," (Set (Var "D")) ")" ")" ) "," (Set "(" ($#k24_pcs_0 :::"pcs-general-power-TR"::: ) "(" (Set (Var "P")) "," (Set (Var "D")) ")" ")" ) "#)" )))); notationlet "P" be ($#l2_pcs_0 :::"pcs-Str"::: ) ; let "D" be ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Const "P")); synonym :::"pcs-general-power"::: "D" for :::"pcs-general-power"::: "(" "P" "," "D" ")" ; end; registrationlet "P" be ($#l2_pcs_0 :::"pcs-Str"::: ) ; let "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k25_pcs_0 :::"pcs-general-power"::: ) "(" "P" "," "D" ")" ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ; end; theorem :: PCS_0:44 (Bool "for" (Set (Var "P")) "being" ($#l2_pcs_0 :::"pcs-Str"::: ) (Bool "for" (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k25_pcs_0 :::"pcs-general-power"::: ) "(" (Set (Var "P")) "," (Set (Var "D")) ")" ")" ) "st" (Bool (Bool (Set (Var "p")) ($#r1_orders_2 :::"<="::: ) (Set (Var "q")))) "holds" (Bool "for" (Set (Var "p9")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "P")) "st" (Bool (Bool (Set (Var "p9")) ($#r2_hidden :::"in"::: ) (Set (Var "p")))) "holds" (Bool "ex" (Set (Var "q9")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "P")) "st" (Bool "(" (Bool (Set (Var "q9")) ($#r2_hidden :::"in"::: ) (Set (Var "q"))) & (Bool (Set (Var "p9")) ($#r1_orders_2 :::"<="::: ) (Set (Var "q9"))) ")" )))))) ; theorem :: PCS_0:45 (Bool "for" (Set (Var "P")) "being" ($#l2_pcs_0 :::"pcs-Str"::: ) (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "P")) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k25_pcs_0 :::"pcs-general-power"::: ) (Set (Var "D")) ")" ) "st" (Bool (Bool "(" "for" (Set (Var "p9")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "P")) "st" (Bool (Bool (Set (Var "p9")) ($#r2_hidden :::"in"::: ) (Set (Var "p")))) "holds" (Bool "ex" (Set (Var "q9")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "P")) "st" (Bool "(" (Bool (Set (Var "q9")) ($#r2_hidden :::"in"::: ) (Set (Var "q"))) & (Bool (Set (Var "p9")) ($#r1_orders_2 :::"<="::: ) (Set (Var "q9"))) ")" )) ")" )) "holds" (Bool (Set (Var "p")) ($#r1_orders_2 :::"<="::: ) (Set (Var "q")))))) ; theorem :: PCS_0:46 (Bool "for" (Set (Var "P")) "being" ($#l2_pcs_0 :::"pcs-Str"::: ) (Bool "for" (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k25_pcs_0 :::"pcs-general-power"::: ) "(" (Set (Var "P")) "," (Set (Var "D")) ")" ")" ) "st" (Bool (Bool (Set (Var "p")) ($#r1_pcs_0 :::"(--)"::: ) (Set (Var "q")))) "holds" (Bool "for" (Set (Var "p9")) "," (Set (Var "q9")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "P")) "st" (Bool (Bool (Set (Var "p9")) ($#r2_hidden :::"in"::: ) (Set (Var "p"))) & (Bool (Set (Var "q9")) ($#r2_hidden :::"in"::: ) (Set (Var "q")))) "holds" (Bool (Set (Var "p9")) ($#r1_pcs_0 :::"(--)"::: ) (Set (Var "q9"))))))) ; theorem :: PCS_0:47 (Bool "for" (Set (Var "P")) "being" ($#l2_pcs_0 :::"pcs-Str"::: ) (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "P")) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k25_pcs_0 :::"pcs-general-power"::: ) (Set (Var "D")) ")" ) "st" (Bool (Bool "(" "for" (Set (Var "p9")) "," (Set (Var "q9")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "P")) "st" (Bool (Bool (Set (Var "p9")) ($#r2_hidden :::"in"::: ) (Set (Var "p"))) & (Bool (Set (Var "q9")) ($#r2_hidden :::"in"::: ) (Set (Var "q")))) "holds" (Bool (Set (Var "p9")) ($#r1_pcs_0 :::"(--)"::: ) (Set (Var "q9"))) ")" )) "holds" (Bool (Set (Var "p")) ($#r1_pcs_0 :::"(--)"::: ) (Set (Var "q")))))) ; registrationlet "P" be ($#l2_pcs_0 :::"pcs-Str"::: ) ; let "D" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k25_pcs_0 :::"pcs-general-power"::: ) "(" "P" "," "D" ")" ) -> ($#v12_pcs_0 :::"strict"::: ) ; end; registrationlet "P" be ($#v3_orders_2 :::"reflexive"::: ) ($#l2_pcs_0 :::"pcs-Str"::: ) ; let "D" be ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Const "P")); cluster (Set ($#k25_pcs_0 :::"pcs-general-power"::: ) "(" "P" "," "D" ")" ) -> ($#v3_orders_2 :::"reflexive"::: ) ; end; registrationlet "P" be ($#v4_orders_2 :::"transitive"::: ) ($#l2_pcs_0 :::"pcs-Str"::: ) ; let "D" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k25_pcs_0 :::"pcs-general-power"::: ) "(" "P" "," "D" ")" ) -> ($#v4_orders_2 :::"transitive"::: ) ; end; registrationlet "P" be ($#v4_pcs_0 :::"pcs-tol-reflexive"::: ) ($#l2_pcs_0 :::"pcs-Str"::: ) ; let "D" be ($#v22_pcs_0 :::"pcs-self-coherent-membered"::: ) ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Const "P")); cluster (Set ($#k25_pcs_0 :::"pcs-general-power"::: ) "(" "P" "," "D" ")" ) -> ($#v4_pcs_0 :::"pcs-tol-reflexive"::: ) ; end; registrationlet "P" be ($#v6_pcs_0 :::"pcs-tol-symmetric"::: ) ($#l2_pcs_0 :::"pcs-Str"::: ) ; let "D" be ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Const "P")); cluster (Set ($#k25_pcs_0 :::"pcs-general-power"::: ) "(" "P" "," "D" ")" ) -> ($#v6_pcs_0 :::"pcs-tol-symmetric"::: ) ; end; registrationlet "P" be ($#v13_pcs_0 :::"pcs-compatible"::: ) ($#l2_pcs_0 :::"pcs-Str"::: ) ; let "D" be ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Const "P")); cluster (Set ($#k25_pcs_0 :::"pcs-general-power"::: ) "(" "P" "," "D" ")" ) -> ($#v13_pcs_0 :::"pcs-compatible"::: ) ; end; definitionlet "P" be ($#l2_pcs_0 :::"pcs-Str"::: ) ; func :::"pcs-coherent-power"::: "P" -> ($#m1_hidden :::"set"::: ) equals :: PCS_0:def 48 "{" (Set (Var "X")) where X "is" ($#m1_subset_1 :::"Subset":::) "of" "P" : (Bool (Set (Var "X")) "is" ($#v21_pcs_0 :::"pcs-self-coherent"::: ) ) "}" ; end; :: deftheorem defines :::"pcs-coherent-power"::: PCS_0:def 48 : (Bool "for" (Set (Var "P")) "being" ($#l2_pcs_0 :::"pcs-Str"::: ) "holds" (Bool (Set ($#k26_pcs_0 :::"pcs-coherent-power"::: ) (Set (Var "P"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "X")) where X "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "P")) : (Bool (Set (Var "X")) "is" ($#v21_pcs_0 :::"pcs-self-coherent"::: ) ) "}" )); registrationlet "P" be ($#l2_pcs_0 :::"pcs-Str"::: ) ; cluster ($#v21_pcs_0 :::"pcs-self-coherent"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "P")); end; theorem :: PCS_0:48 (Bool "for" (Set (Var "P")) "being" ($#l2_pcs_0 :::"pcs-Str"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set ($#k26_pcs_0 :::"pcs-coherent-power"::: ) (Set (Var "P"))))) "holds" (Bool (Set (Var "X")) "is" ($#v21_pcs_0 :::"pcs-self-coherent"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "P"))))) ; registrationlet "P" be ($#l2_pcs_0 :::"pcs-Str"::: ) ; cluster (Set ($#k26_pcs_0 :::"pcs-coherent-power"::: ) "P") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; definitionlet "P" be ($#l2_pcs_0 :::"pcs-Str"::: ) ; :: original: :::"pcs-coherent-power"::: redefine func :::"pcs-coherent-power"::: "P" -> ($#m1_subset_1 :::"Subset-Family":::) "of" "P"; end; registrationlet "P" be ($#l2_pcs_0 :::"pcs-Str"::: ) ; cluster (Set ($#k26_pcs_0 :::"pcs-coherent-power"::: ) "P") -> ($#v22_pcs_0 :::"pcs-self-coherent-membered"::: ) for ($#m1_subset_1 :::"Subset-Family":::) "of" "P"; end; definitionlet "P" be ($#l2_pcs_0 :::"pcs-Str"::: ) ; func :::"pcs-power"::: "P" -> ($#l2_pcs_0 :::"pcs-Str"::: ) equals :: PCS_0:def 49 (Set ($#k25_pcs_0 :::"pcs-general-power"::: ) (Set "(" ($#k27_pcs_0 :::"pcs-coherent-power"::: ) "P" ")" )); end; :: deftheorem defines :::"pcs-power"::: PCS_0:def 49 : (Bool "for" (Set (Var "P")) "being" ($#l2_pcs_0 :::"pcs-Str"::: ) "holds" (Bool (Set ($#k28_pcs_0 :::"pcs-power"::: ) (Set (Var "P"))) ($#r1_hidden :::"="::: ) (Set ($#k25_pcs_0 :::"pcs-general-power"::: ) (Set "(" ($#k27_pcs_0 :::"pcs-coherent-power"::: ) (Set (Var "P")) ")" )))); registrationlet "P" be ($#l2_pcs_0 :::"pcs-Str"::: ) ; cluster (Set ($#k28_pcs_0 :::"pcs-power"::: ) "P") -> ($#v12_pcs_0 :::"strict"::: ) ; end; registrationlet "P" be ($#l2_pcs_0 :::"pcs-Str"::: ) ; cluster (Set ($#k28_pcs_0 :::"pcs-power"::: ) "P") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ; end; registrationlet "P" be ($#v3_orders_2 :::"reflexive"::: ) ($#l2_pcs_0 :::"pcs-Str"::: ) ; cluster (Set ($#k28_pcs_0 :::"pcs-power"::: ) "P") -> ($#v3_orders_2 :::"reflexive"::: ) ; end; registrationlet "P" be ($#v4_orders_2 :::"transitive"::: ) ($#l2_pcs_0 :::"pcs-Str"::: ) ; cluster (Set ($#k28_pcs_0 :::"pcs-power"::: ) "P") -> ($#v4_orders_2 :::"transitive"::: ) ; end; registrationlet "P" be ($#v4_pcs_0 :::"pcs-tol-reflexive"::: ) ($#l2_pcs_0 :::"pcs-Str"::: ) ; cluster (Set ($#k28_pcs_0 :::"pcs-power"::: ) "P") -> ($#v4_pcs_0 :::"pcs-tol-reflexive"::: ) ; end; registrationlet "P" be ($#v6_pcs_0 :::"pcs-tol-symmetric"::: ) ($#l2_pcs_0 :::"pcs-Str"::: ) ; cluster (Set ($#k28_pcs_0 :::"pcs-power"::: ) "P") -> ($#v6_pcs_0 :::"pcs-tol-symmetric"::: ) ; end; registrationlet "P" be ($#v13_pcs_0 :::"pcs-compatible"::: ) ($#l2_pcs_0 :::"pcs-Str"::: ) ; cluster (Set ($#k28_pcs_0 :::"pcs-power"::: ) "P") -> ($#v13_pcs_0 :::"pcs-compatible"::: ) ; end; registrationlet "P" be ($#l2_pcs_0 :::"pcs":::); cluster (Set ($#k28_pcs_0 :::"pcs-power"::: ) "P") -> ($#v14_pcs_0 :::"pcs-like"::: ) ; end;