defpred S1[ Element of NAT ] means ex T being DecoratedTree of F1() st
( T . {} = F2() & ( for t being Element of dom T holds
( len t <= $1 & ( len t < $1 implies ( succ t = { (t ^ <*k*>) where k is Element of NAT : P1[k,T . t] } & ( for n being Element of NAT
for x being set st x = T . t & P1[n,x] holds
T . (t ^ <*n*>) = F3() . x,n ) ) ) ) ) );
A2:
S1[ 0 ]
proof
reconsider W =
{{} } as
Tree by TREES_1:48;
take T =
W --> F2();
( T . {} = F2() & ( for t being Element of dom T holds
( len t <= 0 & ( len t < 0 implies ( succ t = { (t ^ <*k*>) where k is Element of NAT : P1[k,T . t] } & ( for n being Element of NAT
for x being set st x = T . t & P1[n,x] holds
T . (t ^ <*n*>) = F3() . x,n ) ) ) ) ) )
{} in W
by TREES_1:47;
hence
T . {} = F2()
by FUNCOP_1:13;
for t being Element of dom T holds
( len t <= 0 & ( len t < 0 implies ( succ t = { (t ^ <*k*>) where k is Element of NAT : P1[k,T . t] } & ( for n being Element of NAT
for x being set st x = T . t & P1[n,x] holds
T . (t ^ <*n*>) = F3() . x,n ) ) ) )
let t be
Element of
dom T;
( len t <= 0 & ( len t < 0 implies ( succ t = { (t ^ <*k*>) where k is Element of NAT : P1[k,T . t] } & ( for n being Element of NAT
for x being set st x = T . t & P1[n,x] holds
T . (t ^ <*n*>) = F3() . x,n ) ) ) )
dom T = W
by FUNCOP_1:19;
then
t = {}
by TARSKI:def 1;
hence
len t <= 0
;
( len t < 0 implies ( succ t = { (t ^ <*k*>) where k is Element of NAT : P1[k,T . t] } & ( for n being Element of NAT
for x being set st x = T . t & P1[n,x] holds
T . (t ^ <*n*>) = F3() . x,n ) ) )
assume
len t < 0
;
( succ t = { (t ^ <*k*>) where k is Element of NAT : P1[k,T . t] } & ( for n being Element of NAT
for x being set st x = T . t & P1[n,x] holds
T . (t ^ <*n*>) = F3() . x,n ) )
hence
(
succ t = { (t ^ <*k*>) where k is Element of NAT : P1[k,T . t] } & ( for
n being
Element of
NAT for
x being
set st
x = T . t &
P1[
n,
x] holds
T . (t ^ <*n*>) = F3()
. x,
n ) )
;
verum
end;
A7:
for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be
Element of
NAT ;
( S1[k] implies S1[k + 1] )
given T being
DecoratedTree of
F1()
such that A8:
(
T . {} = F2() & ( for
t being
Element of
dom T holds
(
len t <= k & (
len t < k implies (
succ t = { (t ^ <*m*>) where m is Element of NAT : P1[m,T . t] } & ( for
n being
Element of
NAT for
x being
set st
x = T . t &
P1[
n,
x] holds
T . (t ^ <*n*>) = F3()
. x,
n ) ) ) ) ) )
;
S1[k + 1]
reconsider M =
{ (t ^ <*n*>) where n is Element of NAT , t is Element of dom T : P1[n,T . t] } \/ (dom T) as non
empty set ;
M is
Tree-like
proof
thus
M c= NAT *
TREES_1:def 5 ( ( for b1 being FinSequence of NAT holds
( not b1 in M or ProperPrefixes b1 c= M ) ) & ( for b1 being FinSequence of NAT
for b2, b3 being Element of NAT holds
( not b1 ^ <*b2*> in M or not b3 <= b2 or b1 ^ <*b3*> in M ) ) )
thus
for
p being
FinSequence of
NAT st
p in M holds
ProperPrefixes p c= M
for b1 being FinSequence of NAT
for b2, b3 being Element of NAT holds
( not b1 ^ <*b2*> in M or not b3 <= b2 or b1 ^ <*b3*> in M )proof
let p be
FinSequence of
NAT ;
( p in M implies ProperPrefixes p c= M )
assume
p in M
;
ProperPrefixes p c= M
then A15:
(
p in { (t ^ <*n*>) where n is Element of NAT , t is Element of dom T : P1[n,T . t] } or
p in dom T )
by XBOOLE_0:def 3;
now assume
p in { (t ^ <*n*>) where n is Element of NAT , t is Element of dom T : P1[n,T . t] }
;
ProperPrefixes p c= Mthen consider n being
Element of
NAT ,
t being
Element of
dom T such that A18:
p = t ^ <*n*>
and
P1[
n,
T . t]
;
A19:
ProperPrefixes t c= dom T
by TREES_1:def 5;
A20:
dom T c= M
by XBOOLE_1:7;
A21:
t in dom T
;
A22:
ProperPrefixes t c= M
by A19, A20, XBOOLE_1:1;
A23:
{t} c= M
by A20, A21, ZFMISC_1:37;
ProperPrefixes p = (ProperPrefixes t) \/ {t}
by A18, Th6;
hence
ProperPrefixes p c= M
by A22, A23, XBOOLE_1:8;
verum end;
then
(
ProperPrefixes p c= M or (
ProperPrefixes p c= dom T &
dom T c= M ) )
by A15, TREES_1:def 5, XBOOLE_1:7;
hence
ProperPrefixes p c= M
by XBOOLE_1:1;
verum
end;
let p be
FinSequence of
NAT ;
for b1, b2 being Element of NAT holds
( not p ^ <*b1*> in M or not b2 <= b1 or p ^ <*b2*> in M )let m,
n be
Element of
NAT ;
( not p ^ <*m*> in M or not n <= m or p ^ <*n*> in M )
assume
p ^ <*m*> in M
;
( not n <= m or p ^ <*n*> in M )
then A27:
(
p ^ <*m*> in { (t ^ <*l*>) where l is Element of NAT , t is Element of dom T : P1[l,T . t] } or
p ^ <*m*> in dom T )
by XBOOLE_0:def 3;
assume that A28:
n <= m
and A29:
not
p ^ <*n*> in M
;
contradiction
not
p ^ <*n*> in dom T
by A29, XBOOLE_0:def 3;
then consider l being
Element of
NAT ,
t being
Element of
dom T such that A31:
p ^ <*m*> = t ^ <*l*>
and A32:
P1[
l,
T . t]
by A27, A28, TREES_1:def 5;
A33:
(
len (p ^ <*m*>) = (len p) + (len <*m*>) &
len <*m*> = 1 )
by FINSEQ_1:35, FINSEQ_1:57;
A34:
(
len (t ^ <*l*>) = (len t) + (len <*l*>) &
len <*l*> = 1 )
by FINSEQ_1:35, FINSEQ_1:57;
A35:
(
(p ^ <*m*>) . ((len p) + 1) = m &
(t ^ <*l*>) . ((len t) + 1) = l )
by FINSEQ_1:59;
then A36:
p = t
by A31, A33, A34, FINSEQ_1:46;
P1[
n,
T . t]
by A1, A28, A31, A32, A33, A34, A35;
then
p ^ <*n*> in { (s ^ <*i*>) where i is Element of NAT , s is Element of dom T : P1[i,T . s] }
by A36;
hence
contradiction
by A29, XBOOLE_0:def 3;
verum
end;
then reconsider M =
M as
Tree ;
defpred S2[
FinSequence,
set ]
means ( ( $1
in dom T & $2
= T . $1 ) or ( not $1
in dom T & ex
n being
Element of
NAT ex
q being
FinSequence of
NAT st
( $1
= q ^ <*n*> & $2
= F3()
. (T . q),
n ) ) );
A39:
for
p being
FinSequence of
NAT st
p in M holds
ex
x being
set st
S2[
p,
x]
consider T9 being
DecoratedTree such that A45:
(
dom T9 = M & ( for
p being
FinSequence of
NAT st
p in M holds
S2[
p,
T9 . p] ) )
from TREES_2:sch 6(A39);
rng T9 c= F1()
proof
let x be
set ;
TARSKI:def 3 ( not x in rng T9 or x in F1() )
assume
x in rng T9
;
x in F1()
then consider y being
set such that A48:
y in dom T9
and A49:
x = T9 . y
by FUNCT_1:def 5;
reconsider y =
y as
Element of
dom T9 by A48;
now assume A54:
not
y in dom T
;
x in F1()then consider n being
Element of
NAT ,
q being
FinSequence of
NAT such that A55:
y = q ^ <*n*>
and A56:
T9 . y = F3()
. (T . q),
n
by A45;
y in { (t ^ <*l*>) where l is Element of NAT , t is Element of dom T : P1[l,T . t] }
by A45, A54, XBOOLE_0:def 3;
then consider l being
Element of
NAT ,
t being
Element of
dom T such that A58:
y = t ^ <*l*>
and
P1[
l,
T . t]
;
A59:
len <*n*> = 1
by FINSEQ_1:56;
A60:
len <*l*> = 1
by FINSEQ_1:56;
A61:
len (q ^ <*n*>) = (len q) + 1
by A59, FINSEQ_1:35;
A62:
len (t ^ <*l*>) = (len t) + 1
by A60, FINSEQ_1:35;
(
(q ^ <*n*>) . ((len q) + 1) = n &
(t ^ <*l*>) . ((len t) + 1) = l )
by FINSEQ_1:59;
then A64:
q = t
by A55, A58, A61, A62, FINSEQ_1:46;
T . t in F1()
;
then
[(T . q),n] in [:F1(),NAT :]
by A64, ZFMISC_1:106;
hence
x in F1()
by A49, A56, FUNCT_2:7;
verum end;
hence
x in F1()
by A50;
verum
end;
then reconsider T9 =
T9 as
DecoratedTree of
F1()
by RELAT_1:def 19;
take
T9
;
( T9 . {} = F2() & ( for t being Element of dom T9 holds
( len t <= k + 1 & ( len t < k + 1 implies ( succ t = { (t ^ <*k*>) where k is Element of NAT : P1[k,T9 . t] } & ( for n being Element of NAT
for x being set st x = T9 . t & P1[n,x] holds
T9 . (t ^ <*n*>) = F3() . x,n ) ) ) ) ) )
(
<*> NAT in M &
<*> NAT in dom T )
by TREES_1:47;
hence
T9 . {} = F2()
by A8, A45;
for t being Element of dom T9 holds
( len t <= k + 1 & ( len t < k + 1 implies ( succ t = { (t ^ <*k*>) where k is Element of NAT : P1[k,T9 . t] } & ( for n being Element of NAT
for x being set st x = T9 . t & P1[n,x] holds
T9 . (t ^ <*n*>) = F3() . x,n ) ) ) )
let t be
Element of
dom T9;
( len t <= k + 1 & ( len t < k + 1 implies ( succ t = { (t ^ <*k*>) where k is Element of NAT : P1[k,T9 . t] } & ( for n being Element of NAT
for x being set st x = T9 . t & P1[n,x] holds
T9 . (t ^ <*n*>) = F3() . x,n ) ) ) )
hence
len t <= k + 1
by A45, A68, XBOOLE_0:def 3;
( len t < k + 1 implies ( succ t = { (t ^ <*k*>) where k is Element of NAT : P1[k,T9 . t] } & ( for n being Element of NAT
for x being set st x = T9 . t & P1[n,x] holds
T9 . (t ^ <*n*>) = F3() . x,n ) ) )
assume A76:
len t < k + 1
;
( succ t = { (t ^ <*k*>) where k is Element of NAT : P1[k,T9 . t] } & ( for n being Element of NAT
for x being set st x = T9 . t & P1[n,x] holds
T9 . (t ^ <*n*>) = F3() . x,n ) )
A77:
now assume A78:
not
t in dom T
;
contradictionthen
t in { (s ^ <*l*>) where l is Element of NAT , s is Element of dom T : P1[l,T . s] }
by A45, XBOOLE_0:def 3;
then consider l being
Element of
NAT ,
s being
Element of
dom T such that A80:
t = s ^ <*l*>
and A81:
P1[
l,
T . s]
;
A82:
len t = (len s) + (len <*l*>)
by A80, FINSEQ_1:35;
(
len <*l*> = 1 &
len t <= k )
by A76, FINSEQ_1:56, NAT_1:13;
then
len s < k
by A82, NAT_1:13;
then
succ s = { (s ^ <*m*>) where m is Element of NAT : P1[m,T . s] }
by A8;
then
t in succ s
by A80, A81;
hence
contradiction
by A78;
verum end;
then A87:
T9 . t = T . t
by A45;
reconsider t9 =
t as
Element of
dom T by A77;
thus
succ t c= { (t ^ <*i*>) where i is Element of NAT : P1[i,T9 . t] }
XBOOLE_0:def 10 ( { (t ^ <*k*>) where k is Element of NAT : P1[k,T9 . t] } c= succ t & ( for n being Element of NAT
for x being set st x = T9 . t & P1[n,x] holds
T9 . (t ^ <*n*>) = F3() . x,n ) )proof
let x be
set ;
TARSKI:def 3 ( not x in succ t or x in { (t ^ <*i*>) where i is Element of NAT : P1[i,T9 . t] } )
assume
x in succ t
;
x in { (t ^ <*i*>) where i is Element of NAT : P1[i,T9 . t] }
then consider n being
Element of
NAT such that A89:
x = t ^ <*n*>
and A90:
t ^ <*n*> in dom T9
;
now per cases
( t ^ <*n*> in dom T or not t ^ <*n*> in dom T )
;
suppose
not
t ^ <*n*> in dom T
;
x in { (t ^ <*i*>) where i is Element of NAT : P1[i,T9 . t] } then
t ^ <*n*> in { (s ^ <*l*>) where l is Element of NAT , s is Element of dom T : P1[l,T . s] }
by A45, A90, XBOOLE_0:def 3;
then consider l being
Element of
NAT ,
s being
Element of
dom T such that A98:
t ^ <*n*> = s ^ <*l*>
and A99:
P1[
l,
T . s]
;
t = s
by A98, FINSEQ_2:20;
hence
x in { (t ^ <*i*>) where i is Element of NAT : P1[i,T9 . t] }
by A87, A89, A98, A99;
verum end;
hence
x in { (t ^ <*i*>) where i is Element of NAT : P1[i,T9 . t] }
;
verum
end;
thus A101:
{ (t ^ <*i*>) where i is Element of NAT : P1[i,T9 . t] } c= succ t
for n being Element of NAT
for x being set st x = T9 . t & P1[n,x] holds
T9 . (t ^ <*n*>) = F3() . x,n
let n be
Element of
NAT ;
for x being set st x = T9 . t & P1[n,x] holds
T9 . (t ^ <*n*>) = F3() . x,nlet x be
set ;
( x = T9 . t & P1[n,x] implies T9 . (t ^ <*n*>) = F3() . x,n )
assume that A108:
x = T9 . t
and A109:
P1[
n,
x]
;
T9 . (t ^ <*n*>) = F3() . x,n
t ^ <*n*> in { (t ^ <*i*>) where i is Element of NAT : P1[i,T9 . t] }
by A108, A109;
then A111:
t ^ <*n*> in succ t
by A101;
hence
T9 . (t ^ <*n*>) = F3()
. x,
n
;
verum
end;
A121:
for k being Element of NAT holds S1[k]
from NAT_1:sch 1(A2, A7);
defpred S2[ set , set ] means ex T being DecoratedTree of F1() ex k being Element of NAT st
( $1 = k & $2 = T & T . {} = F2() & ( for t being Element of dom T holds
( len t <= k & ( len t < k implies ( succ t = { (t ^ <*i*>) where i is Element of NAT : P1[i,T . t] } & ( for n being Element of NAT
for x being set st x = T . t & P1[n,x] holds
T . (t ^ <*n*>) = F3() . x,n ) ) ) ) ) );
A122:
for x being set st x in NAT holds
ex y being set st S2[x,y]
proof
let x be
set ;
( x in NAT implies ex y being set st S2[x,y] )
assume
x in NAT
;
ex y being set st S2[x,y]
then reconsider n =
x as
Element of
NAT ;
consider T being
DecoratedTree of
F1()
such that A124:
(
T . {} = F2() & ( for
t being
Element of
dom T holds
(
len t <= n & (
len t < n implies (
succ t = { (t ^ <*k*>) where k is Element of NAT : P1[k,T . t] } & ( for
n being
Element of
NAT for
x being
set st
x = T . t &
P1[
n,
x] holds
T . (t ^ <*n*>) = F3()
. x,
n ) ) ) ) ) )
by A121;
reconsider y =
T as
set ;
take
y
;
S2[x,y]
take
T
;
ex k being Element of NAT st
( x = k & y = T & T . {} = F2() & ( for t being Element of dom T holds
( len t <= k & ( len t < k implies ( succ t = { (t ^ <*i*>) where i is Element of NAT : P1[i,T . t] } & ( for n being Element of NAT
for x being set st x = T . t & P1[n,x] holds
T . (t ^ <*n*>) = F3() . x,n ) ) ) ) ) )
take
n
;
( x = n & y = T & T . {} = F2() & ( for t being Element of dom T holds
( len t <= n & ( len t < n implies ( succ t = { (t ^ <*i*>) where i is Element of NAT : P1[i,T . t] } & ( for n being Element of NAT
for x being set st x = T . t & P1[n,x] holds
T . (t ^ <*n*>) = F3() . x,n ) ) ) ) ) )
thus
(
x = n &
y = T &
T . {} = F2() & ( for
t being
Element of
dom T holds
(
len t <= n & (
len t < n implies (
succ t = { (t ^ <*i*>) where i is Element of NAT : P1[i,T . t] } & ( for
n being
Element of
NAT for
x being
set st
x = T . t &
P1[
n,
x] holds
T . (t ^ <*n*>) = F3()
. x,
n ) ) ) ) ) )
by A124;
verum
end;
consider f being Function such that
A125:
( dom f = NAT & ( for x being set st x in NAT holds
S2[x,f . x] ) )
from CLASSES1:sch 1(A122);
reconsider E = rng f as non empty set by A125, RELAT_1:65;
A126:
for x being set st x in E holds
x is DecoratedTree of F1()
A131:
for T1, T2 being DecoratedTree
for k1, k2 being Element of NAT st T1 = f . k1 & T2 = f . k2 & k1 <= k2 holds
T1 c= T2
proof
let T1,
T2 be
DecoratedTree;
for k1, k2 being Element of NAT st T1 = f . k1 & T2 = f . k2 & k1 <= k2 holds
T1 c= T2let x,
y be
Element of
NAT ;
( T1 = f . x & T2 = f . y & x <= y implies T1 c= T2 )
assume that A132:
T1 = f . x
and A133:
T2 = f . y
and A134:
x <= y
;
T1 c= T2
consider T19 being
DecoratedTree of
F1(),
k1 being
Element of
NAT such that A135:
(
x = k1 &
f . x = T19 &
T19 . {} = F2() & ( for
t being
Element of
dom T19 holds
(
len t <= k1 & (
len t < k1 implies (
succ t = { (t ^ <*i*>) where i is Element of NAT : P1[i,T19 . t] } & ( for
n being
Element of
NAT for
x being
set st
x = T19 . t &
P1[
n,
x] holds
T19 . (t ^ <*n*>) = F3()
. x,
n ) ) ) ) ) )
by A125;
consider T29 being
DecoratedTree of
F1(),
k2 being
Element of
NAT such that A136:
(
y = k2 &
f . y = T29 &
T29 . {} = F2() & ( for
t being
Element of
dom T29 holds
(
len t <= k2 & (
len t < k2 implies (
succ t = { (t ^ <*i*>) where i is Element of NAT : P1[i,T29 . t] } & ( for
n being
Element of
NAT for
x being
set st
x = T29 . t &
P1[
n,
x] holds
T29 . (t ^ <*n*>) = F3()
. x,
n ) ) ) ) ) )
by A125;
defpred S3[
Element of
NAT ]
means for
t being
Element of
dom T1 st
len t <= $1 holds
(
t in dom T2 &
T1 . t = T2 . t );
A137:
S3[
0 ]
A140:
for
k being
Element of
NAT st
S3[
k] holds
S3[
k + 1]
proof
let k be
Element of
NAT ;
( S3[k] implies S3[k + 1] )
assume A141:
for
t being
Element of
dom T1 st
len t <= k holds
(
t in dom T2 &
T1 . t = T2 . t )
;
S3[k + 1]
let t be
Element of
dom T1;
( len t <= k + 1 implies ( t in dom T2 & T1 . t = T2 . t ) )
assume
len t <= k + 1
;
( t in dom T2 & T1 . t = T2 . t )
then A143:
(
len t <= k or
len t = k + 1 )
by NAT_1:8;
now assume A145:
len t = k + 1
;
( t in dom T2 & T1 . t = T2 . t )reconsider p =
t | (Seg k) as
FinSequence of
NAT by FINSEQ_1:23;
p is_a_prefix_of t
by TREES_1:def 1;
then reconsider p =
p as
Element of
dom T1 by TREES_1:45;
A147:
k <= k + 1
by NAT_1:11;
A148:
k + 1
<= k1
by A132, A135, A145;
A149:
len p = k
by A145, A147, FINSEQ_1:21;
A150:
k < k1
by A148, NAT_1:13;
A151:
T1 . p = T2 . p
by A141, A149;
reconsider p9 =
p as
Element of
dom T2 by A141, A149;
t <> {}
by A145;
then consider q being
FinSequence,
x being
set such that A153:
t = q ^ <*x*>
by FINSEQ_1:63;
A154:
(
p is_a_prefix_of t &
q is_a_prefix_of t )
by A153, TREES_1:8, TREES_1:def 1;
k + 1
= (len q) + 1
by A145, A153, FINSEQ_2:19;
then A156:
p = q
by A149, A154, Th1, TREES_1:19;
<*x*> is
FinSequence of
NAT
by A153, FINSEQ_1:50;
then A158:
rng <*x*> c= NAT
by FINSEQ_1:def 4;
(
rng <*x*> = {x} &
x in {x} )
by FINSEQ_1:55, TARSKI:def 1;
then reconsider x =
x as
Element of
NAT by A158;
A160:
p ^ <*x*> in succ p
by A153, A156;
succ p = { (p ^ <*i*>) where i is Element of NAT : P1[i,T1 . p] }
by A132, A135, A149, A150;
then consider i being
Element of
NAT such that A162:
p ^ <*x*> = p ^ <*i*>
and A163:
P1[
i,
T1 . p]
by A160;
A164:
k < k2
by A134, A135, A136, A150, XXREAL_0:2;
then A165:
succ p9 = { (p9 ^ <*l*>) where l is Element of NAT : P1[l,T2 . p9] }
by A133, A136, A149;
A166:
x = i
by A162, FINSEQ_2:20;
A167:
t in succ p9
by A151, A153, A156, A162, A163, A165;
T19 . t = F3()
. (T19 . p),
x
by A132, A135, A149, A150, A153, A156, A163, A166;
hence
(
t in dom T2 &
T1 . t = T2 . t )
by A132, A133, A135, A136, A149, A151, A153, A156, A163, A164, A166, A167;
verum end;
hence
(
t in dom T2 &
T1 . t = T2 . t )
by A141, A143;
verum
end;
A169:
for
k being
Element of
NAT holds
S3[
k]
from NAT_1:sch 1(A137, A140);
let x be
set ;
TARSKI:def 3 ( not x in T1 or x in T2 )
assume A170:
x in T1
;
x in T2
then consider y,
z being
set such that A171:
[y,z] = x
by RELAT_1:def 1;
A172:
T1 . y = z
by A170, A171, FUNCT_1:8;
reconsider y =
y as
Element of
dom T1 by A170, A171, FUNCT_1:8;
len y <= len y
;
then
(
y in dom T2 &
T1 . y = T2 . y )
by A169;
hence
x in T2
by A171, A172, FUNCT_1:8;
verum
end;
E is c=-linear
proof
let T1,
T2 be
set ;
ORDINAL1:def 9 ( not T1 in E or not T2 in E or T1,T2 are_c=-comparable )
assume A176:
T1 in E
;
( not T2 in E or T1,T2 are_c=-comparable )
then consider x being
set such that A177:
x in dom f
and A178:
T1 = f . x
by FUNCT_1:def 5;
assume A179:
T2 in E
;
T1,T2 are_c=-comparable
then consider y being
set such that A180:
y in dom f
and A181:
T2 = f . y
by FUNCT_1:def 5;
A182:
T1 is
DecoratedTree
by A126, A176;
A183:
T2 is
DecoratedTree
by A126, A179;
reconsider x =
x,
y =
y as
Element of
NAT by A125, A177, A180;
(
x <= y or
y <= x )
;
hence
(
T1 c= T2 or
T2 c= T1 )
by A131, A178, A181, A182, A183;
XBOOLE_0:def 9 verum
end;
then reconsider T = union (rng f) as DecoratedTree of F1() by A126, Th38;
take
T
; ( T . {} = F2() & ( for t being Element of dom T holds
( succ t = { (t ^ <*k*>) where k is Element of NAT : P1[k,T . t] } & ( for n being Element of NAT st P1[n,T . t] holds
T . (t ^ <*n*>) = F3() . (T . t),n ) ) ) )
consider T9 being DecoratedTree of F1(), k being Element of NAT such that
A185:
( 0 = k & f . 0 = T9 & T9 . {} = F2() & ( for t being Element of dom T9 holds
( len t <= k & ( len t < k implies ( succ t = { (t ^ <*i*>) where i is Element of NAT : P1[i,T9 . t] } & ( for n being Element of NAT
for x being set st x = T9 . t & P1[n,x] holds
T9 . (t ^ <*n*>) = F3() . x,n ) ) ) ) ) )
by A125;
{} in dom T9
by TREES_1:47;
then A187:
[{} ,F2()] in T9
by A185, FUNCT_1:8;
T9 in rng f
by A125, A185, FUNCT_1:def 5;
then
[{} ,F2()] in T
by A187, TARSKI:def 4;
hence
T . {} = F2()
by FUNCT_1:8; for t being Element of dom T holds
( succ t = { (t ^ <*k*>) where k is Element of NAT : P1[k,T . t] } & ( for n being Element of NAT st P1[n,T . t] holds
T . (t ^ <*n*>) = F3() . (T . t),n ) )
A190:
for T1 being DecoratedTree
for x being set st T1 in E & x in dom T1 holds
( x in dom T & T1 . x = T . x )
let t be Element of dom T; ( succ t = { (t ^ <*k*>) where k is Element of NAT : P1[k,T . t] } & ( for n being Element of NAT st P1[n,T . t] holds
T . (t ^ <*n*>) = F3() . (T . t),n ) )
thus
succ t c= { (t ^ <*i*>) where i is Element of NAT : P1[i,T . t] }
XBOOLE_0:def 10 ( { (t ^ <*k*>) where k is Element of NAT : P1[k,T . t] } c= succ t & ( for n being Element of NAT st P1[n,T . t] holds
T . (t ^ <*n*>) = F3() . (T . t),n ) )proof
let x be
set ;
TARSKI:def 3 ( not x in succ t or x in { (t ^ <*i*>) where i is Element of NAT : P1[i,T . t] } )
assume
x in succ t
;
x in { (t ^ <*i*>) where i is Element of NAT : P1[i,T . t] }
then consider l being
Element of
NAT such that A196:
x = t ^ <*l*>
and A197:
t ^ <*l*> in dom T
;
[x,(T . x)] in T
by A196, A197, FUNCT_1:8;
then consider X being
set such that A199:
[x,(T . x)] in X
and A200:
X in rng f
by TARSKI:def 4;
consider y being
set such that A201:
y in NAT
and A202:
X = f . y
by A125, A200, FUNCT_1:def 5;
consider T1 being
DecoratedTree of
F1(),
k1 being
Element of
NAT such that A203:
(
y = k1 &
f . y = T1 &
T1 . {} = F2() & ( for
t being
Element of
dom T1 holds
(
len t <= k1 & (
len t < k1 implies (
succ t = { (t ^ <*i*>) where i is Element of NAT : P1[i,T1 . t] } & ( for
n being
Element of
NAT for
x being
set st
x = T1 . t &
P1[
n,
x] holds
T1 . (t ^ <*n*>) = F3()
. x,
n ) ) ) ) ) )
by A125, A201;
A204:
t ^ <*l*> in dom T1
by A196, A199, A202, A203, FUNCT_1:8;
then reconsider t9 =
t,
p =
t ^ <*l*> as
Element of
dom T1 by TREES_1:46;
len p <= k1
by A203;
then
(len t) + 1
<= k1
by FINSEQ_2:19;
then A207:
len t9 < k1
by NAT_1:13;
then A208:
succ t9 = { (t9 ^ <*i*>) where i is Element of NAT : P1[i,T1 . t9] }
by A203;
T1 . t = T . t
by A190, A200, A202, A203, A207;
hence
x in { (t ^ <*i*>) where i is Element of NAT : P1[i,T . t] }
by A196, A204, A208;
verum
end;
[t,(T . t)] in T
by FUNCT_1:8;
then consider X being set such that
A211:
[t,(T . t)] in X
and
A212:
X in E
by TARSKI:def 4;
consider y being set such that
A213:
y in NAT
and
A214:
X = f . y
by A125, A212, FUNCT_1:def 5;
reconsider y = y as Element of NAT by A213;
consider T1 being DecoratedTree of F1(), k1 being Element of NAT such that
A215:
( y = k1 & f . y = T1 & T1 . {} = F2() & ( for t being Element of dom T1 holds
( len t <= k1 & ( len t < k1 implies ( succ t = { (t ^ <*i*>) where i is Element of NAT : P1[i,T1 . t] } & ( for n being Element of NAT
for x being set st x = T1 . t & P1[n,x] holds
T1 . (t ^ <*n*>) = F3() . x,n ) ) ) ) ) )
by A125;
consider T2 being DecoratedTree of F1(), k2 being Element of NAT such that
A216:
( y + 1 = k2 & f . (y + 1) = T2 & T2 . {} = F2() & ( for t being Element of dom T2 holds
( len t <= k2 & ( len t < k2 implies ( succ t = { (t ^ <*i*>) where i is Element of NAT : P1[i,T2 . t] } & ( for n being Element of NAT
for x being set st x = T2 . t & P1[n,x] holds
T2 . (t ^ <*n*>) = F3() . x,n ) ) ) ) ) )
by A125;
y <= y + 1
by NAT_1:11;
then A218:
T1 c= T2
by A131, A215, A216;
reconsider t1 = t as Element of dom T1 by A211, A214, A215, FUNCT_1:8;
A219:
len t1 <= y
by A215;
A220:
T2 . t = T . t
by A211, A214, A215, A218, FUNCT_1:8;
reconsider t2 = t as Element of dom T2 by A211, A214, A215, A218, FUNCT_1:8;
A221:
len t2 < y + 1
by A219, NAT_1:13;
then A222:
succ t2 = { (t2 ^ <*i*>) where i is Element of NAT : P1[i,T2 . t2] }
by A216;
thus
{ (t ^ <*i*>) where i is Element of NAT : P1[i,T . t] } c= succ t
for n being Element of NAT st P1[n,T . t] holds
T . (t ^ <*n*>) = F3() . (T . t),n
let n be Element of NAT ; ( P1[n,T . t] implies T . (t ^ <*n*>) = F3() . (T . t),n )
assume A228:
P1[n,T . t]
; T . (t ^ <*n*>) = F3() . (T . t),n
then A229:
t ^ <*n*> in succ t2
by A220, A222;
T2 in E
by A125, A216, FUNCT_1:def 5;
then
T2 . (t ^ <*n*>) = T . (t ^ <*n*>)
by A190, A229;
hence
T . (t ^ <*n*>) = F3() . (T . t),n
by A216, A220, A221, A228; verum