Nuprl Definition : int_term_value

int_term_value(f;t) ==
  int_term_ind(t;
               itermConstant(n)⇒ n;
               itermVar(v)⇒ f v;
               itermAdd(l,r)⇒ rl,rr.rl + rr;
               itermSubtract(l,r)⇒ rl,rr.rl - rr;
               itermMultiply(l,r)⇒ rl,rr.rl * rr;
               itermMinus(x)⇒ r.-r) 


Definitions occuring in Statement :  int_term_ind: int_term_ind,  apply: f a,  multiply: n * m,  subtract: n - m,  add: n + m,  minus: -n
Definitions occuring in definition :  int_term_ind: int_term_ind,  apply: f a,  add: n + m,  subtract: n - m,  multiply: n * m,  minus: -n
FDL editor aliases :  int_term_value
Latex:
int\_term\_value(f;t)  ==
    int\_term\_ind(t;
                              itermConstant(n){}\mRightarrow{}  n;
                              itermVar(v){}\mRightarrow{}  f  v;
                              itermAdd(l,r){}\mRightarrow{}  rl,rr.rl  +  rr;
                              itermSubtract(l,r){}\mRightarrow{}  rl,rr.rl  -  rr;
                              itermMultiply(l,r){}\mRightarrow{}  rl,rr.rl  *  rr;
                              itermMinus(x){}\mRightarrow{}  r.-r) 


Date html generated: 2016_05_14-AM-06_59_21
Last ObjectModification: 2015_09_22-PM-05_51_37

Theory : omega


Home Index