Conservative definition
Parameters: n, up, ud, rb, rc
∃ x. ∃ y. ∃ z. ∃ m. ∃ k. ∃ i. ∃ j. ∃ u. ∃ v. ∃ w. ∃ x0. ∃ x1. ∃ x2. S x ≤ S (1 · rc) ∧ (∃ x3. rb = x3 · S (1 · rc) + x) ∧ (S y ≤ S (2 · rc) ∧ (∃ x3. rb = x3 · S (2 · rc) + y) ∧ (S z ≤ S (3 · rc) ∧ (∃ x3. rb = x3 · S (3 · rc) + z) ∧ (S m ≤ S (4 · rc) ∧ (∃ x3. rb = x3 · S (4 · rc) + m) ∧ (S k ≤ S (5 · rc) ∧ (∃ x3. rb = x3 · S (5 · rc) + k) ∧ (S i ≤ S (6 · rc) ∧ (∃ x3. rb = x3 · S (6 · rc) + i) ∧ (S j ≤ S (7 · rc) ∧ (∃ x3. rb = x3 · S (7 · rc) + j) ∧ (S u ≤ S (8 · rc) ∧ (∃ x3. rb = x3 · S (8 · rc) + u) ∧ (S v ≤ S (9 · rc) ∧ (∃ x3. rb = x3 · S (9 · rc) + v) ∧ (S w ≤ S (10 · rc) ∧ (∃ x3. rb = x3 · S (10 · rc) + w) ∧ (S x0 ≤ S (11 · rc) ∧ (∃ x3. rb = x3 · S (11 · rc) + x0) ∧ (S ud ≤ S (12 · rc) ∧ (∃ x3. rb = x3 · S (12 · rc) + ud) ∧ (S x1 ≤ S (13 · rc) ∧ (∃ x3. rb = x3 · S (13 · rc) + x1) ∧ (S x2 ≤ S (14 · rc) ∧ (∃ x3. rb = x3 · S (14 · rc) + x2) ∧ (S up ≤ S (15 · rc) ∧ (∃ x3. rb = x3 · S (15 · rc) + up))))))))))))))) ∧ ((∃ x3. ∃ x4. (∀ x5. S x5 ≤ S (2 · (n + 8)) → S (1 + x5) ≤ S (S x5 · x4) ∧ (∃ x6. x3 = x6 · S (S x5 · x4) + (1 + x5))) ∧ (∃ x5. ∃ x6. 2 ≤ S (1 · x6) ∧ (∃ x7. x5 = x7 · S (1 · x6) + 1) ∧ (S z ≤ S (S S (2 · (n + 8)) · x6) ∧ (∃ x7. x5 = x7 · S (S S (2 · (n + 8)) · x6) + z) ∧ (∀ x7. S x7 ≤ S (2 · (n + 8)) → ∃ x8. ∃ x9. ∃ x10. S x8 ≤ S (S x7 · x4) ∧ (∃ x11. x3 = x11 · S (S x7 · x4) + x8) ∧ (S x9 ≤ S (S x7 · x6) ∧ (∃ x11. x5 = x11 · S (S x7 · x6) + x9) ∧ (S x10 ≤ S (S S x7 · x6) ∧ (∃ x11. x5 = x11 · S (S S x7 · x6) + x10) ∧ x10 = x9 · x8)))))) ∧ (¬z = 0 ∧ ((∃ x3. ∃ x4. (∀ x5. S x5 ≤ n + 8 → 3 ≤ S (S x5 · x4) ∧ (∃ x6. x3 = x6 · S (S x5 · x4) + 2)) ∧ (∃ x5. ∃ x6. 2 ≤ S (1 · x6) ∧ (∃ x7. x5 = x7 · S (1 · x6) + 1) ∧ (S x ≤ S (S (n + 8) · x6) ∧ (∃ x7. x5 = x7 · S (S (n + 8) · x6) + x) ∧ (∀ x7. S x7 ≤ n + 8 → ∃ x8. ∃ x9. ∃ x10. S x8 ≤ S (S x7 · x4) ∧ (∃ x11. x3 = x11 · S (S x7 · x4) + x8) ∧ (S x9 ≤ S (S x7 · x6) ∧ (∃ x11. x5 = x11 · S (S x7 · x6) + x9) ∧ (S x10 ≤ S (S S x7 · x6) ∧ (∃ x11. x5 = x11 · S (S S x7 · x6) + x10) ∧ x10 = x9 · x8)))))) ∧ (y · y ≤ 2 · (x · x) ∧ S (2 · (x · x)) ≤ S y · S y) ∧ ((∀ x3. ∀ x4. S x3 ≤ S (2 · (n + 8)) → S x4 ≤ S (S x3 · k) ∧ (∃ x5. m = x5 · S (S x3 · k) + x4) → (∃ x5. x3 = 2 · x5 ∧ x4 = 0) ∨ (∃ x5. x3 = S (2 · x5) ∧ x3 · x4 = 2 · z)) ∧ ((∃ x3. ∃ x4. 1 ≤ S (1 · x4) ∧ (∃ x5. x3 = x5 · S (1 · x4) + 0) ∧ (∀ x5. S x5 ≤ S (2 · (n + 8)) → ∃ x6. ∃ x7. S x6 ≤ S (S x5 · x4) ∧ (∃ x8. x3 = x8 · S (S x5 · x4) + x6) ∧ (S x7 ≤ S (S x5 · k) ∧ (∃ x8. m = x8 · S (S x5 · k) + x7) ∧ (S (3 · x6 + x7) ≤ S (S S x5 · x4) ∧ (∃ x8. x3 = x8 · S (S S x5 · x4) + (3 · x6 + x7))))) ∧ (S i ≤ S (S S (2 · (n + 8)) · x4) ∧ (∃ x5. x3 = x5 · S (S S (2 · (n + 8)) · x4) + i))) ∧ (∃ x3. ∃ x4. (∀ x5. S x5 ≤ S (2 · (n + 8)) → 4 ≤ S (S x5 · x4) ∧ (∃ x6. x3 = x6 · S (S x5 · x4) + 3)) ∧ (∃ x5. ∃ x6. 2 ≤ S (1 · x6) ∧ (∃ x7. x5 = x7 · S (1 · x6) + 1) ∧ (S j ≤ S (S S (2 · (n + 8)) · x6) ∧ (∃ x7. x5 = x7 · S (S S (2 · (n + 8)) · x6) + j) ∧ (∀ x7. S x7 ≤ S (2 · (n + 8)) → ∃ x8. ∃ x9. ∃ x10. S x8 ≤ S (S x7 · x4) ∧ (∃ x11. x3 = x11 · S (S x7 · x4) + x8) ∧ (S x9 ≤ S (S x7 · x6) ∧ (∃ x11. x5 = x11 · S (S x7 · x6) + x9) ∧ (S x10 ≤ S (S S x7 · x6) ∧ (∃ x11. x5 = x11 · S (S S x7 · x6) + x10) ∧ x10 = x9 · x8)))))))) ∧ (2 ≤ S (S (n + 8 + 2) · v) ∧ (∃ x3. u = x3 · S (S (n + 8 + 2) · v) + 1) ∧ (∀ x3. ∀ x4. ∀ x5. S x3 ≤ n + 8 + 2 → S x4 ≤ S (S x3 · v) ∧ (∃ x6. u = x6 · S (S x3 · v) + x4) → S x5 ≤ S (S S x3 · v) ∧ (∃ x6. u = x6 · S (S S x3 · v) + x5) → x4 = S x3 · (z · j · y) · x5) ∧ ((∀ x3. ∀ x4. ∀ x5. ∀ x6. S x3 ≤ S (n + 8 + 2) → S x4 ≤ S (S x3 · v) ∧ (∃ x7. u = x7 · S (S x3 · v) + x4) → (∃ x7. ∃ x8. (∀ x9. S x9 ≤ x3 → S (3 · i · x) ≤ S (S x9 · x8) ∧ (∃ x10. x7 = x10 · S (S x9 · x8) + 3 · i · x)) ∧ (∃ x9. ∃ x10. 2 ≤ S (1 · x10) ∧ (∃ x11. x9 = x11 · S (1 · x10) + 1) ∧ (S x5 ≤ S (S x3 · x10) ∧ (∃ x11. x9 = x11 · S (S x3 · x10) + x5) ∧ (∀ x11. S x11 ≤ x3 → ∃ x12. ∃ x13. ∃ x14. S x12 ≤ S (S x11 · x8) ∧ (∃ x15. x7 = x15 · S (S x11 · x8) + x12) ∧ (S x13 ≤ S (S x11 · x10) ∧ (∃ x15. x9 = x15 · S (S x11 · x10) + x13) ∧ (S x14 ≤ S (S S x11 · x10) ∧ (∃ x15. x9 = x15 · S (S S x11 · x10) + x14) ∧ x14 = x13 · x12)))))) → S x6 ≤ S (S x3 · x0) ∧ (∃ x7. w = x7 · S (S x3 · x0) + x6) → x6 = x4 · x5) ∧ (S ud ≤ S (1 · v) ∧ (∃ x3. u = x3 · S (1 · v) + ud) ∧ (S ud ≤ S (1 · x0) ∧ (∃ x3. w = x3 · S (1 · x0) + ud) ∧ ((∃ x3. ∃ x4. (∀ x5. S x5 ≤ n + 8 + 2 → S (1 + x5) ≤ S (S x5 · x4) ∧ (∃ x6. x3 = x6 · S (S x5 · x4) + (1 + x5))) ∧ (∃ x5. ∃ x6. 2 ≤ S (1 · x6) ∧ (∃ x7. x5 = x7 · S (1 · x6) + 1) ∧ (S x1 ≤ S (S (n + 8 + 2) · x6) ∧ (∃ x7. x5 = x7 · S (S (n + 8 + 2) · x6) + x1) ∧ (∀ x7. S x7 ≤ n + 8 + 2 → ∃ x8. ∃ x9. ∃ x10. S x8 ≤ S (S x7 · x4) ∧ (∃ x11. x3 = x11 · S (S x7 · x4) + x8) ∧ (S x9 ≤ S (S x7 · x6) ∧ (∃ x11. x5 = x11 · S (S x7 · x6) + x9) ∧ (S x10 ≤ S (S S x7 · x6) ∧ (∃ x11. x5 = x11 · S (S S x7 · x6) + x10) ∧ x10 = x9 · x8)))))) ∧ ((∃ x3. ∃ x4. (∀ x5. S x5 ≤ n + 8 + 2 → S (z · j · y) ≤ S (S x5 · x4) ∧ (∃ x6. x3 = x6 · S (S x5 · x4) + z · j · y)) ∧ (∃ x5. ∃ x6. 2 ≤ S (1 · x6) ∧ (∃ x7. x5 = x7 · S (1 · x6) + 1) ∧ (S x2 ≤ S (S (n + 8 + 2) · x6) ∧ (∃ x7. x5 = x7 · S (S (n + 8 + 2) · x6) + x2) ∧ (∀ x7. S x7 ≤ n + 8 + 2 → ∃ x8. ∃ x9. ∃ x10. S x8 ≤ S (S x7 · x4) ∧ (∃ x11. x3 = x11 · S (S x7 · x4) + x8) ∧ (S x9 ≤ S (S x7 · x6) ∧ (∃ x11. x5 = x11 · S (S x7 · x6) + x9) ∧ (S x10 ≤ S (S S x7 · x6) ∧ (∃ x11. x5 = x11 · S (S S x7 · x6) + x10) ∧ x10 = x9 · x8)))))) ∧ (ud = x1 · x2 ∧ (∃ x3. ∃ x4. 1 ≤ S (1 · x4) ∧ (∃ x5. x3 = x5 · S (1 · x4) + 0) ∧ (S up ≤ S (S S (n + 8 + 2) · x4) ∧ (∃ x5. x3 = x5 · S (S S (n + 8 + 2) · x4) + up) ∧ (∀ x5. S x5 ≤ S (n + 8 + 2) → ∃ x6. ∃ x7. ∃ x8. S x6 ≤ S (S x5 · x0) ∧ (∃ x9. w = x9 · S (S x5 · x0) + x6) ∧ (S x7 ≤ S (S x5 · x4) ∧ (∃ x9. x3 = x9 · S (S x5 · x4) + x7) ∧ (S x8 ≤ S (S S x5 · x4) ∧ (∃ x9. x3 = x9 · S (S S x5 · x4) + x8) ∧ x8 = x7 + x6)))))))))))) ∧ ¬ud = 0)))