---

Step * of Lemma rel_exp-iff-path

∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].
  ∀n:ℕ. ∀x,y:T.  (x R^n y ⇐⇒ ∃L:T List. ((||L|| = (n + 1) ∈ ℤ) ∧ rel-path-between(T;R;x;y;L)))
BY
{ TACTIC:(InductionOnNat THEN RecUnfold `rel_exp` 0 THEN Reduce 0) }

1
1. [T] : Type
2. [R] : T ⟶ T ⟶ ℙ
⊢ ∀x,y:T.  (x = y ∈ T ⇐⇒ ∃L:T List. ((||L|| = 1 ∈ ℤ) ∧ rel-path-between(T;R;x;y;L)))

2
1. [T] : Type
2. [R] : T ⟶ T ⟶ ℙ
3. n : ℤ
4. [%1] : 0 < n
5. ∀x,y:T.  (x R^n - 1 y ⇐⇒ ∃L:T List. ((||L|| = ((n - 1) + 1) ∈ ℤ) ∧ rel-path-between(T;R;x;y;L)))
⊢ ∀x,y:T.
    (x if (n =z 0) then λx,y. (x = y ∈ T) else λx,y. ∃z:T. ((x R z) ∧ (z R^n - 1 y)) fi  y
    ⇐⇒ ∃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{}n:\mBbbN{}.  \mforall{}x,y:T.    (x  R\^{}n  y  \mLeftarrow{}{}\mRightarrow{}  \mexists{}L:T  List.  ((||L||  =  (n  +  1))  \mwedge{}  rel-path-between(T;R;x;y;L)))


By

---

Latex:
TACTIC:(InductionOnNat  THEN  RecUnfold  `rel\_exp`  0  THEN  Reduce  0)

---

Home Index