Conservative definition
Parameters: ab, ac, bb, bc, cb, cc, db, dc, L, H
∀ x. ∀ y. ∀ z. ∀ n. ∀ m. S x ≤ L → S y ≤ S (S x · ac) ∧ (∃ k. ab = k · S (S x · ac) + y) ∧ (S z ≤ S (S x · bc) ∧ (∃ k. bb = k · S (S x · bc) + z) ∧ (S n ≤ S (S x · cc) ∧ (∃ k. cb = k · S (S x · cc) + n) ∧ (S m ≤ S (S x · dc) ∧ (∃ k. db = k · S (S x · dc) + m)))) → ∃ k. k = y + z + 2 · (n + m) ∧ k ≤ H