DivisorSum(F,n,z)

((~(((n))=0)) /\ (exists dm_mask_table_lowertier. ((((exists dst_positive_code_lowertiermasktable dst_positive_scale_lowertiermasktable dst_negative_code_lowertiermasktable dst_negative_scale_lowertiermasktable. (((dm_mask_table_lowertier) = (((((dst_positive_code_lowertiermasktable) + (dst_positive_scale_lowertiermasktable)) * S ((dst_positive_code_lowertiermasktable) + (dst_positive_scale_lowertiermasktable)) + ((dst_positive_scale_lowertiermasktable) + (dst_positive_scale_lowertiermasktable))) + (((dst_negative_code_lowertiermasktable) + (dst_negative_scale_lowertiermasktable)) * S ((dst_negative_code_lowertiermasktable) + (dst_negative_scale_lowertiermasktable)) + ((dst_negative_scale_lowertiermasktable) + (dst_negative_scale_lowertiermasktable)))) * S ((((dst_positive_code_lowertiermasktable) + (dst_positive_scale_lowertiermasktable)) * S ((dst_positive_code_lowertiermasktable) + (dst_positive_scale_lowertiermasktable)) + ((dst_positive_scale_lowertiermasktable) + (dst_positive_scale_lowertiermasktable))) + (((dst_negative_code_lowertiermasktable) + (dst_negative_scale_lowertiermasktable)) * S ((dst_negative_code_lowertiermasktable) + (dst_negative_scale_lowertiermasktable)) + ((dst_negative_scale_lowertiermasktable) + (dst_negative_scale_lowertiermasktable)))) + ((((dst_negative_code_lowertiermasktable) + (dst_negative_scale_lowertiermasktable)) * S ((dst_negative_code_lowertiermasktable) + (dst_negative_scale_lowertiermasktable)) + ((dst_negative_scale_lowertiermasktable) + (dst_negative_scale_lowertiermasktable))) + (((dst_negative_code_lowertiermasktable) + (dst_negative_scale_lowertiermasktable)) * S ((dst_negative_code_lowertiermasktable) + (dst_negative_scale_lowertiermasktable)) + ((dst_negative_scale_lowertiermasktable) + (dst_negative_scale_lowertiermasktable)))))) /\ (forall dst_index_lowertiermasktable. (exists pvs_le_gap_lowertiermasktabledomain. pvs_le_gap_lowertiermasktabledomain + (dst_index_lowertiermasktable) = ((n))) -> exists dst_positive_lowertiermasktable dst_negative_lowertiermasktable dst_value_lowertiermasktable. ((((exists ff_h_pvs_lowertiermasktableentrypositive. ff_h_pvs_lowertiermasktableentrypositive + S (dst_positive_lowertiermasktable) = S ((S (dst_index_lowertiermasktable)) * dst_positive_scale_lowertiermasktable)) /\ exists ff_q_pvs_lowertiermasktableentrypositive. dst_positive_code_lowertiermasktable = ff_q_pvs_lowertiermasktableentrypositive * S ((S (dst_index_lowertiermasktable)) * dst_positive_scale_lowertiermasktable) + (dst_positive_lowertiermasktable))) /\ (((((exists ff_h_pvs_lowertiermasktableentrynegative. ff_h_pvs_lowertiermasktableentrynegative + S (dst_negative_lowertiermasktable) = S ((S (dst_index_lowertiermasktable)) * dst_negative_scale_lowertiermasktable)) /\ exists ff_q_pvs_lowertiermasktableentrynegative. dst_negative_code_lowertiermasktable = ff_q_pvs_lowertiermasktableentrynegative * S ((S (dst_index_lowertiermasktable)) * dst_negative_scale_lowertiermasktable) + (dst_negative_lowertiermasktable))) /\ (exists ge_balance_positive_lowertiermasktableentryvalue ge_balance_negative_lowertiermasktableentryvalue. (((((dst_value_lowertiermasktable) = 2 * (ge_balance_positive_lowertiermasktableentryvalue) /\ (ge_balance_negative_lowertiermasktableentryvalue) = 0) \/ exists ge_signed_half_lowertiermasktableentryvaluedecode. (((dst_value_lowertiermasktable) = 2 * ge_signed_half_lowertiermasktableentryvaluedecode + 1 /\ (ge_balance_positive_lowertiermasktableentryvalue) = 0) /\ (ge_balance_negative_lowertiermasktableentryvalue) = S ge_signed_half_lowertiermasktableentryvaluedecode))) /\ ((dst_positive_lowertiermasktable) + ge_balance_negative_lowertiermasktableentryvalue = (dst_negative_lowertiermasktable) + ge_balance_positive_lowertiermasktableentryvalue))))))))) /\ (forall dm_index_lowertiermask dm_value_lowertiermask. (exists pvs_le_gap_lowertiermaskdomain. pvs_le_gap_lowertiermaskdomain + (dm_index_lowertiermask) = ((n))) -> (exists dst_positive_code_lowertiermasklookup dst_positive_scale_lowertiermasklookup dst_negative_code_lowertiermasklookup dst_negative_scale_lowertiermasklookup dst_positive_lowertiermasklookup dst_negative_lowertiermasklookup. (((dm_mask_table_lowertier) = (((((dst_positive_code_lowertiermasklookup) + (dst_positive_scale_lowertiermasklookup)) * S ((dst_positive_code_lowertiermasklookup) + (dst_positive_scale_lowertiermasklookup)) + ((dst_positive_scale_lowertiermasklookup) + (dst_positive_scale_lowertiermasklookup))) + (((dst_negative_code_lowertiermasklookup) + (dst_negative_scale_lowertiermasklookup)) * S ((dst_negative_code_lowertiermasklookup) + (dst_negative_scale_lowertiermasklookup)) + ((dst_negative_scale_lowertiermasklookup) + (dst_negative_scale_lowertiermasklookup)))) * S ((((dst_positive_code_lowertiermasklookup) + (dst_positive_scale_lowertiermasklookup)) * S ((dst_positive_code_lowertiermasklookup) + (dst_positive_scale_lowertiermasklookup)) + ((dst_positive_scale_lowertiermasklookup) + (dst_positive_scale_lowertiermasklookup))) + (((dst_negative_code_lowertiermasklookup) + (dst_negative_scale_lowertiermasklookup)) * S ((dst_negative_code_lowertiermasklookup) + (dst_negative_scale_lowertiermasklookup)) + ((dst_negative_scale_lowertiermasklookup) + (dst_negative_scale_lowertiermasklookup)))) + ((((dst_negative_code_lowertiermasklookup) + (dst_negative_scale_lowertiermasklookup)) * S ((dst_negative_code_lowertiermasklookup) + (dst_negative_scale_lowertiermasklookup)) + ((dst_negative_scale_lowertiermasklookup) + (dst_negative_scale_lowertiermasklookup))) + (((dst_negative_code_lowertiermasklookup) + (dst_negative_scale_lowertiermasklookup)) * S ((dst_negative_code_lowertiermasklookup) + (dst_negative_scale_lowertiermasklookup)) + ((dst_negative_scale_lowertiermasklookup) + (dst_negative_scale_lowertiermasklookup)))))) /\ (((((exists ff_h_pvs_lowertiermasklookuppositive. ff_h_pvs_lowertiermasklookuppositive + S (dst_positive_lowertiermasklookup) = S ((S (dm_index_lowertiermask)) * dst_positive_scale_lowertiermasklookup)) /\ exists ff_q_pvs_lowertiermasklookuppositive. dst_positive_code_lowertiermasklookup = ff_q_pvs_lowertiermasklookuppositive * S ((S (dm_index_lowertiermask)) * dst_positive_scale_lowertiermasklookup) + (dst_positive_lowertiermasklookup))) /\ (((((exists ff_h_pvs_lowertiermasklookupnegative. ff_h_pvs_lowertiermasklookupnegative + S (dst_negative_lowertiermasklookup) = S ((S (dm_index_lowertiermask)) * dst_negative_scale_lowertiermasklookup)) /\ exists ff_q_pvs_lowertiermasklookupnegative. dst_negative_code_lowertiermasklookup = ff_q_pvs_lowertiermasklookupnegative * S ((S (dm_index_lowertiermask)) * dst_negative_scale_lowertiermasklookup) + (dst_negative_lowertiermasklookup))) /\ (exists ge_balance_positive_lowertiermasklookupvalue ge_balance_negative_lowertiermasklookupvalue. (((((dm_value_lowertiermask) = 2 * (ge_balance_positive_lowertiermasklookupvalue) /\ (ge_balance_negative_lowertiermasklookupvalue) = 0) \/ exists ge_signed_half_lowertiermasklookupvaluedecode. (((dm_value_lowertiermask) = 2 * ge_signed_half_lowertiermasklookupvaluedecode + 1 /\ (ge_balance_positive_lowertiermasklookupvalue) = 0) /\ (ge_balance_negative_lowertiermasklookupvalue) = S ge_signed_half_lowertiermasklookupvaluedecode))) /\ ((dst_positive_lowertiermasklookup) + ge_balance_negative_lowertiermasklookupvalue = (dst_negative_lowertiermasklookup) + ge_balance_positive_lowertiermasklookupvalue))))))))) -> ((((~((dm_index_lowertiermask)=0)) /\ (exists dm_quotient_lowertiermaskentry. ((((n))=(dm_index_lowertiermask)*dm_quotient_lowertiermaskentry) /\ (exists dst_positive_code_lowertiermaskentryinput dst_positive_scale_lowertiermaskentryinput dst_negative_code_lowertiermaskentryinput dst_negative_scale_lowertiermaskentryinput dst_positive_lowertiermaskentryinput dst_negative_lowertiermaskentryinput. ((((F)) = (((((dst_positive_code_lowertiermaskentryinput) + (dst_positive_scale_lowertiermaskentryinput)) * S ((dst_positive_code_lowertiermaskentryinput) + (dst_positive_scale_lowertiermaskentryinput)) + ((dst_positive_scale_lowertiermaskentryinput) + (dst_positive_scale_lowertiermaskentryinput))) + (((dst_negative_code_lowertiermaskentryinput) + (dst_negative_scale_lowertiermaskentryinput)) * S ((dst_negative_code_lowertiermaskentryinput) + (dst_negative_scale_lowertiermaskentryinput)) + ((dst_negative_scale_lowertiermaskentryinput) + (dst_negative_scale_lowertiermaskentryinput)))) * S ((((dst_positive_code_lowertiermaskentryinput) + (dst_positive_scale_lowertiermaskentryinput)) * S ((dst_positive_code_lowertiermaskentryinput) + (dst_positive_scale_lowertiermaskentryinput)) + ((dst_positive_scale_lowertiermaskentryinput) + (dst_positive_scale_lowertiermaskentryinput))) + (((dst_negative_code_lowertiermaskentryinput) + (dst_negative_scale_lowertiermaskentryinput)) * S ((dst_negative_code_lowertiermaskentryinput) + (dst_negative_scale_lowertiermaskentryinput)) + ((dst_negative_scale_lowertiermaskentryinput) + (dst_negative_scale_lowertiermaskentryinput)))) + ((((dst_negative_code_lowertiermaskentryinput) + (dst_negative_scale_lowertiermaskentryinput)) * S ((dst_negative_code_lowertiermaskentryinput) + (dst_negative_scale_lowertiermaskentryinput)) + ((dst_negative_scale_lowertiermaskentryinput) + (dst_negative_scale_lowertiermaskentryinput))) + (((dst_negative_code_lowertiermaskentryinput) + (dst_negative_scale_lowertiermaskentryinput)) * S ((dst_negative_code_lowertiermaskentryinput) + (dst_negative_scale_lowertiermaskentryinput)) + ((dst_negative_scale_lowertiermaskentryinput) + (dst_negative_scale_lowertiermaskentryinput)))))) /\ (((((exists ff_h_pvs_lowertiermaskentryinputpositive. ff_h_pvs_lowertiermaskentryinputpositive + S (dst_positive_lowertiermaskentryinput) = S ((S (dm_index_lowertiermask)) * dst_positive_scale_lowertiermaskentryinput)) /\ exists ff_q_pvs_lowertiermaskentryinputpositive. dst_positive_code_lowertiermaskentryinput = ff_q_pvs_lowertiermaskentryinputpositive * S ((S (dm_index_lowertiermask)) * dst_positive_scale_lowertiermaskentryinput) + (dst_positive_lowertiermaskentryinput))) /\ (((((exists ff_h_pvs_lowertiermaskentryinputnegative. ff_h_pvs_lowertiermaskentryinputnegative + S (dst_negative_lowertiermaskentryinput) = S ((S (dm_index_lowertiermask)) * dst_negative_scale_lowertiermaskentryinput)) /\ exists ff_q_pvs_lowertiermaskentryinputnegative. dst_negative_code_lowertiermaskentryinput = ff_q_pvs_lowertiermaskentryinputnegative * S ((S (dm_index_lowertiermask)) * dst_negative_scale_lowertiermaskentryinput) + (dst_negative_lowertiermaskentryinput))) /\ (exists ge_balance_positive_lowertiermaskentryinputvalue ge_balance_negative_lowertiermaskentryinputvalue. (((((dm_value_lowertiermask) = 2 * (ge_balance_positive_lowertiermaskentryinputvalue) /\ (ge_balance_negative_lowertiermaskentryinputvalue) = 0) \/ exists ge_signed_half_lowertiermaskentryinputvaluedecode. (((dm_value_lowertiermask) = 2 * ge_signed_half_lowertiermaskentryinputvaluedecode + 1 /\ (ge_balance_positive_lowertiermaskentryinputvalue) = 0) /\ (ge_balance_negative_lowertiermaskentryinputvalue) = S ge_signed_half_lowertiermaskentryinputvaluedecode))) /\ ((dst_positive_lowertiermaskentryinput) + ge_balance_negative_lowertiermaskentryinputvalue = (dst_negative_lowertiermaskentryinput) + ge_balance_positive_lowertiermaskentryinputvalue))))))))))))) \/ ((((dm_index_lowertiermask)=0 \/ ~(exists pvs_factor_lowertiermaskentrynondivisor. ((n)) = (dm_index_lowertiermask) * pvs_factor_lowertiermaskentrynondivisor)) /\ ((dm_value_lowertiermask)=0))))))) /\ (exists dst_positive_code_lowertierfold dst_positive_scale_lowertierfold dst_negative_code_lowertierfold dst_negative_scale_lowertierfold dst_positive_sum_lowertierfold dst_negative_sum_lowertierfold. (((dm_mask_table_lowertier) = (((((dst_positive_code_lowertierfold) + (dst_positive_scale_lowertierfold)) * S ((dst_positive_code_lowertierfold) + (dst_positive_scale_lowertierfold)) + ((dst_positive_scale_lowertierfold) + (dst_positive_scale_lowertierfold))) + (((dst_negative_code_lowertierfold) + (dst_negative_scale_lowertierfold)) * S ((dst_negative_code_lowertierfold) + (dst_negative_scale_lowertierfold)) + ((dst_negative_scale_lowertierfold) + (dst_negative_scale_lowertierfold)))) * S ((((dst_positive_code_lowertierfold) + (dst_positive_scale_lowertierfold)) * S ((dst_positive_code_lowertierfold) + (dst_positive_scale_lowertierfold)) + ((dst_positive_scale_lowertierfold) + (dst_positive_scale_lowertierfold))) + (((dst_negative_code_lowertierfold) + (dst_negative_scale_lowertierfold)) * S ((dst_negative_code_lowertierfold) + (dst_negative_scale_lowertierfold)) + ((dst_negative_scale_lowertierfold) + (dst_negative_scale_lowertierfold)))) + ((((dst_negative_code_lowertierfold) + (dst_negative_scale_lowertierfold)) * S ((dst_negative_code_lowertierfold) + (dst_negative_scale_lowertierfold)) + ((dst_negative_scale_lowertierfold) + (dst_negative_scale_lowertierfold))) + (((dst_negative_code_lowertierfold) + (dst_negative_scale_lowertierfold)) * S ((dst_negative_code_lowertierfold) + (dst_negative_scale_lowertierfold)) + ((dst_negative_scale_lowertierfold) + (dst_negative_scale_lowertierfold)))))) /\ (((exists fs_u_dst_lowertierfoldpositive fs_v_dst_lowertierfoldpositive. ((((exists fs_h_dst_lowertierfoldpositive_body_start. fs_h_dst_lowertierfoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_lowertierfoldpositive)) /\ exists fs_q_dst_lowertierfoldpositive_body_start. fs_u_dst_lowertierfoldpositive = fs_q_dst_lowertierfoldpositive_body_start * S ((S (0)) * fs_v_dst_lowertierfoldpositive) + (0))) /\ ((((exists fs_h_dst_lowertierfoldpositive_body_terminal. fs_h_dst_lowertierfoldpositive_body_terminal + S (dst_positive_sum_lowertierfold) = S ((S (S ((n)))) * fs_v_dst_lowertierfoldpositive)) /\ exists fs_q_dst_lowertierfoldpositive_body_terminal. fs_u_dst_lowertierfoldpositive = fs_q_dst_lowertierfoldpositive_body_terminal * S ((S (S ((n)))) * fs_v_dst_lowertierfoldpositive) + (dst_positive_sum_lowertierfold))) /\ forall fs_i_dst_lowertierfoldpositive_body_steps. (exists fs_lt_dst_lowertierfoldpositive_body_steps_bound. fs_lt_dst_lowertierfoldpositive_body_steps_bound + S fs_i_dst_lowertierfoldpositive_body_steps = S ((n))) -> exists fs_a_dst_lowertierfoldpositive_body_steps fs_r_dst_lowertierfoldpositive_body_steps fs_s_dst_lowertierfoldpositive_body_steps. ((((exists fs_h_dst_lowertierfoldpositive_body_steps_summand. fs_h_dst_lowertierfoldpositive_body_steps_summand + S (fs_a_dst_lowertierfoldpositive_body_steps) = S ((S (fs_i_dst_lowertierfoldpositive_body_steps)) * dst_positive_scale_lowertierfold)) /\ exists fs_q_dst_lowertierfoldpositive_body_steps_summand. dst_positive_code_lowertierfold = fs_q_dst_lowertierfoldpositive_body_steps_summand * S ((S (fs_i_dst_lowertierfoldpositive_body_steps)) * dst_positive_scale_lowertierfold) + (fs_a_dst_lowertierfoldpositive_body_steps))) /\ ((((exists fs_h_dst_lowertierfoldpositive_body_steps_partial. fs_h_dst_lowertierfoldpositive_body_steps_partial + S (fs_r_dst_lowertierfoldpositive_body_steps) = S ((S (fs_i_dst_lowertierfoldpositive_body_steps)) * fs_v_dst_lowertierfoldpositive)) /\ exists fs_q_dst_lowertierfoldpositive_body_steps_partial. fs_u_dst_lowertierfoldpositive = fs_q_dst_lowertierfoldpositive_body_steps_partial * S ((S (fs_i_dst_lowertierfoldpositive_body_steps)) * fs_v_dst_lowertierfoldpositive) + (fs_r_dst_lowertierfoldpositive_body_steps))) /\ ((((exists fs_h_dst_lowertierfoldpositive_body_steps_successor. fs_h_dst_lowertierfoldpositive_body_steps_successor + S (fs_s_dst_lowertierfoldpositive_body_steps) = S ((S (S fs_i_dst_lowertierfoldpositive_body_steps)) * fs_v_dst_lowertierfoldpositive)) /\ exists fs_q_dst_lowertierfoldpositive_body_steps_successor. fs_u_dst_lowertierfoldpositive = fs_q_dst_lowertierfoldpositive_body_steps_successor * S ((S (S fs_i_dst_lowertierfoldpositive_body_steps)) * fs_v_dst_lowertierfoldpositive) + (fs_s_dst_lowertierfoldpositive_body_steps))) /\ fs_s_dst_lowertierfoldpositive_body_steps = fs_r_dst_lowertierfoldpositive_body_steps + fs_a_dst_lowertierfoldpositive_body_steps)))))) /\ (((exists fs_u_dst_lowertierfoldnegative fs_v_dst_lowertierfoldnegative. ((((exists fs_h_dst_lowertierfoldnegative_body_start. fs_h_dst_lowertierfoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_lowertierfoldnegative)) /\ exists fs_q_dst_lowertierfoldnegative_body_start. fs_u_dst_lowertierfoldnegative = fs_q_dst_lowertierfoldnegative_body_start * S ((S (0)) * fs_v_dst_lowertierfoldnegative) + (0))) /\ ((((exists fs_h_dst_lowertierfoldnegative_body_terminal. fs_h_dst_lowertierfoldnegative_body_terminal + S (dst_negative_sum_lowertierfold) = S ((S (S ((n)))) * fs_v_dst_lowertierfoldnegative)) /\ exists fs_q_dst_lowertierfoldnegative_body_terminal. fs_u_dst_lowertierfoldnegative = fs_q_dst_lowertierfoldnegative_body_terminal * S ((S (S ((n)))) * fs_v_dst_lowertierfoldnegative) + (dst_negative_sum_lowertierfold))) /\ forall fs_i_dst_lowertierfoldnegative_body_steps. (exists fs_lt_dst_lowertierfoldnegative_body_steps_bound. fs_lt_dst_lowertierfoldnegative_body_steps_bound + S fs_i_dst_lowertierfoldnegative_body_steps = S ((n))) -> exists fs_a_dst_lowertierfoldnegative_body_steps fs_r_dst_lowertierfoldnegative_body_steps fs_s_dst_lowertierfoldnegative_body_steps. ((((exists fs_h_dst_lowertierfoldnegative_body_steps_summand. fs_h_dst_lowertierfoldnegative_body_steps_summand + S (fs_a_dst_lowertierfoldnegative_body_steps) = S ((S (fs_i_dst_lowertierfoldnegative_body_steps)) * dst_negative_scale_lowertierfold)) /\ exists fs_q_dst_lowertierfoldnegative_body_steps_summand. dst_negative_code_lowertierfold = fs_q_dst_lowertierfoldnegative_body_steps_summand * S ((S (fs_i_dst_lowertierfoldnegative_body_steps)) * dst_negative_scale_lowertierfold) + (fs_a_dst_lowertierfoldnegative_body_steps))) /\ ((((exists fs_h_dst_lowertierfoldnegative_body_steps_partial. fs_h_dst_lowertierfoldnegative_body_steps_partial + S (fs_r_dst_lowertierfoldnegative_body_steps) = S ((S (fs_i_dst_lowertierfoldnegative_body_steps)) * fs_v_dst_lowertierfoldnegative)) /\ exists fs_q_dst_lowertierfoldnegative_body_steps_partial. fs_u_dst_lowertierfoldnegative = fs_q_dst_lowertierfoldnegative_body_steps_partial * S ((S (fs_i_dst_lowertierfoldnegative_body_steps)) * fs_v_dst_lowertierfoldnegative) + (fs_r_dst_lowertierfoldnegative_body_steps))) /\ ((((exists fs_h_dst_lowertierfoldnegative_body_steps_successor. fs_h_dst_lowertierfoldnegative_body_steps_successor + S (fs_s_dst_lowertierfoldnegative_body_steps) = S ((S (S fs_i_dst_lowertierfoldnegative_body_steps)) * fs_v_dst_lowertierfoldnegative)) /\ exists fs_q_dst_lowertierfoldnegative_body_steps_successor. fs_u_dst_lowertierfoldnegative = fs_q_dst_lowertierfoldnegative_body_steps_successor * S ((S (S fs_i_dst_lowertierfoldnegative_body_steps)) * fs_v_dst_lowertierfoldnegative) + (fs_s_dst_lowertierfoldnegative_body_steps))) /\ fs_s_dst_lowertierfoldnegative_body_steps = fs_r_dst_lowertierfoldnegative_body_steps + fs_a_dst_lowertierfoldnegative_body_steps)))))) /\ (exists ge_balance_positive_lowertierfoldresult ge_balance_negative_lowertierfoldresult. ((((((z)) = 2 * (ge_balance_positive_lowertierfoldresult) /\ (ge_balance_negative_lowertierfoldresult) = 0) \/ exists ge_signed_half_lowertierfoldresultdecode. ((((z)) = 2 * ge_signed_half_lowertierfoldresultdecode + 1 /\ (ge_balance_positive_lowertierfoldresult) = 0) /\ (ge_balance_negative_lowertierfoldresult) = S ge_signed_half_lowertierfoldresultdecode))) /\ ((dst_positive_sum_lowertierfold) + ge_balance_negative_lowertierfoldresult = (dst_negative_sum_lowertierfold) + ge_balance_positive_lowertierfoldresult))))))))))))

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