:: TREES_1 semantic presentation

begin


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 Element of NAT st p = q | (Seg n);
compatibility
 ( p is_a_prefix_of q iff ex n being Element of NAT st p = q | (Seg n) )
proof
thus  ( p c= q implies ex n being Element of NAT st p = q | (Seg n) ) ::_thesis: ( ex n being Element of NAT st p = q | (Seg n) implies p is_a_prefix_of q )
proof
assume A1: p c= q ; ::_thesis: ex n being Element of NAT st p = q | (Seg n)
consider n being Nat such that
A2: dom p = Seg n by FINSEQ_1:def_2;
reconsider n = n as Element of NAT by ORDINAL1:def_12;
take  n ; ::_thesis: p = q | (Seg n)
thus  p = q | (Seg n) by A1, A2, GRFUNC_1:23; ::_thesis: verum
end;
thus  ( ex n being Element of NAT st p = q | (Seg n) implies p is_a_prefix_of q ) by RELAT_1:59; ::_thesis: verum
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 Element of NAT st p = q | (Seg n) );

theorem Th1: :: TREES_1:1
for p, q being FinSequence holds
( p is_a_prefix_of q iff ex r being FinSequence st q = p ^ r )
proof
let p, q be FinSequence; ::_thesis: ( p is_a_prefix_of q iff ex r being FinSequence st q = p ^ r )
thus  ( p is_a_prefix_of q implies ex r being FinSequence st q = p ^ r ) ::_thesis: ( ex r being FinSequence st q = p ^ r implies p is_a_prefix_of q )
proof
given n being Element of NAT  such that A1: p = q | (Seg n) ; :: according to TREES_1:def_1 ::_thesis: ex r being FinSequence st q = p ^ r
thus  ex r being FinSequence st q = p ^ r by A1, FINSEQ_1:80; ::_thesis: verum
end;
given r being FinSequence such that A2: q = p ^ r ; ::_thesis: p is_a_prefix_of q
 ( dom p = Seg (len p) & p = q | (dom p) ) by A2, FINSEQ_1:21, FINSEQ_1:def_3;
hence  p is_a_prefix_of q by Def1; ::_thesis: verum
end;

theorem Th2: :: TREES_1:2
for p, q being FinSequence st p is_a_prefix_of q & len p = len q holds
p = q
proof
let p, q be FinSequence; ::_thesis: ( p is_a_prefix_of q & len p = len q implies p = q )
assume that
A1: p is_a_prefix_of q and
A2: len p = len q ; ::_thesis: p = q
consider r being FinSequence such that
A3: q = p ^ r by A1, Th1;
 len p = (len p) + (len r) by A2, A3, FINSEQ_1:22;
then  r = {} ;
hence  p = q by A3, FINSEQ_1:34; ::_thesis: verum
end;

theorem Th3: :: TREES_1:3
for x, y being set holds
( <*x*> is_a_prefix_of <*y*> iff x = y )
proof
let x, y be set ; ::_thesis: ( <*x*> is_a_prefix_of <*y*> iff x = y )
thus  ( <*x*> is_a_prefix_of <*y*> implies x = y ) ::_thesis: ( x = y implies <*x*> is_a_prefix_of <*y*> )
proof
assume A1: <*x*> is_a_prefix_of <*y*> ; ::_thesis: x = y
 ( len <*x*> = 1 & len <*y*> = 1 ) by FINSEQ_1:40;
then A2: <*x*> = <*y*> by A1, Th2;
 <*x*> . 1 = x by FINSEQ_1:40;
hence  x = y by A2, FINSEQ_1:40; ::_thesis: verum
end;
thus  ( x = y implies <*x*> is_a_prefix_of <*y*> ) ; ::_thesis: verum
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
let A, B be finite set ; ::_thesis: ( A c= B & card A = card B implies A = B )
assume that
A1: A c= B and
A2: card A = card B ; ::_thesis: A = B
card (B \ A) = (card B) - (card A) by A1, CARD_2:44
.= 0 by A2 ;
then  B \ A = {} ;
then  B c= A by XBOOLE_1:37;
hence  A = B by A1, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem Th4: :: TREES_1:4
for p, q being finite set st p,q are_c=-comparable & card p = card q holds
p = q
proof
let p, q be finite set ; ::_thesis: ( p,q are_c=-comparable & card p = card q implies p = q )
assume that
A1: ( p c= q or q c= p ) and
A2: card p = card q ; :: according to XBOOLE_0:def_9 ::_thesis: p = q
percases ( p c= q or q c= p ) by A1;
suppose p c= q ; ::_thesis: p = q
hence  p = q by A2, Lm1; ::_thesis: verum
end;
suppose q c= p ; ::_thesis: p = q
hence  p = q by A2, Lm1; ::_thesis: verum
end;
end;
end;


theorem Th5: :: TREES_1:5
for x, y being set st <*x*>,<*y*> are_c=-comparable holds
x = y
proof
let x, y be set ; ::_thesis: ( <*x*>,<*y*> are_c=-comparable implies x = y )
assume A1: <*x*>,<*y*> are_c=-comparable ; ::_thesis: x = y
 ( len <*x*> = 1 & len <*y*> = 1 ) by FINSEQ_1:40;
then A2: <*x*> = <*y*> by A1, Th4;
 <*x*> . 1 = x by FINSEQ_1:40;
hence  x = y by A2, FINSEQ_1:40; ::_thesis: verum
end;

theorem Th6: :: TREES_1:6
for p, q being finite set st p c< q holds
card p < card q
proof
let p, q be finite set ; ::_thesis: ( p c< q implies card p < card q )
assume that
A1: p c= q and
A2: p <> q ; :: according to XBOOLE_0:def_8 ::_thesis: card p < card q
A3: card p <= card q by A1, NAT_1:43;
 p,q are_c=-comparable by A1, XBOOLE_0:def_9;
hence  card p < card q by A3, A2, Th4, XXREAL_0:1; ::_thesis: verum
end;

theorem Th7: :: TREES_1:7
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
let x be set ; ::_thesis: for p1, p2 being FinSequence st p1 ^ <*x*> is_a_prefix_of p2 holds
p1 is_a_proper_prefix_of p2
let p1, p2 be FinSequence; ::_thesis: ( p1 ^ <*x*> is_a_prefix_of p2 implies p1 is_a_proper_prefix_of p2 )
assume  p1 ^ <*x*> is_a_prefix_of p2 ; ::_thesis: p1 is_a_proper_prefix_of p2
then consider p3 being FinSequence such that
A1: p2 = (p1 ^ <*x*>) ^ p3 by Th1;
 p2 = p1 ^ (<*x*> ^ p3) by A1, FINSEQ_1:32;
hence  p1 is_a_prefix_of p2 by Th1; :: according to XBOOLE_0:def_8 ::_thesis: not p1 = p2
assume  p1 = p2 ; ::_thesis: contradiction
then  len p1 = (len (p1 ^ <*x*>)) + (len p3) by A1, FINSEQ_1:22
.= ((len p1) + (len <*x*>)) + (len p3) by FINSEQ_1:22
.= ((len p1) + 1) + (len p3) by FINSEQ_1:39 ;
then  (len p1) + 1 <= len p1 by NAT_1:11;
hence  contradiction by NAT_1:13; ::_thesis: verum
end;

theorem Th8: :: TREES_1:8
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
let x be set ; ::_thesis: for p1, p2 being FinSequence st p1 is_a_prefix_of p2 holds
p1 is_a_proper_prefix_of p2 ^ <*x*>
let p1, p2 be FinSequence; ::_thesis: ( p1 is_a_prefix_of p2 implies p1 is_a_proper_prefix_of p2 ^ <*x*> )
assume  p1 is_a_prefix_of p2 ; ::_thesis: p1 is_a_proper_prefix_of p2 ^ <*x*>
then consider p3 being FinSequence such that
A1: p2 = p1 ^ p3 by Th1;
 p2 ^ <*x*> = p1 ^ (p3 ^ <*x*>) by A1, FINSEQ_1:32;
hence  p1 is_a_prefix_of p2 ^ <*x*> by Th1; :: according to XBOOLE_0:def_8 ::_thesis: not p1 = p2 ^ <*x*>
assume  p1 = p2 ^ <*x*> ; ::_thesis: contradiction
then  len p2 = (len (p2 ^ <*x*>)) + (len p3) by A1, FINSEQ_1:22
.= ((len p2) + (len <*x*>)) + (len p3) by FINSEQ_1:22
.= ((len p2) + 1) + (len p3) by FINSEQ_1:39 ;
then  (len p2) + 1 <= len p2 by NAT_1:11;
hence  contradiction by NAT_1:13; ::_thesis: verum
end;

theorem Th9: :: TREES_1:9
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
let x be set ; ::_thesis: for p1, p2 being FinSequence st p1 is_a_proper_prefix_of p2 ^ <*x*> holds
p1 is_a_prefix_of p2
let p1, p2 be FinSequence; ::_thesis: ( p1 is_a_proper_prefix_of p2 ^ <*x*> implies p1 is_a_prefix_of p2 )
assume that
A1: p1 is_a_prefix_of p2 ^ <*x*> and
A2: p1 <> p2 ^ <*x*> ; :: according to XBOOLE_0:def_8 ::_thesis: p1 is_a_prefix_of p2
A3: ex p3 being FinSequence st p2 ^ <*x*> = p1 ^ p3 by A1, Th1;
A4: len p1 <= len (p2 ^ <*x*>) by A1, NAT_1:43;
 ( len (p2 ^ <*x*>) = (len p2) + (len <*x*>) & len <*x*> = 1 ) by FINSEQ_1:22, FINSEQ_1:39;
then  len p1 < (len p2) + 1 by A1, A2, A4, Th2, XXREAL_0:1;
then  len p1 <= len p2 by NAT_1:13;
then  ex p3 being FinSequence st p1 ^ p3 = p2 by A3, FINSEQ_1:47;
hence  p1 is_a_prefix_of p2 by Th1; ::_thesis: verum
end;

theorem :: TREES_1:10
for p2, p1 being FinSequence st ( {} is_a_proper_prefix_of p2 or {} <> p2 ) holds
p1 is_a_proper_prefix_of p1 ^ p2
proof
let p2, p1 be FinSequence; ::_thesis: ( ( {} is_a_proper_prefix_of p2 or {} <> p2 ) implies p1 is_a_proper_prefix_of p1 ^ p2 )
assume A1: ( {} is_a_proper_prefix_of p2 or {} <> p2 ) ; ::_thesis: p1 is_a_proper_prefix_of p1 ^ p2
thus  p1 is_a_prefix_of p1 ^ p2 by Th1; :: according to XBOOLE_0:def_8 ::_thesis: not p1 = p1 ^ p2
assume  p1 = p1 ^ p2 ; ::_thesis: contradiction
then  len p1 = (len p1) + (len p2) by FINSEQ_1:22;
then  p2 = {} ;
hence  contradiction by A1; ::_thesis: verum
end;

definition
let p be FinSequence;
func ProperPrefixes p ->  set  means :Def2: :: TREES_1:def 2
 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
set E = rng p;
defpred S1[ set ] means  ex q being FinSequence st
( $1 = q & q is_a_proper_prefix_of p );
consider X being set  such that
A1: for x being set holds
( x in X iff ( x in (rng p) * & S1[x] ) ) from XBOOLE_0:sch_1();
take  X ; ::_thesis: for x being set holds
( x in X iff ex q being FinSequence st
( x = q & q is_a_proper_prefix_of p ) )
let x be set ; ::_thesis: ( x in X iff ex q being FinSequence st
( x = q & q is_a_proper_prefix_of p ) )
thus  ( x in X implies ex q being FinSequence st
( x = q & q is_a_proper_prefix_of p ) ) by A1; ::_thesis: ( ex q being FinSequence st
( x = q & q is_a_proper_prefix_of p ) implies x in X )
given q being FinSequence such that A2: x = q and
A3: q is_a_proper_prefix_of p ; ::_thesis: x in X
 q is_a_prefix_of p by A3, XBOOLE_0:def_8;
then  ex n being Element of NAT st q = p | (Seg n) by Def1;
then  rng q c= rng p by RELAT_1:70;
then reconsider q = q as FinSequence of rng p by FINSEQ_1:def_4;
 q in (rng p) * by FINSEQ_1:def_11;
hence  x in X by A1, A2, A3; ::_thesis: verum
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
let S1, S2 be set ; ::_thesis: ( ( for x being set holds
( x in S1 iff ex q being FinSequence st
( x = q & q is_a_proper_prefix_of p ) ) ) & ( for x being set holds
( x in S2 iff ex q being FinSequence st
( x = q & q is_a_proper_prefix_of p ) ) ) implies S1 = S2 )
assume that
A4: for x being set holds
( x in S1 iff ex q being FinSequence st
( x = q & q is_a_proper_prefix_of p ) ) and
A5: for x being set holds
( x in S2 iff ex q being FinSequence st
( x = q & q is_a_proper_prefix_of p ) ) ; ::_thesis: S1 = S2
defpred S1[ set ] means  ex q being FinSequence st
( $1 = q & q is_a_proper_prefix_of p );
A6: for x being set holds
( x in S1 iff S1[x] ) by A4;
A7: for x being set holds
( x in S2 iff S1[x] ) by A5;
thus  S1 = S2 from XBOOLE_0:sch_2(A6, A7); ::_thesis: verum
end;
end;

:: deftheorem Def2 defines ProperPrefixes TREES_1:def_2_:_
 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 Th11: :: TREES_1:11
for x being set
for p being FinSequence st x in ProperPrefixes p holds
x is FinSequence
proof
let x be set ; ::_thesis: for p being FinSequence st x in ProperPrefixes p holds
x is FinSequence
let p be FinSequence; ::_thesis: ( x in ProperPrefixes p implies x is FinSequence )
assume  x in ProperPrefixes p ; ::_thesis: x is FinSequence
then  ex q being FinSequence st
( x = q & q is_a_proper_prefix_of p ) by Def2;
hence  x is FinSequence ; ::_thesis: verum
end;

theorem Th12: :: TREES_1:12
for p, q being FinSequence holds
( p in ProperPrefixes q iff p is_a_proper_prefix_of q )
proof
let p, q be FinSequence; ::_thesis: ( p in ProperPrefixes q iff p is_a_proper_prefix_of q )
thus  ( p in ProperPrefixes q implies p is_a_proper_prefix_of q ) ::_thesis: ( p is_a_proper_prefix_of q implies p in ProperPrefixes q )
proof
assume  p in ProperPrefixes q ; ::_thesis: p is_a_proper_prefix_of q
then  ex r being FinSequence st
( p = r & r is_a_proper_prefix_of q ) by Def2;
hence  p is_a_proper_prefix_of q ; ::_thesis: verum
end;
thus  ( p is_a_proper_prefix_of q implies p in ProperPrefixes q ) by Def2; ::_thesis: verum
end;

theorem Th13: :: TREES_1:13
for p, q being FinSequence st p in ProperPrefixes q holds
len p < len q
proof
let p, q be FinSequence; ::_thesis: ( p in ProperPrefixes q implies len p < len q )
assume  p in ProperPrefixes q ; ::_thesis: len p < len q
then  p is_a_proper_prefix_of q by Th12;
hence  len p < len q by Th6; ::_thesis: verum
end;

theorem :: TREES_1:14
for p, q, r being FinSequence st q ^ r in ProperPrefixes p holds
q in ProperPrefixes p
proof
let p, q, r be FinSequence; ::_thesis: ( q ^ r in ProperPrefixes p implies q in ProperPrefixes p )
assume A1: q ^ r in ProperPrefixes p ; ::_thesis: q in ProperPrefixes p
A2: q is_a_prefix_of q ^ r by Th1;
 q ^ r is_a_proper_prefix_of p by A1, Th12;
then  q is_a_proper_prefix_of p by A2, XBOOLE_1:59;
hence  q in ProperPrefixes p by Th12; ::_thesis: verum
end;

theorem Th15: :: TREES_1:15
ProperPrefixes {} = {}
proof
set x = the Element of ProperPrefixes {};
assume A1: not ProperPrefixes {} = {} ; ::_thesis: contradiction
then reconsider x = the Element of ProperPrefixes {} as FinSequence by Th11;
 x is_a_proper_prefix_of {} by A1, Th12;
hence  contradiction by XBOOLE_1:115; ::_thesis: verum
end;

set D = {{}};

theorem Th16: :: TREES_1:16
for x being set holds ProperPrefixes <*x*> = {{}}
proof
let x be set ; ::_thesis: ProperPrefixes <*x*> = {{}}
thus  ProperPrefixes <*x*> c= {{}} :: according to XBOOLE_0:def_10 ::_thesis: {{}} is_a_prefix_of ProperPrefixes <*x*>
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in ProperPrefixes <*x*> or y in {{}} )
assume  y in ProperPrefixes <*x*> ; ::_thesis: y in {{}}
then consider p being FinSequence such that
A1: y = p and
A2: p is_a_proper_prefix_of <*x*> by Def2;
A3: len p < len <*x*> by A2, Th6;
 ( len <*x*> = 1 & 1 = 0 + 1 ) by FINSEQ_1:39;
then  p = {} by A3, NAT_1:13;
hence  y in {{}} by A1, TARSKI:def_1; ::_thesis: verum
end;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in {{}} or y in ProperPrefixes <*x*> )
assume  y in {{}} ; ::_thesis: y in ProperPrefixes <*x*>
then A4: y = {} by TARSKI:def_1;
 {} is_a_prefix_of <*x*> by XBOOLE_1:2;
then  {} is_a_proper_prefix_of <*x*> by XBOOLE_0:def_8;
hence  y in ProperPrefixes <*x*> by A4, Def2; ::_thesis: verum
end;

theorem :: TREES_1:17
for p, q being FinSequence st p is_a_prefix_of q holds
ProperPrefixes p c= ProperPrefixes q
proof
let p, q be FinSequence; ::_thesis: ( p is_a_prefix_of q implies ProperPrefixes p c= ProperPrefixes q )
assume A1: p is_a_prefix_of q ; ::_thesis: ProperPrefixes p c= ProperPrefixes q
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in ProperPrefixes p or x in ProperPrefixes q )
assume A2: x in ProperPrefixes p ; ::_thesis: x in ProperPrefixes q
then reconsider r = x as FinSequence by Th11;
 r is_a_proper_prefix_of p by A2, Th12;
then  r is_a_proper_prefix_of q by A1, XBOOLE_1:58;
hence  x in ProperPrefixes q by Th12; ::_thesis: verum
end;

