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