---

Step * 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. L : {L:(a:A × b:A × (R a b)) List| rel_path(A;L;x;y) ∧ 0 < ||L||} 
⊢ ∃w:{a:A × b:A × (Q a b)| (((fst(w)) = x ∈ A) ∧ ((fst(snd(w))) = y ∈ A))}
BY
{ (UseWitness ⌜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(L)
               with starting value:
                let a,b,r = hd(L) in 
                <x, b, F x b r>)⌝⋅
   THEN RepeatFor 2 (D -1)
   THEN (D -3
         THENL [(Reduce (-1) THEN Auto)
               ; (Thin (-1) THEN RepeatFor 2 (D -3) THEN RepUR ``rel_path`` -1 THEN Fold `rel_path` (-1))]
   )) }

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

---

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.  L  :  \{L:(a:A  \mtimes{}  b:A  \mtimes{}  (R  a  b))  List|  rel\_path(A;L;x;y)  \mwedge{}  0  <  ||L||\} 
\mvdash{}  \mexists{}w:\{a:A  \mtimes{}  b:A  \mtimes{}  (Q  a  b)|  (((fst(w))  =  x)  \mwedge{}  ((fst(snd(w)))  =  y))\}


By

---

Latex:
(UseWitness  \mkleeneopen{}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(L)
                          with  starting  value:
                            let  a,b,r  =  hd(L)  in 
                            <x,  b,  F  x  b  r>)\mkleeneclose{}\mcdot{}
  THEN  RepeatFor  2  (D  -1)
  THEN  (D  -3
              THENL  [(Reduce  (-1)  THEN  Auto)
                          ;  (Thin  (-1)
                                THEN  RepeatFor  2  (D  -3)
                                THEN  RepUR  ``rel\_path``  -1
                                THEN  Fold  `rel\_path`  (-1))]
  ))

---

Home Index