Nuprl Definition : state-class2

state-class2(init;tr1;X1;tr2;X2) ==  loop-class-state((tr1 X1) || (tr2 X2);λloc.{init loc})



Definitions occuring in Statement :  loop-class-state: loop-class-state(X;init) parallel-class: || Y eclass1: (f X) apply: a lambda: λx.A[x] single-bag: {x}
FDL editor aliases :  state-class2

Latex:
state-class2(init;tr1;X1;tr2;X2)  ==    loop-class-state((tr1  o  X1)  ||  (tr2  o  X2);\mlambda{}loc.\{init  loc\})



Date html generated: 2015_07_21-PM-02_38_19
Last ObjectModification: 2012_10_05-PM-01_21_04

Home Index