WS0016

signed_table_scalar_exists

Ordinary finite induction constructs both beta output streams and their actual packed table for pointwise scalar; 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. ∀ a. ∀ F. ArithTable(l,F) → ∃ x. ArithScale(a,F,x,l)

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

Definition DAG

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

Actual proof prerequisites

signed_table_scalar_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_scalar_extend
Original expanded first-order statement 
forall l a F. (exists dst_positive_code_scalar_exists_input0 dst_positive_scale_scalar_exists_input0 dst_negative_code_scalar_exists_input0 dst_negative_scale_scalar_exists_input0. (((F) = (((((dst_positive_code_scalar_exists_input0) + (dst_positive_scale_scalar_exists_input0)) * S ((dst_positive_code_scalar_exists_input0) + (dst_positive_scale_scalar_exists_input0)) + ((dst_positive_scale_scalar_exists_input0) + (dst_positive_scale_scalar_exists_input0))) + (((dst_negative_code_scalar_exists_input0) + (dst_negative_scale_scalar_exists_input0)) * S ((dst_negative_code_scalar_exists_input0) + (dst_negative_scale_scalar_exists_input0)) + ((dst_negative_scale_scalar_exists_input0) + (dst_negative_scale_scalar_exists_input0)))) * S ((((dst_positive_code_scalar_exists_input0) + (dst_positive_scale_scalar_exists_input0)) * S ((dst_positive_code_scalar_exists_input0) + (dst_positive_scale_scalar_exists_input0)) + ((dst_positive_scale_scalar_exists_input0) + (dst_positive_scale_scalar_exists_input0))) + (((dst_negative_code_scalar_exists_input0) + (dst_negative_scale_scalar_exists_input0)) * S ((dst_negative_code_scalar_exists_input0) + (dst_negative_scale_scalar_exists_input0)) + ((dst_negative_scale_scalar_exists_input0) + (dst_negative_scale_scalar_exists_input0)))) + ((((dst_negative_code_scalar_exists_input0) + (dst_negative_scale_scalar_exists_input0)) * S ((dst_negative_code_scalar_exists_input0) + (dst_negative_scale_scalar_exists_input0)) + ((dst_negative_scale_scalar_exists_input0) + (dst_negative_scale_scalar_exists_input0))) + (((dst_negative_code_scalar_exists_input0) + (dst_negative_scale_scalar_exists_input0)) * S ((dst_negative_code_scalar_exists_input0) + (dst_negative_scale_scalar_exists_input0)) + ((dst_negative_scale_scalar_exists_input0) + (dst_negative_scale_scalar_exists_input0)))))) /\ (forall dst_index_scalar_exists_input0. (exists pvs_le_gap_scalar_exists_input0domain. pvs_le_gap_scalar_exists_input0domain + (dst_index_scalar_exists_input0) = (l)) -> exists dst_positive_scalar_exists_input0 dst_negative_scalar_exists_input0 dst_value_scalar_exists_input0. ((((exists ff_h_pvs_scalar_exists_input0entrypositive. ff_h_pvs_scalar_exists_input0entrypositive + S (dst_positive_scalar_exists_input0) = S ((S (dst_index_scalar_exists_input0)) * dst_positive_scale_scalar_exists_input0)) /\ exists ff_q_pvs_scalar_exists_input0entrypositive. dst_positive_code_scalar_exists_input0 = ff_q_pvs_scalar_exists_input0entrypositive * S ((S (dst_index_scalar_exists_input0)) * dst_positive_scale_scalar_exists_input0) + (dst_positive_scalar_exists_input0))) /\ (((((exists ff_h_pvs_scalar_exists_input0entrynegative. ff_h_pvs_scalar_exists_input0entrynegative + S (dst_negative_scalar_exists_input0) = S ((S (dst_index_scalar_exists_input0)) * dst_negative_scale_scalar_exists_input0)) /\ exists ff_q_pvs_scalar_exists_input0entrynegative. dst_negative_code_scalar_exists_input0 = ff_q_pvs_scalar_exists_input0entrynegative * S ((S (dst_index_scalar_exists_input0)) * dst_negative_scale_scalar_exists_input0) + (dst_negative_scalar_exists_input0))) /\ (exists ge_balance_positive_scalar_exists_input0entryvalue ge_balance_negative_scalar_exists_input0entryvalue. (((((dst_value_scalar_exists_input0) = 2 * (ge_balance_positive_scalar_exists_input0entryvalue) /\ (ge_balance_negative_scalar_exists_input0entryvalue) = 0) \/ exists ge_signed_half_scalar_exists_input0entryvaluedecode. (((dst_value_scalar_exists_input0) = 2 * ge_signed_half_scalar_exists_input0entryvaluedecode + 1 /\ (ge_balance_positive_scalar_exists_input0entryvalue) = 0) /\ (ge_balance_negative_scalar_exists_input0entryvalue) = S ge_signed_half_scalar_exists_input0entryvaluedecode))) /\ ((dst_positive_scalar_exists_input0) + ge_balance_negative_scalar_exists_input0entryvalue = (dst_negative_scalar_exists_input0) + ge_balance_positive_scalar_exists_input0entryvalue))))))))) -> exists G. (((exists dst_positive_code_scalar_exists_resultinput_table dst_positive_scale_scalar_exists_resultinput_table dst_negative_code_scalar_exists_resultinput_table dst_negative_scale_scalar_exists_resultinput_table. (((F) = (((((dst_positive_code_scalar_exists_resultinput_table) + (dst_positive_scale_scalar_exists_resultinput_table)) * S ((dst_positive_code_scalar_exists_resultinput_table) + (dst_positive_scale_scalar_exists_resultinput_table)) + ((dst_positive_scale_scalar_exists_resultinput_table) + (dst_positive_scale_scalar_exists_resultinput_table))) + (((dst_negative_code_scalar_exists_resultinput_table) + (dst_negative_scale_scalar_exists_resultinput_table)) * S ((dst_negative_code_scalar_exists_resultinput_table) + (dst_negative_scale_scalar_exists_resultinput_table)) + ((dst_negative_scale_scalar_exists_resultinput_table) + (dst_negative_scale_scalar_exists_resultinput_table)))) * S ((((dst_positive_code_scalar_exists_resultinput_table) + (dst_positive_scale_scalar_exists_resultinput_table)) * S ((dst_positive_code_scalar_exists_resultinput_table) + (dst_positive_scale_scalar_exists_resultinput_table)) + ((dst_positive_scale_scalar_exists_resultinput_table) + (dst_positive_scale_scalar_exists_resultinput_table))) + (((dst_negative_code_scalar_exists_resultinput_table) + (dst_negative_scale_scalar_exists_resultinput_table)) * S ((dst_negative_code_scalar_exists_resultinput_table) + (dst_negative_scale_scalar_exists_resultinput_table)) + ((dst_negative_scale_scalar_exists_resultinput_table) + (dst_negative_scale_scalar_exists_resultinput_table)))) + ((((dst_negative_code_scalar_exists_resultinput_table) + (dst_negative_scale_scalar_exists_resultinput_table)) * S ((dst_negative_code_scalar_exists_resultinput_table) + (dst_negative_scale_scalar_exists_resultinput_table)) + ((dst_negative_scale_scalar_exists_resultinput_table) + (dst_negative_scale_scalar_exists_resultinput_table))) + (((dst_negative_code_scalar_exists_resultinput_table) + (dst_negative_scale_scalar_exists_resultinput_table)) * S ((dst_negative_code_scalar_exists_resultinput_table) + (dst_negative_scale_scalar_exists_resultinput_table)) + ((dst_negative_scale_scalar_exists_resultinput_table) + (dst_negative_scale_scalar_exists_resultinput_table)))))) /\ (forall dst_index_scalar_exists_resultinput_table. (exists pvs_le_gap_scalar_exists_resultinput_tabledomain. pvs_le_gap_scalar_exists_resultinput_tabledomain + (dst_index_scalar_exists_resultinput_table) = (l)) -> exists dst_positive_scalar_exists_resultinput_table dst_negative_scalar_exists_resultinput_table dst_value_scalar_exists_resultinput_table. ((((exists ff_h_pvs_scalar_exists_resultinput_tableentrypositive. ff_h_pvs_scalar_exists_resultinput_tableentrypositive + S (dst_positive_scalar_exists_resultinput_table) = S ((S (dst_index_scalar_exists_resultinput_table)) * dst_positive_scale_scalar_exists_resultinput_table)) /\ exists ff_q_pvs_scalar_exists_resultinput_tableentrypositive. dst_positive_code_scalar_exists_resultinput_table = ff_q_pvs_scalar_exists_resultinput_tableentrypositive * S ((S (dst_index_scalar_exists_resultinput_table)) * dst_positive_scale_scalar_exists_resultinput_table) + (dst_positive_scalar_exists_resultinput_table))) /\ (((((exists ff_h_pvs_scalar_exists_resultinput_tableentrynegative. ff_h_pvs_scalar_exists_resultinput_tableentrynegative + S (dst_negative_scalar_exists_resultinput_table) = S ((S (dst_index_scalar_exists_resultinput_table)) * dst_negative_scale_scalar_exists_resultinput_table)) /\ exists ff_q_pvs_scalar_exists_resultinput_tableentrynegative. dst_negative_code_scalar_exists_resultinput_table = ff_q_pvs_scalar_exists_resultinput_tableentrynegative * S ((S (dst_index_scalar_exists_resultinput_table)) * dst_negative_scale_scalar_exists_resultinput_table) + (dst_negative_scalar_exists_resultinput_table))) /\ (exists ge_balance_positive_scalar_exists_resultinput_tableentryvalue ge_balance_negative_scalar_exists_resultinput_tableentryvalue. (((((dst_value_scalar_exists_resultinput_table) = 2 * (ge_balance_positive_scalar_exists_resultinput_tableentryvalue) /\ (ge_balance_negative_scalar_exists_resultinput_tableentryvalue) = 0) \/ exists ge_signed_half_scalar_exists_resultinput_tableentryvaluedecode. (((dst_value_scalar_exists_resultinput_table) = 2 * ge_signed_half_scalar_exists_resultinput_tableentryvaluedecode + 1 /\ (ge_balance_positive_scalar_exists_resultinput_tableentryvalue) = 0) /\ (ge_balance_negative_scalar_exists_resultinput_tableentryvalue) = S ge_signed_half_scalar_exists_resultinput_tableentryvaluedecode))) /\ ((dst_positive_scalar_exists_resultinput_table) + ge_balance_negative_scalar_exists_resultinput_tableentryvalue = (dst_negative_scalar_exists_resultinput_table) + ge_balance_positive_scalar_exists_resultinput_tableentryvalue))))))))) /\ (((exists dst_positive_code_scalar_exists_resultoutput_table dst_positive_scale_scalar_exists_resultoutput_table dst_negative_code_scalar_exists_resultoutput_table dst_negative_scale_scalar_exists_resultoutput_table. (((G) = (((((dst_positive_code_scalar_exists_resultoutput_table) + (dst_positive_scale_scalar_exists_resultoutput_table)) * S ((dst_positive_code_scalar_exists_resultoutput_table) + (dst_positive_scale_scalar_exists_resultoutput_table)) + ((dst_positive_scale_scalar_exists_resultoutput_table) + (dst_positive_scale_scalar_exists_resultoutput_table))) + (((dst_negative_code_scalar_exists_resultoutput_table) + (dst_negative_scale_scalar_exists_resultoutput_table)) * S ((dst_negative_code_scalar_exists_resultoutput_table) + (dst_negative_scale_scalar_exists_resultoutput_table)) + ((dst_negative_scale_scalar_exists_resultoutput_table) + (dst_negative_scale_scalar_exists_resultoutput_table)))) * S ((((dst_positive_code_scalar_exists_resultoutput_table) + (dst_positive_scale_scalar_exists_resultoutput_table)) * S ((dst_positive_code_scalar_exists_resultoutput_table) + (dst_positive_scale_scalar_exists_resultoutput_table)) + ((dst_positive_scale_scalar_exists_resultoutput_table) + (dst_positive_scale_scalar_exists_resultoutput_table))) + (((dst_negative_code_scalar_exists_resultoutput_table) + (dst_negative_scale_scalar_exists_resultoutput_table)) * S ((dst_negative_code_scalar_exists_resultoutput_table) + (dst_negative_scale_scalar_exists_resultoutput_table)) + ((dst_negative_scale_scalar_exists_resultoutput_table) + (dst_negative_scale_scalar_exists_resultoutput_table)))) + ((((dst_negative_code_scalar_exists_resultoutput_table) + (dst_negative_scale_scalar_exists_resultoutput_table)) * S ((dst_negative_code_scalar_exists_resultoutput_table) + (dst_negative_scale_scalar_exists_resultoutput_table)) + ((dst_negative_scale_scalar_exists_resultoutput_table) + (dst_negative_scale_scalar_exists_resultoutput_table))) + (((dst_negative_code_scalar_exists_resultoutput_table) + (dst_negative_scale_scalar_exists_resultoutput_table)) * S ((dst_negative_code_scalar_exists_resultoutput_table) + (dst_negative_scale_scalar_exists_resultoutput_table)) + ((dst_negative_scale_scalar_exists_resultoutput_table) + (dst_negative_scale_scalar_exists_resultoutput_table)))))) /\ (forall dst_index_scalar_exists_resultoutput_table. (exists pvs_le_gap_scalar_exists_resultoutput_tabledomain. pvs_le_gap_scalar_exists_resultoutput_tabledomain + (dst_index_scalar_exists_resultoutput_table) = (l)) -> exists dst_positive_scalar_exists_resultoutput_table dst_negative_scalar_exists_resultoutput_table dst_value_scalar_exists_resultoutput_table. ((((exists ff_h_pvs_scalar_exists_resultoutput_tableentrypositive. ff_h_pvs_scalar_exists_resultoutput_tableentrypositive + S (dst_positive_scalar_exists_resultoutput_table) = S ((S (dst_index_scalar_exists_resultoutput_table)) * dst_positive_scale_scalar_exists_resultoutput_table)) /\ exists ff_q_pvs_scalar_exists_resultoutput_tableentrypositive. dst_positive_code_scalar_exists_resultoutput_table = ff_q_pvs_scalar_exists_resultoutput_tableentrypositive * S ((S (dst_index_scalar_exists_resultoutput_table)) * dst_positive_scale_scalar_exists_resultoutput_table) + (dst_positive_scalar_exists_resultoutput_table))) /\ (((((exists ff_h_pvs_scalar_exists_resultoutput_tableentrynegative. ff_h_pvs_scalar_exists_resultoutput_tableentrynegative + S (dst_negative_scalar_exists_resultoutput_table) = S ((S (dst_index_scalar_exists_resultoutput_table)) * dst_negative_scale_scalar_exists_resultoutput_table)) /\ exists ff_q_pvs_scalar_exists_resultoutput_tableentrynegative. dst_negative_code_scalar_exists_resultoutput_table = ff_q_pvs_scalar_exists_resultoutput_tableentrynegative * S ((S (dst_index_scalar_exists_resultoutput_table)) * dst_negative_scale_scalar_exists_resultoutput_table) + (dst_negative_scalar_exists_resultoutput_table))) /\ (exists ge_balance_positive_scalar_exists_resultoutput_tableentryvalue ge_balance_negative_scalar_exists_resultoutput_tableentryvalue. (((((dst_value_scalar_exists_resultoutput_table) = 2 * (ge_balance_positive_scalar_exists_resultoutput_tableentryvalue) /\ (ge_balance_negative_scalar_exists_resultoutput_tableentryvalue) = 0) \/ exists ge_signed_half_scalar_exists_resultoutput_tableentryvaluedecode. (((dst_value_scalar_exists_resultoutput_table) = 2 * ge_signed_half_scalar_exists_resultoutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_scalar_exists_resultoutput_tableentryvalue) = 0) /\ (ge_balance_negative_scalar_exists_resultoutput_tableentryvalue) = S ge_signed_half_scalar_exists_resultoutput_tableentryvaluedecode))) /\ ((dst_positive_scalar_exists_resultoutput_table) + ge_balance_negative_scalar_exists_resultoutput_tableentryvalue = (dst_negative_scalar_exists_resultoutput_table) + ge_balance_positive_scalar_exists_resultoutput_tableentryvalue))))))))) /\ (forall sto_index_scalar_exists_resultentries. (exists pvs_gap_scalar_exists_resultentriesbound. pvs_gap_scalar_exists_resultentriesbound + S (sto_index_scalar_exists_resultentries) = (l)) -> exists sto_input_scalar_exists_resultentries sto_output_scalar_exists_resultentries. ((exists dst_positive_code_scalar_exists_resultentriesentryinput dst_positive_scale_scalar_exists_resultentriesentryinput dst_negative_code_scalar_exists_resultentriesentryinput dst_negative_scale_scalar_exists_resultentriesentryinput dst_positive_scalar_exists_resultentriesentryinput dst_negative_scalar_exists_resultentriesentryinput. (((F) = (((((dst_positive_code_scalar_exists_resultentriesentryinput) + (dst_positive_scale_scalar_exists_resultentriesentryinput)) * S ((dst_positive_code_scalar_exists_resultentriesentryinput) + (dst_positive_scale_scalar_exists_resultentriesentryinput)) + ((dst_positive_scale_scalar_exists_resultentriesentryinput) + (dst_positive_scale_scalar_exists_resultentriesentryinput))) + (((dst_negative_code_scalar_exists_resultentriesentryinput) + (dst_negative_scale_scalar_exists_resultentriesentryinput)) * S ((dst_negative_code_scalar_exists_resultentriesentryinput) + (dst_negative_scale_scalar_exists_resultentriesentryinput)) + ((dst_negative_scale_scalar_exists_resultentriesentryinput) + (dst_negative_scale_scalar_exists_resultentriesentryinput)))) * S ((((dst_positive_code_scalar_exists_resultentriesentryinput) + (dst_positive_scale_scalar_exists_resultentriesentryinput)) * S ((dst_positive_code_scalar_exists_resultentriesentryinput) + (dst_positive_scale_scalar_exists_resultentriesentryinput)) + ((dst_positive_scale_scalar_exists_resultentriesentryinput) + (dst_positive_scale_scalar_exists_resultentriesentryinput))) + (((dst_negative_code_scalar_exists_resultentriesentryinput) + (dst_negative_scale_scalar_exists_resultentriesentryinput)) * S ((dst_negative_code_scalar_exists_resultentriesentryinput) + (dst_negative_scale_scalar_exists_resultentriesentryinput)) + ((dst_negative_scale_scalar_exists_resultentriesentryinput) + (dst_negative_scale_scalar_exists_resultentriesentryinput)))) + ((((dst_negative_code_scalar_exists_resultentriesentryinput) + (dst_negative_scale_scalar_exists_resultentriesentryinput)) * S ((dst_negative_code_scalar_exists_resultentriesentryinput) + (dst_negative_scale_scalar_exists_resultentriesentryinput)) + ((dst_negative_scale_scalar_exists_resultentriesentryinput) + (dst_negative_scale_scalar_exists_resultentriesentryinput))) + (((dst_negative_code_scalar_exists_resultentriesentryinput) + (dst_negative_scale_scalar_exists_resultentriesentryinput)) * S ((dst_negative_code_scalar_exists_resultentriesentryinput) + (dst_negative_scale_scalar_exists_resultentriesentryinput)) + ((dst_negative_scale_scalar_exists_resultentriesentryinput) + (dst_negative_scale_scalar_exists_resultentriesentryinput)))))) /\ (((((exists ff_h_pvs_scalar_exists_resultentriesentryinputpositive. ff_h_pvs_scalar_exists_resultentriesentryinputpositive + S (dst_positive_scalar_exists_resultentriesentryinput) = S ((S (sto_index_scalar_exists_resultentries)) * dst_positive_scale_scalar_exists_resultentriesentryinput)) /\ exists ff_q_pvs_scalar_exists_resultentriesentryinputpositive. dst_positive_code_scalar_exists_resultentriesentryinput = ff_q_pvs_scalar_exists_resultentriesentryinputpositive * S ((S (sto_index_scalar_exists_resultentries)) * dst_positive_scale_scalar_exists_resultentriesentryinput) + (dst_positive_scalar_exists_resultentriesentryinput))) /\ (((((exists ff_h_pvs_scalar_exists_resultentriesentryinputnegative. ff_h_pvs_scalar_exists_resultentriesentryinputnegative + S (dst_negative_scalar_exists_resultentriesentryinput) = S ((S (sto_index_scalar_exists_resultentries)) * dst_negative_scale_scalar_exists_resultentriesentryinput)) /\ exists ff_q_pvs_scalar_exists_resultentriesentryinputnegative. dst_negative_code_scalar_exists_resultentriesentryinput = ff_q_pvs_scalar_exists_resultentriesentryinputnegative * S ((S (sto_index_scalar_exists_resultentries)) * dst_negative_scale_scalar_exists_resultentriesentryinput) + (dst_negative_scalar_exists_resultentriesentryinput))) /\ (exists ge_balance_positive_scalar_exists_resultentriesentryinputvalue ge_balance_negative_scalar_exists_resultentriesentryinputvalue. (((((sto_input_scalar_exists_resultentries) = 2 * (ge_balance_positive_scalar_exists_resultentriesentryinputvalue) /\ (ge_balance_negative_scalar_exists_resultentriesentryinputvalue) = 0) \/ exists ge_signed_half_scalar_exists_resultentriesentryinputvaluedecode. (((sto_input_scalar_exists_resultentries) = 2 * ge_signed_half_scalar_exists_resultentriesentryinputvaluedecode + 1 /\ (ge_balance_positive_scalar_exists_resultentriesentryinputvalue) = 0) /\ (ge_balance_negative_scalar_exists_resultentriesentryinputvalue) = S ge_signed_half_scalar_exists_resultentriesentryinputvaluedecode))) /\ ((dst_positive_scalar_exists_resultentriesentryinput) + ge_balance_negative_scalar_exists_resultentriesentryinputvalue = (dst_negative_scalar_exists_resultentriesentryinput) + ge_balance_positive_scalar_exists_resultentriesentryinputvalue))))))))) /\ (((exists dst_positive_code_scalar_exists_resultentriesentryoutput dst_positive_scale_scalar_exists_resultentriesentryoutput dst_negative_code_scalar_exists_resultentriesentryoutput dst_negative_scale_scalar_exists_resultentriesentryoutput dst_positive_scalar_exists_resultentriesentryoutput dst_negative_scalar_exists_resultentriesentryoutput. (((G) = (((((dst_positive_code_scalar_exists_resultentriesentryoutput) + (dst_positive_scale_scalar_exists_resultentriesentryoutput)) * S ((dst_positive_code_scalar_exists_resultentriesentryoutput) + (dst_positive_scale_scalar_exists_resultentriesentryoutput)) + ((dst_positive_scale_scalar_exists_resultentriesentryoutput) + (dst_positive_scale_scalar_exists_resultentriesentryoutput))) + (((dst_negative_code_scalar_exists_resultentriesentryoutput) + (dst_negative_scale_scalar_exists_resultentriesentryoutput)) * S ((dst_negative_code_scalar_exists_resultentriesentryoutput) + (dst_negative_scale_scalar_exists_resultentriesentryoutput)) + ((dst_negative_scale_scalar_exists_resultentriesentryoutput) + (dst_negative_scale_scalar_exists_resultentriesentryoutput)))) * S ((((dst_positive_code_scalar_exists_resultentriesentryoutput) + (dst_positive_scale_scalar_exists_resultentriesentryoutput)) * S ((dst_positive_code_scalar_exists_resultentriesentryoutput) + (dst_positive_scale_scalar_exists_resultentriesentryoutput)) + ((dst_positive_scale_scalar_exists_resultentriesentryoutput) + (dst_positive_scale_scalar_exists_resultentriesentryoutput))) + (((dst_negative_code_scalar_exists_resultentriesentryoutput) + (dst_negative_scale_scalar_exists_resultentriesentryoutput)) * S ((dst_negative_code_scalar_exists_resultentriesentryoutput) + (dst_negative_scale_scalar_exists_resultentriesentryoutput)) + ((dst_negative_scale_scalar_exists_resultentriesentryoutput) + (dst_negative_scale_scalar_exists_resultentriesentryoutput)))) + ((((dst_negative_code_scalar_exists_resultentriesentryoutput) + (dst_negative_scale_scalar_exists_resultentriesentryoutput)) * S ((dst_negative_code_scalar_exists_resultentriesentryoutput) + (dst_negative_scale_scalar_exists_resultentriesentryoutput)) + ((dst_negative_scale_scalar_exists_resultentriesentryoutput) + (dst_negative_scale_scalar_exists_resultentriesentryoutput))) + (((dst_negative_code_scalar_exists_resultentriesentryoutput) + (dst_negative_scale_scalar_exists_resultentriesentryoutput)) * S ((dst_negative_code_scalar_exists_resultentriesentryoutput) + (dst_negative_scale_scalar_exists_resultentriesentryoutput)) + ((dst_negative_scale_scalar_exists_resultentriesentryoutput) + (dst_negative_scale_scalar_exists_resultentriesentryoutput)))))) /\ (((((exists ff_h_pvs_scalar_exists_resultentriesentryoutputpositive. ff_h_pvs_scalar_exists_resultentriesentryoutputpositive + S (dst_positive_scalar_exists_resultentriesentryoutput) = S ((S (sto_index_scalar_exists_resultentries)) * dst_positive_scale_scalar_exists_resultentriesentryoutput)) /\ exists ff_q_pvs_scalar_exists_resultentriesentryoutputpositive. dst_positive_code_scalar_exists_resultentriesentryoutput = ff_q_pvs_scalar_exists_resultentriesentryoutputpositive * S ((S (sto_index_scalar_exists_resultentries)) * dst_positive_scale_scalar_exists_resultentriesentryoutput) + (dst_positive_scalar_exists_resultentriesentryoutput))) /\ (((((exists ff_h_pvs_scalar_exists_resultentriesentryoutputnegative. ff_h_pvs_scalar_exists_resultentriesentryoutputnegative + S (dst_negative_scalar_exists_resultentriesentryoutput) = S ((S (sto_index_scalar_exists_resultentries)) * dst_negative_scale_scalar_exists_resultentriesentryoutput)) /\ exists ff_q_pvs_scalar_exists_resultentriesentryoutputnegative. dst_negative_code_scalar_exists_resultentriesentryoutput = ff_q_pvs_scalar_exists_resultentriesentryoutputnegative * S ((S (sto_index_scalar_exists_resultentries)) * dst_negative_scale_scalar_exists_resultentriesentryoutput) + (dst_negative_scalar_exists_resultentriesentryoutput))) /\ (exists ge_balance_positive_scalar_exists_resultentriesentryoutputvalue ge_balance_negative_scalar_exists_resultentriesentryoutputvalue. (((((sto_output_scalar_exists_resultentries) = 2 * (ge_balance_positive_scalar_exists_resultentriesentryoutputvalue) /\ (ge_balance_negative_scalar_exists_resultentriesentryoutputvalue) = 0) \/ exists ge_signed_half_scalar_exists_resultentriesentryoutputvaluedecode. (((sto_output_scalar_exists_resultentries) = 2 * ge_signed_half_scalar_exists_resultentriesentryoutputvaluedecode + 1 /\ (ge_balance_positive_scalar_exists_resultentriesentryoutputvalue) = 0) /\ (ge_balance_negative_scalar_exists_resultentriesentryoutputvalue) = S ge_signed_half_scalar_exists_resultentriesentryoutputvaluedecode))) /\ ((dst_positive_scalar_exists_resultentriesentryoutput) + ge_balance_negative_scalar_exists_resultentriesentryoutputvalue = (dst_negative_scalar_exists_resultentriesentryoutput) + ge_balance_positive_scalar_exists_resultentriesentryoutputvalue))))))))) /\ (exists sto_ap_scalar_exists_resultentriesentryoperation sto_an_scalar_exists_resultentriesentryoperation sto_bp_scalar_exists_resultentriesentryoperation sto_bn_scalar_exists_resultentriesentryoperation sto_cp_scalar_exists_resultentriesentryoperation sto_cn_scalar_exists_resultentriesentryoperation. (((((a) = 2 * (sto_ap_scalar_exists_resultentriesentryoperation) /\ (sto_an_scalar_exists_resultentriesentryoperation) = 0) \/ exists ge_signed_half_scalar_exists_resultentriesentryoperationleft. (((a) = 2 * ge_signed_half_scalar_exists_resultentriesentryoperationleft + 1 /\ (sto_ap_scalar_exists_resultentriesentryoperation) = 0) /\ (sto_an_scalar_exists_resultentriesentryoperation) = S ge_signed_half_scalar_exists_resultentriesentryoperationleft))) /\ ((((((sto_input_scalar_exists_resultentries) = 2 * (sto_bp_scalar_exists_resultentriesentryoperation) /\ (sto_bn_scalar_exists_resultentriesentryoperation) = 0) \/ exists ge_signed_half_scalar_exists_resultentriesentryoperationright. (((sto_input_scalar_exists_resultentries) = 2 * ge_signed_half_scalar_exists_resultentriesentryoperationright + 1 /\ (sto_bp_scalar_exists_resultentriesentryoperation) = 0) /\ (sto_bn_scalar_exists_resultentriesentryoperation) = S ge_signed_half_scalar_exists_resultentriesentryoperationright))) /\ ((((((sto_output_scalar_exists_resultentries) = 2 * (sto_cp_scalar_exists_resultentriesentryoperation) /\ (sto_cn_scalar_exists_resultentriesentryoperation) = 0) \/ exists ge_signed_half_scalar_exists_resultentriesentryoperationoutput. (((sto_output_scalar_exists_resultentries) = 2 * ge_signed_half_scalar_exists_resultentriesentryoperationoutput + 1 /\ (sto_cp_scalar_exists_resultentriesentryoperation) = 0) /\ (sto_cn_scalar_exists_resultentriesentryoperation) = S ge_signed_half_scalar_exists_resultentriesentryoperationoutput))) /\ ((sto_ap_scalar_exists_resultentriesentryoperation * sto_bp_scalar_exists_resultentriesentryoperation + sto_an_scalar_exists_resultentriesentryoperation * sto_bn_scalar_exists_resultentriesentryoperation) + sto_cn_scalar_exists_resultentriesentryoperation = (sto_ap_scalar_exists_resultentriesentryoperation * sto_bn_scalar_exists_resultentriesentryoperation + sto_an_scalar_exists_resultentriesentryoperation * sto_bp_scalar_exists_resultentriesentryoperation) + sto_cp_scalar_exists_resultentriesentryoperation)))))))))))))))

