Conservative definition
Parameters: k, d, s, D, ab, ac, x, p
(∃ y. ∃ z. (∀ n. S n ≤ k → 3 ≤ S (S n · z) ∧ (∃ m. y = m · S (S n · z) + 2)) ∧ (∃ n. ∃ m. 2 ≤ S (1 · m) ∧ (∃ i. n = i · S (1 · m) + 1) ∧ (S d ≤ S (S k · m) ∧ (∃ i. n = i · S (S k · m) + d) ∧ (∀ i. S i ≤ k → ∃ j. ∃ u. ∃ v. S j ≤ S (S i · z) ∧ (∃ w. y = w · S (S i · z) + j) ∧ (S u ≤ S (S i · m) ∧ (∃ w. n = w · S (S i · m) + u) ∧ (S v ≤ S (S S i · m) ∧ (∃ w. n = w · S (S S i · m) + v) ∧ v = u · j)))))) ∧ (s · s ≤ 2 · (d · d) ∧ S (2 · (d · d)) ≤ S s · S s) ∧ ((∀ y. ∀ z. S y ≤ S (2 · k) → S z ≤ S (S y · ac) ∧ (∃ n. ab = n · S (S y · ac) + z) → (∃ n. y = 2 · n ∧ z = 0) ∨ (∃ n. y = S (2 · n) ∧ y · z = 2 · D)) ∧ ((∃ y. ∃ z. 1 ≤ S (1 · z) ∧ (∃ n. y = n · S (1 · z) + 0) ∧ (∀ n. S n ≤ S (2 · k) → ∃ m. ∃ i. S m ≤ S (S n · z) ∧ (∃ j. y = j · S (S n · z) + m) ∧ (S i ≤ S (S n · ac) ∧ (∃ j. ab = j · S (S n · ac) + i) ∧ (S (3 · m + i) ≤ S (S S n · z) ∧ (∃ j. y = j · S (S S n · z) + (3 · m + i))))) ∧ (S x ≤ S (S S (2 · k) · z) ∧ (∃ n. y = n · S (S S (2 · k) · z) + x))) ∧ (∃ y. ∃ z. (∀ n. S n ≤ S (2 · k) → 4 ≤ S (S n · z) ∧ (∃ m. y = m · S (S n · z) + 3)) ∧ (∃ n. ∃ m. 2 ≤ S (1 · m) ∧ (∃ i. n = i · S (1 · m) + 1) ∧ (S p ≤ S (S S (2 · k) · m) ∧ (∃ i. n = i · S (S S (2 · k) · m) + p) ∧ (∀ i. S i ≤ S (2 · k) → ∃ j. ∃ u. ∃ v. S j ≤ S (S i · z) ∧ (∃ w. y = w · S (S i · z) + j) ∧ (S u ≤ S (S i · m) ∧ (∃ w. n = w · S (S i · m) + u) ∧ (S v ≤ S (S S i · m) ∧ (∃ w. n = w · S (S S i · m) + v) ∧ v = u · j))))))))Definition prerequisites
ND0446 · ND0425 · ND0437 · PD0020