---

Step * 2 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@i
7. ∀e':E. (e ≤loc e'  ⇒ (¬¬(P e')))@i
⊢ ¬(∃e':E. (e ≤loc e'  ∧ (¬(P e'))))
BY
{ (D 0 THENA Auto)
THEN ExRepD
THEN (Assert ¬¬(P e') BY
            Auto)
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.  e  :  E@i
7.  \mforall{}e':E.  (e  \mleq{}loc  e'    {}\mRightarrow{}  (\mneg{}\mneg{}(P  e')))@i
\mvdash{}  \mneg{}(\mexists{}e':E.  (e  \mleq{}loc  e'    \mwedge{}  (\mneg{}(P  e'))))


By

(D  0  THENA  Auto)
THEN  ExRepD
THEN  (Assert  \mneg{}\mneg{}(P  e')  BY
                        Auto)
THEN  Auto

---

Home Index