Conservative definition
Parameters: k, d, s
(∃ x. ∃ y. (∀ z. S z ≤ k → 3 ≤ S (S z · y) ∧ (∃ n. x = n · S (S z · y) + 2)) ∧ (∃ z. ∃ n. 2 ≤ S (1 · n) ∧ (∃ m. z = m · S (1 · n) + 1) ∧ (S d ≤ S (S k · n) ∧ (∃ m. z = m · S (S k · n) + d) ∧ (∀ m. S m ≤ k → ∃ i. ∃ j. ∃ u. S i ≤ S (S m · y) ∧ (∃ v. x = v · S (S m · y) + i) ∧ (S j ≤ S (S m · n) ∧ (∃ v. z = v · S (S m · n) + j) ∧ (S u ≤ S (S S m · n) ∧ (∃ v. z = v · S (S S m · n) + u) ∧ u = j · i)))))) ∧ (s · s ≤ 2 · (d · d) ∧ S (2 · (d · d)) ≤ S s · S s)Definition prerequisites
Theorem uses (notation, not proof premises)
AP025 · AP050 · AP089 · AP090 · AP091 · AP092 · SQ004 · SQ006 · SQ007 · SQ008 · SQ009 · SQ010