---

Step * of Lemma last-transition

∀es:EO. ∀e:E. ∀P:{a:E| loc(a) = loc(e) ∈ Id}  ─→ 𝔹.
  (∀e'≤e.P[e'] = P[e] ∨ ∃e'≤e.(¬P[e'] = P[e]) ∧ ∀e''∈(e',e].P[e''] = P[e])
BY
{ (Auto
   THEN ((InstLemma `last-event` [⌈es⌉; ⌈e⌉; ⌈λ2e'.¬P[e'] = P[e]⌉])⋅ THENA Auto)
   THEN (D -1 THENL [OrLeft; OrRight])
   THEN Try (Complete (Auto))) }

1
1. es : EO@i'
2. e : E@i
3. P : {a:E| loc(a) = loc(e) ∈ Id}  ─→ 𝔹@i
4. ∀e'≤e.¬¬P[e'] = P[e]
⊢ ∀e'≤e.P[e'] = P[e]

2
1. es : EO@i'
2. e : E@i
3. P : {a:E| loc(a) = loc(e) ∈ Id}  ─→ 𝔹@i
4. ∃e':E. (e' ≤loc e  c∧ ((¬P[e'] = P[e]) ∧ (∀e'':E. ((e' <loc e'') ⇒ e'' ≤loc e  ⇒ (¬¬P[e''] = P[e])))))
⊢ ∃e'≤e.(¬P[e'] = P[e]) ∧ ∀e''∈(e',e].P[e''] = P[e]

---

Latex:


\mforall{}es:EO.  \mforall{}e:E.  \mforall{}P:\{a:E|  loc(a)  =  loc(e)\}    {}\mrightarrow{}  \mBbbB{}.
    (\mforall{}e'\mleq{}e.P[e']  =  P[e]  \mvee{}  \mexists{}e'\mleq{}e.(\mneg{}P[e']  =  P[e])  \mwedge{}  \mforall{}e''\mmember{}(e',e].P[e'']  =  P[e])


By

(Auto
  THEN  ((InstLemma  `last-event`  [\mkleeneopen{}es\mkleeneclose{};  \mkleeneopen{}e\mkleeneclose{};  \mkleeneopen{}\mlambda{}\msubtwo{}e'.\mneg{}P[e']  =  P[e]\mkleeneclose{}])\mcdot{}  THENA  Auto)
  THEN  (D  -1  THENL  [OrLeft;  OrRight])
  THEN  Try  (Complete  (Auto)))

---

Home Index