---

Step * of Lemma rel_star_trans

∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  ∀x,y,z:T.  ((x R y) ⇒ (y (R^*) z) ⇒ (x (R^*) z))
BY
{ ((((Auto THEN InstLemma `rel_star_transitivity` [T;R;x;y;z]) THEN Auto) THEN BackThruLemma `rel_rel_star`)
   THEN Auto
   ) }

---

Latex:

---

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


By

---

Latex:
((((Auto  THEN  InstLemma  `rel\_star\_transitivity`  [T;R;x;y;z])  THEN  Auto)
    THEN  BackThruLemma  `rel\_rel\_star`
    )
  THEN  Auto
  )

---

Home Index