---

Step * of Lemma dl-diamond-iterate

∀a:Prog. ∀phi:Prop.  (<(a)*> phi ⇐⇒ phi ∨ <a> <(a)*> phi)
BY
{ (Auto THEN RepeatFor 2 ((D 0 THEN Auto)) THEN DlSemReduce 0 THEN Auto THEN SplitOrHyps 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') ∧ (∃k'@0:K. ((([|a|]^*) k' k'@0) ∧ ([|phi|] k'@0)))))

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

3
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. k'@0 : K
10. ([|a|]^*) k' k'@0
11. [|phi|] k'@0
⊢ ∃k':K. ((([|a|]^*) k k') ∧ ([|phi|] k'))

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  RepeatFor  2  ((D  0  THEN  Auto))  THEN  DlSemReduce  0  THEN  Auto  THEN  SplitOrHyps  THEN  ExRepD)

---

Home Index