Conservative definition
Parameters: ab, ac, o, s, t, m, n, rb, rc
∀ x. S x ≤ m → ∃ y. S y ≤ S (S x · rc) ∧ (∃ z. rb = z · S (S x · rc) + y) ∧ (∃ z. ∃ k. (∀ i. ∀ j. S i ≤ n → S j ≤ S (S i · k) ∧ (∃ u. z = u · S (S i · k) + j) → S j ≤ S (S (o + s · x + t · i) · ac) ∧ (∃ u. ab = u · S (S (o + s · x + t · i) · ac) + j)) ∧ (∃ i. ∃ j. 1 ≤ S (1 · j) ∧ (∃ u. i = u · S (1 · j) + 0) ∧ (S y ≤ S (S n · j) ∧ (∃ u. i = u · S (S n · j) + y) ∧ (∀ u. S u ≤ n → ∃ v. ∃ w. ∃ x0. S v ≤ S (S u · k) ∧ (∃ x1. z = x1 · S (S u · k) + v) ∧ (S w ≤ S (S u · j) ∧ (∃ x1. i = x1 · S (S u · j) + w) ∧ (S x0 ≤ S (S S u · j) ∧ (∃ x1. i = x1 · S (S S u · j) + x0) ∧ x0 = w + v))))))