:: TREES_A semantic presentation

begin

theorem :: TREES_A:1
for p, q, r, s being ( ( Relation-like Function-like FinSequence-like ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence) st p : ( ( Relation-like Function-like FinSequence-like ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence) ^ q : ( ( Relation-like Function-like FinSequence-like ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence) : ( ( Relation-like Function-like FinSequence-like ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like V39() FinSequence-like FinSubsequence-like ) set ) = s : ( ( Relation-like Function-like FinSequence-like ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence) ^ r : ( ( Relation-like Function-like FinSequence-like ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence) : ( ( Relation-like Function-like FinSequence-like ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like V39() FinSequence-like FinSubsequence-like ) set ) holds
p : ( ( Relation-like Function-like FinSequence-like ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence) ,s : ( ( Relation-like Function-like FinSequence-like ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence) are_c=-comparable ;

definition
let T, T1 be ( ( non empty Tree-like ) ( non empty Tree-like ) Tree) ;
let P be ( ( ) ( AntiChain_of_Prefixes-like ) AntiChain_of_Prefixes of T : ( ( non empty Tree-like ) ( non empty Tree-like ) Tree) ) ;
assume P : ( ( ) ( AntiChain_of_Prefixes-like ) AntiChain_of_Prefixes of T : ( ( non empty Tree-like ) ( non empty Tree-like ) Tree) ) <> {} : ( ( ) ( empty functional V32() V33() V34() V35() V36() V37() V38() FinSequence-membered ) set ) ;
func tree (T,P,T1) -> ( ( non empty Tree-like ) ( non empty Tree-like ) Tree) means :: TREES_A:def 1
 for q being ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) holds
( q : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) in it : ( ( ) ( ) set ) iff ( ( q : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) in T : ( ( non empty V39() Tree-like ) ( non empty V39() Tree-like ) set ) & ( for p being ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) st p : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) in P : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) set ) holds
not p : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) is_a_proper_prefix_of q : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) or ex p, r being ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) st
( p : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) in P : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) set ) & r : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) in T1 : ( ( ) ( ) Element of T : ( ( non empty V39() Tree-like ) ( non empty V39() Tree-like ) set ) ) & q : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) = p : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) ^ r : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) );
end;

theorem :: TREES_A:2
for T, T1 being ( ( non empty Tree-like ) ( non empty Tree-like ) Tree)
for P being ( ( ) ( AntiChain_of_Prefixes-like ) AntiChain_of_Prefixes of T : ( ( non empty Tree-like ) ( non empty Tree-like ) Tree) ) st P : ( ( ) ( AntiChain_of_Prefixes-like ) AntiChain_of_Prefixes of b1 : ( ( non empty Tree-like ) ( non empty Tree-like ) Tree) ) <> {} : ( ( ) ( empty functional V32() V33() V34() V35() V36() V37() V38() FinSequence-membered ) set ) holds
tree (T : ( ( non empty Tree-like ) ( non empty Tree-like ) Tree) ,P : ( ( ) ( AntiChain_of_Prefixes-like ) AntiChain_of_Prefixes of b1 : ( ( non empty Tree-like ) ( non empty Tree-like ) Tree) ) ,T1 : ( ( non empty Tree-like ) ( non empty Tree-like ) Tree) ) : ( ( non empty Tree-like ) ( non empty Tree-like ) Tree) = { t1 : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) Element of b1 : ( ( non empty Tree-like ) ( non empty Tree-like ) Tree) ) where t1 is ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) Element of T : ( ( non empty Tree-like ) ( non empty Tree-like ) Tree) ) : for p being ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) st p : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) Element of b2 : ( ( non empty Tree-like ) ( non empty Tree-like ) Tree) ) in P : ( ( ) ( AntiChain_of_Prefixes-like ) AntiChain_of_Prefixes of b1 : ( ( non empty Tree-like ) ( non empty Tree-like ) Tree) ) holds
not p : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) Element of b2 : ( ( non empty Tree-like ) ( non empty Tree-like ) Tree) ) is_a_proper_prefix_of t1 : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) Element of b1 : ( ( non empty Tree-like ) ( non empty Tree-like ) Tree) ) } \/ { (p : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) Element of b1 : ( ( non empty Tree-like ) ( non empty Tree-like ) Tree) ) ^ s : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) Element of b2 : ( ( non empty Tree-like ) ( non empty Tree-like ) Tree) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) where p is ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) Element of T : ( ( non empty Tree-like ) ( non empty Tree-like ) Tree) ) , s is ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) Element of T1 : ( ( non empty Tree-like ) ( non empty Tree-like ) Tree) ) : p : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) Element of b1 : ( ( non empty Tree-like ) ( non empty Tree-like ) Tree) ) in P : ( ( ) ( AntiChain_of_Prefixes-like ) AntiChain_of_Prefixes of b1 : ( ( non empty Tree-like ) ( non empty Tree-like ) Tree) ) } : ( ( ) ( ) set ) ;

