Journal of Formalized Mathematics
Volume 3, 1991
University of Bialystok
Copyright (c) 1991 Association of Mizar Users

### K\"onig's Lemma

by
Grzegorz Bancerek

Received January 10, 1991

MML identifier: TREES_2
[ Mizar article, MML identifier index ]

```environ

vocabulary TREES_1, FUNCT_1, FINSEQ_1, ZFMISC_1, RELAT_1, BOOLE, ORDERS_1,
ORDINAL1, TARSKI, FINSET_1, CARD_1, ARYTM_1, FUNCOP_1, TREES_2, HAHNBAN;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, XREAL_0, RELAT_1,
FUNCT_1, REAL_1, NAT_1, NUMBERS, FINSEQ_1, FINSET_1, CARD_1, FUNCT_2,
FUNCOP_1, TREES_1;
constructors WELLORD2, REAL_1, NAT_1, FUNCOP_1, TREES_1, XREAL_0, MEMBERED,
XBOOLE_0;
clusters SUBSET_1, RELSET_1, FINSEQ_1, CARD_1, TREES_1, FINSET_1, FUNCOP_1,
RELAT_1, NAT_1, XREAL_0, MEMBERED, ZFMISC_1, XBOOLE_0, NUMBERS, ORDINAL2;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;

begin

reserve x,y,z,a,b,c,X,X1,X2,Y,Z for set,
W,W1,W2 for Tree,
w,w' for Element of W,
f for Function,
D,D' 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
for v1,v2,v st v1 is_a_prefix_of v & v2 is_a_prefix_of v
holds v1,v2 are_c=-comparable;

theorem :: TREES_2:2
for v1,v2,v st v1 is_a_proper_prefix_of v & v2 is_a_prefix_of v holds
v1,v2 are_c=-comparable;

canceled;

theorem :: TREES_2:4
len v1 = k+1 implies ex v2,x st v1 = v2^<*x*> & len v2 = k;

canceled;

theorem :: TREES_2:6
ProperPrefixes (v^<*x*>) = ProperPrefixes v \/ {v};

scheme TreeStruct_Ind { T()->Tree, P[set] }:
for t being Element of T() holds P[t]
provided
P[{}] and
for t being Element of T(), n st P[t] & t^<*n*> in T() holds P[t^<*n*>];

theorem :: TREES_2:7
(for p holds p in W1 iff p in W2) implies W1 = W2;

definition let W1,W2;
redefine pred W1 = W2 means
:: TREES_2:def 1
for p holds p in W1 iff p in W2;
end;

theorem :: TREES_2:8
p in W implies W = W with-replacement (p,W|p);

theorem :: TREES_2:9
p in W & q in W & not p is_a_prefix_of q implies
q in W with-replacement (p,W1);

theorem :: TREES_2:10
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);

definition let IT be Tree;
attr IT is finite-order means
:: TREES_2:def 2
ex n st for t being Element of IT holds not t^<*n*> in IT;
end;

definition
cluster finite-order Tree;
end;

definition let W;
mode Chain of W -> Subset of W means
:: TREES_2:def 3

for p,q st p in it & q in it holds p,q are_c=-comparable;
mode Level of W -> Subset of W means
:: TREES_2:def 4

ex n st it = { w: len w = n};
let w;
func succ w -> Subset of W equals
:: TREES_2:def 5

{ w^<*n*>: w^<*n*> in W };
end;

theorem :: TREES_2:11
for L being Level of W holds L is AntiChain_of_Prefixes of W;

theorem :: TREES_2:12
succ w is AntiChain_of_Prefixes of W;

theorem :: TREES_2:13
for A being AntiChain_of_Prefixes of W, C being Chain of W
ex w st A /\ C c= {w};

definition let W,n;
func W-level n -> Level of W equals
:: TREES_2:def 6

{ w: len w = n };
end;

theorem :: TREES_2:14
w^<*n*> in succ w iff w^<*n*> in W;

theorem :: TREES_2:15
w = {} implies W-level 1 = succ w;

theorem :: TREES_2:16
W = union { W-level n: not contradiction };

theorem :: TREES_2:17
for W being finite Tree holds W = union { W-level n: n <= height W };

theorem :: TREES_2:18
for L being Level of W ex n st L = W-level n;

scheme FraenkelCard { A() ->non empty set, X() -> set, F(set) -> set }:
Card { F(w) where w is Element of A(): w in X() } <=` Card X();

scheme FraenkelFinCard { A() ->non empty set,
X,Y() -> finite set, F(set) -> set }:
card Y() <= card X()
provided
Y() = { F(w) where w is Element of A(): w in X() };

theorem :: TREES_2:19
W is finite-order implies ex n st for w holds
ex B being finite set st B = succ w & card B <= n;

theorem :: TREES_2:20
W is finite-order implies succ w is finite;

definition let W be finite-order Tree;
let w be Element of W;
cluster succ w -> finite;
end;

