signed_support_incidence_column_sums_equal

Exact expanded first-order arithmetic statement

forall A B r s L M T C. (((exists dst_positive_code_column_equal_supportsource_table dst_positive_scale_column_equal_supportsource_table dst_negative_code_column_equal_supportsource_table dst_negative_scale_column_equal_supportsource_table. (((A) = (((((dst_positive_code_column_equal_supportsource_table) + (dst_positive_scale_column_equal_supportsource_table)) * S ((dst_positive_code_column_equal_supportsource_table) + (dst_positive_scale_column_equal_supportsource_table)) + ((dst_positive_scale_column_equal_supportsource_table) + (dst_positive_scale_column_equal_supportsource_table))) + (((dst_negative_code_column_equal_supportsource_table) + (dst_negative_scale_column_equal_supportsource_table)) * S ((dst_negative_code_column_equal_supportsource_table) + (dst_negative_scale_column_equal_supportsource_table)) + ((dst_negative_scale_column_equal_supportsource_table) + (dst_negative_scale_column_equal_supportsource_table)))) * S ((((dst_positive_code_column_equal_supportsource_table) + (dst_positive_scale_column_equal_supportsource_table)) * S ((dst_positive_code_column_equal_supportsource_table) + (dst_positive_scale_column_equal_supportsource_table)) + ((dst_positive_scale_column_equal_supportsource_table) + (dst_positive_scale_column_equal_supportsource_table))) + (((dst_negative_code_column_equal_supportsource_table) + (dst_negative_scale_column_equal_supportsource_table)) * S ((dst_negative_code_column_equal_supportsource_table) + (dst_negative_scale_column_equal_supportsource_table)) + ((dst_negative_scale_column_equal_supportsource_table) + (dst_negative_scale_column_equal_supportsource_table)))) + ((((dst_negative_code_column_equal_supportsource_table) + (dst_negative_scale_column_equal_supportsource_table)) * S ((dst_negative_code_column_equal_supportsource_table) + (dst_negative_scale_column_equal_supportsource_table)) + ((dst_negative_scale_column_equal_supportsource_table) + (dst_negative_scale_column_equal_supportsource_table))) + (((dst_negative_code_column_equal_supportsource_table) + (dst_negative_scale_column_equal_supportsource_table)) * S ((dst_negative_code_column_equal_supportsource_table) + (dst_negative_scale_column_equal_supportsource_table)) + ((dst_negative_scale_column_equal_supportsource_table) + (dst_negative_scale_column_equal_supportsource_table)))))) /\ (forall dst_index_column_equal_supportsource_table. (exists pvs_le_gap_column_equal_supportsource_tabledomain. pvs_le_gap_column_equal_supportsource_tabledomain + (dst_index_column_equal_supportsource_table) = (0)) -> exists dst_positive_column_equal_supportsource_table dst_negative_column_equal_supportsource_table dst_value_column_equal_supportsource_table. ((((exists ff_h_pvs_column_equal_supportsource_tableentrypositive. ff_h_pvs_column_equal_supportsource_tableentrypositive + S (dst_positive_column_equal_supportsource_table) = S ((S (dst_index_column_equal_supportsource_table)) * dst_positive_scale_column_equal_supportsource_table)) /\ exists ff_q_pvs_column_equal_supportsource_tableentrypositive. dst_positive_code_column_equal_supportsource_table = ff_q_pvs_column_equal_supportsource_tableentrypositive * S ((S (dst_index_column_equal_supportsource_table)) * dst_positive_scale_column_equal_supportsource_table) + (dst_positive_column_equal_supportsource_table))) /\ (((((exists ff_h_pvs_column_equal_supportsource_tableentrynegative. ff_h_pvs_column_equal_supportsource_tableentrynegative + S (dst_negative_column_equal_supportsource_table) = S ((S (dst_index_column_equal_supportsource_table)) * dst_negative_scale_column_equal_supportsource_table)) /\ exists ff_q_pvs_column_equal_supportsource_tableentrynegative. dst_negative_code_column_equal_supportsource_table = ff_q_pvs_column_equal_supportsource_tableentrynegative * S ((S (dst_index_column_equal_supportsource_table)) * dst_negative_scale_column_equal_supportsource_table) + (dst_negative_column_equal_supportsource_table))) /\ (exists ge_balance_positive_column_equal_supportsource_tableentryvalue ge_balance_negative_column_equal_supportsource_tableentryvalue. (((((dst_value_column_equal_supportsource_table) = 2 * (ge_balance_positive_column_equal_supportsource_tableentryvalue) /\ (ge_balance_negative_column_equal_supportsource_tableentryvalue) = 0) \/ exists ge_signed_half_column_equal_supportsource_tableentryvaluedecode. (((dst_value_column_equal_supportsource_table) = 2 * ge_signed_half_column_equal_supportsource_tableentryvaluedecode + 1 /\ (ge_balance_positive_column_equal_supportsource_tableentryvalue) = 0) /\ (ge_balance_negative_column_equal_supportsource_tableentryvalue) = S ge_signed_half_column_equal_supportsource_tableentryvaluedecode))) /\ ((dst_positive_column_equal_supportsource_table) + ge_balance_negative_column_equal_supportsource_tableentryvalue = (dst_negative_column_equal_supportsource_table) + ge_balance_positive_column_equal_supportsource_tableentryvalue))))))))) /\ (((exists dst_positive_code_column_equal_supporttarget_table dst_positive_scale_column_equal_supporttarget_table dst_negative_code_column_equal_supporttarget_table dst_negative_scale_column_equal_supporttarget_table. (((B) = (((((dst_positive_code_column_equal_supporttarget_table) + (dst_positive_scale_column_equal_supporttarget_table)) * S ((dst_positive_code_column_equal_supporttarget_table) + (dst_positive_scale_column_equal_supporttarget_table)) + ((dst_positive_scale_column_equal_supporttarget_table) + (dst_positive_scale_column_equal_supporttarget_table))) + (((dst_negative_code_column_equal_supporttarget_table) + (dst_negative_scale_column_equal_supporttarget_table)) * S ((dst_negative_code_column_equal_supporttarget_table) + (dst_negative_scale_column_equal_supporttarget_table)) + ((dst_negative_scale_column_equal_supporttarget_table) + (dst_negative_scale_column_equal_supporttarget_table)))) * S ((((dst_positive_code_column_equal_supporttarget_table) + (dst_positive_scale_column_equal_supporttarget_table)) * S ((dst_positive_code_column_equal_supporttarget_table) + (dst_positive_scale_column_equal_supporttarget_table)) + ((dst_positive_scale_column_equal_supporttarget_table) + (dst_positive_scale_column_equal_supporttarget_table))) + (((dst_negative_code_column_equal_supporttarget_table) + (dst_negative_scale_column_equal_supporttarget_table)) * S ((dst_negative_code_column_equal_supporttarget_table) + (dst_negative_scale_column_equal_supporttarget_table)) + ((dst_negative_scale_column_equal_supporttarget_table) + (dst_negative_scale_column_equal_supporttarget_table)))) + ((((dst_negative_code_column_equal_supporttarget_table) + (dst_negative_scale_column_equal_supporttarget_table)) * S ((dst_negative_code_column_equal_supporttarget_table) + (dst_negative_scale_column_equal_supporttarget_table)) + ((dst_negative_scale_column_equal_supporttarget_table) + (dst_negative_scale_column_equal_supporttarget_table))) + (((dst_negative_code_column_equal_supporttarget_table) + (dst_negative_scale_column_equal_supporttarget_table)) * S ((dst_negative_code_column_equal_supporttarget_table) + (dst_negative_scale_column_equal_supporttarget_table)) + ((dst_negative_scale_column_equal_supporttarget_table) + (dst_negative_scale_column_equal_supporttarget_table)))))) /\ (forall dst_index_column_equal_supporttarget_table. (exists pvs_le_gap_column_equal_supporttarget_tabledomain. pvs_le_gap_column_equal_supporttarget_tabledomain + (dst_index_column_equal_supporttarget_table) = (0)) -> exists dst_positive_column_equal_supporttarget_table dst_negative_column_equal_supporttarget_table dst_value_column_equal_supporttarget_table. ((((exists ff_h_pvs_column_equal_supporttarget_tableentrypositive. ff_h_pvs_column_equal_supporttarget_tableentrypositive + S (dst_positive_column_equal_supporttarget_table) = S ((S (dst_index_column_equal_supporttarget_table)) * dst_positive_scale_column_equal_supporttarget_table)) /\ exists ff_q_pvs_column_equal_supporttarget_tableentrypositive. dst_positive_code_column_equal_supporttarget_table = ff_q_pvs_column_equal_supporttarget_tableentrypositive * S ((S (dst_index_column_equal_supporttarget_table)) * dst_positive_scale_column_equal_supporttarget_table) + (dst_positive_column_equal_supporttarget_table))) /\ (((((exists ff_h_pvs_column_equal_supporttarget_tableentrynegative. ff_h_pvs_column_equal_supporttarget_tableentrynegative + S (dst_negative_column_equal_supporttarget_table) = S ((S (dst_index_column_equal_supporttarget_table)) * dst_negative_scale_column_equal_supporttarget_table)) /\ exists ff_q_pvs_column_equal_supporttarget_tableentrynegative. dst_negative_code_column_equal_supporttarget_table = ff_q_pvs_column_equal_supporttarget_tableentrynegative * S ((S (dst_index_column_equal_supporttarget_table)) * dst_negative_scale_column_equal_supporttarget_table) + (dst_negative_column_equal_supporttarget_table))) /\ (exists ge_balance_positive_column_equal_supporttarget_tableentryvalue ge_balance_negative_column_equal_supporttarget_tableentryvalue. (((((dst_value_column_equal_supporttarget_table) = 2 * (ge_balance_positive_column_equal_supporttarget_tableentryvalue) /\ (ge_balance_negative_column_equal_supporttarget_tableentryvalue) = 0) \/ exists ge_signed_half_column_equal_supporttarget_tableentryvaluedecode. (((dst_value_column_equal_supporttarget_table) = 2 * ge_signed_half_column_equal_supporttarget_tableentryvaluedecode + 1 /\ (ge_balance_positive_column_equal_supporttarget_tableentryvalue) = 0) /\ (ge_balance_negative_column_equal_supporttarget_tableentryvalue) = S ge_signed_half_column_equal_supporttarget_tableentryvaluedecode))) /\ ((dst_positive_column_equal_supporttarget_table) + ge_balance_negative_column_equal_supporttarget_tableentryvalue = (dst_negative_column_equal_supporttarget_table) + ge_balance_positive_column_equal_supporttarget_tableentryvalue))))))))) /\ (((forall ssr_source_column_equal_supportpreserve ssr_value_column_equal_supportpreserve. (exists pvs_gap_column_equal_supportpreservesource_bound. pvs_gap_column_equal_supportpreservesource_bound + S (ssr_source_column_equal_supportpreserve) = (L)) -> (exists dst_positive_code_column_equal_supportpreservesource_value dst_positive_scale_column_equal_supportpreservesource_value dst_negative_code_column_equal_supportpreservesource_value dst_negative_scale_column_equal_supportpreservesource_value dst_positive_column_equal_supportpreservesource_value dst_negative_column_equal_supportpreservesource_value. (((A) = (((((dst_positive_code_column_equal_supportpreservesource_value) + (dst_positive_scale_column_equal_supportpreservesource_value)) * S ((dst_positive_code_column_equal_supportpreservesource_value) + (dst_positive_scale_column_equal_supportpreservesource_value)) + ((dst_positive_scale_column_equal_supportpreservesource_value) + (dst_positive_scale_column_equal_supportpreservesource_value))) + (((dst_negative_code_column_equal_supportpreservesource_value) + (dst_negative_scale_column_equal_supportpreservesource_value)) * S ((dst_negative_code_column_equal_supportpreservesource_value) + (dst_negative_scale_column_equal_supportpreservesource_value)) + ((dst_negative_scale_column_equal_supportpreservesource_value) + (dst_negative_scale_column_equal_supportpreservesource_value)))) * S ((((dst_positive_code_column_equal_supportpreservesource_value) + (dst_positive_scale_column_equal_supportpreservesource_value)) * S ((dst_positive_code_column_equal_supportpreservesource_value) + (dst_positive_scale_column_equal_supportpreservesource_value)) + ((dst_positive_scale_column_equal_supportpreservesource_value) + (dst_positive_scale_column_equal_supportpreservesource_value))) + (((dst_negative_code_column_equal_supportpreservesource_value) + (dst_negative_scale_column_equal_supportpreservesource_value)) * S ((dst_negative_code_column_equal_supportpreservesource_value) + (dst_negative_scale_column_equal_supportpreservesource_value)) + ((dst_negative_scale_column_equal_supportpreservesource_value) + (dst_negative_scale_column_equal_supportpreservesource_value)))) + ((((dst_negative_code_column_equal_supportpreservesource_value) + (dst_negative_scale_column_equal_supportpreservesource_value)) * S ((dst_negative_code_column_equal_supportpreservesource_value) + (dst_negative_scale_column_equal_supportpreservesource_value)) + ((dst_negative_scale_column_equal_supportpreservesource_value) + (dst_negative_scale_column_equal_supportpreservesource_value))) + (((dst_negative_code_column_equal_supportpreservesource_value) + (dst_negative_scale_column_equal_supportpreservesource_value)) * S ((dst_negative_code_column_equal_supportpreservesource_value) + (dst_negative_scale_column_equal_supportpreservesource_value)) + ((dst_negative_scale_column_equal_supportpreservesource_value) + (dst_negative_scale_column_equal_supportpreservesource_value)))))) /\ (((((exists ff_h_pvs_column_equal_supportpreservesource_valuepositive. ff_h_pvs_column_equal_supportpreservesource_valuepositive + S (dst_positive_column_equal_supportpreservesource_value) = S ((S (ssr_source_column_equal_supportpreserve)) * dst_positive_scale_column_equal_supportpreservesource_value)) /\ exists ff_q_pvs_column_equal_supportpreservesource_valuepositive. dst_positive_code_column_equal_supportpreservesource_value = ff_q_pvs_column_equal_supportpreservesource_valuepositive * S ((S (ssr_source_column_equal_supportpreserve)) * dst_positive_scale_column_equal_supportpreservesource_value) + (dst_positive_column_equal_supportpreservesource_value))) /\ (((((exists ff_h_pvs_column_equal_supportpreservesource_valuenegative. ff_h_pvs_column_equal_supportpreservesource_valuenegative + S (dst_negative_column_equal_supportpreservesource_value) = S ((S (ssr_source_column_equal_supportpreserve)) * dst_negative_scale_column_equal_supportpreservesource_value)) /\ exists ff_q_pvs_column_equal_supportpreservesource_valuenegative. dst_negative_code_column_equal_supportpreservesource_value = ff_q_pvs_column_equal_supportpreservesource_valuenegative * S ((S (ssr_source_column_equal_supportpreserve)) * dst_negative_scale_column_equal_supportpreservesource_value) + (dst_negative_column_equal_supportpreservesource_value))) /\ (exists ge_balance_positive_column_equal_supportpreservesource_valuevalue ge_balance_negative_column_equal_supportpreservesource_valuevalue. (((((ssr_value_column_equal_supportpreserve) = 2 * (ge_balance_positive_column_equal_supportpreservesource_valuevalue) /\ (ge_balance_negative_column_equal_supportpreservesource_valuevalue) = 0) \/ exists ge_signed_half_column_equal_supportpreservesource_valuevaluedecode. (((ssr_value_column_equal_supportpreserve) = 2 * ge_signed_half_column_equal_supportpreservesource_valuevaluedecode + 1 /\ (ge_balance_positive_column_equal_supportpreservesource_valuevalue) = 0) /\ (ge_balance_negative_column_equal_supportpreservesource_valuevalue) = S ge_signed_half_column_equal_supportpreservesource_valuevaluedecode))) /\ ((dst_positive_column_equal_supportpreservesource_value) + ge_balance_negative_column_equal_supportpreservesource_valuevalue = (dst_negative_column_equal_supportpreservesource_value) + ge_balance_positive_column_equal_supportpreservesource_valuevalue))))))))) -> ~(ssr_value_column_equal_supportpreserve=0) -> exists ssr_target_column_equal_supportpreserve. ((((exists ff_h_pvs_column_equal_supportpreservemap. ff_h_pvs_column_equal_supportpreservemap + S (ssr_target_column_equal_supportpreserve) = S ((S (ssr_source_column_equal_supportpreserve)) * s)) /\ exists ff_q_pvs_column_equal_supportpreservemap. r = ff_q_pvs_column_equal_supportpreservemap * S ((S (ssr_source_column_equal_supportpreserve)) * s) + (ssr_target_column_equal_supportpreserve))) /\ (((exists pvs_gap_column_equal_supportpreservetarget_bound. pvs_gap_column_equal_supportpreservetarget_bound + S (ssr_target_column_equal_supportpreserve) = (M)) /\ (exists dst_positive_code_column_equal_supportpreservetarget_value dst_positive_scale_column_equal_supportpreservetarget_value dst_negative_code_column_equal_supportpreservetarget_value dst_negative_scale_column_equal_supportpreservetarget_value dst_positive_column_equal_supportpreservetarget_value dst_negative_column_equal_supportpreservetarget_value. (((B) = (((((dst_positive_code_column_equal_supportpreservetarget_value) + (dst_positive_scale_column_equal_supportpreservetarget_value)) * S ((dst_positive_code_column_equal_supportpreservetarget_value) + (dst_positive_scale_column_equal_supportpreservetarget_value)) + ((dst_positive_scale_column_equal_supportpreservetarget_value) + (dst_positive_scale_column_equal_supportpreservetarget_value))) + (((dst_negative_code_column_equal_supportpreservetarget_value) + (dst_negative_scale_column_equal_supportpreservetarget_value)) * S ((dst_negative_code_column_equal_supportpreservetarget_value) + (dst_negative_scale_column_equal_supportpreservetarget_value)) + ((dst_negative_scale_column_equal_supportpreservetarget_value) + (dst_negative_scale_column_equal_supportpreservetarget_value)))) * S ((((dst_positive_code_column_equal_supportpreservetarget_value) + (dst_positive_scale_column_equal_supportpreservetarget_value)) * S ((dst_positive_code_column_equal_supportpreservetarget_value) + (dst_positive_scale_column_equal_supportpreservetarget_value)) + ((dst_positive_scale_column_equal_supportpreservetarget_value) + (dst_positive_scale_column_equal_supportpreservetarget_value))) + (((dst_negative_code_column_equal_supportpreservetarget_value) + (dst_negative_scale_column_equal_supportpreservetarget_value)) * S ((dst_negative_code_column_equal_supportpreservetarget_value) + (dst_negative_scale_column_equal_supportpreservetarget_value)) + ((dst_negative_scale_column_equal_supportpreservetarget_value) + (dst_negative_scale_column_equal_supportpreservetarget_value)))) + ((((dst_negative_code_column_equal_supportpreservetarget_value) + (dst_negative_scale_column_equal_supportpreservetarget_value)) * S ((dst_negative_code_column_equal_supportpreservetarget_value) + (dst_negative_scale_column_equal_supportpreservetarget_value)) + ((dst_negative_scale_column_equal_supportpreservetarget_value) + (dst_negative_scale_column_equal_supportpreservetarget_value))) + (((dst_negative_code_column_equal_supportpreservetarget_value) + (dst_negative_scale_column_equal_supportpreservetarget_value)) * S ((dst_negative_code_column_equal_supportpreservetarget_value) + (dst_negative_scale_column_equal_supportpreservetarget_value)) + ((dst_negative_scale_column_equal_supportpreservetarget_value) + (dst_negative_scale_column_equal_supportpreservetarget_value)))))) /\ (((((exists ff_h_pvs_column_equal_supportpreservetarget_valuepositive. ff_h_pvs_column_equal_supportpreservetarget_valuepositive + S (dst_positive_column_equal_supportpreservetarget_value) = S ((S (ssr_target_column_equal_supportpreserve)) * dst_positive_scale_column_equal_supportpreservetarget_value)) /\ exists ff_q_pvs_column_equal_supportpreservetarget_valuepositive. dst_positive_code_column_equal_supportpreservetarget_value = ff_q_pvs_column_equal_supportpreservetarget_valuepositive * S ((S (ssr_target_column_equal_supportpreserve)) * dst_positive_scale_column_equal_supportpreservetarget_value) + (dst_positive_column_equal_supportpreservetarget_value))) /\ (((((exists ff_h_pvs_column_equal_supportpreservetarget_valuenegative. ff_h_pvs_column_equal_supportpreservetarget_valuenegative + S (dst_negative_column_equal_supportpreservetarget_value) = S ((S (ssr_target_column_equal_supportpreserve)) * dst_negative_scale_column_equal_supportpreservetarget_value)) /\ exists ff_q_pvs_column_equal_supportpreservetarget_valuenegative. dst_negative_code_column_equal_supportpreservetarget_value = ff_q_pvs_column_equal_supportpreservetarget_valuenegative * S ((S (ssr_target_column_equal_supportpreserve)) * dst_negative_scale_column_equal_supportpreservetarget_value) + (dst_negative_column_equal_supportpreservetarget_value))) /\ (exists ge_balance_positive_column_equal_supportpreservetarget_valuevalue ge_balance_negative_column_equal_supportpreservetarget_valuevalue. (((((ssr_value_column_equal_supportpreserve) = 2 * (ge_balance_positive_column_equal_supportpreservetarget_valuevalue) /\ (ge_balance_negative_column_equal_supportpreservetarget_valuevalue) = 0) \/ exists ge_signed_half_column_equal_supportpreservetarget_valuevaluedecode. (((ssr_value_column_equal_supportpreserve) = 2 * ge_signed_half_column_equal_supportpreservetarget_valuevaluedecode + 1 /\ (ge_balance_positive_column_equal_supportpreservetarget_valuevalue) = 0) /\ (ge_balance_negative_column_equal_supportpreservetarget_valuevalue) = S ge_signed_half_column_equal_supportpreservetarget_valuevaluedecode))) /\ ((dst_positive_column_equal_supportpreservetarget_value) + ge_balance_negative_column_equal_supportpreservetarget_valuevalue = (dst_negative_column_equal_supportpreservetarget_value) + ge_balance_positive_column_equal_supportpreservetarget_valuevalue))))))))))))) /\ (((forall ssr_first_column_equal_supportinjective ssr_second_column_equal_supportinjective ssr_image_column_equal_supportinjective ssr_a_column_equal_supportinjective ssr_b_column_equal_supportinjective. (exists pvs_gap_column_equal_supportinjectivefirst_bound. pvs_gap_column_equal_supportinjectivefirst_bound + S (ssr_first_column_equal_supportinjective) = (L)) -> (exists pvs_gap_column_equal_supportinjectivesecond_bound. pvs_gap_column_equal_supportinjectivesecond_bound + S (ssr_second_column_equal_supportinjective) = (L)) -> (exists dst_positive_code_column_equal_supportinjectivefirst_value dst_positive_scale_column_equal_supportinjectivefirst_value dst_negative_code_column_equal_supportinjectivefirst_value dst_negative_scale_column_equal_supportinjectivefirst_value dst_positive_column_equal_supportinjectivefirst_value dst_negative_column_equal_supportinjectivefirst_value. (((A) = (((((dst_positive_code_column_equal_supportinjectivefirst_value) + (dst_positive_scale_column_equal_supportinjectivefirst_value)) * S ((dst_positive_code_column_equal_supportinjectivefirst_value) + (dst_positive_scale_column_equal_supportinjectivefirst_value)) + ((dst_positive_scale_column_equal_supportinjectivefirst_value) + (dst_positive_scale_column_equal_supportinjectivefirst_value))) + (((dst_negative_code_column_equal_supportinjectivefirst_value) + (dst_negative_scale_column_equal_supportinjectivefirst_value)) * S ((dst_negative_code_column_equal_supportinjectivefirst_value) + (dst_negative_scale_column_equal_supportinjectivefirst_value)) + ((dst_negative_scale_column_equal_supportinjectivefirst_value) + (dst_negative_scale_column_equal_supportinjectivefirst_value)))) * S ((((dst_positive_code_column_equal_supportinjectivefirst_value) + (dst_positive_scale_column_equal_supportinjectivefirst_value)) * S ((dst_positive_code_column_equal_supportinjectivefirst_value) + (dst_positive_scale_column_equal_supportinjectivefirst_value)) + ((dst_positive_scale_column_equal_supportinjectivefirst_value) + (dst_positive_scale_column_equal_supportinjectivefirst_value))) + (((dst_negative_code_column_equal_supportinjectivefirst_value) + (dst_negative_scale_column_equal_supportinjectivefirst_value)) * S ((dst_negative_code_column_equal_supportinjectivefirst_value) + (dst_negative_scale_column_equal_supportinjectivefirst_value)) + ((dst_negative_scale_column_equal_supportinjectivefirst_value) + (dst_negative_scale_column_equal_supportinjectivefirst_value)))) + ((((dst_negative_code_column_equal_supportinjectivefirst_value) + (dst_negative_scale_column_equal_supportinjectivefirst_value)) * S ((dst_negative_code_column_equal_supportinjectivefirst_value) + (dst_negative_scale_column_equal_supportinjectivefirst_value)) + ((dst_negative_scale_column_equal_supportinjectivefirst_value) + (dst_negative_scale_column_equal_supportinjectivefirst_value))) + (((dst_negative_code_column_equal_supportinjectivefirst_value) + (dst_negative_scale_column_equal_supportinjectivefirst_value)) * S ((dst_negative_code_column_equal_supportinjectivefirst_value) + (dst_negative_scale_column_equal_supportinjectivefirst_value)) + ((dst_negative_scale_column_equal_supportinjectivefirst_value) + (dst_negative_scale_column_equal_supportinjectivefirst_value)))))) /\ (((((exists ff_h_pvs_column_equal_supportinjectivefirst_valuepositive. ff_h_pvs_column_equal_supportinjectivefirst_valuepositive + S (dst_positive_column_equal_supportinjectivefirst_value) = S ((S (ssr_first_column_equal_supportinjective)) * dst_positive_scale_column_equal_supportinjectivefirst_value)) /\ exists ff_q_pvs_column_equal_supportinjectivefirst_valuepositive. dst_positive_code_column_equal_supportinjectivefirst_value = ff_q_pvs_column_equal_supportinjectivefirst_valuepositive * S ((S (ssr_first_column_equal_supportinjective)) * dst_positive_scale_column_equal_supportinjectivefirst_value) + (dst_positive_column_equal_supportinjectivefirst_value))) /\ (((((exists ff_h_pvs_column_equal_supportinjectivefirst_valuenegative. ff_h_pvs_column_equal_supportinjectivefirst_valuenegative + S (dst_negative_column_equal_supportinjectivefirst_value) = S ((S (ssr_first_column_equal_supportinjective)) * dst_negative_scale_column_equal_supportinjectivefirst_value)) /\ exists ff_q_pvs_column_equal_supportinjectivefirst_valuenegative. dst_negative_code_column_equal_supportinjectivefirst_value = ff_q_pvs_column_equal_supportinjectivefirst_valuenegative * S ((S (ssr_first_column_equal_supportinjective)) * dst_negative_scale_column_equal_supportinjectivefirst_value) + (dst_negative_column_equal_supportinjectivefirst_value))) /\ (exists ge_balance_positive_column_equal_supportinjectivefirst_valuevalue ge_balance_negative_column_equal_supportinjectivefirst_valuevalue. (((((ssr_a_column_equal_supportinjective) = 2 * (ge_balance_positive_column_equal_supportinjectivefirst_valuevalue) /\ (ge_balance_negative_column_equal_supportinjectivefirst_valuevalue) = 0) \/ exists ge_signed_half_column_equal_supportinjectivefirst_valuevaluedecode. (((ssr_a_column_equal_supportinjective) = 2 * ge_signed_half_column_equal_supportinjectivefirst_valuevaluedecode + 1 /\ (ge_balance_positive_column_equal_supportinjectivefirst_valuevalue) = 0) /\ (ge_balance_negative_column_equal_supportinjectivefirst_valuevalue) = S ge_signed_half_column_equal_supportinjectivefirst_valuevaluedecode))) /\ ((dst_positive_column_equal_supportinjectivefirst_value) + ge_balance_negative_column_equal_supportinjectivefirst_valuevalue = (dst_negative_column_equal_supportinjectivefirst_value) + ge_balance_positive_column_equal_supportinjectivefirst_valuevalue))))))))) -> ~(ssr_a_column_equal_supportinjective=0) -> (exists dst_positive_code_column_equal_supportinjectivesecond_value dst_positive_scale_column_equal_supportinjectivesecond_value dst_negative_code_column_equal_supportinjectivesecond_value dst_negative_scale_column_equal_supportinjectivesecond_value dst_positive_column_equal_supportinjectivesecond_value dst_negative_column_equal_supportinjectivesecond_value. (((A) = (((((dst_positive_code_column_equal_supportinjectivesecond_value) + (dst_positive_scale_column_equal_supportinjectivesecond_value)) * S ((dst_positive_code_column_equal_supportinjectivesecond_value) + (dst_positive_scale_column_equal_supportinjectivesecond_value)) + ((dst_positive_scale_column_equal_supportinjectivesecond_value) + (dst_positive_scale_column_equal_supportinjectivesecond_value))) + (((dst_negative_code_column_equal_supportinjectivesecond_value) + (dst_negative_scale_column_equal_supportinjectivesecond_value)) * S ((dst_negative_code_column_equal_supportinjectivesecond_value) + (dst_negative_scale_column_equal_supportinjectivesecond_value)) + ((dst_negative_scale_column_equal_supportinjectivesecond_value) + (dst_negative_scale_column_equal_supportinjectivesecond_value)))) * S ((((dst_positive_code_column_equal_supportinjectivesecond_value) + (dst_positive_scale_column_equal_supportinjectivesecond_value)) * S ((dst_positive_code_column_equal_supportinjectivesecond_value) + (dst_positive_scale_column_equal_supportinjectivesecond_value)) + ((dst_positive_scale_column_equal_supportinjectivesecond_value) + (dst_positive_scale_column_equal_supportinjectivesecond_value))) + (((dst_negative_code_column_equal_supportinjectivesecond_value) + (dst_negative_scale_column_equal_supportinjectivesecond_value)) * S ((dst_negative_code_column_equal_supportinjectivesecond_value) + (dst_negative_scale_column_equal_supportinjectivesecond_value)) + ((dst_negative_scale_column_equal_supportinjectivesecond_value) + (dst_negative_scale_column_equal_supportinjectivesecond_value)))) + ((((dst_negative_code_column_equal_supportinjectivesecond_value) + (dst_negative_scale_column_equal_supportinjectivesecond_value)) * S ((dst_negative_code_column_equal_supportinjectivesecond_value) + (dst_negative_scale_column_equal_supportinjectivesecond_value)) + ((dst_negative_scale_column_equal_supportinjectivesecond_value) + (dst_negative_scale_column_equal_supportinjectivesecond_value))) + (((dst_negative_code_column_equal_supportinjectivesecond_value) + (dst_negative_scale_column_equal_supportinjectivesecond_value)) * S ((dst_negative_code_column_equal_supportinjectivesecond_value) + (dst_negative_scale_column_equal_supportinjectivesecond_value)) + ((dst_negative_scale_column_equal_supportinjectivesecond_value) + (dst_negative_scale_column_equal_supportinjectivesecond_value)))))) /\ (((((exists ff_h_pvs_column_equal_supportinjectivesecond_valuepositive. ff_h_pvs_column_equal_supportinjectivesecond_valuepositive + S (dst_positive_column_equal_supportinjectivesecond_value) = S ((S (ssr_second_column_equal_supportinjective)) * dst_positive_scale_column_equal_supportinjectivesecond_value)) /\ exists ff_q_pvs_column_equal_supportinjectivesecond_valuepositive. dst_positive_code_column_equal_supportinjectivesecond_value = ff_q_pvs_column_equal_supportinjectivesecond_valuepositive * S ((S (ssr_second_column_equal_supportinjective)) * dst_positive_scale_column_equal_supportinjectivesecond_value) + (dst_positive_column_equal_supportinjectivesecond_value))) /\ (((((exists ff_h_pvs_column_equal_supportinjectivesecond_valuenegative. ff_h_pvs_column_equal_supportinjectivesecond_valuenegative + S (dst_negative_column_equal_supportinjectivesecond_value) = S ((S (ssr_second_column_equal_supportinjective)) * dst_negative_scale_column_equal_supportinjectivesecond_value)) /\ exists ff_q_pvs_column_equal_supportinjectivesecond_valuenegative. dst_negative_code_column_equal_supportinjectivesecond_value = ff_q_pvs_column_equal_supportinjectivesecond_valuenegative * S ((S (ssr_second_column_equal_supportinjective)) * dst_negative_scale_column_equal_supportinjectivesecond_value) + (dst_negative_column_equal_supportinjectivesecond_value))) /\ (exists ge_balance_positive_column_equal_supportinjectivesecond_valuevalue ge_balance_negative_column_equal_supportinjectivesecond_valuevalue. (((((ssr_b_column_equal_supportinjective) = 2 * (ge_balance_positive_column_equal_supportinjectivesecond_valuevalue) /\ (ge_balance_negative_column_equal_supportinjectivesecond_valuevalue) = 0) \/ exists ge_signed_half_column_equal_supportinjectivesecond_valuevaluedecode. (((ssr_b_column_equal_supportinjective) = 2 * ge_signed_half_column_equal_supportinjectivesecond_valuevaluedecode + 1 /\ (ge_balance_positive_column_equal_supportinjectivesecond_valuevalue) = 0) /\ (ge_balance_negative_column_equal_supportinjectivesecond_valuevalue) = S ge_signed_half_column_equal_supportinjectivesecond_valuevaluedecode))) /\ ((dst_positive_column_equal_supportinjectivesecond_value) + ge_balance_negative_column_equal_supportinjectivesecond_valuevalue = (dst_negative_column_equal_supportinjectivesecond_value) + ge_balance_positive_column_equal_supportinjectivesecond_valuevalue))))))))) -> ~(ssr_b_column_equal_supportinjective=0) -> (((exists ff_h_pvs_column_equal_supportinjectivefirst_map. ff_h_pvs_column_equal_supportinjectivefirst_map + S (ssr_image_column_equal_supportinjective) = S ((S (ssr_first_column_equal_supportinjective)) * s)) /\ exists ff_q_pvs_column_equal_supportinjectivefirst_map. r = ff_q_pvs_column_equal_supportinjectivefirst_map * S ((S (ssr_first_column_equal_supportinjective)) * s) + (ssr_image_column_equal_supportinjective))) -> (((exists ff_h_pvs_column_equal_supportinjectivesecond_map. ff_h_pvs_column_equal_supportinjectivesecond_map + S (ssr_image_column_equal_supportinjective) = S ((S (ssr_second_column_equal_supportinjective)) * s)) /\ exists ff_q_pvs_column_equal_supportinjectivesecond_map. r = ff_q_pvs_column_equal_supportinjectivesecond_map * S ((S (ssr_second_column_equal_supportinjective)) * s) + (ssr_image_column_equal_supportinjective))) -> ssr_first_column_equal_supportinjective=ssr_second_column_equal_supportinjective) /\ (forall ssr_target_column_equal_supportcover ssr_value_column_equal_supportcover. (exists pvs_gap_column_equal_supportcovertarget_bound. pvs_gap_column_equal_supportcovertarget_bound + S (ssr_target_column_equal_supportcover) = (M)) -> (exists dst_positive_code_column_equal_supportcovertarget_value dst_positive_scale_column_equal_supportcovertarget_value dst_negative_code_column_equal_supportcovertarget_value dst_negative_scale_column_equal_supportcovertarget_value dst_positive_column_equal_supportcovertarget_value dst_negative_column_equal_supportcovertarget_value. (((B) = (((((dst_positive_code_column_equal_supportcovertarget_value) + (dst_positive_scale_column_equal_supportcovertarget_value)) * S ((dst_positive_code_column_equal_supportcovertarget_value) + (dst_positive_scale_column_equal_supportcovertarget_value)) + ((dst_positive_scale_column_equal_supportcovertarget_value) + (dst_positive_scale_column_equal_supportcovertarget_value))) + (((dst_negative_code_column_equal_supportcovertarget_value) + (dst_negative_scale_column_equal_supportcovertarget_value)) * S ((dst_negative_code_column_equal_supportcovertarget_value) + (dst_negative_scale_column_equal_supportcovertarget_value)) + ((dst_negative_scale_column_equal_supportcovertarget_value) + (dst_negative_scale_column_equal_supportcovertarget_value)))) * S ((((dst_positive_code_column_equal_supportcovertarget_value) + (dst_positive_scale_column_equal_supportcovertarget_value)) * S ((dst_positive_code_column_equal_supportcovertarget_value) + (dst_positive_scale_column_equal_supportcovertarget_value)) + ((dst_positive_scale_column_equal_supportcovertarget_value) + (dst_positive_scale_column_equal_supportcovertarget_value))) + (((dst_negative_code_column_equal_supportcovertarget_value) + (dst_negative_scale_column_equal_supportcovertarget_value)) * S ((dst_negative_code_column_equal_supportcovertarget_value) + (dst_negative_scale_column_equal_supportcovertarget_value)) + ((dst_negative_scale_column_equal_supportcovertarget_value) + (dst_negative_scale_column_equal_supportcovertarget_value)))) + ((((dst_negative_code_column_equal_supportcovertarget_value) + (dst_negative_scale_column_equal_supportcovertarget_value)) * S ((dst_negative_code_column_equal_supportcovertarget_value) + (dst_negative_scale_column_equal_supportcovertarget_value)) + ((dst_negative_scale_column_equal_supportcovertarget_value) + (dst_negative_scale_column_equal_supportcovertarget_value))) + (((dst_negative_code_column_equal_supportcovertarget_value) + (dst_negative_scale_column_equal_supportcovertarget_value)) * S ((dst_negative_code_column_equal_supportcovertarget_value) + (dst_negative_scale_column_equal_supportcovertarget_value)) + ((dst_negative_scale_column_equal_supportcovertarget_value) + (dst_negative_scale_column_equal_supportcovertarget_value)))))) /\ (((((exists ff_h_pvs_column_equal_supportcovertarget_valuepositive. ff_h_pvs_column_equal_supportcovertarget_valuepositive + S (dst_positive_column_equal_supportcovertarget_value) = S ((S (ssr_target_column_equal_supportcover)) * dst_positive_scale_column_equal_supportcovertarget_value)) /\ exists ff_q_pvs_column_equal_supportcovertarget_valuepositive. dst_positive_code_column_equal_supportcovertarget_value = ff_q_pvs_column_equal_supportcovertarget_valuepositive * S ((S (ssr_target_column_equal_supportcover)) * dst_positive_scale_column_equal_supportcovertarget_value) + (dst_positive_column_equal_supportcovertarget_value))) /\ (((((exists ff_h_pvs_column_equal_supportcovertarget_valuenegative. ff_h_pvs_column_equal_supportcovertarget_valuenegative + S (dst_negative_column_equal_supportcovertarget_value) = S ((S (ssr_target_column_equal_supportcover)) * dst_negative_scale_column_equal_supportcovertarget_value)) /\ exists ff_q_pvs_column_equal_supportcovertarget_valuenegative. dst_negative_code_column_equal_supportcovertarget_value = ff_q_pvs_column_equal_supportcovertarget_valuenegative * S ((S (ssr_target_column_equal_supportcover)) * dst_negative_scale_column_equal_supportcovertarget_value) + (dst_negative_column_equal_supportcovertarget_value))) /\ (exists ge_balance_positive_column_equal_supportcovertarget_valuevalue ge_balance_negative_column_equal_supportcovertarget_valuevalue. (((((ssr_value_column_equal_supportcover) = 2 * (ge_balance_positive_column_equal_supportcovertarget_valuevalue) /\ (ge_balance_negative_column_equal_supportcovertarget_valuevalue) = 0) \/ exists ge_signed_half_column_equal_supportcovertarget_valuevaluedecode. (((ssr_value_column_equal_supportcover) = 2 * ge_signed_half_column_equal_supportcovertarget_valuevaluedecode + 1 /\ (ge_balance_positive_column_equal_supportcovertarget_valuevalue) = 0) /\ (ge_balance_negative_column_equal_supportcovertarget_valuevalue) = S ge_signed_half_column_equal_supportcovertarget_valuevaluedecode))) /\ ((dst_positive_column_equal_supportcovertarget_value) + ge_balance_negative_column_equal_supportcovertarget_valuevalue = (dst_negative_column_equal_supportcovertarget_value) + ge_balance_positive_column_equal_supportcovertarget_valuevalue))))))))) -> ~(ssr_value_column_equal_supportcover=0) -> exists ssr_source_column_equal_supportcover. ((exists pvs_gap_column_equal_supportcoversource_bound. pvs_gap_column_equal_supportcoversource_bound + S (ssr_source_column_equal_supportcover) = (L)) /\ (((((exists ff_h_pvs_column_equal_supportcovermap. ff_h_pvs_column_equal_supportcovermap + S (ssr_target_column_equal_supportcover) = S ((S (ssr_source_column_equal_supportcover)) * s)) /\ exists ff_q_pvs_column_equal_supportcovermap. r = ff_q_pvs_column_equal_supportcovermap * S ((S (ssr_source_column_equal_supportcover)) * s) + (ssr_target_column_equal_supportcover))) /\ (exists dst_positive_code_column_equal_supportcoversource_value dst_positive_scale_column_equal_supportcoversource_value dst_negative_code_column_equal_supportcoversource_value dst_negative_scale_column_equal_supportcoversource_value dst_positive_column_equal_supportcoversource_value dst_negative_column_equal_supportcoversource_value. (((A) = (((((dst_positive_code_column_equal_supportcoversource_value) + (dst_positive_scale_column_equal_supportcoversource_value)) * S ((dst_positive_code_column_equal_supportcoversource_value) + (dst_positive_scale_column_equal_supportcoversource_value)) + ((dst_positive_scale_column_equal_supportcoversource_value) + (dst_positive_scale_column_equal_supportcoversource_value))) + (((dst_negative_code_column_equal_supportcoversource_value) + (dst_negative_scale_column_equal_supportcoversource_value)) * S ((dst_negative_code_column_equal_supportcoversource_value) + (dst_negative_scale_column_equal_supportcoversource_value)) + ((dst_negative_scale_column_equal_supportcoversource_value) + (dst_negative_scale_column_equal_supportcoversource_value)))) * S ((((dst_positive_code_column_equal_supportcoversource_value) + (dst_positive_scale_column_equal_supportcoversource_value)) * S ((dst_positive_code_column_equal_supportcoversource_value) + (dst_positive_scale_column_equal_supportcoversource_value)) + ((dst_positive_scale_column_equal_supportcoversource_value) + (dst_positive_scale_column_equal_supportcoversource_value))) + (((dst_negative_code_column_equal_supportcoversource_value) + (dst_negative_scale_column_equal_supportcoversource_value)) * S ((dst_negative_code_column_equal_supportcoversource_value) + (dst_negative_scale_column_equal_supportcoversource_value)) + ((dst_negative_scale_column_equal_supportcoversource_value) + (dst_negative_scale_column_equal_supportcoversource_value)))) + ((((dst_negative_code_column_equal_supportcoversource_value) + (dst_negative_scale_column_equal_supportcoversource_value)) * S ((dst_negative_code_column_equal_supportcoversource_value) + (dst_negative_scale_column_equal_supportcoversource_value)) + ((dst_negative_scale_column_equal_supportcoversource_value) + (dst_negative_scale_column_equal_supportcoversource_value))) + (((dst_negative_code_column_equal_supportcoversource_value) + (dst_negative_scale_column_equal_supportcoversource_value)) * S ((dst_negative_code_column_equal_supportcoversource_value) + (dst_negative_scale_column_equal_supportcoversource_value)) + ((dst_negative_scale_column_equal_supportcoversource_value) + (dst_negative_scale_column_equal_supportcoversource_value)))))) /\ (((((exists ff_h_pvs_column_equal_supportcoversource_valuepositive. ff_h_pvs_column_equal_supportcoversource_valuepositive + S (dst_positive_column_equal_supportcoversource_value) = S ((S (ssr_source_column_equal_supportcover)) * dst_positive_scale_column_equal_supportcoversource_value)) /\ exists ff_q_pvs_column_equal_supportcoversource_valuepositive. dst_positive_code_column_equal_supportcoversource_value = ff_q_pvs_column_equal_supportcoversource_valuepositive * S ((S (ssr_source_column_equal_supportcover)) * dst_positive_scale_column_equal_supportcoversource_value) + (dst_positive_column_equal_supportcoversource_value))) /\ (((((exists ff_h_pvs_column_equal_supportcoversource_valuenegative. ff_h_pvs_column_equal_supportcoversource_valuenegative + S (dst_negative_column_equal_supportcoversource_value) = S ((S (ssr_source_column_equal_supportcover)) * dst_negative_scale_column_equal_supportcoversource_value)) /\ exists ff_q_pvs_column_equal_supportcoversource_valuenegative. dst_negative_code_column_equal_supportcoversource_value = ff_q_pvs_column_equal_supportcoversource_valuenegative * S ((S (ssr_source_column_equal_supportcover)) * dst_negative_scale_column_equal_supportcoversource_value) + (dst_negative_column_equal_supportcoversource_value))) /\ (exists ge_balance_positive_column_equal_supportcoversource_valuevalue ge_balance_negative_column_equal_supportcoversource_valuevalue. (((((ssr_value_column_equal_supportcover) = 2 * (ge_balance_positive_column_equal_supportcoversource_valuevalue) /\ (ge_balance_negative_column_equal_supportcoversource_valuevalue) = 0) \/ exists ge_signed_half_column_equal_supportcoversource_valuevaluedecode. (((ssr_value_column_equal_supportcover) = 2 * ge_signed_half_column_equal_supportcoversource_valuevaluedecode + 1 /\ (ge_balance_positive_column_equal_supportcoversource_valuevalue) = 0) /\ (ge_balance_negative_column_equal_supportcoversource_valuevalue) = S ge_signed_half_column_equal_supportcoversource_valuevaluedecode))) /\ ((dst_positive_column_equal_supportcoversource_value) + ge_balance_negative_column_equal_supportcoversource_valuevalue = (dst_negative_column_equal_supportcoversource_value) + ge_balance_positive_column_equal_supportcoversource_valuevalue))))))))))))))))))))) -> (((exists dst_positive_code_column_equal_gridsource dst_positive_scale_column_equal_gridsource dst_negative_code_column_equal_gridsource dst_negative_scale_column_equal_gridsource. (((A) = (((((dst_positive_code_column_equal_gridsource) + (dst_positive_scale_column_equal_gridsource)) * S ((dst_positive_code_column_equal_gridsource) + (dst_positive_scale_column_equal_gridsource)) + ((dst_positive_scale_column_equal_gridsource) + (dst_positive_scale_column_equal_gridsource))) + (((dst_negative_code_column_equal_gridsource) + (dst_negative_scale_column_equal_gridsource)) * S ((dst_negative_code_column_equal_gridsource) + (dst_negative_scale_column_equal_gridsource)) + ((dst_negative_scale_column_equal_gridsource) + (dst_negative_scale_column_equal_gridsource)))) * S ((((dst_positive_code_column_equal_gridsource) + (dst_positive_scale_column_equal_gridsource)) * S ((dst_positive_code_column_equal_gridsource) + (dst_positive_scale_column_equal_gridsource)) + ((dst_positive_scale_column_equal_gridsource) + (dst_positive_scale_column_equal_gridsource))) + (((dst_negative_code_column_equal_gridsource) + (dst_negative_scale_column_equal_gridsource)) * S ((dst_negative_code_column_equal_gridsource) + (dst_negative_scale_column_equal_gridsource)) + ((dst_negative_scale_column_equal_gridsource) + (dst_negative_scale_column_equal_gridsource)))) + ((((dst_negative_code_column_equal_gridsource) + (dst_negative_scale_column_equal_gridsource)) * S ((dst_negative_code_column_equal_gridsource) + (dst_negative_scale_column_equal_gridsource)) + ((dst_negative_scale_column_equal_gridsource) + (dst_negative_scale_column_equal_gridsource))) + (((dst_negative_code_column_equal_gridsource) + (dst_negative_scale_column_equal_gridsource)) * S ((dst_negative_code_column_equal_gridsource) + (dst_negative_scale_column_equal_gridsource)) + ((dst_negative_scale_column_equal_gridsource) + (dst_negative_scale_column_equal_gridsource)))))) /\ (forall dst_index_column_equal_gridsource. (exists pvs_le_gap_column_equal_gridsourcedomain. pvs_le_gap_column_equal_gridsourcedomain + (dst_index_column_equal_gridsource) = (0)) -> exists dst_positive_column_equal_gridsource dst_negative_column_equal_gridsource dst_value_column_equal_gridsource. ((((exists ff_h_pvs_column_equal_gridsourceentrypositive. ff_h_pvs_column_equal_gridsourceentrypositive + S (dst_positive_column_equal_gridsource) = S ((S (dst_index_column_equal_gridsource)) * dst_positive_scale_column_equal_gridsource)) /\ exists ff_q_pvs_column_equal_gridsourceentrypositive. dst_positive_code_column_equal_gridsource = ff_q_pvs_column_equal_gridsourceentrypositive * S ((S (dst_index_column_equal_gridsource)) * dst_positive_scale_column_equal_gridsource) + (dst_positive_column_equal_gridsource))) /\ (((((exists ff_h_pvs_column_equal_gridsourceentrynegative. ff_h_pvs_column_equal_gridsourceentrynegative + S (dst_negative_column_equal_gridsource) = S ((S (dst_index_column_equal_gridsource)) * dst_negative_scale_column_equal_gridsource)) /\ exists ff_q_pvs_column_equal_gridsourceentrynegative. dst_negative_code_column_equal_gridsource = ff_q_pvs_column_equal_gridsourceentrynegative * S ((S (dst_index_column_equal_gridsource)) * dst_negative_scale_column_equal_gridsource) + (dst_negative_column_equal_gridsource))) /\ (exists ge_balance_positive_column_equal_gridsourceentryvalue ge_balance_negative_column_equal_gridsourceentryvalue. (((((dst_value_column_equal_gridsource) = 2 * (ge_balance_positive_column_equal_gridsourceentryvalue) /\ (ge_balance_negative_column_equal_gridsourceentryvalue) = 0) \/ exists ge_signed_half_column_equal_gridsourceentryvaluedecode. (((dst_value_column_equal_gridsource) = 2 * ge_signed_half_column_equal_gridsourceentryvaluedecode + 1 /\ (ge_balance_positive_column_equal_gridsourceentryvalue) = 0) /\ (ge_balance_negative_column_equal_gridsourceentryvalue) = S ge_signed_half_column_equal_gridsourceentryvaluedecode))) /\ ((dst_positive_column_equal_gridsource) + ge_balance_negative_column_equal_gridsourceentryvalue = (dst_negative_column_equal_gridsource) + ge_balance_positive_column_equal_gridsourceentryvalue))))))))) /\ (((exists dst_positive_code_column_equal_gridtable dst_positive_scale_column_equal_gridtable dst_negative_code_column_equal_gridtable dst_negative_scale_column_equal_gridtable. (((T) = (((((dst_positive_code_column_equal_gridtable) + (dst_positive_scale_column_equal_gridtable)) * S ((dst_positive_code_column_equal_gridtable) + (dst_positive_scale_column_equal_gridtable)) + ((dst_positive_scale_column_equal_gridtable) + (dst_positive_scale_column_equal_gridtable))) + (((dst_negative_code_column_equal_gridtable) + (dst_negative_scale_column_equal_gridtable)) * S ((dst_negative_code_column_equal_gridtable) + (dst_negative_scale_column_equal_gridtable)) + ((dst_negative_scale_column_equal_gridtable) + (dst_negative_scale_column_equal_gridtable)))) * S ((((dst_positive_code_column_equal_gridtable) + (dst_positive_scale_column_equal_gridtable)) * S ((dst_positive_code_column_equal_gridtable) + (dst_positive_scale_column_equal_gridtable)) + ((dst_positive_scale_column_equal_gridtable) + (dst_positive_scale_column_equal_gridtable))) + (((dst_negative_code_column_equal_gridtable) + (dst_negative_scale_column_equal_gridtable)) * S ((dst_negative_code_column_equal_gridtable) + (dst_negative_scale_column_equal_gridtable)) + ((dst_negative_scale_column_equal_gridtable) + (dst_negative_scale_column_equal_gridtable)))) + ((((dst_negative_code_column_equal_gridtable) + (dst_negative_scale_column_equal_gridtable)) * S ((dst_negative_code_column_equal_gridtable) + (dst_negative_scale_column_equal_gridtable)) + ((dst_negative_scale_column_equal_gridtable) + (dst_negative_scale_column_equal_gridtable))) + (((dst_negative_code_column_equal_gridtable) + (dst_negative_scale_column_equal_gridtable)) * S ((dst_negative_code_column_equal_gridtable) + (dst_negative_scale_column_equal_gridtable)) + ((dst_negative_scale_column_equal_gridtable) + (dst_negative_scale_column_equal_gridtable)))))) /\ (forall dst_index_column_equal_gridtable. (exists pvs_le_gap_column_equal_gridtabledomain. pvs_le_gap_column_equal_gridtabledomain + (dst_index_column_equal_gridtable) = ((L)*(S (M)))) -> exists dst_positive_column_equal_gridtable dst_negative_column_equal_gridtable dst_value_column_equal_gridtable. ((((exists ff_h_pvs_column_equal_gridtableentrypositive. ff_h_pvs_column_equal_gridtableentrypositive + S (dst_positive_column_equal_gridtable) = S ((S (dst_index_column_equal_gridtable)) * dst_positive_scale_column_equal_gridtable)) /\ exists ff_q_pvs_column_equal_gridtableentrypositive. dst_positive_code_column_equal_gridtable = ff_q_pvs_column_equal_gridtableentrypositive * S ((S (dst_index_column_equal_gridtable)) * dst_positive_scale_column_equal_gridtable) + (dst_positive_column_equal_gridtable))) /\ (((((exists ff_h_pvs_column_equal_gridtableentrynegative. ff_h_pvs_column_equal_gridtableentrynegative + S (dst_negative_column_equal_gridtable) = S ((S (dst_index_column_equal_gridtable)) * dst_negative_scale_column_equal_gridtable)) /\ exists ff_q_pvs_column_equal_gridtableentrynegative. dst_negative_code_column_equal_gridtable = ff_q_pvs_column_equal_gridtableentrynegative * S ((S (dst_index_column_equal_gridtable)) * dst_negative_scale_column_equal_gridtable) + (dst_negative_column_equal_gridtable))) /\ (exists ge_balance_positive_column_equal_gridtableentryvalue ge_balance_negative_column_equal_gridtableentryvalue. (((((dst_value_column_equal_gridtable) = 2 * (ge_balance_positive_column_equal_gridtableentryvalue) /\ (ge_balance_negative_column_equal_gridtableentryvalue) = 0) \/ exists ge_signed_half_column_equal_gridtableentryvaluedecode. (((dst_value_column_equal_gridtable) = 2 * ge_signed_half_column_equal_gridtableentryvaluedecode + 1 /\ (ge_balance_positive_column_equal_gridtableentryvalue) = 0) /\ (ge_balance_negative_column_equal_gridtableentryvalue) = S ge_signed_half_column_equal_gridtableentryvaluedecode))) /\ ((dst_positive_column_equal_gridtable) + ge_balance_negative_column_equal_gridtableentryvalue = (dst_negative_column_equal_gridtable) + ge_balance_positive_column_equal_gridtableentryvalue))))))))) /\ (forall ssr_grid_row_column_equal_grid ssr_grid_column_column_equal_grid ssr_grid_value_column_equal_grid. (exists pvs_gap_column_equal_gridrow_bound. pvs_gap_column_equal_gridrow_bound + S (ssr_grid_row_column_equal_grid) = (L)) -> (exists pvs_gap_column_equal_gridcolumn_bound. pvs_gap_column_equal_gridcolumn_bound + S (ssr_grid_column_column_equal_grid) = (M)) -> (exists dst_positive_code_column_equal_gridlookup dst_positive_scale_column_equal_gridlookup dst_negative_code_column_equal_gridlookup dst_negative_scale_column_equal_gridlookup dst_positive_column_equal_gridlookup dst_negative_column_equal_gridlookup. (((T) = (((((dst_positive_code_column_equal_gridlookup) + (dst_positive_scale_column_equal_gridlookup)) * S ((dst_positive_code_column_equal_gridlookup) + (dst_positive_scale_column_equal_gridlookup)) + ((dst_positive_scale_column_equal_gridlookup) + (dst_positive_scale_column_equal_gridlookup))) + (((dst_negative_code_column_equal_gridlookup) + (dst_negative_scale_column_equal_gridlookup)) * S ((dst_negative_code_column_equal_gridlookup) + (dst_negative_scale_column_equal_gridlookup)) + ((dst_negative_scale_column_equal_gridlookup) + (dst_negative_scale_column_equal_gridlookup)))) * S ((((dst_positive_code_column_equal_gridlookup) + (dst_positive_scale_column_equal_gridlookup)) * S ((dst_positive_code_column_equal_gridlookup) + (dst_positive_scale_column_equal_gridlookup)) + ((dst_positive_scale_column_equal_gridlookup) + (dst_positive_scale_column_equal_gridlookup))) + (((dst_negative_code_column_equal_gridlookup) + (dst_negative_scale_column_equal_gridlookup)) * S ((dst_negative_code_column_equal_gridlookup) + (dst_negative_scale_column_equal_gridlookup)) + ((dst_negative_scale_column_equal_gridlookup) + (dst_negative_scale_column_equal_gridlookup)))) + ((((dst_negative_code_column_equal_gridlookup) + (dst_negative_scale_column_equal_gridlookup)) * S ((dst_negative_code_column_equal_gridlookup) + (dst_negative_scale_column_equal_gridlookup)) + ((dst_negative_scale_column_equal_gridlookup) + (dst_negative_scale_column_equal_gridlookup))) + (((dst_negative_code_column_equal_gridlookup) + (dst_negative_scale_column_equal_gridlookup)) * S ((dst_negative_code_column_equal_gridlookup) + (dst_negative_scale_column_equal_gridlookup)) + ((dst_negative_scale_column_equal_gridlookup) + (dst_negative_scale_column_equal_gridlookup)))))) /\ (((((exists ff_h_pvs_column_equal_gridlookuppositive. ff_h_pvs_column_equal_gridlookuppositive + S (dst_positive_column_equal_gridlookup) = S ((S (((S (M))*(ssr_grid_row_column_equal_grid)+(ssr_grid_column_column_equal_grid)))) * dst_positive_scale_column_equal_gridlookup)) /\ exists ff_q_pvs_column_equal_gridlookuppositive. dst_positive_code_column_equal_gridlookup = ff_q_pvs_column_equal_gridlookuppositive * S ((S (((S (M))*(ssr_grid_row_column_equal_grid)+(ssr_grid_column_column_equal_grid)))) * dst_positive_scale_column_equal_gridlookup) + (dst_positive_column_equal_gridlookup))) /\ (((((exists ff_h_pvs_column_equal_gridlookupnegative. ff_h_pvs_column_equal_gridlookupnegative + S (dst_negative_column_equal_gridlookup) = S ((S (((S (M))*(ssr_grid_row_column_equal_grid)+(ssr_grid_column_column_equal_grid)))) * dst_negative_scale_column_equal_gridlookup)) /\ exists ff_q_pvs_column_equal_gridlookupnegative. dst_negative_code_column_equal_gridlookup = ff_q_pvs_column_equal_gridlookupnegative * S ((S (((S (M))*(ssr_grid_row_column_equal_grid)+(ssr_grid_column_column_equal_grid)))) * dst_negative_scale_column_equal_gridlookup) + (dst_negative_column_equal_gridlookup))) /\ (exists ge_balance_positive_column_equal_gridlookupvalue ge_balance_negative_column_equal_gridlookupvalue. (((((ssr_grid_value_column_equal_grid) = 2 * (ge_balance_positive_column_equal_gridlookupvalue) /\ (ge_balance_negative_column_equal_gridlookupvalue) = 0) \/ exists ge_signed_half_column_equal_gridlookupvaluedecode. (((ssr_grid_value_column_equal_grid) = 2 * ge_signed_half_column_equal_gridlookupvaluedecode + 1 /\ (ge_balance_positive_column_equal_gridlookupvalue) = 0) /\ (ge_balance_negative_column_equal_gridlookupvalue) = S ge_signed_half_column_equal_gridlookupvaluedecode))) /\ ((dst_positive_column_equal_gridlookup) + ge_balance_negative_column_equal_gridlookupvalue = (dst_negative_column_equal_gridlookup) + ge_balance_positive_column_equal_gridlookupvalue))))))))) -> (exists ssr_entry_value_column_equal_gridentry ssr_entry_image_column_equal_gridentry. ((exists dst_positive_code_column_equal_gridentrysource dst_positive_scale_column_equal_gridentrysource dst_negative_code_column_equal_gridentrysource dst_negative_scale_column_equal_gridentrysource dst_positive_column_equal_gridentrysource dst_negative_column_equal_gridentrysource. (((A) = (((((dst_positive_code_column_equal_gridentrysource) + (dst_positive_scale_column_equal_gridentrysource)) * S ((dst_positive_code_column_equal_gridentrysource) + (dst_positive_scale_column_equal_gridentrysource)) + ((dst_positive_scale_column_equal_gridentrysource) + (dst_positive_scale_column_equal_gridentrysource))) + (((dst_negative_code_column_equal_gridentrysource) + (dst_negative_scale_column_equal_gridentrysource)) * S ((dst_negative_code_column_equal_gridentrysource) + (dst_negative_scale_column_equal_gridentrysource)) + ((dst_negative_scale_column_equal_gridentrysource) + (dst_negative_scale_column_equal_gridentrysource)))) * S ((((dst_positive_code_column_equal_gridentrysource) + (dst_positive_scale_column_equal_gridentrysource)) * S ((dst_positive_code_column_equal_gridentrysource) + (dst_positive_scale_column_equal_gridentrysource)) + ((dst_positive_scale_column_equal_gridentrysource) + (dst_positive_scale_column_equal_gridentrysource))) + (((dst_negative_code_column_equal_gridentrysource) + (dst_negative_scale_column_equal_gridentrysource)) * S ((dst_negative_code_column_equal_gridentrysource) + (dst_negative_scale_column_equal_gridentrysource)) + ((dst_negative_scale_column_equal_gridentrysource) + (dst_negative_scale_column_equal_gridentrysource)))) + ((((dst_negative_code_column_equal_gridentrysource) + (dst_negative_scale_column_equal_gridentrysource)) * S ((dst_negative_code_column_equal_gridentrysource) + (dst_negative_scale_column_equal_gridentrysource)) + ((dst_negative_scale_column_equal_gridentrysource) + (dst_negative_scale_column_equal_gridentrysource))) + (((dst_negative_code_column_equal_gridentrysource) + (dst_negative_scale_column_equal_gridentrysource)) * S ((dst_negative_code_column_equal_gridentrysource) + (dst_negative_scale_column_equal_gridentrysource)) + ((dst_negative_scale_column_equal_gridentrysource) + (dst_negative_scale_column_equal_gridentrysource)))))) /\ (((((exists ff_h_pvs_column_equal_gridentrysourcepositive. ff_h_pvs_column_equal_gridentrysourcepositive + S (dst_positive_column_equal_gridentrysource) = S ((S (ssr_grid_row_column_equal_grid)) * dst_positive_scale_column_equal_gridentrysource)) /\ exists ff_q_pvs_column_equal_gridentrysourcepositive. dst_positive_code_column_equal_gridentrysource = ff_q_pvs_column_equal_gridentrysourcepositive * S ((S (ssr_grid_row_column_equal_grid)) * dst_positive_scale_column_equal_gridentrysource) + (dst_positive_column_equal_gridentrysource))) /\ (((((exists ff_h_pvs_column_equal_gridentrysourcenegative. ff_h_pvs_column_equal_gridentrysourcenegative + S (dst_negative_column_equal_gridentrysource) = S ((S (ssr_grid_row_column_equal_grid)) * dst_negative_scale_column_equal_gridentrysource)) /\ exists ff_q_pvs_column_equal_gridentrysourcenegative. dst_negative_code_column_equal_gridentrysource = ff_q_pvs_column_equal_gridentrysourcenegative * S ((S (ssr_grid_row_column_equal_grid)) * dst_negative_scale_column_equal_gridentrysource) + (dst_negative_column_equal_gridentrysource))) /\ (exists ge_balance_positive_column_equal_gridentrysourcevalue ge_balance_negative_column_equal_gridentrysourcevalue. (((((ssr_entry_value_column_equal_gridentry) = 2 * (ge_balance_positive_column_equal_gridentrysourcevalue) /\ (ge_balance_negative_column_equal_gridentrysourcevalue) = 0) \/ exists ge_signed_half_column_equal_gridentrysourcevaluedecode. (((ssr_entry_value_column_equal_gridentry) = 2 * ge_signed_half_column_equal_gridentrysourcevaluedecode + 1 /\ (ge_balance_positive_column_equal_gridentrysourcevalue) = 0) /\ (ge_balance_negative_column_equal_gridentrysourcevalue) = S ge_signed_half_column_equal_gridentrysourcevaluedecode))) /\ ((dst_positive_column_equal_gridentrysource) + ge_balance_negative_column_equal_gridentrysourcevalue = (dst_negative_column_equal_gridentrysource) + ge_balance_positive_column_equal_gridentrysourcevalue))))))))) /\ (((((exists ff_h_pvs_column_equal_gridentrymap. ff_h_pvs_column_equal_gridentrymap + S (ssr_entry_image_column_equal_gridentry) = S ((S (ssr_grid_row_column_equal_grid)) * s)) /\ exists ff_q_pvs_column_equal_gridentrymap. r = ff_q_pvs_column_equal_gridentrymap * S ((S (ssr_grid_row_column_equal_grid)) * s) + (ssr_entry_image_column_equal_gridentry))) /\ (((((ssr_grid_column_column_equal_grid)=(ssr_entry_image_column_equal_gridentry)) /\ ((ssr_grid_value_column_equal_grid)=(ssr_entry_value_column_equal_gridentry)))) \/ (((~((ssr_grid_column_column_equal_grid)=(ssr_entry_image_column_equal_gridentry))) /\ ((ssr_grid_value_column_equal_grid)=0))))))))))))) -> (((exists dst_positive_code_column_equal_rowssource_table dst_positive_scale_column_equal_rowssource_table dst_negative_code_column_equal_rowssource_table dst_negative_scale_column_equal_rowssource_table. (((T) = (((((dst_positive_code_column_equal_rowssource_table) + (dst_positive_scale_column_equal_rowssource_table)) * S ((dst_positive_code_column_equal_rowssource_table) + (dst_positive_scale_column_equal_rowssource_table)) + ((dst_positive_scale_column_equal_rowssource_table) + (dst_positive_scale_column_equal_rowssource_table))) + (((dst_negative_code_column_equal_rowssource_table) + (dst_negative_scale_column_equal_rowssource_table)) * S ((dst_negative_code_column_equal_rowssource_table) + (dst_negative_scale_column_equal_rowssource_table)) + ((dst_negative_scale_column_equal_rowssource_table) + (dst_negative_scale_column_equal_rowssource_table)))) * S ((((dst_positive_code_column_equal_rowssource_table) + (dst_positive_scale_column_equal_rowssource_table)) * S ((dst_positive_code_column_equal_rowssource_table) + (dst_positive_scale_column_equal_rowssource_table)) + ((dst_positive_scale_column_equal_rowssource_table) + (dst_positive_scale_column_equal_rowssource_table))) + (((dst_negative_code_column_equal_rowssource_table) + (dst_negative_scale_column_equal_rowssource_table)) * S ((dst_negative_code_column_equal_rowssource_table) + (dst_negative_scale_column_equal_rowssource_table)) + ((dst_negative_scale_column_equal_rowssource_table) + (dst_negative_scale_column_equal_rowssource_table)))) + ((((dst_negative_code_column_equal_rowssource_table) + (dst_negative_scale_column_equal_rowssource_table)) * S ((dst_negative_code_column_equal_rowssource_table) + (dst_negative_scale_column_equal_rowssource_table)) + ((dst_negative_scale_column_equal_rowssource_table) + (dst_negative_scale_column_equal_rowssource_table))) + (((dst_negative_code_column_equal_rowssource_table) + (dst_negative_scale_column_equal_rowssource_table)) * S ((dst_negative_code_column_equal_rowssource_table) + (dst_negative_scale_column_equal_rowssource_table)) + ((dst_negative_scale_column_equal_rowssource_table) + (dst_negative_scale_column_equal_rowssource_table)))))) /\ (forall dst_index_column_equal_rowssource_table. (exists pvs_le_gap_column_equal_rowssource_tabledomain. pvs_le_gap_column_equal_rowssource_tabledomain + (dst_index_column_equal_rowssource_table) = (0)) -> exists dst_positive_column_equal_rowssource_table dst_negative_column_equal_rowssource_table dst_value_column_equal_rowssource_table. ((((exists ff_h_pvs_column_equal_rowssource_tableentrypositive. ff_h_pvs_column_equal_rowssource_tableentrypositive + S (dst_positive_column_equal_rowssource_table) = S ((S (dst_index_column_equal_rowssource_table)) * dst_positive_scale_column_equal_rowssource_table)) /\ exists ff_q_pvs_column_equal_rowssource_tableentrypositive. dst_positive_code_column_equal_rowssource_table = ff_q_pvs_column_equal_rowssource_tableentrypositive * S ((S (dst_index_column_equal_rowssource_table)) * dst_positive_scale_column_equal_rowssource_table) + (dst_positive_column_equal_rowssource_table))) /\ (((((exists ff_h_pvs_column_equal_rowssource_tableentrynegative. ff_h_pvs_column_equal_rowssource_tableentrynegative + S (dst_negative_column_equal_rowssource_table) = S ((S (dst_index_column_equal_rowssource_table)) * dst_negative_scale_column_equal_rowssource_table)) /\ exists ff_q_pvs_column_equal_rowssource_tableentrynegative. dst_negative_code_column_equal_rowssource_table = ff_q_pvs_column_equal_rowssource_tableentrynegative * S ((S (dst_index_column_equal_rowssource_table)) * dst_negative_scale_column_equal_rowssource_table) + (dst_negative_column_equal_rowssource_table))) /\ (exists ge_balance_positive_column_equal_rowssource_tableentryvalue ge_balance_negative_column_equal_rowssource_tableentryvalue. (((((dst_value_column_equal_rowssource_table) = 2 * (ge_balance_positive_column_equal_rowssource_tableentryvalue) /\ (ge_balance_negative_column_equal_rowssource_tableentryvalue) = 0) \/ exists ge_signed_half_column_equal_rowssource_tableentryvaluedecode. (((dst_value_column_equal_rowssource_table) = 2 * ge_signed_half_column_equal_rowssource_tableentryvaluedecode + 1 /\ (ge_balance_positive_column_equal_rowssource_tableentryvalue) = 0) /\ (ge_balance_negative_column_equal_rowssource_tableentryvalue) = S ge_signed_half_column_equal_rowssource_tableentryvaluedecode))) /\ ((dst_positive_column_equal_rowssource_table) + ge_balance_negative_column_equal_rowssource_tableentryvalue = (dst_negative_column_equal_rowssource_table) + ge_balance_positive_column_equal_rowssource_tableentryvalue))))))))) /\ (((exists dst_positive_code_column_equal_rowsrow_table dst_positive_scale_column_equal_rowsrow_table dst_negative_code_column_equal_rowsrow_table dst_negative_scale_column_equal_rowsrow_table. (((C) = (((((dst_positive_code_column_equal_rowsrow_table) + (dst_positive_scale_column_equal_rowsrow_table)) * S ((dst_positive_code_column_equal_rowsrow_table) + (dst_positive_scale_column_equal_rowsrow_table)) + ((dst_positive_scale_column_equal_rowsrow_table) + (dst_positive_scale_column_equal_rowsrow_table))) + (((dst_negative_code_column_equal_rowsrow_table) + (dst_negative_scale_column_equal_rowsrow_table)) * S ((dst_negative_code_column_equal_rowsrow_table) + (dst_negative_scale_column_equal_rowsrow_table)) + ((dst_negative_scale_column_equal_rowsrow_table) + (dst_negative_scale_column_equal_rowsrow_table)))) * S ((((dst_positive_code_column_equal_rowsrow_table) + (dst_positive_scale_column_equal_rowsrow_table)) * S ((dst_positive_code_column_equal_rowsrow_table) + (dst_positive_scale_column_equal_rowsrow_table)) + ((dst_positive_scale_column_equal_rowsrow_table) + (dst_positive_scale_column_equal_rowsrow_table))) + (((dst_negative_code_column_equal_rowsrow_table) + (dst_negative_scale_column_equal_rowsrow_table)) * S ((dst_negative_code_column_equal_rowsrow_table) + (dst_negative_scale_column_equal_rowsrow_table)) + ((dst_negative_scale_column_equal_rowsrow_table) + (dst_negative_scale_column_equal_rowsrow_table)))) + ((((dst_negative_code_column_equal_rowsrow_table) + (dst_negative_scale_column_equal_rowsrow_table)) * S ((dst_negative_code_column_equal_rowsrow_table) + (dst_negative_scale_column_equal_rowsrow_table)) + ((dst_negative_scale_column_equal_rowsrow_table) + (dst_negative_scale_column_equal_rowsrow_table))) + (((dst_negative_code_column_equal_rowsrow_table) + (dst_negative_scale_column_equal_rowsrow_table)) * S ((dst_negative_code_column_equal_rowsrow_table) + (dst_negative_scale_column_equal_rowsrow_table)) + ((dst_negative_scale_column_equal_rowsrow_table) + (dst_negative_scale_column_equal_rowsrow_table)))))) /\ (forall dst_index_column_equal_rowsrow_table. (exists pvs_le_gap_column_equal_rowsrow_tabledomain. pvs_le_gap_column_equal_rowsrow_tabledomain + (dst_index_column_equal_rowsrow_table) = (M)) -> exists dst_positive_column_equal_rowsrow_table dst_negative_column_equal_rowsrow_table dst_value_column_equal_rowsrow_table. ((((exists ff_h_pvs_column_equal_rowsrow_tableentrypositive. ff_h_pvs_column_equal_rowsrow_tableentrypositive + S (dst_positive_column_equal_rowsrow_table) = S ((S (dst_index_column_equal_rowsrow_table)) * dst_positive_scale_column_equal_rowsrow_table)) /\ exists ff_q_pvs_column_equal_rowsrow_tableentrypositive. dst_positive_code_column_equal_rowsrow_table = ff_q_pvs_column_equal_rowsrow_tableentrypositive * S ((S (dst_index_column_equal_rowsrow_table)) * dst_positive_scale_column_equal_rowsrow_table) + (dst_positive_column_equal_rowsrow_table))) /\ (((((exists ff_h_pvs_column_equal_rowsrow_tableentrynegative. ff_h_pvs_column_equal_rowsrow_tableentrynegative + S (dst_negative_column_equal_rowsrow_table) = S ((S (dst_index_column_equal_rowsrow_table)) * dst_negative_scale_column_equal_rowsrow_table)) /\ exists ff_q_pvs_column_equal_rowsrow_tableentrynegative. dst_negative_code_column_equal_rowsrow_table = ff_q_pvs_column_equal_rowsrow_tableentrynegative * S ((S (dst_index_column_equal_rowsrow_table)) * dst_negative_scale_column_equal_rowsrow_table) + (dst_negative_column_equal_rowsrow_table))) /\ (exists ge_balance_positive_column_equal_rowsrow_tableentryvalue ge_balance_negative_column_equal_rowsrow_tableentryvalue. (((((dst_value_column_equal_rowsrow_table) = 2 * (ge_balance_positive_column_equal_rowsrow_tableentryvalue) /\ (ge_balance_negative_column_equal_rowsrow_tableentryvalue) = 0) \/ exists ge_signed_half_column_equal_rowsrow_tableentryvaluedecode. (((dst_value_column_equal_rowsrow_table) = 2 * ge_signed_half_column_equal_rowsrow_tableentryvaluedecode + 1 /\ (ge_balance_positive_column_equal_rowsrow_tableentryvalue) = 0) /\ (ge_balance_negative_column_equal_rowsrow_tableentryvalue) = S ge_signed_half_column_equal_rowsrow_tableentryvaluedecode))) /\ ((dst_positive_column_equal_rowsrow_table) + ge_balance_negative_column_equal_rowsrow_tableentryvalue = (dst_negative_column_equal_rowsrow_table) + ge_balance_positive_column_equal_rowsrow_tableentryvalue))))))))) /\ (forall srt_index_column_equal_rows. (exists pvs_gap_column_equal_rowsbound. pvs_gap_column_equal_rowsbound + S (srt_index_column_equal_rows) = (M)) -> exists srt_value_column_equal_rows. (((exists dst_positive_code_column_equal_rowsrowentry dst_positive_scale_column_equal_rowsrowentry dst_negative_code_column_equal_rowsrowentry dst_negative_scale_column_equal_rowsrowentry dst_positive_column_equal_rowsrowentry dst_negative_column_equal_rowsrowentry. (((C) = (((((dst_positive_code_column_equal_rowsrowentry) + (dst_positive_scale_column_equal_rowsrowentry)) * S ((dst_positive_code_column_equal_rowsrowentry) + (dst_positive_scale_column_equal_rowsrowentry)) + ((dst_positive_scale_column_equal_rowsrowentry) + (dst_positive_scale_column_equal_rowsrowentry))) + (((dst_negative_code_column_equal_rowsrowentry) + (dst_negative_scale_column_equal_rowsrowentry)) * S ((dst_negative_code_column_equal_rowsrowentry) + (dst_negative_scale_column_equal_rowsrowentry)) + ((dst_negative_scale_column_equal_rowsrowentry) + (dst_negative_scale_column_equal_rowsrowentry)))) * S ((((dst_positive_code_column_equal_rowsrowentry) + (dst_positive_scale_column_equal_rowsrowentry)) * S ((dst_positive_code_column_equal_rowsrowentry) + (dst_positive_scale_column_equal_rowsrowentry)) + ((dst_positive_scale_column_equal_rowsrowentry) + (dst_positive_scale_column_equal_rowsrowentry))) + (((dst_negative_code_column_equal_rowsrowentry) + (dst_negative_scale_column_equal_rowsrowentry)) * S ((dst_negative_code_column_equal_rowsrowentry) + (dst_negative_scale_column_equal_rowsrowentry)) + ((dst_negative_scale_column_equal_rowsrowentry) + (dst_negative_scale_column_equal_rowsrowentry)))) + ((((dst_negative_code_column_equal_rowsrowentry) + (dst_negative_scale_column_equal_rowsrowentry)) * S ((dst_negative_code_column_equal_rowsrowentry) + (dst_negative_scale_column_equal_rowsrowentry)) + ((dst_negative_scale_column_equal_rowsrowentry) + (dst_negative_scale_column_equal_rowsrowentry))) + (((dst_negative_code_column_equal_rowsrowentry) + (dst_negative_scale_column_equal_rowsrowentry)) * S ((dst_negative_code_column_equal_rowsrowentry) + (dst_negative_scale_column_equal_rowsrowentry)) + ((dst_negative_scale_column_equal_rowsrowentry) + (dst_negative_scale_column_equal_rowsrowentry)))))) /\ (((((exists ff_h_pvs_column_equal_rowsrowentrypositive. ff_h_pvs_column_equal_rowsrowentrypositive + S (dst_positive_column_equal_rowsrowentry) = S ((S (srt_index_column_equal_rows)) * dst_positive_scale_column_equal_rowsrowentry)) /\ exists ff_q_pvs_column_equal_rowsrowentrypositive. dst_positive_code_column_equal_rowsrowentry = ff_q_pvs_column_equal_rowsrowentrypositive * S ((S (srt_index_column_equal_rows)) * dst_positive_scale_column_equal_rowsrowentry) + (dst_positive_column_equal_rowsrowentry))) /\ (((((exists ff_h_pvs_column_equal_rowsrowentrynegative. ff_h_pvs_column_equal_rowsrowentrynegative + S (dst_negative_column_equal_rowsrowentry) = S ((S (srt_index_column_equal_rows)) * dst_negative_scale_column_equal_rowsrowentry)) /\ exists ff_q_pvs_column_equal_rowsrowentrynegative. dst_negative_code_column_equal_rowsrowentry = ff_q_pvs_column_equal_rowsrowentrynegative * S ((S (srt_index_column_equal_rows)) * dst_negative_scale_column_equal_rowsrowentry) + (dst_negative_column_equal_rowsrowentry))) /\ (exists ge_balance_positive_column_equal_rowsrowentryvalue ge_balance_negative_column_equal_rowsrowentryvalue. (((((srt_value_column_equal_rows) = 2 * (ge_balance_positive_column_equal_rowsrowentryvalue) /\ (ge_balance_negative_column_equal_rowsrowentryvalue) = 0) \/ exists ge_signed_half_column_equal_rowsrowentryvaluedecode. (((srt_value_column_equal_rows) = 2 * ge_signed_half_column_equal_rowsrowentryvaluedecode + 1 /\ (ge_balance_positive_column_equal_rowsrowentryvalue) = 0) /\ (ge_balance_negative_column_equal_rowsrowentryvalue) = S ge_signed_half_column_equal_rowsrowentryvaluedecode))) /\ ((dst_positive_column_equal_rowsrowentry) + ge_balance_negative_column_equal_rowsrowentryvalue = (dst_negative_column_equal_rowsrowentry) + ge_balance_positive_column_equal_rowsrowentryvalue))))))))) /\ (exists srs_slice_column_equal_rowsrowrow_sum. ((((exists dst_positive_code_column_equal_rowsrowrow_sumslicesource_table dst_positive_scale_column_equal_rowsrowrow_sumslicesource_table dst_negative_code_column_equal_rowsrowrow_sumslicesource_table dst_negative_scale_column_equal_rowsrowrow_sumslicesource_table. (((T) = (((((dst_positive_code_column_equal_rowsrowrow_sumslicesource_table) + (dst_positive_scale_column_equal_rowsrowrow_sumslicesource_table)) * S ((dst_positive_code_column_equal_rowsrowrow_sumslicesource_table) + (dst_positive_scale_column_equal_rowsrowrow_sumslicesource_table)) + ((dst_positive_scale_column_equal_rowsrowrow_sumslicesource_table) + (dst_positive_scale_column_equal_rowsrowrow_sumslicesource_table))) + (((dst_negative_code_column_equal_rowsrowrow_sumslicesource_table) + (dst_negative_scale_column_equal_rowsrowrow_sumslicesource_table)) * S ((dst_negative_code_column_equal_rowsrowrow_sumslicesource_table) + (dst_negative_scale_column_equal_rowsrowrow_sumslicesource_table)) + ((dst_negative_scale_column_equal_rowsrowrow_sumslicesource_table) + (dst_negative_scale_column_equal_rowsrowrow_sumslicesource_table)))) * S ((((dst_positive_code_column_equal_rowsrowrow_sumslicesource_table) + (dst_positive_scale_column_equal_rowsrowrow_sumslicesource_table)) * S ((dst_positive_code_column_equal_rowsrowrow_sumslicesource_table) + (dst_positive_scale_column_equal_rowsrowrow_sumslicesource_table)) + ((dst_positive_scale_column_equal_rowsrowrow_sumslicesource_table) + (dst_positive_scale_column_equal_rowsrowrow_sumslicesource_table))) + (((dst_negative_code_column_equal_rowsrowrow_sumslicesource_table) + (dst_negative_scale_column_equal_rowsrowrow_sumslicesource_table)) * S ((dst_negative_code_column_equal_rowsrowrow_sumslicesource_table) + (dst_negative_scale_column_equal_rowsrowrow_sumslicesource_table)) + ((dst_negative_scale_column_equal_rowsrowrow_sumslicesource_table) + (dst_negative_scale_column_equal_rowsrowrow_sumslicesource_table)))) + ((((dst_negative_code_column_equal_rowsrowrow_sumslicesource_table) + (dst_negative_scale_column_equal_rowsrowrow_sumslicesource_table)) * S ((dst_negative_code_column_equal_rowsrowrow_sumslicesource_table) + (dst_negative_scale_column_equal_rowsrowrow_sumslicesource_table)) + ((dst_negative_scale_column_equal_rowsrowrow_sumslicesource_table) + (dst_negative_scale_column_equal_rowsrowrow_sumslicesource_table))) + (((dst_negative_code_column_equal_rowsrowrow_sumslicesource_table) + (dst_negative_scale_column_equal_rowsrowrow_sumslicesource_table)) * S ((dst_negative_code_column_equal_rowsrowrow_sumslicesource_table) + (dst_negative_scale_column_equal_rowsrowrow_sumslicesource_table)) + ((dst_negative_scale_column_equal_rowsrowrow_sumslicesource_table) + (dst_negative_scale_column_equal_rowsrowrow_sumslicesource_table)))))) /\ (forall dst_index_column_equal_rowsrowrow_sumslicesource_table. (exists pvs_le_gap_column_equal_rowsrowrow_sumslicesource_tabledomain. pvs_le_gap_column_equal_rowsrowrow_sumslicesource_tabledomain + (dst_index_column_equal_rowsrowrow_sumslicesource_table) = (0)) -> exists dst_positive_column_equal_rowsrowrow_sumslicesource_table dst_negative_column_equal_rowsrowrow_sumslicesource_table dst_value_column_equal_rowsrowrow_sumslicesource_table. ((((exists ff_h_pvs_column_equal_rowsrowrow_sumslicesource_tableentrypositive. ff_h_pvs_column_equal_rowsrowrow_sumslicesource_tableentrypositive + S (dst_positive_column_equal_rowsrowrow_sumslicesource_table) = S ((S (dst_index_column_equal_rowsrowrow_sumslicesource_table)) * dst_positive_scale_column_equal_rowsrowrow_sumslicesource_table)) /\ exists ff_q_pvs_column_equal_rowsrowrow_sumslicesource_tableentrypositive. dst_positive_code_column_equal_rowsrowrow_sumslicesource_table = ff_q_pvs_column_equal_rowsrowrow_sumslicesource_tableentrypositive * S ((S (dst_index_column_equal_rowsrowrow_sumslicesource_table)) * dst_positive_scale_column_equal_rowsrowrow_sumslicesource_table) + (dst_positive_column_equal_rowsrowrow_sumslicesource_table))) /\ (((((exists ff_h_pvs_column_equal_rowsrowrow_sumslicesource_tableentrynegative. ff_h_pvs_column_equal_rowsrowrow_sumslicesource_tableentrynegative + S (dst_negative_column_equal_rowsrowrow_sumslicesource_table) = S ((S (dst_index_column_equal_rowsrowrow_sumslicesource_table)) * dst_negative_scale_column_equal_rowsrowrow_sumslicesource_table)) /\ exists ff_q_pvs_column_equal_rowsrowrow_sumslicesource_tableentrynegative. dst_negative_code_column_equal_rowsrowrow_sumslicesource_table = ff_q_pvs_column_equal_rowsrowrow_sumslicesource_tableentrynegative * S ((S (dst_index_column_equal_rowsrowrow_sumslicesource_table)) * dst_negative_scale_column_equal_rowsrowrow_sumslicesource_table) + (dst_negative_column_equal_rowsrowrow_sumslicesource_table))) /\ (exists ge_balance_positive_column_equal_rowsrowrow_sumslicesource_tableentryvalue ge_balance_negative_column_equal_rowsrowrow_sumslicesource_tableentryvalue. (((((dst_value_column_equal_rowsrowrow_sumslicesource_table) = 2 * (ge_balance_positive_column_equal_rowsrowrow_sumslicesource_tableentryvalue) /\ (ge_balance_negative_column_equal_rowsrowrow_sumslicesource_tableentryvalue) = 0) \/ exists ge_signed_half_column_equal_rowsrowrow_sumslicesource_tableentryvaluedecode. (((dst_value_column_equal_rowsrowrow_sumslicesource_table) = 2 * ge_signed_half_column_equal_rowsrowrow_sumslicesource_tableentryvaluedecode + 1 /\ (ge_balance_positive_column_equal_rowsrowrow_sumslicesource_tableentryvalue) = 0) /\ (ge_balance_negative_column_equal_rowsrowrow_sumslicesource_tableentryvalue) = S ge_signed_half_column_equal_rowsrowrow_sumslicesource_tableentryvaluedecode))) /\ ((dst_positive_column_equal_rowsrowrow_sumslicesource_table) + ge_balance_negative_column_equal_rowsrowrow_sumslicesource_tableentryvalue = (dst_negative_column_equal_rowsrowrow_sumslicesource_table) + ge_balance_positive_column_equal_rowsrowrow_sumslicesource_tableentryvalue))))))))) /\ (((exists dst_positive_code_column_equal_rowsrowrow_sumsliceoutput_table dst_positive_scale_column_equal_rowsrowrow_sumsliceoutput_table dst_negative_code_column_equal_rowsrowrow_sumsliceoutput_table dst_negative_scale_column_equal_rowsrowrow_sumsliceoutput_table. (((srs_slice_column_equal_rowsrowrow_sum) = (((((dst_positive_code_column_equal_rowsrowrow_sumsliceoutput_table) + (dst_positive_scale_column_equal_rowsrowrow_sumsliceoutput_table)) * S ((dst_positive_code_column_equal_rowsrowrow_sumsliceoutput_table) + (dst_positive_scale_column_equal_rowsrowrow_sumsliceoutput_table)) + ((dst_positive_scale_column_equal_rowsrowrow_sumsliceoutput_table) + (dst_positive_scale_column_equal_rowsrowrow_sumsliceoutput_table))) + (((dst_negative_code_column_equal_rowsrowrow_sumsliceoutput_table) + (dst_negative_scale_column_equal_rowsrowrow_sumsliceoutput_table)) * S ((dst_negative_code_column_equal_rowsrowrow_sumsliceoutput_table) + (dst_negative_scale_column_equal_rowsrowrow_sumsliceoutput_table)) + ((dst_negative_scale_column_equal_rowsrowrow_sumsliceoutput_table) + (dst_negative_scale_column_equal_rowsrowrow_sumsliceoutput_table)))) * S ((((dst_positive_code_column_equal_rowsrowrow_sumsliceoutput_table) + (dst_positive_scale_column_equal_rowsrowrow_sumsliceoutput_table)) * S ((dst_positive_code_column_equal_rowsrowrow_sumsliceoutput_table) + (dst_positive_scale_column_equal_rowsrowrow_sumsliceoutput_table)) + ((dst_positive_scale_column_equal_rowsrowrow_sumsliceoutput_table) + (dst_positive_scale_column_equal_rowsrowrow_sumsliceoutput_table))) + (((dst_negative_code_column_equal_rowsrowrow_sumsliceoutput_table) + (dst_negative_scale_column_equal_rowsrowrow_sumsliceoutput_table)) * S ((dst_negative_code_column_equal_rowsrowrow_sumsliceoutput_table) + (dst_negative_scale_column_equal_rowsrowrow_sumsliceoutput_table)) + ((dst_negative_scale_column_equal_rowsrowrow_sumsliceoutput_table) + (dst_negative_scale_column_equal_rowsrowrow_sumsliceoutput_table)))) + ((((dst_negative_code_column_equal_rowsrowrow_sumsliceoutput_table) + (dst_negative_scale_column_equal_rowsrowrow_sumsliceoutput_table)) * S ((dst_negative_code_column_equal_rowsrowrow_sumsliceoutput_table) + (dst_negative_scale_column_equal_rowsrowrow_sumsliceoutput_table)) + ((dst_negative_scale_column_equal_rowsrowrow_sumsliceoutput_table) + (dst_negative_scale_column_equal_rowsrowrow_sumsliceoutput_table))) + (((dst_negative_code_column_equal_rowsrowrow_sumsliceoutput_table) + (dst_negative_scale_column_equal_rowsrowrow_sumsliceoutput_table)) * S ((dst_negative_code_column_equal_rowsrowrow_sumsliceoutput_table) + (dst_negative_scale_column_equal_rowsrowrow_sumsliceoutput_table)) + ((dst_negative_scale_column_equal_rowsrowrow_sumsliceoutput_table) + (dst_negative_scale_column_equal_rowsrowrow_sumsliceoutput_table)))))) /\ (forall dst_index_column_equal_rowsrowrow_sumsliceoutput_table. (exists pvs_le_gap_column_equal_rowsrowrow_sumsliceoutput_tabledomain. pvs_le_gap_column_equal_rowsrowrow_sumsliceoutput_tabledomain + (dst_index_column_equal_rowsrowrow_sumsliceoutput_table) = (L)) -> exists dst_positive_column_equal_rowsrowrow_sumsliceoutput_table dst_negative_column_equal_rowsrowrow_sumsliceoutput_table dst_value_column_equal_rowsrowrow_sumsliceoutput_table. ((((exists ff_h_pvs_column_equal_rowsrowrow_sumsliceoutput_tableentrypositive. ff_h_pvs_column_equal_rowsrowrow_sumsliceoutput_tableentrypositive + S (dst_positive_column_equal_rowsrowrow_sumsliceoutput_table) = S ((S (dst_index_column_equal_rowsrowrow_sumsliceoutput_table)) * dst_positive_scale_column_equal_rowsrowrow_sumsliceoutput_table)) /\ exists ff_q_pvs_column_equal_rowsrowrow_sumsliceoutput_tableentrypositive. dst_positive_code_column_equal_rowsrowrow_sumsliceoutput_table = ff_q_pvs_column_equal_rowsrowrow_sumsliceoutput_tableentrypositive * S ((S (dst_index_column_equal_rowsrowrow_sumsliceoutput_table)) * dst_positive_scale_column_equal_rowsrowrow_sumsliceoutput_table) + (dst_positive_column_equal_rowsrowrow_sumsliceoutput_table))) /\ (((((exists ff_h_pvs_column_equal_rowsrowrow_sumsliceoutput_tableentrynegative. ff_h_pvs_column_equal_rowsrowrow_sumsliceoutput_tableentrynegative + S (dst_negative_column_equal_rowsrowrow_sumsliceoutput_table) = S ((S (dst_index_column_equal_rowsrowrow_sumsliceoutput_table)) * dst_negative_scale_column_equal_rowsrowrow_sumsliceoutput_table)) /\ exists ff_q_pvs_column_equal_rowsrowrow_sumsliceoutput_tableentrynegative. dst_negative_code_column_equal_rowsrowrow_sumsliceoutput_table = ff_q_pvs_column_equal_rowsrowrow_sumsliceoutput_tableentrynegative * S ((S (dst_index_column_equal_rowsrowrow_sumsliceoutput_table)) * dst_negative_scale_column_equal_rowsrowrow_sumsliceoutput_table) + (dst_negative_column_equal_rowsrowrow_sumsliceoutput_table))) /\ (exists ge_balance_positive_column_equal_rowsrowrow_sumsliceoutput_tableentryvalue ge_balance_negative_column_equal_rowsrowrow_sumsliceoutput_tableentryvalue. (((((dst_value_column_equal_rowsrowrow_sumsliceoutput_table) = 2 * (ge_balance_positive_column_equal_rowsrowrow_sumsliceoutput_tableentryvalue) /\ (ge_balance_negative_column_equal_rowsrowrow_sumsliceoutput_tableentryvalue) = 0) \/ exists ge_signed_half_column_equal_rowsrowrow_sumsliceoutput_tableentryvaluedecode. (((dst_value_column_equal_rowsrowrow_sumsliceoutput_table) = 2 * ge_signed_half_column_equal_rowsrowrow_sumsliceoutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_column_equal_rowsrowrow_sumsliceoutput_tableentryvalue) = 0) /\ (ge_balance_negative_column_equal_rowsrowrow_sumsliceoutput_tableentryvalue) = S ge_signed_half_column_equal_rowsrowrow_sumsliceoutput_tableentryvaluedecode))) /\ ((dst_positive_column_equal_rowsrowrow_sumsliceoutput_table) + ge_balance_negative_column_equal_rowsrowrow_sumsliceoutput_tableentryvalue = (dst_negative_column_equal_rowsrowrow_sumsliceoutput_table) + ge_balance_positive_column_equal_rowsrowrow_sumsliceoutput_tableentryvalue))))))))) /\ (forall srs_index_column_equal_rowsrowrow_sumslice. (exists pvs_gap_column_equal_rowsrowrow_sumslicebound. pvs_gap_column_equal_rowsrowrow_sumslicebound + S (srs_index_column_equal_rowsrowrow_sumslice) = (L)) -> exists srs_value_column_equal_rowsrowrow_sumslice. (((exists dst_positive_code_column_equal_rowsrowrow_sumsliceentrysource dst_positive_scale_column_equal_rowsrowrow_sumsliceentrysource dst_negative_code_column_equal_rowsrowrow_sumsliceentrysource dst_negative_scale_column_equal_rowsrowrow_sumsliceentrysource dst_positive_column_equal_rowsrowrow_sumsliceentrysource dst_negative_column_equal_rowsrowrow_sumsliceentrysource. (((T) = (((((dst_positive_code_column_equal_rowsrowrow_sumsliceentrysource) + (dst_positive_scale_column_equal_rowsrowrow_sumsliceentrysource)) * S ((dst_positive_code_column_equal_rowsrowrow_sumsliceentrysource) + (dst_positive_scale_column_equal_rowsrowrow_sumsliceentrysource)) + ((dst_positive_scale_column_equal_rowsrowrow_sumsliceentrysource) + (dst_positive_scale_column_equal_rowsrowrow_sumsliceentrysource))) + (((dst_negative_code_column_equal_rowsrowrow_sumsliceentrysource) + (dst_negative_scale_column_equal_rowsrowrow_sumsliceentrysource)) * S ((dst_negative_code_column_equal_rowsrowrow_sumsliceentrysource) + (dst_negative_scale_column_equal_rowsrowrow_sumsliceentrysource)) + ((dst_negative_scale_column_equal_rowsrowrow_sumsliceentrysource) + (dst_negative_scale_column_equal_rowsrowrow_sumsliceentrysource)))) * S ((((dst_positive_code_column_equal_rowsrowrow_sumsliceentrysource) + (dst_positive_scale_column_equal_rowsrowrow_sumsliceentrysource)) * S ((dst_positive_code_column_equal_rowsrowrow_sumsliceentrysource) + (dst_positive_scale_column_equal_rowsrowrow_sumsliceentrysource)) + ((dst_positive_scale_column_equal_rowsrowrow_sumsliceentrysource) + (dst_positive_scale_column_equal_rowsrowrow_sumsliceentrysource))) + (((dst_negative_code_column_equal_rowsrowrow_sumsliceentrysource) + (dst_negative_scale_column_equal_rowsrowrow_sumsliceentrysource)) * S ((dst_negative_code_column_equal_rowsrowrow_sumsliceentrysource) + (dst_negative_scale_column_equal_rowsrowrow_sumsliceentrysource)) + ((dst_negative_scale_column_equal_rowsrowrow_sumsliceentrysource) + (dst_negative_scale_column_equal_rowsrowrow_sumsliceentrysource)))) + ((((dst_negative_code_column_equal_rowsrowrow_sumsliceentrysource) + (dst_negative_scale_column_equal_rowsrowrow_sumsliceentrysource)) * S ((dst_negative_code_column_equal_rowsrowrow_sumsliceentrysource) + (dst_negative_scale_column_equal_rowsrowrow_sumsliceentrysource)) + ((dst_negative_scale_column_equal_rowsrowrow_sumsliceentrysource) + (dst_negative_scale_column_equal_rowsrowrow_sumsliceentrysource))) + (((dst_negative_code_column_equal_rowsrowrow_sumsliceentrysource) + (dst_negative_scale_column_equal_rowsrowrow_sumsliceentrysource)) * S ((dst_negative_code_column_equal_rowsrowrow_sumsliceentrysource) + (dst_negative_scale_column_equal_rowsrowrow_sumsliceentrysource)) + ((dst_negative_scale_column_equal_rowsrowrow_sumsliceentrysource) + (dst_negative_scale_column_equal_rowsrowrow_sumsliceentrysource)))))) /\ (((((exists ff_h_pvs_column_equal_rowsrowrow_sumsliceentrysourcepositive. ff_h_pvs_column_equal_rowsrowrow_sumsliceentrysourcepositive + S (dst_positive_column_equal_rowsrowrow_sumsliceentrysource) = S ((S (((((0) + ((1) * (srt_index_column_equal_rows)))) + ((S M) * (srs_index_column_equal_rowsrowrow_sumslice))))) * dst_positive_scale_column_equal_rowsrowrow_sumsliceentrysource)) /\ exists ff_q_pvs_column_equal_rowsrowrow_sumsliceentrysourcepositive. dst_positive_code_column_equal_rowsrowrow_sumsliceentrysource = ff_q_pvs_column_equal_rowsrowrow_sumsliceentrysourcepositive * S ((S (((((0) + ((1) * (srt_index_column_equal_rows)))) + ((S M) * (srs_index_column_equal_rowsrowrow_sumslice))))) * dst_positive_scale_column_equal_rowsrowrow_sumsliceentrysource) + (dst_positive_column_equal_rowsrowrow_sumsliceentrysource))) /\ (((((exists ff_h_pvs_column_equal_rowsrowrow_sumsliceentrysourcenegative. ff_h_pvs_column_equal_rowsrowrow_sumsliceentrysourcenegative + S (dst_negative_column_equal_rowsrowrow_sumsliceentrysource) = S ((S (((((0) + ((1) * (srt_index_column_equal_rows)))) + ((S M) * (srs_index_column_equal_rowsrowrow_sumslice))))) * dst_negative_scale_column_equal_rowsrowrow_sumsliceentrysource)) /\ exists ff_q_pvs_column_equal_rowsrowrow_sumsliceentrysourcenegative. dst_negative_code_column_equal_rowsrowrow_sumsliceentrysource = ff_q_pvs_column_equal_rowsrowrow_sumsliceentrysourcenegative * S ((S (((((0) + ((1) * (srt_index_column_equal_rows)))) + ((S M) * (srs_index_column_equal_rowsrowrow_sumslice))))) * dst_negative_scale_column_equal_rowsrowrow_sumsliceentrysource) + (dst_negative_column_equal_rowsrowrow_sumsliceentrysource))) /\ (exists ge_balance_positive_column_equal_rowsrowrow_sumsliceentrysourcevalue ge_balance_negative_column_equal_rowsrowrow_sumsliceentrysourcevalue. (((((srs_value_column_equal_rowsrowrow_sumslice) = 2 * (ge_balance_positive_column_equal_rowsrowrow_sumsliceentrysourcevalue) /\ (ge_balance_negative_column_equal_rowsrowrow_sumsliceentrysourcevalue) = 0) \/ exists ge_signed_half_column_equal_rowsrowrow_sumsliceentrysourcevaluedecode. (((srs_value_column_equal_rowsrowrow_sumslice) = 2 * ge_signed_half_column_equal_rowsrowrow_sumsliceentrysourcevaluedecode + 1 /\ (ge_balance_positive_column_equal_rowsrowrow_sumsliceentrysourcevalue) = 0) /\ (ge_balance_negative_column_equal_rowsrowrow_sumsliceentrysourcevalue) = S ge_signed_half_column_equal_rowsrowrow_sumsliceentrysourcevaluedecode))) /\ ((dst_positive_column_equal_rowsrowrow_sumsliceentrysource) + ge_balance_negative_column_equal_rowsrowrow_sumsliceentrysourcevalue = (dst_negative_column_equal_rowsrowrow_sumsliceentrysource) + ge_balance_positive_column_equal_rowsrowrow_sumsliceentrysourcevalue))))))))) /\ (exists dst_positive_code_column_equal_rowsrowrow_sumsliceentryoutput dst_positive_scale_column_equal_rowsrowrow_sumsliceentryoutput dst_negative_code_column_equal_rowsrowrow_sumsliceentryoutput dst_negative_scale_column_equal_rowsrowrow_sumsliceentryoutput dst_positive_column_equal_rowsrowrow_sumsliceentryoutput dst_negative_column_equal_rowsrowrow_sumsliceentryoutput. (((srs_slice_column_equal_rowsrowrow_sum) = (((((dst_positive_code_column_equal_rowsrowrow_sumsliceentryoutput) + (dst_positive_scale_column_equal_rowsrowrow_sumsliceentryoutput)) * S ((dst_positive_code_column_equal_rowsrowrow_sumsliceentryoutput) + (dst_positive_scale_column_equal_rowsrowrow_sumsliceentryoutput)) + ((dst_positive_scale_column_equal_rowsrowrow_sumsliceentryoutput) + (dst_positive_scale_column_equal_rowsrowrow_sumsliceentryoutput))) + (((dst_negative_code_column_equal_rowsrowrow_sumsliceentryoutput) + (dst_negative_scale_column_equal_rowsrowrow_sumsliceentryoutput)) * S ((dst_negative_code_column_equal_rowsrowrow_sumsliceentryoutput) + (dst_negative_scale_column_equal_rowsrowrow_sumsliceentryoutput)) + ((dst_negative_scale_column_equal_rowsrowrow_sumsliceentryoutput) + (dst_negative_scale_column_equal_rowsrowrow_sumsliceentryoutput)))) * S ((((dst_positive_code_column_equal_rowsrowrow_sumsliceentryoutput) + (dst_positive_scale_column_equal_rowsrowrow_sumsliceentryoutput)) * S ((dst_positive_code_column_equal_rowsrowrow_sumsliceentryoutput) + (dst_positive_scale_column_equal_rowsrowrow_sumsliceentryoutput)) + ((dst_positive_scale_column_equal_rowsrowrow_sumsliceentryoutput) + (dst_positive_scale_column_equal_rowsrowrow_sumsliceentryoutput))) + (((dst_negative_code_column_equal_rowsrowrow_sumsliceentryoutput) + (dst_negative_scale_column_equal_rowsrowrow_sumsliceentryoutput)) * S ((dst_negative_code_column_equal_rowsrowrow_sumsliceentryoutput) + (dst_negative_scale_column_equal_rowsrowrow_sumsliceentryoutput)) + ((dst_negative_scale_column_equal_rowsrowrow_sumsliceentryoutput) + (dst_negative_scale_column_equal_rowsrowrow_sumsliceentryoutput)))) + ((((dst_negative_code_column_equal_rowsrowrow_sumsliceentryoutput) + (dst_negative_scale_column_equal_rowsrowrow_sumsliceentryoutput)) * S ((dst_negative_code_column_equal_rowsrowrow_sumsliceentryoutput) + (dst_negative_scale_column_equal_rowsrowrow_sumsliceentryoutput)) + ((dst_negative_scale_column_equal_rowsrowrow_sumsliceentryoutput) + (dst_negative_scale_column_equal_rowsrowrow_sumsliceentryoutput))) + (((dst_negative_code_column_equal_rowsrowrow_sumsliceentryoutput) + (dst_negative_scale_column_equal_rowsrowrow_sumsliceentryoutput)) * S ((dst_negative_code_column_equal_rowsrowrow_sumsliceentryoutput) + (dst_negative_scale_column_equal_rowsrowrow_sumsliceentryoutput)) + ((dst_negative_scale_column_equal_rowsrowrow_sumsliceentryoutput) + (dst_negative_scale_column_equal_rowsrowrow_sumsliceentryoutput)))))) /\ (((((exists ff_h_pvs_column_equal_rowsrowrow_sumsliceentryoutputpositive. ff_h_pvs_column_equal_rowsrowrow_sumsliceentryoutputpositive + S (dst_positive_column_equal_rowsrowrow_sumsliceentryoutput) = S ((S (srs_index_column_equal_rowsrowrow_sumslice)) * dst_positive_scale_column_equal_rowsrowrow_sumsliceentryoutput)) /\ exists ff_q_pvs_column_equal_rowsrowrow_sumsliceentryoutputpositive. dst_positive_code_column_equal_rowsrowrow_sumsliceentryoutput = ff_q_pvs_column_equal_rowsrowrow_sumsliceentryoutputpositive * S ((S (srs_index_column_equal_rowsrowrow_sumslice)) * dst_positive_scale_column_equal_rowsrowrow_sumsliceentryoutput) + (dst_positive_column_equal_rowsrowrow_sumsliceentryoutput))) /\ (((((exists ff_h_pvs_column_equal_rowsrowrow_sumsliceentryoutputnegative. ff_h_pvs_column_equal_rowsrowrow_sumsliceentryoutputnegative + S (dst_negative_column_equal_rowsrowrow_sumsliceentryoutput) = S ((S (srs_index_column_equal_rowsrowrow_sumslice)) * dst_negative_scale_column_equal_rowsrowrow_sumsliceentryoutput)) /\ exists ff_q_pvs_column_equal_rowsrowrow_sumsliceentryoutputnegative. dst_negative_code_column_equal_rowsrowrow_sumsliceentryoutput = ff_q_pvs_column_equal_rowsrowrow_sumsliceentryoutputnegative * S ((S (srs_index_column_equal_rowsrowrow_sumslice)) * dst_negative_scale_column_equal_rowsrowrow_sumsliceentryoutput) + (dst_negative_column_equal_rowsrowrow_sumsliceentryoutput))) /\ (exists ge_balance_positive_column_equal_rowsrowrow_sumsliceentryoutputvalue ge_balance_negative_column_equal_rowsrowrow_sumsliceentryoutputvalue. (((((srs_value_column_equal_rowsrowrow_sumslice) = 2 * (ge_balance_positive_column_equal_rowsrowrow_sumsliceentryoutputvalue) /\ (ge_balance_negative_column_equal_rowsrowrow_sumsliceentryoutputvalue) = 0) \/ exists ge_signed_half_column_equal_rowsrowrow_sumsliceentryoutputvaluedecode. (((srs_value_column_equal_rowsrowrow_sumslice) = 2 * ge_signed_half_column_equal_rowsrowrow_sumsliceentryoutputvaluedecode + 1 /\ (ge_balance_positive_column_equal_rowsrowrow_sumsliceentryoutputvalue) = 0) /\ (ge_balance_negative_column_equal_rowsrowrow_sumsliceentryoutputvalue) = S ge_signed_half_column_equal_rowsrowrow_sumsliceentryoutputvaluedecode))) /\ ((dst_positive_column_equal_rowsrowrow_sumsliceentryoutput) + ge_balance_negative_column_equal_rowsrowrow_sumsliceentryoutputvalue = (dst_negative_column_equal_rowsrowrow_sumsliceentryoutput) + ge_balance_positive_column_equal_rowsrowrow_sumsliceentryoutputvalue)))))))))))))))) /\ (exists dst_positive_code_column_equal_rowsrowrow_sumsum dst_positive_scale_column_equal_rowsrowrow_sumsum dst_negative_code_column_equal_rowsrowrow_sumsum dst_negative_scale_column_equal_rowsrowrow_sumsum dst_positive_sum_column_equal_rowsrowrow_sumsum dst_negative_sum_column_equal_rowsrowrow_sumsum. (((srs_slice_column_equal_rowsrowrow_sum) = (((((dst_positive_code_column_equal_rowsrowrow_sumsum) + (dst_positive_scale_column_equal_rowsrowrow_sumsum)) * S ((dst_positive_code_column_equal_rowsrowrow_sumsum) + (dst_positive_scale_column_equal_rowsrowrow_sumsum)) + ((dst_positive_scale_column_equal_rowsrowrow_sumsum) + (dst_positive_scale_column_equal_rowsrowrow_sumsum))) + (((dst_negative_code_column_equal_rowsrowrow_sumsum) + (dst_negative_scale_column_equal_rowsrowrow_sumsum)) * S ((dst_negative_code_column_equal_rowsrowrow_sumsum) + (dst_negative_scale_column_equal_rowsrowrow_sumsum)) + ((dst_negative_scale_column_equal_rowsrowrow_sumsum) + (dst_negative_scale_column_equal_rowsrowrow_sumsum)))) * S ((((dst_positive_code_column_equal_rowsrowrow_sumsum) + (dst_positive_scale_column_equal_rowsrowrow_sumsum)) * S ((dst_positive_code_column_equal_rowsrowrow_sumsum) + (dst_positive_scale_column_equal_rowsrowrow_sumsum)) + ((dst_positive_scale_column_equal_rowsrowrow_sumsum) + (dst_positive_scale_column_equal_rowsrowrow_sumsum))) + (((dst_negative_code_column_equal_rowsrowrow_sumsum) + (dst_negative_scale_column_equal_rowsrowrow_sumsum)) * S ((dst_negative_code_column_equal_rowsrowrow_sumsum) + (dst_negative_scale_column_equal_rowsrowrow_sumsum)) + ((dst_negative_scale_column_equal_rowsrowrow_sumsum) + (dst_negative_scale_column_equal_rowsrowrow_sumsum)))) + ((((dst_negative_code_column_equal_rowsrowrow_sumsum) + (dst_negative_scale_column_equal_rowsrowrow_sumsum)) * S ((dst_negative_code_column_equal_rowsrowrow_sumsum) + (dst_negative_scale_column_equal_rowsrowrow_sumsum)) + ((dst_negative_scale_column_equal_rowsrowrow_sumsum) + (dst_negative_scale_column_equal_rowsrowrow_sumsum))) + (((dst_negative_code_column_equal_rowsrowrow_sumsum) + (dst_negative_scale_column_equal_rowsrowrow_sumsum)) * S ((dst_negative_code_column_equal_rowsrowrow_sumsum) + (dst_negative_scale_column_equal_rowsrowrow_sumsum)) + ((dst_negative_scale_column_equal_rowsrowrow_sumsum) + (dst_negative_scale_column_equal_rowsrowrow_sumsum)))))) /\ (((exists fs_u_dst_column_equal_rowsrowrow_sumsumpositive fs_v_dst_column_equal_rowsrowrow_sumsumpositive. ((((exists fs_h_dst_column_equal_rowsrowrow_sumsumpositive_body_start. fs_h_dst_column_equal_rowsrowrow_sumsumpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_column_equal_rowsrowrow_sumsumpositive)) /\ exists fs_q_dst_column_equal_rowsrowrow_sumsumpositive_body_start. fs_u_dst_column_equal_rowsrowrow_sumsumpositive = fs_q_dst_column_equal_rowsrowrow_sumsumpositive_body_start * S ((S (0)) * fs_v_dst_column_equal_rowsrowrow_sumsumpositive) + (0))) /\ ((((exists fs_h_dst_column_equal_rowsrowrow_sumsumpositive_body_terminal. fs_h_dst_column_equal_rowsrowrow_sumsumpositive_body_terminal + S (dst_positive_sum_column_equal_rowsrowrow_sumsum) = S ((S (L)) * fs_v_dst_column_equal_rowsrowrow_sumsumpositive)) /\ exists fs_q_dst_column_equal_rowsrowrow_sumsumpositive_body_terminal. fs_u_dst_column_equal_rowsrowrow_sumsumpositive = fs_q_dst_column_equal_rowsrowrow_sumsumpositive_body_terminal * S ((S (L)) * fs_v_dst_column_equal_rowsrowrow_sumsumpositive) + (dst_positive_sum_column_equal_rowsrowrow_sumsum))) /\ forall fs_i_dst_column_equal_rowsrowrow_sumsumpositive_body_steps. (exists fs_lt_dst_column_equal_rowsrowrow_sumsumpositive_body_steps_bound. fs_lt_dst_column_equal_rowsrowrow_sumsumpositive_body_steps_bound + S fs_i_dst_column_equal_rowsrowrow_sumsumpositive_body_steps = L) -> exists fs_a_dst_column_equal_rowsrowrow_sumsumpositive_body_steps fs_r_dst_column_equal_rowsrowrow_sumsumpositive_body_steps fs_s_dst_column_equal_rowsrowrow_sumsumpositive_body_steps. ((((exists fs_h_dst_column_equal_rowsrowrow_sumsumpositive_body_steps_summand. fs_h_dst_column_equal_rowsrowrow_sumsumpositive_body_steps_summand + S (fs_a_dst_column_equal_rowsrowrow_sumsumpositive_body_steps) = S ((S (fs_i_dst_column_equal_rowsrowrow_sumsumpositive_body_steps)) * dst_positive_scale_column_equal_rowsrowrow_sumsum)) /\ exists fs_q_dst_column_equal_rowsrowrow_sumsumpositive_body_steps_summand. dst_positive_code_column_equal_rowsrowrow_sumsum = fs_q_dst_column_equal_rowsrowrow_sumsumpositive_body_steps_summand * S ((S (fs_i_dst_column_equal_rowsrowrow_sumsumpositive_body_steps)) * dst_positive_scale_column_equal_rowsrowrow_sumsum) + (fs_a_dst_column_equal_rowsrowrow_sumsumpositive_body_steps))) /\ ((((exists fs_h_dst_column_equal_rowsrowrow_sumsumpositive_body_steps_partial. fs_h_dst_column_equal_rowsrowrow_sumsumpositive_body_steps_partial + S (fs_r_dst_column_equal_rowsrowrow_sumsumpositive_body_steps) = S ((S (fs_i_dst_column_equal_rowsrowrow_sumsumpositive_body_steps)) * fs_v_dst_column_equal_rowsrowrow_sumsumpositive)) /\ exists fs_q_dst_column_equal_rowsrowrow_sumsumpositive_body_steps_partial. fs_u_dst_column_equal_rowsrowrow_sumsumpositive = fs_q_dst_column_equal_rowsrowrow_sumsumpositive_body_steps_partial * S ((S (fs_i_dst_column_equal_rowsrowrow_sumsumpositive_body_steps)) * fs_v_dst_column_equal_rowsrowrow_sumsumpositive) + (fs_r_dst_column_equal_rowsrowrow_sumsumpositive_body_steps))) /\ ((((exists fs_h_dst_column_equal_rowsrowrow_sumsumpositive_body_steps_successor. fs_h_dst_column_equal_rowsrowrow_sumsumpositive_body_steps_successor + S (fs_s_dst_column_equal_rowsrowrow_sumsumpositive_body_steps) = S ((S (S fs_i_dst_column_equal_rowsrowrow_sumsumpositive_body_steps)) * fs_v_dst_column_equal_rowsrowrow_sumsumpositive)) /\ exists fs_q_dst_column_equal_rowsrowrow_sumsumpositive_body_steps_successor. fs_u_dst_column_equal_rowsrowrow_sumsumpositive = fs_q_dst_column_equal_rowsrowrow_sumsumpositive_body_steps_successor * S ((S (S fs_i_dst_column_equal_rowsrowrow_sumsumpositive_body_steps)) * fs_v_dst_column_equal_rowsrowrow_sumsumpositive) + (fs_s_dst_column_equal_rowsrowrow_sumsumpositive_body_steps))) /\ fs_s_dst_column_equal_rowsrowrow_sumsumpositive_body_steps = fs_r_dst_column_equal_rowsrowrow_sumsumpositive_body_steps + fs_a_dst_column_equal_rowsrowrow_sumsumpositive_body_steps)))))) /\ (((exists fs_u_dst_column_equal_rowsrowrow_sumsumnegative fs_v_dst_column_equal_rowsrowrow_sumsumnegative. ((((exists fs_h_dst_column_equal_rowsrowrow_sumsumnegative_body_start. fs_h_dst_column_equal_rowsrowrow_sumsumnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_column_equal_rowsrowrow_sumsumnegative)) /\ exists fs_q_dst_column_equal_rowsrowrow_sumsumnegative_body_start. fs_u_dst_column_equal_rowsrowrow_sumsumnegative = fs_q_dst_column_equal_rowsrowrow_sumsumnegative_body_start * S ((S (0)) * fs_v_dst_column_equal_rowsrowrow_sumsumnegative) + (0))) /\ ((((exists fs_h_dst_column_equal_rowsrowrow_sumsumnegative_body_terminal. fs_h_dst_column_equal_rowsrowrow_sumsumnegative_body_terminal + S (dst_negative_sum_column_equal_rowsrowrow_sumsum) = S ((S (L)) * fs_v_dst_column_equal_rowsrowrow_sumsumnegative)) /\ exists fs_q_dst_column_equal_rowsrowrow_sumsumnegative_body_terminal. fs_u_dst_column_equal_rowsrowrow_sumsumnegative = fs_q_dst_column_equal_rowsrowrow_sumsumnegative_body_terminal * S ((S (L)) * fs_v_dst_column_equal_rowsrowrow_sumsumnegative) + (dst_negative_sum_column_equal_rowsrowrow_sumsum))) /\ forall fs_i_dst_column_equal_rowsrowrow_sumsumnegative_body_steps. (exists fs_lt_dst_column_equal_rowsrowrow_sumsumnegative_body_steps_bound. fs_lt_dst_column_equal_rowsrowrow_sumsumnegative_body_steps_bound + S fs_i_dst_column_equal_rowsrowrow_sumsumnegative_body_steps = L) -> exists fs_a_dst_column_equal_rowsrowrow_sumsumnegative_body_steps fs_r_dst_column_equal_rowsrowrow_sumsumnegative_body_steps fs_s_dst_column_equal_rowsrowrow_sumsumnegative_body_steps. ((((exists fs_h_dst_column_equal_rowsrowrow_sumsumnegative_body_steps_summand. fs_h_dst_column_equal_rowsrowrow_sumsumnegative_body_steps_summand + S (fs_a_dst_column_equal_rowsrowrow_sumsumnegative_body_steps) = S ((S (fs_i_dst_column_equal_rowsrowrow_sumsumnegative_body_steps)) * dst_negative_scale_column_equal_rowsrowrow_sumsum)) /\ exists fs_q_dst_column_equal_rowsrowrow_sumsumnegative_body_steps_summand. dst_negative_code_column_equal_rowsrowrow_sumsum = fs_q_dst_column_equal_rowsrowrow_sumsumnegative_body_steps_summand * S ((S (fs_i_dst_column_equal_rowsrowrow_sumsumnegative_body_steps)) * dst_negative_scale_column_equal_rowsrowrow_sumsum) + (fs_a_dst_column_equal_rowsrowrow_sumsumnegative_body_steps))) /\ ((((exists fs_h_dst_column_equal_rowsrowrow_sumsumnegative_body_steps_partial. fs_h_dst_column_equal_rowsrowrow_sumsumnegative_body_steps_partial + S (fs_r_dst_column_equal_rowsrowrow_sumsumnegative_body_steps) = S ((S (fs_i_dst_column_equal_rowsrowrow_sumsumnegative_body_steps)) * fs_v_dst_column_equal_rowsrowrow_sumsumnegative)) /\ exists fs_q_dst_column_equal_rowsrowrow_sumsumnegative_body_steps_partial. fs_u_dst_column_equal_rowsrowrow_sumsumnegative = fs_q_dst_column_equal_rowsrowrow_sumsumnegative_body_steps_partial * S ((S (fs_i_dst_column_equal_rowsrowrow_sumsumnegative_body_steps)) * fs_v_dst_column_equal_rowsrowrow_sumsumnegative) + (fs_r_dst_column_equal_rowsrowrow_sumsumnegative_body_steps))) /\ ((((exists fs_h_dst_column_equal_rowsrowrow_sumsumnegative_body_steps_successor. fs_h_dst_column_equal_rowsrowrow_sumsumnegative_body_steps_successor + S (fs_s_dst_column_equal_rowsrowrow_sumsumnegative_body_steps) = S ((S (S fs_i_dst_column_equal_rowsrowrow_sumsumnegative_body_steps)) * fs_v_dst_column_equal_rowsrowrow_sumsumnegative)) /\ exists fs_q_dst_column_equal_rowsrowrow_sumsumnegative_body_steps_successor. fs_u_dst_column_equal_rowsrowrow_sumsumnegative = fs_q_dst_column_equal_rowsrowrow_sumsumnegative_body_steps_successor * S ((S (S fs_i_dst_column_equal_rowsrowrow_sumsumnegative_body_steps)) * fs_v_dst_column_equal_rowsrowrow_sumsumnegative) + (fs_s_dst_column_equal_rowsrowrow_sumsumnegative_body_steps))) /\ fs_s_dst_column_equal_rowsrowrow_sumsumnegative_body_steps = fs_r_dst_column_equal_rowsrowrow_sumsumnegative_body_steps + fs_a_dst_column_equal_rowsrowrow_sumsumnegative_body_steps)))))) /\ (exists ge_balance_positive_column_equal_rowsrowrow_sumsumresult ge_balance_negative_column_equal_rowsrowrow_sumsumresult. (((((srt_value_column_equal_rows) = 2 * (ge_balance_positive_column_equal_rowsrowrow_sumsumresult) /\ (ge_balance_negative_column_equal_rowsrowrow_sumsumresult) = 0) \/ exists ge_signed_half_column_equal_rowsrowrow_sumsumresultdecode. (((srt_value_column_equal_rows) = 2 * ge_signed_half_column_equal_rowsrowrow_sumsumresultdecode + 1 /\ (ge_balance_positive_column_equal_rowsrowrow_sumsumresult) = 0) /\ (ge_balance_negative_column_equal_rowsrowrow_sumsumresult) = S ge_signed_half_column_equal_rowsrowrow_sumsumresultdecode))) /\ ((dst_positive_sum_column_equal_rowsrowrow_sumsum) + ge_balance_negative_column_equal_rowsrowrow_sumsumresult = (dst_negative_sum_column_equal_rowsrowrow_sumsum) + ge_balance_positive_column_equal_rowsrowrow_sumsumresult)))))))))))))))))) -> (forall dst_index_column_equal_result dst_first_column_equal_result dst_second_column_equal_result. (exists pvs_gap_column_equal_resultbound. pvs_gap_column_equal_resultbound + S (dst_index_column_equal_result) = (M)) -> (exists dst_positive_code_column_equal_resultfirst dst_positive_scale_column_equal_resultfirst dst_negative_code_column_equal_resultfirst dst_negative_scale_column_equal_resultfirst dst_positive_column_equal_resultfirst dst_negative_column_equal_resultfirst. (((B) = (((((dst_positive_code_column_equal_resultfirst) + (dst_positive_scale_column_equal_resultfirst)) * S ((dst_positive_code_column_equal_resultfirst) + (dst_positive_scale_column_equal_resultfirst)) + ((dst_positive_scale_column_equal_resultfirst) + (dst_positive_scale_column_equal_resultfirst))) + (((dst_negative_code_column_equal_resultfirst) + (dst_negative_scale_column_equal_resultfirst)) * S ((dst_negative_code_column_equal_resultfirst) + (dst_negative_scale_column_equal_resultfirst)) + ((dst_negative_scale_column_equal_resultfirst) + (dst_negative_scale_column_equal_resultfirst)))) * S ((((dst_positive_code_column_equal_resultfirst) + (dst_positive_scale_column_equal_resultfirst)) * S ((dst_positive_code_column_equal_resultfirst) + (dst_positive_scale_column_equal_resultfirst)) + ((dst_positive_scale_column_equal_resultfirst) + (dst_positive_scale_column_equal_resultfirst))) + (((dst_negative_code_column_equal_resultfirst) + (dst_negative_scale_column_equal_resultfirst)) * S ((dst_negative_code_column_equal_resultfirst) + (dst_negative_scale_column_equal_resultfirst)) + ((dst_negative_scale_column_equal_resultfirst) + (dst_negative_scale_column_equal_resultfirst)))) + ((((dst_negative_code_column_equal_resultfirst) + (dst_negative_scale_column_equal_resultfirst)) * S ((dst_negative_code_column_equal_resultfirst) + (dst_negative_scale_column_equal_resultfirst)) + ((dst_negative_scale_column_equal_resultfirst) + (dst_negative_scale_column_equal_resultfirst))) + (((dst_negative_code_column_equal_resultfirst) + (dst_negative_scale_column_equal_resultfirst)) * S ((dst_negative_code_column_equal_resultfirst) + (dst_negative_scale_column_equal_resultfirst)) + ((dst_negative_scale_column_equal_resultfirst) + (dst_negative_scale_column_equal_resultfirst)))))) /\ (((((exists ff_h_pvs_column_equal_resultfirstpositive. ff_h_pvs_column_equal_resultfirstpositive + S (dst_positive_column_equal_resultfirst) = S ((S (dst_index_column_equal_result)) * dst_positive_scale_column_equal_resultfirst)) /\ exists ff_q_pvs_column_equal_resultfirstpositive. dst_positive_code_column_equal_resultfirst = ff_q_pvs_column_equal_resultfirstpositive * S ((S (dst_index_column_equal_result)) * dst_positive_scale_column_equal_resultfirst) + (dst_positive_column_equal_resultfirst))) /\ (((((exists ff_h_pvs_column_equal_resultfirstnegative. ff_h_pvs_column_equal_resultfirstnegative + S (dst_negative_column_equal_resultfirst) = S ((S (dst_index_column_equal_result)) * dst_negative_scale_column_equal_resultfirst)) /\ exists ff_q_pvs_column_equal_resultfirstnegative. dst_negative_code_column_equal_resultfirst = ff_q_pvs_column_equal_resultfirstnegative * S ((S (dst_index_column_equal_result)) * dst_negative_scale_column_equal_resultfirst) + (dst_negative_column_equal_resultfirst))) /\ (exists ge_balance_positive_column_equal_resultfirstvalue ge_balance_negative_column_equal_resultfirstvalue. (((((dst_first_column_equal_result) = 2 * (ge_balance_positive_column_equal_resultfirstvalue) /\ (ge_balance_negative_column_equal_resultfirstvalue) = 0) \/ exists ge_signed_half_column_equal_resultfirstvaluedecode. (((dst_first_column_equal_result) = 2 * ge_signed_half_column_equal_resultfirstvaluedecode + 1 /\ (ge_balance_positive_column_equal_resultfirstvalue) = 0) /\ (ge_balance_negative_column_equal_resultfirstvalue) = S ge_signed_half_column_equal_resultfirstvaluedecode))) /\ ((dst_positive_column_equal_resultfirst) + ge_balance_negative_column_equal_resultfirstvalue = (dst_negative_column_equal_resultfirst) + ge_balance_positive_column_equal_resultfirstvalue))))))))) -> (exists dst_positive_code_column_equal_resultsecond dst_positive_scale_column_equal_resultsecond dst_negative_code_column_equal_resultsecond dst_negative_scale_column_equal_resultsecond dst_positive_column_equal_resultsecond dst_negative_column_equal_resultsecond. (((C) = (((((dst_positive_code_column_equal_resultsecond) + (dst_positive_scale_column_equal_resultsecond)) * S ((dst_positive_code_column_equal_resultsecond) + (dst_positive_scale_column_equal_resultsecond)) + ((dst_positive_scale_column_equal_resultsecond) + (dst_positive_scale_column_equal_resultsecond))) + (((dst_negative_code_column_equal_resultsecond) + (dst_negative_scale_column_equal_resultsecond)) * S ((dst_negative_code_column_equal_resultsecond) + (dst_negative_scale_column_equal_resultsecond)) + ((dst_negative_scale_column_equal_resultsecond) + (dst_negative_scale_column_equal_resultsecond)))) * S ((((dst_positive_code_column_equal_resultsecond) + (dst_positive_scale_column_equal_resultsecond)) * S ((dst_positive_code_column_equal_resultsecond) + (dst_positive_scale_column_equal_resultsecond)) + ((dst_positive_scale_column_equal_resultsecond) + (dst_positive_scale_column_equal_resultsecond))) + (((dst_negative_code_column_equal_resultsecond) + (dst_negative_scale_column_equal_resultsecond)) * S ((dst_negative_code_column_equal_resultsecond) + (dst_negative_scale_column_equal_resultsecond)) + ((dst_negative_scale_column_equal_resultsecond) + (dst_negative_scale_column_equal_resultsecond)))) + ((((dst_negative_code_column_equal_resultsecond) + (dst_negative_scale_column_equal_resultsecond)) * S ((dst_negative_code_column_equal_resultsecond) + (dst_negative_scale_column_equal_resultsecond)) + ((dst_negative_scale_column_equal_resultsecond) + (dst_negative_scale_column_equal_resultsecond))) + (((dst_negative_code_column_equal_resultsecond) + (dst_negative_scale_column_equal_resultsecond)) * S ((dst_negative_code_column_equal_resultsecond) + (dst_negative_scale_column_equal_resultsecond)) + ((dst_negative_scale_column_equal_resultsecond) + (dst_negative_scale_column_equal_resultsecond)))))) /\ (((((exists ff_h_pvs_column_equal_resultsecondpositive. ff_h_pvs_column_equal_resultsecondpositive + S (dst_positive_column_equal_resultsecond) = S ((S (dst_index_column_equal_result)) * dst_positive_scale_column_equal_resultsecond)) /\ exists ff_q_pvs_column_equal_resultsecondpositive. dst_positive_code_column_equal_resultsecond = ff_q_pvs_column_equal_resultsecondpositive * S ((S (dst_index_column_equal_result)) * dst_positive_scale_column_equal_resultsecond) + (dst_positive_column_equal_resultsecond))) /\ (((((exists ff_h_pvs_column_equal_resultsecondnegative. ff_h_pvs_column_equal_resultsecondnegative + S (dst_negative_column_equal_resultsecond) = S ((S (dst_index_column_equal_result)) * dst_negative_scale_column_equal_resultsecond)) /\ exists ff_q_pvs_column_equal_resultsecondnegative. dst_negative_code_column_equal_resultsecond = ff_q_pvs_column_equal_resultsecondnegative * S ((S (dst_index_column_equal_result)) * dst_negative_scale_column_equal_resultsecond) + (dst_negative_column_equal_resultsecond))) /\ (exists ge_balance_positive_column_equal_resultsecondvalue ge_balance_negative_column_equal_resultsecondvalue. (((((dst_second_column_equal_result) = 2 * (ge_balance_positive_column_equal_resultsecondvalue) /\ (ge_balance_negative_column_equal_resultsecondvalue) = 0) \/ exists ge_signed_half_column_equal_resultsecondvaluedecode. (((dst_second_column_equal_result) = 2 * ge_signed_half_column_equal_resultsecondvaluedecode + 1 /\ (ge_balance_positive_column_equal_resultsecondvalue) = 0) /\ (ge_balance_negative_column_equal_resultsecondvalue) = S ge_signed_half_column_equal_resultsecondvaluedecode))) /\ ((dst_positive_column_equal_resultsecond) + ge_balance_negative_column_equal_resultsecondvalue = (dst_negative_column_equal_resultsecond) + ge_balance_positive_column_equal_resultsecondvalue))))))))) -> dst_first_column_equal_result = dst_second_column_equal_result)