defpred S1[ 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 Nat : k in F3((T . t)) } & ( for n being Nat
for x being set st x = T . t & n in F3(x) holds
T . (t ^ <*n*>) = F4() . (x,n) ) ) ) ) ) );
reconsider W = {{}} as Tree ;
A2:
S1[ 0 ]
A3:
for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
given T being
DecoratedTree of
F1()
such that A4:
(
T . {} = F2() & ( for
t being
Element of
dom T holds
(
len t <= k & (
len t < k implies (
succ t = { (t ^ <*m*>) where m is Nat : m in F3((T . t)) } & ( for
n being
Nat for
x being
set st
x = T . t &
n in F3(
x) holds
T . (t ^ <*n*>) = F4()
. (
x,
n) ) ) ) ) ) )
;
S1[k + 1]
reconsider M =
{ (t ^ <*n*>) where n is Nat, t is Element of dom T : n in F3((T . t)) } \/ (dom T) as non
empty set ;
M is
Tree-like
proof
thus
M c= NAT *
TREES_1:def 3 ( ( for b1 being FinSequence of omega holds
( not b1 in M or ProperPrefixes b1 c= M ) ) & ( for b1 being FinSequence of omega
for b2, b3 being set 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 omega
for b2, b3 being set holds
( not b1 ^ <*b2*> in M or not b3 <= b2 or b1 ^ <*b3*> in M )
let p be
FinSequence of
NAT ;
for b1, b2 being set holds
( not p ^ <*b1*> in M or not b2 <= b1 or p ^ <*b2*> in M )let m,
n be
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 A14:
(
p ^ <*m*> in { (t ^ <*l*>) where l is Nat, t is Element of dom T : l in F3((T . t)) } or
p ^ <*m*> in dom T )
by XBOOLE_0:def 3;
assume that A15:
n <= m
and A16:
not
p ^ <*n*> in M
;
contradiction
not
p ^ <*n*> in dom T
by A16, XBOOLE_0:def 3;
then consider l being
Nat,
t being
Element of
dom T such that A17:
p ^ <*m*> = t ^ <*l*>
and A18:
l in F3(
(T . t))
by A14, A15, TREES_1:def 3;
A19:
(
len (p ^ <*m*>) = (len p) + (len <*m*>) &
len <*m*> = 1 )
by FINSEQ_1:22, FINSEQ_1:40;
A20:
(
len (t ^ <*l*>) = (len t) + (len <*l*>) &
len <*l*> = 1 )
by FINSEQ_1:22, FINSEQ_1:40;
A21:
(
(p ^ <*m*>) . ((len p) + 1) = m &
(t ^ <*l*>) . ((len t) + 1) = l )
by FINSEQ_1:42;
then A22:
p = t
by A17, A19, A20, FINSEQ_1:33;
n in F3(
(T . t))
by A1, A15, A17, A18, A19, A20, A21;
then
p ^ <*n*> in { (s ^ <*i*>) where i is Nat, s is Element of dom T : i in F3((T . s)) }
by A22;
hence
contradiction
by A16, 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
Nat ex
q being
FinSequence of
NAT st
( $1
= q ^ <*n*> & $2
= F4()
. (
(T . q),
n) ) ) );
A23:
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 A27:
(
dom T9 = M & ( for
p being
FinSequence of
NAT st
p in M holds
S2[
p,
T9 . p] ) )
from TREES_2:sch 6(A23);
rng T9 c= F1()
proof
let x be
object ;
TARSKI:def 3 ( not x in rng T9 or x in F1() )
assume
x in rng T9
;
x in F1()
then consider y being
object such that A28:
y in dom T9
and A29:
x = T9 . y
by FUNCT_1:def 3;
reconsider y =
y as
Element of
dom T9 by A28;
now ( not y in dom T implies x in F1() )assume A31:
not
y in dom T
;
x in F1()then consider n being
Nat,
q being
FinSequence of
NAT such that A32:
y = q ^ <*n*>
and A33:
T9 . y = F4()
. (
(T . q),
n)
by A27;
y in { (t ^ <*l*>) where l is Nat, t is Element of dom T : l in F3((T . t)) }
by A27, A31, XBOOLE_0:def 3;
then consider l being
Nat,
t being
Element of
dom T such that A34:
y = t ^ <*l*>
and
l in F3(
(T . t))
;
A35:
len <*n*> = 1
by FINSEQ_1:39;
A36:
len <*l*> = 1
by FINSEQ_1:39;
A37:
len (q ^ <*n*>) = (len q) + 1
by A35, FINSEQ_1:22;
A38:
len (t ^ <*l*>) = (len t) + 1
by A36, FINSEQ_1:22;
(
(q ^ <*n*>) . ((len q) + 1) = n &
(t ^ <*l*>) . ((len t) + 1) = l )
by FINSEQ_1:42;
then A39:
q = t
by A32, A34, A37, A38, FINSEQ_1:33;
A40:
n in NAT
by ORDINAL1:def 12;
T . t in F1()
;
then
[(T . q),n] in [:F1(),NAT:]
by A39, ZFMISC_1:87, A40;
hence
x in F1()
by A29, A33, FUNCT_2:5;
verum end;
hence
x in F1()
by A30;
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 Nat : k in F3((T9 . t)) } & ( for n being Nat
for x being set st x = T9 . t & n in F3(x) holds
T9 . (t ^ <*n*>) = F4() . (x,n) ) ) ) ) ) )
(
<*> NAT in M &
<*> NAT in dom T )
by TREES_1:22;
hence
T9 . {} = F2()
by A4, A27;
for t being Element of dom T9 holds
( len t <= k + 1 & ( len t < k + 1 implies ( succ t = { (t ^ <*k*>) where k is Nat : k in F3((T9 . t)) } & ( for n being Nat
for x being set st x = T9 . t & n in F3(x) holds
T9 . (t ^ <*n*>) = F4() . (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 Nat : k in F3((T9 . t)) } & ( for n being Nat
for x being set st x = T9 . t & n in F3(x) holds
T9 . (t ^ <*n*>) = F4() . (x,n) ) ) ) )
hence
len t <= k + 1
by A27, A41, XBOOLE_0:def 3;
( len t < k + 1 implies ( succ t = { (t ^ <*k*>) where k is Nat : k in F3((T9 . t)) } & ( for n being Nat
for x being set st x = T9 . t & n in F3(x) holds
T9 . (t ^ <*n*>) = F4() . (x,n) ) ) )
assume A43:
len t < k + 1
;
( succ t = { (t ^ <*k*>) where k is Nat : k in F3((T9 . t)) } & ( for n being Nat
for x being set st x = T9 . t & n in F3(x) holds
T9 . (t ^ <*n*>) = F4() . (x,n) ) )
then A49:
T9 . t = T . t
by A27;
reconsider t9 =
t as
Element of
dom T by A44;
thus
succ t c= { (t ^ <*i*>) where i is Nat : i in F3((T9 . t)) }
XBOOLE_0:def 10 ( { (t ^ <*k*>) where k is Nat : k in F3((T9 . t)) } c= succ t & ( for n being Nat
for x being set st x = T9 . t & n in F3(x) holds
T9 . (t ^ <*n*>) = F4() . (x,n) ) )
thus A55:
{ (t ^ <*i*>) where i is Nat : i in F3((T9 . t)) } c= succ t
for n being Nat
for x being set st x = T9 . t & n in F3(x) holds
T9 . (t ^ <*n*>) = F4() . (x,n)
let n be
Nat;
for x being set st x = T9 . t & n in F3(x) holds
T9 . (t ^ <*n*>) = F4() . (x,n)let x be
set ;
( x = T9 . t & n in F3(x) implies T9 . (t ^ <*n*>) = F4() . (x,n) )
assume that A58:
x = T9 . t
and A59:
n in F3(
x)
;
T9 . (t ^ <*n*>) = F4() . (x,n)
t ^ <*n*> in { (t ^ <*i*>) where i is Nat : i in F3((T9 . t)) }
by A58, A59;
then A60:
t ^ <*n*> in succ t
by A55;
reconsider n =
n as
Element of
NAT by ORDINAL1:def 12;
hence
T9 . (t ^ <*n*>) = F4()
. (
x,
n)
;
verum
end;
A64:
for k being Nat holds S1[k]
from NAT_1:sch 2(A2, A3);
defpred S2[ object , object ] means ex T being DecoratedTree of F1() ex k being 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 Nat : i in F3((T . t)) } & ( for n being Nat
for x being set st x = T . t & n in F3(x) holds
T . (t ^ <*n*>) = F4() . (x,n) ) ) ) ) ) );
A65:
for x being object st x in NAT holds
ex y being object st S2[x,y]
consider f being Function such that
A67:
( dom f = NAT & ( for x being object st x in NAT holds
S2[x,f . x] ) )
from CLASSES1:sch 1(A65);
A68:
for x being Nat holds S2[x,f . x]
by ORDINAL1:def 12, A67;
reconsider E = rng f as non empty set by A67, RELAT_1:42;
A69:
for x being set st x in E holds
x is DecoratedTree of F1()
A72:
for T1, T2 being DecoratedTree
for k1, k2 being Nat st T1 = f . k1 & T2 = f . k2 & k1 <= k2 holds
T1 c= T2
proof
let T1,
T2 be
DecoratedTree;
for k1, k2 being Nat st T1 = f . k1 & T2 = f . k2 & k1 <= k2 holds
T1 c= T2let x,
y be
Nat;
( T1 = f . x & T2 = f . y & x <= y implies T1 c= T2 )
assume that A73:
T1 = f . x
and A74:
T2 = f . y
and A75:
x <= y
;
T1 c= T2
consider T19 being
DecoratedTree of
F1(),
k1 being
Nat such that A76:
(
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 Nat : i in F3((T19 . t)) } & ( for
n being
Nat for
x being
set st
x = T19 . t &
n in F3(
x) holds
T19 . (t ^ <*n*>) = F4()
. (
x,
n) ) ) ) ) ) )
by A68;
consider T29 being
DecoratedTree of
F1(),
k2 being
Nat such that A77:
(
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 Nat : i in F3((T29 . t)) } & ( for
n being
Nat for
x being
set st
x = T29 . t &
n in F3(
x) holds
T29 . (t ^ <*n*>) = F4()
. (
x,
n) ) ) ) ) ) )
by A68;
defpred S3[
Nat]
means for
t being
Element of
dom T1 st
len t <= $1 holds
(
t in dom T2 &
T1 . t = T2 . t );
A78:
S3[
0 ]
A80:
for
k being
Nat st
S3[
k] holds
S3[
k + 1]
proof
let k be
Nat;
( S3[k] implies S3[k + 1] )
assume A81:
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 A82:
(
len t <= k or
len t = k + 1 )
by NAT_1:8;
now ( len t = k + 1 implies ( t in dom T2 & T1 . t = T2 . t ) )assume A83:
len t = k + 1
;
( t in dom T2 & T1 . t = T2 . t )reconsider p =
t | (Seg k) as
FinSequence of
NAT by FINSEQ_1:18;
p is_a_prefix_of t
;
then reconsider p =
p as
Element of
dom T1 by TREES_1:20;
A84:
k <= k + 1
by NAT_1:11;
A85:
k + 1
<= k1
by A73, A76, A83;
A86:
len p = k
by A83, A84, FINSEQ_1:17;
A87:
k < k1
by A85, NAT_1:13;
A88:
T1 . p = T2 . p
by A81, A86;
reconsider p9 =
p as
Element of
dom T2 by A81, A86;
t <> {}
by A83;
then consider q being
FinSequence,
x being
object such that A89:
t = q ^ <*x*>
by FINSEQ_1:46;
A90:
(
p is_a_prefix_of t &
q is_a_prefix_of t )
by A89, TREES_1:1;
k + 1
= (len q) + 1
by A83, A89, FINSEQ_2:16;
then A91:
p = q
by A86, A90, Th1, TREES_1:4;
<*x*> is
FinSequence of
NAT
by A89, FINSEQ_1:36;
then A92:
rng <*x*> c= NAT
by FINSEQ_1:def 4;
(
rng <*x*> = {x} &
x in {x} )
by FINSEQ_1:38, TARSKI:def 1;
then reconsider x =
x as
Nat by A92;
A93:
p ^ <*x*> in succ p
by A89, A91;
succ p = { (p ^ <*i*>) where i is Nat : i in F3((T1 . p)) }
by A73, A76, A86, A87;
then consider i being
Nat such that A94:
p ^ <*x*> = p ^ <*i*>
and A95:
i in F3(
(T1 . p))
by A93;
A96:
k < k2
by A75, A76, A77, A87, XXREAL_0:2;
then A97:
succ p9 = { (p9 ^ <*l*>) where l is Nat : l in F3((T2 . p9)) }
by A74, A77, A86;
A98:
x = i
by A94, FINSEQ_2:17;
A99:
t in succ p9
by A88, A89, A91, A94, A95, A97;
T19 . t = F4()
. (
(T19 . p),
x)
by A73, A76, A86, A87, A89, A91, A95, A98;
hence
(
t in dom T2 &
T1 . t = T2 . t )
by A73, A74, A76, A77, A86, A88, A89, A91, A95, A96, A98, A99;
verum end;
hence
(
t in dom T2 &
T1 . t = T2 . t )
by A81, A82;
verum
end;
A100:
for
k being
Nat holds
S3[
k]
from NAT_1:sch 2(A78, A80);
let x be
object ;
TARSKI:def 3 ( not x in T1 or x in T2 )
assume A101:
x in T1
;
x in T2
then consider y,
z being
object such that A102:
[y,z] = x
by RELAT_1:def 1;
A103:
T1 . y = z
by A101, A102, FUNCT_1:1;
reconsider y =
y as
Element of
dom T1 by A101, A102, FUNCT_1:1;
len y <= len y
;
then
(
y in dom T2 &
T1 . y = T2 . y )
by A100;
hence
x in T2
by A102, A103, FUNCT_1:1;
verum
end;
E is c=-linear
proof
let T1,
T2 be
set ;
ORDINAL1:def 8 ( not T1 in E or not T2 in E or T1,T2 are_c=-comparable )
assume A104:
T1 in E
;
( not T2 in E or T1,T2 are_c=-comparable )
then consider x being
object such that A105:
x in dom f
and A106:
T1 = f . x
by FUNCT_1:def 3;
assume A107:
T2 in E
;
T1,T2 are_c=-comparable
then consider y being
object such that A108:
y in dom f
and A109:
T2 = f . y
by FUNCT_1:def 3;
A110:
T1 is
DecoratedTree
by A69, A104;
A111:
T2 is
DecoratedTree
by A69, A107;
reconsider x =
x,
y =
y as
Nat by A67, A105, A108;
(
x <= y or
y <= x )
;
hence
(
T1 c= T2 or
T2 c= T1 )
by A72, A106, A109, A110, A111;
XBOOLE_0:def 9 verum
end;
then reconsider T = union (rng f) as DecoratedTree of F1() by A69, Th36;
take
T
; ( T . {} = F2() & ( for t being Element of dom T holds
( succ t = { (t ^ <*k*>) where k is Nat : k in F3((T . t)) } & ( for n being Nat st n in F3((T . t)) holds
T . (t ^ <*n*>) = F4() . ((T . t),n) ) ) ) )
consider T9 being DecoratedTree of F1(), k being Nat such that
A112:
( 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 Nat : i in F3((T9 . t)) } & ( for n being Nat
for x being set st x = T9 . t & n in F3(x) holds
T9 . (t ^ <*n*>) = F4() . (x,n) ) ) ) ) ) )
by A67;
{} in dom T9
by TREES_1:22;
then A113:
[{},F2()] in T9
by A112, FUNCT_1:1;
T9 in rng f
by A67, A112, FUNCT_1:def 3;
then
[{},F2()] in T
by A113, TARSKI:def 4;
hence
T . {} = F2()
by FUNCT_1:1; for t being Element of dom T holds
( succ t = { (t ^ <*k*>) where k is Nat : k in F3((T . t)) } & ( for n being Nat st n in F3((T . t)) holds
T . (t ^ <*n*>) = F4() . ((T . t),n) ) )
A114:
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 Nat : k in F3((T . t)) } & ( for n being Nat st n in F3((T . t)) holds
T . (t ^ <*n*>) = F4() . ((T . t),n) ) )
thus
succ t c= { (t ^ <*i*>) where i is Nat : i in F3((T . t)) }
XBOOLE_0:def 10 ( { (t ^ <*k*>) where k is Nat : k in F3((T . t)) } c= succ t & ( for n being Nat st n in F3((T . t)) holds
T . (t ^ <*n*>) = F4() . ((T . t),n) ) )proof
let x be
object ;
TARSKI:def 3 ( not x in succ t or x in { (t ^ <*i*>) where i is Nat : i in F3((T . t)) } )
assume
x in succ t
;
x in { (t ^ <*i*>) where i is Nat : i in F3((T . t)) }
then consider l being
Nat such that A117:
x = t ^ <*l*>
and A118:
t ^ <*l*> in dom T
;
[x,(T . x)] in T
by A117, A118, FUNCT_1:1;
then consider X being
set such that A119:
[x,(T . x)] in X
and A120:
X in rng f
by TARSKI:def 4;
consider y being
object such that A121:
y in NAT
and A122:
X = f . y
by A67, A120, FUNCT_1:def 3;
consider T1 being
DecoratedTree of
F1(),
k1 being
Nat such that A123:
(
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 Nat : i in F3((T1 . t)) } & ( for
n being
Nat for
x being
set st
x = T1 . t &
n in F3(
x) holds
T1 . (t ^ <*n*>) = F4()
. (
x,
n) ) ) ) ) ) )
by A67, A121;
A124:
t ^ <*l*> in dom T1
by A117, A119, A122, A123, FUNCT_1:1;
then reconsider t9 =
t,
p =
t ^ <*l*> as
Element of
dom T1 by TREES_1:21;
len p <= k1
by A123;
then
(len t) + 1
<= k1
by FINSEQ_2:16;
then A125:
len t9 < k1
by NAT_1:13;
then A126:
succ t9 = { (t9 ^ <*i*>) where i is Nat : i in F3((T1 . t9)) }
by A123;
T1 . t = T . t
by A114, A120, A122, A123, A125;
hence
x in { (t ^ <*i*>) where i is Nat : i in F3((T . t)) }
by A117, A124, A126;
verum
end;
[t,(T . t)] in T
by FUNCT_1:1;
then consider X being set such that
A127:
[t,(T . t)] in X
and
A128:
X in E
by TARSKI:def 4;
consider y being object such that
A129:
y in NAT
and
A130:
X = f . y
by A67, A128, FUNCT_1:def 3;
reconsider y = y as Nat by A129;
consider T1 being DecoratedTree of F1(), k1 being Nat such that
A131:
( 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 Nat : i in F3((T1 . t)) } & ( for n being Nat
for x being set st x = T1 . t & n in F3(x) holds
T1 . (t ^ <*n*>) = F4() . (x,n) ) ) ) ) ) )
by A68;
consider T2 being DecoratedTree of F1(), k2 being Nat such that
A132:
( 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 Nat : i in F3((T2 . t)) } & ( for n being Nat
for x being set st x = T2 . t & n in F3(x) holds
T2 . (t ^ <*n*>) = F4() . (x,n) ) ) ) ) ) )
by A67;
y <= y + 1
by NAT_1:11;
then A133:
T1 c= T2
by A72, A131, A132;
reconsider t1 = t as Element of dom T1 by A127, A130, A131, FUNCT_1:1;
A134:
len t1 <= y
by A131;
A135:
T2 . t = T . t
by A127, A130, A131, A133, FUNCT_1:1;
reconsider t2 = t as Element of dom T2 by A127, A130, A131, A133, FUNCT_1:1;
A136:
len t2 < y + 1
by A134, NAT_1:13;
then A137:
succ t2 = { (t2 ^ <*i*>) where i is Nat : i in F3((T2 . t2)) }
by A132;
thus
{ (t ^ <*i*>) where i is Nat : i in F3((T . t)) } c= succ t
for n being Nat st n in F3((T . t)) holds
T . (t ^ <*n*>) = F4() . ((T . t),n)
let n be Nat; ( n in F3((T . t)) implies T . (t ^ <*n*>) = F4() . ((T . t),n) )
assume A141:
n in F3((T . t))
; T . (t ^ <*n*>) = F4() . ((T . t),n)
then A142:
t ^ <*n*> in succ t2
by A135, A137;
T2 in E
by A67, A132, FUNCT_1:def 3;
then
T2 . (t ^ <*n*>) = T . (t ^ <*n*>)
by A114, A142;
hence
T . (t ^ <*n*>) = F4() . ((T . t),n)
by A132, A135, A136, A141; verum