---

Step * of Lemma eo-forward-pred

∀[Info:Type]. ∀[eo:EO+(Info)]. ∀[e:E]. ∀[e':E].  pred(e') = pred(e') ∈ E supposing ¬↑first(e')
BY
{ (Auto
   THEN (InstLemma `es-pred_property` [⌜eo.e⌝;⌜e'⌝]⋅ THENA Auto)
   THEN (RWO "eo-forward-loc eo-forward-causl" (-1) THENA Auto)
   THEN (Assert ¬↑first(e') BY
               ((D 0 THENA Auto)
                THEN RWO "assert-es-first" (-1)
                THEN Auto
                THEN With ⌜pred(e')⌝ (D (-1))⋅
                THEN Auto
                THEN D -1
                THEN Auto))
   THEN (InstLemma `es-pred_property` [⌜eo⌝;⌜e'⌝]⋅ THENA Auto)) }

1
1. Info : Type
2. eo : EO+(Info)
3. e : E
4. e' : E
5. ¬↑first(e')
6. (loc(pred(e')) = loc(e') ∈ Id)
∧ (pred(e') < e')
∧ (∀e'@0:E. (e'@0 < e') ⇒ ((e'@0 = pred(e') ∈ E) ∨ (e'@0 < pred(e'))) supposing loc(e'@0) = loc(e') ∈ Id)
7. ¬↑first(e')
8. (loc(pred(e')) = loc(e') ∈ Id)
∧ (pred(e') < e')
∧ (∀e'@0:E. (e'@0 < e') ⇒ ((e'@0 = pred(e') ∈ E) ∨ (e'@0 < pred(e'))) supposing loc(e'@0) = loc(e') ∈ Id)
⊢ pred(e') = pred(e') ∈ E

---

Latex:

---

Latex:
\mforall{}[Info:Type].  \mforall{}[eo:EO+(Info)].  \mforall{}[e:E].  \mforall{}[e':E].    pred(e')  =  pred(e')  supposing  \mneg{}\muparrow{}first(e')


By

---

Latex:
(Auto
  THEN  (InstLemma  `es-pred\_property`  [\mkleeneopen{}eo.e\mkleeneclose{};\mkleeneopen{}e'\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (RWO  "eo-forward-loc  eo-forward-causl"  (-1)  THENA  Auto)
  THEN  (Assert  \mneg{}\muparrow{}first(e')  BY
                          ((D  0  THENA  Auto)
                            THEN  RWO  "assert-es-first"  (-1)
                            THEN  Auto
                            THEN  With  \mkleeneopen{}pred(e')\mkleeneclose{}  (D  (-1))\mcdot{}
                            THEN  Auto
                            THEN  D  -1
                            THEN  Auto))
  THEN  (InstLemma  `es-pred\_property`  [\mkleeneopen{}eo\mkleeneclose{};\mkleeneopen{}e'\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index