trees_2.miz
begin
reserve x,y,z,a,b,c,X,X1,X2,Y,Z for
set,
W,W1,W2 for
Tree,
w,w9 for
Element of W,
f for
Function,
D,D9 for non
empty
set,
i,k,k1,k2,l,m,n for
Nat,
v,v1,v2 for
FinSequence,
p,q,r,r1,r2 for
FinSequence of
NAT ;
theorem ::
TREES_2:1
Th1: for v1, v2, v st v1
is_a_prefix_of v & v2
is_a_prefix_of v holds (v1,v2)
are_c=-comparable
proof
let p,q,r be
FinSequence;
assume p
is_a_prefix_of r;
then
A1: ex p9 be
FinSequence st r
= (p
^ p9) by
TREES_1: 1;
assume q
is_a_prefix_of r;
then
A2: ex q9 be
FinSequence st r
= (q
^ q9) by
TREES_1: 1;
(
len p)
<= (
len q) or (
len q)
<= (
len p);
then (ex t be
FinSequence st (p
^ t)
= q) or ex t be
FinSequence st (q
^ t)
= p by
A1,
A2,
FINSEQ_1: 47;
hence p
is_a_prefix_of q or q
is_a_prefix_of p by
TREES_1: 1;
end;
theorem ::
TREES_2:2
Th2: for v1, v2, v st v1
is_a_proper_prefix_of v & v2
is_a_prefix_of v holds (v1,v2)
are_c=-comparable by
Th1;
theorem ::
TREES_2:3
Th3: (
len v1)
= (k
+ 1) implies ex v2, x st v1
= (v2
^
<*x*>) & (
len v2)
= k
proof
assume
A1: (
len v1)
= (k
+ 1);
reconsider v2 = (v1
| (
Seg k)) as
FinSequence by
FINSEQ_1: 15;
v2
is_a_prefix_of v1;
then
consider v such that
A2: v1
= (v2
^ v) by
TREES_1: 1;
take v2, (v
. 1);
A3: k
<= (k
+ 1) by
NAT_1: 11;
then (
len v2)
= k by
A1,
FINSEQ_1: 17;
then (k
+ (
len v))
= (k
+ 1) by
A1,
A2,
FINSEQ_1: 22;
hence thesis by
A1,
A2,
A3,
FINSEQ_1: 17,
FINSEQ_1: 40;
end;
theorem ::
TREES_2:4
Th4: (
ProperPrefixes (v
^
<*x*>))
= ((
ProperPrefixes v)
\/
{v})
proof
thus (
ProperPrefixes (v
^
<*x*>))
c= ((
ProperPrefixes v)
\/
{v})
proof
let y be
object;
assume y
in (
ProperPrefixes (v
^
<*x*>));
then
consider v1 such that
A1: y
= v1 and
A2: v1
is_a_proper_prefix_of (v
^
<*x*>) by
TREES_1:def 2;
v1
is_a_prefix_of v & v1
<> v or v1
= v by
A2,
TREES_1: 9;
then v1
is_a_proper_prefix_of v or v1
in
{v} by
TARSKI:def 1;
then y
in (
ProperPrefixes v) or y
in
{v} by
A1,
TREES_1:def 2;
hence thesis by
XBOOLE_0:def 3;
end;
let y be
object;
assume y
in ((
ProperPrefixes v)
\/
{v});
then
A3: y
in (
ProperPrefixes v) or y
in
{v} by
XBOOLE_0:def 3;
A4:
now
assume y
in (
ProperPrefixes v);
then
consider v1 such that
A5: y
= v1 and
A6: v1
is_a_proper_prefix_of v by
TREES_1:def 2;
v
is_a_prefix_of (v
^
<*x*>) by
TREES_1: 1;
then v1
is_a_proper_prefix_of (v
^
<*x*>) by
A6,
XBOOLE_1: 58;
hence thesis by
A5,
TREES_1:def 2;
end;
(v
^
{} )
= v by
FINSEQ_1: 34;
then v
is_a_prefix_of (v
^
<*x*>) & v
<> (v
^
<*x*>) by
FINSEQ_1: 33,
TREES_1: 1;
then v
is_a_proper_prefix_of (v
^
<*x*>);
then y
in (
ProperPrefixes v) or y
= v & v
in (
ProperPrefixes (v
^
<*x*>)) by
A3,
TARSKI:def 1,
TREES_1:def 2;
hence thesis by
A4;
end;
scheme ::
TREES_2:sch1
TreeStructInd { T() ->
Tree , P[
set] } :
for t be
Element of T() holds P[t]
provided
A1: P[
{} ]
and
A2: for t be
Element of T(), n st P[t] & (t
^
<*n*>)
in T() holds P[(t
^
<*n*>)];
defpred
X[
set] means for t be
Element of T() st (
len t)
= $1 holds P[t];
(
card x)
=
0 implies x
=
{} ;
then
A3:
X[
0 ] by
A1;
A4:
X[k] implies
X[(k
+ 1)]
proof
assume
A5: for t be
Element of T() st (
len t)
= k holds P[t];
let t be
Element of T();
assume (
len t)
= (k
+ 1);
then
consider v, x such that
A6: t
= (v
^
<*x*>) and
A7: (
len v)
= k by
Th3;
reconsider v as
FinSequence of
NAT by
A6,
FINSEQ_1: 36;
reconsider v as
Element of T() by
A6,
TREES_1: 21;
(
rng
<*x*>)
c= (
rng t) by
A6,
FINSEQ_1: 30;
then (
rng
<*x*>)
=
{x} & (
rng
<*x*>)
c=
NAT by
FINSEQ_1: 39,
XBOOLE_1: 1;
then
reconsider x as
Element of
NAT by
ZFMISC_1: 31;
A8: P[v] by
A5,
A7;
x
= x;
hence thesis by
A2,
A6,
A8;
end;
A9:
X[k] from
NAT_1:sch 2(
A3,
A4);
let t be
Element of T();
(
len t)
= (
len t);
hence thesis by
A9;
end;
theorem ::
TREES_2:5
Th5: (for p holds p
in W1 iff p
in W2) implies W1
= W2
proof
assume
A1: for p holds p
in W1 iff p
in W2;
thus W1
c= W2
proof
let x be
object;
assume x
in W1;
then
reconsider p = x as
Element of W1;
p
in W2 by
A1;
hence thesis;
end;
let x be
object;
assume x
in W2;
then
reconsider p = x as
Element of W2;
p
in W1 by
A1;
hence thesis;
end;
definition
let W1, W2;
:: original:
=
redefine
::
TREES_2:def1
pred W1
= W2 means for p holds p
in W1 iff p
in W2;
compatibility by
Th5;
end
theorem ::
TREES_2:6
p
in W implies W
= (W
with-replacement (p,(W
| p)))
proof
assume
A1: p
in W;
now
let q;
thus q
in W implies q
in (W
with-replacement (p,(W
| p)))
proof
assume
A2: q
in W;
now
assume p
is_a_proper_prefix_of q;
then p
is_a_prefix_of q;
then
consider r be
FinSequence such that
A3: q
= (p
^ r) by
TREES_1: 1;
(
rng r)
c= (
rng q) by
A3,
FINSEQ_1: 30;
then (
rng r)
c=
NAT by
XBOOLE_1: 1;
then
reconsider r as
FinSequence of
NAT by
FINSEQ_1:def 4;
take r;
thus r
in (W
| p) & q
= (p
^ r) by
A1,
A2,
A3,
TREES_1:def 6;
end;
hence thesis by
A1,
A2,
TREES_1:def 9;
end;
assume that
A4: q
in (W
with-replacement (p,(W
| p))) and
A5: not q
in W;
ex r st r
in (W
| p) & q
= (p
^ r) by
A1,
A4,
A5,
TREES_1:def 9;
hence contradiction by
A1,
A5,
TREES_1:def 6;
end;
hence thesis;
end;
theorem ::
TREES_2:7
Th7: p
in W & q
in W & not p
is_a_prefix_of q implies q
in (W
with-replacement (p,W1))
proof
not p
is_a_prefix_of q implies not p
is_a_proper_prefix_of q;
hence thesis by
TREES_1:def 9;
end;
theorem ::
TREES_2:8
p
in W & q
in W & not (p,q)
are_c=-comparable implies ((W
with-replacement (p,W1))
with-replacement (q,W2))
= ((W
with-replacement (q,W2))
with-replacement (p,W1))
proof
assume that
A1: p
in W and
A2: q
in W and
A3: not (p,q)
are_c=-comparable ;
A4: not p
is_a_prefix_of q by
A3;
not q
is_a_prefix_of p by
A3;
then
A5: p
in (W
with-replacement (q,W2)) by
A1,
A2,
Th7;
A6: q
in (W
with-replacement (p,W1)) by
A1,
A2,
A4,
Th7;
let r;
thus r
in ((W
with-replacement (p,W1))
with-replacement (q,W2)) implies r
in ((W
with-replacement (q,W2))
with-replacement (p,W1))
proof
assume r
in ((W
with-replacement (p,W1))
with-replacement (q,W2));
then r
in (W
with-replacement (p,W1)) & not q
is_a_proper_prefix_of r or ex r1 st r1
in W2 & r
= (q
^ r1) by
A6,
TREES_1:def 9;
then r
in W & not p
is_a_proper_prefix_of r & not q
is_a_proper_prefix_of r or (ex r2 st r2
in W1 & r
= (p
^ r2)) & not q
is_a_proper_prefix_of r or q
is_a_prefix_of r & ex r1 st r1
in W2 & r
= (q
^ r1) by
A1,
TREES_1: 1,
TREES_1:def 9;
then r
in (W
with-replacement (q,W2)) & not p
is_a_proper_prefix_of r or ex r1 st r1
in W1 & r
= (p
^ r1) by
A2,
A3,
Th2,
TREES_1:def 9;
hence thesis by
A5,
TREES_1:def 9;
end;
assume r
in ((W
with-replacement (q,W2))
with-replacement (p,W1));
then r
in (W
with-replacement (q,W2)) & not p
is_a_proper_prefix_of r or ex r1 st r1
in W1 & r
= (p
^ r1) by
A5,
TREES_1:def 9;
then r
in W & not q
is_a_proper_prefix_of r & not p
is_a_proper_prefix_of r or (ex r2 st r2
in W2 & r
= (q
^ r2)) & not p
is_a_proper_prefix_of r or p
is_a_prefix_of r & ex r1 st r1
in W1 & r
= (p
^ r1) by
A2,
TREES_1: 1,
TREES_1:def 9;
then r
in (W
with-replacement (p,W1)) & not q
is_a_proper_prefix_of r or ex r1 st r1
in W2 & r
= (q
^ r1) by
A1,
A3,
Th2,
TREES_1:def 9;
hence thesis by
A6,
TREES_1:def 9;
end;
definition
let IT be
Tree;
::
TREES_2:def2
attr IT is
finite-order means ex n st for t be
Element of IT holds not (t
^
<*n*>)
in IT;
end
registration
cluster
finite-order for
Tree;
existence
proof
reconsider T =
{
{} } as
Tree;
take T,
0 ;
let t be
Element of T;
thus thesis by
TARSKI:def 1;
end;
end
definition
let W;
::
TREES_2:def3
mode
Chain of W ->
Subset of W means
:
Def3: for p, q st p
in it & q
in it holds (p,q)
are_c=-comparable ;
existence
proof
reconsider S =
{} as
Subset of W by
XBOOLE_1: 2;
take S;
let p, q;
thus thesis;
end;
::
TREES_2:def4
mode
Level of W ->
Subset of W means
:
Def4: ex n be
Nat st it
= { w : (
len w)
= n };
existence
proof
{}
in W by
TREES_1: 22;
then
reconsider L =
{
{} } as
Subset of W by
ZFMISC_1: 31;
take L,
0 ;
thus L
c= { w : (
len w)
=
0 }
proof
let x be
object;
assume
A1: x
in L;
then
A2: x
=
{} by
TARSKI:def 1;
(
len
{} )
=
0 ;
hence thesis by
A1,
A2;
end;
let x be
object;
assume x
in { w : (
len w)
=
0 };
then ex w st x
= w & (
len w)
=
0 ;
then x
=
{} ;
hence thesis by
TARSKI:def 1;
end;
let w;
::
TREES_2:def5
func
succ w ->
Subset of W equals { (w
^
<*n*>) : (w
^
<*n*>)
in W };
coherence
proof
{ (w
^
<*n*>) : (w
^
<*n*>)
in W }
c= W
proof
let x be
object;
assume x
in { (w
^
<*n*>) : (w
^
<*n*>)
in W };
then ex n st x
= (w
^
<*n*>) & (w
^
<*n*>)
in W;
hence thesis;
end;
hence thesis;
end;
end
theorem ::
TREES_2:9
for L be
Level of W holds L is
AntiChain_of_Prefixes of W
proof
let L be
Level of W;
consider n be
Nat such that
A1: L
= { w : (
len w)
= n } by
Def4;
L is
AntiChain_of_Prefixes-like
proof
thus for x st x
in L holds x is
FinSequence
proof
let x;
assume x
in L;
then x is
Element of W;
hence thesis;
end;
let v1, v2;
assume v1
in L;
then
A2: ex w1 be
Element of W st v1
= w1 & (
len w1)
= n by
A1;
assume v2
in L;
then ex w2 be
Element of W st v2
= w2 & (
len w2)
= n by
A1;
hence thesis by
A2,
TREES_1: 4;
end;
hence thesis by
TREES_1:def 11;
end;
theorem ::
TREES_2:10
(
succ w) is
AntiChain_of_Prefixes of W
proof
(
succ w) is
AntiChain_of_Prefixes-like
proof
thus for x st x
in (
succ w) holds x is
FinSequence
proof
let x;
assume x
in (
succ w);
then ex i st x
= (w
^
<*i*>) & (w
^
<*i*>)
in W;
hence thesis;
end;
let v1, v2;
assume v1
in (
succ w);
then
A1: ex k1 st v1
= (w
^
<*k1*>) & (w
^
<*k1*>)
in W;
assume v2
in (
succ w);
then
A2: ex k2 st v2
= (w
^
<*k2*>) & (w
^
<*k2*>)
in W;
A3: (
len v1)
= ((
len w)
+ 1) by
A1,
FINSEQ_2: 16;
(
len v2)
= ((
len w)
+ 1) by
A2,
FINSEQ_2: 16;
hence thesis by
A3,
TREES_1: 4;
end;
hence thesis by
TREES_1:def 11;
end;
theorem ::
TREES_2:11
for A be
AntiChain_of_Prefixes of W, C be
Chain of W holds ex w st (A
/\ C)
c=
{w}
proof
let A be
AntiChain_of_Prefixes of W, C be
Chain of W;
A1:
now
let p, q;
assume
A2: p
in (A
/\ C) & q
in (A
/\ C);
then
A3: p
in A & q
in A by
XBOOLE_0:def 4;
p
in C & q
in C by
A2,
XBOOLE_0:def 4;
then (p,q)
are_c=-comparable by
Def3;
hence p
= q by
A3,
TREES_1:def 10;
end;
set w = the
Element of W;
now
per cases ;
suppose (A
/\ C)
=
{} ;
then (A
/\ C)
c=
{w};
hence thesis;
end;
suppose
A4: (A
/\ C)
<>
{} ;
set x = the
Element of (A
/\ C);
x
in C by
A4,
XBOOLE_0:def 4;
then
reconsider x as
Element of W;
take x;
thus (A
/\ C)
c=
{x}
proof
let y be
object;
assume
A5: y
in (A
/\ C);
then y is
Element of W;
then
reconsider y9 = y as
FinSequence of
NAT ;
x
= y9 by
A1,
A5;
hence thesis by
TARSKI:def 1;
end;
end;
end;
hence thesis;
end;
definition
let W;
let n be
Nat;
::
TREES_2:def6
func W
-level n ->
Level of W equals { w : (
len w)
= n };
coherence
proof
defpred
X[
Element of W] means (
len $1)
= n;
{ w :
X[w] } is
Subset of W from
DOMAIN_1:sch 7;
hence thesis by
Def4;
end;
end
theorem ::
TREES_2:12
(w
^
<*n*>)
in (
succ w) iff (w
^
<*n*>)
in W;
theorem ::
TREES_2:13
w
=
{} implies (W
-level 1)
= (
succ w)
proof
assume
A1: w
=
{} ;
thus (W
-level 1)
c= (
succ w)
proof
let x be
object;
assume x
in (W
-level 1);
then
consider w9 such that
A2: x
= w9 and
A3: (
len w9)
= 1;
A4: w9
=
<*(w9
. 1)*> by
A3,
FINSEQ_1: 40;
then (
rng w9)
=
{(w9
. 1)} by
FINSEQ_1: 39;
then
reconsider n = (w9
. 1) as
Element of
NAT by
ZFMISC_1: 31;
w9
= (w
^
<*n*>) by
A1,
A4,
FINSEQ_1: 34;
hence thesis by
A2;
end;
let x be
object;
assume x
in (
succ w);
then
consider i such that
A5: x
= (w
^
<*i*>) and
A6: (w
^
<*i*>)
in W;
reconsider w9 = (w
^
<*i*>) as
Element of W by
A6;
(
len
<*i*>)
= 1 & w9
=
<*i*> by
A1,
FINSEQ_1: 34,
FINSEQ_1: 39;
hence thesis by
A5;
end;
theorem ::
TREES_2:14
Th14: W
= (
union the set of all (W
-level n))
proof
thus W
c= (
union the set of all (W
-level n))
proof
let x be
object;
assume x
in W;
then
reconsider w = x as
Element of W;
A1: x
in (W
-level (
len w));
(W
-level (
len w))
in the set of all (W
-level n);
hence thesis by
A1,
TARSKI:def 4;
end;
let x be
object;
assume x
in (
union the set of all (W
-level n));
then
consider X such that
A2: x
in X & X
in the set of all (W
-level n) by
TARSKI:def 4;
ex n st X
= (W
-level n) by
A2;
hence thesis by
A2;
end;
theorem ::
TREES_2:15
for W be
finite
Tree holds W
= (
union { (W
-level n) : n
<= (
height W) })
proof
let W be
finite
Tree;
thus W
c= (
union { (W
-level n) : n
<= (
height W) })
proof
let x be
object;
assume x
in W;
then
reconsider w = x as
Element of W;
A1: (
len w)
<= (
height W) by
TREES_1:def 12;
A2: w
in (W
-level (
len w));
(W
-level (
len w))
in { (W
-level n) : n
<= (
height W) } by
A1;
hence thesis by
A2,
TARSKI:def 4;
end;
let x be
object;
assume x
in (
union { (W
-level n) : n
<= (
height W) });
then
consider X such that
A3: x
in X & X
in { (W
-level n) : n
<= (
height W) } by
TARSKI:def 4;
ex n st X
= (W
-level n) & n
<= (
height W) by
A3;
hence thesis by
A3;
end;
theorem ::
TREES_2:16
for L be
Level of W holds ex n st L
= (W
-level n)
proof
let L be
Level of W;
consider n be
Nat such that
A1: L
= { w : (
len w)
= n } by
Def4;
reconsider n as
Nat;
take n;
thus thesis by
A1;
end;
scheme ::
TREES_2:sch2
FraenkelCard { A() -> non
empty
set , X() ->
set , F(
object) ->
set } :
(
card { F(w) where w be
Element of A() : w
in X() })
c= (
card X());
consider f such that
A1: (
dom f)
= X() & for x be
object st x
in X() holds (f
. x)
= F(x) from
FUNCT_1:sch 3;
{ F(w) where w be
Element of A() : w
in X() }
c= (
rng f)
proof
let x be
object;
assume x
in { F(w) where w be
Element of A() : w
in X() };
then
consider w be
Element of A() such that
A2: x
= F(w) and
A3: w
in X();
(f
. w)
= x by
A1,
A2,
A3;
hence thesis by
A1,
A3,
FUNCT_1:def 3;
end;
hence thesis by
A1,
CARD_1: 12;
end;
scheme ::
TREES_2:sch3
FraenkelFinCard { A() -> non
empty
set , X,Y() ->
finite
set , F(
set) ->
set } :
(
card Y())
<= (
card X())
provided
A1: Y()
= { F(w) where w be
Element of A() : w
in X() };
(
card { F(w) where w be
Element of A() : w
in X() })
c= (
card X()) from
FraenkelCard;
then (
Segm (
card Y()))
c= (
Segm (
card X())) by
A1;
hence thesis by
NAT_1: 39;
end;
theorem ::
TREES_2:17
Th17: W is
finite-order implies ex n st for w holds ex B be
finite
set st B
= (
succ w) & (
card B)
<= n
proof
given n such that
A1: for w holds not (w
^
<*n*>)
in W;
A2: (
Seg n) is
finite;
take n;
let w;
deffunc
U(
Real) = (w
^
<*($1
- 1)*>);
A3: {
U(r) where r be
Element of
REAL : r
in (
Seg n) } is
finite from
FRAENKEL:sch 21(
A2);
A4: (
succ w)
c= { (w
^
<*(r
- 1)*>) where r be
Element of
REAL : r
in (
Seg n) }
proof
let x be
object;
assume x
in (
succ w);
then
consider k such that
A5: x
= (w
^
<*k*>) and
A6: (w
^
<*k*>)
in W;
not (w
^
<*n*>)
in W by
A1;
then k
< n by
A6,
TREES_1:def 3;
then
A7: (k
+ 1)
<= n by
NAT_1: 13;
1
<= (k
+ 1) by
NAT_1: 11;
then
A8: (k
+ 1)
in (
Seg n) by
A7,
FINSEQ_1: 1;
A9: (k
+ 1)
in
REAL by
XREAL_0:def 1;
((k
+ 1)
- 1)
= k;
hence thesis by
A5,
A8,
A9;
end;
then
reconsider B = (
succ w) as
finite
set by
A3;
take B;
thus B
= (
succ w);
set C = {
U(r) where r be
Element of
REAL : r
in (
Seg n) };
C is
finite from
FRAENKEL:sch 21(
A2);
then
reconsider C as
finite
set;
A10: C
= {
U(r) where r be
Element of
REAL : r
in (
Seg n) };
(
card C)
<= (
card (
Seg n)) from
FraenkelFinCard(
A10);
then
A11: (
card C)
<= n by
FINSEQ_1: 57;
(
card B)
<= (
card C) by
A4,
NAT_1: 43;
hence thesis by
A11,
XXREAL_0: 2;
end;
theorem ::
TREES_2:18
Th18: W is
finite-order implies (
succ w) is
finite
proof
assume W is
finite-order;
then
consider n such that
A1: for w holds ex B be
finite
set st B
= (
succ w) & (
card B)
<= n by
Th17;
ex B be
finite
set st B
= (
succ w) & (
card B)
<= n by
A1;
hence thesis;
end;
registration
let W be
finite-order
Tree;
let w be
Element of W;
cluster (
succ w) ->
finite;
coherence by
Th18;
end
theorem ::
TREES_2:19
Th19:
{} is
Chain of W
proof
reconsider S =
{} as
Subset of W by
XBOOLE_1: 2;
S is
Chain of W
proof
let p, q;
thus thesis;
end;
hence thesis;
end;
theorem ::
TREES_2:20
Th20:
{
{} } is
Chain of W
proof
{}
in W by
TREES_1: 22;
then
reconsider S =
{
{} } as
Subset of W by
ZFMISC_1: 31;
S is
Chain of W
proof
let p, q;
assume that
A1: p
in S and
A2: q
in S;
p
=
{} by
A1,
TARSKI:def 1;
hence thesis by
A2,
TARSKI:def 1;
end;
hence thesis;
end;
registration
let W;
cluster non
empty for
Chain of W;
existence
proof
{
{} } is
Chain of W by
Th20;
hence thesis;
end;
end
definition
let W;
let IT be
Chain of W;
::
TREES_2:def7
attr IT is
Branch-like means
:
Def7: (for p st p
in IT holds (
ProperPrefixes p)
c= IT) & not ex p st p
in W & for q st q
in IT holds q
is_a_proper_prefix_of p;
end
registration
let W;
cluster
Branch-like for
Chain of W;
existence
proof
defpred
X[
set] means $1 is
Chain of W & for p st p
in $1 holds (
ProperPrefixes p)
c= $1;
consider X such that
A1: Y
in X iff Y
in (
bool W) &
X[Y] from
XFAMILY:sch 1;
{} is
Chain of W & for p st p
in
{} holds (
ProperPrefixes p)
c=
{} by
Th19;
then
A2: X
<>
{} by
A1;
now
let Z;
assume that Z
<>
{} and
A3: Z
c= X and
A4: Z is
c=-linear;
(
union Z)
c= W
proof
let x be
object;
assume x
in (
union Z);
then
consider Y such that
A5: x
in Y and
A6: Y
in Z by
TARSKI:def 4;
Y
in (
bool W) by
A1,
A3,
A6;
hence thesis by
A5;
end;
then
reconsider Z9 = (
union Z) as
Subset of W;
A7: Z9 is
Chain of W
proof
let p, q;
assume p
in Z9;
then
consider X1 such that
A8: p
in X1 and
A9: X1
in Z by
TARSKI:def 4;
assume q
in Z9;
then
consider X2 such that
A10: q
in X2 and
A11: X2
in Z by
TARSKI:def 4;
(X1,X2)
are_c=-comparable by
A4,
A9,
A11;
then
A12: X1
c= X2 or X2
c= X1;
A13: X1 is
Chain of W by
A1,
A3,
A9;
X2 is
Chain of W by
A1,
A3,
A11;
hence thesis by
A8,
A10,
A12,
A13,
Def3;
end;
now
let p;
assume p
in (
union Z);
then
consider X1 such that
A14: p
in X1 & X1
in Z by
TARSKI:def 4;
(
ProperPrefixes p)
c= X1 & X1
c= (
union Z) by
A1,
A3,
A14,
ZFMISC_1: 74;
hence (
ProperPrefixes p)
c= (
union Z);
end;
hence (
union Z)
in X by
A1,
A7;
end;
then
consider Y such that
A15: Y
in X and
A16: Z
in X & Z
<> Y implies not Y
c= Z by
A2,
ORDERS_1: 67;
reconsider Y as
Chain of W by
A1,
A15;
take Y;
thus for p st p
in Y holds (
ProperPrefixes p)
c= Y by
A1,
A15;
given p such that
A17: p
in W and
A18: for q st q
in Y holds q
is_a_proper_prefix_of p;
set Z = ((
ProperPrefixes p)
\/
{p});
(
ProperPrefixes p)
c= W &
{p}
c= W by
A17,
TREES_1:def 3,
ZFMISC_1: 31;
then
reconsider Z9 = Z as
Subset of W by
XBOOLE_1: 8;
A19: Z9 is
Chain of W
proof
let q, r;
assume that
A20: q
in Z9 and
A21: r
in Z9;
A22: q
in (
ProperPrefixes p) or q
in
{p} by
A20,
XBOOLE_0:def 3;
A23: r
in (
ProperPrefixes p) or r
in
{p} by
A21,
XBOOLE_0:def 3;
A24: q
is_a_proper_prefix_of p or q
= p by
A22,
TARSKI:def 1,
TREES_1: 12;
A25: r
is_a_proper_prefix_of p or r
= p by
A23,
TARSKI:def 1,
TREES_1: 12;
A26: q
is_a_prefix_of p by
A24;
r
is_a_prefix_of p by
A25;
hence thesis by
A26,
Th1;
end;
now
let q;
assume q
in Z;
then q
in (
ProperPrefixes p) or q
in
{p} by
XBOOLE_0:def 3;
then q
is_a_proper_prefix_of p or q
= p by
TARSKI:def 1,
TREES_1: 12;
then q
is_a_prefix_of p;
then
A27: (
ProperPrefixes q)
c= (
ProperPrefixes p) by
TREES_1: 17;
(
ProperPrefixes p)
c= Z by
XBOOLE_1: 7;
hence (
ProperPrefixes q)
c= Z by
A27;
end;
then
A28: Z
in X by
A1,
A19;
A29: p
in
{p} by
TARSKI:def 1;
A30: not p
in Y by
A18;
A31: p
in Z by
A29,
XBOOLE_0:def 3;
Y
c= Z
proof
let x be
object;
assume
A32: x
in Y;
then
reconsider t = x as
Element of W;
t
is_a_proper_prefix_of p by
A18,
A32;
then t
in (
ProperPrefixes p) by
TREES_1: 12;
hence thesis by
XBOOLE_0:def 3;
end;
hence thesis by
A16,
A28,
A30,
A31;
end;
end
definition
let W;
mode
Branch of W is
Branch-like
Chain of W;
end
registration
let W;
cluster
Branch-like -> non
empty for
Chain of W;
coherence
proof
let B be
Chain of W such that
A1: B is
Branch-like
empty;
set t = the
Element of W;
for q st q
in B holds q
is_a_proper_prefix_of t by
A1;
hence contradiction by
A1;
end;
end
reserve C for
Chain of W,
B for
Branch of W;
theorem ::
TREES_2:21
Th21: v1
in C & v2
in C implies v1
in (
ProperPrefixes v2) or v2
is_a_prefix_of v1
proof
assume
A1: v1
in C & v2
in C;
then
reconsider p = v1, q = v2 as
Element of W;
assume
A2: not v1
in (
ProperPrefixes v2);
A3: (p,q)
are_c=-comparable by
A1,
Def3;
A4: not v1
is_a_proper_prefix_of v2 by
A2,
TREES_1: 12;
v1
is_a_prefix_of v2 or v2
is_a_prefix_of v1 by
A3;
hence thesis by
A4;
end;
theorem ::
TREES_2:22
Th22: v1
in C & v2
in C & v
is_a_prefix_of v2 implies v1
in (
ProperPrefixes v) or v
is_a_prefix_of v1
proof
assume that
A1: v1
in C & v2
in C and
A2: v
is_a_prefix_of v2;
v1
in (
ProperPrefixes v2) or v2
is_a_prefix_of v1 by
A1,
Th21;
then v1
is_a_proper_prefix_of v2 or v
is_a_prefix_of v1 by
A2,
TREES_1: 12;
then (v,v1)
are_c=-comparable by
A2,
Th2;
then v
is_a_proper_prefix_of v1 or v
= v1 or v1
is_a_proper_prefix_of v;
hence thesis by
TREES_1: 12;
end;
registration
let W;
cluster
finite for
Chain of W;
existence
proof
reconsider C =
{} as
Chain of W by
Th19;
take C;
thus thesis;
end;
end
theorem ::
TREES_2:23
Th23: for C be
finite
Chain of W st (
card C)
> n holds ex p st p
in C & (
len p)
>= n
proof
let C be
finite
Chain of W;
defpred
X[
Nat] means $1
< (
card C) implies ex p st p
in C & (
len p)
>= $1;
A1:
X[
0 ]
proof
assume
A2:
0
< (
card C);
then
A3: C
<>
{} ;
set x = the
Element of C;
reconsider x as
Element of W by
A2,
CARD_1: 27,
TARSKI:def 3;
reconsider x as
FinSequence of
NAT ;
take x;
thus thesis by
A3;
end;
A4:
X[k] implies
X[(k
+ 1)]
proof
assume that
A5: k
< (
card C) implies ex p st p
in C & (
len p)
>= k and
A6: (k
+ 1)
< (
card C);
A7: k
<= (k
+ 1) by
NAT_1: 11;
then
A8: k
< (
card C) by
A6,
XXREAL_0: 2;
consider p such that
A9: p
in C and
A10: (
len p)
>= k by
A5,
A6,
A7,
XXREAL_0: 2;
reconsider q = (p
| (
Seg k)) as
FinSequence by
FINSEQ_1: 15;
A11: (
len q)
= k by
A10,
FINSEQ_1: 17;
then
A12: (
card (
ProperPrefixes q))
= k by
TREES_1: 35;
then (
card (
ProperPrefixes q))
in (
Segm (
card C)) by
A8,
NAT_1: 44;
then
A13: (C
\ (
ProperPrefixes q))
<>
{} by
CARD_1: 68;
set x = the
Element of (C
\ (
ProperPrefixes q));
A14: x
in C by
A13,
XBOOLE_0:def 5;
A15: not x
in (
ProperPrefixes q) by
A13,
XBOOLE_0:def 5;
reconsider x as
Element of W by
A14;
(
card ((
ProperPrefixes q)
\/
{x}))
= (k
+ 1) by
A12,
A15,
CARD_2: 41;
then (
card ((
ProperPrefixes q)
\/
{x}))
in (
Segm (
card C)) by
A6,
NAT_1: 44;
then
A16: (C
\ ((
ProperPrefixes q)
\/
{x}))
<>
{} by
CARD_1: 68;
set y = the
Element of (C
\ ((
ProperPrefixes q)
\/
{x}));
A17: y
in C by
A16,
XBOOLE_0:def 5;
A18: not y
in ((
ProperPrefixes q)
\/
{x}) by
A16,
XBOOLE_0:def 5;
reconsider y as
Element of W by
A17;
A19: not y
in (
ProperPrefixes q) by
A18,
XBOOLE_0:def 3;
A20: not y
in
{x} by
A18,
XBOOLE_0:def 3;
A21: q
is_a_prefix_of p;
then
A22: q
is_a_prefix_of x by
A9,
A14,
A15,
Th22;
A23: q
is_a_prefix_of y by
A9,
A17,
A19,
A21,
Th22;
A24: x
<> y by
A20,
TARSKI:def 1;
q
is_a_proper_prefix_of y or q
is_a_proper_prefix_of x by
A22,
A23,
A24;
then k
< (
len x) or k
< (
len y) by
A11,
TREES_1: 6;
then (k
+ 1)
<= (
len x) or (k
+ 1)
<= (
len y) by
NAT_1: 13;
hence thesis by
A14,
A17;
end;
X[k] from
NAT_1:sch 2(
A1,
A4);
hence thesis;
end;
theorem ::
TREES_2:24
Th24: for C holds { w : ex p st p
in C & w
is_a_prefix_of p } is
Chain of W
proof
let C;
{ w : ex p st p
in C & w
is_a_prefix_of p }
c= W
proof
let x be
object;
assume x
in { w : ex p st p
in C & w
is_a_prefix_of p };
then ex w st x
= w & ex p st p
in C & w
is_a_prefix_of p;
hence thesis;
end;
then
reconsider Z = { w : ex p st p
in C & w
is_a_prefix_of p } as
Subset of W;
Z is
Chain of W
proof
let p, q;
assume p
in Z;
then ex w st p
= w & ex p st p
in C & w
is_a_prefix_of p;
then
consider r1 such that
A1: r1
in C and
A2: p
is_a_prefix_of r1;
assume q
in Z;
then ex w9 st q
= w9 & ex p st p
in C & w9
is_a_prefix_of p;
then
consider r2 such that
A3: r2
in C and
A4: q
is_a_prefix_of r2;
(r1,r2)
are_c=-comparable by
A1,
A3,
Def3;
then r1
is_a_prefix_of r2 or r2
is_a_prefix_of r1;
then p
is_a_prefix_of r2 or q
is_a_prefix_of r1 by
A2,
A4;
hence thesis by
A2,
A4,
Th1;
end;
hence thesis;
end;
theorem ::
TREES_2:25
Th25: p
is_a_prefix_of q & q
in B implies p
in B
proof
assume p
is_a_prefix_of q;
then p
is_a_proper_prefix_of q or p
= q;
then
A1: p
in (
ProperPrefixes q) or p
= q by
TREES_1:def 2;
assume
A2: q
in B;
then (
ProperPrefixes q)
c= B by
Def7;
hence thesis by
A1,
A2;
end;
theorem ::
TREES_2:26
Th26:
{}
in B
proof
set x = the
Element of B;
reconsider x as
Element of W;
(
<*>
NAT )
is_a_prefix_of x;
hence thesis by
Th25;
end;
theorem ::
TREES_2:27
Th27: p
in C & q
in C & (
len p)
<= (
len q) implies p
is_a_prefix_of q
proof
assume p
in C & q
in C & (
len p)
<= (
len q) & not p
is_a_prefix_of q;
then q
in (
ProperPrefixes p) & not q
is_a_proper_prefix_of p by
Th21,
TREES_1: 6;
hence contradiction by
TREES_1: 12;
end;
theorem ::
TREES_2:28
Th28: ex B st C
c= B
proof
defpred
X[
set] means $1 is
Chain of W & C
c= $1 & for p st p
in $1 holds (
ProperPrefixes p)
c= $1;
consider X such that
A1: Y
in X iff Y
in (
bool W) &
X[Y] from
XFAMILY:sch 1;
set Z = { w : ex p st p
in C & w
is_a_prefix_of p };
A2: Z is
Chain of W by
Th24;
A3: C
c= Z
proof
let x be
object;
assume
A4: x
in C;
then
reconsider w = x as
Element of W;
w
is_a_prefix_of w;
hence thesis by
A4;
end;
now
let p;
assume p
in Z;
then
A5: ex w st p
= w & ex p st p
in C & w
is_a_prefix_of p;
then
consider q such that
A6: q
in C and
A7: p
is_a_prefix_of q;
thus (
ProperPrefixes p)
c= Z
proof
let x be
object;
assume x
in (
ProperPrefixes p);
then
consider r be
FinSequence such that
A8: x
= r and
A9: r
is_a_proper_prefix_of p by
TREES_1:def 2;
r
is_a_prefix_of p by
A9;
then r
is_a_prefix_of q & r
in W by
A5,
A7,
TREES_1: 20;
hence thesis by
A6,
A8;
end;
end;
then
A10: X
<>
{} by
A1,
A2,
A3;
now
let Z;
assume that
A11: Z
<>
{} and
A12: Z
c= X and
A13: Z is
c=-linear;
(
union Z)
c= W
proof
let x be
object;
assume x
in (
union Z);
then
consider Y such that
A14: x
in Y and
A15: Y
in Z by
TARSKI:def 4;
Y
in (
bool W) by
A1,
A12,
A15;
hence thesis by
A14;
end;
then
reconsider Z9 = (
union Z) as
Subset of W;
A16: Z9 is
Chain of W
proof
let p, q;
assume p
in Z9;
then
consider X1 such that
A17: p
in X1 and
A18: X1
in Z by
TARSKI:def 4;
assume q
in Z9;
then
consider X2 such that
A19: q
in X2 and
A20: X2
in Z by
TARSKI:def 4;
(X1,X2)
are_c=-comparable by
A13,
A18,
A20;
then
A21: X1
c= X2 or X2
c= X1;
A22: X1 is
Chain of W by
A1,
A12,
A18;
X2 is
Chain of W by
A1,
A12,
A20;
hence thesis by
A17,
A19,
A21,
A22,
Def3;
end;
A23:
now
let p;
assume p
in (
union Z);
then
consider X1 such that
A24: p
in X1 & X1
in Z by
TARSKI:def 4;
(
ProperPrefixes p)
c= X1 & X1
c= (
union Z) by
A1,
A12,
A24,
ZFMISC_1: 74;
hence (
ProperPrefixes p)
c= (
union Z);
end;
set x = the
Element of Z;
x
in X by
A11,
A12;
then
A25: C
c= x by
A1;
x
c= (
union Z) by
A11,
ZFMISC_1: 74;
then C
c= (
union Z) by
A25;
hence (
union Z)
in X by
A1,
A16,
A23;
end;
then
consider Y such that
A26: Y
in X and
A27: for Z st Z
in X & Z
<> Y holds not Y
c= Z by
A10,
ORDERS_1: 67;
reconsider Y as
Chain of W by
A1,
A26;
now
thus for p st p
in Y holds (
ProperPrefixes p)
c= Y by
A1,
A26;
given p such that
A28: p
in W and
A29: for q st q
in Y holds q
is_a_proper_prefix_of p;
set Z = ((
ProperPrefixes p)
\/
{p});
(
ProperPrefixes p)
c= W &
{p}
c= W by
A28,
TREES_1:def 3,
ZFMISC_1: 31;
then
reconsider Z9 = Z as
Subset of W by
XBOOLE_1: 8;
A30: Z9 is
Chain of W
proof
let q, r;
assume that
A31: q
in Z9 and
A32: r
in Z9;
A33: q
in (
ProperPrefixes p) or q
in
{p} by
A31,
XBOOLE_0:def 3;
A34: r
in (
ProperPrefixes p) or r
in
{p} by
A32,
XBOOLE_0:def 3;
A35: q
is_a_proper_prefix_of p or q
= p by
A33,
TARSKI:def 1,
TREES_1: 12;
A36: r
is_a_proper_prefix_of p or r
= p by
A34,
TARSKI:def 1,
TREES_1: 12;
A37: q
is_a_prefix_of p by
A35;
r
is_a_prefix_of p by
A36;
hence thesis by
A37,
Th1;
end;
A38:
now
let q;
assume q
in Z;
then q
in (
ProperPrefixes p) or q
in
{p} by
XBOOLE_0:def 3;
then q
is_a_proper_prefix_of p or q
= p by
TARSKI:def 1,
TREES_1: 12;
then q
is_a_prefix_of p;
then
A39: (
ProperPrefixes q)
c= (
ProperPrefixes p) by
TREES_1: 17;
(
ProperPrefixes p)
c= Z by
XBOOLE_1: 7;
hence (
ProperPrefixes q)
c= Z by
A39;
end;
A40: Y
c= Z
proof
let x be
object;
assume
A41: x
in Y;
then
reconsider t = x as
Element of W;
t
is_a_proper_prefix_of p by
A29,
A41;
then t
in (
ProperPrefixes p) by
TREES_1: 12;
hence thesis by
XBOOLE_0:def 3;
end;
C
c= Y by
A1,
A26;
then C
c= Z by
A40;
then
A42: Z
in X by
A1,
A30,
A38;
A43: p
in
{p} by
TARSKI:def 1;
A44: not p
in Y by
A29;
p
in Z by
A43,
XBOOLE_0:def 3;
hence contradiction by
A27,
A40,
A42,
A44;
end;
then
reconsider Y as
Branch of W by
Def7;
take Y;
thus thesis by
A1,
A26;
end;
scheme ::
TREES_2:sch4
FuncExOfMinNat { P[
object,
Nat], X() ->
set } :
ex f st (
dom f)
= X() & for x be
object st x
in X() holds ex n st (f
. x)
= n & P[x, n] & for m st P[x, m] holds n
<= m
provided
A1: for x be
object st x
in X() holds ex n st P[x, n];
defpred
Q[
object,
object] means ex n st $2
= n & P[$1, n] & for m st P[$1, m] holds n
<= m;
A2: for x be
object st x
in X() holds ex y be
object st
Q[x, y]
proof
let x be
object;
defpred
X[
Nat] means P[x, $1];
assume x
in X();
then ex n st
X[n] by
A1;
then
A3: ex n be
Nat st
X[n];
consider n be
Nat such that
A4:
X[n] & for m be
Nat st
X[m] holds n
<= m from
NAT_1:sch 5(
A3);
take n;
thus thesis by
A4;
end;
thus ex f st (
dom f)
= X() & for x be
object st x
in X() holds
Q[x, (f
. x)] from
CLASSES1:sch 1(
A2);
end;
Lm1: X is
finite implies ex n st for k st k
in X holds k
<= n
proof
assume
A1: X is
finite;
defpred
P[
object,
object] means ex k1,k2 be
Nat st $1
= k1 & $2
= k2 & k1
>= k2;
now
per cases ;
suppose
A2: (X
/\
NAT )
=
{} ;
thus thesis
proof
take
0 ;
let k;
A3: k
in
NAT by
ORDINAL1:def 12;
assume k
in X;
hence thesis by
A2,
XBOOLE_0:def 4,
A3;
end;
end;
suppose
A4: (X
/\
NAT )
<>
{} ;
reconsider XN = (X
/\
NAT ) as
finite
set by
A1;
A5: XN
<>
{} by
A4;
A6: for x,y be
object holds
P[x, y] &
P[y, x] implies x
= y by
XXREAL_0: 1;
A7: for x,y,z be
object st
P[x, y] &
P[y, z] holds
P[x, z] by
XXREAL_0: 2;
consider x be
object such that
A8: x
in XN & for y be
object st y
in XN & y
<> x holds not
P[y, x] from
CARD_2:sch 1(
A5,
A6,
A7);
x
in
NAT by
A8,
XBOOLE_0:def 4;
then
reconsider n = x as
Nat;
take n;
let k;
A9: k
in
NAT by
ORDINAL1:def 12;
assume k
in X;
then k
in (X
/\
NAT ) by
XBOOLE_0:def 4,
A9;
hence k
<= n by
A8;
end;
end;
hence thesis;
end;
scheme ::
TREES_2:sch5
InfiniteChain { X() ->
set , a() ->
object , Q[
object], P[
object,
object] } :
ex f st (
dom f)
=
NAT & (
rng f)
c= X() & (f
.
0 )
= a() & for k holds P[(f
. k), (f
. (k
+ 1))] & Q[(f
. k)]
provided
A1: a()
in X() & Q[a()]
and
A2: for x be
object st x
in X() & Q[x] holds ex y be
object st y
in X() & P[x, y] & Q[y];
consider Y such that
A3: for x be
object holds x
in Y iff x
in X() & Q[x] from
XBOOLE_0:sch 1;
defpred
Q[
object,
object] means $2
in Y & P[$1, $2];
A4: for x be
object st x
in Y holds ex y be
object st
Q[x, y]
proof
let x be
object;
assume x
in Y;
then x
in X() & Q[x] by
A3;
then
consider y be
object such that
A5: y
in X() & P[x, y] & Q[y] by
A2;
take y;
thus thesis by
A3,
A5;
end;
consider g be
Function such that
A6: (
dom g)
= Y & for x be
object st x
in Y holds
Q[x, (g
. x)] from
CLASSES1:sch 1(
A4);
deffunc
U(
set,
set) = (g
. $2);
consider f such that
A7: (
dom f)
=
NAT & (f
.
0 )
= a() & for n be
Nat holds (f
. (n
+ 1))
=
U(n,.) from
NAT_1:sch 11;
take f;
thus (
dom f)
=
NAT by
A7;
defpred
X[
Nat] means (f
. $1)
in Y;
A8:
X[
0 ] by
A1,
A3,
A7;
A9:
X[k] implies
X[(k
+ 1)]
proof
assume (f
. k)
in Y;
then (g
. (f
. k))
in Y by
A6;
hence thesis by
A7;
end;
A10:
X[k] from
NAT_1:sch 2(
A8,
A9);
thus (
rng f)
c= X()
proof
let x be
object;
assume x
in (
rng f);
then
consider y be
object such that
A11: y
in (
dom f) and
A12: x
= (f
. y) by
FUNCT_1:def 3;
reconsider y as
Nat by
A7,
A11;
(f
. y)
in Y by
A10;
hence thesis by
A3,
A12;
end;
thus (f
.
0 )
= a() by
A7;
let k;
A13: (f
. k)
in Y by
A10;
then P[(f
. k), (g
. (f
. k))] by
A6;
hence thesis by
A3,
A7,
A13;
end;
theorem ::
TREES_2:29
Th29: for T be
Tree st (for n holds ex C be
finite
Chain of T st (
card C)
= n) & for t be
Element of T holds (
succ t) is
finite holds ex B be
Chain of T st not B is
finite
proof
let T be
Tree;
assume that
A1: for n holds ex X be
finite
Chain of T st (
card X)
= n and
A2: for t be
Element of T holds (
succ t) is
finite;
defpred
P[
FinSequence] means for n holds ex B be
Branch of T st $1
in B & ex p st p
in B & (
len p)
>= ((
len $1)
+ n);
A3: for x be
Element of T st
P[x] holds ex n st (x
^
<*n*>)
in T &
P[(x
^
<*n*>)]
proof
let x be
Element of T such that
A4:
P[x] and
A5: for n st (x
^
<*n*>)
in T holds not
P[(x
^
<*n*>)];
A6: (
succ x) is
finite by
A2;
defpred
X[
object,
Nat] means for B be
Branch of T, p, q st p
= $1 & $1
in B & q
in B holds ((
len p)
+ $2)
> (
len q);
A7: for y be
object st y
in (
succ x) holds ex n st
X[y, n]
proof
let y be
object;
assume y
in (
succ x);
then
consider k such that
A8: y
= (x
^
<*k*>) and
A9: (x
^
<*k*>)
in T;
consider n such that
A10: for B be
Branch of T st (x
^
<*k*>)
in B holds for p st p
in B holds (
len p)
< ((
len (x
^
<*k*>))
+ n) by
A5,
A9;
take n;
thus thesis by
A8,
A10;
end;
consider f such that
A11: (
dom f)
= (
succ x) and
A12: for y be
object st y
in (
succ x) holds ex n st (f
. y)
= n &
X[y, n] & for m st
X[y, m] holds n
<= m from
FuncExOfMinNat(
A7);
consider k such that
A13: for m st m
in (
rng f) holds m
<= k by
A6,
A11,
Lm1,
FINSET_1: 8;
consider B be
Branch of T such that
A14: x
in B and
A15: ex p st p
in B & (
len p)
>= ((
len x)
+ (k
+ 1)) by
A4;
consider p such that
A16: p
in B and
A17: (
len p)
>= ((
len x)
+ (k
+ 1)) by
A15;
reconsider r = (p
| (
Seg ((
len x)
+ 1))) as
FinSequence of
NAT by
FINSEQ_1: 18;
((
len x)
+ 1)
<= (((
len x)
+ 1)
+ k) by
NAT_1: 11;
then
A18: (
len p)
>= ((
len x)
+ 1) by
A17,
XXREAL_0: 2;
A19: r
is_a_prefix_of p;
A20: (
len r)
= ((
len x)
+ 1) by
A18,
FINSEQ_1: 17;
A21: r
in B by
A16,
A19,
Th25;
then x
is_a_prefix_of r by
A14,
A20,
Th27,
NAT_1: 11;
then
consider j be
FinSequence such that
A22: r
= (x
^ j) by
TREES_1: 1;
((
len x)
+ (
len j))
= (
len r) by
A22,
FINSEQ_1: 22;
then
A23: j
=
<*(j
. 1)*> by
A20,
FINSEQ_1: 40;
A24: (
dom r)
= (
Seg (
len r)) & 1
<= (1
+ (
len x)) by
FINSEQ_1:def 3,
NAT_1: 11;
((
len x)
+ 1)
<= (
len r) by
A18,
FINSEQ_1: 17;
then ((x
^
<*(j
. 1)*>)
. ((
len x)
+ 1))
= (j
. 1) & ((
len x)
+ 1)
in (
dom r) by
A24,
FINSEQ_1: 1,
FINSEQ_1: 42;
then (j
. 1)
in (
rng r) by
A22,
A23,
FUNCT_1:def 3;
then
reconsider l = (j
. 1) as
Nat;
A25: (x
^
<*l*>)
in (
succ x) by
A21,
A22,
A23;
then
consider n such that
A26: (f
. (x
^
<*l*>))
= n and
A27: for B be
Branch of T, p, q st p
= (x
^
<*l*>) & (x
^
<*l*>)
in B & q
in B holds ((
len p)
+ n)
> (
len q) and for m st for B be
Branch of T, p, q st p
= (x
^
<*l*>) & (x
^
<*l*>)
in B & q
in B holds ((
len p)
+ m)
> (
len q) holds n
<= m by
A12;
n
in (
rng f) by
A11,
A25,
A26,
FUNCT_1:def 3;
then n
<= k by
A13;
then ((
len r)
+ n)
<= (((
len x)
+ 1)
+ k) by
A20,
XREAL_1: 7;
hence contradiction by
A16,
A17,
A21,
A22,
A23,
A27,
XXREAL_0: 2;
end;
reconsider e =
{} as
Element of T by
TREES_1: 22;
A28:
P[e]
proof
given n such that
A29: for B be
Branch of T st e
in B holds for p st p
in B holds (
len p)
< ((
len e)
+ n);
consider C be
finite
Chain of T such that
A30: (
card C)
= (n
+ 1) by
A1;
consider B be
Branch of T such that
A31: C
c= B by
Th28;
(n
+
0 )
< (n
+ 1) by
XREAL_1: 6;
then
A32: ex p st p
in C & (
len p)
>= n by
A30,
Th23;
e
in B & (
len e)
=
0 by
Th26;
hence contradiction by
A29,
A31,
A32;
end;
defpred
QQ[
object] means ex t be
Element of T st t
= $1 &
P[t];
defpred
PP[
object,
object] means ex p, n st $1
= p & (p
^
<*n*>)
in T & $2
= (p
^
<*n*>);
A33: e
in T &
QQ[e] by
A28;
A34: for x be
object st x
in T &
QQ[x] holds ex y be
object st y
in T &
PP[x, y] &
QQ[y]
proof
let x be
object such that x
in T;
given t be
Element of T such that
A35: t
= x and
A36:
P[t];
consider n such that
A37: (t
^
<*n*>)
in T and
A38:
P[(t
^
<*n*>)] by
A3,
A36;
reconsider y = (t
^
<*n*>) as
set;
take y;
thus y
in T &
PP[x, y] by
A35,
A37;
reconsider t1 = (t
^
<*n*>) as
Element of T by
A37;
take t1;
thus thesis by
A38;
end;
ex f st (
dom f)
=
NAT & (
rng f)
c= T & (f
.
0 )
= e & for k holds
PP[(f
. k), (f
. (k
+ 1))] &
QQ[(f
. k)] from
InfiniteChain(
A33,
A34);
then
consider f such that
A39: (
dom f)
=
NAT and
A40: (
rng f)
c= T and
A41: (f
.
0 )
= e and
A42: for k holds (ex p, n st (f
. k)
= p & (p
^
<*n*>)
in T & (f
. (k
+ 1))
= (p
^
<*n*>)) & ex t be
Element of T st t
= (f
. k) &
P[t];
reconsider C = (
rng f) as
Subset of T by
A40;
A43:
now
let k be
Nat;
defpred
X[
Nat] means for p, q st p
= (f
. k) & q
= (f
. (k
+ $1)) holds p
is_a_prefix_of q;
A44:
X[
0 ];
A45: for n be
Nat st
X[n] holds
X[(n
+ 1)]
proof
let n be
Nat;
assume
A46: for p, q st p
= (f
. k) & q
= (f
. (k
+ n)) holds p
is_a_prefix_of q;
let p, q such that
A47: p
= (f
. k) and
A48: q
= (f
. (k
+ (n
+ 1)));
reconsider k, n as
Nat;
consider r, l such that
A49: (f
. (k
+ n))
= r and (r
^
<*l*>)
in T and
A50: (f
. ((k
+ n)
+ 1))
= (r
^
<*l*>) by
A42;
A51: p
is_a_prefix_of r by
A46,
A47,
A49;
r
is_a_prefix_of (r
^
<*l*>) by
TREES_1: 1;
hence thesis by
A48,
A50,
A51;
end;
thus for n be
Nat holds
X[n] from
NAT_1:sch 2(
A44,
A45);
end;
A52:
now
let k, l;
assume k
<= l;
then ex n be
Nat st l
= (k
+ n) by
NAT_1: 10;
hence for p, q st p
= (f
. k) & q
= (f
. l) holds p
is_a_prefix_of q by
A43;
end;
C is
Chain of T
proof
let p, q;
assume that
A53: p
in C and
A54: q
in C;
consider x be
object such that
A55: x
in
NAT and
A56: p
= (f
. x) by
A39,
A53,
FUNCT_1:def 3;
consider y be
object such that
A57: y
in
NAT and
A58: q
= (f
. y) by
A39,
A54,
FUNCT_1:def 3;
reconsider x, y as
Nat by
A55,
A57;
x
<= y or y
<= x;
hence p
is_a_prefix_of q or q
is_a_prefix_of p by
A52,
A56,
A58;
end;
then
reconsider C as
Chain of T;
take C;
defpred
X[
Nat] means for p st p
= (f
. $1) holds (
len p)
= $1;
A59:
X[
0 ] by
A41;
A60:
X[k] implies
X[(k
+ 1)]
proof
assume
A61: for p st p
= (f
. k) holds (
len p)
= k;
let p such that
A62: p
= (f
. (k
+ 1));
consider q, n such that
A63: (f
. k)
= q and (q
^
<*n*>)
in T and
A64: (f
. (k
+ 1))
= (q
^
<*n*>) by
A42;
thus (
len p)
= ((
len q)
+ (
len
<*n*>)) by
A62,
A64,
FINSEQ_1: 22
.= ((
len q)
+ 1) by
FINSEQ_1: 39
.= (k
+ 1) by
A61,
A63;
end;
A65:
X[k] from
NAT_1:sch 2(
A59,
A60);
f is
one-to-one
proof
let x,y be
object;
assume x
in (
dom f) & y
in (
dom f);
then
reconsider x9 = x, y9 = y as
Nat by
A39;
consider p, n such that
A66: (f
. x9)
= p and (p
^
<*n*>)
in T and (f
. (x9
+ 1))
= (p
^
<*n*>) by
A42;
A67: ex q, k st (f
. y9)
= q & (q
^
<*k*>)
in T & (f
. (y9
+ 1))
= (q
^
<*k*>) by
A42;
(
len p)
= x9 by
A65,
A66;
hence thesis by
A65,
A66,
A67;
end;
then (
NAT ,C)
are_equipotent by
A39,
WELLORD2:def 4;
hence thesis by
CARD_1: 38;
end;
::$Notion-Name
theorem ::
TREES_2:30
for T be
finite-order
Tree st for n holds ex C be
finite
Chain of T st (
card C)
= n holds ex B be
Chain of T st not B is
finite
proof
let T be
finite-order
Tree;
for t be
Element of T holds (
succ t) is
finite;
hence thesis by
Th29;
end;
definition
let IT be
Relation;
::
TREES_2:def8
attr IT is
DecoratedTree-like means
:
Def8: (
dom IT) is
Tree;
end
registration
cluster
DecoratedTree-like for
Function;
existence
proof
set W = the
Tree;
take f = (W
-->
0 );
thus (
dom f) is
Tree;
end;
end
definition
mode
DecoratedTree is
DecoratedTree-like
Function;
end
reserve T,T1,T2 for
DecoratedTree;
registration
let T;
cluster (
dom T) -> non
empty
Tree-like;
coherence by
Def8;
end
registration
let D;
cluster
DecoratedTree-likeD
-valued for
Function;
existence
proof
set W = the
Tree;
set d = the
Element of D;
set f = (W
--> d);
(
dom f)
= W;
then
reconsider f as
DecoratedTree by
Def8;
f is D
-valued;
hence thesis;
end;
end
definition
let D;
mode
DecoratedTree of D is D
-valued
DecoratedTree;
end
definition
let D be non
empty
set, T be
DecoratedTree of D, t be
Element of (
dom T);
:: original:
.
redefine
func T
. t ->
Element of D ;
coherence
proof
(T
. t)
in (
rng T) & (
rng T)
c= D by
FUNCT_1:def 3;
hence thesis;
end;
end
theorem ::
TREES_2:31
Th31: (
dom T1)
= (
dom T2) & (for p st p
in (
dom T1) holds (T1
. p)
= (T2
. p)) implies T1
= T2
proof
assume that
A1: (
dom T1)
= (
dom T2) and
A2: for p st p
in (
dom T1) holds (T1
. p)
= (T2
. p);
now
let x be
object;
assume x
in (
dom T1);
then
reconsider p = x as
Element of (
dom T1);
(T1
. p)
= (T2
. p) by
A2;
hence (T1
. x)
= (T2
. x);
end;
hence thesis by
A1;
end;
scheme ::
TREES_2:sch6
DTreeEx { T() ->
Tree , P[
object,
object] } :
ex T st (
dom T)
= T() & for p st p
in T() holds P[p, (T
. p)]
provided
A1: for p st p
in T() holds ex x st P[p, x];
A2: for x be
object st x
in T() holds ex y be
object st P[x, y]
proof
let x be
object;
assume x
in T();
then
reconsider p = x as
Element of T();
ex y st P[p, y] by
A1;
hence thesis;
end;
consider f such that
A3: (
dom f)
= T() & for x be
object st x
in T() holds P[x, (f
. x)] from
CLASSES1:sch 1(
A2);
reconsider T = f as
DecoratedTree by
A3,
Def8;
take T;
thus thesis by
A3;
end;
scheme ::
TREES_2:sch7
DTreeLambda { T() ->
Tree , f(
object) ->
set } :
ex T st (
dom T)
= T() & for p st p
in T() holds (T
. p)
= f(p);
consider f such that
A1: (
dom f)
= T() & for x be
object st x
in T() holds (f
. x)
= f(x) from
FUNCT_1:sch 3;
reconsider T = f as
DecoratedTree by
A1,
Def8;
take T;
thus thesis by
A1;
end;
definition
let T;
::
TREES_2:def9
func
Leaves T ->
set equals (T
.: (
Leaves (
dom T)));
correctness ;
let p;
::
TREES_2:def10
func T
| p ->
DecoratedTree means
:
Def10: (
dom it )
= ((
dom T)
| p) & for q st q
in ((
dom T)
| p) holds (it
. q)
= (T
. (p
^ q));
existence
proof
deffunc
U(
FinSequence) = (T
. (p
^ $1));
thus ex t be
DecoratedTree st (
dom t)
= ((
dom T)
| p) & for q st q
in ((
dom T)
| p) holds (t
. q)
=
U(q) from
DTreeLambda;
end;
uniqueness
proof
let T1, T2 such that
A1: (
dom T1)
= ((
dom T)
| p) and
A2: for q st q
in ((
dom T)
| p) holds (T1
. q)
= (T
. (p
^ q)) and
A3: (
dom T2)
= ((
dom T)
| p) and
A4: for q st q
in ((
dom T)
| p) holds (T2
. q)
= (T
. (p
^ q));
now
let q;
assume
A5: q
in ((
dom T)
| p);
then (T1
. q)
= (T
. (p
^ q)) by
A2;
hence (T1
. q)
= (T2
. q) by
A4,
A5;
end;
hence thesis by
A1,
A3,
Th31;
end;
end
theorem ::
TREES_2:32
Th32: p
in (
dom T) implies (
rng (T
| p))
c= (
rng T)
proof
assume
A1: p
in (
dom T);
let x be
object;
assume x
in (
rng (T
| p));
then
consider y be
object such that
A2: y
in (
dom (T
| p)) and
A3: x
= ((T
| p)
. y) by
FUNCT_1:def 3;
reconsider y as
Element of (
dom (T
| p)) by
A2;
A4: (
dom (T
| p))
= ((
dom T)
| p) by
Def10;
then
A5: (p
^ y)
in (
dom T) by
A1,
TREES_1:def 6;
x
= (T
. (p
^ y)) by
A3,
A4,
Def10;
hence thesis by
A5,
FUNCT_1:def 3;
end;
definition
let D;
let T be
DecoratedTree of D;
:: original:
Leaves
redefine
func
Leaves T ->
Subset of D ;
coherence
proof
(T
.: (
Leaves (
dom T)))
c= (
rng T) & (
rng T)
c= D by
RELAT_1: 111;
hence thesis by
XBOOLE_1: 1;
end;
end
registration
let D;
let T be
DecoratedTree of D;
let p be
Element of (
dom T);
cluster (T
| p) -> D
-valued;
coherence
proof
(
rng (T
| p))
c= (
rng T) & (
rng T)
c= D by
Th32;
then (
rng (T
| p))
c= D;
hence thesis;
end;
end
definition
let T, p, T1;
assume
A1: p
in (
dom T);
::
TREES_2:def11
func T
with-replacement (p,T1) ->
DecoratedTree means (
dom it )
= ((
dom T)
with-replacement (p,(
dom T1))) & for q st q
in ((
dom T)
with-replacement (p,(
dom T1))) holds not p
is_a_prefix_of q & (it
. q)
= (T
. q) or ex r st r
in (
dom T1) & q
= (p
^ r) & (it
. q)
= (T1
. r);
existence
proof
defpred
X[
FinSequence,
set] means not p
is_a_prefix_of $1 & $2
= (T
. $1) or ex r st r
in (
dom T1) & $1
= (p
^ r) & $2
= (T1
. r);
A2: for q st q
in ((
dom T)
with-replacement (p,(
dom T1))) holds ex x st
X[q, x]
proof
let q such that
A3: q
in ((
dom T)
with-replacement (p,(
dom T1)));
now
per cases ;
suppose p
is_a_proper_prefix_of q;
then
consider r such that
A4: r
in (
dom T1) & q
= (p
^ r) by
A1,
A3,
TREES_1:def 9;
thus thesis
proof
take (T1
. r);
thus thesis by
A4;
end;
end;
suppose
A5: p
= q;
thus thesis
proof
take (T1
. (
{}
NAT ));
(
{}
NAT )
in (
dom T1) & q
= (p
^ (
<*>
NAT )) by
A5,
FINSEQ_1: 34,
TREES_1: 22;
hence thesis;
end;
end;
suppose not p
is_a_prefix_of q;
hence thesis;
end;
end;
hence thesis;
end;
thus ex TT be
DecoratedTree st (
dom TT)
= ((
dom T)
with-replacement (p,(
dom T1))) & for q st q
in ((
dom T)
with-replacement (p,(
dom T1))) holds
X[q, (TT
. q)] from
DTreeEx(
A2);
end;
uniqueness
proof
let D1,D2 be
DecoratedTree such that
A6: (
dom D1)
= ((
dom T)
with-replacement (p,(
dom T1))) and
A7: for q st q
in ((
dom T)
with-replacement (p,(
dom T1))) holds not p
is_a_prefix_of q & (D1
. q)
= (T
. q) or ex r st r
in (
dom T1) & q
= (p
^ r) & (D1
. q)
= (T1
. r) and
A8: (
dom D2)
= ((
dom T)
with-replacement (p,(
dom T1))) and
A9: for q st q
in ((
dom T)
with-replacement (p,(
dom T1))) holds not p
is_a_prefix_of q & (D2
. q)
= (T
. q) or ex r st r
in (
dom T1) & q
= (p
^ r) & (D2
. q)
= (T1
. r);
now
let q;
assume that
A10: q
in (
dom D1) and
A11: (D1
. q)
<> (D2
. q);
A12: not p
is_a_prefix_of q & (D1
. q)
= (T
. q) or ex r st r
in (
dom T1) & q
= (p
^ r) & (D1
. q)
= (T1
. r) by
A6,
A7,
A10;
not p
is_a_prefix_of q & (D2
. q)
= (T
. q) or ex r st r
in (
dom T1) & q
= (p
^ r) & (D2
. q)
= (T1
. r) by
A6,
A9,
A10;
hence contradiction by
A11,
A12,
FINSEQ_1: 33,
TREES_1: 1;
end;
hence thesis by
A6,
A8,
Th31;
end;
end
registration
let W, x;
cluster (W
--> x) ->
DecoratedTree-like;
coherence ;
end
theorem ::
TREES_2:33
Th33: (for x st x
in D holds x is
Tree) implies (
union D) is
Tree
proof
assume
A1: for x st x
in D holds x is
Tree;
then
reconsider x = the
Element of D as
Tree;
x
c= (
union D) by
ZFMISC_1: 74;
then
reconsider T = (
union D) as non
empty
set;
T is
Tree-like
proof
for X st X
in D holds X
c= (
NAT
* )
proof
let X;
assume X
in D;
then X is
Tree by
A1;
hence thesis by
TREES_1:def 3;
end;
hence T
c= (
NAT
* ) by
ZFMISC_1: 76;
thus for p st p
in T holds (
ProperPrefixes p)
c= T
proof
let p;
assume p
in T;
then
consider X such that
A2: p
in X and
A3: X
in D by
TARSKI:def 4;
reconsider X as
Tree by
A1,
A3;
(
ProperPrefixes p)
c= X & X
c= T by
A2,
A3,
TREES_1:def 3,
ZFMISC_1: 74;
hence thesis;
end;
let p, k, n;
assume that
A4: (p
^
<*k*>)
in T and
A5: n
<= k;
consider X such that
A6: (p
^
<*k*>)
in X and
A7: X
in D by
A4,
TARSKI:def 4;
reconsider X as
Tree by
A1,
A7;
(p
^
<*n*>)
in X by
A5,
A6,
TREES_1:def 3;
hence thesis by
A7,
TARSKI:def 4;
end;
hence thesis;
end;
theorem ::
TREES_2:34
Th34: (for x st x
in X holds x is
Function) & X is
c=-linear implies (
union X) is
Relation-like
Function-like
proof
assume that
A1: for x st x
in X holds x is
Function and
A2: X is
c=-linear;
thus for a be
object holds a
in (
union X) implies ex b,c be
object st
[b, c]
= a
proof
let a be
object;
assume a
in (
union X);
then
consider x be
set such that
A3: a
in x and
A4: x
in X by
TARSKI:def 4;
reconsider x as
Function by
A1,
A4;
x
= x;
hence thesis by
A3,
RELAT_1:def 1;
end;
let a,b,c be
object;
assume that
A5:
[a, b]
in (
union X) and
A6:
[a, c]
in (
union X);
consider x be
set such that
A7:
[a, b]
in x and
A8: x
in X by
A5,
TARSKI:def 4;
consider y be
set such that
A9:
[a, c]
in y and
A10: y
in X by
A6,
TARSKI:def 4;
reconsider x as
Function by
A1,
A8;
reconsider y as
Function by
A1,
A10;
(x,y)
are_c=-comparable by
A2,
A8,
A10;
then x
c= y or y
c= x;
hence thesis by
A7,
A9,
FUNCT_1:def 1;
end;
theorem ::
TREES_2:35
Th35: (for x st x
in D holds x is
DecoratedTree) & D is
c=-linear implies (
union D) is
DecoratedTree
proof
assume that
A1: for x st x
in D holds x is
DecoratedTree and
A2: D is
c=-linear;
for x holds x
in D implies x is
Function by
A1;
then
reconsider T = (
union D) as
Function by
A2,
Th34;
defpred
X[
object,
object] means ex T1 st $1
= T1 & (
dom T1)
= $2;
A3: for x be
object st x
in D holds ex y be
object st
X[x, y]
proof
let x be
object;
assume x
in D;
then
reconsider T1 = x as
DecoratedTree by
A1;
(
dom T1)
= (
dom T1);
hence thesis;
end;
consider f such that
A4: (
dom f)
= D & for x be
object st x
in D holds
X[x, (f
. x)] from
CLASSES1:sch 1(
A3);
reconsider E = (
rng f) as non
empty
set by
A4,
RELAT_1: 42;
now
let x;
assume x
in E;
then
consider y be
object such that
A5: y
in (
dom f) & x
= (f
. y) by
FUNCT_1:def 3;
ex T1 st y
= T1 & (
dom T1)
= x by
A4,
A5;
hence x is
Tree;
end;
then
A6: (
union E) is
Tree by
Th33;
(
dom T)
= (
union E)
proof
thus (
dom T)
c= (
union E)
proof
let x be
object;
assume x
in (
dom T);
then
consider y be
object such that
A7:
[x, y]
in T by
XTUPLE_0:def 12;
consider X such that
A8:
[x, y]
in X and
A9: X
in D by
A7,
TARSKI:def 4;
consider T1 such that
A10: X
= T1 and
A11: (
dom T1)
= (f
. X) by
A4,
A9;
A12: (
dom T1)
in (
rng f) by
A4,
A9,
A11,
FUNCT_1:def 3;
A13: x
in (
dom T1) by
A8,
A10,
XTUPLE_0:def 12;
(
dom T1)
c= (
union E) by
A12,
ZFMISC_1: 74;
hence thesis by
A13;
end;
let x be
object;
assume x
in (
union E);
then
consider X such that
A14: x
in X and
A15: X
in E by
TARSKI:def 4;
consider y be
object such that
A16: y
in (
dom f) and
A17: X
= (f
. y) by
A15,
FUNCT_1:def 3;
consider T1 such that
A18: y
= T1 and
A19: (
dom T1)
= X by
A4,
A16,
A17;
[x, (T1
. x)]
in T1 by
A14,
A19,
FUNCT_1: 1;
then
[x, (T1
. x)]
in (
union D) by
A4,
A16,
A18,
TARSKI:def 4;
hence thesis by
XTUPLE_0:def 12;
end;
hence thesis by
A6,
Def8;
end;
theorem ::
TREES_2:36
Th36: (for x st x
in D9 holds x is
DecoratedTree of D) & D9 is
c=-linear implies (
union D9) is
DecoratedTree of D
proof
assume that
A1: for x st x
in D9 holds x is
DecoratedTree of D and
A2: D9 is
c=-linear;
for x st x
in D9 holds x is
DecoratedTree by
A1;
then
reconsider T = (
union D9) as
DecoratedTree by
A2,
Th35;
(
rng T)
c= D
proof
let x be
object;
assume x
in (
rng T);
then
consider y be
object such that
A3: y
in (
dom T) & x
= (T
. y) by
FUNCT_1:def 3;
[y, x]
in T by
A3,
FUNCT_1: 1;
then
consider X such that
A4:
[y, x]
in X and
A5: X
in D9 by
TARSKI:def 4;
reconsider X as
DecoratedTree of D by
A1,
A5;
y
in (
dom X) & x
= (X
. y) by
A4,
FUNCT_1: 1;
then
A6: x
in (
rng X) by
FUNCT_1:def 3;
thus thesis by
A6;
end;
hence thesis by
RELAT_1:def 19;
end;
scheme ::
TREES_2:sch8
DTreeStructEx { D() -> non
empty
set , d() ->
Element of D() , F(
set) ->
set , S() ->
Function of
[:D(),
NAT :], D() } :
ex T be
DecoratedTree of D() st (T
.
{} )
= d() & for t be
Element of (
dom T) holds (
succ t)
= { (t
^
<*k*>) : k
in F(.) } & for n st n
in F(.) holds (T
. (t
^
<*n*>))
= (S()
. ((T
. t),n))
provided
A1: for d be
Element of D(), k1, k2 st k1
<= k2 & k2
in F(d) holds k1
in F(d);
defpred
P[
Nat] means ex T be
DecoratedTree of D() st (T
.
{} )
= d() & for t be
Element of (
dom T) holds (
len t)
<= $1 & ((
len t)
< $1 implies (
succ t)
= { (t
^
<*k*>) : k
in F(.) } & for n, x st x
= (T
. t) & n
in F(x) holds (T
. (t
^
<*n*>))
= (S()
. (x,n)));
reconsider W =
{
{} } as
Tree;
A2:
P[
0 ]
proof
take T1 = (W
--> d());
{}
in W by
TREES_1: 22;
hence (T1
.
{} )
= d() by
FUNCOP_1: 7;
let t be
Element of (
dom T1);
t
=
{} by
TARSKI:def 1;
hence (
len t)
<=
0 ;
assume (
len t)
<
0 ;
hence thesis;
end;
A3:
P[k] implies
P[(k
+ 1)]
proof
given T be
DecoratedTree of D() such that
A4: (T
.
{} )
= d() & for t be
Element of (
dom T) holds (
len t)
<= k & ((
len t)
< k implies (
succ t)
= { (t
^
<*m*>) : m
in F(.) } & for n, x st x
= (T
. t) & n
in F(x) holds (T
. (t
^
<*n*>))
= (S()
. (x,n)));
reconsider M = ({ (t
^
<*n*>) where t be
Element of (
dom T) : n
in F(.) }
\/ (
dom T)) as non
empty
set;
M is
Tree-like
proof
thus M
c= (
NAT
* )
proof
let x be
object;
assume x
in M;
then
A5: x
in { (t
^
<*n*>) where t be
Element of (
dom T) : n
in F(.) } or x
in (
dom T) & (
dom T)
c= (
NAT
* ) by
TREES_1:def 3,
XBOOLE_0:def 3;
assume
A6: not x
in (
NAT
* );
then
consider n be
Nat, t be
Element of (
dom T) such that
A7: x
= (t
^
<*n*>) & n
in F(.) by
A5;
reconsider n as
Element of
NAT by
ORDINAL1:def 12;
x
= (t
^
<*n*>) by
A7;
hence thesis by
A6,
FINSEQ_1:def 11;
end;
thus for p st p
in M holds (
ProperPrefixes p)
c= M
proof
let p;
assume p
in M;
then
A8: p
in { (t
^
<*n*>) where t be
Element of (
dom T) : n
in F(.) } or p
in (
dom T) by
XBOOLE_0:def 3;
now
assume p
in { (t
^
<*n*>) where t be
Element of (
dom T) : n
in F(.) };
then
consider n be
Nat, t be
Element of (
dom T) such that
A9: p
= (t
^
<*n*>) and n
in F(.);
A10: (
ProperPrefixes t)
c= (
dom T) by
TREES_1:def 3;
A11: (
dom T)
c= M by
XBOOLE_1: 7;
A12: (
ProperPrefixes t)
c= M by
A10,
A11;
A13:
{t}
c= M by
A11,
ZFMISC_1: 31;
(
ProperPrefixes p)
= ((
ProperPrefixes t)
\/
{t}) by
A9,
Th4;
hence thesis by
A12,
A13,
XBOOLE_1: 8;
end;
then (
ProperPrefixes p)
c= M or (
ProperPrefixes p)
c= (
dom T) & (
dom T)
c= M by
A8,
TREES_1:def 3,
XBOOLE_1: 7;
hence thesis;
end;
let p, m, n;
assume (p
^
<*m*>)
in M;
then
A14: (p
^
<*m*>)
in { (t
^
<*l*>) where t be
Element of (
dom T) : l
in F(.) } or (p
^
<*m*>)
in (
dom T) by
XBOOLE_0:def 3;
assume that
A15: n
<= m and
A16: not (p
^
<*n*>)
in M;
not (p
^
<*n*>)
in (
dom T) by
A16,
XBOOLE_0:def 3;
then
consider l be
Nat, t be
Element of (
dom T) such that
A17: (p
^
<*m*>)
= (t
^
<*l*>) and
A18: l
in F(.) 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 F(.) by
A1,
A15,
A17,
A18,
A19,
A20,
A21;
then (p
^
<*n*>)
in { (s
^
<*i*>) where s be
Element of (
dom T) : i
in F(.) } by
A22;
hence thesis by
A16,
XBOOLE_0:def 3;
end;
then
reconsider M as
Tree;
defpred
P[
FinSequence,
set] means $1
in (
dom T) & $2
= (T
. $1) or not $1
in (
dom T) & ex n, q st $1
= (q
^
<*n*>) & $2
= (S()
. ((T
. q),n));
A23: for p st p
in M holds ex x st
P[p, x]
proof
let p;
assume p
in M;
then
A24: p
in { (t
^
<*l*>) where t be
Element of (
dom T) : l
in F(.) } or p
in (
dom T) by
XBOOLE_0:def 3;
now
assume
A25: not p
in (
dom T);
then
consider l be
Nat, t be
Element of (
dom T) such that
A26: p
= (t
^
<*l*>) and l
in F(.) by
A24;
take x = (S()
. ((T
. t),l));
thus p
in (
dom T) & x
= (T
. p) or not p
in (
dom T) & ex n, q st p
= (q
^
<*n*>) & x
= (S()
. ((T
. q),n)) by
A25,
A26;
end;
hence thesis;
end;
consider T9 be
DecoratedTree such that
A27: (
dom T9)
= M & for p st p
in M holds
P[p, (T9
. p)] from
DTreeEx(
A23);
(
rng T9)
c= D()
proof
let x be
object;
assume x
in (
rng T9);
then
consider y be
object such that
A28: y
in (
dom T9) and
A29: x
= (T9
. y) by
FUNCT_1:def 3;
reconsider y as
Element of (
dom T9) by
A28;
A30:
now
assume y
in (
dom T);
then
reconsider t = y as
Element of (
dom T);
(T
. t)
in D();
hence thesis by
A27,
A29;
end;
now
assume
A31: not y
in (
dom T);
then
consider n, q such that
A32: y
= (q
^
<*n*>) and
A33: (T9
. y)
= (S()
. ((T
. q),n)) by
A27;
y
in { (t
^
<*l*>) where t be
Element of (
dom T) : l
in F(.) } by
A27,
A31,
XBOOLE_0:def 3;
then
consider l be
Nat, t be
Element of (
dom T) such that
A34: y
= (t
^
<*l*>) and l
in F(.);
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 D();
then
[(T
. q), n]
in
[:D(),
NAT :] by
A39,
ZFMISC_1: 87,
A40;
hence thesis by
A29,
A33,
FUNCT_2: 5;
end;
hence thesis by
A30;
end;
then
reconsider T9 as
DecoratedTree of D() by
RELAT_1:def 19;
take T9;
(
<*>
NAT )
in M & (
<*>
NAT )
in (
dom T) by
TREES_1: 22;
hence (T9
.
{} )
= d() by
A4,
A27;
let t be
Element of (
dom T9);
A41:
now
assume t
in { (s
^
<*l*>) where s be
Element of (
dom T) : l
in F(.) };
then
consider l be
Nat, s be
Element of (
dom T) such that
A42: t
= (s
^
<*l*>) and l
in F(.);
(
len s)
<= k by
A4;
then (
len
<*l*>)
= 1 & ((
len s)
+ 1)
<= (k
+ 1) by
FINSEQ_1: 39,
XREAL_1: 7;
hence (
len t)
<= (k
+ 1) by
A42,
FINSEQ_1: 22;
end;
now
assume t
in (
dom T);
then
reconsider s = t as
Element of (
dom T);
(
len s)
<= k & k
<= (k
+ 1) by
A4,
NAT_1: 11;
hence (
len t)
<= (k
+ 1) by
XXREAL_0: 2;
end;
hence (
len t)
<= (k
+ 1) by
A27,
A41,
XBOOLE_0:def 3;
assume
A43: (
len t)
< (k
+ 1);
A44:
now
assume
A45: not t
in (
dom T);
then t
in { (s
^
<*l*>) where s be
Element of (
dom T) : l
in F(.) } by
A27,
XBOOLE_0:def 3;
then
consider l be
Nat, s be
Element of (
dom T) such that
A46: t
= (s
^
<*l*>) and
A47: l
in F(.);
A48: (
len t)
= ((
len s)
+ (
len
<*l*>)) by
A46,
FINSEQ_1: 22;
(
len
<*l*>)
= 1 & (
len t)
<= k by
A43,
FINSEQ_1: 39,
NAT_1: 13;
then (
len s)
< k by
A48,
NAT_1: 13;
then (
succ s)
= { (s
^
<*m*>) : m
in F(.) } by
A4;
then t
in (
succ s) by
A46,
A47;
hence contradiction by
A45;
end;
then
A49: (T9
. t)
= (T
. t) by
A27;
reconsider t9 = t as
Element of (
dom T) by
A44;
thus (
succ t)
c= { (t
^
<*i*>) : i
in F(.) }
proof
let x be
object;
assume x
in (
succ t);
then
consider n such that
A50: x
= (t
^
<*n*>) and
A51: (t
^
<*n*>)
in (
dom T9);
now
per cases ;
suppose
A52: (t
^
<*n*>)
in (
dom T);
then
reconsider s = (t
^
<*n*>), t9 = t as
Element of (
dom T) by
TREES_1: 21;
(
len s)
<= k & (
len s)
= ((
len t)
+ 1) by
A4,
FINSEQ_2: 16;
then (
len t)
< k by
NAT_1: 13;
then (
succ t9)
= { (t9
^
<*m*>) : m
in F(.) } by
A4;
hence thesis by
A49,
A50,
A52;
end;
suppose not (t
^
<*n*>)
in (
dom T);
then (t
^
<*n*>)
in { (s
^
<*l*>) where s be
Element of (
dom T) : l
in F(.) } by
A27,
A51,
XBOOLE_0:def 3;
then
consider l be
Nat, s be
Element of (
dom T) such that
A53: (t
^
<*n*>)
= (s
^
<*l*>) and
A54: l
in F(.);
t
= s by
A53,
FINSEQ_2: 17;
hence thesis by
A49,
A50,
A53,
A54;
end;
end;
hence thesis;
end;
thus
A55: { (t
^
<*i*>) : i
in F(.) }
c= (
succ t)
proof
let x be
object;
assume x
in { (t
^
<*i*>) : i
in F(.) };
then
consider n such that
A56: x
= (t
^
<*n*>) and
A57: n
in F(.);
x
= (t9
^
<*n*>) by
A56;
then x
in { (s
^
<*l*>) where s be
Element of (
dom T) : l
in F(.) } by
A49,
A57;
then x
in (
dom T9) by
A27,
XBOOLE_0:def 3;
hence thesis by
A56;
end;
let n, x;
assume that
A58: x
= (T9
. t) and
A59: n
in F(x);
(t
^
<*n*>)
in { (t
^
<*i*>) : i
in F(.) } by
A58,
A59;
then
A60: (t
^
<*n*>)
in (
succ t) by
A55;
reconsider n as
Element of
NAT by
ORDINAL1:def 12;
now
per cases ;
suppose
A61: (t
^
<*n*>)
in (
dom T);
then
reconsider s = (t
^
<*n*>) as
Element of (
dom T);
(
len s)
<= k & (
len s)
= ((
len t)
+ 1) by
A4,
FINSEQ_2: 16;
then (
len t9)
< k by
NAT_1: 13;
then (T
. (t9
^
<*n*>))
= (S()
. (x,n)) by
A4,
A49,
A58,
A59;
hence thesis by
A27,
A60,
A61;
end;
suppose not (t
^
<*n*>)
in (
dom T);
then
consider l, q such that
A62: (t
^
<*n*>)
= (q
^
<*l*>) and
A63: (T9
. (t
^
<*n*>))
= (S()
. ((T
. q),l)) by
A27,
A60;
t
= q & n
= l by
A62,
FINSEQ_2: 17;
hence thesis by
A27,
A44,
A58,
A63;
end;
end;
hence thesis;
end;
A64:
P[k] from
NAT_1:sch 2(
A2,
A3);
defpred
P[
object,
object] means ex T be
DecoratedTree of D(), k st $1
= k & $2
= T & (T
.
{} )
= d() & for t be
Element of (
dom T) holds (
len t)
<= k & ((
len t)
< k implies (
succ t)
= { (t
^
<*i*>) : i
in F(.) } & for n, x st x
= (T
. t) & n
in F(x) holds (T
. (t
^
<*n*>))
= (S()
. (x,n)));
A65: for x be
object st x
in
NAT holds ex y be
object st
P[x, y]
proof
let x be
object;
assume x
in
NAT ;
then
reconsider N = x as
Nat;
consider T be
DecoratedTree of D() such that
A66: (T
.
{} )
= d() & for t be
Element of (
dom T) holds (
len t)
<= N & ((
len t)
< N implies (
succ t)
= { (t
^
<*k*>) : k
in F(.) } & for n, x st x
= (T
. t) & n
in F(x) holds (T
. (t
^
<*n*>))
= (S()
. (x,n))) by
A64;
reconsider y = T as
set;
take y, T, N;
thus thesis by
A66;
end;
consider f such that
A67: (
dom f)
=
NAT & for x be
object st x
in
NAT holds
P[x, (f
. x)] from
CLASSES1:sch 1(
A65);
A68: for x be
Nat holds
P[x, (f
. x)] by
ORDINAL1:def 12,
A67;
reconsider E = (
rng f) as non
empty
set by
A67,
RELAT_1: 42;
A69: for x st x
in E holds x is
DecoratedTree of D()
proof
let x;
assume x
in E;
then
consider y be
object such that
A70: y
in (
dom f) and
A71: x
= (f
. y) by
FUNCT_1:def 3;
ex T be
DecoratedTree of D(), k st y
= k & (f
. y)
= T & (T
.
{} )
= d() & for t be
Element of (
dom T) holds (
len t)
<= k & ((
len t)
< k implies (
succ t)
= { (t
^
<*i*>) : i
in F(.) } & for n, x st x
= (T
. t) & n
in F(x) holds (T
. (t
^
<*n*>))
= (S()
. (x,n))) by
A67,
A70;
hence thesis by
A71;
end;
A72: for T1, T2, k1, k2 st T1
= (f
. k1) & T2
= (f
. k2) & k1
<= k2 holds T1
c= T2
proof
let T1, T2;
let x,y be
Nat such that
A73: T1
= (f
. x) and
A74: T2
= (f
. y) and
A75: x
<= y;
consider T19 be
DecoratedTree of D(), k1 such that
A76: x
= k1 & (f
. x)
= T19 & (T19
.
{} )
= d() & for t be
Element of (
dom T19) holds (
len t)
<= k1 & ((
len t)
< k1 implies (
succ t)
= { (t
^
<*i*>) : i
in F(.) } & for n, x st x
= (T19
. t) & n
in F(x) holds (T19
. (t
^
<*n*>))
= (S()
. (x,n))) by
A68;
consider T29 be
DecoratedTree of D(), k2 such that
A77: y
= k2 & (f
. y)
= T29 & (T29
.
{} )
= d() & for t be
Element of (
dom T29) holds (
len t)
<= k2 & ((
len t)
< k2 implies (
succ t)
= { (t
^
<*i*>) : i
in F(.) } & for n, x st x
= (T29
. t) & n
in F(x) holds (T29
. (t
^
<*n*>))
= (S()
. (x,n))) by
A68;
defpred
I[
Nat] means for t be
Element of (
dom T1) st (
len t)
<= $1 holds t
in (
dom T2) & (T1
. t)
= (T2
. t);
A78:
I[
0 ]
proof
let t be
Element of (
dom T1) such that
A79: (
len t)
<=
0 ;
t
=
{} by
A79;
hence thesis by
A73,
A74,
A76,
A77,
TREES_1: 22;
end;
A80:
I[k] implies
I[(k
+ 1)]
proof
assume
A81: for t be
Element of (
dom T1) st (
len t)
<= k holds t
in (
dom T2) & (T1
. t)
= (T2
. t);
let t be
Element of (
dom T1);
assume (
len t)
<= (k
+ 1);
then
A82: (
len t)
<= k or (
len t)
= (k
+ 1) by
NAT_1: 8;
now
assume
A83: (
len t)
= (k
+ 1);
reconsider p = (t
| (
Seg k)) as
FinSequence of
NAT by
FINSEQ_1: 18;
p
is_a_prefix_of t;
then
reconsider 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 be
FinSequence, x be
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 as
Nat by
A92;
A93: (p
^
<*x*>)
in (
succ p) by
A89,
A91;
(
succ p)
= { (p
^
<*i*>) : i
in F(.) } by
A73,
A76,
A86,
A87;
then
consider i such that
A94: (p
^
<*x*>)
= (p
^
<*i*>) and
A95: i
in F(.) by
A93;
A96: k
< k2 by
A75,
A76,
A77,
A87,
XXREAL_0: 2;
then
A97: (
succ p9)
= { (p9
^
<*l*>) : l
in F(.) } 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)
= (S()
. ((T19
. p),x)) by
A73,
A76,
A86,
A87,
A89,
A91,
A95,
A98;
hence thesis by
A73,
A74,
A76,
A77,
A86,
A88,
A89,
A91,
A95,
A96,
A98,
A99;
end;
hence thesis by
A81,
A82;
end;
A100:
I[k] from
NAT_1:sch 2(
A78,
A80);
let x be
object;
assume
A101: x
in T1;
then
consider y,z be
object such that
A102:
[y, z]
= x by
RELAT_1:def 1;
A103: (T1
. y)
= z by
A101,
A102,
FUNCT_1: 1;
reconsider 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 thesis by
A102,
A103,
FUNCT_1: 1;
end;
E is
c=-linear
proof
let T1,T2 be
set;
assume
A104: T1
in E;
then
consider x be
object such that
A105: x
in (
dom f) and
A106: T1
= (f
. x) by
FUNCT_1:def 3;
assume
A107: T2
in E;
then
consider y be
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, 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;
end;
then
reconsider T = (
union (
rng f)) as
DecoratedTree of D() by
A69,
Th36;
take T;
consider T9 be
DecoratedTree of D(), k such that
A112:
0
= k & (f
.
0 )
= T9 & (T9
.
{} )
= d() & for t be
Element of (
dom T9) holds (
len t)
<= k & ((
len t)
< k implies (
succ t)
= { (t
^
<*i*>) : i
in F(.) } & for n, x st x
= (T9
. t) & n
in F(x) holds (T9
. (t
^
<*n*>))
= (S()
. (x,n))) by
A67;
{}
in (
dom T9) by
TREES_1: 22;
then
A113:
[
{} , d()]
in T9 by
A112,
FUNCT_1: 1;
T9
in (
rng f) by
A67,
A112,
FUNCT_1:def 3;
then
[
{} , d()]
in T by
A113,
TARSKI:def 4;
hence (T
.
{} )
= d() by
FUNCT_1: 1;
A114: for T1, x st T1
in E & x
in (
dom T1) holds x
in (
dom T) & (T1
. x)
= (T
. x)
proof
let T1, x;
assume that
A115: T1
in E and
A116: x
in (
dom T1);
[x, (T1
. x)]
in T1 by
A116,
FUNCT_1: 1;
then
[x, (T1
. x)]
in T by
A115,
TARSKI:def 4;
hence thesis by
FUNCT_1: 1;
end;
let t be
Element of (
dom T);
thus (
succ t)
c= { (t
^
<*i*>) : i
in F(.) }
proof
let x be
object;
assume x
in (
succ t);
then
consider l 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 such that
A119:
[x, (T
. x)]
in X and
A120: X
in (
rng f) by
TARSKI:def 4;
consider y be
object such that
A121: y
in
NAT and
A122: X
= (f
. y) by
A67,
A120,
FUNCT_1:def 3;
consider T1 be
DecoratedTree of D(), k1 such that
A123: y
= k1 & (f
. y)
= T1 & (T1
.
{} )
= d() & for t be
Element of (
dom T1) holds (
len t)
<= k1 & ((
len t)
< k1 implies (
succ t)
= { (t
^
<*i*>) : i
in F(.) } & for n, x st x
= (T1
. t) & n
in F(x) holds (T1
. (t
^
<*n*>))
= (S()
. (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*>) : i
in F(.) } by
A123;
(T1
. t)
= (T
. t) by
A114,
A120,
A122,
A123,
A125;
hence thesis by
A117,
A124,
A126;
end;
[t, (T
. t)]
in T by
FUNCT_1: 1;
then
consider X such that
A127:
[t, (T
. t)]
in X and
A128: X
in E by
TARSKI:def 4;
consider y be
object such that
A129: y
in
NAT and
A130: X
= (f
. y) by
A67,
A128,
FUNCT_1:def 3;
reconsider y as
Nat by
A129;
consider T1 be
DecoratedTree of D(), k1 such that
A131: y
= k1 & (f
. y)
= T1 & (T1
.
{} )
= d() & for t be
Element of (
dom T1) holds (
len t)
<= k1 & ((
len t)
< k1 implies (
succ t)
= { (t
^
<*i*>) : i
in F(.) } & for n, x st x
= (T1
. t) & n
in F(x) holds (T1
. (t
^
<*n*>))
= (S()
. (x,n))) by
A68;
consider T2 be
DecoratedTree of D(), k2 such that
A132: (y
+ 1)
= k2 & (f
. (y
+ 1))
= T2 & (T2
.
{} )
= d() & for t be
Element of (
dom T2) holds (
len t)
<= k2 & ((
len t)
< k2 implies (
succ t)
= { (t
^
<*i*>) : i
in F(.) } & for n, x st x
= (T2
. t) & n
in F(x) holds (T2
. (t
^
<*n*>))
= (S()
. (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*>) : i
in F(.) } by
A132;
thus { (t
^
<*i*>) : i
in F(.) }
c= (
succ t)
proof
let x be
object;
assume
A138: x
in { (t
^
<*i*>) : i
in F(.) };
then
A139: ex l st x
= (t
^
<*l*>) & l
in F(.);
A140: x
in (
succ t2) by
A132,
A135,
A136,
A138;
T2
in E by
A67,
A132,
FUNCT_1:def 3;
then x
in (
dom T) by
A114,
A140;
hence thesis by
A139;
end;
let n;
assume
A141: n
in F(.);
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 thesis by
A132,
A135,
A136,
A141;
end;
scheme ::
TREES_2:sch9
DTreeStructFinEx { D() -> non
empty
set , d() ->
Element of D() , F(
set) ->
Nat , S() ->
Function of
[:D(),
NAT :], D() } :
ex T be
DecoratedTree of D() st (T
.
{} )
= d() & for t be
Element of (
dom T) holds (
succ t)
= { (t
^
<*k*>) : k
< F(.) } & for n st n
< F(.) holds (T
. (t
^
<*n*>))
= (S()
. ((T
. t),n));
deffunc
FF(
Nat) = { i : i
< $1 };
deffunc
U(
set) =
FF(F);
A1: for d be
Element of D(), k1, k2 st k1
<= k2 & k2
in
U(d) holds k1
in
U(d)
proof
let d be
Element of D(), k1, k2;
assume
A2: k1
<= k2 & k2
in { i : i
< F(d) };
then ex i st k2
= i & i
< F(d);
then k1
< F(d) by
A2,
XXREAL_0: 2;
hence thesis;
end;
consider T be
DecoratedTree of D() such that
A3: (T
.
{} )
= d() & for t be
Element of (
dom T) holds (
succ t)
= { (t
^
<*k*>) : k
in
U(.) } & for n st n
in
U(.) holds (T
. (t
^
<*n*>))
= (S()
. ((T
. t),n)) from
DTreeStructEx(
A1);
take T;
thus (T
.
{} )
= d() by
A3;
let t be
Element of (
dom T);
A4: (
succ t)
= { (t
^
<*k*>) : k
in
FF(F) } by
A3;
thus (
succ t)
c= { (t
^
<*i*>) : i
< F(.) }
proof
let x be
object;
assume x
in (
succ t);
then
consider l such that
A5: x
= (t
^
<*l*>) and
A6: l
in
FF(F) by
A4;
ex i st l
= i & i
< F(.) by
A6;
hence thesis by
A5;
end;
thus { (t
^
<*i*>) : i
< F(.) }
c= (
succ t)
proof
let x be
object;
assume x
in { (t
^
<*i*>) : i
< F(.) };
then
consider l such that
A7: x
= (t
^
<*l*>) and
A8: l
< F(.);
l
in
FF(F) by
A8;
hence thesis by
A4,
A7;
end;
let n;
assume n
< F(.);
then n
in
FF(F);
hence thesis by
A3;
end;
begin
registration
let Tr be
finite
Tree, v be
Element of Tr;
cluster (
succ v) ->
finite;
coherence ;
end
definition
let Tr be
finite
Tree, v be
Element of Tr;
::
TREES_2:def12
func
branchdeg v ->
set equals (
card (
succ v));
correctness ;
end
registration
cluster
finite for
DecoratedTree;
existence
proof
reconsider T =
{
{} } as
Tree;
take (T
-->
{} );
thus thesis;
end;
end
registration
let D be non
empty
set;
cluster
finite for
DecoratedTree of D;
existence
proof
set d = the
Element of D;
reconsider T =
{
{} } as
Tree;
take (T
--> d);
thus thesis;
end;
end
registration
let a,b be non
empty
set;
cluster non
empty for
Relation of a, b;
existence
proof
[:a, b:]
c=
[:a, b:];
hence thesis;
end;
end
reserve x1,x2 for
set,
w for
FinSequence of
NAT ;
theorem ::
TREES_2:37
for Z1,Z2 be
Tree, p be
FinSequence of
NAT st p
in Z1 holds for v be
Element of (Z1
with-replacement (p,Z2)), w be
Element of Z2 st v
= (p
^ w) holds ((
succ v),(
succ w))
are_equipotent
proof
let Z1,Z2 be
Tree, p be
FinSequence of
NAT such that
A1: p
in Z1;
set T = (Z1
with-replacement (p,Z2));
let t be
Element of (Z1
with-replacement (p,Z2)), t2 be
Element of Z2;
assume
A2: t
= (p
^ t2);
then
A3: p
is_a_prefix_of t by
TREES_1: 1;
A4: for n holds (t
^
<*n*>)
in T iff (t2
^
<*n*>)
in Z2
proof
let n;
A5: p
is_a_proper_prefix_of (t
^
<*n*>) by
A3,
TREES_1: 8;
reconsider nn = n as
Element of
NAT by
ORDINAL1:def 12;
A6: (t
^
<*nn*>)
= (p
^ (t2
^
<*nn*>)) by
A2,
FINSEQ_1: 32;
thus (t
^
<*n*>)
in T implies (t2
^
<*n*>)
in Z2
proof
assume
A7: (t
^
<*n*>)
in T;
reconsider n as
Element of
NAT by
ORDINAL1:def 12;
ex w st w
in Z2 & (t
^
<*n*>)
= (p
^ w) by
A1,
A5,
TREES_1:def 9,
A7;
hence thesis by
A6,
FINSEQ_1: 33;
end;
assume (t2
^
<*n*>)
in Z2;
hence thesis by
A1,
A6,
TREES_1:def 9;
end;
defpred
P[
object,
object] means for n st $1
= (t
^
<*n*>) holds $2
= (t2
^
<*n*>);
A8: for x be
object st x
in (
succ t) holds ex y be
object st
P[x, y]
proof
let x be
object;
assume x
in (
succ t);
then
consider n such that
A9: x
= (t
^
<*n*>) and (t
^
<*n*>)
in T;
take (t2
^
<*n*>);
let m;
assume x
= (t
^
<*m*>);
hence thesis by
A9,
FINSEQ_1: 33;
end;
consider f be
Function such that
A10: (
dom f)
= (
succ t) & for x be
object st x
in (
succ t) holds
P[x, (f
. x)] from
CLASSES1:sch 1(
A8);
now
let x be
object;
thus x
in (
rng f) implies x
in (
succ t2)
proof
assume x
in (
rng f);
then
consider y be
object such that
A11: y
in (
dom f) and
A12: x
= (f
. y) by
FUNCT_1:def 3;
consider n such that
A13: y
= (t
^
<*n*>) and
A14: (t
^
<*n*>)
in T by
A10,
A11;
A15: x
= (t2
^
<*n*>) by
A10,
A11,
A12,
A13;
(t2
^
<*n*>)
in Z2 by
A4,
A14;
hence thesis by
A15;
end;
assume x
in (
succ t2);
then
consider n such that
A16: x
= (t2
^
<*n*>) and
A17: (t2
^
<*n*>)
in Z2;
(t
^
<*n*>)
in T by
A4,
A17;
then
A18: (t
^
<*n*>)
in (
dom f) by
A10;
then (f
. (t
^
<*n*>))
= x by
A10,
A16;
hence x
in (
rng f) by
A18,
FUNCT_1:def 3;
end;
then
A19: (
rng f)
= (
succ t2) by
TARSKI: 2;
f is
one-to-one
proof
let x1,x2 be
object;
assume that
A20: x1
in (
dom f) and
A21: x2
in (
dom f) and
A22: (f
. x1)
= (f
. x2);
consider m such that
A23: x1
= (t
^
<*m*>) and (t
^
<*m*>)
in T by
A10,
A20;
consider k such that
A24: x2
= (t
^
<*k*>) and (t
^
<*k*>)
in T by
A10,
A21;
(t2
^
<*m*>)
= (f
. x1) by
A10,
A20,
A23
.= (t2
^
<*k*>) by
A10,
A21,
A22,
A24;
hence thesis by
A23,
A24,
FINSEQ_1: 33;
end;
hence thesis by
A10,
A19,
WELLORD2:def 4;
end;
scheme ::
TREES_2:sch10
DTreeStructEx { D() -> non
empty
set , d() ->
Element of D() , Q[
set,
set], S() ->
Function of
[:D(),
NAT :], D() } :
ex T be
DecoratedTree of D() st (T
.
{} )
= d() & for t be
Element of (
dom T) holds (
succ t)
= { (t
^
<*k*>) : Q[k, (T
. t)] } & for n st Q[n, (T
. t)] holds (T
. (t
^
<*n*>))
= (S()
. ((T
. t),n))
provided
A1: for d be
Element of D(), k1, k2 st k1
<= k2 & Q[k2, d] holds Q[k1, d];
defpred
P[
Nat] means ex T be
DecoratedTree of D() st (T
.
{} )
= d() & for t be
Element of (
dom T) holds (
len t)
<= $1 & ((
len t)
< $1 implies (
succ t)
= { (t
^
<*k*>) : Q[k, (T
. t)] } & for n, x st x
= (T
. t) & Q[n, x] holds (T
. (t
^
<*n*>))
= (S()
. (x,n)));
reconsider W =
{
{} } as
Tree;
A2:
P[
0 ]
proof
take T1 = (W
--> d());
{}
in W by
TREES_1: 22;
hence (T1
.
{} )
= d() by
FUNCOP_1: 7;
let t be
Element of (
dom T1);
t
=
{} by
TARSKI:def 1;
hence (
len t)
<=
0 ;
assume (
len t)
<
0 ;
hence thesis;
end;
A3:
P[k] implies
P[(k
+ 1)]
proof
given T be
DecoratedTree of D() such that
A4: (T
.
{} )
= d() & for t be
Element of (
dom T) holds (
len t)
<= k & ((
len t)
< k implies (
succ t)
= { (t
^
<*m*>) : Q[m, (T
. t)] } & for n, x st x
= (T
. t) & Q[n, x] holds (T
. (t
^
<*n*>))
= (S()
. (x,n)));
reconsider M = ({ (t
^
<*n*>) where t be
Element of (
dom T) : Q[n, (T
. t)] }
\/ (
dom T)) as non
empty
set;
M is
Tree-like
proof
thus M
c= (
NAT
* )
proof
let x be
object;
assume x
in M;
then
A5: x
in { (t
^
<*n*>) where t be
Element of (
dom T) : Q[n, (T
. t)] } or x
in (
dom T) & (
dom T)
c= (
NAT
* ) by
TREES_1:def 3,
XBOOLE_0:def 3;
assume
A6: not x
in (
NAT
* );
then
consider n be
Nat, t be
Element of (
dom T) such that
A7: x
= (t
^
<*n*>) & Q[n, (T
. t)] by
A5;
reconsider n as
Element of
NAT by
ORDINAL1:def 12;
x
= (t
^
<*n*>) by
A7;
hence thesis by
A6,
FINSEQ_1:def 11;
end;
thus for p st p
in M holds (
ProperPrefixes p)
c= M
proof
let p;
assume p
in M;
then
A8: p
in { (t
^
<*n*>) where t be
Element of (
dom T) : Q[n, (T
. t)] } or p
in (
dom T) by
XBOOLE_0:def 3;
now
assume p
in { (t
^
<*n*>) where t be
Element of (
dom T) : Q[n, (T
. t)] };
then
consider n be
Nat, t be
Element of (
dom T) such that
A9: p
= (t
^
<*n*>) and Q[n, (T
. t)];
A10: (
ProperPrefixes t)
c= (
dom T) by
TREES_1:def 3;
A11: (
dom T)
c= M by
XBOOLE_1: 7;
A12: (
ProperPrefixes t)
c= M by
A10,
A11;
A13:
{t}
c= M by
A11,
ZFMISC_1: 31;
(
ProperPrefixes p)
= ((
ProperPrefixes t)
\/
{t}) by
A9,
Th4;
hence thesis by
A12,
A13,
XBOOLE_1: 8;
end;
then (
ProperPrefixes p)
c= M or (
ProperPrefixes p)
c= (
dom T) & (
dom T)
c= M by
A8,
TREES_1:def 3,
XBOOLE_1: 7;
hence thesis;
end;
let p, m, n;
assume (p
^
<*m*>)
in M;
then
A14: (p
^
<*m*>)
in { (t
^
<*l*>) where t be
Element of (
dom T) : Q[l, (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;
not (p
^
<*n*>)
in (
dom T) by
A16,
XBOOLE_0:def 3;
then
consider l be
Nat, t be
Element of (
dom T) such that
A17: (p
^
<*m*>)
= (t
^
<*l*>) and
A18: Q[l, (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;
Q[n, (T
. t)] by
A1,
A15,
A17,
A18,
A19,
A20,
A21;
then (p
^
<*n*>)
in { (s
^
<*i*>) where s be
Element of (
dom T) : Q[i, (T
. s)] } by
A22;
hence thesis by
A16,
XBOOLE_0:def 3;
end;
then
reconsider M as
Tree;
defpred
P[
FinSequence,
set] means $1
in (
dom T) & $2
= (T
. $1) or not $1
in (
dom T) & ex n, q st $1
= (q
^
<*n*>) & $2
= (S()
. ((T
. q),n));
A23: for p st p
in M holds ex x st
P[p, x]
proof
let p;
assume p
in M;
then
A24: p
in { (t
^
<*l*>) where t be
Element of (
dom T) : Q[l, (T
. t)] } or p
in (
dom T) by
XBOOLE_0:def 3;
now
assume
A25: not p
in (
dom T);
then
consider l be
Nat, t be
Element of (
dom T) such that
A26: p
= (t
^
<*l*>) and Q[l, (T
. t)] by
A24;
take x = (S()
. ((T
. t),l));
thus p
in (
dom T) & x
= (T
. p) or not p
in (
dom T) & ex n, q st p
= (q
^
<*n*>) & x
= (S()
. ((T
. q),n)) by
A25,
A26;
end;
hence thesis;
end;
consider T9 be
DecoratedTree such that
A27: (
dom T9)
= M & for p st p
in M holds
P[p, (T9
. p)] from
DTreeEx(
A23);
(
rng T9)
c= D()
proof
let x be
object;
assume x
in (
rng T9);
then
consider y be
object such that
A28: y
in (
dom T9) and
A29: x
= (T9
. y) by
FUNCT_1:def 3;
reconsider y as
Element of (
dom T9) by
A28;
A30:
now
assume y
in (
dom T);
then
reconsider t = y as
Element of (
dom T);
(T
. t)
in D();
hence thesis by
A27,
A29;
end;
now
assume
A31: not y
in (
dom T);
then
consider n, q such that
A32: y
= (q
^
<*n*>) and
A33: (T9
. y)
= (S()
. ((T
. q),n)) by
A27;
y
in { (t
^
<*l*>) where t be
Element of (
dom T) : Q[l, (T
. t)] } by
A27,
A31,
XBOOLE_0:def 3;
then
consider l be
Nat, t be
Element of (
dom T) such that
A34: y
= (t
^
<*l*>) and Q[l, (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 D();
then
[(T
. q), n]
in
[:D(),
NAT :] by
A39,
ZFMISC_1: 87,
A40;
hence thesis by
A29,
A33,
FUNCT_2: 5;
end;
hence thesis by
A30;
end;
then
reconsider T9 as
DecoratedTree of D() by
RELAT_1:def 19;
take T9;
(
<*>
NAT )
in M & (
<*>
NAT )
in (
dom T) by
TREES_1: 22;
hence (T9
.
{} )
= d() by
A4,
A27;
let t be
Element of (
dom T9);
A41:
now
assume t
in { (s
^
<*l*>) where s be
Element of (
dom T) : Q[l, (T
. s)] };
then
consider l be
Nat, s be
Element of (
dom T) such that
A42: t
= (s
^
<*l*>) and Q[l, (T
. s)];
(
len s)
<= k by
A4;
then (
len
<*l*>)
= 1 & ((
len s)
+ 1)
<= (k
+ 1) by
FINSEQ_1: 39,
XREAL_1: 7;
hence (
len t)
<= (k
+ 1) by
A42,
FINSEQ_1: 22;
end;
now
assume t
in (
dom T);
then
reconsider s = t as
Element of (
dom T);
(
len s)
<= k & k
<= (k
+ 1) by
A4,
NAT_1: 11;
hence (
len t)
<= (k
+ 1) by
XXREAL_0: 2;
end;
hence (
len t)
<= (k
+ 1) by
A27,
A41,
XBOOLE_0:def 3;
assume
A43: (
len t)
< (k
+ 1);
A44:
now
assume
A45: not t
in (
dom T);
then t
in { (s
^
<*l*>) where s be
Element of (
dom T) : Q[l, (T
. s)] } by
A27,
XBOOLE_0:def 3;
then
consider l be
Nat, s be
Element of (
dom T) such that
A46: t
= (s
^
<*l*>) and
A47: Q[l, (T
. s)];
A48: (
len t)
= ((
len s)
+ (
len
<*l*>)) by
A46,
FINSEQ_1: 22;
(
len
<*l*>)
= 1 & (
len t)
<= k by
A43,
FINSEQ_1: 39,
NAT_1: 13;
then (
len s)
< k by
A48,
NAT_1: 13;
then (
succ s)
= { (s
^
<*m*>) : Q[m, (T
. s)] } by
A4;
then t
in (
succ s) by
A46,
A47;
hence contradiction by
A45;
end;
then
A49: (T9
. t)
= (T
. t) by
A27;
reconsider t9 = t as
Element of (
dom T) by
A44;
thus (
succ t)
c= { (t
^
<*i*>) : Q[i, (T9
. t)] }
proof
let x be
object;
assume x
in (
succ t);
then
consider n such that
A50: x
= (t
^
<*n*>) and
A51: (t
^
<*n*>)
in (
dom T9);
now
per cases ;
suppose
A52: (t
^
<*n*>)
in (
dom T);
then
reconsider s = (t
^
<*n*>), t9 = t as
Element of (
dom T) by
TREES_1: 21;
(
len s)
<= k & (
len s)
= ((
len t)
+ 1) by
A4,
FINSEQ_2: 16;
then (
len t)
< k by
NAT_1: 13;
then (
succ t9)
= { (t9
^
<*m*>) : Q[m, (T
. t9)] } by
A4;
hence thesis by
A49,
A50,
A52;
end;
suppose not (t
^
<*n*>)
in (
dom T);
then (t
^
<*n*>)
in { (s
^
<*l*>) where s be
Element of (
dom T) : Q[l, (T
. s)] } by
A27,
A51,
XBOOLE_0:def 3;
then
consider l be
Nat, s be
Element of (
dom T) such that
A53: (t
^
<*n*>)
= (s
^
<*l*>) and
A54: Q[l, (T
. s)];
t
= s by
A53,
FINSEQ_2: 17;
hence thesis by
A49,
A50,
A53,
A54;
end;
end;
hence thesis;
end;
thus
A55: { (t
^
<*i*>) : Q[i, (T9
. t)] }
c= (
succ t)
proof
let x be
object;
assume x
in { (t
^
<*i*>) : Q[i, (T9
. t)] };
then
consider n such that
A56: x
= (t
^
<*n*>) and
A57: Q[n, (T9
. t)];
x
= (t9
^
<*n*>) by
A56;
then x
in { (s
^
<*l*>) where s be
Element of (
dom T) : Q[l, (T
. s)] } by
A49,
A57;
then x
in (
dom T9) by
A27,
XBOOLE_0:def 3;
hence thesis by
A56;
end;
let n, x;
assume that
A58: x
= (T9
. t) and
A59: Q[n, x];
reconsider n as
Element of
NAT by
ORDINAL1:def 12;
(t
^
<*n*>)
in { (t
^
<*i*>) : Q[i, (T9
. t)] } by
A58,
A59;
then
A60: (t
^
<*n*>)
in (
succ t) by
A55;
now
per cases ;
suppose
A61: (t
^
<*n*>)
in (
dom T);
then
reconsider s = (t
^
<*n*>) as
Element of (
dom T);
(
len s)
<= k & (
len s)
= ((
len t)
+ 1) by
A4,
FINSEQ_2: 16;
then (
len t9)
< k by
NAT_1: 13;
then (T
. (t9
^
<*n*>))
= (S()
. (x,n)) by
A4,
A49,
A58,
A59;
hence thesis by
A27,
A60,
A61;
end;
suppose not (t
^
<*n*>)
in (
dom T);
then
consider l, q such that
A62: (t
^
<*n*>)
= (q
^
<*l*>) and
A63: (T9
. (t
^
<*n*>))
= (S()
. ((T
. q),l)) by
A27,
A60;
t
= q & n
= l by
A62,
FINSEQ_2: 17;
hence thesis by
A27,
A44,
A58,
A63;
end;
end;
hence thesis;
end;
A64:
P[k] from
NAT_1:sch 2(
A2,
A3);
defpred
P[
object,
object] means ex T be
DecoratedTree of D(), k st $1
= k & $2
= T & (T
.
{} )
= d() & for t be
Element of (
dom T) holds (
len t)
<= k & ((
len t)
< k implies (
succ t)
= { (t
^
<*i*>) : Q[i, (T
. t)] } & for n, x st x
= (T
. t) & Q[n, x] holds (T
. (t
^
<*n*>))
= (S()
. (x,n)));
A65: for x be
object st x
in
NAT holds ex y be
object st
P[x, y]
proof
let x be
object;
assume x
in
NAT ;
then
reconsider n = x as
Nat;
consider T be
DecoratedTree of D() such that
A66: (T
.
{} )
= d() & for t be
Element of (
dom T) holds (
len t)
<= n & ((
len t)
< n implies (
succ t)
= { (t
^
<*k*>) : Q[k, (T
. t)] } & for n, x st x
= (T
. t) & Q[n, x] holds (T
. (t
^
<*n*>))
= (S()
. (x,n))) by
A64;
reconsider y = T as
set;
take Y = y, T, N = n;
thus thesis by
A66;
end;
consider f such that
A67: (
dom f)
=
NAT & for x be
object st x
in
NAT holds
P[x, (f
. x)] from
CLASSES1:sch 1(
A65);
A68: for x be
Nat holds
P[x, (f
. x)] by
ORDINAL1:def 12,
A67;
reconsider E = (
rng f) as non
empty
set by
A67,
RELAT_1: 42;
A69: for x st x
in E holds x is
DecoratedTree of D()
proof
let x;
assume x
in E;
then
consider y be
object such that
A70: y
in (
dom f) and
A71: x
= (f
. y) by
FUNCT_1:def 3;
ex T be
DecoratedTree of D(), k st y
= k & (f
. y)
= T & (T
.
{} )
= d() & for t be
Element of (
dom T) holds (
len t)
<= k & ((
len t)
< k implies (
succ t)
= { (t
^
<*i*>) : Q[i, (T
. t)] } & for n, x st x
= (T
. t) & Q[n, x] holds (T
. (t
^
<*n*>))
= (S()
. (x,n))) by
A67,
A70;
hence thesis by
A71;
end;
A72: for T1, T2, k1, k2 st T1
= (f
. k1) & T2
= (f
. k2) & k1
<= k2 holds T1
c= T2
proof
let T1, T2;
let x,y be
Nat such that
A73: T1
= (f
. x) and
A74: T2
= (f
. y) and
A75: x
<= y;
consider T19 be
DecoratedTree of D(), k1 such that
A76: x
= k1 & (f
. x)
= T19 & (T19
.
{} )
= d() & for t be
Element of (
dom T19) holds (
len t)
<= k1 & ((
len t)
< k1 implies (
succ t)
= { (t
^
<*i*>) : Q[i, (T19
. t)] } & for n, x st x
= (T19
. t) & Q[n, x] holds (T19
. (t
^
<*n*>))
= (S()
. (x,n))) by
A68;
consider T29 be
DecoratedTree of D(), k2 such that
A77: y
= k2 & (f
. y)
= T29 & (T29
.
{} )
= d() & for t be
Element of (
dom T29) holds (
len t)
<= k2 & ((
len t)
< k2 implies (
succ t)
= { (t
^
<*i*>) : Q[i, (T29
. t)] } & for n, x st x
= (T29
. t) & Q[n, x] holds (T29
. (t
^
<*n*>))
= (S()
. (x,n))) by
A68;
defpred
I[
Nat] means for t be
Element of (
dom T1) st (
len t)
<= $1 holds t
in (
dom T2) & (T1
. t)
= (T2
. t);
A78:
I[
0 ]
proof
let t be
Element of (
dom T1) such that
A79: (
len t)
<=
0 ;
t
=
{} by
A79;
hence thesis by
A73,
A74,
A76,
A77,
TREES_1: 22;
end;
A80:
I[k] implies
I[(k
+ 1)]
proof
assume
A81: for t be
Element of (
dom T1) st (
len t)
<= k holds t
in (
dom T2) & (T1
. t)
= (T2
. t);
let t be
Element of (
dom T1);
assume (
len t)
<= (k
+ 1);
then
A82: (
len t)
<= k or (
len t)
= (k
+ 1) by
NAT_1: 8;
now
assume
A83: (
len t)
= (k
+ 1);
reconsider p = (t
| (
Seg k)) as
FinSequence of
NAT by
FINSEQ_1: 18;
p
is_a_prefix_of t;
then
reconsider 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 be
FinSequence, x be
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 as
Nat by
A92;
A93: (p
^
<*x*>)
in (
succ p) by
A89,
A91;
(
succ p)
= { (p
^
<*i*>) : Q[i, (T1
. p)] } by
A73,
A76,
A86,
A87;
then
consider i such that
A94: (p
^
<*x*>)
= (p
^
<*i*>) and
A95: Q[i, (T1
. p)] by
A93;
A96: k
< k2 by
A75,
A76,
A77,
A87,
XXREAL_0: 2;
then
A97: (
succ p9)
= { (p9
^
<*l*>) : Q[l, (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)
= (S()
. ((T19
. p),x)) by
A73,
A76,
A86,
A87,
A89,
A91,
A95,
A98;
hence thesis by
A73,
A74,
A76,
A77,
A86,
A88,
A89,
A91,
A95,
A96,
A98,
A99;
end;
hence thesis by
A81,
A82;
end;
A100:
I[k] from
NAT_1:sch 2(
A78,
A80);
let x be
object;
assume
A101: x
in T1;
then
consider y,z be
object such that
A102:
[y, z]
= x by
RELAT_1:def 1;
A103: (T1
. y)
= z by
A101,
A102,
FUNCT_1: 1;
reconsider 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 thesis by
A102,
A103,
FUNCT_1: 1;
end;
E is
c=-linear
proof
let T1,T2 be
set;
assume
A104: T1
in E;
then
consider x be
object such that
A105: x
in (
dom f) and
A106: T1
= (f
. x) by
FUNCT_1:def 3;
assume
A107: T2
in E;
then
consider y be
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, 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;
end;
then
reconsider T = (
union (
rng f)) as
DecoratedTree of D() by
A69,
Th36;
take T;
consider T9 be
DecoratedTree of D(), k such that
A112:
0
= k & (f
.
0 )
= T9 & (T9
.
{} )
= d() & for t be
Element of (
dom T9) holds (
len t)
<= k & ((
len t)
< k implies (
succ t)
= { (t
^
<*i*>) : Q[i, (T9
. t)] } & for n, x st x
= (T9
. t) & Q[n, x] holds (T9
. (t
^
<*n*>))
= (S()
. (x,n))) by
A67;
{}
in (
dom T9) by
TREES_1: 22;
then
A113:
[
{} , d()]
in T9 by
A112,
FUNCT_1: 1;
T9
in (
rng f) by
A67,
A112,
FUNCT_1:def 3;
then
[
{} , d()]
in T by
A113,
TARSKI:def 4;
hence (T
.
{} )
= d() by
FUNCT_1: 1;
A114: for T1, x st T1
in E & x
in (
dom T1) holds x
in (
dom T) & (T1
. x)
= (T
. x)
proof
let T1, x;
assume that
A115: T1
in E and
A116: x
in (
dom T1);
[x, (T1
. x)]
in T1 by
A116,
FUNCT_1: 1;
then
[x, (T1
. x)]
in T by
A115,
TARSKI:def 4;
hence thesis by
FUNCT_1: 1;
end;
let t be
Element of (
dom T);
thus (
succ t)
c= { (t
^
<*i*>) : Q[i, (T
. t)] }
proof
let x be
object;
assume x
in (
succ t);
then
consider l 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 such that
A119:
[x, (T
. x)]
in X and
A120: X
in (
rng f) by
TARSKI:def 4;
consider y be
object such that
A121: y
in
NAT and
A122: X
= (f
. y) by
A67,
A120,
FUNCT_1:def 3;
consider T1 be
DecoratedTree of D(), k1 such that
A123: y
= k1 & (f
. y)
= T1 & (T1
.
{} )
= d() & for t be
Element of (
dom T1) holds (
len t)
<= k1 & ((
len t)
< k1 implies (
succ t)
= { (t
^
<*i*>) : Q[i, (T1
. t)] } & for n, x st x
= (T1
. t) & Q[n, x] holds (T1
. (t
^
<*n*>))
= (S()
. (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*>) : Q[i, (T1
. t9)] } by
A123;
(T1
. t)
= (T
. t) by
A114,
A120,
A122,
A123,
A125;
hence thesis by
A117,
A124,
A126;
end;
[t, (T
. t)]
in T by
FUNCT_1: 1;
then
consider X such that
A127:
[t, (T
. t)]
in X and
A128: X
in E by
TARSKI:def 4;
consider y be
object such that
A129: y
in
NAT and
A130: X
= (f
. y) by
A67,
A128,
FUNCT_1:def 3;
reconsider y as
Nat by
A129;
consider T1 be
DecoratedTree of D(), k1 such that
A131: y
= k1 & (f
. y)
= T1 & (T1
.
{} )
= d() & for t be
Element of (
dom T1) holds (
len t)
<= k1 & ((
len t)
< k1 implies (
succ t)
= { (t
^
<*i*>) : Q[i, (T1
. t)] } & for n, x st x
= (T1
. t) & Q[n, x] holds (T1
. (t
^
<*n*>))
= (S()
. (x,n))) by
A68;
consider T2 be
DecoratedTree of D(), k2 such that
A132: (y
+ 1)
= k2 & (f
. (y
+ 1))
= T2 & (T2
.
{} )
= d() & for t be
Element of (
dom T2) holds (
len t)
<= k2 & ((
len t)
< k2 implies (
succ t)
= { (t
^
<*i*>) : Q[i, (T2
. t)] } & for n, x st x
= (T2
. t) & Q[n, x] holds (T2
. (t
^
<*n*>))
= (S()
. (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*>) : Q[i, (T2
. t2)] } by
A132;
thus { (t
^
<*i*>) : Q[i, (T
. t)] }
c= (
succ t)
proof
let x be
object;
assume
A138: x
in { (t
^
<*i*>) : Q[i, (T
. t)] };
then
A139: ex l st x
= (t
^
<*l*>) & Q[l, (T
. t)];
A140: x
in (
succ t2) by
A132,
A135,
A136,
A138;
T2
in E by
A67,
A132,
FUNCT_1:def 3;
then x
in (
dom T) by
A114,
A140;
hence thesis by
A139;
end;
let n;
assume
A141: Q[n, (T
. t)];
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 thesis by
A132,
A135,
A136,
A141;
end;
theorem ::
TREES_2:38
for T1,T2 be
Tree st for n be
Nat holds (T1
-level n)
= (T2
-level n) holds T1
= T2
proof
let T1,T2 be
Tree such that
A1: for n be
Nat holds (T1
-level n)
= (T2
-level n);
for p be
FinSequence of
NAT holds p
in T1 iff p
in T2
proof
let p be
FinSequence of
NAT ;
A2: T1
= (
union the set of all (T1
-level n) where n be
Nat) by
Th14;
hereby
assume p
in T1;
then
consider Y be
set such that
A3: p
in Y and
A4: Y
in the set of all (T1
-level n) where n be
Nat by
A2,
TARSKI:def 4;
consider n be
Nat such that
A5: Y
= (T1
-level n) by
A4;
Y
= (T2
-level n) by
A1,
A5;
hence p
in T2 by
A3;
end;
assume
A6: p
in T2;
T2
= (
union the set of all (T2
-level n) where n be
Nat) by
Th14;
then
consider Y be
set such that
A7: p
in Y and
A8: Y
in the set of all (T2
-level n) where n be
Nat by
A6,
TARSKI:def 4;
consider n be
Nat such that
A9: Y
= (T2
-level n) by
A8;
Y
= (T1
-level n) by
A1,
A9;
hence thesis by
A7;
end;
hence thesis;
end;
theorem ::
TREES_2:39
for n be
Nat holds (
TrivialInfiniteTree
-level n)
=
{(n
|->
0 )}
proof
set T =
TrivialInfiniteTree ;
let n be
Nat;
set L = { w where w be
Element of T : (
len w)
= n };
set f = (n
|->
0 );
{f}
= L
proof
hereby
let a be
object;
assume a
in
{f};
then
A1: a
= f by
TARSKI:def 1;
f
in T & (
len f)
= n by
CARD_1:def 7;
hence a
in L by
A1;
end;
let a be
object;
assume a
in L;
then
consider w be
Element of T such that
A2: a
= w & (
len w)
= n;
w
in T;
then ex k be
Nat st w
= (k
|->
0 );
then a
= f by
A2,
CARD_1:def 7;
hence thesis by
TARSKI:def 1;
end;
hence thesis;
end;
theorem ::
TREES_2:40
for X,Y be
set holds for B be
c=-linear
Subset of (
PFuncs (X,Y)) holds (
union B)
in (
PFuncs (X,Y))
proof
let X,Y be
set;
let B be
c=-linear
Subset of (
PFuncs (X,Y));
for x be
set st x
in B holds x is
Function;
then
reconsider f = (
union B) as
Function by
Th34;
per cases ;
suppose B
<>
{} ;
then
reconsider D = B as non
empty
functional
set;
A1:
now
let x be
set;
assume x
in the set of all (
dom g) where g be
Element of D;
then
consider g be
Element of D such that
A2: x
= (
dom g);
g
in (
PFuncs (X,Y)) by
TARSKI:def 3;
then ex f be
Function st g
= f & (
dom f)
c= X & (
rng f)
c= Y by
PARTFUN1:def 3;
hence x
c= X by
A2;
end;
A3:
now
let x be
set;
assume x
in the set of all (
rng g) where g be
Element of D;
then
consider g be
Element of D such that
A4: x
= (
rng g);
g
in (
PFuncs (X,Y)) by
TARSKI:def 3;
then ex f be
Function st g
= f & (
dom f)
c= X & (
rng f)
c= Y by
PARTFUN1:def 3;
hence x
c= Y by
A4;
end;
(
rng f)
= (
union the set of all (
rng g) where g be
Element of D) by
FUNCT_1: 110;
then
A5: (
rng f)
c= Y by
A3,
ZFMISC_1: 76;
(
dom f)
= (
union the set of all (
dom g) where g be
Element of D) by
FUNCT_1: 110;
then (
dom f)
c= X by
A1,
ZFMISC_1: 76;
hence thesis by
A5,
PARTFUN1:def 3;
end;
suppose
A6: B
=
{} ;
{} is
PartFunc of X, Y by
RELSET_1: 12;
hence thesis by
A6,
PARTFUN1: 45,
ZFMISC_1: 2;
end;
end;