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

theorem :: TREES_1:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for p, q being FinSequence st q = p | (Seg n) holds
len q <= n
proof end;

theorem Th2: :: TREES_1:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for p, q being FinSequence st q = p | (Seg n) holds
len q <= len p
proof end;

theorem Th3: :: TREES_1:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for p, r being FinSequence st r = p | (Seg n) holds
ex q being FinSequence st p = r ^ q
proof end;

theorem :: TREES_1:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being set holds {} <> <*x*> ;

theorem :: TREES_1:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q being FinSequence st ( p = p ^ q or p = q ^ p ) holds
q = {}
proof end;

theorem Th6: :: TREES_1:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being set
for p, q being FinSequence holds
( not p ^ q = <*x*> or ( p = <*x*> & q = {} ) or ( p = {} & q = <*x*> ) )
proof end;

notation
let p, q be FinSequence;
synonym p is_a_prefix_of q for p c= q;
end;

definition
let p, q be FinSequence;
redefine pred p c= q means :Def1: :: TREES_1:def 1
ex n being Nat st p = q | (Seg n);
compatibility
( p is_a_prefix_of q iff ex n being Nat st p = q | (Seg n) )
proof end;
end;

:: deftheorem Def1 defines is_a_prefix_of TREES_1:def 1 :
for p, q being FinSequence holds
( p is_a_prefix_of q iff ex n being Nat st p = q | (Seg n) );

theorem :: TREES_1:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th8: :: TREES_1:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q being FinSequence holds
( p is_a_prefix_of q iff ex r being FinSequence st q = p ^ r )
proof end;

theorem :: TREES_1:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: TREES_1:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: TREES_1:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: TREES_1:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: TREES_1:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: TREES_1:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th15: :: TREES_1:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q being FinSequence st p is_a_prefix_of q & len p = len q holds
p = q
proof end;

theorem :: TREES_1:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being set holds
( <*x*> is_a_prefix_of <*y*> iff x = y )
proof end;

notation
let p, q be FinSequence;
synonym p is_a_proper_prefix_of q for p c< q;
end;

Lm1: for A, B being finite set st A c= B & card A = card B holds
A = B
proof end;

theorem :: TREES_1:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: TREES_1:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th19: :: TREES_1:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q being finite set st p,q are_c=-comparable & card p = card q holds
p = q
proof end;

theorem :: TREES_1:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: TREES_1:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: TREES_1:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th23: :: TREES_1:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being set holds
( <*x*>,<*y*> are_c=-comparable iff x = y )
proof end;

theorem Th24: :: TREES_1:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q being finite set st p c< q holds
card p < card q
proof end;

theorem Th25: :: TREES_1:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for p being FinSequence holds
( not p is_a_proper_prefix_of {} & not p is_a_proper_prefix_of <*> D )
proof end;

theorem :: TREES_1:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q being FinSequence holds
( not p is_a_proper_prefix_of q or not q is_a_proper_prefix_of p ) ;

theorem :: TREES_1:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q, r being FinSequence st ( ( p is_a_proper_prefix_of q & q is_a_proper_prefix_of r ) or ( p is_a_proper_prefix_of q & q is_a_prefix_of r ) or ( p is_a_prefix_of q & q is_a_proper_prefix_of r ) ) holds
p is_a_proper_prefix_of r by XBOOLE_1:56, XBOOLE_1:58, XBOOLE_1:59;

theorem Th28: :: TREES_1:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p1, p2 being FinSequence st p1 is_a_prefix_of p2 holds
not p2 is_a_proper_prefix_of p1
proof end;

theorem :: TREES_1:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: TREES_1:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being set
for p1, p2 being FinSequence st p1 ^ <*x*> is_a_prefix_of p2 holds
p1 is_a_proper_prefix_of p2
proof end;

theorem Th31: :: TREES_1:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being set
for p1, p2 being FinSequence st p1 is_a_prefix_of p2 holds
p1 is_a_proper_prefix_of p2 ^ <*x*>
proof end;

theorem Th32: :: TREES_1:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being set
for p1, p2 being FinSequence st p1 is_a_proper_prefix_of p2 ^ <*x*> holds
p1 is_a_prefix_of p2
proof end;

theorem :: TREES_1:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p2, p1 being FinSequence st ( {} is_a_proper_prefix_of p2 or {} <> p2 ) holds
p1 is_a_proper_prefix_of p1 ^ p2
proof end;

