signed_table_multiply_extend

forall F G H K l a b c. (((exists dst_positive_code_multiply_extend_sourceleft_table dst_positive_scale_multiply_extend_sourceleft_table dst_negative_code_multiply_extend_sourceleft_table dst_negative_scale_multiply_extend_sourceleft_table. (((F) = (((((dst_positive_code_multiply_extend_sourceleft_table) + (dst_positive_scale_multiply_extend_sourceleft_table)) * S ((dst_positive_code_multiply_extend_sourceleft_table) + (dst_positive_scale_multiply_extend_sourceleft_table)) + ((dst_positive_scale_multiply_extend_sourceleft_table) + (dst_positive_scale_multiply_extend_sourceleft_table))) + (((dst_negative_code_multiply_extend_sourceleft_table) + (dst_negative_scale_multiply_extend_sourceleft_table)) * S ((dst_negative_code_multiply_extend_sourceleft_table) + (dst_negative_scale_multiply_extend_sourceleft_table)) + ((dst_negative_scale_multiply_extend_sourceleft_table) + (dst_negative_scale_multiply_extend_sourceleft_table)))) * S ((((dst_positive_code_multiply_extend_sourceleft_table) + (dst_positive_scale_multiply_extend_sourceleft_table)) * S ((dst_positive_code_multiply_extend_sourceleft_table) + (dst_positive_scale_multiply_extend_sourceleft_table)) + ((dst_positive_scale_multiply_extend_sourceleft_table) + (dst_positive_scale_multiply_extend_sourceleft_table))) + (((dst_negative_code_multiply_extend_sourceleft_table) + (dst_negative_scale_multiply_extend_sourceleft_table)) * S ((dst_negative_code_multiply_extend_sourceleft_table) + (dst_negative_scale_multiply_extend_sourceleft_table)) + ((dst_negative_scale_multiply_extend_sourceleft_table) + (dst_negative_scale_multiply_extend_sourceleft_table)))) + ((((dst_negative_code_multiply_extend_sourceleft_table) + (dst_negative_scale_multiply_extend_sourceleft_table)) * S ((dst_negative_code_multiply_extend_sourceleft_table) + (dst_negative_scale_multiply_extend_sourceleft_table)) + ((dst_negative_scale_multiply_extend_sourceleft_table) + (dst_negative_scale_multiply_extend_sourceleft_table))) + (((dst_negative_code_multiply_extend_sourceleft_table) + (dst_negative_scale_multiply_extend_sourceleft_table)) * S ((dst_negative_code_multiply_extend_sourceleft_table) + (dst_negative_scale_multiply_extend_sourceleft_table)) + ((dst_negative_scale_multiply_extend_sourceleft_table) + (dst_negative_scale_multiply_extend_sourceleft_table)))))) /\ (forall dst_index_multiply_extend_sourceleft_table. (exists pvs_le_gap_multiply_extend_sourceleft_tabledomain. pvs_le_gap_multiply_extend_sourceleft_tabledomain + (dst_index_multiply_extend_sourceleft_table) = (l)) -> exists dst_positive_multiply_extend_sourceleft_table dst_negative_multiply_extend_sourceleft_table dst_value_multiply_extend_sourceleft_table. ((((exists ff_h_pvs_multiply_extend_sourceleft_tableentrypositive. ff_h_pvs_multiply_extend_sourceleft_tableentrypositive + S (dst_positive_multiply_extend_sourceleft_table) = S ((S (dst_index_multiply_extend_sourceleft_table)) * dst_positive_scale_multiply_extend_sourceleft_table)) /\ exists ff_q_pvs_multiply_extend_sourceleft_tableentrypositive. dst_positive_code_multiply_extend_sourceleft_table = ff_q_pvs_multiply_extend_sourceleft_tableentrypositive * S ((S (dst_index_multiply_extend_sourceleft_table)) * dst_positive_scale_multiply_extend_sourceleft_table) + (dst_positive_multiply_extend_sourceleft_table))) /\ (((((exists ff_h_pvs_multiply_extend_sourceleft_tableentrynegative. ff_h_pvs_multiply_extend_sourceleft_tableentrynegative + S (dst_negative_multiply_extend_sourceleft_table) = S ((S (dst_index_multiply_extend_sourceleft_table)) * dst_negative_scale_multiply_extend_sourceleft_table)) /\ exists ff_q_pvs_multiply_extend_sourceleft_tableentrynegative. dst_negative_code_multiply_extend_sourceleft_table = ff_q_pvs_multiply_extend_sourceleft_tableentrynegative * S ((S (dst_index_multiply_extend_sourceleft_table)) * dst_negative_scale_multiply_extend_sourceleft_table) + (dst_negative_multiply_extend_sourceleft_table))) /\ (exists ge_balance_positive_multiply_extend_sourceleft_tableentryvalue ge_balance_negative_multiply_extend_sourceleft_tableentryvalue. (((((dst_value_multiply_extend_sourceleft_table) = 2 * (ge_balance_positive_multiply_extend_sourceleft_tableentryvalue) /\ (ge_balance_negative_multiply_extend_sourceleft_tableentryvalue) = 0) \/ exists ge_signed_half_multiply_extend_sourceleft_tableentryvaluedecode. (((dst_value_multiply_extend_sourceleft_table) = 2 * ge_signed_half_multiply_extend_sourceleft_tableentryvaluedecode + 1 /\ (ge_balance_positive_multiply_extend_sourceleft_tableentryvalue) = 0) /\ (ge_balance_negative_multiply_extend_sourceleft_tableentryvalue) = S ge_signed_half_multiply_extend_sourceleft_tableentryvaluedecode))) /\ ((dst_positive_multiply_extend_sourceleft_table) + ge_balance_negative_multiply_extend_sourceleft_tableentryvalue = (dst_negative_multiply_extend_sourceleft_table) + ge_balance_positive_multiply_extend_sourceleft_tableentryvalue))))))))) /\ (((exists dst_positive_code_multiply_extend_sourceright_table dst_positive_scale_multiply_extend_sourceright_table dst_negative_code_multiply_extend_sourceright_table dst_negative_scale_multiply_extend_sourceright_table. (((G) = (((((dst_positive_code_multiply_extend_sourceright_table) + (dst_positive_scale_multiply_extend_sourceright_table)) * S ((dst_positive_code_multiply_extend_sourceright_table) + (dst_positive_scale_multiply_extend_sourceright_table)) + ((dst_positive_scale_multiply_extend_sourceright_table) + (dst_positive_scale_multiply_extend_sourceright_table))) + (((dst_negative_code_multiply_extend_sourceright_table) + (dst_negative_scale_multiply_extend_sourceright_table)) * S ((dst_negative_code_multiply_extend_sourceright_table) + (dst_negative_scale_multiply_extend_sourceright_table)) + ((dst_negative_scale_multiply_extend_sourceright_table) + (dst_negative_scale_multiply_extend_sourceright_table)))) * S ((((dst_positive_code_multiply_extend_sourceright_table) + (dst_positive_scale_multiply_extend_sourceright_table)) * S ((dst_positive_code_multiply_extend_sourceright_table) + (dst_positive_scale_multiply_extend_sourceright_table)) + ((dst_positive_scale_multiply_extend_sourceright_table) + (dst_positive_scale_multiply_extend_sourceright_table))) + (((dst_negative_code_multiply_extend_sourceright_table) + (dst_negative_scale_multiply_extend_sourceright_table)) * S ((dst_negative_code_multiply_extend_sourceright_table) + (dst_negative_scale_multiply_extend_sourceright_table)) + ((dst_negative_scale_multiply_extend_sourceright_table) + (dst_negative_scale_multiply_extend_sourceright_table)))) + ((((dst_negative_code_multiply_extend_sourceright_table) + (dst_negative_scale_multiply_extend_sourceright_table)) * S ((dst_negative_code_multiply_extend_sourceright_table) + (dst_negative_scale_multiply_extend_sourceright_table)) + ((dst_negative_scale_multiply_extend_sourceright_table) + (dst_negative_scale_multiply_extend_sourceright_table))) + (((dst_negative_code_multiply_extend_sourceright_table) + (dst_negative_scale_multiply_extend_sourceright_table)) * S ((dst_negative_code_multiply_extend_sourceright_table) + (dst_negative_scale_multiply_extend_sourceright_table)) + ((dst_negative_scale_multiply_extend_sourceright_table) + (dst_negative_scale_multiply_extend_sourceright_table)))))) /\ (forall dst_index_multiply_extend_sourceright_table. (exists pvs_le_gap_multiply_extend_sourceright_tabledomain. pvs_le_gap_multiply_extend_sourceright_tabledomain + (dst_index_multiply_extend_sourceright_table) = (l)) -> exists dst_positive_multiply_extend_sourceright_table dst_negative_multiply_extend_sourceright_table dst_value_multiply_extend_sourceright_table. ((((exists ff_h_pvs_multiply_extend_sourceright_tableentrypositive. ff_h_pvs_multiply_extend_sourceright_tableentrypositive + S (dst_positive_multiply_extend_sourceright_table) = S ((S (dst_index_multiply_extend_sourceright_table)) * dst_positive_scale_multiply_extend_sourceright_table)) /\ exists ff_q_pvs_multiply_extend_sourceright_tableentrypositive. dst_positive_code_multiply_extend_sourceright_table = ff_q_pvs_multiply_extend_sourceright_tableentrypositive * S ((S (dst_index_multiply_extend_sourceright_table)) * dst_positive_scale_multiply_extend_sourceright_table) + (dst_positive_multiply_extend_sourceright_table))) /\ (((((exists ff_h_pvs_multiply_extend_sourceright_tableentrynegative. ff_h_pvs_multiply_extend_sourceright_tableentrynegative + S (dst_negative_multiply_extend_sourceright_table) = S ((S (dst_index_multiply_extend_sourceright_table)) * dst_negative_scale_multiply_extend_sourceright_table)) /\ exists ff_q_pvs_multiply_extend_sourceright_tableentrynegative. dst_negative_code_multiply_extend_sourceright_table = ff_q_pvs_multiply_extend_sourceright_tableentrynegative * S ((S (dst_index_multiply_extend_sourceright_table)) * dst_negative_scale_multiply_extend_sourceright_table) + (dst_negative_multiply_extend_sourceright_table))) /\ (exists ge_balance_positive_multiply_extend_sourceright_tableentryvalue ge_balance_negative_multiply_extend_sourceright_tableentryvalue. (((((dst_value_multiply_extend_sourceright_table) = 2 * (ge_balance_positive_multiply_extend_sourceright_tableentryvalue) /\ (ge_balance_negative_multiply_extend_sourceright_tableentryvalue) = 0) \/ exists ge_signed_half_multiply_extend_sourceright_tableentryvaluedecode. (((dst_value_multiply_extend_sourceright_table) = 2 * ge_signed_half_multiply_extend_sourceright_tableentryvaluedecode + 1 /\ (ge_balance_positive_multiply_extend_sourceright_tableentryvalue) = 0) /\ (ge_balance_negative_multiply_extend_sourceright_tableentryvalue) = S ge_signed_half_multiply_extend_sourceright_tableentryvaluedecode))) /\ ((dst_positive_multiply_extend_sourceright_table) + ge_balance_negative_multiply_extend_sourceright_tableentryvalue = (dst_negative_multiply_extend_sourceright_table) + ge_balance_positive_multiply_extend_sourceright_tableentryvalue))))))))) /\ (((exists dst_positive_code_multiply_extend_sourceoutput_table dst_positive_scale_multiply_extend_sourceoutput_table dst_negative_code_multiply_extend_sourceoutput_table dst_negative_scale_multiply_extend_sourceoutput_table. (((H) = (((((dst_positive_code_multiply_extend_sourceoutput_table) + (dst_positive_scale_multiply_extend_sourceoutput_table)) * S ((dst_positive_code_multiply_extend_sourceoutput_table) + (dst_positive_scale_multiply_extend_sourceoutput_table)) + ((dst_positive_scale_multiply_extend_sourceoutput_table) + (dst_positive_scale_multiply_extend_sourceoutput_table))) + (((dst_negative_code_multiply_extend_sourceoutput_table) + (dst_negative_scale_multiply_extend_sourceoutput_table)) * S ((dst_negative_code_multiply_extend_sourceoutput_table) + (dst_negative_scale_multiply_extend_sourceoutput_table)) + ((dst_negative_scale_multiply_extend_sourceoutput_table) + (dst_negative_scale_multiply_extend_sourceoutput_table)))) * S ((((dst_positive_code_multiply_extend_sourceoutput_table) + (dst_positive_scale_multiply_extend_sourceoutput_table)) * S ((dst_positive_code_multiply_extend_sourceoutput_table) + (dst_positive_scale_multiply_extend_sourceoutput_table)) + ((dst_positive_scale_multiply_extend_sourceoutput_table) + (dst_positive_scale_multiply_extend_sourceoutput_table))) + (((dst_negative_code_multiply_extend_sourceoutput_table) + (dst_negative_scale_multiply_extend_sourceoutput_table)) * S ((dst_negative_code_multiply_extend_sourceoutput_table) + (dst_negative_scale_multiply_extend_sourceoutput_table)) + ((dst_negative_scale_multiply_extend_sourceoutput_table) + (dst_negative_scale_multiply_extend_sourceoutput_table)))) + ((((dst_negative_code_multiply_extend_sourceoutput_table) + (dst_negative_scale_multiply_extend_sourceoutput_table)) * S ((dst_negative_code_multiply_extend_sourceoutput_table) + (dst_negative_scale_multiply_extend_sourceoutput_table)) + ((dst_negative_scale_multiply_extend_sourceoutput_table) + (dst_negative_scale_multiply_extend_sourceoutput_table))) + (((dst_negative_code_multiply_extend_sourceoutput_table) + (dst_negative_scale_multiply_extend_sourceoutput_table)) * S ((dst_negative_code_multiply_extend_sourceoutput_table) + (dst_negative_scale_multiply_extend_sourceoutput_table)) + ((dst_negative_scale_multiply_extend_sourceoutput_table) + (dst_negative_scale_multiply_extend_sourceoutput_table)))))) /\ (forall dst_index_multiply_extend_sourceoutput_table. (exists pvs_le_gap_multiply_extend_sourceoutput_tabledomain. pvs_le_gap_multiply_extend_sourceoutput_tabledomain + (dst_index_multiply_extend_sourceoutput_table) = (l)) -> exists dst_positive_multiply_extend_sourceoutput_table dst_negative_multiply_extend_sourceoutput_table dst_value_multiply_extend_sourceoutput_table. ((((exists ff_h_pvs_multiply_extend_sourceoutput_tableentrypositive. ff_h_pvs_multiply_extend_sourceoutput_tableentrypositive + S (dst_positive_multiply_extend_sourceoutput_table) = S ((S (dst_index_multiply_extend_sourceoutput_table)) * dst_positive_scale_multiply_extend_sourceoutput_table)) /\ exists ff_q_pvs_multiply_extend_sourceoutput_tableentrypositive. dst_positive_code_multiply_extend_sourceoutput_table = ff_q_pvs_multiply_extend_sourceoutput_tableentrypositive * S ((S (dst_index_multiply_extend_sourceoutput_table)) * dst_positive_scale_multiply_extend_sourceoutput_table) + (dst_positive_multiply_extend_sourceoutput_table))) /\ (((((exists ff_h_pvs_multiply_extend_sourceoutput_tableentrynegative. ff_h_pvs_multiply_extend_sourceoutput_tableentrynegative + S (dst_negative_multiply_extend_sourceoutput_table) = S ((S (dst_index_multiply_extend_sourceoutput_table)) * dst_negative_scale_multiply_extend_sourceoutput_table)) /\ exists ff_q_pvs_multiply_extend_sourceoutput_tableentrynegative. dst_negative_code_multiply_extend_sourceoutput_table = ff_q_pvs_multiply_extend_sourceoutput_tableentrynegative * S ((S (dst_index_multiply_extend_sourceoutput_table)) * dst_negative_scale_multiply_extend_sourceoutput_table) + (dst_negative_multiply_extend_sourceoutput_table))) /\ (exists ge_balance_positive_multiply_extend_sourceoutput_tableentryvalue ge_balance_negative_multiply_extend_sourceoutput_tableentryvalue. (((((dst_value_multiply_extend_sourceoutput_table) = 2 * (ge_balance_positive_multiply_extend_sourceoutput_tableentryvalue) /\ (ge_balance_negative_multiply_extend_sourceoutput_tableentryvalue) = 0) \/ exists ge_signed_half_multiply_extend_sourceoutput_tableentryvaluedecode. (((dst_value_multiply_extend_sourceoutput_table) = 2 * ge_signed_half_multiply_extend_sourceoutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_multiply_extend_sourceoutput_tableentryvalue) = 0) /\ (ge_balance_negative_multiply_extend_sourceoutput_tableentryvalue) = S ge_signed_half_multiply_extend_sourceoutput_tableentryvaluedecode))) /\ ((dst_positive_multiply_extend_sourceoutput_table) + ge_balance_negative_multiply_extend_sourceoutput_tableentryvalue = (dst_negative_multiply_extend_sourceoutput_table) + ge_balance_positive_multiply_extend_sourceoutput_tableentryvalue))))))))) /\ (forall sto_index_multiply_extend_sourceentries. (exists pvs_gap_multiply_extend_sourceentriesbound. pvs_gap_multiply_extend_sourceentriesbound + S (sto_index_multiply_extend_sourceentries) = (l)) -> exists sto_left_multiply_extend_sourceentries sto_right_multiply_extend_sourceentries sto_output_multiply_extend_sourceentries. ((exists dst_positive_code_multiply_extend_sourceentriesentryleft dst_positive_scale_multiply_extend_sourceentriesentryleft dst_negative_code_multiply_extend_sourceentriesentryleft dst_negative_scale_multiply_extend_sourceentriesentryleft dst_positive_multiply_extend_sourceentriesentryleft dst_negative_multiply_extend_sourceentriesentryleft. (((F) = (((((dst_positive_code_multiply_extend_sourceentriesentryleft) + (dst_positive_scale_multiply_extend_sourceentriesentryleft)) * S ((dst_positive_code_multiply_extend_sourceentriesentryleft) + (dst_positive_scale_multiply_extend_sourceentriesentryleft)) + ((dst_positive_scale_multiply_extend_sourceentriesentryleft) + (dst_positive_scale_multiply_extend_sourceentriesentryleft))) + (((dst_negative_code_multiply_extend_sourceentriesentryleft) + (dst_negative_scale_multiply_extend_sourceentriesentryleft)) * S ((dst_negative_code_multiply_extend_sourceentriesentryleft) + (dst_negative_scale_multiply_extend_sourceentriesentryleft)) + ((dst_negative_scale_multiply_extend_sourceentriesentryleft) + (dst_negative_scale_multiply_extend_sourceentriesentryleft)))) * S ((((dst_positive_code_multiply_extend_sourceentriesentryleft) + (dst_positive_scale_multiply_extend_sourceentriesentryleft)) * S ((dst_positive_code_multiply_extend_sourceentriesentryleft) + (dst_positive_scale_multiply_extend_sourceentriesentryleft)) + ((dst_positive_scale_multiply_extend_sourceentriesentryleft) + (dst_positive_scale_multiply_extend_sourceentriesentryleft))) + (((dst_negative_code_multiply_extend_sourceentriesentryleft) + (dst_negative_scale_multiply_extend_sourceentriesentryleft)) * S ((dst_negative_code_multiply_extend_sourceentriesentryleft) + (dst_negative_scale_multiply_extend_sourceentriesentryleft)) + ((dst_negative_scale_multiply_extend_sourceentriesentryleft) + (dst_negative_scale_multiply_extend_sourceentriesentryleft)))) + ((((dst_negative_code_multiply_extend_sourceentriesentryleft) + (dst_negative_scale_multiply_extend_sourceentriesentryleft)) * S ((dst_negative_code_multiply_extend_sourceentriesentryleft) + (dst_negative_scale_multiply_extend_sourceentriesentryleft)) + ((dst_negative_scale_multiply_extend_sourceentriesentryleft) + (dst_negative_scale_multiply_extend_sourceentriesentryleft))) + (((dst_negative_code_multiply_extend_sourceentriesentryleft) + (dst_negative_scale_multiply_extend_sourceentriesentryleft)) * S ((dst_negative_code_multiply_extend_sourceentriesentryleft) + (dst_negative_scale_multiply_extend_sourceentriesentryleft)) + ((dst_negative_scale_multiply_extend_sourceentriesentryleft) + (dst_negative_scale_multiply_extend_sourceentriesentryleft)))))) /\ (((((exists ff_h_pvs_multiply_extend_sourceentriesentryleftpositive. ff_h_pvs_multiply_extend_sourceentriesentryleftpositive + S (dst_positive_multiply_extend_sourceentriesentryleft) = S ((S (sto_index_multiply_extend_sourceentries)) * dst_positive_scale_multiply_extend_sourceentriesentryleft)) /\ exists ff_q_pvs_multiply_extend_sourceentriesentryleftpositive. dst_positive_code_multiply_extend_sourceentriesentryleft = ff_q_pvs_multiply_extend_sourceentriesentryleftpositive * S ((S (sto_index_multiply_extend_sourceentries)) * dst_positive_scale_multiply_extend_sourceentriesentryleft) + (dst_positive_multiply_extend_sourceentriesentryleft))) /\ (((((exists ff_h_pvs_multiply_extend_sourceentriesentryleftnegative. ff_h_pvs_multiply_extend_sourceentriesentryleftnegative + S (dst_negative_multiply_extend_sourceentriesentryleft) = S ((S (sto_index_multiply_extend_sourceentries)) * dst_negative_scale_multiply_extend_sourceentriesentryleft)) /\ exists ff_q_pvs_multiply_extend_sourceentriesentryleftnegative. dst_negative_code_multiply_extend_sourceentriesentryleft = ff_q_pvs_multiply_extend_sourceentriesentryleftnegative * S ((S (sto_index_multiply_extend_sourceentries)) * dst_negative_scale_multiply_extend_sourceentriesentryleft) + (dst_negative_multiply_extend_sourceentriesentryleft))) /\ (exists ge_balance_positive_multiply_extend_sourceentriesentryleftvalue ge_balance_negative_multiply_extend_sourceentriesentryleftvalue. (((((sto_left_multiply_extend_sourceentries) = 2 * (ge_balance_positive_multiply_extend_sourceentriesentryleftvalue) /\ (ge_balance_negative_multiply_extend_sourceentriesentryleftvalue) = 0) \/ exists ge_signed_half_multiply_extend_sourceentriesentryleftvaluedecode. (((sto_left_multiply_extend_sourceentries) = 2 * ge_signed_half_multiply_extend_sourceentriesentryleftvaluedecode + 1 /\ (ge_balance_positive_multiply_extend_sourceentriesentryleftvalue) = 0) /\ (ge_balance_negative_multiply_extend_sourceentriesentryleftvalue) = S ge_signed_half_multiply_extend_sourceentriesentryleftvaluedecode))) /\ ((dst_positive_multiply_extend_sourceentriesentryleft) + ge_balance_negative_multiply_extend_sourceentriesentryleftvalue = (dst_negative_multiply_extend_sourceentriesentryleft) + ge_balance_positive_multiply_extend_sourceentriesentryleftvalue))))))))) /\ (((exists dst_positive_code_multiply_extend_sourceentriesentryright dst_positive_scale_multiply_extend_sourceentriesentryright dst_negative_code_multiply_extend_sourceentriesentryright dst_negative_scale_multiply_extend_sourceentriesentryright dst_positive_multiply_extend_sourceentriesentryright dst_negative_multiply_extend_sourceentriesentryright. (((G) = (((((dst_positive_code_multiply_extend_sourceentriesentryright) + (dst_positive_scale_multiply_extend_sourceentriesentryright)) * S ((dst_positive_code_multiply_extend_sourceentriesentryright) + (dst_positive_scale_multiply_extend_sourceentriesentryright)) + ((dst_positive_scale_multiply_extend_sourceentriesentryright) + (dst_positive_scale_multiply_extend_sourceentriesentryright))) + (((dst_negative_code_multiply_extend_sourceentriesentryright) + (dst_negative_scale_multiply_extend_sourceentriesentryright)) * S ((dst_negative_code_multiply_extend_sourceentriesentryright) + (dst_negative_scale_multiply_extend_sourceentriesentryright)) + ((dst_negative_scale_multiply_extend_sourceentriesentryright) + (dst_negative_scale_multiply_extend_sourceentriesentryright)))) * S ((((dst_positive_code_multiply_extend_sourceentriesentryright) + (dst_positive_scale_multiply_extend_sourceentriesentryright)) * S ((dst_positive_code_multiply_extend_sourceentriesentryright) + (dst_positive_scale_multiply_extend_sourceentriesentryright)) + ((dst_positive_scale_multiply_extend_sourceentriesentryright) + (dst_positive_scale_multiply_extend_sourceentriesentryright))) + (((dst_negative_code_multiply_extend_sourceentriesentryright) + (dst_negative_scale_multiply_extend_sourceentriesentryright)) * S ((dst_negative_code_multiply_extend_sourceentriesentryright) + (dst_negative_scale_multiply_extend_sourceentriesentryright)) + ((dst_negative_scale_multiply_extend_sourceentriesentryright) + (dst_negative_scale_multiply_extend_sourceentriesentryright)))) + ((((dst_negative_code_multiply_extend_sourceentriesentryright) + (dst_negative_scale_multiply_extend_sourceentriesentryright)) * S ((dst_negative_code_multiply_extend_sourceentriesentryright) + (dst_negative_scale_multiply_extend_sourceentriesentryright)) + ((dst_negative_scale_multiply_extend_sourceentriesentryright) + (dst_negative_scale_multiply_extend_sourceentriesentryright))) + (((dst_negative_code_multiply_extend_sourceentriesentryright) + (dst_negative_scale_multiply_extend_sourceentriesentryright)) * S ((dst_negative_code_multiply_extend_sourceentriesentryright) + (dst_negative_scale_multiply_extend_sourceentriesentryright)) + ((dst_negative_scale_multiply_extend_sourceentriesentryright) + (dst_negative_scale_multiply_extend_sourceentriesentryright)))))) /\ (((((exists ff_h_pvs_multiply_extend_sourceentriesentryrightpositive. ff_h_pvs_multiply_extend_sourceentriesentryrightpositive + S (dst_positive_multiply_extend_sourceentriesentryright) = S ((S (sto_index_multiply_extend_sourceentries)) * dst_positive_scale_multiply_extend_sourceentriesentryright)) /\ exists ff_q_pvs_multiply_extend_sourceentriesentryrightpositive. dst_positive_code_multiply_extend_sourceentriesentryright = ff_q_pvs_multiply_extend_sourceentriesentryrightpositive * S ((S (sto_index_multiply_extend_sourceentries)) * dst_positive_scale_multiply_extend_sourceentriesentryright) + (dst_positive_multiply_extend_sourceentriesentryright))) /\ (((((exists ff_h_pvs_multiply_extend_sourceentriesentryrightnegative. ff_h_pvs_multiply_extend_sourceentriesentryrightnegative + S (dst_negative_multiply_extend_sourceentriesentryright) = S ((S (sto_index_multiply_extend_sourceentries)) * dst_negative_scale_multiply_extend_sourceentriesentryright)) /\ exists ff_q_pvs_multiply_extend_sourceentriesentryrightnegative. dst_negative_code_multiply_extend_sourceentriesentryright = ff_q_pvs_multiply_extend_sourceentriesentryrightnegative * S ((S (sto_index_multiply_extend_sourceentries)) * dst_negative_scale_multiply_extend_sourceentriesentryright) + (dst_negative_multiply_extend_sourceentriesentryright))) /\ (exists ge_balance_positive_multiply_extend_sourceentriesentryrightvalue ge_balance_negative_multiply_extend_sourceentriesentryrightvalue. (((((sto_right_multiply_extend_sourceentries) = 2 * (ge_balance_positive_multiply_extend_sourceentriesentryrightvalue) /\ (ge_balance_negative_multiply_extend_sourceentriesentryrightvalue) = 0) \/ exists ge_signed_half_multiply_extend_sourceentriesentryrightvaluedecode. (((sto_right_multiply_extend_sourceentries) = 2 * ge_signed_half_multiply_extend_sourceentriesentryrightvaluedecode + 1 /\ (ge_balance_positive_multiply_extend_sourceentriesentryrightvalue) = 0) /\ (ge_balance_negative_multiply_extend_sourceentriesentryrightvalue) = S ge_signed_half_multiply_extend_sourceentriesentryrightvaluedecode))) /\ ((dst_positive_multiply_extend_sourceentriesentryright) + ge_balance_negative_multiply_extend_sourceentriesentryrightvalue = (dst_negative_multiply_extend_sourceentriesentryright) + ge_balance_positive_multiply_extend_sourceentriesentryrightvalue))))))))) /\ (((exists dst_positive_code_multiply_extend_sourceentriesentryoutput dst_positive_scale_multiply_extend_sourceentriesentryoutput dst_negative_code_multiply_extend_sourceentriesentryoutput dst_negative_scale_multiply_extend_sourceentriesentryoutput dst_positive_multiply_extend_sourceentriesentryoutput dst_negative_multiply_extend_sourceentriesentryoutput. (((H) = (((((dst_positive_code_multiply_extend_sourceentriesentryoutput) + (dst_positive_scale_multiply_extend_sourceentriesentryoutput)) * S ((dst_positive_code_multiply_extend_sourceentriesentryoutput) + (dst_positive_scale_multiply_extend_sourceentriesentryoutput)) + ((dst_positive_scale_multiply_extend_sourceentriesentryoutput) + (dst_positive_scale_multiply_extend_sourceentriesentryoutput))) + (((dst_negative_code_multiply_extend_sourceentriesentryoutput) + (dst_negative_scale_multiply_extend_sourceentriesentryoutput)) * S ((dst_negative_code_multiply_extend_sourceentriesentryoutput) + (dst_negative_scale_multiply_extend_sourceentriesentryoutput)) + ((dst_negative_scale_multiply_extend_sourceentriesentryoutput) + (dst_negative_scale_multiply_extend_sourceentriesentryoutput)))) * S ((((dst_positive_code_multiply_extend_sourceentriesentryoutput) + (dst_positive_scale_multiply_extend_sourceentriesentryoutput)) * S ((dst_positive_code_multiply_extend_sourceentriesentryoutput) + (dst_positive_scale_multiply_extend_sourceentriesentryoutput)) + ((dst_positive_scale_multiply_extend_sourceentriesentryoutput) + (dst_positive_scale_multiply_extend_sourceentriesentryoutput))) + (((dst_negative_code_multiply_extend_sourceentriesentryoutput) + (dst_negative_scale_multiply_extend_sourceentriesentryoutput)) * S ((dst_negative_code_multiply_extend_sourceentriesentryoutput) + (dst_negative_scale_multiply_extend_sourceentriesentryoutput)) + ((dst_negative_scale_multiply_extend_sourceentriesentryoutput) + (dst_negative_scale_multiply_extend_sourceentriesentryoutput)))) + ((((dst_negative_code_multiply_extend_sourceentriesentryoutput) + (dst_negative_scale_multiply_extend_sourceentriesentryoutput)) * S ((dst_negative_code_multiply_extend_sourceentriesentryoutput) + (dst_negative_scale_multiply_extend_sourceentriesentryoutput)) + ((dst_negative_scale_multiply_extend_sourceentriesentryoutput) + (dst_negative_scale_multiply_extend_sourceentriesentryoutput))) + (((dst_negative_code_multiply_extend_sourceentriesentryoutput) + (dst_negative_scale_multiply_extend_sourceentriesentryoutput)) * S ((dst_negative_code_multiply_extend_sourceentriesentryoutput) + (dst_negative_scale_multiply_extend_sourceentriesentryoutput)) + ((dst_negative_scale_multiply_extend_sourceentriesentryoutput) + (dst_negative_scale_multiply_extend_sourceentriesentryoutput)))))) /\ (((((exists ff_h_pvs_multiply_extend_sourceentriesentryoutputpositive. ff_h_pvs_multiply_extend_sourceentriesentryoutputpositive + S (dst_positive_multiply_extend_sourceentriesentryoutput) = S ((S (sto_index_multiply_extend_sourceentries)) * dst_positive_scale_multiply_extend_sourceentriesentryoutput)) /\ exists ff_q_pvs_multiply_extend_sourceentriesentryoutputpositive. dst_positive_code_multiply_extend_sourceentriesentryoutput = ff_q_pvs_multiply_extend_sourceentriesentryoutputpositive * S ((S (sto_index_multiply_extend_sourceentries)) * dst_positive_scale_multiply_extend_sourceentriesentryoutput) + (dst_positive_multiply_extend_sourceentriesentryoutput))) /\ (((((exists ff_h_pvs_multiply_extend_sourceentriesentryoutputnegative. ff_h_pvs_multiply_extend_sourceentriesentryoutputnegative + S (dst_negative_multiply_extend_sourceentriesentryoutput) = S ((S (sto_index_multiply_extend_sourceentries)) * dst_negative_scale_multiply_extend_sourceentriesentryoutput)) /\ exists ff_q_pvs_multiply_extend_sourceentriesentryoutputnegative. dst_negative_code_multiply_extend_sourceentriesentryoutput = ff_q_pvs_multiply_extend_sourceentriesentryoutputnegative * S ((S (sto_index_multiply_extend_sourceentries)) * dst_negative_scale_multiply_extend_sourceentriesentryoutput) + (dst_negative_multiply_extend_sourceentriesentryoutput))) /\ (exists ge_balance_positive_multiply_extend_sourceentriesentryoutputvalue ge_balance_negative_multiply_extend_sourceentriesentryoutputvalue. (((((sto_output_multiply_extend_sourceentries) = 2 * (ge_balance_positive_multiply_extend_sourceentriesentryoutputvalue) /\ (ge_balance_negative_multiply_extend_sourceentriesentryoutputvalue) = 0) \/ exists ge_signed_half_multiply_extend_sourceentriesentryoutputvaluedecode. (((sto_output_multiply_extend_sourceentries) = 2 * ge_signed_half_multiply_extend_sourceentriesentryoutputvaluedecode + 1 /\ (ge_balance_positive_multiply_extend_sourceentriesentryoutputvalue) = 0) /\ (ge_balance_negative_multiply_extend_sourceentriesentryoutputvalue) = S ge_signed_half_multiply_extend_sourceentriesentryoutputvaluedecode))) /\ ((dst_positive_multiply_extend_sourceentriesentryoutput) + ge_balance_negative_multiply_extend_sourceentriesentryoutputvalue = (dst_negative_multiply_extend_sourceentriesentryoutput) + ge_balance_positive_multiply_extend_sourceentriesentryoutputvalue))))))))) /\ (exists sto_ap_multiply_extend_sourceentriesentryoperation sto_an_multiply_extend_sourceentriesentryoperation sto_bp_multiply_extend_sourceentriesentryoperation sto_bn_multiply_extend_sourceentriesentryoperation sto_cp_multiply_extend_sourceentriesentryoperation sto_cn_multiply_extend_sourceentriesentryoperation. (((((sto_left_multiply_extend_sourceentries) = 2 * (sto_ap_multiply_extend_sourceentriesentryoperation) /\ (sto_an_multiply_extend_sourceentriesentryoperation) = 0) \/ exists ge_signed_half_multiply_extend_sourceentriesentryoperationleft. (((sto_left_multiply_extend_sourceentries) = 2 * ge_signed_half_multiply_extend_sourceentriesentryoperationleft + 1 /\ (sto_ap_multiply_extend_sourceentriesentryoperation) = 0) /\ (sto_an_multiply_extend_sourceentriesentryoperation) = S ge_signed_half_multiply_extend_sourceentriesentryoperationleft))) /\ ((((((sto_right_multiply_extend_sourceentries) = 2 * (sto_bp_multiply_extend_sourceentriesentryoperation) /\ (sto_bn_multiply_extend_sourceentriesentryoperation) = 0) \/ exists ge_signed_half_multiply_extend_sourceentriesentryoperationright. (((sto_right_multiply_extend_sourceentries) = 2 * ge_signed_half_multiply_extend_sourceentriesentryoperationright + 1 /\ (sto_bp_multiply_extend_sourceentriesentryoperation) = 0) /\ (sto_bn_multiply_extend_sourceentriesentryoperation) = S ge_signed_half_multiply_extend_sourceentriesentryoperationright))) /\ ((((((sto_output_multiply_extend_sourceentries) = 2 * (sto_cp_multiply_extend_sourceentriesentryoperation) /\ (sto_cn_multiply_extend_sourceentriesentryoperation) = 0) \/ exists ge_signed_half_multiply_extend_sourceentriesentryoperationoutput. (((sto_output_multiply_extend_sourceentries) = 2 * ge_signed_half_multiply_extend_sourceentriesentryoperationoutput + 1 /\ (sto_cp_multiply_extend_sourceentriesentryoperation) = 0) /\ (sto_cn_multiply_extend_sourceentriesentryoperation) = S ge_signed_half_multiply_extend_sourceentriesentryoperationoutput))) /\ ((sto_ap_multiply_extend_sourceentriesentryoperation * sto_bp_multiply_extend_sourceentriesentryoperation + sto_an_multiply_extend_sourceentriesentryoperation * sto_bn_multiply_extend_sourceentriesentryoperation) + sto_cn_multiply_extend_sourceentriesentryoperation = (sto_ap_multiply_extend_sourceentriesentryoperation * sto_bn_multiply_extend_sourceentriesentryoperation + sto_an_multiply_extend_sourceentriesentryoperation * sto_bp_multiply_extend_sourceentriesentryoperation) + sto_cp_multiply_extend_sourceentriesentryoperation))))))))))))))))))) -> (exists dst_positive_code_multiply_extend_table dst_positive_scale_multiply_extend_table dst_negative_code_multiply_extend_table dst_negative_scale_multiply_extend_table. (((K) = (((((dst_positive_code_multiply_extend_table) + (dst_positive_scale_multiply_extend_table)) * S ((dst_positive_code_multiply_extend_table) + (dst_positive_scale_multiply_extend_table)) + ((dst_positive_scale_multiply_extend_table) + (dst_positive_scale_multiply_extend_table))) + (((dst_negative_code_multiply_extend_table) + (dst_negative_scale_multiply_extend_table)) * S ((dst_negative_code_multiply_extend_table) + (dst_negative_scale_multiply_extend_table)) + ((dst_negative_scale_multiply_extend_table) + (dst_negative_scale_multiply_extend_table)))) * S ((((dst_positive_code_multiply_extend_table) + (dst_positive_scale_multiply_extend_table)) * S ((dst_positive_code_multiply_extend_table) + (dst_positive_scale_multiply_extend_table)) + ((dst_positive_scale_multiply_extend_table) + (dst_positive_scale_multiply_extend_table))) + (((dst_negative_code_multiply_extend_table) + (dst_negative_scale_multiply_extend_table)) * S ((dst_negative_code_multiply_extend_table) + (dst_negative_scale_multiply_extend_table)) + ((dst_negative_scale_multiply_extend_table) + (dst_negative_scale_multiply_extend_table)))) + ((((dst_negative_code_multiply_extend_table) + (dst_negative_scale_multiply_extend_table)) * S ((dst_negative_code_multiply_extend_table) + (dst_negative_scale_multiply_extend_table)) + ((dst_negative_scale_multiply_extend_table) + (dst_negative_scale_multiply_extend_table))) + (((dst_negative_code_multiply_extend_table) + (dst_negative_scale_multiply_extend_table)) * S ((dst_negative_code_multiply_extend_table) + (dst_negative_scale_multiply_extend_table)) + ((dst_negative_scale_multiply_extend_table) + (dst_negative_scale_multiply_extend_table)))))) /\ (forall dst_index_multiply_extend_table. (exists pvs_le_gap_multiply_extend_tabledomain. pvs_le_gap_multiply_extend_tabledomain + (dst_index_multiply_extend_table) = (l)) -> exists dst_positive_multiply_extend_table dst_negative_multiply_extend_table dst_value_multiply_extend_table. ((((exists ff_h_pvs_multiply_extend_tableentrypositive. ff_h_pvs_multiply_extend_tableentrypositive + S (dst_positive_multiply_extend_table) = S ((S (dst_index_multiply_extend_table)) * dst_positive_scale_multiply_extend_table)) /\ exists ff_q_pvs_multiply_extend_tableentrypositive. dst_positive_code_multiply_extend_table = ff_q_pvs_multiply_extend_tableentrypositive * S ((S (dst_index_multiply_extend_table)) * dst_positive_scale_multiply_extend_table) + (dst_positive_multiply_extend_table))) /\ (((((exists ff_h_pvs_multiply_extend_tableentrynegative. ff_h_pvs_multiply_extend_tableentrynegative + S (dst_negative_multiply_extend_table) = S ((S (dst_index_multiply_extend_table)) * dst_negative_scale_multiply_extend_table)) /\ exists ff_q_pvs_multiply_extend_tableentrynegative. dst_negative_code_multiply_extend_table = ff_q_pvs_multiply_extend_tableentrynegative * S ((S (dst_index_multiply_extend_table)) * dst_negative_scale_multiply_extend_table) + (dst_negative_multiply_extend_table))) /\ (exists ge_balance_positive_multiply_extend_tableentryvalue ge_balance_negative_multiply_extend_tableentryvalue. (((((dst_value_multiply_extend_table) = 2 * (ge_balance_positive_multiply_extend_tableentryvalue) /\ (ge_balance_negative_multiply_extend_tableentryvalue) = 0) \/ exists ge_signed_half_multiply_extend_tableentryvaluedecode. (((dst_value_multiply_extend_table) = 2 * ge_signed_half_multiply_extend_tableentryvaluedecode + 1 /\ (ge_balance_positive_multiply_extend_tableentryvalue) = 0) /\ (ge_balance_negative_multiply_extend_tableentryvalue) = S ge_signed_half_multiply_extend_tableentryvaluedecode))) /\ ((dst_positive_multiply_extend_table) + ge_balance_negative_multiply_extend_tableentryvalue = (dst_negative_multiply_extend_table) + ge_balance_positive_multiply_extend_tableentryvalue))))))))) -> (forall dst_index_multiply_extend_preservation dst_first_multiply_extend_preservation dst_second_multiply_extend_preservation. (exists pvs_gap_multiply_extend_preservationbound. pvs_gap_multiply_extend_preservationbound + S (dst_index_multiply_extend_preservation) = (l)) -> (exists dst_positive_code_multiply_extend_preservationfirst dst_positive_scale_multiply_extend_preservationfirst dst_negative_code_multiply_extend_preservationfirst dst_negative_scale_multiply_extend_preservationfirst dst_positive_multiply_extend_preservationfirst dst_negative_multiply_extend_preservationfirst. (((H) = (((((dst_positive_code_multiply_extend_preservationfirst) + (dst_positive_scale_multiply_extend_preservationfirst)) * S ((dst_positive_code_multiply_extend_preservationfirst) + (dst_positive_scale_multiply_extend_preservationfirst)) + ((dst_positive_scale_multiply_extend_preservationfirst) + (dst_positive_scale_multiply_extend_preservationfirst))) + (((dst_negative_code_multiply_extend_preservationfirst) + (dst_negative_scale_multiply_extend_preservationfirst)) * S ((dst_negative_code_multiply_extend_preservationfirst) + (dst_negative_scale_multiply_extend_preservationfirst)) + ((dst_negative_scale_multiply_extend_preservationfirst) + (dst_negative_scale_multiply_extend_preservationfirst)))) * S ((((dst_positive_code_multiply_extend_preservationfirst) + (dst_positive_scale_multiply_extend_preservationfirst)) * S ((dst_positive_code_multiply_extend_preservationfirst) + (dst_positive_scale_multiply_extend_preservationfirst)) + ((dst_positive_scale_multiply_extend_preservationfirst) + (dst_positive_scale_multiply_extend_preservationfirst))) + (((dst_negative_code_multiply_extend_preservationfirst) + (dst_negative_scale_multiply_extend_preservationfirst)) * S ((dst_negative_code_multiply_extend_preservationfirst) + (dst_negative_scale_multiply_extend_preservationfirst)) + ((dst_negative_scale_multiply_extend_preservationfirst) + (dst_negative_scale_multiply_extend_preservationfirst)))) + ((((dst_negative_code_multiply_extend_preservationfirst) + (dst_negative_scale_multiply_extend_preservationfirst)) * S ((dst_negative_code_multiply_extend_preservationfirst) + (dst_negative_scale_multiply_extend_preservationfirst)) + ((dst_negative_scale_multiply_extend_preservationfirst) + (dst_negative_scale_multiply_extend_preservationfirst))) + (((dst_negative_code_multiply_extend_preservationfirst) + (dst_negative_scale_multiply_extend_preservationfirst)) * S ((dst_negative_code_multiply_extend_preservationfirst) + (dst_negative_scale_multiply_extend_preservationfirst)) + ((dst_negative_scale_multiply_extend_preservationfirst) + (dst_negative_scale_multiply_extend_preservationfirst)))))) /\ (((((exists ff_h_pvs_multiply_extend_preservationfirstpositive. ff_h_pvs_multiply_extend_preservationfirstpositive + S (dst_positive_multiply_extend_preservationfirst) = S ((S (dst_index_multiply_extend_preservation)) * dst_positive_scale_multiply_extend_preservationfirst)) /\ exists ff_q_pvs_multiply_extend_preservationfirstpositive. dst_positive_code_multiply_extend_preservationfirst = ff_q_pvs_multiply_extend_preservationfirstpositive * S ((S (dst_index_multiply_extend_preservation)) * dst_positive_scale_multiply_extend_preservationfirst) + (dst_positive_multiply_extend_preservationfirst))) /\ (((((exists ff_h_pvs_multiply_extend_preservationfirstnegative. ff_h_pvs_multiply_extend_preservationfirstnegative + S (dst_negative_multiply_extend_preservationfirst) = S ((S (dst_index_multiply_extend_preservation)) * dst_negative_scale_multiply_extend_preservationfirst)) /\ exists ff_q_pvs_multiply_extend_preservationfirstnegative. dst_negative_code_multiply_extend_preservationfirst = ff_q_pvs_multiply_extend_preservationfirstnegative * S ((S (dst_index_multiply_extend_preservation)) * dst_negative_scale_multiply_extend_preservationfirst) + (dst_negative_multiply_extend_preservationfirst))) /\ (exists ge_balance_positive_multiply_extend_preservationfirstvalue ge_balance_negative_multiply_extend_preservationfirstvalue. (((((dst_first_multiply_extend_preservation) = 2 * (ge_balance_positive_multiply_extend_preservationfirstvalue) /\ (ge_balance_negative_multiply_extend_preservationfirstvalue) = 0) \/ exists ge_signed_half_multiply_extend_preservationfirstvaluedecode. (((dst_first_multiply_extend_preservation) = 2 * ge_signed_half_multiply_extend_preservationfirstvaluedecode + 1 /\ (ge_balance_positive_multiply_extend_preservationfirstvalue) = 0) /\ (ge_balance_negative_multiply_extend_preservationfirstvalue) = S ge_signed_half_multiply_extend_preservationfirstvaluedecode))) /\ ((dst_positive_multiply_extend_preservationfirst) + ge_balance_negative_multiply_extend_preservationfirstvalue = (dst_negative_multiply_extend_preservationfirst) + ge_balance_positive_multiply_extend_preservationfirstvalue))))))))) -> (exists dst_positive_code_multiply_extend_preservationsecond dst_positive_scale_multiply_extend_preservationsecond dst_negative_code_multiply_extend_preservationsecond dst_negative_scale_multiply_extend_preservationsecond dst_positive_multiply_extend_preservationsecond dst_negative_multiply_extend_preservationsecond. (((K) = (((((dst_positive_code_multiply_extend_preservationsecond) + (dst_positive_scale_multiply_extend_preservationsecond)) * S ((dst_positive_code_multiply_extend_preservationsecond) + (dst_positive_scale_multiply_extend_preservationsecond)) + ((dst_positive_scale_multiply_extend_preservationsecond) + (dst_positive_scale_multiply_extend_preservationsecond))) + (((dst_negative_code_multiply_extend_preservationsecond) + (dst_negative_scale_multiply_extend_preservationsecond)) * S ((dst_negative_code_multiply_extend_preservationsecond) + (dst_negative_scale_multiply_extend_preservationsecond)) + ((dst_negative_scale_multiply_extend_preservationsecond) + (dst_negative_scale_multiply_extend_preservationsecond)))) * S ((((dst_positive_code_multiply_extend_preservationsecond) + (dst_positive_scale_multiply_extend_preservationsecond)) * S ((dst_positive_code_multiply_extend_preservationsecond) + (dst_positive_scale_multiply_extend_preservationsecond)) + ((dst_positive_scale_multiply_extend_preservationsecond) + (dst_positive_scale_multiply_extend_preservationsecond))) + (((dst_negative_code_multiply_extend_preservationsecond) + (dst_negative_scale_multiply_extend_preservationsecond)) * S ((dst_negative_code_multiply_extend_preservationsecond) + (dst_negative_scale_multiply_extend_preservationsecond)) + ((dst_negative_scale_multiply_extend_preservationsecond) + (dst_negative_scale_multiply_extend_preservationsecond)))) + ((((dst_negative_code_multiply_extend_preservationsecond) + (dst_negative_scale_multiply_extend_preservationsecond)) * S ((dst_negative_code_multiply_extend_preservationsecond) + (dst_negative_scale_multiply_extend_preservationsecond)) + ((dst_negative_scale_multiply_extend_preservationsecond) + (dst_negative_scale_multiply_extend_preservationsecond))) + (((dst_negative_code_multiply_extend_preservationsecond) + (dst_negative_scale_multiply_extend_preservationsecond)) * S ((dst_negative_code_multiply_extend_preservationsecond) + (dst_negative_scale_multiply_extend_preservationsecond)) + ((dst_negative_scale_multiply_extend_preservationsecond) + (dst_negative_scale_multiply_extend_preservationsecond)))))) /\ (((((exists ff_h_pvs_multiply_extend_preservationsecondpositive. ff_h_pvs_multiply_extend_preservationsecondpositive + S (dst_positive_multiply_extend_preservationsecond) = S ((S (dst_index_multiply_extend_preservation)) * dst_positive_scale_multiply_extend_preservationsecond)) /\ exists ff_q_pvs_multiply_extend_preservationsecondpositive. dst_positive_code_multiply_extend_preservationsecond = ff_q_pvs_multiply_extend_preservationsecondpositive * S ((S (dst_index_multiply_extend_preservation)) * dst_positive_scale_multiply_extend_preservationsecond) + (dst_positive_multiply_extend_preservationsecond))) /\ (((((exists ff_h_pvs_multiply_extend_preservationsecondnegative. ff_h_pvs_multiply_extend_preservationsecondnegative + S (dst_negative_multiply_extend_preservationsecond) = S ((S (dst_index_multiply_extend_preservation)) * dst_negative_scale_multiply_extend_preservationsecond)) /\ exists ff_q_pvs_multiply_extend_preservationsecondnegative. dst_negative_code_multiply_extend_preservationsecond = ff_q_pvs_multiply_extend_preservationsecondnegative * S ((S (dst_index_multiply_extend_preservation)) * dst_negative_scale_multiply_extend_preservationsecond) + (dst_negative_multiply_extend_preservationsecond))) /\ (exists ge_balance_positive_multiply_extend_preservationsecondvalue ge_balance_negative_multiply_extend_preservationsecondvalue. (((((dst_second_multiply_extend_preservation) = 2 * (ge_balance_positive_multiply_extend_preservationsecondvalue) /\ (ge_balance_negative_multiply_extend_preservationsecondvalue) = 0) \/ exists ge_signed_half_multiply_extend_preservationsecondvaluedecode. (((dst_second_multiply_extend_preservation) = 2 * ge_signed_half_multiply_extend_preservationsecondvaluedecode + 1 /\ (ge_balance_positive_multiply_extend_preservationsecondvalue) = 0) /\ (ge_balance_negative_multiply_extend_preservationsecondvalue) = S ge_signed_half_multiply_extend_preservationsecondvaluedecode))) /\ ((dst_positive_multiply_extend_preservationsecond) + ge_balance_negative_multiply_extend_preservationsecondvalue = (dst_negative_multiply_extend_preservationsecond) + ge_balance_positive_multiply_extend_preservationsecondvalue))))))))) -> dst_first_multiply_extend_preservation = dst_second_multiply_extend_preservation) -> (exists dst_positive_code_multiply_extend_at_0 dst_positive_scale_multiply_extend_at_0 dst_negative_code_multiply_extend_at_0 dst_negative_scale_multiply_extend_at_0 dst_positive_multiply_extend_at_0 dst_negative_multiply_extend_at_0. (((F) = (((((dst_positive_code_multiply_extend_at_0) + (dst_positive_scale_multiply_extend_at_0)) * S ((dst_positive_code_multiply_extend_at_0) + (dst_positive_scale_multiply_extend_at_0)) + ((dst_positive_scale_multiply_extend_at_0) + (dst_positive_scale_multiply_extend_at_0))) + (((dst_negative_code_multiply_extend_at_0) + (dst_negative_scale_multiply_extend_at_0)) * S ((dst_negative_code_multiply_extend_at_0) + (dst_negative_scale_multiply_extend_at_0)) + ((dst_negative_scale_multiply_extend_at_0) + (dst_negative_scale_multiply_extend_at_0)))) * S ((((dst_positive_code_multiply_extend_at_0) + (dst_positive_scale_multiply_extend_at_0)) * S ((dst_positive_code_multiply_extend_at_0) + (dst_positive_scale_multiply_extend_at_0)) + ((dst_positive_scale_multiply_extend_at_0) + (dst_positive_scale_multiply_extend_at_0))) + (((dst_negative_code_multiply_extend_at_0) + (dst_negative_scale_multiply_extend_at_0)) * S ((dst_negative_code_multiply_extend_at_0) + (dst_negative_scale_multiply_extend_at_0)) + ((dst_negative_scale_multiply_extend_at_0) + (dst_negative_scale_multiply_extend_at_0)))) + ((((dst_negative_code_multiply_extend_at_0) + (dst_negative_scale_multiply_extend_at_0)) * S ((dst_negative_code_multiply_extend_at_0) + (dst_negative_scale_multiply_extend_at_0)) + ((dst_negative_scale_multiply_extend_at_0) + (dst_negative_scale_multiply_extend_at_0))) + (((dst_negative_code_multiply_extend_at_0) + (dst_negative_scale_multiply_extend_at_0)) * S ((dst_negative_code_multiply_extend_at_0) + (dst_negative_scale_multiply_extend_at_0)) + ((dst_negative_scale_multiply_extend_at_0) + (dst_negative_scale_multiply_extend_at_0)))))) /\ (((((exists ff_h_pvs_multiply_extend_at_0positive. ff_h_pvs_multiply_extend_at_0positive + S (dst_positive_multiply_extend_at_0) = S ((S (l)) * dst_positive_scale_multiply_extend_at_0)) /\ exists ff_q_pvs_multiply_extend_at_0positive. dst_positive_code_multiply_extend_at_0 = ff_q_pvs_multiply_extend_at_0positive * S ((S (l)) * dst_positive_scale_multiply_extend_at_0) + (dst_positive_multiply_extend_at_0))) /\ (((((exists ff_h_pvs_multiply_extend_at_0negative. ff_h_pvs_multiply_extend_at_0negative + S (dst_negative_multiply_extend_at_0) = S ((S (l)) * dst_negative_scale_multiply_extend_at_0)) /\ exists ff_q_pvs_multiply_extend_at_0negative. dst_negative_code_multiply_extend_at_0 = ff_q_pvs_multiply_extend_at_0negative * S ((S (l)) * dst_negative_scale_multiply_extend_at_0) + (dst_negative_multiply_extend_at_0))) /\ (exists ge_balance_positive_multiply_extend_at_0value ge_balance_negative_multiply_extend_at_0value. (((((a) = 2 * (ge_balance_positive_multiply_extend_at_0value) /\ (ge_balance_negative_multiply_extend_at_0value) = 0) \/ exists ge_signed_half_multiply_extend_at_0valuedecode. (((a) = 2 * ge_signed_half_multiply_extend_at_0valuedecode + 1 /\ (ge_balance_positive_multiply_extend_at_0value) = 0) /\ (ge_balance_negative_multiply_extend_at_0value) = S ge_signed_half_multiply_extend_at_0valuedecode))) /\ ((dst_positive_multiply_extend_at_0) + ge_balance_negative_multiply_extend_at_0value = (dst_negative_multiply_extend_at_0) + ge_balance_positive_multiply_extend_at_0value))))))))) -> (exists dst_positive_code_multiply_extend_at_1 dst_positive_scale_multiply_extend_at_1 dst_negative_code_multiply_extend_at_1 dst_negative_scale_multiply_extend_at_1 dst_positive_multiply_extend_at_1 dst_negative_multiply_extend_at_1. (((G) = (((((dst_positive_code_multiply_extend_at_1) + (dst_positive_scale_multiply_extend_at_1)) * S ((dst_positive_code_multiply_extend_at_1) + (dst_positive_scale_multiply_extend_at_1)) + ((dst_positive_scale_multiply_extend_at_1) + (dst_positive_scale_multiply_extend_at_1))) + (((dst_negative_code_multiply_extend_at_1) + (dst_negative_scale_multiply_extend_at_1)) * S ((dst_negative_code_multiply_extend_at_1) + (dst_negative_scale_multiply_extend_at_1)) + ((dst_negative_scale_multiply_extend_at_1) + (dst_negative_scale_multiply_extend_at_1)))) * S ((((dst_positive_code_multiply_extend_at_1) + (dst_positive_scale_multiply_extend_at_1)) * S ((dst_positive_code_multiply_extend_at_1) + (dst_positive_scale_multiply_extend_at_1)) + ((dst_positive_scale_multiply_extend_at_1) + (dst_positive_scale_multiply_extend_at_1))) + (((dst_negative_code_multiply_extend_at_1) + (dst_negative_scale_multiply_extend_at_1)) * S ((dst_negative_code_multiply_extend_at_1) + (dst_negative_scale_multiply_extend_at_1)) + ((dst_negative_scale_multiply_extend_at_1) + (dst_negative_scale_multiply_extend_at_1)))) + ((((dst_negative_code_multiply_extend_at_1) + (dst_negative_scale_multiply_extend_at_1)) * S ((dst_negative_code_multiply_extend_at_1) + (dst_negative_scale_multiply_extend_at_1)) + ((dst_negative_scale_multiply_extend_at_1) + (dst_negative_scale_multiply_extend_at_1))) + (((dst_negative_code_multiply_extend_at_1) + (dst_negative_scale_multiply_extend_at_1)) * S ((dst_negative_code_multiply_extend_at_1) + (dst_negative_scale_multiply_extend_at_1)) + ((dst_negative_scale_multiply_extend_at_1) + (dst_negative_scale_multiply_extend_at_1)))))) /\ (((((exists ff_h_pvs_multiply_extend_at_1positive. ff_h_pvs_multiply_extend_at_1positive + S (dst_positive_multiply_extend_at_1) = S ((S (l)) * dst_positive_scale_multiply_extend_at_1)) /\ exists ff_q_pvs_multiply_extend_at_1positive. dst_positive_code_multiply_extend_at_1 = ff_q_pvs_multiply_extend_at_1positive * S ((S (l)) * dst_positive_scale_multiply_extend_at_1) + (dst_positive_multiply_extend_at_1))) /\ (((((exists ff_h_pvs_multiply_extend_at_1negative. ff_h_pvs_multiply_extend_at_1negative + S (dst_negative_multiply_extend_at_1) = S ((S (l)) * dst_negative_scale_multiply_extend_at_1)) /\ exists ff_q_pvs_multiply_extend_at_1negative. dst_negative_code_multiply_extend_at_1 = ff_q_pvs_multiply_extend_at_1negative * S ((S (l)) * dst_negative_scale_multiply_extend_at_1) + (dst_negative_multiply_extend_at_1))) /\ (exists ge_balance_positive_multiply_extend_at_1value ge_balance_negative_multiply_extend_at_1value. (((((b) = 2 * (ge_balance_positive_multiply_extend_at_1value) /\ (ge_balance_negative_multiply_extend_at_1value) = 0) \/ exists ge_signed_half_multiply_extend_at_1valuedecode. (((b) = 2 * ge_signed_half_multiply_extend_at_1valuedecode + 1 /\ (ge_balance_positive_multiply_extend_at_1value) = 0) /\ (ge_balance_negative_multiply_extend_at_1value) = S ge_signed_half_multiply_extend_at_1valuedecode))) /\ ((dst_positive_multiply_extend_at_1) + ge_balance_negative_multiply_extend_at_1value = (dst_negative_multiply_extend_at_1) + ge_balance_positive_multiply_extend_at_1value))))))))) -> (exists dst_positive_code_multiply_extend_at_2 dst_positive_scale_multiply_extend_at_2 dst_negative_code_multiply_extend_at_2 dst_negative_scale_multiply_extend_at_2 dst_positive_multiply_extend_at_2 dst_negative_multiply_extend_at_2. (((K) = (((((dst_positive_code_multiply_extend_at_2) + (dst_positive_scale_multiply_extend_at_2)) * S ((dst_positive_code_multiply_extend_at_2) + (dst_positive_scale_multiply_extend_at_2)) + ((dst_positive_scale_multiply_extend_at_2) + (dst_positive_scale_multiply_extend_at_2))) + (((dst_negative_code_multiply_extend_at_2) + (dst_negative_scale_multiply_extend_at_2)) * S ((dst_negative_code_multiply_extend_at_2) + (dst_negative_scale_multiply_extend_at_2)) + ((dst_negative_scale_multiply_extend_at_2) + (dst_negative_scale_multiply_extend_at_2)))) * S ((((dst_positive_code_multiply_extend_at_2) + (dst_positive_scale_multiply_extend_at_2)) * S ((dst_positive_code_multiply_extend_at_2) + (dst_positive_scale_multiply_extend_at_2)) + ((dst_positive_scale_multiply_extend_at_2) + (dst_positive_scale_multiply_extend_at_2))) + (((dst_negative_code_multiply_extend_at_2) + (dst_negative_scale_multiply_extend_at_2)) * S ((dst_negative_code_multiply_extend_at_2) + (dst_negative_scale_multiply_extend_at_2)) + ((dst_negative_scale_multiply_extend_at_2) + (dst_negative_scale_multiply_extend_at_2)))) + ((((dst_negative_code_multiply_extend_at_2) + (dst_negative_scale_multiply_extend_at_2)) * S ((dst_negative_code_multiply_extend_at_2) + (dst_negative_scale_multiply_extend_at_2)) + ((dst_negative_scale_multiply_extend_at_2) + (dst_negative_scale_multiply_extend_at_2))) + (((dst_negative_code_multiply_extend_at_2) + (dst_negative_scale_multiply_extend_at_2)) * S ((dst_negative_code_multiply_extend_at_2) + (dst_negative_scale_multiply_extend_at_2)) + ((dst_negative_scale_multiply_extend_at_2) + (dst_negative_scale_multiply_extend_at_2)))))) /\ (((((exists ff_h_pvs_multiply_extend_at_2positive. ff_h_pvs_multiply_extend_at_2positive + S (dst_positive_multiply_extend_at_2) = S ((S (l)) * dst_positive_scale_multiply_extend_at_2)) /\ exists ff_q_pvs_multiply_extend_at_2positive. dst_positive_code_multiply_extend_at_2 = ff_q_pvs_multiply_extend_at_2positive * S ((S (l)) * dst_positive_scale_multiply_extend_at_2) + (dst_positive_multiply_extend_at_2))) /\ (((((exists ff_h_pvs_multiply_extend_at_2negative. ff_h_pvs_multiply_extend_at_2negative + S (dst_negative_multiply_extend_at_2) = S ((S (l)) * dst_negative_scale_multiply_extend_at_2)) /\ exists ff_q_pvs_multiply_extend_at_2negative. dst_negative_code_multiply_extend_at_2 = ff_q_pvs_multiply_extend_at_2negative * S ((S (l)) * dst_negative_scale_multiply_extend_at_2) + (dst_negative_multiply_extend_at_2))) /\ (exists ge_balance_positive_multiply_extend_at_2value ge_balance_negative_multiply_extend_at_2value. (((((c) = 2 * (ge_balance_positive_multiply_extend_at_2value) /\ (ge_balance_negative_multiply_extend_at_2value) = 0) \/ exists ge_signed_half_multiply_extend_at_2valuedecode. (((c) = 2 * ge_signed_half_multiply_extend_at_2valuedecode + 1 /\ (ge_balance_positive_multiply_extend_at_2value) = 0) /\ (ge_balance_negative_multiply_extend_at_2value) = S ge_signed_half_multiply_extend_at_2valuedecode))) /\ ((dst_positive_multiply_extend_at_2) + ge_balance_negative_multiply_extend_at_2value = (dst_negative_multiply_extend_at_2) + ge_balance_positive_multiply_extend_at_2value))))))))) -> (exists sto_ap_multiply_extend_operation sto_an_multiply_extend_operation sto_bp_multiply_extend_operation sto_bn_multiply_extend_operation sto_cp_multiply_extend_operation sto_cn_multiply_extend_operation. (((((a) = 2 * (sto_ap_multiply_extend_operation) /\ (sto_an_multiply_extend_operation) = 0) \/ exists ge_signed_half_multiply_extend_operationleft. (((a) = 2 * ge_signed_half_multiply_extend_operationleft + 1 /\ (sto_ap_multiply_extend_operation) = 0) /\ (sto_an_multiply_extend_operation) = S ge_signed_half_multiply_extend_operationleft))) /\ ((((((b) = 2 * (sto_bp_multiply_extend_operation) /\ (sto_bn_multiply_extend_operation) = 0) \/ exists ge_signed_half_multiply_extend_operationright. (((b) = 2 * ge_signed_half_multiply_extend_operationright + 1 /\ (sto_bp_multiply_extend_operation) = 0) /\ (sto_bn_multiply_extend_operation) = S ge_signed_half_multiply_extend_operationright))) /\ ((((((c) = 2 * (sto_cp_multiply_extend_operation) /\ (sto_cn_multiply_extend_operation) = 0) \/ exists ge_signed_half_multiply_extend_operationoutput. (((c) = 2 * ge_signed_half_multiply_extend_operationoutput + 1 /\ (sto_cp_multiply_extend_operation) = 0) /\ (sto_cn_multiply_extend_operation) = S ge_signed_half_multiply_extend_operationoutput))) /\ ((sto_ap_multiply_extend_operation * sto_bp_multiply_extend_operation + sto_an_multiply_extend_operation * sto_bn_multiply_extend_operation) + sto_cn_multiply_extend_operation = (sto_ap_multiply_extend_operation * sto_bn_multiply_extend_operation + sto_an_multiply_extend_operation * sto_bp_multiply_extend_operation) + sto_cp_multiply_extend_operation))))))) -> (((exists dst_positive_code_multiply_extend_resultleft_table dst_positive_scale_multiply_extend_resultleft_table dst_negative_code_multiply_extend_resultleft_table dst_negative_scale_multiply_extend_resultleft_table. (((F) = (((((dst_positive_code_multiply_extend_resultleft_table) + (dst_positive_scale_multiply_extend_resultleft_table)) * S ((dst_positive_code_multiply_extend_resultleft_table) + (dst_positive_scale_multiply_extend_resultleft_table)) + ((dst_positive_scale_multiply_extend_resultleft_table) + (dst_positive_scale_multiply_extend_resultleft_table))) + (((dst_negative_code_multiply_extend_resultleft_table) + (dst_negative_scale_multiply_extend_resultleft_table)) * S ((dst_negative_code_multiply_extend_resultleft_table) + (dst_negative_scale_multiply_extend_resultleft_table)) + ((dst_negative_scale_multiply_extend_resultleft_table) + (dst_negative_scale_multiply_extend_resultleft_table)))) * S ((((dst_positive_code_multiply_extend_resultleft_table) + (dst_positive_scale_multiply_extend_resultleft_table)) * S ((dst_positive_code_multiply_extend_resultleft_table) + (dst_positive_scale_multiply_extend_resultleft_table)) + ((dst_positive_scale_multiply_extend_resultleft_table) + (dst_positive_scale_multiply_extend_resultleft_table))) + (((dst_negative_code_multiply_extend_resultleft_table) + (dst_negative_scale_multiply_extend_resultleft_table)) * S ((dst_negative_code_multiply_extend_resultleft_table) + (dst_negative_scale_multiply_extend_resultleft_table)) + ((dst_negative_scale_multiply_extend_resultleft_table) + (dst_negative_scale_multiply_extend_resultleft_table)))) + ((((dst_negative_code_multiply_extend_resultleft_table) + (dst_negative_scale_multiply_extend_resultleft_table)) * S ((dst_negative_code_multiply_extend_resultleft_table) + (dst_negative_scale_multiply_extend_resultleft_table)) + ((dst_negative_scale_multiply_extend_resultleft_table) + (dst_negative_scale_multiply_extend_resultleft_table))) + (((dst_negative_code_multiply_extend_resultleft_table) + (dst_negative_scale_multiply_extend_resultleft_table)) * S ((dst_negative_code_multiply_extend_resultleft_table) + (dst_negative_scale_multiply_extend_resultleft_table)) + ((dst_negative_scale_multiply_extend_resultleft_table) + (dst_negative_scale_multiply_extend_resultleft_table)))))) /\ (forall dst_index_multiply_extend_resultleft_table. (exists pvs_le_gap_multiply_extend_resultleft_tabledomain. pvs_le_gap_multiply_extend_resultleft_tabledomain + (dst_index_multiply_extend_resultleft_table) = (S l)) -> exists dst_positive_multiply_extend_resultleft_table dst_negative_multiply_extend_resultleft_table dst_value_multiply_extend_resultleft_table. ((((exists ff_h_pvs_multiply_extend_resultleft_tableentrypositive. ff_h_pvs_multiply_extend_resultleft_tableentrypositive + S (dst_positive_multiply_extend_resultleft_table) = S ((S (dst_index_multiply_extend_resultleft_table)) * dst_positive_scale_multiply_extend_resultleft_table)) /\ exists ff_q_pvs_multiply_extend_resultleft_tableentrypositive. dst_positive_code_multiply_extend_resultleft_table = ff_q_pvs_multiply_extend_resultleft_tableentrypositive * S ((S (dst_index_multiply_extend_resultleft_table)) * dst_positive_scale_multiply_extend_resultleft_table) + (dst_positive_multiply_extend_resultleft_table))) /\ (((((exists ff_h_pvs_multiply_extend_resultleft_tableentrynegative. ff_h_pvs_multiply_extend_resultleft_tableentrynegative + S (dst_negative_multiply_extend_resultleft_table) = S ((S (dst_index_multiply_extend_resultleft_table)) * dst_negative_scale_multiply_extend_resultleft_table)) /\ exists ff_q_pvs_multiply_extend_resultleft_tableentrynegative. dst_negative_code_multiply_extend_resultleft_table = ff_q_pvs_multiply_extend_resultleft_tableentrynegative * S ((S (dst_index_multiply_extend_resultleft_table)) * dst_negative_scale_multiply_extend_resultleft_table) + (dst_negative_multiply_extend_resultleft_table))) /\ (exists ge_balance_positive_multiply_extend_resultleft_tableentryvalue ge_balance_negative_multiply_extend_resultleft_tableentryvalue. (((((dst_value_multiply_extend_resultleft_table) = 2 * (ge_balance_positive_multiply_extend_resultleft_tableentryvalue) /\ (ge_balance_negative_multiply_extend_resultleft_tableentryvalue) = 0) \/ exists ge_signed_half_multiply_extend_resultleft_tableentryvaluedecode. (((dst_value_multiply_extend_resultleft_table) = 2 * ge_signed_half_multiply_extend_resultleft_tableentryvaluedecode + 1 /\ (ge_balance_positive_multiply_extend_resultleft_tableentryvalue) = 0) /\ (ge_balance_negative_multiply_extend_resultleft_tableentryvalue) = S ge_signed_half_multiply_extend_resultleft_tableentryvaluedecode))) /\ ((dst_positive_multiply_extend_resultleft_table) + ge_balance_negative_multiply_extend_resultleft_tableentryvalue = (dst_negative_multiply_extend_resultleft_table) + ge_balance_positive_multiply_extend_resultleft_tableentryvalue))))))))) /\ (((exists dst_positive_code_multiply_extend_resultright_table dst_positive_scale_multiply_extend_resultright_table dst_negative_code_multiply_extend_resultright_table dst_negative_scale_multiply_extend_resultright_table. (((G) = (((((dst_positive_code_multiply_extend_resultright_table) + (dst_positive_scale_multiply_extend_resultright_table)) * S ((dst_positive_code_multiply_extend_resultright_table) + (dst_positive_scale_multiply_extend_resultright_table)) + ((dst_positive_scale_multiply_extend_resultright_table) + (dst_positive_scale_multiply_extend_resultright_table))) + (((dst_negative_code_multiply_extend_resultright_table) + (dst_negative_scale_multiply_extend_resultright_table)) * S ((dst_negative_code_multiply_extend_resultright_table) + (dst_negative_scale_multiply_extend_resultright_table)) + ((dst_negative_scale_multiply_extend_resultright_table) + (dst_negative_scale_multiply_extend_resultright_table)))) * S ((((dst_positive_code_multiply_extend_resultright_table) + (dst_positive_scale_multiply_extend_resultright_table)) * S ((dst_positive_code_multiply_extend_resultright_table) + (dst_positive_scale_multiply_extend_resultright_table)) + ((dst_positive_scale_multiply_extend_resultright_table) + (dst_positive_scale_multiply_extend_resultright_table))) + (((dst_negative_code_multiply_extend_resultright_table) + (dst_negative_scale_multiply_extend_resultright_table)) * S ((dst_negative_code_multiply_extend_resultright_table) + (dst_negative_scale_multiply_extend_resultright_table)) + ((dst_negative_scale_multiply_extend_resultright_table) + (dst_negative_scale_multiply_extend_resultright_table)))) + ((((dst_negative_code_multiply_extend_resultright_table) + (dst_negative_scale_multiply_extend_resultright_table)) * S ((dst_negative_code_multiply_extend_resultright_table) + (dst_negative_scale_multiply_extend_resultright_table)) + ((dst_negative_scale_multiply_extend_resultright_table) + (dst_negative_scale_multiply_extend_resultright_table))) + (((dst_negative_code_multiply_extend_resultright_table) + (dst_negative_scale_multiply_extend_resultright_table)) * S ((dst_negative_code_multiply_extend_resultright_table) + (dst_negative_scale_multiply_extend_resultright_table)) + ((dst_negative_scale_multiply_extend_resultright_table) + (dst_negative_scale_multiply_extend_resultright_table)))))) /\ (forall dst_index_multiply_extend_resultright_table. (exists pvs_le_gap_multiply_extend_resultright_tabledomain. pvs_le_gap_multiply_extend_resultright_tabledomain + (dst_index_multiply_extend_resultright_table) = (S l)) -> exists dst_positive_multiply_extend_resultright_table dst_negative_multiply_extend_resultright_table dst_value_multiply_extend_resultright_table. ((((exists ff_h_pvs_multiply_extend_resultright_tableentrypositive. ff_h_pvs_multiply_extend_resultright_tableentrypositive + S (dst_positive_multiply_extend_resultright_table) = S ((S (dst_index_multiply_extend_resultright_table)) * dst_positive_scale_multiply_extend_resultright_table)) /\ exists ff_q_pvs_multiply_extend_resultright_tableentrypositive. dst_positive_code_multiply_extend_resultright_table = ff_q_pvs_multiply_extend_resultright_tableentrypositive * S ((S (dst_index_multiply_extend_resultright_table)) * dst_positive_scale_multiply_extend_resultright_table) + (dst_positive_multiply_extend_resultright_table))) /\ (((((exists ff_h_pvs_multiply_extend_resultright_tableentrynegative. ff_h_pvs_multiply_extend_resultright_tableentrynegative + S (dst_negative_multiply_extend_resultright_table) = S ((S (dst_index_multiply_extend_resultright_table)) * dst_negative_scale_multiply_extend_resultright_table)) /\ exists ff_q_pvs_multiply_extend_resultright_tableentrynegative. dst_negative_code_multiply_extend_resultright_table = ff_q_pvs_multiply_extend_resultright_tableentrynegative * S ((S (dst_index_multiply_extend_resultright_table)) * dst_negative_scale_multiply_extend_resultright_table) + (dst_negative_multiply_extend_resultright_table))) /\ (exists ge_balance_positive_multiply_extend_resultright_tableentryvalue ge_balance_negative_multiply_extend_resultright_tableentryvalue. (((((dst_value_multiply_extend_resultright_table) = 2 * (ge_balance_positive_multiply_extend_resultright_tableentryvalue) /\ (ge_balance_negative_multiply_extend_resultright_tableentryvalue) = 0) \/ exists ge_signed_half_multiply_extend_resultright_tableentryvaluedecode. (((dst_value_multiply_extend_resultright_table) = 2 * ge_signed_half_multiply_extend_resultright_tableentryvaluedecode + 1 /\ (ge_balance_positive_multiply_extend_resultright_tableentryvalue) = 0) /\ (ge_balance_negative_multiply_extend_resultright_tableentryvalue) = S ge_signed_half_multiply_extend_resultright_tableentryvaluedecode))) /\ ((dst_positive_multiply_extend_resultright_table) + ge_balance_negative_multiply_extend_resultright_tableentryvalue = (dst_negative_multiply_extend_resultright_table) + ge_balance_positive_multiply_extend_resultright_tableentryvalue))))))))) /\ (((exists dst_positive_code_multiply_extend_resultoutput_table dst_positive_scale_multiply_extend_resultoutput_table dst_negative_code_multiply_extend_resultoutput_table dst_negative_scale_multiply_extend_resultoutput_table. (((K) = (((((dst_positive_code_multiply_extend_resultoutput_table) + (dst_positive_scale_multiply_extend_resultoutput_table)) * S ((dst_positive_code_multiply_extend_resultoutput_table) + (dst_positive_scale_multiply_extend_resultoutput_table)) + ((dst_positive_scale_multiply_extend_resultoutput_table) + (dst_positive_scale_multiply_extend_resultoutput_table))) + (((dst_negative_code_multiply_extend_resultoutput_table) + (dst_negative_scale_multiply_extend_resultoutput_table)) * S ((dst_negative_code_multiply_extend_resultoutput_table) + (dst_negative_scale_multiply_extend_resultoutput_table)) + ((dst_negative_scale_multiply_extend_resultoutput_table) + (dst_negative_scale_multiply_extend_resultoutput_table)))) * S ((((dst_positive_code_multiply_extend_resultoutput_table) + (dst_positive_scale_multiply_extend_resultoutput_table)) * S ((dst_positive_code_multiply_extend_resultoutput_table) + (dst_positive_scale_multiply_extend_resultoutput_table)) + ((dst_positive_scale_multiply_extend_resultoutput_table) + (dst_positive_scale_multiply_extend_resultoutput_table))) + (((dst_negative_code_multiply_extend_resultoutput_table) + (dst_negative_scale_multiply_extend_resultoutput_table)) * S ((dst_negative_code_multiply_extend_resultoutput_table) + (dst_negative_scale_multiply_extend_resultoutput_table)) + ((dst_negative_scale_multiply_extend_resultoutput_table) + (dst_negative_scale_multiply_extend_resultoutput_table)))) + ((((dst_negative_code_multiply_extend_resultoutput_table) + (dst_negative_scale_multiply_extend_resultoutput_table)) * S ((dst_negative_code_multiply_extend_resultoutput_table) + (dst_negative_scale_multiply_extend_resultoutput_table)) + ((dst_negative_scale_multiply_extend_resultoutput_table) + (dst_negative_scale_multiply_extend_resultoutput_table))) + (((dst_negative_code_multiply_extend_resultoutput_table) + (dst_negative_scale_multiply_extend_resultoutput_table)) * S ((dst_negative_code_multiply_extend_resultoutput_table) + (dst_negative_scale_multiply_extend_resultoutput_table)) + ((dst_negative_scale_multiply_extend_resultoutput_table) + (dst_negative_scale_multiply_extend_resultoutput_table)))))) /\ (forall dst_index_multiply_extend_resultoutput_table. (exists pvs_le_gap_multiply_extend_resultoutput_tabledomain. pvs_le_gap_multiply_extend_resultoutput_tabledomain + (dst_index_multiply_extend_resultoutput_table) = (S l)) -> exists dst_positive_multiply_extend_resultoutput_table dst_negative_multiply_extend_resultoutput_table dst_value_multiply_extend_resultoutput_table. ((((exists ff_h_pvs_multiply_extend_resultoutput_tableentrypositive. ff_h_pvs_multiply_extend_resultoutput_tableentrypositive + S (dst_positive_multiply_extend_resultoutput_table) = S ((S (dst_index_multiply_extend_resultoutput_table)) * dst_positive_scale_multiply_extend_resultoutput_table)) /\ exists ff_q_pvs_multiply_extend_resultoutput_tableentrypositive. dst_positive_code_multiply_extend_resultoutput_table = ff_q_pvs_multiply_extend_resultoutput_tableentrypositive * S ((S (dst_index_multiply_extend_resultoutput_table)) * dst_positive_scale_multiply_extend_resultoutput_table) + (dst_positive_multiply_extend_resultoutput_table))) /\ (((((exists ff_h_pvs_multiply_extend_resultoutput_tableentrynegative. ff_h_pvs_multiply_extend_resultoutput_tableentrynegative + S (dst_negative_multiply_extend_resultoutput_table) = S ((S (dst_index_multiply_extend_resultoutput_table)) * dst_negative_scale_multiply_extend_resultoutput_table)) /\ exists ff_q_pvs_multiply_extend_resultoutput_tableentrynegative. dst_negative_code_multiply_extend_resultoutput_table = ff_q_pvs_multiply_extend_resultoutput_tableentrynegative * S ((S (dst_index_multiply_extend_resultoutput_table)) * dst_negative_scale_multiply_extend_resultoutput_table) + (dst_negative_multiply_extend_resultoutput_table))) /\ (exists ge_balance_positive_multiply_extend_resultoutput_tableentryvalue ge_balance_negative_multiply_extend_resultoutput_tableentryvalue. (((((dst_value_multiply_extend_resultoutput_table) = 2 * (ge_balance_positive_multiply_extend_resultoutput_tableentryvalue) /\ (ge_balance_negative_multiply_extend_resultoutput_tableentryvalue) = 0) \/ exists ge_signed_half_multiply_extend_resultoutput_tableentryvaluedecode. (((dst_value_multiply_extend_resultoutput_table) = 2 * ge_signed_half_multiply_extend_resultoutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_multiply_extend_resultoutput_tableentryvalue) = 0) /\ (ge_balance_negative_multiply_extend_resultoutput_tableentryvalue) = S ge_signed_half_multiply_extend_resultoutput_tableentryvaluedecode))) /\ ((dst_positive_multiply_extend_resultoutput_table) + ge_balance_negative_multiply_extend_resultoutput_tableentryvalue = (dst_negative_multiply_extend_resultoutput_table) + ge_balance_positive_multiply_extend_resultoutput_tableentryvalue))))))))) /\ (forall sto_index_multiply_extend_resultentries. (exists pvs_gap_multiply_extend_resultentriesbound. pvs_gap_multiply_extend_resultentriesbound + S (sto_index_multiply_extend_resultentries) = (S l)) -> exists sto_left_multiply_extend_resultentries sto_right_multiply_extend_resultentries sto_output_multiply_extend_resultentries. ((exists dst_positive_code_multiply_extend_resultentriesentryleft dst_positive_scale_multiply_extend_resultentriesentryleft dst_negative_code_multiply_extend_resultentriesentryleft dst_negative_scale_multiply_extend_resultentriesentryleft dst_positive_multiply_extend_resultentriesentryleft dst_negative_multiply_extend_resultentriesentryleft. (((F) = (((((dst_positive_code_multiply_extend_resultentriesentryleft) + (dst_positive_scale_multiply_extend_resultentriesentryleft)) * S ((dst_positive_code_multiply_extend_resultentriesentryleft) + (dst_positive_scale_multiply_extend_resultentriesentryleft)) + ((dst_positive_scale_multiply_extend_resultentriesentryleft) + (dst_positive_scale_multiply_extend_resultentriesentryleft))) + (((dst_negative_code_multiply_extend_resultentriesentryleft) + (dst_negative_scale_multiply_extend_resultentriesentryleft)) * S ((dst_negative_code_multiply_extend_resultentriesentryleft) + (dst_negative_scale_multiply_extend_resultentriesentryleft)) + ((dst_negative_scale_multiply_extend_resultentriesentryleft) + (dst_negative_scale_multiply_extend_resultentriesentryleft)))) * S ((((dst_positive_code_multiply_extend_resultentriesentryleft) + (dst_positive_scale_multiply_extend_resultentriesentryleft)) * S ((dst_positive_code_multiply_extend_resultentriesentryleft) + (dst_positive_scale_multiply_extend_resultentriesentryleft)) + ((dst_positive_scale_multiply_extend_resultentriesentryleft) + (dst_positive_scale_multiply_extend_resultentriesentryleft))) + (((dst_negative_code_multiply_extend_resultentriesentryleft) + (dst_negative_scale_multiply_extend_resultentriesentryleft)) * S ((dst_negative_code_multiply_extend_resultentriesentryleft) + (dst_negative_scale_multiply_extend_resultentriesentryleft)) + ((dst_negative_scale_multiply_extend_resultentriesentryleft) + (dst_negative_scale_multiply_extend_resultentriesentryleft)))) + ((((dst_negative_code_multiply_extend_resultentriesentryleft) + (dst_negative_scale_multiply_extend_resultentriesentryleft)) * S ((dst_negative_code_multiply_extend_resultentriesentryleft) + (dst_negative_scale_multiply_extend_resultentriesentryleft)) + ((dst_negative_scale_multiply_extend_resultentriesentryleft) + (dst_negative_scale_multiply_extend_resultentriesentryleft))) + (((dst_negative_code_multiply_extend_resultentriesentryleft) + (dst_negative_scale_multiply_extend_resultentriesentryleft)) * S ((dst_negative_code_multiply_extend_resultentriesentryleft) + (dst_negative_scale_multiply_extend_resultentriesentryleft)) + ((dst_negative_scale_multiply_extend_resultentriesentryleft) + (dst_negative_scale_multiply_extend_resultentriesentryleft)))))) /\ (((((exists ff_h_pvs_multiply_extend_resultentriesentryleftpositive. ff_h_pvs_multiply_extend_resultentriesentryleftpositive + S (dst_positive_multiply_extend_resultentriesentryleft) = S ((S (sto_index_multiply_extend_resultentries)) * dst_positive_scale_multiply_extend_resultentriesentryleft)) /\ exists ff_q_pvs_multiply_extend_resultentriesentryleftpositive. dst_positive_code_multiply_extend_resultentriesentryleft = ff_q_pvs_multiply_extend_resultentriesentryleftpositive * S ((S (sto_index_multiply_extend_resultentries)) * dst_positive_scale_multiply_extend_resultentriesentryleft) + (dst_positive_multiply_extend_resultentriesentryleft))) /\ (((((exists ff_h_pvs_multiply_extend_resultentriesentryleftnegative. ff_h_pvs_multiply_extend_resultentriesentryleftnegative + S (dst_negative_multiply_extend_resultentriesentryleft) = S ((S (sto_index_multiply_extend_resultentries)) * dst_negative_scale_multiply_extend_resultentriesentryleft)) /\ exists ff_q_pvs_multiply_extend_resultentriesentryleftnegative. dst_negative_code_multiply_extend_resultentriesentryleft = ff_q_pvs_multiply_extend_resultentriesentryleftnegative * S ((S (sto_index_multiply_extend_resultentries)) * dst_negative_scale_multiply_extend_resultentriesentryleft) + (dst_negative_multiply_extend_resultentriesentryleft))) /\ (exists ge_balance_positive_multiply_extend_resultentriesentryleftvalue ge_balance_negative_multiply_extend_resultentriesentryleftvalue. (((((sto_left_multiply_extend_resultentries) = 2 * (ge_balance_positive_multiply_extend_resultentriesentryleftvalue) /\ (ge_balance_negative_multiply_extend_resultentriesentryleftvalue) = 0) \/ exists ge_signed_half_multiply_extend_resultentriesentryleftvaluedecode. (((sto_left_multiply_extend_resultentries) = 2 * ge_signed_half_multiply_extend_resultentriesentryleftvaluedecode + 1 /\ (ge_balance_positive_multiply_extend_resultentriesentryleftvalue) = 0) /\ (ge_balance_negative_multiply_extend_resultentriesentryleftvalue) = S ge_signed_half_multiply_extend_resultentriesentryleftvaluedecode))) /\ ((dst_positive_multiply_extend_resultentriesentryleft) + ge_balance_negative_multiply_extend_resultentriesentryleftvalue = (dst_negative_multiply_extend_resultentriesentryleft) + ge_balance_positive_multiply_extend_resultentriesentryleftvalue))))))))) /\ (((exists dst_positive_code_multiply_extend_resultentriesentryright dst_positive_scale_multiply_extend_resultentriesentryright dst_negative_code_multiply_extend_resultentriesentryright dst_negative_scale_multiply_extend_resultentriesentryright dst_positive_multiply_extend_resultentriesentryright dst_negative_multiply_extend_resultentriesentryright. (((G) = (((((dst_positive_code_multiply_extend_resultentriesentryright) + (dst_positive_scale_multiply_extend_resultentriesentryright)) * S ((dst_positive_code_multiply_extend_resultentriesentryright) + (dst_positive_scale_multiply_extend_resultentriesentryright)) + ((dst_positive_scale_multiply_extend_resultentriesentryright) + (dst_positive_scale_multiply_extend_resultentriesentryright))) + (((dst_negative_code_multiply_extend_resultentriesentryright) + (dst_negative_scale_multiply_extend_resultentriesentryright)) * S ((dst_negative_code_multiply_extend_resultentriesentryright) + (dst_negative_scale_multiply_extend_resultentriesentryright)) + ((dst_negative_scale_multiply_extend_resultentriesentryright) + (dst_negative_scale_multiply_extend_resultentriesentryright)))) * S ((((dst_positive_code_multiply_extend_resultentriesentryright) + (dst_positive_scale_multiply_extend_resultentriesentryright)) * S ((dst_positive_code_multiply_extend_resultentriesentryright) + (dst_positive_scale_multiply_extend_resultentriesentryright)) + ((dst_positive_scale_multiply_extend_resultentriesentryright) + (dst_positive_scale_multiply_extend_resultentriesentryright))) + (((dst_negative_code_multiply_extend_resultentriesentryright) + (dst_negative_scale_multiply_extend_resultentriesentryright)) * S ((dst_negative_code_multiply_extend_resultentriesentryright) + (dst_negative_scale_multiply_extend_resultentriesentryright)) + ((dst_negative_scale_multiply_extend_resultentriesentryright) + (dst_negative_scale_multiply_extend_resultentriesentryright)))) + ((((dst_negative_code_multiply_extend_resultentriesentryright) + (dst_negative_scale_multiply_extend_resultentriesentryright)) * S ((dst_negative_code_multiply_extend_resultentriesentryright) + (dst_negative_scale_multiply_extend_resultentriesentryright)) + ((dst_negative_scale_multiply_extend_resultentriesentryright) + (dst_negative_scale_multiply_extend_resultentriesentryright))) + (((dst_negative_code_multiply_extend_resultentriesentryright) + (dst_negative_scale_multiply_extend_resultentriesentryright)) * S ((dst_negative_code_multiply_extend_resultentriesentryright) + (dst_negative_scale_multiply_extend_resultentriesentryright)) + ((dst_negative_scale_multiply_extend_resultentriesentryright) + (dst_negative_scale_multiply_extend_resultentriesentryright)))))) /\ (((((exists ff_h_pvs_multiply_extend_resultentriesentryrightpositive. ff_h_pvs_multiply_extend_resultentriesentryrightpositive + S (dst_positive_multiply_extend_resultentriesentryright) = S ((S (sto_index_multiply_extend_resultentries)) * dst_positive_scale_multiply_extend_resultentriesentryright)) /\ exists ff_q_pvs_multiply_extend_resultentriesentryrightpositive. dst_positive_code_multiply_extend_resultentriesentryright = ff_q_pvs_multiply_extend_resultentriesentryrightpositive * S ((S (sto_index_multiply_extend_resultentries)) * dst_positive_scale_multiply_extend_resultentriesentryright) + (dst_positive_multiply_extend_resultentriesentryright))) /\ (((((exists ff_h_pvs_multiply_extend_resultentriesentryrightnegative. ff_h_pvs_multiply_extend_resultentriesentryrightnegative + S (dst_negative_multiply_extend_resultentriesentryright) = S ((S (sto_index_multiply_extend_resultentries)) * dst_negative_scale_multiply_extend_resultentriesentryright)) /\ exists ff_q_pvs_multiply_extend_resultentriesentryrightnegative. dst_negative_code_multiply_extend_resultentriesentryright = ff_q_pvs_multiply_extend_resultentriesentryrightnegative * S ((S (sto_index_multiply_extend_resultentries)) * dst_negative_scale_multiply_extend_resultentriesentryright) + (dst_negative_multiply_extend_resultentriesentryright))) /\ (exists ge_balance_positive_multiply_extend_resultentriesentryrightvalue ge_balance_negative_multiply_extend_resultentriesentryrightvalue. (((((sto_right_multiply_extend_resultentries) = 2 * (ge_balance_positive_multiply_extend_resultentriesentryrightvalue) /\ (ge_balance_negative_multiply_extend_resultentriesentryrightvalue) = 0) \/ exists ge_signed_half_multiply_extend_resultentriesentryrightvaluedecode. (((sto_right_multiply_extend_resultentries) = 2 * ge_signed_half_multiply_extend_resultentriesentryrightvaluedecode + 1 /\ (ge_balance_positive_multiply_extend_resultentriesentryrightvalue) = 0) /\ (ge_balance_negative_multiply_extend_resultentriesentryrightvalue) = S ge_signed_half_multiply_extend_resultentriesentryrightvaluedecode))) /\ ((dst_positive_multiply_extend_resultentriesentryright) + ge_balance_negative_multiply_extend_resultentriesentryrightvalue = (dst_negative_multiply_extend_resultentriesentryright) + ge_balance_positive_multiply_extend_resultentriesentryrightvalue))))))))) /\ (((exists dst_positive_code_multiply_extend_resultentriesentryoutput dst_positive_scale_multiply_extend_resultentriesentryoutput dst_negative_code_multiply_extend_resultentriesentryoutput dst_negative_scale_multiply_extend_resultentriesentryoutput dst_positive_multiply_extend_resultentriesentryoutput dst_negative_multiply_extend_resultentriesentryoutput. (((K) = (((((dst_positive_code_multiply_extend_resultentriesentryoutput) + (dst_positive_scale_multiply_extend_resultentriesentryoutput)) * S ((dst_positive_code_multiply_extend_resultentriesentryoutput) + (dst_positive_scale_multiply_extend_resultentriesentryoutput)) + ((dst_positive_scale_multiply_extend_resultentriesentryoutput) + (dst_positive_scale_multiply_extend_resultentriesentryoutput))) + (((dst_negative_code_multiply_extend_resultentriesentryoutput) + (dst_negative_scale_multiply_extend_resultentriesentryoutput)) * S ((dst_negative_code_multiply_extend_resultentriesentryoutput) + (dst_negative_scale_multiply_extend_resultentriesentryoutput)) + ((dst_negative_scale_multiply_extend_resultentriesentryoutput) + (dst_negative_scale_multiply_extend_resultentriesentryoutput)))) * S ((((dst_positive_code_multiply_extend_resultentriesentryoutput) + (dst_positive_scale_multiply_extend_resultentriesentryoutput)) * S ((dst_positive_code_multiply_extend_resultentriesentryoutput) + (dst_positive_scale_multiply_extend_resultentriesentryoutput)) + ((dst_positive_scale_multiply_extend_resultentriesentryoutput) + (dst_positive_scale_multiply_extend_resultentriesentryoutput))) + (((dst_negative_code_multiply_extend_resultentriesentryoutput) + (dst_negative_scale_multiply_extend_resultentriesentryoutput)) * S ((dst_negative_code_multiply_extend_resultentriesentryoutput) + (dst_negative_scale_multiply_extend_resultentriesentryoutput)) + ((dst_negative_scale_multiply_extend_resultentriesentryoutput) + (dst_negative_scale_multiply_extend_resultentriesentryoutput)))) + ((((dst_negative_code_multiply_extend_resultentriesentryoutput) + (dst_negative_scale_multiply_extend_resultentriesentryoutput)) * S ((dst_negative_code_multiply_extend_resultentriesentryoutput) + (dst_negative_scale_multiply_extend_resultentriesentryoutput)) + ((dst_negative_scale_multiply_extend_resultentriesentryoutput) + (dst_negative_scale_multiply_extend_resultentriesentryoutput))) + (((dst_negative_code_multiply_extend_resultentriesentryoutput) + (dst_negative_scale_multiply_extend_resultentriesentryoutput)) * S ((dst_negative_code_multiply_extend_resultentriesentryoutput) + (dst_negative_scale_multiply_extend_resultentriesentryoutput)) + ((dst_negative_scale_multiply_extend_resultentriesentryoutput) + (dst_negative_scale_multiply_extend_resultentriesentryoutput)))))) /\ (((((exists ff_h_pvs_multiply_extend_resultentriesentryoutputpositive. ff_h_pvs_multiply_extend_resultentriesentryoutputpositive + S (dst_positive_multiply_extend_resultentriesentryoutput) = S ((S (sto_index_multiply_extend_resultentries)) * dst_positive_scale_multiply_extend_resultentriesentryoutput)) /\ exists ff_q_pvs_multiply_extend_resultentriesentryoutputpositive. dst_positive_code_multiply_extend_resultentriesentryoutput = ff_q_pvs_multiply_extend_resultentriesentryoutputpositive * S ((S (sto_index_multiply_extend_resultentries)) * dst_positive_scale_multiply_extend_resultentriesentryoutput) + (dst_positive_multiply_extend_resultentriesentryoutput))) /\ (((((exists ff_h_pvs_multiply_extend_resultentriesentryoutputnegative. ff_h_pvs_multiply_extend_resultentriesentryoutputnegative + S (dst_negative_multiply_extend_resultentriesentryoutput) = S ((S (sto_index_multiply_extend_resultentries)) * dst_negative_scale_multiply_extend_resultentriesentryoutput)) /\ exists ff_q_pvs_multiply_extend_resultentriesentryoutputnegative. dst_negative_code_multiply_extend_resultentriesentryoutput = ff_q_pvs_multiply_extend_resultentriesentryoutputnegative * S ((S (sto_index_multiply_extend_resultentries)) * dst_negative_scale_multiply_extend_resultentriesentryoutput) + (dst_negative_multiply_extend_resultentriesentryoutput))) /\ (exists ge_balance_positive_multiply_extend_resultentriesentryoutputvalue ge_balance_negative_multiply_extend_resultentriesentryoutputvalue. (((((sto_output_multiply_extend_resultentries) = 2 * (ge_balance_positive_multiply_extend_resultentriesentryoutputvalue) /\ (ge_balance_negative_multiply_extend_resultentriesentryoutputvalue) = 0) \/ exists ge_signed_half_multiply_extend_resultentriesentryoutputvaluedecode. (((sto_output_multiply_extend_resultentries) = 2 * ge_signed_half_multiply_extend_resultentriesentryoutputvaluedecode + 1 /\ (ge_balance_positive_multiply_extend_resultentriesentryoutputvalue) = 0) /\ (ge_balance_negative_multiply_extend_resultentriesentryoutputvalue) = S ge_signed_half_multiply_extend_resultentriesentryoutputvaluedecode))) /\ ((dst_positive_multiply_extend_resultentriesentryoutput) + ge_balance_negative_multiply_extend_resultentriesentryoutputvalue = (dst_negative_multiply_extend_resultentriesentryoutput) + ge_balance_positive_multiply_extend_resultentriesentryoutputvalue))))))))) /\ (exists sto_ap_multiply_extend_resultentriesentryoperation sto_an_multiply_extend_resultentriesentryoperation sto_bp_multiply_extend_resultentriesentryoperation sto_bn_multiply_extend_resultentriesentryoperation sto_cp_multiply_extend_resultentriesentryoperation sto_cn_multiply_extend_resultentriesentryoperation. (((((sto_left_multiply_extend_resultentries) = 2 * (sto_ap_multiply_extend_resultentriesentryoperation) /\ (sto_an_multiply_extend_resultentriesentryoperation) = 0) \/ exists ge_signed_half_multiply_extend_resultentriesentryoperationleft. (((sto_left_multiply_extend_resultentries) = 2 * ge_signed_half_multiply_extend_resultentriesentryoperationleft + 1 /\ (sto_ap_multiply_extend_resultentriesentryoperation) = 0) /\ (sto_an_multiply_extend_resultentriesentryoperation) = S ge_signed_half_multiply_extend_resultentriesentryoperationleft))) /\ ((((((sto_right_multiply_extend_resultentries) = 2 * (sto_bp_multiply_extend_resultentriesentryoperation) /\ (sto_bn_multiply_extend_resultentriesentryoperation) = 0) \/ exists ge_signed_half_multiply_extend_resultentriesentryoperationright. (((sto_right_multiply_extend_resultentries) = 2 * ge_signed_half_multiply_extend_resultentriesentryoperationright + 1 /\ (sto_bp_multiply_extend_resultentriesentryoperation) = 0) /\ (sto_bn_multiply_extend_resultentriesentryoperation) = S ge_signed_half_multiply_extend_resultentriesentryoperationright))) /\ ((((((sto_output_multiply_extend_resultentries) = 2 * (sto_cp_multiply_extend_resultentriesentryoperation) /\ (sto_cn_multiply_extend_resultentriesentryoperation) = 0) \/ exists ge_signed_half_multiply_extend_resultentriesentryoperationoutput. (((sto_output_multiply_extend_resultentries) = 2 * ge_signed_half_multiply_extend_resultentriesentryoperationoutput + 1 /\ (sto_cp_multiply_extend_resultentriesentryoperation) = 0) /\ (sto_cn_multiply_extend_resultentriesentryoperation) = S ge_signed_half_multiply_extend_resultentriesentryoperationoutput))) /\ ((sto_ap_multiply_extend_resultentriesentryoperation * sto_bp_multiply_extend_resultentriesentryoperation + sto_an_multiply_extend_resultentriesentryoperation * sto_bn_multiply_extend_resultentriesentryoperation) + sto_cn_multiply_extend_resultentriesentryoperation = (sto_ap_multiply_extend_resultentriesentryoperation * sto_bn_multiply_extend_resultentriesentryoperation + sto_an_multiply_extend_resultentriesentryoperation * sto_bp_multiply_extend_resultentriesentryoperation) + sto_cp_multiply_extend_resultentriesentryoperation)))))))))))))))))))