---

Step * 1 1 1 of Lemma decidable__run-pred


1. e5 : ℕ@i
2. e6 : Id@i
3. e7 : ℕ@i
4. e8 : Id@i
5. ¬((e6 = e8 ∈ Id) ∧ e5 < e7)
6. e3 : ℤ@i
7. e4 : Id@i
8. ¬((e6 = e4 ∈ Id) ∧ (e5 = e3 ∈ ℤ))
9. ff ∈ 𝔹
10. ff ∈ 𝔹
11. x1 : e6 = e8 ∈ Id × e5 < e7@i
⊢ Ax ∈ False
BY
{ (D 5 THEN D -1 THEN Auto) }

---

Latex:

---

Latex:

1.  e5  :  \mBbbN{}@i
2.  e6  :  Id@i
3.  e7  :  \mBbbN{}@i
4.  e8  :  Id@i
5.  \mneg{}((e6  =  e8)  \mwedge{}  e5  <  e7)
6.  e3  :  \mBbbZ{}@i
7.  e4  :  Id@i
8.  \mneg{}((e6  =  e4)  \mwedge{}  (e5  =  e3))
9.  ff  \mmember{}  \mBbbB{}
10.  ff  \mmember{}  \mBbbB{}
11.  x1  :  e6  =  e8  \mtimes{}  e5  <  e7@i
\mvdash{}  Ax  \mmember{}  False


By

---

Latex:
(D  5  THEN  D  -1  THEN  Auto)

---

Home Index