---

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

.....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. ∀n,m:ℕ.  ∃i:ℕ. (m < i ∧ ((∃b:ℕ. ∃a:ℕb. ∀k:ℕp. (A[k;a] ≤ A[k;b])) ∨ (n ≤ A[0;i])))
⊢ ∀n:ℕ. ∃i:ℕ. (n < i ∧ ((∃b:ℕ. ∃a:ℕb. ∀k:ℕp. (A[k;a] ≤ A[k;b])) ∨ (A[0;n] ≤ A[0;i])))
BY
{ TACTIC:(Auto THEN BackThruSomeHyp) }

---

Latex:

---

Latex:
.....assertion..... 
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.  \mforall{}n,m:\mBbbN{}.    \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])))
\mvdash{}  \mforall{}n:\mBbbN{}.  \mexists{}i:\mBbbN{}.  (n  <  i  \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;i])))


By

---

Latex:
TACTIC:(Auto  THEN  BackThruSomeHyp)

---

Home Index