Conservative definition
Parameters: ab, ac, L, bb, bc, M, N, v, z
∃ x. ∃ y. v = S N · x + y ∧ (S y ≤ S N ∧ ((∃ n. ∃ m. ∃ k. y + n = x ∧ ((S y ≤ L ∧ (S m ≤ S (S y · ac) ∧ (∃ i. ab = i · S (S y · ac) + m)) ∨ L ≤ y ∧ m = 0) ∧ ((S n ≤ M ∧ (S k ≤ S (S n · bc) ∧ (∃ i. bb = i · S (S n · bc) + k)) ∨ M ≤ n ∧ k = 0) ∧ z = m · k))) ∨ S x ≤ y ∧ z = 0))