Complete tactic proof in conservative notation

All 70 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

70 script commands · 19 reading checkpoints · 4 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 scalar emptysigned table domain resizesigned table lookup anysigned table scalar extend
01Induction on lL1–4

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 a
  3. L3
    intro F
  4. L4
    intro ht0
02Construct an explicit witnessL5–5

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

  1. L5
    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 factsL6–15

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

  1. L6
    specialize signed_table_scalar_empty (a)
  2. L7
    specialize signed_table_scalar_empty (F)
  3. L8
    specialize signed_table_scalar_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. L9
    apply signed_table_scalar_empty
  5. L10
    exact ht0
  6. L11
    specialize divisor_signed_table_from_components (0)
  7. L12
    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)))))
  8. L13
    specialize divisor_signed_table_from_components (0)
  9. L14
    specialize divisor_signed_table_from_components (0)
  10. L15
    specialize divisor_signed_table_from_components (0)
04Use earlier factsL16–17

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

  1. L16
    specialize divisor_signed_table_from_components (0)
  2. L17
    apply divisor_signed_table_from_components
05Calculate and transport equalitiesL18–18

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

  1. L18
    refl
06Fix variables and assumptionsL19–21

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

  1. L19
    intro a
  2. L20
    intro F
  3. L21
    intro ht0
