MX0020

signed_cartesian_flat_entry_lookup

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

Unique bounded remainder coordinates and signed lookup functionality recover the actual prescribed cell product.

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 n i j a b z. (exists pvs_gap_flat_lookup_bound. pvs_gap_flat_lookup_bound + S (j) = (n)) -> (exists dst_positive_code_flat_lookup_F dst_positive_scale_flat_lookup_F dst_negative_code_flat_lookup_F dst_negative_scale_flat_lookup_F dst_positive_flat_lookup_F dst_negative_flat_lookup_F. (((F) = (((((dst_positive_code_flat_lookup_F) + (dst_positive_scale_flat_lookup_F)) * S ((dst_positive_code_flat_lookup_F) + (dst_positive_scale_flat_lookup_F)) + ((dst_positive_scale_flat_lookup_F) + (dst_positive_scale_flat_lookup_F))) + (((dst_negative_code_flat_lookup_F) + (dst_negative_scale_flat_lookup_F)) * S ((dst_negative_code_flat_lookup_F) + (dst_negative_scale_flat_lookup_F)) + ((dst_negative_scale_flat_lookup_F) + (dst_negative_scale_flat_lookup_F)))) * S ((((dst_positive_code_flat_lookup_F) + (dst_positive_scale_flat_lookup_F)) * S ((dst_positive_code_flat_lookup_F) + (dst_positive_scale_flat_lookup_F)) + ((dst_positive_scale_flat_lookup_F) + (dst_positive_scale_flat_lookup_F))) + (((dst_negative_code_flat_lookup_F) + (dst_negative_scale_flat_lookup_F)) * S ((dst_negative_code_flat_lookup_F) + (dst_negative_scale_flat_lookup_F)) + ((dst_negative_scale_flat_lookup_F) + (dst_negative_scale_flat_lookup_F)))) + ((((dst_negative_code_flat_lookup_F) + (dst_negative_scale_flat_lookup_F)) * S ((dst_negative_code_flat_lookup_F) + (dst_negative_scale_flat_lookup_F)) + ((dst_negative_scale_flat_lookup_F) + (dst_negative_scale_flat_lookup_F))) + (((dst_negative_code_flat_lookup_F) + (dst_negative_scale_flat_lookup_F)) * S ((dst_negative_code_flat_lookup_F) + (dst_negative_scale_flat_lookup_F)) + ((dst_negative_scale_flat_lookup_F) + (dst_negative_scale_flat_lookup_F)))))) /\ (((((exists ff_h_pvs_flat_lookup_Fpositive. ff_h_pvs_flat_lookup_Fpositive + S (dst_positive_flat_lookup_F) = S ((S (i)) * dst_positive_scale_flat_lookup_F)) /\ exists ff_q_pvs_flat_lookup_Fpositive. dst_positive_code_flat_lookup_F = ff_q_pvs_flat_lookup_Fpositive * S ((S (i)) * dst_positive_scale_flat_lookup_F) + (dst_positive_flat_lookup_F))) /\ (((((exists ff_h_pvs_flat_lookup_Fnegative. ff_h_pvs_flat_lookup_Fnegative + S (dst_negative_flat_lookup_F) = S ((S (i)) * dst_negative_scale_flat_lookup_F)) /\ exists ff_q_pvs_flat_lookup_Fnegative. dst_negative_code_flat_lookup_F = ff_q_pvs_flat_lookup_Fnegative * S ((S (i)) * dst_negative_scale_flat_lookup_F) + (dst_negative_flat_lookup_F))) /\ (exists ge_balance_positive_flat_lookup_Fvalue ge_balance_negative_flat_lookup_Fvalue. (((((a) = 2 * (ge_balance_positive_flat_lookup_Fvalue) /\ (ge_balance_negative_flat_lookup_Fvalue) = 0) \/ exists ge_signed_half_flat_lookup_Fvaluedecode. (((a) = 2 * ge_signed_half_flat_lookup_Fvaluedecode + 1 /\ (ge_balance_positive_flat_lookup_Fvalue) = 0) /\ (ge_balance_negative_flat_lookup_Fvalue) = S ge_signed_half_flat_lookup_Fvaluedecode))) /\ ((dst_positive_flat_lookup_F) + ge_balance_negative_flat_lookup_Fvalue = (dst_negative_flat_lookup_F) + ge_balance_positive_flat_lookup_Fvalue))))))))) -> (exists dst_positive_code_flat_lookup_G dst_positive_scale_flat_lookup_G dst_negative_code_flat_lookup_G dst_negative_scale_flat_lookup_G dst_positive_flat_lookup_G dst_negative_flat_lookup_G. (((G) = (((((dst_positive_code_flat_lookup_G) + (dst_positive_scale_flat_lookup_G)) * S ((dst_positive_code_flat_lookup_G) + (dst_positive_scale_flat_lookup_G)) + ((dst_positive_scale_flat_lookup_G) + (dst_positive_scale_flat_lookup_G))) + (((dst_negative_code_flat_lookup_G) + (dst_negative_scale_flat_lookup_G)) * S ((dst_negative_code_flat_lookup_G) + (dst_negative_scale_flat_lookup_G)) + ((dst_negative_scale_flat_lookup_G) + (dst_negative_scale_flat_lookup_G)))) * S ((((dst_positive_code_flat_lookup_G) + (dst_positive_scale_flat_lookup_G)) * S ((dst_positive_code_flat_lookup_G) + (dst_positive_scale_flat_lookup_G)) + ((dst_positive_scale_flat_lookup_G) + (dst_positive_scale_flat_lookup_G))) + (((dst_negative_code_flat_lookup_G) + (dst_negative_scale_flat_lookup_G)) * S ((dst_negative_code_flat_lookup_G) + (dst_negative_scale_flat_lookup_G)) + ((dst_negative_scale_flat_lookup_G) + (dst_negative_scale_flat_lookup_G)))) + ((((dst_negative_code_flat_lookup_G) + (dst_negative_scale_flat_lookup_G)) * S ((dst_negative_code_flat_lookup_G) + (dst_negative_scale_flat_lookup_G)) + ((dst_negative_scale_flat_lookup_G) + (dst_negative_scale_flat_lookup_G))) + (((dst_negative_code_flat_lookup_G) + (dst_negative_scale_flat_lookup_G)) * S ((dst_negative_code_flat_lookup_G) + (dst_negative_scale_flat_lookup_G)) + ((dst_negative_scale_flat_lookup_G) + (dst_negative_scale_flat_lookup_G)))))) /\ (((((exists ff_h_pvs_flat_lookup_Gpositive. ff_h_pvs_flat_lookup_Gpositive + S (dst_positive_flat_lookup_G) = S ((S (j)) * dst_positive_scale_flat_lookup_G)) /\ exists ff_q_pvs_flat_lookup_Gpositive. dst_positive_code_flat_lookup_G = ff_q_pvs_flat_lookup_Gpositive * S ((S (j)) * dst_positive_scale_flat_lookup_G) + (dst_positive_flat_lookup_G))) /\ (((((exists ff_h_pvs_flat_lookup_Gnegative. ff_h_pvs_flat_lookup_Gnegative + S (dst_negative_flat_lookup_G) = S ((S (j)) * dst_negative_scale_flat_lookup_G)) /\ exists ff_q_pvs_flat_lookup_Gnegative. dst_negative_code_flat_lookup_G = ff_q_pvs_flat_lookup_Gnegative * S ((S (j)) * dst_negative_scale_flat_lookup_G) + (dst_negative_flat_lookup_G))) /\ (exists ge_balance_positive_flat_lookup_Gvalue ge_balance_negative_flat_lookup_Gvalue. (((((b) = 2 * (ge_balance_positive_flat_lookup_Gvalue) /\ (ge_balance_negative_flat_lookup_Gvalue) = 0) \/ exists ge_signed_half_flat_lookup_Gvaluedecode. (((b) = 2 * ge_signed_half_flat_lookup_Gvaluedecode + 1 /\ (ge_balance_positive_flat_lookup_Gvalue) = 0) /\ (ge_balance_negative_flat_lookup_Gvalue) = S ge_signed_half_flat_lookup_Gvaluedecode))) /\ ((dst_positive_flat_lookup_G) + ge_balance_negative_flat_lookup_Gvalue = (dst_negative_flat_lookup_G) + ge_balance_positive_flat_lookup_Gvalue))))))))) -> (exists scp_flat_row_flat_lookup_entry scp_flat_column_flat_lookup_entry scp_flat_first_flat_lookup_entry scp_flat_second_flat_lookup_entry. (((((n)*(i)+(j)))=((n)*(scp_flat_row_flat_lookup_entry)+(scp_flat_column_flat_lookup_entry))) /\ (((exists pvs_gap_flat_lookup_entryremainder. pvs_gap_flat_lookup_entryremainder + S (scp_flat_column_flat_lookup_entry) = (n)) /\ (((exists dst_positive_code_flat_lookup_entryF dst_positive_scale_flat_lookup_entryF dst_negative_code_flat_lookup_entryF dst_negative_scale_flat_lookup_entryF dst_positive_flat_lookup_entryF dst_negative_flat_lookup_entryF. (((F) = (((((dst_positive_code_flat_lookup_entryF) + (dst_positive_scale_flat_lookup_entryF)) * S ((dst_positive_code_flat_lookup_entryF) + (dst_positive_scale_flat_lookup_entryF)) + ((dst_positive_scale_flat_lookup_entryF) + (dst_positive_scale_flat_lookup_entryF))) + (((dst_negative_code_flat_lookup_entryF) + (dst_negative_scale_flat_lookup_entryF)) * S ((dst_negative_code_flat_lookup_entryF) + (dst_negative_scale_flat_lookup_entryF)) + ((dst_negative_scale_flat_lookup_entryF) + (dst_negative_scale_flat_lookup_entryF)))) * S ((((dst_positive_code_flat_lookup_entryF) + (dst_positive_scale_flat_lookup_entryF)) * S ((dst_positive_code_flat_lookup_entryF) + (dst_positive_scale_flat_lookup_entryF)) + ((dst_positive_scale_flat_lookup_entryF) + (dst_positive_scale_flat_lookup_entryF))) + (((dst_negative_code_flat_lookup_entryF) + (dst_negative_scale_flat_lookup_entryF)) * S ((dst_negative_code_flat_lookup_entryF) + (dst_negative_scale_flat_lookup_entryF)) + ((dst_negative_scale_flat_lookup_entryF) + (dst_negative_scale_flat_lookup_entryF)))) + ((((dst_negative_code_flat_lookup_entryF) + (dst_negative_scale_flat_lookup_entryF)) * S ((dst_negative_code_flat_lookup_entryF) + (dst_negative_scale_flat_lookup_entryF)) + ((dst_negative_scale_flat_lookup_entryF) + (dst_negative_scale_flat_lookup_entryF))) + (((dst_negative_code_flat_lookup_entryF) + (dst_negative_scale_flat_lookup_entryF)) * S ((dst_negative_code_flat_lookup_entryF) + (dst_negative_scale_flat_lookup_entryF)) + ((dst_negative_scale_flat_lookup_entryF) + (dst_negative_scale_flat_lookup_entryF)))))) /\ (((((exists ff_h_pvs_flat_lookup_entryFpositive. ff_h_pvs_flat_lookup_entryFpositive + S (dst_positive_flat_lookup_entryF) = S ((S (scp_flat_row_flat_lookup_entry)) * dst_positive_scale_flat_lookup_entryF)) /\ exists ff_q_pvs_flat_lookup_entryFpositive. dst_positive_code_flat_lookup_entryF = ff_q_pvs_flat_lookup_entryFpositive * S ((S (scp_flat_row_flat_lookup_entry)) * dst_positive_scale_flat_lookup_entryF) + (dst_positive_flat_lookup_entryF))) /\ (((((exists ff_h_pvs_flat_lookup_entryFnegative. ff_h_pvs_flat_lookup_entryFnegative + S (dst_negative_flat_lookup_entryF) = S ((S (scp_flat_row_flat_lookup_entry)) * dst_negative_scale_flat_lookup_entryF)) /\ exists ff_q_pvs_flat_lookup_entryFnegative. dst_negative_code_flat_lookup_entryF = ff_q_pvs_flat_lookup_entryFnegative * S ((S (scp_flat_row_flat_lookup_entry)) * dst_negative_scale_flat_lookup_entryF) + (dst_negative_flat_lookup_entryF))) /\ (exists ge_balance_positive_flat_lookup_entryFvalue ge_balance_negative_flat_lookup_entryFvalue. (((((scp_flat_first_flat_lookup_entry) = 2 * (ge_balance_positive_flat_lookup_entryFvalue) /\ (ge_balance_negative_flat_lookup_entryFvalue) = 0) \/ exists ge_signed_half_flat_lookup_entryFvaluedecode. (((scp_flat_first_flat_lookup_entry) = 2 * ge_signed_half_flat_lookup_entryFvaluedecode + 1 /\ (ge_balance_positive_flat_lookup_entryFvalue) = 0) /\ (ge_balance_negative_flat_lookup_entryFvalue) = S ge_signed_half_flat_lookup_entryFvaluedecode))) /\ ((dst_positive_flat_lookup_entryF) + ge_balance_negative_flat_lookup_entryFvalue = (dst_negative_flat_lookup_entryF) + ge_balance_positive_flat_lookup_entryFvalue))))))))) /\ (((exists dst_positive_code_flat_lookup_entryG dst_positive_scale_flat_lookup_entryG dst_negative_code_flat_lookup_entryG dst_negative_scale_flat_lookup_entryG dst_positive_flat_lookup_entryG dst_negative_flat_lookup_entryG. (((G) = (((((dst_positive_code_flat_lookup_entryG) + (dst_positive_scale_flat_lookup_entryG)) * S ((dst_positive_code_flat_lookup_entryG) + (dst_positive_scale_flat_lookup_entryG)) + ((dst_positive_scale_flat_lookup_entryG) + (dst_positive_scale_flat_lookup_entryG))) + (((dst_negative_code_flat_lookup_entryG) + (dst_negative_scale_flat_lookup_entryG)) * S ((dst_negative_code_flat_lookup_entryG) + (dst_negative_scale_flat_lookup_entryG)) + ((dst_negative_scale_flat_lookup_entryG) + (dst_negative_scale_flat_lookup_entryG)))) * S ((((dst_positive_code_flat_lookup_entryG) + (dst_positive_scale_flat_lookup_entryG)) * S ((dst_positive_code_flat_lookup_entryG) + (dst_positive_scale_flat_lookup_entryG)) + ((dst_positive_scale_flat_lookup_entryG) + (dst_positive_scale_flat_lookup_entryG))) + (((dst_negative_code_flat_lookup_entryG) + (dst_negative_scale_flat_lookup_entryG)) * S ((dst_negative_code_flat_lookup_entryG) + (dst_negative_scale_flat_lookup_entryG)) + ((dst_negative_scale_flat_lookup_entryG) + (dst_negative_scale_flat_lookup_entryG)))) + ((((dst_negative_code_flat_lookup_entryG) + (dst_negative_scale_flat_lookup_entryG)) * S ((dst_negative_code_flat_lookup_entryG) + (dst_negative_scale_flat_lookup_entryG)) + ((dst_negative_scale_flat_lookup_entryG) + (dst_negative_scale_flat_lookup_entryG))) + (((dst_negative_code_flat_lookup_entryG) + (dst_negative_scale_flat_lookup_entryG)) * S ((dst_negative_code_flat_lookup_entryG) + (dst_negative_scale_flat_lookup_entryG)) + ((dst_negative_scale_flat_lookup_entryG) + (dst_negative_scale_flat_lookup_entryG)))))) /\ (((((exists ff_h_pvs_flat_lookup_entryGpositive. ff_h_pvs_flat_lookup_entryGpositive + S (dst_positive_flat_lookup_entryG) = S ((S (scp_flat_column_flat_lookup_entry)) * dst_positive_scale_flat_lookup_entryG)) /\ exists ff_q_pvs_flat_lookup_entryGpositive. dst_positive_code_flat_lookup_entryG = ff_q_pvs_flat_lookup_entryGpositive * S ((S (scp_flat_column_flat_lookup_entry)) * dst_positive_scale_flat_lookup_entryG) + (dst_positive_flat_lookup_entryG))) /\ (((((exists ff_h_pvs_flat_lookup_entryGnegative. ff_h_pvs_flat_lookup_entryGnegative + S (dst_negative_flat_lookup_entryG) = S ((S (scp_flat_column_flat_lookup_entry)) * dst_negative_scale_flat_lookup_entryG)) /\ exists ff_q_pvs_flat_lookup_entryGnegative. dst_negative_code_flat_lookup_entryG = ff_q_pvs_flat_lookup_entryGnegative * S ((S (scp_flat_column_flat_lookup_entry)) * dst_negative_scale_flat_lookup_entryG) + (dst_negative_flat_lookup_entryG))) /\ (exists ge_balance_positive_flat_lookup_entryGvalue ge_balance_negative_flat_lookup_entryGvalue. (((((scp_flat_second_flat_lookup_entry) = 2 * (ge_balance_positive_flat_lookup_entryGvalue) /\ (ge_balance_negative_flat_lookup_entryGvalue) = 0) \/ exists ge_signed_half_flat_lookup_entryGvaluedecode. (((scp_flat_second_flat_lookup_entry) = 2 * ge_signed_half_flat_lookup_entryGvaluedecode + 1 /\ (ge_balance_positive_flat_lookup_entryGvalue) = 0) /\ (ge_balance_negative_flat_lookup_entryGvalue) = S ge_signed_half_flat_lookup_entryGvaluedecode))) /\ ((dst_positive_flat_lookup_entryG) + ge_balance_negative_flat_lookup_entryGvalue = (dst_negative_flat_lookup_entryG) + ge_balance_positive_flat_lookup_entryGvalue))))))))) /\ (exists sto_ap_flat_lookup_entryvalue sto_an_flat_lookup_entryvalue sto_bp_flat_lookup_entryvalue sto_bn_flat_lookup_entryvalue sto_cp_flat_lookup_entryvalue sto_cn_flat_lookup_entryvalue. (((((scp_flat_first_flat_lookup_entry) = 2 * (sto_ap_flat_lookup_entryvalue) /\ (sto_an_flat_lookup_entryvalue) = 0) \/ exists ge_signed_half_flat_lookup_entryvalueleft. (((scp_flat_first_flat_lookup_entry) = 2 * ge_signed_half_flat_lookup_entryvalueleft + 1 /\ (sto_ap_flat_lookup_entryvalue) = 0) /\ (sto_an_flat_lookup_entryvalue) = S ge_signed_half_flat_lookup_entryvalueleft))) /\ ((((((scp_flat_second_flat_lookup_entry) = 2 * (sto_bp_flat_lookup_entryvalue) /\ (sto_bn_flat_lookup_entryvalue) = 0) \/ exists ge_signed_half_flat_lookup_entryvalueright. (((scp_flat_second_flat_lookup_entry) = 2 * ge_signed_half_flat_lookup_entryvalueright + 1 /\ (sto_bp_flat_lookup_entryvalue) = 0) /\ (sto_bn_flat_lookup_entryvalue) = S ge_signed_half_flat_lookup_entryvalueright))) /\ ((((((z) = 2 * (sto_cp_flat_lookup_entryvalue) /\ (sto_cn_flat_lookup_entryvalue) = 0) \/ exists ge_signed_half_flat_lookup_entryvalueoutput. (((z) = 2 * ge_signed_half_flat_lookup_entryvalueoutput + 1 /\ (sto_cp_flat_lookup_entryvalue) = 0) /\ (sto_cn_flat_lookup_entryvalue) = S ge_signed_half_flat_lookup_entryvalueoutput))) /\ ((sto_ap_flat_lookup_entryvalue * sto_bp_flat_lookup_entryvalue + sto_an_flat_lookup_entryvalue * sto_bn_flat_lookup_entryvalue) + sto_cn_flat_lookup_entryvalue = (sto_ap_flat_lookup_entryvalue * sto_bn_flat_lookup_entryvalue + sto_an_flat_lookup_entryvalue * sto_bp_flat_lookup_entryvalue) + sto_cp_flat_lookup_entryvalue))))))))))))))) -> (exists sto_ap_flat_lookup_result sto_an_flat_lookup_result sto_bp_flat_lookup_result sto_bn_flat_lookup_result sto_cp_flat_lookup_result sto_cn_flat_lookup_result. (((((a) = 2 * (sto_ap_flat_lookup_result) /\ (sto_an_flat_lookup_result) = 0) \/ exists ge_signed_half_flat_lookup_resultleft. (((a) = 2 * ge_signed_half_flat_lookup_resultleft + 1 /\ (sto_ap_flat_lookup_result) = 0) /\ (sto_an_flat_lookup_result) = S ge_signed_half_flat_lookup_resultleft))) /\ ((((((b) = 2 * (sto_bp_flat_lookup_result) /\ (sto_bn_flat_lookup_result) = 0) \/ exists ge_signed_half_flat_lookup_resultright. (((b) = 2 * ge_signed_half_flat_lookup_resultright + 1 /\ (sto_bp_flat_lookup_result) = 0) /\ (sto_bn_flat_lookup_result) = S ge_signed_half_flat_lookup_resultright))) /\ ((((((z) = 2 * (sto_cp_flat_lookup_result) /\ (sto_cn_flat_lookup_result) = 0) \/ exists ge_signed_half_flat_lookup_resultoutput. (((z) = 2 * ge_signed_half_flat_lookup_resultoutput + 1 /\ (sto_cp_flat_lookup_result) = 0) /\ (sto_cn_flat_lookup_result) = S ge_signed_half_flat_lookup_resultoutput))) /\ ((sto_ap_flat_lookup_result * sto_bp_flat_lookup_result + sto_an_flat_lookup_result * sto_bn_flat_lookup_result) + sto_cn_flat_lookup_result = (sto_ap_flat_lookup_result * sto_bn_flat_lookup_result + sto_an_flat_lookup_result * sto_bp_flat_lookup_result) + sto_cp_flat_lookup_result)))))))

