---

Step * of Lemma LTL-identities

∀es:EO. ∀[P:E ─→ ℙ]. ([][]P ≡ []P ∧ <><>P ≡ <>P ∧ <>P ≡ (TR ∪ P) ∧ []¬¬P ≡ ¬<>¬P ∧ ¬¬<>P ≡ ¬[]¬P)
BY
{ RepUR ``es-box es-diamond es-equiv es-until es-not es-TR`` 0
THEN Auto
THEN ExRepD
THEN Auto
THEN Try (Auto)
THEN ExRepD }

1
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'

2
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'))))

3
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'))))

---

Latex:


\mforall{}es:EO.  \mforall{}[P:E  {}\mrightarrow{}  \mBbbP{}].  ([][]P  \mequiv{}  []P  \mwedge{}  <><>P  \mequiv{}  <>P  \mwedge{}  <>P  \mequiv{}  (TR  \mcup{}  P)  \mwedge{}  []\mneg{}\mneg{}P  \mequiv{}  \mneg{}<>\mneg{}P  \mwedge{}  \mneg{}\mneg{}<>P  \mequiv{}  \mneg{}[]\mneg{}P)


By

RepUR  ``es-box  es-diamond  es-equiv  es-until  es-not  es-TR``  0
THEN  Auto
THEN  ExRepD
THEN  Auto
THEN  Try  (Auto)
THEN  ExRepD

---

Home Index