theorem Th18: :: TREES_1:18
for p, q, r being FinSequence st q in ProperPrefixes p & r in ProperPrefixes p holds
q,r are_c=-comparable
proof
let p, q, r be FinSequence; ::_thesis: ( q in ProperPrefixes p & r in ProperPrefixes p implies q,r are_c=-comparable )
assume  q in ProperPrefixes p ; ::_thesis: ( not r in ProperPrefixes p or q,r are_c=-comparable )
then A1: ex q1 being FinSequence st
( q = q1 & q1 is_a_proper_prefix_of p ) by Def2;
assume  r in ProperPrefixes p ; ::_thesis: q,r are_c=-comparable
then A2: ex r1 being FinSequence st
( r = r1 & r1 is_a_proper_prefix_of p ) by Def2;
 q is_a_prefix_of p by A1, XBOOLE_0:def_8;
then consider n being Element of NAT  such that
A3: q = p | (Seg n) by Def1;
 r is_a_prefix_of p by A2, XBOOLE_0:def_8;
then consider k being Element of NAT  such that
A4: r = p | (Seg k) by Def1;
A5: ( n <= k implies q,r are_c=-comparable )
proof
assume  n <= k ; ::_thesis: q,r are_c=-comparable
then  Seg n c= Seg k by FINSEQ_1:5;
then  q = r | (Seg n) by A3, A4, FUNCT_1:51;
then  q is_a_prefix_of r by Def1;
hence  q,r are_c=-comparable by XBOOLE_0:def_9; ::_thesis: verum
end;
 ( k <= n implies q,r are_c=-comparable )
proof
assume  k <= n ; ::_thesis: q,r are_c=-comparable
then  Seg k c= Seg n by FINSEQ_1:5;
then  r = q | (Seg k) by A3, A4, FUNCT_1:51;
then  r is_a_prefix_of q by Def1;
hence  q,r are_c=-comparable by XBOOLE_0:def_9; ::_thesis: verum
end;
hence  q,r are_c=-comparable by A5; ::_thesis: verum
end;

definition
let X be set ;
attrX is Tree-like  means :Def3: :: TREES_1:def 3
( 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 Element of NAT st p ^ <*k*> in X & n <= k holds
p ^ <*n*> in X ) );
end;

:: deftheorem Def3 defines Tree-like TREES_1:def_3_:_
 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 Element of NAT st p ^ <*k*> in X & n <= k holds
p ^ <*n*> in X ) ) );

registration
cluster{{}} ->  Tree-like ;
coherence
 {{}} is Tree-like
proof
thus  {{}} c= NAT * :: according to TREES_1:def_3 ::_thesis: ( ( for p being FinSequence of NAT st p in {{}} holds
ProperPrefixes p c= {{}} ) & ( for p being FinSequence of NAT
for k, n being Element of NAT st p ^ <*k*> in {{}} & n <= k holds
p ^ <*n*> in {{}} ) )
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {{}} or x in NAT * )
assume  x in {{}} ; ::_thesis: x in NAT *
then  x = {} by TARSKI:def_1;
hence  x in NAT * by FINSEQ_1:49; ::_thesis: verum
end;
thus  for p being FinSequence of NAT st p in {{}} holds
ProperPrefixes p c= {{}} ::_thesis: for p being FinSequence of NAT
for k, n being Element of NAT st p ^ <*k*> in {{}} & n <= k holds
p ^ <*n*> in {{}}
proof
let p be FinSequence of NAT ; ::_thesis: ( p in {{}} implies ProperPrefixes p c= {{}} )
assume  p in {{}} ; ::_thesis: ProperPrefixes p c= {{}}
then  p = {} by TARSKI:def_1;
hence  ProperPrefixes p c= {{}} by Th15, XBOOLE_1:2; ::_thesis: verum
end;
thus  for p being FinSequence of NAT
for k, n being Element of NAT st p ^ <*k*> in {{}} & n <= k holds
p ^ <*n*> in {{}} by TARSKI:def_1; ::_thesis: verum
end;
end;

registration
cluster non empty Tree-like for set ;
existence
 ex b1 being set st
( not b1 is empty & b1 is Tree-like )
proof
take D = {(<*> NAT)}; ::_thesis: ( not D is empty & D is Tree-like )
thus  ( not D is empty & D is Tree-like ) ; ::_thesis: verum
end;
end;

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


theorem Th19: :: TREES_1:19
for x being set
for T being Tree st x in T holds
x is FinSequence of NAT
proof
let x be set ; ::_thesis: for T being Tree st x in T holds
x is FinSequence of NAT
let T be Tree; ::_thesis: ( x in T implies x is FinSequence of NAT )
 T c= NAT * by Def3;
hence  ( x in T implies x is FinSequence of NAT ) by FINSEQ_1:def_11; ::_thesis: verum
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 Th19;
end;

theorem Th20: :: TREES_1:20
for T being Tree
for p, q being FinSequence st p in T & q is_a_prefix_of p holds
q in T
proof
let T be Tree; ::_thesis: for p, q being FinSequence st p in T & q is_a_prefix_of p holds
q in T
let p, q be FinSequence; ::_thesis: ( p in T & q is_a_prefix_of p implies q in T )
assume that
A1: p in T and
A2: q is_a_prefix_of p ; ::_thesis: q in T
reconsider r = p as Element of T by A1;
A3: ProperPrefixes r c= T by Def3;
 ( q is_a_proper_prefix_of p or q = p ) by A2, XBOOLE_0:def_8;
then  ( q in ProperPrefixes p or p = q ) by Th12;
hence  q in T by A3; ::_thesis: verum
end;

theorem Th21: :: TREES_1:21
for q being FinSequence of NAT
for T being Tree
for r being FinSequence st q ^ r in T holds
q in T
proof
let q be FinSequence of NAT ; ::_thesis: for T being Tree
for r being FinSequence st q ^ r in T holds
q in T
let T be Tree; ::_thesis: for r being FinSequence st q ^ r in T holds
q in T
let r be FinSequence; ::_thesis: ( q ^ r in T implies q in T )
assume A1: q ^ r in T ; ::_thesis: q in T
then reconsider p = q ^ r as FinSequence of NAT by Th19;
reconsider s = p | (Seg (len q)) as FinSequence of NAT by FINSEQ_1:18;
 len p = (len q) + (len r) by FINSEQ_1:22;
then  len q <= len p by NAT_1:11;
then A2: len s = len q by FINSEQ_1:17;
now__::_thesis:_for_n_being_Nat_st_1_<=_n_&_n_<=_len_q_holds_
q_._n_=_s_._n
let n be Nat; ::_thesis: ( 1 <= n & n <= len q implies q . n = s . n )
assume  ( 1 <= n & n <= len q ) ; ::_thesis: q . n = s . n
then A3: n in Seg (len q) by FINSEQ_1:1;
 Seg (len q) = dom q by FINSEQ_1:def_3;
then  p . n = q . n by A3, FINSEQ_1:def_7;
hence  q . n = s . n by A3, FUNCT_1:49; ::_thesis: verum
end;
then  q = s by A2, FINSEQ_1:14;
then A4: q is_a_prefix_of p by Def1;
now__::_thesis:_(_q_<>_p_implies_q_in_T_)
assume  q <> p ; ::_thesis: q in T
then  q is_a_proper_prefix_of p by A4, XBOOLE_0:def_8;
then A5: q in ProperPrefixes p by Def2;
 ProperPrefixes p c= T by A1, Def3;
hence  q in T by A5; ::_thesis: verum
end;
hence  q in T by A1; ::_thesis: verum
end;

theorem Th22: :: TREES_1:22
for T being Tree holds
( {} in T & <*> NAT in T )
proof
let T be Tree; ::_thesis: ( {} in T & <*> NAT in T )
reconsider x = the Element of T as FinSequence of NAT ;
 x in T ;
then A1: {} ^ x in T by FINSEQ_1:34;
 {} = <*> NAT ;
hence  ( {} in T & <*> NAT in T ) by A1, Th21; ::_thesis: verum
end;

theorem :: TREES_1:23
{{}} is Tree ;

registration
let T, T1 be Tree;
clusterT \/ T1 ->  Tree-like ;
coherence
 T \/ T1 is Tree-like
proof
set D = T \/ T1;
 ( T c= NAT * & T1 c= NAT * ) by Def3;
hence  T \/ T1 c= NAT * by XBOOLE_1:8; :: according to TREES_1:def_3 ::_thesis: ( ( for p being FinSequence of NAT st p in T \/ T1 holds
ProperPrefixes p c= T \/ T1 ) & ( for p being FinSequence of NAT
for k, n being Element of NAT st p ^ <*k*> in T \/ T1 & n <= k holds
p ^ <*n*> in T \/ T1 ) )
thus  for p being FinSequence of NAT st p in T \/ T1 holds
ProperPrefixes p c= T \/ T1 ::_thesis: for p being FinSequence of NAT
for k, n being Element of NAT st p ^ <*k*> in T \/ T1 & n <= k holds
p ^ <*n*> in T \/ T1
proof
let p be FinSequence of NAT ; ::_thesis: ( p in T \/ T1 implies ProperPrefixes p c= T \/ T1 )
assume  p in T \/ T1 ; ::_thesis: ProperPrefixes p c= T \/ T1
then  ( p in T or p in T1 ) by XBOOLE_0:def_3;
then A1: ( ProperPrefixes p c= T or ProperPrefixes p c= T1 ) by Def3;
 ( T c= T \/ T1 & T1 c= T \/ T1 ) by XBOOLE_1:7;
hence  ProperPrefixes p c= T \/ T1 by A1, XBOOLE_1:1; ::_thesis: verum
end;
let p be FinSequence of NAT ; ::_thesis: for k, n being Element of NAT st p ^ <*k*> in T \/ T1 & n <= k holds
p ^ <*n*> in T \/ T1
let k, n be Element of NAT ; ::_thesis: ( p ^ <*k*> in T \/ T1 & n <= k implies p ^ <*n*> in T \/ T1 )
assume that
A2: p ^ <*k*> in T \/ T1 and
A3: n <= k ; ::_thesis: p ^ <*n*> in T \/ T1
 ( p ^ <*k*> in T or p ^ <*k*> in T1 ) by A2, XBOOLE_0:def_3;
then  ( p ^ <*n*> in T or p ^ <*n*> in T1 ) by A3, Def3;
hence  p ^ <*n*> in T \/ T1 by XBOOLE_0:def_3; ::_thesis: verum
end;
clusterT /\ T1 ->  non empty Tree-like ;
coherence
 ( T /\ T1 is Tree-like & not T /\ T1 is empty )
proof
set D = T /\ T1;
thus  T /\ T1 is Tree-like ::_thesis: not T /\ T1 is empty
proof
 ( T c= NAT * & T /\ T1 c= T ) by Def3, XBOOLE_1:17;
hence  T /\ T1 c= NAT * by XBOOLE_1:1; :: according to TREES_1:def_3 ::_thesis: ( ( for p being FinSequence of NAT st p in T /\ T1 holds
ProperPrefixes p c= T /\ T1 ) & ( for p being FinSequence of NAT
for k, n being Element of NAT st p ^ <*k*> in T /\ T1 & n <= k holds
p ^ <*n*> in T /\ T1 ) )
thus  for p being FinSequence of NAT st p in T /\ T1 holds
ProperPrefixes p c= T /\ T1 ::_thesis: for p being FinSequence of NAT
for k, n being Element of NAT st p ^ <*k*> in T /\ T1 & n <= k holds
p ^ <*n*> in T /\ T1
proof
let p be FinSequence of NAT ; ::_thesis: ( p in T /\ T1 implies ProperPrefixes p c= T /\ T1 )
assume A4: p in T /\ T1 ; ::_thesis: ProperPrefixes p c= T /\ T1
then A5: p in T by XBOOLE_0:def_4;
A6: p in T1 by A4, XBOOLE_0:def_4;
A7: ProperPrefixes p c= T by A5, Def3;
 ProperPrefixes p c= T1 by A6, Def3;
hence  ProperPrefixes p c= T /\ T1 by A7, XBOOLE_1:19; ::_thesis: verum
end;
let p be FinSequence of NAT ; ::_thesis: for k, n being Element of NAT st p ^ <*k*> in T /\ T1 & n <= k holds
p ^ <*n*> in T /\ T1
let k, n be Element of NAT ; ::_thesis: ( p ^ <*k*> in T /\ T1 & n <= k implies p ^ <*n*> in T /\ T1 )
assume that
A8: p ^ <*k*> in T /\ T1 and
A9: n <= k ; ::_thesis: p ^ <*n*> in T /\ T1
A10: p ^ <*k*> in T by A8, XBOOLE_0:def_4;
A11: p ^ <*k*> in T1 by A8, XBOOLE_0:def_4;
A12: p ^ <*n*> in T by A9, A10, Def3;
 p ^ <*n*> in T1 by A9, A11, Def3;
hence  p ^ <*n*> in T /\ T1 by A12, XBOOLE_0:def_4; ::_thesis: verum
end;
 ( {} in T & {} in T1 ) by Th22;
hence  not T /\ T1 is empty by XBOOLE_0:def_4; ::_thesis: verum
end;
end;

theorem :: TREES_1:24
for T, T1 being Tree holds T \/ T1 is Tree ;

theorem :: TREES_1:25
for T, T1 being Tree holds T /\ T1 is Tree ;

registration
cluster non empty finite Tree-like for set ;
existence
 ex b1 being Tree st b1 is finite
proof
take  {{}} ; ::_thesis: {{}} is finite
thus  {{}} is finite ; ::_thesis: verum
end;
end;


theorem :: TREES_1:26
for fT, fT1 being finite Tree holds fT \/ fT1 is finite Tree ;

theorem :: TREES_1:27
for T being Tree
for fT being finite Tree holds fT /\ T is finite Tree ;

definition
let n be Element of NAT ;
func elementary_tree n ->  Tree equals :: TREES_1:def 4
 {  <*k*> where k is Element of NAT : k < n  }  \/ {{}};
correctness
coherence
{  <*k*> where k is Element of NAT : k < n  }  \/ {{}} is Tree;
proof
set IT =  {  <*k*> where k is Element of NAT : k < n  }  \/ {{}};
  {  <*k*> where k is Element of NAT : k < n  }  \/ {{}} is Tree-like
proof
thus   {  <*k*> where k is Element of NAT : k < n  }  \/ {{}} c= NAT * :: according to TREES_1:def_3 ::_thesis: ( ( for p being FinSequence of NAT st p in  {  <*k*> where k is Element of NAT : k < n  }  \/ {{}} holds
ProperPrefixes p c=  {  <*k*> where k is Element of NAT : k < n  }  \/ {{}} ) & ( for p being FinSequence of NAT
for k, n being Element of NAT st p ^ <*k*> in  {  <*k*> where k is Element of NAT : k < n  }  \/ {{}} & n <= k holds
p ^ <*n*> in  {  <*k*> where k is Element of NAT : k < n  }  \/ {{}} ) )
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  <*k*> where k is Element of NAT : k < n  }  \/ {{}} or x in NAT * )
assume  x in  {  <*k*> where k is Element of NAT : k < n  }  \/ {{}} ; ::_thesis: x in NAT *
then A1: ( x in  {  <*k*> where k is Element of NAT : k < n  }  or x in {{}} ) by XBOOLE_0:def_3;
A2: {} in NAT * by FINSEQ_1:49;
now__::_thesis:_(_x_in__{__<*k*>_where_k_is_Element_of_NAT_:_k_<_n__}__implies_x_in_NAT_*_)
assume  x in  {  <*k*> where k is Element of NAT : k < n  }  ; ::_thesis: x in NAT *
then  ex k being Element of NAT st
( x = <*k*> & k < n ) ;
hence  x in NAT * by FINSEQ_1:def_11; ::_thesis: verum
end;
hence  x in NAT * by A1, A2, TARSKI:def_1; ::_thesis: verum
end;
thus  for p being FinSequence of NAT st p in  {  <*k*> where k is Element of NAT : k < n  }  \/ {{}} holds
ProperPrefixes p c=  {  <*k*> where k is Element of NAT : k < n  }  \/ {{}} ::_thesis: for p being FinSequence of NAT
for k, n being Element of NAT st p ^ <*k*> in  {  <*k*> where k is Element of NAT : k < n  }  \/ {{}} & n <= k holds
p ^ <*n*> in  {  <*k*> where k is Element of NAT : k < n  }  \/ {{}}
proof
let p be FinSequence of NAT ; ::_thesis: ( p in  {  <*k*> where k is Element of NAT : k < n  }  \/ {{}} implies ProperPrefixes p c=  {  <*k*> where k is Element of NAT : k < n  }  \/ {{}} )
assume  p in  {  <*k*> where k is Element of NAT : k < n  }  \/ {{}} ; ::_thesis: ProperPrefixes p c=  {  <*k*> where k is Element of NAT : k < n  }  \/ {{}}
then A3: ( p in  {  <*k*> where k is Element of NAT : k < n  }  or p in {{}} ) by XBOOLE_0:def_3;
A4: {} c=  {  <*k*> where k is Element of NAT : k < n  }  \/ {{}} by XBOOLE_1:2;
now__::_thesis:_(_p_in__{__<*k*>_where_k_is_Element_of_NAT_:_k_<_n__}__implies_ProperPrefixes_p_c=__{__<*k*>_where_k_is_Element_of_NAT_:_k_<_n__}__\/_{{}}_)
assume  p in  {  <*k*> where k is Element of NAT : k < n  }  ; ::_thesis: ProperPrefixes p c=  {  <*k*> where k is Element of NAT : k < n  }  \/ {{}}
then  ex k being Element of NAT st
( p = <*k*> & k < n ) ;
then  ProperPrefixes p = {{}} by Th16;
hence  ProperPrefixes p c=  {  <*k*> where k is Element of NAT : k < n  }  \/ {{}} by XBOOLE_1:7; ::_thesis: verum
end;
hence  ProperPrefixes p c=  {  <*k*> where k is Element of NAT : k < n  }  \/ {{}} by A3, A4, Th15, TARSKI:def_1; ::_thesis: verum
end;
let p be FinSequence of NAT ; ::_thesis: for k, n being Element of NAT st p ^ <*k*> in  {  <*k*> where k is Element of NAT : k < n  }  \/ {{}} & n <= k holds
p ^ <*n*> in  {  <*k*> where k is Element of NAT : k < n  }  \/ {{}}
let k, m be Element of NAT ; ::_thesis: ( p ^ <*k*> in  {  <*k*> where k is Element of NAT : k < n  }  \/ {{}} & m <= k implies p ^ <*m*> in  {  <*k*> where k is Element of NAT : k < n  }  \/ {{}} )
assume  p ^ <*k*> in  {  <*k*> where k is Element of NAT : k < n  }  \/ {{}} ; ::_thesis: ( not m <= k or p ^ <*m*> in  {  <*k*> where k is Element of NAT : k < n  }  \/ {{}} )
then  ( p ^ <*k*> in  {  <*j*> where j is Element of NAT : j < n  }  or p ^ <*k*> in {{}} ) by XBOOLE_0:def_3;
then consider l being Element of NAT  such that
A5: p ^ <*k*> = <*l*> and
A6: l < n by TARSKI:def_1;
(len p) + (len <*k*>) = len <*l*> by A5, FINSEQ_1:22
.= 1 by FINSEQ_1:39 ;
then  (len p) + 1 = 0 + 1 by FINSEQ_1:39;
then A7: p = {} ;
then A8: <*k*> = <*l*> by A5, FINSEQ_1:34;
 <*k*> . 1 = k by FINSEQ_1:def_8;
