Nuprl Lemma : poly-int-val_wf
∀[n:ℕ]. ∀[p:polyform(n)]. ∀[l:{l:ℤ List| n ≤ ||l||} ]. (p@l ∈ ℤ)
Proof
Definitions occuring in Statement :
poly-int-val: p@l,
polyform: polyform(n),
length: ||as||,
list: T List,
nat: ℕ,
uall: ∀[x:A]. B[x],
le: A ≤ B,
member: t ∈ T,
set: {x:A| B[x]} ,
int: ℤ
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
poly-int-val: p@l,
nat: ℕ,
prop: ℙ,
so_lambda: λ2x.t[x],
so_apply: x[s]
Lemmas referenced :
poly-val-fun_wf,
le_wf,
length_wf,
set_wf,
list_wf,
polyform_wf,
nat_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
introduction,
cut,
setElimination,
thin,
rename,
sqequalRule,
applyEquality,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
hypothesisEquality,
hypothesis,
dependent_set_memberEquality,
intEquality,
axiomEquality,
equalityTransitivity,
equalitySymmetry,
lambdaEquality,
isect_memberEquality,
because_Cache
Latex:
\mforall{}[n:\mBbbN{}]. \mforall{}[p:polyform(n)]. \mforall{}[l:\{l:\mBbbZ{} List| n \mleq{} ||l||\} ]. (p@l \mmember{} \mBbbZ{})
Date html generated:
2017_10_01-AM-08_32_29
Last ObjectModification:
2017_05_02-PM-01_49_46
Theory : integer!polynomial!trees
Home
Index