### Nuprl Lemma : sparse-rep-base_wf

`∀[r:{-2..3-}]`
`  (sparse-rep-base(r) ∈ {L:{-1..2-} List| `
`                         (r = Σi<||L||.L[i]*2^i ∈ ℤ)`
`                         ∧ (||L|| = 2 ∈ ℤ)`
`                         ∧ (∀i:ℕ||L|| - 1. ((L[i] = 0 ∈ ℤ) ∨ (L[i + 1] = 0 ∈ ℤ)))} )`

Proof

Definitions occuring in Statement :  sparse-rep-base: `sparse-rep-base(r)` power-sum: `Σi<n.a[i]*x^i` select: `L[n]` length: `||as||` list: `T List` int_seg: `{i..j-}` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` or: `P ∨ Q` and: `P ∧ Q` member: `t ∈ T` set: `{x:A| B[x]} ` subtract: `n - m` add: `n + m` minus: `-n` natural_number: `\$n` int: `ℤ` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` sparse-rep-base: `sparse-rep-base(r)` subtype_rel: `A ⊆r B` all: `∀x:A. B[x]` so_lambda: `λ2x.t[x]` prop: `ℙ` and: `P ∧ Q` int_seg: `{i..j-}` uimplies: `b supposing a` guard: `{T}` lelt: `i ≤ j < k` decidable: `Dec(P)` or: `P ∨ Q` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` false: `False` implies: `P `` Q` not: `¬A` top: `Top` less_than: `a < b` squash: `↓T` so_apply: `x[s]` sq_exists: `∃x:A [B[x]]`
Lemmas referenced :  small-sparse-rep-ext all_wf int_seg_wf sq_exists_wf list_wf equal_wf power-sum_wf length_wf_nat select_wf int_seg_properties decidable__le satisfiable-full-omega-tt intformand_wf intformnot_wf intformle_wf itermConstant_wf itermVar_wf int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_wf decidable__lt length_wf intformless_wf int_formula_prop_less_lemma equal-wf-T-base subtract_wf or_wf itermSubtract_wf int_term_value_subtract_lemma itermAdd_wf int_term_value_add_lemma
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule applyEquality thin instantiate extract_by_obid hypothesis lambdaEquality sqequalHypSubstitution hypothesisEquality isectElimination minusEquality natural_numberEquality productEquality intEquality setElimination rename because_Cache independent_isectElimination productElimination dependent_functionElimination unionElimination dependent_pairFormation int_eqEquality isect_memberEquality voidElimination voidEquality independent_pairFormation computeAll imageElimination baseClosed equalityTransitivity equalitySymmetry axiomEquality

Latex:
\mforall{}[r:\{-2..3\msupminus{}\}]
(sparse-rep-base(r)  \mmember{}  \{L:\{-1..2\msupminus{}\}  List|
(r  =  \mSigma{}i<||L||.L[i]*2\^{}i)
\mwedge{}  (||L||  =  2)
\mwedge{}  (\mforall{}i:\mBbbN{}||L||  -  1.  ((L[i]  =  0)  \mvee{}  (L[i  +  1]  =  0)))\}  )

Date html generated: 2018_05_21-PM-08_34_38
Last ObjectModification: 2017_07_26-PM-05_59_52

Theory : general

Home Index