Conservative definition
Parameters: ab, ac, t, N, hb, hc
1 ≤ S (1 · hc) ∧ (∃ x. hb = x · S (1 · hc) + 0) ∧ (∀ x. S x ≤ N → ∃ y. ∃ z. S y ≤ S (S x · hc) ∧ (∃ n. hb = n · S (S x · hc) + y) ∧ (S z ≤ S (S x · ac) ∧ (∃ n. ab = n · S (S x · ac) + z) ∧ (S (t · y + z) ≤ S (S S x · hc) ∧ (∃ n. hb = n · S (S S x · hc) + (t · y + z)))))Definition prerequisites
Theorem uses (notation, not proof premises)
CV032 · CV033 · CV034 · CV035 · CV036 · CV037 · CV039 · CV040 · CV049 · CV055 · CV056 · CV057 · CV058 · CV061 · CV074 · CV076 · CV077 · CV080 · CV081