MX001F

signed_cartesian_flat_entry_exists

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

For positive physical width, actual quotient/remainder and actual signed lookups construct each flattened product value.

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 k. (exists dst_positive_code_flat_exists_F dst_positive_scale_flat_exists_F dst_negative_code_flat_exists_F dst_negative_scale_flat_exists_F. (((F) = (((((dst_positive_code_flat_exists_F) + (dst_positive_scale_flat_exists_F)) * S ((dst_positive_code_flat_exists_F) + (dst_positive_scale_flat_exists_F)) + ((dst_positive_scale_flat_exists_F) + (dst_positive_scale_flat_exists_F))) + (((dst_negative_code_flat_exists_F) + (dst_negative_scale_flat_exists_F)) * S ((dst_negative_code_flat_exists_F) + (dst_negative_scale_flat_exists_F)) + ((dst_negative_scale_flat_exists_F) + (dst_negative_scale_flat_exists_F)))) * S ((((dst_positive_code_flat_exists_F) + (dst_positive_scale_flat_exists_F)) * S ((dst_positive_code_flat_exists_F) + (dst_positive_scale_flat_exists_F)) + ((dst_positive_scale_flat_exists_F) + (dst_positive_scale_flat_exists_F))) + (((dst_negative_code_flat_exists_F) + (dst_negative_scale_flat_exists_F)) * S ((dst_negative_code_flat_exists_F) + (dst_negative_scale_flat_exists_F)) + ((dst_negative_scale_flat_exists_F) + (dst_negative_scale_flat_exists_F)))) + ((((dst_negative_code_flat_exists_F) + (dst_negative_scale_flat_exists_F)) * S ((dst_negative_code_flat_exists_F) + (dst_negative_scale_flat_exists_F)) + ((dst_negative_scale_flat_exists_F) + (dst_negative_scale_flat_exists_F))) + (((dst_negative_code_flat_exists_F) + (dst_negative_scale_flat_exists_F)) * S ((dst_negative_code_flat_exists_F) + (dst_negative_scale_flat_exists_F)) + ((dst_negative_scale_flat_exists_F) + (dst_negative_scale_flat_exists_F)))))) /\ (forall dst_index_flat_exists_F. (exists pvs_le_gap_flat_exists_Fdomain. pvs_le_gap_flat_exists_Fdomain + (dst_index_flat_exists_F) = (0)) -> exists dst_positive_flat_exists_F dst_negative_flat_exists_F dst_value_flat_exists_F. ((((exists ff_h_pvs_flat_exists_Fentrypositive. ff_h_pvs_flat_exists_Fentrypositive + S (dst_positive_flat_exists_F) = S ((S (dst_index_flat_exists_F)) * dst_positive_scale_flat_exists_F)) /\ exists ff_q_pvs_flat_exists_Fentrypositive. dst_positive_code_flat_exists_F = ff_q_pvs_flat_exists_Fentrypositive * S ((S (dst_index_flat_exists_F)) * dst_positive_scale_flat_exists_F) + (dst_positive_flat_exists_F))) /\ (((((exists ff_h_pvs_flat_exists_Fentrynegative. ff_h_pvs_flat_exists_Fentrynegative + S (dst_negative_flat_exists_F) = S ((S (dst_index_flat_exists_F)) * dst_negative_scale_flat_exists_F)) /\ exists ff_q_pvs_flat_exists_Fentrynegative. dst_negative_code_flat_exists_F = ff_q_pvs_flat_exists_Fentrynegative * S ((S (dst_index_flat_exists_F)) * dst_negative_scale_flat_exists_F) + (dst_negative_flat_exists_F))) /\ (exists ge_balance_positive_flat_exists_Fentryvalue ge_balance_negative_flat_exists_Fentryvalue. (((((dst_value_flat_exists_F) = 2 * (ge_balance_positive_flat_exists_Fentryvalue) /\ (ge_balance_negative_flat_exists_Fentryvalue) = 0) \/ exists ge_signed_half_flat_exists_Fentryvaluedecode. (((dst_value_flat_exists_F) = 2 * ge_signed_half_flat_exists_Fentryvaluedecode + 1 /\ (ge_balance_positive_flat_exists_Fentryvalue) = 0) /\ (ge_balance_negative_flat_exists_Fentryvalue) = S ge_signed_half_flat_exists_Fentryvaluedecode))) /\ ((dst_positive_flat_exists_F) + ge_balance_negative_flat_exists_Fentryvalue = (dst_negative_flat_exists_F) + ge_balance_positive_flat_exists_Fentryvalue))))))))) -> (exists dst_positive_code_flat_exists_G dst_positive_scale_flat_exists_G dst_negative_code_flat_exists_G dst_negative_scale_flat_exists_G. (((G) = (((((dst_positive_code_flat_exists_G) + (dst_positive_scale_flat_exists_G)) * S ((dst_positive_code_flat_exists_G) + (dst_positive_scale_flat_exists_G)) + ((dst_positive_scale_flat_exists_G) + (dst_positive_scale_flat_exists_G))) + (((dst_negative_code_flat_exists_G) + (dst_negative_scale_flat_exists_G)) * S ((dst_negative_code_flat_exists_G) + (dst_negative_scale_flat_exists_G)) + ((dst_negative_scale_flat_exists_G) + (dst_negative_scale_flat_exists_G)))) * S ((((dst_positive_code_flat_exists_G) + (dst_positive_scale_flat_exists_G)) * S ((dst_positive_code_flat_exists_G) + (dst_positive_scale_flat_exists_G)) + ((dst_positive_scale_flat_exists_G) + (dst_positive_scale_flat_exists_G))) + (((dst_negative_code_flat_exists_G) + (dst_negative_scale_flat_exists_G)) * S ((dst_negative_code_flat_exists_G) + (dst_negative_scale_flat_exists_G)) + ((dst_negative_scale_flat_exists_G) + (dst_negative_scale_flat_exists_G)))) + ((((dst_negative_code_flat_exists_G) + (dst_negative_scale_flat_exists_G)) * S ((dst_negative_code_flat_exists_G) + (dst_negative_scale_flat_exists_G)) + ((dst_negative_scale_flat_exists_G) + (dst_negative_scale_flat_exists_G))) + (((dst_negative_code_flat_exists_G) + (dst_negative_scale_flat_exists_G)) * S ((dst_negative_code_flat_exists_G) + (dst_negative_scale_flat_exists_G)) + ((dst_negative_scale_flat_exists_G) + (dst_negative_scale_flat_exists_G)))))) /\ (forall dst_index_flat_exists_G. (exists pvs_le_gap_flat_exists_Gdomain. pvs_le_gap_flat_exists_Gdomain + (dst_index_flat_exists_G) = (0)) -> exists dst_positive_flat_exists_G dst_negative_flat_exists_G dst_value_flat_exists_G. ((((exists ff_h_pvs_flat_exists_Gentrypositive. ff_h_pvs_flat_exists_Gentrypositive + S (dst_positive_flat_exists_G) = S ((S (dst_index_flat_exists_G)) * dst_positive_scale_flat_exists_G)) /\ exists ff_q_pvs_flat_exists_Gentrypositive. dst_positive_code_flat_exists_G = ff_q_pvs_flat_exists_Gentrypositive * S ((S (dst_index_flat_exists_G)) * dst_positive_scale_flat_exists_G) + (dst_positive_flat_exists_G))) /\ (((((exists ff_h_pvs_flat_exists_Gentrynegative. ff_h_pvs_flat_exists_Gentrynegative + S (dst_negative_flat_exists_G) = S ((S (dst_index_flat_exists_G)) * dst_negative_scale_flat_exists_G)) /\ exists ff_q_pvs_flat_exists_Gentrynegative. dst_negative_code_flat_exists_G = ff_q_pvs_flat_exists_Gentrynegative * S ((S (dst_index_flat_exists_G)) * dst_negative_scale_flat_exists_G) + (dst_negative_flat_exists_G))) /\ (exists ge_balance_positive_flat_exists_Gentryvalue ge_balance_negative_flat_exists_Gentryvalue. (((((dst_value_flat_exists_G) = 2 * (ge_balance_positive_flat_exists_Gentryvalue) /\ (ge_balance_negative_flat_exists_Gentryvalue) = 0) \/ exists ge_signed_half_flat_exists_Gentryvaluedecode. (((dst_value_flat_exists_G) = 2 * ge_signed_half_flat_exists_Gentryvaluedecode + 1 /\ (ge_balance_positive_flat_exists_Gentryvalue) = 0) /\ (ge_balance_negative_flat_exists_Gentryvalue) = S ge_signed_half_flat_exists_Gentryvaluedecode))) /\ ((dst_positive_flat_exists_G) + ge_balance_negative_flat_exists_Gentryvalue = (dst_negative_flat_exists_G) + ge_balance_positive_flat_exists_Gentryvalue))))))))) -> ~(n=0) -> exists z. (exists scp_flat_row_flat_exists_result scp_flat_column_flat_exists_result scp_flat_first_flat_exists_result scp_flat_second_flat_exists_result. (((k)=((n)*(scp_flat_row_flat_exists_result)+(scp_flat_column_flat_exists_result))) /\ (((exists pvs_gap_flat_exists_resultremainder. pvs_gap_flat_exists_resultremainder + S (scp_flat_column_flat_exists_result) = (n)) /\ (((exists dst_positive_code_flat_exists_resultF dst_positive_scale_flat_exists_resultF dst_negative_code_flat_exists_resultF dst_negative_scale_flat_exists_resultF dst_positive_flat_exists_resultF dst_negative_flat_exists_resultF. (((F) = (((((dst_positive_code_flat_exists_resultF) + (dst_positive_scale_flat_exists_resultF)) * S ((dst_positive_code_flat_exists_resultF) + (dst_positive_scale_flat_exists_resultF)) + ((dst_positive_scale_flat_exists_resultF) + (dst_positive_scale_flat_exists_resultF))) + (((dst_negative_code_flat_exists_resultF) + (dst_negative_scale_flat_exists_resultF)) * S ((dst_negative_code_flat_exists_resultF) + (dst_negative_scale_flat_exists_resultF)) + ((dst_negative_scale_flat_exists_resultF) + (dst_negative_scale_flat_exists_resultF)))) * S ((((dst_positive_code_flat_exists_resultF) + (dst_positive_scale_flat_exists_resultF)) * S ((dst_positive_code_flat_exists_resultF) + (dst_positive_scale_flat_exists_resultF)) + ((dst_positive_scale_flat_exists_resultF) + (dst_positive_scale_flat_exists_resultF))) + (((dst_negative_code_flat_exists_resultF) + (dst_negative_scale_flat_exists_resultF)) * S ((dst_negative_code_flat_exists_resultF) + (dst_negative_scale_flat_exists_resultF)) + ((dst_negative_scale_flat_exists_resultF) + (dst_negative_scale_flat_exists_resultF)))) + ((((dst_negative_code_flat_exists_resultF) + (dst_negative_scale_flat_exists_resultF)) * S ((dst_negative_code_flat_exists_resultF) + (dst_negative_scale_flat_exists_resultF)) + ((dst_negative_scale_flat_exists_resultF) + (dst_negative_scale_flat_exists_resultF))) + (((dst_negative_code_flat_exists_resultF) + (dst_negative_scale_flat_exists_resultF)) * S ((dst_negative_code_flat_exists_resultF) + (dst_negative_scale_flat_exists_resultF)) + ((dst_negative_scale_flat_exists_resultF) + (dst_negative_scale_flat_exists_resultF)))))) /\ (((((exists ff_h_pvs_flat_exists_resultFpositive. ff_h_pvs_flat_exists_resultFpositive + S (dst_positive_flat_exists_resultF) = S ((S (scp_flat_row_flat_exists_result)) * dst_positive_scale_flat_exists_resultF)) /\ exists ff_q_pvs_flat_exists_resultFpositive. dst_positive_code_flat_exists_resultF = ff_q_pvs_flat_exists_resultFpositive * S ((S (scp_flat_row_flat_exists_result)) * dst_positive_scale_flat_exists_resultF) + (dst_positive_flat_exists_resultF))) /\ (((((exists ff_h_pvs_flat_exists_resultFnegative. ff_h_pvs_flat_exists_resultFnegative + S (dst_negative_flat_exists_resultF) = S ((S (scp_flat_row_flat_exists_result)) * dst_negative_scale_flat_exists_resultF)) /\ exists ff_q_pvs_flat_exists_resultFnegative. dst_negative_code_flat_exists_resultF = ff_q_pvs_flat_exists_resultFnegative * S ((S (scp_flat_row_flat_exists_result)) * dst_negative_scale_flat_exists_resultF) + (dst_negative_flat_exists_resultF))) /\ (exists ge_balance_positive_flat_exists_resultFvalue ge_balance_negative_flat_exists_resultFvalue. (((((scp_flat_first_flat_exists_result) = 2 * (ge_balance_positive_flat_exists_resultFvalue) /\ (ge_balance_negative_flat_exists_resultFvalue) = 0) \/ exists ge_signed_half_flat_exists_resultFvaluedecode. (((scp_flat_first_flat_exists_result) = 2 * ge_signed_half_flat_exists_resultFvaluedecode + 1 /\ (ge_balance_positive_flat_exists_resultFvalue) = 0) /\ (ge_balance_negative_flat_exists_resultFvalue) = S ge_signed_half_flat_exists_resultFvaluedecode))) /\ ((dst_positive_flat_exists_resultF) + ge_balance_negative_flat_exists_resultFvalue = (dst_negative_flat_exists_resultF) + ge_balance_positive_flat_exists_resultFvalue))))))))) /\ (((exists dst_positive_code_flat_exists_resultG dst_positive_scale_flat_exists_resultG dst_negative_code_flat_exists_resultG dst_negative_scale_flat_exists_resultG dst_positive_flat_exists_resultG dst_negative_flat_exists_resultG. (((G) = (((((dst_positive_code_flat_exists_resultG) + (dst_positive_scale_flat_exists_resultG)) * S ((dst_positive_code_flat_exists_resultG) + (dst_positive_scale_flat_exists_resultG)) + ((dst_positive_scale_flat_exists_resultG) + (dst_positive_scale_flat_exists_resultG))) + (((dst_negative_code_flat_exists_resultG) + (dst_negative_scale_flat_exists_resultG)) * S ((dst_negative_code_flat_exists_resultG) + (dst_negative_scale_flat_exists_resultG)) + ((dst_negative_scale_flat_exists_resultG) + (dst_negative_scale_flat_exists_resultG)))) * S ((((dst_positive_code_flat_exists_resultG) + (dst_positive_scale_flat_exists_resultG)) * S ((dst_positive_code_flat_exists_resultG) + (dst_positive_scale_flat_exists_resultG)) + ((dst_positive_scale_flat_exists_resultG) + (dst_positive_scale_flat_exists_resultG))) + (((dst_negative_code_flat_exists_resultG) + (dst_negative_scale_flat_exists_resultG)) * S ((dst_negative_code_flat_exists_resultG) + (dst_negative_scale_flat_exists_resultG)) + ((dst_negative_scale_flat_exists_resultG) + (dst_negative_scale_flat_exists_resultG)))) + ((((dst_negative_code_flat_exists_resultG) + (dst_negative_scale_flat_exists_resultG)) * S ((dst_negative_code_flat_exists_resultG) + (dst_negative_scale_flat_exists_resultG)) + ((dst_negative_scale_flat_exists_resultG) + (dst_negative_scale_flat_exists_resultG))) + (((dst_negative_code_flat_exists_resultG) + (dst_negative_scale_flat_exists_resultG)) * S ((dst_negative_code_flat_exists_resultG) + (dst_negative_scale_flat_exists_resultG)) + ((dst_negative_scale_flat_exists_resultG) + (dst_negative_scale_flat_exists_resultG)))))) /\ (((((exists ff_h_pvs_flat_exists_resultGpositive. ff_h_pvs_flat_exists_resultGpositive + S (dst_positive_flat_exists_resultG) = S ((S (scp_flat_column_flat_exists_result)) * dst_positive_scale_flat_exists_resultG)) /\ exists ff_q_pvs_flat_exists_resultGpositive. dst_positive_code_flat_exists_resultG = ff_q_pvs_flat_exists_resultGpositive * S ((S (scp_flat_column_flat_exists_result)) * dst_positive_scale_flat_exists_resultG) + (dst_positive_flat_exists_resultG))) /\ (((((exists ff_h_pvs_flat_exists_resultGnegative. ff_h_pvs_flat_exists_resultGnegative + S (dst_negative_flat_exists_resultG) = S ((S (scp_flat_column_flat_exists_result)) * dst_negative_scale_flat_exists_resultG)) /\ exists ff_q_pvs_flat_exists_resultGnegative. dst_negative_code_flat_exists_resultG = ff_q_pvs_flat_exists_resultGnegative * S ((S (scp_flat_column_flat_exists_result)) * dst_negative_scale_flat_exists_resultG) + (dst_negative_flat_exists_resultG))) /\ (exists ge_balance_positive_flat_exists_resultGvalue ge_balance_negative_flat_exists_resultGvalue. (((((scp_flat_second_flat_exists_result) = 2 * (ge_balance_positive_flat_exists_resultGvalue) /\ (ge_balance_negative_flat_exists_resultGvalue) = 0) \/ exists ge_signed_half_flat_exists_resultGvaluedecode. (((scp_flat_second_flat_exists_result) = 2 * ge_signed_half_flat_exists_resultGvaluedecode + 1 /\ (ge_balance_positive_flat_exists_resultGvalue) = 0) /\ (ge_balance_negative_flat_exists_resultGvalue) = S ge_signed_half_flat_exists_resultGvaluedecode))) /\ ((dst_positive_flat_exists_resultG) + ge_balance_negative_flat_exists_resultGvalue = (dst_negative_flat_exists_resultG) + ge_balance_positive_flat_exists_resultGvalue))))))))) /\ (exists sto_ap_flat_exists_resultvalue sto_an_flat_exists_resultvalue sto_bp_flat_exists_resultvalue sto_bn_flat_exists_resultvalue sto_cp_flat_exists_resultvalue sto_cn_flat_exists_resultvalue. (((((scp_flat_first_flat_exists_result) = 2 * (sto_ap_flat_exists_resultvalue) /\ (sto_an_flat_exists_resultvalue) = 0) \/ exists ge_signed_half_flat_exists_resultvalueleft. (((scp_flat_first_flat_exists_result) = 2 * ge_signed_half_flat_exists_resultvalueleft + 1 /\ (sto_ap_flat_exists_resultvalue) = 0) /\ (sto_an_flat_exists_resultvalue) = S ge_signed_half_flat_exists_resultvalueleft))) /\ ((((((scp_flat_second_flat_exists_result) = 2 * (sto_bp_flat_exists_resultvalue) /\ (sto_bn_flat_exists_resultvalue) = 0) \/ exists ge_signed_half_flat_exists_resultvalueright. (((scp_flat_second_flat_exists_result) = 2 * ge_signed_half_flat_exists_resultvalueright + 1 /\ (sto_bp_flat_exists_resultvalue) = 0) /\ (sto_bn_flat_exists_resultvalue) = S ge_signed_half_flat_exists_resultvalueright))) /\ ((((((z) = 2 * (sto_cp_flat_exists_resultvalue) /\ (sto_cn_flat_exists_resultvalue) = 0) \/ exists ge_signed_half_flat_exists_resultvalueoutput. (((z) = 2 * ge_signed_half_flat_exists_resultvalueoutput + 1 /\ (sto_cp_flat_exists_resultvalue) = 0) /\ (sto_cn_flat_exists_resultvalue) = S ge_signed_half_flat_exists_resultvalueoutput))) /\ ((sto_ap_flat_exists_resultvalue * sto_bp_flat_exists_resultvalue + sto_an_flat_exists_resultvalue * sto_bn_flat_exists_resultvalue) + sto_cn_flat_exists_resultvalue = (sto_ap_flat_exists_resultvalue * sto_bn_flat_exists_resultvalue + sto_an_flat_exists_resultvalue * sto_bp_flat_exists_resultvalue) + sto_cp_flat_exists_resultvalue)))))))))))))))

