---

Step * of Lemma dl-box-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) }

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

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

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

---

Latex:

---

Latex:
\mforall{}a:Prog.  \mforall{}phi:Prop.    ([(a)*]  phi  \mLeftarrow{}{}\mRightarrow{}  phi  \mwedge{}  [a]  [(a)*]  phi)


By

---

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

---

Home Index