---

Step * of Lemma transitive-reflexive-closure-map

∀[A:Type]. ∀[R:A ⟶ A ⟶ ℙ].
  ∀f:A ⟶ A. ((∀x,y:A.  ((R x y) ⇒ (R (f x) (f y)))) ⇒ (∀x,y:A.  ((R^* x y) ⇒ (R^* (f x) (f y)))))
BY
{ (Auto THEN All (RepUR  ``transitive-reflexive-closure``) THEN ParallelLast THEN Auto) }

1
1. [A] : Type
2. [R] : A ⟶ A ⟶ ℙ
3. f : A ⟶ A
4. ∀x,y:A.  ((R x y) ⇒ (R (f x) (f y)))
5. x : A
6. y : A
7. TC(R) x y
⊢ TC(R) (f x) (f y)

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  All  (RepUR    ``transitive-reflexive-closure``)  THEN  ParallelLast  THEN  Auto)

---

Home Index