:: PARTIT_2 semantic presentation begin definitionlet "Y" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "G" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_bvfunc_2 :::"PARTITIONS"::: ) (Set (Const "Y")) ")" ); :: original: :::"Element"::: redefine mode :::"Element"::: "of" "G" -> ($#m1_eqrel_1 :::"a_partition"::: ) "of" "Y"; end; theorem :: PARTIT_2:1 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k2_bvfunc_2 :::"'/\'"::: ) (Set "(" ($#k1_subset_1 :::"{}"::: ) (Set "(" ($#k1_bvfunc_2 :::"PARTITIONS"::: ) (Set (Var "Y")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_partit1 :::"%O"::: ) (Set (Var "Y"))))) ; theorem :: PARTIT_2:2 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "," (Set (Var "S")) "being" ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Var "Y")) "holds" (Bool (Set (Set (Var "R")) ($#k3_eqrel_1 :::"\/"::: ) (Set (Var "S"))) ($#r1_relset_1 :::"c="::: ) (Set (Set (Var "R")) ($#k4_relset_1 :::"*"::: ) (Set (Var "S")))))) ; theorem :: PARTIT_2:3 (Bool "for" (Set (Var "Y")) "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 "Y")) "holds" (Bool (Set (Var "R")) ($#r1_relset_1 :::"c="::: ) (Set ($#k1_eqrel_1 :::"nabla"::: ) (Set (Var "Y")))))) ; theorem :: PARTIT_2:4 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Var "Y")) "holds" (Bool "(" (Bool (Set (Set "(" ($#k1_eqrel_1 :::"nabla"::: ) (Set (Var "Y")) ")" ) ($#k4_relset_1 :::"*"::: ) (Set (Var "R"))) ($#r2_relset_1 :::"="::: ) (Set ($#k1_eqrel_1 :::"nabla"::: ) (Set (Var "Y")))) & (Bool (Set (Set (Var "R")) ($#k4_relset_1 :::"*"::: ) (Set "(" ($#k1_eqrel_1 :::"nabla"::: ) (Set (Var "Y")) ")" )) ($#r2_relset_1 :::"="::: ) (Set ($#k1_eqrel_1 :::"nabla"::: ) (Set (Var "Y")))) ")" ))) ; theorem :: PARTIT_2:5 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "P")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "Y")) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k4_partit1 :::"ERl"::: ) (Set (Var "P")))) "iff" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k15_bvfunc_1 :::"EqClass"::: ) "(" (Set (Var "y")) "," (Set (Var "P")) ")" )) ")" )))) ; theorem :: PARTIT_2:6 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "," (Set (Var "R")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set ($#k4_partit1 :::"ERl"::: ) (Set (Var "R"))) ($#r2_relset_1 :::"="::: ) (Set (Set "(" ($#k4_partit1 :::"ERl"::: ) (Set (Var "P")) ")" ) ($#k4_relset_1 :::"*"::: ) (Set "(" ($#k4_partit1 :::"ERl"::: ) (Set (Var "Q")) ")" )))) "holds" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "Y")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k15_bvfunc_1 :::"EqClass"::: ) "(" (Set (Var "y")) "," (Set (Var "R")) ")" )) "iff" (Bool "ex" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "Y")) "st" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k15_bvfunc_1 :::"EqClass"::: ) "(" (Set (Var "z")) "," (Set (Var "P")) ")" )) & (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set ($#k15_bvfunc_1 :::"EqClass"::: ) "(" (Set (Var "y")) "," (Set (Var "Q")) ")" )) ")" )) ")" )))) ; theorem :: PARTIT_2:7 (Bool "for" (Set (Var "R")) "," (Set (Var "S")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "R")) ($#r1_relat_2 :::"is_reflexive_in"::: ) (Set (Var "Y"))) & (Bool (Set (Var "S")) ($#r1_relat_2 :::"is_reflexive_in"::: ) (Set (Var "Y")))) "holds" (Bool (Set (Set (Var "R")) ($#k3_relat_1 :::"*"::: ) (Set (Var "S"))) ($#r1_relat_2 :::"is_reflexive_in"::: ) (Set (Var "Y"))))) ; theorem :: PARTIT_2:8 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "R")) ($#r1_relat_2 :::"is_reflexive_in"::: ) (Set (Var "Y")))) "holds" (Bool (Set (Var "Y")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relat_1 :::"field"::: ) (Set (Var "R")))))) ; theorem :: PARTIT_2:9 (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "R")) ($#r1_relat_2 :::"is_reflexive_in"::: ) (Set (Var "Y")))) "holds" (Bool (Set (Var "Y")) ($#r1_hidden :::"="::: ) (Set ($#k1_relat_1 :::"field"::: ) (Set (Var "R")))))) ; theorem :: PARTIT_2:10 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "," (Set (Var "S")) "being" ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Set (Var "R")) ($#k4_relset_1 :::"*"::: ) (Set (Var "S"))) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "S")) ($#k4_relset_1 :::"*"::: ) (Set (Var "R"))))) "holds" (Bool (Set (Set (Var "R")) ($#k4_relset_1 :::"*"::: ) (Set (Var "S"))) "is" ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Var "Y"))))) ; begin theorem :: PARTIT_2:11 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "st" (Bool (Bool (Set (Var "a")) ($#r1_bvfunc_1 :::"'<'"::: ) (Set (Var "b")))) "holds" (Bool (Set ($#k1_bvfunc_1 :::"'not'"::: ) (Set (Var "b"))) ($#r1_bvfunc_1 :::"'<'"::: ) (Set ($#k1_bvfunc_1 :::"'not'"::: ) (Set (Var "a")))))) ; theorem :: PARTIT_2:12 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_bvfunc_2 :::"PARTITIONS"::: ) (Set (Var "Y")) ")" ) (Bool "for" (Set (Var "P")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "a")) ($#r1_bvfunc_1 :::"'<'"::: ) (Set (Var "b")))) "holds" (Bool (Set ($#k6_bvfunc_2 :::"All"::: ) "(" (Set (Var "a")) "," (Set (Var "P")) "," (Set (Var "G")) ")" ) ($#r1_bvfunc_1 :::"'<'"::: ) (Set ($#k6_bvfunc_2 :::"All"::: ) "(" (Set (Var "b")) "," (Set (Var "P")) "," (Set (Var "G")) ")" )))))) ; theorem :: PARTIT_2:13 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_bvfunc_2 :::"PARTITIONS"::: ) (Set (Var "Y")) ")" ) (Bool "for" (Set (Var "P")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "a")) ($#r1_bvfunc_1 :::"'<'"::: ) (Set (Var "b")))) "holds" (Bool (Set ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set (Var "a")) "," (Set (Var "P")) "," (Set (Var "G")) ")" ) ($#r1_bvfunc_1 :::"'<'"::: ) (Set ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set (Var "b")) "," (Set (Var "P")) "," (Set (Var "G")) ")" )))))) ; begin theorem :: PARTIT_2:14 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_bvfunc_2 :::"PARTITIONS"::: ) (Set (Var "Y")) ")" ) "st" (Bool (Bool (Set (Var "G")) "is" ($#v2_bvfunc_2 :::"independent"::: ) )) "holds" (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_bvfunc_2 :::"PARTITIONS"::: ) (Set (Var "Y")) ")" ) "st" (Bool (Bool (Set (Var "P")) ($#r1_tarski :::"c="::: ) (Set (Var "G"))) & (Bool (Set (Var "Q")) ($#r1_tarski :::"c="::: ) (Set (Var "G")))) "holds" (Bool (Set (Set "(" ($#k4_partit1 :::"ERl"::: ) (Set "(" ($#k2_bvfunc_2 :::"'/\'"::: ) (Set (Var "P")) ")" ) ")" ) ($#k4_relset_1 :::"*"::: ) (Set "(" ($#k4_partit1 :::"ERl"::: ) (Set "(" ($#k2_bvfunc_2 :::"'/\'"::: ) (Set (Var "Q")) ")" ) ")" )) ($#r2_relset_1 :::"="::: ) (Set (Set "(" ($#k4_partit1 :::"ERl"::: ) (Set "(" ($#k2_bvfunc_2 :::"'/\'"::: ) (Set (Var "Q")) ")" ) ")" ) ($#k4_relset_1 :::"*"::: ) (Set "(" ($#k4_partit1 :::"ERl"::: ) (Set "(" ($#k2_bvfunc_2 :::"'/\'"::: ) (Set (Var "P")) ")" ) ")" )))))) ; theorem :: PARTIT_2:15 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_bvfunc_2 :::"PARTITIONS"::: ) (Set (Var "Y")) ")" ) (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) "is" ($#v2_bvfunc_2 :::"independent"::: ) )) "holds" (Bool (Set ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set (Var "a")) "," (Set (Var "P")) "," (Set (Var "G")) ")" ")" ) "," (Set (Var "Q")) "," (Set (Var "G")) ")" ) ($#r2_funct_2 :::"="::: ) (Set ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set (Var "a")) "," (Set (Var "Q")) "," (Set (Var "G")) ")" ")" ) "," (Set (Var "P")) "," (Set (Var "G")) ")" )))))) ; theorem :: PARTIT_2:16 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_bvfunc_2 :::"PARTITIONS"::: ) (Set (Var "Y")) ")" ) (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) "is" ($#v2_bvfunc_2 :::"independent"::: ) )) "holds" (Bool (Set ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set (Var "a")) "," (Set (Var "P")) "," (Set (Var "G")) ")" ")" ) "," (Set (Var "Q")) "," (Set (Var "G")) ")" ) ($#r2_funct_2 :::"="::: ) (Set ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set (Var "a")) "," (Set (Var "Q")) "," (Set (Var "G")) ")" ")" ) "," (Set (Var "P")) "," (Set (Var "G")) ")" )))))) ; theorem :: PARTIT_2:17 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_bvfunc_2 :::"PARTITIONS"::: ) (Set (Var "Y")) ")" ) (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) "is" ($#v2_bvfunc_2 :::"independent"::: ) )) "holds" (Bool (Set ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set "(" ($#k6_bvfunc_2 :::"All"::: ) "(" (Set (Var "a")) "," (Set (Var "P")) "," (Set (Var "G")) ")" ")" ) "," (Set (Var "Q")) "," (Set (Var "G")) ")" ) ($#r1_bvfunc_1 :::"'<'"::: ) (Set ($#k6_bvfunc_2 :::"All"::: ) "(" (Set "(" ($#k7_bvfunc_2 :::"Ex"::: ) "(" (Set (Var "a")) "," (Set (Var "Q")) "," (Set (Var "G")) ")" ")" ) "," (Set (Var "P")) "," (Set (Var "G")) ")" )))))) ; begin notationlet "A", "B" be ($#m1_hidden :::"set"::: ) ; synonym :::"[#]"::: "(" "A" "," "B" ")" for :::"[:":::"A" "," "B":::":]":::; end; definitionlet "A", "B" be ($#m1_hidden :::"set"::: ) ; func :::"{}"::: "(" "A" "," "B" ")" -> ($#m1_subset_1 :::"Relation":::) "of" "A" "," "B" equals :: PARTIT_2:def 1 (Set ($#k1_xboole_0 :::"{}"::: ) ); :: original: :::"[#]"::: redefine func :::"[#]"::: "(" "A" "," "B" ")" -> ($#m1_subset_1 :::"Relation":::) "of" "A" "," "B"; end; :: deftheorem defines :::"{}"::: PARTIT_2:def 1 : (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k1_partit_2 :::"{}"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))); registrationlet "A", "B" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k1_partit_2 :::"{}"::: ) "(" "A" "," "B" ")" ) -> ($#v1_xboole_0 :::"empty"::: ) ; end; theorem :: PARTIT_2:18 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k1_relat_1 :::"field"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set (Var "X")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "X")))) ; theorem :: PARTIT_2:19 (Bool (Set ($#k8_funct_5 :::"op1"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#k1_tarski :::"}"::: ) )) ; theorem :: PARTIT_2:20 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k1_relat_1 :::"field"::: ) (Set "(" ($#k1_partit_2 :::"{}"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ; theorem :: PARTIT_2:21 (Bool "for" (Set (Var "X")) "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 "X")) "st" (Bool (Bool (Set (Var "R")) ($#r1_relat_2 :::"is_reflexive_in"::: ) (Set (Var "X")))) "holds" (Bool "(" (Bool (Set (Var "R")) "is" ($#v1_relat_2 :::"reflexive"::: ) ) & (Bool (Set ($#k1_relat_1 :::"field"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set (Var "X"))) ")" ))) ; theorem :: PARTIT_2:22 (Bool "for" (Set (Var "X")) "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 "X")) "st" (Bool (Bool (Set (Var "R")) ($#r3_relat_2 :::"is_symmetric_in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "R")) "is" ($#v3_relat_2 :::"symmetric"::: ) ))) ; theorem :: PARTIT_2:23 (Bool "for" (Set (Var "X")) "," (Set (Var "S")) "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 "X")) "st" (Bool (Bool (Set (Var "R")) "is" ($#v3_relat_2 :::"symmetric"::: ) )) "holds" (Bool (Set (Var "R")) ($#r3_relat_2 :::"is_symmetric_in"::: ) (Set (Var "S"))))) ; theorem :: PARTIT_2:24 (Bool "for" (Set (Var "X")) "," (Set (Var "S")) "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 "X")) "st" (Bool (Bool (Set (Var "R")) "is" ($#v4_relat_2 :::"antisymmetric"::: ) )) "holds" (Bool (Set (Var "R")) ($#r4_relat_2 :::"is_antisymmetric_in"::: ) (Set (Var "S"))))) ; theorem :: PARTIT_2:25 (Bool "for" (Set (Var "X")) "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 "X")) "st" (Bool (Bool (Set (Var "R")) ($#r4_relat_2 :::"is_antisymmetric_in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "R")) "is" ($#v4_relat_2 :::"antisymmetric"::: ) ))) ; theorem :: PARTIT_2:26 (Bool "for" (Set (Var "X")) "," (Set (Var "S")) "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 "X")) "st" (Bool (Bool (Set (Var "R")) "is" ($#v8_relat_2 :::"transitive"::: ) )) "holds" (Bool (Set (Var "R")) ($#r8_relat_2 :::"is_transitive_in"::: ) (Set (Var "S"))))) ; theorem :: PARTIT_2:27 (Bool "for" (Set (Var "X")) "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 "X")) "st" (Bool (Bool (Set (Var "R")) ($#r8_relat_2 :::"is_transitive_in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "R")) "is" ($#v8_relat_2 :::"transitive"::: ) ))) ; theorem :: PARTIT_2:28 (Bool "for" (Set (Var "X")) "," (Set (Var "S")) "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 "X")) "st" (Bool (Bool (Set (Var "R")) "is" ($#v5_relat_2 :::"asymmetric"::: ) )) "holds" (Bool (Set (Var "R")) ($#r5_relat_2 :::"is_asymmetric_in"::: ) (Set (Var "S"))))) ; theorem :: PARTIT_2:29 (Bool "for" (Set (Var "X")) "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 "X")) "st" (Bool (Bool (Set (Var "R")) ($#r5_relat_2 :::"is_asymmetric_in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "R")) "is" ($#v5_relat_2 :::"asymmetric"::: ) ))) ; theorem :: PARTIT_2:30 (Bool "for" (Set (Var "X")) "," (Set (Var "S")) "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 "X")) "st" (Bool (Bool (Set (Var "R")) "is" ($#v2_relat_2 :::"irreflexive"::: ) ) & (Bool (Set ($#k1_relat_1 :::"field"::: ) (Set (Var "R"))) ($#r1_tarski :::"c="::: ) (Set (Var "S")))) "holds" (Bool (Set (Var "R")) ($#r2_relat_2 :::"is_irreflexive_in"::: ) (Set (Var "S"))))) ; theorem :: PARTIT_2:31 (Bool "for" (Set (Var "X")) "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 "X")) "st" (Bool (Bool (Set (Var "R")) ($#r2_relat_2 :::"is_irreflexive_in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "R")) "is" ($#v2_relat_2 :::"irreflexive"::: ) ))) ; registration cluster ($#v1_xboole_0 :::"empty"::: ) ($#v1_relat_1 :::"Relation-like"::: ) -> ($#v2_relat_2 :::"irreflexive"::: ) ($#v5_relat_2 :::"asymmetric"::: ) ($#v8_relat_2 :::"transitive"::: ) for ($#m1_hidden :::"set"::: ) ; end; definitionlet "f" be ($#m1_hidden :::"Function":::); attr "f" is :::"involutive"::: means :: PARTIT_2:def 2 (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 "(" "f" ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "x")))); end; :: deftheorem defines :::"involutive"::: PARTIT_2:def 2 : (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v1_partit_2 :::"involutive"::: ) ) "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 "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "x")))) ")" )); definitionlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"UnOp":::) "of" (Set (Const "X")); :: original: :::"involutive"::: redefine attr "f" is :::"involutive"::: means :: PARTIT_2:def 3 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "X" "holds" (Bool (Set "f" ($#k3_funct_2 :::"."::: ) (Set "(" "f" ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "x")))); end; :: deftheorem defines :::"involutive"::: PARTIT_2:def 3 : (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"UnOp":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v1_partit_2 :::"involutive"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "x")))) ")" ))); registration cluster (Set ($#k6_funct_5 :::"op1"::: ) ) -> ($#v1_partit_2 :::"involutive"::: ) for ($#m1_hidden :::"Function":::); end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k4_relat_1 :::"id"::: ) "X") -> ($#v1_partit_2 :::"involutive"::: ) ; end;