Conservative definition
Parameters: ab, ac, L, bb, bc, M, cb, cc, N
∀ x. S x ≤ N → ∃ y. S y ≤ S (S x · cc) ∧ (∃ z. cb = z · S (S x · cc) + y) ∧ (∃ z. ∃ n. (∀ m. S m ≤ S x → ∃ k. S k ≤ S (S m · n) ∧ (∃ i. z = i · S (S m · n) + k) ∧ (∃ i. ∃ j. ∃ u. m + i = x ∧ ((S m ≤ L ∧ (S j ≤ S (S m · ac) ∧ (∃ v. ab = v · S (S m · ac) + j)) ∨ L ≤ m ∧ j = 0) ∧ ((S i ≤ M ∧ (S u ≤ S (S i · bc) ∧ (∃ v. bb = v · S (S i · bc) + u)) ∨ M ≤ i ∧ u = 0) ∧ k = j · u)))) ∧ (∃ m. ∃ k. 1 ≤ S (1 · k) ∧ (∃ i. m = i · S (1 · k) + 0) ∧ (S y ≤ S (S S x · k) ∧ (∃ i. m = i · S (S S x · k) + y) ∧ (∀ i. S i ≤ S x → ∃ j. ∃ u. ∃ v. S j ≤ S (S i · n) ∧ (∃ w. z = w · S (S i · n) + j) ∧ (S u ≤ S (S i · k) ∧ (∃ w. m = w · S (S i · k) + u) ∧ (S v ≤ S (S S i · k) ∧ (∃ w. m = w · S (S S i · k) + v) ∧ v = u + j))))))Definition prerequisites
Theorem uses (notation, not proof premises)
AP039 · AP041 · AP042 · AP059 · CV003 · CV014 · CV048 · CV049 · CV053 · CV056 · CV057