WS0013

signed_table_multiply_exists

Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

Ordinary finite induction constructs both beta output streams and their actual packed table for pointwise multiply; no finite-choice or supplied-table oracle is used.

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 l F G. (exists dst_positive_code_multiply_exists_input0 dst_positive_scale_multiply_exists_input0 dst_negative_code_multiply_exists_input0 dst_negative_scale_multiply_exists_input0. (((F) = (((((dst_positive_code_multiply_exists_input0) + (dst_positive_scale_multiply_exists_input0)) * S ((dst_positive_code_multiply_exists_input0) + (dst_positive_scale_multiply_exists_input0)) + ((dst_positive_scale_multiply_exists_input0) + (dst_positive_scale_multiply_exists_input0))) + (((dst_negative_code_multiply_exists_input0) + (dst_negative_scale_multiply_exists_input0)) * S ((dst_negative_code_multiply_exists_input0) + (dst_negative_scale_multiply_exists_input0)) + ((dst_negative_scale_multiply_exists_input0) + (dst_negative_scale_multiply_exists_input0)))) * S ((((dst_positive_code_multiply_exists_input0) + (dst_positive_scale_multiply_exists_input0)) * S ((dst_positive_code_multiply_exists_input0) + (dst_positive_scale_multiply_exists_input0)) + ((dst_positive_scale_multiply_exists_input0) + (dst_positive_scale_multiply_exists_input0))) + (((dst_negative_code_multiply_exists_input0) + (dst_negative_scale_multiply_exists_input0)) * S ((dst_negative_code_multiply_exists_input0) + (dst_negative_scale_multiply_exists_input0)) + ((dst_negative_scale_multiply_exists_input0) + (dst_negative_scale_multiply_exists_input0)))) + ((((dst_negative_code_multiply_exists_input0) + (dst_negative_scale_multiply_exists_input0)) * S ((dst_negative_code_multiply_exists_input0) + (dst_negative_scale_multiply_exists_input0)) + ((dst_negative_scale_multiply_exists_input0) + (dst_negative_scale_multiply_exists_input0))) + (((dst_negative_code_multiply_exists_input0) + (dst_negative_scale_multiply_exists_input0)) * S ((dst_negative_code_multiply_exists_input0) + (dst_negative_scale_multiply_exists_input0)) + ((dst_negative_scale_multiply_exists_input0) + (dst_negative_scale_multiply_exists_input0)))))) /\ (forall dst_index_multiply_exists_input0. (exists pvs_le_gap_multiply_exists_input0domain. pvs_le_gap_multiply_exists_input0domain + (dst_index_multiply_exists_input0) = (l)) -> exists dst_positive_multiply_exists_input0 dst_negative_multiply_exists_input0 dst_value_multiply_exists_input0. ((((exists ff_h_pvs_multiply_exists_input0entrypositive. ff_h_pvs_multiply_exists_input0entrypositive + S (dst_positive_multiply_exists_input0) = S ((S (dst_index_multiply_exists_input0)) * dst_positive_scale_multiply_exists_input0)) /\ exists ff_q_pvs_multiply_exists_input0entrypositive. dst_positive_code_multiply_exists_input0 = ff_q_pvs_multiply_exists_input0entrypositive * S ((S (dst_index_multiply_exists_input0)) * dst_positive_scale_multiply_exists_input0) + (dst_positive_multiply_exists_input0))) /\ (((((exists ff_h_pvs_multiply_exists_input0entrynegative. ff_h_pvs_multiply_exists_input0entrynegative + S (dst_negative_multiply_exists_input0) = S ((S (dst_index_multiply_exists_input0)) * dst_negative_scale_multiply_exists_input0)) /\ exists ff_q_pvs_multiply_exists_input0entrynegative. dst_negative_code_multiply_exists_input0 = ff_q_pvs_multiply_exists_input0entrynegative * S ((S (dst_index_multiply_exists_input0)) * dst_negative_scale_multiply_exists_input0) + (dst_negative_multiply_exists_input0))) /\ (exists ge_balance_positive_multiply_exists_input0entryvalue ge_balance_negative_multiply_exists_input0entryvalue. (((((dst_value_multiply_exists_input0) = 2 * (ge_balance_positive_multiply_exists_input0entryvalue) /\ (ge_balance_negative_multiply_exists_input0entryvalue) = 0) \/ exists ge_signed_half_multiply_exists_input0entryvaluedecode. (((dst_value_multiply_exists_input0) = 2 * ge_signed_half_multiply_exists_input0entryvaluedecode + 1 /\ (ge_balance_positive_multiply_exists_input0entryvalue) = 0) /\ (ge_balance_negative_multiply_exists_input0entryvalue) = S ge_signed_half_multiply_exists_input0entryvaluedecode))) /\ ((dst_positive_multiply_exists_input0) + ge_balance_negative_multiply_exists_input0entryvalue = (dst_negative_multiply_exists_input0) + ge_balance_positive_multiply_exists_input0entryvalue))))))))) -> (exists dst_positive_code_multiply_exists_input1 dst_positive_scale_multiply_exists_input1 dst_negative_code_multiply_exists_input1 dst_negative_scale_multiply_exists_input1. (((G) = (((((dst_positive_code_multiply_exists_input1) + (dst_positive_scale_multiply_exists_input1)) * S ((dst_positive_code_multiply_exists_input1) + (dst_positive_scale_multiply_exists_input1)) + ((dst_positive_scale_multiply_exists_input1) + (dst_positive_scale_multiply_exists_input1))) + (((dst_negative_code_multiply_exists_input1) + (dst_negative_scale_multiply_exists_input1)) * S ((dst_negative_code_multiply_exists_input1) + (dst_negative_scale_multiply_exists_input1)) + ((dst_negative_scale_multiply_exists_input1) + (dst_negative_scale_multiply_exists_input1)))) * S ((((dst_positive_code_multiply_exists_input1) + (dst_positive_scale_multiply_exists_input1)) * S ((dst_positive_code_multiply_exists_input1) + (dst_positive_scale_multiply_exists_input1)) + ((dst_positive_scale_multiply_exists_input1) + (dst_positive_scale_multiply_exists_input1))) + (((dst_negative_code_multiply_exists_input1) + (dst_negative_scale_multiply_exists_input1)) * S ((dst_negative_code_multiply_exists_input1) + (dst_negative_scale_multiply_exists_input1)) + ((dst_negative_scale_multiply_exists_input1) + (dst_negative_scale_multiply_exists_input1)))) + ((((dst_negative_code_multiply_exists_input1) + (dst_negative_scale_multiply_exists_input1)) * S ((dst_negative_code_multiply_exists_input1) + (dst_negative_scale_multiply_exists_input1)) + ((dst_negative_scale_multiply_exists_input1) + (dst_negative_scale_multiply_exists_input1))) + (((dst_negative_code_multiply_exists_input1) + (dst_negative_scale_multiply_exists_input1)) * S ((dst_negative_code_multiply_exists_input1) + (dst_negative_scale_multiply_exists_input1)) + ((dst_negative_scale_multiply_exists_input1) + (dst_negative_scale_multiply_exists_input1)))))) /\ (forall dst_index_multiply_exists_input1. (exists pvs_le_gap_multiply_exists_input1domain. pvs_le_gap_multiply_exists_input1domain + (dst_index_multiply_exists_input1) = (l)) -> exists dst_positive_multiply_exists_input1 dst_negative_multiply_exists_input1 dst_value_multiply_exists_input1. ((((exists ff_h_pvs_multiply_exists_input1entrypositive. ff_h_pvs_multiply_exists_input1entrypositive + S (dst_positive_multiply_exists_input1) = S ((S (dst_index_multiply_exists_input1)) * dst_positive_scale_multiply_exists_input1)) /\ exists ff_q_pvs_multiply_exists_input1entrypositive. dst_positive_code_multiply_exists_input1 = ff_q_pvs_multiply_exists_input1entrypositive * S ((S (dst_index_multiply_exists_input1)) * dst_positive_scale_multiply_exists_input1) + (dst_positive_multiply_exists_input1))) /\ (((((exists ff_h_pvs_multiply_exists_input1entrynegative. ff_h_pvs_multiply_exists_input1entrynegative + S (dst_negative_multiply_exists_input1) = S ((S (dst_index_multiply_exists_input1)) * dst_negative_scale_multiply_exists_input1)) /\ exists ff_q_pvs_multiply_exists_input1entrynegative. dst_negative_code_multiply_exists_input1 = ff_q_pvs_multiply_exists_input1entrynegative * S ((S (dst_index_multiply_exists_input1)) * dst_negative_scale_multiply_exists_input1) + (dst_negative_multiply_exists_input1))) /\ (exists ge_balance_positive_multiply_exists_input1entryvalue ge_balance_negative_multiply_exists_input1entryvalue. (((((dst_value_multiply_exists_input1) = 2 * (ge_balance_positive_multiply_exists_input1entryvalue) /\ (ge_balance_negative_multiply_exists_input1entryvalue) = 0) \/ exists ge_signed_half_multiply_exists_input1entryvaluedecode. (((dst_value_multiply_exists_input1) = 2 * ge_signed_half_multiply_exists_input1entryvaluedecode + 1 /\ (ge_balance_positive_multiply_exists_input1entryvalue) = 0) /\ (ge_balance_negative_multiply_exists_input1entryvalue) = S ge_signed_half_multiply_exists_input1entryvaluedecode))) /\ ((dst_positive_multiply_exists_input1) + ge_balance_negative_multiply_exists_input1entryvalue = (dst_negative_multiply_exists_input1) + ge_balance_positive_multiply_exists_input1entryvalue))))))))) -> exists H. (((exists dst_positive_code_multiply_exists_resultleft_table dst_positive_scale_multiply_exists_resultleft_table dst_negative_code_multiply_exists_resultleft_table dst_negative_scale_multiply_exists_resultleft_table. (((F) = (((((dst_positive_code_multiply_exists_resultleft_table) + (dst_positive_scale_multiply_exists_resultleft_table)) * S ((dst_positive_code_multiply_exists_resultleft_table) + (dst_positive_scale_multiply_exists_resultleft_table)) + ((dst_positive_scale_multiply_exists_resultleft_table) + (dst_positive_scale_multiply_exists_resultleft_table))) + (((dst_negative_code_multiply_exists_resultleft_table) + (dst_negative_scale_multiply_exists_resultleft_table)) * S ((dst_negative_code_multiply_exists_resultleft_table) + (dst_negative_scale_multiply_exists_resultleft_table)) + ((dst_negative_scale_multiply_exists_resultleft_table) + (dst_negative_scale_multiply_exists_resultleft_table)))) * S ((((dst_positive_code_multiply_exists_resultleft_table) + (dst_positive_scale_multiply_exists_resultleft_table)) * S ((dst_positive_code_multiply_exists_resultleft_table) + (dst_positive_scale_multiply_exists_resultleft_table)) + ((dst_positive_scale_multiply_exists_resultleft_table) + (dst_positive_scale_multiply_exists_resultleft_table))) + (((dst_negative_code_multiply_exists_resultleft_table) + (dst_negative_scale_multiply_exists_resultleft_table)) * S ((dst_negative_code_multiply_exists_resultleft_table) + (dst_negative_scale_multiply_exists_resultleft_table)) + ((dst_negative_scale_multiply_exists_resultleft_table) + (dst_negative_scale_multiply_exists_resultleft_table)))) + ((((dst_negative_code_multiply_exists_resultleft_table) + (dst_negative_scale_multiply_exists_resultleft_table)) * S ((dst_negative_code_multiply_exists_resultleft_table) + (dst_negative_scale_multiply_exists_resultleft_table)) + ((dst_negative_scale_multiply_exists_resultleft_table) + (dst_negative_scale_multiply_exists_resultleft_table))) + (((dst_negative_code_multiply_exists_resultleft_table) + (dst_negative_scale_multiply_exists_resultleft_table)) * S ((dst_negative_code_multiply_exists_resultleft_table) + (dst_negative_scale_multiply_exists_resultleft_table)) + ((dst_negative_scale_multiply_exists_resultleft_table) + (dst_negative_scale_multiply_exists_resultleft_table)))))) /\ (forall dst_index_multiply_exists_resultleft_table. (exists pvs_le_gap_multiply_exists_resultleft_tabledomain. pvs_le_gap_multiply_exists_resultleft_tabledomain + (dst_index_multiply_exists_resultleft_table) = (l)) -> exists dst_positive_multiply_exists_resultleft_table dst_negative_multiply_exists_resultleft_table dst_value_multiply_exists_resultleft_table. ((((exists ff_h_pvs_multiply_exists_resultleft_tableentrypositive. ff_h_pvs_multiply_exists_resultleft_tableentrypositive + S (dst_positive_multiply_exists_resultleft_table) = S ((S (dst_index_multiply_exists_resultleft_table)) * dst_positive_scale_multiply_exists_resultleft_table)) /\ exists ff_q_pvs_multiply_exists_resultleft_tableentrypositive. dst_positive_code_multiply_exists_resultleft_table = ff_q_pvs_multiply_exists_resultleft_tableentrypositive * S ((S (dst_index_multiply_exists_resultleft_table)) * dst_positive_scale_multiply_exists_resultleft_table) + (dst_positive_multiply_exists_resultleft_table))) /\ (((((exists ff_h_pvs_multiply_exists_resultleft_tableentrynegative. ff_h_pvs_multiply_exists_resultleft_tableentrynegative + S (dst_negative_multiply_exists_resultleft_table) = S ((S (dst_index_multiply_exists_resultleft_table)) * dst_negative_scale_multiply_exists_resultleft_table)) /\ exists ff_q_pvs_multiply_exists_resultleft_tableentrynegative. dst_negative_code_multiply_exists_resultleft_table = ff_q_pvs_multiply_exists_resultleft_tableentrynegative * S ((S (dst_index_multiply_exists_resultleft_table)) * dst_negative_scale_multiply_exists_resultleft_table) + (dst_negative_multiply_exists_resultleft_table))) /\ (exists ge_balance_positive_multiply_exists_resultleft_tableentryvalue ge_balance_negative_multiply_exists_resultleft_tableentryvalue. (((((dst_value_multiply_exists_resultleft_table) = 2 * (ge_balance_positive_multiply_exists_resultleft_tableentryvalue) /\ (ge_balance_negative_multiply_exists_resultleft_tableentryvalue) = 0) \/ exists ge_signed_half_multiply_exists_resultleft_tableentryvaluedecode. (((dst_value_multiply_exists_resultleft_table) = 2 * ge_signed_half_multiply_exists_resultleft_tableentryvaluedecode + 1 /\ (ge_balance_positive_multiply_exists_resultleft_tableentryvalue) = 0) /\ (ge_balance_negative_multiply_exists_resultleft_tableentryvalue) = S ge_signed_half_multiply_exists_resultleft_tableentryvaluedecode))) /\ ((dst_positive_multiply_exists_resultleft_table) + ge_balance_negative_multiply_exists_resultleft_tableentryvalue = (dst_negative_multiply_exists_resultleft_table) + ge_balance_positive_multiply_exists_resultleft_tableentryvalue))))))))) /\ (((exists dst_positive_code_multiply_exists_resultright_table dst_positive_scale_multiply_exists_resultright_table dst_negative_code_multiply_exists_resultright_table dst_negative_scale_multiply_exists_resultright_table. (((G) = (((((dst_positive_code_multiply_exists_resultright_table) + (dst_positive_scale_multiply_exists_resultright_table)) * S ((dst_positive_code_multiply_exists_resultright_table) + (dst_positive_scale_multiply_exists_resultright_table)) + ((dst_positive_scale_multiply_exists_resultright_table) + (dst_positive_scale_multiply_exists_resultright_table))) + (((dst_negative_code_multiply_exists_resultright_table) + (dst_negative_scale_multiply_exists_resultright_table)) * S ((dst_negative_code_multiply_exists_resultright_table) + (dst_negative_scale_multiply_exists_resultright_table)) + ((dst_negative_scale_multiply_exists_resultright_table) + (dst_negative_scale_multiply_exists_resultright_table)))) * S ((((dst_positive_code_multiply_exists_resultright_table) + (dst_positive_scale_multiply_exists_resultright_table)) * S ((dst_positive_code_multiply_exists_resultright_table) + (dst_positive_scale_multiply_exists_resultright_table)) + ((dst_positive_scale_multiply_exists_resultright_table) + (dst_positive_scale_multiply_exists_resultright_table))) + (((dst_negative_code_multiply_exists_resultright_table) + (dst_negative_scale_multiply_exists_resultright_table)) * S ((dst_negative_code_multiply_exists_resultright_table) + (dst_negative_scale_multiply_exists_resultright_table)) + ((dst_negative_scale_multiply_exists_resultright_table) + (dst_negative_scale_multiply_exists_resultright_table)))) + ((((dst_negative_code_multiply_exists_resultright_table) + (dst_negative_scale_multiply_exists_resultright_table)) * S ((dst_negative_code_multiply_exists_resultright_table) + (dst_negative_scale_multiply_exists_resultright_table)) + ((dst_negative_scale_multiply_exists_resultright_table) + (dst_negative_scale_multiply_exists_resultright_table))) + (((dst_negative_code_multiply_exists_resultright_table) + (dst_negative_scale_multiply_exists_resultright_table)) * S ((dst_negative_code_multiply_exists_resultright_table) + (dst_negative_scale_multiply_exists_resultright_table)) + ((dst_negative_scale_multiply_exists_resultright_table) + (dst_negative_scale_multiply_exists_resultright_table)))))) /\ (forall dst_index_multiply_exists_resultright_table. (exists pvs_le_gap_multiply_exists_resultright_tabledomain. pvs_le_gap_multiply_exists_resultright_tabledomain + (dst_index_multiply_exists_resultright_table) = (l)) -> exists dst_positive_multiply_exists_resultright_table dst_negative_multiply_exists_resultright_table dst_value_multiply_exists_resultright_table. ((((exists ff_h_pvs_multiply_exists_resultright_tableentrypositive. ff_h_pvs_multiply_exists_resultright_tableentrypositive + S (dst_positive_multiply_exists_resultright_table) = S ((S (dst_index_multiply_exists_resultright_table)) * dst_positive_scale_multiply_exists_resultright_table)) /\ exists ff_q_pvs_multiply_exists_resultright_tableentrypositive. dst_positive_code_multiply_exists_resultright_table = ff_q_pvs_multiply_exists_resultright_tableentrypositive * S ((S (dst_index_multiply_exists_resultright_table)) * dst_positive_scale_multiply_exists_resultright_table) + (dst_positive_multiply_exists_resultright_table))) /\ (((((exists ff_h_pvs_multiply_exists_resultright_tableentrynegative. ff_h_pvs_multiply_exists_resultright_tableentrynegative + S (dst_negative_multiply_exists_resultright_table) = S ((S (dst_index_multiply_exists_resultright_table)) * dst_negative_scale_multiply_exists_resultright_table)) /\ exists ff_q_pvs_multiply_exists_resultright_tableentrynegative. dst_negative_code_multiply_exists_resultright_table = ff_q_pvs_multiply_exists_resultright_tableentrynegative * S ((S (dst_index_multiply_exists_resultright_table)) * dst_negative_scale_multiply_exists_resultright_table) + (dst_negative_multiply_exists_resultright_table))) /\ (exists ge_balance_positive_multiply_exists_resultright_tableentryvalue ge_balance_negative_multiply_exists_resultright_tableentryvalue. (((((dst_value_multiply_exists_resultright_table) = 2 * (ge_balance_positive_multiply_exists_resultright_tableentryvalue) /\ (ge_balance_negative_multiply_exists_resultright_tableentryvalue) = 0) \/ exists ge_signed_half_multiply_exists_resultright_tableentryvaluedecode. (((dst_value_multiply_exists_resultright_table) = 2 * ge_signed_half_multiply_exists_resultright_tableentryvaluedecode + 1 /\ (ge_balance_positive_multiply_exists_resultright_tableentryvalue) = 0) /\ (ge_balance_negative_multiply_exists_resultright_tableentryvalue) = S ge_signed_half_multiply_exists_resultright_tableentryvaluedecode))) /\ ((dst_positive_multiply_exists_resultright_table) + ge_balance_negative_multiply_exists_resultright_tableentryvalue = (dst_negative_multiply_exists_resultright_table) + ge_balance_positive_multiply_exists_resultright_tableentryvalue))))))))) /\ (((exists dst_positive_code_multiply_exists_resultoutput_table dst_positive_scale_multiply_exists_resultoutput_table dst_negative_code_multiply_exists_resultoutput_table dst_negative_scale_multiply_exists_resultoutput_table. (((H) = (((((dst_positive_code_multiply_exists_resultoutput_table) + (dst_positive_scale_multiply_exists_resultoutput_table)) * S ((dst_positive_code_multiply_exists_resultoutput_table) + (dst_positive_scale_multiply_exists_resultoutput_table)) + ((dst_positive_scale_multiply_exists_resultoutput_table) + (dst_positive_scale_multiply_exists_resultoutput_table))) + (((dst_negative_code_multiply_exists_resultoutput_table) + (dst_negative_scale_multiply_exists_resultoutput_table)) * S ((dst_negative_code_multiply_exists_resultoutput_table) + (dst_negative_scale_multiply_exists_resultoutput_table)) + ((dst_negative_scale_multiply_exists_resultoutput_table) + (dst_negative_scale_multiply_exists_resultoutput_table)))) * S ((((dst_positive_code_multiply_exists_resultoutput_table) + (dst_positive_scale_multiply_exists_resultoutput_table)) * S ((dst_positive_code_multiply_exists_resultoutput_table) + (dst_positive_scale_multiply_exists_resultoutput_table)) + ((dst_positive_scale_multiply_exists_resultoutput_table) + (dst_positive_scale_multiply_exists_resultoutput_table))) + (((dst_negative_code_multiply_exists_resultoutput_table) + (dst_negative_scale_multiply_exists_resultoutput_table)) * S ((dst_negative_code_multiply_exists_resultoutput_table) + (dst_negative_scale_multiply_exists_resultoutput_table)) + ((dst_negative_scale_multiply_exists_resultoutput_table) + (dst_negative_scale_multiply_exists_resultoutput_table)))) + ((((dst_negative_code_multiply_exists_resultoutput_table) + (dst_negative_scale_multiply_exists_resultoutput_table)) * S ((dst_negative_code_multiply_exists_resultoutput_table) + (dst_negative_scale_multiply_exists_resultoutput_table)) + ((dst_negative_scale_multiply_exists_resultoutput_table) + (dst_negative_scale_multiply_exists_resultoutput_table))) + (((dst_negative_code_multiply_exists_resultoutput_table) + (dst_negative_scale_multiply_exists_resultoutput_table)) * S ((dst_negative_code_multiply_exists_resultoutput_table) + (dst_negative_scale_multiply_exists_resultoutput_table)) + ((dst_negative_scale_multiply_exists_resultoutput_table) + (dst_negative_scale_multiply_exists_resultoutput_table)))))) /\ (forall dst_index_multiply_exists_resultoutput_table. (exists pvs_le_gap_multiply_exists_resultoutput_tabledomain. pvs_le_gap_multiply_exists_resultoutput_tabledomain + (dst_index_multiply_exists_resultoutput_table) = (l)) -> exists dst_positive_multiply_exists_resultoutput_table dst_negative_multiply_exists_resultoutput_table dst_value_multiply_exists_resultoutput_table. ((((exists ff_h_pvs_multiply_exists_resultoutput_tableentrypositive. ff_h_pvs_multiply_exists_resultoutput_tableentrypositive + S (dst_positive_multiply_exists_resultoutput_table) = S ((S (dst_index_multiply_exists_resultoutput_table)) * dst_positive_scale_multiply_exists_resultoutput_table)) /\ exists ff_q_pvs_multiply_exists_resultoutput_tableentrypositive. dst_positive_code_multiply_exists_resultoutput_table = ff_q_pvs_multiply_exists_resultoutput_tableentrypositive * S ((S (dst_index_multiply_exists_resultoutput_table)) * dst_positive_scale_multiply_exists_resultoutput_table) + (dst_positive_multiply_exists_resultoutput_table))) /\ (((((exists ff_h_pvs_multiply_exists_resultoutput_tableentrynegative. ff_h_pvs_multiply_exists_resultoutput_tableentrynegative + S (dst_negative_multiply_exists_resultoutput_table) = S ((S (dst_index_multiply_exists_resultoutput_table)) * dst_negative_scale_multiply_exists_resultoutput_table)) /\ exists ff_q_pvs_multiply_exists_resultoutput_tableentrynegative. dst_negative_code_multiply_exists_resultoutput_table = ff_q_pvs_multiply_exists_resultoutput_tableentrynegative * S ((S (dst_index_multiply_exists_resultoutput_table)) * dst_negative_scale_multiply_exists_resultoutput_table) + (dst_negative_multiply_exists_resultoutput_table))) /\ (exists ge_balance_positive_multiply_exists_resultoutput_tableentryvalue ge_balance_negative_multiply_exists_resultoutput_tableentryvalue. (((((dst_value_multiply_exists_resultoutput_table) = 2 * (ge_balance_positive_multiply_exists_resultoutput_tableentryvalue) /\ (ge_balance_negative_multiply_exists_resultoutput_tableentryvalue) = 0) \/ exists ge_signed_half_multiply_exists_resultoutput_tableentryvaluedecode. (((dst_value_multiply_exists_resultoutput_table) = 2 * ge_signed_half_multiply_exists_resultoutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_multiply_exists_resultoutput_tableentryvalue) = 0) /\ (ge_balance_negative_multiply_exists_resultoutput_tableentryvalue) = S ge_signed_half_multiply_exists_resultoutput_tableentryvaluedecode))) /\ ((dst_positive_multiply_exists_resultoutput_table) + ge_balance_negative_multiply_exists_resultoutput_tableentryvalue = (dst_negative_multiply_exists_resultoutput_table) + ge_balance_positive_multiply_exists_resultoutput_tableentryvalue))))))))) /\ (forall sto_index_multiply_exists_resultentries. (exists pvs_gap_multiply_exists_resultentriesbound. pvs_gap_multiply_exists_resultentriesbound + S (sto_index_multiply_exists_resultentries) = (l)) -> exists sto_left_multiply_exists_resultentries sto_right_multiply_exists_resultentries sto_output_multiply_exists_resultentries. ((exists dst_positive_code_multiply_exists_resultentriesentryleft dst_positive_scale_multiply_exists_resultentriesentryleft dst_negative_code_multiply_exists_resultentriesentryleft dst_negative_scale_multiply_exists_resultentriesentryleft dst_positive_multiply_exists_resultentriesentryleft dst_negative_multiply_exists_resultentriesentryleft. (((F) = (((((dst_positive_code_multiply_exists_resultentriesentryleft) + (dst_positive_scale_multiply_exists_resultentriesentryleft)) * S ((dst_positive_code_multiply_exists_resultentriesentryleft) + (dst_positive_scale_multiply_exists_resultentriesentryleft)) + ((dst_positive_scale_multiply_exists_resultentriesentryleft) + (dst_positive_scale_multiply_exists_resultentriesentryleft))) + (((dst_negative_code_multiply_exists_resultentriesentryleft) + (dst_negative_scale_multiply_exists_resultentriesentryleft)) * S ((dst_negative_code_multiply_exists_resultentriesentryleft) + (dst_negative_scale_multiply_exists_resultentriesentryleft)) + ((dst_negative_scale_multiply_exists_resultentriesentryleft) + (dst_negative_scale_multiply_exists_resultentriesentryleft)))) * S ((((dst_positive_code_multiply_exists_resultentriesentryleft) + (dst_positive_scale_multiply_exists_resultentriesentryleft)) * S ((dst_positive_code_multiply_exists_resultentriesentryleft) + (dst_positive_scale_multiply_exists_resultentriesentryleft)) + ((dst_positive_scale_multiply_exists_resultentriesentryleft) + (dst_positive_scale_multiply_exists_resultentriesentryleft))) + (((dst_negative_code_multiply_exists_resultentriesentryleft) + (dst_negative_scale_multiply_exists_resultentriesentryleft)) * S ((dst_negative_code_multiply_exists_resultentriesentryleft) + (dst_negative_scale_multiply_exists_resultentriesentryleft)) + ((dst_negative_scale_multiply_exists_resultentriesentryleft) + (dst_negative_scale_multiply_exists_resultentriesentryleft)))) + ((((dst_negative_code_multiply_exists_resultentriesentryleft) + (dst_negative_scale_multiply_exists_resultentriesentryleft)) * S ((dst_negative_code_multiply_exists_resultentriesentryleft) + (dst_negative_scale_multiply_exists_resultentriesentryleft)) + ((dst_negative_scale_multiply_exists_resultentriesentryleft) + (dst_negative_scale_multiply_exists_resultentriesentryleft))) + (((dst_negative_code_multiply_exists_resultentriesentryleft) + (dst_negative_scale_multiply_exists_resultentriesentryleft)) * S ((dst_negative_code_multiply_exists_resultentriesentryleft) + (dst_negative_scale_multiply_exists_resultentriesentryleft)) + ((dst_negative_scale_multiply_exists_resultentriesentryleft) + (dst_negative_scale_multiply_exists_resultentriesentryleft)))))) /\ (((((exists ff_h_pvs_multiply_exists_resultentriesentryleftpositive. ff_h_pvs_multiply_exists_resultentriesentryleftpositive + S (dst_positive_multiply_exists_resultentriesentryleft) = S ((S (sto_index_multiply_exists_resultentries)) * dst_positive_scale_multiply_exists_resultentriesentryleft)) /\ exists ff_q_pvs_multiply_exists_resultentriesentryleftpositive. dst_positive_code_multiply_exists_resultentriesentryleft = ff_q_pvs_multiply_exists_resultentriesentryleftpositive * S ((S (sto_index_multiply_exists_resultentries)) * dst_positive_scale_multiply_exists_resultentriesentryleft) + (dst_positive_multiply_exists_resultentriesentryleft))) /\ (((((exists ff_h_pvs_multiply_exists_resultentriesentryleftnegative. ff_h_pvs_multiply_exists_resultentriesentryleftnegative + S (dst_negative_multiply_exists_resultentriesentryleft) = S ((S (sto_index_multiply_exists_resultentries)) * dst_negative_scale_multiply_exists_resultentriesentryleft)) /\ exists ff_q_pvs_multiply_exists_resultentriesentryleftnegative. dst_negative_code_multiply_exists_resultentriesentryleft = ff_q_pvs_multiply_exists_resultentriesentryleftnegative * S ((S (sto_index_multiply_exists_resultentries)) * dst_negative_scale_multiply_exists_resultentriesentryleft) + (dst_negative_multiply_exists_resultentriesentryleft))) /\ (exists ge_balance_positive_multiply_exists_resultentriesentryleftvalue ge_balance_negative_multiply_exists_resultentriesentryleftvalue. (((((sto_left_multiply_exists_resultentries) = 2 * (ge_balance_positive_multiply_exists_resultentriesentryleftvalue) /\ (ge_balance_negative_multiply_exists_resultentriesentryleftvalue) = 0) \/ exists ge_signed_half_multiply_exists_resultentriesentryleftvaluedecode. (((sto_left_multiply_exists_resultentries) = 2 * ge_signed_half_multiply_exists_resultentriesentryleftvaluedecode + 1 /\ (ge_balance_positive_multiply_exists_resultentriesentryleftvalue) = 0) /\ (ge_balance_negative_multiply_exists_resultentriesentryleftvalue) = S ge_signed_half_multiply_exists_resultentriesentryleftvaluedecode))) /\ ((dst_positive_multiply_exists_resultentriesentryleft) + ge_balance_negative_multiply_exists_resultentriesentryleftvalue = (dst_negative_multiply_exists_resultentriesentryleft) + ge_balance_positive_multiply_exists_resultentriesentryleftvalue))))))))) /\ (((exists dst_positive_code_multiply_exists_resultentriesentryright dst_positive_scale_multiply_exists_resultentriesentryright dst_negative_code_multiply_exists_resultentriesentryright dst_negative_scale_multiply_exists_resultentriesentryright dst_positive_multiply_exists_resultentriesentryright dst_negative_multiply_exists_resultentriesentryright. (((G) = (((((dst_positive_code_multiply_exists_resultentriesentryright) + (dst_positive_scale_multiply_exists_resultentriesentryright)) * S ((dst_positive_code_multiply_exists_resultentriesentryright) + (dst_positive_scale_multiply_exists_resultentriesentryright)) + ((dst_positive_scale_multiply_exists_resultentriesentryright) + (dst_positive_scale_multiply_exists_resultentriesentryright))) + (((dst_negative_code_multiply_exists_resultentriesentryright) + (dst_negative_scale_multiply_exists_resultentriesentryright)) * S ((dst_negative_code_multiply_exists_resultentriesentryright) + (dst_negative_scale_multiply_exists_resultentriesentryright)) + ((dst_negative_scale_multiply_exists_resultentriesentryright) + (dst_negative_scale_multiply_exists_resultentriesentryright)))) * S ((((dst_positive_code_multiply_exists_resultentriesentryright) + (dst_positive_scale_multiply_exists_resultentriesentryright)) * S ((dst_positive_code_multiply_exists_resultentriesentryright) + (dst_positive_scale_multiply_exists_resultentriesentryright)) + ((dst_positive_scale_multiply_exists_resultentriesentryright) + (dst_positive_scale_multiply_exists_resultentriesentryright))) + (((dst_negative_code_multiply_exists_resultentriesentryright) + (dst_negative_scale_multiply_exists_resultentriesentryright)) * S ((dst_negative_code_multiply_exists_resultentriesentryright) + (dst_negative_scale_multiply_exists_resultentriesentryright)) + ((dst_negative_scale_multiply_exists_resultentriesentryright) + (dst_negative_scale_multiply_exists_resultentriesentryright)))) + ((((dst_negative_code_multiply_exists_resultentriesentryright) + (dst_negative_scale_multiply_exists_resultentriesentryright)) * S ((dst_negative_code_multiply_exists_resultentriesentryright) + (dst_negative_scale_multiply_exists_resultentriesentryright)) + ((dst_negative_scale_multiply_exists_resultentriesentryright) + (dst_negative_scale_multiply_exists_resultentriesentryright))) + (((dst_negative_code_multiply_exists_resultentriesentryright) + (dst_negative_scale_multiply_exists_resultentriesentryright)) * S ((dst_negative_code_multiply_exists_resultentriesentryright) + (dst_negative_scale_multiply_exists_resultentriesentryright)) + ((dst_negative_scale_multiply_exists_resultentriesentryright) + (dst_negative_scale_multiply_exists_resultentriesentryright)))))) /\ (((((exists ff_h_pvs_multiply_exists_resultentriesentryrightpositive. ff_h_pvs_multiply_exists_resultentriesentryrightpositive + S (dst_positive_multiply_exists_resultentriesentryright) = S ((S (sto_index_multiply_exists_resultentries)) * dst_positive_scale_multiply_exists_resultentriesentryright)) /\ exists ff_q_pvs_multiply_exists_resultentriesentryrightpositive. dst_positive_code_multiply_exists_resultentriesentryright = ff_q_pvs_multiply_exists_resultentriesentryrightpositive * S ((S (sto_index_multiply_exists_resultentries)) * dst_positive_scale_multiply_exists_resultentriesentryright) + (dst_positive_multiply_exists_resultentriesentryright))) /\ (((((exists ff_h_pvs_multiply_exists_resultentriesentryrightnegative. ff_h_pvs_multiply_exists_resultentriesentryrightnegative + S (dst_negative_multiply_exists_resultentriesentryright) = S ((S (sto_index_multiply_exists_resultentries)) * dst_negative_scale_multiply_exists_resultentriesentryright)) /\ exists ff_q_pvs_multiply_exists_resultentriesentryrightnegative. dst_negative_code_multiply_exists_resultentriesentryright = ff_q_pvs_multiply_exists_resultentriesentryrightnegative * S ((S (sto_index_multiply_exists_resultentries)) * dst_negative_scale_multiply_exists_resultentriesentryright) + (dst_negative_multiply_exists_resultentriesentryright))) /\ (exists ge_balance_positive_multiply_exists_resultentriesentryrightvalue ge_balance_negative_multiply_exists_resultentriesentryrightvalue. (((((sto_right_multiply_exists_resultentries) = 2 * (ge_balance_positive_multiply_exists_resultentriesentryrightvalue) /\ (ge_balance_negative_multiply_exists_resultentriesentryrightvalue) = 0) \/ exists ge_signed_half_multiply_exists_resultentriesentryrightvaluedecode. (((sto_right_multiply_exists_resultentries) = 2 * ge_signed_half_multiply_exists_resultentriesentryrightvaluedecode + 1 /\ (ge_balance_positive_multiply_exists_resultentriesentryrightvalue) = 0) /\ (ge_balance_negative_multiply_exists_resultentriesentryrightvalue) = S ge_signed_half_multiply_exists_resultentriesentryrightvaluedecode))) /\ ((dst_positive_multiply_exists_resultentriesentryright) + ge_balance_negative_multiply_exists_resultentriesentryrightvalue = (dst_negative_multiply_exists_resultentriesentryright) + ge_balance_positive_multiply_exists_resultentriesentryrightvalue))))))))) /\ (((exists dst_positive_code_multiply_exists_resultentriesentryoutput dst_positive_scale_multiply_exists_resultentriesentryoutput dst_negative_code_multiply_exists_resultentriesentryoutput dst_negative_scale_multiply_exists_resultentriesentryoutput dst_positive_multiply_exists_resultentriesentryoutput dst_negative_multiply_exists_resultentriesentryoutput. (((H) = (((((dst_positive_code_multiply_exists_resultentriesentryoutput) + (dst_positive_scale_multiply_exists_resultentriesentryoutput)) * S ((dst_positive_code_multiply_exists_resultentriesentryoutput) + (dst_positive_scale_multiply_exists_resultentriesentryoutput)) + ((dst_positive_scale_multiply_exists_resultentriesentryoutput) + (dst_positive_scale_multiply_exists_resultentriesentryoutput))) + (((dst_negative_code_multiply_exists_resultentriesentryoutput) + (dst_negative_scale_multiply_exists_resultentriesentryoutput)) * S ((dst_negative_code_multiply_exists_resultentriesentryoutput) + (dst_negative_scale_multiply_exists_resultentriesentryoutput)) + ((dst_negative_scale_multiply_exists_resultentriesentryoutput) + (dst_negative_scale_multiply_exists_resultentriesentryoutput)))) * S ((((dst_positive_code_multiply_exists_resultentriesentryoutput) + (dst_positive_scale_multiply_exists_resultentriesentryoutput)) * S ((dst_positive_code_multiply_exists_resultentriesentryoutput) + (dst_positive_scale_multiply_exists_resultentriesentryoutput)) + ((dst_positive_scale_multiply_exists_resultentriesentryoutput) + (dst_positive_scale_multiply_exists_resultentriesentryoutput))) + (((dst_negative_code_multiply_exists_resultentriesentryoutput) + (dst_negative_scale_multiply_exists_resultentriesentryoutput)) * S ((dst_negative_code_multiply_exists_resultentriesentryoutput) + (dst_negative_scale_multiply_exists_resultentriesentryoutput)) + ((dst_negative_scale_multiply_exists_resultentriesentryoutput) + (dst_negative_scale_multiply_exists_resultentriesentryoutput)))) + ((((dst_negative_code_multiply_exists_resultentriesentryoutput) + (dst_negative_scale_multiply_exists_resultentriesentryoutput)) * S ((dst_negative_code_multiply_exists_resultentriesentryoutput) + (dst_negative_scale_multiply_exists_resultentriesentryoutput)) + ((dst_negative_scale_multiply_exists_resultentriesentryoutput) + (dst_negative_scale_multiply_exists_resultentriesentryoutput))) + (((dst_negative_code_multiply_exists_resultentriesentryoutput) + (dst_negative_scale_multiply_exists_resultentriesentryoutput)) * S ((dst_negative_code_multiply_exists_resultentriesentryoutput) + (dst_negative_scale_multiply_exists_resultentriesentryoutput)) + ((dst_negative_scale_multiply_exists_resultentriesentryoutput) + (dst_negative_scale_multiply_exists_resultentriesentryoutput)))))) /\ (((((exists ff_h_pvs_multiply_exists_resultentriesentryoutputpositive. ff_h_pvs_multiply_exists_resultentriesentryoutputpositive + S (dst_positive_multiply_exists_resultentriesentryoutput) = S ((S (sto_index_multiply_exists_resultentries)) * dst_positive_scale_multiply_exists_resultentriesentryoutput)) /\ exists ff_q_pvs_multiply_exists_resultentriesentryoutputpositive. dst_positive_code_multiply_exists_resultentriesentryoutput = ff_q_pvs_multiply_exists_resultentriesentryoutputpositive * S ((S (sto_index_multiply_exists_resultentries)) * dst_positive_scale_multiply_exists_resultentriesentryoutput) + (dst_positive_multiply_exists_resultentriesentryoutput))) /\ (((((exists ff_h_pvs_multiply_exists_resultentriesentryoutputnegative. ff_h_pvs_multiply_exists_resultentriesentryoutputnegative + S (dst_negative_multiply_exists_resultentriesentryoutput) = S ((S (sto_index_multiply_exists_resultentries)) * dst_negative_scale_multiply_exists_resultentriesentryoutput)) /\ exists ff_q_pvs_multiply_exists_resultentriesentryoutputnegative. dst_negative_code_multiply_exists_resultentriesentryoutput = ff_q_pvs_multiply_exists_resultentriesentryoutputnegative * S ((S (sto_index_multiply_exists_resultentries)) * dst_negative_scale_multiply_exists_resultentriesentryoutput) + (dst_negative_multiply_exists_resultentriesentryoutput))) /\ (exists ge_balance_positive_multiply_exists_resultentriesentryoutputvalue ge_balance_negative_multiply_exists_resultentriesentryoutputvalue. (((((sto_output_multiply_exists_resultentries) = 2 * (ge_balance_positive_multiply_exists_resultentriesentryoutputvalue) /\ (ge_balance_negative_multiply_exists_resultentriesentryoutputvalue) = 0) \/ exists ge_signed_half_multiply_exists_resultentriesentryoutputvaluedecode. (((sto_output_multiply_exists_resultentries) = 2 * ge_signed_half_multiply_exists_resultentriesentryoutputvaluedecode + 1 /\ (ge_balance_positive_multiply_exists_resultentriesentryoutputvalue) = 0) /\ (ge_balance_negative_multiply_exists_resultentriesentryoutputvalue) = S ge_signed_half_multiply_exists_resultentriesentryoutputvaluedecode))) /\ ((dst_positive_multiply_exists_resultentriesentryoutput) + ge_balance_negative_multiply_exists_resultentriesentryoutputvalue = (dst_negative_multiply_exists_resultentriesentryoutput) + ge_balance_positive_multiply_exists_resultentriesentryoutputvalue))))))))) /\ (exists sto_ap_multiply_exists_resultentriesentryoperation sto_an_multiply_exists_resultentriesentryoperation sto_bp_multiply_exists_resultentriesentryoperation sto_bn_multiply_exists_resultentriesentryoperation sto_cp_multiply_exists_resultentriesentryoperation sto_cn_multiply_exists_resultentriesentryoperation. (((((sto_left_multiply_exists_resultentries) = 2 * (sto_ap_multiply_exists_resultentriesentryoperation) /\ (sto_an_multiply_exists_resultentriesentryoperation) = 0) \/ exists ge_signed_half_multiply_exists_resultentriesentryoperationleft. (((sto_left_multiply_exists_resultentries) = 2 * ge_signed_half_multiply_exists_resultentriesentryoperationleft + 1 /\ (sto_ap_multiply_exists_resultentriesentryoperation) = 0) /\ (sto_an_multiply_exists_resultentriesentryoperation) = S ge_signed_half_multiply_exists_resultentriesentryoperationleft))) /\ ((((((sto_right_multiply_exists_resultentries) = 2 * (sto_bp_multiply_exists_resultentriesentryoperation) /\ (sto_bn_multiply_exists_resultentriesentryoperation) = 0) \/ exists ge_signed_half_multiply_exists_resultentriesentryoperationright. (((sto_right_multiply_exists_resultentries) = 2 * ge_signed_half_multiply_exists_resultentriesentryoperationright + 1 /\ (sto_bp_multiply_exists_resultentriesentryoperation) = 0) /\ (sto_bn_multiply_exists_resultentriesentryoperation) = S ge_signed_half_multiply_exists_resultentriesentryoperationright))) /\ ((((((sto_output_multiply_exists_resultentries) = 2 * (sto_cp_multiply_exists_resultentriesentryoperation) /\ (sto_cn_multiply_exists_resultentriesentryoperation) = 0) \/ exists ge_signed_half_multiply_exists_resultentriesentryoperationoutput. (((sto_output_multiply_exists_resultentries) = 2 * ge_signed_half_multiply_exists_resultentriesentryoperationoutput + 1 /\ (sto_cp_multiply_exists_resultentriesentryoperation) = 0) /\ (sto_cn_multiply_exists_resultentriesentryoperation) = S ge_signed_half_multiply_exists_resultentriesentryoperationoutput))) /\ ((sto_ap_multiply_exists_resultentriesentryoperation * sto_bp_multiply_exists_resultentriesentryoperation + sto_an_multiply_exists_resultentriesentryoperation * sto_bn_multiply_exists_resultentriesentryoperation) + sto_cn_multiply_exists_resultentriesentryoperation = (sto_ap_multiply_exists_resultentriesentryoperation * sto_bn_multiply_exists_resultentriesentryoperation + sto_an_multiply_exists_resultentriesentryoperation * sto_bp_multiply_exists_resultentriesentryoperation) + sto_cp_multiply_exists_resultentriesentryoperation)))))))))))))))))))

