---

Step * 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. x : A
7. y : A
8. L : {L:(a:A × b:A × (R a b)) List| rel_path(A;L;x;y) ∧ 0 < ||L||} 
⊢ x Q y
BY
{ (UseWitness ⌜accumulate (with value q and list item y):
                let b,c,r = y in 
                g q (F b c r)
               over list:
                 tl(L)
               with starting value:
                let a,b,r = hd(L) in 
                F a b r)⌝⋅
   THEN RepeatFor 2 (D -1)
   THEN (D -3 THENL [(Assert ⌜False⌝⋅ THEN Auto); Thin (-1)])
   THEN RepeatFor 2 (D -3)
   THEN RepUR ``rel_path`` -1
   THEN Fold `rel_path` (-1)
   THEN Reduce 0
   THEN SubsumeC ⌜a Q y⌝⋅
   THEN Try ((BLemma `subtype_rel-equal` THEN Auto))
   THEN D (-1)
   THEN ThinVar `x') }

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

---

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{}  x  Q  y


By

---

Latex:
(UseWitness  \mkleeneopen{}accumulate  (with  value  q  and  list  item  y):
                            let  b,c,r  =  y  in 
                            g  q  (F  b  c  r)
                          over  list:
                              tl(L)
                          with  starting  value:
                            let  a,b,r  =  hd(L)  in 
                            F  a  b  r)\mkleeneclose{}\mcdot{}
  THEN  RepeatFor  2  (D  -1)
  THEN  (D  -3  THENL  [(Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}  THEN  Auto);  Thin  (-1)])
  THEN  RepeatFor  2  (D  -3)
  THEN  RepUR  ``rel\_path``  -1
  THEN  Fold  `rel\_path`  (-1)
  THEN  Reduce  0
  THEN  SubsumeC  \mkleeneopen{}a  Q  y\mkleeneclose{}\mcdot{}
  THEN  Try  ((BLemma  `subtype\_rel-equal`  THEN  Auto))
  THEN  D  (-1)
  THEN  ThinVar  `x')

---

Home Index