theorem :: TREES_A:3
for T being ( ( non empty Tree-like ) ( non empty Tree-like ) Tree)
for P being ( ( ) ( AntiChain_of_Prefixes-like ) AntiChain_of_Prefixes of T : ( ( non empty Tree-like ) ( non empty Tree-like ) Tree) ) holds { t1 : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) Element of b1 : ( ( non empty Tree-like ) ( non empty Tree-like ) Tree) ) where t1 is ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) Element of T : ( ( non empty Tree-like ) ( non empty Tree-like ) Tree) ) : for p being ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) st p : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) in P : ( ( ) ( AntiChain_of_Prefixes-like ) AntiChain_of_Prefixes of b1 : ( ( non empty Tree-like ) ( non empty Tree-like ) Tree) ) holds
not p : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) is_a_prefix_of t1 : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) Element of b1 : ( ( non empty Tree-like ) ( non empty Tree-like ) Tree) ) } c= { t1 : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) Element of b1 : ( ( non empty Tree-like ) ( non empty Tree-like ) Tree) ) where t1 is ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) Element of T : ( ( non empty Tree-like ) ( non empty Tree-like ) Tree) ) : for p being ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) st p : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) in P : ( ( ) ( AntiChain_of_Prefixes-like ) AntiChain_of_Prefixes of b1 : ( ( non empty Tree-like ) ( non empty Tree-like ) Tree) ) holds
not p : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) is_a_proper_prefix_of t1 : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) Element of b1 : ( ( non empty Tree-like ) ( non empty Tree-like ) Tree) ) } ;

theorem :: TREES_A:4
for T being ( ( non empty Tree-like ) ( non empty Tree-like ) Tree)
for P being ( ( ) ( AntiChain_of_Prefixes-like ) AntiChain_of_Prefixes of T : ( ( non empty Tree-like ) ( non empty Tree-like ) Tree) ) holds P : ( ( ) ( AntiChain_of_Prefixes-like ) AntiChain_of_Prefixes of b1 : ( ( non empty Tree-like ) ( non empty Tree-like ) Tree) ) c= { t1 : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) Element of b1 : ( ( non empty Tree-like ) ( non empty Tree-like ) Tree) ) where t1 is ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) Element of T : ( ( non empty Tree-like ) ( non empty Tree-like ) Tree) ) : for p being ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) st p : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) in P : ( ( ) ( AntiChain_of_Prefixes-like ) AntiChain_of_Prefixes of b1 : ( ( non empty Tree-like ) ( non empty Tree-like ) Tree) ) holds
not p : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) is_a_proper_prefix_of t1 : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) Element of b1 : ( ( non empty Tree-like ) ( non empty Tree-like ) Tree) ) } ;

