---

Step * 1 1 1 of Lemma ts-transitive-stable


1. ts : transition-system{i:l}@i'
2. [R] : ts-type(ts) ⟶ ts-type(ts) ⟶ ℙ
3. Refl(ts-type(ts);x,y.R[x;y])@i
4. Trans(ts-type(ts);x,y.R[x;y])@i
5. ts-rel(ts) => λx,y. R[x;y]@i
6. x : ts-type(ts)@i
7. y : ts-type(ts)@i
8. x (ts-rel(ts)^*) y@i
9. y1 : ts-type(ts)@i
10. y@0 : ts-type(ts)@i
11. R[x;y1]@i
12. y1 ts-rel(ts) y@0@i
⊢ R[x;y@0]
BY
{ (RepUR ``rel_implies`` 5 THEN Auto) }

---

Latex:

---

Latex:

1.  ts  :  transition-system\{i:l\}@i'
2.  [R]  :  ts-type(ts)  {}\mrightarrow{}  ts-type(ts)  {}\mrightarrow{}  \mBbbP{}
3.  Refl(ts-type(ts);x,y.R[x;y])@i
4.  Trans(ts-type(ts);x,y.R[x;y])@i
5.  ts-rel(ts)  =>  \mlambda{}x,y.  R[x;y]@i
6.  x  :  ts-type(ts)@i
7.  y  :  ts-type(ts)@i
8.  x  rel\_star(ts-type(ts);  ts-rel(ts))  y@i
9.  y1  :  ts-type(ts)@i
10.  y@0  :  ts-type(ts)@i
11.  R[x;y1]@i
12.  y1  ts-rel(ts)  y@0@i
\mvdash{}  R[x;y@0]


By

---

Latex:
(RepUR  ``rel\_implies``  5  THEN  Auto)

---

Home Index