theorem :: TREES_2:21
{} is Chain of W;

theorem :: TREES_2:22
{{}} is Chain of W;

definition let W;
cluster non empty Chain of W;
end;

definition let W;
let IT be Chain of W;
attr IT is Branch-like means
:: TREES_2:def 7

(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;

definition let W;
cluster Branch-like Chain of W;
end;

definition let W;
mode Branch of W is Branch-like Chain of W;
end;

definition let W;
cluster Branch-like -> non empty Chain of W;
end;

reserve C for Chain of W, B for Branch of W;

theorem :: TREES_2:23
v1 in C & v2 in C implies v1 in
ProperPrefixes v2 or v2 is_a_prefix_of v1;

theorem :: TREES_2:24
v1 in C & v2 in C & v is_a_prefix_of v2 implies
v1 in ProperPrefixes v or v is_a_prefix_of v1;

definition let W;
cluster finite Chain of W;
end;

theorem :: TREES_2:25
for C being finite Chain of W st card C > n
ex p st p in C & len p >= n;

theorem :: TREES_2:26
for C holds { w: ex p st p in C & w is_a_prefix_of p } is Chain of W;

theorem :: TREES_2:27
p is_a_prefix_of q & q in B implies p in B;

theorem :: TREES_2:28
{} in B;

theorem :: TREES_2:29
p in C & q in C & len p <= len q implies p is_a_prefix_of q;

theorem :: TREES_2:30
ex B st C c= B;

scheme FuncExOfMinNat { P[set,Nat], X()->set }:
ex f st dom f = X() & for x st x in X() ex n st f.x = n & P[x,n] &
for m st P[x,m] holds n <= m
provided
for x st x in X() ex n st P[x,n];

scheme InfiniteChain { X()->set, a()->set, Q[set], P[set,set] }:
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
a() in X() & Q[a()] and
for x st x in X() & Q[x] ex y st y in X() & P[x,y] & Q[y];

theorem :: TREES_2:31
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;

theorem :: TREES_2:32
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;

definition let IT be Relation;
attr IT is DecoratedTree-like means
:: TREES_2:def 8
dom IT is Tree;
end;

definition
cluster DecoratedTree-like Function;
end;

definition
mode DecoratedTree is DecoratedTree-like Function;
end;

reserve T,T1,T2 for DecoratedTree;

definition let T;
cluster dom T -> non empty Tree-like;
end;

definition let X be set;
mode ParametrizedSubset of X -> Relation means
:: TREES_2:def 9
rng it c= X;
end;

definition let D;
cluster DecoratedTree-like Function-like ParametrizedSubset of D;
end;

definition let D;
mode DecoratedTree of D is
DecoratedTree-like Function-like ParametrizedSubset of D;
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;
end;

theorem :: TREES_2:33
dom T1 = dom T2 & (for p st p in dom T1 holds T1.p = T2.p) implies T1 = T2;

scheme DTreeEx { T() -> Tree, P[set,set] }:
ex T st dom T = T() & for p st p in T() holds P[p,T.p]
provided
for p st p in T() ex x st P[p,x];

scheme DTreeLambda { T() -> Tree, f(set) -> set }:
ex T st dom T = T() & for p st p in T() holds T.p = f(p);

definition let T;
func Leaves T -> set equals
:: TREES_2:def 10

T.:Leaves dom T;
let p;
func T|p -> DecoratedTree means
:: TREES_2:def 11

dom it = (dom T)|p & for q st q in (dom T)|p holds it.q = T.(p^q);
end;

theorem :: TREES_2:34
p in dom T implies rng (T|p) c= rng T;

definition let D; let T be DecoratedTree of D;
redefine func Leaves T -> Subset of D;
let p be Element of dom T;
func T|p -> DecoratedTree of D;
end;

definition let T,p,T1;
assume
p in dom T;
func T with-replacement (p,T1) -> DecoratedTree means
:: TREES_2:def 12
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;
end;

definition let W,x;
cluster W --> x -> DecoratedTree-like;
end;

definition let D be non empty set; let W; let d be Element of D;
redefine func W --> d -> DecoratedTree of D;
end;

theorem :: TREES_2:35
(for x st x in D holds x is Tree) implies union D is Tree;

theorem :: TREES_2:36
(for x st x in X holds x is Function) & X is c=-linear
implies
union X is Relation-like Function-like;

theorem :: TREES_2:37
(for x st x in D holds x is DecoratedTree) & D is c=-linear
implies union D is DecoratedTree;

theorem :: TREES_2:38
(for x st x in D' holds x is DecoratedTree of D) &
D' is c=-linear implies
union D' is DecoratedTree of D;

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,x st x = T.t & n in F(x) holds T.(t^<*n*>) = S().[x,n]
provided
for d being Element of D(), k1,k2 st k1 <= k2 & k2 in F(d) holds k1 in F(d);

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,x st x = T.t & n < F(x) holds T.(t^<*n*>) = S().[x,n];
```

Back to top