reconsider P9 = P as Subset of T by TREES_1:def 14;

now

let x be set ; :: thesis: ( x in P9 implies x in { t where t is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of t } )
assume A3: x in P9 ; :: thesis: x in { t where t is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of t }
then reconsider x9 = x as FinSequence by TREES_1:def 13;
reconsider x9 = x9 as Element of T by A3;

now

let p be FinSequence of NAT ; :: thesis: ( p in P implies not b₁ is_a_proper_prefix_of x9 )
assume A5: p in P ; :: thesis: not b₁ is_a_proper_prefix_of x9

per cases ( p <> x9 or p = x9 ) ;

suppose p <> x9 ; :: thesis: not b₁ is_a_proper_prefix_of x9

then not p,x9 are_c=-comparable by A3, A5, TREES_1:def 13;
hence not p is_a_proper_prefix_of x9 by XBOOLE_1:104; :: thesis: verum

end;

suppose p = x9 ; :: thesis: not b₁ is_a_proper_prefix_of x9

hence not p is_a_proper_prefix_of x9 ; :: thesis: verum

end;

end;

end;

hence x in { t where t is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of t } ; :: thesis: verum

end;

then P c= { t where t is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of t } by TARSKI:def 3;
then reconsider Y = { t where t is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of t } as non empty set by A1, XBOOLE_1:3;
consider Z being set such that
A10: Z = { (p ^ s) where p is Element of T, s is Element of T1 : p in P } ;
reconsider X = Y \/ Z as non empty set ;
A11: for x being set st x in { t where t is Element of T : for p being FinSequence of NAT st p in P holds
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 : for p being FinSequence of NAT st p in P holds
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 : for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of t } ; :: thesis: ( x is FinSequence of NAT & x in NAT * & x in T )
then A13: ex t being Element of T st
( x = t & ( for p being FinSequence of NAT st p in P holds
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 A13, FINSEQ_1:def 11; :: thesis: verum

end;

X is Tree-like

proof

thus X c= NAT * :: according to TREES_1:def 5 :: thesis: ( ( for b₁ being FinSequence of NAT holds
( not b₁ in X or ProperPrefixes b₁ c= X ) ) & ( for b₁ being FinSequence of NAT
for b₂, b₃ being Element of NAT holds
( not b₁ ^ <*b₂*> in X or not b₃ <= b₂ or b₁ ^ <*b₃*> 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 A16: ( x in { t where t is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of t } or x in { (p ^ s) where p is Element of T, s is Element of T1 : p in P } ) by A10, XBOOLE_0:def 3;

now

assume x in { (p ^ s) where p is Element of T, s is Element of T1 : p in P } ; :: thesis: x is FinSequence of NAT
then ex p being Element of T ex s being Element of T1 st
( x = p ^ s & p in P ) ;
hence x is FinSequence of NAT ; :: thesis: verum

end;

hence x in NAT * by A11, A16, 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 b₁ being FinSequence of NAT
for b₂, b₃ being Element of NAT holds
( not b₁ ^ <*b₂*> in X or not b₃ <= b₂ or b₁ ^ <*b₃*> in X )

proof

let q be FinSequence of NAT ; :: thesis: ( q in X implies ProperPrefixes q c= X )
assume A20: q in X ; :: thesis: ProperPrefixes q c= X

A21: now

assume A22: q in { t where t is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of t } ; :: thesis: ProperPrefixes q c= X
then ex t being Element of T st
( q = t & ( for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of t ) ) ;
then A24: ProperPrefixes q c= T by TREES_1:def 5;
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 A25: x in ProperPrefixes q ; :: thesis: x in X
then consider p1 being FinSequence such that
A26: x = p1 and
A27: p1 is_a_proper_prefix_of q by TREES_1:def 4;
reconsider p1 = p1 as Element of T by A24, A25, A26;
for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of p1

proof

let p be FinSequence of NAT ; :: thesis: ( p in P implies not p is_a_proper_prefix_of p1 )
assume A29: p in P ; :: thesis: not p is_a_proper_prefix_of p1
ex t being Element of T st
( q = t & ( for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of t ) ) by A22;
hence not p is_a_proper_prefix_of p1 by A27, A29, XBOOLE_1:56; :: thesis: verum

end;

then x in { s1 where s1 is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of s1 } by A26;
hence x in X by XBOOLE_0:def 3; :: thesis: verum

end;

end;

now

assume q in Z ; :: thesis: ProperPrefixes q c= X
then consider p being Element of T, s being Element of T1 such that
A34: q = p ^ s and
A35: p in P by A10;
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 A36: x in ProperPrefixes q ; :: thesis: x in X
then reconsider r = x as FinSequence by TREES_1:35;
r is_a_proper_prefix_of p ^ s by A34, A36, TREES_1:36;
then r is_a_prefix_of p ^ s by XBOOLE_0:def 8;
then consider r1 being FinSequence such that
A39: p ^ s = r ^ r1 by TREES_1:8;

A40: now

assume len p <= len r ; :: thesis: r in X
then consider r2 being FinSequence such that
A42: p ^ r2 = r by A39, FINSEQ_1:64;
p ^ s = p ^ (r2 ^ r1) by A39, A42, FINSEQ_1:45;
then s = r2 ^ r1 by FINSEQ_1:46;
then s | (dom r2) = r2 by FINSEQ_1:33;
then A46: s | (Seg (len r2)) = r2 by FINSEQ_1:def 3;
then reconsider r2 = r2 as FinSequence of NAT by FINSEQ_1:23;
r2 is_a_prefix_of s by A46, TREES_1:def 1;
then reconsider r2 = r2 as Element of T1 by TREES_1:45;
r = p ^ r2 by A42;
then r in { (w ^ v) where w is Element of T, v is Element of T1 : w in P } by A35;
hence r in X by A10, XBOOLE_0:def 3; :: thesis: verum

end;

now

assume len r <= len p ; :: thesis: r in X
then ex r2 being FinSequence st r ^ r2 = p by A39, FINSEQ_1:64;
then p | (dom r) = r by FINSEQ_1:33;
then A54: p | (Seg (len r)) = r by FINSEQ_1:def 3;
then reconsider r3 = r as FinSequence of NAT by FINSEQ_1:23;
A55: r3 is_a_prefix_of p by A54, TREES_1:def 1;
then reconsider r3 = r3 as Element of T by TREES_1:45;
for p9 being FinSequence of NAT st p9 in P holds
not p9 is_a_proper_prefix_of r3

proof

let p9 be FinSequence of NAT ; :: thesis: ( p9 in P implies not p9 is_a_proper_prefix_of r3 )
assume A57: p9 in P ; :: thesis: not p9 is_a_proper_prefix_of r3
assume A58: p9 is_a_proper_prefix_of r3 ; :: thesis: contradiction
then p9 is_a_prefix_of r3 by XBOOLE_0:def 8;
then p9 is_a_prefix_of p by A55, XBOOLE_1:1;
then A61: p,p9 are_c=-comparable by XBOOLE_0:def 9;

per cases ( p <> p9 or p = p9 ) ;

suppose p <> p9 ; :: thesis: contradiction

hence contradiction by A35, A57, A61, TREES_1:def 13; :: thesis: verum

end;

suppose p = p9 ; :: thesis: contradiction

hence contradiction by A55, A58, XBOOLE_0:def 8; :: thesis: verum

end;

end;

end;

then r3 in { t where t is Element of T : for p9 being FinSequence of NAT st p9 in P holds
not p9 is_a_proper_prefix_of t } ;
hence r in X by XBOOLE_0:def 3; :: thesis: verum

end;

hence x in X by A40; :: thesis: verum

end;

end;

hence ProperPrefixes q c= X by A20, A21, XBOOLE_0:def 3; :: thesis: verum

end;

let q be FinSequence of NAT ; :: thesis: for b₁, b₂ being Element of NAT holds
( not q ^ <*b₁*> in X or not b₂ <= b₁ or q ^ <*b₂*> in X )
let k, n be Element of NAT ; :: thesis: ( not q ^ <*k*> in X or not n <= k or q ^ <*n*> in X )
assume that
A65: q ^ <*k*> in X and
A66: n <= k ; :: thesis: q ^ <*n*> in X

A67: now

assume A68: q ^ <*k*> in { t where t is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of t } ; :: thesis: q ^ <*n*> in X
then ex s being Element of T st
( q ^ <*k*> = s & ( for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of s ) ) ;
then reconsider u = q ^ <*n*> as Element of T by A66, TREES_1:def 5;

now

let p be FinSequence of NAT ; :: thesis: ( p in P implies not p is_a_proper_prefix_of u )
assume A71: p in P ; :: thesis: not p is_a_proper_prefix_of u
assume p is_a_proper_prefix_of u ; :: thesis: contradiction
then A73: p is_a_prefix_of q by TREES_1:32;
ex s being Element of T st
( q ^ <*k*> = s & ( for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of s ) ) by A68;
hence contradiction by A71, A73, TREES_1:31; :: thesis: verum

end;

then q ^ <*n*> in { t where t is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of t } ;
hence q ^ <*n*> in X by XBOOLE_0:def 3; :: thesis: verum

end;

now

assume q ^ <*k*> in Z ; :: thesis: q ^ <*n*> in X
then consider p being Element of T, s being Element of T1 such that
A78: q ^ <*k*> = p ^ s and
A79: p in P by A10;

A80: now

assume len q <= len p ; :: thesis: q ^ <*n*> in X
then consider r being FinSequence such that
A82: q ^ r = p by A78, FINSEQ_1:64;
q ^ <*k*> = q ^ (r ^ s) by A78, A82, FINSEQ_1:45;
then A84: <*k*> = r ^ s by FINSEQ_1:46;

A85: now

assume A86: r = <*k*> ; :: thesis: q ^ <*n*> in { t where t is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of t }
then reconsider s9 = q ^ <*n*> as Element of T by A66, A82, TREES_1:def 5;

now

let p9 be FinSequence of NAT ; :: thesis: ( p9 in P implies not p9 is_a_proper_prefix_of s9 )
assume A88: p9 in P ; :: thesis: not p9 is_a_proper_prefix_of s9
assume A89: p9 is_a_proper_prefix_of s9 ; :: thesis: contradiction
then A90: p9 is_a_prefix_of s9 by XBOOLE_0:def 8;
A91: len p = (len q) + (len <*k*>) by A82, A86, FINSEQ_1:35
.= (len q) + 1 by FINSEQ_1:57
.= (len q) + (len <*n*>) by FINSEQ_1:57
.= len s9 by FINSEQ_1:35 ;

per cases ( p9 = p or p9 <> p ) ;

suppose p9 = p ; :: thesis: contradiction

hence contradiction by A89, A90, A91, TREES_1:15; :: thesis: verum

end;

suppose A93: p9 <> p ; :: thesis: contradiction

( q is_a_prefix_of p & p9 is_a_prefix_of q ) by A82, A89, TREES_1:8, TREES_1:32;
then p9 is_a_prefix_of p by XBOOLE_1:1;
then p,p9 are_c=-comparable by XBOOLE_0:def 9;
hence contradiction by A79, A88, A93, TREES_1:def 13; :: thesis: verum

end;

end;

end;

hence q ^ <*n*> in { t where t is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of t } ; :: thesis: verum

end;

now

assume that
A98: s = <*k*> and
A99: r = {} ; :: thesis: q ^ <*n*> in Z
s = (<*> NAT) ^ s by FINSEQ_1:47;
then (<*> NAT) ^ <*n*> in T1 by A66, A98, TREES_1:def 5;
then reconsider t = <*n*> as Element of T1 by FINSEQ_1:47;
q ^ <*n*> = p ^ t by A82, A99, FINSEQ_1:47;
hence q ^ <*n*> in Z by A10, A79; :: thesis: verum

end;

hence q ^ <*n*> in X by A84, A85, FINSEQ_1:109, XBOOLE_0:def 3; :: thesis: verum

end;

now

assume len p <= len q ; :: thesis: q ^ <*n*> in X
then consider r being FinSequence such that
A105: p ^ r = q by A78, FINSEQ_1:64;
p ^ (r ^ <*k*>) = p ^ s by A78, A105, FINSEQ_1:45;
then A107: r ^ <*k*> = s by FINSEQ_1:46;
then s | (dom r) = r by FINSEQ_1:33;
then s | (Seg (len r)) = r by FINSEQ_1:def 3;
then reconsider r = r as FinSequence of NAT by FINSEQ_1:23;
reconsider t = r ^ <*n*> as Element of T1 by A66, A107, TREES_1:def 5;
q ^ <*n*> = p ^ t by A105, FINSEQ_1:45;
then q ^ <*n*> in { (p9 ^ v) where p9 is Element of T, v is Element of T1 : p9 in P } by A79;
hence q ^ <*n*> in X by A10, XBOOLE_0:def 3; :: thesis: verum

end;

hence q ^ <*n*> in X by A80; :: thesis: verum

end;

hence q ^ <*n*> in X by A65, A67, 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 & ( for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of q ) ) or ex p, r being FinSequence of NAT st
( p in P & r in T1 & q = p ^ r ) ) )
let q be FinSequence of NAT ; :: thesis: ( q in X iff ( ( q in T & ( for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of q ) ) or ex p, r being FinSequence of NAT st
( p in P & r in T1 & q = p ^ r ) ) )
thus ( not q in X or ( q in T & ( for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of q ) ) or ex p, r being FinSequence of NAT st
( p in P & r in T1 & q = p ^ r ) ) :: thesis: ( ( ( q in T & ( for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of q ) ) or ex p, r being FinSequence of NAT st
( p in P & r in T1 & q = p ^ r ) ) implies q in X )

proof

assume A112: q in X ; :: thesis: ( ( q in T & ( for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of q ) ) or ex p, r being FinSequence of NAT st
( p in P & r in T1 & q = p ^ r ) )

A113: now

assume q in Y ; :: thesis: ( ( q in T & ( for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of q ) ) or ex p, r being FinSequence of NAT st
( p in P & r in T1 & q = p ^ r ) )
then ex s being Element of T st
( q = s & ( for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of s ) ) ;
hence ( ( q in T & ( for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of q ) ) or ex p, r being FinSequence of NAT st
( p in P & r in T1 & q = p ^ r ) ) ; :: thesis: verum

end;

now

assume q in Z ; :: thesis: ex p, r being FinSequence of NAT st
( p in P & r in T1 & q = p ^ r )
then ex p being Element of T ex s being Element of T1 st
( q = p ^ s & p in P ) by A10;
hence ex p, r being FinSequence of NAT st
( p in P & r in T1 & q = p ^ r ) ; :: thesis: verum

end;

hence ( ( q in T & ( for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of q ) ) or ex p, r being FinSequence of NAT st
( p in P & r in T1 & q = p ^ r ) ) by A112, A113, XBOOLE_0:def 3; :: thesis: verum

end;

assume A119: ( ( q in T & ( for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of q ) ) or ex p, r being FinSequence of NAT st
( p in P & r in T1 & q = p ^ r ) ) ; :: thesis: q in X
A120: ( q in T & ( for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of q ) implies q in { t where t is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of t } ) ;

now

given p, r being FinSequence of NAT such that A122: ( p in P & r in T1 & q = p ^ r ) ; :: thesis: q in Z
P c= T by TREES_1:def 14;
hence q in Z by A10, A122; :: thesis: verum

end;

hence q in X by A119, A120, XBOOLE_0:def 3; :: thesis: verum