definition
let p be FinSequence;
canceled;
canceled;
func ProperPrefixes p -> set means :Def4: :: TREES_1:def 4
for x being set holds
( x in it iff ex q being FinSequence st
( x = q & q is_a_proper_prefix_of p ) );
existence
ex b1 being set st
for x being set holds
( x in b1 iff ex q being FinSequence st
( x = q & q is_a_proper_prefix_of p ) )
proof end;
uniqueness
for b1, b2 being set st ( for x being set holds
( x in b1 iff ex q being FinSequence st
( x = q & q is_a_proper_prefix_of p ) ) ) & ( for x being set holds
( x in b2 iff ex q being FinSequence st
( x = q & q is_a_proper_prefix_of p ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem TREES_1:def 2 :
canceled;

:: deftheorem TREES_1:def 3 :
canceled;

:: deftheorem Def4 defines ProperPrefixes TREES_1:def 4 :
for p being FinSequence
for b2 being set holds
( b2 = ProperPrefixes p iff for x being set holds
( x in b2 iff ex q being FinSequence st
( x = q & q is_a_proper_prefix_of p ) ) );

theorem :: TREES_1:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th35: :: TREES_1:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being set
for p being FinSequence st x in ProperPrefixes p holds
x is FinSequence
proof end;

theorem Th36: :: TREES_1:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q being FinSequence holds
( p in ProperPrefixes q iff p is_a_proper_prefix_of q )
proof end;

theorem Th37: :: TREES_1:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q being FinSequence st p in ProperPrefixes q holds
len p < len q
proof end;

theorem :: TREES_1:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q, r being FinSequence st q ^ r in ProperPrefixes p holds
q in ProperPrefixes p
proof end;

theorem Th39: :: TREES_1:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
ProperPrefixes {} = {}
proof end;

theorem Th40: :: TREES_1:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being set holds ProperPrefixes <*x*> = {{} }
proof end;

theorem :: TREES_1:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q being FinSequence st p is_a_prefix_of q holds
ProperPrefixes p c= ProperPrefixes q
proof end;

theorem Th42: :: TREES_1:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q, r being FinSequence st q in ProperPrefixes p & r in ProperPrefixes p holds
q,r are_c=-comparable
proof end;

definition
let X be set ;
attr X is Tree-like means :Def5: :: TREES_1:def 5
( X c= NAT * & ( for p being FinSequence of NAT st p in X holds
ProperPrefixes p c= X ) & ( for p being FinSequence of NAT
for k, n being Nat st p ^ <*k*> in X & n <= k holds
p ^ <*n*> in X ) );
end;

:: deftheorem Def5 defines Tree-like TREES_1:def 5 :
for X being set holds
( X is Tree-like iff ( X c= NAT * & ( for p being FinSequence of NAT st p in X holds
ProperPrefixes p c= X ) & ( for p being FinSequence of NAT
for k, n being Nat st p ^ <*k*> in X & n <= k holds
p ^ <*n*> in X ) ) );

registration
cluster non empty Tree-like set ;
existence
ex b1 being set st
( not b1 is empty & b1 is Tree-like )
proof end;
end;

definition
mode Tree is non empty Tree-like set ;
end;

theorem :: TREES_1:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th44: :: TREES_1:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being set
for T being Tree st x in T holds
x is FinSequence of NAT
proof end;

definition
let T be Tree;
:: original: Element
redefine mode Element of T -> FinSequence of NAT ;
coherence
for b1 being Element of T holds b1 is FinSequence of NAT
by Th44;
end;

theorem Th45: :: TREES_1:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being Tree
for p, q being FinSequence st p in T & q is_a_prefix_of p holds
q in T
proof end;

theorem Th46: :: TREES_1:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for q being FinSequence of NAT
for T being Tree
for r being FinSequence st q ^ r in T holds
q in T
proof end;

theorem Th47: :: TREES_1:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being Tree holds
( {} in T & <*> NAT in T )
proof end;

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

theorem Th49: :: TREES_1:49  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T, T1 being Tree holds T \/ T1 is Tree
proof end;

theorem Th50: :: TREES_1:50  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T, T1 being Tree holds T /\ T1 is Tree
proof end;

registration
cluster finite set ;
existence
ex b1 being Tree st b1 is finite
by Th48;
end;

theorem :: TREES_1:51  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: TREES_1:52  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for fT, fT1 being finite Tree holds fT \/ fT1 is finite Tree by Th49;

theorem :: TREES_1:53  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being Tree
for fT being finite Tree holds
( fT /\ T is finite Tree & T /\ fT is finite Tree ) by Th50;

definition
let n be Nat;
canceled;
func elementary_tree n -> finite Tree equals :: TREES_1:def 7
{ <*k*> where k is Nat : k < n } \/ {{} };
correctness
coherence
{ <*k*> where k is Nat : k < n } \/ {{} } is finite Tree
;
proof end;
end;

:: deftheorem TREES_1:def 6 :
canceled;

:: deftheorem defines elementary_tree TREES_1:def 7 :
for n being Nat holds elementary_tree n = { <*k*> where k is Nat : k < n } \/ {{} };

theorem :: TREES_1:54  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th55: :: TREES_1:55  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k, n being Nat st k < n holds
<*k*> in elementary_tree n
proof end;

theorem Th56: :: TREES_1:56  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
elementary_tree 0 = {{} }
proof end;

theorem :: TREES_1:57  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for p being FinSequence of NAT holds
( not p in elementary_tree n or p = {} or ex k being Nat st
( k < n & p = <*k*> ) )
proof end;

definition
let T be Tree;
func Leaves T -> Subset of T means :: TREES_1:def 8
for p being FinSequence of NAT holds
( p in it iff ( p in T & ( for q being FinSequence of NAT holds
( not q in T or not p is_a_proper_prefix_of q ) ) ) );
existence
ex b1 being Subset of T st
for p being FinSequence of NAT holds
( p in b1 iff ( p in T & ( for q being FinSequence of NAT holds
( not q in T or not p is_a_proper_prefix_of q ) ) ) )
proof end;
uniqueness
for b1, b2 being Subset of T st ( for p being FinSequence of NAT holds
( p in b1 iff ( p in T & ( for q being FinSequence of NAT holds
( not q in T or not p is_a_proper_prefix_of q ) ) ) ) ) & ( for p being FinSequence of NAT holds
( p in b2 iff ( p in T & ( for q being FinSequence of NAT holds
( not q in T or not p is_a_proper_prefix_of q ) ) ) ) ) holds
b1 = b2
proof end;
let p be FinSequence of NAT ;
assume A8: p in T ;
func T | p -> Tree means :Def9: :: TREES_1:def 9
for q being FinSequence of NAT holds
( q in it iff p ^ q in T );
existence
ex b1 being Tree st
for q being FinSequence of NAT holds
( q in b1 iff p ^ q in T )
proof end;
uniqueness
for b1, b2 being Tree st ( for q being FinSequence of NAT holds
( q in b1 iff p ^ q in T ) ) & ( for q being FinSequence of NAT holds
( q in b2 iff p ^ q in T ) ) holds
b1 = b2
proof end;
end;

:: deftheorem defines Leaves TREES_1:def 8 :
for T being Tree
for b2 being Subset of T holds
( b2 = Leaves T iff for p being FinSequence of NAT holds
( p in b2 iff ( p in T & ( for q being FinSequence of NAT holds
( not q in T or not p is_a_proper_prefix_of q ) ) ) ) );

:: deftheorem Def9 defines | TREES_1:def 9 :
for T being Tree
for p being FinSequence of NAT st p in T holds
for b3 being Tree holds
( b3 = T | p iff for q being FinSequence of NAT holds
( q in b3 iff p ^ q in T ) );

theorem :: TREES_1:58  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: TREES_1:59  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: TREES_1:60  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being Tree holds T | (<*> NAT ) = T
proof end;

registration
let T be finite Tree;
let p be Element of T;
cluster T | p -> finite ;
coherence
T | p is finite
proof end;
end;

definition
let T be Tree;
assume A1: Leaves T <> {} ;
mode Leaf of T -> Element of T means :: TREES_1:def 10
it in Leaves T;
existence
ex b1 being Element of T st b1 in Leaves T
proof end;
end;

:: deftheorem defines Leaf TREES_1:def 10 :
for T being Tree st Leaves T <> {} holds
for b2 being Element of T holds
( b2 is Leaf of T iff b2 in Leaves T );

definition
let T be Tree;
mode Subtree of T -> Tree means :: TREES_1:def 11
ex p being Element of T st it = T | p;
existence
ex b1 being Tree ex p being Element of T st b1 = T | p
proof end;
end;

:: deftheorem defines Subtree TREES_1:def 11 :
for T, b2 being Tree holds
( b2 is Subtree of T iff ex p being Element of T st b2 = T | p );

definition
let T be Tree;
let p be FinSequence of NAT ;
let T1 be Tree;
assume A1: p in T ;
func T with-replacement p,T1 -> Tree means :Def12: :: TREES_1:def 12
for q being FinSequence of NAT holds
( q in it iff ( ( q in T & not p is_a_proper_prefix_of q ) or ex r being FinSequence of NAT st
( r in T1 & q = p ^ r ) ) );
existence
ex b1 being Tree st
for q being FinSequence of NAT holds
( q in b1 iff ( ( q in T & not p is_a_proper_prefix_of q ) or ex r being FinSequence of NAT st
( r in T1 & q = p ^ r ) ) )
proof end;
uniqueness
for b1, b2 being Tree st ( for q being FinSequence of NAT holds
( q in b1 iff ( ( q in T & not p is_a_proper_prefix_of q ) or ex r being FinSequence of NAT st
( r in T1 & q = p ^ r ) ) ) ) & ( for q being FinSequence of NAT holds
( q in b2 iff ( ( q in T & not p is_a_proper_prefix_of q ) or ex r being FinSequence of NAT st
( r in T1 & q = p ^ r ) ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def12 defines with-replacement TREES_1:def 12 :
for T being Tree
for p being FinSequence of NAT
for T1 being Tree st p in T holds
for b4 being Tree holds
( b4 = T with-replacement p,T1 iff for q being FinSequence of NAT holds
( q in b4 iff ( ( q in T & not p is_a_proper_prefix_of q ) or ex r being FinSequence of NAT st
( r in T1 & q = p ^ r ) ) ) );

theorem :: TREES_1:61  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: TREES_1:62  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: TREES_1:63  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th64: :: TREES_1:64  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being FinSequence of NAT
for T, T1 being Tree st p in T holds
T with-replacement p,T1 = { t1 where t1 is Element of T : not p is_a_proper_prefix_of t1 } \/ { (p ^ s) where s is Element of T1 : s = s }
proof end;

theorem :: TREES_1:65  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: TREES_1:66  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being FinSequence of NAT
for T, T1 being Tree st p in T holds
T1 = (T with-replacement p,T1) | p
proof end;

registration
let T be finite Tree;
let t be Element of T;
let T1 be finite Tree;
cluster T with-replacement t,T1 -> finite ;
coherence
T with-replacement t,T1 is finite
proof end;
end;

theorem Th67: :: TREES_1:67  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being FinSequence holds ProperPrefixes p, dom p are_equipotent
proof end;

registration
let p be FinSequence;
cluster ProperPrefixes p -> finite ;
coherence
ProperPrefixes p is finite
proof end;
end;

theorem :: TREES_1:68  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being FinSequence holds card (ProperPrefixes p) = len p
proof end;

definition
let IT be set ;
attr IT is AntiChain_of_Prefixes-like means :Def13: :: TREES_1:def 13
( ( for x being set st x in IT holds
x is FinSequence ) & ( for p1, p2 being FinSequence st p1 in IT & p2 in IT & p1 <> p2 holds
not p1,p2 are_c=-comparable ) );
end;

:: deftheorem Def13 defines AntiChain_of_Prefixes-like TREES_1:def 13 :
for IT being set holds
( IT is AntiChain_of_Prefixes-like iff ( ( for x being set st x in IT holds
x is FinSequence ) & ( for p1, p2 being FinSequence st p1 in IT & p2 in IT & p1 <> p2 holds
not p1,p2 are_c=-comparable ) ) );

registration
cluster AntiChain_of_Prefixes-like set ;
existence
ex b1 being set st b1 is AntiChain_of_Prefixes-like
proof end;
end;

definition
mode AntiChain_of_Prefixes is AntiChain_of_Prefixes-like set ;
end;

theorem :: TREES_1:69  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th70: :: TREES_1:70  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for w being FinSequence holds {w} is AntiChain_of_Prefixes-like
proof end;

theorem Th71: :: TREES_1:71  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p1, p2 being FinSequence st not p1,p2 are_c=-comparable holds
{p1,p2} is AntiChain_of_Prefixes-like
proof end;

definition
let T be Tree;
mode AntiChain_of_Prefixes of T -> AntiChain_of_Prefixes means :Def14: :: TREES_1:def 14
it c= T;
existence
ex b1 being AntiChain_of_Prefixes st b1 c= T
proof end;
end;

:: deftheorem Def14 defines AntiChain_of_Prefixes TREES_1:def 14 :
for T being Tree
for b2 being AntiChain_of_Prefixes holds
( b2 is AntiChain_of_Prefixes of T iff b2 c= T );

theorem :: TREES_1:72  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th73: :: TREES_1:73  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being Tree holds
( {} is AntiChain_of_Prefixes of T & {{} } is AntiChain_of_Prefixes of T )
proof end;

theorem :: TREES_1:74  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being Tree
for t being Element of T holds {t} is AntiChain_of_Prefixes of T
proof end;

theorem :: TREES_1:75  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being Tree
for t1, t2 being Element of T st not t1,t2 are_c=-comparable holds
{t1,t2} is AntiChain_of_Prefixes of T
proof end;

registration
let T be finite Tree;
cluster -> finite AntiChain_of_Prefixes of T;
coherence
for b1 being AntiChain_of_Prefixes of T holds b1 is finite
proof end;
end;

definition
let T be finite Tree;
func height T -> Nat means :Def15: :: TREES_1:def 15
( ex p being FinSequence of NAT st
( p in T & len p = it ) & ( for p being FinSequence of NAT st p in T holds
len p <= it ) );
existence
ex b1 being Nat st
( ex p being FinSequence of NAT st
( p in T & len p = b1 ) & ( for p being FinSequence of NAT st p in T holds
len p <= b1 ) )
proof end;
uniqueness
for b1, b2 being Nat st ex p being FinSequence of NAT st
( p in T & len p = b1 ) & ( for p being FinSequence of NAT st p in T holds
len p <= b1 ) & ex p being FinSequence of NAT st
( p in T & len p = b2 ) & ( for p being FinSequence of NAT st p in T holds
len p <= b2 ) holds
b1 = b2
proof end;
func width T -> Nat means :Def16: :: TREES_1:def 16
ex X being AntiChain_of_Prefixes of T st
( it = card X & ( for Y being AntiChain_of_Prefixes of T holds card Y <= card X ) );
existence
ex b1 being Nat ex X being AntiChain_of_Prefixes of T st
( b1 = card X & ( for Y being AntiChain_of_Prefixes of T holds card Y <= card X ) )
proof end;
uniqueness
for b1, b2 being Nat st ex X being AntiChain_of_Prefixes of T st
( b1 = card X & ( for Y being AntiChain_of_Prefixes of T holds card Y <= card X ) ) & ex X being AntiChain_of_Prefixes of T st
( b2 = card X & ( for Y being AntiChain_of_Prefixes of T holds card Y <= card X ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def15 defines height TREES_1:def 15 :
for T being finite Tree
for b2 being Nat holds
( b2 = height T iff ( ex p being FinSequence of NAT st
( p in T & len p = b2 ) & ( for p being FinSequence of NAT st p in T holds
len p <= b2 ) ) );

:: deftheorem Def16 defines width TREES_1:def 16 :
for T being finite Tree
for b2 being Nat holds
( b2 = width T iff ex X being AntiChain_of_Prefixes of T st
( b2 = card X & ( for Y being AntiChain_of_Prefixes of T holds card Y <= card X ) ) );

theorem :: TREES_1:76  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: TREES_1:77  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: TREES_1:78  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for fT being finite Tree holds 1 <= width fT
proof end;

theorem :: TREES_1:79  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
height (elementary_tree 0) = 0
proof end;

theorem :: TREES_1:80  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for fT being finite Tree st height fT = 0 holds
fT = elementary_tree 0
proof end;

theorem :: TREES_1:81  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat holds height (elementary_tree (n + 1)) = 1
proof end;

theorem :: TREES_1:82  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
width (elementary_tree 0) = 1
proof end;

theorem :: TREES_1:83  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat holds width (elementary_tree (n + 1)) = n + 1
proof end;

theorem :: TREES_1:84  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for fT being finite Tree
for t being Element of fT holds height (fT | t) <= height fT
proof end;

theorem Th85: :: TREES_1:85  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for fT being finite Tree
for t being Element of fT st t <> {} holds
height (fT | t) < height fT
proof end;

scheme :: TREES_1:sch 1
TreeInd{ P1[ Tree] } :
for fT being finite Tree holds P1[fT]
provided
A1: for fT being finite Tree st ( for n being Nat st <*n*> in fT holds
P1[fT | <*n*>] ) holds
P1[fT]
proof end;