theorem :: TREES_A:5
for T being ( ( non empty Tree-like ) ( non empty Tree-like ) Tree)
for P being ( ( ) ( AntiChain_of_Prefixes-like ) AntiChain_of_Prefixes of T : ( ( non empty Tree-like ) ( non empty Tree-like ) Tree) ) holds { t1 : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) Element of b1 : ( ( non empty Tree-like ) ( non empty Tree-like ) Tree) ) where t1 is ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) Element of T : ( ( non empty Tree-like ) ( non empty Tree-like ) Tree) ) : for p being ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) st p : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) in P : ( ( ) ( AntiChain_of_Prefixes-like ) AntiChain_of_Prefixes of b1 : ( ( non empty Tree-like ) ( non empty Tree-like ) Tree) ) holds
not p : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) is_a_proper_prefix_of t1 : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) Element of b1 : ( ( non empty Tree-like ) ( non empty Tree-like ) Tree) ) } \ { t1 : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) Element of b1 : ( ( non empty Tree-like ) ( non empty Tree-like ) Tree) ) where t1 is ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) Element of T : ( ( non empty Tree-like ) ( non empty Tree-like ) Tree) ) : for p being ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) st p : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) in P : ( ( ) ( AntiChain_of_Prefixes-like ) AntiChain_of_Prefixes of b1 : ( ( non empty Tree-like ) ( non empty Tree-like ) Tree) ) holds
not p : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) is_a_prefix_of t1 : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) Element of b1 : ( ( non empty Tree-like ) ( non empty Tree-like ) Tree) ) } : ( ( ) ( ) Element of K11( { b3 : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) Element of b1 : ( ( non empty Tree-like ) ( non empty Tree-like ) Tree) ) where t1 is ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) Element of b1 : ( ( non empty Tree-like ) ( non empty Tree-like ) Tree) ) : for p being ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) st b4 : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) in p : ( ( ) ( AntiChain_of_Prefixes-like ) AntiChain_of_Prefixes of b1 : ( ( non empty Tree-like ) ( non empty Tree-like ) Tree) ) holds
not b4 : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) is_a_proper_prefix_of b3 : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) Element of b1 : ( ( non empty Tree-like ) ( non empty Tree-like ) Tree) ) } ) : ( ( ) ( ) set ) ) = P : ( ( ) ( AntiChain_of_Prefixes-like ) AntiChain_of_Prefixes of b1 : ( ( non empty Tree-like ) ( non empty Tree-like ) Tree) ) ;

theorem :: TREES_A:6
for T, T1 being ( ( non empty Tree-like ) ( non empty Tree-like ) Tree)
for P being ( ( ) ( AntiChain_of_Prefixes-like ) AntiChain_of_Prefixes of T : ( ( non empty Tree-like ) ( non empty Tree-like ) Tree) ) holds P : ( ( ) ( AntiChain_of_Prefixes-like ) AntiChain_of_Prefixes of b1 : ( ( non empty Tree-like ) ( non empty Tree-like ) Tree) ) c= { (p : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) Element of b1 : ( ( non empty Tree-like ) ( non empty Tree-like ) Tree) ) ^ s : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) Element of b2 : ( ( non empty Tree-like ) ( non empty Tree-like ) Tree) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) where p is ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) Element of T : ( ( non empty Tree-like ) ( non empty Tree-like ) Tree) ) , s is ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) Element of T1 : ( ( non empty Tree-like ) ( non empty Tree-like ) Tree) ) : p : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) Element of b1 : ( ( non empty Tree-like ) ( non empty Tree-like ) Tree) ) in P : ( ( ) ( AntiChain_of_Prefixes-like ) AntiChain_of_Prefixes of b1 : ( ( non empty Tree-like ) ( non empty Tree-like ) Tree) ) } ;

theorem :: TREES_A:7
for T, T1 being ( ( non empty Tree-like ) ( non empty Tree-like ) Tree)
for P being ( ( ) ( AntiChain_of_Prefixes-like ) AntiChain_of_Prefixes of T : ( ( non empty Tree-like ) ( non empty Tree-like ) Tree) ) st P : ( ( ) ( AntiChain_of_Prefixes-like ) AntiChain_of_Prefixes of b1 : ( ( non empty Tree-like ) ( non empty Tree-like ) Tree) ) <> {} : ( ( ) ( empty functional V32() V33() V34() V35() V36() V37() V38() FinSequence-membered ) set ) holds
tree (T : ( ( non empty Tree-like ) ( non empty Tree-like ) Tree) ,P : ( ( ) ( AntiChain_of_Prefixes-like ) AntiChain_of_Prefixes of b1 : ( ( non empty Tree-like ) ( non empty Tree-like ) Tree) ) ,T1 : ( ( non empty Tree-like ) ( non empty Tree-like ) Tree) ) : ( ( non empty Tree-like ) ( non empty Tree-like ) Tree) = { t1 : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) Element of b1 : ( ( non empty Tree-like ) ( non empty Tree-like ) Tree) ) where t1 is ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) Element of T : ( ( non empty Tree-like ) ( non empty Tree-like ) Tree) ) : for p being ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) st p : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) Element of b2 : ( ( non empty Tree-like ) ( non empty Tree-like ) Tree) ) in P : ( ( ) ( AntiChain_of_Prefixes-like ) AntiChain_of_Prefixes of b1 : ( ( non empty Tree-like ) ( non empty Tree-like ) Tree) ) holds
not p : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) Element of b2 : ( ( non empty Tree-like ) ( non empty Tree-like ) Tree) ) is_a_prefix_of t1 : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) Element of b1 : ( ( non empty Tree-like ) ( non empty Tree-like ) Tree) ) } \/ { (p : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) Element of b1 : ( ( non empty Tree-like ) ( non empty Tree-like ) Tree) ) ^ s : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) Element of b2 : ( ( non empty Tree-like ) ( non empty Tree-like ) Tree) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) where p is ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) Element of T : ( ( non empty Tree-like ) ( non empty Tree-like ) Tree) ) , s is ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) Element of T1 : ( ( non empty Tree-like ) ( non empty Tree-like ) Tree) ) : p : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) Element of b1 : ( ( non empty Tree-like ) ( non empty Tree-like ) Tree) ) in P : ( ( ) ( AntiChain_of_Prefixes-like ) AntiChain_of_Prefixes of b1 : ( ( non empty Tree-like ) ( non empty Tree-like ) Tree) ) } : ( ( ) ( ) set ) ;

