SignedPrefixSum(F,l,z)

exists dst_positive_code_bottomlayer dst_positive_scale_bottomlayer dst_negative_code_bottomlayer dst_negative_scale_bottomlayer dst_positive_sum_bottomlayer dst_negative_sum_bottomlayer. ((((F)) = (((((dst_positive_code_bottomlayer) + (dst_positive_scale_bottomlayer)) * S ((dst_positive_code_bottomlayer) + (dst_positive_scale_bottomlayer)) + ((dst_positive_scale_bottomlayer) + (dst_positive_scale_bottomlayer))) + (((dst_negative_code_bottomlayer) + (dst_negative_scale_bottomlayer)) * S ((dst_negative_code_bottomlayer) + (dst_negative_scale_bottomlayer)) + ((dst_negative_scale_bottomlayer) + (dst_negative_scale_bottomlayer)))) * S ((((dst_positive_code_bottomlayer) + (dst_positive_scale_bottomlayer)) * S ((dst_positive_code_bottomlayer) + (dst_positive_scale_bottomlayer)) + ((dst_positive_scale_bottomlayer) + (dst_positive_scale_bottomlayer))) + (((dst_negative_code_bottomlayer) + (dst_negative_scale_bottomlayer)) * S ((dst_negative_code_bottomlayer) + (dst_negative_scale_bottomlayer)) + ((dst_negative_scale_bottomlayer) + (dst_negative_scale_bottomlayer)))) + ((((dst_negative_code_bottomlayer) + (dst_negative_scale_bottomlayer)) * S ((dst_negative_code_bottomlayer) + (dst_negative_scale_bottomlayer)) + ((dst_negative_scale_bottomlayer) + (dst_negative_scale_bottomlayer))) + (((dst_negative_code_bottomlayer) + (dst_negative_scale_bottomlayer)) * S ((dst_negative_code_bottomlayer) + (dst_negative_scale_bottomlayer)) + ((dst_negative_scale_bottomlayer) + (dst_negative_scale_bottomlayer)))))) /\ (((exists fs_u_dst_bottomlayerpositive fs_v_dst_bottomlayerpositive. ((((exists fs_h_dst_bottomlayerpositive_body_start. fs_h_dst_bottomlayerpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_bottomlayerpositive)) /\ exists fs_q_dst_bottomlayerpositive_body_start. fs_u_dst_bottomlayerpositive = fs_q_dst_bottomlayerpositive_body_start * S ((S (0)) * fs_v_dst_bottomlayerpositive) + (0))) /\ ((((exists fs_h_dst_bottomlayerpositive_body_terminal. fs_h_dst_bottomlayerpositive_body_terminal + S (dst_positive_sum_bottomlayer) = S ((S ((l))) * fs_v_dst_bottomlayerpositive)) /\ exists fs_q_dst_bottomlayerpositive_body_terminal. fs_u_dst_bottomlayerpositive = fs_q_dst_bottomlayerpositive_body_terminal * S ((S ((l))) * fs_v_dst_bottomlayerpositive) + (dst_positive_sum_bottomlayer))) /\ forall fs_i_dst_bottomlayerpositive_body_steps. (exists fs_lt_dst_bottomlayerpositive_body_steps_bound. fs_lt_dst_bottomlayerpositive_body_steps_bound + S fs_i_dst_bottomlayerpositive_body_steps = (l)) -> exists fs_a_dst_bottomlayerpositive_body_steps fs_r_dst_bottomlayerpositive_body_steps fs_s_dst_bottomlayerpositive_body_steps. ((((exists fs_h_dst_bottomlayerpositive_body_steps_summand. fs_h_dst_bottomlayerpositive_body_steps_summand + S (fs_a_dst_bottomlayerpositive_body_steps) = S ((S (fs_i_dst_bottomlayerpositive_body_steps)) * dst_positive_scale_bottomlayer)) /\ exists fs_q_dst_bottomlayerpositive_body_steps_summand. dst_positive_code_bottomlayer = fs_q_dst_bottomlayerpositive_body_steps_summand * S ((S (fs_i_dst_bottomlayerpositive_body_steps)) * dst_positive_scale_bottomlayer) + (fs_a_dst_bottomlayerpositive_body_steps))) /\ ((((exists fs_h_dst_bottomlayerpositive_body_steps_partial. fs_h_dst_bottomlayerpositive_body_steps_partial + S (fs_r_dst_bottomlayerpositive_body_steps) = S ((S (fs_i_dst_bottomlayerpositive_body_steps)) * fs_v_dst_bottomlayerpositive)) /\ exists fs_q_dst_bottomlayerpositive_body_steps_partial. fs_u_dst_bottomlayerpositive = fs_q_dst_bottomlayerpositive_body_steps_partial * S ((S (fs_i_dst_bottomlayerpositive_body_steps)) * fs_v_dst_bottomlayerpositive) + (fs_r_dst_bottomlayerpositive_body_steps))) /\ ((((exists fs_h_dst_bottomlayerpositive_body_steps_successor. fs_h_dst_bottomlayerpositive_body_steps_successor + S (fs_s_dst_bottomlayerpositive_body_steps) = S ((S (S fs_i_dst_bottomlayerpositive_body_steps)) * fs_v_dst_bottomlayerpositive)) /\ exists fs_q_dst_bottomlayerpositive_body_steps_successor. fs_u_dst_bottomlayerpositive = fs_q_dst_bottomlayerpositive_body_steps_successor * S ((S (S fs_i_dst_bottomlayerpositive_body_steps)) * fs_v_dst_bottomlayerpositive) + (fs_s_dst_bottomlayerpositive_body_steps))) /\ fs_s_dst_bottomlayerpositive_body_steps = fs_r_dst_bottomlayerpositive_body_steps + fs_a_dst_bottomlayerpositive_body_steps)))))) /\ (((exists fs_u_dst_bottomlayernegative fs_v_dst_bottomlayernegative. ((((exists fs_h_dst_bottomlayernegative_body_start. fs_h_dst_bottomlayernegative_body_start + S (0) = S ((S (0)) * fs_v_dst_bottomlayernegative)) /\ exists fs_q_dst_bottomlayernegative_body_start. fs_u_dst_bottomlayernegative = fs_q_dst_bottomlayernegative_body_start * S ((S (0)) * fs_v_dst_bottomlayernegative) + (0))) /\ ((((exists fs_h_dst_bottomlayernegative_body_terminal. fs_h_dst_bottomlayernegative_body_terminal + S (dst_negative_sum_bottomlayer) = S ((S ((l))) * fs_v_dst_bottomlayernegative)) /\ exists fs_q_dst_bottomlayernegative_body_terminal. fs_u_dst_bottomlayernegative = fs_q_dst_bottomlayernegative_body_terminal * S ((S ((l))) * fs_v_dst_bottomlayernegative) + (dst_negative_sum_bottomlayer))) /\ forall fs_i_dst_bottomlayernegative_body_steps. (exists fs_lt_dst_bottomlayernegative_body_steps_bound. fs_lt_dst_bottomlayernegative_body_steps_bound + S fs_i_dst_bottomlayernegative_body_steps = (l)) -> exists fs_a_dst_bottomlayernegative_body_steps fs_r_dst_bottomlayernegative_body_steps fs_s_dst_bottomlayernegative_body_steps. ((((exists fs_h_dst_bottomlayernegative_body_steps_summand. fs_h_dst_bottomlayernegative_body_steps_summand + S (fs_a_dst_bottomlayernegative_body_steps) = S ((S (fs_i_dst_bottomlayernegative_body_steps)) * dst_negative_scale_bottomlayer)) /\ exists fs_q_dst_bottomlayernegative_body_steps_summand. dst_negative_code_bottomlayer = fs_q_dst_bottomlayernegative_body_steps_summand * S ((S (fs_i_dst_bottomlayernegative_body_steps)) * dst_negative_scale_bottomlayer) + (fs_a_dst_bottomlayernegative_body_steps))) /\ ((((exists fs_h_dst_bottomlayernegative_body_steps_partial. fs_h_dst_bottomlayernegative_body_steps_partial + S (fs_r_dst_bottomlayernegative_body_steps) = S ((S (fs_i_dst_bottomlayernegative_body_steps)) * fs_v_dst_bottomlayernegative)) /\ exists fs_q_dst_bottomlayernegative_body_steps_partial. fs_u_dst_bottomlayernegative = fs_q_dst_bottomlayernegative_body_steps_partial * S ((S (fs_i_dst_bottomlayernegative_body_steps)) * fs_v_dst_bottomlayernegative) + (fs_r_dst_bottomlayernegative_body_steps))) /\ ((((exists fs_h_dst_bottomlayernegative_body_steps_successor. fs_h_dst_bottomlayernegative_body_steps_successor + S (fs_s_dst_bottomlayernegative_body_steps) = S ((S (S fs_i_dst_bottomlayernegative_body_steps)) * fs_v_dst_bottomlayernegative)) /\ exists fs_q_dst_bottomlayernegative_body_steps_successor. fs_u_dst_bottomlayernegative = fs_q_dst_bottomlayernegative_body_steps_successor * S ((S (S fs_i_dst_bottomlayernegative_body_steps)) * fs_v_dst_bottomlayernegative) + (fs_s_dst_bottomlayernegative_body_steps))) /\ fs_s_dst_bottomlayernegative_body_steps = fs_r_dst_bottomlayernegative_body_steps + fs_a_dst_bottomlayernegative_body_steps)))))) /\ (exists ge_balance_positive_bottomlayerresult ge_balance_negative_bottomlayerresult. ((((((z)) = 2 * (ge_balance_positive_bottomlayerresult) /\ (ge_balance_negative_bottomlayerresult) = 0) \/ exists ge_signed_half_bottomlayerresultdecode. ((((z)) = 2 * ge_signed_half_bottomlayerresultdecode + 1 /\ (ge_balance_positive_bottomlayerresult) = 0) /\ (ge_balance_negative_bottomlayerresult) = S ge_signed_half_bottomlayerresultdecode))) /\ ((dst_positive_sum_bottomlayer) + ge_balance_negative_bottomlayerresult = (dst_negative_sum_bottomlayer) + ge_balance_positive_bottomlayerresult))))))))

The unchanged native kernel never receives this surface symbol. Binder-safe expansion produces only its existing first-order syntax.