signed_divisor_sum_one

forall N F a. (exists dst_positive_code_sum_one_input dst_positive_scale_sum_one_input dst_negative_code_sum_one_input dst_negative_scale_sum_one_input. (((F) = (((((dst_positive_code_sum_one_input) + (dst_positive_scale_sum_one_input)) * S ((dst_positive_code_sum_one_input) + (dst_positive_scale_sum_one_input)) + ((dst_positive_scale_sum_one_input) + (dst_positive_scale_sum_one_input))) + (((dst_negative_code_sum_one_input) + (dst_negative_scale_sum_one_input)) * S ((dst_negative_code_sum_one_input) + (dst_negative_scale_sum_one_input)) + ((dst_negative_scale_sum_one_input) + (dst_negative_scale_sum_one_input)))) * S ((((dst_positive_code_sum_one_input) + (dst_positive_scale_sum_one_input)) * S ((dst_positive_code_sum_one_input) + (dst_positive_scale_sum_one_input)) + ((dst_positive_scale_sum_one_input) + (dst_positive_scale_sum_one_input))) + (((dst_negative_code_sum_one_input) + (dst_negative_scale_sum_one_input)) * S ((dst_negative_code_sum_one_input) + (dst_negative_scale_sum_one_input)) + ((dst_negative_scale_sum_one_input) + (dst_negative_scale_sum_one_input)))) + ((((dst_negative_code_sum_one_input) + (dst_negative_scale_sum_one_input)) * S ((dst_negative_code_sum_one_input) + (dst_negative_scale_sum_one_input)) + ((dst_negative_scale_sum_one_input) + (dst_negative_scale_sum_one_input))) + (((dst_negative_code_sum_one_input) + (dst_negative_scale_sum_one_input)) * S ((dst_negative_code_sum_one_input) + (dst_negative_scale_sum_one_input)) + ((dst_negative_scale_sum_one_input) + (dst_negative_scale_sum_one_input)))))) /\ (forall dst_index_sum_one_input. (exists pvs_le_gap_sum_one_inputdomain. pvs_le_gap_sum_one_inputdomain + (dst_index_sum_one_input) = (N)) -> exists dst_positive_sum_one_input dst_negative_sum_one_input dst_value_sum_one_input. ((((exists ff_h_pvs_sum_one_inputentrypositive. ff_h_pvs_sum_one_inputentrypositive + S (dst_positive_sum_one_input) = S ((S (dst_index_sum_one_input)) * dst_positive_scale_sum_one_input)) /\ exists ff_q_pvs_sum_one_inputentrypositive. dst_positive_code_sum_one_input = ff_q_pvs_sum_one_inputentrypositive * S ((S (dst_index_sum_one_input)) * dst_positive_scale_sum_one_input) + (dst_positive_sum_one_input))) /\ (((((exists ff_h_pvs_sum_one_inputentrynegative. ff_h_pvs_sum_one_inputentrynegative + S (dst_negative_sum_one_input) = S ((S (dst_index_sum_one_input)) * dst_negative_scale_sum_one_input)) /\ exists ff_q_pvs_sum_one_inputentrynegative. dst_negative_code_sum_one_input = ff_q_pvs_sum_one_inputentrynegative * S ((S (dst_index_sum_one_input)) * dst_negative_scale_sum_one_input) + (dst_negative_sum_one_input))) /\ (exists ge_balance_positive_sum_one_inputentryvalue ge_balance_negative_sum_one_inputentryvalue. (((((dst_value_sum_one_input) = 2 * (ge_balance_positive_sum_one_inputentryvalue) /\ (ge_balance_negative_sum_one_inputentryvalue) = 0) \/ exists ge_signed_half_sum_one_inputentryvaluedecode. (((dst_value_sum_one_input) = 2 * ge_signed_half_sum_one_inputentryvaluedecode + 1 /\ (ge_balance_positive_sum_one_inputentryvalue) = 0) /\ (ge_balance_negative_sum_one_inputentryvalue) = S ge_signed_half_sum_one_inputentryvaluedecode))) /\ ((dst_positive_sum_one_input) + ge_balance_negative_sum_one_inputentryvalue = (dst_negative_sum_one_input) + ge_balance_positive_sum_one_inputentryvalue))))))))) -> (exists pvs_le_gap_sum_one_bound. pvs_le_gap_sum_one_bound + (1) = (N)) -> (exists dst_positive_code_sum_one_entry dst_positive_scale_sum_one_entry dst_negative_code_sum_one_entry dst_negative_scale_sum_one_entry dst_positive_sum_one_entry dst_negative_sum_one_entry. (((F) = (((((dst_positive_code_sum_one_entry) + (dst_positive_scale_sum_one_entry)) * S ((dst_positive_code_sum_one_entry) + (dst_positive_scale_sum_one_entry)) + ((dst_positive_scale_sum_one_entry) + (dst_positive_scale_sum_one_entry))) + (((dst_negative_code_sum_one_entry) + (dst_negative_scale_sum_one_entry)) * S ((dst_negative_code_sum_one_entry) + (dst_negative_scale_sum_one_entry)) + ((dst_negative_scale_sum_one_entry) + (dst_negative_scale_sum_one_entry)))) * S ((((dst_positive_code_sum_one_entry) + (dst_positive_scale_sum_one_entry)) * S ((dst_positive_code_sum_one_entry) + (dst_positive_scale_sum_one_entry)) + ((dst_positive_scale_sum_one_entry) + (dst_positive_scale_sum_one_entry))) + (((dst_negative_code_sum_one_entry) + (dst_negative_scale_sum_one_entry)) * S ((dst_negative_code_sum_one_entry) + (dst_negative_scale_sum_one_entry)) + ((dst_negative_scale_sum_one_entry) + (dst_negative_scale_sum_one_entry)))) + ((((dst_negative_code_sum_one_entry) + (dst_negative_scale_sum_one_entry)) * S ((dst_negative_code_sum_one_entry) + (dst_negative_scale_sum_one_entry)) + ((dst_negative_scale_sum_one_entry) + (dst_negative_scale_sum_one_entry))) + (((dst_negative_code_sum_one_entry) + (dst_negative_scale_sum_one_entry)) * S ((dst_negative_code_sum_one_entry) + (dst_negative_scale_sum_one_entry)) + ((dst_negative_scale_sum_one_entry) + (dst_negative_scale_sum_one_entry)))))) /\ (((((exists ff_h_pvs_sum_one_entrypositive. ff_h_pvs_sum_one_entrypositive + S (dst_positive_sum_one_entry) = S ((S (1)) * dst_positive_scale_sum_one_entry)) /\ exists ff_q_pvs_sum_one_entrypositive. dst_positive_code_sum_one_entry = ff_q_pvs_sum_one_entrypositive * S ((S (1)) * dst_positive_scale_sum_one_entry) + (dst_positive_sum_one_entry))) /\ (((((exists ff_h_pvs_sum_one_entrynegative. ff_h_pvs_sum_one_entrynegative + S (dst_negative_sum_one_entry) = S ((S (1)) * dst_negative_scale_sum_one_entry)) /\ exists ff_q_pvs_sum_one_entrynegative. dst_negative_code_sum_one_entry = ff_q_pvs_sum_one_entrynegative * S ((S (1)) * dst_negative_scale_sum_one_entry) + (dst_negative_sum_one_entry))) /\ (exists ge_balance_positive_sum_one_entryvalue ge_balance_negative_sum_one_entryvalue. (((((a) = 2 * (ge_balance_positive_sum_one_entryvalue) /\ (ge_balance_negative_sum_one_entryvalue) = 0) \/ exists ge_signed_half_sum_one_entryvaluedecode. (((a) = 2 * ge_signed_half_sum_one_entryvaluedecode + 1 /\ (ge_balance_positive_sum_one_entryvalue) = 0) /\ (ge_balance_negative_sum_one_entryvalue) = S ge_signed_half_sum_one_entryvaluedecode))) /\ ((dst_positive_sum_one_entry) + ge_balance_negative_sum_one_entryvalue = (dst_negative_sum_one_entry) + ge_balance_positive_sum_one_entryvalue))))))))) -> (((~((1)=0)) /\ (exists dm_mask_table_sum_one_result. ((((exists dst_positive_code_sum_one_resultmasktable dst_positive_scale_sum_one_resultmasktable dst_negative_code_sum_one_resultmasktable dst_negative_scale_sum_one_resultmasktable. (((dm_mask_table_sum_one_result) = (((((dst_positive_code_sum_one_resultmasktable) + (dst_positive_scale_sum_one_resultmasktable)) * S ((dst_positive_code_sum_one_resultmasktable) + (dst_positive_scale_sum_one_resultmasktable)) + ((dst_positive_scale_sum_one_resultmasktable) + (dst_positive_scale_sum_one_resultmasktable))) + (((dst_negative_code_sum_one_resultmasktable) + (dst_negative_scale_sum_one_resultmasktable)) * S ((dst_negative_code_sum_one_resultmasktable) + (dst_negative_scale_sum_one_resultmasktable)) + ((dst_negative_scale_sum_one_resultmasktable) + (dst_negative_scale_sum_one_resultmasktable)))) * S ((((dst_positive_code_sum_one_resultmasktable) + (dst_positive_scale_sum_one_resultmasktable)) * S ((dst_positive_code_sum_one_resultmasktable) + (dst_positive_scale_sum_one_resultmasktable)) + ((dst_positive_scale_sum_one_resultmasktable) + (dst_positive_scale_sum_one_resultmasktable))) + (((dst_negative_code_sum_one_resultmasktable) + (dst_negative_scale_sum_one_resultmasktable)) * S ((dst_negative_code_sum_one_resultmasktable) + (dst_negative_scale_sum_one_resultmasktable)) + ((dst_negative_scale_sum_one_resultmasktable) + (dst_negative_scale_sum_one_resultmasktable)))) + ((((dst_negative_code_sum_one_resultmasktable) + (dst_negative_scale_sum_one_resultmasktable)) * S ((dst_negative_code_sum_one_resultmasktable) + (dst_negative_scale_sum_one_resultmasktable)) + ((dst_negative_scale_sum_one_resultmasktable) + (dst_negative_scale_sum_one_resultmasktable))) + (((dst_negative_code_sum_one_resultmasktable) + (dst_negative_scale_sum_one_resultmasktable)) * S ((dst_negative_code_sum_one_resultmasktable) + (dst_negative_scale_sum_one_resultmasktable)) + ((dst_negative_scale_sum_one_resultmasktable) + (dst_negative_scale_sum_one_resultmasktable)))))) /\ (forall dst_index_sum_one_resultmasktable. (exists pvs_le_gap_sum_one_resultmasktabledomain. pvs_le_gap_sum_one_resultmasktabledomain + (dst_index_sum_one_resultmasktable) = (1)) -> exists dst_positive_sum_one_resultmasktable dst_negative_sum_one_resultmasktable dst_value_sum_one_resultmasktable. ((((exists ff_h_pvs_sum_one_resultmasktableentrypositive. ff_h_pvs_sum_one_resultmasktableentrypositive + S (dst_positive_sum_one_resultmasktable) = S ((S (dst_index_sum_one_resultmasktable)) * dst_positive_scale_sum_one_resultmasktable)) /\ exists ff_q_pvs_sum_one_resultmasktableentrypositive. dst_positive_code_sum_one_resultmasktable = ff_q_pvs_sum_one_resultmasktableentrypositive * S ((S (dst_index_sum_one_resultmasktable)) * dst_positive_scale_sum_one_resultmasktable) + (dst_positive_sum_one_resultmasktable))) /\ (((((exists ff_h_pvs_sum_one_resultmasktableentrynegative. ff_h_pvs_sum_one_resultmasktableentrynegative + S (dst_negative_sum_one_resultmasktable) = S ((S (dst_index_sum_one_resultmasktable)) * dst_negative_scale_sum_one_resultmasktable)) /\ exists ff_q_pvs_sum_one_resultmasktableentrynegative. dst_negative_code_sum_one_resultmasktable = ff_q_pvs_sum_one_resultmasktableentrynegative * S ((S (dst_index_sum_one_resultmasktable)) * dst_negative_scale_sum_one_resultmasktable) + (dst_negative_sum_one_resultmasktable))) /\ (exists ge_balance_positive_sum_one_resultmasktableentryvalue ge_balance_negative_sum_one_resultmasktableentryvalue. (((((dst_value_sum_one_resultmasktable) = 2 * (ge_balance_positive_sum_one_resultmasktableentryvalue) /\ (ge_balance_negative_sum_one_resultmasktableentryvalue) = 0) \/ exists ge_signed_half_sum_one_resultmasktableentryvaluedecode. (((dst_value_sum_one_resultmasktable) = 2 * ge_signed_half_sum_one_resultmasktableentryvaluedecode + 1 /\ (ge_balance_positive_sum_one_resultmasktableentryvalue) = 0) /\ (ge_balance_negative_sum_one_resultmasktableentryvalue) = S ge_signed_half_sum_one_resultmasktableentryvaluedecode))) /\ ((dst_positive_sum_one_resultmasktable) + ge_balance_negative_sum_one_resultmasktableentryvalue = (dst_negative_sum_one_resultmasktable) + ge_balance_positive_sum_one_resultmasktableentryvalue))))))))) /\ (forall dm_index_sum_one_resultmask dm_value_sum_one_resultmask. (exists pvs_le_gap_sum_one_resultmaskdomain. pvs_le_gap_sum_one_resultmaskdomain + (dm_index_sum_one_resultmask) = (1)) -> (exists dst_positive_code_sum_one_resultmasklookup dst_positive_scale_sum_one_resultmasklookup dst_negative_code_sum_one_resultmasklookup dst_negative_scale_sum_one_resultmasklookup dst_positive_sum_one_resultmasklookup dst_negative_sum_one_resultmasklookup. (((dm_mask_table_sum_one_result) = (((((dst_positive_code_sum_one_resultmasklookup) + (dst_positive_scale_sum_one_resultmasklookup)) * S ((dst_positive_code_sum_one_resultmasklookup) + (dst_positive_scale_sum_one_resultmasklookup)) + ((dst_positive_scale_sum_one_resultmasklookup) + (dst_positive_scale_sum_one_resultmasklookup))) + (((dst_negative_code_sum_one_resultmasklookup) + (dst_negative_scale_sum_one_resultmasklookup)) * S ((dst_negative_code_sum_one_resultmasklookup) + (dst_negative_scale_sum_one_resultmasklookup)) + ((dst_negative_scale_sum_one_resultmasklookup) + (dst_negative_scale_sum_one_resultmasklookup)))) * S ((((dst_positive_code_sum_one_resultmasklookup) + (dst_positive_scale_sum_one_resultmasklookup)) * S ((dst_positive_code_sum_one_resultmasklookup) + (dst_positive_scale_sum_one_resultmasklookup)) + ((dst_positive_scale_sum_one_resultmasklookup) + (dst_positive_scale_sum_one_resultmasklookup))) + (((dst_negative_code_sum_one_resultmasklookup) + (dst_negative_scale_sum_one_resultmasklookup)) * S ((dst_negative_code_sum_one_resultmasklookup) + (dst_negative_scale_sum_one_resultmasklookup)) + ((dst_negative_scale_sum_one_resultmasklookup) + (dst_negative_scale_sum_one_resultmasklookup)))) + ((((dst_negative_code_sum_one_resultmasklookup) + (dst_negative_scale_sum_one_resultmasklookup)) * S ((dst_negative_code_sum_one_resultmasklookup) + (dst_negative_scale_sum_one_resultmasklookup)) + ((dst_negative_scale_sum_one_resultmasklookup) + (dst_negative_scale_sum_one_resultmasklookup))) + (((dst_negative_code_sum_one_resultmasklookup) + (dst_negative_scale_sum_one_resultmasklookup)) * S ((dst_negative_code_sum_one_resultmasklookup) + (dst_negative_scale_sum_one_resultmasklookup)) + ((dst_negative_scale_sum_one_resultmasklookup) + (dst_negative_scale_sum_one_resultmasklookup)))))) /\ (((((exists ff_h_pvs_sum_one_resultmasklookuppositive. ff_h_pvs_sum_one_resultmasklookuppositive + S (dst_positive_sum_one_resultmasklookup) = S ((S (dm_index_sum_one_resultmask)) * dst_positive_scale_sum_one_resultmasklookup)) /\ exists ff_q_pvs_sum_one_resultmasklookuppositive. dst_positive_code_sum_one_resultmasklookup = ff_q_pvs_sum_one_resultmasklookuppositive * S ((S (dm_index_sum_one_resultmask)) * dst_positive_scale_sum_one_resultmasklookup) + (dst_positive_sum_one_resultmasklookup))) /\ (((((exists ff_h_pvs_sum_one_resultmasklookupnegative. ff_h_pvs_sum_one_resultmasklookupnegative + S (dst_negative_sum_one_resultmasklookup) = S ((S (dm_index_sum_one_resultmask)) * dst_negative_scale_sum_one_resultmasklookup)) /\ exists ff_q_pvs_sum_one_resultmasklookupnegative. dst_negative_code_sum_one_resultmasklookup = ff_q_pvs_sum_one_resultmasklookupnegative * S ((S (dm_index_sum_one_resultmask)) * dst_negative_scale_sum_one_resultmasklookup) + (dst_negative_sum_one_resultmasklookup))) /\ (exists ge_balance_positive_sum_one_resultmasklookupvalue ge_balance_negative_sum_one_resultmasklookupvalue. (((((dm_value_sum_one_resultmask) = 2 * (ge_balance_positive_sum_one_resultmasklookupvalue) /\ (ge_balance_negative_sum_one_resultmasklookupvalue) = 0) \/ exists ge_signed_half_sum_one_resultmasklookupvaluedecode. (((dm_value_sum_one_resultmask) = 2 * ge_signed_half_sum_one_resultmasklookupvaluedecode + 1 /\ (ge_balance_positive_sum_one_resultmasklookupvalue) = 0) /\ (ge_balance_negative_sum_one_resultmasklookupvalue) = S ge_signed_half_sum_one_resultmasklookupvaluedecode))) /\ ((dst_positive_sum_one_resultmasklookup) + ge_balance_negative_sum_one_resultmasklookupvalue = (dst_negative_sum_one_resultmasklookup) + ge_balance_positive_sum_one_resultmasklookupvalue))))))))) -> ((((~((dm_index_sum_one_resultmask)=0)) /\ (exists dm_quotient_sum_one_resultmaskentry. (((1)=(dm_index_sum_one_resultmask)*dm_quotient_sum_one_resultmaskentry) /\ (exists dst_positive_code_sum_one_resultmaskentryinput dst_positive_scale_sum_one_resultmaskentryinput dst_negative_code_sum_one_resultmaskentryinput dst_negative_scale_sum_one_resultmaskentryinput dst_positive_sum_one_resultmaskentryinput dst_negative_sum_one_resultmaskentryinput. (((F) = (((((dst_positive_code_sum_one_resultmaskentryinput) + (dst_positive_scale_sum_one_resultmaskentryinput)) * S ((dst_positive_code_sum_one_resultmaskentryinput) + (dst_positive_scale_sum_one_resultmaskentryinput)) + ((dst_positive_scale_sum_one_resultmaskentryinput) + (dst_positive_scale_sum_one_resultmaskentryinput))) + (((dst_negative_code_sum_one_resultmaskentryinput) + (dst_negative_scale_sum_one_resultmaskentryinput)) * S ((dst_negative_code_sum_one_resultmaskentryinput) + (dst_negative_scale_sum_one_resultmaskentryinput)) + ((dst_negative_scale_sum_one_resultmaskentryinput) + (dst_negative_scale_sum_one_resultmaskentryinput)))) * S ((((dst_positive_code_sum_one_resultmaskentryinput) + (dst_positive_scale_sum_one_resultmaskentryinput)) * S ((dst_positive_code_sum_one_resultmaskentryinput) + (dst_positive_scale_sum_one_resultmaskentryinput)) + ((dst_positive_scale_sum_one_resultmaskentryinput) + (dst_positive_scale_sum_one_resultmaskentryinput))) + (((dst_negative_code_sum_one_resultmaskentryinput) + (dst_negative_scale_sum_one_resultmaskentryinput)) * S ((dst_negative_code_sum_one_resultmaskentryinput) + (dst_negative_scale_sum_one_resultmaskentryinput)) + ((dst_negative_scale_sum_one_resultmaskentryinput) + (dst_negative_scale_sum_one_resultmaskentryinput)))) + ((((dst_negative_code_sum_one_resultmaskentryinput) + (dst_negative_scale_sum_one_resultmaskentryinput)) * S ((dst_negative_code_sum_one_resultmaskentryinput) + (dst_negative_scale_sum_one_resultmaskentryinput)) + ((dst_negative_scale_sum_one_resultmaskentryinput) + (dst_negative_scale_sum_one_resultmaskentryinput))) + (((dst_negative_code_sum_one_resultmaskentryinput) + (dst_negative_scale_sum_one_resultmaskentryinput)) * S ((dst_negative_code_sum_one_resultmaskentryinput) + (dst_negative_scale_sum_one_resultmaskentryinput)) + ((dst_negative_scale_sum_one_resultmaskentryinput) + (dst_negative_scale_sum_one_resultmaskentryinput)))))) /\ (((((exists ff_h_pvs_sum_one_resultmaskentryinputpositive. ff_h_pvs_sum_one_resultmaskentryinputpositive + S (dst_positive_sum_one_resultmaskentryinput) = S ((S (dm_index_sum_one_resultmask)) * dst_positive_scale_sum_one_resultmaskentryinput)) /\ exists ff_q_pvs_sum_one_resultmaskentryinputpositive. dst_positive_code_sum_one_resultmaskentryinput = ff_q_pvs_sum_one_resultmaskentryinputpositive * S ((S (dm_index_sum_one_resultmask)) * dst_positive_scale_sum_one_resultmaskentryinput) + (dst_positive_sum_one_resultmaskentryinput))) /\ (((((exists ff_h_pvs_sum_one_resultmaskentryinputnegative. ff_h_pvs_sum_one_resultmaskentryinputnegative + S (dst_negative_sum_one_resultmaskentryinput) = S ((S (dm_index_sum_one_resultmask)) * dst_negative_scale_sum_one_resultmaskentryinput)) /\ exists ff_q_pvs_sum_one_resultmaskentryinputnegative. dst_negative_code_sum_one_resultmaskentryinput = ff_q_pvs_sum_one_resultmaskentryinputnegative * S ((S (dm_index_sum_one_resultmask)) * dst_negative_scale_sum_one_resultmaskentryinput) + (dst_negative_sum_one_resultmaskentryinput))) /\ (exists ge_balance_positive_sum_one_resultmaskentryinputvalue ge_balance_negative_sum_one_resultmaskentryinputvalue. (((((dm_value_sum_one_resultmask) = 2 * (ge_balance_positive_sum_one_resultmaskentryinputvalue) /\ (ge_balance_negative_sum_one_resultmaskentryinputvalue) = 0) \/ exists ge_signed_half_sum_one_resultmaskentryinputvaluedecode. (((dm_value_sum_one_resultmask) = 2 * ge_signed_half_sum_one_resultmaskentryinputvaluedecode + 1 /\ (ge_balance_positive_sum_one_resultmaskentryinputvalue) = 0) /\ (ge_balance_negative_sum_one_resultmaskentryinputvalue) = S ge_signed_half_sum_one_resultmaskentryinputvaluedecode))) /\ ((dst_positive_sum_one_resultmaskentryinput) + ge_balance_negative_sum_one_resultmaskentryinputvalue = (dst_negative_sum_one_resultmaskentryinput) + ge_balance_positive_sum_one_resultmaskentryinputvalue))))))))))))) \/ ((((dm_index_sum_one_resultmask)=0 \/ ~(exists pvs_factor_sum_one_resultmaskentrynondivisor. (1) = (dm_index_sum_one_resultmask) * pvs_factor_sum_one_resultmaskentrynondivisor)) /\ ((dm_value_sum_one_resultmask)=0))))))) /\ (exists dst_positive_code_sum_one_resultfold dst_positive_scale_sum_one_resultfold dst_negative_code_sum_one_resultfold dst_negative_scale_sum_one_resultfold dst_positive_sum_sum_one_resultfold dst_negative_sum_sum_one_resultfold. (((dm_mask_table_sum_one_result) = (((((dst_positive_code_sum_one_resultfold) + (dst_positive_scale_sum_one_resultfold)) * S ((dst_positive_code_sum_one_resultfold) + (dst_positive_scale_sum_one_resultfold)) + ((dst_positive_scale_sum_one_resultfold) + (dst_positive_scale_sum_one_resultfold))) + (((dst_negative_code_sum_one_resultfold) + (dst_negative_scale_sum_one_resultfold)) * S ((dst_negative_code_sum_one_resultfold) + (dst_negative_scale_sum_one_resultfold)) + ((dst_negative_scale_sum_one_resultfold) + (dst_negative_scale_sum_one_resultfold)))) * S ((((dst_positive_code_sum_one_resultfold) + (dst_positive_scale_sum_one_resultfold)) * S ((dst_positive_code_sum_one_resultfold) + (dst_positive_scale_sum_one_resultfold)) + ((dst_positive_scale_sum_one_resultfold) + (dst_positive_scale_sum_one_resultfold))) + (((dst_negative_code_sum_one_resultfold) + (dst_negative_scale_sum_one_resultfold)) * S ((dst_negative_code_sum_one_resultfold) + (dst_negative_scale_sum_one_resultfold)) + ((dst_negative_scale_sum_one_resultfold) + (dst_negative_scale_sum_one_resultfold)))) + ((((dst_negative_code_sum_one_resultfold) + (dst_negative_scale_sum_one_resultfold)) * S ((dst_negative_code_sum_one_resultfold) + (dst_negative_scale_sum_one_resultfold)) + ((dst_negative_scale_sum_one_resultfold) + (dst_negative_scale_sum_one_resultfold))) + (((dst_negative_code_sum_one_resultfold) + (dst_negative_scale_sum_one_resultfold)) * S ((dst_negative_code_sum_one_resultfold) + (dst_negative_scale_sum_one_resultfold)) + ((dst_negative_scale_sum_one_resultfold) + (dst_negative_scale_sum_one_resultfold)))))) /\ (((exists fs_u_dst_sum_one_resultfoldpositive fs_v_dst_sum_one_resultfoldpositive. ((((exists fs_h_dst_sum_one_resultfoldpositive_body_start. fs_h_dst_sum_one_resultfoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_sum_one_resultfoldpositive)) /\ exists fs_q_dst_sum_one_resultfoldpositive_body_start. fs_u_dst_sum_one_resultfoldpositive = fs_q_dst_sum_one_resultfoldpositive_body_start * S ((S (0)) * fs_v_dst_sum_one_resultfoldpositive) + (0))) /\ ((((exists fs_h_dst_sum_one_resultfoldpositive_body_terminal. fs_h_dst_sum_one_resultfoldpositive_body_terminal + S (dst_positive_sum_sum_one_resultfold) = S ((S (S (1))) * fs_v_dst_sum_one_resultfoldpositive)) /\ exists fs_q_dst_sum_one_resultfoldpositive_body_terminal. fs_u_dst_sum_one_resultfoldpositive = fs_q_dst_sum_one_resultfoldpositive_body_terminal * S ((S (S (1))) * fs_v_dst_sum_one_resultfoldpositive) + (dst_positive_sum_sum_one_resultfold))) /\ forall fs_i_dst_sum_one_resultfoldpositive_body_steps. (exists fs_lt_dst_sum_one_resultfoldpositive_body_steps_bound. fs_lt_dst_sum_one_resultfoldpositive_body_steps_bound + S fs_i_dst_sum_one_resultfoldpositive_body_steps = S (1)) -> exists fs_a_dst_sum_one_resultfoldpositive_body_steps fs_r_dst_sum_one_resultfoldpositive_body_steps fs_s_dst_sum_one_resultfoldpositive_body_steps. ((((exists fs_h_dst_sum_one_resultfoldpositive_body_steps_summand. fs_h_dst_sum_one_resultfoldpositive_body_steps_summand + S (fs_a_dst_sum_one_resultfoldpositive_body_steps) = S ((S (fs_i_dst_sum_one_resultfoldpositive_body_steps)) * dst_positive_scale_sum_one_resultfold)) /\ exists fs_q_dst_sum_one_resultfoldpositive_body_steps_summand. dst_positive_code_sum_one_resultfold = fs_q_dst_sum_one_resultfoldpositive_body_steps_summand * S ((S (fs_i_dst_sum_one_resultfoldpositive_body_steps)) * dst_positive_scale_sum_one_resultfold) + (fs_a_dst_sum_one_resultfoldpositive_body_steps))) /\ ((((exists fs_h_dst_sum_one_resultfoldpositive_body_steps_partial. fs_h_dst_sum_one_resultfoldpositive_body_steps_partial + S (fs_r_dst_sum_one_resultfoldpositive_body_steps) = S ((S (fs_i_dst_sum_one_resultfoldpositive_body_steps)) * fs_v_dst_sum_one_resultfoldpositive)) /\ exists fs_q_dst_sum_one_resultfoldpositive_body_steps_partial. fs_u_dst_sum_one_resultfoldpositive = fs_q_dst_sum_one_resultfoldpositive_body_steps_partial * S ((S (fs_i_dst_sum_one_resultfoldpositive_body_steps)) * fs_v_dst_sum_one_resultfoldpositive) + (fs_r_dst_sum_one_resultfoldpositive_body_steps))) /\ ((((exists fs_h_dst_sum_one_resultfoldpositive_body_steps_successor. fs_h_dst_sum_one_resultfoldpositive_body_steps_successor + S (fs_s_dst_sum_one_resultfoldpositive_body_steps) = S ((S (S fs_i_dst_sum_one_resultfoldpositive_body_steps)) * fs_v_dst_sum_one_resultfoldpositive)) /\ exists fs_q_dst_sum_one_resultfoldpositive_body_steps_successor. fs_u_dst_sum_one_resultfoldpositive = fs_q_dst_sum_one_resultfoldpositive_body_steps_successor * S ((S (S fs_i_dst_sum_one_resultfoldpositive_body_steps)) * fs_v_dst_sum_one_resultfoldpositive) + (fs_s_dst_sum_one_resultfoldpositive_body_steps))) /\ fs_s_dst_sum_one_resultfoldpositive_body_steps = fs_r_dst_sum_one_resultfoldpositive_body_steps + fs_a_dst_sum_one_resultfoldpositive_body_steps)))))) /\ (((exists fs_u_dst_sum_one_resultfoldnegative fs_v_dst_sum_one_resultfoldnegative. ((((exists fs_h_dst_sum_one_resultfoldnegative_body_start. fs_h_dst_sum_one_resultfoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_sum_one_resultfoldnegative)) /\ exists fs_q_dst_sum_one_resultfoldnegative_body_start. fs_u_dst_sum_one_resultfoldnegative = fs_q_dst_sum_one_resultfoldnegative_body_start * S ((S (0)) * fs_v_dst_sum_one_resultfoldnegative) + (0))) /\ ((((exists fs_h_dst_sum_one_resultfoldnegative_body_terminal. fs_h_dst_sum_one_resultfoldnegative_body_terminal + S (dst_negative_sum_sum_one_resultfold) = S ((S (S (1))) * fs_v_dst_sum_one_resultfoldnegative)) /\ exists fs_q_dst_sum_one_resultfoldnegative_body_terminal. fs_u_dst_sum_one_resultfoldnegative = fs_q_dst_sum_one_resultfoldnegative_body_terminal * S ((S (S (1))) * fs_v_dst_sum_one_resultfoldnegative) + (dst_negative_sum_sum_one_resultfold))) /\ forall fs_i_dst_sum_one_resultfoldnegative_body_steps. (exists fs_lt_dst_sum_one_resultfoldnegative_body_steps_bound. fs_lt_dst_sum_one_resultfoldnegative_body_steps_bound + S fs_i_dst_sum_one_resultfoldnegative_body_steps = S (1)) -> exists fs_a_dst_sum_one_resultfoldnegative_body_steps fs_r_dst_sum_one_resultfoldnegative_body_steps fs_s_dst_sum_one_resultfoldnegative_body_steps. ((((exists fs_h_dst_sum_one_resultfoldnegative_body_steps_summand. fs_h_dst_sum_one_resultfoldnegative_body_steps_summand + S (fs_a_dst_sum_one_resultfoldnegative_body_steps) = S ((S (fs_i_dst_sum_one_resultfoldnegative_body_steps)) * dst_negative_scale_sum_one_resultfold)) /\ exists fs_q_dst_sum_one_resultfoldnegative_body_steps_summand. dst_negative_code_sum_one_resultfold = fs_q_dst_sum_one_resultfoldnegative_body_steps_summand * S ((S (fs_i_dst_sum_one_resultfoldnegative_body_steps)) * dst_negative_scale_sum_one_resultfold) + (fs_a_dst_sum_one_resultfoldnegative_body_steps))) /\ ((((exists fs_h_dst_sum_one_resultfoldnegative_body_steps_partial. fs_h_dst_sum_one_resultfoldnegative_body_steps_partial + S (fs_r_dst_sum_one_resultfoldnegative_body_steps) = S ((S (fs_i_dst_sum_one_resultfoldnegative_body_steps)) * fs_v_dst_sum_one_resultfoldnegative)) /\ exists fs_q_dst_sum_one_resultfoldnegative_body_steps_partial. fs_u_dst_sum_one_resultfoldnegative = fs_q_dst_sum_one_resultfoldnegative_body_steps_partial * S ((S (fs_i_dst_sum_one_resultfoldnegative_body_steps)) * fs_v_dst_sum_one_resultfoldnegative) + (fs_r_dst_sum_one_resultfoldnegative_body_steps))) /\ ((((exists fs_h_dst_sum_one_resultfoldnegative_body_steps_successor. fs_h_dst_sum_one_resultfoldnegative_body_steps_successor + S (fs_s_dst_sum_one_resultfoldnegative_body_steps) = S ((S (S fs_i_dst_sum_one_resultfoldnegative_body_steps)) * fs_v_dst_sum_one_resultfoldnegative)) /\ exists fs_q_dst_sum_one_resultfoldnegative_body_steps_successor. fs_u_dst_sum_one_resultfoldnegative = fs_q_dst_sum_one_resultfoldnegative_body_steps_successor * S ((S (S fs_i_dst_sum_one_resultfoldnegative_body_steps)) * fs_v_dst_sum_one_resultfoldnegative) + (fs_s_dst_sum_one_resultfoldnegative_body_steps))) /\ fs_s_dst_sum_one_resultfoldnegative_body_steps = fs_r_dst_sum_one_resultfoldnegative_body_steps + fs_a_dst_sum_one_resultfoldnegative_body_steps)))))) /\ (exists ge_balance_positive_sum_one_resultfoldresult ge_balance_negative_sum_one_resultfoldresult. (((((a) = 2 * (ge_balance_positive_sum_one_resultfoldresult) /\ (ge_balance_negative_sum_one_resultfoldresult) = 0) \/ exists ge_signed_half_sum_one_resultfoldresultdecode. (((a) = 2 * ge_signed_half_sum_one_resultfoldresultdecode + 1 /\ (ge_balance_positive_sum_one_resultfoldresult) = 0) /\ (ge_balance_negative_sum_one_resultfoldresult) = S ge_signed_half_sum_one_resultfoldresultdecode))) /\ ((dst_positive_sum_sum_one_resultfold) + ge_balance_negative_sum_one_resultfoldresult = (dst_negative_sum_sum_one_resultfold) + ge_balance_positive_sum_one_resultfoldresult)))))))))))))