theorem :: TREES_A:8
for T1, T being ( ( non empty Tree-like ) ( non empty Tree-like ) Tree)
for P being ( ( ) ( AntiChain_of_Prefixes-like ) AntiChain_of_Prefixes of T : ( ( non empty Tree-like ) ( non empty Tree-like ) Tree) )
for p being ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) st p : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) in P : ( ( ) ( AntiChain_of_Prefixes-like ) AntiChain_of_Prefixes of b2 : ( ( non empty Tree-like ) ( non empty Tree-like ) Tree) ) holds
T1 : ( ( non empty Tree-like ) ( non empty Tree-like ) Tree) = (tree (T : ( ( non empty Tree-like ) ( non empty Tree-like ) Tree) ,P : ( ( ) ( AntiChain_of_Prefixes-like ) AntiChain_of_Prefixes of b2 : ( ( non empty Tree-like ) ( non empty Tree-like ) Tree) ) ,T1 : ( ( non empty Tree-like ) ( non empty Tree-like ) Tree) )) : ( ( non empty Tree-like ) ( non empty Tree-like ) Tree) | p : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( non empty Tree-like ) ( non empty Tree-like ) set ) ;

registration
let T be ( ( non empty Tree-like ) ( non empty Tree-like ) Tree) ;
cluster non empty AntiChain_of_Prefixes-like for ( ( ) ( ) AntiChain_of_Prefixes of T : ( ( non empty Tree-like ) ( non empty Tree-like ) set ) ) ;
end;

definition
let T be ( ( non empty Tree-like ) ( non empty Tree-like ) Tree) ;
let t be ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) Element of T : ( ( non empty Tree-like ) ( non empty Tree-like ) Tree) ) ;
:: original: {
redefine func {t} -> ( ( ) ( AntiChain_of_Prefixes-like ) AntiChain_of_Prefixes of T : ( ( non empty Tree-like ) ( non empty Tree-like ) set ) ) ;
end;

theorem :: TREES_A:9
for T, T1 being ( ( non empty Tree-like ) ( non empty Tree-like ) Tree)
for t being ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) Element of T : ( ( non empty Tree-like ) ( non empty Tree-like ) Tree) ) holds tree (T : ( ( non empty Tree-like ) ( non empty Tree-like ) Tree) ,{t : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) Element of b1 : ( ( non empty Tree-like ) ( non empty Tree-like ) Tree) ) } : ( ( ) ( non empty AntiChain_of_Prefixes-like ) AntiChain_of_Prefixes of b1 : ( ( non empty Tree-like ) ( non empty Tree-like ) Tree) ) ,T1 : ( ( non empty Tree-like ) ( non empty Tree-like ) Tree) ) : ( ( non empty Tree-like ) ( non empty Tree-like ) Tree) = T : ( ( non empty Tree-like ) ( non empty Tree-like ) Tree) with-replacement (t : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) Element of b1 : ( ( non empty Tree-like ) ( non empty Tree-like ) Tree) ) ,T1 : ( ( non empty Tree-like ) ( non empty Tree-like ) Tree) ) : ( ( non empty Tree-like ) ( non empty Tree-like ) set ) ;

