Conservative definition
Parameters: d, N, wb, wc
2 ≤ S (S N · wc) ∧ (∃ x. wb = x · S (S N · wc) + 1) ∧ (∀ x. ∀ y. ∀ z. S x ≤ N → S y ≤ S (S x · wc) ∧ (∃ n. wb = n · S (S x · wc) + y) → S z ≤ S (S S x · wc) ∧ (∃ n. wb = n · S (S S x · wc) + z) → y = S x · d · z)Definition prerequisites
Theorem uses (notation, not proof premises)
AP026 · AP044 · AP047 · AP050 · AP058 · AP066 · AP067 · AP086 · AP091 · AP092 · CV022 · CV024 · CV028 · CV029 · CV030 · CV031 · CV034 · CV070 · CV071 · CV073 · CV074 · CV076 · CV077 · CV080 · CV085