RS0006

signed_rectangular_slice_exists

Ordinary induction constructs the affine output by actual two-beta extension, including zero length and zero stride.

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.

Every slice, row table, column table and signed sum is an actual beta-coded witness. Entries are F((o+s*i)+t*j), for i<m and j<n. Zero dimensions and zero strides are allowed; separately certified endpoints are unused. Table uniqueness concerns values, not codes. No infinite-sum assertion is made.

Exact theorem in conservative defined notation

∀ l. ∀ F. ∀ o. ∀ s. ArithTable(0,F) → ∃ x. ArithSlice(F,x,o,s,l)

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

Definition DAG

ArithTable(N,F) · 1ArithAt(F,i,z) · 1ArithExtend(F,G,l,z) · 1ArithSlice(F,G,o,s,l) · 2

Actual proof prerequisites

signed_rectangular_slice_emptydivisor_signed_table_from_components · checked external prerequisitesigned_table_lookup_any · checked external prerequisitearithmetic_signed_table_extend_at · checked external prerequisitesigned_rectangular_slice_extend
Original expanded first-order statement 
forall l F o s. (exists dst_positive_code_exists_input dst_positive_scale_exists_input dst_negative_code_exists_input dst_negative_scale_exists_input. (((F) = (((((dst_positive_code_exists_input) + (dst_positive_scale_exists_input)) * S ((dst_positive_code_exists_input) + (dst_positive_scale_exists_input)) + ((dst_positive_scale_exists_input) + (dst_positive_scale_exists_input))) + (((dst_negative_code_exists_input) + (dst_negative_scale_exists_input)) * S ((dst_negative_code_exists_input) + (dst_negative_scale_exists_input)) + ((dst_negative_scale_exists_input) + (dst_negative_scale_exists_input)))) * S ((((dst_positive_code_exists_input) + (dst_positive_scale_exists_input)) * S ((dst_positive_code_exists_input) + (dst_positive_scale_exists_input)) + ((dst_positive_scale_exists_input) + (dst_positive_scale_exists_input))) + (((dst_negative_code_exists_input) + (dst_negative_scale_exists_input)) * S ((dst_negative_code_exists_input) + (dst_negative_scale_exists_input)) + ((dst_negative_scale_exists_input) + (dst_negative_scale_exists_input)))) + ((((dst_negative_code_exists_input) + (dst_negative_scale_exists_input)) * S ((dst_negative_code_exists_input) + (dst_negative_scale_exists_input)) + ((dst_negative_scale_exists_input) + (dst_negative_scale_exists_input))) + (((dst_negative_code_exists_input) + (dst_negative_scale_exists_input)) * S ((dst_negative_code_exists_input) + (dst_negative_scale_exists_input)) + ((dst_negative_scale_exists_input) + (dst_negative_scale_exists_input)))))) /\ (forall dst_index_exists_input. (exists pvs_le_gap_exists_inputdomain. pvs_le_gap_exists_inputdomain + (dst_index_exists_input) = (0)) -> exists dst_positive_exists_input dst_negative_exists_input dst_value_exists_input. ((((exists ff_h_pvs_exists_inputentrypositive. ff_h_pvs_exists_inputentrypositive + S (dst_positive_exists_input) = S ((S (dst_index_exists_input)) * dst_positive_scale_exists_input)) /\ exists ff_q_pvs_exists_inputentrypositive. dst_positive_code_exists_input = ff_q_pvs_exists_inputentrypositive * S ((S (dst_index_exists_input)) * dst_positive_scale_exists_input) + (dst_positive_exists_input))) /\ (((((exists ff_h_pvs_exists_inputentrynegative. ff_h_pvs_exists_inputentrynegative + S (dst_negative_exists_input) = S ((S (dst_index_exists_input)) * dst_negative_scale_exists_input)) /\ exists ff_q_pvs_exists_inputentrynegative. dst_negative_code_exists_input = ff_q_pvs_exists_inputentrynegative * S ((S (dst_index_exists_input)) * dst_negative_scale_exists_input) + (dst_negative_exists_input))) /\ (exists ge_balance_positive_exists_inputentryvalue ge_balance_negative_exists_inputentryvalue. (((((dst_value_exists_input) = 2 * (ge_balance_positive_exists_inputentryvalue) /\ (ge_balance_negative_exists_inputentryvalue) = 0) \/ exists ge_signed_half_exists_inputentryvaluedecode. (((dst_value_exists_input) = 2 * ge_signed_half_exists_inputentryvaluedecode + 1 /\ (ge_balance_positive_exists_inputentryvalue) = 0) /\ (ge_balance_negative_exists_inputentryvalue) = S ge_signed_half_exists_inputentryvaluedecode))) /\ ((dst_positive_exists_input) + ge_balance_negative_exists_inputentryvalue = (dst_negative_exists_input) + ge_balance_positive_exists_inputentryvalue))))))))) -> exists G. (((exists dst_positive_code_exists_resultsource_table dst_positive_scale_exists_resultsource_table dst_negative_code_exists_resultsource_table dst_negative_scale_exists_resultsource_table. (((F) = (((((dst_positive_code_exists_resultsource_table) + (dst_positive_scale_exists_resultsource_table)) * S ((dst_positive_code_exists_resultsource_table) + (dst_positive_scale_exists_resultsource_table)) + ((dst_positive_scale_exists_resultsource_table) + (dst_positive_scale_exists_resultsource_table))) + (((dst_negative_code_exists_resultsource_table) + (dst_negative_scale_exists_resultsource_table)) * S ((dst_negative_code_exists_resultsource_table) + (dst_negative_scale_exists_resultsource_table)) + ((dst_negative_scale_exists_resultsource_table) + (dst_negative_scale_exists_resultsource_table)))) * S ((((dst_positive_code_exists_resultsource_table) + (dst_positive_scale_exists_resultsource_table)) * S ((dst_positive_code_exists_resultsource_table) + (dst_positive_scale_exists_resultsource_table)) + ((dst_positive_scale_exists_resultsource_table) + (dst_positive_scale_exists_resultsource_table))) + (((dst_negative_code_exists_resultsource_table) + (dst_negative_scale_exists_resultsource_table)) * S ((dst_negative_code_exists_resultsource_table) + (dst_negative_scale_exists_resultsource_table)) + ((dst_negative_scale_exists_resultsource_table) + (dst_negative_scale_exists_resultsource_table)))) + ((((dst_negative_code_exists_resultsource_table) + (dst_negative_scale_exists_resultsource_table)) * S ((dst_negative_code_exists_resultsource_table) + (dst_negative_scale_exists_resultsource_table)) + ((dst_negative_scale_exists_resultsource_table) + (dst_negative_scale_exists_resultsource_table))) + (((dst_negative_code_exists_resultsource_table) + (dst_negative_scale_exists_resultsource_table)) * S ((dst_negative_code_exists_resultsource_table) + (dst_negative_scale_exists_resultsource_table)) + ((dst_negative_scale_exists_resultsource_table) + (dst_negative_scale_exists_resultsource_table)))))) /\ (forall dst_index_exists_resultsource_table. (exists pvs_le_gap_exists_resultsource_tabledomain. pvs_le_gap_exists_resultsource_tabledomain + (dst_index_exists_resultsource_table) = (0)) -> exists dst_positive_exists_resultsource_table dst_negative_exists_resultsource_table dst_value_exists_resultsource_table. ((((exists ff_h_pvs_exists_resultsource_tableentrypositive. ff_h_pvs_exists_resultsource_tableentrypositive + S (dst_positive_exists_resultsource_table) = S ((S (dst_index_exists_resultsource_table)) * dst_positive_scale_exists_resultsource_table)) /\ exists ff_q_pvs_exists_resultsource_tableentrypositive. dst_positive_code_exists_resultsource_table = ff_q_pvs_exists_resultsource_tableentrypositive * S ((S (dst_index_exists_resultsource_table)) * dst_positive_scale_exists_resultsource_table) + (dst_positive_exists_resultsource_table))) /\ (((((exists ff_h_pvs_exists_resultsource_tableentrynegative. ff_h_pvs_exists_resultsource_tableentrynegative + S (dst_negative_exists_resultsource_table) = S ((S (dst_index_exists_resultsource_table)) * dst_negative_scale_exists_resultsource_table)) /\ exists ff_q_pvs_exists_resultsource_tableentrynegative. dst_negative_code_exists_resultsource_table = ff_q_pvs_exists_resultsource_tableentrynegative * S ((S (dst_index_exists_resultsource_table)) * dst_negative_scale_exists_resultsource_table) + (dst_negative_exists_resultsource_table))) /\ (exists ge_balance_positive_exists_resultsource_tableentryvalue ge_balance_negative_exists_resultsource_tableentryvalue. (((((dst_value_exists_resultsource_table) = 2 * (ge_balance_positive_exists_resultsource_tableentryvalue) /\ (ge_balance_negative_exists_resultsource_tableentryvalue) = 0) \/ exists ge_signed_half_exists_resultsource_tableentryvaluedecode. (((dst_value_exists_resultsource_table) = 2 * ge_signed_half_exists_resultsource_tableentryvaluedecode + 1 /\ (ge_balance_positive_exists_resultsource_tableentryvalue) = 0) /\ (ge_balance_negative_exists_resultsource_tableentryvalue) = S ge_signed_half_exists_resultsource_tableentryvaluedecode))) /\ ((dst_positive_exists_resultsource_table) + ge_balance_negative_exists_resultsource_tableentryvalue = (dst_negative_exists_resultsource_table) + ge_balance_positive_exists_resultsource_tableentryvalue))))))))) /\ (((exists dst_positive_code_exists_resultoutput_table dst_positive_scale_exists_resultoutput_table dst_negative_code_exists_resultoutput_table dst_negative_scale_exists_resultoutput_table. (((G) = (((((dst_positive_code_exists_resultoutput_table) + (dst_positive_scale_exists_resultoutput_table)) * S ((dst_positive_code_exists_resultoutput_table) + (dst_positive_scale_exists_resultoutput_table)) + ((dst_positive_scale_exists_resultoutput_table) + (dst_positive_scale_exists_resultoutput_table))) + (((dst_negative_code_exists_resultoutput_table) + (dst_negative_scale_exists_resultoutput_table)) * S ((dst_negative_code_exists_resultoutput_table) + (dst_negative_scale_exists_resultoutput_table)) + ((dst_negative_scale_exists_resultoutput_table) + (dst_negative_scale_exists_resultoutput_table)))) * S ((((dst_positive_code_exists_resultoutput_table) + (dst_positive_scale_exists_resultoutput_table)) * S ((dst_positive_code_exists_resultoutput_table) + (dst_positive_scale_exists_resultoutput_table)) + ((dst_positive_scale_exists_resultoutput_table) + (dst_positive_scale_exists_resultoutput_table))) + (((dst_negative_code_exists_resultoutput_table) + (dst_negative_scale_exists_resultoutput_table)) * S ((dst_negative_code_exists_resultoutput_table) + (dst_negative_scale_exists_resultoutput_table)) + ((dst_negative_scale_exists_resultoutput_table) + (dst_negative_scale_exists_resultoutput_table)))) + ((((dst_negative_code_exists_resultoutput_table) + (dst_negative_scale_exists_resultoutput_table)) * S ((dst_negative_code_exists_resultoutput_table) + (dst_negative_scale_exists_resultoutput_table)) + ((dst_negative_scale_exists_resultoutput_table) + (dst_negative_scale_exists_resultoutput_table))) + (((dst_negative_code_exists_resultoutput_table) + (dst_negative_scale_exists_resultoutput_table)) * S ((dst_negative_code_exists_resultoutput_table) + (dst_negative_scale_exists_resultoutput_table)) + ((dst_negative_scale_exists_resultoutput_table) + (dst_negative_scale_exists_resultoutput_table)))))) /\ (forall dst_index_exists_resultoutput_table. (exists pvs_le_gap_exists_resultoutput_tabledomain. pvs_le_gap_exists_resultoutput_tabledomain + (dst_index_exists_resultoutput_table) = (l)) -> exists dst_positive_exists_resultoutput_table dst_negative_exists_resultoutput_table dst_value_exists_resultoutput_table. ((((exists ff_h_pvs_exists_resultoutput_tableentrypositive. ff_h_pvs_exists_resultoutput_tableentrypositive + S (dst_positive_exists_resultoutput_table) = S ((S (dst_index_exists_resultoutput_table)) * dst_positive_scale_exists_resultoutput_table)) /\ exists ff_q_pvs_exists_resultoutput_tableentrypositive. dst_positive_code_exists_resultoutput_table = ff_q_pvs_exists_resultoutput_tableentrypositive * S ((S (dst_index_exists_resultoutput_table)) * dst_positive_scale_exists_resultoutput_table) + (dst_positive_exists_resultoutput_table))) /\ (((((exists ff_h_pvs_exists_resultoutput_tableentrynegative. ff_h_pvs_exists_resultoutput_tableentrynegative + S (dst_negative_exists_resultoutput_table) = S ((S (dst_index_exists_resultoutput_table)) * dst_negative_scale_exists_resultoutput_table)) /\ exists ff_q_pvs_exists_resultoutput_tableentrynegative. dst_negative_code_exists_resultoutput_table = ff_q_pvs_exists_resultoutput_tableentrynegative * S ((S (dst_index_exists_resultoutput_table)) * dst_negative_scale_exists_resultoutput_table) + (dst_negative_exists_resultoutput_table))) /\ (exists ge_balance_positive_exists_resultoutput_tableentryvalue ge_balance_negative_exists_resultoutput_tableentryvalue. (((((dst_value_exists_resultoutput_table) = 2 * (ge_balance_positive_exists_resultoutput_tableentryvalue) /\ (ge_balance_negative_exists_resultoutput_tableentryvalue) = 0) \/ exists ge_signed_half_exists_resultoutput_tableentryvaluedecode. (((dst_value_exists_resultoutput_table) = 2 * ge_signed_half_exists_resultoutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_exists_resultoutput_tableentryvalue) = 0) /\ (ge_balance_negative_exists_resultoutput_tableentryvalue) = S ge_signed_half_exists_resultoutput_tableentryvaluedecode))) /\ ((dst_positive_exists_resultoutput_table) + ge_balance_negative_exists_resultoutput_tableentryvalue = (dst_negative_exists_resultoutput_table) + ge_balance_positive_exists_resultoutput_tableentryvalue))))))))) /\ (forall srs_index_exists_result. (exists pvs_gap_exists_resultbound. pvs_gap_exists_resultbound + S (srs_index_exists_result) = (l)) -> exists srs_value_exists_result. (((exists dst_positive_code_exists_resultentrysource dst_positive_scale_exists_resultentrysource dst_negative_code_exists_resultentrysource dst_negative_scale_exists_resultentrysource dst_positive_exists_resultentrysource dst_negative_exists_resultentrysource. (((F) = (((((dst_positive_code_exists_resultentrysource) + (dst_positive_scale_exists_resultentrysource)) * S ((dst_positive_code_exists_resultentrysource) + (dst_positive_scale_exists_resultentrysource)) + ((dst_positive_scale_exists_resultentrysource) + (dst_positive_scale_exists_resultentrysource))) + (((dst_negative_code_exists_resultentrysource) + (dst_negative_scale_exists_resultentrysource)) * S ((dst_negative_code_exists_resultentrysource) + (dst_negative_scale_exists_resultentrysource)) + ((dst_negative_scale_exists_resultentrysource) + (dst_negative_scale_exists_resultentrysource)))) * S ((((dst_positive_code_exists_resultentrysource) + (dst_positive_scale_exists_resultentrysource)) * S ((dst_positive_code_exists_resultentrysource) + (dst_positive_scale_exists_resultentrysource)) + ((dst_positive_scale_exists_resultentrysource) + (dst_positive_scale_exists_resultentrysource))) + (((dst_negative_code_exists_resultentrysource) + (dst_negative_scale_exists_resultentrysource)) * S ((dst_negative_code_exists_resultentrysource) + (dst_negative_scale_exists_resultentrysource)) + ((dst_negative_scale_exists_resultentrysource) + (dst_negative_scale_exists_resultentrysource)))) + ((((dst_negative_code_exists_resultentrysource) + (dst_negative_scale_exists_resultentrysource)) * S ((dst_negative_code_exists_resultentrysource) + (dst_negative_scale_exists_resultentrysource)) + ((dst_negative_scale_exists_resultentrysource) + (dst_negative_scale_exists_resultentrysource))) + (((dst_negative_code_exists_resultentrysource) + (dst_negative_scale_exists_resultentrysource)) * S ((dst_negative_code_exists_resultentrysource) + (dst_negative_scale_exists_resultentrysource)) + ((dst_negative_scale_exists_resultentrysource) + (dst_negative_scale_exists_resultentrysource)))))) /\ (((((exists ff_h_pvs_exists_resultentrysourcepositive. ff_h_pvs_exists_resultentrysourcepositive + S (dst_positive_exists_resultentrysource) = S ((S (((o) + ((s) * (srs_index_exists_result))))) * dst_positive_scale_exists_resultentrysource)) /\ exists ff_q_pvs_exists_resultentrysourcepositive. dst_positive_code_exists_resultentrysource = ff_q_pvs_exists_resultentrysourcepositive * S ((S (((o) + ((s) * (srs_index_exists_result))))) * dst_positive_scale_exists_resultentrysource) + (dst_positive_exists_resultentrysource))) /\ (((((exists ff_h_pvs_exists_resultentrysourcenegative. ff_h_pvs_exists_resultentrysourcenegative + S (dst_negative_exists_resultentrysource) = S ((S (((o) + ((s) * (srs_index_exists_result))))) * dst_negative_scale_exists_resultentrysource)) /\ exists ff_q_pvs_exists_resultentrysourcenegative. dst_negative_code_exists_resultentrysource = ff_q_pvs_exists_resultentrysourcenegative * S ((S (((o) + ((s) * (srs_index_exists_result))))) * dst_negative_scale_exists_resultentrysource) + (dst_negative_exists_resultentrysource))) /\ (exists ge_balance_positive_exists_resultentrysourcevalue ge_balance_negative_exists_resultentrysourcevalue. (((((srs_value_exists_result) = 2 * (ge_balance_positive_exists_resultentrysourcevalue) /\ (ge_balance_negative_exists_resultentrysourcevalue) = 0) \/ exists ge_signed_half_exists_resultentrysourcevaluedecode. (((srs_value_exists_result) = 2 * ge_signed_half_exists_resultentrysourcevaluedecode + 1 /\ (ge_balance_positive_exists_resultentrysourcevalue) = 0) /\ (ge_balance_negative_exists_resultentrysourcevalue) = S ge_signed_half_exists_resultentrysourcevaluedecode))) /\ ((dst_positive_exists_resultentrysource) + ge_balance_negative_exists_resultentrysourcevalue = (dst_negative_exists_resultentrysource) + ge_balance_positive_exists_resultentrysourcevalue))))))))) /\ (exists dst_positive_code_exists_resultentryoutput dst_positive_scale_exists_resultentryoutput dst_negative_code_exists_resultentryoutput dst_negative_scale_exists_resultentryoutput dst_positive_exists_resultentryoutput dst_negative_exists_resultentryoutput. (((G) = (((((dst_positive_code_exists_resultentryoutput) + (dst_positive_scale_exists_resultentryoutput)) * S ((dst_positive_code_exists_resultentryoutput) + (dst_positive_scale_exists_resultentryoutput)) + ((dst_positive_scale_exists_resultentryoutput) + (dst_positive_scale_exists_resultentryoutput))) + (((dst_negative_code_exists_resultentryoutput) + (dst_negative_scale_exists_resultentryoutput)) * S ((dst_negative_code_exists_resultentryoutput) + (dst_negative_scale_exists_resultentryoutput)) + ((dst_negative_scale_exists_resultentryoutput) + (dst_negative_scale_exists_resultentryoutput)))) * S ((((dst_positive_code_exists_resultentryoutput) + (dst_positive_scale_exists_resultentryoutput)) * S ((dst_positive_code_exists_resultentryoutput) + (dst_positive_scale_exists_resultentryoutput)) + ((dst_positive_scale_exists_resultentryoutput) + (dst_positive_scale_exists_resultentryoutput))) + (((dst_negative_code_exists_resultentryoutput) + (dst_negative_scale_exists_resultentryoutput)) * S ((dst_negative_code_exists_resultentryoutput) + (dst_negative_scale_exists_resultentryoutput)) + ((dst_negative_scale_exists_resultentryoutput) + (dst_negative_scale_exists_resultentryoutput)))) + ((((dst_negative_code_exists_resultentryoutput) + (dst_negative_scale_exists_resultentryoutput)) * S ((dst_negative_code_exists_resultentryoutput) + (dst_negative_scale_exists_resultentryoutput)) + ((dst_negative_scale_exists_resultentryoutput) + (dst_negative_scale_exists_resultentryoutput))) + (((dst_negative_code_exists_resultentryoutput) + (dst_negative_scale_exists_resultentryoutput)) * S ((dst_negative_code_exists_resultentryoutput) + (dst_negative_scale_exists_resultentryoutput)) + ((dst_negative_scale_exists_resultentryoutput) + (dst_negative_scale_exists_resultentryoutput)))))) /\ (((((exists ff_h_pvs_exists_resultentryoutputpositive. ff_h_pvs_exists_resultentryoutputpositive + S (dst_positive_exists_resultentryoutput) = S ((S (srs_index_exists_result)) * dst_positive_scale_exists_resultentryoutput)) /\ exists ff_q_pvs_exists_resultentryoutputpositive. dst_positive_code_exists_resultentryoutput = ff_q_pvs_exists_resultentryoutputpositive * S ((S (srs_index_exists_result)) * dst_positive_scale_exists_resultentryoutput) + (dst_positive_exists_resultentryoutput))) /\ (((((exists ff_h_pvs_exists_resultentryoutputnegative. ff_h_pvs_exists_resultentryoutputnegative + S (dst_negative_exists_resultentryoutput) = S ((S (srs_index_exists_result)) * dst_negative_scale_exists_resultentryoutput)) /\ exists ff_q_pvs_exists_resultentryoutputnegative. dst_negative_code_exists_resultentryoutput = ff_q_pvs_exists_resultentryoutputnegative * S ((S (srs_index_exists_result)) * dst_negative_scale_exists_resultentryoutput) + (dst_negative_exists_resultentryoutput))) /\ (exists ge_balance_positive_exists_resultentryoutputvalue ge_balance_negative_exists_resultentryoutputvalue. (((((srs_value_exists_result) = 2 * (ge_balance_positive_exists_resultentryoutputvalue) /\ (ge_balance_negative_exists_resultentryoutputvalue) = 0) \/ exists ge_signed_half_exists_resultentryoutputvaluedecode. (((srs_value_exists_result) = 2 * ge_signed_half_exists_resultentryoutputvaluedecode + 1 /\ (ge_balance_positive_exists_resultentryoutputvalue) = 0) /\ (ge_balance_negative_exists_resultentryoutputvalue) = S ge_signed_half_exists_resultentryoutputvaluedecode))) /\ ((dst_positive_exists_resultentryoutput) + ge_balance_negative_exists_resultentryoutputvalue = (dst_negative_exists_resultentryoutput) + ge_balance_positive_exists_resultentryoutputvalue))))))))))))))))

