signed_weighted_sum_empty_value

Exact expanded first-order arithmetic statement

forall W F z. (exists sws_product_table_weighted_empty. ((((exists dst_positive_code_weighted_emptyproductsleft_table dst_positive_scale_weighted_emptyproductsleft_table dst_negative_code_weighted_emptyproductsleft_table dst_negative_scale_weighted_emptyproductsleft_table. (((W) = (((((dst_positive_code_weighted_emptyproductsleft_table) + (dst_positive_scale_weighted_emptyproductsleft_table)) * S ((dst_positive_code_weighted_emptyproductsleft_table) + (dst_positive_scale_weighted_emptyproductsleft_table)) + ((dst_positive_scale_weighted_emptyproductsleft_table) + (dst_positive_scale_weighted_emptyproductsleft_table))) + (((dst_negative_code_weighted_emptyproductsleft_table) + (dst_negative_scale_weighted_emptyproductsleft_table)) * S ((dst_negative_code_weighted_emptyproductsleft_table) + (dst_negative_scale_weighted_emptyproductsleft_table)) + ((dst_negative_scale_weighted_emptyproductsleft_table) + (dst_negative_scale_weighted_emptyproductsleft_table)))) * S ((((dst_positive_code_weighted_emptyproductsleft_table) + (dst_positive_scale_weighted_emptyproductsleft_table)) * S ((dst_positive_code_weighted_emptyproductsleft_table) + (dst_positive_scale_weighted_emptyproductsleft_table)) + ((dst_positive_scale_weighted_emptyproductsleft_table) + (dst_positive_scale_weighted_emptyproductsleft_table))) + (((dst_negative_code_weighted_emptyproductsleft_table) + (dst_negative_scale_weighted_emptyproductsleft_table)) * S ((dst_negative_code_weighted_emptyproductsleft_table) + (dst_negative_scale_weighted_emptyproductsleft_table)) + ((dst_negative_scale_weighted_emptyproductsleft_table) + (dst_negative_scale_weighted_emptyproductsleft_table)))) + ((((dst_negative_code_weighted_emptyproductsleft_table) + (dst_negative_scale_weighted_emptyproductsleft_table)) * S ((dst_negative_code_weighted_emptyproductsleft_table) + (dst_negative_scale_weighted_emptyproductsleft_table)) + ((dst_negative_scale_weighted_emptyproductsleft_table) + (dst_negative_scale_weighted_emptyproductsleft_table))) + (((dst_negative_code_weighted_emptyproductsleft_table) + (dst_negative_scale_weighted_emptyproductsleft_table)) * S ((dst_negative_code_weighted_emptyproductsleft_table) + (dst_negative_scale_weighted_emptyproductsleft_table)) + ((dst_negative_scale_weighted_emptyproductsleft_table) + (dst_negative_scale_weighted_emptyproductsleft_table)))))) /\ (forall dst_index_weighted_emptyproductsleft_table. (exists pvs_le_gap_weighted_emptyproductsleft_tabledomain. pvs_le_gap_weighted_emptyproductsleft_tabledomain + (dst_index_weighted_emptyproductsleft_table) = (0)) -> exists dst_positive_weighted_emptyproductsleft_table dst_negative_weighted_emptyproductsleft_table dst_value_weighted_emptyproductsleft_table. ((((exists ff_h_pvs_weighted_emptyproductsleft_tableentrypositive. ff_h_pvs_weighted_emptyproductsleft_tableentrypositive + S (dst_positive_weighted_emptyproductsleft_table) = S ((S (dst_index_weighted_emptyproductsleft_table)) * dst_positive_scale_weighted_emptyproductsleft_table)) /\ exists ff_q_pvs_weighted_emptyproductsleft_tableentrypositive. dst_positive_code_weighted_emptyproductsleft_table = ff_q_pvs_weighted_emptyproductsleft_tableentrypositive * S ((S (dst_index_weighted_emptyproductsleft_table)) * dst_positive_scale_weighted_emptyproductsleft_table) + (dst_positive_weighted_emptyproductsleft_table))) /\ (((((exists ff_h_pvs_weighted_emptyproductsleft_tableentrynegative. ff_h_pvs_weighted_emptyproductsleft_tableentrynegative + S (dst_negative_weighted_emptyproductsleft_table) = S ((S (dst_index_weighted_emptyproductsleft_table)) * dst_negative_scale_weighted_emptyproductsleft_table)) /\ exists ff_q_pvs_weighted_emptyproductsleft_tableentrynegative. dst_negative_code_weighted_emptyproductsleft_table = ff_q_pvs_weighted_emptyproductsleft_tableentrynegative * S ((S (dst_index_weighted_emptyproductsleft_table)) * dst_negative_scale_weighted_emptyproductsleft_table) + (dst_negative_weighted_emptyproductsleft_table))) /\ (exists ge_balance_positive_weighted_emptyproductsleft_tableentryvalue ge_balance_negative_weighted_emptyproductsleft_tableentryvalue. (((((dst_value_weighted_emptyproductsleft_table) = 2 * (ge_balance_positive_weighted_emptyproductsleft_tableentryvalue) /\ (ge_balance_negative_weighted_emptyproductsleft_tableentryvalue) = 0) \/ exists ge_signed_half_weighted_emptyproductsleft_tableentryvaluedecode. (((dst_value_weighted_emptyproductsleft_table) = 2 * ge_signed_half_weighted_emptyproductsleft_tableentryvaluedecode + 1 /\ (ge_balance_positive_weighted_emptyproductsleft_tableentryvalue) = 0) /\ (ge_balance_negative_weighted_emptyproductsleft_tableentryvalue) = S ge_signed_half_weighted_emptyproductsleft_tableentryvaluedecode))) /\ ((dst_positive_weighted_emptyproductsleft_table) + ge_balance_negative_weighted_emptyproductsleft_tableentryvalue = (dst_negative_weighted_emptyproductsleft_table) + ge_balance_positive_weighted_emptyproductsleft_tableentryvalue))))))))) /\ (((exists dst_positive_code_weighted_emptyproductsright_table dst_positive_scale_weighted_emptyproductsright_table dst_negative_code_weighted_emptyproductsright_table dst_negative_scale_weighted_emptyproductsright_table. (((F) = (((((dst_positive_code_weighted_emptyproductsright_table) + (dst_positive_scale_weighted_emptyproductsright_table)) * S ((dst_positive_code_weighted_emptyproductsright_table) + (dst_positive_scale_weighted_emptyproductsright_table)) + ((dst_positive_scale_weighted_emptyproductsright_table) + (dst_positive_scale_weighted_emptyproductsright_table))) + (((dst_negative_code_weighted_emptyproductsright_table) + (dst_negative_scale_weighted_emptyproductsright_table)) * S ((dst_negative_code_weighted_emptyproductsright_table) + (dst_negative_scale_weighted_emptyproductsright_table)) + ((dst_negative_scale_weighted_emptyproductsright_table) + (dst_negative_scale_weighted_emptyproductsright_table)))) * S ((((dst_positive_code_weighted_emptyproductsright_table) + (dst_positive_scale_weighted_emptyproductsright_table)) * S ((dst_positive_code_weighted_emptyproductsright_table) + (dst_positive_scale_weighted_emptyproductsright_table)) + ((dst_positive_scale_weighted_emptyproductsright_table) + (dst_positive_scale_weighted_emptyproductsright_table))) + (((dst_negative_code_weighted_emptyproductsright_table) + (dst_negative_scale_weighted_emptyproductsright_table)) * S ((dst_negative_code_weighted_emptyproductsright_table) + (dst_negative_scale_weighted_emptyproductsright_table)) + ((dst_negative_scale_weighted_emptyproductsright_table) + (dst_negative_scale_weighted_emptyproductsright_table)))) + ((((dst_negative_code_weighted_emptyproductsright_table) + (dst_negative_scale_weighted_emptyproductsright_table)) * S ((dst_negative_code_weighted_emptyproductsright_table) + (dst_negative_scale_weighted_emptyproductsright_table)) + ((dst_negative_scale_weighted_emptyproductsright_table) + (dst_negative_scale_weighted_emptyproductsright_table))) + (((dst_negative_code_weighted_emptyproductsright_table) + (dst_negative_scale_weighted_emptyproductsright_table)) * S ((dst_negative_code_weighted_emptyproductsright_table) + (dst_negative_scale_weighted_emptyproductsright_table)) + ((dst_negative_scale_weighted_emptyproductsright_table) + (dst_negative_scale_weighted_emptyproductsright_table)))))) /\ (forall dst_index_weighted_emptyproductsright_table. (exists pvs_le_gap_weighted_emptyproductsright_tabledomain. pvs_le_gap_weighted_emptyproductsright_tabledomain + (dst_index_weighted_emptyproductsright_table) = (0)) -> exists dst_positive_weighted_emptyproductsright_table dst_negative_weighted_emptyproductsright_table dst_value_weighted_emptyproductsright_table. ((((exists ff_h_pvs_weighted_emptyproductsright_tableentrypositive. ff_h_pvs_weighted_emptyproductsright_tableentrypositive + S (dst_positive_weighted_emptyproductsright_table) = S ((S (dst_index_weighted_emptyproductsright_table)) * dst_positive_scale_weighted_emptyproductsright_table)) /\ exists ff_q_pvs_weighted_emptyproductsright_tableentrypositive. dst_positive_code_weighted_emptyproductsright_table = ff_q_pvs_weighted_emptyproductsright_tableentrypositive * S ((S (dst_index_weighted_emptyproductsright_table)) * dst_positive_scale_weighted_emptyproductsright_table) + (dst_positive_weighted_emptyproductsright_table))) /\ (((((exists ff_h_pvs_weighted_emptyproductsright_tableentrynegative. ff_h_pvs_weighted_emptyproductsright_tableentrynegative + S (dst_negative_weighted_emptyproductsright_table) = S ((S (dst_index_weighted_emptyproductsright_table)) * dst_negative_scale_weighted_emptyproductsright_table)) /\ exists ff_q_pvs_weighted_emptyproductsright_tableentrynegative. dst_negative_code_weighted_emptyproductsright_table = ff_q_pvs_weighted_emptyproductsright_tableentrynegative * S ((S (dst_index_weighted_emptyproductsright_table)) * dst_negative_scale_weighted_emptyproductsright_table) + (dst_negative_weighted_emptyproductsright_table))) /\ (exists ge_balance_positive_weighted_emptyproductsright_tableentryvalue ge_balance_negative_weighted_emptyproductsright_tableentryvalue. (((((dst_value_weighted_emptyproductsright_table) = 2 * (ge_balance_positive_weighted_emptyproductsright_tableentryvalue) /\ (ge_balance_negative_weighted_emptyproductsright_tableentryvalue) = 0) \/ exists ge_signed_half_weighted_emptyproductsright_tableentryvaluedecode. (((dst_value_weighted_emptyproductsright_table) = 2 * ge_signed_half_weighted_emptyproductsright_tableentryvaluedecode + 1 /\ (ge_balance_positive_weighted_emptyproductsright_tableentryvalue) = 0) /\ (ge_balance_negative_weighted_emptyproductsright_tableentryvalue) = S ge_signed_half_weighted_emptyproductsright_tableentryvaluedecode))) /\ ((dst_positive_weighted_emptyproductsright_table) + ge_balance_negative_weighted_emptyproductsright_tableentryvalue = (dst_negative_weighted_emptyproductsright_table) + ge_balance_positive_weighted_emptyproductsright_tableentryvalue))))))))) /\ (((exists dst_positive_code_weighted_emptyproductsoutput_table dst_positive_scale_weighted_emptyproductsoutput_table dst_negative_code_weighted_emptyproductsoutput_table dst_negative_scale_weighted_emptyproductsoutput_table. (((sws_product_table_weighted_empty) = (((((dst_positive_code_weighted_emptyproductsoutput_table) + (dst_positive_scale_weighted_emptyproductsoutput_table)) * S ((dst_positive_code_weighted_emptyproductsoutput_table) + (dst_positive_scale_weighted_emptyproductsoutput_table)) + ((dst_positive_scale_weighted_emptyproductsoutput_table) + (dst_positive_scale_weighted_emptyproductsoutput_table))) + (((dst_negative_code_weighted_emptyproductsoutput_table) + (dst_negative_scale_weighted_emptyproductsoutput_table)) * S ((dst_negative_code_weighted_emptyproductsoutput_table) + (dst_negative_scale_weighted_emptyproductsoutput_table)) + ((dst_negative_scale_weighted_emptyproductsoutput_table) + (dst_negative_scale_weighted_emptyproductsoutput_table)))) * S ((((dst_positive_code_weighted_emptyproductsoutput_table) + (dst_positive_scale_weighted_emptyproductsoutput_table)) * S ((dst_positive_code_weighted_emptyproductsoutput_table) + (dst_positive_scale_weighted_emptyproductsoutput_table)) + ((dst_positive_scale_weighted_emptyproductsoutput_table) + (dst_positive_scale_weighted_emptyproductsoutput_table))) + (((dst_negative_code_weighted_emptyproductsoutput_table) + (dst_negative_scale_weighted_emptyproductsoutput_table)) * S ((dst_negative_code_weighted_emptyproductsoutput_table) + (dst_negative_scale_weighted_emptyproductsoutput_table)) + ((dst_negative_scale_weighted_emptyproductsoutput_table) + (dst_negative_scale_weighted_emptyproductsoutput_table)))) + ((((dst_negative_code_weighted_emptyproductsoutput_table) + (dst_negative_scale_weighted_emptyproductsoutput_table)) * S ((dst_negative_code_weighted_emptyproductsoutput_table) + (dst_negative_scale_weighted_emptyproductsoutput_table)) + ((dst_negative_scale_weighted_emptyproductsoutput_table) + (dst_negative_scale_weighted_emptyproductsoutput_table))) + (((dst_negative_code_weighted_emptyproductsoutput_table) + (dst_negative_scale_weighted_emptyproductsoutput_table)) * S ((dst_negative_code_weighted_emptyproductsoutput_table) + (dst_negative_scale_weighted_emptyproductsoutput_table)) + ((dst_negative_scale_weighted_emptyproductsoutput_table) + (dst_negative_scale_weighted_emptyproductsoutput_table)))))) /\ (forall dst_index_weighted_emptyproductsoutput_table. (exists pvs_le_gap_weighted_emptyproductsoutput_tabledomain. pvs_le_gap_weighted_emptyproductsoutput_tabledomain + (dst_index_weighted_emptyproductsoutput_table) = (0)) -> exists dst_positive_weighted_emptyproductsoutput_table dst_negative_weighted_emptyproductsoutput_table dst_value_weighted_emptyproductsoutput_table. ((((exists ff_h_pvs_weighted_emptyproductsoutput_tableentrypositive. ff_h_pvs_weighted_emptyproductsoutput_tableentrypositive + S (dst_positive_weighted_emptyproductsoutput_table) = S ((S (dst_index_weighted_emptyproductsoutput_table)) * dst_positive_scale_weighted_emptyproductsoutput_table)) /\ exists ff_q_pvs_weighted_emptyproductsoutput_tableentrypositive. dst_positive_code_weighted_emptyproductsoutput_table = ff_q_pvs_weighted_emptyproductsoutput_tableentrypositive * S ((S (dst_index_weighted_emptyproductsoutput_table)) * dst_positive_scale_weighted_emptyproductsoutput_table) + (dst_positive_weighted_emptyproductsoutput_table))) /\ (((((exists ff_h_pvs_weighted_emptyproductsoutput_tableentrynegative. ff_h_pvs_weighted_emptyproductsoutput_tableentrynegative + S (dst_negative_weighted_emptyproductsoutput_table) = S ((S (dst_index_weighted_emptyproductsoutput_table)) * dst_negative_scale_weighted_emptyproductsoutput_table)) /\ exists ff_q_pvs_weighted_emptyproductsoutput_tableentrynegative. dst_negative_code_weighted_emptyproductsoutput_table = ff_q_pvs_weighted_emptyproductsoutput_tableentrynegative * S ((S (dst_index_weighted_emptyproductsoutput_table)) * dst_negative_scale_weighted_emptyproductsoutput_table) + (dst_negative_weighted_emptyproductsoutput_table))) /\ (exists ge_balance_positive_weighted_emptyproductsoutput_tableentryvalue ge_balance_negative_weighted_emptyproductsoutput_tableentryvalue. (((((dst_value_weighted_emptyproductsoutput_table) = 2 * (ge_balance_positive_weighted_emptyproductsoutput_tableentryvalue) /\ (ge_balance_negative_weighted_emptyproductsoutput_tableentryvalue) = 0) \/ exists ge_signed_half_weighted_emptyproductsoutput_tableentryvaluedecode. (((dst_value_weighted_emptyproductsoutput_table) = 2 * ge_signed_half_weighted_emptyproductsoutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_weighted_emptyproductsoutput_tableentryvalue) = 0) /\ (ge_balance_negative_weighted_emptyproductsoutput_tableentryvalue) = S ge_signed_half_weighted_emptyproductsoutput_tableentryvaluedecode))) /\ ((dst_positive_weighted_emptyproductsoutput_table) + ge_balance_negative_weighted_emptyproductsoutput_tableentryvalue = (dst_negative_weighted_emptyproductsoutput_table) + ge_balance_positive_weighted_emptyproductsoutput_tableentryvalue))))))))) /\ (forall sto_index_weighted_emptyproductsentries. (exists pvs_gap_weighted_emptyproductsentriesbound. pvs_gap_weighted_emptyproductsentriesbound + S (sto_index_weighted_emptyproductsentries) = (0)) -> exists sto_left_weighted_emptyproductsentries sto_right_weighted_emptyproductsentries sto_output_weighted_emptyproductsentries. ((exists dst_positive_code_weighted_emptyproductsentriesentryleft dst_positive_scale_weighted_emptyproductsentriesentryleft dst_negative_code_weighted_emptyproductsentriesentryleft dst_negative_scale_weighted_emptyproductsentriesentryleft dst_positive_weighted_emptyproductsentriesentryleft dst_negative_weighted_emptyproductsentriesentryleft. (((W) = (((((dst_positive_code_weighted_emptyproductsentriesentryleft) + (dst_positive_scale_weighted_emptyproductsentriesentryleft)) * S ((dst_positive_code_weighted_emptyproductsentriesentryleft) + (dst_positive_scale_weighted_emptyproductsentriesentryleft)) + ((dst_positive_scale_weighted_emptyproductsentriesentryleft) + (dst_positive_scale_weighted_emptyproductsentriesentryleft))) + (((dst_negative_code_weighted_emptyproductsentriesentryleft) + (dst_negative_scale_weighted_emptyproductsentriesentryleft)) * S ((dst_negative_code_weighted_emptyproductsentriesentryleft) + (dst_negative_scale_weighted_emptyproductsentriesentryleft)) + ((dst_negative_scale_weighted_emptyproductsentriesentryleft) + (dst_negative_scale_weighted_emptyproductsentriesentryleft)))) * S ((((dst_positive_code_weighted_emptyproductsentriesentryleft) + (dst_positive_scale_weighted_emptyproductsentriesentryleft)) * S ((dst_positive_code_weighted_emptyproductsentriesentryleft) + (dst_positive_scale_weighted_emptyproductsentriesentryleft)) + ((dst_positive_scale_weighted_emptyproductsentriesentryleft) + (dst_positive_scale_weighted_emptyproductsentriesentryleft))) + (((dst_negative_code_weighted_emptyproductsentriesentryleft) + (dst_negative_scale_weighted_emptyproductsentriesentryleft)) * S ((dst_negative_code_weighted_emptyproductsentriesentryleft) + (dst_negative_scale_weighted_emptyproductsentriesentryleft)) + ((dst_negative_scale_weighted_emptyproductsentriesentryleft) + (dst_negative_scale_weighted_emptyproductsentriesentryleft)))) + ((((dst_negative_code_weighted_emptyproductsentriesentryleft) + (dst_negative_scale_weighted_emptyproductsentriesentryleft)) * S ((dst_negative_code_weighted_emptyproductsentriesentryleft) + (dst_negative_scale_weighted_emptyproductsentriesentryleft)) + ((dst_negative_scale_weighted_emptyproductsentriesentryleft) + (dst_negative_scale_weighted_emptyproductsentriesentryleft))) + (((dst_negative_code_weighted_emptyproductsentriesentryleft) + (dst_negative_scale_weighted_emptyproductsentriesentryleft)) * S ((dst_negative_code_weighted_emptyproductsentriesentryleft) + (dst_negative_scale_weighted_emptyproductsentriesentryleft)) + ((dst_negative_scale_weighted_emptyproductsentriesentryleft) + (dst_negative_scale_weighted_emptyproductsentriesentryleft)))))) /\ (((((exists ff_h_pvs_weighted_emptyproductsentriesentryleftpositive. ff_h_pvs_weighted_emptyproductsentriesentryleftpositive + S (dst_positive_weighted_emptyproductsentriesentryleft) = S ((S (sto_index_weighted_emptyproductsentries)) * dst_positive_scale_weighted_emptyproductsentriesentryleft)) /\ exists ff_q_pvs_weighted_emptyproductsentriesentryleftpositive. dst_positive_code_weighted_emptyproductsentriesentryleft = ff_q_pvs_weighted_emptyproductsentriesentryleftpositive * S ((S (sto_index_weighted_emptyproductsentries)) * dst_positive_scale_weighted_emptyproductsentriesentryleft) + (dst_positive_weighted_emptyproductsentriesentryleft))) /\ (((((exists ff_h_pvs_weighted_emptyproductsentriesentryleftnegative. ff_h_pvs_weighted_emptyproductsentriesentryleftnegative + S (dst_negative_weighted_emptyproductsentriesentryleft) = S ((S (sto_index_weighted_emptyproductsentries)) * dst_negative_scale_weighted_emptyproductsentriesentryleft)) /\ exists ff_q_pvs_weighted_emptyproductsentriesentryleftnegative. dst_negative_code_weighted_emptyproductsentriesentryleft = ff_q_pvs_weighted_emptyproductsentriesentryleftnegative * S ((S (sto_index_weighted_emptyproductsentries)) * dst_negative_scale_weighted_emptyproductsentriesentryleft) + (dst_negative_weighted_emptyproductsentriesentryleft))) /\ (exists ge_balance_positive_weighted_emptyproductsentriesentryleftvalue ge_balance_negative_weighted_emptyproductsentriesentryleftvalue. (((((sto_left_weighted_emptyproductsentries) = 2 * (ge_balance_positive_weighted_emptyproductsentriesentryleftvalue) /\ (ge_balance_negative_weighted_emptyproductsentriesentryleftvalue) = 0) \/ exists ge_signed_half_weighted_emptyproductsentriesentryleftvaluedecode. (((sto_left_weighted_emptyproductsentries) = 2 * ge_signed_half_weighted_emptyproductsentriesentryleftvaluedecode + 1 /\ (ge_balance_positive_weighted_emptyproductsentriesentryleftvalue) = 0) /\ (ge_balance_negative_weighted_emptyproductsentriesentryleftvalue) = S ge_signed_half_weighted_emptyproductsentriesentryleftvaluedecode))) /\ ((dst_positive_weighted_emptyproductsentriesentryleft) + ge_balance_negative_weighted_emptyproductsentriesentryleftvalue = (dst_negative_weighted_emptyproductsentriesentryleft) + ge_balance_positive_weighted_emptyproductsentriesentryleftvalue))))))))) /\ (((exists dst_positive_code_weighted_emptyproductsentriesentryright dst_positive_scale_weighted_emptyproductsentriesentryright dst_negative_code_weighted_emptyproductsentriesentryright dst_negative_scale_weighted_emptyproductsentriesentryright dst_positive_weighted_emptyproductsentriesentryright dst_negative_weighted_emptyproductsentriesentryright. (((F) = (((((dst_positive_code_weighted_emptyproductsentriesentryright) + (dst_positive_scale_weighted_emptyproductsentriesentryright)) * S ((dst_positive_code_weighted_emptyproductsentriesentryright) + (dst_positive_scale_weighted_emptyproductsentriesentryright)) + ((dst_positive_scale_weighted_emptyproductsentriesentryright) + (dst_positive_scale_weighted_emptyproductsentriesentryright))) + (((dst_negative_code_weighted_emptyproductsentriesentryright) + (dst_negative_scale_weighted_emptyproductsentriesentryright)) * S ((dst_negative_code_weighted_emptyproductsentriesentryright) + (dst_negative_scale_weighted_emptyproductsentriesentryright)) + ((dst_negative_scale_weighted_emptyproductsentriesentryright) + (dst_negative_scale_weighted_emptyproductsentriesentryright)))) * S ((((dst_positive_code_weighted_emptyproductsentriesentryright) + (dst_positive_scale_weighted_emptyproductsentriesentryright)) * S ((dst_positive_code_weighted_emptyproductsentriesentryright) + (dst_positive_scale_weighted_emptyproductsentriesentryright)) + ((dst_positive_scale_weighted_emptyproductsentriesentryright) + (dst_positive_scale_weighted_emptyproductsentriesentryright))) + (((dst_negative_code_weighted_emptyproductsentriesentryright) + (dst_negative_scale_weighted_emptyproductsentriesentryright)) * S ((dst_negative_code_weighted_emptyproductsentriesentryright) + (dst_negative_scale_weighted_emptyproductsentriesentryright)) + ((dst_negative_scale_weighted_emptyproductsentriesentryright) + (dst_negative_scale_weighted_emptyproductsentriesentryright)))) + ((((dst_negative_code_weighted_emptyproductsentriesentryright) + (dst_negative_scale_weighted_emptyproductsentriesentryright)) * S ((dst_negative_code_weighted_emptyproductsentriesentryright) + (dst_negative_scale_weighted_emptyproductsentriesentryright)) + ((dst_negative_scale_weighted_emptyproductsentriesentryright) + (dst_negative_scale_weighted_emptyproductsentriesentryright))) + (((dst_negative_code_weighted_emptyproductsentriesentryright) + (dst_negative_scale_weighted_emptyproductsentriesentryright)) * S ((dst_negative_code_weighted_emptyproductsentriesentryright) + (dst_negative_scale_weighted_emptyproductsentriesentryright)) + ((dst_negative_scale_weighted_emptyproductsentriesentryright) + (dst_negative_scale_weighted_emptyproductsentriesentryright)))))) /\ (((((exists ff_h_pvs_weighted_emptyproductsentriesentryrightpositive. ff_h_pvs_weighted_emptyproductsentriesentryrightpositive + S (dst_positive_weighted_emptyproductsentriesentryright) = S ((S (sto_index_weighted_emptyproductsentries)) * dst_positive_scale_weighted_emptyproductsentriesentryright)) /\ exists ff_q_pvs_weighted_emptyproductsentriesentryrightpositive. dst_positive_code_weighted_emptyproductsentriesentryright = ff_q_pvs_weighted_emptyproductsentriesentryrightpositive * S ((S (sto_index_weighted_emptyproductsentries)) * dst_positive_scale_weighted_emptyproductsentriesentryright) + (dst_positive_weighted_emptyproductsentriesentryright))) /\ (((((exists ff_h_pvs_weighted_emptyproductsentriesentryrightnegative. ff_h_pvs_weighted_emptyproductsentriesentryrightnegative + S (dst_negative_weighted_emptyproductsentriesentryright) = S ((S (sto_index_weighted_emptyproductsentries)) * dst_negative_scale_weighted_emptyproductsentriesentryright)) /\ exists ff_q_pvs_weighted_emptyproductsentriesentryrightnegative. dst_negative_code_weighted_emptyproductsentriesentryright = ff_q_pvs_weighted_emptyproductsentriesentryrightnegative * S ((S (sto_index_weighted_emptyproductsentries)) * dst_negative_scale_weighted_emptyproductsentriesentryright) + (dst_negative_weighted_emptyproductsentriesentryright))) /\ (exists ge_balance_positive_weighted_emptyproductsentriesentryrightvalue ge_balance_negative_weighted_emptyproductsentriesentryrightvalue. (((((sto_right_weighted_emptyproductsentries) = 2 * (ge_balance_positive_weighted_emptyproductsentriesentryrightvalue) /\ (ge_balance_negative_weighted_emptyproductsentriesentryrightvalue) = 0) \/ exists ge_signed_half_weighted_emptyproductsentriesentryrightvaluedecode. (((sto_right_weighted_emptyproductsentries) = 2 * ge_signed_half_weighted_emptyproductsentriesentryrightvaluedecode + 1 /\ (ge_balance_positive_weighted_emptyproductsentriesentryrightvalue) = 0) /\ (ge_balance_negative_weighted_emptyproductsentriesentryrightvalue) = S ge_signed_half_weighted_emptyproductsentriesentryrightvaluedecode))) /\ ((dst_positive_weighted_emptyproductsentriesentryright) + ge_balance_negative_weighted_emptyproductsentriesentryrightvalue = (dst_negative_weighted_emptyproductsentriesentryright) + ge_balance_positive_weighted_emptyproductsentriesentryrightvalue))))))))) /\ (((exists dst_positive_code_weighted_emptyproductsentriesentryoutput dst_positive_scale_weighted_emptyproductsentriesentryoutput dst_negative_code_weighted_emptyproductsentriesentryoutput dst_negative_scale_weighted_emptyproductsentriesentryoutput dst_positive_weighted_emptyproductsentriesentryoutput dst_negative_weighted_emptyproductsentriesentryoutput. (((sws_product_table_weighted_empty) = (((((dst_positive_code_weighted_emptyproductsentriesentryoutput) + (dst_positive_scale_weighted_emptyproductsentriesentryoutput)) * S ((dst_positive_code_weighted_emptyproductsentriesentryoutput) + (dst_positive_scale_weighted_emptyproductsentriesentryoutput)) + ((dst_positive_scale_weighted_emptyproductsentriesentryoutput) + (dst_positive_scale_weighted_emptyproductsentriesentryoutput))) + (((dst_negative_code_weighted_emptyproductsentriesentryoutput) + (dst_negative_scale_weighted_emptyproductsentriesentryoutput)) * S ((dst_negative_code_weighted_emptyproductsentriesentryoutput) + (dst_negative_scale_weighted_emptyproductsentriesentryoutput)) + ((dst_negative_scale_weighted_emptyproductsentriesentryoutput) + (dst_negative_scale_weighted_emptyproductsentriesentryoutput)))) * S ((((dst_positive_code_weighted_emptyproductsentriesentryoutput) + (dst_positive_scale_weighted_emptyproductsentriesentryoutput)) * S ((dst_positive_code_weighted_emptyproductsentriesentryoutput) + (dst_positive_scale_weighted_emptyproductsentriesentryoutput)) + ((dst_positive_scale_weighted_emptyproductsentriesentryoutput) + (dst_positive_scale_weighted_emptyproductsentriesentryoutput))) + (((dst_negative_code_weighted_emptyproductsentriesentryoutput) + (dst_negative_scale_weighted_emptyproductsentriesentryoutput)) * S ((dst_negative_code_weighted_emptyproductsentriesentryoutput) + (dst_negative_scale_weighted_emptyproductsentriesentryoutput)) + ((dst_negative_scale_weighted_emptyproductsentriesentryoutput) + (dst_negative_scale_weighted_emptyproductsentriesentryoutput)))) + ((((dst_negative_code_weighted_emptyproductsentriesentryoutput) + (dst_negative_scale_weighted_emptyproductsentriesentryoutput)) * S ((dst_negative_code_weighted_emptyproductsentriesentryoutput) + (dst_negative_scale_weighted_emptyproductsentriesentryoutput)) + ((dst_negative_scale_weighted_emptyproductsentriesentryoutput) + (dst_negative_scale_weighted_emptyproductsentriesentryoutput))) + (((dst_negative_code_weighted_emptyproductsentriesentryoutput) + (dst_negative_scale_weighted_emptyproductsentriesentryoutput)) * S ((dst_negative_code_weighted_emptyproductsentriesentryoutput) + (dst_negative_scale_weighted_emptyproductsentriesentryoutput)) + ((dst_negative_scale_weighted_emptyproductsentriesentryoutput) + (dst_negative_scale_weighted_emptyproductsentriesentryoutput)))))) /\ (((((exists ff_h_pvs_weighted_emptyproductsentriesentryoutputpositive. ff_h_pvs_weighted_emptyproductsentriesentryoutputpositive + S (dst_positive_weighted_emptyproductsentriesentryoutput) = S ((S (sto_index_weighted_emptyproductsentries)) * dst_positive_scale_weighted_emptyproductsentriesentryoutput)) /\ exists ff_q_pvs_weighted_emptyproductsentriesentryoutputpositive. dst_positive_code_weighted_emptyproductsentriesentryoutput = ff_q_pvs_weighted_emptyproductsentriesentryoutputpositive * S ((S (sto_index_weighted_emptyproductsentries)) * dst_positive_scale_weighted_emptyproductsentriesentryoutput) + (dst_positive_weighted_emptyproductsentriesentryoutput))) /\ (((((exists ff_h_pvs_weighted_emptyproductsentriesentryoutputnegative. ff_h_pvs_weighted_emptyproductsentriesentryoutputnegative + S (dst_negative_weighted_emptyproductsentriesentryoutput) = S ((S (sto_index_weighted_emptyproductsentries)) * dst_negative_scale_weighted_emptyproductsentriesentryoutput)) /\ exists ff_q_pvs_weighted_emptyproductsentriesentryoutputnegative. dst_negative_code_weighted_emptyproductsentriesentryoutput = ff_q_pvs_weighted_emptyproductsentriesentryoutputnegative * S ((S (sto_index_weighted_emptyproductsentries)) * dst_negative_scale_weighted_emptyproductsentriesentryoutput) + (dst_negative_weighted_emptyproductsentriesentryoutput))) /\ (exists ge_balance_positive_weighted_emptyproductsentriesentryoutputvalue ge_balance_negative_weighted_emptyproductsentriesentryoutputvalue. (((((sto_output_weighted_emptyproductsentries) = 2 * (ge_balance_positive_weighted_emptyproductsentriesentryoutputvalue) /\ (ge_balance_negative_weighted_emptyproductsentriesentryoutputvalue) = 0) \/ exists ge_signed_half_weighted_emptyproductsentriesentryoutputvaluedecode. (((sto_output_weighted_emptyproductsentries) = 2 * ge_signed_half_weighted_emptyproductsentriesentryoutputvaluedecode + 1 /\ (ge_balance_positive_weighted_emptyproductsentriesentryoutputvalue) = 0) /\ (ge_balance_negative_weighted_emptyproductsentriesentryoutputvalue) = S ge_signed_half_weighted_emptyproductsentriesentryoutputvaluedecode))) /\ ((dst_positive_weighted_emptyproductsentriesentryoutput) + ge_balance_negative_weighted_emptyproductsentriesentryoutputvalue = (dst_negative_weighted_emptyproductsentriesentryoutput) + ge_balance_positive_weighted_emptyproductsentriesentryoutputvalue))))))))) /\ (exists sto_ap_weighted_emptyproductsentriesentryoperation sto_an_weighted_emptyproductsentriesentryoperation sto_bp_weighted_emptyproductsentriesentryoperation sto_bn_weighted_emptyproductsentriesentryoperation sto_cp_weighted_emptyproductsentriesentryoperation sto_cn_weighted_emptyproductsentriesentryoperation. (((((sto_left_weighted_emptyproductsentries) = 2 * (sto_ap_weighted_emptyproductsentriesentryoperation) /\ (sto_an_weighted_emptyproductsentriesentryoperation) = 0) \/ exists ge_signed_half_weighted_emptyproductsentriesentryoperationleft. (((sto_left_weighted_emptyproductsentries) = 2 * ge_signed_half_weighted_emptyproductsentriesentryoperationleft + 1 /\ (sto_ap_weighted_emptyproductsentriesentryoperation) = 0) /\ (sto_an_weighted_emptyproductsentriesentryoperation) = S ge_signed_half_weighted_emptyproductsentriesentryoperationleft))) /\ ((((((sto_right_weighted_emptyproductsentries) = 2 * (sto_bp_weighted_emptyproductsentriesentryoperation) /\ (sto_bn_weighted_emptyproductsentriesentryoperation) = 0) \/ exists ge_signed_half_weighted_emptyproductsentriesentryoperationright. (((sto_right_weighted_emptyproductsentries) = 2 * ge_signed_half_weighted_emptyproductsentriesentryoperationright + 1 /\ (sto_bp_weighted_emptyproductsentriesentryoperation) = 0) /\ (sto_bn_weighted_emptyproductsentriesentryoperation) = S ge_signed_half_weighted_emptyproductsentriesentryoperationright))) /\ ((((((sto_output_weighted_emptyproductsentries) = 2 * (sto_cp_weighted_emptyproductsentriesentryoperation) /\ (sto_cn_weighted_emptyproductsentriesentryoperation) = 0) \/ exists ge_signed_half_weighted_emptyproductsentriesentryoperationoutput. (((sto_output_weighted_emptyproductsentries) = 2 * ge_signed_half_weighted_emptyproductsentriesentryoperationoutput + 1 /\ (sto_cp_weighted_emptyproductsentriesentryoperation) = 0) /\ (sto_cn_weighted_emptyproductsentriesentryoperation) = S ge_signed_half_weighted_emptyproductsentriesentryoperationoutput))) /\ ((sto_ap_weighted_emptyproductsentriesentryoperation * sto_bp_weighted_emptyproductsentriesentryoperation + sto_an_weighted_emptyproductsentriesentryoperation * sto_bn_weighted_emptyproductsentriesentryoperation) + sto_cn_weighted_emptyproductsentriesentryoperation = (sto_ap_weighted_emptyproductsentriesentryoperation * sto_bn_weighted_emptyproductsentriesentryoperation + sto_an_weighted_emptyproductsentriesentryoperation * sto_bp_weighted_emptyproductsentriesentryoperation) + sto_cp_weighted_emptyproductsentriesentryoperation))))))))))))))))))) /\ (exists dst_positive_code_weighted_emptysum dst_positive_scale_weighted_emptysum dst_negative_code_weighted_emptysum dst_negative_scale_weighted_emptysum dst_positive_sum_weighted_emptysum dst_negative_sum_weighted_emptysum. (((sws_product_table_weighted_empty) = (((((dst_positive_code_weighted_emptysum) + (dst_positive_scale_weighted_emptysum)) * S ((dst_positive_code_weighted_emptysum) + (dst_positive_scale_weighted_emptysum)) + ((dst_positive_scale_weighted_emptysum) + (dst_positive_scale_weighted_emptysum))) + (((dst_negative_code_weighted_emptysum) + (dst_negative_scale_weighted_emptysum)) * S ((dst_negative_code_weighted_emptysum) + (dst_negative_scale_weighted_emptysum)) + ((dst_negative_scale_weighted_emptysum) + (dst_negative_scale_weighted_emptysum)))) * S ((((dst_positive_code_weighted_emptysum) + (dst_positive_scale_weighted_emptysum)) * S ((dst_positive_code_weighted_emptysum) + (dst_positive_scale_weighted_emptysum)) + ((dst_positive_scale_weighted_emptysum) + (dst_positive_scale_weighted_emptysum))) + (((dst_negative_code_weighted_emptysum) + (dst_negative_scale_weighted_emptysum)) * S ((dst_negative_code_weighted_emptysum) + (dst_negative_scale_weighted_emptysum)) + ((dst_negative_scale_weighted_emptysum) + (dst_negative_scale_weighted_emptysum)))) + ((((dst_negative_code_weighted_emptysum) + (dst_negative_scale_weighted_emptysum)) * S ((dst_negative_code_weighted_emptysum) + (dst_negative_scale_weighted_emptysum)) + ((dst_negative_scale_weighted_emptysum) + (dst_negative_scale_weighted_emptysum))) + (((dst_negative_code_weighted_emptysum) + (dst_negative_scale_weighted_emptysum)) * S ((dst_negative_code_weighted_emptysum) + (dst_negative_scale_weighted_emptysum)) + ((dst_negative_scale_weighted_emptysum) + (dst_negative_scale_weighted_emptysum)))))) /\ (((exists fs_u_dst_weighted_emptysumpositive fs_v_dst_weighted_emptysumpositive. ((((exists fs_h_dst_weighted_emptysumpositive_body_start. fs_h_dst_weighted_emptysumpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_weighted_emptysumpositive)) /\ exists fs_q_dst_weighted_emptysumpositive_body_start. fs_u_dst_weighted_emptysumpositive = fs_q_dst_weighted_emptysumpositive_body_start * S ((S (0)) * fs_v_dst_weighted_emptysumpositive) + (0))) /\ ((((exists fs_h_dst_weighted_emptysumpositive_body_terminal. fs_h_dst_weighted_emptysumpositive_body_terminal + S (dst_positive_sum_weighted_emptysum) = S ((S (0)) * fs_v_dst_weighted_emptysumpositive)) /\ exists fs_q_dst_weighted_emptysumpositive_body_terminal. fs_u_dst_weighted_emptysumpositive = fs_q_dst_weighted_emptysumpositive_body_terminal * S ((S (0)) * fs_v_dst_weighted_emptysumpositive) + (dst_positive_sum_weighted_emptysum))) /\ forall fs_i_dst_weighted_emptysumpositive_body_steps. (exists fs_lt_dst_weighted_emptysumpositive_body_steps_bound. fs_lt_dst_weighted_emptysumpositive_body_steps_bound + S fs_i_dst_weighted_emptysumpositive_body_steps = 0) -> exists fs_a_dst_weighted_emptysumpositive_body_steps fs_r_dst_weighted_emptysumpositive_body_steps fs_s_dst_weighted_emptysumpositive_body_steps. ((((exists fs_h_dst_weighted_emptysumpositive_body_steps_summand. fs_h_dst_weighted_emptysumpositive_body_steps_summand + S (fs_a_dst_weighted_emptysumpositive_body_steps) = S ((S (fs_i_dst_weighted_emptysumpositive_body_steps)) * dst_positive_scale_weighted_emptysum)) /\ exists fs_q_dst_weighted_emptysumpositive_body_steps_summand. dst_positive_code_weighted_emptysum = fs_q_dst_weighted_emptysumpositive_body_steps_summand * S ((S (fs_i_dst_weighted_emptysumpositive_body_steps)) * dst_positive_scale_weighted_emptysum) + (fs_a_dst_weighted_emptysumpositive_body_steps))) /\ ((((exists fs_h_dst_weighted_emptysumpositive_body_steps_partial. fs_h_dst_weighted_emptysumpositive_body_steps_partial + S (fs_r_dst_weighted_emptysumpositive_body_steps) = S ((S (fs_i_dst_weighted_emptysumpositive_body_steps)) * fs_v_dst_weighted_emptysumpositive)) /\ exists fs_q_dst_weighted_emptysumpositive_body_steps_partial. fs_u_dst_weighted_emptysumpositive = fs_q_dst_weighted_emptysumpositive_body_steps_partial * S ((S (fs_i_dst_weighted_emptysumpositive_body_steps)) * fs_v_dst_weighted_emptysumpositive) + (fs_r_dst_weighted_emptysumpositive_body_steps))) /\ ((((exists fs_h_dst_weighted_emptysumpositive_body_steps_successor. fs_h_dst_weighted_emptysumpositive_body_steps_successor + S (fs_s_dst_weighted_emptysumpositive_body_steps) = S ((S (S fs_i_dst_weighted_emptysumpositive_body_steps)) * fs_v_dst_weighted_emptysumpositive)) /\ exists fs_q_dst_weighted_emptysumpositive_body_steps_successor. fs_u_dst_weighted_emptysumpositive = fs_q_dst_weighted_emptysumpositive_body_steps_successor * S ((S (S fs_i_dst_weighted_emptysumpositive_body_steps)) * fs_v_dst_weighted_emptysumpositive) + (fs_s_dst_weighted_emptysumpositive_body_steps))) /\ fs_s_dst_weighted_emptysumpositive_body_steps = fs_r_dst_weighted_emptysumpositive_body_steps + fs_a_dst_weighted_emptysumpositive_body_steps)))))) /\ (((exists fs_u_dst_weighted_emptysumnegative fs_v_dst_weighted_emptysumnegative. ((((exists fs_h_dst_weighted_emptysumnegative_body_start. fs_h_dst_weighted_emptysumnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_weighted_emptysumnegative)) /\ exists fs_q_dst_weighted_emptysumnegative_body_start. fs_u_dst_weighted_emptysumnegative = fs_q_dst_weighted_emptysumnegative_body_start * S ((S (0)) * fs_v_dst_weighted_emptysumnegative) + (0))) /\ ((((exists fs_h_dst_weighted_emptysumnegative_body_terminal. fs_h_dst_weighted_emptysumnegative_body_terminal + S (dst_negative_sum_weighted_emptysum) = S ((S (0)) * fs_v_dst_weighted_emptysumnegative)) /\ exists fs_q_dst_weighted_emptysumnegative_body_terminal. fs_u_dst_weighted_emptysumnegative = fs_q_dst_weighted_emptysumnegative_body_terminal * S ((S (0)) * fs_v_dst_weighted_emptysumnegative) + (dst_negative_sum_weighted_emptysum))) /\ forall fs_i_dst_weighted_emptysumnegative_body_steps. (exists fs_lt_dst_weighted_emptysumnegative_body_steps_bound. fs_lt_dst_weighted_emptysumnegative_body_steps_bound + S fs_i_dst_weighted_emptysumnegative_body_steps = 0) -> exists fs_a_dst_weighted_emptysumnegative_body_steps fs_r_dst_weighted_emptysumnegative_body_steps fs_s_dst_weighted_emptysumnegative_body_steps. ((((exists fs_h_dst_weighted_emptysumnegative_body_steps_summand. fs_h_dst_weighted_emptysumnegative_body_steps_summand + S (fs_a_dst_weighted_emptysumnegative_body_steps) = S ((S (fs_i_dst_weighted_emptysumnegative_body_steps)) * dst_negative_scale_weighted_emptysum)) /\ exists fs_q_dst_weighted_emptysumnegative_body_steps_summand. dst_negative_code_weighted_emptysum = fs_q_dst_weighted_emptysumnegative_body_steps_summand * S ((S (fs_i_dst_weighted_emptysumnegative_body_steps)) * dst_negative_scale_weighted_emptysum) + (fs_a_dst_weighted_emptysumnegative_body_steps))) /\ ((((exists fs_h_dst_weighted_emptysumnegative_body_steps_partial. fs_h_dst_weighted_emptysumnegative_body_steps_partial + S (fs_r_dst_weighted_emptysumnegative_body_steps) = S ((S (fs_i_dst_weighted_emptysumnegative_body_steps)) * fs_v_dst_weighted_emptysumnegative)) /\ exists fs_q_dst_weighted_emptysumnegative_body_steps_partial. fs_u_dst_weighted_emptysumnegative = fs_q_dst_weighted_emptysumnegative_body_steps_partial * S ((S (fs_i_dst_weighted_emptysumnegative_body_steps)) * fs_v_dst_weighted_emptysumnegative) + (fs_r_dst_weighted_emptysumnegative_body_steps))) /\ ((((exists fs_h_dst_weighted_emptysumnegative_body_steps_successor. fs_h_dst_weighted_emptysumnegative_body_steps_successor + S (fs_s_dst_weighted_emptysumnegative_body_steps) = S ((S (S fs_i_dst_weighted_emptysumnegative_body_steps)) * fs_v_dst_weighted_emptysumnegative)) /\ exists fs_q_dst_weighted_emptysumnegative_body_steps_successor. fs_u_dst_weighted_emptysumnegative = fs_q_dst_weighted_emptysumnegative_body_steps_successor * S ((S (S fs_i_dst_weighted_emptysumnegative_body_steps)) * fs_v_dst_weighted_emptysumnegative) + (fs_s_dst_weighted_emptysumnegative_body_steps))) /\ fs_s_dst_weighted_emptysumnegative_body_steps = fs_r_dst_weighted_emptysumnegative_body_steps + fs_a_dst_weighted_emptysumnegative_body_steps)))))) /\ (exists ge_balance_positive_weighted_emptysumresult ge_balance_negative_weighted_emptysumresult. (((((z) = 2 * (ge_balance_positive_weighted_emptysumresult) /\ (ge_balance_negative_weighted_emptysumresult) = 0) \/ exists ge_signed_half_weighted_emptysumresultdecode. (((z) = 2 * ge_signed_half_weighted_emptysumresultdecode + 1 /\ (ge_balance_positive_weighted_emptysumresult) = 0) /\ (ge_balance_negative_weighted_emptysumresult) = S ge_signed_half_weighted_emptysumresultdecode))) /\ ((dst_positive_sum_weighted_emptysum) + ge_balance_negative_weighted_emptysumresult = (dst_negative_sum_weighted_emptysum) + ge_balance_positive_weighted_emptysumresult))))))))))) -> z = 0