---

Step * 1 of Lemma last-transition


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]
BY
{ (RepeatFor 3 (ParallelLast) THEN SupposeNot THEN Auto) }

---

Latex:

---

Latex:

1.  es  :  EO@i'
2.  e  :  E@i
3.  P  :  \{a:E|  loc(a)  =  loc(e)\}    {}\mrightarrow{}  \mBbbB{}@i
4.  \mforall{}e'\mleq{}e.\mneg{}\mneg{}P[e']  =  P[e]
\mvdash{}  \mforall{}e'\mleq{}e.P[e']  =  P[e]


By

---

Latex:
(RepeatFor  3  (ParallelLast)  THEN  SupposeNot  THEN  Auto)

---

Home Index