---

Step * 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. v : (a:A × b:A × (R a b)) List
⊢ ∀x,y,b:A.
    (rel_path(A;v;b;y)
    ⇒ (∀q:x Q b
          (accumulate (with value x and list item y):
            let a,b,q1 = x in 
            let b',c,r = y in 
            <a, c, g a b c q1 (F b c r)>
           over list:
             v
           with starting value:
            <x, b, q>) ∈ ∃w:{a:A × b:A × (Q a b)| (((fst(w)) = x ∈ A) ∧ ((fst(snd(w))) = y ∈ A))})))
BY
{ (Unfold `sq_exists` 0
   THEN ListInd (-1)
   THEN Try (RepeatFor 2 (D (-3)))
   THEN RepUR ``rel_path`` 0⋅
   THEN Try (Fold `rel_path` 0)
   THEN (UnivCD THENA Auto)
   THEN Try ((BackThruSomeHyp THEN Auto)))⋅ }

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. 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)} 

---

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.  v  :  (a:A  \mtimes{}  b:A  \mtimes{}  (R  a  b))  List
\mvdash{}  \mforall{}x,y,b:A.
        (rel\_path(A;v;b;y)
        {}\mRightarrow{}  (\mforall{}q:x  Q  b
                    (accumulate  (with  value  x  and  list  item  y):
                        let  a,b,q1  =  x  in 
                        let  b',c,r  =  y  in 
                        <a,  c,  g  a  b  c  q1  (F  b  c  r)>
                      over  list:
                          v
                      with  starting  value:
                        <x,  b,  q>)  \mmember{}  \mexists{}w:\{a:A  \mtimes{}  b:A  \mtimes{}  (Q  a  b)|  (((fst(w))  =  x)  \mwedge{}  ((fst(snd(w)))  =  y))\})))


By

---

Latex:
(Unfold  `sq\_exists`  0
  THEN  ListInd  (-1)
  THEN  Try  (RepeatFor  2  (D  (-3)))
  THEN  RepUR  ``rel\_path``  0\mcdot{}
  THEN  Try  (Fold  `rel\_path`  0)
  THEN  (UnivCD  THENA  Auto)
  THEN  Try  ((BackThruSomeHyp  THEN  Auto)))\mcdot{}

---

Home Index