Constructive proof overview

Generated structural guide

For positive physical width, actual quotient/remainder and actual signed lookups construct each flattened product value.

The unchanged tactic script uses 3 declared prerequisites and contains 48 exact native proof lines.

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

Proof neighborhood

Direct dependencies

division_remainder_exists Stable theorem; checked-use authorized signed_table_lookup_any Alpha theorem; checked-use authorized signed_mul_total Alpha theorem; checked-use authorized

Direct dependents

MX0023 signed_cartesian_flat_prefix_exists

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

48 script commands · 18 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.

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–7

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 k
  5. L5
    intro hF
  6. L6
    intro hG
  7. L7
    intro hn
02Establish hdL8–12

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

  1. L8
    have hd : exists i j. ((k=n*i+j) /\ (exists pvs_gap_flat_division. pvs_gap_flat_division + S (j) = (n)))
  2. L9
    specialize division_remainder_exists (n)
  3. L10
    specialize division_remainder_exists (k)
  4. L11
    apply division_remainder_exists
  5. L12
    exact hn
03Separate the logical casesL13–15

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

  1. L13
    cases hd
  2. L14
    cases hd_witness
  3. L15
    cases hd_witness_witness
04Establish haL16–21

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

  1. L16
    have ha : ∃ a. ArithAt(F,x,a)Definitions: ArithAt
  2. L17
    specialize signed_table_lookup_any (0)
  3. L18
    specialize signed_table_lookup_any (F)
  4. L19
    specialize signed_table_lookup_any (x)
  5. L20
    apply signed_table_lookup_any
  6. L21
    exact hF
