---

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

.....wf..... 
1. Info : Type
2. es : EO+(Info)@i'
3. e : E@i
4. P : {e':E| (e' <loc e)}  ⟶ 𝔹@i
5. (¬↑first(e))
   ∧ (((↑(P pred(e))) ∧ (do-apply(last(P);e) ~ pred(e)))
     ∨ ((¬↑(P pred(e))) ∧ (↑can-apply(last(P);pred(e))) ∧ (do-apply(last(P);e) ~ do-apply(last(P);pred(e))))) 
   supposing ↑can-apply(last(P);e)
⊢ ↑can-apply(last(P);e) ∈ ℙ
BY
{ (((InstLemma `es-local-pred_wf2` [⌜Info⌝;⌜es⌝;⌜e⌝;⌜P⌝]⋅ THENA Try (Complete (Auto))) THEN Unfold `can-apply` 0)⋅
   THEN (GenConclAtAddr  [2;1]⋅ THENA Auto)
   THEN D (-2)
   THEN Reduce 0
   THEN Auto)⋅ }

---

Latex:

---

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


By

---

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

---

Home Index