---

Step * 2 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. (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]
BY
{ (Unfolds ``existse-le alle-between3`` 0
   THEN RepeatFor 6 ((ParallelLast THEN Try (Complete (Auto))))
   THEN SupposeNot
   THEN Auto) }

---

Latex:



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


By

(Unfolds  ``existse-le  alle-between3``  0
  THEN  RepeatFor  6  ((ParallelLast  THEN  Try  (Complete  (Auto))))
  THEN  SupposeNot
  THEN  Auto)

---

Home Index