Conservative definition
Parameters: ab, ac, L, H, pb, pc, qb, qc, k
∃ x. ∃ y. ∃ z. ∃ n. S x ≤ S (S k · pc) ∧ (∃ m. pb = m · S (S k · pc) + x) ∧ (S y ≤ S (S k · qc) ∧ (∃ m. qb = m · S (S k · qc) + y)) ∧ (S z ≤ S (S S k · pc) ∧ (∃ m. pb = m · S (S S k · pc) + z) ∧ (S n ≤ S (S S k · qc) ∧ (∃ m. qb = m · S (S S k · qc) + n)) ∧ (∀ m. S m ≤ H → ∃ i. S i ≤ S (S m · n) ∧ (∃ j. z = j · S (S m · n) + i) ∧ (∃ j. ∃ u. (∀ v. S v ≤ S m → ∃ w. S w ≤ S (S v · u) ∧ (∃ x0. j = x0 · S (S v · u) + w) ∧ (∃ x0. ∃ x1. ∃ x2. v + x0 = m ∧ ((S v ≤ L ∧ (S x1 ≤ S (S v · ac) ∧ (∃ x3. ab = x3 · S (S v · ac) + x1)) ∨ L ≤ v ∧ x1 = 0) ∧ ((S x0 ≤ H ∧ (S x2 ≤ S (S x0 · y) ∧ (∃ x3. x = x3 · S (S x0 · y) + x2)) ∨ H ≤ x0 ∧ x2 = 0) ∧ w = x1 · x2)))) ∧ (∃ v. ∃ w. 1 ≤ S (1 · w) ∧ (∃ x0. v = x0 · S (1 · w) + 0) ∧ (S i ≤ S (S S m · w) ∧ (∃ x0. v = x0 · S (S S m · w) + i) ∧ (∀ x0. S x0 ≤ S m → ∃ x1. ∃ x2. ∃ x3. S x1 ≤ S (S x0 · u) ∧ (∃ x4. j = x4 · S (S x0 · u) + x1) ∧ (S x2 ≤ S (S x0 · w) ∧ (∃ x4. v = x4 · S (S x0 · w) + x2) ∧ (S x3 ≤ S (S S x0 · w) ∧ (∃ x4. v = x4 · S (S S x0 · w) + x3) ∧ x3 = x2 + x1))))))))