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