---

Step * 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
⊢ R[x;y]
BY
{ Assert ⌜ts-stable(ts;y.R[x;y])⌝⋅ }

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

2
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. ts-stable(ts;y.R[x;y])
⊢ R[x;y]

---

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
\mvdash{}  R[x;y]


By

---

Latex:
Assert  \mkleeneopen{}ts-stable(ts;y.R[x;y])\mkleeneclose{}\mcdot{}

---

Home Index