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