Constructive proof overview

Generated structural guide

Ordinary finite induction constructs both beta output streams and their actual packed table for pointwise multiply; no finite-choice or supplied-table oracle is used.

The unchanged tactic script uses 7 declared prerequisites and contains 88 exact native proof lines.

Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not Stable

Proof neighborhood

Direct dependencies

WS0009 signed_table_multiply_empty divisor_signed_table_from_components Alpha theorem; checked-use authorized WS0001 signed_table_domain_resize WS0002 signed_table_lookup_any signed_mul_total Alpha theorem; checked-use authorized arithmetic_signed_table_extend_at Alpha theorem; checked-use authorized WS0012 signed_table_multiply_extend

Direct dependents

WS0014 signed_table_multiply_exists_extensionally_unique WS001F signed_weighted_sum_exists

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

88 script commands · 22 reading checkpoints · 5 local claims

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 (4)
signed table multiply emptysigned table domain resizesigned table lookup anysigned table multiply extend

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

01Induction on lL1–5

Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.

  1. L1
    induction l
  2. L2
    intro F
  3. L3
    intro G
  4. L4
    intro ht0
  5. L5
    intro ht1
02Construct an explicit witnessL6–6

Supply the displayed value, then prove that it has the required property.

  1. L6
    exists ((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) + ((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0))))
