---

Step * of Lemma rel_exp_add

∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  ∀m,n:ℕ.  ∀[x,y,z:T].  ((x R^m y) ⇒ (y R^n z) ⇒ (x R^m + n z))
BY
{ (RepeatFor 2 ((D 0 THENA Auto))
   THEN (InstLemma `complete_nat_ind_with_y` [⌜parm{i}⌝;⌜λ2m.∀n:ℕ
                                                               ∀[x,y,z:T].  ((x R^m y) ⇒ (y R^n z) ⇒ (x R^m + n z))⌝]⋅
         THENA Auto'
         )
   ) }

1
1. [T] : Type
2. [R] : T ⟶ T ⟶ ℙ
3. i : ℕ
4. ∀j:ℕi. ∀n:ℕ.  ∀[x,y,z:T].  ((x R^j y) ⇒ (y R^n z) ⇒ (x R^j + n z))
5. n : ℕ
6. [x] : T
7. [y] : T
8. [z] : T
9. x R^i y
10. y R^n z
⊢ x R^i + n z

2
1. [T] : Type
2. [R] : T ⟶ T ⟶ ℙ
3. ∀i,n:ℕ.  ∀[x,y,z:T].  ((x R^i y) ⇒ (y R^n z) ⇒ (x R^i + n z))
⊢ ∀m,n:ℕ.  ∀[x,y,z:T].  ((x R^m y) ⇒ (y R^n z) ⇒ (x R^m + n z))

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].
    \mforall{}m,n:\mBbbN{}.    \mforall{}[x,y,z:T].    ((x  R\^{}m  y)  {}\mRightarrow{}  (y  R\^{}n  z)  {}\mRightarrow{}  (x  rel\_exp(T;  R;  m  +  n)  z))


By

---

Latex:
(RepeatFor  2  ((D  0  THENA  Auto))
  THEN  (InstLemma  `complete\_nat\_ind\_with\_y`  [\mkleeneopen{}parm\{i\}\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}m.\mforall{}n:\mBbbN{}
                                                                                                                          \mforall{}[x,y,z:T].
                                                                                                                              ((x  rel\_exp(T;  R;  m)  y)
                                                                                                                              {}\mRightarrow{}  (y  R\^{}n  z)
                                                                                                                              {}\mRightarrow{}  (x  rel\_exp(T;  R;  m  +  n)  z))\mkleeneclose{}]\mcdot{}
              THENA  Auto'
              )
  )

---

Home Index