---

Step * of Lemma decidable__strictly-increasing-seq

∀n:ℕ. ∀s:ℕn ⟶ ℤ.  Dec(strictly-increasing-seq(n;s))
BY
{ (Unfold `strictly-increasing-seq` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}.  \mforall{}s:\mBbbN{}n  {}\mrightarrow{}  \mBbbZ{}.    Dec(strictly-increasing-seq(n;s))


By

---

Latex:
(Unfold  `strictly-increasing-seq`  0  THEN  Auto)

---

Home Index