definition
let T be ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) DecoratedTree) ;
let P be ( ( ) ( AntiChain_of_Prefixes-like ) AntiChain_of_Prefixes of dom T : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) DecoratedTree) : ( ( ) ( non empty Tree-like ) set ) ) ;
let T1 be ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) DecoratedTree) ;
assume P : ( ( ) ( AntiChain_of_Prefixes-like ) AntiChain_of_Prefixes of dom T : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) DecoratedTree) : ( ( ) ( non empty Tree-like ) set ) ) <> {} : ( ( ) ( empty functional V32() V33() V34() V35() V36() V37() V38() FinSequence-membered ) set ) ;
func tree (T,P,T1) -> ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) DecoratedTree) means :: TREES_A:def 2
( dom it : ( ( ) ( ) set ) : ( ( ) ( ) set ) = tree ((dom T : ( ( non empty Tree-like ) ( non empty Tree-like ) set ) ) : ( ( ) ( ) set ) ,P : ( ( ) ( ) Element of T : ( ( non empty Tree-like ) ( non empty Tree-like ) set ) ) ,(dom T1 : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) set ) ) : ( ( ) ( non empty Tree-like ) set ) ) : ( ( non empty Tree-like ) ( non empty Tree-like ) Tree) & ( for q being ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) holds
( not q : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) in tree ((dom T : ( ( non empty Tree-like ) ( non empty Tree-like ) set ) ) : ( ( ) ( ) set ) ,P : ( ( ) ( ) Element of T : ( ( non empty Tree-like ) ( non empty Tree-like ) set ) ) ,(dom T1 : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) set ) ) : ( ( ) ( non empty Tree-like ) set ) ) : ( ( non empty Tree-like ) ( non empty Tree-like ) Tree) or for p being ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) st p : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) in P : ( ( ) ( ) Element of T : ( ( non empty Tree-like ) ( non empty Tree-like ) set ) ) holds
( not p : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) is_a_prefix_of q : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) & it : ( ( ) ( ) set ) . q : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) = T : ( ( non empty Tree-like ) ( non empty Tree-like ) set ) . q : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) or ex p, r being ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) st
( p : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) in P : ( ( ) ( ) Element of T : ( ( non empty Tree-like ) ( non empty Tree-like ) set ) ) & r : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) in dom T1 : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) set ) : ( ( ) ( non empty Tree-like ) set ) & q : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) = p : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) ^ r : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) & it : ( ( ) ( ) set ) . q : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) = T1 : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) set ) . r : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) ) ) );
end;

