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