---

Step * of Lemma es-prior-interface-cases

∀[Info:Type]
  ∀X:EClass(Top). ∀es:EO+(Info). ∀e:E.
    (¬↑first(e))
    ∧ (((↑pred(e) ∈b X) ∧ (prior(X)(e) = pred(e) ∈ E))
      ∨ ((¬↑pred(e) ∈b X) ∧ (↑pred(e) ∈b prior(X)) ∧ (prior(X)(e) = prior(X)(pred(e)) ∈ E))) 
    supposing ↑e ∈b prior(X)
BY
{ (InstLemma `es-local-pred-cases` []⋅
   THEN ParallelLast'
   THEN (D 0 THENA Auto)
   THEN ParallelOp -2
   THEN Thin (-4)
   THEN ParallelLast'
   THEN (SimpleInstHyp ⌜λe.e ∈b X⌝ (-1)⋅ THENA Auto)
   THEN Reduce (-1)
   THEN Thin (-2)
   THEN MoveToConcl (-1)
   THEN RepUR ``can-apply do-apply es-prior-interface local-pred-class in-eclass eclass-val`` 0) }

1
1. [Info] : Type
2. X : EClass(Top)@i'
3. es : EO+(Info)@i'
4. e : E@i
⊢ (¬↑first(e))
  ∧ (((↑(#(X es pred(e)) =z 1)) ∧ (outl(last(λe.(#(X es e) =z 1)) e) = pred(e) ∈ E))
    ∨ ((¬↑(#(X es pred(e)) =z 1))
      ∧ (↑isl(last(λe.(#(X es e) =z 1)) pred(e)))
      ∧ (outl(last(λe.(#(X es e) =z 1)) e) = outl(last(λe.(#(X es e) =z 1)) pred(e)) ∈ E))) 
  supposing ↑isl(last(λe.(#(X es e) =z 1)) e)
⇒ (¬↑first(e))
   ∧ (((↑(#(X es pred(e)) =z 1))
     ∧ (only(case last(λe.(#(X es e) =z 1)) e of inl(e') => {e'} | inr(x) => {}) = pred(e) ∈ E))
     ∨ ((¬↑(#(X es pred(e)) =z 1))
       ∧ (↑(#(case last(λe.(#(X es e) =z 1)) pred(e) of inl(e') => {e'} | inr(x) => {}) =z 1))
       ∧ (only(case last(λe.(#(X es e) =z 1)) e of inl(e') => {e'} | inr(x) => {})
         = only(case last(λe.(#(X es e) =z 1)) pred(e) of inl(e') => {e'} | inr(x) => {})
         ∈ E))) 
   supposing ↑(#(case last(λe.(#(X es e) =z 1)) e of inl(e') => {e'} | inr(x) => {}) =z 1)

---

Latex:

---

Latex:
\mforall{}[Info:Type]
    \mforall{}X:EClass(Top).  \mforall{}es:EO+(Info).  \mforall{}e:E.
        (\mneg{}\muparrow{}first(e))
        \mwedge{}  (((\muparrow{}pred(e)  \mmember{}\msubb{}  X)  \mwedge{}  (prior(X)(e)  =  pred(e)))
            \mvee{}  ((\mneg{}\muparrow{}pred(e)  \mmember{}\msubb{}  X)  \mwedge{}  (\muparrow{}pred(e)  \mmember{}\msubb{}  prior(X))  \mwedge{}  (prior(X)(e)  =  prior(X)(pred(e))))) 
        supposing  \muparrow{}e  \mmember{}\msubb{}  prior(X)


By

---

Latex:
(InstLemma  `es-local-pred-cases`  []\mcdot{}
  THEN  ParallelLast'
  THEN  (D  0  THENA  Auto)
  THEN  ParallelOp  -2
  THEN  Thin  (-4)
  THEN  ParallelLast'
  THEN  (SimpleInstHyp  \mkleeneopen{}\mlambda{}e.e  \mmember{}\msubb{}  X\mkleeneclose{}  (-1)\mcdot{}  THENA  Auto)
  THEN  Reduce  (-1)
  THEN  Thin  (-2)
  THEN  MoveToConcl  (-1)
  THEN  RepUR  ``can-apply  do-apply  es-prior-interface  local-pred-class  in-eclass  eclass-val``  0)

---

Home Index