then A9: k = l by A8, FINSEQ_1:def_8;
assume A10: m <= k ; ::_thesis: p ^ <*m*> in  {  <*k*> where k is Element of NAT : k < n  }  \/ {{}}
A11: p ^ <*m*> = <*m*> by A7, FINSEQ_1:34;
 m < n by A6, A9, A10, XXREAL_0:2;
then  p ^ <*m*> in  {  <*j*> where j is Element of NAT : j < n  }  by A11;
hence  p ^ <*m*> in  {  <*k*> where k is Element of NAT : k < n  }  \/ {{}} by XBOOLE_0:def_3; ::_thesis: verum
end;
hence   {  <*k*> where k is Element of NAT : k < n  }  \/ {{}} is Tree ; ::_thesis: verum
end;
end;

:: deftheorem  defines elementary_tree TREES_1:def_4_:_
 for n being Element of NAT holds elementary_tree n =  {  <*k*> where k is Element of NAT : k < n  }  \/ {{}};

registration
let n be Element of NAT ;
cluster elementary_tree n ->  finite ;
coherence
 elementary_tree n is finite
proof
set IT = elementary_tree n;
 elementary_tree n, Seg (n + 1) are_equipotent
proof
defpred S1[ set , set ] means ( ( n = {} & c2 = 1 ) or ex n being Element of NAT st
( n = <*n*> & c2 = n + 2 ) );
A1: for x, y, z being set st x in elementary_tree n & S1[x,y] & S1[x,z] holds
y = z
proof
let x, y, z be set ; ::_thesis: ( x in elementary_tree n & S1[x,y] & S1[x,z] implies y = z )
assume that
 x in elementary_tree n and
A2: ( ( ( x = {} & y = 1 ) or ex n being Element of NAT st
( x = <*n*> & y = n + 2 ) ) & ( ( x = {} & z = 1 ) or ex n being Element of NAT st
( x = <*n*> & z = n + 2 ) ) ) ; ::_thesis: y = z
now__::_thesis:_(_ex_n1_being_Element_of_NAT_st_
(_x_=_<*n1*>_&_y_=_n1_+_2_)_&_ex_n2_being_Element_of_NAT_st_
(_x_=_<*n2*>_&_z_=_n2_+_2_)_implies_y_=_z_)
given n1 being Element of NAT  such that A3: ( x = <*n1*> & y = n1 + 2 ) ; ::_thesis: ( ex n2 being Element of NAT st
( x = <*n2*> & z = n2 + 2 ) implies y = z )
given n2 being Element of NAT  such that A4: ( x = <*n2*> & z = n2 + 2 ) ; ::_thesis: y = z
 <*n1*> . 1 = n1 by FINSEQ_1:def_8;
hence  y = z by A3, A4, FINSEQ_1:def_8; ::_thesis: verum
end;
hence  y = z by A2; ::_thesis: verum
end;
A5: for x being set st x in elementary_tree n holds
ex y being set st S1[x,y]
proof
let x be set ; ::_thesis: ( x in elementary_tree n implies ex y being set st S1[x,y] )
assume A6: x in elementary_tree n ; ::_thesis: ex y being set st S1[x,y]
A7: now__::_thesis:_(_x_in__{__<*k*>_where_k_is_Element_of_NAT_:_k_<_n__}__implies_ex_y_being_set_st_S1[x,y]_)
assume  x in  {  <*k*> where k is Element of NAT : k < n  }  ; ::_thesis: ex y being set st S1[x,y]
then consider k being Element of NAT  such that
A8: x = <*k*> and
 k < n ;
reconsider y = k + 2 as set ;
take y = y; ::_thesis: S1[x,y]
thus  S1[x,y] by A8; ::_thesis: verum
end;
now__::_thesis:_(_x_in_{{}}_implies_ex_y_being_set_st_S1[x,y]_)
assume A9: x in {{}} ; ::_thesis: ex y being set st S1[x,y]
reconsider y = 1 as set ;
take y = y; ::_thesis: S1[x,y]
thus  S1[x,y] by A9, TARSKI:def_1; ::_thesis: verum
end;
hence  ex y being set st S1[x,y] by A6, A7, XBOOLE_0:def_3; ::_thesis: verum
end;
consider f being Function such that
A10: ( dom f = elementary_tree n & ( for x being set st x in elementary_tree n holds
S1[x,f . x] ) ) from CLASSES1:sch_1(A5);
take  f ; :: according to WELLORD2:def_4 ::_thesis: ( f is one-to-one & dom f = elementary_tree n & rng f = Seg (n + 1) )
thus  f is one-to-one ::_thesis: ( dom f = elementary_tree n & rng f = Seg (n + 1) )
proof
let x be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds
( not x in dom f or not b1 in dom f or not f . x = f . b1 or x = b1 )
let y be set ; ::_thesis: ( not x in dom f or not y in dom f or not f . x = f . y or x = y )
assume that
A11: x in dom f and
A12: y in dom f and
A13: f . x = f . y ; ::_thesis: x = y
A14: ( ( x = {} & f . x = 1 ) or ex n being Element of NAT st
( x = <*n*> & f . x = n + 2 ) ) by A10, A11;
A15: ( ( y = {} & f . y = 1 ) or ex n being Element of NAT st
( y = <*n*> & f . y = n + 2 ) ) by A10, A12;
A16: now__::_thesis:_(_x_=_{}_&_f_._x_=_1_implies_for_n_being_Element_of_NAT_holds_
(_not_y_=_<*n*>_or_not_f_._y_=_n_+_2_)_)
assume that
 x = {} and
A17: f . x = 1 ; ::_thesis: for n being Element of NAT holds
( not y = <*n*> or not f . y = n + 2 )
given n being Element of NAT  such that  y = <*n*> and
A18: f . y = n + 2 ; ::_thesis: contradiction
 0 + 1 = (n + 1) + 1 by A13, A17, A18;
hence  contradiction ; ::_thesis: verum
end;
now__::_thesis:_(_y_=_{}_&_f_._y_=_1_implies_for_n_being_Element_of_NAT_holds_
(_not_x_=_<*n*>_or_not_f_._x_=_n_+_2_)_)
assume that
 y = {} and
A19: f . y = 1 ; ::_thesis: for n being Element of NAT holds
( not x = <*n*> or not f . x = n + 2 )
given n being Element of NAT  such that  x = <*n*> and
A20: f . x = n + 2 ; ::_thesis: contradiction
 0 + 1 = (n + 1) + 1 by A13, A19, A20;
hence  contradiction ; ::_thesis: verum
end;
hence  x = y by A13, A14, A15, A16; ::_thesis: verum
end;
thus  dom f = elementary_tree n by A10; ::_thesis: rng f = Seg (n + 1)
thus  rng f c= Seg (n + 1) :: according to XBOOLE_0:def_10 ::_thesis: Seg (n + 1) is_a_prefix_of rng f
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng f or x in Seg (n + 1) )
assume  x in rng f ; ::_thesis: x in Seg (n + 1)
then consider y being set  such that
A21: y in dom f and
A22: x = f . y by FUNCT_1:def_3;
 1 <= 1 + n by NAT_1:11;
then A23: 1 in Seg (n + 1) by FINSEQ_1:1;
now__::_thesis:_(_ex_k_being_Element_of_NAT_st_
(_y_=_<*k*>_&_x_=_k_+_2_)_implies_x_in_Seg_(n_+_1)_)
given k being Element of NAT  such that A24: y = <*k*> and
A25: x = k + 2 ; ::_thesis: x in Seg (n + 1)
 ( y in  {  <*j*> where j is Element of NAT : j < n  }  or y in {{}} ) by A10, A21, XBOOLE_0:def_3;
then consider l being Element of NAT  such that
A26: ( y = <*l*> & l < n ) by A24, TARSKI:def_1;
 ( <*k*> . 1 = k & <*l*> . 1 = l ) by FINSEQ_1:def_8;
then  k + 1 <= n by A24, A26, NAT_1:13;
then  ( 1 + 0 <= (k + 1) + 1 & (k + 1) + 1 <= n + 1 ) by XREAL_1:7;
hence  x in Seg (n + 1) by A25, FINSEQ_1:1; ::_thesis: verum
end;
hence  x in Seg (n + 1) by A10, A21, A22, A23; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Seg (n + 1) or x in rng f )
assume A27: x in Seg (n + 1) ; ::_thesis: x in rng f
then reconsider k = x as Element of NAT ;
A28: 1 <= k by A27, FINSEQ_1:1;
A29: k <= n + 1 by A27, FINSEQ_1:1;
 {} in {{}} by TARSKI:def_1;
then A30: {} in elementary_tree n by XBOOLE_0:def_3;
then  S1[ {} ,f . {}] by A10;
then A31: 1 in rng f by A10, A30, FUNCT_1:def_3;
now__::_thesis:_(_1_<_k_implies_k_in_rng_f_)
assume  1 < k ; ::_thesis: k in rng f
then  1 + 1 <= k by NAT_1:13;
then consider m being Nat such that
A32: k = 2 + m by NAT_1:10;
reconsider m = m as Element of NAT by ORDINAL1:def_12;
 (1 + 1) + m = 1 + (1 + m) ;
then  1 + m <= n by A29, A32, XREAL_1:6;
then  m < n by NAT_1:13;
then  <*m*> in  {  <*j*> where j is Element of NAT : j < n  }  ;
then A33: <*m*> in elementary_tree n by XBOOLE_0:def_3;
then  S1[<*m*>,f . <*m*>] by A10;
then  k = f . <*m*> by A1, A32, A33;
hence  k in rng f by A10, A33, FUNCT_1:def_3; ::_thesis: verum
end;
hence  x in rng f by A28, A31, XXREAL_0:1; ::_thesis: verum
end;
hence  elementary_tree n is finite by CARD_1:38; ::_thesis: verum
end;
end;

theorem Th28: :: TREES_1:28
for k, n being Element of NAT st k < n holds
<*k*> in elementary_tree n
proof
let k, n be Element of NAT ; ::_thesis: ( k < n implies <*k*> in elementary_tree n )
assume  k < n ; ::_thesis: <*k*> in elementary_tree n
then  <*k*> in  {  <*j*> where j is Element of NAT : j < n  }  ;
hence  <*k*> in elementary_tree n by XBOOLE_0:def_3; ::_thesis: verum
end;

theorem Th29: :: TREES_1:29
elementary_tree 0 = {{}}
proof
now__::_thesis:_not__{__<*j*>_where_j_is_Element_of_NAT_:_j_<_0__}__<>_{}
set x = the Element of  {  <*j*> where j is Element of NAT : j < 0  }  ;
assume   {  <*j*> where j is Element of NAT : j < 0  }  <> {} ; ::_thesis: contradiction
then  the Element of  {  <*j*> where j is Element of NAT : j < 0  }  in  {  <*j*> where j is Element of NAT : j < 0  }  ;
then  ex k being Element of NAT st
( the Element of  {  <*j*> where j is Element of NAT : j < 0  }  = <*k*> & k < 0 ) ;
hence  contradiction ; ::_thesis: verum
end;
hence  elementary_tree 0 = {{}} ; ::_thesis: verum
end;

theorem :: TREES_1:30
for n being Element of NAT
for p being FinSequence of NAT holds
( not p in elementary_tree n or p = {} or ex k being Element of NAT st
( k < n & p = <*k*> ) )
proof
let n be Element of NAT ; ::_thesis: for p being FinSequence of NAT holds
( not p in elementary_tree n or p = {} or ex k being Element of NAT st
( k < n & p = <*k*> ) )
let p be FinSequence of NAT ; ::_thesis: ( not p in elementary_tree n or p = {} or ex k being Element of NAT st
( k < n & p = <*k*> ) )
assume  p in elementary_tree n ; ::_thesis: ( p = {} or ex k being Element of NAT st
( k < n & p = <*k*> ) )
then A1: ( p in {{}} or p in  {  <*k*> where k is Element of NAT : k < n  }  ) by XBOOLE_0:def_3;
 ( p in  {  <*k*> where k is Element of NAT : k < n  }  implies ex k being Element of NAT st
( p = <*k*> & k < n ) ) ;
hence  ( p = {} or ex k being Element of NAT st
( k < n & p = <*k*> ) ) by A1, TARSKI:def_1; ::_thesis: verum
end;

definition
let T be Tree;
func Leaves T ->  Subset of T means :Def5: :: TREES_1:def 5
 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
defpred S1[ set ] means  for p being FinSequence of NAT st $1 = p holds
for q being FinSequence of NAT st q in T holds
not p is_a_proper_prefix_of q;
consider X being set  such that
A1: for x being set holds
( x in X iff ( x in T & S1[x] ) ) from XBOOLE_0:sch_1();
 X c= T
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in T )
thus  ( not x in X or x in T ) by A1; ::_thesis: verum
end;
then reconsider X = X as Subset of T ;
take  X ; ::_thesis: for p being FinSequence of NAT holds
( p in X iff ( p in T & ( for q being FinSequence of NAT holds
( not q in T or not p is_a_proper_prefix_of q ) ) ) )
let p be FinSequence of NAT ; ::_thesis: ( p in X iff ( p in T & ( for q being FinSequence of NAT holds
( not q in T or not p is_a_proper_prefix_of q ) ) ) )
thus  ( p in X implies ( p in T & ( for q being FinSequence of NAT holds
( not q in T or not p is_a_proper_prefix_of q ) ) ) ) by A1; ::_thesis: ( p in T & ( for q being FinSequence of NAT holds
( not q in T or not p is_a_proper_prefix_of q ) ) implies p in X )
assume that
A2: p in T and
A3: for q being FinSequence of NAT holds
( not q in T or not p is_a_proper_prefix_of q ) ; ::_thesis: p in X
 for r being FinSequence of NAT st p = r holds
for q being FinSequence of NAT st q in T holds
not r is_a_proper_prefix_of q by A3;
hence  p in X by A1, A2; ::_thesis: verum
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
let L1, L2 be Subset of T; ::_thesis: ( ( for p being FinSequence of NAT holds
( p in L1 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 L2 iff ( p in T & ( for q being FinSequence of NAT holds
( not q in T or not p is_a_proper_prefix_of q ) ) ) ) ) implies L1 = L2 )
assume that
A4: for p being FinSequence of NAT holds
( p in L1 iff ( p in T & ( for q being FinSequence of NAT holds
( not q in T or not p is_a_proper_prefix_of q ) ) ) ) and
A5: for p being FinSequence of NAT holds
( p in L2 iff ( p in T & ( for q being FinSequence of NAT holds
( not q in T or not p is_a_proper_prefix_of q ) ) ) ) ; ::_thesis: L1 = L2
A6: T c= NAT * by Def3;
then A7: L1 c= NAT * by XBOOLE_1:1;
A8: L2 c= NAT * by A6, XBOOLE_1:1;
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_L1_implies_x_in_L2_)_&_(_x_in_L2_implies_x_in_L1_)_)
let x be set ; ::_thesis: ( ( x in L1 implies x in L2 ) & ( x in L2 implies x in L1 ) )
thus  ( x in L1 implies x in L2 ) ::_thesis: ( x in L2 implies x in L1 )
proof
assume A9: x in L1 ; ::_thesis: x in L2
then reconsider p = x as FinSequence of NAT by A7, FINSEQ_1:def_11;
 for q being FinSequence of NAT holds
( not q in T or not p is_a_proper_prefix_of q ) by A4, A9;
hence  x in L2 by A5, A9; ::_thesis: verum
end;
assume A10: x in L2 ; ::_thesis: x in L1
then reconsider p = x as FinSequence of NAT by A8, FINSEQ_1:def_11;
 for q being FinSequence of NAT holds
( not q in T or not p is_a_proper_prefix_of q ) by A5, A10;
hence  x in L1 by A4, A10; ::_thesis: verum
end;
hence  L1 = L2 by TARSKI:1; ::_thesis: verum
end;
let p be FinSequence of NAT ;
assume B11: p in T ;
funcT | p ->  Tree means :Def6: :: TREES_1:def 6
 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
defpred S1[ set ] means  for q being FinSequence of NAT st $1 = q holds
p ^ q in T;
consider X being set  such that
A11: for x being set holds
( x in X iff ( x in NAT * & S1[x] ) ) from XBOOLE_0:sch_1();
 ( <*> NAT in NAT * & ( for q being FinSequence of NAT st <*> NAT = q holds
p ^ q in T ) ) by B11, FINSEQ_1:34, FINSEQ_1:def_11;
then reconsider X = X as non empty set by A11;
A12: X c= NAT *
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in NAT * )
thus  ( not x in X or x in NAT * ) by A11; ::_thesis: verum
end;
A13: now__::_thesis:_for_q_being_FinSequence_of_NAT_st_q_in_X_holds_
ProperPrefixes_q_c=_X
let q be FinSequence of NAT ; ::_thesis: ( q in X implies ProperPrefixes q c= X )
assume A14: q in X ; ::_thesis: ProperPrefixes q c= X
thus  ProperPrefixes q c= X ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in ProperPrefixes q or x in X )
assume  x in ProperPrefixes q ; ::_thesis: x in X
then consider r being FinSequence such that
A15: x = r and
A16: r is_a_proper_prefix_of q by Def2;
 r is_a_prefix_of q by A16, XBOOLE_0:def_8;
then A17: ex n being Element of NAT st r = q | (Seg n) by Def1;
then reconsider r = r as FinSequence of NAT by FINSEQ_1:18;
consider s being FinSequence such that
A18: q = r ^ s by A17, FINSEQ_1:80;
A19: p ^ q in T by A11, A14;
 p ^ q = (p ^ r) ^ s by A18, FINSEQ_1:32;