Constructive proof overview

Generated structural guide

Unique bounded remainder coordinates and signed lookup functionality recover the actual prescribed cell product.

The unchanged tactic script uses 2 declared prerequisites and contains 62 exact native proof lines.

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

Proof neighborhood

Direct dependencies

division_remainder_unique Stable theorem; checked-use authorized divisor_signed_table_at_functional Alpha theorem; checked-use authorized

Direct dependents

MX0024 signed_cartesian_product_from_flat_prefix

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

62 script commands · 12 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.

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 n
  4. L4
    intro i
  5. L5
    intro j
  6. L6
    intro a
  7. L7
    intro b
  8. L8
    intro z
  9. L9
    intro hj
  10. L10
    intro ha
02Fix variables and assumptionsL11–12

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

  1. L11
    intro hb
  2. L12
    intro hv
03Separate the logical casesL13–20

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

  1. L13
    cases hv
  2. L14
    cases hv_witness
  3. L15
    cases hv_witness_witness
  4. L16
    cases hv_witness_witness_witness
  5. L17
    cases hv_witness_witness_witness_witness
  6. L18
    cases hv_witness_witness_witness_witness_right
  7. L19
    cases hv_witness_witness_witness_witness_right_right
  8. L20
    cases hv_witness_witness_witness_witness_right_right_right