05Separate the logical casesL22–22

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

  1. L22
    cases ha
06Establish hbL23–28

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

  1. L23
    have hb : ∃ b. ArithAt(G,x1,b)Definitions: ArithAt
  2. L24
    specialize signed_table_lookup_any (0)
  3. L25
    specialize signed_table_lookup_any (G)
  4. L26
    specialize signed_table_lookup_any (x1)
  5. L27
    apply signed_table_lookup_any
  6. L28
    exact hG
07Separate the logical casesL29–29

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

  1. L29
    cases hb
08Establish hzL30–33

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

  1. L30
    have hz : ∃ z. SignedMul(x2,x3,z)Definitions: SignedMul
  2. L31
    specialize signed_mul_total (x2)
  3. L32
    specialize signed_mul_total (x3)
  4. L33
    apply signed_mul_total
09Separate the logical casesL34–34

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

  1. L34
    cases hz
10Construct an explicit witnessL35–39

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

  1. L35
    exists x4
  2. L36
    exists x
  3. L37
    exists x1
  4. L38
    exists x2
  5. L39
    exists x3
11Separate the logical casesL40–40

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

  1. L40
    split
12Use earlier factsL41–41

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

  1. L41
    exact hd_witness_witness_left
13Separate the logical casesL42–42

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

  1. L42
    split
