Conservative definition
Parameters: pb, pc, qb, qc, k, ub, uc
S ub ≤ S (S k · pc) ∧ (∃ x. pb = x · S (S k · pc) + ub) ∧ (S uc ≤ S (S k · qc) ∧ (∃ x. qb = x · S (S k · qc) + uc))Definition prerequisites
Theorem uses (notation, not proof premises)
CV005 · CV017 · CV021 · CV023 · CV024 · CV028 · CV029 · CV031 · CV034 · CV051 · CV052 · CV054 · CV058 · CV059 · CV060 · CV061 · CV074 · CV076 · CV077 · CV078 · CV079 · CV080 · CV081