Nuprl Definition : ot-less-trans

ot-less-trans() ==
  λa,b,c,%,%1. let A,<,c2 = c in 
              let A1,<1,b2 = b in 
              let A2,<2,a2 = a in 
              let f,b,%4,%5 = %1 
              in let f1,b3,%8,%9 = % 
                 in <f o f1, b, λa1,a3,%. (%4 (f1 a1) (f1 a3) (%8 a1 a3 %)), λa.(%5 (f1 a))>    


Definitions occuring in Statement :  compose: f o g,  spreadn: spread4,  spreadn: spread3,  apply: f a,  lambda: λx.A[x],  pair: <a, b>
Definitions occuring in definition :  spreadn: spread3,  spreadn: spread4,  compose: f o g,  pair: <a, b>,  lambda: λx.A[x],  apply: f a
FDL editor aliases :  ot-less-trans
Latex:
ot-less-trans()  ==
    \mlambda{}a,b,c,\%,\%1.  let  A,<,c2  =  c  in 
                            let  A1,ə,b2  =  b  in 
                            let  A2,ɚ,a2  =  a  in 
                            let  f,b,\%4,\%5  =  \%1 
                            in  let  f1,b3,\%8,\%9  =  \% 
                                  in  <f  o  f1,  b,  \mlambda{}a1,a3,\%.  (\%4  (f1  a1)  (f1  a3)  (\%8  a1  a3  \%)),  \mlambda{}a.(\%5  (f1  a))>       


Date html generated: 2016_05_15-PM-04_14_00
Last ObjectModification: 2015_09_23-AM-07_47_10

Theory : general


Home Index