---

Step * of Lemma rel-exp-add-iff

∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  ∀a,b:ℕ. ∀x,z:T.  (x R^a + b z ⇐⇒ ∃y:T. ((x R^a y) ∧ (y R^b z)))
BY
{ Assert ⌜∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  ∀a,b:ℕ. ∀x,z:T.  ((x R^a + b z) ⇒ (∃y:T. ((x R^a y) ∧ (y R^b z))))⌝⋅ }

1
.....assertion..... 
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  ∀a,b:ℕ. ∀x,z:T.  ((x R^a + b z) ⇒ (∃y:T. ((x R^a y) ∧ (y R^b z))))

2
1. ∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  ∀a,b:ℕ. ∀x,z:T.  ((x R^a + b z) ⇒ (∃y:T. ((x R^a y) ∧ (y R^b z))))
⊢ ∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  ∀a,b:ℕ. ∀x,z:T.  (x R^a + b z ⇐⇒ ∃y:T. ((x R^a y) ∧ (y R^b z)))

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].
    \mforall{}a,b:\mBbbN{}.  \mforall{}x,z:T.    (x  R\^{}a  +  b  z  \mLeftarrow{}{}\mRightarrow{}  \mexists{}y:T.  ((x  R\^{}a  y)  \mwedge{}  (y  rel\_exp(T;  R;  b)  z)))


By

---

Latex:
Assert  \mkleeneopen{}\mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].
                    \mforall{}a,b:\mBbbN{}.  \mforall{}x,z:T.    ((x  R\^{}a  +  b  z)  {}\mRightarrow{}  (\mexists{}y:T.  ((x  R\^{}a  y)  \mwedge{}  (y  rel\_exp(T;  R;  b)  z))))\mkleeneclose{}\mcdot{}

---

Home Index