Step
*
1
2
2
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. 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) ∧ (∀l:ℕ. ((∃b:ℕ. ∃a:ℕb. ∀k:ℕp. (A[k;a] ≤ A[k;b])) ∨ (A[0;g l] ≤ A[0;g (l + 1)])))
⊢ ∃j:ℕ. ∃i:ℕj. ∀k:ℕp. (A[k;i] ≤ A[k;j])
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. 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])
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)
\mwedge{} (\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)])))
\mvdash{} \mexists{}j:\mBbbN{}. \mexists{}i:\mBbbN{}j. \mforall{}k:\mBbbN{}p. (A[k;i] \mleq{} A[k;j])
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