Nuprl Definition : sm-class

sm-class(init;s,x.F[s; x];X) ==  accum-class(p,x.F[fst(p); x];x.F[init; x];X)


Proof not projected



Definitions occuring in Statement :  accum-class: accum-class(a,x.f[a; x];x.base[x];X),  pi1: fst(t)
Definitions :  accum-class: accum-class(a,x.f[a; x];x.base[x];X),  pi1: fst(t)
FDL editor aliases :  sm-class
sm-class(init;s,x.F[s;  x];X)  ==    accum-class(p,x.F[fst(p);  x];x.F[init;  x];X)


Date html generated: 2011_10_20-PM-04_08_58
Last ObjectModification: 2011_01_24-PM-06_55_37

Home Index