---

Step * 1 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||} 
⊢ x Q y
BY
{ Assert ⌜∃w:{a:A × b:A × (Q a b)| (((fst(w)) = x ∈ A) ∧ ((fst(snd(w))) = y ∈ A))}⌝⋅ }

1
.....assertion..... 
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||} 
⊢ ∃w:{a:A × b:A × (Q a b)| (((fst(w)) = x ∈ A) ∧ ((fst(snd(w))) = y ∈ A))}

2
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

---

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||\} 
\mvdash{}  x  Q  y


By

---

Latex:
Assert  \mkleeneopen{}\mexists{}w:\{a:A  \mtimes{}  b:A  \mtimes{}  (Q  a  b)|  (((fst(w))  =  x)  \mwedge{}  ((fst(snd(w)))  =  y))\}\mkleeneclose{}\mcdot{}

---

Home Index