03Use earlier factsL7–16

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L7
    specialize signed_table_multiply_empty (F)
  2. L8
    specialize signed_table_multiply_empty (G)
  3. L9
    specialize signed_table_multiply_empty (((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) + ((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))))
  4. L10
    apply signed_table_multiply_empty
  5. L11
    exact ht0
  6. L12
    exact ht1
  7. L13
    specialize divisor_signed_table_from_components (0)
  8. L14
    specialize divisor_signed_table_from_components (((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) + ((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))))
  9. L15
    specialize divisor_signed_table_from_components (0)
  10. L16
    specialize divisor_signed_table_from_components (0)
04Use earlier factsL17–19

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L17
    specialize divisor_signed_table_from_components (0)
  2. L18
    specialize divisor_signed_table_from_components (0)
  3. L19
    apply divisor_signed_table_from_components
05Calculate and transport equalitiesL20–20

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L20
    refl
06Fix variables and assumptionsL21–24

Work with arbitrary variables or the premises of the current implication.

  1. L21
    intro F
  2. L22
    intro G
  3. L23
    intro ht0
  4. L24
    intro ht1
07Establish hpL25–34

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply IH.

  1. L25
    have hp : ∃ K. ArithMul(F,G,K,l)Definitions: ArithMul
  2. L26
    specialize IH (F)
  3. L27
    specialize IH (G)
  4. L28
    apply IH
  5. L29
    specialize signed_table_domain_resize (S l)
  6. L30
    specialize signed_table_domain_resize (l)
  7. L31
    specialize signed_table_domain_resize (F)
  8. L32
    apply signed_table_domain_resize
  9. L33
    exact ht0
  10. L34
    specialize signed_table_domain_resize (S l)
