---

Step * of Lemma rel_exp_add-ext

∀[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
{ Extract of Obid: rel_exp_add
  normalizes to:
  
  fix((λf,m,n,rm,rn. if m=0
                        then rn
                        else if m + n=0
                                then Ax
                                else let z1,r_rm' = rm 
                                     in <z1, let r,rm' = r_rm' in <r, f (m - 1) n rm' rn>>))
  finishing with Auto }

---

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:
Extract  of  Obid:  rel\_exp\_add
normalizes  to:

fix((\mlambda{}f,m,n,rm,rn.  if  m=0
                                            then  rn
                                            else  if  m  +  n=0
                                                            then  Ax
                                                            else  let  z1,r$_{rm'}$  =  rm 
                                                                      in  <z1,  let  r,rm'  =  r$_{rm'}$  in  <r,  f  (m  -  1\000C)  n  rm'  rn>>))
finishing  with  Auto

---

Home Index