:: K\"onig's Lemma :: by Grzegorz Bancerek :: :: Received January 10, 1991 :: Copyright (c) 1991-2021 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; 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 :: 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; theorem :: TREES_2:3 len v1 = k+1 implies ex v2,x st v1 = v2^<*x*> & len v2 = k; theorem :: TREES_2:4 ProperPrefixes (v^<*x*>) = ProperPrefixes v \/ {v}; scheme :: TREES_2:sch 1 TreeStructInd { 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:5 (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:6 p in W implies W = W with-replacement (p,W|p); theorem :: TREES_2:7 p in W & q in W & not p is_a_prefix_of q implies q in W with-replacement (p,W1); theorem :: TREES_2:8 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; registration cluster finite-order for 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 being Nat 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:9 for L being Level of W holds L is AntiChain_of_Prefixes of W; theorem :: TREES_2:10 succ w is AntiChain_of_Prefixes of W; theorem :: TREES_2:11 for A being AntiChain_of_Prefixes of W, C being Chain of W ex w st A /\ C c= {w}; definition let W; let n be Nat; func W-level n -> Level of W equals :: TREES_2:def 6 { w: len w = n }; end; theorem :: TREES_2:12 w^<*n*> in succ w iff w^<*n*> in W; theorem :: TREES_2:13 w = {} implies W-level 1 = succ w; theorem :: TREES_2:14 W = union the set of all W-level n; theorem :: TREES_2:15 for W being finite Tree holds W = union { W-level n: n <= height W }; theorem :: TREES_2:16 for L being Level of W ex n st L = W-level n; scheme :: TREES_2:sch 2 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(); scheme :: TREES_2:sch 3 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:17 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:18 W is finite-order implies succ w is finite; registration let W be finite-order Tree; let w be Element of W; cluster succ w -> finite; end; theorem :: TREES_2:19 {} is Chain of W; theorem :: TREES_2:20 {{}} is Chain of W; registration let W; cluster non empty for 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; registration let W; cluster Branch-like for Chain of W; 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; end; reserve C for Chain of W, B for Branch of W; theorem :: TREES_2:21 v1 in C & v2 in C implies v1 in ProperPrefixes v2 or v2 is_a_prefix_of v1; theorem :: TREES_2:22 v1 in C & v2 in C & v is_a_prefix_of v2 implies v1 in ProperPrefixes v or v is_a_prefix_of v1; registration let W; cluster finite for Chain of W; end; theorem :: TREES_2:23 for C being finite Chain of W st card C > n ex p st p in C & len p >= n; theorem :: TREES_2:24 for C holds { w: ex p st p in C & w is_a_prefix_of p } is Chain of W; theorem :: TREES_2:25 p is_a_prefix_of q & q in B implies p in B; theorem :: TREES_2:26 {} in B; theorem :: TREES_2:27 p in C & q in C & len p <= len q implies p is_a_prefix_of q; theorem :: TREES_2:28 ex B st C c= B; scheme :: TREES_2:sch 4 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 for x being object st x in X() ex n st P[x,n]; scheme :: TREES_2:sch 5 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 a() in X() & Q[a()] and for x being object st x in X() & Q[x] ex y being object st y in X() & P[x,y] & Q[y]; theorem :: TREES_2:29 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; ::$N Koenig Lemma theorem :: TREES_2:30 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; registration cluster DecoratedTree-like for Function; 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; end; registration let D; cluster DecoratedTree-like D-valued for Function; 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; end; theorem :: TREES_2:31 dom T1 = dom T2 & (for p st p in dom T1 holds T1.p = T2.p) implies T1 = T2; scheme :: TREES_2:sch 6 DTreeEx { T() -> Tree, P[object,object] }: 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 :: TREES_2:sch 7 DTreeLambda { T() -> Tree, f(object) -> 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 9 T.:Leaves dom T; let p; func T|p -> DecoratedTree means :: TREES_2:def 10 dom it = (dom T)|p & for q st q in (dom T)|p holds it.q = T.(p^q); end; theorem :: TREES_2:32 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; end; registration let D; let T be DecoratedTree of D; let p be Element of dom T; cluster T|p -> D-valued; end; definition let T,p,T1; assume 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 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; registration let W,x; cluster W --> x -> DecoratedTree-like; end; theorem :: TREES_2:33 (for x st x in D holds x is Tree) implies union D is Tree; theorem :: TREES_2:34 (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:35 (for x st x in D holds x is DecoratedTree) & D is c=-linear implies union D is DecoratedTree; theorem :: TREES_2:36 (for x st x in D9 holds x is DecoratedTree of D) & D9 is c=-linear implies union D9 is DecoratedTree of D; scheme :: TREES_2:sch 8 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 for d being Element of D(), k1,k2 st k1 <= k2 & k2 in F(d) holds k1 in F(d); scheme :: TREES_2:sch 9 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); begin :: Addenda :: from PRELAMB registration let Tr be finite Tree, v be Element of Tr; cluster succ v -> finite; end; definition let Tr be finite Tree, v be Element of Tr; func branchdeg v -> set equals :: TREES_2:def 12 card succ v; end; registration cluster finite for DecoratedTree; end; registration let D be non empty set; cluster finite for DecoratedTree of D; end; registration let a,b be non empty set; cluster non empty for Relation of a,b; end; :: from MODAL_1, 2007.03.14, A.T. reserve x1,x2 for set, w for FinSequence of NAT; theorem :: TREES_2:37 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; scheme :: TREES_2:sch 10 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 for d being Element of D(), k1,k2 st k1 <= k2 & Q[k2,d] holds Q[k1,d]; :: 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; theorem :: TREES_2:39 for n being Nat holds TrivialInfiniteTree-level n = { n |-> 0 }; 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);