04Establish hcoordL21–30

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

  1. L21
    have hcoord : x=i /\ x1=j
  2. L22
    specialize division_remainder_unique (n)
  3. L23
    specialize division_remainder_unique (((n)*(i)+(j)))
  4. L24
    specialize division_remainder_unique (x)
  5. L25
    specialize division_remainder_unique (x1)
  6. L26
    specialize division_remainder_unique (i)
  7. L27
    specialize division_remainder_unique (j)
  8. L28
    apply division_remainder_unique
  9. L29
    exact hv_witness_witness_witness_witness_left
  10. L30
    exact hv_witness_witness_witness_witness_right_left
05Calculate and transport equalitiesL31–31

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

  1. L31
    refl
06Use earlier factsL32–32

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

  1. L32
    exact hj
07Separate the logical casesL33–33

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

  1. L33
    cases hcoord
08Calculate and transport equalitiesL34–41

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

  1. L34
    rewrite hcoord_left at hv_witness_witness_witness_witness_right_right_left
  2. L35
    rewrite hcoord_left at hv_witness_witness_witness_witness_right_right_left
  3. L36
    rewrite hcoord_left at hv_witness_witness_witness_witness_right_right_left
  4. L37
    rewrite hcoord_left at hv_witness_witness_witness_witness_right_right_left
  5. L38
    rewrite hcoord_right at hv_witness_witness_witness_witness_right_right_right_left
  6. L39
    rewrite hcoord_right at hv_witness_witness_witness_witness_right_right_right_left
  7. L40
    rewrite hcoord_right at hv_witness_witness_witness_witness_right_right_right_left
  8. L41
    rewrite hcoord_right at hv_witness_witness_witness_witness_right_right_right_left
