---

Step * 1 of Lemma decidable__run-pred


1. e5 : ℕ@i
2. e6 : Id@i
3. e7 : ℕ@i
4. e8 : Id@i
5. e3 : ℤ@i
6. e4 : Id@i
⊢ if e6 = e8 ∧b e5 <z e7 then inl inl <Ax, Ax>
  if e6 = e4 ∧b (e5 =z e3) then inl (inr Ax )
  else inr (λx.Ax) 
  fi  ∈ e6 = e8 ∈ Id × e5 < e7 + (<e5, e6> = <e3, e4> ∈ (ℤ × Id)) + ((e6 = e8 ∈ Id × e5 < e7 + (<e5, e6>
                                                                                              = <e3, e4>
                                                                                              ∈ (ℤ × Id)))
                                                                   ⇒ False)
BY
{ Auto }

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. x : e6 = e8 ∈ Id × e5 < e7 + (<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.  e3  :  \mBbbZ{}@i
6.  e4  :  Id@i
\mvdash{}  if  e6  =  e8  \mwedge{}\msubb{}  e5  <z  e7  then  inl  inl  <Ax,  Ax>
    if  e6  =  e4  \mwedge{}\msubb{}  (e5  =\msubz{}  e3)  then  inl  (inr  Ax  )
    else  inr  (\mlambda{}x.Ax) 
    fi    \mmember{}  e6  =  e8  \mtimes{}  e5  <  e7  +  (<e5,  e6>  =  <e3,  e4>)  +  ((e6  =  e8  \mtimes{}  e5  <  e7  +  (<e5,  e6>  =  <e3,  e4>))
                                                                                                      {}\mRightarrow{}  False)


By

---

Latex:
Auto

---

Home Index