Nuprl Definition : Formco

Nuprl Definition : Formco_size

Formco_size(p) ==
  fix((λsize,p. let lbl,x = p
                in if lbl =a "Var" then 0
                   if lbl =a "Const" then 0
                   if lbl =a "Set" then 1 + (size (snd(x)))
                   if lbl =a "Equal" then 1 + (size (fst(x))) + (size (snd(x)))
                   if lbl =a "Member" then 1 + (size (fst(x))) + (size (snd(x)))
                   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 "Not" then 1 + (size x)
                   if lbl =a "All" then 1 + (size (snd(x)))
                   if lbl =a "Exists" then 1 + (size (snd(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), ifthenelse: if b then t else f fi , eq_atom: x =a y, token: "$token", add: n + m, apply: f a, pi2: snd(t), natural_number: $n
FDL editor aliases : Formco_size Formco_size

Latex:
Formco\_size(p) == fix((\mlambda{}size,p. let lbl,x = p in if lbl =a "Var" then 0 if lbl =a "Const" then 0 if lbl =a "Set" then 1 + (size (snd(x))) if lbl =a "Equal" then 1 + (size (fst(x))) + (size (snd(x))) if lbl =a "Member" then 1 + (size (fst(x))) + (size (snd(x))) 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 "Not" then 1 + (size x) if lbl =a "All" then 1 + (size (snd(x))) if lbl =a "Exists" then 1 + (size (snd(x))) else 0 fi )) p Date html generated: 2018_05_21-PM-10_42_02 Last ObjectModification: 2017_10_10-PM-04_31_26 Theory : PZF Home Index