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 <n
                  letrec f(x)=λn,Rm,Rn. if x=0
                                             then Rn
                                             else if n=0
                                                     then Ax
                                                     else let z1,R_Rm' Rm 
                                                          in <z1, let R,Rm' R_Rm' in <R, (x 1) Rm' Rn>> in
                     f(m) 
                    
                    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