### Nuprl Lemma : reg-seq-inv_wf

`∀[b:ℕ+]. ∀[x:{f:ℕ+ ⟶ ℤ| b-regular-seq(f)} ]. ∀[k:ℕ+].`
`  reg-seq-inv(x) ∈ {f:ℕ+ ⟶ ℤ| b * ((k * k) + 1)-regular-seq(f)}  supposing ∀m:ℕ+. ((2 * m) ≤ (k * |x m|))`

Proof

Definitions occuring in Statement :  reg-seq-inv: `reg-seq-inv(x)` regular-int-seq: `k-regular-seq(f)` absval: `|i|` nat_plus: `ℕ+` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` le: `A ≤ B` all: `∀x:A. B[x]` member: `t ∈ T` set: `{x:A| B[x]} ` apply: `f a` function: `x:A ⟶ B[x]` multiply: `n * m` add: `n + m` natural_number: `\$n` int: `ℤ`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` all: `∀x:A. B[x]` not: `¬A` implies: `P `` Q` false: `False` decidable: `Dec(P)` or: `P ∨ Q` nat: `ℕ` so_lambda: `λ2x.t[x]` so_apply: `x[s]` squash: `↓T` prop: `ℙ` nat_plus: `ℕ+` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` top: `Top` and: `P ∧ Q` true: `True` subtype_rel: `A ⊆r B` guard: `{T}` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` sq_type: `SQType(T)` reg-seq-inv: `reg-seq-inv(x)` nequal: `a ≠ b ∈ T ` regular-int-seq: `k-regular-seq(f)` bool: `𝔹` unit: `Unit` it: `⋅` btrue: `tt` uiff: `uiff(P;Q)` less_than: `a < b` less_than': `less_than'(a;b)` bfalse: `ff` bnot: `¬bb` ifthenelse: `if b then t else f fi ` assert: `↑b` le: `A ≤ B` int_nzero: `ℤ-o` sq_stable: `SqStable(P)` rev_uimplies: `rev_uimplies(P;Q)` ge: `i ≥ j ` subtract: `n - m` absval: `|i|`
Lemmas referenced :  decidable__not decidable__equal_int nat_plus_wf subtype_base_sq nat_wf set_subtype_base le_wf int_subtype_base absval-non-neg equal_wf squash_wf true_wf absval_pos nat_plus_properties decidable__le satisfiable-full-omega-tt intformand_wf intformnot_wf intformle_wf itermConstant_wf itermVar_wf intformeq_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_eq_lemma int_formula_prop_wf iff_weakening_equal itermMultiply_wf intformless_wf int_term_value_mul_lemma int_formula_prop_less_lemma equal-wf-T-base regular-int-seq_wf all_wf absval_wf set_wf absval_unfold lt_int_wf bool_wf eqtt_to_assert assert_of_lt_int top_wf less_than_wf decidable__lt eqff_to_assert bool_cases_sqequal bool_subtype_base assert-bnot itermMinus_wf int_term_value_minus_lemma mul_cancel_in_le subtract_wf absval_nat_plus int_entire_a absval_mul multiply_nat_plus add_nat_plus multiply_nat_wf nat_plus_subtype_nat left_mul_subtract_distrib div_rem_sum2 nequal_wf rem_bounds_absval sq_stable__less_than le_functionality le_weakening add_functionality_wrt_le int-triangle-inequality mul-distributes minus-add add-associates minus-one-mul mul-swap mul-commutes mul-associates one-mul add-swap itermSubtract_wf int_term_value_subtract_lemma add_functionality_wrt_eq mul_bounds_1a multiply_functionality_wrt_le false_wf itermAdd_wf int_term_value_add_lemma multiply-is-int-iff absval_sym nat_properties
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut setElimination thin rename lambdaFormation extract_by_obid sqequalHypSubstitution isectElimination because_Cache independent_functionElimination dependent_functionElimination applyEquality functionExtensionality hypothesisEquality hypothesis natural_numberEquality unionElimination instantiate cumulativity independent_isectElimination sqequalRule intEquality lambdaEquality dependent_set_memberEquality imageElimination equalityTransitivity equalitySymmetry universeEquality dependent_pairFormation int_eqEquality isect_memberEquality voidElimination voidEquality independent_pairFormation computeAll imageMemberEquality baseClosed productElimination divideEquality multiplyEquality addEquality axiomEquality functionEquality minusEquality equalityElimination lessCases sqequalAxiom promote_hyp remainderEquality applyLambdaEquality baseApply closedConclusion

Latex:
\mforall{}[b:\mBbbN{}\msupplus{}].  \mforall{}[x:\{f:\mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}|  b-regular-seq(f)\}  ].  \mforall{}[k:\mBbbN{}\msupplus{}].
reg-seq-inv(x)  \mmember{}  \{f:\mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}|  b  *  ((k  *  k)  +  1)-regular-seq(f)\}    supposing  \mforall{}m:\mBbbN{}\msupplus{}.  ((2  *  m)  \mleq{}  (k  *  |\000Cx  m|))

Date html generated: 2017_10_02-PM-07_16_26
Last ObjectModification: 2017_07_28-AM-07_20_56

Theory : reals

Home Index