---

Step * 3 of Lemma dl-box-iterate


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'
BY
{ ((RWO "rel_star_iff2" (-1) THEN Auto) THEN D -1 THEN Auto THEN ExRepD) }

1
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. z : K
11. k [|a|] z
12. z ([|a|]^*) k'
⊢ [|phi|] k'

---

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.  [|phi|]  k
8.  \mforall{}k':K.  (([|a|]  k  k')  {}\mRightarrow{}  (\mforall{}k'@0:K.  ((rel\_star(K;  [|a|])  k'  k'@0)  {}\mRightarrow{}  ([|phi|]  k'@0))))
9.  k'  :  K
10.  rel\_star(K;  [|a|])  k  k'
\mvdash{}  [|phi|]  k'


By

---

Latex:
((RWO  "rel\_star\_iff2"  (-1)  THEN  Auto)  THEN  D  -1  THEN  Auto  THEN  ExRepD)

---

Home Index