---

Step * of Lemma rel_star_transitivity_ext

∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ]. ∀[x,y,z:T].  ((x (R^*) y) ⇒ (y (R^*) z) ⇒ (x (R^*) z))
BY
{ Extract of Obid: rel_star_transitivity
  normalizes to:
  
  λxRy,yRz. let n,Rn = yRz 
            in let m,Rm = xRy 
               in <m + n
                  , letrec f(x)=λn,Rm,Rn. if x=0
                                             then Rn
                                             else if x + n=0
                                                     then Ax
                                                     else let z1,R_Rm' = Rm 
                                                          in <z1, let R,Rm' = R_Rm' in <R, f (x - 1) n Rm' Rn>> in
                     f(m) 
                    n 
                    Rm 
                    Rn
                  >
  finishing with Auto }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[x,y,z:T].
    ((x  (R\^{}*)  y)  {}\mRightarrow{}  (y  (R\^{}*)  z)  {}\mRightarrow{}  (x  (R\^{}*)  z))


By

---

Latex:
Extract  of  Obid:  rel\_star\_transitivity
normalizes  to:

\mlambda{}xRy,yRz.  let  n,Rn  =  yRz 
                    in  let  m,Rm  =  xRy 
                          in  <m  +  n
                                ,  letrec  f(x)=\mlambda{}n,Rm,Rn.  if  x=0
                                                                                      then  Rn
                                                                                      else  if  x  +  n=0
                                                                                                      then  Ax
                                                                                                      else  let  z1,R$_{Rm'}$  =  Rm 
                                                                                                                in  <z1
                                                                                                                      ,  let  R,Rm'  =  R$_{Rm'}\mbackslash{}ff\000C24 
                                                                                                                          in  <R,  f  (x  -  1)  n  Rm'  Rn>
                                                                                                                      >  in
                                      f(m) 
                                    n 
                                    Rm 
                                    Rn
                                >
finishing  with  Auto

---

Home Index