---

Step * 2 1 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. do-apply(last(P);e) ~ do-apply(last(P);pred(e))
⊢ (↑can-apply(last(P);pred(e))) ⇒ (do-apply(last(P);pred(e)) ∈ E)
BY
{ (((InstLemma `es-local-pred_wf2` [⌈Info⌉;⌈es⌉;⌈pred(e)⌉;⌈P⌉]⋅ THENA Try (Complete (Auto)))
    THEN Unfolds ``can-apply do-apply`` 0
    )⋅
   THEN (GenConclAtAddr  [1;1;1]⋅ THENA Auto)
   THEN D (-2)
   THEN Reduce 0
   THEN Auto)⋅ }

---

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.  do-apply(last(P);e)  \msim{}  do-apply(last(P);pred(e))
\mvdash{}  (\muparrow{}can-apply(last(P);pred(e)))  {}\mRightarrow{}  (do-apply(last(P);pred(e))  \mmember{}  E)


By

---

Latex:
(((InstLemma  `es-local-pred\_wf2`  [\mkleeneopen{}Info\mkleeneclose{};\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}pred(e)\mkleeneclose{};\mkleeneopen{}P\mkleeneclose{}]\mcdot{}  THENA  Try  (Complete  (Auto)))
    THEN  Unfolds  ``can-apply  do-apply``  0
    )\mcdot{}
  THEN  (GenConclAtAddr    [1;1;1]\mcdot{}  THENA  Auto)
  THEN  D  (-2)
  THEN  Reduce  0
  THEN  Auto)\mcdot{}

---

Home Index