reconsider P9 = P as Subset of T by TREES_1:def 14;
A9:
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 A2, TARSKI:def 3;
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, A9, 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 )
A14:
X is Tree-like
proof
thus
X c= NAT *
TREES_1:def 5 ( ( 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 Element of NAT holds
( not b1 ^ <*b2*> in X or not b3 <= b2 or b1 ^ <*b3*> in X ) ) )
thus
for
q being
FinSequence of
NAT st
q in X holds
ProperPrefixes q c= X
for b1 being FinSequence of NAT
for b2, b3 being Element of NAT holds
( not b1 ^ <*b2*> in X or not b3 <= b2 or b1 ^ <*b3*> in X )proof
let q be
FinSequence of
NAT ;
( q in X implies ProperPrefixes q c= X )
assume A20:
q in X
;
ProperPrefixes q c= X
A32:
now assume A33:
q in Z
;
ProperPrefixes q c= Xconsider p being
Element of
T,
s being
Element of
T1 such that A34:
q = p ^ s
and A35:
p in P
by A10, A33;
thus
ProperPrefixes q c= X
verumproof
let x be
set ;
TARSKI:def 3 ( not x in ProperPrefixes q or x in X )
assume A36:
x in ProperPrefixes q
;
x in X
reconsider r =
x as
FinSequence by A36, TREES_1:35;
A37:
r is_a_proper_prefix_of p ^ s
by A34, A36, TREES_1:36;
A38:
r is_a_prefix_of p ^ s
by A37, XBOOLE_0:def 8;
consider r1 being
FinSequence such that A39:
p ^ s = r ^ r1
by A38, TREES_1:8;
A40:
now assume A41:
len p <= len r
;
r in Xconsider r2 being
FinSequence such that A42:
p ^ r2 = r
by A39, A41, FINSEQ_1:64;
A43:
p ^ s = p ^ (r2 ^ r1)
by A39, A42, FINSEQ_1:45;
A44:
s = r2 ^ r1
by A43, FINSEQ_1:46;
A45:
s | (dom r2) = r2
by A44, FINSEQ_1:33;
A46:
s | (Seg (len r2)) = r2
by A45, FINSEQ_1:def 3;
reconsider r2 =
r2 as
FinSequence of
NAT by A46, FINSEQ_1:23;
A47:
r2 is_a_prefix_of s
by A46, TREES_1:def 1;
reconsider r2 =
r2 as
Element of
T1 by A47, TREES_1:45;
A48:
r = p ^ r2
by A42;
A49:
r in { (w ^ v) where w is Element of T, v is Element of T1 : w in P }
by A35, A48;
thus
r in X
by A10, A49, XBOOLE_0:def 3;
verum end;
thus
x in X
by A40, A50;
verum
end; end;
thus
ProperPrefixes q c= X
by A20, A21, A32, XBOOLE_0:def 3;
verum
end;
let q be
FinSequence of
NAT ;
for b1, b2 being Element of NAT holds
( not q ^ <*b1*> in X or not b2 <= b1 or q ^ <*b2*> in X )let k,
n be
Element of
NAT ;
( 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
;
q ^ <*n*> in X
A76:
now assume A77:
q ^ <*k*> in Z
;
q ^ <*n*> in Xconsider p being
Element of
T,
s being
Element of
T1 such that A78:
q ^ <*k*> = p ^ s
and A79:
p in P
by A10, A77;
A80:
now assume A81:
len q <= len p
;
q ^ <*n*> in Xconsider r being
FinSequence such that A82:
q ^ r = p
by A78, A81, FINSEQ_1:64;
A83:
q ^ <*k*> = q ^ (r ^ s)
by A78, A82, FINSEQ_1:45;
A84:
<*k*> = r ^ s
by A83, FINSEQ_1:46;
A85:
now assume A86:
r = <*k*>
;
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 } reconsider s9 =
q ^ <*n*> as
Element of
T by A66, A82, A86, TREES_1:def 5;
A87:
now let p9 be
FinSequence of
NAT ;
( p9 in P implies not p9 is_a_proper_prefix_of s9 )assume A88:
p9 in P
;
not p9 is_a_proper_prefix_of s9assume A89:
p9 is_a_proper_prefix_of s9
;
contradictionA90:
p9 is_a_prefix_of s9
by A89, 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 A93:
p9 <> p
;
contradictionA94:
(
q is_a_prefix_of p &
p9 is_a_prefix_of q )
by A82, A89, TREES_1:8, TREES_1:32;
A95:
p9 is_a_prefix_of p
by A94, XBOOLE_1:1;
A96:
p,
p9 are_c=-comparable
by A95, XBOOLE_0:def 9;
thus
contradiction
by A79, A88, A93, A96, TREES_1:def 13;
verum end; end; thus
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 }
by A87;
verum end; thus
q ^ <*n*> in X
by A84, A85, A97, FINSEQ_1:109, XBOOLE_0:def 3;
verum end; A103:
now assume A104:
len p <= len q
;
q ^ <*n*> in Xconsider r being
FinSequence such that A105:
p ^ r = q
by A78, A104, FINSEQ_1:64;
A106:
p ^ (r ^ <*k*>) = p ^ s
by A78, A105, FINSEQ_1:45;
A107:
r ^ <*k*> = s
by A106, FINSEQ_1:46;
A108:
s | (dom r) = r
by A107, FINSEQ_1:33;
A109:
s | (Seg (len r)) = r
by A108, FINSEQ_1:def 3;
reconsider r =
r as
FinSequence of
NAT by A109, FINSEQ_1:23;
reconsider t =
r ^ <*n*> as
Element of
T1 by A66, A107, TREES_1:def 5;
A110:
q ^ <*n*> = p ^ t
by A105, FINSEQ_1:45;
A111:
q ^ <*n*> in { (p9 ^ v) where p9 is Element of T, v is Element of T1 : p9 in P }
by A79, A110;
thus
q ^ <*n*> in X
by A10, A111, XBOOLE_0:def 3;
verum end; thus
q ^ <*n*> in X
by A80, A103;
verum end;
thus
q ^ <*n*> in X
by A65, A67, A76, XBOOLE_0:def 3;
verum
end;
reconsider X = X as Tree by A14;
take
X
; 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 ; ( 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 ) )
( ( ( 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 )
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 ) )
; 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 } )
;
thus
q in X
by A119, A120, A121, XBOOLE_0:def 3; verum