signed_table_multiply_empty

Exact expanded first-order arithmetic statement

forall F G H. (exists dst_positive_code_multiply_empty_0 dst_positive_scale_multiply_empty_0 dst_negative_code_multiply_empty_0 dst_negative_scale_multiply_empty_0. (((F) = (((((dst_positive_code_multiply_empty_0) + (dst_positive_scale_multiply_empty_0)) * S ((dst_positive_code_multiply_empty_0) + (dst_positive_scale_multiply_empty_0)) + ((dst_positive_scale_multiply_empty_0) + (dst_positive_scale_multiply_empty_0))) + (((dst_negative_code_multiply_empty_0) + (dst_negative_scale_multiply_empty_0)) * S ((dst_negative_code_multiply_empty_0) + (dst_negative_scale_multiply_empty_0)) + ((dst_negative_scale_multiply_empty_0) + (dst_negative_scale_multiply_empty_0)))) * S ((((dst_positive_code_multiply_empty_0) + (dst_positive_scale_multiply_empty_0)) * S ((dst_positive_code_multiply_empty_0) + (dst_positive_scale_multiply_empty_0)) + ((dst_positive_scale_multiply_empty_0) + (dst_positive_scale_multiply_empty_0))) + (((dst_negative_code_multiply_empty_0) + (dst_negative_scale_multiply_empty_0)) * S ((dst_negative_code_multiply_empty_0) + (dst_negative_scale_multiply_empty_0)) + ((dst_negative_scale_multiply_empty_0) + (dst_negative_scale_multiply_empty_0)))) + ((((dst_negative_code_multiply_empty_0) + (dst_negative_scale_multiply_empty_0)) * S ((dst_negative_code_multiply_empty_0) + (dst_negative_scale_multiply_empty_0)) + ((dst_negative_scale_multiply_empty_0) + (dst_negative_scale_multiply_empty_0))) + (((dst_negative_code_multiply_empty_0) + (dst_negative_scale_multiply_empty_0)) * S ((dst_negative_code_multiply_empty_0) + (dst_negative_scale_multiply_empty_0)) + ((dst_negative_scale_multiply_empty_0) + (dst_negative_scale_multiply_empty_0)))))) /\ (forall dst_index_multiply_empty_0. (exists pvs_le_gap_multiply_empty_0domain. pvs_le_gap_multiply_empty_0domain + (dst_index_multiply_empty_0) = (0)) -> exists dst_positive_multiply_empty_0 dst_negative_multiply_empty_0 dst_value_multiply_empty_0. ((((exists ff_h_pvs_multiply_empty_0entrypositive. ff_h_pvs_multiply_empty_0entrypositive + S (dst_positive_multiply_empty_0) = S ((S (dst_index_multiply_empty_0)) * dst_positive_scale_multiply_empty_0)) /\ exists ff_q_pvs_multiply_empty_0entrypositive. dst_positive_code_multiply_empty_0 = ff_q_pvs_multiply_empty_0entrypositive * S ((S (dst_index_multiply_empty_0)) * dst_positive_scale_multiply_empty_0) + (dst_positive_multiply_empty_0))) /\ (((((exists ff_h_pvs_multiply_empty_0entrynegative. ff_h_pvs_multiply_empty_0entrynegative + S (dst_negative_multiply_empty_0) = S ((S (dst_index_multiply_empty_0)) * dst_negative_scale_multiply_empty_0)) /\ exists ff_q_pvs_multiply_empty_0entrynegative. dst_negative_code_multiply_empty_0 = ff_q_pvs_multiply_empty_0entrynegative * S ((S (dst_index_multiply_empty_0)) * dst_negative_scale_multiply_empty_0) + (dst_negative_multiply_empty_0))) /\ (exists ge_balance_positive_multiply_empty_0entryvalue ge_balance_negative_multiply_empty_0entryvalue. (((((dst_value_multiply_empty_0) = 2 * (ge_balance_positive_multiply_empty_0entryvalue) /\ (ge_balance_negative_multiply_empty_0entryvalue) = 0) \/ exists ge_signed_half_multiply_empty_0entryvaluedecode. (((dst_value_multiply_empty_0) = 2 * ge_signed_half_multiply_empty_0entryvaluedecode + 1 /\ (ge_balance_positive_multiply_empty_0entryvalue) = 0) /\ (ge_balance_negative_multiply_empty_0entryvalue) = S ge_signed_half_multiply_empty_0entryvaluedecode))) /\ ((dst_positive_multiply_empty_0) + ge_balance_negative_multiply_empty_0entryvalue = (dst_negative_multiply_empty_0) + ge_balance_positive_multiply_empty_0entryvalue))))))))) -> (exists dst_positive_code_multiply_empty_1 dst_positive_scale_multiply_empty_1 dst_negative_code_multiply_empty_1 dst_negative_scale_multiply_empty_1. (((G) = (((((dst_positive_code_multiply_empty_1) + (dst_positive_scale_multiply_empty_1)) * S ((dst_positive_code_multiply_empty_1) + (dst_positive_scale_multiply_empty_1)) + ((dst_positive_scale_multiply_empty_1) + (dst_positive_scale_multiply_empty_1))) + (((dst_negative_code_multiply_empty_1) + (dst_negative_scale_multiply_empty_1)) * S ((dst_negative_code_multiply_empty_1) + (dst_negative_scale_multiply_empty_1)) + ((dst_negative_scale_multiply_empty_1) + (dst_negative_scale_multiply_empty_1)))) * S ((((dst_positive_code_multiply_empty_1) + (dst_positive_scale_multiply_empty_1)) * S ((dst_positive_code_multiply_empty_1) + (dst_positive_scale_multiply_empty_1)) + ((dst_positive_scale_multiply_empty_1) + (dst_positive_scale_multiply_empty_1))) + (((dst_negative_code_multiply_empty_1) + (dst_negative_scale_multiply_empty_1)) * S ((dst_negative_code_multiply_empty_1) + (dst_negative_scale_multiply_empty_1)) + ((dst_negative_scale_multiply_empty_1) + (dst_negative_scale_multiply_empty_1)))) + ((((dst_negative_code_multiply_empty_1) + (dst_negative_scale_multiply_empty_1)) * S ((dst_negative_code_multiply_empty_1) + (dst_negative_scale_multiply_empty_1)) + ((dst_negative_scale_multiply_empty_1) + (dst_negative_scale_multiply_empty_1))) + (((dst_negative_code_multiply_empty_1) + (dst_negative_scale_multiply_empty_1)) * S ((dst_negative_code_multiply_empty_1) + (dst_negative_scale_multiply_empty_1)) + ((dst_negative_scale_multiply_empty_1) + (dst_negative_scale_multiply_empty_1)))))) /\ (forall dst_index_multiply_empty_1. (exists pvs_le_gap_multiply_empty_1domain. pvs_le_gap_multiply_empty_1domain + (dst_index_multiply_empty_1) = (0)) -> exists dst_positive_multiply_empty_1 dst_negative_multiply_empty_1 dst_value_multiply_empty_1. ((((exists ff_h_pvs_multiply_empty_1entrypositive. ff_h_pvs_multiply_empty_1entrypositive + S (dst_positive_multiply_empty_1) = S ((S (dst_index_multiply_empty_1)) * dst_positive_scale_multiply_empty_1)) /\ exists ff_q_pvs_multiply_empty_1entrypositive. dst_positive_code_multiply_empty_1 = ff_q_pvs_multiply_empty_1entrypositive * S ((S (dst_index_multiply_empty_1)) * dst_positive_scale_multiply_empty_1) + (dst_positive_multiply_empty_1))) /\ (((((exists ff_h_pvs_multiply_empty_1entrynegative. ff_h_pvs_multiply_empty_1entrynegative + S (dst_negative_multiply_empty_1) = S ((S (dst_index_multiply_empty_1)) * dst_negative_scale_multiply_empty_1)) /\ exists ff_q_pvs_multiply_empty_1entrynegative. dst_negative_code_multiply_empty_1 = ff_q_pvs_multiply_empty_1entrynegative * S ((S (dst_index_multiply_empty_1)) * dst_negative_scale_multiply_empty_1) + (dst_negative_multiply_empty_1))) /\ (exists ge_balance_positive_multiply_empty_1entryvalue ge_balance_negative_multiply_empty_1entryvalue. (((((dst_value_multiply_empty_1) = 2 * (ge_balance_positive_multiply_empty_1entryvalue) /\ (ge_balance_negative_multiply_empty_1entryvalue) = 0) \/ exists ge_signed_half_multiply_empty_1entryvaluedecode. (((dst_value_multiply_empty_1) = 2 * ge_signed_half_multiply_empty_1entryvaluedecode + 1 /\ (ge_balance_positive_multiply_empty_1entryvalue) = 0) /\ (ge_balance_negative_multiply_empty_1entryvalue) = S ge_signed_half_multiply_empty_1entryvaluedecode))) /\ ((dst_positive_multiply_empty_1) + ge_balance_negative_multiply_empty_1entryvalue = (dst_negative_multiply_empty_1) + ge_balance_positive_multiply_empty_1entryvalue))))))))) -> (exists dst_positive_code_multiply_empty_2 dst_positive_scale_multiply_empty_2 dst_negative_code_multiply_empty_2 dst_negative_scale_multiply_empty_2. (((H) = (((((dst_positive_code_multiply_empty_2) + (dst_positive_scale_multiply_empty_2)) * S ((dst_positive_code_multiply_empty_2) + (dst_positive_scale_multiply_empty_2)) + ((dst_positive_scale_multiply_empty_2) + (dst_positive_scale_multiply_empty_2))) + (((dst_negative_code_multiply_empty_2) + (dst_negative_scale_multiply_empty_2)) * S ((dst_negative_code_multiply_empty_2) + (dst_negative_scale_multiply_empty_2)) + ((dst_negative_scale_multiply_empty_2) + (dst_negative_scale_multiply_empty_2)))) * S ((((dst_positive_code_multiply_empty_2) + (dst_positive_scale_multiply_empty_2)) * S ((dst_positive_code_multiply_empty_2) + (dst_positive_scale_multiply_empty_2)) + ((dst_positive_scale_multiply_empty_2) + (dst_positive_scale_multiply_empty_2))) + (((dst_negative_code_multiply_empty_2) + (dst_negative_scale_multiply_empty_2)) * S ((dst_negative_code_multiply_empty_2) + (dst_negative_scale_multiply_empty_2)) + ((dst_negative_scale_multiply_empty_2) + (dst_negative_scale_multiply_empty_2)))) + ((((dst_negative_code_multiply_empty_2) + (dst_negative_scale_multiply_empty_2)) * S ((dst_negative_code_multiply_empty_2) + (dst_negative_scale_multiply_empty_2)) + ((dst_negative_scale_multiply_empty_2) + (dst_negative_scale_multiply_empty_2))) + (((dst_negative_code_multiply_empty_2) + (dst_negative_scale_multiply_empty_2)) * S ((dst_negative_code_multiply_empty_2) + (dst_negative_scale_multiply_empty_2)) + ((dst_negative_scale_multiply_empty_2) + (dst_negative_scale_multiply_empty_2)))))) /\ (forall dst_index_multiply_empty_2. (exists pvs_le_gap_multiply_empty_2domain. pvs_le_gap_multiply_empty_2domain + (dst_index_multiply_empty_2) = (0)) -> exists dst_positive_multiply_empty_2 dst_negative_multiply_empty_2 dst_value_multiply_empty_2. ((((exists ff_h_pvs_multiply_empty_2entrypositive. ff_h_pvs_multiply_empty_2entrypositive + S (dst_positive_multiply_empty_2) = S ((S (dst_index_multiply_empty_2)) * dst_positive_scale_multiply_empty_2)) /\ exists ff_q_pvs_multiply_empty_2entrypositive. dst_positive_code_multiply_empty_2 = ff_q_pvs_multiply_empty_2entrypositive * S ((S (dst_index_multiply_empty_2)) * dst_positive_scale_multiply_empty_2) + (dst_positive_multiply_empty_2))) /\ (((((exists ff_h_pvs_multiply_empty_2entrynegative. ff_h_pvs_multiply_empty_2entrynegative + S (dst_negative_multiply_empty_2) = S ((S (dst_index_multiply_empty_2)) * dst_negative_scale_multiply_empty_2)) /\ exists ff_q_pvs_multiply_empty_2entrynegative. dst_negative_code_multiply_empty_2 = ff_q_pvs_multiply_empty_2entrynegative * S ((S (dst_index_multiply_empty_2)) * dst_negative_scale_multiply_empty_2) + (dst_negative_multiply_empty_2))) /\ (exists ge_balance_positive_multiply_empty_2entryvalue ge_balance_negative_multiply_empty_2entryvalue. (((((dst_value_multiply_empty_2) = 2 * (ge_balance_positive_multiply_empty_2entryvalue) /\ (ge_balance_negative_multiply_empty_2entryvalue) = 0) \/ exists ge_signed_half_multiply_empty_2entryvaluedecode. (((dst_value_multiply_empty_2) = 2 * ge_signed_half_multiply_empty_2entryvaluedecode + 1 /\ (ge_balance_positive_multiply_empty_2entryvalue) = 0) /\ (ge_balance_negative_multiply_empty_2entryvalue) = S ge_signed_half_multiply_empty_2entryvaluedecode))) /\ ((dst_positive_multiply_empty_2) + ge_balance_negative_multiply_empty_2entryvalue = (dst_negative_multiply_empty_2) + ge_balance_positive_multiply_empty_2entryvalue))))))))) -> (((exists dst_positive_code_multiply_empty_resultleft_table dst_positive_scale_multiply_empty_resultleft_table dst_negative_code_multiply_empty_resultleft_table dst_negative_scale_multiply_empty_resultleft_table. (((F) = (((((dst_positive_code_multiply_empty_resultleft_table) + (dst_positive_scale_multiply_empty_resultleft_table)) * S ((dst_positive_code_multiply_empty_resultleft_table) + (dst_positive_scale_multiply_empty_resultleft_table)) + ((dst_positive_scale_multiply_empty_resultleft_table) + (dst_positive_scale_multiply_empty_resultleft_table))) + (((dst_negative_code_multiply_empty_resultleft_table) + (dst_negative_scale_multiply_empty_resultleft_table)) * S ((dst_negative_code_multiply_empty_resultleft_table) + (dst_negative_scale_multiply_empty_resultleft_table)) + ((dst_negative_scale_multiply_empty_resultleft_table) + (dst_negative_scale_multiply_empty_resultleft_table)))) * S ((((dst_positive_code_multiply_empty_resultleft_table) + (dst_positive_scale_multiply_empty_resultleft_table)) * S ((dst_positive_code_multiply_empty_resultleft_table) + (dst_positive_scale_multiply_empty_resultleft_table)) + ((dst_positive_scale_multiply_empty_resultleft_table) + (dst_positive_scale_multiply_empty_resultleft_table))) + (((dst_negative_code_multiply_empty_resultleft_table) + (dst_negative_scale_multiply_empty_resultleft_table)) * S ((dst_negative_code_multiply_empty_resultleft_table) + (dst_negative_scale_multiply_empty_resultleft_table)) + ((dst_negative_scale_multiply_empty_resultleft_table) + (dst_negative_scale_multiply_empty_resultleft_table)))) + ((((dst_negative_code_multiply_empty_resultleft_table) + (dst_negative_scale_multiply_empty_resultleft_table)) * S ((dst_negative_code_multiply_empty_resultleft_table) + (dst_negative_scale_multiply_empty_resultleft_table)) + ((dst_negative_scale_multiply_empty_resultleft_table) + (dst_negative_scale_multiply_empty_resultleft_table))) + (((dst_negative_code_multiply_empty_resultleft_table) + (dst_negative_scale_multiply_empty_resultleft_table)) * S ((dst_negative_code_multiply_empty_resultleft_table) + (dst_negative_scale_multiply_empty_resultleft_table)) + ((dst_negative_scale_multiply_empty_resultleft_table) + (dst_negative_scale_multiply_empty_resultleft_table)))))) /\ (forall dst_index_multiply_empty_resultleft_table. (exists pvs_le_gap_multiply_empty_resultleft_tabledomain. pvs_le_gap_multiply_empty_resultleft_tabledomain + (dst_index_multiply_empty_resultleft_table) = (0)) -> exists dst_positive_multiply_empty_resultleft_table dst_negative_multiply_empty_resultleft_table dst_value_multiply_empty_resultleft_table. ((((exists ff_h_pvs_multiply_empty_resultleft_tableentrypositive. ff_h_pvs_multiply_empty_resultleft_tableentrypositive + S (dst_positive_multiply_empty_resultleft_table) = S ((S (dst_index_multiply_empty_resultleft_table)) * dst_positive_scale_multiply_empty_resultleft_table)) /\ exists ff_q_pvs_multiply_empty_resultleft_tableentrypositive. dst_positive_code_multiply_empty_resultleft_table = ff_q_pvs_multiply_empty_resultleft_tableentrypositive * S ((S (dst_index_multiply_empty_resultleft_table)) * dst_positive_scale_multiply_empty_resultleft_table) + (dst_positive_multiply_empty_resultleft_table))) /\ (((((exists ff_h_pvs_multiply_empty_resultleft_tableentrynegative. ff_h_pvs_multiply_empty_resultleft_tableentrynegative + S (dst_negative_multiply_empty_resultleft_table) = S ((S (dst_index_multiply_empty_resultleft_table)) * dst_negative_scale_multiply_empty_resultleft_table)) /\ exists ff_q_pvs_multiply_empty_resultleft_tableentrynegative. dst_negative_code_multiply_empty_resultleft_table = ff_q_pvs_multiply_empty_resultleft_tableentrynegative * S ((S (dst_index_multiply_empty_resultleft_table)) * dst_negative_scale_multiply_empty_resultleft_table) + (dst_negative_multiply_empty_resultleft_table))) /\ (exists ge_balance_positive_multiply_empty_resultleft_tableentryvalue ge_balance_negative_multiply_empty_resultleft_tableentryvalue. (((((dst_value_multiply_empty_resultleft_table) = 2 * (ge_balance_positive_multiply_empty_resultleft_tableentryvalue) /\ (ge_balance_negative_multiply_empty_resultleft_tableentryvalue) = 0) \/ exists ge_signed_half_multiply_empty_resultleft_tableentryvaluedecode. (((dst_value_multiply_empty_resultleft_table) = 2 * ge_signed_half_multiply_empty_resultleft_tableentryvaluedecode + 1 /\ (ge_balance_positive_multiply_empty_resultleft_tableentryvalue) = 0) /\ (ge_balance_negative_multiply_empty_resultleft_tableentryvalue) = S ge_signed_half_multiply_empty_resultleft_tableentryvaluedecode))) /\ ((dst_positive_multiply_empty_resultleft_table) + ge_balance_negative_multiply_empty_resultleft_tableentryvalue = (dst_negative_multiply_empty_resultleft_table) + ge_balance_positive_multiply_empty_resultleft_tableentryvalue))))))))) /\ (((exists dst_positive_code_multiply_empty_resultright_table dst_positive_scale_multiply_empty_resultright_table dst_negative_code_multiply_empty_resultright_table dst_negative_scale_multiply_empty_resultright_table. (((G) = (((((dst_positive_code_multiply_empty_resultright_table) + (dst_positive_scale_multiply_empty_resultright_table)) * S ((dst_positive_code_multiply_empty_resultright_table) + (dst_positive_scale_multiply_empty_resultright_table)) + ((dst_positive_scale_multiply_empty_resultright_table) + (dst_positive_scale_multiply_empty_resultright_table))) + (((dst_negative_code_multiply_empty_resultright_table) + (dst_negative_scale_multiply_empty_resultright_table)) * S ((dst_negative_code_multiply_empty_resultright_table) + (dst_negative_scale_multiply_empty_resultright_table)) + ((dst_negative_scale_multiply_empty_resultright_table) + (dst_negative_scale_multiply_empty_resultright_table)))) * S ((((dst_positive_code_multiply_empty_resultright_table) + (dst_positive_scale_multiply_empty_resultright_table)) * S ((dst_positive_code_multiply_empty_resultright_table) + (dst_positive_scale_multiply_empty_resultright_table)) + ((dst_positive_scale_multiply_empty_resultright_table) + (dst_positive_scale_multiply_empty_resultright_table))) + (((dst_negative_code_multiply_empty_resultright_table) + (dst_negative_scale_multiply_empty_resultright_table)) * S ((dst_negative_code_multiply_empty_resultright_table) + (dst_negative_scale_multiply_empty_resultright_table)) + ((dst_negative_scale_multiply_empty_resultright_table) + (dst_negative_scale_multiply_empty_resultright_table)))) + ((((dst_negative_code_multiply_empty_resultright_table) + (dst_negative_scale_multiply_empty_resultright_table)) * S ((dst_negative_code_multiply_empty_resultright_table) + (dst_negative_scale_multiply_empty_resultright_table)) + ((dst_negative_scale_multiply_empty_resultright_table) + (dst_negative_scale_multiply_empty_resultright_table))) + (((dst_negative_code_multiply_empty_resultright_table) + (dst_negative_scale_multiply_empty_resultright_table)) * S ((dst_negative_code_multiply_empty_resultright_table) + (dst_negative_scale_multiply_empty_resultright_table)) + ((dst_negative_scale_multiply_empty_resultright_table) + (dst_negative_scale_multiply_empty_resultright_table)))))) /\ (forall dst_index_multiply_empty_resultright_table. (exists pvs_le_gap_multiply_empty_resultright_tabledomain. pvs_le_gap_multiply_empty_resultright_tabledomain + (dst_index_multiply_empty_resultright_table) = (0)) -> exists dst_positive_multiply_empty_resultright_table dst_negative_multiply_empty_resultright_table dst_value_multiply_empty_resultright_table. ((((exists ff_h_pvs_multiply_empty_resultright_tableentrypositive. ff_h_pvs_multiply_empty_resultright_tableentrypositive + S (dst_positive_multiply_empty_resultright_table) = S ((S (dst_index_multiply_empty_resultright_table)) * dst_positive_scale_multiply_empty_resultright_table)) /\ exists ff_q_pvs_multiply_empty_resultright_tableentrypositive. dst_positive_code_multiply_empty_resultright_table = ff_q_pvs_multiply_empty_resultright_tableentrypositive * S ((S (dst_index_multiply_empty_resultright_table)) * dst_positive_scale_multiply_empty_resultright_table) + (dst_positive_multiply_empty_resultright_table))) /\ (((((exists ff_h_pvs_multiply_empty_resultright_tableentrynegative. ff_h_pvs_multiply_empty_resultright_tableentrynegative + S (dst_negative_multiply_empty_resultright_table) = S ((S (dst_index_multiply_empty_resultright_table)) * dst_negative_scale_multiply_empty_resultright_table)) /\ exists ff_q_pvs_multiply_empty_resultright_tableentrynegative. dst_negative_code_multiply_empty_resultright_table = ff_q_pvs_multiply_empty_resultright_tableentrynegative * S ((S (dst_index_multiply_empty_resultright_table)) * dst_negative_scale_multiply_empty_resultright_table) + (dst_negative_multiply_empty_resultright_table))) /\ (exists ge_balance_positive_multiply_empty_resultright_tableentryvalue ge_balance_negative_multiply_empty_resultright_tableentryvalue. (((((dst_value_multiply_empty_resultright_table) = 2 * (ge_balance_positive_multiply_empty_resultright_tableentryvalue) /\ (ge_balance_negative_multiply_empty_resultright_tableentryvalue) = 0) \/ exists ge_signed_half_multiply_empty_resultright_tableentryvaluedecode. (((dst_value_multiply_empty_resultright_table) = 2 * ge_signed_half_multiply_empty_resultright_tableentryvaluedecode + 1 /\ (ge_balance_positive_multiply_empty_resultright_tableentryvalue) = 0) /\ (ge_balance_negative_multiply_empty_resultright_tableentryvalue) = S ge_signed_half_multiply_empty_resultright_tableentryvaluedecode))) /\ ((dst_positive_multiply_empty_resultright_table) + ge_balance_negative_multiply_empty_resultright_tableentryvalue = (dst_negative_multiply_empty_resultright_table) + ge_balance_positive_multiply_empty_resultright_tableentryvalue))))))))) /\ (((exists dst_positive_code_multiply_empty_resultoutput_table dst_positive_scale_multiply_empty_resultoutput_table dst_negative_code_multiply_empty_resultoutput_table dst_negative_scale_multiply_empty_resultoutput_table. (((H) = (((((dst_positive_code_multiply_empty_resultoutput_table) + (dst_positive_scale_multiply_empty_resultoutput_table)) * S ((dst_positive_code_multiply_empty_resultoutput_table) + (dst_positive_scale_multiply_empty_resultoutput_table)) + ((dst_positive_scale_multiply_empty_resultoutput_table) + (dst_positive_scale_multiply_empty_resultoutput_table))) + (((dst_negative_code_multiply_empty_resultoutput_table) + (dst_negative_scale_multiply_empty_resultoutput_table)) * S ((dst_negative_code_multiply_empty_resultoutput_table) + (dst_negative_scale_multiply_empty_resultoutput_table)) + ((dst_negative_scale_multiply_empty_resultoutput_table) + (dst_negative_scale_multiply_empty_resultoutput_table)))) * S ((((dst_positive_code_multiply_empty_resultoutput_table) + (dst_positive_scale_multiply_empty_resultoutput_table)) * S ((dst_positive_code_multiply_empty_resultoutput_table) + (dst_positive_scale_multiply_empty_resultoutput_table)) + ((dst_positive_scale_multiply_empty_resultoutput_table) + (dst_positive_scale_multiply_empty_resultoutput_table))) + (((dst_negative_code_multiply_empty_resultoutput_table) + (dst_negative_scale_multiply_empty_resultoutput_table)) * S ((dst_negative_code_multiply_empty_resultoutput_table) + (dst_negative_scale_multiply_empty_resultoutput_table)) + ((dst_negative_scale_multiply_empty_resultoutput_table) + (dst_negative_scale_multiply_empty_resultoutput_table)))) + ((((dst_negative_code_multiply_empty_resultoutput_table) + (dst_negative_scale_multiply_empty_resultoutput_table)) * S ((dst_negative_code_multiply_empty_resultoutput_table) + (dst_negative_scale_multiply_empty_resultoutput_table)) + ((dst_negative_scale_multiply_empty_resultoutput_table) + (dst_negative_scale_multiply_empty_resultoutput_table))) + (((dst_negative_code_multiply_empty_resultoutput_table) + (dst_negative_scale_multiply_empty_resultoutput_table)) * S ((dst_negative_code_multiply_empty_resultoutput_table) + (dst_negative_scale_multiply_empty_resultoutput_table)) + ((dst_negative_scale_multiply_empty_resultoutput_table) + (dst_negative_scale_multiply_empty_resultoutput_table)))))) /\ (forall dst_index_multiply_empty_resultoutput_table. (exists pvs_le_gap_multiply_empty_resultoutput_tabledomain. pvs_le_gap_multiply_empty_resultoutput_tabledomain + (dst_index_multiply_empty_resultoutput_table) = (0)) -> exists dst_positive_multiply_empty_resultoutput_table dst_negative_multiply_empty_resultoutput_table dst_value_multiply_empty_resultoutput_table. ((((exists ff_h_pvs_multiply_empty_resultoutput_tableentrypositive. ff_h_pvs_multiply_empty_resultoutput_tableentrypositive + S (dst_positive_multiply_empty_resultoutput_table) = S ((S (dst_index_multiply_empty_resultoutput_table)) * dst_positive_scale_multiply_empty_resultoutput_table)) /\ exists ff_q_pvs_multiply_empty_resultoutput_tableentrypositive. dst_positive_code_multiply_empty_resultoutput_table = ff_q_pvs_multiply_empty_resultoutput_tableentrypositive * S ((S (dst_index_multiply_empty_resultoutput_table)) * dst_positive_scale_multiply_empty_resultoutput_table) + (dst_positive_multiply_empty_resultoutput_table))) /\ (((((exists ff_h_pvs_multiply_empty_resultoutput_tableentrynegative. ff_h_pvs_multiply_empty_resultoutput_tableentrynegative + S (dst_negative_multiply_empty_resultoutput_table) = S ((S (dst_index_multiply_empty_resultoutput_table)) * dst_negative_scale_multiply_empty_resultoutput_table)) /\ exists ff_q_pvs_multiply_empty_resultoutput_tableentrynegative. dst_negative_code_multiply_empty_resultoutput_table = ff_q_pvs_multiply_empty_resultoutput_tableentrynegative * S ((S (dst_index_multiply_empty_resultoutput_table)) * dst_negative_scale_multiply_empty_resultoutput_table) + (dst_negative_multiply_empty_resultoutput_table))) /\ (exists ge_balance_positive_multiply_empty_resultoutput_tableentryvalue ge_balance_negative_multiply_empty_resultoutput_tableentryvalue. (((((dst_value_multiply_empty_resultoutput_table) = 2 * (ge_balance_positive_multiply_empty_resultoutput_tableentryvalue) /\ (ge_balance_negative_multiply_empty_resultoutput_tableentryvalue) = 0) \/ exists ge_signed_half_multiply_empty_resultoutput_tableentryvaluedecode. (((dst_value_multiply_empty_resultoutput_table) = 2 * ge_signed_half_multiply_empty_resultoutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_multiply_empty_resultoutput_tableentryvalue) = 0) /\ (ge_balance_negative_multiply_empty_resultoutput_tableentryvalue) = S ge_signed_half_multiply_empty_resultoutput_tableentryvaluedecode))) /\ ((dst_positive_multiply_empty_resultoutput_table) + ge_balance_negative_multiply_empty_resultoutput_tableentryvalue = (dst_negative_multiply_empty_resultoutput_table) + ge_balance_positive_multiply_empty_resultoutput_tableentryvalue))))))))) /\ (forall sto_index_multiply_empty_resultentries. (exists pvs_gap_multiply_empty_resultentriesbound. pvs_gap_multiply_empty_resultentriesbound + S (sto_index_multiply_empty_resultentries) = (0)) -> exists sto_left_multiply_empty_resultentries sto_right_multiply_empty_resultentries sto_output_multiply_empty_resultentries. ((exists dst_positive_code_multiply_empty_resultentriesentryleft dst_positive_scale_multiply_empty_resultentriesentryleft dst_negative_code_multiply_empty_resultentriesentryleft dst_negative_scale_multiply_empty_resultentriesentryleft dst_positive_multiply_empty_resultentriesentryleft dst_negative_multiply_empty_resultentriesentryleft. (((F) = (((((dst_positive_code_multiply_empty_resultentriesentryleft) + (dst_positive_scale_multiply_empty_resultentriesentryleft)) * S ((dst_positive_code_multiply_empty_resultentriesentryleft) + (dst_positive_scale_multiply_empty_resultentriesentryleft)) + ((dst_positive_scale_multiply_empty_resultentriesentryleft) + (dst_positive_scale_multiply_empty_resultentriesentryleft))) + (((dst_negative_code_multiply_empty_resultentriesentryleft) + (dst_negative_scale_multiply_empty_resultentriesentryleft)) * S ((dst_negative_code_multiply_empty_resultentriesentryleft) + (dst_negative_scale_multiply_empty_resultentriesentryleft)) + ((dst_negative_scale_multiply_empty_resultentriesentryleft) + (dst_negative_scale_multiply_empty_resultentriesentryleft)))) * S ((((dst_positive_code_multiply_empty_resultentriesentryleft) + (dst_positive_scale_multiply_empty_resultentriesentryleft)) * S ((dst_positive_code_multiply_empty_resultentriesentryleft) + (dst_positive_scale_multiply_empty_resultentriesentryleft)) + ((dst_positive_scale_multiply_empty_resultentriesentryleft) + (dst_positive_scale_multiply_empty_resultentriesentryleft))) + (((dst_negative_code_multiply_empty_resultentriesentryleft) + (dst_negative_scale_multiply_empty_resultentriesentryleft)) * S ((dst_negative_code_multiply_empty_resultentriesentryleft) + (dst_negative_scale_multiply_empty_resultentriesentryleft)) + ((dst_negative_scale_multiply_empty_resultentriesentryleft) + (dst_negative_scale_multiply_empty_resultentriesentryleft)))) + ((((dst_negative_code_multiply_empty_resultentriesentryleft) + (dst_negative_scale_multiply_empty_resultentriesentryleft)) * S ((dst_negative_code_multiply_empty_resultentriesentryleft) + (dst_negative_scale_multiply_empty_resultentriesentryleft)) + ((dst_negative_scale_multiply_empty_resultentriesentryleft) + (dst_negative_scale_multiply_empty_resultentriesentryleft))) + (((dst_negative_code_multiply_empty_resultentriesentryleft) + (dst_negative_scale_multiply_empty_resultentriesentryleft)) * S ((dst_negative_code_multiply_empty_resultentriesentryleft) + (dst_negative_scale_multiply_empty_resultentriesentryleft)) + ((dst_negative_scale_multiply_empty_resultentriesentryleft) + (dst_negative_scale_multiply_empty_resultentriesentryleft)))))) /\ (((((exists ff_h_pvs_multiply_empty_resultentriesentryleftpositive. ff_h_pvs_multiply_empty_resultentriesentryleftpositive + S (dst_positive_multiply_empty_resultentriesentryleft) = S ((S (sto_index_multiply_empty_resultentries)) * dst_positive_scale_multiply_empty_resultentriesentryleft)) /\ exists ff_q_pvs_multiply_empty_resultentriesentryleftpositive. dst_positive_code_multiply_empty_resultentriesentryleft = ff_q_pvs_multiply_empty_resultentriesentryleftpositive * S ((S (sto_index_multiply_empty_resultentries)) * dst_positive_scale_multiply_empty_resultentriesentryleft) + (dst_positive_multiply_empty_resultentriesentryleft))) /\ (((((exists ff_h_pvs_multiply_empty_resultentriesentryleftnegative. ff_h_pvs_multiply_empty_resultentriesentryleftnegative + S (dst_negative_multiply_empty_resultentriesentryleft) = S ((S (sto_index_multiply_empty_resultentries)) * dst_negative_scale_multiply_empty_resultentriesentryleft)) /\ exists ff_q_pvs_multiply_empty_resultentriesentryleftnegative. dst_negative_code_multiply_empty_resultentriesentryleft = ff_q_pvs_multiply_empty_resultentriesentryleftnegative * S ((S (sto_index_multiply_empty_resultentries)) * dst_negative_scale_multiply_empty_resultentriesentryleft) + (dst_negative_multiply_empty_resultentriesentryleft))) /\ (exists ge_balance_positive_multiply_empty_resultentriesentryleftvalue ge_balance_negative_multiply_empty_resultentriesentryleftvalue. (((((sto_left_multiply_empty_resultentries) = 2 * (ge_balance_positive_multiply_empty_resultentriesentryleftvalue) /\ (ge_balance_negative_multiply_empty_resultentriesentryleftvalue) = 0) \/ exists ge_signed_half_multiply_empty_resultentriesentryleftvaluedecode. (((sto_left_multiply_empty_resultentries) = 2 * ge_signed_half_multiply_empty_resultentriesentryleftvaluedecode + 1 /\ (ge_balance_positive_multiply_empty_resultentriesentryleftvalue) = 0) /\ (ge_balance_negative_multiply_empty_resultentriesentryleftvalue) = S ge_signed_half_multiply_empty_resultentriesentryleftvaluedecode))) /\ ((dst_positive_multiply_empty_resultentriesentryleft) + ge_balance_negative_multiply_empty_resultentriesentryleftvalue = (dst_negative_multiply_empty_resultentriesentryleft) + ge_balance_positive_multiply_empty_resultentriesentryleftvalue))))))))) /\ (((exists dst_positive_code_multiply_empty_resultentriesentryright dst_positive_scale_multiply_empty_resultentriesentryright dst_negative_code_multiply_empty_resultentriesentryright dst_negative_scale_multiply_empty_resultentriesentryright dst_positive_multiply_empty_resultentriesentryright dst_negative_multiply_empty_resultentriesentryright. (((G) = (((((dst_positive_code_multiply_empty_resultentriesentryright) + (dst_positive_scale_multiply_empty_resultentriesentryright)) * S ((dst_positive_code_multiply_empty_resultentriesentryright) + (dst_positive_scale_multiply_empty_resultentriesentryright)) + ((dst_positive_scale_multiply_empty_resultentriesentryright) + (dst_positive_scale_multiply_empty_resultentriesentryright))) + (((dst_negative_code_multiply_empty_resultentriesentryright) + (dst_negative_scale_multiply_empty_resultentriesentryright)) * S ((dst_negative_code_multiply_empty_resultentriesentryright) + (dst_negative_scale_multiply_empty_resultentriesentryright)) + ((dst_negative_scale_multiply_empty_resultentriesentryright) + (dst_negative_scale_multiply_empty_resultentriesentryright)))) * S ((((dst_positive_code_multiply_empty_resultentriesentryright) + (dst_positive_scale_multiply_empty_resultentriesentryright)) * S ((dst_positive_code_multiply_empty_resultentriesentryright) + (dst_positive_scale_multiply_empty_resultentriesentryright)) + ((dst_positive_scale_multiply_empty_resultentriesentryright) + (dst_positive_scale_multiply_empty_resultentriesentryright))) + (((dst_negative_code_multiply_empty_resultentriesentryright) + (dst_negative_scale_multiply_empty_resultentriesentryright)) * S ((dst_negative_code_multiply_empty_resultentriesentryright) + (dst_negative_scale_multiply_empty_resultentriesentryright)) + ((dst_negative_scale_multiply_empty_resultentriesentryright) + (dst_negative_scale_multiply_empty_resultentriesentryright)))) + ((((dst_negative_code_multiply_empty_resultentriesentryright) + (dst_negative_scale_multiply_empty_resultentriesentryright)) * S ((dst_negative_code_multiply_empty_resultentriesentryright) + (dst_negative_scale_multiply_empty_resultentriesentryright)) + ((dst_negative_scale_multiply_empty_resultentriesentryright) + (dst_negative_scale_multiply_empty_resultentriesentryright))) + (((dst_negative_code_multiply_empty_resultentriesentryright) + (dst_negative_scale_multiply_empty_resultentriesentryright)) * S ((dst_negative_code_multiply_empty_resultentriesentryright) + (dst_negative_scale_multiply_empty_resultentriesentryright)) + ((dst_negative_scale_multiply_empty_resultentriesentryright) + (dst_negative_scale_multiply_empty_resultentriesentryright)))))) /\ (((((exists ff_h_pvs_multiply_empty_resultentriesentryrightpositive. ff_h_pvs_multiply_empty_resultentriesentryrightpositive + S (dst_positive_multiply_empty_resultentriesentryright) = S ((S (sto_index_multiply_empty_resultentries)) * dst_positive_scale_multiply_empty_resultentriesentryright)) /\ exists ff_q_pvs_multiply_empty_resultentriesentryrightpositive. dst_positive_code_multiply_empty_resultentriesentryright = ff_q_pvs_multiply_empty_resultentriesentryrightpositive * S ((S (sto_index_multiply_empty_resultentries)) * dst_positive_scale_multiply_empty_resultentriesentryright) + (dst_positive_multiply_empty_resultentriesentryright))) /\ (((((exists ff_h_pvs_multiply_empty_resultentriesentryrightnegative. ff_h_pvs_multiply_empty_resultentriesentryrightnegative + S (dst_negative_multiply_empty_resultentriesentryright) = S ((S (sto_index_multiply_empty_resultentries)) * dst_negative_scale_multiply_empty_resultentriesentryright)) /\ exists ff_q_pvs_multiply_empty_resultentriesentryrightnegative. dst_negative_code_multiply_empty_resultentriesentryright = ff_q_pvs_multiply_empty_resultentriesentryrightnegative * S ((S (sto_index_multiply_empty_resultentries)) * dst_negative_scale_multiply_empty_resultentriesentryright) + (dst_negative_multiply_empty_resultentriesentryright))) /\ (exists ge_balance_positive_multiply_empty_resultentriesentryrightvalue ge_balance_negative_multiply_empty_resultentriesentryrightvalue. (((((sto_right_multiply_empty_resultentries) = 2 * (ge_balance_positive_multiply_empty_resultentriesentryrightvalue) /\ (ge_balance_negative_multiply_empty_resultentriesentryrightvalue) = 0) \/ exists ge_signed_half_multiply_empty_resultentriesentryrightvaluedecode. (((sto_right_multiply_empty_resultentries) = 2 * ge_signed_half_multiply_empty_resultentriesentryrightvaluedecode + 1 /\ (ge_balance_positive_multiply_empty_resultentriesentryrightvalue) = 0) /\ (ge_balance_negative_multiply_empty_resultentriesentryrightvalue) = S ge_signed_half_multiply_empty_resultentriesentryrightvaluedecode))) /\ ((dst_positive_multiply_empty_resultentriesentryright) + ge_balance_negative_multiply_empty_resultentriesentryrightvalue = (dst_negative_multiply_empty_resultentriesentryright) + ge_balance_positive_multiply_empty_resultentriesentryrightvalue))))))))) /\ (((exists dst_positive_code_multiply_empty_resultentriesentryoutput dst_positive_scale_multiply_empty_resultentriesentryoutput dst_negative_code_multiply_empty_resultentriesentryoutput dst_negative_scale_multiply_empty_resultentriesentryoutput dst_positive_multiply_empty_resultentriesentryoutput dst_negative_multiply_empty_resultentriesentryoutput. (((H) = (((((dst_positive_code_multiply_empty_resultentriesentryoutput) + (dst_positive_scale_multiply_empty_resultentriesentryoutput)) * S ((dst_positive_code_multiply_empty_resultentriesentryoutput) + (dst_positive_scale_multiply_empty_resultentriesentryoutput)) + ((dst_positive_scale_multiply_empty_resultentriesentryoutput) + (dst_positive_scale_multiply_empty_resultentriesentryoutput))) + (((dst_negative_code_multiply_empty_resultentriesentryoutput) + (dst_negative_scale_multiply_empty_resultentriesentryoutput)) * S ((dst_negative_code_multiply_empty_resultentriesentryoutput) + (dst_negative_scale_multiply_empty_resultentriesentryoutput)) + ((dst_negative_scale_multiply_empty_resultentriesentryoutput) + (dst_negative_scale_multiply_empty_resultentriesentryoutput)))) * S ((((dst_positive_code_multiply_empty_resultentriesentryoutput) + (dst_positive_scale_multiply_empty_resultentriesentryoutput)) * S ((dst_positive_code_multiply_empty_resultentriesentryoutput) + (dst_positive_scale_multiply_empty_resultentriesentryoutput)) + ((dst_positive_scale_multiply_empty_resultentriesentryoutput) + (dst_positive_scale_multiply_empty_resultentriesentryoutput))) + (((dst_negative_code_multiply_empty_resultentriesentryoutput) + (dst_negative_scale_multiply_empty_resultentriesentryoutput)) * S ((dst_negative_code_multiply_empty_resultentriesentryoutput) + (dst_negative_scale_multiply_empty_resultentriesentryoutput)) + ((dst_negative_scale_multiply_empty_resultentriesentryoutput) + (dst_negative_scale_multiply_empty_resultentriesentryoutput)))) + ((((dst_negative_code_multiply_empty_resultentriesentryoutput) + (dst_negative_scale_multiply_empty_resultentriesentryoutput)) * S ((dst_negative_code_multiply_empty_resultentriesentryoutput) + (dst_negative_scale_multiply_empty_resultentriesentryoutput)) + ((dst_negative_scale_multiply_empty_resultentriesentryoutput) + (dst_negative_scale_multiply_empty_resultentriesentryoutput))) + (((dst_negative_code_multiply_empty_resultentriesentryoutput) + (dst_negative_scale_multiply_empty_resultentriesentryoutput)) * S ((dst_negative_code_multiply_empty_resultentriesentryoutput) + (dst_negative_scale_multiply_empty_resultentriesentryoutput)) + ((dst_negative_scale_multiply_empty_resultentriesentryoutput) + (dst_negative_scale_multiply_empty_resultentriesentryoutput)))))) /\ (((((exists ff_h_pvs_multiply_empty_resultentriesentryoutputpositive. ff_h_pvs_multiply_empty_resultentriesentryoutputpositive + S (dst_positive_multiply_empty_resultentriesentryoutput) = S ((S (sto_index_multiply_empty_resultentries)) * dst_positive_scale_multiply_empty_resultentriesentryoutput)) /\ exists ff_q_pvs_multiply_empty_resultentriesentryoutputpositive. dst_positive_code_multiply_empty_resultentriesentryoutput = ff_q_pvs_multiply_empty_resultentriesentryoutputpositive * S ((S (sto_index_multiply_empty_resultentries)) * dst_positive_scale_multiply_empty_resultentriesentryoutput) + (dst_positive_multiply_empty_resultentriesentryoutput))) /\ (((((exists ff_h_pvs_multiply_empty_resultentriesentryoutputnegative. ff_h_pvs_multiply_empty_resultentriesentryoutputnegative + S (dst_negative_multiply_empty_resultentriesentryoutput) = S ((S (sto_index_multiply_empty_resultentries)) * dst_negative_scale_multiply_empty_resultentriesentryoutput)) /\ exists ff_q_pvs_multiply_empty_resultentriesentryoutputnegative. dst_negative_code_multiply_empty_resultentriesentryoutput = ff_q_pvs_multiply_empty_resultentriesentryoutputnegative * S ((S (sto_index_multiply_empty_resultentries)) * dst_negative_scale_multiply_empty_resultentriesentryoutput) + (dst_negative_multiply_empty_resultentriesentryoutput))) /\ (exists ge_balance_positive_multiply_empty_resultentriesentryoutputvalue ge_balance_negative_multiply_empty_resultentriesentryoutputvalue. (((((sto_output_multiply_empty_resultentries) = 2 * (ge_balance_positive_multiply_empty_resultentriesentryoutputvalue) /\ (ge_balance_negative_multiply_empty_resultentriesentryoutputvalue) = 0) \/ exists ge_signed_half_multiply_empty_resultentriesentryoutputvaluedecode. (((sto_output_multiply_empty_resultentries) = 2 * ge_signed_half_multiply_empty_resultentriesentryoutputvaluedecode + 1 /\ (ge_balance_positive_multiply_empty_resultentriesentryoutputvalue) = 0) /\ (ge_balance_negative_multiply_empty_resultentriesentryoutputvalue) = S ge_signed_half_multiply_empty_resultentriesentryoutputvaluedecode))) /\ ((dst_positive_multiply_empty_resultentriesentryoutput) + ge_balance_negative_multiply_empty_resultentriesentryoutputvalue = (dst_negative_multiply_empty_resultentriesentryoutput) + ge_balance_positive_multiply_empty_resultentriesentryoutputvalue))))))))) /\ (exists sto_ap_multiply_empty_resultentriesentryoperation sto_an_multiply_empty_resultentriesentryoperation sto_bp_multiply_empty_resultentriesentryoperation sto_bn_multiply_empty_resultentriesentryoperation sto_cp_multiply_empty_resultentriesentryoperation sto_cn_multiply_empty_resultentriesentryoperation. (((((sto_left_multiply_empty_resultentries) = 2 * (sto_ap_multiply_empty_resultentriesentryoperation) /\ (sto_an_multiply_empty_resultentriesentryoperation) = 0) \/ exists ge_signed_half_multiply_empty_resultentriesentryoperationleft. (((sto_left_multiply_empty_resultentries) = 2 * ge_signed_half_multiply_empty_resultentriesentryoperationleft + 1 /\ (sto_ap_multiply_empty_resultentriesentryoperation) = 0) /\ (sto_an_multiply_empty_resultentriesentryoperation) = S ge_signed_half_multiply_empty_resultentriesentryoperationleft))) /\ ((((((sto_right_multiply_empty_resultentries) = 2 * (sto_bp_multiply_empty_resultentriesentryoperation) /\ (sto_bn_multiply_empty_resultentriesentryoperation) = 0) \/ exists ge_signed_half_multiply_empty_resultentriesentryoperationright. (((sto_right_multiply_empty_resultentries) = 2 * ge_signed_half_multiply_empty_resultentriesentryoperationright + 1 /\ (sto_bp_multiply_empty_resultentriesentryoperation) = 0) /\ (sto_bn_multiply_empty_resultentriesentryoperation) = S ge_signed_half_multiply_empty_resultentriesentryoperationright))) /\ ((((((sto_output_multiply_empty_resultentries) = 2 * (sto_cp_multiply_empty_resultentriesentryoperation) /\ (sto_cn_multiply_empty_resultentriesentryoperation) = 0) \/ exists ge_signed_half_multiply_empty_resultentriesentryoperationoutput. (((sto_output_multiply_empty_resultentries) = 2 * ge_signed_half_multiply_empty_resultentriesentryoperationoutput + 1 /\ (sto_cp_multiply_empty_resultentriesentryoperation) = 0) /\ (sto_cn_multiply_empty_resultentriesentryoperation) = S ge_signed_half_multiply_empty_resultentriesentryoperationoutput))) /\ ((sto_ap_multiply_empty_resultentriesentryoperation * sto_bp_multiply_empty_resultentriesentryoperation + sto_an_multiply_empty_resultentriesentryoperation * sto_bn_multiply_empty_resultentriesentryoperation) + sto_cn_multiply_empty_resultentriesentryoperation = (sto_ap_multiply_empty_resultentriesentryoperation * sto_bn_multiply_empty_resultentriesentryoperation + sto_an_multiply_empty_resultentriesentryoperation * sto_bp_multiply_empty_resultentriesentryoperation) + sto_cp_multiply_empty_resultentriesentryoperation)))))))))))))))))))