---

Step * of Lemma transitive-closure-map

∀[A:Type]. ∀[R:A ⟶ A ⟶ ℙ].
  ∀f:A ⟶ A. ((∀x,y:A.  ((R x y) ⇒ (R (f x) (f y)))) ⇒ (∀x,y:A.  ((TC(R) x y) ⇒ (TC(R) (f x) (f y)))))
BY
{ (Auto THEN RenameVar `L' (-1) THEN All (RepUR  ``transitive-closure``)) }

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. L : {L:(a:A × b:A × (R a b)) List| rel_path(A;L;x;y) ∧ 0 < ||L||} 
⊢ {L:(a:A × b:A × (R a b)) List| rel_path(A;L;f x;f y) ∧ 0 < ||L||} 

---

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.    ((TC(R)  x  y)  {}\mRightarrow{}  (TC(R)  (f  x)  (f  y)))))


By

---

Latex:
(Auto  THEN  RenameVar  `L'  (-1)  THEN  All  (RepUR    ``transitive-closure``))

---

Home Index