:: K\"onig's Lemma
:: by Grzegorz Bancerek
::
:: Received January 10, 1991
:: Copyright (c) 1991-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, TREES_1, SUBSET_1, FUNCT_1, XBOOLE_0, FINSEQ_1,
ORDINAL4, XXREAL_0, ARYTM_3, RELAT_1, TARSKI, CARD_1, NAT_1, ORDINAL1,
FINSET_1, REAL_1, ARYTM_1, ZFMISC_1, FUNCOP_1, TREES_2, AMISTD_3,
FINSEQ_2, PARTFUN1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, RELAT_1, XCMPLX_0,
FUNCT_1, PARTFUN1, XREAL_0, REAL_1, NAT_1, CARD_1, NUMBERS, FINSEQ_1,
FINSEQ_2, FINSET_1, RELSET_1, BINOP_1, FUNCT_2, FUNCOP_1, TREES_1,
XXREAL_0;
constructors WELLORD2, BINOP_1, FUNCOP_1, XXREAL_0, REAL_1, NAT_1, TREES_1,
RELSET_1, FINSEQ_2, XREAL_0, NUMBERS;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, FUNCOP_1,
FINSET_1, NUMBERS, XXREAL_0, XREAL_0, NAT_1, FINSEQ_1, TREES_1, CARD_1,
FINSEQ_2, PARTFUN1;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
definitions RELAT_1, TARSKI, FUNCT_1, TREES_1, ORDINAL1, XBOOLE_0;
equalities TREES_1, BINOP_1, ORDINAL1;
expansions RELAT_1, TARSKI, FUNCT_1, TREES_1, ORDINAL1, XBOOLE_0;
theorems FUNCT_1, NAT_1, FINSEQ_1, TREES_1, TARSKI, ORDERS_1, ZFMISC_1,
FINSET_1, CARD_1, CARD_2, WELLORD2, FUNCOP_1, FUNCT_2, RELAT_1, FINSEQ_2,
ORDINAL1, XBOOLE_0, XBOOLE_1, XREAL_1, XXREAL_0, PARTFUN1, RELSET_1,
XTUPLE_0, XREAL_0;
schemes FUNCT_1, FRAENKEL, NAT_1, CARD_2, CLASSES1, DOMAIN_1, XBOOLE_0,
XFAMILY;
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 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 being FinSequence st r = p^p9 by TREES_1:1;
assume q is_a_prefix_of r;
then A2: ex q9 being FinSequence st r = q^q9 by TREES_1:1;
len p <= len q or len q <= len p;
then (ex t being FinSequence st p^t = q) or
ex t being 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 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 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,40;
end;
theorem 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 TreeStructInd { T()->Tree, P[set] }:
for t being Element of T() holds P[t]
provided
A1: P[{}] and
A2: for t being Element of T(), n st P[t] & t^<*n*> in T() holds P[t^<*n*>]
proof
defpred X[set] means for t being 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 being 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 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;
redefine pred W1 = W2 means :: redefines = (XBOOLE_0, redefinition) → = (HIDDEN, definition)
for p holds p in W1 iff p in W2;
compatibility by Th5;
end;
theorem
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 being 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 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
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,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,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;
attr IT is finite-order means
ex n st for t being 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;
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;
mode Level of W -> Subset of W means
: Def4:
ex n being 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;
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
for L being Level of W holds L is AntiChain_of_Prefixes of W
proof
let L be Level of W;
consider n being 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
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
for A being AntiChain_of_Prefixes of W, C being Chain of W
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;
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
w^<*n*> in succ w iff w^<*n*> in W;
theorem
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,39;
hence thesis by A5;
end;
theorem 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
for W being 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
for L being Level of W ex n st L = W-level n
proof
let L be Level of W;
consider n being Nat such that
A1: L = { w: len w = n} by Def4;
reconsider n as Nat;
take n;
thus thesis by A1;
end;
scheme FraenkelCard { A() ->non empty set, X() -> set, F(object) -> set }:
card { F(w) where w is Element of A(): w in X() } c= card X()
proof
consider f such that
A1: dom f = X() & for x being object st x in X() holds f.x = F(x)
from FUNCT_1:sch 3;
{ F(w) where w is Element of A(): w in X() } c= rng f
proof
let x be object;
assume x in { F(w) where w is Element of A(): w in X() };
then consider w being 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 FraenkelFinCard { A() ->non empty set,
X,Y() -> finite set, F(set) -> set }: card Y() <= card X()
provided
A1: Y() = { F(w) where w is Element of A(): w in X() }
proof
card { F(w) where w is 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 Th17:
W is finite-order implies ex n st for w holds
ex B being 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 is Element of REAL: r in Seg n }
is finite from FRAENKEL:sch 21(A2
);
A4: succ w c= { w^<*r-1*> where r is 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 is 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 is 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 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 being finite set st B = succ w & card B <= n by Th17;
ex B being 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 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 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;
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 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 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 Th23:
for C being finite Chain of W st card C > n 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 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 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 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 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 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 being 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 FuncExOfMinNat { P[object,Nat], X()->set }:
ex f st dom f = X() &
for x being object st x in X() ex n st f.x = n & P[x,n] &
for m st P[x,m] holds n <= m
provided
A1: for x being object st x in X() ex n st P[x,n]
proof
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 being object st x in X() ex y being 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 being 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 being 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 being object holds P[x,y] & P[y,x] implies x = y by XXREAL_0:1;
A7: for x,y,z being object st P[x,y] & P[y,z] holds P[x,z] by XXREAL_0:2;
consider x being object such that
A8: x in XN & for y being 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 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 being object st x in X() & Q[x]
ex y being object st y in X() & P[x,y] & Q[y]
proof
consider Y such that
A3: for x being 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 being object st x in Y ex y being 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 being 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 being 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 being Nat holds f.(n+1) = U(n,f.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 being 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 Th29:
for T being Tree st (for n ex C being finite Chain of T st card C = n) &
for t being Element of T holds succ t is finite
ex B being Chain of T st not B is finite
proof
let T be Tree;
assume that
A1: for n ex X being finite Chain of T st card X = n and
A2: for t being Element of T holds succ t is finite;
defpred P[FinSequence] means for n ex B being Branch of T st
$1 in B & ex p st p in B & len p >= len $1 + n;
A3: for x being Element of T st P[x] 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 being Branch of T,p,q st
p = $1 & $1 in B & q in B holds len p + $2 > len q;
A7: for y being object st y in succ x 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 being Branch of T st x^<*k*> in B 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 being object st y in succ x 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 being 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 being 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,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 being 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 being 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 being Branch of T st e in B for p st p in B holds len p < len e + n;
consider C being finite Chain of T such that
A30: card C = n+1 by A1;
consider B being 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 being 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 being object st x in T & QQ[x]
ex y being object st y in T & PP[x,y] & QQ[y]
proof
let x being object such that x in T;
given t being 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 being 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 being object such that
A55: x in NAT and
A56: p = f.x by A39,A53,FUNCT_1:def 3;
consider y being 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;
::$N Koenig Lemma
theorem
for T being finite-order Tree st
for n ex C being finite Chain of T st card C = n
ex B being Chain of T st not B is finite
proof
let T be finite-order Tree;
for t being Element of T holds succ t is finite;
hence thesis by Th29;
end;
definition
let IT be Relation;
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-like D-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;
redefine func T.t -> Element of D; :: redefines . (FUNCT_1, definition)
coherence
proof
T.t in rng T & rng T c= D by FUNCT_1:def 3;
hence thesis;
end;
end;
theorem 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 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() ex x st P[p,x]
proof
A2: for x being object st x in T() ex y being 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 being 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 DTreeLambda { T() -> Tree, f(object) -> set }:
ex T st dom T = T() & for p st p in T() holds T.p = f(p)
proof
consider f such that
A1: dom f = T() & for x being 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;
func Leaves T -> set equals
T.:Leaves dom T;
correctness;
let p;
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 being 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 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 being 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;
redefine func Leaves T -> Subset of D; :: redefines Leaves (TREES_2, definition)
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;
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) 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 being 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 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 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 being object holds a in union X implies
ex b,c being 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 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 being object st x in D ex y being 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 being 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 being 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 being 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 being 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 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 being 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 DTreeStructEx
{ D() -> non empty set, d() -> Element of D(), F(set) -> set,
S() -> Function of [:D(),NAT:],D()}:
ex T being DecoratedTree of D() st T.{} = d() &
for t being Element of dom T holds succ t = { t^<*k*>: k in F(T.t)} &
for n st n in F(T.t) holds T.(t^<*n*>) = S().(T.t,n)
provided
A1: for d being Element of D(), k1,k2 st k1 <= k2 & k2 in F(d) holds k1 in F(d)
proof
defpred P[Nat] means
ex T being DecoratedTree of D() st T.{} = d() &
for t being Element of dom T holds len t <= $1 &
(len t < $1 implies succ t = { t^<*k*>: k in F(T.t)} &
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 being Element of dom T holds len t <= k &
(len t < k implies succ t = { t^<*m*>: m in F(T.t)} &
for n,x st x = T.t & n in F(x) holds T.(t^<*n*>) = S().(x,n));
reconsider M
= { t^<*n*> where t is Element of dom T: n in F(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 is Element of dom T: n in F(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 being Element of dom T such that
A7: x = t^<*n*> & n in F (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 is Element of dom T: n in F(T.t) } or
p in dom T by XBOOLE_0:def 3;
now
assume p in { t^<*n*> where t is Element of dom T: n in F(T.t) };
then consider n be Nat, t be Element of dom T such that
A9: p = t^<*n*> and n in F(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 is Element of dom T: l in F(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: l in F(T.t) by A14,A15,TREES_1:def 3;
A19: len (p^<*m*>) = len p + len <*m*> & len <*m*> = 1 by FINSEQ_1:22,40
;
A20: len (t^<*l*>) = len t + len <*l*> & len <*l*> = 1 by FINSEQ_1:22,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(T.t) by A1,A15,A17,A18,A19,A20,A21;
then p^<*n*> in { s^<*i*> where s is Element of dom T: i in F(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 ex x st P[p,x]
proof
let p;
assume p in M;
then A24: p in { t^<*l*> where t is Element of dom T: l in F(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 l in F(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 being 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 is Element of dom T: l in F(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 l in F(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 is Element of dom T: l in F(T.s) };
then consider l be Nat, s being Element of dom T such that
A42: t = s^<*l*> and l in F(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 is Element of dom T: l in F(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: l in F(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*>: m in F(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*>: i in F(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*>: m in F(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 is Element of dom T: l in F(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: l in F(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*>: i in F(T9.t)} c= succ t
proof
let x be object;
assume x in { t^<*i*>: i in F(T9.t)};
then consider n such that
A56: x = t^<*n*> and
A57: n in F(T9.t);
x = t9^<*n*> by A56;
then x in { s^<*l*> where s is Element of dom T: l in F(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: n in F(x);
t^<*n*> in { t^<*i*>: i in F(T9.t)} 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 being DecoratedTree of D(), k st
$1 = k & $2 = T & T.{} = d() &
for t being Element of dom T holds len t <= k &
(len t < k implies succ t = { t^<*i*>: i in F(T.t)} &
for n,x st x = T.t & n in F(x) holds T.(t^<*n*>) = S().(x,n));
A65: for x being object st x in NAT ex y being object st P[x,y]
proof
let x be object;
assume x in NAT;
then reconsider N = x as Nat;
consider T being DecoratedTree of D() such that
A66: T.{} = d() & for t being Element of dom T holds len t <= N &
(len t < N implies succ t = { t^<*k*>: k in F(T.t)} &
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 being object st x in NAT holds P[x,f.x] from CLASSES1:sch 1(A65);
A68: for x being 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 being object such that
A70: y in dom f and
A71: x = f.y by FUNCT_1:def 3;
ex T being DecoratedTree of D(), k st y = k & f.y = T & T.{} = d() &
for t being Element of dom T holds len t <= k &
(len t < k implies succ t = { t^<*i*>: i in F(T.t)} &
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 being DecoratedTree of D(), k1 such that
A76: x = k1 & f.x = T19 & T19.{} = d() &
for t being Element of dom T19 holds len t <= k1 &
(len t < k1 implies succ t = { t^<*i*>: i in F(T19.t)} &
for n,x st x = T19.t & n in F(x) holds T19.(t^<*n*>) = S().(x,n))
by A68;
consider T29 being DecoratedTree of D(), k2 such that
A77: y = k2 & f.y = T29 & T29.{} = d() &
for t being Element of dom T29 holds len t <= k2 &
(len t < k2 implies succ t = { t^<*i*>: i in F(T29.t)} &
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 being 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 being 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 being FinSequence, x being object such that
A89: t = q^<*x*> by FINSEQ_1:46;
A90: p
is_a_prefix_of t & q is_a_prefix_of t by A89,TREES_1:1;
k+1 = len q + 1 by A83,A89,FINSEQ_2:16;
then A91: p = q by A86,A90,Th1,TREES_1:4;
<*x*> is FinSequence of NAT by A89,FINSEQ_1:36;
then A92: rng <*x*> c= NAT by FINSEQ_1:def 4;
rng <*x*> = {x} & x in {x} by FINSEQ_1:38,TARSKI:def 1;
then reconsider x as Nat by A92;
A93: p^<*x*> in succ p by A89,A91;
succ p = { p^<*i*>: i in F(T1.p)} by A73,A76,A86,A87;
then consider i such that
A94: p^<*x*> = p^<*i*> and
A95: i in F(T1.p) by A93;
A96: k < k2 by A75,A76,A77,A87,XXREAL_0:2;
then A97: succ p9 = { p9^<*l*>: l in F(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 being object such that
A102: [y,z] = x by RELAT_1:def 1;
A103: T1.y = z by A101,A102,FUNCT_1:1;
reconsider y 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 being 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 being object such that
A108: y in dom f and
A109: T2 = f.y by FUNCT_1:def 3;
A110: T1 is DecoratedTree by A69,A104;
A111: T2 is DecoratedTree by A69,A107;
reconsider x,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 being DecoratedTree of D(), k such that
A112: 0 = k & f.0 = T9 & T9.{} = d() &
for t being Element of dom T9 holds len t <= k &
(len t < k implies succ t = { t^<*i*>: i in F(T9.t)} &
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(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 being object such that
A121: y in NAT and
A122: X = f.y by A67,A120,FUNCT_1:def 3;
consider T1 being DecoratedTree of D(), k1 such that
A123: y = k1 & f.y = T1 & T1.{} = d() &
for t being Element of dom T1 holds len t <= k1 &
(len t < k1 implies succ t = { t^<*i*>: i in F(T1.t)} &
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(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 being 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 being DecoratedTree of D(), k1 such that
A131: y = k1 & f.y = T1 & T1.{} = d() &
for t being Element of dom T1 holds len t <= k1 &
(len t < k1 implies succ t = { t^<*i*>: i in F(T1.t)} &
for n,x st x = T1.t & n in F(x) holds T1.(t^<*n*>) = S().(x,n))
by A68;
consider T2 being DecoratedTree of D(), k2 such that
A132: y+1 = k2 & f.(y+1) = T2 & T2.{} = d() &
for t being Element of dom T2 holds len t <= k2 &
(len t < k2 implies succ t = { t^<*i*>: i in F(T2.t)} &
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(T2.t2)} by A132;
thus { t^<*i*>: i in F(T.t)} c= succ t
proof
let x be object;
assume
A138: x in { t^<*i*>: i in F(T.t)};
then A139: ex l st x = t^<*l*> & l in F(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: n in F(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;
scheme DTreeStructFinEx
{ D() -> non empty set, d() -> Element of D(), F(set) -> Nat,
S() -> Function of [:D(),NAT:],D()}:
ex T being DecoratedTree of D() st T.{} = d() &
for t being Element of dom T holds succ t = { t^<*k*>: k < F(T.t)} &
for n st n < F(T.t) holds T.(t^<*n*>) = S().(T.t,n)
proof
deffunc FF(Nat) = { i: i < $1};
deffunc U(set) = FF(F($1));
A1: for d being 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 being DecoratedTree of D() such that
A3: T.{} = d() &
for t being Element of dom T holds succ t = { t^<*k*>: k in U(T.t)} &
for n st n in U(T.t) 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(T.t))} by A3;
thus succ t c= { t^<*i*>: i < F(T.t)}
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(T.t)) by A4;
ex i st l = i & i < F(T.t) by A6;
hence thesis by A5;
end;
thus { t^<*i*>: i < F(T.t)} c= succ t
proof
let x be object;
assume x in { t^<*i*>: i < F(T.t)};
then consider l such that
A7: x = t^<*l*> and
A8: l < F(T.t);
l in FF(F(T.t)) by A8;
hence thesis by A4,A7;
end;
let n;
assume n < F(T.t);
then n in FF(F(T.t));
hence thesis by A3;
end;
begin :: Addenda
:: from PRELAMB
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;
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;
:: from MODAL_1, 2007.03.14, A.T.
reserve x1,x2 for set,
w for FinSequence of NAT;
theorem
for Z1,Z2 being Tree,p being FinSequence of NAT st p in Z1 holds
for v being Element of Z1 with-replacement (p,Z2),w being 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 being object st x in succ t ex y being 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 being Function such that
A10: dom f = succ t & for x being 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 being 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 DTreeStructEx
{ D() -> non empty set, d() -> Element of D(), Q[set,set],
S() -> Function of [:D(),NAT:],D()}:
ex T being DecoratedTree of D() st T.{} = d() &
for t being 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 being Element of D(), k1,k2 st k1 <= k2 & Q[k2,d] holds Q[k1,d]
proof
defpred P[Nat] means
ex T being DecoratedTree of D() st T.{} = d() &
for t being 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 being 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 is 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 is 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 being 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 is 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 is 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 is 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,40
;
A20: len (t^<*l*>) = len t + len <*l*> & len <*l*> = 1 by FINSEQ_1:22,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 is 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 ex x st P[p,x]
proof
let p;
assume p in M;
then A24: p in { t^<*l*> where t is 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 being 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 is 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 is Element of dom T: Q[l,T.s] };
then consider l be Nat, s being 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 is 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 is 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 is 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 being DecoratedTree of D(), k st
$1 = k & $2 = T & T.{} = d() &
for t being 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 being object st x in NAT ex y being object st P[x,y]
proof
let x be object;
assume x in NAT;
then reconsider n = x as Nat;
consider T being DecoratedTree of D() such that
A66: T.{} = d() & for t being 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 being object st x in NAT holds P[x,f.x]
from CLASSES1:sch 1(A65);
A68: for x being 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 being object such that
A70: y in dom f and
A71: x = f.y by FUNCT_1:def 3;
ex T being DecoratedTree of D(), k st y = k & f.y = T & T.{} = d() &
for t being 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 being DecoratedTree of D(), k1 such that
A76: x = k1 & f.x = T19 & T19.{} = d() &
for t being 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 being DecoratedTree of D(), k2 such that
A77: y = k2 & f.y = T29 & T29.{} = d() &
for t being 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 being 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 being 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 being FinSequence, x being object such that
A89: t = q^<*x*> by FINSEQ_1:46;
A90: p
is_a_prefix_of t & q is_a_prefix_of t by A89,TREES_1:1;
k+1 = len q + 1 by A83,A89,FINSEQ_2:16;
then A91: p = q by A86,A90,Th1,TREES_1:4;
<*x*> is FinSequence of NAT by A89,FINSEQ_1:36;
then A92: rng <*x*> c= NAT by FINSEQ_1:def 4;
rng <*x*> = {x} & x in {x} by FINSEQ_1:38,TARSKI:def 1;
then reconsider x 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 being object such that
A102: [y,z] = x by RELAT_1:def 1;
A103: T1.y = z by A101,A102,FUNCT_1:1;
reconsider y 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 being 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 being object such that
A108: y in dom f and
A109: T2 = f.y by FUNCT_1:def 3;
A110: T1 is DecoratedTree by A69,A104;
A111: T2 is DecoratedTree by A69,A107;
reconsider x,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 being DecoratedTree of D(), k such that
A112: 0 = k & f.0 = T9 & T9.{} = d() &
for t being 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 being object such that
A121: y in NAT and
A122: X = f.y by A67,A120,FUNCT_1:def 3;
consider T1 being DecoratedTree of D(), k1 such that
A123: y = k1 & f.y = T1 & T1.{} = d() &
for t being 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 being 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 being DecoratedTree of D(), k1 such that
A131: y = k1 & f.y = T1 & T1.{} = d() &
for t being 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 being DecoratedTree of D(), k2 such that
A132: y+1 = k2 & f.(y+1) = T2 & T2.{} = d() &
for t being 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;
:: from AMISTD_3, 2010.01.10, A.T.
theorem
for T1, T2 being Tree st
for n being Nat holds T1-level n = T2-level n
holds T1 = T2
proof
let T1, T2 be Tree such that
A1: for n being Nat holds T1-level n = T2-level n;
for p being 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 is Nat
by Th14;
hereby
assume p in T1;
then consider Y being set such that
A3: p in Y and
A4: Y in the set of all T1-level n where n is Nat
by A2,TARSKI:def 4;
consider n being 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 is Nat
by Th14;
then consider Y being set such that
A7: p in Y and
A8: Y in the set of all T2-level n where n is Nat
by A6,TARSKI:def 4;
consider n being 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
for n being Nat holds TrivialInfiniteTree-level n = { n |-> 0 }
proof
set T = TrivialInfiniteTree;
let n be Nat;
set L = { w where w is 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 being Element of T such that
A2: a = w & len w = n;
w in T;
then ex k being 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
for X,Y being set for B being 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 is Element of D;
then consider g being Element of D such that
A2: x = dom g;
g in PFuncs(X,Y) by TARSKI:def 3;
then ex f being 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 is Element of D;
then consider g being Element of D such that
A4: x = rng g;
g in PFuncs(X,Y) by TARSKI:def 3;
then ex f being 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 is 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 is 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;