Nuprl Definition : eclass-disju-program
xpr + ypr == eclass1-program(λl,x. (inl x);xpr) || eclass1-program(λl,x. (inr x );ypr)
Definitions occuring in Statement :
parallel-class-program: X || Y,
eclass1-program: eclass1-program(f;pr),
lambda: λx.A[x],
inr: inr x ,
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