Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.
Exact expanded first-order arithmetic statement
forall F G H K l a b c. (((exists dst_positive_code_multiply_extend_sourceleft_table dst_positive_scale_multiply_extend_sourceleft_table dst_negative_code_multiply_extend_sourceleft_table dst_negative_scale_multiply_extend_sourceleft_table. (((F) = (((((dst_positive_code_multiply_extend_sourceleft_table) + (dst_positive_scale_multiply_extend_sourceleft_table)) * S ((dst_positive_code_multiply_extend_sourceleft_table) + (dst_positive_scale_multiply_extend_sourceleft_table)) + ((dst_positive_scale_multiply_extend_sourceleft_table) + (dst_positive_scale_multiply_extend_sourceleft_table))) + (((dst_negative_code_multiply_extend_sourceleft_table) + (dst_negative_scale_multiply_extend_sourceleft_table)) * S ((dst_negative_code_multiply_extend_sourceleft_table) + (dst_negative_scale_multiply_extend_sourceleft_table)) + ((dst_negative_scale_multiply_extend_sourceleft_table) + (dst_negative_scale_multiply_extend_sourceleft_table)))) * S ((((dst_positive_code_multiply_extend_sourceleft_table) + (dst_positive_scale_multiply_extend_sourceleft_table)) * S ((dst_positive_code_multiply_extend_sourceleft_table) + (dst_positive_scale_multiply_extend_sourceleft_table)) + ((dst_positive_scale_multiply_extend_sourceleft_table) + (dst_positive_scale_multiply_extend_sourceleft_table))) + (((dst_negative_code_multiply_extend_sourceleft_table) + (dst_negative_scale_multiply_extend_sourceleft_table)) * S ((dst_negative_code_multiply_extend_sourceleft_table) + (dst_negative_scale_multiply_extend_sourceleft_table)) + ((dst_negative_scale_multiply_extend_sourceleft_table) + (dst_negative_scale_multiply_extend_sourceleft_table)))) + ((((dst_negative_code_multiply_extend_sourceleft_table) + (dst_negative_scale_multiply_extend_sourceleft_table)) * S ((dst_negative_code_multiply_extend_sourceleft_table) + (dst_negative_scale_multiply_extend_sourceleft_table)) + ((dst_negative_scale_multiply_extend_sourceleft_table) + (dst_negative_scale_multiply_extend_sourceleft_table))) + (((dst_negative_code_multiply_extend_sourceleft_table) + (dst_negative_scale_multiply_extend_sourceleft_table)) * S ((dst_negative_code_multiply_extend_sourceleft_table) + (dst_negative_scale_multiply_extend_sourceleft_table)) + ((dst_negative_scale_multiply_extend_sourceleft_table) + (dst_negative_scale_multiply_extend_sourceleft_table)))))) /\ (forall dst_index_multiply_extend_sourceleft_table. (exists pvs_le_gap_multiply_extend_sourceleft_tabledomain. pvs_le_gap_multiply_extend_sourceleft_tabledomain + (dst_index_multiply_extend_sourceleft_table) = (l)) -> exists dst_positive_multiply_extend_sourceleft_table dst_negative_multiply_extend_sourceleft_table dst_value_multiply_extend_sourceleft_table. ((((exists ff_h_pvs_multiply_extend_sourceleft_tableentrypositive. ff_h_pvs_multiply_extend_sourceleft_tableentrypositive + S (dst_positive_multiply_extend_sourceleft_table) = S ((S (dst_index_multiply_extend_sourceleft_table)) * dst_positive_scale_multiply_extend_sourceleft_table)) /\ exists ff_q_pvs_multiply_extend_sourceleft_tableentrypositive. dst_positive_code_multiply_extend_sourceleft_table = ff_q_pvs_multiply_extend_sourceleft_tableentrypositive * S ((S (dst_index_multiply_extend_sourceleft_table)) * dst_positive_scale_multiply_extend_sourceleft_table) + (dst_positive_multiply_extend_sourceleft_table))) /\ (((((exists ff_h_pvs_multiply_extend_sourceleft_tableentrynegative. ff_h_pvs_multiply_extend_sourceleft_tableentrynegative + S (dst_negative_multiply_extend_sourceleft_table) = S ((S (dst_index_multiply_extend_sourceleft_table)) * dst_negative_scale_multiply_extend_sourceleft_table)) /\ exists ff_q_pvs_multiply_extend_sourceleft_tableentrynegative. dst_negative_code_multiply_extend_sourceleft_table = ff_q_pvs_multiply_extend_sourceleft_tableentrynegative * S ((S (dst_index_multiply_extend_sourceleft_table)) * dst_negative_scale_multiply_extend_sourceleft_table) + (dst_negative_multiply_extend_sourceleft_table))) /\ (exists ge_balance_positive_multiply_extend_sourceleft_tableentryvalue ge_balance_negative_multiply_extend_sourceleft_tableentryvalue. (((((dst_value_multiply_extend_sourceleft_table) = 2 * (ge_balance_positive_multiply_extend_sourceleft_tableentryvalue) /\ (ge_balance_negative_multiply_extend_sourceleft_tableentryvalue) = 0) \/ exists ge_signed_half_multiply_extend_sourceleft_tableentryvaluedecode. (((dst_value_multiply_extend_sourceleft_table) = 2 * ge_signed_half_multiply_extend_sourceleft_tableentryvaluedecode + 1 /\ (ge_balance_positive_multiply_extend_sourceleft_tableentryvalue) = 0) /\ (ge_balance_negative_multiply_extend_sourceleft_tableentryvalue) = S ge_signed_half_multiply_extend_sourceleft_tableentryvaluedecode))) /\ ((dst_positive_multiply_extend_sourceleft_table) + ge_balance_negative_multiply_extend_sourceleft_tableentryvalue = (dst_negative_multiply_extend_sourceleft_table) + ge_balance_positive_multiply_extend_sourceleft_tableentryvalue))))))))) /\ (((exists dst_positive_code_multiply_extend_sourceright_table dst_positive_scale_multiply_extend_sourceright_table dst_negative_code_multiply_extend_sourceright_table dst_negative_scale_multiply_extend_sourceright_table. (((G) = (((((dst_positive_code_multiply_extend_sourceright_table) + (dst_positive_scale_multiply_extend_sourceright_table)) * S ((dst_positive_code_multiply_extend_sourceright_table) + (dst_positive_scale_multiply_extend_sourceright_table)) + ((dst_positive_scale_multiply_extend_sourceright_table) + (dst_positive_scale_multiply_extend_sourceright_table))) + (((dst_negative_code_multiply_extend_sourceright_table) + (dst_negative_scale_multiply_extend_sourceright_table)) * S ((dst_negative_code_multiply_extend_sourceright_table) + (dst_negative_scale_multiply_extend_sourceright_table)) + ((dst_negative_scale_multiply_extend_sourceright_table) + (dst_negative_scale_multiply_extend_sourceright_table)))) * S ((((dst_positive_code_multiply_extend_sourceright_table) + (dst_positive_scale_multiply_extend_sourceright_table)) * S ((dst_positive_code_multiply_extend_sourceright_table) + (dst_positive_scale_multiply_extend_sourceright_table)) + ((dst_positive_scale_multiply_extend_sourceright_table) + (dst_positive_scale_multiply_extend_sourceright_table))) + (((dst_negative_code_multiply_extend_sourceright_table) + (dst_negative_scale_multiply_extend_sourceright_table)) * S ((dst_negative_code_multiply_extend_sourceright_table) + (dst_negative_scale_multiply_extend_sourceright_table)) + ((dst_negative_scale_multiply_extend_sourceright_table) + (dst_negative_scale_multiply_extend_sourceright_table)))) + ((((dst_negative_code_multiply_extend_sourceright_table) + (dst_negative_scale_multiply_extend_sourceright_table)) * S ((dst_negative_code_multiply_extend_sourceright_table) + (dst_negative_scale_multiply_extend_sourceright_table)) + ((dst_negative_scale_multiply_extend_sourceright_table) + (dst_negative_scale_multiply_extend_sourceright_table))) + (((dst_negative_code_multiply_extend_sourceright_table) + (dst_negative_scale_multiply_extend_sourceright_table)) * S ((dst_negative_code_multiply_extend_sourceright_table) + (dst_negative_scale_multiply_extend_sourceright_table)) + ((dst_negative_scale_multiply_extend_sourceright_table) + (dst_negative_scale_multiply_extend_sourceright_table)))))) /\ (forall dst_index_multiply_extend_sourceright_table. (exists pvs_le_gap_multiply_extend_sourceright_tabledomain. pvs_le_gap_multiply_extend_sourceright_tabledomain + (dst_index_multiply_extend_sourceright_table) = (l)) -> exists dst_positive_multiply_extend_sourceright_table dst_negative_multiply_extend_sourceright_table dst_value_multiply_extend_sourceright_table. ((((exists ff_h_pvs_multiply_extend_sourceright_tableentrypositive. ff_h_pvs_multiply_extend_sourceright_tableentrypositive + S (dst_positive_multiply_extend_sourceright_table) = S ((S (dst_index_multiply_extend_sourceright_table)) * dst_positive_scale_multiply_extend_sourceright_table)) /\ exists ff_q_pvs_multiply_extend_sourceright_tableentrypositive. dst_positive_code_multiply_extend_sourceright_table = ff_q_pvs_multiply_extend_sourceright_tableentrypositive * S ((S (dst_index_multiply_extend_sourceright_table)) * dst_positive_scale_multiply_extend_sourceright_table) + (dst_positive_multiply_extend_sourceright_table))) /\ (((((exists ff_h_pvs_multiply_extend_sourceright_tableentrynegative. ff_h_pvs_multiply_extend_sourceright_tableentrynegative + S (dst_negative_multiply_extend_sourceright_table) = S ((S (dst_index_multiply_extend_sourceright_table)) * dst_negative_scale_multiply_extend_sourceright_table)) /\ exists ff_q_pvs_multiply_extend_sourceright_tableentrynegative. dst_negative_code_multiply_extend_sourceright_table = ff_q_pvs_multiply_extend_sourceright_tableentrynegative * S ((S (dst_index_multiply_extend_sourceright_table)) * dst_negative_scale_multiply_extend_sourceright_table) + (dst_negative_multiply_extend_sourceright_table))) /\ (exists ge_balance_positive_multiply_extend_sourceright_tableentryvalue ge_balance_negative_multiply_extend_sourceright_tableentryvalue. (((((dst_value_multiply_extend_sourceright_table) = 2 * (ge_balance_positive_multiply_extend_sourceright_tableentryvalue) /\ (ge_balance_negative_multiply_extend_sourceright_tableentryvalue) = 0) \/ exists ge_signed_half_multiply_extend_sourceright_tableentryvaluedecode. (((dst_value_multiply_extend_sourceright_table) = 2 * ge_signed_half_multiply_extend_sourceright_tableentryvaluedecode + 1 /\ (ge_balance_positive_multiply_extend_sourceright_tableentryvalue) = 0) /\ (ge_balance_negative_multiply_extend_sourceright_tableentryvalue) = S ge_signed_half_multiply_extend_sourceright_tableentryvaluedecode))) /\ ((dst_positive_multiply_extend_sourceright_table) + ge_balance_negative_multiply_extend_sourceright_tableentryvalue = (dst_negative_multiply_extend_sourceright_table) + ge_balance_positive_multiply_extend_sourceright_tableentryvalue))))))))) /\ (((exists dst_positive_code_multiply_extend_sourceoutput_table dst_positive_scale_multiply_extend_sourceoutput_table dst_negative_code_multiply_extend_sourceoutput_table dst_negative_scale_multiply_extend_sourceoutput_table. (((H) = (((((dst_positive_code_multiply_extend_sourceoutput_table) + (dst_positive_scale_multiply_extend_sourceoutput_table)) * S ((dst_positive_code_multiply_extend_sourceoutput_table) + (dst_positive_scale_multiply_extend_sourceoutput_table)) + ((dst_positive_scale_multiply_extend_sourceoutput_table) + (dst_positive_scale_multiply_extend_sourceoutput_table))) + (((dst_negative_code_multiply_extend_sourceoutput_table) + (dst_negative_scale_multiply_extend_sourceoutput_table)) * S ((dst_negative_code_multiply_extend_sourceoutput_table) + (dst_negative_scale_multiply_extend_sourceoutput_table)) + ((dst_negative_scale_multiply_extend_sourceoutput_table) + (dst_negative_scale_multiply_extend_sourceoutput_table)))) * S ((((dst_positive_code_multiply_extend_sourceoutput_table) + (dst_positive_scale_multiply_extend_sourceoutput_table)) * S ((dst_positive_code_multiply_extend_sourceoutput_table) + (dst_positive_scale_multiply_extend_sourceoutput_table)) + ((dst_positive_scale_multiply_extend_sourceoutput_table) + (dst_positive_scale_multiply_extend_sourceoutput_table))) + (((dst_negative_code_multiply_extend_sourceoutput_table) + (dst_negative_scale_multiply_extend_sourceoutput_table)) * S ((dst_negative_code_multiply_extend_sourceoutput_table) + (dst_negative_scale_multiply_extend_sourceoutput_table)) + ((dst_negative_scale_multiply_extend_sourceoutput_table) + (dst_negative_scale_multiply_extend_sourceoutput_table)))) + ((((dst_negative_code_multiply_extend_sourceoutput_table) + (dst_negative_scale_multiply_extend_sourceoutput_table)) * S ((dst_negative_code_multiply_extend_sourceoutput_table) + (dst_negative_scale_multiply_extend_sourceoutput_table)) + ((dst_negative_scale_multiply_extend_sourceoutput_table) + (dst_negative_scale_multiply_extend_sourceoutput_table))) + (((dst_negative_code_multiply_extend_sourceoutput_table) + (dst_negative_scale_multiply_extend_sourceoutput_table)) * S ((dst_negative_code_multiply_extend_sourceoutput_table) + (dst_negative_scale_multiply_extend_sourceoutput_table)) + ((dst_negative_scale_multiply_extend_sourceoutput_table) + (dst_negative_scale_multiply_extend_sourceoutput_table)))))) /\ (forall dst_index_multiply_extend_sourceoutput_table. (exists pvs_le_gap_multiply_extend_sourceoutput_tabledomain. pvs_le_gap_multiply_extend_sourceoutput_tabledomain + (dst_index_multiply_extend_sourceoutput_table) = (l)) -> exists dst_positive_multiply_extend_sourceoutput_table dst_negative_multiply_extend_sourceoutput_table dst_value_multiply_extend_sourceoutput_table. ((((exists ff_h_pvs_multiply_extend_sourceoutput_tableentrypositive. ff_h_pvs_multiply_extend_sourceoutput_tableentrypositive + S (dst_positive_multiply_extend_sourceoutput_table) = S ((S (dst_index_multiply_extend_sourceoutput_table)) * dst_positive_scale_multiply_extend_sourceoutput_table)) /\ exists ff_q_pvs_multiply_extend_sourceoutput_tableentrypositive. dst_positive_code_multiply_extend_sourceoutput_table = ff_q_pvs_multiply_extend_sourceoutput_tableentrypositive * S ((S (dst_index_multiply_extend_sourceoutput_table)) * dst_positive_scale_multiply_extend_sourceoutput_table) + (dst_positive_multiply_extend_sourceoutput_table))) /\ (((((exists ff_h_pvs_multiply_extend_sourceoutput_tableentrynegative. ff_h_pvs_multiply_extend_sourceoutput_tableentrynegative + S (dst_negative_multiply_extend_sourceoutput_table) = S ((S (dst_index_multiply_extend_sourceoutput_table)) * dst_negative_scale_multiply_extend_sourceoutput_table)) /\ exists ff_q_pvs_multiply_extend_sourceoutput_tableentrynegative. dst_negative_code_multiply_extend_sourceoutput_table = ff_q_pvs_multiply_extend_sourceoutput_tableentrynegative * S ((S (dst_index_multiply_extend_sourceoutput_table)) * dst_negative_scale_multiply_extend_sourceoutput_table) + (dst_negative_multiply_extend_sourceoutput_table))) /\ (exists ge_balance_positive_multiply_extend_sourceoutput_tableentryvalue ge_balance_negative_multiply_extend_sourceoutput_tableentryvalue. (((((dst_value_multiply_extend_sourceoutput_table) = 2 * (ge_balance_positive_multiply_extend_sourceoutput_tableentryvalue) /\ (ge_balance_negative_multiply_extend_sourceoutput_tableentryvalue) = 0) \/ exists ge_signed_half_multiply_extend_sourceoutput_tableentryvaluedecode. (((dst_value_multiply_extend_sourceoutput_table) = 2 * ge_signed_half_multiply_extend_sourceoutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_multiply_extend_sourceoutput_tableentryvalue) = 0) /\ (ge_balance_negative_multiply_extend_sourceoutput_tableentryvalue) = S ge_signed_half_multiply_extend_sourceoutput_tableentryvaluedecode))) /\ ((dst_positive_multiply_extend_sourceoutput_table) + ge_balance_negative_multiply_extend_sourceoutput_tableentryvalue = (dst_negative_multiply_extend_sourceoutput_table) + ge_balance_positive_multiply_extend_sourceoutput_tableentryvalue))))))))) /\ (forall sto_index_multiply_extend_sourceentries. (exists pvs_gap_multiply_extend_sourceentriesbound. pvs_gap_multiply_extend_sourceentriesbound + S (sto_index_multiply_extend_sourceentries) = (l)) -> exists sto_left_multiply_extend_sourceentries sto_right_multiply_extend_sourceentries sto_output_multiply_extend_sourceentries. ((exists dst_positive_code_multiply_extend_sourceentriesentryleft dst_positive_scale_multiply_extend_sourceentriesentryleft dst_negative_code_multiply_extend_sourceentriesentryleft dst_negative_scale_multiply_extend_sourceentriesentryleft dst_positive_multiply_extend_sourceentriesentryleft dst_negative_multiply_extend_sourceentriesentryleft. (((F) = (((((dst_positive_code_multiply_extend_sourceentriesentryleft) + (dst_positive_scale_multiply_extend_sourceentriesentryleft)) * S ((dst_positive_code_multiply_extend_sourceentriesentryleft) + (dst_positive_scale_multiply_extend_sourceentriesentryleft)) + ((dst_positive_scale_multiply_extend_sourceentriesentryleft) + (dst_positive_scale_multiply_extend_sourceentriesentryleft))) + (((dst_negative_code_multiply_extend_sourceentriesentryleft) + (dst_negative_scale_multiply_extend_sourceentriesentryleft)) * S ((dst_negative_code_multiply_extend_sourceentriesentryleft) + (dst_negative_scale_multiply_extend_sourceentriesentryleft)) + ((dst_negative_scale_multiply_extend_sourceentriesentryleft) + (dst_negative_scale_multiply_extend_sourceentriesentryleft)))) * S ((((dst_positive_code_multiply_extend_sourceentriesentryleft) + (dst_positive_scale_multiply_extend_sourceentriesentryleft)) * S ((dst_positive_code_multiply_extend_sourceentriesentryleft) + (dst_positive_scale_multiply_extend_sourceentriesentryleft)) + ((dst_positive_scale_multiply_extend_sourceentriesentryleft) + (dst_positive_scale_multiply_extend_sourceentriesentryleft))) + (((dst_negative_code_multiply_extend_sourceentriesentryleft) + (dst_negative_scale_multiply_extend_sourceentriesentryleft)) * S ((dst_negative_code_multiply_extend_sourceentriesentryleft) + (dst_negative_scale_multiply_extend_sourceentriesentryleft)) + ((dst_negative_scale_multiply_extend_sourceentriesentryleft) + (dst_negative_scale_multiply_extend_sourceentriesentryleft)))) + ((((dst_negative_code_multiply_extend_sourceentriesentryleft) + (dst_negative_scale_multiply_extend_sourceentriesentryleft)) * S ((dst_negative_code_multiply_extend_sourceentriesentryleft) + (dst_negative_scale_multiply_extend_sourceentriesentryleft)) + ((dst_negative_scale_multiply_extend_sourceentriesentryleft) + (dst_negative_scale_multiply_extend_sourceentriesentryleft))) + (((dst_negative_code_multiply_extend_sourceentriesentryleft) + (dst_negative_scale_multiply_extend_sourceentriesentryleft)) * S ((dst_negative_code_multiply_extend_sourceentriesentryleft) + (dst_negative_scale_multiply_extend_sourceentriesentryleft)) + ((dst_negative_scale_multiply_extend_sourceentriesentryleft) + (dst_negative_scale_multiply_extend_sourceentriesentryleft)))))) /\ (((((exists ff_h_pvs_multiply_extend_sourceentriesentryleftpositive. ff_h_pvs_multiply_extend_sourceentriesentryleftpositive + S (dst_positive_multiply_extend_sourceentriesentryleft) = S ((S (sto_index_multiply_extend_sourceentries)) * dst_positive_scale_multiply_extend_sourceentriesentryleft)) /\ exists ff_q_pvs_multiply_extend_sourceentriesentryleftpositive. dst_positive_code_multiply_extend_sourceentriesentryleft = ff_q_pvs_multiply_extend_sourceentriesentryleftpositive * S ((S (sto_index_multiply_extend_sourceentries)) * dst_positive_scale_multiply_extend_sourceentriesentryleft) + (dst_positive_multiply_extend_sourceentriesentryleft))) /\ (((((exists ff_h_pvs_multiply_extend_sourceentriesentryleftnegative. ff_h_pvs_multiply_extend_sourceentriesentryleftnegative + S (dst_negative_multiply_extend_sourceentriesentryleft) = S ((S (sto_index_multiply_extend_sourceentries)) * dst_negative_scale_multiply_extend_sourceentriesentryleft)) /\ exists ff_q_pvs_multiply_extend_sourceentriesentryleftnegative. dst_negative_code_multiply_extend_sourceentriesentryleft = ff_q_pvs_multiply_extend_sourceentriesentryleftnegative * S ((S (sto_index_multiply_extend_sourceentries)) * dst_negative_scale_multiply_extend_sourceentriesentryleft) + (dst_negative_multiply_extend_sourceentriesentryleft))) /\ (exists ge_balance_positive_multiply_extend_sourceentriesentryleftvalue ge_balance_negative_multiply_extend_sourceentriesentryleftvalue. (((((sto_left_multiply_extend_sourceentries) = 2 * (ge_balance_positive_multiply_extend_sourceentriesentryleftvalue) /\ (ge_balance_negative_multiply_extend_sourceentriesentryleftvalue) = 0) \/ exists ge_signed_half_multiply_extend_sourceentriesentryleftvaluedecode. (((sto_left_multiply_extend_sourceentries) = 2 * ge_signed_half_multiply_extend_sourceentriesentryleftvaluedecode + 1 /\ (ge_balance_positive_multiply_extend_sourceentriesentryleftvalue) = 0) /\ (ge_balance_negative_multiply_extend_sourceentriesentryleftvalue) = S ge_signed_half_multiply_extend_sourceentriesentryleftvaluedecode))) /\ ((dst_positive_multiply_extend_sourceentriesentryleft) + ge_balance_negative_multiply_extend_sourceentriesentryleftvalue = (dst_negative_multiply_extend_sourceentriesentryleft) + ge_balance_positive_multiply_extend_sourceentriesentryleftvalue))))))))) /\ (((exists dst_positive_code_multiply_extend_sourceentriesentryright dst_positive_scale_multiply_extend_sourceentriesentryright dst_negative_code_multiply_extend_sourceentriesentryright dst_negative_scale_multiply_extend_sourceentriesentryright dst_positive_multiply_extend_sourceentriesentryright dst_negative_multiply_extend_sourceentriesentryright. (((G) = (((((dst_positive_code_multiply_extend_sourceentriesentryright) + (dst_positive_scale_multiply_extend_sourceentriesentryright)) * S ((dst_positive_code_multiply_extend_sourceentriesentryright) + (dst_positive_scale_multiply_extend_sourceentriesentryright)) + ((dst_positive_scale_multiply_extend_sourceentriesentryright) + (dst_positive_scale_multiply_extend_sourceentriesentryright))) + (((dst_negative_code_multiply_extend_sourceentriesentryright) + (dst_negative_scale_multiply_extend_sourceentriesentryright)) * S ((dst_negative_code_multiply_extend_sourceentriesentryright) + (dst_negative_scale_multiply_extend_sourceentriesentryright)) + ((dst_negative_scale_multiply_extend_sourceentriesentryright) + (dst_negative_scale_multiply_extend_sourceentriesentryright)))) * S ((((dst_positive_code_multiply_extend_sourceentriesentryright) + (dst_positive_scale_multiply_extend_sourceentriesentryright)) * S ((dst_positive_code_multiply_extend_sourceentriesentryright) + (dst_positive_scale_multiply_extend_sourceentriesentryright)) + ((dst_positive_scale_multiply_extend_sourceentriesentryright) + (dst_positive_scale_multiply_extend_sourceentriesentryright))) + (((dst_negative_code_multiply_extend_sourceentriesentryright) + (dst_negative_scale_multiply_extend_sourceentriesentryright)) * S ((dst_negative_code_multiply_extend_sourceentriesentryright) + (dst_negative_scale_multiply_extend_sourceentriesentryright)) + ((dst_negative_scale_multiply_extend_sourceentriesentryright) + (dst_negative_scale_multiply_extend_sourceentriesentryright)))) + ((((dst_negative_code_multiply_extend_sourceentriesentryright) + (dst_negative_scale_multiply_extend_sourceentriesentryright)) * S ((dst_negative_code_multiply_extend_sourceentriesentryright) + (dst_negative_scale_multiply_extend_sourceentriesentryright)) + ((dst_negative_scale_multiply_extend_sourceentriesentryright) + (dst_negative_scale_multiply_extend_sourceentriesentryright))) + (((dst_negative_code_multiply_extend_sourceentriesentryright) + (dst_negative_scale_multiply_extend_sourceentriesentryright)) * S ((dst_negative_code_multiply_extend_sourceentriesentryright) + (dst_negative_scale_multiply_extend_sourceentriesentryright)) + ((dst_negative_scale_multiply_extend_sourceentriesentryright) + (dst_negative_scale_multiply_extend_sourceentriesentryright)))))) /\ (((((exists ff_h_pvs_multiply_extend_sourceentriesentryrightpositive. ff_h_pvs_multiply_extend_sourceentriesentryrightpositive + S (dst_positive_multiply_extend_sourceentriesentryright) = S ((S (sto_index_multiply_extend_sourceentries)) * dst_positive_scale_multiply_extend_sourceentriesentryright)) /\ exists ff_q_pvs_multiply_extend_sourceentriesentryrightpositive. dst_positive_code_multiply_extend_sourceentriesentryright = ff_q_pvs_multiply_extend_sourceentriesentryrightpositive * S ((S (sto_index_multiply_extend_sourceentries)) * dst_positive_scale_multiply_extend_sourceentriesentryright) + (dst_positive_multiply_extend_sourceentriesentryright))) /\ (((((exists ff_h_pvs_multiply_extend_sourceentriesentryrightnegative. ff_h_pvs_multiply_extend_sourceentriesentryrightnegative + S (dst_negative_multiply_extend_sourceentriesentryright) = S ((S (sto_index_multiply_extend_sourceentries)) * dst_negative_scale_multiply_extend_sourceentriesentryright)) /\ exists ff_q_pvs_multiply_extend_sourceentriesentryrightnegative. dst_negative_code_multiply_extend_sourceentriesentryright = ff_q_pvs_multiply_extend_sourceentriesentryrightnegative * S ((S (sto_index_multiply_extend_sourceentries)) * dst_negative_scale_multiply_extend_sourceentriesentryright) + (dst_negative_multiply_extend_sourceentriesentryright))) /\ (exists ge_balance_positive_multiply_extend_sourceentriesentryrightvalue ge_balance_negative_multiply_extend_sourceentriesentryrightvalue. (((((sto_right_multiply_extend_sourceentries) = 2 * (ge_balance_positive_multiply_extend_sourceentriesentryrightvalue) /\ (ge_balance_negative_multiply_extend_sourceentriesentryrightvalue) = 0) \/ exists ge_signed_half_multiply_extend_sourceentriesentryrightvaluedecode. (((sto_right_multiply_extend_sourceentries) = 2 * ge_signed_half_multiply_extend_sourceentriesentryrightvaluedecode + 1 /\ (ge_balance_positive_multiply_extend_sourceentriesentryrightvalue) = 0) /\ (ge_balance_negative_multiply_extend_sourceentriesentryrightvalue) = S ge_signed_half_multiply_extend_sourceentriesentryrightvaluedecode))) /\ ((dst_positive_multiply_extend_sourceentriesentryright) + ge_balance_negative_multiply_extend_sourceentriesentryrightvalue = (dst_negative_multiply_extend_sourceentriesentryright) + ge_balance_positive_multiply_extend_sourceentriesentryrightvalue))))))))) /\ (((exists dst_positive_code_multiply_extend_sourceentriesentryoutput dst_positive_scale_multiply_extend_sourceentriesentryoutput dst_negative_code_multiply_extend_sourceentriesentryoutput dst_negative_scale_multiply_extend_sourceentriesentryoutput dst_positive_multiply_extend_sourceentriesentryoutput dst_negative_multiply_extend_sourceentriesentryoutput. (((H) = (((((dst_positive_code_multiply_extend_sourceentriesentryoutput) + (dst_positive_scale_multiply_extend_sourceentriesentryoutput)) * S ((dst_positive_code_multiply_extend_sourceentriesentryoutput) + (dst_positive_scale_multiply_extend_sourceentriesentryoutput)) + ((dst_positive_scale_multiply_extend_sourceentriesentryoutput) + (dst_positive_scale_multiply_extend_sourceentriesentryoutput))) + (((dst_negative_code_multiply_extend_sourceentriesentryoutput) + (dst_negative_scale_multiply_extend_sourceentriesentryoutput)) * S ((dst_negative_code_multiply_extend_sourceentriesentryoutput) + (dst_negative_scale_multiply_extend_sourceentriesentryoutput)) + ((dst_negative_scale_multiply_extend_sourceentriesentryoutput) + (dst_negative_scale_multiply_extend_sourceentriesentryoutput)))) * S ((((dst_positive_code_multiply_extend_sourceentriesentryoutput) + (dst_positive_scale_multiply_extend_sourceentriesentryoutput)) * S ((dst_positive_code_multiply_extend_sourceentriesentryoutput) + (dst_positive_scale_multiply_extend_sourceentriesentryoutput)) + ((dst_positive_scale_multiply_extend_sourceentriesentryoutput) + (dst_positive_scale_multiply_extend_sourceentriesentryoutput))) + (((dst_negative_code_multiply_extend_sourceentriesentryoutput) + (dst_negative_scale_multiply_extend_sourceentriesentryoutput)) * S ((dst_negative_code_multiply_extend_sourceentriesentryoutput) + (dst_negative_scale_multiply_extend_sourceentriesentryoutput)) + ((dst_negative_scale_multiply_extend_sourceentriesentryoutput) + (dst_negative_scale_multiply_extend_sourceentriesentryoutput)))) + ((((dst_negative_code_multiply_extend_sourceentriesentryoutput) + (dst_negative_scale_multiply_extend_sourceentriesentryoutput)) * S ((dst_negative_code_multiply_extend_sourceentriesentryoutput) + (dst_negative_scale_multiply_extend_sourceentriesentryoutput)) + ((dst_negative_scale_multiply_extend_sourceentriesentryoutput) + (dst_negative_scale_multiply_extend_sourceentriesentryoutput))) + (((dst_negative_code_multiply_extend_sourceentriesentryoutput) + (dst_negative_scale_multiply_extend_sourceentriesentryoutput)) * S ((dst_negative_code_multiply_extend_sourceentriesentryoutput) + (dst_negative_scale_multiply_extend_sourceentriesentryoutput)) + ((dst_negative_scale_multiply_extend_sourceentriesentryoutput) + (dst_negative_scale_multiply_extend_sourceentriesentryoutput)))))) /\ (((((exists ff_h_pvs_multiply_extend_sourceentriesentryoutputpositive. ff_h_pvs_multiply_extend_sourceentriesentryoutputpositive + S (dst_positive_multiply_extend_sourceentriesentryoutput) = S ((S (sto_index_multiply_extend_sourceentries)) * dst_positive_scale_multiply_extend_sourceentriesentryoutput)) /\ exists ff_q_pvs_multiply_extend_sourceentriesentryoutputpositive. dst_positive_code_multiply_extend_sourceentriesentryoutput = ff_q_pvs_multiply_extend_sourceentriesentryoutputpositive * S ((S (sto_index_multiply_extend_sourceentries)) * dst_positive_scale_multiply_extend_sourceentriesentryoutput) + (dst_positive_multiply_extend_sourceentriesentryoutput))) /\ (((((exists ff_h_pvs_multiply_extend_sourceentriesentryoutputnegative. ff_h_pvs_multiply_extend_sourceentriesentryoutputnegative + S (dst_negative_multiply_extend_sourceentriesentryoutput) = S ((S (sto_index_multiply_extend_sourceentries)) * dst_negative_scale_multiply_extend_sourceentriesentryoutput)) /\ exists ff_q_pvs_multiply_extend_sourceentriesentryoutputnegative. dst_negative_code_multiply_extend_sourceentriesentryoutput = ff_q_pvs_multiply_extend_sourceentriesentryoutputnegative * S ((S (sto_index_multiply_extend_sourceentries)) * dst_negative_scale_multiply_extend_sourceentriesentryoutput) + (dst_negative_multiply_extend_sourceentriesentryoutput))) /\ (exists ge_balance_positive_multiply_extend_sourceentriesentryoutputvalue ge_balance_negative_multiply_extend_sourceentriesentryoutputvalue. (((((sto_output_multiply_extend_sourceentries) = 2 * (ge_balance_positive_multiply_extend_sourceentriesentryoutputvalue) /\ (ge_balance_negative_multiply_extend_sourceentriesentryoutputvalue) = 0) \/ exists ge_signed_half_multiply_extend_sourceentriesentryoutputvaluedecode. (((sto_output_multiply_extend_sourceentries) = 2 * ge_signed_half_multiply_extend_sourceentriesentryoutputvaluedecode + 1 /\ (ge_balance_positive_multiply_extend_sourceentriesentryoutputvalue) = 0) /\ (ge_balance_negative_multiply_extend_sourceentriesentryoutputvalue) = S ge_signed_half_multiply_extend_sourceentriesentryoutputvaluedecode))) /\ ((dst_positive_multiply_extend_sourceentriesentryoutput) + ge_balance_negative_multiply_extend_sourceentriesentryoutputvalue = (dst_negative_multiply_extend_sourceentriesentryoutput) + ge_balance_positive_multiply_extend_sourceentriesentryoutputvalue))))))))) /\ (exists sto_ap_multiply_extend_sourceentriesentryoperation sto_an_multiply_extend_sourceentriesentryoperation sto_bp_multiply_extend_sourceentriesentryoperation sto_bn_multiply_extend_sourceentriesentryoperation sto_cp_multiply_extend_sourceentriesentryoperation sto_cn_multiply_extend_sourceentriesentryoperation. (((((sto_left_multiply_extend_sourceentries) = 2 * (sto_ap_multiply_extend_sourceentriesentryoperation) /\ (sto_an_multiply_extend_sourceentriesentryoperation) = 0) \/ exists ge_signed_half_multiply_extend_sourceentriesentryoperationleft. (((sto_left_multiply_extend_sourceentries) = 2 * ge_signed_half_multiply_extend_sourceentriesentryoperationleft + 1 /\ (sto_ap_multiply_extend_sourceentriesentryoperation) = 0) /\ (sto_an_multiply_extend_sourceentriesentryoperation) = S ge_signed_half_multiply_extend_sourceentriesentryoperationleft))) /\ ((((((sto_right_multiply_extend_sourceentries) = 2 * (sto_bp_multiply_extend_sourceentriesentryoperation) /\ (sto_bn_multiply_extend_sourceentriesentryoperation) = 0) \/ exists ge_signed_half_multiply_extend_sourceentriesentryoperationright. (((sto_right_multiply_extend_sourceentries) = 2 * ge_signed_half_multiply_extend_sourceentriesentryoperationright + 1 /\ (sto_bp_multiply_extend_sourceentriesentryoperation) = 0) /\ (sto_bn_multiply_extend_sourceentriesentryoperation) = S ge_signed_half_multiply_extend_sourceentriesentryoperationright))) /\ ((((((sto_output_multiply_extend_sourceentries) = 2 * (sto_cp_multiply_extend_sourceentriesentryoperation) /\ (sto_cn_multiply_extend_sourceentriesentryoperation) = 0) \/ exists ge_signed_half_multiply_extend_sourceentriesentryoperationoutput. (((sto_output_multiply_extend_sourceentries) = 2 * ge_signed_half_multiply_extend_sourceentriesentryoperationoutput + 1 /\ (sto_cp_multiply_extend_sourceentriesentryoperation) = 0) /\ (sto_cn_multiply_extend_sourceentriesentryoperation) = S ge_signed_half_multiply_extend_sourceentriesentryoperationoutput))) /\ ((sto_ap_multiply_extend_sourceentriesentryoperation * sto_bp_multiply_extend_sourceentriesentryoperation + sto_an_multiply_extend_sourceentriesentryoperation * sto_bn_multiply_extend_sourceentriesentryoperation) + sto_cn_multiply_extend_sourceentriesentryoperation = (sto_ap_multiply_extend_sourceentriesentryoperation * sto_bn_multiply_extend_sourceentriesentryoperation + sto_an_multiply_extend_sourceentriesentryoperation * sto_bp_multiply_extend_sourceentriesentryoperation) + sto_cp_multiply_extend_sourceentriesentryoperation))))))))))))))))))) -> (exists dst_positive_code_multiply_extend_table dst_positive_scale_multiply_extend_table dst_negative_code_multiply_extend_table dst_negative_scale_multiply_extend_table. (((K) = (((((dst_positive_code_multiply_extend_table) + (dst_positive_scale_multiply_extend_table)) * S ((dst_positive_code_multiply_extend_table) + (dst_positive_scale_multiply_extend_table)) + ((dst_positive_scale_multiply_extend_table) + (dst_positive_scale_multiply_extend_table))) + (((dst_negative_code_multiply_extend_table) + (dst_negative_scale_multiply_extend_table)) * S ((dst_negative_code_multiply_extend_table) + (dst_negative_scale_multiply_extend_table)) + ((dst_negative_scale_multiply_extend_table) + (dst_negative_scale_multiply_extend_table)))) * S ((((dst_positive_code_multiply_extend_table) + (dst_positive_scale_multiply_extend_table)) * S ((dst_positive_code_multiply_extend_table) + (dst_positive_scale_multiply_extend_table)) + ((dst_positive_scale_multiply_extend_table) + (dst_positive_scale_multiply_extend_table))) + (((dst_negative_code_multiply_extend_table) + (dst_negative_scale_multiply_extend_table)) * S ((dst_negative_code_multiply_extend_table) + (dst_negative_scale_multiply_extend_table)) + ((dst_negative_scale_multiply_extend_table) + (dst_negative_scale_multiply_extend_table)))) + ((((dst_negative_code_multiply_extend_table) + (dst_negative_scale_multiply_extend_table)) * S ((dst_negative_code_multiply_extend_table) + (dst_negative_scale_multiply_extend_table)) + ((dst_negative_scale_multiply_extend_table) + (dst_negative_scale_multiply_extend_table))) + (((dst_negative_code_multiply_extend_table) + (dst_negative_scale_multiply_extend_table)) * S ((dst_negative_code_multiply_extend_table) + (dst_negative_scale_multiply_extend_table)) + ((dst_negative_scale_multiply_extend_table) + (dst_negative_scale_multiply_extend_table)))))) /\ (forall dst_index_multiply_extend_table. (exists pvs_le_gap_multiply_extend_tabledomain. pvs_le_gap_multiply_extend_tabledomain + (dst_index_multiply_extend_table) = (l)) -> exists dst_positive_multiply_extend_table dst_negative_multiply_extend_table dst_value_multiply_extend_table. ((((exists ff_h_pvs_multiply_extend_tableentrypositive. ff_h_pvs_multiply_extend_tableentrypositive + S (dst_positive_multiply_extend_table) = S ((S (dst_index_multiply_extend_table)) * dst_positive_scale_multiply_extend_table)) /\ exists ff_q_pvs_multiply_extend_tableentrypositive. dst_positive_code_multiply_extend_table = ff_q_pvs_multiply_extend_tableentrypositive * S ((S (dst_index_multiply_extend_table)) * dst_positive_scale_multiply_extend_table) + (dst_positive_multiply_extend_table))) /\ (((((exists ff_h_pvs_multiply_extend_tableentrynegative. ff_h_pvs_multiply_extend_tableentrynegative + S (dst_negative_multiply_extend_table) = S ((S (dst_index_multiply_extend_table)) * dst_negative_scale_multiply_extend_table)) /\ exists ff_q_pvs_multiply_extend_tableentrynegative. dst_negative_code_multiply_extend_table = ff_q_pvs_multiply_extend_tableentrynegative * S ((S (dst_index_multiply_extend_table)) * dst_negative_scale_multiply_extend_table) + (dst_negative_multiply_extend_table))) /\ (exists ge_balance_positive_multiply_extend_tableentryvalue ge_balance_negative_multiply_extend_tableentryvalue. (((((dst_value_multiply_extend_table) = 2 * (ge_balance_positive_multiply_extend_tableentryvalue) /\ (ge_balance_negative_multiply_extend_tableentryvalue) = 0) \/ exists ge_signed_half_multiply_extend_tableentryvaluedecode. (((dst_value_multiply_extend_table) = 2 * ge_signed_half_multiply_extend_tableentryvaluedecode + 1 /\ (ge_balance_positive_multiply_extend_tableentryvalue) = 0) /\ (ge_balance_negative_multiply_extend_tableentryvalue) = S ge_signed_half_multiply_extend_tableentryvaluedecode))) /\ ((dst_positive_multiply_extend_table) + ge_balance_negative_multiply_extend_tableentryvalue = (dst_negative_multiply_extend_table) + ge_balance_positive_multiply_extend_tableentryvalue))))))))) -> (forall dst_index_multiply_extend_preservation dst_first_multiply_extend_preservation dst_second_multiply_extend_preservation. (exists pvs_gap_multiply_extend_preservationbound. pvs_gap_multiply_extend_preservationbound + S (dst_index_multiply_extend_preservation) = (l)) -> (exists dst_positive_code_multiply_extend_preservationfirst dst_positive_scale_multiply_extend_preservationfirst dst_negative_code_multiply_extend_preservationfirst dst_negative_scale_multiply_extend_preservationfirst dst_positive_multiply_extend_preservationfirst dst_negative_multiply_extend_preservationfirst. (((H) = (((((dst_positive_code_multiply_extend_preservationfirst) + (dst_positive_scale_multiply_extend_preservationfirst)) * S ((dst_positive_code_multiply_extend_preservationfirst) + (dst_positive_scale_multiply_extend_preservationfirst)) + ((dst_positive_scale_multiply_extend_preservationfirst) + (dst_positive_scale_multiply_extend_preservationfirst))) + (((dst_negative_code_multiply_extend_preservationfirst) + (dst_negative_scale_multiply_extend_preservationfirst)) * S ((dst_negative_code_multiply_extend_preservationfirst) + (dst_negative_scale_multiply_extend_preservationfirst)) + ((dst_negative_scale_multiply_extend_preservationfirst) + (dst_negative_scale_multiply_extend_preservationfirst)))) * S ((((dst_positive_code_multiply_extend_preservationfirst) + (dst_positive_scale_multiply_extend_preservationfirst)) * S ((dst_positive_code_multiply_extend_preservationfirst) + (dst_positive_scale_multiply_extend_preservationfirst)) + ((dst_positive_scale_multiply_extend_preservationfirst) + (dst_positive_scale_multiply_extend_preservationfirst))) + (((dst_negative_code_multiply_extend_preservationfirst) + (dst_negative_scale_multiply_extend_preservationfirst)) * S ((dst_negative_code_multiply_extend_preservationfirst) + (dst_negative_scale_multiply_extend_preservationfirst)) + ((dst_negative_scale_multiply_extend_preservationfirst) + (dst_negative_scale_multiply_extend_preservationfirst)))) + ((((dst_negative_code_multiply_extend_preservationfirst) + (dst_negative_scale_multiply_extend_preservationfirst)) * S ((dst_negative_code_multiply_extend_preservationfirst) + (dst_negative_scale_multiply_extend_preservationfirst)) + ((dst_negative_scale_multiply_extend_preservationfirst) + (dst_negative_scale_multiply_extend_preservationfirst))) + (((dst_negative_code_multiply_extend_preservationfirst) + (dst_negative_scale_multiply_extend_preservationfirst)) * S ((dst_negative_code_multiply_extend_preservationfirst) + (dst_negative_scale_multiply_extend_preservationfirst)) + ((dst_negative_scale_multiply_extend_preservationfirst) + (dst_negative_scale_multiply_extend_preservationfirst)))))) /\ (((((exists ff_h_pvs_multiply_extend_preservationfirstpositive. ff_h_pvs_multiply_extend_preservationfirstpositive + S (dst_positive_multiply_extend_preservationfirst) = S ((S (dst_index_multiply_extend_preservation)) * dst_positive_scale_multiply_extend_preservationfirst)) /\ exists ff_q_pvs_multiply_extend_preservationfirstpositive. dst_positive_code_multiply_extend_preservationfirst = ff_q_pvs_multiply_extend_preservationfirstpositive * S ((S (dst_index_multiply_extend_preservation)) * dst_positive_scale_multiply_extend_preservationfirst) + (dst_positive_multiply_extend_preservationfirst))) /\ (((((exists ff_h_pvs_multiply_extend_preservationfirstnegative. ff_h_pvs_multiply_extend_preservationfirstnegative + S (dst_negative_multiply_extend_preservationfirst) = S ((S (dst_index_multiply_extend_preservation)) * dst_negative_scale_multiply_extend_preservationfirst)) /\ exists ff_q_pvs_multiply_extend_preservationfirstnegative. dst_negative_code_multiply_extend_preservationfirst = ff_q_pvs_multiply_extend_preservationfirstnegative * S ((S (dst_index_multiply_extend_preservation)) * dst_negative_scale_multiply_extend_preservationfirst) + (dst_negative_multiply_extend_preservationfirst))) /\ (exists ge_balance_positive_multiply_extend_preservationfirstvalue ge_balance_negative_multiply_extend_preservationfirstvalue. (((((dst_first_multiply_extend_preservation) = 2 * (ge_balance_positive_multiply_extend_preservationfirstvalue) /\ (ge_balance_negative_multiply_extend_preservationfirstvalue) = 0) \/ exists ge_signed_half_multiply_extend_preservationfirstvaluedecode. (((dst_first_multiply_extend_preservation) = 2 * ge_signed_half_multiply_extend_preservationfirstvaluedecode + 1 /\ (ge_balance_positive_multiply_extend_preservationfirstvalue) = 0) /\ (ge_balance_negative_multiply_extend_preservationfirstvalue) = S ge_signed_half_multiply_extend_preservationfirstvaluedecode))) /\ ((dst_positive_multiply_extend_preservationfirst) + ge_balance_negative_multiply_extend_preservationfirstvalue = (dst_negative_multiply_extend_preservationfirst) + ge_balance_positive_multiply_extend_preservationfirstvalue))))))))) -> (exists dst_positive_code_multiply_extend_preservationsecond dst_positive_scale_multiply_extend_preservationsecond dst_negative_code_multiply_extend_preservationsecond dst_negative_scale_multiply_extend_preservationsecond dst_positive_multiply_extend_preservationsecond dst_negative_multiply_extend_preservationsecond. (((K) = (((((dst_positive_code_multiply_extend_preservationsecond) + (dst_positive_scale_multiply_extend_preservationsecond)) * S ((dst_positive_code_multiply_extend_preservationsecond) + (dst_positive_scale_multiply_extend_preservationsecond)) + ((dst_positive_scale_multiply_extend_preservationsecond) + (dst_positive_scale_multiply_extend_preservationsecond))) + (((dst_negative_code_multiply_extend_preservationsecond) + (dst_negative_scale_multiply_extend_preservationsecond)) * S ((dst_negative_code_multiply_extend_preservationsecond) + (dst_negative_scale_multiply_extend_preservationsecond)) + ((dst_negative_scale_multiply_extend_preservationsecond) + (dst_negative_scale_multiply_extend_preservationsecond)))) * S ((((dst_positive_code_multiply_extend_preservationsecond) + (dst_positive_scale_multiply_extend_preservationsecond)) * S ((dst_positive_code_multiply_extend_preservationsecond) + (dst_positive_scale_multiply_extend_preservationsecond)) + ((dst_positive_scale_multiply_extend_preservationsecond) + (dst_positive_scale_multiply_extend_preservationsecond))) + (((dst_negative_code_multiply_extend_preservationsecond) + (dst_negative_scale_multiply_extend_preservationsecond)) * S ((dst_negative_code_multiply_extend_preservationsecond) + (dst_negative_scale_multiply_extend_preservationsecond)) + ((dst_negative_scale_multiply_extend_preservationsecond) + (dst_negative_scale_multiply_extend_preservationsecond)))) + ((((dst_negative_code_multiply_extend_preservationsecond) + (dst_negative_scale_multiply_extend_preservationsecond)) * S ((dst_negative_code_multiply_extend_preservationsecond) + (dst_negative_scale_multiply_extend_preservationsecond)) + ((dst_negative_scale_multiply_extend_preservationsecond) + (dst_negative_scale_multiply_extend_preservationsecond))) + (((dst_negative_code_multiply_extend_preservationsecond) + (dst_negative_scale_multiply_extend_preservationsecond)) * S ((dst_negative_code_multiply_extend_preservationsecond) + (dst_negative_scale_multiply_extend_preservationsecond)) + ((dst_negative_scale_multiply_extend_preservationsecond) + (dst_negative_scale_multiply_extend_preservationsecond)))))) /\ (((((exists ff_h_pvs_multiply_extend_preservationsecondpositive. ff_h_pvs_multiply_extend_preservationsecondpositive + S (dst_positive_multiply_extend_preservationsecond) = S ((S (dst_index_multiply_extend_preservation)) * dst_positive_scale_multiply_extend_preservationsecond)) /\ exists ff_q_pvs_multiply_extend_preservationsecondpositive. dst_positive_code_multiply_extend_preservationsecond = ff_q_pvs_multiply_extend_preservationsecondpositive * S ((S (dst_index_multiply_extend_preservation)) * dst_positive_scale_multiply_extend_preservationsecond) + (dst_positive_multiply_extend_preservationsecond))) /\ (((((exists ff_h_pvs_multiply_extend_preservationsecondnegative. ff_h_pvs_multiply_extend_preservationsecondnegative + S (dst_negative_multiply_extend_preservationsecond) = S ((S (dst_index_multiply_extend_preservation)) * dst_negative_scale_multiply_extend_preservationsecond)) /\ exists ff_q_pvs_multiply_extend_preservationsecondnegative. dst_negative_code_multiply_extend_preservationsecond = ff_q_pvs_multiply_extend_preservationsecondnegative * S ((S (dst_index_multiply_extend_preservation)) * dst_negative_scale_multiply_extend_preservationsecond) + (dst_negative_multiply_extend_preservationsecond))) /\ (exists ge_balance_positive_multiply_extend_preservationsecondvalue ge_balance_negative_multiply_extend_preservationsecondvalue. (((((dst_second_multiply_extend_preservation) = 2 * (ge_balance_positive_multiply_extend_preservationsecondvalue) /\ (ge_balance_negative_multiply_extend_preservationsecondvalue) = 0) \/ exists ge_signed_half_multiply_extend_preservationsecondvaluedecode. (((dst_second_multiply_extend_preservation) = 2 * ge_signed_half_multiply_extend_preservationsecondvaluedecode + 1 /\ (ge_balance_positive_multiply_extend_preservationsecondvalue) = 0) /\ (ge_balance_negative_multiply_extend_preservationsecondvalue) = S ge_signed_half_multiply_extend_preservationsecondvaluedecode))) /\ ((dst_positive_multiply_extend_preservationsecond) + ge_balance_negative_multiply_extend_preservationsecondvalue = (dst_negative_multiply_extend_preservationsecond) + ge_balance_positive_multiply_extend_preservationsecondvalue))))))))) -> dst_first_multiply_extend_preservation = dst_second_multiply_extend_preservation) -> (exists dst_positive_code_multiply_extend_at_0 dst_positive_scale_multiply_extend_at_0 dst_negative_code_multiply_extend_at_0 dst_negative_scale_multiply_extend_at_0 dst_positive_multiply_extend_at_0 dst_negative_multiply_extend_at_0. (((F) = (((((dst_positive_code_multiply_extend_at_0) + (dst_positive_scale_multiply_extend_at_0)) * S ((dst_positive_code_multiply_extend_at_0) + (dst_positive_scale_multiply_extend_at_0)) + ((dst_positive_scale_multiply_extend_at_0) + (dst_positive_scale_multiply_extend_at_0))) + (((dst_negative_code_multiply_extend_at_0) + (dst_negative_scale_multiply_extend_at_0)) * S ((dst_negative_code_multiply_extend_at_0) + (dst_negative_scale_multiply_extend_at_0)) + ((dst_negative_scale_multiply_extend_at_0) + (dst_negative_scale_multiply_extend_at_0)))) * S ((((dst_positive_code_multiply_extend_at_0) + (dst_positive_scale_multiply_extend_at_0)) * S ((dst_positive_code_multiply_extend_at_0) + (dst_positive_scale_multiply_extend_at_0)) + ((dst_positive_scale_multiply_extend_at_0) + (dst_positive_scale_multiply_extend_at_0))) + (((dst_negative_code_multiply_extend_at_0) + (dst_negative_scale_multiply_extend_at_0)) * S ((dst_negative_code_multiply_extend_at_0) + (dst_negative_scale_multiply_extend_at_0)) + ((dst_negative_scale_multiply_extend_at_0) + (dst_negative_scale_multiply_extend_at_0)))) + ((((dst_negative_code_multiply_extend_at_0) + (dst_negative_scale_multiply_extend_at_0)) * S ((dst_negative_code_multiply_extend_at_0) + (dst_negative_scale_multiply_extend_at_0)) + ((dst_negative_scale_multiply_extend_at_0) + (dst_negative_scale_multiply_extend_at_0))) + (((dst_negative_code_multiply_extend_at_0) + (dst_negative_scale_multiply_extend_at_0)) * S ((dst_negative_code_multiply_extend_at_0) + (dst_negative_scale_multiply_extend_at_0)) + ((dst_negative_scale_multiply_extend_at_0) + (dst_negative_scale_multiply_extend_at_0)))))) /\ (((((exists ff_h_pvs_multiply_extend_at_0positive. ff_h_pvs_multiply_extend_at_0positive + S (dst_positive_multiply_extend_at_0) = S ((S (l)) * dst_positive_scale_multiply_extend_at_0)) /\ exists ff_q_pvs_multiply_extend_at_0positive. dst_positive_code_multiply_extend_at_0 = ff_q_pvs_multiply_extend_at_0positive * S ((S (l)) * dst_positive_scale_multiply_extend_at_0) + (dst_positive_multiply_extend_at_0))) /\ (((((exists ff_h_pvs_multiply_extend_at_0negative. ff_h_pvs_multiply_extend_at_0negative + S (dst_negative_multiply_extend_at_0) = S ((S (l)) * dst_negative_scale_multiply_extend_at_0)) /\ exists ff_q_pvs_multiply_extend_at_0negative. dst_negative_code_multiply_extend_at_0 = ff_q_pvs_multiply_extend_at_0negative * S ((S (l)) * dst_negative_scale_multiply_extend_at_0) + (dst_negative_multiply_extend_at_0))) /\ (exists ge_balance_positive_multiply_extend_at_0value ge_balance_negative_multiply_extend_at_0value. (((((a) = 2 * (ge_balance_positive_multiply_extend_at_0value) /\ (ge_balance_negative_multiply_extend_at_0value) = 0) \/ exists ge_signed_half_multiply_extend_at_0valuedecode. (((a) = 2 * ge_signed_half_multiply_extend_at_0valuedecode + 1 /\ (ge_balance_positive_multiply_extend_at_0value) = 0) /\ (ge_balance_negative_multiply_extend_at_0value) = S ge_signed_half_multiply_extend_at_0valuedecode))) /\ ((dst_positive_multiply_extend_at_0) + ge_balance_negative_multiply_extend_at_0value = (dst_negative_multiply_extend_at_0) + ge_balance_positive_multiply_extend_at_0value))))))))) -> (exists dst_positive_code_multiply_extend_at_1 dst_positive_scale_multiply_extend_at_1 dst_negative_code_multiply_extend_at_1 dst_negative_scale_multiply_extend_at_1 dst_positive_multiply_extend_at_1 dst_negative_multiply_extend_at_1. (((G) = (((((dst_positive_code_multiply_extend_at_1) + (dst_positive_scale_multiply_extend_at_1)) * S ((dst_positive_code_multiply_extend_at_1) + (dst_positive_scale_multiply_extend_at_1)) + ((dst_positive_scale_multiply_extend_at_1) + (dst_positive_scale_multiply_extend_at_1))) + (((dst_negative_code_multiply_extend_at_1) + (dst_negative_scale_multiply_extend_at_1)) * S ((dst_negative_code_multiply_extend_at_1) + (dst_negative_scale_multiply_extend_at_1)) + ((dst_negative_scale_multiply_extend_at_1) + (dst_negative_scale_multiply_extend_at_1)))) * S ((((dst_positive_code_multiply_extend_at_1) + (dst_positive_scale_multiply_extend_at_1)) * S ((dst_positive_code_multiply_extend_at_1) + (dst_positive_scale_multiply_extend_at_1)) + ((dst_positive_scale_multiply_extend_at_1) + (dst_positive_scale_multiply_extend_at_1))) + (((dst_negative_code_multiply_extend_at_1) + (dst_negative_scale_multiply_extend_at_1)) * S ((dst_negative_code_multiply_extend_at_1) + (dst_negative_scale_multiply_extend_at_1)) + ((dst_negative_scale_multiply_extend_at_1) + (dst_negative_scale_multiply_extend_at_1)))) + ((((dst_negative_code_multiply_extend_at_1) + (dst_negative_scale_multiply_extend_at_1)) * S ((dst_negative_code_multiply_extend_at_1) + (dst_negative_scale_multiply_extend_at_1)) + ((dst_negative_scale_multiply_extend_at_1) + (dst_negative_scale_multiply_extend_at_1))) + (((dst_negative_code_multiply_extend_at_1) + (dst_negative_scale_multiply_extend_at_1)) * S ((dst_negative_code_multiply_extend_at_1) + (dst_negative_scale_multiply_extend_at_1)) + ((dst_negative_scale_multiply_extend_at_1) + (dst_negative_scale_multiply_extend_at_1)))))) /\ (((((exists ff_h_pvs_multiply_extend_at_1positive. ff_h_pvs_multiply_extend_at_1positive + S (dst_positive_multiply_extend_at_1) = S ((S (l)) * dst_positive_scale_multiply_extend_at_1)) /\ exists ff_q_pvs_multiply_extend_at_1positive. dst_positive_code_multiply_extend_at_1 = ff_q_pvs_multiply_extend_at_1positive * S ((S (l)) * dst_positive_scale_multiply_extend_at_1) + (dst_positive_multiply_extend_at_1))) /\ (((((exists ff_h_pvs_multiply_extend_at_1negative. ff_h_pvs_multiply_extend_at_1negative + S (dst_negative_multiply_extend_at_1) = S ((S (l)) * dst_negative_scale_multiply_extend_at_1)) /\ exists ff_q_pvs_multiply_extend_at_1negative. dst_negative_code_multiply_extend_at_1 = ff_q_pvs_multiply_extend_at_1negative * S ((S (l)) * dst_negative_scale_multiply_extend_at_1) + (dst_negative_multiply_extend_at_1))) /\ (exists ge_balance_positive_multiply_extend_at_1value ge_balance_negative_multiply_extend_at_1value. (((((b) = 2 * (ge_balance_positive_multiply_extend_at_1value) /\ (ge_balance_negative_multiply_extend_at_1value) = 0) \/ exists ge_signed_half_multiply_extend_at_1valuedecode. (((b) = 2 * ge_signed_half_multiply_extend_at_1valuedecode + 1 /\ (ge_balance_positive_multiply_extend_at_1value) = 0) /\ (ge_balance_negative_multiply_extend_at_1value) = S ge_signed_half_multiply_extend_at_1valuedecode))) /\ ((dst_positive_multiply_extend_at_1) + ge_balance_negative_multiply_extend_at_1value = (dst_negative_multiply_extend_at_1) + ge_balance_positive_multiply_extend_at_1value))))))))) -> (exists dst_positive_code_multiply_extend_at_2 dst_positive_scale_multiply_extend_at_2 dst_negative_code_multiply_extend_at_2 dst_negative_scale_multiply_extend_at_2 dst_positive_multiply_extend_at_2 dst_negative_multiply_extend_at_2. (((K) = (((((dst_positive_code_multiply_extend_at_2) + (dst_positive_scale_multiply_extend_at_2)) * S ((dst_positive_code_multiply_extend_at_2) + (dst_positive_scale_multiply_extend_at_2)) + ((dst_positive_scale_multiply_extend_at_2) + (dst_positive_scale_multiply_extend_at_2))) + (((dst_negative_code_multiply_extend_at_2) + (dst_negative_scale_multiply_extend_at_2)) * S ((dst_negative_code_multiply_extend_at_2) + (dst_negative_scale_multiply_extend_at_2)) + ((dst_negative_scale_multiply_extend_at_2) + (dst_negative_scale_multiply_extend_at_2)))) * S ((((dst_positive_code_multiply_extend_at_2) + (dst_positive_scale_multiply_extend_at_2)) * S ((dst_positive_code_multiply_extend_at_2) + (dst_positive_scale_multiply_extend_at_2)) + ((dst_positive_scale_multiply_extend_at_2) + (dst_positive_scale_multiply_extend_at_2))) + (((dst_negative_code_multiply_extend_at_2) + (dst_negative_scale_multiply_extend_at_2)) * S ((dst_negative_code_multiply_extend_at_2) + (dst_negative_scale_multiply_extend_at_2)) + ((dst_negative_scale_multiply_extend_at_2) + (dst_negative_scale_multiply_extend_at_2)))) + ((((dst_negative_code_multiply_extend_at_2) + (dst_negative_scale_multiply_extend_at_2)) * S ((dst_negative_code_multiply_extend_at_2) + (dst_negative_scale_multiply_extend_at_2)) + ((dst_negative_scale_multiply_extend_at_2) + (dst_negative_scale_multiply_extend_at_2))) + (((dst_negative_code_multiply_extend_at_2) + (dst_negative_scale_multiply_extend_at_2)) * S ((dst_negative_code_multiply_extend_at_2) + (dst_negative_scale_multiply_extend_at_2)) + ((dst_negative_scale_multiply_extend_at_2) + (dst_negative_scale_multiply_extend_at_2)))))) /\ (((((exists ff_h_pvs_multiply_extend_at_2positive. ff_h_pvs_multiply_extend_at_2positive + S (dst_positive_multiply_extend_at_2) = S ((S (l)) * dst_positive_scale_multiply_extend_at_2)) /\ exists ff_q_pvs_multiply_extend_at_2positive. dst_positive_code_multiply_extend_at_2 = ff_q_pvs_multiply_extend_at_2positive * S ((S (l)) * dst_positive_scale_multiply_extend_at_2) + (dst_positive_multiply_extend_at_2))) /\ (((((exists ff_h_pvs_multiply_extend_at_2negative. ff_h_pvs_multiply_extend_at_2negative + S (dst_negative_multiply_extend_at_2) = S ((S (l)) * dst_negative_scale_multiply_extend_at_2)) /\ exists ff_q_pvs_multiply_extend_at_2negative. dst_negative_code_multiply_extend_at_2 = ff_q_pvs_multiply_extend_at_2negative * S ((S (l)) * dst_negative_scale_multiply_extend_at_2) + (dst_negative_multiply_extend_at_2))) /\ (exists ge_balance_positive_multiply_extend_at_2value ge_balance_negative_multiply_extend_at_2value. (((((c) = 2 * (ge_balance_positive_multiply_extend_at_2value) /\ (ge_balance_negative_multiply_extend_at_2value) = 0) \/ exists ge_signed_half_multiply_extend_at_2valuedecode. (((c) = 2 * ge_signed_half_multiply_extend_at_2valuedecode + 1 /\ (ge_balance_positive_multiply_extend_at_2value) = 0) /\ (ge_balance_negative_multiply_extend_at_2value) = S ge_signed_half_multiply_extend_at_2valuedecode))) /\ ((dst_positive_multiply_extend_at_2) + ge_balance_negative_multiply_extend_at_2value = (dst_negative_multiply_extend_at_2) + ge_balance_positive_multiply_extend_at_2value))))))))) -> (exists sto_ap_multiply_extend_operation sto_an_multiply_extend_operation sto_bp_multiply_extend_operation sto_bn_multiply_extend_operation sto_cp_multiply_extend_operation sto_cn_multiply_extend_operation. (((((a) = 2 * (sto_ap_multiply_extend_operation) /\ (sto_an_multiply_extend_operation) = 0) \/ exists ge_signed_half_multiply_extend_operationleft. (((a) = 2 * ge_signed_half_multiply_extend_operationleft + 1 /\ (sto_ap_multiply_extend_operation) = 0) /\ (sto_an_multiply_extend_operation) = S ge_signed_half_multiply_extend_operationleft))) /\ ((((((b) = 2 * (sto_bp_multiply_extend_operation) /\ (sto_bn_multiply_extend_operation) = 0) \/ exists ge_signed_half_multiply_extend_operationright. (((b) = 2 * ge_signed_half_multiply_extend_operationright + 1 /\ (sto_bp_multiply_extend_operation) = 0) /\ (sto_bn_multiply_extend_operation) = S ge_signed_half_multiply_extend_operationright))) /\ ((((((c) = 2 * (sto_cp_multiply_extend_operation) /\ (sto_cn_multiply_extend_operation) = 0) \/ exists ge_signed_half_multiply_extend_operationoutput. (((c) = 2 * ge_signed_half_multiply_extend_operationoutput + 1 /\ (sto_cp_multiply_extend_operation) = 0) /\ (sto_cn_multiply_extend_operation) = S ge_signed_half_multiply_extend_operationoutput))) /\ ((sto_ap_multiply_extend_operation * sto_bp_multiply_extend_operation + sto_an_multiply_extend_operation * sto_bn_multiply_extend_operation) + sto_cn_multiply_extend_operation = (sto_ap_multiply_extend_operation * sto_bn_multiply_extend_operation + sto_an_multiply_extend_operation * sto_bp_multiply_extend_operation) + sto_cp_multiply_extend_operation))))))) -> (((exists dst_positive_code_multiply_extend_resultleft_table dst_positive_scale_multiply_extend_resultleft_table dst_negative_code_multiply_extend_resultleft_table dst_negative_scale_multiply_extend_resultleft_table. (((F) = (((((dst_positive_code_multiply_extend_resultleft_table) + (dst_positive_scale_multiply_extend_resultleft_table)) * S ((dst_positive_code_multiply_extend_resultleft_table) + (dst_positive_scale_multiply_extend_resultleft_table)) + ((dst_positive_scale_multiply_extend_resultleft_table) + (dst_positive_scale_multiply_extend_resultleft_table))) + (((dst_negative_code_multiply_extend_resultleft_table) + (dst_negative_scale_multiply_extend_resultleft_table)) * S ((dst_negative_code_multiply_extend_resultleft_table) + (dst_negative_scale_multiply_extend_resultleft_table)) + ((dst_negative_scale_multiply_extend_resultleft_table) + (dst_negative_scale_multiply_extend_resultleft_table)))) * S ((((dst_positive_code_multiply_extend_resultleft_table) + (dst_positive_scale_multiply_extend_resultleft_table)) * S ((dst_positive_code_multiply_extend_resultleft_table) + (dst_positive_scale_multiply_extend_resultleft_table)) + ((dst_positive_scale_multiply_extend_resultleft_table) + (dst_positive_scale_multiply_extend_resultleft_table))) + (((dst_negative_code_multiply_extend_resultleft_table) + (dst_negative_scale_multiply_extend_resultleft_table)) * S ((dst_negative_code_multiply_extend_resultleft_table) + (dst_negative_scale_multiply_extend_resultleft_table)) + ((dst_negative_scale_multiply_extend_resultleft_table) + (dst_negative_scale_multiply_extend_resultleft_table)))) + ((((dst_negative_code_multiply_extend_resultleft_table) + (dst_negative_scale_multiply_extend_resultleft_table)) * S ((dst_negative_code_multiply_extend_resultleft_table) + (dst_negative_scale_multiply_extend_resultleft_table)) + ((dst_negative_scale_multiply_extend_resultleft_table) + (dst_negative_scale_multiply_extend_resultleft_table))) + (((dst_negative_code_multiply_extend_resultleft_table) + (dst_negative_scale_multiply_extend_resultleft_table)) * S ((dst_negative_code_multiply_extend_resultleft_table) + (dst_negative_scale_multiply_extend_resultleft_table)) + ((dst_negative_scale_multiply_extend_resultleft_table) + (dst_negative_scale_multiply_extend_resultleft_table)))))) /\ (forall dst_index_multiply_extend_resultleft_table. (exists pvs_le_gap_multiply_extend_resultleft_tabledomain. pvs_le_gap_multiply_extend_resultleft_tabledomain + (dst_index_multiply_extend_resultleft_table) = (S l)) -> exists dst_positive_multiply_extend_resultleft_table dst_negative_multiply_extend_resultleft_table dst_value_multiply_extend_resultleft_table. ((((exists ff_h_pvs_multiply_extend_resultleft_tableentrypositive. ff_h_pvs_multiply_extend_resultleft_tableentrypositive + S (dst_positive_multiply_extend_resultleft_table) = S ((S (dst_index_multiply_extend_resultleft_table)) * dst_positive_scale_multiply_extend_resultleft_table)) /\ exists ff_q_pvs_multiply_extend_resultleft_tableentrypositive. dst_positive_code_multiply_extend_resultleft_table = ff_q_pvs_multiply_extend_resultleft_tableentrypositive * S ((S (dst_index_multiply_extend_resultleft_table)) * dst_positive_scale_multiply_extend_resultleft_table) + (dst_positive_multiply_extend_resultleft_table))) /\ (((((exists ff_h_pvs_multiply_extend_resultleft_tableentrynegative. ff_h_pvs_multiply_extend_resultleft_tableentrynegative + S (dst_negative_multiply_extend_resultleft_table) = S ((S (dst_index_multiply_extend_resultleft_table)) * dst_negative_scale_multiply_extend_resultleft_table)) /\ exists ff_q_pvs_multiply_extend_resultleft_tableentrynegative. dst_negative_code_multiply_extend_resultleft_table = ff_q_pvs_multiply_extend_resultleft_tableentrynegative * S ((S (dst_index_multiply_extend_resultleft_table)) * dst_negative_scale_multiply_extend_resultleft_table) + (dst_negative_multiply_extend_resultleft_table))) /\ (exists ge_balance_positive_multiply_extend_resultleft_tableentryvalue ge_balance_negative_multiply_extend_resultleft_tableentryvalue. (((((dst_value_multiply_extend_resultleft_table) = 2 * (ge_balance_positive_multiply_extend_resultleft_tableentryvalue) /\ (ge_balance_negative_multiply_extend_resultleft_tableentryvalue) = 0) \/ exists ge_signed_half_multiply_extend_resultleft_tableentryvaluedecode. (((dst_value_multiply_extend_resultleft_table) = 2 * ge_signed_half_multiply_extend_resultleft_tableentryvaluedecode + 1 /\ (ge_balance_positive_multiply_extend_resultleft_tableentryvalue) = 0) /\ (ge_balance_negative_multiply_extend_resultleft_tableentryvalue) = S ge_signed_half_multiply_extend_resultleft_tableentryvaluedecode))) /\ ((dst_positive_multiply_extend_resultleft_table) + ge_balance_negative_multiply_extend_resultleft_tableentryvalue = (dst_negative_multiply_extend_resultleft_table) + ge_balance_positive_multiply_extend_resultleft_tableentryvalue))))))))) /\ (((exists dst_positive_code_multiply_extend_resultright_table dst_positive_scale_multiply_extend_resultright_table dst_negative_code_multiply_extend_resultright_table dst_negative_scale_multiply_extend_resultright_table. (((G) = (((((dst_positive_code_multiply_extend_resultright_table) + (dst_positive_scale_multiply_extend_resultright_table)) * S ((dst_positive_code_multiply_extend_resultright_table) + (dst_positive_scale_multiply_extend_resultright_table)) + ((dst_positive_scale_multiply_extend_resultright_table) + (dst_positive_scale_multiply_extend_resultright_table))) + (((dst_negative_code_multiply_extend_resultright_table) + (dst_negative_scale_multiply_extend_resultright_table)) * S ((dst_negative_code_multiply_extend_resultright_table) + (dst_negative_scale_multiply_extend_resultright_table)) + ((dst_negative_scale_multiply_extend_resultright_table) + (dst_negative_scale_multiply_extend_resultright_table)))) * S ((((dst_positive_code_multiply_extend_resultright_table) + (dst_positive_scale_multiply_extend_resultright_table)) * S ((dst_positive_code_multiply_extend_resultright_table) + (dst_positive_scale_multiply_extend_resultright_table)) + ((dst_positive_scale_multiply_extend_resultright_table) + (dst_positive_scale_multiply_extend_resultright_table))) + (((dst_negative_code_multiply_extend_resultright_table) + (dst_negative_scale_multiply_extend_resultright_table)) * S ((dst_negative_code_multiply_extend_resultright_table) + (dst_negative_scale_multiply_extend_resultright_table)) + ((dst_negative_scale_multiply_extend_resultright_table) + (dst_negative_scale_multiply_extend_resultright_table)))) + ((((dst_negative_code_multiply_extend_resultright_table) + (dst_negative_scale_multiply_extend_resultright_table)) * S ((dst_negative_code_multiply_extend_resultright_table) + (dst_negative_scale_multiply_extend_resultright_table)) + ((dst_negative_scale_multiply_extend_resultright_table) + (dst_negative_scale_multiply_extend_resultright_table))) + (((dst_negative_code_multiply_extend_resultright_table) + (dst_negative_scale_multiply_extend_resultright_table)) * S ((dst_negative_code_multiply_extend_resultright_table) + (dst_negative_scale_multiply_extend_resultright_table)) + ((dst_negative_scale_multiply_extend_resultright_table) + (dst_negative_scale_multiply_extend_resultright_table)))))) /\ (forall dst_index_multiply_extend_resultright_table. (exists pvs_le_gap_multiply_extend_resultright_tabledomain. pvs_le_gap_multiply_extend_resultright_tabledomain + (dst_index_multiply_extend_resultright_table) = (S l)) -> exists dst_positive_multiply_extend_resultright_table dst_negative_multiply_extend_resultright_table dst_value_multiply_extend_resultright_table. ((((exists ff_h_pvs_multiply_extend_resultright_tableentrypositive. ff_h_pvs_multiply_extend_resultright_tableentrypositive + S (dst_positive_multiply_extend_resultright_table) = S ((S (dst_index_multiply_extend_resultright_table)) * dst_positive_scale_multiply_extend_resultright_table)) /\ exists ff_q_pvs_multiply_extend_resultright_tableentrypositive. dst_positive_code_multiply_extend_resultright_table = ff_q_pvs_multiply_extend_resultright_tableentrypositive * S ((S (dst_index_multiply_extend_resultright_table)) * dst_positive_scale_multiply_extend_resultright_table) + (dst_positive_multiply_extend_resultright_table))) /\ (((((exists ff_h_pvs_multiply_extend_resultright_tableentrynegative. ff_h_pvs_multiply_extend_resultright_tableentrynegative + S (dst_negative_multiply_extend_resultright_table) = S ((S (dst_index_multiply_extend_resultright_table)) * dst_negative_scale_multiply_extend_resultright_table)) /\ exists ff_q_pvs_multiply_extend_resultright_tableentrynegative. dst_negative_code_multiply_extend_resultright_table = ff_q_pvs_multiply_extend_resultright_tableentrynegative * S ((S (dst_index_multiply_extend_resultright_table)) * dst_negative_scale_multiply_extend_resultright_table) + (dst_negative_multiply_extend_resultright_table))) /\ (exists ge_balance_positive_multiply_extend_resultright_tableentryvalue ge_balance_negative_multiply_extend_resultright_tableentryvalue. (((((dst_value_multiply_extend_resultright_table) = 2 * (ge_balance_positive_multiply_extend_resultright_tableentryvalue) /\ (ge_balance_negative_multiply_extend_resultright_tableentryvalue) = 0) \/ exists ge_signed_half_multiply_extend_resultright_tableentryvaluedecode. (((dst_value_multiply_extend_resultright_table) = 2 * ge_signed_half_multiply_extend_resultright_tableentryvaluedecode + 1 /\ (ge_balance_positive_multiply_extend_resultright_tableentryvalue) = 0) /\ (ge_balance_negative_multiply_extend_resultright_tableentryvalue) = S ge_signed_half_multiply_extend_resultright_tableentryvaluedecode))) /\ ((dst_positive_multiply_extend_resultright_table) + ge_balance_negative_multiply_extend_resultright_tableentryvalue = (dst_negative_multiply_extend_resultright_table) + ge_balance_positive_multiply_extend_resultright_tableentryvalue))))))))) /\ (((exists dst_positive_code_multiply_extend_resultoutput_table dst_positive_scale_multiply_extend_resultoutput_table dst_negative_code_multiply_extend_resultoutput_table dst_negative_scale_multiply_extend_resultoutput_table. (((K) = (((((dst_positive_code_multiply_extend_resultoutput_table) + (dst_positive_scale_multiply_extend_resultoutput_table)) * S ((dst_positive_code_multiply_extend_resultoutput_table) + (dst_positive_scale_multiply_extend_resultoutput_table)) + ((dst_positive_scale_multiply_extend_resultoutput_table) + (dst_positive_scale_multiply_extend_resultoutput_table))) + (((dst_negative_code_multiply_extend_resultoutput_table) + (dst_negative_scale_multiply_extend_resultoutput_table)) * S ((dst_negative_code_multiply_extend_resultoutput_table) + (dst_negative_scale_multiply_extend_resultoutput_table)) + ((dst_negative_scale_multiply_extend_resultoutput_table) + (dst_negative_scale_multiply_extend_resultoutput_table)))) * S ((((dst_positive_code_multiply_extend_resultoutput_table) + (dst_positive_scale_multiply_extend_resultoutput_table)) * S ((dst_positive_code_multiply_extend_resultoutput_table) + (dst_positive_scale_multiply_extend_resultoutput_table)) + ((dst_positive_scale_multiply_extend_resultoutput_table) + (dst_positive_scale_multiply_extend_resultoutput_table))) + (((dst_negative_code_multiply_extend_resultoutput_table) + (dst_negative_scale_multiply_extend_resultoutput_table)) * S ((dst_negative_code_multiply_extend_resultoutput_table) + (dst_negative_scale_multiply_extend_resultoutput_table)) + ((dst_negative_scale_multiply_extend_resultoutput_table) + (dst_negative_scale_multiply_extend_resultoutput_table)))) + ((((dst_negative_code_multiply_extend_resultoutput_table) + (dst_negative_scale_multiply_extend_resultoutput_table)) * S ((dst_negative_code_multiply_extend_resultoutput_table) + (dst_negative_scale_multiply_extend_resultoutput_table)) + ((dst_negative_scale_multiply_extend_resultoutput_table) + (dst_negative_scale_multiply_extend_resultoutput_table))) + (((dst_negative_code_multiply_extend_resultoutput_table) + (dst_negative_scale_multiply_extend_resultoutput_table)) * S ((dst_negative_code_multiply_extend_resultoutput_table) + (dst_negative_scale_multiply_extend_resultoutput_table)) + ((dst_negative_scale_multiply_extend_resultoutput_table) + (dst_negative_scale_multiply_extend_resultoutput_table)))))) /\ (forall dst_index_multiply_extend_resultoutput_table. (exists pvs_le_gap_multiply_extend_resultoutput_tabledomain. pvs_le_gap_multiply_extend_resultoutput_tabledomain + (dst_index_multiply_extend_resultoutput_table) = (S l)) -> exists dst_positive_multiply_extend_resultoutput_table dst_negative_multiply_extend_resultoutput_table dst_value_multiply_extend_resultoutput_table. ((((exists ff_h_pvs_multiply_extend_resultoutput_tableentrypositive. ff_h_pvs_multiply_extend_resultoutput_tableentrypositive + S (dst_positive_multiply_extend_resultoutput_table) = S ((S (dst_index_multiply_extend_resultoutput_table)) * dst_positive_scale_multiply_extend_resultoutput_table)) /\ exists ff_q_pvs_multiply_extend_resultoutput_tableentrypositive. dst_positive_code_multiply_extend_resultoutput_table = ff_q_pvs_multiply_extend_resultoutput_tableentrypositive * S ((S (dst_index_multiply_extend_resultoutput_table)) * dst_positive_scale_multiply_extend_resultoutput_table) + (dst_positive_multiply_extend_resultoutput_table))) /\ (((((exists ff_h_pvs_multiply_extend_resultoutput_tableentrynegative. ff_h_pvs_multiply_extend_resultoutput_tableentrynegative + S (dst_negative_multiply_extend_resultoutput_table) = S ((S (dst_index_multiply_extend_resultoutput_table)) * dst_negative_scale_multiply_extend_resultoutput_table)) /\ exists ff_q_pvs_multiply_extend_resultoutput_tableentrynegative. dst_negative_code_multiply_extend_resultoutput_table = ff_q_pvs_multiply_extend_resultoutput_tableentrynegative * S ((S (dst_index_multiply_extend_resultoutput_table)) * dst_negative_scale_multiply_extend_resultoutput_table) + (dst_negative_multiply_extend_resultoutput_table))) /\ (exists ge_balance_positive_multiply_extend_resultoutput_tableentryvalue ge_balance_negative_multiply_extend_resultoutput_tableentryvalue. (((((dst_value_multiply_extend_resultoutput_table) = 2 * (ge_balance_positive_multiply_extend_resultoutput_tableentryvalue) /\ (ge_balance_negative_multiply_extend_resultoutput_tableentryvalue) = 0) \/ exists ge_signed_half_multiply_extend_resultoutput_tableentryvaluedecode. (((dst_value_multiply_extend_resultoutput_table) = 2 * ge_signed_half_multiply_extend_resultoutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_multiply_extend_resultoutput_tableentryvalue) = 0) /\ (ge_balance_negative_multiply_extend_resultoutput_tableentryvalue) = S ge_signed_half_multiply_extend_resultoutput_tableentryvaluedecode))) /\ ((dst_positive_multiply_extend_resultoutput_table) + ge_balance_negative_multiply_extend_resultoutput_tableentryvalue = (dst_negative_multiply_extend_resultoutput_table) + ge_balance_positive_multiply_extend_resultoutput_tableentryvalue))))))))) /\ (forall sto_index_multiply_extend_resultentries. (exists pvs_gap_multiply_extend_resultentriesbound. pvs_gap_multiply_extend_resultentriesbound + S (sto_index_multiply_extend_resultentries) = (S l)) -> exists sto_left_multiply_extend_resultentries sto_right_multiply_extend_resultentries sto_output_multiply_extend_resultentries. ((exists dst_positive_code_multiply_extend_resultentriesentryleft dst_positive_scale_multiply_extend_resultentriesentryleft dst_negative_code_multiply_extend_resultentriesentryleft dst_negative_scale_multiply_extend_resultentriesentryleft dst_positive_multiply_extend_resultentriesentryleft dst_negative_multiply_extend_resultentriesentryleft. (((F) = (((((dst_positive_code_multiply_extend_resultentriesentryleft) + (dst_positive_scale_multiply_extend_resultentriesentryleft)) * S ((dst_positive_code_multiply_extend_resultentriesentryleft) + (dst_positive_scale_multiply_extend_resultentriesentryleft)) + ((dst_positive_scale_multiply_extend_resultentriesentryleft) + (dst_positive_scale_multiply_extend_resultentriesentryleft))) + (((dst_negative_code_multiply_extend_resultentriesentryleft) + (dst_negative_scale_multiply_extend_resultentriesentryleft)) * S ((dst_negative_code_multiply_extend_resultentriesentryleft) + (dst_negative_scale_multiply_extend_resultentriesentryleft)) + ((dst_negative_scale_multiply_extend_resultentriesentryleft) + (dst_negative_scale_multiply_extend_resultentriesentryleft)))) * S ((((dst_positive_code_multiply_extend_resultentriesentryleft) + (dst_positive_scale_multiply_extend_resultentriesentryleft)) * S ((dst_positive_code_multiply_extend_resultentriesentryleft) + (dst_positive_scale_multiply_extend_resultentriesentryleft)) + ((dst_positive_scale_multiply_extend_resultentriesentryleft) + (dst_positive_scale_multiply_extend_resultentriesentryleft))) + (((dst_negative_code_multiply_extend_resultentriesentryleft) + (dst_negative_scale_multiply_extend_resultentriesentryleft)) * S ((dst_negative_code_multiply_extend_resultentriesentryleft) + (dst_negative_scale_multiply_extend_resultentriesentryleft)) + ((dst_negative_scale_multiply_extend_resultentriesentryleft) + (dst_negative_scale_multiply_extend_resultentriesentryleft)))) + ((((dst_negative_code_multiply_extend_resultentriesentryleft) + (dst_negative_scale_multiply_extend_resultentriesentryleft)) * S ((dst_negative_code_multiply_extend_resultentriesentryleft) + (dst_negative_scale_multiply_extend_resultentriesentryleft)) + ((dst_negative_scale_multiply_extend_resultentriesentryleft) + (dst_negative_scale_multiply_extend_resultentriesentryleft))) + (((dst_negative_code_multiply_extend_resultentriesentryleft) + (dst_negative_scale_multiply_extend_resultentriesentryleft)) * S ((dst_negative_code_multiply_extend_resultentriesentryleft) + (dst_negative_scale_multiply_extend_resultentriesentryleft)) + ((dst_negative_scale_multiply_extend_resultentriesentryleft) + (dst_negative_scale_multiply_extend_resultentriesentryleft)))))) /\ (((((exists ff_h_pvs_multiply_extend_resultentriesentryleftpositive. ff_h_pvs_multiply_extend_resultentriesentryleftpositive + S (dst_positive_multiply_extend_resultentriesentryleft) = S ((S (sto_index_multiply_extend_resultentries)) * dst_positive_scale_multiply_extend_resultentriesentryleft)) /\ exists ff_q_pvs_multiply_extend_resultentriesentryleftpositive. dst_positive_code_multiply_extend_resultentriesentryleft = ff_q_pvs_multiply_extend_resultentriesentryleftpositive * S ((S (sto_index_multiply_extend_resultentries)) * dst_positive_scale_multiply_extend_resultentriesentryleft) + (dst_positive_multiply_extend_resultentriesentryleft))) /\ (((((exists ff_h_pvs_multiply_extend_resultentriesentryleftnegative. ff_h_pvs_multiply_extend_resultentriesentryleftnegative + S (dst_negative_multiply_extend_resultentriesentryleft) = S ((S (sto_index_multiply_extend_resultentries)) * dst_negative_scale_multiply_extend_resultentriesentryleft)) /\ exists ff_q_pvs_multiply_extend_resultentriesentryleftnegative. dst_negative_code_multiply_extend_resultentriesentryleft = ff_q_pvs_multiply_extend_resultentriesentryleftnegative * S ((S (sto_index_multiply_extend_resultentries)) * dst_negative_scale_multiply_extend_resultentriesentryleft) + (dst_negative_multiply_extend_resultentriesentryleft))) /\ (exists ge_balance_positive_multiply_extend_resultentriesentryleftvalue ge_balance_negative_multiply_extend_resultentriesentryleftvalue. (((((sto_left_multiply_extend_resultentries) = 2 * (ge_balance_positive_multiply_extend_resultentriesentryleftvalue) /\ (ge_balance_negative_multiply_extend_resultentriesentryleftvalue) = 0) \/ exists ge_signed_half_multiply_extend_resultentriesentryleftvaluedecode. (((sto_left_multiply_extend_resultentries) = 2 * ge_signed_half_multiply_extend_resultentriesentryleftvaluedecode + 1 /\ (ge_balance_positive_multiply_extend_resultentriesentryleftvalue) = 0) /\ (ge_balance_negative_multiply_extend_resultentriesentryleftvalue) = S ge_signed_half_multiply_extend_resultentriesentryleftvaluedecode))) /\ ((dst_positive_multiply_extend_resultentriesentryleft) + ge_balance_negative_multiply_extend_resultentriesentryleftvalue = (dst_negative_multiply_extend_resultentriesentryleft) + ge_balance_positive_multiply_extend_resultentriesentryleftvalue))))))))) /\ (((exists dst_positive_code_multiply_extend_resultentriesentryright dst_positive_scale_multiply_extend_resultentriesentryright dst_negative_code_multiply_extend_resultentriesentryright dst_negative_scale_multiply_extend_resultentriesentryright dst_positive_multiply_extend_resultentriesentryright dst_negative_multiply_extend_resultentriesentryright. (((G) = (((((dst_positive_code_multiply_extend_resultentriesentryright) + (dst_positive_scale_multiply_extend_resultentriesentryright)) * S ((dst_positive_code_multiply_extend_resultentriesentryright) + (dst_positive_scale_multiply_extend_resultentriesentryright)) + ((dst_positive_scale_multiply_extend_resultentriesentryright) + (dst_positive_scale_multiply_extend_resultentriesentryright))) + (((dst_negative_code_multiply_extend_resultentriesentryright) + (dst_negative_scale_multiply_extend_resultentriesentryright)) * S ((dst_negative_code_multiply_extend_resultentriesentryright) + (dst_negative_scale_multiply_extend_resultentriesentryright)) + ((dst_negative_scale_multiply_extend_resultentriesentryright) + (dst_negative_scale_multiply_extend_resultentriesentryright)))) * S ((((dst_positive_code_multiply_extend_resultentriesentryright) + (dst_positive_scale_multiply_extend_resultentriesentryright)) * S ((dst_positive_code_multiply_extend_resultentriesentryright) + (dst_positive_scale_multiply_extend_resultentriesentryright)) + ((dst_positive_scale_multiply_extend_resultentriesentryright) + (dst_positive_scale_multiply_extend_resultentriesentryright))) + (((dst_negative_code_multiply_extend_resultentriesentryright) + (dst_negative_scale_multiply_extend_resultentriesentryright)) * S ((dst_negative_code_multiply_extend_resultentriesentryright) + (dst_negative_scale_multiply_extend_resultentriesentryright)) + ((dst_negative_scale_multiply_extend_resultentriesentryright) + (dst_negative_scale_multiply_extend_resultentriesentryright)))) + ((((dst_negative_code_multiply_extend_resultentriesentryright) + (dst_negative_scale_multiply_extend_resultentriesentryright)) * S ((dst_negative_code_multiply_extend_resultentriesentryright) + (dst_negative_scale_multiply_extend_resultentriesentryright)) + ((dst_negative_scale_multiply_extend_resultentriesentryright) + (dst_negative_scale_multiply_extend_resultentriesentryright))) + (((dst_negative_code_multiply_extend_resultentriesentryright) + (dst_negative_scale_multiply_extend_resultentriesentryright)) * S ((dst_negative_code_multiply_extend_resultentriesentryright) + (dst_negative_scale_multiply_extend_resultentriesentryright)) + ((dst_negative_scale_multiply_extend_resultentriesentryright) + (dst_negative_scale_multiply_extend_resultentriesentryright)))))) /\ (((((exists ff_h_pvs_multiply_extend_resultentriesentryrightpositive. ff_h_pvs_multiply_extend_resultentriesentryrightpositive + S (dst_positive_multiply_extend_resultentriesentryright) = S ((S (sto_index_multiply_extend_resultentries)) * dst_positive_scale_multiply_extend_resultentriesentryright)) /\ exists ff_q_pvs_multiply_extend_resultentriesentryrightpositive. dst_positive_code_multiply_extend_resultentriesentryright = ff_q_pvs_multiply_extend_resultentriesentryrightpositive * S ((S (sto_index_multiply_extend_resultentries)) * dst_positive_scale_multiply_extend_resultentriesentryright) + (dst_positive_multiply_extend_resultentriesentryright))) /\ (((((exists ff_h_pvs_multiply_extend_resultentriesentryrightnegative. ff_h_pvs_multiply_extend_resultentriesentryrightnegative + S (dst_negative_multiply_extend_resultentriesentryright) = S ((S (sto_index_multiply_extend_resultentries)) * dst_negative_scale_multiply_extend_resultentriesentryright)) /\ exists ff_q_pvs_multiply_extend_resultentriesentryrightnegative. dst_negative_code_multiply_extend_resultentriesentryright = ff_q_pvs_multiply_extend_resultentriesentryrightnegative * S ((S (sto_index_multiply_extend_resultentries)) * dst_negative_scale_multiply_extend_resultentriesentryright) + (dst_negative_multiply_extend_resultentriesentryright))) /\ (exists ge_balance_positive_multiply_extend_resultentriesentryrightvalue ge_balance_negative_multiply_extend_resultentriesentryrightvalue. (((((sto_right_multiply_extend_resultentries) = 2 * (ge_balance_positive_multiply_extend_resultentriesentryrightvalue) /\ (ge_balance_negative_multiply_extend_resultentriesentryrightvalue) = 0) \/ exists ge_signed_half_multiply_extend_resultentriesentryrightvaluedecode. (((sto_right_multiply_extend_resultentries) = 2 * ge_signed_half_multiply_extend_resultentriesentryrightvaluedecode + 1 /\ (ge_balance_positive_multiply_extend_resultentriesentryrightvalue) = 0) /\ (ge_balance_negative_multiply_extend_resultentriesentryrightvalue) = S ge_signed_half_multiply_extend_resultentriesentryrightvaluedecode))) /\ ((dst_positive_multiply_extend_resultentriesentryright) + ge_balance_negative_multiply_extend_resultentriesentryrightvalue = (dst_negative_multiply_extend_resultentriesentryright) + ge_balance_positive_multiply_extend_resultentriesentryrightvalue))))))))) /\ (((exists dst_positive_code_multiply_extend_resultentriesentryoutput dst_positive_scale_multiply_extend_resultentriesentryoutput dst_negative_code_multiply_extend_resultentriesentryoutput dst_negative_scale_multiply_extend_resultentriesentryoutput dst_positive_multiply_extend_resultentriesentryoutput dst_negative_multiply_extend_resultentriesentryoutput. (((K) = (((((dst_positive_code_multiply_extend_resultentriesentryoutput) + (dst_positive_scale_multiply_extend_resultentriesentryoutput)) * S ((dst_positive_code_multiply_extend_resultentriesentryoutput) + (dst_positive_scale_multiply_extend_resultentriesentryoutput)) + ((dst_positive_scale_multiply_extend_resultentriesentryoutput) + (dst_positive_scale_multiply_extend_resultentriesentryoutput))) + (((dst_negative_code_multiply_extend_resultentriesentryoutput) + (dst_negative_scale_multiply_extend_resultentriesentryoutput)) * S ((dst_negative_code_multiply_extend_resultentriesentryoutput) + (dst_negative_scale_multiply_extend_resultentriesentryoutput)) + ((dst_negative_scale_multiply_extend_resultentriesentryoutput) + (dst_negative_scale_multiply_extend_resultentriesentryoutput)))) * S ((((dst_positive_code_multiply_extend_resultentriesentryoutput) + (dst_positive_scale_multiply_extend_resultentriesentryoutput)) * S ((dst_positive_code_multiply_extend_resultentriesentryoutput) + (dst_positive_scale_multiply_extend_resultentriesentryoutput)) + ((dst_positive_scale_multiply_extend_resultentriesentryoutput) + (dst_positive_scale_multiply_extend_resultentriesentryoutput))) + (((dst_negative_code_multiply_extend_resultentriesentryoutput) + (dst_negative_scale_multiply_extend_resultentriesentryoutput)) * S ((dst_negative_code_multiply_extend_resultentriesentryoutput) + (dst_negative_scale_multiply_extend_resultentriesentryoutput)) + ((dst_negative_scale_multiply_extend_resultentriesentryoutput) + (dst_negative_scale_multiply_extend_resultentriesentryoutput)))) + ((((dst_negative_code_multiply_extend_resultentriesentryoutput) + (dst_negative_scale_multiply_extend_resultentriesentryoutput)) * S ((dst_negative_code_multiply_extend_resultentriesentryoutput) + (dst_negative_scale_multiply_extend_resultentriesentryoutput)) + ((dst_negative_scale_multiply_extend_resultentriesentryoutput) + (dst_negative_scale_multiply_extend_resultentriesentryoutput))) + (((dst_negative_code_multiply_extend_resultentriesentryoutput) + (dst_negative_scale_multiply_extend_resultentriesentryoutput)) * S ((dst_negative_code_multiply_extend_resultentriesentryoutput) + (dst_negative_scale_multiply_extend_resultentriesentryoutput)) + ((dst_negative_scale_multiply_extend_resultentriesentryoutput) + (dst_negative_scale_multiply_extend_resultentriesentryoutput)))))) /\ (((((exists ff_h_pvs_multiply_extend_resultentriesentryoutputpositive. ff_h_pvs_multiply_extend_resultentriesentryoutputpositive + S (dst_positive_multiply_extend_resultentriesentryoutput) = S ((S (sto_index_multiply_extend_resultentries)) * dst_positive_scale_multiply_extend_resultentriesentryoutput)) /\ exists ff_q_pvs_multiply_extend_resultentriesentryoutputpositive. dst_positive_code_multiply_extend_resultentriesentryoutput = ff_q_pvs_multiply_extend_resultentriesentryoutputpositive * S ((S (sto_index_multiply_extend_resultentries)) * dst_positive_scale_multiply_extend_resultentriesentryoutput) + (dst_positive_multiply_extend_resultentriesentryoutput))) /\ (((((exists ff_h_pvs_multiply_extend_resultentriesentryoutputnegative. ff_h_pvs_multiply_extend_resultentriesentryoutputnegative + S (dst_negative_multiply_extend_resultentriesentryoutput) = S ((S (sto_index_multiply_extend_resultentries)) * dst_negative_scale_multiply_extend_resultentriesentryoutput)) /\ exists ff_q_pvs_multiply_extend_resultentriesentryoutputnegative. dst_negative_code_multiply_extend_resultentriesentryoutput = ff_q_pvs_multiply_extend_resultentriesentryoutputnegative * S ((S (sto_index_multiply_extend_resultentries)) * dst_negative_scale_multiply_extend_resultentriesentryoutput) + (dst_negative_multiply_extend_resultentriesentryoutput))) /\ (exists ge_balance_positive_multiply_extend_resultentriesentryoutputvalue ge_balance_negative_multiply_extend_resultentriesentryoutputvalue. (((((sto_output_multiply_extend_resultentries) = 2 * (ge_balance_positive_multiply_extend_resultentriesentryoutputvalue) /\ (ge_balance_negative_multiply_extend_resultentriesentryoutputvalue) = 0) \/ exists ge_signed_half_multiply_extend_resultentriesentryoutputvaluedecode. (((sto_output_multiply_extend_resultentries) = 2 * ge_signed_half_multiply_extend_resultentriesentryoutputvaluedecode + 1 /\ (ge_balance_positive_multiply_extend_resultentriesentryoutputvalue) = 0) /\ (ge_balance_negative_multiply_extend_resultentriesentryoutputvalue) = S ge_signed_half_multiply_extend_resultentriesentryoutputvaluedecode))) /\ ((dst_positive_multiply_extend_resultentriesentryoutput) + ge_balance_negative_multiply_extend_resultentriesentryoutputvalue = (dst_negative_multiply_extend_resultentriesentryoutput) + ge_balance_positive_multiply_extend_resultentriesentryoutputvalue))))))))) /\ (exists sto_ap_multiply_extend_resultentriesentryoperation sto_an_multiply_extend_resultentriesentryoperation sto_bp_multiply_extend_resultentriesentryoperation sto_bn_multiply_extend_resultentriesentryoperation sto_cp_multiply_extend_resultentriesentryoperation sto_cn_multiply_extend_resultentriesentryoperation. (((((sto_left_multiply_extend_resultentries) = 2 * (sto_ap_multiply_extend_resultentriesentryoperation) /\ (sto_an_multiply_extend_resultentriesentryoperation) = 0) \/ exists ge_signed_half_multiply_extend_resultentriesentryoperationleft. (((sto_left_multiply_extend_resultentries) = 2 * ge_signed_half_multiply_extend_resultentriesentryoperationleft + 1 /\ (sto_ap_multiply_extend_resultentriesentryoperation) = 0) /\ (sto_an_multiply_extend_resultentriesentryoperation) = S ge_signed_half_multiply_extend_resultentriesentryoperationleft))) /\ ((((((sto_right_multiply_extend_resultentries) = 2 * (sto_bp_multiply_extend_resultentriesentryoperation) /\ (sto_bn_multiply_extend_resultentriesentryoperation) = 0) \/ exists ge_signed_half_multiply_extend_resultentriesentryoperationright. (((sto_right_multiply_extend_resultentries) = 2 * ge_signed_half_multiply_extend_resultentriesentryoperationright + 1 /\ (sto_bp_multiply_extend_resultentriesentryoperation) = 0) /\ (sto_bn_multiply_extend_resultentriesentryoperation) = S ge_signed_half_multiply_extend_resultentriesentryoperationright))) /\ ((((((sto_output_multiply_extend_resultentries) = 2 * (sto_cp_multiply_extend_resultentriesentryoperation) /\ (sto_cn_multiply_extend_resultentriesentryoperation) = 0) \/ exists ge_signed_half_multiply_extend_resultentriesentryoperationoutput. (((sto_output_multiply_extend_resultentries) = 2 * ge_signed_half_multiply_extend_resultentriesentryoperationoutput + 1 /\ (sto_cp_multiply_extend_resultentriesentryoperation) = 0) /\ (sto_cn_multiply_extend_resultentriesentryoperation) = S ge_signed_half_multiply_extend_resultentriesentryoperationoutput))) /\ ((sto_ap_multiply_extend_resultentriesentryoperation * sto_bp_multiply_extend_resultentriesentryoperation + sto_an_multiply_extend_resultentriesentryoperation * sto_bn_multiply_extend_resultentriesentryoperation) + sto_cn_multiply_extend_resultentriesentryoperation = (sto_ap_multiply_extend_resultentriesentryoperation * sto_bn_multiply_extend_resultentriesentryoperation + sto_an_multiply_extend_resultentriesentryoperation * sto_bp_multiply_extend_resultentriesentryoperation) + sto_cp_multiply_extend_resultentriesentryoperation)))))))))))))))))))Constructive proof overview
Generated structural guide
The actual pointwise multiply graph extends across a preserved strict prefix and a genuine new entry, without equating table codes.
The unchanged tactic script uses 4 declared prerequisites and contains 102 exact native proof lines.
Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not Stable
Proof neighborhood
Direct dependencies
WS0001 signed_table_domain_resize finite_lt_succ_eq_or_lt Stable theorem; checked-use authorized arithmetic_signed_table_equal_entry_transport Alpha theorem; checked-use authorized le_refl Stable theorem; checked-use authorizedDirect dependents
Formal native tactic body
Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.
Read the argument
Proof checkpoints
This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.
Named ingredients (1)
01Fix variables and assumptionsL1–10
02Fix variables and assumptionsL11–15
03Separate the logical casesL16–19
04Use earlier factsL20–24
05Separate the logical casesL25–25
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L25
split
06Use earlier factsL26–30
07Separate the logical casesL31–31
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L31
split
08Use earlier factsL32–36
09Fix variables and assumptionsL37–38
10Establish hcaseL39–43
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply finite lt succ eq or lt.
11Separate the logical casesL44–44
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L44
cases hcase
12Calculate and transport equalitiesL45–54
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
13Calculate and transport equalitiesL55–56
14Construct an explicit witnessL57–59
15Separate the logical casesL60–60
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L60
split
16Use earlier factsL61–61
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L61
exact he0
17Separate the logical casesL62–62
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L62
split
18Use earlier factsL63–63
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L63
exact he1
19Separate the logical casesL64–64
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L64
split
20Use earlier factsL65–66
21Establish holdL67–70
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hop right right right.
22Separate the logical casesL71–76
23Construct an explicit witnessL77–79
24Separate the logical casesL80–80
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L80
split
25Use earlier factsL81–81
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L81
exact hold_witness_witness_witness_left
26Separate the logical casesL82–82
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L82
split
27Use earlier factsL83–83
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L83
exact hold_witness_witness_witness_right_left
28Separate the logical casesL84–84
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L84
split
29Use earlier factsL85–94
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L85
specialize arithmetic_signed_table_equal_entry_transport (i) - L86
specialize arithmetic_signed_table_equal_entry_transport (H) - L87
specialize arithmetic_signed_table_equal_entry_transport (K) - L88
specialize arithmetic_signed_table_equal_entry_transport (l) - L89
specialize arithmetic_signed_table_equal_entry_transport (i) - L90
specialize arithmetic_signed_table_equal_entry_transport (x2) - L91
apply arithmetic_signed_table_equal_entry_transport - L92
specialize signed_table_domain_resize (l) - L93
specialize signed_table_domain_resize (i) - L94
specialize signed_table_domain_resize (K)
30Use earlier factsL95–102
Instantiate or apply named facts and discharge the corresponding proof obligations.
Original exact command ledger · 102 lines
- 0001
intro F - 0002
intro G - 0003
intro H - 0004
intro K - 0005
intro l - 0006
intro a - 0007
intro b - 0008
intro c - 0009
intro hop - 0010
intro hK - 0011
intro hequal - 0012
intro he0 - 0013
intro he1 - 0014
intro he2 - 0015
intro hvalue - 0016
cases hop - 0017
cases hop_right - 0018
cases hop_right_right - 0019
split - 0020
specialize signed_table_domain_resize (l) - 0021
specialize signed_table_domain_resize (S l) - 0022
specialize signed_table_domain_resize (F) - 0023
apply signed_table_domain_resize - 0024
exact hop_left - 0025
split - 0026
specialize signed_table_domain_resize (l) - 0027
specialize signed_table_domain_resize (S l) - 0028
specialize signed_table_domain_resize (G) - 0029
apply signed_table_domain_resize - 0030
exact hop_right_left - 0031
split - 0032
specialize signed_table_domain_resize (l) - 0033
specialize signed_table_domain_resize (S l) - 0034
specialize signed_table_domain_resize (K) - 0035
apply signed_table_domain_resize - 0036
exact hK - 0037
intro i - 0038
intro hi - 0039
have hcase : i = l \/ (exists pvs_gap_multiply_extend_cases. pvs_gap_multiply_extend_cases + S (i) = (l)) - 0040
specialize finite_lt_succ_eq_or_lt (l) - 0041
specialize finite_lt_succ_eq_or_lt (i) - 0042
apply finite_lt_succ_eq_or_lt - 0043
exact hi - 0044
cases hcase - 0045
rewrite hcase_left - 0046
rewrite hcase_left - 0047
rewrite hcase_left - 0048
rewrite hcase_left - 0049
rewrite hcase_left - 0050
rewrite hcase_left - 0051
rewrite hcase_left - 0052
rewrite hcase_left - 0053
rewrite hcase_left - 0054
rewrite hcase_left - 0055
rewrite hcase_left - 0056
rewrite hcase_left - 0057
exists a - 0058
exists b - 0059
exists c - 0060
split - 0061
exact he0 - 0062
split - 0063
exact he1 - 0064
split - 0065
exact he2 - 0066
exact hvalue - 0067
have hold : exists u v w. ((exists dst_positive_code_multiply_extend_old_entryleft dst_positive_scale_multiply_extend_old_entryleft dst_negative_code_multiply_extend_old_entryleft dst_negative_scale_multiply_extend_old_entryleft dst_positive_multiply_extend_old_entryleft dst_negative_multiply_extend_old_entryleft. (((F) = (((((dst_positive_code_multiply_extend_old_entryleft) + (dst_positive_scale_multiply_extend_old_entryleft)) * S ((dst_positive_code_multiply_extend_old_entryleft) + (dst_positive_scale_multiply_extend_old_entryleft)) + ((dst_positive_scale_multiply_extend_old_entryleft) + (dst_positive_scale_multiply_extend_old_entryleft))) + (((dst_negative_code_multiply_extend_old_entryleft) + (dst_negative_scale_multiply_extend_old_entryleft)) * S ((dst_negative_code_multiply_extend_old_entryleft) + (dst_negative_scale_multiply_extend_old_entryleft)) + ((dst_negative_scale_multiply_extend_old_entryleft) + (dst_negative_scale_multiply_extend_old_entryleft)))) * S ((((dst_positive_code_multiply_extend_old_entryleft) + (dst_positive_scale_multiply_extend_old_entryleft)) * S ((dst_positive_code_multiply_extend_old_entryleft) + (dst_positive_scale_multiply_extend_old_entryleft)) + ((dst_positive_scale_multiply_extend_old_entryleft) + (dst_positive_scale_multiply_extend_old_entryleft))) + (((dst_negative_code_multiply_extend_old_entryleft) + (dst_negative_scale_multiply_extend_old_entryleft)) * S ((dst_negative_code_multiply_extend_old_entryleft) + (dst_negative_scale_multiply_extend_old_entryleft)) + ((dst_negative_scale_multiply_extend_old_entryleft) + (dst_negative_scale_multiply_extend_old_entryleft)))) + ((((dst_negative_code_multiply_extend_old_entryleft) + (dst_negative_scale_multiply_extend_old_entryleft)) * S ((dst_negative_code_multiply_extend_old_entryleft) + (dst_negative_scale_multiply_extend_old_entryleft)) + ((dst_negative_scale_multiply_extend_old_entryleft) + (dst_negative_scale_multiply_extend_old_entryleft))) + (((dst_negative_code_multiply_extend_old_entryleft) + (dst_negative_scale_multiply_extend_old_entryleft)) * S ((dst_negative_code_multiply_extend_old_entryleft) + (dst_negative_scale_multiply_extend_old_entryleft)) + ((dst_negative_scale_multiply_extend_old_entryleft) + (dst_negative_scale_multiply_extend_old_entryleft)))))) /\ (((((exists ff_h_pvs_multiply_extend_old_entryleftpositive. ff_h_pvs_multiply_extend_old_entryleftpositive + S (dst_positive_multiply_extend_old_entryleft) = S ((S (i)) * dst_positive_scale_multiply_extend_old_entryleft)) /\ exists ff_q_pvs_multiply_extend_old_entryleftpositive. dst_positive_code_multiply_extend_old_entryleft = ff_q_pvs_multiply_extend_old_entryleftpositive * S ((S (i)) * dst_positive_scale_multiply_extend_old_entryleft) + (dst_positive_multiply_extend_old_entryleft))) /\ (((((exists ff_h_pvs_multiply_extend_old_entryleftnegative. ff_h_pvs_multiply_extend_old_entryleftnegative + S (dst_negative_multiply_extend_old_entryleft) = S ((S (i)) * dst_negative_scale_multiply_extend_old_entryleft)) /\ exists ff_q_pvs_multiply_extend_old_entryleftnegative. dst_negative_code_multiply_extend_old_entryleft = ff_q_pvs_multiply_extend_old_entryleftnegative * S ((S (i)) * dst_negative_scale_multiply_extend_old_entryleft) + (dst_negative_multiply_extend_old_entryleft))) /\ (exists ge_balance_positive_multiply_extend_old_entryleftvalue ge_balance_negative_multiply_extend_old_entryleftvalue. (((((u) = 2 * (ge_balance_positive_multiply_extend_old_entryleftvalue) /\ (ge_balance_negative_multiply_extend_old_entryleftvalue) = 0) \/ exists ge_signed_half_multiply_extend_old_entryleftvaluedecode. (((u) = 2 * ge_signed_half_multiply_extend_old_entryleftvaluedecode + 1 /\ (ge_balance_positive_multiply_extend_old_entryleftvalue) = 0) /\ (ge_balance_negative_multiply_extend_old_entryleftvalue) = S ge_signed_half_multiply_extend_old_entryleftvaluedecode))) /\ ((dst_positive_multiply_extend_old_entryleft) + ge_balance_negative_multiply_extend_old_entryleftvalue = (dst_negative_multiply_extend_old_entryleft) + ge_balance_positive_multiply_extend_old_entryleftvalue))))))))) /\ (((exists dst_positive_code_multiply_extend_old_entryright dst_positive_scale_multiply_extend_old_entryright dst_negative_code_multiply_extend_old_entryright dst_negative_scale_multiply_extend_old_entryright dst_positive_multiply_extend_old_entryright dst_negative_multiply_extend_old_entryright. (((G) = (((((dst_positive_code_multiply_extend_old_entryright) + (dst_positive_scale_multiply_extend_old_entryright)) * S ((dst_positive_code_multiply_extend_old_entryright) + (dst_positive_scale_multiply_extend_old_entryright)) + ((dst_positive_scale_multiply_extend_old_entryright) + (dst_positive_scale_multiply_extend_old_entryright))) + (((dst_negative_code_multiply_extend_old_entryright) + (dst_negative_scale_multiply_extend_old_entryright)) * S ((dst_negative_code_multiply_extend_old_entryright) + (dst_negative_scale_multiply_extend_old_entryright)) + ((dst_negative_scale_multiply_extend_old_entryright) + (dst_negative_scale_multiply_extend_old_entryright)))) * S ((((dst_positive_code_multiply_extend_old_entryright) + (dst_positive_scale_multiply_extend_old_entryright)) * S ((dst_positive_code_multiply_extend_old_entryright) + (dst_positive_scale_multiply_extend_old_entryright)) + ((dst_positive_scale_multiply_extend_old_entryright) + (dst_positive_scale_multiply_extend_old_entryright))) + (((dst_negative_code_multiply_extend_old_entryright) + (dst_negative_scale_multiply_extend_old_entryright)) * S ((dst_negative_code_multiply_extend_old_entryright) + (dst_negative_scale_multiply_extend_old_entryright)) + ((dst_negative_scale_multiply_extend_old_entryright) + (dst_negative_scale_multiply_extend_old_entryright)))) + ((((dst_negative_code_multiply_extend_old_entryright) + (dst_negative_scale_multiply_extend_old_entryright)) * S ((dst_negative_code_multiply_extend_old_entryright) + (dst_negative_scale_multiply_extend_old_entryright)) + ((dst_negative_scale_multiply_extend_old_entryright) + (dst_negative_scale_multiply_extend_old_entryright))) + (((dst_negative_code_multiply_extend_old_entryright) + (dst_negative_scale_multiply_extend_old_entryright)) * S ((dst_negative_code_multiply_extend_old_entryright) + (dst_negative_scale_multiply_extend_old_entryright)) + ((dst_negative_scale_multiply_extend_old_entryright) + (dst_negative_scale_multiply_extend_old_entryright)))))) /\ (((((exists ff_h_pvs_multiply_extend_old_entryrightpositive. ff_h_pvs_multiply_extend_old_entryrightpositive + S (dst_positive_multiply_extend_old_entryright) = S ((S (i)) * dst_positive_scale_multiply_extend_old_entryright)) /\ exists ff_q_pvs_multiply_extend_old_entryrightpositive. dst_positive_code_multiply_extend_old_entryright = ff_q_pvs_multiply_extend_old_entryrightpositive * S ((S (i)) * dst_positive_scale_multiply_extend_old_entryright) + (dst_positive_multiply_extend_old_entryright))) /\ (((((exists ff_h_pvs_multiply_extend_old_entryrightnegative. ff_h_pvs_multiply_extend_old_entryrightnegative + S (dst_negative_multiply_extend_old_entryright) = S ((S (i)) * dst_negative_scale_multiply_extend_old_entryright)) /\ exists ff_q_pvs_multiply_extend_old_entryrightnegative. dst_negative_code_multiply_extend_old_entryright = ff_q_pvs_multiply_extend_old_entryrightnegative * S ((S (i)) * dst_negative_scale_multiply_extend_old_entryright) + (dst_negative_multiply_extend_old_entryright))) /\ (exists ge_balance_positive_multiply_extend_old_entryrightvalue ge_balance_negative_multiply_extend_old_entryrightvalue. (((((v) = 2 * (ge_balance_positive_multiply_extend_old_entryrightvalue) /\ (ge_balance_negative_multiply_extend_old_entryrightvalue) = 0) \/ exists ge_signed_half_multiply_extend_old_entryrightvaluedecode. (((v) = 2 * ge_signed_half_multiply_extend_old_entryrightvaluedecode + 1 /\ (ge_balance_positive_multiply_extend_old_entryrightvalue) = 0) /\ (ge_balance_negative_multiply_extend_old_entryrightvalue) = S ge_signed_half_multiply_extend_old_entryrightvaluedecode))) /\ ((dst_positive_multiply_extend_old_entryright) + ge_balance_negative_multiply_extend_old_entryrightvalue = (dst_negative_multiply_extend_old_entryright) + ge_balance_positive_multiply_extend_old_entryrightvalue))))))))) /\ (((exists dst_positive_code_multiply_extend_old_entryoutput dst_positive_scale_multiply_extend_old_entryoutput dst_negative_code_multiply_extend_old_entryoutput dst_negative_scale_multiply_extend_old_entryoutput dst_positive_multiply_extend_old_entryoutput dst_negative_multiply_extend_old_entryoutput. (((H) = (((((dst_positive_code_multiply_extend_old_entryoutput) + (dst_positive_scale_multiply_extend_old_entryoutput)) * S ((dst_positive_code_multiply_extend_old_entryoutput) + (dst_positive_scale_multiply_extend_old_entryoutput)) + ((dst_positive_scale_multiply_extend_old_entryoutput) + (dst_positive_scale_multiply_extend_old_entryoutput))) + (((dst_negative_code_multiply_extend_old_entryoutput) + (dst_negative_scale_multiply_extend_old_entryoutput)) * S ((dst_negative_code_multiply_extend_old_entryoutput) + (dst_negative_scale_multiply_extend_old_entryoutput)) + ((dst_negative_scale_multiply_extend_old_entryoutput) + (dst_negative_scale_multiply_extend_old_entryoutput)))) * S ((((dst_positive_code_multiply_extend_old_entryoutput) + (dst_positive_scale_multiply_extend_old_entryoutput)) * S ((dst_positive_code_multiply_extend_old_entryoutput) + (dst_positive_scale_multiply_extend_old_entryoutput)) + ((dst_positive_scale_multiply_extend_old_entryoutput) + (dst_positive_scale_multiply_extend_old_entryoutput))) + (((dst_negative_code_multiply_extend_old_entryoutput) + (dst_negative_scale_multiply_extend_old_entryoutput)) * S ((dst_negative_code_multiply_extend_old_entryoutput) + (dst_negative_scale_multiply_extend_old_entryoutput)) + ((dst_negative_scale_multiply_extend_old_entryoutput) + (dst_negative_scale_multiply_extend_old_entryoutput)))) + ((((dst_negative_code_multiply_extend_old_entryoutput) + (dst_negative_scale_multiply_extend_old_entryoutput)) * S ((dst_negative_code_multiply_extend_old_entryoutput) + (dst_negative_scale_multiply_extend_old_entryoutput)) + ((dst_negative_scale_multiply_extend_old_entryoutput) + (dst_negative_scale_multiply_extend_old_entryoutput))) + (((dst_negative_code_multiply_extend_old_entryoutput) + (dst_negative_scale_multiply_extend_old_entryoutput)) * S ((dst_negative_code_multiply_extend_old_entryoutput) + (dst_negative_scale_multiply_extend_old_entryoutput)) + ((dst_negative_scale_multiply_extend_old_entryoutput) + (dst_negative_scale_multiply_extend_old_entryoutput)))))) /\ (((((exists ff_h_pvs_multiply_extend_old_entryoutputpositive. ff_h_pvs_multiply_extend_old_entryoutputpositive + S (dst_positive_multiply_extend_old_entryoutput) = S ((S (i)) * dst_positive_scale_multiply_extend_old_entryoutput)) /\ exists ff_q_pvs_multiply_extend_old_entryoutputpositive. dst_positive_code_multiply_extend_old_entryoutput = ff_q_pvs_multiply_extend_old_entryoutputpositive * S ((S (i)) * dst_positive_scale_multiply_extend_old_entryoutput) + (dst_positive_multiply_extend_old_entryoutput))) /\ (((((exists ff_h_pvs_multiply_extend_old_entryoutputnegative. ff_h_pvs_multiply_extend_old_entryoutputnegative + S (dst_negative_multiply_extend_old_entryoutput) = S ((S (i)) * dst_negative_scale_multiply_extend_old_entryoutput)) /\ exists ff_q_pvs_multiply_extend_old_entryoutputnegative. dst_negative_code_multiply_extend_old_entryoutput = ff_q_pvs_multiply_extend_old_entryoutputnegative * S ((S (i)) * dst_negative_scale_multiply_extend_old_entryoutput) + (dst_negative_multiply_extend_old_entryoutput))) /\ (exists ge_balance_positive_multiply_extend_old_entryoutputvalue ge_balance_negative_multiply_extend_old_entryoutputvalue. (((((w) = 2 * (ge_balance_positive_multiply_extend_old_entryoutputvalue) /\ (ge_balance_negative_multiply_extend_old_entryoutputvalue) = 0) \/ exists ge_signed_half_multiply_extend_old_entryoutputvaluedecode. (((w) = 2 * ge_signed_half_multiply_extend_old_entryoutputvaluedecode + 1 /\ (ge_balance_positive_multiply_extend_old_entryoutputvalue) = 0) /\ (ge_balance_negative_multiply_extend_old_entryoutputvalue) = S ge_signed_half_multiply_extend_old_entryoutputvaluedecode))) /\ ((dst_positive_multiply_extend_old_entryoutput) + ge_balance_negative_multiply_extend_old_entryoutputvalue = (dst_negative_multiply_extend_old_entryoutput) + ge_balance_positive_multiply_extend_old_entryoutputvalue))))))))) /\ (exists sto_ap_multiply_extend_old_entryoperation sto_an_multiply_extend_old_entryoperation sto_bp_multiply_extend_old_entryoperation sto_bn_multiply_extend_old_entryoperation sto_cp_multiply_extend_old_entryoperation sto_cn_multiply_extend_old_entryoperation. (((((u) = 2 * (sto_ap_multiply_extend_old_entryoperation) /\ (sto_an_multiply_extend_old_entryoperation) = 0) \/ exists ge_signed_half_multiply_extend_old_entryoperationleft. (((u) = 2 * ge_signed_half_multiply_extend_old_entryoperationleft + 1 /\ (sto_ap_multiply_extend_old_entryoperation) = 0) /\ (sto_an_multiply_extend_old_entryoperation) = S ge_signed_half_multiply_extend_old_entryoperationleft))) /\ ((((((v) = 2 * (sto_bp_multiply_extend_old_entryoperation) /\ (sto_bn_multiply_extend_old_entryoperation) = 0) \/ exists ge_signed_half_multiply_extend_old_entryoperationright. (((v) = 2 * ge_signed_half_multiply_extend_old_entryoperationright + 1 /\ (sto_bp_multiply_extend_old_entryoperation) = 0) /\ (sto_bn_multiply_extend_old_entryoperation) = S ge_signed_half_multiply_extend_old_entryoperationright))) /\ ((((((w) = 2 * (sto_cp_multiply_extend_old_entryoperation) /\ (sto_cn_multiply_extend_old_entryoperation) = 0) \/ exists ge_signed_half_multiply_extend_old_entryoperationoutput. (((w) = 2 * ge_signed_half_multiply_extend_old_entryoperationoutput + 1 /\ (sto_cp_multiply_extend_old_entryoperation) = 0) /\ (sto_cn_multiply_extend_old_entryoperation) = S ge_signed_half_multiply_extend_old_entryoperationoutput))) /\ ((sto_ap_multiply_extend_old_entryoperation * sto_bp_multiply_extend_old_entryoperation + sto_an_multiply_extend_old_entryoperation * sto_bn_multiply_extend_old_entryoperation) + sto_cn_multiply_extend_old_entryoperation = (sto_ap_multiply_extend_old_entryoperation * sto_bn_multiply_extend_old_entryoperation + sto_an_multiply_extend_old_entryoperation * sto_bp_multiply_extend_old_entryoperation) + sto_cp_multiply_extend_old_entryoperation)))))))))))) - 0068
specialize hop_right_right_right (i) - 0069
apply hop_right_right_right - 0070
exact hcase_right - 0071
cases hold - 0072
cases hold_witness - 0073
cases hold_witness_witness - 0074
cases hold_witness_witness_witness - 0075
cases hold_witness_witness_witness_right - 0076
cases hold_witness_witness_witness_right_right - 0077
exists x - 0078
exists x1 - 0079
exists x2 - 0080
split - 0081
exact hold_witness_witness_witness_left - 0082
split - 0083
exact hold_witness_witness_witness_right_left - 0084
split - 0085
specialize arithmetic_signed_table_equal_entry_transport (i) - 0086
specialize arithmetic_signed_table_equal_entry_transport (H) - 0087
specialize arithmetic_signed_table_equal_entry_transport (K) - 0088
specialize arithmetic_signed_table_equal_entry_transport (l) - 0089
specialize arithmetic_signed_table_equal_entry_transport (i) - 0090
specialize arithmetic_signed_table_equal_entry_transport (x2) - 0091
apply arithmetic_signed_table_equal_entry_transport - 0092
specialize signed_table_domain_resize (l) - 0093
specialize signed_table_domain_resize (i) - 0094
specialize signed_table_domain_resize (K) - 0095
apply signed_table_domain_resize - 0096
exact hK - 0097
exact hequal - 0098
specialize le_refl (i) - 0099
apply le_refl - 0100
exact hcase_right - 0101
exact hold_witness_witness_witness_right_right_left - 0102
exact hold_witness_witness_witness_right_right_right