---

Step * 3 of Lemma LTL-identities


1. es : EO@i'
2. P : E ─→ ℙ
3. ∀e:E. (∀e':E. (e ≤loc e'  ⇒ (∀e'@0:E. (e' ≤loc e'@0  ⇒ (P e'@0)))) ⇐⇒ ∀e':E. (e ≤loc e'  ⇒ (P e')))
4. ∀e:E. (∃e':E. (e ≤loc e'  ∧ (∃e'@0:E. (e' ≤loc e'@0  ∧ (P e'@0)))) ⇐⇒ ∃e':E. (e ≤loc e'  ∧ (P e')))
5. ∀e:E
     (∃e':E. (e ≤loc e'  ∧ (P e')) ⇐⇒ ∃e':E. (e ≤loc e'  ∧ (P e') ∧ (∀e'':E. (e ≤loc e''  ⇒ (e'' <loc e') ⇒ True))))
6. ∀e:E. (∀e':E. (e ≤loc e'  ⇒ (¬¬(P e'))) ⇐⇒ ¬(∃e':E. (e ≤loc e'  ∧ (¬(P e')))))
7. e : E@i
8. ¬¬(∃e':E. (e ≤loc e'  ∧ (P e')))@i
⊢ ¬(∀e':E. (e ≤loc e'  ⇒ (¬(P e'))))
BY
{ ParallelLast
THEN (D 0 THENA Auto)
THEN ExRepD
THEN Contradict (-1)
THEN Auto }

---

Latex:



1.  es  :  EO@i'
2.  P  :  E  {}\mrightarrow{}  \mBbbP{}
3.  \mforall{}e:E
          (\mforall{}e':E.  (e  \mleq{}loc  e'    {}\mRightarrow{}  (\mforall{}e'@0:E.  (e'  \mleq{}loc  e'@0    {}\mRightarrow{}  (P  e'@0))))
          \mLeftarrow{}{}\mRightarrow{}  \mforall{}e':E.  (e  \mleq{}loc  e'    {}\mRightarrow{}  (P  e')))
4.  \mforall{}e:E
          (\mexists{}e':E.  (e  \mleq{}loc  e'    \mwedge{}  (\mexists{}e'@0:E.  (e'  \mleq{}loc  e'@0    \mwedge{}  (P  e'@0))))  \mLeftarrow{}{}\mRightarrow{}  \mexists{}e':E.  (e  \mleq{}loc  e'    \mwedge{}  (P  e')))
5.  \mforall{}e:E
          (\mexists{}e':E.  (e  \mleq{}loc  e'    \mwedge{}  (P  e'))
          \mLeftarrow{}{}\mRightarrow{}  \mexists{}e':E.  (e  \mleq{}loc  e'    \mwedge{}  (P  e')  \mwedge{}  (\mforall{}e'':E.  (e  \mleq{}loc  e''    {}\mRightarrow{}  (e''  <loc  e')  {}\mRightarrow{}  True))))
6.  \mforall{}e:E.  (\mforall{}e':E.  (e  \mleq{}loc  e'    {}\mRightarrow{}  (\mneg{}\mneg{}(P  e')))  \mLeftarrow{}{}\mRightarrow{}  \mneg{}(\mexists{}e':E.  (e  \mleq{}loc  e'    \mwedge{}  (\mneg{}(P  e')))))
7.  e  :  E@i
8.  \mneg{}\mneg{}(\mexists{}e':E.  (e  \mleq{}loc  e'    \mwedge{}  (P  e')))@i
\mvdash{}  \mneg{}(\mforall{}e':E.  (e  \mleq{}loc  e'    {}\mRightarrow{}  (\mneg{}(P  e'))))


By

ParallelLast
THEN  (D  0  THENA  Auto)
THEN  ExRepD
THEN  Contradict  (-1)
THEN  Auto

---

Home Index