signed_table_add_lookup

Exact expanded first-order arithmetic statement

forall F G H l i a b c. (((exists dst_positive_code_add_lookup_relationleft_table dst_positive_scale_add_lookup_relationleft_table dst_negative_code_add_lookup_relationleft_table dst_negative_scale_add_lookup_relationleft_table. (((F) = (((((dst_positive_code_add_lookup_relationleft_table) + (dst_positive_scale_add_lookup_relationleft_table)) * S ((dst_positive_code_add_lookup_relationleft_table) + (dst_positive_scale_add_lookup_relationleft_table)) + ((dst_positive_scale_add_lookup_relationleft_table) + (dst_positive_scale_add_lookup_relationleft_table))) + (((dst_negative_code_add_lookup_relationleft_table) + (dst_negative_scale_add_lookup_relationleft_table)) * S ((dst_negative_code_add_lookup_relationleft_table) + (dst_negative_scale_add_lookup_relationleft_table)) + ((dst_negative_scale_add_lookup_relationleft_table) + (dst_negative_scale_add_lookup_relationleft_table)))) * S ((((dst_positive_code_add_lookup_relationleft_table) + (dst_positive_scale_add_lookup_relationleft_table)) * S ((dst_positive_code_add_lookup_relationleft_table) + (dst_positive_scale_add_lookup_relationleft_table)) + ((dst_positive_scale_add_lookup_relationleft_table) + (dst_positive_scale_add_lookup_relationleft_table))) + (((dst_negative_code_add_lookup_relationleft_table) + (dst_negative_scale_add_lookup_relationleft_table)) * S ((dst_negative_code_add_lookup_relationleft_table) + (dst_negative_scale_add_lookup_relationleft_table)) + ((dst_negative_scale_add_lookup_relationleft_table) + (dst_negative_scale_add_lookup_relationleft_table)))) + ((((dst_negative_code_add_lookup_relationleft_table) + (dst_negative_scale_add_lookup_relationleft_table)) * S ((dst_negative_code_add_lookup_relationleft_table) + (dst_negative_scale_add_lookup_relationleft_table)) + ((dst_negative_scale_add_lookup_relationleft_table) + (dst_negative_scale_add_lookup_relationleft_table))) + (((dst_negative_code_add_lookup_relationleft_table) + (dst_negative_scale_add_lookup_relationleft_table)) * S ((dst_negative_code_add_lookup_relationleft_table) + (dst_negative_scale_add_lookup_relationleft_table)) + ((dst_negative_scale_add_lookup_relationleft_table) + (dst_negative_scale_add_lookup_relationleft_table)))))) /\ (forall dst_index_add_lookup_relationleft_table. (exists pvs_le_gap_add_lookup_relationleft_tabledomain. pvs_le_gap_add_lookup_relationleft_tabledomain + (dst_index_add_lookup_relationleft_table) = (l)) -> exists dst_positive_add_lookup_relationleft_table dst_negative_add_lookup_relationleft_table dst_value_add_lookup_relationleft_table. ((((exists ff_h_pvs_add_lookup_relationleft_tableentrypositive. ff_h_pvs_add_lookup_relationleft_tableentrypositive + S (dst_positive_add_lookup_relationleft_table) = S ((S (dst_index_add_lookup_relationleft_table)) * dst_positive_scale_add_lookup_relationleft_table)) /\ exists ff_q_pvs_add_lookup_relationleft_tableentrypositive. dst_positive_code_add_lookup_relationleft_table = ff_q_pvs_add_lookup_relationleft_tableentrypositive * S ((S (dst_index_add_lookup_relationleft_table)) * dst_positive_scale_add_lookup_relationleft_table) + (dst_positive_add_lookup_relationleft_table))) /\ (((((exists ff_h_pvs_add_lookup_relationleft_tableentrynegative. ff_h_pvs_add_lookup_relationleft_tableentrynegative + S (dst_negative_add_lookup_relationleft_table) = S ((S (dst_index_add_lookup_relationleft_table)) * dst_negative_scale_add_lookup_relationleft_table)) /\ exists ff_q_pvs_add_lookup_relationleft_tableentrynegative. dst_negative_code_add_lookup_relationleft_table = ff_q_pvs_add_lookup_relationleft_tableentrynegative * S ((S (dst_index_add_lookup_relationleft_table)) * dst_negative_scale_add_lookup_relationleft_table) + (dst_negative_add_lookup_relationleft_table))) /\ (exists ge_balance_positive_add_lookup_relationleft_tableentryvalue ge_balance_negative_add_lookup_relationleft_tableentryvalue. (((((dst_value_add_lookup_relationleft_table) = 2 * (ge_balance_positive_add_lookup_relationleft_tableentryvalue) /\ (ge_balance_negative_add_lookup_relationleft_tableentryvalue) = 0) \/ exists ge_signed_half_add_lookup_relationleft_tableentryvaluedecode. (((dst_value_add_lookup_relationleft_table) = 2 * ge_signed_half_add_lookup_relationleft_tableentryvaluedecode + 1 /\ (ge_balance_positive_add_lookup_relationleft_tableentryvalue) = 0) /\ (ge_balance_negative_add_lookup_relationleft_tableentryvalue) = S ge_signed_half_add_lookup_relationleft_tableentryvaluedecode))) /\ ((dst_positive_add_lookup_relationleft_table) + ge_balance_negative_add_lookup_relationleft_tableentryvalue = (dst_negative_add_lookup_relationleft_table) + ge_balance_positive_add_lookup_relationleft_tableentryvalue))))))))) /\ (((exists dst_positive_code_add_lookup_relationright_table dst_positive_scale_add_lookup_relationright_table dst_negative_code_add_lookup_relationright_table dst_negative_scale_add_lookup_relationright_table. (((G) = (((((dst_positive_code_add_lookup_relationright_table) + (dst_positive_scale_add_lookup_relationright_table)) * S ((dst_positive_code_add_lookup_relationright_table) + (dst_positive_scale_add_lookup_relationright_table)) + ((dst_positive_scale_add_lookup_relationright_table) + (dst_positive_scale_add_lookup_relationright_table))) + (((dst_negative_code_add_lookup_relationright_table) + (dst_negative_scale_add_lookup_relationright_table)) * S ((dst_negative_code_add_lookup_relationright_table) + (dst_negative_scale_add_lookup_relationright_table)) + ((dst_negative_scale_add_lookup_relationright_table) + (dst_negative_scale_add_lookup_relationright_table)))) * S ((((dst_positive_code_add_lookup_relationright_table) + (dst_positive_scale_add_lookup_relationright_table)) * S ((dst_positive_code_add_lookup_relationright_table) + (dst_positive_scale_add_lookup_relationright_table)) + ((dst_positive_scale_add_lookup_relationright_table) + (dst_positive_scale_add_lookup_relationright_table))) + (((dst_negative_code_add_lookup_relationright_table) + (dst_negative_scale_add_lookup_relationright_table)) * S ((dst_negative_code_add_lookup_relationright_table) + (dst_negative_scale_add_lookup_relationright_table)) + ((dst_negative_scale_add_lookup_relationright_table) + (dst_negative_scale_add_lookup_relationright_table)))) + ((((dst_negative_code_add_lookup_relationright_table) + (dst_negative_scale_add_lookup_relationright_table)) * S ((dst_negative_code_add_lookup_relationright_table) + (dst_negative_scale_add_lookup_relationright_table)) + ((dst_negative_scale_add_lookup_relationright_table) + (dst_negative_scale_add_lookup_relationright_table))) + (((dst_negative_code_add_lookup_relationright_table) + (dst_negative_scale_add_lookup_relationright_table)) * S ((dst_negative_code_add_lookup_relationright_table) + (dst_negative_scale_add_lookup_relationright_table)) + ((dst_negative_scale_add_lookup_relationright_table) + (dst_negative_scale_add_lookup_relationright_table)))))) /\ (forall dst_index_add_lookup_relationright_table. (exists pvs_le_gap_add_lookup_relationright_tabledomain. pvs_le_gap_add_lookup_relationright_tabledomain + (dst_index_add_lookup_relationright_table) = (l)) -> exists dst_positive_add_lookup_relationright_table dst_negative_add_lookup_relationright_table dst_value_add_lookup_relationright_table. ((((exists ff_h_pvs_add_lookup_relationright_tableentrypositive. ff_h_pvs_add_lookup_relationright_tableentrypositive + S (dst_positive_add_lookup_relationright_table) = S ((S (dst_index_add_lookup_relationright_table)) * dst_positive_scale_add_lookup_relationright_table)) /\ exists ff_q_pvs_add_lookup_relationright_tableentrypositive. dst_positive_code_add_lookup_relationright_table = ff_q_pvs_add_lookup_relationright_tableentrypositive * S ((S (dst_index_add_lookup_relationright_table)) * dst_positive_scale_add_lookup_relationright_table) + (dst_positive_add_lookup_relationright_table))) /\ (((((exists ff_h_pvs_add_lookup_relationright_tableentrynegative. ff_h_pvs_add_lookup_relationright_tableentrynegative + S (dst_negative_add_lookup_relationright_table) = S ((S (dst_index_add_lookup_relationright_table)) * dst_negative_scale_add_lookup_relationright_table)) /\ exists ff_q_pvs_add_lookup_relationright_tableentrynegative. dst_negative_code_add_lookup_relationright_table = ff_q_pvs_add_lookup_relationright_tableentrynegative * S ((S (dst_index_add_lookup_relationright_table)) * dst_negative_scale_add_lookup_relationright_table) + (dst_negative_add_lookup_relationright_table))) /\ (exists ge_balance_positive_add_lookup_relationright_tableentryvalue ge_balance_negative_add_lookup_relationright_tableentryvalue. (((((dst_value_add_lookup_relationright_table) = 2 * (ge_balance_positive_add_lookup_relationright_tableentryvalue) /\ (ge_balance_negative_add_lookup_relationright_tableentryvalue) = 0) \/ exists ge_signed_half_add_lookup_relationright_tableentryvaluedecode. (((dst_value_add_lookup_relationright_table) = 2 * ge_signed_half_add_lookup_relationright_tableentryvaluedecode + 1 /\ (ge_balance_positive_add_lookup_relationright_tableentryvalue) = 0) /\ (ge_balance_negative_add_lookup_relationright_tableentryvalue) = S ge_signed_half_add_lookup_relationright_tableentryvaluedecode))) /\ ((dst_positive_add_lookup_relationright_table) + ge_balance_negative_add_lookup_relationright_tableentryvalue = (dst_negative_add_lookup_relationright_table) + ge_balance_positive_add_lookup_relationright_tableentryvalue))))))))) /\ (((exists dst_positive_code_add_lookup_relationoutput_table dst_positive_scale_add_lookup_relationoutput_table dst_negative_code_add_lookup_relationoutput_table dst_negative_scale_add_lookup_relationoutput_table. (((H) = (((((dst_positive_code_add_lookup_relationoutput_table) + (dst_positive_scale_add_lookup_relationoutput_table)) * S ((dst_positive_code_add_lookup_relationoutput_table) + (dst_positive_scale_add_lookup_relationoutput_table)) + ((dst_positive_scale_add_lookup_relationoutput_table) + (dst_positive_scale_add_lookup_relationoutput_table))) + (((dst_negative_code_add_lookup_relationoutput_table) + (dst_negative_scale_add_lookup_relationoutput_table)) * S ((dst_negative_code_add_lookup_relationoutput_table) + (dst_negative_scale_add_lookup_relationoutput_table)) + ((dst_negative_scale_add_lookup_relationoutput_table) + (dst_negative_scale_add_lookup_relationoutput_table)))) * S ((((dst_positive_code_add_lookup_relationoutput_table) + (dst_positive_scale_add_lookup_relationoutput_table)) * S ((dst_positive_code_add_lookup_relationoutput_table) + (dst_positive_scale_add_lookup_relationoutput_table)) + ((dst_positive_scale_add_lookup_relationoutput_table) + (dst_positive_scale_add_lookup_relationoutput_table))) + (((dst_negative_code_add_lookup_relationoutput_table) + (dst_negative_scale_add_lookup_relationoutput_table)) * S ((dst_negative_code_add_lookup_relationoutput_table) + (dst_negative_scale_add_lookup_relationoutput_table)) + ((dst_negative_scale_add_lookup_relationoutput_table) + (dst_negative_scale_add_lookup_relationoutput_table)))) + ((((dst_negative_code_add_lookup_relationoutput_table) + (dst_negative_scale_add_lookup_relationoutput_table)) * S ((dst_negative_code_add_lookup_relationoutput_table) + (dst_negative_scale_add_lookup_relationoutput_table)) + ((dst_negative_scale_add_lookup_relationoutput_table) + (dst_negative_scale_add_lookup_relationoutput_table))) + (((dst_negative_code_add_lookup_relationoutput_table) + (dst_negative_scale_add_lookup_relationoutput_table)) * S ((dst_negative_code_add_lookup_relationoutput_table) + (dst_negative_scale_add_lookup_relationoutput_table)) + ((dst_negative_scale_add_lookup_relationoutput_table) + (dst_negative_scale_add_lookup_relationoutput_table)))))) /\ (forall dst_index_add_lookup_relationoutput_table. (exists pvs_le_gap_add_lookup_relationoutput_tabledomain. pvs_le_gap_add_lookup_relationoutput_tabledomain + (dst_index_add_lookup_relationoutput_table) = (l)) -> exists dst_positive_add_lookup_relationoutput_table dst_negative_add_lookup_relationoutput_table dst_value_add_lookup_relationoutput_table. ((((exists ff_h_pvs_add_lookup_relationoutput_tableentrypositive. ff_h_pvs_add_lookup_relationoutput_tableentrypositive + S (dst_positive_add_lookup_relationoutput_table) = S ((S (dst_index_add_lookup_relationoutput_table)) * dst_positive_scale_add_lookup_relationoutput_table)) /\ exists ff_q_pvs_add_lookup_relationoutput_tableentrypositive. dst_positive_code_add_lookup_relationoutput_table = ff_q_pvs_add_lookup_relationoutput_tableentrypositive * S ((S (dst_index_add_lookup_relationoutput_table)) * dst_positive_scale_add_lookup_relationoutput_table) + (dst_positive_add_lookup_relationoutput_table))) /\ (((((exists ff_h_pvs_add_lookup_relationoutput_tableentrynegative. ff_h_pvs_add_lookup_relationoutput_tableentrynegative + S (dst_negative_add_lookup_relationoutput_table) = S ((S (dst_index_add_lookup_relationoutput_table)) * dst_negative_scale_add_lookup_relationoutput_table)) /\ exists ff_q_pvs_add_lookup_relationoutput_tableentrynegative. dst_negative_code_add_lookup_relationoutput_table = ff_q_pvs_add_lookup_relationoutput_tableentrynegative * S ((S (dst_index_add_lookup_relationoutput_table)) * dst_negative_scale_add_lookup_relationoutput_table) + (dst_negative_add_lookup_relationoutput_table))) /\ (exists ge_balance_positive_add_lookup_relationoutput_tableentryvalue ge_balance_negative_add_lookup_relationoutput_tableentryvalue. (((((dst_value_add_lookup_relationoutput_table) = 2 * (ge_balance_positive_add_lookup_relationoutput_tableentryvalue) /\ (ge_balance_negative_add_lookup_relationoutput_tableentryvalue) = 0) \/ exists ge_signed_half_add_lookup_relationoutput_tableentryvaluedecode. (((dst_value_add_lookup_relationoutput_table) = 2 * ge_signed_half_add_lookup_relationoutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_add_lookup_relationoutput_tableentryvalue) = 0) /\ (ge_balance_negative_add_lookup_relationoutput_tableentryvalue) = S ge_signed_half_add_lookup_relationoutput_tableentryvaluedecode))) /\ ((dst_positive_add_lookup_relationoutput_table) + ge_balance_negative_add_lookup_relationoutput_tableentryvalue = (dst_negative_add_lookup_relationoutput_table) + ge_balance_positive_add_lookup_relationoutput_tableentryvalue))))))))) /\ (forall sto_index_add_lookup_relationentries. (exists pvs_gap_add_lookup_relationentriesbound. pvs_gap_add_lookup_relationentriesbound + S (sto_index_add_lookup_relationentries) = (l)) -> exists sto_left_add_lookup_relationentries sto_right_add_lookup_relationentries sto_output_add_lookup_relationentries. ((exists dst_positive_code_add_lookup_relationentriesentryleft dst_positive_scale_add_lookup_relationentriesentryleft dst_negative_code_add_lookup_relationentriesentryleft dst_negative_scale_add_lookup_relationentriesentryleft dst_positive_add_lookup_relationentriesentryleft dst_negative_add_lookup_relationentriesentryleft. (((F) = (((((dst_positive_code_add_lookup_relationentriesentryleft) + (dst_positive_scale_add_lookup_relationentriesentryleft)) * S ((dst_positive_code_add_lookup_relationentriesentryleft) + (dst_positive_scale_add_lookup_relationentriesentryleft)) + ((dst_positive_scale_add_lookup_relationentriesentryleft) + (dst_positive_scale_add_lookup_relationentriesentryleft))) + (((dst_negative_code_add_lookup_relationentriesentryleft) + (dst_negative_scale_add_lookup_relationentriesentryleft)) * S ((dst_negative_code_add_lookup_relationentriesentryleft) + (dst_negative_scale_add_lookup_relationentriesentryleft)) + ((dst_negative_scale_add_lookup_relationentriesentryleft) + (dst_negative_scale_add_lookup_relationentriesentryleft)))) * S ((((dst_positive_code_add_lookup_relationentriesentryleft) + (dst_positive_scale_add_lookup_relationentriesentryleft)) * S ((dst_positive_code_add_lookup_relationentriesentryleft) + (dst_positive_scale_add_lookup_relationentriesentryleft)) + ((dst_positive_scale_add_lookup_relationentriesentryleft) + (dst_positive_scale_add_lookup_relationentriesentryleft))) + (((dst_negative_code_add_lookup_relationentriesentryleft) + (dst_negative_scale_add_lookup_relationentriesentryleft)) * S ((dst_negative_code_add_lookup_relationentriesentryleft) + (dst_negative_scale_add_lookup_relationentriesentryleft)) + ((dst_negative_scale_add_lookup_relationentriesentryleft) + (dst_negative_scale_add_lookup_relationentriesentryleft)))) + ((((dst_negative_code_add_lookup_relationentriesentryleft) + (dst_negative_scale_add_lookup_relationentriesentryleft)) * S ((dst_negative_code_add_lookup_relationentriesentryleft) + (dst_negative_scale_add_lookup_relationentriesentryleft)) + ((dst_negative_scale_add_lookup_relationentriesentryleft) + (dst_negative_scale_add_lookup_relationentriesentryleft))) + (((dst_negative_code_add_lookup_relationentriesentryleft) + (dst_negative_scale_add_lookup_relationentriesentryleft)) * S ((dst_negative_code_add_lookup_relationentriesentryleft) + (dst_negative_scale_add_lookup_relationentriesentryleft)) + ((dst_negative_scale_add_lookup_relationentriesentryleft) + (dst_negative_scale_add_lookup_relationentriesentryleft)))))) /\ (((((exists ff_h_pvs_add_lookup_relationentriesentryleftpositive. ff_h_pvs_add_lookup_relationentriesentryleftpositive + S (dst_positive_add_lookup_relationentriesentryleft) = S ((S (sto_index_add_lookup_relationentries)) * dst_positive_scale_add_lookup_relationentriesentryleft)) /\ exists ff_q_pvs_add_lookup_relationentriesentryleftpositive. dst_positive_code_add_lookup_relationentriesentryleft = ff_q_pvs_add_lookup_relationentriesentryleftpositive * S ((S (sto_index_add_lookup_relationentries)) * dst_positive_scale_add_lookup_relationentriesentryleft) + (dst_positive_add_lookup_relationentriesentryleft))) /\ (((((exists ff_h_pvs_add_lookup_relationentriesentryleftnegative. ff_h_pvs_add_lookup_relationentriesentryleftnegative + S (dst_negative_add_lookup_relationentriesentryleft) = S ((S (sto_index_add_lookup_relationentries)) * dst_negative_scale_add_lookup_relationentriesentryleft)) /\ exists ff_q_pvs_add_lookup_relationentriesentryleftnegative. dst_negative_code_add_lookup_relationentriesentryleft = ff_q_pvs_add_lookup_relationentriesentryleftnegative * S ((S (sto_index_add_lookup_relationentries)) * dst_negative_scale_add_lookup_relationentriesentryleft) + (dst_negative_add_lookup_relationentriesentryleft))) /\ (exists ge_balance_positive_add_lookup_relationentriesentryleftvalue ge_balance_negative_add_lookup_relationentriesentryleftvalue. (((((sto_left_add_lookup_relationentries) = 2 * (ge_balance_positive_add_lookup_relationentriesentryleftvalue) /\ (ge_balance_negative_add_lookup_relationentriesentryleftvalue) = 0) \/ exists ge_signed_half_add_lookup_relationentriesentryleftvaluedecode. (((sto_left_add_lookup_relationentries) = 2 * ge_signed_half_add_lookup_relationentriesentryleftvaluedecode + 1 /\ (ge_balance_positive_add_lookup_relationentriesentryleftvalue) = 0) /\ (ge_balance_negative_add_lookup_relationentriesentryleftvalue) = S ge_signed_half_add_lookup_relationentriesentryleftvaluedecode))) /\ ((dst_positive_add_lookup_relationentriesentryleft) + ge_balance_negative_add_lookup_relationentriesentryleftvalue = (dst_negative_add_lookup_relationentriesentryleft) + ge_balance_positive_add_lookup_relationentriesentryleftvalue))))))))) /\ (((exists dst_positive_code_add_lookup_relationentriesentryright dst_positive_scale_add_lookup_relationentriesentryright dst_negative_code_add_lookup_relationentriesentryright dst_negative_scale_add_lookup_relationentriesentryright dst_positive_add_lookup_relationentriesentryright dst_negative_add_lookup_relationentriesentryright. (((G) = (((((dst_positive_code_add_lookup_relationentriesentryright) + (dst_positive_scale_add_lookup_relationentriesentryright)) * S ((dst_positive_code_add_lookup_relationentriesentryright) + (dst_positive_scale_add_lookup_relationentriesentryright)) + ((dst_positive_scale_add_lookup_relationentriesentryright) + (dst_positive_scale_add_lookup_relationentriesentryright))) + (((dst_negative_code_add_lookup_relationentriesentryright) + (dst_negative_scale_add_lookup_relationentriesentryright)) * S ((dst_negative_code_add_lookup_relationentriesentryright) + (dst_negative_scale_add_lookup_relationentriesentryright)) + ((dst_negative_scale_add_lookup_relationentriesentryright) + (dst_negative_scale_add_lookup_relationentriesentryright)))) * S ((((dst_positive_code_add_lookup_relationentriesentryright) + (dst_positive_scale_add_lookup_relationentriesentryright)) * S ((dst_positive_code_add_lookup_relationentriesentryright) + (dst_positive_scale_add_lookup_relationentriesentryright)) + ((dst_positive_scale_add_lookup_relationentriesentryright) + (dst_positive_scale_add_lookup_relationentriesentryright))) + (((dst_negative_code_add_lookup_relationentriesentryright) + (dst_negative_scale_add_lookup_relationentriesentryright)) * S ((dst_negative_code_add_lookup_relationentriesentryright) + (dst_negative_scale_add_lookup_relationentriesentryright)) + ((dst_negative_scale_add_lookup_relationentriesentryright) + (dst_negative_scale_add_lookup_relationentriesentryright)))) + ((((dst_negative_code_add_lookup_relationentriesentryright) + (dst_negative_scale_add_lookup_relationentriesentryright)) * S ((dst_negative_code_add_lookup_relationentriesentryright) + (dst_negative_scale_add_lookup_relationentriesentryright)) + ((dst_negative_scale_add_lookup_relationentriesentryright) + (dst_negative_scale_add_lookup_relationentriesentryright))) + (((dst_negative_code_add_lookup_relationentriesentryright) + (dst_negative_scale_add_lookup_relationentriesentryright)) * S ((dst_negative_code_add_lookup_relationentriesentryright) + (dst_negative_scale_add_lookup_relationentriesentryright)) + ((dst_negative_scale_add_lookup_relationentriesentryright) + (dst_negative_scale_add_lookup_relationentriesentryright)))))) /\ (((((exists ff_h_pvs_add_lookup_relationentriesentryrightpositive. ff_h_pvs_add_lookup_relationentriesentryrightpositive + S (dst_positive_add_lookup_relationentriesentryright) = S ((S (sto_index_add_lookup_relationentries)) * dst_positive_scale_add_lookup_relationentriesentryright)) /\ exists ff_q_pvs_add_lookup_relationentriesentryrightpositive. dst_positive_code_add_lookup_relationentriesentryright = ff_q_pvs_add_lookup_relationentriesentryrightpositive * S ((S (sto_index_add_lookup_relationentries)) * dst_positive_scale_add_lookup_relationentriesentryright) + (dst_positive_add_lookup_relationentriesentryright))) /\ (((((exists ff_h_pvs_add_lookup_relationentriesentryrightnegative. ff_h_pvs_add_lookup_relationentriesentryrightnegative + S (dst_negative_add_lookup_relationentriesentryright) = S ((S (sto_index_add_lookup_relationentries)) * dst_negative_scale_add_lookup_relationentriesentryright)) /\ exists ff_q_pvs_add_lookup_relationentriesentryrightnegative. dst_negative_code_add_lookup_relationentriesentryright = ff_q_pvs_add_lookup_relationentriesentryrightnegative * S ((S (sto_index_add_lookup_relationentries)) * dst_negative_scale_add_lookup_relationentriesentryright) + (dst_negative_add_lookup_relationentriesentryright))) /\ (exists ge_balance_positive_add_lookup_relationentriesentryrightvalue ge_balance_negative_add_lookup_relationentriesentryrightvalue. (((((sto_right_add_lookup_relationentries) = 2 * (ge_balance_positive_add_lookup_relationentriesentryrightvalue) /\ (ge_balance_negative_add_lookup_relationentriesentryrightvalue) = 0) \/ exists ge_signed_half_add_lookup_relationentriesentryrightvaluedecode. (((sto_right_add_lookup_relationentries) = 2 * ge_signed_half_add_lookup_relationentriesentryrightvaluedecode + 1 /\ (ge_balance_positive_add_lookup_relationentriesentryrightvalue) = 0) /\ (ge_balance_negative_add_lookup_relationentriesentryrightvalue) = S ge_signed_half_add_lookup_relationentriesentryrightvaluedecode))) /\ ((dst_positive_add_lookup_relationentriesentryright) + ge_balance_negative_add_lookup_relationentriesentryrightvalue = (dst_negative_add_lookup_relationentriesentryright) + ge_balance_positive_add_lookup_relationentriesentryrightvalue))))))))) /\ (((exists dst_positive_code_add_lookup_relationentriesentryoutput dst_positive_scale_add_lookup_relationentriesentryoutput dst_negative_code_add_lookup_relationentriesentryoutput dst_negative_scale_add_lookup_relationentriesentryoutput dst_positive_add_lookup_relationentriesentryoutput dst_negative_add_lookup_relationentriesentryoutput. (((H) = (((((dst_positive_code_add_lookup_relationentriesentryoutput) + (dst_positive_scale_add_lookup_relationentriesentryoutput)) * S ((dst_positive_code_add_lookup_relationentriesentryoutput) + (dst_positive_scale_add_lookup_relationentriesentryoutput)) + ((dst_positive_scale_add_lookup_relationentriesentryoutput) + (dst_positive_scale_add_lookup_relationentriesentryoutput))) + (((dst_negative_code_add_lookup_relationentriesentryoutput) + (dst_negative_scale_add_lookup_relationentriesentryoutput)) * S ((dst_negative_code_add_lookup_relationentriesentryoutput) + (dst_negative_scale_add_lookup_relationentriesentryoutput)) + ((dst_negative_scale_add_lookup_relationentriesentryoutput) + (dst_negative_scale_add_lookup_relationentriesentryoutput)))) * S ((((dst_positive_code_add_lookup_relationentriesentryoutput) + (dst_positive_scale_add_lookup_relationentriesentryoutput)) * S ((dst_positive_code_add_lookup_relationentriesentryoutput) + (dst_positive_scale_add_lookup_relationentriesentryoutput)) + ((dst_positive_scale_add_lookup_relationentriesentryoutput) + (dst_positive_scale_add_lookup_relationentriesentryoutput))) + (((dst_negative_code_add_lookup_relationentriesentryoutput) + (dst_negative_scale_add_lookup_relationentriesentryoutput)) * S ((dst_negative_code_add_lookup_relationentriesentryoutput) + (dst_negative_scale_add_lookup_relationentriesentryoutput)) + ((dst_negative_scale_add_lookup_relationentriesentryoutput) + (dst_negative_scale_add_lookup_relationentriesentryoutput)))) + ((((dst_negative_code_add_lookup_relationentriesentryoutput) + (dst_negative_scale_add_lookup_relationentriesentryoutput)) * S ((dst_negative_code_add_lookup_relationentriesentryoutput) + (dst_negative_scale_add_lookup_relationentriesentryoutput)) + ((dst_negative_scale_add_lookup_relationentriesentryoutput) + (dst_negative_scale_add_lookup_relationentriesentryoutput))) + (((dst_negative_code_add_lookup_relationentriesentryoutput) + (dst_negative_scale_add_lookup_relationentriesentryoutput)) * S ((dst_negative_code_add_lookup_relationentriesentryoutput) + (dst_negative_scale_add_lookup_relationentriesentryoutput)) + ((dst_negative_scale_add_lookup_relationentriesentryoutput) + (dst_negative_scale_add_lookup_relationentriesentryoutput)))))) /\ (((((exists ff_h_pvs_add_lookup_relationentriesentryoutputpositive. ff_h_pvs_add_lookup_relationentriesentryoutputpositive + S (dst_positive_add_lookup_relationentriesentryoutput) = S ((S (sto_index_add_lookup_relationentries)) * dst_positive_scale_add_lookup_relationentriesentryoutput)) /\ exists ff_q_pvs_add_lookup_relationentriesentryoutputpositive. dst_positive_code_add_lookup_relationentriesentryoutput = ff_q_pvs_add_lookup_relationentriesentryoutputpositive * S ((S (sto_index_add_lookup_relationentries)) * dst_positive_scale_add_lookup_relationentriesentryoutput) + (dst_positive_add_lookup_relationentriesentryoutput))) /\ (((((exists ff_h_pvs_add_lookup_relationentriesentryoutputnegative. ff_h_pvs_add_lookup_relationentriesentryoutputnegative + S (dst_negative_add_lookup_relationentriesentryoutput) = S ((S (sto_index_add_lookup_relationentries)) * dst_negative_scale_add_lookup_relationentriesentryoutput)) /\ exists ff_q_pvs_add_lookup_relationentriesentryoutputnegative. dst_negative_code_add_lookup_relationentriesentryoutput = ff_q_pvs_add_lookup_relationentriesentryoutputnegative * S ((S (sto_index_add_lookup_relationentries)) * dst_negative_scale_add_lookup_relationentriesentryoutput) + (dst_negative_add_lookup_relationentriesentryoutput))) /\ (exists ge_balance_positive_add_lookup_relationentriesentryoutputvalue ge_balance_negative_add_lookup_relationentriesentryoutputvalue. (((((sto_output_add_lookup_relationentries) = 2 * (ge_balance_positive_add_lookup_relationentriesentryoutputvalue) /\ (ge_balance_negative_add_lookup_relationentriesentryoutputvalue) = 0) \/ exists ge_signed_half_add_lookup_relationentriesentryoutputvaluedecode. (((sto_output_add_lookup_relationentries) = 2 * ge_signed_half_add_lookup_relationentriesentryoutputvaluedecode + 1 /\ (ge_balance_positive_add_lookup_relationentriesentryoutputvalue) = 0) /\ (ge_balance_negative_add_lookup_relationentriesentryoutputvalue) = S ge_signed_half_add_lookup_relationentriesentryoutputvaluedecode))) /\ ((dst_positive_add_lookup_relationentriesentryoutput) + ge_balance_negative_add_lookup_relationentriesentryoutputvalue = (dst_negative_add_lookup_relationentriesentryoutput) + ge_balance_positive_add_lookup_relationentriesentryoutputvalue))))))))) /\ (exists dsa_ap_add_lookup_relationentriesentryoperation dsa_an_add_lookup_relationentriesentryoperation dsa_bp_add_lookup_relationentriesentryoperation dsa_bn_add_lookup_relationentriesentryoperation dsa_cp_add_lookup_relationentriesentryoperation dsa_cn_add_lookup_relationentriesentryoperation. (((((sto_left_add_lookup_relationentries) = 2 * (dsa_ap_add_lookup_relationentriesentryoperation) /\ (dsa_an_add_lookup_relationentriesentryoperation) = 0) \/ exists ge_signed_half_add_lookup_relationentriesentryoperationleft. (((sto_left_add_lookup_relationentries) = 2 * ge_signed_half_add_lookup_relationentriesentryoperationleft + 1 /\ (dsa_ap_add_lookup_relationentriesentryoperation) = 0) /\ (dsa_an_add_lookup_relationentriesentryoperation) = S ge_signed_half_add_lookup_relationentriesentryoperationleft))) /\ ((((((sto_right_add_lookup_relationentries) = 2 * (dsa_bp_add_lookup_relationentriesentryoperation) /\ (dsa_bn_add_lookup_relationentriesentryoperation) = 0) \/ exists ge_signed_half_add_lookup_relationentriesentryoperationright. (((sto_right_add_lookup_relationentries) = 2 * ge_signed_half_add_lookup_relationentriesentryoperationright + 1 /\ (dsa_bp_add_lookup_relationentriesentryoperation) = 0) /\ (dsa_bn_add_lookup_relationentriesentryoperation) = S ge_signed_half_add_lookup_relationentriesentryoperationright))) /\ ((((((sto_output_add_lookup_relationentries) = 2 * (dsa_cp_add_lookup_relationentriesentryoperation) /\ (dsa_cn_add_lookup_relationentriesentryoperation) = 0) \/ exists ge_signed_half_add_lookup_relationentriesentryoperationoutput. (((sto_output_add_lookup_relationentries) = 2 * ge_signed_half_add_lookup_relationentriesentryoperationoutput + 1 /\ (dsa_cp_add_lookup_relationentriesentryoperation) = 0) /\ (dsa_cn_add_lookup_relationentriesentryoperation) = S ge_signed_half_add_lookup_relationentriesentryoperationoutput))) /\ ((dsa_ap_add_lookup_relationentriesentryoperation + dsa_bp_add_lookup_relationentriesentryoperation) + dsa_cn_add_lookup_relationentriesentryoperation = (dsa_an_add_lookup_relationentriesentryoperation + dsa_bn_add_lookup_relationentriesentryoperation) + dsa_cp_add_lookup_relationentriesentryoperation))))))))))))))))))) -> (exists pvs_gap_add_lookup_bound. pvs_gap_add_lookup_bound + S (i) = (l)) -> (exists dst_positive_code_add_lookup_0 dst_positive_scale_add_lookup_0 dst_negative_code_add_lookup_0 dst_negative_scale_add_lookup_0 dst_positive_add_lookup_0 dst_negative_add_lookup_0. (((F) = (((((dst_positive_code_add_lookup_0) + (dst_positive_scale_add_lookup_0)) * S ((dst_positive_code_add_lookup_0) + (dst_positive_scale_add_lookup_0)) + ((dst_positive_scale_add_lookup_0) + (dst_positive_scale_add_lookup_0))) + (((dst_negative_code_add_lookup_0) + (dst_negative_scale_add_lookup_0)) * S ((dst_negative_code_add_lookup_0) + (dst_negative_scale_add_lookup_0)) + ((dst_negative_scale_add_lookup_0) + (dst_negative_scale_add_lookup_0)))) * S ((((dst_positive_code_add_lookup_0) + (dst_positive_scale_add_lookup_0)) * S ((dst_positive_code_add_lookup_0) + (dst_positive_scale_add_lookup_0)) + ((dst_positive_scale_add_lookup_0) + (dst_positive_scale_add_lookup_0))) + (((dst_negative_code_add_lookup_0) + (dst_negative_scale_add_lookup_0)) * S ((dst_negative_code_add_lookup_0) + (dst_negative_scale_add_lookup_0)) + ((dst_negative_scale_add_lookup_0) + (dst_negative_scale_add_lookup_0)))) + ((((dst_negative_code_add_lookup_0) + (dst_negative_scale_add_lookup_0)) * S ((dst_negative_code_add_lookup_0) + (dst_negative_scale_add_lookup_0)) + ((dst_negative_scale_add_lookup_0) + (dst_negative_scale_add_lookup_0))) + (((dst_negative_code_add_lookup_0) + (dst_negative_scale_add_lookup_0)) * S ((dst_negative_code_add_lookup_0) + (dst_negative_scale_add_lookup_0)) + ((dst_negative_scale_add_lookup_0) + (dst_negative_scale_add_lookup_0)))))) /\ (((((exists ff_h_pvs_add_lookup_0positive. ff_h_pvs_add_lookup_0positive + S (dst_positive_add_lookup_0) = S ((S (i)) * dst_positive_scale_add_lookup_0)) /\ exists ff_q_pvs_add_lookup_0positive. dst_positive_code_add_lookup_0 = ff_q_pvs_add_lookup_0positive * S ((S (i)) * dst_positive_scale_add_lookup_0) + (dst_positive_add_lookup_0))) /\ (((((exists ff_h_pvs_add_lookup_0negative. ff_h_pvs_add_lookup_0negative + S (dst_negative_add_lookup_0) = S ((S (i)) * dst_negative_scale_add_lookup_0)) /\ exists ff_q_pvs_add_lookup_0negative. dst_negative_code_add_lookup_0 = ff_q_pvs_add_lookup_0negative * S ((S (i)) * dst_negative_scale_add_lookup_0) + (dst_negative_add_lookup_0))) /\ (exists ge_balance_positive_add_lookup_0value ge_balance_negative_add_lookup_0value. (((((a) = 2 * (ge_balance_positive_add_lookup_0value) /\ (ge_balance_negative_add_lookup_0value) = 0) \/ exists ge_signed_half_add_lookup_0valuedecode. (((a) = 2 * ge_signed_half_add_lookup_0valuedecode + 1 /\ (ge_balance_positive_add_lookup_0value) = 0) /\ (ge_balance_negative_add_lookup_0value) = S ge_signed_half_add_lookup_0valuedecode))) /\ ((dst_positive_add_lookup_0) + ge_balance_negative_add_lookup_0value = (dst_negative_add_lookup_0) + ge_balance_positive_add_lookup_0value))))))))) -> (exists dst_positive_code_add_lookup_1 dst_positive_scale_add_lookup_1 dst_negative_code_add_lookup_1 dst_negative_scale_add_lookup_1 dst_positive_add_lookup_1 dst_negative_add_lookup_1. (((G) = (((((dst_positive_code_add_lookup_1) + (dst_positive_scale_add_lookup_1)) * S ((dst_positive_code_add_lookup_1) + (dst_positive_scale_add_lookup_1)) + ((dst_positive_scale_add_lookup_1) + (dst_positive_scale_add_lookup_1))) + (((dst_negative_code_add_lookup_1) + (dst_negative_scale_add_lookup_1)) * S ((dst_negative_code_add_lookup_1) + (dst_negative_scale_add_lookup_1)) + ((dst_negative_scale_add_lookup_1) + (dst_negative_scale_add_lookup_1)))) * S ((((dst_positive_code_add_lookup_1) + (dst_positive_scale_add_lookup_1)) * S ((dst_positive_code_add_lookup_1) + (dst_positive_scale_add_lookup_1)) + ((dst_positive_scale_add_lookup_1) + (dst_positive_scale_add_lookup_1))) + (((dst_negative_code_add_lookup_1) + (dst_negative_scale_add_lookup_1)) * S ((dst_negative_code_add_lookup_1) + (dst_negative_scale_add_lookup_1)) + ((dst_negative_scale_add_lookup_1) + (dst_negative_scale_add_lookup_1)))) + ((((dst_negative_code_add_lookup_1) + (dst_negative_scale_add_lookup_1)) * S ((dst_negative_code_add_lookup_1) + (dst_negative_scale_add_lookup_1)) + ((dst_negative_scale_add_lookup_1) + (dst_negative_scale_add_lookup_1))) + (((dst_negative_code_add_lookup_1) + (dst_negative_scale_add_lookup_1)) * S ((dst_negative_code_add_lookup_1) + (dst_negative_scale_add_lookup_1)) + ((dst_negative_scale_add_lookup_1) + (dst_negative_scale_add_lookup_1)))))) /\ (((((exists ff_h_pvs_add_lookup_1positive. ff_h_pvs_add_lookup_1positive + S (dst_positive_add_lookup_1) = S ((S (i)) * dst_positive_scale_add_lookup_1)) /\ exists ff_q_pvs_add_lookup_1positive. dst_positive_code_add_lookup_1 = ff_q_pvs_add_lookup_1positive * S ((S (i)) * dst_positive_scale_add_lookup_1) + (dst_positive_add_lookup_1))) /\ (((((exists ff_h_pvs_add_lookup_1negative. ff_h_pvs_add_lookup_1negative + S (dst_negative_add_lookup_1) = S ((S (i)) * dst_negative_scale_add_lookup_1)) /\ exists ff_q_pvs_add_lookup_1negative. dst_negative_code_add_lookup_1 = ff_q_pvs_add_lookup_1negative * S ((S (i)) * dst_negative_scale_add_lookup_1) + (dst_negative_add_lookup_1))) /\ (exists ge_balance_positive_add_lookup_1value ge_balance_negative_add_lookup_1value. (((((b) = 2 * (ge_balance_positive_add_lookup_1value) /\ (ge_balance_negative_add_lookup_1value) = 0) \/ exists ge_signed_half_add_lookup_1valuedecode. (((b) = 2 * ge_signed_half_add_lookup_1valuedecode + 1 /\ (ge_balance_positive_add_lookup_1value) = 0) /\ (ge_balance_negative_add_lookup_1value) = S ge_signed_half_add_lookup_1valuedecode))) /\ ((dst_positive_add_lookup_1) + ge_balance_negative_add_lookup_1value = (dst_negative_add_lookup_1) + ge_balance_positive_add_lookup_1value))))))))) -> (exists dst_positive_code_add_lookup_2 dst_positive_scale_add_lookup_2 dst_negative_code_add_lookup_2 dst_negative_scale_add_lookup_2 dst_positive_add_lookup_2 dst_negative_add_lookup_2. (((H) = (((((dst_positive_code_add_lookup_2) + (dst_positive_scale_add_lookup_2)) * S ((dst_positive_code_add_lookup_2) + (dst_positive_scale_add_lookup_2)) + ((dst_positive_scale_add_lookup_2) + (dst_positive_scale_add_lookup_2))) + (((dst_negative_code_add_lookup_2) + (dst_negative_scale_add_lookup_2)) * S ((dst_negative_code_add_lookup_2) + (dst_negative_scale_add_lookup_2)) + ((dst_negative_scale_add_lookup_2) + (dst_negative_scale_add_lookup_2)))) * S ((((dst_positive_code_add_lookup_2) + (dst_positive_scale_add_lookup_2)) * S ((dst_positive_code_add_lookup_2) + (dst_positive_scale_add_lookup_2)) + ((dst_positive_scale_add_lookup_2) + (dst_positive_scale_add_lookup_2))) + (((dst_negative_code_add_lookup_2) + (dst_negative_scale_add_lookup_2)) * S ((dst_negative_code_add_lookup_2) + (dst_negative_scale_add_lookup_2)) + ((dst_negative_scale_add_lookup_2) + (dst_negative_scale_add_lookup_2)))) + ((((dst_negative_code_add_lookup_2) + (dst_negative_scale_add_lookup_2)) * S ((dst_negative_code_add_lookup_2) + (dst_negative_scale_add_lookup_2)) + ((dst_negative_scale_add_lookup_2) + (dst_negative_scale_add_lookup_2))) + (((dst_negative_code_add_lookup_2) + (dst_negative_scale_add_lookup_2)) * S ((dst_negative_code_add_lookup_2) + (dst_negative_scale_add_lookup_2)) + ((dst_negative_scale_add_lookup_2) + (dst_negative_scale_add_lookup_2)))))) /\ (((((exists ff_h_pvs_add_lookup_2positive. ff_h_pvs_add_lookup_2positive + S (dst_positive_add_lookup_2) = S ((S (i)) * dst_positive_scale_add_lookup_2)) /\ exists ff_q_pvs_add_lookup_2positive. dst_positive_code_add_lookup_2 = ff_q_pvs_add_lookup_2positive * S ((S (i)) * dst_positive_scale_add_lookup_2) + (dst_positive_add_lookup_2))) /\ (((((exists ff_h_pvs_add_lookup_2negative. ff_h_pvs_add_lookup_2negative + S (dst_negative_add_lookup_2) = S ((S (i)) * dst_negative_scale_add_lookup_2)) /\ exists ff_q_pvs_add_lookup_2negative. dst_negative_code_add_lookup_2 = ff_q_pvs_add_lookup_2negative * S ((S (i)) * dst_negative_scale_add_lookup_2) + (dst_negative_add_lookup_2))) /\ (exists ge_balance_positive_add_lookup_2value ge_balance_negative_add_lookup_2value. (((((c) = 2 * (ge_balance_positive_add_lookup_2value) /\ (ge_balance_negative_add_lookup_2value) = 0) \/ exists ge_signed_half_add_lookup_2valuedecode. (((c) = 2 * ge_signed_half_add_lookup_2valuedecode + 1 /\ (ge_balance_positive_add_lookup_2value) = 0) /\ (ge_balance_negative_add_lookup_2value) = S ge_signed_half_add_lookup_2valuedecode))) /\ ((dst_positive_add_lookup_2) + ge_balance_negative_add_lookup_2value = (dst_negative_add_lookup_2) + ge_balance_positive_add_lookup_2value))))))))) -> (exists dsa_ap_add_lookup_operation dsa_an_add_lookup_operation dsa_bp_add_lookup_operation dsa_bn_add_lookup_operation dsa_cp_add_lookup_operation dsa_cn_add_lookup_operation. (((((a) = 2 * (dsa_ap_add_lookup_operation) /\ (dsa_an_add_lookup_operation) = 0) \/ exists ge_signed_half_add_lookup_operationleft. (((a) = 2 * ge_signed_half_add_lookup_operationleft + 1 /\ (dsa_ap_add_lookup_operation) = 0) /\ (dsa_an_add_lookup_operation) = S ge_signed_half_add_lookup_operationleft))) /\ ((((((b) = 2 * (dsa_bp_add_lookup_operation) /\ (dsa_bn_add_lookup_operation) = 0) \/ exists ge_signed_half_add_lookup_operationright. (((b) = 2 * ge_signed_half_add_lookup_operationright + 1 /\ (dsa_bp_add_lookup_operation) = 0) /\ (dsa_bn_add_lookup_operation) = S ge_signed_half_add_lookup_operationright))) /\ ((((((c) = 2 * (dsa_cp_add_lookup_operation) /\ (dsa_cn_add_lookup_operation) = 0) \/ exists ge_signed_half_add_lookup_operationoutput. (((c) = 2 * ge_signed_half_add_lookup_operationoutput + 1 /\ (dsa_cp_add_lookup_operation) = 0) /\ (dsa_cn_add_lookup_operation) = S ge_signed_half_add_lookup_operationoutput))) /\ ((dsa_ap_add_lookup_operation + dsa_bp_add_lookup_operation) + dsa_cn_add_lookup_operation = (dsa_an_add_lookup_operation + dsa_bn_add_lookup_operation) + dsa_cp_add_lookup_operation)))))))