:: TAXONOM2 semantic presentation begin definitionlet "A" be ($#l1_orders_2 :::"RelStr"::: ) ; attr "A" is :::"with_superior"::: means :: TAXONOM2:def 1 (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" "A" "st" (Bool (Set (Var "x")) ($#r8_orders_1 :::"is_superior_of"::: ) (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" "A"))); end; :: deftheorem defines :::"with_superior"::: TAXONOM2:def 1 : (Bool "for" (Set (Var "A")) "being" ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v1_taxonom2 :::"with_superior"::: ) ) "iff" (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "A")) "st" (Bool (Set (Var "x")) ($#r8_orders_1 :::"is_superior_of"::: ) (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "A"))))) ")" )); definitionlet "A" be ($#l1_orders_2 :::"RelStr"::: ) ; attr "A" is :::"with_comparable_down"::: means :: TAXONOM2:def 2 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" "A" "holds" (Bool "(" (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" "A" "holds" (Bool "(" "not" (Bool (Set (Var "z")) ($#r1_orders_2 :::"<="::: ) (Set (Var "x"))) "or" "not" (Bool (Set (Var "z")) ($#r1_orders_2 :::"<="::: ) (Set (Var "y"))) ")" )) "or" (Bool (Set (Var "x")) ($#r1_orders_2 :::"<="::: ) (Set (Var "y"))) "or" (Bool (Set (Var "y")) ($#r1_orders_2 :::"<="::: ) (Set (Var "x"))) ")" )); end; :: deftheorem defines :::"with_comparable_down"::: TAXONOM2:def 2 : (Bool "for" (Set (Var "A")) "being" ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v2_taxonom2 :::"with_comparable_down"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "A")) "holds" (Bool "(" (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "A")) "holds" (Bool "(" "not" (Bool (Set (Var "z")) ($#r1_orders_2 :::"<="::: ) (Set (Var "x"))) "or" "not" (Bool (Set (Var "z")) ($#r1_orders_2 :::"<="::: ) (Set (Var "y"))) ")" )) "or" (Bool (Set (Var "x")) ($#r1_orders_2 :::"<="::: ) (Set (Var "y"))) "or" (Bool (Set (Var "y")) ($#r1_orders_2 :::"<="::: ) (Set (Var "x"))) ")" )) ")" )); theorem :: TAXONOM2:1 (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Bool "not" (Set ($#k2_yellow_1 :::"InclPoset"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "a")) ($#k1_tarski :::"}"::: ) ) ($#k1_tarski :::"}"::: ) )) "is" ($#v2_struct_0 :::"empty"::: ) )) & (Bool (Set ($#k2_yellow_1 :::"InclPoset"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "a")) ($#k1_tarski :::"}"::: ) ) ($#k1_tarski :::"}"::: ) )) "is" ($#v3_orders_2 :::"reflexive"::: ) ) & (Bool (Set ($#k2_yellow_1 :::"InclPoset"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "a")) ($#k1_tarski :::"}"::: ) ) ($#k1_tarski :::"}"::: ) )) "is" ($#v4_orders_2 :::"transitive"::: ) ) & (Bool (Set ($#k2_yellow_1 :::"InclPoset"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "a")) ($#k1_tarski :::"}"::: ) ) ($#k1_tarski :::"}"::: ) )) "is" ($#v5_orders_2 :::"antisymmetric"::: ) ) & (Bool (Set ($#k2_yellow_1 :::"InclPoset"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "a")) ($#k1_tarski :::"}"::: ) ) ($#k1_tarski :::"}"::: ) )) "is" ($#v1_taxonom2 :::"with_superior"::: ) ) & (Bool (Set ($#k2_yellow_1 :::"InclPoset"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "a")) ($#k1_tarski :::"}"::: ) ) ($#k1_tarski :::"}"::: ) )) "is" ($#v2_taxonom2 :::"with_comparable_down"::: ) ) ")" )) ; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_orders_2 :::"strict"::: ) ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v1_taxonom2 :::"with_superior"::: ) ($#v2_taxonom2 :::"with_comparable_down"::: ) for ($#l1_orders_2 :::"RelStr"::: ) ; end; definitionmode Tree is ($#v1_taxonom2 :::"with_superior"::: ) ($#v2_taxonom2 :::"with_comparable_down"::: ) ($#l1_orders_2 :::"Poset":::); end; theorem :: TAXONOM2:2 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "EqR")) "being" ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set (Var "EqR")) "," (Set (Var "x")) ")" )) & (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set (Var "EqR")) "," (Set (Var "y")) ")" ))) "holds" (Bool (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set (Var "EqR")) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set (Var "EqR")) "," (Set (Var "y")) ")" ))))) ; theorem :: TAXONOM2:3 canceled; theorem :: TAXONOM2:4 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "C")) "is" ($#m1_taxonom1 :::"Classification"::: ) "of" (Set (Var "X"))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k3_tarski :::"union"::: ) (Set (Var "C"))))) "holds" (Bool (Set (Var "x")) ($#r1_tarski :::"c="::: ) (Set (Var "X"))))) ; theorem :: TAXONOM2:5 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "C")) "is" ($#m2_taxonom1 :::"Strong_Classification"::: ) "of" (Set (Var "X")))) "holds" (Bool (Set ($#k2_yellow_1 :::"InclPoset"::: ) (Set "(" ($#k3_tarski :::"union"::: ) (Set (Var "C")) ")" )) "is" ($#l1_orders_2 :::"Tree":::)))) ; begin definitionlet "Y" be ($#m1_hidden :::"set"::: ) ; attr "Y" is :::"hierarchic"::: means :: TAXONOM2:def 3 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "Y") & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) "Y") & (Bool (Bool "not" (Set (Var "x")) ($#r1_tarski :::"c="::: ) (Set (Var "y")))) & (Bool (Bool "not" (Set (Var "y")) ($#r1_tarski :::"c="::: ) (Set (Var "x"))))) "holds" (Bool (Set (Var "x")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "y")))); end; :: deftheorem defines :::"hierarchic"::: TAXONOM2:def 3 : (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "Y")) "is" ($#v3_taxonom2 :::"hierarchic"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Y"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "Y"))) & (Bool (Bool "not" (Set (Var "x")) ($#r1_tarski :::"c="::: ) (Set (Var "y")))) & (Bool (Bool "not" (Set (Var "y")) ($#r1_tarski :::"c="::: ) (Set (Var "x"))))) "holds" (Bool (Set (Var "x")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "y")))) ")" )); registration cluster ($#v1_zfmisc_1 :::"trivial"::: ) -> ($#v3_taxonom2 :::"hierarchic"::: ) for ($#m1_hidden :::"set"::: ) ; end; registration cluster ($#~v1_zfmisc_1 "non" ($#v1_zfmisc_1 :::"trivial"::: ) ) ($#v3_taxonom2 :::"hierarchic"::: ) for ($#m1_hidden :::"set"::: ) ; end; theorem :: TAXONOM2:6 (Bool (Set ($#k1_xboole_0 :::"{}"::: ) ) "is" ($#v3_taxonom2 :::"hierarchic"::: ) ) ; theorem :: TAXONOM2:7 (Bool (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) ) "is" ($#v3_taxonom2 :::"hierarchic"::: ) ) ; definitionlet "Y" be ($#m1_hidden :::"set"::: ) ; mode :::"Hierarchy"::: "of" "Y" -> ($#m1_subset_1 :::"Subset-Family":::) "of" "Y" means :: TAXONOM2:def 4 (Bool it "is" ($#v3_taxonom2 :::"hierarchic"::: ) ); end; :: deftheorem defines :::"Hierarchy"::: TAXONOM2:def 4 : (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "Y")) "holds" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m1_taxonom2 :::"Hierarchy"::: ) "of" (Set (Var "Y"))) "iff" (Bool (Set (Var "b2")) "is" ($#v3_taxonom2 :::"hierarchic"::: ) ) ")" ))); definitionlet "Y" be ($#m1_hidden :::"set"::: ) ; attr "Y" is :::"mutually-disjoint"::: means :: TAXONOM2:def 5 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "Y") & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) "Y") & (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y")))) "holds" (Bool (Set (Var "x")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "y")))); end; :: deftheorem defines :::"mutually-disjoint"::: TAXONOM2:def 5 : (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "Y")) "is" ($#v4_taxonom2 :::"mutually-disjoint"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Y"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "Y"))) & (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y")))) "holds" (Bool (Set (Var "x")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "y")))) ")" )); registrationlet "Y" be ($#m1_hidden :::"set"::: ) ; cluster ($#v4_taxonom2 :::"mutually-disjoint"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "(" ($#k1_zfmisc_1 :::"bool"::: ) "Y" ")" )); end; theorem :: TAXONOM2:8 (Bool (Set ($#k1_xboole_0 :::"{}"::: ) ) "is" ($#v4_taxonom2 :::"mutually-disjoint"::: ) ) ; theorem :: TAXONOM2:9 (Bool (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) ) "is" ($#v4_taxonom2 :::"mutually-disjoint"::: ) ) ; theorem :: TAXONOM2:10 (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k1_tarski :::"{"::: ) (Set (Var "a")) ($#k1_tarski :::"}"::: ) ) "is" ($#v4_taxonom2 :::"mutually-disjoint"::: ) )) ; definitionlet "Y" be ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Const "Y")); attr "F" is :::"T_3"::: means :: TAXONOM2:def 6 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" "Y" "st" (Bool (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) "F")) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "Y" "st" (Bool (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))))) "holds" (Bool "ex" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" "Y" "st" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) & (Bool (Set (Var "B")) ($#r2_hidden :::"in"::: ) "F") & (Bool (Set (Var "A")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "B"))) ")" )))); end; :: deftheorem defines :::"T_3"::: TAXONOM2:def 6 : (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "Y")) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v5_taxonom2 :::"T_3"::: ) ) "iff" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set (Var "F")))) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))))) "holds" (Bool "ex" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) "st" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) & (Bool (Set (Var "B")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) & (Bool (Set (Var "A")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "B"))) ")" )))) ")" ))); theorem :: TAXONOM2:11 (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set (Var "F")) "is" ($#v5_taxonom2 :::"T_3"::: ) ))) ; registrationlet "Y" be ($#m1_hidden :::"set"::: ) ; cluster ($#v3_abian :::"covering"::: ) ($#v5_taxonom2 :::"T_3"::: ) for ($#m1_taxonom2 :::"Hierarchy"::: ) "of" "Y"; end; definitionlet "Y" be ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Const "Y")); attr "F" is :::"lower-bounded"::: means :: TAXONOM2:def 7 (Bool "for" (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "B")) ($#r1_tarski :::"c="::: ) "F") & (Bool (Set (Var "B")) "is" ($#v6_ordinal1 :::"c=-linear"::: ) )) "holds" (Bool "ex" (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) "F") & (Bool (Set (Var "c")) ($#r1_tarski :::"c="::: ) (Set ($#k1_setfam_1 :::"meet"::: ) (Set (Var "B")))) ")" ))); end; :: deftheorem defines :::"lower-bounded"::: TAXONOM2:def 7 : (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "Y")) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v6_taxonom2 :::"lower-bounded"::: ) ) "iff" (Bool "for" (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "B")) ($#r1_tarski :::"c="::: ) (Set (Var "F"))) & (Bool (Set (Var "B")) "is" ($#v6_ordinal1 :::"c=-linear"::: ) )) "holds" (Bool "ex" (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) & (Bool (Set (Var "c")) ($#r1_tarski :::"c="::: ) (Set ($#k1_setfam_1 :::"meet"::: ) (Set (Var "B")))) ")" ))) ")" ))); theorem :: TAXONOM2:12 (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) (Bool "for" (Set (Var "B")) "being" ($#v4_taxonom2 :::"mutually-disjoint"::: ) ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "Y")) "st" (Bool (Bool "(" "for" (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "B")))) "holds" (Bool "(" (Bool (Set (Var "S1")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "b"))) & (Bool (Set (Var "Y")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ) ")" )) "holds" (Bool "(" (Bool (Set (Set (Var "B")) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "S1")) ($#k1_tarski :::"}"::: ) )) "is" ($#v4_taxonom2 :::"mutually-disjoint"::: ) ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "Y"))) & "(" (Bool (Bool (Set (Var "S1")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "implies" (Bool (Set ($#k3_tarski :::"union"::: ) (Set "(" (Set (Var "B")) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "S1")) ($#k1_tarski :::"}"::: ) ) ")" )) ($#r1_hidden :::"<>"::: ) (Set ($#k5_setfam_1 :::"union"::: ) (Set (Var "B")))) ")" ")" )))) ; definitionlet "Y" be ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Const "Y")); attr "F" is :::"with_max's"::: means :: TAXONOM2:def 8 (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" "Y" "st" (Bool (Bool (Set (Var "S")) ($#r2_hidden :::"in"::: ) "F")) "holds" (Bool "ex" (Set (Var "T")) "being" ($#m1_subset_1 :::"Subset":::) "of" "Y" "st" (Bool "(" (Bool (Set (Var "S")) ($#r1_tarski :::"c="::: ) (Set (Var "T"))) & (Bool (Set (Var "T")) ($#r2_hidden :::"in"::: ) "F") & (Bool "(" "for" (Set (Var "V")) "being" ($#m1_subset_1 :::"Subset":::) "of" "Y" "st" (Bool (Bool (Set (Var "T")) ($#r1_tarski :::"c="::: ) (Set (Var "V"))) & (Bool (Set (Var "V")) ($#r2_hidden :::"in"::: ) "F")) "holds" (Bool (Set (Var "V")) ($#r1_hidden :::"="::: ) "Y") ")" ) ")" ))); end; :: deftheorem defines :::"with_max's"::: TAXONOM2:def 8 : (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "Y")) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v7_taxonom2 :::"with_max's"::: ) ) "iff" (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "S")) ($#r2_hidden :::"in"::: ) (Set (Var "F")))) "holds" (Bool "ex" (Set (Var "T")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) "st" (Bool "(" (Bool (Set (Var "S")) ($#r1_tarski :::"c="::: ) (Set (Var "T"))) & (Bool (Set (Var "T")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) & (Bool "(" "for" (Set (Var "V")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "T")) ($#r1_tarski :::"c="::: ) (Set (Var "V"))) & (Bool (Set (Var "V")) ($#r2_hidden :::"in"::: ) (Set (Var "F")))) "holds" (Bool (Set (Var "V")) ($#r1_hidden :::"="::: ) (Set (Var "Y"))) ")" ) ")" ))) ")" ))); begin theorem :: TAXONOM2:13 (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "H")) "being" ($#v3_abian :::"covering"::: ) ($#m1_taxonom2 :::"Hierarchy"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "H")) "is" ($#v7_taxonom2 :::"with_max's"::: ) )) "holds" (Bool "ex" (Set (Var "P")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Set (Var "P")) ($#r1_tarski :::"c="::: ) (Set (Var "H")))))) ; theorem :: TAXONOM2:14 (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "H")) "being" ($#v3_abian :::"covering"::: ) ($#m1_taxonom2 :::"Hierarchy"::: ) "of" (Set (Var "Y")) (Bool "for" (Set (Var "B")) "being" ($#v4_taxonom2 :::"mutually-disjoint"::: ) ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "B")) ($#r1_tarski :::"c="::: ) (Set (Var "H"))) & (Bool "(" "for" (Set (Var "C")) "being" ($#v4_taxonom2 :::"mutually-disjoint"::: ) ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "C")) ($#r1_tarski :::"c="::: ) (Set (Var "H"))) & (Bool (Set ($#k5_setfam_1 :::"union"::: ) (Set (Var "B"))) ($#r1_tarski :::"c="::: ) (Set ($#k5_setfam_1 :::"union"::: ) (Set (Var "C"))))) "holds" (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set (Var "C"))) ")" )) "holds" (Bool (Set (Var "B")) "is" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")))))) ; theorem :: TAXONOM2:15 (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "H")) "being" ($#v3_abian :::"covering"::: ) ($#v5_taxonom2 :::"T_3"::: ) ($#m1_taxonom2 :::"Hierarchy"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "H")) "is" ($#v6_taxonom2 :::"lower-bounded"::: ) ) & (Bool (Bool "not" (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "H"))))) "holds" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) (Bool "for" (Set (Var "B")) "being" ($#v4_taxonom2 :::"mutually-disjoint"::: ) ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) & (Bool (Set (Var "B")) ($#r1_tarski :::"c="::: ) (Set (Var "H"))) & (Bool "(" "for" (Set (Var "C")) "being" ($#v4_taxonom2 :::"mutually-disjoint"::: ) ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set (Var "C"))) & (Bool (Set (Var "C")) ($#r1_tarski :::"c="::: ) (Set (Var "H"))) & (Bool (Set ($#k5_setfam_1 :::"union"::: ) (Set (Var "B"))) ($#r1_tarski :::"c="::: ) (Set ($#k5_setfam_1 :::"union"::: ) (Set (Var "C"))))) "holds" (Bool (Set ($#k5_setfam_1 :::"union"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set ($#k5_setfam_1 :::"union"::: ) (Set (Var "C")))) ")" )) "holds" (Bool (Set (Var "B")) "is" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y"))))))) ; theorem :: TAXONOM2:16 (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "H")) "being" ($#v3_abian :::"covering"::: ) ($#v5_taxonom2 :::"T_3"::: ) ($#m1_taxonom2 :::"Hierarchy"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "H")) "is" ($#v6_taxonom2 :::"lower-bounded"::: ) ) & (Bool (Bool "not" (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "H"))))) "holds" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) (Bool "for" (Set (Var "B")) "being" ($#v4_taxonom2 :::"mutually-disjoint"::: ) ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) & (Bool (Set (Var "B")) ($#r1_tarski :::"c="::: ) (Set (Var "H"))) & (Bool "(" "for" (Set (Var "C")) "being" ($#v4_taxonom2 :::"mutually-disjoint"::: ) ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set (Var "C"))) & (Bool (Set (Var "C")) ($#r1_tarski :::"c="::: ) (Set (Var "H"))) & (Bool (Set (Var "B")) ($#r1_tarski :::"c="::: ) (Set (Var "C")))) "holds" (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set (Var "C"))) ")" )) "holds" (Bool (Set (Var "B")) "is" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y"))))))) ; theorem :: TAXONOM2:17 (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "H")) "being" ($#v3_abian :::"covering"::: ) ($#v5_taxonom2 :::"T_3"::: ) ($#m1_taxonom2 :::"Hierarchy"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "H")) "is" ($#v6_taxonom2 :::"lower-bounded"::: ) ) & (Bool (Bool "not" (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "H"))))) "holds" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set (Var "H")))) "holds" (Bool "ex" (Set (Var "P")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool "(" (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set (Var "P")) ($#r1_tarski :::"c="::: ) (Set (Var "H"))) ")" ))))) ; theorem :: TAXONOM2:18 (Bool "for" (Set (Var "X")) "," (Set (Var "h")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Pmin")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "hw")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "hw")) ($#r2_hidden :::"in"::: ) (Set (Var "Pmin"))) & (Bool (Set (Var "h")) ($#r1_tarski :::"c="::: ) (Set (Var "hw")))) "holds" (Bool "for" (Set (Var "PS")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "h")) ($#r2_hidden :::"in"::: ) (Set (Var "PS"))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "not" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "PS"))) "or" (Bool (Set (Var "x")) ($#r1_tarski :::"c="::: ) (Set (Var "hw"))) "or" (Bool (Set (Var "hw")) ($#r1_tarski :::"c="::: ) (Set (Var "x"))) "or" (Bool (Set (Var "hw")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "x"))) ")" ) ")" )) "holds" (Bool "for" (Set (Var "PT")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "(" "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "PT"))) "iff" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "PS"))) & (Bool (Set (Var "a")) ($#r1_tarski :::"c="::: ) (Set (Var "hw"))) ")" ) ")" ) ")" )) "holds" (Bool "(" (Bool (Set (Set (Var "PT")) ($#k2_xboole_0 :::"\/"::: ) (Set "(" (Set (Var "Pmin")) ($#k7_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "hw")) ($#k1_tarski :::"}"::: ) ) ")" )) "is" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "X"))) & (Bool (Set (Set (Var "PT")) ($#k2_xboole_0 :::"\/"::: ) (Set "(" (Set (Var "Pmin")) ($#k7_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "hw")) ($#k1_tarski :::"}"::: ) ) ")" )) ($#r1_setfam_1 :::"is_finer_than"::: ) (Set (Var "Pmin"))) ")" )))))) ; theorem :: TAXONOM2:19 (Bool "for" (Set (Var "X")) "," (Set (Var "h")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "h")) ($#r1_tarski :::"c="::: ) (Set (Var "X")))) "holds" (Bool "for" (Set (Var "Pmax")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "X")) "st" (Bool (Bool "ex" (Set (Var "hy")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "hy")) ($#r2_hidden :::"in"::: ) (Set (Var "Pmax"))) & (Bool (Set (Var "hy")) ($#r1_tarski :::"c="::: ) (Set (Var "h"))) ")" )) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "not" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Pmax"))) "or" (Bool (Set (Var "x")) ($#r1_tarski :::"c="::: ) (Set (Var "h"))) "or" (Bool (Set (Var "h")) ($#r1_tarski :::"c="::: ) (Set (Var "x"))) "or" (Bool (Set (Var "h")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "x"))) ")" ) ")" )) "holds" (Bool "for" (Set (Var "Pb")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Pb"))) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Pmax"))) & (Bool (Set (Var "x")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "h"))) ")" ) ")" ) ")" )) "holds" (Bool "(" (Bool (Set (Set (Var "Pb")) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "h")) ($#k1_tarski :::"}"::: ) )) "is" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "X"))) & (Bool (Set (Var "Pmax")) ($#r1_setfam_1 :::"is_finer_than"::: ) (Set (Set (Var "Pb")) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "h")) ($#k1_tarski :::"}"::: ) ))) & (Bool "(" "for" (Set (Var "Pmin")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "Pmax")) ($#r1_setfam_1 :::"is_finer_than"::: ) (Set (Var "Pmin")))) "holds" (Bool "for" (Set (Var "hw")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "hw")) ($#r2_hidden :::"in"::: ) (Set (Var "Pmin"))) & (Bool (Set (Var "h")) ($#r1_tarski :::"c="::: ) (Set (Var "hw")))) "holds" (Bool (Set (Set (Var "Pb")) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "h")) ($#k1_tarski :::"}"::: ) )) ($#r1_setfam_1 :::"is_finer_than"::: ) (Set (Var "Pmin")))) ")" ) ")" )))) ; theorem :: TAXONOM2:20 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "H")) "being" ($#v3_abian :::"covering"::: ) ($#v5_taxonom2 :::"T_3"::: ) ($#m1_taxonom2 :::"Hierarchy"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "H")) "is" ($#v6_taxonom2 :::"lower-bounded"::: ) ) & (Bool (Bool "not" (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "H")))) & (Bool "(" "for" (Set (Var "C1")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "C1")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "C1")) ($#r1_tarski :::"c="::: ) (Set ($#k1_partit1 :::"PARTITIONS"::: ) (Set (Var "X")))) & (Bool "(" "for" (Set (Var "P1")) "," (Set (Var "P2")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "P1")) ($#r2_hidden :::"in"::: ) (Set (Var "C1"))) & (Bool (Set (Var "P2")) ($#r2_hidden :::"in"::: ) (Set (Var "C1"))) & (Bool (Bool "not" (Set (Var "P1")) ($#r1_setfam_1 :::"is_finer_than"::: ) (Set (Var "P2"))))) "holds" (Bool (Set (Var "P2")) ($#r1_setfam_1 :::"is_finer_than"::: ) (Set (Var "P1"))) ")" )) "holds" (Bool "ex" (Set (Var "PX")) "," (Set (Var "PY")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "PX")) ($#r2_hidden :::"in"::: ) (Set (Var "C1"))) & (Bool (Set (Var "PY")) ($#r2_hidden :::"in"::: ) (Set (Var "C1"))) & (Bool "(" "for" (Set (Var "PZ")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "PZ")) ($#r2_hidden :::"in"::: ) (Set (Var "C1")))) "holds" (Bool "(" (Bool (Set (Var "PZ")) ($#r1_setfam_1 :::"is_finer_than"::: ) (Set (Var "PY"))) & (Bool (Set (Var "PX")) ($#r1_setfam_1 :::"is_finer_than"::: ) (Set (Var "PZ"))) ")" ) ")" ) ")" )) ")" )) "holds" (Bool "ex" (Set (Var "C")) "being" ($#m1_taxonom1 :::"Classification"::: ) "of" (Set (Var "X")) "st" (Bool (Set ($#k3_tarski :::"union"::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set (Var "H")))))) ;