---

Step * 3 of Lemma dl-diamond-iterate


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'))
BY
{ (RenameVar `z' (-3) THEN D 0 With ⌜z⌝  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
8. [|a|] k k'
9. z : K
10. ([|a|]^*) k' z
11. [|phi|] z
⊢ ([|a|]^*) k z

---

Latex:

---

Latex:

1.  a  :  Prog
2.  phi  :  Prop
3.  K  :  Type
4.  R  :  \mBbbN{}  {}\mrightarrow{}  K  {}\mrightarrow{}  K  {}\mrightarrow{}  \mBbbP{}
5.  P  :  \mBbbN{}  {}\mrightarrow{}  K  {}\mrightarrow{}  \mBbbP{}
6.  k  :  K
7.  k'  :  K
8.  [|a|]  k  k'
9.  k'@0  :  K
10.  rel\_star(K;  [|a|])  k'  k'@0
11.  [|phi|]  k'@0
\mvdash{}  \mexists{}k':K.  ((rel\_star(K;  [|a|])  k  k')  \mwedge{}  ([|phi|]  k'))


By

---

Latex:
(RenameVar  `z'  (-3)  THEN  D  0  With  \mkleeneopen{}z\mkleeneclose{}    THEN  Auto)

---

Home Index