---

Step * 1 1 1 1 1 1 2 of Lemma not-ni-eventually-equal-inf


1. x : ℕ ⟶ 𝔹
2. ∀n:ℕ. ((↑(x (n + 1))) ⇒ (↑(x n)))
3. i : ℕ
4. ¬↑(x i)
5. m : {i...}
6. ¬m < 0
7. ↑(x m)
8. ∀d:ℕ. (¬↑(x (i + d)))
⊢ tt = ff
BY
{ (InstHyp [⌜m - i⌝] (-1)⋅ THENA Auto) }

1
1. x : ℕ ⟶ 𝔹
2. ∀n:ℕ. ((↑(x (n + 1))) ⇒ (↑(x n)))
3. i : ℕ
4. ¬↑(x i)
5. m : {i...}
6. ¬m < 0
7. ↑(x m)
8. ∀d:ℕ. (¬↑(x (i + d)))
9. ¬↑(x (i + (m - i)))
⊢ tt = ff

---

Latex:

---

Latex:

1.  x  :  \mBbbN{}  {}\mrightarrow{}  \mBbbB{}
2.  \mforall{}n:\mBbbN{}.  ((\muparrow{}(x  (n  +  1)))  {}\mRightarrow{}  (\muparrow{}(x  n)))
3.  i  :  \mBbbN{}
4.  \mneg{}\muparrow{}(x  i)
5.  m  :  \{i...\}
6.  \mneg{}m  <  0
7.  \muparrow{}(x  m)
8.  \mforall{}d:\mBbbN{}.  (\mneg{}\muparrow{}(x  (i  +  d)))
\mvdash{}  tt  =  ff


By

---

Latex:
(InstHyp  [\mkleeneopen{}m  -  i\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)

---

Home Index