---

Step * 1 of Lemma LTL-identities


1. es : EO@i'
2. [P] : E ─→ ℙ
3. e : E@i
4. ∀e':E. (e ≤loc e'  ⇒ (∀e'@0:E. (e' ≤loc e'@0  ⇒ (P e'@0))))@i
5. e' : E@i
6. e ≤loc e' @i
⊢ P e'
BY
{ InstHyp [⌈e'⌉;⌈e'⌉] (-3)⋅
THEN Auto }

---

Latex:



1.  es  :  EO@i'
2.  [P]  :  E  {}\mrightarrow{}  \mBbbP{}
3.  e  :  E@i
4.  \mforall{}e':E.  (e  \mleq{}loc  e'    {}\mRightarrow{}  (\mforall{}e'@0:E.  (e'  \mleq{}loc  e'@0    {}\mRightarrow{}  (P  e'@0))))@i
5.  e'  :  E@i
6.  e  \mleq{}loc  e'  @i
\mvdash{}  P  e'


By

InstHyp  [\mkleeneopen{}e'\mkleeneclose{};\mkleeneopen{}e'\mkleeneclose{}]  (-3)\mcdot{}
THEN  Auto

---

Home Index