---

Step * 1 1 1 of Lemma transitive-closure-minimal-uniform


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
⊢ ∀y,a,b:A.
    (rel_path(A;v;b;y)
    ⇒ (∀q:a Q b
          (accumulate (with value q and list item y):
            let b,c,r = y in 
            g q (F b c r)
           over list:
             v
           with starting value:
            q) ∈ a Q y)))
BY
{ (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. y : A
7. a : A
8. b : A
9. b = y ∈ A
10. q : a Q b
⊢ q ∈ a Q y

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. g : ∀[a,b,c:A].  ((a Q b) ⇒ (b Q c) ⇒ (a Q c))
6. a : A
7. b : A
8. u2 : R a b
9. v : (a:A × b:A × (R a b)) List
10. ∀y,a,b:A.
      (rel_path(A;v;b;y)
      ⇒ (∀q:a Q b
            (accumulate (with value q and list item y):
              let b,c,r = y in 
              g q (F b c r)
             over list:
               v
             with starting value:
              q) ∈ a Q y)))
11. y : A
12. a@0 : A
13. b@0 : A
14. (a = b@0 ∈ A) ∧ rel_path(A;v;b;y)
15. q : a@0 Q b@0
⊢ accumulate (with value q and list item y):
   let b,c,r = y in 
   g q (F b c r)
  over list:
    v
  with starting value:
   g q (F a b u2)) ∈ a@0 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.  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{}y,a,b:A.
        (rel\_path(A;v;b;y)
        {}\mRightarrow{}  (\mforall{}q:a  Q  b
                    (accumulate  (with  value  q  and  list  item  y):
                        let  b,c,r  =  y  in 
                        g  q  (F  b  c  r)
                      over  list:
                          v
                      with  starting  value:
                        q)  \mmember{}  a  Q  y)))


By

---

Latex:
(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