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