signed_divisor_sum_functional

Exact expanded first-order arithmetic statement

forall F n a b. (((~((n)=0)) /\ (exists dm_mask_table_sum_unique_first. ((((exists dst_positive_code_sum_unique_firstmasktable dst_positive_scale_sum_unique_firstmasktable dst_negative_code_sum_unique_firstmasktable dst_negative_scale_sum_unique_firstmasktable. (((dm_mask_table_sum_unique_first) = (((((dst_positive_code_sum_unique_firstmasktable) + (dst_positive_scale_sum_unique_firstmasktable)) * S ((dst_positive_code_sum_unique_firstmasktable) + (dst_positive_scale_sum_unique_firstmasktable)) + ((dst_positive_scale_sum_unique_firstmasktable) + (dst_positive_scale_sum_unique_firstmasktable))) + (((dst_negative_code_sum_unique_firstmasktable) + (dst_negative_scale_sum_unique_firstmasktable)) * S ((dst_negative_code_sum_unique_firstmasktable) + (dst_negative_scale_sum_unique_firstmasktable)) + ((dst_negative_scale_sum_unique_firstmasktable) + (dst_negative_scale_sum_unique_firstmasktable)))) * S ((((dst_positive_code_sum_unique_firstmasktable) + (dst_positive_scale_sum_unique_firstmasktable)) * S ((dst_positive_code_sum_unique_firstmasktable) + (dst_positive_scale_sum_unique_firstmasktable)) + ((dst_positive_scale_sum_unique_firstmasktable) + (dst_positive_scale_sum_unique_firstmasktable))) + (((dst_negative_code_sum_unique_firstmasktable) + (dst_negative_scale_sum_unique_firstmasktable)) * S ((dst_negative_code_sum_unique_firstmasktable) + (dst_negative_scale_sum_unique_firstmasktable)) + ((dst_negative_scale_sum_unique_firstmasktable) + (dst_negative_scale_sum_unique_firstmasktable)))) + ((((dst_negative_code_sum_unique_firstmasktable) + (dst_negative_scale_sum_unique_firstmasktable)) * S ((dst_negative_code_sum_unique_firstmasktable) + (dst_negative_scale_sum_unique_firstmasktable)) + ((dst_negative_scale_sum_unique_firstmasktable) + (dst_negative_scale_sum_unique_firstmasktable))) + (((dst_negative_code_sum_unique_firstmasktable) + (dst_negative_scale_sum_unique_firstmasktable)) * S ((dst_negative_code_sum_unique_firstmasktable) + (dst_negative_scale_sum_unique_firstmasktable)) + ((dst_negative_scale_sum_unique_firstmasktable) + (dst_negative_scale_sum_unique_firstmasktable)))))) /\ (forall dst_index_sum_unique_firstmasktable. (exists pvs_le_gap_sum_unique_firstmasktabledomain. pvs_le_gap_sum_unique_firstmasktabledomain + (dst_index_sum_unique_firstmasktable) = (n)) -> exists dst_positive_sum_unique_firstmasktable dst_negative_sum_unique_firstmasktable dst_value_sum_unique_firstmasktable. ((((exists ff_h_pvs_sum_unique_firstmasktableentrypositive. ff_h_pvs_sum_unique_firstmasktableentrypositive + S (dst_positive_sum_unique_firstmasktable) = S ((S (dst_index_sum_unique_firstmasktable)) * dst_positive_scale_sum_unique_firstmasktable)) /\ exists ff_q_pvs_sum_unique_firstmasktableentrypositive. dst_positive_code_sum_unique_firstmasktable = ff_q_pvs_sum_unique_firstmasktableentrypositive * S ((S (dst_index_sum_unique_firstmasktable)) * dst_positive_scale_sum_unique_firstmasktable) + (dst_positive_sum_unique_firstmasktable))) /\ (((((exists ff_h_pvs_sum_unique_firstmasktableentrynegative. ff_h_pvs_sum_unique_firstmasktableentrynegative + S (dst_negative_sum_unique_firstmasktable) = S ((S (dst_index_sum_unique_firstmasktable)) * dst_negative_scale_sum_unique_firstmasktable)) /\ exists ff_q_pvs_sum_unique_firstmasktableentrynegative. dst_negative_code_sum_unique_firstmasktable = ff_q_pvs_sum_unique_firstmasktableentrynegative * S ((S (dst_index_sum_unique_firstmasktable)) * dst_negative_scale_sum_unique_firstmasktable) + (dst_negative_sum_unique_firstmasktable))) /\ (exists ge_balance_positive_sum_unique_firstmasktableentryvalue ge_balance_negative_sum_unique_firstmasktableentryvalue. (((((dst_value_sum_unique_firstmasktable) = 2 * (ge_balance_positive_sum_unique_firstmasktableentryvalue) /\ (ge_balance_negative_sum_unique_firstmasktableentryvalue) = 0) \/ exists ge_signed_half_sum_unique_firstmasktableentryvaluedecode. (((dst_value_sum_unique_firstmasktable) = 2 * ge_signed_half_sum_unique_firstmasktableentryvaluedecode + 1 /\ (ge_balance_positive_sum_unique_firstmasktableentryvalue) = 0) /\ (ge_balance_negative_sum_unique_firstmasktableentryvalue) = S ge_signed_half_sum_unique_firstmasktableentryvaluedecode))) /\ ((dst_positive_sum_unique_firstmasktable) + ge_balance_negative_sum_unique_firstmasktableentryvalue = (dst_negative_sum_unique_firstmasktable) + ge_balance_positive_sum_unique_firstmasktableentryvalue))))))))) /\ (forall dm_index_sum_unique_firstmask dm_value_sum_unique_firstmask. (exists pvs_le_gap_sum_unique_firstmaskdomain. pvs_le_gap_sum_unique_firstmaskdomain + (dm_index_sum_unique_firstmask) = (n)) -> (exists dst_positive_code_sum_unique_firstmasklookup dst_positive_scale_sum_unique_firstmasklookup dst_negative_code_sum_unique_firstmasklookup dst_negative_scale_sum_unique_firstmasklookup dst_positive_sum_unique_firstmasklookup dst_negative_sum_unique_firstmasklookup. (((dm_mask_table_sum_unique_first) = (((((dst_positive_code_sum_unique_firstmasklookup) + (dst_positive_scale_sum_unique_firstmasklookup)) * S ((dst_positive_code_sum_unique_firstmasklookup) + (dst_positive_scale_sum_unique_firstmasklookup)) + ((dst_positive_scale_sum_unique_firstmasklookup) + (dst_positive_scale_sum_unique_firstmasklookup))) + (((dst_negative_code_sum_unique_firstmasklookup) + (dst_negative_scale_sum_unique_firstmasklookup)) * S ((dst_negative_code_sum_unique_firstmasklookup) + (dst_negative_scale_sum_unique_firstmasklookup)) + ((dst_negative_scale_sum_unique_firstmasklookup) + (dst_negative_scale_sum_unique_firstmasklookup)))) * S ((((dst_positive_code_sum_unique_firstmasklookup) + (dst_positive_scale_sum_unique_firstmasklookup)) * S ((dst_positive_code_sum_unique_firstmasklookup) + (dst_positive_scale_sum_unique_firstmasklookup)) + ((dst_positive_scale_sum_unique_firstmasklookup) + (dst_positive_scale_sum_unique_firstmasklookup))) + (((dst_negative_code_sum_unique_firstmasklookup) + (dst_negative_scale_sum_unique_firstmasklookup)) * S ((dst_negative_code_sum_unique_firstmasklookup) + (dst_negative_scale_sum_unique_firstmasklookup)) + ((dst_negative_scale_sum_unique_firstmasklookup) + (dst_negative_scale_sum_unique_firstmasklookup)))) + ((((dst_negative_code_sum_unique_firstmasklookup) + (dst_negative_scale_sum_unique_firstmasklookup)) * S ((dst_negative_code_sum_unique_firstmasklookup) + (dst_negative_scale_sum_unique_firstmasklookup)) + ((dst_negative_scale_sum_unique_firstmasklookup) + (dst_negative_scale_sum_unique_firstmasklookup))) + (((dst_negative_code_sum_unique_firstmasklookup) + (dst_negative_scale_sum_unique_firstmasklookup)) * S ((dst_negative_code_sum_unique_firstmasklookup) + (dst_negative_scale_sum_unique_firstmasklookup)) + ((dst_negative_scale_sum_unique_firstmasklookup) + (dst_negative_scale_sum_unique_firstmasklookup)))))) /\ (((((exists ff_h_pvs_sum_unique_firstmasklookuppositive. ff_h_pvs_sum_unique_firstmasklookuppositive + S (dst_positive_sum_unique_firstmasklookup) = S ((S (dm_index_sum_unique_firstmask)) * dst_positive_scale_sum_unique_firstmasklookup)) /\ exists ff_q_pvs_sum_unique_firstmasklookuppositive. dst_positive_code_sum_unique_firstmasklookup = ff_q_pvs_sum_unique_firstmasklookuppositive * S ((S (dm_index_sum_unique_firstmask)) * dst_positive_scale_sum_unique_firstmasklookup) + (dst_positive_sum_unique_firstmasklookup))) /\ (((((exists ff_h_pvs_sum_unique_firstmasklookupnegative. ff_h_pvs_sum_unique_firstmasklookupnegative + S (dst_negative_sum_unique_firstmasklookup) = S ((S (dm_index_sum_unique_firstmask)) * dst_negative_scale_sum_unique_firstmasklookup)) /\ exists ff_q_pvs_sum_unique_firstmasklookupnegative. dst_negative_code_sum_unique_firstmasklookup = ff_q_pvs_sum_unique_firstmasklookupnegative * S ((S (dm_index_sum_unique_firstmask)) * dst_negative_scale_sum_unique_firstmasklookup) + (dst_negative_sum_unique_firstmasklookup))) /\ (exists ge_balance_positive_sum_unique_firstmasklookupvalue ge_balance_negative_sum_unique_firstmasklookupvalue. (((((dm_value_sum_unique_firstmask) = 2 * (ge_balance_positive_sum_unique_firstmasklookupvalue) /\ (ge_balance_negative_sum_unique_firstmasklookupvalue) = 0) \/ exists ge_signed_half_sum_unique_firstmasklookupvaluedecode. (((dm_value_sum_unique_firstmask) = 2 * ge_signed_half_sum_unique_firstmasklookupvaluedecode + 1 /\ (ge_balance_positive_sum_unique_firstmasklookupvalue) = 0) /\ (ge_balance_negative_sum_unique_firstmasklookupvalue) = S ge_signed_half_sum_unique_firstmasklookupvaluedecode))) /\ ((dst_positive_sum_unique_firstmasklookup) + ge_balance_negative_sum_unique_firstmasklookupvalue = (dst_negative_sum_unique_firstmasklookup) + ge_balance_positive_sum_unique_firstmasklookupvalue))))))))) -> ((((~((dm_index_sum_unique_firstmask)=0)) /\ (exists dm_quotient_sum_unique_firstmaskentry. (((n)=(dm_index_sum_unique_firstmask)*dm_quotient_sum_unique_firstmaskentry) /\ (exists dst_positive_code_sum_unique_firstmaskentryinput dst_positive_scale_sum_unique_firstmaskentryinput dst_negative_code_sum_unique_firstmaskentryinput dst_negative_scale_sum_unique_firstmaskentryinput dst_positive_sum_unique_firstmaskentryinput dst_negative_sum_unique_firstmaskentryinput. (((F) = (((((dst_positive_code_sum_unique_firstmaskentryinput) + (dst_positive_scale_sum_unique_firstmaskentryinput)) * S ((dst_positive_code_sum_unique_firstmaskentryinput) + (dst_positive_scale_sum_unique_firstmaskentryinput)) + ((dst_positive_scale_sum_unique_firstmaskentryinput) + (dst_positive_scale_sum_unique_firstmaskentryinput))) + (((dst_negative_code_sum_unique_firstmaskentryinput) + (dst_negative_scale_sum_unique_firstmaskentryinput)) * S ((dst_negative_code_sum_unique_firstmaskentryinput) + (dst_negative_scale_sum_unique_firstmaskentryinput)) + ((dst_negative_scale_sum_unique_firstmaskentryinput) + (dst_negative_scale_sum_unique_firstmaskentryinput)))) * S ((((dst_positive_code_sum_unique_firstmaskentryinput) + (dst_positive_scale_sum_unique_firstmaskentryinput)) * S ((dst_positive_code_sum_unique_firstmaskentryinput) + (dst_positive_scale_sum_unique_firstmaskentryinput)) + ((dst_positive_scale_sum_unique_firstmaskentryinput) + (dst_positive_scale_sum_unique_firstmaskentryinput))) + (((dst_negative_code_sum_unique_firstmaskentryinput) + (dst_negative_scale_sum_unique_firstmaskentryinput)) * S ((dst_negative_code_sum_unique_firstmaskentryinput) + (dst_negative_scale_sum_unique_firstmaskentryinput)) + ((dst_negative_scale_sum_unique_firstmaskentryinput) + (dst_negative_scale_sum_unique_firstmaskentryinput)))) + ((((dst_negative_code_sum_unique_firstmaskentryinput) + (dst_negative_scale_sum_unique_firstmaskentryinput)) * S ((dst_negative_code_sum_unique_firstmaskentryinput) + (dst_negative_scale_sum_unique_firstmaskentryinput)) + ((dst_negative_scale_sum_unique_firstmaskentryinput) + (dst_negative_scale_sum_unique_firstmaskentryinput))) + (((dst_negative_code_sum_unique_firstmaskentryinput) + (dst_negative_scale_sum_unique_firstmaskentryinput)) * S ((dst_negative_code_sum_unique_firstmaskentryinput) + (dst_negative_scale_sum_unique_firstmaskentryinput)) + ((dst_negative_scale_sum_unique_firstmaskentryinput) + (dst_negative_scale_sum_unique_firstmaskentryinput)))))) /\ (((((exists ff_h_pvs_sum_unique_firstmaskentryinputpositive. ff_h_pvs_sum_unique_firstmaskentryinputpositive + S (dst_positive_sum_unique_firstmaskentryinput) = S ((S (dm_index_sum_unique_firstmask)) * dst_positive_scale_sum_unique_firstmaskentryinput)) /\ exists ff_q_pvs_sum_unique_firstmaskentryinputpositive. dst_positive_code_sum_unique_firstmaskentryinput = ff_q_pvs_sum_unique_firstmaskentryinputpositive * S ((S (dm_index_sum_unique_firstmask)) * dst_positive_scale_sum_unique_firstmaskentryinput) + (dst_positive_sum_unique_firstmaskentryinput))) /\ (((((exists ff_h_pvs_sum_unique_firstmaskentryinputnegative. ff_h_pvs_sum_unique_firstmaskentryinputnegative + S (dst_negative_sum_unique_firstmaskentryinput) = S ((S (dm_index_sum_unique_firstmask)) * dst_negative_scale_sum_unique_firstmaskentryinput)) /\ exists ff_q_pvs_sum_unique_firstmaskentryinputnegative. dst_negative_code_sum_unique_firstmaskentryinput = ff_q_pvs_sum_unique_firstmaskentryinputnegative * S ((S (dm_index_sum_unique_firstmask)) * dst_negative_scale_sum_unique_firstmaskentryinput) + (dst_negative_sum_unique_firstmaskentryinput))) /\ (exists ge_balance_positive_sum_unique_firstmaskentryinputvalue ge_balance_negative_sum_unique_firstmaskentryinputvalue. (((((dm_value_sum_unique_firstmask) = 2 * (ge_balance_positive_sum_unique_firstmaskentryinputvalue) /\ (ge_balance_negative_sum_unique_firstmaskentryinputvalue) = 0) \/ exists ge_signed_half_sum_unique_firstmaskentryinputvaluedecode. (((dm_value_sum_unique_firstmask) = 2 * ge_signed_half_sum_unique_firstmaskentryinputvaluedecode + 1 /\ (ge_balance_positive_sum_unique_firstmaskentryinputvalue) = 0) /\ (ge_balance_negative_sum_unique_firstmaskentryinputvalue) = S ge_signed_half_sum_unique_firstmaskentryinputvaluedecode))) /\ ((dst_positive_sum_unique_firstmaskentryinput) + ge_balance_negative_sum_unique_firstmaskentryinputvalue = (dst_negative_sum_unique_firstmaskentryinput) + ge_balance_positive_sum_unique_firstmaskentryinputvalue))))))))))))) \/ ((((dm_index_sum_unique_firstmask)=0 \/ ~(exists pvs_factor_sum_unique_firstmaskentrynondivisor. (n) = (dm_index_sum_unique_firstmask) * pvs_factor_sum_unique_firstmaskentrynondivisor)) /\ ((dm_value_sum_unique_firstmask)=0))))))) /\ (exists dst_positive_code_sum_unique_firstfold dst_positive_scale_sum_unique_firstfold dst_negative_code_sum_unique_firstfold dst_negative_scale_sum_unique_firstfold dst_positive_sum_sum_unique_firstfold dst_negative_sum_sum_unique_firstfold. (((dm_mask_table_sum_unique_first) = (((((dst_positive_code_sum_unique_firstfold) + (dst_positive_scale_sum_unique_firstfold)) * S ((dst_positive_code_sum_unique_firstfold) + (dst_positive_scale_sum_unique_firstfold)) + ((dst_positive_scale_sum_unique_firstfold) + (dst_positive_scale_sum_unique_firstfold))) + (((dst_negative_code_sum_unique_firstfold) + (dst_negative_scale_sum_unique_firstfold)) * S ((dst_negative_code_sum_unique_firstfold) + (dst_negative_scale_sum_unique_firstfold)) + ((dst_negative_scale_sum_unique_firstfold) + (dst_negative_scale_sum_unique_firstfold)))) * S ((((dst_positive_code_sum_unique_firstfold) + (dst_positive_scale_sum_unique_firstfold)) * S ((dst_positive_code_sum_unique_firstfold) + (dst_positive_scale_sum_unique_firstfold)) + ((dst_positive_scale_sum_unique_firstfold) + (dst_positive_scale_sum_unique_firstfold))) + (((dst_negative_code_sum_unique_firstfold) + (dst_negative_scale_sum_unique_firstfold)) * S ((dst_negative_code_sum_unique_firstfold) + (dst_negative_scale_sum_unique_firstfold)) + ((dst_negative_scale_sum_unique_firstfold) + (dst_negative_scale_sum_unique_firstfold)))) + ((((dst_negative_code_sum_unique_firstfold) + (dst_negative_scale_sum_unique_firstfold)) * S ((dst_negative_code_sum_unique_firstfold) + (dst_negative_scale_sum_unique_firstfold)) + ((dst_negative_scale_sum_unique_firstfold) + (dst_negative_scale_sum_unique_firstfold))) + (((dst_negative_code_sum_unique_firstfold) + (dst_negative_scale_sum_unique_firstfold)) * S ((dst_negative_code_sum_unique_firstfold) + (dst_negative_scale_sum_unique_firstfold)) + ((dst_negative_scale_sum_unique_firstfold) + (dst_negative_scale_sum_unique_firstfold)))))) /\ (((exists fs_u_dst_sum_unique_firstfoldpositive fs_v_dst_sum_unique_firstfoldpositive. ((((exists fs_h_dst_sum_unique_firstfoldpositive_body_start. fs_h_dst_sum_unique_firstfoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_sum_unique_firstfoldpositive)) /\ exists fs_q_dst_sum_unique_firstfoldpositive_body_start. fs_u_dst_sum_unique_firstfoldpositive = fs_q_dst_sum_unique_firstfoldpositive_body_start * S ((S (0)) * fs_v_dst_sum_unique_firstfoldpositive) + (0))) /\ ((((exists fs_h_dst_sum_unique_firstfoldpositive_body_terminal. fs_h_dst_sum_unique_firstfoldpositive_body_terminal + S (dst_positive_sum_sum_unique_firstfold) = S ((S (S (n))) * fs_v_dst_sum_unique_firstfoldpositive)) /\ exists fs_q_dst_sum_unique_firstfoldpositive_body_terminal. fs_u_dst_sum_unique_firstfoldpositive = fs_q_dst_sum_unique_firstfoldpositive_body_terminal * S ((S (S (n))) * fs_v_dst_sum_unique_firstfoldpositive) + (dst_positive_sum_sum_unique_firstfold))) /\ forall fs_i_dst_sum_unique_firstfoldpositive_body_steps. (exists fs_lt_dst_sum_unique_firstfoldpositive_body_steps_bound. fs_lt_dst_sum_unique_firstfoldpositive_body_steps_bound + S fs_i_dst_sum_unique_firstfoldpositive_body_steps = S (n)) -> exists fs_a_dst_sum_unique_firstfoldpositive_body_steps fs_r_dst_sum_unique_firstfoldpositive_body_steps fs_s_dst_sum_unique_firstfoldpositive_body_steps. ((((exists fs_h_dst_sum_unique_firstfoldpositive_body_steps_summand. fs_h_dst_sum_unique_firstfoldpositive_body_steps_summand + S (fs_a_dst_sum_unique_firstfoldpositive_body_steps) = S ((S (fs_i_dst_sum_unique_firstfoldpositive_body_steps)) * dst_positive_scale_sum_unique_firstfold)) /\ exists fs_q_dst_sum_unique_firstfoldpositive_body_steps_summand. dst_positive_code_sum_unique_firstfold = fs_q_dst_sum_unique_firstfoldpositive_body_steps_summand * S ((S (fs_i_dst_sum_unique_firstfoldpositive_body_steps)) * dst_positive_scale_sum_unique_firstfold) + (fs_a_dst_sum_unique_firstfoldpositive_body_steps))) /\ ((((exists fs_h_dst_sum_unique_firstfoldpositive_body_steps_partial. fs_h_dst_sum_unique_firstfoldpositive_body_steps_partial + S (fs_r_dst_sum_unique_firstfoldpositive_body_steps) = S ((S (fs_i_dst_sum_unique_firstfoldpositive_body_steps)) * fs_v_dst_sum_unique_firstfoldpositive)) /\ exists fs_q_dst_sum_unique_firstfoldpositive_body_steps_partial. fs_u_dst_sum_unique_firstfoldpositive = fs_q_dst_sum_unique_firstfoldpositive_body_steps_partial * S ((S (fs_i_dst_sum_unique_firstfoldpositive_body_steps)) * fs_v_dst_sum_unique_firstfoldpositive) + (fs_r_dst_sum_unique_firstfoldpositive_body_steps))) /\ ((((exists fs_h_dst_sum_unique_firstfoldpositive_body_steps_successor. fs_h_dst_sum_unique_firstfoldpositive_body_steps_successor + S (fs_s_dst_sum_unique_firstfoldpositive_body_steps) = S ((S (S fs_i_dst_sum_unique_firstfoldpositive_body_steps)) * fs_v_dst_sum_unique_firstfoldpositive)) /\ exists fs_q_dst_sum_unique_firstfoldpositive_body_steps_successor. fs_u_dst_sum_unique_firstfoldpositive = fs_q_dst_sum_unique_firstfoldpositive_body_steps_successor * S ((S (S fs_i_dst_sum_unique_firstfoldpositive_body_steps)) * fs_v_dst_sum_unique_firstfoldpositive) + (fs_s_dst_sum_unique_firstfoldpositive_body_steps))) /\ fs_s_dst_sum_unique_firstfoldpositive_body_steps = fs_r_dst_sum_unique_firstfoldpositive_body_steps + fs_a_dst_sum_unique_firstfoldpositive_body_steps)))))) /\ (((exists fs_u_dst_sum_unique_firstfoldnegative fs_v_dst_sum_unique_firstfoldnegative. ((((exists fs_h_dst_sum_unique_firstfoldnegative_body_start. fs_h_dst_sum_unique_firstfoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_sum_unique_firstfoldnegative)) /\ exists fs_q_dst_sum_unique_firstfoldnegative_body_start. fs_u_dst_sum_unique_firstfoldnegative = fs_q_dst_sum_unique_firstfoldnegative_body_start * S ((S (0)) * fs_v_dst_sum_unique_firstfoldnegative) + (0))) /\ ((((exists fs_h_dst_sum_unique_firstfoldnegative_body_terminal. fs_h_dst_sum_unique_firstfoldnegative_body_terminal + S (dst_negative_sum_sum_unique_firstfold) = S ((S (S (n))) * fs_v_dst_sum_unique_firstfoldnegative)) /\ exists fs_q_dst_sum_unique_firstfoldnegative_body_terminal. fs_u_dst_sum_unique_firstfoldnegative = fs_q_dst_sum_unique_firstfoldnegative_body_terminal * S ((S (S (n))) * fs_v_dst_sum_unique_firstfoldnegative) + (dst_negative_sum_sum_unique_firstfold))) /\ forall fs_i_dst_sum_unique_firstfoldnegative_body_steps. (exists fs_lt_dst_sum_unique_firstfoldnegative_body_steps_bound. fs_lt_dst_sum_unique_firstfoldnegative_body_steps_bound + S fs_i_dst_sum_unique_firstfoldnegative_body_steps = S (n)) -> exists fs_a_dst_sum_unique_firstfoldnegative_body_steps fs_r_dst_sum_unique_firstfoldnegative_body_steps fs_s_dst_sum_unique_firstfoldnegative_body_steps. ((((exists fs_h_dst_sum_unique_firstfoldnegative_body_steps_summand. fs_h_dst_sum_unique_firstfoldnegative_body_steps_summand + S (fs_a_dst_sum_unique_firstfoldnegative_body_steps) = S ((S (fs_i_dst_sum_unique_firstfoldnegative_body_steps)) * dst_negative_scale_sum_unique_firstfold)) /\ exists fs_q_dst_sum_unique_firstfoldnegative_body_steps_summand. dst_negative_code_sum_unique_firstfold = fs_q_dst_sum_unique_firstfoldnegative_body_steps_summand * S ((S (fs_i_dst_sum_unique_firstfoldnegative_body_steps)) * dst_negative_scale_sum_unique_firstfold) + (fs_a_dst_sum_unique_firstfoldnegative_body_steps))) /\ ((((exists fs_h_dst_sum_unique_firstfoldnegative_body_steps_partial. fs_h_dst_sum_unique_firstfoldnegative_body_steps_partial + S (fs_r_dst_sum_unique_firstfoldnegative_body_steps) = S ((S (fs_i_dst_sum_unique_firstfoldnegative_body_steps)) * fs_v_dst_sum_unique_firstfoldnegative)) /\ exists fs_q_dst_sum_unique_firstfoldnegative_body_steps_partial. fs_u_dst_sum_unique_firstfoldnegative = fs_q_dst_sum_unique_firstfoldnegative_body_steps_partial * S ((S (fs_i_dst_sum_unique_firstfoldnegative_body_steps)) * fs_v_dst_sum_unique_firstfoldnegative) + (fs_r_dst_sum_unique_firstfoldnegative_body_steps))) /\ ((((exists fs_h_dst_sum_unique_firstfoldnegative_body_steps_successor. fs_h_dst_sum_unique_firstfoldnegative_body_steps_successor + S (fs_s_dst_sum_unique_firstfoldnegative_body_steps) = S ((S (S fs_i_dst_sum_unique_firstfoldnegative_body_steps)) * fs_v_dst_sum_unique_firstfoldnegative)) /\ exists fs_q_dst_sum_unique_firstfoldnegative_body_steps_successor. fs_u_dst_sum_unique_firstfoldnegative = fs_q_dst_sum_unique_firstfoldnegative_body_steps_successor * S ((S (S fs_i_dst_sum_unique_firstfoldnegative_body_steps)) * fs_v_dst_sum_unique_firstfoldnegative) + (fs_s_dst_sum_unique_firstfoldnegative_body_steps))) /\ fs_s_dst_sum_unique_firstfoldnegative_body_steps = fs_r_dst_sum_unique_firstfoldnegative_body_steps + fs_a_dst_sum_unique_firstfoldnegative_body_steps)))))) /\ (exists ge_balance_positive_sum_unique_firstfoldresult ge_balance_negative_sum_unique_firstfoldresult. (((((a) = 2 * (ge_balance_positive_sum_unique_firstfoldresult) /\ (ge_balance_negative_sum_unique_firstfoldresult) = 0) \/ exists ge_signed_half_sum_unique_firstfoldresultdecode. (((a) = 2 * ge_signed_half_sum_unique_firstfoldresultdecode + 1 /\ (ge_balance_positive_sum_unique_firstfoldresult) = 0) /\ (ge_balance_negative_sum_unique_firstfoldresult) = S ge_signed_half_sum_unique_firstfoldresultdecode))) /\ ((dst_positive_sum_sum_unique_firstfold) + ge_balance_negative_sum_unique_firstfoldresult = (dst_negative_sum_sum_unique_firstfold) + ge_balance_positive_sum_unique_firstfoldresult))))))))))))) -> (((~((n)=0)) /\ (exists dm_mask_table_sum_unique_second. ((((exists dst_positive_code_sum_unique_secondmasktable dst_positive_scale_sum_unique_secondmasktable dst_negative_code_sum_unique_secondmasktable dst_negative_scale_sum_unique_secondmasktable. (((dm_mask_table_sum_unique_second) = (((((dst_positive_code_sum_unique_secondmasktable) + (dst_positive_scale_sum_unique_secondmasktable)) * S ((dst_positive_code_sum_unique_secondmasktable) + (dst_positive_scale_sum_unique_secondmasktable)) + ((dst_positive_scale_sum_unique_secondmasktable) + (dst_positive_scale_sum_unique_secondmasktable))) + (((dst_negative_code_sum_unique_secondmasktable) + (dst_negative_scale_sum_unique_secondmasktable)) * S ((dst_negative_code_sum_unique_secondmasktable) + (dst_negative_scale_sum_unique_secondmasktable)) + ((dst_negative_scale_sum_unique_secondmasktable) + (dst_negative_scale_sum_unique_secondmasktable)))) * S ((((dst_positive_code_sum_unique_secondmasktable) + (dst_positive_scale_sum_unique_secondmasktable)) * S ((dst_positive_code_sum_unique_secondmasktable) + (dst_positive_scale_sum_unique_secondmasktable)) + ((dst_positive_scale_sum_unique_secondmasktable) + (dst_positive_scale_sum_unique_secondmasktable))) + (((dst_negative_code_sum_unique_secondmasktable) + (dst_negative_scale_sum_unique_secondmasktable)) * S ((dst_negative_code_sum_unique_secondmasktable) + (dst_negative_scale_sum_unique_secondmasktable)) + ((dst_negative_scale_sum_unique_secondmasktable) + (dst_negative_scale_sum_unique_secondmasktable)))) + ((((dst_negative_code_sum_unique_secondmasktable) + (dst_negative_scale_sum_unique_secondmasktable)) * S ((dst_negative_code_sum_unique_secondmasktable) + (dst_negative_scale_sum_unique_secondmasktable)) + ((dst_negative_scale_sum_unique_secondmasktable) + (dst_negative_scale_sum_unique_secondmasktable))) + (((dst_negative_code_sum_unique_secondmasktable) + (dst_negative_scale_sum_unique_secondmasktable)) * S ((dst_negative_code_sum_unique_secondmasktable) + (dst_negative_scale_sum_unique_secondmasktable)) + ((dst_negative_scale_sum_unique_secondmasktable) + (dst_negative_scale_sum_unique_secondmasktable)))))) /\ (forall dst_index_sum_unique_secondmasktable. (exists pvs_le_gap_sum_unique_secondmasktabledomain. pvs_le_gap_sum_unique_secondmasktabledomain + (dst_index_sum_unique_secondmasktable) = (n)) -> exists dst_positive_sum_unique_secondmasktable dst_negative_sum_unique_secondmasktable dst_value_sum_unique_secondmasktable. ((((exists ff_h_pvs_sum_unique_secondmasktableentrypositive. ff_h_pvs_sum_unique_secondmasktableentrypositive + S (dst_positive_sum_unique_secondmasktable) = S ((S (dst_index_sum_unique_secondmasktable)) * dst_positive_scale_sum_unique_secondmasktable)) /\ exists ff_q_pvs_sum_unique_secondmasktableentrypositive. dst_positive_code_sum_unique_secondmasktable = ff_q_pvs_sum_unique_secondmasktableentrypositive * S ((S (dst_index_sum_unique_secondmasktable)) * dst_positive_scale_sum_unique_secondmasktable) + (dst_positive_sum_unique_secondmasktable))) /\ (((((exists ff_h_pvs_sum_unique_secondmasktableentrynegative. ff_h_pvs_sum_unique_secondmasktableentrynegative + S (dst_negative_sum_unique_secondmasktable) = S ((S (dst_index_sum_unique_secondmasktable)) * dst_negative_scale_sum_unique_secondmasktable)) /\ exists ff_q_pvs_sum_unique_secondmasktableentrynegative. dst_negative_code_sum_unique_secondmasktable = ff_q_pvs_sum_unique_secondmasktableentrynegative * S ((S (dst_index_sum_unique_secondmasktable)) * dst_negative_scale_sum_unique_secondmasktable) + (dst_negative_sum_unique_secondmasktable))) /\ (exists ge_balance_positive_sum_unique_secondmasktableentryvalue ge_balance_negative_sum_unique_secondmasktableentryvalue. (((((dst_value_sum_unique_secondmasktable) = 2 * (ge_balance_positive_sum_unique_secondmasktableentryvalue) /\ (ge_balance_negative_sum_unique_secondmasktableentryvalue) = 0) \/ exists ge_signed_half_sum_unique_secondmasktableentryvaluedecode. (((dst_value_sum_unique_secondmasktable) = 2 * ge_signed_half_sum_unique_secondmasktableentryvaluedecode + 1 /\ (ge_balance_positive_sum_unique_secondmasktableentryvalue) = 0) /\ (ge_balance_negative_sum_unique_secondmasktableentryvalue) = S ge_signed_half_sum_unique_secondmasktableentryvaluedecode))) /\ ((dst_positive_sum_unique_secondmasktable) + ge_balance_negative_sum_unique_secondmasktableentryvalue = (dst_negative_sum_unique_secondmasktable) + ge_balance_positive_sum_unique_secondmasktableentryvalue))))))))) /\ (forall dm_index_sum_unique_secondmask dm_value_sum_unique_secondmask. (exists pvs_le_gap_sum_unique_secondmaskdomain. pvs_le_gap_sum_unique_secondmaskdomain + (dm_index_sum_unique_secondmask) = (n)) -> (exists dst_positive_code_sum_unique_secondmasklookup dst_positive_scale_sum_unique_secondmasklookup dst_negative_code_sum_unique_secondmasklookup dst_negative_scale_sum_unique_secondmasklookup dst_positive_sum_unique_secondmasklookup dst_negative_sum_unique_secondmasklookup. (((dm_mask_table_sum_unique_second) = (((((dst_positive_code_sum_unique_secondmasklookup) + (dst_positive_scale_sum_unique_secondmasklookup)) * S ((dst_positive_code_sum_unique_secondmasklookup) + (dst_positive_scale_sum_unique_secondmasklookup)) + ((dst_positive_scale_sum_unique_secondmasklookup) + (dst_positive_scale_sum_unique_secondmasklookup))) + (((dst_negative_code_sum_unique_secondmasklookup) + (dst_negative_scale_sum_unique_secondmasklookup)) * S ((dst_negative_code_sum_unique_secondmasklookup) + (dst_negative_scale_sum_unique_secondmasklookup)) + ((dst_negative_scale_sum_unique_secondmasklookup) + (dst_negative_scale_sum_unique_secondmasklookup)))) * S ((((dst_positive_code_sum_unique_secondmasklookup) + (dst_positive_scale_sum_unique_secondmasklookup)) * S ((dst_positive_code_sum_unique_secondmasklookup) + (dst_positive_scale_sum_unique_secondmasklookup)) + ((dst_positive_scale_sum_unique_secondmasklookup) + (dst_positive_scale_sum_unique_secondmasklookup))) + (((dst_negative_code_sum_unique_secondmasklookup) + (dst_negative_scale_sum_unique_secondmasklookup)) * S ((dst_negative_code_sum_unique_secondmasklookup) + (dst_negative_scale_sum_unique_secondmasklookup)) + ((dst_negative_scale_sum_unique_secondmasklookup) + (dst_negative_scale_sum_unique_secondmasklookup)))) + ((((dst_negative_code_sum_unique_secondmasklookup) + (dst_negative_scale_sum_unique_secondmasklookup)) * S ((dst_negative_code_sum_unique_secondmasklookup) + (dst_negative_scale_sum_unique_secondmasklookup)) + ((dst_negative_scale_sum_unique_secondmasklookup) + (dst_negative_scale_sum_unique_secondmasklookup))) + (((dst_negative_code_sum_unique_secondmasklookup) + (dst_negative_scale_sum_unique_secondmasklookup)) * S ((dst_negative_code_sum_unique_secondmasklookup) + (dst_negative_scale_sum_unique_secondmasklookup)) + ((dst_negative_scale_sum_unique_secondmasklookup) + (dst_negative_scale_sum_unique_secondmasklookup)))))) /\ (((((exists ff_h_pvs_sum_unique_secondmasklookuppositive. ff_h_pvs_sum_unique_secondmasklookuppositive + S (dst_positive_sum_unique_secondmasklookup) = S ((S (dm_index_sum_unique_secondmask)) * dst_positive_scale_sum_unique_secondmasklookup)) /\ exists ff_q_pvs_sum_unique_secondmasklookuppositive. dst_positive_code_sum_unique_secondmasklookup = ff_q_pvs_sum_unique_secondmasklookuppositive * S ((S (dm_index_sum_unique_secondmask)) * dst_positive_scale_sum_unique_secondmasklookup) + (dst_positive_sum_unique_secondmasklookup))) /\ (((((exists ff_h_pvs_sum_unique_secondmasklookupnegative. ff_h_pvs_sum_unique_secondmasklookupnegative + S (dst_negative_sum_unique_secondmasklookup) = S ((S (dm_index_sum_unique_secondmask)) * dst_negative_scale_sum_unique_secondmasklookup)) /\ exists ff_q_pvs_sum_unique_secondmasklookupnegative. dst_negative_code_sum_unique_secondmasklookup = ff_q_pvs_sum_unique_secondmasklookupnegative * S ((S (dm_index_sum_unique_secondmask)) * dst_negative_scale_sum_unique_secondmasklookup) + (dst_negative_sum_unique_secondmasklookup))) /\ (exists ge_balance_positive_sum_unique_secondmasklookupvalue ge_balance_negative_sum_unique_secondmasklookupvalue. (((((dm_value_sum_unique_secondmask) = 2 * (ge_balance_positive_sum_unique_secondmasklookupvalue) /\ (ge_balance_negative_sum_unique_secondmasklookupvalue) = 0) \/ exists ge_signed_half_sum_unique_secondmasklookupvaluedecode. (((dm_value_sum_unique_secondmask) = 2 * ge_signed_half_sum_unique_secondmasklookupvaluedecode + 1 /\ (ge_balance_positive_sum_unique_secondmasklookupvalue) = 0) /\ (ge_balance_negative_sum_unique_secondmasklookupvalue) = S ge_signed_half_sum_unique_secondmasklookupvaluedecode))) /\ ((dst_positive_sum_unique_secondmasklookup) + ge_balance_negative_sum_unique_secondmasklookupvalue = (dst_negative_sum_unique_secondmasklookup) + ge_balance_positive_sum_unique_secondmasklookupvalue))))))))) -> ((((~((dm_index_sum_unique_secondmask)=0)) /\ (exists dm_quotient_sum_unique_secondmaskentry. (((n)=(dm_index_sum_unique_secondmask)*dm_quotient_sum_unique_secondmaskentry) /\ (exists dst_positive_code_sum_unique_secondmaskentryinput dst_positive_scale_sum_unique_secondmaskentryinput dst_negative_code_sum_unique_secondmaskentryinput dst_negative_scale_sum_unique_secondmaskentryinput dst_positive_sum_unique_secondmaskentryinput dst_negative_sum_unique_secondmaskentryinput. (((F) = (((((dst_positive_code_sum_unique_secondmaskentryinput) + (dst_positive_scale_sum_unique_secondmaskentryinput)) * S ((dst_positive_code_sum_unique_secondmaskentryinput) + (dst_positive_scale_sum_unique_secondmaskentryinput)) + ((dst_positive_scale_sum_unique_secondmaskentryinput) + (dst_positive_scale_sum_unique_secondmaskentryinput))) + (((dst_negative_code_sum_unique_secondmaskentryinput) + (dst_negative_scale_sum_unique_secondmaskentryinput)) * S ((dst_negative_code_sum_unique_secondmaskentryinput) + (dst_negative_scale_sum_unique_secondmaskentryinput)) + ((dst_negative_scale_sum_unique_secondmaskentryinput) + (dst_negative_scale_sum_unique_secondmaskentryinput)))) * S ((((dst_positive_code_sum_unique_secondmaskentryinput) + (dst_positive_scale_sum_unique_secondmaskentryinput)) * S ((dst_positive_code_sum_unique_secondmaskentryinput) + (dst_positive_scale_sum_unique_secondmaskentryinput)) + ((dst_positive_scale_sum_unique_secondmaskentryinput) + (dst_positive_scale_sum_unique_secondmaskentryinput))) + (((dst_negative_code_sum_unique_secondmaskentryinput) + (dst_negative_scale_sum_unique_secondmaskentryinput)) * S ((dst_negative_code_sum_unique_secondmaskentryinput) + (dst_negative_scale_sum_unique_secondmaskentryinput)) + ((dst_negative_scale_sum_unique_secondmaskentryinput) + (dst_negative_scale_sum_unique_secondmaskentryinput)))) + ((((dst_negative_code_sum_unique_secondmaskentryinput) + (dst_negative_scale_sum_unique_secondmaskentryinput)) * S ((dst_negative_code_sum_unique_secondmaskentryinput) + (dst_negative_scale_sum_unique_secondmaskentryinput)) + ((dst_negative_scale_sum_unique_secondmaskentryinput) + (dst_negative_scale_sum_unique_secondmaskentryinput))) + (((dst_negative_code_sum_unique_secondmaskentryinput) + (dst_negative_scale_sum_unique_secondmaskentryinput)) * S ((dst_negative_code_sum_unique_secondmaskentryinput) + (dst_negative_scale_sum_unique_secondmaskentryinput)) + ((dst_negative_scale_sum_unique_secondmaskentryinput) + (dst_negative_scale_sum_unique_secondmaskentryinput)))))) /\ (((((exists ff_h_pvs_sum_unique_secondmaskentryinputpositive. ff_h_pvs_sum_unique_secondmaskentryinputpositive + S (dst_positive_sum_unique_secondmaskentryinput) = S ((S (dm_index_sum_unique_secondmask)) * dst_positive_scale_sum_unique_secondmaskentryinput)) /\ exists ff_q_pvs_sum_unique_secondmaskentryinputpositive. dst_positive_code_sum_unique_secondmaskentryinput = ff_q_pvs_sum_unique_secondmaskentryinputpositive * S ((S (dm_index_sum_unique_secondmask)) * dst_positive_scale_sum_unique_secondmaskentryinput) + (dst_positive_sum_unique_secondmaskentryinput))) /\ (((((exists ff_h_pvs_sum_unique_secondmaskentryinputnegative. ff_h_pvs_sum_unique_secondmaskentryinputnegative + S (dst_negative_sum_unique_secondmaskentryinput) = S ((S (dm_index_sum_unique_secondmask)) * dst_negative_scale_sum_unique_secondmaskentryinput)) /\ exists ff_q_pvs_sum_unique_secondmaskentryinputnegative. dst_negative_code_sum_unique_secondmaskentryinput = ff_q_pvs_sum_unique_secondmaskentryinputnegative * S ((S (dm_index_sum_unique_secondmask)) * dst_negative_scale_sum_unique_secondmaskentryinput) + (dst_negative_sum_unique_secondmaskentryinput))) /\ (exists ge_balance_positive_sum_unique_secondmaskentryinputvalue ge_balance_negative_sum_unique_secondmaskentryinputvalue. (((((dm_value_sum_unique_secondmask) = 2 * (ge_balance_positive_sum_unique_secondmaskentryinputvalue) /\ (ge_balance_negative_sum_unique_secondmaskentryinputvalue) = 0) \/ exists ge_signed_half_sum_unique_secondmaskentryinputvaluedecode. (((dm_value_sum_unique_secondmask) = 2 * ge_signed_half_sum_unique_secondmaskentryinputvaluedecode + 1 /\ (ge_balance_positive_sum_unique_secondmaskentryinputvalue) = 0) /\ (ge_balance_negative_sum_unique_secondmaskentryinputvalue) = S ge_signed_half_sum_unique_secondmaskentryinputvaluedecode))) /\ ((dst_positive_sum_unique_secondmaskentryinput) + ge_balance_negative_sum_unique_secondmaskentryinputvalue = (dst_negative_sum_unique_secondmaskentryinput) + ge_balance_positive_sum_unique_secondmaskentryinputvalue))))))))))))) \/ ((((dm_index_sum_unique_secondmask)=0 \/ ~(exists pvs_factor_sum_unique_secondmaskentrynondivisor. (n) = (dm_index_sum_unique_secondmask) * pvs_factor_sum_unique_secondmaskentrynondivisor)) /\ ((dm_value_sum_unique_secondmask)=0))))))) /\ (exists dst_positive_code_sum_unique_secondfold dst_positive_scale_sum_unique_secondfold dst_negative_code_sum_unique_secondfold dst_negative_scale_sum_unique_secondfold dst_positive_sum_sum_unique_secondfold dst_negative_sum_sum_unique_secondfold. (((dm_mask_table_sum_unique_second) = (((((dst_positive_code_sum_unique_secondfold) + (dst_positive_scale_sum_unique_secondfold)) * S ((dst_positive_code_sum_unique_secondfold) + (dst_positive_scale_sum_unique_secondfold)) + ((dst_positive_scale_sum_unique_secondfold) + (dst_positive_scale_sum_unique_secondfold))) + (((dst_negative_code_sum_unique_secondfold) + (dst_negative_scale_sum_unique_secondfold)) * S ((dst_negative_code_sum_unique_secondfold) + (dst_negative_scale_sum_unique_secondfold)) + ((dst_negative_scale_sum_unique_secondfold) + (dst_negative_scale_sum_unique_secondfold)))) * S ((((dst_positive_code_sum_unique_secondfold) + (dst_positive_scale_sum_unique_secondfold)) * S ((dst_positive_code_sum_unique_secondfold) + (dst_positive_scale_sum_unique_secondfold)) + ((dst_positive_scale_sum_unique_secondfold) + (dst_positive_scale_sum_unique_secondfold))) + (((dst_negative_code_sum_unique_secondfold) + (dst_negative_scale_sum_unique_secondfold)) * S ((dst_negative_code_sum_unique_secondfold) + (dst_negative_scale_sum_unique_secondfold)) + ((dst_negative_scale_sum_unique_secondfold) + (dst_negative_scale_sum_unique_secondfold)))) + ((((dst_negative_code_sum_unique_secondfold) + (dst_negative_scale_sum_unique_secondfold)) * S ((dst_negative_code_sum_unique_secondfold) + (dst_negative_scale_sum_unique_secondfold)) + ((dst_negative_scale_sum_unique_secondfold) + (dst_negative_scale_sum_unique_secondfold))) + (((dst_negative_code_sum_unique_secondfold) + (dst_negative_scale_sum_unique_secondfold)) * S ((dst_negative_code_sum_unique_secondfold) + (dst_negative_scale_sum_unique_secondfold)) + ((dst_negative_scale_sum_unique_secondfold) + (dst_negative_scale_sum_unique_secondfold)))))) /\ (((exists fs_u_dst_sum_unique_secondfoldpositive fs_v_dst_sum_unique_secondfoldpositive. ((((exists fs_h_dst_sum_unique_secondfoldpositive_body_start. fs_h_dst_sum_unique_secondfoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_sum_unique_secondfoldpositive)) /\ exists fs_q_dst_sum_unique_secondfoldpositive_body_start. fs_u_dst_sum_unique_secondfoldpositive = fs_q_dst_sum_unique_secondfoldpositive_body_start * S ((S (0)) * fs_v_dst_sum_unique_secondfoldpositive) + (0))) /\ ((((exists fs_h_dst_sum_unique_secondfoldpositive_body_terminal. fs_h_dst_sum_unique_secondfoldpositive_body_terminal + S (dst_positive_sum_sum_unique_secondfold) = S ((S (S (n))) * fs_v_dst_sum_unique_secondfoldpositive)) /\ exists fs_q_dst_sum_unique_secondfoldpositive_body_terminal. fs_u_dst_sum_unique_secondfoldpositive = fs_q_dst_sum_unique_secondfoldpositive_body_terminal * S ((S (S (n))) * fs_v_dst_sum_unique_secondfoldpositive) + (dst_positive_sum_sum_unique_secondfold))) /\ forall fs_i_dst_sum_unique_secondfoldpositive_body_steps. (exists fs_lt_dst_sum_unique_secondfoldpositive_body_steps_bound. fs_lt_dst_sum_unique_secondfoldpositive_body_steps_bound + S fs_i_dst_sum_unique_secondfoldpositive_body_steps = S (n)) -> exists fs_a_dst_sum_unique_secondfoldpositive_body_steps fs_r_dst_sum_unique_secondfoldpositive_body_steps fs_s_dst_sum_unique_secondfoldpositive_body_steps. ((((exists fs_h_dst_sum_unique_secondfoldpositive_body_steps_summand. fs_h_dst_sum_unique_secondfoldpositive_body_steps_summand + S (fs_a_dst_sum_unique_secondfoldpositive_body_steps) = S ((S (fs_i_dst_sum_unique_secondfoldpositive_body_steps)) * dst_positive_scale_sum_unique_secondfold)) /\ exists fs_q_dst_sum_unique_secondfoldpositive_body_steps_summand. dst_positive_code_sum_unique_secondfold = fs_q_dst_sum_unique_secondfoldpositive_body_steps_summand * S ((S (fs_i_dst_sum_unique_secondfoldpositive_body_steps)) * dst_positive_scale_sum_unique_secondfold) + (fs_a_dst_sum_unique_secondfoldpositive_body_steps))) /\ ((((exists fs_h_dst_sum_unique_secondfoldpositive_body_steps_partial. fs_h_dst_sum_unique_secondfoldpositive_body_steps_partial + S (fs_r_dst_sum_unique_secondfoldpositive_body_steps) = S ((S (fs_i_dst_sum_unique_secondfoldpositive_body_steps)) * fs_v_dst_sum_unique_secondfoldpositive)) /\ exists fs_q_dst_sum_unique_secondfoldpositive_body_steps_partial. fs_u_dst_sum_unique_secondfoldpositive = fs_q_dst_sum_unique_secondfoldpositive_body_steps_partial * S ((S (fs_i_dst_sum_unique_secondfoldpositive_body_steps)) * fs_v_dst_sum_unique_secondfoldpositive) + (fs_r_dst_sum_unique_secondfoldpositive_body_steps))) /\ ((((exists fs_h_dst_sum_unique_secondfoldpositive_body_steps_successor. fs_h_dst_sum_unique_secondfoldpositive_body_steps_successor + S (fs_s_dst_sum_unique_secondfoldpositive_body_steps) = S ((S (S fs_i_dst_sum_unique_secondfoldpositive_body_steps)) * fs_v_dst_sum_unique_secondfoldpositive)) /\ exists fs_q_dst_sum_unique_secondfoldpositive_body_steps_successor. fs_u_dst_sum_unique_secondfoldpositive = fs_q_dst_sum_unique_secondfoldpositive_body_steps_successor * S ((S (S fs_i_dst_sum_unique_secondfoldpositive_body_steps)) * fs_v_dst_sum_unique_secondfoldpositive) + (fs_s_dst_sum_unique_secondfoldpositive_body_steps))) /\ fs_s_dst_sum_unique_secondfoldpositive_body_steps = fs_r_dst_sum_unique_secondfoldpositive_body_steps + fs_a_dst_sum_unique_secondfoldpositive_body_steps)))))) /\ (((exists fs_u_dst_sum_unique_secondfoldnegative fs_v_dst_sum_unique_secondfoldnegative. ((((exists fs_h_dst_sum_unique_secondfoldnegative_body_start. fs_h_dst_sum_unique_secondfoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_sum_unique_secondfoldnegative)) /\ exists fs_q_dst_sum_unique_secondfoldnegative_body_start. fs_u_dst_sum_unique_secondfoldnegative = fs_q_dst_sum_unique_secondfoldnegative_body_start * S ((S (0)) * fs_v_dst_sum_unique_secondfoldnegative) + (0))) /\ ((((exists fs_h_dst_sum_unique_secondfoldnegative_body_terminal. fs_h_dst_sum_unique_secondfoldnegative_body_terminal + S (dst_negative_sum_sum_unique_secondfold) = S ((S (S (n))) * fs_v_dst_sum_unique_secondfoldnegative)) /\ exists fs_q_dst_sum_unique_secondfoldnegative_body_terminal. fs_u_dst_sum_unique_secondfoldnegative = fs_q_dst_sum_unique_secondfoldnegative_body_terminal * S ((S (S (n))) * fs_v_dst_sum_unique_secondfoldnegative) + (dst_negative_sum_sum_unique_secondfold))) /\ forall fs_i_dst_sum_unique_secondfoldnegative_body_steps. (exists fs_lt_dst_sum_unique_secondfoldnegative_body_steps_bound. fs_lt_dst_sum_unique_secondfoldnegative_body_steps_bound + S fs_i_dst_sum_unique_secondfoldnegative_body_steps = S (n)) -> exists fs_a_dst_sum_unique_secondfoldnegative_body_steps fs_r_dst_sum_unique_secondfoldnegative_body_steps fs_s_dst_sum_unique_secondfoldnegative_body_steps. ((((exists fs_h_dst_sum_unique_secondfoldnegative_body_steps_summand. fs_h_dst_sum_unique_secondfoldnegative_body_steps_summand + S (fs_a_dst_sum_unique_secondfoldnegative_body_steps) = S ((S (fs_i_dst_sum_unique_secondfoldnegative_body_steps)) * dst_negative_scale_sum_unique_secondfold)) /\ exists fs_q_dst_sum_unique_secondfoldnegative_body_steps_summand. dst_negative_code_sum_unique_secondfold = fs_q_dst_sum_unique_secondfoldnegative_body_steps_summand * S ((S (fs_i_dst_sum_unique_secondfoldnegative_body_steps)) * dst_negative_scale_sum_unique_secondfold) + (fs_a_dst_sum_unique_secondfoldnegative_body_steps))) /\ ((((exists fs_h_dst_sum_unique_secondfoldnegative_body_steps_partial. fs_h_dst_sum_unique_secondfoldnegative_body_steps_partial + S (fs_r_dst_sum_unique_secondfoldnegative_body_steps) = S ((S (fs_i_dst_sum_unique_secondfoldnegative_body_steps)) * fs_v_dst_sum_unique_secondfoldnegative)) /\ exists fs_q_dst_sum_unique_secondfoldnegative_body_steps_partial. fs_u_dst_sum_unique_secondfoldnegative = fs_q_dst_sum_unique_secondfoldnegative_body_steps_partial * S ((S (fs_i_dst_sum_unique_secondfoldnegative_body_steps)) * fs_v_dst_sum_unique_secondfoldnegative) + (fs_r_dst_sum_unique_secondfoldnegative_body_steps))) /\ ((((exists fs_h_dst_sum_unique_secondfoldnegative_body_steps_successor. fs_h_dst_sum_unique_secondfoldnegative_body_steps_successor + S (fs_s_dst_sum_unique_secondfoldnegative_body_steps) = S ((S (S fs_i_dst_sum_unique_secondfoldnegative_body_steps)) * fs_v_dst_sum_unique_secondfoldnegative)) /\ exists fs_q_dst_sum_unique_secondfoldnegative_body_steps_successor. fs_u_dst_sum_unique_secondfoldnegative = fs_q_dst_sum_unique_secondfoldnegative_body_steps_successor * S ((S (S fs_i_dst_sum_unique_secondfoldnegative_body_steps)) * fs_v_dst_sum_unique_secondfoldnegative) + (fs_s_dst_sum_unique_secondfoldnegative_body_steps))) /\ fs_s_dst_sum_unique_secondfoldnegative_body_steps = fs_r_dst_sum_unique_secondfoldnegative_body_steps + fs_a_dst_sum_unique_secondfoldnegative_body_steps)))))) /\ (exists ge_balance_positive_sum_unique_secondfoldresult ge_balance_negative_sum_unique_secondfoldresult. (((((b) = 2 * (ge_balance_positive_sum_unique_secondfoldresult) /\ (ge_balance_negative_sum_unique_secondfoldresult) = 0) \/ exists ge_signed_half_sum_unique_secondfoldresultdecode. (((b) = 2 * ge_signed_half_sum_unique_secondfoldresultdecode + 1 /\ (ge_balance_positive_sum_unique_secondfoldresult) = 0) /\ (ge_balance_negative_sum_unique_secondfoldresult) = S ge_signed_half_sum_unique_secondfoldresultdecode))) /\ ((dst_positive_sum_sum_unique_secondfold) + ge_balance_negative_sum_unique_secondfoldresult = (dst_negative_sum_sum_unique_secondfold) + ge_balance_positive_sum_unique_secondfoldresult))))))))))))) -> a=b