:: K\"onig's Lemma
:: by Grzegorz Bancerek
::
:: Received January 10, 1991
:: Copyright (c) 1991-2012 Association of Mizar Users


begin

theorem Th1: :: TREES_2:1
for v1, v2, v being FinSequence st v1 is_a_prefix_of v & v2 is_a_prefix_of v holds
v1,v2 are_c=-comparable
proofend;

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

theorem Th3: :: TREES_2:3
for k being Element of NAT
for v1 being FinSequence st len v1 = k + 1 holds
ex v2 being FinSequence ex x being set st
( v1 = v2 ^ <*x*> &amp; len v2 = k )
proofend;

theorem Th4: :: TREES_2:4
for x being set
for v being FinSequence holds ProperPrefixes (v ^ <*x*>) = (ProperPrefixes v) \/ {v}
proofend;

scheme :: TREES_2:sch 1
TreeStructInd{ F1() ->  Tree, P1[ set ] } :
 for t being Element of F1() holds P1[t]
provided
A1: P1[ {} ] and
A2: for t being Element of F1()
for n being Element of NAT st P1[t] &amp; t ^ <*n*> in F1() holds
P1[t ^ <*n*>]
proofend;

theorem Th5: :: TREES_2:5
for W1, W2 being Tree st ( for p being FinSequence of NAT holds
( p in W1 iff p in W2 ) ) holds
W1 = W2
proofend;

definition
let W1, W2 be Tree;
redefine pred W1 = W2 means :: TREES_2:def 1
 for p being FinSequence of NAT holds
( p in W1 iff p in W2 );
compatibility
 ( W1 = W2 iff for p being FinSequence of NAT holds
( p in W1 iff p in W2 ) ) by Th5;
end;

:: deftheorem  defines = TREES_2:def_1_:_
 for W1, W2 being Tree holds
( W1 = W2 iff for p being FinSequence of NAT holds
( p in W1 iff p in W2 ) );

theorem :: TREES_2:6
for W being Tree
for p being FinSequence of NAT st p in W holds
W = W with-replacement (p,(W | p))
proofend;

theorem Th7: :: TREES_2:7
for W, W1 being Tree
for p, q being FinSequence of NAT st p in W &amp; q in W &amp; not p is_a_prefix_of q holds
q in W with-replacement (p,W1)
proofend;

theorem :: TREES_2:8
for W, W1, W2 being Tree
for p, q being FinSequence of NAT st p in W &amp; q in W &amp; not p,q are_c=-comparable holds
(W with-replacement (p,W1)) with-replacement (q,W2) = (W with-replacement (q,W2)) with-replacement (p,W1)
proofend;

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

:: deftheorem  defines finite-order TREES_2:def_2_:_
 for IT being Tree holds
( IT is finite-order iff ex n being Element of NAT st
for t being Element of IT holds not t ^ <*n*> in IT );

registration
cluster non empty Tree-like finite-order for set ;
existence
 ex b1 being Tree st b1 is finite-order
proofend;
end;

definition
let W be Tree;
mode Chain of W ->  Subset of W means :Def3: :: TREES_2:def 3
 for p, q being FinSequence of NAT st p in it &amp; q in it holds
p,q are_c=-comparable ;
existence
 ex b1 being Subset of W st
for p, q being FinSequence of NAT st p in b1 &amp; q in b1 holds
p,q are_c=-comparable
proofend;
mode Level of W ->  Subset of W means :Def4: :: TREES_2:def 4
 ex n being Nat st it =  {  w where w is Element of W : len w = n  }  ;
existence
 ex b1 being Subset of W ex n being Nat st b1 =  {  w where w is Element of W : len w = n  }
proofend;
let w be Element of W;
func succ w ->  Subset of W equals :: TREES_2:def 5
 {  (w ^ <*n*>) where n is Element of NAT : w ^ <*n*> in W  }  ;
coherence
  {  (w ^ <*n*>) where n is Element of NAT : w ^ <*n*> in W  }  is Subset of W
proofend;
end;

:: deftheorem Def3 defines Chain TREES_2:def_3_:_
 for W being Tree
