Conservative definition
Parameters: ab, ac, L, H, pb, pc, qb, qc, K
(∃ x. ∃ y. S x ≤ S (1 · pc) ∧ (∃ z. pb = z · S (1 · pc) + x) ∧ (S y ≤ S (1 · qc) ∧ (∃ z. qb = z · S (1 · qc) + y)) ∧ (∀ z. S z ≤ H → ∃ n. S n ≤ S (S z · y) ∧ (∃ m. x = m · S (S z · y) + n) ∧ (z = 0 ∧ n = 1 ∨ (∃ m. z = S m ∧ n = 0)))) ∧ (∀ x. S x ≤ K → ∃ y. ∃ z. ∃ n. ∃ m. S y ≤ S (S x · pc) ∧ (∃ k. pb = k · S (S x · pc) + y) ∧ (S z ≤ S (S x · qc) ∧ (∃ k. qb = k · S (S x · qc) + z)) ∧ (S n ≤ S (S S x · pc) ∧ (∃ k. pb = k · S (S S x · pc) + n) ∧ (S m ≤ S (S S x · qc) ∧ (∃ k. qb = k · S (S S x · qc) + m)) ∧ (∀ k. S k ≤ H → ∃ i. S i ≤ S (S k · m) ∧ (∃ j. n = j · S (S k · m) + i) ∧ (∃ j. ∃ u. (∀ v. S v ≤ S k → ∃ w. S w ≤ S (S v · u) ∧ (∃ x0. j = x0 · S (S v · u) + w) ∧ (∃ x0. ∃ x1. ∃ x2. v + x0 = k ∧ ((S v ≤ L ∧ (S x1 ≤ S (S v · ac) ∧ (∃ x3. ab = x3 · S (S v · ac) + x1)) ∨ L ≤ v ∧ x1 = 0) ∧ ((S x0 ≤ H ∧ (S x2 ≤ S (S x0 · z) ∧ (∃ x3. y = x3 · S (S x0 · z) + x2)) ∨ H ≤ x0 ∧ x2 = 0) ∧ w = x1 · x2)))) ∧ (∃ v. ∃ w. 1 ≤ S (1 · w) ∧ (∃ x0. v = x0 · S (1 · w) + 0) ∧ (S i ≤ S (S S k · w) ∧ (∃ x0. v = x0 · S (S S k · w) + i) ∧ (∀ x0. S x0 ≤ S k → ∃ 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)))))))))Definition prerequisites
ND0405 · ND0404 · PD0002 · ND0406
Theorem uses (notation, not proof premises)
CV004 · CV005 · CV017 · CV021 · CV024 · CV028 · CV029 · CV031 · CV034 · CV051 · CV052 · CV054 · CV058 · CV061 · CV074 · CV076 · CV077 · CV079 · CV080 · CV081