### Nuprl Lemma : small-sparse-rep

`∀r:{-2..3-}`
`  (∃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 :  power-sum: `Σi<n.a[i]*x^i` select: `L[n]` length: `||as||` list: `T List` int_seg: `{i..j-}` all: `∀x:A. B[x]` sq_exists: `∃x:A [B[x]]` or: `P ∨ Q` and: `P ∧ Q` subtract: `n - m` add: `n + m` minus: `-n` natural_number: `\$n` int: `ℤ` equal: `s = t ∈ T`
Definitions unfolded in proof :  all: `∀x:A. B[x]` member: `t ∈ T` int_seg: `{i..j-}` decidable: `Dec(P)` or: `P ∨ Q` uall: `∀[x:A]. B[x]` uimplies: `b supposing a` sq_type: `SQType(T)` implies: `P `` Q` guard: `{T}` lelt: `i ≤ j < k` and: `P ∧ Q` not: `¬A` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` false: `False` top: `Top` prop: `ℙ` sq_exists: `∃x:A [B[x]]` le: `A ≤ B` less_than': `less_than'(a;b)` less_than: `a < b` squash: `↓T` true: `True` subtract: `n - m` power-sum: `Σi<n.a[i]*x^i` cand: `A c∧ B` sum: `Σ(f[x] | x < k)` sum_aux: `sum_aux(k;v;i;x.f[x])` select: `L[n]` cons: `[a / b]` exp: `i^n` primrec: `primrec(n;b;c)` nat: `ℕ` so_lambda: `λ2x.t[x]` subtype_rel: `A ⊆r B` so_apply: `x[s]`
Lemmas referenced :  decidable__equal_int subtype_base_sq int_subtype_base int_seg_properties int_seg_subtype_special int_seg_cases full-omega-unsat intformand_wf intformless_wf itermVar_wf itermConstant_wf intformle_wf istype-int int_formula_prop_and_lemma istype-void int_formula_prop_less_lemma int_term_value_var_lemma int_term_value_constant_lemma int_formula_prop_le_lemma int_formula_prop_wf int_seg_wf cons_wf istype-false le_wf less_than_wf nil_wf length_of_cons_lemma length_of_nil_lemma sum_wf select_wf decidable__le intformnot_wf int_formula_prop_not_lemma decidable__lt itermAdd_wf int_term_value_add_lemma exp_wf2 int_seg_subtype_nat select-cons-hd list_subtype_base set_subtype_base lelt_wf length_wf_nat subtract_wf length_wf itermSubtract_wf int_term_value_subtract_lemma intformeq_wf int_formula_prop_eq_lemma
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation_alt cut introduction extract_by_obid sqequalHypSubstitution dependent_functionElimination thin setElimination rename hypothesisEquality hypothesis minusEquality natural_numberEquality unionElimination instantiate isectElimination cumulativity intEquality independent_isectElimination because_Cache independent_functionElimination equalityTransitivity equalitySymmetry hypothesis_subsumption sqequalRule productElimination approximateComputation dependent_pairFormation_alt lambdaEquality_alt int_eqEquality isect_memberEquality_alt voidElimination independent_pairFormation universeIsType dependent_set_memberFormation_alt closedConclusion dependent_set_memberEquality_alt imageMemberEquality baseClosed productIsType multiplyEquality addEquality applyEquality inlFormation_alt equalityIsType4 inhabitedIsType baseApply functionIsType unionIsType inrFormation_alt

Latex:
\mforall{}r:\{-2..3\msupminus{}\}
(\mexists{}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: 2019_10_15-AM-11_27_10
Last ObjectModification: 2018_10_11-PM-10_14_48

Theory : general

Home Index