Nuprl Definition : State-class

State-class(init;f;X) ==  λx,s. if bag-null(x) then s else lifting-2(f) x s fi |X, Memory-class(f;init;X)|


Definitions occuring in Statement :  Memory-class: Memory-class(f;init;X),  simple-comb-2: F|X, Y|,  ifthenelse: if b then t else f fi ,  apply: f a,  lambda: λx.A[x],  lifting-2: lifting-2(f),  bag-null: bag-null(bs)
FDL editor aliases :  State-class
Latex:
State-class(init;f;X)  ==
    \mlambda{}x,s.  if  bag-null(x)  then  s  else  lifting-2(f)  x  s  fi  |X,  Memory-class(f;init;X)|


Date html generated: 2016_05_17-AM-09_35_32
Last ObjectModification: 2012_11_29-AM-11_16_59

Theory : classrel!lemmas


Home Index