---

Step * of Lemma rel-plus-rel-star

∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  ∀x,y:T.  ((x R+ y) ⇒ (x (R^*) y))
BY
{ (Unfolds ``rel_plus rel_star`` 0 THEN Reduce 0 THEN Auto THEN (ParallelOp (-1)) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].    \mforall{}x,y:T.    ((x  R\msupplus{}  y)  {}\mRightarrow{}  (x  rel\_star(T;  R)  y))


By

---

Latex:
(Unfolds  ``rel\_plus  rel\_star``  0  THEN  Reduce  0  THEN  Auto  THEN  (ParallelOp  (-1))  THEN  Auto)

---

Home Index