signed_weighted_sum_exists_unique

Exact expanded first-order arithmetic statement

forall l W F. (exists dst_positive_code_weighted_total_weights dst_positive_scale_weighted_total_weights dst_negative_code_weighted_total_weights dst_negative_scale_weighted_total_weights. (((W) = (((((dst_positive_code_weighted_total_weights) + (dst_positive_scale_weighted_total_weights)) * S ((dst_positive_code_weighted_total_weights) + (dst_positive_scale_weighted_total_weights)) + ((dst_positive_scale_weighted_total_weights) + (dst_positive_scale_weighted_total_weights))) + (((dst_negative_code_weighted_total_weights) + (dst_negative_scale_weighted_total_weights)) * S ((dst_negative_code_weighted_total_weights) + (dst_negative_scale_weighted_total_weights)) + ((dst_negative_scale_weighted_total_weights) + (dst_negative_scale_weighted_total_weights)))) * S ((((dst_positive_code_weighted_total_weights) + (dst_positive_scale_weighted_total_weights)) * S ((dst_positive_code_weighted_total_weights) + (dst_positive_scale_weighted_total_weights)) + ((dst_positive_scale_weighted_total_weights) + (dst_positive_scale_weighted_total_weights))) + (((dst_negative_code_weighted_total_weights) + (dst_negative_scale_weighted_total_weights)) * S ((dst_negative_code_weighted_total_weights) + (dst_negative_scale_weighted_total_weights)) + ((dst_negative_scale_weighted_total_weights) + (dst_negative_scale_weighted_total_weights)))) + ((((dst_negative_code_weighted_total_weights) + (dst_negative_scale_weighted_total_weights)) * S ((dst_negative_code_weighted_total_weights) + (dst_negative_scale_weighted_total_weights)) + ((dst_negative_scale_weighted_total_weights) + (dst_negative_scale_weighted_total_weights))) + (((dst_negative_code_weighted_total_weights) + (dst_negative_scale_weighted_total_weights)) * S ((dst_negative_code_weighted_total_weights) + (dst_negative_scale_weighted_total_weights)) + ((dst_negative_scale_weighted_total_weights) + (dst_negative_scale_weighted_total_weights)))))) /\ (forall dst_index_weighted_total_weights. (exists pvs_le_gap_weighted_total_weightsdomain. pvs_le_gap_weighted_total_weightsdomain + (dst_index_weighted_total_weights) = (l)) -> exists dst_positive_weighted_total_weights dst_negative_weighted_total_weights dst_value_weighted_total_weights. ((((exists ff_h_pvs_weighted_total_weightsentrypositive. ff_h_pvs_weighted_total_weightsentrypositive + S (dst_positive_weighted_total_weights) = S ((S (dst_index_weighted_total_weights)) * dst_positive_scale_weighted_total_weights)) /\ exists ff_q_pvs_weighted_total_weightsentrypositive. dst_positive_code_weighted_total_weights = ff_q_pvs_weighted_total_weightsentrypositive * S ((S (dst_index_weighted_total_weights)) * dst_positive_scale_weighted_total_weights) + (dst_positive_weighted_total_weights))) /\ (((((exists ff_h_pvs_weighted_total_weightsentrynegative. ff_h_pvs_weighted_total_weightsentrynegative + S (dst_negative_weighted_total_weights) = S ((S (dst_index_weighted_total_weights)) * dst_negative_scale_weighted_total_weights)) /\ exists ff_q_pvs_weighted_total_weightsentrynegative. dst_negative_code_weighted_total_weights = ff_q_pvs_weighted_total_weightsentrynegative * S ((S (dst_index_weighted_total_weights)) * dst_negative_scale_weighted_total_weights) + (dst_negative_weighted_total_weights))) /\ (exists ge_balance_positive_weighted_total_weightsentryvalue ge_balance_negative_weighted_total_weightsentryvalue. (((((dst_value_weighted_total_weights) = 2 * (ge_balance_positive_weighted_total_weightsentryvalue) /\ (ge_balance_negative_weighted_total_weightsentryvalue) = 0) \/ exists ge_signed_half_weighted_total_weightsentryvaluedecode. (((dst_value_weighted_total_weights) = 2 * ge_signed_half_weighted_total_weightsentryvaluedecode + 1 /\ (ge_balance_positive_weighted_total_weightsentryvalue) = 0) /\ (ge_balance_negative_weighted_total_weightsentryvalue) = S ge_signed_half_weighted_total_weightsentryvaluedecode))) /\ ((dst_positive_weighted_total_weights) + ge_balance_negative_weighted_total_weightsentryvalue = (dst_negative_weighted_total_weights) + ge_balance_positive_weighted_total_weightsentryvalue))))))))) -> (exists dst_positive_code_weighted_total_values dst_positive_scale_weighted_total_values dst_negative_code_weighted_total_values dst_negative_scale_weighted_total_values. (((F) = (((((dst_positive_code_weighted_total_values) + (dst_positive_scale_weighted_total_values)) * S ((dst_positive_code_weighted_total_values) + (dst_positive_scale_weighted_total_values)) + ((dst_positive_scale_weighted_total_values) + (dst_positive_scale_weighted_total_values))) + (((dst_negative_code_weighted_total_values) + (dst_negative_scale_weighted_total_values)) * S ((dst_negative_code_weighted_total_values) + (dst_negative_scale_weighted_total_values)) + ((dst_negative_scale_weighted_total_values) + (dst_negative_scale_weighted_total_values)))) * S ((((dst_positive_code_weighted_total_values) + (dst_positive_scale_weighted_total_values)) * S ((dst_positive_code_weighted_total_values) + (dst_positive_scale_weighted_total_values)) + ((dst_positive_scale_weighted_total_values) + (dst_positive_scale_weighted_total_values))) + (((dst_negative_code_weighted_total_values) + (dst_negative_scale_weighted_total_values)) * S ((dst_negative_code_weighted_total_values) + (dst_negative_scale_weighted_total_values)) + ((dst_negative_scale_weighted_total_values) + (dst_negative_scale_weighted_total_values)))) + ((((dst_negative_code_weighted_total_values) + (dst_negative_scale_weighted_total_values)) * S ((dst_negative_code_weighted_total_values) + (dst_negative_scale_weighted_total_values)) + ((dst_negative_scale_weighted_total_values) + (dst_negative_scale_weighted_total_values))) + (((dst_negative_code_weighted_total_values) + (dst_negative_scale_weighted_total_values)) * S ((dst_negative_code_weighted_total_values) + (dst_negative_scale_weighted_total_values)) + ((dst_negative_scale_weighted_total_values) + (dst_negative_scale_weighted_total_values)))))) /\ (forall dst_index_weighted_total_values. (exists pvs_le_gap_weighted_total_valuesdomain. pvs_le_gap_weighted_total_valuesdomain + (dst_index_weighted_total_values) = (l)) -> exists dst_positive_weighted_total_values dst_negative_weighted_total_values dst_value_weighted_total_values. ((((exists ff_h_pvs_weighted_total_valuesentrypositive. ff_h_pvs_weighted_total_valuesentrypositive + S (dst_positive_weighted_total_values) = S ((S (dst_index_weighted_total_values)) * dst_positive_scale_weighted_total_values)) /\ exists ff_q_pvs_weighted_total_valuesentrypositive. dst_positive_code_weighted_total_values = ff_q_pvs_weighted_total_valuesentrypositive * S ((S (dst_index_weighted_total_values)) * dst_positive_scale_weighted_total_values) + (dst_positive_weighted_total_values))) /\ (((((exists ff_h_pvs_weighted_total_valuesentrynegative. ff_h_pvs_weighted_total_valuesentrynegative + S (dst_negative_weighted_total_values) = S ((S (dst_index_weighted_total_values)) * dst_negative_scale_weighted_total_values)) /\ exists ff_q_pvs_weighted_total_valuesentrynegative. dst_negative_code_weighted_total_values = ff_q_pvs_weighted_total_valuesentrynegative * S ((S (dst_index_weighted_total_values)) * dst_negative_scale_weighted_total_values) + (dst_negative_weighted_total_values))) /\ (exists ge_balance_positive_weighted_total_valuesentryvalue ge_balance_negative_weighted_total_valuesentryvalue. (((((dst_value_weighted_total_values) = 2 * (ge_balance_positive_weighted_total_valuesentryvalue) /\ (ge_balance_negative_weighted_total_valuesentryvalue) = 0) \/ exists ge_signed_half_weighted_total_valuesentryvaluedecode. (((dst_value_weighted_total_values) = 2 * ge_signed_half_weighted_total_valuesentryvaluedecode + 1 /\ (ge_balance_positive_weighted_total_valuesentryvalue) = 0) /\ (ge_balance_negative_weighted_total_valuesentryvalue) = S ge_signed_half_weighted_total_valuesentryvaluedecode))) /\ ((dst_positive_weighted_total_values) + ge_balance_negative_weighted_total_valuesentryvalue = (dst_negative_weighted_total_values) + ge_balance_positive_weighted_total_valuesentryvalue))))))))) -> exists z. ((exists sws_product_table_weighted_total_result. ((((exists dst_positive_code_weighted_total_resultproductsleft_table dst_positive_scale_weighted_total_resultproductsleft_table dst_negative_code_weighted_total_resultproductsleft_table dst_negative_scale_weighted_total_resultproductsleft_table. (((W) = (((((dst_positive_code_weighted_total_resultproductsleft_table) + (dst_positive_scale_weighted_total_resultproductsleft_table)) * S ((dst_positive_code_weighted_total_resultproductsleft_table) + (dst_positive_scale_weighted_total_resultproductsleft_table)) + ((dst_positive_scale_weighted_total_resultproductsleft_table) + (dst_positive_scale_weighted_total_resultproductsleft_table))) + (((dst_negative_code_weighted_total_resultproductsleft_table) + (dst_negative_scale_weighted_total_resultproductsleft_table)) * S ((dst_negative_code_weighted_total_resultproductsleft_table) + (dst_negative_scale_weighted_total_resultproductsleft_table)) + ((dst_negative_scale_weighted_total_resultproductsleft_table) + (dst_negative_scale_weighted_total_resultproductsleft_table)))) * S ((((dst_positive_code_weighted_total_resultproductsleft_table) + (dst_positive_scale_weighted_total_resultproductsleft_table)) * S ((dst_positive_code_weighted_total_resultproductsleft_table) + (dst_positive_scale_weighted_total_resultproductsleft_table)) + ((dst_positive_scale_weighted_total_resultproductsleft_table) + (dst_positive_scale_weighted_total_resultproductsleft_table))) + (((dst_negative_code_weighted_total_resultproductsleft_table) + (dst_negative_scale_weighted_total_resultproductsleft_table)) * S ((dst_negative_code_weighted_total_resultproductsleft_table) + (dst_negative_scale_weighted_total_resultproductsleft_table)) + ((dst_negative_scale_weighted_total_resultproductsleft_table) + (dst_negative_scale_weighted_total_resultproductsleft_table)))) + ((((dst_negative_code_weighted_total_resultproductsleft_table) + (dst_negative_scale_weighted_total_resultproductsleft_table)) * S ((dst_negative_code_weighted_total_resultproductsleft_table) + (dst_negative_scale_weighted_total_resultproductsleft_table)) + ((dst_negative_scale_weighted_total_resultproductsleft_table) + (dst_negative_scale_weighted_total_resultproductsleft_table))) + (((dst_negative_code_weighted_total_resultproductsleft_table) + (dst_negative_scale_weighted_total_resultproductsleft_table)) * S ((dst_negative_code_weighted_total_resultproductsleft_table) + (dst_negative_scale_weighted_total_resultproductsleft_table)) + ((dst_negative_scale_weighted_total_resultproductsleft_table) + (dst_negative_scale_weighted_total_resultproductsleft_table)))))) /\ (forall dst_index_weighted_total_resultproductsleft_table. (exists pvs_le_gap_weighted_total_resultproductsleft_tabledomain. pvs_le_gap_weighted_total_resultproductsleft_tabledomain + (dst_index_weighted_total_resultproductsleft_table) = (l)) -> exists dst_positive_weighted_total_resultproductsleft_table dst_negative_weighted_total_resultproductsleft_table dst_value_weighted_total_resultproductsleft_table. ((((exists ff_h_pvs_weighted_total_resultproductsleft_tableentrypositive. ff_h_pvs_weighted_total_resultproductsleft_tableentrypositive + S (dst_positive_weighted_total_resultproductsleft_table) = S ((S (dst_index_weighted_total_resultproductsleft_table)) * dst_positive_scale_weighted_total_resultproductsleft_table)) /\ exists ff_q_pvs_weighted_total_resultproductsleft_tableentrypositive. dst_positive_code_weighted_total_resultproductsleft_table = ff_q_pvs_weighted_total_resultproductsleft_tableentrypositive * S ((S (dst_index_weighted_total_resultproductsleft_table)) * dst_positive_scale_weighted_total_resultproductsleft_table) + (dst_positive_weighted_total_resultproductsleft_table))) /\ (((((exists ff_h_pvs_weighted_total_resultproductsleft_tableentrynegative. ff_h_pvs_weighted_total_resultproductsleft_tableentrynegative + S (dst_negative_weighted_total_resultproductsleft_table) = S ((S (dst_index_weighted_total_resultproductsleft_table)) * dst_negative_scale_weighted_total_resultproductsleft_table)) /\ exists ff_q_pvs_weighted_total_resultproductsleft_tableentrynegative. dst_negative_code_weighted_total_resultproductsleft_table = ff_q_pvs_weighted_total_resultproductsleft_tableentrynegative * S ((S (dst_index_weighted_total_resultproductsleft_table)) * dst_negative_scale_weighted_total_resultproductsleft_table) + (dst_negative_weighted_total_resultproductsleft_table))) /\ (exists ge_balance_positive_weighted_total_resultproductsleft_tableentryvalue ge_balance_negative_weighted_total_resultproductsleft_tableentryvalue. (((((dst_value_weighted_total_resultproductsleft_table) = 2 * (ge_balance_positive_weighted_total_resultproductsleft_tableentryvalue) /\ (ge_balance_negative_weighted_total_resultproductsleft_tableentryvalue) = 0) \/ exists ge_signed_half_weighted_total_resultproductsleft_tableentryvaluedecode. (((dst_value_weighted_total_resultproductsleft_table) = 2 * ge_signed_half_weighted_total_resultproductsleft_tableentryvaluedecode + 1 /\ (ge_balance_positive_weighted_total_resultproductsleft_tableentryvalue) = 0) /\ (ge_balance_negative_weighted_total_resultproductsleft_tableentryvalue) = S ge_signed_half_weighted_total_resultproductsleft_tableentryvaluedecode))) /\ ((dst_positive_weighted_total_resultproductsleft_table) + ge_balance_negative_weighted_total_resultproductsleft_tableentryvalue = (dst_negative_weighted_total_resultproductsleft_table) + ge_balance_positive_weighted_total_resultproductsleft_tableentryvalue))))))))) /\ (((exists dst_positive_code_weighted_total_resultproductsright_table dst_positive_scale_weighted_total_resultproductsright_table dst_negative_code_weighted_total_resultproductsright_table dst_negative_scale_weighted_total_resultproductsright_table. (((F) = (((((dst_positive_code_weighted_total_resultproductsright_table) + (dst_positive_scale_weighted_total_resultproductsright_table)) * S ((dst_positive_code_weighted_total_resultproductsright_table) + (dst_positive_scale_weighted_total_resultproductsright_table)) + ((dst_positive_scale_weighted_total_resultproductsright_table) + (dst_positive_scale_weighted_total_resultproductsright_table))) + (((dst_negative_code_weighted_total_resultproductsright_table) + (dst_negative_scale_weighted_total_resultproductsright_table)) * S ((dst_negative_code_weighted_total_resultproductsright_table) + (dst_negative_scale_weighted_total_resultproductsright_table)) + ((dst_negative_scale_weighted_total_resultproductsright_table) + (dst_negative_scale_weighted_total_resultproductsright_table)))) * S ((((dst_positive_code_weighted_total_resultproductsright_table) + (dst_positive_scale_weighted_total_resultproductsright_table)) * S ((dst_positive_code_weighted_total_resultproductsright_table) + (dst_positive_scale_weighted_total_resultproductsright_table)) + ((dst_positive_scale_weighted_total_resultproductsright_table) + (dst_positive_scale_weighted_total_resultproductsright_table))) + (((dst_negative_code_weighted_total_resultproductsright_table) + (dst_negative_scale_weighted_total_resultproductsright_table)) * S ((dst_negative_code_weighted_total_resultproductsright_table) + (dst_negative_scale_weighted_total_resultproductsright_table)) + ((dst_negative_scale_weighted_total_resultproductsright_table) + (dst_negative_scale_weighted_total_resultproductsright_table)))) + ((((dst_negative_code_weighted_total_resultproductsright_table) + (dst_negative_scale_weighted_total_resultproductsright_table)) * S ((dst_negative_code_weighted_total_resultproductsright_table) + (dst_negative_scale_weighted_total_resultproductsright_table)) + ((dst_negative_scale_weighted_total_resultproductsright_table) + (dst_negative_scale_weighted_total_resultproductsright_table))) + (((dst_negative_code_weighted_total_resultproductsright_table) + (dst_negative_scale_weighted_total_resultproductsright_table)) * S ((dst_negative_code_weighted_total_resultproductsright_table) + (dst_negative_scale_weighted_total_resultproductsright_table)) + ((dst_negative_scale_weighted_total_resultproductsright_table) + (dst_negative_scale_weighted_total_resultproductsright_table)))))) /\ (forall dst_index_weighted_total_resultproductsright_table. (exists pvs_le_gap_weighted_total_resultproductsright_tabledomain. pvs_le_gap_weighted_total_resultproductsright_tabledomain + (dst_index_weighted_total_resultproductsright_table) = (l)) -> exists dst_positive_weighted_total_resultproductsright_table dst_negative_weighted_total_resultproductsright_table dst_value_weighted_total_resultproductsright_table. ((((exists ff_h_pvs_weighted_total_resultproductsright_tableentrypositive. ff_h_pvs_weighted_total_resultproductsright_tableentrypositive + S (dst_positive_weighted_total_resultproductsright_table) = S ((S (dst_index_weighted_total_resultproductsright_table)) * dst_positive_scale_weighted_total_resultproductsright_table)) /\ exists ff_q_pvs_weighted_total_resultproductsright_tableentrypositive. dst_positive_code_weighted_total_resultproductsright_table = ff_q_pvs_weighted_total_resultproductsright_tableentrypositive * S ((S (dst_index_weighted_total_resultproductsright_table)) * dst_positive_scale_weighted_total_resultproductsright_table) + (dst_positive_weighted_total_resultproductsright_table))) /\ (((((exists ff_h_pvs_weighted_total_resultproductsright_tableentrynegative. ff_h_pvs_weighted_total_resultproductsright_tableentrynegative + S (dst_negative_weighted_total_resultproductsright_table) = S ((S (dst_index_weighted_total_resultproductsright_table)) * dst_negative_scale_weighted_total_resultproductsright_table)) /\ exists ff_q_pvs_weighted_total_resultproductsright_tableentrynegative. dst_negative_code_weighted_total_resultproductsright_table = ff_q_pvs_weighted_total_resultproductsright_tableentrynegative * S ((S (dst_index_weighted_total_resultproductsright_table)) * dst_negative_scale_weighted_total_resultproductsright_table) + (dst_negative_weighted_total_resultproductsright_table))) /\ (exists ge_balance_positive_weighted_total_resultproductsright_tableentryvalue ge_balance_negative_weighted_total_resultproductsright_tableentryvalue. (((((dst_value_weighted_total_resultproductsright_table) = 2 * (ge_balance_positive_weighted_total_resultproductsright_tableentryvalue) /\ (ge_balance_negative_weighted_total_resultproductsright_tableentryvalue) = 0) \/ exists ge_signed_half_weighted_total_resultproductsright_tableentryvaluedecode. (((dst_value_weighted_total_resultproductsright_table) = 2 * ge_signed_half_weighted_total_resultproductsright_tableentryvaluedecode + 1 /\ (ge_balance_positive_weighted_total_resultproductsright_tableentryvalue) = 0) /\ (ge_balance_negative_weighted_total_resultproductsright_tableentryvalue) = S ge_signed_half_weighted_total_resultproductsright_tableentryvaluedecode))) /\ ((dst_positive_weighted_total_resultproductsright_table) + ge_balance_negative_weighted_total_resultproductsright_tableentryvalue = (dst_negative_weighted_total_resultproductsright_table) + ge_balance_positive_weighted_total_resultproductsright_tableentryvalue))))))))) /\ (((exists dst_positive_code_weighted_total_resultproductsoutput_table dst_positive_scale_weighted_total_resultproductsoutput_table dst_negative_code_weighted_total_resultproductsoutput_table dst_negative_scale_weighted_total_resultproductsoutput_table. (((sws_product_table_weighted_total_result) = (((((dst_positive_code_weighted_total_resultproductsoutput_table) + (dst_positive_scale_weighted_total_resultproductsoutput_table)) * S ((dst_positive_code_weighted_total_resultproductsoutput_table) + (dst_positive_scale_weighted_total_resultproductsoutput_table)) + ((dst_positive_scale_weighted_total_resultproductsoutput_table) + (dst_positive_scale_weighted_total_resultproductsoutput_table))) + (((dst_negative_code_weighted_total_resultproductsoutput_table) + (dst_negative_scale_weighted_total_resultproductsoutput_table)) * S ((dst_negative_code_weighted_total_resultproductsoutput_table) + (dst_negative_scale_weighted_total_resultproductsoutput_table)) + ((dst_negative_scale_weighted_total_resultproductsoutput_table) + (dst_negative_scale_weighted_total_resultproductsoutput_table)))) * S ((((dst_positive_code_weighted_total_resultproductsoutput_table) + (dst_positive_scale_weighted_total_resultproductsoutput_table)) * S ((dst_positive_code_weighted_total_resultproductsoutput_table) + (dst_positive_scale_weighted_total_resultproductsoutput_table)) + ((dst_positive_scale_weighted_total_resultproductsoutput_table) + (dst_positive_scale_weighted_total_resultproductsoutput_table))) + (((dst_negative_code_weighted_total_resultproductsoutput_table) + (dst_negative_scale_weighted_total_resultproductsoutput_table)) * S ((dst_negative_code_weighted_total_resultproductsoutput_table) + (dst_negative_scale_weighted_total_resultproductsoutput_table)) + ((dst_negative_scale_weighted_total_resultproductsoutput_table) + (dst_negative_scale_weighted_total_resultproductsoutput_table)))) + ((((dst_negative_code_weighted_total_resultproductsoutput_table) + (dst_negative_scale_weighted_total_resultproductsoutput_table)) * S ((dst_negative_code_weighted_total_resultproductsoutput_table) + (dst_negative_scale_weighted_total_resultproductsoutput_table)) + ((dst_negative_scale_weighted_total_resultproductsoutput_table) + (dst_negative_scale_weighted_total_resultproductsoutput_table))) + (((dst_negative_code_weighted_total_resultproductsoutput_table) + (dst_negative_scale_weighted_total_resultproductsoutput_table)) * S ((dst_negative_code_weighted_total_resultproductsoutput_table) + (dst_negative_scale_weighted_total_resultproductsoutput_table)) + ((dst_negative_scale_weighted_total_resultproductsoutput_table) + (dst_negative_scale_weighted_total_resultproductsoutput_table)))))) /\ (forall dst_index_weighted_total_resultproductsoutput_table. (exists pvs_le_gap_weighted_total_resultproductsoutput_tabledomain. pvs_le_gap_weighted_total_resultproductsoutput_tabledomain + (dst_index_weighted_total_resultproductsoutput_table) = (l)) -> exists dst_positive_weighted_total_resultproductsoutput_table dst_negative_weighted_total_resultproductsoutput_table dst_value_weighted_total_resultproductsoutput_table. ((((exists ff_h_pvs_weighted_total_resultproductsoutput_tableentrypositive. ff_h_pvs_weighted_total_resultproductsoutput_tableentrypositive + S (dst_positive_weighted_total_resultproductsoutput_table) = S ((S (dst_index_weighted_total_resultproductsoutput_table)) * dst_positive_scale_weighted_total_resultproductsoutput_table)) /\ exists ff_q_pvs_weighted_total_resultproductsoutput_tableentrypositive. dst_positive_code_weighted_total_resultproductsoutput_table = ff_q_pvs_weighted_total_resultproductsoutput_tableentrypositive * S ((S (dst_index_weighted_total_resultproductsoutput_table)) * dst_positive_scale_weighted_total_resultproductsoutput_table) + (dst_positive_weighted_total_resultproductsoutput_table))) /\ (((((exists ff_h_pvs_weighted_total_resultproductsoutput_tableentrynegative. ff_h_pvs_weighted_total_resultproductsoutput_tableentrynegative + S (dst_negative_weighted_total_resultproductsoutput_table) = S ((S (dst_index_weighted_total_resultproductsoutput_table)) * dst_negative_scale_weighted_total_resultproductsoutput_table)) /\ exists ff_q_pvs_weighted_total_resultproductsoutput_tableentrynegative. dst_negative_code_weighted_total_resultproductsoutput_table = ff_q_pvs_weighted_total_resultproductsoutput_tableentrynegative * S ((S (dst_index_weighted_total_resultproductsoutput_table)) * dst_negative_scale_weighted_total_resultproductsoutput_table) + (dst_negative_weighted_total_resultproductsoutput_table))) /\ (exists ge_balance_positive_weighted_total_resultproductsoutput_tableentryvalue ge_balance_negative_weighted_total_resultproductsoutput_tableentryvalue. (((((dst_value_weighted_total_resultproductsoutput_table) = 2 * (ge_balance_positive_weighted_total_resultproductsoutput_tableentryvalue) /\ (ge_balance_negative_weighted_total_resultproductsoutput_tableentryvalue) = 0) \/ exists ge_signed_half_weighted_total_resultproductsoutput_tableentryvaluedecode. (((dst_value_weighted_total_resultproductsoutput_table) = 2 * ge_signed_half_weighted_total_resultproductsoutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_weighted_total_resultproductsoutput_tableentryvalue) = 0) /\ (ge_balance_negative_weighted_total_resultproductsoutput_tableentryvalue) = S ge_signed_half_weighted_total_resultproductsoutput_tableentryvaluedecode))) /\ ((dst_positive_weighted_total_resultproductsoutput_table) + ge_balance_negative_weighted_total_resultproductsoutput_tableentryvalue = (dst_negative_weighted_total_resultproductsoutput_table) + ge_balance_positive_weighted_total_resultproductsoutput_tableentryvalue))))))))) /\ (forall sto_index_weighted_total_resultproductsentries. (exists pvs_gap_weighted_total_resultproductsentriesbound. pvs_gap_weighted_total_resultproductsentriesbound + S (sto_index_weighted_total_resultproductsentries) = (l)) -> exists sto_left_weighted_total_resultproductsentries sto_right_weighted_total_resultproductsentries sto_output_weighted_total_resultproductsentries. ((exists dst_positive_code_weighted_total_resultproductsentriesentryleft dst_positive_scale_weighted_total_resultproductsentriesentryleft dst_negative_code_weighted_total_resultproductsentriesentryleft dst_negative_scale_weighted_total_resultproductsentriesentryleft dst_positive_weighted_total_resultproductsentriesentryleft dst_negative_weighted_total_resultproductsentriesentryleft. (((W) = (((((dst_positive_code_weighted_total_resultproductsentriesentryleft) + (dst_positive_scale_weighted_total_resultproductsentriesentryleft)) * S ((dst_positive_code_weighted_total_resultproductsentriesentryleft) + (dst_positive_scale_weighted_total_resultproductsentriesentryleft)) + ((dst_positive_scale_weighted_total_resultproductsentriesentryleft) + (dst_positive_scale_weighted_total_resultproductsentriesentryleft))) + (((dst_negative_code_weighted_total_resultproductsentriesentryleft) + (dst_negative_scale_weighted_total_resultproductsentriesentryleft)) * S ((dst_negative_code_weighted_total_resultproductsentriesentryleft) + (dst_negative_scale_weighted_total_resultproductsentriesentryleft)) + ((dst_negative_scale_weighted_total_resultproductsentriesentryleft) + (dst_negative_scale_weighted_total_resultproductsentriesentryleft)))) * S ((((dst_positive_code_weighted_total_resultproductsentriesentryleft) + (dst_positive_scale_weighted_total_resultproductsentriesentryleft)) * S ((dst_positive_code_weighted_total_resultproductsentriesentryleft) + (dst_positive_scale_weighted_total_resultproductsentriesentryleft)) + ((dst_positive_scale_weighted_total_resultproductsentriesentryleft) + (dst_positive_scale_weighted_total_resultproductsentriesentryleft))) + (((dst_negative_code_weighted_total_resultproductsentriesentryleft) + (dst_negative_scale_weighted_total_resultproductsentriesentryleft)) * S ((dst_negative_code_weighted_total_resultproductsentriesentryleft) + (dst_negative_scale_weighted_total_resultproductsentriesentryleft)) + ((dst_negative_scale_weighted_total_resultproductsentriesentryleft) + (dst_negative_scale_weighted_total_resultproductsentriesentryleft)))) + ((((dst_negative_code_weighted_total_resultproductsentriesentryleft) + (dst_negative_scale_weighted_total_resultproductsentriesentryleft)) * S ((dst_negative_code_weighted_total_resultproductsentriesentryleft) + (dst_negative_scale_weighted_total_resultproductsentriesentryleft)) + ((dst_negative_scale_weighted_total_resultproductsentriesentryleft) + (dst_negative_scale_weighted_total_resultproductsentriesentryleft))) + (((dst_negative_code_weighted_total_resultproductsentriesentryleft) + (dst_negative_scale_weighted_total_resultproductsentriesentryleft)) * S ((dst_negative_code_weighted_total_resultproductsentriesentryleft) + (dst_negative_scale_weighted_total_resultproductsentriesentryleft)) + ((dst_negative_scale_weighted_total_resultproductsentriesentryleft) + (dst_negative_scale_weighted_total_resultproductsentriesentryleft)))))) /\ (((((exists ff_h_pvs_weighted_total_resultproductsentriesentryleftpositive. ff_h_pvs_weighted_total_resultproductsentriesentryleftpositive + S (dst_positive_weighted_total_resultproductsentriesentryleft) = S ((S (sto_index_weighted_total_resultproductsentries)) * dst_positive_scale_weighted_total_resultproductsentriesentryleft)) /\ exists ff_q_pvs_weighted_total_resultproductsentriesentryleftpositive. dst_positive_code_weighted_total_resultproductsentriesentryleft = ff_q_pvs_weighted_total_resultproductsentriesentryleftpositive * S ((S (sto_index_weighted_total_resultproductsentries)) * dst_positive_scale_weighted_total_resultproductsentriesentryleft) + (dst_positive_weighted_total_resultproductsentriesentryleft))) /\ (((((exists ff_h_pvs_weighted_total_resultproductsentriesentryleftnegative. ff_h_pvs_weighted_total_resultproductsentriesentryleftnegative + S (dst_negative_weighted_total_resultproductsentriesentryleft) = S ((S (sto_index_weighted_total_resultproductsentries)) * dst_negative_scale_weighted_total_resultproductsentriesentryleft)) /\ exists ff_q_pvs_weighted_total_resultproductsentriesentryleftnegative. dst_negative_code_weighted_total_resultproductsentriesentryleft = ff_q_pvs_weighted_total_resultproductsentriesentryleftnegative * S ((S (sto_index_weighted_total_resultproductsentries)) * dst_negative_scale_weighted_total_resultproductsentriesentryleft) + (dst_negative_weighted_total_resultproductsentriesentryleft))) /\ (exists ge_balance_positive_weighted_total_resultproductsentriesentryleftvalue ge_balance_negative_weighted_total_resultproductsentriesentryleftvalue. (((((sto_left_weighted_total_resultproductsentries) = 2 * (ge_balance_positive_weighted_total_resultproductsentriesentryleftvalue) /\ (ge_balance_negative_weighted_total_resultproductsentriesentryleftvalue) = 0) \/ exists ge_signed_half_weighted_total_resultproductsentriesentryleftvaluedecode. (((sto_left_weighted_total_resultproductsentries) = 2 * ge_signed_half_weighted_total_resultproductsentriesentryleftvaluedecode + 1 /\ (ge_balance_positive_weighted_total_resultproductsentriesentryleftvalue) = 0) /\ (ge_balance_negative_weighted_total_resultproductsentriesentryleftvalue) = S ge_signed_half_weighted_total_resultproductsentriesentryleftvaluedecode))) /\ ((dst_positive_weighted_total_resultproductsentriesentryleft) + ge_balance_negative_weighted_total_resultproductsentriesentryleftvalue = (dst_negative_weighted_total_resultproductsentriesentryleft) + ge_balance_positive_weighted_total_resultproductsentriesentryleftvalue))))))))) /\ (((exists dst_positive_code_weighted_total_resultproductsentriesentryright dst_positive_scale_weighted_total_resultproductsentriesentryright dst_negative_code_weighted_total_resultproductsentriesentryright dst_negative_scale_weighted_total_resultproductsentriesentryright dst_positive_weighted_total_resultproductsentriesentryright dst_negative_weighted_total_resultproductsentriesentryright. (((F) = (((((dst_positive_code_weighted_total_resultproductsentriesentryright) + (dst_positive_scale_weighted_total_resultproductsentriesentryright)) * S ((dst_positive_code_weighted_total_resultproductsentriesentryright) + (dst_positive_scale_weighted_total_resultproductsentriesentryright)) + ((dst_positive_scale_weighted_total_resultproductsentriesentryright) + (dst_positive_scale_weighted_total_resultproductsentriesentryright))) + (((dst_negative_code_weighted_total_resultproductsentriesentryright) + (dst_negative_scale_weighted_total_resultproductsentriesentryright)) * S ((dst_negative_code_weighted_total_resultproductsentriesentryright) + (dst_negative_scale_weighted_total_resultproductsentriesentryright)) + ((dst_negative_scale_weighted_total_resultproductsentriesentryright) + (dst_negative_scale_weighted_total_resultproductsentriesentryright)))) * S ((((dst_positive_code_weighted_total_resultproductsentriesentryright) + (dst_positive_scale_weighted_total_resultproductsentriesentryright)) * S ((dst_positive_code_weighted_total_resultproductsentriesentryright) + (dst_positive_scale_weighted_total_resultproductsentriesentryright)) + ((dst_positive_scale_weighted_total_resultproductsentriesentryright) + (dst_positive_scale_weighted_total_resultproductsentriesentryright))) + (((dst_negative_code_weighted_total_resultproductsentriesentryright) + (dst_negative_scale_weighted_total_resultproductsentriesentryright)) * S ((dst_negative_code_weighted_total_resultproductsentriesentryright) + (dst_negative_scale_weighted_total_resultproductsentriesentryright)) + ((dst_negative_scale_weighted_total_resultproductsentriesentryright) + (dst_negative_scale_weighted_total_resultproductsentriesentryright)))) + ((((dst_negative_code_weighted_total_resultproductsentriesentryright) + (dst_negative_scale_weighted_total_resultproductsentriesentryright)) * S ((dst_negative_code_weighted_total_resultproductsentriesentryright) + (dst_negative_scale_weighted_total_resultproductsentriesentryright)) + ((dst_negative_scale_weighted_total_resultproductsentriesentryright) + (dst_negative_scale_weighted_total_resultproductsentriesentryright))) + (((dst_negative_code_weighted_total_resultproductsentriesentryright) + (dst_negative_scale_weighted_total_resultproductsentriesentryright)) * S ((dst_negative_code_weighted_total_resultproductsentriesentryright) + (dst_negative_scale_weighted_total_resultproductsentriesentryright)) + ((dst_negative_scale_weighted_total_resultproductsentriesentryright) + (dst_negative_scale_weighted_total_resultproductsentriesentryright)))))) /\ (((((exists ff_h_pvs_weighted_total_resultproductsentriesentryrightpositive. ff_h_pvs_weighted_total_resultproductsentriesentryrightpositive + S (dst_positive_weighted_total_resultproductsentriesentryright) = S ((S (sto_index_weighted_total_resultproductsentries)) * dst_positive_scale_weighted_total_resultproductsentriesentryright)) /\ exists ff_q_pvs_weighted_total_resultproductsentriesentryrightpositive. dst_positive_code_weighted_total_resultproductsentriesentryright = ff_q_pvs_weighted_total_resultproductsentriesentryrightpositive * S ((S (sto_index_weighted_total_resultproductsentries)) * dst_positive_scale_weighted_total_resultproductsentriesentryright) + (dst_positive_weighted_total_resultproductsentriesentryright))) /\ (((((exists ff_h_pvs_weighted_total_resultproductsentriesentryrightnegative. ff_h_pvs_weighted_total_resultproductsentriesentryrightnegative + S (dst_negative_weighted_total_resultproductsentriesentryright) = S ((S (sto_index_weighted_total_resultproductsentries)) * dst_negative_scale_weighted_total_resultproductsentriesentryright)) /\ exists ff_q_pvs_weighted_total_resultproductsentriesentryrightnegative. dst_negative_code_weighted_total_resultproductsentriesentryright = ff_q_pvs_weighted_total_resultproductsentriesentryrightnegative * S ((S (sto_index_weighted_total_resultproductsentries)) * dst_negative_scale_weighted_total_resultproductsentriesentryright) + (dst_negative_weighted_total_resultproductsentriesentryright))) /\ (exists ge_balance_positive_weighted_total_resultproductsentriesentryrightvalue ge_balance_negative_weighted_total_resultproductsentriesentryrightvalue. (((((sto_right_weighted_total_resultproductsentries) = 2 * (ge_balance_positive_weighted_total_resultproductsentriesentryrightvalue) /\ (ge_balance_negative_weighted_total_resultproductsentriesentryrightvalue) = 0) \/ exists ge_signed_half_weighted_total_resultproductsentriesentryrightvaluedecode. (((sto_right_weighted_total_resultproductsentries) = 2 * ge_signed_half_weighted_total_resultproductsentriesentryrightvaluedecode + 1 /\ (ge_balance_positive_weighted_total_resultproductsentriesentryrightvalue) = 0) /\ (ge_balance_negative_weighted_total_resultproductsentriesentryrightvalue) = S ge_signed_half_weighted_total_resultproductsentriesentryrightvaluedecode))) /\ ((dst_positive_weighted_total_resultproductsentriesentryright) + ge_balance_negative_weighted_total_resultproductsentriesentryrightvalue = (dst_negative_weighted_total_resultproductsentriesentryright) + ge_balance_positive_weighted_total_resultproductsentriesentryrightvalue))))))))) /\ (((exists dst_positive_code_weighted_total_resultproductsentriesentryoutput dst_positive_scale_weighted_total_resultproductsentriesentryoutput dst_negative_code_weighted_total_resultproductsentriesentryoutput dst_negative_scale_weighted_total_resultproductsentriesentryoutput dst_positive_weighted_total_resultproductsentriesentryoutput dst_negative_weighted_total_resultproductsentriesentryoutput. (((sws_product_table_weighted_total_result) = (((((dst_positive_code_weighted_total_resultproductsentriesentryoutput) + (dst_positive_scale_weighted_total_resultproductsentriesentryoutput)) * S ((dst_positive_code_weighted_total_resultproductsentriesentryoutput) + (dst_positive_scale_weighted_total_resultproductsentriesentryoutput)) + ((dst_positive_scale_weighted_total_resultproductsentriesentryoutput) + (dst_positive_scale_weighted_total_resultproductsentriesentryoutput))) + (((dst_negative_code_weighted_total_resultproductsentriesentryoutput) + (dst_negative_scale_weighted_total_resultproductsentriesentryoutput)) * S ((dst_negative_code_weighted_total_resultproductsentriesentryoutput) + (dst_negative_scale_weighted_total_resultproductsentriesentryoutput)) + ((dst_negative_scale_weighted_total_resultproductsentriesentryoutput) + (dst_negative_scale_weighted_total_resultproductsentriesentryoutput)))) * S ((((dst_positive_code_weighted_total_resultproductsentriesentryoutput) + (dst_positive_scale_weighted_total_resultproductsentriesentryoutput)) * S ((dst_positive_code_weighted_total_resultproductsentriesentryoutput) + (dst_positive_scale_weighted_total_resultproductsentriesentryoutput)) + ((dst_positive_scale_weighted_total_resultproductsentriesentryoutput) + (dst_positive_scale_weighted_total_resultproductsentriesentryoutput))) + (((dst_negative_code_weighted_total_resultproductsentriesentryoutput) + (dst_negative_scale_weighted_total_resultproductsentriesentryoutput)) * S ((dst_negative_code_weighted_total_resultproductsentriesentryoutput) + (dst_negative_scale_weighted_total_resultproductsentriesentryoutput)) + ((dst_negative_scale_weighted_total_resultproductsentriesentryoutput) + (dst_negative_scale_weighted_total_resultproductsentriesentryoutput)))) + ((((dst_negative_code_weighted_total_resultproductsentriesentryoutput) + (dst_negative_scale_weighted_total_resultproductsentriesentryoutput)) * S ((dst_negative_code_weighted_total_resultproductsentriesentryoutput) + (dst_negative_scale_weighted_total_resultproductsentriesentryoutput)) + ((dst_negative_scale_weighted_total_resultproductsentriesentryoutput) + (dst_negative_scale_weighted_total_resultproductsentriesentryoutput))) + (((dst_negative_code_weighted_total_resultproductsentriesentryoutput) + (dst_negative_scale_weighted_total_resultproductsentriesentryoutput)) * S ((dst_negative_code_weighted_total_resultproductsentriesentryoutput) + (dst_negative_scale_weighted_total_resultproductsentriesentryoutput)) + ((dst_negative_scale_weighted_total_resultproductsentriesentryoutput) + (dst_negative_scale_weighted_total_resultproductsentriesentryoutput)))))) /\ (((((exists ff_h_pvs_weighted_total_resultproductsentriesentryoutputpositive. ff_h_pvs_weighted_total_resultproductsentriesentryoutputpositive + S (dst_positive_weighted_total_resultproductsentriesentryoutput) = S ((S (sto_index_weighted_total_resultproductsentries)) * dst_positive_scale_weighted_total_resultproductsentriesentryoutput)) /\ exists ff_q_pvs_weighted_total_resultproductsentriesentryoutputpositive. dst_positive_code_weighted_total_resultproductsentriesentryoutput = ff_q_pvs_weighted_total_resultproductsentriesentryoutputpositive * S ((S (sto_index_weighted_total_resultproductsentries)) * dst_positive_scale_weighted_total_resultproductsentriesentryoutput) + (dst_positive_weighted_total_resultproductsentriesentryoutput))) /\ (((((exists ff_h_pvs_weighted_total_resultproductsentriesentryoutputnegative. ff_h_pvs_weighted_total_resultproductsentriesentryoutputnegative + S (dst_negative_weighted_total_resultproductsentriesentryoutput) = S ((S (sto_index_weighted_total_resultproductsentries)) * dst_negative_scale_weighted_total_resultproductsentriesentryoutput)) /\ exists ff_q_pvs_weighted_total_resultproductsentriesentryoutputnegative. dst_negative_code_weighted_total_resultproductsentriesentryoutput = ff_q_pvs_weighted_total_resultproductsentriesentryoutputnegative * S ((S (sto_index_weighted_total_resultproductsentries)) * dst_negative_scale_weighted_total_resultproductsentriesentryoutput) + (dst_negative_weighted_total_resultproductsentriesentryoutput))) /\ (exists ge_balance_positive_weighted_total_resultproductsentriesentryoutputvalue ge_balance_negative_weighted_total_resultproductsentriesentryoutputvalue. (((((sto_output_weighted_total_resultproductsentries) = 2 * (ge_balance_positive_weighted_total_resultproductsentriesentryoutputvalue) /\ (ge_balance_negative_weighted_total_resultproductsentriesentryoutputvalue) = 0) \/ exists ge_signed_half_weighted_total_resultproductsentriesentryoutputvaluedecode. (((sto_output_weighted_total_resultproductsentries) = 2 * ge_signed_half_weighted_total_resultproductsentriesentryoutputvaluedecode + 1 /\ (ge_balance_positive_weighted_total_resultproductsentriesentryoutputvalue) = 0) /\ (ge_balance_negative_weighted_total_resultproductsentriesentryoutputvalue) = S ge_signed_half_weighted_total_resultproductsentriesentryoutputvaluedecode))) /\ ((dst_positive_weighted_total_resultproductsentriesentryoutput) + ge_balance_negative_weighted_total_resultproductsentriesentryoutputvalue = (dst_negative_weighted_total_resultproductsentriesentryoutput) + ge_balance_positive_weighted_total_resultproductsentriesentryoutputvalue))))))))) /\ (exists sto_ap_weighted_total_resultproductsentriesentryoperation sto_an_weighted_total_resultproductsentriesentryoperation sto_bp_weighted_total_resultproductsentriesentryoperation sto_bn_weighted_total_resultproductsentriesentryoperation sto_cp_weighted_total_resultproductsentriesentryoperation sto_cn_weighted_total_resultproductsentriesentryoperation. (((((sto_left_weighted_total_resultproductsentries) = 2 * (sto_ap_weighted_total_resultproductsentriesentryoperation) /\ (sto_an_weighted_total_resultproductsentriesentryoperation) = 0) \/ exists ge_signed_half_weighted_total_resultproductsentriesentryoperationleft. (((sto_left_weighted_total_resultproductsentries) = 2 * ge_signed_half_weighted_total_resultproductsentriesentryoperationleft + 1 /\ (sto_ap_weighted_total_resultproductsentriesentryoperation) = 0) /\ (sto_an_weighted_total_resultproductsentriesentryoperation) = S ge_signed_half_weighted_total_resultproductsentriesentryoperationleft))) /\ ((((((sto_right_weighted_total_resultproductsentries) = 2 * (sto_bp_weighted_total_resultproductsentriesentryoperation) /\ (sto_bn_weighted_total_resultproductsentriesentryoperation) = 0) \/ exists ge_signed_half_weighted_total_resultproductsentriesentryoperationright. (((sto_right_weighted_total_resultproductsentries) = 2 * ge_signed_half_weighted_total_resultproductsentriesentryoperationright + 1 /\ (sto_bp_weighted_total_resultproductsentriesentryoperation) = 0) /\ (sto_bn_weighted_total_resultproductsentriesentryoperation) = S ge_signed_half_weighted_total_resultproductsentriesentryoperationright))) /\ ((((((sto_output_weighted_total_resultproductsentries) = 2 * (sto_cp_weighted_total_resultproductsentriesentryoperation) /\ (sto_cn_weighted_total_resultproductsentriesentryoperation) = 0) \/ exists ge_signed_half_weighted_total_resultproductsentriesentryoperationoutput. (((sto_output_weighted_total_resultproductsentries) = 2 * ge_signed_half_weighted_total_resultproductsentriesentryoperationoutput + 1 /\ (sto_cp_weighted_total_resultproductsentriesentryoperation) = 0) /\ (sto_cn_weighted_total_resultproductsentriesentryoperation) = S ge_signed_half_weighted_total_resultproductsentriesentryoperationoutput))) /\ ((sto_ap_weighted_total_resultproductsentriesentryoperation * sto_bp_weighted_total_resultproductsentriesentryoperation + sto_an_weighted_total_resultproductsentriesentryoperation * sto_bn_weighted_total_resultproductsentriesentryoperation) + sto_cn_weighted_total_resultproductsentriesentryoperation = (sto_ap_weighted_total_resultproductsentriesentryoperation * sto_bn_weighted_total_resultproductsentriesentryoperation + sto_an_weighted_total_resultproductsentriesentryoperation * sto_bp_weighted_total_resultproductsentriesentryoperation) + sto_cp_weighted_total_resultproductsentriesentryoperation))))))))))))))))))) /\ (exists dst_positive_code_weighted_total_resultsum dst_positive_scale_weighted_total_resultsum dst_negative_code_weighted_total_resultsum dst_negative_scale_weighted_total_resultsum dst_positive_sum_weighted_total_resultsum dst_negative_sum_weighted_total_resultsum. (((sws_product_table_weighted_total_result) = (((((dst_positive_code_weighted_total_resultsum) + (dst_positive_scale_weighted_total_resultsum)) * S ((dst_positive_code_weighted_total_resultsum) + (dst_positive_scale_weighted_total_resultsum)) + ((dst_positive_scale_weighted_total_resultsum) + (dst_positive_scale_weighted_total_resultsum))) + (((dst_negative_code_weighted_total_resultsum) + (dst_negative_scale_weighted_total_resultsum)) * S ((dst_negative_code_weighted_total_resultsum) + (dst_negative_scale_weighted_total_resultsum)) + ((dst_negative_scale_weighted_total_resultsum) + (dst_negative_scale_weighted_total_resultsum)))) * S ((((dst_positive_code_weighted_total_resultsum) + (dst_positive_scale_weighted_total_resultsum)) * S ((dst_positive_code_weighted_total_resultsum) + (dst_positive_scale_weighted_total_resultsum)) + ((dst_positive_scale_weighted_total_resultsum) + (dst_positive_scale_weighted_total_resultsum))) + (((dst_negative_code_weighted_total_resultsum) + (dst_negative_scale_weighted_total_resultsum)) * S ((dst_negative_code_weighted_total_resultsum) + (dst_negative_scale_weighted_total_resultsum)) + ((dst_negative_scale_weighted_total_resultsum) + (dst_negative_scale_weighted_total_resultsum)))) + ((((dst_negative_code_weighted_total_resultsum) + (dst_negative_scale_weighted_total_resultsum)) * S ((dst_negative_code_weighted_total_resultsum) + (dst_negative_scale_weighted_total_resultsum)) + ((dst_negative_scale_weighted_total_resultsum) + (dst_negative_scale_weighted_total_resultsum))) + (((dst_negative_code_weighted_total_resultsum) + (dst_negative_scale_weighted_total_resultsum)) * S ((dst_negative_code_weighted_total_resultsum) + (dst_negative_scale_weighted_total_resultsum)) + ((dst_negative_scale_weighted_total_resultsum) + (dst_negative_scale_weighted_total_resultsum)))))) /\ (((exists fs_u_dst_weighted_total_resultsumpositive fs_v_dst_weighted_total_resultsumpositive. ((((exists fs_h_dst_weighted_total_resultsumpositive_body_start. fs_h_dst_weighted_total_resultsumpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_weighted_total_resultsumpositive)) /\ exists fs_q_dst_weighted_total_resultsumpositive_body_start. fs_u_dst_weighted_total_resultsumpositive = fs_q_dst_weighted_total_resultsumpositive_body_start * S ((S (0)) * fs_v_dst_weighted_total_resultsumpositive) + (0))) /\ ((((exists fs_h_dst_weighted_total_resultsumpositive_body_terminal. fs_h_dst_weighted_total_resultsumpositive_body_terminal + S (dst_positive_sum_weighted_total_resultsum) = S ((S (l)) * fs_v_dst_weighted_total_resultsumpositive)) /\ exists fs_q_dst_weighted_total_resultsumpositive_body_terminal. fs_u_dst_weighted_total_resultsumpositive = fs_q_dst_weighted_total_resultsumpositive_body_terminal * S ((S (l)) * fs_v_dst_weighted_total_resultsumpositive) + (dst_positive_sum_weighted_total_resultsum))) /\ forall fs_i_dst_weighted_total_resultsumpositive_body_steps. (exists fs_lt_dst_weighted_total_resultsumpositive_body_steps_bound. fs_lt_dst_weighted_total_resultsumpositive_body_steps_bound + S fs_i_dst_weighted_total_resultsumpositive_body_steps = l) -> exists fs_a_dst_weighted_total_resultsumpositive_body_steps fs_r_dst_weighted_total_resultsumpositive_body_steps fs_s_dst_weighted_total_resultsumpositive_body_steps. ((((exists fs_h_dst_weighted_total_resultsumpositive_body_steps_summand. fs_h_dst_weighted_total_resultsumpositive_body_steps_summand + S (fs_a_dst_weighted_total_resultsumpositive_body_steps) = S ((S (fs_i_dst_weighted_total_resultsumpositive_body_steps)) * dst_positive_scale_weighted_total_resultsum)) /\ exists fs_q_dst_weighted_total_resultsumpositive_body_steps_summand. dst_positive_code_weighted_total_resultsum = fs_q_dst_weighted_total_resultsumpositive_body_steps_summand * S ((S (fs_i_dst_weighted_total_resultsumpositive_body_steps)) * dst_positive_scale_weighted_total_resultsum) + (fs_a_dst_weighted_total_resultsumpositive_body_steps))) /\ ((((exists fs_h_dst_weighted_total_resultsumpositive_body_steps_partial. fs_h_dst_weighted_total_resultsumpositive_body_steps_partial + S (fs_r_dst_weighted_total_resultsumpositive_body_steps) = S ((S (fs_i_dst_weighted_total_resultsumpositive_body_steps)) * fs_v_dst_weighted_total_resultsumpositive)) /\ exists fs_q_dst_weighted_total_resultsumpositive_body_steps_partial. fs_u_dst_weighted_total_resultsumpositive = fs_q_dst_weighted_total_resultsumpositive_body_steps_partial * S ((S (fs_i_dst_weighted_total_resultsumpositive_body_steps)) * fs_v_dst_weighted_total_resultsumpositive) + (fs_r_dst_weighted_total_resultsumpositive_body_steps))) /\ ((((exists fs_h_dst_weighted_total_resultsumpositive_body_steps_successor. fs_h_dst_weighted_total_resultsumpositive_body_steps_successor + S (fs_s_dst_weighted_total_resultsumpositive_body_steps) = S ((S (S fs_i_dst_weighted_total_resultsumpositive_body_steps)) * fs_v_dst_weighted_total_resultsumpositive)) /\ exists fs_q_dst_weighted_total_resultsumpositive_body_steps_successor. fs_u_dst_weighted_total_resultsumpositive = fs_q_dst_weighted_total_resultsumpositive_body_steps_successor * S ((S (S fs_i_dst_weighted_total_resultsumpositive_body_steps)) * fs_v_dst_weighted_total_resultsumpositive) + (fs_s_dst_weighted_total_resultsumpositive_body_steps))) /\ fs_s_dst_weighted_total_resultsumpositive_body_steps = fs_r_dst_weighted_total_resultsumpositive_body_steps + fs_a_dst_weighted_total_resultsumpositive_body_steps)))))) /\ (((exists fs_u_dst_weighted_total_resultsumnegative fs_v_dst_weighted_total_resultsumnegative. ((((exists fs_h_dst_weighted_total_resultsumnegative_body_start. fs_h_dst_weighted_total_resultsumnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_weighted_total_resultsumnegative)) /\ exists fs_q_dst_weighted_total_resultsumnegative_body_start. fs_u_dst_weighted_total_resultsumnegative = fs_q_dst_weighted_total_resultsumnegative_body_start * S ((S (0)) * fs_v_dst_weighted_total_resultsumnegative) + (0))) /\ ((((exists fs_h_dst_weighted_total_resultsumnegative_body_terminal. fs_h_dst_weighted_total_resultsumnegative_body_terminal + S (dst_negative_sum_weighted_total_resultsum) = S ((S (l)) * fs_v_dst_weighted_total_resultsumnegative)) /\ exists fs_q_dst_weighted_total_resultsumnegative_body_terminal. fs_u_dst_weighted_total_resultsumnegative = fs_q_dst_weighted_total_resultsumnegative_body_terminal * S ((S (l)) * fs_v_dst_weighted_total_resultsumnegative) + (dst_negative_sum_weighted_total_resultsum))) /\ forall fs_i_dst_weighted_total_resultsumnegative_body_steps. (exists fs_lt_dst_weighted_total_resultsumnegative_body_steps_bound. fs_lt_dst_weighted_total_resultsumnegative_body_steps_bound + S fs_i_dst_weighted_total_resultsumnegative_body_steps = l) -> exists fs_a_dst_weighted_total_resultsumnegative_body_steps fs_r_dst_weighted_total_resultsumnegative_body_steps fs_s_dst_weighted_total_resultsumnegative_body_steps. ((((exists fs_h_dst_weighted_total_resultsumnegative_body_steps_summand. fs_h_dst_weighted_total_resultsumnegative_body_steps_summand + S (fs_a_dst_weighted_total_resultsumnegative_body_steps) = S ((S (fs_i_dst_weighted_total_resultsumnegative_body_steps)) * dst_negative_scale_weighted_total_resultsum)) /\ exists fs_q_dst_weighted_total_resultsumnegative_body_steps_summand. dst_negative_code_weighted_total_resultsum = fs_q_dst_weighted_total_resultsumnegative_body_steps_summand * S ((S (fs_i_dst_weighted_total_resultsumnegative_body_steps)) * dst_negative_scale_weighted_total_resultsum) + (fs_a_dst_weighted_total_resultsumnegative_body_steps))) /\ ((((exists fs_h_dst_weighted_total_resultsumnegative_body_steps_partial. fs_h_dst_weighted_total_resultsumnegative_body_steps_partial + S (fs_r_dst_weighted_total_resultsumnegative_body_steps) = S ((S (fs_i_dst_weighted_total_resultsumnegative_body_steps)) * fs_v_dst_weighted_total_resultsumnegative)) /\ exists fs_q_dst_weighted_total_resultsumnegative_body_steps_partial. fs_u_dst_weighted_total_resultsumnegative = fs_q_dst_weighted_total_resultsumnegative_body_steps_partial * S ((S (fs_i_dst_weighted_total_resultsumnegative_body_steps)) * fs_v_dst_weighted_total_resultsumnegative) + (fs_r_dst_weighted_total_resultsumnegative_body_steps))) /\ ((((exists fs_h_dst_weighted_total_resultsumnegative_body_steps_successor. fs_h_dst_weighted_total_resultsumnegative_body_steps_successor + S (fs_s_dst_weighted_total_resultsumnegative_body_steps) = S ((S (S fs_i_dst_weighted_total_resultsumnegative_body_steps)) * fs_v_dst_weighted_total_resultsumnegative)) /\ exists fs_q_dst_weighted_total_resultsumnegative_body_steps_successor. fs_u_dst_weighted_total_resultsumnegative = fs_q_dst_weighted_total_resultsumnegative_body_steps_successor * S ((S (S fs_i_dst_weighted_total_resultsumnegative_body_steps)) * fs_v_dst_weighted_total_resultsumnegative) + (fs_s_dst_weighted_total_resultsumnegative_body_steps))) /\ fs_s_dst_weighted_total_resultsumnegative_body_steps = fs_r_dst_weighted_total_resultsumnegative_body_steps + fs_a_dst_weighted_total_resultsumnegative_body_steps)))))) /\ (exists ge_balance_positive_weighted_total_resultsumresult ge_balance_negative_weighted_total_resultsumresult. (((((z) = 2 * (ge_balance_positive_weighted_total_resultsumresult) /\ (ge_balance_negative_weighted_total_resultsumresult) = 0) \/ exists ge_signed_half_weighted_total_resultsumresultdecode. (((z) = 2 * ge_signed_half_weighted_total_resultsumresultdecode + 1 /\ (ge_balance_positive_weighted_total_resultsumresult) = 0) /\ (ge_balance_negative_weighted_total_resultsumresult) = S ge_signed_half_weighted_total_resultsumresultdecode))) /\ ((dst_positive_sum_weighted_total_resultsum) + ge_balance_negative_weighted_total_resultsumresult = (dst_negative_sum_weighted_total_resultsum) + ge_balance_positive_weighted_total_resultsumresult))))))))))) /\ (forall u. (exists sws_product_table_weighted_total_compare. ((((exists dst_positive_code_weighted_total_compareproductsleft_table dst_positive_scale_weighted_total_compareproductsleft_table dst_negative_code_weighted_total_compareproductsleft_table dst_negative_scale_weighted_total_compareproductsleft_table. (((W) = (((((dst_positive_code_weighted_total_compareproductsleft_table) + (dst_positive_scale_weighted_total_compareproductsleft_table)) * S ((dst_positive_code_weighted_total_compareproductsleft_table) + (dst_positive_scale_weighted_total_compareproductsleft_table)) + ((dst_positive_scale_weighted_total_compareproductsleft_table) + (dst_positive_scale_weighted_total_compareproductsleft_table))) + (((dst_negative_code_weighted_total_compareproductsleft_table) + (dst_negative_scale_weighted_total_compareproductsleft_table)) * S ((dst_negative_code_weighted_total_compareproductsleft_table) + (dst_negative_scale_weighted_total_compareproductsleft_table)) + ((dst_negative_scale_weighted_total_compareproductsleft_table) + (dst_negative_scale_weighted_total_compareproductsleft_table)))) * S ((((dst_positive_code_weighted_total_compareproductsleft_table) + (dst_positive_scale_weighted_total_compareproductsleft_table)) * S ((dst_positive_code_weighted_total_compareproductsleft_table) + (dst_positive_scale_weighted_total_compareproductsleft_table)) + ((dst_positive_scale_weighted_total_compareproductsleft_table) + (dst_positive_scale_weighted_total_compareproductsleft_table))) + (((dst_negative_code_weighted_total_compareproductsleft_table) + (dst_negative_scale_weighted_total_compareproductsleft_table)) * S ((dst_negative_code_weighted_total_compareproductsleft_table) + (dst_negative_scale_weighted_total_compareproductsleft_table)) + ((dst_negative_scale_weighted_total_compareproductsleft_table) + (dst_negative_scale_weighted_total_compareproductsleft_table)))) + ((((dst_negative_code_weighted_total_compareproductsleft_table) + (dst_negative_scale_weighted_total_compareproductsleft_table)) * S ((dst_negative_code_weighted_total_compareproductsleft_table) + (dst_negative_scale_weighted_total_compareproductsleft_table)) + ((dst_negative_scale_weighted_total_compareproductsleft_table) + (dst_negative_scale_weighted_total_compareproductsleft_table))) + (((dst_negative_code_weighted_total_compareproductsleft_table) + (dst_negative_scale_weighted_total_compareproductsleft_table)) * S ((dst_negative_code_weighted_total_compareproductsleft_table) + (dst_negative_scale_weighted_total_compareproductsleft_table)) + ((dst_negative_scale_weighted_total_compareproductsleft_table) + (dst_negative_scale_weighted_total_compareproductsleft_table)))))) /\ (forall dst_index_weighted_total_compareproductsleft_table. (exists pvs_le_gap_weighted_total_compareproductsleft_tabledomain. pvs_le_gap_weighted_total_compareproductsleft_tabledomain + (dst_index_weighted_total_compareproductsleft_table) = (l)) -> exists dst_positive_weighted_total_compareproductsleft_table dst_negative_weighted_total_compareproductsleft_table dst_value_weighted_total_compareproductsleft_table. ((((exists ff_h_pvs_weighted_total_compareproductsleft_tableentrypositive. ff_h_pvs_weighted_total_compareproductsleft_tableentrypositive + S (dst_positive_weighted_total_compareproductsleft_table) = S ((S (dst_index_weighted_total_compareproductsleft_table)) * dst_positive_scale_weighted_total_compareproductsleft_table)) /\ exists ff_q_pvs_weighted_total_compareproductsleft_tableentrypositive. dst_positive_code_weighted_total_compareproductsleft_table = ff_q_pvs_weighted_total_compareproductsleft_tableentrypositive * S ((S (dst_index_weighted_total_compareproductsleft_table)) * dst_positive_scale_weighted_total_compareproductsleft_table) + (dst_positive_weighted_total_compareproductsleft_table))) /\ (((((exists ff_h_pvs_weighted_total_compareproductsleft_tableentrynegative. ff_h_pvs_weighted_total_compareproductsleft_tableentrynegative + S (dst_negative_weighted_total_compareproductsleft_table) = S ((S (dst_index_weighted_total_compareproductsleft_table)) * dst_negative_scale_weighted_total_compareproductsleft_table)) /\ exists ff_q_pvs_weighted_total_compareproductsleft_tableentrynegative. dst_negative_code_weighted_total_compareproductsleft_table = ff_q_pvs_weighted_total_compareproductsleft_tableentrynegative * S ((S (dst_index_weighted_total_compareproductsleft_table)) * dst_negative_scale_weighted_total_compareproductsleft_table) + (dst_negative_weighted_total_compareproductsleft_table))) /\ (exists ge_balance_positive_weighted_total_compareproductsleft_tableentryvalue ge_balance_negative_weighted_total_compareproductsleft_tableentryvalue. (((((dst_value_weighted_total_compareproductsleft_table) = 2 * (ge_balance_positive_weighted_total_compareproductsleft_tableentryvalue) /\ (ge_balance_negative_weighted_total_compareproductsleft_tableentryvalue) = 0) \/ exists ge_signed_half_weighted_total_compareproductsleft_tableentryvaluedecode. (((dst_value_weighted_total_compareproductsleft_table) = 2 * ge_signed_half_weighted_total_compareproductsleft_tableentryvaluedecode + 1 /\ (ge_balance_positive_weighted_total_compareproductsleft_tableentryvalue) = 0) /\ (ge_balance_negative_weighted_total_compareproductsleft_tableentryvalue) = S ge_signed_half_weighted_total_compareproductsleft_tableentryvaluedecode))) /\ ((dst_positive_weighted_total_compareproductsleft_table) + ge_balance_negative_weighted_total_compareproductsleft_tableentryvalue = (dst_negative_weighted_total_compareproductsleft_table) + ge_balance_positive_weighted_total_compareproductsleft_tableentryvalue))))))))) /\ (((exists dst_positive_code_weighted_total_compareproductsright_table dst_positive_scale_weighted_total_compareproductsright_table dst_negative_code_weighted_total_compareproductsright_table dst_negative_scale_weighted_total_compareproductsright_table. (((F) = (((((dst_positive_code_weighted_total_compareproductsright_table) + (dst_positive_scale_weighted_total_compareproductsright_table)) * S ((dst_positive_code_weighted_total_compareproductsright_table) + (dst_positive_scale_weighted_total_compareproductsright_table)) + ((dst_positive_scale_weighted_total_compareproductsright_table) + (dst_positive_scale_weighted_total_compareproductsright_table))) + (((dst_negative_code_weighted_total_compareproductsright_table) + (dst_negative_scale_weighted_total_compareproductsright_table)) * S ((dst_negative_code_weighted_total_compareproductsright_table) + (dst_negative_scale_weighted_total_compareproductsright_table)) + ((dst_negative_scale_weighted_total_compareproductsright_table) + (dst_negative_scale_weighted_total_compareproductsright_table)))) * S ((((dst_positive_code_weighted_total_compareproductsright_table) + (dst_positive_scale_weighted_total_compareproductsright_table)) * S ((dst_positive_code_weighted_total_compareproductsright_table) + (dst_positive_scale_weighted_total_compareproductsright_table)) + ((dst_positive_scale_weighted_total_compareproductsright_table) + (dst_positive_scale_weighted_total_compareproductsright_table))) + (((dst_negative_code_weighted_total_compareproductsright_table) + (dst_negative_scale_weighted_total_compareproductsright_table)) * S ((dst_negative_code_weighted_total_compareproductsright_table) + (dst_negative_scale_weighted_total_compareproductsright_table)) + ((dst_negative_scale_weighted_total_compareproductsright_table) + (dst_negative_scale_weighted_total_compareproductsright_table)))) + ((((dst_negative_code_weighted_total_compareproductsright_table) + (dst_negative_scale_weighted_total_compareproductsright_table)) * S ((dst_negative_code_weighted_total_compareproductsright_table) + (dst_negative_scale_weighted_total_compareproductsright_table)) + ((dst_negative_scale_weighted_total_compareproductsright_table) + (dst_negative_scale_weighted_total_compareproductsright_table))) + (((dst_negative_code_weighted_total_compareproductsright_table) + (dst_negative_scale_weighted_total_compareproductsright_table)) * S ((dst_negative_code_weighted_total_compareproductsright_table) + (dst_negative_scale_weighted_total_compareproductsright_table)) + ((dst_negative_scale_weighted_total_compareproductsright_table) + (dst_negative_scale_weighted_total_compareproductsright_table)))))) /\ (forall dst_index_weighted_total_compareproductsright_table. (exists pvs_le_gap_weighted_total_compareproductsright_tabledomain. pvs_le_gap_weighted_total_compareproductsright_tabledomain + (dst_index_weighted_total_compareproductsright_table) = (l)) -> exists dst_positive_weighted_total_compareproductsright_table dst_negative_weighted_total_compareproductsright_table dst_value_weighted_total_compareproductsright_table. ((((exists ff_h_pvs_weighted_total_compareproductsright_tableentrypositive. ff_h_pvs_weighted_total_compareproductsright_tableentrypositive + S (dst_positive_weighted_total_compareproductsright_table) = S ((S (dst_index_weighted_total_compareproductsright_table)) * dst_positive_scale_weighted_total_compareproductsright_table)) /\ exists ff_q_pvs_weighted_total_compareproductsright_tableentrypositive. dst_positive_code_weighted_total_compareproductsright_table = ff_q_pvs_weighted_total_compareproductsright_tableentrypositive * S ((S (dst_index_weighted_total_compareproductsright_table)) * dst_positive_scale_weighted_total_compareproductsright_table) + (dst_positive_weighted_total_compareproductsright_table))) /\ (((((exists ff_h_pvs_weighted_total_compareproductsright_tableentrynegative. ff_h_pvs_weighted_total_compareproductsright_tableentrynegative + S (dst_negative_weighted_total_compareproductsright_table) = S ((S (dst_index_weighted_total_compareproductsright_table)) * dst_negative_scale_weighted_total_compareproductsright_table)) /\ exists ff_q_pvs_weighted_total_compareproductsright_tableentrynegative. dst_negative_code_weighted_total_compareproductsright_table = ff_q_pvs_weighted_total_compareproductsright_tableentrynegative * S ((S (dst_index_weighted_total_compareproductsright_table)) * dst_negative_scale_weighted_total_compareproductsright_table) + (dst_negative_weighted_total_compareproductsright_table))) /\ (exists ge_balance_positive_weighted_total_compareproductsright_tableentryvalue ge_balance_negative_weighted_total_compareproductsright_tableentryvalue. (((((dst_value_weighted_total_compareproductsright_table) = 2 * (ge_balance_positive_weighted_total_compareproductsright_tableentryvalue) /\ (ge_balance_negative_weighted_total_compareproductsright_tableentryvalue) = 0) \/ exists ge_signed_half_weighted_total_compareproductsright_tableentryvaluedecode. (((dst_value_weighted_total_compareproductsright_table) = 2 * ge_signed_half_weighted_total_compareproductsright_tableentryvaluedecode + 1 /\ (ge_balance_positive_weighted_total_compareproductsright_tableentryvalue) = 0) /\ (ge_balance_negative_weighted_total_compareproductsright_tableentryvalue) = S ge_signed_half_weighted_total_compareproductsright_tableentryvaluedecode))) /\ ((dst_positive_weighted_total_compareproductsright_table) + ge_balance_negative_weighted_total_compareproductsright_tableentryvalue = (dst_negative_weighted_total_compareproductsright_table) + ge_balance_positive_weighted_total_compareproductsright_tableentryvalue))))))))) /\ (((exists dst_positive_code_weighted_total_compareproductsoutput_table dst_positive_scale_weighted_total_compareproductsoutput_table dst_negative_code_weighted_total_compareproductsoutput_table dst_negative_scale_weighted_total_compareproductsoutput_table. (((sws_product_table_weighted_total_compare) = (((((dst_positive_code_weighted_total_compareproductsoutput_table) + (dst_positive_scale_weighted_total_compareproductsoutput_table)) * S ((dst_positive_code_weighted_total_compareproductsoutput_table) + (dst_positive_scale_weighted_total_compareproductsoutput_table)) + ((dst_positive_scale_weighted_total_compareproductsoutput_table) + (dst_positive_scale_weighted_total_compareproductsoutput_table))) + (((dst_negative_code_weighted_total_compareproductsoutput_table) + (dst_negative_scale_weighted_total_compareproductsoutput_table)) * S ((dst_negative_code_weighted_total_compareproductsoutput_table) + (dst_negative_scale_weighted_total_compareproductsoutput_table)) + ((dst_negative_scale_weighted_total_compareproductsoutput_table) + (dst_negative_scale_weighted_total_compareproductsoutput_table)))) * S ((((dst_positive_code_weighted_total_compareproductsoutput_table) + (dst_positive_scale_weighted_total_compareproductsoutput_table)) * S ((dst_positive_code_weighted_total_compareproductsoutput_table) + (dst_positive_scale_weighted_total_compareproductsoutput_table)) + ((dst_positive_scale_weighted_total_compareproductsoutput_table) + (dst_positive_scale_weighted_total_compareproductsoutput_table))) + (((dst_negative_code_weighted_total_compareproductsoutput_table) + (dst_negative_scale_weighted_total_compareproductsoutput_table)) * S ((dst_negative_code_weighted_total_compareproductsoutput_table) + (dst_negative_scale_weighted_total_compareproductsoutput_table)) + ((dst_negative_scale_weighted_total_compareproductsoutput_table) + (dst_negative_scale_weighted_total_compareproductsoutput_table)))) + ((((dst_negative_code_weighted_total_compareproductsoutput_table) + (dst_negative_scale_weighted_total_compareproductsoutput_table)) * S ((dst_negative_code_weighted_total_compareproductsoutput_table) + (dst_negative_scale_weighted_total_compareproductsoutput_table)) + ((dst_negative_scale_weighted_total_compareproductsoutput_table) + (dst_negative_scale_weighted_total_compareproductsoutput_table))) + (((dst_negative_code_weighted_total_compareproductsoutput_table) + (dst_negative_scale_weighted_total_compareproductsoutput_table)) * S ((dst_negative_code_weighted_total_compareproductsoutput_table) + (dst_negative_scale_weighted_total_compareproductsoutput_table)) + ((dst_negative_scale_weighted_total_compareproductsoutput_table) + (dst_negative_scale_weighted_total_compareproductsoutput_table)))))) /\ (forall dst_index_weighted_total_compareproductsoutput_table. (exists pvs_le_gap_weighted_total_compareproductsoutput_tabledomain. pvs_le_gap_weighted_total_compareproductsoutput_tabledomain + (dst_index_weighted_total_compareproductsoutput_table) = (l)) -> exists dst_positive_weighted_total_compareproductsoutput_table dst_negative_weighted_total_compareproductsoutput_table dst_value_weighted_total_compareproductsoutput_table. ((((exists ff_h_pvs_weighted_total_compareproductsoutput_tableentrypositive. ff_h_pvs_weighted_total_compareproductsoutput_tableentrypositive + S (dst_positive_weighted_total_compareproductsoutput_table) = S ((S (dst_index_weighted_total_compareproductsoutput_table)) * dst_positive_scale_weighted_total_compareproductsoutput_table)) /\ exists ff_q_pvs_weighted_total_compareproductsoutput_tableentrypositive. dst_positive_code_weighted_total_compareproductsoutput_table = ff_q_pvs_weighted_total_compareproductsoutput_tableentrypositive * S ((S (dst_index_weighted_total_compareproductsoutput_table)) * dst_positive_scale_weighted_total_compareproductsoutput_table) + (dst_positive_weighted_total_compareproductsoutput_table))) /\ (((((exists ff_h_pvs_weighted_total_compareproductsoutput_tableentrynegative. ff_h_pvs_weighted_total_compareproductsoutput_tableentrynegative + S (dst_negative_weighted_total_compareproductsoutput_table) = S ((S (dst_index_weighted_total_compareproductsoutput_table)) * dst_negative_scale_weighted_total_compareproductsoutput_table)) /\ exists ff_q_pvs_weighted_total_compareproductsoutput_tableentrynegative. dst_negative_code_weighted_total_compareproductsoutput_table = ff_q_pvs_weighted_total_compareproductsoutput_tableentrynegative * S ((S (dst_index_weighted_total_compareproductsoutput_table)) * dst_negative_scale_weighted_total_compareproductsoutput_table) + (dst_negative_weighted_total_compareproductsoutput_table))) /\ (exists ge_balance_positive_weighted_total_compareproductsoutput_tableentryvalue ge_balance_negative_weighted_total_compareproductsoutput_tableentryvalue. (((((dst_value_weighted_total_compareproductsoutput_table) = 2 * (ge_balance_positive_weighted_total_compareproductsoutput_tableentryvalue) /\ (ge_balance_negative_weighted_total_compareproductsoutput_tableentryvalue) = 0) \/ exists ge_signed_half_weighted_total_compareproductsoutput_tableentryvaluedecode. (((dst_value_weighted_total_compareproductsoutput_table) = 2 * ge_signed_half_weighted_total_compareproductsoutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_weighted_total_compareproductsoutput_tableentryvalue) = 0) /\ (ge_balance_negative_weighted_total_compareproductsoutput_tableentryvalue) = S ge_signed_half_weighted_total_compareproductsoutput_tableentryvaluedecode))) /\ ((dst_positive_weighted_total_compareproductsoutput_table) + ge_balance_negative_weighted_total_compareproductsoutput_tableentryvalue = (dst_negative_weighted_total_compareproductsoutput_table) + ge_balance_positive_weighted_total_compareproductsoutput_tableentryvalue))))))))) /\ (forall sto_index_weighted_total_compareproductsentries. (exists pvs_gap_weighted_total_compareproductsentriesbound. pvs_gap_weighted_total_compareproductsentriesbound + S (sto_index_weighted_total_compareproductsentries) = (l)) -> exists sto_left_weighted_total_compareproductsentries sto_right_weighted_total_compareproductsentries sto_output_weighted_total_compareproductsentries. ((exists dst_positive_code_weighted_total_compareproductsentriesentryleft dst_positive_scale_weighted_total_compareproductsentriesentryleft dst_negative_code_weighted_total_compareproductsentriesentryleft dst_negative_scale_weighted_total_compareproductsentriesentryleft dst_positive_weighted_total_compareproductsentriesentryleft dst_negative_weighted_total_compareproductsentriesentryleft. (((W) = (((((dst_positive_code_weighted_total_compareproductsentriesentryleft) + (dst_positive_scale_weighted_total_compareproductsentriesentryleft)) * S ((dst_positive_code_weighted_total_compareproductsentriesentryleft) + (dst_positive_scale_weighted_total_compareproductsentriesentryleft)) + ((dst_positive_scale_weighted_total_compareproductsentriesentryleft) + (dst_positive_scale_weighted_total_compareproductsentriesentryleft))) + (((dst_negative_code_weighted_total_compareproductsentriesentryleft) + (dst_negative_scale_weighted_total_compareproductsentriesentryleft)) * S ((dst_negative_code_weighted_total_compareproductsentriesentryleft) + (dst_negative_scale_weighted_total_compareproductsentriesentryleft)) + ((dst_negative_scale_weighted_total_compareproductsentriesentryleft) + (dst_negative_scale_weighted_total_compareproductsentriesentryleft)))) * S ((((dst_positive_code_weighted_total_compareproductsentriesentryleft) + (dst_positive_scale_weighted_total_compareproductsentriesentryleft)) * S ((dst_positive_code_weighted_total_compareproductsentriesentryleft) + (dst_positive_scale_weighted_total_compareproductsentriesentryleft)) + ((dst_positive_scale_weighted_total_compareproductsentriesentryleft) + (dst_positive_scale_weighted_total_compareproductsentriesentryleft))) + (((dst_negative_code_weighted_total_compareproductsentriesentryleft) + (dst_negative_scale_weighted_total_compareproductsentriesentryleft)) * S ((dst_negative_code_weighted_total_compareproductsentriesentryleft) + (dst_negative_scale_weighted_total_compareproductsentriesentryleft)) + ((dst_negative_scale_weighted_total_compareproductsentriesentryleft) + (dst_negative_scale_weighted_total_compareproductsentriesentryleft)))) + ((((dst_negative_code_weighted_total_compareproductsentriesentryleft) + (dst_negative_scale_weighted_total_compareproductsentriesentryleft)) * S ((dst_negative_code_weighted_total_compareproductsentriesentryleft) + (dst_negative_scale_weighted_total_compareproductsentriesentryleft)) + ((dst_negative_scale_weighted_total_compareproductsentriesentryleft) + (dst_negative_scale_weighted_total_compareproductsentriesentryleft))) + (((dst_negative_code_weighted_total_compareproductsentriesentryleft) + (dst_negative_scale_weighted_total_compareproductsentriesentryleft)) * S ((dst_negative_code_weighted_total_compareproductsentriesentryleft) + (dst_negative_scale_weighted_total_compareproductsentriesentryleft)) + ((dst_negative_scale_weighted_total_compareproductsentriesentryleft) + (dst_negative_scale_weighted_total_compareproductsentriesentryleft)))))) /\ (((((exists ff_h_pvs_weighted_total_compareproductsentriesentryleftpositive. ff_h_pvs_weighted_total_compareproductsentriesentryleftpositive + S (dst_positive_weighted_total_compareproductsentriesentryleft) = S ((S (sto_index_weighted_total_compareproductsentries)) * dst_positive_scale_weighted_total_compareproductsentriesentryleft)) /\ exists ff_q_pvs_weighted_total_compareproductsentriesentryleftpositive. dst_positive_code_weighted_total_compareproductsentriesentryleft = ff_q_pvs_weighted_total_compareproductsentriesentryleftpositive * S ((S (sto_index_weighted_total_compareproductsentries)) * dst_positive_scale_weighted_total_compareproductsentriesentryleft) + (dst_positive_weighted_total_compareproductsentriesentryleft))) /\ (((((exists ff_h_pvs_weighted_total_compareproductsentriesentryleftnegative. ff_h_pvs_weighted_total_compareproductsentriesentryleftnegative + S (dst_negative_weighted_total_compareproductsentriesentryleft) = S ((S (sto_index_weighted_total_compareproductsentries)) * dst_negative_scale_weighted_total_compareproductsentriesentryleft)) /\ exists ff_q_pvs_weighted_total_compareproductsentriesentryleftnegative. dst_negative_code_weighted_total_compareproductsentriesentryleft = ff_q_pvs_weighted_total_compareproductsentriesentryleftnegative * S ((S (sto_index_weighted_total_compareproductsentries)) * dst_negative_scale_weighted_total_compareproductsentriesentryleft) + (dst_negative_weighted_total_compareproductsentriesentryleft))) /\ (exists ge_balance_positive_weighted_total_compareproductsentriesentryleftvalue ge_balance_negative_weighted_total_compareproductsentriesentryleftvalue. (((((sto_left_weighted_total_compareproductsentries) = 2 * (ge_balance_positive_weighted_total_compareproductsentriesentryleftvalue) /\ (ge_balance_negative_weighted_total_compareproductsentriesentryleftvalue) = 0) \/ exists ge_signed_half_weighted_total_compareproductsentriesentryleftvaluedecode. (((sto_left_weighted_total_compareproductsentries) = 2 * ge_signed_half_weighted_total_compareproductsentriesentryleftvaluedecode + 1 /\ (ge_balance_positive_weighted_total_compareproductsentriesentryleftvalue) = 0) /\ (ge_balance_negative_weighted_total_compareproductsentriesentryleftvalue) = S ge_signed_half_weighted_total_compareproductsentriesentryleftvaluedecode))) /\ ((dst_positive_weighted_total_compareproductsentriesentryleft) + ge_balance_negative_weighted_total_compareproductsentriesentryleftvalue = (dst_negative_weighted_total_compareproductsentriesentryleft) + ge_balance_positive_weighted_total_compareproductsentriesentryleftvalue))))))))) /\ (((exists dst_positive_code_weighted_total_compareproductsentriesentryright dst_positive_scale_weighted_total_compareproductsentriesentryright dst_negative_code_weighted_total_compareproductsentriesentryright dst_negative_scale_weighted_total_compareproductsentriesentryright dst_positive_weighted_total_compareproductsentriesentryright dst_negative_weighted_total_compareproductsentriesentryright. (((F) = (((((dst_positive_code_weighted_total_compareproductsentriesentryright) + (dst_positive_scale_weighted_total_compareproductsentriesentryright)) * S ((dst_positive_code_weighted_total_compareproductsentriesentryright) + (dst_positive_scale_weighted_total_compareproductsentriesentryright)) + ((dst_positive_scale_weighted_total_compareproductsentriesentryright) + (dst_positive_scale_weighted_total_compareproductsentriesentryright))) + (((dst_negative_code_weighted_total_compareproductsentriesentryright) + (dst_negative_scale_weighted_total_compareproductsentriesentryright)) * S ((dst_negative_code_weighted_total_compareproductsentriesentryright) + (dst_negative_scale_weighted_total_compareproductsentriesentryright)) + ((dst_negative_scale_weighted_total_compareproductsentriesentryright) + (dst_negative_scale_weighted_total_compareproductsentriesentryright)))) * S ((((dst_positive_code_weighted_total_compareproductsentriesentryright) + (dst_positive_scale_weighted_total_compareproductsentriesentryright)) * S ((dst_positive_code_weighted_total_compareproductsentriesentryright) + (dst_positive_scale_weighted_total_compareproductsentriesentryright)) + ((dst_positive_scale_weighted_total_compareproductsentriesentryright) + (dst_positive_scale_weighted_total_compareproductsentriesentryright))) + (((dst_negative_code_weighted_total_compareproductsentriesentryright) + (dst_negative_scale_weighted_total_compareproductsentriesentryright)) * S ((dst_negative_code_weighted_total_compareproductsentriesentryright) + (dst_negative_scale_weighted_total_compareproductsentriesentryright)) + ((dst_negative_scale_weighted_total_compareproductsentriesentryright) + (dst_negative_scale_weighted_total_compareproductsentriesentryright)))) + ((((dst_negative_code_weighted_total_compareproductsentriesentryright) + (dst_negative_scale_weighted_total_compareproductsentriesentryright)) * S ((dst_negative_code_weighted_total_compareproductsentriesentryright) + (dst_negative_scale_weighted_total_compareproductsentriesentryright)) + ((dst_negative_scale_weighted_total_compareproductsentriesentryright) + (dst_negative_scale_weighted_total_compareproductsentriesentryright))) + (((dst_negative_code_weighted_total_compareproductsentriesentryright) + (dst_negative_scale_weighted_total_compareproductsentriesentryright)) * S ((dst_negative_code_weighted_total_compareproductsentriesentryright) + (dst_negative_scale_weighted_total_compareproductsentriesentryright)) + ((dst_negative_scale_weighted_total_compareproductsentriesentryright) + (dst_negative_scale_weighted_total_compareproductsentriesentryright)))))) /\ (((((exists ff_h_pvs_weighted_total_compareproductsentriesentryrightpositive. ff_h_pvs_weighted_total_compareproductsentriesentryrightpositive + S (dst_positive_weighted_total_compareproductsentriesentryright) = S ((S (sto_index_weighted_total_compareproductsentries)) * dst_positive_scale_weighted_total_compareproductsentriesentryright)) /\ exists ff_q_pvs_weighted_total_compareproductsentriesentryrightpositive. dst_positive_code_weighted_total_compareproductsentriesentryright = ff_q_pvs_weighted_total_compareproductsentriesentryrightpositive * S ((S (sto_index_weighted_total_compareproductsentries)) * dst_positive_scale_weighted_total_compareproductsentriesentryright) + (dst_positive_weighted_total_compareproductsentriesentryright))) /\ (((((exists ff_h_pvs_weighted_total_compareproductsentriesentryrightnegative. ff_h_pvs_weighted_total_compareproductsentriesentryrightnegative + S (dst_negative_weighted_total_compareproductsentriesentryright) = S ((S (sto_index_weighted_total_compareproductsentries)) * dst_negative_scale_weighted_total_compareproductsentriesentryright)) /\ exists ff_q_pvs_weighted_total_compareproductsentriesentryrightnegative. dst_negative_code_weighted_total_compareproductsentriesentryright = ff_q_pvs_weighted_total_compareproductsentriesentryrightnegative * S ((S (sto_index_weighted_total_compareproductsentries)) * dst_negative_scale_weighted_total_compareproductsentriesentryright) + (dst_negative_weighted_total_compareproductsentriesentryright))) /\ (exists ge_balance_positive_weighted_total_compareproductsentriesentryrightvalue ge_balance_negative_weighted_total_compareproductsentriesentryrightvalue. (((((sto_right_weighted_total_compareproductsentries) = 2 * (ge_balance_positive_weighted_total_compareproductsentriesentryrightvalue) /\ (ge_balance_negative_weighted_total_compareproductsentriesentryrightvalue) = 0) \/ exists ge_signed_half_weighted_total_compareproductsentriesentryrightvaluedecode. (((sto_right_weighted_total_compareproductsentries) = 2 * ge_signed_half_weighted_total_compareproductsentriesentryrightvaluedecode + 1 /\ (ge_balance_positive_weighted_total_compareproductsentriesentryrightvalue) = 0) /\ (ge_balance_negative_weighted_total_compareproductsentriesentryrightvalue) = S ge_signed_half_weighted_total_compareproductsentriesentryrightvaluedecode))) /\ ((dst_positive_weighted_total_compareproductsentriesentryright) + ge_balance_negative_weighted_total_compareproductsentriesentryrightvalue = (dst_negative_weighted_total_compareproductsentriesentryright) + ge_balance_positive_weighted_total_compareproductsentriesentryrightvalue))))))))) /\ (((exists dst_positive_code_weighted_total_compareproductsentriesentryoutput dst_positive_scale_weighted_total_compareproductsentriesentryoutput dst_negative_code_weighted_total_compareproductsentriesentryoutput dst_negative_scale_weighted_total_compareproductsentriesentryoutput dst_positive_weighted_total_compareproductsentriesentryoutput dst_negative_weighted_total_compareproductsentriesentryoutput. (((sws_product_table_weighted_total_compare) = (((((dst_positive_code_weighted_total_compareproductsentriesentryoutput) + (dst_positive_scale_weighted_total_compareproductsentriesentryoutput)) * S ((dst_positive_code_weighted_total_compareproductsentriesentryoutput) + (dst_positive_scale_weighted_total_compareproductsentriesentryoutput)) + ((dst_positive_scale_weighted_total_compareproductsentriesentryoutput) + (dst_positive_scale_weighted_total_compareproductsentriesentryoutput))) + (((dst_negative_code_weighted_total_compareproductsentriesentryoutput) + (dst_negative_scale_weighted_total_compareproductsentriesentryoutput)) * S ((dst_negative_code_weighted_total_compareproductsentriesentryoutput) + (dst_negative_scale_weighted_total_compareproductsentriesentryoutput)) + ((dst_negative_scale_weighted_total_compareproductsentriesentryoutput) + (dst_negative_scale_weighted_total_compareproductsentriesentryoutput)))) * S ((((dst_positive_code_weighted_total_compareproductsentriesentryoutput) + (dst_positive_scale_weighted_total_compareproductsentriesentryoutput)) * S ((dst_positive_code_weighted_total_compareproductsentriesentryoutput) + (dst_positive_scale_weighted_total_compareproductsentriesentryoutput)) + ((dst_positive_scale_weighted_total_compareproductsentriesentryoutput) + (dst_positive_scale_weighted_total_compareproductsentriesentryoutput))) + (((dst_negative_code_weighted_total_compareproductsentriesentryoutput) + (dst_negative_scale_weighted_total_compareproductsentriesentryoutput)) * S ((dst_negative_code_weighted_total_compareproductsentriesentryoutput) + (dst_negative_scale_weighted_total_compareproductsentriesentryoutput)) + ((dst_negative_scale_weighted_total_compareproductsentriesentryoutput) + (dst_negative_scale_weighted_total_compareproductsentriesentryoutput)))) + ((((dst_negative_code_weighted_total_compareproductsentriesentryoutput) + (dst_negative_scale_weighted_total_compareproductsentriesentryoutput)) * S ((dst_negative_code_weighted_total_compareproductsentriesentryoutput) + (dst_negative_scale_weighted_total_compareproductsentriesentryoutput)) + ((dst_negative_scale_weighted_total_compareproductsentriesentryoutput) + (dst_negative_scale_weighted_total_compareproductsentriesentryoutput))) + (((dst_negative_code_weighted_total_compareproductsentriesentryoutput) + (dst_negative_scale_weighted_total_compareproductsentriesentryoutput)) * S ((dst_negative_code_weighted_total_compareproductsentriesentryoutput) + (dst_negative_scale_weighted_total_compareproductsentriesentryoutput)) + ((dst_negative_scale_weighted_total_compareproductsentriesentryoutput) + (dst_negative_scale_weighted_total_compareproductsentriesentryoutput)))))) /\ (((((exists ff_h_pvs_weighted_total_compareproductsentriesentryoutputpositive. ff_h_pvs_weighted_total_compareproductsentriesentryoutputpositive + S (dst_positive_weighted_total_compareproductsentriesentryoutput) = S ((S (sto_index_weighted_total_compareproductsentries)) * dst_positive_scale_weighted_total_compareproductsentriesentryoutput)) /\ exists ff_q_pvs_weighted_total_compareproductsentriesentryoutputpositive. dst_positive_code_weighted_total_compareproductsentriesentryoutput = ff_q_pvs_weighted_total_compareproductsentriesentryoutputpositive * S ((S (sto_index_weighted_total_compareproductsentries)) * dst_positive_scale_weighted_total_compareproductsentriesentryoutput) + (dst_positive_weighted_total_compareproductsentriesentryoutput))) /\ (((((exists ff_h_pvs_weighted_total_compareproductsentriesentryoutputnegative. ff_h_pvs_weighted_total_compareproductsentriesentryoutputnegative + S (dst_negative_weighted_total_compareproductsentriesentryoutput) = S ((S (sto_index_weighted_total_compareproductsentries)) * dst_negative_scale_weighted_total_compareproductsentriesentryoutput)) /\ exists ff_q_pvs_weighted_total_compareproductsentriesentryoutputnegative. dst_negative_code_weighted_total_compareproductsentriesentryoutput = ff_q_pvs_weighted_total_compareproductsentriesentryoutputnegative * S ((S (sto_index_weighted_total_compareproductsentries)) * dst_negative_scale_weighted_total_compareproductsentriesentryoutput) + (dst_negative_weighted_total_compareproductsentriesentryoutput))) /\ (exists ge_balance_positive_weighted_total_compareproductsentriesentryoutputvalue ge_balance_negative_weighted_total_compareproductsentriesentryoutputvalue. (((((sto_output_weighted_total_compareproductsentries) = 2 * (ge_balance_positive_weighted_total_compareproductsentriesentryoutputvalue) /\ (ge_balance_negative_weighted_total_compareproductsentriesentryoutputvalue) = 0) \/ exists ge_signed_half_weighted_total_compareproductsentriesentryoutputvaluedecode. (((sto_output_weighted_total_compareproductsentries) = 2 * ge_signed_half_weighted_total_compareproductsentriesentryoutputvaluedecode + 1 /\ (ge_balance_positive_weighted_total_compareproductsentriesentryoutputvalue) = 0) /\ (ge_balance_negative_weighted_total_compareproductsentriesentryoutputvalue) = S ge_signed_half_weighted_total_compareproductsentriesentryoutputvaluedecode))) /\ ((dst_positive_weighted_total_compareproductsentriesentryoutput) + ge_balance_negative_weighted_total_compareproductsentriesentryoutputvalue = (dst_negative_weighted_total_compareproductsentriesentryoutput) + ge_balance_positive_weighted_total_compareproductsentriesentryoutputvalue))))))))) /\ (exists sto_ap_weighted_total_compareproductsentriesentryoperation sto_an_weighted_total_compareproductsentriesentryoperation sto_bp_weighted_total_compareproductsentriesentryoperation sto_bn_weighted_total_compareproductsentriesentryoperation sto_cp_weighted_total_compareproductsentriesentryoperation sto_cn_weighted_total_compareproductsentriesentryoperation. (((((sto_left_weighted_total_compareproductsentries) = 2 * (sto_ap_weighted_total_compareproductsentriesentryoperation) /\ (sto_an_weighted_total_compareproductsentriesentryoperation) = 0) \/ exists ge_signed_half_weighted_total_compareproductsentriesentryoperationleft. (((sto_left_weighted_total_compareproductsentries) = 2 * ge_signed_half_weighted_total_compareproductsentriesentryoperationleft + 1 /\ (sto_ap_weighted_total_compareproductsentriesentryoperation) = 0) /\ (sto_an_weighted_total_compareproductsentriesentryoperation) = S ge_signed_half_weighted_total_compareproductsentriesentryoperationleft))) /\ ((((((sto_right_weighted_total_compareproductsentries) = 2 * (sto_bp_weighted_total_compareproductsentriesentryoperation) /\ (sto_bn_weighted_total_compareproductsentriesentryoperation) = 0) \/ exists ge_signed_half_weighted_total_compareproductsentriesentryoperationright. (((sto_right_weighted_total_compareproductsentries) = 2 * ge_signed_half_weighted_total_compareproductsentriesentryoperationright + 1 /\ (sto_bp_weighted_total_compareproductsentriesentryoperation) = 0) /\ (sto_bn_weighted_total_compareproductsentriesentryoperation) = S ge_signed_half_weighted_total_compareproductsentriesentryoperationright))) /\ ((((((sto_output_weighted_total_compareproductsentries) = 2 * (sto_cp_weighted_total_compareproductsentriesentryoperation) /\ (sto_cn_weighted_total_compareproductsentriesentryoperation) = 0) \/ exists ge_signed_half_weighted_total_compareproductsentriesentryoperationoutput. (((sto_output_weighted_total_compareproductsentries) = 2 * ge_signed_half_weighted_total_compareproductsentriesentryoperationoutput + 1 /\ (sto_cp_weighted_total_compareproductsentriesentryoperation) = 0) /\ (sto_cn_weighted_total_compareproductsentriesentryoperation) = S ge_signed_half_weighted_total_compareproductsentriesentryoperationoutput))) /\ ((sto_ap_weighted_total_compareproductsentriesentryoperation * sto_bp_weighted_total_compareproductsentriesentryoperation + sto_an_weighted_total_compareproductsentriesentryoperation * sto_bn_weighted_total_compareproductsentriesentryoperation) + sto_cn_weighted_total_compareproductsentriesentryoperation = (sto_ap_weighted_total_compareproductsentriesentryoperation * sto_bn_weighted_total_compareproductsentriesentryoperation + sto_an_weighted_total_compareproductsentriesentryoperation * sto_bp_weighted_total_compareproductsentriesentryoperation) + sto_cp_weighted_total_compareproductsentriesentryoperation))))))))))))))))))) /\ (exists dst_positive_code_weighted_total_comparesum dst_positive_scale_weighted_total_comparesum dst_negative_code_weighted_total_comparesum dst_negative_scale_weighted_total_comparesum dst_positive_sum_weighted_total_comparesum dst_negative_sum_weighted_total_comparesum. (((sws_product_table_weighted_total_compare) = (((((dst_positive_code_weighted_total_comparesum) + (dst_positive_scale_weighted_total_comparesum)) * S ((dst_positive_code_weighted_total_comparesum) + (dst_positive_scale_weighted_total_comparesum)) + ((dst_positive_scale_weighted_total_comparesum) + (dst_positive_scale_weighted_total_comparesum))) + (((dst_negative_code_weighted_total_comparesum) + (dst_negative_scale_weighted_total_comparesum)) * S ((dst_negative_code_weighted_total_comparesum) + (dst_negative_scale_weighted_total_comparesum)) + ((dst_negative_scale_weighted_total_comparesum) + (dst_negative_scale_weighted_total_comparesum)))) * S ((((dst_positive_code_weighted_total_comparesum) + (dst_positive_scale_weighted_total_comparesum)) * S ((dst_positive_code_weighted_total_comparesum) + (dst_positive_scale_weighted_total_comparesum)) + ((dst_positive_scale_weighted_total_comparesum) + (dst_positive_scale_weighted_total_comparesum))) + (((dst_negative_code_weighted_total_comparesum) + (dst_negative_scale_weighted_total_comparesum)) * S ((dst_negative_code_weighted_total_comparesum) + (dst_negative_scale_weighted_total_comparesum)) + ((dst_negative_scale_weighted_total_comparesum) + (dst_negative_scale_weighted_total_comparesum)))) + ((((dst_negative_code_weighted_total_comparesum) + (dst_negative_scale_weighted_total_comparesum)) * S ((dst_negative_code_weighted_total_comparesum) + (dst_negative_scale_weighted_total_comparesum)) + ((dst_negative_scale_weighted_total_comparesum) + (dst_negative_scale_weighted_total_comparesum))) + (((dst_negative_code_weighted_total_comparesum) + (dst_negative_scale_weighted_total_comparesum)) * S ((dst_negative_code_weighted_total_comparesum) + (dst_negative_scale_weighted_total_comparesum)) + ((dst_negative_scale_weighted_total_comparesum) + (dst_negative_scale_weighted_total_comparesum)))))) /\ (((exists fs_u_dst_weighted_total_comparesumpositive fs_v_dst_weighted_total_comparesumpositive. ((((exists fs_h_dst_weighted_total_comparesumpositive_body_start. fs_h_dst_weighted_total_comparesumpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_weighted_total_comparesumpositive)) /\ exists fs_q_dst_weighted_total_comparesumpositive_body_start. fs_u_dst_weighted_total_comparesumpositive = fs_q_dst_weighted_total_comparesumpositive_body_start * S ((S (0)) * fs_v_dst_weighted_total_comparesumpositive) + (0))) /\ ((((exists fs_h_dst_weighted_total_comparesumpositive_body_terminal. fs_h_dst_weighted_total_comparesumpositive_body_terminal + S (dst_positive_sum_weighted_total_comparesum) = S ((S (l)) * fs_v_dst_weighted_total_comparesumpositive)) /\ exists fs_q_dst_weighted_total_comparesumpositive_body_terminal. fs_u_dst_weighted_total_comparesumpositive = fs_q_dst_weighted_total_comparesumpositive_body_terminal * S ((S (l)) * fs_v_dst_weighted_total_comparesumpositive) + (dst_positive_sum_weighted_total_comparesum))) /\ forall fs_i_dst_weighted_total_comparesumpositive_body_steps. (exists fs_lt_dst_weighted_total_comparesumpositive_body_steps_bound. fs_lt_dst_weighted_total_comparesumpositive_body_steps_bound + S fs_i_dst_weighted_total_comparesumpositive_body_steps = l) -> exists fs_a_dst_weighted_total_comparesumpositive_body_steps fs_r_dst_weighted_total_comparesumpositive_body_steps fs_s_dst_weighted_total_comparesumpositive_body_steps. ((((exists fs_h_dst_weighted_total_comparesumpositive_body_steps_summand. fs_h_dst_weighted_total_comparesumpositive_body_steps_summand + S (fs_a_dst_weighted_total_comparesumpositive_body_steps) = S ((S (fs_i_dst_weighted_total_comparesumpositive_body_steps)) * dst_positive_scale_weighted_total_comparesum)) /\ exists fs_q_dst_weighted_total_comparesumpositive_body_steps_summand. dst_positive_code_weighted_total_comparesum = fs_q_dst_weighted_total_comparesumpositive_body_steps_summand * S ((S (fs_i_dst_weighted_total_comparesumpositive_body_steps)) * dst_positive_scale_weighted_total_comparesum) + (fs_a_dst_weighted_total_comparesumpositive_body_steps))) /\ ((((exists fs_h_dst_weighted_total_comparesumpositive_body_steps_partial. fs_h_dst_weighted_total_comparesumpositive_body_steps_partial + S (fs_r_dst_weighted_total_comparesumpositive_body_steps) = S ((S (fs_i_dst_weighted_total_comparesumpositive_body_steps)) * fs_v_dst_weighted_total_comparesumpositive)) /\ exists fs_q_dst_weighted_total_comparesumpositive_body_steps_partial. fs_u_dst_weighted_total_comparesumpositive = fs_q_dst_weighted_total_comparesumpositive_body_steps_partial * S ((S (fs_i_dst_weighted_total_comparesumpositive_body_steps)) * fs_v_dst_weighted_total_comparesumpositive) + (fs_r_dst_weighted_total_comparesumpositive_body_steps))) /\ ((((exists fs_h_dst_weighted_total_comparesumpositive_body_steps_successor. fs_h_dst_weighted_total_comparesumpositive_body_steps_successor + S (fs_s_dst_weighted_total_comparesumpositive_body_steps) = S ((S (S fs_i_dst_weighted_total_comparesumpositive_body_steps)) * fs_v_dst_weighted_total_comparesumpositive)) /\ exists fs_q_dst_weighted_total_comparesumpositive_body_steps_successor. fs_u_dst_weighted_total_comparesumpositive = fs_q_dst_weighted_total_comparesumpositive_body_steps_successor * S ((S (S fs_i_dst_weighted_total_comparesumpositive_body_steps)) * fs_v_dst_weighted_total_comparesumpositive) + (fs_s_dst_weighted_total_comparesumpositive_body_steps))) /\ fs_s_dst_weighted_total_comparesumpositive_body_steps = fs_r_dst_weighted_total_comparesumpositive_body_steps + fs_a_dst_weighted_total_comparesumpositive_body_steps)))))) /\ (((exists fs_u_dst_weighted_total_comparesumnegative fs_v_dst_weighted_total_comparesumnegative. ((((exists fs_h_dst_weighted_total_comparesumnegative_body_start. fs_h_dst_weighted_total_comparesumnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_weighted_total_comparesumnegative)) /\ exists fs_q_dst_weighted_total_comparesumnegative_body_start. fs_u_dst_weighted_total_comparesumnegative = fs_q_dst_weighted_total_comparesumnegative_body_start * S ((S (0)) * fs_v_dst_weighted_total_comparesumnegative) + (0))) /\ ((((exists fs_h_dst_weighted_total_comparesumnegative_body_terminal. fs_h_dst_weighted_total_comparesumnegative_body_terminal + S (dst_negative_sum_weighted_total_comparesum) = S ((S (l)) * fs_v_dst_weighted_total_comparesumnegative)) /\ exists fs_q_dst_weighted_total_comparesumnegative_body_terminal. fs_u_dst_weighted_total_comparesumnegative = fs_q_dst_weighted_total_comparesumnegative_body_terminal * S ((S (l)) * fs_v_dst_weighted_total_comparesumnegative) + (dst_negative_sum_weighted_total_comparesum))) /\ forall fs_i_dst_weighted_total_comparesumnegative_body_steps. (exists fs_lt_dst_weighted_total_comparesumnegative_body_steps_bound. fs_lt_dst_weighted_total_comparesumnegative_body_steps_bound + S fs_i_dst_weighted_total_comparesumnegative_body_steps = l) -> exists fs_a_dst_weighted_total_comparesumnegative_body_steps fs_r_dst_weighted_total_comparesumnegative_body_steps fs_s_dst_weighted_total_comparesumnegative_body_steps. ((((exists fs_h_dst_weighted_total_comparesumnegative_body_steps_summand. fs_h_dst_weighted_total_comparesumnegative_body_steps_summand + S (fs_a_dst_weighted_total_comparesumnegative_body_steps) = S ((S (fs_i_dst_weighted_total_comparesumnegative_body_steps)) * dst_negative_scale_weighted_total_comparesum)) /\ exists fs_q_dst_weighted_total_comparesumnegative_body_steps_summand. dst_negative_code_weighted_total_comparesum = fs_q_dst_weighted_total_comparesumnegative_body_steps_summand * S ((S (fs_i_dst_weighted_total_comparesumnegative_body_steps)) * dst_negative_scale_weighted_total_comparesum) + (fs_a_dst_weighted_total_comparesumnegative_body_steps))) /\ ((((exists fs_h_dst_weighted_total_comparesumnegative_body_steps_partial. fs_h_dst_weighted_total_comparesumnegative_body_steps_partial + S (fs_r_dst_weighted_total_comparesumnegative_body_steps) = S ((S (fs_i_dst_weighted_total_comparesumnegative_body_steps)) * fs_v_dst_weighted_total_comparesumnegative)) /\ exists fs_q_dst_weighted_total_comparesumnegative_body_steps_partial. fs_u_dst_weighted_total_comparesumnegative = fs_q_dst_weighted_total_comparesumnegative_body_steps_partial * S ((S (fs_i_dst_weighted_total_comparesumnegative_body_steps)) * fs_v_dst_weighted_total_comparesumnegative) + (fs_r_dst_weighted_total_comparesumnegative_body_steps))) /\ ((((exists fs_h_dst_weighted_total_comparesumnegative_body_steps_successor. fs_h_dst_weighted_total_comparesumnegative_body_steps_successor + S (fs_s_dst_weighted_total_comparesumnegative_body_steps) = S ((S (S fs_i_dst_weighted_total_comparesumnegative_body_steps)) * fs_v_dst_weighted_total_comparesumnegative)) /\ exists fs_q_dst_weighted_total_comparesumnegative_body_steps_successor. fs_u_dst_weighted_total_comparesumnegative = fs_q_dst_weighted_total_comparesumnegative_body_steps_successor * S ((S (S fs_i_dst_weighted_total_comparesumnegative_body_steps)) * fs_v_dst_weighted_total_comparesumnegative) + (fs_s_dst_weighted_total_comparesumnegative_body_steps))) /\ fs_s_dst_weighted_total_comparesumnegative_body_steps = fs_r_dst_weighted_total_comparesumnegative_body_steps + fs_a_dst_weighted_total_comparesumnegative_body_steps)))))) /\ (exists ge_balance_positive_weighted_total_comparesumresult ge_balance_negative_weighted_total_comparesumresult. (((((u) = 2 * (ge_balance_positive_weighted_total_comparesumresult) /\ (ge_balance_negative_weighted_total_comparesumresult) = 0) \/ exists ge_signed_half_weighted_total_comparesumresultdecode. (((u) = 2 * ge_signed_half_weighted_total_comparesumresultdecode + 1 /\ (ge_balance_positive_weighted_total_comparesumresult) = 0) /\ (ge_balance_negative_weighted_total_comparesumresult) = S ge_signed_half_weighted_total_comparesumresultdecode))) /\ ((dst_positive_sum_weighted_total_comparesum) + ge_balance_negative_weighted_total_comparesumresult = (dst_negative_sum_weighted_total_comparesum) + ge_balance_positive_weighted_total_comparesumresult))))))))))) -> u = z))