then  ( r in NAT * & ( for q being FinSequence of NAT st r = q holds
p ^ q in T ) ) by A19, Th21, FINSEQ_1:def_11;
hence  x in X by A11, A15; ::_thesis: verum
end;
end;
now__::_thesis:_for_q_being_FinSequence_of_NAT_
for_k,_n_being_Element_of_NAT_st_q_^_<*k*>_in_X_&_n_<=_k_holds_
q_^_<*n*>_in_X
let q be FinSequence of NAT ; ::_thesis: for k, n being Element of NAT st q ^ <*k*> in X & n <= k holds
q ^ <*n*> in X
let k, n be Element of NAT ; ::_thesis: ( q ^ <*k*> in X & n <= k implies q ^ <*n*> in X )
assume that
A20: q ^ <*k*> in X and
A21: n <= k ; ::_thesis: q ^ <*n*> in X
 p ^ (q ^ <*k*>) in T by A11, A20;
then  (p ^ q) ^ <*k*> in T by FINSEQ_1:32;
then  (p ^ q) ^ <*n*> in T by A21, Def3;
then  ( q ^ <*n*> in NAT * & ( for r being FinSequence of NAT st r = q ^ <*n*> holds
p ^ r in T ) ) by FINSEQ_1:32, FINSEQ_1:def_11;
hence  q ^ <*n*> in X by A11; ::_thesis: verum
end;
then reconsider X = X as Tree by A12, A13, Def3;
take  X ; ::_thesis: for q being FinSequence of NAT holds
( q in X iff p ^ q in T )
let q be FinSequence of NAT ; ::_thesis: ( q in X iff p ^ q in T )
thus  ( q in X implies p ^ q in T ) by A11; ::_thesis: ( p ^ q in T implies q in X )
assume  p ^ q in T ; ::_thesis: q in X
then  ( q in NAT * & ( for r being FinSequence of NAT st q = r holds
p ^ r in T ) ) by FINSEQ_1:def_11;
hence  q in X by A11; ::_thesis: verum
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
let T1, T2 be Tree; ::_thesis: ( ( for q being FinSequence of NAT holds
( q in T1 iff p ^ q in T ) ) & ( for q being FinSequence of NAT holds
( q in T2 iff p ^ q in T ) ) implies T1 = T2 )
assume that
A22: for q being FinSequence of NAT holds
( q in T1 iff p ^ q in T ) and
A23: for q being FinSequence of NAT holds
( q in T2 iff p ^ q in T ) ; ::_thesis: T1 = T2
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_T1_implies_x_in_T2_)_&_(_x_in_T2_implies_x_in_T1_)_)
let x be set ; ::_thesis: ( ( x in T1 implies x in T2 ) & ( x in T2 implies x in T1 ) )
thus  ( x in T1 implies x in T2 ) ::_thesis: ( x in T2 implies x in T1 )
proof
assume A24: x in T1 ; ::_thesis: x in T2
then reconsider q = x as FinSequence of NAT by Th19;
 p ^ q in T by A22, A24;
hence  x in T2 by A23; ::_thesis: verum
end;
assume A25: x in T2 ; ::_thesis: x in T1
then reconsider q = x as FinSequence of NAT by Th19;
 p ^ q in T by A23, A25;
hence  x in T1 by A22; ::_thesis: verum
end;
hence  T1 = T2 by TARSKI:1; ::_thesis: verum
end;
end;

:: deftheorem Def5 defines Leaves TREES_1:def_5_:_
 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 Def6 defines | TREES_1:def_6_:_
 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:31
for T being Tree holds T | (<*> NAT) = T
proof
let T be Tree; ::_thesis: T | (<*> NAT) = T
A1: <*> NAT in T by Th22;
thus  T | (<*> NAT) c= T :: according to XBOOLE_0:def_10 ::_thesis: T is_a_prefix_of T | (<*> NAT)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in T | (<*> NAT) or x in T )
assume  x in T | (<*> NAT) ; ::_thesis: x in T
then reconsider p = x as Element of T | (<*> NAT) ;
 {} ^ p = p by FINSEQ_1:34;
hence  x in T by A1, Def6; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in T or x in T | (<*> NAT) )
assume  x in T ; ::_thesis: x in T | (<*> NAT)
then reconsider p = x as Element of T ;
 {} ^ p = p by FINSEQ_1:34;
hence  x in T | (<*> NAT) by A1, Def6; ::_thesis: verum
end;

registration
let T be finite Tree;
let p be Element of T;
clusterT | p ->  finite ;
coherence
 T | p is finite
proof
consider t being Function such that
A1: rng t = T and
A2: dom t in omega by FINSET_1:def_1;
defpred S1[ set , set ] means  ex q being FinSequence of NAT st
( t . T = q & ( ex r being FinSequence of NAT st
( p = r & q = p ^ r ) or ( ( for r being FinSequence of NAT holds q <> p ^ r ) & p = <*> NAT ) ) );
A3: for x being set st x in dom t holds
ex y being set st S1[x,y]
proof
let x be set ; ::_thesis: ( x in dom t implies ex y being set st S1[x,y] )
assume  x in dom t ; ::_thesis: ex y being set st S1[x,y]
then  t . x in T by A1, FUNCT_1:def_3;
then reconsider q = t . x as FinSequence of NAT by Th19;
 ( ex r being FinSequence of NAT st q = p ^ r implies ex y being set st S1[x,y] ) ;
hence  ex y being set st S1[x,y] ; ::_thesis: verum
end;
consider f being Function such that
A4: ( dom f = dom t & ( for x being set st x in dom t holds
S1[x,f . x] ) ) from CLASSES1:sch_1(A3);
 T | p is finite
proof
take  f ; :: according to FINSET_1:def_1 ::_thesis: ( rng f = T | p & dom f in omega )
thus  rng f c= T | p :: according to XBOOLE_0:def_10 ::_thesis: ( T | p is_a_prefix_of rng f & dom f in omega )
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng f or x in T | p )
assume  x in rng f ; ::_thesis: x in T | p
then consider y being set  such that
A5: y in dom f and
A6: x = f . y by FUNCT_1:def_3;
consider q being FinSequence of NAT  such that
A7: t . y = q and
A8: ( ex r being FinSequence of NAT st
( x = r & q = p ^ r ) or ( ( for r being FinSequence of NAT holds q <> p ^ r ) & x = <*> NAT ) ) by A4, A5, A6;
assume A9: not x in T | p ; ::_thesis: contradiction
 ( p ^ (<*> NAT) = p & q in T ) by A1, A4, A5, A7, FINSEQ_1:34, FUNCT_1:def_3;
hence  contradiction by A8, A9, Def6; ::_thesis: verum
end;
thus  T | p c= rng f ::_thesis: dom f in omega
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in T | p or x in rng f )
assume A10: x in T | p ; ::_thesis: x in rng f
then reconsider q = x as FinSequence of NAT by Th19;
 p ^ q in T by A10, Def6;
then consider y being set  such that
A11: y in dom t and
A12: p ^ q = t . y by A1, FUNCT_1:def_3;
 S1[y,f . y] by A4, A11;
then  x = f . y by A12, FINSEQ_1:33;
hence  x in rng f by A4, A11, FUNCT_1:def_3; ::_thesis: verum
end;
thus  dom f in omega by A2, A4; ::_thesis: verum
end;
hence  T | p is finite ; ::_thesis: verum
end;
end;

definition
let T be Tree;
assume A1: Leaves T <> {} ;
mode Leaf of T ->  Element of T means :: TREES_1:def 7
it in Leaves T;
existence
 ex b1 being Element of T st b1 in Leaves T
proof
set x = the Element of Leaves T;
reconsider x = the Element of Leaves T as Element of T by A1, TARSKI:def_3;
take  x ; ::_thesis: x in Leaves T
thus  x in Leaves T by A1; ::_thesis: verum
end;
end;

:: deftheorem  defines Leaf TREES_1:def_7_:_
 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 8
 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
set p = the Element of T;
take  T | the Element of T ; ::_thesis: ex p being Element of T st T | the Element of T = T | p
take  the Element of T ; ::_thesis: T | the Element of T = T | the Element of T
thus  T | the Element of T = T | the Element of T ; ::_thesis: verum
end;
end;

:: deftheorem  defines Subtree TREES_1:def_8_:_
 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 ;
funcT with-replacement (p,T1) ->  Tree means :Def9: :: TREES_1:def 9
 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
reconsider p9 = p as Element of T by A1;
 not p is_a_proper_prefix_of p9 ;
then  p in  {  t where t is Element of T : not p is_a_proper_prefix_of t  }  ;
then reconsider X =  {  t where t is Element of T : not p is_a_proper_prefix_of t  }  \/  {  (p ^ s) where s is Element of T1 : s = s  }  as non empty set ;
A2: for x being set st x in  {  t where t is Element of T : not p is_a_proper_prefix_of t  }  holds
( x is FinSequence of NAT & x in NAT * & x in T )
proof
let x be set ; ::_thesis: ( x in  {  t where t is Element of T : not p is_a_proper_prefix_of t  }  implies ( x is FinSequence of NAT & x in NAT * & x in T ) )
assume  x in  {  t where t is Element of T : not p is_a_proper_prefix_of t  }  ; ::_thesis: ( x is FinSequence of NAT & x in NAT * & x in T )
then A3: ex t being Element of T st
( x = t & not p is_a_proper_prefix_of t ) ;
hence  x is FinSequence of NAT ; ::_thesis: ( x in NAT * & x in T )
thus  ( x in NAT * & x in T ) by A3, FINSEQ_1:def_11; ::_thesis: verum
end;
 X is Tree-like
proof
thus  X c= NAT * :: according to TREES_1:def_3 ::_thesis: ( ( 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 Element of NAT st p ^ <*k*> in X & n <= k holds
p ^ <*n*> in X ) )
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in NAT * )
assume  x in X ; ::_thesis: x in NAT *
then A4: ( x in  {  t where t is Element of T : not p is_a_proper_prefix_of t  }  or x in  {  (p ^ s) where s is Element of T1 : s = s  }  ) by XBOOLE_0:def_3;
now__::_thesis:_(_x_in__{__(p_^_s)_where_s_is_Element_of_T1_:_s_=_s__}__implies_x_is_FinSequence_of_NAT_)
assume  x in  {  (p ^ s) where s is Element of T1 : s = s  }  ; ::_thesis: x is FinSequence of NAT
then  ex s being Element of T1 st
( x = p ^ s & s = s ) ;
hence  x is FinSequence of NAT ; ::_thesis: verum
end;
hence  x in NAT * by A2, A4, FINSEQ_1:def_11; ::_thesis: verum
end;
thus  for q being FinSequence of NAT st q in X holds
ProperPrefixes q c= X ::_thesis: for p being FinSequence of NAT
for k, n being Element of NAT st p ^ <*k*> in X & n <= k holds
p ^ <*n*> in X
proof
let q be FinSequence of NAT ; ::_thesis: ( q in X implies ProperPrefixes q c= X )
assume A5: q in X ; ::_thesis: ProperPrefixes q c= X
A6: now__::_thesis:_(_q_in__{__t_where_t_is_Element_of_T_:_not_p_is_a_proper_prefix_of_t__}__implies_ProperPrefixes_q_c=_X_)
assume  q in  {  t where t is Element of T : not p is_a_proper_prefix_of t  }  ; ::_thesis: ProperPrefixes q c= X
then A7: ex t being Element of T st
( q = t & not p is_a_proper_prefix_of t ) ;
then A8: ProperPrefixes q c= T by Def3;
thus  ProperPrefixes q c= X ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in ProperPrefixes q or x in X )
assume A9: x in ProperPrefixes q ; ::_thesis: x in X
then consider p1 being FinSequence such that
A10: x = p1 and
A11: p1 is_a_proper_prefix_of q by Def2;
reconsider p1 = p1 as Element of T by A8, A9, A10;
 not p is_a_proper_prefix_of p1 by A7, A11, XBOOLE_1:56;
then  x in  {  s1 where s1 is Element of T : not p is_a_proper_prefix_of s1  }  by A10;
hence  x in X by XBOOLE_0:def_3; ::_thesis: verum
end;
end;
now__::_thesis:_(_q_in__{__(p_^_s)_where_s_is_Element_of_T1_:_s_=_s__}__implies_ProperPrefixes_q_c=_X_)
assume  q in  {  (p ^ s) where s is Element of T1 : s = s  }  ; ::_thesis: ProperPrefixes q c= X
then consider s being Element of T1 such that
A12: q = p ^ s and
 s = s ;
thus  ProperPrefixes q c= X ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in ProperPrefixes q or x in X )
assume A13: x in ProperPrefixes q ; ::_thesis: x in X
then reconsider r = x as FinSequence by Th11;
 r is_a_proper_prefix_of p ^ s by A12, A13, Th12;
then  r is_a_prefix_of p ^ s by XBOOLE_0:def_8;
then consider r1 being FinSequence such that
A14: p ^ s = r ^ r1 by Th1;
A15: now__::_thesis:_(_len_p_<=_len_r_implies_r_in_X_)
assume  len p <= len r ; ::_thesis: r in X
then consider r2 being FinSequence such that
A16: p ^ r2 = r by A14, FINSEQ_1:47;
 p ^ s = p ^ (r2 ^ r1) by A14, A16, FINSEQ_1:32;
then  s = r2 ^ r1 by FINSEQ_1:33;
then A17: ( dom r2 = Seg (len r2) & s | (dom r2) = r2 ) by FINSEQ_1:21, FINSEQ_1:def_3;
then reconsider r2 = r2 as FinSequence of NAT by FINSEQ_1:18;
 r2 is_a_prefix_of s by A17, Def1;
then reconsider r2 = r2 as Element of T1 by Th20;
 r = p ^ r2 by A16;
then  r in  {  (p ^ v) where v is Element of T1 : v = v  }  ;
hence  r in X by XBOOLE_0:def_3; ::_thesis: verum
end;
now__::_thesis:_(_len_r_<=_len_p_implies_r_in_X_)
assume  len r <= len p ; ::_thesis: r in X
then  ex r2 being FinSequence st r ^ r2 = p by A14, FINSEQ_1:47;
then A18: p | (dom r) = r by FINSEQ_1:21;
A19: dom r = Seg (len r) by FINSEQ_1:def_3;
then reconsider r3 = r as FinSequence of NAT by A18, FINSEQ_1:18;
A20: r3 is_a_prefix_of p by A18, A19, Def1;
then A21: not p is_a_proper_prefix_of r3 by XBOOLE_0:def_8;
reconsider r3 = r3 as Element of T by A1, A20, Th20;
 r3 in  {  t where t is Element of T : not p is_a_proper_prefix_of t  }  by A21;
hence  r in X by XBOOLE_0:def_3; ::_thesis: verum
end;
hence  x in X by A15; ::_thesis: verum
end;
end;
hence  ProperPrefixes q c= X by A5, A6, XBOOLE_0:def_3; ::_thesis: verum
end;
let q be FinSequence of NAT ; ::_thesis: for k, n being Element of NAT st q ^ <*k*> in X & n <= k holds
q ^ <*n*> in X
let k, n be Element of NAT ; ::_thesis: ( q ^ <*k*> in X & n <= k implies q ^ <*n*> in X )
assume that
A22: q ^ <*k*> in X and
A23: n <= k ; ::_thesis: q ^ <*n*> in X
A24: now__::_thesis:_(_q_^_<*k*>_in__{__t_where_t_is_Element_of_T_:_not_p_is_a_proper_prefix_of_t__}__implies_q_^_<*n*>_in_X_)
assume  q ^ <*k*> in  {  t where t is Element of T : not p is_a_proper_prefix_of t  }  ; ::_thesis: q ^ <*n*> in X
then A25: ex s being Element of T st
( q ^ <*k*> = s & not p is_a_proper_prefix_of s ) ;
then reconsider u = q ^ <*n*> as Element of T by A23, Def3;
now__::_thesis:_not_p_is_a_proper_prefix_of_u
assume  p is_a_proper_prefix_of u ; ::_thesis: contradiction
then  p is_a_prefix_of q by Th9;
hence  contradiction by A25, Th8; ::_thesis: verum
end;
then  q ^ <*n*> in  {  t where t is Element of T : not p is_a_proper_prefix_of t  }  ;
hence  q ^ <*n*> in X by XBOOLE_0:def_3; ::_thesis: verum
end;
now__::_thesis:_(_q_^_<*k*>_in__{__(p_^_s)_where_s_is_Element_of_T1_:_s_=_s__}__implies_q_^_<*n*>_in_X_)
assume  q ^ <*k*> in  {  (p ^ s) where s is Element of T1 : s = s  }  ; ::_thesis: q ^ <*n*> in X
then consider s being Element of T1 such that
A26: q ^ <*k*> = p ^ s and
 s = s ;
A27: now__::_thesis:_(_len_q_<=_len_p_implies_q_^_<*n*>_in_X_)
assume  len q <= len p ; ::_thesis: q ^ <*n*> in X
then consider r being FinSequence such that
A28: q ^ r = p by A26, FINSEQ_1:47;
 q ^ <*k*> = q ^ (r ^ s) by A26, A28, FINSEQ_1:32;
then A29: <*k*> = r ^ s by FINSEQ_1:33;
A30: now__::_thesis:_(_r_=_<*k*>_implies_q_^_<*n*>_in__{__t_where_t_is_Element_of_T_:_not_p_is_a_proper_prefix_of_t__}__)
assume A31: r = <*k*> ; ::_thesis: q ^ <*n*> in  {  t where t is Element of T : not p is_a_proper_prefix_of t  }
then reconsider s = q ^ <*n*> as Element of T by A1, A23, A28, Def3;
now__::_thesis:_not_p_is_a_proper_prefix_of_s
assume A32: p is_a_proper_prefix_of s ; ::_thesis: contradiction
then A33: p is_a_prefix_of s by XBOOLE_0:def_8;
len p = (len q) + (len <*k*>) by A28, A31, FINSEQ_1:22
.= (len q) + 1 by FINSEQ_1:40
.= (len q) + (len <*n*>) by FINSEQ_1:40
.= len s by FINSEQ_1:22 ;
hence  contradiction by A32, A33, Th2; ::_thesis: verum
end;
hence  q ^ <*n*> in  {  t where t is Element of T : not p is_a_proper_prefix_of t  }  ; ::_thesis: verum
end;
now__::_thesis:_(_s_=_<*k*>_&_r_=_{}_implies_q_^_<*n*>_in__{__(p_^_v)_where_v_is_Element_of_T1_:_v_=_v__}__)
assume that
A34: s = <*k*> and
A35: r = {} ; ::_thesis: q ^ <*n*> in  {  (p ^ v) where v is Element of T1 : v = v  }
 ( s = {} ^ s & {} = <*> NAT ) by FINSEQ_1:34;
