Nuprl Definition : polyvar

polyvar(v)

==r if v=0  then tree_node(tree_leaf(0);tree_leaf(1))  else eval a = polyvar(v - 1) in tree_node(a;tree_leaf(0))

polyvar(v) ==
  fix((λpolyvar,v. if v=0
                      then tree_node(tree_leaf(0);tree_leaf(1))
                      else eval a = polyvar (v - 1) in
                           tree_node(a;tree_leaf(0))))
  v

Wellformedness Lemmas : polyvar_wf2, polyvar_wf
Definitions occuring in Statement : tree_node: tree_node(left;right), tree_leaf: tree_leaf(value), callbyvalue: callbyvalue, int_eq: if a=b then c else d, apply: f a, fix: fix(F), lambda: λx.A[x], subtract: n - m, natural_number: $n
Definitions occuring in definition : fix: fix(F), lambda: λx.A[x], int_eq: if a=b then c else d, callbyvalue: callbyvalue, apply: f a, subtract: n - m, tree_node: tree_node(left;right), tree_leaf: tree_leaf(value), natural_number: $n
FDL editor aliases : polyvar

Latex:
polyvar(v) ==r if v=0 then tree\_node(tree\_leaf(0);tree\_leaf(1)) else eval a = polyvar(v - 1) in tree\_node(a;tree\_leaf(0))

Latex:
polyvar(v) == fix((\mlambda{}polyvar,v. if v=0 then tree\_node(tree\_leaf(0);tree\_leaf(1)) else eval a = polyvar (v - 1) in tree\_node(a;tree\_leaf(0)))) v Date html generated: 2017_10_01-AM-08_32_23 Last ObjectModification: 2017_05_02-PM-06_04_12 Theory : integer!polynomial!trees Home Index