Nuprl Definition : eclass-disju-program

xpr ypr ==  eclass1-program(λl,x. (inl x);xpr) || eclass1-program(λl,x. (inr );ypr)



Definitions occuring in Statement :  parallel-class-program: || Y eclass1-program: eclass1-program(f;pr) lambda: λx.A[x] inr: inr  inl: inl x
FDL editor aliases :  eclass-disju-program

Latex:
xpr  +  ypr  ==    eclass1-program(\mlambda{}l,x.  (inl  x);xpr)  ||  eclass1-program(\mlambda{}l,x.  (inr  x  );ypr)



Date html generated: 2016_05_17-AM-09_09_30
Last ObjectModification: 2012_11_29-PM-06_21_56

Theory : local!classes


Home Index