reconsider p9 = p as Element of T by A1;
A2:
not p is_a_proper_prefix_of p9
;
A3:
p in { t where t is Element of T : not p is_a_proper_prefix_of t }
by A2;
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 by A3;
A4:
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 )
A7:
X is Tree-like
proof
thus
X c= NAT *
TREES_1:def 5 ( ( 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 ) )
thus
for
q being
FinSequence of
NAT st
q in X holds
ProperPrefixes q 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 Xproof
let q be
FinSequence of
NAT ;
( q in X implies ProperPrefixes q c= X )
assume A13:
q in X
;
ProperPrefixes q c= X
A23:
now assume A24:
q in { (p ^ s) where s is Element of T1 : s = s }
;
ProperPrefixes q c= Xconsider s being
Element of
T1 such that A25:
q = p ^ s
and
s = s
by A24;
thus
ProperPrefixes q c= X
verumproof
let x be
set ;
TARSKI:def 3 ( not x in ProperPrefixes q or x in X )
assume A26:
x in ProperPrefixes q
;
x in X
reconsider r =
x as
FinSequence by A26, Th35;
A27:
r is_a_proper_prefix_of p ^ s
by A25, A26, Th36;
A28:
r is_a_prefix_of p ^ s
by A27, XBOOLE_0:def 8;
consider r1 being
FinSequence such that A29:
p ^ s = r ^ r1
by A28, Th8;
A30:
now assume A31:
len p <= len r
;
r in Xconsider r2 being
FinSequence such that A32:
p ^ r2 = r
by A29, A31, FINSEQ_1:64;
A33:
p ^ s = p ^ (r2 ^ r1)
by A29, A32, FINSEQ_1:45;
A34:
s = r2 ^ r1
by A33, FINSEQ_1:46;
A35:
(
dom r2 = Seg (len r2) &
s | (dom r2) = r2 )
by A34, FINSEQ_1:33, FINSEQ_1:def 3;
reconsider r2 =
r2 as
FinSequence of
NAT by A35, FINSEQ_1:23;
A36:
r2 is_a_prefix_of s
by A35, Def1;
reconsider r2 =
r2 as
Element of
T1 by A36, Th45;
A37:
r = p ^ r2
by A32;
A38:
r in { (p ^ v) where v is Element of T1 : v = v }
by A37;
thus
r in X
by A38, XBOOLE_0:def 3;
verum end;
A39:
now assume A40:
len r <= len p
;
r in XA41:
ex
r2 being
FinSequence st
r ^ r2 = p
by A29, A40, FINSEQ_1:64;
A42:
p | (dom r) = r
by A41, FINSEQ_1:33;
A43:
dom r = Seg (len r)
by FINSEQ_1:def 3;
reconsider r3 =
r as
FinSequence of
NAT by A42, A43, FINSEQ_1:23;
A44:
r3 is_a_prefix_of p
by A42, A43, Def1;
A45:
not
p is_a_proper_prefix_of r3
by A44, XBOOLE_0:def 8;
reconsider r3 =
r3 as
Element of
T by A1, A44, Th45;
A46:
r3 in { t where t is Element of T : not p is_a_proper_prefix_of t }
by A45;
thus
r in X
by A46, XBOOLE_0:def 3;
verum end;
thus
x in X
by A30, A39;
verum
end; end;
thus
ProperPrefixes q c= X
by A13, A14, A23, XBOOLE_0:def 3;
verum
end;
let q be
FinSequence of
NAT ;
for k, n being Element of NAT st q ^ <*k*> in X & n <= k holds
q ^ <*n*> in Xlet k,
n be
Element of
NAT ;
( q ^ <*k*> in X & n <= k implies q ^ <*n*> in X )
assume that A47:
q ^ <*k*> in X
and A48:
n <= k
;
q ^ <*n*> in X
A56:
now assume A57:
q ^ <*k*> in { (p ^ s) where s is Element of T1 : s = s }
;
q ^ <*n*> in Xconsider s being
Element of
T1 such that A58:
q ^ <*k*> = p ^ s
and
s = s
by A57;
A76:
now assume A77:
len p <= len q
;
q ^ <*n*> in Xconsider r being
FinSequence such that A78:
p ^ r = q
by A58, A77, FINSEQ_1:64;
A79:
p ^ (r ^ <*k*>) = p ^ s
by A58, A78, FINSEQ_1:45;
A80:
r ^ <*k*> = s
by A79, FINSEQ_1:46;
A81:
(
dom r = Seg (len r) &
s | (dom r) = r )
by A80, FINSEQ_1:33, FINSEQ_1:def 3;
reconsider r =
r as
FinSequence of
NAT by A81, FINSEQ_1:23;
reconsider t =
r ^ <*n*> as
Element of
T1 by A48, A80, Def5;
A82:
q ^ <*n*> = p ^ t
by A78, FINSEQ_1:45;
A83:
q ^ <*n*> in { (p ^ v) where v is Element of T1 : v = v }
by A82;
thus
q ^ <*n*> in X
by A83, XBOOLE_0:def 3;
verum end; thus
q ^ <*n*> in X
by A59, A76;
verum end;
thus
q ^ <*n*> in X
by A47, A49, A56, XBOOLE_0:def 3;
verum
end;
reconsider X = X as Tree by A7;
take
X
; 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 ; ( 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 ) )
( ( ( 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 )
assume A91:
( ( 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 ) )
; q in X
A92:
( 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 } )
;
A93:
( 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 } )
;
thus
q in X
by A91, A92, A93, XBOOLE_0:def 3; verum