:: TAXONOM1 semantic presentation begin registration cluster bbbadV1_XCMPLX_0() ($#v1_xxreal_0 :::"ext-real"::: ) ($#~v3_xxreal_0 "non" ($#v3_xxreal_0 :::"negative"::: ) ) ($#v1_xreal_0 :::"real"::: ) for ($#m1_hidden :::"set"::: ) ; end; theorem :: TAXONOM1:1 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Set (Var "k")) ($#k1_nat_1 :::"+"::: ) (Num 1)) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p")))) & (Bool (Bool "not" (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p")))))) "holds" (Bool (Set (Var "k")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )))) ; theorem :: TAXONOM1:2 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p")))) & (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p")))) & (Bool "(" "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p")))) & (Bool (Set (Set (Var "k")) ($#k1_nat_1 :::"+"::: ) (Num 1)) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "k")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ))) ")" )) "holds" (Bool (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "j")))))) ; theorem :: TAXONOM1:3 (Bool "for" (Set (Var "X")) "being" ($#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 (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set (Var "X"))))) ; theorem :: TAXONOM1:4 (Bool "for" (Set (Var "X")) "being" ($#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 (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set (Var "X"))))) ; theorem :: TAXONOM1:5 (Bool "for" (Set (Var "X")) "being" ($#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 (Set (Set (Var "R")) ($#k18_finseq_1 :::"[*]"::: ) ) ($#r1_relat_2 :::"is_reflexive_in"::: ) (Set (Var "X"))))) ; theorem :: TAXONOM1:6 (Bool "for" (Set (Var "X")) "," (Set (Var "x")) "," (Set (Var "y")) "being" ($#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"))) & (Bool (Set (Var "R")) ($#r1_rewrite1 :::"reduces"::: ) (Set (Var "x")) "," (Set (Var "y"))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Set (Var "R")) ($#k18_finseq_1 :::"[*]"::: ) )))) ; theorem :: TAXONOM1:7 (Bool "for" (Set (Var "X")) "being" ($#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 (Set (Var "R")) ($#k18_finseq_1 :::"[*]"::: ) ) ($#r3_relat_2 :::"is_symmetric_in"::: ) (Set (Var "X"))))) ; theorem :: TAXONOM1:8 (Bool "for" (Set (Var "X")) "being" ($#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 (Set (Set (Var "R")) ($#k18_finseq_1 :::"[*]"::: ) ) ($#r8_relat_2 :::"is_transitive_in"::: ) (Set (Var "X"))))) ; theorem :: TAXONOM1:9 (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"))) & (Bool (Set (Var "R")) ($#r3_relat_2 :::"is_symmetric_in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Set (Var "R")) ($#k13_lang1 :::"[*]"::: ) ) "is" ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Var "X"))))) ; theorem :: TAXONOM1:10 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R1")) "," (Set (Var "R2")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "R1")) ($#r1_relset_1 :::"c="::: ) (Set (Var "R2")))) "holds" (Bool (Set (Set (Var "R1")) ($#k13_lang1 :::"[*]"::: ) ) ($#r1_relset_1 :::"c="::: ) (Set (Set (Var "R2")) ($#k13_lang1 :::"[*]"::: ) )))) ; theorem :: TAXONOM1:11 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k10_eqrel_1 :::"SmallestPartition"::: ) (Set (Var "A"))) ($#r1_setfam_1 :::"is_finer_than"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "A")) ($#k1_tarski :::"}"::: ) ))) ; begin definitionlet "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; mode :::"Classification"::: "of" "A" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_partit1 :::"PARTITIONS"::: ) "A" ")" ) means :: TAXONOM1:def 1 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" "A" "st" (Bool (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) it) & (Bool (Set (Var "Y")) ($#r2_hidden :::"in"::: ) it) & (Bool (Bool "not" (Set (Var "X")) ($#r1_setfam_1 :::"is_finer_than"::: ) (Set (Var "Y"))))) "holds" (Bool (Set (Var "Y")) ($#r1_setfam_1 :::"is_finer_than"::: ) (Set (Var "X")))); end; :: deftheorem defines :::"Classification"::: TAXONOM1:def 1 : (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_partit1 :::"PARTITIONS"::: ) (Set (Var "A")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m1_taxonom1 :::"Classification"::: ) "of" (Set (Var "A"))) "iff" (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) & (Bool (Set (Var "Y")) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) & (Bool (Bool "not" (Set (Var "X")) ($#r1_setfam_1 :::"is_finer_than"::: ) (Set (Var "Y"))))) "holds" (Bool (Set (Var "Y")) ($#r1_setfam_1 :::"is_finer_than"::: ) (Set (Var "X")))) ")" ))); theorem :: TAXONOM1:12 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "A")) ($#k1_tarski :::"}"::: ) ) ($#k1_tarski :::"}"::: ) ) "is" ($#m1_taxonom1 :::"Classification"::: ) "of" (Set (Var "A")))) ; theorem :: TAXONOM1:13 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k1_tarski :::"{"::: ) (Set "(" ($#k10_eqrel_1 :::"SmallestPartition"::: ) (Set (Var "A")) ")" ) ($#k1_tarski :::"}"::: ) ) "is" ($#m1_taxonom1 :::"Classification"::: ) "of" (Set (Var "A")))) ; theorem :: TAXONOM1:14 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_partit1 :::"PARTITIONS"::: ) (Set (Var "A")) ")" ) "st" (Bool (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "A")) ($#k1_tarski :::"}"::: ) ) "," (Set "(" ($#k10_eqrel_1 :::"SmallestPartition"::: ) (Set (Var "A")) ")" ) ($#k2_tarski :::"}"::: ) ))) "holds" (Bool (Set (Var "S")) "is" ($#m1_taxonom1 :::"Classification"::: ) "of" (Set (Var "A"))))) ; definitionlet "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; mode :::"Strong_Classification"::: "of" "A" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_partit1 :::"PARTITIONS"::: ) "A" ")" ) means :: TAXONOM1:def 2 (Bool "(" (Bool it "is" ($#m1_taxonom1 :::"Classification"::: ) "of" "A") & (Bool (Set ($#k1_tarski :::"{"::: ) "A" ($#k1_tarski :::"}"::: ) ) ($#r2_hidden :::"in"::: ) it) & (Bool (Set ($#k10_eqrel_1 :::"SmallestPartition"::: ) "A") ($#r2_hidden :::"in"::: ) it) ")" ); end; :: deftheorem defines :::"Strong_Classification"::: TAXONOM1:def 2 : (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_partit1 :::"PARTITIONS"::: ) (Set (Var "A")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m2_taxonom1 :::"Strong_Classification"::: ) "of" (Set (Var "A"))) "iff" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m1_taxonom1 :::"Classification"::: ) "of" (Set (Var "A"))) & (Bool (Set ($#k1_tarski :::"{"::: ) (Set (Var "A")) ($#k1_tarski :::"}"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) & (Bool (Set ($#k10_eqrel_1 :::"SmallestPartition"::: ) (Set (Var "A"))) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) ")" ) ")" ))); theorem :: TAXONOM1:15 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_partit1 :::"PARTITIONS"::: ) (Set (Var "A")) ")" ) "st" (Bool (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "A")) ($#k1_tarski :::"}"::: ) ) "," (Set "(" ($#k10_eqrel_1 :::"SmallestPartition"::: ) (Set (Var "A")) ")" ) ($#k2_tarski :::"}"::: ) ))) "holds" (Bool (Set (Var "S")) "is" ($#m2_taxonom1 :::"Strong_Classification"::: ) "of" (Set (Var "A"))))) ; begin definitionlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Const "X")) "," (Set (Const "X")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ); let "a" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; func :::"low_toler"::: "(" "f" "," "a" ")" -> ($#m1_subset_1 :::"Relation":::) "of" "X" means :: TAXONOM1:def 3 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "X" "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) it) "iff" (Bool (Set "f" ($#k1_metric_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_xxreal_0 :::"<="::: ) "a") ")" )); end; :: deftheorem defines :::"low_toler"::: TAXONOM1: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 :::"PartFunc":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "X")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k1_taxonom1 :::"low_toler"::: ) "(" (Set (Var "f")) "," (Set (Var "a")) ")" )) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "b4"))) "iff" (Bool (Set (Set (Var "f")) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "a"))) ")" )) ")" ))))); theorem :: TAXONOM1:16 (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 :::"PartFunc":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "X")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "f")) "is" ($#v2_metric_1 :::"Reflexive"::: ) ) & (Bool (Set (Var "a")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k1_taxonom1 :::"low_toler"::: ) "(" (Set (Var "f")) "," (Set (Var "a")) ")" ) ($#r1_relat_2 :::"is_reflexive_in"::: ) (Set (Var "X")))))) ; theorem :: TAXONOM1:17 (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 :::"PartFunc":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "X")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "f")) "is" ($#v4_metric_1 :::"symmetric"::: ) )) "holds" (Bool (Set ($#k1_taxonom1 :::"low_toler"::: ) "(" (Set (Var "f")) "," (Set (Var "a")) ")" ) ($#r3_relat_2 :::"is_symmetric_in"::: ) (Set (Var "X")))))) ; theorem :: TAXONOM1:18 (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 :::"PartFunc":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "X")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "f")) "is" ($#v2_metric_1 :::"Reflexive"::: ) ) & (Bool (Set (Var "f")) "is" ($#v4_metric_1 :::"symmetric"::: ) )) "holds" (Bool (Set ($#k1_taxonom1 :::"low_toler"::: ) "(" (Set (Var "f")) "," (Set (Var "a")) ")" ) "is" ($#m1_subset_1 :::"Tolerance":::) "of" (Set (Var "X")))))) ; theorem :: TAXONOM1:19 (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 :::"PartFunc":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "X")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a1")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "a2")))) "holds" (Bool (Set ($#k1_taxonom1 :::"low_toler"::: ) "(" (Set (Var "f")) "," (Set (Var "a1")) ")" ) ($#r1_relset_1 :::"c="::: ) (Set ($#k1_taxonom1 :::"low_toler"::: ) "(" (Set (Var "f")) "," (Set (Var "a2")) ")" ))))) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Const "X")) "," (Set (Const "X")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ); attr "f" is :::"nonnegative"::: means :: TAXONOM1:def 4 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "X" "holds" (Bool (Set "f" ($#k1_metric_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) ))); end; :: deftheorem defines :::"nonnegative"::: TAXONOM1:def 4 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "X")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v1_taxonom1 :::"nonnegative"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "f")) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ")" ))); theorem :: TAXONOM1:20 (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 :::"PartFunc":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "X")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "f")) "is" ($#v1_taxonom1 :::"nonnegative"::: ) ) & (Bool (Set (Var "f")) "is" ($#v2_metric_1 :::"Reflexive"::: ) ) & (Bool (Set (Var "f")) "is" ($#v3_metric_1 :::"discerning"::: ) ) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_taxonom1 :::"low_toler"::: ) "(" (Set (Var "f")) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ))) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y")))))) ; theorem :: TAXONOM1:21 (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 :::"PartFunc":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "X")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v2_metric_1 :::"Reflexive"::: ) ) & (Bool (Set (Var "f")) "is" ($#v3_metric_1 :::"discerning"::: ) )) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "x")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_taxonom1 :::"low_toler"::: ) "(" (Set (Var "f")) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ))))) ; theorem :: TAXONOM1:22 (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 :::"PartFunc":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "X")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k1_taxonom1 :::"low_toler"::: ) "(" (Set (Var "f")) "," (Set (Var "a")) ")" ) ($#r1_relat_2 :::"is_reflexive_in"::: ) (Set (Var "X"))) & (Bool (Set (Var "f")) "is" ($#v4_metric_1 :::"symmetric"::: ) )) "holds" (Bool (Set (Set "(" ($#k1_taxonom1 :::"low_toler"::: ) "(" (Set (Var "f")) "," (Set (Var "a")) ")" ")" ) ($#k13_lang1 :::"[*]"::: ) ) "is" ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Var "X")))))) ; begin theorem :: TAXONOM1:23 (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 :::"PartFunc":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "X")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f")) "is" ($#v1_taxonom1 :::"nonnegative"::: ) ) & (Bool (Set (Var "f")) "is" ($#v2_metric_1 :::"Reflexive"::: ) ) & (Bool (Set (Var "f")) "is" ($#v3_metric_1 :::"discerning"::: ) )) "holds" (Bool (Set (Set "(" ($#k1_taxonom1 :::"low_toler"::: ) "(" (Set (Var "f")) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ")" ) ($#k13_lang1 :::"[*]"::: ) ) ($#r2_relset_1 :::"="::: ) (Set ($#k1_taxonom1 :::"low_toler"::: ) "(" (Set (Var "f")) "," (Set ($#k6_numbers :::"0"::: ) ) ")" )))) ; theorem :: TAXONOM1:24 (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 :::"PartFunc":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "X")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "R")) ($#r2_relset_1 :::"="::: ) (Set (Set "(" ($#k1_taxonom1 :::"low_toler"::: ) "(" (Set (Var "f")) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ")" ) ($#k13_lang1 :::"[*]"::: ) )) & (Bool (Set (Var "f")) "is" ($#v1_taxonom1 :::"nonnegative"::: ) ) & (Bool (Set (Var "f")) "is" ($#v2_metric_1 :::"Reflexive"::: ) ) & (Bool (Set (Var "f")) "is" ($#v3_metric_1 :::"discerning"::: ) )) "holds" (Bool (Set (Var "R")) ($#r1_hidden :::"="::: ) (Set ($#k4_relat_1 :::"id"::: ) (Set (Var "X"))))))) ; theorem :: TAXONOM1:25 (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 :::"PartFunc":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "X")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "R")) ($#r2_relset_1 :::"="::: ) (Set (Set "(" ($#k1_taxonom1 :::"low_toler"::: ) "(" (Set (Var "f")) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ")" ) ($#k13_lang1 :::"[*]"::: ) )) & (Bool (Set (Var "f")) "is" ($#v1_taxonom1 :::"nonnegative"::: ) ) & (Bool (Set (Var "f")) "is" ($#v2_metric_1 :::"Reflexive"::: ) ) & (Bool (Set (Var "f")) "is" ($#v3_metric_1 :::"discerning"::: ) )) "holds" (Bool (Set ($#k8_eqrel_1 :::"Class"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set ($#k10_eqrel_1 :::"SmallestPartition"::: ) (Set (Var "X"))))))) ; theorem :: TAXONOM1:26 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "X")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "z")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "f")))) & (Bool (Set (Var "A")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k1_xxreal_2 :::"max"::: ) (Set (Var "z"))))) "holds" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "f")) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "A")))))))) ; theorem :: TAXONOM1:27 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "X")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "z")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "f")))) & (Bool (Set (Var "A")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k1_xxreal_2 :::"max"::: ) (Set (Var "z"))))) "holds" (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "R")) ($#r2_relset_1 :::"="::: ) (Set (Set "(" ($#k1_taxonom1 :::"low_toler"::: ) "(" (Set (Var "f")) "," (Set (Var "A")) ")" ")" ) ($#k13_lang1 :::"[*]"::: ) ))) "holds" (Bool (Set ($#k8_eqrel_1 :::"Class"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "X")) ($#k1_tarski :::"}"::: ) ))))))) ; theorem :: TAXONOM1:28 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "X")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "z")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "f")))) & (Bool (Set (Var "A")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k1_xxreal_2 :::"max"::: ) (Set (Var "z"))))) "holds" (Bool (Set (Set "(" ($#k1_taxonom1 :::"low_toler"::: ) "(" (Set (Var "f")) "," (Set (Var "A")) ")" ")" ) ($#k13_lang1 :::"[*]"::: ) ) ($#r2_relset_1 :::"="::: ) (Set ($#k1_taxonom1 :::"low_toler"::: ) "(" (Set (Var "f")) "," (Set (Var "A")) ")" )))))) ; begin definitionlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Const "X")) "," (Set (Const "X")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ); func :::"fam_class"::: "f" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_partit1 :::"PARTITIONS"::: ) "X" ")" ) means :: TAXONOM1:def 5 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "ex" (Set (Var "a")) "being" ($#~v3_xxreal_0 "non" ($#v3_xxreal_0 :::"negative"::: ) ) ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "ex" (Set (Var "R")) "being" ($#m1_subset_1 :::"Equivalence_Relation":::) "of" "X" "st" (Bool "(" (Bool (Set (Var "R")) ($#r2_relset_1 :::"="::: ) (Set (Set "(" ($#k1_taxonom1 :::"low_toler"::: ) "(" "f" "," (Set (Var "a")) ")" ")" ) ($#k13_lang1 :::"[*]"::: ) )) & (Bool (Set ($#k8_eqrel_1 :::"Class"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set (Var "x"))) ")" ))) ")" )); end; :: deftheorem defines :::"fam_class"::: TAXONOM1:def 5 : (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 :::"PartFunc":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "X")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_partit1 :::"PARTITIONS"::: ) (Set (Var "X")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k2_taxonom1 :::"fam_class"::: ) (Set (Var "f")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b3"))) "iff" (Bool "ex" (Set (Var "a")) "being" ($#~v3_xxreal_0 "non" ($#v3_xxreal_0 :::"negative"::: ) ) ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "ex" (Set (Var "R")) "being" ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Var "X")) "st" (Bool "(" (Bool (Set (Var "R")) ($#r2_relset_1 :::"="::: ) (Set (Set "(" ($#k1_taxonom1 :::"low_toler"::: ) "(" (Set (Var "f")) "," (Set (Var "a")) ")" ")" ) ($#k13_lang1 :::"[*]"::: ) )) & (Bool (Set ($#k8_eqrel_1 :::"Class"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set (Var "x"))) ")" ))) ")" )) ")" )))); theorem :: TAXONOM1:29 (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 :::"PartFunc":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "X")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#~v3_xxreal_0 "non" ($#v3_xxreal_0 :::"negative"::: ) ) ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k1_taxonom1 :::"low_toler"::: ) "(" (Set (Var "f")) "," (Set (Var "a")) ")" ) ($#r1_relat_2 :::"is_reflexive_in"::: ) (Set (Var "X"))) & (Bool (Set (Var "f")) "is" ($#v4_metric_1 :::"symmetric"::: ) )) "holds" (Bool (Set ($#k2_taxonom1 :::"fam_class"::: ) (Set (Var "f"))) "is" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) )))) ; theorem :: TAXONOM1:30 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "X")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f")) "is" ($#v4_metric_1 :::"symmetric"::: ) ) & (Bool (Set (Var "f")) "is" ($#v1_taxonom1 :::"nonnegative"::: ) )) "holds" (Bool (Set ($#k1_tarski :::"{"::: ) (Set (Var "X")) ($#k1_tarski :::"}"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_taxonom1 :::"fam_class"::: ) (Set (Var "f")))))) ; theorem :: TAXONOM1:31 (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 :::"PartFunc":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "X")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set ($#k2_taxonom1 :::"fam_class"::: ) (Set (Var "f"))) "is" ($#m1_taxonom1 :::"Classification"::: ) "of" (Set (Var "X"))))) ; theorem :: TAXONOM1:32 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "X")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set ($#k10_eqrel_1 :::"SmallestPartition"::: ) (Set (Var "X"))) ($#r2_hidden :::"in"::: ) (Set ($#k2_taxonom1 :::"fam_class"::: ) (Set (Var "f")))) & (Bool (Set (Var "f")) "is" ($#v4_metric_1 :::"symmetric"::: ) ) & (Bool (Set (Var "f")) "is" ($#v1_taxonom1 :::"nonnegative"::: ) )) "holds" (Bool (Set ($#k2_taxonom1 :::"fam_class"::: ) (Set (Var "f"))) "is" ($#m2_taxonom1 :::"Strong_Classification"::: ) "of" (Set (Var "X"))))) ; begin definitionlet "M" be ($#l1_metric_1 :::"MetrStruct"::: ) ; let "a" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; let "x", "y" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "M")); pred "x" "," "y" :::"are_in_tolerance_wrt"::: "a" means :: TAXONOM1:def 6 (Bool (Set ($#k2_metric_1 :::"dist"::: ) "(" "x" "," "y" ")" ) ($#r1_xxreal_0 :::"<="::: ) "a"); end; :: deftheorem defines :::"are_in_tolerance_wrt"::: TAXONOM1:def 6 : (Bool "for" (Set (Var "M")) "being" ($#l1_metric_1 :::"MetrStruct"::: ) (Bool "for" (Set (Var "a")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "holds" (Bool "(" (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r1_taxonom1 :::"are_in_tolerance_wrt"::: ) (Set (Var "a"))) "iff" (Bool (Set ($#k2_metric_1 :::"dist"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "a"))) ")" )))); definitionlet "M" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrStruct"::: ) ; let "a" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; func :::"dist_toler"::: "(" "M" "," "a" ")" -> ($#m1_subset_1 :::"Relation":::) "of" "M" means :: TAXONOM1:def 7 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" "M" "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) it) "iff" (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r1_taxonom1 :::"are_in_tolerance_wrt"::: ) "a") ")" )); end; :: deftheorem defines :::"dist_toler"::: TAXONOM1:def 7 : (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrStruct"::: ) (Bool "for" (Set (Var "a")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "M")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k3_taxonom1 :::"dist_toler"::: ) "(" (Set (Var "M")) "," (Set (Var "a")) ")" )) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "b3"))) "iff" (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r1_taxonom1 :::"are_in_tolerance_wrt"::: ) (Set (Var "a"))) ")" )) ")" )))); theorem :: TAXONOM1:33 (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrStruct"::: ) (Bool "for" (Set (Var "a")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k3_taxonom1 :::"dist_toler"::: ) "(" (Set (Var "M")) "," (Set (Var "a")) ")" ) ($#r2_relset_1 :::"="::: ) (Set ($#k1_taxonom1 :::"low_toler"::: ) "(" (Set "the" ($#u1_metric_1 :::"distance"::: ) "of" (Set (Var "M"))) "," (Set (Var "a")) ")" )))) ; theorem :: TAXONOM1:34 (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v6_metric_1 :::"Reflexive"::: ) ($#v8_metric_1 :::"symmetric"::: ) ($#l1_metric_1 :::"MetrStruct"::: ) (Bool "for" (Set (Var "a")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "T")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) "st" (Bool (Bool (Set (Var "T")) ($#r2_relset_1 :::"="::: ) (Set ($#k3_taxonom1 :::"dist_toler"::: ) "(" (Set (Var "M")) "," (Set (Var "a")) ")" )) & (Bool (Set (Var "a")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Var "T")) "is" ($#m1_subset_1 :::"Tolerance":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))))))) ; definitionlet "M" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v6_metric_1 :::"Reflexive"::: ) ($#v8_metric_1 :::"symmetric"::: ) ($#l1_metric_1 :::"MetrStruct"::: ) ; func :::"fam_class_metr"::: "M" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_partit1 :::"PARTITIONS"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "M") ")" ) means :: TAXONOM1:def 8 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "ex" (Set (Var "a")) "being" ($#~v3_xxreal_0 "non" ($#v3_xxreal_0 :::"negative"::: ) ) ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "ex" (Set (Var "R")) "being" ($#m1_subset_1 :::"Equivalence_Relation":::) "of" "M" "st" (Bool "(" (Bool (Set (Var "R")) ($#r2_relset_1 :::"="::: ) (Set (Set "(" ($#k3_taxonom1 :::"dist_toler"::: ) "(" "M" "," (Set (Var "a")) ")" ")" ) ($#k13_lang1 :::"[*]"::: ) )) & (Bool (Set ($#k8_eqrel_1 :::"Class"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set (Var "x"))) ")" ))) ")" )); end; :: deftheorem defines :::"fam_class_metr"::: TAXONOM1:def 8 : (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v6_metric_1 :::"Reflexive"::: ) ($#v8_metric_1 :::"symmetric"::: ) ($#l1_metric_1 :::"MetrStruct"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_partit1 :::"PARTITIONS"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ")" ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k4_taxonom1 :::"fam_class_metr"::: ) (Set (Var "M")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) "iff" (Bool "ex" (Set (Var "a")) "being" ($#~v3_xxreal_0 "non" ($#v3_xxreal_0 :::"negative"::: ) ) ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "ex" (Set (Var "R")) "being" ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Var "M")) "st" (Bool "(" (Bool (Set (Var "R")) ($#r2_relset_1 :::"="::: ) (Set (Set "(" ($#k3_taxonom1 :::"dist_toler"::: ) "(" (Set (Var "M")) "," (Set (Var "a")) ")" ")" ) ($#k13_lang1 :::"[*]"::: ) )) & (Bool (Set ($#k8_eqrel_1 :::"Class"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set (Var "x"))) ")" ))) ")" )) ")" ))); theorem :: TAXONOM1:35 (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v6_metric_1 :::"Reflexive"::: ) ($#v8_metric_1 :::"symmetric"::: ) ($#l1_metric_1 :::"MetrStruct"::: ) "holds" (Bool (Set ($#k4_taxonom1 :::"fam_class_metr"::: ) (Set (Var "M"))) ($#r1_hidden :::"="::: ) (Set ($#k2_taxonom1 :::"fam_class"::: ) (Set "the" ($#u1_metric_1 :::"distance"::: ) "of" (Set (Var "M")))))) ; theorem :: TAXONOM1:36 (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "R")) ($#r2_relset_1 :::"="::: ) (Set (Set "(" ($#k3_taxonom1 :::"dist_toler"::: ) "(" (Set (Var "M")) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ")" ) ($#k13_lang1 :::"[*]"::: ) ))) "holds" (Bool (Set ($#k8_eqrel_1 :::"Class"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set ($#k10_eqrel_1 :::"SmallestPartition"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))))))) ; theorem :: TAXONOM1:37 (Bool "for" (Set (Var "a")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v6_metric_1 :::"Reflexive"::: ) ($#v8_metric_1 :::"symmetric"::: ) ($#v5_tbsp_1 :::"bounded"::: ) ($#l1_metric_1 :::"MetrStruct"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_tbsp_1 :::"diameter"::: ) (Set "(" ($#k2_struct_0 :::"[#]"::: ) (Set (Var "M")) ")" )))) "holds" (Bool (Set ($#k3_taxonom1 :::"dist_toler"::: ) "(" (Set (Var "M")) "," (Set (Var "a")) ")" ) ($#r2_relset_1 :::"="::: ) (Set ($#k1_eqrel_1 :::"nabla"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))))))) ; theorem :: TAXONOM1:38 (Bool "for" (Set (Var "a")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v6_metric_1 :::"Reflexive"::: ) ($#v8_metric_1 :::"symmetric"::: ) ($#v5_tbsp_1 :::"bounded"::: ) ($#l1_metric_1 :::"MetrStruct"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_tbsp_1 :::"diameter"::: ) (Set "(" ($#k2_struct_0 :::"[#]"::: ) (Set (Var "M")) ")" )))) "holds" (Bool (Set ($#k3_taxonom1 :::"dist_toler"::: ) "(" (Set (Var "M")) "," (Set (Var "a")) ")" ) ($#r2_relset_1 :::"="::: ) (Set (Set "(" ($#k3_taxonom1 :::"dist_toler"::: ) "(" (Set (Var "M")) "," (Set (Var "a")) ")" ")" ) ($#k13_lang1 :::"[*]"::: ) )))) ; theorem :: TAXONOM1:39 (Bool "for" (Set (Var "a")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v6_metric_1 :::"Reflexive"::: ) ($#v8_metric_1 :::"symmetric"::: ) ($#v5_tbsp_1 :::"bounded"::: ) ($#l1_metric_1 :::"MetrStruct"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_tbsp_1 :::"diameter"::: ) (Set "(" ($#k2_struct_0 :::"[#]"::: ) (Set (Var "M")) ")" )))) "holds" (Bool (Set (Set "(" ($#k3_taxonom1 :::"dist_toler"::: ) "(" (Set (Var "M")) "," (Set (Var "a")) ")" ")" ) ($#k13_lang1 :::"[*]"::: ) ) ($#r2_relset_1 :::"="::: ) (Set ($#k1_eqrel_1 :::"nabla"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))))))) ; theorem :: TAXONOM1:40 (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v6_metric_1 :::"Reflexive"::: ) ($#v8_metric_1 :::"symmetric"::: ) ($#v5_tbsp_1 :::"bounded"::: ) ($#l1_metric_1 :::"MetrStruct"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Var "M")) (Bool "for" (Set (Var "a")) "being" ($#~v3_xxreal_0 "non" ($#v3_xxreal_0 :::"negative"::: ) ) ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_tbsp_1 :::"diameter"::: ) (Set "(" ($#k2_struct_0 :::"[#]"::: ) (Set (Var "M")) ")" ))) & (Bool (Set (Var "R")) ($#r2_relset_1 :::"="::: ) (Set (Set "(" ($#k3_taxonom1 :::"dist_toler"::: ) "(" (Set (Var "M")) "," (Set (Var "a")) ")" ")" ) ($#k13_lang1 :::"[*]"::: ) ))) "holds" (Bool (Set ($#k8_eqrel_1 :::"Class"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ($#k1_tarski :::"}"::: ) ))))) ; registrationlet "M" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v6_metric_1 :::"Reflexive"::: ) ($#v8_metric_1 :::"symmetric"::: ) ($#v9_metric_1 :::"triangle"::: ) ($#l1_metric_1 :::"MetrStruct"::: ) ; let "C" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v6_tbsp_1 :::"bounded"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "M")); cluster (Set ($#k3_tbsp_1 :::"diameter"::: ) "C") -> ($#~v3_xxreal_0 "non" ($#v3_xxreal_0 :::"negative"::: ) ) ; end; theorem :: TAXONOM1:41 (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_tbsp_1 :::"bounded"::: ) ($#l1_metric_1 :::"MetrSpace":::) "holds" (Bool (Set ($#k1_tarski :::"{"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ($#k1_tarski :::"}"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k4_taxonom1 :::"fam_class_metr"::: ) (Set (Var "M"))))) ; theorem :: TAXONOM1:42 (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v6_metric_1 :::"Reflexive"::: ) ($#v8_metric_1 :::"symmetric"::: ) ($#l1_metric_1 :::"MetrStruct"::: ) "holds" (Bool (Set ($#k4_taxonom1 :::"fam_class_metr"::: ) (Set (Var "M"))) "is" ($#m1_taxonom1 :::"Classification"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))))) ; theorem :: TAXONOM1:43 (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_tbsp_1 :::"bounded"::: ) ($#l1_metric_1 :::"MetrSpace":::) "holds" (Bool (Set ($#k4_taxonom1 :::"fam_class_metr"::: ) (Set (Var "M"))) "is" ($#m2_taxonom1 :::"Strong_Classification"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))))) ;