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

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 by Th1;

theorem Th3: :: TREES_2:3

for k being 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{ F₁() -> Tree, P₁[ set ] } :

for t being Element of F₁() holds P₁[t]

provided

A1: P₁[ {} ] and
A2: for t being Element of F₁()
for n being Nat st P₁[t] & t ^ <*n*> in F₁() holds
P₁[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 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 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 b₁ being Tree st b₁ 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 b₁ being Subset of W st
for p, q being FinSequence of NAT st p in b₁ & q in b₁ 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 b₁ being Subset of W ex n being Nat st b₁ = { 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 Nat : w ^ <*n*> in W } ;

coherence
{ (w ^ <*n*>) where n is 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 b₂ being Subset of W holds
( b₂ is Chain of W iff for p, q being FinSequence of NAT st p in b₂ & q in b₂ holds
p,q are_c=-comparable );

:: deftheorem Def4 defines Level TREES_2:def 4 :
for W being Tree
for b₂ being Subset of W holds
( b₂ is Level of W iff ex n being Nat st b₂ = { 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 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 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 Nat : verum }

proof end;

theorem :: TREES_2:15

for W being finite Tree holds W = union { (W -level n) where n is Nat : n <= height W }

proof end;

theorem :: TREES_2:16

for W being Tree
for L being Level of W ex n being Nat st L = W -level n

proof end;

scheme :: TREES_2:sch 2
FraenkelCard{ F₁() -> non empty set , F₂() -> set , F₃( object ) -> set } :

card { F₃(w) where w is Element of F₁() : w in F₂() } c= card F₂()

proof end;

scheme :: TREES_2:sch 3
FraenkelFinCard{ F₁() -> non empty set , F₂() -> finite set , F₃() -> finite set , F₄( set ) -> set } :

card F₃() <= card F₂()

provided

A1: F₃() = { F₄(w) where w is Element of F₁() : w in F₂() }

proof end;

theorem Th17: :: TREES_2:17

for W being Tree st W is finite-order holds
ex n being 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 b₁ being Chain of W holds b₁ 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 b₁ being Chain of W st b₁ 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 b₁ being Chain of W st b₁ is Branch-like holds
not b₁ 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 v, v1, v2 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 b₁ being Chain of W st b₁ is finite

proof end;

end;

theorem Th23: :: TREES_2:23

for W being Tree
for n being 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{ P₁[ object , Nat], F₁() -> set } :

ex f being Function st
( dom f = F₁() & ( for x being object st x in F₁() holds
ex n being Nat st
( f . x = n & P₁[x,n] & ( for m being Nat st P₁[x,m] holds
n <= m ) ) ) )

provided

A1: for x being object st x in F₁() holds
ex n being Nat st P₁[x,n]

proof end;

Lm1: for X being set st X is finite holds
ex n being Nat st
for k being Nat st k in X holds
k <= n

proof end;

scheme :: TREES_2:sch 5
InfiniteChain{ F₁() -> set , F₂() -> object , P₁[ object ], P₂[ object , object ] } :

ex f being Function st
( dom f = NAT & rng f c= F₁() & f . 0 = F₂() & ( for k being Nat holds
( P₂[f . k,f . (k + 1)] & P₁[f . k] ) ) )

provided

A1: ( F₂() in F₁() & P₁[F₂()] ) and
A2: for x being object st x in F₁() & P₁[x] holds
ex y being object st
( y in F₁() & P₂[x,y] & P₁[y] )

proof end;

theorem Th29: :: TREES_2:29

for T being Tree st ( for n being 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;

:: Koenig Lemma

theorem :: TREES_2:30

for T being finite-order Tree st ( for n being 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 b₁ being Function st b₁ 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 b₁ being Function st
( b₁ is DecoratedTree-like & b₁ 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{ F₁() -> Tree, P₁[ object , object ] } :

ex T being DecoratedTree st
( dom T = F₁() & ( for p being FinSequence of NAT st p in F₁() holds
P₁[p,T . p] ) )

provided

A1: for p being FinSequence of NAT st p in F₁() holds
ex x being set st P₁[p,x]

proof end;

scheme :: TREES_2:sch 7
DTreeLambda{ F₁() -> Tree, F₂( object ) -> set } :

ex T being DecoratedTree st
( dom T = F₁() & ( for p being FinSequence of NAT st p in F₁() holds
T . p = F₂(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 b₁ being DecoratedTree st
( dom b₁ = (dom T) | p & ( for q being FinSequence of NAT st q in (dom T) | p holds
b₁ . q = T . (p ^ q) ) )

proof end;

uniqueness
for b₁, b₂ being DecoratedTree st dom b₁ = (dom T) | p & ( for q being FinSequence of NAT st q in (dom T) | p holds
b₁ . q = T . (p ^ q) ) & dom b₂ = (dom T) | p & ( for q being FinSequence of NAT st q in (dom T) | p holds
b₂ . q = T . (p ^ q) ) holds
b₁ = b₂

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 b₃ being DecoratedTree holds
( b₃ = T | p iff ( dom b₃ = (dom T) | p & ( for q being FinSequence of NAT st q in (dom T) | p holds
b₃ . 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 b₁ being DecoratedTree st
( dom b₁ = (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 & b₁ . q = T . q ) or ex r being FinSequence of NAT st
( r in dom T1 & q = p ^ r & b₁ . q = T1 . r ) ) ) )

proof end;

uniqueness
for b₁, b₂ being DecoratedTree st dom b₁ = (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 & b₁ . q = T . q ) or ex r being FinSequence of NAT st
( r in dom T1 & q = p ^ r & b₁ . q = T1 . r ) ) ) & dom b₂ = (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 & b₂ . q = T . q ) or ex r being FinSequence of NAT st
( r in dom T1 & q = p ^ r & b₂ . q = T1 . r ) ) ) holds
b₁ = b₂

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 b₄ being DecoratedTree holds
( b₄ = T with-replacement (p,T1) iff ( dom b₄ = (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 & b₄ . q = T . q ) or ex r being FinSequence of NAT st
( r in dom T1 & q = p ^ r & b₄ . q = T1 . r ) ) ) ) );

registration

let W be Tree;
let x be set ;

cluster W --> x -> DecoratedTree-like ;

coherence
W --> x is DecoratedTree-like ;

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 D, D9 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{ F₁() -> non empty set , F₂() -> Element of F₁(), F₃( set ) -> set , F₄() -> Function of [:F₁(),NAT:],F₁() } :

ex T being DecoratedTree of F₁() st
( T . {} = F₂() & ( for t being Element of dom T holds
( succ t = { (t ^ <*k*>) where k is Nat : k in F₃((T . t)) } & ( for n being Nat st n in F₃((T . t)) holds
T . (t ^ <*n*>) = F₄() . ((T . t),n) ) ) ) )

provided

A1: for d being Element of F₁()
for k1, k2 being Nat st k1 <= k2 & k2 in F₃(d) holds
k1 in F₃(d)

proof end;

scheme :: TREES_2:sch 9
DTreeStructFinEx{ F₁() -> non empty set , F₂() -> Element of F₁(), F₃( set ) -> Nat, F₄() -> Function of [:F₁(),NAT:],F₁() } :

ex T being DecoratedTree of F₁() st
( T . {} = F₂() & ( for t being Element of dom T holds
( succ t = { (t ^ <*k*>) where k is Nat : k < F₃((T . t)) } & ( for n being Nat st n < F₃((T . t)) holds
T . (t ^ <*n*>) = F₄() . ((T . t),n) ) ) ) )

proof end;

:: 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 b₁ being DecoratedTree st b₁ 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 b₁ being DecoratedTree of D st b₁ is finite

proof end;

end;

registration

let a, b be non empty set ;

cluster Relation-like non empty for Element of bool [:a,b:];

existence
not for b₁ being Relation of a,b holds b₁ 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{ F₁() -> non empty set , F₂() -> Element of F₁(), P₁[ set , set ], F₃() -> Function of [:F₁(),NAT:],F₁() } :

ex T being DecoratedTree of F₁() st
( T . {} = F₂() & ( for t being Element of dom T holds
( succ t = { (t ^ <*k*>) where k is Nat : P₁[k,T . t] } & ( for n being Nat st P₁[n,T . t] holds
T . (t ^ <*n*>) = F₃() . ((T . t),n) ) ) ) )

provided

A1: for d being Element of F₁()
for k1, k2 being Nat st k1 <= k2 & P₁[k2,d] holds
P₁[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 Nat holds T1 -level n = T2 -level n ) holds
T1 = T2

proof end;

theorem :: TREES_2:39

for n being 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;