Definition in prerequisite notation
∀ dp_i. Lt(dp_i,l) → ∃ x. ∃ y. ∃ z. BetaAt(b,c,dp_i,x) ∧ (BetaAt(qb,qc,dp_i,y) ∧ (BetaAt(rb,rc,dp_i,z) ∧ DivRem(x,m,y,z)))Only definitions earlier in this acyclic notation graph are used here.
Hygienic expanded first-order definition
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))))The unchanged native kernel never receives this surface symbol. Binder-safe expansion produces only its existing first-order syntax.
Direct definition dependencies
Definitions depending on this notation
none