Complete tactic proof in conservative notation

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

64 script commands · 17 reading checkpoints · 3 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 (2)
signed rectangular slice emptysigned rectangular slice 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 o
  4. L4
    intro s
  5. L5
    intro hF
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_rectangular_slice_empty (F)
  2. L8
    specialize signed_rectangular_slice_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)))))
  3. L9
    specialize signed_rectangular_slice_empty (o)
  4. L10
    specialize signed_rectangular_slice_empty (s)
  5. L11
    apply signed_rectangular_slice_empty
  6. L12
    exact hF
  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 o
  3. L23
    intro s
  4. L24
    intro hF
07Establish hpL25–30

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

  1. L25
    have hp : ∃ G. ArithSlice(F,G,o,s,l)Definitions: ArithSlice(F,G,o,s,l)Original native command in the exact edition
  2. L26
    specialize IH (F)
  3. L27
    specialize IH (o)
  4. L28
    specialize IH (s)
  5. L29
    apply IH
  6. L30
    exact hF
08Separate the logical casesL31–31

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

  1. L31
    cases hp
09Establish hvL32–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 hv : ∃ z. ArithAt(F,o + s · l,z)Definitions: ArithAt(F,o + s · l,z)Original native command in the exact edition
  2. L33
    specialize signed_table_lookup_any (0)
  3. L34
    specialize signed_table_lookup_any (F)
  4. L35
    specialize signed_table_lookup_any (((o) + ((s) * (l))))
  5. L36
    apply signed_table_lookup_any
  6. L37
    exact hF