then  {} ^ <*n*> in T1 by A23, A34, Def3;
then reconsider t = <*n*> as Element of T1 by FINSEQ_1:34;
 q ^ <*n*> = p ^ t by A28, A35, FINSEQ_1:34;
hence  q ^ <*n*> in  {  (p ^ v) where v is Element of T1 : v = v  }  ; ::_thesis: verum
end;
hence  q ^ <*n*> in X by A29, A30, FINSEQ_1:88, XBOOLE_0:def_3; ::_thesis: verum
end;
now__::_thesis:_(_len_p_<=_len_q_implies_q_^_<*n*>_in_X_)
assume  len p <= len q ; ::_thesis: q ^ <*n*> in X
then consider r being FinSequence such that
A36: p ^ r = q by A26, FINSEQ_1:47;
 p ^ (r ^ <*k*>) = p ^ s by A26, A36, FINSEQ_1:32;
then A37: r ^ <*k*> = s by FINSEQ_1:33;
then  ( dom r = Seg (len r) & s | (dom r) = r ) by FINSEQ_1:21, FINSEQ_1:def_3;
then reconsider r = r as FinSequence of NAT by FINSEQ_1:18;
reconsider t = r ^ <*n*> as Element of T1 by A23, A37, Def3;
 q ^ <*n*> = p ^ t by A36, FINSEQ_1:32;
then  q ^ <*n*> in  {  (p ^ v) where v is Element of T1 : v = v  }  ;
hence  q ^ <*n*> in X by XBOOLE_0:def_3; ::_thesis: verum
end;
hence  q ^ <*n*> in X by A27; ::_thesis: verum
end;
hence  q ^ <*n*> in X by A22, A24, XBOOLE_0:def_3; ::_thesis: verum
end;
then reconsider X = X as Tree ;
take  X ; ::_thesis: for q being FinSequence of NAT holds
( q in X 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 ) ) )
let q be FinSequence of NAT ; ::_thesis: ( q in X 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 ) ) )
thus  ( not q in X or ( 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 ) ) ::_thesis: ( ( ( 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 ) ) implies q in X )
proof
assume A38: q in X ; ::_thesis: ( ( 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 ) )
A39: now__::_thesis:_(_not_q_in__{__t_where_t_is_Element_of_T_:_not_p_is_a_proper_prefix_of_t__}__or_(_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_)_)
assume  q in  {  t where t is Element of T : not p is_a_proper_prefix_of t  }  ; ::_thesis: ( ( 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 ) )
then  ex s being Element of T st
( q = s & not p is_a_proper_prefix_of s ) ;
hence  ( ( 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 ) ) ; ::_thesis: verum
end;
now__::_thesis:_(_q_in__{__(p_^_s)_where_s_is_Element_of_T1_:_s_=_s__}__implies_ex_r_being_FinSequence_of_NAT_st_
(_r_in_T1_&_q_=_p_^_r_)_)
assume  q in  {  (p ^ s) where s is Element of T1 : s = s  }  ; ::_thesis: ex r being FinSequence of NAT st
( r in T1 & q = p ^ r )
then  ex s being Element of T1 st
( q = p ^ s & s = s ) ;
hence  ex r being FinSequence of NAT st
( r in T1 & q = p ^ r ) ; ::_thesis: verum
end;
hence  ( ( 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 ) ) by A38, A39, XBOOLE_0:def_3; ::_thesis: verum
end;
assume A40: ( ( 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 ) ) ; ::_thesis: q in X
A41: ( q in T & not p is_a_proper_prefix_of q implies q in  {  t where t is Element of T : not p is_a_proper_prefix_of t  }  ) ;
 ( ex r being FinSequence of NAT st
( r in T1 & q = p ^ r ) implies q in  {  (p ^ v) where v is Element of T1 : v = v  }  ) ;
hence  q in X by A40, A41, XBOOLE_0:def_3; ::_thesis: verum
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
let S1, S2 be Tree; ::_thesis: ( ( for q being FinSequence of NAT holds
( q in S1 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 S2 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 ) ) ) ) implies S1 = S2 )
assume that
A42: for q being FinSequence of NAT holds
( q in S1 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 ) ) ) and
A43: for q being FinSequence of NAT holds
( q in S2 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 ) ) ) ; ::_thesis: S1 = S2
thus  S1 c= S2 :: according to XBOOLE_0:def_10 ::_thesis: S2 is_a_prefix_of S1
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in S1 or x in S2 )
assume A44: x in S1 ; ::_thesis: x in S2
then reconsider q = x as FinSequence of NAT by Th19;
 ( ( 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 ) ) by A42, A44;
hence  x in S2 by A43; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in S2 or x in S1 )
assume A45: x in S2 ; ::_thesis: x in S1
then reconsider q = x as FinSequence of NAT by Th19;
 ( ( 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 ) ) by A43, A45;
hence  x in S1 by A42; ::_thesis: verum
end;
end;

:: deftheorem Def9 defines with-replacement TREES_1:def_9_:_
 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 Th32: :: TREES_1:32
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
let p be FinSequence of NAT ; ::_thesis: 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  }
let T, T1 be Tree; ::_thesis: ( p in T implies 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  }  )
assume A1: p in T ; ::_thesis: 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  }
thus  T with-replacement (p,T1) c=  {  t where t is Element of T : not p is_a_proper_prefix_of t  }  \/  {  (p ^ s) where s is Element of T1 : s = s  }  :: according to XBOOLE_0:def_10 ::_thesis:  {  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  }  is_a_prefix_of T with-replacement (p,T1)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in T with-replacement (p,T1) or x in  {  t where t is Element of T : not p is_a_proper_prefix_of t  }  \/  {  (p ^ s) where s is Element of T1 : s = s  }  )
assume A2: x in T with-replacement (p,T1) ; ::_thesis: x in  {  t where t is Element of T : not p is_a_proper_prefix_of t  }  \/  {  (p ^ s) where s is Element of T1 : s = s  }
then reconsider q = x as FinSequence of NAT by Th19;
A3: ( ex r being FinSequence of NAT st
( r in T1 & q = p ^ r ) implies x in  {  (p ^ s) where s is Element of T1 : s = s  }  ) ;
 ( q in T & not p is_a_proper_prefix_of q implies x in  {  t where t is Element of T : not p is_a_proper_prefix_of t  }  ) ;
hence  x in  {  t where t is Element of T : not p is_a_proper_prefix_of t  }  \/  {  (p ^ s) where s is Element of T1 : s = s  }  by A1, A2, A3, Def9, XBOOLE_0:def_3; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  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  }  or x in T with-replacement (p,T1) )
assume A4: x in  {  t where t is Element of T : not p is_a_proper_prefix_of t  }  \/  {  (p ^ s) where s is Element of T1 : s = s  }  ; ::_thesis: x in T with-replacement (p,T1)
A5: now__::_thesis:_(_x_in__{__(p_^_s)_where_s_is_Element_of_T1_:_s_=_s__}__implies_x_in_T_with-replacement_(p,T1)_)
assume  x in  {  (p ^ s) where s is Element of T1 : s = s  }  ; ::_thesis: x in T with-replacement (p,T1)
then  ex s being Element of T1 st
( x = p ^ s & s = s ) ;
hence  x in T with-replacement (p,T1) by A1, Def9; ::_thesis: verum
end;
now__::_thesis:_(_x_in__{__t_where_t_is_Element_of_T_:_not_p_is_a_proper_prefix_of_t__}__implies_x_in_T_with-replacement_(p,T1)_)
assume  x in  {  t where t is Element of T : not p is_a_proper_prefix_of t  }  ; ::_thesis: x in T with-replacement (p,T1)
then  ex t being Element of T st
( x = t & not p is_a_proper_prefix_of t ) ;
hence  x in T with-replacement (p,T1) by A1, Def9; ::_thesis: verum
end;
hence  x in T with-replacement (p,T1) by A4, A5, XBOOLE_0:def_3; ::_thesis: verum
end;

theorem :: TREES_1:33
for p being FinSequence of NAT
for T, T1 being Tree st p in T holds
T1 = (T with-replacement (p,T1)) | p
proof
let p be FinSequence of NAT ; ::_thesis: for T, T1 being Tree st p in T holds
T1 = (T with-replacement (p,T1)) | p
let T, T1 be Tree; ::_thesis: ( p in T implies T1 = (T with-replacement (p,T1)) | p )
assume A1: p in T ; ::_thesis: T1 = (T with-replacement (p,T1)) | p
then A2: p in T with-replacement (p,T1) by Def9;
thus  T1 c= (T with-replacement (p,T1)) | p :: according to XBOOLE_0:def_10 ::_thesis: (T with-replacement (p,T1)) | p is_a_prefix_of T1
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in T1 or x in (T with-replacement (p,T1)) | p )
assume A3: x in T1 ; ::_thesis: x in (T with-replacement (p,T1)) | p
then reconsider q = x as FinSequence of NAT by Th19;
 p ^ q in T with-replacement (p,T1) by A1, A3, Def9;
hence  x in (T with-replacement (p,T1)) | p by A2, Def6; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (T with-replacement (p,T1)) | p or x in T1 )
assume A4: x in (T with-replacement (p,T1)) | p ; ::_thesis: x in T1
then reconsider q = x as FinSequence of NAT by Th19;
A5: p ^ q in T with-replacement (p,T1) by A2, A4, Def6;
A6: now__::_thesis:_(_p_^_q_in_T_&_not_p_is_a_proper_prefix_of_p_^_q_implies_q_in_T1_)
assume that
 p ^ q in T and
A7: not p is_a_proper_prefix_of p ^ q ; ::_thesis: q in T1
 p is_a_prefix_of p ^ q by Th1;
then p ^ q = p by A7, XBOOLE_0:def_8
.= p ^ {} by FINSEQ_1:34 ;
then  q = {} by FINSEQ_1:33;
hence  q in T1 by Th22; ::_thesis: verum
end;
 ( ex r being FinSequence of NAT st
( r in T1 & p ^ q = p ^ r ) implies q in T1 ) by FINSEQ_1:33;
hence  x in T1 by A1, A5, A6, Def9; ::_thesis: verum
end;

registration
let T be finite Tree;
let t be Element of T;
let T1 be finite Tree;
clusterT with-replacement (t,T1) ->  finite ;
coherence
 T with-replacement (t,T1) is finite
proof
A1:  {  s where s is Element of T : not t is_a_proper_prefix_of s  }  c= T
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  s where s is Element of T : not t is_a_proper_prefix_of s  }  or x in T )
assume  x in  {  s where s is Element of T : not t is_a_proper_prefix_of s  }  ; ::_thesis: x in T
then  ex s being Element of T st
( x = s & not t is_a_proper_prefix_of s ) ;
hence  x in T ; ::_thesis: verum
end;
 T1, {  (t ^ s) where s is Element of T1 : s = s  }  are_equipotent
proof
defpred S1[ set , set ] means  ex q being FinSequence of NAT st
( T = q & t = t ^ q );
A2: for x being set st x in T1 holds
ex y being set st S1[x,y]
proof
let x be set ; ::_thesis: ( x in T1 implies ex y being set st S1[x,y] )
assume  x in T1 ; ::_thesis: ex y being set st S1[x,y]
then reconsider q = x as FinSequence of NAT by Th19;
 t ^ q = t ^ q ;
hence  ex y being set st S1[x,y] ; ::_thesis: verum
end;
consider f being Function such that
A3: ( dom f = T1 & ( for x being set st x in T1 holds
S1[x,f . x] ) ) from CLASSES1:sch_1(A2);
take  f ; :: according to WELLORD2:def_4 ::_thesis: ( f is one-to-one & dom f = T1 & rng f =  {  (t ^ s) where s is Element of T1 : s = s  }  )
thus  f is one-to-one ::_thesis: ( dom f = T1 & rng f =  {  (t ^ s) where s is Element of T1 : s = s  }  )
proof
let x be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds
( not x in dom f or not b1 in dom f or not f . x = f . b1 or x = b1 )
let y be set ; ::_thesis: ( not x in dom f or not y in dom f or not f . x = f . y or x = y )
assume that
A4: ( x in dom f & y in dom f ) and
A5: f . x = f . y ; ::_thesis: x = y
 ( ex q being FinSequence of NAT st
( x = q & f . x = t ^ q ) & ex r being FinSequence of NAT st
( y = r & f . y = t ^ r ) ) by A3, A4;
hence  x = y by A5, FINSEQ_1:33; ::_thesis: verum
end;
thus  dom f = T1 by A3; ::_thesis: rng f =  {  (t ^ s) where s is Element of T1 : s = s  }
thus  rng f c=  {  (t ^ s) where s is Element of T1 : s = s  }  :: according to XBOOLE_0:def_10 ::_thesis:  {  (t ^ s) where s is Element of T1 : s = s  }  is_a_prefix_of rng f
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng f or x in  {  (t ^ s) where s is Element of T1 : s = s  }  )
assume  x in rng f ; ::_thesis: x in  {  (t ^ s) where s is Element of T1 : s = s  }
then consider y being set  such that
A6: y in dom f and
A7: x = f . y by FUNCT_1:def_3;
consider q being FinSequence of NAT  such that
A8: y = q and
A9: f . y = t ^ q by A3, A6;
reconsider q = q as Element of T1 by A3, A6, A8;
 x = t ^ q by A7, A9;
hence  x in  {  (t ^ s) where s is Element of T1 : s = s  }  ; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  (t ^ s) where s is Element of T1 : s = s  }  or x in rng f )
assume  x in  {  (t ^ s) where s is Element of T1 : s = s  }  ; ::_thesis: x in rng f
then consider s being Element of T1 such that
A10: x = t ^ s and
 s = s ;
 S1[s,f . s] by A3;
hence  x in rng f by A3, A10, FUNCT_1:def_3; ::_thesis: verum
end;
then   {  (t ^ s) where s is Element of T1 : s = s  }  is finite by CARD_1:38;
then   {  v where v is Element of T : not t is_a_proper_prefix_of v  }  \/  {  (t ^ s) where s is Element of T1 : s = s  }  is finite by A1;
hence  T with-replacement (t,T1) is finite by Th32; ::_thesis: verum
end;
end;

theorem Th34: :: TREES_1:34
for p being FinSequence holds ProperPrefixes p, dom p are_equipotent
proof
let p be FinSequence; ::_thesis: ProperPrefixes p, dom p are_equipotent
defpred S1[ set , set ] means  ex w being FinSequence st
( $1 = w & $2 = (len w) + 1 );
A1: for x being set st x in ProperPrefixes p holds
ex y being set st S1[x,y]
proof
let x be set ; ::_thesis: ( x in ProperPrefixes p implies ex y being set st S1[x,y] )
assume  x in ProperPrefixes p ; ::_thesis: ex y being set st S1[x,y]
then consider q being FinSequence such that
A2: x = q and
 q is_a_proper_prefix_of p by Def2;
reconsider y = (len q) + 1 as set ;
take  y ; ::_thesis: S1[x,y]
take  q ; ::_thesis: ( x = q & y = (len q) + 1 )
thus  ( x = q & y = (len q) + 1 ) by A2; ::_thesis: verum
end;
consider f being Function such that
A3: dom f = ProperPrefixes p and
A4: for x being set st x in ProperPrefixes p holds
S1[x,f . x] from CLASSES1:sch_1(A1);
take  f ; :: according to WELLORD2:def_4 ::_thesis: ( f is one-to-one & dom f = ProperPrefixes p & rng f = dom p )
thus  f is one-to-one ::_thesis: ( dom f = ProperPrefixes p & rng f = dom p )
proof
let x be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds
( not x in dom f or not b1 in dom f or not f . x = f . b1 or x = b1 )
let y be set ; ::_thesis: ( not x in dom f or not y in dom f or not f . x = f . y or x = y )
assume that
A5: ( x in dom f & y in dom f ) and
A6: f . x = f . y ; ::_thesis: x = y
 ( ex q being FinSequence st
( x = q & f . x = (len q) + 1 ) & ex r being FinSequence st
( y = r & f . x = (len r) + 1 ) ) by A3, A4, A5, A6;
hence  x = y by A3, A5, Th4, Th18; ::_thesis: verum
end;
thus  dom f = ProperPrefixes p by A3; ::_thesis: rng f = dom p
thus  rng f c= dom p :: according to XBOOLE_0:def_10 ::_thesis: dom p is_a_prefix_of rng f
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng f or x in dom p )
assume  x in rng f ; ::_thesis: x in dom p
then consider y being set  such that
A7: y in dom f and
A8: x = f . y by FUNCT_1:def_3;
consider q being FinSequence such that
A9: y = q and
A10: x = (len q) + 1 by A3, A4, A7, A8;
 len q < len p by A3, A7, A9, Th13;
then  ( 0 + 1 <= (len q) + 1 & (len q) + 1 <= len p ) by NAT_1:13;
then  x in Seg (len p) by A10, FINSEQ_1:1;
hence  x in dom p by FINSEQ_1:def_3; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom p or x in rng f )
assume A11: x in dom p ; ::_thesis: x in rng f
then A12: x in Seg (len p) by FINSEQ_1:def_3;
reconsider n = x as Element of NAT by A11;
A13: 1 <= n by A12, FINSEQ_1:1;
A14: n <= len p by A12, FINSEQ_1:1;
consider m being Nat such that
A15: n = 1 + m by A13, NAT_1:10;
reconsider m = m as Element of NAT by ORDINAL1:def_12;
reconsider q = p | (Seg m) as FinSequence by FINSEQ_1:15;
A16: m <= len p by A14, A15, NAT_1:13;
A17: m <> len p by A14, A15, NAT_1:13;
A18: len q = m by A16, FINSEQ_1:17;
A19: q is_a_prefix_of p by Def1;
 len q = m by A16, FINSEQ_1:17;
then  q is_a_proper_prefix_of p by A17, A19, XBOOLE_0:def_8;
then A20: q in ProperPrefixes p by Th12;
then  ex r being FinSequence st
( q = r & f . q = (len r) + 1 ) by A4;
hence  x in rng f by A3, A15, A18, A20, FUNCT_1:def_3; ::_thesis: verum
end;

registration
let p be FinSequence;
cluster ProperPrefixes p ->  finite ;
coherence
 ProperPrefixes p is finite
proof
 ProperPrefixes p, dom p are_equipotent by Th34;
