---

Step * 1 of Lemma dl-diamond-unwind-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))))))
BY
{ (Duplicate (8) THEN Unfold `rel_star` 8 THEN Reduce 8 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. n : ℕ
9. k [|a|]^n k'
10. [|phi|] k'
11. ([|a|]^*) k k'
⊢ ([|phi|] k) ∨ (∃k':K. (([|a|] k k') ∧ ((([|phi|] k') ⇒ False) ∨ (∃k'@0:K. ((([|a|]^*) k' k'@0) ∧ ([|phi|] k'@0))))))

---

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.  rel\_star(K;  [|a|])  k  k'
9.  [|phi|]  k'
\mvdash{}  ([|phi|]  k)
\mvee{}  (\mexists{}k':K
        (([|a|]  k  k')
        \mwedge{}  ((([|phi|]  k')  {}\mRightarrow{}  False)  \mvee{}  (\mexists{}k'@0:K.  ((([|a|]\^{}*)  k'  k'@0)  \mwedge{}  ([|phi|]  k'@0))))))


By

---

Latex:
(Duplicate  (8)  THEN  Unfold  `rel\_star`  8  THEN  Reduce  8  THEN  ExRepD)

---

Home Index