---

Step * of Lemma es-first-at-implies-first-at

∀es:EO. ∀i:Id.
  ∀[P:{e:E| loc(e) = i ∈ Id}  ─→ ℙ]
    ∀e:E
      (e is first@ i s.t.  e.P[e]
      ⇒ {∀[Q:{e:E| loc(e) = i ∈ Id}  ─→ ℙ]
            (e is first@ i s.t.  e.Q[e] ⇐⇒ Q[e] ∧ ∀e'<e.e' is first@ i s.t.  e.Q[e] ⇒ P[e'])})
BY
{ (Unfold `guard` 0
   THEN Auto
   THEN D 0
   THEN Auto
   THEN Try ((Assert ⌈¬Q[e']⌉⋅ THEN Auto THEN D (-1) THEN Complete (Auto)))
   THEN UnfoldTopAb 0
   THEN CausalInd'
   THEN (D 0 THEN Auto)
   THEN (D 0 THENA Auto)
   THEN Assert ⌈P[e'] ∧ (¬P[e'])⌉⋅
   THEN Auto
   THEN BackThruSomeHyp'
   THEN Auto
   THEN (RepeatFor 2 ((D 0 THEN Auto)) THEN BackThruSomeHyp' THEN Auto)⋅) }

---

Latex:


\mforall{}es:EO.  \mforall{}i:Id.
    \mforall{}[P:\{e:E|  loc(e)  =  i\}    {}\mrightarrow{}  \mBbbP{}]
        \mforall{}e:E
            (e  is  first@  i  s.t.    e.P[e]
            {}\mRightarrow{}  \{\mforall{}[Q:\{e:E|  loc(e)  =  i\}    {}\mrightarrow{}  \mBbbP{}]
                        (e  is  first@  i  s.t.    e.Q[e]  \mLeftarrow{}{}\mRightarrow{}  Q[e]  \mwedge{}  \mforall{}e'<e.e'  is  first@  i  s.t.    e.Q[e]  {}\mRightarrow{}  P[e'])\})


By

(Unfold  `guard`  0
  THEN  Auto
  THEN  D  0
  THEN  Auto
  THEN  Try  ((Assert  \mkleeneopen{}\mneg{}Q[e']\mkleeneclose{}\mcdot{}  THEN  Auto  THEN  D  (-1)  THEN  Complete  (Auto)))
  THEN  UnfoldTopAb  0
  THEN  CausalInd'
  THEN  (D  0  THEN  Auto)
  THEN  (D  0  THENA  Auto)
  THEN  Assert  \mkleeneopen{}P[e']  \mwedge{}  (\mneg{}P[e'])\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  BackThruSomeHyp'
  THEN  Auto
  THEN  (RepeatFor  2  ((D  0  THEN  Auto))  THEN  BackThruSomeHyp'  THEN  Auto)\mcdot{})

---

Home Index