---

Step * of Lemma transitive-closure-minimal-uniform

∀[A:Type]. ∀[R,Q:A ⟶ A ⟶ ℙ].  (R => Q ⇒ UniformlyTrans(A;x,y.x Q y) ⇒ TC(R) => Q)
BY
{ (Auto
   THEN RepUR ``rel_implies all implies`` -2
   THEN RenameVar `F' (-2)
   THEN Unfold `utrans` -1
   THEN D 0
   THEN Auto
   THEN RepUR ``transitive-closure`` -1
   THEN RenameVar `g' 5
   THEN RenameVar `L' (-1)) }

1
1. [A] : Type
2. [R] : A ⟶ A ⟶ ℙ
3. [Q] : A ⟶ A ⟶ ℙ
4. F : x:A ⟶ y:A ⟶ (x R y) ⟶ (x Q y)
5. g : ∀[a,b,c:A].  ((a Q b) ⇒ (b Q c) ⇒ (a Q c))
6. x : A
7. y : A
8. L : {L:(a:A × b:A × (R a b)) List| rel_path(A;L;x;y) ∧ 0 < ||L||} 
⊢ x Q y

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[R,Q:A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}].    (R  =>  Q  {}\mRightarrow{}  UniformlyTrans(A;x,y.x  Q  y)  {}\mRightarrow{}  TC(R)  =>  Q)


By

---

Latex:
(Auto
  THEN  RepUR  ``rel\_implies  all  implies``  -2
  THEN  RenameVar  `F'  (-2)
  THEN  Unfold  `utrans`  -1
  THEN  D  0
  THEN  Auto
  THEN  RepUR  ``transitive-closure``  -1
  THEN  RenameVar  `g'  5
  THEN  RenameVar  `L'  (-1))

---

Home Index