Conservative definition
Parameters: ab, ac, L, bb, bc, M, j, 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. j + z = x ∧ ((S j ≤ L ∧ (S n ≤ S (S j · ac) ∧ (∃ k. ab = k · S (S j · ac) + n)) ∨ L ≤ j ∧ n = 0) ∧ ((S z ≤ M ∧ (S m ≤ S (S z · bc) ∧ (∃ k. bb = k · S (S z · bc) + m)) ∨ M ≤ z ∧ m = 0) ∧ y = n · m))) ∨ S x ≤ j ∧ y = 0