Nuprl Definition : regular-int-seq
The factor ⌜2⌝ on the right of the inequality is essential to prove accelerate_wf⋅
k-regular-seq(f) == ∀n,m:ℕ+. (|(m * (f n)) - n * (f m)| ≤ ((2 * k) * (n + m)))
Definitions occuring in Statement :
absval: |i|,
nat_plus: ℕ+,
le: A ≤ B,
all: ∀x:A. B[x],
apply: f a,
multiply: n * m,
subtract: n - m,
add: n + m,
natural_number: $n
Definitions occuring in definition :
all: ∀x:A. B[x],
nat_plus: ℕ+,
le: A ≤ B,
absval: |i|,
subtract: n - m,
apply: f a,
multiply: n * m,
natural_number: $n,
add: n + m
FDL editor aliases :
k-reg-seq
Latex:
k-regular-seq(f) == \mforall{}n,m:\mBbbN{}\msupplus{}. (|(m * (f n)) - n * (f m)| \mleq{} ((2 * k) * (n + m)))
Date html generated:
2016_07_08-PM-06_30_10
Last ObjectModification:
2015_09_23-AM-09_00_35
Theory : reals
Home
Index