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