10Separate the logical casesL38–38

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

  1. L38
    cases hv
11Establish heL39–44

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

  1. L39
    have he : ∃ H. ArithExtend(x,H,l,x1)Definitions: ArithExtend(x,H,l,x1)Original native command in the exact edition
  2. L40
    specialize arithmetic_signed_table_extend_at (l)
  3. L41
    specialize arithmetic_signed_table_extend_at (x)
  4. L42
    specialize arithmetic_signed_table_extend_at (l)
  5. L43
    specialize arithmetic_signed_table_extend_at (x1)
  6. L44
    apply arithmetic_signed_table_extend_at
12Separate the logical casesL45–46

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

  1. L45
    cases hp_witness
  2. L46
    cases hp_witness_right
13Use earlier factsL47–47

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

  1. L47
    exact hp_witness_right_left
14Separate the logical casesL48–50

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

  1. L48
    cases he
  2. L49
    cases he_witness
  3. L50
    cases he_witness_right
15Construct an explicit witnessL51–51

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

  1. L51
    exists x2
16Use earlier factsL52–61

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

  1. L52
    specialize signed_rectangular_slice_extend (F)
  2. L53
    specialize signed_rectangular_slice_extend (x)
  3. L54
    specialize signed_rectangular_slice_extend (x2)
  4. L55
    specialize signed_rectangular_slice_extend (o)
  5. L56
    specialize signed_rectangular_slice_extend (s)
  6. L57
    specialize signed_rectangular_slice_extend (l)
  7. L58
    specialize signed_rectangular_slice_extend (x1)
  8. L59
    apply signed_rectangular_slice_extend
  9. L60
    exact hp_witness
  10. L61
    exact he_witness_left
