---

Step * 2 1 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))))
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
BY
{ (ExRepD THEN Using [`y',⌜y⌝] (BLemma `rel_exp_add`)⋅ THEN Auto)⋅ }

---

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))))
2.  [T]  :  Type
3.  \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))))
4.  [R]  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}
5.  \mforall{}a,b:\mBbbN{}.  \mforall{}x,z:T.
          ((x  R\^{}a  +  b  z)  {}\mRightarrow{}  (\mexists{}y:T.  ((x  R\^{}a  y)  \mwedge{}  (y  R\^{}b  z))))
6.  a  :  \mBbbN{}
7.  \mforall{}b:\mBbbN{}.  \mforall{}x,z:T.
          ((x  R\^{}a  +  b  z)  {}\mRightarrow{}  (\mexists{}y:T.  ((x  R\^{}a  y)  \mwedge{}  (y  R\^{}b  z))))
8.  b  :  \mBbbN{}
9.  \mforall{}x,z:T.
          ((x  R\^{}a  +  b  z)  {}\mRightarrow{}  (\mexists{}y:T.  ((x  R\^{}a  y)  \mwedge{}  (y  R\^{}b  z))))
10.  x  :  T
11.  \mforall{}z:T.  ((x  rel\_exp(T;  R;  a  +  b)  z)  {}\mRightarrow{}  (\mexists{}y:T.  ((x  rel\_exp(T;  R;  a)  y)  \mwedge{}  (y  rel\_exp(T;  R;  b)  z))))
12.  z  :  T
13.  (x  rel\_exp(T;  R;  a  +  b)  z)  {}\mRightarrow{}  (\mexists{}y:T.  ((x  rel\_exp(T;  R;  a)  y)  \mwedge{}  (y  rel\_exp(T;  R;  b)  z)))
14.  \mexists{}y:T.  ((x  rel\_exp(T;  R;  a)  y)  \mwedge{}  (y  rel\_exp(T;  R;  b)  z))
\mvdash{}  x  rel\_exp(T;  R;  a  +  b)  z


By

---

Latex:
(ExRepD  THEN  Using  [`y',\mkleeneopen{}y\mkleeneclose{}]  (BLemma  `rel\_exp\_add`)\mcdot{}  THEN  Auto)\mcdot{}

---

Home Index