---

Step * 1 2 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. ts-stable(ts;y.R[x;y])
⊢ R[x;y]
BY
{ (InstLemma `ts-stable-star` [⌜ts⌝;⌜λ2y.R[x;y]⌝;⌜x⌝;⌜y⌝]⋅ 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.  ts-stable(ts;y.R[x;y])
\mvdash{}  R[x;y]


By

---

Latex:
(InstLemma  `ts-stable-star`  [\mkleeneopen{}ts\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}y.R[x;y]\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index