---

Step * of Lemma rel_plus_iff

∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  ∀x,z:T.  (x R+ z ⇐⇒ ∃y:T. ((x (R^*) y) ∧ (y R z)))
BY
{ (Auto THEN ExRepD) }

1
1. [T] : Type
2. [R] : T ⟶ T ⟶ ℙ
3. x : T@i
4. z : T@i
5. x R+ z@i
⊢ ∃y:T. ((x (R^*) y) ∧ (y R z))

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

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].    \mforall{}x,z:T.    (x  R\msupplus{}  z  \mLeftarrow{}{}\mRightarrow{}  \mexists{}y:T.  ((x  rel\_star(T;  R)  y)  \mwedge{}  (y  R  z)))


By

---

Latex:
(Auto  THEN  ExRepD)

---

Home Index