:: 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
proof end;

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
proof end;

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*> & len v2 = k )
proof end;

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

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] & t ^ <*n*> in F1() holds
P1[t ^ <*n*>]
proof end;

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
proof end;

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))
proof end;

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

theorem :: TREES_2:8
for W, W1, W2 being Tree
for p, q being FinSequence of NAT st p in W & q in W & 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)
proof end;

definition
let IT be Tree;
attr IT 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
proof end;
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 & 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 & q in b1 holds
p,q are_c=-comparable
proof end;
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 }
proof end;
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
proof end;
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 & 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
proof end;

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

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}
proof end;

definition
let W be Tree;
let n be Nat;
func W -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
proof end;
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
proof end;

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

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

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
proof end;

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()
proof end;

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() }
proof end;

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 & card B <= n )
proof end;

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
proof end;

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
proof end;

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

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

definition
let W be Tree;
let IT be Chain of W;
attr IT is Branch-like means :Def7: :: TREES_2:def 7
( ( for p being FinSequence of NAT st p in IT holds
ProperPrefixes p c= IT ) & ( for p being FinSequence of NAT holds
( not p in W or ex q being FinSequence of NAT st
( q in IT & 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 ) & ( for p being FinSequence of NAT holds
( not p in W or ex q being FinSequence of NAT st
( q in IT & 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
proof end;
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
proof end;
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 & v2 in C & not v1 in ProperPrefixes v2 holds
v2 is_a_prefix_of v1
proof end;

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 & v2 in C & v is_a_prefix_of v2 & not v1 in ProperPrefixes v holds
v is_a_prefix_of v1
proof end;

registration
let W be Tree;
cluster finite for Chain of W;
existence
ex b1 being Chain of W st b1 is finite
proof end;
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 & len p >= n )
proof end;

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 & w is_a_prefix_of p ) } is Chain of W
proof end;

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 & q in B holds
p in B
proof end;

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

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 & q in C & len p <= len q holds
p is_a_prefix_of q
proof end;

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
proof end;

scheme :: TREES_2:sch 4
FuncExOfMinNat{ P1[ set , Nat], F1() -> set } :
ex f being Function st
( dom f = F1() & ( for x being set st x in F1() holds
ex n being Element of NAT st
( f . x = n & P1[x,n] & ( 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]
proof end;

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
proof end;

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

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 ) & ( for t being Element of T holds succ t is finite ) holds
ex B being Chain of T st not B is finite
proof end;

:: 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
proof end;

definition
let IT be Relation;
attr IT 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
proof end;
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 & 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 & b1 is D -valued )
proof end;
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 func T . t -> Element of D;
coherence
T . t is Element of D
proof end;
end;

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

scheme :: TREES_2:sch 6
DTreeEx{ F1() -> Tree, P1[ set , set ] } :
ex T being DecoratedTree st
( dom T = F1() & ( 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]
proof end;

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

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 ;
func T | p -> DecoratedTree means :Def10: :: TREES_2:def 10
( dom it = (dom T) | p & ( 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 & ( for q being FinSequence of NAT st q in (dom T) | p holds
b1 . q = T . (p ^ q) ) )
proof end;
uniqueness
for b1, b2 being DecoratedTree st dom b1 = (dom T) | p & ( for q being FinSequence of NAT st q in (dom T) | p holds
b1 . q = T . (p ^ q) ) & dom b2 = (dom T) | p & ( for q being FinSequence of NAT st q in (dom T) | p holds
b2 . q = T . (p ^ q) ) holds
b1 = b2
proof end;
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 & ( 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
proof end;

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
proof end;
end;

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

definition
let T be DecoratedTree;
let p be FinSequence of NAT ;
let T1 be DecoratedTree;
assume A1: p in dom T ;
func T with-replacement (p,T1) -> DecoratedTree means :: TREES_2:def 11
( dom it = (dom T) with-replacement (p,(dom T1)) & ( 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 & it . q = T . q ) or ex r being FinSequence of NAT st
( r in dom T1 & q = p ^ r & it . q = T1 . r ) ) ) );
existence
ex b1 being DecoratedTree st
( dom b1 = (dom T) with-replacement (p,(dom T1)) & ( 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 & b1 . q = T . q ) or ex r being FinSequence of NAT st
( r in dom T1 & q = p ^ r & b1 . q = T1 . r ) ) ) )
proof end;
uniqueness
for b1, b2 being DecoratedTree st dom b1 = (dom T) with-replacement (p,(dom T1)) & ( 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 & b1 . q = T . q ) or ex r being FinSequence of NAT st
( r in dom T1 & q = p ^ r & b1 . q = T1 . r ) ) ) & dom b2 = (dom T) with-replacement (p,(dom T1)) & ( 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 & b2 . q = T . q ) or ex r being FinSequence of NAT st
( r in dom T1 & q = p ^ r & b2 . q = T1 . r ) ) ) holds
b1 = b2
proof end;
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)) & ( 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 & b4 . q = T . q ) or ex r being FinSequence of NAT st
( r in dom T1 & q = p ^ r & b4 . q = T1 . r ) ) ) ) );

registration
let W be Tree;
let x be set ;
cluster W --> x -> DecoratedTree-like ;
coherence
W --> x is DecoratedTree-like
proof end;
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
proof end;

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

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

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 ) & D9 is c=-linear holds
union D9 is DecoratedTree of D
proof end;

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() & ( for t being Element of dom T holds
( succ t = { (t ^ <*k*>) where k is Element of NAT : k in F3((T . t)) } & ( 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 & k2 in F3(d) holds
k1 in F3(d)
proof end;

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() & ( for t being Element of dom T holds
( succ t = { (t ^ <*k*>) where k is Element of NAT : k < F3((T . t)) } & ( for n being Element of NAT st n < F3((T . t)) holds
T . (t ^ <*n*>) = F4() . ((T . t),n) ) ) ) )
proof end;

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
proof end;
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
proof end;
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
proof end;
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
proof end;

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() & ( for t being Element of dom T holds
( succ t = { (t ^ <*k*>) where k is Element of NAT : P1[k,T . t] } & ( 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 & P1[k2,d] holds
P1[k1,d]
proof end;

:: 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
proof end;

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

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)
proof end;