:: TAXONOM2 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

definition
let A be RelStr ;
attr A is with_superior means :: TAXONOM2:def 1
 ex x being Element of A st x is_superior_of the InternalRel of A;
end;

:: deftheorem defines with_superior TAXONOM2:def 1 :
for A being RelStr holds
( A is with_superior iff ex x being Element of A st x is_superior_of the InternalRel of A );

definition
let A be RelStr ;
attr A is with_comparable_down means :Def2: :: TAXONOM2:def 2
for x, y being Element of A holds
( for z being Element of A holds
( not z <= x or not z <= y ) or x <= y or y <= x );
end;

:: deftheorem Def2 defines with_comparable_down TAXONOM2:def 2 :
for A being RelStr holds
( A is with_comparable_down iff for x, y being Element of A holds
( for z being Element of A holds
( not z <= x or not z <= y ) or x <= y or y <= x ) );

theorem Th1: :: TAXONOM2:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being set holds
( not InclPoset {{a}} is empty & InclPoset {{a}} is reflexive & InclPoset {{a}} is transitive & InclPoset {{a}} is antisymmetric & InclPoset {{a}} is with_superior & InclPoset {{a}} is with_comparable_down )
proof end;

registration
cluster non empty strict reflexive transitive antisymmetric with_superior with_comparable_down RelStr ;
existence
ex b1 being RelStr st
( not b1 is empty & b1 is reflexive & b1 is transitive & b1 is antisymmetric & b1 is with_superior & b1 is with_comparable_down & b1 is strict )
proof end;
end;

definition
mode Tree is with_superior with_comparable_down Poset;
end;

theorem Th2: :: TAXONOM2:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty set
for EqR being Equivalence_Relation of X
for x, y, z being set st z in Class EqR,x & z in Class EqR,y holds
Class EqR,x = Class EqR,y
proof end;

theorem Th3: :: TAXONOM2:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty set
for P being a_partition of X
for x, y, z being set st x in P & y in P & z in x & z in y holds
x = y
proof end;

theorem Th4: :: TAXONOM2:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty set
for C, x being set st C is Classification of X & x in union C holds
x c= X
proof end;

theorem :: TAXONOM2:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty set
for C being set st C is Strong_Classification of X holds
InclPoset (union C) is Tree
proof end;

definition
let Y be set ;
attr Y is hierarchic means :Def3: :: TAXONOM2:def 3
for x, y being set st x in Y & y in Y & not x c= y & not y c= x holds
x misses y;
end;

:: deftheorem Def3 defines hierarchic TAXONOM2:def 3 :
for Y being set holds
( Y is hierarchic iff for x, y being set st x in Y & y in Y & not x c= y & not y c= x holds
x misses y );

registration
cluster trivial -> hierarchic set ;
coherence
for b1 being set st b1 is trivial holds
b1 is hierarchic
proof end;
end;

registration
cluster non trivial hierarchic set ;
existence
ex b1 being set st
( not b1 is trivial & b1 is hierarchic )
proof end;
end;

theorem Th6: :: TAXONOM2:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
{} is hierarchic
proof end;

theorem :: TAXONOM2:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
{{} } is hierarchic
proof end;

definition
let Y be set ;
mode Hierarchy of Y -> Subset-Family of Y means :Def4: :: TAXONOM2:def 4
it is hierarchic;
existence
ex b1 being Subset-Family of Y st b1 is hierarchic
proof end;
end;

:: deftheorem Def4 defines Hierarchy TAXONOM2:def 4 :
for Y being set
for b2 being Subset-Family of Y holds
( b2 is Hierarchy of Y iff b2 is hierarchic );

definition
let Y be set ;
attr Y is mutually-disjoint means :Def5: :: TAXONOM2:def 5
for x, y being set st x in Y & y in Y & x <> y holds
x misses y;
end;

:: deftheorem Def5 defines mutually-disjoint TAXONOM2:def 5 :
for Y being set holds
( Y is mutually-disjoint iff for x, y being set st x in Y & y in Y & x <> y holds
x misses y );

