Nuprl Definition : rat_term_size
rat_term_size(p) ==
  fix((λsize,p. let lbl,x = p 
                in if lbl =a "Constant" then 0
                   if lbl =a "Var" then 0
                   if lbl =a "Add" then 1 + (size (fst(x))) + (size (snd(x)))
                   if lbl =a "Subtract" then 1 + (size (fst(x))) + (size (snd(x)))
                   if lbl =a "Multiply" then 1 + (size (fst(x))) + (size (snd(x)))
                   if lbl =a "Divide" then 1 + (size (fst(x))) + (size (snd(x)))
                   if lbl =a "Minus" then 1 + (size x)
                   else 0
                   fi )) 
  p
Definitions occuring in Statement : 
ifthenelse: if b then t else f fi 
, 
eq_atom: x =a y
, 
pi1: fst(t)
, 
pi2: snd(t)
, 
apply: f a
, 
fix: fix(F)
, 
lambda: λx.A[x]
, 
spread: spread def, 
add: n + m
, 
natural_number: $n
, 
token: "$token"
Definitions occuring in definition : 
fix: fix(F)
, 
lambda: λx.A[x]
, 
spread: spread def, 
pi1: fst(t)
, 
pi2: snd(t)
, 
ifthenelse: if b then t else f fi 
, 
eq_atom: x =a y
, 
token: "$token"
, 
add: n + m
, 
apply: f a
, 
natural_number: $n
FDL editor aliases : 
rat_term_size
Latex:
rat\_term\_size(p)  ==
    fix((\mlambda{}size,p.  let  lbl,x  =  p 
                                in  if  lbl  =a  "Constant"  then  0
                                      if  lbl  =a  "Var"  then  0
                                      if  lbl  =a  "Add"  then  1  +  (size  (fst(x)))  +  (size  (snd(x)))
                                      if  lbl  =a  "Subtract"  then  1  +  (size  (fst(x)))  +  (size  (snd(x)))
                                      if  lbl  =a  "Multiply"  then  1  +  (size  (fst(x)))  +  (size  (snd(x)))
                                      if  lbl  =a  "Divide"  then  1  +  (size  (fst(x)))  +  (size  (snd(x)))
                                      if  lbl  =a  "Minus"  then  1  +  (size  x)
                                      else  0
                                      fi  )) 
    p
Date html generated:
2019_10_29-AM-09_25_23
Last ObjectModification:
2019_03_31-PM-05_15_59
Theory : reals
Home
Index