signed_weighted_sum_functional

Exact expanded first-order arithmetic statement

forall W F l a b. (exists sws_product_table_weighted_unique_first. ((((exists dst_positive_code_weighted_unique_firstproductsleft_table dst_positive_scale_weighted_unique_firstproductsleft_table dst_negative_code_weighted_unique_firstproductsleft_table dst_negative_scale_weighted_unique_firstproductsleft_table. (((W) = (((((dst_positive_code_weighted_unique_firstproductsleft_table) + (dst_positive_scale_weighted_unique_firstproductsleft_table)) * S ((dst_positive_code_weighted_unique_firstproductsleft_table) + (dst_positive_scale_weighted_unique_firstproductsleft_table)) + ((dst_positive_scale_weighted_unique_firstproductsleft_table) + (dst_positive_scale_weighted_unique_firstproductsleft_table))) + (((dst_negative_code_weighted_unique_firstproductsleft_table) + (dst_negative_scale_weighted_unique_firstproductsleft_table)) * S ((dst_negative_code_weighted_unique_firstproductsleft_table) + (dst_negative_scale_weighted_unique_firstproductsleft_table)) + ((dst_negative_scale_weighted_unique_firstproductsleft_table) + (dst_negative_scale_weighted_unique_firstproductsleft_table)))) * S ((((dst_positive_code_weighted_unique_firstproductsleft_table) + (dst_positive_scale_weighted_unique_firstproductsleft_table)) * S ((dst_positive_code_weighted_unique_firstproductsleft_table) + (dst_positive_scale_weighted_unique_firstproductsleft_table)) + ((dst_positive_scale_weighted_unique_firstproductsleft_table) + (dst_positive_scale_weighted_unique_firstproductsleft_table))) + (((dst_negative_code_weighted_unique_firstproductsleft_table) + (dst_negative_scale_weighted_unique_firstproductsleft_table)) * S ((dst_negative_code_weighted_unique_firstproductsleft_table) + (dst_negative_scale_weighted_unique_firstproductsleft_table)) + ((dst_negative_scale_weighted_unique_firstproductsleft_table) + (dst_negative_scale_weighted_unique_firstproductsleft_table)))) + ((((dst_negative_code_weighted_unique_firstproductsleft_table) + (dst_negative_scale_weighted_unique_firstproductsleft_table)) * S ((dst_negative_code_weighted_unique_firstproductsleft_table) + (dst_negative_scale_weighted_unique_firstproductsleft_table)) + ((dst_negative_scale_weighted_unique_firstproductsleft_table) + (dst_negative_scale_weighted_unique_firstproductsleft_table))) + (((dst_negative_code_weighted_unique_firstproductsleft_table) + (dst_negative_scale_weighted_unique_firstproductsleft_table)) * S ((dst_negative_code_weighted_unique_firstproductsleft_table) + (dst_negative_scale_weighted_unique_firstproductsleft_table)) + ((dst_negative_scale_weighted_unique_firstproductsleft_table) + (dst_negative_scale_weighted_unique_firstproductsleft_table)))))) /\ (forall dst_index_weighted_unique_firstproductsleft_table. (exists pvs_le_gap_weighted_unique_firstproductsleft_tabledomain. pvs_le_gap_weighted_unique_firstproductsleft_tabledomain + (dst_index_weighted_unique_firstproductsleft_table) = (l)) -> exists dst_positive_weighted_unique_firstproductsleft_table dst_negative_weighted_unique_firstproductsleft_table dst_value_weighted_unique_firstproductsleft_table. ((((exists ff_h_pvs_weighted_unique_firstproductsleft_tableentrypositive. ff_h_pvs_weighted_unique_firstproductsleft_tableentrypositive + S (dst_positive_weighted_unique_firstproductsleft_table) = S ((S (dst_index_weighted_unique_firstproductsleft_table)) * dst_positive_scale_weighted_unique_firstproductsleft_table)) /\ exists ff_q_pvs_weighted_unique_firstproductsleft_tableentrypositive. dst_positive_code_weighted_unique_firstproductsleft_table = ff_q_pvs_weighted_unique_firstproductsleft_tableentrypositive * S ((S (dst_index_weighted_unique_firstproductsleft_table)) * dst_positive_scale_weighted_unique_firstproductsleft_table) + (dst_positive_weighted_unique_firstproductsleft_table))) /\ (((((exists ff_h_pvs_weighted_unique_firstproductsleft_tableentrynegative. ff_h_pvs_weighted_unique_firstproductsleft_tableentrynegative + S (dst_negative_weighted_unique_firstproductsleft_table) = S ((S (dst_index_weighted_unique_firstproductsleft_table)) * dst_negative_scale_weighted_unique_firstproductsleft_table)) /\ exists ff_q_pvs_weighted_unique_firstproductsleft_tableentrynegative. dst_negative_code_weighted_unique_firstproductsleft_table = ff_q_pvs_weighted_unique_firstproductsleft_tableentrynegative * S ((S (dst_index_weighted_unique_firstproductsleft_table)) * dst_negative_scale_weighted_unique_firstproductsleft_table) + (dst_negative_weighted_unique_firstproductsleft_table))) /\ (exists ge_balance_positive_weighted_unique_firstproductsleft_tableentryvalue ge_balance_negative_weighted_unique_firstproductsleft_tableentryvalue. (((((dst_value_weighted_unique_firstproductsleft_table) = 2 * (ge_balance_positive_weighted_unique_firstproductsleft_tableentryvalue) /\ (ge_balance_negative_weighted_unique_firstproductsleft_tableentryvalue) = 0) \/ exists ge_signed_half_weighted_unique_firstproductsleft_tableentryvaluedecode. (((dst_value_weighted_unique_firstproductsleft_table) = 2 * ge_signed_half_weighted_unique_firstproductsleft_tableentryvaluedecode + 1 /\ (ge_balance_positive_weighted_unique_firstproductsleft_tableentryvalue) = 0) /\ (ge_balance_negative_weighted_unique_firstproductsleft_tableentryvalue) = S ge_signed_half_weighted_unique_firstproductsleft_tableentryvaluedecode))) /\ ((dst_positive_weighted_unique_firstproductsleft_table) + ge_balance_negative_weighted_unique_firstproductsleft_tableentryvalue = (dst_negative_weighted_unique_firstproductsleft_table) + ge_balance_positive_weighted_unique_firstproductsleft_tableentryvalue))))))))) /\ (((exists dst_positive_code_weighted_unique_firstproductsright_table dst_positive_scale_weighted_unique_firstproductsright_table dst_negative_code_weighted_unique_firstproductsright_table dst_negative_scale_weighted_unique_firstproductsright_table. (((F) = (((((dst_positive_code_weighted_unique_firstproductsright_table) + (dst_positive_scale_weighted_unique_firstproductsright_table)) * S ((dst_positive_code_weighted_unique_firstproductsright_table) + (dst_positive_scale_weighted_unique_firstproductsright_table)) + ((dst_positive_scale_weighted_unique_firstproductsright_table) + (dst_positive_scale_weighted_unique_firstproductsright_table))) + (((dst_negative_code_weighted_unique_firstproductsright_table) + (dst_negative_scale_weighted_unique_firstproductsright_table)) * S ((dst_negative_code_weighted_unique_firstproductsright_table) + (dst_negative_scale_weighted_unique_firstproductsright_table)) + ((dst_negative_scale_weighted_unique_firstproductsright_table) + (dst_negative_scale_weighted_unique_firstproductsright_table)))) * S ((((dst_positive_code_weighted_unique_firstproductsright_table) + (dst_positive_scale_weighted_unique_firstproductsright_table)) * S ((dst_positive_code_weighted_unique_firstproductsright_table) + (dst_positive_scale_weighted_unique_firstproductsright_table)) + ((dst_positive_scale_weighted_unique_firstproductsright_table) + (dst_positive_scale_weighted_unique_firstproductsright_table))) + (((dst_negative_code_weighted_unique_firstproductsright_table) + (dst_negative_scale_weighted_unique_firstproductsright_table)) * S ((dst_negative_code_weighted_unique_firstproductsright_table) + (dst_negative_scale_weighted_unique_firstproductsright_table)) + ((dst_negative_scale_weighted_unique_firstproductsright_table) + (dst_negative_scale_weighted_unique_firstproductsright_table)))) + ((((dst_negative_code_weighted_unique_firstproductsright_table) + (dst_negative_scale_weighted_unique_firstproductsright_table)) * S ((dst_negative_code_weighted_unique_firstproductsright_table) + (dst_negative_scale_weighted_unique_firstproductsright_table)) + ((dst_negative_scale_weighted_unique_firstproductsright_table) + (dst_negative_scale_weighted_unique_firstproductsright_table))) + (((dst_negative_code_weighted_unique_firstproductsright_table) + (dst_negative_scale_weighted_unique_firstproductsright_table)) * S ((dst_negative_code_weighted_unique_firstproductsright_table) + (dst_negative_scale_weighted_unique_firstproductsright_table)) + ((dst_negative_scale_weighted_unique_firstproductsright_table) + (dst_negative_scale_weighted_unique_firstproductsright_table)))))) /\ (forall dst_index_weighted_unique_firstproductsright_table. (exists pvs_le_gap_weighted_unique_firstproductsright_tabledomain. pvs_le_gap_weighted_unique_firstproductsright_tabledomain + (dst_index_weighted_unique_firstproductsright_table) = (l)) -> exists dst_positive_weighted_unique_firstproductsright_table dst_negative_weighted_unique_firstproductsright_table dst_value_weighted_unique_firstproductsright_table. ((((exists ff_h_pvs_weighted_unique_firstproductsright_tableentrypositive. ff_h_pvs_weighted_unique_firstproductsright_tableentrypositive + S (dst_positive_weighted_unique_firstproductsright_table) = S ((S (dst_index_weighted_unique_firstproductsright_table)) * dst_positive_scale_weighted_unique_firstproductsright_table)) /\ exists ff_q_pvs_weighted_unique_firstproductsright_tableentrypositive. dst_positive_code_weighted_unique_firstproductsright_table = ff_q_pvs_weighted_unique_firstproductsright_tableentrypositive * S ((S (dst_index_weighted_unique_firstproductsright_table)) * dst_positive_scale_weighted_unique_firstproductsright_table) + (dst_positive_weighted_unique_firstproductsright_table))) /\ (((((exists ff_h_pvs_weighted_unique_firstproductsright_tableentrynegative. ff_h_pvs_weighted_unique_firstproductsright_tableentrynegative + S (dst_negative_weighted_unique_firstproductsright_table) = S ((S (dst_index_weighted_unique_firstproductsright_table)) * dst_negative_scale_weighted_unique_firstproductsright_table)) /\ exists ff_q_pvs_weighted_unique_firstproductsright_tableentrynegative. dst_negative_code_weighted_unique_firstproductsright_table = ff_q_pvs_weighted_unique_firstproductsright_tableentrynegative * S ((S (dst_index_weighted_unique_firstproductsright_table)) * dst_negative_scale_weighted_unique_firstproductsright_table) + (dst_negative_weighted_unique_firstproductsright_table))) /\ (exists ge_balance_positive_weighted_unique_firstproductsright_tableentryvalue ge_balance_negative_weighted_unique_firstproductsright_tableentryvalue. (((((dst_value_weighted_unique_firstproductsright_table) = 2 * (ge_balance_positive_weighted_unique_firstproductsright_tableentryvalue) /\ (ge_balance_negative_weighted_unique_firstproductsright_tableentryvalue) = 0) \/ exists ge_signed_half_weighted_unique_firstproductsright_tableentryvaluedecode. (((dst_value_weighted_unique_firstproductsright_table) = 2 * ge_signed_half_weighted_unique_firstproductsright_tableentryvaluedecode + 1 /\ (ge_balance_positive_weighted_unique_firstproductsright_tableentryvalue) = 0) /\ (ge_balance_negative_weighted_unique_firstproductsright_tableentryvalue) = S ge_signed_half_weighted_unique_firstproductsright_tableentryvaluedecode))) /\ ((dst_positive_weighted_unique_firstproductsright_table) + ge_balance_negative_weighted_unique_firstproductsright_tableentryvalue = (dst_negative_weighted_unique_firstproductsright_table) + ge_balance_positive_weighted_unique_firstproductsright_tableentryvalue))))))))) /\ (((exists dst_positive_code_weighted_unique_firstproductsoutput_table dst_positive_scale_weighted_unique_firstproductsoutput_table dst_negative_code_weighted_unique_firstproductsoutput_table dst_negative_scale_weighted_unique_firstproductsoutput_table. (((sws_product_table_weighted_unique_first) = (((((dst_positive_code_weighted_unique_firstproductsoutput_table) + (dst_positive_scale_weighted_unique_firstproductsoutput_table)) * S ((dst_positive_code_weighted_unique_firstproductsoutput_table) + (dst_positive_scale_weighted_unique_firstproductsoutput_table)) + ((dst_positive_scale_weighted_unique_firstproductsoutput_table) + (dst_positive_scale_weighted_unique_firstproductsoutput_table))) + (((dst_negative_code_weighted_unique_firstproductsoutput_table) + (dst_negative_scale_weighted_unique_firstproductsoutput_table)) * S ((dst_negative_code_weighted_unique_firstproductsoutput_table) + (dst_negative_scale_weighted_unique_firstproductsoutput_table)) + ((dst_negative_scale_weighted_unique_firstproductsoutput_table) + (dst_negative_scale_weighted_unique_firstproductsoutput_table)))) * S ((((dst_positive_code_weighted_unique_firstproductsoutput_table) + (dst_positive_scale_weighted_unique_firstproductsoutput_table)) * S ((dst_positive_code_weighted_unique_firstproductsoutput_table) + (dst_positive_scale_weighted_unique_firstproductsoutput_table)) + ((dst_positive_scale_weighted_unique_firstproductsoutput_table) + (dst_positive_scale_weighted_unique_firstproductsoutput_table))) + (((dst_negative_code_weighted_unique_firstproductsoutput_table) + (dst_negative_scale_weighted_unique_firstproductsoutput_table)) * S ((dst_negative_code_weighted_unique_firstproductsoutput_table) + (dst_negative_scale_weighted_unique_firstproductsoutput_table)) + ((dst_negative_scale_weighted_unique_firstproductsoutput_table) + (dst_negative_scale_weighted_unique_firstproductsoutput_table)))) + ((((dst_negative_code_weighted_unique_firstproductsoutput_table) + (dst_negative_scale_weighted_unique_firstproductsoutput_table)) * S ((dst_negative_code_weighted_unique_firstproductsoutput_table) + (dst_negative_scale_weighted_unique_firstproductsoutput_table)) + ((dst_negative_scale_weighted_unique_firstproductsoutput_table) + (dst_negative_scale_weighted_unique_firstproductsoutput_table))) + (((dst_negative_code_weighted_unique_firstproductsoutput_table) + (dst_negative_scale_weighted_unique_firstproductsoutput_table)) * S ((dst_negative_code_weighted_unique_firstproductsoutput_table) + (dst_negative_scale_weighted_unique_firstproductsoutput_table)) + ((dst_negative_scale_weighted_unique_firstproductsoutput_table) + (dst_negative_scale_weighted_unique_firstproductsoutput_table)))))) /\ (forall dst_index_weighted_unique_firstproductsoutput_table. (exists pvs_le_gap_weighted_unique_firstproductsoutput_tabledomain. pvs_le_gap_weighted_unique_firstproductsoutput_tabledomain + (dst_index_weighted_unique_firstproductsoutput_table) = (l)) -> exists dst_positive_weighted_unique_firstproductsoutput_table dst_negative_weighted_unique_firstproductsoutput_table dst_value_weighted_unique_firstproductsoutput_table. ((((exists ff_h_pvs_weighted_unique_firstproductsoutput_tableentrypositive. ff_h_pvs_weighted_unique_firstproductsoutput_tableentrypositive + S (dst_positive_weighted_unique_firstproductsoutput_table) = S ((S (dst_index_weighted_unique_firstproductsoutput_table)) * dst_positive_scale_weighted_unique_firstproductsoutput_table)) /\ exists ff_q_pvs_weighted_unique_firstproductsoutput_tableentrypositive. dst_positive_code_weighted_unique_firstproductsoutput_table = ff_q_pvs_weighted_unique_firstproductsoutput_tableentrypositive * S ((S (dst_index_weighted_unique_firstproductsoutput_table)) * dst_positive_scale_weighted_unique_firstproductsoutput_table) + (dst_positive_weighted_unique_firstproductsoutput_table))) /\ (((((exists ff_h_pvs_weighted_unique_firstproductsoutput_tableentrynegative. ff_h_pvs_weighted_unique_firstproductsoutput_tableentrynegative + S (dst_negative_weighted_unique_firstproductsoutput_table) = S ((S (dst_index_weighted_unique_firstproductsoutput_table)) * dst_negative_scale_weighted_unique_firstproductsoutput_table)) /\ exists ff_q_pvs_weighted_unique_firstproductsoutput_tableentrynegative. dst_negative_code_weighted_unique_firstproductsoutput_table = ff_q_pvs_weighted_unique_firstproductsoutput_tableentrynegative * S ((S (dst_index_weighted_unique_firstproductsoutput_table)) * dst_negative_scale_weighted_unique_firstproductsoutput_table) + (dst_negative_weighted_unique_firstproductsoutput_table))) /\ (exists ge_balance_positive_weighted_unique_firstproductsoutput_tableentryvalue ge_balance_negative_weighted_unique_firstproductsoutput_tableentryvalue. (((((dst_value_weighted_unique_firstproductsoutput_table) = 2 * (ge_balance_positive_weighted_unique_firstproductsoutput_tableentryvalue) /\ (ge_balance_negative_weighted_unique_firstproductsoutput_tableentryvalue) = 0) \/ exists ge_signed_half_weighted_unique_firstproductsoutput_tableentryvaluedecode. (((dst_value_weighted_unique_firstproductsoutput_table) = 2 * ge_signed_half_weighted_unique_firstproductsoutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_weighted_unique_firstproductsoutput_tableentryvalue) = 0) /\ (ge_balance_negative_weighted_unique_firstproductsoutput_tableentryvalue) = S ge_signed_half_weighted_unique_firstproductsoutput_tableentryvaluedecode))) /\ ((dst_positive_weighted_unique_firstproductsoutput_table) + ge_balance_negative_weighted_unique_firstproductsoutput_tableentryvalue = (dst_negative_weighted_unique_firstproductsoutput_table) + ge_balance_positive_weighted_unique_firstproductsoutput_tableentryvalue))))))))) /\ (forall sto_index_weighted_unique_firstproductsentries. (exists pvs_gap_weighted_unique_firstproductsentriesbound. pvs_gap_weighted_unique_firstproductsentriesbound + S (sto_index_weighted_unique_firstproductsentries) = (l)) -> exists sto_left_weighted_unique_firstproductsentries sto_right_weighted_unique_firstproductsentries sto_output_weighted_unique_firstproductsentries. ((exists dst_positive_code_weighted_unique_firstproductsentriesentryleft dst_positive_scale_weighted_unique_firstproductsentriesentryleft dst_negative_code_weighted_unique_firstproductsentriesentryleft dst_negative_scale_weighted_unique_firstproductsentriesentryleft dst_positive_weighted_unique_firstproductsentriesentryleft dst_negative_weighted_unique_firstproductsentriesentryleft. (((W) = (((((dst_positive_code_weighted_unique_firstproductsentriesentryleft) + (dst_positive_scale_weighted_unique_firstproductsentriesentryleft)) * S ((dst_positive_code_weighted_unique_firstproductsentriesentryleft) + (dst_positive_scale_weighted_unique_firstproductsentriesentryleft)) + ((dst_positive_scale_weighted_unique_firstproductsentriesentryleft) + (dst_positive_scale_weighted_unique_firstproductsentriesentryleft))) + (((dst_negative_code_weighted_unique_firstproductsentriesentryleft) + (dst_negative_scale_weighted_unique_firstproductsentriesentryleft)) * S ((dst_negative_code_weighted_unique_firstproductsentriesentryleft) + (dst_negative_scale_weighted_unique_firstproductsentriesentryleft)) + ((dst_negative_scale_weighted_unique_firstproductsentriesentryleft) + (dst_negative_scale_weighted_unique_firstproductsentriesentryleft)))) * S ((((dst_positive_code_weighted_unique_firstproductsentriesentryleft) + (dst_positive_scale_weighted_unique_firstproductsentriesentryleft)) * S ((dst_positive_code_weighted_unique_firstproductsentriesentryleft) + (dst_positive_scale_weighted_unique_firstproductsentriesentryleft)) + ((dst_positive_scale_weighted_unique_firstproductsentriesentryleft) + (dst_positive_scale_weighted_unique_firstproductsentriesentryleft))) + (((dst_negative_code_weighted_unique_firstproductsentriesentryleft) + (dst_negative_scale_weighted_unique_firstproductsentriesentryleft)) * S ((dst_negative_code_weighted_unique_firstproductsentriesentryleft) + (dst_negative_scale_weighted_unique_firstproductsentriesentryleft)) + ((dst_negative_scale_weighted_unique_firstproductsentriesentryleft) + (dst_negative_scale_weighted_unique_firstproductsentriesentryleft)))) + ((((dst_negative_code_weighted_unique_firstproductsentriesentryleft) + (dst_negative_scale_weighted_unique_firstproductsentriesentryleft)) * S ((dst_negative_code_weighted_unique_firstproductsentriesentryleft) + (dst_negative_scale_weighted_unique_firstproductsentriesentryleft)) + ((dst_negative_scale_weighted_unique_firstproductsentriesentryleft) + (dst_negative_scale_weighted_unique_firstproductsentriesentryleft))) + (((dst_negative_code_weighted_unique_firstproductsentriesentryleft) + (dst_negative_scale_weighted_unique_firstproductsentriesentryleft)) * S ((dst_negative_code_weighted_unique_firstproductsentriesentryleft) + (dst_negative_scale_weighted_unique_firstproductsentriesentryleft)) + ((dst_negative_scale_weighted_unique_firstproductsentriesentryleft) + (dst_negative_scale_weighted_unique_firstproductsentriesentryleft)))))) /\ (((((exists ff_h_pvs_weighted_unique_firstproductsentriesentryleftpositive. ff_h_pvs_weighted_unique_firstproductsentriesentryleftpositive + S (dst_positive_weighted_unique_firstproductsentriesentryleft) = S ((S (sto_index_weighted_unique_firstproductsentries)) * dst_positive_scale_weighted_unique_firstproductsentriesentryleft)) /\ exists ff_q_pvs_weighted_unique_firstproductsentriesentryleftpositive. dst_positive_code_weighted_unique_firstproductsentriesentryleft = ff_q_pvs_weighted_unique_firstproductsentriesentryleftpositive * S ((S (sto_index_weighted_unique_firstproductsentries)) * dst_positive_scale_weighted_unique_firstproductsentriesentryleft) + (dst_positive_weighted_unique_firstproductsentriesentryleft))) /\ (((((exists ff_h_pvs_weighted_unique_firstproductsentriesentryleftnegative. ff_h_pvs_weighted_unique_firstproductsentriesentryleftnegative + S (dst_negative_weighted_unique_firstproductsentriesentryleft) = S ((S (sto_index_weighted_unique_firstproductsentries)) * dst_negative_scale_weighted_unique_firstproductsentriesentryleft)) /\ exists ff_q_pvs_weighted_unique_firstproductsentriesentryleftnegative. dst_negative_code_weighted_unique_firstproductsentriesentryleft = ff_q_pvs_weighted_unique_firstproductsentriesentryleftnegative * S ((S (sto_index_weighted_unique_firstproductsentries)) * dst_negative_scale_weighted_unique_firstproductsentriesentryleft) + (dst_negative_weighted_unique_firstproductsentriesentryleft))) /\ (exists ge_balance_positive_weighted_unique_firstproductsentriesentryleftvalue ge_balance_negative_weighted_unique_firstproductsentriesentryleftvalue. (((((sto_left_weighted_unique_firstproductsentries) = 2 * (ge_balance_positive_weighted_unique_firstproductsentriesentryleftvalue) /\ (ge_balance_negative_weighted_unique_firstproductsentriesentryleftvalue) = 0) \/ exists ge_signed_half_weighted_unique_firstproductsentriesentryleftvaluedecode. (((sto_left_weighted_unique_firstproductsentries) = 2 * ge_signed_half_weighted_unique_firstproductsentriesentryleftvaluedecode + 1 /\ (ge_balance_positive_weighted_unique_firstproductsentriesentryleftvalue) = 0) /\ (ge_balance_negative_weighted_unique_firstproductsentriesentryleftvalue) = S ge_signed_half_weighted_unique_firstproductsentriesentryleftvaluedecode))) /\ ((dst_positive_weighted_unique_firstproductsentriesentryleft) + ge_balance_negative_weighted_unique_firstproductsentriesentryleftvalue = (dst_negative_weighted_unique_firstproductsentriesentryleft) + ge_balance_positive_weighted_unique_firstproductsentriesentryleftvalue))))))))) /\ (((exists dst_positive_code_weighted_unique_firstproductsentriesentryright dst_positive_scale_weighted_unique_firstproductsentriesentryright dst_negative_code_weighted_unique_firstproductsentriesentryright dst_negative_scale_weighted_unique_firstproductsentriesentryright dst_positive_weighted_unique_firstproductsentriesentryright dst_negative_weighted_unique_firstproductsentriesentryright. (((F) = (((((dst_positive_code_weighted_unique_firstproductsentriesentryright) + (dst_positive_scale_weighted_unique_firstproductsentriesentryright)) * S ((dst_positive_code_weighted_unique_firstproductsentriesentryright) + (dst_positive_scale_weighted_unique_firstproductsentriesentryright)) + ((dst_positive_scale_weighted_unique_firstproductsentriesentryright) + (dst_positive_scale_weighted_unique_firstproductsentriesentryright))) + (((dst_negative_code_weighted_unique_firstproductsentriesentryright) + (dst_negative_scale_weighted_unique_firstproductsentriesentryright)) * S ((dst_negative_code_weighted_unique_firstproductsentriesentryright) + (dst_negative_scale_weighted_unique_firstproductsentriesentryright)) + ((dst_negative_scale_weighted_unique_firstproductsentriesentryright) + (dst_negative_scale_weighted_unique_firstproductsentriesentryright)))) * S ((((dst_positive_code_weighted_unique_firstproductsentriesentryright) + (dst_positive_scale_weighted_unique_firstproductsentriesentryright)) * S ((dst_positive_code_weighted_unique_firstproductsentriesentryright) + (dst_positive_scale_weighted_unique_firstproductsentriesentryright)) + ((dst_positive_scale_weighted_unique_firstproductsentriesentryright) + (dst_positive_scale_weighted_unique_firstproductsentriesentryright))) + (((dst_negative_code_weighted_unique_firstproductsentriesentryright) + (dst_negative_scale_weighted_unique_firstproductsentriesentryright)) * S ((dst_negative_code_weighted_unique_firstproductsentriesentryright) + (dst_negative_scale_weighted_unique_firstproductsentriesentryright)) + ((dst_negative_scale_weighted_unique_firstproductsentriesentryright) + (dst_negative_scale_weighted_unique_firstproductsentriesentryright)))) + ((((dst_negative_code_weighted_unique_firstproductsentriesentryright) + (dst_negative_scale_weighted_unique_firstproductsentriesentryright)) * S ((dst_negative_code_weighted_unique_firstproductsentriesentryright) + (dst_negative_scale_weighted_unique_firstproductsentriesentryright)) + ((dst_negative_scale_weighted_unique_firstproductsentriesentryright) + (dst_negative_scale_weighted_unique_firstproductsentriesentryright))) + (((dst_negative_code_weighted_unique_firstproductsentriesentryright) + (dst_negative_scale_weighted_unique_firstproductsentriesentryright)) * S ((dst_negative_code_weighted_unique_firstproductsentriesentryright) + (dst_negative_scale_weighted_unique_firstproductsentriesentryright)) + ((dst_negative_scale_weighted_unique_firstproductsentriesentryright) + (dst_negative_scale_weighted_unique_firstproductsentriesentryright)))))) /\ (((((exists ff_h_pvs_weighted_unique_firstproductsentriesentryrightpositive. ff_h_pvs_weighted_unique_firstproductsentriesentryrightpositive + S (dst_positive_weighted_unique_firstproductsentriesentryright) = S ((S (sto_index_weighted_unique_firstproductsentries)) * dst_positive_scale_weighted_unique_firstproductsentriesentryright)) /\ exists ff_q_pvs_weighted_unique_firstproductsentriesentryrightpositive. dst_positive_code_weighted_unique_firstproductsentriesentryright = ff_q_pvs_weighted_unique_firstproductsentriesentryrightpositive * S ((S (sto_index_weighted_unique_firstproductsentries)) * dst_positive_scale_weighted_unique_firstproductsentriesentryright) + (dst_positive_weighted_unique_firstproductsentriesentryright))) /\ (((((exists ff_h_pvs_weighted_unique_firstproductsentriesentryrightnegative. ff_h_pvs_weighted_unique_firstproductsentriesentryrightnegative + S (dst_negative_weighted_unique_firstproductsentriesentryright) = S ((S (sto_index_weighted_unique_firstproductsentries)) * dst_negative_scale_weighted_unique_firstproductsentriesentryright)) /\ exists ff_q_pvs_weighted_unique_firstproductsentriesentryrightnegative. dst_negative_code_weighted_unique_firstproductsentriesentryright = ff_q_pvs_weighted_unique_firstproductsentriesentryrightnegative * S ((S (sto_index_weighted_unique_firstproductsentries)) * dst_negative_scale_weighted_unique_firstproductsentriesentryright) + (dst_negative_weighted_unique_firstproductsentriesentryright))) /\ (exists ge_balance_positive_weighted_unique_firstproductsentriesentryrightvalue ge_balance_negative_weighted_unique_firstproductsentriesentryrightvalue. (((((sto_right_weighted_unique_firstproductsentries) = 2 * (ge_balance_positive_weighted_unique_firstproductsentriesentryrightvalue) /\ (ge_balance_negative_weighted_unique_firstproductsentriesentryrightvalue) = 0) \/ exists ge_signed_half_weighted_unique_firstproductsentriesentryrightvaluedecode. (((sto_right_weighted_unique_firstproductsentries) = 2 * ge_signed_half_weighted_unique_firstproductsentriesentryrightvaluedecode + 1 /\ (ge_balance_positive_weighted_unique_firstproductsentriesentryrightvalue) = 0) /\ (ge_balance_negative_weighted_unique_firstproductsentriesentryrightvalue) = S ge_signed_half_weighted_unique_firstproductsentriesentryrightvaluedecode))) /\ ((dst_positive_weighted_unique_firstproductsentriesentryright) + ge_balance_negative_weighted_unique_firstproductsentriesentryrightvalue = (dst_negative_weighted_unique_firstproductsentriesentryright) + ge_balance_positive_weighted_unique_firstproductsentriesentryrightvalue))))))))) /\ (((exists dst_positive_code_weighted_unique_firstproductsentriesentryoutput dst_positive_scale_weighted_unique_firstproductsentriesentryoutput dst_negative_code_weighted_unique_firstproductsentriesentryoutput dst_negative_scale_weighted_unique_firstproductsentriesentryoutput dst_positive_weighted_unique_firstproductsentriesentryoutput dst_negative_weighted_unique_firstproductsentriesentryoutput. (((sws_product_table_weighted_unique_first) = (((((dst_positive_code_weighted_unique_firstproductsentriesentryoutput) + (dst_positive_scale_weighted_unique_firstproductsentriesentryoutput)) * S ((dst_positive_code_weighted_unique_firstproductsentriesentryoutput) + (dst_positive_scale_weighted_unique_firstproductsentriesentryoutput)) + ((dst_positive_scale_weighted_unique_firstproductsentriesentryoutput) + (dst_positive_scale_weighted_unique_firstproductsentriesentryoutput))) + (((dst_negative_code_weighted_unique_firstproductsentriesentryoutput) + (dst_negative_scale_weighted_unique_firstproductsentriesentryoutput)) * S ((dst_negative_code_weighted_unique_firstproductsentriesentryoutput) + (dst_negative_scale_weighted_unique_firstproductsentriesentryoutput)) + ((dst_negative_scale_weighted_unique_firstproductsentriesentryoutput) + (dst_negative_scale_weighted_unique_firstproductsentriesentryoutput)))) * S ((((dst_positive_code_weighted_unique_firstproductsentriesentryoutput) + (dst_positive_scale_weighted_unique_firstproductsentriesentryoutput)) * S ((dst_positive_code_weighted_unique_firstproductsentriesentryoutput) + (dst_positive_scale_weighted_unique_firstproductsentriesentryoutput)) + ((dst_positive_scale_weighted_unique_firstproductsentriesentryoutput) + (dst_positive_scale_weighted_unique_firstproductsentriesentryoutput))) + (((dst_negative_code_weighted_unique_firstproductsentriesentryoutput) + (dst_negative_scale_weighted_unique_firstproductsentriesentryoutput)) * S ((dst_negative_code_weighted_unique_firstproductsentriesentryoutput) + (dst_negative_scale_weighted_unique_firstproductsentriesentryoutput)) + ((dst_negative_scale_weighted_unique_firstproductsentriesentryoutput) + (dst_negative_scale_weighted_unique_firstproductsentriesentryoutput)))) + ((((dst_negative_code_weighted_unique_firstproductsentriesentryoutput) + (dst_negative_scale_weighted_unique_firstproductsentriesentryoutput)) * S ((dst_negative_code_weighted_unique_firstproductsentriesentryoutput) + (dst_negative_scale_weighted_unique_firstproductsentriesentryoutput)) + ((dst_negative_scale_weighted_unique_firstproductsentriesentryoutput) + (dst_negative_scale_weighted_unique_firstproductsentriesentryoutput))) + (((dst_negative_code_weighted_unique_firstproductsentriesentryoutput) + (dst_negative_scale_weighted_unique_firstproductsentriesentryoutput)) * S ((dst_negative_code_weighted_unique_firstproductsentriesentryoutput) + (dst_negative_scale_weighted_unique_firstproductsentriesentryoutput)) + ((dst_negative_scale_weighted_unique_firstproductsentriesentryoutput) + (dst_negative_scale_weighted_unique_firstproductsentriesentryoutput)))))) /\ (((((exists ff_h_pvs_weighted_unique_firstproductsentriesentryoutputpositive. ff_h_pvs_weighted_unique_firstproductsentriesentryoutputpositive + S (dst_positive_weighted_unique_firstproductsentriesentryoutput) = S ((S (sto_index_weighted_unique_firstproductsentries)) * dst_positive_scale_weighted_unique_firstproductsentriesentryoutput)) /\ exists ff_q_pvs_weighted_unique_firstproductsentriesentryoutputpositive. dst_positive_code_weighted_unique_firstproductsentriesentryoutput = ff_q_pvs_weighted_unique_firstproductsentriesentryoutputpositive * S ((S (sto_index_weighted_unique_firstproductsentries)) * dst_positive_scale_weighted_unique_firstproductsentriesentryoutput) + (dst_positive_weighted_unique_firstproductsentriesentryoutput))) /\ (((((exists ff_h_pvs_weighted_unique_firstproductsentriesentryoutputnegative. ff_h_pvs_weighted_unique_firstproductsentriesentryoutputnegative + S (dst_negative_weighted_unique_firstproductsentriesentryoutput) = S ((S (sto_index_weighted_unique_firstproductsentries)) * dst_negative_scale_weighted_unique_firstproductsentriesentryoutput)) /\ exists ff_q_pvs_weighted_unique_firstproductsentriesentryoutputnegative. dst_negative_code_weighted_unique_firstproductsentriesentryoutput = ff_q_pvs_weighted_unique_firstproductsentriesentryoutputnegative * S ((S (sto_index_weighted_unique_firstproductsentries)) * dst_negative_scale_weighted_unique_firstproductsentriesentryoutput) + (dst_negative_weighted_unique_firstproductsentriesentryoutput))) /\ (exists ge_balance_positive_weighted_unique_firstproductsentriesentryoutputvalue ge_balance_negative_weighted_unique_firstproductsentriesentryoutputvalue. (((((sto_output_weighted_unique_firstproductsentries) = 2 * (ge_balance_positive_weighted_unique_firstproductsentriesentryoutputvalue) /\ (ge_balance_negative_weighted_unique_firstproductsentriesentryoutputvalue) = 0) \/ exists ge_signed_half_weighted_unique_firstproductsentriesentryoutputvaluedecode. (((sto_output_weighted_unique_firstproductsentries) = 2 * ge_signed_half_weighted_unique_firstproductsentriesentryoutputvaluedecode + 1 /\ (ge_balance_positive_weighted_unique_firstproductsentriesentryoutputvalue) = 0) /\ (ge_balance_negative_weighted_unique_firstproductsentriesentryoutputvalue) = S ge_signed_half_weighted_unique_firstproductsentriesentryoutputvaluedecode))) /\ ((dst_positive_weighted_unique_firstproductsentriesentryoutput) + ge_balance_negative_weighted_unique_firstproductsentriesentryoutputvalue = (dst_negative_weighted_unique_firstproductsentriesentryoutput) + ge_balance_positive_weighted_unique_firstproductsentriesentryoutputvalue))))))))) /\ (exists sto_ap_weighted_unique_firstproductsentriesentryoperation sto_an_weighted_unique_firstproductsentriesentryoperation sto_bp_weighted_unique_firstproductsentriesentryoperation sto_bn_weighted_unique_firstproductsentriesentryoperation sto_cp_weighted_unique_firstproductsentriesentryoperation sto_cn_weighted_unique_firstproductsentriesentryoperation. (((((sto_left_weighted_unique_firstproductsentries) = 2 * (sto_ap_weighted_unique_firstproductsentriesentryoperation) /\ (sto_an_weighted_unique_firstproductsentriesentryoperation) = 0) \/ exists ge_signed_half_weighted_unique_firstproductsentriesentryoperationleft. (((sto_left_weighted_unique_firstproductsentries) = 2 * ge_signed_half_weighted_unique_firstproductsentriesentryoperationleft + 1 /\ (sto_ap_weighted_unique_firstproductsentriesentryoperation) = 0) /\ (sto_an_weighted_unique_firstproductsentriesentryoperation) = S ge_signed_half_weighted_unique_firstproductsentriesentryoperationleft))) /\ ((((((sto_right_weighted_unique_firstproductsentries) = 2 * (sto_bp_weighted_unique_firstproductsentriesentryoperation) /\ (sto_bn_weighted_unique_firstproductsentriesentryoperation) = 0) \/ exists ge_signed_half_weighted_unique_firstproductsentriesentryoperationright. (((sto_right_weighted_unique_firstproductsentries) = 2 * ge_signed_half_weighted_unique_firstproductsentriesentryoperationright + 1 /\ (sto_bp_weighted_unique_firstproductsentriesentryoperation) = 0) /\ (sto_bn_weighted_unique_firstproductsentriesentryoperation) = S ge_signed_half_weighted_unique_firstproductsentriesentryoperationright))) /\ ((((((sto_output_weighted_unique_firstproductsentries) = 2 * (sto_cp_weighted_unique_firstproductsentriesentryoperation) /\ (sto_cn_weighted_unique_firstproductsentriesentryoperation) = 0) \/ exists ge_signed_half_weighted_unique_firstproductsentriesentryoperationoutput. (((sto_output_weighted_unique_firstproductsentries) = 2 * ge_signed_half_weighted_unique_firstproductsentriesentryoperationoutput + 1 /\ (sto_cp_weighted_unique_firstproductsentriesentryoperation) = 0) /\ (sto_cn_weighted_unique_firstproductsentriesentryoperation) = S ge_signed_half_weighted_unique_firstproductsentriesentryoperationoutput))) /\ ((sto_ap_weighted_unique_firstproductsentriesentryoperation * sto_bp_weighted_unique_firstproductsentriesentryoperation + sto_an_weighted_unique_firstproductsentriesentryoperation * sto_bn_weighted_unique_firstproductsentriesentryoperation) + sto_cn_weighted_unique_firstproductsentriesentryoperation = (sto_ap_weighted_unique_firstproductsentriesentryoperation * sto_bn_weighted_unique_firstproductsentriesentryoperation + sto_an_weighted_unique_firstproductsentriesentryoperation * sto_bp_weighted_unique_firstproductsentriesentryoperation) + sto_cp_weighted_unique_firstproductsentriesentryoperation))))))))))))))))))) /\ (exists dst_positive_code_weighted_unique_firstsum dst_positive_scale_weighted_unique_firstsum dst_negative_code_weighted_unique_firstsum dst_negative_scale_weighted_unique_firstsum dst_positive_sum_weighted_unique_firstsum dst_negative_sum_weighted_unique_firstsum. (((sws_product_table_weighted_unique_first) = (((((dst_positive_code_weighted_unique_firstsum) + (dst_positive_scale_weighted_unique_firstsum)) * S ((dst_positive_code_weighted_unique_firstsum) + (dst_positive_scale_weighted_unique_firstsum)) + ((dst_positive_scale_weighted_unique_firstsum) + (dst_positive_scale_weighted_unique_firstsum))) + (((dst_negative_code_weighted_unique_firstsum) + (dst_negative_scale_weighted_unique_firstsum)) * S ((dst_negative_code_weighted_unique_firstsum) + (dst_negative_scale_weighted_unique_firstsum)) + ((dst_negative_scale_weighted_unique_firstsum) + (dst_negative_scale_weighted_unique_firstsum)))) * S ((((dst_positive_code_weighted_unique_firstsum) + (dst_positive_scale_weighted_unique_firstsum)) * S ((dst_positive_code_weighted_unique_firstsum) + (dst_positive_scale_weighted_unique_firstsum)) + ((dst_positive_scale_weighted_unique_firstsum) + (dst_positive_scale_weighted_unique_firstsum))) + (((dst_negative_code_weighted_unique_firstsum) + (dst_negative_scale_weighted_unique_firstsum)) * S ((dst_negative_code_weighted_unique_firstsum) + (dst_negative_scale_weighted_unique_firstsum)) + ((dst_negative_scale_weighted_unique_firstsum) + (dst_negative_scale_weighted_unique_firstsum)))) + ((((dst_negative_code_weighted_unique_firstsum) + (dst_negative_scale_weighted_unique_firstsum)) * S ((dst_negative_code_weighted_unique_firstsum) + (dst_negative_scale_weighted_unique_firstsum)) + ((dst_negative_scale_weighted_unique_firstsum) + (dst_negative_scale_weighted_unique_firstsum))) + (((dst_negative_code_weighted_unique_firstsum) + (dst_negative_scale_weighted_unique_firstsum)) * S ((dst_negative_code_weighted_unique_firstsum) + (dst_negative_scale_weighted_unique_firstsum)) + ((dst_negative_scale_weighted_unique_firstsum) + (dst_negative_scale_weighted_unique_firstsum)))))) /\ (((exists fs_u_dst_weighted_unique_firstsumpositive fs_v_dst_weighted_unique_firstsumpositive. ((((exists fs_h_dst_weighted_unique_firstsumpositive_body_start. fs_h_dst_weighted_unique_firstsumpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_weighted_unique_firstsumpositive)) /\ exists fs_q_dst_weighted_unique_firstsumpositive_body_start. fs_u_dst_weighted_unique_firstsumpositive = fs_q_dst_weighted_unique_firstsumpositive_body_start * S ((S (0)) * fs_v_dst_weighted_unique_firstsumpositive) + (0))) /\ ((((exists fs_h_dst_weighted_unique_firstsumpositive_body_terminal. fs_h_dst_weighted_unique_firstsumpositive_body_terminal + S (dst_positive_sum_weighted_unique_firstsum) = S ((S (l)) * fs_v_dst_weighted_unique_firstsumpositive)) /\ exists fs_q_dst_weighted_unique_firstsumpositive_body_terminal. fs_u_dst_weighted_unique_firstsumpositive = fs_q_dst_weighted_unique_firstsumpositive_body_terminal * S ((S (l)) * fs_v_dst_weighted_unique_firstsumpositive) + (dst_positive_sum_weighted_unique_firstsum))) /\ forall fs_i_dst_weighted_unique_firstsumpositive_body_steps. (exists fs_lt_dst_weighted_unique_firstsumpositive_body_steps_bound. fs_lt_dst_weighted_unique_firstsumpositive_body_steps_bound + S fs_i_dst_weighted_unique_firstsumpositive_body_steps = l) -> exists fs_a_dst_weighted_unique_firstsumpositive_body_steps fs_r_dst_weighted_unique_firstsumpositive_body_steps fs_s_dst_weighted_unique_firstsumpositive_body_steps. ((((exists fs_h_dst_weighted_unique_firstsumpositive_body_steps_summand. fs_h_dst_weighted_unique_firstsumpositive_body_steps_summand + S (fs_a_dst_weighted_unique_firstsumpositive_body_steps) = S ((S (fs_i_dst_weighted_unique_firstsumpositive_body_steps)) * dst_positive_scale_weighted_unique_firstsum)) /\ exists fs_q_dst_weighted_unique_firstsumpositive_body_steps_summand. dst_positive_code_weighted_unique_firstsum = fs_q_dst_weighted_unique_firstsumpositive_body_steps_summand * S ((S (fs_i_dst_weighted_unique_firstsumpositive_body_steps)) * dst_positive_scale_weighted_unique_firstsum) + (fs_a_dst_weighted_unique_firstsumpositive_body_steps))) /\ ((((exists fs_h_dst_weighted_unique_firstsumpositive_body_steps_partial. fs_h_dst_weighted_unique_firstsumpositive_body_steps_partial + S (fs_r_dst_weighted_unique_firstsumpositive_body_steps) = S ((S (fs_i_dst_weighted_unique_firstsumpositive_body_steps)) * fs_v_dst_weighted_unique_firstsumpositive)) /\ exists fs_q_dst_weighted_unique_firstsumpositive_body_steps_partial. fs_u_dst_weighted_unique_firstsumpositive = fs_q_dst_weighted_unique_firstsumpositive_body_steps_partial * S ((S (fs_i_dst_weighted_unique_firstsumpositive_body_steps)) * fs_v_dst_weighted_unique_firstsumpositive) + (fs_r_dst_weighted_unique_firstsumpositive_body_steps))) /\ ((((exists fs_h_dst_weighted_unique_firstsumpositive_body_steps_successor. fs_h_dst_weighted_unique_firstsumpositive_body_steps_successor + S (fs_s_dst_weighted_unique_firstsumpositive_body_steps) = S ((S (S fs_i_dst_weighted_unique_firstsumpositive_body_steps)) * fs_v_dst_weighted_unique_firstsumpositive)) /\ exists fs_q_dst_weighted_unique_firstsumpositive_body_steps_successor. fs_u_dst_weighted_unique_firstsumpositive = fs_q_dst_weighted_unique_firstsumpositive_body_steps_successor * S ((S (S fs_i_dst_weighted_unique_firstsumpositive_body_steps)) * fs_v_dst_weighted_unique_firstsumpositive) + (fs_s_dst_weighted_unique_firstsumpositive_body_steps))) /\ fs_s_dst_weighted_unique_firstsumpositive_body_steps = fs_r_dst_weighted_unique_firstsumpositive_body_steps + fs_a_dst_weighted_unique_firstsumpositive_body_steps)))))) /\ (((exists fs_u_dst_weighted_unique_firstsumnegative fs_v_dst_weighted_unique_firstsumnegative. ((((exists fs_h_dst_weighted_unique_firstsumnegative_body_start. fs_h_dst_weighted_unique_firstsumnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_weighted_unique_firstsumnegative)) /\ exists fs_q_dst_weighted_unique_firstsumnegative_body_start. fs_u_dst_weighted_unique_firstsumnegative = fs_q_dst_weighted_unique_firstsumnegative_body_start * S ((S (0)) * fs_v_dst_weighted_unique_firstsumnegative) + (0))) /\ ((((exists fs_h_dst_weighted_unique_firstsumnegative_body_terminal. fs_h_dst_weighted_unique_firstsumnegative_body_terminal + S (dst_negative_sum_weighted_unique_firstsum) = S ((S (l)) * fs_v_dst_weighted_unique_firstsumnegative)) /\ exists fs_q_dst_weighted_unique_firstsumnegative_body_terminal. fs_u_dst_weighted_unique_firstsumnegative = fs_q_dst_weighted_unique_firstsumnegative_body_terminal * S ((S (l)) * fs_v_dst_weighted_unique_firstsumnegative) + (dst_negative_sum_weighted_unique_firstsum))) /\ forall fs_i_dst_weighted_unique_firstsumnegative_body_steps. (exists fs_lt_dst_weighted_unique_firstsumnegative_body_steps_bound. fs_lt_dst_weighted_unique_firstsumnegative_body_steps_bound + S fs_i_dst_weighted_unique_firstsumnegative_body_steps = l) -> exists fs_a_dst_weighted_unique_firstsumnegative_body_steps fs_r_dst_weighted_unique_firstsumnegative_body_steps fs_s_dst_weighted_unique_firstsumnegative_body_steps. ((((exists fs_h_dst_weighted_unique_firstsumnegative_body_steps_summand. fs_h_dst_weighted_unique_firstsumnegative_body_steps_summand + S (fs_a_dst_weighted_unique_firstsumnegative_body_steps) = S ((S (fs_i_dst_weighted_unique_firstsumnegative_body_steps)) * dst_negative_scale_weighted_unique_firstsum)) /\ exists fs_q_dst_weighted_unique_firstsumnegative_body_steps_summand. dst_negative_code_weighted_unique_firstsum = fs_q_dst_weighted_unique_firstsumnegative_body_steps_summand * S ((S (fs_i_dst_weighted_unique_firstsumnegative_body_steps)) * dst_negative_scale_weighted_unique_firstsum) + (fs_a_dst_weighted_unique_firstsumnegative_body_steps))) /\ ((((exists fs_h_dst_weighted_unique_firstsumnegative_body_steps_partial. fs_h_dst_weighted_unique_firstsumnegative_body_steps_partial + S (fs_r_dst_weighted_unique_firstsumnegative_body_steps) = S ((S (fs_i_dst_weighted_unique_firstsumnegative_body_steps)) * fs_v_dst_weighted_unique_firstsumnegative)) /\ exists fs_q_dst_weighted_unique_firstsumnegative_body_steps_partial. fs_u_dst_weighted_unique_firstsumnegative = fs_q_dst_weighted_unique_firstsumnegative_body_steps_partial * S ((S (fs_i_dst_weighted_unique_firstsumnegative_body_steps)) * fs_v_dst_weighted_unique_firstsumnegative) + (fs_r_dst_weighted_unique_firstsumnegative_body_steps))) /\ ((((exists fs_h_dst_weighted_unique_firstsumnegative_body_steps_successor. fs_h_dst_weighted_unique_firstsumnegative_body_steps_successor + S (fs_s_dst_weighted_unique_firstsumnegative_body_steps) = S ((S (S fs_i_dst_weighted_unique_firstsumnegative_body_steps)) * fs_v_dst_weighted_unique_firstsumnegative)) /\ exists fs_q_dst_weighted_unique_firstsumnegative_body_steps_successor. fs_u_dst_weighted_unique_firstsumnegative = fs_q_dst_weighted_unique_firstsumnegative_body_steps_successor * S ((S (S fs_i_dst_weighted_unique_firstsumnegative_body_steps)) * fs_v_dst_weighted_unique_firstsumnegative) + (fs_s_dst_weighted_unique_firstsumnegative_body_steps))) /\ fs_s_dst_weighted_unique_firstsumnegative_body_steps = fs_r_dst_weighted_unique_firstsumnegative_body_steps + fs_a_dst_weighted_unique_firstsumnegative_body_steps)))))) /\ (exists ge_balance_positive_weighted_unique_firstsumresult ge_balance_negative_weighted_unique_firstsumresult. (((((a) = 2 * (ge_balance_positive_weighted_unique_firstsumresult) /\ (ge_balance_negative_weighted_unique_firstsumresult) = 0) \/ exists ge_signed_half_weighted_unique_firstsumresultdecode. (((a) = 2 * ge_signed_half_weighted_unique_firstsumresultdecode + 1 /\ (ge_balance_positive_weighted_unique_firstsumresult) = 0) /\ (ge_balance_negative_weighted_unique_firstsumresult) = S ge_signed_half_weighted_unique_firstsumresultdecode))) /\ ((dst_positive_sum_weighted_unique_firstsum) + ge_balance_negative_weighted_unique_firstsumresult = (dst_negative_sum_weighted_unique_firstsum) + ge_balance_positive_weighted_unique_firstsumresult))))))))))) -> (exists sws_product_table_weighted_unique_second. ((((exists dst_positive_code_weighted_unique_secondproductsleft_table dst_positive_scale_weighted_unique_secondproductsleft_table dst_negative_code_weighted_unique_secondproductsleft_table dst_negative_scale_weighted_unique_secondproductsleft_table. (((W) = (((((dst_positive_code_weighted_unique_secondproductsleft_table) + (dst_positive_scale_weighted_unique_secondproductsleft_table)) * S ((dst_positive_code_weighted_unique_secondproductsleft_table) + (dst_positive_scale_weighted_unique_secondproductsleft_table)) + ((dst_positive_scale_weighted_unique_secondproductsleft_table) + (dst_positive_scale_weighted_unique_secondproductsleft_table))) + (((dst_negative_code_weighted_unique_secondproductsleft_table) + (dst_negative_scale_weighted_unique_secondproductsleft_table)) * S ((dst_negative_code_weighted_unique_secondproductsleft_table) + (dst_negative_scale_weighted_unique_secondproductsleft_table)) + ((dst_negative_scale_weighted_unique_secondproductsleft_table) + (dst_negative_scale_weighted_unique_secondproductsleft_table)))) * S ((((dst_positive_code_weighted_unique_secondproductsleft_table) + (dst_positive_scale_weighted_unique_secondproductsleft_table)) * S ((dst_positive_code_weighted_unique_secondproductsleft_table) + (dst_positive_scale_weighted_unique_secondproductsleft_table)) + ((dst_positive_scale_weighted_unique_secondproductsleft_table) + (dst_positive_scale_weighted_unique_secondproductsleft_table))) + (((dst_negative_code_weighted_unique_secondproductsleft_table) + (dst_negative_scale_weighted_unique_secondproductsleft_table)) * S ((dst_negative_code_weighted_unique_secondproductsleft_table) + (dst_negative_scale_weighted_unique_secondproductsleft_table)) + ((dst_negative_scale_weighted_unique_secondproductsleft_table) + (dst_negative_scale_weighted_unique_secondproductsleft_table)))) + ((((dst_negative_code_weighted_unique_secondproductsleft_table) + (dst_negative_scale_weighted_unique_secondproductsleft_table)) * S ((dst_negative_code_weighted_unique_secondproductsleft_table) + (dst_negative_scale_weighted_unique_secondproductsleft_table)) + ((dst_negative_scale_weighted_unique_secondproductsleft_table) + (dst_negative_scale_weighted_unique_secondproductsleft_table))) + (((dst_negative_code_weighted_unique_secondproductsleft_table) + (dst_negative_scale_weighted_unique_secondproductsleft_table)) * S ((dst_negative_code_weighted_unique_secondproductsleft_table) + (dst_negative_scale_weighted_unique_secondproductsleft_table)) + ((dst_negative_scale_weighted_unique_secondproductsleft_table) + (dst_negative_scale_weighted_unique_secondproductsleft_table)))))) /\ (forall dst_index_weighted_unique_secondproductsleft_table. (exists pvs_le_gap_weighted_unique_secondproductsleft_tabledomain. pvs_le_gap_weighted_unique_secondproductsleft_tabledomain + (dst_index_weighted_unique_secondproductsleft_table) = (l)) -> exists dst_positive_weighted_unique_secondproductsleft_table dst_negative_weighted_unique_secondproductsleft_table dst_value_weighted_unique_secondproductsleft_table. ((((exists ff_h_pvs_weighted_unique_secondproductsleft_tableentrypositive. ff_h_pvs_weighted_unique_secondproductsleft_tableentrypositive + S (dst_positive_weighted_unique_secondproductsleft_table) = S ((S (dst_index_weighted_unique_secondproductsleft_table)) * dst_positive_scale_weighted_unique_secondproductsleft_table)) /\ exists ff_q_pvs_weighted_unique_secondproductsleft_tableentrypositive. dst_positive_code_weighted_unique_secondproductsleft_table = ff_q_pvs_weighted_unique_secondproductsleft_tableentrypositive * S ((S (dst_index_weighted_unique_secondproductsleft_table)) * dst_positive_scale_weighted_unique_secondproductsleft_table) + (dst_positive_weighted_unique_secondproductsleft_table))) /\ (((((exists ff_h_pvs_weighted_unique_secondproductsleft_tableentrynegative. ff_h_pvs_weighted_unique_secondproductsleft_tableentrynegative + S (dst_negative_weighted_unique_secondproductsleft_table) = S ((S (dst_index_weighted_unique_secondproductsleft_table)) * dst_negative_scale_weighted_unique_secondproductsleft_table)) /\ exists ff_q_pvs_weighted_unique_secondproductsleft_tableentrynegative. dst_negative_code_weighted_unique_secondproductsleft_table = ff_q_pvs_weighted_unique_secondproductsleft_tableentrynegative * S ((S (dst_index_weighted_unique_secondproductsleft_table)) * dst_negative_scale_weighted_unique_secondproductsleft_table) + (dst_negative_weighted_unique_secondproductsleft_table))) /\ (exists ge_balance_positive_weighted_unique_secondproductsleft_tableentryvalue ge_balance_negative_weighted_unique_secondproductsleft_tableentryvalue. (((((dst_value_weighted_unique_secondproductsleft_table) = 2 * (ge_balance_positive_weighted_unique_secondproductsleft_tableentryvalue) /\ (ge_balance_negative_weighted_unique_secondproductsleft_tableentryvalue) = 0) \/ exists ge_signed_half_weighted_unique_secondproductsleft_tableentryvaluedecode. (((dst_value_weighted_unique_secondproductsleft_table) = 2 * ge_signed_half_weighted_unique_secondproductsleft_tableentryvaluedecode + 1 /\ (ge_balance_positive_weighted_unique_secondproductsleft_tableentryvalue) = 0) /\ (ge_balance_negative_weighted_unique_secondproductsleft_tableentryvalue) = S ge_signed_half_weighted_unique_secondproductsleft_tableentryvaluedecode))) /\ ((dst_positive_weighted_unique_secondproductsleft_table) + ge_balance_negative_weighted_unique_secondproductsleft_tableentryvalue = (dst_negative_weighted_unique_secondproductsleft_table) + ge_balance_positive_weighted_unique_secondproductsleft_tableentryvalue))))))))) /\ (((exists dst_positive_code_weighted_unique_secondproductsright_table dst_positive_scale_weighted_unique_secondproductsright_table dst_negative_code_weighted_unique_secondproductsright_table dst_negative_scale_weighted_unique_secondproductsright_table. (((F) = (((((dst_positive_code_weighted_unique_secondproductsright_table) + (dst_positive_scale_weighted_unique_secondproductsright_table)) * S ((dst_positive_code_weighted_unique_secondproductsright_table) + (dst_positive_scale_weighted_unique_secondproductsright_table)) + ((dst_positive_scale_weighted_unique_secondproductsright_table) + (dst_positive_scale_weighted_unique_secondproductsright_table))) + (((dst_negative_code_weighted_unique_secondproductsright_table) + (dst_negative_scale_weighted_unique_secondproductsright_table)) * S ((dst_negative_code_weighted_unique_secondproductsright_table) + (dst_negative_scale_weighted_unique_secondproductsright_table)) + ((dst_negative_scale_weighted_unique_secondproductsright_table) + (dst_negative_scale_weighted_unique_secondproductsright_table)))) * S ((((dst_positive_code_weighted_unique_secondproductsright_table) + (dst_positive_scale_weighted_unique_secondproductsright_table)) * S ((dst_positive_code_weighted_unique_secondproductsright_table) + (dst_positive_scale_weighted_unique_secondproductsright_table)) + ((dst_positive_scale_weighted_unique_secondproductsright_table) + (dst_positive_scale_weighted_unique_secondproductsright_table))) + (((dst_negative_code_weighted_unique_secondproductsright_table) + (dst_negative_scale_weighted_unique_secondproductsright_table)) * S ((dst_negative_code_weighted_unique_secondproductsright_table) + (dst_negative_scale_weighted_unique_secondproductsright_table)) + ((dst_negative_scale_weighted_unique_secondproductsright_table) + (dst_negative_scale_weighted_unique_secondproductsright_table)))) + ((((dst_negative_code_weighted_unique_secondproductsright_table) + (dst_negative_scale_weighted_unique_secondproductsright_table)) * S ((dst_negative_code_weighted_unique_secondproductsright_table) + (dst_negative_scale_weighted_unique_secondproductsright_table)) + ((dst_negative_scale_weighted_unique_secondproductsright_table) + (dst_negative_scale_weighted_unique_secondproductsright_table))) + (((dst_negative_code_weighted_unique_secondproductsright_table) + (dst_negative_scale_weighted_unique_secondproductsright_table)) * S ((dst_negative_code_weighted_unique_secondproductsright_table) + (dst_negative_scale_weighted_unique_secondproductsright_table)) + ((dst_negative_scale_weighted_unique_secondproductsright_table) + (dst_negative_scale_weighted_unique_secondproductsright_table)))))) /\ (forall dst_index_weighted_unique_secondproductsright_table. (exists pvs_le_gap_weighted_unique_secondproductsright_tabledomain. pvs_le_gap_weighted_unique_secondproductsright_tabledomain + (dst_index_weighted_unique_secondproductsright_table) = (l)) -> exists dst_positive_weighted_unique_secondproductsright_table dst_negative_weighted_unique_secondproductsright_table dst_value_weighted_unique_secondproductsright_table. ((((exists ff_h_pvs_weighted_unique_secondproductsright_tableentrypositive. ff_h_pvs_weighted_unique_secondproductsright_tableentrypositive + S (dst_positive_weighted_unique_secondproductsright_table) = S ((S (dst_index_weighted_unique_secondproductsright_table)) * dst_positive_scale_weighted_unique_secondproductsright_table)) /\ exists ff_q_pvs_weighted_unique_secondproductsright_tableentrypositive. dst_positive_code_weighted_unique_secondproductsright_table = ff_q_pvs_weighted_unique_secondproductsright_tableentrypositive * S ((S (dst_index_weighted_unique_secondproductsright_table)) * dst_positive_scale_weighted_unique_secondproductsright_table) + (dst_positive_weighted_unique_secondproductsright_table))) /\ (((((exists ff_h_pvs_weighted_unique_secondproductsright_tableentrynegative. ff_h_pvs_weighted_unique_secondproductsright_tableentrynegative + S (dst_negative_weighted_unique_secondproductsright_table) = S ((S (dst_index_weighted_unique_secondproductsright_table)) * dst_negative_scale_weighted_unique_secondproductsright_table)) /\ exists ff_q_pvs_weighted_unique_secondproductsright_tableentrynegative. dst_negative_code_weighted_unique_secondproductsright_table = ff_q_pvs_weighted_unique_secondproductsright_tableentrynegative * S ((S (dst_index_weighted_unique_secondproductsright_table)) * dst_negative_scale_weighted_unique_secondproductsright_table) + (dst_negative_weighted_unique_secondproductsright_table))) /\ (exists ge_balance_positive_weighted_unique_secondproductsright_tableentryvalue ge_balance_negative_weighted_unique_secondproductsright_tableentryvalue. (((((dst_value_weighted_unique_secondproductsright_table) = 2 * (ge_balance_positive_weighted_unique_secondproductsright_tableentryvalue) /\ (ge_balance_negative_weighted_unique_secondproductsright_tableentryvalue) = 0) \/ exists ge_signed_half_weighted_unique_secondproductsright_tableentryvaluedecode. (((dst_value_weighted_unique_secondproductsright_table) = 2 * ge_signed_half_weighted_unique_secondproductsright_tableentryvaluedecode + 1 /\ (ge_balance_positive_weighted_unique_secondproductsright_tableentryvalue) = 0) /\ (ge_balance_negative_weighted_unique_secondproductsright_tableentryvalue) = S ge_signed_half_weighted_unique_secondproductsright_tableentryvaluedecode))) /\ ((dst_positive_weighted_unique_secondproductsright_table) + ge_balance_negative_weighted_unique_secondproductsright_tableentryvalue = (dst_negative_weighted_unique_secondproductsright_table) + ge_balance_positive_weighted_unique_secondproductsright_tableentryvalue))))))))) /\ (((exists dst_positive_code_weighted_unique_secondproductsoutput_table dst_positive_scale_weighted_unique_secondproductsoutput_table dst_negative_code_weighted_unique_secondproductsoutput_table dst_negative_scale_weighted_unique_secondproductsoutput_table. (((sws_product_table_weighted_unique_second) = (((((dst_positive_code_weighted_unique_secondproductsoutput_table) + (dst_positive_scale_weighted_unique_secondproductsoutput_table)) * S ((dst_positive_code_weighted_unique_secondproductsoutput_table) + (dst_positive_scale_weighted_unique_secondproductsoutput_table)) + ((dst_positive_scale_weighted_unique_secondproductsoutput_table) + (dst_positive_scale_weighted_unique_secondproductsoutput_table))) + (((dst_negative_code_weighted_unique_secondproductsoutput_table) + (dst_negative_scale_weighted_unique_secondproductsoutput_table)) * S ((dst_negative_code_weighted_unique_secondproductsoutput_table) + (dst_negative_scale_weighted_unique_secondproductsoutput_table)) + ((dst_negative_scale_weighted_unique_secondproductsoutput_table) + (dst_negative_scale_weighted_unique_secondproductsoutput_table)))) * S ((((dst_positive_code_weighted_unique_secondproductsoutput_table) + (dst_positive_scale_weighted_unique_secondproductsoutput_table)) * S ((dst_positive_code_weighted_unique_secondproductsoutput_table) + (dst_positive_scale_weighted_unique_secondproductsoutput_table)) + ((dst_positive_scale_weighted_unique_secondproductsoutput_table) + (dst_positive_scale_weighted_unique_secondproductsoutput_table))) + (((dst_negative_code_weighted_unique_secondproductsoutput_table) + (dst_negative_scale_weighted_unique_secondproductsoutput_table)) * S ((dst_negative_code_weighted_unique_secondproductsoutput_table) + (dst_negative_scale_weighted_unique_secondproductsoutput_table)) + ((dst_negative_scale_weighted_unique_secondproductsoutput_table) + (dst_negative_scale_weighted_unique_secondproductsoutput_table)))) + ((((dst_negative_code_weighted_unique_secondproductsoutput_table) + (dst_negative_scale_weighted_unique_secondproductsoutput_table)) * S ((dst_negative_code_weighted_unique_secondproductsoutput_table) + (dst_negative_scale_weighted_unique_secondproductsoutput_table)) + ((dst_negative_scale_weighted_unique_secondproductsoutput_table) + (dst_negative_scale_weighted_unique_secondproductsoutput_table))) + (((dst_negative_code_weighted_unique_secondproductsoutput_table) + (dst_negative_scale_weighted_unique_secondproductsoutput_table)) * S ((dst_negative_code_weighted_unique_secondproductsoutput_table) + (dst_negative_scale_weighted_unique_secondproductsoutput_table)) + ((dst_negative_scale_weighted_unique_secondproductsoutput_table) + (dst_negative_scale_weighted_unique_secondproductsoutput_table)))))) /\ (forall dst_index_weighted_unique_secondproductsoutput_table. (exists pvs_le_gap_weighted_unique_secondproductsoutput_tabledomain. pvs_le_gap_weighted_unique_secondproductsoutput_tabledomain + (dst_index_weighted_unique_secondproductsoutput_table) = (l)) -> exists dst_positive_weighted_unique_secondproductsoutput_table dst_negative_weighted_unique_secondproductsoutput_table dst_value_weighted_unique_secondproductsoutput_table. ((((exists ff_h_pvs_weighted_unique_secondproductsoutput_tableentrypositive. ff_h_pvs_weighted_unique_secondproductsoutput_tableentrypositive + S (dst_positive_weighted_unique_secondproductsoutput_table) = S ((S (dst_index_weighted_unique_secondproductsoutput_table)) * dst_positive_scale_weighted_unique_secondproductsoutput_table)) /\ exists ff_q_pvs_weighted_unique_secondproductsoutput_tableentrypositive. dst_positive_code_weighted_unique_secondproductsoutput_table = ff_q_pvs_weighted_unique_secondproductsoutput_tableentrypositive * S ((S (dst_index_weighted_unique_secondproductsoutput_table)) * dst_positive_scale_weighted_unique_secondproductsoutput_table) + (dst_positive_weighted_unique_secondproductsoutput_table))) /\ (((((exists ff_h_pvs_weighted_unique_secondproductsoutput_tableentrynegative. ff_h_pvs_weighted_unique_secondproductsoutput_tableentrynegative + S (dst_negative_weighted_unique_secondproductsoutput_table) = S ((S (dst_index_weighted_unique_secondproductsoutput_table)) * dst_negative_scale_weighted_unique_secondproductsoutput_table)) /\ exists ff_q_pvs_weighted_unique_secondproductsoutput_tableentrynegative. dst_negative_code_weighted_unique_secondproductsoutput_table = ff_q_pvs_weighted_unique_secondproductsoutput_tableentrynegative * S ((S (dst_index_weighted_unique_secondproductsoutput_table)) * dst_negative_scale_weighted_unique_secondproductsoutput_table) + (dst_negative_weighted_unique_secondproductsoutput_table))) /\ (exists ge_balance_positive_weighted_unique_secondproductsoutput_tableentryvalue ge_balance_negative_weighted_unique_secondproductsoutput_tableentryvalue. (((((dst_value_weighted_unique_secondproductsoutput_table) = 2 * (ge_balance_positive_weighted_unique_secondproductsoutput_tableentryvalue) /\ (ge_balance_negative_weighted_unique_secondproductsoutput_tableentryvalue) = 0) \/ exists ge_signed_half_weighted_unique_secondproductsoutput_tableentryvaluedecode. (((dst_value_weighted_unique_secondproductsoutput_table) = 2 * ge_signed_half_weighted_unique_secondproductsoutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_weighted_unique_secondproductsoutput_tableentryvalue) = 0) /\ (ge_balance_negative_weighted_unique_secondproductsoutput_tableentryvalue) = S ge_signed_half_weighted_unique_secondproductsoutput_tableentryvaluedecode))) /\ ((dst_positive_weighted_unique_secondproductsoutput_table) + ge_balance_negative_weighted_unique_secondproductsoutput_tableentryvalue = (dst_negative_weighted_unique_secondproductsoutput_table) + ge_balance_positive_weighted_unique_secondproductsoutput_tableentryvalue))))))))) /\ (forall sto_index_weighted_unique_secondproductsentries. (exists pvs_gap_weighted_unique_secondproductsentriesbound. pvs_gap_weighted_unique_secondproductsentriesbound + S (sto_index_weighted_unique_secondproductsentries) = (l)) -> exists sto_left_weighted_unique_secondproductsentries sto_right_weighted_unique_secondproductsentries sto_output_weighted_unique_secondproductsentries. ((exists dst_positive_code_weighted_unique_secondproductsentriesentryleft dst_positive_scale_weighted_unique_secondproductsentriesentryleft dst_negative_code_weighted_unique_secondproductsentriesentryleft dst_negative_scale_weighted_unique_secondproductsentriesentryleft dst_positive_weighted_unique_secondproductsentriesentryleft dst_negative_weighted_unique_secondproductsentriesentryleft. (((W) = (((((dst_positive_code_weighted_unique_secondproductsentriesentryleft) + (dst_positive_scale_weighted_unique_secondproductsentriesentryleft)) * S ((dst_positive_code_weighted_unique_secondproductsentriesentryleft) + (dst_positive_scale_weighted_unique_secondproductsentriesentryleft)) + ((dst_positive_scale_weighted_unique_secondproductsentriesentryleft) + (dst_positive_scale_weighted_unique_secondproductsentriesentryleft))) + (((dst_negative_code_weighted_unique_secondproductsentriesentryleft) + (dst_negative_scale_weighted_unique_secondproductsentriesentryleft)) * S ((dst_negative_code_weighted_unique_secondproductsentriesentryleft) + (dst_negative_scale_weighted_unique_secondproductsentriesentryleft)) + ((dst_negative_scale_weighted_unique_secondproductsentriesentryleft) + (dst_negative_scale_weighted_unique_secondproductsentriesentryleft)))) * S ((((dst_positive_code_weighted_unique_secondproductsentriesentryleft) + (dst_positive_scale_weighted_unique_secondproductsentriesentryleft)) * S ((dst_positive_code_weighted_unique_secondproductsentriesentryleft) + (dst_positive_scale_weighted_unique_secondproductsentriesentryleft)) + ((dst_positive_scale_weighted_unique_secondproductsentriesentryleft) + (dst_positive_scale_weighted_unique_secondproductsentriesentryleft))) + (((dst_negative_code_weighted_unique_secondproductsentriesentryleft) + (dst_negative_scale_weighted_unique_secondproductsentriesentryleft)) * S ((dst_negative_code_weighted_unique_secondproductsentriesentryleft) + (dst_negative_scale_weighted_unique_secondproductsentriesentryleft)) + ((dst_negative_scale_weighted_unique_secondproductsentriesentryleft) + (dst_negative_scale_weighted_unique_secondproductsentriesentryleft)))) + ((((dst_negative_code_weighted_unique_secondproductsentriesentryleft) + (dst_negative_scale_weighted_unique_secondproductsentriesentryleft)) * S ((dst_negative_code_weighted_unique_secondproductsentriesentryleft) + (dst_negative_scale_weighted_unique_secondproductsentriesentryleft)) + ((dst_negative_scale_weighted_unique_secondproductsentriesentryleft) + (dst_negative_scale_weighted_unique_secondproductsentriesentryleft))) + (((dst_negative_code_weighted_unique_secondproductsentriesentryleft) + (dst_negative_scale_weighted_unique_secondproductsentriesentryleft)) * S ((dst_negative_code_weighted_unique_secondproductsentriesentryleft) + (dst_negative_scale_weighted_unique_secondproductsentriesentryleft)) + ((dst_negative_scale_weighted_unique_secondproductsentriesentryleft) + (dst_negative_scale_weighted_unique_secondproductsentriesentryleft)))))) /\ (((((exists ff_h_pvs_weighted_unique_secondproductsentriesentryleftpositive. ff_h_pvs_weighted_unique_secondproductsentriesentryleftpositive + S (dst_positive_weighted_unique_secondproductsentriesentryleft) = S ((S (sto_index_weighted_unique_secondproductsentries)) * dst_positive_scale_weighted_unique_secondproductsentriesentryleft)) /\ exists ff_q_pvs_weighted_unique_secondproductsentriesentryleftpositive. dst_positive_code_weighted_unique_secondproductsentriesentryleft = ff_q_pvs_weighted_unique_secondproductsentriesentryleftpositive * S ((S (sto_index_weighted_unique_secondproductsentries)) * dst_positive_scale_weighted_unique_secondproductsentriesentryleft) + (dst_positive_weighted_unique_secondproductsentriesentryleft))) /\ (((((exists ff_h_pvs_weighted_unique_secondproductsentriesentryleftnegative. ff_h_pvs_weighted_unique_secondproductsentriesentryleftnegative + S (dst_negative_weighted_unique_secondproductsentriesentryleft) = S ((S (sto_index_weighted_unique_secondproductsentries)) * dst_negative_scale_weighted_unique_secondproductsentriesentryleft)) /\ exists ff_q_pvs_weighted_unique_secondproductsentriesentryleftnegative. dst_negative_code_weighted_unique_secondproductsentriesentryleft = ff_q_pvs_weighted_unique_secondproductsentriesentryleftnegative * S ((S (sto_index_weighted_unique_secondproductsentries)) * dst_negative_scale_weighted_unique_secondproductsentriesentryleft) + (dst_negative_weighted_unique_secondproductsentriesentryleft))) /\ (exists ge_balance_positive_weighted_unique_secondproductsentriesentryleftvalue ge_balance_negative_weighted_unique_secondproductsentriesentryleftvalue. (((((sto_left_weighted_unique_secondproductsentries) = 2 * (ge_balance_positive_weighted_unique_secondproductsentriesentryleftvalue) /\ (ge_balance_negative_weighted_unique_secondproductsentriesentryleftvalue) = 0) \/ exists ge_signed_half_weighted_unique_secondproductsentriesentryleftvaluedecode. (((sto_left_weighted_unique_secondproductsentries) = 2 * ge_signed_half_weighted_unique_secondproductsentriesentryleftvaluedecode + 1 /\ (ge_balance_positive_weighted_unique_secondproductsentriesentryleftvalue) = 0) /\ (ge_balance_negative_weighted_unique_secondproductsentriesentryleftvalue) = S ge_signed_half_weighted_unique_secondproductsentriesentryleftvaluedecode))) /\ ((dst_positive_weighted_unique_secondproductsentriesentryleft) + ge_balance_negative_weighted_unique_secondproductsentriesentryleftvalue = (dst_negative_weighted_unique_secondproductsentriesentryleft) + ge_balance_positive_weighted_unique_secondproductsentriesentryleftvalue))))))))) /\ (((exists dst_positive_code_weighted_unique_secondproductsentriesentryright dst_positive_scale_weighted_unique_secondproductsentriesentryright dst_negative_code_weighted_unique_secondproductsentriesentryright dst_negative_scale_weighted_unique_secondproductsentriesentryright dst_positive_weighted_unique_secondproductsentriesentryright dst_negative_weighted_unique_secondproductsentriesentryright. (((F) = (((((dst_positive_code_weighted_unique_secondproductsentriesentryright) + (dst_positive_scale_weighted_unique_secondproductsentriesentryright)) * S ((dst_positive_code_weighted_unique_secondproductsentriesentryright) + (dst_positive_scale_weighted_unique_secondproductsentriesentryright)) + ((dst_positive_scale_weighted_unique_secondproductsentriesentryright) + (dst_positive_scale_weighted_unique_secondproductsentriesentryright))) + (((dst_negative_code_weighted_unique_secondproductsentriesentryright) + (dst_negative_scale_weighted_unique_secondproductsentriesentryright)) * S ((dst_negative_code_weighted_unique_secondproductsentriesentryright) + (dst_negative_scale_weighted_unique_secondproductsentriesentryright)) + ((dst_negative_scale_weighted_unique_secondproductsentriesentryright) + (dst_negative_scale_weighted_unique_secondproductsentriesentryright)))) * S ((((dst_positive_code_weighted_unique_secondproductsentriesentryright) + (dst_positive_scale_weighted_unique_secondproductsentriesentryright)) * S ((dst_positive_code_weighted_unique_secondproductsentriesentryright) + (dst_positive_scale_weighted_unique_secondproductsentriesentryright)) + ((dst_positive_scale_weighted_unique_secondproductsentriesentryright) + (dst_positive_scale_weighted_unique_secondproductsentriesentryright))) + (((dst_negative_code_weighted_unique_secondproductsentriesentryright) + (dst_negative_scale_weighted_unique_secondproductsentriesentryright)) * S ((dst_negative_code_weighted_unique_secondproductsentriesentryright) + (dst_negative_scale_weighted_unique_secondproductsentriesentryright)) + ((dst_negative_scale_weighted_unique_secondproductsentriesentryright) + (dst_negative_scale_weighted_unique_secondproductsentriesentryright)))) + ((((dst_negative_code_weighted_unique_secondproductsentriesentryright) + (dst_negative_scale_weighted_unique_secondproductsentriesentryright)) * S ((dst_negative_code_weighted_unique_secondproductsentriesentryright) + (dst_negative_scale_weighted_unique_secondproductsentriesentryright)) + ((dst_negative_scale_weighted_unique_secondproductsentriesentryright) + (dst_negative_scale_weighted_unique_secondproductsentriesentryright))) + (((dst_negative_code_weighted_unique_secondproductsentriesentryright) + (dst_negative_scale_weighted_unique_secondproductsentriesentryright)) * S ((dst_negative_code_weighted_unique_secondproductsentriesentryright) + (dst_negative_scale_weighted_unique_secondproductsentriesentryright)) + ((dst_negative_scale_weighted_unique_secondproductsentriesentryright) + (dst_negative_scale_weighted_unique_secondproductsentriesentryright)))))) /\ (((((exists ff_h_pvs_weighted_unique_secondproductsentriesentryrightpositive. ff_h_pvs_weighted_unique_secondproductsentriesentryrightpositive + S (dst_positive_weighted_unique_secondproductsentriesentryright) = S ((S (sto_index_weighted_unique_secondproductsentries)) * dst_positive_scale_weighted_unique_secondproductsentriesentryright)) /\ exists ff_q_pvs_weighted_unique_secondproductsentriesentryrightpositive. dst_positive_code_weighted_unique_secondproductsentriesentryright = ff_q_pvs_weighted_unique_secondproductsentriesentryrightpositive * S ((S (sto_index_weighted_unique_secondproductsentries)) * dst_positive_scale_weighted_unique_secondproductsentriesentryright) + (dst_positive_weighted_unique_secondproductsentriesentryright))) /\ (((((exists ff_h_pvs_weighted_unique_secondproductsentriesentryrightnegative. ff_h_pvs_weighted_unique_secondproductsentriesentryrightnegative + S (dst_negative_weighted_unique_secondproductsentriesentryright) = S ((S (sto_index_weighted_unique_secondproductsentries)) * dst_negative_scale_weighted_unique_secondproductsentriesentryright)) /\ exists ff_q_pvs_weighted_unique_secondproductsentriesentryrightnegative. dst_negative_code_weighted_unique_secondproductsentriesentryright = ff_q_pvs_weighted_unique_secondproductsentriesentryrightnegative * S ((S (sto_index_weighted_unique_secondproductsentries)) * dst_negative_scale_weighted_unique_secondproductsentriesentryright) + (dst_negative_weighted_unique_secondproductsentriesentryright))) /\ (exists ge_balance_positive_weighted_unique_secondproductsentriesentryrightvalue ge_balance_negative_weighted_unique_secondproductsentriesentryrightvalue. (((((sto_right_weighted_unique_secondproductsentries) = 2 * (ge_balance_positive_weighted_unique_secondproductsentriesentryrightvalue) /\ (ge_balance_negative_weighted_unique_secondproductsentriesentryrightvalue) = 0) \/ exists ge_signed_half_weighted_unique_secondproductsentriesentryrightvaluedecode. (((sto_right_weighted_unique_secondproductsentries) = 2 * ge_signed_half_weighted_unique_secondproductsentriesentryrightvaluedecode + 1 /\ (ge_balance_positive_weighted_unique_secondproductsentriesentryrightvalue) = 0) /\ (ge_balance_negative_weighted_unique_secondproductsentriesentryrightvalue) = S ge_signed_half_weighted_unique_secondproductsentriesentryrightvaluedecode))) /\ ((dst_positive_weighted_unique_secondproductsentriesentryright) + ge_balance_negative_weighted_unique_secondproductsentriesentryrightvalue = (dst_negative_weighted_unique_secondproductsentriesentryright) + ge_balance_positive_weighted_unique_secondproductsentriesentryrightvalue))))))))) /\ (((exists dst_positive_code_weighted_unique_secondproductsentriesentryoutput dst_positive_scale_weighted_unique_secondproductsentriesentryoutput dst_negative_code_weighted_unique_secondproductsentriesentryoutput dst_negative_scale_weighted_unique_secondproductsentriesentryoutput dst_positive_weighted_unique_secondproductsentriesentryoutput dst_negative_weighted_unique_secondproductsentriesentryoutput. (((sws_product_table_weighted_unique_second) = (((((dst_positive_code_weighted_unique_secondproductsentriesentryoutput) + (dst_positive_scale_weighted_unique_secondproductsentriesentryoutput)) * S ((dst_positive_code_weighted_unique_secondproductsentriesentryoutput) + (dst_positive_scale_weighted_unique_secondproductsentriesentryoutput)) + ((dst_positive_scale_weighted_unique_secondproductsentriesentryoutput) + (dst_positive_scale_weighted_unique_secondproductsentriesentryoutput))) + (((dst_negative_code_weighted_unique_secondproductsentriesentryoutput) + (dst_negative_scale_weighted_unique_secondproductsentriesentryoutput)) * S ((dst_negative_code_weighted_unique_secondproductsentriesentryoutput) + (dst_negative_scale_weighted_unique_secondproductsentriesentryoutput)) + ((dst_negative_scale_weighted_unique_secondproductsentriesentryoutput) + (dst_negative_scale_weighted_unique_secondproductsentriesentryoutput)))) * S ((((dst_positive_code_weighted_unique_secondproductsentriesentryoutput) + (dst_positive_scale_weighted_unique_secondproductsentriesentryoutput)) * S ((dst_positive_code_weighted_unique_secondproductsentriesentryoutput) + (dst_positive_scale_weighted_unique_secondproductsentriesentryoutput)) + ((dst_positive_scale_weighted_unique_secondproductsentriesentryoutput) + (dst_positive_scale_weighted_unique_secondproductsentriesentryoutput))) + (((dst_negative_code_weighted_unique_secondproductsentriesentryoutput) + (dst_negative_scale_weighted_unique_secondproductsentriesentryoutput)) * S ((dst_negative_code_weighted_unique_secondproductsentriesentryoutput) + (dst_negative_scale_weighted_unique_secondproductsentriesentryoutput)) + ((dst_negative_scale_weighted_unique_secondproductsentriesentryoutput) + (dst_negative_scale_weighted_unique_secondproductsentriesentryoutput)))) + ((((dst_negative_code_weighted_unique_secondproductsentriesentryoutput) + (dst_negative_scale_weighted_unique_secondproductsentriesentryoutput)) * S ((dst_negative_code_weighted_unique_secondproductsentriesentryoutput) + (dst_negative_scale_weighted_unique_secondproductsentriesentryoutput)) + ((dst_negative_scale_weighted_unique_secondproductsentriesentryoutput) + (dst_negative_scale_weighted_unique_secondproductsentriesentryoutput))) + (((dst_negative_code_weighted_unique_secondproductsentriesentryoutput) + (dst_negative_scale_weighted_unique_secondproductsentriesentryoutput)) * S ((dst_negative_code_weighted_unique_secondproductsentriesentryoutput) + (dst_negative_scale_weighted_unique_secondproductsentriesentryoutput)) + ((dst_negative_scale_weighted_unique_secondproductsentriesentryoutput) + (dst_negative_scale_weighted_unique_secondproductsentriesentryoutput)))))) /\ (((((exists ff_h_pvs_weighted_unique_secondproductsentriesentryoutputpositive. ff_h_pvs_weighted_unique_secondproductsentriesentryoutputpositive + S (dst_positive_weighted_unique_secondproductsentriesentryoutput) = S ((S (sto_index_weighted_unique_secondproductsentries)) * dst_positive_scale_weighted_unique_secondproductsentriesentryoutput)) /\ exists ff_q_pvs_weighted_unique_secondproductsentriesentryoutputpositive. dst_positive_code_weighted_unique_secondproductsentriesentryoutput = ff_q_pvs_weighted_unique_secondproductsentriesentryoutputpositive * S ((S (sto_index_weighted_unique_secondproductsentries)) * dst_positive_scale_weighted_unique_secondproductsentriesentryoutput) + (dst_positive_weighted_unique_secondproductsentriesentryoutput))) /\ (((((exists ff_h_pvs_weighted_unique_secondproductsentriesentryoutputnegative. ff_h_pvs_weighted_unique_secondproductsentriesentryoutputnegative + S (dst_negative_weighted_unique_secondproductsentriesentryoutput) = S ((S (sto_index_weighted_unique_secondproductsentries)) * dst_negative_scale_weighted_unique_secondproductsentriesentryoutput)) /\ exists ff_q_pvs_weighted_unique_secondproductsentriesentryoutputnegative. dst_negative_code_weighted_unique_secondproductsentriesentryoutput = ff_q_pvs_weighted_unique_secondproductsentriesentryoutputnegative * S ((S (sto_index_weighted_unique_secondproductsentries)) * dst_negative_scale_weighted_unique_secondproductsentriesentryoutput) + (dst_negative_weighted_unique_secondproductsentriesentryoutput))) /\ (exists ge_balance_positive_weighted_unique_secondproductsentriesentryoutputvalue ge_balance_negative_weighted_unique_secondproductsentriesentryoutputvalue. (((((sto_output_weighted_unique_secondproductsentries) = 2 * (ge_balance_positive_weighted_unique_secondproductsentriesentryoutputvalue) /\ (ge_balance_negative_weighted_unique_secondproductsentriesentryoutputvalue) = 0) \/ exists ge_signed_half_weighted_unique_secondproductsentriesentryoutputvaluedecode. (((sto_output_weighted_unique_secondproductsentries) = 2 * ge_signed_half_weighted_unique_secondproductsentriesentryoutputvaluedecode + 1 /\ (ge_balance_positive_weighted_unique_secondproductsentriesentryoutputvalue) = 0) /\ (ge_balance_negative_weighted_unique_secondproductsentriesentryoutputvalue) = S ge_signed_half_weighted_unique_secondproductsentriesentryoutputvaluedecode))) /\ ((dst_positive_weighted_unique_secondproductsentriesentryoutput) + ge_balance_negative_weighted_unique_secondproductsentriesentryoutputvalue = (dst_negative_weighted_unique_secondproductsentriesentryoutput) + ge_balance_positive_weighted_unique_secondproductsentriesentryoutputvalue))))))))) /\ (exists sto_ap_weighted_unique_secondproductsentriesentryoperation sto_an_weighted_unique_secondproductsentriesentryoperation sto_bp_weighted_unique_secondproductsentriesentryoperation sto_bn_weighted_unique_secondproductsentriesentryoperation sto_cp_weighted_unique_secondproductsentriesentryoperation sto_cn_weighted_unique_secondproductsentriesentryoperation. (((((sto_left_weighted_unique_secondproductsentries) = 2 * (sto_ap_weighted_unique_secondproductsentriesentryoperation) /\ (sto_an_weighted_unique_secondproductsentriesentryoperation) = 0) \/ exists ge_signed_half_weighted_unique_secondproductsentriesentryoperationleft. (((sto_left_weighted_unique_secondproductsentries) = 2 * ge_signed_half_weighted_unique_secondproductsentriesentryoperationleft + 1 /\ (sto_ap_weighted_unique_secondproductsentriesentryoperation) = 0) /\ (sto_an_weighted_unique_secondproductsentriesentryoperation) = S ge_signed_half_weighted_unique_secondproductsentriesentryoperationleft))) /\ ((((((sto_right_weighted_unique_secondproductsentries) = 2 * (sto_bp_weighted_unique_secondproductsentriesentryoperation) /\ (sto_bn_weighted_unique_secondproductsentriesentryoperation) = 0) \/ exists ge_signed_half_weighted_unique_secondproductsentriesentryoperationright. (((sto_right_weighted_unique_secondproductsentries) = 2 * ge_signed_half_weighted_unique_secondproductsentriesentryoperationright + 1 /\ (sto_bp_weighted_unique_secondproductsentriesentryoperation) = 0) /\ (sto_bn_weighted_unique_secondproductsentriesentryoperation) = S ge_signed_half_weighted_unique_secondproductsentriesentryoperationright))) /\ ((((((sto_output_weighted_unique_secondproductsentries) = 2 * (sto_cp_weighted_unique_secondproductsentriesentryoperation) /\ (sto_cn_weighted_unique_secondproductsentriesentryoperation) = 0) \/ exists ge_signed_half_weighted_unique_secondproductsentriesentryoperationoutput. (((sto_output_weighted_unique_secondproductsentries) = 2 * ge_signed_half_weighted_unique_secondproductsentriesentryoperationoutput + 1 /\ (sto_cp_weighted_unique_secondproductsentriesentryoperation) = 0) /\ (sto_cn_weighted_unique_secondproductsentriesentryoperation) = S ge_signed_half_weighted_unique_secondproductsentriesentryoperationoutput))) /\ ((sto_ap_weighted_unique_secondproductsentriesentryoperation * sto_bp_weighted_unique_secondproductsentriesentryoperation + sto_an_weighted_unique_secondproductsentriesentryoperation * sto_bn_weighted_unique_secondproductsentriesentryoperation) + sto_cn_weighted_unique_secondproductsentriesentryoperation = (sto_ap_weighted_unique_secondproductsentriesentryoperation * sto_bn_weighted_unique_secondproductsentriesentryoperation + sto_an_weighted_unique_secondproductsentriesentryoperation * sto_bp_weighted_unique_secondproductsentriesentryoperation) + sto_cp_weighted_unique_secondproductsentriesentryoperation))))))))))))))))))) /\ (exists dst_positive_code_weighted_unique_secondsum dst_positive_scale_weighted_unique_secondsum dst_negative_code_weighted_unique_secondsum dst_negative_scale_weighted_unique_secondsum dst_positive_sum_weighted_unique_secondsum dst_negative_sum_weighted_unique_secondsum. (((sws_product_table_weighted_unique_second) = (((((dst_positive_code_weighted_unique_secondsum) + (dst_positive_scale_weighted_unique_secondsum)) * S ((dst_positive_code_weighted_unique_secondsum) + (dst_positive_scale_weighted_unique_secondsum)) + ((dst_positive_scale_weighted_unique_secondsum) + (dst_positive_scale_weighted_unique_secondsum))) + (((dst_negative_code_weighted_unique_secondsum) + (dst_negative_scale_weighted_unique_secondsum)) * S ((dst_negative_code_weighted_unique_secondsum) + (dst_negative_scale_weighted_unique_secondsum)) + ((dst_negative_scale_weighted_unique_secondsum) + (dst_negative_scale_weighted_unique_secondsum)))) * S ((((dst_positive_code_weighted_unique_secondsum) + (dst_positive_scale_weighted_unique_secondsum)) * S ((dst_positive_code_weighted_unique_secondsum) + (dst_positive_scale_weighted_unique_secondsum)) + ((dst_positive_scale_weighted_unique_secondsum) + (dst_positive_scale_weighted_unique_secondsum))) + (((dst_negative_code_weighted_unique_secondsum) + (dst_negative_scale_weighted_unique_secondsum)) * S ((dst_negative_code_weighted_unique_secondsum) + (dst_negative_scale_weighted_unique_secondsum)) + ((dst_negative_scale_weighted_unique_secondsum) + (dst_negative_scale_weighted_unique_secondsum)))) + ((((dst_negative_code_weighted_unique_secondsum) + (dst_negative_scale_weighted_unique_secondsum)) * S ((dst_negative_code_weighted_unique_secondsum) + (dst_negative_scale_weighted_unique_secondsum)) + ((dst_negative_scale_weighted_unique_secondsum) + (dst_negative_scale_weighted_unique_secondsum))) + (((dst_negative_code_weighted_unique_secondsum) + (dst_negative_scale_weighted_unique_secondsum)) * S ((dst_negative_code_weighted_unique_secondsum) + (dst_negative_scale_weighted_unique_secondsum)) + ((dst_negative_scale_weighted_unique_secondsum) + (dst_negative_scale_weighted_unique_secondsum)))))) /\ (((exists fs_u_dst_weighted_unique_secondsumpositive fs_v_dst_weighted_unique_secondsumpositive. ((((exists fs_h_dst_weighted_unique_secondsumpositive_body_start. fs_h_dst_weighted_unique_secondsumpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_weighted_unique_secondsumpositive)) /\ exists fs_q_dst_weighted_unique_secondsumpositive_body_start. fs_u_dst_weighted_unique_secondsumpositive = fs_q_dst_weighted_unique_secondsumpositive_body_start * S ((S (0)) * fs_v_dst_weighted_unique_secondsumpositive) + (0))) /\ ((((exists fs_h_dst_weighted_unique_secondsumpositive_body_terminal. fs_h_dst_weighted_unique_secondsumpositive_body_terminal + S (dst_positive_sum_weighted_unique_secondsum) = S ((S (l)) * fs_v_dst_weighted_unique_secondsumpositive)) /\ exists fs_q_dst_weighted_unique_secondsumpositive_body_terminal. fs_u_dst_weighted_unique_secondsumpositive = fs_q_dst_weighted_unique_secondsumpositive_body_terminal * S ((S (l)) * fs_v_dst_weighted_unique_secondsumpositive) + (dst_positive_sum_weighted_unique_secondsum))) /\ forall fs_i_dst_weighted_unique_secondsumpositive_body_steps. (exists fs_lt_dst_weighted_unique_secondsumpositive_body_steps_bound. fs_lt_dst_weighted_unique_secondsumpositive_body_steps_bound + S fs_i_dst_weighted_unique_secondsumpositive_body_steps = l) -> exists fs_a_dst_weighted_unique_secondsumpositive_body_steps fs_r_dst_weighted_unique_secondsumpositive_body_steps fs_s_dst_weighted_unique_secondsumpositive_body_steps. ((((exists fs_h_dst_weighted_unique_secondsumpositive_body_steps_summand. fs_h_dst_weighted_unique_secondsumpositive_body_steps_summand + S (fs_a_dst_weighted_unique_secondsumpositive_body_steps) = S ((S (fs_i_dst_weighted_unique_secondsumpositive_body_steps)) * dst_positive_scale_weighted_unique_secondsum)) /\ exists fs_q_dst_weighted_unique_secondsumpositive_body_steps_summand. dst_positive_code_weighted_unique_secondsum = fs_q_dst_weighted_unique_secondsumpositive_body_steps_summand * S ((S (fs_i_dst_weighted_unique_secondsumpositive_body_steps)) * dst_positive_scale_weighted_unique_secondsum) + (fs_a_dst_weighted_unique_secondsumpositive_body_steps))) /\ ((((exists fs_h_dst_weighted_unique_secondsumpositive_body_steps_partial. fs_h_dst_weighted_unique_secondsumpositive_body_steps_partial + S (fs_r_dst_weighted_unique_secondsumpositive_body_steps) = S ((S (fs_i_dst_weighted_unique_secondsumpositive_body_steps)) * fs_v_dst_weighted_unique_secondsumpositive)) /\ exists fs_q_dst_weighted_unique_secondsumpositive_body_steps_partial. fs_u_dst_weighted_unique_secondsumpositive = fs_q_dst_weighted_unique_secondsumpositive_body_steps_partial * S ((S (fs_i_dst_weighted_unique_secondsumpositive_body_steps)) * fs_v_dst_weighted_unique_secondsumpositive) + (fs_r_dst_weighted_unique_secondsumpositive_body_steps))) /\ ((((exists fs_h_dst_weighted_unique_secondsumpositive_body_steps_successor. fs_h_dst_weighted_unique_secondsumpositive_body_steps_successor + S (fs_s_dst_weighted_unique_secondsumpositive_body_steps) = S ((S (S fs_i_dst_weighted_unique_secondsumpositive_body_steps)) * fs_v_dst_weighted_unique_secondsumpositive)) /\ exists fs_q_dst_weighted_unique_secondsumpositive_body_steps_successor. fs_u_dst_weighted_unique_secondsumpositive = fs_q_dst_weighted_unique_secondsumpositive_body_steps_successor * S ((S (S fs_i_dst_weighted_unique_secondsumpositive_body_steps)) * fs_v_dst_weighted_unique_secondsumpositive) + (fs_s_dst_weighted_unique_secondsumpositive_body_steps))) /\ fs_s_dst_weighted_unique_secondsumpositive_body_steps = fs_r_dst_weighted_unique_secondsumpositive_body_steps + fs_a_dst_weighted_unique_secondsumpositive_body_steps)))))) /\ (((exists fs_u_dst_weighted_unique_secondsumnegative fs_v_dst_weighted_unique_secondsumnegative. ((((exists fs_h_dst_weighted_unique_secondsumnegative_body_start. fs_h_dst_weighted_unique_secondsumnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_weighted_unique_secondsumnegative)) /\ exists fs_q_dst_weighted_unique_secondsumnegative_body_start. fs_u_dst_weighted_unique_secondsumnegative = fs_q_dst_weighted_unique_secondsumnegative_body_start * S ((S (0)) * fs_v_dst_weighted_unique_secondsumnegative) + (0))) /\ ((((exists fs_h_dst_weighted_unique_secondsumnegative_body_terminal. fs_h_dst_weighted_unique_secondsumnegative_body_terminal + S (dst_negative_sum_weighted_unique_secondsum) = S ((S (l)) * fs_v_dst_weighted_unique_secondsumnegative)) /\ exists fs_q_dst_weighted_unique_secondsumnegative_body_terminal. fs_u_dst_weighted_unique_secondsumnegative = fs_q_dst_weighted_unique_secondsumnegative_body_terminal * S ((S (l)) * fs_v_dst_weighted_unique_secondsumnegative) + (dst_negative_sum_weighted_unique_secondsum))) /\ forall fs_i_dst_weighted_unique_secondsumnegative_body_steps. (exists fs_lt_dst_weighted_unique_secondsumnegative_body_steps_bound. fs_lt_dst_weighted_unique_secondsumnegative_body_steps_bound + S fs_i_dst_weighted_unique_secondsumnegative_body_steps = l) -> exists fs_a_dst_weighted_unique_secondsumnegative_body_steps fs_r_dst_weighted_unique_secondsumnegative_body_steps fs_s_dst_weighted_unique_secondsumnegative_body_steps. ((((exists fs_h_dst_weighted_unique_secondsumnegative_body_steps_summand. fs_h_dst_weighted_unique_secondsumnegative_body_steps_summand + S (fs_a_dst_weighted_unique_secondsumnegative_body_steps) = S ((S (fs_i_dst_weighted_unique_secondsumnegative_body_steps)) * dst_negative_scale_weighted_unique_secondsum)) /\ exists fs_q_dst_weighted_unique_secondsumnegative_body_steps_summand. dst_negative_code_weighted_unique_secondsum = fs_q_dst_weighted_unique_secondsumnegative_body_steps_summand * S ((S (fs_i_dst_weighted_unique_secondsumnegative_body_steps)) * dst_negative_scale_weighted_unique_secondsum) + (fs_a_dst_weighted_unique_secondsumnegative_body_steps))) /\ ((((exists fs_h_dst_weighted_unique_secondsumnegative_body_steps_partial. fs_h_dst_weighted_unique_secondsumnegative_body_steps_partial + S (fs_r_dst_weighted_unique_secondsumnegative_body_steps) = S ((S (fs_i_dst_weighted_unique_secondsumnegative_body_steps)) * fs_v_dst_weighted_unique_secondsumnegative)) /\ exists fs_q_dst_weighted_unique_secondsumnegative_body_steps_partial. fs_u_dst_weighted_unique_secondsumnegative = fs_q_dst_weighted_unique_secondsumnegative_body_steps_partial * S ((S (fs_i_dst_weighted_unique_secondsumnegative_body_steps)) * fs_v_dst_weighted_unique_secondsumnegative) + (fs_r_dst_weighted_unique_secondsumnegative_body_steps))) /\ ((((exists fs_h_dst_weighted_unique_secondsumnegative_body_steps_successor. fs_h_dst_weighted_unique_secondsumnegative_body_steps_successor + S (fs_s_dst_weighted_unique_secondsumnegative_body_steps) = S ((S (S fs_i_dst_weighted_unique_secondsumnegative_body_steps)) * fs_v_dst_weighted_unique_secondsumnegative)) /\ exists fs_q_dst_weighted_unique_secondsumnegative_body_steps_successor. fs_u_dst_weighted_unique_secondsumnegative = fs_q_dst_weighted_unique_secondsumnegative_body_steps_successor * S ((S (S fs_i_dst_weighted_unique_secondsumnegative_body_steps)) * fs_v_dst_weighted_unique_secondsumnegative) + (fs_s_dst_weighted_unique_secondsumnegative_body_steps))) /\ fs_s_dst_weighted_unique_secondsumnegative_body_steps = fs_r_dst_weighted_unique_secondsumnegative_body_steps + fs_a_dst_weighted_unique_secondsumnegative_body_steps)))))) /\ (exists ge_balance_positive_weighted_unique_secondsumresult ge_balance_negative_weighted_unique_secondsumresult. (((((b) = 2 * (ge_balance_positive_weighted_unique_secondsumresult) /\ (ge_balance_negative_weighted_unique_secondsumresult) = 0) \/ exists ge_signed_half_weighted_unique_secondsumresultdecode. (((b) = 2 * ge_signed_half_weighted_unique_secondsumresultdecode + 1 /\ (ge_balance_positive_weighted_unique_secondsumresult) = 0) /\ (ge_balance_negative_weighted_unique_secondsumresult) = S ge_signed_half_weighted_unique_secondsumresultdecode))) /\ ((dst_positive_sum_weighted_unique_secondsum) + ge_balance_negative_weighted_unique_secondsumresult = (dst_negative_sum_weighted_unique_secondsum) + ge_balance_positive_weighted_unique_secondsumresult))))))))))) -> a = b