---

Step * 1 2 of Lemma transitive-closure-minimal


1. [A] : Type
2. [R] : A ⟶ A ⟶ ℙ
3. [Q] : A ⟶ A ⟶ ℙ
4. F : x:A ⟶ y:A ⟶ (x R y) ⟶ (x Q y)
5. ∀a,b,c:A.  ((a Q b) ⇒ (b Q c) ⇒ (a Q c))
6. x : A
7. y : A
8. {L:(a:A × b:A × (R a b)) List| rel_path(A;L;x;y) ∧ 0 < ||L||} 
9. ∃w:{a:A × b:A × (Q a b)| (((fst(w)) = x ∈ A) ∧ ((fst(snd(w))) = y ∈ A))}
⊢ x Q y
BY
{ (D (-1) THEN RepeatFor 2 (D -2) THEN Reduce (-1) THEN All (Fold `infix_ap`) THEN Auto) }

---

Latex:

---

Latex:

1.  [A]  :  Type
2.  [R]  :  A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}
3.  [Q]  :  A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}
4.  F  :  x:A  {}\mrightarrow{}  y:A  {}\mrightarrow{}  (x  R  y)  {}\mrightarrow{}  (x  Q  y)
5.  \mforall{}a,b,c:A.    ((a  Q  b)  {}\mRightarrow{}  (b  Q  c)  {}\mRightarrow{}  (a  Q  c))
6.  x  :  A
7.  y  :  A
8.  \{L:(a:A  \mtimes{}  b:A  \mtimes{}  (R  a  b))  List|  rel\_path(A;L;x;y)  \mwedge{}  0  <  ||L||\} 
9.  \mexists{}w:\{a:A  \mtimes{}  b:A  \mtimes{}  (Q  a  b)|  (((fst(w))  =  x)  \mwedge{}  ((fst(snd(w)))  =  y))\}
\mvdash{}  x  Q  y


By

---

Latex:
(D  (-1)  THEN  RepeatFor  2  (D  -2)  THEN  Reduce  (-1)  THEN  All  (Fold  `infix\_ap`)  THEN  Auto)

---

Home Index