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

proof end;

uniqueness

proof end;

end;

:: deftheorem TREES_1:def 2 :

:: deftheorem TREES_1:def 3 :

:: deftheorem Def4 defines ProperPrefixes TREES_1:def 4 :

theorem :: TREES_1:34

canceled;

theorem Th35: :: TREES_1:35

for x being set
for p being FinSequence st x in ProperPrefixes p holds
x is FinSequence

proof end;

theorem Th36: :: TREES_1:36

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

for p, q being FinSequence st p in ProperPrefixes q holds
len p < len q

proof end;

theorem :: TREES_1:38

for p, q, r being FinSequence st q ^ r in ProperPrefixes p holds
q in ProperPrefixes p

proof end;

theorem Th39: :: TREES_1:39

ProperPrefixes {} = {}

proof end;

theorem Th40: :: TREES_1:40

for x being set holds ProperPrefixes <*x*> = {{} }

proof end;

theorem :: TREES_1:41

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

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 :

registration

cluster non empty Tree-like set ;
existence

proof end;

end;

definition

mode Tree is non empty Tree-like set ;

end;

theorem :: TREES_1:43

canceled;

theorem Th44: :: TREES_1:44

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 by Th44;

end;

theorem Th45: :: TREES_1:45

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

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

for T being Tree holds
( {} in T & <*> NAT in T )

proof end;

theorem Th48: :: TREES_1:48

{{} } is Tree

proof end;

theorem Th49: :: TREES_1:49

for T, T1 being Tree holds T \/ T1 is Tree

proof end;

theorem Th50: :: TREES_1:50

for T, T1 being Tree holds T /\ T1 is Tree

proof end;

registration

cluster finite set ;
existence by Th48;

end;

theorem :: TREES_1:51

canceled;

theorem :: TREES_1:52

for fT, fT1 being finite Tree holds fT \/ fT1 is finite Tree by Th49;

theorem :: TREES_1:53

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

proof end;

end;

:: deftheorem TREES_1:def 6 :

:: deftheorem defines elementary_tree TREES_1:def 7 :

theorem :: TREES_1:54

canceled;

theorem Th55: :: TREES_1:55

for k, n being Nat st k < n holds
<*k*> in elementary_tree n

proof end;

theorem Th56: :: TREES_1:56

elementary_tree 0 = {{} }

proof end;

theorem :: TREES_1:57

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

proof end;

uniqueness

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

proof end;

uniqueness

proof end;

end;

:: deftheorem defines Leaves TREES_1:def 8 :

:: deftheorem Def9 defines | TREES_1:def 9 :

theorem :: TREES_1:58

canceled;

theorem :: TREES_1:59

canceled;

theorem :: TREES_1:60

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

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

proof end;

end;

:: deftheorem defines Leaf TREES_1:def 10 :

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

proof end;

end;

:: deftheorem defines Subtree TREES_1:def 11 :

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def12 defines with-replacement TREES_1:def 12 :

theorem :: TREES_1:61

canceled;

theorem :: TREES_1:62

canceled;

theorem :: TREES_1:63

canceled;

theorem Th64: :: TREES_1:64

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

canceled;

theorem :: TREES_1:66

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

proof end;

end;

theorem Th67: :: TREES_1:67

for p being FinSequence holds ProperPrefixes p, dom p are_equipotent

proof end;

registration

let p be FinSequence;
cluster ProperPrefixes p -> finite ;
coherence

proof end;

end;

theorem :: TREES_1:68

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 :

registration

cluster AntiChain_of_Prefixes-like set ;
existence

proof end;

end;

definition

mode AntiChain_of_Prefixes is AntiChain_of_Prefixes-like set ;

end;

theorem :: TREES_1:69

canceled;

theorem Th70: :: TREES_1:70

for w being FinSequence holds {w} is AntiChain_of_Prefixes-like

proof end;

theorem Th71: :: TREES_1:71

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

proof end;

end;

:: deftheorem Def14 defines AntiChain_of_Prefixes TREES_1:def 14 :

theorem :: TREES_1:72

canceled;

theorem Th73: :: TREES_1:73

for T being Tree holds
( {} is AntiChain_of_Prefixes of T & {{} } is AntiChain_of_Prefixes of T )

proof end;

theorem :: TREES_1:74

for T being Tree
for t being Element of T holds {t} is AntiChain_of_Prefixes of T

proof end;

theorem :: TREES_1:75

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

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

proof end;