Conservative definition
Parameters: H, wb, wc, pb, pc, qb, qc, tb, tc, vb, vc, k
∃ x. ∃ y. ∃ z. ∃ n. ∃ m. ∃ i. ∃ j. S x ≤ S (S k · pc) ∧ (∃ u. pb = u · S (S k · pc) + x) ∧ (S y ≤ S (S k · qc) ∧ (∃ u. qb = u · S (S k · qc) + y)) ∧ (S z ≤ S (S k · tc) ∧ (∃ u. tb = u · S (S k · tc) + z) ∧ (S n ≤ S (S k · vc) ∧ (∃ u. vb = u · S (S k · vc) + n)) ∧ (S m ≤ S (S S k · tc) ∧ (∃ u. tb = u · S (S S k · tc) + m) ∧ (S i ≤ S (S S k · vc) ∧ (∃ u. vb = u · S (S S k · vc) + i)) ∧ (S j ≤ S (S k · wc) ∧ (∃ u. wb = u · S (S k · wc) + j) ∧ (∀ u. ∀ v. ∀ w. ∀ x0. S u ≤ H → S v ≤ S (S u · n) ∧ (∃ x1. z = x1 · S (S u · n) + v) → S w ≤ S (S u · y) ∧ (∃ x1. x = x1 · S (S u · y) + w) → S x0 ≤ S (S u · i) ∧ (∃ x1. m = x1 · S (S u · i) + x0) → 1 · x0 = 1 · v + j · w))))