Conservative definition
Parameters: pb, pc, qb, qc, t, H, vb, vc, K
∀ x. S x ≤ K → ∃ y. ∃ z. ∃ n. S y ≤ S (S x · pc) ∧ (∃ m. pb = m · S (S x · pc) + y) ∧ (S z ≤ S (S x · qc) ∧ (∃ m. qb = m · S (S x · qc) + z)) ∧ ((∃ m. ∃ k. 1 ≤ S (1 · k) ∧ (∃ i. m = i · S (1 · k) + 0) ∧ (∀ i. S i ≤ H → ∃ j. ∃ u. S j ≤ S (S i · k) ∧ (∃ v. m = v · S (S i · k) + j) ∧ (S u ≤ S (S i · z) ∧ (∃ v. y = v · S (S i · z) + u) ∧ (S (t · j + u) ≤ S (S S i · k) ∧ (∃ v. m = v · S (S S i · k) + (t · j + u))))) ∧ (S n ≤ S (S H · k) ∧ (∃ i. m = i · S (S H · k) + n))) ∧ (S n ≤ S (S x · vc) ∧ (∃ m. vb = m · S (S x · vc) + n)))Definition prerequisites
PD0002 · ND0405 · ND0437 · PD0013