Nuprl Definition : eclass-state
eclass-state(init;f;X) == loop-class((λi,a,b. {f i a b} o X);λl.{init l})
Definitions occuring in Statement :
loop-class: loop-class(X;init),
eclass1: (f o X),
apply: f a,
lambda: λx.A[x],
single-bag: {x}
FDL editor aliases :
eclass-state
Latex:
eclass-state(init;f;X) == loop-class((\mlambda{}i,a,b. \{f i a b\} o X);\mlambda{}l.\{init l\})
Date html generated:
2016_05_16-PM-11_47_06
Last ObjectModification:
2012_08_15-AM-02_18_26
Theory : event-ordering
Home
Index