---

Step * of Lemma es-pplus-first-since

∀es:EO. ∀e1:E. ∀e2:{e:E| loc(e) = loc(e1) ∈ Id} .
  ∀[Q:{e:E| loc(e) = loc(e1) ∈ Id}  ─→ ℙ]
    ((∀e:{e:E| loc(e) = loc(e1) ∈ Id} . Dec(Q[e])) ⇒ ([e1,e2]~([a,b].b = first e ≥ a.Q[e])+ ⇐⇒ e1 ≤loc e2  ∧ Q[e2]))
BY
{ (Auto
   THEN Auto
   THEN Try (((FLemma `es-pplus-le` [(-1)]) THEN Auto))
   THEN Try (((D (-2)) THEN ExRepD THEN (D (-2)) THEN ExRepD THEN Trivial))) }

1
1. es : EO@i'
2. e1 : E@i
3. e2 : {e:E| loc(e) = loc(e1) ∈ Id} @i
4. [Q] : {e:E| loc(e) = loc(e1) ∈ Id}  ─→ ℙ
5. ∀e:{e:E| loc(e) = loc(e1) ∈ Id} . Dec(Q[e])@i
6. e1 ≤loc e2 @i
7. Q[e2]@i
⊢ [e1,e2]~([a,b].b = first e ≥ a.Q[e])+

---

Latex:


\mforall{}es:EO.  \mforall{}e1:E.  \mforall{}e2:\{e:E|  loc(e)  =  loc(e1)\}  .
    \mforall{}[Q:\{e:E|  loc(e)  =  loc(e1)\}    {}\mrightarrow{}  \mBbbP{}]
        ((\mforall{}e:\{e:E|  loc(e)  =  loc(e1)\}  .  Dec(Q[e]))
        {}\mRightarrow{}  ([e1,e2]\msim{}([a,b].b  =  first  e  \mgeq{}  a.Q[e])+  \mLeftarrow{}{}\mRightarrow{}  e1  \mleq{}loc  e2    \mwedge{}  Q[e2]))


By

(Auto
  THEN  Auto
  THEN  Try  (((FLemma  `es-pplus-le`  [(-1)])  THEN  Auto))
  THEN  Try  (((D  (-2))  THEN  ExRepD  THEN  (D  (-2))  THEN  ExRepD  THEN  Trivial)))

---

Home Index