hence  ProperPrefixes p is finite by CARD_1:38; ::_thesis: verum
end;
end;

theorem :: TREES_1:35
for p being FinSequence holds card (ProperPrefixes p) = len p
proof
let p be FinSequence; ::_thesis: card (ProperPrefixes p) = len p
A1: dom p = Seg (len p) by FINSEQ_1:def_3;
A2: ProperPrefixes p, dom p are_equipotent by Th34;
 card (dom p) = card (len p) by A1, FINSEQ_1:55;
hence  card (ProperPrefixes p) = len p by A2, CARD_1:5; ::_thesis: verum
end;

definition
let IT be set ;
attrIT is AntiChain_of_Prefixes-like  means :Def10: :: TREES_1:def 10
( ( 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 Def10 defines AntiChain_of_Prefixes-like TREES_1:def_10_:_
 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 for set ;
existence
 ex b1 being set st b1 is AntiChain_of_Prefixes-like
proof
take  {} ; ::_thesis: {} is AntiChain_of_Prefixes-like
thus  for x being set st x in {} holds
x is FinSequence ; :: according to TREES_1:def_10 ::_thesis: for p1, p2 being FinSequence st p1 in {} & p2 in {} & p1 <> p2 holds
not p1,p2 are_c=-comparable
let p1, p2 be FinSequence; ::_thesis: ( p1 in {} & p2 in {} & p1 <> p2 implies not p1,p2 are_c=-comparable )
thus  ( p1 in {} & p2 in {} & p1 <> p2 implies not p1,p2 are_c=-comparable ) ; ::_thesis: verum
end;
end;

definition
mode AntiChain_of_Prefixes is AntiChain_of_Prefixes-like set ;
end;

theorem Th36: :: TREES_1:36
for w being FinSequence holds {w} is AntiChain_of_Prefixes-like
proof
let w be FinSequence; ::_thesis: {w} is AntiChain_of_Prefixes-like
thus  for x being set st x in {w} holds
x is FinSequence by TARSKI:def_1; :: according to TREES_1:def_10 ::_thesis: for p1, p2 being FinSequence st p1 in {w} & p2 in {w} & p1 <> p2 holds
not p1,p2 are_c=-comparable
let p1, p2 be FinSequence; ::_thesis: ( p1 in {w} & p2 in {w} & p1 <> p2 implies not p1,p2 are_c=-comparable )
assume that
A1: p1 in {w} and
A2: p2 in {w} ; ::_thesis: ( not p1 <> p2 or not p1,p2 are_c=-comparable )
 p1 = w by A1, TARSKI:def_1;
hence  ( not p1 <> p2 or not p1,p2 are_c=-comparable ) by A2, TARSKI:def_1; ::_thesis: verum
end;

theorem Th37: :: TREES_1:37
for p1, p2 being FinSequence st not p1,p2 are_c=-comparable holds
{p1,p2} is AntiChain_of_Prefixes-like
proof
let p1, p2 be FinSequence; ::_thesis: ( not p1,p2 are_c=-comparable implies {p1,p2} is AntiChain_of_Prefixes-like )
assume A1: not p1,p2 are_c=-comparable ; ::_thesis: {p1,p2} is AntiChain_of_Prefixes-like
thus  for x being set st x in {p1,p2} holds
x is FinSequence by TARSKI:def_2; :: according to TREES_1:def_10 ::_thesis: for p1, p2 being FinSequence st p1 in {p1,p2} & p2 in {p1,p2} & p1 <> p2 holds
not p1,p2 are_c=-comparable
let q1, q2 be FinSequence; ::_thesis: ( q1 in {p1,p2} & q2 in {p1,p2} & q1 <> q2 implies not q1,q2 are_c=-comparable )
assume that
A2: q1 in {p1,p2} and
A3: q2 in {p1,p2} ; ::_thesis: ( not q1 <> q2 or not q1,q2 are_c=-comparable )
A4: ( q1 = p1 or q1 = p2 ) by A2, TARSKI:def_2;
 ( q2 = p1 or q2 = p2 ) by A3, TARSKI:def_2;
hence  ( not q1 <> q2 or not q1,q2 are_c=-comparable ) by A1, A4; ::_thesis: verum
end;

definition
let T be Tree;
mode AntiChain_of_Prefixes of T ->  AntiChain_of_Prefixes means :Def11: :: TREES_1:def 11
it c= T;
existence
 ex b1 being AntiChain_of_Prefixes st b1 c= T
proof
set t = the Element of T;
reconsider S = { the Element of T} as AntiChain_of_Prefixes by Th36;
take  S ; ::_thesis: S c= T
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in S or x in T )
assume  x in S ; ::_thesis: x in T
then  x = the Element of T by TARSKI:def_1;
hence  x in T ; ::_thesis: verum
end;
end;

:: deftheorem Def11 defines AntiChain_of_Prefixes TREES_1:def_11_:_
 for T being Tree
for b2 being AntiChain_of_Prefixes holds
( b2 is AntiChain_of_Prefixes of T iff b2 c= T );


theorem Th38: :: TREES_1:38
for T being Tree holds
( {} is AntiChain_of_Prefixes of T & {{}} is AntiChain_of_Prefixes of T )
proof
let T be Tree; ::_thesis: ( {} is AntiChain_of_Prefixes of T & {{}} is AntiChain_of_Prefixes of T )
 {} is AntiChain_of_Prefixes-like
proof
thus  for x being set st x in {} holds
x is FinSequence ; :: according to TREES_1:def_10 ::_thesis: for p1, p2 being FinSequence st p1 in {} & p2 in {} & p1 <> p2 holds
not p1,p2 are_c=-comparable
let p1, p2 be FinSequence; ::_thesis: ( p1 in {} & p2 in {} & p1 <> p2 implies not p1,p2 are_c=-comparable )
thus  ( p1 in {} & p2 in {} & p1 <> p2 implies not p1,p2 are_c=-comparable ) ; ::_thesis: verum
end;
then reconsider S = {} as AntiChain_of_Prefixes ;
 S c= T by XBOOLE_1:2;
hence  {} is AntiChain_of_Prefixes of T by Def11; ::_thesis: {{}} is AntiChain_of_Prefixes of T
reconsider S = {{}} as AntiChain_of_Prefixes by Th36;
 S is AntiChain_of_Prefixes of T
proof
let x be set ; :: according to TARSKI:def_3,TREES_1:def_11 ::_thesis: ( not x in S or x in T )
assume  x in S ; ::_thesis: x in T
then  x = {} by TARSKI:def_1;
hence  x in T by Th22; ::_thesis: verum
end;
hence  {{}} is AntiChain_of_Prefixes of T ; ::_thesis: verum
end;

theorem :: TREES_1:39
for T being Tree
for t being Element of T holds {t} is AntiChain_of_Prefixes of T
proof
let T be Tree; ::_thesis: for t being Element of T holds {t} is AntiChain_of_Prefixes of T
let t be Element of T; ::_thesis: {t} is AntiChain_of_Prefixes of T
reconsider S = {t} as AntiChain_of_Prefixes by Th36;
 S is AntiChain_of_Prefixes of T
proof
let x be set ; :: according to TARSKI:def_3,TREES_1:def_11 ::_thesis: ( not x in S or x in T )
assume  x in S ; ::_thesis: x in T
then  x = t by TARSKI:def_1;
hence  x in T ; ::_thesis: verum
end;
hence  {t} is AntiChain_of_Prefixes of T ; ::_thesis: verum
end;

theorem :: TREES_1:40
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
let T be Tree; ::_thesis: for t1, t2 being Element of T st not t1,t2 are_c=-comparable holds
{t1,t2} is AntiChain_of_Prefixes of T
let t1, t2 be Element of T; ::_thesis: ( not t1,t2 are_c=-comparable implies {t1,t2} is AntiChain_of_Prefixes of T )
assume  not t1,t2 are_c=-comparable ; ::_thesis: {t1,t2} is AntiChain_of_Prefixes of T
then reconsider A = {t1,t2} as AntiChain_of_Prefixes by Th37;
 A is AntiChain_of_Prefixes of T
proof
let x be set ; :: according to TARSKI:def_3,TREES_1:def_11 ::_thesis: ( not x in A or x in T )
assume  x in A ; ::_thesis: x in T
then  ( x = t1 or x = t2 ) by TARSKI:def_2;
hence  x in T ; ::_thesis: verum
end;
hence  {t1,t2} is AntiChain_of_Prefixes of T ; ::_thesis: verum
end;

registration
let T be finite Tree;
cluster  ->  finite for AntiChain_of_Prefixes of T;
coherence
 for b1 being AntiChain_of_Prefixes of T holds b1 is finite
proof
let X be AntiChain_of_Prefixes of T; ::_thesis: X is finite
 X c= T by Def11;
hence  X is finite ; ::_thesis: verum
end;
end;

definition
let T be finite Tree;
func height T ->  Element of NAT  means :Def12: :: TREES_1:def 12
( 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 Element of 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
consider n being Nat such that
A1: T, Seg n are_equipotent by FINSEQ_1:56;
defpred S1[ Nat] means  for p being FinSequence of NAT st p in T holds
len p <= $1;
A2: ex n being Nat st S1[n]
proof
now__::_thesis:_for_p_being_FinSequence_of_NAT_holds_
(_not_p_in_T_or_len_p_<=_n_)
given p being FinSequence of NAT  such that A3: p in T and
A4: not len p <= n ; ::_thesis: contradiction
A5: ProperPrefixes p c= T by A3, Def3;
A6: ProperPrefixes p, dom p are_equipotent by Th34;
A7: card (ProperPrefixes p) c= card T by A5, CARD_1:11;
A8: card (ProperPrefixes p) = card (dom p) by A6, CARD_1:5;
A9: ( card T = card (Seg n) & dom p = Seg (len p) ) by A1, CARD_1:5, FINSEQ_1:def_3;
 Seg n c= Seg (len p) by A4, FINSEQ_1:5;
then A10: card (Seg n) c= card (Seg (len p)) by CARD_1:11;
 ( card (Seg n) = card n & card (Seg (len p)) = card (len p) ) by FINSEQ_1:55;
then  card n = card (len p) by A7, A8, A9, A10, XBOOLE_0:def_10;
hence  contradiction by A4, CARD_1:40; ::_thesis: verum
end;
then consider n being Nat such that
A11: S1[n] ;
reconsider n = n as Element of NAT by ORDINAL1:def_12;
take  n ; ::_thesis: S1[n]
thus  S1[n] by A11; ::_thesis: verum
end;
consider n being Nat such that
A12: S1[n] and
A13: for m being Nat st S1[m] holds
n <= m from NAT_1:sch_5(A2);
set x = the Element of T;
reconsider n = n as Element of NAT by ORDINAL1:def_12;
take  n ; ::_thesis: ( ex p being FinSequence of NAT st
( p in T & len p = n ) & ( for p being FinSequence of NAT st p in T holds
len p <= n ) )
thus  ex p being FinSequence of NAT st
( p in T & len p = n ) ::_thesis: for p being FinSequence of NAT st p in T holds
len p <= n
proof
assume A14: for p being FinSequence of NAT st p in T holds
len p <> n ; ::_thesis: contradiction
reconsider x = the Element of T as FinSequence of NAT ;
 len x <= n by A12;
then  len x < n by A14, XXREAL_0:1;
then consider k being Nat such that
A15: n = k + 1 by NAT_1:6;
reconsider k = k as Element of NAT by ORDINAL1:def_12;
 for p being FinSequence of NAT st p in T holds
len p <= k
proof
let p be FinSequence of NAT ; ::_thesis: ( p in T implies len p <= k )
assume A16: p in T ; ::_thesis: len p <= k
then  len p <= n by A12;
then  len p < k + 1 by A14, A15, A16, XXREAL_0:1;
hence  len p <= k by NAT_1:13; ::_thesis: verum
end;
then  n <= k by A13;
hence  contradiction by A15, NAT_1:13; ::_thesis: verum
end;
let p be FinSequence of NAT ; ::_thesis: ( p in T implies len p <= n )
assume  p in T ; ::_thesis: len p <= n
hence  len p <= n by A12; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Element of 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
let l1, l2 be Element of NAT ; ::_thesis: ( ex p being FinSequence of NAT st
( p in T & len p = l1 ) & ( for p being FinSequence of NAT st p in T holds
len p <= l1 ) & ex p being FinSequence of NAT st
( p in T & len p = l2 ) & ( for p being FinSequence of NAT st p in T holds
len p <= l2 ) implies l1 = l2 )
given p1 being FinSequence of NAT  such that A17: ( p1 in T & len p1 = l1 ) ; ::_thesis: ( ex p being FinSequence of NAT st
( p in T & not len p <= l1 ) or for p being FinSequence of NAT holds
( not p in T or not len p = l2 ) or ex p being FinSequence of NAT st
( p in T & not len p <= l2 ) or l1 = l2 )
assume A18: for p being FinSequence of NAT st p in T holds
len p <= l1 ; ::_thesis: ( for p being FinSequence of NAT holds
( not p in T or not len p = l2 ) or ex p being FinSequence of NAT st
( p in T & not len p <= l2 ) or l1 = l2 )
given p2 being FinSequence of NAT  such that A19: ( p2 in T & len p2 = l2 ) ; ::_thesis: ( ex p being FinSequence of NAT st
( p in T & not len p <= l2 ) or l1 = l2 )
assume  for p being FinSequence of NAT st p in T holds
len p <= l2 ; ::_thesis: l1 = l2
then A20: l1 <= l2 by A17;
 l2 <= l1 by A18, A19;
hence  l1 = l2 by A20, XXREAL_0:1; ::_thesis: verum
end;
func width T ->  Element of NAT  means :Def13: :: TREES_1:def 13
 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 Element of 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
defpred S1[ Nat] means  ex X being finite set st
( $1 = card X & X c= T & ( for p, q being FinSequence of NAT st p in X & q in X & p <> q holds
not p,q are_c=-comparable ) );
 ( 0 = card {} & ( for p, q being FinSequence of NAT st p in {} & q in {} & p <> q holds
not p,q are_c=-comparable ) ) ;
then A21: ex n being Nat st S1[n] by XBOOLE_1:2;
A22: for n being Nat st S1[n] holds
n <= card T
proof
let n be Nat; ::_thesis: ( S1[n] implies n <= card T )
given X being finite set  such that A23: ( n = card X & X c= T ) and
 for p, q being FinSequence of NAT st p in X & q in X & p <> q holds
not p,q are_c=-comparable ; ::_thesis: n <= card T
A24: ( card X c= card T & card X = card n ) by A23, CARD_1:11;
 card T = card (card T) ;
hence  n <= card T by A24, NAT_1:40; ::_thesis: verum
end;
consider n being Nat such that
A25: S1[n] and
A26: for m being Nat st S1[m] holds
m <= n from NAT_1:sch_6(A22, A21);
consider X being finite set  such that
A27: n = card X and
A28: X c= T and
A29: for p, q being FinSequence of NAT st p in X & q in X & p <> q holds
not p,q are_c=-comparable by A25;
 X is AntiChain_of_Prefixes-like
proof
thus  for x being set st x in X holds
x is FinSequence :: according to TREES_1:def_10 ::_thesis: for p1, p2 being FinSequence st p1 in X & p2 in X & p1 <> p2 holds
not p1,p2 are_c=-comparable
proof
let x be set ; ::_thesis: ( x in X implies x is FinSequence )
assume A30: x in X ; ::_thesis: x is FinSequence
 T c= NAT * by Def3;
hence  x is FinSequence by A30, A28; ::_thesis: verum
end;
let p1, p2 be FinSequence; ::_thesis: ( p1 in X & p2 in X & p1 <> p2 implies not p1,p2 are_c=-comparable )
assume A31: ( p1 in X & p2 in X ) ; ::_thesis: ( not p1 <> p2 or not p1,p2 are_c=-comparable )
then reconsider q1 = p1, q2 = p2 as Element of T by A28;
 ( p1 = q1 & p2 = q2 ) ;
hence  ( not p1 <> p2 or not p1,p2 are_c=-comparable ) by A29, A31; ::_thesis: verum
end;
then reconsider X = X as AntiChain_of_Prefixes ;
reconsider X = X as AntiChain_of_Prefixes of T by A28, Def11;
reconsider n = n as Element of NAT by ORDINAL1:def_12;
take  n ; ::_thesis: ex X being AntiChain_of_Prefixes of T st
( n = card X & ( for Y being AntiChain_of_Prefixes of T holds card Y <= card X ) )
take  X ; ::_thesis: ( n = card X & ( for Y being AntiChain_of_Prefixes of T holds card Y <= card X ) )
thus  n = card X by A27; ::_thesis: for Y being AntiChain_of_Prefixes of T holds card Y <= card X
let Y be AntiChain_of_Prefixes of T; ::_thesis: card Y <= card X
 ( Y c= T & ( for p, q being FinSequence of NAT st p in Y & q in Y & p <> q holds
not p,q are_c=-comparable ) ) by Def10, Def11;
hence  card Y <= card X by A26, A27; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Element of 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
let n1, n2 be Element of NAT ; ::_thesis: ( ex X being AntiChain_of_Prefixes of T st
( n1 = card X & ( for Y being AntiChain_of_Prefixes of T holds card Y <= card X ) ) & ex X being AntiChain_of_Prefixes of T st
( n2 = card X & ( for Y being AntiChain_of_Prefixes of T holds card Y <= card X ) ) implies n1 = n2 )
given X1 being AntiChain_of_Prefixes of T such that A32: n1 = card X1 and
A33: for Y being AntiChain_of_Prefixes of T holds card Y <= card X1 ; ::_thesis: ( for X being AntiChain_of_Prefixes of T holds
( not n2 = card X or ex Y being AntiChain_of_Prefixes of T st not card Y <= card X ) or n1 = n2 )
given X2 being AntiChain_of_Prefixes of T such that A34: n2 = card X2 and
A35: for Y being AntiChain_of_Prefixes of T holds card Y <= card X2 ; ::_thesis: n1 = n2
A36: card X1 <= card X2 by A35;
 card X2 <= card X1 by A33;
hence  n1 = n2 by A32, A34, A36, XXREAL_0:1; ::_thesis: verum
end;
end;

:: deftheorem Def12 defines height TREES_1:def_12_:_
 for T being finite Tree
for b2 being Element of 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 Def13 defines width TREES_1:def_13_:_
 for T being finite Tree
for b2 being Element of 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:41
for fT being finite Tree holds 1 <= width fT
proof
let fT be finite Tree; ::_thesis: 1 <= width fT
 ( ex X being AntiChain_of_Prefixes of fT st
( width fT = card X & ( for Y being AntiChain_of_Prefixes of fT holds card Y <= card X ) ) & {{}} is AntiChain_of_Prefixes of fT ) by Def13, Th38;
then  card {{}} <= width fT ;
hence  1 <= width fT by CARD_1:30; ::_thesis: verum
end;

theorem :: TREES_1:42
height (elementary_tree 0) = 0
proof
now__::_thesis:_(_ex_p_being_FinSequence_of_NAT_st_
(_p_in_elementary_tree_0_&_len_p_=_0_)_&_(_for_p_being_FinSequence_of_NAT_st_p_in_elementary_tree_0_holds_
len_p_<=_0_)_)
thus  ex p being FinSequence of NAT st
( p in elementary_tree 0 & len p = 0 ) ::_thesis: for p being FinSequence of NAT st p in elementary_tree 0 holds
len p <= 0
proof
take  <*> NAT ; ::_thesis: ( <*> NAT in elementary_tree 0 & len (<*> NAT) = 0 )
thus  ( <*> NAT in elementary_tree 0 & len (<*> NAT) = 0 ) by Th29, TARSKI:def_1; ::_thesis: verum
end;
let p be FinSequence of NAT ; ::_thesis: ( p in elementary_tree 0 implies len p <= 0 )
assume  p in elementary_tree 0 ; ::_thesis: len p <= 0
then  p = {} by Th29, TARSKI:def_1;
hence  len p <= 0 ; ::_thesis: verum
end;
hence  height (elementary_tree 0) = 0 by Def12; ::_thesis: verum
end;

theorem :: TREES_1:43
for fT being finite Tree st height fT = 0 holds
fT = elementary_tree 0
proof
let fT be finite Tree; ::_thesis: ( height fT = 0 implies fT = elementary_tree 0 )
assume A1: height fT = 0 ; ::_thesis: fT = elementary_tree 0
thus  fT c= elementary_tree 0 :: according to XBOOLE_0:def_10 ::_thesis: elementary_tree 0 is_a_prefix_of fT
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in fT or x in elementary_tree 0 )
assume  x in fT ; ::_thesis: x in elementary_tree 0
then reconsider t = x as Element of fT ;
 len t = 0 by A1, Def12;
then  x = {} ;
hence  x in elementary_tree 0 by Th22; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in elementary_tree 0 or x in fT )
assume  x in elementary_tree 0 ; ::_thesis: x in fT
then  x = {} by Th29, TARSKI:def_1;
hence  x in fT by Th22; ::_thesis: verum
end;

