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

not p is_a_proper_prefix_of t } ;

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

A4: 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 ;

A5: 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 )

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 )

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

A52: ( 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 :: thesis: for x being object st x in P9 holds

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
P c= { t where t is Element of T : for p being FinSequence of NAT st p in P holds 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 }

let x be object ; :: 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 A2: 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 10;

reconsider x9 = x9 as Element of T by A2;

not p is_a_proper_prefix_of t } ; :: thesis: verum

end;not p is_a_proper_prefix_of t } )

assume A2: 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 10;

reconsider x9 = x9 as Element of T by A2;

now :: thesis: for p being FinSequence of NAT st p in P holds

not p is_a_proper_prefix_of x9

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 x9

let p be FinSequence of NAT ; :: thesis: ( p in P implies not b_{1} is_a_proper_prefix_of x9 )

assume A3: p in P ; :: thesis: not b_{1} is_a_proper_prefix_of x9

end;assume A3: p in P ; :: thesis: not b

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

end;

suppose
p <> x9
; :: thesis: not b_{1} is_a_proper_prefix_of x9

then
not p,x9 are_c=-comparable
by A2, A3, TREES_1:def 10;

hence not p is_a_proper_prefix_of x9 ; :: thesis: verum

end;hence not p is_a_proper_prefix_of x9 ; :: thesis: verum

not p is_a_proper_prefix_of t } ; :: thesis: verum

not p is_a_proper_prefix_of t } ;

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

A4: 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 ;

A5: 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

X is Tree-like
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 A6: 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 A6, FINSEQ_1:def 11; :: thesis: verum

end;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 A6: 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 A6, FINSEQ_1:def 11; :: thesis: verum

proof

then reconsider X = X as Tree ;
thus
X c= NAT *
:: according to TREES_1:def 3 :: thesis: ( ( for b_{1} being FinSequence of NAT holds

( not b_{1} in X or ProperPrefixes b_{1} c= X ) ) & ( for b_{1} being FinSequence of NAT

for b_{2}, b_{3} being set holds

( not b_{1} ^ <*b_{2}*> in X or not b_{3} <= b_{2} or b_{1} ^ <*b_{3}*> in X ) ) )

ProperPrefixes q c= X :: thesis: for b_{1} being FinSequence of NAT

for b_{2}, b_{3} being set holds

( not b_{1} ^ <*b_{2}*> in X or not b_{3} <= b_{2} or b_{1} ^ <*b_{3}*> in X )_{1}, b_{2} being set holds

( not q ^ <*b_{1}*> in X or not b_{2} <= b_{1} or q ^ <*b_{2}*> in X )

let k, n be Nat; :: thesis: ( not q ^ <*k*> in X or not n <= k or q ^ <*n*> in X )

assume that

A28: q ^ <*k*> in X and

A29: n <= k ; :: thesis: q ^ <*n*> in X

end;( not b

for b

( not b

proof

thus
for q being FinSequence of NAT st q in X holds
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in NAT * )

assume x in X ; :: thesis: x in NAT *

then A7: ( 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 A4, XBOOLE_0:def 3;

end;assume x in X ; :: thesis: x in NAT *

then A7: ( 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 A4, XBOOLE_0:def 3;

now :: thesis: ( x in { (p ^ s) where p is Element of T, s is Element of T1 : p in P } implies x is FinSequence of NAT )

hence
x in NAT *
by A5, A7, FINSEQ_1:def 11; :: thesis: verumassume
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;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

ProperPrefixes q c= X :: thesis: for b

for b

( not b

proof

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

assume A8: q in X ; :: thesis: ProperPrefixes q c= X

end;assume A8: q in X ; :: thesis: ProperPrefixes q c= X

A9: now :: thesis: ( 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 } implies ProperPrefixes q c= X )

not p is_a_proper_prefix_of t } implies ProperPrefixes q c= X )

assume A10:
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 A11: ProperPrefixes q c= T by TREES_1:def 3;

thus ProperPrefixes q c= X :: thesis: verum

end;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 A11: ProperPrefixes q c= T by TREES_1:def 3;

thus ProperPrefixes q c= X :: thesis: verum

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in ProperPrefixes q or x in X )

