### Nuprl Lemma : regularize-2-regular

`∀f:ℤ ⟶ ℤ. 2-regular-seq(regularize(f))`

Proof

Definitions occuring in Statement :  regularize: `regularize(f)` regular-int-seq: `k-regular-seq(f)` all: `∀x:A. B[x]` function: `x:A ⟶ B[x]` natural_number: `\$n` int: `ℤ`
Definitions unfolded in proof :  absval: `|i|` subtract: `n - m` true: `True` has-value: `(a)↓` top: `Top` satisfiable_int_formula: `satisfiable_int_formula(fmla)` decidable: `Dec(P)` lelt: `i ≤ j < k` ge: `i ≥ j ` nat_plus: `ℕ+` int_seg: `{i..j-}` rev_implies: `P `` Q` iff: `P `⇐⇒` Q` less_than': `less_than'(a;b)` le: `A ≤ B` nat: `ℕ` not: `¬A` so_apply: `x[s]` so_lambda: `λ2x.t[x]` false: `False` assert: `↑b` bnot: `¬bb` guard: `{T}` sq_type: `SQType(T)` or: `P ∨ Q` prop: `ℙ` exists: `∃x:A. B[x]` bfalse: `ff` ifthenelse: `if b then t else f fi ` uimplies: `b supposing a` and: `P ∧ Q` uiff: `uiff(P;Q)` btrue: `tt` it: `⋅` unit: `Unit` bool: `𝔹` implies: `P `` Q` subtype_rel: `A ⊆r B` uall: `∀[x:A]. B[x]` member: `t ∈ T` regularize: `regularize(f)` regular-int-seq: `k-regular-seq(f)` all: `∀x:A. B[x]` rev_uimplies: `rev_uimplies(P;Q)` squash: `↓T` less_than: `a < b` nequal: `a ≠ b ∈ T ` int_nzero: `ℤ-o` cand: `A c∧ B`
Rules used in proof :  multiplyEquality functionEquality equalityEquality minusEquality callbyvalueReduce computeAll voidEquality isect_memberEquality int_eqEquality addEquality natural_numberEquality dependent_set_memberEquality intEquality levelHypothesis rename setElimination cumulativity isect_memberFormation uallFunctionality independent_pairFormation introduction existsFunctionality addLevel lambdaEquality voidElimination independent_functionElimination instantiate dependent_functionElimination promote_hyp dependent_pairFormation independent_isectElimination productElimination equalitySymmetry equalityTransitivity equalityElimination unionElimination hypothesis because_Cache applyEquality hypothesisEquality thin isectElimination sqequalHypSubstitution lemma_by_obid cut sqequalRule lambdaFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution universeEquality imageElimination baseClosed imageMemberEquality sqequalAxiom lessCases setEquality divideEquality remainderEquality impliesFunctionality

Latex:
\mforall{}f:\mBbbZ{}  {}\mrightarrow{}  \mBbbZ{}.  2-regular-seq(regularize(f))

Date html generated: 2016_05_18-AM-10_51_02
Last ObjectModification: 2016_01_17-AM-00_19_19

Theory : reals

Home Index