Nuprl Definition : ispolyform
ispolyform(p) == tree_ind(p; tree_leaf(x)⇒ λn.tt; tree_node(a,b)⇒ ra,rb.λn.(((ra (n - 1)) ∧b (rb n)) ∧b 0 <z n))
Definitions occuring in Statement :
tree_ind: tree_ind,
band: p ∧b q,
lt_int: i <z j,
btrue: tt,
apply: f a,
lambda: λx.A[x],
subtract: n - m,
natural_number: $n
Definitions occuring in definition :
tree_ind: tree_ind,
btrue: tt,
lambda: λx.A[x],
band: p ∧b q,
subtract: n - m,
apply: f a,
lt_int: i <z j,
natural_number: $n
FDL editor aliases :
ispolyform
Latex:
ispolyform(p) ==
tree\_ind(p;
tree\_leaf(x){}\mRightarrow{} \mlambda{}n.tt;
tree\_node(a,b){}\mRightarrow{} ra,rb.\mlambda{}n.(((ra (n - 1)) \mwedge{}\msubb{} (rb n)) \mwedge{}\msubb{} 0 <z n))
Date html generated:
2017_10_01-AM-08_32_11
Last ObjectModification:
2017_05_02-PM-00_37_03
Theory : integer!polynomial!trees
Home
Index