assume A12: x in ProperPrefixes q ; :: thesis: x in X

then consider p1 being FinSequence such that

A13: x = p1 and

A14: p1 is_a_proper_prefix_of q by TREES_1:def 2;

reconsider p1 = p1 as Element of T by A11, A12, A13;

for p being FinSequence of NAT st p in P holds

not p is_a_proper_prefix_of p1

not p is_a_proper_prefix_of s1 } by A13;

hence x in X by XBOOLE_0:def 3; :: thesis: verum

end;assume A12: x in ProperPrefixes q ; :: thesis: x in X

then consider p1 being FinSequence such that

A13: x = p1 and

A14: p1 is_a_proper_prefix_of q by TREES_1:def 2;

reconsider p1 = p1 as Element of T by A11, A12, A13;

for p being FinSequence of NAT st p in P holds

not p is_a_proper_prefix_of p1

proof

then
x in { s1 where s1 is Element of T : for p being FinSequence of NAT st p in P holds
let p be FinSequence of NAT ; :: thesis: ( p in P implies not p is_a_proper_prefix_of p1 )

assume A15: 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 A10;

hence not p is_a_proper_prefix_of p1 by A14, A15, XBOOLE_1:56; :: thesis: verum

end;assume A15: 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 A10;

hence not p is_a_proper_prefix_of p1 by A14, A15, XBOOLE_1:56; :: thesis: verum

not p is_a_proper_prefix_of s1 } by A13;

hence x in X by XBOOLE_0:def 3; :: thesis: verum

now :: thesis: ( q in Z implies ProperPrefixes q c= X )

hence
ProperPrefixes q c= X
by A8, A9, XBOOLE_0:def 3; :: thesis: verumassume
q in Z
; :: thesis: ProperPrefixes q c= X

then consider p being Element of T, s being Element of T1 such that

A16: q = p ^ s and

A17: p in P by A4;

thus ProperPrefixes q c= X :: thesis: verum

end;then consider p being Element of T, s being Element of T1 such that

A16: q = p ^ s and

A17: p in P by A4;

thus ProperPrefixes q c= X :: thesis: verum

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in ProperPrefixes q or x in X )

assume A18: x in ProperPrefixes q ; :: thesis: x in X

then reconsider r = x as FinSequence by TREES_1:11;

r is_a_proper_prefix_of p ^ s by A16, A18, TREES_1:12;

then r is_a_prefix_of p ^ s ;

then consider r1 being FinSequence such that

A19: p ^ s = r ^ r1 by TREES_1:1;

end;assume A18: x in ProperPrefixes q ; :: thesis: x in X

then reconsider r = x as FinSequence by TREES_1:11;

r is_a_proper_prefix_of p ^ s by A16, A18, TREES_1:12;

then r is_a_prefix_of p ^ s ;

then consider r1 being FinSequence such that

A19: p ^ s = r ^ r1 by TREES_1:1;

A20: 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

A21: p ^ r2 = r by A19, FINSEQ_1:47;

p ^ s = p ^ (r2 ^ r1) by A19, A21, FINSEQ_1:32;

then s = r2 ^ r1 by FINSEQ_1:33;

then s | (dom r2) = r2 by FINSEQ_1:21;

then A22: s | (Seg (len r2)) = r2 by FINSEQ_1:def 3;

then reconsider r2 = r2 as FinSequence of NAT by FINSEQ_1:18;

r2 is_a_prefix_of s by A22;

then reconsider r2 = r2 as Element of T1 by TREES_1:20;

r = p ^ r2 by A21;

then r in { (w ^ v) where w is Element of T, v is Element of T1 : w in P } by A17;

hence r in X by A4, XBOOLE_0:def 3; :: thesis: verum

end;then consider r2 being FinSequence such that

A21: p ^ r2 = r by A19, FINSEQ_1:47;

p ^ s = p ^ (r2 ^ r1) by A19, A21, FINSEQ_1:32;

then s = r2 ^ r1 by FINSEQ_1:33;

