Conservative definition
Parameters: ab, ac, L, bb, bc, M, i, n
∃ x. ∃ y. (∀ z. S z ≤ S i → ∃ m. S m ≤ S (S z · y) ∧ (∃ k. x = k · S (S z · y) + m) ∧ (∃ k. ∃ j. ∃ u. z + k = i ∧ ((S z ≤ L ∧ (S j ≤ S (S z · ac) ∧ (∃ v. ab = v · S (S z · ac) + j)) ∨ L ≤ z ∧ j = 0) ∧ ((S k ≤ M ∧ (S u ≤ S (S k · bc) ∧ (∃ v. bb = v · S (S k · bc) + u)) ∨ M ≤ k ∧ u = 0) ∧ m = j · u)))) ∧ (∃ z. ∃ m. 1 ≤ S (1 · m) ∧ (∃ k. z = k · S (1 · m) + 0) ∧ (S n ≤ S (S S i · m) ∧ (∃ k. z = k · S (S S i · m) + n) ∧ (∀ k. S k ≤ S i → ∃ j. ∃ u. ∃ v. S j ≤ S (S k · y) ∧ (∃ w. x = w · S (S k · y) + j) ∧ (S u ≤ S (S k · m) ∧ (∃ w. z = w · S (S k · m) + u) ∧ (S v ≤ S (S S k · m) ∧ (∃ w. z = w · S (S S k · m) + v) ∧ v = u + j)))))Definition prerequisites
Theorem uses (notation, not proof premises)
AP037 · AP038 · AP040 · CV007 · CV010 · CV013 · CV014 · CV015 · CV016 · CV017 · CV018 · CV021 · CV024 · CV027 · CV028 · CV029 · CV031 · CV034 · CV042 · CV045 · CV047 · CV050