08Use earlier factsL35–38

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L35
    specialize signed_table_domain_resize (l)
  2. L36
    specialize signed_table_domain_resize (G)
  3. L37
    apply signed_table_domain_resize
  4. L38
    exact ht1
09Separate the logical casesL39–39

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L39
    cases hp
10Establish he0L40–45

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply signed table lookup any.

  1. L40
    have he0 : ∃ z. ArithAt(F,l,z)Definitions: ArithAt
  2. L41
    specialize signed_table_lookup_any (S l)
  3. L42
    specialize signed_table_lookup_any (F)
  4. L43
    specialize signed_table_lookup_any (l)
  5. L44
    apply signed_table_lookup_any
  6. L45
    exact ht0
11Separate the logical casesL46–46

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L46
    cases he0
12Establish he1L47–52

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply signed table lookup any.

  1. L47
    have he1 : ∃ z. ArithAt(G,l,z)Definitions: ArithAt
  2. L48
    specialize signed_table_lookup_any (S l)
  3. L49
    specialize signed_table_lookup_any (G)
  4. L50
    specialize signed_table_lookup_any (l)
  5. L51
    apply signed_table_lookup_any
  6. L52
    exact ht1
13Separate the logical casesL53–53

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L53
    cases he1
14Establish hvL54–57

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply signed mul total.

  1. L54
    have hv : ∃ z. SignedMul(x1,x2,z)Definitions: SignedMul
  2. L55
    specialize signed_mul_total (x1)
  3. L56
    specialize signed_mul_total (x2)
  4. L57
    apply signed_mul_total
15Separate the logical casesL58–58

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L58
    cases hv
16Establish hnextL59–64

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply arithmetic signed table extend at.

  1. L59
    have hnext : ∃ K. ArithExtend(x,K,l,x3)Definitions: ArithExtend
  2. L60
    specialize arithmetic_signed_table_extend_at (l)
  3. L61
    specialize arithmetic_signed_table_extend_at (x)
  4. L62
    specialize arithmetic_signed_table_extend_at (l)
  5. L63
    specialize arithmetic_signed_table_extend_at (x3)
  6. L64
    apply arithmetic_signed_table_extend_at
17Separate the logical casesL65–67

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L65
    cases hp_witness
  2. L66
    cases hp_witness_right
  3. L67
    cases hp_witness_right_right
18Use earlier factsL68–68

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L68
    exact hp_witness_right_right_left
19Separate the logical casesL69–71

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L69
    cases hnext
  2. L70
    cases hnext_witness
  3. L71
    cases hnext_witness_right
20Construct an explicit witnessL72–72

Supply the displayed value, then prove that it has the required property.

  1. L72
    exists x4
21Use earlier factsL73–82

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L73
    specialize signed_table_multiply_extend (F)
  2. L74
    specialize signed_table_multiply_extend (G)
  3. L75
    specialize signed_table_multiply_extend (x)
  4. L76
    specialize signed_table_multiply_extend (x4)
  5. L77
    specialize signed_table_multiply_extend (l)
  6. L78
    specialize signed_table_multiply_extend (x1)
  7. L79
    specialize signed_table_multiply_extend (x2)
  8. L80
    specialize signed_table_multiply_extend (x3)
  9. L81
    apply signed_table_multiply_extend
  10. L82
    exact hp_witness
22Use earlier factsL83–88

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L83
    exact hnext_witness_left
  2. L84
    exact hnext_witness_right_left
  3. L85
    exact he0_witness
  4. L86
    exact he1_witness
  5. L87
    exact hnext_witness_right_right
  6. L88
    exact hv_witness

Library-wide reading audit