09Establish hfirstL42–49

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

  1. L42
    have hfirst : x2=a
  2. L43
    specialize divisor_signed_table_at_functional (F)
  3. L44
    specialize divisor_signed_table_at_functional (i)
  4. L45
    specialize divisor_signed_table_at_functional (x2)
  5. L46
    specialize divisor_signed_table_at_functional (a)
  6. L47
    apply divisor_signed_table_at_functional
  7. L48
    exact hv_witness_witness_witness_witness_right_right_left
  8. L49
    exact ha
10Establish hsecondL50–59

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

  1. L50
    have hsecond : x3=b
  2. L51
    specialize divisor_signed_table_at_functional (G)
  3. L52
    specialize divisor_signed_table_at_functional (j)
  4. L53
    specialize divisor_signed_table_at_functional (x3)
  5. L54
    specialize divisor_signed_table_at_functional (b)
  6. L55
    apply divisor_signed_table_at_functional
  7. L56
    exact hv_witness_witness_witness_witness_right_right_right_left
  8. L57
    exact hb
  9. L58
    rewrite hfirst at hv_witness_witness_witness_witness_right_right_right_right
  10. L59
    rewrite hfirst at hv_witness_witness_witness_witness_right_right_right_right
11Calculate and transport equalitiesL60–61

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

  1. L60
    rewrite hsecond at hv_witness_witness_witness_witness_right_right_right_right
  2. L61
    rewrite hsecond at hv_witness_witness_witness_witness_right_right_right_right
