---

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

∀[Info:Type]
  ∀es:EO+(Info). ∀e:E. ∀P:{e':E| (e' <loc e)}  ─→ 𝔹.
    (¬↑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)
BY
{ (RepeatFor 4 ((D 0 THENA Auto))
   THEN RepUR ``can-apply do-apply`` 0
   THEN (Subst' last(P) e ~ (λe.if first(e) then inr (λx.⋅)  if P pred(e) then inl pred(e) else last(P) pred(e) fi ) e 0
         THENL [(RW (AddrC [1] (RecUnfoldC `es-local-pred`)) 0⋅ THEN Auto); (Reduce 0⋅ THEN RepeatFor 2 (AutoSplit))]
   )) }

1
1. [Info] : Type
2. es : EO+(Info)@i'
3. e : E@i
4. ¬↑first(e)
5. P : {e':E| (e' <loc e)}  ─→ 𝔹@i
6. ¬↑(P pred(e))
⊢ (¬False)
  ∧ ((False ∧ (outl(last(P) pred(e)) ~ pred(e)))
    ∨ ((¬False) ∧ (↑isl(last(P) pred(e))) ∧ (outl(last(P) pred(e)) ~ outl(last(P) pred(e))))) 
  supposing ↑isl(last(P) pred(e))

---

Latex:

---

Latex:
\mforall{}[Info:Type]
    \mforall{}es:EO+(Info).  \mforall{}e:E.  \mforall{}P:\{e':E|  (e'  <loc  e)\}    {}\mrightarrow{}  \mBbbB{}.
        (\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)


By

---

Latex:
(RepeatFor  4  ((D  0  THENA  Auto))
  THEN  RepUR  ``can-apply  do-apply``  0
  THEN  (Subst'  last(P)  e  \msim{}  (\mlambda{}e.if  first(e)  then  inr  (\mlambda{}x.\mcdot{}) 
                                                            if  P  pred(e)  then  inl  pred(e)
                                                            else  last(P)  pred(e)
                                                            fi  ) 
                                                    e  0
              THENL  [(RW  (AddrC  [1]  (RecUnfoldC  `es-local-pred`))  0\mcdot{}  THEN  Auto)
                          ;  (Reduce  0\mcdot{}  THEN  RepeatFor  2  (AutoSplit))]
  ))

---

Home Index