Nuprl Lemma : polyconst_wf
∀[k,n:ℤ]. (polyconst(k) ∈ polynom(n))
Proof
Definitions occuring in Statement :
polyconst: polyconst(k),
polynom: polynom(n),
uall: ∀[x:A]. B[x],
member: t ∈ T,
int: ℤ
Definitions unfolded in proof :
polynom: polynom(n),
uall: ∀[x:A]. B[x],
member: t ∈ T,
polyconst: polyconst(k),
implies: P ⇒ Q,
assert: ↑b,
ifthenelse: if b then t else f fi ,
tree_leaf?: tree_leaf?(v),
eq_atom: x =a y,
pi1: fst(t),
tree_leaf: tree_leaf(value),
btrue: tt,
true: True,
prop: ℙ,
ispolyform: ispolyform(p),
tree_ind: tree_ind,
polyform: polyform(n)
Lemmas referenced :
assert_wf,
poly-int_wf,
tree_leaf_wf,
ispolyform_wf,
tree_leaf?_wf
Rules used in proof :
sqequalSubstitution,
sqequalRule,
sqequalReflexivity,
sqequalTransitivity,
computationStep,
isect_memberFormation,
introduction,
cut,
lambdaFormation,
hypothesis,
natural_numberEquality,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
intEquality,
hypothesisEquality,
dependent_set_memberEquality,
applyEquality,
functionEquality,
setElimination,
rename,
because_Cache,
axiomEquality,
equalityTransitivity,
equalitySymmetry,
isect_memberEquality
Latex:
\mforall{}[k,n:\mBbbZ{}]. (polyconst(k) \mmember{} polynom(n))
Date html generated:
2017_10_01-AM-08_32_22
Last ObjectModification:
2017_05_02-PM-00_39_20
Theory : integer!polynomial!trees
Home
Index