---

Step * of Lemma rel_star-iff-path

∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  ∀x,y:T.  (x (R^*) y ⇐⇒ ∃L:T List. rel-path-between(T;R;x;y;L))
BY
{ TACTIC:(Intros
          THEN Unfold `rel_star` 0
          THEN Reduce 0
          THEN (RWO "rel_exp-iff-path" 0 THEN Auto)
          THEN ExRepD
          THEN Auto) }

1
1. [T] : Type
2. [R] : T ⟶ T ⟶ ℙ
3. x : T
4. y : T
5. L : T List
6. rel-path-between(T;R;x;y;L)
⊢ ∃n:ℕ. ∃L:T List. ((||L|| = (n + 1) ∈ ℤ) ∧ rel-path-between(T;R;x;y;L))

---

Latex:

---

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


By

---

Latex:
TACTIC:(Intros
                THEN  Unfold  `rel\_star`  0
                THEN  Reduce  0
                THEN  (RWO  "rel\_exp-iff-path"  0  THEN  Auto)
                THEN  ExRepD
                THEN  Auto)

---

Home Index