---

Step * of Lemma es-pplus-first-since-exit

∀es:EO. ∀e1:E. ∀e2:{e:E| loc(e) = loc(e1) ∈ Id} .
  ∀[Q,R:{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] ∧ ∀e∈[a,b).¬R[e])+ ⇐⇒ e1 ≤loc e2  ∧ Q[e2] ∧ ∀e∈[e1,e2].R[e] ⇒ Q[e]))
BY
{ RepeatFor 8 ((D 0 THENA Complete (Auto))) }

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. [R] : {e:E| loc(e) = loc(e1) ∈ Id}  ─→ ℙ
6. ∀e:{e:E| loc(e) = loc(e1) ∈ Id} . Dec(Q[e])@i
7. [e1,e2]~([a,b].b = first e ≥ a.Q[e] ∧ ∀e∈[a,b).¬R[e])+@i
⊢ e1 ≤loc e2  ∧ Q[e2] ∧ ∀e∈[e1,e2].R[e] ⇒ Q[e]

2
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. [R] : {e:E| loc(e) = loc(e1) ∈ Id}  ─→ ℙ
6. ∀e:{e:E| loc(e) = loc(e1) ∈ Id} . Dec(Q[e])@i
7. e1 ≤loc e2  ∧ Q[e2] ∧ ∀e∈[e1,e2].R[e] ⇒ Q[e]@i
⊢ [e1,e2]~([a,b].b = first e ≥ a.Q[e] ∧ ∀e∈[a,b).¬R[e])+

---

Latex:


\mforall{}es:EO.  \mforall{}e1:E.  \mforall{}e2:\{e:E|  loc(e)  =  loc(e1)\}  .
    \mforall{}[Q,R:\{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]  \mwedge{}  \mforall{}e\mmember{}[a,b).\mneg{}R[e])+
              \mLeftarrow{}{}\mRightarrow{}  e1  \mleq{}loc  e2    \mwedge{}  Q[e2]  \mwedge{}  \mforall{}e\mmember{}[e1,e2].R[e]  {}\mRightarrow{}  Q[e]))


By

RepeatFor  8  ((D  0  THENA  Complete  (Auto)))

---

Home Index