Nuprl Definition : omral_scale

<k,v>* ps ==
  Y 
  (λomral_scale,ps. case ps of 
                      [] => [] 
                      p::ps' =>
                       if (v * (snd(p))) =b 0
                      then omral_scale ps'
                      else [<k * (fst(p)), v * (snd(p))> / (omral_scale ps')]
                      fi  
                   esac) 
  ps


Definitions occuring in Statement :  list_ind: list_ind,  cons: [a / b],  nil: [],  ifthenelse: if b then t else f fi ,  infix_ap: x f y,  pi1: fst(t),  pi2: snd(t),  ycomb: Y,  apply: f a,  lambda: λx.A[x],  pair: <a, b>,  rng_times: *,  rng_zero: 0,  rng_eq: =b,  grp_op: *
Definitions occuring in definition :  ycomb: Y,  lambda: λx.A[x],  list_ind: list_ind,  nil: [],  ifthenelse: if b then t else f fi ,  rng_eq: =b,  rng_zero: 0,  cons: [a / b],  pair: <a, b>,  grp_op: *,  pi1: fst(t),  infix_ap: x f y,  rng_times: *,  pi2: snd(t),  apply: f a
Latex:
<k,v>*  ps  ==
    Y 
    (\mlambda{}omral$_{scale}$,ps.  case  ps  of 
                                          []  =>  [] 
                                          p::ps'  =>
                                            if  (v  *  (snd(p)))  =\msubb{}  0
                                          then  omral$_{scale}$  ps'
                                          else  [<k  *  (fst(p)),  v  *  (snd(p))>  /  (omral$_{scale}$  ps')]
                                          fi   
                                    esac) 
    ps


Date html generated: 2016_05_16-AM-08_24_23
Last ObjectModification: 2015_09_23-AM-09_53_18

Theory : polynom_3


Home Index