Nuprl Definition : SM4-class

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


Date html generated: 2011_10_20-PM-03_37_25
Last ObjectModification: 2011_09_12-AM-10_31_36

Home Index