---

Step * 1 1 1 2 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. 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
17. v1 : a Q b
18. (F a b u2) = v1 ∈ (a Q b)
⊢ g q v1 ∈ a@0 Q b
BY
{ (RevHypSubst (-5) (-3) THENA 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 a
17. v1 : a Q b
18. (F a b u2) = v1 ∈ (a Q b)
⊢ g q v1 ∈ 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
15.  rel\_path(A;v;b;y)
16.  q  :  a@0  Q  b@0
17.  v1  :  a  Q  b
18.  (F  a  b  u2)  =  v1
\mvdash{}  g  q  v1  \mmember{}  a@0  Q  b


By

---

Latex:
(RevHypSubst  (-5)  (-3)  THENA  Auto)

---

Home Index