Nuprl Definition : int_formulaco_size

int_formulaco_size(p) ==
  fix((λsize,p. let lbl,x 
                in if lbl =a "less" then 0
                   if lbl =a "le" then 0
                   if lbl =a "eq" then 0
                   if lbl =a "and" then (size (fst(x))) (size (snd(x)))
                   if lbl =a "or" then (size (fst(x))) (size (snd(x)))
                   if lbl =a "implies" then (size (fst(x))) (size (snd(x)))
                   if lbl =a "not" then (size x)
                   else 0
                   fi )) 
  p



Definitions occuring in Statement :  ifthenelse: if then else fi  eq_atom: =a y pi1: fst(t) pi2: snd(t) apply: a fix: fix(F) lambda: λx.A[x] spread: spread def add: 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 then else fi  eq_atom: =a y token: "$token" add: m apply: a natural_number: $n
FDL editor aliases :  int_formulaco_size

Latex:
int\_formulaco\_size(p)  ==
    fix((\mlambda{}size,p.  let  lbl,x  =  p 
                                in  if  lbl  =a  "less"  then  0
                                      if  lbl  =a  "le"  then  0
                                      if  lbl  =a  "eq"  then  0
                                      if  lbl  =a  "and"  then  1  +  (size  (fst(x)))  +  (size  (snd(x)))
                                      if  lbl  =a  "or"  then  1  +  (size  (fst(x)))  +  (size  (snd(x)))
                                      if  lbl  =a  "implies"  then  1  +  (size  (fst(x)))  +  (size  (snd(x)))
                                      if  lbl  =a  "not"  then  1  +  (size  x)
                                      else  0
                                      fi  )) 
    p



Date html generated: 2016_05_14-AM-07_04_11
Last ObjectModification: 2015_09_22-PM-05_51_56

Theory : omega


Home Index