---

Step * 1 1 1 of Lemma ts-reachable-induction


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

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

---

Latex:

---

Latex:

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


By

---

Latex:
xxx(Assert  \mkleeneopen{}z  \mmember{}  ts-reachable(ts)\mkleeneclose{}\mcdot{}  THEN  Auto)xxx

---

Home Index