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