then s | (dom r2) = r2 by FINSEQ_1:21;

then A22: s | (Seg (len r2)) = r2 by FINSEQ_1:def 3;

then reconsider r2 = r2 as FinSequence of NAT by FINSEQ_1:18;

r2 is_a_prefix_of s by A22;

then reconsider r2 = r2 as Element of T1 by TREES_1:20;

r = p ^ r2 by A21;

then r in { (w ^ v) where w is Element of T, v is Element of T1 : w in P } by A17;

hence r in X by A4, XBOOLE_0:def 3; :: thesis: verum

now :: thesis: ( len r <= len p implies r in X )

hence
x in X
by A20; :: thesis: verumassume
len r <= len p
; :: thesis: r in X

then ex r2 being FinSequence st r ^ r2 = p by A19, FINSEQ_1:47;

then p | (dom r) = r by FINSEQ_1:21;

then A23: p | (Seg (len r)) = r by FINSEQ_1:def 3;

then reconsider r3 = r as FinSequence of NAT by FINSEQ_1:18;

A24: r3 is_a_prefix_of p by A23;

then reconsider r3 = r3 as Element of T by TREES_1:20;

for p9 being FinSequence of NAT st p9 in P holds

not p9 is_a_proper_prefix_of r3

not p9 is_a_proper_prefix_of t } ;

hence r in X by XBOOLE_0:def 3; :: thesis: verum

end;then ex r2 being FinSequence st r ^ r2 = p by A19, FINSEQ_1:47;

then p | (dom r) = r by FINSEQ_1:21;

then A23: p | (Seg (len r)) = r by FINSEQ_1:def 3;

then reconsider r3 = r as FinSequence of NAT by FINSEQ_1:18;

A24: r3 is_a_prefix_of p by A23;

then reconsider r3 = r3 as Element of T by TREES_1:20;

for p9 being FinSequence of NAT st p9 in P holds

not p9 is_a_proper_prefix_of r3

proof

then
r3 in { t where t is Element of T : for p9 being FinSequence of NAT st p9 in P holds
let p9 be FinSequence of NAT ; :: thesis: ( p9 in P implies not p9 is_a_proper_prefix_of r3 )

assume A25: p9 in P ; :: thesis: not p9 is_a_proper_prefix_of r3

assume A26: p9 is_a_proper_prefix_of r3 ; :: thesis: contradiction

then p9 is_a_prefix_of r3 ;

then p9 is_a_prefix_of p by A24;

then A27: p,p9 are_c=-comparable ;

end;assume A25: p9 in P ; :: thesis: not p9 is_a_proper_prefix_of r3

assume A26: p9 is_a_proper_prefix_of r3 ; :: thesis: contradiction

then p9 is_a_prefix_of r3 ;

then p9 is_a_prefix_of p by A24;

then A27: p,p9 are_c=-comparable ;

not p9 is_a_proper_prefix_of t } ;

hence r in X by XBOOLE_0:def 3; :: thesis: verum

( not q ^ <*b

let k, n be Nat; :: thesis: ( not q ^ <*k*> in X or not n <= k or q ^ <*n*> in X )

assume that

A28: q ^ <*k*> in X and

A29: n <= k ; :: thesis: q ^ <*n*> in X

A30: now :: thesis: ( 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 } implies q ^ <*n*> in X )

not p is_a_proper_prefix_of t } implies q ^ <*n*> in X )

assume A31:
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 A29, TREES_1:def 3;

not p is_a_proper_prefix_of t } ;

hence q ^ <*n*> in X by XBOOLE_0:def 3; :: thesis: verum

end;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 A29, TREES_1:def 3;

now :: thesis: for p being FinSequence of NAT st p in P holds

not p is_a_proper_prefix_of u

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 u

let p be FinSequence of NAT ; :: thesis: ( p in P implies not p is_a_proper_prefix_of u )

assume A32: p in P ; :: thesis: not p is_a_proper_prefix_of u

assume p is_a_proper_prefix_of u ; :: thesis: contradiction

then A33: p is_a_prefix_of q by TREES_1:9;

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 A31;

hence contradiction by A32, A33, TREES_1:8; :: thesis: verum

