---

Step * of Lemma rel_star_iff2

∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  ∀x,y:T.  (x (R^*) y ⇐⇒ (∃z:T. ((x R z) ∧ (z (R^*) y))) ∨ (x = y ∈ T))
BY
{ (Unfold `rel_star` 0 THEN Reduce 0 THEN Auto THEN SplitOrHyps THEN ExRepD) }

1
1. [T] : Type
2. [R] : T ⟶ T ⟶ ℙ
3. x : T@i
4. y : T@i
5. n : ℕ@i
6. x R^n y@i
⊢ (∃z:T. ((x R z) ∧ (∃n:ℕ. (z R^n y)))) ∨ (x = y ∈ T)

2
1. [T] : Type
2. [R] : T ⟶ T ⟶ ℙ
3. x : T@i
4. y : T@i
5. z : T@i
6. x R z@i
7. n : ℕ@i
8. z R^n y@i
⊢ ∃n:ℕ. (x R^n y)

3
1. [T] : Type
2. [R] : T ⟶ T ⟶ ℙ
3. x : T@i
4. y : T@i
5. x = y ∈ T@i
⊢ ∃n:ℕ. (x R^n y)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].
    \mforall{}x,y:T.    (x  (R\^{}*)  y  \mLeftarrow{}{}\mRightarrow{}  (\mexists{}z:T.  ((x  R  z)  \mwedge{}  (z  (R\^{}*)  y)))  \mvee{}  (x  =  y))


By

---

Latex:
(Unfold  `rel\_star`  0  THEN  Reduce  0  THEN  Auto  THEN  SplitOrHyps  THEN  ExRepD)

---

Home Index