---

Step * of Lemma ts-transitive-stable

∀ts:transition-system{i:l}
  ∀[R:ts-type(ts) ⟶ ts-type(ts) ⟶ ℙ]
    (Refl(ts-type(ts);x,y.R[x;y])
    ⇒ Trans(ts-type(ts);x,y.R[x;y])
    ⇒ ts-rel(ts) => λx,y. R[x;y]
    ⇒ ts-stable-rel(ts;x,y.R[x;y]))
BY
{ (Auto THEN 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
⊢ R[x;y]

---

Latex:

---

Latex:
\mforall{}ts:transition-system\{i:l\}
    \mforall{}[R:ts-type(ts)  {}\mrightarrow{}  ts-type(ts)  {}\mrightarrow{}  \mBbbP{}]
        (Refl(ts-type(ts);x,y.R[x;y])
        {}\mRightarrow{}  Trans(ts-type(ts);x,y.R[x;y])
        {}\mRightarrow{}  ts-rel(ts)  =>  \mlambda{}x,y.  R[x;y]
        {}\mRightarrow{}  ts-stable-rel(ts;x,y.R[x;y]))


By

---

Latex:
(Auto  THEN  D  0  THEN  Auto)

---

Home Index