signed_support_incidence_column_sum_value

Exact expanded first-order arithmetic statement

forall A B r s L M T j b z. (((exists dst_positive_code_column_value_supportsource_table dst_positive_scale_column_value_supportsource_table dst_negative_code_column_value_supportsource_table dst_negative_scale_column_value_supportsource_table. (((A) = (((((dst_positive_code_column_value_supportsource_table) + (dst_positive_scale_column_value_supportsource_table)) * S ((dst_positive_code_column_value_supportsource_table) + (dst_positive_scale_column_value_supportsource_table)) + ((dst_positive_scale_column_value_supportsource_table) + (dst_positive_scale_column_value_supportsource_table))) + (((dst_negative_code_column_value_supportsource_table) + (dst_negative_scale_column_value_supportsource_table)) * S ((dst_negative_code_column_value_supportsource_table) + (dst_negative_scale_column_value_supportsource_table)) + ((dst_negative_scale_column_value_supportsource_table) + (dst_negative_scale_column_value_supportsource_table)))) * S ((((dst_positive_code_column_value_supportsource_table) + (dst_positive_scale_column_value_supportsource_table)) * S ((dst_positive_code_column_value_supportsource_table) + (dst_positive_scale_column_value_supportsource_table)) + ((dst_positive_scale_column_value_supportsource_table) + (dst_positive_scale_column_value_supportsource_table))) + (((dst_negative_code_column_value_supportsource_table) + (dst_negative_scale_column_value_supportsource_table)) * S ((dst_negative_code_column_value_supportsource_table) + (dst_negative_scale_column_value_supportsource_table)) + ((dst_negative_scale_column_value_supportsource_table) + (dst_negative_scale_column_value_supportsource_table)))) + ((((dst_negative_code_column_value_supportsource_table) + (dst_negative_scale_column_value_supportsource_table)) * S ((dst_negative_code_column_value_supportsource_table) + (dst_negative_scale_column_value_supportsource_table)) + ((dst_negative_scale_column_value_supportsource_table) + (dst_negative_scale_column_value_supportsource_table))) + (((dst_negative_code_column_value_supportsource_table) + (dst_negative_scale_column_value_supportsource_table)) * S ((dst_negative_code_column_value_supportsource_table) + (dst_negative_scale_column_value_supportsource_table)) + ((dst_negative_scale_column_value_supportsource_table) + (dst_negative_scale_column_value_supportsource_table)))))) /\ (forall dst_index_column_value_supportsource_table. (exists pvs_le_gap_column_value_supportsource_tabledomain. pvs_le_gap_column_value_supportsource_tabledomain + (dst_index_column_value_supportsource_table) = (0)) -> exists dst_positive_column_value_supportsource_table dst_negative_column_value_supportsource_table dst_value_column_value_supportsource_table. ((((exists ff_h_pvs_column_value_supportsource_tableentrypositive. ff_h_pvs_column_value_supportsource_tableentrypositive + S (dst_positive_column_value_supportsource_table) = S ((S (dst_index_column_value_supportsource_table)) * dst_positive_scale_column_value_supportsource_table)) /\ exists ff_q_pvs_column_value_supportsource_tableentrypositive. dst_positive_code_column_value_supportsource_table = ff_q_pvs_column_value_supportsource_tableentrypositive * S ((S (dst_index_column_value_supportsource_table)) * dst_positive_scale_column_value_supportsource_table) + (dst_positive_column_value_supportsource_table))) /\ (((((exists ff_h_pvs_column_value_supportsource_tableentrynegative. ff_h_pvs_column_value_supportsource_tableentrynegative + S (dst_negative_column_value_supportsource_table) = S ((S (dst_index_column_value_supportsource_table)) * dst_negative_scale_column_value_supportsource_table)) /\ exists ff_q_pvs_column_value_supportsource_tableentrynegative. dst_negative_code_column_value_supportsource_table = ff_q_pvs_column_value_supportsource_tableentrynegative * S ((S (dst_index_column_value_supportsource_table)) * dst_negative_scale_column_value_supportsource_table) + (dst_negative_column_value_supportsource_table))) /\ (exists ge_balance_positive_column_value_supportsource_tableentryvalue ge_balance_negative_column_value_supportsource_tableentryvalue. (((((dst_value_column_value_supportsource_table) = 2 * (ge_balance_positive_column_value_supportsource_tableentryvalue) /\ (ge_balance_negative_column_value_supportsource_tableentryvalue) = 0) \/ exists ge_signed_half_column_value_supportsource_tableentryvaluedecode. (((dst_value_column_value_supportsource_table) = 2 * ge_signed_half_column_value_supportsource_tableentryvaluedecode + 1 /\ (ge_balance_positive_column_value_supportsource_tableentryvalue) = 0) /\ (ge_balance_negative_column_value_supportsource_tableentryvalue) = S ge_signed_half_column_value_supportsource_tableentryvaluedecode))) /\ ((dst_positive_column_value_supportsource_table) + ge_balance_negative_column_value_supportsource_tableentryvalue = (dst_negative_column_value_supportsource_table) + ge_balance_positive_column_value_supportsource_tableentryvalue))))))))) /\ (((exists dst_positive_code_column_value_supporttarget_table dst_positive_scale_column_value_supporttarget_table dst_negative_code_column_value_supporttarget_table dst_negative_scale_column_value_supporttarget_table. (((B) = (((((dst_positive_code_column_value_supporttarget_table) + (dst_positive_scale_column_value_supporttarget_table)) * S ((dst_positive_code_column_value_supporttarget_table) + (dst_positive_scale_column_value_supporttarget_table)) + ((dst_positive_scale_column_value_supporttarget_table) + (dst_positive_scale_column_value_supporttarget_table))) + (((dst_negative_code_column_value_supporttarget_table) + (dst_negative_scale_column_value_supporttarget_table)) * S ((dst_negative_code_column_value_supporttarget_table) + (dst_negative_scale_column_value_supporttarget_table)) + ((dst_negative_scale_column_value_supporttarget_table) + (dst_negative_scale_column_value_supporttarget_table)))) * S ((((dst_positive_code_column_value_supporttarget_table) + (dst_positive_scale_column_value_supporttarget_table)) * S ((dst_positive_code_column_value_supporttarget_table) + (dst_positive_scale_column_value_supporttarget_table)) + ((dst_positive_scale_column_value_supporttarget_table) + (dst_positive_scale_column_value_supporttarget_table))) + (((dst_negative_code_column_value_supporttarget_table) + (dst_negative_scale_column_value_supporttarget_table)) * S ((dst_negative_code_column_value_supporttarget_table) + (dst_negative_scale_column_value_supporttarget_table)) + ((dst_negative_scale_column_value_supporttarget_table) + (dst_negative_scale_column_value_supporttarget_table)))) + ((((dst_negative_code_column_value_supporttarget_table) + (dst_negative_scale_column_value_supporttarget_table)) * S ((dst_negative_code_column_value_supporttarget_table) + (dst_negative_scale_column_value_supporttarget_table)) + ((dst_negative_scale_column_value_supporttarget_table) + (dst_negative_scale_column_value_supporttarget_table))) + (((dst_negative_code_column_value_supporttarget_table) + (dst_negative_scale_column_value_supporttarget_table)) * S ((dst_negative_code_column_value_supporttarget_table) + (dst_negative_scale_column_value_supporttarget_table)) + ((dst_negative_scale_column_value_supporttarget_table) + (dst_negative_scale_column_value_supporttarget_table)))))) /\ (forall dst_index_column_value_supporttarget_table. (exists pvs_le_gap_column_value_supporttarget_tabledomain. pvs_le_gap_column_value_supporttarget_tabledomain + (dst_index_column_value_supporttarget_table) = (0)) -> exists dst_positive_column_value_supporttarget_table dst_negative_column_value_supporttarget_table dst_value_column_value_supporttarget_table. ((((exists ff_h_pvs_column_value_supporttarget_tableentrypositive. ff_h_pvs_column_value_supporttarget_tableentrypositive + S (dst_positive_column_value_supporttarget_table) = S ((S (dst_index_column_value_supporttarget_table)) * dst_positive_scale_column_value_supporttarget_table)) /\ exists ff_q_pvs_column_value_supporttarget_tableentrypositive. dst_positive_code_column_value_supporttarget_table = ff_q_pvs_column_value_supporttarget_tableentrypositive * S ((S (dst_index_column_value_supporttarget_table)) * dst_positive_scale_column_value_supporttarget_table) + (dst_positive_column_value_supporttarget_table))) /\ (((((exists ff_h_pvs_column_value_supporttarget_tableentrynegative. ff_h_pvs_column_value_supporttarget_tableentrynegative + S (dst_negative_column_value_supporttarget_table) = S ((S (dst_index_column_value_supporttarget_table)) * dst_negative_scale_column_value_supporttarget_table)) /\ exists ff_q_pvs_column_value_supporttarget_tableentrynegative. dst_negative_code_column_value_supporttarget_table = ff_q_pvs_column_value_supporttarget_tableentrynegative * S ((S (dst_index_column_value_supporttarget_table)) * dst_negative_scale_column_value_supporttarget_table) + (dst_negative_column_value_supporttarget_table))) /\ (exists ge_balance_positive_column_value_supporttarget_tableentryvalue ge_balance_negative_column_value_supporttarget_tableentryvalue. (((((dst_value_column_value_supporttarget_table) = 2 * (ge_balance_positive_column_value_supporttarget_tableentryvalue) /\ (ge_balance_negative_column_value_supporttarget_tableentryvalue) = 0) \/ exists ge_signed_half_column_value_supporttarget_tableentryvaluedecode. (((dst_value_column_value_supporttarget_table) = 2 * ge_signed_half_column_value_supporttarget_tableentryvaluedecode + 1 /\ (ge_balance_positive_column_value_supporttarget_tableentryvalue) = 0) /\ (ge_balance_negative_column_value_supporttarget_tableentryvalue) = S ge_signed_half_column_value_supporttarget_tableentryvaluedecode))) /\ ((dst_positive_column_value_supporttarget_table) + ge_balance_negative_column_value_supporttarget_tableentryvalue = (dst_negative_column_value_supporttarget_table) + ge_balance_positive_column_value_supporttarget_tableentryvalue))))))))) /\ (((forall ssr_source_column_value_supportpreserve ssr_value_column_value_supportpreserve. (exists pvs_gap_column_value_supportpreservesource_bound. pvs_gap_column_value_supportpreservesource_bound + S (ssr_source_column_value_supportpreserve) = (L)) -> (exists dst_positive_code_column_value_supportpreservesource_value dst_positive_scale_column_value_supportpreservesource_value dst_negative_code_column_value_supportpreservesource_value dst_negative_scale_column_value_supportpreservesource_value dst_positive_column_value_supportpreservesource_value dst_negative_column_value_supportpreservesource_value. (((A) = (((((dst_positive_code_column_value_supportpreservesource_value) + (dst_positive_scale_column_value_supportpreservesource_value)) * S ((dst_positive_code_column_value_supportpreservesource_value) + (dst_positive_scale_column_value_supportpreservesource_value)) + ((dst_positive_scale_column_value_supportpreservesource_value) + (dst_positive_scale_column_value_supportpreservesource_value))) + (((dst_negative_code_column_value_supportpreservesource_value) + (dst_negative_scale_column_value_supportpreservesource_value)) * S ((dst_negative_code_column_value_supportpreservesource_value) + (dst_negative_scale_column_value_supportpreservesource_value)) + ((dst_negative_scale_column_value_supportpreservesource_value) + (dst_negative_scale_column_value_supportpreservesource_value)))) * S ((((dst_positive_code_column_value_supportpreservesource_value) + (dst_positive_scale_column_value_supportpreservesource_value)) * S ((dst_positive_code_column_value_supportpreservesource_value) + (dst_positive_scale_column_value_supportpreservesource_value)) + ((dst_positive_scale_column_value_supportpreservesource_value) + (dst_positive_scale_column_value_supportpreservesource_value))) + (((dst_negative_code_column_value_supportpreservesource_value) + (dst_negative_scale_column_value_supportpreservesource_value)) * S ((dst_negative_code_column_value_supportpreservesource_value) + (dst_negative_scale_column_value_supportpreservesource_value)) + ((dst_negative_scale_column_value_supportpreservesource_value) + (dst_negative_scale_column_value_supportpreservesource_value)))) + ((((dst_negative_code_column_value_supportpreservesource_value) + (dst_negative_scale_column_value_supportpreservesource_value)) * S ((dst_negative_code_column_value_supportpreservesource_value) + (dst_negative_scale_column_value_supportpreservesource_value)) + ((dst_negative_scale_column_value_supportpreservesource_value) + (dst_negative_scale_column_value_supportpreservesource_value))) + (((dst_negative_code_column_value_supportpreservesource_value) + (dst_negative_scale_column_value_supportpreservesource_value)) * S ((dst_negative_code_column_value_supportpreservesource_value) + (dst_negative_scale_column_value_supportpreservesource_value)) + ((dst_negative_scale_column_value_supportpreservesource_value) + (dst_negative_scale_column_value_supportpreservesource_value)))))) /\ (((((exists ff_h_pvs_column_value_supportpreservesource_valuepositive. ff_h_pvs_column_value_supportpreservesource_valuepositive + S (dst_positive_column_value_supportpreservesource_value) = S ((S (ssr_source_column_value_supportpreserve)) * dst_positive_scale_column_value_supportpreservesource_value)) /\ exists ff_q_pvs_column_value_supportpreservesource_valuepositive. dst_positive_code_column_value_supportpreservesource_value = ff_q_pvs_column_value_supportpreservesource_valuepositive * S ((S (ssr_source_column_value_supportpreserve)) * dst_positive_scale_column_value_supportpreservesource_value) + (dst_positive_column_value_supportpreservesource_value))) /\ (((((exists ff_h_pvs_column_value_supportpreservesource_valuenegative. ff_h_pvs_column_value_supportpreservesource_valuenegative + S (dst_negative_column_value_supportpreservesource_value) = S ((S (ssr_source_column_value_supportpreserve)) * dst_negative_scale_column_value_supportpreservesource_value)) /\ exists ff_q_pvs_column_value_supportpreservesource_valuenegative. dst_negative_code_column_value_supportpreservesource_value = ff_q_pvs_column_value_supportpreservesource_valuenegative * S ((S (ssr_source_column_value_supportpreserve)) * dst_negative_scale_column_value_supportpreservesource_value) + (dst_negative_column_value_supportpreservesource_value))) /\ (exists ge_balance_positive_column_value_supportpreservesource_valuevalue ge_balance_negative_column_value_supportpreservesource_valuevalue. (((((ssr_value_column_value_supportpreserve) = 2 * (ge_balance_positive_column_value_supportpreservesource_valuevalue) /\ (ge_balance_negative_column_value_supportpreservesource_valuevalue) = 0) \/ exists ge_signed_half_column_value_supportpreservesource_valuevaluedecode. (((ssr_value_column_value_supportpreserve) = 2 * ge_signed_half_column_value_supportpreservesource_valuevaluedecode + 1 /\ (ge_balance_positive_column_value_supportpreservesource_valuevalue) = 0) /\ (ge_balance_negative_column_value_supportpreservesource_valuevalue) = S ge_signed_half_column_value_supportpreservesource_valuevaluedecode))) /\ ((dst_positive_column_value_supportpreservesource_value) + ge_balance_negative_column_value_supportpreservesource_valuevalue = (dst_negative_column_value_supportpreservesource_value) + ge_balance_positive_column_value_supportpreservesource_valuevalue))))))))) -> ~(ssr_value_column_value_supportpreserve=0) -> exists ssr_target_column_value_supportpreserve. ((((exists ff_h_pvs_column_value_supportpreservemap. ff_h_pvs_column_value_supportpreservemap + S (ssr_target_column_value_supportpreserve) = S ((S (ssr_source_column_value_supportpreserve)) * s)) /\ exists ff_q_pvs_column_value_supportpreservemap. r = ff_q_pvs_column_value_supportpreservemap * S ((S (ssr_source_column_value_supportpreserve)) * s) + (ssr_target_column_value_supportpreserve))) /\ (((exists pvs_gap_column_value_supportpreservetarget_bound. pvs_gap_column_value_supportpreservetarget_bound + S (ssr_target_column_value_supportpreserve) = (M)) /\ (exists dst_positive_code_column_value_supportpreservetarget_value dst_positive_scale_column_value_supportpreservetarget_value dst_negative_code_column_value_supportpreservetarget_value dst_negative_scale_column_value_supportpreservetarget_value dst_positive_column_value_supportpreservetarget_value dst_negative_column_value_supportpreservetarget_value. (((B) = (((((dst_positive_code_column_value_supportpreservetarget_value) + (dst_positive_scale_column_value_supportpreservetarget_value)) * S ((dst_positive_code_column_value_supportpreservetarget_value) + (dst_positive_scale_column_value_supportpreservetarget_value)) + ((dst_positive_scale_column_value_supportpreservetarget_value) + (dst_positive_scale_column_value_supportpreservetarget_value))) + (((dst_negative_code_column_value_supportpreservetarget_value) + (dst_negative_scale_column_value_supportpreservetarget_value)) * S ((dst_negative_code_column_value_supportpreservetarget_value) + (dst_negative_scale_column_value_supportpreservetarget_value)) + ((dst_negative_scale_column_value_supportpreservetarget_value) + (dst_negative_scale_column_value_supportpreservetarget_value)))) * S ((((dst_positive_code_column_value_supportpreservetarget_value) + (dst_positive_scale_column_value_supportpreservetarget_value)) * S ((dst_positive_code_column_value_supportpreservetarget_value) + (dst_positive_scale_column_value_supportpreservetarget_value)) + ((dst_positive_scale_column_value_supportpreservetarget_value) + (dst_positive_scale_column_value_supportpreservetarget_value))) + (((dst_negative_code_column_value_supportpreservetarget_value) + (dst_negative_scale_column_value_supportpreservetarget_value)) * S ((dst_negative_code_column_value_supportpreservetarget_value) + (dst_negative_scale_column_value_supportpreservetarget_value)) + ((dst_negative_scale_column_value_supportpreservetarget_value) + (dst_negative_scale_column_value_supportpreservetarget_value)))) + ((((dst_negative_code_column_value_supportpreservetarget_value) + (dst_negative_scale_column_value_supportpreservetarget_value)) * S ((dst_negative_code_column_value_supportpreservetarget_value) + (dst_negative_scale_column_value_supportpreservetarget_value)) + ((dst_negative_scale_column_value_supportpreservetarget_value) + (dst_negative_scale_column_value_supportpreservetarget_value))) + (((dst_negative_code_column_value_supportpreservetarget_value) + (dst_negative_scale_column_value_supportpreservetarget_value)) * S ((dst_negative_code_column_value_supportpreservetarget_value) + (dst_negative_scale_column_value_supportpreservetarget_value)) + ((dst_negative_scale_column_value_supportpreservetarget_value) + (dst_negative_scale_column_value_supportpreservetarget_value)))))) /\ (((((exists ff_h_pvs_column_value_supportpreservetarget_valuepositive. ff_h_pvs_column_value_supportpreservetarget_valuepositive + S (dst_positive_column_value_supportpreservetarget_value) = S ((S (ssr_target_column_value_supportpreserve)) * dst_positive_scale_column_value_supportpreservetarget_value)) /\ exists ff_q_pvs_column_value_supportpreservetarget_valuepositive. dst_positive_code_column_value_supportpreservetarget_value = ff_q_pvs_column_value_supportpreservetarget_valuepositive * S ((S (ssr_target_column_value_supportpreserve)) * dst_positive_scale_column_value_supportpreservetarget_value) + (dst_positive_column_value_supportpreservetarget_value))) /\ (((((exists ff_h_pvs_column_value_supportpreservetarget_valuenegative. ff_h_pvs_column_value_supportpreservetarget_valuenegative + S (dst_negative_column_value_supportpreservetarget_value) = S ((S (ssr_target_column_value_supportpreserve)) * dst_negative_scale_column_value_supportpreservetarget_value)) /\ exists ff_q_pvs_column_value_supportpreservetarget_valuenegative. dst_negative_code_column_value_supportpreservetarget_value = ff_q_pvs_column_value_supportpreservetarget_valuenegative * S ((S (ssr_target_column_value_supportpreserve)) * dst_negative_scale_column_value_supportpreservetarget_value) + (dst_negative_column_value_supportpreservetarget_value))) /\ (exists ge_balance_positive_column_value_supportpreservetarget_valuevalue ge_balance_negative_column_value_supportpreservetarget_valuevalue. (((((ssr_value_column_value_supportpreserve) = 2 * (ge_balance_positive_column_value_supportpreservetarget_valuevalue) /\ (ge_balance_negative_column_value_supportpreservetarget_valuevalue) = 0) \/ exists ge_signed_half_column_value_supportpreservetarget_valuevaluedecode. (((ssr_value_column_value_supportpreserve) = 2 * ge_signed_half_column_value_supportpreservetarget_valuevaluedecode + 1 /\ (ge_balance_positive_column_value_supportpreservetarget_valuevalue) = 0) /\ (ge_balance_negative_column_value_supportpreservetarget_valuevalue) = S ge_signed_half_column_value_supportpreservetarget_valuevaluedecode))) /\ ((dst_positive_column_value_supportpreservetarget_value) + ge_balance_negative_column_value_supportpreservetarget_valuevalue = (dst_negative_column_value_supportpreservetarget_value) + ge_balance_positive_column_value_supportpreservetarget_valuevalue))))))))))))) /\ (((forall ssr_first_column_value_supportinjective ssr_second_column_value_supportinjective ssr_image_column_value_supportinjective ssr_a_column_value_supportinjective ssr_b_column_value_supportinjective. (exists pvs_gap_column_value_supportinjectivefirst_bound. pvs_gap_column_value_supportinjectivefirst_bound + S (ssr_first_column_value_supportinjective) = (L)) -> (exists pvs_gap_column_value_supportinjectivesecond_bound. pvs_gap_column_value_supportinjectivesecond_bound + S (ssr_second_column_value_supportinjective) = (L)) -> (exists dst_positive_code_column_value_supportinjectivefirst_value dst_positive_scale_column_value_supportinjectivefirst_value dst_negative_code_column_value_supportinjectivefirst_value dst_negative_scale_column_value_supportinjectivefirst_value dst_positive_column_value_supportinjectivefirst_value dst_negative_column_value_supportinjectivefirst_value. (((A) = (((((dst_positive_code_column_value_supportinjectivefirst_value) + (dst_positive_scale_column_value_supportinjectivefirst_value)) * S ((dst_positive_code_column_value_supportinjectivefirst_value) + (dst_positive_scale_column_value_supportinjectivefirst_value)) + ((dst_positive_scale_column_value_supportinjectivefirst_value) + (dst_positive_scale_column_value_supportinjectivefirst_value))) + (((dst_negative_code_column_value_supportinjectivefirst_value) + (dst_negative_scale_column_value_supportinjectivefirst_value)) * S ((dst_negative_code_column_value_supportinjectivefirst_value) + (dst_negative_scale_column_value_supportinjectivefirst_value)) + ((dst_negative_scale_column_value_supportinjectivefirst_value) + (dst_negative_scale_column_value_supportinjectivefirst_value)))) * S ((((dst_positive_code_column_value_supportinjectivefirst_value) + (dst_positive_scale_column_value_supportinjectivefirst_value)) * S ((dst_positive_code_column_value_supportinjectivefirst_value) + (dst_positive_scale_column_value_supportinjectivefirst_value)) + ((dst_positive_scale_column_value_supportinjectivefirst_value) + (dst_positive_scale_column_value_supportinjectivefirst_value))) + (((dst_negative_code_column_value_supportinjectivefirst_value) + (dst_negative_scale_column_value_supportinjectivefirst_value)) * S ((dst_negative_code_column_value_supportinjectivefirst_value) + (dst_negative_scale_column_value_supportinjectivefirst_value)) + ((dst_negative_scale_column_value_supportinjectivefirst_value) + (dst_negative_scale_column_value_supportinjectivefirst_value)))) + ((((dst_negative_code_column_value_supportinjectivefirst_value) + (dst_negative_scale_column_value_supportinjectivefirst_value)) * S ((dst_negative_code_column_value_supportinjectivefirst_value) + (dst_negative_scale_column_value_supportinjectivefirst_value)) + ((dst_negative_scale_column_value_supportinjectivefirst_value) + (dst_negative_scale_column_value_supportinjectivefirst_value))) + (((dst_negative_code_column_value_supportinjectivefirst_value) + (dst_negative_scale_column_value_supportinjectivefirst_value)) * S ((dst_negative_code_column_value_supportinjectivefirst_value) + (dst_negative_scale_column_value_supportinjectivefirst_value)) + ((dst_negative_scale_column_value_supportinjectivefirst_value) + (dst_negative_scale_column_value_supportinjectivefirst_value)))))) /\ (((((exists ff_h_pvs_column_value_supportinjectivefirst_valuepositive. ff_h_pvs_column_value_supportinjectivefirst_valuepositive + S (dst_positive_column_value_supportinjectivefirst_value) = S ((S (ssr_first_column_value_supportinjective)) * dst_positive_scale_column_value_supportinjectivefirst_value)) /\ exists ff_q_pvs_column_value_supportinjectivefirst_valuepositive. dst_positive_code_column_value_supportinjectivefirst_value = ff_q_pvs_column_value_supportinjectivefirst_valuepositive * S ((S (ssr_first_column_value_supportinjective)) * dst_positive_scale_column_value_supportinjectivefirst_value) + (dst_positive_column_value_supportinjectivefirst_value))) /\ (((((exists ff_h_pvs_column_value_supportinjectivefirst_valuenegative. ff_h_pvs_column_value_supportinjectivefirst_valuenegative + S (dst_negative_column_value_supportinjectivefirst_value) = S ((S (ssr_first_column_value_supportinjective)) * dst_negative_scale_column_value_supportinjectivefirst_value)) /\ exists ff_q_pvs_column_value_supportinjectivefirst_valuenegative. dst_negative_code_column_value_supportinjectivefirst_value = ff_q_pvs_column_value_supportinjectivefirst_valuenegative * S ((S (ssr_first_column_value_supportinjective)) * dst_negative_scale_column_value_supportinjectivefirst_value) + (dst_negative_column_value_supportinjectivefirst_value))) /\ (exists ge_balance_positive_column_value_supportinjectivefirst_valuevalue ge_balance_negative_column_value_supportinjectivefirst_valuevalue. (((((ssr_a_column_value_supportinjective) = 2 * (ge_balance_positive_column_value_supportinjectivefirst_valuevalue) /\ (ge_balance_negative_column_value_supportinjectivefirst_valuevalue) = 0) \/ exists ge_signed_half_column_value_supportinjectivefirst_valuevaluedecode. (((ssr_a_column_value_supportinjective) = 2 * ge_signed_half_column_value_supportinjectivefirst_valuevaluedecode + 1 /\ (ge_balance_positive_column_value_supportinjectivefirst_valuevalue) = 0) /\ (ge_balance_negative_column_value_supportinjectivefirst_valuevalue) = S ge_signed_half_column_value_supportinjectivefirst_valuevaluedecode))) /\ ((dst_positive_column_value_supportinjectivefirst_value) + ge_balance_negative_column_value_supportinjectivefirst_valuevalue = (dst_negative_column_value_supportinjectivefirst_value) + ge_balance_positive_column_value_supportinjectivefirst_valuevalue))))))))) -> ~(ssr_a_column_value_supportinjective=0) -> (exists dst_positive_code_column_value_supportinjectivesecond_value dst_positive_scale_column_value_supportinjectivesecond_value dst_negative_code_column_value_supportinjectivesecond_value dst_negative_scale_column_value_supportinjectivesecond_value dst_positive_column_value_supportinjectivesecond_value dst_negative_column_value_supportinjectivesecond_value. (((A) = (((((dst_positive_code_column_value_supportinjectivesecond_value) + (dst_positive_scale_column_value_supportinjectivesecond_value)) * S ((dst_positive_code_column_value_supportinjectivesecond_value) + (dst_positive_scale_column_value_supportinjectivesecond_value)) + ((dst_positive_scale_column_value_supportinjectivesecond_value) + (dst_positive_scale_column_value_supportinjectivesecond_value))) + (((dst_negative_code_column_value_supportinjectivesecond_value) + (dst_negative_scale_column_value_supportinjectivesecond_value)) * S ((dst_negative_code_column_value_supportinjectivesecond_value) + (dst_negative_scale_column_value_supportinjectivesecond_value)) + ((dst_negative_scale_column_value_supportinjectivesecond_value) + (dst_negative_scale_column_value_supportinjectivesecond_value)))) * S ((((dst_positive_code_column_value_supportinjectivesecond_value) + (dst_positive_scale_column_value_supportinjectivesecond_value)) * S ((dst_positive_code_column_value_supportinjectivesecond_value) + (dst_positive_scale_column_value_supportinjectivesecond_value)) + ((dst_positive_scale_column_value_supportinjectivesecond_value) + (dst_positive_scale_column_value_supportinjectivesecond_value))) + (((dst_negative_code_column_value_supportinjectivesecond_value) + (dst_negative_scale_column_value_supportinjectivesecond_value)) * S ((dst_negative_code_column_value_supportinjectivesecond_value) + (dst_negative_scale_column_value_supportinjectivesecond_value)) + ((dst_negative_scale_column_value_supportinjectivesecond_value) + (dst_negative_scale_column_value_supportinjectivesecond_value)))) + ((((dst_negative_code_column_value_supportinjectivesecond_value) + (dst_negative_scale_column_value_supportinjectivesecond_value)) * S ((dst_negative_code_column_value_supportinjectivesecond_value) + (dst_negative_scale_column_value_supportinjectivesecond_value)) + ((dst_negative_scale_column_value_supportinjectivesecond_value) + (dst_negative_scale_column_value_supportinjectivesecond_value))) + (((dst_negative_code_column_value_supportinjectivesecond_value) + (dst_negative_scale_column_value_supportinjectivesecond_value)) * S ((dst_negative_code_column_value_supportinjectivesecond_value) + (dst_negative_scale_column_value_supportinjectivesecond_value)) + ((dst_negative_scale_column_value_supportinjectivesecond_value) + (dst_negative_scale_column_value_supportinjectivesecond_value)))))) /\ (((((exists ff_h_pvs_column_value_supportinjectivesecond_valuepositive. ff_h_pvs_column_value_supportinjectivesecond_valuepositive + S (dst_positive_column_value_supportinjectivesecond_value) = S ((S (ssr_second_column_value_supportinjective)) * dst_positive_scale_column_value_supportinjectivesecond_value)) /\ exists ff_q_pvs_column_value_supportinjectivesecond_valuepositive. dst_positive_code_column_value_supportinjectivesecond_value = ff_q_pvs_column_value_supportinjectivesecond_valuepositive * S ((S (ssr_second_column_value_supportinjective)) * dst_positive_scale_column_value_supportinjectivesecond_value) + (dst_positive_column_value_supportinjectivesecond_value))) /\ (((((exists ff_h_pvs_column_value_supportinjectivesecond_valuenegative. ff_h_pvs_column_value_supportinjectivesecond_valuenegative + S (dst_negative_column_value_supportinjectivesecond_value) = S ((S (ssr_second_column_value_supportinjective)) * dst_negative_scale_column_value_supportinjectivesecond_value)) /\ exists ff_q_pvs_column_value_supportinjectivesecond_valuenegative. dst_negative_code_column_value_supportinjectivesecond_value = ff_q_pvs_column_value_supportinjectivesecond_valuenegative * S ((S (ssr_second_column_value_supportinjective)) * dst_negative_scale_column_value_supportinjectivesecond_value) + (dst_negative_column_value_supportinjectivesecond_value))) /\ (exists ge_balance_positive_column_value_supportinjectivesecond_valuevalue ge_balance_negative_column_value_supportinjectivesecond_valuevalue. (((((ssr_b_column_value_supportinjective) = 2 * (ge_balance_positive_column_value_supportinjectivesecond_valuevalue) /\ (ge_balance_negative_column_value_supportinjectivesecond_valuevalue) = 0) \/ exists ge_signed_half_column_value_supportinjectivesecond_valuevaluedecode. (((ssr_b_column_value_supportinjective) = 2 * ge_signed_half_column_value_supportinjectivesecond_valuevaluedecode + 1 /\ (ge_balance_positive_column_value_supportinjectivesecond_valuevalue) = 0) /\ (ge_balance_negative_column_value_supportinjectivesecond_valuevalue) = S ge_signed_half_column_value_supportinjectivesecond_valuevaluedecode))) /\ ((dst_positive_column_value_supportinjectivesecond_value) + ge_balance_negative_column_value_supportinjectivesecond_valuevalue = (dst_negative_column_value_supportinjectivesecond_value) + ge_balance_positive_column_value_supportinjectivesecond_valuevalue))))))))) -> ~(ssr_b_column_value_supportinjective=0) -> (((exists ff_h_pvs_column_value_supportinjectivefirst_map. ff_h_pvs_column_value_supportinjectivefirst_map + S (ssr_image_column_value_supportinjective) = S ((S (ssr_first_column_value_supportinjective)) * s)) /\ exists ff_q_pvs_column_value_supportinjectivefirst_map. r = ff_q_pvs_column_value_supportinjectivefirst_map * S ((S (ssr_first_column_value_supportinjective)) * s) + (ssr_image_column_value_supportinjective))) -> (((exists ff_h_pvs_column_value_supportinjectivesecond_map. ff_h_pvs_column_value_supportinjectivesecond_map + S (ssr_image_column_value_supportinjective) = S ((S (ssr_second_column_value_supportinjective)) * s)) /\ exists ff_q_pvs_column_value_supportinjectivesecond_map. r = ff_q_pvs_column_value_supportinjectivesecond_map * S ((S (ssr_second_column_value_supportinjective)) * s) + (ssr_image_column_value_supportinjective))) -> ssr_first_column_value_supportinjective=ssr_second_column_value_supportinjective) /\ (forall ssr_target_column_value_supportcover ssr_value_column_value_supportcover. (exists pvs_gap_column_value_supportcovertarget_bound. pvs_gap_column_value_supportcovertarget_bound + S (ssr_target_column_value_supportcover) = (M)) -> (exists dst_positive_code_column_value_supportcovertarget_value dst_positive_scale_column_value_supportcovertarget_value dst_negative_code_column_value_supportcovertarget_value dst_negative_scale_column_value_supportcovertarget_value dst_positive_column_value_supportcovertarget_value dst_negative_column_value_supportcovertarget_value. (((B) = (((((dst_positive_code_column_value_supportcovertarget_value) + (dst_positive_scale_column_value_supportcovertarget_value)) * S ((dst_positive_code_column_value_supportcovertarget_value) + (dst_positive_scale_column_value_supportcovertarget_value)) + ((dst_positive_scale_column_value_supportcovertarget_value) + (dst_positive_scale_column_value_supportcovertarget_value))) + (((dst_negative_code_column_value_supportcovertarget_value) + (dst_negative_scale_column_value_supportcovertarget_value)) * S ((dst_negative_code_column_value_supportcovertarget_value) + (dst_negative_scale_column_value_supportcovertarget_value)) + ((dst_negative_scale_column_value_supportcovertarget_value) + (dst_negative_scale_column_value_supportcovertarget_value)))) * S ((((dst_positive_code_column_value_supportcovertarget_value) + (dst_positive_scale_column_value_supportcovertarget_value)) * S ((dst_positive_code_column_value_supportcovertarget_value) + (dst_positive_scale_column_value_supportcovertarget_value)) + ((dst_positive_scale_column_value_supportcovertarget_value) + (dst_positive_scale_column_value_supportcovertarget_value))) + (((dst_negative_code_column_value_supportcovertarget_value) + (dst_negative_scale_column_value_supportcovertarget_value)) * S ((dst_negative_code_column_value_supportcovertarget_value) + (dst_negative_scale_column_value_supportcovertarget_value)) + ((dst_negative_scale_column_value_supportcovertarget_value) + (dst_negative_scale_column_value_supportcovertarget_value)))) + ((((dst_negative_code_column_value_supportcovertarget_value) + (dst_negative_scale_column_value_supportcovertarget_value)) * S ((dst_negative_code_column_value_supportcovertarget_value) + (dst_negative_scale_column_value_supportcovertarget_value)) + ((dst_negative_scale_column_value_supportcovertarget_value) + (dst_negative_scale_column_value_supportcovertarget_value))) + (((dst_negative_code_column_value_supportcovertarget_value) + (dst_negative_scale_column_value_supportcovertarget_value)) * S ((dst_negative_code_column_value_supportcovertarget_value) + (dst_negative_scale_column_value_supportcovertarget_value)) + ((dst_negative_scale_column_value_supportcovertarget_value) + (dst_negative_scale_column_value_supportcovertarget_value)))))) /\ (((((exists ff_h_pvs_column_value_supportcovertarget_valuepositive. ff_h_pvs_column_value_supportcovertarget_valuepositive + S (dst_positive_column_value_supportcovertarget_value) = S ((S (ssr_target_column_value_supportcover)) * dst_positive_scale_column_value_supportcovertarget_value)) /\ exists ff_q_pvs_column_value_supportcovertarget_valuepositive. dst_positive_code_column_value_supportcovertarget_value = ff_q_pvs_column_value_supportcovertarget_valuepositive * S ((S (ssr_target_column_value_supportcover)) * dst_positive_scale_column_value_supportcovertarget_value) + (dst_positive_column_value_supportcovertarget_value))) /\ (((((exists ff_h_pvs_column_value_supportcovertarget_valuenegative. ff_h_pvs_column_value_supportcovertarget_valuenegative + S (dst_negative_column_value_supportcovertarget_value) = S ((S (ssr_target_column_value_supportcover)) * dst_negative_scale_column_value_supportcovertarget_value)) /\ exists ff_q_pvs_column_value_supportcovertarget_valuenegative. dst_negative_code_column_value_supportcovertarget_value = ff_q_pvs_column_value_supportcovertarget_valuenegative * S ((S (ssr_target_column_value_supportcover)) * dst_negative_scale_column_value_supportcovertarget_value) + (dst_negative_column_value_supportcovertarget_value))) /\ (exists ge_balance_positive_column_value_supportcovertarget_valuevalue ge_balance_negative_column_value_supportcovertarget_valuevalue. (((((ssr_value_column_value_supportcover) = 2 * (ge_balance_positive_column_value_supportcovertarget_valuevalue) /\ (ge_balance_negative_column_value_supportcovertarget_valuevalue) = 0) \/ exists ge_signed_half_column_value_supportcovertarget_valuevaluedecode. (((ssr_value_column_value_supportcover) = 2 * ge_signed_half_column_value_supportcovertarget_valuevaluedecode + 1 /\ (ge_balance_positive_column_value_supportcovertarget_valuevalue) = 0) /\ (ge_balance_negative_column_value_supportcovertarget_valuevalue) = S ge_signed_half_column_value_supportcovertarget_valuevaluedecode))) /\ ((dst_positive_column_value_supportcovertarget_value) + ge_balance_negative_column_value_supportcovertarget_valuevalue = (dst_negative_column_value_supportcovertarget_value) + ge_balance_positive_column_value_supportcovertarget_valuevalue))))))))) -> ~(ssr_value_column_value_supportcover=0) -> exists ssr_source_column_value_supportcover. ((exists pvs_gap_column_value_supportcoversource_bound. pvs_gap_column_value_supportcoversource_bound + S (ssr_source_column_value_supportcover) = (L)) /\ (((((exists ff_h_pvs_column_value_supportcovermap. ff_h_pvs_column_value_supportcovermap + S (ssr_target_column_value_supportcover) = S ((S (ssr_source_column_value_supportcover)) * s)) /\ exists ff_q_pvs_column_value_supportcovermap. r = ff_q_pvs_column_value_supportcovermap * S ((S (ssr_source_column_value_supportcover)) * s) + (ssr_target_column_value_supportcover))) /\ (exists dst_positive_code_column_value_supportcoversource_value dst_positive_scale_column_value_supportcoversource_value dst_negative_code_column_value_supportcoversource_value dst_negative_scale_column_value_supportcoversource_value dst_positive_column_value_supportcoversource_value dst_negative_column_value_supportcoversource_value. (((A) = (((((dst_positive_code_column_value_supportcoversource_value) + (dst_positive_scale_column_value_supportcoversource_value)) * S ((dst_positive_code_column_value_supportcoversource_value) + (dst_positive_scale_column_value_supportcoversource_value)) + ((dst_positive_scale_column_value_supportcoversource_value) + (dst_positive_scale_column_value_supportcoversource_value))) + (((dst_negative_code_column_value_supportcoversource_value) + (dst_negative_scale_column_value_supportcoversource_value)) * S ((dst_negative_code_column_value_supportcoversource_value) + (dst_negative_scale_column_value_supportcoversource_value)) + ((dst_negative_scale_column_value_supportcoversource_value) + (dst_negative_scale_column_value_supportcoversource_value)))) * S ((((dst_positive_code_column_value_supportcoversource_value) + (dst_positive_scale_column_value_supportcoversource_value)) * S ((dst_positive_code_column_value_supportcoversource_value) + (dst_positive_scale_column_value_supportcoversource_value)) + ((dst_positive_scale_column_value_supportcoversource_value) + (dst_positive_scale_column_value_supportcoversource_value))) + (((dst_negative_code_column_value_supportcoversource_value) + (dst_negative_scale_column_value_supportcoversource_value)) * S ((dst_negative_code_column_value_supportcoversource_value) + (dst_negative_scale_column_value_supportcoversource_value)) + ((dst_negative_scale_column_value_supportcoversource_value) + (dst_negative_scale_column_value_supportcoversource_value)))) + ((((dst_negative_code_column_value_supportcoversource_value) + (dst_negative_scale_column_value_supportcoversource_value)) * S ((dst_negative_code_column_value_supportcoversource_value) + (dst_negative_scale_column_value_supportcoversource_value)) + ((dst_negative_scale_column_value_supportcoversource_value) + (dst_negative_scale_column_value_supportcoversource_value))) + (((dst_negative_code_column_value_supportcoversource_value) + (dst_negative_scale_column_value_supportcoversource_value)) * S ((dst_negative_code_column_value_supportcoversource_value) + (dst_negative_scale_column_value_supportcoversource_value)) + ((dst_negative_scale_column_value_supportcoversource_value) + (dst_negative_scale_column_value_supportcoversource_value)))))) /\ (((((exists ff_h_pvs_column_value_supportcoversource_valuepositive. ff_h_pvs_column_value_supportcoversource_valuepositive + S (dst_positive_column_value_supportcoversource_value) = S ((S (ssr_source_column_value_supportcover)) * dst_positive_scale_column_value_supportcoversource_value)) /\ exists ff_q_pvs_column_value_supportcoversource_valuepositive. dst_positive_code_column_value_supportcoversource_value = ff_q_pvs_column_value_supportcoversource_valuepositive * S ((S (ssr_source_column_value_supportcover)) * dst_positive_scale_column_value_supportcoversource_value) + (dst_positive_column_value_supportcoversource_value))) /\ (((((exists ff_h_pvs_column_value_supportcoversource_valuenegative. ff_h_pvs_column_value_supportcoversource_valuenegative + S (dst_negative_column_value_supportcoversource_value) = S ((S (ssr_source_column_value_supportcover)) * dst_negative_scale_column_value_supportcoversource_value)) /\ exists ff_q_pvs_column_value_supportcoversource_valuenegative. dst_negative_code_column_value_supportcoversource_value = ff_q_pvs_column_value_supportcoversource_valuenegative * S ((S (ssr_source_column_value_supportcover)) * dst_negative_scale_column_value_supportcoversource_value) + (dst_negative_column_value_supportcoversource_value))) /\ (exists ge_balance_positive_column_value_supportcoversource_valuevalue ge_balance_negative_column_value_supportcoversource_valuevalue. (((((ssr_value_column_value_supportcover) = 2 * (ge_balance_positive_column_value_supportcoversource_valuevalue) /\ (ge_balance_negative_column_value_supportcoversource_valuevalue) = 0) \/ exists ge_signed_half_column_value_supportcoversource_valuevaluedecode. (((ssr_value_column_value_supportcover) = 2 * ge_signed_half_column_value_supportcoversource_valuevaluedecode + 1 /\ (ge_balance_positive_column_value_supportcoversource_valuevalue) = 0) /\ (ge_balance_negative_column_value_supportcoversource_valuevalue) = S ge_signed_half_column_value_supportcoversource_valuevaluedecode))) /\ ((dst_positive_column_value_supportcoversource_value) + ge_balance_negative_column_value_supportcoversource_valuevalue = (dst_negative_column_value_supportcoversource_value) + ge_balance_positive_column_value_supportcoversource_valuevalue))))))))))))))))))))) -> (((exists dst_positive_code_column_value_gridsource dst_positive_scale_column_value_gridsource dst_negative_code_column_value_gridsource dst_negative_scale_column_value_gridsource. (((A) = (((((dst_positive_code_column_value_gridsource) + (dst_positive_scale_column_value_gridsource)) * S ((dst_positive_code_column_value_gridsource) + (dst_positive_scale_column_value_gridsource)) + ((dst_positive_scale_column_value_gridsource) + (dst_positive_scale_column_value_gridsource))) + (((dst_negative_code_column_value_gridsource) + (dst_negative_scale_column_value_gridsource)) * S ((dst_negative_code_column_value_gridsource) + (dst_negative_scale_column_value_gridsource)) + ((dst_negative_scale_column_value_gridsource) + (dst_negative_scale_column_value_gridsource)))) * S ((((dst_positive_code_column_value_gridsource) + (dst_positive_scale_column_value_gridsource)) * S ((dst_positive_code_column_value_gridsource) + (dst_positive_scale_column_value_gridsource)) + ((dst_positive_scale_column_value_gridsource) + (dst_positive_scale_column_value_gridsource))) + (((dst_negative_code_column_value_gridsource) + (dst_negative_scale_column_value_gridsource)) * S ((dst_negative_code_column_value_gridsource) + (dst_negative_scale_column_value_gridsource)) + ((dst_negative_scale_column_value_gridsource) + (dst_negative_scale_column_value_gridsource)))) + ((((dst_negative_code_column_value_gridsource) + (dst_negative_scale_column_value_gridsource)) * S ((dst_negative_code_column_value_gridsource) + (dst_negative_scale_column_value_gridsource)) + ((dst_negative_scale_column_value_gridsource) + (dst_negative_scale_column_value_gridsource))) + (((dst_negative_code_column_value_gridsource) + (dst_negative_scale_column_value_gridsource)) * S ((dst_negative_code_column_value_gridsource) + (dst_negative_scale_column_value_gridsource)) + ((dst_negative_scale_column_value_gridsource) + (dst_negative_scale_column_value_gridsource)))))) /\ (forall dst_index_column_value_gridsource. (exists pvs_le_gap_column_value_gridsourcedomain. pvs_le_gap_column_value_gridsourcedomain + (dst_index_column_value_gridsource) = (0)) -> exists dst_positive_column_value_gridsource dst_negative_column_value_gridsource dst_value_column_value_gridsource. ((((exists ff_h_pvs_column_value_gridsourceentrypositive. ff_h_pvs_column_value_gridsourceentrypositive + S (dst_positive_column_value_gridsource) = S ((S (dst_index_column_value_gridsource)) * dst_positive_scale_column_value_gridsource)) /\ exists ff_q_pvs_column_value_gridsourceentrypositive. dst_positive_code_column_value_gridsource = ff_q_pvs_column_value_gridsourceentrypositive * S ((S (dst_index_column_value_gridsource)) * dst_positive_scale_column_value_gridsource) + (dst_positive_column_value_gridsource))) /\ (((((exists ff_h_pvs_column_value_gridsourceentrynegative. ff_h_pvs_column_value_gridsourceentrynegative + S (dst_negative_column_value_gridsource) = S ((S (dst_index_column_value_gridsource)) * dst_negative_scale_column_value_gridsource)) /\ exists ff_q_pvs_column_value_gridsourceentrynegative. dst_negative_code_column_value_gridsource = ff_q_pvs_column_value_gridsourceentrynegative * S ((S (dst_index_column_value_gridsource)) * dst_negative_scale_column_value_gridsource) + (dst_negative_column_value_gridsource))) /\ (exists ge_balance_positive_column_value_gridsourceentryvalue ge_balance_negative_column_value_gridsourceentryvalue. (((((dst_value_column_value_gridsource) = 2 * (ge_balance_positive_column_value_gridsourceentryvalue) /\ (ge_balance_negative_column_value_gridsourceentryvalue) = 0) \/ exists ge_signed_half_column_value_gridsourceentryvaluedecode. (((dst_value_column_value_gridsource) = 2 * ge_signed_half_column_value_gridsourceentryvaluedecode + 1 /\ (ge_balance_positive_column_value_gridsourceentryvalue) = 0) /\ (ge_balance_negative_column_value_gridsourceentryvalue) = S ge_signed_half_column_value_gridsourceentryvaluedecode))) /\ ((dst_positive_column_value_gridsource) + ge_balance_negative_column_value_gridsourceentryvalue = (dst_negative_column_value_gridsource) + ge_balance_positive_column_value_gridsourceentryvalue))))))))) /\ (((exists dst_positive_code_column_value_gridtable dst_positive_scale_column_value_gridtable dst_negative_code_column_value_gridtable dst_negative_scale_column_value_gridtable. (((T) = (((((dst_positive_code_column_value_gridtable) + (dst_positive_scale_column_value_gridtable)) * S ((dst_positive_code_column_value_gridtable) + (dst_positive_scale_column_value_gridtable)) + ((dst_positive_scale_column_value_gridtable) + (dst_positive_scale_column_value_gridtable))) + (((dst_negative_code_column_value_gridtable) + (dst_negative_scale_column_value_gridtable)) * S ((dst_negative_code_column_value_gridtable) + (dst_negative_scale_column_value_gridtable)) + ((dst_negative_scale_column_value_gridtable) + (dst_negative_scale_column_value_gridtable)))) * S ((((dst_positive_code_column_value_gridtable) + (dst_positive_scale_column_value_gridtable)) * S ((dst_positive_code_column_value_gridtable) + (dst_positive_scale_column_value_gridtable)) + ((dst_positive_scale_column_value_gridtable) + (dst_positive_scale_column_value_gridtable))) + (((dst_negative_code_column_value_gridtable) + (dst_negative_scale_column_value_gridtable)) * S ((dst_negative_code_column_value_gridtable) + (dst_negative_scale_column_value_gridtable)) + ((dst_negative_scale_column_value_gridtable) + (dst_negative_scale_column_value_gridtable)))) + ((((dst_negative_code_column_value_gridtable) + (dst_negative_scale_column_value_gridtable)) * S ((dst_negative_code_column_value_gridtable) + (dst_negative_scale_column_value_gridtable)) + ((dst_negative_scale_column_value_gridtable) + (dst_negative_scale_column_value_gridtable))) + (((dst_negative_code_column_value_gridtable) + (dst_negative_scale_column_value_gridtable)) * S ((dst_negative_code_column_value_gridtable) + (dst_negative_scale_column_value_gridtable)) + ((dst_negative_scale_column_value_gridtable) + (dst_negative_scale_column_value_gridtable)))))) /\ (forall dst_index_column_value_gridtable. (exists pvs_le_gap_column_value_gridtabledomain. pvs_le_gap_column_value_gridtabledomain + (dst_index_column_value_gridtable) = ((L)*(S (M)))) -> exists dst_positive_column_value_gridtable dst_negative_column_value_gridtable dst_value_column_value_gridtable. ((((exists ff_h_pvs_column_value_gridtableentrypositive. ff_h_pvs_column_value_gridtableentrypositive + S (dst_positive_column_value_gridtable) = S ((S (dst_index_column_value_gridtable)) * dst_positive_scale_column_value_gridtable)) /\ exists ff_q_pvs_column_value_gridtableentrypositive. dst_positive_code_column_value_gridtable = ff_q_pvs_column_value_gridtableentrypositive * S ((S (dst_index_column_value_gridtable)) * dst_positive_scale_column_value_gridtable) + (dst_positive_column_value_gridtable))) /\ (((((exists ff_h_pvs_column_value_gridtableentrynegative. ff_h_pvs_column_value_gridtableentrynegative + S (dst_negative_column_value_gridtable) = S ((S (dst_index_column_value_gridtable)) * dst_negative_scale_column_value_gridtable)) /\ exists ff_q_pvs_column_value_gridtableentrynegative. dst_negative_code_column_value_gridtable = ff_q_pvs_column_value_gridtableentrynegative * S ((S (dst_index_column_value_gridtable)) * dst_negative_scale_column_value_gridtable) + (dst_negative_column_value_gridtable))) /\ (exists ge_balance_positive_column_value_gridtableentryvalue ge_balance_negative_column_value_gridtableentryvalue. (((((dst_value_column_value_gridtable) = 2 * (ge_balance_positive_column_value_gridtableentryvalue) /\ (ge_balance_negative_column_value_gridtableentryvalue) = 0) \/ exists ge_signed_half_column_value_gridtableentryvaluedecode. (((dst_value_column_value_gridtable) = 2 * ge_signed_half_column_value_gridtableentryvaluedecode + 1 /\ (ge_balance_positive_column_value_gridtableentryvalue) = 0) /\ (ge_balance_negative_column_value_gridtableentryvalue) = S ge_signed_half_column_value_gridtableentryvaluedecode))) /\ ((dst_positive_column_value_gridtable) + ge_balance_negative_column_value_gridtableentryvalue = (dst_negative_column_value_gridtable) + ge_balance_positive_column_value_gridtableentryvalue))))))))) /\ (forall ssr_grid_row_column_value_grid ssr_grid_column_column_value_grid ssr_grid_value_column_value_grid. (exists pvs_gap_column_value_gridrow_bound. pvs_gap_column_value_gridrow_bound + S (ssr_grid_row_column_value_grid) = (L)) -> (exists pvs_gap_column_value_gridcolumn_bound. pvs_gap_column_value_gridcolumn_bound + S (ssr_grid_column_column_value_grid) = (M)) -> (exists dst_positive_code_column_value_gridlookup dst_positive_scale_column_value_gridlookup dst_negative_code_column_value_gridlookup dst_negative_scale_column_value_gridlookup dst_positive_column_value_gridlookup dst_negative_column_value_gridlookup. (((T) = (((((dst_positive_code_column_value_gridlookup) + (dst_positive_scale_column_value_gridlookup)) * S ((dst_positive_code_column_value_gridlookup) + (dst_positive_scale_column_value_gridlookup)) + ((dst_positive_scale_column_value_gridlookup) + (dst_positive_scale_column_value_gridlookup))) + (((dst_negative_code_column_value_gridlookup) + (dst_negative_scale_column_value_gridlookup)) * S ((dst_negative_code_column_value_gridlookup) + (dst_negative_scale_column_value_gridlookup)) + ((dst_negative_scale_column_value_gridlookup) + (dst_negative_scale_column_value_gridlookup)))) * S ((((dst_positive_code_column_value_gridlookup) + (dst_positive_scale_column_value_gridlookup)) * S ((dst_positive_code_column_value_gridlookup) + (dst_positive_scale_column_value_gridlookup)) + ((dst_positive_scale_column_value_gridlookup) + (dst_positive_scale_column_value_gridlookup))) + (((dst_negative_code_column_value_gridlookup) + (dst_negative_scale_column_value_gridlookup)) * S ((dst_negative_code_column_value_gridlookup) + (dst_negative_scale_column_value_gridlookup)) + ((dst_negative_scale_column_value_gridlookup) + (dst_negative_scale_column_value_gridlookup)))) + ((((dst_negative_code_column_value_gridlookup) + (dst_negative_scale_column_value_gridlookup)) * S ((dst_negative_code_column_value_gridlookup) + (dst_negative_scale_column_value_gridlookup)) + ((dst_negative_scale_column_value_gridlookup) + (dst_negative_scale_column_value_gridlookup))) + (((dst_negative_code_column_value_gridlookup) + (dst_negative_scale_column_value_gridlookup)) * S ((dst_negative_code_column_value_gridlookup) + (dst_negative_scale_column_value_gridlookup)) + ((dst_negative_scale_column_value_gridlookup) + (dst_negative_scale_column_value_gridlookup)))))) /\ (((((exists ff_h_pvs_column_value_gridlookuppositive. ff_h_pvs_column_value_gridlookuppositive + S (dst_positive_column_value_gridlookup) = S ((S (((S (M))*(ssr_grid_row_column_value_grid)+(ssr_grid_column_column_value_grid)))) * dst_positive_scale_column_value_gridlookup)) /\ exists ff_q_pvs_column_value_gridlookuppositive. dst_positive_code_column_value_gridlookup = ff_q_pvs_column_value_gridlookuppositive * S ((S (((S (M))*(ssr_grid_row_column_value_grid)+(ssr_grid_column_column_value_grid)))) * dst_positive_scale_column_value_gridlookup) + (dst_positive_column_value_gridlookup))) /\ (((((exists ff_h_pvs_column_value_gridlookupnegative. ff_h_pvs_column_value_gridlookupnegative + S (dst_negative_column_value_gridlookup) = S ((S (((S (M))*(ssr_grid_row_column_value_grid)+(ssr_grid_column_column_value_grid)))) * dst_negative_scale_column_value_gridlookup)) /\ exists ff_q_pvs_column_value_gridlookupnegative. dst_negative_code_column_value_gridlookup = ff_q_pvs_column_value_gridlookupnegative * S ((S (((S (M))*(ssr_grid_row_column_value_grid)+(ssr_grid_column_column_value_grid)))) * dst_negative_scale_column_value_gridlookup) + (dst_negative_column_value_gridlookup))) /\ (exists ge_balance_positive_column_value_gridlookupvalue ge_balance_negative_column_value_gridlookupvalue. (((((ssr_grid_value_column_value_grid) = 2 * (ge_balance_positive_column_value_gridlookupvalue) /\ (ge_balance_negative_column_value_gridlookupvalue) = 0) \/ exists ge_signed_half_column_value_gridlookupvaluedecode. (((ssr_grid_value_column_value_grid) = 2 * ge_signed_half_column_value_gridlookupvaluedecode + 1 /\ (ge_balance_positive_column_value_gridlookupvalue) = 0) /\ (ge_balance_negative_column_value_gridlookupvalue) = S ge_signed_half_column_value_gridlookupvaluedecode))) /\ ((dst_positive_column_value_gridlookup) + ge_balance_negative_column_value_gridlookupvalue = (dst_negative_column_value_gridlookup) + ge_balance_positive_column_value_gridlookupvalue))))))))) -> (exists ssr_entry_value_column_value_gridentry ssr_entry_image_column_value_gridentry. ((exists dst_positive_code_column_value_gridentrysource dst_positive_scale_column_value_gridentrysource dst_negative_code_column_value_gridentrysource dst_negative_scale_column_value_gridentrysource dst_positive_column_value_gridentrysource dst_negative_column_value_gridentrysource. (((A) = (((((dst_positive_code_column_value_gridentrysource) + (dst_positive_scale_column_value_gridentrysource)) * S ((dst_positive_code_column_value_gridentrysource) + (dst_positive_scale_column_value_gridentrysource)) + ((dst_positive_scale_column_value_gridentrysource) + (dst_positive_scale_column_value_gridentrysource))) + (((dst_negative_code_column_value_gridentrysource) + (dst_negative_scale_column_value_gridentrysource)) * S ((dst_negative_code_column_value_gridentrysource) + (dst_negative_scale_column_value_gridentrysource)) + ((dst_negative_scale_column_value_gridentrysource) + (dst_negative_scale_column_value_gridentrysource)))) * S ((((dst_positive_code_column_value_gridentrysource) + (dst_positive_scale_column_value_gridentrysource)) * S ((dst_positive_code_column_value_gridentrysource) + (dst_positive_scale_column_value_gridentrysource)) + ((dst_positive_scale_column_value_gridentrysource) + (dst_positive_scale_column_value_gridentrysource))) + (((dst_negative_code_column_value_gridentrysource) + (dst_negative_scale_column_value_gridentrysource)) * S ((dst_negative_code_column_value_gridentrysource) + (dst_negative_scale_column_value_gridentrysource)) + ((dst_negative_scale_column_value_gridentrysource) + (dst_negative_scale_column_value_gridentrysource)))) + ((((dst_negative_code_column_value_gridentrysource) + (dst_negative_scale_column_value_gridentrysource)) * S ((dst_negative_code_column_value_gridentrysource) + (dst_negative_scale_column_value_gridentrysource)) + ((dst_negative_scale_column_value_gridentrysource) + (dst_negative_scale_column_value_gridentrysource))) + (((dst_negative_code_column_value_gridentrysource) + (dst_negative_scale_column_value_gridentrysource)) * S ((dst_negative_code_column_value_gridentrysource) + (dst_negative_scale_column_value_gridentrysource)) + ((dst_negative_scale_column_value_gridentrysource) + (dst_negative_scale_column_value_gridentrysource)))))) /\ (((((exists ff_h_pvs_column_value_gridentrysourcepositive. ff_h_pvs_column_value_gridentrysourcepositive + S (dst_positive_column_value_gridentrysource) = S ((S (ssr_grid_row_column_value_grid)) * dst_positive_scale_column_value_gridentrysource)) /\ exists ff_q_pvs_column_value_gridentrysourcepositive. dst_positive_code_column_value_gridentrysource = ff_q_pvs_column_value_gridentrysourcepositive * S ((S (ssr_grid_row_column_value_grid)) * dst_positive_scale_column_value_gridentrysource) + (dst_positive_column_value_gridentrysource))) /\ (((((exists ff_h_pvs_column_value_gridentrysourcenegative. ff_h_pvs_column_value_gridentrysourcenegative + S (dst_negative_column_value_gridentrysource) = S ((S (ssr_grid_row_column_value_grid)) * dst_negative_scale_column_value_gridentrysource)) /\ exists ff_q_pvs_column_value_gridentrysourcenegative. dst_negative_code_column_value_gridentrysource = ff_q_pvs_column_value_gridentrysourcenegative * S ((S (ssr_grid_row_column_value_grid)) * dst_negative_scale_column_value_gridentrysource) + (dst_negative_column_value_gridentrysource))) /\ (exists ge_balance_positive_column_value_gridentrysourcevalue ge_balance_negative_column_value_gridentrysourcevalue. (((((ssr_entry_value_column_value_gridentry) = 2 * (ge_balance_positive_column_value_gridentrysourcevalue) /\ (ge_balance_negative_column_value_gridentrysourcevalue) = 0) \/ exists ge_signed_half_column_value_gridentrysourcevaluedecode. (((ssr_entry_value_column_value_gridentry) = 2 * ge_signed_half_column_value_gridentrysourcevaluedecode + 1 /\ (ge_balance_positive_column_value_gridentrysourcevalue) = 0) /\ (ge_balance_negative_column_value_gridentrysourcevalue) = S ge_signed_half_column_value_gridentrysourcevaluedecode))) /\ ((dst_positive_column_value_gridentrysource) + ge_balance_negative_column_value_gridentrysourcevalue = (dst_negative_column_value_gridentrysource) + ge_balance_positive_column_value_gridentrysourcevalue))))))))) /\ (((((exists ff_h_pvs_column_value_gridentrymap. ff_h_pvs_column_value_gridentrymap + S (ssr_entry_image_column_value_gridentry) = S ((S (ssr_grid_row_column_value_grid)) * s)) /\ exists ff_q_pvs_column_value_gridentrymap. r = ff_q_pvs_column_value_gridentrymap * S ((S (ssr_grid_row_column_value_grid)) * s) + (ssr_entry_image_column_value_gridentry))) /\ (((((ssr_grid_column_column_value_grid)=(ssr_entry_image_column_value_gridentry)) /\ ((ssr_grid_value_column_value_grid)=(ssr_entry_value_column_value_gridentry)))) \/ (((~((ssr_grid_column_column_value_grid)=(ssr_entry_image_column_value_gridentry))) /\ ((ssr_grid_value_column_value_grid)=0))))))))))))) -> (exists pvs_gap_column_value_bound. pvs_gap_column_value_bound + S (j) = (M)) -> (exists dst_positive_code_column_value_target dst_positive_scale_column_value_target dst_negative_code_column_value_target dst_negative_scale_column_value_target dst_positive_column_value_target dst_negative_column_value_target. (((B) = (((((dst_positive_code_column_value_target) + (dst_positive_scale_column_value_target)) * S ((dst_positive_code_column_value_target) + (dst_positive_scale_column_value_target)) + ((dst_positive_scale_column_value_target) + (dst_positive_scale_column_value_target))) + (((dst_negative_code_column_value_target) + (dst_negative_scale_column_value_target)) * S ((dst_negative_code_column_value_target) + (dst_negative_scale_column_value_target)) + ((dst_negative_scale_column_value_target) + (dst_negative_scale_column_value_target)))) * S ((((dst_positive_code_column_value_target) + (dst_positive_scale_column_value_target)) * S ((dst_positive_code_column_value_target) + (dst_positive_scale_column_value_target)) + ((dst_positive_scale_column_value_target) + (dst_positive_scale_column_value_target))) + (((dst_negative_code_column_value_target) + (dst_negative_scale_column_value_target)) * S ((dst_negative_code_column_value_target) + (dst_negative_scale_column_value_target)) + ((dst_negative_scale_column_value_target) + (dst_negative_scale_column_value_target)))) + ((((dst_negative_code_column_value_target) + (dst_negative_scale_column_value_target)) * S ((dst_negative_code_column_value_target) + (dst_negative_scale_column_value_target)) + ((dst_negative_scale_column_value_target) + (dst_negative_scale_column_value_target))) + (((dst_negative_code_column_value_target) + (dst_negative_scale_column_value_target)) * S ((dst_negative_code_column_value_target) + (dst_negative_scale_column_value_target)) + ((dst_negative_scale_column_value_target) + (dst_negative_scale_column_value_target)))))) /\ (((((exists ff_h_pvs_column_value_targetpositive. ff_h_pvs_column_value_targetpositive + S (dst_positive_column_value_target) = S ((S (j)) * dst_positive_scale_column_value_target)) /\ exists ff_q_pvs_column_value_targetpositive. dst_positive_code_column_value_target = ff_q_pvs_column_value_targetpositive * S ((S (j)) * dst_positive_scale_column_value_target) + (dst_positive_column_value_target))) /\ (((((exists ff_h_pvs_column_value_targetnegative. ff_h_pvs_column_value_targetnegative + S (dst_negative_column_value_target) = S ((S (j)) * dst_negative_scale_column_value_target)) /\ exists ff_q_pvs_column_value_targetnegative. dst_negative_code_column_value_target = ff_q_pvs_column_value_targetnegative * S ((S (j)) * dst_negative_scale_column_value_target) + (dst_negative_column_value_target))) /\ (exists ge_balance_positive_column_value_targetvalue ge_balance_negative_column_value_targetvalue. (((((b) = 2 * (ge_balance_positive_column_value_targetvalue) /\ (ge_balance_negative_column_value_targetvalue) = 0) \/ exists ge_signed_half_column_value_targetvaluedecode. (((b) = 2 * ge_signed_half_column_value_targetvaluedecode + 1 /\ (ge_balance_positive_column_value_targetvalue) = 0) /\ (ge_balance_negative_column_value_targetvalue) = S ge_signed_half_column_value_targetvaluedecode))) /\ ((dst_positive_column_value_target) + ge_balance_negative_column_value_targetvalue = (dst_negative_column_value_target) + ge_balance_positive_column_value_targetvalue))))))))) -> (exists srs_slice_column_value_sum. ((((exists dst_positive_code_column_value_sumslicesource_table dst_positive_scale_column_value_sumslicesource_table dst_negative_code_column_value_sumslicesource_table dst_negative_scale_column_value_sumslicesource_table. (((T) = (((((dst_positive_code_column_value_sumslicesource_table) + (dst_positive_scale_column_value_sumslicesource_table)) * S ((dst_positive_code_column_value_sumslicesource_table) + (dst_positive_scale_column_value_sumslicesource_table)) + ((dst_positive_scale_column_value_sumslicesource_table) + (dst_positive_scale_column_value_sumslicesource_table))) + (((dst_negative_code_column_value_sumslicesource_table) + (dst_negative_scale_column_value_sumslicesource_table)) * S ((dst_negative_code_column_value_sumslicesource_table) + (dst_negative_scale_column_value_sumslicesource_table)) + ((dst_negative_scale_column_value_sumslicesource_table) + (dst_negative_scale_column_value_sumslicesource_table)))) * S ((((dst_positive_code_column_value_sumslicesource_table) + (dst_positive_scale_column_value_sumslicesource_table)) * S ((dst_positive_code_column_value_sumslicesource_table) + (dst_positive_scale_column_value_sumslicesource_table)) + ((dst_positive_scale_column_value_sumslicesource_table) + (dst_positive_scale_column_value_sumslicesource_table))) + (((dst_negative_code_column_value_sumslicesource_table) + (dst_negative_scale_column_value_sumslicesource_table)) * S ((dst_negative_code_column_value_sumslicesource_table) + (dst_negative_scale_column_value_sumslicesource_table)) + ((dst_negative_scale_column_value_sumslicesource_table) + (dst_negative_scale_column_value_sumslicesource_table)))) + ((((dst_negative_code_column_value_sumslicesource_table) + (dst_negative_scale_column_value_sumslicesource_table)) * S ((dst_negative_code_column_value_sumslicesource_table) + (dst_negative_scale_column_value_sumslicesource_table)) + ((dst_negative_scale_column_value_sumslicesource_table) + (dst_negative_scale_column_value_sumslicesource_table))) + (((dst_negative_code_column_value_sumslicesource_table) + (dst_negative_scale_column_value_sumslicesource_table)) * S ((dst_negative_code_column_value_sumslicesource_table) + (dst_negative_scale_column_value_sumslicesource_table)) + ((dst_negative_scale_column_value_sumslicesource_table) + (dst_negative_scale_column_value_sumslicesource_table)))))) /\ (forall dst_index_column_value_sumslicesource_table. (exists pvs_le_gap_column_value_sumslicesource_tabledomain. pvs_le_gap_column_value_sumslicesource_tabledomain + (dst_index_column_value_sumslicesource_table) = (0)) -> exists dst_positive_column_value_sumslicesource_table dst_negative_column_value_sumslicesource_table dst_value_column_value_sumslicesource_table. ((((exists ff_h_pvs_column_value_sumslicesource_tableentrypositive. ff_h_pvs_column_value_sumslicesource_tableentrypositive + S (dst_positive_column_value_sumslicesource_table) = S ((S (dst_index_column_value_sumslicesource_table)) * dst_positive_scale_column_value_sumslicesource_table)) /\ exists ff_q_pvs_column_value_sumslicesource_tableentrypositive. dst_positive_code_column_value_sumslicesource_table = ff_q_pvs_column_value_sumslicesource_tableentrypositive * S ((S (dst_index_column_value_sumslicesource_table)) * dst_positive_scale_column_value_sumslicesource_table) + (dst_positive_column_value_sumslicesource_table))) /\ (((((exists ff_h_pvs_column_value_sumslicesource_tableentrynegative. ff_h_pvs_column_value_sumslicesource_tableentrynegative + S (dst_negative_column_value_sumslicesource_table) = S ((S (dst_index_column_value_sumslicesource_table)) * dst_negative_scale_column_value_sumslicesource_table)) /\ exists ff_q_pvs_column_value_sumslicesource_tableentrynegative. dst_negative_code_column_value_sumslicesource_table = ff_q_pvs_column_value_sumslicesource_tableentrynegative * S ((S (dst_index_column_value_sumslicesource_table)) * dst_negative_scale_column_value_sumslicesource_table) + (dst_negative_column_value_sumslicesource_table))) /\ (exists ge_balance_positive_column_value_sumslicesource_tableentryvalue ge_balance_negative_column_value_sumslicesource_tableentryvalue. (((((dst_value_column_value_sumslicesource_table) = 2 * (ge_balance_positive_column_value_sumslicesource_tableentryvalue) /\ (ge_balance_negative_column_value_sumslicesource_tableentryvalue) = 0) \/ exists ge_signed_half_column_value_sumslicesource_tableentryvaluedecode. (((dst_value_column_value_sumslicesource_table) = 2 * ge_signed_half_column_value_sumslicesource_tableentryvaluedecode + 1 /\ (ge_balance_positive_column_value_sumslicesource_tableentryvalue) = 0) /\ (ge_balance_negative_column_value_sumslicesource_tableentryvalue) = S ge_signed_half_column_value_sumslicesource_tableentryvaluedecode))) /\ ((dst_positive_column_value_sumslicesource_table) + ge_balance_negative_column_value_sumslicesource_tableentryvalue = (dst_negative_column_value_sumslicesource_table) + ge_balance_positive_column_value_sumslicesource_tableentryvalue))))))))) /\ (((exists dst_positive_code_column_value_sumsliceoutput_table dst_positive_scale_column_value_sumsliceoutput_table dst_negative_code_column_value_sumsliceoutput_table dst_negative_scale_column_value_sumsliceoutput_table. (((srs_slice_column_value_sum) = (((((dst_positive_code_column_value_sumsliceoutput_table) + (dst_positive_scale_column_value_sumsliceoutput_table)) * S ((dst_positive_code_column_value_sumsliceoutput_table) + (dst_positive_scale_column_value_sumsliceoutput_table)) + ((dst_positive_scale_column_value_sumsliceoutput_table) + (dst_positive_scale_column_value_sumsliceoutput_table))) + (((dst_negative_code_column_value_sumsliceoutput_table) + (dst_negative_scale_column_value_sumsliceoutput_table)) * S ((dst_negative_code_column_value_sumsliceoutput_table) + (dst_negative_scale_column_value_sumsliceoutput_table)) + ((dst_negative_scale_column_value_sumsliceoutput_table) + (dst_negative_scale_column_value_sumsliceoutput_table)))) * S ((((dst_positive_code_column_value_sumsliceoutput_table) + (dst_positive_scale_column_value_sumsliceoutput_table)) * S ((dst_positive_code_column_value_sumsliceoutput_table) + (dst_positive_scale_column_value_sumsliceoutput_table)) + ((dst_positive_scale_column_value_sumsliceoutput_table) + (dst_positive_scale_column_value_sumsliceoutput_table))) + (((dst_negative_code_column_value_sumsliceoutput_table) + (dst_negative_scale_column_value_sumsliceoutput_table)) * S ((dst_negative_code_column_value_sumsliceoutput_table) + (dst_negative_scale_column_value_sumsliceoutput_table)) + ((dst_negative_scale_column_value_sumsliceoutput_table) + (dst_negative_scale_column_value_sumsliceoutput_table)))) + ((((dst_negative_code_column_value_sumsliceoutput_table) + (dst_negative_scale_column_value_sumsliceoutput_table)) * S ((dst_negative_code_column_value_sumsliceoutput_table) + (dst_negative_scale_column_value_sumsliceoutput_table)) + ((dst_negative_scale_column_value_sumsliceoutput_table) + (dst_negative_scale_column_value_sumsliceoutput_table))) + (((dst_negative_code_column_value_sumsliceoutput_table) + (dst_negative_scale_column_value_sumsliceoutput_table)) * S ((dst_negative_code_column_value_sumsliceoutput_table) + (dst_negative_scale_column_value_sumsliceoutput_table)) + ((dst_negative_scale_column_value_sumsliceoutput_table) + (dst_negative_scale_column_value_sumsliceoutput_table)))))) /\ (forall dst_index_column_value_sumsliceoutput_table. (exists pvs_le_gap_column_value_sumsliceoutput_tabledomain. pvs_le_gap_column_value_sumsliceoutput_tabledomain + (dst_index_column_value_sumsliceoutput_table) = (L)) -> exists dst_positive_column_value_sumsliceoutput_table dst_negative_column_value_sumsliceoutput_table dst_value_column_value_sumsliceoutput_table. ((((exists ff_h_pvs_column_value_sumsliceoutput_tableentrypositive. ff_h_pvs_column_value_sumsliceoutput_tableentrypositive + S (dst_positive_column_value_sumsliceoutput_table) = S ((S (dst_index_column_value_sumsliceoutput_table)) * dst_positive_scale_column_value_sumsliceoutput_table)) /\ exists ff_q_pvs_column_value_sumsliceoutput_tableentrypositive. dst_positive_code_column_value_sumsliceoutput_table = ff_q_pvs_column_value_sumsliceoutput_tableentrypositive * S ((S (dst_index_column_value_sumsliceoutput_table)) * dst_positive_scale_column_value_sumsliceoutput_table) + (dst_positive_column_value_sumsliceoutput_table))) /\ (((((exists ff_h_pvs_column_value_sumsliceoutput_tableentrynegative. ff_h_pvs_column_value_sumsliceoutput_tableentrynegative + S (dst_negative_column_value_sumsliceoutput_table) = S ((S (dst_index_column_value_sumsliceoutput_table)) * dst_negative_scale_column_value_sumsliceoutput_table)) /\ exists ff_q_pvs_column_value_sumsliceoutput_tableentrynegative. dst_negative_code_column_value_sumsliceoutput_table = ff_q_pvs_column_value_sumsliceoutput_tableentrynegative * S ((S (dst_index_column_value_sumsliceoutput_table)) * dst_negative_scale_column_value_sumsliceoutput_table) + (dst_negative_column_value_sumsliceoutput_table))) /\ (exists ge_balance_positive_column_value_sumsliceoutput_tableentryvalue ge_balance_negative_column_value_sumsliceoutput_tableentryvalue. (((((dst_value_column_value_sumsliceoutput_table) = 2 * (ge_balance_positive_column_value_sumsliceoutput_tableentryvalue) /\ (ge_balance_negative_column_value_sumsliceoutput_tableentryvalue) = 0) \/ exists ge_signed_half_column_value_sumsliceoutput_tableentryvaluedecode. (((dst_value_column_value_sumsliceoutput_table) = 2 * ge_signed_half_column_value_sumsliceoutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_column_value_sumsliceoutput_tableentryvalue) = 0) /\ (ge_balance_negative_column_value_sumsliceoutput_tableentryvalue) = S ge_signed_half_column_value_sumsliceoutput_tableentryvaluedecode))) /\ ((dst_positive_column_value_sumsliceoutput_table) + ge_balance_negative_column_value_sumsliceoutput_tableentryvalue = (dst_negative_column_value_sumsliceoutput_table) + ge_balance_positive_column_value_sumsliceoutput_tableentryvalue))))))))) /\ (forall srs_index_column_value_sumslice. (exists pvs_gap_column_value_sumslicebound. pvs_gap_column_value_sumslicebound + S (srs_index_column_value_sumslice) = (L)) -> exists srs_value_column_value_sumslice. (((exists dst_positive_code_column_value_sumsliceentrysource dst_positive_scale_column_value_sumsliceentrysource dst_negative_code_column_value_sumsliceentrysource dst_negative_scale_column_value_sumsliceentrysource dst_positive_column_value_sumsliceentrysource dst_negative_column_value_sumsliceentrysource. (((T) = (((((dst_positive_code_column_value_sumsliceentrysource) + (dst_positive_scale_column_value_sumsliceentrysource)) * S ((dst_positive_code_column_value_sumsliceentrysource) + (dst_positive_scale_column_value_sumsliceentrysource)) + ((dst_positive_scale_column_value_sumsliceentrysource) + (dst_positive_scale_column_value_sumsliceentrysource))) + (((dst_negative_code_column_value_sumsliceentrysource) + (dst_negative_scale_column_value_sumsliceentrysource)) * S ((dst_negative_code_column_value_sumsliceentrysource) + (dst_negative_scale_column_value_sumsliceentrysource)) + ((dst_negative_scale_column_value_sumsliceentrysource) + (dst_negative_scale_column_value_sumsliceentrysource)))) * S ((((dst_positive_code_column_value_sumsliceentrysource) + (dst_positive_scale_column_value_sumsliceentrysource)) * S ((dst_positive_code_column_value_sumsliceentrysource) + (dst_positive_scale_column_value_sumsliceentrysource)) + ((dst_positive_scale_column_value_sumsliceentrysource) + (dst_positive_scale_column_value_sumsliceentrysource))) + (((dst_negative_code_column_value_sumsliceentrysource) + (dst_negative_scale_column_value_sumsliceentrysource)) * S ((dst_negative_code_column_value_sumsliceentrysource) + (dst_negative_scale_column_value_sumsliceentrysource)) + ((dst_negative_scale_column_value_sumsliceentrysource) + (dst_negative_scale_column_value_sumsliceentrysource)))) + ((((dst_negative_code_column_value_sumsliceentrysource) + (dst_negative_scale_column_value_sumsliceentrysource)) * S ((dst_negative_code_column_value_sumsliceentrysource) + (dst_negative_scale_column_value_sumsliceentrysource)) + ((dst_negative_scale_column_value_sumsliceentrysource) + (dst_negative_scale_column_value_sumsliceentrysource))) + (((dst_negative_code_column_value_sumsliceentrysource) + (dst_negative_scale_column_value_sumsliceentrysource)) * S ((dst_negative_code_column_value_sumsliceentrysource) + (dst_negative_scale_column_value_sumsliceentrysource)) + ((dst_negative_scale_column_value_sumsliceentrysource) + (dst_negative_scale_column_value_sumsliceentrysource)))))) /\ (((((exists ff_h_pvs_column_value_sumsliceentrysourcepositive. ff_h_pvs_column_value_sumsliceentrysourcepositive + S (dst_positive_column_value_sumsliceentrysource) = S ((S (((((0) + ((1) * (j)))) + ((S M) * (srs_index_column_value_sumslice))))) * dst_positive_scale_column_value_sumsliceentrysource)) /\ exists ff_q_pvs_column_value_sumsliceentrysourcepositive. dst_positive_code_column_value_sumsliceentrysource = ff_q_pvs_column_value_sumsliceentrysourcepositive * S ((S (((((0) + ((1) * (j)))) + ((S M) * (srs_index_column_value_sumslice))))) * dst_positive_scale_column_value_sumsliceentrysource) + (dst_positive_column_value_sumsliceentrysource))) /\ (((((exists ff_h_pvs_column_value_sumsliceentrysourcenegative. ff_h_pvs_column_value_sumsliceentrysourcenegative + S (dst_negative_column_value_sumsliceentrysource) = S ((S (((((0) + ((1) * (j)))) + ((S M) * (srs_index_column_value_sumslice))))) * dst_negative_scale_column_value_sumsliceentrysource)) /\ exists ff_q_pvs_column_value_sumsliceentrysourcenegative. dst_negative_code_column_value_sumsliceentrysource = ff_q_pvs_column_value_sumsliceentrysourcenegative * S ((S (((((0) + ((1) * (j)))) + ((S M) * (srs_index_column_value_sumslice))))) * dst_negative_scale_column_value_sumsliceentrysource) + (dst_negative_column_value_sumsliceentrysource))) /\ (exists ge_balance_positive_column_value_sumsliceentrysourcevalue ge_balance_negative_column_value_sumsliceentrysourcevalue. (((((srs_value_column_value_sumslice) = 2 * (ge_balance_positive_column_value_sumsliceentrysourcevalue) /\ (ge_balance_negative_column_value_sumsliceentrysourcevalue) = 0) \/ exists ge_signed_half_column_value_sumsliceentrysourcevaluedecode. (((srs_value_column_value_sumslice) = 2 * ge_signed_half_column_value_sumsliceentrysourcevaluedecode + 1 /\ (ge_balance_positive_column_value_sumsliceentrysourcevalue) = 0) /\ (ge_balance_negative_column_value_sumsliceentrysourcevalue) = S ge_signed_half_column_value_sumsliceentrysourcevaluedecode))) /\ ((dst_positive_column_value_sumsliceentrysource) + ge_balance_negative_column_value_sumsliceentrysourcevalue = (dst_negative_column_value_sumsliceentrysource) + ge_balance_positive_column_value_sumsliceentrysourcevalue))))))))) /\ (exists dst_positive_code_column_value_sumsliceentryoutput dst_positive_scale_column_value_sumsliceentryoutput dst_negative_code_column_value_sumsliceentryoutput dst_negative_scale_column_value_sumsliceentryoutput dst_positive_column_value_sumsliceentryoutput dst_negative_column_value_sumsliceentryoutput. (((srs_slice_column_value_sum) = (((((dst_positive_code_column_value_sumsliceentryoutput) + (dst_positive_scale_column_value_sumsliceentryoutput)) * S ((dst_positive_code_column_value_sumsliceentryoutput) + (dst_positive_scale_column_value_sumsliceentryoutput)) + ((dst_positive_scale_column_value_sumsliceentryoutput) + (dst_positive_scale_column_value_sumsliceentryoutput))) + (((dst_negative_code_column_value_sumsliceentryoutput) + (dst_negative_scale_column_value_sumsliceentryoutput)) * S ((dst_negative_code_column_value_sumsliceentryoutput) + (dst_negative_scale_column_value_sumsliceentryoutput)) + ((dst_negative_scale_column_value_sumsliceentryoutput) + (dst_negative_scale_column_value_sumsliceentryoutput)))) * S ((((dst_positive_code_column_value_sumsliceentryoutput) + (dst_positive_scale_column_value_sumsliceentryoutput)) * S ((dst_positive_code_column_value_sumsliceentryoutput) + (dst_positive_scale_column_value_sumsliceentryoutput)) + ((dst_positive_scale_column_value_sumsliceentryoutput) + (dst_positive_scale_column_value_sumsliceentryoutput))) + (((dst_negative_code_column_value_sumsliceentryoutput) + (dst_negative_scale_column_value_sumsliceentryoutput)) * S ((dst_negative_code_column_value_sumsliceentryoutput) + (dst_negative_scale_column_value_sumsliceentryoutput)) + ((dst_negative_scale_column_value_sumsliceentryoutput) + (dst_negative_scale_column_value_sumsliceentryoutput)))) + ((((dst_negative_code_column_value_sumsliceentryoutput) + (dst_negative_scale_column_value_sumsliceentryoutput)) * S ((dst_negative_code_column_value_sumsliceentryoutput) + (dst_negative_scale_column_value_sumsliceentryoutput)) + ((dst_negative_scale_column_value_sumsliceentryoutput) + (dst_negative_scale_column_value_sumsliceentryoutput))) + (((dst_negative_code_column_value_sumsliceentryoutput) + (dst_negative_scale_column_value_sumsliceentryoutput)) * S ((dst_negative_code_column_value_sumsliceentryoutput) + (dst_negative_scale_column_value_sumsliceentryoutput)) + ((dst_negative_scale_column_value_sumsliceentryoutput) + (dst_negative_scale_column_value_sumsliceentryoutput)))))) /\ (((((exists ff_h_pvs_column_value_sumsliceentryoutputpositive. ff_h_pvs_column_value_sumsliceentryoutputpositive + S (dst_positive_column_value_sumsliceentryoutput) = S ((S (srs_index_column_value_sumslice)) * dst_positive_scale_column_value_sumsliceentryoutput)) /\ exists ff_q_pvs_column_value_sumsliceentryoutputpositive. dst_positive_code_column_value_sumsliceentryoutput = ff_q_pvs_column_value_sumsliceentryoutputpositive * S ((S (srs_index_column_value_sumslice)) * dst_positive_scale_column_value_sumsliceentryoutput) + (dst_positive_column_value_sumsliceentryoutput))) /\ (((((exists ff_h_pvs_column_value_sumsliceentryoutputnegative. ff_h_pvs_column_value_sumsliceentryoutputnegative + S (dst_negative_column_value_sumsliceentryoutput) = S ((S (srs_index_column_value_sumslice)) * dst_negative_scale_column_value_sumsliceentryoutput)) /\ exists ff_q_pvs_column_value_sumsliceentryoutputnegative. dst_negative_code_column_value_sumsliceentryoutput = ff_q_pvs_column_value_sumsliceentryoutputnegative * S ((S (srs_index_column_value_sumslice)) * dst_negative_scale_column_value_sumsliceentryoutput) + (dst_negative_column_value_sumsliceentryoutput))) /\ (exists ge_balance_positive_column_value_sumsliceentryoutputvalue ge_balance_negative_column_value_sumsliceentryoutputvalue. (((((srs_value_column_value_sumslice) = 2 * (ge_balance_positive_column_value_sumsliceentryoutputvalue) /\ (ge_balance_negative_column_value_sumsliceentryoutputvalue) = 0) \/ exists ge_signed_half_column_value_sumsliceentryoutputvaluedecode. (((srs_value_column_value_sumslice) = 2 * ge_signed_half_column_value_sumsliceentryoutputvaluedecode + 1 /\ (ge_balance_positive_column_value_sumsliceentryoutputvalue) = 0) /\ (ge_balance_negative_column_value_sumsliceentryoutputvalue) = S ge_signed_half_column_value_sumsliceentryoutputvaluedecode))) /\ ((dst_positive_column_value_sumsliceentryoutput) + ge_balance_negative_column_value_sumsliceentryoutputvalue = (dst_negative_column_value_sumsliceentryoutput) + ge_balance_positive_column_value_sumsliceentryoutputvalue)))))))))))))))) /\ (exists dst_positive_code_column_value_sumsum dst_positive_scale_column_value_sumsum dst_negative_code_column_value_sumsum dst_negative_scale_column_value_sumsum dst_positive_sum_column_value_sumsum dst_negative_sum_column_value_sumsum. (((srs_slice_column_value_sum) = (((((dst_positive_code_column_value_sumsum) + (dst_positive_scale_column_value_sumsum)) * S ((dst_positive_code_column_value_sumsum) + (dst_positive_scale_column_value_sumsum)) + ((dst_positive_scale_column_value_sumsum) + (dst_positive_scale_column_value_sumsum))) + (((dst_negative_code_column_value_sumsum) + (dst_negative_scale_column_value_sumsum)) * S ((dst_negative_code_column_value_sumsum) + (dst_negative_scale_column_value_sumsum)) + ((dst_negative_scale_column_value_sumsum) + (dst_negative_scale_column_value_sumsum)))) * S ((((dst_positive_code_column_value_sumsum) + (dst_positive_scale_column_value_sumsum)) * S ((dst_positive_code_column_value_sumsum) + (dst_positive_scale_column_value_sumsum)) + ((dst_positive_scale_column_value_sumsum) + (dst_positive_scale_column_value_sumsum))) + (((dst_negative_code_column_value_sumsum) + (dst_negative_scale_column_value_sumsum)) * S ((dst_negative_code_column_value_sumsum) + (dst_negative_scale_column_value_sumsum)) + ((dst_negative_scale_column_value_sumsum) + (dst_negative_scale_column_value_sumsum)))) + ((((dst_negative_code_column_value_sumsum) + (dst_negative_scale_column_value_sumsum)) * S ((dst_negative_code_column_value_sumsum) + (dst_negative_scale_column_value_sumsum)) + ((dst_negative_scale_column_value_sumsum) + (dst_negative_scale_column_value_sumsum))) + (((dst_negative_code_column_value_sumsum) + (dst_negative_scale_column_value_sumsum)) * S ((dst_negative_code_column_value_sumsum) + (dst_negative_scale_column_value_sumsum)) + ((dst_negative_scale_column_value_sumsum) + (dst_negative_scale_column_value_sumsum)))))) /\ (((exists fs_u_dst_column_value_sumsumpositive fs_v_dst_column_value_sumsumpositive. ((((exists fs_h_dst_column_value_sumsumpositive_body_start. fs_h_dst_column_value_sumsumpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_column_value_sumsumpositive)) /\ exists fs_q_dst_column_value_sumsumpositive_body_start. fs_u_dst_column_value_sumsumpositive = fs_q_dst_column_value_sumsumpositive_body_start * S ((S (0)) * fs_v_dst_column_value_sumsumpositive) + (0))) /\ ((((exists fs_h_dst_column_value_sumsumpositive_body_terminal. fs_h_dst_column_value_sumsumpositive_body_terminal + S (dst_positive_sum_column_value_sumsum) = S ((S (L)) * fs_v_dst_column_value_sumsumpositive)) /\ exists fs_q_dst_column_value_sumsumpositive_body_terminal. fs_u_dst_column_value_sumsumpositive = fs_q_dst_column_value_sumsumpositive_body_terminal * S ((S (L)) * fs_v_dst_column_value_sumsumpositive) + (dst_positive_sum_column_value_sumsum))) /\ forall fs_i_dst_column_value_sumsumpositive_body_steps. (exists fs_lt_dst_column_value_sumsumpositive_body_steps_bound. fs_lt_dst_column_value_sumsumpositive_body_steps_bound + S fs_i_dst_column_value_sumsumpositive_body_steps = L) -> exists fs_a_dst_column_value_sumsumpositive_body_steps fs_r_dst_column_value_sumsumpositive_body_steps fs_s_dst_column_value_sumsumpositive_body_steps. ((((exists fs_h_dst_column_value_sumsumpositive_body_steps_summand. fs_h_dst_column_value_sumsumpositive_body_steps_summand + S (fs_a_dst_column_value_sumsumpositive_body_steps) = S ((S (fs_i_dst_column_value_sumsumpositive_body_steps)) * dst_positive_scale_column_value_sumsum)) /\ exists fs_q_dst_column_value_sumsumpositive_body_steps_summand. dst_positive_code_column_value_sumsum = fs_q_dst_column_value_sumsumpositive_body_steps_summand * S ((S (fs_i_dst_column_value_sumsumpositive_body_steps)) * dst_positive_scale_column_value_sumsum) + (fs_a_dst_column_value_sumsumpositive_body_steps))) /\ ((((exists fs_h_dst_column_value_sumsumpositive_body_steps_partial. fs_h_dst_column_value_sumsumpositive_body_steps_partial + S (fs_r_dst_column_value_sumsumpositive_body_steps) = S ((S (fs_i_dst_column_value_sumsumpositive_body_steps)) * fs_v_dst_column_value_sumsumpositive)) /\ exists fs_q_dst_column_value_sumsumpositive_body_steps_partial. fs_u_dst_column_value_sumsumpositive = fs_q_dst_column_value_sumsumpositive_body_steps_partial * S ((S (fs_i_dst_column_value_sumsumpositive_body_steps)) * fs_v_dst_column_value_sumsumpositive) + (fs_r_dst_column_value_sumsumpositive_body_steps))) /\ ((((exists fs_h_dst_column_value_sumsumpositive_body_steps_successor. fs_h_dst_column_value_sumsumpositive_body_steps_successor + S (fs_s_dst_column_value_sumsumpositive_body_steps) = S ((S (S fs_i_dst_column_value_sumsumpositive_body_steps)) * fs_v_dst_column_value_sumsumpositive)) /\ exists fs_q_dst_column_value_sumsumpositive_body_steps_successor. fs_u_dst_column_value_sumsumpositive = fs_q_dst_column_value_sumsumpositive_body_steps_successor * S ((S (S fs_i_dst_column_value_sumsumpositive_body_steps)) * fs_v_dst_column_value_sumsumpositive) + (fs_s_dst_column_value_sumsumpositive_body_steps))) /\ fs_s_dst_column_value_sumsumpositive_body_steps = fs_r_dst_column_value_sumsumpositive_body_steps + fs_a_dst_column_value_sumsumpositive_body_steps)))))) /\ (((exists fs_u_dst_column_value_sumsumnegative fs_v_dst_column_value_sumsumnegative. ((((exists fs_h_dst_column_value_sumsumnegative_body_start. fs_h_dst_column_value_sumsumnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_column_value_sumsumnegative)) /\ exists fs_q_dst_column_value_sumsumnegative_body_start. fs_u_dst_column_value_sumsumnegative = fs_q_dst_column_value_sumsumnegative_body_start * S ((S (0)) * fs_v_dst_column_value_sumsumnegative) + (0))) /\ ((((exists fs_h_dst_column_value_sumsumnegative_body_terminal. fs_h_dst_column_value_sumsumnegative_body_terminal + S (dst_negative_sum_column_value_sumsum) = S ((S (L)) * fs_v_dst_column_value_sumsumnegative)) /\ exists fs_q_dst_column_value_sumsumnegative_body_terminal. fs_u_dst_column_value_sumsumnegative = fs_q_dst_column_value_sumsumnegative_body_terminal * S ((S (L)) * fs_v_dst_column_value_sumsumnegative) + (dst_negative_sum_column_value_sumsum))) /\ forall fs_i_dst_column_value_sumsumnegative_body_steps. (exists fs_lt_dst_column_value_sumsumnegative_body_steps_bound. fs_lt_dst_column_value_sumsumnegative_body_steps_bound + S fs_i_dst_column_value_sumsumnegative_body_steps = L) -> exists fs_a_dst_column_value_sumsumnegative_body_steps fs_r_dst_column_value_sumsumnegative_body_steps fs_s_dst_column_value_sumsumnegative_body_steps. ((((exists fs_h_dst_column_value_sumsumnegative_body_steps_summand. fs_h_dst_column_value_sumsumnegative_body_steps_summand + S (fs_a_dst_column_value_sumsumnegative_body_steps) = S ((S (fs_i_dst_column_value_sumsumnegative_body_steps)) * dst_negative_scale_column_value_sumsum)) /\ exists fs_q_dst_column_value_sumsumnegative_body_steps_summand. dst_negative_code_column_value_sumsum = fs_q_dst_column_value_sumsumnegative_body_steps_summand * S ((S (fs_i_dst_column_value_sumsumnegative_body_steps)) * dst_negative_scale_column_value_sumsum) + (fs_a_dst_column_value_sumsumnegative_body_steps))) /\ ((((exists fs_h_dst_column_value_sumsumnegative_body_steps_partial. fs_h_dst_column_value_sumsumnegative_body_steps_partial + S (fs_r_dst_column_value_sumsumnegative_body_steps) = S ((S (fs_i_dst_column_value_sumsumnegative_body_steps)) * fs_v_dst_column_value_sumsumnegative)) /\ exists fs_q_dst_column_value_sumsumnegative_body_steps_partial. fs_u_dst_column_value_sumsumnegative = fs_q_dst_column_value_sumsumnegative_body_steps_partial * S ((S (fs_i_dst_column_value_sumsumnegative_body_steps)) * fs_v_dst_column_value_sumsumnegative) + (fs_r_dst_column_value_sumsumnegative_body_steps))) /\ ((((exists fs_h_dst_column_value_sumsumnegative_body_steps_successor. fs_h_dst_column_value_sumsumnegative_body_steps_successor + S (fs_s_dst_column_value_sumsumnegative_body_steps) = S ((S (S fs_i_dst_column_value_sumsumnegative_body_steps)) * fs_v_dst_column_value_sumsumnegative)) /\ exists fs_q_dst_column_value_sumsumnegative_body_steps_successor. fs_u_dst_column_value_sumsumnegative = fs_q_dst_column_value_sumsumnegative_body_steps_successor * S ((S (S fs_i_dst_column_value_sumsumnegative_body_steps)) * fs_v_dst_column_value_sumsumnegative) + (fs_s_dst_column_value_sumsumnegative_body_steps))) /\ fs_s_dst_column_value_sumsumnegative_body_steps = fs_r_dst_column_value_sumsumnegative_body_steps + fs_a_dst_column_value_sumsumnegative_body_steps)))))) /\ (exists ge_balance_positive_column_value_sumsumresult ge_balance_negative_column_value_sumsumresult. (((((z) = 2 * (ge_balance_positive_column_value_sumsumresult) /\ (ge_balance_negative_column_value_sumsumresult) = 0) \/ exists ge_signed_half_column_value_sumsumresultdecode. (((z) = 2 * ge_signed_half_column_value_sumsumresultdecode + 1 /\ (ge_balance_positive_column_value_sumsumresult) = 0) /\ (ge_balance_negative_column_value_sumsumresult) = S ge_signed_half_column_value_sumsumresultdecode))) /\ ((dst_positive_sum_column_value_sumsum) + ge_balance_negative_column_value_sumsumresult = (dst_negative_sum_column_value_sumsum) + ge_balance_positive_column_value_sumsumresult))))))))))) -> z=b