RS0001

signed_rectangular_slice_lookup

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

Every actual slice lookup is the identical canonical signed value at its explicitly computed source index.

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

Exact expanded first-order arithmetic statement

forall F G o s l i z. (((exists dst_positive_code_lookup_slicesource_table dst_positive_scale_lookup_slicesource_table dst_negative_code_lookup_slicesource_table dst_negative_scale_lookup_slicesource_table. (((F) = (((((dst_positive_code_lookup_slicesource_table) + (dst_positive_scale_lookup_slicesource_table)) * S ((dst_positive_code_lookup_slicesource_table) + (dst_positive_scale_lookup_slicesource_table)) + ((dst_positive_scale_lookup_slicesource_table) + (dst_positive_scale_lookup_slicesource_table))) + (((dst_negative_code_lookup_slicesource_table) + (dst_negative_scale_lookup_slicesource_table)) * S ((dst_negative_code_lookup_slicesource_table) + (dst_negative_scale_lookup_slicesource_table)) + ((dst_negative_scale_lookup_slicesource_table) + (dst_negative_scale_lookup_slicesource_table)))) * S ((((dst_positive_code_lookup_slicesource_table) + (dst_positive_scale_lookup_slicesource_table)) * S ((dst_positive_code_lookup_slicesource_table) + (dst_positive_scale_lookup_slicesource_table)) + ((dst_positive_scale_lookup_slicesource_table) + (dst_positive_scale_lookup_slicesource_table))) + (((dst_negative_code_lookup_slicesource_table) + (dst_negative_scale_lookup_slicesource_table)) * S ((dst_negative_code_lookup_slicesource_table) + (dst_negative_scale_lookup_slicesource_table)) + ((dst_negative_scale_lookup_slicesource_table) + (dst_negative_scale_lookup_slicesource_table)))) + ((((dst_negative_code_lookup_slicesource_table) + (dst_negative_scale_lookup_slicesource_table)) * S ((dst_negative_code_lookup_slicesource_table) + (dst_negative_scale_lookup_slicesource_table)) + ((dst_negative_scale_lookup_slicesource_table) + (dst_negative_scale_lookup_slicesource_table))) + (((dst_negative_code_lookup_slicesource_table) + (dst_negative_scale_lookup_slicesource_table)) * S ((dst_negative_code_lookup_slicesource_table) + (dst_negative_scale_lookup_slicesource_table)) + ((dst_negative_scale_lookup_slicesource_table) + (dst_negative_scale_lookup_slicesource_table)))))) /\ (forall dst_index_lookup_slicesource_table. (exists pvs_le_gap_lookup_slicesource_tabledomain. pvs_le_gap_lookup_slicesource_tabledomain + (dst_index_lookup_slicesource_table) = (0)) -> exists dst_positive_lookup_slicesource_table dst_negative_lookup_slicesource_table dst_value_lookup_slicesource_table. ((((exists ff_h_pvs_lookup_slicesource_tableentrypositive. ff_h_pvs_lookup_slicesource_tableentrypositive + S (dst_positive_lookup_slicesource_table) = S ((S (dst_index_lookup_slicesource_table)) * dst_positive_scale_lookup_slicesource_table)) /\ exists ff_q_pvs_lookup_slicesource_tableentrypositive. dst_positive_code_lookup_slicesource_table = ff_q_pvs_lookup_slicesource_tableentrypositive * S ((S (dst_index_lookup_slicesource_table)) * dst_positive_scale_lookup_slicesource_table) + (dst_positive_lookup_slicesource_table))) /\ (((((exists ff_h_pvs_lookup_slicesource_tableentrynegative. ff_h_pvs_lookup_slicesource_tableentrynegative + S (dst_negative_lookup_slicesource_table) = S ((S (dst_index_lookup_slicesource_table)) * dst_negative_scale_lookup_slicesource_table)) /\ exists ff_q_pvs_lookup_slicesource_tableentrynegative. dst_negative_code_lookup_slicesource_table = ff_q_pvs_lookup_slicesource_tableentrynegative * S ((S (dst_index_lookup_slicesource_table)) * dst_negative_scale_lookup_slicesource_table) + (dst_negative_lookup_slicesource_table))) /\ (exists ge_balance_positive_lookup_slicesource_tableentryvalue ge_balance_negative_lookup_slicesource_tableentryvalue. (((((dst_value_lookup_slicesource_table) = 2 * (ge_balance_positive_lookup_slicesource_tableentryvalue) /\ (ge_balance_negative_lookup_slicesource_tableentryvalue) = 0) \/ exists ge_signed_half_lookup_slicesource_tableentryvaluedecode. (((dst_value_lookup_slicesource_table) = 2 * ge_signed_half_lookup_slicesource_tableentryvaluedecode + 1 /\ (ge_balance_positive_lookup_slicesource_tableentryvalue) = 0) /\ (ge_balance_negative_lookup_slicesource_tableentryvalue) = S ge_signed_half_lookup_slicesource_tableentryvaluedecode))) /\ ((dst_positive_lookup_slicesource_table) + ge_balance_negative_lookup_slicesource_tableentryvalue = (dst_negative_lookup_slicesource_table) + ge_balance_positive_lookup_slicesource_tableentryvalue))))))))) /\ (((exists dst_positive_code_lookup_sliceoutput_table dst_positive_scale_lookup_sliceoutput_table dst_negative_code_lookup_sliceoutput_table dst_negative_scale_lookup_sliceoutput_table. (((G) = (((((dst_positive_code_lookup_sliceoutput_table) + (dst_positive_scale_lookup_sliceoutput_table)) * S ((dst_positive_code_lookup_sliceoutput_table) + (dst_positive_scale_lookup_sliceoutput_table)) + ((dst_positive_scale_lookup_sliceoutput_table) + (dst_positive_scale_lookup_sliceoutput_table))) + (((dst_negative_code_lookup_sliceoutput_table) + (dst_negative_scale_lookup_sliceoutput_table)) * S ((dst_negative_code_lookup_sliceoutput_table) + (dst_negative_scale_lookup_sliceoutput_table)) + ((dst_negative_scale_lookup_sliceoutput_table) + (dst_negative_scale_lookup_sliceoutput_table)))) * S ((((dst_positive_code_lookup_sliceoutput_table) + (dst_positive_scale_lookup_sliceoutput_table)) * S ((dst_positive_code_lookup_sliceoutput_table) + (dst_positive_scale_lookup_sliceoutput_table)) + ((dst_positive_scale_lookup_sliceoutput_table) + (dst_positive_scale_lookup_sliceoutput_table))) + (((dst_negative_code_lookup_sliceoutput_table) + (dst_negative_scale_lookup_sliceoutput_table)) * S ((dst_negative_code_lookup_sliceoutput_table) + (dst_negative_scale_lookup_sliceoutput_table)) + ((dst_negative_scale_lookup_sliceoutput_table) + (dst_negative_scale_lookup_sliceoutput_table)))) + ((((dst_negative_code_lookup_sliceoutput_table) + (dst_negative_scale_lookup_sliceoutput_table)) * S ((dst_negative_code_lookup_sliceoutput_table) + (dst_negative_scale_lookup_sliceoutput_table)) + ((dst_negative_scale_lookup_sliceoutput_table) + (dst_negative_scale_lookup_sliceoutput_table))) + (((dst_negative_code_lookup_sliceoutput_table) + (dst_negative_scale_lookup_sliceoutput_table)) * S ((dst_negative_code_lookup_sliceoutput_table) + (dst_negative_scale_lookup_sliceoutput_table)) + ((dst_negative_scale_lookup_sliceoutput_table) + (dst_negative_scale_lookup_sliceoutput_table)))))) /\ (forall dst_index_lookup_sliceoutput_table. (exists pvs_le_gap_lookup_sliceoutput_tabledomain. pvs_le_gap_lookup_sliceoutput_tabledomain + (dst_index_lookup_sliceoutput_table) = (l)) -> exists dst_positive_lookup_sliceoutput_table dst_negative_lookup_sliceoutput_table dst_value_lookup_sliceoutput_table. ((((exists ff_h_pvs_lookup_sliceoutput_tableentrypositive. ff_h_pvs_lookup_sliceoutput_tableentrypositive + S (dst_positive_lookup_sliceoutput_table) = S ((S (dst_index_lookup_sliceoutput_table)) * dst_positive_scale_lookup_sliceoutput_table)) /\ exists ff_q_pvs_lookup_sliceoutput_tableentrypositive. dst_positive_code_lookup_sliceoutput_table = ff_q_pvs_lookup_sliceoutput_tableentrypositive * S ((S (dst_index_lookup_sliceoutput_table)) * dst_positive_scale_lookup_sliceoutput_table) + (dst_positive_lookup_sliceoutput_table))) /\ (((((exists ff_h_pvs_lookup_sliceoutput_tableentrynegative. ff_h_pvs_lookup_sliceoutput_tableentrynegative + S (dst_negative_lookup_sliceoutput_table) = S ((S (dst_index_lookup_sliceoutput_table)) * dst_negative_scale_lookup_sliceoutput_table)) /\ exists ff_q_pvs_lookup_sliceoutput_tableentrynegative. dst_negative_code_lookup_sliceoutput_table = ff_q_pvs_lookup_sliceoutput_tableentrynegative * S ((S (dst_index_lookup_sliceoutput_table)) * dst_negative_scale_lookup_sliceoutput_table) + (dst_negative_lookup_sliceoutput_table))) /\ (exists ge_balance_positive_lookup_sliceoutput_tableentryvalue ge_balance_negative_lookup_sliceoutput_tableentryvalue. (((((dst_value_lookup_sliceoutput_table) = 2 * (ge_balance_positive_lookup_sliceoutput_tableentryvalue) /\ (ge_balance_negative_lookup_sliceoutput_tableentryvalue) = 0) \/ exists ge_signed_half_lookup_sliceoutput_tableentryvaluedecode. (((dst_value_lookup_sliceoutput_table) = 2 * ge_signed_half_lookup_sliceoutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_lookup_sliceoutput_tableentryvalue) = 0) /\ (ge_balance_negative_lookup_sliceoutput_tableentryvalue) = S ge_signed_half_lookup_sliceoutput_tableentryvaluedecode))) /\ ((dst_positive_lookup_sliceoutput_table) + ge_balance_negative_lookup_sliceoutput_tableentryvalue = (dst_negative_lookup_sliceoutput_table) + ge_balance_positive_lookup_sliceoutput_tableentryvalue))))))))) /\ (forall srs_index_lookup_slice. (exists pvs_gap_lookup_slicebound. pvs_gap_lookup_slicebound + S (srs_index_lookup_slice) = (l)) -> exists srs_value_lookup_slice. (((exists dst_positive_code_lookup_sliceentrysource dst_positive_scale_lookup_sliceentrysource dst_negative_code_lookup_sliceentrysource dst_negative_scale_lookup_sliceentrysource dst_positive_lookup_sliceentrysource dst_negative_lookup_sliceentrysource. (((F) = (((((dst_positive_code_lookup_sliceentrysource) + (dst_positive_scale_lookup_sliceentrysource)) * S ((dst_positive_code_lookup_sliceentrysource) + (dst_positive_scale_lookup_sliceentrysource)) + ((dst_positive_scale_lookup_sliceentrysource) + (dst_positive_scale_lookup_sliceentrysource))) + (((dst_negative_code_lookup_sliceentrysource) + (dst_negative_scale_lookup_sliceentrysource)) * S ((dst_negative_code_lookup_sliceentrysource) + (dst_negative_scale_lookup_sliceentrysource)) + ((dst_negative_scale_lookup_sliceentrysource) + (dst_negative_scale_lookup_sliceentrysource)))) * S ((((dst_positive_code_lookup_sliceentrysource) + (dst_positive_scale_lookup_sliceentrysource)) * S ((dst_positive_code_lookup_sliceentrysource) + (dst_positive_scale_lookup_sliceentrysource)) + ((dst_positive_scale_lookup_sliceentrysource) + (dst_positive_scale_lookup_sliceentrysource))) + (((dst_negative_code_lookup_sliceentrysource) + (dst_negative_scale_lookup_sliceentrysource)) * S ((dst_negative_code_lookup_sliceentrysource) + (dst_negative_scale_lookup_sliceentrysource)) + ((dst_negative_scale_lookup_sliceentrysource) + (dst_negative_scale_lookup_sliceentrysource)))) + ((((dst_negative_code_lookup_sliceentrysource) + (dst_negative_scale_lookup_sliceentrysource)) * S ((dst_negative_code_lookup_sliceentrysource) + (dst_negative_scale_lookup_sliceentrysource)) + ((dst_negative_scale_lookup_sliceentrysource) + (dst_negative_scale_lookup_sliceentrysource))) + (((dst_negative_code_lookup_sliceentrysource) + (dst_negative_scale_lookup_sliceentrysource)) * S ((dst_negative_code_lookup_sliceentrysource) + (dst_negative_scale_lookup_sliceentrysource)) + ((dst_negative_scale_lookup_sliceentrysource) + (dst_negative_scale_lookup_sliceentrysource)))))) /\ (((((exists ff_h_pvs_lookup_sliceentrysourcepositive. ff_h_pvs_lookup_sliceentrysourcepositive + S (dst_positive_lookup_sliceentrysource) = S ((S (((o) + ((s) * (srs_index_lookup_slice))))) * dst_positive_scale_lookup_sliceentrysource)) /\ exists ff_q_pvs_lookup_sliceentrysourcepositive. dst_positive_code_lookup_sliceentrysource = ff_q_pvs_lookup_sliceentrysourcepositive * S ((S (((o) + ((s) * (srs_index_lookup_slice))))) * dst_positive_scale_lookup_sliceentrysource) + (dst_positive_lookup_sliceentrysource))) /\ (((((exists ff_h_pvs_lookup_sliceentrysourcenegative. ff_h_pvs_lookup_sliceentrysourcenegative + S (dst_negative_lookup_sliceentrysource) = S ((S (((o) + ((s) * (srs_index_lookup_slice))))) * dst_negative_scale_lookup_sliceentrysource)) /\ exists ff_q_pvs_lookup_sliceentrysourcenegative. dst_negative_code_lookup_sliceentrysource = ff_q_pvs_lookup_sliceentrysourcenegative * S ((S (((o) + ((s) * (srs_index_lookup_slice))))) * dst_negative_scale_lookup_sliceentrysource) + (dst_negative_lookup_sliceentrysource))) /\ (exists ge_balance_positive_lookup_sliceentrysourcevalue ge_balance_negative_lookup_sliceentrysourcevalue. (((((srs_value_lookup_slice) = 2 * (ge_balance_positive_lookup_sliceentrysourcevalue) /\ (ge_balance_negative_lookup_sliceentrysourcevalue) = 0) \/ exists ge_signed_half_lookup_sliceentrysourcevaluedecode. (((srs_value_lookup_slice) = 2 * ge_signed_half_lookup_sliceentrysourcevaluedecode + 1 /\ (ge_balance_positive_lookup_sliceentrysourcevalue) = 0) /\ (ge_balance_negative_lookup_sliceentrysourcevalue) = S ge_signed_half_lookup_sliceentrysourcevaluedecode))) /\ ((dst_positive_lookup_sliceentrysource) + ge_balance_negative_lookup_sliceentrysourcevalue = (dst_negative_lookup_sliceentrysource) + ge_balance_positive_lookup_sliceentrysourcevalue))))))))) /\ (exists dst_positive_code_lookup_sliceentryoutput dst_positive_scale_lookup_sliceentryoutput dst_negative_code_lookup_sliceentryoutput dst_negative_scale_lookup_sliceentryoutput dst_positive_lookup_sliceentryoutput dst_negative_lookup_sliceentryoutput. (((G) = (((((dst_positive_code_lookup_sliceentryoutput) + (dst_positive_scale_lookup_sliceentryoutput)) * S ((dst_positive_code_lookup_sliceentryoutput) + (dst_positive_scale_lookup_sliceentryoutput)) + ((dst_positive_scale_lookup_sliceentryoutput) + (dst_positive_scale_lookup_sliceentryoutput))) + (((dst_negative_code_lookup_sliceentryoutput) + (dst_negative_scale_lookup_sliceentryoutput)) * S ((dst_negative_code_lookup_sliceentryoutput) + (dst_negative_scale_lookup_sliceentryoutput)) + ((dst_negative_scale_lookup_sliceentryoutput) + (dst_negative_scale_lookup_sliceentryoutput)))) * S ((((dst_positive_code_lookup_sliceentryoutput) + (dst_positive_scale_lookup_sliceentryoutput)) * S ((dst_positive_code_lookup_sliceentryoutput) + (dst_positive_scale_lookup_sliceentryoutput)) + ((dst_positive_scale_lookup_sliceentryoutput) + (dst_positive_scale_lookup_sliceentryoutput))) + (((dst_negative_code_lookup_sliceentryoutput) + (dst_negative_scale_lookup_sliceentryoutput)) * S ((dst_negative_code_lookup_sliceentryoutput) + (dst_negative_scale_lookup_sliceentryoutput)) + ((dst_negative_scale_lookup_sliceentryoutput) + (dst_negative_scale_lookup_sliceentryoutput)))) + ((((dst_negative_code_lookup_sliceentryoutput) + (dst_negative_scale_lookup_sliceentryoutput)) * S ((dst_negative_code_lookup_sliceentryoutput) + (dst_negative_scale_lookup_sliceentryoutput)) + ((dst_negative_scale_lookup_sliceentryoutput) + (dst_negative_scale_lookup_sliceentryoutput))) + (((dst_negative_code_lookup_sliceentryoutput) + (dst_negative_scale_lookup_sliceentryoutput)) * S ((dst_negative_code_lookup_sliceentryoutput) + (dst_negative_scale_lookup_sliceentryoutput)) + ((dst_negative_scale_lookup_sliceentryoutput) + (dst_negative_scale_lookup_sliceentryoutput)))))) /\ (((((exists ff_h_pvs_lookup_sliceentryoutputpositive. ff_h_pvs_lookup_sliceentryoutputpositive + S (dst_positive_lookup_sliceentryoutput) = S ((S (srs_index_lookup_slice)) * dst_positive_scale_lookup_sliceentryoutput)) /\ exists ff_q_pvs_lookup_sliceentryoutputpositive. dst_positive_code_lookup_sliceentryoutput = ff_q_pvs_lookup_sliceentryoutputpositive * S ((S (srs_index_lookup_slice)) * dst_positive_scale_lookup_sliceentryoutput) + (dst_positive_lookup_sliceentryoutput))) /\ (((((exists ff_h_pvs_lookup_sliceentryoutputnegative. ff_h_pvs_lookup_sliceentryoutputnegative + S (dst_negative_lookup_sliceentryoutput) = S ((S (srs_index_lookup_slice)) * dst_negative_scale_lookup_sliceentryoutput)) /\ exists ff_q_pvs_lookup_sliceentryoutputnegative. dst_negative_code_lookup_sliceentryoutput = ff_q_pvs_lookup_sliceentryoutputnegative * S ((S (srs_index_lookup_slice)) * dst_negative_scale_lookup_sliceentryoutput) + (dst_negative_lookup_sliceentryoutput))) /\ (exists ge_balance_positive_lookup_sliceentryoutputvalue ge_balance_negative_lookup_sliceentryoutputvalue. (((((srs_value_lookup_slice) = 2 * (ge_balance_positive_lookup_sliceentryoutputvalue) /\ (ge_balance_negative_lookup_sliceentryoutputvalue) = 0) \/ exists ge_signed_half_lookup_sliceentryoutputvaluedecode. (((srs_value_lookup_slice) = 2 * ge_signed_half_lookup_sliceentryoutputvaluedecode + 1 /\ (ge_balance_positive_lookup_sliceentryoutputvalue) = 0) /\ (ge_balance_negative_lookup_sliceentryoutputvalue) = S ge_signed_half_lookup_sliceentryoutputvaluedecode))) /\ ((dst_positive_lookup_sliceentryoutput) + ge_balance_negative_lookup_sliceentryoutputvalue = (dst_negative_lookup_sliceentryoutput) + ge_balance_positive_lookup_sliceentryoutputvalue)))))))))))))))) -> (exists pvs_gap_lookup_bound. pvs_gap_lookup_bound + S (i) = (l)) -> (exists dst_positive_code_lookup_value dst_positive_scale_lookup_value dst_negative_code_lookup_value dst_negative_scale_lookup_value dst_positive_lookup_value dst_negative_lookup_value. (((G) = (((((dst_positive_code_lookup_value) + (dst_positive_scale_lookup_value)) * S ((dst_positive_code_lookup_value) + (dst_positive_scale_lookup_value)) + ((dst_positive_scale_lookup_value) + (dst_positive_scale_lookup_value))) + (((dst_negative_code_lookup_value) + (dst_negative_scale_lookup_value)) * S ((dst_negative_code_lookup_value) + (dst_negative_scale_lookup_value)) + ((dst_negative_scale_lookup_value) + (dst_negative_scale_lookup_value)))) * S ((((dst_positive_code_lookup_value) + (dst_positive_scale_lookup_value)) * S ((dst_positive_code_lookup_value) + (dst_positive_scale_lookup_value)) + ((dst_positive_scale_lookup_value) + (dst_positive_scale_lookup_value))) + (((dst_negative_code_lookup_value) + (dst_negative_scale_lookup_value)) * S ((dst_negative_code_lookup_value) + (dst_negative_scale_lookup_value)) + ((dst_negative_scale_lookup_value) + (dst_negative_scale_lookup_value)))) + ((((dst_negative_code_lookup_value) + (dst_negative_scale_lookup_value)) * S ((dst_negative_code_lookup_value) + (dst_negative_scale_lookup_value)) + ((dst_negative_scale_lookup_value) + (dst_negative_scale_lookup_value))) + (((dst_negative_code_lookup_value) + (dst_negative_scale_lookup_value)) * S ((dst_negative_code_lookup_value) + (dst_negative_scale_lookup_value)) + ((dst_negative_scale_lookup_value) + (dst_negative_scale_lookup_value)))))) /\ (((((exists ff_h_pvs_lookup_valuepositive. ff_h_pvs_lookup_valuepositive + S (dst_positive_lookup_value) = S ((S (i)) * dst_positive_scale_lookup_value)) /\ exists ff_q_pvs_lookup_valuepositive. dst_positive_code_lookup_value = ff_q_pvs_lookup_valuepositive * S ((S (i)) * dst_positive_scale_lookup_value) + (dst_positive_lookup_value))) /\ (((((exists ff_h_pvs_lookup_valuenegative. ff_h_pvs_lookup_valuenegative + S (dst_negative_lookup_value) = S ((S (i)) * dst_negative_scale_lookup_value)) /\ exists ff_q_pvs_lookup_valuenegative. dst_negative_code_lookup_value = ff_q_pvs_lookup_valuenegative * S ((S (i)) * dst_negative_scale_lookup_value) + (dst_negative_lookup_value))) /\ (exists ge_balance_positive_lookup_valuevalue ge_balance_negative_lookup_valuevalue. (((((z) = 2 * (ge_balance_positive_lookup_valuevalue) /\ (ge_balance_negative_lookup_valuevalue) = 0) \/ exists ge_signed_half_lookup_valuevaluedecode. (((z) = 2 * ge_signed_half_lookup_valuevaluedecode + 1 /\ (ge_balance_positive_lookup_valuevalue) = 0) /\ (ge_balance_negative_lookup_valuevalue) = S ge_signed_half_lookup_valuevaluedecode))) /\ ((dst_positive_lookup_value) + ge_balance_negative_lookup_valuevalue = (dst_negative_lookup_value) + ge_balance_positive_lookup_valuevalue))))))))) -> (exists dst_positive_code_lookup_source dst_positive_scale_lookup_source dst_negative_code_lookup_source dst_negative_scale_lookup_source dst_positive_lookup_source dst_negative_lookup_source. (((F) = (((((dst_positive_code_lookup_source) + (dst_positive_scale_lookup_source)) * S ((dst_positive_code_lookup_source) + (dst_positive_scale_lookup_source)) + ((dst_positive_scale_lookup_source) + (dst_positive_scale_lookup_source))) + (((dst_negative_code_lookup_source) + (dst_negative_scale_lookup_source)) * S ((dst_negative_code_lookup_source) + (dst_negative_scale_lookup_source)) + ((dst_negative_scale_lookup_source) + (dst_negative_scale_lookup_source)))) * S ((((dst_positive_code_lookup_source) + (dst_positive_scale_lookup_source)) * S ((dst_positive_code_lookup_source) + (dst_positive_scale_lookup_source)) + ((dst_positive_scale_lookup_source) + (dst_positive_scale_lookup_source))) + (((dst_negative_code_lookup_source) + (dst_negative_scale_lookup_source)) * S ((dst_negative_code_lookup_source) + (dst_negative_scale_lookup_source)) + ((dst_negative_scale_lookup_source) + (dst_negative_scale_lookup_source)))) + ((((dst_negative_code_lookup_source) + (dst_negative_scale_lookup_source)) * S ((dst_negative_code_lookup_source) + (dst_negative_scale_lookup_source)) + ((dst_negative_scale_lookup_source) + (dst_negative_scale_lookup_source))) + (((dst_negative_code_lookup_source) + (dst_negative_scale_lookup_source)) * S ((dst_negative_code_lookup_source) + (dst_negative_scale_lookup_source)) + ((dst_negative_scale_lookup_source) + (dst_negative_scale_lookup_source)))))) /\ (((((exists ff_h_pvs_lookup_sourcepositive. ff_h_pvs_lookup_sourcepositive + S (dst_positive_lookup_source) = S ((S (((o) + ((s) * (i))))) * dst_positive_scale_lookup_source)) /\ exists ff_q_pvs_lookup_sourcepositive. dst_positive_code_lookup_source = ff_q_pvs_lookup_sourcepositive * S ((S (((o) + ((s) * (i))))) * dst_positive_scale_lookup_source) + (dst_positive_lookup_source))) /\ (((((exists ff_h_pvs_lookup_sourcenegative. ff_h_pvs_lookup_sourcenegative + S (dst_negative_lookup_source) = S ((S (((o) + ((s) * (i))))) * dst_negative_scale_lookup_source)) /\ exists ff_q_pvs_lookup_sourcenegative. dst_negative_code_lookup_source = ff_q_pvs_lookup_sourcenegative * S ((S (((o) + ((s) * (i))))) * dst_negative_scale_lookup_source) + (dst_negative_lookup_source))) /\ (exists ge_balance_positive_lookup_sourcevalue ge_balance_negative_lookup_sourcevalue. (((((z) = 2 * (ge_balance_positive_lookup_sourcevalue) /\ (ge_balance_negative_lookup_sourcevalue) = 0) \/ exists ge_signed_half_lookup_sourcevaluedecode. (((z) = 2 * ge_signed_half_lookup_sourcevaluedecode + 1 /\ (ge_balance_positive_lookup_sourcevalue) = 0) /\ (ge_balance_negative_lookup_sourcevalue) = S ge_signed_half_lookup_sourcevaluedecode))) /\ ((dst_positive_lookup_source) + ge_balance_negative_lookup_sourcevalue = (dst_negative_lookup_source) + ge_balance_positive_lookup_sourcevalue)))))))))

