---

Step * 1 1 1 2 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. 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
BY
{ (InstHyp [⌜y⌝;⌜a@0⌝;⌜b⌝;⌜g q (F a b u2)⌝] (-6)⋅ 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. 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
15. rel_path(A;v;b;y)
16. q : a@0 Q b@0
⊢ g q (F a b u2) ∈ a@0 Q b

---

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.  a  :  A
7.  b  :  A
8.  u2  :  R  a  b
9.  v  :  (a:A  \mtimes{}  b:A  \mtimes{}  (R  a  b))  List
10.  \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)))
11.  y  :  A
12.  a@0  :  A
13.  b@0  :  A
14.  (a  =  b@0)  \mwedge{}  rel\_path(A;v;b;y)
15.  q  :  a@0  Q  b@0
\mvdash{}  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))  \mmember{}  a@0  Q  y


By

---

Latex:
(InstHyp  [\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}a@0\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}g  q  (F  a  b  u2)\mkleeneclose{}]  (-6)\mcdot{}  THEN  Auto)

---

Home Index