---

Step * 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 ∈ ℤ
⊢ ∃j:ℕ. ∃i:ℕj. ∀k:ℕ0. (A[k;i] ≤ A[k;j])
BY
{ TACTIC:(InstConcl [⌜1⌝;⌜0⌝] ⋅ THEN Auto) }

---

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.  p  =  0
\mvdash{}  \mexists{}j:\mBbbN{}.  \mexists{}i:\mBbbN{}j.  \mforall{}k:\mBbbN{}0.  (A[k;i]  \mleq{}  A[k;j])


By

---

Latex:
TACTIC:(InstConcl  [\mkleeneopen{}1\mkleeneclose{};\mkleeneopen{}0\mkleeneclose{}]  \mcdot{}  THEN  Auto)

---

Home Index