signed_table_multiply_extensional_unique

forall F G H K l. (((exists dst_positive_code_multiply_unique_firstleft_table dst_positive_scale_multiply_unique_firstleft_table dst_negative_code_multiply_unique_firstleft_table dst_negative_scale_multiply_unique_firstleft_table. (((F) = (((((dst_positive_code_multiply_unique_firstleft_table) + (dst_positive_scale_multiply_unique_firstleft_table)) * S ((dst_positive_code_multiply_unique_firstleft_table) + (dst_positive_scale_multiply_unique_firstleft_table)) + ((dst_positive_scale_multiply_unique_firstleft_table) + (dst_positive_scale_multiply_unique_firstleft_table))) + (((dst_negative_code_multiply_unique_firstleft_table) + (dst_negative_scale_multiply_unique_firstleft_table)) * S ((dst_negative_code_multiply_unique_firstleft_table) + (dst_negative_scale_multiply_unique_firstleft_table)) + ((dst_negative_scale_multiply_unique_firstleft_table) + (dst_negative_scale_multiply_unique_firstleft_table)))) * S ((((dst_positive_code_multiply_unique_firstleft_table) + (dst_positive_scale_multiply_unique_firstleft_table)) * S ((dst_positive_code_multiply_unique_firstleft_table) + (dst_positive_scale_multiply_unique_firstleft_table)) + ((dst_positive_scale_multiply_unique_firstleft_table) + (dst_positive_scale_multiply_unique_firstleft_table))) + (((dst_negative_code_multiply_unique_firstleft_table) + (dst_negative_scale_multiply_unique_firstleft_table)) * S ((dst_negative_code_multiply_unique_firstleft_table) + (dst_negative_scale_multiply_unique_firstleft_table)) + ((dst_negative_scale_multiply_unique_firstleft_table) + (dst_negative_scale_multiply_unique_firstleft_table)))) + ((((dst_negative_code_multiply_unique_firstleft_table) + (dst_negative_scale_multiply_unique_firstleft_table)) * S ((dst_negative_code_multiply_unique_firstleft_table) + (dst_negative_scale_multiply_unique_firstleft_table)) + ((dst_negative_scale_multiply_unique_firstleft_table) + (dst_negative_scale_multiply_unique_firstleft_table))) + (((dst_negative_code_multiply_unique_firstleft_table) + (dst_negative_scale_multiply_unique_firstleft_table)) * S ((dst_negative_code_multiply_unique_firstleft_table) + (dst_negative_scale_multiply_unique_firstleft_table)) + ((dst_negative_scale_multiply_unique_firstleft_table) + (dst_negative_scale_multiply_unique_firstleft_table)))))) /\ (forall dst_index_multiply_unique_firstleft_table. (exists pvs_le_gap_multiply_unique_firstleft_tabledomain. pvs_le_gap_multiply_unique_firstleft_tabledomain + (dst_index_multiply_unique_firstleft_table) = (l)) -> exists dst_positive_multiply_unique_firstleft_table dst_negative_multiply_unique_firstleft_table dst_value_multiply_unique_firstleft_table. ((((exists ff_h_pvs_multiply_unique_firstleft_tableentrypositive. ff_h_pvs_multiply_unique_firstleft_tableentrypositive + S (dst_positive_multiply_unique_firstleft_table) = S ((S (dst_index_multiply_unique_firstleft_table)) * dst_positive_scale_multiply_unique_firstleft_table)) /\ exists ff_q_pvs_multiply_unique_firstleft_tableentrypositive. dst_positive_code_multiply_unique_firstleft_table = ff_q_pvs_multiply_unique_firstleft_tableentrypositive * S ((S (dst_index_multiply_unique_firstleft_table)) * dst_positive_scale_multiply_unique_firstleft_table) + (dst_positive_multiply_unique_firstleft_table))) /\ (((((exists ff_h_pvs_multiply_unique_firstleft_tableentrynegative. ff_h_pvs_multiply_unique_firstleft_tableentrynegative + S (dst_negative_multiply_unique_firstleft_table) = S ((S (dst_index_multiply_unique_firstleft_table)) * dst_negative_scale_multiply_unique_firstleft_table)) /\ exists ff_q_pvs_multiply_unique_firstleft_tableentrynegative. dst_negative_code_multiply_unique_firstleft_table = ff_q_pvs_multiply_unique_firstleft_tableentrynegative * S ((S (dst_index_multiply_unique_firstleft_table)) * dst_negative_scale_multiply_unique_firstleft_table) + (dst_negative_multiply_unique_firstleft_table))) /\ (exists ge_balance_positive_multiply_unique_firstleft_tableentryvalue ge_balance_negative_multiply_unique_firstleft_tableentryvalue. (((((dst_value_multiply_unique_firstleft_table) = 2 * (ge_balance_positive_multiply_unique_firstleft_tableentryvalue) /\ (ge_balance_negative_multiply_unique_firstleft_tableentryvalue) = 0) \/ exists ge_signed_half_multiply_unique_firstleft_tableentryvaluedecode. (((dst_value_multiply_unique_firstleft_table) = 2 * ge_signed_half_multiply_unique_firstleft_tableentryvaluedecode + 1 /\ (ge_balance_positive_multiply_unique_firstleft_tableentryvalue) = 0) /\ (ge_balance_negative_multiply_unique_firstleft_tableentryvalue) = S ge_signed_half_multiply_unique_firstleft_tableentryvaluedecode))) /\ ((dst_positive_multiply_unique_firstleft_table) + ge_balance_negative_multiply_unique_firstleft_tableentryvalue = (dst_negative_multiply_unique_firstleft_table) + ge_balance_positive_multiply_unique_firstleft_tableentryvalue))))))))) /\ (((exists dst_positive_code_multiply_unique_firstright_table dst_positive_scale_multiply_unique_firstright_table dst_negative_code_multiply_unique_firstright_table dst_negative_scale_multiply_unique_firstright_table. (((G) = (((((dst_positive_code_multiply_unique_firstright_table) + (dst_positive_scale_multiply_unique_firstright_table)) * S ((dst_positive_code_multiply_unique_firstright_table) + (dst_positive_scale_multiply_unique_firstright_table)) + ((dst_positive_scale_multiply_unique_firstright_table) + (dst_positive_scale_multiply_unique_firstright_table))) + (((dst_negative_code_multiply_unique_firstright_table) + (dst_negative_scale_multiply_unique_firstright_table)) * S ((dst_negative_code_multiply_unique_firstright_table) + (dst_negative_scale_multiply_unique_firstright_table)) + ((dst_negative_scale_multiply_unique_firstright_table) + (dst_negative_scale_multiply_unique_firstright_table)))) * S ((((dst_positive_code_multiply_unique_firstright_table) + (dst_positive_scale_multiply_unique_firstright_table)) * S ((dst_positive_code_multiply_unique_firstright_table) + (dst_positive_scale_multiply_unique_firstright_table)) + ((dst_positive_scale_multiply_unique_firstright_table) + (dst_positive_scale_multiply_unique_firstright_table))) + (((dst_negative_code_multiply_unique_firstright_table) + (dst_negative_scale_multiply_unique_firstright_table)) * S ((dst_negative_code_multiply_unique_firstright_table) + (dst_negative_scale_multiply_unique_firstright_table)) + ((dst_negative_scale_multiply_unique_firstright_table) + (dst_negative_scale_multiply_unique_firstright_table)))) + ((((dst_negative_code_multiply_unique_firstright_table) + (dst_negative_scale_multiply_unique_firstright_table)) * S ((dst_negative_code_multiply_unique_firstright_table) + (dst_negative_scale_multiply_unique_firstright_table)) + ((dst_negative_scale_multiply_unique_firstright_table) + (dst_negative_scale_multiply_unique_firstright_table))) + (((dst_negative_code_multiply_unique_firstright_table) + (dst_negative_scale_multiply_unique_firstright_table)) * S ((dst_negative_code_multiply_unique_firstright_table) + (dst_negative_scale_multiply_unique_firstright_table)) + ((dst_negative_scale_multiply_unique_firstright_table) + (dst_negative_scale_multiply_unique_firstright_table)))))) /\ (forall dst_index_multiply_unique_firstright_table. (exists pvs_le_gap_multiply_unique_firstright_tabledomain. pvs_le_gap_multiply_unique_firstright_tabledomain + (dst_index_multiply_unique_firstright_table) = (l)) -> exists dst_positive_multiply_unique_firstright_table dst_negative_multiply_unique_firstright_table dst_value_multiply_unique_firstright_table. ((((exists ff_h_pvs_multiply_unique_firstright_tableentrypositive. ff_h_pvs_multiply_unique_firstright_tableentrypositive + S (dst_positive_multiply_unique_firstright_table) = S ((S (dst_index_multiply_unique_firstright_table)) * dst_positive_scale_multiply_unique_firstright_table)) /\ exists ff_q_pvs_multiply_unique_firstright_tableentrypositive. dst_positive_code_multiply_unique_firstright_table = ff_q_pvs_multiply_unique_firstright_tableentrypositive * S ((S (dst_index_multiply_unique_firstright_table)) * dst_positive_scale_multiply_unique_firstright_table) + (dst_positive_multiply_unique_firstright_table))) /\ (((((exists ff_h_pvs_multiply_unique_firstright_tableentrynegative. ff_h_pvs_multiply_unique_firstright_tableentrynegative + S (dst_negative_multiply_unique_firstright_table) = S ((S (dst_index_multiply_unique_firstright_table)) * dst_negative_scale_multiply_unique_firstright_table)) /\ exists ff_q_pvs_multiply_unique_firstright_tableentrynegative. dst_negative_code_multiply_unique_firstright_table = ff_q_pvs_multiply_unique_firstright_tableentrynegative * S ((S (dst_index_multiply_unique_firstright_table)) * dst_negative_scale_multiply_unique_firstright_table) + (dst_negative_multiply_unique_firstright_table))) /\ (exists ge_balance_positive_multiply_unique_firstright_tableentryvalue ge_balance_negative_multiply_unique_firstright_tableentryvalue. (((((dst_value_multiply_unique_firstright_table) = 2 * (ge_balance_positive_multiply_unique_firstright_tableentryvalue) /\ (ge_balance_negative_multiply_unique_firstright_tableentryvalue) = 0) \/ exists ge_signed_half_multiply_unique_firstright_tableentryvaluedecode. (((dst_value_multiply_unique_firstright_table) = 2 * ge_signed_half_multiply_unique_firstright_tableentryvaluedecode + 1 /\ (ge_balance_positive_multiply_unique_firstright_tableentryvalue) = 0) /\ (ge_balance_negative_multiply_unique_firstright_tableentryvalue) = S ge_signed_half_multiply_unique_firstright_tableentryvaluedecode))) /\ ((dst_positive_multiply_unique_firstright_table) + ge_balance_negative_multiply_unique_firstright_tableentryvalue = (dst_negative_multiply_unique_firstright_table) + ge_balance_positive_multiply_unique_firstright_tableentryvalue))))))))) /\ (((exists dst_positive_code_multiply_unique_firstoutput_table dst_positive_scale_multiply_unique_firstoutput_table dst_negative_code_multiply_unique_firstoutput_table dst_negative_scale_multiply_unique_firstoutput_table. (((H) = (((((dst_positive_code_multiply_unique_firstoutput_table) + (dst_positive_scale_multiply_unique_firstoutput_table)) * S ((dst_positive_code_multiply_unique_firstoutput_table) + (dst_positive_scale_multiply_unique_firstoutput_table)) + ((dst_positive_scale_multiply_unique_firstoutput_table) + (dst_positive_scale_multiply_unique_firstoutput_table))) + (((dst_negative_code_multiply_unique_firstoutput_table) + (dst_negative_scale_multiply_unique_firstoutput_table)) * S ((dst_negative_code_multiply_unique_firstoutput_table) + (dst_negative_scale_multiply_unique_firstoutput_table)) + ((dst_negative_scale_multiply_unique_firstoutput_table) + (dst_negative_scale_multiply_unique_firstoutput_table)))) * S ((((dst_positive_code_multiply_unique_firstoutput_table) + (dst_positive_scale_multiply_unique_firstoutput_table)) * S ((dst_positive_code_multiply_unique_firstoutput_table) + (dst_positive_scale_multiply_unique_firstoutput_table)) + ((dst_positive_scale_multiply_unique_firstoutput_table) + (dst_positive_scale_multiply_unique_firstoutput_table))) + (((dst_negative_code_multiply_unique_firstoutput_table) + (dst_negative_scale_multiply_unique_firstoutput_table)) * S ((dst_negative_code_multiply_unique_firstoutput_table) + (dst_negative_scale_multiply_unique_firstoutput_table)) + ((dst_negative_scale_multiply_unique_firstoutput_table) + (dst_negative_scale_multiply_unique_firstoutput_table)))) + ((((dst_negative_code_multiply_unique_firstoutput_table) + (dst_negative_scale_multiply_unique_firstoutput_table)) * S ((dst_negative_code_multiply_unique_firstoutput_table) + (dst_negative_scale_multiply_unique_firstoutput_table)) + ((dst_negative_scale_multiply_unique_firstoutput_table) + (dst_negative_scale_multiply_unique_firstoutput_table))) + (((dst_negative_code_multiply_unique_firstoutput_table) + (dst_negative_scale_multiply_unique_firstoutput_table)) * S ((dst_negative_code_multiply_unique_firstoutput_table) + (dst_negative_scale_multiply_unique_firstoutput_table)) + ((dst_negative_scale_multiply_unique_firstoutput_table) + (dst_negative_scale_multiply_unique_firstoutput_table)))))) /\ (forall dst_index_multiply_unique_firstoutput_table. (exists pvs_le_gap_multiply_unique_firstoutput_tabledomain. pvs_le_gap_multiply_unique_firstoutput_tabledomain + (dst_index_multiply_unique_firstoutput_table) = (l)) -> exists dst_positive_multiply_unique_firstoutput_table dst_negative_multiply_unique_firstoutput_table dst_value_multiply_unique_firstoutput_table. ((((exists ff_h_pvs_multiply_unique_firstoutput_tableentrypositive. ff_h_pvs_multiply_unique_firstoutput_tableentrypositive + S (dst_positive_multiply_unique_firstoutput_table) = S ((S (dst_index_multiply_unique_firstoutput_table)) * dst_positive_scale_multiply_unique_firstoutput_table)) /\ exists ff_q_pvs_multiply_unique_firstoutput_tableentrypositive. dst_positive_code_multiply_unique_firstoutput_table = ff_q_pvs_multiply_unique_firstoutput_tableentrypositive * S ((S (dst_index_multiply_unique_firstoutput_table)) * dst_positive_scale_multiply_unique_firstoutput_table) + (dst_positive_multiply_unique_firstoutput_table))) /\ (((((exists ff_h_pvs_multiply_unique_firstoutput_tableentrynegative. ff_h_pvs_multiply_unique_firstoutput_tableentrynegative + S (dst_negative_multiply_unique_firstoutput_table) = S ((S (dst_index_multiply_unique_firstoutput_table)) * dst_negative_scale_multiply_unique_firstoutput_table)) /\ exists ff_q_pvs_multiply_unique_firstoutput_tableentrynegative. dst_negative_code_multiply_unique_firstoutput_table = ff_q_pvs_multiply_unique_firstoutput_tableentrynegative * S ((S (dst_index_multiply_unique_firstoutput_table)) * dst_negative_scale_multiply_unique_firstoutput_table) + (dst_negative_multiply_unique_firstoutput_table))) /\ (exists ge_balance_positive_multiply_unique_firstoutput_tableentryvalue ge_balance_negative_multiply_unique_firstoutput_tableentryvalue. (((((dst_value_multiply_unique_firstoutput_table) = 2 * (ge_balance_positive_multiply_unique_firstoutput_tableentryvalue) /\ (ge_balance_negative_multiply_unique_firstoutput_tableentryvalue) = 0) \/ exists ge_signed_half_multiply_unique_firstoutput_tableentryvaluedecode. (((dst_value_multiply_unique_firstoutput_table) = 2 * ge_signed_half_multiply_unique_firstoutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_multiply_unique_firstoutput_tableentryvalue) = 0) /\ (ge_balance_negative_multiply_unique_firstoutput_tableentryvalue) = S ge_signed_half_multiply_unique_firstoutput_tableentryvaluedecode))) /\ ((dst_positive_multiply_unique_firstoutput_table) + ge_balance_negative_multiply_unique_firstoutput_tableentryvalue = (dst_negative_multiply_unique_firstoutput_table) + ge_balance_positive_multiply_unique_firstoutput_tableentryvalue))))))))) /\ (forall sto_index_multiply_unique_firstentries. (exists pvs_gap_multiply_unique_firstentriesbound. pvs_gap_multiply_unique_firstentriesbound + S (sto_index_multiply_unique_firstentries) = (l)) -> exists sto_left_multiply_unique_firstentries sto_right_multiply_unique_firstentries sto_output_multiply_unique_firstentries. ((exists dst_positive_code_multiply_unique_firstentriesentryleft dst_positive_scale_multiply_unique_firstentriesentryleft dst_negative_code_multiply_unique_firstentriesentryleft dst_negative_scale_multiply_unique_firstentriesentryleft dst_positive_multiply_unique_firstentriesentryleft dst_negative_multiply_unique_firstentriesentryleft. (((F) = (((((dst_positive_code_multiply_unique_firstentriesentryleft) + (dst_positive_scale_multiply_unique_firstentriesentryleft)) * S ((dst_positive_code_multiply_unique_firstentriesentryleft) + (dst_positive_scale_multiply_unique_firstentriesentryleft)) + ((dst_positive_scale_multiply_unique_firstentriesentryleft) + (dst_positive_scale_multiply_unique_firstentriesentryleft))) + (((dst_negative_code_multiply_unique_firstentriesentryleft) + (dst_negative_scale_multiply_unique_firstentriesentryleft)) * S ((dst_negative_code_multiply_unique_firstentriesentryleft) + (dst_negative_scale_multiply_unique_firstentriesentryleft)) + ((dst_negative_scale_multiply_unique_firstentriesentryleft) + (dst_negative_scale_multiply_unique_firstentriesentryleft)))) * S ((((dst_positive_code_multiply_unique_firstentriesentryleft) + (dst_positive_scale_multiply_unique_firstentriesentryleft)) * S ((dst_positive_code_multiply_unique_firstentriesentryleft) + (dst_positive_scale_multiply_unique_firstentriesentryleft)) + ((dst_positive_scale_multiply_unique_firstentriesentryleft) + (dst_positive_scale_multiply_unique_firstentriesentryleft))) + (((dst_negative_code_multiply_unique_firstentriesentryleft) + (dst_negative_scale_multiply_unique_firstentriesentryleft)) * S ((dst_negative_code_multiply_unique_firstentriesentryleft) + (dst_negative_scale_multiply_unique_firstentriesentryleft)) + ((dst_negative_scale_multiply_unique_firstentriesentryleft) + (dst_negative_scale_multiply_unique_firstentriesentryleft)))) + ((((dst_negative_code_multiply_unique_firstentriesentryleft) + (dst_negative_scale_multiply_unique_firstentriesentryleft)) * S ((dst_negative_code_multiply_unique_firstentriesentryleft) + (dst_negative_scale_multiply_unique_firstentriesentryleft)) + ((dst_negative_scale_multiply_unique_firstentriesentryleft) + (dst_negative_scale_multiply_unique_firstentriesentryleft))) + (((dst_negative_code_multiply_unique_firstentriesentryleft) + (dst_negative_scale_multiply_unique_firstentriesentryleft)) * S ((dst_negative_code_multiply_unique_firstentriesentryleft) + (dst_negative_scale_multiply_unique_firstentriesentryleft)) + ((dst_negative_scale_multiply_unique_firstentriesentryleft) + (dst_negative_scale_multiply_unique_firstentriesentryleft)))))) /\ (((((exists ff_h_pvs_multiply_unique_firstentriesentryleftpositive. ff_h_pvs_multiply_unique_firstentriesentryleftpositive + S (dst_positive_multiply_unique_firstentriesentryleft) = S ((S (sto_index_multiply_unique_firstentries)) * dst_positive_scale_multiply_unique_firstentriesentryleft)) /\ exists ff_q_pvs_multiply_unique_firstentriesentryleftpositive. dst_positive_code_multiply_unique_firstentriesentryleft = ff_q_pvs_multiply_unique_firstentriesentryleftpositive * S ((S (sto_index_multiply_unique_firstentries)) * dst_positive_scale_multiply_unique_firstentriesentryleft) + (dst_positive_multiply_unique_firstentriesentryleft))) /\ (((((exists ff_h_pvs_multiply_unique_firstentriesentryleftnegative. ff_h_pvs_multiply_unique_firstentriesentryleftnegative + S (dst_negative_multiply_unique_firstentriesentryleft) = S ((S (sto_index_multiply_unique_firstentries)) * dst_negative_scale_multiply_unique_firstentriesentryleft)) /\ exists ff_q_pvs_multiply_unique_firstentriesentryleftnegative. dst_negative_code_multiply_unique_firstentriesentryleft = ff_q_pvs_multiply_unique_firstentriesentryleftnegative * S ((S (sto_index_multiply_unique_firstentries)) * dst_negative_scale_multiply_unique_firstentriesentryleft) + (dst_negative_multiply_unique_firstentriesentryleft))) /\ (exists ge_balance_positive_multiply_unique_firstentriesentryleftvalue ge_balance_negative_multiply_unique_firstentriesentryleftvalue. (((((sto_left_multiply_unique_firstentries) = 2 * (ge_balance_positive_multiply_unique_firstentriesentryleftvalue) /\ (ge_balance_negative_multiply_unique_firstentriesentryleftvalue) = 0) \/ exists ge_signed_half_multiply_unique_firstentriesentryleftvaluedecode. (((sto_left_multiply_unique_firstentries) = 2 * ge_signed_half_multiply_unique_firstentriesentryleftvaluedecode + 1 /\ (ge_balance_positive_multiply_unique_firstentriesentryleftvalue) = 0) /\ (ge_balance_negative_multiply_unique_firstentriesentryleftvalue) = S ge_signed_half_multiply_unique_firstentriesentryleftvaluedecode))) /\ ((dst_positive_multiply_unique_firstentriesentryleft) + ge_balance_negative_multiply_unique_firstentriesentryleftvalue = (dst_negative_multiply_unique_firstentriesentryleft) + ge_balance_positive_multiply_unique_firstentriesentryleftvalue))))))))) /\ (((exists dst_positive_code_multiply_unique_firstentriesentryright dst_positive_scale_multiply_unique_firstentriesentryright dst_negative_code_multiply_unique_firstentriesentryright dst_negative_scale_multiply_unique_firstentriesentryright dst_positive_multiply_unique_firstentriesentryright dst_negative_multiply_unique_firstentriesentryright. (((G) = (((((dst_positive_code_multiply_unique_firstentriesentryright) + (dst_positive_scale_multiply_unique_firstentriesentryright)) * S ((dst_positive_code_multiply_unique_firstentriesentryright) + (dst_positive_scale_multiply_unique_firstentriesentryright)) + ((dst_positive_scale_multiply_unique_firstentriesentryright) + (dst_positive_scale_multiply_unique_firstentriesentryright))) + (((dst_negative_code_multiply_unique_firstentriesentryright) + (dst_negative_scale_multiply_unique_firstentriesentryright)) * S ((dst_negative_code_multiply_unique_firstentriesentryright) + (dst_negative_scale_multiply_unique_firstentriesentryright)) + ((dst_negative_scale_multiply_unique_firstentriesentryright) + (dst_negative_scale_multiply_unique_firstentriesentryright)))) * S ((((dst_positive_code_multiply_unique_firstentriesentryright) + (dst_positive_scale_multiply_unique_firstentriesentryright)) * S ((dst_positive_code_multiply_unique_firstentriesentryright) + (dst_positive_scale_multiply_unique_firstentriesentryright)) + ((dst_positive_scale_multiply_unique_firstentriesentryright) + (dst_positive_scale_multiply_unique_firstentriesentryright))) + (((dst_negative_code_multiply_unique_firstentriesentryright) + (dst_negative_scale_multiply_unique_firstentriesentryright)) * S ((dst_negative_code_multiply_unique_firstentriesentryright) + (dst_negative_scale_multiply_unique_firstentriesentryright)) + ((dst_negative_scale_multiply_unique_firstentriesentryright) + (dst_negative_scale_multiply_unique_firstentriesentryright)))) + ((((dst_negative_code_multiply_unique_firstentriesentryright) + (dst_negative_scale_multiply_unique_firstentriesentryright)) * S ((dst_negative_code_multiply_unique_firstentriesentryright) + (dst_negative_scale_multiply_unique_firstentriesentryright)) + ((dst_negative_scale_multiply_unique_firstentriesentryright) + (dst_negative_scale_multiply_unique_firstentriesentryright))) + (((dst_negative_code_multiply_unique_firstentriesentryright) + (dst_negative_scale_multiply_unique_firstentriesentryright)) * S ((dst_negative_code_multiply_unique_firstentriesentryright) + (dst_negative_scale_multiply_unique_firstentriesentryright)) + ((dst_negative_scale_multiply_unique_firstentriesentryright) + (dst_negative_scale_multiply_unique_firstentriesentryright)))))) /\ (((((exists ff_h_pvs_multiply_unique_firstentriesentryrightpositive. ff_h_pvs_multiply_unique_firstentriesentryrightpositive + S (dst_positive_multiply_unique_firstentriesentryright) = S ((S (sto_index_multiply_unique_firstentries)) * dst_positive_scale_multiply_unique_firstentriesentryright)) /\ exists ff_q_pvs_multiply_unique_firstentriesentryrightpositive. dst_positive_code_multiply_unique_firstentriesentryright = ff_q_pvs_multiply_unique_firstentriesentryrightpositive * S ((S (sto_index_multiply_unique_firstentries)) * dst_positive_scale_multiply_unique_firstentriesentryright) + (dst_positive_multiply_unique_firstentriesentryright))) /\ (((((exists ff_h_pvs_multiply_unique_firstentriesentryrightnegative. ff_h_pvs_multiply_unique_firstentriesentryrightnegative + S (dst_negative_multiply_unique_firstentriesentryright) = S ((S (sto_index_multiply_unique_firstentries)) * dst_negative_scale_multiply_unique_firstentriesentryright)) /\ exists ff_q_pvs_multiply_unique_firstentriesentryrightnegative. dst_negative_code_multiply_unique_firstentriesentryright = ff_q_pvs_multiply_unique_firstentriesentryrightnegative * S ((S (sto_index_multiply_unique_firstentries)) * dst_negative_scale_multiply_unique_firstentriesentryright) + (dst_negative_multiply_unique_firstentriesentryright))) /\ (exists ge_balance_positive_multiply_unique_firstentriesentryrightvalue ge_balance_negative_multiply_unique_firstentriesentryrightvalue. (((((sto_right_multiply_unique_firstentries) = 2 * (ge_balance_positive_multiply_unique_firstentriesentryrightvalue) /\ (ge_balance_negative_multiply_unique_firstentriesentryrightvalue) = 0) \/ exists ge_signed_half_multiply_unique_firstentriesentryrightvaluedecode. (((sto_right_multiply_unique_firstentries) = 2 * ge_signed_half_multiply_unique_firstentriesentryrightvaluedecode + 1 /\ (ge_balance_positive_multiply_unique_firstentriesentryrightvalue) = 0) /\ (ge_balance_negative_multiply_unique_firstentriesentryrightvalue) = S ge_signed_half_multiply_unique_firstentriesentryrightvaluedecode))) /\ ((dst_positive_multiply_unique_firstentriesentryright) + ge_balance_negative_multiply_unique_firstentriesentryrightvalue = (dst_negative_multiply_unique_firstentriesentryright) + ge_balance_positive_multiply_unique_firstentriesentryrightvalue))))))))) /\ (((exists dst_positive_code_multiply_unique_firstentriesentryoutput dst_positive_scale_multiply_unique_firstentriesentryoutput dst_negative_code_multiply_unique_firstentriesentryoutput dst_negative_scale_multiply_unique_firstentriesentryoutput dst_positive_multiply_unique_firstentriesentryoutput dst_negative_multiply_unique_firstentriesentryoutput. (((H) = (((((dst_positive_code_multiply_unique_firstentriesentryoutput) + (dst_positive_scale_multiply_unique_firstentriesentryoutput)) * S ((dst_positive_code_multiply_unique_firstentriesentryoutput) + (dst_positive_scale_multiply_unique_firstentriesentryoutput)) + ((dst_positive_scale_multiply_unique_firstentriesentryoutput) + (dst_positive_scale_multiply_unique_firstentriesentryoutput))) + (((dst_negative_code_multiply_unique_firstentriesentryoutput) + (dst_negative_scale_multiply_unique_firstentriesentryoutput)) * S ((dst_negative_code_multiply_unique_firstentriesentryoutput) + (dst_negative_scale_multiply_unique_firstentriesentryoutput)) + ((dst_negative_scale_multiply_unique_firstentriesentryoutput) + (dst_negative_scale_multiply_unique_firstentriesentryoutput)))) * S ((((dst_positive_code_multiply_unique_firstentriesentryoutput) + (dst_positive_scale_multiply_unique_firstentriesentryoutput)) * S ((dst_positive_code_multiply_unique_firstentriesentryoutput) + (dst_positive_scale_multiply_unique_firstentriesentryoutput)) + ((dst_positive_scale_multiply_unique_firstentriesentryoutput) + (dst_positive_scale_multiply_unique_firstentriesentryoutput))) + (((dst_negative_code_multiply_unique_firstentriesentryoutput) + (dst_negative_scale_multiply_unique_firstentriesentryoutput)) * S ((dst_negative_code_multiply_unique_firstentriesentryoutput) + (dst_negative_scale_multiply_unique_firstentriesentryoutput)) + ((dst_negative_scale_multiply_unique_firstentriesentryoutput) + (dst_negative_scale_multiply_unique_firstentriesentryoutput)))) + ((((dst_negative_code_multiply_unique_firstentriesentryoutput) + (dst_negative_scale_multiply_unique_firstentriesentryoutput)) * S ((dst_negative_code_multiply_unique_firstentriesentryoutput) + (dst_negative_scale_multiply_unique_firstentriesentryoutput)) + ((dst_negative_scale_multiply_unique_firstentriesentryoutput) + (dst_negative_scale_multiply_unique_firstentriesentryoutput))) + (((dst_negative_code_multiply_unique_firstentriesentryoutput) + (dst_negative_scale_multiply_unique_firstentriesentryoutput)) * S ((dst_negative_code_multiply_unique_firstentriesentryoutput) + (dst_negative_scale_multiply_unique_firstentriesentryoutput)) + ((dst_negative_scale_multiply_unique_firstentriesentryoutput) + (dst_negative_scale_multiply_unique_firstentriesentryoutput)))))) /\ (((((exists ff_h_pvs_multiply_unique_firstentriesentryoutputpositive. ff_h_pvs_multiply_unique_firstentriesentryoutputpositive + S (dst_positive_multiply_unique_firstentriesentryoutput) = S ((S (sto_index_multiply_unique_firstentries)) * dst_positive_scale_multiply_unique_firstentriesentryoutput)) /\ exists ff_q_pvs_multiply_unique_firstentriesentryoutputpositive. dst_positive_code_multiply_unique_firstentriesentryoutput = ff_q_pvs_multiply_unique_firstentriesentryoutputpositive * S ((S (sto_index_multiply_unique_firstentries)) * dst_positive_scale_multiply_unique_firstentriesentryoutput) + (dst_positive_multiply_unique_firstentriesentryoutput))) /\ (((((exists ff_h_pvs_multiply_unique_firstentriesentryoutputnegative. ff_h_pvs_multiply_unique_firstentriesentryoutputnegative + S (dst_negative_multiply_unique_firstentriesentryoutput) = S ((S (sto_index_multiply_unique_firstentries)) * dst_negative_scale_multiply_unique_firstentriesentryoutput)) /\ exists ff_q_pvs_multiply_unique_firstentriesentryoutputnegative. dst_negative_code_multiply_unique_firstentriesentryoutput = ff_q_pvs_multiply_unique_firstentriesentryoutputnegative * S ((S (sto_index_multiply_unique_firstentries)) * dst_negative_scale_multiply_unique_firstentriesentryoutput) + (dst_negative_multiply_unique_firstentriesentryoutput))) /\ (exists ge_balance_positive_multiply_unique_firstentriesentryoutputvalue ge_balance_negative_multiply_unique_firstentriesentryoutputvalue. (((((sto_output_multiply_unique_firstentries) = 2 * (ge_balance_positive_multiply_unique_firstentriesentryoutputvalue) /\ (ge_balance_negative_multiply_unique_firstentriesentryoutputvalue) = 0) \/ exists ge_signed_half_multiply_unique_firstentriesentryoutputvaluedecode. (((sto_output_multiply_unique_firstentries) = 2 * ge_signed_half_multiply_unique_firstentriesentryoutputvaluedecode + 1 /\ (ge_balance_positive_multiply_unique_firstentriesentryoutputvalue) = 0) /\ (ge_balance_negative_multiply_unique_firstentriesentryoutputvalue) = S ge_signed_half_multiply_unique_firstentriesentryoutputvaluedecode))) /\ ((dst_positive_multiply_unique_firstentriesentryoutput) + ge_balance_negative_multiply_unique_firstentriesentryoutputvalue = (dst_negative_multiply_unique_firstentriesentryoutput) + ge_balance_positive_multiply_unique_firstentriesentryoutputvalue))))))))) /\ (exists sto_ap_multiply_unique_firstentriesentryoperation sto_an_multiply_unique_firstentriesentryoperation sto_bp_multiply_unique_firstentriesentryoperation sto_bn_multiply_unique_firstentriesentryoperation sto_cp_multiply_unique_firstentriesentryoperation sto_cn_multiply_unique_firstentriesentryoperation. (((((sto_left_multiply_unique_firstentries) = 2 * (sto_ap_multiply_unique_firstentriesentryoperation) /\ (sto_an_multiply_unique_firstentriesentryoperation) = 0) \/ exists ge_signed_half_multiply_unique_firstentriesentryoperationleft. (((sto_left_multiply_unique_firstentries) = 2 * ge_signed_half_multiply_unique_firstentriesentryoperationleft + 1 /\ (sto_ap_multiply_unique_firstentriesentryoperation) = 0) /\ (sto_an_multiply_unique_firstentriesentryoperation) = S ge_signed_half_multiply_unique_firstentriesentryoperationleft))) /\ ((((((sto_right_multiply_unique_firstentries) = 2 * (sto_bp_multiply_unique_firstentriesentryoperation) /\ (sto_bn_multiply_unique_firstentriesentryoperation) = 0) \/ exists ge_signed_half_multiply_unique_firstentriesentryoperationright. (((sto_right_multiply_unique_firstentries) = 2 * ge_signed_half_multiply_unique_firstentriesentryoperationright + 1 /\ (sto_bp_multiply_unique_firstentriesentryoperation) = 0) /\ (sto_bn_multiply_unique_firstentriesentryoperation) = S ge_signed_half_multiply_unique_firstentriesentryoperationright))) /\ ((((((sto_output_multiply_unique_firstentries) = 2 * (sto_cp_multiply_unique_firstentriesentryoperation) /\ (sto_cn_multiply_unique_firstentriesentryoperation) = 0) \/ exists ge_signed_half_multiply_unique_firstentriesentryoperationoutput. (((sto_output_multiply_unique_firstentries) = 2 * ge_signed_half_multiply_unique_firstentriesentryoperationoutput + 1 /\ (sto_cp_multiply_unique_firstentriesentryoperation) = 0) /\ (sto_cn_multiply_unique_firstentriesentryoperation) = S ge_signed_half_multiply_unique_firstentriesentryoperationoutput))) /\ ((sto_ap_multiply_unique_firstentriesentryoperation * sto_bp_multiply_unique_firstentriesentryoperation + sto_an_multiply_unique_firstentriesentryoperation * sto_bn_multiply_unique_firstentriesentryoperation) + sto_cn_multiply_unique_firstentriesentryoperation = (sto_ap_multiply_unique_firstentriesentryoperation * sto_bn_multiply_unique_firstentriesentryoperation + sto_an_multiply_unique_firstentriesentryoperation * sto_bp_multiply_unique_firstentriesentryoperation) + sto_cp_multiply_unique_firstentriesentryoperation))))))))))))))))))) -> (((exists dst_positive_code_multiply_unique_secondleft_table dst_positive_scale_multiply_unique_secondleft_table dst_negative_code_multiply_unique_secondleft_table dst_negative_scale_multiply_unique_secondleft_table. (((F) = (((((dst_positive_code_multiply_unique_secondleft_table) + (dst_positive_scale_multiply_unique_secondleft_table)) * S ((dst_positive_code_multiply_unique_secondleft_table) + (dst_positive_scale_multiply_unique_secondleft_table)) + ((dst_positive_scale_multiply_unique_secondleft_table) + (dst_positive_scale_multiply_unique_secondleft_table))) + (((dst_negative_code_multiply_unique_secondleft_table) + (dst_negative_scale_multiply_unique_secondleft_table)) * S ((dst_negative_code_multiply_unique_secondleft_table) + (dst_negative_scale_multiply_unique_secondleft_table)) + ((dst_negative_scale_multiply_unique_secondleft_table) + (dst_negative_scale_multiply_unique_secondleft_table)))) * S ((((dst_positive_code_multiply_unique_secondleft_table) + (dst_positive_scale_multiply_unique_secondleft_table)) * S ((dst_positive_code_multiply_unique_secondleft_table) + (dst_positive_scale_multiply_unique_secondleft_table)) + ((dst_positive_scale_multiply_unique_secondleft_table) + (dst_positive_scale_multiply_unique_secondleft_table))) + (((dst_negative_code_multiply_unique_secondleft_table) + (dst_negative_scale_multiply_unique_secondleft_table)) * S ((dst_negative_code_multiply_unique_secondleft_table) + (dst_negative_scale_multiply_unique_secondleft_table)) + ((dst_negative_scale_multiply_unique_secondleft_table) + (dst_negative_scale_multiply_unique_secondleft_table)))) + ((((dst_negative_code_multiply_unique_secondleft_table) + (dst_negative_scale_multiply_unique_secondleft_table)) * S ((dst_negative_code_multiply_unique_secondleft_table) + (dst_negative_scale_multiply_unique_secondleft_table)) + ((dst_negative_scale_multiply_unique_secondleft_table) + (dst_negative_scale_multiply_unique_secondleft_table))) + (((dst_negative_code_multiply_unique_secondleft_table) + (dst_negative_scale_multiply_unique_secondleft_table)) * S ((dst_negative_code_multiply_unique_secondleft_table) + (dst_negative_scale_multiply_unique_secondleft_table)) + ((dst_negative_scale_multiply_unique_secondleft_table) + (dst_negative_scale_multiply_unique_secondleft_table)))))) /\ (forall dst_index_multiply_unique_secondleft_table. (exists pvs_le_gap_multiply_unique_secondleft_tabledomain. pvs_le_gap_multiply_unique_secondleft_tabledomain + (dst_index_multiply_unique_secondleft_table) = (l)) -> exists dst_positive_multiply_unique_secondleft_table dst_negative_multiply_unique_secondleft_table dst_value_multiply_unique_secondleft_table. ((((exists ff_h_pvs_multiply_unique_secondleft_tableentrypositive. ff_h_pvs_multiply_unique_secondleft_tableentrypositive + S (dst_positive_multiply_unique_secondleft_table) = S ((S (dst_index_multiply_unique_secondleft_table)) * dst_positive_scale_multiply_unique_secondleft_table)) /\ exists ff_q_pvs_multiply_unique_secondleft_tableentrypositive. dst_positive_code_multiply_unique_secondleft_table = ff_q_pvs_multiply_unique_secondleft_tableentrypositive * S ((S (dst_index_multiply_unique_secondleft_table)) * dst_positive_scale_multiply_unique_secondleft_table) + (dst_positive_multiply_unique_secondleft_table))) /\ (((((exists ff_h_pvs_multiply_unique_secondleft_tableentrynegative. ff_h_pvs_multiply_unique_secondleft_tableentrynegative + S (dst_negative_multiply_unique_secondleft_table) = S ((S (dst_index_multiply_unique_secondleft_table)) * dst_negative_scale_multiply_unique_secondleft_table)) /\ exists ff_q_pvs_multiply_unique_secondleft_tableentrynegative. dst_negative_code_multiply_unique_secondleft_table = ff_q_pvs_multiply_unique_secondleft_tableentrynegative * S ((S (dst_index_multiply_unique_secondleft_table)) * dst_negative_scale_multiply_unique_secondleft_table) + (dst_negative_multiply_unique_secondleft_table))) /\ (exists ge_balance_positive_multiply_unique_secondleft_tableentryvalue ge_balance_negative_multiply_unique_secondleft_tableentryvalue. (((((dst_value_multiply_unique_secondleft_table) = 2 * (ge_balance_positive_multiply_unique_secondleft_tableentryvalue) /\ (ge_balance_negative_multiply_unique_secondleft_tableentryvalue) = 0) \/ exists ge_signed_half_multiply_unique_secondleft_tableentryvaluedecode. (((dst_value_multiply_unique_secondleft_table) = 2 * ge_signed_half_multiply_unique_secondleft_tableentryvaluedecode + 1 /\ (ge_balance_positive_multiply_unique_secondleft_tableentryvalue) = 0) /\ (ge_balance_negative_multiply_unique_secondleft_tableentryvalue) = S ge_signed_half_multiply_unique_secondleft_tableentryvaluedecode))) /\ ((dst_positive_multiply_unique_secondleft_table) + ge_balance_negative_multiply_unique_secondleft_tableentryvalue = (dst_negative_multiply_unique_secondleft_table) + ge_balance_positive_multiply_unique_secondleft_tableentryvalue))))))))) /\ (((exists dst_positive_code_multiply_unique_secondright_table dst_positive_scale_multiply_unique_secondright_table dst_negative_code_multiply_unique_secondright_table dst_negative_scale_multiply_unique_secondright_table. (((G) = (((((dst_positive_code_multiply_unique_secondright_table) + (dst_positive_scale_multiply_unique_secondright_table)) * S ((dst_positive_code_multiply_unique_secondright_table) + (dst_positive_scale_multiply_unique_secondright_table)) + ((dst_positive_scale_multiply_unique_secondright_table) + (dst_positive_scale_multiply_unique_secondright_table))) + (((dst_negative_code_multiply_unique_secondright_table) + (dst_negative_scale_multiply_unique_secondright_table)) * S ((dst_negative_code_multiply_unique_secondright_table) + (dst_negative_scale_multiply_unique_secondright_table)) + ((dst_negative_scale_multiply_unique_secondright_table) + (dst_negative_scale_multiply_unique_secondright_table)))) * S ((((dst_positive_code_multiply_unique_secondright_table) + (dst_positive_scale_multiply_unique_secondright_table)) * S ((dst_positive_code_multiply_unique_secondright_table) + (dst_positive_scale_multiply_unique_secondright_table)) + ((dst_positive_scale_multiply_unique_secondright_table) + (dst_positive_scale_multiply_unique_secondright_table))) + (((dst_negative_code_multiply_unique_secondright_table) + (dst_negative_scale_multiply_unique_secondright_table)) * S ((dst_negative_code_multiply_unique_secondright_table) + (dst_negative_scale_multiply_unique_secondright_table)) + ((dst_negative_scale_multiply_unique_secondright_table) + (dst_negative_scale_multiply_unique_secondright_table)))) + ((((dst_negative_code_multiply_unique_secondright_table) + (dst_negative_scale_multiply_unique_secondright_table)) * S ((dst_negative_code_multiply_unique_secondright_table) + (dst_negative_scale_multiply_unique_secondright_table)) + ((dst_negative_scale_multiply_unique_secondright_table) + (dst_negative_scale_multiply_unique_secondright_table))) + (((dst_negative_code_multiply_unique_secondright_table) + (dst_negative_scale_multiply_unique_secondright_table)) * S ((dst_negative_code_multiply_unique_secondright_table) + (dst_negative_scale_multiply_unique_secondright_table)) + ((dst_negative_scale_multiply_unique_secondright_table) + (dst_negative_scale_multiply_unique_secondright_table)))))) /\ (forall dst_index_multiply_unique_secondright_table. (exists pvs_le_gap_multiply_unique_secondright_tabledomain. pvs_le_gap_multiply_unique_secondright_tabledomain + (dst_index_multiply_unique_secondright_table) = (l)) -> exists dst_positive_multiply_unique_secondright_table dst_negative_multiply_unique_secondright_table dst_value_multiply_unique_secondright_table. ((((exists ff_h_pvs_multiply_unique_secondright_tableentrypositive. ff_h_pvs_multiply_unique_secondright_tableentrypositive + S (dst_positive_multiply_unique_secondright_table) = S ((S (dst_index_multiply_unique_secondright_table)) * dst_positive_scale_multiply_unique_secondright_table)) /\ exists ff_q_pvs_multiply_unique_secondright_tableentrypositive. dst_positive_code_multiply_unique_secondright_table = ff_q_pvs_multiply_unique_secondright_tableentrypositive * S ((S (dst_index_multiply_unique_secondright_table)) * dst_positive_scale_multiply_unique_secondright_table) + (dst_positive_multiply_unique_secondright_table))) /\ (((((exists ff_h_pvs_multiply_unique_secondright_tableentrynegative. ff_h_pvs_multiply_unique_secondright_tableentrynegative + S (dst_negative_multiply_unique_secondright_table) = S ((S (dst_index_multiply_unique_secondright_table)) * dst_negative_scale_multiply_unique_secondright_table)) /\ exists ff_q_pvs_multiply_unique_secondright_tableentrynegative. dst_negative_code_multiply_unique_secondright_table = ff_q_pvs_multiply_unique_secondright_tableentrynegative * S ((S (dst_index_multiply_unique_secondright_table)) * dst_negative_scale_multiply_unique_secondright_table) + (dst_negative_multiply_unique_secondright_table))) /\ (exists ge_balance_positive_multiply_unique_secondright_tableentryvalue ge_balance_negative_multiply_unique_secondright_tableentryvalue. (((((dst_value_multiply_unique_secondright_table) = 2 * (ge_balance_positive_multiply_unique_secondright_tableentryvalue) /\ (ge_balance_negative_multiply_unique_secondright_tableentryvalue) = 0) \/ exists ge_signed_half_multiply_unique_secondright_tableentryvaluedecode. (((dst_value_multiply_unique_secondright_table) = 2 * ge_signed_half_multiply_unique_secondright_tableentryvaluedecode + 1 /\ (ge_balance_positive_multiply_unique_secondright_tableentryvalue) = 0) /\ (ge_balance_negative_multiply_unique_secondright_tableentryvalue) = S ge_signed_half_multiply_unique_secondright_tableentryvaluedecode))) /\ ((dst_positive_multiply_unique_secondright_table) + ge_balance_negative_multiply_unique_secondright_tableentryvalue = (dst_negative_multiply_unique_secondright_table) + ge_balance_positive_multiply_unique_secondright_tableentryvalue))))))))) /\ (((exists dst_positive_code_multiply_unique_secondoutput_table dst_positive_scale_multiply_unique_secondoutput_table dst_negative_code_multiply_unique_secondoutput_table dst_negative_scale_multiply_unique_secondoutput_table. (((K) = (((((dst_positive_code_multiply_unique_secondoutput_table) + (dst_positive_scale_multiply_unique_secondoutput_table)) * S ((dst_positive_code_multiply_unique_secondoutput_table) + (dst_positive_scale_multiply_unique_secondoutput_table)) + ((dst_positive_scale_multiply_unique_secondoutput_table) + (dst_positive_scale_multiply_unique_secondoutput_table))) + (((dst_negative_code_multiply_unique_secondoutput_table) + (dst_negative_scale_multiply_unique_secondoutput_table)) * S ((dst_negative_code_multiply_unique_secondoutput_table) + (dst_negative_scale_multiply_unique_secondoutput_table)) + ((dst_negative_scale_multiply_unique_secondoutput_table) + (dst_negative_scale_multiply_unique_secondoutput_table)))) * S ((((dst_positive_code_multiply_unique_secondoutput_table) + (dst_positive_scale_multiply_unique_secondoutput_table)) * S ((dst_positive_code_multiply_unique_secondoutput_table) + (dst_positive_scale_multiply_unique_secondoutput_table)) + ((dst_positive_scale_multiply_unique_secondoutput_table) + (dst_positive_scale_multiply_unique_secondoutput_table))) + (((dst_negative_code_multiply_unique_secondoutput_table) + (dst_negative_scale_multiply_unique_secondoutput_table)) * S ((dst_negative_code_multiply_unique_secondoutput_table) + (dst_negative_scale_multiply_unique_secondoutput_table)) + ((dst_negative_scale_multiply_unique_secondoutput_table) + (dst_negative_scale_multiply_unique_secondoutput_table)))) + ((((dst_negative_code_multiply_unique_secondoutput_table) + (dst_negative_scale_multiply_unique_secondoutput_table)) * S ((dst_negative_code_multiply_unique_secondoutput_table) + (dst_negative_scale_multiply_unique_secondoutput_table)) + ((dst_negative_scale_multiply_unique_secondoutput_table) + (dst_negative_scale_multiply_unique_secondoutput_table))) + (((dst_negative_code_multiply_unique_secondoutput_table) + (dst_negative_scale_multiply_unique_secondoutput_table)) * S ((dst_negative_code_multiply_unique_secondoutput_table) + (dst_negative_scale_multiply_unique_secondoutput_table)) + ((dst_negative_scale_multiply_unique_secondoutput_table) + (dst_negative_scale_multiply_unique_secondoutput_table)))))) /\ (forall dst_index_multiply_unique_secondoutput_table. (exists pvs_le_gap_multiply_unique_secondoutput_tabledomain. pvs_le_gap_multiply_unique_secondoutput_tabledomain + (dst_index_multiply_unique_secondoutput_table) = (l)) -> exists dst_positive_multiply_unique_secondoutput_table dst_negative_multiply_unique_secondoutput_table dst_value_multiply_unique_secondoutput_table. ((((exists ff_h_pvs_multiply_unique_secondoutput_tableentrypositive. ff_h_pvs_multiply_unique_secondoutput_tableentrypositive + S (dst_positive_multiply_unique_secondoutput_table) = S ((S (dst_index_multiply_unique_secondoutput_table)) * dst_positive_scale_multiply_unique_secondoutput_table)) /\ exists ff_q_pvs_multiply_unique_secondoutput_tableentrypositive. dst_positive_code_multiply_unique_secondoutput_table = ff_q_pvs_multiply_unique_secondoutput_tableentrypositive * S ((S (dst_index_multiply_unique_secondoutput_table)) * dst_positive_scale_multiply_unique_secondoutput_table) + (dst_positive_multiply_unique_secondoutput_table))) /\ (((((exists ff_h_pvs_multiply_unique_secondoutput_tableentrynegative. ff_h_pvs_multiply_unique_secondoutput_tableentrynegative + S (dst_negative_multiply_unique_secondoutput_table) = S ((S (dst_index_multiply_unique_secondoutput_table)) * dst_negative_scale_multiply_unique_secondoutput_table)) /\ exists ff_q_pvs_multiply_unique_secondoutput_tableentrynegative. dst_negative_code_multiply_unique_secondoutput_table = ff_q_pvs_multiply_unique_secondoutput_tableentrynegative * S ((S (dst_index_multiply_unique_secondoutput_table)) * dst_negative_scale_multiply_unique_secondoutput_table) + (dst_negative_multiply_unique_secondoutput_table))) /\ (exists ge_balance_positive_multiply_unique_secondoutput_tableentryvalue ge_balance_negative_multiply_unique_secondoutput_tableentryvalue. (((((dst_value_multiply_unique_secondoutput_table) = 2 * (ge_balance_positive_multiply_unique_secondoutput_tableentryvalue) /\ (ge_balance_negative_multiply_unique_secondoutput_tableentryvalue) = 0) \/ exists ge_signed_half_multiply_unique_secondoutput_tableentryvaluedecode. (((dst_value_multiply_unique_secondoutput_table) = 2 * ge_signed_half_multiply_unique_secondoutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_multiply_unique_secondoutput_tableentryvalue) = 0) /\ (ge_balance_negative_multiply_unique_secondoutput_tableentryvalue) = S ge_signed_half_multiply_unique_secondoutput_tableentryvaluedecode))) /\ ((dst_positive_multiply_unique_secondoutput_table) + ge_balance_negative_multiply_unique_secondoutput_tableentryvalue = (dst_negative_multiply_unique_secondoutput_table) + ge_balance_positive_multiply_unique_secondoutput_tableentryvalue))))))))) /\ (forall sto_index_multiply_unique_secondentries. (exists pvs_gap_multiply_unique_secondentriesbound. pvs_gap_multiply_unique_secondentriesbound + S (sto_index_multiply_unique_secondentries) = (l)) -> exists sto_left_multiply_unique_secondentries sto_right_multiply_unique_secondentries sto_output_multiply_unique_secondentries. ((exists dst_positive_code_multiply_unique_secondentriesentryleft dst_positive_scale_multiply_unique_secondentriesentryleft dst_negative_code_multiply_unique_secondentriesentryleft dst_negative_scale_multiply_unique_secondentriesentryleft dst_positive_multiply_unique_secondentriesentryleft dst_negative_multiply_unique_secondentriesentryleft. (((F) = (((((dst_positive_code_multiply_unique_secondentriesentryleft) + (dst_positive_scale_multiply_unique_secondentriesentryleft)) * S ((dst_positive_code_multiply_unique_secondentriesentryleft) + (dst_positive_scale_multiply_unique_secondentriesentryleft)) + ((dst_positive_scale_multiply_unique_secondentriesentryleft) + (dst_positive_scale_multiply_unique_secondentriesentryleft))) + (((dst_negative_code_multiply_unique_secondentriesentryleft) + (dst_negative_scale_multiply_unique_secondentriesentryleft)) * S ((dst_negative_code_multiply_unique_secondentriesentryleft) + (dst_negative_scale_multiply_unique_secondentriesentryleft)) + ((dst_negative_scale_multiply_unique_secondentriesentryleft) + (dst_negative_scale_multiply_unique_secondentriesentryleft)))) * S ((((dst_positive_code_multiply_unique_secondentriesentryleft) + (dst_positive_scale_multiply_unique_secondentriesentryleft)) * S ((dst_positive_code_multiply_unique_secondentriesentryleft) + (dst_positive_scale_multiply_unique_secondentriesentryleft)) + ((dst_positive_scale_multiply_unique_secondentriesentryleft) + (dst_positive_scale_multiply_unique_secondentriesentryleft))) + (((dst_negative_code_multiply_unique_secondentriesentryleft) + (dst_negative_scale_multiply_unique_secondentriesentryleft)) * S ((dst_negative_code_multiply_unique_secondentriesentryleft) + (dst_negative_scale_multiply_unique_secondentriesentryleft)) + ((dst_negative_scale_multiply_unique_secondentriesentryleft) + (dst_negative_scale_multiply_unique_secondentriesentryleft)))) + ((((dst_negative_code_multiply_unique_secondentriesentryleft) + (dst_negative_scale_multiply_unique_secondentriesentryleft)) * S ((dst_negative_code_multiply_unique_secondentriesentryleft) + (dst_negative_scale_multiply_unique_secondentriesentryleft)) + ((dst_negative_scale_multiply_unique_secondentriesentryleft) + (dst_negative_scale_multiply_unique_secondentriesentryleft))) + (((dst_negative_code_multiply_unique_secondentriesentryleft) + (dst_negative_scale_multiply_unique_secondentriesentryleft)) * S ((dst_negative_code_multiply_unique_secondentriesentryleft) + (dst_negative_scale_multiply_unique_secondentriesentryleft)) + ((dst_negative_scale_multiply_unique_secondentriesentryleft) + (dst_negative_scale_multiply_unique_secondentriesentryleft)))))) /\ (((((exists ff_h_pvs_multiply_unique_secondentriesentryleftpositive. ff_h_pvs_multiply_unique_secondentriesentryleftpositive + S (dst_positive_multiply_unique_secondentriesentryleft) = S ((S (sto_index_multiply_unique_secondentries)) * dst_positive_scale_multiply_unique_secondentriesentryleft)) /\ exists ff_q_pvs_multiply_unique_secondentriesentryleftpositive. dst_positive_code_multiply_unique_secondentriesentryleft = ff_q_pvs_multiply_unique_secondentriesentryleftpositive * S ((S (sto_index_multiply_unique_secondentries)) * dst_positive_scale_multiply_unique_secondentriesentryleft) + (dst_positive_multiply_unique_secondentriesentryleft))) /\ (((((exists ff_h_pvs_multiply_unique_secondentriesentryleftnegative. ff_h_pvs_multiply_unique_secondentriesentryleftnegative + S (dst_negative_multiply_unique_secondentriesentryleft) = S ((S (sto_index_multiply_unique_secondentries)) * dst_negative_scale_multiply_unique_secondentriesentryleft)) /\ exists ff_q_pvs_multiply_unique_secondentriesentryleftnegative. dst_negative_code_multiply_unique_secondentriesentryleft = ff_q_pvs_multiply_unique_secondentriesentryleftnegative * S ((S (sto_index_multiply_unique_secondentries)) * dst_negative_scale_multiply_unique_secondentriesentryleft) + (dst_negative_multiply_unique_secondentriesentryleft))) /\ (exists ge_balance_positive_multiply_unique_secondentriesentryleftvalue ge_balance_negative_multiply_unique_secondentriesentryleftvalue. (((((sto_left_multiply_unique_secondentries) = 2 * (ge_balance_positive_multiply_unique_secondentriesentryleftvalue) /\ (ge_balance_negative_multiply_unique_secondentriesentryleftvalue) = 0) \/ exists ge_signed_half_multiply_unique_secondentriesentryleftvaluedecode. (((sto_left_multiply_unique_secondentries) = 2 * ge_signed_half_multiply_unique_secondentriesentryleftvaluedecode + 1 /\ (ge_balance_positive_multiply_unique_secondentriesentryleftvalue) = 0) /\ (ge_balance_negative_multiply_unique_secondentriesentryleftvalue) = S ge_signed_half_multiply_unique_secondentriesentryleftvaluedecode))) /\ ((dst_positive_multiply_unique_secondentriesentryleft) + ge_balance_negative_multiply_unique_secondentriesentryleftvalue = (dst_negative_multiply_unique_secondentriesentryleft) + ge_balance_positive_multiply_unique_secondentriesentryleftvalue))))))))) /\ (((exists dst_positive_code_multiply_unique_secondentriesentryright dst_positive_scale_multiply_unique_secondentriesentryright dst_negative_code_multiply_unique_secondentriesentryright dst_negative_scale_multiply_unique_secondentriesentryright dst_positive_multiply_unique_secondentriesentryright dst_negative_multiply_unique_secondentriesentryright. (((G) = (((((dst_positive_code_multiply_unique_secondentriesentryright) + (dst_positive_scale_multiply_unique_secondentriesentryright)) * S ((dst_positive_code_multiply_unique_secondentriesentryright) + (dst_positive_scale_multiply_unique_secondentriesentryright)) + ((dst_positive_scale_multiply_unique_secondentriesentryright) + (dst_positive_scale_multiply_unique_secondentriesentryright))) + (((dst_negative_code_multiply_unique_secondentriesentryright) + (dst_negative_scale_multiply_unique_secondentriesentryright)) * S ((dst_negative_code_multiply_unique_secondentriesentryright) + (dst_negative_scale_multiply_unique_secondentriesentryright)) + ((dst_negative_scale_multiply_unique_secondentriesentryright) + (dst_negative_scale_multiply_unique_secondentriesentryright)))) * S ((((dst_positive_code_multiply_unique_secondentriesentryright) + (dst_positive_scale_multiply_unique_secondentriesentryright)) * S ((dst_positive_code_multiply_unique_secondentriesentryright) + (dst_positive_scale_multiply_unique_secondentriesentryright)) + ((dst_positive_scale_multiply_unique_secondentriesentryright) + (dst_positive_scale_multiply_unique_secondentriesentryright))) + (((dst_negative_code_multiply_unique_secondentriesentryright) + (dst_negative_scale_multiply_unique_secondentriesentryright)) * S ((dst_negative_code_multiply_unique_secondentriesentryright) + (dst_negative_scale_multiply_unique_secondentriesentryright)) + ((dst_negative_scale_multiply_unique_secondentriesentryright) + (dst_negative_scale_multiply_unique_secondentriesentryright)))) + ((((dst_negative_code_multiply_unique_secondentriesentryright) + (dst_negative_scale_multiply_unique_secondentriesentryright)) * S ((dst_negative_code_multiply_unique_secondentriesentryright) + (dst_negative_scale_multiply_unique_secondentriesentryright)) + ((dst_negative_scale_multiply_unique_secondentriesentryright) + (dst_negative_scale_multiply_unique_secondentriesentryright))) + (((dst_negative_code_multiply_unique_secondentriesentryright) + (dst_negative_scale_multiply_unique_secondentriesentryright)) * S ((dst_negative_code_multiply_unique_secondentriesentryright) + (dst_negative_scale_multiply_unique_secondentriesentryright)) + ((dst_negative_scale_multiply_unique_secondentriesentryright) + (dst_negative_scale_multiply_unique_secondentriesentryright)))))) /\ (((((exists ff_h_pvs_multiply_unique_secondentriesentryrightpositive. ff_h_pvs_multiply_unique_secondentriesentryrightpositive + S (dst_positive_multiply_unique_secondentriesentryright) = S ((S (sto_index_multiply_unique_secondentries)) * dst_positive_scale_multiply_unique_secondentriesentryright)) /\ exists ff_q_pvs_multiply_unique_secondentriesentryrightpositive. dst_positive_code_multiply_unique_secondentriesentryright = ff_q_pvs_multiply_unique_secondentriesentryrightpositive * S ((S (sto_index_multiply_unique_secondentries)) * dst_positive_scale_multiply_unique_secondentriesentryright) + (dst_positive_multiply_unique_secondentriesentryright))) /\ (((((exists ff_h_pvs_multiply_unique_secondentriesentryrightnegative. ff_h_pvs_multiply_unique_secondentriesentryrightnegative + S (dst_negative_multiply_unique_secondentriesentryright) = S ((S (sto_index_multiply_unique_secondentries)) * dst_negative_scale_multiply_unique_secondentriesentryright)) /\ exists ff_q_pvs_multiply_unique_secondentriesentryrightnegative. dst_negative_code_multiply_unique_secondentriesentryright = ff_q_pvs_multiply_unique_secondentriesentryrightnegative * S ((S (sto_index_multiply_unique_secondentries)) * dst_negative_scale_multiply_unique_secondentriesentryright) + (dst_negative_multiply_unique_secondentriesentryright))) /\ (exists ge_balance_positive_multiply_unique_secondentriesentryrightvalue ge_balance_negative_multiply_unique_secondentriesentryrightvalue. (((((sto_right_multiply_unique_secondentries) = 2 * (ge_balance_positive_multiply_unique_secondentriesentryrightvalue) /\ (ge_balance_negative_multiply_unique_secondentriesentryrightvalue) = 0) \/ exists ge_signed_half_multiply_unique_secondentriesentryrightvaluedecode. (((sto_right_multiply_unique_secondentries) = 2 * ge_signed_half_multiply_unique_secondentriesentryrightvaluedecode + 1 /\ (ge_balance_positive_multiply_unique_secondentriesentryrightvalue) = 0) /\ (ge_balance_negative_multiply_unique_secondentriesentryrightvalue) = S ge_signed_half_multiply_unique_secondentriesentryrightvaluedecode))) /\ ((dst_positive_multiply_unique_secondentriesentryright) + ge_balance_negative_multiply_unique_secondentriesentryrightvalue = (dst_negative_multiply_unique_secondentriesentryright) + ge_balance_positive_multiply_unique_secondentriesentryrightvalue))))))))) /\ (((exists dst_positive_code_multiply_unique_secondentriesentryoutput dst_positive_scale_multiply_unique_secondentriesentryoutput dst_negative_code_multiply_unique_secondentriesentryoutput dst_negative_scale_multiply_unique_secondentriesentryoutput dst_positive_multiply_unique_secondentriesentryoutput dst_negative_multiply_unique_secondentriesentryoutput. (((K) = (((((dst_positive_code_multiply_unique_secondentriesentryoutput) + (dst_positive_scale_multiply_unique_secondentriesentryoutput)) * S ((dst_positive_code_multiply_unique_secondentriesentryoutput) + (dst_positive_scale_multiply_unique_secondentriesentryoutput)) + ((dst_positive_scale_multiply_unique_secondentriesentryoutput) + (dst_positive_scale_multiply_unique_secondentriesentryoutput))) + (((dst_negative_code_multiply_unique_secondentriesentryoutput) + (dst_negative_scale_multiply_unique_secondentriesentryoutput)) * S ((dst_negative_code_multiply_unique_secondentriesentryoutput) + (dst_negative_scale_multiply_unique_secondentriesentryoutput)) + ((dst_negative_scale_multiply_unique_secondentriesentryoutput) + (dst_negative_scale_multiply_unique_secondentriesentryoutput)))) * S ((((dst_positive_code_multiply_unique_secondentriesentryoutput) + (dst_positive_scale_multiply_unique_secondentriesentryoutput)) * S ((dst_positive_code_multiply_unique_secondentriesentryoutput) + (dst_positive_scale_multiply_unique_secondentriesentryoutput)) + ((dst_positive_scale_multiply_unique_secondentriesentryoutput) + (dst_positive_scale_multiply_unique_secondentriesentryoutput))) + (((dst_negative_code_multiply_unique_secondentriesentryoutput) + (dst_negative_scale_multiply_unique_secondentriesentryoutput)) * S ((dst_negative_code_multiply_unique_secondentriesentryoutput) + (dst_negative_scale_multiply_unique_secondentriesentryoutput)) + ((dst_negative_scale_multiply_unique_secondentriesentryoutput) + (dst_negative_scale_multiply_unique_secondentriesentryoutput)))) + ((((dst_negative_code_multiply_unique_secondentriesentryoutput) + (dst_negative_scale_multiply_unique_secondentriesentryoutput)) * S ((dst_negative_code_multiply_unique_secondentriesentryoutput) + (dst_negative_scale_multiply_unique_secondentriesentryoutput)) + ((dst_negative_scale_multiply_unique_secondentriesentryoutput) + (dst_negative_scale_multiply_unique_secondentriesentryoutput))) + (((dst_negative_code_multiply_unique_secondentriesentryoutput) + (dst_negative_scale_multiply_unique_secondentriesentryoutput)) * S ((dst_negative_code_multiply_unique_secondentriesentryoutput) + (dst_negative_scale_multiply_unique_secondentriesentryoutput)) + ((dst_negative_scale_multiply_unique_secondentriesentryoutput) + (dst_negative_scale_multiply_unique_secondentriesentryoutput)))))) /\ (((((exists ff_h_pvs_multiply_unique_secondentriesentryoutputpositive. ff_h_pvs_multiply_unique_secondentriesentryoutputpositive + S (dst_positive_multiply_unique_secondentriesentryoutput) = S ((S (sto_index_multiply_unique_secondentries)) * dst_positive_scale_multiply_unique_secondentriesentryoutput)) /\ exists ff_q_pvs_multiply_unique_secondentriesentryoutputpositive. dst_positive_code_multiply_unique_secondentriesentryoutput = ff_q_pvs_multiply_unique_secondentriesentryoutputpositive * S ((S (sto_index_multiply_unique_secondentries)) * dst_positive_scale_multiply_unique_secondentriesentryoutput) + (dst_positive_multiply_unique_secondentriesentryoutput))) /\ (((((exists ff_h_pvs_multiply_unique_secondentriesentryoutputnegative. ff_h_pvs_multiply_unique_secondentriesentryoutputnegative + S (dst_negative_multiply_unique_secondentriesentryoutput) = S ((S (sto_index_multiply_unique_secondentries)) * dst_negative_scale_multiply_unique_secondentriesentryoutput)) /\ exists ff_q_pvs_multiply_unique_secondentriesentryoutputnegative. dst_negative_code_multiply_unique_secondentriesentryoutput = ff_q_pvs_multiply_unique_secondentriesentryoutputnegative * S ((S (sto_index_multiply_unique_secondentries)) * dst_negative_scale_multiply_unique_secondentriesentryoutput) + (dst_negative_multiply_unique_secondentriesentryoutput))) /\ (exists ge_balance_positive_multiply_unique_secondentriesentryoutputvalue ge_balance_negative_multiply_unique_secondentriesentryoutputvalue. (((((sto_output_multiply_unique_secondentries) = 2 * (ge_balance_positive_multiply_unique_secondentriesentryoutputvalue) /\ (ge_balance_negative_multiply_unique_secondentriesentryoutputvalue) = 0) \/ exists ge_signed_half_multiply_unique_secondentriesentryoutputvaluedecode. (((sto_output_multiply_unique_secondentries) = 2 * ge_signed_half_multiply_unique_secondentriesentryoutputvaluedecode + 1 /\ (ge_balance_positive_multiply_unique_secondentriesentryoutputvalue) = 0) /\ (ge_balance_negative_multiply_unique_secondentriesentryoutputvalue) = S ge_signed_half_multiply_unique_secondentriesentryoutputvaluedecode))) /\ ((dst_positive_multiply_unique_secondentriesentryoutput) + ge_balance_negative_multiply_unique_secondentriesentryoutputvalue = (dst_negative_multiply_unique_secondentriesentryoutput) + ge_balance_positive_multiply_unique_secondentriesentryoutputvalue))))))))) /\ (exists sto_ap_multiply_unique_secondentriesentryoperation sto_an_multiply_unique_secondentriesentryoperation sto_bp_multiply_unique_secondentriesentryoperation sto_bn_multiply_unique_secondentriesentryoperation sto_cp_multiply_unique_secondentriesentryoperation sto_cn_multiply_unique_secondentriesentryoperation. (((((sto_left_multiply_unique_secondentries) = 2 * (sto_ap_multiply_unique_secondentriesentryoperation) /\ (sto_an_multiply_unique_secondentriesentryoperation) = 0) \/ exists ge_signed_half_multiply_unique_secondentriesentryoperationleft. (((sto_left_multiply_unique_secondentries) = 2 * ge_signed_half_multiply_unique_secondentriesentryoperationleft + 1 /\ (sto_ap_multiply_unique_secondentriesentryoperation) = 0) /\ (sto_an_multiply_unique_secondentriesentryoperation) = S ge_signed_half_multiply_unique_secondentriesentryoperationleft))) /\ ((((((sto_right_multiply_unique_secondentries) = 2 * (sto_bp_multiply_unique_secondentriesentryoperation) /\ (sto_bn_multiply_unique_secondentriesentryoperation) = 0) \/ exists ge_signed_half_multiply_unique_secondentriesentryoperationright. (((sto_right_multiply_unique_secondentries) = 2 * ge_signed_half_multiply_unique_secondentriesentryoperationright + 1 /\ (sto_bp_multiply_unique_secondentriesentryoperation) = 0) /\ (sto_bn_multiply_unique_secondentriesentryoperation) = S ge_signed_half_multiply_unique_secondentriesentryoperationright))) /\ ((((((sto_output_multiply_unique_secondentries) = 2 * (sto_cp_multiply_unique_secondentriesentryoperation) /\ (sto_cn_multiply_unique_secondentriesentryoperation) = 0) \/ exists ge_signed_half_multiply_unique_secondentriesentryoperationoutput. (((sto_output_multiply_unique_secondentries) = 2 * ge_signed_half_multiply_unique_secondentriesentryoperationoutput + 1 /\ (sto_cp_multiply_unique_secondentriesentryoperation) = 0) /\ (sto_cn_multiply_unique_secondentriesentryoperation) = S ge_signed_half_multiply_unique_secondentriesentryoperationoutput))) /\ ((sto_ap_multiply_unique_secondentriesentryoperation * sto_bp_multiply_unique_secondentriesentryoperation + sto_an_multiply_unique_secondentriesentryoperation * sto_bn_multiply_unique_secondentriesentryoperation) + sto_cn_multiply_unique_secondentriesentryoperation = (sto_ap_multiply_unique_secondentriesentryoperation * sto_bn_multiply_unique_secondentriesentryoperation + sto_an_multiply_unique_secondentriesentryoperation * sto_bp_multiply_unique_secondentriesentryoperation) + sto_cp_multiply_unique_secondentriesentryoperation))))))))))))))))))) -> (forall dst_index_multiply_unique_result dst_first_multiply_unique_result dst_second_multiply_unique_result. (exists pvs_gap_multiply_unique_resultbound. pvs_gap_multiply_unique_resultbound + S (dst_index_multiply_unique_result) = (l)) -> (exists dst_positive_code_multiply_unique_resultfirst dst_positive_scale_multiply_unique_resultfirst dst_negative_code_multiply_unique_resultfirst dst_negative_scale_multiply_unique_resultfirst dst_positive_multiply_unique_resultfirst dst_negative_multiply_unique_resultfirst. (((H) = (((((dst_positive_code_multiply_unique_resultfirst) + (dst_positive_scale_multiply_unique_resultfirst)) * S ((dst_positive_code_multiply_unique_resultfirst) + (dst_positive_scale_multiply_unique_resultfirst)) + ((dst_positive_scale_multiply_unique_resultfirst) + (dst_positive_scale_multiply_unique_resultfirst))) + (((dst_negative_code_multiply_unique_resultfirst) + (dst_negative_scale_multiply_unique_resultfirst)) * S ((dst_negative_code_multiply_unique_resultfirst) + (dst_negative_scale_multiply_unique_resultfirst)) + ((dst_negative_scale_multiply_unique_resultfirst) + (dst_negative_scale_multiply_unique_resultfirst)))) * S ((((dst_positive_code_multiply_unique_resultfirst) + (dst_positive_scale_multiply_unique_resultfirst)) * S ((dst_positive_code_multiply_unique_resultfirst) + (dst_positive_scale_multiply_unique_resultfirst)) + ((dst_positive_scale_multiply_unique_resultfirst) + (dst_positive_scale_multiply_unique_resultfirst))) + (((dst_negative_code_multiply_unique_resultfirst) + (dst_negative_scale_multiply_unique_resultfirst)) * S ((dst_negative_code_multiply_unique_resultfirst) + (dst_negative_scale_multiply_unique_resultfirst)) + ((dst_negative_scale_multiply_unique_resultfirst) + (dst_negative_scale_multiply_unique_resultfirst)))) + ((((dst_negative_code_multiply_unique_resultfirst) + (dst_negative_scale_multiply_unique_resultfirst)) * S ((dst_negative_code_multiply_unique_resultfirst) + (dst_negative_scale_multiply_unique_resultfirst)) + ((dst_negative_scale_multiply_unique_resultfirst) + (dst_negative_scale_multiply_unique_resultfirst))) + (((dst_negative_code_multiply_unique_resultfirst) + (dst_negative_scale_multiply_unique_resultfirst)) * S ((dst_negative_code_multiply_unique_resultfirst) + (dst_negative_scale_multiply_unique_resultfirst)) + ((dst_negative_scale_multiply_unique_resultfirst) + (dst_negative_scale_multiply_unique_resultfirst)))))) /\ (((((exists ff_h_pvs_multiply_unique_resultfirstpositive. ff_h_pvs_multiply_unique_resultfirstpositive + S (dst_positive_multiply_unique_resultfirst) = S ((S (dst_index_multiply_unique_result)) * dst_positive_scale_multiply_unique_resultfirst)) /\ exists ff_q_pvs_multiply_unique_resultfirstpositive. dst_positive_code_multiply_unique_resultfirst = ff_q_pvs_multiply_unique_resultfirstpositive * S ((S (dst_index_multiply_unique_result)) * dst_positive_scale_multiply_unique_resultfirst) + (dst_positive_multiply_unique_resultfirst))) /\ (((((exists ff_h_pvs_multiply_unique_resultfirstnegative. ff_h_pvs_multiply_unique_resultfirstnegative + S (dst_negative_multiply_unique_resultfirst) = S ((S (dst_index_multiply_unique_result)) * dst_negative_scale_multiply_unique_resultfirst)) /\ exists ff_q_pvs_multiply_unique_resultfirstnegative. dst_negative_code_multiply_unique_resultfirst = ff_q_pvs_multiply_unique_resultfirstnegative * S ((S (dst_index_multiply_unique_result)) * dst_negative_scale_multiply_unique_resultfirst) + (dst_negative_multiply_unique_resultfirst))) /\ (exists ge_balance_positive_multiply_unique_resultfirstvalue ge_balance_negative_multiply_unique_resultfirstvalue. (((((dst_first_multiply_unique_result) = 2 * (ge_balance_positive_multiply_unique_resultfirstvalue) /\ (ge_balance_negative_multiply_unique_resultfirstvalue) = 0) \/ exists ge_signed_half_multiply_unique_resultfirstvaluedecode. (((dst_first_multiply_unique_result) = 2 * ge_signed_half_multiply_unique_resultfirstvaluedecode + 1 /\ (ge_balance_positive_multiply_unique_resultfirstvalue) = 0) /\ (ge_balance_negative_multiply_unique_resultfirstvalue) = S ge_signed_half_multiply_unique_resultfirstvaluedecode))) /\ ((dst_positive_multiply_unique_resultfirst) + ge_balance_negative_multiply_unique_resultfirstvalue = (dst_negative_multiply_unique_resultfirst) + ge_balance_positive_multiply_unique_resultfirstvalue))))))))) -> (exists dst_positive_code_multiply_unique_resultsecond dst_positive_scale_multiply_unique_resultsecond dst_negative_code_multiply_unique_resultsecond dst_negative_scale_multiply_unique_resultsecond dst_positive_multiply_unique_resultsecond dst_negative_multiply_unique_resultsecond. (((K) = (((((dst_positive_code_multiply_unique_resultsecond) + (dst_positive_scale_multiply_unique_resultsecond)) * S ((dst_positive_code_multiply_unique_resultsecond) + (dst_positive_scale_multiply_unique_resultsecond)) + ((dst_positive_scale_multiply_unique_resultsecond) + (dst_positive_scale_multiply_unique_resultsecond))) + (((dst_negative_code_multiply_unique_resultsecond) + (dst_negative_scale_multiply_unique_resultsecond)) * S ((dst_negative_code_multiply_unique_resultsecond) + (dst_negative_scale_multiply_unique_resultsecond)) + ((dst_negative_scale_multiply_unique_resultsecond) + (dst_negative_scale_multiply_unique_resultsecond)))) * S ((((dst_positive_code_multiply_unique_resultsecond) + (dst_positive_scale_multiply_unique_resultsecond)) * S ((dst_positive_code_multiply_unique_resultsecond) + (dst_positive_scale_multiply_unique_resultsecond)) + ((dst_positive_scale_multiply_unique_resultsecond) + (dst_positive_scale_multiply_unique_resultsecond))) + (((dst_negative_code_multiply_unique_resultsecond) + (dst_negative_scale_multiply_unique_resultsecond)) * S ((dst_negative_code_multiply_unique_resultsecond) + (dst_negative_scale_multiply_unique_resultsecond)) + ((dst_negative_scale_multiply_unique_resultsecond) + (dst_negative_scale_multiply_unique_resultsecond)))) + ((((dst_negative_code_multiply_unique_resultsecond) + (dst_negative_scale_multiply_unique_resultsecond)) * S ((dst_negative_code_multiply_unique_resultsecond) + (dst_negative_scale_multiply_unique_resultsecond)) + ((dst_negative_scale_multiply_unique_resultsecond) + (dst_negative_scale_multiply_unique_resultsecond))) + (((dst_negative_code_multiply_unique_resultsecond) + (dst_negative_scale_multiply_unique_resultsecond)) * S ((dst_negative_code_multiply_unique_resultsecond) + (dst_negative_scale_multiply_unique_resultsecond)) + ((dst_negative_scale_multiply_unique_resultsecond) + (dst_negative_scale_multiply_unique_resultsecond)))))) /\ (((((exists ff_h_pvs_multiply_unique_resultsecondpositive. ff_h_pvs_multiply_unique_resultsecondpositive + S (dst_positive_multiply_unique_resultsecond) = S ((S (dst_index_multiply_unique_result)) * dst_positive_scale_multiply_unique_resultsecond)) /\ exists ff_q_pvs_multiply_unique_resultsecondpositive. dst_positive_code_multiply_unique_resultsecond = ff_q_pvs_multiply_unique_resultsecondpositive * S ((S (dst_index_multiply_unique_result)) * dst_positive_scale_multiply_unique_resultsecond) + (dst_positive_multiply_unique_resultsecond))) /\ (((((exists ff_h_pvs_multiply_unique_resultsecondnegative. ff_h_pvs_multiply_unique_resultsecondnegative + S (dst_negative_multiply_unique_resultsecond) = S ((S (dst_index_multiply_unique_result)) * dst_negative_scale_multiply_unique_resultsecond)) /\ exists ff_q_pvs_multiply_unique_resultsecondnegative. dst_negative_code_multiply_unique_resultsecond = ff_q_pvs_multiply_unique_resultsecondnegative * S ((S (dst_index_multiply_unique_result)) * dst_negative_scale_multiply_unique_resultsecond) + (dst_negative_multiply_unique_resultsecond))) /\ (exists ge_balance_positive_multiply_unique_resultsecondvalue ge_balance_negative_multiply_unique_resultsecondvalue. (((((dst_second_multiply_unique_result) = 2 * (ge_balance_positive_multiply_unique_resultsecondvalue) /\ (ge_balance_negative_multiply_unique_resultsecondvalue) = 0) \/ exists ge_signed_half_multiply_unique_resultsecondvaluedecode. (((dst_second_multiply_unique_result) = 2 * ge_signed_half_multiply_unique_resultsecondvaluedecode + 1 /\ (ge_balance_positive_multiply_unique_resultsecondvalue) = 0) /\ (ge_balance_negative_multiply_unique_resultsecondvalue) = S ge_signed_half_multiply_unique_resultsecondvaluedecode))) /\ ((dst_positive_multiply_unique_resultsecond) + ge_balance_negative_multiply_unique_resultsecondvalue = (dst_negative_multiply_unique_resultsecond) + ge_balance_positive_multiply_unique_resultsecondvalue))))))))) -> dst_first_multiply_unique_result = dst_second_multiply_unique_result)