---

Step * 1 1 1 2 1 of Lemma ts-reachable-induction3


1. ts : transition-system{i:l}
2. [P] : ts-reachable(ts) ⟶ ℙ
3. P[ts-init(ts)]
4. ∀x:ts-type(ts). (((ts-rel(ts)^*) ts-init(ts) x) ⇒ (∀y:ts-reachable(ts). (P[x] ⇒ (ts-rel(ts) x y) ⇒ P[y])))
5. x : ts-type(ts)
6. n : ℤ
7. [%3] : 0 < n
8. ∀v:ts-reachable(ts). ((ts-rel(ts)^n - 1 ts-init(ts) v) ⇒ P[v])
9. v : ts-reachable(ts)
10. z : ts-type(ts)
11. 0 < n
12. ts-rel(ts)^n - 1 ts-init(ts) z
13. ts-rel(ts) z v
14. z ∈ ts-reachable(ts)
15. P[z]
⊢ P[v]
BY
{ xxx(InstHyp [⌜z⌝] 4⋅ THEN Auto)xxx }

1
.....antecedent..... 
1. ts : transition-system{i:l}
2. [P] : ts-reachable(ts) ⟶ ℙ
3. P[ts-init(ts)]
4. ∀x:ts-type(ts). (((ts-rel(ts)^*) ts-init(ts) x) ⇒ (∀y:ts-reachable(ts). (P[x] ⇒ (ts-rel(ts) x y) ⇒ P[y])))
5. x : ts-type(ts)
6. n : ℤ
7. [%3] : 0 < n
8. ∀v:ts-reachable(ts). ((ts-rel(ts)^n - 1 ts-init(ts) v) ⇒ P[v])
9. v : ts-reachable(ts)
10. z : ts-type(ts)
11. 0 < n
12. ts-rel(ts)^n - 1 ts-init(ts) z
13. ts-rel(ts) z v
14. z ∈ ts-reachable(ts)
15. P[z]
⊢ (ts-rel(ts)^*) ts-init(ts) z

---

Latex:

---

Latex:

1.  ts  :  transition-system\{i:l\}
2.  [P]  :  ts-reachable(ts)  {}\mrightarrow{}  \mBbbP{}
3.  P[ts-init(ts)]
4.  \mforall{}x:ts-type(ts)
          (((ts-rel(ts)\^{}*)  ts-init(ts)  x)  {}\mRightarrow{}  (\mforall{}y:ts-reachable(ts).  (P[x]  {}\mRightarrow{}  (ts-rel(ts)  x  y)  {}\mRightarrow{}  P[y])))
5.  x  :  ts-type(ts)
6.  n  :  \mBbbZ{}
7.  [\%3]  :  0  <  n
8.  \mforall{}v:ts-reachable(ts).  ((rel\_exp(ts-type(ts);  ts-rel(ts);  n  -  1)  ts-init(ts)  v)  {}\mRightarrow{}  P[v])
9.  v  :  ts-reachable(ts)
10.  z  :  ts-type(ts)
11.  0  <  n
12.  rel\_exp(ts-type(ts);  ts-rel(ts);  n  -  1)  ts-init(ts)  z
13.  ts-rel(ts)  z  v
14.  z  \mmember{}  ts-reachable(ts)
15.  P[z]
\mvdash{}  P[v]


By

---

Latex:
xxx(InstHyp  [\mkleeneopen{}z\mkleeneclose{}]  4\mcdot{}  THEN  Auto)xxx

---

Home Index