---

Step * of Lemma rel-exp-add-1-iff

∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  ∀a:ℕ+. ∀x,z:T.  (x R^a z ⇐⇒ ∃y:T. ((x R^a - 1 y) ∧ (y R z)))
BY
{ Auto }

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

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

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].
    \mforall{}a:\mBbbN{}\msupplus{}.  \mforall{}x,z:T.    (x  R\^{}a  z  \mLeftarrow{}{}\mRightarrow{}  \mexists{}y:T.  ((x  R\^{}a  -  1  y)  \mwedge{}  (y  R  z)))


By

---

Latex:
Auto

---

Home Index