---

Step * of Lemma transitive-reflexive-closure_transitivity

∀[A:Type]. ∀[R:A ⟶ A ⟶ ℙ].  ∀x,y,z:A.  ((x R^* y) ⇒ (y R^* z) ⇒ (x R^* z))
BY
{ (Auto
   THEN DupHyp (-2)
   THEN RepUR ``transitive-reflexive-closure`` -1
   THEN D -1
   THEN Try ((RWO "-1" 0 THEN Auto))
   THEN RepUR ``transitive-reflexive-closure`` -2
   THEN D -2
   THEN Try ((RWO "-2<" 0 THEN Auto))) }

1
1. [A] : Type
2. [R] : A ⟶ A ⟶ ℙ
3. x : A
4. y : A
5. z : A
6. x R^* y
7. TC(R) y z
8. TC(R) x y
⊢ x R^* z

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[R:A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}].    \mforall{}x,y,z:A.    ((x  R\^{}*  y)  {}\mRightarrow{}  (y  R\^{}*  z)  {}\mRightarrow{}  (x  R\^{}*  z))


By

---

Latex:
(Auto
  THEN  DupHyp  (-2)
  THEN  RepUR  ``transitive-reflexive-closure``  -1
  THEN  D  -1
  THEN  Try  ((RWO  "-1"  0  THEN  Auto))
  THEN  RepUR  ``transitive-reflexive-closure``  -2
  THEN  D  -2
  THEN  Try  ((RWO  "-2<"  0  THEN  Auto)))

---

Home Index