---

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


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)))
BY
{ (RepeatFor 6 (ParallelLast) THEN D 0 THEN Try (Trivial) THEN Auto) }

1
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))))
2. [T] : Type
3. ∀[R:T ⟶ T ⟶ ℙ]. ∀a,b:ℕ. ∀x,z:T.  ((x R^a + b z) ⇒ (∃y:T. ((x R^a y) ∧ (y R^b z))))
4. [R] : T ⟶ T ⟶ ℙ
5. ∀a,b:ℕ. ∀x,z:T.  ((x R^a + b z) ⇒ (∃y:T. ((x R^a y) ∧ (y R^b z))))
6. a : ℕ
7. ∀b:ℕ. ∀x,z:T.  ((x R^a + b z) ⇒ (∃y:T. ((x R^a y) ∧ (y R^b z))))
8. b : ℕ
9. ∀x,z:T.  ((x R^a + b z) ⇒ (∃y:T. ((x R^a y) ∧ (y R^b z))))
10. x : T
11. ∀z:T. ((x R^a + b z) ⇒ (∃y:T. ((x R^a y) ∧ (y R^b z))))
12. z : T
13. (x R^a + b z) ⇒ (∃y:T. ((x R^a y) ∧ (y R^b z)))
14. ∃y:T. ((x R^a y) ∧ (y R^b z))
⊢ x R^a + b z

---

Latex:

---

Latex:

1.  \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))))
\mvdash{}  \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:
(RepeatFor  6  (ParallelLast)  THEN  D  0  THEN  Try  (Trivial)  THEN  Auto)

---

Home Index