Nuprl Definition : SM3-class

SM3-class(init;trX1;trX2;trX3) ==  SM-gen-class(init;3;1;n.if (n = 1) then trX1 if (n = 2) then trX2 else trX3 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 :  SM3-class
SM3-class(init;trX1;trX2;trX3)  ==
    SM-gen-class(init;3;1;\mlambda{}n.if  (n  =\msubz{}  1)  then  trX1
                                                      if  (n  =\msubz{}  2)  then  trX2
                                                      else  trX3
                                                      fi  )


Date html generated: 2011_10_20-PM-03_36_58
Last ObjectModification: 2011_08_17-AM-00_56_01

Home Index