14Use earlier factsL43–43

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

  1. L43
    exact hd_witness_witness_right
15Separate the logical casesL44–44

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

  1. L44
    split
16Use earlier factsL45–45

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

  1. L45
    exact ha_witness
17Separate the logical casesL46–46

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

  1. L46
    split
18Use earlier factsL47–48

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

  1. L47
    exact hb_witness
  2. L48
    exact hz_witness

Library-wide reading audit

Original exact command ledger · 48 lines
  1. 0001intro F
  2. 0002intro G
  3. 0003intro n
  4. 0004intro k
  5. 0005intro hF
  6. 0006intro hG
  7. 0007intro hn
  8. 0008have hd : exists i j. ((k=n*i+j) /\ (exists pvs_gap_flat_division. pvs_gap_flat_division + S (j) = (n)))
  9. 0009specialize division_remainder_exists (n)
  10. 0010specialize division_remainder_exists (k)
  11. 0011apply division_remainder_exists
  12. 0012exact hn
  13. 0013cases hd
  14. 0014cases hd_witness
  15. 0015cases hd_witness_witness
  16. 0016have ha : exists a. (exists dst_positive_code_flat_first dst_positive_scale_flat_first dst_negative_code_flat_first dst_negative_scale_flat_first dst_positive_flat_first dst_negative_flat_first. (((F) = (((((dst_positive_code_flat_first) + (dst_positive_scale_flat_first)) * S ((dst_positive_code_flat_first) + (dst_positive_scale_flat_first)) + ((dst_positive_scale_flat_first) + (dst_positive_scale_flat_first))) + (((dst_negative_code_flat_first) + (dst_negative_scale_flat_first)) * S ((dst_negative_code_flat_first) + (dst_negative_scale_flat_first)) + ((dst_negative_scale_flat_first) + (dst_negative_scale_flat_first)))) * S ((((dst_positive_code_flat_first) + (dst_positive_scale_flat_first)) * S ((dst_positive_code_flat_first) + (dst_positive_scale_flat_first)) + ((dst_positive_scale_flat_first) + (dst_positive_scale_flat_first))) + (((dst_negative_code_flat_first) + (dst_negative_scale_flat_first)) * S ((dst_negative_code_flat_first) + (dst_negative_scale_flat_first)) + ((dst_negative_scale_flat_first) + (dst_negative_scale_flat_first)))) + ((((dst_negative_code_flat_first) + (dst_negative_scale_flat_first)) * S ((dst_negative_code_flat_first) + (dst_negative_scale_flat_first)) + ((dst_negative_scale_flat_first) + (dst_negative_scale_flat_first))) + (((dst_negative_code_flat_first) + (dst_negative_scale_flat_first)) * S ((dst_negative_code_flat_first) + (dst_negative_scale_flat_first)) + ((dst_negative_scale_flat_first) + (dst_negative_scale_flat_first)))))) /\ (((((exists ff_h_pvs_flat_firstpositive. ff_h_pvs_flat_firstpositive + S (dst_positive_flat_first) = S ((S (x)) * dst_positive_scale_flat_first)) /\ exists ff_q_pvs_flat_firstpositive. dst_positive_code_flat_first = ff_q_pvs_flat_firstpositive * S ((S (x)) * dst_positive_scale_flat_first) + (dst_positive_flat_first))) /\ (((((exists ff_h_pvs_flat_firstnegative. ff_h_pvs_flat_firstnegative + S (dst_negative_flat_first) = S ((S (x)) * dst_negative_scale_flat_first)) /\ exists ff_q_pvs_flat_firstnegative. dst_negative_code_flat_first = ff_q_pvs_flat_firstnegative * S ((S (x)) * dst_negative_scale_flat_first) + (dst_negative_flat_first))) /\ (exists ge_balance_positive_flat_firstvalue ge_balance_negative_flat_firstvalue. (((((a) = 2 * (ge_balance_positive_flat_firstvalue) /\ (ge_balance_negative_flat_firstvalue) = 0) \/ exists ge_signed_half_flat_firstvaluedecode. (((a) = 2 * ge_signed_half_flat_firstvaluedecode + 1 /\ (ge_balance_positive_flat_firstvalue) = 0) /\ (ge_balance_negative_flat_firstvalue) = S ge_signed_half_flat_firstvaluedecode))) /\ ((dst_positive_flat_first) + ge_balance_negative_flat_firstvalue = (dst_negative_flat_first) + ge_balance_positive_flat_firstvalue)))))))))
  17. 0017specialize signed_table_lookup_any (0)
  18. 0018specialize signed_table_lookup_any (F)
  19. 0019specialize signed_table_lookup_any (x)
  20. 0020apply signed_table_lookup_any
  21. 0021exact hF
  22. 0022cases ha
  23. 0023have hb : exists b. (exists dst_positive_code_flat_second dst_positive_scale_flat_second dst_negative_code_flat_second dst_negative_scale_flat_second dst_positive_flat_second dst_negative_flat_second. (((G) = (((((dst_positive_code_flat_second) + (dst_positive_scale_flat_second)) * S ((dst_positive_code_flat_second) + (dst_positive_scale_flat_second)) + ((dst_positive_scale_flat_second) + (dst_positive_scale_flat_second))) + (((dst_negative_code_flat_second) + (dst_negative_scale_flat_second)) * S ((dst_negative_code_flat_second) + (dst_negative_scale_flat_second)) + ((dst_negative_scale_flat_second) + (dst_negative_scale_flat_second)))) * S ((((dst_positive_code_flat_second) + (dst_positive_scale_flat_second)) * S ((dst_positive_code_flat_second) + (dst_positive_scale_flat_second)) + ((dst_positive_scale_flat_second) + (dst_positive_scale_flat_second))) + (((dst_negative_code_flat_second) + (dst_negative_scale_flat_second)) * S ((dst_negative_code_flat_second) + (dst_negative_scale_flat_second)) + ((dst_negative_scale_flat_second) + (dst_negative_scale_flat_second)))) + ((((dst_negative_code_flat_second) + (dst_negative_scale_flat_second)) * S ((dst_negative_code_flat_second) + (dst_negative_scale_flat_second)) + ((dst_negative_scale_flat_second) + (dst_negative_scale_flat_second))) + (((dst_negative_code_flat_second) + (dst_negative_scale_flat_second)) * S ((dst_negative_code_flat_second) + (dst_negative_scale_flat_second)) + ((dst_negative_scale_flat_second) + (dst_negative_scale_flat_second)))))) /\ (((((exists ff_h_pvs_flat_secondpositive. ff_h_pvs_flat_secondpositive + S (dst_positive_flat_second) = S ((S (x1)) * dst_positive_scale_flat_second)) /\ exists ff_q_pvs_flat_secondpositive. dst_positive_code_flat_second = ff_q_pvs_flat_secondpositive * S ((S (x1)) * dst_positive_scale_flat_second) + (dst_positive_flat_second))) /\ (((((exists ff_h_pvs_flat_secondnegative. ff_h_pvs_flat_secondnegative + S (dst_negative_flat_second) = S ((S (x1)) * dst_negative_scale_flat_second)) /\ exists ff_q_pvs_flat_secondnegative. dst_negative_code_flat_second = ff_q_pvs_flat_secondnegative * S ((S (x1)) * dst_negative_scale_flat_second) + (dst_negative_flat_second))) /\ (exists ge_balance_positive_flat_secondvalue ge_balance_negative_flat_secondvalue. (((((b) = 2 * (ge_balance_positive_flat_secondvalue) /\ (ge_balance_negative_flat_secondvalue) = 0) \/ exists ge_signed_half_flat_secondvaluedecode. (((b) = 2 * ge_signed_half_flat_secondvaluedecode + 1 /\ (ge_balance_positive_flat_secondvalue) = 0) /\ (ge_balance_negative_flat_secondvalue) = S ge_signed_half_flat_secondvaluedecode))) /\ ((dst_positive_flat_second) + ge_balance_negative_flat_secondvalue = (dst_negative_flat_second) + ge_balance_positive_flat_secondvalue)))))))))
  24. 0024specialize signed_table_lookup_any (0)
  25. 0025specialize signed_table_lookup_any (G)
  26. 0026specialize signed_table_lookup_any (x1)
  27. 0027apply signed_table_lookup_any
  28. 0028exact hG
  29. 0029cases hb
  30. 0030have hz : exists z. (exists sto_ap_flat_product sto_an_flat_product sto_bp_flat_product sto_bn_flat_product sto_cp_flat_product sto_cn_flat_product. (((((x2) = 2 * (sto_ap_flat_product) /\ (sto_an_flat_product) = 0) \/ exists ge_signed_half_flat_productleft. (((x2) = 2 * ge_signed_half_flat_productleft + 1 /\ (sto_ap_flat_product) = 0) /\ (sto_an_flat_product) = S ge_signed_half_flat_productleft))) /\ ((((((x3) = 2 * (sto_bp_flat_product) /\ (sto_bn_flat_product) = 0) \/ exists ge_signed_half_flat_productright. (((x3) = 2 * ge_signed_half_flat_productright + 1 /\ (sto_bp_flat_product) = 0) /\ (sto_bn_flat_product) = S ge_signed_half_flat_productright))) /\ ((((((z) = 2 * (sto_cp_flat_product) /\ (sto_cn_flat_product) = 0) \/ exists ge_signed_half_flat_productoutput. (((z) = 2 * ge_signed_half_flat_productoutput + 1 /\ (sto_cp_flat_product) = 0) /\ (sto_cn_flat_product) = S ge_signed_half_flat_productoutput))) /\ ((sto_ap_flat_product * sto_bp_flat_product + sto_an_flat_product * sto_bn_flat_product) + sto_cn_flat_product = (sto_ap_flat_product * sto_bn_flat_product + sto_an_flat_product * sto_bp_flat_product) + sto_cp_flat_product)))))))
  31. 0031specialize signed_mul_total (x2)
  32. 0032specialize signed_mul_total (x3)
  33. 0033apply signed_mul_total
  34. 0034cases hz
  35. 0035exists x4
  36. 0036exists x
  37. 0037exists x1
  38. 0038exists x2
  39. 0039exists x3
  40. 0040split
  41. 0041exact hd_witness_witness_left
  42. 0042split
  43. 0043exact hd_witness_witness_right
  44. 0044split
  45. 0045exact ha_witness
  46. 0046split
  47. 0047exact hb_witness
  48. 0048exact hz_witness