WS0013

signed_table_multiply_exists

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.

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

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.

Operation tables contain actual beta-coded entries and compare represented signed values, not encodings. The strict sum window is i<l and the separately certified endpoint i=l is unused. Rectangular Fubini and full finite signed Möbius inversion are separate, now-admitted families.

Exact theorem in conservative defined notation

∀ l. ∀ F. ∀ G. ArithTable(l,F) → ArithTable(l,G) → ∃ x. ArithMul(F,G,x,l)

Every linked abbreviation expands hygienically to the identical original native formula.

Definition DAG

SignedMul(a,b,c) · 1ArithTable(N,F) · 2ArithAt(F,i,z) · 2ArithExtend(F,G,l,z) · 1ArithMul(F,G,H,l) · 2

Actual proof prerequisites

signed_table_multiply_emptydivisor_signed_table_from_components · checked external prerequisitesigned_table_domain_resizesigned_table_lookup_anysigned_mul_total · checked external prerequisitearithmetic_signed_table_extend_at · checked external prerequisitesigned_table_multiply_extend
Original expanded first-order 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)))))))))))))))))))

Complete tactic proof in conservative notation

All 88 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.

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.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

Named ingredients (4)
signed table multiply emptysigned table domain resizesigned table lookup anysigned table multiply extend
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(F,G,K,l)Original native command in the exact edition
  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(F,l,z)Original native command in the exact edition
  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(G,l,z)Original native command in the exact edition
  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(x1,x2,z)Original native command in the exact edition
  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(x,K,l,x3)Original native command in the exact edition
  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 defined 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 : ∃ K. ArithMul(F,G,K,l)
  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 : ∃ z. ArithAt(F,l,z)
  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 : ∃ z. ArithAt(G,l,z)
  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 : ∃ z. SignedMul(x1,x2,z)
  55. 0055specialize signed_mul_total (x1)
  56. 0056specialize signed_mul_total (x2)
  57. 0057apply signed_mul_total
  58. 0058cases hv
  59. 0059have hnext : ∃ K. ArithExtend(x,K,l,x3)
  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