Lm1: now
let x, y be set ; :: thesis: ( x in {{} } & y in {{} } & x <> y implies x misses y )
assume A1: ( x in {{} } & y in {{} } & x <> y ) ; :: thesis: x misses y
( x = {} & y = {} ) by A1, TARSKI:def 1;
hence x misses y by A1; :: thesis: verum
end;

registration
let Y be set ;
cluster mutually-disjoint Element of bool (bool Y);
existence
ex b1 being Subset-Family of Y st b1 is mutually-disjoint
proof end;
end;

theorem :: TAXONOM2:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
{} is mutually-disjoint
proof end;

theorem :: TAXONOM2:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
{{} } is mutually-disjoint by Def5, Lm1;

theorem Th10: :: TAXONOM2:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being set holds {a} is mutually-disjoint
proof end;

Lm2: now
let Y be set ; :: thesis: for H being Hierarchy of Y st H is covering holds
for B being mutually-disjoint Subset-Family of Y st B c= H & ( for C being mutually-disjoint Subset-Family of Y st C c= H & union B c= union C holds
B = C ) holds
union B = Y
let H be Hierarchy of Y; :: thesis: ( H is covering implies for B being mutually-disjoint Subset-Family of Y st B c= H & ( for C being mutually-disjoint Subset-Family of Y st C c= H & union B c= union C holds
B = C ) holds
union B = Y )
assume A1: H is covering ; :: thesis: for B being mutually-disjoint Subset-Family of Y st B c= H & ( for C being mutually-disjoint Subset-Family of Y st C c= H & union B c= union C holds
B = C ) holds
union B = Y
let B be mutually-disjoint Subset-Family of Y; :: thesis: ( B c= H & ( for C being mutually-disjoint Subset-Family of Y st C c= H & union B c= union C holds
B = C ) implies union B = Y )
assume A2: ( B c= H & ( for C being mutually-disjoint Subset-Family of Y st C c= H & union B c= union C holds
B = C ) ) ; :: thesis: union B = Y
thus union B = Y :: thesis: verum
proof
thus union B c= Y ; :: according to XBOOLE_0:def 10 :: thesis: Y c= union B
thus Y c= union B :: thesis: verum
proof
let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in Y or y in union B )
assume A3: y in Y ; :: thesis: y in union B
y in union H by A1, A3, ABIAN:4;
then consider x being set such that
A4: ( y in x & x in H ) by TARSKI:def 4;
now
assume A5: not y in union B ; :: thesis: contradiction
defpred S1[ set ] means $1 c= x;
consider D being set such that
A6: for a being set holds
( a in D iff ( a in B & S1[a] ) ) from XBOOLE_0:sch 1( RL );
set C = (B \ D) \/ {x};
x in {x} by TARSKI:def 1;
then A7: x in (B \ D) \/ {x} by XBOOLE_0:def 2;
A8: B \ D c= (B \ D) \/ {x} by XBOOLE_1:7;
B \ D c= B by XBOOLE_1:36;
then A9: B \ D c= H by A2, XBOOLE_1:1;
{x} c= H
proof
let s be set ; :: according to TARSKI:def 3 :: thesis: ( not s in {x} or s in H )
assume A10: s in {x} ; :: thesis: s in H
thus s in H by A4, A10, TARSKI:def 1; :: thesis: verum
end;
then A11: (B \ D) \/ {x} c= H by A9, XBOOLE_1:8;
then A12: (B \ D) \/ {x} c= bool Y by XBOOLE_1:1;
A13: for p being set st p in B & not p in D & p <> x holds
p misses x
proof
let p be set ; :: thesis: ( p in B & not p in D & p <> x implies p misses x )
assume A14: ( p in B & not p in D & p <> x ) ; :: thesis: p misses x
A15: not p c= x by A6, A14;
A16: not x c= p by A4, A5, A14, TARSKI:def 4;
H is hierarchic by Def4;
hence p misses x by A2, A4, A14, A15, A16, Def3; :: thesis: verum
end;
for p, q being set st p in (B \ D) \/ {x} & q in (B \ D) \/ {x} & p <> q holds
p misses q
proof
let p, q be set ; :: thesis: ( p in (B \ D) \/ {x} & q in (B \ D) \/ {x} & p <> q implies p misses q )
assume A17: ( p in (B \ D) \/ {x} & q in (B \ D) \/ {x} & p <> q ) ; :: thesis: p misses q
per cases ( p in B \ D or p in {x} ) by A17, XBOOLE_0:def 2;
suppose p in B \ D ; :: thesis: p misses q
then A18: ( p in B & not p in D ) by XBOOLE_0:def 4;
per cases ( q in B \ D or q in {x} ) by A17, XBOOLE_0:def 2;
suppose q in B \ D ; :: thesis: p misses q
then ( q in B & not q in D ) by XBOOLE_0:def 4;
hence p misses q by A17, A18, Def5; :: thesis: verum
end;
suppose q in {x} ; :: thesis: p misses q
then q = x by TARSKI:def 1;
hence p misses q by A13, A17, A18; :: thesis: verum
end;
end;
end;
suppose p in {x} ; :: thesis: p misses q
then A19: p = x by TARSKI:def 1;
per cases ( q in B \ D or q in {x} ) by A17, XBOOLE_0:def 2;
suppose q in B \ D ; :: thesis: p misses q
then ( q in B & not q in D ) by XBOOLE_0:def 4;
hence p misses q by A13, A17, A19; :: thesis: verum
end;
suppose q in {x} ; :: thesis: p misses q
hence p misses q by A17, A19, TARSKI:def 1; :: thesis: verum
end;
end;
end;
end;
end;
then A20: (B \ D) \/ {x} is mutually-disjoint Subset-Family of Y by A12, Def5;
union B c= union ((B \ D) \/ {x})
proof
let s be set ; :: according to TARSKI:def 3 :: thesis: ( not s in union B or s in union ((B \ D) \/ {x}) )
assume A21: s in union B ; :: thesis: s in union ((B \ D) \/ {x})
consider t being set such that
A22: ( s in t & t in B ) by A21, TARSKI:def 4;
per cases ( t in D or not t in D ) ;
suppose t in D ; :: thesis: s in union ((B \ D) \/ {x})
then t c= x by A6;
hence s in union ((B \ D) \/ {x}) by A7, A22, TARSKI:def 4; :: thesis: verum
end;
suppose not t in D ; :: thesis: s in union ((B \ D) \/ {x})
then t in B \ D by A22, XBOOLE_0:def 4;
hence s in union ((B \ D) \/ {x}) by A8, A22, TARSKI:def 4; :: thesis: verum
end;
end;
end;
then A23: B = (B \ D) \/ {x} by A2, A11, A20;
A24: {x} c= (B \ D) \/ {x} by XBOOLE_1:7;
x in {x} by TARSKI:def 1;
hence contradiction by A4, A5, A23, A24, TARSKI:def 4; :: thesis: verum
end;
hence y in union B ; :: thesis: verum
end;
end;
end;

