Nuprl Definition : smr-class

smr-class(init;s,x.F[s; x];X) ==  (snd(sr) where sr from sm-class(init;s,x.F[s; x];X))


Proof not projected



Definitions occuring in Statement :  sm-class: sm-class(init;s,x.F[s; x];X),  map-class: (f[v] where v from X),  pi2: snd(t)
Definitions :  map-class: (f[v] where v from X),  pi2: snd(t),  sm-class: sm-class(init;s,x.F[s; x];X)
FDL editor aliases :  smr-class
smr-class(init;s,x.F[s;  x];X)  ==    (snd(sr)  where  sr  from  sm-class(init;s,x.F[s;  x];X))


Date html generated: 2011_10_20-PM-04_09_23
Last ObjectModification: 2011_01_24-PM-06_58_14

Home Index