dirichlet_delta_right_sum

forall N F E n a. (exists dst_positive_code_unit_sum_input dst_positive_scale_unit_sum_input dst_negative_code_unit_sum_input dst_negative_scale_unit_sum_input. (((F) = (((((dst_positive_code_unit_sum_input) + (dst_positive_scale_unit_sum_input)) * S ((dst_positive_code_unit_sum_input) + (dst_positive_scale_unit_sum_input)) + ((dst_positive_scale_unit_sum_input) + (dst_positive_scale_unit_sum_input))) + (((dst_negative_code_unit_sum_input) + (dst_negative_scale_unit_sum_input)) * S ((dst_negative_code_unit_sum_input) + (dst_negative_scale_unit_sum_input)) + ((dst_negative_scale_unit_sum_input) + (dst_negative_scale_unit_sum_input)))) * S ((((dst_positive_code_unit_sum_input) + (dst_positive_scale_unit_sum_input)) * S ((dst_positive_code_unit_sum_input) + (dst_positive_scale_unit_sum_input)) + ((dst_positive_scale_unit_sum_input) + (dst_positive_scale_unit_sum_input))) + (((dst_negative_code_unit_sum_input) + (dst_negative_scale_unit_sum_input)) * S ((dst_negative_code_unit_sum_input) + (dst_negative_scale_unit_sum_input)) + ((dst_negative_scale_unit_sum_input) + (dst_negative_scale_unit_sum_input)))) + ((((dst_negative_code_unit_sum_input) + (dst_negative_scale_unit_sum_input)) * S ((dst_negative_code_unit_sum_input) + (dst_negative_scale_unit_sum_input)) + ((dst_negative_scale_unit_sum_input) + (dst_negative_scale_unit_sum_input))) + (((dst_negative_code_unit_sum_input) + (dst_negative_scale_unit_sum_input)) * S ((dst_negative_code_unit_sum_input) + (dst_negative_scale_unit_sum_input)) + ((dst_negative_scale_unit_sum_input) + (dst_negative_scale_unit_sum_input)))))) /\ (forall dst_index_unit_sum_input. (exists pvs_le_gap_unit_sum_inputdomain. pvs_le_gap_unit_sum_inputdomain + (dst_index_unit_sum_input) = (N)) -> exists dst_positive_unit_sum_input dst_negative_unit_sum_input dst_value_unit_sum_input. ((((exists ff_h_pvs_unit_sum_inputentrypositive. ff_h_pvs_unit_sum_inputentrypositive + S (dst_positive_unit_sum_input) = S ((S (dst_index_unit_sum_input)) * dst_positive_scale_unit_sum_input)) /\ exists ff_q_pvs_unit_sum_inputentrypositive. dst_positive_code_unit_sum_input = ff_q_pvs_unit_sum_inputentrypositive * S ((S (dst_index_unit_sum_input)) * dst_positive_scale_unit_sum_input) + (dst_positive_unit_sum_input))) /\ (((((exists ff_h_pvs_unit_sum_inputentrynegative. ff_h_pvs_unit_sum_inputentrynegative + S (dst_negative_unit_sum_input) = S ((S (dst_index_unit_sum_input)) * dst_negative_scale_unit_sum_input)) /\ exists ff_q_pvs_unit_sum_inputentrynegative. dst_negative_code_unit_sum_input = ff_q_pvs_unit_sum_inputentrynegative * S ((S (dst_index_unit_sum_input)) * dst_negative_scale_unit_sum_input) + (dst_negative_unit_sum_input))) /\ (exists ge_balance_positive_unit_sum_inputentryvalue ge_balance_negative_unit_sum_inputentryvalue. (((((dst_value_unit_sum_input) = 2 * (ge_balance_positive_unit_sum_inputentryvalue) /\ (ge_balance_negative_unit_sum_inputentryvalue) = 0) \/ exists ge_signed_half_unit_sum_inputentryvaluedecode. (((dst_value_unit_sum_input) = 2 * ge_signed_half_unit_sum_inputentryvaluedecode + 1 /\ (ge_balance_positive_unit_sum_inputentryvalue) = 0) /\ (ge_balance_negative_unit_sum_inputentryvalue) = S ge_signed_half_unit_sum_inputentryvaluedecode))) /\ ((dst_positive_unit_sum_input) + ge_balance_negative_unit_sum_inputentryvalue = (dst_negative_unit_sum_input) + ge_balance_positive_unit_sum_inputentryvalue))))))))) -> (((exists dst_positive_code_unit_sum_deltatable dst_positive_scale_unit_sum_deltatable dst_negative_code_unit_sum_deltatable dst_negative_scale_unit_sum_deltatable. (((E) = (((((dst_positive_code_unit_sum_deltatable) + (dst_positive_scale_unit_sum_deltatable)) * S ((dst_positive_code_unit_sum_deltatable) + (dst_positive_scale_unit_sum_deltatable)) + ((dst_positive_scale_unit_sum_deltatable) + (dst_positive_scale_unit_sum_deltatable))) + (((dst_negative_code_unit_sum_deltatable) + (dst_negative_scale_unit_sum_deltatable)) * S ((dst_negative_code_unit_sum_deltatable) + (dst_negative_scale_unit_sum_deltatable)) + ((dst_negative_scale_unit_sum_deltatable) + (dst_negative_scale_unit_sum_deltatable)))) * S ((((dst_positive_code_unit_sum_deltatable) + (dst_positive_scale_unit_sum_deltatable)) * S ((dst_positive_code_unit_sum_deltatable) + (dst_positive_scale_unit_sum_deltatable)) + ((dst_positive_scale_unit_sum_deltatable) + (dst_positive_scale_unit_sum_deltatable))) + (((dst_negative_code_unit_sum_deltatable) + (dst_negative_scale_unit_sum_deltatable)) * S ((dst_negative_code_unit_sum_deltatable) + (dst_negative_scale_unit_sum_deltatable)) + ((dst_negative_scale_unit_sum_deltatable) + (dst_negative_scale_unit_sum_deltatable)))) + ((((dst_negative_code_unit_sum_deltatable) + (dst_negative_scale_unit_sum_deltatable)) * S ((dst_negative_code_unit_sum_deltatable) + (dst_negative_scale_unit_sum_deltatable)) + ((dst_negative_scale_unit_sum_deltatable) + (dst_negative_scale_unit_sum_deltatable))) + (((dst_negative_code_unit_sum_deltatable) + (dst_negative_scale_unit_sum_deltatable)) * S ((dst_negative_code_unit_sum_deltatable) + (dst_negative_scale_unit_sum_deltatable)) + ((dst_negative_scale_unit_sum_deltatable) + (dst_negative_scale_unit_sum_deltatable)))))) /\ (forall dst_index_unit_sum_deltatable. (exists pvs_le_gap_unit_sum_deltatabledomain. pvs_le_gap_unit_sum_deltatabledomain + (dst_index_unit_sum_deltatable) = (N)) -> exists dst_positive_unit_sum_deltatable dst_negative_unit_sum_deltatable dst_value_unit_sum_deltatable. ((((exists ff_h_pvs_unit_sum_deltatableentrypositive. ff_h_pvs_unit_sum_deltatableentrypositive + S (dst_positive_unit_sum_deltatable) = S ((S (dst_index_unit_sum_deltatable)) * dst_positive_scale_unit_sum_deltatable)) /\ exists ff_q_pvs_unit_sum_deltatableentrypositive. dst_positive_code_unit_sum_deltatable = ff_q_pvs_unit_sum_deltatableentrypositive * S ((S (dst_index_unit_sum_deltatable)) * dst_positive_scale_unit_sum_deltatable) + (dst_positive_unit_sum_deltatable))) /\ (((((exists ff_h_pvs_unit_sum_deltatableentrynegative. ff_h_pvs_unit_sum_deltatableentrynegative + S (dst_negative_unit_sum_deltatable) = S ((S (dst_index_unit_sum_deltatable)) * dst_negative_scale_unit_sum_deltatable)) /\ exists ff_q_pvs_unit_sum_deltatableentrynegative. dst_negative_code_unit_sum_deltatable = ff_q_pvs_unit_sum_deltatableentrynegative * S ((S (dst_index_unit_sum_deltatable)) * dst_negative_scale_unit_sum_deltatable) + (dst_negative_unit_sum_deltatable))) /\ (exists ge_balance_positive_unit_sum_deltatableentryvalue ge_balance_negative_unit_sum_deltatableentryvalue. (((((dst_value_unit_sum_deltatable) = 2 * (ge_balance_positive_unit_sum_deltatableentryvalue) /\ (ge_balance_negative_unit_sum_deltatableentryvalue) = 0) \/ exists ge_signed_half_unit_sum_deltatableentryvaluedecode. (((dst_value_unit_sum_deltatable) = 2 * ge_signed_half_unit_sum_deltatableentryvaluedecode + 1 /\ (ge_balance_positive_unit_sum_deltatableentryvalue) = 0) /\ (ge_balance_negative_unit_sum_deltatableentryvalue) = S ge_signed_half_unit_sum_deltatableentryvaluedecode))) /\ ((dst_positive_unit_sum_deltatable) + ge_balance_negative_unit_sum_deltatableentryvalue = (dst_negative_unit_sum_deltatable) + ge_balance_positive_unit_sum_deltatableentryvalue))))))))) /\ (forall du_index_unit_sum_delta du_value_unit_sum_delta. ~(du_index_unit_sum_delta=0) -> (exists pvs_le_gap_unit_sum_deltabound. pvs_le_gap_unit_sum_deltabound + (du_index_unit_sum_delta) = (N)) -> (exists dst_positive_code_unit_sum_deltaentry dst_positive_scale_unit_sum_deltaentry dst_negative_code_unit_sum_deltaentry dst_negative_scale_unit_sum_deltaentry dst_positive_unit_sum_deltaentry dst_negative_unit_sum_deltaentry. (((E) = (((((dst_positive_code_unit_sum_deltaentry) + (dst_positive_scale_unit_sum_deltaentry)) * S ((dst_positive_code_unit_sum_deltaentry) + (dst_positive_scale_unit_sum_deltaentry)) + ((dst_positive_scale_unit_sum_deltaentry) + (dst_positive_scale_unit_sum_deltaentry))) + (((dst_negative_code_unit_sum_deltaentry) + (dst_negative_scale_unit_sum_deltaentry)) * S ((dst_negative_code_unit_sum_deltaentry) + (dst_negative_scale_unit_sum_deltaentry)) + ((dst_negative_scale_unit_sum_deltaentry) + (dst_negative_scale_unit_sum_deltaentry)))) * S ((((dst_positive_code_unit_sum_deltaentry) + (dst_positive_scale_unit_sum_deltaentry)) * S ((dst_positive_code_unit_sum_deltaentry) + (dst_positive_scale_unit_sum_deltaentry)) + ((dst_positive_scale_unit_sum_deltaentry) + (dst_positive_scale_unit_sum_deltaentry))) + (((dst_negative_code_unit_sum_deltaentry) + (dst_negative_scale_unit_sum_deltaentry)) * S ((dst_negative_code_unit_sum_deltaentry) + (dst_negative_scale_unit_sum_deltaentry)) + ((dst_negative_scale_unit_sum_deltaentry) + (dst_negative_scale_unit_sum_deltaentry)))) + ((((dst_negative_code_unit_sum_deltaentry) + (dst_negative_scale_unit_sum_deltaentry)) * S ((dst_negative_code_unit_sum_deltaentry) + (dst_negative_scale_unit_sum_deltaentry)) + ((dst_negative_scale_unit_sum_deltaentry) + (dst_negative_scale_unit_sum_deltaentry))) + (((dst_negative_code_unit_sum_deltaentry) + (dst_negative_scale_unit_sum_deltaentry)) * S ((dst_negative_code_unit_sum_deltaentry) + (dst_negative_scale_unit_sum_deltaentry)) + ((dst_negative_scale_unit_sum_deltaentry) + (dst_negative_scale_unit_sum_deltaentry)))))) /\ (((((exists ff_h_pvs_unit_sum_deltaentrypositive. ff_h_pvs_unit_sum_deltaentrypositive + S (dst_positive_unit_sum_deltaentry) = S ((S (du_index_unit_sum_delta)) * dst_positive_scale_unit_sum_deltaentry)) /\ exists ff_q_pvs_unit_sum_deltaentrypositive. dst_positive_code_unit_sum_deltaentry = ff_q_pvs_unit_sum_deltaentrypositive * S ((S (du_index_unit_sum_delta)) * dst_positive_scale_unit_sum_deltaentry) + (dst_positive_unit_sum_deltaentry))) /\ (((((exists ff_h_pvs_unit_sum_deltaentrynegative. ff_h_pvs_unit_sum_deltaentrynegative + S (dst_negative_unit_sum_deltaentry) = S ((S (du_index_unit_sum_delta)) * dst_negative_scale_unit_sum_deltaentry)) /\ exists ff_q_pvs_unit_sum_deltaentrynegative. dst_negative_code_unit_sum_deltaentry = ff_q_pvs_unit_sum_deltaentrynegative * S ((S (du_index_unit_sum_delta)) * dst_negative_scale_unit_sum_deltaentry) + (dst_negative_unit_sum_deltaentry))) /\ (exists ge_balance_positive_unit_sum_deltaentryvalue ge_balance_negative_unit_sum_deltaentryvalue. (((((du_value_unit_sum_delta) = 2 * (ge_balance_positive_unit_sum_deltaentryvalue) /\ (ge_balance_negative_unit_sum_deltaentryvalue) = 0) \/ exists ge_signed_half_unit_sum_deltaentryvaluedecode. (((du_value_unit_sum_delta) = 2 * ge_signed_half_unit_sum_deltaentryvaluedecode + 1 /\ (ge_balance_positive_unit_sum_deltaentryvalue) = 0) /\ (ge_balance_negative_unit_sum_deltaentryvalue) = S ge_signed_half_unit_sum_deltaentryvaluedecode))) /\ ((dst_positive_unit_sum_deltaentry) + ge_balance_negative_unit_sum_deltaentryvalue = (dst_negative_unit_sum_deltaentry) + ge_balance_positive_unit_sum_deltaentryvalue))))))))) -> ((((du_index_unit_sum_delta)=1 -> (du_value_unit_sum_delta)=2) /\ (~((du_index_unit_sum_delta)=1) -> (du_value_unit_sum_delta)=0)))))) -> ~(n=0) -> (exists pvs_le_gap_unit_sum_bound. pvs_le_gap_unit_sum_bound + (n) = (N)) -> (exists dst_positive_code_unit_sum_source dst_positive_scale_unit_sum_source dst_negative_code_unit_sum_source dst_negative_scale_unit_sum_source dst_positive_unit_sum_source dst_negative_unit_sum_source. (((F) = (((((dst_positive_code_unit_sum_source) + (dst_positive_scale_unit_sum_source)) * S ((dst_positive_code_unit_sum_source) + (dst_positive_scale_unit_sum_source)) + ((dst_positive_scale_unit_sum_source) + (dst_positive_scale_unit_sum_source))) + (((dst_negative_code_unit_sum_source) + (dst_negative_scale_unit_sum_source)) * S ((dst_negative_code_unit_sum_source) + (dst_negative_scale_unit_sum_source)) + ((dst_negative_scale_unit_sum_source) + (dst_negative_scale_unit_sum_source)))) * S ((((dst_positive_code_unit_sum_source) + (dst_positive_scale_unit_sum_source)) * S ((dst_positive_code_unit_sum_source) + (dst_positive_scale_unit_sum_source)) + ((dst_positive_scale_unit_sum_source) + (dst_positive_scale_unit_sum_source))) + (((dst_negative_code_unit_sum_source) + (dst_negative_scale_unit_sum_source)) * S ((dst_negative_code_unit_sum_source) + (dst_negative_scale_unit_sum_source)) + ((dst_negative_scale_unit_sum_source) + (dst_negative_scale_unit_sum_source)))) + ((((dst_negative_code_unit_sum_source) + (dst_negative_scale_unit_sum_source)) * S ((dst_negative_code_unit_sum_source) + (dst_negative_scale_unit_sum_source)) + ((dst_negative_scale_unit_sum_source) + (dst_negative_scale_unit_sum_source))) + (((dst_negative_code_unit_sum_source) + (dst_negative_scale_unit_sum_source)) * S ((dst_negative_code_unit_sum_source) + (dst_negative_scale_unit_sum_source)) + ((dst_negative_scale_unit_sum_source) + (dst_negative_scale_unit_sum_source)))))) /\ (((((exists ff_h_pvs_unit_sum_sourcepositive. ff_h_pvs_unit_sum_sourcepositive + S (dst_positive_unit_sum_source) = S ((S (n)) * dst_positive_scale_unit_sum_source)) /\ exists ff_q_pvs_unit_sum_sourcepositive. dst_positive_code_unit_sum_source = ff_q_pvs_unit_sum_sourcepositive * S ((S (n)) * dst_positive_scale_unit_sum_source) + (dst_positive_unit_sum_source))) /\ (((((exists ff_h_pvs_unit_sum_sourcenegative. ff_h_pvs_unit_sum_sourcenegative + S (dst_negative_unit_sum_source) = S ((S (n)) * dst_negative_scale_unit_sum_source)) /\ exists ff_q_pvs_unit_sum_sourcenegative. dst_negative_code_unit_sum_source = ff_q_pvs_unit_sum_sourcenegative * S ((S (n)) * dst_negative_scale_unit_sum_source) + (dst_negative_unit_sum_source))) /\ (exists ge_balance_positive_unit_sum_sourcevalue ge_balance_negative_unit_sum_sourcevalue. (((((a) = 2 * (ge_balance_positive_unit_sum_sourcevalue) /\ (ge_balance_negative_unit_sum_sourcevalue) = 0) \/ exists ge_signed_half_unit_sum_sourcevaluedecode. (((a) = 2 * ge_signed_half_unit_sum_sourcevaluedecode + 1 /\ (ge_balance_positive_unit_sum_sourcevalue) = 0) /\ (ge_balance_negative_unit_sum_sourcevalue) = S ge_signed_half_unit_sum_sourcevaluedecode))) /\ ((dst_positive_unit_sum_source) + ge_balance_negative_unit_sum_sourcevalue = (dst_negative_unit_sum_source) + ge_balance_positive_unit_sum_sourcevalue))))))))) -> (((~((n)=0)) /\ (exists dc_mask_unit_sum_result. ((((exists dst_positive_code_unit_sum_resultmasktable dst_positive_scale_unit_sum_resultmasktable dst_negative_code_unit_sum_resultmasktable dst_negative_scale_unit_sum_resultmasktable. (((dc_mask_unit_sum_result) = (((((dst_positive_code_unit_sum_resultmasktable) + (dst_positive_scale_unit_sum_resultmasktable)) * S ((dst_positive_code_unit_sum_resultmasktable) + (dst_positive_scale_unit_sum_resultmasktable)) + ((dst_positive_scale_unit_sum_resultmasktable) + (dst_positive_scale_unit_sum_resultmasktable))) + (((dst_negative_code_unit_sum_resultmasktable) + (dst_negative_scale_unit_sum_resultmasktable)) * S ((dst_negative_code_unit_sum_resultmasktable) + (dst_negative_scale_unit_sum_resultmasktable)) + ((dst_negative_scale_unit_sum_resultmasktable) + (dst_negative_scale_unit_sum_resultmasktable)))) * S ((((dst_positive_code_unit_sum_resultmasktable) + (dst_positive_scale_unit_sum_resultmasktable)) * S ((dst_positive_code_unit_sum_resultmasktable) + (dst_positive_scale_unit_sum_resultmasktable)) + ((dst_positive_scale_unit_sum_resultmasktable) + (dst_positive_scale_unit_sum_resultmasktable))) + (((dst_negative_code_unit_sum_resultmasktable) + (dst_negative_scale_unit_sum_resultmasktable)) * S ((dst_negative_code_unit_sum_resultmasktable) + (dst_negative_scale_unit_sum_resultmasktable)) + ((dst_negative_scale_unit_sum_resultmasktable) + (dst_negative_scale_unit_sum_resultmasktable)))) + ((((dst_negative_code_unit_sum_resultmasktable) + (dst_negative_scale_unit_sum_resultmasktable)) * S ((dst_negative_code_unit_sum_resultmasktable) + (dst_negative_scale_unit_sum_resultmasktable)) + ((dst_negative_scale_unit_sum_resultmasktable) + (dst_negative_scale_unit_sum_resultmasktable))) + (((dst_negative_code_unit_sum_resultmasktable) + (dst_negative_scale_unit_sum_resultmasktable)) * S ((dst_negative_code_unit_sum_resultmasktable) + (dst_negative_scale_unit_sum_resultmasktable)) + ((dst_negative_scale_unit_sum_resultmasktable) + (dst_negative_scale_unit_sum_resultmasktable)))))) /\ (forall dst_index_unit_sum_resultmasktable. (exists pvs_le_gap_unit_sum_resultmasktabledomain. pvs_le_gap_unit_sum_resultmasktabledomain + (dst_index_unit_sum_resultmasktable) = (n)) -> exists dst_positive_unit_sum_resultmasktable dst_negative_unit_sum_resultmasktable dst_value_unit_sum_resultmasktable. ((((exists ff_h_pvs_unit_sum_resultmasktableentrypositive. ff_h_pvs_unit_sum_resultmasktableentrypositive + S (dst_positive_unit_sum_resultmasktable) = S ((S (dst_index_unit_sum_resultmasktable)) * dst_positive_scale_unit_sum_resultmasktable)) /\ exists ff_q_pvs_unit_sum_resultmasktableentrypositive. dst_positive_code_unit_sum_resultmasktable = ff_q_pvs_unit_sum_resultmasktableentrypositive * S ((S (dst_index_unit_sum_resultmasktable)) * dst_positive_scale_unit_sum_resultmasktable) + (dst_positive_unit_sum_resultmasktable))) /\ (((((exists ff_h_pvs_unit_sum_resultmasktableentrynegative. ff_h_pvs_unit_sum_resultmasktableentrynegative + S (dst_negative_unit_sum_resultmasktable) = S ((S (dst_index_unit_sum_resultmasktable)) * dst_negative_scale_unit_sum_resultmasktable)) /\ exists ff_q_pvs_unit_sum_resultmasktableentrynegative. dst_negative_code_unit_sum_resultmasktable = ff_q_pvs_unit_sum_resultmasktableentrynegative * S ((S (dst_index_unit_sum_resultmasktable)) * dst_negative_scale_unit_sum_resultmasktable) + (dst_negative_unit_sum_resultmasktable))) /\ (exists ge_balance_positive_unit_sum_resultmasktableentryvalue ge_balance_negative_unit_sum_resultmasktableentryvalue. (((((dst_value_unit_sum_resultmasktable) = 2 * (ge_balance_positive_unit_sum_resultmasktableentryvalue) /\ (ge_balance_negative_unit_sum_resultmasktableentryvalue) = 0) \/ exists ge_signed_half_unit_sum_resultmasktableentryvaluedecode. (((dst_value_unit_sum_resultmasktable) = 2 * ge_signed_half_unit_sum_resultmasktableentryvaluedecode + 1 /\ (ge_balance_positive_unit_sum_resultmasktableentryvalue) = 0) /\ (ge_balance_negative_unit_sum_resultmasktableentryvalue) = S ge_signed_half_unit_sum_resultmasktableentryvaluedecode))) /\ ((dst_positive_unit_sum_resultmasktable) + ge_balance_negative_unit_sum_resultmasktableentryvalue = (dst_negative_unit_sum_resultmasktable) + ge_balance_positive_unit_sum_resultmasktableentryvalue))))))))) /\ (forall dc_index_unit_sum_resultmask dc_value_unit_sum_resultmask. (exists pvs_le_gap_unit_sum_resultmaskdomain. pvs_le_gap_unit_sum_resultmaskdomain + (dc_index_unit_sum_resultmask) = (n)) -> (exists dst_positive_code_unit_sum_resultmasklookup dst_positive_scale_unit_sum_resultmasklookup dst_negative_code_unit_sum_resultmasklookup dst_negative_scale_unit_sum_resultmasklookup dst_positive_unit_sum_resultmasklookup dst_negative_unit_sum_resultmasklookup. (((dc_mask_unit_sum_result) = (((((dst_positive_code_unit_sum_resultmasklookup) + (dst_positive_scale_unit_sum_resultmasklookup)) * S ((dst_positive_code_unit_sum_resultmasklookup) + (dst_positive_scale_unit_sum_resultmasklookup)) + ((dst_positive_scale_unit_sum_resultmasklookup) + (dst_positive_scale_unit_sum_resultmasklookup))) + (((dst_negative_code_unit_sum_resultmasklookup) + (dst_negative_scale_unit_sum_resultmasklookup)) * S ((dst_negative_code_unit_sum_resultmasklookup) + (dst_negative_scale_unit_sum_resultmasklookup)) + ((dst_negative_scale_unit_sum_resultmasklookup) + (dst_negative_scale_unit_sum_resultmasklookup)))) * S ((((dst_positive_code_unit_sum_resultmasklookup) + (dst_positive_scale_unit_sum_resultmasklookup)) * S ((dst_positive_code_unit_sum_resultmasklookup) + (dst_positive_scale_unit_sum_resultmasklookup)) + ((dst_positive_scale_unit_sum_resultmasklookup) + (dst_positive_scale_unit_sum_resultmasklookup))) + (((dst_negative_code_unit_sum_resultmasklookup) + (dst_negative_scale_unit_sum_resultmasklookup)) * S ((dst_negative_code_unit_sum_resultmasklookup) + (dst_negative_scale_unit_sum_resultmasklookup)) + ((dst_negative_scale_unit_sum_resultmasklookup) + (dst_negative_scale_unit_sum_resultmasklookup)))) + ((((dst_negative_code_unit_sum_resultmasklookup) + (dst_negative_scale_unit_sum_resultmasklookup)) * S ((dst_negative_code_unit_sum_resultmasklookup) + (dst_negative_scale_unit_sum_resultmasklookup)) + ((dst_negative_scale_unit_sum_resultmasklookup) + (dst_negative_scale_unit_sum_resultmasklookup))) + (((dst_negative_code_unit_sum_resultmasklookup) + (dst_negative_scale_unit_sum_resultmasklookup)) * S ((dst_negative_code_unit_sum_resultmasklookup) + (dst_negative_scale_unit_sum_resultmasklookup)) + ((dst_negative_scale_unit_sum_resultmasklookup) + (dst_negative_scale_unit_sum_resultmasklookup)))))) /\ (((((exists ff_h_pvs_unit_sum_resultmasklookuppositive. ff_h_pvs_unit_sum_resultmasklookuppositive + S (dst_positive_unit_sum_resultmasklookup) = S ((S (dc_index_unit_sum_resultmask)) * dst_positive_scale_unit_sum_resultmasklookup)) /\ exists ff_q_pvs_unit_sum_resultmasklookuppositive. dst_positive_code_unit_sum_resultmasklookup = ff_q_pvs_unit_sum_resultmasklookuppositive * S ((S (dc_index_unit_sum_resultmask)) * dst_positive_scale_unit_sum_resultmasklookup) + (dst_positive_unit_sum_resultmasklookup))) /\ (((((exists ff_h_pvs_unit_sum_resultmasklookupnegative. ff_h_pvs_unit_sum_resultmasklookupnegative + S (dst_negative_unit_sum_resultmasklookup) = S ((S (dc_index_unit_sum_resultmask)) * dst_negative_scale_unit_sum_resultmasklookup)) /\ exists ff_q_pvs_unit_sum_resultmasklookupnegative. dst_negative_code_unit_sum_resultmasklookup = ff_q_pvs_unit_sum_resultmasklookupnegative * S ((S (dc_index_unit_sum_resultmask)) * dst_negative_scale_unit_sum_resultmasklookup) + (dst_negative_unit_sum_resultmasklookup))) /\ (exists ge_balance_positive_unit_sum_resultmasklookupvalue ge_balance_negative_unit_sum_resultmasklookupvalue. (((((dc_value_unit_sum_resultmask) = 2 * (ge_balance_positive_unit_sum_resultmasklookupvalue) /\ (ge_balance_negative_unit_sum_resultmasklookupvalue) = 0) \/ exists ge_signed_half_unit_sum_resultmasklookupvaluedecode. (((dc_value_unit_sum_resultmask) = 2 * ge_signed_half_unit_sum_resultmasklookupvaluedecode + 1 /\ (ge_balance_positive_unit_sum_resultmasklookupvalue) = 0) /\ (ge_balance_negative_unit_sum_resultmasklookupvalue) = S ge_signed_half_unit_sum_resultmasklookupvaluedecode))) /\ ((dst_positive_unit_sum_resultmasklookup) + ge_balance_negative_unit_sum_resultmasklookupvalue = (dst_negative_unit_sum_resultmasklookup) + ge_balance_positive_unit_sum_resultmasklookupvalue))))))))) -> ((((~((dc_index_unit_sum_resultmask)=0)) /\ (exists dc_quotient_unit_sum_resultmaskentry dc_left_unit_sum_resultmaskentry dc_right_unit_sum_resultmaskentry. (((n)=(dc_index_unit_sum_resultmask)*dc_quotient_unit_sum_resultmaskentry) /\ (((exists dst_positive_code_unit_sum_resultmaskentryleft dst_positive_scale_unit_sum_resultmaskentryleft dst_negative_code_unit_sum_resultmaskentryleft dst_negative_scale_unit_sum_resultmaskentryleft dst_positive_unit_sum_resultmaskentryleft dst_negative_unit_sum_resultmaskentryleft. (((F) = (((((dst_positive_code_unit_sum_resultmaskentryleft) + (dst_positive_scale_unit_sum_resultmaskentryleft)) * S ((dst_positive_code_unit_sum_resultmaskentryleft) + (dst_positive_scale_unit_sum_resultmaskentryleft)) + ((dst_positive_scale_unit_sum_resultmaskentryleft) + (dst_positive_scale_unit_sum_resultmaskentryleft))) + (((dst_negative_code_unit_sum_resultmaskentryleft) + (dst_negative_scale_unit_sum_resultmaskentryleft)) * S ((dst_negative_code_unit_sum_resultmaskentryleft) + (dst_negative_scale_unit_sum_resultmaskentryleft)) + ((dst_negative_scale_unit_sum_resultmaskentryleft) + (dst_negative_scale_unit_sum_resultmaskentryleft)))) * S ((((dst_positive_code_unit_sum_resultmaskentryleft) + (dst_positive_scale_unit_sum_resultmaskentryleft)) * S ((dst_positive_code_unit_sum_resultmaskentryleft) + (dst_positive_scale_unit_sum_resultmaskentryleft)) + ((dst_positive_scale_unit_sum_resultmaskentryleft) + (dst_positive_scale_unit_sum_resultmaskentryleft))) + (((dst_negative_code_unit_sum_resultmaskentryleft) + (dst_negative_scale_unit_sum_resultmaskentryleft)) * S ((dst_negative_code_unit_sum_resultmaskentryleft) + (dst_negative_scale_unit_sum_resultmaskentryleft)) + ((dst_negative_scale_unit_sum_resultmaskentryleft) + (dst_negative_scale_unit_sum_resultmaskentryleft)))) + ((((dst_negative_code_unit_sum_resultmaskentryleft) + (dst_negative_scale_unit_sum_resultmaskentryleft)) * S ((dst_negative_code_unit_sum_resultmaskentryleft) + (dst_negative_scale_unit_sum_resultmaskentryleft)) + ((dst_negative_scale_unit_sum_resultmaskentryleft) + (dst_negative_scale_unit_sum_resultmaskentryleft))) + (((dst_negative_code_unit_sum_resultmaskentryleft) + (dst_negative_scale_unit_sum_resultmaskentryleft)) * S ((dst_negative_code_unit_sum_resultmaskentryleft) + (dst_negative_scale_unit_sum_resultmaskentryleft)) + ((dst_negative_scale_unit_sum_resultmaskentryleft) + (dst_negative_scale_unit_sum_resultmaskentryleft)))))) /\ (((((exists ff_h_pvs_unit_sum_resultmaskentryleftpositive. ff_h_pvs_unit_sum_resultmaskentryleftpositive + S (dst_positive_unit_sum_resultmaskentryleft) = S ((S (dc_index_unit_sum_resultmask)) * dst_positive_scale_unit_sum_resultmaskentryleft)) /\ exists ff_q_pvs_unit_sum_resultmaskentryleftpositive. dst_positive_code_unit_sum_resultmaskentryleft = ff_q_pvs_unit_sum_resultmaskentryleftpositive * S ((S (dc_index_unit_sum_resultmask)) * dst_positive_scale_unit_sum_resultmaskentryleft) + (dst_positive_unit_sum_resultmaskentryleft))) /\ (((((exists ff_h_pvs_unit_sum_resultmaskentryleftnegative. ff_h_pvs_unit_sum_resultmaskentryleftnegative + S (dst_negative_unit_sum_resultmaskentryleft) = S ((S (dc_index_unit_sum_resultmask)) * dst_negative_scale_unit_sum_resultmaskentryleft)) /\ exists ff_q_pvs_unit_sum_resultmaskentryleftnegative. dst_negative_code_unit_sum_resultmaskentryleft = ff_q_pvs_unit_sum_resultmaskentryleftnegative * S ((S (dc_index_unit_sum_resultmask)) * dst_negative_scale_unit_sum_resultmaskentryleft) + (dst_negative_unit_sum_resultmaskentryleft))) /\ (exists ge_balance_positive_unit_sum_resultmaskentryleftvalue ge_balance_negative_unit_sum_resultmaskentryleftvalue. (((((dc_left_unit_sum_resultmaskentry) = 2 * (ge_balance_positive_unit_sum_resultmaskentryleftvalue) /\ (ge_balance_negative_unit_sum_resultmaskentryleftvalue) = 0) \/ exists ge_signed_half_unit_sum_resultmaskentryleftvaluedecode. (((dc_left_unit_sum_resultmaskentry) = 2 * ge_signed_half_unit_sum_resultmaskentryleftvaluedecode + 1 /\ (ge_balance_positive_unit_sum_resultmaskentryleftvalue) = 0) /\ (ge_balance_negative_unit_sum_resultmaskentryleftvalue) = S ge_signed_half_unit_sum_resultmaskentryleftvaluedecode))) /\ ((dst_positive_unit_sum_resultmaskentryleft) + ge_balance_negative_unit_sum_resultmaskentryleftvalue = (dst_negative_unit_sum_resultmaskentryleft) + ge_balance_positive_unit_sum_resultmaskentryleftvalue))))))))) /\ (((exists dst_positive_code_unit_sum_resultmaskentryright dst_positive_scale_unit_sum_resultmaskentryright dst_negative_code_unit_sum_resultmaskentryright dst_negative_scale_unit_sum_resultmaskentryright dst_positive_unit_sum_resultmaskentryright dst_negative_unit_sum_resultmaskentryright. (((E) = (((((dst_positive_code_unit_sum_resultmaskentryright) + (dst_positive_scale_unit_sum_resultmaskentryright)) * S ((dst_positive_code_unit_sum_resultmaskentryright) + (dst_positive_scale_unit_sum_resultmaskentryright)) + ((dst_positive_scale_unit_sum_resultmaskentryright) + (dst_positive_scale_unit_sum_resultmaskentryright))) + (((dst_negative_code_unit_sum_resultmaskentryright) + (dst_negative_scale_unit_sum_resultmaskentryright)) * S ((dst_negative_code_unit_sum_resultmaskentryright) + (dst_negative_scale_unit_sum_resultmaskentryright)) + ((dst_negative_scale_unit_sum_resultmaskentryright) + (dst_negative_scale_unit_sum_resultmaskentryright)))) * S ((((dst_positive_code_unit_sum_resultmaskentryright) + (dst_positive_scale_unit_sum_resultmaskentryright)) * S ((dst_positive_code_unit_sum_resultmaskentryright) + (dst_positive_scale_unit_sum_resultmaskentryright)) + ((dst_positive_scale_unit_sum_resultmaskentryright) + (dst_positive_scale_unit_sum_resultmaskentryright))) + (((dst_negative_code_unit_sum_resultmaskentryright) + (dst_negative_scale_unit_sum_resultmaskentryright)) * S ((dst_negative_code_unit_sum_resultmaskentryright) + (dst_negative_scale_unit_sum_resultmaskentryright)) + ((dst_negative_scale_unit_sum_resultmaskentryright) + (dst_negative_scale_unit_sum_resultmaskentryright)))) + ((((dst_negative_code_unit_sum_resultmaskentryright) + (dst_negative_scale_unit_sum_resultmaskentryright)) * S ((dst_negative_code_unit_sum_resultmaskentryright) + (dst_negative_scale_unit_sum_resultmaskentryright)) + ((dst_negative_scale_unit_sum_resultmaskentryright) + (dst_negative_scale_unit_sum_resultmaskentryright))) + (((dst_negative_code_unit_sum_resultmaskentryright) + (dst_negative_scale_unit_sum_resultmaskentryright)) * S ((dst_negative_code_unit_sum_resultmaskentryright) + (dst_negative_scale_unit_sum_resultmaskentryright)) + ((dst_negative_scale_unit_sum_resultmaskentryright) + (dst_negative_scale_unit_sum_resultmaskentryright)))))) /\ (((((exists ff_h_pvs_unit_sum_resultmaskentryrightpositive. ff_h_pvs_unit_sum_resultmaskentryrightpositive + S (dst_positive_unit_sum_resultmaskentryright) = S ((S (dc_quotient_unit_sum_resultmaskentry)) * dst_positive_scale_unit_sum_resultmaskentryright)) /\ exists ff_q_pvs_unit_sum_resultmaskentryrightpositive. dst_positive_code_unit_sum_resultmaskentryright = ff_q_pvs_unit_sum_resultmaskentryrightpositive * S ((S (dc_quotient_unit_sum_resultmaskentry)) * dst_positive_scale_unit_sum_resultmaskentryright) + (dst_positive_unit_sum_resultmaskentryright))) /\ (((((exists ff_h_pvs_unit_sum_resultmaskentryrightnegative. ff_h_pvs_unit_sum_resultmaskentryrightnegative + S (dst_negative_unit_sum_resultmaskentryright) = S ((S (dc_quotient_unit_sum_resultmaskentry)) * dst_negative_scale_unit_sum_resultmaskentryright)) /\ exists ff_q_pvs_unit_sum_resultmaskentryrightnegative. dst_negative_code_unit_sum_resultmaskentryright = ff_q_pvs_unit_sum_resultmaskentryrightnegative * S ((S (dc_quotient_unit_sum_resultmaskentry)) * dst_negative_scale_unit_sum_resultmaskentryright) + (dst_negative_unit_sum_resultmaskentryright))) /\ (exists ge_balance_positive_unit_sum_resultmaskentryrightvalue ge_balance_negative_unit_sum_resultmaskentryrightvalue. (((((dc_right_unit_sum_resultmaskentry) = 2 * (ge_balance_positive_unit_sum_resultmaskentryrightvalue) /\ (ge_balance_negative_unit_sum_resultmaskentryrightvalue) = 0) \/ exists ge_signed_half_unit_sum_resultmaskentryrightvaluedecode. (((dc_right_unit_sum_resultmaskentry) = 2 * ge_signed_half_unit_sum_resultmaskentryrightvaluedecode + 1 /\ (ge_balance_positive_unit_sum_resultmaskentryrightvalue) = 0) /\ (ge_balance_negative_unit_sum_resultmaskentryrightvalue) = S ge_signed_half_unit_sum_resultmaskentryrightvaluedecode))) /\ ((dst_positive_unit_sum_resultmaskentryright) + ge_balance_negative_unit_sum_resultmaskentryrightvalue = (dst_negative_unit_sum_resultmaskentryright) + ge_balance_positive_unit_sum_resultmaskentryrightvalue))))))))) /\ (exists sto_ap_unit_sum_resultmaskentryproduct sto_an_unit_sum_resultmaskentryproduct sto_bp_unit_sum_resultmaskentryproduct sto_bn_unit_sum_resultmaskentryproduct sto_cp_unit_sum_resultmaskentryproduct sto_cn_unit_sum_resultmaskentryproduct. (((((dc_left_unit_sum_resultmaskentry) = 2 * (sto_ap_unit_sum_resultmaskentryproduct) /\ (sto_an_unit_sum_resultmaskentryproduct) = 0) \/ exists ge_signed_half_unit_sum_resultmaskentryproductleft. (((dc_left_unit_sum_resultmaskentry) = 2 * ge_signed_half_unit_sum_resultmaskentryproductleft + 1 /\ (sto_ap_unit_sum_resultmaskentryproduct) = 0) /\ (sto_an_unit_sum_resultmaskentryproduct) = S ge_signed_half_unit_sum_resultmaskentryproductleft))) /\ ((((((dc_right_unit_sum_resultmaskentry) = 2 * (sto_bp_unit_sum_resultmaskentryproduct) /\ (sto_bn_unit_sum_resultmaskentryproduct) = 0) \/ exists ge_signed_half_unit_sum_resultmaskentryproductright. (((dc_right_unit_sum_resultmaskentry) = 2 * ge_signed_half_unit_sum_resultmaskentryproductright + 1 /\ (sto_bp_unit_sum_resultmaskentryproduct) = 0) /\ (sto_bn_unit_sum_resultmaskentryproduct) = S ge_signed_half_unit_sum_resultmaskentryproductright))) /\ ((((((dc_value_unit_sum_resultmask) = 2 * (sto_cp_unit_sum_resultmaskentryproduct) /\ (sto_cn_unit_sum_resultmaskentryproduct) = 0) \/ exists ge_signed_half_unit_sum_resultmaskentryproductoutput. (((dc_value_unit_sum_resultmask) = 2 * ge_signed_half_unit_sum_resultmaskentryproductoutput + 1 /\ (sto_cp_unit_sum_resultmaskentryproduct) = 0) /\ (sto_cn_unit_sum_resultmaskentryproduct) = S ge_signed_half_unit_sum_resultmaskentryproductoutput))) /\ ((sto_ap_unit_sum_resultmaskentryproduct * sto_bp_unit_sum_resultmaskentryproduct + sto_an_unit_sum_resultmaskentryproduct * sto_bn_unit_sum_resultmaskentryproduct) + sto_cn_unit_sum_resultmaskentryproduct = (sto_ap_unit_sum_resultmaskentryproduct * sto_bn_unit_sum_resultmaskentryproduct + sto_an_unit_sum_resultmaskentryproduct * sto_bp_unit_sum_resultmaskentryproduct) + sto_cp_unit_sum_resultmaskentryproduct))))))))))))))) \/ ((((dc_index_unit_sum_resultmask)=0 \/ ~(exists pvs_factor_unit_sum_resultmaskentrynondivisor. (n) = (dc_index_unit_sum_resultmask) * pvs_factor_unit_sum_resultmaskentrynondivisor)) /\ ((dc_value_unit_sum_resultmask)=0))))))) /\ (exists dst_positive_code_unit_sum_resultfold dst_positive_scale_unit_sum_resultfold dst_negative_code_unit_sum_resultfold dst_negative_scale_unit_sum_resultfold dst_positive_sum_unit_sum_resultfold dst_negative_sum_unit_sum_resultfold. (((dc_mask_unit_sum_result) = (((((dst_positive_code_unit_sum_resultfold) + (dst_positive_scale_unit_sum_resultfold)) * S ((dst_positive_code_unit_sum_resultfold) + (dst_positive_scale_unit_sum_resultfold)) + ((dst_positive_scale_unit_sum_resultfold) + (dst_positive_scale_unit_sum_resultfold))) + (((dst_negative_code_unit_sum_resultfold) + (dst_negative_scale_unit_sum_resultfold)) * S ((dst_negative_code_unit_sum_resultfold) + (dst_negative_scale_unit_sum_resultfold)) + ((dst_negative_scale_unit_sum_resultfold) + (dst_negative_scale_unit_sum_resultfold)))) * S ((((dst_positive_code_unit_sum_resultfold) + (dst_positive_scale_unit_sum_resultfold)) * S ((dst_positive_code_unit_sum_resultfold) + (dst_positive_scale_unit_sum_resultfold)) + ((dst_positive_scale_unit_sum_resultfold) + (dst_positive_scale_unit_sum_resultfold))) + (((dst_negative_code_unit_sum_resultfold) + (dst_negative_scale_unit_sum_resultfold)) * S ((dst_negative_code_unit_sum_resultfold) + (dst_negative_scale_unit_sum_resultfold)) + ((dst_negative_scale_unit_sum_resultfold) + (dst_negative_scale_unit_sum_resultfold)))) + ((((dst_negative_code_unit_sum_resultfold) + (dst_negative_scale_unit_sum_resultfold)) * S ((dst_negative_code_unit_sum_resultfold) + (dst_negative_scale_unit_sum_resultfold)) + ((dst_negative_scale_unit_sum_resultfold) + (dst_negative_scale_unit_sum_resultfold))) + (((dst_negative_code_unit_sum_resultfold) + (dst_negative_scale_unit_sum_resultfold)) * S ((dst_negative_code_unit_sum_resultfold) + (dst_negative_scale_unit_sum_resultfold)) + ((dst_negative_scale_unit_sum_resultfold) + (dst_negative_scale_unit_sum_resultfold)))))) /\ (((exists fs_u_dst_unit_sum_resultfoldpositive fs_v_dst_unit_sum_resultfoldpositive. ((((exists fs_h_dst_unit_sum_resultfoldpositive_body_start. fs_h_dst_unit_sum_resultfoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_unit_sum_resultfoldpositive)) /\ exists fs_q_dst_unit_sum_resultfoldpositive_body_start. fs_u_dst_unit_sum_resultfoldpositive = fs_q_dst_unit_sum_resultfoldpositive_body_start * S ((S (0)) * fs_v_dst_unit_sum_resultfoldpositive) + (0))) /\ ((((exists fs_h_dst_unit_sum_resultfoldpositive_body_terminal. fs_h_dst_unit_sum_resultfoldpositive_body_terminal + S (dst_positive_sum_unit_sum_resultfold) = S ((S (S (n))) * fs_v_dst_unit_sum_resultfoldpositive)) /\ exists fs_q_dst_unit_sum_resultfoldpositive_body_terminal. fs_u_dst_unit_sum_resultfoldpositive = fs_q_dst_unit_sum_resultfoldpositive_body_terminal * S ((S (S (n))) * fs_v_dst_unit_sum_resultfoldpositive) + (dst_positive_sum_unit_sum_resultfold))) /\ forall fs_i_dst_unit_sum_resultfoldpositive_body_steps. (exists fs_lt_dst_unit_sum_resultfoldpositive_body_steps_bound. fs_lt_dst_unit_sum_resultfoldpositive_body_steps_bound + S fs_i_dst_unit_sum_resultfoldpositive_body_steps = S (n)) -> exists fs_a_dst_unit_sum_resultfoldpositive_body_steps fs_r_dst_unit_sum_resultfoldpositive_body_steps fs_s_dst_unit_sum_resultfoldpositive_body_steps. ((((exists fs_h_dst_unit_sum_resultfoldpositive_body_steps_summand. fs_h_dst_unit_sum_resultfoldpositive_body_steps_summand + S (fs_a_dst_unit_sum_resultfoldpositive_body_steps) = S ((S (fs_i_dst_unit_sum_resultfoldpositive_body_steps)) * dst_positive_scale_unit_sum_resultfold)) /\ exists fs_q_dst_unit_sum_resultfoldpositive_body_steps_summand. dst_positive_code_unit_sum_resultfold = fs_q_dst_unit_sum_resultfoldpositive_body_steps_summand * S ((S (fs_i_dst_unit_sum_resultfoldpositive_body_steps)) * dst_positive_scale_unit_sum_resultfold) + (fs_a_dst_unit_sum_resultfoldpositive_body_steps))) /\ ((((exists fs_h_dst_unit_sum_resultfoldpositive_body_steps_partial. fs_h_dst_unit_sum_resultfoldpositive_body_steps_partial + S (fs_r_dst_unit_sum_resultfoldpositive_body_steps) = S ((S (fs_i_dst_unit_sum_resultfoldpositive_body_steps)) * fs_v_dst_unit_sum_resultfoldpositive)) /\ exists fs_q_dst_unit_sum_resultfoldpositive_body_steps_partial. fs_u_dst_unit_sum_resultfoldpositive = fs_q_dst_unit_sum_resultfoldpositive_body_steps_partial * S ((S (fs_i_dst_unit_sum_resultfoldpositive_body_steps)) * fs_v_dst_unit_sum_resultfoldpositive) + (fs_r_dst_unit_sum_resultfoldpositive_body_steps))) /\ ((((exists fs_h_dst_unit_sum_resultfoldpositive_body_steps_successor. fs_h_dst_unit_sum_resultfoldpositive_body_steps_successor + S (fs_s_dst_unit_sum_resultfoldpositive_body_steps) = S ((S (S fs_i_dst_unit_sum_resultfoldpositive_body_steps)) * fs_v_dst_unit_sum_resultfoldpositive)) /\ exists fs_q_dst_unit_sum_resultfoldpositive_body_steps_successor. fs_u_dst_unit_sum_resultfoldpositive = fs_q_dst_unit_sum_resultfoldpositive_body_steps_successor * S ((S (S fs_i_dst_unit_sum_resultfoldpositive_body_steps)) * fs_v_dst_unit_sum_resultfoldpositive) + (fs_s_dst_unit_sum_resultfoldpositive_body_steps))) /\ fs_s_dst_unit_sum_resultfoldpositive_body_steps = fs_r_dst_unit_sum_resultfoldpositive_body_steps + fs_a_dst_unit_sum_resultfoldpositive_body_steps)))))) /\ (((exists fs_u_dst_unit_sum_resultfoldnegative fs_v_dst_unit_sum_resultfoldnegative. ((((exists fs_h_dst_unit_sum_resultfoldnegative_body_start. fs_h_dst_unit_sum_resultfoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_unit_sum_resultfoldnegative)) /\ exists fs_q_dst_unit_sum_resultfoldnegative_body_start. fs_u_dst_unit_sum_resultfoldnegative = fs_q_dst_unit_sum_resultfoldnegative_body_start * S ((S (0)) * fs_v_dst_unit_sum_resultfoldnegative) + (0))) /\ ((((exists fs_h_dst_unit_sum_resultfoldnegative_body_terminal. fs_h_dst_unit_sum_resultfoldnegative_body_terminal + S (dst_negative_sum_unit_sum_resultfold) = S ((S (S (n))) * fs_v_dst_unit_sum_resultfoldnegative)) /\ exists fs_q_dst_unit_sum_resultfoldnegative_body_terminal. fs_u_dst_unit_sum_resultfoldnegative = fs_q_dst_unit_sum_resultfoldnegative_body_terminal * S ((S (S (n))) * fs_v_dst_unit_sum_resultfoldnegative) + (dst_negative_sum_unit_sum_resultfold))) /\ forall fs_i_dst_unit_sum_resultfoldnegative_body_steps. (exists fs_lt_dst_unit_sum_resultfoldnegative_body_steps_bound. fs_lt_dst_unit_sum_resultfoldnegative_body_steps_bound + S fs_i_dst_unit_sum_resultfoldnegative_body_steps = S (n)) -> exists fs_a_dst_unit_sum_resultfoldnegative_body_steps fs_r_dst_unit_sum_resultfoldnegative_body_steps fs_s_dst_unit_sum_resultfoldnegative_body_steps. ((((exists fs_h_dst_unit_sum_resultfoldnegative_body_steps_summand. fs_h_dst_unit_sum_resultfoldnegative_body_steps_summand + S (fs_a_dst_unit_sum_resultfoldnegative_body_steps) = S ((S (fs_i_dst_unit_sum_resultfoldnegative_body_steps)) * dst_negative_scale_unit_sum_resultfold)) /\ exists fs_q_dst_unit_sum_resultfoldnegative_body_steps_summand. dst_negative_code_unit_sum_resultfold = fs_q_dst_unit_sum_resultfoldnegative_body_steps_summand * S ((S (fs_i_dst_unit_sum_resultfoldnegative_body_steps)) * dst_negative_scale_unit_sum_resultfold) + (fs_a_dst_unit_sum_resultfoldnegative_body_steps))) /\ ((((exists fs_h_dst_unit_sum_resultfoldnegative_body_steps_partial. fs_h_dst_unit_sum_resultfoldnegative_body_steps_partial + S (fs_r_dst_unit_sum_resultfoldnegative_body_steps) = S ((S (fs_i_dst_unit_sum_resultfoldnegative_body_steps)) * fs_v_dst_unit_sum_resultfoldnegative)) /\ exists fs_q_dst_unit_sum_resultfoldnegative_body_steps_partial. fs_u_dst_unit_sum_resultfoldnegative = fs_q_dst_unit_sum_resultfoldnegative_body_steps_partial * S ((S (fs_i_dst_unit_sum_resultfoldnegative_body_steps)) * fs_v_dst_unit_sum_resultfoldnegative) + (fs_r_dst_unit_sum_resultfoldnegative_body_steps))) /\ ((((exists fs_h_dst_unit_sum_resultfoldnegative_body_steps_successor. fs_h_dst_unit_sum_resultfoldnegative_body_steps_successor + S (fs_s_dst_unit_sum_resultfoldnegative_body_steps) = S ((S (S fs_i_dst_unit_sum_resultfoldnegative_body_steps)) * fs_v_dst_unit_sum_resultfoldnegative)) /\ exists fs_q_dst_unit_sum_resultfoldnegative_body_steps_successor. fs_u_dst_unit_sum_resultfoldnegative = fs_q_dst_unit_sum_resultfoldnegative_body_steps_successor * S ((S (S fs_i_dst_unit_sum_resultfoldnegative_body_steps)) * fs_v_dst_unit_sum_resultfoldnegative) + (fs_s_dst_unit_sum_resultfoldnegative_body_steps))) /\ fs_s_dst_unit_sum_resultfoldnegative_body_steps = fs_r_dst_unit_sum_resultfoldnegative_body_steps + fs_a_dst_unit_sum_resultfoldnegative_body_steps)))))) /\ (exists ge_balance_positive_unit_sum_resultfoldresult ge_balance_negative_unit_sum_resultfoldresult. (((((a) = 2 * (ge_balance_positive_unit_sum_resultfoldresult) /\ (ge_balance_negative_unit_sum_resultfoldresult) = 0) \/ exists ge_signed_half_unit_sum_resultfoldresultdecode. (((a) = 2 * ge_signed_half_unit_sum_resultfoldresultdecode + 1 /\ (ge_balance_positive_unit_sum_resultfoldresult) = 0) /\ (ge_balance_negative_unit_sum_resultfoldresult) = S ge_signed_half_unit_sum_resultfoldresultdecode))) /\ ((dst_positive_sum_unit_sum_resultfold) + ge_balance_negative_unit_sum_resultfoldresult = (dst_negative_sum_unit_sum_resultfold) + ge_balance_positive_unit_sum_resultfoldresult)))))))))))))