---

Step * of Lemma dl-diamond-unwind-1

∀a:Prog. ∀phi:Prop.  |= <(a)*> phi ⇒ (phi ∨ <a> (phi ⇒ 0) ∨ <(a)*> phi)
BY
{ (((Auto THEN Unfold `dl-valid` 0) THEN Auto) THEN DlSemReduce 0 THEN Auto THEN ExRepD) }

1
1. a : Prog
2. phi : Prop
3. K : Type
4. R : ℕ ⟶ K ⟶ K ⟶ ℙ
5. P : ℕ ⟶ K ⟶ ℙ
6. k : K
7. k' : K
8. ([|a|]^*) k k'
9. [|phi|] k'
⊢ ([|phi|] k) ∨ (∃k':K. (([|a|] k k') ∧ ((([|phi|] k') ⇒ False) ∨ (∃k'@0:K. ((([|a|]^*) k' k'@0) ∧ ([|phi|] k'@0))))))

---

Latex:

---

Latex:
\mforall{}a:Prog.  \mforall{}phi:Prop.    |=  <(a)*>  phi  {}\mRightarrow{}  (phi  \mvee{}  <a>  (phi  {}\mRightarrow{}  0)  \mvee{}  <(a)*>  phi)


By

---

Latex:
(((Auto  THEN  Unfold  `dl-valid`  0)  THEN  Auto)  THEN  DlSemReduce  0  THEN  Auto  THEN  ExRepD)

---

Home Index