signed_divisor_sum_zero_excluded

Exact expanded first-order arithmetic statement

forall F z. (((~((0)=0)) /\ (exists dm_mask_table_sum_zero_excluded. ((((exists dst_positive_code_sum_zero_excludedmasktable dst_positive_scale_sum_zero_excludedmasktable dst_negative_code_sum_zero_excludedmasktable dst_negative_scale_sum_zero_excludedmasktable. (((dm_mask_table_sum_zero_excluded) = (((((dst_positive_code_sum_zero_excludedmasktable) + (dst_positive_scale_sum_zero_excludedmasktable)) * S ((dst_positive_code_sum_zero_excludedmasktable) + (dst_positive_scale_sum_zero_excludedmasktable)) + ((dst_positive_scale_sum_zero_excludedmasktable) + (dst_positive_scale_sum_zero_excludedmasktable))) + (((dst_negative_code_sum_zero_excludedmasktable) + (dst_negative_scale_sum_zero_excludedmasktable)) * S ((dst_negative_code_sum_zero_excludedmasktable) + (dst_negative_scale_sum_zero_excludedmasktable)) + ((dst_negative_scale_sum_zero_excludedmasktable) + (dst_negative_scale_sum_zero_excludedmasktable)))) * S ((((dst_positive_code_sum_zero_excludedmasktable) + (dst_positive_scale_sum_zero_excludedmasktable)) * S ((dst_positive_code_sum_zero_excludedmasktable) + (dst_positive_scale_sum_zero_excludedmasktable)) + ((dst_positive_scale_sum_zero_excludedmasktable) + (dst_positive_scale_sum_zero_excludedmasktable))) + (((dst_negative_code_sum_zero_excludedmasktable) + (dst_negative_scale_sum_zero_excludedmasktable)) * S ((dst_negative_code_sum_zero_excludedmasktable) + (dst_negative_scale_sum_zero_excludedmasktable)) + ((dst_negative_scale_sum_zero_excludedmasktable) + (dst_negative_scale_sum_zero_excludedmasktable)))) + ((((dst_negative_code_sum_zero_excludedmasktable) + (dst_negative_scale_sum_zero_excludedmasktable)) * S ((dst_negative_code_sum_zero_excludedmasktable) + (dst_negative_scale_sum_zero_excludedmasktable)) + ((dst_negative_scale_sum_zero_excludedmasktable) + (dst_negative_scale_sum_zero_excludedmasktable))) + (((dst_negative_code_sum_zero_excludedmasktable) + (dst_negative_scale_sum_zero_excludedmasktable)) * S ((dst_negative_code_sum_zero_excludedmasktable) + (dst_negative_scale_sum_zero_excludedmasktable)) + ((dst_negative_scale_sum_zero_excludedmasktable) + (dst_negative_scale_sum_zero_excludedmasktable)))))) /\ (forall dst_index_sum_zero_excludedmasktable. (exists pvs_le_gap_sum_zero_excludedmasktabledomain. pvs_le_gap_sum_zero_excludedmasktabledomain + (dst_index_sum_zero_excludedmasktable) = (0)) -> exists dst_positive_sum_zero_excludedmasktable dst_negative_sum_zero_excludedmasktable dst_value_sum_zero_excludedmasktable. ((((exists ff_h_pvs_sum_zero_excludedmasktableentrypositive. ff_h_pvs_sum_zero_excludedmasktableentrypositive + S (dst_positive_sum_zero_excludedmasktable) = S ((S (dst_index_sum_zero_excludedmasktable)) * dst_positive_scale_sum_zero_excludedmasktable)) /\ exists ff_q_pvs_sum_zero_excludedmasktableentrypositive. dst_positive_code_sum_zero_excludedmasktable = ff_q_pvs_sum_zero_excludedmasktableentrypositive * S ((S (dst_index_sum_zero_excludedmasktable)) * dst_positive_scale_sum_zero_excludedmasktable) + (dst_positive_sum_zero_excludedmasktable))) /\ (((((exists ff_h_pvs_sum_zero_excludedmasktableentrynegative. ff_h_pvs_sum_zero_excludedmasktableentrynegative + S (dst_negative_sum_zero_excludedmasktable) = S ((S (dst_index_sum_zero_excludedmasktable)) * dst_negative_scale_sum_zero_excludedmasktable)) /\ exists ff_q_pvs_sum_zero_excludedmasktableentrynegative. dst_negative_code_sum_zero_excludedmasktable = ff_q_pvs_sum_zero_excludedmasktableentrynegative * S ((S (dst_index_sum_zero_excludedmasktable)) * dst_negative_scale_sum_zero_excludedmasktable) + (dst_negative_sum_zero_excludedmasktable))) /\ (exists ge_balance_positive_sum_zero_excludedmasktableentryvalue ge_balance_negative_sum_zero_excludedmasktableentryvalue. (((((dst_value_sum_zero_excludedmasktable) = 2 * (ge_balance_positive_sum_zero_excludedmasktableentryvalue) /\ (ge_balance_negative_sum_zero_excludedmasktableentryvalue) = 0) \/ exists ge_signed_half_sum_zero_excludedmasktableentryvaluedecode. (((dst_value_sum_zero_excludedmasktable) = 2 * ge_signed_half_sum_zero_excludedmasktableentryvaluedecode + 1 /\ (ge_balance_positive_sum_zero_excludedmasktableentryvalue) = 0) /\ (ge_balance_negative_sum_zero_excludedmasktableentryvalue) = S ge_signed_half_sum_zero_excludedmasktableentryvaluedecode))) /\ ((dst_positive_sum_zero_excludedmasktable) + ge_balance_negative_sum_zero_excludedmasktableentryvalue = (dst_negative_sum_zero_excludedmasktable) + ge_balance_positive_sum_zero_excludedmasktableentryvalue))))))))) /\ (forall dm_index_sum_zero_excludedmask dm_value_sum_zero_excludedmask. (exists pvs_le_gap_sum_zero_excludedmaskdomain. pvs_le_gap_sum_zero_excludedmaskdomain + (dm_index_sum_zero_excludedmask) = (0)) -> (exists dst_positive_code_sum_zero_excludedmasklookup dst_positive_scale_sum_zero_excludedmasklookup dst_negative_code_sum_zero_excludedmasklookup dst_negative_scale_sum_zero_excludedmasklookup dst_positive_sum_zero_excludedmasklookup dst_negative_sum_zero_excludedmasklookup. (((dm_mask_table_sum_zero_excluded) = (((((dst_positive_code_sum_zero_excludedmasklookup) + (dst_positive_scale_sum_zero_excludedmasklookup)) * S ((dst_positive_code_sum_zero_excludedmasklookup) + (dst_positive_scale_sum_zero_excludedmasklookup)) + ((dst_positive_scale_sum_zero_excludedmasklookup) + (dst_positive_scale_sum_zero_excludedmasklookup))) + (((dst_negative_code_sum_zero_excludedmasklookup) + (dst_negative_scale_sum_zero_excludedmasklookup)) * S ((dst_negative_code_sum_zero_excludedmasklookup) + (dst_negative_scale_sum_zero_excludedmasklookup)) + ((dst_negative_scale_sum_zero_excludedmasklookup) + (dst_negative_scale_sum_zero_excludedmasklookup)))) * S ((((dst_positive_code_sum_zero_excludedmasklookup) + (dst_positive_scale_sum_zero_excludedmasklookup)) * S ((dst_positive_code_sum_zero_excludedmasklookup) + (dst_positive_scale_sum_zero_excludedmasklookup)) + ((dst_positive_scale_sum_zero_excludedmasklookup) + (dst_positive_scale_sum_zero_excludedmasklookup))) + (((dst_negative_code_sum_zero_excludedmasklookup) + (dst_negative_scale_sum_zero_excludedmasklookup)) * S ((dst_negative_code_sum_zero_excludedmasklookup) + (dst_negative_scale_sum_zero_excludedmasklookup)) + ((dst_negative_scale_sum_zero_excludedmasklookup) + (dst_negative_scale_sum_zero_excludedmasklookup)))) + ((((dst_negative_code_sum_zero_excludedmasklookup) + (dst_negative_scale_sum_zero_excludedmasklookup)) * S ((dst_negative_code_sum_zero_excludedmasklookup) + (dst_negative_scale_sum_zero_excludedmasklookup)) + ((dst_negative_scale_sum_zero_excludedmasklookup) + (dst_negative_scale_sum_zero_excludedmasklookup))) + (((dst_negative_code_sum_zero_excludedmasklookup) + (dst_negative_scale_sum_zero_excludedmasklookup)) * S ((dst_negative_code_sum_zero_excludedmasklookup) + (dst_negative_scale_sum_zero_excludedmasklookup)) + ((dst_negative_scale_sum_zero_excludedmasklookup) + (dst_negative_scale_sum_zero_excludedmasklookup)))))) /\ (((((exists ff_h_pvs_sum_zero_excludedmasklookuppositive. ff_h_pvs_sum_zero_excludedmasklookuppositive + S (dst_positive_sum_zero_excludedmasklookup) = S ((S (dm_index_sum_zero_excludedmask)) * dst_positive_scale_sum_zero_excludedmasklookup)) /\ exists ff_q_pvs_sum_zero_excludedmasklookuppositive. dst_positive_code_sum_zero_excludedmasklookup = ff_q_pvs_sum_zero_excludedmasklookuppositive * S ((S (dm_index_sum_zero_excludedmask)) * dst_positive_scale_sum_zero_excludedmasklookup) + (dst_positive_sum_zero_excludedmasklookup))) /\ (((((exists ff_h_pvs_sum_zero_excludedmasklookupnegative. ff_h_pvs_sum_zero_excludedmasklookupnegative + S (dst_negative_sum_zero_excludedmasklookup) = S ((S (dm_index_sum_zero_excludedmask)) * dst_negative_scale_sum_zero_excludedmasklookup)) /\ exists ff_q_pvs_sum_zero_excludedmasklookupnegative. dst_negative_code_sum_zero_excludedmasklookup = ff_q_pvs_sum_zero_excludedmasklookupnegative * S ((S (dm_index_sum_zero_excludedmask)) * dst_negative_scale_sum_zero_excludedmasklookup) + (dst_negative_sum_zero_excludedmasklookup))) /\ (exists ge_balance_positive_sum_zero_excludedmasklookupvalue ge_balance_negative_sum_zero_excludedmasklookupvalue. (((((dm_value_sum_zero_excludedmask) = 2 * (ge_balance_positive_sum_zero_excludedmasklookupvalue) /\ (ge_balance_negative_sum_zero_excludedmasklookupvalue) = 0) \/ exists ge_signed_half_sum_zero_excludedmasklookupvaluedecode. (((dm_value_sum_zero_excludedmask) = 2 * ge_signed_half_sum_zero_excludedmasklookupvaluedecode + 1 /\ (ge_balance_positive_sum_zero_excludedmasklookupvalue) = 0) /\ (ge_balance_negative_sum_zero_excludedmasklookupvalue) = S ge_signed_half_sum_zero_excludedmasklookupvaluedecode))) /\ ((dst_positive_sum_zero_excludedmasklookup) + ge_balance_negative_sum_zero_excludedmasklookupvalue = (dst_negative_sum_zero_excludedmasklookup) + ge_balance_positive_sum_zero_excludedmasklookupvalue))))))))) -> ((((~((dm_index_sum_zero_excludedmask)=0)) /\ (exists dm_quotient_sum_zero_excludedmaskentry. (((0)=(dm_index_sum_zero_excludedmask)*dm_quotient_sum_zero_excludedmaskentry) /\ (exists dst_positive_code_sum_zero_excludedmaskentryinput dst_positive_scale_sum_zero_excludedmaskentryinput dst_negative_code_sum_zero_excludedmaskentryinput dst_negative_scale_sum_zero_excludedmaskentryinput dst_positive_sum_zero_excludedmaskentryinput dst_negative_sum_zero_excludedmaskentryinput. (((F) = (((((dst_positive_code_sum_zero_excludedmaskentryinput) + (dst_positive_scale_sum_zero_excludedmaskentryinput)) * S ((dst_positive_code_sum_zero_excludedmaskentryinput) + (dst_positive_scale_sum_zero_excludedmaskentryinput)) + ((dst_positive_scale_sum_zero_excludedmaskentryinput) + (dst_positive_scale_sum_zero_excludedmaskentryinput))) + (((dst_negative_code_sum_zero_excludedmaskentryinput) + (dst_negative_scale_sum_zero_excludedmaskentryinput)) * S ((dst_negative_code_sum_zero_excludedmaskentryinput) + (dst_negative_scale_sum_zero_excludedmaskentryinput)) + ((dst_negative_scale_sum_zero_excludedmaskentryinput) + (dst_negative_scale_sum_zero_excludedmaskentryinput)))) * S ((((dst_positive_code_sum_zero_excludedmaskentryinput) + (dst_positive_scale_sum_zero_excludedmaskentryinput)) * S ((dst_positive_code_sum_zero_excludedmaskentryinput) + (dst_positive_scale_sum_zero_excludedmaskentryinput)) + ((dst_positive_scale_sum_zero_excludedmaskentryinput) + (dst_positive_scale_sum_zero_excludedmaskentryinput))) + (((dst_negative_code_sum_zero_excludedmaskentryinput) + (dst_negative_scale_sum_zero_excludedmaskentryinput)) * S ((dst_negative_code_sum_zero_excludedmaskentryinput) + (dst_negative_scale_sum_zero_excludedmaskentryinput)) + ((dst_negative_scale_sum_zero_excludedmaskentryinput) + (dst_negative_scale_sum_zero_excludedmaskentryinput)))) + ((((dst_negative_code_sum_zero_excludedmaskentryinput) + (dst_negative_scale_sum_zero_excludedmaskentryinput)) * S ((dst_negative_code_sum_zero_excludedmaskentryinput) + (dst_negative_scale_sum_zero_excludedmaskentryinput)) + ((dst_negative_scale_sum_zero_excludedmaskentryinput) + (dst_negative_scale_sum_zero_excludedmaskentryinput))) + (((dst_negative_code_sum_zero_excludedmaskentryinput) + (dst_negative_scale_sum_zero_excludedmaskentryinput)) * S ((dst_negative_code_sum_zero_excludedmaskentryinput) + (dst_negative_scale_sum_zero_excludedmaskentryinput)) + ((dst_negative_scale_sum_zero_excludedmaskentryinput) + (dst_negative_scale_sum_zero_excludedmaskentryinput)))))) /\ (((((exists ff_h_pvs_sum_zero_excludedmaskentryinputpositive. ff_h_pvs_sum_zero_excludedmaskentryinputpositive + S (dst_positive_sum_zero_excludedmaskentryinput) = S ((S (dm_index_sum_zero_excludedmask)) * dst_positive_scale_sum_zero_excludedmaskentryinput)) /\ exists ff_q_pvs_sum_zero_excludedmaskentryinputpositive. dst_positive_code_sum_zero_excludedmaskentryinput = ff_q_pvs_sum_zero_excludedmaskentryinputpositive * S ((S (dm_index_sum_zero_excludedmask)) * dst_positive_scale_sum_zero_excludedmaskentryinput) + (dst_positive_sum_zero_excludedmaskentryinput))) /\ (((((exists ff_h_pvs_sum_zero_excludedmaskentryinputnegative. ff_h_pvs_sum_zero_excludedmaskentryinputnegative + S (dst_negative_sum_zero_excludedmaskentryinput) = S ((S (dm_index_sum_zero_excludedmask)) * dst_negative_scale_sum_zero_excludedmaskentryinput)) /\ exists ff_q_pvs_sum_zero_excludedmaskentryinputnegative. dst_negative_code_sum_zero_excludedmaskentryinput = ff_q_pvs_sum_zero_excludedmaskentryinputnegative * S ((S (dm_index_sum_zero_excludedmask)) * dst_negative_scale_sum_zero_excludedmaskentryinput) + (dst_negative_sum_zero_excludedmaskentryinput))) /\ (exists ge_balance_positive_sum_zero_excludedmaskentryinputvalue ge_balance_negative_sum_zero_excludedmaskentryinputvalue. (((((dm_value_sum_zero_excludedmask) = 2 * (ge_balance_positive_sum_zero_excludedmaskentryinputvalue) /\ (ge_balance_negative_sum_zero_excludedmaskentryinputvalue) = 0) \/ exists ge_signed_half_sum_zero_excludedmaskentryinputvaluedecode. (((dm_value_sum_zero_excludedmask) = 2 * ge_signed_half_sum_zero_excludedmaskentryinputvaluedecode + 1 /\ (ge_balance_positive_sum_zero_excludedmaskentryinputvalue) = 0) /\ (ge_balance_negative_sum_zero_excludedmaskentryinputvalue) = S ge_signed_half_sum_zero_excludedmaskentryinputvaluedecode))) /\ ((dst_positive_sum_zero_excludedmaskentryinput) + ge_balance_negative_sum_zero_excludedmaskentryinputvalue = (dst_negative_sum_zero_excludedmaskentryinput) + ge_balance_positive_sum_zero_excludedmaskentryinputvalue))))))))))))) \/ ((((dm_index_sum_zero_excludedmask)=0 \/ ~(exists pvs_factor_sum_zero_excludedmaskentrynondivisor. (0) = (dm_index_sum_zero_excludedmask) * pvs_factor_sum_zero_excludedmaskentrynondivisor)) /\ ((dm_value_sum_zero_excludedmask)=0))))))) /\ (exists dst_positive_code_sum_zero_excludedfold dst_positive_scale_sum_zero_excludedfold dst_negative_code_sum_zero_excludedfold dst_negative_scale_sum_zero_excludedfold dst_positive_sum_sum_zero_excludedfold dst_negative_sum_sum_zero_excludedfold. (((dm_mask_table_sum_zero_excluded) = (((((dst_positive_code_sum_zero_excludedfold) + (dst_positive_scale_sum_zero_excludedfold)) * S ((dst_positive_code_sum_zero_excludedfold) + (dst_positive_scale_sum_zero_excludedfold)) + ((dst_positive_scale_sum_zero_excludedfold) + (dst_positive_scale_sum_zero_excludedfold))) + (((dst_negative_code_sum_zero_excludedfold) + (dst_negative_scale_sum_zero_excludedfold)) * S ((dst_negative_code_sum_zero_excludedfold) + (dst_negative_scale_sum_zero_excludedfold)) + ((dst_negative_scale_sum_zero_excludedfold) + (dst_negative_scale_sum_zero_excludedfold)))) * S ((((dst_positive_code_sum_zero_excludedfold) + (dst_positive_scale_sum_zero_excludedfold)) * S ((dst_positive_code_sum_zero_excludedfold) + (dst_positive_scale_sum_zero_excludedfold)) + ((dst_positive_scale_sum_zero_excludedfold) + (dst_positive_scale_sum_zero_excludedfold))) + (((dst_negative_code_sum_zero_excludedfold) + (dst_negative_scale_sum_zero_excludedfold)) * S ((dst_negative_code_sum_zero_excludedfold) + (dst_negative_scale_sum_zero_excludedfold)) + ((dst_negative_scale_sum_zero_excludedfold) + (dst_negative_scale_sum_zero_excludedfold)))) + ((((dst_negative_code_sum_zero_excludedfold) + (dst_negative_scale_sum_zero_excludedfold)) * S ((dst_negative_code_sum_zero_excludedfold) + (dst_negative_scale_sum_zero_excludedfold)) + ((dst_negative_scale_sum_zero_excludedfold) + (dst_negative_scale_sum_zero_excludedfold))) + (((dst_negative_code_sum_zero_excludedfold) + (dst_negative_scale_sum_zero_excludedfold)) * S ((dst_negative_code_sum_zero_excludedfold) + (dst_negative_scale_sum_zero_excludedfold)) + ((dst_negative_scale_sum_zero_excludedfold) + (dst_negative_scale_sum_zero_excludedfold)))))) /\ (((exists fs_u_dst_sum_zero_excludedfoldpositive fs_v_dst_sum_zero_excludedfoldpositive. ((((exists fs_h_dst_sum_zero_excludedfoldpositive_body_start. fs_h_dst_sum_zero_excludedfoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_sum_zero_excludedfoldpositive)) /\ exists fs_q_dst_sum_zero_excludedfoldpositive_body_start. fs_u_dst_sum_zero_excludedfoldpositive = fs_q_dst_sum_zero_excludedfoldpositive_body_start * S ((S (0)) * fs_v_dst_sum_zero_excludedfoldpositive) + (0))) /\ ((((exists fs_h_dst_sum_zero_excludedfoldpositive_body_terminal. fs_h_dst_sum_zero_excludedfoldpositive_body_terminal + S (dst_positive_sum_sum_zero_excludedfold) = S ((S (S (0))) * fs_v_dst_sum_zero_excludedfoldpositive)) /\ exists fs_q_dst_sum_zero_excludedfoldpositive_body_terminal. fs_u_dst_sum_zero_excludedfoldpositive = fs_q_dst_sum_zero_excludedfoldpositive_body_terminal * S ((S (S (0))) * fs_v_dst_sum_zero_excludedfoldpositive) + (dst_positive_sum_sum_zero_excludedfold))) /\ forall fs_i_dst_sum_zero_excludedfoldpositive_body_steps. (exists fs_lt_dst_sum_zero_excludedfoldpositive_body_steps_bound. fs_lt_dst_sum_zero_excludedfoldpositive_body_steps_bound + S fs_i_dst_sum_zero_excludedfoldpositive_body_steps = S (0)) -> exists fs_a_dst_sum_zero_excludedfoldpositive_body_steps fs_r_dst_sum_zero_excludedfoldpositive_body_steps fs_s_dst_sum_zero_excludedfoldpositive_body_steps. ((((exists fs_h_dst_sum_zero_excludedfoldpositive_body_steps_summand. fs_h_dst_sum_zero_excludedfoldpositive_body_steps_summand + S (fs_a_dst_sum_zero_excludedfoldpositive_body_steps) = S ((S (fs_i_dst_sum_zero_excludedfoldpositive_body_steps)) * dst_positive_scale_sum_zero_excludedfold)) /\ exists fs_q_dst_sum_zero_excludedfoldpositive_body_steps_summand. dst_positive_code_sum_zero_excludedfold = fs_q_dst_sum_zero_excludedfoldpositive_body_steps_summand * S ((S (fs_i_dst_sum_zero_excludedfoldpositive_body_steps)) * dst_positive_scale_sum_zero_excludedfold) + (fs_a_dst_sum_zero_excludedfoldpositive_body_steps))) /\ ((((exists fs_h_dst_sum_zero_excludedfoldpositive_body_steps_partial. fs_h_dst_sum_zero_excludedfoldpositive_body_steps_partial + S (fs_r_dst_sum_zero_excludedfoldpositive_body_steps) = S ((S (fs_i_dst_sum_zero_excludedfoldpositive_body_steps)) * fs_v_dst_sum_zero_excludedfoldpositive)) /\ exists fs_q_dst_sum_zero_excludedfoldpositive_body_steps_partial. fs_u_dst_sum_zero_excludedfoldpositive = fs_q_dst_sum_zero_excludedfoldpositive_body_steps_partial * S ((S (fs_i_dst_sum_zero_excludedfoldpositive_body_steps)) * fs_v_dst_sum_zero_excludedfoldpositive) + (fs_r_dst_sum_zero_excludedfoldpositive_body_steps))) /\ ((((exists fs_h_dst_sum_zero_excludedfoldpositive_body_steps_successor. fs_h_dst_sum_zero_excludedfoldpositive_body_steps_successor + S (fs_s_dst_sum_zero_excludedfoldpositive_body_steps) = S ((S (S fs_i_dst_sum_zero_excludedfoldpositive_body_steps)) * fs_v_dst_sum_zero_excludedfoldpositive)) /\ exists fs_q_dst_sum_zero_excludedfoldpositive_body_steps_successor. fs_u_dst_sum_zero_excludedfoldpositive = fs_q_dst_sum_zero_excludedfoldpositive_body_steps_successor * S ((S (S fs_i_dst_sum_zero_excludedfoldpositive_body_steps)) * fs_v_dst_sum_zero_excludedfoldpositive) + (fs_s_dst_sum_zero_excludedfoldpositive_body_steps))) /\ fs_s_dst_sum_zero_excludedfoldpositive_body_steps = fs_r_dst_sum_zero_excludedfoldpositive_body_steps + fs_a_dst_sum_zero_excludedfoldpositive_body_steps)))))) /\ (((exists fs_u_dst_sum_zero_excludedfoldnegative fs_v_dst_sum_zero_excludedfoldnegative. ((((exists fs_h_dst_sum_zero_excludedfoldnegative_body_start. fs_h_dst_sum_zero_excludedfoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_sum_zero_excludedfoldnegative)) /\ exists fs_q_dst_sum_zero_excludedfoldnegative_body_start. fs_u_dst_sum_zero_excludedfoldnegative = fs_q_dst_sum_zero_excludedfoldnegative_body_start * S ((S (0)) * fs_v_dst_sum_zero_excludedfoldnegative) + (0))) /\ ((((exists fs_h_dst_sum_zero_excludedfoldnegative_body_terminal. fs_h_dst_sum_zero_excludedfoldnegative_body_terminal + S (dst_negative_sum_sum_zero_excludedfold) = S ((S (S (0))) * fs_v_dst_sum_zero_excludedfoldnegative)) /\ exists fs_q_dst_sum_zero_excludedfoldnegative_body_terminal. fs_u_dst_sum_zero_excludedfoldnegative = fs_q_dst_sum_zero_excludedfoldnegative_body_terminal * S ((S (S (0))) * fs_v_dst_sum_zero_excludedfoldnegative) + (dst_negative_sum_sum_zero_excludedfold))) /\ forall fs_i_dst_sum_zero_excludedfoldnegative_body_steps. (exists fs_lt_dst_sum_zero_excludedfoldnegative_body_steps_bound. fs_lt_dst_sum_zero_excludedfoldnegative_body_steps_bound + S fs_i_dst_sum_zero_excludedfoldnegative_body_steps = S (0)) -> exists fs_a_dst_sum_zero_excludedfoldnegative_body_steps fs_r_dst_sum_zero_excludedfoldnegative_body_steps fs_s_dst_sum_zero_excludedfoldnegative_body_steps. ((((exists fs_h_dst_sum_zero_excludedfoldnegative_body_steps_summand. fs_h_dst_sum_zero_excludedfoldnegative_body_steps_summand + S (fs_a_dst_sum_zero_excludedfoldnegative_body_steps) = S ((S (fs_i_dst_sum_zero_excludedfoldnegative_body_steps)) * dst_negative_scale_sum_zero_excludedfold)) /\ exists fs_q_dst_sum_zero_excludedfoldnegative_body_steps_summand. dst_negative_code_sum_zero_excludedfold = fs_q_dst_sum_zero_excludedfoldnegative_body_steps_summand * S ((S (fs_i_dst_sum_zero_excludedfoldnegative_body_steps)) * dst_negative_scale_sum_zero_excludedfold) + (fs_a_dst_sum_zero_excludedfoldnegative_body_steps))) /\ ((((exists fs_h_dst_sum_zero_excludedfoldnegative_body_steps_partial. fs_h_dst_sum_zero_excludedfoldnegative_body_steps_partial + S (fs_r_dst_sum_zero_excludedfoldnegative_body_steps) = S ((S (fs_i_dst_sum_zero_excludedfoldnegative_body_steps)) * fs_v_dst_sum_zero_excludedfoldnegative)) /\ exists fs_q_dst_sum_zero_excludedfoldnegative_body_steps_partial. fs_u_dst_sum_zero_excludedfoldnegative = fs_q_dst_sum_zero_excludedfoldnegative_body_steps_partial * S ((S (fs_i_dst_sum_zero_excludedfoldnegative_body_steps)) * fs_v_dst_sum_zero_excludedfoldnegative) + (fs_r_dst_sum_zero_excludedfoldnegative_body_steps))) /\ ((((exists fs_h_dst_sum_zero_excludedfoldnegative_body_steps_successor. fs_h_dst_sum_zero_excludedfoldnegative_body_steps_successor + S (fs_s_dst_sum_zero_excludedfoldnegative_body_steps) = S ((S (S fs_i_dst_sum_zero_excludedfoldnegative_body_steps)) * fs_v_dst_sum_zero_excludedfoldnegative)) /\ exists fs_q_dst_sum_zero_excludedfoldnegative_body_steps_successor. fs_u_dst_sum_zero_excludedfoldnegative = fs_q_dst_sum_zero_excludedfoldnegative_body_steps_successor * S ((S (S fs_i_dst_sum_zero_excludedfoldnegative_body_steps)) * fs_v_dst_sum_zero_excludedfoldnegative) + (fs_s_dst_sum_zero_excludedfoldnegative_body_steps))) /\ fs_s_dst_sum_zero_excludedfoldnegative_body_steps = fs_r_dst_sum_zero_excludedfoldnegative_body_steps + fs_a_dst_sum_zero_excludedfoldnegative_body_steps)))))) /\ (exists ge_balance_positive_sum_zero_excludedfoldresult ge_balance_negative_sum_zero_excludedfoldresult. (((((z) = 2 * (ge_balance_positive_sum_zero_excludedfoldresult) /\ (ge_balance_negative_sum_zero_excludedfoldresult) = 0) \/ exists ge_signed_half_sum_zero_excludedfoldresultdecode. (((z) = 2 * ge_signed_half_sum_zero_excludedfoldresultdecode + 1 /\ (ge_balance_positive_sum_zero_excludedfoldresult) = 0) /\ (ge_balance_negative_sum_zero_excludedfoldresult) = S ge_signed_half_sum_zero_excludedfoldresultdecode))) /\ ((dst_positive_sum_sum_zero_excludedfold) + ge_balance_negative_sum_zero_excludedfoldresult = (dst_negative_sum_sum_zero_excludedfold) + ge_balance_positive_sum_zero_excludedfoldresult))))))))))))) -> false