theorem :: TREES_A:10
for T, T1 being ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) DecoratedTree)
for P being ( ( ) ( AntiChain_of_Prefixes-like ) AntiChain_of_Prefixes of dom T : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) DecoratedTree) : ( ( ) ( non empty Tree-like ) set ) ) st P : ( ( ) ( AntiChain_of_Prefixes-like ) AntiChain_of_Prefixes of dom b1 : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) DecoratedTree) : ( ( ) ( non empty Tree-like ) set ) ) <> {} : ( ( ) ( empty functional V32() V33() V34() V35() V36() V37() V38() FinSequence-membered ) set ) holds
for q being ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) holds
( not q : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) in dom (tree (T : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) DecoratedTree) ,P : ( ( ) ( AntiChain_of_Prefixes-like ) AntiChain_of_Prefixes of dom b1 : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) DecoratedTree) : ( ( ) ( non empty Tree-like ) set ) ) ,T1 : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) DecoratedTree) )) : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) DecoratedTree) : ( ( ) ( non empty Tree-like ) set ) or for p being ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) st p : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) in P : ( ( ) ( AntiChain_of_Prefixes-like ) AntiChain_of_Prefixes of dom b1 : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) DecoratedTree) : ( ( ) ( non empty Tree-like ) set ) ) holds
( not p : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) is_a_prefix_of q : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) & (tree (T : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) DecoratedTree) ,P : ( ( ) ( AntiChain_of_Prefixes-like ) AntiChain_of_Prefixes of dom b1 : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) DecoratedTree) : ( ( ) ( non empty Tree-like ) set ) ) ,T1 : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) DecoratedTree) )) : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) DecoratedTree) . q : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) = T : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) DecoratedTree) . q : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) or ex p, r being ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) st
( p : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) in P : ( ( ) ( AntiChain_of_Prefixes-like ) AntiChain_of_Prefixes of dom b1 : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) DecoratedTree) : ( ( ) ( non empty Tree-like ) set ) ) & r : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) in dom T1 : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) DecoratedTree) : ( ( ) ( non empty Tree-like ) set ) & q : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) = p : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) ^ r : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) & (tree (T : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) DecoratedTree) ,P : ( ( ) ( AntiChain_of_Prefixes-like ) AntiChain_of_Prefixes of dom b1 : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) DecoratedTree) : ( ( ) ( non empty Tree-like ) set ) ) ,T1 : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) DecoratedTree) )) : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) DecoratedTree) . q : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) = T1 : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) DecoratedTree) . r : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: TREES_A:11
for p being ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) )
for T, T1 being ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) DecoratedTree) st p : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) in dom T : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) DecoratedTree) : ( ( ) ( non empty Tree-like ) set ) holds
for q being ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) holds
( not q : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) in dom (T : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) DecoratedTree) with-replacement (p : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) ,T1 : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) DecoratedTree) )) : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) set ) : ( ( ) ( non empty Tree-like ) set ) or ( not p : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) is_a_prefix_of q : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) & (T : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) DecoratedTree) with-replacement (p : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) ,T1 : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) DecoratedTree) )) : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) set ) . q : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) = T : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) DecoratedTree) . q : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) or ex r being ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) st
( r : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) in dom T1 : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) DecoratedTree) : ( ( ) ( non empty Tree-like ) set ) & q : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) = p : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) ^ r : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) & (T : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) DecoratedTree) with-replacement (p : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) ,T1 : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) DecoratedTree) )) : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) set ) . q : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) = T1 : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) DecoratedTree) . r : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: TREES_A:12
for T, T1 being ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) DecoratedTree)
for P being ( ( ) ( AntiChain_of_Prefixes-like ) AntiChain_of_Prefixes of dom T : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) DecoratedTree) : ( ( ) ( non empty Tree-like ) set ) ) st P : ( ( ) ( AntiChain_of_Prefixes-like ) AntiChain_of_Prefixes of dom b1 : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) DecoratedTree) : ( ( ) ( non empty Tree-like ) set ) ) <> {} : ( ( ) ( empty functional V32() V33() V34() V35() V36() V37() V38() FinSequence-membered ) set ) holds
for q being ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) st q : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) in dom (tree (T : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) DecoratedTree) ,P : ( ( ) ( AntiChain_of_Prefixes-like ) AntiChain_of_Prefixes of dom b1 : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) DecoratedTree) : ( ( ) ( non empty Tree-like ) set ) ) ,T1 : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) DecoratedTree) )) : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) DecoratedTree) : ( ( ) ( non empty Tree-like ) set ) & q : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) in { t1 : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) Element of dom b1 : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) DecoratedTree) : ( ( ) ( non empty Tree-like ) set ) ) where t1 is ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) Element of dom T : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) DecoratedTree) : ( ( ) ( non empty Tree-like ) set ) ) : for p being ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) st p : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) in P : ( ( ) ( AntiChain_of_Prefixes-like ) AntiChain_of_Prefixes of dom b1 : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) DecoratedTree) : ( ( ) ( non empty Tree-like ) set ) ) holds
not p : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) is_a_prefix_of t1 : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) Element of dom b1 : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) DecoratedTree) : ( ( ) ( non empty Tree-like ) set ) ) } holds
(tree (T : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) DecoratedTree) ,P : ( ( ) ( AntiChain_of_Prefixes-like ) AntiChain_of_Prefixes of dom b1 : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) DecoratedTree) : ( ( ) ( non empty Tree-like ) set ) ) ,T1 : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) DecoratedTree) )) : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) DecoratedTree) . q : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) = T : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) DecoratedTree) . q : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ;

