Conservative definition
Parameters: ab, ac, t, hb, hc, k
∃ x. ∃ y. S x ≤ S (S k · hc) ∧ (∃ z. hb = z · S (S k · hc) + x) ∧ (S y ≤ S (S k · ac) ∧ (∃ z. ab = z · S (S k · ac) + y) ∧ (S (t · x + y) ≤ S (S S k · hc) ∧ (∃ z. hb = z · S (S S k · hc) + (t · x + y))))