theorem :: TREES_1:44
for n being Element of NAT holds height (elementary_tree (n + 1)) = 1
proof
let n be Element of NAT ; ::_thesis: height (elementary_tree (n + 1)) = 1
set T = elementary_tree (n + 1);
now__::_thesis:_(_ex_p_being_FinSequence_of_NAT_st_
(_p_in_elementary_tree_(n_+_1)_&_len_p_=_1_)_&_(_for_p_being_FinSequence_of_NAT_st_p_in_elementary_tree_(n_+_1)_holds_
len_p_<=_1_)_)
thus  ex p being FinSequence of NAT st
( p in elementary_tree (n + 1) & len p = 1 ) ::_thesis: for p being FinSequence of NAT st p in elementary_tree (n + 1) holds
len p <= 1
proof
take p = <*0*>; ::_thesis: ( p in elementary_tree (n + 1) & len p = 1 )
thus  p in elementary_tree (n + 1) by Th28; ::_thesis: len p = 1
thus  len p = 1 by FINSEQ_1:40; ::_thesis: verum
end;
let p be FinSequence of NAT ; ::_thesis: ( p in elementary_tree (n + 1) implies len p <= 1 )
assume A1: p in elementary_tree (n + 1) ; ::_thesis: len p <= 1
A2: ( p in {{}} implies p = {} ) by TARSKI:def_1;
now__::_thesis:_(_p_in__{__<*k*>_where_k_is_Element_of_NAT_:_k_<_n_+_1__}__implies_len_p_=_1_)
assume  p in  {  <*k*> where k is Element of NAT : k < n + 1  }  ; ::_thesis: len p = 1
then  ex k being Element of NAT st
( p = <*k*> & k < n + 1 ) ;
hence  len p = 1 by FINSEQ_1:40; ::_thesis: verum
end;
hence  len p <= 1 by A1, A2, XBOOLE_0:def_3; ::_thesis: verum
end;
hence  height (elementary_tree (n + 1)) = 1 by Def12; ::_thesis: verum
end;

theorem :: TREES_1:45
width (elementary_tree 0) = 1
proof
set T = elementary_tree 0;
now__::_thesis:_ex_X_being_AntiChain_of_Prefixes_of_elementary_tree_0_st_
(_1_=_card_X_&_(_for_Y_being_AntiChain_of_Prefixes_of_elementary_tree_0_holds_card_Y_<=_card_X_)_)
reconsider X = {{}} as AntiChain_of_Prefixes of elementary_tree 0 by Th38;
take X = X; ::_thesis: ( 1 = card X & ( for Y being AntiChain_of_Prefixes of elementary_tree 0 holds card Y <= card X ) )
thus  1 = card X by CARD_1:30; ::_thesis: for Y being AntiChain_of_Prefixes of elementary_tree 0 holds card Y <= card X
let Y be AntiChain_of_Prefixes of elementary_tree 0; ::_thesis: card Y <= card X
 Y c= X by Def11, Th29;
hence  card Y <= card X by NAT_1:43; ::_thesis: verum
end;
hence  width (elementary_tree 0) = 1 by Def13; ::_thesis: verum
end;

theorem :: TREES_1:46
for n being Element of NAT holds width (elementary_tree (n + 1)) = n + 1
proof
let n be Element of NAT ; ::_thesis: width (elementary_tree (n + 1)) = n + 1
set T = elementary_tree (n + 1);
now__::_thesis:_ex_X_being_AntiChain_of_Prefixes_of_elementary_tree_(n_+_1)_st_
(_n_+_1_=_card_X_&_(_for_Y_being_AntiChain_of_Prefixes_of_elementary_tree_(n_+_1)_holds_card_Y_<=_card_X_)_)
  {  <*k*> where k is Element of NAT : k < n + 1  }  is AntiChain_of_Prefixes-like
proof
thus  for x being set st x in  {  <*k*> where k is Element of NAT : k < n + 1  }  holds
x is FinSequence :: according to TREES_1:def_10 ::_thesis: for p1, p2 being FinSequence st p1 in  {  <*k*> where k is Element of NAT : k < n + 1  }  & p2 in  {  <*k*> where k is Element of NAT : k < n + 1  }  & p1 <> p2 holds
not p1,p2 are_c=-comparable
proof
let x be set ; ::_thesis: ( x in  {  <*k*> where k is Element of NAT : k < n + 1  }  implies x is FinSequence )
assume  x in  {  <*k*> where k is Element of NAT : k < n + 1  }  ; ::_thesis: x is FinSequence
then  ex k being Element of NAT st
( x = <*k*> & k < n + 1 ) ;
hence  x is FinSequence ; ::_thesis: verum
end;
let p1, p2 be FinSequence; ::_thesis: ( p1 in  {  <*k*> where k is Element of NAT : k < n + 1  }  & p2 in  {  <*k*> where k is Element of NAT : k < n + 1  }  & p1 <> p2 implies not p1,p2 are_c=-comparable )
assume  ( p1 in  {  <*k*> where k is Element of NAT : k < n + 1  }  & p2 in  {  <*m*> where m is Element of NAT : m < n + 1  }  ) ; ::_thesis: ( not p1 <> p2 or not p1,p2 are_c=-comparable )
then  ( ex k being Element of NAT st
( p1 = <*k*> & k < n + 1 ) & ex m being Element of NAT st
( p2 = <*m*> & m < n + 1 ) ) ;
hence  ( not p1 <> p2 or not p1,p2 are_c=-comparable ) by Th5; ::_thesis: verum
end;
then reconsider X =  {  <*k*> where k is Element of NAT : k < n + 1  }  as AntiChain_of_Prefixes ;
 X c= elementary_tree (n + 1) by XBOOLE_1:7;
then reconsider X = X as AntiChain_of_Prefixes of elementary_tree (n + 1) by Def11;
take X = X; ::_thesis: ( n + 1 = card X & ( for Y being AntiChain_of_Prefixes of elementary_tree (n + 1) holds card Y <= card X ) )
 X, Seg (n + 1) are_equipotent
proof
defpred S1[ set , set ] means  ex n being Element of NAT st
( $1 = <*n*> & $2 = n + 1 );
A1: for x, y, z being set st x in X & S1[x,y] & S1[x,z] holds
y = z
proof
let x, y, z be set ; ::_thesis: ( x in X & S1[x,y] & S1[x,z] implies y = z )
assume  x in X ; ::_thesis: ( not S1[x,y] or not S1[x,z] or y = z )
given n1 being Element of NAT  such that A2: ( x = <*n1*> & y = n1 + 1 ) ; ::_thesis: ( not S1[x,z] or y = z )
given n2 being Element of NAT  such that A3: ( x = <*n2*> & z = n2 + 1 ) ; ::_thesis: y = z
 <*n1*> . 1 = n1 by FINSEQ_1:def_8;
hence  y = z by A2, A3, FINSEQ_1:def_8; ::_thesis: verum
end;
A4: for x being set st x in X holds
ex y being set st S1[x,y]
proof
let x be set ; ::_thesis: ( x in X implies ex y being set st S1[x,y] )
assume  x in X ; ::_thesis: ex y being set st S1[x,y]
then consider k being Element of NAT  such that
A5: x = <*k*> and
 k < n + 1 ;
reconsider y = k + 1 as set ;
take  y ; ::_thesis: S1[x,y]
thus  S1[x,y] by A5; ::_thesis: verum
end;
consider f being Function such that
A6: ( dom f = X & ( for x being set st x in X holds
S1[x,f . x] ) ) from CLASSES1:sch_1(A4);
take  f ; :: according to WELLORD2:def_4 ::_thesis: ( f is one-to-one & dom f = X & rng f = Seg (n + 1) )
thus  f is one-to-one ::_thesis: ( dom f = X & rng f = Seg (n + 1) )
proof
let x be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds
( not x in dom f or not b1 in dom f or not f . x = f . b1 or x = b1 )
let y be set ; ::_thesis: ( not x in dom f or not y in dom f or not f . x = f . y or x = y )
assume that
A7: ( x in dom f & y in dom f ) and
A8: f . x = f . y ; ::_thesis: x = y
 ( ex k1 being Element of NAT st
( x = <*k1*> & f . x = k1 + 1 ) & ex k2 being Element of NAT st
( y = <*k2*> & f . y = k2 + 1 ) ) by A6, A7;
hence  x = y by A8; ::_thesis: verum
end;
thus  dom f = X by A6; ::_thesis: rng f = Seg (n + 1)
thus  rng f c= Seg (n + 1) :: according to XBOOLE_0:def_10 ::_thesis: Seg (n + 1) is_a_prefix_of rng f
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng f or x in Seg (n + 1) )
assume  x in rng f ; ::_thesis: x in Seg (n + 1)
then consider y being set  such that
A9: y in dom f and
A10: x = f . y by FUNCT_1:def_3;
consider k being Element of NAT  such that
A11: y = <*k*> and
A12: x = k + 1 by A6, A9, A10;
consider m being Element of NAT  such that
A13: ( y = <*m*> & m < n + 1 ) by A6, A9;
 ( <*k*> . 1 = k & <*m*> . 1 = m ) by FINSEQ_1:def_8;
then  ( 0 + 1 <= k + 1 & k + 1 <= n + 1 ) by A11, A13, NAT_1:13;
hence  x in Seg (n + 1) by A12, FINSEQ_1:1; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Seg (n + 1) or x in rng f )
assume A14: x in Seg (n + 1) ; ::_thesis: x in rng f
then reconsider k = x as Element of NAT ;
A15: 1 <= k by A14, FINSEQ_1:1;
A16: k <= n + 1 by A14, FINSEQ_1:1;
consider m being Nat such that
A17: k = 1 + m by A15, NAT_1:10;
reconsider m = m as Element of NAT by ORDINAL1:def_12;
 m < n + 1 by A16, A17, NAT_1:13;
then A18: <*m*> in X ;
then  S1[<*m*>,f . <*m*>] by A6;
then  x = f . <*m*> by A1, A17, A18;
hence  x in rng f by A6, A18, FUNCT_1:def_3; ::_thesis: verum
end;
then A19: card (Seg (n + 1)) = card X by CARD_1:5;
hence  n + 1 = card X by FINSEQ_1:57; ::_thesis: for Y being AntiChain_of_Prefixes of elementary_tree (n + 1) holds card Y <= card X
let Y be AntiChain_of_Prefixes of elementary_tree (n + 1); ::_thesis: card Y <= card X
A20: Y c= elementary_tree (n + 1) by Def11;
A21: ( {} in Y implies Y = {{}} )
proof
assume that
A22: {} in Y and
A23: Y <> {{}} ; ::_thesis: contradiction
consider x being set  such that
A24: ( ( x in Y & not x in {{}} ) or ( x in {{}} & not x in Y ) ) by A23, TARSKI:1;
A25: {} <> x by A22, A24, TARSKI:def_1;
reconsider x = x as FinSequence of NAT by A20, A24, Th19;
 {} is_a_prefix_of x by XBOOLE_1:2;
then  {} ,x are_c=-comparable by XBOOLE_0:def_9;
hence  contradiction by A22, A24, A25, Def10, TARSKI:def_1; ::_thesis: verum
end;
A26: ( card {{}} = 1 & 1 <= 1 + n ) by CARD_1:30, NAT_1:11;
now__::_thesis:_(_not_{}_in_Y_implies_card_Y_<=_card_X_)
assume A27: not {} in Y ; ::_thesis: card Y <= card X
 Y c= X
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Y or x in X )
assume A28: x in Y ; ::_thesis: x in X
then  ( x in  {  <*k*> where k is Element of NAT : k < n + 1  }  or x in {{}} ) by A20, XBOOLE_0:def_3;
hence  x in X by A27, A28, TARSKI:def_1; ::_thesis: verum
end;
hence  card Y <= card X by NAT_1:43; ::_thesis: verum
end;
hence  card Y <= card X by A19, A21, A26, FINSEQ_1:57; ::_thesis: verum
end;
hence  width (elementary_tree (n + 1)) = n + 1 by Def13; ::_thesis: verum
end;

theorem :: TREES_1:47
for fT being finite Tree
for t being Element of fT holds height (fT | t) <= height fT
proof
let fT be finite Tree; ::_thesis: for t being Element of fT holds height (fT | t) <= height fT
let t be Element of fT; ::_thesis: height (fT | t) <= height fT
consider p being FinSequence of NAT  such that
A1: p in fT | t and
A2: len p = height (fT | t) by Def12;
 t ^ p in fT by A1, Def6;
then A3: len (t ^ p) <= height fT by Def12;
 ( len (t ^ p) = (len t) + (len p) & len p <= (len p) + (len t) ) by FINSEQ_1:22, NAT_1:11;
hence  height (fT | t) <= height fT by A2, A3, XXREAL_0:2; ::_thesis: verum
end;

theorem Th48: :: TREES_1:48
for fT being finite Tree
for t being Element of fT st t <> {} holds
height (fT | t) < height fT
proof
let fT be finite Tree; ::_thesis: for t being Element of fT st t <> {} holds
height (fT | t) < height fT
let t be Element of fT; ::_thesis: ( t <> {} implies height (fT | t) < height fT )
assume  t <> {} ; ::_thesis: height (fT | t) < height fT
then A1: 0 + 1 <= len t by NAT_1:13;
consider p being FinSequence of NAT  such that
A2: p in fT | t and
A3: len p = height (fT | t) by Def12;
 t ^ p in fT by A2, Def6;
then A4: len (t ^ p) <= height fT by Def12;
 ( len (t ^ p) = (len t) + (len p) & (len p) + 1 <= (len t) + (len p) ) by A1, FINSEQ_1:22, XREAL_1:7;
then  (height (fT | t)) + 1 <= height fT by A3, A4, XXREAL_0:2;
hence  height (fT | t) < height fT by NAT_1:13; ::_thesis: verum
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 Element of NAT st <*n*> in fT holds
P1[fT | <*n*>] ) holds
P1[fT]
proof
defpred S1[ set ] means  for fT being finite Tree st height fT = $1 holds
P1[fT];
A2: for n being Nat st ( for k being Nat st k < n holds
S1[k] ) holds
S1[n]
proof
let n be Nat; ::_thesis: ( ( for k being Nat st k < n holds
S1[k] ) implies S1[n] )
assume A3: for k being Nat st k < n holds
for fT being finite Tree st height fT = k holds
P1[fT] ; ::_thesis: S1[n]
let fT be finite Tree; ::_thesis: ( height fT = n implies P1[fT] )
assume A4: height fT = n ; ::_thesis: P1[fT]
now__::_thesis:_for_k_being_Element_of_NAT_st_<*k*>_in_fT_holds_
P1[fT_|_<*k*>]
let k be Element of NAT ; ::_thesis: ( <*k*> in fT implies P1[fT | <*k*>] )
assume  <*k*> in fT ; ::_thesis: P1[fT | <*k*>]
then reconsider k9 = <*k*> as Element of fT ;
 height (fT | k9) < height fT by Th48;
hence  P1[fT | <*k*>] by A3, A4; ::_thesis: verum
end;
hence  P1[fT] by A1; ::_thesis: verum
end;
A5: for n being Nat holds S1[n] from NAT_1:sch_4(A2);
let fT be finite Tree; ::_thesis: P1[fT]
 height fT = height fT ;
hence  P1[fT] by A5; ::_thesis: verum
end;

begin


theorem :: TREES_1:49
for w, t, s being FinSequence st w ^ t is_a_proper_prefix_of w ^ s holds
t is_a_proper_prefix_of s
proof
let w, t, s be FinSequence; ::_thesis: ( w ^ t is_a_proper_prefix_of w ^ s implies t is_a_proper_prefix_of s )
assume A1: w ^ t is_a_proper_prefix_of w ^ s ; ::_thesis: t is_a_proper_prefix_of s
then  w ^ t is_a_prefix_of w ^ s by XBOOLE_0:def_8;
then consider a being FinSequence such that
A2: w ^ s = (w ^ t) ^ a by Th1;
 (w ^ t) ^ a = w ^ (t ^ a) by FINSEQ_1:32;
