---

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

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

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
⊢ (∃n:ℕ+. (x R^n y)) ∨ (x = y ∈ T)

---

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\_plus  rel\_star``  0  THEN  Reduce  0)
  THEN  Auto
  THEN  SplitOrHyps
  THEN  ExRepD
  THEN  Auto
  THEN  Try  ((With  \mkleeneopen{}0\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto)))

---

Home Index