---

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

.....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))))
BY
{ (InductionOnNat THEN Auto') }

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

2
1. [T] : Type
2. [R] : T ⟶ T ⟶ ℙ
3. a : ℤ
4. [%1] : 0 < a
5. ∀b:ℕ. ∀x,z:T.  ((x R^(a - 1) + b z) ⇒ (∃y:T. ((x R^a - 1 y) ∧ (y R^b z))))
6. b : ℕ
7. x : T
8. z : T
9. x R^a + b z
⊢ ∃y:T. ((x R^a y) ∧ (y R^b z))

---

Latex:

---

Latex:
.....assertion..... 
\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))))


By

---

Latex:
(InductionOnNat  THEN  Auto')

---

Home Index