signed_table_multiply_restrict

forall F G H l. (((exists dst_positive_code_multiply_restrict_inputleft_table dst_positive_scale_multiply_restrict_inputleft_table dst_negative_code_multiply_restrict_inputleft_table dst_negative_scale_multiply_restrict_inputleft_table. (((F) = (((((dst_positive_code_multiply_restrict_inputleft_table) + (dst_positive_scale_multiply_restrict_inputleft_table)) * S ((dst_positive_code_multiply_restrict_inputleft_table) + (dst_positive_scale_multiply_restrict_inputleft_table)) + ((dst_positive_scale_multiply_restrict_inputleft_table) + (dst_positive_scale_multiply_restrict_inputleft_table))) + (((dst_negative_code_multiply_restrict_inputleft_table) + (dst_negative_scale_multiply_restrict_inputleft_table)) * S ((dst_negative_code_multiply_restrict_inputleft_table) + (dst_negative_scale_multiply_restrict_inputleft_table)) + ((dst_negative_scale_multiply_restrict_inputleft_table) + (dst_negative_scale_multiply_restrict_inputleft_table)))) * S ((((dst_positive_code_multiply_restrict_inputleft_table) + (dst_positive_scale_multiply_restrict_inputleft_table)) * S ((dst_positive_code_multiply_restrict_inputleft_table) + (dst_positive_scale_multiply_restrict_inputleft_table)) + ((dst_positive_scale_multiply_restrict_inputleft_table) + (dst_positive_scale_multiply_restrict_inputleft_table))) + (((dst_negative_code_multiply_restrict_inputleft_table) + (dst_negative_scale_multiply_restrict_inputleft_table)) * S ((dst_negative_code_multiply_restrict_inputleft_table) + (dst_negative_scale_multiply_restrict_inputleft_table)) + ((dst_negative_scale_multiply_restrict_inputleft_table) + (dst_negative_scale_multiply_restrict_inputleft_table)))) + ((((dst_negative_code_multiply_restrict_inputleft_table) + (dst_negative_scale_multiply_restrict_inputleft_table)) * S ((dst_negative_code_multiply_restrict_inputleft_table) + (dst_negative_scale_multiply_restrict_inputleft_table)) + ((dst_negative_scale_multiply_restrict_inputleft_table) + (dst_negative_scale_multiply_restrict_inputleft_table))) + (((dst_negative_code_multiply_restrict_inputleft_table) + (dst_negative_scale_multiply_restrict_inputleft_table)) * S ((dst_negative_code_multiply_restrict_inputleft_table) + (dst_negative_scale_multiply_restrict_inputleft_table)) + ((dst_negative_scale_multiply_restrict_inputleft_table) + (dst_negative_scale_multiply_restrict_inputleft_table)))))) /\ (forall dst_index_multiply_restrict_inputleft_table. (exists pvs_le_gap_multiply_restrict_inputleft_tabledomain. pvs_le_gap_multiply_restrict_inputleft_tabledomain + (dst_index_multiply_restrict_inputleft_table) = (S l)) -> exists dst_positive_multiply_restrict_inputleft_table dst_negative_multiply_restrict_inputleft_table dst_value_multiply_restrict_inputleft_table. ((((exists ff_h_pvs_multiply_restrict_inputleft_tableentrypositive. ff_h_pvs_multiply_restrict_inputleft_tableentrypositive + S (dst_positive_multiply_restrict_inputleft_table) = S ((S (dst_index_multiply_restrict_inputleft_table)) * dst_positive_scale_multiply_restrict_inputleft_table)) /\ exists ff_q_pvs_multiply_restrict_inputleft_tableentrypositive. dst_positive_code_multiply_restrict_inputleft_table = ff_q_pvs_multiply_restrict_inputleft_tableentrypositive * S ((S (dst_index_multiply_restrict_inputleft_table)) * dst_positive_scale_multiply_restrict_inputleft_table) + (dst_positive_multiply_restrict_inputleft_table))) /\ (((((exists ff_h_pvs_multiply_restrict_inputleft_tableentrynegative. ff_h_pvs_multiply_restrict_inputleft_tableentrynegative + S (dst_negative_multiply_restrict_inputleft_table) = S ((S (dst_index_multiply_restrict_inputleft_table)) * dst_negative_scale_multiply_restrict_inputleft_table)) /\ exists ff_q_pvs_multiply_restrict_inputleft_tableentrynegative. dst_negative_code_multiply_restrict_inputleft_table = ff_q_pvs_multiply_restrict_inputleft_tableentrynegative * S ((S (dst_index_multiply_restrict_inputleft_table)) * dst_negative_scale_multiply_restrict_inputleft_table) + (dst_negative_multiply_restrict_inputleft_table))) /\ (exists ge_balance_positive_multiply_restrict_inputleft_tableentryvalue ge_balance_negative_multiply_restrict_inputleft_tableentryvalue. (((((dst_value_multiply_restrict_inputleft_table) = 2 * (ge_balance_positive_multiply_restrict_inputleft_tableentryvalue) /\ (ge_balance_negative_multiply_restrict_inputleft_tableentryvalue) = 0) \/ exists ge_signed_half_multiply_restrict_inputleft_tableentryvaluedecode. (((dst_value_multiply_restrict_inputleft_table) = 2 * ge_signed_half_multiply_restrict_inputleft_tableentryvaluedecode + 1 /\ (ge_balance_positive_multiply_restrict_inputleft_tableentryvalue) = 0) /\ (ge_balance_negative_multiply_restrict_inputleft_tableentryvalue) = S ge_signed_half_multiply_restrict_inputleft_tableentryvaluedecode))) /\ ((dst_positive_multiply_restrict_inputleft_table) + ge_balance_negative_multiply_restrict_inputleft_tableentryvalue = (dst_negative_multiply_restrict_inputleft_table) + ge_balance_positive_multiply_restrict_inputleft_tableentryvalue))))))))) /\ (((exists dst_positive_code_multiply_restrict_inputright_table dst_positive_scale_multiply_restrict_inputright_table dst_negative_code_multiply_restrict_inputright_table dst_negative_scale_multiply_restrict_inputright_table. (((G) = (((((dst_positive_code_multiply_restrict_inputright_table) + (dst_positive_scale_multiply_restrict_inputright_table)) * S ((dst_positive_code_multiply_restrict_inputright_table) + (dst_positive_scale_multiply_restrict_inputright_table)) + ((dst_positive_scale_multiply_restrict_inputright_table) + (dst_positive_scale_multiply_restrict_inputright_table))) + (((dst_negative_code_multiply_restrict_inputright_table) + (dst_negative_scale_multiply_restrict_inputright_table)) * S ((dst_negative_code_multiply_restrict_inputright_table) + (dst_negative_scale_multiply_restrict_inputright_table)) + ((dst_negative_scale_multiply_restrict_inputright_table) + (dst_negative_scale_multiply_restrict_inputright_table)))) * S ((((dst_positive_code_multiply_restrict_inputright_table) + (dst_positive_scale_multiply_restrict_inputright_table)) * S ((dst_positive_code_multiply_restrict_inputright_table) + (dst_positive_scale_multiply_restrict_inputright_table)) + ((dst_positive_scale_multiply_restrict_inputright_table) + (dst_positive_scale_multiply_restrict_inputright_table))) + (((dst_negative_code_multiply_restrict_inputright_table) + (dst_negative_scale_multiply_restrict_inputright_table)) * S ((dst_negative_code_multiply_restrict_inputright_table) + (dst_negative_scale_multiply_restrict_inputright_table)) + ((dst_negative_scale_multiply_restrict_inputright_table) + (dst_negative_scale_multiply_restrict_inputright_table)))) + ((((dst_negative_code_multiply_restrict_inputright_table) + (dst_negative_scale_multiply_restrict_inputright_table)) * S ((dst_negative_code_multiply_restrict_inputright_table) + (dst_negative_scale_multiply_restrict_inputright_table)) + ((dst_negative_scale_multiply_restrict_inputright_table) + (dst_negative_scale_multiply_restrict_inputright_table))) + (((dst_negative_code_multiply_restrict_inputright_table) + (dst_negative_scale_multiply_restrict_inputright_table)) * S ((dst_negative_code_multiply_restrict_inputright_table) + (dst_negative_scale_multiply_restrict_inputright_table)) + ((dst_negative_scale_multiply_restrict_inputright_table) + (dst_negative_scale_multiply_restrict_inputright_table)))))) /\ (forall dst_index_multiply_restrict_inputright_table. (exists pvs_le_gap_multiply_restrict_inputright_tabledomain. pvs_le_gap_multiply_restrict_inputright_tabledomain + (dst_index_multiply_restrict_inputright_table) = (S l)) -> exists dst_positive_multiply_restrict_inputright_table dst_negative_multiply_restrict_inputright_table dst_value_multiply_restrict_inputright_table. ((((exists ff_h_pvs_multiply_restrict_inputright_tableentrypositive. ff_h_pvs_multiply_restrict_inputright_tableentrypositive + S (dst_positive_multiply_restrict_inputright_table) = S ((S (dst_index_multiply_restrict_inputright_table)) * dst_positive_scale_multiply_restrict_inputright_table)) /\ exists ff_q_pvs_multiply_restrict_inputright_tableentrypositive. dst_positive_code_multiply_restrict_inputright_table = ff_q_pvs_multiply_restrict_inputright_tableentrypositive * S ((S (dst_index_multiply_restrict_inputright_table)) * dst_positive_scale_multiply_restrict_inputright_table) + (dst_positive_multiply_restrict_inputright_table))) /\ (((((exists ff_h_pvs_multiply_restrict_inputright_tableentrynegative. ff_h_pvs_multiply_restrict_inputright_tableentrynegative + S (dst_negative_multiply_restrict_inputright_table) = S ((S (dst_index_multiply_restrict_inputright_table)) * dst_negative_scale_multiply_restrict_inputright_table)) /\ exists ff_q_pvs_multiply_restrict_inputright_tableentrynegative. dst_negative_code_multiply_restrict_inputright_table = ff_q_pvs_multiply_restrict_inputright_tableentrynegative * S ((S (dst_index_multiply_restrict_inputright_table)) * dst_negative_scale_multiply_restrict_inputright_table) + (dst_negative_multiply_restrict_inputright_table))) /\ (exists ge_balance_positive_multiply_restrict_inputright_tableentryvalue ge_balance_negative_multiply_restrict_inputright_tableentryvalue. (((((dst_value_multiply_restrict_inputright_table) = 2 * (ge_balance_positive_multiply_restrict_inputright_tableentryvalue) /\ (ge_balance_negative_multiply_restrict_inputright_tableentryvalue) = 0) \/ exists ge_signed_half_multiply_restrict_inputright_tableentryvaluedecode. (((dst_value_multiply_restrict_inputright_table) = 2 * ge_signed_half_multiply_restrict_inputright_tableentryvaluedecode + 1 /\ (ge_balance_positive_multiply_restrict_inputright_tableentryvalue) = 0) /\ (ge_balance_negative_multiply_restrict_inputright_tableentryvalue) = S ge_signed_half_multiply_restrict_inputright_tableentryvaluedecode))) /\ ((dst_positive_multiply_restrict_inputright_table) + ge_balance_negative_multiply_restrict_inputright_tableentryvalue = (dst_negative_multiply_restrict_inputright_table) + ge_balance_positive_multiply_restrict_inputright_tableentryvalue))))))))) /\ (((exists dst_positive_code_multiply_restrict_inputoutput_table dst_positive_scale_multiply_restrict_inputoutput_table dst_negative_code_multiply_restrict_inputoutput_table dst_negative_scale_multiply_restrict_inputoutput_table. (((H) = (((((dst_positive_code_multiply_restrict_inputoutput_table) + (dst_positive_scale_multiply_restrict_inputoutput_table)) * S ((dst_positive_code_multiply_restrict_inputoutput_table) + (dst_positive_scale_multiply_restrict_inputoutput_table)) + ((dst_positive_scale_multiply_restrict_inputoutput_table) + (dst_positive_scale_multiply_restrict_inputoutput_table))) + (((dst_negative_code_multiply_restrict_inputoutput_table) + (dst_negative_scale_multiply_restrict_inputoutput_table)) * S ((dst_negative_code_multiply_restrict_inputoutput_table) + (dst_negative_scale_multiply_restrict_inputoutput_table)) + ((dst_negative_scale_multiply_restrict_inputoutput_table) + (dst_negative_scale_multiply_restrict_inputoutput_table)))) * S ((((dst_positive_code_multiply_restrict_inputoutput_table) + (dst_positive_scale_multiply_restrict_inputoutput_table)) * S ((dst_positive_code_multiply_restrict_inputoutput_table) + (dst_positive_scale_multiply_restrict_inputoutput_table)) + ((dst_positive_scale_multiply_restrict_inputoutput_table) + (dst_positive_scale_multiply_restrict_inputoutput_table))) + (((dst_negative_code_multiply_restrict_inputoutput_table) + (dst_negative_scale_multiply_restrict_inputoutput_table)) * S ((dst_negative_code_multiply_restrict_inputoutput_table) + (dst_negative_scale_multiply_restrict_inputoutput_table)) + ((dst_negative_scale_multiply_restrict_inputoutput_table) + (dst_negative_scale_multiply_restrict_inputoutput_table)))) + ((((dst_negative_code_multiply_restrict_inputoutput_table) + (dst_negative_scale_multiply_restrict_inputoutput_table)) * S ((dst_negative_code_multiply_restrict_inputoutput_table) + (dst_negative_scale_multiply_restrict_inputoutput_table)) + ((dst_negative_scale_multiply_restrict_inputoutput_table) + (dst_negative_scale_multiply_restrict_inputoutput_table))) + (((dst_negative_code_multiply_restrict_inputoutput_table) + (dst_negative_scale_multiply_restrict_inputoutput_table)) * S ((dst_negative_code_multiply_restrict_inputoutput_table) + (dst_negative_scale_multiply_restrict_inputoutput_table)) + ((dst_negative_scale_multiply_restrict_inputoutput_table) + (dst_negative_scale_multiply_restrict_inputoutput_table)))))) /\ (forall dst_index_multiply_restrict_inputoutput_table. (exists pvs_le_gap_multiply_restrict_inputoutput_tabledomain. pvs_le_gap_multiply_restrict_inputoutput_tabledomain + (dst_index_multiply_restrict_inputoutput_table) = (S l)) -> exists dst_positive_multiply_restrict_inputoutput_table dst_negative_multiply_restrict_inputoutput_table dst_value_multiply_restrict_inputoutput_table. ((((exists ff_h_pvs_multiply_restrict_inputoutput_tableentrypositive. ff_h_pvs_multiply_restrict_inputoutput_tableentrypositive + S (dst_positive_multiply_restrict_inputoutput_table) = S ((S (dst_index_multiply_restrict_inputoutput_table)) * dst_positive_scale_multiply_restrict_inputoutput_table)) /\ exists ff_q_pvs_multiply_restrict_inputoutput_tableentrypositive. dst_positive_code_multiply_restrict_inputoutput_table = ff_q_pvs_multiply_restrict_inputoutput_tableentrypositive * S ((S (dst_index_multiply_restrict_inputoutput_table)) * dst_positive_scale_multiply_restrict_inputoutput_table) + (dst_positive_multiply_restrict_inputoutput_table))) /\ (((((exists ff_h_pvs_multiply_restrict_inputoutput_tableentrynegative. ff_h_pvs_multiply_restrict_inputoutput_tableentrynegative + S (dst_negative_multiply_restrict_inputoutput_table) = S ((S (dst_index_multiply_restrict_inputoutput_table)) * dst_negative_scale_multiply_restrict_inputoutput_table)) /\ exists ff_q_pvs_multiply_restrict_inputoutput_tableentrynegative. dst_negative_code_multiply_restrict_inputoutput_table = ff_q_pvs_multiply_restrict_inputoutput_tableentrynegative * S ((S (dst_index_multiply_restrict_inputoutput_table)) * dst_negative_scale_multiply_restrict_inputoutput_table) + (dst_negative_multiply_restrict_inputoutput_table))) /\ (exists ge_balance_positive_multiply_restrict_inputoutput_tableentryvalue ge_balance_negative_multiply_restrict_inputoutput_tableentryvalue. (((((dst_value_multiply_restrict_inputoutput_table) = 2 * (ge_balance_positive_multiply_restrict_inputoutput_tableentryvalue) /\ (ge_balance_negative_multiply_restrict_inputoutput_tableentryvalue) = 0) \/ exists ge_signed_half_multiply_restrict_inputoutput_tableentryvaluedecode. (((dst_value_multiply_restrict_inputoutput_table) = 2 * ge_signed_half_multiply_restrict_inputoutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_multiply_restrict_inputoutput_tableentryvalue) = 0) /\ (ge_balance_negative_multiply_restrict_inputoutput_tableentryvalue) = S ge_signed_half_multiply_restrict_inputoutput_tableentryvaluedecode))) /\ ((dst_positive_multiply_restrict_inputoutput_table) + ge_balance_negative_multiply_restrict_inputoutput_tableentryvalue = (dst_negative_multiply_restrict_inputoutput_table) + ge_balance_positive_multiply_restrict_inputoutput_tableentryvalue))))))))) /\ (forall sto_index_multiply_restrict_inputentries. (exists pvs_gap_multiply_restrict_inputentriesbound. pvs_gap_multiply_restrict_inputentriesbound + S (sto_index_multiply_restrict_inputentries) = (S l)) -> exists sto_left_multiply_restrict_inputentries sto_right_multiply_restrict_inputentries sto_output_multiply_restrict_inputentries. ((exists dst_positive_code_multiply_restrict_inputentriesentryleft dst_positive_scale_multiply_restrict_inputentriesentryleft dst_negative_code_multiply_restrict_inputentriesentryleft dst_negative_scale_multiply_restrict_inputentriesentryleft dst_positive_multiply_restrict_inputentriesentryleft dst_negative_multiply_restrict_inputentriesentryleft. (((F) = (((((dst_positive_code_multiply_restrict_inputentriesentryleft) + (dst_positive_scale_multiply_restrict_inputentriesentryleft)) * S ((dst_positive_code_multiply_restrict_inputentriesentryleft) + (dst_positive_scale_multiply_restrict_inputentriesentryleft)) + ((dst_positive_scale_multiply_restrict_inputentriesentryleft) + (dst_positive_scale_multiply_restrict_inputentriesentryleft))) + (((dst_negative_code_multiply_restrict_inputentriesentryleft) + (dst_negative_scale_multiply_restrict_inputentriesentryleft)) * S ((dst_negative_code_multiply_restrict_inputentriesentryleft) + (dst_negative_scale_multiply_restrict_inputentriesentryleft)) + ((dst_negative_scale_multiply_restrict_inputentriesentryleft) + (dst_negative_scale_multiply_restrict_inputentriesentryleft)))) * S ((((dst_positive_code_multiply_restrict_inputentriesentryleft) + (dst_positive_scale_multiply_restrict_inputentriesentryleft)) * S ((dst_positive_code_multiply_restrict_inputentriesentryleft) + (dst_positive_scale_multiply_restrict_inputentriesentryleft)) + ((dst_positive_scale_multiply_restrict_inputentriesentryleft) + (dst_positive_scale_multiply_restrict_inputentriesentryleft))) + (((dst_negative_code_multiply_restrict_inputentriesentryleft) + (dst_negative_scale_multiply_restrict_inputentriesentryleft)) * S ((dst_negative_code_multiply_restrict_inputentriesentryleft) + (dst_negative_scale_multiply_restrict_inputentriesentryleft)) + ((dst_negative_scale_multiply_restrict_inputentriesentryleft) + (dst_negative_scale_multiply_restrict_inputentriesentryleft)))) + ((((dst_negative_code_multiply_restrict_inputentriesentryleft) + (dst_negative_scale_multiply_restrict_inputentriesentryleft)) * S ((dst_negative_code_multiply_restrict_inputentriesentryleft) + (dst_negative_scale_multiply_restrict_inputentriesentryleft)) + ((dst_negative_scale_multiply_restrict_inputentriesentryleft) + (dst_negative_scale_multiply_restrict_inputentriesentryleft))) + (((dst_negative_code_multiply_restrict_inputentriesentryleft) + (dst_negative_scale_multiply_restrict_inputentriesentryleft)) * S ((dst_negative_code_multiply_restrict_inputentriesentryleft) + (dst_negative_scale_multiply_restrict_inputentriesentryleft)) + ((dst_negative_scale_multiply_restrict_inputentriesentryleft) + (dst_negative_scale_multiply_restrict_inputentriesentryleft)))))) /\ (((((exists ff_h_pvs_multiply_restrict_inputentriesentryleftpositive. ff_h_pvs_multiply_restrict_inputentriesentryleftpositive + S (dst_positive_multiply_restrict_inputentriesentryleft) = S ((S (sto_index_multiply_restrict_inputentries)) * dst_positive_scale_multiply_restrict_inputentriesentryleft)) /\ exists ff_q_pvs_multiply_restrict_inputentriesentryleftpositive. dst_positive_code_multiply_restrict_inputentriesentryleft = ff_q_pvs_multiply_restrict_inputentriesentryleftpositive * S ((S (sto_index_multiply_restrict_inputentries)) * dst_positive_scale_multiply_restrict_inputentriesentryleft) + (dst_positive_multiply_restrict_inputentriesentryleft))) /\ (((((exists ff_h_pvs_multiply_restrict_inputentriesentryleftnegative. ff_h_pvs_multiply_restrict_inputentriesentryleftnegative + S (dst_negative_multiply_restrict_inputentriesentryleft) = S ((S (sto_index_multiply_restrict_inputentries)) * dst_negative_scale_multiply_restrict_inputentriesentryleft)) /\ exists ff_q_pvs_multiply_restrict_inputentriesentryleftnegative. dst_negative_code_multiply_restrict_inputentriesentryleft = ff_q_pvs_multiply_restrict_inputentriesentryleftnegative * S ((S (sto_index_multiply_restrict_inputentries)) * dst_negative_scale_multiply_restrict_inputentriesentryleft) + (dst_negative_multiply_restrict_inputentriesentryleft))) /\ (exists ge_balance_positive_multiply_restrict_inputentriesentryleftvalue ge_balance_negative_multiply_restrict_inputentriesentryleftvalue. (((((sto_left_multiply_restrict_inputentries) = 2 * (ge_balance_positive_multiply_restrict_inputentriesentryleftvalue) /\ (ge_balance_negative_multiply_restrict_inputentriesentryleftvalue) = 0) \/ exists ge_signed_half_multiply_restrict_inputentriesentryleftvaluedecode. (((sto_left_multiply_restrict_inputentries) = 2 * ge_signed_half_multiply_restrict_inputentriesentryleftvaluedecode + 1 /\ (ge_balance_positive_multiply_restrict_inputentriesentryleftvalue) = 0) /\ (ge_balance_negative_multiply_restrict_inputentriesentryleftvalue) = S ge_signed_half_multiply_restrict_inputentriesentryleftvaluedecode))) /\ ((dst_positive_multiply_restrict_inputentriesentryleft) + ge_balance_negative_multiply_restrict_inputentriesentryleftvalue = (dst_negative_multiply_restrict_inputentriesentryleft) + ge_balance_positive_multiply_restrict_inputentriesentryleftvalue))))))))) /\ (((exists dst_positive_code_multiply_restrict_inputentriesentryright dst_positive_scale_multiply_restrict_inputentriesentryright dst_negative_code_multiply_restrict_inputentriesentryright dst_negative_scale_multiply_restrict_inputentriesentryright dst_positive_multiply_restrict_inputentriesentryright dst_negative_multiply_restrict_inputentriesentryright. (((G) = (((((dst_positive_code_multiply_restrict_inputentriesentryright) + (dst_positive_scale_multiply_restrict_inputentriesentryright)) * S ((dst_positive_code_multiply_restrict_inputentriesentryright) + (dst_positive_scale_multiply_restrict_inputentriesentryright)) + ((dst_positive_scale_multiply_restrict_inputentriesentryright) + (dst_positive_scale_multiply_restrict_inputentriesentryright))) + (((dst_negative_code_multiply_restrict_inputentriesentryright) + (dst_negative_scale_multiply_restrict_inputentriesentryright)) * S ((dst_negative_code_multiply_restrict_inputentriesentryright) + (dst_negative_scale_multiply_restrict_inputentriesentryright)) + ((dst_negative_scale_multiply_restrict_inputentriesentryright) + (dst_negative_scale_multiply_restrict_inputentriesentryright)))) * S ((((dst_positive_code_multiply_restrict_inputentriesentryright) + (dst_positive_scale_multiply_restrict_inputentriesentryright)) * S ((dst_positive_code_multiply_restrict_inputentriesentryright) + (dst_positive_scale_multiply_restrict_inputentriesentryright)) + ((dst_positive_scale_multiply_restrict_inputentriesentryright) + (dst_positive_scale_multiply_restrict_inputentriesentryright))) + (((dst_negative_code_multiply_restrict_inputentriesentryright) + (dst_negative_scale_multiply_restrict_inputentriesentryright)) * S ((dst_negative_code_multiply_restrict_inputentriesentryright) + (dst_negative_scale_multiply_restrict_inputentriesentryright)) + ((dst_negative_scale_multiply_restrict_inputentriesentryright) + (dst_negative_scale_multiply_restrict_inputentriesentryright)))) + ((((dst_negative_code_multiply_restrict_inputentriesentryright) + (dst_negative_scale_multiply_restrict_inputentriesentryright)) * S ((dst_negative_code_multiply_restrict_inputentriesentryright) + (dst_negative_scale_multiply_restrict_inputentriesentryright)) + ((dst_negative_scale_multiply_restrict_inputentriesentryright) + (dst_negative_scale_multiply_restrict_inputentriesentryright))) + (((dst_negative_code_multiply_restrict_inputentriesentryright) + (dst_negative_scale_multiply_restrict_inputentriesentryright)) * S ((dst_negative_code_multiply_restrict_inputentriesentryright) + (dst_negative_scale_multiply_restrict_inputentriesentryright)) + ((dst_negative_scale_multiply_restrict_inputentriesentryright) + (dst_negative_scale_multiply_restrict_inputentriesentryright)))))) /\ (((((exists ff_h_pvs_multiply_restrict_inputentriesentryrightpositive. ff_h_pvs_multiply_restrict_inputentriesentryrightpositive + S (dst_positive_multiply_restrict_inputentriesentryright) = S ((S (sto_index_multiply_restrict_inputentries)) * dst_positive_scale_multiply_restrict_inputentriesentryright)) /\ exists ff_q_pvs_multiply_restrict_inputentriesentryrightpositive. dst_positive_code_multiply_restrict_inputentriesentryright = ff_q_pvs_multiply_restrict_inputentriesentryrightpositive * S ((S (sto_index_multiply_restrict_inputentries)) * dst_positive_scale_multiply_restrict_inputentriesentryright) + (dst_positive_multiply_restrict_inputentriesentryright))) /\ (((((exists ff_h_pvs_multiply_restrict_inputentriesentryrightnegative. ff_h_pvs_multiply_restrict_inputentriesentryrightnegative + S (dst_negative_multiply_restrict_inputentriesentryright) = S ((S (sto_index_multiply_restrict_inputentries)) * dst_negative_scale_multiply_restrict_inputentriesentryright)) /\ exists ff_q_pvs_multiply_restrict_inputentriesentryrightnegative. dst_negative_code_multiply_restrict_inputentriesentryright = ff_q_pvs_multiply_restrict_inputentriesentryrightnegative * S ((S (sto_index_multiply_restrict_inputentries)) * dst_negative_scale_multiply_restrict_inputentriesentryright) + (dst_negative_multiply_restrict_inputentriesentryright))) /\ (exists ge_balance_positive_multiply_restrict_inputentriesentryrightvalue ge_balance_negative_multiply_restrict_inputentriesentryrightvalue. (((((sto_right_multiply_restrict_inputentries) = 2 * (ge_balance_positive_multiply_restrict_inputentriesentryrightvalue) /\ (ge_balance_negative_multiply_restrict_inputentriesentryrightvalue) = 0) \/ exists ge_signed_half_multiply_restrict_inputentriesentryrightvaluedecode. (((sto_right_multiply_restrict_inputentries) = 2 * ge_signed_half_multiply_restrict_inputentriesentryrightvaluedecode + 1 /\ (ge_balance_positive_multiply_restrict_inputentriesentryrightvalue) = 0) /\ (ge_balance_negative_multiply_restrict_inputentriesentryrightvalue) = S ge_signed_half_multiply_restrict_inputentriesentryrightvaluedecode))) /\ ((dst_positive_multiply_restrict_inputentriesentryright) + ge_balance_negative_multiply_restrict_inputentriesentryrightvalue = (dst_negative_multiply_restrict_inputentriesentryright) + ge_balance_positive_multiply_restrict_inputentriesentryrightvalue))))))))) /\ (((exists dst_positive_code_multiply_restrict_inputentriesentryoutput dst_positive_scale_multiply_restrict_inputentriesentryoutput dst_negative_code_multiply_restrict_inputentriesentryoutput dst_negative_scale_multiply_restrict_inputentriesentryoutput dst_positive_multiply_restrict_inputentriesentryoutput dst_negative_multiply_restrict_inputentriesentryoutput. (((H) = (((((dst_positive_code_multiply_restrict_inputentriesentryoutput) + (dst_positive_scale_multiply_restrict_inputentriesentryoutput)) * S ((dst_positive_code_multiply_restrict_inputentriesentryoutput) + (dst_positive_scale_multiply_restrict_inputentriesentryoutput)) + ((dst_positive_scale_multiply_restrict_inputentriesentryoutput) + (dst_positive_scale_multiply_restrict_inputentriesentryoutput))) + (((dst_negative_code_multiply_restrict_inputentriesentryoutput) + (dst_negative_scale_multiply_restrict_inputentriesentryoutput)) * S ((dst_negative_code_multiply_restrict_inputentriesentryoutput) + (dst_negative_scale_multiply_restrict_inputentriesentryoutput)) + ((dst_negative_scale_multiply_restrict_inputentriesentryoutput) + (dst_negative_scale_multiply_restrict_inputentriesentryoutput)))) * S ((((dst_positive_code_multiply_restrict_inputentriesentryoutput) + (dst_positive_scale_multiply_restrict_inputentriesentryoutput)) * S ((dst_positive_code_multiply_restrict_inputentriesentryoutput) + (dst_positive_scale_multiply_restrict_inputentriesentryoutput)) + ((dst_positive_scale_multiply_restrict_inputentriesentryoutput) + (dst_positive_scale_multiply_restrict_inputentriesentryoutput))) + (((dst_negative_code_multiply_restrict_inputentriesentryoutput) + (dst_negative_scale_multiply_restrict_inputentriesentryoutput)) * S ((dst_negative_code_multiply_restrict_inputentriesentryoutput) + (dst_negative_scale_multiply_restrict_inputentriesentryoutput)) + ((dst_negative_scale_multiply_restrict_inputentriesentryoutput) + (dst_negative_scale_multiply_restrict_inputentriesentryoutput)))) + ((((dst_negative_code_multiply_restrict_inputentriesentryoutput) + (dst_negative_scale_multiply_restrict_inputentriesentryoutput)) * S ((dst_negative_code_multiply_restrict_inputentriesentryoutput) + (dst_negative_scale_multiply_restrict_inputentriesentryoutput)) + ((dst_negative_scale_multiply_restrict_inputentriesentryoutput) + (dst_negative_scale_multiply_restrict_inputentriesentryoutput))) + (((dst_negative_code_multiply_restrict_inputentriesentryoutput) + (dst_negative_scale_multiply_restrict_inputentriesentryoutput)) * S ((dst_negative_code_multiply_restrict_inputentriesentryoutput) + (dst_negative_scale_multiply_restrict_inputentriesentryoutput)) + ((dst_negative_scale_multiply_restrict_inputentriesentryoutput) + (dst_negative_scale_multiply_restrict_inputentriesentryoutput)))))) /\ (((((exists ff_h_pvs_multiply_restrict_inputentriesentryoutputpositive. ff_h_pvs_multiply_restrict_inputentriesentryoutputpositive + S (dst_positive_multiply_restrict_inputentriesentryoutput) = S ((S (sto_index_multiply_restrict_inputentries)) * dst_positive_scale_multiply_restrict_inputentriesentryoutput)) /\ exists ff_q_pvs_multiply_restrict_inputentriesentryoutputpositive. dst_positive_code_multiply_restrict_inputentriesentryoutput = ff_q_pvs_multiply_restrict_inputentriesentryoutputpositive * S ((S (sto_index_multiply_restrict_inputentries)) * dst_positive_scale_multiply_restrict_inputentriesentryoutput) + (dst_positive_multiply_restrict_inputentriesentryoutput))) /\ (((((exists ff_h_pvs_multiply_restrict_inputentriesentryoutputnegative. ff_h_pvs_multiply_restrict_inputentriesentryoutputnegative + S (dst_negative_multiply_restrict_inputentriesentryoutput) = S ((S (sto_index_multiply_restrict_inputentries)) * dst_negative_scale_multiply_restrict_inputentriesentryoutput)) /\ exists ff_q_pvs_multiply_restrict_inputentriesentryoutputnegative. dst_negative_code_multiply_restrict_inputentriesentryoutput = ff_q_pvs_multiply_restrict_inputentriesentryoutputnegative * S ((S (sto_index_multiply_restrict_inputentries)) * dst_negative_scale_multiply_restrict_inputentriesentryoutput) + (dst_negative_multiply_restrict_inputentriesentryoutput))) /\ (exists ge_balance_positive_multiply_restrict_inputentriesentryoutputvalue ge_balance_negative_multiply_restrict_inputentriesentryoutputvalue. (((((sto_output_multiply_restrict_inputentries) = 2 * (ge_balance_positive_multiply_restrict_inputentriesentryoutputvalue) /\ (ge_balance_negative_multiply_restrict_inputentriesentryoutputvalue) = 0) \/ exists ge_signed_half_multiply_restrict_inputentriesentryoutputvaluedecode. (((sto_output_multiply_restrict_inputentries) = 2 * ge_signed_half_multiply_restrict_inputentriesentryoutputvaluedecode + 1 /\ (ge_balance_positive_multiply_restrict_inputentriesentryoutputvalue) = 0) /\ (ge_balance_negative_multiply_restrict_inputentriesentryoutputvalue) = S ge_signed_half_multiply_restrict_inputentriesentryoutputvaluedecode))) /\ ((dst_positive_multiply_restrict_inputentriesentryoutput) + ge_balance_negative_multiply_restrict_inputentriesentryoutputvalue = (dst_negative_multiply_restrict_inputentriesentryoutput) + ge_balance_positive_multiply_restrict_inputentriesentryoutputvalue))))))))) /\ (exists sto_ap_multiply_restrict_inputentriesentryoperation sto_an_multiply_restrict_inputentriesentryoperation sto_bp_multiply_restrict_inputentriesentryoperation sto_bn_multiply_restrict_inputentriesentryoperation sto_cp_multiply_restrict_inputentriesentryoperation sto_cn_multiply_restrict_inputentriesentryoperation. (((((sto_left_multiply_restrict_inputentries) = 2 * (sto_ap_multiply_restrict_inputentriesentryoperation) /\ (sto_an_multiply_restrict_inputentriesentryoperation) = 0) \/ exists ge_signed_half_multiply_restrict_inputentriesentryoperationleft. (((sto_left_multiply_restrict_inputentries) = 2 * ge_signed_half_multiply_restrict_inputentriesentryoperationleft + 1 /\ (sto_ap_multiply_restrict_inputentriesentryoperation) = 0) /\ (sto_an_multiply_restrict_inputentriesentryoperation) = S ge_signed_half_multiply_restrict_inputentriesentryoperationleft))) /\ ((((((sto_right_multiply_restrict_inputentries) = 2 * (sto_bp_multiply_restrict_inputentriesentryoperation) /\ (sto_bn_multiply_restrict_inputentriesentryoperation) = 0) \/ exists ge_signed_half_multiply_restrict_inputentriesentryoperationright. (((sto_right_multiply_restrict_inputentries) = 2 * ge_signed_half_multiply_restrict_inputentriesentryoperationright + 1 /\ (sto_bp_multiply_restrict_inputentriesentryoperation) = 0) /\ (sto_bn_multiply_restrict_inputentriesentryoperation) = S ge_signed_half_multiply_restrict_inputentriesentryoperationright))) /\ ((((((sto_output_multiply_restrict_inputentries) = 2 * (sto_cp_multiply_restrict_inputentriesentryoperation) /\ (sto_cn_multiply_restrict_inputentriesentryoperation) = 0) \/ exists ge_signed_half_multiply_restrict_inputentriesentryoperationoutput. (((sto_output_multiply_restrict_inputentries) = 2 * ge_signed_half_multiply_restrict_inputentriesentryoperationoutput + 1 /\ (sto_cp_multiply_restrict_inputentriesentryoperation) = 0) /\ (sto_cn_multiply_restrict_inputentriesentryoperation) = S ge_signed_half_multiply_restrict_inputentriesentryoperationoutput))) /\ ((sto_ap_multiply_restrict_inputentriesentryoperation * sto_bp_multiply_restrict_inputentriesentryoperation + sto_an_multiply_restrict_inputentriesentryoperation * sto_bn_multiply_restrict_inputentriesentryoperation) + sto_cn_multiply_restrict_inputentriesentryoperation = (sto_ap_multiply_restrict_inputentriesentryoperation * sto_bn_multiply_restrict_inputentriesentryoperation + sto_an_multiply_restrict_inputentriesentryoperation * sto_bp_multiply_restrict_inputentriesentryoperation) + sto_cp_multiply_restrict_inputentriesentryoperation))))))))))))))))))) -> (((exists dst_positive_code_multiply_restrict_outputleft_table dst_positive_scale_multiply_restrict_outputleft_table dst_negative_code_multiply_restrict_outputleft_table dst_negative_scale_multiply_restrict_outputleft_table. (((F) = (((((dst_positive_code_multiply_restrict_outputleft_table) + (dst_positive_scale_multiply_restrict_outputleft_table)) * S ((dst_positive_code_multiply_restrict_outputleft_table) + (dst_positive_scale_multiply_restrict_outputleft_table)) + ((dst_positive_scale_multiply_restrict_outputleft_table) + (dst_positive_scale_multiply_restrict_outputleft_table))) + (((dst_negative_code_multiply_restrict_outputleft_table) + (dst_negative_scale_multiply_restrict_outputleft_table)) * S ((dst_negative_code_multiply_restrict_outputleft_table) + (dst_negative_scale_multiply_restrict_outputleft_table)) + ((dst_negative_scale_multiply_restrict_outputleft_table) + (dst_negative_scale_multiply_restrict_outputleft_table)))) * S ((((dst_positive_code_multiply_restrict_outputleft_table) + (dst_positive_scale_multiply_restrict_outputleft_table)) * S ((dst_positive_code_multiply_restrict_outputleft_table) + (dst_positive_scale_multiply_restrict_outputleft_table)) + ((dst_positive_scale_multiply_restrict_outputleft_table) + (dst_positive_scale_multiply_restrict_outputleft_table))) + (((dst_negative_code_multiply_restrict_outputleft_table) + (dst_negative_scale_multiply_restrict_outputleft_table)) * S ((dst_negative_code_multiply_restrict_outputleft_table) + (dst_negative_scale_multiply_restrict_outputleft_table)) + ((dst_negative_scale_multiply_restrict_outputleft_table) + (dst_negative_scale_multiply_restrict_outputleft_table)))) + ((((dst_negative_code_multiply_restrict_outputleft_table) + (dst_negative_scale_multiply_restrict_outputleft_table)) * S ((dst_negative_code_multiply_restrict_outputleft_table) + (dst_negative_scale_multiply_restrict_outputleft_table)) + ((dst_negative_scale_multiply_restrict_outputleft_table) + (dst_negative_scale_multiply_restrict_outputleft_table))) + (((dst_negative_code_multiply_restrict_outputleft_table) + (dst_negative_scale_multiply_restrict_outputleft_table)) * S ((dst_negative_code_multiply_restrict_outputleft_table) + (dst_negative_scale_multiply_restrict_outputleft_table)) + ((dst_negative_scale_multiply_restrict_outputleft_table) + (dst_negative_scale_multiply_restrict_outputleft_table)))))) /\ (forall dst_index_multiply_restrict_outputleft_table. (exists pvs_le_gap_multiply_restrict_outputleft_tabledomain. pvs_le_gap_multiply_restrict_outputleft_tabledomain + (dst_index_multiply_restrict_outputleft_table) = (l)) -> exists dst_positive_multiply_restrict_outputleft_table dst_negative_multiply_restrict_outputleft_table dst_value_multiply_restrict_outputleft_table. ((((exists ff_h_pvs_multiply_restrict_outputleft_tableentrypositive. ff_h_pvs_multiply_restrict_outputleft_tableentrypositive + S (dst_positive_multiply_restrict_outputleft_table) = S ((S (dst_index_multiply_restrict_outputleft_table)) * dst_positive_scale_multiply_restrict_outputleft_table)) /\ exists ff_q_pvs_multiply_restrict_outputleft_tableentrypositive. dst_positive_code_multiply_restrict_outputleft_table = ff_q_pvs_multiply_restrict_outputleft_tableentrypositive * S ((S (dst_index_multiply_restrict_outputleft_table)) * dst_positive_scale_multiply_restrict_outputleft_table) + (dst_positive_multiply_restrict_outputleft_table))) /\ (((((exists ff_h_pvs_multiply_restrict_outputleft_tableentrynegative. ff_h_pvs_multiply_restrict_outputleft_tableentrynegative + S (dst_negative_multiply_restrict_outputleft_table) = S ((S (dst_index_multiply_restrict_outputleft_table)) * dst_negative_scale_multiply_restrict_outputleft_table)) /\ exists ff_q_pvs_multiply_restrict_outputleft_tableentrynegative. dst_negative_code_multiply_restrict_outputleft_table = ff_q_pvs_multiply_restrict_outputleft_tableentrynegative * S ((S (dst_index_multiply_restrict_outputleft_table)) * dst_negative_scale_multiply_restrict_outputleft_table) + (dst_negative_multiply_restrict_outputleft_table))) /\ (exists ge_balance_positive_multiply_restrict_outputleft_tableentryvalue ge_balance_negative_multiply_restrict_outputleft_tableentryvalue. (((((dst_value_multiply_restrict_outputleft_table) = 2 * (ge_balance_positive_multiply_restrict_outputleft_tableentryvalue) /\ (ge_balance_negative_multiply_restrict_outputleft_tableentryvalue) = 0) \/ exists ge_signed_half_multiply_restrict_outputleft_tableentryvaluedecode. (((dst_value_multiply_restrict_outputleft_table) = 2 * ge_signed_half_multiply_restrict_outputleft_tableentryvaluedecode + 1 /\ (ge_balance_positive_multiply_restrict_outputleft_tableentryvalue) = 0) /\ (ge_balance_negative_multiply_restrict_outputleft_tableentryvalue) = S ge_signed_half_multiply_restrict_outputleft_tableentryvaluedecode))) /\ ((dst_positive_multiply_restrict_outputleft_table) + ge_balance_negative_multiply_restrict_outputleft_tableentryvalue = (dst_negative_multiply_restrict_outputleft_table) + ge_balance_positive_multiply_restrict_outputleft_tableentryvalue))))))))) /\ (((exists dst_positive_code_multiply_restrict_outputright_table dst_positive_scale_multiply_restrict_outputright_table dst_negative_code_multiply_restrict_outputright_table dst_negative_scale_multiply_restrict_outputright_table. (((G) = (((((dst_positive_code_multiply_restrict_outputright_table) + (dst_positive_scale_multiply_restrict_outputright_table)) * S ((dst_positive_code_multiply_restrict_outputright_table) + (dst_positive_scale_multiply_restrict_outputright_table)) + ((dst_positive_scale_multiply_restrict_outputright_table) + (dst_positive_scale_multiply_restrict_outputright_table))) + (((dst_negative_code_multiply_restrict_outputright_table) + (dst_negative_scale_multiply_restrict_outputright_table)) * S ((dst_negative_code_multiply_restrict_outputright_table) + (dst_negative_scale_multiply_restrict_outputright_table)) + ((dst_negative_scale_multiply_restrict_outputright_table) + (dst_negative_scale_multiply_restrict_outputright_table)))) * S ((((dst_positive_code_multiply_restrict_outputright_table) + (dst_positive_scale_multiply_restrict_outputright_table)) * S ((dst_positive_code_multiply_restrict_outputright_table) + (dst_positive_scale_multiply_restrict_outputright_table)) + ((dst_positive_scale_multiply_restrict_outputright_table) + (dst_positive_scale_multiply_restrict_outputright_table))) + (((dst_negative_code_multiply_restrict_outputright_table) + (dst_negative_scale_multiply_restrict_outputright_table)) * S ((dst_negative_code_multiply_restrict_outputright_table) + (dst_negative_scale_multiply_restrict_outputright_table)) + ((dst_negative_scale_multiply_restrict_outputright_table) + (dst_negative_scale_multiply_restrict_outputright_table)))) + ((((dst_negative_code_multiply_restrict_outputright_table) + (dst_negative_scale_multiply_restrict_outputright_table)) * S ((dst_negative_code_multiply_restrict_outputright_table) + (dst_negative_scale_multiply_restrict_outputright_table)) + ((dst_negative_scale_multiply_restrict_outputright_table) + (dst_negative_scale_multiply_restrict_outputright_table))) + (((dst_negative_code_multiply_restrict_outputright_table) + (dst_negative_scale_multiply_restrict_outputright_table)) * S ((dst_negative_code_multiply_restrict_outputright_table) + (dst_negative_scale_multiply_restrict_outputright_table)) + ((dst_negative_scale_multiply_restrict_outputright_table) + (dst_negative_scale_multiply_restrict_outputright_table)))))) /\ (forall dst_index_multiply_restrict_outputright_table. (exists pvs_le_gap_multiply_restrict_outputright_tabledomain. pvs_le_gap_multiply_restrict_outputright_tabledomain + (dst_index_multiply_restrict_outputright_table) = (l)) -> exists dst_positive_multiply_restrict_outputright_table dst_negative_multiply_restrict_outputright_table dst_value_multiply_restrict_outputright_table. ((((exists ff_h_pvs_multiply_restrict_outputright_tableentrypositive. ff_h_pvs_multiply_restrict_outputright_tableentrypositive + S (dst_positive_multiply_restrict_outputright_table) = S ((S (dst_index_multiply_restrict_outputright_table)) * dst_positive_scale_multiply_restrict_outputright_table)) /\ exists ff_q_pvs_multiply_restrict_outputright_tableentrypositive. dst_positive_code_multiply_restrict_outputright_table = ff_q_pvs_multiply_restrict_outputright_tableentrypositive * S ((S (dst_index_multiply_restrict_outputright_table)) * dst_positive_scale_multiply_restrict_outputright_table) + (dst_positive_multiply_restrict_outputright_table))) /\ (((((exists ff_h_pvs_multiply_restrict_outputright_tableentrynegative. ff_h_pvs_multiply_restrict_outputright_tableentrynegative + S (dst_negative_multiply_restrict_outputright_table) = S ((S (dst_index_multiply_restrict_outputright_table)) * dst_negative_scale_multiply_restrict_outputright_table)) /\ exists ff_q_pvs_multiply_restrict_outputright_tableentrynegative. dst_negative_code_multiply_restrict_outputright_table = ff_q_pvs_multiply_restrict_outputright_tableentrynegative * S ((S (dst_index_multiply_restrict_outputright_table)) * dst_negative_scale_multiply_restrict_outputright_table) + (dst_negative_multiply_restrict_outputright_table))) /\ (exists ge_balance_positive_multiply_restrict_outputright_tableentryvalue ge_balance_negative_multiply_restrict_outputright_tableentryvalue. (((((dst_value_multiply_restrict_outputright_table) = 2 * (ge_balance_positive_multiply_restrict_outputright_tableentryvalue) /\ (ge_balance_negative_multiply_restrict_outputright_tableentryvalue) = 0) \/ exists ge_signed_half_multiply_restrict_outputright_tableentryvaluedecode. (((dst_value_multiply_restrict_outputright_table) = 2 * ge_signed_half_multiply_restrict_outputright_tableentryvaluedecode + 1 /\ (ge_balance_positive_multiply_restrict_outputright_tableentryvalue) = 0) /\ (ge_balance_negative_multiply_restrict_outputright_tableentryvalue) = S ge_signed_half_multiply_restrict_outputright_tableentryvaluedecode))) /\ ((dst_positive_multiply_restrict_outputright_table) + ge_balance_negative_multiply_restrict_outputright_tableentryvalue = (dst_negative_multiply_restrict_outputright_table) + ge_balance_positive_multiply_restrict_outputright_tableentryvalue))))))))) /\ (((exists dst_positive_code_multiply_restrict_outputoutput_table dst_positive_scale_multiply_restrict_outputoutput_table dst_negative_code_multiply_restrict_outputoutput_table dst_negative_scale_multiply_restrict_outputoutput_table. (((H) = (((((dst_positive_code_multiply_restrict_outputoutput_table) + (dst_positive_scale_multiply_restrict_outputoutput_table)) * S ((dst_positive_code_multiply_restrict_outputoutput_table) + (dst_positive_scale_multiply_restrict_outputoutput_table)) + ((dst_positive_scale_multiply_restrict_outputoutput_table) + (dst_positive_scale_multiply_restrict_outputoutput_table))) + (((dst_negative_code_multiply_restrict_outputoutput_table) + (dst_negative_scale_multiply_restrict_outputoutput_table)) * S ((dst_negative_code_multiply_restrict_outputoutput_table) + (dst_negative_scale_multiply_restrict_outputoutput_table)) + ((dst_negative_scale_multiply_restrict_outputoutput_table) + (dst_negative_scale_multiply_restrict_outputoutput_table)))) * S ((((dst_positive_code_multiply_restrict_outputoutput_table) + (dst_positive_scale_multiply_restrict_outputoutput_table)) * S ((dst_positive_code_multiply_restrict_outputoutput_table) + (dst_positive_scale_multiply_restrict_outputoutput_table)) + ((dst_positive_scale_multiply_restrict_outputoutput_table) + (dst_positive_scale_multiply_restrict_outputoutput_table))) + (((dst_negative_code_multiply_restrict_outputoutput_table) + (dst_negative_scale_multiply_restrict_outputoutput_table)) * S ((dst_negative_code_multiply_restrict_outputoutput_table) + (dst_negative_scale_multiply_restrict_outputoutput_table)) + ((dst_negative_scale_multiply_restrict_outputoutput_table) + (dst_negative_scale_multiply_restrict_outputoutput_table)))) + ((((dst_negative_code_multiply_restrict_outputoutput_table) + (dst_negative_scale_multiply_restrict_outputoutput_table)) * S ((dst_negative_code_multiply_restrict_outputoutput_table) + (dst_negative_scale_multiply_restrict_outputoutput_table)) + ((dst_negative_scale_multiply_restrict_outputoutput_table) + (dst_negative_scale_multiply_restrict_outputoutput_table))) + (((dst_negative_code_multiply_restrict_outputoutput_table) + (dst_negative_scale_multiply_restrict_outputoutput_table)) * S ((dst_negative_code_multiply_restrict_outputoutput_table) + (dst_negative_scale_multiply_restrict_outputoutput_table)) + ((dst_negative_scale_multiply_restrict_outputoutput_table) + (dst_negative_scale_multiply_restrict_outputoutput_table)))))) /\ (forall dst_index_multiply_restrict_outputoutput_table. (exists pvs_le_gap_multiply_restrict_outputoutput_tabledomain. pvs_le_gap_multiply_restrict_outputoutput_tabledomain + (dst_index_multiply_restrict_outputoutput_table) = (l)) -> exists dst_positive_multiply_restrict_outputoutput_table dst_negative_multiply_restrict_outputoutput_table dst_value_multiply_restrict_outputoutput_table. ((((exists ff_h_pvs_multiply_restrict_outputoutput_tableentrypositive. ff_h_pvs_multiply_restrict_outputoutput_tableentrypositive + S (dst_positive_multiply_restrict_outputoutput_table) = S ((S (dst_index_multiply_restrict_outputoutput_table)) * dst_positive_scale_multiply_restrict_outputoutput_table)) /\ exists ff_q_pvs_multiply_restrict_outputoutput_tableentrypositive. dst_positive_code_multiply_restrict_outputoutput_table = ff_q_pvs_multiply_restrict_outputoutput_tableentrypositive * S ((S (dst_index_multiply_restrict_outputoutput_table)) * dst_positive_scale_multiply_restrict_outputoutput_table) + (dst_positive_multiply_restrict_outputoutput_table))) /\ (((((exists ff_h_pvs_multiply_restrict_outputoutput_tableentrynegative. ff_h_pvs_multiply_restrict_outputoutput_tableentrynegative + S (dst_negative_multiply_restrict_outputoutput_table) = S ((S (dst_index_multiply_restrict_outputoutput_table)) * dst_negative_scale_multiply_restrict_outputoutput_table)) /\ exists ff_q_pvs_multiply_restrict_outputoutput_tableentrynegative. dst_negative_code_multiply_restrict_outputoutput_table = ff_q_pvs_multiply_restrict_outputoutput_tableentrynegative * S ((S (dst_index_multiply_restrict_outputoutput_table)) * dst_negative_scale_multiply_restrict_outputoutput_table) + (dst_negative_multiply_restrict_outputoutput_table))) /\ (exists ge_balance_positive_multiply_restrict_outputoutput_tableentryvalue ge_balance_negative_multiply_restrict_outputoutput_tableentryvalue. (((((dst_value_multiply_restrict_outputoutput_table) = 2 * (ge_balance_positive_multiply_restrict_outputoutput_tableentryvalue) /\ (ge_balance_negative_multiply_restrict_outputoutput_tableentryvalue) = 0) \/ exists ge_signed_half_multiply_restrict_outputoutput_tableentryvaluedecode. (((dst_value_multiply_restrict_outputoutput_table) = 2 * ge_signed_half_multiply_restrict_outputoutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_multiply_restrict_outputoutput_tableentryvalue) = 0) /\ (ge_balance_negative_multiply_restrict_outputoutput_tableentryvalue) = S ge_signed_half_multiply_restrict_outputoutput_tableentryvaluedecode))) /\ ((dst_positive_multiply_restrict_outputoutput_table) + ge_balance_negative_multiply_restrict_outputoutput_tableentryvalue = (dst_negative_multiply_restrict_outputoutput_table) + ge_balance_positive_multiply_restrict_outputoutput_tableentryvalue))))))))) /\ (forall sto_index_multiply_restrict_outputentries. (exists pvs_gap_multiply_restrict_outputentriesbound. pvs_gap_multiply_restrict_outputentriesbound + S (sto_index_multiply_restrict_outputentries) = (l)) -> exists sto_left_multiply_restrict_outputentries sto_right_multiply_restrict_outputentries sto_output_multiply_restrict_outputentries. ((exists dst_positive_code_multiply_restrict_outputentriesentryleft dst_positive_scale_multiply_restrict_outputentriesentryleft dst_negative_code_multiply_restrict_outputentriesentryleft dst_negative_scale_multiply_restrict_outputentriesentryleft dst_positive_multiply_restrict_outputentriesentryleft dst_negative_multiply_restrict_outputentriesentryleft. (((F) = (((((dst_positive_code_multiply_restrict_outputentriesentryleft) + (dst_positive_scale_multiply_restrict_outputentriesentryleft)) * S ((dst_positive_code_multiply_restrict_outputentriesentryleft) + (dst_positive_scale_multiply_restrict_outputentriesentryleft)) + ((dst_positive_scale_multiply_restrict_outputentriesentryleft) + (dst_positive_scale_multiply_restrict_outputentriesentryleft))) + (((dst_negative_code_multiply_restrict_outputentriesentryleft) + (dst_negative_scale_multiply_restrict_outputentriesentryleft)) * S ((dst_negative_code_multiply_restrict_outputentriesentryleft) + (dst_negative_scale_multiply_restrict_outputentriesentryleft)) + ((dst_negative_scale_multiply_restrict_outputentriesentryleft) + (dst_negative_scale_multiply_restrict_outputentriesentryleft)))) * S ((((dst_positive_code_multiply_restrict_outputentriesentryleft) + (dst_positive_scale_multiply_restrict_outputentriesentryleft)) * S ((dst_positive_code_multiply_restrict_outputentriesentryleft) + (dst_positive_scale_multiply_restrict_outputentriesentryleft)) + ((dst_positive_scale_multiply_restrict_outputentriesentryleft) + (dst_positive_scale_multiply_restrict_outputentriesentryleft))) + (((dst_negative_code_multiply_restrict_outputentriesentryleft) + (dst_negative_scale_multiply_restrict_outputentriesentryleft)) * S ((dst_negative_code_multiply_restrict_outputentriesentryleft) + (dst_negative_scale_multiply_restrict_outputentriesentryleft)) + ((dst_negative_scale_multiply_restrict_outputentriesentryleft) + (dst_negative_scale_multiply_restrict_outputentriesentryleft)))) + ((((dst_negative_code_multiply_restrict_outputentriesentryleft) + (dst_negative_scale_multiply_restrict_outputentriesentryleft)) * S ((dst_negative_code_multiply_restrict_outputentriesentryleft) + (dst_negative_scale_multiply_restrict_outputentriesentryleft)) + ((dst_negative_scale_multiply_restrict_outputentriesentryleft) + (dst_negative_scale_multiply_restrict_outputentriesentryleft))) + (((dst_negative_code_multiply_restrict_outputentriesentryleft) + (dst_negative_scale_multiply_restrict_outputentriesentryleft)) * S ((dst_negative_code_multiply_restrict_outputentriesentryleft) + (dst_negative_scale_multiply_restrict_outputentriesentryleft)) + ((dst_negative_scale_multiply_restrict_outputentriesentryleft) + (dst_negative_scale_multiply_restrict_outputentriesentryleft)))))) /\ (((((exists ff_h_pvs_multiply_restrict_outputentriesentryleftpositive. ff_h_pvs_multiply_restrict_outputentriesentryleftpositive + S (dst_positive_multiply_restrict_outputentriesentryleft) = S ((S (sto_index_multiply_restrict_outputentries)) * dst_positive_scale_multiply_restrict_outputentriesentryleft)) /\ exists ff_q_pvs_multiply_restrict_outputentriesentryleftpositive. dst_positive_code_multiply_restrict_outputentriesentryleft = ff_q_pvs_multiply_restrict_outputentriesentryleftpositive * S ((S (sto_index_multiply_restrict_outputentries)) * dst_positive_scale_multiply_restrict_outputentriesentryleft) + (dst_positive_multiply_restrict_outputentriesentryleft))) /\ (((((exists ff_h_pvs_multiply_restrict_outputentriesentryleftnegative. ff_h_pvs_multiply_restrict_outputentriesentryleftnegative + S (dst_negative_multiply_restrict_outputentriesentryleft) = S ((S (sto_index_multiply_restrict_outputentries)) * dst_negative_scale_multiply_restrict_outputentriesentryleft)) /\ exists ff_q_pvs_multiply_restrict_outputentriesentryleftnegative. dst_negative_code_multiply_restrict_outputentriesentryleft = ff_q_pvs_multiply_restrict_outputentriesentryleftnegative * S ((S (sto_index_multiply_restrict_outputentries)) * dst_negative_scale_multiply_restrict_outputentriesentryleft) + (dst_negative_multiply_restrict_outputentriesentryleft))) /\ (exists ge_balance_positive_multiply_restrict_outputentriesentryleftvalue ge_balance_negative_multiply_restrict_outputentriesentryleftvalue. (((((sto_left_multiply_restrict_outputentries) = 2 * (ge_balance_positive_multiply_restrict_outputentriesentryleftvalue) /\ (ge_balance_negative_multiply_restrict_outputentriesentryleftvalue) = 0) \/ exists ge_signed_half_multiply_restrict_outputentriesentryleftvaluedecode. (((sto_left_multiply_restrict_outputentries) = 2 * ge_signed_half_multiply_restrict_outputentriesentryleftvaluedecode + 1 /\ (ge_balance_positive_multiply_restrict_outputentriesentryleftvalue) = 0) /\ (ge_balance_negative_multiply_restrict_outputentriesentryleftvalue) = S ge_signed_half_multiply_restrict_outputentriesentryleftvaluedecode))) /\ ((dst_positive_multiply_restrict_outputentriesentryleft) + ge_balance_negative_multiply_restrict_outputentriesentryleftvalue = (dst_negative_multiply_restrict_outputentriesentryleft) + ge_balance_positive_multiply_restrict_outputentriesentryleftvalue))))))))) /\ (((exists dst_positive_code_multiply_restrict_outputentriesentryright dst_positive_scale_multiply_restrict_outputentriesentryright dst_negative_code_multiply_restrict_outputentriesentryright dst_negative_scale_multiply_restrict_outputentriesentryright dst_positive_multiply_restrict_outputentriesentryright dst_negative_multiply_restrict_outputentriesentryright. (((G) = (((((dst_positive_code_multiply_restrict_outputentriesentryright) + (dst_positive_scale_multiply_restrict_outputentriesentryright)) * S ((dst_positive_code_multiply_restrict_outputentriesentryright) + (dst_positive_scale_multiply_restrict_outputentriesentryright)) + ((dst_positive_scale_multiply_restrict_outputentriesentryright) + (dst_positive_scale_multiply_restrict_outputentriesentryright))) + (((dst_negative_code_multiply_restrict_outputentriesentryright) + (dst_negative_scale_multiply_restrict_outputentriesentryright)) * S ((dst_negative_code_multiply_restrict_outputentriesentryright) + (dst_negative_scale_multiply_restrict_outputentriesentryright)) + ((dst_negative_scale_multiply_restrict_outputentriesentryright) + (dst_negative_scale_multiply_restrict_outputentriesentryright)))) * S ((((dst_positive_code_multiply_restrict_outputentriesentryright) + (dst_positive_scale_multiply_restrict_outputentriesentryright)) * S ((dst_positive_code_multiply_restrict_outputentriesentryright) + (dst_positive_scale_multiply_restrict_outputentriesentryright)) + ((dst_positive_scale_multiply_restrict_outputentriesentryright) + (dst_positive_scale_multiply_restrict_outputentriesentryright))) + (((dst_negative_code_multiply_restrict_outputentriesentryright) + (dst_negative_scale_multiply_restrict_outputentriesentryright)) * S ((dst_negative_code_multiply_restrict_outputentriesentryright) + (dst_negative_scale_multiply_restrict_outputentriesentryright)) + ((dst_negative_scale_multiply_restrict_outputentriesentryright) + (dst_negative_scale_multiply_restrict_outputentriesentryright)))) + ((((dst_negative_code_multiply_restrict_outputentriesentryright) + (dst_negative_scale_multiply_restrict_outputentriesentryright)) * S ((dst_negative_code_multiply_restrict_outputentriesentryright) + (dst_negative_scale_multiply_restrict_outputentriesentryright)) + ((dst_negative_scale_multiply_restrict_outputentriesentryright) + (dst_negative_scale_multiply_restrict_outputentriesentryright))) + (((dst_negative_code_multiply_restrict_outputentriesentryright) + (dst_negative_scale_multiply_restrict_outputentriesentryright)) * S ((dst_negative_code_multiply_restrict_outputentriesentryright) + (dst_negative_scale_multiply_restrict_outputentriesentryright)) + ((dst_negative_scale_multiply_restrict_outputentriesentryright) + (dst_negative_scale_multiply_restrict_outputentriesentryright)))))) /\ (((((exists ff_h_pvs_multiply_restrict_outputentriesentryrightpositive. ff_h_pvs_multiply_restrict_outputentriesentryrightpositive + S (dst_positive_multiply_restrict_outputentriesentryright) = S ((S (sto_index_multiply_restrict_outputentries)) * dst_positive_scale_multiply_restrict_outputentriesentryright)) /\ exists ff_q_pvs_multiply_restrict_outputentriesentryrightpositive. dst_positive_code_multiply_restrict_outputentriesentryright = ff_q_pvs_multiply_restrict_outputentriesentryrightpositive * S ((S (sto_index_multiply_restrict_outputentries)) * dst_positive_scale_multiply_restrict_outputentriesentryright) + (dst_positive_multiply_restrict_outputentriesentryright))) /\ (((((exists ff_h_pvs_multiply_restrict_outputentriesentryrightnegative. ff_h_pvs_multiply_restrict_outputentriesentryrightnegative + S (dst_negative_multiply_restrict_outputentriesentryright) = S ((S (sto_index_multiply_restrict_outputentries)) * dst_negative_scale_multiply_restrict_outputentriesentryright)) /\ exists ff_q_pvs_multiply_restrict_outputentriesentryrightnegative. dst_negative_code_multiply_restrict_outputentriesentryright = ff_q_pvs_multiply_restrict_outputentriesentryrightnegative * S ((S (sto_index_multiply_restrict_outputentries)) * dst_negative_scale_multiply_restrict_outputentriesentryright) + (dst_negative_multiply_restrict_outputentriesentryright))) /\ (exists ge_balance_positive_multiply_restrict_outputentriesentryrightvalue ge_balance_negative_multiply_restrict_outputentriesentryrightvalue. (((((sto_right_multiply_restrict_outputentries) = 2 * (ge_balance_positive_multiply_restrict_outputentriesentryrightvalue) /\ (ge_balance_negative_multiply_restrict_outputentriesentryrightvalue) = 0) \/ exists ge_signed_half_multiply_restrict_outputentriesentryrightvaluedecode. (((sto_right_multiply_restrict_outputentries) = 2 * ge_signed_half_multiply_restrict_outputentriesentryrightvaluedecode + 1 /\ (ge_balance_positive_multiply_restrict_outputentriesentryrightvalue) = 0) /\ (ge_balance_negative_multiply_restrict_outputentriesentryrightvalue) = S ge_signed_half_multiply_restrict_outputentriesentryrightvaluedecode))) /\ ((dst_positive_multiply_restrict_outputentriesentryright) + ge_balance_negative_multiply_restrict_outputentriesentryrightvalue = (dst_negative_multiply_restrict_outputentriesentryright) + ge_balance_positive_multiply_restrict_outputentriesentryrightvalue))))))))) /\ (((exists dst_positive_code_multiply_restrict_outputentriesentryoutput dst_positive_scale_multiply_restrict_outputentriesentryoutput dst_negative_code_multiply_restrict_outputentriesentryoutput dst_negative_scale_multiply_restrict_outputentriesentryoutput dst_positive_multiply_restrict_outputentriesentryoutput dst_negative_multiply_restrict_outputentriesentryoutput. (((H) = (((((dst_positive_code_multiply_restrict_outputentriesentryoutput) + (dst_positive_scale_multiply_restrict_outputentriesentryoutput)) * S ((dst_positive_code_multiply_restrict_outputentriesentryoutput) + (dst_positive_scale_multiply_restrict_outputentriesentryoutput)) + ((dst_positive_scale_multiply_restrict_outputentriesentryoutput) + (dst_positive_scale_multiply_restrict_outputentriesentryoutput))) + (((dst_negative_code_multiply_restrict_outputentriesentryoutput) + (dst_negative_scale_multiply_restrict_outputentriesentryoutput)) * S ((dst_negative_code_multiply_restrict_outputentriesentryoutput) + (dst_negative_scale_multiply_restrict_outputentriesentryoutput)) + ((dst_negative_scale_multiply_restrict_outputentriesentryoutput) + (dst_negative_scale_multiply_restrict_outputentriesentryoutput)))) * S ((((dst_positive_code_multiply_restrict_outputentriesentryoutput) + (dst_positive_scale_multiply_restrict_outputentriesentryoutput)) * S ((dst_positive_code_multiply_restrict_outputentriesentryoutput) + (dst_positive_scale_multiply_restrict_outputentriesentryoutput)) + ((dst_positive_scale_multiply_restrict_outputentriesentryoutput) + (dst_positive_scale_multiply_restrict_outputentriesentryoutput))) + (((dst_negative_code_multiply_restrict_outputentriesentryoutput) + (dst_negative_scale_multiply_restrict_outputentriesentryoutput)) * S ((dst_negative_code_multiply_restrict_outputentriesentryoutput) + (dst_negative_scale_multiply_restrict_outputentriesentryoutput)) + ((dst_negative_scale_multiply_restrict_outputentriesentryoutput) + (dst_negative_scale_multiply_restrict_outputentriesentryoutput)))) + ((((dst_negative_code_multiply_restrict_outputentriesentryoutput) + (dst_negative_scale_multiply_restrict_outputentriesentryoutput)) * S ((dst_negative_code_multiply_restrict_outputentriesentryoutput) + (dst_negative_scale_multiply_restrict_outputentriesentryoutput)) + ((dst_negative_scale_multiply_restrict_outputentriesentryoutput) + (dst_negative_scale_multiply_restrict_outputentriesentryoutput))) + (((dst_negative_code_multiply_restrict_outputentriesentryoutput) + (dst_negative_scale_multiply_restrict_outputentriesentryoutput)) * S ((dst_negative_code_multiply_restrict_outputentriesentryoutput) + (dst_negative_scale_multiply_restrict_outputentriesentryoutput)) + ((dst_negative_scale_multiply_restrict_outputentriesentryoutput) + (dst_negative_scale_multiply_restrict_outputentriesentryoutput)))))) /\ (((((exists ff_h_pvs_multiply_restrict_outputentriesentryoutputpositive. ff_h_pvs_multiply_restrict_outputentriesentryoutputpositive + S (dst_positive_multiply_restrict_outputentriesentryoutput) = S ((S (sto_index_multiply_restrict_outputentries)) * dst_positive_scale_multiply_restrict_outputentriesentryoutput)) /\ exists ff_q_pvs_multiply_restrict_outputentriesentryoutputpositive. dst_positive_code_multiply_restrict_outputentriesentryoutput = ff_q_pvs_multiply_restrict_outputentriesentryoutputpositive * S ((S (sto_index_multiply_restrict_outputentries)) * dst_positive_scale_multiply_restrict_outputentriesentryoutput) + (dst_positive_multiply_restrict_outputentriesentryoutput))) /\ (((((exists ff_h_pvs_multiply_restrict_outputentriesentryoutputnegative. ff_h_pvs_multiply_restrict_outputentriesentryoutputnegative + S (dst_negative_multiply_restrict_outputentriesentryoutput) = S ((S (sto_index_multiply_restrict_outputentries)) * dst_negative_scale_multiply_restrict_outputentriesentryoutput)) /\ exists ff_q_pvs_multiply_restrict_outputentriesentryoutputnegative. dst_negative_code_multiply_restrict_outputentriesentryoutput = ff_q_pvs_multiply_restrict_outputentriesentryoutputnegative * S ((S (sto_index_multiply_restrict_outputentries)) * dst_negative_scale_multiply_restrict_outputentriesentryoutput) + (dst_negative_multiply_restrict_outputentriesentryoutput))) /\ (exists ge_balance_positive_multiply_restrict_outputentriesentryoutputvalue ge_balance_negative_multiply_restrict_outputentriesentryoutputvalue. (((((sto_output_multiply_restrict_outputentries) = 2 * (ge_balance_positive_multiply_restrict_outputentriesentryoutputvalue) /\ (ge_balance_negative_multiply_restrict_outputentriesentryoutputvalue) = 0) \/ exists ge_signed_half_multiply_restrict_outputentriesentryoutputvaluedecode. (((sto_output_multiply_restrict_outputentries) = 2 * ge_signed_half_multiply_restrict_outputentriesentryoutputvaluedecode + 1 /\ (ge_balance_positive_multiply_restrict_outputentriesentryoutputvalue) = 0) /\ (ge_balance_negative_multiply_restrict_outputentriesentryoutputvalue) = S ge_signed_half_multiply_restrict_outputentriesentryoutputvaluedecode))) /\ ((dst_positive_multiply_restrict_outputentriesentryoutput) + ge_balance_negative_multiply_restrict_outputentriesentryoutputvalue = (dst_negative_multiply_restrict_outputentriesentryoutput) + ge_balance_positive_multiply_restrict_outputentriesentryoutputvalue))))))))) /\ (exists sto_ap_multiply_restrict_outputentriesentryoperation sto_an_multiply_restrict_outputentriesentryoperation sto_bp_multiply_restrict_outputentriesentryoperation sto_bn_multiply_restrict_outputentriesentryoperation sto_cp_multiply_restrict_outputentriesentryoperation sto_cn_multiply_restrict_outputentriesentryoperation. (((((sto_left_multiply_restrict_outputentries) = 2 * (sto_ap_multiply_restrict_outputentriesentryoperation) /\ (sto_an_multiply_restrict_outputentriesentryoperation) = 0) \/ exists ge_signed_half_multiply_restrict_outputentriesentryoperationleft. (((sto_left_multiply_restrict_outputentries) = 2 * ge_signed_half_multiply_restrict_outputentriesentryoperationleft + 1 /\ (sto_ap_multiply_restrict_outputentriesentryoperation) = 0) /\ (sto_an_multiply_restrict_outputentriesentryoperation) = S ge_signed_half_multiply_restrict_outputentriesentryoperationleft))) /\ ((((((sto_right_multiply_restrict_outputentries) = 2 * (sto_bp_multiply_restrict_outputentriesentryoperation) /\ (sto_bn_multiply_restrict_outputentriesentryoperation) = 0) \/ exists ge_signed_half_multiply_restrict_outputentriesentryoperationright. (((sto_right_multiply_restrict_outputentries) = 2 * ge_signed_half_multiply_restrict_outputentriesentryoperationright + 1 /\ (sto_bp_multiply_restrict_outputentriesentryoperation) = 0) /\ (sto_bn_multiply_restrict_outputentriesentryoperation) = S ge_signed_half_multiply_restrict_outputentriesentryoperationright))) /\ ((((((sto_output_multiply_restrict_outputentries) = 2 * (sto_cp_multiply_restrict_outputentriesentryoperation) /\ (sto_cn_multiply_restrict_outputentriesentryoperation) = 0) \/ exists ge_signed_half_multiply_restrict_outputentriesentryoperationoutput. (((sto_output_multiply_restrict_outputentries) = 2 * ge_signed_half_multiply_restrict_outputentriesentryoperationoutput + 1 /\ (sto_cp_multiply_restrict_outputentriesentryoperation) = 0) /\ (sto_cn_multiply_restrict_outputentriesentryoperation) = S ge_signed_half_multiply_restrict_outputentriesentryoperationoutput))) /\ ((sto_ap_multiply_restrict_outputentriesentryoperation * sto_bp_multiply_restrict_outputentriesentryoperation + sto_an_multiply_restrict_outputentriesentryoperation * sto_bn_multiply_restrict_outputentriesentryoperation) + sto_cn_multiply_restrict_outputentriesentryoperation = (sto_ap_multiply_restrict_outputentriesentryoperation * sto_bn_multiply_restrict_outputentriesentryoperation + sto_an_multiply_restrict_outputentriesentryoperation * sto_bp_multiply_restrict_outputentriesentryoperation) + sto_cp_multiply_restrict_outputentriesentryoperation)))))))))))))))))))