for b2 being Subset of W holds
( b2 is Chain of W iff for p, q being FinSequence of NAT st p in b2 &amp; q in b2 holds
p,q are_c=-comparable );

:: deftheorem Def4 defines Level TREES_2:def_4_:_
 for W being Tree
for b2 being Subset of W holds
( b2 is Level of W iff ex n being Nat st b2 =  {  w where w is Element of W : len w = n  }  );

:: deftheorem  defines succ TREES_2:def_5_:_
 for W being Tree
for w being Element of W holds succ w =  {  (w ^ <*n*>) where n is Element of NAT : w ^ <*n*> in W  }  ;

theorem :: TREES_2:9
for W being Tree
for L being Level of W holds L is AntiChain_of_Prefixes of W
proofend;

theorem :: TREES_2:10
for W being Tree
for w being Element of W holds succ w is AntiChain_of_Prefixes of W
proofend;

theorem :: TREES_2:11
for W being Tree
for A being AntiChain_of_Prefixes of W
for C being Chain of W ex w being Element of W st A /\ C c= {w}
proofend;

definition
let W be Tree;
let n be Nat;
funcW -level n ->  Level of W equals :: TREES_2:def 6
 {  w where w is Element of W : len w = n  }  ;
coherence
  {  w where w is Element of W : len w = n  }  is Level of W
proofend;
end;

:: deftheorem  defines -level TREES_2:def_6_:_
 for W being Tree
for n being Nat holds W -level n =  {  w where w is Element of W : len w = n  }  ;

theorem :: TREES_2:12
for W being Tree
for w being Element of W
for n being Element of NAT holds
( w ^ <*n*> in succ w iff w ^ <*n*> in W ) ;

theorem :: TREES_2:13
for W being Tree
for w being Element of W st w = {} holds
W -level 1 = succ w
proofend;

theorem Th14: :: TREES_2:14
for W being Tree holds W = union  {  (W -level n) where n is Element of NAT : verum  }
proofend;

theorem :: TREES_2:15
for W being finite Tree holds W = union  {  (W -level n) where n is Element of NAT : n <= height W  }
proofend;

theorem :: TREES_2:16
for W being Tree
for L being Level of W ex n being Element of NAT st L = W -level n
proofend;

scheme :: TREES_2:sch 2
FraenkelCard{ F1() ->  non empty set , F2() ->  set , F3( set ) ->  set } :
 card  {  F3(w) where w is Element of F1() : w in F2()  }  c= card F2()
proofend;

scheme :: TREES_2:sch 3
FraenkelFinCard{ F1() ->  non empty set , F2() ->  finite set , F3() ->  finite set , F4( set ) ->  set } :
 card F3() <= card F2()
provided
A1: F3() =  {  F4(w) where w is Element of F1() : w in F2()  }
proofend;

theorem Th17: :: TREES_2:17
for W being Tree st W is finite-order holds
ex n being Element of NAT st
for w being Element of W ex B being finite set st
( B = succ w &amp; card B <= n )
proofend;

theorem Th18: :: TREES_2:18
for W being Tree
for w being Element of W st W is finite-order holds
succ w is finite
proofend;

registration
let W be finite-order Tree;
let w be Element of W;
cluster succ w ->  finite ;
coherence
 succ w is finite by Th18;
end;

theorem Th19: :: TREES_2:19
for W being Tree holds {} is Chain of W
proofend;

theorem Th20: :: TREES_2:20
for W being Tree holds {{}} is Chain of W
proofend;

registration
let W be Tree;
cluster non empty for Chain of W;
existence
 not for b1 being Chain of W holds b1 is empty
proofend;
end;

definition
let W be Tree;
let IT be Chain of W;
attrIT is Branch-like  means :Def7: :: TREES_2:def 7
( ( for p being FinSequence of NAT st p in IT holds
ProperPrefixes p c= IT ) &amp; ( for p being FinSequence of NAT holds
( not p in W or ex q being FinSequence of NAT st
( q in IT &amp; not q is_a_proper_prefix_of p ) ) ) );
end;