17Use earlier factsL62–64

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

  1. L62
    exact he_witness_right_left
  2. L63
    exact hv_witness
  3. L64
    exact he_witness_right_right

Library-wide reading audit

Original defined command ledger · 64 lines
  1. 0001induction l
  2. 0002intro F
  3. 0003intro o
  4. 0004intro s
  5. 0005intro hF
  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_rectangular_slice_empty (F)
  8. 0008specialize signed_rectangular_slice_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. 0009specialize signed_rectangular_slice_empty (o)
  10. 0010specialize signed_rectangular_slice_empty (s)
  11. 0011apply signed_rectangular_slice_empty
  12. 0012exact hF
  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 o
  23. 0023intro s
  24. 0024intro hF
  25. 0025have hp : ∃ G. ArithSlice(F,G,o,s,l)
  26. 0026specialize IH (F)
  27. 0027specialize IH (o)
  28. 0028specialize IH (s)
  29. 0029apply IH
  30. 0030exact hF
  31. 0031cases hp
  32. 0032have hv : ∃ z. ArithAt(F,o + s · l,z)
  33. 0033specialize signed_table_lookup_any (0)
  34. 0034specialize signed_table_lookup_any (F)
  35. 0035specialize signed_table_lookup_any (((o) + ((s) * (l))))
  36. 0036apply signed_table_lookup_any
  37. 0037exact hF
  38. 0038cases hv
  39. 0039have he : ∃ H. ArithExtend(x,H,l,x1)
  40. 0040specialize arithmetic_signed_table_extend_at (l)
  41. 0041specialize arithmetic_signed_table_extend_at (x)
  42. 0042specialize arithmetic_signed_table_extend_at (l)
  43. 0043specialize arithmetic_signed_table_extend_at (x1)
  44. 0044apply arithmetic_signed_table_extend_at
  45. 0045cases hp_witness
  46. 0046cases hp_witness_right
  47. 0047exact hp_witness_right_left
  48. 0048cases he
  49. 0049cases he_witness
  50. 0050cases he_witness_right
  51. 0051exists x2
  52. 0052specialize signed_rectangular_slice_extend (F)
  53. 0053specialize signed_rectangular_slice_extend (x)
  54. 0054specialize signed_rectangular_slice_extend (x2)
  55. 0055specialize signed_rectangular_slice_extend (o)
  56. 0056specialize signed_rectangular_slice_extend (s)
  57. 0057specialize signed_rectangular_slice_extend (l)
  58. 0058specialize signed_rectangular_slice_extend (x1)
  59. 0059apply signed_rectangular_slice_extend
  60. 0060exact hp_witness
  61. 0061exact he_witness_left
  62. 0062exact he_witness_right_left
  63. 0063exact hv_witness
  64. 0064exact he_witness_right_right