Lm3: now
let Y be set ; :: thesis: for H being Hierarchy of Y
for B being mutually-disjoint Subset-Family of Y st B c= H & ( for C being mutually-disjoint Subset-Family of Y st C c= H & union B c= union C holds
B = C ) holds
for S1 being Subset of Y st S1 in B holds
S1 <> {}
let H be Hierarchy of Y; :: thesis: for B being mutually-disjoint Subset-Family of Y st B c= H & ( for C being mutually-disjoint Subset-Family of Y st C c= H & union B c= union C holds
B = C ) holds
for S1 being Subset of Y st S1 in B holds
S1 <> {}
let B be mutually-disjoint Subset-Family of Y; :: thesis: ( B c= H & ( for C being mutually-disjoint Subset-Family of Y st C c= H & union B c= union C holds
B = C ) implies for S1 being Subset of Y st S1 in B holds
S1 <> {} )
assume A1: ( B c= H & ( for C being mutually-disjoint Subset-Family of Y st C c= H & union B c= union C holds
B = C ) ) ; :: thesis: for S1 being Subset of Y st S1 in B holds
S1 <> {}
let S1 be Subset of Y; :: thesis: ( S1 in B implies S1 <> {} )
assume A2: S1 in B ; :: thesis: S1 <> {}
now
assume A3: S1 = {} ; :: thesis: contradiction
set C = B \ {{} };
A4: union B c= union (B \ {{} })
proof
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in union B or x in union (B \ {{} }) )
assume A5: x in union B ; :: thesis: x in union (B \ {{} })
consider y being set such that
A6: ( x in y & y in B ) by A5, TARSKI:def 4;
not y in {{} } by A6, TARSKI:def 1;
then y in B \ {{} } by A6, XBOOLE_0:def 4;
hence x in union (B \ {{} }) by A6, TARSKI:def 4; :: thesis: verum
end;
A7: B \ {{} } c= B by XBOOLE_1:36;
then A8: B \ {{} } c= H by A1, XBOOLE_1:1;
B \ {{} } c= bool Y by A7, XBOOLE_1:1;
then A9: B \ {{} } is Subset-Family of Y ;
B \ {{} } is mutually-disjoint
proof
let x, y be set ; :: according to TAXONOM2:def 5 :: thesis: ( x in B \ {{} } & y in B \ {{} } & x <> y implies x misses y )
assume A10: ( x in B \ {{} } & y in B \ {{} } & x <> y ) ; :: thesis: x misses y
( x in B & y in B ) by A10, XBOOLE_0:def 4;
hence x misses y by A10, Def5; :: thesis: verum
end;
then B = B \ {{} } by A1, A4, A8, A9;
then not {} in {{} } by A2, A3, XBOOLE_0:def 4;
hence contradiction by TARSKI:def 1; :: thesis: verum
end;
hence S1 <> {} ; :: thesis: verum
end;

