Conservative definition
Parameters: k, d, s, D, ab, ac, x, p, wb, wc, tb, tc, w0, f, h, y
(∃ z. ∃ n. (∀ m. S m ≤ k → 3 ≤ S (S m · n) ∧ (∃ i. z = i · S (S m · n) + 2)) ∧ (∃ m. ∃ i. 2 ≤ S (1 · i) ∧ (∃ j. m = j · S (1 · i) + 1) ∧ (S d ≤ S (S k · i) ∧ (∃ j. m = j · S (S k · i) + d) ∧ (∀ j. S j ≤ k → ∃ u. ∃ v. ∃ w. S u ≤ S (S j · n) ∧ (∃ x0. z = x0 · S (S j · n) + u) ∧ (S v ≤ S (S j · i) ∧ (∃ x0. m = x0 · S (S j · i) + v) ∧ (S w ≤ S (S S j · i) ∧ (∃ x0. m = x0 · S (S S j · i) + w) ∧ w = v · u)))))) ∧ (s · s ≤ 2 · (d · d) ∧ S (2 · (d · d)) ≤ S s · S s) ∧ ((∀ z. ∀ n. S z ≤ S (2 · k) → S n ≤ S (S z · ac) ∧ (∃ m. ab = m · S (S z · ac) + n) → (∃ m. z = 2 · m ∧ n = 0) ∨ (∃ m. z = S (2 · m) ∧ z · n = 2 · D)) ∧ ((∃ z. ∃ n. 1 ≤ S (1 · n) ∧ (∃ m. z = m · S (1 · n) + 0) ∧ (∀ m. S m ≤ S (2 · k) → ∃ i. ∃ j. S i ≤ S (S m · n) ∧ (∃ u. z = u · S (S m · n) + i) ∧ (S j ≤ S (S m · ac) ∧ (∃ u. ab = u · S (S m · ac) + j) ∧ (S (3 · i + j) ≤ S (S S m · n) ∧ (∃ u. z = u · S (S S m · n) + (3 · i + j))))) ∧ (S x ≤ S (S S (2 · k) · n) ∧ (∃ m. z = m · S (S S (2 · k) · n) + x))) ∧ (∃ z. ∃ n. (∀ m. S m ≤ S (2 · k) → 4 ≤ S (S m · n) ∧ (∃ i. z = i · S (S m · n) + 3)) ∧ (∃ m. ∃ i. 2 ≤ S (1 · i) ∧ (∃ j. m = j · S (1 · i) + 1) ∧ (S p ≤ S (S S (2 · k) · i) ∧ (∃ j. m = j · S (S S (2 · k) · i) + p) ∧ (∀ j. S j ≤ S (2 · k) → ∃ u. ∃ v. ∃ w. S u ≤ S (S j · n) ∧ (∃ x0. z = x0 · S (S j · n) + u) ∧ (S v ≤ S (S j · i) ∧ (∃ x0. m = x0 · S (S j · i) + v) ∧ (S w ≤ S (S S j · i) ∧ (∃ x0. m = x0 · S (S S j · i) + w) ∧ w = v · u)))))))) ∧ (2 ≤ S (S (k + 2) · wc) ∧ (∃ z. wb = z · S (S (k + 2) · wc) + 1) ∧ (∀ z. ∀ n. ∀ m. S z ≤ k + 2 → S n ≤ S (S z · wc) ∧ (∃ i. wb = i · S (S z · wc) + n) → S m ≤ S (S S z · wc) ∧ (∃ i. wb = i · S (S S z · wc) + m) → n = S z · (D · p · s) · m) ∧ ((∀ z. ∀ n. ∀ m. ∀ i. S z ≤ S (k + 2) → S n ≤ S (S z · wc) ∧ (∃ j. wb = j · S (S z · wc) + n) → (∃ j. ∃ u. (∀ v. S v ≤ z → S (3 · x · d) ≤ S (S v · u) ∧ (∃ w. j = w · S (S v · u) + 3 · x · d)) ∧ (∃ v. ∃ w. 2 ≤ S (1 · w) ∧ (∃ x0. v = x0 · S (1 · w) + 1) ∧ (S m ≤ S (S z · w) ∧ (∃ x0. v = x0 · S (S z · w) + m) ∧ (∀ x0. S x0 ≤ z → ∃ x1. ∃ x2. ∃ x3. S x1 ≤ S (S x0 · u) ∧ (∃ x4. j = x4 · S (S x0 · u) + x1) ∧ (S x2 ≤ S (S x0 · w) ∧ (∃ x4. v = x4 · S (S x0 · w) + x2) ∧ (S x3 ≤ S (S S x0 · w) ∧ (∃ x4. v = x4 · S (S S x0 · w) + x3) ∧ x3 = x2 · x1)))))) → S i ≤ S (S z · tc) ∧ (∃ j. tb = j · S (S z · tc) + i) → i = n · m) ∧ (S w0 ≤ S (1 · wc) ∧ (∃ z. wb = z · S (1 · wc) + w0) ∧ (S w0 ≤ S (1 · tc) ∧ (∃ z. tb = z · S (1 · tc) + w0) ∧ ((∃ z. ∃ n. (∀ m. S m ≤ k + 2 → S (1 + m) ≤ S (S m · n) ∧ (∃ i. z = i · S (S m · n) + (1 + m))) ∧ (∃ m. ∃ i. 2 ≤ S (1 · i) ∧ (∃ j. m = j · S (1 · i) + 1) ∧ (S f ≤ S (S (k + 2) · i) ∧ (∃ j. m = j · S (S (k + 2) · i) + f) ∧ (∀ j. S j ≤ k + 2 → ∃ u. ∃ v. ∃ w. S u ≤ S (S j · n) ∧ (∃ x0. z = x0 · S (S j · n) + u) ∧ (S v ≤ S (S j · i) ∧ (∃ x0. m = x0 · S (S j · i) + v) ∧ (S w ≤ S (S S j · i) ∧ (∃ x0. m = x0 · S (S S j · i) + w) ∧ w = v · u)))))) ∧ ((∃ z. ∃ n. (∀ m. S m ≤ k + 2 → S (D · p · s) ≤ S (S m · n) ∧ (∃ i. z = i · S (S m · n) + D · p · s)) ∧ (∃ m. ∃ i. 2 ≤ S (1 · i) ∧ (∃ j. m = j · S (1 · i) + 1) ∧ (S h ≤ S (S (k + 2) · i) ∧ (∃ j. m = j · S (S (k + 2) · i) + h) ∧ (∀ j. S j ≤ k + 2 → ∃ u. ∃ v. ∃ w. S u ≤ S (S j · n) ∧ (∃ x0. z = x0 · S (S j · n) + u) ∧ (S v ≤ S (S j · i) ∧ (∃ x0. m = x0 · S (S j · i) + v) ∧ (S w ≤ S (S S j · i) ∧ (∃ x0. m = x0 · S (S S j · i) + w) ∧ w = v · u)))))) ∧ (w0 = f · h ∧ (∃ z. ∃ n. 1 ≤ S (1 · n) ∧ (∃ m. z = m · S (1 · n) + 0) ∧ (S y ≤ S (S S (k + 2) · n) ∧ (∃ m. z = m · S (S S (k + 2) · n) + y) ∧ (∀ m. S m ≤ S (k + 2) → ∃ i. ∃ j. ∃ u. S i ≤ S (S m · tc) ∧ (∃ v. tb = v · S (S m · tc) + 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))))))))))))Definition prerequisites
ND0447 · ND0423 · ND0442 · PD0013 · PD0023 · PD0020 · PD0015
Theorem uses (notation, not proof premises)
AP002 · AP004 · AP005 · AP009 · AP012 · AP013 · AP015 · AP021 · AP023 · AP027 · AP094 · AP095