07Establish hpL22–30

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

  1. L22
    have hp : ∃ K. ArithScale(a,F,K,l)Definitions: ArithScale(a,F,K,l)Original native command in the exact edition
  2. L23
    specialize IH (a)
  3. L24
    specialize IH (F)
  4. L25
    apply IH
  5. L26
    specialize signed_table_domain_resize (S l)
  6. L27
    specialize signed_table_domain_resize (l)
  7. L28
    specialize signed_table_domain_resize (F)
  8. L29
    apply signed_table_domain_resize
  9. L30
    exact ht0
08Separate the logical casesL31–31

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

  1. L31
    cases hp
09Establish he0L32–37

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

  1. L32
    have he0 : ∃ z. ArithAt(F,l,z)Definitions: ArithAt(F,l,z)Original native command in the exact edition
  2. L33
    specialize signed_table_lookup_any (S l)
  3. L34
    specialize signed_table_lookup_any (F)
  4. L35
    specialize signed_table_lookup_any (l)
  5. L36
    apply signed_table_lookup_any
  6. L37
    exact ht0
10Separate the logical casesL38–38

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

  1. L38
    cases he0
11Establish hvL39–42

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

  1. L39
    have hv : ∃ z. SignedMul(a,x1,z)Definitions: SignedMul(a,x1,z)Original native command in the exact edition
  2. L40
    specialize signed_mul_total (a)
  3. L41
    specialize signed_mul_total (x1)
  4. L42
    apply signed_mul_total
