Nuprl Definition : SM2-class

SM2-class(init;trX1;trX2) == SM-gen-class(init;2;1;

n.if (n =

1) then trX1 else trX2 fi )

Proof not projected

Definitions occuring in Statement : SM-gen-class: SM-gen-class(init;n;m;trXs), eq_int: (i =

j), ifthenelse: if b then t else f fi , lambda:

x.A[x], natural_number: $n
FDL editor aliases : SM2-class

SM2-class(init;trX1;trX2) == SM-gen-class(init;2;1;\mlambda{}n.if (n =\msubz{} 1) then trX1 else trX2 fi ) Date html generated: 2011_10_20-PM-03_36_30 Last ObjectModification: 2011_08_17-AM-00_53_29 Home Index