---

Step * 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. x : e6 = e8 ∈ Id × e5 < e7 + (<e5, e6> = <e3, e4> ∈ (ℤ × Id))@i
⊢ Ax ∈ False
BY
{ D (-1) }

1
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

2
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. y : <e5, e6> = <e3, e4> ∈ (ℤ × Id)@i
⊢ Ax ∈ False

---

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.  x  :  e6  =  e8  \mtimes{}  e5  <  e7  +  (<e5,  e6>  =  <e3,  e4>)@i
\mvdash{}  Ax  \mmember{}  False


By

---

Latex:
D  (-1)

---

Home Index