---

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


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))
BY
{ ((D 0 THENM Auto)
   THEN (GenConcl ⌈(last(P) pred(e)) = Z ∈ (Top + Top)⌉⋅ THENM (D (-2) THEN Reduce 0 THEN Auto)⋅)
   THEN DoSubsume
   THEN Try (BLemma `es-local-pred_wf2`)
   THEN Auto) }

---

Latex:

---

Latex:

1.  [Info]  :  Type
2.  es  :  EO+(Info)@i'
3.  e  :  E@i
4.  \mneg{}\muparrow{}first(e)
5.  P  :  \{e':E|  (e'  <loc  e)\}    {}\mrightarrow{}  \mBbbB{}@i
6.  \mneg{}\muparrow{}(P  pred(e))
\mvdash{}  (\mneg{}False)
    \mwedge{}  ((False  \mwedge{}  (outl(last(P)  pred(e))  \msim{}  pred(e)))
        \mvee{}  ((\mneg{}False)  \mwedge{}  (\muparrow{}isl(last(P)  pred(e)))  \mwedge{}  (outl(last(P)  pred(e))  \msim{}  outl(last(P)  pred(e))))) 
    supposing  \muparrow{}isl(last(P)  pred(e))


By

---

Latex:
((D  0  THENM  Auto)
  THEN  (GenConcl  \mkleeneopen{}(last(P)  pred(e))  =  Z\mkleeneclose{}\mcdot{}  THENM  (D  (-2)  THEN  Reduce  0  THEN  Auto)\mcdot{})
  THEN  DoSubsume
  THEN  Try  (BLemma  `es-local-pred\_wf2`)
  THEN  Auto)

---

Home Index