:: deftheorem Def7 defines Branch-like TREES_2:def_7_:_
 for W being Tree
for IT being Chain of W holds
( IT is Branch-like iff ( ( for p being FinSequence of NAT st p in IT holds
ProperPrefixes p c= IT ) &amp; ( for p being FinSequence of NAT holds
( not p in W or ex q being FinSequence of NAT st
( q in IT &amp; not q is_a_proper_prefix_of p ) ) ) ) );

registration
let W be Tree;
cluster Branch-like for Chain of W;
existence
 ex b1 being Chain of W st b1 is Branch-like
proofend;
end;

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

registration
let W be Tree;
cluster Branch-like  ->  non empty for Chain of W;
coherence
 for b1 being Chain of W st b1 is Branch-like holds
not b1 is empty
proofend;
end;

theorem Th21: :: TREES_2:21
for W being Tree
for v1, v2 being FinSequence
for C being Chain of W st v1 in C &amp; v2 in C &amp; not v1 in ProperPrefixes v2 holds
v2 is_a_prefix_of v1
proofend;

theorem Th22: :: TREES_2:22
for W being Tree
for v1, v2, v being FinSequence
for C being Chain of W st v1 in C &amp; v2 in C &amp; v is_a_prefix_of v2 &amp; not v1 in ProperPrefixes v holds
v is_a_prefix_of v1
proofend;

registration
let W be Tree;
cluster finite for Chain of W;
existence
 ex b1 being Chain of W st b1 is finite
proofend;
end;

theorem Th23: :: TREES_2:23
for W being Tree
for n being Element of NAT
for C being finite Chain of W st card C > n holds
ex p being FinSequence of NAT st
( p in C &amp; len p >= n )
proofend;

theorem Th24: :: TREES_2:24
for W being Tree
for C being Chain of W holds  {  w where w is Element of W : ex p being FinSequence of NAT st
( p in C &amp; w is_a_prefix_of p )  }  is Chain of W
proofend;

theorem Th25: :: TREES_2:25
for W being Tree
for p, q being FinSequence of NAT
for B being Branch of W st p is_a_prefix_of q &amp; q in B holds
p in B
proofend;

theorem Th26: :: TREES_2:26
for W being Tree
for B being Branch of W holds {} in B
proofend;

theorem Th27: :: TREES_2:27
for W being Tree
for p, q being FinSequence of NAT
for C being Chain of W st p in C &amp; q in C &amp; len p <= len q holds
p is_a_prefix_of q
proofend;

theorem Th28: :: TREES_2:28
for W being Tree
for C being Chain of W ex B being Branch of W st C c= B
proofend;

scheme :: TREES_2:sch 4
FuncExOfMinNat{ P1[ set , Nat], F1() ->  set } :
 ex f being Function st
( dom f = F1() &amp; ( for x being set st x in F1() holds
ex n being Element of NAT st
( f . x = n &amp; P1[x,n] &amp; ( for m being Element of NAT st P1[x,m] holds
n <= m ) ) ) )
provided
A1: for x being set st x in F1() holds
ex n being Element of NAT st P1[x,n]
proofend;

Lm1:  for X being set st X is finite holds
ex n being Element of NAT st
for k being Element of NAT st k in X holds
k <= n
proofend;

scheme :: TREES_2:sch 5
InfiniteChain{ F1() ->  set , F2() ->  set , P1[ set ], P2[ set , set ] } :
 ex f being Function st
( dom f = NAT &amp; rng f c= F1() &amp; f . 0 = F2() &amp; ( for k being Element of NAT holds
( P2[f . k,f . (k + 1)] &amp; P1[f . k] ) ) )
provided
A1: ( F2() in F1() &amp; P1[F2()] ) and
A2: for x being set st x in F1() &amp; P1[x] holds
ex y being set st
( y in F1() &amp; P2[x,y] &amp; P1[y] )
proofend;

theorem Th29: :: TREES_2:29
for T being Tree st ( for n being Element of NAT ex C being finite Chain of T st card C = n ) &amp; ( for t being Element of T holds succ t is finite ) holds
ex B being Chain of T st not B is finite
proofend;

