Nuprl Definition : first-m-not-reg

We can search for the first place, up to bound k,
where sequence s is not 2-regular.
We either locate the first failure of 2-regularity
or we find that the sequence is at least 3-regular up to k.
(see Error :first-m-not-reg-property). ⋅

first-m-not-reg(d;s;k) == search(k;λn.m-not-reg(d;s;n))

Definitions occuring in Statement : m-not-reg: m-not-reg(d;s;n), search: search(k;P), lambda: λx.A[x]
Definitions occuring in definition : search: search(k;P), lambda: λx.A[x], m-not-reg: m-not-reg(d;s;n)
FDL editor aliases : first-m-not-reg

Latex:
first-m-not-reg(d;s;k) == search(k;\mlambda{}n.m-not-reg(d;s;n)) Date html generated: 2019_10_30-AM-07_01_32 Last ObjectModification: 2019_10_11-PM-01_00_18 Theory : reals Home Index