signed_weighted_sum_empty_exists

Exact expanded first-order arithmetic statement

forall W F. (exists dst_positive_code_weighted_empty_weights dst_positive_scale_weighted_empty_weights dst_negative_code_weighted_empty_weights dst_negative_scale_weighted_empty_weights. (((W) = (((((dst_positive_code_weighted_empty_weights) + (dst_positive_scale_weighted_empty_weights)) * S ((dst_positive_code_weighted_empty_weights) + (dst_positive_scale_weighted_empty_weights)) + ((dst_positive_scale_weighted_empty_weights) + (dst_positive_scale_weighted_empty_weights))) + (((dst_negative_code_weighted_empty_weights) + (dst_negative_scale_weighted_empty_weights)) * S ((dst_negative_code_weighted_empty_weights) + (dst_negative_scale_weighted_empty_weights)) + ((dst_negative_scale_weighted_empty_weights) + (dst_negative_scale_weighted_empty_weights)))) * S ((((dst_positive_code_weighted_empty_weights) + (dst_positive_scale_weighted_empty_weights)) * S ((dst_positive_code_weighted_empty_weights) + (dst_positive_scale_weighted_empty_weights)) + ((dst_positive_scale_weighted_empty_weights) + (dst_positive_scale_weighted_empty_weights))) + (((dst_negative_code_weighted_empty_weights) + (dst_negative_scale_weighted_empty_weights)) * S ((dst_negative_code_weighted_empty_weights) + (dst_negative_scale_weighted_empty_weights)) + ((dst_negative_scale_weighted_empty_weights) + (dst_negative_scale_weighted_empty_weights)))) + ((((dst_negative_code_weighted_empty_weights) + (dst_negative_scale_weighted_empty_weights)) * S ((dst_negative_code_weighted_empty_weights) + (dst_negative_scale_weighted_empty_weights)) + ((dst_negative_scale_weighted_empty_weights) + (dst_negative_scale_weighted_empty_weights))) + (((dst_negative_code_weighted_empty_weights) + (dst_negative_scale_weighted_empty_weights)) * S ((dst_negative_code_weighted_empty_weights) + (dst_negative_scale_weighted_empty_weights)) + ((dst_negative_scale_weighted_empty_weights) + (dst_negative_scale_weighted_empty_weights)))))) /\ (forall dst_index_weighted_empty_weights. (exists pvs_le_gap_weighted_empty_weightsdomain. pvs_le_gap_weighted_empty_weightsdomain + (dst_index_weighted_empty_weights) = (0)) -> exists dst_positive_weighted_empty_weights dst_negative_weighted_empty_weights dst_value_weighted_empty_weights. ((((exists ff_h_pvs_weighted_empty_weightsentrypositive. ff_h_pvs_weighted_empty_weightsentrypositive + S (dst_positive_weighted_empty_weights) = S ((S (dst_index_weighted_empty_weights)) * dst_positive_scale_weighted_empty_weights)) /\ exists ff_q_pvs_weighted_empty_weightsentrypositive. dst_positive_code_weighted_empty_weights = ff_q_pvs_weighted_empty_weightsentrypositive * S ((S (dst_index_weighted_empty_weights)) * dst_positive_scale_weighted_empty_weights) + (dst_positive_weighted_empty_weights))) /\ (((((exists ff_h_pvs_weighted_empty_weightsentrynegative. ff_h_pvs_weighted_empty_weightsentrynegative + S (dst_negative_weighted_empty_weights) = S ((S (dst_index_weighted_empty_weights)) * dst_negative_scale_weighted_empty_weights)) /\ exists ff_q_pvs_weighted_empty_weightsentrynegative. dst_negative_code_weighted_empty_weights = ff_q_pvs_weighted_empty_weightsentrynegative * S ((S (dst_index_weighted_empty_weights)) * dst_negative_scale_weighted_empty_weights) + (dst_negative_weighted_empty_weights))) /\ (exists ge_balance_positive_weighted_empty_weightsentryvalue ge_balance_negative_weighted_empty_weightsentryvalue. (((((dst_value_weighted_empty_weights) = 2 * (ge_balance_positive_weighted_empty_weightsentryvalue) /\ (ge_balance_negative_weighted_empty_weightsentryvalue) = 0) \/ exists ge_signed_half_weighted_empty_weightsentryvaluedecode. (((dst_value_weighted_empty_weights) = 2 * ge_signed_half_weighted_empty_weightsentryvaluedecode + 1 /\ (ge_balance_positive_weighted_empty_weightsentryvalue) = 0) /\ (ge_balance_negative_weighted_empty_weightsentryvalue) = S ge_signed_half_weighted_empty_weightsentryvaluedecode))) /\ ((dst_positive_weighted_empty_weights) + ge_balance_negative_weighted_empty_weightsentryvalue = (dst_negative_weighted_empty_weights) + ge_balance_positive_weighted_empty_weightsentryvalue))))))))) -> (exists dst_positive_code_weighted_empty_values dst_positive_scale_weighted_empty_values dst_negative_code_weighted_empty_values dst_negative_scale_weighted_empty_values. (((F) = (((((dst_positive_code_weighted_empty_values) + (dst_positive_scale_weighted_empty_values)) * S ((dst_positive_code_weighted_empty_values) + (dst_positive_scale_weighted_empty_values)) + ((dst_positive_scale_weighted_empty_values) + (dst_positive_scale_weighted_empty_values))) + (((dst_negative_code_weighted_empty_values) + (dst_negative_scale_weighted_empty_values)) * S ((dst_negative_code_weighted_empty_values) + (dst_negative_scale_weighted_empty_values)) + ((dst_negative_scale_weighted_empty_values) + (dst_negative_scale_weighted_empty_values)))) * S ((((dst_positive_code_weighted_empty_values) + (dst_positive_scale_weighted_empty_values)) * S ((dst_positive_code_weighted_empty_values) + (dst_positive_scale_weighted_empty_values)) + ((dst_positive_scale_weighted_empty_values) + (dst_positive_scale_weighted_empty_values))) + (((dst_negative_code_weighted_empty_values) + (dst_negative_scale_weighted_empty_values)) * S ((dst_negative_code_weighted_empty_values) + (dst_negative_scale_weighted_empty_values)) + ((dst_negative_scale_weighted_empty_values) + (dst_negative_scale_weighted_empty_values)))) + ((((dst_negative_code_weighted_empty_values) + (dst_negative_scale_weighted_empty_values)) * S ((dst_negative_code_weighted_empty_values) + (dst_negative_scale_weighted_empty_values)) + ((dst_negative_scale_weighted_empty_values) + (dst_negative_scale_weighted_empty_values))) + (((dst_negative_code_weighted_empty_values) + (dst_negative_scale_weighted_empty_values)) * S ((dst_negative_code_weighted_empty_values) + (dst_negative_scale_weighted_empty_values)) + ((dst_negative_scale_weighted_empty_values) + (dst_negative_scale_weighted_empty_values)))))) /\ (forall dst_index_weighted_empty_values. (exists pvs_le_gap_weighted_empty_valuesdomain. pvs_le_gap_weighted_empty_valuesdomain + (dst_index_weighted_empty_values) = (0)) -> exists dst_positive_weighted_empty_values dst_negative_weighted_empty_values dst_value_weighted_empty_values. ((((exists ff_h_pvs_weighted_empty_valuesentrypositive. ff_h_pvs_weighted_empty_valuesentrypositive + S (dst_positive_weighted_empty_values) = S ((S (dst_index_weighted_empty_values)) * dst_positive_scale_weighted_empty_values)) /\ exists ff_q_pvs_weighted_empty_valuesentrypositive. dst_positive_code_weighted_empty_values = ff_q_pvs_weighted_empty_valuesentrypositive * S ((S (dst_index_weighted_empty_values)) * dst_positive_scale_weighted_empty_values) + (dst_positive_weighted_empty_values))) /\ (((((exists ff_h_pvs_weighted_empty_valuesentrynegative. ff_h_pvs_weighted_empty_valuesentrynegative + S (dst_negative_weighted_empty_values) = S ((S (dst_index_weighted_empty_values)) * dst_negative_scale_weighted_empty_values)) /\ exists ff_q_pvs_weighted_empty_valuesentrynegative. dst_negative_code_weighted_empty_values = ff_q_pvs_weighted_empty_valuesentrynegative * S ((S (dst_index_weighted_empty_values)) * dst_negative_scale_weighted_empty_values) + (dst_negative_weighted_empty_values))) /\ (exists ge_balance_positive_weighted_empty_valuesentryvalue ge_balance_negative_weighted_empty_valuesentryvalue. (((((dst_value_weighted_empty_values) = 2 * (ge_balance_positive_weighted_empty_valuesentryvalue) /\ (ge_balance_negative_weighted_empty_valuesentryvalue) = 0) \/ exists ge_signed_half_weighted_empty_valuesentryvaluedecode. (((dst_value_weighted_empty_values) = 2 * ge_signed_half_weighted_empty_valuesentryvaluedecode + 1 /\ (ge_balance_positive_weighted_empty_valuesentryvalue) = 0) /\ (ge_balance_negative_weighted_empty_valuesentryvalue) = S ge_signed_half_weighted_empty_valuesentryvaluedecode))) /\ ((dst_positive_weighted_empty_values) + ge_balance_negative_weighted_empty_valuesentryvalue = (dst_negative_weighted_empty_values) + ge_balance_positive_weighted_empty_valuesentryvalue))))))))) -> (exists sws_product_table_weighted_empty_result. ((((exists dst_positive_code_weighted_empty_resultproductsleft_table dst_positive_scale_weighted_empty_resultproductsleft_table dst_negative_code_weighted_empty_resultproductsleft_table dst_negative_scale_weighted_empty_resultproductsleft_table. (((W) = (((((dst_positive_code_weighted_empty_resultproductsleft_table) + (dst_positive_scale_weighted_empty_resultproductsleft_table)) * S ((dst_positive_code_weighted_empty_resultproductsleft_table) + (dst_positive_scale_weighted_empty_resultproductsleft_table)) + ((dst_positive_scale_weighted_empty_resultproductsleft_table) + (dst_positive_scale_weighted_empty_resultproductsleft_table))) + (((dst_negative_code_weighted_empty_resultproductsleft_table) + (dst_negative_scale_weighted_empty_resultproductsleft_table)) * S ((dst_negative_code_weighted_empty_resultproductsleft_table) + (dst_negative_scale_weighted_empty_resultproductsleft_table)) + ((dst_negative_scale_weighted_empty_resultproductsleft_table) + (dst_negative_scale_weighted_empty_resultproductsleft_table)))) * S ((((dst_positive_code_weighted_empty_resultproductsleft_table) + (dst_positive_scale_weighted_empty_resultproductsleft_table)) * S ((dst_positive_code_weighted_empty_resultproductsleft_table) + (dst_positive_scale_weighted_empty_resultproductsleft_table)) + ((dst_positive_scale_weighted_empty_resultproductsleft_table) + (dst_positive_scale_weighted_empty_resultproductsleft_table))) + (((dst_negative_code_weighted_empty_resultproductsleft_table) + (dst_negative_scale_weighted_empty_resultproductsleft_table)) * S ((dst_negative_code_weighted_empty_resultproductsleft_table) + (dst_negative_scale_weighted_empty_resultproductsleft_table)) + ((dst_negative_scale_weighted_empty_resultproductsleft_table) + (dst_negative_scale_weighted_empty_resultproductsleft_table)))) + ((((dst_negative_code_weighted_empty_resultproductsleft_table) + (dst_negative_scale_weighted_empty_resultproductsleft_table)) * S ((dst_negative_code_weighted_empty_resultproductsleft_table) + (dst_negative_scale_weighted_empty_resultproductsleft_table)) + ((dst_negative_scale_weighted_empty_resultproductsleft_table) + (dst_negative_scale_weighted_empty_resultproductsleft_table))) + (((dst_negative_code_weighted_empty_resultproductsleft_table) + (dst_negative_scale_weighted_empty_resultproductsleft_table)) * S ((dst_negative_code_weighted_empty_resultproductsleft_table) + (dst_negative_scale_weighted_empty_resultproductsleft_table)) + ((dst_negative_scale_weighted_empty_resultproductsleft_table) + (dst_negative_scale_weighted_empty_resultproductsleft_table)))))) /\ (forall dst_index_weighted_empty_resultproductsleft_table. (exists pvs_le_gap_weighted_empty_resultproductsleft_tabledomain. pvs_le_gap_weighted_empty_resultproductsleft_tabledomain + (dst_index_weighted_empty_resultproductsleft_table) = (0)) -> exists dst_positive_weighted_empty_resultproductsleft_table dst_negative_weighted_empty_resultproductsleft_table dst_value_weighted_empty_resultproductsleft_table. ((((exists ff_h_pvs_weighted_empty_resultproductsleft_tableentrypositive. ff_h_pvs_weighted_empty_resultproductsleft_tableentrypositive + S (dst_positive_weighted_empty_resultproductsleft_table) = S ((S (dst_index_weighted_empty_resultproductsleft_table)) * dst_positive_scale_weighted_empty_resultproductsleft_table)) /\ exists ff_q_pvs_weighted_empty_resultproductsleft_tableentrypositive. dst_positive_code_weighted_empty_resultproductsleft_table = ff_q_pvs_weighted_empty_resultproductsleft_tableentrypositive * S ((S (dst_index_weighted_empty_resultproductsleft_table)) * dst_positive_scale_weighted_empty_resultproductsleft_table) + (dst_positive_weighted_empty_resultproductsleft_table))) /\ (((((exists ff_h_pvs_weighted_empty_resultproductsleft_tableentrynegative. ff_h_pvs_weighted_empty_resultproductsleft_tableentrynegative + S (dst_negative_weighted_empty_resultproductsleft_table) = S ((S (dst_index_weighted_empty_resultproductsleft_table)) * dst_negative_scale_weighted_empty_resultproductsleft_table)) /\ exists ff_q_pvs_weighted_empty_resultproductsleft_tableentrynegative. dst_negative_code_weighted_empty_resultproductsleft_table = ff_q_pvs_weighted_empty_resultproductsleft_tableentrynegative * S ((S (dst_index_weighted_empty_resultproductsleft_table)) * dst_negative_scale_weighted_empty_resultproductsleft_table) + (dst_negative_weighted_empty_resultproductsleft_table))) /\ (exists ge_balance_positive_weighted_empty_resultproductsleft_tableentryvalue ge_balance_negative_weighted_empty_resultproductsleft_tableentryvalue. (((((dst_value_weighted_empty_resultproductsleft_table) = 2 * (ge_balance_positive_weighted_empty_resultproductsleft_tableentryvalue) /\ (ge_balance_negative_weighted_empty_resultproductsleft_tableentryvalue) = 0) \/ exists ge_signed_half_weighted_empty_resultproductsleft_tableentryvaluedecode. (((dst_value_weighted_empty_resultproductsleft_table) = 2 * ge_signed_half_weighted_empty_resultproductsleft_tableentryvaluedecode + 1 /\ (ge_balance_positive_weighted_empty_resultproductsleft_tableentryvalue) = 0) /\ (ge_balance_negative_weighted_empty_resultproductsleft_tableentryvalue) = S ge_signed_half_weighted_empty_resultproductsleft_tableentryvaluedecode))) /\ ((dst_positive_weighted_empty_resultproductsleft_table) + ge_balance_negative_weighted_empty_resultproductsleft_tableentryvalue = (dst_negative_weighted_empty_resultproductsleft_table) + ge_balance_positive_weighted_empty_resultproductsleft_tableentryvalue))))))))) /\ (((exists dst_positive_code_weighted_empty_resultproductsright_table dst_positive_scale_weighted_empty_resultproductsright_table dst_negative_code_weighted_empty_resultproductsright_table dst_negative_scale_weighted_empty_resultproductsright_table. (((F) = (((((dst_positive_code_weighted_empty_resultproductsright_table) + (dst_positive_scale_weighted_empty_resultproductsright_table)) * S ((dst_positive_code_weighted_empty_resultproductsright_table) + (dst_positive_scale_weighted_empty_resultproductsright_table)) + ((dst_positive_scale_weighted_empty_resultproductsright_table) + (dst_positive_scale_weighted_empty_resultproductsright_table))) + (((dst_negative_code_weighted_empty_resultproductsright_table) + (dst_negative_scale_weighted_empty_resultproductsright_table)) * S ((dst_negative_code_weighted_empty_resultproductsright_table) + (dst_negative_scale_weighted_empty_resultproductsright_table)) + ((dst_negative_scale_weighted_empty_resultproductsright_table) + (dst_negative_scale_weighted_empty_resultproductsright_table)))) * S ((((dst_positive_code_weighted_empty_resultproductsright_table) + (dst_positive_scale_weighted_empty_resultproductsright_table)) * S ((dst_positive_code_weighted_empty_resultproductsright_table) + (dst_positive_scale_weighted_empty_resultproductsright_table)) + ((dst_positive_scale_weighted_empty_resultproductsright_table) + (dst_positive_scale_weighted_empty_resultproductsright_table))) + (((dst_negative_code_weighted_empty_resultproductsright_table) + (dst_negative_scale_weighted_empty_resultproductsright_table)) * S ((dst_negative_code_weighted_empty_resultproductsright_table) + (dst_negative_scale_weighted_empty_resultproductsright_table)) + ((dst_negative_scale_weighted_empty_resultproductsright_table) + (dst_negative_scale_weighted_empty_resultproductsright_table)))) + ((((dst_negative_code_weighted_empty_resultproductsright_table) + (dst_negative_scale_weighted_empty_resultproductsright_table)) * S ((dst_negative_code_weighted_empty_resultproductsright_table) + (dst_negative_scale_weighted_empty_resultproductsright_table)) + ((dst_negative_scale_weighted_empty_resultproductsright_table) + (dst_negative_scale_weighted_empty_resultproductsright_table))) + (((dst_negative_code_weighted_empty_resultproductsright_table) + (dst_negative_scale_weighted_empty_resultproductsright_table)) * S ((dst_negative_code_weighted_empty_resultproductsright_table) + (dst_negative_scale_weighted_empty_resultproductsright_table)) + ((dst_negative_scale_weighted_empty_resultproductsright_table) + (dst_negative_scale_weighted_empty_resultproductsright_table)))))) /\ (forall dst_index_weighted_empty_resultproductsright_table. (exists pvs_le_gap_weighted_empty_resultproductsright_tabledomain. pvs_le_gap_weighted_empty_resultproductsright_tabledomain + (dst_index_weighted_empty_resultproductsright_table) = (0)) -> exists dst_positive_weighted_empty_resultproductsright_table dst_negative_weighted_empty_resultproductsright_table dst_value_weighted_empty_resultproductsright_table. ((((exists ff_h_pvs_weighted_empty_resultproductsright_tableentrypositive. ff_h_pvs_weighted_empty_resultproductsright_tableentrypositive + S (dst_positive_weighted_empty_resultproductsright_table) = S ((S (dst_index_weighted_empty_resultproductsright_table)) * dst_positive_scale_weighted_empty_resultproductsright_table)) /\ exists ff_q_pvs_weighted_empty_resultproductsright_tableentrypositive. dst_positive_code_weighted_empty_resultproductsright_table = ff_q_pvs_weighted_empty_resultproductsright_tableentrypositive * S ((S (dst_index_weighted_empty_resultproductsright_table)) * dst_positive_scale_weighted_empty_resultproductsright_table) + (dst_positive_weighted_empty_resultproductsright_table))) /\ (((((exists ff_h_pvs_weighted_empty_resultproductsright_tableentrynegative. ff_h_pvs_weighted_empty_resultproductsright_tableentrynegative + S (dst_negative_weighted_empty_resultproductsright_table) = S ((S (dst_index_weighted_empty_resultproductsright_table)) * dst_negative_scale_weighted_empty_resultproductsright_table)) /\ exists ff_q_pvs_weighted_empty_resultproductsright_tableentrynegative. dst_negative_code_weighted_empty_resultproductsright_table = ff_q_pvs_weighted_empty_resultproductsright_tableentrynegative * S ((S (dst_index_weighted_empty_resultproductsright_table)) * dst_negative_scale_weighted_empty_resultproductsright_table) + (dst_negative_weighted_empty_resultproductsright_table))) /\ (exists ge_balance_positive_weighted_empty_resultproductsright_tableentryvalue ge_balance_negative_weighted_empty_resultproductsright_tableentryvalue. (((((dst_value_weighted_empty_resultproductsright_table) = 2 * (ge_balance_positive_weighted_empty_resultproductsright_tableentryvalue) /\ (ge_balance_negative_weighted_empty_resultproductsright_tableentryvalue) = 0) \/ exists ge_signed_half_weighted_empty_resultproductsright_tableentryvaluedecode. (((dst_value_weighted_empty_resultproductsright_table) = 2 * ge_signed_half_weighted_empty_resultproductsright_tableentryvaluedecode + 1 /\ (ge_balance_positive_weighted_empty_resultproductsright_tableentryvalue) = 0) /\ (ge_balance_negative_weighted_empty_resultproductsright_tableentryvalue) = S ge_signed_half_weighted_empty_resultproductsright_tableentryvaluedecode))) /\ ((dst_positive_weighted_empty_resultproductsright_table) + ge_balance_negative_weighted_empty_resultproductsright_tableentryvalue = (dst_negative_weighted_empty_resultproductsright_table) + ge_balance_positive_weighted_empty_resultproductsright_tableentryvalue))))))))) /\ (((exists dst_positive_code_weighted_empty_resultproductsoutput_table dst_positive_scale_weighted_empty_resultproductsoutput_table dst_negative_code_weighted_empty_resultproductsoutput_table dst_negative_scale_weighted_empty_resultproductsoutput_table. (((sws_product_table_weighted_empty_result) = (((((dst_positive_code_weighted_empty_resultproductsoutput_table) + (dst_positive_scale_weighted_empty_resultproductsoutput_table)) * S ((dst_positive_code_weighted_empty_resultproductsoutput_table) + (dst_positive_scale_weighted_empty_resultproductsoutput_table)) + ((dst_positive_scale_weighted_empty_resultproductsoutput_table) + (dst_positive_scale_weighted_empty_resultproductsoutput_table))) + (((dst_negative_code_weighted_empty_resultproductsoutput_table) + (dst_negative_scale_weighted_empty_resultproductsoutput_table)) * S ((dst_negative_code_weighted_empty_resultproductsoutput_table) + (dst_negative_scale_weighted_empty_resultproductsoutput_table)) + ((dst_negative_scale_weighted_empty_resultproductsoutput_table) + (dst_negative_scale_weighted_empty_resultproductsoutput_table)))) * S ((((dst_positive_code_weighted_empty_resultproductsoutput_table) + (dst_positive_scale_weighted_empty_resultproductsoutput_table)) * S ((dst_positive_code_weighted_empty_resultproductsoutput_table) + (dst_positive_scale_weighted_empty_resultproductsoutput_table)) + ((dst_positive_scale_weighted_empty_resultproductsoutput_table) + (dst_positive_scale_weighted_empty_resultproductsoutput_table))) + (((dst_negative_code_weighted_empty_resultproductsoutput_table) + (dst_negative_scale_weighted_empty_resultproductsoutput_table)) * S ((dst_negative_code_weighted_empty_resultproductsoutput_table) + (dst_negative_scale_weighted_empty_resultproductsoutput_table)) + ((dst_negative_scale_weighted_empty_resultproductsoutput_table) + (dst_negative_scale_weighted_empty_resultproductsoutput_table)))) + ((((dst_negative_code_weighted_empty_resultproductsoutput_table) + (dst_negative_scale_weighted_empty_resultproductsoutput_table)) * S ((dst_negative_code_weighted_empty_resultproductsoutput_table) + (dst_negative_scale_weighted_empty_resultproductsoutput_table)) + ((dst_negative_scale_weighted_empty_resultproductsoutput_table) + (dst_negative_scale_weighted_empty_resultproductsoutput_table))) + (((dst_negative_code_weighted_empty_resultproductsoutput_table) + (dst_negative_scale_weighted_empty_resultproductsoutput_table)) * S ((dst_negative_code_weighted_empty_resultproductsoutput_table) + (dst_negative_scale_weighted_empty_resultproductsoutput_table)) + ((dst_negative_scale_weighted_empty_resultproductsoutput_table) + (dst_negative_scale_weighted_empty_resultproductsoutput_table)))))) /\ (forall dst_index_weighted_empty_resultproductsoutput_table. (exists pvs_le_gap_weighted_empty_resultproductsoutput_tabledomain. pvs_le_gap_weighted_empty_resultproductsoutput_tabledomain + (dst_index_weighted_empty_resultproductsoutput_table) = (0)) -> exists dst_positive_weighted_empty_resultproductsoutput_table dst_negative_weighted_empty_resultproductsoutput_table dst_value_weighted_empty_resultproductsoutput_table. ((((exists ff_h_pvs_weighted_empty_resultproductsoutput_tableentrypositive. ff_h_pvs_weighted_empty_resultproductsoutput_tableentrypositive + S (dst_positive_weighted_empty_resultproductsoutput_table) = S ((S (dst_index_weighted_empty_resultproductsoutput_table)) * dst_positive_scale_weighted_empty_resultproductsoutput_table)) /\ exists ff_q_pvs_weighted_empty_resultproductsoutput_tableentrypositive. dst_positive_code_weighted_empty_resultproductsoutput_table = ff_q_pvs_weighted_empty_resultproductsoutput_tableentrypositive * S ((S (dst_index_weighted_empty_resultproductsoutput_table)) * dst_positive_scale_weighted_empty_resultproductsoutput_table) + (dst_positive_weighted_empty_resultproductsoutput_table))) /\ (((((exists ff_h_pvs_weighted_empty_resultproductsoutput_tableentrynegative. ff_h_pvs_weighted_empty_resultproductsoutput_tableentrynegative + S (dst_negative_weighted_empty_resultproductsoutput_table) = S ((S (dst_index_weighted_empty_resultproductsoutput_table)) * dst_negative_scale_weighted_empty_resultproductsoutput_table)) /\ exists ff_q_pvs_weighted_empty_resultproductsoutput_tableentrynegative. dst_negative_code_weighted_empty_resultproductsoutput_table = ff_q_pvs_weighted_empty_resultproductsoutput_tableentrynegative * S ((S (dst_index_weighted_empty_resultproductsoutput_table)) * dst_negative_scale_weighted_empty_resultproductsoutput_table) + (dst_negative_weighted_empty_resultproductsoutput_table))) /\ (exists ge_balance_positive_weighted_empty_resultproductsoutput_tableentryvalue ge_balance_negative_weighted_empty_resultproductsoutput_tableentryvalue. (((((dst_value_weighted_empty_resultproductsoutput_table) = 2 * (ge_balance_positive_weighted_empty_resultproductsoutput_tableentryvalue) /\ (ge_balance_negative_weighted_empty_resultproductsoutput_tableentryvalue) = 0) \/ exists ge_signed_half_weighted_empty_resultproductsoutput_tableentryvaluedecode. (((dst_value_weighted_empty_resultproductsoutput_table) = 2 * ge_signed_half_weighted_empty_resultproductsoutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_weighted_empty_resultproductsoutput_tableentryvalue) = 0) /\ (ge_balance_negative_weighted_empty_resultproductsoutput_tableentryvalue) = S ge_signed_half_weighted_empty_resultproductsoutput_tableentryvaluedecode))) /\ ((dst_positive_weighted_empty_resultproductsoutput_table) + ge_balance_negative_weighted_empty_resultproductsoutput_tableentryvalue = (dst_negative_weighted_empty_resultproductsoutput_table) + ge_balance_positive_weighted_empty_resultproductsoutput_tableentryvalue))))))))) /\ (forall sto_index_weighted_empty_resultproductsentries. (exists pvs_gap_weighted_empty_resultproductsentriesbound. pvs_gap_weighted_empty_resultproductsentriesbound + S (sto_index_weighted_empty_resultproductsentries) = (0)) -> exists sto_left_weighted_empty_resultproductsentries sto_right_weighted_empty_resultproductsentries sto_output_weighted_empty_resultproductsentries. ((exists dst_positive_code_weighted_empty_resultproductsentriesentryleft dst_positive_scale_weighted_empty_resultproductsentriesentryleft dst_negative_code_weighted_empty_resultproductsentriesentryleft dst_negative_scale_weighted_empty_resultproductsentriesentryleft dst_positive_weighted_empty_resultproductsentriesentryleft dst_negative_weighted_empty_resultproductsentriesentryleft. (((W) = (((((dst_positive_code_weighted_empty_resultproductsentriesentryleft) + (dst_positive_scale_weighted_empty_resultproductsentriesentryleft)) * S ((dst_positive_code_weighted_empty_resultproductsentriesentryleft) + (dst_positive_scale_weighted_empty_resultproductsentriesentryleft)) + ((dst_positive_scale_weighted_empty_resultproductsentriesentryleft) + (dst_positive_scale_weighted_empty_resultproductsentriesentryleft))) + (((dst_negative_code_weighted_empty_resultproductsentriesentryleft) + (dst_negative_scale_weighted_empty_resultproductsentriesentryleft)) * S ((dst_negative_code_weighted_empty_resultproductsentriesentryleft) + (dst_negative_scale_weighted_empty_resultproductsentriesentryleft)) + ((dst_negative_scale_weighted_empty_resultproductsentriesentryleft) + (dst_negative_scale_weighted_empty_resultproductsentriesentryleft)))) * S ((((dst_positive_code_weighted_empty_resultproductsentriesentryleft) + (dst_positive_scale_weighted_empty_resultproductsentriesentryleft)) * S ((dst_positive_code_weighted_empty_resultproductsentriesentryleft) + (dst_positive_scale_weighted_empty_resultproductsentriesentryleft)) + ((dst_positive_scale_weighted_empty_resultproductsentriesentryleft) + (dst_positive_scale_weighted_empty_resultproductsentriesentryleft))) + (((dst_negative_code_weighted_empty_resultproductsentriesentryleft) + (dst_negative_scale_weighted_empty_resultproductsentriesentryleft)) * S ((dst_negative_code_weighted_empty_resultproductsentriesentryleft) + (dst_negative_scale_weighted_empty_resultproductsentriesentryleft)) + ((dst_negative_scale_weighted_empty_resultproductsentriesentryleft) + (dst_negative_scale_weighted_empty_resultproductsentriesentryleft)))) + ((((dst_negative_code_weighted_empty_resultproductsentriesentryleft) + (dst_negative_scale_weighted_empty_resultproductsentriesentryleft)) * S ((dst_negative_code_weighted_empty_resultproductsentriesentryleft) + (dst_negative_scale_weighted_empty_resultproductsentriesentryleft)) + ((dst_negative_scale_weighted_empty_resultproductsentriesentryleft) + (dst_negative_scale_weighted_empty_resultproductsentriesentryleft))) + (((dst_negative_code_weighted_empty_resultproductsentriesentryleft) + (dst_negative_scale_weighted_empty_resultproductsentriesentryleft)) * S ((dst_negative_code_weighted_empty_resultproductsentriesentryleft) + (dst_negative_scale_weighted_empty_resultproductsentriesentryleft)) + ((dst_negative_scale_weighted_empty_resultproductsentriesentryleft) + (dst_negative_scale_weighted_empty_resultproductsentriesentryleft)))))) /\ (((((exists ff_h_pvs_weighted_empty_resultproductsentriesentryleftpositive. ff_h_pvs_weighted_empty_resultproductsentriesentryleftpositive + S (dst_positive_weighted_empty_resultproductsentriesentryleft) = S ((S (sto_index_weighted_empty_resultproductsentries)) * dst_positive_scale_weighted_empty_resultproductsentriesentryleft)) /\ exists ff_q_pvs_weighted_empty_resultproductsentriesentryleftpositive. dst_positive_code_weighted_empty_resultproductsentriesentryleft = ff_q_pvs_weighted_empty_resultproductsentriesentryleftpositive * S ((S (sto_index_weighted_empty_resultproductsentries)) * dst_positive_scale_weighted_empty_resultproductsentriesentryleft) + (dst_positive_weighted_empty_resultproductsentriesentryleft))) /\ (((((exists ff_h_pvs_weighted_empty_resultproductsentriesentryleftnegative. ff_h_pvs_weighted_empty_resultproductsentriesentryleftnegative + S (dst_negative_weighted_empty_resultproductsentriesentryleft) = S ((S (sto_index_weighted_empty_resultproductsentries)) * dst_negative_scale_weighted_empty_resultproductsentriesentryleft)) /\ exists ff_q_pvs_weighted_empty_resultproductsentriesentryleftnegative. dst_negative_code_weighted_empty_resultproductsentriesentryleft = ff_q_pvs_weighted_empty_resultproductsentriesentryleftnegative * S ((S (sto_index_weighted_empty_resultproductsentries)) * dst_negative_scale_weighted_empty_resultproductsentriesentryleft) + (dst_negative_weighted_empty_resultproductsentriesentryleft))) /\ (exists ge_balance_positive_weighted_empty_resultproductsentriesentryleftvalue ge_balance_negative_weighted_empty_resultproductsentriesentryleftvalue. (((((sto_left_weighted_empty_resultproductsentries) = 2 * (ge_balance_positive_weighted_empty_resultproductsentriesentryleftvalue) /\ (ge_balance_negative_weighted_empty_resultproductsentriesentryleftvalue) = 0) \/ exists ge_signed_half_weighted_empty_resultproductsentriesentryleftvaluedecode. (((sto_left_weighted_empty_resultproductsentries) = 2 * ge_signed_half_weighted_empty_resultproductsentriesentryleftvaluedecode + 1 /\ (ge_balance_positive_weighted_empty_resultproductsentriesentryleftvalue) = 0) /\ (ge_balance_negative_weighted_empty_resultproductsentriesentryleftvalue) = S ge_signed_half_weighted_empty_resultproductsentriesentryleftvaluedecode))) /\ ((dst_positive_weighted_empty_resultproductsentriesentryleft) + ge_balance_negative_weighted_empty_resultproductsentriesentryleftvalue = (dst_negative_weighted_empty_resultproductsentriesentryleft) + ge_balance_positive_weighted_empty_resultproductsentriesentryleftvalue))))))))) /\ (((exists dst_positive_code_weighted_empty_resultproductsentriesentryright dst_positive_scale_weighted_empty_resultproductsentriesentryright dst_negative_code_weighted_empty_resultproductsentriesentryright dst_negative_scale_weighted_empty_resultproductsentriesentryright dst_positive_weighted_empty_resultproductsentriesentryright dst_negative_weighted_empty_resultproductsentriesentryright. (((F) = (((((dst_positive_code_weighted_empty_resultproductsentriesentryright) + (dst_positive_scale_weighted_empty_resultproductsentriesentryright)) * S ((dst_positive_code_weighted_empty_resultproductsentriesentryright) + (dst_positive_scale_weighted_empty_resultproductsentriesentryright)) + ((dst_positive_scale_weighted_empty_resultproductsentriesentryright) + (dst_positive_scale_weighted_empty_resultproductsentriesentryright))) + (((dst_negative_code_weighted_empty_resultproductsentriesentryright) + (dst_negative_scale_weighted_empty_resultproductsentriesentryright)) * S ((dst_negative_code_weighted_empty_resultproductsentriesentryright) + (dst_negative_scale_weighted_empty_resultproductsentriesentryright)) + ((dst_negative_scale_weighted_empty_resultproductsentriesentryright) + (dst_negative_scale_weighted_empty_resultproductsentriesentryright)))) * S ((((dst_positive_code_weighted_empty_resultproductsentriesentryright) + (dst_positive_scale_weighted_empty_resultproductsentriesentryright)) * S ((dst_positive_code_weighted_empty_resultproductsentriesentryright) + (dst_positive_scale_weighted_empty_resultproductsentriesentryright)) + ((dst_positive_scale_weighted_empty_resultproductsentriesentryright) + (dst_positive_scale_weighted_empty_resultproductsentriesentryright))) + (((dst_negative_code_weighted_empty_resultproductsentriesentryright) + (dst_negative_scale_weighted_empty_resultproductsentriesentryright)) * S ((dst_negative_code_weighted_empty_resultproductsentriesentryright) + (dst_negative_scale_weighted_empty_resultproductsentriesentryright)) + ((dst_negative_scale_weighted_empty_resultproductsentriesentryright) + (dst_negative_scale_weighted_empty_resultproductsentriesentryright)))) + ((((dst_negative_code_weighted_empty_resultproductsentriesentryright) + (dst_negative_scale_weighted_empty_resultproductsentriesentryright)) * S ((dst_negative_code_weighted_empty_resultproductsentriesentryright) + (dst_negative_scale_weighted_empty_resultproductsentriesentryright)) + ((dst_negative_scale_weighted_empty_resultproductsentriesentryright) + (dst_negative_scale_weighted_empty_resultproductsentriesentryright))) + (((dst_negative_code_weighted_empty_resultproductsentriesentryright) + (dst_negative_scale_weighted_empty_resultproductsentriesentryright)) * S ((dst_negative_code_weighted_empty_resultproductsentriesentryright) + (dst_negative_scale_weighted_empty_resultproductsentriesentryright)) + ((dst_negative_scale_weighted_empty_resultproductsentriesentryright) + (dst_negative_scale_weighted_empty_resultproductsentriesentryright)))))) /\ (((((exists ff_h_pvs_weighted_empty_resultproductsentriesentryrightpositive. ff_h_pvs_weighted_empty_resultproductsentriesentryrightpositive + S (dst_positive_weighted_empty_resultproductsentriesentryright) = S ((S (sto_index_weighted_empty_resultproductsentries)) * dst_positive_scale_weighted_empty_resultproductsentriesentryright)) /\ exists ff_q_pvs_weighted_empty_resultproductsentriesentryrightpositive. dst_positive_code_weighted_empty_resultproductsentriesentryright = ff_q_pvs_weighted_empty_resultproductsentriesentryrightpositive * S ((S (sto_index_weighted_empty_resultproductsentries)) * dst_positive_scale_weighted_empty_resultproductsentriesentryright) + (dst_positive_weighted_empty_resultproductsentriesentryright))) /\ (((((exists ff_h_pvs_weighted_empty_resultproductsentriesentryrightnegative. ff_h_pvs_weighted_empty_resultproductsentriesentryrightnegative + S (dst_negative_weighted_empty_resultproductsentriesentryright) = S ((S (sto_index_weighted_empty_resultproductsentries)) * dst_negative_scale_weighted_empty_resultproductsentriesentryright)) /\ exists ff_q_pvs_weighted_empty_resultproductsentriesentryrightnegative. dst_negative_code_weighted_empty_resultproductsentriesentryright = ff_q_pvs_weighted_empty_resultproductsentriesentryrightnegative * S ((S (sto_index_weighted_empty_resultproductsentries)) * dst_negative_scale_weighted_empty_resultproductsentriesentryright) + (dst_negative_weighted_empty_resultproductsentriesentryright))) /\ (exists ge_balance_positive_weighted_empty_resultproductsentriesentryrightvalue ge_balance_negative_weighted_empty_resultproductsentriesentryrightvalue. (((((sto_right_weighted_empty_resultproductsentries) = 2 * (ge_balance_positive_weighted_empty_resultproductsentriesentryrightvalue) /\ (ge_balance_negative_weighted_empty_resultproductsentriesentryrightvalue) = 0) \/ exists ge_signed_half_weighted_empty_resultproductsentriesentryrightvaluedecode. (((sto_right_weighted_empty_resultproductsentries) = 2 * ge_signed_half_weighted_empty_resultproductsentriesentryrightvaluedecode + 1 /\ (ge_balance_positive_weighted_empty_resultproductsentriesentryrightvalue) = 0) /\ (ge_balance_negative_weighted_empty_resultproductsentriesentryrightvalue) = S ge_signed_half_weighted_empty_resultproductsentriesentryrightvaluedecode))) /\ ((dst_positive_weighted_empty_resultproductsentriesentryright) + ge_balance_negative_weighted_empty_resultproductsentriesentryrightvalue = (dst_negative_weighted_empty_resultproductsentriesentryright) + ge_balance_positive_weighted_empty_resultproductsentriesentryrightvalue))))))))) /\ (((exists dst_positive_code_weighted_empty_resultproductsentriesentryoutput dst_positive_scale_weighted_empty_resultproductsentriesentryoutput dst_negative_code_weighted_empty_resultproductsentriesentryoutput dst_negative_scale_weighted_empty_resultproductsentriesentryoutput dst_positive_weighted_empty_resultproductsentriesentryoutput dst_negative_weighted_empty_resultproductsentriesentryoutput. (((sws_product_table_weighted_empty_result) = (((((dst_positive_code_weighted_empty_resultproductsentriesentryoutput) + (dst_positive_scale_weighted_empty_resultproductsentriesentryoutput)) * S ((dst_positive_code_weighted_empty_resultproductsentriesentryoutput) + (dst_positive_scale_weighted_empty_resultproductsentriesentryoutput)) + ((dst_positive_scale_weighted_empty_resultproductsentriesentryoutput) + (dst_positive_scale_weighted_empty_resultproductsentriesentryoutput))) + (((dst_negative_code_weighted_empty_resultproductsentriesentryoutput) + (dst_negative_scale_weighted_empty_resultproductsentriesentryoutput)) * S ((dst_negative_code_weighted_empty_resultproductsentriesentryoutput) + (dst_negative_scale_weighted_empty_resultproductsentriesentryoutput)) + ((dst_negative_scale_weighted_empty_resultproductsentriesentryoutput) + (dst_negative_scale_weighted_empty_resultproductsentriesentryoutput)))) * S ((((dst_positive_code_weighted_empty_resultproductsentriesentryoutput) + (dst_positive_scale_weighted_empty_resultproductsentriesentryoutput)) * S ((dst_positive_code_weighted_empty_resultproductsentriesentryoutput) + (dst_positive_scale_weighted_empty_resultproductsentriesentryoutput)) + ((dst_positive_scale_weighted_empty_resultproductsentriesentryoutput) + (dst_positive_scale_weighted_empty_resultproductsentriesentryoutput))) + (((dst_negative_code_weighted_empty_resultproductsentriesentryoutput) + (dst_negative_scale_weighted_empty_resultproductsentriesentryoutput)) * S ((dst_negative_code_weighted_empty_resultproductsentriesentryoutput) + (dst_negative_scale_weighted_empty_resultproductsentriesentryoutput)) + ((dst_negative_scale_weighted_empty_resultproductsentriesentryoutput) + (dst_negative_scale_weighted_empty_resultproductsentriesentryoutput)))) + ((((dst_negative_code_weighted_empty_resultproductsentriesentryoutput) + (dst_negative_scale_weighted_empty_resultproductsentriesentryoutput)) * S ((dst_negative_code_weighted_empty_resultproductsentriesentryoutput) + (dst_negative_scale_weighted_empty_resultproductsentriesentryoutput)) + ((dst_negative_scale_weighted_empty_resultproductsentriesentryoutput) + (dst_negative_scale_weighted_empty_resultproductsentriesentryoutput))) + (((dst_negative_code_weighted_empty_resultproductsentriesentryoutput) + (dst_negative_scale_weighted_empty_resultproductsentriesentryoutput)) * S ((dst_negative_code_weighted_empty_resultproductsentriesentryoutput) + (dst_negative_scale_weighted_empty_resultproductsentriesentryoutput)) + ((dst_negative_scale_weighted_empty_resultproductsentriesentryoutput) + (dst_negative_scale_weighted_empty_resultproductsentriesentryoutput)))))) /\ (((((exists ff_h_pvs_weighted_empty_resultproductsentriesentryoutputpositive. ff_h_pvs_weighted_empty_resultproductsentriesentryoutputpositive + S (dst_positive_weighted_empty_resultproductsentriesentryoutput) = S ((S (sto_index_weighted_empty_resultproductsentries)) * dst_positive_scale_weighted_empty_resultproductsentriesentryoutput)) /\ exists ff_q_pvs_weighted_empty_resultproductsentriesentryoutputpositive. dst_positive_code_weighted_empty_resultproductsentriesentryoutput = ff_q_pvs_weighted_empty_resultproductsentriesentryoutputpositive * S ((S (sto_index_weighted_empty_resultproductsentries)) * dst_positive_scale_weighted_empty_resultproductsentriesentryoutput) + (dst_positive_weighted_empty_resultproductsentriesentryoutput))) /\ (((((exists ff_h_pvs_weighted_empty_resultproductsentriesentryoutputnegative. ff_h_pvs_weighted_empty_resultproductsentriesentryoutputnegative + S (dst_negative_weighted_empty_resultproductsentriesentryoutput) = S ((S (sto_index_weighted_empty_resultproductsentries)) * dst_negative_scale_weighted_empty_resultproductsentriesentryoutput)) /\ exists ff_q_pvs_weighted_empty_resultproductsentriesentryoutputnegative. dst_negative_code_weighted_empty_resultproductsentriesentryoutput = ff_q_pvs_weighted_empty_resultproductsentriesentryoutputnegative * S ((S (sto_index_weighted_empty_resultproductsentries)) * dst_negative_scale_weighted_empty_resultproductsentriesentryoutput) + (dst_negative_weighted_empty_resultproductsentriesentryoutput))) /\ (exists ge_balance_positive_weighted_empty_resultproductsentriesentryoutputvalue ge_balance_negative_weighted_empty_resultproductsentriesentryoutputvalue. (((((sto_output_weighted_empty_resultproductsentries) = 2 * (ge_balance_positive_weighted_empty_resultproductsentriesentryoutputvalue) /\ (ge_balance_negative_weighted_empty_resultproductsentriesentryoutputvalue) = 0) \/ exists ge_signed_half_weighted_empty_resultproductsentriesentryoutputvaluedecode. (((sto_output_weighted_empty_resultproductsentries) = 2 * ge_signed_half_weighted_empty_resultproductsentriesentryoutputvaluedecode + 1 /\ (ge_balance_positive_weighted_empty_resultproductsentriesentryoutputvalue) = 0) /\ (ge_balance_negative_weighted_empty_resultproductsentriesentryoutputvalue) = S ge_signed_half_weighted_empty_resultproductsentriesentryoutputvaluedecode))) /\ ((dst_positive_weighted_empty_resultproductsentriesentryoutput) + ge_balance_negative_weighted_empty_resultproductsentriesentryoutputvalue = (dst_negative_weighted_empty_resultproductsentriesentryoutput) + ge_balance_positive_weighted_empty_resultproductsentriesentryoutputvalue))))))))) /\ (exists sto_ap_weighted_empty_resultproductsentriesentryoperation sto_an_weighted_empty_resultproductsentriesentryoperation sto_bp_weighted_empty_resultproductsentriesentryoperation sto_bn_weighted_empty_resultproductsentriesentryoperation sto_cp_weighted_empty_resultproductsentriesentryoperation sto_cn_weighted_empty_resultproductsentriesentryoperation. (((((sto_left_weighted_empty_resultproductsentries) = 2 * (sto_ap_weighted_empty_resultproductsentriesentryoperation) /\ (sto_an_weighted_empty_resultproductsentriesentryoperation) = 0) \/ exists ge_signed_half_weighted_empty_resultproductsentriesentryoperationleft. (((sto_left_weighted_empty_resultproductsentries) = 2 * ge_signed_half_weighted_empty_resultproductsentriesentryoperationleft + 1 /\ (sto_ap_weighted_empty_resultproductsentriesentryoperation) = 0) /\ (sto_an_weighted_empty_resultproductsentriesentryoperation) = S ge_signed_half_weighted_empty_resultproductsentriesentryoperationleft))) /\ ((((((sto_right_weighted_empty_resultproductsentries) = 2 * (sto_bp_weighted_empty_resultproductsentriesentryoperation) /\ (sto_bn_weighted_empty_resultproductsentriesentryoperation) = 0) \/ exists ge_signed_half_weighted_empty_resultproductsentriesentryoperationright. (((sto_right_weighted_empty_resultproductsentries) = 2 * ge_signed_half_weighted_empty_resultproductsentriesentryoperationright + 1 /\ (sto_bp_weighted_empty_resultproductsentriesentryoperation) = 0) /\ (sto_bn_weighted_empty_resultproductsentriesentryoperation) = S ge_signed_half_weighted_empty_resultproductsentriesentryoperationright))) /\ ((((((sto_output_weighted_empty_resultproductsentries) = 2 * (sto_cp_weighted_empty_resultproductsentriesentryoperation) /\ (sto_cn_weighted_empty_resultproductsentriesentryoperation) = 0) \/ exists ge_signed_half_weighted_empty_resultproductsentriesentryoperationoutput. (((sto_output_weighted_empty_resultproductsentries) = 2 * ge_signed_half_weighted_empty_resultproductsentriesentryoperationoutput + 1 /\ (sto_cp_weighted_empty_resultproductsentriesentryoperation) = 0) /\ (sto_cn_weighted_empty_resultproductsentriesentryoperation) = S ge_signed_half_weighted_empty_resultproductsentriesentryoperationoutput))) /\ ((sto_ap_weighted_empty_resultproductsentriesentryoperation * sto_bp_weighted_empty_resultproductsentriesentryoperation + sto_an_weighted_empty_resultproductsentriesentryoperation * sto_bn_weighted_empty_resultproductsentriesentryoperation) + sto_cn_weighted_empty_resultproductsentriesentryoperation = (sto_ap_weighted_empty_resultproductsentriesentryoperation * sto_bn_weighted_empty_resultproductsentriesentryoperation + sto_an_weighted_empty_resultproductsentriesentryoperation * sto_bp_weighted_empty_resultproductsentriesentryoperation) + sto_cp_weighted_empty_resultproductsentriesentryoperation))))))))))))))))))) /\ (exists dst_positive_code_weighted_empty_resultsum dst_positive_scale_weighted_empty_resultsum dst_negative_code_weighted_empty_resultsum dst_negative_scale_weighted_empty_resultsum dst_positive_sum_weighted_empty_resultsum dst_negative_sum_weighted_empty_resultsum. (((sws_product_table_weighted_empty_result) = (((((dst_positive_code_weighted_empty_resultsum) + (dst_positive_scale_weighted_empty_resultsum)) * S ((dst_positive_code_weighted_empty_resultsum) + (dst_positive_scale_weighted_empty_resultsum)) + ((dst_positive_scale_weighted_empty_resultsum) + (dst_positive_scale_weighted_empty_resultsum))) + (((dst_negative_code_weighted_empty_resultsum) + (dst_negative_scale_weighted_empty_resultsum)) * S ((dst_negative_code_weighted_empty_resultsum) + (dst_negative_scale_weighted_empty_resultsum)) + ((dst_negative_scale_weighted_empty_resultsum) + (dst_negative_scale_weighted_empty_resultsum)))) * S ((((dst_positive_code_weighted_empty_resultsum) + (dst_positive_scale_weighted_empty_resultsum)) * S ((dst_positive_code_weighted_empty_resultsum) + (dst_positive_scale_weighted_empty_resultsum)) + ((dst_positive_scale_weighted_empty_resultsum) + (dst_positive_scale_weighted_empty_resultsum))) + (((dst_negative_code_weighted_empty_resultsum) + (dst_negative_scale_weighted_empty_resultsum)) * S ((dst_negative_code_weighted_empty_resultsum) + (dst_negative_scale_weighted_empty_resultsum)) + ((dst_negative_scale_weighted_empty_resultsum) + (dst_negative_scale_weighted_empty_resultsum)))) + ((((dst_negative_code_weighted_empty_resultsum) + (dst_negative_scale_weighted_empty_resultsum)) * S ((dst_negative_code_weighted_empty_resultsum) + (dst_negative_scale_weighted_empty_resultsum)) + ((dst_negative_scale_weighted_empty_resultsum) + (dst_negative_scale_weighted_empty_resultsum))) + (((dst_negative_code_weighted_empty_resultsum) + (dst_negative_scale_weighted_empty_resultsum)) * S ((dst_negative_code_weighted_empty_resultsum) + (dst_negative_scale_weighted_empty_resultsum)) + ((dst_negative_scale_weighted_empty_resultsum) + (dst_negative_scale_weighted_empty_resultsum)))))) /\ (((exists fs_u_dst_weighted_empty_resultsumpositive fs_v_dst_weighted_empty_resultsumpositive. ((((exists fs_h_dst_weighted_empty_resultsumpositive_body_start. fs_h_dst_weighted_empty_resultsumpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_weighted_empty_resultsumpositive)) /\ exists fs_q_dst_weighted_empty_resultsumpositive_body_start. fs_u_dst_weighted_empty_resultsumpositive = fs_q_dst_weighted_empty_resultsumpositive_body_start * S ((S (0)) * fs_v_dst_weighted_empty_resultsumpositive) + (0))) /\ ((((exists fs_h_dst_weighted_empty_resultsumpositive_body_terminal. fs_h_dst_weighted_empty_resultsumpositive_body_terminal + S (dst_positive_sum_weighted_empty_resultsum) = S ((S (0)) * fs_v_dst_weighted_empty_resultsumpositive)) /\ exists fs_q_dst_weighted_empty_resultsumpositive_body_terminal. fs_u_dst_weighted_empty_resultsumpositive = fs_q_dst_weighted_empty_resultsumpositive_body_terminal * S ((S (0)) * fs_v_dst_weighted_empty_resultsumpositive) + (dst_positive_sum_weighted_empty_resultsum))) /\ forall fs_i_dst_weighted_empty_resultsumpositive_body_steps. (exists fs_lt_dst_weighted_empty_resultsumpositive_body_steps_bound. fs_lt_dst_weighted_empty_resultsumpositive_body_steps_bound + S fs_i_dst_weighted_empty_resultsumpositive_body_steps = 0) -> exists fs_a_dst_weighted_empty_resultsumpositive_body_steps fs_r_dst_weighted_empty_resultsumpositive_body_steps fs_s_dst_weighted_empty_resultsumpositive_body_steps. ((((exists fs_h_dst_weighted_empty_resultsumpositive_body_steps_summand. fs_h_dst_weighted_empty_resultsumpositive_body_steps_summand + S (fs_a_dst_weighted_empty_resultsumpositive_body_steps) = S ((S (fs_i_dst_weighted_empty_resultsumpositive_body_steps)) * dst_positive_scale_weighted_empty_resultsum)) /\ exists fs_q_dst_weighted_empty_resultsumpositive_body_steps_summand. dst_positive_code_weighted_empty_resultsum = fs_q_dst_weighted_empty_resultsumpositive_body_steps_summand * S ((S (fs_i_dst_weighted_empty_resultsumpositive_body_steps)) * dst_positive_scale_weighted_empty_resultsum) + (fs_a_dst_weighted_empty_resultsumpositive_body_steps))) /\ ((((exists fs_h_dst_weighted_empty_resultsumpositive_body_steps_partial. fs_h_dst_weighted_empty_resultsumpositive_body_steps_partial + S (fs_r_dst_weighted_empty_resultsumpositive_body_steps) = S ((S (fs_i_dst_weighted_empty_resultsumpositive_body_steps)) * fs_v_dst_weighted_empty_resultsumpositive)) /\ exists fs_q_dst_weighted_empty_resultsumpositive_body_steps_partial. fs_u_dst_weighted_empty_resultsumpositive = fs_q_dst_weighted_empty_resultsumpositive_body_steps_partial * S ((S (fs_i_dst_weighted_empty_resultsumpositive_body_steps)) * fs_v_dst_weighted_empty_resultsumpositive) + (fs_r_dst_weighted_empty_resultsumpositive_body_steps))) /\ ((((exists fs_h_dst_weighted_empty_resultsumpositive_body_steps_successor. fs_h_dst_weighted_empty_resultsumpositive_body_steps_successor + S (fs_s_dst_weighted_empty_resultsumpositive_body_steps) = S ((S (S fs_i_dst_weighted_empty_resultsumpositive_body_steps)) * fs_v_dst_weighted_empty_resultsumpositive)) /\ exists fs_q_dst_weighted_empty_resultsumpositive_body_steps_successor. fs_u_dst_weighted_empty_resultsumpositive = fs_q_dst_weighted_empty_resultsumpositive_body_steps_successor * S ((S (S fs_i_dst_weighted_empty_resultsumpositive_body_steps)) * fs_v_dst_weighted_empty_resultsumpositive) + (fs_s_dst_weighted_empty_resultsumpositive_body_steps))) /\ fs_s_dst_weighted_empty_resultsumpositive_body_steps = fs_r_dst_weighted_empty_resultsumpositive_body_steps + fs_a_dst_weighted_empty_resultsumpositive_body_steps)))))) /\ (((exists fs_u_dst_weighted_empty_resultsumnegative fs_v_dst_weighted_empty_resultsumnegative. ((((exists fs_h_dst_weighted_empty_resultsumnegative_body_start. fs_h_dst_weighted_empty_resultsumnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_weighted_empty_resultsumnegative)) /\ exists fs_q_dst_weighted_empty_resultsumnegative_body_start. fs_u_dst_weighted_empty_resultsumnegative = fs_q_dst_weighted_empty_resultsumnegative_body_start * S ((S (0)) * fs_v_dst_weighted_empty_resultsumnegative) + (0))) /\ ((((exists fs_h_dst_weighted_empty_resultsumnegative_body_terminal. fs_h_dst_weighted_empty_resultsumnegative_body_terminal + S (dst_negative_sum_weighted_empty_resultsum) = S ((S (0)) * fs_v_dst_weighted_empty_resultsumnegative)) /\ exists fs_q_dst_weighted_empty_resultsumnegative_body_terminal. fs_u_dst_weighted_empty_resultsumnegative = fs_q_dst_weighted_empty_resultsumnegative_body_terminal * S ((S (0)) * fs_v_dst_weighted_empty_resultsumnegative) + (dst_negative_sum_weighted_empty_resultsum))) /\ forall fs_i_dst_weighted_empty_resultsumnegative_body_steps. (exists fs_lt_dst_weighted_empty_resultsumnegative_body_steps_bound. fs_lt_dst_weighted_empty_resultsumnegative_body_steps_bound + S fs_i_dst_weighted_empty_resultsumnegative_body_steps = 0) -> exists fs_a_dst_weighted_empty_resultsumnegative_body_steps fs_r_dst_weighted_empty_resultsumnegative_body_steps fs_s_dst_weighted_empty_resultsumnegative_body_steps. ((((exists fs_h_dst_weighted_empty_resultsumnegative_body_steps_summand. fs_h_dst_weighted_empty_resultsumnegative_body_steps_summand + S (fs_a_dst_weighted_empty_resultsumnegative_body_steps) = S ((S (fs_i_dst_weighted_empty_resultsumnegative_body_steps)) * dst_negative_scale_weighted_empty_resultsum)) /\ exists fs_q_dst_weighted_empty_resultsumnegative_body_steps_summand. dst_negative_code_weighted_empty_resultsum = fs_q_dst_weighted_empty_resultsumnegative_body_steps_summand * S ((S (fs_i_dst_weighted_empty_resultsumnegative_body_steps)) * dst_negative_scale_weighted_empty_resultsum) + (fs_a_dst_weighted_empty_resultsumnegative_body_steps))) /\ ((((exists fs_h_dst_weighted_empty_resultsumnegative_body_steps_partial. fs_h_dst_weighted_empty_resultsumnegative_body_steps_partial + S (fs_r_dst_weighted_empty_resultsumnegative_body_steps) = S ((S (fs_i_dst_weighted_empty_resultsumnegative_body_steps)) * fs_v_dst_weighted_empty_resultsumnegative)) /\ exists fs_q_dst_weighted_empty_resultsumnegative_body_steps_partial. fs_u_dst_weighted_empty_resultsumnegative = fs_q_dst_weighted_empty_resultsumnegative_body_steps_partial * S ((S (fs_i_dst_weighted_empty_resultsumnegative_body_steps)) * fs_v_dst_weighted_empty_resultsumnegative) + (fs_r_dst_weighted_empty_resultsumnegative_body_steps))) /\ ((((exists fs_h_dst_weighted_empty_resultsumnegative_body_steps_successor. fs_h_dst_weighted_empty_resultsumnegative_body_steps_successor + S (fs_s_dst_weighted_empty_resultsumnegative_body_steps) = S ((S (S fs_i_dst_weighted_empty_resultsumnegative_body_steps)) * fs_v_dst_weighted_empty_resultsumnegative)) /\ exists fs_q_dst_weighted_empty_resultsumnegative_body_steps_successor. fs_u_dst_weighted_empty_resultsumnegative = fs_q_dst_weighted_empty_resultsumnegative_body_steps_successor * S ((S (S fs_i_dst_weighted_empty_resultsumnegative_body_steps)) * fs_v_dst_weighted_empty_resultsumnegative) + (fs_s_dst_weighted_empty_resultsumnegative_body_steps))) /\ fs_s_dst_weighted_empty_resultsumnegative_body_steps = fs_r_dst_weighted_empty_resultsumnegative_body_steps + fs_a_dst_weighted_empty_resultsumnegative_body_steps)))))) /\ (exists ge_balance_positive_weighted_empty_resultsumresult ge_balance_negative_weighted_empty_resultsumresult. (((((0) = 2 * (ge_balance_positive_weighted_empty_resultsumresult) /\ (ge_balance_negative_weighted_empty_resultsumresult) = 0) \/ exists ge_signed_half_weighted_empty_resultsumresultdecode. (((0) = 2 * ge_signed_half_weighted_empty_resultsumresultdecode + 1 /\ (ge_balance_positive_weighted_empty_resultsumresult) = 0) /\ (ge_balance_negative_weighted_empty_resultsumresult) = S ge_signed_half_weighted_empty_resultsumresultdecode))) /\ ((dst_positive_sum_weighted_empty_resultsum) + ge_balance_negative_weighted_empty_resultsumresult = (dst_negative_sum_weighted_empty_resultsum) + ge_balance_positive_weighted_empty_resultsumresult)))))))))))