signed_support_reindex_sum_exists

Exact expanded first-order arithmetic statement

forall A B r s L M. (((exists dst_positive_code_exists_supportsource_table dst_positive_scale_exists_supportsource_table dst_negative_code_exists_supportsource_table dst_negative_scale_exists_supportsource_table. (((A) = (((((dst_positive_code_exists_supportsource_table) + (dst_positive_scale_exists_supportsource_table)) * S ((dst_positive_code_exists_supportsource_table) + (dst_positive_scale_exists_supportsource_table)) + ((dst_positive_scale_exists_supportsource_table) + (dst_positive_scale_exists_supportsource_table))) + (((dst_negative_code_exists_supportsource_table) + (dst_negative_scale_exists_supportsource_table)) * S ((dst_negative_code_exists_supportsource_table) + (dst_negative_scale_exists_supportsource_table)) + ((dst_negative_scale_exists_supportsource_table) + (dst_negative_scale_exists_supportsource_table)))) * S ((((dst_positive_code_exists_supportsource_table) + (dst_positive_scale_exists_supportsource_table)) * S ((dst_positive_code_exists_supportsource_table) + (dst_positive_scale_exists_supportsource_table)) + ((dst_positive_scale_exists_supportsource_table) + (dst_positive_scale_exists_supportsource_table))) + (((dst_negative_code_exists_supportsource_table) + (dst_negative_scale_exists_supportsource_table)) * S ((dst_negative_code_exists_supportsource_table) + (dst_negative_scale_exists_supportsource_table)) + ((dst_negative_scale_exists_supportsource_table) + (dst_negative_scale_exists_supportsource_table)))) + ((((dst_negative_code_exists_supportsource_table) + (dst_negative_scale_exists_supportsource_table)) * S ((dst_negative_code_exists_supportsource_table) + (dst_negative_scale_exists_supportsource_table)) + ((dst_negative_scale_exists_supportsource_table) + (dst_negative_scale_exists_supportsource_table))) + (((dst_negative_code_exists_supportsource_table) + (dst_negative_scale_exists_supportsource_table)) * S ((dst_negative_code_exists_supportsource_table) + (dst_negative_scale_exists_supportsource_table)) + ((dst_negative_scale_exists_supportsource_table) + (dst_negative_scale_exists_supportsource_table)))))) /\ (forall dst_index_exists_supportsource_table. (exists pvs_le_gap_exists_supportsource_tabledomain. pvs_le_gap_exists_supportsource_tabledomain + (dst_index_exists_supportsource_table) = (0)) -> exists dst_positive_exists_supportsource_table dst_negative_exists_supportsource_table dst_value_exists_supportsource_table. ((((exists ff_h_pvs_exists_supportsource_tableentrypositive. ff_h_pvs_exists_supportsource_tableentrypositive + S (dst_positive_exists_supportsource_table) = S ((S (dst_index_exists_supportsource_table)) * dst_positive_scale_exists_supportsource_table)) /\ exists ff_q_pvs_exists_supportsource_tableentrypositive. dst_positive_code_exists_supportsource_table = ff_q_pvs_exists_supportsource_tableentrypositive * S ((S (dst_index_exists_supportsource_table)) * dst_positive_scale_exists_supportsource_table) + (dst_positive_exists_supportsource_table))) /\ (((((exists ff_h_pvs_exists_supportsource_tableentrynegative. ff_h_pvs_exists_supportsource_tableentrynegative + S (dst_negative_exists_supportsource_table) = S ((S (dst_index_exists_supportsource_table)) * dst_negative_scale_exists_supportsource_table)) /\ exists ff_q_pvs_exists_supportsource_tableentrynegative. dst_negative_code_exists_supportsource_table = ff_q_pvs_exists_supportsource_tableentrynegative * S ((S (dst_index_exists_supportsource_table)) * dst_negative_scale_exists_supportsource_table) + (dst_negative_exists_supportsource_table))) /\ (exists ge_balance_positive_exists_supportsource_tableentryvalue ge_balance_negative_exists_supportsource_tableentryvalue. (((((dst_value_exists_supportsource_table) = 2 * (ge_balance_positive_exists_supportsource_tableentryvalue) /\ (ge_balance_negative_exists_supportsource_tableentryvalue) = 0) \/ exists ge_signed_half_exists_supportsource_tableentryvaluedecode. (((dst_value_exists_supportsource_table) = 2 * ge_signed_half_exists_supportsource_tableentryvaluedecode + 1 /\ (ge_balance_positive_exists_supportsource_tableentryvalue) = 0) /\ (ge_balance_negative_exists_supportsource_tableentryvalue) = S ge_signed_half_exists_supportsource_tableentryvaluedecode))) /\ ((dst_positive_exists_supportsource_table) + ge_balance_negative_exists_supportsource_tableentryvalue = (dst_negative_exists_supportsource_table) + ge_balance_positive_exists_supportsource_tableentryvalue))))))))) /\ (((exists dst_positive_code_exists_supporttarget_table dst_positive_scale_exists_supporttarget_table dst_negative_code_exists_supporttarget_table dst_negative_scale_exists_supporttarget_table. (((B) = (((((dst_positive_code_exists_supporttarget_table) + (dst_positive_scale_exists_supporttarget_table)) * S ((dst_positive_code_exists_supporttarget_table) + (dst_positive_scale_exists_supporttarget_table)) + ((dst_positive_scale_exists_supporttarget_table) + (dst_positive_scale_exists_supporttarget_table))) + (((dst_negative_code_exists_supporttarget_table) + (dst_negative_scale_exists_supporttarget_table)) * S ((dst_negative_code_exists_supporttarget_table) + (dst_negative_scale_exists_supporttarget_table)) + ((dst_negative_scale_exists_supporttarget_table) + (dst_negative_scale_exists_supporttarget_table)))) * S ((((dst_positive_code_exists_supporttarget_table) + (dst_positive_scale_exists_supporttarget_table)) * S ((dst_positive_code_exists_supporttarget_table) + (dst_positive_scale_exists_supporttarget_table)) + ((dst_positive_scale_exists_supporttarget_table) + (dst_positive_scale_exists_supporttarget_table))) + (((dst_negative_code_exists_supporttarget_table) + (dst_negative_scale_exists_supporttarget_table)) * S ((dst_negative_code_exists_supporttarget_table) + (dst_negative_scale_exists_supporttarget_table)) + ((dst_negative_scale_exists_supporttarget_table) + (dst_negative_scale_exists_supporttarget_table)))) + ((((dst_negative_code_exists_supporttarget_table) + (dst_negative_scale_exists_supporttarget_table)) * S ((dst_negative_code_exists_supporttarget_table) + (dst_negative_scale_exists_supporttarget_table)) + ((dst_negative_scale_exists_supporttarget_table) + (dst_negative_scale_exists_supporttarget_table))) + (((dst_negative_code_exists_supporttarget_table) + (dst_negative_scale_exists_supporttarget_table)) * S ((dst_negative_code_exists_supporttarget_table) + (dst_negative_scale_exists_supporttarget_table)) + ((dst_negative_scale_exists_supporttarget_table) + (dst_negative_scale_exists_supporttarget_table)))))) /\ (forall dst_index_exists_supporttarget_table. (exists pvs_le_gap_exists_supporttarget_tabledomain. pvs_le_gap_exists_supporttarget_tabledomain + (dst_index_exists_supporttarget_table) = (0)) -> exists dst_positive_exists_supporttarget_table dst_negative_exists_supporttarget_table dst_value_exists_supporttarget_table. ((((exists ff_h_pvs_exists_supporttarget_tableentrypositive. ff_h_pvs_exists_supporttarget_tableentrypositive + S (dst_positive_exists_supporttarget_table) = S ((S (dst_index_exists_supporttarget_table)) * dst_positive_scale_exists_supporttarget_table)) /\ exists ff_q_pvs_exists_supporttarget_tableentrypositive. dst_positive_code_exists_supporttarget_table = ff_q_pvs_exists_supporttarget_tableentrypositive * S ((S (dst_index_exists_supporttarget_table)) * dst_positive_scale_exists_supporttarget_table) + (dst_positive_exists_supporttarget_table))) /\ (((((exists ff_h_pvs_exists_supporttarget_tableentrynegative. ff_h_pvs_exists_supporttarget_tableentrynegative + S (dst_negative_exists_supporttarget_table) = S ((S (dst_index_exists_supporttarget_table)) * dst_negative_scale_exists_supporttarget_table)) /\ exists ff_q_pvs_exists_supporttarget_tableentrynegative. dst_negative_code_exists_supporttarget_table = ff_q_pvs_exists_supporttarget_tableentrynegative * S ((S (dst_index_exists_supporttarget_table)) * dst_negative_scale_exists_supporttarget_table) + (dst_negative_exists_supporttarget_table))) /\ (exists ge_balance_positive_exists_supporttarget_tableentryvalue ge_balance_negative_exists_supporttarget_tableentryvalue. (((((dst_value_exists_supporttarget_table) = 2 * (ge_balance_positive_exists_supporttarget_tableentryvalue) /\ (ge_balance_negative_exists_supporttarget_tableentryvalue) = 0) \/ exists ge_signed_half_exists_supporttarget_tableentryvaluedecode. (((dst_value_exists_supporttarget_table) = 2 * ge_signed_half_exists_supporttarget_tableentryvaluedecode + 1 /\ (ge_balance_positive_exists_supporttarget_tableentryvalue) = 0) /\ (ge_balance_negative_exists_supporttarget_tableentryvalue) = S ge_signed_half_exists_supporttarget_tableentryvaluedecode))) /\ ((dst_positive_exists_supporttarget_table) + ge_balance_negative_exists_supporttarget_tableentryvalue = (dst_negative_exists_supporttarget_table) + ge_balance_positive_exists_supporttarget_tableentryvalue))))))))) /\ (((forall ssr_source_exists_supportpreserve ssr_value_exists_supportpreserve. (exists pvs_gap_exists_supportpreservesource_bound. pvs_gap_exists_supportpreservesource_bound + S (ssr_source_exists_supportpreserve) = (L)) -> (exists dst_positive_code_exists_supportpreservesource_value dst_positive_scale_exists_supportpreservesource_value dst_negative_code_exists_supportpreservesource_value dst_negative_scale_exists_supportpreservesource_value dst_positive_exists_supportpreservesource_value dst_negative_exists_supportpreservesource_value. (((A) = (((((dst_positive_code_exists_supportpreservesource_value) + (dst_positive_scale_exists_supportpreservesource_value)) * S ((dst_positive_code_exists_supportpreservesource_value) + (dst_positive_scale_exists_supportpreservesource_value)) + ((dst_positive_scale_exists_supportpreservesource_value) + (dst_positive_scale_exists_supportpreservesource_value))) + (((dst_negative_code_exists_supportpreservesource_value) + (dst_negative_scale_exists_supportpreservesource_value)) * S ((dst_negative_code_exists_supportpreservesource_value) + (dst_negative_scale_exists_supportpreservesource_value)) + ((dst_negative_scale_exists_supportpreservesource_value) + (dst_negative_scale_exists_supportpreservesource_value)))) * S ((((dst_positive_code_exists_supportpreservesource_value) + (dst_positive_scale_exists_supportpreservesource_value)) * S ((dst_positive_code_exists_supportpreservesource_value) + (dst_positive_scale_exists_supportpreservesource_value)) + ((dst_positive_scale_exists_supportpreservesource_value) + (dst_positive_scale_exists_supportpreservesource_value))) + (((dst_negative_code_exists_supportpreservesource_value) + (dst_negative_scale_exists_supportpreservesource_value)) * S ((dst_negative_code_exists_supportpreservesource_value) + (dst_negative_scale_exists_supportpreservesource_value)) + ((dst_negative_scale_exists_supportpreservesource_value) + (dst_negative_scale_exists_supportpreservesource_value)))) + ((((dst_negative_code_exists_supportpreservesource_value) + (dst_negative_scale_exists_supportpreservesource_value)) * S ((dst_negative_code_exists_supportpreservesource_value) + (dst_negative_scale_exists_supportpreservesource_value)) + ((dst_negative_scale_exists_supportpreservesource_value) + (dst_negative_scale_exists_supportpreservesource_value))) + (((dst_negative_code_exists_supportpreservesource_value) + (dst_negative_scale_exists_supportpreservesource_value)) * S ((dst_negative_code_exists_supportpreservesource_value) + (dst_negative_scale_exists_supportpreservesource_value)) + ((dst_negative_scale_exists_supportpreservesource_value) + (dst_negative_scale_exists_supportpreservesource_value)))))) /\ (((((exists ff_h_pvs_exists_supportpreservesource_valuepositive. ff_h_pvs_exists_supportpreservesource_valuepositive + S (dst_positive_exists_supportpreservesource_value) = S ((S (ssr_source_exists_supportpreserve)) * dst_positive_scale_exists_supportpreservesource_value)) /\ exists ff_q_pvs_exists_supportpreservesource_valuepositive. dst_positive_code_exists_supportpreservesource_value = ff_q_pvs_exists_supportpreservesource_valuepositive * S ((S (ssr_source_exists_supportpreserve)) * dst_positive_scale_exists_supportpreservesource_value) + (dst_positive_exists_supportpreservesource_value))) /\ (((((exists ff_h_pvs_exists_supportpreservesource_valuenegative. ff_h_pvs_exists_supportpreservesource_valuenegative + S (dst_negative_exists_supportpreservesource_value) = S ((S (ssr_source_exists_supportpreserve)) * dst_negative_scale_exists_supportpreservesource_value)) /\ exists ff_q_pvs_exists_supportpreservesource_valuenegative. dst_negative_code_exists_supportpreservesource_value = ff_q_pvs_exists_supportpreservesource_valuenegative * S ((S (ssr_source_exists_supportpreserve)) * dst_negative_scale_exists_supportpreservesource_value) + (dst_negative_exists_supportpreservesource_value))) /\ (exists ge_balance_positive_exists_supportpreservesource_valuevalue ge_balance_negative_exists_supportpreservesource_valuevalue. (((((ssr_value_exists_supportpreserve) = 2 * (ge_balance_positive_exists_supportpreservesource_valuevalue) /\ (ge_balance_negative_exists_supportpreservesource_valuevalue) = 0) \/ exists ge_signed_half_exists_supportpreservesource_valuevaluedecode. (((ssr_value_exists_supportpreserve) = 2 * ge_signed_half_exists_supportpreservesource_valuevaluedecode + 1 /\ (ge_balance_positive_exists_supportpreservesource_valuevalue) = 0) /\ (ge_balance_negative_exists_supportpreservesource_valuevalue) = S ge_signed_half_exists_supportpreservesource_valuevaluedecode))) /\ ((dst_positive_exists_supportpreservesource_value) + ge_balance_negative_exists_supportpreservesource_valuevalue = (dst_negative_exists_supportpreservesource_value) + ge_balance_positive_exists_supportpreservesource_valuevalue))))))))) -> ~(ssr_value_exists_supportpreserve=0) -> exists ssr_target_exists_supportpreserve. ((((exists ff_h_pvs_exists_supportpreservemap. ff_h_pvs_exists_supportpreservemap + S (ssr_target_exists_supportpreserve) = S ((S (ssr_source_exists_supportpreserve)) * s)) /\ exists ff_q_pvs_exists_supportpreservemap. r = ff_q_pvs_exists_supportpreservemap * S ((S (ssr_source_exists_supportpreserve)) * s) + (ssr_target_exists_supportpreserve))) /\ (((exists pvs_gap_exists_supportpreservetarget_bound. pvs_gap_exists_supportpreservetarget_bound + S (ssr_target_exists_supportpreserve) = (M)) /\ (exists dst_positive_code_exists_supportpreservetarget_value dst_positive_scale_exists_supportpreservetarget_value dst_negative_code_exists_supportpreservetarget_value dst_negative_scale_exists_supportpreservetarget_value dst_positive_exists_supportpreservetarget_value dst_negative_exists_supportpreservetarget_value. (((B) = (((((dst_positive_code_exists_supportpreservetarget_value) + (dst_positive_scale_exists_supportpreservetarget_value)) * S ((dst_positive_code_exists_supportpreservetarget_value) + (dst_positive_scale_exists_supportpreservetarget_value)) + ((dst_positive_scale_exists_supportpreservetarget_value) + (dst_positive_scale_exists_supportpreservetarget_value))) + (((dst_negative_code_exists_supportpreservetarget_value) + (dst_negative_scale_exists_supportpreservetarget_value)) * S ((dst_negative_code_exists_supportpreservetarget_value) + (dst_negative_scale_exists_supportpreservetarget_value)) + ((dst_negative_scale_exists_supportpreservetarget_value) + (dst_negative_scale_exists_supportpreservetarget_value)))) * S ((((dst_positive_code_exists_supportpreservetarget_value) + (dst_positive_scale_exists_supportpreservetarget_value)) * S ((dst_positive_code_exists_supportpreservetarget_value) + (dst_positive_scale_exists_supportpreservetarget_value)) + ((dst_positive_scale_exists_supportpreservetarget_value) + (dst_positive_scale_exists_supportpreservetarget_value))) + (((dst_negative_code_exists_supportpreservetarget_value) + (dst_negative_scale_exists_supportpreservetarget_value)) * S ((dst_negative_code_exists_supportpreservetarget_value) + (dst_negative_scale_exists_supportpreservetarget_value)) + ((dst_negative_scale_exists_supportpreservetarget_value) + (dst_negative_scale_exists_supportpreservetarget_value)))) + ((((dst_negative_code_exists_supportpreservetarget_value) + (dst_negative_scale_exists_supportpreservetarget_value)) * S ((dst_negative_code_exists_supportpreservetarget_value) + (dst_negative_scale_exists_supportpreservetarget_value)) + ((dst_negative_scale_exists_supportpreservetarget_value) + (dst_negative_scale_exists_supportpreservetarget_value))) + (((dst_negative_code_exists_supportpreservetarget_value) + (dst_negative_scale_exists_supportpreservetarget_value)) * S ((dst_negative_code_exists_supportpreservetarget_value) + (dst_negative_scale_exists_supportpreservetarget_value)) + ((dst_negative_scale_exists_supportpreservetarget_value) + (dst_negative_scale_exists_supportpreservetarget_value)))))) /\ (((((exists ff_h_pvs_exists_supportpreservetarget_valuepositive. ff_h_pvs_exists_supportpreservetarget_valuepositive + S (dst_positive_exists_supportpreservetarget_value) = S ((S (ssr_target_exists_supportpreserve)) * dst_positive_scale_exists_supportpreservetarget_value)) /\ exists ff_q_pvs_exists_supportpreservetarget_valuepositive. dst_positive_code_exists_supportpreservetarget_value = ff_q_pvs_exists_supportpreservetarget_valuepositive * S ((S (ssr_target_exists_supportpreserve)) * dst_positive_scale_exists_supportpreservetarget_value) + (dst_positive_exists_supportpreservetarget_value))) /\ (((((exists ff_h_pvs_exists_supportpreservetarget_valuenegative. ff_h_pvs_exists_supportpreservetarget_valuenegative + S (dst_negative_exists_supportpreservetarget_value) = S ((S (ssr_target_exists_supportpreserve)) * dst_negative_scale_exists_supportpreservetarget_value)) /\ exists ff_q_pvs_exists_supportpreservetarget_valuenegative. dst_negative_code_exists_supportpreservetarget_value = ff_q_pvs_exists_supportpreservetarget_valuenegative * S ((S (ssr_target_exists_supportpreserve)) * dst_negative_scale_exists_supportpreservetarget_value) + (dst_negative_exists_supportpreservetarget_value))) /\ (exists ge_balance_positive_exists_supportpreservetarget_valuevalue ge_balance_negative_exists_supportpreservetarget_valuevalue. (((((ssr_value_exists_supportpreserve) = 2 * (ge_balance_positive_exists_supportpreservetarget_valuevalue) /\ (ge_balance_negative_exists_supportpreservetarget_valuevalue) = 0) \/ exists ge_signed_half_exists_supportpreservetarget_valuevaluedecode. (((ssr_value_exists_supportpreserve) = 2 * ge_signed_half_exists_supportpreservetarget_valuevaluedecode + 1 /\ (ge_balance_positive_exists_supportpreservetarget_valuevalue) = 0) /\ (ge_balance_negative_exists_supportpreservetarget_valuevalue) = S ge_signed_half_exists_supportpreservetarget_valuevaluedecode))) /\ ((dst_positive_exists_supportpreservetarget_value) + ge_balance_negative_exists_supportpreservetarget_valuevalue = (dst_negative_exists_supportpreservetarget_value) + ge_balance_positive_exists_supportpreservetarget_valuevalue))))))))))))) /\ (((forall ssr_first_exists_supportinjective ssr_second_exists_supportinjective ssr_image_exists_supportinjective ssr_a_exists_supportinjective ssr_b_exists_supportinjective. (exists pvs_gap_exists_supportinjectivefirst_bound. pvs_gap_exists_supportinjectivefirst_bound + S (ssr_first_exists_supportinjective) = (L)) -> (exists pvs_gap_exists_supportinjectivesecond_bound. pvs_gap_exists_supportinjectivesecond_bound + S (ssr_second_exists_supportinjective) = (L)) -> (exists dst_positive_code_exists_supportinjectivefirst_value dst_positive_scale_exists_supportinjectivefirst_value dst_negative_code_exists_supportinjectivefirst_value dst_negative_scale_exists_supportinjectivefirst_value dst_positive_exists_supportinjectivefirst_value dst_negative_exists_supportinjectivefirst_value. (((A) = (((((dst_positive_code_exists_supportinjectivefirst_value) + (dst_positive_scale_exists_supportinjectivefirst_value)) * S ((dst_positive_code_exists_supportinjectivefirst_value) + (dst_positive_scale_exists_supportinjectivefirst_value)) + ((dst_positive_scale_exists_supportinjectivefirst_value) + (dst_positive_scale_exists_supportinjectivefirst_value))) + (((dst_negative_code_exists_supportinjectivefirst_value) + (dst_negative_scale_exists_supportinjectivefirst_value)) * S ((dst_negative_code_exists_supportinjectivefirst_value) + (dst_negative_scale_exists_supportinjectivefirst_value)) + ((dst_negative_scale_exists_supportinjectivefirst_value) + (dst_negative_scale_exists_supportinjectivefirst_value)))) * S ((((dst_positive_code_exists_supportinjectivefirst_value) + (dst_positive_scale_exists_supportinjectivefirst_value)) * S ((dst_positive_code_exists_supportinjectivefirst_value) + (dst_positive_scale_exists_supportinjectivefirst_value)) + ((dst_positive_scale_exists_supportinjectivefirst_value) + (dst_positive_scale_exists_supportinjectivefirst_value))) + (((dst_negative_code_exists_supportinjectivefirst_value) + (dst_negative_scale_exists_supportinjectivefirst_value)) * S ((dst_negative_code_exists_supportinjectivefirst_value) + (dst_negative_scale_exists_supportinjectivefirst_value)) + ((dst_negative_scale_exists_supportinjectivefirst_value) + (dst_negative_scale_exists_supportinjectivefirst_value)))) + ((((dst_negative_code_exists_supportinjectivefirst_value) + (dst_negative_scale_exists_supportinjectivefirst_value)) * S ((dst_negative_code_exists_supportinjectivefirst_value) + (dst_negative_scale_exists_supportinjectivefirst_value)) + ((dst_negative_scale_exists_supportinjectivefirst_value) + (dst_negative_scale_exists_supportinjectivefirst_value))) + (((dst_negative_code_exists_supportinjectivefirst_value) + (dst_negative_scale_exists_supportinjectivefirst_value)) * S ((dst_negative_code_exists_supportinjectivefirst_value) + (dst_negative_scale_exists_supportinjectivefirst_value)) + ((dst_negative_scale_exists_supportinjectivefirst_value) + (dst_negative_scale_exists_supportinjectivefirst_value)))))) /\ (((((exists ff_h_pvs_exists_supportinjectivefirst_valuepositive. ff_h_pvs_exists_supportinjectivefirst_valuepositive + S (dst_positive_exists_supportinjectivefirst_value) = S ((S (ssr_first_exists_supportinjective)) * dst_positive_scale_exists_supportinjectivefirst_value)) /\ exists ff_q_pvs_exists_supportinjectivefirst_valuepositive. dst_positive_code_exists_supportinjectivefirst_value = ff_q_pvs_exists_supportinjectivefirst_valuepositive * S ((S (ssr_first_exists_supportinjective)) * dst_positive_scale_exists_supportinjectivefirst_value) + (dst_positive_exists_supportinjectivefirst_value))) /\ (((((exists ff_h_pvs_exists_supportinjectivefirst_valuenegative. ff_h_pvs_exists_supportinjectivefirst_valuenegative + S (dst_negative_exists_supportinjectivefirst_value) = S ((S (ssr_first_exists_supportinjective)) * dst_negative_scale_exists_supportinjectivefirst_value)) /\ exists ff_q_pvs_exists_supportinjectivefirst_valuenegative. dst_negative_code_exists_supportinjectivefirst_value = ff_q_pvs_exists_supportinjectivefirst_valuenegative * S ((S (ssr_first_exists_supportinjective)) * dst_negative_scale_exists_supportinjectivefirst_value) + (dst_negative_exists_supportinjectivefirst_value))) /\ (exists ge_balance_positive_exists_supportinjectivefirst_valuevalue ge_balance_negative_exists_supportinjectivefirst_valuevalue. (((((ssr_a_exists_supportinjective) = 2 * (ge_balance_positive_exists_supportinjectivefirst_valuevalue) /\ (ge_balance_negative_exists_supportinjectivefirst_valuevalue) = 0) \/ exists ge_signed_half_exists_supportinjectivefirst_valuevaluedecode. (((ssr_a_exists_supportinjective) = 2 * ge_signed_half_exists_supportinjectivefirst_valuevaluedecode + 1 /\ (ge_balance_positive_exists_supportinjectivefirst_valuevalue) = 0) /\ (ge_balance_negative_exists_supportinjectivefirst_valuevalue) = S ge_signed_half_exists_supportinjectivefirst_valuevaluedecode))) /\ ((dst_positive_exists_supportinjectivefirst_value) + ge_balance_negative_exists_supportinjectivefirst_valuevalue = (dst_negative_exists_supportinjectivefirst_value) + ge_balance_positive_exists_supportinjectivefirst_valuevalue))))))))) -> ~(ssr_a_exists_supportinjective=0) -> (exists dst_positive_code_exists_supportinjectivesecond_value dst_positive_scale_exists_supportinjectivesecond_value dst_negative_code_exists_supportinjectivesecond_value dst_negative_scale_exists_supportinjectivesecond_value dst_positive_exists_supportinjectivesecond_value dst_negative_exists_supportinjectivesecond_value. (((A) = (((((dst_positive_code_exists_supportinjectivesecond_value) + (dst_positive_scale_exists_supportinjectivesecond_value)) * S ((dst_positive_code_exists_supportinjectivesecond_value) + (dst_positive_scale_exists_supportinjectivesecond_value)) + ((dst_positive_scale_exists_supportinjectivesecond_value) + (dst_positive_scale_exists_supportinjectivesecond_value))) + (((dst_negative_code_exists_supportinjectivesecond_value) + (dst_negative_scale_exists_supportinjectivesecond_value)) * S ((dst_negative_code_exists_supportinjectivesecond_value) + (dst_negative_scale_exists_supportinjectivesecond_value)) + ((dst_negative_scale_exists_supportinjectivesecond_value) + (dst_negative_scale_exists_supportinjectivesecond_value)))) * S ((((dst_positive_code_exists_supportinjectivesecond_value) + (dst_positive_scale_exists_supportinjectivesecond_value)) * S ((dst_positive_code_exists_supportinjectivesecond_value) + (dst_positive_scale_exists_supportinjectivesecond_value)) + ((dst_positive_scale_exists_supportinjectivesecond_value) + (dst_positive_scale_exists_supportinjectivesecond_value))) + (((dst_negative_code_exists_supportinjectivesecond_value) + (dst_negative_scale_exists_supportinjectivesecond_value)) * S ((dst_negative_code_exists_supportinjectivesecond_value) + (dst_negative_scale_exists_supportinjectivesecond_value)) + ((dst_negative_scale_exists_supportinjectivesecond_value) + (dst_negative_scale_exists_supportinjectivesecond_value)))) + ((((dst_negative_code_exists_supportinjectivesecond_value) + (dst_negative_scale_exists_supportinjectivesecond_value)) * S ((dst_negative_code_exists_supportinjectivesecond_value) + (dst_negative_scale_exists_supportinjectivesecond_value)) + ((dst_negative_scale_exists_supportinjectivesecond_value) + (dst_negative_scale_exists_supportinjectivesecond_value))) + (((dst_negative_code_exists_supportinjectivesecond_value) + (dst_negative_scale_exists_supportinjectivesecond_value)) * S ((dst_negative_code_exists_supportinjectivesecond_value) + (dst_negative_scale_exists_supportinjectivesecond_value)) + ((dst_negative_scale_exists_supportinjectivesecond_value) + (dst_negative_scale_exists_supportinjectivesecond_value)))))) /\ (((((exists ff_h_pvs_exists_supportinjectivesecond_valuepositive. ff_h_pvs_exists_supportinjectivesecond_valuepositive + S (dst_positive_exists_supportinjectivesecond_value) = S ((S (ssr_second_exists_supportinjective)) * dst_positive_scale_exists_supportinjectivesecond_value)) /\ exists ff_q_pvs_exists_supportinjectivesecond_valuepositive. dst_positive_code_exists_supportinjectivesecond_value = ff_q_pvs_exists_supportinjectivesecond_valuepositive * S ((S (ssr_second_exists_supportinjective)) * dst_positive_scale_exists_supportinjectivesecond_value) + (dst_positive_exists_supportinjectivesecond_value))) /\ (((((exists ff_h_pvs_exists_supportinjectivesecond_valuenegative. ff_h_pvs_exists_supportinjectivesecond_valuenegative + S (dst_negative_exists_supportinjectivesecond_value) = S ((S (ssr_second_exists_supportinjective)) * dst_negative_scale_exists_supportinjectivesecond_value)) /\ exists ff_q_pvs_exists_supportinjectivesecond_valuenegative. dst_negative_code_exists_supportinjectivesecond_value = ff_q_pvs_exists_supportinjectivesecond_valuenegative * S ((S (ssr_second_exists_supportinjective)) * dst_negative_scale_exists_supportinjectivesecond_value) + (dst_negative_exists_supportinjectivesecond_value))) /\ (exists ge_balance_positive_exists_supportinjectivesecond_valuevalue ge_balance_negative_exists_supportinjectivesecond_valuevalue. (((((ssr_b_exists_supportinjective) = 2 * (ge_balance_positive_exists_supportinjectivesecond_valuevalue) /\ (ge_balance_negative_exists_supportinjectivesecond_valuevalue) = 0) \/ exists ge_signed_half_exists_supportinjectivesecond_valuevaluedecode. (((ssr_b_exists_supportinjective) = 2 * ge_signed_half_exists_supportinjectivesecond_valuevaluedecode + 1 /\ (ge_balance_positive_exists_supportinjectivesecond_valuevalue) = 0) /\ (ge_balance_negative_exists_supportinjectivesecond_valuevalue) = S ge_signed_half_exists_supportinjectivesecond_valuevaluedecode))) /\ ((dst_positive_exists_supportinjectivesecond_value) + ge_balance_negative_exists_supportinjectivesecond_valuevalue = (dst_negative_exists_supportinjectivesecond_value) + ge_balance_positive_exists_supportinjectivesecond_valuevalue))))))))) -> ~(ssr_b_exists_supportinjective=0) -> (((exists ff_h_pvs_exists_supportinjectivefirst_map. ff_h_pvs_exists_supportinjectivefirst_map + S (ssr_image_exists_supportinjective) = S ((S (ssr_first_exists_supportinjective)) * s)) /\ exists ff_q_pvs_exists_supportinjectivefirst_map. r = ff_q_pvs_exists_supportinjectivefirst_map * S ((S (ssr_first_exists_supportinjective)) * s) + (ssr_image_exists_supportinjective))) -> (((exists ff_h_pvs_exists_supportinjectivesecond_map. ff_h_pvs_exists_supportinjectivesecond_map + S (ssr_image_exists_supportinjective) = S ((S (ssr_second_exists_supportinjective)) * s)) /\ exists ff_q_pvs_exists_supportinjectivesecond_map. r = ff_q_pvs_exists_supportinjectivesecond_map * S ((S (ssr_second_exists_supportinjective)) * s) + (ssr_image_exists_supportinjective))) -> ssr_first_exists_supportinjective=ssr_second_exists_supportinjective) /\ (forall ssr_target_exists_supportcover ssr_value_exists_supportcover. (exists pvs_gap_exists_supportcovertarget_bound. pvs_gap_exists_supportcovertarget_bound + S (ssr_target_exists_supportcover) = (M)) -> (exists dst_positive_code_exists_supportcovertarget_value dst_positive_scale_exists_supportcovertarget_value dst_negative_code_exists_supportcovertarget_value dst_negative_scale_exists_supportcovertarget_value dst_positive_exists_supportcovertarget_value dst_negative_exists_supportcovertarget_value. (((B) = (((((dst_positive_code_exists_supportcovertarget_value) + (dst_positive_scale_exists_supportcovertarget_value)) * S ((dst_positive_code_exists_supportcovertarget_value) + (dst_positive_scale_exists_supportcovertarget_value)) + ((dst_positive_scale_exists_supportcovertarget_value) + (dst_positive_scale_exists_supportcovertarget_value))) + (((dst_negative_code_exists_supportcovertarget_value) + (dst_negative_scale_exists_supportcovertarget_value)) * S ((dst_negative_code_exists_supportcovertarget_value) + (dst_negative_scale_exists_supportcovertarget_value)) + ((dst_negative_scale_exists_supportcovertarget_value) + (dst_negative_scale_exists_supportcovertarget_value)))) * S ((((dst_positive_code_exists_supportcovertarget_value) + (dst_positive_scale_exists_supportcovertarget_value)) * S ((dst_positive_code_exists_supportcovertarget_value) + (dst_positive_scale_exists_supportcovertarget_value)) + ((dst_positive_scale_exists_supportcovertarget_value) + (dst_positive_scale_exists_supportcovertarget_value))) + (((dst_negative_code_exists_supportcovertarget_value) + (dst_negative_scale_exists_supportcovertarget_value)) * S ((dst_negative_code_exists_supportcovertarget_value) + (dst_negative_scale_exists_supportcovertarget_value)) + ((dst_negative_scale_exists_supportcovertarget_value) + (dst_negative_scale_exists_supportcovertarget_value)))) + ((((dst_negative_code_exists_supportcovertarget_value) + (dst_negative_scale_exists_supportcovertarget_value)) * S ((dst_negative_code_exists_supportcovertarget_value) + (dst_negative_scale_exists_supportcovertarget_value)) + ((dst_negative_scale_exists_supportcovertarget_value) + (dst_negative_scale_exists_supportcovertarget_value))) + (((dst_negative_code_exists_supportcovertarget_value) + (dst_negative_scale_exists_supportcovertarget_value)) * S ((dst_negative_code_exists_supportcovertarget_value) + (dst_negative_scale_exists_supportcovertarget_value)) + ((dst_negative_scale_exists_supportcovertarget_value) + (dst_negative_scale_exists_supportcovertarget_value)))))) /\ (((((exists ff_h_pvs_exists_supportcovertarget_valuepositive. ff_h_pvs_exists_supportcovertarget_valuepositive + S (dst_positive_exists_supportcovertarget_value) = S ((S (ssr_target_exists_supportcover)) * dst_positive_scale_exists_supportcovertarget_value)) /\ exists ff_q_pvs_exists_supportcovertarget_valuepositive. dst_positive_code_exists_supportcovertarget_value = ff_q_pvs_exists_supportcovertarget_valuepositive * S ((S (ssr_target_exists_supportcover)) * dst_positive_scale_exists_supportcovertarget_value) + (dst_positive_exists_supportcovertarget_value))) /\ (((((exists ff_h_pvs_exists_supportcovertarget_valuenegative. ff_h_pvs_exists_supportcovertarget_valuenegative + S (dst_negative_exists_supportcovertarget_value) = S ((S (ssr_target_exists_supportcover)) * dst_negative_scale_exists_supportcovertarget_value)) /\ exists ff_q_pvs_exists_supportcovertarget_valuenegative. dst_negative_code_exists_supportcovertarget_value = ff_q_pvs_exists_supportcovertarget_valuenegative * S ((S (ssr_target_exists_supportcover)) * dst_negative_scale_exists_supportcovertarget_value) + (dst_negative_exists_supportcovertarget_value))) /\ (exists ge_balance_positive_exists_supportcovertarget_valuevalue ge_balance_negative_exists_supportcovertarget_valuevalue. (((((ssr_value_exists_supportcover) = 2 * (ge_balance_positive_exists_supportcovertarget_valuevalue) /\ (ge_balance_negative_exists_supportcovertarget_valuevalue) = 0) \/ exists ge_signed_half_exists_supportcovertarget_valuevaluedecode. (((ssr_value_exists_supportcover) = 2 * ge_signed_half_exists_supportcovertarget_valuevaluedecode + 1 /\ (ge_balance_positive_exists_supportcovertarget_valuevalue) = 0) /\ (ge_balance_negative_exists_supportcovertarget_valuevalue) = S ge_signed_half_exists_supportcovertarget_valuevaluedecode))) /\ ((dst_positive_exists_supportcovertarget_value) + ge_balance_negative_exists_supportcovertarget_valuevalue = (dst_negative_exists_supportcovertarget_value) + ge_balance_positive_exists_supportcovertarget_valuevalue))))))))) -> ~(ssr_value_exists_supportcover=0) -> exists ssr_source_exists_supportcover. ((exists pvs_gap_exists_supportcoversource_bound. pvs_gap_exists_supportcoversource_bound + S (ssr_source_exists_supportcover) = (L)) /\ (((((exists ff_h_pvs_exists_supportcovermap. ff_h_pvs_exists_supportcovermap + S (ssr_target_exists_supportcover) = S ((S (ssr_source_exists_supportcover)) * s)) /\ exists ff_q_pvs_exists_supportcovermap. r = ff_q_pvs_exists_supportcovermap * S ((S (ssr_source_exists_supportcover)) * s) + (ssr_target_exists_supportcover))) /\ (exists dst_positive_code_exists_supportcoversource_value dst_positive_scale_exists_supportcoversource_value dst_negative_code_exists_supportcoversource_value dst_negative_scale_exists_supportcoversource_value dst_positive_exists_supportcoversource_value dst_negative_exists_supportcoversource_value. (((A) = (((((dst_positive_code_exists_supportcoversource_value) + (dst_positive_scale_exists_supportcoversource_value)) * S ((dst_positive_code_exists_supportcoversource_value) + (dst_positive_scale_exists_supportcoversource_value)) + ((dst_positive_scale_exists_supportcoversource_value) + (dst_positive_scale_exists_supportcoversource_value))) + (((dst_negative_code_exists_supportcoversource_value) + (dst_negative_scale_exists_supportcoversource_value)) * S ((dst_negative_code_exists_supportcoversource_value) + (dst_negative_scale_exists_supportcoversource_value)) + ((dst_negative_scale_exists_supportcoversource_value) + (dst_negative_scale_exists_supportcoversource_value)))) * S ((((dst_positive_code_exists_supportcoversource_value) + (dst_positive_scale_exists_supportcoversource_value)) * S ((dst_positive_code_exists_supportcoversource_value) + (dst_positive_scale_exists_supportcoversource_value)) + ((dst_positive_scale_exists_supportcoversource_value) + (dst_positive_scale_exists_supportcoversource_value))) + (((dst_negative_code_exists_supportcoversource_value) + (dst_negative_scale_exists_supportcoversource_value)) * S ((dst_negative_code_exists_supportcoversource_value) + (dst_negative_scale_exists_supportcoversource_value)) + ((dst_negative_scale_exists_supportcoversource_value) + (dst_negative_scale_exists_supportcoversource_value)))) + ((((dst_negative_code_exists_supportcoversource_value) + (dst_negative_scale_exists_supportcoversource_value)) * S ((dst_negative_code_exists_supportcoversource_value) + (dst_negative_scale_exists_supportcoversource_value)) + ((dst_negative_scale_exists_supportcoversource_value) + (dst_negative_scale_exists_supportcoversource_value))) + (((dst_negative_code_exists_supportcoversource_value) + (dst_negative_scale_exists_supportcoversource_value)) * S ((dst_negative_code_exists_supportcoversource_value) + (dst_negative_scale_exists_supportcoversource_value)) + ((dst_negative_scale_exists_supportcoversource_value) + (dst_negative_scale_exists_supportcoversource_value)))))) /\ (((((exists ff_h_pvs_exists_supportcoversource_valuepositive. ff_h_pvs_exists_supportcoversource_valuepositive + S (dst_positive_exists_supportcoversource_value) = S ((S (ssr_source_exists_supportcover)) * dst_positive_scale_exists_supportcoversource_value)) /\ exists ff_q_pvs_exists_supportcoversource_valuepositive. dst_positive_code_exists_supportcoversource_value = ff_q_pvs_exists_supportcoversource_valuepositive * S ((S (ssr_source_exists_supportcover)) * dst_positive_scale_exists_supportcoversource_value) + (dst_positive_exists_supportcoversource_value))) /\ (((((exists ff_h_pvs_exists_supportcoversource_valuenegative. ff_h_pvs_exists_supportcoversource_valuenegative + S (dst_negative_exists_supportcoversource_value) = S ((S (ssr_source_exists_supportcover)) * dst_negative_scale_exists_supportcoversource_value)) /\ exists ff_q_pvs_exists_supportcoversource_valuenegative. dst_negative_code_exists_supportcoversource_value = ff_q_pvs_exists_supportcoversource_valuenegative * S ((S (ssr_source_exists_supportcover)) * dst_negative_scale_exists_supportcoversource_value) + (dst_negative_exists_supportcoversource_value))) /\ (exists ge_balance_positive_exists_supportcoversource_valuevalue ge_balance_negative_exists_supportcoversource_valuevalue. (((((ssr_value_exists_supportcover) = 2 * (ge_balance_positive_exists_supportcoversource_valuevalue) /\ (ge_balance_negative_exists_supportcoversource_valuevalue) = 0) \/ exists ge_signed_half_exists_supportcoversource_valuevaluedecode. (((ssr_value_exists_supportcover) = 2 * ge_signed_half_exists_supportcoversource_valuevaluedecode + 1 /\ (ge_balance_positive_exists_supportcoversource_valuevalue) = 0) /\ (ge_balance_negative_exists_supportcoversource_valuevalue) = S ge_signed_half_exists_supportcoversource_valuevaluedecode))) /\ ((dst_positive_exists_supportcoversource_value) + ge_balance_negative_exists_supportcoversource_valuevalue = (dst_negative_exists_supportcoversource_value) + ge_balance_positive_exists_supportcoversource_valuevalue))))))))))))))))))))) -> exists z. ((exists dst_positive_code_exists_source_sum dst_positive_scale_exists_source_sum dst_negative_code_exists_source_sum dst_negative_scale_exists_source_sum dst_positive_sum_exists_source_sum dst_negative_sum_exists_source_sum. (((A) = (((((dst_positive_code_exists_source_sum) + (dst_positive_scale_exists_source_sum)) * S ((dst_positive_code_exists_source_sum) + (dst_positive_scale_exists_source_sum)) + ((dst_positive_scale_exists_source_sum) + (dst_positive_scale_exists_source_sum))) + (((dst_negative_code_exists_source_sum) + (dst_negative_scale_exists_source_sum)) * S ((dst_negative_code_exists_source_sum) + (dst_negative_scale_exists_source_sum)) + ((dst_negative_scale_exists_source_sum) + (dst_negative_scale_exists_source_sum)))) * S ((((dst_positive_code_exists_source_sum) + (dst_positive_scale_exists_source_sum)) * S ((dst_positive_code_exists_source_sum) + (dst_positive_scale_exists_source_sum)) + ((dst_positive_scale_exists_source_sum) + (dst_positive_scale_exists_source_sum))) + (((dst_negative_code_exists_source_sum) + (dst_negative_scale_exists_source_sum)) * S ((dst_negative_code_exists_source_sum) + (dst_negative_scale_exists_source_sum)) + ((dst_negative_scale_exists_source_sum) + (dst_negative_scale_exists_source_sum)))) + ((((dst_negative_code_exists_source_sum) + (dst_negative_scale_exists_source_sum)) * S ((dst_negative_code_exists_source_sum) + (dst_negative_scale_exists_source_sum)) + ((dst_negative_scale_exists_source_sum) + (dst_negative_scale_exists_source_sum))) + (((dst_negative_code_exists_source_sum) + (dst_negative_scale_exists_source_sum)) * S ((dst_negative_code_exists_source_sum) + (dst_negative_scale_exists_source_sum)) + ((dst_negative_scale_exists_source_sum) + (dst_negative_scale_exists_source_sum)))))) /\ (((exists fs_u_dst_exists_source_sumpositive fs_v_dst_exists_source_sumpositive. ((((exists fs_h_dst_exists_source_sumpositive_body_start. fs_h_dst_exists_source_sumpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_exists_source_sumpositive)) /\ exists fs_q_dst_exists_source_sumpositive_body_start. fs_u_dst_exists_source_sumpositive = fs_q_dst_exists_source_sumpositive_body_start * S ((S (0)) * fs_v_dst_exists_source_sumpositive) + (0))) /\ ((((exists fs_h_dst_exists_source_sumpositive_body_terminal. fs_h_dst_exists_source_sumpositive_body_terminal + S (dst_positive_sum_exists_source_sum) = S ((S (L)) * fs_v_dst_exists_source_sumpositive)) /\ exists fs_q_dst_exists_source_sumpositive_body_terminal. fs_u_dst_exists_source_sumpositive = fs_q_dst_exists_source_sumpositive_body_terminal * S ((S (L)) * fs_v_dst_exists_source_sumpositive) + (dst_positive_sum_exists_source_sum))) /\ forall fs_i_dst_exists_source_sumpositive_body_steps. (exists fs_lt_dst_exists_source_sumpositive_body_steps_bound. fs_lt_dst_exists_source_sumpositive_body_steps_bound + S fs_i_dst_exists_source_sumpositive_body_steps = L) -> exists fs_a_dst_exists_source_sumpositive_body_steps fs_r_dst_exists_source_sumpositive_body_steps fs_s_dst_exists_source_sumpositive_body_steps. ((((exists fs_h_dst_exists_source_sumpositive_body_steps_summand. fs_h_dst_exists_source_sumpositive_body_steps_summand + S (fs_a_dst_exists_source_sumpositive_body_steps) = S ((S (fs_i_dst_exists_source_sumpositive_body_steps)) * dst_positive_scale_exists_source_sum)) /\ exists fs_q_dst_exists_source_sumpositive_body_steps_summand. dst_positive_code_exists_source_sum = fs_q_dst_exists_source_sumpositive_body_steps_summand * S ((S (fs_i_dst_exists_source_sumpositive_body_steps)) * dst_positive_scale_exists_source_sum) + (fs_a_dst_exists_source_sumpositive_body_steps))) /\ ((((exists fs_h_dst_exists_source_sumpositive_body_steps_partial. fs_h_dst_exists_source_sumpositive_body_steps_partial + S (fs_r_dst_exists_source_sumpositive_body_steps) = S ((S (fs_i_dst_exists_source_sumpositive_body_steps)) * fs_v_dst_exists_source_sumpositive)) /\ exists fs_q_dst_exists_source_sumpositive_body_steps_partial. fs_u_dst_exists_source_sumpositive = fs_q_dst_exists_source_sumpositive_body_steps_partial * S ((S (fs_i_dst_exists_source_sumpositive_body_steps)) * fs_v_dst_exists_source_sumpositive) + (fs_r_dst_exists_source_sumpositive_body_steps))) /\ ((((exists fs_h_dst_exists_source_sumpositive_body_steps_successor. fs_h_dst_exists_source_sumpositive_body_steps_successor + S (fs_s_dst_exists_source_sumpositive_body_steps) = S ((S (S fs_i_dst_exists_source_sumpositive_body_steps)) * fs_v_dst_exists_source_sumpositive)) /\ exists fs_q_dst_exists_source_sumpositive_body_steps_successor. fs_u_dst_exists_source_sumpositive = fs_q_dst_exists_source_sumpositive_body_steps_successor * S ((S (S fs_i_dst_exists_source_sumpositive_body_steps)) * fs_v_dst_exists_source_sumpositive) + (fs_s_dst_exists_source_sumpositive_body_steps))) /\ fs_s_dst_exists_source_sumpositive_body_steps = fs_r_dst_exists_source_sumpositive_body_steps + fs_a_dst_exists_source_sumpositive_body_steps)))))) /\ (((exists fs_u_dst_exists_source_sumnegative fs_v_dst_exists_source_sumnegative. ((((exists fs_h_dst_exists_source_sumnegative_body_start. fs_h_dst_exists_source_sumnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_exists_source_sumnegative)) /\ exists fs_q_dst_exists_source_sumnegative_body_start. fs_u_dst_exists_source_sumnegative = fs_q_dst_exists_source_sumnegative_body_start * S ((S (0)) * fs_v_dst_exists_source_sumnegative) + (0))) /\ ((((exists fs_h_dst_exists_source_sumnegative_body_terminal. fs_h_dst_exists_source_sumnegative_body_terminal + S (dst_negative_sum_exists_source_sum) = S ((S (L)) * fs_v_dst_exists_source_sumnegative)) /\ exists fs_q_dst_exists_source_sumnegative_body_terminal. fs_u_dst_exists_source_sumnegative = fs_q_dst_exists_source_sumnegative_body_terminal * S ((S (L)) * fs_v_dst_exists_source_sumnegative) + (dst_negative_sum_exists_source_sum))) /\ forall fs_i_dst_exists_source_sumnegative_body_steps. (exists fs_lt_dst_exists_source_sumnegative_body_steps_bound. fs_lt_dst_exists_source_sumnegative_body_steps_bound + S fs_i_dst_exists_source_sumnegative_body_steps = L) -> exists fs_a_dst_exists_source_sumnegative_body_steps fs_r_dst_exists_source_sumnegative_body_steps fs_s_dst_exists_source_sumnegative_body_steps. ((((exists fs_h_dst_exists_source_sumnegative_body_steps_summand. fs_h_dst_exists_source_sumnegative_body_steps_summand + S (fs_a_dst_exists_source_sumnegative_body_steps) = S ((S (fs_i_dst_exists_source_sumnegative_body_steps)) * dst_negative_scale_exists_source_sum)) /\ exists fs_q_dst_exists_source_sumnegative_body_steps_summand. dst_negative_code_exists_source_sum = fs_q_dst_exists_source_sumnegative_body_steps_summand * S ((S (fs_i_dst_exists_source_sumnegative_body_steps)) * dst_negative_scale_exists_source_sum) + (fs_a_dst_exists_source_sumnegative_body_steps))) /\ ((((exists fs_h_dst_exists_source_sumnegative_body_steps_partial. fs_h_dst_exists_source_sumnegative_body_steps_partial + S (fs_r_dst_exists_source_sumnegative_body_steps) = S ((S (fs_i_dst_exists_source_sumnegative_body_steps)) * fs_v_dst_exists_source_sumnegative)) /\ exists fs_q_dst_exists_source_sumnegative_body_steps_partial. fs_u_dst_exists_source_sumnegative = fs_q_dst_exists_source_sumnegative_body_steps_partial * S ((S (fs_i_dst_exists_source_sumnegative_body_steps)) * fs_v_dst_exists_source_sumnegative) + (fs_r_dst_exists_source_sumnegative_body_steps))) /\ ((((exists fs_h_dst_exists_source_sumnegative_body_steps_successor. fs_h_dst_exists_source_sumnegative_body_steps_successor + S (fs_s_dst_exists_source_sumnegative_body_steps) = S ((S (S fs_i_dst_exists_source_sumnegative_body_steps)) * fs_v_dst_exists_source_sumnegative)) /\ exists fs_q_dst_exists_source_sumnegative_body_steps_successor. fs_u_dst_exists_source_sumnegative = fs_q_dst_exists_source_sumnegative_body_steps_successor * S ((S (S fs_i_dst_exists_source_sumnegative_body_steps)) * fs_v_dst_exists_source_sumnegative) + (fs_s_dst_exists_source_sumnegative_body_steps))) /\ fs_s_dst_exists_source_sumnegative_body_steps = fs_r_dst_exists_source_sumnegative_body_steps + fs_a_dst_exists_source_sumnegative_body_steps)))))) /\ (exists ge_balance_positive_exists_source_sumresult ge_balance_negative_exists_source_sumresult. (((((z) = 2 * (ge_balance_positive_exists_source_sumresult) /\ (ge_balance_negative_exists_source_sumresult) = 0) \/ exists ge_signed_half_exists_source_sumresultdecode. (((z) = 2 * ge_signed_half_exists_source_sumresultdecode + 1 /\ (ge_balance_positive_exists_source_sumresult) = 0) /\ (ge_balance_negative_exists_source_sumresult) = S ge_signed_half_exists_source_sumresultdecode))) /\ ((dst_positive_sum_exists_source_sum) + ge_balance_negative_exists_source_sumresult = (dst_negative_sum_exists_source_sum) + ge_balance_positive_exists_source_sumresult))))))))) /\ (exists dst_positive_code_exists_target_sum dst_positive_scale_exists_target_sum dst_negative_code_exists_target_sum dst_negative_scale_exists_target_sum dst_positive_sum_exists_target_sum dst_negative_sum_exists_target_sum. (((B) = (((((dst_positive_code_exists_target_sum) + (dst_positive_scale_exists_target_sum)) * S ((dst_positive_code_exists_target_sum) + (dst_positive_scale_exists_target_sum)) + ((dst_positive_scale_exists_target_sum) + (dst_positive_scale_exists_target_sum))) + (((dst_negative_code_exists_target_sum) + (dst_negative_scale_exists_target_sum)) * S ((dst_negative_code_exists_target_sum) + (dst_negative_scale_exists_target_sum)) + ((dst_negative_scale_exists_target_sum) + (dst_negative_scale_exists_target_sum)))) * S ((((dst_positive_code_exists_target_sum) + (dst_positive_scale_exists_target_sum)) * S ((dst_positive_code_exists_target_sum) + (dst_positive_scale_exists_target_sum)) + ((dst_positive_scale_exists_target_sum) + (dst_positive_scale_exists_target_sum))) + (((dst_negative_code_exists_target_sum) + (dst_negative_scale_exists_target_sum)) * S ((dst_negative_code_exists_target_sum) + (dst_negative_scale_exists_target_sum)) + ((dst_negative_scale_exists_target_sum) + (dst_negative_scale_exists_target_sum)))) + ((((dst_negative_code_exists_target_sum) + (dst_negative_scale_exists_target_sum)) * S ((dst_negative_code_exists_target_sum) + (dst_negative_scale_exists_target_sum)) + ((dst_negative_scale_exists_target_sum) + (dst_negative_scale_exists_target_sum))) + (((dst_negative_code_exists_target_sum) + (dst_negative_scale_exists_target_sum)) * S ((dst_negative_code_exists_target_sum) + (dst_negative_scale_exists_target_sum)) + ((dst_negative_scale_exists_target_sum) + (dst_negative_scale_exists_target_sum)))))) /\ (((exists fs_u_dst_exists_target_sumpositive fs_v_dst_exists_target_sumpositive. ((((exists fs_h_dst_exists_target_sumpositive_body_start. fs_h_dst_exists_target_sumpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_exists_target_sumpositive)) /\ exists fs_q_dst_exists_target_sumpositive_body_start. fs_u_dst_exists_target_sumpositive = fs_q_dst_exists_target_sumpositive_body_start * S ((S (0)) * fs_v_dst_exists_target_sumpositive) + (0))) /\ ((((exists fs_h_dst_exists_target_sumpositive_body_terminal. fs_h_dst_exists_target_sumpositive_body_terminal + S (dst_positive_sum_exists_target_sum) = S ((S (M)) * fs_v_dst_exists_target_sumpositive)) /\ exists fs_q_dst_exists_target_sumpositive_body_terminal. fs_u_dst_exists_target_sumpositive = fs_q_dst_exists_target_sumpositive_body_terminal * S ((S (M)) * fs_v_dst_exists_target_sumpositive) + (dst_positive_sum_exists_target_sum))) /\ forall fs_i_dst_exists_target_sumpositive_body_steps. (exists fs_lt_dst_exists_target_sumpositive_body_steps_bound. fs_lt_dst_exists_target_sumpositive_body_steps_bound + S fs_i_dst_exists_target_sumpositive_body_steps = M) -> exists fs_a_dst_exists_target_sumpositive_body_steps fs_r_dst_exists_target_sumpositive_body_steps fs_s_dst_exists_target_sumpositive_body_steps. ((((exists fs_h_dst_exists_target_sumpositive_body_steps_summand. fs_h_dst_exists_target_sumpositive_body_steps_summand + S (fs_a_dst_exists_target_sumpositive_body_steps) = S ((S (fs_i_dst_exists_target_sumpositive_body_steps)) * dst_positive_scale_exists_target_sum)) /\ exists fs_q_dst_exists_target_sumpositive_body_steps_summand. dst_positive_code_exists_target_sum = fs_q_dst_exists_target_sumpositive_body_steps_summand * S ((S (fs_i_dst_exists_target_sumpositive_body_steps)) * dst_positive_scale_exists_target_sum) + (fs_a_dst_exists_target_sumpositive_body_steps))) /\ ((((exists fs_h_dst_exists_target_sumpositive_body_steps_partial. fs_h_dst_exists_target_sumpositive_body_steps_partial + S (fs_r_dst_exists_target_sumpositive_body_steps) = S ((S (fs_i_dst_exists_target_sumpositive_body_steps)) * fs_v_dst_exists_target_sumpositive)) /\ exists fs_q_dst_exists_target_sumpositive_body_steps_partial. fs_u_dst_exists_target_sumpositive = fs_q_dst_exists_target_sumpositive_body_steps_partial * S ((S (fs_i_dst_exists_target_sumpositive_body_steps)) * fs_v_dst_exists_target_sumpositive) + (fs_r_dst_exists_target_sumpositive_body_steps))) /\ ((((exists fs_h_dst_exists_target_sumpositive_body_steps_successor. fs_h_dst_exists_target_sumpositive_body_steps_successor + S (fs_s_dst_exists_target_sumpositive_body_steps) = S ((S (S fs_i_dst_exists_target_sumpositive_body_steps)) * fs_v_dst_exists_target_sumpositive)) /\ exists fs_q_dst_exists_target_sumpositive_body_steps_successor. fs_u_dst_exists_target_sumpositive = fs_q_dst_exists_target_sumpositive_body_steps_successor * S ((S (S fs_i_dst_exists_target_sumpositive_body_steps)) * fs_v_dst_exists_target_sumpositive) + (fs_s_dst_exists_target_sumpositive_body_steps))) /\ fs_s_dst_exists_target_sumpositive_body_steps = fs_r_dst_exists_target_sumpositive_body_steps + fs_a_dst_exists_target_sumpositive_body_steps)))))) /\ (((exists fs_u_dst_exists_target_sumnegative fs_v_dst_exists_target_sumnegative. ((((exists fs_h_dst_exists_target_sumnegative_body_start. fs_h_dst_exists_target_sumnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_exists_target_sumnegative)) /\ exists fs_q_dst_exists_target_sumnegative_body_start. fs_u_dst_exists_target_sumnegative = fs_q_dst_exists_target_sumnegative_body_start * S ((S (0)) * fs_v_dst_exists_target_sumnegative) + (0))) /\ ((((exists fs_h_dst_exists_target_sumnegative_body_terminal. fs_h_dst_exists_target_sumnegative_body_terminal + S (dst_negative_sum_exists_target_sum) = S ((S (M)) * fs_v_dst_exists_target_sumnegative)) /\ exists fs_q_dst_exists_target_sumnegative_body_terminal. fs_u_dst_exists_target_sumnegative = fs_q_dst_exists_target_sumnegative_body_terminal * S ((S (M)) * fs_v_dst_exists_target_sumnegative) + (dst_negative_sum_exists_target_sum))) /\ forall fs_i_dst_exists_target_sumnegative_body_steps. (exists fs_lt_dst_exists_target_sumnegative_body_steps_bound. fs_lt_dst_exists_target_sumnegative_body_steps_bound + S fs_i_dst_exists_target_sumnegative_body_steps = M) -> exists fs_a_dst_exists_target_sumnegative_body_steps fs_r_dst_exists_target_sumnegative_body_steps fs_s_dst_exists_target_sumnegative_body_steps. ((((exists fs_h_dst_exists_target_sumnegative_body_steps_summand. fs_h_dst_exists_target_sumnegative_body_steps_summand + S (fs_a_dst_exists_target_sumnegative_body_steps) = S ((S (fs_i_dst_exists_target_sumnegative_body_steps)) * dst_negative_scale_exists_target_sum)) /\ exists fs_q_dst_exists_target_sumnegative_body_steps_summand. dst_negative_code_exists_target_sum = fs_q_dst_exists_target_sumnegative_body_steps_summand * S ((S (fs_i_dst_exists_target_sumnegative_body_steps)) * dst_negative_scale_exists_target_sum) + (fs_a_dst_exists_target_sumnegative_body_steps))) /\ ((((exists fs_h_dst_exists_target_sumnegative_body_steps_partial. fs_h_dst_exists_target_sumnegative_body_steps_partial + S (fs_r_dst_exists_target_sumnegative_body_steps) = S ((S (fs_i_dst_exists_target_sumnegative_body_steps)) * fs_v_dst_exists_target_sumnegative)) /\ exists fs_q_dst_exists_target_sumnegative_body_steps_partial. fs_u_dst_exists_target_sumnegative = fs_q_dst_exists_target_sumnegative_body_steps_partial * S ((S (fs_i_dst_exists_target_sumnegative_body_steps)) * fs_v_dst_exists_target_sumnegative) + (fs_r_dst_exists_target_sumnegative_body_steps))) /\ ((((exists fs_h_dst_exists_target_sumnegative_body_steps_successor. fs_h_dst_exists_target_sumnegative_body_steps_successor + S (fs_s_dst_exists_target_sumnegative_body_steps) = S ((S (S fs_i_dst_exists_target_sumnegative_body_steps)) * fs_v_dst_exists_target_sumnegative)) /\ exists fs_q_dst_exists_target_sumnegative_body_steps_successor. fs_u_dst_exists_target_sumnegative = fs_q_dst_exists_target_sumnegative_body_steps_successor * S ((S (S fs_i_dst_exists_target_sumnegative_body_steps)) * fs_v_dst_exists_target_sumnegative) + (fs_s_dst_exists_target_sumnegative_body_steps))) /\ fs_s_dst_exists_target_sumnegative_body_steps = fs_r_dst_exists_target_sumnegative_body_steps + fs_a_dst_exists_target_sumnegative_body_steps)))))) /\ (exists ge_balance_positive_exists_target_sumresult ge_balance_negative_exists_target_sumresult. (((((z) = 2 * (ge_balance_positive_exists_target_sumresult) /\ (ge_balance_negative_exists_target_sumresult) = 0) \/ exists ge_signed_half_exists_target_sumresultdecode. (((z) = 2 * ge_signed_half_exists_target_sumresultdecode + 1 /\ (ge_balance_positive_exists_target_sumresult) = 0) /\ (ge_balance_negative_exists_target_sumresult) = S ge_signed_half_exists_target_sumresultdecode))) /\ ((dst_positive_sum_exists_target_sum) + ge_balance_negative_exists_target_sumresult = (dst_negative_sum_exists_target_sum) + ge_balance_positive_exists_target_sumresult))))))))))