---

Step * of Lemma rel_plus-iff-path

∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  ∀x,y:T.  (x R+ y ⇐⇒ ∃L:T List. (1 < ||L|| ∧ rel-path-between(T;R;x;y;L)))
BY
{ (Intros
   THEN Unfold `rel_plus` 0
   THEN Reduce 0
   THEN (RWO "rel_exp-iff-path" 0 THEN Auto)
   THEN ExRepD
   THEN Auto
   THEN InstConcl [⌜||L|| - 1⌝;⌜L⌝]⋅
   THEN Auto') }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].
    \mforall{}x,y:T.    (x  R\msupplus{}  y  \mLeftarrow{}{}\mRightarrow{}  \mexists{}L:T  List.  (1  <  ||L||  \mwedge{}  rel-path-between(T;R;x;y;L)))


By

---

Latex:
(Intros
  THEN  Unfold  `rel\_plus`  0
  THEN  Reduce  0
  THEN  (RWO  "rel\_exp-iff-path"  0  THEN  Auto)
  THEN  ExRepD
  THEN  Auto
  THEN  InstConcl  [\mkleeneopen{}||L||  -  1\mkleeneclose{};\mkleeneopen{}L\mkleeneclose{}]\mcdot{}
  THEN  Auto')

---

Home Index