12Use earlier factsL62–62

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

  1. L62
    exact hv_witness_witness_witness_witness_right_right_right_right

Library-wide reading audit

Original exact command ledger · 62 lines
  1. 0001intro F
  2. 0002intro G
  3. 0003intro n
  4. 0004intro i
  5. 0005intro j
  6. 0006intro a
  7. 0007intro b
  8. 0008intro z
  9. 0009intro hj
  10. 0010intro ha
  11. 0011intro hb
  12. 0012intro hv
  13. 0013cases hv
  14. 0014cases hv_witness
  15. 0015cases hv_witness_witness
  16. 0016cases hv_witness_witness_witness
  17. 0017cases hv_witness_witness_witness_witness
  18. 0018cases hv_witness_witness_witness_witness_right
  19. 0019cases hv_witness_witness_witness_witness_right_right
  20. 0020cases hv_witness_witness_witness_witness_right_right_right
  21. 0021have hcoord : x=i /\ x1=j
  22. 0022specialize division_remainder_unique (n)
  23. 0023specialize division_remainder_unique (((n)*(i)+(j)))
  24. 0024specialize division_remainder_unique (x)
  25. 0025specialize division_remainder_unique (x1)
  26. 0026specialize division_remainder_unique (i)
  27. 0027specialize division_remainder_unique (j)
  28. 0028apply division_remainder_unique
  29. 0029exact hv_witness_witness_witness_witness_left
  30. 0030exact hv_witness_witness_witness_witness_right_left
  31. 0031refl
  32. 0032exact hj
  33. 0033cases hcoord
  34. 0034rewrite hcoord_left at hv_witness_witness_witness_witness_right_right_left
  35. 0035rewrite hcoord_left at hv_witness_witness_witness_witness_right_right_left
  36. 0036rewrite hcoord_left at hv_witness_witness_witness_witness_right_right_left
  37. 0037rewrite hcoord_left at hv_witness_witness_witness_witness_right_right_left
  38. 0038rewrite hcoord_right at hv_witness_witness_witness_witness_right_right_right_left
  39. 0039rewrite hcoord_right at hv_witness_witness_witness_witness_right_right_right_left
  40. 0040rewrite hcoord_right at hv_witness_witness_witness_witness_right_right_right_left
  41. 0041rewrite hcoord_right at hv_witness_witness_witness_witness_right_right_right_left
  42. 0042have hfirst : x2=a
  43. 0043specialize divisor_signed_table_at_functional (F)
  44. 0044specialize divisor_signed_table_at_functional (i)
  45. 0045specialize divisor_signed_table_at_functional (x2)
  46. 0046specialize divisor_signed_table_at_functional (a)
  47. 0047apply divisor_signed_table_at_functional
  48. 0048exact hv_witness_witness_witness_witness_right_right_left
  49. 0049exact ha
  50. 0050have hsecond : x3=b
  51. 0051specialize divisor_signed_table_at_functional (G)
  52. 0052specialize divisor_signed_table_at_functional (j)
  53. 0053specialize divisor_signed_table_at_functional (x3)
  54. 0054specialize divisor_signed_table_at_functional (b)
  55. 0055apply divisor_signed_table_at_functional
  56. 0056exact hv_witness_witness_witness_witness_right_right_right_left
  57. 0057exact hb
  58. 0058rewrite hfirst at hv_witness_witness_witness_witness_right_right_right_right
  59. 0059rewrite hfirst at hv_witness_witness_witness_witness_right_right_right_right
  60. 0060rewrite hsecond at hv_witness_witness_witness_witness_right_right_right_right
  61. 0061rewrite hsecond at hv_witness_witness_witness_witness_right_right_right_right
  62. 0062exact hv_witness_witness_witness_witness_right_right_right_right