signed_table_weighted_add_distributive

Exact expanded first-order arithmetic statement

forall l W F G H P Q R. (((exists dst_positive_code_weighted_add_inputsleft_table dst_positive_scale_weighted_add_inputsleft_table dst_negative_code_weighted_add_inputsleft_table dst_negative_scale_weighted_add_inputsleft_table. (((F) = (((((dst_positive_code_weighted_add_inputsleft_table) + (dst_positive_scale_weighted_add_inputsleft_table)) * S ((dst_positive_code_weighted_add_inputsleft_table) + (dst_positive_scale_weighted_add_inputsleft_table)) + ((dst_positive_scale_weighted_add_inputsleft_table) + (dst_positive_scale_weighted_add_inputsleft_table))) + (((dst_negative_code_weighted_add_inputsleft_table) + (dst_negative_scale_weighted_add_inputsleft_table)) * S ((dst_negative_code_weighted_add_inputsleft_table) + (dst_negative_scale_weighted_add_inputsleft_table)) + ((dst_negative_scale_weighted_add_inputsleft_table) + (dst_negative_scale_weighted_add_inputsleft_table)))) * S ((((dst_positive_code_weighted_add_inputsleft_table) + (dst_positive_scale_weighted_add_inputsleft_table)) * S ((dst_positive_code_weighted_add_inputsleft_table) + (dst_positive_scale_weighted_add_inputsleft_table)) + ((dst_positive_scale_weighted_add_inputsleft_table) + (dst_positive_scale_weighted_add_inputsleft_table))) + (((dst_negative_code_weighted_add_inputsleft_table) + (dst_negative_scale_weighted_add_inputsleft_table)) * S ((dst_negative_code_weighted_add_inputsleft_table) + (dst_negative_scale_weighted_add_inputsleft_table)) + ((dst_negative_scale_weighted_add_inputsleft_table) + (dst_negative_scale_weighted_add_inputsleft_table)))) + ((((dst_negative_code_weighted_add_inputsleft_table) + (dst_negative_scale_weighted_add_inputsleft_table)) * S ((dst_negative_code_weighted_add_inputsleft_table) + (dst_negative_scale_weighted_add_inputsleft_table)) + ((dst_negative_scale_weighted_add_inputsleft_table) + (dst_negative_scale_weighted_add_inputsleft_table))) + (((dst_negative_code_weighted_add_inputsleft_table) + (dst_negative_scale_weighted_add_inputsleft_table)) * S ((dst_negative_code_weighted_add_inputsleft_table) + (dst_negative_scale_weighted_add_inputsleft_table)) + ((dst_negative_scale_weighted_add_inputsleft_table) + (dst_negative_scale_weighted_add_inputsleft_table)))))) /\ (forall dst_index_weighted_add_inputsleft_table. (exists pvs_le_gap_weighted_add_inputsleft_tabledomain. pvs_le_gap_weighted_add_inputsleft_tabledomain + (dst_index_weighted_add_inputsleft_table) = (l)) -> exists dst_positive_weighted_add_inputsleft_table dst_negative_weighted_add_inputsleft_table dst_value_weighted_add_inputsleft_table. ((((exists ff_h_pvs_weighted_add_inputsleft_tableentrypositive. ff_h_pvs_weighted_add_inputsleft_tableentrypositive + S (dst_positive_weighted_add_inputsleft_table) = S ((S (dst_index_weighted_add_inputsleft_table)) * dst_positive_scale_weighted_add_inputsleft_table)) /\ exists ff_q_pvs_weighted_add_inputsleft_tableentrypositive. dst_positive_code_weighted_add_inputsleft_table = ff_q_pvs_weighted_add_inputsleft_tableentrypositive * S ((S (dst_index_weighted_add_inputsleft_table)) * dst_positive_scale_weighted_add_inputsleft_table) + (dst_positive_weighted_add_inputsleft_table))) /\ (((((exists ff_h_pvs_weighted_add_inputsleft_tableentrynegative. ff_h_pvs_weighted_add_inputsleft_tableentrynegative + S (dst_negative_weighted_add_inputsleft_table) = S ((S (dst_index_weighted_add_inputsleft_table)) * dst_negative_scale_weighted_add_inputsleft_table)) /\ exists ff_q_pvs_weighted_add_inputsleft_tableentrynegative. dst_negative_code_weighted_add_inputsleft_table = ff_q_pvs_weighted_add_inputsleft_tableentrynegative * S ((S (dst_index_weighted_add_inputsleft_table)) * dst_negative_scale_weighted_add_inputsleft_table) + (dst_negative_weighted_add_inputsleft_table))) /\ (exists ge_balance_positive_weighted_add_inputsleft_tableentryvalue ge_balance_negative_weighted_add_inputsleft_tableentryvalue. (((((dst_value_weighted_add_inputsleft_table) = 2 * (ge_balance_positive_weighted_add_inputsleft_tableentryvalue) /\ (ge_balance_negative_weighted_add_inputsleft_tableentryvalue) = 0) \/ exists ge_signed_half_weighted_add_inputsleft_tableentryvaluedecode. (((dst_value_weighted_add_inputsleft_table) = 2 * ge_signed_half_weighted_add_inputsleft_tableentryvaluedecode + 1 /\ (ge_balance_positive_weighted_add_inputsleft_tableentryvalue) = 0) /\ (ge_balance_negative_weighted_add_inputsleft_tableentryvalue) = S ge_signed_half_weighted_add_inputsleft_tableentryvaluedecode))) /\ ((dst_positive_weighted_add_inputsleft_table) + ge_balance_negative_weighted_add_inputsleft_tableentryvalue = (dst_negative_weighted_add_inputsleft_table) + ge_balance_positive_weighted_add_inputsleft_tableentryvalue))))))))) /\ (((exists dst_positive_code_weighted_add_inputsright_table dst_positive_scale_weighted_add_inputsright_table dst_negative_code_weighted_add_inputsright_table dst_negative_scale_weighted_add_inputsright_table. (((G) = (((((dst_positive_code_weighted_add_inputsright_table) + (dst_positive_scale_weighted_add_inputsright_table)) * S ((dst_positive_code_weighted_add_inputsright_table) + (dst_positive_scale_weighted_add_inputsright_table)) + ((dst_positive_scale_weighted_add_inputsright_table) + (dst_positive_scale_weighted_add_inputsright_table))) + (((dst_negative_code_weighted_add_inputsright_table) + (dst_negative_scale_weighted_add_inputsright_table)) * S ((dst_negative_code_weighted_add_inputsright_table) + (dst_negative_scale_weighted_add_inputsright_table)) + ((dst_negative_scale_weighted_add_inputsright_table) + (dst_negative_scale_weighted_add_inputsright_table)))) * S ((((dst_positive_code_weighted_add_inputsright_table) + (dst_positive_scale_weighted_add_inputsright_table)) * S ((dst_positive_code_weighted_add_inputsright_table) + (dst_positive_scale_weighted_add_inputsright_table)) + ((dst_positive_scale_weighted_add_inputsright_table) + (dst_positive_scale_weighted_add_inputsright_table))) + (((dst_negative_code_weighted_add_inputsright_table) + (dst_negative_scale_weighted_add_inputsright_table)) * S ((dst_negative_code_weighted_add_inputsright_table) + (dst_negative_scale_weighted_add_inputsright_table)) + ((dst_negative_scale_weighted_add_inputsright_table) + (dst_negative_scale_weighted_add_inputsright_table)))) + ((((dst_negative_code_weighted_add_inputsright_table) + (dst_negative_scale_weighted_add_inputsright_table)) * S ((dst_negative_code_weighted_add_inputsright_table) + (dst_negative_scale_weighted_add_inputsright_table)) + ((dst_negative_scale_weighted_add_inputsright_table) + (dst_negative_scale_weighted_add_inputsright_table))) + (((dst_negative_code_weighted_add_inputsright_table) + (dst_negative_scale_weighted_add_inputsright_table)) * S ((dst_negative_code_weighted_add_inputsright_table) + (dst_negative_scale_weighted_add_inputsright_table)) + ((dst_negative_scale_weighted_add_inputsright_table) + (dst_negative_scale_weighted_add_inputsright_table)))))) /\ (forall dst_index_weighted_add_inputsright_table. (exists pvs_le_gap_weighted_add_inputsright_tabledomain. pvs_le_gap_weighted_add_inputsright_tabledomain + (dst_index_weighted_add_inputsright_table) = (l)) -> exists dst_positive_weighted_add_inputsright_table dst_negative_weighted_add_inputsright_table dst_value_weighted_add_inputsright_table. ((((exists ff_h_pvs_weighted_add_inputsright_tableentrypositive. ff_h_pvs_weighted_add_inputsright_tableentrypositive + S (dst_positive_weighted_add_inputsright_table) = S ((S (dst_index_weighted_add_inputsright_table)) * dst_positive_scale_weighted_add_inputsright_table)) /\ exists ff_q_pvs_weighted_add_inputsright_tableentrypositive. dst_positive_code_weighted_add_inputsright_table = ff_q_pvs_weighted_add_inputsright_tableentrypositive * S ((S (dst_index_weighted_add_inputsright_table)) * dst_positive_scale_weighted_add_inputsright_table) + (dst_positive_weighted_add_inputsright_table))) /\ (((((exists ff_h_pvs_weighted_add_inputsright_tableentrynegative. ff_h_pvs_weighted_add_inputsright_tableentrynegative + S (dst_negative_weighted_add_inputsright_table) = S ((S (dst_index_weighted_add_inputsright_table)) * dst_negative_scale_weighted_add_inputsright_table)) /\ exists ff_q_pvs_weighted_add_inputsright_tableentrynegative. dst_negative_code_weighted_add_inputsright_table = ff_q_pvs_weighted_add_inputsright_tableentrynegative * S ((S (dst_index_weighted_add_inputsright_table)) * dst_negative_scale_weighted_add_inputsright_table) + (dst_negative_weighted_add_inputsright_table))) /\ (exists ge_balance_positive_weighted_add_inputsright_tableentryvalue ge_balance_negative_weighted_add_inputsright_tableentryvalue. (((((dst_value_weighted_add_inputsright_table) = 2 * (ge_balance_positive_weighted_add_inputsright_tableentryvalue) /\ (ge_balance_negative_weighted_add_inputsright_tableentryvalue) = 0) \/ exists ge_signed_half_weighted_add_inputsright_tableentryvaluedecode. (((dst_value_weighted_add_inputsright_table) = 2 * ge_signed_half_weighted_add_inputsright_tableentryvaluedecode + 1 /\ (ge_balance_positive_weighted_add_inputsright_tableentryvalue) = 0) /\ (ge_balance_negative_weighted_add_inputsright_tableentryvalue) = S ge_signed_half_weighted_add_inputsright_tableentryvaluedecode))) /\ ((dst_positive_weighted_add_inputsright_table) + ge_balance_negative_weighted_add_inputsright_tableentryvalue = (dst_negative_weighted_add_inputsright_table) + ge_balance_positive_weighted_add_inputsright_tableentryvalue))))))))) /\ (((exists dst_positive_code_weighted_add_inputsoutput_table dst_positive_scale_weighted_add_inputsoutput_table dst_negative_code_weighted_add_inputsoutput_table dst_negative_scale_weighted_add_inputsoutput_table. (((H) = (((((dst_positive_code_weighted_add_inputsoutput_table) + (dst_positive_scale_weighted_add_inputsoutput_table)) * S ((dst_positive_code_weighted_add_inputsoutput_table) + (dst_positive_scale_weighted_add_inputsoutput_table)) + ((dst_positive_scale_weighted_add_inputsoutput_table) + (dst_positive_scale_weighted_add_inputsoutput_table))) + (((dst_negative_code_weighted_add_inputsoutput_table) + (dst_negative_scale_weighted_add_inputsoutput_table)) * S ((dst_negative_code_weighted_add_inputsoutput_table) + (dst_negative_scale_weighted_add_inputsoutput_table)) + ((dst_negative_scale_weighted_add_inputsoutput_table) + (dst_negative_scale_weighted_add_inputsoutput_table)))) * S ((((dst_positive_code_weighted_add_inputsoutput_table) + (dst_positive_scale_weighted_add_inputsoutput_table)) * S ((dst_positive_code_weighted_add_inputsoutput_table) + (dst_positive_scale_weighted_add_inputsoutput_table)) + ((dst_positive_scale_weighted_add_inputsoutput_table) + (dst_positive_scale_weighted_add_inputsoutput_table))) + (((dst_negative_code_weighted_add_inputsoutput_table) + (dst_negative_scale_weighted_add_inputsoutput_table)) * S ((dst_negative_code_weighted_add_inputsoutput_table) + (dst_negative_scale_weighted_add_inputsoutput_table)) + ((dst_negative_scale_weighted_add_inputsoutput_table) + (dst_negative_scale_weighted_add_inputsoutput_table)))) + ((((dst_negative_code_weighted_add_inputsoutput_table) + (dst_negative_scale_weighted_add_inputsoutput_table)) * S ((dst_negative_code_weighted_add_inputsoutput_table) + (dst_negative_scale_weighted_add_inputsoutput_table)) + ((dst_negative_scale_weighted_add_inputsoutput_table) + (dst_negative_scale_weighted_add_inputsoutput_table))) + (((dst_negative_code_weighted_add_inputsoutput_table) + (dst_negative_scale_weighted_add_inputsoutput_table)) * S ((dst_negative_code_weighted_add_inputsoutput_table) + (dst_negative_scale_weighted_add_inputsoutput_table)) + ((dst_negative_scale_weighted_add_inputsoutput_table) + (dst_negative_scale_weighted_add_inputsoutput_table)))))) /\ (forall dst_index_weighted_add_inputsoutput_table. (exists pvs_le_gap_weighted_add_inputsoutput_tabledomain. pvs_le_gap_weighted_add_inputsoutput_tabledomain + (dst_index_weighted_add_inputsoutput_table) = (l)) -> exists dst_positive_weighted_add_inputsoutput_table dst_negative_weighted_add_inputsoutput_table dst_value_weighted_add_inputsoutput_table. ((((exists ff_h_pvs_weighted_add_inputsoutput_tableentrypositive. ff_h_pvs_weighted_add_inputsoutput_tableentrypositive + S (dst_positive_weighted_add_inputsoutput_table) = S ((S (dst_index_weighted_add_inputsoutput_table)) * dst_positive_scale_weighted_add_inputsoutput_table)) /\ exists ff_q_pvs_weighted_add_inputsoutput_tableentrypositive. dst_positive_code_weighted_add_inputsoutput_table = ff_q_pvs_weighted_add_inputsoutput_tableentrypositive * S ((S (dst_index_weighted_add_inputsoutput_table)) * dst_positive_scale_weighted_add_inputsoutput_table) + (dst_positive_weighted_add_inputsoutput_table))) /\ (((((exists ff_h_pvs_weighted_add_inputsoutput_tableentrynegative. ff_h_pvs_weighted_add_inputsoutput_tableentrynegative + S (dst_negative_weighted_add_inputsoutput_table) = S ((S (dst_index_weighted_add_inputsoutput_table)) * dst_negative_scale_weighted_add_inputsoutput_table)) /\ exists ff_q_pvs_weighted_add_inputsoutput_tableentrynegative. dst_negative_code_weighted_add_inputsoutput_table = ff_q_pvs_weighted_add_inputsoutput_tableentrynegative * S ((S (dst_index_weighted_add_inputsoutput_table)) * dst_negative_scale_weighted_add_inputsoutput_table) + (dst_negative_weighted_add_inputsoutput_table))) /\ (exists ge_balance_positive_weighted_add_inputsoutput_tableentryvalue ge_balance_negative_weighted_add_inputsoutput_tableentryvalue. (((((dst_value_weighted_add_inputsoutput_table) = 2 * (ge_balance_positive_weighted_add_inputsoutput_tableentryvalue) /\ (ge_balance_negative_weighted_add_inputsoutput_tableentryvalue) = 0) \/ exists ge_signed_half_weighted_add_inputsoutput_tableentryvaluedecode. (((dst_value_weighted_add_inputsoutput_table) = 2 * ge_signed_half_weighted_add_inputsoutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_weighted_add_inputsoutput_tableentryvalue) = 0) /\ (ge_balance_negative_weighted_add_inputsoutput_tableentryvalue) = S ge_signed_half_weighted_add_inputsoutput_tableentryvaluedecode))) /\ ((dst_positive_weighted_add_inputsoutput_table) + ge_balance_negative_weighted_add_inputsoutput_tableentryvalue = (dst_negative_weighted_add_inputsoutput_table) + ge_balance_positive_weighted_add_inputsoutput_tableentryvalue))))))))) /\ (forall sto_index_weighted_add_inputsentries. (exists pvs_gap_weighted_add_inputsentriesbound. pvs_gap_weighted_add_inputsentriesbound + S (sto_index_weighted_add_inputsentries) = (l)) -> exists sto_left_weighted_add_inputsentries sto_right_weighted_add_inputsentries sto_output_weighted_add_inputsentries. ((exists dst_positive_code_weighted_add_inputsentriesentryleft dst_positive_scale_weighted_add_inputsentriesentryleft dst_negative_code_weighted_add_inputsentriesentryleft dst_negative_scale_weighted_add_inputsentriesentryleft dst_positive_weighted_add_inputsentriesentryleft dst_negative_weighted_add_inputsentriesentryleft. (((F) = (((((dst_positive_code_weighted_add_inputsentriesentryleft) + (dst_positive_scale_weighted_add_inputsentriesentryleft)) * S ((dst_positive_code_weighted_add_inputsentriesentryleft) + (dst_positive_scale_weighted_add_inputsentriesentryleft)) + ((dst_positive_scale_weighted_add_inputsentriesentryleft) + (dst_positive_scale_weighted_add_inputsentriesentryleft))) + (((dst_negative_code_weighted_add_inputsentriesentryleft) + (dst_negative_scale_weighted_add_inputsentriesentryleft)) * S ((dst_negative_code_weighted_add_inputsentriesentryleft) + (dst_negative_scale_weighted_add_inputsentriesentryleft)) + ((dst_negative_scale_weighted_add_inputsentriesentryleft) + (dst_negative_scale_weighted_add_inputsentriesentryleft)))) * S ((((dst_positive_code_weighted_add_inputsentriesentryleft) + (dst_positive_scale_weighted_add_inputsentriesentryleft)) * S ((dst_positive_code_weighted_add_inputsentriesentryleft) + (dst_positive_scale_weighted_add_inputsentriesentryleft)) + ((dst_positive_scale_weighted_add_inputsentriesentryleft) + (dst_positive_scale_weighted_add_inputsentriesentryleft))) + (((dst_negative_code_weighted_add_inputsentriesentryleft) + (dst_negative_scale_weighted_add_inputsentriesentryleft)) * S ((dst_negative_code_weighted_add_inputsentriesentryleft) + (dst_negative_scale_weighted_add_inputsentriesentryleft)) + ((dst_negative_scale_weighted_add_inputsentriesentryleft) + (dst_negative_scale_weighted_add_inputsentriesentryleft)))) + ((((dst_negative_code_weighted_add_inputsentriesentryleft) + (dst_negative_scale_weighted_add_inputsentriesentryleft)) * S ((dst_negative_code_weighted_add_inputsentriesentryleft) + (dst_negative_scale_weighted_add_inputsentriesentryleft)) + ((dst_negative_scale_weighted_add_inputsentriesentryleft) + (dst_negative_scale_weighted_add_inputsentriesentryleft))) + (((dst_negative_code_weighted_add_inputsentriesentryleft) + (dst_negative_scale_weighted_add_inputsentriesentryleft)) * S ((dst_negative_code_weighted_add_inputsentriesentryleft) + (dst_negative_scale_weighted_add_inputsentriesentryleft)) + ((dst_negative_scale_weighted_add_inputsentriesentryleft) + (dst_negative_scale_weighted_add_inputsentriesentryleft)))))) /\ (((((exists ff_h_pvs_weighted_add_inputsentriesentryleftpositive. ff_h_pvs_weighted_add_inputsentriesentryleftpositive + S (dst_positive_weighted_add_inputsentriesentryleft) = S ((S (sto_index_weighted_add_inputsentries)) * dst_positive_scale_weighted_add_inputsentriesentryleft)) /\ exists ff_q_pvs_weighted_add_inputsentriesentryleftpositive. dst_positive_code_weighted_add_inputsentriesentryleft = ff_q_pvs_weighted_add_inputsentriesentryleftpositive * S ((S (sto_index_weighted_add_inputsentries)) * dst_positive_scale_weighted_add_inputsentriesentryleft) + (dst_positive_weighted_add_inputsentriesentryleft))) /\ (((((exists ff_h_pvs_weighted_add_inputsentriesentryleftnegative. ff_h_pvs_weighted_add_inputsentriesentryleftnegative + S (dst_negative_weighted_add_inputsentriesentryleft) = S ((S (sto_index_weighted_add_inputsentries)) * dst_negative_scale_weighted_add_inputsentriesentryleft)) /\ exists ff_q_pvs_weighted_add_inputsentriesentryleftnegative. dst_negative_code_weighted_add_inputsentriesentryleft = ff_q_pvs_weighted_add_inputsentriesentryleftnegative * S ((S (sto_index_weighted_add_inputsentries)) * dst_negative_scale_weighted_add_inputsentriesentryleft) + (dst_negative_weighted_add_inputsentriesentryleft))) /\ (exists ge_balance_positive_weighted_add_inputsentriesentryleftvalue ge_balance_negative_weighted_add_inputsentriesentryleftvalue. (((((sto_left_weighted_add_inputsentries) = 2 * (ge_balance_positive_weighted_add_inputsentriesentryleftvalue) /\ (ge_balance_negative_weighted_add_inputsentriesentryleftvalue) = 0) \/ exists ge_signed_half_weighted_add_inputsentriesentryleftvaluedecode. (((sto_left_weighted_add_inputsentries) = 2 * ge_signed_half_weighted_add_inputsentriesentryleftvaluedecode + 1 /\ (ge_balance_positive_weighted_add_inputsentriesentryleftvalue) = 0) /\ (ge_balance_negative_weighted_add_inputsentriesentryleftvalue) = S ge_signed_half_weighted_add_inputsentriesentryleftvaluedecode))) /\ ((dst_positive_weighted_add_inputsentriesentryleft) + ge_balance_negative_weighted_add_inputsentriesentryleftvalue = (dst_negative_weighted_add_inputsentriesentryleft) + ge_balance_positive_weighted_add_inputsentriesentryleftvalue))))))))) /\ (((exists dst_positive_code_weighted_add_inputsentriesentryright dst_positive_scale_weighted_add_inputsentriesentryright dst_negative_code_weighted_add_inputsentriesentryright dst_negative_scale_weighted_add_inputsentriesentryright dst_positive_weighted_add_inputsentriesentryright dst_negative_weighted_add_inputsentriesentryright. (((G) = (((((dst_positive_code_weighted_add_inputsentriesentryright) + (dst_positive_scale_weighted_add_inputsentriesentryright)) * S ((dst_positive_code_weighted_add_inputsentriesentryright) + (dst_positive_scale_weighted_add_inputsentriesentryright)) + ((dst_positive_scale_weighted_add_inputsentriesentryright) + (dst_positive_scale_weighted_add_inputsentriesentryright))) + (((dst_negative_code_weighted_add_inputsentriesentryright) + (dst_negative_scale_weighted_add_inputsentriesentryright)) * S ((dst_negative_code_weighted_add_inputsentriesentryright) + (dst_negative_scale_weighted_add_inputsentriesentryright)) + ((dst_negative_scale_weighted_add_inputsentriesentryright) + (dst_negative_scale_weighted_add_inputsentriesentryright)))) * S ((((dst_positive_code_weighted_add_inputsentriesentryright) + (dst_positive_scale_weighted_add_inputsentriesentryright)) * S ((dst_positive_code_weighted_add_inputsentriesentryright) + (dst_positive_scale_weighted_add_inputsentriesentryright)) + ((dst_positive_scale_weighted_add_inputsentriesentryright) + (dst_positive_scale_weighted_add_inputsentriesentryright))) + (((dst_negative_code_weighted_add_inputsentriesentryright) + (dst_negative_scale_weighted_add_inputsentriesentryright)) * S ((dst_negative_code_weighted_add_inputsentriesentryright) + (dst_negative_scale_weighted_add_inputsentriesentryright)) + ((dst_negative_scale_weighted_add_inputsentriesentryright) + (dst_negative_scale_weighted_add_inputsentriesentryright)))) + ((((dst_negative_code_weighted_add_inputsentriesentryright) + (dst_negative_scale_weighted_add_inputsentriesentryright)) * S ((dst_negative_code_weighted_add_inputsentriesentryright) + (dst_negative_scale_weighted_add_inputsentriesentryright)) + ((dst_negative_scale_weighted_add_inputsentriesentryright) + (dst_negative_scale_weighted_add_inputsentriesentryright))) + (((dst_negative_code_weighted_add_inputsentriesentryright) + (dst_negative_scale_weighted_add_inputsentriesentryright)) * S ((dst_negative_code_weighted_add_inputsentriesentryright) + (dst_negative_scale_weighted_add_inputsentriesentryright)) + ((dst_negative_scale_weighted_add_inputsentriesentryright) + (dst_negative_scale_weighted_add_inputsentriesentryright)))))) /\ (((((exists ff_h_pvs_weighted_add_inputsentriesentryrightpositive. ff_h_pvs_weighted_add_inputsentriesentryrightpositive + S (dst_positive_weighted_add_inputsentriesentryright) = S ((S (sto_index_weighted_add_inputsentries)) * dst_positive_scale_weighted_add_inputsentriesentryright)) /\ exists ff_q_pvs_weighted_add_inputsentriesentryrightpositive. dst_positive_code_weighted_add_inputsentriesentryright = ff_q_pvs_weighted_add_inputsentriesentryrightpositive * S ((S (sto_index_weighted_add_inputsentries)) * dst_positive_scale_weighted_add_inputsentriesentryright) + (dst_positive_weighted_add_inputsentriesentryright))) /\ (((((exists ff_h_pvs_weighted_add_inputsentriesentryrightnegative. ff_h_pvs_weighted_add_inputsentriesentryrightnegative + S (dst_negative_weighted_add_inputsentriesentryright) = S ((S (sto_index_weighted_add_inputsentries)) * dst_negative_scale_weighted_add_inputsentriesentryright)) /\ exists ff_q_pvs_weighted_add_inputsentriesentryrightnegative. dst_negative_code_weighted_add_inputsentriesentryright = ff_q_pvs_weighted_add_inputsentriesentryrightnegative * S ((S (sto_index_weighted_add_inputsentries)) * dst_negative_scale_weighted_add_inputsentriesentryright) + (dst_negative_weighted_add_inputsentriesentryright))) /\ (exists ge_balance_positive_weighted_add_inputsentriesentryrightvalue ge_balance_negative_weighted_add_inputsentriesentryrightvalue. (((((sto_right_weighted_add_inputsentries) = 2 * (ge_balance_positive_weighted_add_inputsentriesentryrightvalue) /\ (ge_balance_negative_weighted_add_inputsentriesentryrightvalue) = 0) \/ exists ge_signed_half_weighted_add_inputsentriesentryrightvaluedecode. (((sto_right_weighted_add_inputsentries) = 2 * ge_signed_half_weighted_add_inputsentriesentryrightvaluedecode + 1 /\ (ge_balance_positive_weighted_add_inputsentriesentryrightvalue) = 0) /\ (ge_balance_negative_weighted_add_inputsentriesentryrightvalue) = S ge_signed_half_weighted_add_inputsentriesentryrightvaluedecode))) /\ ((dst_positive_weighted_add_inputsentriesentryright) + ge_balance_negative_weighted_add_inputsentriesentryrightvalue = (dst_negative_weighted_add_inputsentriesentryright) + ge_balance_positive_weighted_add_inputsentriesentryrightvalue))))))))) /\ (((exists dst_positive_code_weighted_add_inputsentriesentryoutput dst_positive_scale_weighted_add_inputsentriesentryoutput dst_negative_code_weighted_add_inputsentriesentryoutput dst_negative_scale_weighted_add_inputsentriesentryoutput dst_positive_weighted_add_inputsentriesentryoutput dst_negative_weighted_add_inputsentriesentryoutput. (((H) = (((((dst_positive_code_weighted_add_inputsentriesentryoutput) + (dst_positive_scale_weighted_add_inputsentriesentryoutput)) * S ((dst_positive_code_weighted_add_inputsentriesentryoutput) + (dst_positive_scale_weighted_add_inputsentriesentryoutput)) + ((dst_positive_scale_weighted_add_inputsentriesentryoutput) + (dst_positive_scale_weighted_add_inputsentriesentryoutput))) + (((dst_negative_code_weighted_add_inputsentriesentryoutput) + (dst_negative_scale_weighted_add_inputsentriesentryoutput)) * S ((dst_negative_code_weighted_add_inputsentriesentryoutput) + (dst_negative_scale_weighted_add_inputsentriesentryoutput)) + ((dst_negative_scale_weighted_add_inputsentriesentryoutput) + (dst_negative_scale_weighted_add_inputsentriesentryoutput)))) * S ((((dst_positive_code_weighted_add_inputsentriesentryoutput) + (dst_positive_scale_weighted_add_inputsentriesentryoutput)) * S ((dst_positive_code_weighted_add_inputsentriesentryoutput) + (dst_positive_scale_weighted_add_inputsentriesentryoutput)) + ((dst_positive_scale_weighted_add_inputsentriesentryoutput) + (dst_positive_scale_weighted_add_inputsentriesentryoutput))) + (((dst_negative_code_weighted_add_inputsentriesentryoutput) + (dst_negative_scale_weighted_add_inputsentriesentryoutput)) * S ((dst_negative_code_weighted_add_inputsentriesentryoutput) + (dst_negative_scale_weighted_add_inputsentriesentryoutput)) + ((dst_negative_scale_weighted_add_inputsentriesentryoutput) + (dst_negative_scale_weighted_add_inputsentriesentryoutput)))) + ((((dst_negative_code_weighted_add_inputsentriesentryoutput) + (dst_negative_scale_weighted_add_inputsentriesentryoutput)) * S ((dst_negative_code_weighted_add_inputsentriesentryoutput) + (dst_negative_scale_weighted_add_inputsentriesentryoutput)) + ((dst_negative_scale_weighted_add_inputsentriesentryoutput) + (dst_negative_scale_weighted_add_inputsentriesentryoutput))) + (((dst_negative_code_weighted_add_inputsentriesentryoutput) + (dst_negative_scale_weighted_add_inputsentriesentryoutput)) * S ((dst_negative_code_weighted_add_inputsentriesentryoutput) + (dst_negative_scale_weighted_add_inputsentriesentryoutput)) + ((dst_negative_scale_weighted_add_inputsentriesentryoutput) + (dst_negative_scale_weighted_add_inputsentriesentryoutput)))))) /\ (((((exists ff_h_pvs_weighted_add_inputsentriesentryoutputpositive. ff_h_pvs_weighted_add_inputsentriesentryoutputpositive + S (dst_positive_weighted_add_inputsentriesentryoutput) = S ((S (sto_index_weighted_add_inputsentries)) * dst_positive_scale_weighted_add_inputsentriesentryoutput)) /\ exists ff_q_pvs_weighted_add_inputsentriesentryoutputpositive. dst_positive_code_weighted_add_inputsentriesentryoutput = ff_q_pvs_weighted_add_inputsentriesentryoutputpositive * S ((S (sto_index_weighted_add_inputsentries)) * dst_positive_scale_weighted_add_inputsentriesentryoutput) + (dst_positive_weighted_add_inputsentriesentryoutput))) /\ (((((exists ff_h_pvs_weighted_add_inputsentriesentryoutputnegative. ff_h_pvs_weighted_add_inputsentriesentryoutputnegative + S (dst_negative_weighted_add_inputsentriesentryoutput) = S ((S (sto_index_weighted_add_inputsentries)) * dst_negative_scale_weighted_add_inputsentriesentryoutput)) /\ exists ff_q_pvs_weighted_add_inputsentriesentryoutputnegative. dst_negative_code_weighted_add_inputsentriesentryoutput = ff_q_pvs_weighted_add_inputsentriesentryoutputnegative * S ((S (sto_index_weighted_add_inputsentries)) * dst_negative_scale_weighted_add_inputsentriesentryoutput) + (dst_negative_weighted_add_inputsentriesentryoutput))) /\ (exists ge_balance_positive_weighted_add_inputsentriesentryoutputvalue ge_balance_negative_weighted_add_inputsentriesentryoutputvalue. (((((sto_output_weighted_add_inputsentries) = 2 * (ge_balance_positive_weighted_add_inputsentriesentryoutputvalue) /\ (ge_balance_negative_weighted_add_inputsentriesentryoutputvalue) = 0) \/ exists ge_signed_half_weighted_add_inputsentriesentryoutputvaluedecode. (((sto_output_weighted_add_inputsentries) = 2 * ge_signed_half_weighted_add_inputsentriesentryoutputvaluedecode + 1 /\ (ge_balance_positive_weighted_add_inputsentriesentryoutputvalue) = 0) /\ (ge_balance_negative_weighted_add_inputsentriesentryoutputvalue) = S ge_signed_half_weighted_add_inputsentriesentryoutputvaluedecode))) /\ ((dst_positive_weighted_add_inputsentriesentryoutput) + ge_balance_negative_weighted_add_inputsentriesentryoutputvalue = (dst_negative_weighted_add_inputsentriesentryoutput) + ge_balance_positive_weighted_add_inputsentriesentryoutputvalue))))))))) /\ (exists dsa_ap_weighted_add_inputsentriesentryoperation dsa_an_weighted_add_inputsentriesentryoperation dsa_bp_weighted_add_inputsentriesentryoperation dsa_bn_weighted_add_inputsentriesentryoperation dsa_cp_weighted_add_inputsentriesentryoperation dsa_cn_weighted_add_inputsentriesentryoperation. (((((sto_left_weighted_add_inputsentries) = 2 * (dsa_ap_weighted_add_inputsentriesentryoperation) /\ (dsa_an_weighted_add_inputsentriesentryoperation) = 0) \/ exists ge_signed_half_weighted_add_inputsentriesentryoperationleft. (((sto_left_weighted_add_inputsentries) = 2 * ge_signed_half_weighted_add_inputsentriesentryoperationleft + 1 /\ (dsa_ap_weighted_add_inputsentriesentryoperation) = 0) /\ (dsa_an_weighted_add_inputsentriesentryoperation) = S ge_signed_half_weighted_add_inputsentriesentryoperationleft))) /\ ((((((sto_right_weighted_add_inputsentries) = 2 * (dsa_bp_weighted_add_inputsentriesentryoperation) /\ (dsa_bn_weighted_add_inputsentriesentryoperation) = 0) \/ exists ge_signed_half_weighted_add_inputsentriesentryoperationright. (((sto_right_weighted_add_inputsentries) = 2 * ge_signed_half_weighted_add_inputsentriesentryoperationright + 1 /\ (dsa_bp_weighted_add_inputsentriesentryoperation) = 0) /\ (dsa_bn_weighted_add_inputsentriesentryoperation) = S ge_signed_half_weighted_add_inputsentriesentryoperationright))) /\ ((((((sto_output_weighted_add_inputsentries) = 2 * (dsa_cp_weighted_add_inputsentriesentryoperation) /\ (dsa_cn_weighted_add_inputsentriesentryoperation) = 0) \/ exists ge_signed_half_weighted_add_inputsentriesentryoperationoutput. (((sto_output_weighted_add_inputsentries) = 2 * ge_signed_half_weighted_add_inputsentriesentryoperationoutput + 1 /\ (dsa_cp_weighted_add_inputsentriesentryoperation) = 0) /\ (dsa_cn_weighted_add_inputsentriesentryoperation) = S ge_signed_half_weighted_add_inputsentriesentryoperationoutput))) /\ ((dsa_ap_weighted_add_inputsentriesentryoperation + dsa_bp_weighted_add_inputsentriesentryoperation) + dsa_cn_weighted_add_inputsentriesentryoperation = (dsa_an_weighted_add_inputsentriesentryoperation + dsa_bn_weighted_add_inputsentriesentryoperation) + dsa_cp_weighted_add_inputsentriesentryoperation))))))))))))))))))) -> (((exists dst_positive_code_weighted_add_firstleft_table dst_positive_scale_weighted_add_firstleft_table dst_negative_code_weighted_add_firstleft_table dst_negative_scale_weighted_add_firstleft_table. (((W) = (((((dst_positive_code_weighted_add_firstleft_table) + (dst_positive_scale_weighted_add_firstleft_table)) * S ((dst_positive_code_weighted_add_firstleft_table) + (dst_positive_scale_weighted_add_firstleft_table)) + ((dst_positive_scale_weighted_add_firstleft_table) + (dst_positive_scale_weighted_add_firstleft_table))) + (((dst_negative_code_weighted_add_firstleft_table) + (dst_negative_scale_weighted_add_firstleft_table)) * S ((dst_negative_code_weighted_add_firstleft_table) + (dst_negative_scale_weighted_add_firstleft_table)) + ((dst_negative_scale_weighted_add_firstleft_table) + (dst_negative_scale_weighted_add_firstleft_table)))) * S ((((dst_positive_code_weighted_add_firstleft_table) + (dst_positive_scale_weighted_add_firstleft_table)) * S ((dst_positive_code_weighted_add_firstleft_table) + (dst_positive_scale_weighted_add_firstleft_table)) + ((dst_positive_scale_weighted_add_firstleft_table) + (dst_positive_scale_weighted_add_firstleft_table))) + (((dst_negative_code_weighted_add_firstleft_table) + (dst_negative_scale_weighted_add_firstleft_table)) * S ((dst_negative_code_weighted_add_firstleft_table) + (dst_negative_scale_weighted_add_firstleft_table)) + ((dst_negative_scale_weighted_add_firstleft_table) + (dst_negative_scale_weighted_add_firstleft_table)))) + ((((dst_negative_code_weighted_add_firstleft_table) + (dst_negative_scale_weighted_add_firstleft_table)) * S ((dst_negative_code_weighted_add_firstleft_table) + (dst_negative_scale_weighted_add_firstleft_table)) + ((dst_negative_scale_weighted_add_firstleft_table) + (dst_negative_scale_weighted_add_firstleft_table))) + (((dst_negative_code_weighted_add_firstleft_table) + (dst_negative_scale_weighted_add_firstleft_table)) * S ((dst_negative_code_weighted_add_firstleft_table) + (dst_negative_scale_weighted_add_firstleft_table)) + ((dst_negative_scale_weighted_add_firstleft_table) + (dst_negative_scale_weighted_add_firstleft_table)))))) /\ (forall dst_index_weighted_add_firstleft_table. (exists pvs_le_gap_weighted_add_firstleft_tabledomain. pvs_le_gap_weighted_add_firstleft_tabledomain + (dst_index_weighted_add_firstleft_table) = (l)) -> exists dst_positive_weighted_add_firstleft_table dst_negative_weighted_add_firstleft_table dst_value_weighted_add_firstleft_table. ((((exists ff_h_pvs_weighted_add_firstleft_tableentrypositive. ff_h_pvs_weighted_add_firstleft_tableentrypositive + S (dst_positive_weighted_add_firstleft_table) = S ((S (dst_index_weighted_add_firstleft_table)) * dst_positive_scale_weighted_add_firstleft_table)) /\ exists ff_q_pvs_weighted_add_firstleft_tableentrypositive. dst_positive_code_weighted_add_firstleft_table = ff_q_pvs_weighted_add_firstleft_tableentrypositive * S ((S (dst_index_weighted_add_firstleft_table)) * dst_positive_scale_weighted_add_firstleft_table) + (dst_positive_weighted_add_firstleft_table))) /\ (((((exists ff_h_pvs_weighted_add_firstleft_tableentrynegative. ff_h_pvs_weighted_add_firstleft_tableentrynegative + S (dst_negative_weighted_add_firstleft_table) = S ((S (dst_index_weighted_add_firstleft_table)) * dst_negative_scale_weighted_add_firstleft_table)) /\ exists ff_q_pvs_weighted_add_firstleft_tableentrynegative. dst_negative_code_weighted_add_firstleft_table = ff_q_pvs_weighted_add_firstleft_tableentrynegative * S ((S (dst_index_weighted_add_firstleft_table)) * dst_negative_scale_weighted_add_firstleft_table) + (dst_negative_weighted_add_firstleft_table))) /\ (exists ge_balance_positive_weighted_add_firstleft_tableentryvalue ge_balance_negative_weighted_add_firstleft_tableentryvalue. (((((dst_value_weighted_add_firstleft_table) = 2 * (ge_balance_positive_weighted_add_firstleft_tableentryvalue) /\ (ge_balance_negative_weighted_add_firstleft_tableentryvalue) = 0) \/ exists ge_signed_half_weighted_add_firstleft_tableentryvaluedecode. (((dst_value_weighted_add_firstleft_table) = 2 * ge_signed_half_weighted_add_firstleft_tableentryvaluedecode + 1 /\ (ge_balance_positive_weighted_add_firstleft_tableentryvalue) = 0) /\ (ge_balance_negative_weighted_add_firstleft_tableentryvalue) = S ge_signed_half_weighted_add_firstleft_tableentryvaluedecode))) /\ ((dst_positive_weighted_add_firstleft_table) + ge_balance_negative_weighted_add_firstleft_tableentryvalue = (dst_negative_weighted_add_firstleft_table) + ge_balance_positive_weighted_add_firstleft_tableentryvalue))))))))) /\ (((exists dst_positive_code_weighted_add_firstright_table dst_positive_scale_weighted_add_firstright_table dst_negative_code_weighted_add_firstright_table dst_negative_scale_weighted_add_firstright_table. (((F) = (((((dst_positive_code_weighted_add_firstright_table) + (dst_positive_scale_weighted_add_firstright_table)) * S ((dst_positive_code_weighted_add_firstright_table) + (dst_positive_scale_weighted_add_firstright_table)) + ((dst_positive_scale_weighted_add_firstright_table) + (dst_positive_scale_weighted_add_firstright_table))) + (((dst_negative_code_weighted_add_firstright_table) + (dst_negative_scale_weighted_add_firstright_table)) * S ((dst_negative_code_weighted_add_firstright_table) + (dst_negative_scale_weighted_add_firstright_table)) + ((dst_negative_scale_weighted_add_firstright_table) + (dst_negative_scale_weighted_add_firstright_table)))) * S ((((dst_positive_code_weighted_add_firstright_table) + (dst_positive_scale_weighted_add_firstright_table)) * S ((dst_positive_code_weighted_add_firstright_table) + (dst_positive_scale_weighted_add_firstright_table)) + ((dst_positive_scale_weighted_add_firstright_table) + (dst_positive_scale_weighted_add_firstright_table))) + (((dst_negative_code_weighted_add_firstright_table) + (dst_negative_scale_weighted_add_firstright_table)) * S ((dst_negative_code_weighted_add_firstright_table) + (dst_negative_scale_weighted_add_firstright_table)) + ((dst_negative_scale_weighted_add_firstright_table) + (dst_negative_scale_weighted_add_firstright_table)))) + ((((dst_negative_code_weighted_add_firstright_table) + (dst_negative_scale_weighted_add_firstright_table)) * S ((dst_negative_code_weighted_add_firstright_table) + (dst_negative_scale_weighted_add_firstright_table)) + ((dst_negative_scale_weighted_add_firstright_table) + (dst_negative_scale_weighted_add_firstright_table))) + (((dst_negative_code_weighted_add_firstright_table) + (dst_negative_scale_weighted_add_firstright_table)) * S ((dst_negative_code_weighted_add_firstright_table) + (dst_negative_scale_weighted_add_firstright_table)) + ((dst_negative_scale_weighted_add_firstright_table) + (dst_negative_scale_weighted_add_firstright_table)))))) /\ (forall dst_index_weighted_add_firstright_table. (exists pvs_le_gap_weighted_add_firstright_tabledomain. pvs_le_gap_weighted_add_firstright_tabledomain + (dst_index_weighted_add_firstright_table) = (l)) -> exists dst_positive_weighted_add_firstright_table dst_negative_weighted_add_firstright_table dst_value_weighted_add_firstright_table. ((((exists ff_h_pvs_weighted_add_firstright_tableentrypositive. ff_h_pvs_weighted_add_firstright_tableentrypositive + S (dst_positive_weighted_add_firstright_table) = S ((S (dst_index_weighted_add_firstright_table)) * dst_positive_scale_weighted_add_firstright_table)) /\ exists ff_q_pvs_weighted_add_firstright_tableentrypositive. dst_positive_code_weighted_add_firstright_table = ff_q_pvs_weighted_add_firstright_tableentrypositive * S ((S (dst_index_weighted_add_firstright_table)) * dst_positive_scale_weighted_add_firstright_table) + (dst_positive_weighted_add_firstright_table))) /\ (((((exists ff_h_pvs_weighted_add_firstright_tableentrynegative. ff_h_pvs_weighted_add_firstright_tableentrynegative + S (dst_negative_weighted_add_firstright_table) = S ((S (dst_index_weighted_add_firstright_table)) * dst_negative_scale_weighted_add_firstright_table)) /\ exists ff_q_pvs_weighted_add_firstright_tableentrynegative. dst_negative_code_weighted_add_firstright_table = ff_q_pvs_weighted_add_firstright_tableentrynegative * S ((S (dst_index_weighted_add_firstright_table)) * dst_negative_scale_weighted_add_firstright_table) + (dst_negative_weighted_add_firstright_table))) /\ (exists ge_balance_positive_weighted_add_firstright_tableentryvalue ge_balance_negative_weighted_add_firstright_tableentryvalue. (((((dst_value_weighted_add_firstright_table) = 2 * (ge_balance_positive_weighted_add_firstright_tableentryvalue) /\ (ge_balance_negative_weighted_add_firstright_tableentryvalue) = 0) \/ exists ge_signed_half_weighted_add_firstright_tableentryvaluedecode. (((dst_value_weighted_add_firstright_table) = 2 * ge_signed_half_weighted_add_firstright_tableentryvaluedecode + 1 /\ (ge_balance_positive_weighted_add_firstright_tableentryvalue) = 0) /\ (ge_balance_negative_weighted_add_firstright_tableentryvalue) = S ge_signed_half_weighted_add_firstright_tableentryvaluedecode))) /\ ((dst_positive_weighted_add_firstright_table) + ge_balance_negative_weighted_add_firstright_tableentryvalue = (dst_negative_weighted_add_firstright_table) + ge_balance_positive_weighted_add_firstright_tableentryvalue))))))))) /\ (((exists dst_positive_code_weighted_add_firstoutput_table dst_positive_scale_weighted_add_firstoutput_table dst_negative_code_weighted_add_firstoutput_table dst_negative_scale_weighted_add_firstoutput_table. (((P) = (((((dst_positive_code_weighted_add_firstoutput_table) + (dst_positive_scale_weighted_add_firstoutput_table)) * S ((dst_positive_code_weighted_add_firstoutput_table) + (dst_positive_scale_weighted_add_firstoutput_table)) + ((dst_positive_scale_weighted_add_firstoutput_table) + (dst_positive_scale_weighted_add_firstoutput_table))) + (((dst_negative_code_weighted_add_firstoutput_table) + (dst_negative_scale_weighted_add_firstoutput_table)) * S ((dst_negative_code_weighted_add_firstoutput_table) + (dst_negative_scale_weighted_add_firstoutput_table)) + ((dst_negative_scale_weighted_add_firstoutput_table) + (dst_negative_scale_weighted_add_firstoutput_table)))) * S ((((dst_positive_code_weighted_add_firstoutput_table) + (dst_positive_scale_weighted_add_firstoutput_table)) * S ((dst_positive_code_weighted_add_firstoutput_table) + (dst_positive_scale_weighted_add_firstoutput_table)) + ((dst_positive_scale_weighted_add_firstoutput_table) + (dst_positive_scale_weighted_add_firstoutput_table))) + (((dst_negative_code_weighted_add_firstoutput_table) + (dst_negative_scale_weighted_add_firstoutput_table)) * S ((dst_negative_code_weighted_add_firstoutput_table) + (dst_negative_scale_weighted_add_firstoutput_table)) + ((dst_negative_scale_weighted_add_firstoutput_table) + (dst_negative_scale_weighted_add_firstoutput_table)))) + ((((dst_negative_code_weighted_add_firstoutput_table) + (dst_negative_scale_weighted_add_firstoutput_table)) * S ((dst_negative_code_weighted_add_firstoutput_table) + (dst_negative_scale_weighted_add_firstoutput_table)) + ((dst_negative_scale_weighted_add_firstoutput_table) + (dst_negative_scale_weighted_add_firstoutput_table))) + (((dst_negative_code_weighted_add_firstoutput_table) + (dst_negative_scale_weighted_add_firstoutput_table)) * S ((dst_negative_code_weighted_add_firstoutput_table) + (dst_negative_scale_weighted_add_firstoutput_table)) + ((dst_negative_scale_weighted_add_firstoutput_table) + (dst_negative_scale_weighted_add_firstoutput_table)))))) /\ (forall dst_index_weighted_add_firstoutput_table. (exists pvs_le_gap_weighted_add_firstoutput_tabledomain. pvs_le_gap_weighted_add_firstoutput_tabledomain + (dst_index_weighted_add_firstoutput_table) = (l)) -> exists dst_positive_weighted_add_firstoutput_table dst_negative_weighted_add_firstoutput_table dst_value_weighted_add_firstoutput_table. ((((exists ff_h_pvs_weighted_add_firstoutput_tableentrypositive. ff_h_pvs_weighted_add_firstoutput_tableentrypositive + S (dst_positive_weighted_add_firstoutput_table) = S ((S (dst_index_weighted_add_firstoutput_table)) * dst_positive_scale_weighted_add_firstoutput_table)) /\ exists ff_q_pvs_weighted_add_firstoutput_tableentrypositive. dst_positive_code_weighted_add_firstoutput_table = ff_q_pvs_weighted_add_firstoutput_tableentrypositive * S ((S (dst_index_weighted_add_firstoutput_table)) * dst_positive_scale_weighted_add_firstoutput_table) + (dst_positive_weighted_add_firstoutput_table))) /\ (((((exists ff_h_pvs_weighted_add_firstoutput_tableentrynegative. ff_h_pvs_weighted_add_firstoutput_tableentrynegative + S (dst_negative_weighted_add_firstoutput_table) = S ((S (dst_index_weighted_add_firstoutput_table)) * dst_negative_scale_weighted_add_firstoutput_table)) /\ exists ff_q_pvs_weighted_add_firstoutput_tableentrynegative. dst_negative_code_weighted_add_firstoutput_table = ff_q_pvs_weighted_add_firstoutput_tableentrynegative * S ((S (dst_index_weighted_add_firstoutput_table)) * dst_negative_scale_weighted_add_firstoutput_table) + (dst_negative_weighted_add_firstoutput_table))) /\ (exists ge_balance_positive_weighted_add_firstoutput_tableentryvalue ge_balance_negative_weighted_add_firstoutput_tableentryvalue. (((((dst_value_weighted_add_firstoutput_table) = 2 * (ge_balance_positive_weighted_add_firstoutput_tableentryvalue) /\ (ge_balance_negative_weighted_add_firstoutput_tableentryvalue) = 0) \/ exists ge_signed_half_weighted_add_firstoutput_tableentryvaluedecode. (((dst_value_weighted_add_firstoutput_table) = 2 * ge_signed_half_weighted_add_firstoutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_weighted_add_firstoutput_tableentryvalue) = 0) /\ (ge_balance_negative_weighted_add_firstoutput_tableentryvalue) = S ge_signed_half_weighted_add_firstoutput_tableentryvaluedecode))) /\ ((dst_positive_weighted_add_firstoutput_table) + ge_balance_negative_weighted_add_firstoutput_tableentryvalue = (dst_negative_weighted_add_firstoutput_table) + ge_balance_positive_weighted_add_firstoutput_tableentryvalue))))))))) /\ (forall sto_index_weighted_add_firstentries. (exists pvs_gap_weighted_add_firstentriesbound. pvs_gap_weighted_add_firstentriesbound + S (sto_index_weighted_add_firstentries) = (l)) -> exists sto_left_weighted_add_firstentries sto_right_weighted_add_firstentries sto_output_weighted_add_firstentries. ((exists dst_positive_code_weighted_add_firstentriesentryleft dst_positive_scale_weighted_add_firstentriesentryleft dst_negative_code_weighted_add_firstentriesentryleft dst_negative_scale_weighted_add_firstentriesentryleft dst_positive_weighted_add_firstentriesentryleft dst_negative_weighted_add_firstentriesentryleft. (((W) = (((((dst_positive_code_weighted_add_firstentriesentryleft) + (dst_positive_scale_weighted_add_firstentriesentryleft)) * S ((dst_positive_code_weighted_add_firstentriesentryleft) + (dst_positive_scale_weighted_add_firstentriesentryleft)) + ((dst_positive_scale_weighted_add_firstentriesentryleft) + (dst_positive_scale_weighted_add_firstentriesentryleft))) + (((dst_negative_code_weighted_add_firstentriesentryleft) + (dst_negative_scale_weighted_add_firstentriesentryleft)) * S ((dst_negative_code_weighted_add_firstentriesentryleft) + (dst_negative_scale_weighted_add_firstentriesentryleft)) + ((dst_negative_scale_weighted_add_firstentriesentryleft) + (dst_negative_scale_weighted_add_firstentriesentryleft)))) * S ((((dst_positive_code_weighted_add_firstentriesentryleft) + (dst_positive_scale_weighted_add_firstentriesentryleft)) * S ((dst_positive_code_weighted_add_firstentriesentryleft) + (dst_positive_scale_weighted_add_firstentriesentryleft)) + ((dst_positive_scale_weighted_add_firstentriesentryleft) + (dst_positive_scale_weighted_add_firstentriesentryleft))) + (((dst_negative_code_weighted_add_firstentriesentryleft) + (dst_negative_scale_weighted_add_firstentriesentryleft)) * S ((dst_negative_code_weighted_add_firstentriesentryleft) + (dst_negative_scale_weighted_add_firstentriesentryleft)) + ((dst_negative_scale_weighted_add_firstentriesentryleft) + (dst_negative_scale_weighted_add_firstentriesentryleft)))) + ((((dst_negative_code_weighted_add_firstentriesentryleft) + (dst_negative_scale_weighted_add_firstentriesentryleft)) * S ((dst_negative_code_weighted_add_firstentriesentryleft) + (dst_negative_scale_weighted_add_firstentriesentryleft)) + ((dst_negative_scale_weighted_add_firstentriesentryleft) + (dst_negative_scale_weighted_add_firstentriesentryleft))) + (((dst_negative_code_weighted_add_firstentriesentryleft) + (dst_negative_scale_weighted_add_firstentriesentryleft)) * S ((dst_negative_code_weighted_add_firstentriesentryleft) + (dst_negative_scale_weighted_add_firstentriesentryleft)) + ((dst_negative_scale_weighted_add_firstentriesentryleft) + (dst_negative_scale_weighted_add_firstentriesentryleft)))))) /\ (((((exists ff_h_pvs_weighted_add_firstentriesentryleftpositive. ff_h_pvs_weighted_add_firstentriesentryleftpositive + S (dst_positive_weighted_add_firstentriesentryleft) = S ((S (sto_index_weighted_add_firstentries)) * dst_positive_scale_weighted_add_firstentriesentryleft)) /\ exists ff_q_pvs_weighted_add_firstentriesentryleftpositive. dst_positive_code_weighted_add_firstentriesentryleft = ff_q_pvs_weighted_add_firstentriesentryleftpositive * S ((S (sto_index_weighted_add_firstentries)) * dst_positive_scale_weighted_add_firstentriesentryleft) + (dst_positive_weighted_add_firstentriesentryleft))) /\ (((((exists ff_h_pvs_weighted_add_firstentriesentryleftnegative. ff_h_pvs_weighted_add_firstentriesentryleftnegative + S (dst_negative_weighted_add_firstentriesentryleft) = S ((S (sto_index_weighted_add_firstentries)) * dst_negative_scale_weighted_add_firstentriesentryleft)) /\ exists ff_q_pvs_weighted_add_firstentriesentryleftnegative. dst_negative_code_weighted_add_firstentriesentryleft = ff_q_pvs_weighted_add_firstentriesentryleftnegative * S ((S (sto_index_weighted_add_firstentries)) * dst_negative_scale_weighted_add_firstentriesentryleft) + (dst_negative_weighted_add_firstentriesentryleft))) /\ (exists ge_balance_positive_weighted_add_firstentriesentryleftvalue ge_balance_negative_weighted_add_firstentriesentryleftvalue. (((((sto_left_weighted_add_firstentries) = 2 * (ge_balance_positive_weighted_add_firstentriesentryleftvalue) /\ (ge_balance_negative_weighted_add_firstentriesentryleftvalue) = 0) \/ exists ge_signed_half_weighted_add_firstentriesentryleftvaluedecode. (((sto_left_weighted_add_firstentries) = 2 * ge_signed_half_weighted_add_firstentriesentryleftvaluedecode + 1 /\ (ge_balance_positive_weighted_add_firstentriesentryleftvalue) = 0) /\ (ge_balance_negative_weighted_add_firstentriesentryleftvalue) = S ge_signed_half_weighted_add_firstentriesentryleftvaluedecode))) /\ ((dst_positive_weighted_add_firstentriesentryleft) + ge_balance_negative_weighted_add_firstentriesentryleftvalue = (dst_negative_weighted_add_firstentriesentryleft) + ge_balance_positive_weighted_add_firstentriesentryleftvalue))))))))) /\ (((exists dst_positive_code_weighted_add_firstentriesentryright dst_positive_scale_weighted_add_firstentriesentryright dst_negative_code_weighted_add_firstentriesentryright dst_negative_scale_weighted_add_firstentriesentryright dst_positive_weighted_add_firstentriesentryright dst_negative_weighted_add_firstentriesentryright. (((F) = (((((dst_positive_code_weighted_add_firstentriesentryright) + (dst_positive_scale_weighted_add_firstentriesentryright)) * S ((dst_positive_code_weighted_add_firstentriesentryright) + (dst_positive_scale_weighted_add_firstentriesentryright)) + ((dst_positive_scale_weighted_add_firstentriesentryright) + (dst_positive_scale_weighted_add_firstentriesentryright))) + (((dst_negative_code_weighted_add_firstentriesentryright) + (dst_negative_scale_weighted_add_firstentriesentryright)) * S ((dst_negative_code_weighted_add_firstentriesentryright) + (dst_negative_scale_weighted_add_firstentriesentryright)) + ((dst_negative_scale_weighted_add_firstentriesentryright) + (dst_negative_scale_weighted_add_firstentriesentryright)))) * S ((((dst_positive_code_weighted_add_firstentriesentryright) + (dst_positive_scale_weighted_add_firstentriesentryright)) * S ((dst_positive_code_weighted_add_firstentriesentryright) + (dst_positive_scale_weighted_add_firstentriesentryright)) + ((dst_positive_scale_weighted_add_firstentriesentryright) + (dst_positive_scale_weighted_add_firstentriesentryright))) + (((dst_negative_code_weighted_add_firstentriesentryright) + (dst_negative_scale_weighted_add_firstentriesentryright)) * S ((dst_negative_code_weighted_add_firstentriesentryright) + (dst_negative_scale_weighted_add_firstentriesentryright)) + ((dst_negative_scale_weighted_add_firstentriesentryright) + (dst_negative_scale_weighted_add_firstentriesentryright)))) + ((((dst_negative_code_weighted_add_firstentriesentryright) + (dst_negative_scale_weighted_add_firstentriesentryright)) * S ((dst_negative_code_weighted_add_firstentriesentryright) + (dst_negative_scale_weighted_add_firstentriesentryright)) + ((dst_negative_scale_weighted_add_firstentriesentryright) + (dst_negative_scale_weighted_add_firstentriesentryright))) + (((dst_negative_code_weighted_add_firstentriesentryright) + (dst_negative_scale_weighted_add_firstentriesentryright)) * S ((dst_negative_code_weighted_add_firstentriesentryright) + (dst_negative_scale_weighted_add_firstentriesentryright)) + ((dst_negative_scale_weighted_add_firstentriesentryright) + (dst_negative_scale_weighted_add_firstentriesentryright)))))) /\ (((((exists ff_h_pvs_weighted_add_firstentriesentryrightpositive. ff_h_pvs_weighted_add_firstentriesentryrightpositive + S (dst_positive_weighted_add_firstentriesentryright) = S ((S (sto_index_weighted_add_firstentries)) * dst_positive_scale_weighted_add_firstentriesentryright)) /\ exists ff_q_pvs_weighted_add_firstentriesentryrightpositive. dst_positive_code_weighted_add_firstentriesentryright = ff_q_pvs_weighted_add_firstentriesentryrightpositive * S ((S (sto_index_weighted_add_firstentries)) * dst_positive_scale_weighted_add_firstentriesentryright) + (dst_positive_weighted_add_firstentriesentryright))) /\ (((((exists ff_h_pvs_weighted_add_firstentriesentryrightnegative. ff_h_pvs_weighted_add_firstentriesentryrightnegative + S (dst_negative_weighted_add_firstentriesentryright) = S ((S (sto_index_weighted_add_firstentries)) * dst_negative_scale_weighted_add_firstentriesentryright)) /\ exists ff_q_pvs_weighted_add_firstentriesentryrightnegative. dst_negative_code_weighted_add_firstentriesentryright = ff_q_pvs_weighted_add_firstentriesentryrightnegative * S ((S (sto_index_weighted_add_firstentries)) * dst_negative_scale_weighted_add_firstentriesentryright) + (dst_negative_weighted_add_firstentriesentryright))) /\ (exists ge_balance_positive_weighted_add_firstentriesentryrightvalue ge_balance_negative_weighted_add_firstentriesentryrightvalue. (((((sto_right_weighted_add_firstentries) = 2 * (ge_balance_positive_weighted_add_firstentriesentryrightvalue) /\ (ge_balance_negative_weighted_add_firstentriesentryrightvalue) = 0) \/ exists ge_signed_half_weighted_add_firstentriesentryrightvaluedecode. (((sto_right_weighted_add_firstentries) = 2 * ge_signed_half_weighted_add_firstentriesentryrightvaluedecode + 1 /\ (ge_balance_positive_weighted_add_firstentriesentryrightvalue) = 0) /\ (ge_balance_negative_weighted_add_firstentriesentryrightvalue) = S ge_signed_half_weighted_add_firstentriesentryrightvaluedecode))) /\ ((dst_positive_weighted_add_firstentriesentryright) + ge_balance_negative_weighted_add_firstentriesentryrightvalue = (dst_negative_weighted_add_firstentriesentryright) + ge_balance_positive_weighted_add_firstentriesentryrightvalue))))))))) /\ (((exists dst_positive_code_weighted_add_firstentriesentryoutput dst_positive_scale_weighted_add_firstentriesentryoutput dst_negative_code_weighted_add_firstentriesentryoutput dst_negative_scale_weighted_add_firstentriesentryoutput dst_positive_weighted_add_firstentriesentryoutput dst_negative_weighted_add_firstentriesentryoutput. (((P) = (((((dst_positive_code_weighted_add_firstentriesentryoutput) + (dst_positive_scale_weighted_add_firstentriesentryoutput)) * S ((dst_positive_code_weighted_add_firstentriesentryoutput) + (dst_positive_scale_weighted_add_firstentriesentryoutput)) + ((dst_positive_scale_weighted_add_firstentriesentryoutput) + (dst_positive_scale_weighted_add_firstentriesentryoutput))) + (((dst_negative_code_weighted_add_firstentriesentryoutput) + (dst_negative_scale_weighted_add_firstentriesentryoutput)) * S ((dst_negative_code_weighted_add_firstentriesentryoutput) + (dst_negative_scale_weighted_add_firstentriesentryoutput)) + ((dst_negative_scale_weighted_add_firstentriesentryoutput) + (dst_negative_scale_weighted_add_firstentriesentryoutput)))) * S ((((dst_positive_code_weighted_add_firstentriesentryoutput) + (dst_positive_scale_weighted_add_firstentriesentryoutput)) * S ((dst_positive_code_weighted_add_firstentriesentryoutput) + (dst_positive_scale_weighted_add_firstentriesentryoutput)) + ((dst_positive_scale_weighted_add_firstentriesentryoutput) + (dst_positive_scale_weighted_add_firstentriesentryoutput))) + (((dst_negative_code_weighted_add_firstentriesentryoutput) + (dst_negative_scale_weighted_add_firstentriesentryoutput)) * S ((dst_negative_code_weighted_add_firstentriesentryoutput) + (dst_negative_scale_weighted_add_firstentriesentryoutput)) + ((dst_negative_scale_weighted_add_firstentriesentryoutput) + (dst_negative_scale_weighted_add_firstentriesentryoutput)))) + ((((dst_negative_code_weighted_add_firstentriesentryoutput) + (dst_negative_scale_weighted_add_firstentriesentryoutput)) * S ((dst_negative_code_weighted_add_firstentriesentryoutput) + (dst_negative_scale_weighted_add_firstentriesentryoutput)) + ((dst_negative_scale_weighted_add_firstentriesentryoutput) + (dst_negative_scale_weighted_add_firstentriesentryoutput))) + (((dst_negative_code_weighted_add_firstentriesentryoutput) + (dst_negative_scale_weighted_add_firstentriesentryoutput)) * S ((dst_negative_code_weighted_add_firstentriesentryoutput) + (dst_negative_scale_weighted_add_firstentriesentryoutput)) + ((dst_negative_scale_weighted_add_firstentriesentryoutput) + (dst_negative_scale_weighted_add_firstentriesentryoutput)))))) /\ (((((exists ff_h_pvs_weighted_add_firstentriesentryoutputpositive. ff_h_pvs_weighted_add_firstentriesentryoutputpositive + S (dst_positive_weighted_add_firstentriesentryoutput) = S ((S (sto_index_weighted_add_firstentries)) * dst_positive_scale_weighted_add_firstentriesentryoutput)) /\ exists ff_q_pvs_weighted_add_firstentriesentryoutputpositive. dst_positive_code_weighted_add_firstentriesentryoutput = ff_q_pvs_weighted_add_firstentriesentryoutputpositive * S ((S (sto_index_weighted_add_firstentries)) * dst_positive_scale_weighted_add_firstentriesentryoutput) + (dst_positive_weighted_add_firstentriesentryoutput))) /\ (((((exists ff_h_pvs_weighted_add_firstentriesentryoutputnegative. ff_h_pvs_weighted_add_firstentriesentryoutputnegative + S (dst_negative_weighted_add_firstentriesentryoutput) = S ((S (sto_index_weighted_add_firstentries)) * dst_negative_scale_weighted_add_firstentriesentryoutput)) /\ exists ff_q_pvs_weighted_add_firstentriesentryoutputnegative. dst_negative_code_weighted_add_firstentriesentryoutput = ff_q_pvs_weighted_add_firstentriesentryoutputnegative * S ((S (sto_index_weighted_add_firstentries)) * dst_negative_scale_weighted_add_firstentriesentryoutput) + (dst_negative_weighted_add_firstentriesentryoutput))) /\ (exists ge_balance_positive_weighted_add_firstentriesentryoutputvalue ge_balance_negative_weighted_add_firstentriesentryoutputvalue. (((((sto_output_weighted_add_firstentries) = 2 * (ge_balance_positive_weighted_add_firstentriesentryoutputvalue) /\ (ge_balance_negative_weighted_add_firstentriesentryoutputvalue) = 0) \/ exists ge_signed_half_weighted_add_firstentriesentryoutputvaluedecode. (((sto_output_weighted_add_firstentries) = 2 * ge_signed_half_weighted_add_firstentriesentryoutputvaluedecode + 1 /\ (ge_balance_positive_weighted_add_firstentriesentryoutputvalue) = 0) /\ (ge_balance_negative_weighted_add_firstentriesentryoutputvalue) = S ge_signed_half_weighted_add_firstentriesentryoutputvaluedecode))) /\ ((dst_positive_weighted_add_firstentriesentryoutput) + ge_balance_negative_weighted_add_firstentriesentryoutputvalue = (dst_negative_weighted_add_firstentriesentryoutput) + ge_balance_positive_weighted_add_firstentriesentryoutputvalue))))))))) /\ (exists sto_ap_weighted_add_firstentriesentryoperation sto_an_weighted_add_firstentriesentryoperation sto_bp_weighted_add_firstentriesentryoperation sto_bn_weighted_add_firstentriesentryoperation sto_cp_weighted_add_firstentriesentryoperation sto_cn_weighted_add_firstentriesentryoperation. (((((sto_left_weighted_add_firstentries) = 2 * (sto_ap_weighted_add_firstentriesentryoperation) /\ (sto_an_weighted_add_firstentriesentryoperation) = 0) \/ exists ge_signed_half_weighted_add_firstentriesentryoperationleft. (((sto_left_weighted_add_firstentries) = 2 * ge_signed_half_weighted_add_firstentriesentryoperationleft + 1 /\ (sto_ap_weighted_add_firstentriesentryoperation) = 0) /\ (sto_an_weighted_add_firstentriesentryoperation) = S ge_signed_half_weighted_add_firstentriesentryoperationleft))) /\ ((((((sto_right_weighted_add_firstentries) = 2 * (sto_bp_weighted_add_firstentriesentryoperation) /\ (sto_bn_weighted_add_firstentriesentryoperation) = 0) \/ exists ge_signed_half_weighted_add_firstentriesentryoperationright. (((sto_right_weighted_add_firstentries) = 2 * ge_signed_half_weighted_add_firstentriesentryoperationright + 1 /\ (sto_bp_weighted_add_firstentriesentryoperation) = 0) /\ (sto_bn_weighted_add_firstentriesentryoperation) = S ge_signed_half_weighted_add_firstentriesentryoperationright))) /\ ((((((sto_output_weighted_add_firstentries) = 2 * (sto_cp_weighted_add_firstentriesentryoperation) /\ (sto_cn_weighted_add_firstentriesentryoperation) = 0) \/ exists ge_signed_half_weighted_add_firstentriesentryoperationoutput. (((sto_output_weighted_add_firstentries) = 2 * ge_signed_half_weighted_add_firstentriesentryoperationoutput + 1 /\ (sto_cp_weighted_add_firstentriesentryoperation) = 0) /\ (sto_cn_weighted_add_firstentriesentryoperation) = S ge_signed_half_weighted_add_firstentriesentryoperationoutput))) /\ ((sto_ap_weighted_add_firstentriesentryoperation * sto_bp_weighted_add_firstentriesentryoperation + sto_an_weighted_add_firstentriesentryoperation * sto_bn_weighted_add_firstentriesentryoperation) + sto_cn_weighted_add_firstentriesentryoperation = (sto_ap_weighted_add_firstentriesentryoperation * sto_bn_weighted_add_firstentriesentryoperation + sto_an_weighted_add_firstentriesentryoperation * sto_bp_weighted_add_firstentriesentryoperation) + sto_cp_weighted_add_firstentriesentryoperation))))))))))))))))))) -> (((exists dst_positive_code_weighted_add_secondleft_table dst_positive_scale_weighted_add_secondleft_table dst_negative_code_weighted_add_secondleft_table dst_negative_scale_weighted_add_secondleft_table. (((W) = (((((dst_positive_code_weighted_add_secondleft_table) + (dst_positive_scale_weighted_add_secondleft_table)) * S ((dst_positive_code_weighted_add_secondleft_table) + (dst_positive_scale_weighted_add_secondleft_table)) + ((dst_positive_scale_weighted_add_secondleft_table) + (dst_positive_scale_weighted_add_secondleft_table))) + (((dst_negative_code_weighted_add_secondleft_table) + (dst_negative_scale_weighted_add_secondleft_table)) * S ((dst_negative_code_weighted_add_secondleft_table) + (dst_negative_scale_weighted_add_secondleft_table)) + ((dst_negative_scale_weighted_add_secondleft_table) + (dst_negative_scale_weighted_add_secondleft_table)))) * S ((((dst_positive_code_weighted_add_secondleft_table) + (dst_positive_scale_weighted_add_secondleft_table)) * S ((dst_positive_code_weighted_add_secondleft_table) + (dst_positive_scale_weighted_add_secondleft_table)) + ((dst_positive_scale_weighted_add_secondleft_table) + (dst_positive_scale_weighted_add_secondleft_table))) + (((dst_negative_code_weighted_add_secondleft_table) + (dst_negative_scale_weighted_add_secondleft_table)) * S ((dst_negative_code_weighted_add_secondleft_table) + (dst_negative_scale_weighted_add_secondleft_table)) + ((dst_negative_scale_weighted_add_secondleft_table) + (dst_negative_scale_weighted_add_secondleft_table)))) + ((((dst_negative_code_weighted_add_secondleft_table) + (dst_negative_scale_weighted_add_secondleft_table)) * S ((dst_negative_code_weighted_add_secondleft_table) + (dst_negative_scale_weighted_add_secondleft_table)) + ((dst_negative_scale_weighted_add_secondleft_table) + (dst_negative_scale_weighted_add_secondleft_table))) + (((dst_negative_code_weighted_add_secondleft_table) + (dst_negative_scale_weighted_add_secondleft_table)) * S ((dst_negative_code_weighted_add_secondleft_table) + (dst_negative_scale_weighted_add_secondleft_table)) + ((dst_negative_scale_weighted_add_secondleft_table) + (dst_negative_scale_weighted_add_secondleft_table)))))) /\ (forall dst_index_weighted_add_secondleft_table. (exists pvs_le_gap_weighted_add_secondleft_tabledomain. pvs_le_gap_weighted_add_secondleft_tabledomain + (dst_index_weighted_add_secondleft_table) = (l)) -> exists dst_positive_weighted_add_secondleft_table dst_negative_weighted_add_secondleft_table dst_value_weighted_add_secondleft_table. ((((exists ff_h_pvs_weighted_add_secondleft_tableentrypositive. ff_h_pvs_weighted_add_secondleft_tableentrypositive + S (dst_positive_weighted_add_secondleft_table) = S ((S (dst_index_weighted_add_secondleft_table)) * dst_positive_scale_weighted_add_secondleft_table)) /\ exists ff_q_pvs_weighted_add_secondleft_tableentrypositive. dst_positive_code_weighted_add_secondleft_table = ff_q_pvs_weighted_add_secondleft_tableentrypositive * S ((S (dst_index_weighted_add_secondleft_table)) * dst_positive_scale_weighted_add_secondleft_table) + (dst_positive_weighted_add_secondleft_table))) /\ (((((exists ff_h_pvs_weighted_add_secondleft_tableentrynegative. ff_h_pvs_weighted_add_secondleft_tableentrynegative + S (dst_negative_weighted_add_secondleft_table) = S ((S (dst_index_weighted_add_secondleft_table)) * dst_negative_scale_weighted_add_secondleft_table)) /\ exists ff_q_pvs_weighted_add_secondleft_tableentrynegative. dst_negative_code_weighted_add_secondleft_table = ff_q_pvs_weighted_add_secondleft_tableentrynegative * S ((S (dst_index_weighted_add_secondleft_table)) * dst_negative_scale_weighted_add_secondleft_table) + (dst_negative_weighted_add_secondleft_table))) /\ (exists ge_balance_positive_weighted_add_secondleft_tableentryvalue ge_balance_negative_weighted_add_secondleft_tableentryvalue. (((((dst_value_weighted_add_secondleft_table) = 2 * (ge_balance_positive_weighted_add_secondleft_tableentryvalue) /\ (ge_balance_negative_weighted_add_secondleft_tableentryvalue) = 0) \/ exists ge_signed_half_weighted_add_secondleft_tableentryvaluedecode. (((dst_value_weighted_add_secondleft_table) = 2 * ge_signed_half_weighted_add_secondleft_tableentryvaluedecode + 1 /\ (ge_balance_positive_weighted_add_secondleft_tableentryvalue) = 0) /\ (ge_balance_negative_weighted_add_secondleft_tableentryvalue) = S ge_signed_half_weighted_add_secondleft_tableentryvaluedecode))) /\ ((dst_positive_weighted_add_secondleft_table) + ge_balance_negative_weighted_add_secondleft_tableentryvalue = (dst_negative_weighted_add_secondleft_table) + ge_balance_positive_weighted_add_secondleft_tableentryvalue))))))))) /\ (((exists dst_positive_code_weighted_add_secondright_table dst_positive_scale_weighted_add_secondright_table dst_negative_code_weighted_add_secondright_table dst_negative_scale_weighted_add_secondright_table. (((G) = (((((dst_positive_code_weighted_add_secondright_table) + (dst_positive_scale_weighted_add_secondright_table)) * S ((dst_positive_code_weighted_add_secondright_table) + (dst_positive_scale_weighted_add_secondright_table)) + ((dst_positive_scale_weighted_add_secondright_table) + (dst_positive_scale_weighted_add_secondright_table))) + (((dst_negative_code_weighted_add_secondright_table) + (dst_negative_scale_weighted_add_secondright_table)) * S ((dst_negative_code_weighted_add_secondright_table) + (dst_negative_scale_weighted_add_secondright_table)) + ((dst_negative_scale_weighted_add_secondright_table) + (dst_negative_scale_weighted_add_secondright_table)))) * S ((((dst_positive_code_weighted_add_secondright_table) + (dst_positive_scale_weighted_add_secondright_table)) * S ((dst_positive_code_weighted_add_secondright_table) + (dst_positive_scale_weighted_add_secondright_table)) + ((dst_positive_scale_weighted_add_secondright_table) + (dst_positive_scale_weighted_add_secondright_table))) + (((dst_negative_code_weighted_add_secondright_table) + (dst_negative_scale_weighted_add_secondright_table)) * S ((dst_negative_code_weighted_add_secondright_table) + (dst_negative_scale_weighted_add_secondright_table)) + ((dst_negative_scale_weighted_add_secondright_table) + (dst_negative_scale_weighted_add_secondright_table)))) + ((((dst_negative_code_weighted_add_secondright_table) + (dst_negative_scale_weighted_add_secondright_table)) * S ((dst_negative_code_weighted_add_secondright_table) + (dst_negative_scale_weighted_add_secondright_table)) + ((dst_negative_scale_weighted_add_secondright_table) + (dst_negative_scale_weighted_add_secondright_table))) + (((dst_negative_code_weighted_add_secondright_table) + (dst_negative_scale_weighted_add_secondright_table)) * S ((dst_negative_code_weighted_add_secondright_table) + (dst_negative_scale_weighted_add_secondright_table)) + ((dst_negative_scale_weighted_add_secondright_table) + (dst_negative_scale_weighted_add_secondright_table)))))) /\ (forall dst_index_weighted_add_secondright_table. (exists pvs_le_gap_weighted_add_secondright_tabledomain. pvs_le_gap_weighted_add_secondright_tabledomain + (dst_index_weighted_add_secondright_table) = (l)) -> exists dst_positive_weighted_add_secondright_table dst_negative_weighted_add_secondright_table dst_value_weighted_add_secondright_table. ((((exists ff_h_pvs_weighted_add_secondright_tableentrypositive. ff_h_pvs_weighted_add_secondright_tableentrypositive + S (dst_positive_weighted_add_secondright_table) = S ((S (dst_index_weighted_add_secondright_table)) * dst_positive_scale_weighted_add_secondright_table)) /\ exists ff_q_pvs_weighted_add_secondright_tableentrypositive. dst_positive_code_weighted_add_secondright_table = ff_q_pvs_weighted_add_secondright_tableentrypositive * S ((S (dst_index_weighted_add_secondright_table)) * dst_positive_scale_weighted_add_secondright_table) + (dst_positive_weighted_add_secondright_table))) /\ (((((exists ff_h_pvs_weighted_add_secondright_tableentrynegative. ff_h_pvs_weighted_add_secondright_tableentrynegative + S (dst_negative_weighted_add_secondright_table) = S ((S (dst_index_weighted_add_secondright_table)) * dst_negative_scale_weighted_add_secondright_table)) /\ exists ff_q_pvs_weighted_add_secondright_tableentrynegative. dst_negative_code_weighted_add_secondright_table = ff_q_pvs_weighted_add_secondright_tableentrynegative * S ((S (dst_index_weighted_add_secondright_table)) * dst_negative_scale_weighted_add_secondright_table) + (dst_negative_weighted_add_secondright_table))) /\ (exists ge_balance_positive_weighted_add_secondright_tableentryvalue ge_balance_negative_weighted_add_secondright_tableentryvalue. (((((dst_value_weighted_add_secondright_table) = 2 * (ge_balance_positive_weighted_add_secondright_tableentryvalue) /\ (ge_balance_negative_weighted_add_secondright_tableentryvalue) = 0) \/ exists ge_signed_half_weighted_add_secondright_tableentryvaluedecode. (((dst_value_weighted_add_secondright_table) = 2 * ge_signed_half_weighted_add_secondright_tableentryvaluedecode + 1 /\ (ge_balance_positive_weighted_add_secondright_tableentryvalue) = 0) /\ (ge_balance_negative_weighted_add_secondright_tableentryvalue) = S ge_signed_half_weighted_add_secondright_tableentryvaluedecode))) /\ ((dst_positive_weighted_add_secondright_table) + ge_balance_negative_weighted_add_secondright_tableentryvalue = (dst_negative_weighted_add_secondright_table) + ge_balance_positive_weighted_add_secondright_tableentryvalue))))))))) /\ (((exists dst_positive_code_weighted_add_secondoutput_table dst_positive_scale_weighted_add_secondoutput_table dst_negative_code_weighted_add_secondoutput_table dst_negative_scale_weighted_add_secondoutput_table. (((Q) = (((((dst_positive_code_weighted_add_secondoutput_table) + (dst_positive_scale_weighted_add_secondoutput_table)) * S ((dst_positive_code_weighted_add_secondoutput_table) + (dst_positive_scale_weighted_add_secondoutput_table)) + ((dst_positive_scale_weighted_add_secondoutput_table) + (dst_positive_scale_weighted_add_secondoutput_table))) + (((dst_negative_code_weighted_add_secondoutput_table) + (dst_negative_scale_weighted_add_secondoutput_table)) * S ((dst_negative_code_weighted_add_secondoutput_table) + (dst_negative_scale_weighted_add_secondoutput_table)) + ((dst_negative_scale_weighted_add_secondoutput_table) + (dst_negative_scale_weighted_add_secondoutput_table)))) * S ((((dst_positive_code_weighted_add_secondoutput_table) + (dst_positive_scale_weighted_add_secondoutput_table)) * S ((dst_positive_code_weighted_add_secondoutput_table) + (dst_positive_scale_weighted_add_secondoutput_table)) + ((dst_positive_scale_weighted_add_secondoutput_table) + (dst_positive_scale_weighted_add_secondoutput_table))) + (((dst_negative_code_weighted_add_secondoutput_table) + (dst_negative_scale_weighted_add_secondoutput_table)) * S ((dst_negative_code_weighted_add_secondoutput_table) + (dst_negative_scale_weighted_add_secondoutput_table)) + ((dst_negative_scale_weighted_add_secondoutput_table) + (dst_negative_scale_weighted_add_secondoutput_table)))) + ((((dst_negative_code_weighted_add_secondoutput_table) + (dst_negative_scale_weighted_add_secondoutput_table)) * S ((dst_negative_code_weighted_add_secondoutput_table) + (dst_negative_scale_weighted_add_secondoutput_table)) + ((dst_negative_scale_weighted_add_secondoutput_table) + (dst_negative_scale_weighted_add_secondoutput_table))) + (((dst_negative_code_weighted_add_secondoutput_table) + (dst_negative_scale_weighted_add_secondoutput_table)) * S ((dst_negative_code_weighted_add_secondoutput_table) + (dst_negative_scale_weighted_add_secondoutput_table)) + ((dst_negative_scale_weighted_add_secondoutput_table) + (dst_negative_scale_weighted_add_secondoutput_table)))))) /\ (forall dst_index_weighted_add_secondoutput_table. (exists pvs_le_gap_weighted_add_secondoutput_tabledomain. pvs_le_gap_weighted_add_secondoutput_tabledomain + (dst_index_weighted_add_secondoutput_table) = (l)) -> exists dst_positive_weighted_add_secondoutput_table dst_negative_weighted_add_secondoutput_table dst_value_weighted_add_secondoutput_table. ((((exists ff_h_pvs_weighted_add_secondoutput_tableentrypositive. ff_h_pvs_weighted_add_secondoutput_tableentrypositive + S (dst_positive_weighted_add_secondoutput_table) = S ((S (dst_index_weighted_add_secondoutput_table)) * dst_positive_scale_weighted_add_secondoutput_table)) /\ exists ff_q_pvs_weighted_add_secondoutput_tableentrypositive. dst_positive_code_weighted_add_secondoutput_table = ff_q_pvs_weighted_add_secondoutput_tableentrypositive * S ((S (dst_index_weighted_add_secondoutput_table)) * dst_positive_scale_weighted_add_secondoutput_table) + (dst_positive_weighted_add_secondoutput_table))) /\ (((((exists ff_h_pvs_weighted_add_secondoutput_tableentrynegative. ff_h_pvs_weighted_add_secondoutput_tableentrynegative + S (dst_negative_weighted_add_secondoutput_table) = S ((S (dst_index_weighted_add_secondoutput_table)) * dst_negative_scale_weighted_add_secondoutput_table)) /\ exists ff_q_pvs_weighted_add_secondoutput_tableentrynegative. dst_negative_code_weighted_add_secondoutput_table = ff_q_pvs_weighted_add_secondoutput_tableentrynegative * S ((S (dst_index_weighted_add_secondoutput_table)) * dst_negative_scale_weighted_add_secondoutput_table) + (dst_negative_weighted_add_secondoutput_table))) /\ (exists ge_balance_positive_weighted_add_secondoutput_tableentryvalue ge_balance_negative_weighted_add_secondoutput_tableentryvalue. (((((dst_value_weighted_add_secondoutput_table) = 2 * (ge_balance_positive_weighted_add_secondoutput_tableentryvalue) /\ (ge_balance_negative_weighted_add_secondoutput_tableentryvalue) = 0) \/ exists ge_signed_half_weighted_add_secondoutput_tableentryvaluedecode. (((dst_value_weighted_add_secondoutput_table) = 2 * ge_signed_half_weighted_add_secondoutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_weighted_add_secondoutput_tableentryvalue) = 0) /\ (ge_balance_negative_weighted_add_secondoutput_tableentryvalue) = S ge_signed_half_weighted_add_secondoutput_tableentryvaluedecode))) /\ ((dst_positive_weighted_add_secondoutput_table) + ge_balance_negative_weighted_add_secondoutput_tableentryvalue = (dst_negative_weighted_add_secondoutput_table) + ge_balance_positive_weighted_add_secondoutput_tableentryvalue))))))))) /\ (forall sto_index_weighted_add_secondentries. (exists pvs_gap_weighted_add_secondentriesbound. pvs_gap_weighted_add_secondentriesbound + S (sto_index_weighted_add_secondentries) = (l)) -> exists sto_left_weighted_add_secondentries sto_right_weighted_add_secondentries sto_output_weighted_add_secondentries. ((exists dst_positive_code_weighted_add_secondentriesentryleft dst_positive_scale_weighted_add_secondentriesentryleft dst_negative_code_weighted_add_secondentriesentryleft dst_negative_scale_weighted_add_secondentriesentryleft dst_positive_weighted_add_secondentriesentryleft dst_negative_weighted_add_secondentriesentryleft. (((W) = (((((dst_positive_code_weighted_add_secondentriesentryleft) + (dst_positive_scale_weighted_add_secondentriesentryleft)) * S ((dst_positive_code_weighted_add_secondentriesentryleft) + (dst_positive_scale_weighted_add_secondentriesentryleft)) + ((dst_positive_scale_weighted_add_secondentriesentryleft) + (dst_positive_scale_weighted_add_secondentriesentryleft))) + (((dst_negative_code_weighted_add_secondentriesentryleft) + (dst_negative_scale_weighted_add_secondentriesentryleft)) * S ((dst_negative_code_weighted_add_secondentriesentryleft) + (dst_negative_scale_weighted_add_secondentriesentryleft)) + ((dst_negative_scale_weighted_add_secondentriesentryleft) + (dst_negative_scale_weighted_add_secondentriesentryleft)))) * S ((((dst_positive_code_weighted_add_secondentriesentryleft) + (dst_positive_scale_weighted_add_secondentriesentryleft)) * S ((dst_positive_code_weighted_add_secondentriesentryleft) + (dst_positive_scale_weighted_add_secondentriesentryleft)) + ((dst_positive_scale_weighted_add_secondentriesentryleft) + (dst_positive_scale_weighted_add_secondentriesentryleft))) + (((dst_negative_code_weighted_add_secondentriesentryleft) + (dst_negative_scale_weighted_add_secondentriesentryleft)) * S ((dst_negative_code_weighted_add_secondentriesentryleft) + (dst_negative_scale_weighted_add_secondentriesentryleft)) + ((dst_negative_scale_weighted_add_secondentriesentryleft) + (dst_negative_scale_weighted_add_secondentriesentryleft)))) + ((((dst_negative_code_weighted_add_secondentriesentryleft) + (dst_negative_scale_weighted_add_secondentriesentryleft)) * S ((dst_negative_code_weighted_add_secondentriesentryleft) + (dst_negative_scale_weighted_add_secondentriesentryleft)) + ((dst_negative_scale_weighted_add_secondentriesentryleft) + (dst_negative_scale_weighted_add_secondentriesentryleft))) + (((dst_negative_code_weighted_add_secondentriesentryleft) + (dst_negative_scale_weighted_add_secondentriesentryleft)) * S ((dst_negative_code_weighted_add_secondentriesentryleft) + (dst_negative_scale_weighted_add_secondentriesentryleft)) + ((dst_negative_scale_weighted_add_secondentriesentryleft) + (dst_negative_scale_weighted_add_secondentriesentryleft)))))) /\ (((((exists ff_h_pvs_weighted_add_secondentriesentryleftpositive. ff_h_pvs_weighted_add_secondentriesentryleftpositive + S (dst_positive_weighted_add_secondentriesentryleft) = S ((S (sto_index_weighted_add_secondentries)) * dst_positive_scale_weighted_add_secondentriesentryleft)) /\ exists ff_q_pvs_weighted_add_secondentriesentryleftpositive. dst_positive_code_weighted_add_secondentriesentryleft = ff_q_pvs_weighted_add_secondentriesentryleftpositive * S ((S (sto_index_weighted_add_secondentries)) * dst_positive_scale_weighted_add_secondentriesentryleft) + (dst_positive_weighted_add_secondentriesentryleft))) /\ (((((exists ff_h_pvs_weighted_add_secondentriesentryleftnegative. ff_h_pvs_weighted_add_secondentriesentryleftnegative + S (dst_negative_weighted_add_secondentriesentryleft) = S ((S (sto_index_weighted_add_secondentries)) * dst_negative_scale_weighted_add_secondentriesentryleft)) /\ exists ff_q_pvs_weighted_add_secondentriesentryleftnegative. dst_negative_code_weighted_add_secondentriesentryleft = ff_q_pvs_weighted_add_secondentriesentryleftnegative * S ((S (sto_index_weighted_add_secondentries)) * dst_negative_scale_weighted_add_secondentriesentryleft) + (dst_negative_weighted_add_secondentriesentryleft))) /\ (exists ge_balance_positive_weighted_add_secondentriesentryleftvalue ge_balance_negative_weighted_add_secondentriesentryleftvalue. (((((sto_left_weighted_add_secondentries) = 2 * (ge_balance_positive_weighted_add_secondentriesentryleftvalue) /\ (ge_balance_negative_weighted_add_secondentriesentryleftvalue) = 0) \/ exists ge_signed_half_weighted_add_secondentriesentryleftvaluedecode. (((sto_left_weighted_add_secondentries) = 2 * ge_signed_half_weighted_add_secondentriesentryleftvaluedecode + 1 /\ (ge_balance_positive_weighted_add_secondentriesentryleftvalue) = 0) /\ (ge_balance_negative_weighted_add_secondentriesentryleftvalue) = S ge_signed_half_weighted_add_secondentriesentryleftvaluedecode))) /\ ((dst_positive_weighted_add_secondentriesentryleft) + ge_balance_negative_weighted_add_secondentriesentryleftvalue = (dst_negative_weighted_add_secondentriesentryleft) + ge_balance_positive_weighted_add_secondentriesentryleftvalue))))))))) /\ (((exists dst_positive_code_weighted_add_secondentriesentryright dst_positive_scale_weighted_add_secondentriesentryright dst_negative_code_weighted_add_secondentriesentryright dst_negative_scale_weighted_add_secondentriesentryright dst_positive_weighted_add_secondentriesentryright dst_negative_weighted_add_secondentriesentryright. (((G) = (((((dst_positive_code_weighted_add_secondentriesentryright) + (dst_positive_scale_weighted_add_secondentriesentryright)) * S ((dst_positive_code_weighted_add_secondentriesentryright) + (dst_positive_scale_weighted_add_secondentriesentryright)) + ((dst_positive_scale_weighted_add_secondentriesentryright) + (dst_positive_scale_weighted_add_secondentriesentryright))) + (((dst_negative_code_weighted_add_secondentriesentryright) + (dst_negative_scale_weighted_add_secondentriesentryright)) * S ((dst_negative_code_weighted_add_secondentriesentryright) + (dst_negative_scale_weighted_add_secondentriesentryright)) + ((dst_negative_scale_weighted_add_secondentriesentryright) + (dst_negative_scale_weighted_add_secondentriesentryright)))) * S ((((dst_positive_code_weighted_add_secondentriesentryright) + (dst_positive_scale_weighted_add_secondentriesentryright)) * S ((dst_positive_code_weighted_add_secondentriesentryright) + (dst_positive_scale_weighted_add_secondentriesentryright)) + ((dst_positive_scale_weighted_add_secondentriesentryright) + (dst_positive_scale_weighted_add_secondentriesentryright))) + (((dst_negative_code_weighted_add_secondentriesentryright) + (dst_negative_scale_weighted_add_secondentriesentryright)) * S ((dst_negative_code_weighted_add_secondentriesentryright) + (dst_negative_scale_weighted_add_secondentriesentryright)) + ((dst_negative_scale_weighted_add_secondentriesentryright) + (dst_negative_scale_weighted_add_secondentriesentryright)))) + ((((dst_negative_code_weighted_add_secondentriesentryright) + (dst_negative_scale_weighted_add_secondentriesentryright)) * S ((dst_negative_code_weighted_add_secondentriesentryright) + (dst_negative_scale_weighted_add_secondentriesentryright)) + ((dst_negative_scale_weighted_add_secondentriesentryright) + (dst_negative_scale_weighted_add_secondentriesentryright))) + (((dst_negative_code_weighted_add_secondentriesentryright) + (dst_negative_scale_weighted_add_secondentriesentryright)) * S ((dst_negative_code_weighted_add_secondentriesentryright) + (dst_negative_scale_weighted_add_secondentriesentryright)) + ((dst_negative_scale_weighted_add_secondentriesentryright) + (dst_negative_scale_weighted_add_secondentriesentryright)))))) /\ (((((exists ff_h_pvs_weighted_add_secondentriesentryrightpositive. ff_h_pvs_weighted_add_secondentriesentryrightpositive + S (dst_positive_weighted_add_secondentriesentryright) = S ((S (sto_index_weighted_add_secondentries)) * dst_positive_scale_weighted_add_secondentriesentryright)) /\ exists ff_q_pvs_weighted_add_secondentriesentryrightpositive. dst_positive_code_weighted_add_secondentriesentryright = ff_q_pvs_weighted_add_secondentriesentryrightpositive * S ((S (sto_index_weighted_add_secondentries)) * dst_positive_scale_weighted_add_secondentriesentryright) + (dst_positive_weighted_add_secondentriesentryright))) /\ (((((exists ff_h_pvs_weighted_add_secondentriesentryrightnegative. ff_h_pvs_weighted_add_secondentriesentryrightnegative + S (dst_negative_weighted_add_secondentriesentryright) = S ((S (sto_index_weighted_add_secondentries)) * dst_negative_scale_weighted_add_secondentriesentryright)) /\ exists ff_q_pvs_weighted_add_secondentriesentryrightnegative. dst_negative_code_weighted_add_secondentriesentryright = ff_q_pvs_weighted_add_secondentriesentryrightnegative * S ((S (sto_index_weighted_add_secondentries)) * dst_negative_scale_weighted_add_secondentriesentryright) + (dst_negative_weighted_add_secondentriesentryright))) /\ (exists ge_balance_positive_weighted_add_secondentriesentryrightvalue ge_balance_negative_weighted_add_secondentriesentryrightvalue. (((((sto_right_weighted_add_secondentries) = 2 * (ge_balance_positive_weighted_add_secondentriesentryrightvalue) /\ (ge_balance_negative_weighted_add_secondentriesentryrightvalue) = 0) \/ exists ge_signed_half_weighted_add_secondentriesentryrightvaluedecode. (((sto_right_weighted_add_secondentries) = 2 * ge_signed_half_weighted_add_secondentriesentryrightvaluedecode + 1 /\ (ge_balance_positive_weighted_add_secondentriesentryrightvalue) = 0) /\ (ge_balance_negative_weighted_add_secondentriesentryrightvalue) = S ge_signed_half_weighted_add_secondentriesentryrightvaluedecode))) /\ ((dst_positive_weighted_add_secondentriesentryright) + ge_balance_negative_weighted_add_secondentriesentryrightvalue = (dst_negative_weighted_add_secondentriesentryright) + ge_balance_positive_weighted_add_secondentriesentryrightvalue))))))))) /\ (((exists dst_positive_code_weighted_add_secondentriesentryoutput dst_positive_scale_weighted_add_secondentriesentryoutput dst_negative_code_weighted_add_secondentriesentryoutput dst_negative_scale_weighted_add_secondentriesentryoutput dst_positive_weighted_add_secondentriesentryoutput dst_negative_weighted_add_secondentriesentryoutput. (((Q) = (((((dst_positive_code_weighted_add_secondentriesentryoutput) + (dst_positive_scale_weighted_add_secondentriesentryoutput)) * S ((dst_positive_code_weighted_add_secondentriesentryoutput) + (dst_positive_scale_weighted_add_secondentriesentryoutput)) + ((dst_positive_scale_weighted_add_secondentriesentryoutput) + (dst_positive_scale_weighted_add_secondentriesentryoutput))) + (((dst_negative_code_weighted_add_secondentriesentryoutput) + (dst_negative_scale_weighted_add_secondentriesentryoutput)) * S ((dst_negative_code_weighted_add_secondentriesentryoutput) + (dst_negative_scale_weighted_add_secondentriesentryoutput)) + ((dst_negative_scale_weighted_add_secondentriesentryoutput) + (dst_negative_scale_weighted_add_secondentriesentryoutput)))) * S ((((dst_positive_code_weighted_add_secondentriesentryoutput) + (dst_positive_scale_weighted_add_secondentriesentryoutput)) * S ((dst_positive_code_weighted_add_secondentriesentryoutput) + (dst_positive_scale_weighted_add_secondentriesentryoutput)) + ((dst_positive_scale_weighted_add_secondentriesentryoutput) + (dst_positive_scale_weighted_add_secondentriesentryoutput))) + (((dst_negative_code_weighted_add_secondentriesentryoutput) + (dst_negative_scale_weighted_add_secondentriesentryoutput)) * S ((dst_negative_code_weighted_add_secondentriesentryoutput) + (dst_negative_scale_weighted_add_secondentriesentryoutput)) + ((dst_negative_scale_weighted_add_secondentriesentryoutput) + (dst_negative_scale_weighted_add_secondentriesentryoutput)))) + ((((dst_negative_code_weighted_add_secondentriesentryoutput) + (dst_negative_scale_weighted_add_secondentriesentryoutput)) * S ((dst_negative_code_weighted_add_secondentriesentryoutput) + (dst_negative_scale_weighted_add_secondentriesentryoutput)) + ((dst_negative_scale_weighted_add_secondentriesentryoutput) + (dst_negative_scale_weighted_add_secondentriesentryoutput))) + (((dst_negative_code_weighted_add_secondentriesentryoutput) + (dst_negative_scale_weighted_add_secondentriesentryoutput)) * S ((dst_negative_code_weighted_add_secondentriesentryoutput) + (dst_negative_scale_weighted_add_secondentriesentryoutput)) + ((dst_negative_scale_weighted_add_secondentriesentryoutput) + (dst_negative_scale_weighted_add_secondentriesentryoutput)))))) /\ (((((exists ff_h_pvs_weighted_add_secondentriesentryoutputpositive. ff_h_pvs_weighted_add_secondentriesentryoutputpositive + S (dst_positive_weighted_add_secondentriesentryoutput) = S ((S (sto_index_weighted_add_secondentries)) * dst_positive_scale_weighted_add_secondentriesentryoutput)) /\ exists ff_q_pvs_weighted_add_secondentriesentryoutputpositive. dst_positive_code_weighted_add_secondentriesentryoutput = ff_q_pvs_weighted_add_secondentriesentryoutputpositive * S ((S (sto_index_weighted_add_secondentries)) * dst_positive_scale_weighted_add_secondentriesentryoutput) + (dst_positive_weighted_add_secondentriesentryoutput))) /\ (((((exists ff_h_pvs_weighted_add_secondentriesentryoutputnegative. ff_h_pvs_weighted_add_secondentriesentryoutputnegative + S (dst_negative_weighted_add_secondentriesentryoutput) = S ((S (sto_index_weighted_add_secondentries)) * dst_negative_scale_weighted_add_secondentriesentryoutput)) /\ exists ff_q_pvs_weighted_add_secondentriesentryoutputnegative. dst_negative_code_weighted_add_secondentriesentryoutput = ff_q_pvs_weighted_add_secondentriesentryoutputnegative * S ((S (sto_index_weighted_add_secondentries)) * dst_negative_scale_weighted_add_secondentriesentryoutput) + (dst_negative_weighted_add_secondentriesentryoutput))) /\ (exists ge_balance_positive_weighted_add_secondentriesentryoutputvalue ge_balance_negative_weighted_add_secondentriesentryoutputvalue. (((((sto_output_weighted_add_secondentries) = 2 * (ge_balance_positive_weighted_add_secondentriesentryoutputvalue) /\ (ge_balance_negative_weighted_add_secondentriesentryoutputvalue) = 0) \/ exists ge_signed_half_weighted_add_secondentriesentryoutputvaluedecode. (((sto_output_weighted_add_secondentries) = 2 * ge_signed_half_weighted_add_secondentriesentryoutputvaluedecode + 1 /\ (ge_balance_positive_weighted_add_secondentriesentryoutputvalue) = 0) /\ (ge_balance_negative_weighted_add_secondentriesentryoutputvalue) = S ge_signed_half_weighted_add_secondentriesentryoutputvaluedecode))) /\ ((dst_positive_weighted_add_secondentriesentryoutput) + ge_balance_negative_weighted_add_secondentriesentryoutputvalue = (dst_negative_weighted_add_secondentriesentryoutput) + ge_balance_positive_weighted_add_secondentriesentryoutputvalue))))))))) /\ (exists sto_ap_weighted_add_secondentriesentryoperation sto_an_weighted_add_secondentriesentryoperation sto_bp_weighted_add_secondentriesentryoperation sto_bn_weighted_add_secondentriesentryoperation sto_cp_weighted_add_secondentriesentryoperation sto_cn_weighted_add_secondentriesentryoperation. (((((sto_left_weighted_add_secondentries) = 2 * (sto_ap_weighted_add_secondentriesentryoperation) /\ (sto_an_weighted_add_secondentriesentryoperation) = 0) \/ exists ge_signed_half_weighted_add_secondentriesentryoperationleft. (((sto_left_weighted_add_secondentries) = 2 * ge_signed_half_weighted_add_secondentriesentryoperationleft + 1 /\ (sto_ap_weighted_add_secondentriesentryoperation) = 0) /\ (sto_an_weighted_add_secondentriesentryoperation) = S ge_signed_half_weighted_add_secondentriesentryoperationleft))) /\ ((((((sto_right_weighted_add_secondentries) = 2 * (sto_bp_weighted_add_secondentriesentryoperation) /\ (sto_bn_weighted_add_secondentriesentryoperation) = 0) \/ exists ge_signed_half_weighted_add_secondentriesentryoperationright. (((sto_right_weighted_add_secondentries) = 2 * ge_signed_half_weighted_add_secondentriesentryoperationright + 1 /\ (sto_bp_weighted_add_secondentriesentryoperation) = 0) /\ (sto_bn_weighted_add_secondentriesentryoperation) = S ge_signed_half_weighted_add_secondentriesentryoperationright))) /\ ((((((sto_output_weighted_add_secondentries) = 2 * (sto_cp_weighted_add_secondentriesentryoperation) /\ (sto_cn_weighted_add_secondentriesentryoperation) = 0) \/ exists ge_signed_half_weighted_add_secondentriesentryoperationoutput. (((sto_output_weighted_add_secondentries) = 2 * ge_signed_half_weighted_add_secondentriesentryoperationoutput + 1 /\ (sto_cp_weighted_add_secondentriesentryoperation) = 0) /\ (sto_cn_weighted_add_secondentriesentryoperation) = S ge_signed_half_weighted_add_secondentriesentryoperationoutput))) /\ ((sto_ap_weighted_add_secondentriesentryoperation * sto_bp_weighted_add_secondentriesentryoperation + sto_an_weighted_add_secondentriesentryoperation * sto_bn_weighted_add_secondentriesentryoperation) + sto_cn_weighted_add_secondentriesentryoperation = (sto_ap_weighted_add_secondentriesentryoperation * sto_bn_weighted_add_secondentriesentryoperation + sto_an_weighted_add_secondentriesentryoperation * sto_bp_weighted_add_secondentriesentryoperation) + sto_cp_weighted_add_secondentriesentryoperation))))))))))))))))))) -> (((exists dst_positive_code_weighted_add_thirdleft_table dst_positive_scale_weighted_add_thirdleft_table dst_negative_code_weighted_add_thirdleft_table dst_negative_scale_weighted_add_thirdleft_table. (((W) = (((((dst_positive_code_weighted_add_thirdleft_table) + (dst_positive_scale_weighted_add_thirdleft_table)) * S ((dst_positive_code_weighted_add_thirdleft_table) + (dst_positive_scale_weighted_add_thirdleft_table)) + ((dst_positive_scale_weighted_add_thirdleft_table) + (dst_positive_scale_weighted_add_thirdleft_table))) + (((dst_negative_code_weighted_add_thirdleft_table) + (dst_negative_scale_weighted_add_thirdleft_table)) * S ((dst_negative_code_weighted_add_thirdleft_table) + (dst_negative_scale_weighted_add_thirdleft_table)) + ((dst_negative_scale_weighted_add_thirdleft_table) + (dst_negative_scale_weighted_add_thirdleft_table)))) * S ((((dst_positive_code_weighted_add_thirdleft_table) + (dst_positive_scale_weighted_add_thirdleft_table)) * S ((dst_positive_code_weighted_add_thirdleft_table) + (dst_positive_scale_weighted_add_thirdleft_table)) + ((dst_positive_scale_weighted_add_thirdleft_table) + (dst_positive_scale_weighted_add_thirdleft_table))) + (((dst_negative_code_weighted_add_thirdleft_table) + (dst_negative_scale_weighted_add_thirdleft_table)) * S ((dst_negative_code_weighted_add_thirdleft_table) + (dst_negative_scale_weighted_add_thirdleft_table)) + ((dst_negative_scale_weighted_add_thirdleft_table) + (dst_negative_scale_weighted_add_thirdleft_table)))) + ((((dst_negative_code_weighted_add_thirdleft_table) + (dst_negative_scale_weighted_add_thirdleft_table)) * S ((dst_negative_code_weighted_add_thirdleft_table) + (dst_negative_scale_weighted_add_thirdleft_table)) + ((dst_negative_scale_weighted_add_thirdleft_table) + (dst_negative_scale_weighted_add_thirdleft_table))) + (((dst_negative_code_weighted_add_thirdleft_table) + (dst_negative_scale_weighted_add_thirdleft_table)) * S ((dst_negative_code_weighted_add_thirdleft_table) + (dst_negative_scale_weighted_add_thirdleft_table)) + ((dst_negative_scale_weighted_add_thirdleft_table) + (dst_negative_scale_weighted_add_thirdleft_table)))))) /\ (forall dst_index_weighted_add_thirdleft_table. (exists pvs_le_gap_weighted_add_thirdleft_tabledomain. pvs_le_gap_weighted_add_thirdleft_tabledomain + (dst_index_weighted_add_thirdleft_table) = (l)) -> exists dst_positive_weighted_add_thirdleft_table dst_negative_weighted_add_thirdleft_table dst_value_weighted_add_thirdleft_table. ((((exists ff_h_pvs_weighted_add_thirdleft_tableentrypositive. ff_h_pvs_weighted_add_thirdleft_tableentrypositive + S (dst_positive_weighted_add_thirdleft_table) = S ((S (dst_index_weighted_add_thirdleft_table)) * dst_positive_scale_weighted_add_thirdleft_table)) /\ exists ff_q_pvs_weighted_add_thirdleft_tableentrypositive. dst_positive_code_weighted_add_thirdleft_table = ff_q_pvs_weighted_add_thirdleft_tableentrypositive * S ((S (dst_index_weighted_add_thirdleft_table)) * dst_positive_scale_weighted_add_thirdleft_table) + (dst_positive_weighted_add_thirdleft_table))) /\ (((((exists ff_h_pvs_weighted_add_thirdleft_tableentrynegative. ff_h_pvs_weighted_add_thirdleft_tableentrynegative + S (dst_negative_weighted_add_thirdleft_table) = S ((S (dst_index_weighted_add_thirdleft_table)) * dst_negative_scale_weighted_add_thirdleft_table)) /\ exists ff_q_pvs_weighted_add_thirdleft_tableentrynegative. dst_negative_code_weighted_add_thirdleft_table = ff_q_pvs_weighted_add_thirdleft_tableentrynegative * S ((S (dst_index_weighted_add_thirdleft_table)) * dst_negative_scale_weighted_add_thirdleft_table) + (dst_negative_weighted_add_thirdleft_table))) /\ (exists ge_balance_positive_weighted_add_thirdleft_tableentryvalue ge_balance_negative_weighted_add_thirdleft_tableentryvalue. (((((dst_value_weighted_add_thirdleft_table) = 2 * (ge_balance_positive_weighted_add_thirdleft_tableentryvalue) /\ (ge_balance_negative_weighted_add_thirdleft_tableentryvalue) = 0) \/ exists ge_signed_half_weighted_add_thirdleft_tableentryvaluedecode. (((dst_value_weighted_add_thirdleft_table) = 2 * ge_signed_half_weighted_add_thirdleft_tableentryvaluedecode + 1 /\ (ge_balance_positive_weighted_add_thirdleft_tableentryvalue) = 0) /\ (ge_balance_negative_weighted_add_thirdleft_tableentryvalue) = S ge_signed_half_weighted_add_thirdleft_tableentryvaluedecode))) /\ ((dst_positive_weighted_add_thirdleft_table) + ge_balance_negative_weighted_add_thirdleft_tableentryvalue = (dst_negative_weighted_add_thirdleft_table) + ge_balance_positive_weighted_add_thirdleft_tableentryvalue))))))))) /\ (((exists dst_positive_code_weighted_add_thirdright_table dst_positive_scale_weighted_add_thirdright_table dst_negative_code_weighted_add_thirdright_table dst_negative_scale_weighted_add_thirdright_table. (((H) = (((((dst_positive_code_weighted_add_thirdright_table) + (dst_positive_scale_weighted_add_thirdright_table)) * S ((dst_positive_code_weighted_add_thirdright_table) + (dst_positive_scale_weighted_add_thirdright_table)) + ((dst_positive_scale_weighted_add_thirdright_table) + (dst_positive_scale_weighted_add_thirdright_table))) + (((dst_negative_code_weighted_add_thirdright_table) + (dst_negative_scale_weighted_add_thirdright_table)) * S ((dst_negative_code_weighted_add_thirdright_table) + (dst_negative_scale_weighted_add_thirdright_table)) + ((dst_negative_scale_weighted_add_thirdright_table) + (dst_negative_scale_weighted_add_thirdright_table)))) * S ((((dst_positive_code_weighted_add_thirdright_table) + (dst_positive_scale_weighted_add_thirdright_table)) * S ((dst_positive_code_weighted_add_thirdright_table) + (dst_positive_scale_weighted_add_thirdright_table)) + ((dst_positive_scale_weighted_add_thirdright_table) + (dst_positive_scale_weighted_add_thirdright_table))) + (((dst_negative_code_weighted_add_thirdright_table) + (dst_negative_scale_weighted_add_thirdright_table)) * S ((dst_negative_code_weighted_add_thirdright_table) + (dst_negative_scale_weighted_add_thirdright_table)) + ((dst_negative_scale_weighted_add_thirdright_table) + (dst_negative_scale_weighted_add_thirdright_table)))) + ((((dst_negative_code_weighted_add_thirdright_table) + (dst_negative_scale_weighted_add_thirdright_table)) * S ((dst_negative_code_weighted_add_thirdright_table) + (dst_negative_scale_weighted_add_thirdright_table)) + ((dst_negative_scale_weighted_add_thirdright_table) + (dst_negative_scale_weighted_add_thirdright_table))) + (((dst_negative_code_weighted_add_thirdright_table) + (dst_negative_scale_weighted_add_thirdright_table)) * S ((dst_negative_code_weighted_add_thirdright_table) + (dst_negative_scale_weighted_add_thirdright_table)) + ((dst_negative_scale_weighted_add_thirdright_table) + (dst_negative_scale_weighted_add_thirdright_table)))))) /\ (forall dst_index_weighted_add_thirdright_table. (exists pvs_le_gap_weighted_add_thirdright_tabledomain. pvs_le_gap_weighted_add_thirdright_tabledomain + (dst_index_weighted_add_thirdright_table) = (l)) -> exists dst_positive_weighted_add_thirdright_table dst_negative_weighted_add_thirdright_table dst_value_weighted_add_thirdright_table. ((((exists ff_h_pvs_weighted_add_thirdright_tableentrypositive. ff_h_pvs_weighted_add_thirdright_tableentrypositive + S (dst_positive_weighted_add_thirdright_table) = S ((S (dst_index_weighted_add_thirdright_table)) * dst_positive_scale_weighted_add_thirdright_table)) /\ exists ff_q_pvs_weighted_add_thirdright_tableentrypositive. dst_positive_code_weighted_add_thirdright_table = ff_q_pvs_weighted_add_thirdright_tableentrypositive * S ((S (dst_index_weighted_add_thirdright_table)) * dst_positive_scale_weighted_add_thirdright_table) + (dst_positive_weighted_add_thirdright_table))) /\ (((((exists ff_h_pvs_weighted_add_thirdright_tableentrynegative. ff_h_pvs_weighted_add_thirdright_tableentrynegative + S (dst_negative_weighted_add_thirdright_table) = S ((S (dst_index_weighted_add_thirdright_table)) * dst_negative_scale_weighted_add_thirdright_table)) /\ exists ff_q_pvs_weighted_add_thirdright_tableentrynegative. dst_negative_code_weighted_add_thirdright_table = ff_q_pvs_weighted_add_thirdright_tableentrynegative * S ((S (dst_index_weighted_add_thirdright_table)) * dst_negative_scale_weighted_add_thirdright_table) + (dst_negative_weighted_add_thirdright_table))) /\ (exists ge_balance_positive_weighted_add_thirdright_tableentryvalue ge_balance_negative_weighted_add_thirdright_tableentryvalue. (((((dst_value_weighted_add_thirdright_table) = 2 * (ge_balance_positive_weighted_add_thirdright_tableentryvalue) /\ (ge_balance_negative_weighted_add_thirdright_tableentryvalue) = 0) \/ exists ge_signed_half_weighted_add_thirdright_tableentryvaluedecode. (((dst_value_weighted_add_thirdright_table) = 2 * ge_signed_half_weighted_add_thirdright_tableentryvaluedecode + 1 /\ (ge_balance_positive_weighted_add_thirdright_tableentryvalue) = 0) /\ (ge_balance_negative_weighted_add_thirdright_tableentryvalue) = S ge_signed_half_weighted_add_thirdright_tableentryvaluedecode))) /\ ((dst_positive_weighted_add_thirdright_table) + ge_balance_negative_weighted_add_thirdright_tableentryvalue = (dst_negative_weighted_add_thirdright_table) + ge_balance_positive_weighted_add_thirdright_tableentryvalue))))))))) /\ (((exists dst_positive_code_weighted_add_thirdoutput_table dst_positive_scale_weighted_add_thirdoutput_table dst_negative_code_weighted_add_thirdoutput_table dst_negative_scale_weighted_add_thirdoutput_table. (((R) = (((((dst_positive_code_weighted_add_thirdoutput_table) + (dst_positive_scale_weighted_add_thirdoutput_table)) * S ((dst_positive_code_weighted_add_thirdoutput_table) + (dst_positive_scale_weighted_add_thirdoutput_table)) + ((dst_positive_scale_weighted_add_thirdoutput_table) + (dst_positive_scale_weighted_add_thirdoutput_table))) + (((dst_negative_code_weighted_add_thirdoutput_table) + (dst_negative_scale_weighted_add_thirdoutput_table)) * S ((dst_negative_code_weighted_add_thirdoutput_table) + (dst_negative_scale_weighted_add_thirdoutput_table)) + ((dst_negative_scale_weighted_add_thirdoutput_table) + (dst_negative_scale_weighted_add_thirdoutput_table)))) * S ((((dst_positive_code_weighted_add_thirdoutput_table) + (dst_positive_scale_weighted_add_thirdoutput_table)) * S ((dst_positive_code_weighted_add_thirdoutput_table) + (dst_positive_scale_weighted_add_thirdoutput_table)) + ((dst_positive_scale_weighted_add_thirdoutput_table) + (dst_positive_scale_weighted_add_thirdoutput_table))) + (((dst_negative_code_weighted_add_thirdoutput_table) + (dst_negative_scale_weighted_add_thirdoutput_table)) * S ((dst_negative_code_weighted_add_thirdoutput_table) + (dst_negative_scale_weighted_add_thirdoutput_table)) + ((dst_negative_scale_weighted_add_thirdoutput_table) + (dst_negative_scale_weighted_add_thirdoutput_table)))) + ((((dst_negative_code_weighted_add_thirdoutput_table) + (dst_negative_scale_weighted_add_thirdoutput_table)) * S ((dst_negative_code_weighted_add_thirdoutput_table) + (dst_negative_scale_weighted_add_thirdoutput_table)) + ((dst_negative_scale_weighted_add_thirdoutput_table) + (dst_negative_scale_weighted_add_thirdoutput_table))) + (((dst_negative_code_weighted_add_thirdoutput_table) + (dst_negative_scale_weighted_add_thirdoutput_table)) * S ((dst_negative_code_weighted_add_thirdoutput_table) + (dst_negative_scale_weighted_add_thirdoutput_table)) + ((dst_negative_scale_weighted_add_thirdoutput_table) + (dst_negative_scale_weighted_add_thirdoutput_table)))))) /\ (forall dst_index_weighted_add_thirdoutput_table. (exists pvs_le_gap_weighted_add_thirdoutput_tabledomain. pvs_le_gap_weighted_add_thirdoutput_tabledomain + (dst_index_weighted_add_thirdoutput_table) = (l)) -> exists dst_positive_weighted_add_thirdoutput_table dst_negative_weighted_add_thirdoutput_table dst_value_weighted_add_thirdoutput_table. ((((exists ff_h_pvs_weighted_add_thirdoutput_tableentrypositive. ff_h_pvs_weighted_add_thirdoutput_tableentrypositive + S (dst_positive_weighted_add_thirdoutput_table) = S ((S (dst_index_weighted_add_thirdoutput_table)) * dst_positive_scale_weighted_add_thirdoutput_table)) /\ exists ff_q_pvs_weighted_add_thirdoutput_tableentrypositive. dst_positive_code_weighted_add_thirdoutput_table = ff_q_pvs_weighted_add_thirdoutput_tableentrypositive * S ((S (dst_index_weighted_add_thirdoutput_table)) * dst_positive_scale_weighted_add_thirdoutput_table) + (dst_positive_weighted_add_thirdoutput_table))) /\ (((((exists ff_h_pvs_weighted_add_thirdoutput_tableentrynegative. ff_h_pvs_weighted_add_thirdoutput_tableentrynegative + S (dst_negative_weighted_add_thirdoutput_table) = S ((S (dst_index_weighted_add_thirdoutput_table)) * dst_negative_scale_weighted_add_thirdoutput_table)) /\ exists ff_q_pvs_weighted_add_thirdoutput_tableentrynegative. dst_negative_code_weighted_add_thirdoutput_table = ff_q_pvs_weighted_add_thirdoutput_tableentrynegative * S ((S (dst_index_weighted_add_thirdoutput_table)) * dst_negative_scale_weighted_add_thirdoutput_table) + (dst_negative_weighted_add_thirdoutput_table))) /\ (exists ge_balance_positive_weighted_add_thirdoutput_tableentryvalue ge_balance_negative_weighted_add_thirdoutput_tableentryvalue. (((((dst_value_weighted_add_thirdoutput_table) = 2 * (ge_balance_positive_weighted_add_thirdoutput_tableentryvalue) /\ (ge_balance_negative_weighted_add_thirdoutput_tableentryvalue) = 0) \/ exists ge_signed_half_weighted_add_thirdoutput_tableentryvaluedecode. (((dst_value_weighted_add_thirdoutput_table) = 2 * ge_signed_half_weighted_add_thirdoutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_weighted_add_thirdoutput_tableentryvalue) = 0) /\ (ge_balance_negative_weighted_add_thirdoutput_tableentryvalue) = S ge_signed_half_weighted_add_thirdoutput_tableentryvaluedecode))) /\ ((dst_positive_weighted_add_thirdoutput_table) + ge_balance_negative_weighted_add_thirdoutput_tableentryvalue = (dst_negative_weighted_add_thirdoutput_table) + ge_balance_positive_weighted_add_thirdoutput_tableentryvalue))))))))) /\ (forall sto_index_weighted_add_thirdentries. (exists pvs_gap_weighted_add_thirdentriesbound. pvs_gap_weighted_add_thirdentriesbound + S (sto_index_weighted_add_thirdentries) = (l)) -> exists sto_left_weighted_add_thirdentries sto_right_weighted_add_thirdentries sto_output_weighted_add_thirdentries. ((exists dst_positive_code_weighted_add_thirdentriesentryleft dst_positive_scale_weighted_add_thirdentriesentryleft dst_negative_code_weighted_add_thirdentriesentryleft dst_negative_scale_weighted_add_thirdentriesentryleft dst_positive_weighted_add_thirdentriesentryleft dst_negative_weighted_add_thirdentriesentryleft. (((W) = (((((dst_positive_code_weighted_add_thirdentriesentryleft) + (dst_positive_scale_weighted_add_thirdentriesentryleft)) * S ((dst_positive_code_weighted_add_thirdentriesentryleft) + (dst_positive_scale_weighted_add_thirdentriesentryleft)) + ((dst_positive_scale_weighted_add_thirdentriesentryleft) + (dst_positive_scale_weighted_add_thirdentriesentryleft))) + (((dst_negative_code_weighted_add_thirdentriesentryleft) + (dst_negative_scale_weighted_add_thirdentriesentryleft)) * S ((dst_negative_code_weighted_add_thirdentriesentryleft) + (dst_negative_scale_weighted_add_thirdentriesentryleft)) + ((dst_negative_scale_weighted_add_thirdentriesentryleft) + (dst_negative_scale_weighted_add_thirdentriesentryleft)))) * S ((((dst_positive_code_weighted_add_thirdentriesentryleft) + (dst_positive_scale_weighted_add_thirdentriesentryleft)) * S ((dst_positive_code_weighted_add_thirdentriesentryleft) + (dst_positive_scale_weighted_add_thirdentriesentryleft)) + ((dst_positive_scale_weighted_add_thirdentriesentryleft) + (dst_positive_scale_weighted_add_thirdentriesentryleft))) + (((dst_negative_code_weighted_add_thirdentriesentryleft) + (dst_negative_scale_weighted_add_thirdentriesentryleft)) * S ((dst_negative_code_weighted_add_thirdentriesentryleft) + (dst_negative_scale_weighted_add_thirdentriesentryleft)) + ((dst_negative_scale_weighted_add_thirdentriesentryleft) + (dst_negative_scale_weighted_add_thirdentriesentryleft)))) + ((((dst_negative_code_weighted_add_thirdentriesentryleft) + (dst_negative_scale_weighted_add_thirdentriesentryleft)) * S ((dst_negative_code_weighted_add_thirdentriesentryleft) + (dst_negative_scale_weighted_add_thirdentriesentryleft)) + ((dst_negative_scale_weighted_add_thirdentriesentryleft) + (dst_negative_scale_weighted_add_thirdentriesentryleft))) + (((dst_negative_code_weighted_add_thirdentriesentryleft) + (dst_negative_scale_weighted_add_thirdentriesentryleft)) * S ((dst_negative_code_weighted_add_thirdentriesentryleft) + (dst_negative_scale_weighted_add_thirdentriesentryleft)) + ((dst_negative_scale_weighted_add_thirdentriesentryleft) + (dst_negative_scale_weighted_add_thirdentriesentryleft)))))) /\ (((((exists ff_h_pvs_weighted_add_thirdentriesentryleftpositive. ff_h_pvs_weighted_add_thirdentriesentryleftpositive + S (dst_positive_weighted_add_thirdentriesentryleft) = S ((S (sto_index_weighted_add_thirdentries)) * dst_positive_scale_weighted_add_thirdentriesentryleft)) /\ exists ff_q_pvs_weighted_add_thirdentriesentryleftpositive. dst_positive_code_weighted_add_thirdentriesentryleft = ff_q_pvs_weighted_add_thirdentriesentryleftpositive * S ((S (sto_index_weighted_add_thirdentries)) * dst_positive_scale_weighted_add_thirdentriesentryleft) + (dst_positive_weighted_add_thirdentriesentryleft))) /\ (((((exists ff_h_pvs_weighted_add_thirdentriesentryleftnegative. ff_h_pvs_weighted_add_thirdentriesentryleftnegative + S (dst_negative_weighted_add_thirdentriesentryleft) = S ((S (sto_index_weighted_add_thirdentries)) * dst_negative_scale_weighted_add_thirdentriesentryleft)) /\ exists ff_q_pvs_weighted_add_thirdentriesentryleftnegative. dst_negative_code_weighted_add_thirdentriesentryleft = ff_q_pvs_weighted_add_thirdentriesentryleftnegative * S ((S (sto_index_weighted_add_thirdentries)) * dst_negative_scale_weighted_add_thirdentriesentryleft) + (dst_negative_weighted_add_thirdentriesentryleft))) /\ (exists ge_balance_positive_weighted_add_thirdentriesentryleftvalue ge_balance_negative_weighted_add_thirdentriesentryleftvalue. (((((sto_left_weighted_add_thirdentries) = 2 * (ge_balance_positive_weighted_add_thirdentriesentryleftvalue) /\ (ge_balance_negative_weighted_add_thirdentriesentryleftvalue) = 0) \/ exists ge_signed_half_weighted_add_thirdentriesentryleftvaluedecode. (((sto_left_weighted_add_thirdentries) = 2 * ge_signed_half_weighted_add_thirdentriesentryleftvaluedecode + 1 /\ (ge_balance_positive_weighted_add_thirdentriesentryleftvalue) = 0) /\ (ge_balance_negative_weighted_add_thirdentriesentryleftvalue) = S ge_signed_half_weighted_add_thirdentriesentryleftvaluedecode))) /\ ((dst_positive_weighted_add_thirdentriesentryleft) + ge_balance_negative_weighted_add_thirdentriesentryleftvalue = (dst_negative_weighted_add_thirdentriesentryleft) + ge_balance_positive_weighted_add_thirdentriesentryleftvalue))))))))) /\ (((exists dst_positive_code_weighted_add_thirdentriesentryright dst_positive_scale_weighted_add_thirdentriesentryright dst_negative_code_weighted_add_thirdentriesentryright dst_negative_scale_weighted_add_thirdentriesentryright dst_positive_weighted_add_thirdentriesentryright dst_negative_weighted_add_thirdentriesentryright. (((H) = (((((dst_positive_code_weighted_add_thirdentriesentryright) + (dst_positive_scale_weighted_add_thirdentriesentryright)) * S ((dst_positive_code_weighted_add_thirdentriesentryright) + (dst_positive_scale_weighted_add_thirdentriesentryright)) + ((dst_positive_scale_weighted_add_thirdentriesentryright) + (dst_positive_scale_weighted_add_thirdentriesentryright))) + (((dst_negative_code_weighted_add_thirdentriesentryright) + (dst_negative_scale_weighted_add_thirdentriesentryright)) * S ((dst_negative_code_weighted_add_thirdentriesentryright) + (dst_negative_scale_weighted_add_thirdentriesentryright)) + ((dst_negative_scale_weighted_add_thirdentriesentryright) + (dst_negative_scale_weighted_add_thirdentriesentryright)))) * S ((((dst_positive_code_weighted_add_thirdentriesentryright) + (dst_positive_scale_weighted_add_thirdentriesentryright)) * S ((dst_positive_code_weighted_add_thirdentriesentryright) + (dst_positive_scale_weighted_add_thirdentriesentryright)) + ((dst_positive_scale_weighted_add_thirdentriesentryright) + (dst_positive_scale_weighted_add_thirdentriesentryright))) + (((dst_negative_code_weighted_add_thirdentriesentryright) + (dst_negative_scale_weighted_add_thirdentriesentryright)) * S ((dst_negative_code_weighted_add_thirdentriesentryright) + (dst_negative_scale_weighted_add_thirdentriesentryright)) + ((dst_negative_scale_weighted_add_thirdentriesentryright) + (dst_negative_scale_weighted_add_thirdentriesentryright)))) + ((((dst_negative_code_weighted_add_thirdentriesentryright) + (dst_negative_scale_weighted_add_thirdentriesentryright)) * S ((dst_negative_code_weighted_add_thirdentriesentryright) + (dst_negative_scale_weighted_add_thirdentriesentryright)) + ((dst_negative_scale_weighted_add_thirdentriesentryright) + (dst_negative_scale_weighted_add_thirdentriesentryright))) + (((dst_negative_code_weighted_add_thirdentriesentryright) + (dst_negative_scale_weighted_add_thirdentriesentryright)) * S ((dst_negative_code_weighted_add_thirdentriesentryright) + (dst_negative_scale_weighted_add_thirdentriesentryright)) + ((dst_negative_scale_weighted_add_thirdentriesentryright) + (dst_negative_scale_weighted_add_thirdentriesentryright)))))) /\ (((((exists ff_h_pvs_weighted_add_thirdentriesentryrightpositive. ff_h_pvs_weighted_add_thirdentriesentryrightpositive + S (dst_positive_weighted_add_thirdentriesentryright) = S ((S (sto_index_weighted_add_thirdentries)) * dst_positive_scale_weighted_add_thirdentriesentryright)) /\ exists ff_q_pvs_weighted_add_thirdentriesentryrightpositive. dst_positive_code_weighted_add_thirdentriesentryright = ff_q_pvs_weighted_add_thirdentriesentryrightpositive * S ((S (sto_index_weighted_add_thirdentries)) * dst_positive_scale_weighted_add_thirdentriesentryright) + (dst_positive_weighted_add_thirdentriesentryright))) /\ (((((exists ff_h_pvs_weighted_add_thirdentriesentryrightnegative. ff_h_pvs_weighted_add_thirdentriesentryrightnegative + S (dst_negative_weighted_add_thirdentriesentryright) = S ((S (sto_index_weighted_add_thirdentries)) * dst_negative_scale_weighted_add_thirdentriesentryright)) /\ exists ff_q_pvs_weighted_add_thirdentriesentryrightnegative. dst_negative_code_weighted_add_thirdentriesentryright = ff_q_pvs_weighted_add_thirdentriesentryrightnegative * S ((S (sto_index_weighted_add_thirdentries)) * dst_negative_scale_weighted_add_thirdentriesentryright) + (dst_negative_weighted_add_thirdentriesentryright))) /\ (exists ge_balance_positive_weighted_add_thirdentriesentryrightvalue ge_balance_negative_weighted_add_thirdentriesentryrightvalue. (((((sto_right_weighted_add_thirdentries) = 2 * (ge_balance_positive_weighted_add_thirdentriesentryrightvalue) /\ (ge_balance_negative_weighted_add_thirdentriesentryrightvalue) = 0) \/ exists ge_signed_half_weighted_add_thirdentriesentryrightvaluedecode. (((sto_right_weighted_add_thirdentries) = 2 * ge_signed_half_weighted_add_thirdentriesentryrightvaluedecode + 1 /\ (ge_balance_positive_weighted_add_thirdentriesentryrightvalue) = 0) /\ (ge_balance_negative_weighted_add_thirdentriesentryrightvalue) = S ge_signed_half_weighted_add_thirdentriesentryrightvaluedecode))) /\ ((dst_positive_weighted_add_thirdentriesentryright) + ge_balance_negative_weighted_add_thirdentriesentryrightvalue = (dst_negative_weighted_add_thirdentriesentryright) + ge_balance_positive_weighted_add_thirdentriesentryrightvalue))))))))) /\ (((exists dst_positive_code_weighted_add_thirdentriesentryoutput dst_positive_scale_weighted_add_thirdentriesentryoutput dst_negative_code_weighted_add_thirdentriesentryoutput dst_negative_scale_weighted_add_thirdentriesentryoutput dst_positive_weighted_add_thirdentriesentryoutput dst_negative_weighted_add_thirdentriesentryoutput. (((R) = (((((dst_positive_code_weighted_add_thirdentriesentryoutput) + (dst_positive_scale_weighted_add_thirdentriesentryoutput)) * S ((dst_positive_code_weighted_add_thirdentriesentryoutput) + (dst_positive_scale_weighted_add_thirdentriesentryoutput)) + ((dst_positive_scale_weighted_add_thirdentriesentryoutput) + (dst_positive_scale_weighted_add_thirdentriesentryoutput))) + (((dst_negative_code_weighted_add_thirdentriesentryoutput) + (dst_negative_scale_weighted_add_thirdentriesentryoutput)) * S ((dst_negative_code_weighted_add_thirdentriesentryoutput) + (dst_negative_scale_weighted_add_thirdentriesentryoutput)) + ((dst_negative_scale_weighted_add_thirdentriesentryoutput) + (dst_negative_scale_weighted_add_thirdentriesentryoutput)))) * S ((((dst_positive_code_weighted_add_thirdentriesentryoutput) + (dst_positive_scale_weighted_add_thirdentriesentryoutput)) * S ((dst_positive_code_weighted_add_thirdentriesentryoutput) + (dst_positive_scale_weighted_add_thirdentriesentryoutput)) + ((dst_positive_scale_weighted_add_thirdentriesentryoutput) + (dst_positive_scale_weighted_add_thirdentriesentryoutput))) + (((dst_negative_code_weighted_add_thirdentriesentryoutput) + (dst_negative_scale_weighted_add_thirdentriesentryoutput)) * S ((dst_negative_code_weighted_add_thirdentriesentryoutput) + (dst_negative_scale_weighted_add_thirdentriesentryoutput)) + ((dst_negative_scale_weighted_add_thirdentriesentryoutput) + (dst_negative_scale_weighted_add_thirdentriesentryoutput)))) + ((((dst_negative_code_weighted_add_thirdentriesentryoutput) + (dst_negative_scale_weighted_add_thirdentriesentryoutput)) * S ((dst_negative_code_weighted_add_thirdentriesentryoutput) + (dst_negative_scale_weighted_add_thirdentriesentryoutput)) + ((dst_negative_scale_weighted_add_thirdentriesentryoutput) + (dst_negative_scale_weighted_add_thirdentriesentryoutput))) + (((dst_negative_code_weighted_add_thirdentriesentryoutput) + (dst_negative_scale_weighted_add_thirdentriesentryoutput)) * S ((dst_negative_code_weighted_add_thirdentriesentryoutput) + (dst_negative_scale_weighted_add_thirdentriesentryoutput)) + ((dst_negative_scale_weighted_add_thirdentriesentryoutput) + (dst_negative_scale_weighted_add_thirdentriesentryoutput)))))) /\ (((((exists ff_h_pvs_weighted_add_thirdentriesentryoutputpositive. ff_h_pvs_weighted_add_thirdentriesentryoutputpositive + S (dst_positive_weighted_add_thirdentriesentryoutput) = S ((S (sto_index_weighted_add_thirdentries)) * dst_positive_scale_weighted_add_thirdentriesentryoutput)) /\ exists ff_q_pvs_weighted_add_thirdentriesentryoutputpositive. dst_positive_code_weighted_add_thirdentriesentryoutput = ff_q_pvs_weighted_add_thirdentriesentryoutputpositive * S ((S (sto_index_weighted_add_thirdentries)) * dst_positive_scale_weighted_add_thirdentriesentryoutput) + (dst_positive_weighted_add_thirdentriesentryoutput))) /\ (((((exists ff_h_pvs_weighted_add_thirdentriesentryoutputnegative. ff_h_pvs_weighted_add_thirdentriesentryoutputnegative + S (dst_negative_weighted_add_thirdentriesentryoutput) = S ((S (sto_index_weighted_add_thirdentries)) * dst_negative_scale_weighted_add_thirdentriesentryoutput)) /\ exists ff_q_pvs_weighted_add_thirdentriesentryoutputnegative. dst_negative_code_weighted_add_thirdentriesentryoutput = ff_q_pvs_weighted_add_thirdentriesentryoutputnegative * S ((S (sto_index_weighted_add_thirdentries)) * dst_negative_scale_weighted_add_thirdentriesentryoutput) + (dst_negative_weighted_add_thirdentriesentryoutput))) /\ (exists ge_balance_positive_weighted_add_thirdentriesentryoutputvalue ge_balance_negative_weighted_add_thirdentriesentryoutputvalue. (((((sto_output_weighted_add_thirdentries) = 2 * (ge_balance_positive_weighted_add_thirdentriesentryoutputvalue) /\ (ge_balance_negative_weighted_add_thirdentriesentryoutputvalue) = 0) \/ exists ge_signed_half_weighted_add_thirdentriesentryoutputvaluedecode. (((sto_output_weighted_add_thirdentries) = 2 * ge_signed_half_weighted_add_thirdentriesentryoutputvaluedecode + 1 /\ (ge_balance_positive_weighted_add_thirdentriesentryoutputvalue) = 0) /\ (ge_balance_negative_weighted_add_thirdentriesentryoutputvalue) = S ge_signed_half_weighted_add_thirdentriesentryoutputvaluedecode))) /\ ((dst_positive_weighted_add_thirdentriesentryoutput) + ge_balance_negative_weighted_add_thirdentriesentryoutputvalue = (dst_negative_weighted_add_thirdentriesentryoutput) + ge_balance_positive_weighted_add_thirdentriesentryoutputvalue))))))))) /\ (exists sto_ap_weighted_add_thirdentriesentryoperation sto_an_weighted_add_thirdentriesentryoperation sto_bp_weighted_add_thirdentriesentryoperation sto_bn_weighted_add_thirdentriesentryoperation sto_cp_weighted_add_thirdentriesentryoperation sto_cn_weighted_add_thirdentriesentryoperation. (((((sto_left_weighted_add_thirdentries) = 2 * (sto_ap_weighted_add_thirdentriesentryoperation) /\ (sto_an_weighted_add_thirdentriesentryoperation) = 0) \/ exists ge_signed_half_weighted_add_thirdentriesentryoperationleft. (((sto_left_weighted_add_thirdentries) = 2 * ge_signed_half_weighted_add_thirdentriesentryoperationleft + 1 /\ (sto_ap_weighted_add_thirdentriesentryoperation) = 0) /\ (sto_an_weighted_add_thirdentriesentryoperation) = S ge_signed_half_weighted_add_thirdentriesentryoperationleft))) /\ ((((((sto_right_weighted_add_thirdentries) = 2 * (sto_bp_weighted_add_thirdentriesentryoperation) /\ (sto_bn_weighted_add_thirdentriesentryoperation) = 0) \/ exists ge_signed_half_weighted_add_thirdentriesentryoperationright. (((sto_right_weighted_add_thirdentries) = 2 * ge_signed_half_weighted_add_thirdentriesentryoperationright + 1 /\ (sto_bp_weighted_add_thirdentriesentryoperation) = 0) /\ (sto_bn_weighted_add_thirdentriesentryoperation) = S ge_signed_half_weighted_add_thirdentriesentryoperationright))) /\ ((((((sto_output_weighted_add_thirdentries) = 2 * (sto_cp_weighted_add_thirdentriesentryoperation) /\ (sto_cn_weighted_add_thirdentriesentryoperation) = 0) \/ exists ge_signed_half_weighted_add_thirdentriesentryoperationoutput. (((sto_output_weighted_add_thirdentries) = 2 * ge_signed_half_weighted_add_thirdentriesentryoperationoutput + 1 /\ (sto_cp_weighted_add_thirdentriesentryoperation) = 0) /\ (sto_cn_weighted_add_thirdentriesentryoperation) = S ge_signed_half_weighted_add_thirdentriesentryoperationoutput))) /\ ((sto_ap_weighted_add_thirdentriesentryoperation * sto_bp_weighted_add_thirdentriesentryoperation + sto_an_weighted_add_thirdentriesentryoperation * sto_bn_weighted_add_thirdentriesentryoperation) + sto_cn_weighted_add_thirdentriesentryoperation = (sto_ap_weighted_add_thirdentriesentryoperation * sto_bn_weighted_add_thirdentriesentryoperation + sto_an_weighted_add_thirdentriesentryoperation * sto_bp_weighted_add_thirdentriesentryoperation) + sto_cp_weighted_add_thirdentriesentryoperation))))))))))))))))))) -> (((exists dst_positive_code_weighted_add_outputsleft_table dst_positive_scale_weighted_add_outputsleft_table dst_negative_code_weighted_add_outputsleft_table dst_negative_scale_weighted_add_outputsleft_table. (((P) = (((((dst_positive_code_weighted_add_outputsleft_table) + (dst_positive_scale_weighted_add_outputsleft_table)) * S ((dst_positive_code_weighted_add_outputsleft_table) + (dst_positive_scale_weighted_add_outputsleft_table)) + ((dst_positive_scale_weighted_add_outputsleft_table) + (dst_positive_scale_weighted_add_outputsleft_table))) + (((dst_negative_code_weighted_add_outputsleft_table) + (dst_negative_scale_weighted_add_outputsleft_table)) * S ((dst_negative_code_weighted_add_outputsleft_table) + (dst_negative_scale_weighted_add_outputsleft_table)) + ((dst_negative_scale_weighted_add_outputsleft_table) + (dst_negative_scale_weighted_add_outputsleft_table)))) * S ((((dst_positive_code_weighted_add_outputsleft_table) + (dst_positive_scale_weighted_add_outputsleft_table)) * S ((dst_positive_code_weighted_add_outputsleft_table) + (dst_positive_scale_weighted_add_outputsleft_table)) + ((dst_positive_scale_weighted_add_outputsleft_table) + (dst_positive_scale_weighted_add_outputsleft_table))) + (((dst_negative_code_weighted_add_outputsleft_table) + (dst_negative_scale_weighted_add_outputsleft_table)) * S ((dst_negative_code_weighted_add_outputsleft_table) + (dst_negative_scale_weighted_add_outputsleft_table)) + ((dst_negative_scale_weighted_add_outputsleft_table) + (dst_negative_scale_weighted_add_outputsleft_table)))) + ((((dst_negative_code_weighted_add_outputsleft_table) + (dst_negative_scale_weighted_add_outputsleft_table)) * S ((dst_negative_code_weighted_add_outputsleft_table) + (dst_negative_scale_weighted_add_outputsleft_table)) + ((dst_negative_scale_weighted_add_outputsleft_table) + (dst_negative_scale_weighted_add_outputsleft_table))) + (((dst_negative_code_weighted_add_outputsleft_table) + (dst_negative_scale_weighted_add_outputsleft_table)) * S ((dst_negative_code_weighted_add_outputsleft_table) + (dst_negative_scale_weighted_add_outputsleft_table)) + ((dst_negative_scale_weighted_add_outputsleft_table) + (dst_negative_scale_weighted_add_outputsleft_table)))))) /\ (forall dst_index_weighted_add_outputsleft_table. (exists pvs_le_gap_weighted_add_outputsleft_tabledomain. pvs_le_gap_weighted_add_outputsleft_tabledomain + (dst_index_weighted_add_outputsleft_table) = (l)) -> exists dst_positive_weighted_add_outputsleft_table dst_negative_weighted_add_outputsleft_table dst_value_weighted_add_outputsleft_table. ((((exists ff_h_pvs_weighted_add_outputsleft_tableentrypositive. ff_h_pvs_weighted_add_outputsleft_tableentrypositive + S (dst_positive_weighted_add_outputsleft_table) = S ((S (dst_index_weighted_add_outputsleft_table)) * dst_positive_scale_weighted_add_outputsleft_table)) /\ exists ff_q_pvs_weighted_add_outputsleft_tableentrypositive. dst_positive_code_weighted_add_outputsleft_table = ff_q_pvs_weighted_add_outputsleft_tableentrypositive * S ((S (dst_index_weighted_add_outputsleft_table)) * dst_positive_scale_weighted_add_outputsleft_table) + (dst_positive_weighted_add_outputsleft_table))) /\ (((((exists ff_h_pvs_weighted_add_outputsleft_tableentrynegative. ff_h_pvs_weighted_add_outputsleft_tableentrynegative + S (dst_negative_weighted_add_outputsleft_table) = S ((S (dst_index_weighted_add_outputsleft_table)) * dst_negative_scale_weighted_add_outputsleft_table)) /\ exists ff_q_pvs_weighted_add_outputsleft_tableentrynegative. dst_negative_code_weighted_add_outputsleft_table = ff_q_pvs_weighted_add_outputsleft_tableentrynegative * S ((S (dst_index_weighted_add_outputsleft_table)) * dst_negative_scale_weighted_add_outputsleft_table) + (dst_negative_weighted_add_outputsleft_table))) /\ (exists ge_balance_positive_weighted_add_outputsleft_tableentryvalue ge_balance_negative_weighted_add_outputsleft_tableentryvalue. (((((dst_value_weighted_add_outputsleft_table) = 2 * (ge_balance_positive_weighted_add_outputsleft_tableentryvalue) /\ (ge_balance_negative_weighted_add_outputsleft_tableentryvalue) = 0) \/ exists ge_signed_half_weighted_add_outputsleft_tableentryvaluedecode. (((dst_value_weighted_add_outputsleft_table) = 2 * ge_signed_half_weighted_add_outputsleft_tableentryvaluedecode + 1 /\ (ge_balance_positive_weighted_add_outputsleft_tableentryvalue) = 0) /\ (ge_balance_negative_weighted_add_outputsleft_tableentryvalue) = S ge_signed_half_weighted_add_outputsleft_tableentryvaluedecode))) /\ ((dst_positive_weighted_add_outputsleft_table) + ge_balance_negative_weighted_add_outputsleft_tableentryvalue = (dst_negative_weighted_add_outputsleft_table) + ge_balance_positive_weighted_add_outputsleft_tableentryvalue))))))))) /\ (((exists dst_positive_code_weighted_add_outputsright_table dst_positive_scale_weighted_add_outputsright_table dst_negative_code_weighted_add_outputsright_table dst_negative_scale_weighted_add_outputsright_table. (((Q) = (((((dst_positive_code_weighted_add_outputsright_table) + (dst_positive_scale_weighted_add_outputsright_table)) * S ((dst_positive_code_weighted_add_outputsright_table) + (dst_positive_scale_weighted_add_outputsright_table)) + ((dst_positive_scale_weighted_add_outputsright_table) + (dst_positive_scale_weighted_add_outputsright_table))) + (((dst_negative_code_weighted_add_outputsright_table) + (dst_negative_scale_weighted_add_outputsright_table)) * S ((dst_negative_code_weighted_add_outputsright_table) + (dst_negative_scale_weighted_add_outputsright_table)) + ((dst_negative_scale_weighted_add_outputsright_table) + (dst_negative_scale_weighted_add_outputsright_table)))) * S ((((dst_positive_code_weighted_add_outputsright_table) + (dst_positive_scale_weighted_add_outputsright_table)) * S ((dst_positive_code_weighted_add_outputsright_table) + (dst_positive_scale_weighted_add_outputsright_table)) + ((dst_positive_scale_weighted_add_outputsright_table) + (dst_positive_scale_weighted_add_outputsright_table))) + (((dst_negative_code_weighted_add_outputsright_table) + (dst_negative_scale_weighted_add_outputsright_table)) * S ((dst_negative_code_weighted_add_outputsright_table) + (dst_negative_scale_weighted_add_outputsright_table)) + ((dst_negative_scale_weighted_add_outputsright_table) + (dst_negative_scale_weighted_add_outputsright_table)))) + ((((dst_negative_code_weighted_add_outputsright_table) + (dst_negative_scale_weighted_add_outputsright_table)) * S ((dst_negative_code_weighted_add_outputsright_table) + (dst_negative_scale_weighted_add_outputsright_table)) + ((dst_negative_scale_weighted_add_outputsright_table) + (dst_negative_scale_weighted_add_outputsright_table))) + (((dst_negative_code_weighted_add_outputsright_table) + (dst_negative_scale_weighted_add_outputsright_table)) * S ((dst_negative_code_weighted_add_outputsright_table) + (dst_negative_scale_weighted_add_outputsright_table)) + ((dst_negative_scale_weighted_add_outputsright_table) + (dst_negative_scale_weighted_add_outputsright_table)))))) /\ (forall dst_index_weighted_add_outputsright_table. (exists pvs_le_gap_weighted_add_outputsright_tabledomain. pvs_le_gap_weighted_add_outputsright_tabledomain + (dst_index_weighted_add_outputsright_table) = (l)) -> exists dst_positive_weighted_add_outputsright_table dst_negative_weighted_add_outputsright_table dst_value_weighted_add_outputsright_table. ((((exists ff_h_pvs_weighted_add_outputsright_tableentrypositive. ff_h_pvs_weighted_add_outputsright_tableentrypositive + S (dst_positive_weighted_add_outputsright_table) = S ((S (dst_index_weighted_add_outputsright_table)) * dst_positive_scale_weighted_add_outputsright_table)) /\ exists ff_q_pvs_weighted_add_outputsright_tableentrypositive. dst_positive_code_weighted_add_outputsright_table = ff_q_pvs_weighted_add_outputsright_tableentrypositive * S ((S (dst_index_weighted_add_outputsright_table)) * dst_positive_scale_weighted_add_outputsright_table) + (dst_positive_weighted_add_outputsright_table))) /\ (((((exists ff_h_pvs_weighted_add_outputsright_tableentrynegative. ff_h_pvs_weighted_add_outputsright_tableentrynegative + S (dst_negative_weighted_add_outputsright_table) = S ((S (dst_index_weighted_add_outputsright_table)) * dst_negative_scale_weighted_add_outputsright_table)) /\ exists ff_q_pvs_weighted_add_outputsright_tableentrynegative. dst_negative_code_weighted_add_outputsright_table = ff_q_pvs_weighted_add_outputsright_tableentrynegative * S ((S (dst_index_weighted_add_outputsright_table)) * dst_negative_scale_weighted_add_outputsright_table) + (dst_negative_weighted_add_outputsright_table))) /\ (exists ge_balance_positive_weighted_add_outputsright_tableentryvalue ge_balance_negative_weighted_add_outputsright_tableentryvalue. (((((dst_value_weighted_add_outputsright_table) = 2 * (ge_balance_positive_weighted_add_outputsright_tableentryvalue) /\ (ge_balance_negative_weighted_add_outputsright_tableentryvalue) = 0) \/ exists ge_signed_half_weighted_add_outputsright_tableentryvaluedecode. (((dst_value_weighted_add_outputsright_table) = 2 * ge_signed_half_weighted_add_outputsright_tableentryvaluedecode + 1 /\ (ge_balance_positive_weighted_add_outputsright_tableentryvalue) = 0) /\ (ge_balance_negative_weighted_add_outputsright_tableentryvalue) = S ge_signed_half_weighted_add_outputsright_tableentryvaluedecode))) /\ ((dst_positive_weighted_add_outputsright_table) + ge_balance_negative_weighted_add_outputsright_tableentryvalue = (dst_negative_weighted_add_outputsright_table) + ge_balance_positive_weighted_add_outputsright_tableentryvalue))))))))) /\ (((exists dst_positive_code_weighted_add_outputsoutput_table dst_positive_scale_weighted_add_outputsoutput_table dst_negative_code_weighted_add_outputsoutput_table dst_negative_scale_weighted_add_outputsoutput_table. (((R) = (((((dst_positive_code_weighted_add_outputsoutput_table) + (dst_positive_scale_weighted_add_outputsoutput_table)) * S ((dst_positive_code_weighted_add_outputsoutput_table) + (dst_positive_scale_weighted_add_outputsoutput_table)) + ((dst_positive_scale_weighted_add_outputsoutput_table) + (dst_positive_scale_weighted_add_outputsoutput_table))) + (((dst_negative_code_weighted_add_outputsoutput_table) + (dst_negative_scale_weighted_add_outputsoutput_table)) * S ((dst_negative_code_weighted_add_outputsoutput_table) + (dst_negative_scale_weighted_add_outputsoutput_table)) + ((dst_negative_scale_weighted_add_outputsoutput_table) + (dst_negative_scale_weighted_add_outputsoutput_table)))) * S ((((dst_positive_code_weighted_add_outputsoutput_table) + (dst_positive_scale_weighted_add_outputsoutput_table)) * S ((dst_positive_code_weighted_add_outputsoutput_table) + (dst_positive_scale_weighted_add_outputsoutput_table)) + ((dst_positive_scale_weighted_add_outputsoutput_table) + (dst_positive_scale_weighted_add_outputsoutput_table))) + (((dst_negative_code_weighted_add_outputsoutput_table) + (dst_negative_scale_weighted_add_outputsoutput_table)) * S ((dst_negative_code_weighted_add_outputsoutput_table) + (dst_negative_scale_weighted_add_outputsoutput_table)) + ((dst_negative_scale_weighted_add_outputsoutput_table) + (dst_negative_scale_weighted_add_outputsoutput_table)))) + ((((dst_negative_code_weighted_add_outputsoutput_table) + (dst_negative_scale_weighted_add_outputsoutput_table)) * S ((dst_negative_code_weighted_add_outputsoutput_table) + (dst_negative_scale_weighted_add_outputsoutput_table)) + ((dst_negative_scale_weighted_add_outputsoutput_table) + (dst_negative_scale_weighted_add_outputsoutput_table))) + (((dst_negative_code_weighted_add_outputsoutput_table) + (dst_negative_scale_weighted_add_outputsoutput_table)) * S ((dst_negative_code_weighted_add_outputsoutput_table) + (dst_negative_scale_weighted_add_outputsoutput_table)) + ((dst_negative_scale_weighted_add_outputsoutput_table) + (dst_negative_scale_weighted_add_outputsoutput_table)))))) /\ (forall dst_index_weighted_add_outputsoutput_table. (exists pvs_le_gap_weighted_add_outputsoutput_tabledomain. pvs_le_gap_weighted_add_outputsoutput_tabledomain + (dst_index_weighted_add_outputsoutput_table) = (l)) -> exists dst_positive_weighted_add_outputsoutput_table dst_negative_weighted_add_outputsoutput_table dst_value_weighted_add_outputsoutput_table. ((((exists ff_h_pvs_weighted_add_outputsoutput_tableentrypositive. ff_h_pvs_weighted_add_outputsoutput_tableentrypositive + S (dst_positive_weighted_add_outputsoutput_table) = S ((S (dst_index_weighted_add_outputsoutput_table)) * dst_positive_scale_weighted_add_outputsoutput_table)) /\ exists ff_q_pvs_weighted_add_outputsoutput_tableentrypositive. dst_positive_code_weighted_add_outputsoutput_table = ff_q_pvs_weighted_add_outputsoutput_tableentrypositive * S ((S (dst_index_weighted_add_outputsoutput_table)) * dst_positive_scale_weighted_add_outputsoutput_table) + (dst_positive_weighted_add_outputsoutput_table))) /\ (((((exists ff_h_pvs_weighted_add_outputsoutput_tableentrynegative. ff_h_pvs_weighted_add_outputsoutput_tableentrynegative + S (dst_negative_weighted_add_outputsoutput_table) = S ((S (dst_index_weighted_add_outputsoutput_table)) * dst_negative_scale_weighted_add_outputsoutput_table)) /\ exists ff_q_pvs_weighted_add_outputsoutput_tableentrynegative. dst_negative_code_weighted_add_outputsoutput_table = ff_q_pvs_weighted_add_outputsoutput_tableentrynegative * S ((S (dst_index_weighted_add_outputsoutput_table)) * dst_negative_scale_weighted_add_outputsoutput_table) + (dst_negative_weighted_add_outputsoutput_table))) /\ (exists ge_balance_positive_weighted_add_outputsoutput_tableentryvalue ge_balance_negative_weighted_add_outputsoutput_tableentryvalue. (((((dst_value_weighted_add_outputsoutput_table) = 2 * (ge_balance_positive_weighted_add_outputsoutput_tableentryvalue) /\ (ge_balance_negative_weighted_add_outputsoutput_tableentryvalue) = 0) \/ exists ge_signed_half_weighted_add_outputsoutput_tableentryvaluedecode. (((dst_value_weighted_add_outputsoutput_table) = 2 * ge_signed_half_weighted_add_outputsoutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_weighted_add_outputsoutput_tableentryvalue) = 0) /\ (ge_balance_negative_weighted_add_outputsoutput_tableentryvalue) = S ge_signed_half_weighted_add_outputsoutput_tableentryvaluedecode))) /\ ((dst_positive_weighted_add_outputsoutput_table) + ge_balance_negative_weighted_add_outputsoutput_tableentryvalue = (dst_negative_weighted_add_outputsoutput_table) + ge_balance_positive_weighted_add_outputsoutput_tableentryvalue))))))))) /\ (forall sto_index_weighted_add_outputsentries. (exists pvs_gap_weighted_add_outputsentriesbound. pvs_gap_weighted_add_outputsentriesbound + S (sto_index_weighted_add_outputsentries) = (l)) -> exists sto_left_weighted_add_outputsentries sto_right_weighted_add_outputsentries sto_output_weighted_add_outputsentries. ((exists dst_positive_code_weighted_add_outputsentriesentryleft dst_positive_scale_weighted_add_outputsentriesentryleft dst_negative_code_weighted_add_outputsentriesentryleft dst_negative_scale_weighted_add_outputsentriesentryleft dst_positive_weighted_add_outputsentriesentryleft dst_negative_weighted_add_outputsentriesentryleft. (((P) = (((((dst_positive_code_weighted_add_outputsentriesentryleft) + (dst_positive_scale_weighted_add_outputsentriesentryleft)) * S ((dst_positive_code_weighted_add_outputsentriesentryleft) + (dst_positive_scale_weighted_add_outputsentriesentryleft)) + ((dst_positive_scale_weighted_add_outputsentriesentryleft) + (dst_positive_scale_weighted_add_outputsentriesentryleft))) + (((dst_negative_code_weighted_add_outputsentriesentryleft) + (dst_negative_scale_weighted_add_outputsentriesentryleft)) * S ((dst_negative_code_weighted_add_outputsentriesentryleft) + (dst_negative_scale_weighted_add_outputsentriesentryleft)) + ((dst_negative_scale_weighted_add_outputsentriesentryleft) + (dst_negative_scale_weighted_add_outputsentriesentryleft)))) * S ((((dst_positive_code_weighted_add_outputsentriesentryleft) + (dst_positive_scale_weighted_add_outputsentriesentryleft)) * S ((dst_positive_code_weighted_add_outputsentriesentryleft) + (dst_positive_scale_weighted_add_outputsentriesentryleft)) + ((dst_positive_scale_weighted_add_outputsentriesentryleft) + (dst_positive_scale_weighted_add_outputsentriesentryleft))) + (((dst_negative_code_weighted_add_outputsentriesentryleft) + (dst_negative_scale_weighted_add_outputsentriesentryleft)) * S ((dst_negative_code_weighted_add_outputsentriesentryleft) + (dst_negative_scale_weighted_add_outputsentriesentryleft)) + ((dst_negative_scale_weighted_add_outputsentriesentryleft) + (dst_negative_scale_weighted_add_outputsentriesentryleft)))) + ((((dst_negative_code_weighted_add_outputsentriesentryleft) + (dst_negative_scale_weighted_add_outputsentriesentryleft)) * S ((dst_negative_code_weighted_add_outputsentriesentryleft) + (dst_negative_scale_weighted_add_outputsentriesentryleft)) + ((dst_negative_scale_weighted_add_outputsentriesentryleft) + (dst_negative_scale_weighted_add_outputsentriesentryleft))) + (((dst_negative_code_weighted_add_outputsentriesentryleft) + (dst_negative_scale_weighted_add_outputsentriesentryleft)) * S ((dst_negative_code_weighted_add_outputsentriesentryleft) + (dst_negative_scale_weighted_add_outputsentriesentryleft)) + ((dst_negative_scale_weighted_add_outputsentriesentryleft) + (dst_negative_scale_weighted_add_outputsentriesentryleft)))))) /\ (((((exists ff_h_pvs_weighted_add_outputsentriesentryleftpositive. ff_h_pvs_weighted_add_outputsentriesentryleftpositive + S (dst_positive_weighted_add_outputsentriesentryleft) = S ((S (sto_index_weighted_add_outputsentries)) * dst_positive_scale_weighted_add_outputsentriesentryleft)) /\ exists ff_q_pvs_weighted_add_outputsentriesentryleftpositive. dst_positive_code_weighted_add_outputsentriesentryleft = ff_q_pvs_weighted_add_outputsentriesentryleftpositive * S ((S (sto_index_weighted_add_outputsentries)) * dst_positive_scale_weighted_add_outputsentriesentryleft) + (dst_positive_weighted_add_outputsentriesentryleft))) /\ (((((exists ff_h_pvs_weighted_add_outputsentriesentryleftnegative. ff_h_pvs_weighted_add_outputsentriesentryleftnegative + S (dst_negative_weighted_add_outputsentriesentryleft) = S ((S (sto_index_weighted_add_outputsentries)) * dst_negative_scale_weighted_add_outputsentriesentryleft)) /\ exists ff_q_pvs_weighted_add_outputsentriesentryleftnegative. dst_negative_code_weighted_add_outputsentriesentryleft = ff_q_pvs_weighted_add_outputsentriesentryleftnegative * S ((S (sto_index_weighted_add_outputsentries)) * dst_negative_scale_weighted_add_outputsentriesentryleft) + (dst_negative_weighted_add_outputsentriesentryleft))) /\ (exists ge_balance_positive_weighted_add_outputsentriesentryleftvalue ge_balance_negative_weighted_add_outputsentriesentryleftvalue. (((((sto_left_weighted_add_outputsentries) = 2 * (ge_balance_positive_weighted_add_outputsentriesentryleftvalue) /\ (ge_balance_negative_weighted_add_outputsentriesentryleftvalue) = 0) \/ exists ge_signed_half_weighted_add_outputsentriesentryleftvaluedecode. (((sto_left_weighted_add_outputsentries) = 2 * ge_signed_half_weighted_add_outputsentriesentryleftvaluedecode + 1 /\ (ge_balance_positive_weighted_add_outputsentriesentryleftvalue) = 0) /\ (ge_balance_negative_weighted_add_outputsentriesentryleftvalue) = S ge_signed_half_weighted_add_outputsentriesentryleftvaluedecode))) /\ ((dst_positive_weighted_add_outputsentriesentryleft) + ge_balance_negative_weighted_add_outputsentriesentryleftvalue = (dst_negative_weighted_add_outputsentriesentryleft) + ge_balance_positive_weighted_add_outputsentriesentryleftvalue))))))))) /\ (((exists dst_positive_code_weighted_add_outputsentriesentryright dst_positive_scale_weighted_add_outputsentriesentryright dst_negative_code_weighted_add_outputsentriesentryright dst_negative_scale_weighted_add_outputsentriesentryright dst_positive_weighted_add_outputsentriesentryright dst_negative_weighted_add_outputsentriesentryright. (((Q) = (((((dst_positive_code_weighted_add_outputsentriesentryright) + (dst_positive_scale_weighted_add_outputsentriesentryright)) * S ((dst_positive_code_weighted_add_outputsentriesentryright) + (dst_positive_scale_weighted_add_outputsentriesentryright)) + ((dst_positive_scale_weighted_add_outputsentriesentryright) + (dst_positive_scale_weighted_add_outputsentriesentryright))) + (((dst_negative_code_weighted_add_outputsentriesentryright) + (dst_negative_scale_weighted_add_outputsentriesentryright)) * S ((dst_negative_code_weighted_add_outputsentriesentryright) + (dst_negative_scale_weighted_add_outputsentriesentryright)) + ((dst_negative_scale_weighted_add_outputsentriesentryright) + (dst_negative_scale_weighted_add_outputsentriesentryright)))) * S ((((dst_positive_code_weighted_add_outputsentriesentryright) + (dst_positive_scale_weighted_add_outputsentriesentryright)) * S ((dst_positive_code_weighted_add_outputsentriesentryright) + (dst_positive_scale_weighted_add_outputsentriesentryright)) + ((dst_positive_scale_weighted_add_outputsentriesentryright) + (dst_positive_scale_weighted_add_outputsentriesentryright))) + (((dst_negative_code_weighted_add_outputsentriesentryright) + (dst_negative_scale_weighted_add_outputsentriesentryright)) * S ((dst_negative_code_weighted_add_outputsentriesentryright) + (dst_negative_scale_weighted_add_outputsentriesentryright)) + ((dst_negative_scale_weighted_add_outputsentriesentryright) + (dst_negative_scale_weighted_add_outputsentriesentryright)))) + ((((dst_negative_code_weighted_add_outputsentriesentryright) + (dst_negative_scale_weighted_add_outputsentriesentryright)) * S ((dst_negative_code_weighted_add_outputsentriesentryright) + (dst_negative_scale_weighted_add_outputsentriesentryright)) + ((dst_negative_scale_weighted_add_outputsentriesentryright) + (dst_negative_scale_weighted_add_outputsentriesentryright))) + (((dst_negative_code_weighted_add_outputsentriesentryright) + (dst_negative_scale_weighted_add_outputsentriesentryright)) * S ((dst_negative_code_weighted_add_outputsentriesentryright) + (dst_negative_scale_weighted_add_outputsentriesentryright)) + ((dst_negative_scale_weighted_add_outputsentriesentryright) + (dst_negative_scale_weighted_add_outputsentriesentryright)))))) /\ (((((exists ff_h_pvs_weighted_add_outputsentriesentryrightpositive. ff_h_pvs_weighted_add_outputsentriesentryrightpositive + S (dst_positive_weighted_add_outputsentriesentryright) = S ((S (sto_index_weighted_add_outputsentries)) * dst_positive_scale_weighted_add_outputsentriesentryright)) /\ exists ff_q_pvs_weighted_add_outputsentriesentryrightpositive. dst_positive_code_weighted_add_outputsentriesentryright = ff_q_pvs_weighted_add_outputsentriesentryrightpositive * S ((S (sto_index_weighted_add_outputsentries)) * dst_positive_scale_weighted_add_outputsentriesentryright) + (dst_positive_weighted_add_outputsentriesentryright))) /\ (((((exists ff_h_pvs_weighted_add_outputsentriesentryrightnegative. ff_h_pvs_weighted_add_outputsentriesentryrightnegative + S (dst_negative_weighted_add_outputsentriesentryright) = S ((S (sto_index_weighted_add_outputsentries)) * dst_negative_scale_weighted_add_outputsentriesentryright)) /\ exists ff_q_pvs_weighted_add_outputsentriesentryrightnegative. dst_negative_code_weighted_add_outputsentriesentryright = ff_q_pvs_weighted_add_outputsentriesentryrightnegative * S ((S (sto_index_weighted_add_outputsentries)) * dst_negative_scale_weighted_add_outputsentriesentryright) + (dst_negative_weighted_add_outputsentriesentryright))) /\ (exists ge_balance_positive_weighted_add_outputsentriesentryrightvalue ge_balance_negative_weighted_add_outputsentriesentryrightvalue. (((((sto_right_weighted_add_outputsentries) = 2 * (ge_balance_positive_weighted_add_outputsentriesentryrightvalue) /\ (ge_balance_negative_weighted_add_outputsentriesentryrightvalue) = 0) \/ exists ge_signed_half_weighted_add_outputsentriesentryrightvaluedecode. (((sto_right_weighted_add_outputsentries) = 2 * ge_signed_half_weighted_add_outputsentriesentryrightvaluedecode + 1 /\ (ge_balance_positive_weighted_add_outputsentriesentryrightvalue) = 0) /\ (ge_balance_negative_weighted_add_outputsentriesentryrightvalue) = S ge_signed_half_weighted_add_outputsentriesentryrightvaluedecode))) /\ ((dst_positive_weighted_add_outputsentriesentryright) + ge_balance_negative_weighted_add_outputsentriesentryrightvalue = (dst_negative_weighted_add_outputsentriesentryright) + ge_balance_positive_weighted_add_outputsentriesentryrightvalue))))))))) /\ (((exists dst_positive_code_weighted_add_outputsentriesentryoutput dst_positive_scale_weighted_add_outputsentriesentryoutput dst_negative_code_weighted_add_outputsentriesentryoutput dst_negative_scale_weighted_add_outputsentriesentryoutput dst_positive_weighted_add_outputsentriesentryoutput dst_negative_weighted_add_outputsentriesentryoutput. (((R) = (((((dst_positive_code_weighted_add_outputsentriesentryoutput) + (dst_positive_scale_weighted_add_outputsentriesentryoutput)) * S ((dst_positive_code_weighted_add_outputsentriesentryoutput) + (dst_positive_scale_weighted_add_outputsentriesentryoutput)) + ((dst_positive_scale_weighted_add_outputsentriesentryoutput) + (dst_positive_scale_weighted_add_outputsentriesentryoutput))) + (((dst_negative_code_weighted_add_outputsentriesentryoutput) + (dst_negative_scale_weighted_add_outputsentriesentryoutput)) * S ((dst_negative_code_weighted_add_outputsentriesentryoutput) + (dst_negative_scale_weighted_add_outputsentriesentryoutput)) + ((dst_negative_scale_weighted_add_outputsentriesentryoutput) + (dst_negative_scale_weighted_add_outputsentriesentryoutput)))) * S ((((dst_positive_code_weighted_add_outputsentriesentryoutput) + (dst_positive_scale_weighted_add_outputsentriesentryoutput)) * S ((dst_positive_code_weighted_add_outputsentriesentryoutput) + (dst_positive_scale_weighted_add_outputsentriesentryoutput)) + ((dst_positive_scale_weighted_add_outputsentriesentryoutput) + (dst_positive_scale_weighted_add_outputsentriesentryoutput))) + (((dst_negative_code_weighted_add_outputsentriesentryoutput) + (dst_negative_scale_weighted_add_outputsentriesentryoutput)) * S ((dst_negative_code_weighted_add_outputsentriesentryoutput) + (dst_negative_scale_weighted_add_outputsentriesentryoutput)) + ((dst_negative_scale_weighted_add_outputsentriesentryoutput) + (dst_negative_scale_weighted_add_outputsentriesentryoutput)))) + ((((dst_negative_code_weighted_add_outputsentriesentryoutput) + (dst_negative_scale_weighted_add_outputsentriesentryoutput)) * S ((dst_negative_code_weighted_add_outputsentriesentryoutput) + (dst_negative_scale_weighted_add_outputsentriesentryoutput)) + ((dst_negative_scale_weighted_add_outputsentriesentryoutput) + (dst_negative_scale_weighted_add_outputsentriesentryoutput))) + (((dst_negative_code_weighted_add_outputsentriesentryoutput) + (dst_negative_scale_weighted_add_outputsentriesentryoutput)) * S ((dst_negative_code_weighted_add_outputsentriesentryoutput) + (dst_negative_scale_weighted_add_outputsentriesentryoutput)) + ((dst_negative_scale_weighted_add_outputsentriesentryoutput) + (dst_negative_scale_weighted_add_outputsentriesentryoutput)))))) /\ (((((exists ff_h_pvs_weighted_add_outputsentriesentryoutputpositive. ff_h_pvs_weighted_add_outputsentriesentryoutputpositive + S (dst_positive_weighted_add_outputsentriesentryoutput) = S ((S (sto_index_weighted_add_outputsentries)) * dst_positive_scale_weighted_add_outputsentriesentryoutput)) /\ exists ff_q_pvs_weighted_add_outputsentriesentryoutputpositive. dst_positive_code_weighted_add_outputsentriesentryoutput = ff_q_pvs_weighted_add_outputsentriesentryoutputpositive * S ((S (sto_index_weighted_add_outputsentries)) * dst_positive_scale_weighted_add_outputsentriesentryoutput) + (dst_positive_weighted_add_outputsentriesentryoutput))) /\ (((((exists ff_h_pvs_weighted_add_outputsentriesentryoutputnegative. ff_h_pvs_weighted_add_outputsentriesentryoutputnegative + S (dst_negative_weighted_add_outputsentriesentryoutput) = S ((S (sto_index_weighted_add_outputsentries)) * dst_negative_scale_weighted_add_outputsentriesentryoutput)) /\ exists ff_q_pvs_weighted_add_outputsentriesentryoutputnegative. dst_negative_code_weighted_add_outputsentriesentryoutput = ff_q_pvs_weighted_add_outputsentriesentryoutputnegative * S ((S (sto_index_weighted_add_outputsentries)) * dst_negative_scale_weighted_add_outputsentriesentryoutput) + (dst_negative_weighted_add_outputsentriesentryoutput))) /\ (exists ge_balance_positive_weighted_add_outputsentriesentryoutputvalue ge_balance_negative_weighted_add_outputsentriesentryoutputvalue. (((((sto_output_weighted_add_outputsentries) = 2 * (ge_balance_positive_weighted_add_outputsentriesentryoutputvalue) /\ (ge_balance_negative_weighted_add_outputsentriesentryoutputvalue) = 0) \/ exists ge_signed_half_weighted_add_outputsentriesentryoutputvaluedecode. (((sto_output_weighted_add_outputsentries) = 2 * ge_signed_half_weighted_add_outputsentriesentryoutputvaluedecode + 1 /\ (ge_balance_positive_weighted_add_outputsentriesentryoutputvalue) = 0) /\ (ge_balance_negative_weighted_add_outputsentriesentryoutputvalue) = S ge_signed_half_weighted_add_outputsentriesentryoutputvaluedecode))) /\ ((dst_positive_weighted_add_outputsentriesentryoutput) + ge_balance_negative_weighted_add_outputsentriesentryoutputvalue = (dst_negative_weighted_add_outputsentriesentryoutput) + ge_balance_positive_weighted_add_outputsentriesentryoutputvalue))))))))) /\ (exists dsa_ap_weighted_add_outputsentriesentryoperation dsa_an_weighted_add_outputsentriesentryoperation dsa_bp_weighted_add_outputsentriesentryoperation dsa_bn_weighted_add_outputsentriesentryoperation dsa_cp_weighted_add_outputsentriesentryoperation dsa_cn_weighted_add_outputsentriesentryoperation. (((((sto_left_weighted_add_outputsentries) = 2 * (dsa_ap_weighted_add_outputsentriesentryoperation) /\ (dsa_an_weighted_add_outputsentriesentryoperation) = 0) \/ exists ge_signed_half_weighted_add_outputsentriesentryoperationleft. (((sto_left_weighted_add_outputsentries) = 2 * ge_signed_half_weighted_add_outputsentriesentryoperationleft + 1 /\ (dsa_ap_weighted_add_outputsentriesentryoperation) = 0) /\ (dsa_an_weighted_add_outputsentriesentryoperation) = S ge_signed_half_weighted_add_outputsentriesentryoperationleft))) /\ ((((((sto_right_weighted_add_outputsentries) = 2 * (dsa_bp_weighted_add_outputsentriesentryoperation) /\ (dsa_bn_weighted_add_outputsentriesentryoperation) = 0) \/ exists ge_signed_half_weighted_add_outputsentriesentryoperationright. (((sto_right_weighted_add_outputsentries) = 2 * ge_signed_half_weighted_add_outputsentriesentryoperationright + 1 /\ (dsa_bp_weighted_add_outputsentriesentryoperation) = 0) /\ (dsa_bn_weighted_add_outputsentriesentryoperation) = S ge_signed_half_weighted_add_outputsentriesentryoperationright))) /\ ((((((sto_output_weighted_add_outputsentries) = 2 * (dsa_cp_weighted_add_outputsentriesentryoperation) /\ (dsa_cn_weighted_add_outputsentriesentryoperation) = 0) \/ exists ge_signed_half_weighted_add_outputsentriesentryoperationoutput. (((sto_output_weighted_add_outputsentries) = 2 * ge_signed_half_weighted_add_outputsentriesentryoperationoutput + 1 /\ (dsa_cp_weighted_add_outputsentriesentryoperation) = 0) /\ (dsa_cn_weighted_add_outputsentriesentryoperation) = S ge_signed_half_weighted_add_outputsentriesentryoperationoutput))) /\ ((dsa_ap_weighted_add_outputsentriesentryoperation + dsa_bp_weighted_add_outputsentriesentryoperation) + dsa_cn_weighted_add_outputsentriesentryoperation = (dsa_an_weighted_add_outputsentriesentryoperation + dsa_bn_weighted_add_outputsentriesentryoperation) + dsa_cp_weighted_add_outputsentriesentryoperation)))))))))))))))))))