12Separate the logical casesL43–43

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

  1. L43
    cases hv
13Establish hnextL44–49

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

  1. L44
    have hnext : ∃ K. ArithExtend(x,K,l,x2)Definitions: ArithExtend(x,K,l,x2)Original native command in the exact edition
  2. L45
    specialize arithmetic_signed_table_extend_at (l)
  3. L46
    specialize arithmetic_signed_table_extend_at (x)
  4. L47
    specialize arithmetic_signed_table_extend_at (l)
  5. L48
    specialize arithmetic_signed_table_extend_at (x2)
  6. L49
    apply arithmetic_signed_table_extend_at
14Separate the logical casesL50–51

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

  1. L50
    cases hp_witness
  2. L51
    cases hp_witness_right
15Use earlier factsL52–52

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

  1. L52
    exact hp_witness_right_left
16Separate the logical casesL53–55

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

  1. L53
    cases hnext
  2. L54
    cases hnext_witness
  3. L55
    cases hnext_witness_right
17Construct an explicit witnessL56–56

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

  1. L56
    exists x3
18Use earlier factsL57–66

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

  1. L57
    specialize signed_table_scalar_extend (a)
  2. L58
    specialize signed_table_scalar_extend (F)
  3. L59
    specialize signed_table_scalar_extend (x)
  4. L60
    specialize signed_table_scalar_extend (x3)
  5. L61
    specialize signed_table_scalar_extend (l)
  6. L62
    specialize signed_table_scalar_extend (x1)
  7. L63
    specialize signed_table_scalar_extend (x2)
  8. L64
    apply signed_table_scalar_extend
  9. L65
    exact hp_witness
  10. L66
    exact hnext_witness_left
