DivisionPrefix

Readable signature

DivisionPrefix(m, b, c, qb, qc, rb, rc, l)

Exact expansion

forall dp_i. (exists dp_index_gap. dp_index_gap + S dp_i = l) -> exists dp_x dp_q dp_r. (((exists ff_h_defined_division_prefix_source. ff_h_defined_division_prefix_source + S (dp_x) = S ((S (dp_i)) * c)) /\ exists ff_q_defined_division_prefix_source. b = ff_q_defined_division_prefix_source * S ((S (dp_i)) * c) + (dp_x))) /\ ((((exists ff_h_defined_division_prefix_quotient. ff_h_defined_division_prefix_quotient + S (dp_q) = S ((S (dp_i)) * qc)) /\ exists ff_q_defined_division_prefix_quotient. qb = ff_q_defined_division_prefix_quotient * S ((S (dp_i)) * qc) + (dp_q))) /\ ((((exists ff_h_defined_division_prefix_remainder. ff_h_defined_division_prefix_remainder + S (dp_r) = S ((S (dp_i)) * rc)) /\ exists ff_q_defined_division_prefix_remainder. rb = ff_q_defined_division_prefix_remainder * S ((S (dp_i)) * rc) + (dp_r))) /\ (dp_x = m * dp_q + dp_r /\ (exists dp_remainder_gap. dp_remainder_gap + S dp_r = m))))

This node is conservative notation, not a theorem, axiom, predicate constant, or kernel rule. Its expansion remains in the unchanged first-order language.

Definition neighborhood

Depends on conservative definitions

Used by conservative definitions

All transitive conservative prerequisites

Used by theorem statements or local proof propositions

Grand-campaign planning vocabulary

Locate DivisionPrefix in the global campaign vocabulary →

Reviewed DivisionPrefix corresponds to blueprint DivisionPrefix with checked argument positions [0, 1, 2, 3, 4, 5, 6, 7].

The global atlas describes planning vocabulary and does not itself certify a definition or theorem. The reviewed expansion and conservative dependency DAG on this page are the actual family-local reading definitions.