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