Constructive proof overview

Generated structural guide

Every actual slice lookup is the identical canonical signed value at its explicitly computed source index.

The unchanged tactic script uses 1 declared prerequisite and contains 29 exact native proof lines.

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

Proof neighborhood

Direct dependencies

divisor_signed_table_at_functional Alpha theorem; checked-use authorized

Direct dependents

RS0004 signed_rectangular_slice_extensional_unique RS000C signed_rectangular_slice_sum_successor_decompose RS001D signed_rectangular_columns_successor_add

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

Read the argument

Proof checkpoints

29 script commands · 6 reading checkpoints · 2 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.

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

01Fix variables and assumptionsL1–10

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

  1. L1
    intro F
  2. L2
    intro G
  3. L3
    intro o
  4. L4
    intro s
  5. L5
    intro l
  6. L6
    intro i
  7. L7
    intro z
  8. L8
    intro hs
  9. L9
    intro hi
  10. L10
    intro hz
02Separate the logical casesL11–12

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

  1. L11
    cases hs
  2. L12
    cases hs_right
03Establish heL13–16

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

  1. L13
    have he : ∃ a. ArithAt(F,o + s · i,a) ∧ ArithAt(G,i,a)Definitions: ArithAt
  2. L14
    specialize hs_right_right (i)
  3. L15
    apply hs_right_right
  4. L16
    exact hi