definition
let Y be set ;
let F be Subset-Family of Y;
attr F is T_3 means :Def6: :: TAXONOM2:def 6
for A being Subset of Y st A in F holds
for x being Element of Y st not x in A holds
ex B being Subset of Y st
( x in B & B in F & A misses B );
end;

:: deftheorem Def6 defines T_3 TAXONOM2:def 6 :
for Y being set
for F being Subset-Family of Y holds
( F is T_3 iff for A being Subset of Y st A in F holds
for x being Element of Y st not x in A holds
ex B being Subset of Y st
( x in B & B in F & A misses B ) );

theorem Th11: :: TAXONOM2:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Y being set
for F being Subset-Family of Y st F = {} holds
F is T_3
proof end;

registration
let Y be set ;
cluster covering T_3 Hierarchy of Y;
existence
ex b1 being Hierarchy of Y st
( b1 is covering & b1 is T_3 )
proof end;
end;

definition
let Y be set ;
let F be Subset-Family of Y;
attr F is lower-bounded means :Def7: :: TAXONOM2:def 7
for B being set st B <> {} & B c= F & B is c=-linear holds
ex c being set st
( c in F & c c= meet B );
end;

:: deftheorem Def7 defines lower-bounded TAXONOM2:def 7 :
for Y being set
for F being Subset-Family of Y holds
( F is lower-bounded iff for B being set st B <> {} & B c= F & B is c=-linear holds
ex c being set st
( c in F & c c= meet B ) );

theorem Th12: :: TAXONOM2:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Y being set
for S1 being Subset of Y
for B being mutually-disjoint Subset-Family of Y st ( for b being set st b in B holds
( S1 misses b & Y <> {} ) ) holds
( B \/ {S1} is mutually-disjoint Subset-Family of Y & ( S1 <> {} implies union (B \/ {S1}) <> union B ) )
proof end;

definition
let Y be set ;
let F be Subset-Family of Y;
attr F is with_max's means :Def8: :: TAXONOM2:def 8
for S being Subset of Y st S in F holds
ex T being Subset of Y st
( S c= T & T in F & ( for V being Subset of Y st T c= V & V in F holds
V = Y ) );
end;

