---

Step * 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. y : A
7. a : A
8. b : A
9. u2 : R a b
10. v : (a:A × b:A × (R a b)) List
11. rel_path(A;v;b;y)
⊢ 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:
   F a b u2) ∈ a Q y
BY
{ (GenConclAtAddr [2;2]
   THEN Thin (-1)
   THEN RenameVar `q' (-1)
   THEN ThinVar `u2'
   THEN (RepeatFor 2 (MoveToConcl (-1)) THEN RepeatFor 3 (MoveToConcl (-2)))⋅)⋅ }

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

---

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.  y  :  A
7.  a  :  A
8.  b  :  A
9.  u2  :  R  a  b
10.  v  :  (a:A  \mtimes{}  b:A  \mtimes{}  (R  a  b))  List
11.  rel\_path(A;v;b;y)
\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:
      F  a  b  u2)  \mmember{}  a  Q  y


By

---

Latex:
(GenConclAtAddr  [2;2]
  THEN  Thin  (-1)
  THEN  RenameVar  `q'  (-1)
  THEN  ThinVar  `u2'
  THEN  (RepeatFor  2  (MoveToConcl  (-1))  THEN  RepeatFor  3  (MoveToConcl  (-2)))\mcdot{})\mcdot{}

---

Home Index