Volume 3, 1991

University of Bialystok

Copyright (c) 1991 Association of Mizar Users

### The abstract of the Mizar article:

### 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