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 notation, not a theorem, axiom, predicate constant, or kernel rule. The elaboration layer must expand it before proof checking.

Definition neighborhood

Expands using

Used by definitions

Used by theorem statements or local proof propositions