:: [WP: ] Koenig_Lemma
theorem :: TREES_2:30
for T being finite-order Tree st ( for n being Element of NAT ex C being finite Chain of T st card C = n ) holds
ex B being Chain of T st not B is finite
proofend;

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

:: deftheorem Def8 defines DecoratedTree-like TREES_2:def_8_:_
 for IT being Relation holds
( IT is DecoratedTree-like iff dom IT is Tree );

registration
cluster Relation-like Function-like DecoratedTree-like for set ;
existence
 ex b1 being Function st b1 is DecoratedTree-like
proofend;
end;

definition
mode DecoratedTree is DecoratedTree-like Function;
end;

registration
let T be DecoratedTree;
cluster dom T ->  non empty Tree-like ;
coherence
 ( not dom T is empty &amp; dom T is Tree-like ) by Def8;
end;

registration
let D be non empty set ;
cluster Relation-like D -valued Function-like DecoratedTree-like for set ;
existence
 ex b1 being Function st
( b1 is DecoratedTree-like &amp; b1 is D -valued )
proofend;
end;

definition
let D be non empty set ;
mode DecoratedTree of D is D -valued DecoratedTree;
end;

definition
let D be non empty set ;
let T be DecoratedTree of D;
let t be Element of dom T;
:: original:.
redefine funcT . t ->  Element of D;
coherence
 T . t is Element of D
proofend;
end;

theorem Th31: :: TREES_2:31
for T1, T2 being DecoratedTree st dom T1 = dom T2 &amp; ( for p being FinSequence of NAT st p in dom T1 holds
T1 . p = T2 . p ) holds
T1 = T2
proofend;

scheme :: TREES_2:sch 6
DTreeEx{ F1() ->  Tree, P1[ set , set ] } :
 ex T being DecoratedTree st
( dom T = F1() &amp; ( for p being FinSequence of NAT st p in F1() holds
P1[p,T . p] ) )
provided
A1: for p being FinSequence of NAT st p in F1() holds
ex x being set st P1[p,x]
proofend;

scheme :: TREES_2:sch 7
DTreeLambda{ F1() ->  Tree, F2( set ) ->  set } :
 ex T being DecoratedTree st
( dom T = F1() &amp; ( for p being FinSequence of NAT st p in F1() holds
T . p = F2(p) ) )
proofend;

definition
let T be DecoratedTree;
func Leaves T ->  set  equals :: TREES_2:def 9
T .: (Leaves (dom T));
correctness
coherence
T .: (Leaves (dom T)) is set ;
;
let p be FinSequence of NAT ;
funcT | p ->  DecoratedTree means :Def10: :: TREES_2:def 10
( dom it = (dom T) | p &amp; ( for q being FinSequence of NAT st q in (dom T) | p holds
it . q = T . (p ^ q) ) );
existence
 ex b1 being DecoratedTree st
( dom b1 = (dom T) | p &amp; ( for q being FinSequence of NAT st q in (dom T) | p holds
b1 . q = T . (p ^ q) ) )
proofend;
uniqueness
 for b1, b2 being DecoratedTree st dom b1 = (dom T) | p &amp; ( for q being FinSequence of NAT st q in (dom T) | p holds
b1 . q = T . (p ^ q) ) &amp; dom b2 = (dom T) | p &amp; ( for q being FinSequence of NAT st q in (dom T) | p holds
b2 . q = T . (p ^ q) ) holds
b1 = b2
proofend;
end;

:: deftheorem  defines Leaves TREES_2:def_9_:_
 for T being DecoratedTree holds Leaves T = T .: (Leaves (dom T));

:: deftheorem Def10 defines | TREES_2:def_10_:_
 for T being DecoratedTree
for p being FinSequence of NAT
for b3 being DecoratedTree holds
( b3 = T | p iff ( dom b3 = (dom T) | p &amp; ( for q being FinSequence of NAT st q in (dom T) | p holds
b3 . q = T . (p ^ q) ) ) );

