Nuprl Definition : SM-gen-class

SM-gen-class(init;n;m;trXs) == rec-comb(

i.(snd((trXs i)));

l,bs,bp.SM-gen-tr(l;

i.<bs i, fst((trXs i))>;bp;n;m);init)

Proof not projected

Definitions occuring in Statement : SM-gen-tr: SM-gen-tr(l;btrs;bp;n;m), rec-comb: rec-comb(X;f;init), pi1: fst(t), pi2: snd(t), apply: f a, lambda:

x.A[x], pair: <a, b>
FDL editor aliases : SM-gen-class

SM-gen-class(init;n;m;trXs) == rec-comb(\mlambda{}i.(snd((trXs i)));\mlambda{}l,bs,bp.SM-gen-tr(l;\mlambda{}i.<bs i, fst((trXs i))>bp;n;m);init) Date html generated: 2011_10_20-PM-03_35_25 Last ObjectModification: 2011_08_17-AM-00_39_07 Home Index