Conservative definition
Parameters: wb, wc, vb, vc, zb, zc, K
∀ x. ∀ y. ∀ z. ∀ n. S x ≤ K → S y ≤ S (S x · wc) ∧ (∃ m. wb = m · S (S x · wc) + y) → S z ≤ S (S x · vc) ∧ (∃ m. vb = m · S (S x · vc) + z) → S n ≤ S (S x · zc) ∧ (∃ m. zb = m · S (S x · zc) + n) → n = y · zDefinition prerequisites
Theorem uses (notation, not proof premises)
CV060 · CV061 · CV073 · CV074 · CV076 · CV077 · CV081 · CV085