SignedWeightedSum(W,F,l,z)

exists sws_product_table_lowertier. ((((exists dst_positive_code_lowertierproductsleft_table dst_positive_scale_lowertierproductsleft_table dst_negative_code_lowertierproductsleft_table dst_negative_scale_lowertierproductsleft_table. ((((W)) = (((((dst_positive_code_lowertierproductsleft_table) + (dst_positive_scale_lowertierproductsleft_table)) * S ((dst_positive_code_lowertierproductsleft_table) + (dst_positive_scale_lowertierproductsleft_table)) + ((dst_positive_scale_lowertierproductsleft_table) + (dst_positive_scale_lowertierproductsleft_table))) + (((dst_negative_code_lowertierproductsleft_table) + (dst_negative_scale_lowertierproductsleft_table)) * S ((dst_negative_code_lowertierproductsleft_table) + (dst_negative_scale_lowertierproductsleft_table)) + ((dst_negative_scale_lowertierproductsleft_table) + (dst_negative_scale_lowertierproductsleft_table)))) * S ((((dst_positive_code_lowertierproductsleft_table) + (dst_positive_scale_lowertierproductsleft_table)) * S ((dst_positive_code_lowertierproductsleft_table) + (dst_positive_scale_lowertierproductsleft_table)) + ((dst_positive_scale_lowertierproductsleft_table) + (dst_positive_scale_lowertierproductsleft_table))) + (((dst_negative_code_lowertierproductsleft_table) + (dst_negative_scale_lowertierproductsleft_table)) * S ((dst_negative_code_lowertierproductsleft_table) + (dst_negative_scale_lowertierproductsleft_table)) + ((dst_negative_scale_lowertierproductsleft_table) + (dst_negative_scale_lowertierproductsleft_table)))) + ((((dst_negative_code_lowertierproductsleft_table) + (dst_negative_scale_lowertierproductsleft_table)) * S ((dst_negative_code_lowertierproductsleft_table) + (dst_negative_scale_lowertierproductsleft_table)) + ((dst_negative_scale_lowertierproductsleft_table) + (dst_negative_scale_lowertierproductsleft_table))) + (((dst_negative_code_lowertierproductsleft_table) + (dst_negative_scale_lowertierproductsleft_table)) * S ((dst_negative_code_lowertierproductsleft_table) + (dst_negative_scale_lowertierproductsleft_table)) + ((dst_negative_scale_lowertierproductsleft_table) + (dst_negative_scale_lowertierproductsleft_table)))))) /\ (forall dst_index_lowertierproductsleft_table. (exists pvs_le_gap_lowertierproductsleft_tabledomain. pvs_le_gap_lowertierproductsleft_tabledomain + (dst_index_lowertierproductsleft_table) = ((l))) -> exists dst_positive_lowertierproductsleft_table dst_negative_lowertierproductsleft_table dst_value_lowertierproductsleft_table. ((((exists ff_h_pvs_lowertierproductsleft_tableentrypositive. ff_h_pvs_lowertierproductsleft_tableentrypositive + S (dst_positive_lowertierproductsleft_table) = S ((S (dst_index_lowertierproductsleft_table)) * dst_positive_scale_lowertierproductsleft_table)) /\ exists ff_q_pvs_lowertierproductsleft_tableentrypositive. dst_positive_code_lowertierproductsleft_table = ff_q_pvs_lowertierproductsleft_tableentrypositive * S ((S (dst_index_lowertierproductsleft_table)) * dst_positive_scale_lowertierproductsleft_table) + (dst_positive_lowertierproductsleft_table))) /\ (((((exists ff_h_pvs_lowertierproductsleft_tableentrynegative. ff_h_pvs_lowertierproductsleft_tableentrynegative + S (dst_negative_lowertierproductsleft_table) = S ((S (dst_index_lowertierproductsleft_table)) * dst_negative_scale_lowertierproductsleft_table)) /\ exists ff_q_pvs_lowertierproductsleft_tableentrynegative. dst_negative_code_lowertierproductsleft_table = ff_q_pvs_lowertierproductsleft_tableentrynegative * S ((S (dst_index_lowertierproductsleft_table)) * dst_negative_scale_lowertierproductsleft_table) + (dst_negative_lowertierproductsleft_table))) /\ (exists ge_balance_positive_lowertierproductsleft_tableentryvalue ge_balance_negative_lowertierproductsleft_tableentryvalue. (((((dst_value_lowertierproductsleft_table) = 2 * (ge_balance_positive_lowertierproductsleft_tableentryvalue) /\ (ge_balance_negative_lowertierproductsleft_tableentryvalue) = 0) \/ exists ge_signed_half_lowertierproductsleft_tableentryvaluedecode. (((dst_value_lowertierproductsleft_table) = 2 * ge_signed_half_lowertierproductsleft_tableentryvaluedecode + 1 /\ (ge_balance_positive_lowertierproductsleft_tableentryvalue) = 0) /\ (ge_balance_negative_lowertierproductsleft_tableentryvalue) = S ge_signed_half_lowertierproductsleft_tableentryvaluedecode))) /\ ((dst_positive_lowertierproductsleft_table) + ge_balance_negative_lowertierproductsleft_tableentryvalue = (dst_negative_lowertierproductsleft_table) + ge_balance_positive_lowertierproductsleft_tableentryvalue))))))))) /\ (((exists dst_positive_code_lowertierproductsright_table dst_positive_scale_lowertierproductsright_table dst_negative_code_lowertierproductsright_table dst_negative_scale_lowertierproductsright_table. ((((F)) = (((((dst_positive_code_lowertierproductsright_table) + (dst_positive_scale_lowertierproductsright_table)) * S ((dst_positive_code_lowertierproductsright_table) + (dst_positive_scale_lowertierproductsright_table)) + ((dst_positive_scale_lowertierproductsright_table) + (dst_positive_scale_lowertierproductsright_table))) + (((dst_negative_code_lowertierproductsright_table) + (dst_negative_scale_lowertierproductsright_table)) * S ((dst_negative_code_lowertierproductsright_table) + (dst_negative_scale_lowertierproductsright_table)) + ((dst_negative_scale_lowertierproductsright_table) + (dst_negative_scale_lowertierproductsright_table)))) * S ((((dst_positive_code_lowertierproductsright_table) + (dst_positive_scale_lowertierproductsright_table)) * S ((dst_positive_code_lowertierproductsright_table) + (dst_positive_scale_lowertierproductsright_table)) + ((dst_positive_scale_lowertierproductsright_table) + (dst_positive_scale_lowertierproductsright_table))) + (((dst_negative_code_lowertierproductsright_table) + (dst_negative_scale_lowertierproductsright_table)) * S ((dst_negative_code_lowertierproductsright_table) + (dst_negative_scale_lowertierproductsright_table)) + ((dst_negative_scale_lowertierproductsright_table) + (dst_negative_scale_lowertierproductsright_table)))) + ((((dst_negative_code_lowertierproductsright_table) + (dst_negative_scale_lowertierproductsright_table)) * S ((dst_negative_code_lowertierproductsright_table) + (dst_negative_scale_lowertierproductsright_table)) + ((dst_negative_scale_lowertierproductsright_table) + (dst_negative_scale_lowertierproductsright_table))) + (((dst_negative_code_lowertierproductsright_table) + (dst_negative_scale_lowertierproductsright_table)) * S ((dst_negative_code_lowertierproductsright_table) + (dst_negative_scale_lowertierproductsright_table)) + ((dst_negative_scale_lowertierproductsright_table) + (dst_negative_scale_lowertierproductsright_table)))))) /\ (forall dst_index_lowertierproductsright_table. (exists pvs_le_gap_lowertierproductsright_tabledomain. pvs_le_gap_lowertierproductsright_tabledomain + (dst_index_lowertierproductsright_table) = ((l))) -> exists dst_positive_lowertierproductsright_table dst_negative_lowertierproductsright_table dst_value_lowertierproductsright_table. ((((exists ff_h_pvs_lowertierproductsright_tableentrypositive. ff_h_pvs_lowertierproductsright_tableentrypositive + S (dst_positive_lowertierproductsright_table) = S ((S (dst_index_lowertierproductsright_table)) * dst_positive_scale_lowertierproductsright_table)) /\ exists ff_q_pvs_lowertierproductsright_tableentrypositive. dst_positive_code_lowertierproductsright_table = ff_q_pvs_lowertierproductsright_tableentrypositive * S ((S (dst_index_lowertierproductsright_table)) * dst_positive_scale_lowertierproductsright_table) + (dst_positive_lowertierproductsright_table))) /\ (((((exists ff_h_pvs_lowertierproductsright_tableentrynegative. ff_h_pvs_lowertierproductsright_tableentrynegative + S (dst_negative_lowertierproductsright_table) = S ((S (dst_index_lowertierproductsright_table)) * dst_negative_scale_lowertierproductsright_table)) /\ exists ff_q_pvs_lowertierproductsright_tableentrynegative. dst_negative_code_lowertierproductsright_table = ff_q_pvs_lowertierproductsright_tableentrynegative * S ((S (dst_index_lowertierproductsright_table)) * dst_negative_scale_lowertierproductsright_table) + (dst_negative_lowertierproductsright_table))) /\ (exists ge_balance_positive_lowertierproductsright_tableentryvalue ge_balance_negative_lowertierproductsright_tableentryvalue. (((((dst_value_lowertierproductsright_table) = 2 * (ge_balance_positive_lowertierproductsright_tableentryvalue) /\ (ge_balance_negative_lowertierproductsright_tableentryvalue) = 0) \/ exists ge_signed_half_lowertierproductsright_tableentryvaluedecode. (((dst_value_lowertierproductsright_table) = 2 * ge_signed_half_lowertierproductsright_tableentryvaluedecode + 1 /\ (ge_balance_positive_lowertierproductsright_tableentryvalue) = 0) /\ (ge_balance_negative_lowertierproductsright_tableentryvalue) = S ge_signed_half_lowertierproductsright_tableentryvaluedecode))) /\ ((dst_positive_lowertierproductsright_table) + ge_balance_negative_lowertierproductsright_tableentryvalue = (dst_negative_lowertierproductsright_table) + ge_balance_positive_lowertierproductsright_tableentryvalue))))))))) /\ (((exists dst_positive_code_lowertierproductsoutput_table dst_positive_scale_lowertierproductsoutput_table dst_negative_code_lowertierproductsoutput_table dst_negative_scale_lowertierproductsoutput_table. (((sws_product_table_lowertier) = (((((dst_positive_code_lowertierproductsoutput_table) + (dst_positive_scale_lowertierproductsoutput_table)) * S ((dst_positive_code_lowertierproductsoutput_table) + (dst_positive_scale_lowertierproductsoutput_table)) + ((dst_positive_scale_lowertierproductsoutput_table) + (dst_positive_scale_lowertierproductsoutput_table))) + (((dst_negative_code_lowertierproductsoutput_table) + (dst_negative_scale_lowertierproductsoutput_table)) * S ((dst_negative_code_lowertierproductsoutput_table) + (dst_negative_scale_lowertierproductsoutput_table)) + ((dst_negative_scale_lowertierproductsoutput_table) + (dst_negative_scale_lowertierproductsoutput_table)))) * S ((((dst_positive_code_lowertierproductsoutput_table) + (dst_positive_scale_lowertierproductsoutput_table)) * S ((dst_positive_code_lowertierproductsoutput_table) + (dst_positive_scale_lowertierproductsoutput_table)) + ((dst_positive_scale_lowertierproductsoutput_table) + (dst_positive_scale_lowertierproductsoutput_table))) + (((dst_negative_code_lowertierproductsoutput_table) + (dst_negative_scale_lowertierproductsoutput_table)) * S ((dst_negative_code_lowertierproductsoutput_table) + (dst_negative_scale_lowertierproductsoutput_table)) + ((dst_negative_scale_lowertierproductsoutput_table) + (dst_negative_scale_lowertierproductsoutput_table)))) + ((((dst_negative_code_lowertierproductsoutput_table) + (dst_negative_scale_lowertierproductsoutput_table)) * S ((dst_negative_code_lowertierproductsoutput_table) + (dst_negative_scale_lowertierproductsoutput_table)) + ((dst_negative_scale_lowertierproductsoutput_table) + (dst_negative_scale_lowertierproductsoutput_table))) + (((dst_negative_code_lowertierproductsoutput_table) + (dst_negative_scale_lowertierproductsoutput_table)) * S ((dst_negative_code_lowertierproductsoutput_table) + (dst_negative_scale_lowertierproductsoutput_table)) + ((dst_negative_scale_lowertierproductsoutput_table) + (dst_negative_scale_lowertierproductsoutput_table)))))) /\ (forall dst_index_lowertierproductsoutput_table. (exists pvs_le_gap_lowertierproductsoutput_tabledomain. pvs_le_gap_lowertierproductsoutput_tabledomain + (dst_index_lowertierproductsoutput_table) = ((l))) -> exists dst_positive_lowertierproductsoutput_table dst_negative_lowertierproductsoutput_table dst_value_lowertierproductsoutput_table. ((((exists ff_h_pvs_lowertierproductsoutput_tableentrypositive. ff_h_pvs_lowertierproductsoutput_tableentrypositive + S (dst_positive_lowertierproductsoutput_table) = S ((S (dst_index_lowertierproductsoutput_table)) * dst_positive_scale_lowertierproductsoutput_table)) /\ exists ff_q_pvs_lowertierproductsoutput_tableentrypositive. dst_positive_code_lowertierproductsoutput_table = ff_q_pvs_lowertierproductsoutput_tableentrypositive * S ((S (dst_index_lowertierproductsoutput_table)) * dst_positive_scale_lowertierproductsoutput_table) + (dst_positive_lowertierproductsoutput_table))) /\ (((((exists ff_h_pvs_lowertierproductsoutput_tableentrynegative. ff_h_pvs_lowertierproductsoutput_tableentrynegative + S (dst_negative_lowertierproductsoutput_table) = S ((S (dst_index_lowertierproductsoutput_table)) * dst_negative_scale_lowertierproductsoutput_table)) /\ exists ff_q_pvs_lowertierproductsoutput_tableentrynegative. dst_negative_code_lowertierproductsoutput_table = ff_q_pvs_lowertierproductsoutput_tableentrynegative * S ((S (dst_index_lowertierproductsoutput_table)) * dst_negative_scale_lowertierproductsoutput_table) + (dst_negative_lowertierproductsoutput_table))) /\ (exists ge_balance_positive_lowertierproductsoutput_tableentryvalue ge_balance_negative_lowertierproductsoutput_tableentryvalue. (((((dst_value_lowertierproductsoutput_table) = 2 * (ge_balance_positive_lowertierproductsoutput_tableentryvalue) /\ (ge_balance_negative_lowertierproductsoutput_tableentryvalue) = 0) \/ exists ge_signed_half_lowertierproductsoutput_tableentryvaluedecode. (((dst_value_lowertierproductsoutput_table) = 2 * ge_signed_half_lowertierproductsoutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_lowertierproductsoutput_tableentryvalue) = 0) /\ (ge_balance_negative_lowertierproductsoutput_tableentryvalue) = S ge_signed_half_lowertierproductsoutput_tableentryvaluedecode))) /\ ((dst_positive_lowertierproductsoutput_table) + ge_balance_negative_lowertierproductsoutput_tableentryvalue = (dst_negative_lowertierproductsoutput_table) + ge_balance_positive_lowertierproductsoutput_tableentryvalue))))))))) /\ (forall sto_index_lowertierproductsentries. (exists pvs_gap_lowertierproductsentriesbound. pvs_gap_lowertierproductsentriesbound + S (sto_index_lowertierproductsentries) = ((l))) -> exists sto_left_lowertierproductsentries sto_right_lowertierproductsentries sto_output_lowertierproductsentries. ((exists dst_positive_code_lowertierproductsentriesentryleft dst_positive_scale_lowertierproductsentriesentryleft dst_negative_code_lowertierproductsentriesentryleft dst_negative_scale_lowertierproductsentriesentryleft dst_positive_lowertierproductsentriesentryleft dst_negative_lowertierproductsentriesentryleft. ((((W)) = (((((dst_positive_code_lowertierproductsentriesentryleft) + (dst_positive_scale_lowertierproductsentriesentryleft)) * S ((dst_positive_code_lowertierproductsentriesentryleft) + (dst_positive_scale_lowertierproductsentriesentryleft)) + ((dst_positive_scale_lowertierproductsentriesentryleft) + (dst_positive_scale_lowertierproductsentriesentryleft))) + (((dst_negative_code_lowertierproductsentriesentryleft) + (dst_negative_scale_lowertierproductsentriesentryleft)) * S ((dst_negative_code_lowertierproductsentriesentryleft) + (dst_negative_scale_lowertierproductsentriesentryleft)) + ((dst_negative_scale_lowertierproductsentriesentryleft) + (dst_negative_scale_lowertierproductsentriesentryleft)))) * S ((((dst_positive_code_lowertierproductsentriesentryleft) + (dst_positive_scale_lowertierproductsentriesentryleft)) * S ((dst_positive_code_lowertierproductsentriesentryleft) + (dst_positive_scale_lowertierproductsentriesentryleft)) + ((dst_positive_scale_lowertierproductsentriesentryleft) + (dst_positive_scale_lowertierproductsentriesentryleft))) + (((dst_negative_code_lowertierproductsentriesentryleft) + (dst_negative_scale_lowertierproductsentriesentryleft)) * S ((dst_negative_code_lowertierproductsentriesentryleft) + (dst_negative_scale_lowertierproductsentriesentryleft)) + ((dst_negative_scale_lowertierproductsentriesentryleft) + (dst_negative_scale_lowertierproductsentriesentryleft)))) + ((((dst_negative_code_lowertierproductsentriesentryleft) + (dst_negative_scale_lowertierproductsentriesentryleft)) * S ((dst_negative_code_lowertierproductsentriesentryleft) + (dst_negative_scale_lowertierproductsentriesentryleft)) + ((dst_negative_scale_lowertierproductsentriesentryleft) + (dst_negative_scale_lowertierproductsentriesentryleft))) + (((dst_negative_code_lowertierproductsentriesentryleft) + (dst_negative_scale_lowertierproductsentriesentryleft)) * S ((dst_negative_code_lowertierproductsentriesentryleft) + (dst_negative_scale_lowertierproductsentriesentryleft)) + ((dst_negative_scale_lowertierproductsentriesentryleft) + (dst_negative_scale_lowertierproductsentriesentryleft)))))) /\ (((((exists ff_h_pvs_lowertierproductsentriesentryleftpositive. ff_h_pvs_lowertierproductsentriesentryleftpositive + S (dst_positive_lowertierproductsentriesentryleft) = S ((S (sto_index_lowertierproductsentries)) * dst_positive_scale_lowertierproductsentriesentryleft)) /\ exists ff_q_pvs_lowertierproductsentriesentryleftpositive. dst_positive_code_lowertierproductsentriesentryleft = ff_q_pvs_lowertierproductsentriesentryleftpositive * S ((S (sto_index_lowertierproductsentries)) * dst_positive_scale_lowertierproductsentriesentryleft) + (dst_positive_lowertierproductsentriesentryleft))) /\ (((((exists ff_h_pvs_lowertierproductsentriesentryleftnegative. ff_h_pvs_lowertierproductsentriesentryleftnegative + S (dst_negative_lowertierproductsentriesentryleft) = S ((S (sto_index_lowertierproductsentries)) * dst_negative_scale_lowertierproductsentriesentryleft)) /\ exists ff_q_pvs_lowertierproductsentriesentryleftnegative. dst_negative_code_lowertierproductsentriesentryleft = ff_q_pvs_lowertierproductsentriesentryleftnegative * S ((S (sto_index_lowertierproductsentries)) * dst_negative_scale_lowertierproductsentriesentryleft) + (dst_negative_lowertierproductsentriesentryleft))) /\ (exists ge_balance_positive_lowertierproductsentriesentryleftvalue ge_balance_negative_lowertierproductsentriesentryleftvalue. (((((sto_left_lowertierproductsentries) = 2 * (ge_balance_positive_lowertierproductsentriesentryleftvalue) /\ (ge_balance_negative_lowertierproductsentriesentryleftvalue) = 0) \/ exists ge_signed_half_lowertierproductsentriesentryleftvaluedecode. (((sto_left_lowertierproductsentries) = 2 * ge_signed_half_lowertierproductsentriesentryleftvaluedecode + 1 /\ (ge_balance_positive_lowertierproductsentriesentryleftvalue) = 0) /\ (ge_balance_negative_lowertierproductsentriesentryleftvalue) = S ge_signed_half_lowertierproductsentriesentryleftvaluedecode))) /\ ((dst_positive_lowertierproductsentriesentryleft) + ge_balance_negative_lowertierproductsentriesentryleftvalue = (dst_negative_lowertierproductsentriesentryleft) + ge_balance_positive_lowertierproductsentriesentryleftvalue))))))))) /\ (((exists dst_positive_code_lowertierproductsentriesentryright dst_positive_scale_lowertierproductsentriesentryright dst_negative_code_lowertierproductsentriesentryright dst_negative_scale_lowertierproductsentriesentryright dst_positive_lowertierproductsentriesentryright dst_negative_lowertierproductsentriesentryright. ((((F)) = (((((dst_positive_code_lowertierproductsentriesentryright) + (dst_positive_scale_lowertierproductsentriesentryright)) * S ((dst_positive_code_lowertierproductsentriesentryright) + (dst_positive_scale_lowertierproductsentriesentryright)) + ((dst_positive_scale_lowertierproductsentriesentryright) + (dst_positive_scale_lowertierproductsentriesentryright))) + (((dst_negative_code_lowertierproductsentriesentryright) + (dst_negative_scale_lowertierproductsentriesentryright)) * S ((dst_negative_code_lowertierproductsentriesentryright) + (dst_negative_scale_lowertierproductsentriesentryright)) + ((dst_negative_scale_lowertierproductsentriesentryright) + (dst_negative_scale_lowertierproductsentriesentryright)))) * S ((((dst_positive_code_lowertierproductsentriesentryright) + (dst_positive_scale_lowertierproductsentriesentryright)) * S ((dst_positive_code_lowertierproductsentriesentryright) + (dst_positive_scale_lowertierproductsentriesentryright)) + ((dst_positive_scale_lowertierproductsentriesentryright) + (dst_positive_scale_lowertierproductsentriesentryright))) + (((dst_negative_code_lowertierproductsentriesentryright) + (dst_negative_scale_lowertierproductsentriesentryright)) * S ((dst_negative_code_lowertierproductsentriesentryright) + (dst_negative_scale_lowertierproductsentriesentryright)) + ((dst_negative_scale_lowertierproductsentriesentryright) + (dst_negative_scale_lowertierproductsentriesentryright)))) + ((((dst_negative_code_lowertierproductsentriesentryright) + (dst_negative_scale_lowertierproductsentriesentryright)) * S ((dst_negative_code_lowertierproductsentriesentryright) + (dst_negative_scale_lowertierproductsentriesentryright)) + ((dst_negative_scale_lowertierproductsentriesentryright) + (dst_negative_scale_lowertierproductsentriesentryright))) + (((dst_negative_code_lowertierproductsentriesentryright) + (dst_negative_scale_lowertierproductsentriesentryright)) * S ((dst_negative_code_lowertierproductsentriesentryright) + (dst_negative_scale_lowertierproductsentriesentryright)) + ((dst_negative_scale_lowertierproductsentriesentryright) + (dst_negative_scale_lowertierproductsentriesentryright)))))) /\ (((((exists ff_h_pvs_lowertierproductsentriesentryrightpositive. ff_h_pvs_lowertierproductsentriesentryrightpositive + S (dst_positive_lowertierproductsentriesentryright) = S ((S (sto_index_lowertierproductsentries)) * dst_positive_scale_lowertierproductsentriesentryright)) /\ exists ff_q_pvs_lowertierproductsentriesentryrightpositive. dst_positive_code_lowertierproductsentriesentryright = ff_q_pvs_lowertierproductsentriesentryrightpositive * S ((S (sto_index_lowertierproductsentries)) * dst_positive_scale_lowertierproductsentriesentryright) + (dst_positive_lowertierproductsentriesentryright))) /\ (((((exists ff_h_pvs_lowertierproductsentriesentryrightnegative. ff_h_pvs_lowertierproductsentriesentryrightnegative + S (dst_negative_lowertierproductsentriesentryright) = S ((S (sto_index_lowertierproductsentries)) * dst_negative_scale_lowertierproductsentriesentryright)) /\ exists ff_q_pvs_lowertierproductsentriesentryrightnegative. dst_negative_code_lowertierproductsentriesentryright = ff_q_pvs_lowertierproductsentriesentryrightnegative * S ((S (sto_index_lowertierproductsentries)) * dst_negative_scale_lowertierproductsentriesentryright) + (dst_negative_lowertierproductsentriesentryright))) /\ (exists ge_balance_positive_lowertierproductsentriesentryrightvalue ge_balance_negative_lowertierproductsentriesentryrightvalue. (((((sto_right_lowertierproductsentries) = 2 * (ge_balance_positive_lowertierproductsentriesentryrightvalue) /\ (ge_balance_negative_lowertierproductsentriesentryrightvalue) = 0) \/ exists ge_signed_half_lowertierproductsentriesentryrightvaluedecode. (((sto_right_lowertierproductsentries) = 2 * ge_signed_half_lowertierproductsentriesentryrightvaluedecode + 1 /\ (ge_balance_positive_lowertierproductsentriesentryrightvalue) = 0) /\ (ge_balance_negative_lowertierproductsentriesentryrightvalue) = S ge_signed_half_lowertierproductsentriesentryrightvaluedecode))) /\ ((dst_positive_lowertierproductsentriesentryright) + ge_balance_negative_lowertierproductsentriesentryrightvalue = (dst_negative_lowertierproductsentriesentryright) + ge_balance_positive_lowertierproductsentriesentryrightvalue))))))))) /\ (((exists dst_positive_code_lowertierproductsentriesentryoutput dst_positive_scale_lowertierproductsentriesentryoutput dst_negative_code_lowertierproductsentriesentryoutput dst_negative_scale_lowertierproductsentriesentryoutput dst_positive_lowertierproductsentriesentryoutput dst_negative_lowertierproductsentriesentryoutput. (((sws_product_table_lowertier) = (((((dst_positive_code_lowertierproductsentriesentryoutput) + (dst_positive_scale_lowertierproductsentriesentryoutput)) * S ((dst_positive_code_lowertierproductsentriesentryoutput) + (dst_positive_scale_lowertierproductsentriesentryoutput)) + ((dst_positive_scale_lowertierproductsentriesentryoutput) + (dst_positive_scale_lowertierproductsentriesentryoutput))) + (((dst_negative_code_lowertierproductsentriesentryoutput) + (dst_negative_scale_lowertierproductsentriesentryoutput)) * S ((dst_negative_code_lowertierproductsentriesentryoutput) + (dst_negative_scale_lowertierproductsentriesentryoutput)) + ((dst_negative_scale_lowertierproductsentriesentryoutput) + (dst_negative_scale_lowertierproductsentriesentryoutput)))) * S ((((dst_positive_code_lowertierproductsentriesentryoutput) + (dst_positive_scale_lowertierproductsentriesentryoutput)) * S ((dst_positive_code_lowertierproductsentriesentryoutput) + (dst_positive_scale_lowertierproductsentriesentryoutput)) + ((dst_positive_scale_lowertierproductsentriesentryoutput) + (dst_positive_scale_lowertierproductsentriesentryoutput))) + (((dst_negative_code_lowertierproductsentriesentryoutput) + (dst_negative_scale_lowertierproductsentriesentryoutput)) * S ((dst_negative_code_lowertierproductsentriesentryoutput) + (dst_negative_scale_lowertierproductsentriesentryoutput)) + ((dst_negative_scale_lowertierproductsentriesentryoutput) + (dst_negative_scale_lowertierproductsentriesentryoutput)))) + ((((dst_negative_code_lowertierproductsentriesentryoutput) + (dst_negative_scale_lowertierproductsentriesentryoutput)) * S ((dst_negative_code_lowertierproductsentriesentryoutput) + (dst_negative_scale_lowertierproductsentriesentryoutput)) + ((dst_negative_scale_lowertierproductsentriesentryoutput) + (dst_negative_scale_lowertierproductsentriesentryoutput))) + (((dst_negative_code_lowertierproductsentriesentryoutput) + (dst_negative_scale_lowertierproductsentriesentryoutput)) * S ((dst_negative_code_lowertierproductsentriesentryoutput) + (dst_negative_scale_lowertierproductsentriesentryoutput)) + ((dst_negative_scale_lowertierproductsentriesentryoutput) + (dst_negative_scale_lowertierproductsentriesentryoutput)))))) /\ (((((exists ff_h_pvs_lowertierproductsentriesentryoutputpositive. ff_h_pvs_lowertierproductsentriesentryoutputpositive + S (dst_positive_lowertierproductsentriesentryoutput) = S ((S (sto_index_lowertierproductsentries)) * dst_positive_scale_lowertierproductsentriesentryoutput)) /\ exists ff_q_pvs_lowertierproductsentriesentryoutputpositive. dst_positive_code_lowertierproductsentriesentryoutput = ff_q_pvs_lowertierproductsentriesentryoutputpositive * S ((S (sto_index_lowertierproductsentries)) * dst_positive_scale_lowertierproductsentriesentryoutput) + (dst_positive_lowertierproductsentriesentryoutput))) /\ (((((exists ff_h_pvs_lowertierproductsentriesentryoutputnegative. ff_h_pvs_lowertierproductsentriesentryoutputnegative + S (dst_negative_lowertierproductsentriesentryoutput) = S ((S (sto_index_lowertierproductsentries)) * dst_negative_scale_lowertierproductsentriesentryoutput)) /\ exists ff_q_pvs_lowertierproductsentriesentryoutputnegative. dst_negative_code_lowertierproductsentriesentryoutput = ff_q_pvs_lowertierproductsentriesentryoutputnegative * S ((S (sto_index_lowertierproductsentries)) * dst_negative_scale_lowertierproductsentriesentryoutput) + (dst_negative_lowertierproductsentriesentryoutput))) /\ (exists ge_balance_positive_lowertierproductsentriesentryoutputvalue ge_balance_negative_lowertierproductsentriesentryoutputvalue. (((((sto_output_lowertierproductsentries) = 2 * (ge_balance_positive_lowertierproductsentriesentryoutputvalue) /\ (ge_balance_negative_lowertierproductsentriesentryoutputvalue) = 0) \/ exists ge_signed_half_lowertierproductsentriesentryoutputvaluedecode. (((sto_output_lowertierproductsentries) = 2 * ge_signed_half_lowertierproductsentriesentryoutputvaluedecode + 1 /\ (ge_balance_positive_lowertierproductsentriesentryoutputvalue) = 0) /\ (ge_balance_negative_lowertierproductsentriesentryoutputvalue) = S ge_signed_half_lowertierproductsentriesentryoutputvaluedecode))) /\ ((dst_positive_lowertierproductsentriesentryoutput) + ge_balance_negative_lowertierproductsentriesentryoutputvalue = (dst_negative_lowertierproductsentriesentryoutput) + ge_balance_positive_lowertierproductsentriesentryoutputvalue))))))))) /\ (exists sto_ap_lowertierproductsentriesentryoperation sto_an_lowertierproductsentriesentryoperation sto_bp_lowertierproductsentriesentryoperation sto_bn_lowertierproductsentriesentryoperation sto_cp_lowertierproductsentriesentryoperation sto_cn_lowertierproductsentriesentryoperation. (((((sto_left_lowertierproductsentries) = 2 * (sto_ap_lowertierproductsentriesentryoperation) /\ (sto_an_lowertierproductsentriesentryoperation) = 0) \/ exists ge_signed_half_lowertierproductsentriesentryoperationleft. (((sto_left_lowertierproductsentries) = 2 * ge_signed_half_lowertierproductsentriesentryoperationleft + 1 /\ (sto_ap_lowertierproductsentriesentryoperation) = 0) /\ (sto_an_lowertierproductsentriesentryoperation) = S ge_signed_half_lowertierproductsentriesentryoperationleft))) /\ ((((((sto_right_lowertierproductsentries) = 2 * (sto_bp_lowertierproductsentriesentryoperation) /\ (sto_bn_lowertierproductsentriesentryoperation) = 0) \/ exists ge_signed_half_lowertierproductsentriesentryoperationright. (((sto_right_lowertierproductsentries) = 2 * ge_signed_half_lowertierproductsentriesentryoperationright + 1 /\ (sto_bp_lowertierproductsentriesentryoperation) = 0) /\ (sto_bn_lowertierproductsentriesentryoperation) = S ge_signed_half_lowertierproductsentriesentryoperationright))) /\ ((((((sto_output_lowertierproductsentries) = 2 * (sto_cp_lowertierproductsentriesentryoperation) /\ (sto_cn_lowertierproductsentriesentryoperation) = 0) \/ exists ge_signed_half_lowertierproductsentriesentryoperationoutput. (((sto_output_lowertierproductsentries) = 2 * ge_signed_half_lowertierproductsentriesentryoperationoutput + 1 /\ (sto_cp_lowertierproductsentriesentryoperation) = 0) /\ (sto_cn_lowertierproductsentriesentryoperation) = S ge_signed_half_lowertierproductsentriesentryoperationoutput))) /\ ((sto_ap_lowertierproductsentriesentryoperation * sto_bp_lowertierproductsentriesentryoperation + sto_an_lowertierproductsentriesentryoperation * sto_bn_lowertierproductsentriesentryoperation) + sto_cn_lowertierproductsentriesentryoperation = (sto_ap_lowertierproductsentriesentryoperation * sto_bn_lowertierproductsentriesentryoperation + sto_an_lowertierproductsentriesentryoperation * sto_bp_lowertierproductsentriesentryoperation) + sto_cp_lowertierproductsentriesentryoperation))))))))))))))))))) /\ (exists dst_positive_code_lowertiersum dst_positive_scale_lowertiersum dst_negative_code_lowertiersum dst_negative_scale_lowertiersum dst_positive_sum_lowertiersum dst_negative_sum_lowertiersum. (((sws_product_table_lowertier) = (((((dst_positive_code_lowertiersum) + (dst_positive_scale_lowertiersum)) * S ((dst_positive_code_lowertiersum) + (dst_positive_scale_lowertiersum)) + ((dst_positive_scale_lowertiersum) + (dst_positive_scale_lowertiersum))) + (((dst_negative_code_lowertiersum) + (dst_negative_scale_lowertiersum)) * S ((dst_negative_code_lowertiersum) + (dst_negative_scale_lowertiersum)) + ((dst_negative_scale_lowertiersum) + (dst_negative_scale_lowertiersum)))) * S ((((dst_positive_code_lowertiersum) + (dst_positive_scale_lowertiersum)) * S ((dst_positive_code_lowertiersum) + (dst_positive_scale_lowertiersum)) + ((dst_positive_scale_lowertiersum) + (dst_positive_scale_lowertiersum))) + (((dst_negative_code_lowertiersum) + (dst_negative_scale_lowertiersum)) * S ((dst_negative_code_lowertiersum) + (dst_negative_scale_lowertiersum)) + ((dst_negative_scale_lowertiersum) + (dst_negative_scale_lowertiersum)))) + ((((dst_negative_code_lowertiersum) + (dst_negative_scale_lowertiersum)) * S ((dst_negative_code_lowertiersum) + (dst_negative_scale_lowertiersum)) + ((dst_negative_scale_lowertiersum) + (dst_negative_scale_lowertiersum))) + (((dst_negative_code_lowertiersum) + (dst_negative_scale_lowertiersum)) * S ((dst_negative_code_lowertiersum) + (dst_negative_scale_lowertiersum)) + ((dst_negative_scale_lowertiersum) + (dst_negative_scale_lowertiersum)))))) /\ (((exists fs_u_dst_lowertiersumpositive fs_v_dst_lowertiersumpositive. ((((exists fs_h_dst_lowertiersumpositive_body_start. fs_h_dst_lowertiersumpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_lowertiersumpositive)) /\ exists fs_q_dst_lowertiersumpositive_body_start. fs_u_dst_lowertiersumpositive = fs_q_dst_lowertiersumpositive_body_start * S ((S (0)) * fs_v_dst_lowertiersumpositive) + (0))) /\ ((((exists fs_h_dst_lowertiersumpositive_body_terminal. fs_h_dst_lowertiersumpositive_body_terminal + S (dst_positive_sum_lowertiersum) = S ((S ((l))) * fs_v_dst_lowertiersumpositive)) /\ exists fs_q_dst_lowertiersumpositive_body_terminal. fs_u_dst_lowertiersumpositive = fs_q_dst_lowertiersumpositive_body_terminal * S ((S ((l))) * fs_v_dst_lowertiersumpositive) + (dst_positive_sum_lowertiersum))) /\ forall fs_i_dst_lowertiersumpositive_body_steps. (exists fs_lt_dst_lowertiersumpositive_body_steps_bound. fs_lt_dst_lowertiersumpositive_body_steps_bound + S fs_i_dst_lowertiersumpositive_body_steps = (l)) -> exists fs_a_dst_lowertiersumpositive_body_steps fs_r_dst_lowertiersumpositive_body_steps fs_s_dst_lowertiersumpositive_body_steps. ((((exists fs_h_dst_lowertiersumpositive_body_steps_summand. fs_h_dst_lowertiersumpositive_body_steps_summand + S (fs_a_dst_lowertiersumpositive_body_steps) = S ((S (fs_i_dst_lowertiersumpositive_body_steps)) * dst_positive_scale_lowertiersum)) /\ exists fs_q_dst_lowertiersumpositive_body_steps_summand. dst_positive_code_lowertiersum = fs_q_dst_lowertiersumpositive_body_steps_summand * S ((S (fs_i_dst_lowertiersumpositive_body_steps)) * dst_positive_scale_lowertiersum) + (fs_a_dst_lowertiersumpositive_body_steps))) /\ ((((exists fs_h_dst_lowertiersumpositive_body_steps_partial. fs_h_dst_lowertiersumpositive_body_steps_partial + S (fs_r_dst_lowertiersumpositive_body_steps) = S ((S (fs_i_dst_lowertiersumpositive_body_steps)) * fs_v_dst_lowertiersumpositive)) /\ exists fs_q_dst_lowertiersumpositive_body_steps_partial. fs_u_dst_lowertiersumpositive = fs_q_dst_lowertiersumpositive_body_steps_partial * S ((S (fs_i_dst_lowertiersumpositive_body_steps)) * fs_v_dst_lowertiersumpositive) + (fs_r_dst_lowertiersumpositive_body_steps))) /\ ((((exists fs_h_dst_lowertiersumpositive_body_steps_successor. fs_h_dst_lowertiersumpositive_body_steps_successor + S (fs_s_dst_lowertiersumpositive_body_steps) = S ((S (S fs_i_dst_lowertiersumpositive_body_steps)) * fs_v_dst_lowertiersumpositive)) /\ exists fs_q_dst_lowertiersumpositive_body_steps_successor. fs_u_dst_lowertiersumpositive = fs_q_dst_lowertiersumpositive_body_steps_successor * S ((S (S fs_i_dst_lowertiersumpositive_body_steps)) * fs_v_dst_lowertiersumpositive) + (fs_s_dst_lowertiersumpositive_body_steps))) /\ fs_s_dst_lowertiersumpositive_body_steps = fs_r_dst_lowertiersumpositive_body_steps + fs_a_dst_lowertiersumpositive_body_steps)))))) /\ (((exists fs_u_dst_lowertiersumnegative fs_v_dst_lowertiersumnegative. ((((exists fs_h_dst_lowertiersumnegative_body_start. fs_h_dst_lowertiersumnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_lowertiersumnegative)) /\ exists fs_q_dst_lowertiersumnegative_body_start. fs_u_dst_lowertiersumnegative = fs_q_dst_lowertiersumnegative_body_start * S ((S (0)) * fs_v_dst_lowertiersumnegative) + (0))) /\ ((((exists fs_h_dst_lowertiersumnegative_body_terminal. fs_h_dst_lowertiersumnegative_body_terminal + S (dst_negative_sum_lowertiersum) = S ((S ((l))) * fs_v_dst_lowertiersumnegative)) /\ exists fs_q_dst_lowertiersumnegative_body_terminal. fs_u_dst_lowertiersumnegative = fs_q_dst_lowertiersumnegative_body_terminal * S ((S ((l))) * fs_v_dst_lowertiersumnegative) + (dst_negative_sum_lowertiersum))) /\ forall fs_i_dst_lowertiersumnegative_body_steps. (exists fs_lt_dst_lowertiersumnegative_body_steps_bound. fs_lt_dst_lowertiersumnegative_body_steps_bound + S fs_i_dst_lowertiersumnegative_body_steps = (l)) -> exists fs_a_dst_lowertiersumnegative_body_steps fs_r_dst_lowertiersumnegative_body_steps fs_s_dst_lowertiersumnegative_body_steps. ((((exists fs_h_dst_lowertiersumnegative_body_steps_summand. fs_h_dst_lowertiersumnegative_body_steps_summand + S (fs_a_dst_lowertiersumnegative_body_steps) = S ((S (fs_i_dst_lowertiersumnegative_body_steps)) * dst_negative_scale_lowertiersum)) /\ exists fs_q_dst_lowertiersumnegative_body_steps_summand. dst_negative_code_lowertiersum = fs_q_dst_lowertiersumnegative_body_steps_summand * S ((S (fs_i_dst_lowertiersumnegative_body_steps)) * dst_negative_scale_lowertiersum) + (fs_a_dst_lowertiersumnegative_body_steps))) /\ ((((exists fs_h_dst_lowertiersumnegative_body_steps_partial. fs_h_dst_lowertiersumnegative_body_steps_partial + S (fs_r_dst_lowertiersumnegative_body_steps) = S ((S (fs_i_dst_lowertiersumnegative_body_steps)) * fs_v_dst_lowertiersumnegative)) /\ exists fs_q_dst_lowertiersumnegative_body_steps_partial. fs_u_dst_lowertiersumnegative = fs_q_dst_lowertiersumnegative_body_steps_partial * S ((S (fs_i_dst_lowertiersumnegative_body_steps)) * fs_v_dst_lowertiersumnegative) + (fs_r_dst_lowertiersumnegative_body_steps))) /\ ((((exists fs_h_dst_lowertiersumnegative_body_steps_successor. fs_h_dst_lowertiersumnegative_body_steps_successor + S (fs_s_dst_lowertiersumnegative_body_steps) = S ((S (S fs_i_dst_lowertiersumnegative_body_steps)) * fs_v_dst_lowertiersumnegative)) /\ exists fs_q_dst_lowertiersumnegative_body_steps_successor. fs_u_dst_lowertiersumnegative = fs_q_dst_lowertiersumnegative_body_steps_successor * S ((S (S fs_i_dst_lowertiersumnegative_body_steps)) * fs_v_dst_lowertiersumnegative) + (fs_s_dst_lowertiersumnegative_body_steps))) /\ fs_s_dst_lowertiersumnegative_body_steps = fs_r_dst_lowertiersumnegative_body_steps + fs_a_dst_lowertiersumnegative_body_steps)))))) /\ (exists ge_balance_positive_lowertiersumresult ge_balance_negative_lowertiersumresult. ((((((z)) = 2 * (ge_balance_positive_lowertiersumresult) /\ (ge_balance_negative_lowertiersumresult) = 0) \/ exists ge_signed_half_lowertiersumresultdecode. ((((z)) = 2 * ge_signed_half_lowertiersumresultdecode + 1 /\ (ge_balance_positive_lowertiersumresult) = 0) /\ (ge_balance_negative_lowertiersumresult) = S ge_signed_half_lowertiersumresultdecode))) /\ ((dst_positive_sum_lowertiersum) + ge_balance_negative_lowertiersumresult = (dst_negative_sum_lowertiersum) + ge_balance_positive_lowertiersumresult))))))))))

The unchanged native kernel never receives this surface symbol. Binder-safe expansion produces only its existing first-order syntax.