04Separate the logical casesL17–18

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

  1. L17
    cases he
  2. L18
    cases he_witness
05Establish heqL19–28

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

  1. L19
    have heq : x = z
  2. L20
    specialize divisor_signed_table_at_functional (G)
  3. L21
    specialize divisor_signed_table_at_functional (i)
  4. L22
    specialize divisor_signed_table_at_functional (x)
  5. L23
    specialize divisor_signed_table_at_functional (z)
  6. L24
    apply divisor_signed_table_at_functional
  7. L25
    exact he_witness_right
  8. L26
    exact hz
  9. L27
    rewrite heq at he_witness_left
  10. L28
    rewrite heq at he_witness_left
06Use earlier factsL29–29

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

  1. L29
    exact he_witness_left

Library-wide reading audit

Original exact command ledger · 29 lines
  1. 0001intro F
  2. 0002intro G
  3. 0003intro o
  4. 0004intro s
  5. 0005intro l
  6. 0006intro i
  7. 0007intro z
  8. 0008intro hs
  9. 0009intro hi
  10. 0010intro hz
  11. 0011cases hs
  12. 0012cases hs_right
  13. 0013have he : exists a. (((exists dst_positive_code_lookup_entrysource dst_positive_scale_lookup_entrysource dst_negative_code_lookup_entrysource dst_negative_scale_lookup_entrysource dst_positive_lookup_entrysource dst_negative_lookup_entrysource. (((F) = (((((dst_positive_code_lookup_entrysource) + (dst_positive_scale_lookup_entrysource)) * S ((dst_positive_code_lookup_entrysource) + (dst_positive_scale_lookup_entrysource)) + ((dst_positive_scale_lookup_entrysource) + (dst_positive_scale_lookup_entrysource))) + (((dst_negative_code_lookup_entrysource) + (dst_negative_scale_lookup_entrysource)) * S ((dst_negative_code_lookup_entrysource) + (dst_negative_scale_lookup_entrysource)) + ((dst_negative_scale_lookup_entrysource) + (dst_negative_scale_lookup_entrysource)))) * S ((((dst_positive_code_lookup_entrysource) + (dst_positive_scale_lookup_entrysource)) * S ((dst_positive_code_lookup_entrysource) + (dst_positive_scale_lookup_entrysource)) + ((dst_positive_scale_lookup_entrysource) + (dst_positive_scale_lookup_entrysource))) + (((dst_negative_code_lookup_entrysource) + (dst_negative_scale_lookup_entrysource)) * S ((dst_negative_code_lookup_entrysource) + (dst_negative_scale_lookup_entrysource)) + ((dst_negative_scale_lookup_entrysource) + (dst_negative_scale_lookup_entrysource)))) + ((((dst_negative_code_lookup_entrysource) + (dst_negative_scale_lookup_entrysource)) * S ((dst_negative_code_lookup_entrysource) + (dst_negative_scale_lookup_entrysource)) + ((dst_negative_scale_lookup_entrysource) + (dst_negative_scale_lookup_entrysource))) + (((dst_negative_code_lookup_entrysource) + (dst_negative_scale_lookup_entrysource)) * S ((dst_negative_code_lookup_entrysource) + (dst_negative_scale_lookup_entrysource)) + ((dst_negative_scale_lookup_entrysource) + (dst_negative_scale_lookup_entrysource)))))) /\ (((((exists ff_h_pvs_lookup_entrysourcepositive. ff_h_pvs_lookup_entrysourcepositive + S (dst_positive_lookup_entrysource) = S ((S (((o) + ((s) * (i))))) * dst_positive_scale_lookup_entrysource)) /\ exists ff_q_pvs_lookup_entrysourcepositive. dst_positive_code_lookup_entrysource = ff_q_pvs_lookup_entrysourcepositive * S ((S (((o) + ((s) * (i))))) * dst_positive_scale_lookup_entrysource) + (dst_positive_lookup_entrysource))) /\ (((((exists ff_h_pvs_lookup_entrysourcenegative. ff_h_pvs_lookup_entrysourcenegative + S (dst_negative_lookup_entrysource) = S ((S (((o) + ((s) * (i))))) * dst_negative_scale_lookup_entrysource)) /\ exists ff_q_pvs_lookup_entrysourcenegative. dst_negative_code_lookup_entrysource = ff_q_pvs_lookup_entrysourcenegative * S ((S (((o) + ((s) * (i))))) * dst_negative_scale_lookup_entrysource) + (dst_negative_lookup_entrysource))) /\ (exists ge_balance_positive_lookup_entrysourcevalue ge_balance_negative_lookup_entrysourcevalue. (((((a) = 2 * (ge_balance_positive_lookup_entrysourcevalue) /\ (ge_balance_negative_lookup_entrysourcevalue) = 0) \/ exists ge_signed_half_lookup_entrysourcevaluedecode. (((a) = 2 * ge_signed_half_lookup_entrysourcevaluedecode + 1 /\ (ge_balance_positive_lookup_entrysourcevalue) = 0) /\ (ge_balance_negative_lookup_entrysourcevalue) = S ge_signed_half_lookup_entrysourcevaluedecode))) /\ ((dst_positive_lookup_entrysource) + ge_balance_negative_lookup_entrysourcevalue = (dst_negative_lookup_entrysource) + ge_balance_positive_lookup_entrysourcevalue))))))))) /\ (exists dst_positive_code_lookup_entryoutput dst_positive_scale_lookup_entryoutput dst_negative_code_lookup_entryoutput dst_negative_scale_lookup_entryoutput dst_positive_lookup_entryoutput dst_negative_lookup_entryoutput. (((G) = (((((dst_positive_code_lookup_entryoutput) + (dst_positive_scale_lookup_entryoutput)) * S ((dst_positive_code_lookup_entryoutput) + (dst_positive_scale_lookup_entryoutput)) + ((dst_positive_scale_lookup_entryoutput) + (dst_positive_scale_lookup_entryoutput))) + (((dst_negative_code_lookup_entryoutput) + (dst_negative_scale_lookup_entryoutput)) * S ((dst_negative_code_lookup_entryoutput) + (dst_negative_scale_lookup_entryoutput)) + ((dst_negative_scale_lookup_entryoutput) + (dst_negative_scale_lookup_entryoutput)))) * S ((((dst_positive_code_lookup_entryoutput) + (dst_positive_scale_lookup_entryoutput)) * S ((dst_positive_code_lookup_entryoutput) + (dst_positive_scale_lookup_entryoutput)) + ((dst_positive_scale_lookup_entryoutput) + (dst_positive_scale_lookup_entryoutput))) + (((dst_negative_code_lookup_entryoutput) + (dst_negative_scale_lookup_entryoutput)) * S ((dst_negative_code_lookup_entryoutput) + (dst_negative_scale_lookup_entryoutput)) + ((dst_negative_scale_lookup_entryoutput) + (dst_negative_scale_lookup_entryoutput)))) + ((((dst_negative_code_lookup_entryoutput) + (dst_negative_scale_lookup_entryoutput)) * S ((dst_negative_code_lookup_entryoutput) + (dst_negative_scale_lookup_entryoutput)) + ((dst_negative_scale_lookup_entryoutput) + (dst_negative_scale_lookup_entryoutput))) + (((dst_negative_code_lookup_entryoutput) + (dst_negative_scale_lookup_entryoutput)) * S ((dst_negative_code_lookup_entryoutput) + (dst_negative_scale_lookup_entryoutput)) + ((dst_negative_scale_lookup_entryoutput) + (dst_negative_scale_lookup_entryoutput)))))) /\ (((((exists ff_h_pvs_lookup_entryoutputpositive. ff_h_pvs_lookup_entryoutputpositive + S (dst_positive_lookup_entryoutput) = S ((S (i)) * dst_positive_scale_lookup_entryoutput)) /\ exists ff_q_pvs_lookup_entryoutputpositive. dst_positive_code_lookup_entryoutput = ff_q_pvs_lookup_entryoutputpositive * S ((S (i)) * dst_positive_scale_lookup_entryoutput) + (dst_positive_lookup_entryoutput))) /\ (((((exists ff_h_pvs_lookup_entryoutputnegative. ff_h_pvs_lookup_entryoutputnegative + S (dst_negative_lookup_entryoutput) = S ((S (i)) * dst_negative_scale_lookup_entryoutput)) /\ exists ff_q_pvs_lookup_entryoutputnegative. dst_negative_code_lookup_entryoutput = ff_q_pvs_lookup_entryoutputnegative * S ((S (i)) * dst_negative_scale_lookup_entryoutput) + (dst_negative_lookup_entryoutput))) /\ (exists ge_balance_positive_lookup_entryoutputvalue ge_balance_negative_lookup_entryoutputvalue. (((((a) = 2 * (ge_balance_positive_lookup_entryoutputvalue) /\ (ge_balance_negative_lookup_entryoutputvalue) = 0) \/ exists ge_signed_half_lookup_entryoutputvaluedecode. (((a) = 2 * ge_signed_half_lookup_entryoutputvaluedecode + 1 /\ (ge_balance_positive_lookup_entryoutputvalue) = 0) /\ (ge_balance_negative_lookup_entryoutputvalue) = S ge_signed_half_lookup_entryoutputvaluedecode))) /\ ((dst_positive_lookup_entryoutput) + ge_balance_negative_lookup_entryoutputvalue = (dst_negative_lookup_entryoutput) + ge_balance_positive_lookup_entryoutputvalue)))))))))))
  14. 0014specialize hs_right_right (i)
  15. 0015apply hs_right_right
  16. 0016exact hi
  17. 0017cases he
  18. 0018cases he_witness
  19. 0019have heq : x = z
  20. 0020specialize divisor_signed_table_at_functional (G)
  21. 0021specialize divisor_signed_table_at_functional (i)
  22. 0022specialize divisor_signed_table_at_functional (x)
  23. 0023specialize divisor_signed_table_at_functional (z)
  24. 0024apply divisor_signed_table_at_functional
  25. 0025exact he_witness_right
  26. 0026exact hz
  27. 0027rewrite heq at he_witness_left
  28. 0028rewrite heq at he_witness_left
  29. 0029exact he_witness_left