:: deftheorem Def8 defines with_max's TAXONOM2:def 8 :
for Y being set
for F being Subset-Family of Y holds
( F is with_max's iff for S being Subset of Y st S in F holds
ex T being Subset of Y st
( S c= T & T in F & ( for V being Subset of Y st T c= V & V in F holds
V = Y ) ) );

theorem :: TAXONOM2:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Y being set
for H being covering Hierarchy of Y st H is with_max's holds
ex P being a_partition of Y st P c= H
proof end;

theorem :: TAXONOM2:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Y being set
for H being covering Hierarchy of Y
for B being mutually-disjoint Subset-Family of Y st B c= H & ( for C being mutually-disjoint Subset-Family of Y st C c= H & union B c= union C holds
B = C ) holds
B is a_partition of Y
proof end;

theorem :: TAXONOM2:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Y being set
for H being covering T_3 Hierarchy of Y st H is lower-bounded & not {} in H holds
for A being Subset of Y
for B being mutually-disjoint Subset-Family of Y st A in B & B c= H & ( for C being mutually-disjoint Subset-Family of Y st A in C & C c= H & union B c= union C holds
union B = union C ) holds
B is a_partition of Y
proof end;

theorem Th16: :: TAXONOM2:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Y being set
for H being covering T_3 Hierarchy of Y st H is lower-bounded & not {} in H holds
for A being Subset of Y
for B being mutually-disjoint Subset-Family of Y st A in B & B c= H & ( for C being mutually-disjoint Subset-Family of Y st A in C & C c= H & B c= C holds
B = C ) holds
B is a_partition of Y
proof end;

theorem Th17: :: TAXONOM2:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Y being set
for H being covering T_3 Hierarchy of Y st H is lower-bounded & not {} in H holds
for A being Subset of Y st A in H holds
ex P being a_partition of Y st
( A in P & P c= H )
proof end;

Lm4: now
let x be non empty set ; :: thesis: for y being set st x c= y holds
x meets y
let y be set ; :: thesis: ( x c= y implies x meets y )
assume A1: x c= y ; :: thesis: x meets y
consider a being set such that
A2: a in x by XBOOLE_0:def 1;
thus x meets y by A1, A2, XBOOLE_0:3; :: thesis: verum
end;

theorem Th18: :: TAXONOM2:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, h being non empty set
for Pmin being a_partition of X
for hw being set st hw in Pmin & h c= hw holds
for PS being a_partition of X st h in PS & ( for x being set holds
( not x in PS or x c= hw or hw c= x or hw misses x ) ) holds
for PT being set st ( for a being set holds
( a in PT iff ( a in PS & a c= hw ) ) ) holds
( PT \/ (Pmin \ {hw}) is a_partition of X & PT \/ (Pmin \ {hw}) is_finer_than Pmin )
proof end;

theorem Th19: :: TAXONOM2:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, h being non empty set st h c= X holds
for Pmax being a_partition of X st ex hy being set st
( hy in Pmax & hy c= h ) & ( for x being set holds
( not x in Pmax or x c= h or h c= x or h misses x ) ) holds
for Pb being set st ( for x being set holds
( x in Pb iff ( x in Pmax & x misses h ) ) ) holds
( Pb \/ {h} is a_partition of X & Pmax is_finer_than Pb \/ {h} & ( for Pmin being a_partition of X st Pmax is_finer_than Pmin holds
for hw being set st hw in Pmin & h c= hw holds
Pb \/ {h} is_finer_than Pmin ) )
proof end;

theorem :: TAXONOM2:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty set
for H being covering T_3 Hierarchy of X st H is lower-bounded & not {} in H & ( for C1 being set st C1 <> {} & C1 c= PARTITIONS X & ( for P1, P2 being set st P1 in C1 & P2 in C1 & not P1 is_finer_than P2 holds
P2 is_finer_than P1 ) holds
ex PX, PY being set st
( PX in C1 & PY in C1 & ( for PZ being set st PZ in C1 holds
( PZ is_finer_than PY & PX is_finer_than PZ ) ) ) ) holds
ex C being Classification of X st union C = H
proof end;