---

Step * 1 1 of Lemma ts-transitive-stable

.....assertion..... 
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
⊢ ts-stable(ts;y.R[x;y])
BY
{ (D 0 THEN Auto) }

1
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]

---

Latex:

---

Latex:
.....assertion..... 
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
\mvdash{}  ts-stable(ts;y.R[x;y])


By

---

Latex:
(D  0  THEN  Auto)

---

Home Index