19Use earlier factsL67–70

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

  1. L67
    exact hnext_witness_right_left
  2. L68
    exact he0_witness
  3. L69
    exact hnext_witness_right_right
  4. L70
    exact hv_witness

Library-wide reading audit

Original defined command ledger · 70 lines
  1. 0001induction l
  2. 0002intro a
  3. 0003intro F
  4. 0004intro ht0
  5. 0005exists ((((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))))
  6. 0006specialize signed_table_scalar_empty (a)
  7. 0007specialize signed_table_scalar_empty (F)
  8. 0008specialize signed_table_scalar_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)))))
  9. 0009apply signed_table_scalar_empty
  10. 0010exact ht0
  11. 0011specialize divisor_signed_table_from_components (0)
  12. 0012specialize 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)))))
  13. 0013specialize divisor_signed_table_from_components (0)
  14. 0014specialize divisor_signed_table_from_components (0)
  15. 0015specialize divisor_signed_table_from_components (0)
  16. 0016specialize divisor_signed_table_from_components (0)
  17. 0017apply divisor_signed_table_from_components
  18. 0018refl
  19. 0019intro a
  20. 0020intro F
  21. 0021intro ht0
  22. 0022have hp : ∃ K. ArithScale(a,F,K,l)
  23. 0023specialize IH (a)
  24. 0024specialize IH (F)
  25. 0025apply IH
  26. 0026specialize signed_table_domain_resize (S l)
  27. 0027specialize signed_table_domain_resize (l)
  28. 0028specialize signed_table_domain_resize (F)
  29. 0029apply signed_table_domain_resize
  30. 0030exact ht0
  31. 0031cases hp
  32. 0032have he0 : ∃ z. ArithAt(F,l,z)
  33. 0033specialize signed_table_lookup_any (S l)
  34. 0034specialize signed_table_lookup_any (F)
  35. 0035specialize signed_table_lookup_any (l)
  36. 0036apply signed_table_lookup_any
  37. 0037exact ht0
  38. 0038cases he0
  39. 0039have hv : ∃ z. SignedMul(a,x1,z)
  40. 0040specialize signed_mul_total (a)
  41. 0041specialize signed_mul_total (x1)
  42. 0042apply signed_mul_total
  43. 0043cases hv
  44. 0044have hnext : ∃ K. ArithExtend(x,K,l,x2)
  45. 0045specialize arithmetic_signed_table_extend_at (l)
  46. 0046specialize arithmetic_signed_table_extend_at (x)
  47. 0047specialize arithmetic_signed_table_extend_at (l)
  48. 0048specialize arithmetic_signed_table_extend_at (x2)
  49. 0049apply arithmetic_signed_table_extend_at
  50. 0050cases hp_witness
  51. 0051cases hp_witness_right
  52. 0052exact hp_witness_right_left
  53. 0053cases hnext
  54. 0054cases hnext_witness
  55. 0055cases hnext_witness_right
  56. 0056exists x3
  57. 0057specialize signed_table_scalar_extend (a)
  58. 0058specialize signed_table_scalar_extend (F)
  59. 0059specialize signed_table_scalar_extend (x)
  60. 0060specialize signed_table_scalar_extend (x3)
  61. 0061specialize signed_table_scalar_extend (l)
  62. 0062specialize signed_table_scalar_extend (x1)
  63. 0063specialize signed_table_scalar_extend (x2)
  64. 0064apply signed_table_scalar_extend
  65. 0065exact hp_witness
  66. 0066exact hnext_witness_left
  67. 0067exact hnext_witness_right_left
  68. 0068exact he0_witness
  69. 0069exact hnext_witness_right_right
  70. 0070exact hv_witness