---

Step * 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. x : A
7. y : A
8. a : A
9. b : A
10. u2 : R a b
11. v : (a:A × b:A × (R a b)) List
12. (a = x ∈ A) ∧ rel_path(A;v;b;y)
⊢ 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:
    tl([<a, b, u2> / v])
  with starting value:
   let a,b,r = hd([<a, b, u2> / v]) in 
   <x, b, F x b r>) ∈ ∃w:{a:A × b:A × (Q a b)| (((fst(w)) = x ∈ A) ∧ ((fst(snd(w))) = y ∈ A))}
BY
{ (D -1
   THEN (HypSubst (-2) (-4) THENA Auto)
   THEN Reduce 0
   THEN (ThinVar `a'
         THEN GenConclAtAddr [2;2;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
⊢ ∀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))})))

---

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.  x  :  A
7.  y  :  A
8.  a  :  A
9.  b  :  A
10.  u2  :  R  a  b
11.  v  :  (a:A  \mtimes{}  b:A  \mtimes{}  (R  a  b))  List
12.  (a  =  x)  \mwedge{}  rel\_path(A;v;b;y)
\mvdash{}  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:
        tl([<a,  b,  u2>  /  v])
    with  starting  value:
      let  a,b,r  =  hd([<a,  b,  u2>  /  v])  in 
      <x,  b,  F  x  b  r>)  \mmember{}  \mexists{}w:\{a:A  \mtimes{}  b:A  \mtimes{}  (Q  a  b)|  (((fst(w))  =  x)  \mwedge{}  ((fst(snd(w)))  =  y))\}


By

---

Latex:
(D  -1
  THEN  (HypSubst  (-2)  (-4)  THENA  Auto)
  THEN  Reduce  0
  THEN  (ThinVar  `a'
              THEN  GenConclAtAddr  [2;2;2;2]
              THEN  Thin  (-1)
              THEN  RenameVar  `q'  (-1)
              THEN  ThinVar  `u2'
              THEN  (RepeatFor  2  (MoveToConcl  (-1))  THEN  RepeatFor  3  (MoveToConcl  (-2)))\mcdot{})\mcdot{})\mcdot{}

---

Home Index