Conservative definition
Parameters: ab, ac, o, t, ub, uc, N
∀ x. ∀ y. S x ≤ N → S y ≤ S (S x · uc) ∧ (∃ z. ub = z · S (S x · uc) + y) → S y ≤ S (S (o + t · x) · ac) ∧ (∃ z. ab = z · S (S (o + t · x) · ac) + y)Definition prerequisites
Theorem uses (notation, not proof premises)
AP016 · AP017 · AP019 · AP020 · AP052 · AP054 · CV062 · CV064 · CV075 · CV076 · CV077 · CV080 · CV082 · CV084 · CV087 · CV088 · CV090