signed_weighted_sum_exists

Exact expanded first-order arithmetic statement

forall l W F. (exists dst_positive_code_weighted_exists_weights dst_positive_scale_weighted_exists_weights dst_negative_code_weighted_exists_weights dst_negative_scale_weighted_exists_weights. (((W) = (((((dst_positive_code_weighted_exists_weights) + (dst_positive_scale_weighted_exists_weights)) * S ((dst_positive_code_weighted_exists_weights) + (dst_positive_scale_weighted_exists_weights)) + ((dst_positive_scale_weighted_exists_weights) + (dst_positive_scale_weighted_exists_weights))) + (((dst_negative_code_weighted_exists_weights) + (dst_negative_scale_weighted_exists_weights)) * S ((dst_negative_code_weighted_exists_weights) + (dst_negative_scale_weighted_exists_weights)) + ((dst_negative_scale_weighted_exists_weights) + (dst_negative_scale_weighted_exists_weights)))) * S ((((dst_positive_code_weighted_exists_weights) + (dst_positive_scale_weighted_exists_weights)) * S ((dst_positive_code_weighted_exists_weights) + (dst_positive_scale_weighted_exists_weights)) + ((dst_positive_scale_weighted_exists_weights) + (dst_positive_scale_weighted_exists_weights))) + (((dst_negative_code_weighted_exists_weights) + (dst_negative_scale_weighted_exists_weights)) * S ((dst_negative_code_weighted_exists_weights) + (dst_negative_scale_weighted_exists_weights)) + ((dst_negative_scale_weighted_exists_weights) + (dst_negative_scale_weighted_exists_weights)))) + ((((dst_negative_code_weighted_exists_weights) + (dst_negative_scale_weighted_exists_weights)) * S ((dst_negative_code_weighted_exists_weights) + (dst_negative_scale_weighted_exists_weights)) + ((dst_negative_scale_weighted_exists_weights) + (dst_negative_scale_weighted_exists_weights))) + (((dst_negative_code_weighted_exists_weights) + (dst_negative_scale_weighted_exists_weights)) * S ((dst_negative_code_weighted_exists_weights) + (dst_negative_scale_weighted_exists_weights)) + ((dst_negative_scale_weighted_exists_weights) + (dst_negative_scale_weighted_exists_weights)))))) /\ (forall dst_index_weighted_exists_weights. (exists pvs_le_gap_weighted_exists_weightsdomain. pvs_le_gap_weighted_exists_weightsdomain + (dst_index_weighted_exists_weights) = (l)) -> exists dst_positive_weighted_exists_weights dst_negative_weighted_exists_weights dst_value_weighted_exists_weights. ((((exists ff_h_pvs_weighted_exists_weightsentrypositive. ff_h_pvs_weighted_exists_weightsentrypositive + S (dst_positive_weighted_exists_weights) = S ((S (dst_index_weighted_exists_weights)) * dst_positive_scale_weighted_exists_weights)) /\ exists ff_q_pvs_weighted_exists_weightsentrypositive. dst_positive_code_weighted_exists_weights = ff_q_pvs_weighted_exists_weightsentrypositive * S ((S (dst_index_weighted_exists_weights)) * dst_positive_scale_weighted_exists_weights) + (dst_positive_weighted_exists_weights))) /\ (((((exists ff_h_pvs_weighted_exists_weightsentrynegative. ff_h_pvs_weighted_exists_weightsentrynegative + S (dst_negative_weighted_exists_weights) = S ((S (dst_index_weighted_exists_weights)) * dst_negative_scale_weighted_exists_weights)) /\ exists ff_q_pvs_weighted_exists_weightsentrynegative. dst_negative_code_weighted_exists_weights = ff_q_pvs_weighted_exists_weightsentrynegative * S ((S (dst_index_weighted_exists_weights)) * dst_negative_scale_weighted_exists_weights) + (dst_negative_weighted_exists_weights))) /\ (exists ge_balance_positive_weighted_exists_weightsentryvalue ge_balance_negative_weighted_exists_weightsentryvalue. (((((dst_value_weighted_exists_weights) = 2 * (ge_balance_positive_weighted_exists_weightsentryvalue) /\ (ge_balance_negative_weighted_exists_weightsentryvalue) = 0) \/ exists ge_signed_half_weighted_exists_weightsentryvaluedecode. (((dst_value_weighted_exists_weights) = 2 * ge_signed_half_weighted_exists_weightsentryvaluedecode + 1 /\ (ge_balance_positive_weighted_exists_weightsentryvalue) = 0) /\ (ge_balance_negative_weighted_exists_weightsentryvalue) = S ge_signed_half_weighted_exists_weightsentryvaluedecode))) /\ ((dst_positive_weighted_exists_weights) + ge_balance_negative_weighted_exists_weightsentryvalue = (dst_negative_weighted_exists_weights) + ge_balance_positive_weighted_exists_weightsentryvalue))))))))) -> (exists dst_positive_code_weighted_exists_values dst_positive_scale_weighted_exists_values dst_negative_code_weighted_exists_values dst_negative_scale_weighted_exists_values. (((F) = (((((dst_positive_code_weighted_exists_values) + (dst_positive_scale_weighted_exists_values)) * S ((dst_positive_code_weighted_exists_values) + (dst_positive_scale_weighted_exists_values)) + ((dst_positive_scale_weighted_exists_values) + (dst_positive_scale_weighted_exists_values))) + (((dst_negative_code_weighted_exists_values) + (dst_negative_scale_weighted_exists_values)) * S ((dst_negative_code_weighted_exists_values) + (dst_negative_scale_weighted_exists_values)) + ((dst_negative_scale_weighted_exists_values) + (dst_negative_scale_weighted_exists_values)))) * S ((((dst_positive_code_weighted_exists_values) + (dst_positive_scale_weighted_exists_values)) * S ((dst_positive_code_weighted_exists_values) + (dst_positive_scale_weighted_exists_values)) + ((dst_positive_scale_weighted_exists_values) + (dst_positive_scale_weighted_exists_values))) + (((dst_negative_code_weighted_exists_values) + (dst_negative_scale_weighted_exists_values)) * S ((dst_negative_code_weighted_exists_values) + (dst_negative_scale_weighted_exists_values)) + ((dst_negative_scale_weighted_exists_values) + (dst_negative_scale_weighted_exists_values)))) + ((((dst_negative_code_weighted_exists_values) + (dst_negative_scale_weighted_exists_values)) * S ((dst_negative_code_weighted_exists_values) + (dst_negative_scale_weighted_exists_values)) + ((dst_negative_scale_weighted_exists_values) + (dst_negative_scale_weighted_exists_values))) + (((dst_negative_code_weighted_exists_values) + (dst_negative_scale_weighted_exists_values)) * S ((dst_negative_code_weighted_exists_values) + (dst_negative_scale_weighted_exists_values)) + ((dst_negative_scale_weighted_exists_values) + (dst_negative_scale_weighted_exists_values)))))) /\ (forall dst_index_weighted_exists_values. (exists pvs_le_gap_weighted_exists_valuesdomain. pvs_le_gap_weighted_exists_valuesdomain + (dst_index_weighted_exists_values) = (l)) -> exists dst_positive_weighted_exists_values dst_negative_weighted_exists_values dst_value_weighted_exists_values. ((((exists ff_h_pvs_weighted_exists_valuesentrypositive. ff_h_pvs_weighted_exists_valuesentrypositive + S (dst_positive_weighted_exists_values) = S ((S (dst_index_weighted_exists_values)) * dst_positive_scale_weighted_exists_values)) /\ exists ff_q_pvs_weighted_exists_valuesentrypositive. dst_positive_code_weighted_exists_values = ff_q_pvs_weighted_exists_valuesentrypositive * S ((S (dst_index_weighted_exists_values)) * dst_positive_scale_weighted_exists_values) + (dst_positive_weighted_exists_values))) /\ (((((exists ff_h_pvs_weighted_exists_valuesentrynegative. ff_h_pvs_weighted_exists_valuesentrynegative + S (dst_negative_weighted_exists_values) = S ((S (dst_index_weighted_exists_values)) * dst_negative_scale_weighted_exists_values)) /\ exists ff_q_pvs_weighted_exists_valuesentrynegative. dst_negative_code_weighted_exists_values = ff_q_pvs_weighted_exists_valuesentrynegative * S ((S (dst_index_weighted_exists_values)) * dst_negative_scale_weighted_exists_values) + (dst_negative_weighted_exists_values))) /\ (exists ge_balance_positive_weighted_exists_valuesentryvalue ge_balance_negative_weighted_exists_valuesentryvalue. (((((dst_value_weighted_exists_values) = 2 * (ge_balance_positive_weighted_exists_valuesentryvalue) /\ (ge_balance_negative_weighted_exists_valuesentryvalue) = 0) \/ exists ge_signed_half_weighted_exists_valuesentryvaluedecode. (((dst_value_weighted_exists_values) = 2 * ge_signed_half_weighted_exists_valuesentryvaluedecode + 1 /\ (ge_balance_positive_weighted_exists_valuesentryvalue) = 0) /\ (ge_balance_negative_weighted_exists_valuesentryvalue) = S ge_signed_half_weighted_exists_valuesentryvaluedecode))) /\ ((dst_positive_weighted_exists_values) + ge_balance_negative_weighted_exists_valuesentryvalue = (dst_negative_weighted_exists_values) + ge_balance_positive_weighted_exists_valuesentryvalue))))))))) -> exists z. (exists sws_product_table_weighted_exists_result. ((((exists dst_positive_code_weighted_exists_resultproductsleft_table dst_positive_scale_weighted_exists_resultproductsleft_table dst_negative_code_weighted_exists_resultproductsleft_table dst_negative_scale_weighted_exists_resultproductsleft_table. (((W) = (((((dst_positive_code_weighted_exists_resultproductsleft_table) + (dst_positive_scale_weighted_exists_resultproductsleft_table)) * S ((dst_positive_code_weighted_exists_resultproductsleft_table) + (dst_positive_scale_weighted_exists_resultproductsleft_table)) + ((dst_positive_scale_weighted_exists_resultproductsleft_table) + (dst_positive_scale_weighted_exists_resultproductsleft_table))) + (((dst_negative_code_weighted_exists_resultproductsleft_table) + (dst_negative_scale_weighted_exists_resultproductsleft_table)) * S ((dst_negative_code_weighted_exists_resultproductsleft_table) + (dst_negative_scale_weighted_exists_resultproductsleft_table)) + ((dst_negative_scale_weighted_exists_resultproductsleft_table) + (dst_negative_scale_weighted_exists_resultproductsleft_table)))) * S ((((dst_positive_code_weighted_exists_resultproductsleft_table) + (dst_positive_scale_weighted_exists_resultproductsleft_table)) * S ((dst_positive_code_weighted_exists_resultproductsleft_table) + (dst_positive_scale_weighted_exists_resultproductsleft_table)) + ((dst_positive_scale_weighted_exists_resultproductsleft_table) + (dst_positive_scale_weighted_exists_resultproductsleft_table))) + (((dst_negative_code_weighted_exists_resultproductsleft_table) + (dst_negative_scale_weighted_exists_resultproductsleft_table)) * S ((dst_negative_code_weighted_exists_resultproductsleft_table) + (dst_negative_scale_weighted_exists_resultproductsleft_table)) + ((dst_negative_scale_weighted_exists_resultproductsleft_table) + (dst_negative_scale_weighted_exists_resultproductsleft_table)))) + ((((dst_negative_code_weighted_exists_resultproductsleft_table) + (dst_negative_scale_weighted_exists_resultproductsleft_table)) * S ((dst_negative_code_weighted_exists_resultproductsleft_table) + (dst_negative_scale_weighted_exists_resultproductsleft_table)) + ((dst_negative_scale_weighted_exists_resultproductsleft_table) + (dst_negative_scale_weighted_exists_resultproductsleft_table))) + (((dst_negative_code_weighted_exists_resultproductsleft_table) + (dst_negative_scale_weighted_exists_resultproductsleft_table)) * S ((dst_negative_code_weighted_exists_resultproductsleft_table) + (dst_negative_scale_weighted_exists_resultproductsleft_table)) + ((dst_negative_scale_weighted_exists_resultproductsleft_table) + (dst_negative_scale_weighted_exists_resultproductsleft_table)))))) /\ (forall dst_index_weighted_exists_resultproductsleft_table. (exists pvs_le_gap_weighted_exists_resultproductsleft_tabledomain. pvs_le_gap_weighted_exists_resultproductsleft_tabledomain + (dst_index_weighted_exists_resultproductsleft_table) = (l)) -> exists dst_positive_weighted_exists_resultproductsleft_table dst_negative_weighted_exists_resultproductsleft_table dst_value_weighted_exists_resultproductsleft_table. ((((exists ff_h_pvs_weighted_exists_resultproductsleft_tableentrypositive. ff_h_pvs_weighted_exists_resultproductsleft_tableentrypositive + S (dst_positive_weighted_exists_resultproductsleft_table) = S ((S (dst_index_weighted_exists_resultproductsleft_table)) * dst_positive_scale_weighted_exists_resultproductsleft_table)) /\ exists ff_q_pvs_weighted_exists_resultproductsleft_tableentrypositive. dst_positive_code_weighted_exists_resultproductsleft_table = ff_q_pvs_weighted_exists_resultproductsleft_tableentrypositive * S ((S (dst_index_weighted_exists_resultproductsleft_table)) * dst_positive_scale_weighted_exists_resultproductsleft_table) + (dst_positive_weighted_exists_resultproductsleft_table))) /\ (((((exists ff_h_pvs_weighted_exists_resultproductsleft_tableentrynegative. ff_h_pvs_weighted_exists_resultproductsleft_tableentrynegative + S (dst_negative_weighted_exists_resultproductsleft_table) = S ((S (dst_index_weighted_exists_resultproductsleft_table)) * dst_negative_scale_weighted_exists_resultproductsleft_table)) /\ exists ff_q_pvs_weighted_exists_resultproductsleft_tableentrynegative. dst_negative_code_weighted_exists_resultproductsleft_table = ff_q_pvs_weighted_exists_resultproductsleft_tableentrynegative * S ((S (dst_index_weighted_exists_resultproductsleft_table)) * dst_negative_scale_weighted_exists_resultproductsleft_table) + (dst_negative_weighted_exists_resultproductsleft_table))) /\ (exists ge_balance_positive_weighted_exists_resultproductsleft_tableentryvalue ge_balance_negative_weighted_exists_resultproductsleft_tableentryvalue. (((((dst_value_weighted_exists_resultproductsleft_table) = 2 * (ge_balance_positive_weighted_exists_resultproductsleft_tableentryvalue) /\ (ge_balance_negative_weighted_exists_resultproductsleft_tableentryvalue) = 0) \/ exists ge_signed_half_weighted_exists_resultproductsleft_tableentryvaluedecode. (((dst_value_weighted_exists_resultproductsleft_table) = 2 * ge_signed_half_weighted_exists_resultproductsleft_tableentryvaluedecode + 1 /\ (ge_balance_positive_weighted_exists_resultproductsleft_tableentryvalue) = 0) /\ (ge_balance_negative_weighted_exists_resultproductsleft_tableentryvalue) = S ge_signed_half_weighted_exists_resultproductsleft_tableentryvaluedecode))) /\ ((dst_positive_weighted_exists_resultproductsleft_table) + ge_balance_negative_weighted_exists_resultproductsleft_tableentryvalue = (dst_negative_weighted_exists_resultproductsleft_table) + ge_balance_positive_weighted_exists_resultproductsleft_tableentryvalue))))))))) /\ (((exists dst_positive_code_weighted_exists_resultproductsright_table dst_positive_scale_weighted_exists_resultproductsright_table dst_negative_code_weighted_exists_resultproductsright_table dst_negative_scale_weighted_exists_resultproductsright_table. (((F) = (((((dst_positive_code_weighted_exists_resultproductsright_table) + (dst_positive_scale_weighted_exists_resultproductsright_table)) * S ((dst_positive_code_weighted_exists_resultproductsright_table) + (dst_positive_scale_weighted_exists_resultproductsright_table)) + ((dst_positive_scale_weighted_exists_resultproductsright_table) + (dst_positive_scale_weighted_exists_resultproductsright_table))) + (((dst_negative_code_weighted_exists_resultproductsright_table) + (dst_negative_scale_weighted_exists_resultproductsright_table)) * S ((dst_negative_code_weighted_exists_resultproductsright_table) + (dst_negative_scale_weighted_exists_resultproductsright_table)) + ((dst_negative_scale_weighted_exists_resultproductsright_table) + (dst_negative_scale_weighted_exists_resultproductsright_table)))) * S ((((dst_positive_code_weighted_exists_resultproductsright_table) + (dst_positive_scale_weighted_exists_resultproductsright_table)) * S ((dst_positive_code_weighted_exists_resultproductsright_table) + (dst_positive_scale_weighted_exists_resultproductsright_table)) + ((dst_positive_scale_weighted_exists_resultproductsright_table) + (dst_positive_scale_weighted_exists_resultproductsright_table))) + (((dst_negative_code_weighted_exists_resultproductsright_table) + (dst_negative_scale_weighted_exists_resultproductsright_table)) * S ((dst_negative_code_weighted_exists_resultproductsright_table) + (dst_negative_scale_weighted_exists_resultproductsright_table)) + ((dst_negative_scale_weighted_exists_resultproductsright_table) + (dst_negative_scale_weighted_exists_resultproductsright_table)))) + ((((dst_negative_code_weighted_exists_resultproductsright_table) + (dst_negative_scale_weighted_exists_resultproductsright_table)) * S ((dst_negative_code_weighted_exists_resultproductsright_table) + (dst_negative_scale_weighted_exists_resultproductsright_table)) + ((dst_negative_scale_weighted_exists_resultproductsright_table) + (dst_negative_scale_weighted_exists_resultproductsright_table))) + (((dst_negative_code_weighted_exists_resultproductsright_table) + (dst_negative_scale_weighted_exists_resultproductsright_table)) * S ((dst_negative_code_weighted_exists_resultproductsright_table) + (dst_negative_scale_weighted_exists_resultproductsright_table)) + ((dst_negative_scale_weighted_exists_resultproductsright_table) + (dst_negative_scale_weighted_exists_resultproductsright_table)))))) /\ (forall dst_index_weighted_exists_resultproductsright_table. (exists pvs_le_gap_weighted_exists_resultproductsright_tabledomain. pvs_le_gap_weighted_exists_resultproductsright_tabledomain + (dst_index_weighted_exists_resultproductsright_table) = (l)) -> exists dst_positive_weighted_exists_resultproductsright_table dst_negative_weighted_exists_resultproductsright_table dst_value_weighted_exists_resultproductsright_table. ((((exists ff_h_pvs_weighted_exists_resultproductsright_tableentrypositive. ff_h_pvs_weighted_exists_resultproductsright_tableentrypositive + S (dst_positive_weighted_exists_resultproductsright_table) = S ((S (dst_index_weighted_exists_resultproductsright_table)) * dst_positive_scale_weighted_exists_resultproductsright_table)) /\ exists ff_q_pvs_weighted_exists_resultproductsright_tableentrypositive. dst_positive_code_weighted_exists_resultproductsright_table = ff_q_pvs_weighted_exists_resultproductsright_tableentrypositive * S ((S (dst_index_weighted_exists_resultproductsright_table)) * dst_positive_scale_weighted_exists_resultproductsright_table) + (dst_positive_weighted_exists_resultproductsright_table))) /\ (((((exists ff_h_pvs_weighted_exists_resultproductsright_tableentrynegative. ff_h_pvs_weighted_exists_resultproductsright_tableentrynegative + S (dst_negative_weighted_exists_resultproductsright_table) = S ((S (dst_index_weighted_exists_resultproductsright_table)) * dst_negative_scale_weighted_exists_resultproductsright_table)) /\ exists ff_q_pvs_weighted_exists_resultproductsright_tableentrynegative. dst_negative_code_weighted_exists_resultproductsright_table = ff_q_pvs_weighted_exists_resultproductsright_tableentrynegative * S ((S (dst_index_weighted_exists_resultproductsright_table)) * dst_negative_scale_weighted_exists_resultproductsright_table) + (dst_negative_weighted_exists_resultproductsright_table))) /\ (exists ge_balance_positive_weighted_exists_resultproductsright_tableentryvalue ge_balance_negative_weighted_exists_resultproductsright_tableentryvalue. (((((dst_value_weighted_exists_resultproductsright_table) = 2 * (ge_balance_positive_weighted_exists_resultproductsright_tableentryvalue) /\ (ge_balance_negative_weighted_exists_resultproductsright_tableentryvalue) = 0) \/ exists ge_signed_half_weighted_exists_resultproductsright_tableentryvaluedecode. (((dst_value_weighted_exists_resultproductsright_table) = 2 * ge_signed_half_weighted_exists_resultproductsright_tableentryvaluedecode + 1 /\ (ge_balance_positive_weighted_exists_resultproductsright_tableentryvalue) = 0) /\ (ge_balance_negative_weighted_exists_resultproductsright_tableentryvalue) = S ge_signed_half_weighted_exists_resultproductsright_tableentryvaluedecode))) /\ ((dst_positive_weighted_exists_resultproductsright_table) + ge_balance_negative_weighted_exists_resultproductsright_tableentryvalue = (dst_negative_weighted_exists_resultproductsright_table) + ge_balance_positive_weighted_exists_resultproductsright_tableentryvalue))))))))) /\ (((exists dst_positive_code_weighted_exists_resultproductsoutput_table dst_positive_scale_weighted_exists_resultproductsoutput_table dst_negative_code_weighted_exists_resultproductsoutput_table dst_negative_scale_weighted_exists_resultproductsoutput_table. (((sws_product_table_weighted_exists_result) = (((((dst_positive_code_weighted_exists_resultproductsoutput_table) + (dst_positive_scale_weighted_exists_resultproductsoutput_table)) * S ((dst_positive_code_weighted_exists_resultproductsoutput_table) + (dst_positive_scale_weighted_exists_resultproductsoutput_table)) + ((dst_positive_scale_weighted_exists_resultproductsoutput_table) + (dst_positive_scale_weighted_exists_resultproductsoutput_table))) + (((dst_negative_code_weighted_exists_resultproductsoutput_table) + (dst_negative_scale_weighted_exists_resultproductsoutput_table)) * S ((dst_negative_code_weighted_exists_resultproductsoutput_table) + (dst_negative_scale_weighted_exists_resultproductsoutput_table)) + ((dst_negative_scale_weighted_exists_resultproductsoutput_table) + (dst_negative_scale_weighted_exists_resultproductsoutput_table)))) * S ((((dst_positive_code_weighted_exists_resultproductsoutput_table) + (dst_positive_scale_weighted_exists_resultproductsoutput_table)) * S ((dst_positive_code_weighted_exists_resultproductsoutput_table) + (dst_positive_scale_weighted_exists_resultproductsoutput_table)) + ((dst_positive_scale_weighted_exists_resultproductsoutput_table) + (dst_positive_scale_weighted_exists_resultproductsoutput_table))) + (((dst_negative_code_weighted_exists_resultproductsoutput_table) + (dst_negative_scale_weighted_exists_resultproductsoutput_table)) * S ((dst_negative_code_weighted_exists_resultproductsoutput_table) + (dst_negative_scale_weighted_exists_resultproductsoutput_table)) + ((dst_negative_scale_weighted_exists_resultproductsoutput_table) + (dst_negative_scale_weighted_exists_resultproductsoutput_table)))) + ((((dst_negative_code_weighted_exists_resultproductsoutput_table) + (dst_negative_scale_weighted_exists_resultproductsoutput_table)) * S ((dst_negative_code_weighted_exists_resultproductsoutput_table) + (dst_negative_scale_weighted_exists_resultproductsoutput_table)) + ((dst_negative_scale_weighted_exists_resultproductsoutput_table) + (dst_negative_scale_weighted_exists_resultproductsoutput_table))) + (((dst_negative_code_weighted_exists_resultproductsoutput_table) + (dst_negative_scale_weighted_exists_resultproductsoutput_table)) * S ((dst_negative_code_weighted_exists_resultproductsoutput_table) + (dst_negative_scale_weighted_exists_resultproductsoutput_table)) + ((dst_negative_scale_weighted_exists_resultproductsoutput_table) + (dst_negative_scale_weighted_exists_resultproductsoutput_table)))))) /\ (forall dst_index_weighted_exists_resultproductsoutput_table. (exists pvs_le_gap_weighted_exists_resultproductsoutput_tabledomain. pvs_le_gap_weighted_exists_resultproductsoutput_tabledomain + (dst_index_weighted_exists_resultproductsoutput_table) = (l)) -> exists dst_positive_weighted_exists_resultproductsoutput_table dst_negative_weighted_exists_resultproductsoutput_table dst_value_weighted_exists_resultproductsoutput_table. ((((exists ff_h_pvs_weighted_exists_resultproductsoutput_tableentrypositive. ff_h_pvs_weighted_exists_resultproductsoutput_tableentrypositive + S (dst_positive_weighted_exists_resultproductsoutput_table) = S ((S (dst_index_weighted_exists_resultproductsoutput_table)) * dst_positive_scale_weighted_exists_resultproductsoutput_table)) /\ exists ff_q_pvs_weighted_exists_resultproductsoutput_tableentrypositive. dst_positive_code_weighted_exists_resultproductsoutput_table = ff_q_pvs_weighted_exists_resultproductsoutput_tableentrypositive * S ((S (dst_index_weighted_exists_resultproductsoutput_table)) * dst_positive_scale_weighted_exists_resultproductsoutput_table) + (dst_positive_weighted_exists_resultproductsoutput_table))) /\ (((((exists ff_h_pvs_weighted_exists_resultproductsoutput_tableentrynegative. ff_h_pvs_weighted_exists_resultproductsoutput_tableentrynegative + S (dst_negative_weighted_exists_resultproductsoutput_table) = S ((S (dst_index_weighted_exists_resultproductsoutput_table)) * dst_negative_scale_weighted_exists_resultproductsoutput_table)) /\ exists ff_q_pvs_weighted_exists_resultproductsoutput_tableentrynegative. dst_negative_code_weighted_exists_resultproductsoutput_table = ff_q_pvs_weighted_exists_resultproductsoutput_tableentrynegative * S ((S (dst_index_weighted_exists_resultproductsoutput_table)) * dst_negative_scale_weighted_exists_resultproductsoutput_table) + (dst_negative_weighted_exists_resultproductsoutput_table))) /\ (exists ge_balance_positive_weighted_exists_resultproductsoutput_tableentryvalue ge_balance_negative_weighted_exists_resultproductsoutput_tableentryvalue. (((((dst_value_weighted_exists_resultproductsoutput_table) = 2 * (ge_balance_positive_weighted_exists_resultproductsoutput_tableentryvalue) /\ (ge_balance_negative_weighted_exists_resultproductsoutput_tableentryvalue) = 0) \/ exists ge_signed_half_weighted_exists_resultproductsoutput_tableentryvaluedecode. (((dst_value_weighted_exists_resultproductsoutput_table) = 2 * ge_signed_half_weighted_exists_resultproductsoutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_weighted_exists_resultproductsoutput_tableentryvalue) = 0) /\ (ge_balance_negative_weighted_exists_resultproductsoutput_tableentryvalue) = S ge_signed_half_weighted_exists_resultproductsoutput_tableentryvaluedecode))) /\ ((dst_positive_weighted_exists_resultproductsoutput_table) + ge_balance_negative_weighted_exists_resultproductsoutput_tableentryvalue = (dst_negative_weighted_exists_resultproductsoutput_table) + ge_balance_positive_weighted_exists_resultproductsoutput_tableentryvalue))))))))) /\ (forall sto_index_weighted_exists_resultproductsentries. (exists pvs_gap_weighted_exists_resultproductsentriesbound. pvs_gap_weighted_exists_resultproductsentriesbound + S (sto_index_weighted_exists_resultproductsentries) = (l)) -> exists sto_left_weighted_exists_resultproductsentries sto_right_weighted_exists_resultproductsentries sto_output_weighted_exists_resultproductsentries. ((exists dst_positive_code_weighted_exists_resultproductsentriesentryleft dst_positive_scale_weighted_exists_resultproductsentriesentryleft dst_negative_code_weighted_exists_resultproductsentriesentryleft dst_negative_scale_weighted_exists_resultproductsentriesentryleft dst_positive_weighted_exists_resultproductsentriesentryleft dst_negative_weighted_exists_resultproductsentriesentryleft. (((W) = (((((dst_positive_code_weighted_exists_resultproductsentriesentryleft) + (dst_positive_scale_weighted_exists_resultproductsentriesentryleft)) * S ((dst_positive_code_weighted_exists_resultproductsentriesentryleft) + (dst_positive_scale_weighted_exists_resultproductsentriesentryleft)) + ((dst_positive_scale_weighted_exists_resultproductsentriesentryleft) + (dst_positive_scale_weighted_exists_resultproductsentriesentryleft))) + (((dst_negative_code_weighted_exists_resultproductsentriesentryleft) + (dst_negative_scale_weighted_exists_resultproductsentriesentryleft)) * S ((dst_negative_code_weighted_exists_resultproductsentriesentryleft) + (dst_negative_scale_weighted_exists_resultproductsentriesentryleft)) + ((dst_negative_scale_weighted_exists_resultproductsentriesentryleft) + (dst_negative_scale_weighted_exists_resultproductsentriesentryleft)))) * S ((((dst_positive_code_weighted_exists_resultproductsentriesentryleft) + (dst_positive_scale_weighted_exists_resultproductsentriesentryleft)) * S ((dst_positive_code_weighted_exists_resultproductsentriesentryleft) + (dst_positive_scale_weighted_exists_resultproductsentriesentryleft)) + ((dst_positive_scale_weighted_exists_resultproductsentriesentryleft) + (dst_positive_scale_weighted_exists_resultproductsentriesentryleft))) + (((dst_negative_code_weighted_exists_resultproductsentriesentryleft) + (dst_negative_scale_weighted_exists_resultproductsentriesentryleft)) * S ((dst_negative_code_weighted_exists_resultproductsentriesentryleft) + (dst_negative_scale_weighted_exists_resultproductsentriesentryleft)) + ((dst_negative_scale_weighted_exists_resultproductsentriesentryleft) + (dst_negative_scale_weighted_exists_resultproductsentriesentryleft)))) + ((((dst_negative_code_weighted_exists_resultproductsentriesentryleft) + (dst_negative_scale_weighted_exists_resultproductsentriesentryleft)) * S ((dst_negative_code_weighted_exists_resultproductsentriesentryleft) + (dst_negative_scale_weighted_exists_resultproductsentriesentryleft)) + ((dst_negative_scale_weighted_exists_resultproductsentriesentryleft) + (dst_negative_scale_weighted_exists_resultproductsentriesentryleft))) + (((dst_negative_code_weighted_exists_resultproductsentriesentryleft) + (dst_negative_scale_weighted_exists_resultproductsentriesentryleft)) * S ((dst_negative_code_weighted_exists_resultproductsentriesentryleft) + (dst_negative_scale_weighted_exists_resultproductsentriesentryleft)) + ((dst_negative_scale_weighted_exists_resultproductsentriesentryleft) + (dst_negative_scale_weighted_exists_resultproductsentriesentryleft)))))) /\ (((((exists ff_h_pvs_weighted_exists_resultproductsentriesentryleftpositive. ff_h_pvs_weighted_exists_resultproductsentriesentryleftpositive + S (dst_positive_weighted_exists_resultproductsentriesentryleft) = S ((S (sto_index_weighted_exists_resultproductsentries)) * dst_positive_scale_weighted_exists_resultproductsentriesentryleft)) /\ exists ff_q_pvs_weighted_exists_resultproductsentriesentryleftpositive. dst_positive_code_weighted_exists_resultproductsentriesentryleft = ff_q_pvs_weighted_exists_resultproductsentriesentryleftpositive * S ((S (sto_index_weighted_exists_resultproductsentries)) * dst_positive_scale_weighted_exists_resultproductsentriesentryleft) + (dst_positive_weighted_exists_resultproductsentriesentryleft))) /\ (((((exists ff_h_pvs_weighted_exists_resultproductsentriesentryleftnegative. ff_h_pvs_weighted_exists_resultproductsentriesentryleftnegative + S (dst_negative_weighted_exists_resultproductsentriesentryleft) = S ((S (sto_index_weighted_exists_resultproductsentries)) * dst_negative_scale_weighted_exists_resultproductsentriesentryleft)) /\ exists ff_q_pvs_weighted_exists_resultproductsentriesentryleftnegative. dst_negative_code_weighted_exists_resultproductsentriesentryleft = ff_q_pvs_weighted_exists_resultproductsentriesentryleftnegative * S ((S (sto_index_weighted_exists_resultproductsentries)) * dst_negative_scale_weighted_exists_resultproductsentriesentryleft) + (dst_negative_weighted_exists_resultproductsentriesentryleft))) /\ (exists ge_balance_positive_weighted_exists_resultproductsentriesentryleftvalue ge_balance_negative_weighted_exists_resultproductsentriesentryleftvalue. (((((sto_left_weighted_exists_resultproductsentries) = 2 * (ge_balance_positive_weighted_exists_resultproductsentriesentryleftvalue) /\ (ge_balance_negative_weighted_exists_resultproductsentriesentryleftvalue) = 0) \/ exists ge_signed_half_weighted_exists_resultproductsentriesentryleftvaluedecode. (((sto_left_weighted_exists_resultproductsentries) = 2 * ge_signed_half_weighted_exists_resultproductsentriesentryleftvaluedecode + 1 /\ (ge_balance_positive_weighted_exists_resultproductsentriesentryleftvalue) = 0) /\ (ge_balance_negative_weighted_exists_resultproductsentriesentryleftvalue) = S ge_signed_half_weighted_exists_resultproductsentriesentryleftvaluedecode))) /\ ((dst_positive_weighted_exists_resultproductsentriesentryleft) + ge_balance_negative_weighted_exists_resultproductsentriesentryleftvalue = (dst_negative_weighted_exists_resultproductsentriesentryleft) + ge_balance_positive_weighted_exists_resultproductsentriesentryleftvalue))))))))) /\ (((exists dst_positive_code_weighted_exists_resultproductsentriesentryright dst_positive_scale_weighted_exists_resultproductsentriesentryright dst_negative_code_weighted_exists_resultproductsentriesentryright dst_negative_scale_weighted_exists_resultproductsentriesentryright dst_positive_weighted_exists_resultproductsentriesentryright dst_negative_weighted_exists_resultproductsentriesentryright. (((F) = (((((dst_positive_code_weighted_exists_resultproductsentriesentryright) + (dst_positive_scale_weighted_exists_resultproductsentriesentryright)) * S ((dst_positive_code_weighted_exists_resultproductsentriesentryright) + (dst_positive_scale_weighted_exists_resultproductsentriesentryright)) + ((dst_positive_scale_weighted_exists_resultproductsentriesentryright) + (dst_positive_scale_weighted_exists_resultproductsentriesentryright))) + (((dst_negative_code_weighted_exists_resultproductsentriesentryright) + (dst_negative_scale_weighted_exists_resultproductsentriesentryright)) * S ((dst_negative_code_weighted_exists_resultproductsentriesentryright) + (dst_negative_scale_weighted_exists_resultproductsentriesentryright)) + ((dst_negative_scale_weighted_exists_resultproductsentriesentryright) + (dst_negative_scale_weighted_exists_resultproductsentriesentryright)))) * S ((((dst_positive_code_weighted_exists_resultproductsentriesentryright) + (dst_positive_scale_weighted_exists_resultproductsentriesentryright)) * S ((dst_positive_code_weighted_exists_resultproductsentriesentryright) + (dst_positive_scale_weighted_exists_resultproductsentriesentryright)) + ((dst_positive_scale_weighted_exists_resultproductsentriesentryright) + (dst_positive_scale_weighted_exists_resultproductsentriesentryright))) + (((dst_negative_code_weighted_exists_resultproductsentriesentryright) + (dst_negative_scale_weighted_exists_resultproductsentriesentryright)) * S ((dst_negative_code_weighted_exists_resultproductsentriesentryright) + (dst_negative_scale_weighted_exists_resultproductsentriesentryright)) + ((dst_negative_scale_weighted_exists_resultproductsentriesentryright) + (dst_negative_scale_weighted_exists_resultproductsentriesentryright)))) + ((((dst_negative_code_weighted_exists_resultproductsentriesentryright) + (dst_negative_scale_weighted_exists_resultproductsentriesentryright)) * S ((dst_negative_code_weighted_exists_resultproductsentriesentryright) + (dst_negative_scale_weighted_exists_resultproductsentriesentryright)) + ((dst_negative_scale_weighted_exists_resultproductsentriesentryright) + (dst_negative_scale_weighted_exists_resultproductsentriesentryright))) + (((dst_negative_code_weighted_exists_resultproductsentriesentryright) + (dst_negative_scale_weighted_exists_resultproductsentriesentryright)) * S ((dst_negative_code_weighted_exists_resultproductsentriesentryright) + (dst_negative_scale_weighted_exists_resultproductsentriesentryright)) + ((dst_negative_scale_weighted_exists_resultproductsentriesentryright) + (dst_negative_scale_weighted_exists_resultproductsentriesentryright)))))) /\ (((((exists ff_h_pvs_weighted_exists_resultproductsentriesentryrightpositive. ff_h_pvs_weighted_exists_resultproductsentriesentryrightpositive + S (dst_positive_weighted_exists_resultproductsentriesentryright) = S ((S (sto_index_weighted_exists_resultproductsentries)) * dst_positive_scale_weighted_exists_resultproductsentriesentryright)) /\ exists ff_q_pvs_weighted_exists_resultproductsentriesentryrightpositive. dst_positive_code_weighted_exists_resultproductsentriesentryright = ff_q_pvs_weighted_exists_resultproductsentriesentryrightpositive * S ((S (sto_index_weighted_exists_resultproductsentries)) * dst_positive_scale_weighted_exists_resultproductsentriesentryright) + (dst_positive_weighted_exists_resultproductsentriesentryright))) /\ (((((exists ff_h_pvs_weighted_exists_resultproductsentriesentryrightnegative. ff_h_pvs_weighted_exists_resultproductsentriesentryrightnegative + S (dst_negative_weighted_exists_resultproductsentriesentryright) = S ((S (sto_index_weighted_exists_resultproductsentries)) * dst_negative_scale_weighted_exists_resultproductsentriesentryright)) /\ exists ff_q_pvs_weighted_exists_resultproductsentriesentryrightnegative. dst_negative_code_weighted_exists_resultproductsentriesentryright = ff_q_pvs_weighted_exists_resultproductsentriesentryrightnegative * S ((S (sto_index_weighted_exists_resultproductsentries)) * dst_negative_scale_weighted_exists_resultproductsentriesentryright) + (dst_negative_weighted_exists_resultproductsentriesentryright))) /\ (exists ge_balance_positive_weighted_exists_resultproductsentriesentryrightvalue ge_balance_negative_weighted_exists_resultproductsentriesentryrightvalue. (((((sto_right_weighted_exists_resultproductsentries) = 2 * (ge_balance_positive_weighted_exists_resultproductsentriesentryrightvalue) /\ (ge_balance_negative_weighted_exists_resultproductsentriesentryrightvalue) = 0) \/ exists ge_signed_half_weighted_exists_resultproductsentriesentryrightvaluedecode. (((sto_right_weighted_exists_resultproductsentries) = 2 * ge_signed_half_weighted_exists_resultproductsentriesentryrightvaluedecode + 1 /\ (ge_balance_positive_weighted_exists_resultproductsentriesentryrightvalue) = 0) /\ (ge_balance_negative_weighted_exists_resultproductsentriesentryrightvalue) = S ge_signed_half_weighted_exists_resultproductsentriesentryrightvaluedecode))) /\ ((dst_positive_weighted_exists_resultproductsentriesentryright) + ge_balance_negative_weighted_exists_resultproductsentriesentryrightvalue = (dst_negative_weighted_exists_resultproductsentriesentryright) + ge_balance_positive_weighted_exists_resultproductsentriesentryrightvalue))))))))) /\ (((exists dst_positive_code_weighted_exists_resultproductsentriesentryoutput dst_positive_scale_weighted_exists_resultproductsentriesentryoutput dst_negative_code_weighted_exists_resultproductsentriesentryoutput dst_negative_scale_weighted_exists_resultproductsentriesentryoutput dst_positive_weighted_exists_resultproductsentriesentryoutput dst_negative_weighted_exists_resultproductsentriesentryoutput. (((sws_product_table_weighted_exists_result) = (((((dst_positive_code_weighted_exists_resultproductsentriesentryoutput) + (dst_positive_scale_weighted_exists_resultproductsentriesentryoutput)) * S ((dst_positive_code_weighted_exists_resultproductsentriesentryoutput) + (dst_positive_scale_weighted_exists_resultproductsentriesentryoutput)) + ((dst_positive_scale_weighted_exists_resultproductsentriesentryoutput) + (dst_positive_scale_weighted_exists_resultproductsentriesentryoutput))) + (((dst_negative_code_weighted_exists_resultproductsentriesentryoutput) + (dst_negative_scale_weighted_exists_resultproductsentriesentryoutput)) * S ((dst_negative_code_weighted_exists_resultproductsentriesentryoutput) + (dst_negative_scale_weighted_exists_resultproductsentriesentryoutput)) + ((dst_negative_scale_weighted_exists_resultproductsentriesentryoutput) + (dst_negative_scale_weighted_exists_resultproductsentriesentryoutput)))) * S ((((dst_positive_code_weighted_exists_resultproductsentriesentryoutput) + (dst_positive_scale_weighted_exists_resultproductsentriesentryoutput)) * S ((dst_positive_code_weighted_exists_resultproductsentriesentryoutput) + (dst_positive_scale_weighted_exists_resultproductsentriesentryoutput)) + ((dst_positive_scale_weighted_exists_resultproductsentriesentryoutput) + (dst_positive_scale_weighted_exists_resultproductsentriesentryoutput))) + (((dst_negative_code_weighted_exists_resultproductsentriesentryoutput) + (dst_negative_scale_weighted_exists_resultproductsentriesentryoutput)) * S ((dst_negative_code_weighted_exists_resultproductsentriesentryoutput) + (dst_negative_scale_weighted_exists_resultproductsentriesentryoutput)) + ((dst_negative_scale_weighted_exists_resultproductsentriesentryoutput) + (dst_negative_scale_weighted_exists_resultproductsentriesentryoutput)))) + ((((dst_negative_code_weighted_exists_resultproductsentriesentryoutput) + (dst_negative_scale_weighted_exists_resultproductsentriesentryoutput)) * S ((dst_negative_code_weighted_exists_resultproductsentriesentryoutput) + (dst_negative_scale_weighted_exists_resultproductsentriesentryoutput)) + ((dst_negative_scale_weighted_exists_resultproductsentriesentryoutput) + (dst_negative_scale_weighted_exists_resultproductsentriesentryoutput))) + (((dst_negative_code_weighted_exists_resultproductsentriesentryoutput) + (dst_negative_scale_weighted_exists_resultproductsentriesentryoutput)) * S ((dst_negative_code_weighted_exists_resultproductsentriesentryoutput) + (dst_negative_scale_weighted_exists_resultproductsentriesentryoutput)) + ((dst_negative_scale_weighted_exists_resultproductsentriesentryoutput) + (dst_negative_scale_weighted_exists_resultproductsentriesentryoutput)))))) /\ (((((exists ff_h_pvs_weighted_exists_resultproductsentriesentryoutputpositive. ff_h_pvs_weighted_exists_resultproductsentriesentryoutputpositive + S (dst_positive_weighted_exists_resultproductsentriesentryoutput) = S ((S (sto_index_weighted_exists_resultproductsentries)) * dst_positive_scale_weighted_exists_resultproductsentriesentryoutput)) /\ exists ff_q_pvs_weighted_exists_resultproductsentriesentryoutputpositive. dst_positive_code_weighted_exists_resultproductsentriesentryoutput = ff_q_pvs_weighted_exists_resultproductsentriesentryoutputpositive * S ((S (sto_index_weighted_exists_resultproductsentries)) * dst_positive_scale_weighted_exists_resultproductsentriesentryoutput) + (dst_positive_weighted_exists_resultproductsentriesentryoutput))) /\ (((((exists ff_h_pvs_weighted_exists_resultproductsentriesentryoutputnegative. ff_h_pvs_weighted_exists_resultproductsentriesentryoutputnegative + S (dst_negative_weighted_exists_resultproductsentriesentryoutput) = S ((S (sto_index_weighted_exists_resultproductsentries)) * dst_negative_scale_weighted_exists_resultproductsentriesentryoutput)) /\ exists ff_q_pvs_weighted_exists_resultproductsentriesentryoutputnegative. dst_negative_code_weighted_exists_resultproductsentriesentryoutput = ff_q_pvs_weighted_exists_resultproductsentriesentryoutputnegative * S ((S (sto_index_weighted_exists_resultproductsentries)) * dst_negative_scale_weighted_exists_resultproductsentriesentryoutput) + (dst_negative_weighted_exists_resultproductsentriesentryoutput))) /\ (exists ge_balance_positive_weighted_exists_resultproductsentriesentryoutputvalue ge_balance_negative_weighted_exists_resultproductsentriesentryoutputvalue. (((((sto_output_weighted_exists_resultproductsentries) = 2 * (ge_balance_positive_weighted_exists_resultproductsentriesentryoutputvalue) /\ (ge_balance_negative_weighted_exists_resultproductsentriesentryoutputvalue) = 0) \/ exists ge_signed_half_weighted_exists_resultproductsentriesentryoutputvaluedecode. (((sto_output_weighted_exists_resultproductsentries) = 2 * ge_signed_half_weighted_exists_resultproductsentriesentryoutputvaluedecode + 1 /\ (ge_balance_positive_weighted_exists_resultproductsentriesentryoutputvalue) = 0) /\ (ge_balance_negative_weighted_exists_resultproductsentriesentryoutputvalue) = S ge_signed_half_weighted_exists_resultproductsentriesentryoutputvaluedecode))) /\ ((dst_positive_weighted_exists_resultproductsentriesentryoutput) + ge_balance_negative_weighted_exists_resultproductsentriesentryoutputvalue = (dst_negative_weighted_exists_resultproductsentriesentryoutput) + ge_balance_positive_weighted_exists_resultproductsentriesentryoutputvalue))))))))) /\ (exists sto_ap_weighted_exists_resultproductsentriesentryoperation sto_an_weighted_exists_resultproductsentriesentryoperation sto_bp_weighted_exists_resultproductsentriesentryoperation sto_bn_weighted_exists_resultproductsentriesentryoperation sto_cp_weighted_exists_resultproductsentriesentryoperation sto_cn_weighted_exists_resultproductsentriesentryoperation. (((((sto_left_weighted_exists_resultproductsentries) = 2 * (sto_ap_weighted_exists_resultproductsentriesentryoperation) /\ (sto_an_weighted_exists_resultproductsentriesentryoperation) = 0) \/ exists ge_signed_half_weighted_exists_resultproductsentriesentryoperationleft. (((sto_left_weighted_exists_resultproductsentries) = 2 * ge_signed_half_weighted_exists_resultproductsentriesentryoperationleft + 1 /\ (sto_ap_weighted_exists_resultproductsentriesentryoperation) = 0) /\ (sto_an_weighted_exists_resultproductsentriesentryoperation) = S ge_signed_half_weighted_exists_resultproductsentriesentryoperationleft))) /\ ((((((sto_right_weighted_exists_resultproductsentries) = 2 * (sto_bp_weighted_exists_resultproductsentriesentryoperation) /\ (sto_bn_weighted_exists_resultproductsentriesentryoperation) = 0) \/ exists ge_signed_half_weighted_exists_resultproductsentriesentryoperationright. (((sto_right_weighted_exists_resultproductsentries) = 2 * ge_signed_half_weighted_exists_resultproductsentriesentryoperationright + 1 /\ (sto_bp_weighted_exists_resultproductsentriesentryoperation) = 0) /\ (sto_bn_weighted_exists_resultproductsentriesentryoperation) = S ge_signed_half_weighted_exists_resultproductsentriesentryoperationright))) /\ ((((((sto_output_weighted_exists_resultproductsentries) = 2 * (sto_cp_weighted_exists_resultproductsentriesentryoperation) /\ (sto_cn_weighted_exists_resultproductsentriesentryoperation) = 0) \/ exists ge_signed_half_weighted_exists_resultproductsentriesentryoperationoutput. (((sto_output_weighted_exists_resultproductsentries) = 2 * ge_signed_half_weighted_exists_resultproductsentriesentryoperationoutput + 1 /\ (sto_cp_weighted_exists_resultproductsentriesentryoperation) = 0) /\ (sto_cn_weighted_exists_resultproductsentriesentryoperation) = S ge_signed_half_weighted_exists_resultproductsentriesentryoperationoutput))) /\ ((sto_ap_weighted_exists_resultproductsentriesentryoperation * sto_bp_weighted_exists_resultproductsentriesentryoperation + sto_an_weighted_exists_resultproductsentriesentryoperation * sto_bn_weighted_exists_resultproductsentriesentryoperation) + sto_cn_weighted_exists_resultproductsentriesentryoperation = (sto_ap_weighted_exists_resultproductsentriesentryoperation * sto_bn_weighted_exists_resultproductsentriesentryoperation + sto_an_weighted_exists_resultproductsentriesentryoperation * sto_bp_weighted_exists_resultproductsentriesentryoperation) + sto_cp_weighted_exists_resultproductsentriesentryoperation))))))))))))))))))) /\ (exists dst_positive_code_weighted_exists_resultsum dst_positive_scale_weighted_exists_resultsum dst_negative_code_weighted_exists_resultsum dst_negative_scale_weighted_exists_resultsum dst_positive_sum_weighted_exists_resultsum dst_negative_sum_weighted_exists_resultsum. (((sws_product_table_weighted_exists_result) = (((((dst_positive_code_weighted_exists_resultsum) + (dst_positive_scale_weighted_exists_resultsum)) * S ((dst_positive_code_weighted_exists_resultsum) + (dst_positive_scale_weighted_exists_resultsum)) + ((dst_positive_scale_weighted_exists_resultsum) + (dst_positive_scale_weighted_exists_resultsum))) + (((dst_negative_code_weighted_exists_resultsum) + (dst_negative_scale_weighted_exists_resultsum)) * S ((dst_negative_code_weighted_exists_resultsum) + (dst_negative_scale_weighted_exists_resultsum)) + ((dst_negative_scale_weighted_exists_resultsum) + (dst_negative_scale_weighted_exists_resultsum)))) * S ((((dst_positive_code_weighted_exists_resultsum) + (dst_positive_scale_weighted_exists_resultsum)) * S ((dst_positive_code_weighted_exists_resultsum) + (dst_positive_scale_weighted_exists_resultsum)) + ((dst_positive_scale_weighted_exists_resultsum) + (dst_positive_scale_weighted_exists_resultsum))) + (((dst_negative_code_weighted_exists_resultsum) + (dst_negative_scale_weighted_exists_resultsum)) * S ((dst_negative_code_weighted_exists_resultsum) + (dst_negative_scale_weighted_exists_resultsum)) + ((dst_negative_scale_weighted_exists_resultsum) + (dst_negative_scale_weighted_exists_resultsum)))) + ((((dst_negative_code_weighted_exists_resultsum) + (dst_negative_scale_weighted_exists_resultsum)) * S ((dst_negative_code_weighted_exists_resultsum) + (dst_negative_scale_weighted_exists_resultsum)) + ((dst_negative_scale_weighted_exists_resultsum) + (dst_negative_scale_weighted_exists_resultsum))) + (((dst_negative_code_weighted_exists_resultsum) + (dst_negative_scale_weighted_exists_resultsum)) * S ((dst_negative_code_weighted_exists_resultsum) + (dst_negative_scale_weighted_exists_resultsum)) + ((dst_negative_scale_weighted_exists_resultsum) + (dst_negative_scale_weighted_exists_resultsum)))))) /\ (((exists fs_u_dst_weighted_exists_resultsumpositive fs_v_dst_weighted_exists_resultsumpositive. ((((exists fs_h_dst_weighted_exists_resultsumpositive_body_start. fs_h_dst_weighted_exists_resultsumpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_weighted_exists_resultsumpositive)) /\ exists fs_q_dst_weighted_exists_resultsumpositive_body_start. fs_u_dst_weighted_exists_resultsumpositive = fs_q_dst_weighted_exists_resultsumpositive_body_start * S ((S (0)) * fs_v_dst_weighted_exists_resultsumpositive) + (0))) /\ ((((exists fs_h_dst_weighted_exists_resultsumpositive_body_terminal. fs_h_dst_weighted_exists_resultsumpositive_body_terminal + S (dst_positive_sum_weighted_exists_resultsum) = S ((S (l)) * fs_v_dst_weighted_exists_resultsumpositive)) /\ exists fs_q_dst_weighted_exists_resultsumpositive_body_terminal. fs_u_dst_weighted_exists_resultsumpositive = fs_q_dst_weighted_exists_resultsumpositive_body_terminal * S ((S (l)) * fs_v_dst_weighted_exists_resultsumpositive) + (dst_positive_sum_weighted_exists_resultsum))) /\ forall fs_i_dst_weighted_exists_resultsumpositive_body_steps. (exists fs_lt_dst_weighted_exists_resultsumpositive_body_steps_bound. fs_lt_dst_weighted_exists_resultsumpositive_body_steps_bound + S fs_i_dst_weighted_exists_resultsumpositive_body_steps = l) -> exists fs_a_dst_weighted_exists_resultsumpositive_body_steps fs_r_dst_weighted_exists_resultsumpositive_body_steps fs_s_dst_weighted_exists_resultsumpositive_body_steps. ((((exists fs_h_dst_weighted_exists_resultsumpositive_body_steps_summand. fs_h_dst_weighted_exists_resultsumpositive_body_steps_summand + S (fs_a_dst_weighted_exists_resultsumpositive_body_steps) = S ((S (fs_i_dst_weighted_exists_resultsumpositive_body_steps)) * dst_positive_scale_weighted_exists_resultsum)) /\ exists fs_q_dst_weighted_exists_resultsumpositive_body_steps_summand. dst_positive_code_weighted_exists_resultsum = fs_q_dst_weighted_exists_resultsumpositive_body_steps_summand * S ((S (fs_i_dst_weighted_exists_resultsumpositive_body_steps)) * dst_positive_scale_weighted_exists_resultsum) + (fs_a_dst_weighted_exists_resultsumpositive_body_steps))) /\ ((((exists fs_h_dst_weighted_exists_resultsumpositive_body_steps_partial. fs_h_dst_weighted_exists_resultsumpositive_body_steps_partial + S (fs_r_dst_weighted_exists_resultsumpositive_body_steps) = S ((S (fs_i_dst_weighted_exists_resultsumpositive_body_steps)) * fs_v_dst_weighted_exists_resultsumpositive)) /\ exists fs_q_dst_weighted_exists_resultsumpositive_body_steps_partial. fs_u_dst_weighted_exists_resultsumpositive = fs_q_dst_weighted_exists_resultsumpositive_body_steps_partial * S ((S (fs_i_dst_weighted_exists_resultsumpositive_body_steps)) * fs_v_dst_weighted_exists_resultsumpositive) + (fs_r_dst_weighted_exists_resultsumpositive_body_steps))) /\ ((((exists fs_h_dst_weighted_exists_resultsumpositive_body_steps_successor. fs_h_dst_weighted_exists_resultsumpositive_body_steps_successor + S (fs_s_dst_weighted_exists_resultsumpositive_body_steps) = S ((S (S fs_i_dst_weighted_exists_resultsumpositive_body_steps)) * fs_v_dst_weighted_exists_resultsumpositive)) /\ exists fs_q_dst_weighted_exists_resultsumpositive_body_steps_successor. fs_u_dst_weighted_exists_resultsumpositive = fs_q_dst_weighted_exists_resultsumpositive_body_steps_successor * S ((S (S fs_i_dst_weighted_exists_resultsumpositive_body_steps)) * fs_v_dst_weighted_exists_resultsumpositive) + (fs_s_dst_weighted_exists_resultsumpositive_body_steps))) /\ fs_s_dst_weighted_exists_resultsumpositive_body_steps = fs_r_dst_weighted_exists_resultsumpositive_body_steps + fs_a_dst_weighted_exists_resultsumpositive_body_steps)))))) /\ (((exists fs_u_dst_weighted_exists_resultsumnegative fs_v_dst_weighted_exists_resultsumnegative. ((((exists fs_h_dst_weighted_exists_resultsumnegative_body_start. fs_h_dst_weighted_exists_resultsumnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_weighted_exists_resultsumnegative)) /\ exists fs_q_dst_weighted_exists_resultsumnegative_body_start. fs_u_dst_weighted_exists_resultsumnegative = fs_q_dst_weighted_exists_resultsumnegative_body_start * S ((S (0)) * fs_v_dst_weighted_exists_resultsumnegative) + (0))) /\ ((((exists fs_h_dst_weighted_exists_resultsumnegative_body_terminal. fs_h_dst_weighted_exists_resultsumnegative_body_terminal + S (dst_negative_sum_weighted_exists_resultsum) = S ((S (l)) * fs_v_dst_weighted_exists_resultsumnegative)) /\ exists fs_q_dst_weighted_exists_resultsumnegative_body_terminal. fs_u_dst_weighted_exists_resultsumnegative = fs_q_dst_weighted_exists_resultsumnegative_body_terminal * S ((S (l)) * fs_v_dst_weighted_exists_resultsumnegative) + (dst_negative_sum_weighted_exists_resultsum))) /\ forall fs_i_dst_weighted_exists_resultsumnegative_body_steps. (exists fs_lt_dst_weighted_exists_resultsumnegative_body_steps_bound. fs_lt_dst_weighted_exists_resultsumnegative_body_steps_bound + S fs_i_dst_weighted_exists_resultsumnegative_body_steps = l) -> exists fs_a_dst_weighted_exists_resultsumnegative_body_steps fs_r_dst_weighted_exists_resultsumnegative_body_steps fs_s_dst_weighted_exists_resultsumnegative_body_steps. ((((exists fs_h_dst_weighted_exists_resultsumnegative_body_steps_summand. fs_h_dst_weighted_exists_resultsumnegative_body_steps_summand + S (fs_a_dst_weighted_exists_resultsumnegative_body_steps) = S ((S (fs_i_dst_weighted_exists_resultsumnegative_body_steps)) * dst_negative_scale_weighted_exists_resultsum)) /\ exists fs_q_dst_weighted_exists_resultsumnegative_body_steps_summand. dst_negative_code_weighted_exists_resultsum = fs_q_dst_weighted_exists_resultsumnegative_body_steps_summand * S ((S (fs_i_dst_weighted_exists_resultsumnegative_body_steps)) * dst_negative_scale_weighted_exists_resultsum) + (fs_a_dst_weighted_exists_resultsumnegative_body_steps))) /\ ((((exists fs_h_dst_weighted_exists_resultsumnegative_body_steps_partial. fs_h_dst_weighted_exists_resultsumnegative_body_steps_partial + S (fs_r_dst_weighted_exists_resultsumnegative_body_steps) = S ((S (fs_i_dst_weighted_exists_resultsumnegative_body_steps)) * fs_v_dst_weighted_exists_resultsumnegative)) /\ exists fs_q_dst_weighted_exists_resultsumnegative_body_steps_partial. fs_u_dst_weighted_exists_resultsumnegative = fs_q_dst_weighted_exists_resultsumnegative_body_steps_partial * S ((S (fs_i_dst_weighted_exists_resultsumnegative_body_steps)) * fs_v_dst_weighted_exists_resultsumnegative) + (fs_r_dst_weighted_exists_resultsumnegative_body_steps))) /\ ((((exists fs_h_dst_weighted_exists_resultsumnegative_body_steps_successor. fs_h_dst_weighted_exists_resultsumnegative_body_steps_successor + S (fs_s_dst_weighted_exists_resultsumnegative_body_steps) = S ((S (S fs_i_dst_weighted_exists_resultsumnegative_body_steps)) * fs_v_dst_weighted_exists_resultsumnegative)) /\ exists fs_q_dst_weighted_exists_resultsumnegative_body_steps_successor. fs_u_dst_weighted_exists_resultsumnegative = fs_q_dst_weighted_exists_resultsumnegative_body_steps_successor * S ((S (S fs_i_dst_weighted_exists_resultsumnegative_body_steps)) * fs_v_dst_weighted_exists_resultsumnegative) + (fs_s_dst_weighted_exists_resultsumnegative_body_steps))) /\ fs_s_dst_weighted_exists_resultsumnegative_body_steps = fs_r_dst_weighted_exists_resultsumnegative_body_steps + fs_a_dst_weighted_exists_resultsumnegative_body_steps)))))) /\ (exists ge_balance_positive_weighted_exists_resultsumresult ge_balance_negative_weighted_exists_resultsumresult. (((((z) = 2 * (ge_balance_positive_weighted_exists_resultsumresult) /\ (ge_balance_negative_weighted_exists_resultsumresult) = 0) \/ exists ge_signed_half_weighted_exists_resultsumresultdecode. (((z) = 2 * ge_signed_half_weighted_exists_resultsumresultdecode + 1 /\ (ge_balance_positive_weighted_exists_resultsumresult) = 0) /\ (ge_balance_negative_weighted_exists_resultsumresult) = S ge_signed_half_weighted_exists_resultsumresultdecode))) /\ ((dst_positive_sum_weighted_exists_resultsum) + ge_balance_negative_weighted_exists_resultsumresult = (dst_negative_sum_weighted_exists_resultsum) + ge_balance_positive_weighted_exists_resultsumresult)))))))))))