Conservative definition
Parameters: H, wb, wc, pb, pc, qb, qc, tb, tc, vb, vc, K
(∃ x. ∃ y. S x ≤ S (1 · tc) ∧ (∃ z. tb = z · S (1 · tc) + x) ∧ (S y ≤ S (1 · vc) ∧ (∃ z. vb = z · S (1 · vc) + y)) ∧ (∀ z. S z ≤ H → 1 ≤ S (S z · y) ∧ (∃ n. x = n · S (S z · y) + 0))) ∧ (∀ x. S x ≤ K → ∃ y. ∃ z. ∃ n. ∃ m. ∃ k. ∃ i. ∃ j. S y ≤ S (S x · pc) ∧ (∃ u. pb = u · S (S x · pc) + y) ∧ (S z ≤ S (S x · qc) ∧ (∃ u. qb = u · S (S x · qc) + z)) ∧ (S n ≤ S (S x · tc) ∧ (∃ u. tb = u · S (S x · tc) + n) ∧ (S m ≤ S (S x · vc) ∧ (∃ u. vb = u · S (S x · vc) + m)) ∧ (S k ≤ S (S S x · tc) ∧ (∃ u. tb = u · S (S S x · tc) + k) ∧ (S i ≤ S (S S x · vc) ∧ (∃ u. vb = u · S (S S x · vc) + i)) ∧ (S j ≤ S (S x · wc) ∧ (∃ u. wb = u · S (S x · wc) + j) ∧ (∀ u. ∀ v. ∀ w. ∀ x0. S u ≤ H → S v ≤ S (S u · m) ∧ (∃ x1. n = x1 · S (S u · m) + v) → S w ≤ S (S u · z) ∧ (∃ x1. y = x1 · S (S u · z) + w) → S x0 ≤ S (S u · i) ∧ (∃ x1. k = x1 · S (S u · i) + x0) → 1 · x0 = 1 · v + j · w)))))Definition prerequisites
ND0405 · ND0419 · PD0002 · ND0420
Theorem uses (notation, not proof premises)
CV019 · CV021 · CV023 · CV024 · CV028 · CV029 · CV031 · CV034 · CV052 · CV060 · CV061 · CV074 · CV076 · CV077 · CV078 · CV079 · CV080 · CV081