defpred S1[ object ] means ( $1 = {} or ex n being Nat ex q being FinSequence st
( n < len p & q in p . (n + 1) & $1 = <*n*> ^ q ) );
consider T being set such that
A2:
for y being object holds
( y in T iff ( y in NAT * & S1[y] ) )
from XBOOLE_0:sch 1();
<*> NAT in NAT *
by FINSEQ_1:def 11;
then reconsider T = T as non empty set by A2;
A3:
rng p is constituted-Trees
by A1;
then A4:
for n being Nat st n < len p holds
p . (n + 1) is Tree
by Lm3;
T is Tree-like
proof
thus
T c= NAT *
by A2;
TREES_1:def 3 ( ( for b1 being FinSequence of NAT holds
( not b1 in T or ProperPrefixes b1 c= T ) ) & ( for b1 being FinSequence of NAT
for b2, b3 being set holds
( not b1 ^ <*b2*> in T or not b3 <= b2 or b1 ^ <*b3*> in T ) ) )
thus
for
w being
FinSequence of
NAT st
w in T holds
ProperPrefixes w c= T
for b1 being FinSequence of NAT
for b2, b3 being set holds
( not b1 ^ <*b2*> in T or not b3 <= b2 or b1 ^ <*b3*> in T )proof
let w be
FinSequence of
NAT ;
( w in T implies ProperPrefixes w c= T )
assume A5:
w in T
;
ProperPrefixes w c= T
now ( w <> {} implies ProperPrefixes w c= T )assume
w <> {}
;
ProperPrefixes w c= Tthen consider n being
Nat,
q being
FinSequence such that A6:
n < len p
and A7:
q in p . (n + 1)
and A8:
w = <*n*> ^ q
by A2, A5;
reconsider q =
q as
FinSequence of
NAT by A8, FINSEQ_1:36;
thus
ProperPrefixes w c= T
verumproof
let x be
object ;
TARSKI:def 3 ( not x in ProperPrefixes w or x in T )
assume
x in ProperPrefixes w
;
x in T
then consider r being
FinSequence such that A9:
x = r
and A10:
r is_a_proper_prefix_of w
by TREES_1:def 2;
r is_a_prefix_of w
by A10;
then consider k being
Nat such that A11:
r = w | (Seg k)
;
rng r = w .: (Seg k)
by A11, RELAT_1:115;
then reconsider r =
r as
FinSequence of
NAT by FINSEQ_1:def 4;
A12:
r in NAT *
by FINSEQ_1:def 11;
now ( r <> {} implies x in T )assume
r <> {}
;
x in Tthen consider r1 being
FinSequence of
NAT ,
i being
Element of
NAT such that A13:
r = <*i*> ^ r1
by FINSEQ_2:130;
A14:
dom <*i*> = Seg 1
by FINSEQ_1:38;
A15:
1
in Seg 1
by FINSEQ_1:2, TARSKI:def 1;
A16:
Seg 1
c= dom r
by A13, A14, FINSEQ_1:26;
A17:
r . 1
= i
by A13, FINSEQ_1:41;
A18:
w . 1
= n
by A8, FINSEQ_1:41;
A19:
r . 1
= w . 1
by A11, A15, A16, FUNCT_1:47;
then A20:
r1 is_a_proper_prefix_of q
by A8, A10, A13, A17, A18, TREES_1:49;
A21:
p . (n + 1) is
Tree
by A4, A6;
r1 is_a_prefix_of q
by A20;
then
r1 in p . (n + 1)
by A7, A21, TREES_1:20;
hence
x in T
by A2, A6, A9, A12, A13, A17, A18, A19;
verum end;
hence
x in T
by A2, A9, A12;
verum
end; end;
hence
ProperPrefixes w c= T
by TREES_1:15;
verum
end;
let w be
FinSequence of
NAT ;
for b1, b2 being set holds
( not w ^ <*b1*> in T or not b2 <= b1 or w ^ <*b2*> in T )let k,
n be
Nat;
( not w ^ <*k*> in T or not n <= k or w ^ <*n*> in T )
assume that A22:
w ^ <*k*> in T
and A23:
n <= k
;
w ^ <*n*> in T
A24:
now ( w = {} implies w ^ <*n*> in T )assume A25:
w = {}
;
w ^ <*n*> in Tthen
<*k*> in T
by A22, FINSEQ_1:34;
then consider m being
Nat,
q being
FinSequence such that A26:
m < len p
and
q in p . (m + 1)
and A27:
<*k*> = <*m*> ^ q
by A2;
A28:
<*k*> . 1
= k
by FINSEQ_1:def 8;
(<*m*> ^ q) . 1
= m
by FINSEQ_1:41;
then A29:
n < len p
by A23, A26, A27, A28, XXREAL_0:2;
then
p . (n + 1) in rng p
by Lm3;
then A30:
{} in p . (n + 1)
by A3, TREES_1:22;
A31:
<*n*> ^ {} = <*n*>
by FINSEQ_1:34;
A32:
{} ^ <*n*> = <*n*>
by FINSEQ_1:34;
reconsider n =
n as
Element of
NAT by ORDINAL1:def 12;
<*n*> in NAT *
by FINSEQ_1:def 11;
hence
w ^ <*n*> in T
by A2, A25, A29, A30, A31, A32;
verum end;
now ( w <> {} implies w ^ <*n*> in T )assume
w <> {}
;
w ^ <*n*> in Tthen consider q being
FinSequence of
NAT ,
m being
Element of
NAT such that A33:
w = <*m*> ^ q
by FINSEQ_2:130;
consider m9 being
Nat,
r being
FinSequence such that A34:
m9 < len p
and A35:
r in p . (m9 + 1)
and A36:
w ^ <*k*> = <*m9*> ^ r
by A2, A22;
reconsider n =
n as
Element of
NAT by ORDINAL1:def 12;
A37:
w ^ <*k*> = <*m*> ^ (q ^ <*k*>)
by A33, FINSEQ_1:32;
A38:
w ^ <*n*> = <*m*> ^ (q ^ <*n*>)
by A33, FINSEQ_1:32;
A39:
(w ^ <*k*>) . 1
= m
by A37, FINSEQ_1:41;
A40:
(w ^ <*k*>) . 1
= m9
by A36, FINSEQ_1:41;
A41:
<*m*> ^ (q ^ <*n*>) in NAT *
by FINSEQ_1:def 11;
A42:
r = q ^ <*k*>
by A36, A37, A39, A40, FINSEQ_1:33;
p . (m + 1) in rng p
by A34, A39, A40, Lm3;
then
q ^ <*n*> in p . (m + 1)
by A3, A23, A35, A39, A40, A42, TREES_1:def 3;
hence
w ^ <*n*> in T
by A2, A34, A38, A39, A40, A41;
verum end;
hence
w ^ <*n*> in T
by A24;
verum
end;
then reconsider T = T as Tree ;
take
T
; for x being object holds
( x in T iff ( x = {} or ex n being Nat ex q being FinSequence st
( n < len p & q in p . (n + 1) & x = <*n*> ^ q ) ) )
let x be object ; ( x in T iff ( x = {} or ex n being Nat ex q being FinSequence st
( n < len p & q in p . (n + 1) & x = <*n*> ^ q ) ) )
thus
( not x in T or x = {} or ex n being Nat ex q being FinSequence st
( n < len p & q in p . (n + 1) & x = <*n*> ^ q ) )
by A2; ( ( x = {} or ex n being Nat ex q being FinSequence st
( n < len p & q in p . (n + 1) & x = <*n*> ^ q ) ) implies x in T )
assume A43:
( x = {} or ex n being Nat ex q being FinSequence st
( n < len p & q in p . (n + 1) & x = <*n*> ^ q ) )
; x in T
{} in NAT *
by FINSEQ_1:49;
hence
x in T
by A2, A43, A44; verum