floor_ceil_division_budget

Exact expanded PA statement

forall n q r s e. (((exists bcs_sqrt_lower_gap_division_bridge_floor. bcs_sqrt_lower_gap_division_bridge_floor + (s) * (s) = (2 * n)) /\ exists bcs_sqrt_upper_gap_division_bridge_floor. bcs_sqrt_upper_gap_division_bridge_floor + S (2 * n) = S (s) * S (s))) -> (((exists bcs_lower_gap_division_bridge_ceil. bcs_lower_gap_division_bridge_ceil + (s * s) = 6 * (e)) /\ exists bcs_upper_gap_division_bridge_ceil. bcs_upper_gap_division_bridge_ceil + S (6 * (e)) = (s * s) + 6)) -> (((2 * (n) = 3 * (q) + (r)) /\ exists bqb_remainder_gap_division_bridge_source. bqb_remainder_gap_division_bridge_source + S (r) = 3)) -> exists c. ((((((q) + (c) = (n)) /\ exists bqb_budget_gap_division_bridge_result. bqb_budget_gap_division_bridge_result + 2 * (n) = 6 * (c))) /\ ((exists bqb_le_gap_division_bridge_ec. bqb_le_gap_division_bridge_ec + (e) = (c)) /\ (exists bqb_le_gap_division_bridge_sum. bqb_le_gap_division_bridge_sum + (q + e) = (n)))) /\ exists bqb_remainder_gap_division_bridge_preserved. bqb_remainder_gap_division_bridge_preserved + S r = 3)