---

Step * 2 of Lemma es-local-pred-cases


1. Info : Type
2. es : EO+(Info)@i'
3. e : E@i
4. P : {e':E| (e' <loc e)}  ─→ 𝔹@i
5. ↑can-apply(last(P);e)
6. ¬↑first(e)
7. ¬↑(P pred(e))
8. ↑can-apply(last(P);pred(e))
9. do-apply(last(P);e) ~ do-apply(last(P);pred(e))
⊢ do-apply(last(P);pred(e)) ∈ E
BY
{ MoveToConcl (-2) }

1
1. Info : Type
2. es : EO+(Info)@i'
3. e : E@i
4. P : {e':E| (e' <loc e)}  ─→ 𝔹@i
5. ↑can-apply(last(P);e)
6. ¬↑first(e)
7. ¬↑(P pred(e))
8. do-apply(last(P);e) ~ do-apply(last(P);pred(e))
⊢ (↑can-apply(last(P);pred(e))) ⇒ (do-apply(last(P);pred(e)) ∈ E)

---

Latex:

---

Latex:

1.  Info  :  Type
2.  es  :  EO+(Info)@i'
3.  e  :  E@i
4.  P  :  \{e':E|  (e'  <loc  e)\}    {}\mrightarrow{}  \mBbbB{}@i
5.  \muparrow{}can-apply(last(P);e)
6.  \mneg{}\muparrow{}first(e)
7.  \mneg{}\muparrow{}(P  pred(e))
8.  \muparrow{}can-apply(last(P);pred(e))
9.  do-apply(last(P);e)  \msim{}  do-apply(last(P);pred(e))
\mvdash{}  do-apply(last(P);pred(e))  \mmember{}  E


By

---

Latex:
MoveToConcl  (-2)

---

Home Index