---

Step * 1 2 1 2 1 2 1 of Lemma Dickson's lemma


1. p : ℕ
2. ∀p1:ℕp. ∀A:ℕp1 ⟶ ℕ ⟶ ℕ.  ∃j:ℕ. ∃i:ℕj. ∀k:ℕp1. (A[k;i] ≤ A[k;j])
3. A : ℕp ⟶ ℕ ⟶ ℕ
4. ¬(p = 0 ∈ ℤ)
5. n : ℤ
6. [%5] : 0 < n
7. ∀m1:ℕ. ∃i:ℕ. (m1 < i ∧ ((∃b:ℕ. ∃a:ℕb. ∀k:ℕp. (A[k;a] ≤ A[k;b])) ∨ ((n - 1) ≤ A[0;i])))
8. m : ℕ
9. G : m1:ℕ ⟶ ℕ
10. ∀m1:ℕ. (m1 < G m1 ∧ ((∃b:ℕ. ∃a:ℕb. ∀k:ℕp. (A[k;a] ≤ A[k;b])) ∨ ((n - 1) ≤ A[0;G m1])))
11. g : ℕ ⟶ ℕ
12. m < g 0 ∧ (∀b:ℕ. ∀a:ℕb.  g a < g b) ∧ (∀l:ℕ. ((∃b:ℕ. ∃a:ℕb. ∀k:ℕp. (A[k;a] ≤ A[k;b])) ∨ ((n - 1) ≤ A[0;g l])))
⊢ ∃i:ℕ. (m < i ∧ ((∃b:ℕ. ∃a:ℕb. ∀k:ℕp. (A[k;a] ≤ A[k;b])) ∨ (n ≤ A[0;i])))
BY
{ ((InstHyp [⌜p - 1⌝;⌜λ2k i.A[k + 1;g i]⌝] 2⋅ THENA Auto) THEN ExRepD) }

1
1. p : ℕ
2. ∀p1:ℕp. ∀A:ℕp1 ⟶ ℕ ⟶ ℕ.  ∃j:ℕ. ∃i:ℕj. ∀k:ℕp1. (A[k;i] ≤ A[k;j])
3. A : ℕp ⟶ ℕ ⟶ ℕ
4. ¬(p = 0 ∈ ℤ)
5. n : ℤ
6. [%5] : 0 < n
7. ∀m1:ℕ. ∃i:ℕ. (m1 < i ∧ ((∃b:ℕ. ∃a:ℕb. ∀k:ℕp. (A[k;a] ≤ A[k;b])) ∨ ((n - 1) ≤ A[0;i])))
8. m : ℕ
9. G : m1:ℕ ⟶ ℕ
10. ∀m1:ℕ. (m1 < G m1 ∧ ((∃b:ℕ. ∃a:ℕb. ∀k:ℕp. (A[k;a] ≤ A[k;b])) ∨ ((n - 1) ≤ A[0;G m1])))
11. g : ℕ ⟶ ℕ
12. m < g 0
13. ∀b:ℕ. ∀a:ℕb.  g a < g b
14. ∀l:ℕ. ((∃b:ℕ. ∃a:ℕb. ∀k:ℕp. (A[k;a] ≤ A[k;b])) ∨ ((n - 1) ≤ A[0;g l]))
15. j : ℕ
16. i : ℕj
17. ∀k:ℕp - 1. (A[k + 1;g i] ≤ A[k + 1;g j])
⊢ ∃i:ℕ. (m < i ∧ ((∃b:ℕ. ∃a:ℕb. ∀k:ℕp. (A[k;a] ≤ A[k;b])) ∨ (n ≤ A[0;i])))

---

Latex:

---

Latex:

1.  p  :  \mBbbN{}
2.  \mforall{}p1:\mBbbN{}p.  \mforall{}A:\mBbbN{}p1  {}\mrightarrow{}  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}.    \mexists{}j:\mBbbN{}.  \mexists{}i:\mBbbN{}j.  \mforall{}k:\mBbbN{}p1.  (A[k;i]  \mleq{}  A[k;j])
3.  A  :  \mBbbN{}p  {}\mrightarrow{}  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}
4.  \mneg{}(p  =  0)
5.  n  :  \mBbbZ{}
6.  [\%5]  :  0  <  n
7.  \mforall{}m1:\mBbbN{}.  \mexists{}i:\mBbbN{}.  (m1  <  i  \mwedge{}  ((\mexists{}b:\mBbbN{}.  \mexists{}a:\mBbbN{}b.  \mforall{}k:\mBbbN{}p.  (A[k;a]  \mleq{}  A[k;b]))  \mvee{}  ((n  -  1)  \mleq{}  A[0;i])))
8.  m  :  \mBbbN{}
9.  G  :  m1:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}
10.  \mforall{}m1:\mBbbN{}.  (m1  <  G  m1  \mwedge{}  ((\mexists{}b:\mBbbN{}.  \mexists{}a:\mBbbN{}b.  \mforall{}k:\mBbbN{}p.  (A[k;a]  \mleq{}  A[k;b]))  \mvee{}  ((n  -  1)  \mleq{}  A[0;G  m1])))
11.  g  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}
12.  m  <  g  0
\mwedge{}  (\mforall{}b:\mBbbN{}.  \mforall{}a:\mBbbN{}b.    g  a  <  g  b)
\mwedge{}  (\mforall{}l:\mBbbN{}.  ((\mexists{}b:\mBbbN{}.  \mexists{}a:\mBbbN{}b.  \mforall{}k:\mBbbN{}p.  (A[k;a]  \mleq{}  A[k;b]))  \mvee{}  ((n  -  1)  \mleq{}  A[0;g  l])))
\mvdash{}  \mexists{}i:\mBbbN{}.  (m  <  i  \mwedge{}  ((\mexists{}b:\mBbbN{}.  \mexists{}a:\mBbbN{}b.  \mforall{}k:\mBbbN{}p.  (A[k;a]  \mleq{}  A[k;b]))  \mvee{}  (n  \mleq{}  A[0;i])))


By

---

Latex:
((InstHyp  [\mkleeneopen{}p  -  1\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}k  i.A[k  +  1;g  i]\mkleeneclose{}]  2\mcdot{}  THENA  Auto)  THEN  ExRepD)

---

Home Index