signed_table_add_exists_extensionally_unique

Exact expanded first-order arithmetic statement

forall l F G. (exists dst_positive_code_add_exists_unique_input0 dst_positive_scale_add_exists_unique_input0 dst_negative_code_add_exists_unique_input0 dst_negative_scale_add_exists_unique_input0. (((F) = (((((dst_positive_code_add_exists_unique_input0) + (dst_positive_scale_add_exists_unique_input0)) * S ((dst_positive_code_add_exists_unique_input0) + (dst_positive_scale_add_exists_unique_input0)) + ((dst_positive_scale_add_exists_unique_input0) + (dst_positive_scale_add_exists_unique_input0))) + (((dst_negative_code_add_exists_unique_input0) + (dst_negative_scale_add_exists_unique_input0)) * S ((dst_negative_code_add_exists_unique_input0) + (dst_negative_scale_add_exists_unique_input0)) + ((dst_negative_scale_add_exists_unique_input0) + (dst_negative_scale_add_exists_unique_input0)))) * S ((((dst_positive_code_add_exists_unique_input0) + (dst_positive_scale_add_exists_unique_input0)) * S ((dst_positive_code_add_exists_unique_input0) + (dst_positive_scale_add_exists_unique_input0)) + ((dst_positive_scale_add_exists_unique_input0) + (dst_positive_scale_add_exists_unique_input0))) + (((dst_negative_code_add_exists_unique_input0) + (dst_negative_scale_add_exists_unique_input0)) * S ((dst_negative_code_add_exists_unique_input0) + (dst_negative_scale_add_exists_unique_input0)) + ((dst_negative_scale_add_exists_unique_input0) + (dst_negative_scale_add_exists_unique_input0)))) + ((((dst_negative_code_add_exists_unique_input0) + (dst_negative_scale_add_exists_unique_input0)) * S ((dst_negative_code_add_exists_unique_input0) + (dst_negative_scale_add_exists_unique_input0)) + ((dst_negative_scale_add_exists_unique_input0) + (dst_negative_scale_add_exists_unique_input0))) + (((dst_negative_code_add_exists_unique_input0) + (dst_negative_scale_add_exists_unique_input0)) * S ((dst_negative_code_add_exists_unique_input0) + (dst_negative_scale_add_exists_unique_input0)) + ((dst_negative_scale_add_exists_unique_input0) + (dst_negative_scale_add_exists_unique_input0)))))) /\ (forall dst_index_add_exists_unique_input0. (exists pvs_le_gap_add_exists_unique_input0domain. pvs_le_gap_add_exists_unique_input0domain + (dst_index_add_exists_unique_input0) = (l)) -> exists dst_positive_add_exists_unique_input0 dst_negative_add_exists_unique_input0 dst_value_add_exists_unique_input0. ((((exists ff_h_pvs_add_exists_unique_input0entrypositive. ff_h_pvs_add_exists_unique_input0entrypositive + S (dst_positive_add_exists_unique_input0) = S ((S (dst_index_add_exists_unique_input0)) * dst_positive_scale_add_exists_unique_input0)) /\ exists ff_q_pvs_add_exists_unique_input0entrypositive. dst_positive_code_add_exists_unique_input0 = ff_q_pvs_add_exists_unique_input0entrypositive * S ((S (dst_index_add_exists_unique_input0)) * dst_positive_scale_add_exists_unique_input0) + (dst_positive_add_exists_unique_input0))) /\ (((((exists ff_h_pvs_add_exists_unique_input0entrynegative. ff_h_pvs_add_exists_unique_input0entrynegative + S (dst_negative_add_exists_unique_input0) = S ((S (dst_index_add_exists_unique_input0)) * dst_negative_scale_add_exists_unique_input0)) /\ exists ff_q_pvs_add_exists_unique_input0entrynegative. dst_negative_code_add_exists_unique_input0 = ff_q_pvs_add_exists_unique_input0entrynegative * S ((S (dst_index_add_exists_unique_input0)) * dst_negative_scale_add_exists_unique_input0) + (dst_negative_add_exists_unique_input0))) /\ (exists ge_balance_positive_add_exists_unique_input0entryvalue ge_balance_negative_add_exists_unique_input0entryvalue. (((((dst_value_add_exists_unique_input0) = 2 * (ge_balance_positive_add_exists_unique_input0entryvalue) /\ (ge_balance_negative_add_exists_unique_input0entryvalue) = 0) \/ exists ge_signed_half_add_exists_unique_input0entryvaluedecode. (((dst_value_add_exists_unique_input0) = 2 * ge_signed_half_add_exists_unique_input0entryvaluedecode + 1 /\ (ge_balance_positive_add_exists_unique_input0entryvalue) = 0) /\ (ge_balance_negative_add_exists_unique_input0entryvalue) = S ge_signed_half_add_exists_unique_input0entryvaluedecode))) /\ ((dst_positive_add_exists_unique_input0) + ge_balance_negative_add_exists_unique_input0entryvalue = (dst_negative_add_exists_unique_input0) + ge_balance_positive_add_exists_unique_input0entryvalue))))))))) -> (exists dst_positive_code_add_exists_unique_input1 dst_positive_scale_add_exists_unique_input1 dst_negative_code_add_exists_unique_input1 dst_negative_scale_add_exists_unique_input1. (((G) = (((((dst_positive_code_add_exists_unique_input1) + (dst_positive_scale_add_exists_unique_input1)) * S ((dst_positive_code_add_exists_unique_input1) + (dst_positive_scale_add_exists_unique_input1)) + ((dst_positive_scale_add_exists_unique_input1) + (dst_positive_scale_add_exists_unique_input1))) + (((dst_negative_code_add_exists_unique_input1) + (dst_negative_scale_add_exists_unique_input1)) * S ((dst_negative_code_add_exists_unique_input1) + (dst_negative_scale_add_exists_unique_input1)) + ((dst_negative_scale_add_exists_unique_input1) + (dst_negative_scale_add_exists_unique_input1)))) * S ((((dst_positive_code_add_exists_unique_input1) + (dst_positive_scale_add_exists_unique_input1)) * S ((dst_positive_code_add_exists_unique_input1) + (dst_positive_scale_add_exists_unique_input1)) + ((dst_positive_scale_add_exists_unique_input1) + (dst_positive_scale_add_exists_unique_input1))) + (((dst_negative_code_add_exists_unique_input1) + (dst_negative_scale_add_exists_unique_input1)) * S ((dst_negative_code_add_exists_unique_input1) + (dst_negative_scale_add_exists_unique_input1)) + ((dst_negative_scale_add_exists_unique_input1) + (dst_negative_scale_add_exists_unique_input1)))) + ((((dst_negative_code_add_exists_unique_input1) + (dst_negative_scale_add_exists_unique_input1)) * S ((dst_negative_code_add_exists_unique_input1) + (dst_negative_scale_add_exists_unique_input1)) + ((dst_negative_scale_add_exists_unique_input1) + (dst_negative_scale_add_exists_unique_input1))) + (((dst_negative_code_add_exists_unique_input1) + (dst_negative_scale_add_exists_unique_input1)) * S ((dst_negative_code_add_exists_unique_input1) + (dst_negative_scale_add_exists_unique_input1)) + ((dst_negative_scale_add_exists_unique_input1) + (dst_negative_scale_add_exists_unique_input1)))))) /\ (forall dst_index_add_exists_unique_input1. (exists pvs_le_gap_add_exists_unique_input1domain. pvs_le_gap_add_exists_unique_input1domain + (dst_index_add_exists_unique_input1) = (l)) -> exists dst_positive_add_exists_unique_input1 dst_negative_add_exists_unique_input1 dst_value_add_exists_unique_input1. ((((exists ff_h_pvs_add_exists_unique_input1entrypositive. ff_h_pvs_add_exists_unique_input1entrypositive + S (dst_positive_add_exists_unique_input1) = S ((S (dst_index_add_exists_unique_input1)) * dst_positive_scale_add_exists_unique_input1)) /\ exists ff_q_pvs_add_exists_unique_input1entrypositive. dst_positive_code_add_exists_unique_input1 = ff_q_pvs_add_exists_unique_input1entrypositive * S ((S (dst_index_add_exists_unique_input1)) * dst_positive_scale_add_exists_unique_input1) + (dst_positive_add_exists_unique_input1))) /\ (((((exists ff_h_pvs_add_exists_unique_input1entrynegative. ff_h_pvs_add_exists_unique_input1entrynegative + S (dst_negative_add_exists_unique_input1) = S ((S (dst_index_add_exists_unique_input1)) * dst_negative_scale_add_exists_unique_input1)) /\ exists ff_q_pvs_add_exists_unique_input1entrynegative. dst_negative_code_add_exists_unique_input1 = ff_q_pvs_add_exists_unique_input1entrynegative * S ((S (dst_index_add_exists_unique_input1)) * dst_negative_scale_add_exists_unique_input1) + (dst_negative_add_exists_unique_input1))) /\ (exists ge_balance_positive_add_exists_unique_input1entryvalue ge_balance_negative_add_exists_unique_input1entryvalue. (((((dst_value_add_exists_unique_input1) = 2 * (ge_balance_positive_add_exists_unique_input1entryvalue) /\ (ge_balance_negative_add_exists_unique_input1entryvalue) = 0) \/ exists ge_signed_half_add_exists_unique_input1entryvaluedecode. (((dst_value_add_exists_unique_input1) = 2 * ge_signed_half_add_exists_unique_input1entryvaluedecode + 1 /\ (ge_balance_positive_add_exists_unique_input1entryvalue) = 0) /\ (ge_balance_negative_add_exists_unique_input1entryvalue) = S ge_signed_half_add_exists_unique_input1entryvaluedecode))) /\ ((dst_positive_add_exists_unique_input1) + ge_balance_negative_add_exists_unique_input1entryvalue = (dst_negative_add_exists_unique_input1) + ge_balance_positive_add_exists_unique_input1entryvalue))))))))) -> exists H. ((((exists dst_positive_code_add_exists_unique_resultleft_table dst_positive_scale_add_exists_unique_resultleft_table dst_negative_code_add_exists_unique_resultleft_table dst_negative_scale_add_exists_unique_resultleft_table. (((F) = (((((dst_positive_code_add_exists_unique_resultleft_table) + (dst_positive_scale_add_exists_unique_resultleft_table)) * S ((dst_positive_code_add_exists_unique_resultleft_table) + (dst_positive_scale_add_exists_unique_resultleft_table)) + ((dst_positive_scale_add_exists_unique_resultleft_table) + (dst_positive_scale_add_exists_unique_resultleft_table))) + (((dst_negative_code_add_exists_unique_resultleft_table) + (dst_negative_scale_add_exists_unique_resultleft_table)) * S ((dst_negative_code_add_exists_unique_resultleft_table) + (dst_negative_scale_add_exists_unique_resultleft_table)) + ((dst_negative_scale_add_exists_unique_resultleft_table) + (dst_negative_scale_add_exists_unique_resultleft_table)))) * S ((((dst_positive_code_add_exists_unique_resultleft_table) + (dst_positive_scale_add_exists_unique_resultleft_table)) * S ((dst_positive_code_add_exists_unique_resultleft_table) + (dst_positive_scale_add_exists_unique_resultleft_table)) + ((dst_positive_scale_add_exists_unique_resultleft_table) + (dst_positive_scale_add_exists_unique_resultleft_table))) + (((dst_negative_code_add_exists_unique_resultleft_table) + (dst_negative_scale_add_exists_unique_resultleft_table)) * S ((dst_negative_code_add_exists_unique_resultleft_table) + (dst_negative_scale_add_exists_unique_resultleft_table)) + ((dst_negative_scale_add_exists_unique_resultleft_table) + (dst_negative_scale_add_exists_unique_resultleft_table)))) + ((((dst_negative_code_add_exists_unique_resultleft_table) + (dst_negative_scale_add_exists_unique_resultleft_table)) * S ((dst_negative_code_add_exists_unique_resultleft_table) + (dst_negative_scale_add_exists_unique_resultleft_table)) + ((dst_negative_scale_add_exists_unique_resultleft_table) + (dst_negative_scale_add_exists_unique_resultleft_table))) + (((dst_negative_code_add_exists_unique_resultleft_table) + (dst_negative_scale_add_exists_unique_resultleft_table)) * S ((dst_negative_code_add_exists_unique_resultleft_table) + (dst_negative_scale_add_exists_unique_resultleft_table)) + ((dst_negative_scale_add_exists_unique_resultleft_table) + (dst_negative_scale_add_exists_unique_resultleft_table)))))) /\ (forall dst_index_add_exists_unique_resultleft_table. (exists pvs_le_gap_add_exists_unique_resultleft_tabledomain. pvs_le_gap_add_exists_unique_resultleft_tabledomain + (dst_index_add_exists_unique_resultleft_table) = (l)) -> exists dst_positive_add_exists_unique_resultleft_table dst_negative_add_exists_unique_resultleft_table dst_value_add_exists_unique_resultleft_table. ((((exists ff_h_pvs_add_exists_unique_resultleft_tableentrypositive. ff_h_pvs_add_exists_unique_resultleft_tableentrypositive + S (dst_positive_add_exists_unique_resultleft_table) = S ((S (dst_index_add_exists_unique_resultleft_table)) * dst_positive_scale_add_exists_unique_resultleft_table)) /\ exists ff_q_pvs_add_exists_unique_resultleft_tableentrypositive. dst_positive_code_add_exists_unique_resultleft_table = ff_q_pvs_add_exists_unique_resultleft_tableentrypositive * S ((S (dst_index_add_exists_unique_resultleft_table)) * dst_positive_scale_add_exists_unique_resultleft_table) + (dst_positive_add_exists_unique_resultleft_table))) /\ (((((exists ff_h_pvs_add_exists_unique_resultleft_tableentrynegative. ff_h_pvs_add_exists_unique_resultleft_tableentrynegative + S (dst_negative_add_exists_unique_resultleft_table) = S ((S (dst_index_add_exists_unique_resultleft_table)) * dst_negative_scale_add_exists_unique_resultleft_table)) /\ exists ff_q_pvs_add_exists_unique_resultleft_tableentrynegative. dst_negative_code_add_exists_unique_resultleft_table = ff_q_pvs_add_exists_unique_resultleft_tableentrynegative * S ((S (dst_index_add_exists_unique_resultleft_table)) * dst_negative_scale_add_exists_unique_resultleft_table) + (dst_negative_add_exists_unique_resultleft_table))) /\ (exists ge_balance_positive_add_exists_unique_resultleft_tableentryvalue ge_balance_negative_add_exists_unique_resultleft_tableentryvalue. (((((dst_value_add_exists_unique_resultleft_table) = 2 * (ge_balance_positive_add_exists_unique_resultleft_tableentryvalue) /\ (ge_balance_negative_add_exists_unique_resultleft_tableentryvalue) = 0) \/ exists ge_signed_half_add_exists_unique_resultleft_tableentryvaluedecode. (((dst_value_add_exists_unique_resultleft_table) = 2 * ge_signed_half_add_exists_unique_resultleft_tableentryvaluedecode + 1 /\ (ge_balance_positive_add_exists_unique_resultleft_tableentryvalue) = 0) /\ (ge_balance_negative_add_exists_unique_resultleft_tableentryvalue) = S ge_signed_half_add_exists_unique_resultleft_tableentryvaluedecode))) /\ ((dst_positive_add_exists_unique_resultleft_table) + ge_balance_negative_add_exists_unique_resultleft_tableentryvalue = (dst_negative_add_exists_unique_resultleft_table) + ge_balance_positive_add_exists_unique_resultleft_tableentryvalue))))))))) /\ (((exists dst_positive_code_add_exists_unique_resultright_table dst_positive_scale_add_exists_unique_resultright_table dst_negative_code_add_exists_unique_resultright_table dst_negative_scale_add_exists_unique_resultright_table. (((G) = (((((dst_positive_code_add_exists_unique_resultright_table) + (dst_positive_scale_add_exists_unique_resultright_table)) * S ((dst_positive_code_add_exists_unique_resultright_table) + (dst_positive_scale_add_exists_unique_resultright_table)) + ((dst_positive_scale_add_exists_unique_resultright_table) + (dst_positive_scale_add_exists_unique_resultright_table))) + (((dst_negative_code_add_exists_unique_resultright_table) + (dst_negative_scale_add_exists_unique_resultright_table)) * S ((dst_negative_code_add_exists_unique_resultright_table) + (dst_negative_scale_add_exists_unique_resultright_table)) + ((dst_negative_scale_add_exists_unique_resultright_table) + (dst_negative_scale_add_exists_unique_resultright_table)))) * S ((((dst_positive_code_add_exists_unique_resultright_table) + (dst_positive_scale_add_exists_unique_resultright_table)) * S ((dst_positive_code_add_exists_unique_resultright_table) + (dst_positive_scale_add_exists_unique_resultright_table)) + ((dst_positive_scale_add_exists_unique_resultright_table) + (dst_positive_scale_add_exists_unique_resultright_table))) + (((dst_negative_code_add_exists_unique_resultright_table) + (dst_negative_scale_add_exists_unique_resultright_table)) * S ((dst_negative_code_add_exists_unique_resultright_table) + (dst_negative_scale_add_exists_unique_resultright_table)) + ((dst_negative_scale_add_exists_unique_resultright_table) + (dst_negative_scale_add_exists_unique_resultright_table)))) + ((((dst_negative_code_add_exists_unique_resultright_table) + (dst_negative_scale_add_exists_unique_resultright_table)) * S ((dst_negative_code_add_exists_unique_resultright_table) + (dst_negative_scale_add_exists_unique_resultright_table)) + ((dst_negative_scale_add_exists_unique_resultright_table) + (dst_negative_scale_add_exists_unique_resultright_table))) + (((dst_negative_code_add_exists_unique_resultright_table) + (dst_negative_scale_add_exists_unique_resultright_table)) * S ((dst_negative_code_add_exists_unique_resultright_table) + (dst_negative_scale_add_exists_unique_resultright_table)) + ((dst_negative_scale_add_exists_unique_resultright_table) + (dst_negative_scale_add_exists_unique_resultright_table)))))) /\ (forall dst_index_add_exists_unique_resultright_table. (exists pvs_le_gap_add_exists_unique_resultright_tabledomain. pvs_le_gap_add_exists_unique_resultright_tabledomain + (dst_index_add_exists_unique_resultright_table) = (l)) -> exists dst_positive_add_exists_unique_resultright_table dst_negative_add_exists_unique_resultright_table dst_value_add_exists_unique_resultright_table. ((((exists ff_h_pvs_add_exists_unique_resultright_tableentrypositive. ff_h_pvs_add_exists_unique_resultright_tableentrypositive + S (dst_positive_add_exists_unique_resultright_table) = S ((S (dst_index_add_exists_unique_resultright_table)) * dst_positive_scale_add_exists_unique_resultright_table)) /\ exists ff_q_pvs_add_exists_unique_resultright_tableentrypositive. dst_positive_code_add_exists_unique_resultright_table = ff_q_pvs_add_exists_unique_resultright_tableentrypositive * S ((S (dst_index_add_exists_unique_resultright_table)) * dst_positive_scale_add_exists_unique_resultright_table) + (dst_positive_add_exists_unique_resultright_table))) /\ (((((exists ff_h_pvs_add_exists_unique_resultright_tableentrynegative. ff_h_pvs_add_exists_unique_resultright_tableentrynegative + S (dst_negative_add_exists_unique_resultright_table) = S ((S (dst_index_add_exists_unique_resultright_table)) * dst_negative_scale_add_exists_unique_resultright_table)) /\ exists ff_q_pvs_add_exists_unique_resultright_tableentrynegative. dst_negative_code_add_exists_unique_resultright_table = ff_q_pvs_add_exists_unique_resultright_tableentrynegative * S ((S (dst_index_add_exists_unique_resultright_table)) * dst_negative_scale_add_exists_unique_resultright_table) + (dst_negative_add_exists_unique_resultright_table))) /\ (exists ge_balance_positive_add_exists_unique_resultright_tableentryvalue ge_balance_negative_add_exists_unique_resultright_tableentryvalue. (((((dst_value_add_exists_unique_resultright_table) = 2 * (ge_balance_positive_add_exists_unique_resultright_tableentryvalue) /\ (ge_balance_negative_add_exists_unique_resultright_tableentryvalue) = 0) \/ exists ge_signed_half_add_exists_unique_resultright_tableentryvaluedecode. (((dst_value_add_exists_unique_resultright_table) = 2 * ge_signed_half_add_exists_unique_resultright_tableentryvaluedecode + 1 /\ (ge_balance_positive_add_exists_unique_resultright_tableentryvalue) = 0) /\ (ge_balance_negative_add_exists_unique_resultright_tableentryvalue) = S ge_signed_half_add_exists_unique_resultright_tableentryvaluedecode))) /\ ((dst_positive_add_exists_unique_resultright_table) + ge_balance_negative_add_exists_unique_resultright_tableentryvalue = (dst_negative_add_exists_unique_resultright_table) + ge_balance_positive_add_exists_unique_resultright_tableentryvalue))))))))) /\ (((exists dst_positive_code_add_exists_unique_resultoutput_table dst_positive_scale_add_exists_unique_resultoutput_table dst_negative_code_add_exists_unique_resultoutput_table dst_negative_scale_add_exists_unique_resultoutput_table. (((H) = (((((dst_positive_code_add_exists_unique_resultoutput_table) + (dst_positive_scale_add_exists_unique_resultoutput_table)) * S ((dst_positive_code_add_exists_unique_resultoutput_table) + (dst_positive_scale_add_exists_unique_resultoutput_table)) + ((dst_positive_scale_add_exists_unique_resultoutput_table) + (dst_positive_scale_add_exists_unique_resultoutput_table))) + (((dst_negative_code_add_exists_unique_resultoutput_table) + (dst_negative_scale_add_exists_unique_resultoutput_table)) * S ((dst_negative_code_add_exists_unique_resultoutput_table) + (dst_negative_scale_add_exists_unique_resultoutput_table)) + ((dst_negative_scale_add_exists_unique_resultoutput_table) + (dst_negative_scale_add_exists_unique_resultoutput_table)))) * S ((((dst_positive_code_add_exists_unique_resultoutput_table) + (dst_positive_scale_add_exists_unique_resultoutput_table)) * S ((dst_positive_code_add_exists_unique_resultoutput_table) + (dst_positive_scale_add_exists_unique_resultoutput_table)) + ((dst_positive_scale_add_exists_unique_resultoutput_table) + (dst_positive_scale_add_exists_unique_resultoutput_table))) + (((dst_negative_code_add_exists_unique_resultoutput_table) + (dst_negative_scale_add_exists_unique_resultoutput_table)) * S ((dst_negative_code_add_exists_unique_resultoutput_table) + (dst_negative_scale_add_exists_unique_resultoutput_table)) + ((dst_negative_scale_add_exists_unique_resultoutput_table) + (dst_negative_scale_add_exists_unique_resultoutput_table)))) + ((((dst_negative_code_add_exists_unique_resultoutput_table) + (dst_negative_scale_add_exists_unique_resultoutput_table)) * S ((dst_negative_code_add_exists_unique_resultoutput_table) + (dst_negative_scale_add_exists_unique_resultoutput_table)) + ((dst_negative_scale_add_exists_unique_resultoutput_table) + (dst_negative_scale_add_exists_unique_resultoutput_table))) + (((dst_negative_code_add_exists_unique_resultoutput_table) + (dst_negative_scale_add_exists_unique_resultoutput_table)) * S ((dst_negative_code_add_exists_unique_resultoutput_table) + (dst_negative_scale_add_exists_unique_resultoutput_table)) + ((dst_negative_scale_add_exists_unique_resultoutput_table) + (dst_negative_scale_add_exists_unique_resultoutput_table)))))) /\ (forall dst_index_add_exists_unique_resultoutput_table. (exists pvs_le_gap_add_exists_unique_resultoutput_tabledomain. pvs_le_gap_add_exists_unique_resultoutput_tabledomain + (dst_index_add_exists_unique_resultoutput_table) = (l)) -> exists dst_positive_add_exists_unique_resultoutput_table dst_negative_add_exists_unique_resultoutput_table dst_value_add_exists_unique_resultoutput_table. ((((exists ff_h_pvs_add_exists_unique_resultoutput_tableentrypositive. ff_h_pvs_add_exists_unique_resultoutput_tableentrypositive + S (dst_positive_add_exists_unique_resultoutput_table) = S ((S (dst_index_add_exists_unique_resultoutput_table)) * dst_positive_scale_add_exists_unique_resultoutput_table)) /\ exists ff_q_pvs_add_exists_unique_resultoutput_tableentrypositive. dst_positive_code_add_exists_unique_resultoutput_table = ff_q_pvs_add_exists_unique_resultoutput_tableentrypositive * S ((S (dst_index_add_exists_unique_resultoutput_table)) * dst_positive_scale_add_exists_unique_resultoutput_table) + (dst_positive_add_exists_unique_resultoutput_table))) /\ (((((exists ff_h_pvs_add_exists_unique_resultoutput_tableentrynegative. ff_h_pvs_add_exists_unique_resultoutput_tableentrynegative + S (dst_negative_add_exists_unique_resultoutput_table) = S ((S (dst_index_add_exists_unique_resultoutput_table)) * dst_negative_scale_add_exists_unique_resultoutput_table)) /\ exists ff_q_pvs_add_exists_unique_resultoutput_tableentrynegative. dst_negative_code_add_exists_unique_resultoutput_table = ff_q_pvs_add_exists_unique_resultoutput_tableentrynegative * S ((S (dst_index_add_exists_unique_resultoutput_table)) * dst_negative_scale_add_exists_unique_resultoutput_table) + (dst_negative_add_exists_unique_resultoutput_table))) /\ (exists ge_balance_positive_add_exists_unique_resultoutput_tableentryvalue ge_balance_negative_add_exists_unique_resultoutput_tableentryvalue. (((((dst_value_add_exists_unique_resultoutput_table) = 2 * (ge_balance_positive_add_exists_unique_resultoutput_tableentryvalue) /\ (ge_balance_negative_add_exists_unique_resultoutput_tableentryvalue) = 0) \/ exists ge_signed_half_add_exists_unique_resultoutput_tableentryvaluedecode. (((dst_value_add_exists_unique_resultoutput_table) = 2 * ge_signed_half_add_exists_unique_resultoutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_add_exists_unique_resultoutput_tableentryvalue) = 0) /\ (ge_balance_negative_add_exists_unique_resultoutput_tableentryvalue) = S ge_signed_half_add_exists_unique_resultoutput_tableentryvaluedecode))) /\ ((dst_positive_add_exists_unique_resultoutput_table) + ge_balance_negative_add_exists_unique_resultoutput_tableentryvalue = (dst_negative_add_exists_unique_resultoutput_table) + ge_balance_positive_add_exists_unique_resultoutput_tableentryvalue))))))))) /\ (forall sto_index_add_exists_unique_resultentries. (exists pvs_gap_add_exists_unique_resultentriesbound. pvs_gap_add_exists_unique_resultentriesbound + S (sto_index_add_exists_unique_resultentries) = (l)) -> exists sto_left_add_exists_unique_resultentries sto_right_add_exists_unique_resultentries sto_output_add_exists_unique_resultentries. ((exists dst_positive_code_add_exists_unique_resultentriesentryleft dst_positive_scale_add_exists_unique_resultentriesentryleft dst_negative_code_add_exists_unique_resultentriesentryleft dst_negative_scale_add_exists_unique_resultentriesentryleft dst_positive_add_exists_unique_resultentriesentryleft dst_negative_add_exists_unique_resultentriesentryleft. (((F) = (((((dst_positive_code_add_exists_unique_resultentriesentryleft) + (dst_positive_scale_add_exists_unique_resultentriesentryleft)) * S ((dst_positive_code_add_exists_unique_resultentriesentryleft) + (dst_positive_scale_add_exists_unique_resultentriesentryleft)) + ((dst_positive_scale_add_exists_unique_resultentriesentryleft) + (dst_positive_scale_add_exists_unique_resultentriesentryleft))) + (((dst_negative_code_add_exists_unique_resultentriesentryleft) + (dst_negative_scale_add_exists_unique_resultentriesentryleft)) * S ((dst_negative_code_add_exists_unique_resultentriesentryleft) + (dst_negative_scale_add_exists_unique_resultentriesentryleft)) + ((dst_negative_scale_add_exists_unique_resultentriesentryleft) + (dst_negative_scale_add_exists_unique_resultentriesentryleft)))) * S ((((dst_positive_code_add_exists_unique_resultentriesentryleft) + (dst_positive_scale_add_exists_unique_resultentriesentryleft)) * S ((dst_positive_code_add_exists_unique_resultentriesentryleft) + (dst_positive_scale_add_exists_unique_resultentriesentryleft)) + ((dst_positive_scale_add_exists_unique_resultentriesentryleft) + (dst_positive_scale_add_exists_unique_resultentriesentryleft))) + (((dst_negative_code_add_exists_unique_resultentriesentryleft) + (dst_negative_scale_add_exists_unique_resultentriesentryleft)) * S ((dst_negative_code_add_exists_unique_resultentriesentryleft) + (dst_negative_scale_add_exists_unique_resultentriesentryleft)) + ((dst_negative_scale_add_exists_unique_resultentriesentryleft) + (dst_negative_scale_add_exists_unique_resultentriesentryleft)))) + ((((dst_negative_code_add_exists_unique_resultentriesentryleft) + (dst_negative_scale_add_exists_unique_resultentriesentryleft)) * S ((dst_negative_code_add_exists_unique_resultentriesentryleft) + (dst_negative_scale_add_exists_unique_resultentriesentryleft)) + ((dst_negative_scale_add_exists_unique_resultentriesentryleft) + (dst_negative_scale_add_exists_unique_resultentriesentryleft))) + (((dst_negative_code_add_exists_unique_resultentriesentryleft) + (dst_negative_scale_add_exists_unique_resultentriesentryleft)) * S ((dst_negative_code_add_exists_unique_resultentriesentryleft) + (dst_negative_scale_add_exists_unique_resultentriesentryleft)) + ((dst_negative_scale_add_exists_unique_resultentriesentryleft) + (dst_negative_scale_add_exists_unique_resultentriesentryleft)))))) /\ (((((exists ff_h_pvs_add_exists_unique_resultentriesentryleftpositive. ff_h_pvs_add_exists_unique_resultentriesentryleftpositive + S (dst_positive_add_exists_unique_resultentriesentryleft) = S ((S (sto_index_add_exists_unique_resultentries)) * dst_positive_scale_add_exists_unique_resultentriesentryleft)) /\ exists ff_q_pvs_add_exists_unique_resultentriesentryleftpositive. dst_positive_code_add_exists_unique_resultentriesentryleft = ff_q_pvs_add_exists_unique_resultentriesentryleftpositive * S ((S (sto_index_add_exists_unique_resultentries)) * dst_positive_scale_add_exists_unique_resultentriesentryleft) + (dst_positive_add_exists_unique_resultentriesentryleft))) /\ (((((exists ff_h_pvs_add_exists_unique_resultentriesentryleftnegative. ff_h_pvs_add_exists_unique_resultentriesentryleftnegative + S (dst_negative_add_exists_unique_resultentriesentryleft) = S ((S (sto_index_add_exists_unique_resultentries)) * dst_negative_scale_add_exists_unique_resultentriesentryleft)) /\ exists ff_q_pvs_add_exists_unique_resultentriesentryleftnegative. dst_negative_code_add_exists_unique_resultentriesentryleft = ff_q_pvs_add_exists_unique_resultentriesentryleftnegative * S ((S (sto_index_add_exists_unique_resultentries)) * dst_negative_scale_add_exists_unique_resultentriesentryleft) + (dst_negative_add_exists_unique_resultentriesentryleft))) /\ (exists ge_balance_positive_add_exists_unique_resultentriesentryleftvalue ge_balance_negative_add_exists_unique_resultentriesentryleftvalue. (((((sto_left_add_exists_unique_resultentries) = 2 * (ge_balance_positive_add_exists_unique_resultentriesentryleftvalue) /\ (ge_balance_negative_add_exists_unique_resultentriesentryleftvalue) = 0) \/ exists ge_signed_half_add_exists_unique_resultentriesentryleftvaluedecode. (((sto_left_add_exists_unique_resultentries) = 2 * ge_signed_half_add_exists_unique_resultentriesentryleftvaluedecode + 1 /\ (ge_balance_positive_add_exists_unique_resultentriesentryleftvalue) = 0) /\ (ge_balance_negative_add_exists_unique_resultentriesentryleftvalue) = S ge_signed_half_add_exists_unique_resultentriesentryleftvaluedecode))) /\ ((dst_positive_add_exists_unique_resultentriesentryleft) + ge_balance_negative_add_exists_unique_resultentriesentryleftvalue = (dst_negative_add_exists_unique_resultentriesentryleft) + ge_balance_positive_add_exists_unique_resultentriesentryleftvalue))))))))) /\ (((exists dst_positive_code_add_exists_unique_resultentriesentryright dst_positive_scale_add_exists_unique_resultentriesentryright dst_negative_code_add_exists_unique_resultentriesentryright dst_negative_scale_add_exists_unique_resultentriesentryright dst_positive_add_exists_unique_resultentriesentryright dst_negative_add_exists_unique_resultentriesentryright. (((G) = (((((dst_positive_code_add_exists_unique_resultentriesentryright) + (dst_positive_scale_add_exists_unique_resultentriesentryright)) * S ((dst_positive_code_add_exists_unique_resultentriesentryright) + (dst_positive_scale_add_exists_unique_resultentriesentryright)) + ((dst_positive_scale_add_exists_unique_resultentriesentryright) + (dst_positive_scale_add_exists_unique_resultentriesentryright))) + (((dst_negative_code_add_exists_unique_resultentriesentryright) + (dst_negative_scale_add_exists_unique_resultentriesentryright)) * S ((dst_negative_code_add_exists_unique_resultentriesentryright) + (dst_negative_scale_add_exists_unique_resultentriesentryright)) + ((dst_negative_scale_add_exists_unique_resultentriesentryright) + (dst_negative_scale_add_exists_unique_resultentriesentryright)))) * S ((((dst_positive_code_add_exists_unique_resultentriesentryright) + (dst_positive_scale_add_exists_unique_resultentriesentryright)) * S ((dst_positive_code_add_exists_unique_resultentriesentryright) + (dst_positive_scale_add_exists_unique_resultentriesentryright)) + ((dst_positive_scale_add_exists_unique_resultentriesentryright) + (dst_positive_scale_add_exists_unique_resultentriesentryright))) + (((dst_negative_code_add_exists_unique_resultentriesentryright) + (dst_negative_scale_add_exists_unique_resultentriesentryright)) * S ((dst_negative_code_add_exists_unique_resultentriesentryright) + (dst_negative_scale_add_exists_unique_resultentriesentryright)) + ((dst_negative_scale_add_exists_unique_resultentriesentryright) + (dst_negative_scale_add_exists_unique_resultentriesentryright)))) + ((((dst_negative_code_add_exists_unique_resultentriesentryright) + (dst_negative_scale_add_exists_unique_resultentriesentryright)) * S ((dst_negative_code_add_exists_unique_resultentriesentryright) + (dst_negative_scale_add_exists_unique_resultentriesentryright)) + ((dst_negative_scale_add_exists_unique_resultentriesentryright) + (dst_negative_scale_add_exists_unique_resultentriesentryright))) + (((dst_negative_code_add_exists_unique_resultentriesentryright) + (dst_negative_scale_add_exists_unique_resultentriesentryright)) * S ((dst_negative_code_add_exists_unique_resultentriesentryright) + (dst_negative_scale_add_exists_unique_resultentriesentryright)) + ((dst_negative_scale_add_exists_unique_resultentriesentryright) + (dst_negative_scale_add_exists_unique_resultentriesentryright)))))) /\ (((((exists ff_h_pvs_add_exists_unique_resultentriesentryrightpositive. ff_h_pvs_add_exists_unique_resultentriesentryrightpositive + S (dst_positive_add_exists_unique_resultentriesentryright) = S ((S (sto_index_add_exists_unique_resultentries)) * dst_positive_scale_add_exists_unique_resultentriesentryright)) /\ exists ff_q_pvs_add_exists_unique_resultentriesentryrightpositive. dst_positive_code_add_exists_unique_resultentriesentryright = ff_q_pvs_add_exists_unique_resultentriesentryrightpositive * S ((S (sto_index_add_exists_unique_resultentries)) * dst_positive_scale_add_exists_unique_resultentriesentryright) + (dst_positive_add_exists_unique_resultentriesentryright))) /\ (((((exists ff_h_pvs_add_exists_unique_resultentriesentryrightnegative. ff_h_pvs_add_exists_unique_resultentriesentryrightnegative + S (dst_negative_add_exists_unique_resultentriesentryright) = S ((S (sto_index_add_exists_unique_resultentries)) * dst_negative_scale_add_exists_unique_resultentriesentryright)) /\ exists ff_q_pvs_add_exists_unique_resultentriesentryrightnegative. dst_negative_code_add_exists_unique_resultentriesentryright = ff_q_pvs_add_exists_unique_resultentriesentryrightnegative * S ((S (sto_index_add_exists_unique_resultentries)) * dst_negative_scale_add_exists_unique_resultentriesentryright) + (dst_negative_add_exists_unique_resultentriesentryright))) /\ (exists ge_balance_positive_add_exists_unique_resultentriesentryrightvalue ge_balance_negative_add_exists_unique_resultentriesentryrightvalue. (((((sto_right_add_exists_unique_resultentries) = 2 * (ge_balance_positive_add_exists_unique_resultentriesentryrightvalue) /\ (ge_balance_negative_add_exists_unique_resultentriesentryrightvalue) = 0) \/ exists ge_signed_half_add_exists_unique_resultentriesentryrightvaluedecode. (((sto_right_add_exists_unique_resultentries) = 2 * ge_signed_half_add_exists_unique_resultentriesentryrightvaluedecode + 1 /\ (ge_balance_positive_add_exists_unique_resultentriesentryrightvalue) = 0) /\ (ge_balance_negative_add_exists_unique_resultentriesentryrightvalue) = S ge_signed_half_add_exists_unique_resultentriesentryrightvaluedecode))) /\ ((dst_positive_add_exists_unique_resultentriesentryright) + ge_balance_negative_add_exists_unique_resultentriesentryrightvalue = (dst_negative_add_exists_unique_resultentriesentryright) + ge_balance_positive_add_exists_unique_resultentriesentryrightvalue))))))))) /\ (((exists dst_positive_code_add_exists_unique_resultentriesentryoutput dst_positive_scale_add_exists_unique_resultentriesentryoutput dst_negative_code_add_exists_unique_resultentriesentryoutput dst_negative_scale_add_exists_unique_resultentriesentryoutput dst_positive_add_exists_unique_resultentriesentryoutput dst_negative_add_exists_unique_resultentriesentryoutput. (((H) = (((((dst_positive_code_add_exists_unique_resultentriesentryoutput) + (dst_positive_scale_add_exists_unique_resultentriesentryoutput)) * S ((dst_positive_code_add_exists_unique_resultentriesentryoutput) + (dst_positive_scale_add_exists_unique_resultentriesentryoutput)) + ((dst_positive_scale_add_exists_unique_resultentriesentryoutput) + (dst_positive_scale_add_exists_unique_resultentriesentryoutput))) + (((dst_negative_code_add_exists_unique_resultentriesentryoutput) + (dst_negative_scale_add_exists_unique_resultentriesentryoutput)) * S ((dst_negative_code_add_exists_unique_resultentriesentryoutput) + (dst_negative_scale_add_exists_unique_resultentriesentryoutput)) + ((dst_negative_scale_add_exists_unique_resultentriesentryoutput) + (dst_negative_scale_add_exists_unique_resultentriesentryoutput)))) * S ((((dst_positive_code_add_exists_unique_resultentriesentryoutput) + (dst_positive_scale_add_exists_unique_resultentriesentryoutput)) * S ((dst_positive_code_add_exists_unique_resultentriesentryoutput) + (dst_positive_scale_add_exists_unique_resultentriesentryoutput)) + ((dst_positive_scale_add_exists_unique_resultentriesentryoutput) + (dst_positive_scale_add_exists_unique_resultentriesentryoutput))) + (((dst_negative_code_add_exists_unique_resultentriesentryoutput) + (dst_negative_scale_add_exists_unique_resultentriesentryoutput)) * S ((dst_negative_code_add_exists_unique_resultentriesentryoutput) + (dst_negative_scale_add_exists_unique_resultentriesentryoutput)) + ((dst_negative_scale_add_exists_unique_resultentriesentryoutput) + (dst_negative_scale_add_exists_unique_resultentriesentryoutput)))) + ((((dst_negative_code_add_exists_unique_resultentriesentryoutput) + (dst_negative_scale_add_exists_unique_resultentriesentryoutput)) * S ((dst_negative_code_add_exists_unique_resultentriesentryoutput) + (dst_negative_scale_add_exists_unique_resultentriesentryoutput)) + ((dst_negative_scale_add_exists_unique_resultentriesentryoutput) + (dst_negative_scale_add_exists_unique_resultentriesentryoutput))) + (((dst_negative_code_add_exists_unique_resultentriesentryoutput) + (dst_negative_scale_add_exists_unique_resultentriesentryoutput)) * S ((dst_negative_code_add_exists_unique_resultentriesentryoutput) + (dst_negative_scale_add_exists_unique_resultentriesentryoutput)) + ((dst_negative_scale_add_exists_unique_resultentriesentryoutput) + (dst_negative_scale_add_exists_unique_resultentriesentryoutput)))))) /\ (((((exists ff_h_pvs_add_exists_unique_resultentriesentryoutputpositive. ff_h_pvs_add_exists_unique_resultentriesentryoutputpositive + S (dst_positive_add_exists_unique_resultentriesentryoutput) = S ((S (sto_index_add_exists_unique_resultentries)) * dst_positive_scale_add_exists_unique_resultentriesentryoutput)) /\ exists ff_q_pvs_add_exists_unique_resultentriesentryoutputpositive. dst_positive_code_add_exists_unique_resultentriesentryoutput = ff_q_pvs_add_exists_unique_resultentriesentryoutputpositive * S ((S (sto_index_add_exists_unique_resultentries)) * dst_positive_scale_add_exists_unique_resultentriesentryoutput) + (dst_positive_add_exists_unique_resultentriesentryoutput))) /\ (((((exists ff_h_pvs_add_exists_unique_resultentriesentryoutputnegative. ff_h_pvs_add_exists_unique_resultentriesentryoutputnegative + S (dst_negative_add_exists_unique_resultentriesentryoutput) = S ((S (sto_index_add_exists_unique_resultentries)) * dst_negative_scale_add_exists_unique_resultentriesentryoutput)) /\ exists ff_q_pvs_add_exists_unique_resultentriesentryoutputnegative. dst_negative_code_add_exists_unique_resultentriesentryoutput = ff_q_pvs_add_exists_unique_resultentriesentryoutputnegative * S ((S (sto_index_add_exists_unique_resultentries)) * dst_negative_scale_add_exists_unique_resultentriesentryoutput) + (dst_negative_add_exists_unique_resultentriesentryoutput))) /\ (exists ge_balance_positive_add_exists_unique_resultentriesentryoutputvalue ge_balance_negative_add_exists_unique_resultentriesentryoutputvalue. (((((sto_output_add_exists_unique_resultentries) = 2 * (ge_balance_positive_add_exists_unique_resultentriesentryoutputvalue) /\ (ge_balance_negative_add_exists_unique_resultentriesentryoutputvalue) = 0) \/ exists ge_signed_half_add_exists_unique_resultentriesentryoutputvaluedecode. (((sto_output_add_exists_unique_resultentries) = 2 * ge_signed_half_add_exists_unique_resultentriesentryoutputvaluedecode + 1 /\ (ge_balance_positive_add_exists_unique_resultentriesentryoutputvalue) = 0) /\ (ge_balance_negative_add_exists_unique_resultentriesentryoutputvalue) = S ge_signed_half_add_exists_unique_resultentriesentryoutputvaluedecode))) /\ ((dst_positive_add_exists_unique_resultentriesentryoutput) + ge_balance_negative_add_exists_unique_resultentriesentryoutputvalue = (dst_negative_add_exists_unique_resultentriesentryoutput) + ge_balance_positive_add_exists_unique_resultentriesentryoutputvalue))))))))) /\ (exists dsa_ap_add_exists_unique_resultentriesentryoperation dsa_an_add_exists_unique_resultentriesentryoperation dsa_bp_add_exists_unique_resultentriesentryoperation dsa_bn_add_exists_unique_resultentriesentryoperation dsa_cp_add_exists_unique_resultentriesentryoperation dsa_cn_add_exists_unique_resultentriesentryoperation. (((((sto_left_add_exists_unique_resultentries) = 2 * (dsa_ap_add_exists_unique_resultentriesentryoperation) /\ (dsa_an_add_exists_unique_resultentriesentryoperation) = 0) \/ exists ge_signed_half_add_exists_unique_resultentriesentryoperationleft. (((sto_left_add_exists_unique_resultentries) = 2 * ge_signed_half_add_exists_unique_resultentriesentryoperationleft + 1 /\ (dsa_ap_add_exists_unique_resultentriesentryoperation) = 0) /\ (dsa_an_add_exists_unique_resultentriesentryoperation) = S ge_signed_half_add_exists_unique_resultentriesentryoperationleft))) /\ ((((((sto_right_add_exists_unique_resultentries) = 2 * (dsa_bp_add_exists_unique_resultentriesentryoperation) /\ (dsa_bn_add_exists_unique_resultentriesentryoperation) = 0) \/ exists ge_signed_half_add_exists_unique_resultentriesentryoperationright. (((sto_right_add_exists_unique_resultentries) = 2 * ge_signed_half_add_exists_unique_resultentriesentryoperationright + 1 /\ (dsa_bp_add_exists_unique_resultentriesentryoperation) = 0) /\ (dsa_bn_add_exists_unique_resultentriesentryoperation) = S ge_signed_half_add_exists_unique_resultentriesentryoperationright))) /\ ((((((sto_output_add_exists_unique_resultentries) = 2 * (dsa_cp_add_exists_unique_resultentriesentryoperation) /\ (dsa_cn_add_exists_unique_resultentriesentryoperation) = 0) \/ exists ge_signed_half_add_exists_unique_resultentriesentryoperationoutput. (((sto_output_add_exists_unique_resultentries) = 2 * ge_signed_half_add_exists_unique_resultentriesentryoperationoutput + 1 /\ (dsa_cp_add_exists_unique_resultentriesentryoperation) = 0) /\ (dsa_cn_add_exists_unique_resultentriesentryoperation) = S ge_signed_half_add_exists_unique_resultentriesentryoperationoutput))) /\ ((dsa_ap_add_exists_unique_resultentriesentryoperation + dsa_bp_add_exists_unique_resultentriesentryoperation) + dsa_cn_add_exists_unique_resultentriesentryoperation = (dsa_an_add_exists_unique_resultentriesentryoperation + dsa_bn_add_exists_unique_resultentriesentryoperation) + dsa_cp_add_exists_unique_resultentriesentryoperation))))))))))))))))))) /\ (forall K. (((exists dst_positive_code_add_exists_unique_otherleft_table dst_positive_scale_add_exists_unique_otherleft_table dst_negative_code_add_exists_unique_otherleft_table dst_negative_scale_add_exists_unique_otherleft_table. (((F) = (((((dst_positive_code_add_exists_unique_otherleft_table) + (dst_positive_scale_add_exists_unique_otherleft_table)) * S ((dst_positive_code_add_exists_unique_otherleft_table) + (dst_positive_scale_add_exists_unique_otherleft_table)) + ((dst_positive_scale_add_exists_unique_otherleft_table) + (dst_positive_scale_add_exists_unique_otherleft_table))) + (((dst_negative_code_add_exists_unique_otherleft_table) + (dst_negative_scale_add_exists_unique_otherleft_table)) * S ((dst_negative_code_add_exists_unique_otherleft_table) + (dst_negative_scale_add_exists_unique_otherleft_table)) + ((dst_negative_scale_add_exists_unique_otherleft_table) + (dst_negative_scale_add_exists_unique_otherleft_table)))) * S ((((dst_positive_code_add_exists_unique_otherleft_table) + (dst_positive_scale_add_exists_unique_otherleft_table)) * S ((dst_positive_code_add_exists_unique_otherleft_table) + (dst_positive_scale_add_exists_unique_otherleft_table)) + ((dst_positive_scale_add_exists_unique_otherleft_table) + (dst_positive_scale_add_exists_unique_otherleft_table))) + (((dst_negative_code_add_exists_unique_otherleft_table) + (dst_negative_scale_add_exists_unique_otherleft_table)) * S ((dst_negative_code_add_exists_unique_otherleft_table) + (dst_negative_scale_add_exists_unique_otherleft_table)) + ((dst_negative_scale_add_exists_unique_otherleft_table) + (dst_negative_scale_add_exists_unique_otherleft_table)))) + ((((dst_negative_code_add_exists_unique_otherleft_table) + (dst_negative_scale_add_exists_unique_otherleft_table)) * S ((dst_negative_code_add_exists_unique_otherleft_table) + (dst_negative_scale_add_exists_unique_otherleft_table)) + ((dst_negative_scale_add_exists_unique_otherleft_table) + (dst_negative_scale_add_exists_unique_otherleft_table))) + (((dst_negative_code_add_exists_unique_otherleft_table) + (dst_negative_scale_add_exists_unique_otherleft_table)) * S ((dst_negative_code_add_exists_unique_otherleft_table) + (dst_negative_scale_add_exists_unique_otherleft_table)) + ((dst_negative_scale_add_exists_unique_otherleft_table) + (dst_negative_scale_add_exists_unique_otherleft_table)))))) /\ (forall dst_index_add_exists_unique_otherleft_table. (exists pvs_le_gap_add_exists_unique_otherleft_tabledomain. pvs_le_gap_add_exists_unique_otherleft_tabledomain + (dst_index_add_exists_unique_otherleft_table) = (l)) -> exists dst_positive_add_exists_unique_otherleft_table dst_negative_add_exists_unique_otherleft_table dst_value_add_exists_unique_otherleft_table. ((((exists ff_h_pvs_add_exists_unique_otherleft_tableentrypositive. ff_h_pvs_add_exists_unique_otherleft_tableentrypositive + S (dst_positive_add_exists_unique_otherleft_table) = S ((S (dst_index_add_exists_unique_otherleft_table)) * dst_positive_scale_add_exists_unique_otherleft_table)) /\ exists ff_q_pvs_add_exists_unique_otherleft_tableentrypositive. dst_positive_code_add_exists_unique_otherleft_table = ff_q_pvs_add_exists_unique_otherleft_tableentrypositive * S ((S (dst_index_add_exists_unique_otherleft_table)) * dst_positive_scale_add_exists_unique_otherleft_table) + (dst_positive_add_exists_unique_otherleft_table))) /\ (((((exists ff_h_pvs_add_exists_unique_otherleft_tableentrynegative. ff_h_pvs_add_exists_unique_otherleft_tableentrynegative + S (dst_negative_add_exists_unique_otherleft_table) = S ((S (dst_index_add_exists_unique_otherleft_table)) * dst_negative_scale_add_exists_unique_otherleft_table)) /\ exists ff_q_pvs_add_exists_unique_otherleft_tableentrynegative. dst_negative_code_add_exists_unique_otherleft_table = ff_q_pvs_add_exists_unique_otherleft_tableentrynegative * S ((S (dst_index_add_exists_unique_otherleft_table)) * dst_negative_scale_add_exists_unique_otherleft_table) + (dst_negative_add_exists_unique_otherleft_table))) /\ (exists ge_balance_positive_add_exists_unique_otherleft_tableentryvalue ge_balance_negative_add_exists_unique_otherleft_tableentryvalue. (((((dst_value_add_exists_unique_otherleft_table) = 2 * (ge_balance_positive_add_exists_unique_otherleft_tableentryvalue) /\ (ge_balance_negative_add_exists_unique_otherleft_tableentryvalue) = 0) \/ exists ge_signed_half_add_exists_unique_otherleft_tableentryvaluedecode. (((dst_value_add_exists_unique_otherleft_table) = 2 * ge_signed_half_add_exists_unique_otherleft_tableentryvaluedecode + 1 /\ (ge_balance_positive_add_exists_unique_otherleft_tableentryvalue) = 0) /\ (ge_balance_negative_add_exists_unique_otherleft_tableentryvalue) = S ge_signed_half_add_exists_unique_otherleft_tableentryvaluedecode))) /\ ((dst_positive_add_exists_unique_otherleft_table) + ge_balance_negative_add_exists_unique_otherleft_tableentryvalue = (dst_negative_add_exists_unique_otherleft_table) + ge_balance_positive_add_exists_unique_otherleft_tableentryvalue))))))))) /\ (((exists dst_positive_code_add_exists_unique_otherright_table dst_positive_scale_add_exists_unique_otherright_table dst_negative_code_add_exists_unique_otherright_table dst_negative_scale_add_exists_unique_otherright_table. (((G) = (((((dst_positive_code_add_exists_unique_otherright_table) + (dst_positive_scale_add_exists_unique_otherright_table)) * S ((dst_positive_code_add_exists_unique_otherright_table) + (dst_positive_scale_add_exists_unique_otherright_table)) + ((dst_positive_scale_add_exists_unique_otherright_table) + (dst_positive_scale_add_exists_unique_otherright_table))) + (((dst_negative_code_add_exists_unique_otherright_table) + (dst_negative_scale_add_exists_unique_otherright_table)) * S ((dst_negative_code_add_exists_unique_otherright_table) + (dst_negative_scale_add_exists_unique_otherright_table)) + ((dst_negative_scale_add_exists_unique_otherright_table) + (dst_negative_scale_add_exists_unique_otherright_table)))) * S ((((dst_positive_code_add_exists_unique_otherright_table) + (dst_positive_scale_add_exists_unique_otherright_table)) * S ((dst_positive_code_add_exists_unique_otherright_table) + (dst_positive_scale_add_exists_unique_otherright_table)) + ((dst_positive_scale_add_exists_unique_otherright_table) + (dst_positive_scale_add_exists_unique_otherright_table))) + (((dst_negative_code_add_exists_unique_otherright_table) + (dst_negative_scale_add_exists_unique_otherright_table)) * S ((dst_negative_code_add_exists_unique_otherright_table) + (dst_negative_scale_add_exists_unique_otherright_table)) + ((dst_negative_scale_add_exists_unique_otherright_table) + (dst_negative_scale_add_exists_unique_otherright_table)))) + ((((dst_negative_code_add_exists_unique_otherright_table) + (dst_negative_scale_add_exists_unique_otherright_table)) * S ((dst_negative_code_add_exists_unique_otherright_table) + (dst_negative_scale_add_exists_unique_otherright_table)) + ((dst_negative_scale_add_exists_unique_otherright_table) + (dst_negative_scale_add_exists_unique_otherright_table))) + (((dst_negative_code_add_exists_unique_otherright_table) + (dst_negative_scale_add_exists_unique_otherright_table)) * S ((dst_negative_code_add_exists_unique_otherright_table) + (dst_negative_scale_add_exists_unique_otherright_table)) + ((dst_negative_scale_add_exists_unique_otherright_table) + (dst_negative_scale_add_exists_unique_otherright_table)))))) /\ (forall dst_index_add_exists_unique_otherright_table. (exists pvs_le_gap_add_exists_unique_otherright_tabledomain. pvs_le_gap_add_exists_unique_otherright_tabledomain + (dst_index_add_exists_unique_otherright_table) = (l)) -> exists dst_positive_add_exists_unique_otherright_table dst_negative_add_exists_unique_otherright_table dst_value_add_exists_unique_otherright_table. ((((exists ff_h_pvs_add_exists_unique_otherright_tableentrypositive. ff_h_pvs_add_exists_unique_otherright_tableentrypositive + S (dst_positive_add_exists_unique_otherright_table) = S ((S (dst_index_add_exists_unique_otherright_table)) * dst_positive_scale_add_exists_unique_otherright_table)) /\ exists ff_q_pvs_add_exists_unique_otherright_tableentrypositive. dst_positive_code_add_exists_unique_otherright_table = ff_q_pvs_add_exists_unique_otherright_tableentrypositive * S ((S (dst_index_add_exists_unique_otherright_table)) * dst_positive_scale_add_exists_unique_otherright_table) + (dst_positive_add_exists_unique_otherright_table))) /\ (((((exists ff_h_pvs_add_exists_unique_otherright_tableentrynegative. ff_h_pvs_add_exists_unique_otherright_tableentrynegative + S (dst_negative_add_exists_unique_otherright_table) = S ((S (dst_index_add_exists_unique_otherright_table)) * dst_negative_scale_add_exists_unique_otherright_table)) /\ exists ff_q_pvs_add_exists_unique_otherright_tableentrynegative. dst_negative_code_add_exists_unique_otherright_table = ff_q_pvs_add_exists_unique_otherright_tableentrynegative * S ((S (dst_index_add_exists_unique_otherright_table)) * dst_negative_scale_add_exists_unique_otherright_table) + (dst_negative_add_exists_unique_otherright_table))) /\ (exists ge_balance_positive_add_exists_unique_otherright_tableentryvalue ge_balance_negative_add_exists_unique_otherright_tableentryvalue. (((((dst_value_add_exists_unique_otherright_table) = 2 * (ge_balance_positive_add_exists_unique_otherright_tableentryvalue) /\ (ge_balance_negative_add_exists_unique_otherright_tableentryvalue) = 0) \/ exists ge_signed_half_add_exists_unique_otherright_tableentryvaluedecode. (((dst_value_add_exists_unique_otherright_table) = 2 * ge_signed_half_add_exists_unique_otherright_tableentryvaluedecode + 1 /\ (ge_balance_positive_add_exists_unique_otherright_tableentryvalue) = 0) /\ (ge_balance_negative_add_exists_unique_otherright_tableentryvalue) = S ge_signed_half_add_exists_unique_otherright_tableentryvaluedecode))) /\ ((dst_positive_add_exists_unique_otherright_table) + ge_balance_negative_add_exists_unique_otherright_tableentryvalue = (dst_negative_add_exists_unique_otherright_table) + ge_balance_positive_add_exists_unique_otherright_tableentryvalue))))))))) /\ (((exists dst_positive_code_add_exists_unique_otheroutput_table dst_positive_scale_add_exists_unique_otheroutput_table dst_negative_code_add_exists_unique_otheroutput_table dst_negative_scale_add_exists_unique_otheroutput_table. (((K) = (((((dst_positive_code_add_exists_unique_otheroutput_table) + (dst_positive_scale_add_exists_unique_otheroutput_table)) * S ((dst_positive_code_add_exists_unique_otheroutput_table) + (dst_positive_scale_add_exists_unique_otheroutput_table)) + ((dst_positive_scale_add_exists_unique_otheroutput_table) + (dst_positive_scale_add_exists_unique_otheroutput_table))) + (((dst_negative_code_add_exists_unique_otheroutput_table) + (dst_negative_scale_add_exists_unique_otheroutput_table)) * S ((dst_negative_code_add_exists_unique_otheroutput_table) + (dst_negative_scale_add_exists_unique_otheroutput_table)) + ((dst_negative_scale_add_exists_unique_otheroutput_table) + (dst_negative_scale_add_exists_unique_otheroutput_table)))) * S ((((dst_positive_code_add_exists_unique_otheroutput_table) + (dst_positive_scale_add_exists_unique_otheroutput_table)) * S ((dst_positive_code_add_exists_unique_otheroutput_table) + (dst_positive_scale_add_exists_unique_otheroutput_table)) + ((dst_positive_scale_add_exists_unique_otheroutput_table) + (dst_positive_scale_add_exists_unique_otheroutput_table))) + (((dst_negative_code_add_exists_unique_otheroutput_table) + (dst_negative_scale_add_exists_unique_otheroutput_table)) * S ((dst_negative_code_add_exists_unique_otheroutput_table) + (dst_negative_scale_add_exists_unique_otheroutput_table)) + ((dst_negative_scale_add_exists_unique_otheroutput_table) + (dst_negative_scale_add_exists_unique_otheroutput_table)))) + ((((dst_negative_code_add_exists_unique_otheroutput_table) + (dst_negative_scale_add_exists_unique_otheroutput_table)) * S ((dst_negative_code_add_exists_unique_otheroutput_table) + (dst_negative_scale_add_exists_unique_otheroutput_table)) + ((dst_negative_scale_add_exists_unique_otheroutput_table) + (dst_negative_scale_add_exists_unique_otheroutput_table))) + (((dst_negative_code_add_exists_unique_otheroutput_table) + (dst_negative_scale_add_exists_unique_otheroutput_table)) * S ((dst_negative_code_add_exists_unique_otheroutput_table) + (dst_negative_scale_add_exists_unique_otheroutput_table)) + ((dst_negative_scale_add_exists_unique_otheroutput_table) + (dst_negative_scale_add_exists_unique_otheroutput_table)))))) /\ (forall dst_index_add_exists_unique_otheroutput_table. (exists pvs_le_gap_add_exists_unique_otheroutput_tabledomain. pvs_le_gap_add_exists_unique_otheroutput_tabledomain + (dst_index_add_exists_unique_otheroutput_table) = (l)) -> exists dst_positive_add_exists_unique_otheroutput_table dst_negative_add_exists_unique_otheroutput_table dst_value_add_exists_unique_otheroutput_table. ((((exists ff_h_pvs_add_exists_unique_otheroutput_tableentrypositive. ff_h_pvs_add_exists_unique_otheroutput_tableentrypositive + S (dst_positive_add_exists_unique_otheroutput_table) = S ((S (dst_index_add_exists_unique_otheroutput_table)) * dst_positive_scale_add_exists_unique_otheroutput_table)) /\ exists ff_q_pvs_add_exists_unique_otheroutput_tableentrypositive. dst_positive_code_add_exists_unique_otheroutput_table = ff_q_pvs_add_exists_unique_otheroutput_tableentrypositive * S ((S (dst_index_add_exists_unique_otheroutput_table)) * dst_positive_scale_add_exists_unique_otheroutput_table) + (dst_positive_add_exists_unique_otheroutput_table))) /\ (((((exists ff_h_pvs_add_exists_unique_otheroutput_tableentrynegative. ff_h_pvs_add_exists_unique_otheroutput_tableentrynegative + S (dst_negative_add_exists_unique_otheroutput_table) = S ((S (dst_index_add_exists_unique_otheroutput_table)) * dst_negative_scale_add_exists_unique_otheroutput_table)) /\ exists ff_q_pvs_add_exists_unique_otheroutput_tableentrynegative. dst_negative_code_add_exists_unique_otheroutput_table = ff_q_pvs_add_exists_unique_otheroutput_tableentrynegative * S ((S (dst_index_add_exists_unique_otheroutput_table)) * dst_negative_scale_add_exists_unique_otheroutput_table) + (dst_negative_add_exists_unique_otheroutput_table))) /\ (exists ge_balance_positive_add_exists_unique_otheroutput_tableentryvalue ge_balance_negative_add_exists_unique_otheroutput_tableentryvalue. (((((dst_value_add_exists_unique_otheroutput_table) = 2 * (ge_balance_positive_add_exists_unique_otheroutput_tableentryvalue) /\ (ge_balance_negative_add_exists_unique_otheroutput_tableentryvalue) = 0) \/ exists ge_signed_half_add_exists_unique_otheroutput_tableentryvaluedecode. (((dst_value_add_exists_unique_otheroutput_table) = 2 * ge_signed_half_add_exists_unique_otheroutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_add_exists_unique_otheroutput_tableentryvalue) = 0) /\ (ge_balance_negative_add_exists_unique_otheroutput_tableentryvalue) = S ge_signed_half_add_exists_unique_otheroutput_tableentryvaluedecode))) /\ ((dst_positive_add_exists_unique_otheroutput_table) + ge_balance_negative_add_exists_unique_otheroutput_tableentryvalue = (dst_negative_add_exists_unique_otheroutput_table) + ge_balance_positive_add_exists_unique_otheroutput_tableentryvalue))))))))) /\ (forall sto_index_add_exists_unique_otherentries. (exists pvs_gap_add_exists_unique_otherentriesbound. pvs_gap_add_exists_unique_otherentriesbound + S (sto_index_add_exists_unique_otherentries) = (l)) -> exists sto_left_add_exists_unique_otherentries sto_right_add_exists_unique_otherentries sto_output_add_exists_unique_otherentries. ((exists dst_positive_code_add_exists_unique_otherentriesentryleft dst_positive_scale_add_exists_unique_otherentriesentryleft dst_negative_code_add_exists_unique_otherentriesentryleft dst_negative_scale_add_exists_unique_otherentriesentryleft dst_positive_add_exists_unique_otherentriesentryleft dst_negative_add_exists_unique_otherentriesentryleft. (((F) = (((((dst_positive_code_add_exists_unique_otherentriesentryleft) + (dst_positive_scale_add_exists_unique_otherentriesentryleft)) * S ((dst_positive_code_add_exists_unique_otherentriesentryleft) + (dst_positive_scale_add_exists_unique_otherentriesentryleft)) + ((dst_positive_scale_add_exists_unique_otherentriesentryleft) + (dst_positive_scale_add_exists_unique_otherentriesentryleft))) + (((dst_negative_code_add_exists_unique_otherentriesentryleft) + (dst_negative_scale_add_exists_unique_otherentriesentryleft)) * S ((dst_negative_code_add_exists_unique_otherentriesentryleft) + (dst_negative_scale_add_exists_unique_otherentriesentryleft)) + ((dst_negative_scale_add_exists_unique_otherentriesentryleft) + (dst_negative_scale_add_exists_unique_otherentriesentryleft)))) * S ((((dst_positive_code_add_exists_unique_otherentriesentryleft) + (dst_positive_scale_add_exists_unique_otherentriesentryleft)) * S ((dst_positive_code_add_exists_unique_otherentriesentryleft) + (dst_positive_scale_add_exists_unique_otherentriesentryleft)) + ((dst_positive_scale_add_exists_unique_otherentriesentryleft) + (dst_positive_scale_add_exists_unique_otherentriesentryleft))) + (((dst_negative_code_add_exists_unique_otherentriesentryleft) + (dst_negative_scale_add_exists_unique_otherentriesentryleft)) * S ((dst_negative_code_add_exists_unique_otherentriesentryleft) + (dst_negative_scale_add_exists_unique_otherentriesentryleft)) + ((dst_negative_scale_add_exists_unique_otherentriesentryleft) + (dst_negative_scale_add_exists_unique_otherentriesentryleft)))) + ((((dst_negative_code_add_exists_unique_otherentriesentryleft) + (dst_negative_scale_add_exists_unique_otherentriesentryleft)) * S ((dst_negative_code_add_exists_unique_otherentriesentryleft) + (dst_negative_scale_add_exists_unique_otherentriesentryleft)) + ((dst_negative_scale_add_exists_unique_otherentriesentryleft) + (dst_negative_scale_add_exists_unique_otherentriesentryleft))) + (((dst_negative_code_add_exists_unique_otherentriesentryleft) + (dst_negative_scale_add_exists_unique_otherentriesentryleft)) * S ((dst_negative_code_add_exists_unique_otherentriesentryleft) + (dst_negative_scale_add_exists_unique_otherentriesentryleft)) + ((dst_negative_scale_add_exists_unique_otherentriesentryleft) + (dst_negative_scale_add_exists_unique_otherentriesentryleft)))))) /\ (((((exists ff_h_pvs_add_exists_unique_otherentriesentryleftpositive. ff_h_pvs_add_exists_unique_otherentriesentryleftpositive + S (dst_positive_add_exists_unique_otherentriesentryleft) = S ((S (sto_index_add_exists_unique_otherentries)) * dst_positive_scale_add_exists_unique_otherentriesentryleft)) /\ exists ff_q_pvs_add_exists_unique_otherentriesentryleftpositive. dst_positive_code_add_exists_unique_otherentriesentryleft = ff_q_pvs_add_exists_unique_otherentriesentryleftpositive * S ((S (sto_index_add_exists_unique_otherentries)) * dst_positive_scale_add_exists_unique_otherentriesentryleft) + (dst_positive_add_exists_unique_otherentriesentryleft))) /\ (((((exists ff_h_pvs_add_exists_unique_otherentriesentryleftnegative. ff_h_pvs_add_exists_unique_otherentriesentryleftnegative + S (dst_negative_add_exists_unique_otherentriesentryleft) = S ((S (sto_index_add_exists_unique_otherentries)) * dst_negative_scale_add_exists_unique_otherentriesentryleft)) /\ exists ff_q_pvs_add_exists_unique_otherentriesentryleftnegative. dst_negative_code_add_exists_unique_otherentriesentryleft = ff_q_pvs_add_exists_unique_otherentriesentryleftnegative * S ((S (sto_index_add_exists_unique_otherentries)) * dst_negative_scale_add_exists_unique_otherentriesentryleft) + (dst_negative_add_exists_unique_otherentriesentryleft))) /\ (exists ge_balance_positive_add_exists_unique_otherentriesentryleftvalue ge_balance_negative_add_exists_unique_otherentriesentryleftvalue. (((((sto_left_add_exists_unique_otherentries) = 2 * (ge_balance_positive_add_exists_unique_otherentriesentryleftvalue) /\ (ge_balance_negative_add_exists_unique_otherentriesentryleftvalue) = 0) \/ exists ge_signed_half_add_exists_unique_otherentriesentryleftvaluedecode. (((sto_left_add_exists_unique_otherentries) = 2 * ge_signed_half_add_exists_unique_otherentriesentryleftvaluedecode + 1 /\ (ge_balance_positive_add_exists_unique_otherentriesentryleftvalue) = 0) /\ (ge_balance_negative_add_exists_unique_otherentriesentryleftvalue) = S ge_signed_half_add_exists_unique_otherentriesentryleftvaluedecode))) /\ ((dst_positive_add_exists_unique_otherentriesentryleft) + ge_balance_negative_add_exists_unique_otherentriesentryleftvalue = (dst_negative_add_exists_unique_otherentriesentryleft) + ge_balance_positive_add_exists_unique_otherentriesentryleftvalue))))))))) /\ (((exists dst_positive_code_add_exists_unique_otherentriesentryright dst_positive_scale_add_exists_unique_otherentriesentryright dst_negative_code_add_exists_unique_otherentriesentryright dst_negative_scale_add_exists_unique_otherentriesentryright dst_positive_add_exists_unique_otherentriesentryright dst_negative_add_exists_unique_otherentriesentryright. (((G) = (((((dst_positive_code_add_exists_unique_otherentriesentryright) + (dst_positive_scale_add_exists_unique_otherentriesentryright)) * S ((dst_positive_code_add_exists_unique_otherentriesentryright) + (dst_positive_scale_add_exists_unique_otherentriesentryright)) + ((dst_positive_scale_add_exists_unique_otherentriesentryright) + (dst_positive_scale_add_exists_unique_otherentriesentryright))) + (((dst_negative_code_add_exists_unique_otherentriesentryright) + (dst_negative_scale_add_exists_unique_otherentriesentryright)) * S ((dst_negative_code_add_exists_unique_otherentriesentryright) + (dst_negative_scale_add_exists_unique_otherentriesentryright)) + ((dst_negative_scale_add_exists_unique_otherentriesentryright) + (dst_negative_scale_add_exists_unique_otherentriesentryright)))) * S ((((dst_positive_code_add_exists_unique_otherentriesentryright) + (dst_positive_scale_add_exists_unique_otherentriesentryright)) * S ((dst_positive_code_add_exists_unique_otherentriesentryright) + (dst_positive_scale_add_exists_unique_otherentriesentryright)) + ((dst_positive_scale_add_exists_unique_otherentriesentryright) + (dst_positive_scale_add_exists_unique_otherentriesentryright))) + (((dst_negative_code_add_exists_unique_otherentriesentryright) + (dst_negative_scale_add_exists_unique_otherentriesentryright)) * S ((dst_negative_code_add_exists_unique_otherentriesentryright) + (dst_negative_scale_add_exists_unique_otherentriesentryright)) + ((dst_negative_scale_add_exists_unique_otherentriesentryright) + (dst_negative_scale_add_exists_unique_otherentriesentryright)))) + ((((dst_negative_code_add_exists_unique_otherentriesentryright) + (dst_negative_scale_add_exists_unique_otherentriesentryright)) * S ((dst_negative_code_add_exists_unique_otherentriesentryright) + (dst_negative_scale_add_exists_unique_otherentriesentryright)) + ((dst_negative_scale_add_exists_unique_otherentriesentryright) + (dst_negative_scale_add_exists_unique_otherentriesentryright))) + (((dst_negative_code_add_exists_unique_otherentriesentryright) + (dst_negative_scale_add_exists_unique_otherentriesentryright)) * S ((dst_negative_code_add_exists_unique_otherentriesentryright) + (dst_negative_scale_add_exists_unique_otherentriesentryright)) + ((dst_negative_scale_add_exists_unique_otherentriesentryright) + (dst_negative_scale_add_exists_unique_otherentriesentryright)))))) /\ (((((exists ff_h_pvs_add_exists_unique_otherentriesentryrightpositive. ff_h_pvs_add_exists_unique_otherentriesentryrightpositive + S (dst_positive_add_exists_unique_otherentriesentryright) = S ((S (sto_index_add_exists_unique_otherentries)) * dst_positive_scale_add_exists_unique_otherentriesentryright)) /\ exists ff_q_pvs_add_exists_unique_otherentriesentryrightpositive. dst_positive_code_add_exists_unique_otherentriesentryright = ff_q_pvs_add_exists_unique_otherentriesentryrightpositive * S ((S (sto_index_add_exists_unique_otherentries)) * dst_positive_scale_add_exists_unique_otherentriesentryright) + (dst_positive_add_exists_unique_otherentriesentryright))) /\ (((((exists ff_h_pvs_add_exists_unique_otherentriesentryrightnegative. ff_h_pvs_add_exists_unique_otherentriesentryrightnegative + S (dst_negative_add_exists_unique_otherentriesentryright) = S ((S (sto_index_add_exists_unique_otherentries)) * dst_negative_scale_add_exists_unique_otherentriesentryright)) /\ exists ff_q_pvs_add_exists_unique_otherentriesentryrightnegative. dst_negative_code_add_exists_unique_otherentriesentryright = ff_q_pvs_add_exists_unique_otherentriesentryrightnegative * S ((S (sto_index_add_exists_unique_otherentries)) * dst_negative_scale_add_exists_unique_otherentriesentryright) + (dst_negative_add_exists_unique_otherentriesentryright))) /\ (exists ge_balance_positive_add_exists_unique_otherentriesentryrightvalue ge_balance_negative_add_exists_unique_otherentriesentryrightvalue. (((((sto_right_add_exists_unique_otherentries) = 2 * (ge_balance_positive_add_exists_unique_otherentriesentryrightvalue) /\ (ge_balance_negative_add_exists_unique_otherentriesentryrightvalue) = 0) \/ exists ge_signed_half_add_exists_unique_otherentriesentryrightvaluedecode. (((sto_right_add_exists_unique_otherentries) = 2 * ge_signed_half_add_exists_unique_otherentriesentryrightvaluedecode + 1 /\ (ge_balance_positive_add_exists_unique_otherentriesentryrightvalue) = 0) /\ (ge_balance_negative_add_exists_unique_otherentriesentryrightvalue) = S ge_signed_half_add_exists_unique_otherentriesentryrightvaluedecode))) /\ ((dst_positive_add_exists_unique_otherentriesentryright) + ge_balance_negative_add_exists_unique_otherentriesentryrightvalue = (dst_negative_add_exists_unique_otherentriesentryright) + ge_balance_positive_add_exists_unique_otherentriesentryrightvalue))))))))) /\ (((exists dst_positive_code_add_exists_unique_otherentriesentryoutput dst_positive_scale_add_exists_unique_otherentriesentryoutput dst_negative_code_add_exists_unique_otherentriesentryoutput dst_negative_scale_add_exists_unique_otherentriesentryoutput dst_positive_add_exists_unique_otherentriesentryoutput dst_negative_add_exists_unique_otherentriesentryoutput. (((K) = (((((dst_positive_code_add_exists_unique_otherentriesentryoutput) + (dst_positive_scale_add_exists_unique_otherentriesentryoutput)) * S ((dst_positive_code_add_exists_unique_otherentriesentryoutput) + (dst_positive_scale_add_exists_unique_otherentriesentryoutput)) + ((dst_positive_scale_add_exists_unique_otherentriesentryoutput) + (dst_positive_scale_add_exists_unique_otherentriesentryoutput))) + (((dst_negative_code_add_exists_unique_otherentriesentryoutput) + (dst_negative_scale_add_exists_unique_otherentriesentryoutput)) * S ((dst_negative_code_add_exists_unique_otherentriesentryoutput) + (dst_negative_scale_add_exists_unique_otherentriesentryoutput)) + ((dst_negative_scale_add_exists_unique_otherentriesentryoutput) + (dst_negative_scale_add_exists_unique_otherentriesentryoutput)))) * S ((((dst_positive_code_add_exists_unique_otherentriesentryoutput) + (dst_positive_scale_add_exists_unique_otherentriesentryoutput)) * S ((dst_positive_code_add_exists_unique_otherentriesentryoutput) + (dst_positive_scale_add_exists_unique_otherentriesentryoutput)) + ((dst_positive_scale_add_exists_unique_otherentriesentryoutput) + (dst_positive_scale_add_exists_unique_otherentriesentryoutput))) + (((dst_negative_code_add_exists_unique_otherentriesentryoutput) + (dst_negative_scale_add_exists_unique_otherentriesentryoutput)) * S ((dst_negative_code_add_exists_unique_otherentriesentryoutput) + (dst_negative_scale_add_exists_unique_otherentriesentryoutput)) + ((dst_negative_scale_add_exists_unique_otherentriesentryoutput) + (dst_negative_scale_add_exists_unique_otherentriesentryoutput)))) + ((((dst_negative_code_add_exists_unique_otherentriesentryoutput) + (dst_negative_scale_add_exists_unique_otherentriesentryoutput)) * S ((dst_negative_code_add_exists_unique_otherentriesentryoutput) + (dst_negative_scale_add_exists_unique_otherentriesentryoutput)) + ((dst_negative_scale_add_exists_unique_otherentriesentryoutput) + (dst_negative_scale_add_exists_unique_otherentriesentryoutput))) + (((dst_negative_code_add_exists_unique_otherentriesentryoutput) + (dst_negative_scale_add_exists_unique_otherentriesentryoutput)) * S ((dst_negative_code_add_exists_unique_otherentriesentryoutput) + (dst_negative_scale_add_exists_unique_otherentriesentryoutput)) + ((dst_negative_scale_add_exists_unique_otherentriesentryoutput) + (dst_negative_scale_add_exists_unique_otherentriesentryoutput)))))) /\ (((((exists ff_h_pvs_add_exists_unique_otherentriesentryoutputpositive. ff_h_pvs_add_exists_unique_otherentriesentryoutputpositive + S (dst_positive_add_exists_unique_otherentriesentryoutput) = S ((S (sto_index_add_exists_unique_otherentries)) * dst_positive_scale_add_exists_unique_otherentriesentryoutput)) /\ exists ff_q_pvs_add_exists_unique_otherentriesentryoutputpositive. dst_positive_code_add_exists_unique_otherentriesentryoutput = ff_q_pvs_add_exists_unique_otherentriesentryoutputpositive * S ((S (sto_index_add_exists_unique_otherentries)) * dst_positive_scale_add_exists_unique_otherentriesentryoutput) + (dst_positive_add_exists_unique_otherentriesentryoutput))) /\ (((((exists ff_h_pvs_add_exists_unique_otherentriesentryoutputnegative. ff_h_pvs_add_exists_unique_otherentriesentryoutputnegative + S (dst_negative_add_exists_unique_otherentriesentryoutput) = S ((S (sto_index_add_exists_unique_otherentries)) * dst_negative_scale_add_exists_unique_otherentriesentryoutput)) /\ exists ff_q_pvs_add_exists_unique_otherentriesentryoutputnegative. dst_negative_code_add_exists_unique_otherentriesentryoutput = ff_q_pvs_add_exists_unique_otherentriesentryoutputnegative * S ((S (sto_index_add_exists_unique_otherentries)) * dst_negative_scale_add_exists_unique_otherentriesentryoutput) + (dst_negative_add_exists_unique_otherentriesentryoutput))) /\ (exists ge_balance_positive_add_exists_unique_otherentriesentryoutputvalue ge_balance_negative_add_exists_unique_otherentriesentryoutputvalue. (((((sto_output_add_exists_unique_otherentries) = 2 * (ge_balance_positive_add_exists_unique_otherentriesentryoutputvalue) /\ (ge_balance_negative_add_exists_unique_otherentriesentryoutputvalue) = 0) \/ exists ge_signed_half_add_exists_unique_otherentriesentryoutputvaluedecode. (((sto_output_add_exists_unique_otherentries) = 2 * ge_signed_half_add_exists_unique_otherentriesentryoutputvaluedecode + 1 /\ (ge_balance_positive_add_exists_unique_otherentriesentryoutputvalue) = 0) /\ (ge_balance_negative_add_exists_unique_otherentriesentryoutputvalue) = S ge_signed_half_add_exists_unique_otherentriesentryoutputvaluedecode))) /\ ((dst_positive_add_exists_unique_otherentriesentryoutput) + ge_balance_negative_add_exists_unique_otherentriesentryoutputvalue = (dst_negative_add_exists_unique_otherentriesentryoutput) + ge_balance_positive_add_exists_unique_otherentriesentryoutputvalue))))))))) /\ (exists dsa_ap_add_exists_unique_otherentriesentryoperation dsa_an_add_exists_unique_otherentriesentryoperation dsa_bp_add_exists_unique_otherentriesentryoperation dsa_bn_add_exists_unique_otherentriesentryoperation dsa_cp_add_exists_unique_otherentriesentryoperation dsa_cn_add_exists_unique_otherentriesentryoperation. (((((sto_left_add_exists_unique_otherentries) = 2 * (dsa_ap_add_exists_unique_otherentriesentryoperation) /\ (dsa_an_add_exists_unique_otherentriesentryoperation) = 0) \/ exists ge_signed_half_add_exists_unique_otherentriesentryoperationleft. (((sto_left_add_exists_unique_otherentries) = 2 * ge_signed_half_add_exists_unique_otherentriesentryoperationleft + 1 /\ (dsa_ap_add_exists_unique_otherentriesentryoperation) = 0) /\ (dsa_an_add_exists_unique_otherentriesentryoperation) = S ge_signed_half_add_exists_unique_otherentriesentryoperationleft))) /\ ((((((sto_right_add_exists_unique_otherentries) = 2 * (dsa_bp_add_exists_unique_otherentriesentryoperation) /\ (dsa_bn_add_exists_unique_otherentriesentryoperation) = 0) \/ exists ge_signed_half_add_exists_unique_otherentriesentryoperationright. (((sto_right_add_exists_unique_otherentries) = 2 * ge_signed_half_add_exists_unique_otherentriesentryoperationright + 1 /\ (dsa_bp_add_exists_unique_otherentriesentryoperation) = 0) /\ (dsa_bn_add_exists_unique_otherentriesentryoperation) = S ge_signed_half_add_exists_unique_otherentriesentryoperationright))) /\ ((((((sto_output_add_exists_unique_otherentries) = 2 * (dsa_cp_add_exists_unique_otherentriesentryoperation) /\ (dsa_cn_add_exists_unique_otherentriesentryoperation) = 0) \/ exists ge_signed_half_add_exists_unique_otherentriesentryoperationoutput. (((sto_output_add_exists_unique_otherentries) = 2 * ge_signed_half_add_exists_unique_otherentriesentryoperationoutput + 1 /\ (dsa_cp_add_exists_unique_otherentriesentryoperation) = 0) /\ (dsa_cn_add_exists_unique_otherentriesentryoperation) = S ge_signed_half_add_exists_unique_otherentriesentryoperationoutput))) /\ ((dsa_ap_add_exists_unique_otherentriesentryoperation + dsa_bp_add_exists_unique_otherentriesentryoperation) + dsa_cn_add_exists_unique_otherentriesentryoperation = (dsa_an_add_exists_unique_otherentriesentryoperation + dsa_bn_add_exists_unique_otherentriesentryoperation) + dsa_cp_add_exists_unique_otherentriesentryoperation))))))))))))))))))) -> (forall dst_index_add_exists_unique_equal dst_first_add_exists_unique_equal dst_second_add_exists_unique_equal. (exists pvs_gap_add_exists_unique_equalbound. pvs_gap_add_exists_unique_equalbound + S (dst_index_add_exists_unique_equal) = (l)) -> (exists dst_positive_code_add_exists_unique_equalfirst dst_positive_scale_add_exists_unique_equalfirst dst_negative_code_add_exists_unique_equalfirst dst_negative_scale_add_exists_unique_equalfirst dst_positive_add_exists_unique_equalfirst dst_negative_add_exists_unique_equalfirst. (((H) = (((((dst_positive_code_add_exists_unique_equalfirst) + (dst_positive_scale_add_exists_unique_equalfirst)) * S ((dst_positive_code_add_exists_unique_equalfirst) + (dst_positive_scale_add_exists_unique_equalfirst)) + ((dst_positive_scale_add_exists_unique_equalfirst) + (dst_positive_scale_add_exists_unique_equalfirst))) + (((dst_negative_code_add_exists_unique_equalfirst) + (dst_negative_scale_add_exists_unique_equalfirst)) * S ((dst_negative_code_add_exists_unique_equalfirst) + (dst_negative_scale_add_exists_unique_equalfirst)) + ((dst_negative_scale_add_exists_unique_equalfirst) + (dst_negative_scale_add_exists_unique_equalfirst)))) * S ((((dst_positive_code_add_exists_unique_equalfirst) + (dst_positive_scale_add_exists_unique_equalfirst)) * S ((dst_positive_code_add_exists_unique_equalfirst) + (dst_positive_scale_add_exists_unique_equalfirst)) + ((dst_positive_scale_add_exists_unique_equalfirst) + (dst_positive_scale_add_exists_unique_equalfirst))) + (((dst_negative_code_add_exists_unique_equalfirst) + (dst_negative_scale_add_exists_unique_equalfirst)) * S ((dst_negative_code_add_exists_unique_equalfirst) + (dst_negative_scale_add_exists_unique_equalfirst)) + ((dst_negative_scale_add_exists_unique_equalfirst) + (dst_negative_scale_add_exists_unique_equalfirst)))) + ((((dst_negative_code_add_exists_unique_equalfirst) + (dst_negative_scale_add_exists_unique_equalfirst)) * S ((dst_negative_code_add_exists_unique_equalfirst) + (dst_negative_scale_add_exists_unique_equalfirst)) + ((dst_negative_scale_add_exists_unique_equalfirst) + (dst_negative_scale_add_exists_unique_equalfirst))) + (((dst_negative_code_add_exists_unique_equalfirst) + (dst_negative_scale_add_exists_unique_equalfirst)) * S ((dst_negative_code_add_exists_unique_equalfirst) + (dst_negative_scale_add_exists_unique_equalfirst)) + ((dst_negative_scale_add_exists_unique_equalfirst) + (dst_negative_scale_add_exists_unique_equalfirst)))))) /\ (((((exists ff_h_pvs_add_exists_unique_equalfirstpositive. ff_h_pvs_add_exists_unique_equalfirstpositive + S (dst_positive_add_exists_unique_equalfirst) = S ((S (dst_index_add_exists_unique_equal)) * dst_positive_scale_add_exists_unique_equalfirst)) /\ exists ff_q_pvs_add_exists_unique_equalfirstpositive. dst_positive_code_add_exists_unique_equalfirst = ff_q_pvs_add_exists_unique_equalfirstpositive * S ((S (dst_index_add_exists_unique_equal)) * dst_positive_scale_add_exists_unique_equalfirst) + (dst_positive_add_exists_unique_equalfirst))) /\ (((((exists ff_h_pvs_add_exists_unique_equalfirstnegative. ff_h_pvs_add_exists_unique_equalfirstnegative + S (dst_negative_add_exists_unique_equalfirst) = S ((S (dst_index_add_exists_unique_equal)) * dst_negative_scale_add_exists_unique_equalfirst)) /\ exists ff_q_pvs_add_exists_unique_equalfirstnegative. dst_negative_code_add_exists_unique_equalfirst = ff_q_pvs_add_exists_unique_equalfirstnegative * S ((S (dst_index_add_exists_unique_equal)) * dst_negative_scale_add_exists_unique_equalfirst) + (dst_negative_add_exists_unique_equalfirst))) /\ (exists ge_balance_positive_add_exists_unique_equalfirstvalue ge_balance_negative_add_exists_unique_equalfirstvalue. (((((dst_first_add_exists_unique_equal) = 2 * (ge_balance_positive_add_exists_unique_equalfirstvalue) /\ (ge_balance_negative_add_exists_unique_equalfirstvalue) = 0) \/ exists ge_signed_half_add_exists_unique_equalfirstvaluedecode. (((dst_first_add_exists_unique_equal) = 2 * ge_signed_half_add_exists_unique_equalfirstvaluedecode + 1 /\ (ge_balance_positive_add_exists_unique_equalfirstvalue) = 0) /\ (ge_balance_negative_add_exists_unique_equalfirstvalue) = S ge_signed_half_add_exists_unique_equalfirstvaluedecode))) /\ ((dst_positive_add_exists_unique_equalfirst) + ge_balance_negative_add_exists_unique_equalfirstvalue = (dst_negative_add_exists_unique_equalfirst) + ge_balance_positive_add_exists_unique_equalfirstvalue))))))))) -> (exists dst_positive_code_add_exists_unique_equalsecond dst_positive_scale_add_exists_unique_equalsecond dst_negative_code_add_exists_unique_equalsecond dst_negative_scale_add_exists_unique_equalsecond dst_positive_add_exists_unique_equalsecond dst_negative_add_exists_unique_equalsecond. (((K) = (((((dst_positive_code_add_exists_unique_equalsecond) + (dst_positive_scale_add_exists_unique_equalsecond)) * S ((dst_positive_code_add_exists_unique_equalsecond) + (dst_positive_scale_add_exists_unique_equalsecond)) + ((dst_positive_scale_add_exists_unique_equalsecond) + (dst_positive_scale_add_exists_unique_equalsecond))) + (((dst_negative_code_add_exists_unique_equalsecond) + (dst_negative_scale_add_exists_unique_equalsecond)) * S ((dst_negative_code_add_exists_unique_equalsecond) + (dst_negative_scale_add_exists_unique_equalsecond)) + ((dst_negative_scale_add_exists_unique_equalsecond) + (dst_negative_scale_add_exists_unique_equalsecond)))) * S ((((dst_positive_code_add_exists_unique_equalsecond) + (dst_positive_scale_add_exists_unique_equalsecond)) * S ((dst_positive_code_add_exists_unique_equalsecond) + (dst_positive_scale_add_exists_unique_equalsecond)) + ((dst_positive_scale_add_exists_unique_equalsecond) + (dst_positive_scale_add_exists_unique_equalsecond))) + (((dst_negative_code_add_exists_unique_equalsecond) + (dst_negative_scale_add_exists_unique_equalsecond)) * S ((dst_negative_code_add_exists_unique_equalsecond) + (dst_negative_scale_add_exists_unique_equalsecond)) + ((dst_negative_scale_add_exists_unique_equalsecond) + (dst_negative_scale_add_exists_unique_equalsecond)))) + ((((dst_negative_code_add_exists_unique_equalsecond) + (dst_negative_scale_add_exists_unique_equalsecond)) * S ((dst_negative_code_add_exists_unique_equalsecond) + (dst_negative_scale_add_exists_unique_equalsecond)) + ((dst_negative_scale_add_exists_unique_equalsecond) + (dst_negative_scale_add_exists_unique_equalsecond))) + (((dst_negative_code_add_exists_unique_equalsecond) + (dst_negative_scale_add_exists_unique_equalsecond)) * S ((dst_negative_code_add_exists_unique_equalsecond) + (dst_negative_scale_add_exists_unique_equalsecond)) + ((dst_negative_scale_add_exists_unique_equalsecond) + (dst_negative_scale_add_exists_unique_equalsecond)))))) /\ (((((exists ff_h_pvs_add_exists_unique_equalsecondpositive. ff_h_pvs_add_exists_unique_equalsecondpositive + S (dst_positive_add_exists_unique_equalsecond) = S ((S (dst_index_add_exists_unique_equal)) * dst_positive_scale_add_exists_unique_equalsecond)) /\ exists ff_q_pvs_add_exists_unique_equalsecondpositive. dst_positive_code_add_exists_unique_equalsecond = ff_q_pvs_add_exists_unique_equalsecondpositive * S ((S (dst_index_add_exists_unique_equal)) * dst_positive_scale_add_exists_unique_equalsecond) + (dst_positive_add_exists_unique_equalsecond))) /\ (((((exists ff_h_pvs_add_exists_unique_equalsecondnegative. ff_h_pvs_add_exists_unique_equalsecondnegative + S (dst_negative_add_exists_unique_equalsecond) = S ((S (dst_index_add_exists_unique_equal)) * dst_negative_scale_add_exists_unique_equalsecond)) /\ exists ff_q_pvs_add_exists_unique_equalsecondnegative. dst_negative_code_add_exists_unique_equalsecond = ff_q_pvs_add_exists_unique_equalsecondnegative * S ((S (dst_index_add_exists_unique_equal)) * dst_negative_scale_add_exists_unique_equalsecond) + (dst_negative_add_exists_unique_equalsecond))) /\ (exists ge_balance_positive_add_exists_unique_equalsecondvalue ge_balance_negative_add_exists_unique_equalsecondvalue. (((((dst_second_add_exists_unique_equal) = 2 * (ge_balance_positive_add_exists_unique_equalsecondvalue) /\ (ge_balance_negative_add_exists_unique_equalsecondvalue) = 0) \/ exists ge_signed_half_add_exists_unique_equalsecondvaluedecode. (((dst_second_add_exists_unique_equal) = 2 * ge_signed_half_add_exists_unique_equalsecondvaluedecode + 1 /\ (ge_balance_positive_add_exists_unique_equalsecondvalue) = 0) /\ (ge_balance_negative_add_exists_unique_equalsecondvalue) = S ge_signed_half_add_exists_unique_equalsecondvaluedecode))) /\ ((dst_positive_add_exists_unique_equalsecond) + ge_balance_negative_add_exists_unique_equalsecondvalue = (dst_negative_add_exists_unique_equalsecond) + ge_balance_positive_add_exists_unique_equalsecondvalue))))))))) -> dst_first_add_exists_unique_equal = dst_second_add_exists_unique_equal)))