theorem :: TREES_A:13
for p being ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) )
for T, T1 being ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) DecoratedTree) st p : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) in dom T : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) DecoratedTree) : ( ( ) ( non empty Tree-like ) set ) holds
for q being ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) st q : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) in dom (T : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) DecoratedTree) with-replacement (p : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) ,T1 : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) DecoratedTree) )) : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) set ) : ( ( ) ( non empty Tree-like ) set ) & q : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) in { t1 : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) Element of dom b2 : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) DecoratedTree) : ( ( ) ( non empty Tree-like ) set ) ) where t1 is ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) Element of dom T : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) DecoratedTree) : ( ( ) ( non empty Tree-like ) set ) ) : not p : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) is_a_prefix_of t1 : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) Element of dom b2 : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) DecoratedTree) : ( ( ) ( non empty Tree-like ) set ) ) } holds
(T : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) DecoratedTree) with-replacement (p : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) ,T1 : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) DecoratedTree) )) : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) set ) . q : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) = T : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) DecoratedTree) . q : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ;

theorem :: TREES_A:14
for T, T1 being ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) DecoratedTree)
for P being ( ( ) ( AntiChain_of_Prefixes-like ) AntiChain_of_Prefixes of dom T : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) DecoratedTree) : ( ( ) ( non empty Tree-like ) set ) )
for q being ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) st q : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) in dom (tree (T : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) DecoratedTree) ,P : ( ( ) ( AntiChain_of_Prefixes-like ) AntiChain_of_Prefixes of dom b1 : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) DecoratedTree) : ( ( ) ( non empty Tree-like ) set ) ) ,T1 : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) DecoratedTree) )) : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) DecoratedTree) : ( ( ) ( non empty Tree-like ) set ) & q : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) in { (p : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) Element of dom b1 : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) DecoratedTree) : ( ( ) ( non empty Tree-like ) set ) ) ^ s : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) Element of dom b2 : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) DecoratedTree) : ( ( ) ( non empty Tree-like ) set ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) where p is ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) Element of dom T : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) DecoratedTree) : ( ( ) ( non empty Tree-like ) set ) ) , s is ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) Element of dom T1 : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) DecoratedTree) : ( ( ) ( non empty Tree-like ) set ) ) : p : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) Element of dom b1 : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) DecoratedTree) : ( ( ) ( non empty Tree-like ) set ) ) in P : ( ( ) ( AntiChain_of_Prefixes-like ) AntiChain_of_Prefixes of dom b1 : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) DecoratedTree) : ( ( ) ( non empty Tree-like ) set ) ) } holds
ex p9 being ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) Element of dom T : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) DecoratedTree) : ( ( ) ( non empty Tree-like ) set ) ) ex r being ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) Element of dom T1 : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) DecoratedTree) : ( ( ) ( non empty Tree-like ) set ) ) st
( q : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) = p9 : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) Element of dom b1 : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) DecoratedTree) : ( ( ) ( non empty Tree-like ) set ) ) ^ r : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) Element of dom b2 : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) DecoratedTree) : ( ( ) ( non empty Tree-like ) set ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) & p9 : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) Element of dom b1 : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) DecoratedTree) : ( ( ) ( non empty Tree-like ) set ) ) in P : ( ( ) ( AntiChain_of_Prefixes-like ) AntiChain_of_Prefixes of dom b1 : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) DecoratedTree) : ( ( ) ( non empty Tree-like ) set ) ) & (tree (T : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) DecoratedTree) ,P : ( ( ) ( AntiChain_of_Prefixes-like ) AntiChain_of_Prefixes of dom b1 : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) DecoratedTree) : ( ( ) ( non empty Tree-like ) set ) ) ,T1 : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) DecoratedTree) )) : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) DecoratedTree) . q : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) = T1 : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) DecoratedTree) . r : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) Element of dom b2 : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) DecoratedTree) : ( ( ) ( non empty Tree-like ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: TREES_A:15
for p being ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) )
for T, T1 being ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) DecoratedTree) st p : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) in dom T : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) DecoratedTree) : ( ( ) ( non empty Tree-like ) set ) holds
for q being ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) st q : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) in dom (T : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) DecoratedTree) with-replacement (p : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) ,T1 : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) DecoratedTree) )) : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) set ) : ( ( ) ( non empty Tree-like ) set ) & q : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) in { (p : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) ^ s : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) Element of dom b3 : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) DecoratedTree) : ( ( ) ( non empty Tree-like ) set ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) where s is ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) Element of dom T1 : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) DecoratedTree) : ( ( ) ( non empty Tree-like ) set ) ) : s : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) Element of dom b3 : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) DecoratedTree) : ( ( ) ( non empty Tree-like ) set ) ) = s : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) Element of dom b3 : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) DecoratedTree) : ( ( ) ( non empty Tree-like ) set ) ) } holds
ex r being ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) Element of dom T1 : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) DecoratedTree) : ( ( ) ( non empty Tree-like ) set ) ) st
( q : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) = p : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) ^ r : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) Element of dom b3 : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) DecoratedTree) : ( ( ) ( non empty Tree-like ) set ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) & (T : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) DecoratedTree) with-replacement (p : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) ,T1 : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) DecoratedTree) )) : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) set ) . q : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) = T1 : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) DecoratedTree) . r : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) Element of dom b3 : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) DecoratedTree) : ( ( ) ( non empty Tree-like ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: TREES_A:16
for T, T1 being ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) DecoratedTree)
for t being ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) Element of dom T : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) DecoratedTree) : ( ( ) ( non empty Tree-like ) set ) ) holds tree (T : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) DecoratedTree) ,{t : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) Element of dom b1 : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) DecoratedTree) : ( ( ) ( non empty Tree-like ) set ) ) } : ( ( ) ( non empty AntiChain_of_Prefixes-like ) AntiChain_of_Prefixes of dom b1 : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) DecoratedTree) : ( ( ) ( non empty Tree-like ) set ) ) ,T1 : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) DecoratedTree) ) : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) DecoratedTree) = T : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) DecoratedTree) with-replacement (t : ( ( ) ( Relation-like NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of K11(REAL : ( ( ) ( V32() V33() V34() V38() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V39() FinSequence-like FinSubsequence-like ) Element of dom b1 : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) DecoratedTree) : ( ( ) ( non empty Tree-like ) set ) ) ,T1 : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) DecoratedTree) ) : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) set ) ;