then  s = t ^ a by A2, FINSEQ_1:33;
then  t is_a_prefix_of s by Th1;
hence  t is_a_proper_prefix_of s by A1, XBOOLE_0:def_8; ::_thesis: verum
end;

theorem :: TREES_1:50
for n, m being Element of NAT
for s being FinSequence st n <> m holds
not <*n*> is_a_prefix_of <*m*> ^ s
proof
let n, m be Element of NAT ; ::_thesis: for s being FinSequence st n <> m holds
not <*n*> is_a_prefix_of <*m*> ^ s
let s be FinSequence; ::_thesis: ( n <> m implies not <*n*> is_a_prefix_of <*m*> ^ s )
assume A1: n <> m ; ::_thesis: not <*n*> is_a_prefix_of <*m*> ^ s
assume  <*n*> is_a_prefix_of <*m*> ^ s ; ::_thesis: contradiction
then A2: ex a being FinSequence st <*m*> ^ s = <*n*> ^ a by Th1;
m = (<*m*> ^ s) . 1 by FINSEQ_1:41
.= n by A2, FINSEQ_1:41 ;
hence  contradiction by A1; ::_thesis: verum
end;

theorem :: TREES_1:51
elementary_tree 1 = {{},<*0*>}
proof
now__::_thesis:_for_x_being_set_holds_
(_(_not_x_in_{{},<*0*>}_or_x_in__{__<*n*>_where_n_is_Element_of_NAT_:_n_<_1__}__or_x_in_{{}}_)_&_(_(_x_in__{__<*n*>_where_n_is_Element_of_NAT_:_n_<_1__}__or_x_in_{{}}_)_implies_x_in_{{},<*0*>}_)_)
let x be set ; ::_thesis: ( ( not x in {{},<*0*>} or x in  {  <*n*> where n is Element of NAT : n < 1  }  or x in {{}} ) & ( ( x in  {  <*n*> where n is Element of NAT : n < 1  }  or x in {{}} ) implies x in {{},<*0*>} ) )
thus  ( not x in {{},<*0*>} or x in  {  <*n*> where n is Element of NAT : n < 1  }  or x in {{}} ) ::_thesis: ( ( x in  {  <*n*> where n is Element of NAT : n < 1  }  or x in {{}} ) implies x in {{},<*0*>} )
proof
assume  x in {{},<*0*>} ; ::_thesis: ( x in  {  <*n*> where n is Element of NAT : n < 1  }  or x in {{}} )
then  ( x = {} or x = <*0*> ) by TARSKI:def_2;
hence  ( x in  {  <*n*> where n is Element of NAT : n < 1  }  or x in {{}} ) by TARSKI:def_1; ::_thesis: verum
end;
assume A1: ( x in  {  <*n*> where n is Element of NAT : n < 1  }  or x in {{}} ) ; ::_thesis: x in {{},<*0*>}
now__::_thesis:_x_in_{{},<*0*>}
percases ( x in  {  <*n*> where n is Element of NAT : n < 1  }  or x in {{}} ) by A1;
suppose x in  {  <*n*> where n is Element of NAT : n < 1  }  ; ::_thesis: x in {{},<*0*>}
then consider n being Element of NAT  such that
A2: x = <*n*> and
A3: n < 1 ;
 n = 0 by A3, NAT_1:25;
hence  x in {{},<*0*>} by A2, TARSKI:def_2; ::_thesis: verum
end;
suppose x in {{}} ; ::_thesis: x in {{},<*0*>}
then  x = {} by TARSKI:def_1;
hence  x in {{},<*0*>} by TARSKI:def_2; ::_thesis: verum
end;
end;
end;
hence  x in {{},<*0*>} ; ::_thesis: verum
end;
hence  elementary_tree 1 = {{},<*0*>} by XBOOLE_0:def_3; ::_thesis: verum
end;

theorem :: TREES_1:52
for n, m being Element of NAT holds not <*n*> is_a_proper_prefix_of <*m*>
proof
let n, m be Element of NAT ; ::_thesis: not <*n*> is_a_proper_prefix_of <*m*>
assume A1: <*n*> is_a_proper_prefix_of <*m*> ; ::_thesis: contradiction
then  <*n*> is_a_prefix_of <*m*> by XBOOLE_0:def_8;
hence  contradiction by A1, Th3; ::_thesis: verum
end;

theorem :: TREES_1:53
elementary_tree 2 = {{},<*0*>,<*1*>}
proof
now__::_thesis:_for_x_being_set_holds_
(_(_not_x_in_{{},<*0*>,<*1*>}_or_x_in__{__<*n*>_where_n_is_Element_of_NAT_:_n_<_2__}__or_x_in_{{}}_)_&_(_(_x_in__{__<*n*>_where_n_is_Element_of_NAT_:_n_<_2__}__or_x_in_{{}}_)_implies_x_in_{{},<*0*>,<*1*>}_)_)
let x be set ; ::_thesis: ( ( not x in {{},<*0*>,<*1*>} or x in  {  <*n*> where n is Element of NAT : n < 2  }  or x in {{}} ) & ( ( x in  {  <*n*> where n is Element of NAT : n < 2  }  or x in {{}} ) implies x in {{},<*0*>,<*1*>} ) )
thus  ( not x in {{},<*0*>,<*1*>} or x in  {  <*n*> where n is Element of NAT : n < 2  }  or x in {{}} ) ::_thesis: ( ( x in  {  <*n*> where n is Element of NAT : n < 2  }  or x in {{}} ) implies x in {{},<*0*>,<*1*>} )
proof
assume  x in {{},<*0*>,<*1*>} ; ::_thesis: ( x in  {  <*n*> where n is Element of NAT : n < 2  }  or x in {{}} )
then  ( x = {} or x = <*0*> or x = <*1*> ) by ENUMSET1:def_1;
hence  ( x in  {  <*n*> where n is Element of NAT : n < 2  }  or x in {{}} ) by TARSKI:def_1; ::_thesis: verum
end;
assume A1: ( x in  {  <*n*> where n is Element of NAT : n < 2  }  or x in {{}} ) ; ::_thesis: x in {{},<*0*>,<*1*>}
now__::_thesis:_x_in_{{},<*0*>,<*1*>}
percases ( x in  {  <*n*> where n is Element of NAT : n < 2  }  or x in {{}} ) by A1;
suppose x in  {  <*n*> where n is Element of NAT : n < 2  }  ; ::_thesis: x in {{},<*0*>,<*1*>}
then consider n being Element of NAT  such that
A2: x = <*n*> and
A3: n < 2 ;
 ( n = 0 or n = 1 ) by A3, NAT_1:26;
hence  x in {{},<*0*>,<*1*>} by A2, ENUMSET1:def_1; ::_thesis: verum
end;
suppose x in {{}} ; ::_thesis: x in {{},<*0*>,<*1*>}
then  x = {} by TARSKI:def_1;
hence  x in {{},<*0*>,<*1*>} by ENUMSET1:def_1; ::_thesis: verum
end;
end;
end;
hence  x in {{},<*0*>,<*1*>} ; ::_thesis: verum
end;
hence  elementary_tree 2 = {{},<*0*>,<*1*>} by XBOOLE_0:def_3; ::_thesis: verum
end;

theorem :: TREES_1:54
for T being Tree
for t being Element of T holds
( t in Leaves T iff not t ^ <*0*> in T )
proof
let T be Tree; ::_thesis: for t being Element of T holds
( t in Leaves T iff not t ^ <*0*> in T )
let t be Element of T; ::_thesis: ( t in Leaves T iff not t ^ <*0*> in T )
hereby  ::_thesis: ( not t ^ <*0*> in T implies t in Leaves T )
assume A1: t in Leaves T ; ::_thesis: not t ^ <*0*> in T
 t is_a_proper_prefix_of t ^ <*0*> by Th7;
hence  not t ^ <*0*> in T by A1, Def5; ::_thesis: verum
end;
assume that
A2: not t ^ <*0*> in T and
A3: not t in Leaves T ; ::_thesis: contradiction
consider q being FinSequence of NAT  such that
A4: q in T and
A5: t is_a_proper_prefix_of q by A3, Def5;
 t is_a_prefix_of q by A5, XBOOLE_0:def_8;
then consider r being FinSequence such that
A6: q = t ^ r by Th1;
reconsider r = r as FinSequence of NAT by A6, FINSEQ_1:36;
 len q = (len t) + (len r) by A6, FINSEQ_1:22;
then  len r <> 0 by A5, Th6;
then  r <> {} ;
then consider p being FinSequence of NAT , x being Element of NAT  such that
A7: r = <*x*> ^ p by FINSEQ_2:130;
reconsider x = x as Element of NAT ;
 q = (t ^ <*x*>) ^ p by A6, A7, FINSEQ_1:32;
then  t ^ <*x*> in T by A4, Th21;
hence  contradiction by A2, Def3; ::_thesis: verum
end;

theorem :: TREES_1:55
for T being Tree
for t being Element of T holds
( t in Leaves T iff for n being Element of NAT holds not t ^ <*n*> in T )
proof
let T be Tree; ::_thesis: for t being Element of T holds
( t in Leaves T iff for n being Element of NAT holds not t ^ <*n*> in T )
let t be Element of T; ::_thesis: ( t in Leaves T iff for n being Element of NAT holds not t ^ <*n*> in T )
hereby  ::_thesis: ( ( for n being Element of NAT holds not t ^ <*n*> in T ) implies t in Leaves T )
assume A1: t in Leaves T ; ::_thesis: for n being Element of NAT holds not t ^ <*n*> in T
given n being Element of NAT  such that A2: t ^ <*n*> in T ; ::_thesis: contradiction
A3: not t is_a_proper_prefix_of t ^ <*n*> by A1, A2, Def5;
 t is_a_prefix_of t ^ <*n*> by Th1;
then A4: t = t ^ <*n*> by A3, XBOOLE_0:def_8;
 t = t ^ {} by FINSEQ_1:34;
hence  contradiction by A4, FINSEQ_1:33; ::_thesis: verum
end;
assume that
A5: for n being Element of NAT holds not t ^ <*n*> in T and
A6: not t in Leaves T ; ::_thesis: contradiction
consider q being FinSequence of NAT  such that
A7: q in T and
A8: t is_a_proper_prefix_of q by A6, Def5;
 t is_a_prefix_of q by A8, XBOOLE_0:def_8;
then consider r being FinSequence such that
A9: q = t ^ r by Th1;
reconsider r = r as FinSequence of NAT by A9, FINSEQ_1:36;
 len q = (len t) + (len r) by A9, FINSEQ_1:22;
then  len r <> 0 by A8, Th6;
then  r <> {} ;
then consider p being FinSequence of NAT , x being Element of NAT  such that
A10: r = <*x*> ^ p by FINSEQ_2:130;
reconsider x = x as Element of NAT ;
 q = (t ^ <*x*>) ^ p by A9, A10, FINSEQ_1:32;
hence  contradiction by A5, A7, Th21; ::_thesis: verum
end;

definition
func TrivialInfiniteTree  ->  set  equals :: TREES_1:def 14
 {  (k |-> 0) where k is Element of NAT : verum  }  ;
coherence
  {  (k |-> 0) where k is Element of NAT : verum  }  is set ;
end;

:: deftheorem  defines TrivialInfiniteTree TREES_1:def_14_:_
 TrivialInfiniteTree =  {  (k |-> 0) where k is Element of NAT : verum  }  ;

registration
cluster TrivialInfiniteTree  ->  non empty Tree-like ;
coherence
 ( not TrivialInfiniteTree is empty & TrivialInfiniteTree is Tree-like )
proof
set X = TrivialInfiniteTree ;
 0 |-> 0 in TrivialInfiniteTree ;
hence  not TrivialInfiniteTree is empty ; ::_thesis: TrivialInfiniteTree is Tree-like
thus  TrivialInfiniteTree c= NAT * :: according to TREES_1:def_3 ::_thesis: ( ( for p being FinSequence of NAT st p in TrivialInfiniteTree holds
ProperPrefixes p c= TrivialInfiniteTree ) & ( for p being FinSequence of NAT
for k, n being Element of NAT st p ^ <*k*> in TrivialInfiniteTree & n <= k holds
p ^ <*n*> in TrivialInfiniteTree ) )
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in TrivialInfiniteTree or x in NAT * )
assume  x in TrivialInfiniteTree ; ::_thesis: x in NAT *
then  ex k being Element of NAT st x = k |-> 0 ;
hence  x in NAT * by FINSEQ_1:def_11; ::_thesis: verum
end;
thus  for p being FinSequence of NAT st p in TrivialInfiniteTree holds
ProperPrefixes p c= TrivialInfiniteTree ::_thesis: for p being FinSequence of NAT
for k, n being Element of NAT st p ^ <*k*> in TrivialInfiniteTree & n <= k holds
p ^ <*n*> in TrivialInfiniteTree
proof
let p be FinSequence of NAT ; ::_thesis: ( p in TrivialInfiniteTree implies ProperPrefixes p c= TrivialInfiniteTree )
assume  p in TrivialInfiniteTree ; ::_thesis: ProperPrefixes p c= TrivialInfiniteTree
then consider m being Element of NAT  such that
A1: p = m |-> 0 ;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in ProperPrefixes p or x in TrivialInfiniteTree )
assume A2: x in ProperPrefixes p ; ::_thesis: x in TrivialInfiniteTree
then reconsider x = x as FinSequence by Th11;
A3: for k being Nat st 1 <= k & k <= len x holds
x . k = ((len x) |-> 0) . k
proof
 x is_a_proper_prefix_of p by A2, Th12;
then A4: x c= p by XBOOLE_0:def_8;
let k be Nat; ::_thesis: ( 1 <= k & k <= len x implies x . k = ((len x) |-> 0) . k )
assume  ( 1 <= k & k <= len x ) ; ::_thesis: x . k = ((len x) |-> 0) . k
then A5: k in dom x by FINSEQ_3:25;
thus ((len x) |-> 0) . k = 0
.= p . k by A1
.= x . k by A5, A4, GRFUNC_1:2 ; ::_thesis: verum
end;
 len x = len ((len x) |-> 0) by CARD_1:def_7;
then  x = (len x) |-> 0 by A3, FINSEQ_1:14;
hence  x in TrivialInfiniteTree ; ::_thesis: verum
end;
let p be FinSequence of NAT ; ::_thesis: for k, n being Element of NAT st p ^ <*k*> in TrivialInfiniteTree & n <= k holds
p ^ <*n*> in TrivialInfiniteTree
let m, n be Element of NAT ; ::_thesis: ( p ^ <*m*> in TrivialInfiniteTree & n <= m implies p ^ <*n*> in TrivialInfiniteTree )
assume  p ^ <*m*> in TrivialInfiniteTree ; ::_thesis: ( not n <= m or p ^ <*n*> in TrivialInfiniteTree )
then consider k being Element of NAT  such that
A7: p ^ <*m*> = k |-> 0 ;
assume A8: n <= m ; ::_thesis: p ^ <*n*> in TrivialInfiniteTree
 len (p ^ <*m*>) = (len p) + 1 by FINSEQ_2:16;
then  (p ^ <*m*>) . (len (p ^ <*m*>)) = m by FINSEQ_1:42;
then A11: m = 0 by A7;
A12: for z being Nat st 1 <= z & z <= len (p ^ <*n*>) holds
((len (p ^ <*n*>)) |-> 0) . z = (p ^ <*n*>) . z
proof
let z be Nat; ::_thesis: ( 1 <= z & z <= len (p ^ <*n*>) implies ((len (p ^ <*n*>)) |-> 0) . z = (p ^ <*n*>) . z )
assume  ( 1 <= z & z <= len (p ^ <*n*>) ) ; ::_thesis: ((len (p ^ <*n*>)) |-> 0) . z = (p ^ <*n*>) . z
thus ((len (p ^ <*n*>)) |-> 0) . z = 0
.= (p ^ <*m*>) . z by A7
.= (p ^ <*n*>) . z by A8, A11 ; ::_thesis: verum
end;
 len (p ^ <*n*>) = len ((len (p ^ <*n*>)) |-> 0) by CARD_1:def_7;
then  (len (p ^ <*n*>)) |-> 0 = p ^ <*n*> by A12, FINSEQ_1:14;
hence  p ^ <*n*> in TrivialInfiniteTree ; ::_thesis: verum
end;
end;

theorem Th56: :: TREES_1:56
NAT , TrivialInfiniteTree are_equipotent
proof
defpred S1[ Element of NAT , set ] means $2 = $1 |-> 0;
A1: for x being Element of NAT ex y being Element of TrivialInfiniteTree st S1[x,y]
proof
let x be Element of NAT ; ::_thesis: ex y being Element of TrivialInfiniteTree st S1[x,y]
 x |-> 0 in TrivialInfiniteTree ;
then reconsider y = x |-> 0 as Element of TrivialInfiniteTree ;
take  y ; ::_thesis: S1[x,y]
thus  S1[x,y] ; ::_thesis: verum
end;
consider f being Function of NAT,TrivialInfiniteTree such that
A2: for x being Element of NAT holds S1[x,f . x] from FUNCT_2:sch_3(A1);
take  f ; :: according to WELLORD2:def_4 ::_thesis: ( f is one-to-one & dom f = NAT & rng f = TrivialInfiniteTree )
thus  f is one-to-one ::_thesis: ( dom f = NAT & rng f = TrivialInfiniteTree )
proof
let x, y be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not x in dom f or not y in dom f or not f . x = f . y or x = y )
assume A3: ( x in dom f & y in dom f ) ; ::_thesis: ( not f . x = f . y or x = y )
assume A4: f . x = f . y ; ::_thesis: x = y
reconsider x = x, y = y as Element of NAT by A3, FUNCT_2:def_1;
 ( S1[x,f . x] & S1[y,f . y] ) by A2;
hence  x = y by A4, FINSEQ_2:143; ::_thesis: verum
end;
thus A5: dom f = NAT by FUNCT_2:def_1; ::_thesis: rng f = TrivialInfiniteTree
thus  rng f c= TrivialInfiniteTree by RELAT_1:def_19; :: according to XBOOLE_0:def_10 ::_thesis: TrivialInfiniteTree is_a_prefix_of rng f
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in TrivialInfiniteTree or a in rng f )
assume  a in TrivialInfiniteTree ; ::_thesis: a in rng f
then consider k being Element of NAT  such that
A6: a = k |-> 0 ;
 f . k = a by A2, A6;
hence  a in rng f by A5, FUNCT_1:def_3; ::_thesis: verum
end;

registration
cluster TrivialInfiniteTree  ->  infinite ;
coherence
 not TrivialInfiniteTree is finite by Th56, CARD_1:38;
end;