end;assume A32: p in P ; :: thesis: not p is_a_proper_prefix_of u

assume p is_a_proper_prefix_of u ; :: thesis: contradiction

then A33: p is_a_prefix_of q by TREES_1:9;

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 A31;

hence contradiction by A32, A33, TREES_1:8; :: thesis: verum

not p is_a_proper_prefix_of t } ;

hence q ^ <*n*> in X by XBOOLE_0:def 3; :: thesis: verum

now :: thesis: ( q ^ <*k*> in Z implies q ^ <*n*> in X )

hence
q ^ <*n*> in X
by A28, A30, XBOOLE_0:def 3; :: thesis: verumassume
q ^ <*k*> in Z
; :: thesis: q ^ <*n*> in X

then consider p being Element of T, s being Element of T1 such that

A34: q ^ <*k*> = p ^ s and

A35: p in P by A4;

end;then consider p being Element of T, s being Element of T1 such that

A34: q ^ <*k*> = p ^ s and

A35: p in P by A4;

A36: 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

A37: q ^ r = p by A34, FINSEQ_1:47;

q ^ <*k*> = q ^ (r ^ s) by A34, A37, FINSEQ_1:32;

then A38: <*k*> = r ^ s by FINSEQ_1:33;

end;then consider r being FinSequence such that

A37: q ^ r = p by A34, FINSEQ_1:47;

q ^ <*k*> = q ^ (r ^ s) by A34, A37, FINSEQ_1:32;

then A38: <*k*> = r ^ s by FINSEQ_1:33;

A39: now :: thesis: ( r = <*k*> implies 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 } )

not p is_a_proper_prefix_of t } )

assume A40:
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 A29, A37, TREES_1:def 3;

not p is_a_proper_prefix_of t } ; :: thesis: verum

end;not p is_a_proper_prefix_of t }

then reconsider s9 = q ^ <*n*> as Element of T by A29, A37, TREES_1:def 3;

now :: thesis: for p9 being FinSequence of NAT st p9 in P holds

not p9 is_a_proper_prefix_of s9

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

let p9 be FinSequence of NAT ; :: thesis: ( p9 in P implies not p9 is_a_proper_prefix_of s9 )

assume A41: p9 in P ; :: thesis: not p9 is_a_proper_prefix_of s9

assume A42: p9 is_a_proper_prefix_of s9 ; :: thesis: contradiction

A43: len p = (len q) + (len <*k*>) by A37, A40, FINSEQ_1:22

.= (len q) + 1 by FINSEQ_1:40

.= (len q) + (len <*n*>) by FINSEQ_1:40

.= len s9 by FINSEQ_1:22 ;

end;assume A41: p9 in P ; :: thesis: not p9 is_a_proper_prefix_of s9

assume A42: p9 is_a_proper_prefix_of s9 ; :: thesis: contradiction

A43: len p = (len q) + (len <*k*>) by A37, A40, FINSEQ_1:22

.= (len q) + 1 by FINSEQ_1:40

.= (len q) + (len <*n*>) by FINSEQ_1:40

.= len s9 by FINSEQ_1:22 ;

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

end;

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

( q is_a_prefix_of p & p9 is_a_prefix_of q )
by A37, A42, TREES_1:1, TREES_1:9;

then p9 is_a_prefix_of p ;

then p,p9 are_c=-comparable ;

hence contradiction by A35, A41, A44, TREES_1:def 10; :: thesis: verum

end;then p9 is_a_prefix_of p ;

then p,p9 are_c=-comparable ;

hence contradiction by A35, A41, A44, TREES_1:def 10; :: thesis: verum

not p is_a_proper_prefix_of t } ; :: thesis: verum

now :: thesis: ( s = <*k*> & r = {} implies q ^ <*n*> in Z )

hence
q ^ <*n*> in X
by A38, A39, FINSEQ_1:88, XBOOLE_0:def 3; :: thesis: verumassume that

A45: s = <*k*> and

A46: r = {} ; :: thesis: q ^ <*n*> in Z

s = (<*> NAT) ^ s by FINSEQ_1:34;

