---

Step * 1 2 2 2 1 2 1 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. G : n:ℕ ⟶ ℕ
6. ∀n:ℕ. (n < G n ∧ ((∃b:ℕ. ∃a:ℕb. ∀k:ℕp. (A[k;a] ≤ A[k;b])) ∨ (A[0;n] ≤ A[0;G n])))
7. g : ℕ ⟶ ℕ
8. ∀b:ℕ. ∀a:ℕb.  g a < g b
9. ∀l:ℕ. ((∃b:ℕ. ∃a:ℕb. ∀k:ℕp. (A[k;a] ≤ A[k;b])) ∨ (A[0;g l] ≤ A[0;g (l + 1)]))
10. j : ℕ
11. i : ℕj
12. ∀k:ℕp - 1. (A[k + 1;g i] ≤ A[k + 1;g j])
⊢ ∃j:ℕ. ∃i:ℕj. ∀k:ℕp. (A[k;i] ≤ A[k;j])
BY
{ TACTIC:TACTIC:Assert ⌜∀n:ℕ+. ∀l:ℕ.  ((∃b:ℕ. ∃a:ℕb. ∀k:ℕp. (A[k;a] ≤ A[k;b])) ∨ (A[0;g l] ≤ A[0;g (l + n)]))⌝⋅ }

1
.....assertion..... 
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. G : n:ℕ ⟶ ℕ
6. ∀n:ℕ. (n < G n ∧ ((∃b:ℕ. ∃a:ℕb. ∀k:ℕp. (A[k;a] ≤ A[k;b])) ∨ (A[0;n] ≤ A[0;G n])))
7. g : ℕ ⟶ ℕ
8. ∀b:ℕ. ∀a:ℕb.  g a < g b
9. ∀l:ℕ. ((∃b:ℕ. ∃a:ℕb. ∀k:ℕp. (A[k;a] ≤ A[k;b])) ∨ (A[0;g l] ≤ A[0;g (l + 1)]))
10. j : ℕ
11. i : ℕj
12. ∀k:ℕp - 1. (A[k + 1;g i] ≤ A[k + 1;g j])
⊢ ∀n:ℕ+. ∀l:ℕ.  ((∃b:ℕ. ∃a:ℕb. ∀k:ℕp. (A[k;a] ≤ A[k;b])) ∨ (A[0;g l] ≤ A[0;g (l + n)]))

2
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. G : n:ℕ ⟶ ℕ
6. ∀n:ℕ. (n < G n ∧ ((∃b:ℕ. ∃a:ℕb. ∀k:ℕp. (A[k;a] ≤ A[k;b])) ∨ (A[0;n] ≤ A[0;G n])))
7. g : ℕ ⟶ ℕ
8. ∀b:ℕ. ∀a:ℕb.  g a < g b
9. ∀l:ℕ. ((∃b:ℕ. ∃a:ℕb. ∀k:ℕp. (A[k;a] ≤ A[k;b])) ∨ (A[0;g l] ≤ A[0;g (l + 1)]))
10. j : ℕ
11. i : ℕj
12. ∀k:ℕp - 1. (A[k + 1;g i] ≤ A[k + 1;g j])
13. ∀n:ℕ+. ∀l:ℕ.  ((∃b:ℕ. ∃a:ℕb. ∀k:ℕp. (A[k;a] ≤ A[k;b])) ∨ (A[0;g l] ≤ A[0;g (l + n)]))
⊢ ∃j:ℕ. ∃i:ℕj. ∀k:ℕp. (A[k;i] ≤ A[k;j])

---

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.  G  :  n:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}
6.  \mforall{}n:\mBbbN{}.  (n  <  G  n  \mwedge{}  ((\mexists{}b:\mBbbN{}.  \mexists{}a:\mBbbN{}b.  \mforall{}k:\mBbbN{}p.  (A[k;a]  \mleq{}  A[k;b]))  \mvee{}  (A[0;n]  \mleq{}  A[0;G  n])))
7.  g  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}
8.  \mforall{}b:\mBbbN{}.  \mforall{}a:\mBbbN{}b.    g  a  <  g  b
9.  \mforall{}l:\mBbbN{}.  ((\mexists{}b:\mBbbN{}.  \mexists{}a:\mBbbN{}b.  \mforall{}k:\mBbbN{}p.  (A[k;a]  \mleq{}  A[k;b]))  \mvee{}  (A[0;g  l]  \mleq{}  A[0;g  (l  +  1)]))
10.  j  :  \mBbbN{}
11.  i  :  \mBbbN{}j
12.  \mforall{}k:\mBbbN{}p  -  1.  (A[k  +  1;g  i]  \mleq{}  A[k  +  1;g  j])
\mvdash{}  \mexists{}j:\mBbbN{}.  \mexists{}i:\mBbbN{}j.  \mforall{}k:\mBbbN{}p.  (A[k;i]  \mleq{}  A[k;j])


By

---

Latex:
TACTIC:TACTIC:Assert  \mkleeneopen{}\mforall{}n:\mBbbN{}\msupplus{}.  \mforall{}l:\mBbbN{}.
                                                ((\mexists{}b:\mBbbN{}.  \mexists{}a:\mBbbN{}b.  \mforall{}k:\mBbbN{}p.  (A[k;a]  \mleq{}  A[k;b]))  \mvee{}  (A[0;g  l]  \mleq{}  A[0;g  (l  +  n)]))\mkleeneclose{}\mcdot{}

---

Home Index