reconsider P9 = P as Subset of T by TREES_1:def 11;
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
}
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;
now :: thesis: for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of x9
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
}
;
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 ;
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
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 ; :: thesis: verum
end;
X is Tree-like
proof
thus X c= NAT * :: according to TREES_1:def 3 :: thesis: ( ( for b1 being FinSequence of NAT holds
( not b1 in X or ProperPrefixes b1 c= X ) ) & ( for b1 being FinSequence of NAT
for b2, b3 being set holds
( not b1 ^ <*b2*> in X or not b3 <= b2 or b1 ^ <*b3*> in X ) ) )
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in NAT * )
assume x in X ; :: thesis:
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 ;
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 )
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 ; :: thesis: verum
end;
thus for q being FinSequence of NAT st q in X holds
ProperPrefixes q c= X :: thesis: for b1 being FinSequence of NAT
for b2, b3 being set holds
( not b1 ^ <*b2*> in X or not b3 <= b2 or b1 ^ <*b3*> in X )
proof
let q be FinSequence of NAT ; :: thesis: ( q in X implies ProperPrefixes q c= X )
assume A8: q in X ; :: thesis:
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 )
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:
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 ;
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 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 ; :: 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 A13;
hence x in X by XBOOLE_0:def 3; :: thesis: verum
end;
end;
now :: thesis: ( q in Z implies ProperPrefixes q c= X )
assume q in Z ; :: thesis:
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 ;
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 ;
p ^ s = p ^ (r2 ^ r1) by ;
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 ; :: 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 ;
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 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 A20; :: thesis: verum
end;
end;
hence ProperPrefixes q c= X by ; :: thesis: verum
end;
let q be FinSequence of NAT ; :: thesis: for b1, b2 being set holds
( not q ^ <*b1*> in X or not b2 <= b1 or q ^ <*b2*> 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
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 )
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 ;
now :: thesis: 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:
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;
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 :: thesis: ( q ^ <*k*> in Z implies q ^ <*n*> in X )
assume 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;
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 ;
q ^ <*k*> = q ^ (r ^ s) by ;
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
}
)
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 ;
now :: thesis: for p9 being FinSequence of NAT st p9 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) + () by
.= (len q) + 1 by FINSEQ_1:40
.= (len q) + () by FINSEQ_1:40
.= len s9 by FINSEQ_1:22 ;
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 :: thesis: ( s = <*k*> & r = {} implies q ^ <*n*> in Z )
assume that
A45: s = <*k*> and
A46: r = {} ; :: thesis: q ^ <*n*> in Z
s = () ^ s by FINSEQ_1:34;
then (<*> NAT) ^ <*n*> in T1 by ;
then reconsider t = <*n*> as Element of T1 by FINSEQ_1:34;
q ^ <*n*> = p ^ t by ;
hence q ^ <*n*> in Z by ; :: thesis: verum
end;
hence q ^ <*n*> in X by ; :: 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
A47: p ^ r = q by ;
p ^ (r ^ <*k*>) = p ^ s by ;
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 ;
q ^ <*n*> = p ^ t by ;
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 ; :: thesis: verum
end;
hence q ^ <*n*> in X by A36; :: thesis: verum
end;
hence q ^ <*n*> in X by ; :: 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 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 ) )

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 ) )
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 :: thesis: ( q in Z implies ex p, r being FinSequence of NAT st
( 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;
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 ; :: thesis: verum
end;
assume A51: ( ( 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
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 )
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 ; :: thesis: verum
end;
hence q in X by ; :: thesis: verum