---

Step * 1 of Lemma transitive-closure-transitive


1. [A] : Type
2. [R] : A ⟶ A ⟶ ℙ
3. [a] : A
4. [b] : A
5. [c] : A
6. p : (a:A × b:A × (R a b)) List
7. [%2] : rel_path(A;p;a;b) ∧ 0 < ||p||
8. q : (a:A × b:A × (R a b)) List
9. [%3] : rel_path(A;q;b;c) ∧ 0 < ||q||
⊢ {L:(a:A × b:A × (R a b)) List| rel_path(A;L;a;c) ∧ 0 < ||L||} 
BY
{ (UseWitness ⌜p @ q⌝⋅
   THEN MemTypeCD
   THEN Auto'
   THEN Thin (-1)
   THEN Thin (-3)
   THEN (RepeatFor 3 (MoveToConcl (-1))
         THEN RepeatFor 3 (MoveToConcl (-2))
         THEN ListInd (-1)
         THEN Reduce 0
         THEN (Unfold `rel_path` 0 THEN Reduce 0 THEN Fold `rel_path` 0 THEN Auto)⋅)⋅) }

---

Latex:

---

Latex:

1.  [A]  :  Type
2.  [R]  :  A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}
3.  [a]  :  A
4.  [b]  :  A
5.  [c]  :  A
6.  p  :  (a:A  \mtimes{}  b:A  \mtimes{}  (R  a  b))  List
7.  [\%2]  :  rel\_path(A;p;a;b)  \mwedge{}  0  <  ||p||
8.  q  :  (a:A  \mtimes{}  b:A  \mtimes{}  (R  a  b))  List
9.  [\%3]  :  rel\_path(A;q;b;c)  \mwedge{}  0  <  ||q||
\mvdash{}  \{L:(a:A  \mtimes{}  b:A  \mtimes{}  (R  a  b))  List|  rel\_path(A;L;a;c)  \mwedge{}  0  <  ||L||\} 


By

---

Latex:
(UseWitness  \mkleeneopen{}p  @  q\mkleeneclose{}\mcdot{}
  THEN  MemTypeCD
  THEN  Auto'
  THEN  Thin  (-1)
  THEN  Thin  (-3)
  THEN  (RepeatFor  3  (MoveToConcl  (-1))
              THEN  RepeatFor  3  (MoveToConcl  (-2))
              THEN  ListInd  (-1)
              THEN  Reduce  0
              THEN  (Unfold  `rel\_path`  0  THEN  Reduce  0  THEN  Fold  `rel\_path`  0  THEN  Auto)\mcdot{})\mcdot{})

---

Home Index