then (<*> NAT) ^ <*n*> in T1 by A29, A45, TREES_1:def 3;

then reconsider t = <*n*> as Element of T1 by FINSEQ_1:34;

q ^ <*n*> = p ^ t by A37, A46, FINSEQ_1:34;

hence q ^ <*n*> in Z by A4, A35; :: thesis: verum

end;A45: s = <*k*> and

A46: r = {} ; :: thesis: q ^ <*n*> in Z

s = (<*> NAT) ^ s by FINSEQ_1:34;

then (<*> NAT) ^ <*n*> in T1 by A29, A45, TREES_1:def 3;

then reconsider t = <*n*> as Element of T1 by FINSEQ_1:34;

q ^ <*n*> = p ^ t by A37, A46, FINSEQ_1:34;

hence q ^ <*n*> in Z by A4, A35; :: thesis: verum

now :: thesis: ( len p <= len q implies q ^ <*n*> in X )

hence
q ^ <*n*> in X
by A36; :: thesis: verumassume
len p <= len q
; :: thesis: q ^ <*n*> in X

then consider r being FinSequence such that

A47: p ^ r = q by A34, FINSEQ_1:47;

p ^ (r ^ <*k*>) = p ^ s by A34, A47, FINSEQ_1:32;

then A48: r ^ <*k*> = s by FINSEQ_1:33;

then s | (dom r) = r by FINSEQ_1:21;

then s | (Seg (len r)) = r by 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 A29, A48, TREES_1:def 3;

q ^ <*n*> = p ^ t by A47, FINSEQ_1:32;

then q ^ <*n*> in { (p9 ^ v) where p9 is Element of T, v is Element of T1 : p9 in P } by A35;

hence q ^ <*n*> in X by A4, XBOOLE_0:def 3; :: thesis: verum

end;then consider r being FinSequence such that

A47: p ^ r = q by A34, FINSEQ_1:47;

p ^ (r ^ <*k*>) = p ^ s by A34, A47, FINSEQ_1:32;

then A48: r ^ <*k*> = s by FINSEQ_1:33;

then s | (dom r) = r by FINSEQ_1:21;

then s | (Seg (len r)) = r by 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 A29, A48, TREES_1:def 3;

q ^ <*n*> = p ^ t by A47, FINSEQ_1:32;

then q ^ <*n*> in { (p9 ^ v) where p9 is Element of T, v is Element of T1 : p9 in P } by A35;

hence q ^ <*n*> in X by A4, XBOOLE_0:def 3; :: thesis: verum

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 A51:
( ( q in T & ( for p being FinSequence of NAT st p in P holds
assume A49:
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 ) )

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 A49, A50, XBOOLE_0:def 3; :: thesis: verum

end;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 ) )

A50: now :: thesis: ( not q in Y 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 ) )

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 ) )

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

now :: thesis: ( q in Z implies ex p, r being FinSequence of NAT st

( p in P & r in T1 & q = p ^ r ) )

hence
( ( q in T & ( for p being FinSequence of NAT st p in P holds ( p in P & r in T1 & q = p ^ r ) )

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 A4;

hence ex p, r being FinSequence of NAT st

( p in P & r in T1 & q = p ^ r ) ; :: thesis: verum

end;( 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 A4;

hence ex p, r being FinSequence of NAT st

( p in P & r in T1 & q = p ^ r ) ; :: thesis: verum

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 A49, A50, XBOOLE_0:def 3; :: thesis: verum

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

A52: ( 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 :: thesis: ( ex p, r being FinSequence of NAT st

( p in P & r in T1 & q = p ^ r ) implies q in Z )

hence
q in X
by A51, A52, XBOOLE_0:def 3; :: thesis: verum( p in P & r in T1 & q = p ^ r ) implies q in Z )

given p, r being FinSequence of NAT such that A53:
( p in P & r in T1 & q = p ^ r )
; :: thesis: q in Z

P c= T by TREES_1:def 11;

hence q in Z by A4, A53; :: thesis: verum

end;P c= T by TREES_1:def 11;

hence q in Z by A4, A53; :: thesis: verum