---

Step * 1 1 1 1 1 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. g : ∀a,b,c:A.  ((a Q b) ⇒ (b Q c) ⇒ (a Q c))
6. x : A
7. y : A
8. b : A
9. b = y ∈ A
10. q : x Q b
⊢ <x, b, q> ∈ {w:a:A × b:A × (Q a b)| ((fst(w)) = x ∈ A) ∧ ((fst(snd(w))) = y ∈ A)} 
BY
{ (MemTypeCD THEN Reduce 0 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.  g  :  \mforall{}a,b,c:A.    ((a  Q  b)  {}\mRightarrow{}  (b  Q  c)  {}\mRightarrow{}  (a  Q  c))
6.  x  :  A
7.  y  :  A
8.  b  :  A
9.  b  =  y
10.  q  :  x  Q  b
\mvdash{}  <x,  b,  q>  \mmember{}  \{w:a:A  \mtimes{}  b:A  \mtimes{}  (Q  a  b)|  ((fst(w))  =  x)  \mwedge{}  ((fst(snd(w)))  =  y)\} 


By

---

Latex:
(MemTypeCD  THEN  Reduce  0  THEN  Auto)

---

Home Index