---

Step * of Lemma rel-star-iff-rel-plus-or

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

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

2
1. [T] : Type
2. [R] : T ⟶ T ⟶ ℙ
3. x : T@i
4. y : T@i
5. ∃n:ℕ+. (x 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  rel\_star(T;  R)  y  \mLeftarrow{}{}\mRightarrow{}  (x  R\msupplus{}  y)  \mvee{}  (x  =  y))


By

---

Latex:
(Unfolds  ``rel\_star  rel\_plus``  0  THEN  Reduce  0  THEN  Auto  THEN  SplitOrHyps)

---

Home Index