definition
let D be ( ( non empty ) ( non empty ) set ) ;
let T be ( ( Relation-like D : ( ( non empty ) ( non empty ) set ) -valued Function-like DecoratedTree-like ) ( Relation-like D : ( ( non empty ) ( non empty ) set ) -valued Function-like DecoratedTree-like ) DecoratedTree of D : ( ( non empty ) ( non empty ) set ) ) ;
let P be ( ( ) ( AntiChain_of_Prefixes-like ) AntiChain_of_Prefixes of dom T : ( ( Relation-like D : ( ( non empty ) ( non empty ) set ) -valued Function-like DecoratedTree-like ) ( Relation-like D : ( ( non empty ) ( non empty ) set ) -valued Function-like DecoratedTree-like ) DecoratedTree of D : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty Tree-like ) set ) ) ;
let T1 be ( ( Relation-like D : ( ( non empty ) ( non empty ) set ) -valued Function-like DecoratedTree-like ) ( Relation-like D : ( ( non empty ) ( non empty ) set ) -valued Function-like DecoratedTree-like ) DecoratedTree of D : ( ( non empty ) ( non empty ) set ) ) ;
assume P : ( ( ) ( AntiChain_of_Prefixes-like ) AntiChain_of_Prefixes of dom T : ( ( Relation-like D : ( ( non empty ) ( non empty ) set ) -valued Function-like DecoratedTree-like ) ( Relation-like D : ( ( non empty ) ( non empty ) set ) -valued Function-like DecoratedTree-like ) DecoratedTree of D : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty Tree-like ) set ) ) <> {} : ( ( ) ( empty functional V32() V33() V34() V35() V36() V37() V38() FinSequence-membered ) set ) ;
func tree (T,P,T1) -> ( ( Relation-like D : ( ( non empty Tree-like ) ( non empty Tree-like ) set ) -valued Function-like DecoratedTree-like ) ( Relation-like D : ( ( non empty Tree-like ) ( non empty Tree-like ) set ) -valued Function-like DecoratedTree-like ) DecoratedTree of D : ( ( non empty Tree-like ) ( non empty Tree-like ) set ) ) equals :: TREES_A:def 3
 tree (T : ( ( ) ( ) Element of D : ( ( non empty Tree-like ) ( non empty Tree-like ) set ) ) ,P : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) set ) ,T1 : ( ( ) ( ) set ) ) : ( ( Relation-like Function-like DecoratedTree-like ) ( Relation-like Function-like DecoratedTree-like ) DecoratedTree) ;
end;