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