---

Step * of Lemma es-pred?_property

∀es:EO. ∀e:E.
  case es-pred?(es;e)
   of inl(p) =>
   (loc(p) = loc(e) ∈ Id) ∧ (p < e) ∧ (∀e':E. (e' < e) ⇒ ((e' = p ∈ E) ∨ (e' < p)) supposing loc(e') = loc(e) ∈ Id)
   | inr(z) =>
   ∀e':E. ¬(e' < e) supposing loc(e') = loc(e) ∈ Id
BY
{ (Auto THEN Unfold `es-pred?` 0 THEN AutoSplit) }

1
1. es : EO@i'
2. e : E@i
3. ↑first(e)
⊢ ∀e':E. ¬(e' < e) supposing loc(e') = loc(e) ∈ Id

2
1. es : EO@i'
2. e : E@i
3. ¬↑first(e)
⊢ (loc(pred(e)) = loc(e) ∈ Id)
∧ (pred(e) < e)
∧ (∀e':E. (e' < e) ⇒ ((e' = pred(e) ∈ E) ∨ (e' < pred(e))) supposing loc(e') = loc(e) ∈ Id)

---

Latex:


\mforall{}es:EO.  \mforall{}e:E.
    case  es-pred?(es;e)
      of  inl(p)  =>
      (loc(p)  =  loc(e))
      \mwedge{}  (p  <  e)
      \mwedge{}  (\mforall{}e':E.  (e'  <  e)  {}\mRightarrow{}  ((e'  =  p)  \mvee{}  (e'  <  p))  supposing  loc(e')  =  loc(e))
      |  inr(z)  =>
      \mforall{}e':E.  \mneg{}(e'  <  e)  supposing  loc(e')  =  loc(e)


By

(Auto  THEN  Unfold  `es-pred?`  0  THEN  AutoSplit)

---

Home Index