---

Step * 1 1 2 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. [|phi|] k'
9. ([|a|]^*) k k'
10. n : ℤ
11. [%5] : 0 < n
12. (k [|a|]^n - 1 k')
⇒ (([|phi|] k)
   ∨ (∃k':K. (([|a|] k k') ∧ ((([|phi|] k') ⇒ False) ∨ (∃k'@0:K. ((([|a|]^*) k' k'@0) ∧ ([|phi|] k'@0)))))))
13. k [|a|]^n k'
14. (k [|a|]^1 + (n - 1) k') ⇐ ∃y:K. ((k [|a|]^1 y) ∧ (y [|a|]^n - 1 k'))
15. ∃y:K. ((k [|a|]^1 y) ∧ (y [|a|]^n - 1 k'))
⊢ ([|phi|] k) ∨ (∃k':K. (([|a|] k k') ∧ ((([|phi|] k') ⇒ False) ∨ (∃k'@0:K. ((([|a|]^*) k' k'@0) ∧ ([|phi|] k'@0))))))
BY
{ (((OrRight THENA Auto) THEN ExRepD) THEN D 0 With ⌜y⌝  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. [|phi|] k'
9. ([|a|]^*) k k'
10. n : ℤ
11. [%5] : 0 < n
12. (k [|a|]^n - 1 k')
⇒ (([|phi|] k)
   ∨ (∃k':K. (([|a|] k k') ∧ ((([|phi|] k') ⇒ False) ∨ (∃k'@0:K. ((([|a|]^*) k' k'@0) ∧ ([|phi|] k'@0)))))))
13. k [|a|]^n k'
14. (k [|a|]^1 + (n - 1) k') ⇐ ∃y:K. ((k [|a|]^1 y) ∧ (y [|a|]^n - 1 k'))
15. y : K
16. k [|a|]^1 y
17. y [|a|]^n - 1 k'
⊢ [|a|] k y

2
1. a : Prog
2. phi : Prop
3. K : Type
4. R : ℕ ⟶ K ⟶ K ⟶ ℙ
5. P : ℕ ⟶ K ⟶ ℙ
6. k : K
7. k' : K
8. [|phi|] k'
9. ([|a|]^*) k k'
10. n : ℤ
11. [%5] : 0 < n
12. (k [|a|]^n - 1 k')
⇒ (([|phi|] k)
   ∨ (∃k':K. (([|a|] k k') ∧ ((([|phi|] k') ⇒ False) ∨ (∃k'@0:K. ((([|a|]^*) k' k'@0) ∧ ([|phi|] k'@0)))))))
13. k [|a|]^n k'
14. (k [|a|]^1 + (n - 1) k') ⇐ ∃y:K. ((k [|a|]^1 y) ∧ (y [|a|]^n - 1 k'))
15. y : K
16. k [|a|]^1 y
17. y [|a|]^n - 1 k'
18. [|a|] k y
⊢ (([|phi|] y) ⇒ False) ∨ (∃k'@0:K. ((([|a|]^*) y 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.  [|phi|]  k'
9.  rel\_star(K;  [|a|])  k  k'
10.  n  :  \mBbbZ{}
11.  [\%5]  :  0  <  n
12.  (k  rel\_exp(K;  [|a|];  n  -  1)  k')
{}\mRightarrow{}  (([|phi|]  k)
      \mvee{}  (\mexists{}k':K
              (([|a|]  k  k')
              \mwedge{}  ((([|phi|]  k')  {}\mRightarrow{}  False)  \mvee{}  (\mexists{}k'@0:K.  ((rel\_star(K;  [|a|])  k'  k'@0)  \mwedge{}  ([|phi|]  k'@0)))))))
13.  k  rel\_exp(K;  [|a|];  n)  k'
14.  (k  rel\_exp(K;  [|a|];  1  +  (n  -  1))  k')  \mLeftarrow{}{}  \mexists{}y:K
                                                                                            ((k  [|a|]\^{}1  y)  \mwedge{}  (y  [|a|]\^{}n  -  1  k'))
15.  \mexists{}y:K.  ((k  rel\_exp(K;  [|a|];  1)  y)  \mwedge{}  (y  rel\_exp(K;  [|a|];  n  -  1)  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:
(((OrRight  THENA  Auto)  THEN  ExRepD)  THEN  D  0  With  \mkleeneopen{}y\mkleeneclose{}    THEN  Auto)

---

Home Index