### Nuprl Lemma : poly_int_val_cons

`∀p,l,a:Top.  (p@[a / l] ~ Σ(p[i]@l * a^||p|| - 1 - i | i < ||p||))`

Proof

Definitions occuring in Statement :  poly-int-val: `p@l` exp: `i^n` sum: `Σ(f[x] | x < k)` select: `L[n]` length: `||as||` cons: `[a / b]` top: `Top` all: `∀x:A. B[x]` multiply: `n * m` subtract: `n - m` natural_number: `\$n` sqequal: `s ~ t`
Definitions unfolded in proof :  bfalse: `ff` ifthenelse: `if b then t else f fi ` so_apply: `x[s1;s2]` so_lambda: `λ2x y.t[x; y]` top: `Top` poly-int-val: `p@l` member: `t ∈ T` all: `∀x:A. B[x]`
Lemmas referenced :  spread_cons_lemma null_cons_lemma top_wf
Rules used in proof :  voidEquality voidElimination isect_memberEquality thin dependent_functionElimination sqequalHypSubstitution sqequalRule extract_by_obid introduction hypothesis cut lambdaFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

Latex:
\mforall{}p,l,a:Top.    (p@[a  /  l]  \msim{}  \mSigma{}(p[i]@l  *  a\^{}||p||  -  1  -  i  |  i  <  ||p||))

Date html generated: 2017_04_20-AM-07_08_30
Last ObjectModification: 2017_04_17-AM-11_46_20

Theory : list_1

Home Index