Conservative definition
Parameters: ab, ac, L, bb, bc, M, N, gb, gc
∀ x. ∀ y. ∀ z. S x ≤ S N → S y ≤ S N → S z ≤ S (S (S N · x + y) · gc) ∧ (∃ n. gb = n · S (S (S N · x + y) · gc) + z) → (∃ n. ∃ m. ∃ k. y + n = x ∧ ((S y ≤ L ∧ (S m ≤ S (S y · ac) ∧ (∃ i. ab = i · S (S y · ac) + m)) ∨ L ≤ y ∧ m = 0) ∧ ((S n ≤ M ∧ (S k ≤ S (S n · bc) ∧ (∃ i. bb = i · S (S n · bc) + k)) ∨ M ≤ n ∧ k = 0) ∧ z = m · k))) ∨ S x ≤ y ∧ z = 0