Original exact command ledger · 88 lines
  1. 0001induction l
  2. 0002intro F
  3. 0003intro G
  4. 0004intro ht0
  5. 0005intro ht1
  6. 0006exists ((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) + ((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0))))
  7. 0007specialize signed_table_multiply_empty (F)
  8. 0008specialize signed_table_multiply_empty (G)
  9. 0009specialize signed_table_multiply_empty (((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) + ((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))))
  10. 0010apply signed_table_multiply_empty
  11. 0011exact ht0
  12. 0012exact ht1
  13. 0013specialize divisor_signed_table_from_components (0)
  14. 0014specialize divisor_signed_table_from_components (((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) + ((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))))
  15. 0015specialize divisor_signed_table_from_components (0)
  16. 0016specialize divisor_signed_table_from_components (0)
  17. 0017specialize divisor_signed_table_from_components (0)
  18. 0018specialize divisor_signed_table_from_components (0)
  19. 0019apply divisor_signed_table_from_components
  20. 0020refl
  21. 0021intro F
  22. 0022intro G
  23. 0023intro ht0
  24. 0024intro ht1
  25. 0025have hp : exists K. (((exists dst_positive_code_multiply_construct_prefixleft_table dst_positive_scale_multiply_construct_prefixleft_table dst_negative_code_multiply_construct_prefixleft_table dst_negative_scale_multiply_construct_prefixleft_table. (((F) = (((((dst_positive_code_multiply_construct_prefixleft_table) + (dst_positive_scale_multiply_construct_prefixleft_table)) * S ((dst_positive_code_multiply_construct_prefixleft_table) + (dst_positive_scale_multiply_construct_prefixleft_table)) + ((dst_positive_scale_multiply_construct_prefixleft_table) + (dst_positive_scale_multiply_construct_prefixleft_table))) + (((dst_negative_code_multiply_construct_prefixleft_table) + (dst_negative_scale_multiply_construct_prefixleft_table)) * S ((dst_negative_code_multiply_construct_prefixleft_table) + (dst_negative_scale_multiply_construct_prefixleft_table)) + ((dst_negative_scale_multiply_construct_prefixleft_table) + (dst_negative_scale_multiply_construct_prefixleft_table)))) * S ((((dst_positive_code_multiply_construct_prefixleft_table) + (dst_positive_scale_multiply_construct_prefixleft_table)) * S ((dst_positive_code_multiply_construct_prefixleft_table) + (dst_positive_scale_multiply_construct_prefixleft_table)) + ((dst_positive_scale_multiply_construct_prefixleft_table) + (dst_positive_scale_multiply_construct_prefixleft_table))) + (((dst_negative_code_multiply_construct_prefixleft_table) + (dst_negative_scale_multiply_construct_prefixleft_table)) * S ((dst_negative_code_multiply_construct_prefixleft_table) + (dst_negative_scale_multiply_construct_prefixleft_table)) + ((dst_negative_scale_multiply_construct_prefixleft_table) + (dst_negative_scale_multiply_construct_prefixleft_table)))) + ((((dst_negative_code_multiply_construct_prefixleft_table) + (dst_negative_scale_multiply_construct_prefixleft_table)) * S ((dst_negative_code_multiply_construct_prefixleft_table) + (dst_negative_scale_multiply_construct_prefixleft_table)) + ((dst_negative_scale_multiply_construct_prefixleft_table) + (dst_negative_scale_multiply_construct_prefixleft_table))) + (((dst_negative_code_multiply_construct_prefixleft_table) + (dst_negative_scale_multiply_construct_prefixleft_table)) * S ((dst_negative_code_multiply_construct_prefixleft_table) + (dst_negative_scale_multiply_construct_prefixleft_table)) + ((dst_negative_scale_multiply_construct_prefixleft_table) + (dst_negative_scale_multiply_construct_prefixleft_table)))))) /\ (forall dst_index_multiply_construct_prefixleft_table. (exists pvs_le_gap_multiply_construct_prefixleft_tabledomain. pvs_le_gap_multiply_construct_prefixleft_tabledomain + (dst_index_multiply_construct_prefixleft_table) = (l)) -> exists dst_positive_multiply_construct_prefixleft_table dst_negative_multiply_construct_prefixleft_table dst_value_multiply_construct_prefixleft_table. ((((exists ff_h_pvs_multiply_construct_prefixleft_tableentrypositive. ff_h_pvs_multiply_construct_prefixleft_tableentrypositive + S (dst_positive_multiply_construct_prefixleft_table) = S ((S (dst_index_multiply_construct_prefixleft_table)) * dst_positive_scale_multiply_construct_prefixleft_table)) /\ exists ff_q_pvs_multiply_construct_prefixleft_tableentrypositive. dst_positive_code_multiply_construct_prefixleft_table = ff_q_pvs_multiply_construct_prefixleft_tableentrypositive * S ((S (dst_index_multiply_construct_prefixleft_table)) * dst_positive_scale_multiply_construct_prefixleft_table) + (dst_positive_multiply_construct_prefixleft_table))) /\ (((((exists ff_h_pvs_multiply_construct_prefixleft_tableentrynegative. ff_h_pvs_multiply_construct_prefixleft_tableentrynegative + S (dst_negative_multiply_construct_prefixleft_table) = S ((S (dst_index_multiply_construct_prefixleft_table)) * dst_negative_scale_multiply_construct_prefixleft_table)) /\ exists ff_q_pvs_multiply_construct_prefixleft_tableentrynegative. dst_negative_code_multiply_construct_prefixleft_table = ff_q_pvs_multiply_construct_prefixleft_tableentrynegative * S ((S (dst_index_multiply_construct_prefixleft_table)) * dst_negative_scale_multiply_construct_prefixleft_table) + (dst_negative_multiply_construct_prefixleft_table))) /\ (exists ge_balance_positive_multiply_construct_prefixleft_tableentryvalue ge_balance_negative_multiply_construct_prefixleft_tableentryvalue. (((((dst_value_multiply_construct_prefixleft_table) = 2 * (ge_balance_positive_multiply_construct_prefixleft_tableentryvalue) /\ (ge_balance_negative_multiply_construct_prefixleft_tableentryvalue) = 0) \/ exists ge_signed_half_multiply_construct_prefixleft_tableentryvaluedecode. (((dst_value_multiply_construct_prefixleft_table) = 2 * ge_signed_half_multiply_construct_prefixleft_tableentryvaluedecode + 1 /\ (ge_balance_positive_multiply_construct_prefixleft_tableentryvalue) = 0) /\ (ge_balance_negative_multiply_construct_prefixleft_tableentryvalue) = S ge_signed_half_multiply_construct_prefixleft_tableentryvaluedecode))) /\ ((dst_positive_multiply_construct_prefixleft_table) + ge_balance_negative_multiply_construct_prefixleft_tableentryvalue = (dst_negative_multiply_construct_prefixleft_table) + ge_balance_positive_multiply_construct_prefixleft_tableentryvalue))))))))) /\ (((exists dst_positive_code_multiply_construct_prefixright_table dst_positive_scale_multiply_construct_prefixright_table dst_negative_code_multiply_construct_prefixright_table dst_negative_scale_multiply_construct_prefixright_table. (((G) = (((((dst_positive_code_multiply_construct_prefixright_table) + (dst_positive_scale_multiply_construct_prefixright_table)) * S ((dst_positive_code_multiply_construct_prefixright_table) + (dst_positive_scale_multiply_construct_prefixright_table)) + ((dst_positive_scale_multiply_construct_prefixright_table) + (dst_positive_scale_multiply_construct_prefixright_table))) + (((dst_negative_code_multiply_construct_prefixright_table) + (dst_negative_scale_multiply_construct_prefixright_table)) * S ((dst_negative_code_multiply_construct_prefixright_table) + (dst_negative_scale_multiply_construct_prefixright_table)) + ((dst_negative_scale_multiply_construct_prefixright_table) + (dst_negative_scale_multiply_construct_prefixright_table)))) * S ((((dst_positive_code_multiply_construct_prefixright_table) + (dst_positive_scale_multiply_construct_prefixright_table)) * S ((dst_positive_code_multiply_construct_prefixright_table) + (dst_positive_scale_multiply_construct_prefixright_table)) + ((dst_positive_scale_multiply_construct_prefixright_table) + (dst_positive_scale_multiply_construct_prefixright_table))) + (((dst_negative_code_multiply_construct_prefixright_table) + (dst_negative_scale_multiply_construct_prefixright_table)) * S ((dst_negative_code_multiply_construct_prefixright_table) + (dst_negative_scale_multiply_construct_prefixright_table)) + ((dst_negative_scale_multiply_construct_prefixright_table) + (dst_negative_scale_multiply_construct_prefixright_table)))) + ((((dst_negative_code_multiply_construct_prefixright_table) + (dst_negative_scale_multiply_construct_prefixright_table)) * S ((dst_negative_code_multiply_construct_prefixright_table) + (dst_negative_scale_multiply_construct_prefixright_table)) + ((dst_negative_scale_multiply_construct_prefixright_table) + (dst_negative_scale_multiply_construct_prefixright_table))) + (((dst_negative_code_multiply_construct_prefixright_table) + (dst_negative_scale_multiply_construct_prefixright_table)) * S ((dst_negative_code_multiply_construct_prefixright_table) + (dst_negative_scale_multiply_construct_prefixright_table)) + ((dst_negative_scale_multiply_construct_prefixright_table) + (dst_negative_scale_multiply_construct_prefixright_table)))))) /\ (forall dst_index_multiply_construct_prefixright_table. (exists pvs_le_gap_multiply_construct_prefixright_tabledomain. pvs_le_gap_multiply_construct_prefixright_tabledomain + (dst_index_multiply_construct_prefixright_table) = (l)) -> exists dst_positive_multiply_construct_prefixright_table dst_negative_multiply_construct_prefixright_table dst_value_multiply_construct_prefixright_table. ((((exists ff_h_pvs_multiply_construct_prefixright_tableentrypositive. ff_h_pvs_multiply_construct_prefixright_tableentrypositive + S (dst_positive_multiply_construct_prefixright_table) = S ((S (dst_index_multiply_construct_prefixright_table)) * dst_positive_scale_multiply_construct_prefixright_table)) /\ exists ff_q_pvs_multiply_construct_prefixright_tableentrypositive. dst_positive_code_multiply_construct_prefixright_table = ff_q_pvs_multiply_construct_prefixright_tableentrypositive * S ((S (dst_index_multiply_construct_prefixright_table)) * dst_positive_scale_multiply_construct_prefixright_table) + (dst_positive_multiply_construct_prefixright_table))) /\ (((((exists ff_h_pvs_multiply_construct_prefixright_tableentrynegative. ff_h_pvs_multiply_construct_prefixright_tableentrynegative + S (dst_negative_multiply_construct_prefixright_table) = S ((S (dst_index_multiply_construct_prefixright_table)) * dst_negative_scale_multiply_construct_prefixright_table)) /\ exists ff_q_pvs_multiply_construct_prefixright_tableentrynegative. dst_negative_code_multiply_construct_prefixright_table = ff_q_pvs_multiply_construct_prefixright_tableentrynegative * S ((S (dst_index_multiply_construct_prefixright_table)) * dst_negative_scale_multiply_construct_prefixright_table) + (dst_negative_multiply_construct_prefixright_table))) /\ (exists ge_balance_positive_multiply_construct_prefixright_tableentryvalue ge_balance_negative_multiply_construct_prefixright_tableentryvalue. (((((dst_value_multiply_construct_prefixright_table) = 2 * (ge_balance_positive_multiply_construct_prefixright_tableentryvalue) /\ (ge_balance_negative_multiply_construct_prefixright_tableentryvalue) = 0) \/ exists ge_signed_half_multiply_construct_prefixright_tableentryvaluedecode. (((dst_value_multiply_construct_prefixright_table) = 2 * ge_signed_half_multiply_construct_prefixright_tableentryvaluedecode + 1 /\ (ge_balance_positive_multiply_construct_prefixright_tableentryvalue) = 0) /\ (ge_balance_negative_multiply_construct_prefixright_tableentryvalue) = S ge_signed_half_multiply_construct_prefixright_tableentryvaluedecode))) /\ ((dst_positive_multiply_construct_prefixright_table) + ge_balance_negative_multiply_construct_prefixright_tableentryvalue = (dst_negative_multiply_construct_prefixright_table) + ge_balance_positive_multiply_construct_prefixright_tableentryvalue))))))))) /\ (((exists dst_positive_code_multiply_construct_prefixoutput_table dst_positive_scale_multiply_construct_prefixoutput_table dst_negative_code_multiply_construct_prefixoutput_table dst_negative_scale_multiply_construct_prefixoutput_table. (((K) = (((((dst_positive_code_multiply_construct_prefixoutput_table) + (dst_positive_scale_multiply_construct_prefixoutput_table)) * S ((dst_positive_code_multiply_construct_prefixoutput_table) + (dst_positive_scale_multiply_construct_prefixoutput_table)) + ((dst_positive_scale_multiply_construct_prefixoutput_table) + (dst_positive_scale_multiply_construct_prefixoutput_table))) + (((dst_negative_code_multiply_construct_prefixoutput_table) + (dst_negative_scale_multiply_construct_prefixoutput_table)) * S ((dst_negative_code_multiply_construct_prefixoutput_table) + (dst_negative_scale_multiply_construct_prefixoutput_table)) + ((dst_negative_scale_multiply_construct_prefixoutput_table) + (dst_negative_scale_multiply_construct_prefixoutput_table)))) * S ((((dst_positive_code_multiply_construct_prefixoutput_table) + (dst_positive_scale_multiply_construct_prefixoutput_table)) * S ((dst_positive_code_multiply_construct_prefixoutput_table) + (dst_positive_scale_multiply_construct_prefixoutput_table)) + ((dst_positive_scale_multiply_construct_prefixoutput_table) + (dst_positive_scale_multiply_construct_prefixoutput_table))) + (((dst_negative_code_multiply_construct_prefixoutput_table) + (dst_negative_scale_multiply_construct_prefixoutput_table)) * S ((dst_negative_code_multiply_construct_prefixoutput_table) + (dst_negative_scale_multiply_construct_prefixoutput_table)) + ((dst_negative_scale_multiply_construct_prefixoutput_table) + (dst_negative_scale_multiply_construct_prefixoutput_table)))) + ((((dst_negative_code_multiply_construct_prefixoutput_table) + (dst_negative_scale_multiply_construct_prefixoutput_table)) * S ((dst_negative_code_multiply_construct_prefixoutput_table) + (dst_negative_scale_multiply_construct_prefixoutput_table)) + ((dst_negative_scale_multiply_construct_prefixoutput_table) + (dst_negative_scale_multiply_construct_prefixoutput_table))) + (((dst_negative_code_multiply_construct_prefixoutput_table) + (dst_negative_scale_multiply_construct_prefixoutput_table)) * S ((dst_negative_code_multiply_construct_prefixoutput_table) + (dst_negative_scale_multiply_construct_prefixoutput_table)) + ((dst_negative_scale_multiply_construct_prefixoutput_table) + (dst_negative_scale_multiply_construct_prefixoutput_table)))))) /\ (forall dst_index_multiply_construct_prefixoutput_table. (exists pvs_le_gap_multiply_construct_prefixoutput_tabledomain. pvs_le_gap_multiply_construct_prefixoutput_tabledomain + (dst_index_multiply_construct_prefixoutput_table) = (l)) -> exists dst_positive_multiply_construct_prefixoutput_table dst_negative_multiply_construct_prefixoutput_table dst_value_multiply_construct_prefixoutput_table. ((((exists ff_h_pvs_multiply_construct_prefixoutput_tableentrypositive. ff_h_pvs_multiply_construct_prefixoutput_tableentrypositive + S (dst_positive_multiply_construct_prefixoutput_table) = S ((S (dst_index_multiply_construct_prefixoutput_table)) * dst_positive_scale_multiply_construct_prefixoutput_table)) /\ exists ff_q_pvs_multiply_construct_prefixoutput_tableentrypositive. dst_positive_code_multiply_construct_prefixoutput_table = ff_q_pvs_multiply_construct_prefixoutput_tableentrypositive * S ((S (dst_index_multiply_construct_prefixoutput_table)) * dst_positive_scale_multiply_construct_prefixoutput_table) + (dst_positive_multiply_construct_prefixoutput_table))) /\ (((((exists ff_h_pvs_multiply_construct_prefixoutput_tableentrynegative. ff_h_pvs_multiply_construct_prefixoutput_tableentrynegative + S (dst_negative_multiply_construct_prefixoutput_table) = S ((S (dst_index_multiply_construct_prefixoutput_table)) * dst_negative_scale_multiply_construct_prefixoutput_table)) /\ exists ff_q_pvs_multiply_construct_prefixoutput_tableentrynegative. dst_negative_code_multiply_construct_prefixoutput_table = ff_q_pvs_multiply_construct_prefixoutput_tableentrynegative * S ((S (dst_index_multiply_construct_prefixoutput_table)) * dst_negative_scale_multiply_construct_prefixoutput_table) + (dst_negative_multiply_construct_prefixoutput_table))) /\ (exists ge_balance_positive_multiply_construct_prefixoutput_tableentryvalue ge_balance_negative_multiply_construct_prefixoutput_tableentryvalue. (((((dst_value_multiply_construct_prefixoutput_table) = 2 * (ge_balance_positive_multiply_construct_prefixoutput_tableentryvalue) /\ (ge_balance_negative_multiply_construct_prefixoutput_tableentryvalue) = 0) \/ exists ge_signed_half_multiply_construct_prefixoutput_tableentryvaluedecode. (((dst_value_multiply_construct_prefixoutput_table) = 2 * ge_signed_half_multiply_construct_prefixoutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_multiply_construct_prefixoutput_tableentryvalue) = 0) /\ (ge_balance_negative_multiply_construct_prefixoutput_tableentryvalue) = S ge_signed_half_multiply_construct_prefixoutput_tableentryvaluedecode))) /\ ((dst_positive_multiply_construct_prefixoutput_table) + ge_balance_negative_multiply_construct_prefixoutput_tableentryvalue = (dst_negative_multiply_construct_prefixoutput_table) + ge_balance_positive_multiply_construct_prefixoutput_tableentryvalue))))))))) /\ (forall sto_index_multiply_construct_prefixentries. (exists pvs_gap_multiply_construct_prefixentriesbound. pvs_gap_multiply_construct_prefixentriesbound + S (sto_index_multiply_construct_prefixentries) = (l)) -> exists sto_left_multiply_construct_prefixentries sto_right_multiply_construct_prefixentries sto_output_multiply_construct_prefixentries. ((exists dst_positive_code_multiply_construct_prefixentriesentryleft dst_positive_scale_multiply_construct_prefixentriesentryleft dst_negative_code_multiply_construct_prefixentriesentryleft dst_negative_scale_multiply_construct_prefixentriesentryleft dst_positive_multiply_construct_prefixentriesentryleft dst_negative_multiply_construct_prefixentriesentryleft. (((F) = (((((dst_positive_code_multiply_construct_prefixentriesentryleft) + (dst_positive_scale_multiply_construct_prefixentriesentryleft)) * S ((dst_positive_code_multiply_construct_prefixentriesentryleft) + (dst_positive_scale_multiply_construct_prefixentriesentryleft)) + ((dst_positive_scale_multiply_construct_prefixentriesentryleft) + (dst_positive_scale_multiply_construct_prefixentriesentryleft))) + (((dst_negative_code_multiply_construct_prefixentriesentryleft) + (dst_negative_scale_multiply_construct_prefixentriesentryleft)) * S ((dst_negative_code_multiply_construct_prefixentriesentryleft) + (dst_negative_scale_multiply_construct_prefixentriesentryleft)) + ((dst_negative_scale_multiply_construct_prefixentriesentryleft) + (dst_negative_scale_multiply_construct_prefixentriesentryleft)))) * S ((((dst_positive_code_multiply_construct_prefixentriesentryleft) + (dst_positive_scale_multiply_construct_prefixentriesentryleft)) * S ((dst_positive_code_multiply_construct_prefixentriesentryleft) + (dst_positive_scale_multiply_construct_prefixentriesentryleft)) + ((dst_positive_scale_multiply_construct_prefixentriesentryleft) + (dst_positive_scale_multiply_construct_prefixentriesentryleft))) + (((dst_negative_code_multiply_construct_prefixentriesentryleft) + (dst_negative_scale_multiply_construct_prefixentriesentryleft)) * S ((dst_negative_code_multiply_construct_prefixentriesentryleft) + (dst_negative_scale_multiply_construct_prefixentriesentryleft)) + ((dst_negative_scale_multiply_construct_prefixentriesentryleft) + (dst_negative_scale_multiply_construct_prefixentriesentryleft)))) + ((((dst_negative_code_multiply_construct_prefixentriesentryleft) + (dst_negative_scale_multiply_construct_prefixentriesentryleft)) * S ((dst_negative_code_multiply_construct_prefixentriesentryleft) + (dst_negative_scale_multiply_construct_prefixentriesentryleft)) + ((dst_negative_scale_multiply_construct_prefixentriesentryleft) + (dst_negative_scale_multiply_construct_prefixentriesentryleft))) + (((dst_negative_code_multiply_construct_prefixentriesentryleft) + (dst_negative_scale_multiply_construct_prefixentriesentryleft)) * S ((dst_negative_code_multiply_construct_prefixentriesentryleft) + (dst_negative_scale_multiply_construct_prefixentriesentryleft)) + ((dst_negative_scale_multiply_construct_prefixentriesentryleft) + (dst_negative_scale_multiply_construct_prefixentriesentryleft)))))) /\ (((((exists ff_h_pvs_multiply_construct_prefixentriesentryleftpositive. ff_h_pvs_multiply_construct_prefixentriesentryleftpositive + S (dst_positive_multiply_construct_prefixentriesentryleft) = S ((S (sto_index_multiply_construct_prefixentries)) * dst_positive_scale_multiply_construct_prefixentriesentryleft)) /\ exists ff_q_pvs_multiply_construct_prefixentriesentryleftpositive. dst_positive_code_multiply_construct_prefixentriesentryleft = ff_q_pvs_multiply_construct_prefixentriesentryleftpositive * S ((S (sto_index_multiply_construct_prefixentries)) * dst_positive_scale_multiply_construct_prefixentriesentryleft) + (dst_positive_multiply_construct_prefixentriesentryleft))) /\ (((((exists ff_h_pvs_multiply_construct_prefixentriesentryleftnegative. ff_h_pvs_multiply_construct_prefixentriesentryleftnegative + S (dst_negative_multiply_construct_prefixentriesentryleft) = S ((S (sto_index_multiply_construct_prefixentries)) * dst_negative_scale_multiply_construct_prefixentriesentryleft)) /\ exists ff_q_pvs_multiply_construct_prefixentriesentryleftnegative. dst_negative_code_multiply_construct_prefixentriesentryleft = ff_q_pvs_multiply_construct_prefixentriesentryleftnegative * S ((S (sto_index_multiply_construct_prefixentries)) * dst_negative_scale_multiply_construct_prefixentriesentryleft) + (dst_negative_multiply_construct_prefixentriesentryleft))) /\ (exists ge_balance_positive_multiply_construct_prefixentriesentryleftvalue ge_balance_negative_multiply_construct_prefixentriesentryleftvalue. (((((sto_left_multiply_construct_prefixentries) = 2 * (ge_balance_positive_multiply_construct_prefixentriesentryleftvalue) /\ (ge_balance_negative_multiply_construct_prefixentriesentryleftvalue) = 0) \/ exists ge_signed_half_multiply_construct_prefixentriesentryleftvaluedecode. (((sto_left_multiply_construct_prefixentries) = 2 * ge_signed_half_multiply_construct_prefixentriesentryleftvaluedecode + 1 /\ (ge_balance_positive_multiply_construct_prefixentriesentryleftvalue) = 0) /\ (ge_balance_negative_multiply_construct_prefixentriesentryleftvalue) = S ge_signed_half_multiply_construct_prefixentriesentryleftvaluedecode))) /\ ((dst_positive_multiply_construct_prefixentriesentryleft) + ge_balance_negative_multiply_construct_prefixentriesentryleftvalue = (dst_negative_multiply_construct_prefixentriesentryleft) + ge_balance_positive_multiply_construct_prefixentriesentryleftvalue))))))))) /\ (((exists dst_positive_code_multiply_construct_prefixentriesentryright dst_positive_scale_multiply_construct_prefixentriesentryright dst_negative_code_multiply_construct_prefixentriesentryright dst_negative_scale_multiply_construct_prefixentriesentryright dst_positive_multiply_construct_prefixentriesentryright dst_negative_multiply_construct_prefixentriesentryright. (((G) = (((((dst_positive_code_multiply_construct_prefixentriesentryright) + (dst_positive_scale_multiply_construct_prefixentriesentryright)) * S ((dst_positive_code_multiply_construct_prefixentriesentryright) + (dst_positive_scale_multiply_construct_prefixentriesentryright)) + ((dst_positive_scale_multiply_construct_prefixentriesentryright) + (dst_positive_scale_multiply_construct_prefixentriesentryright))) + (((dst_negative_code_multiply_construct_prefixentriesentryright) + (dst_negative_scale_multiply_construct_prefixentriesentryright)) * S ((dst_negative_code_multiply_construct_prefixentriesentryright) + (dst_negative_scale_multiply_construct_prefixentriesentryright)) + ((dst_negative_scale_multiply_construct_prefixentriesentryright) + (dst_negative_scale_multiply_construct_prefixentriesentryright)))) * S ((((dst_positive_code_multiply_construct_prefixentriesentryright) + (dst_positive_scale_multiply_construct_prefixentriesentryright)) * S ((dst_positive_code_multiply_construct_prefixentriesentryright) + (dst_positive_scale_multiply_construct_prefixentriesentryright)) + ((dst_positive_scale_multiply_construct_prefixentriesentryright) + (dst_positive_scale_multiply_construct_prefixentriesentryright))) + (((dst_negative_code_multiply_construct_prefixentriesentryright) + (dst_negative_scale_multiply_construct_prefixentriesentryright)) * S ((dst_negative_code_multiply_construct_prefixentriesentryright) + (dst_negative_scale_multiply_construct_prefixentriesentryright)) + ((dst_negative_scale_multiply_construct_prefixentriesentryright) + (dst_negative_scale_multiply_construct_prefixentriesentryright)))) + ((((dst_negative_code_multiply_construct_prefixentriesentryright) + (dst_negative_scale_multiply_construct_prefixentriesentryright)) * S ((dst_negative_code_multiply_construct_prefixentriesentryright) + (dst_negative_scale_multiply_construct_prefixentriesentryright)) + ((dst_negative_scale_multiply_construct_prefixentriesentryright) + (dst_negative_scale_multiply_construct_prefixentriesentryright))) + (((dst_negative_code_multiply_construct_prefixentriesentryright) + (dst_negative_scale_multiply_construct_prefixentriesentryright)) * S ((dst_negative_code_multiply_construct_prefixentriesentryright) + (dst_negative_scale_multiply_construct_prefixentriesentryright)) + ((dst_negative_scale_multiply_construct_prefixentriesentryright) + (dst_negative_scale_multiply_construct_prefixentriesentryright)))))) /\ (((((exists ff_h_pvs_multiply_construct_prefixentriesentryrightpositive. ff_h_pvs_multiply_construct_prefixentriesentryrightpositive + S (dst_positive_multiply_construct_prefixentriesentryright) = S ((S (sto_index_multiply_construct_prefixentries)) * dst_positive_scale_multiply_construct_prefixentriesentryright)) /\ exists ff_q_pvs_multiply_construct_prefixentriesentryrightpositive. dst_positive_code_multiply_construct_prefixentriesentryright = ff_q_pvs_multiply_construct_prefixentriesentryrightpositive * S ((S (sto_index_multiply_construct_prefixentries)) * dst_positive_scale_multiply_construct_prefixentriesentryright) + (dst_positive_multiply_construct_prefixentriesentryright))) /\ (((((exists ff_h_pvs_multiply_construct_prefixentriesentryrightnegative. ff_h_pvs_multiply_construct_prefixentriesentryrightnegative + S (dst_negative_multiply_construct_prefixentriesentryright) = S ((S (sto_index_multiply_construct_prefixentries)) * dst_negative_scale_multiply_construct_prefixentriesentryright)) /\ exists ff_q_pvs_multiply_construct_prefixentriesentryrightnegative. dst_negative_code_multiply_construct_prefixentriesentryright = ff_q_pvs_multiply_construct_prefixentriesentryrightnegative * S ((S (sto_index_multiply_construct_prefixentries)) * dst_negative_scale_multiply_construct_prefixentriesentryright) + (dst_negative_multiply_construct_prefixentriesentryright))) /\ (exists ge_balance_positive_multiply_construct_prefixentriesentryrightvalue ge_balance_negative_multiply_construct_prefixentriesentryrightvalue. (((((sto_right_multiply_construct_prefixentries) = 2 * (ge_balance_positive_multiply_construct_prefixentriesentryrightvalue) /\ (ge_balance_negative_multiply_construct_prefixentriesentryrightvalue) = 0) \/ exists ge_signed_half_multiply_construct_prefixentriesentryrightvaluedecode. (((sto_right_multiply_construct_prefixentries) = 2 * ge_signed_half_multiply_construct_prefixentriesentryrightvaluedecode + 1 /\ (ge_balance_positive_multiply_construct_prefixentriesentryrightvalue) = 0) /\ (ge_balance_negative_multiply_construct_prefixentriesentryrightvalue) = S ge_signed_half_multiply_construct_prefixentriesentryrightvaluedecode))) /\ ((dst_positive_multiply_construct_prefixentriesentryright) + ge_balance_negative_multiply_construct_prefixentriesentryrightvalue = (dst_negative_multiply_construct_prefixentriesentryright) + ge_balance_positive_multiply_construct_prefixentriesentryrightvalue))))))))) /\ (((exists dst_positive_code_multiply_construct_prefixentriesentryoutput dst_positive_scale_multiply_construct_prefixentriesentryoutput dst_negative_code_multiply_construct_prefixentriesentryoutput dst_negative_scale_multiply_construct_prefixentriesentryoutput dst_positive_multiply_construct_prefixentriesentryoutput dst_negative_multiply_construct_prefixentriesentryoutput. (((K) = (((((dst_positive_code_multiply_construct_prefixentriesentryoutput) + (dst_positive_scale_multiply_construct_prefixentriesentryoutput)) * S ((dst_positive_code_multiply_construct_prefixentriesentryoutput) + (dst_positive_scale_multiply_construct_prefixentriesentryoutput)) + ((dst_positive_scale_multiply_construct_prefixentriesentryoutput) + (dst_positive_scale_multiply_construct_prefixentriesentryoutput))) + (((dst_negative_code_multiply_construct_prefixentriesentryoutput) + (dst_negative_scale_multiply_construct_prefixentriesentryoutput)) * S ((dst_negative_code_multiply_construct_prefixentriesentryoutput) + (dst_negative_scale_multiply_construct_prefixentriesentryoutput)) + ((dst_negative_scale_multiply_construct_prefixentriesentryoutput) + (dst_negative_scale_multiply_construct_prefixentriesentryoutput)))) * S ((((dst_positive_code_multiply_construct_prefixentriesentryoutput) + (dst_positive_scale_multiply_construct_prefixentriesentryoutput)) * S ((dst_positive_code_multiply_construct_prefixentriesentryoutput) + (dst_positive_scale_multiply_construct_prefixentriesentryoutput)) + ((dst_positive_scale_multiply_construct_prefixentriesentryoutput) + (dst_positive_scale_multiply_construct_prefixentriesentryoutput))) + (((dst_negative_code_multiply_construct_prefixentriesentryoutput) + (dst_negative_scale_multiply_construct_prefixentriesentryoutput)) * S ((dst_negative_code_multiply_construct_prefixentriesentryoutput) + (dst_negative_scale_multiply_construct_prefixentriesentryoutput)) + ((dst_negative_scale_multiply_construct_prefixentriesentryoutput) + (dst_negative_scale_multiply_construct_prefixentriesentryoutput)))) + ((((dst_negative_code_multiply_construct_prefixentriesentryoutput) + (dst_negative_scale_multiply_construct_prefixentriesentryoutput)) * S ((dst_negative_code_multiply_construct_prefixentriesentryoutput) + (dst_negative_scale_multiply_construct_prefixentriesentryoutput)) + ((dst_negative_scale_multiply_construct_prefixentriesentryoutput) + (dst_negative_scale_multiply_construct_prefixentriesentryoutput))) + (((dst_negative_code_multiply_construct_prefixentriesentryoutput) + (dst_negative_scale_multiply_construct_prefixentriesentryoutput)) * S ((dst_negative_code_multiply_construct_prefixentriesentryoutput) + (dst_negative_scale_multiply_construct_prefixentriesentryoutput)) + ((dst_negative_scale_multiply_construct_prefixentriesentryoutput) + (dst_negative_scale_multiply_construct_prefixentriesentryoutput)))))) /\ (((((exists ff_h_pvs_multiply_construct_prefixentriesentryoutputpositive. ff_h_pvs_multiply_construct_prefixentriesentryoutputpositive + S (dst_positive_multiply_construct_prefixentriesentryoutput) = S ((S (sto_index_multiply_construct_prefixentries)) * dst_positive_scale_multiply_construct_prefixentriesentryoutput)) /\ exists ff_q_pvs_multiply_construct_prefixentriesentryoutputpositive. dst_positive_code_multiply_construct_prefixentriesentryoutput = ff_q_pvs_multiply_construct_prefixentriesentryoutputpositive * S ((S (sto_index_multiply_construct_prefixentries)) * dst_positive_scale_multiply_construct_prefixentriesentryoutput) + (dst_positive_multiply_construct_prefixentriesentryoutput))) /\ (((((exists ff_h_pvs_multiply_construct_prefixentriesentryoutputnegative. ff_h_pvs_multiply_construct_prefixentriesentryoutputnegative + S (dst_negative_multiply_construct_prefixentriesentryoutput) = S ((S (sto_index_multiply_construct_prefixentries)) * dst_negative_scale_multiply_construct_prefixentriesentryoutput)) /\ exists ff_q_pvs_multiply_construct_prefixentriesentryoutputnegative. dst_negative_code_multiply_construct_prefixentriesentryoutput = ff_q_pvs_multiply_construct_prefixentriesentryoutputnegative * S ((S (sto_index_multiply_construct_prefixentries)) * dst_negative_scale_multiply_construct_prefixentriesentryoutput) + (dst_negative_multiply_construct_prefixentriesentryoutput))) /\ (exists ge_balance_positive_multiply_construct_prefixentriesentryoutputvalue ge_balance_negative_multiply_construct_prefixentriesentryoutputvalue. (((((sto_output_multiply_construct_prefixentries) = 2 * (ge_balance_positive_multiply_construct_prefixentriesentryoutputvalue) /\ (ge_balance_negative_multiply_construct_prefixentriesentryoutputvalue) = 0) \/ exists ge_signed_half_multiply_construct_prefixentriesentryoutputvaluedecode. (((sto_output_multiply_construct_prefixentries) = 2 * ge_signed_half_multiply_construct_prefixentriesentryoutputvaluedecode + 1 /\ (ge_balance_positive_multiply_construct_prefixentriesentryoutputvalue) = 0) /\ (ge_balance_negative_multiply_construct_prefixentriesentryoutputvalue) = S ge_signed_half_multiply_construct_prefixentriesentryoutputvaluedecode))) /\ ((dst_positive_multiply_construct_prefixentriesentryoutput) + ge_balance_negative_multiply_construct_prefixentriesentryoutputvalue = (dst_negative_multiply_construct_prefixentriesentryoutput) + ge_balance_positive_multiply_construct_prefixentriesentryoutputvalue))))))))) /\ (exists sto_ap_multiply_construct_prefixentriesentryoperation sto_an_multiply_construct_prefixentriesentryoperation sto_bp_multiply_construct_prefixentriesentryoperation sto_bn_multiply_construct_prefixentriesentryoperation sto_cp_multiply_construct_prefixentriesentryoperation sto_cn_multiply_construct_prefixentriesentryoperation. (((((sto_left_multiply_construct_prefixentries) = 2 * (sto_ap_multiply_construct_prefixentriesentryoperation) /\ (sto_an_multiply_construct_prefixentriesentryoperation) = 0) \/ exists ge_signed_half_multiply_construct_prefixentriesentryoperationleft. (((sto_left_multiply_construct_prefixentries) = 2 * ge_signed_half_multiply_construct_prefixentriesentryoperationleft + 1 /\ (sto_ap_multiply_construct_prefixentriesentryoperation) = 0) /\ (sto_an_multiply_construct_prefixentriesentryoperation) = S ge_signed_half_multiply_construct_prefixentriesentryoperationleft))) /\ ((((((sto_right_multiply_construct_prefixentries) = 2 * (sto_bp_multiply_construct_prefixentriesentryoperation) /\ (sto_bn_multiply_construct_prefixentriesentryoperation) = 0) \/ exists ge_signed_half_multiply_construct_prefixentriesentryoperationright. (((sto_right_multiply_construct_prefixentries) = 2 * ge_signed_half_multiply_construct_prefixentriesentryoperationright + 1 /\ (sto_bp_multiply_construct_prefixentriesentryoperation) = 0) /\ (sto_bn_multiply_construct_prefixentriesentryoperation) = S ge_signed_half_multiply_construct_prefixentriesentryoperationright))) /\ ((((((sto_output_multiply_construct_prefixentries) = 2 * (sto_cp_multiply_construct_prefixentriesentryoperation) /\ (sto_cn_multiply_construct_prefixentriesentryoperation) = 0) \/ exists ge_signed_half_multiply_construct_prefixentriesentryoperationoutput. (((sto_output_multiply_construct_prefixentries) = 2 * ge_signed_half_multiply_construct_prefixentriesentryoperationoutput + 1 /\ (sto_cp_multiply_construct_prefixentriesentryoperation) = 0) /\ (sto_cn_multiply_construct_prefixentriesentryoperation) = S ge_signed_half_multiply_construct_prefixentriesentryoperationoutput))) /\ ((sto_ap_multiply_construct_prefixentriesentryoperation * sto_bp_multiply_construct_prefixentriesentryoperation + sto_an_multiply_construct_prefixentriesentryoperation * sto_bn_multiply_construct_prefixentriesentryoperation) + sto_cn_multiply_construct_prefixentriesentryoperation = (sto_ap_multiply_construct_prefixentriesentryoperation * sto_bn_multiply_construct_prefixentriesentryoperation + sto_an_multiply_construct_prefixentriesentryoperation * sto_bp_multiply_construct_prefixentriesentryoperation) + sto_cp_multiply_construct_prefixentriesentryoperation)))))))))))))))))))
  26. 0026specialize IH (F)
  27. 0027specialize IH (G)
  28. 0028apply IH
  29. 0029specialize signed_table_domain_resize (S l)
  30. 0030specialize signed_table_domain_resize (l)
  31. 0031specialize signed_table_domain_resize (F)
  32. 0032apply signed_table_domain_resize
  33. 0033exact ht0
  34. 0034specialize signed_table_domain_resize (S l)
  35. 0035specialize signed_table_domain_resize (l)
  36. 0036specialize signed_table_domain_resize (G)
  37. 0037apply signed_table_domain_resize
  38. 0038exact ht1
  39. 0039cases hp
  40. 0040have he0 : exists z. (exists dst_positive_code_multiply_construct_input0 dst_positive_scale_multiply_construct_input0 dst_negative_code_multiply_construct_input0 dst_negative_scale_multiply_construct_input0 dst_positive_multiply_construct_input0 dst_negative_multiply_construct_input0. (((F) = (((((dst_positive_code_multiply_construct_input0) + (dst_positive_scale_multiply_construct_input0)) * S ((dst_positive_code_multiply_construct_input0) + (dst_positive_scale_multiply_construct_input0)) + ((dst_positive_scale_multiply_construct_input0) + (dst_positive_scale_multiply_construct_input0))) + (((dst_negative_code_multiply_construct_input0) + (dst_negative_scale_multiply_construct_input0)) * S ((dst_negative_code_multiply_construct_input0) + (dst_negative_scale_multiply_construct_input0)) + ((dst_negative_scale_multiply_construct_input0) + (dst_negative_scale_multiply_construct_input0)))) * S ((((dst_positive_code_multiply_construct_input0) + (dst_positive_scale_multiply_construct_input0)) * S ((dst_positive_code_multiply_construct_input0) + (dst_positive_scale_multiply_construct_input0)) + ((dst_positive_scale_multiply_construct_input0) + (dst_positive_scale_multiply_construct_input0))) + (((dst_negative_code_multiply_construct_input0) + (dst_negative_scale_multiply_construct_input0)) * S ((dst_negative_code_multiply_construct_input0) + (dst_negative_scale_multiply_construct_input0)) + ((dst_negative_scale_multiply_construct_input0) + (dst_negative_scale_multiply_construct_input0)))) + ((((dst_negative_code_multiply_construct_input0) + (dst_negative_scale_multiply_construct_input0)) * S ((dst_negative_code_multiply_construct_input0) + (dst_negative_scale_multiply_construct_input0)) + ((dst_negative_scale_multiply_construct_input0) + (dst_negative_scale_multiply_construct_input0))) + (((dst_negative_code_multiply_construct_input0) + (dst_negative_scale_multiply_construct_input0)) * S ((dst_negative_code_multiply_construct_input0) + (dst_negative_scale_multiply_construct_input0)) + ((dst_negative_scale_multiply_construct_input0) + (dst_negative_scale_multiply_construct_input0)))))) /\ (((((exists ff_h_pvs_multiply_construct_input0positive. ff_h_pvs_multiply_construct_input0positive + S (dst_positive_multiply_construct_input0) = S ((S (l)) * dst_positive_scale_multiply_construct_input0)) /\ exists ff_q_pvs_multiply_construct_input0positive. dst_positive_code_multiply_construct_input0 = ff_q_pvs_multiply_construct_input0positive * S ((S (l)) * dst_positive_scale_multiply_construct_input0) + (dst_positive_multiply_construct_input0))) /\ (((((exists ff_h_pvs_multiply_construct_input0negative. ff_h_pvs_multiply_construct_input0negative + S (dst_negative_multiply_construct_input0) = S ((S (l)) * dst_negative_scale_multiply_construct_input0)) /\ exists ff_q_pvs_multiply_construct_input0negative. dst_negative_code_multiply_construct_input0 = ff_q_pvs_multiply_construct_input0negative * S ((S (l)) * dst_negative_scale_multiply_construct_input0) + (dst_negative_multiply_construct_input0))) /\ (exists ge_balance_positive_multiply_construct_input0value ge_balance_negative_multiply_construct_input0value. (((((z) = 2 * (ge_balance_positive_multiply_construct_input0value) /\ (ge_balance_negative_multiply_construct_input0value) = 0) \/ exists ge_signed_half_multiply_construct_input0valuedecode. (((z) = 2 * ge_signed_half_multiply_construct_input0valuedecode + 1 /\ (ge_balance_positive_multiply_construct_input0value) = 0) /\ (ge_balance_negative_multiply_construct_input0value) = S ge_signed_half_multiply_construct_input0valuedecode))) /\ ((dst_positive_multiply_construct_input0) + ge_balance_negative_multiply_construct_input0value = (dst_negative_multiply_construct_input0) + ge_balance_positive_multiply_construct_input0value)))))))))
  41. 0041specialize signed_table_lookup_any (S l)
  42. 0042specialize signed_table_lookup_any (F)
  43. 0043specialize signed_table_lookup_any (l)
  44. 0044apply signed_table_lookup_any
  45. 0045exact ht0
  46. 0046cases he0
  47. 0047have he1 : exists z. (exists dst_positive_code_multiply_construct_input1 dst_positive_scale_multiply_construct_input1 dst_negative_code_multiply_construct_input1 dst_negative_scale_multiply_construct_input1 dst_positive_multiply_construct_input1 dst_negative_multiply_construct_input1. (((G) = (((((dst_positive_code_multiply_construct_input1) + (dst_positive_scale_multiply_construct_input1)) * S ((dst_positive_code_multiply_construct_input1) + (dst_positive_scale_multiply_construct_input1)) + ((dst_positive_scale_multiply_construct_input1) + (dst_positive_scale_multiply_construct_input1))) + (((dst_negative_code_multiply_construct_input1) + (dst_negative_scale_multiply_construct_input1)) * S ((dst_negative_code_multiply_construct_input1) + (dst_negative_scale_multiply_construct_input1)) + ((dst_negative_scale_multiply_construct_input1) + (dst_negative_scale_multiply_construct_input1)))) * S ((((dst_positive_code_multiply_construct_input1) + (dst_positive_scale_multiply_construct_input1)) * S ((dst_positive_code_multiply_construct_input1) + (dst_positive_scale_multiply_construct_input1)) + ((dst_positive_scale_multiply_construct_input1) + (dst_positive_scale_multiply_construct_input1))) + (((dst_negative_code_multiply_construct_input1) + (dst_negative_scale_multiply_construct_input1)) * S ((dst_negative_code_multiply_construct_input1) + (dst_negative_scale_multiply_construct_input1)) + ((dst_negative_scale_multiply_construct_input1) + (dst_negative_scale_multiply_construct_input1)))) + ((((dst_negative_code_multiply_construct_input1) + (dst_negative_scale_multiply_construct_input1)) * S ((dst_negative_code_multiply_construct_input1) + (dst_negative_scale_multiply_construct_input1)) + ((dst_negative_scale_multiply_construct_input1) + (dst_negative_scale_multiply_construct_input1))) + (((dst_negative_code_multiply_construct_input1) + (dst_negative_scale_multiply_construct_input1)) * S ((dst_negative_code_multiply_construct_input1) + (dst_negative_scale_multiply_construct_input1)) + ((dst_negative_scale_multiply_construct_input1) + (dst_negative_scale_multiply_construct_input1)))))) /\ (((((exists ff_h_pvs_multiply_construct_input1positive. ff_h_pvs_multiply_construct_input1positive + S (dst_positive_multiply_construct_input1) = S ((S (l)) * dst_positive_scale_multiply_construct_input1)) /\ exists ff_q_pvs_multiply_construct_input1positive. dst_positive_code_multiply_construct_input1 = ff_q_pvs_multiply_construct_input1positive * S ((S (l)) * dst_positive_scale_multiply_construct_input1) + (dst_positive_multiply_construct_input1))) /\ (((((exists ff_h_pvs_multiply_construct_input1negative. ff_h_pvs_multiply_construct_input1negative + S (dst_negative_multiply_construct_input1) = S ((S (l)) * dst_negative_scale_multiply_construct_input1)) /\ exists ff_q_pvs_multiply_construct_input1negative. dst_negative_code_multiply_construct_input1 = ff_q_pvs_multiply_construct_input1negative * S ((S (l)) * dst_negative_scale_multiply_construct_input1) + (dst_negative_multiply_construct_input1))) /\ (exists ge_balance_positive_multiply_construct_input1value ge_balance_negative_multiply_construct_input1value. (((((z) = 2 * (ge_balance_positive_multiply_construct_input1value) /\ (ge_balance_negative_multiply_construct_input1value) = 0) \/ exists ge_signed_half_multiply_construct_input1valuedecode. (((z) = 2 * ge_signed_half_multiply_construct_input1valuedecode + 1 /\ (ge_balance_positive_multiply_construct_input1value) = 0) /\ (ge_balance_negative_multiply_construct_input1value) = S ge_signed_half_multiply_construct_input1valuedecode))) /\ ((dst_positive_multiply_construct_input1) + ge_balance_negative_multiply_construct_input1value = (dst_negative_multiply_construct_input1) + ge_balance_positive_multiply_construct_input1value)))))))))
  48. 0048specialize signed_table_lookup_any (S l)
  49. 0049specialize signed_table_lookup_any (G)
  50. 0050specialize signed_table_lookup_any (l)
  51. 0051apply signed_table_lookup_any
  52. 0052exact ht1
  53. 0053cases he1
  54. 0054have hv : exists z. (exists sto_ap_multiply_construct_operation sto_an_multiply_construct_operation sto_bp_multiply_construct_operation sto_bn_multiply_construct_operation sto_cp_multiply_construct_operation sto_cn_multiply_construct_operation. (((((x1) = 2 * (sto_ap_multiply_construct_operation) /\ (sto_an_multiply_construct_operation) = 0) \/ exists ge_signed_half_multiply_construct_operationleft. (((x1) = 2 * ge_signed_half_multiply_construct_operationleft + 1 /\ (sto_ap_multiply_construct_operation) = 0) /\ (sto_an_multiply_construct_operation) = S ge_signed_half_multiply_construct_operationleft))) /\ ((((((x2) = 2 * (sto_bp_multiply_construct_operation) /\ (sto_bn_multiply_construct_operation) = 0) \/ exists ge_signed_half_multiply_construct_operationright. (((x2) = 2 * ge_signed_half_multiply_construct_operationright + 1 /\ (sto_bp_multiply_construct_operation) = 0) /\ (sto_bn_multiply_construct_operation) = S ge_signed_half_multiply_construct_operationright))) /\ ((((((z) = 2 * (sto_cp_multiply_construct_operation) /\ (sto_cn_multiply_construct_operation) = 0) \/ exists ge_signed_half_multiply_construct_operationoutput. (((z) = 2 * ge_signed_half_multiply_construct_operationoutput + 1 /\ (sto_cp_multiply_construct_operation) = 0) /\ (sto_cn_multiply_construct_operation) = S ge_signed_half_multiply_construct_operationoutput))) /\ ((sto_ap_multiply_construct_operation * sto_bp_multiply_construct_operation + sto_an_multiply_construct_operation * sto_bn_multiply_construct_operation) + sto_cn_multiply_construct_operation = (sto_ap_multiply_construct_operation * sto_bn_multiply_construct_operation + sto_an_multiply_construct_operation * sto_bp_multiply_construct_operation) + sto_cp_multiply_construct_operation)))))))
  55. 0055specialize signed_mul_total (x1)
  56. 0056specialize signed_mul_total (x2)
  57. 0057apply signed_mul_total
  58. 0058cases hv
  59. 0059have hnext : exists K. ((exists dst_positive_code_multiply_construct_table dst_positive_scale_multiply_construct_table dst_negative_code_multiply_construct_table dst_negative_scale_multiply_construct_table. (((K) = (((((dst_positive_code_multiply_construct_table) + (dst_positive_scale_multiply_construct_table)) * S ((dst_positive_code_multiply_construct_table) + (dst_positive_scale_multiply_construct_table)) + ((dst_positive_scale_multiply_construct_table) + (dst_positive_scale_multiply_construct_table))) + (((dst_negative_code_multiply_construct_table) + (dst_negative_scale_multiply_construct_table)) * S ((dst_negative_code_multiply_construct_table) + (dst_negative_scale_multiply_construct_table)) + ((dst_negative_scale_multiply_construct_table) + (dst_negative_scale_multiply_construct_table)))) * S ((((dst_positive_code_multiply_construct_table) + (dst_positive_scale_multiply_construct_table)) * S ((dst_positive_code_multiply_construct_table) + (dst_positive_scale_multiply_construct_table)) + ((dst_positive_scale_multiply_construct_table) + (dst_positive_scale_multiply_construct_table))) + (((dst_negative_code_multiply_construct_table) + (dst_negative_scale_multiply_construct_table)) * S ((dst_negative_code_multiply_construct_table) + (dst_negative_scale_multiply_construct_table)) + ((dst_negative_scale_multiply_construct_table) + (dst_negative_scale_multiply_construct_table)))) + ((((dst_negative_code_multiply_construct_table) + (dst_negative_scale_multiply_construct_table)) * S ((dst_negative_code_multiply_construct_table) + (dst_negative_scale_multiply_construct_table)) + ((dst_negative_scale_multiply_construct_table) + (dst_negative_scale_multiply_construct_table))) + (((dst_negative_code_multiply_construct_table) + (dst_negative_scale_multiply_construct_table)) * S ((dst_negative_code_multiply_construct_table) + (dst_negative_scale_multiply_construct_table)) + ((dst_negative_scale_multiply_construct_table) + (dst_negative_scale_multiply_construct_table)))))) /\ (forall dst_index_multiply_construct_table. (exists pvs_le_gap_multiply_construct_tabledomain. pvs_le_gap_multiply_construct_tabledomain + (dst_index_multiply_construct_table) = (l)) -> exists dst_positive_multiply_construct_table dst_negative_multiply_construct_table dst_value_multiply_construct_table. ((((exists ff_h_pvs_multiply_construct_tableentrypositive. ff_h_pvs_multiply_construct_tableentrypositive + S (dst_positive_multiply_construct_table) = S ((S (dst_index_multiply_construct_table)) * dst_positive_scale_multiply_construct_table)) /\ exists ff_q_pvs_multiply_construct_tableentrypositive. dst_positive_code_multiply_construct_table = ff_q_pvs_multiply_construct_tableentrypositive * S ((S (dst_index_multiply_construct_table)) * dst_positive_scale_multiply_construct_table) + (dst_positive_multiply_construct_table))) /\ (((((exists ff_h_pvs_multiply_construct_tableentrynegative. ff_h_pvs_multiply_construct_tableentrynegative + S (dst_negative_multiply_construct_table) = S ((S (dst_index_multiply_construct_table)) * dst_negative_scale_multiply_construct_table)) /\ exists ff_q_pvs_multiply_construct_tableentrynegative. dst_negative_code_multiply_construct_table = ff_q_pvs_multiply_construct_tableentrynegative * S ((S (dst_index_multiply_construct_table)) * dst_negative_scale_multiply_construct_table) + (dst_negative_multiply_construct_table))) /\ (exists ge_balance_positive_multiply_construct_tableentryvalue ge_balance_negative_multiply_construct_tableentryvalue. (((((dst_value_multiply_construct_table) = 2 * (ge_balance_positive_multiply_construct_tableentryvalue) /\ (ge_balance_negative_multiply_construct_tableentryvalue) = 0) \/ exists ge_signed_half_multiply_construct_tableentryvaluedecode. (((dst_value_multiply_construct_table) = 2 * ge_signed_half_multiply_construct_tableentryvaluedecode + 1 /\ (ge_balance_positive_multiply_construct_tableentryvalue) = 0) /\ (ge_balance_negative_multiply_construct_tableentryvalue) = S ge_signed_half_multiply_construct_tableentryvaluedecode))) /\ ((dst_positive_multiply_construct_table) + ge_balance_negative_multiply_construct_tableentryvalue = (dst_negative_multiply_construct_table) + ge_balance_positive_multiply_construct_tableentryvalue))))))))) /\ (((forall dst_index_multiply_construct_equal dst_first_multiply_construct_equal dst_second_multiply_construct_equal. (exists pvs_gap_multiply_construct_equalbound. pvs_gap_multiply_construct_equalbound + S (dst_index_multiply_construct_equal) = (l)) -> (exists dst_positive_code_multiply_construct_equalfirst dst_positive_scale_multiply_construct_equalfirst dst_negative_code_multiply_construct_equalfirst dst_negative_scale_multiply_construct_equalfirst dst_positive_multiply_construct_equalfirst dst_negative_multiply_construct_equalfirst. (((x) = (((((dst_positive_code_multiply_construct_equalfirst) + (dst_positive_scale_multiply_construct_equalfirst)) * S ((dst_positive_code_multiply_construct_equalfirst) + (dst_positive_scale_multiply_construct_equalfirst)) + ((dst_positive_scale_multiply_construct_equalfirst) + (dst_positive_scale_multiply_construct_equalfirst))) + (((dst_negative_code_multiply_construct_equalfirst) + (dst_negative_scale_multiply_construct_equalfirst)) * S ((dst_negative_code_multiply_construct_equalfirst) + (dst_negative_scale_multiply_construct_equalfirst)) + ((dst_negative_scale_multiply_construct_equalfirst) + (dst_negative_scale_multiply_construct_equalfirst)))) * S ((((dst_positive_code_multiply_construct_equalfirst) + (dst_positive_scale_multiply_construct_equalfirst)) * S ((dst_positive_code_multiply_construct_equalfirst) + (dst_positive_scale_multiply_construct_equalfirst)) + ((dst_positive_scale_multiply_construct_equalfirst) + (dst_positive_scale_multiply_construct_equalfirst))) + (((dst_negative_code_multiply_construct_equalfirst) + (dst_negative_scale_multiply_construct_equalfirst)) * S ((dst_negative_code_multiply_construct_equalfirst) + (dst_negative_scale_multiply_construct_equalfirst)) + ((dst_negative_scale_multiply_construct_equalfirst) + (dst_negative_scale_multiply_construct_equalfirst)))) + ((((dst_negative_code_multiply_construct_equalfirst) + (dst_negative_scale_multiply_construct_equalfirst)) * S ((dst_negative_code_multiply_construct_equalfirst) + (dst_negative_scale_multiply_construct_equalfirst)) + ((dst_negative_scale_multiply_construct_equalfirst) + (dst_negative_scale_multiply_construct_equalfirst))) + (((dst_negative_code_multiply_construct_equalfirst) + (dst_negative_scale_multiply_construct_equalfirst)) * S ((dst_negative_code_multiply_construct_equalfirst) + (dst_negative_scale_multiply_construct_equalfirst)) + ((dst_negative_scale_multiply_construct_equalfirst) + (dst_negative_scale_multiply_construct_equalfirst)))))) /\ (((((exists ff_h_pvs_multiply_construct_equalfirstpositive. ff_h_pvs_multiply_construct_equalfirstpositive + S (dst_positive_multiply_construct_equalfirst) = S ((S (dst_index_multiply_construct_equal)) * dst_positive_scale_multiply_construct_equalfirst)) /\ exists ff_q_pvs_multiply_construct_equalfirstpositive. dst_positive_code_multiply_construct_equalfirst = ff_q_pvs_multiply_construct_equalfirstpositive * S ((S (dst_index_multiply_construct_equal)) * dst_positive_scale_multiply_construct_equalfirst) + (dst_positive_multiply_construct_equalfirst))) /\ (((((exists ff_h_pvs_multiply_construct_equalfirstnegative. ff_h_pvs_multiply_construct_equalfirstnegative + S (dst_negative_multiply_construct_equalfirst) = S ((S (dst_index_multiply_construct_equal)) * dst_negative_scale_multiply_construct_equalfirst)) /\ exists ff_q_pvs_multiply_construct_equalfirstnegative. dst_negative_code_multiply_construct_equalfirst = ff_q_pvs_multiply_construct_equalfirstnegative * S ((S (dst_index_multiply_construct_equal)) * dst_negative_scale_multiply_construct_equalfirst) + (dst_negative_multiply_construct_equalfirst))) /\ (exists ge_balance_positive_multiply_construct_equalfirstvalue ge_balance_negative_multiply_construct_equalfirstvalue. (((((dst_first_multiply_construct_equal) = 2 * (ge_balance_positive_multiply_construct_equalfirstvalue) /\ (ge_balance_negative_multiply_construct_equalfirstvalue) = 0) \/ exists ge_signed_half_multiply_construct_equalfirstvaluedecode. (((dst_first_multiply_construct_equal) = 2 * ge_signed_half_multiply_construct_equalfirstvaluedecode + 1 /\ (ge_balance_positive_multiply_construct_equalfirstvalue) = 0) /\ (ge_balance_negative_multiply_construct_equalfirstvalue) = S ge_signed_half_multiply_construct_equalfirstvaluedecode))) /\ ((dst_positive_multiply_construct_equalfirst) + ge_balance_negative_multiply_construct_equalfirstvalue = (dst_negative_multiply_construct_equalfirst) + ge_balance_positive_multiply_construct_equalfirstvalue))))))))) -> (exists dst_positive_code_multiply_construct_equalsecond dst_positive_scale_multiply_construct_equalsecond dst_negative_code_multiply_construct_equalsecond dst_negative_scale_multiply_construct_equalsecond dst_positive_multiply_construct_equalsecond dst_negative_multiply_construct_equalsecond. (((K) = (((((dst_positive_code_multiply_construct_equalsecond) + (dst_positive_scale_multiply_construct_equalsecond)) * S ((dst_positive_code_multiply_construct_equalsecond) + (dst_positive_scale_multiply_construct_equalsecond)) + ((dst_positive_scale_multiply_construct_equalsecond) + (dst_positive_scale_multiply_construct_equalsecond))) + (((dst_negative_code_multiply_construct_equalsecond) + (dst_negative_scale_multiply_construct_equalsecond)) * S ((dst_negative_code_multiply_construct_equalsecond) + (dst_negative_scale_multiply_construct_equalsecond)) + ((dst_negative_scale_multiply_construct_equalsecond) + (dst_negative_scale_multiply_construct_equalsecond)))) * S ((((dst_positive_code_multiply_construct_equalsecond) + (dst_positive_scale_multiply_construct_equalsecond)) * S ((dst_positive_code_multiply_construct_equalsecond) + (dst_positive_scale_multiply_construct_equalsecond)) + ((dst_positive_scale_multiply_construct_equalsecond) + (dst_positive_scale_multiply_construct_equalsecond))) + (((dst_negative_code_multiply_construct_equalsecond) + (dst_negative_scale_multiply_construct_equalsecond)) * S ((dst_negative_code_multiply_construct_equalsecond) + (dst_negative_scale_multiply_construct_equalsecond)) + ((dst_negative_scale_multiply_construct_equalsecond) + (dst_negative_scale_multiply_construct_equalsecond)))) + ((((dst_negative_code_multiply_construct_equalsecond) + (dst_negative_scale_multiply_construct_equalsecond)) * S ((dst_negative_code_multiply_construct_equalsecond) + (dst_negative_scale_multiply_construct_equalsecond)) + ((dst_negative_scale_multiply_construct_equalsecond) + (dst_negative_scale_multiply_construct_equalsecond))) + (((dst_negative_code_multiply_construct_equalsecond) + (dst_negative_scale_multiply_construct_equalsecond)) * S ((dst_negative_code_multiply_construct_equalsecond) + (dst_negative_scale_multiply_construct_equalsecond)) + ((dst_negative_scale_multiply_construct_equalsecond) + (dst_negative_scale_multiply_construct_equalsecond)))))) /\ (((((exists ff_h_pvs_multiply_construct_equalsecondpositive. ff_h_pvs_multiply_construct_equalsecondpositive + S (dst_positive_multiply_construct_equalsecond) = S ((S (dst_index_multiply_construct_equal)) * dst_positive_scale_multiply_construct_equalsecond)) /\ exists ff_q_pvs_multiply_construct_equalsecondpositive. dst_positive_code_multiply_construct_equalsecond = ff_q_pvs_multiply_construct_equalsecondpositive * S ((S (dst_index_multiply_construct_equal)) * dst_positive_scale_multiply_construct_equalsecond) + (dst_positive_multiply_construct_equalsecond))) /\ (((((exists ff_h_pvs_multiply_construct_equalsecondnegative. ff_h_pvs_multiply_construct_equalsecondnegative + S (dst_negative_multiply_construct_equalsecond) = S ((S (dst_index_multiply_construct_equal)) * dst_negative_scale_multiply_construct_equalsecond)) /\ exists ff_q_pvs_multiply_construct_equalsecondnegative. dst_negative_code_multiply_construct_equalsecond = ff_q_pvs_multiply_construct_equalsecondnegative * S ((S (dst_index_multiply_construct_equal)) * dst_negative_scale_multiply_construct_equalsecond) + (dst_negative_multiply_construct_equalsecond))) /\ (exists ge_balance_positive_multiply_construct_equalsecondvalue ge_balance_negative_multiply_construct_equalsecondvalue. (((((dst_second_multiply_construct_equal) = 2 * (ge_balance_positive_multiply_construct_equalsecondvalue) /\ (ge_balance_negative_multiply_construct_equalsecondvalue) = 0) \/ exists ge_signed_half_multiply_construct_equalsecondvaluedecode. (((dst_second_multiply_construct_equal) = 2 * ge_signed_half_multiply_construct_equalsecondvaluedecode + 1 /\ (ge_balance_positive_multiply_construct_equalsecondvalue) = 0) /\ (ge_balance_negative_multiply_construct_equalsecondvalue) = S ge_signed_half_multiply_construct_equalsecondvaluedecode))) /\ ((dst_positive_multiply_construct_equalsecond) + ge_balance_negative_multiply_construct_equalsecondvalue = (dst_negative_multiply_construct_equalsecond) + ge_balance_positive_multiply_construct_equalsecondvalue))))))))) -> dst_first_multiply_construct_equal = dst_second_multiply_construct_equal) /\ (exists dst_positive_code_multiply_construct_entry dst_positive_scale_multiply_construct_entry dst_negative_code_multiply_construct_entry dst_negative_scale_multiply_construct_entry dst_positive_multiply_construct_entry dst_negative_multiply_construct_entry. (((K) = (((((dst_positive_code_multiply_construct_entry) + (dst_positive_scale_multiply_construct_entry)) * S ((dst_positive_code_multiply_construct_entry) + (dst_positive_scale_multiply_construct_entry)) + ((dst_positive_scale_multiply_construct_entry) + (dst_positive_scale_multiply_construct_entry))) + (((dst_negative_code_multiply_construct_entry) + (dst_negative_scale_multiply_construct_entry)) * S ((dst_negative_code_multiply_construct_entry) + (dst_negative_scale_multiply_construct_entry)) + ((dst_negative_scale_multiply_construct_entry) + (dst_negative_scale_multiply_construct_entry)))) * S ((((dst_positive_code_multiply_construct_entry) + (dst_positive_scale_multiply_construct_entry)) * S ((dst_positive_code_multiply_construct_entry) + (dst_positive_scale_multiply_construct_entry)) + ((dst_positive_scale_multiply_construct_entry) + (dst_positive_scale_multiply_construct_entry))) + (((dst_negative_code_multiply_construct_entry) + (dst_negative_scale_multiply_construct_entry)) * S ((dst_negative_code_multiply_construct_entry) + (dst_negative_scale_multiply_construct_entry)) + ((dst_negative_scale_multiply_construct_entry) + (dst_negative_scale_multiply_construct_entry)))) + ((((dst_negative_code_multiply_construct_entry) + (dst_negative_scale_multiply_construct_entry)) * S ((dst_negative_code_multiply_construct_entry) + (dst_negative_scale_multiply_construct_entry)) + ((dst_negative_scale_multiply_construct_entry) + (dst_negative_scale_multiply_construct_entry))) + (((dst_negative_code_multiply_construct_entry) + (dst_negative_scale_multiply_construct_entry)) * S ((dst_negative_code_multiply_construct_entry) + (dst_negative_scale_multiply_construct_entry)) + ((dst_negative_scale_multiply_construct_entry) + (dst_negative_scale_multiply_construct_entry)))))) /\ (((((exists ff_h_pvs_multiply_construct_entrypositive. ff_h_pvs_multiply_construct_entrypositive + S (dst_positive_multiply_construct_entry) = S ((S (l)) * dst_positive_scale_multiply_construct_entry)) /\ exists ff_q_pvs_multiply_construct_entrypositive. dst_positive_code_multiply_construct_entry = ff_q_pvs_multiply_construct_entrypositive * S ((S (l)) * dst_positive_scale_multiply_construct_entry) + (dst_positive_multiply_construct_entry))) /\ (((((exists ff_h_pvs_multiply_construct_entrynegative. ff_h_pvs_multiply_construct_entrynegative + S (dst_negative_multiply_construct_entry) = S ((S (l)) * dst_negative_scale_multiply_construct_entry)) /\ exists ff_q_pvs_multiply_construct_entrynegative. dst_negative_code_multiply_construct_entry = ff_q_pvs_multiply_construct_entrynegative * S ((S (l)) * dst_negative_scale_multiply_construct_entry) + (dst_negative_multiply_construct_entry))) /\ (exists ge_balance_positive_multiply_construct_entryvalue ge_balance_negative_multiply_construct_entryvalue. (((((x3) = 2 * (ge_balance_positive_multiply_construct_entryvalue) /\ (ge_balance_negative_multiply_construct_entryvalue) = 0) \/ exists ge_signed_half_multiply_construct_entryvaluedecode. (((x3) = 2 * ge_signed_half_multiply_construct_entryvaluedecode + 1 /\ (ge_balance_positive_multiply_construct_entryvalue) = 0) /\ (ge_balance_negative_multiply_construct_entryvalue) = S ge_signed_half_multiply_construct_entryvaluedecode))) /\ ((dst_positive_multiply_construct_entry) + ge_balance_negative_multiply_construct_entryvalue = (dst_negative_multiply_construct_entry) + ge_balance_positive_multiply_construct_entryvalue))))))))))))
  60. 0060specialize arithmetic_signed_table_extend_at (l)
  61. 0061specialize arithmetic_signed_table_extend_at (x)
  62. 0062specialize arithmetic_signed_table_extend_at (l)
  63. 0063specialize arithmetic_signed_table_extend_at (x3)
  64. 0064apply arithmetic_signed_table_extend_at
  65. 0065cases hp_witness
  66. 0066cases hp_witness_right
  67. 0067cases hp_witness_right_right
  68. 0068exact hp_witness_right_right_left
  69. 0069cases hnext
  70. 0070cases hnext_witness
  71. 0071cases hnext_witness_right
  72. 0072exists x4
  73. 0073specialize signed_table_multiply_extend (F)
  74. 0074specialize signed_table_multiply_extend (G)
  75. 0075specialize signed_table_multiply_extend (x)
  76. 0076specialize signed_table_multiply_extend (x4)
  77. 0077specialize signed_table_multiply_extend (l)
  78. 0078specialize signed_table_multiply_extend (x1)
  79. 0079specialize signed_table_multiply_extend (x2)
  80. 0080specialize signed_table_multiply_extend (x3)
  81. 0081apply signed_table_multiply_extend
  82. 0082exact hp_witness
  83. 0083exact hnext_witness_left
  84. 0084exact hnext_witness_right_left
  85. 0085exact he0_witness
  86. 0086exact he1_witness
  87. 0087exact hnext_witness_right_right
  88. 0088exact hv_witness