WS0010

signed_table_add_exists

Ordinary finite induction constructs both beta output streams and their actual packed table for pointwise add; 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. ArithAdd(F,G,x,l)

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

Definition DAG

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

Actual proof prerequisites

signed_table_add_emptydivisor_signed_table_from_components · checked external prerequisitesigned_table_domain_resizesigned_table_lookup_anysigned_add_total · checked external prerequisitearithmetic_signed_table_extend_at · checked external prerequisitesigned_table_add_extend
Original expanded first-order statement 
forall l F G. (exists dst_positive_code_add_exists_input0 dst_positive_scale_add_exists_input0 dst_negative_code_add_exists_input0 dst_negative_scale_add_exists_input0. (((F) = (((((dst_positive_code_add_exists_input0) + (dst_positive_scale_add_exists_input0)) * S ((dst_positive_code_add_exists_input0) + (dst_positive_scale_add_exists_input0)) + ((dst_positive_scale_add_exists_input0) + (dst_positive_scale_add_exists_input0))) + (((dst_negative_code_add_exists_input0) + (dst_negative_scale_add_exists_input0)) * S ((dst_negative_code_add_exists_input0) + (dst_negative_scale_add_exists_input0)) + ((dst_negative_scale_add_exists_input0) + (dst_negative_scale_add_exists_input0)))) * S ((((dst_positive_code_add_exists_input0) + (dst_positive_scale_add_exists_input0)) * S ((dst_positive_code_add_exists_input0) + (dst_positive_scale_add_exists_input0)) + ((dst_positive_scale_add_exists_input0) + (dst_positive_scale_add_exists_input0))) + (((dst_negative_code_add_exists_input0) + (dst_negative_scale_add_exists_input0)) * S ((dst_negative_code_add_exists_input0) + (dst_negative_scale_add_exists_input0)) + ((dst_negative_scale_add_exists_input0) + (dst_negative_scale_add_exists_input0)))) + ((((dst_negative_code_add_exists_input0) + (dst_negative_scale_add_exists_input0)) * S ((dst_negative_code_add_exists_input0) + (dst_negative_scale_add_exists_input0)) + ((dst_negative_scale_add_exists_input0) + (dst_negative_scale_add_exists_input0))) + (((dst_negative_code_add_exists_input0) + (dst_negative_scale_add_exists_input0)) * S ((dst_negative_code_add_exists_input0) + (dst_negative_scale_add_exists_input0)) + ((dst_negative_scale_add_exists_input0) + (dst_negative_scale_add_exists_input0)))))) /\ (forall dst_index_add_exists_input0. (exists pvs_le_gap_add_exists_input0domain. pvs_le_gap_add_exists_input0domain + (dst_index_add_exists_input0) = (l)) -> exists dst_positive_add_exists_input0 dst_negative_add_exists_input0 dst_value_add_exists_input0. ((((exists ff_h_pvs_add_exists_input0entrypositive. ff_h_pvs_add_exists_input0entrypositive + S (dst_positive_add_exists_input0) = S ((S (dst_index_add_exists_input0)) * dst_positive_scale_add_exists_input0)) /\ exists ff_q_pvs_add_exists_input0entrypositive. dst_positive_code_add_exists_input0 = ff_q_pvs_add_exists_input0entrypositive * S ((S (dst_index_add_exists_input0)) * dst_positive_scale_add_exists_input0) + (dst_positive_add_exists_input0))) /\ (((((exists ff_h_pvs_add_exists_input0entrynegative. ff_h_pvs_add_exists_input0entrynegative + S (dst_negative_add_exists_input0) = S ((S (dst_index_add_exists_input0)) * dst_negative_scale_add_exists_input0)) /\ exists ff_q_pvs_add_exists_input0entrynegative. dst_negative_code_add_exists_input0 = ff_q_pvs_add_exists_input0entrynegative * S ((S (dst_index_add_exists_input0)) * dst_negative_scale_add_exists_input0) + (dst_negative_add_exists_input0))) /\ (exists ge_balance_positive_add_exists_input0entryvalue ge_balance_negative_add_exists_input0entryvalue. (((((dst_value_add_exists_input0) = 2 * (ge_balance_positive_add_exists_input0entryvalue) /\ (ge_balance_negative_add_exists_input0entryvalue) = 0) \/ exists ge_signed_half_add_exists_input0entryvaluedecode. (((dst_value_add_exists_input0) = 2 * ge_signed_half_add_exists_input0entryvaluedecode + 1 /\ (ge_balance_positive_add_exists_input0entryvalue) = 0) /\ (ge_balance_negative_add_exists_input0entryvalue) = S ge_signed_half_add_exists_input0entryvaluedecode))) /\ ((dst_positive_add_exists_input0) + ge_balance_negative_add_exists_input0entryvalue = (dst_negative_add_exists_input0) + ge_balance_positive_add_exists_input0entryvalue))))))))) -> (exists dst_positive_code_add_exists_input1 dst_positive_scale_add_exists_input1 dst_negative_code_add_exists_input1 dst_negative_scale_add_exists_input1. (((G) = (((((dst_positive_code_add_exists_input1) + (dst_positive_scale_add_exists_input1)) * S ((dst_positive_code_add_exists_input1) + (dst_positive_scale_add_exists_input1)) + ((dst_positive_scale_add_exists_input1) + (dst_positive_scale_add_exists_input1))) + (((dst_negative_code_add_exists_input1) + (dst_negative_scale_add_exists_input1)) * S ((dst_negative_code_add_exists_input1) + (dst_negative_scale_add_exists_input1)) + ((dst_negative_scale_add_exists_input1) + (dst_negative_scale_add_exists_input1)))) * S ((((dst_positive_code_add_exists_input1) + (dst_positive_scale_add_exists_input1)) * S ((dst_positive_code_add_exists_input1) + (dst_positive_scale_add_exists_input1)) + ((dst_positive_scale_add_exists_input1) + (dst_positive_scale_add_exists_input1))) + (((dst_negative_code_add_exists_input1) + (dst_negative_scale_add_exists_input1)) * S ((dst_negative_code_add_exists_input1) + (dst_negative_scale_add_exists_input1)) + ((dst_negative_scale_add_exists_input1) + (dst_negative_scale_add_exists_input1)))) + ((((dst_negative_code_add_exists_input1) + (dst_negative_scale_add_exists_input1)) * S ((dst_negative_code_add_exists_input1) + (dst_negative_scale_add_exists_input1)) + ((dst_negative_scale_add_exists_input1) + (dst_negative_scale_add_exists_input1))) + (((dst_negative_code_add_exists_input1) + (dst_negative_scale_add_exists_input1)) * S ((dst_negative_code_add_exists_input1) + (dst_negative_scale_add_exists_input1)) + ((dst_negative_scale_add_exists_input1) + (dst_negative_scale_add_exists_input1)))))) /\ (forall dst_index_add_exists_input1. (exists pvs_le_gap_add_exists_input1domain. pvs_le_gap_add_exists_input1domain + (dst_index_add_exists_input1) = (l)) -> exists dst_positive_add_exists_input1 dst_negative_add_exists_input1 dst_value_add_exists_input1. ((((exists ff_h_pvs_add_exists_input1entrypositive. ff_h_pvs_add_exists_input1entrypositive + S (dst_positive_add_exists_input1) = S ((S (dst_index_add_exists_input1)) * dst_positive_scale_add_exists_input1)) /\ exists ff_q_pvs_add_exists_input1entrypositive. dst_positive_code_add_exists_input1 = ff_q_pvs_add_exists_input1entrypositive * S ((S (dst_index_add_exists_input1)) * dst_positive_scale_add_exists_input1) + (dst_positive_add_exists_input1))) /\ (((((exists ff_h_pvs_add_exists_input1entrynegative. ff_h_pvs_add_exists_input1entrynegative + S (dst_negative_add_exists_input1) = S ((S (dst_index_add_exists_input1)) * dst_negative_scale_add_exists_input1)) /\ exists ff_q_pvs_add_exists_input1entrynegative. dst_negative_code_add_exists_input1 = ff_q_pvs_add_exists_input1entrynegative * S ((S (dst_index_add_exists_input1)) * dst_negative_scale_add_exists_input1) + (dst_negative_add_exists_input1))) /\ (exists ge_balance_positive_add_exists_input1entryvalue ge_balance_negative_add_exists_input1entryvalue. (((((dst_value_add_exists_input1) = 2 * (ge_balance_positive_add_exists_input1entryvalue) /\ (ge_balance_negative_add_exists_input1entryvalue) = 0) \/ exists ge_signed_half_add_exists_input1entryvaluedecode. (((dst_value_add_exists_input1) = 2 * ge_signed_half_add_exists_input1entryvaluedecode + 1 /\ (ge_balance_positive_add_exists_input1entryvalue) = 0) /\ (ge_balance_negative_add_exists_input1entryvalue) = S ge_signed_half_add_exists_input1entryvaluedecode))) /\ ((dst_positive_add_exists_input1) + ge_balance_negative_add_exists_input1entryvalue = (dst_negative_add_exists_input1) + ge_balance_positive_add_exists_input1entryvalue))))))))) -> exists H. (((exists dst_positive_code_add_exists_resultleft_table dst_positive_scale_add_exists_resultleft_table dst_negative_code_add_exists_resultleft_table dst_negative_scale_add_exists_resultleft_table. (((F) = (((((dst_positive_code_add_exists_resultleft_table) + (dst_positive_scale_add_exists_resultleft_table)) * S ((dst_positive_code_add_exists_resultleft_table) + (dst_positive_scale_add_exists_resultleft_table)) + ((dst_positive_scale_add_exists_resultleft_table) + (dst_positive_scale_add_exists_resultleft_table))) + (((dst_negative_code_add_exists_resultleft_table) + (dst_negative_scale_add_exists_resultleft_table)) * S ((dst_negative_code_add_exists_resultleft_table) + (dst_negative_scale_add_exists_resultleft_table)) + ((dst_negative_scale_add_exists_resultleft_table) + (dst_negative_scale_add_exists_resultleft_table)))) * S ((((dst_positive_code_add_exists_resultleft_table) + (dst_positive_scale_add_exists_resultleft_table)) * S ((dst_positive_code_add_exists_resultleft_table) + (dst_positive_scale_add_exists_resultleft_table)) + ((dst_positive_scale_add_exists_resultleft_table) + (dst_positive_scale_add_exists_resultleft_table))) + (((dst_negative_code_add_exists_resultleft_table) + (dst_negative_scale_add_exists_resultleft_table)) * S ((dst_negative_code_add_exists_resultleft_table) + (dst_negative_scale_add_exists_resultleft_table)) + ((dst_negative_scale_add_exists_resultleft_table) + (dst_negative_scale_add_exists_resultleft_table)))) + ((((dst_negative_code_add_exists_resultleft_table) + (dst_negative_scale_add_exists_resultleft_table)) * S ((dst_negative_code_add_exists_resultleft_table) + (dst_negative_scale_add_exists_resultleft_table)) + ((dst_negative_scale_add_exists_resultleft_table) + (dst_negative_scale_add_exists_resultleft_table))) + (((dst_negative_code_add_exists_resultleft_table) + (dst_negative_scale_add_exists_resultleft_table)) * S ((dst_negative_code_add_exists_resultleft_table) + (dst_negative_scale_add_exists_resultleft_table)) + ((dst_negative_scale_add_exists_resultleft_table) + (dst_negative_scale_add_exists_resultleft_table)))))) /\ (forall dst_index_add_exists_resultleft_table. (exists pvs_le_gap_add_exists_resultleft_tabledomain. pvs_le_gap_add_exists_resultleft_tabledomain + (dst_index_add_exists_resultleft_table) = (l)) -> exists dst_positive_add_exists_resultleft_table dst_negative_add_exists_resultleft_table dst_value_add_exists_resultleft_table. ((((exists ff_h_pvs_add_exists_resultleft_tableentrypositive. ff_h_pvs_add_exists_resultleft_tableentrypositive + S (dst_positive_add_exists_resultleft_table) = S ((S (dst_index_add_exists_resultleft_table)) * dst_positive_scale_add_exists_resultleft_table)) /\ exists ff_q_pvs_add_exists_resultleft_tableentrypositive. dst_positive_code_add_exists_resultleft_table = ff_q_pvs_add_exists_resultleft_tableentrypositive * S ((S (dst_index_add_exists_resultleft_table)) * dst_positive_scale_add_exists_resultleft_table) + (dst_positive_add_exists_resultleft_table))) /\ (((((exists ff_h_pvs_add_exists_resultleft_tableentrynegative. ff_h_pvs_add_exists_resultleft_tableentrynegative + S (dst_negative_add_exists_resultleft_table) = S ((S (dst_index_add_exists_resultleft_table)) * dst_negative_scale_add_exists_resultleft_table)) /\ exists ff_q_pvs_add_exists_resultleft_tableentrynegative. dst_negative_code_add_exists_resultleft_table = ff_q_pvs_add_exists_resultleft_tableentrynegative * S ((S (dst_index_add_exists_resultleft_table)) * dst_negative_scale_add_exists_resultleft_table) + (dst_negative_add_exists_resultleft_table))) /\ (exists ge_balance_positive_add_exists_resultleft_tableentryvalue ge_balance_negative_add_exists_resultleft_tableentryvalue. (((((dst_value_add_exists_resultleft_table) = 2 * (ge_balance_positive_add_exists_resultleft_tableentryvalue) /\ (ge_balance_negative_add_exists_resultleft_tableentryvalue) = 0) \/ exists ge_signed_half_add_exists_resultleft_tableentryvaluedecode. (((dst_value_add_exists_resultleft_table) = 2 * ge_signed_half_add_exists_resultleft_tableentryvaluedecode + 1 /\ (ge_balance_positive_add_exists_resultleft_tableentryvalue) = 0) /\ (ge_balance_negative_add_exists_resultleft_tableentryvalue) = S ge_signed_half_add_exists_resultleft_tableentryvaluedecode))) /\ ((dst_positive_add_exists_resultleft_table) + ge_balance_negative_add_exists_resultleft_tableentryvalue = (dst_negative_add_exists_resultleft_table) + ge_balance_positive_add_exists_resultleft_tableentryvalue))))))))) /\ (((exists dst_positive_code_add_exists_resultright_table dst_positive_scale_add_exists_resultright_table dst_negative_code_add_exists_resultright_table dst_negative_scale_add_exists_resultright_table. (((G) = (((((dst_positive_code_add_exists_resultright_table) + (dst_positive_scale_add_exists_resultright_table)) * S ((dst_positive_code_add_exists_resultright_table) + (dst_positive_scale_add_exists_resultright_table)) + ((dst_positive_scale_add_exists_resultright_table) + (dst_positive_scale_add_exists_resultright_table))) + (((dst_negative_code_add_exists_resultright_table) + (dst_negative_scale_add_exists_resultright_table)) * S ((dst_negative_code_add_exists_resultright_table) + (dst_negative_scale_add_exists_resultright_table)) + ((dst_negative_scale_add_exists_resultright_table) + (dst_negative_scale_add_exists_resultright_table)))) * S ((((dst_positive_code_add_exists_resultright_table) + (dst_positive_scale_add_exists_resultright_table)) * S ((dst_positive_code_add_exists_resultright_table) + (dst_positive_scale_add_exists_resultright_table)) + ((dst_positive_scale_add_exists_resultright_table) + (dst_positive_scale_add_exists_resultright_table))) + (((dst_negative_code_add_exists_resultright_table) + (dst_negative_scale_add_exists_resultright_table)) * S ((dst_negative_code_add_exists_resultright_table) + (dst_negative_scale_add_exists_resultright_table)) + ((dst_negative_scale_add_exists_resultright_table) + (dst_negative_scale_add_exists_resultright_table)))) + ((((dst_negative_code_add_exists_resultright_table) + (dst_negative_scale_add_exists_resultright_table)) * S ((dst_negative_code_add_exists_resultright_table) + (dst_negative_scale_add_exists_resultright_table)) + ((dst_negative_scale_add_exists_resultright_table) + (dst_negative_scale_add_exists_resultright_table))) + (((dst_negative_code_add_exists_resultright_table) + (dst_negative_scale_add_exists_resultright_table)) * S ((dst_negative_code_add_exists_resultright_table) + (dst_negative_scale_add_exists_resultright_table)) + ((dst_negative_scale_add_exists_resultright_table) + (dst_negative_scale_add_exists_resultright_table)))))) /\ (forall dst_index_add_exists_resultright_table. (exists pvs_le_gap_add_exists_resultright_tabledomain. pvs_le_gap_add_exists_resultright_tabledomain + (dst_index_add_exists_resultright_table) = (l)) -> exists dst_positive_add_exists_resultright_table dst_negative_add_exists_resultright_table dst_value_add_exists_resultright_table. ((((exists ff_h_pvs_add_exists_resultright_tableentrypositive. ff_h_pvs_add_exists_resultright_tableentrypositive + S (dst_positive_add_exists_resultright_table) = S ((S (dst_index_add_exists_resultright_table)) * dst_positive_scale_add_exists_resultright_table)) /\ exists ff_q_pvs_add_exists_resultright_tableentrypositive. dst_positive_code_add_exists_resultright_table = ff_q_pvs_add_exists_resultright_tableentrypositive * S ((S (dst_index_add_exists_resultright_table)) * dst_positive_scale_add_exists_resultright_table) + (dst_positive_add_exists_resultright_table))) /\ (((((exists ff_h_pvs_add_exists_resultright_tableentrynegative. ff_h_pvs_add_exists_resultright_tableentrynegative + S (dst_negative_add_exists_resultright_table) = S ((S (dst_index_add_exists_resultright_table)) * dst_negative_scale_add_exists_resultright_table)) /\ exists ff_q_pvs_add_exists_resultright_tableentrynegative. dst_negative_code_add_exists_resultright_table = ff_q_pvs_add_exists_resultright_tableentrynegative * S ((S (dst_index_add_exists_resultright_table)) * dst_negative_scale_add_exists_resultright_table) + (dst_negative_add_exists_resultright_table))) /\ (exists ge_balance_positive_add_exists_resultright_tableentryvalue ge_balance_negative_add_exists_resultright_tableentryvalue. (((((dst_value_add_exists_resultright_table) = 2 * (ge_balance_positive_add_exists_resultright_tableentryvalue) /\ (ge_balance_negative_add_exists_resultright_tableentryvalue) = 0) \/ exists ge_signed_half_add_exists_resultright_tableentryvaluedecode. (((dst_value_add_exists_resultright_table) = 2 * ge_signed_half_add_exists_resultright_tableentryvaluedecode + 1 /\ (ge_balance_positive_add_exists_resultright_tableentryvalue) = 0) /\ (ge_balance_negative_add_exists_resultright_tableentryvalue) = S ge_signed_half_add_exists_resultright_tableentryvaluedecode))) /\ ((dst_positive_add_exists_resultright_table) + ge_balance_negative_add_exists_resultright_tableentryvalue = (dst_negative_add_exists_resultright_table) + ge_balance_positive_add_exists_resultright_tableentryvalue))))))))) /\ (((exists dst_positive_code_add_exists_resultoutput_table dst_positive_scale_add_exists_resultoutput_table dst_negative_code_add_exists_resultoutput_table dst_negative_scale_add_exists_resultoutput_table. (((H) = (((((dst_positive_code_add_exists_resultoutput_table) + (dst_positive_scale_add_exists_resultoutput_table)) * S ((dst_positive_code_add_exists_resultoutput_table) + (dst_positive_scale_add_exists_resultoutput_table)) + ((dst_positive_scale_add_exists_resultoutput_table) + (dst_positive_scale_add_exists_resultoutput_table))) + (((dst_negative_code_add_exists_resultoutput_table) + (dst_negative_scale_add_exists_resultoutput_table)) * S ((dst_negative_code_add_exists_resultoutput_table) + (dst_negative_scale_add_exists_resultoutput_table)) + ((dst_negative_scale_add_exists_resultoutput_table) + (dst_negative_scale_add_exists_resultoutput_table)))) * S ((((dst_positive_code_add_exists_resultoutput_table) + (dst_positive_scale_add_exists_resultoutput_table)) * S ((dst_positive_code_add_exists_resultoutput_table) + (dst_positive_scale_add_exists_resultoutput_table)) + ((dst_positive_scale_add_exists_resultoutput_table) + (dst_positive_scale_add_exists_resultoutput_table))) + (((dst_negative_code_add_exists_resultoutput_table) + (dst_negative_scale_add_exists_resultoutput_table)) * S ((dst_negative_code_add_exists_resultoutput_table) + (dst_negative_scale_add_exists_resultoutput_table)) + ((dst_negative_scale_add_exists_resultoutput_table) + (dst_negative_scale_add_exists_resultoutput_table)))) + ((((dst_negative_code_add_exists_resultoutput_table) + (dst_negative_scale_add_exists_resultoutput_table)) * S ((dst_negative_code_add_exists_resultoutput_table) + (dst_negative_scale_add_exists_resultoutput_table)) + ((dst_negative_scale_add_exists_resultoutput_table) + (dst_negative_scale_add_exists_resultoutput_table))) + (((dst_negative_code_add_exists_resultoutput_table) + (dst_negative_scale_add_exists_resultoutput_table)) * S ((dst_negative_code_add_exists_resultoutput_table) + (dst_negative_scale_add_exists_resultoutput_table)) + ((dst_negative_scale_add_exists_resultoutput_table) + (dst_negative_scale_add_exists_resultoutput_table)))))) /\ (forall dst_index_add_exists_resultoutput_table. (exists pvs_le_gap_add_exists_resultoutput_tabledomain. pvs_le_gap_add_exists_resultoutput_tabledomain + (dst_index_add_exists_resultoutput_table) = (l)) -> exists dst_positive_add_exists_resultoutput_table dst_negative_add_exists_resultoutput_table dst_value_add_exists_resultoutput_table. ((((exists ff_h_pvs_add_exists_resultoutput_tableentrypositive. ff_h_pvs_add_exists_resultoutput_tableentrypositive + S (dst_positive_add_exists_resultoutput_table) = S ((S (dst_index_add_exists_resultoutput_table)) * dst_positive_scale_add_exists_resultoutput_table)) /\ exists ff_q_pvs_add_exists_resultoutput_tableentrypositive. dst_positive_code_add_exists_resultoutput_table = ff_q_pvs_add_exists_resultoutput_tableentrypositive * S ((S (dst_index_add_exists_resultoutput_table)) * dst_positive_scale_add_exists_resultoutput_table) + (dst_positive_add_exists_resultoutput_table))) /\ (((((exists ff_h_pvs_add_exists_resultoutput_tableentrynegative. ff_h_pvs_add_exists_resultoutput_tableentrynegative + S (dst_negative_add_exists_resultoutput_table) = S ((S (dst_index_add_exists_resultoutput_table)) * dst_negative_scale_add_exists_resultoutput_table)) /\ exists ff_q_pvs_add_exists_resultoutput_tableentrynegative. dst_negative_code_add_exists_resultoutput_table = ff_q_pvs_add_exists_resultoutput_tableentrynegative * S ((S (dst_index_add_exists_resultoutput_table)) * dst_negative_scale_add_exists_resultoutput_table) + (dst_negative_add_exists_resultoutput_table))) /\ (exists ge_balance_positive_add_exists_resultoutput_tableentryvalue ge_balance_negative_add_exists_resultoutput_tableentryvalue. (((((dst_value_add_exists_resultoutput_table) = 2 * (ge_balance_positive_add_exists_resultoutput_tableentryvalue) /\ (ge_balance_negative_add_exists_resultoutput_tableentryvalue) = 0) \/ exists ge_signed_half_add_exists_resultoutput_tableentryvaluedecode. (((dst_value_add_exists_resultoutput_table) = 2 * ge_signed_half_add_exists_resultoutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_add_exists_resultoutput_tableentryvalue) = 0) /\ (ge_balance_negative_add_exists_resultoutput_tableentryvalue) = S ge_signed_half_add_exists_resultoutput_tableentryvaluedecode))) /\ ((dst_positive_add_exists_resultoutput_table) + ge_balance_negative_add_exists_resultoutput_tableentryvalue = (dst_negative_add_exists_resultoutput_table) + ge_balance_positive_add_exists_resultoutput_tableentryvalue))))))))) /\ (forall sto_index_add_exists_resultentries. (exists pvs_gap_add_exists_resultentriesbound. pvs_gap_add_exists_resultentriesbound + S (sto_index_add_exists_resultentries) = (l)) -> exists sto_left_add_exists_resultentries sto_right_add_exists_resultentries sto_output_add_exists_resultentries. ((exists dst_positive_code_add_exists_resultentriesentryleft dst_positive_scale_add_exists_resultentriesentryleft dst_negative_code_add_exists_resultentriesentryleft dst_negative_scale_add_exists_resultentriesentryleft dst_positive_add_exists_resultentriesentryleft dst_negative_add_exists_resultentriesentryleft. (((F) = (((((dst_positive_code_add_exists_resultentriesentryleft) + (dst_positive_scale_add_exists_resultentriesentryleft)) * S ((dst_positive_code_add_exists_resultentriesentryleft) + (dst_positive_scale_add_exists_resultentriesentryleft)) + ((dst_positive_scale_add_exists_resultentriesentryleft) + (dst_positive_scale_add_exists_resultentriesentryleft))) + (((dst_negative_code_add_exists_resultentriesentryleft) + (dst_negative_scale_add_exists_resultentriesentryleft)) * S ((dst_negative_code_add_exists_resultentriesentryleft) + (dst_negative_scale_add_exists_resultentriesentryleft)) + ((dst_negative_scale_add_exists_resultentriesentryleft) + (dst_negative_scale_add_exists_resultentriesentryleft)))) * S ((((dst_positive_code_add_exists_resultentriesentryleft) + (dst_positive_scale_add_exists_resultentriesentryleft)) * S ((dst_positive_code_add_exists_resultentriesentryleft) + (dst_positive_scale_add_exists_resultentriesentryleft)) + ((dst_positive_scale_add_exists_resultentriesentryleft) + (dst_positive_scale_add_exists_resultentriesentryleft))) + (((dst_negative_code_add_exists_resultentriesentryleft) + (dst_negative_scale_add_exists_resultentriesentryleft)) * S ((dst_negative_code_add_exists_resultentriesentryleft) + (dst_negative_scale_add_exists_resultentriesentryleft)) + ((dst_negative_scale_add_exists_resultentriesentryleft) + (dst_negative_scale_add_exists_resultentriesentryleft)))) + ((((dst_negative_code_add_exists_resultentriesentryleft) + (dst_negative_scale_add_exists_resultentriesentryleft)) * S ((dst_negative_code_add_exists_resultentriesentryleft) + (dst_negative_scale_add_exists_resultentriesentryleft)) + ((dst_negative_scale_add_exists_resultentriesentryleft) + (dst_negative_scale_add_exists_resultentriesentryleft))) + (((dst_negative_code_add_exists_resultentriesentryleft) + (dst_negative_scale_add_exists_resultentriesentryleft)) * S ((dst_negative_code_add_exists_resultentriesentryleft) + (dst_negative_scale_add_exists_resultentriesentryleft)) + ((dst_negative_scale_add_exists_resultentriesentryleft) + (dst_negative_scale_add_exists_resultentriesentryleft)))))) /\ (((((exists ff_h_pvs_add_exists_resultentriesentryleftpositive. ff_h_pvs_add_exists_resultentriesentryleftpositive + S (dst_positive_add_exists_resultentriesentryleft) = S ((S (sto_index_add_exists_resultentries)) * dst_positive_scale_add_exists_resultentriesentryleft)) /\ exists ff_q_pvs_add_exists_resultentriesentryleftpositive. dst_positive_code_add_exists_resultentriesentryleft = ff_q_pvs_add_exists_resultentriesentryleftpositive * S ((S (sto_index_add_exists_resultentries)) * dst_positive_scale_add_exists_resultentriesentryleft) + (dst_positive_add_exists_resultentriesentryleft))) /\ (((((exists ff_h_pvs_add_exists_resultentriesentryleftnegative. ff_h_pvs_add_exists_resultentriesentryleftnegative + S (dst_negative_add_exists_resultentriesentryleft) = S ((S (sto_index_add_exists_resultentries)) * dst_negative_scale_add_exists_resultentriesentryleft)) /\ exists ff_q_pvs_add_exists_resultentriesentryleftnegative. dst_negative_code_add_exists_resultentriesentryleft = ff_q_pvs_add_exists_resultentriesentryleftnegative * S ((S (sto_index_add_exists_resultentries)) * dst_negative_scale_add_exists_resultentriesentryleft) + (dst_negative_add_exists_resultentriesentryleft))) /\ (exists ge_balance_positive_add_exists_resultentriesentryleftvalue ge_balance_negative_add_exists_resultentriesentryleftvalue. (((((sto_left_add_exists_resultentries) = 2 * (ge_balance_positive_add_exists_resultentriesentryleftvalue) /\ (ge_balance_negative_add_exists_resultentriesentryleftvalue) = 0) \/ exists ge_signed_half_add_exists_resultentriesentryleftvaluedecode. (((sto_left_add_exists_resultentries) = 2 * ge_signed_half_add_exists_resultentriesentryleftvaluedecode + 1 /\ (ge_balance_positive_add_exists_resultentriesentryleftvalue) = 0) /\ (ge_balance_negative_add_exists_resultentriesentryleftvalue) = S ge_signed_half_add_exists_resultentriesentryleftvaluedecode))) /\ ((dst_positive_add_exists_resultentriesentryleft) + ge_balance_negative_add_exists_resultentriesentryleftvalue = (dst_negative_add_exists_resultentriesentryleft) + ge_balance_positive_add_exists_resultentriesentryleftvalue))))))))) /\ (((exists dst_positive_code_add_exists_resultentriesentryright dst_positive_scale_add_exists_resultentriesentryright dst_negative_code_add_exists_resultentriesentryright dst_negative_scale_add_exists_resultentriesentryright dst_positive_add_exists_resultentriesentryright dst_negative_add_exists_resultentriesentryright. (((G) = (((((dst_positive_code_add_exists_resultentriesentryright) + (dst_positive_scale_add_exists_resultentriesentryright)) * S ((dst_positive_code_add_exists_resultentriesentryright) + (dst_positive_scale_add_exists_resultentriesentryright)) + ((dst_positive_scale_add_exists_resultentriesentryright) + (dst_positive_scale_add_exists_resultentriesentryright))) + (((dst_negative_code_add_exists_resultentriesentryright) + (dst_negative_scale_add_exists_resultentriesentryright)) * S ((dst_negative_code_add_exists_resultentriesentryright) + (dst_negative_scale_add_exists_resultentriesentryright)) + ((dst_negative_scale_add_exists_resultentriesentryright) + (dst_negative_scale_add_exists_resultentriesentryright)))) * S ((((dst_positive_code_add_exists_resultentriesentryright) + (dst_positive_scale_add_exists_resultentriesentryright)) * S ((dst_positive_code_add_exists_resultentriesentryright) + (dst_positive_scale_add_exists_resultentriesentryright)) + ((dst_positive_scale_add_exists_resultentriesentryright) + (dst_positive_scale_add_exists_resultentriesentryright))) + (((dst_negative_code_add_exists_resultentriesentryright) + (dst_negative_scale_add_exists_resultentriesentryright)) * S ((dst_negative_code_add_exists_resultentriesentryright) + (dst_negative_scale_add_exists_resultentriesentryright)) + ((dst_negative_scale_add_exists_resultentriesentryright) + (dst_negative_scale_add_exists_resultentriesentryright)))) + ((((dst_negative_code_add_exists_resultentriesentryright) + (dst_negative_scale_add_exists_resultentriesentryright)) * S ((dst_negative_code_add_exists_resultentriesentryright) + (dst_negative_scale_add_exists_resultentriesentryright)) + ((dst_negative_scale_add_exists_resultentriesentryright) + (dst_negative_scale_add_exists_resultentriesentryright))) + (((dst_negative_code_add_exists_resultentriesentryright) + (dst_negative_scale_add_exists_resultentriesentryright)) * S ((dst_negative_code_add_exists_resultentriesentryright) + (dst_negative_scale_add_exists_resultentriesentryright)) + ((dst_negative_scale_add_exists_resultentriesentryright) + (dst_negative_scale_add_exists_resultentriesentryright)))))) /\ (((((exists ff_h_pvs_add_exists_resultentriesentryrightpositive. ff_h_pvs_add_exists_resultentriesentryrightpositive + S (dst_positive_add_exists_resultentriesentryright) = S ((S (sto_index_add_exists_resultentries)) * dst_positive_scale_add_exists_resultentriesentryright)) /\ exists ff_q_pvs_add_exists_resultentriesentryrightpositive. dst_positive_code_add_exists_resultentriesentryright = ff_q_pvs_add_exists_resultentriesentryrightpositive * S ((S (sto_index_add_exists_resultentries)) * dst_positive_scale_add_exists_resultentriesentryright) + (dst_positive_add_exists_resultentriesentryright))) /\ (((((exists ff_h_pvs_add_exists_resultentriesentryrightnegative. ff_h_pvs_add_exists_resultentriesentryrightnegative + S (dst_negative_add_exists_resultentriesentryright) = S ((S (sto_index_add_exists_resultentries)) * dst_negative_scale_add_exists_resultentriesentryright)) /\ exists ff_q_pvs_add_exists_resultentriesentryrightnegative. dst_negative_code_add_exists_resultentriesentryright = ff_q_pvs_add_exists_resultentriesentryrightnegative * S ((S (sto_index_add_exists_resultentries)) * dst_negative_scale_add_exists_resultentriesentryright) + (dst_negative_add_exists_resultentriesentryright))) /\ (exists ge_balance_positive_add_exists_resultentriesentryrightvalue ge_balance_negative_add_exists_resultentriesentryrightvalue. (((((sto_right_add_exists_resultentries) = 2 * (ge_balance_positive_add_exists_resultentriesentryrightvalue) /\ (ge_balance_negative_add_exists_resultentriesentryrightvalue) = 0) \/ exists ge_signed_half_add_exists_resultentriesentryrightvaluedecode. (((sto_right_add_exists_resultentries) = 2 * ge_signed_half_add_exists_resultentriesentryrightvaluedecode + 1 /\ (ge_balance_positive_add_exists_resultentriesentryrightvalue) = 0) /\ (ge_balance_negative_add_exists_resultentriesentryrightvalue) = S ge_signed_half_add_exists_resultentriesentryrightvaluedecode))) /\ ((dst_positive_add_exists_resultentriesentryright) + ge_balance_negative_add_exists_resultentriesentryrightvalue = (dst_negative_add_exists_resultentriesentryright) + ge_balance_positive_add_exists_resultentriesentryrightvalue))))))))) /\ (((exists dst_positive_code_add_exists_resultentriesentryoutput dst_positive_scale_add_exists_resultentriesentryoutput dst_negative_code_add_exists_resultentriesentryoutput dst_negative_scale_add_exists_resultentriesentryoutput dst_positive_add_exists_resultentriesentryoutput dst_negative_add_exists_resultentriesentryoutput. (((H) = (((((dst_positive_code_add_exists_resultentriesentryoutput) + (dst_positive_scale_add_exists_resultentriesentryoutput)) * S ((dst_positive_code_add_exists_resultentriesentryoutput) + (dst_positive_scale_add_exists_resultentriesentryoutput)) + ((dst_positive_scale_add_exists_resultentriesentryoutput) + (dst_positive_scale_add_exists_resultentriesentryoutput))) + (((dst_negative_code_add_exists_resultentriesentryoutput) + (dst_negative_scale_add_exists_resultentriesentryoutput)) * S ((dst_negative_code_add_exists_resultentriesentryoutput) + (dst_negative_scale_add_exists_resultentriesentryoutput)) + ((dst_negative_scale_add_exists_resultentriesentryoutput) + (dst_negative_scale_add_exists_resultentriesentryoutput)))) * S ((((dst_positive_code_add_exists_resultentriesentryoutput) + (dst_positive_scale_add_exists_resultentriesentryoutput)) * S ((dst_positive_code_add_exists_resultentriesentryoutput) + (dst_positive_scale_add_exists_resultentriesentryoutput)) + ((dst_positive_scale_add_exists_resultentriesentryoutput) + (dst_positive_scale_add_exists_resultentriesentryoutput))) + (((dst_negative_code_add_exists_resultentriesentryoutput) + (dst_negative_scale_add_exists_resultentriesentryoutput)) * S ((dst_negative_code_add_exists_resultentriesentryoutput) + (dst_negative_scale_add_exists_resultentriesentryoutput)) + ((dst_negative_scale_add_exists_resultentriesentryoutput) + (dst_negative_scale_add_exists_resultentriesentryoutput)))) + ((((dst_negative_code_add_exists_resultentriesentryoutput) + (dst_negative_scale_add_exists_resultentriesentryoutput)) * S ((dst_negative_code_add_exists_resultentriesentryoutput) + (dst_negative_scale_add_exists_resultentriesentryoutput)) + ((dst_negative_scale_add_exists_resultentriesentryoutput) + (dst_negative_scale_add_exists_resultentriesentryoutput))) + (((dst_negative_code_add_exists_resultentriesentryoutput) + (dst_negative_scale_add_exists_resultentriesentryoutput)) * S ((dst_negative_code_add_exists_resultentriesentryoutput) + (dst_negative_scale_add_exists_resultentriesentryoutput)) + ((dst_negative_scale_add_exists_resultentriesentryoutput) + (dst_negative_scale_add_exists_resultentriesentryoutput)))))) /\ (((((exists ff_h_pvs_add_exists_resultentriesentryoutputpositive. ff_h_pvs_add_exists_resultentriesentryoutputpositive + S (dst_positive_add_exists_resultentriesentryoutput) = S ((S (sto_index_add_exists_resultentries)) * dst_positive_scale_add_exists_resultentriesentryoutput)) /\ exists ff_q_pvs_add_exists_resultentriesentryoutputpositive. dst_positive_code_add_exists_resultentriesentryoutput = ff_q_pvs_add_exists_resultentriesentryoutputpositive * S ((S (sto_index_add_exists_resultentries)) * dst_positive_scale_add_exists_resultentriesentryoutput) + (dst_positive_add_exists_resultentriesentryoutput))) /\ (((((exists ff_h_pvs_add_exists_resultentriesentryoutputnegative. ff_h_pvs_add_exists_resultentriesentryoutputnegative + S (dst_negative_add_exists_resultentriesentryoutput) = S ((S (sto_index_add_exists_resultentries)) * dst_negative_scale_add_exists_resultentriesentryoutput)) /\ exists ff_q_pvs_add_exists_resultentriesentryoutputnegative. dst_negative_code_add_exists_resultentriesentryoutput = ff_q_pvs_add_exists_resultentriesentryoutputnegative * S ((S (sto_index_add_exists_resultentries)) * dst_negative_scale_add_exists_resultentriesentryoutput) + (dst_negative_add_exists_resultentriesentryoutput))) /\ (exists ge_balance_positive_add_exists_resultentriesentryoutputvalue ge_balance_negative_add_exists_resultentriesentryoutputvalue. (((((sto_output_add_exists_resultentries) = 2 * (ge_balance_positive_add_exists_resultentriesentryoutputvalue) /\ (ge_balance_negative_add_exists_resultentriesentryoutputvalue) = 0) \/ exists ge_signed_half_add_exists_resultentriesentryoutputvaluedecode. (((sto_output_add_exists_resultentries) = 2 * ge_signed_half_add_exists_resultentriesentryoutputvaluedecode + 1 /\ (ge_balance_positive_add_exists_resultentriesentryoutputvalue) = 0) /\ (ge_balance_negative_add_exists_resultentriesentryoutputvalue) = S ge_signed_half_add_exists_resultentriesentryoutputvaluedecode))) /\ ((dst_positive_add_exists_resultentriesentryoutput) + ge_balance_negative_add_exists_resultentriesentryoutputvalue = (dst_negative_add_exists_resultentriesentryoutput) + ge_balance_positive_add_exists_resultentriesentryoutputvalue))))))))) /\ (exists dsa_ap_add_exists_resultentriesentryoperation dsa_an_add_exists_resultentriesentryoperation dsa_bp_add_exists_resultentriesentryoperation dsa_bn_add_exists_resultentriesentryoperation dsa_cp_add_exists_resultentriesentryoperation dsa_cn_add_exists_resultentriesentryoperation. (((((sto_left_add_exists_resultentries) = 2 * (dsa_ap_add_exists_resultentriesentryoperation) /\ (dsa_an_add_exists_resultentriesentryoperation) = 0) \/ exists ge_signed_half_add_exists_resultentriesentryoperationleft. (((sto_left_add_exists_resultentries) = 2 * ge_signed_half_add_exists_resultentriesentryoperationleft + 1 /\ (dsa_ap_add_exists_resultentriesentryoperation) = 0) /\ (dsa_an_add_exists_resultentriesentryoperation) = S ge_signed_half_add_exists_resultentriesentryoperationleft))) /\ ((((((sto_right_add_exists_resultentries) = 2 * (dsa_bp_add_exists_resultentriesentryoperation) /\ (dsa_bn_add_exists_resultentriesentryoperation) = 0) \/ exists ge_signed_half_add_exists_resultentriesentryoperationright. (((sto_right_add_exists_resultentries) = 2 * ge_signed_half_add_exists_resultentriesentryoperationright + 1 /\ (dsa_bp_add_exists_resultentriesentryoperation) = 0) /\ (dsa_bn_add_exists_resultentriesentryoperation) = S ge_signed_half_add_exists_resultentriesentryoperationright))) /\ ((((((sto_output_add_exists_resultentries) = 2 * (dsa_cp_add_exists_resultentriesentryoperation) /\ (dsa_cn_add_exists_resultentriesentryoperation) = 0) \/ exists ge_signed_half_add_exists_resultentriesentryoperationoutput. (((sto_output_add_exists_resultentries) = 2 * ge_signed_half_add_exists_resultentriesentryoperationoutput + 1 /\ (dsa_cp_add_exists_resultentriesentryoperation) = 0) /\ (dsa_cn_add_exists_resultentriesentryoperation) = S ge_signed_half_add_exists_resultentriesentryoperationoutput))) /\ ((dsa_ap_add_exists_resultentriesentryoperation + dsa_bp_add_exists_resultentriesentryoperation) + dsa_cn_add_exists_resultentriesentryoperation = (dsa_an_add_exists_resultentriesentryoperation + dsa_bn_add_exists_resultentriesentryoperation) + dsa_cp_add_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 add emptysigned table domain resizesigned table lookup anysigned table add 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_add_empty (F)
  2. L8
    specialize signed_table_add_empty (G)
  3. L9
    specialize signed_table_add_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_add_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. ArithAdd(F,G,K,l)Definitions: ArithAdd(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 add total.

  1. L54
    have hv : ∃ z. SignedAdd(x1,x2,z)Definitions: SignedAdd(x1,x2,z)Original native command in the exact edition
  2. L55
    specialize signed_add_total (x1)
  3. L56
    specialize signed_add_total (x2)
  4. L57
    apply signed_add_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_add_extend (F)
  2. L74
    specialize signed_table_add_extend (G)
  3. L75
    specialize signed_table_add_extend (x)
  4. L76
    specialize signed_table_add_extend (x4)
  5. L77
    specialize signed_table_add_extend (l)
  6. L78
    specialize signed_table_add_extend (x1)
  7. L79
    specialize signed_table_add_extend (x2)
  8. L80
    specialize signed_table_add_extend (x3)
  9. L81
    apply signed_table_add_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_add_empty (F)
  8. 0008specialize signed_table_add_empty (G)
  9. 0009specialize signed_table_add_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_add_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. ArithAdd(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. SignedAdd(x1,x2,z)
  55. 0055specialize signed_add_total (x1)
  56. 0056specialize signed_add_total (x2)
  57. 0057apply signed_add_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_add_extend (F)
  74. 0074specialize signed_table_add_extend (G)
  75. 0075specialize signed_table_add_extend (x)
  76. 0076specialize signed_table_add_extend (x4)
  77. 0077specialize signed_table_add_extend (l)
  78. 0078specialize signed_table_add_extend (x1)
  79. 0079specialize signed_table_add_extend (x2)
  80. 0080specialize signed_table_add_extend (x3)
  81. 0081apply signed_table_add_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