theorem Th32: :: TREES_2:32
for p being FinSequence of NAT
for T being DecoratedTree st p in dom T holds
rng (T | p) c= rng T
proofend;

definition
let D be non empty set ;
let T be DecoratedTree of D;
:: original:Leaves
redefine func Leaves T ->  Subset of D;
coherence
 Leaves T is Subset of D
proofend;
end;

registration
let D be non empty set ;
let T be DecoratedTree of D;
let p be Element of dom T;
clusterT | p -> D -valued ;
coherence
 T | p is D -valued
proofend;
end;

definition
let T be DecoratedTree;
let p be FinSequence of NAT ;
let T1 be DecoratedTree;
assume A1: p in dom T ;
funcT with-replacement (p,T1) ->  DecoratedTree means :: TREES_2:def 11
( dom it = (dom T) with-replacement (p,(dom T1)) &amp; ( for q being FinSequence of NAT holds
( not q in (dom T) with-replacement (p,(dom T1)) or ( not p is_a_prefix_of q &amp; it . q = T . q ) or ex r being FinSequence of NAT st
( r in dom T1 &amp; q = p ^ r &amp; it . q = T1 . r ) ) ) );
existence
 ex b1 being DecoratedTree st
( dom b1 = (dom T) with-replacement (p,(dom T1)) &amp; ( for q being FinSequence of NAT holds
( not q in (dom T) with-replacement (p,(dom T1)) or ( not p is_a_prefix_of q &amp; b1 . q = T . q ) or ex r being FinSequence of NAT st
( r in dom T1 &amp; q = p ^ r &amp; b1 . q = T1 . r ) ) ) )
proofend;
uniqueness
 for b1, b2 being DecoratedTree st dom b1 = (dom T) with-replacement (p,(dom T1)) &amp; ( for q being FinSequence of NAT holds
( not q in (dom T) with-replacement (p,(dom T1)) or ( not p is_a_prefix_of q &amp; b1 . q = T . q ) or ex r being FinSequence of NAT st
( r in dom T1 &amp; q = p ^ r &amp; b1 . q = T1 . r ) ) ) &amp; dom b2 = (dom T) with-replacement (p,(dom T1)) &amp; ( for q being FinSequence of NAT holds
( not q in (dom T) with-replacement (p,(dom T1)) or ( not p is_a_prefix_of q &amp; b2 . q = T . q ) or ex r being FinSequence of NAT st
( r in dom T1 &amp; q = p ^ r &amp; b2 . q = T1 . r ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem  defines with-replacement TREES_2:def_11_:_
 for T being DecoratedTree
for p being FinSequence of NAT
for T1 being DecoratedTree st p in dom T holds
for b4 being DecoratedTree holds
( b4 = T with-replacement (p,T1) iff ( dom b4 = (dom T) with-replacement (p,(dom T1)) &amp; ( for q being FinSequence of NAT holds
( not q in (dom T) with-replacement (p,(dom T1)) or ( not p is_a_prefix_of q &amp; b4 . q = T . q ) or ex r being FinSequence of NAT st
( r in dom T1 &amp; q = p ^ r &amp; b4 . q = T1 . r ) ) ) ) );

registration
let W be Tree;
let x be set ;
clusterW --> x ->  DecoratedTree-like ;
coherence
 W --> x is DecoratedTree-like
proofend;
end;

theorem Th33: :: TREES_2:33
for D being non empty set st ( for x being set st x in D holds
x is Tree ) holds
union D is Tree
proofend;

theorem Th34: :: TREES_2:34
for X being set st ( for x being set st x in X holds
x is Function ) &amp; X is c=-linear holds
( union X is Relation-like &amp; union X is Function-like )
proofend;

theorem Th35: :: TREES_2:35
for D being non empty set st ( for x being set st x in D holds
x is DecoratedTree ) &amp; D is c=-linear holds
union D is DecoratedTree
proofend;

theorem Th36: :: TREES_2:36
for D9, D being non empty set st ( for x being set st x in D9 holds
x is DecoratedTree of D ) &amp; D9 is c=-linear holds
union D9 is DecoratedTree of D
proofend;

scheme :: TREES_2:sch 8
DTreeStructEx{ F1() ->  non empty set , F2() ->  Element of F1(), F3( set ) ->  set , F4() ->  Function of [:F1(),NAT:],F1() } :
 ex T being DecoratedTree of F1() st
( T . {} = F2() &amp; ( for t being Element of dom T holds
( succ t =  {  (t ^ <*k*>) where k is Element of NAT : k in F3((T . t))  }  &amp; ( for n being Element of NAT st n in F3((T . t)) holds
T . (t ^ <*n*>) = F4() . ((T . t),n) ) ) ) )
provided
A1: for d being Element of F1()
for k1, k2 being Element of NAT st k1 <= k2 &amp; k2 in F3(d) holds
k1 in F3(d)
proofend;

scheme :: TREES_2:sch 9
DTreeStructFinEx{ F1() ->  non empty set , F2() ->  Element of F1(), F3( set ) ->  Element of NAT , F4() ->  Function of [:F1(),NAT:],F1() } :
 ex T being DecoratedTree of F1() st
( T . {} = F2() &amp; ( for t being Element of dom T holds
( succ t =  {  (t ^ <*k*>) where k is Element of NAT : k < F3((T . t))  }  &amp; ( for n being Element of NAT st n < F3((T . t)) holds
T . (t ^ <*n*>) = F4() . ((T . t),n) ) ) ) )
proofend;

begin

:: from PRELAMB
registration
let Tr be finite Tree;
let v be Element of Tr;
cluster succ v ->  finite ;
coherence
 succ v is finite ;
end;

definition
let Tr be finite Tree;
let v be Element of Tr;
func branchdeg v ->  set  equals :: TREES_2:def 12
 card (succ v);
correctness
coherence
card (succ v) is set ;
;
end;

:: deftheorem  defines branchdeg TREES_2:def_12_:_
 for Tr being finite Tree
for v being Element of Tr holds branchdeg v = card (succ v);

registration
cluster Relation-like Function-like finite DecoratedTree-like for set ;
existence
 ex b1 being DecoratedTree st b1 is finite
proofend;
end;

registration
let D be non empty set ;
cluster Relation-like D -valued Function-like finite DecoratedTree-like for set ;
existence
 ex b1 being DecoratedTree of D st b1 is finite
proofend;
end;

registration
let a, b be non empty set ;
cluster Relation-like a -defined b -valued non empty for Element of bool [:a,b:];
existence
 not for b1 being Relation of a,b holds b1 is empty
proofend;
end;

theorem :: TREES_2:37
for Z1, Z2 being Tree
for p being FinSequence of NAT st p in Z1 holds
for v being Element of Z1 with-replacement (p,Z2)
for w being Element of Z2 st v = p ^ w holds
succ v, succ w are_equipotent
proofend;

scheme :: TREES_2:sch 10
DTreeStructEx{ F1() ->  non empty set , F2() ->  Element of F1(), P1[ set , set ], F3() ->  Function of [:F1(),NAT:],F1() } :
 ex T being DecoratedTree of F1() st
( T . {} = F2() &amp; ( for t being Element of dom T holds
( succ t =  {  (t ^ <*k*>) where k is Element of NAT : P1[k,T . t]  }  &amp; ( for n being Element of NAT st P1[n,T . t] holds
T . (t ^ <*n*>) = F3() . ((T . t),n) ) ) ) )
provided
A1: for d being Element of F1()
for k1, k2 being Element of NAT st k1 <= k2 &amp; P1[k2,d] holds
P1[k1,d]
proofend;

:: from AMISTD_3, 2010.01.10, A.T.
theorem :: TREES_2:38
for T1, T2 being Tree st ( for n being Element of NAT holds T1 -level n = T2 -level n ) holds
T1 = T2
proofend;

theorem :: TREES_2:39
for n being Element of NAT holds TrivialInfiniteTree -level n = {(n |-> 0)}
proofend;

theorem :: TREES_2:40
for X, Y being set
for B being c=-linear Subset of (PFuncs (X,Y)) holds union B in PFuncs (X,Y)
proofend;