SS001B

divisor_signed_table_reindex_exists

Public research checkpoint, not admitted to Alpha or Stable. Alpha v30 remains 3222 checked-use theorems; Stable remains 432. The on-demand Alpha Lean service does not yet expose these checkpoint theorems; their independently checked literal bundles and unchanged sources are available below.

Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; not Stable

Any actual finite signed table admits a genuinely beta-coded pullback along an actual beta map, with its new table code constructed.

Exact expanded first-order arithmetic statement

forall N F r s l. (exists dst_positive_code_constructed_source dst_positive_scale_constructed_source dst_negative_code_constructed_source dst_negative_scale_constructed_source. (((F) = (((((dst_positive_code_constructed_source) + (dst_positive_scale_constructed_source)) * S ((dst_positive_code_constructed_source) + (dst_positive_scale_constructed_source)) + ((dst_positive_scale_constructed_source) + (dst_positive_scale_constructed_source))) + (((dst_negative_code_constructed_source) + (dst_negative_scale_constructed_source)) * S ((dst_negative_code_constructed_source) + (dst_negative_scale_constructed_source)) + ((dst_negative_scale_constructed_source) + (dst_negative_scale_constructed_source)))) * S ((((dst_positive_code_constructed_source) + (dst_positive_scale_constructed_source)) * S ((dst_positive_code_constructed_source) + (dst_positive_scale_constructed_source)) + ((dst_positive_scale_constructed_source) + (dst_positive_scale_constructed_source))) + (((dst_negative_code_constructed_source) + (dst_negative_scale_constructed_source)) * S ((dst_negative_code_constructed_source) + (dst_negative_scale_constructed_source)) + ((dst_negative_scale_constructed_source) + (dst_negative_scale_constructed_source)))) + ((((dst_negative_code_constructed_source) + (dst_negative_scale_constructed_source)) * S ((dst_negative_code_constructed_source) + (dst_negative_scale_constructed_source)) + ((dst_negative_scale_constructed_source) + (dst_negative_scale_constructed_source))) + (((dst_negative_code_constructed_source) + (dst_negative_scale_constructed_source)) * S ((dst_negative_code_constructed_source) + (dst_negative_scale_constructed_source)) + ((dst_negative_scale_constructed_source) + (dst_negative_scale_constructed_source)))))) /\ (forall dst_index_constructed_source. (exists pvs_le_gap_constructed_sourcedomain. pvs_le_gap_constructed_sourcedomain + (dst_index_constructed_source) = (N)) -> exists dst_positive_constructed_source dst_negative_constructed_source dst_value_constructed_source. ((((exists ff_h_pvs_constructed_sourceentrypositive. ff_h_pvs_constructed_sourceentrypositive + S (dst_positive_constructed_source) = S ((S (dst_index_constructed_source)) * dst_positive_scale_constructed_source)) /\ exists ff_q_pvs_constructed_sourceentrypositive. dst_positive_code_constructed_source = ff_q_pvs_constructed_sourceentrypositive * S ((S (dst_index_constructed_source)) * dst_positive_scale_constructed_source) + (dst_positive_constructed_source))) /\ (((((exists ff_h_pvs_constructed_sourceentrynegative. ff_h_pvs_constructed_sourceentrynegative + S (dst_negative_constructed_source) = S ((S (dst_index_constructed_source)) * dst_negative_scale_constructed_source)) /\ exists ff_q_pvs_constructed_sourceentrynegative. dst_negative_code_constructed_source = ff_q_pvs_constructed_sourceentrynegative * S ((S (dst_index_constructed_source)) * dst_negative_scale_constructed_source) + (dst_negative_constructed_source))) /\ (exists ge_balance_positive_constructed_sourceentryvalue ge_balance_negative_constructed_sourceentryvalue. (((((dst_value_constructed_source) = 2 * (ge_balance_positive_constructed_sourceentryvalue) /\ (ge_balance_negative_constructed_sourceentryvalue) = 0) \/ exists ge_signed_half_constructed_sourceentryvaluedecode. (((dst_value_constructed_source) = 2 * ge_signed_half_constructed_sourceentryvaluedecode + 1 /\ (ge_balance_positive_constructed_sourceentryvalue) = 0) /\ (ge_balance_negative_constructed_sourceentryvalue) = S ge_signed_half_constructed_sourceentryvaluedecode))) /\ ((dst_positive_constructed_source) + ge_balance_negative_constructed_sourceentryvalue = (dst_negative_constructed_source) + ge_balance_positive_constructed_sourceentryvalue))))))))) -> exists G. (exists dst_positive_code_constructed_target dst_positive_scale_constructed_target dst_negative_code_constructed_target dst_negative_scale_constructed_target. (((G) = (((((dst_positive_code_constructed_target) + (dst_positive_scale_constructed_target)) * S ((dst_positive_code_constructed_target) + (dst_positive_scale_constructed_target)) + ((dst_positive_scale_constructed_target) + (dst_positive_scale_constructed_target))) + (((dst_negative_code_constructed_target) + (dst_negative_scale_constructed_target)) * S ((dst_negative_code_constructed_target) + (dst_negative_scale_constructed_target)) + ((dst_negative_scale_constructed_target) + (dst_negative_scale_constructed_target)))) * S ((((dst_positive_code_constructed_target) + (dst_positive_scale_constructed_target)) * S ((dst_positive_code_constructed_target) + (dst_positive_scale_constructed_target)) + ((dst_positive_scale_constructed_target) + (dst_positive_scale_constructed_target))) + (((dst_negative_code_constructed_target) + (dst_negative_scale_constructed_target)) * S ((dst_negative_code_constructed_target) + (dst_negative_scale_constructed_target)) + ((dst_negative_scale_constructed_target) + (dst_negative_scale_constructed_target)))) + ((((dst_negative_code_constructed_target) + (dst_negative_scale_constructed_target)) * S ((dst_negative_code_constructed_target) + (dst_negative_scale_constructed_target)) + ((dst_negative_scale_constructed_target) + (dst_negative_scale_constructed_target))) + (((dst_negative_code_constructed_target) + (dst_negative_scale_constructed_target)) * S ((dst_negative_code_constructed_target) + (dst_negative_scale_constructed_target)) + ((dst_negative_scale_constructed_target) + (dst_negative_scale_constructed_target)))))) /\ (forall dst_index_constructed_target. (exists pvs_le_gap_constructed_targetdomain. pvs_le_gap_constructed_targetdomain + (dst_index_constructed_target) = (l)) -> exists dst_positive_constructed_target dst_negative_constructed_target dst_value_constructed_target. ((((exists ff_h_pvs_constructed_targetentrypositive. ff_h_pvs_constructed_targetentrypositive + S (dst_positive_constructed_target) = S ((S (dst_index_constructed_target)) * dst_positive_scale_constructed_target)) /\ exists ff_q_pvs_constructed_targetentrypositive. dst_positive_code_constructed_target = ff_q_pvs_constructed_targetentrypositive * S ((S (dst_index_constructed_target)) * dst_positive_scale_constructed_target) + (dst_positive_constructed_target))) /\ (((((exists ff_h_pvs_constructed_targetentrynegative. ff_h_pvs_constructed_targetentrynegative + S (dst_negative_constructed_target) = S ((S (dst_index_constructed_target)) * dst_negative_scale_constructed_target)) /\ exists ff_q_pvs_constructed_targetentrynegative. dst_negative_code_constructed_target = ff_q_pvs_constructed_targetentrynegative * S ((S (dst_index_constructed_target)) * dst_negative_scale_constructed_target) + (dst_negative_constructed_target))) /\ (exists ge_balance_positive_constructed_targetentryvalue ge_balance_negative_constructed_targetentryvalue. (((((dst_value_constructed_target) = 2 * (ge_balance_positive_constructed_targetentryvalue) /\ (ge_balance_negative_constructed_targetentryvalue) = 0) \/ exists ge_signed_half_constructed_targetentryvaluedecode. (((dst_value_constructed_target) = 2 * ge_signed_half_constructed_targetentryvaluedecode + 1 /\ (ge_balance_positive_constructed_targetentryvalue) = 0) /\ (ge_balance_negative_constructed_targetentryvalue) = S ge_signed_half_constructed_targetentryvaluedecode))) /\ ((dst_positive_constructed_target) + ge_balance_negative_constructed_targetentryvalue = (dst_negative_constructed_target) + ge_balance_positive_constructed_targetentryvalue))))))))) /\ (forall dsr_index_constructed_reindex dsr_image_constructed_reindex dsr_value_constructed_reindex. (exists pvs_gap_constructed_reindexbound. pvs_gap_constructed_reindexbound + S (dsr_index_constructed_reindex) = (l)) -> (((exists ff_h_pvs_constructed_reindexmap. ff_h_pvs_constructed_reindexmap + S (dsr_image_constructed_reindex) = S ((S (dsr_index_constructed_reindex)) * s)) /\ exists ff_q_pvs_constructed_reindexmap. r = ff_q_pvs_constructed_reindexmap * S ((S (dsr_index_constructed_reindex)) * s) + (dsr_image_constructed_reindex))) -> (exists dst_positive_code_constructed_reindexsource dst_positive_scale_constructed_reindexsource dst_negative_code_constructed_reindexsource dst_negative_scale_constructed_reindexsource dst_positive_constructed_reindexsource dst_negative_constructed_reindexsource. (((F) = (((((dst_positive_code_constructed_reindexsource) + (dst_positive_scale_constructed_reindexsource)) * S ((dst_positive_code_constructed_reindexsource) + (dst_positive_scale_constructed_reindexsource)) + ((dst_positive_scale_constructed_reindexsource) + (dst_positive_scale_constructed_reindexsource))) + (((dst_negative_code_constructed_reindexsource) + (dst_negative_scale_constructed_reindexsource)) * S ((dst_negative_code_constructed_reindexsource) + (dst_negative_scale_constructed_reindexsource)) + ((dst_negative_scale_constructed_reindexsource) + (dst_negative_scale_constructed_reindexsource)))) * S ((((dst_positive_code_constructed_reindexsource) + (dst_positive_scale_constructed_reindexsource)) * S ((dst_positive_code_constructed_reindexsource) + (dst_positive_scale_constructed_reindexsource)) + ((dst_positive_scale_constructed_reindexsource) + (dst_positive_scale_constructed_reindexsource))) + (((dst_negative_code_constructed_reindexsource) + (dst_negative_scale_constructed_reindexsource)) * S ((dst_negative_code_constructed_reindexsource) + (dst_negative_scale_constructed_reindexsource)) + ((dst_negative_scale_constructed_reindexsource) + (dst_negative_scale_constructed_reindexsource)))) + ((((dst_negative_code_constructed_reindexsource) + (dst_negative_scale_constructed_reindexsource)) * S ((dst_negative_code_constructed_reindexsource) + (dst_negative_scale_constructed_reindexsource)) + ((dst_negative_scale_constructed_reindexsource) + (dst_negative_scale_constructed_reindexsource))) + (((dst_negative_code_constructed_reindexsource) + (dst_negative_scale_constructed_reindexsource)) * S ((dst_negative_code_constructed_reindexsource) + (dst_negative_scale_constructed_reindexsource)) + ((dst_negative_scale_constructed_reindexsource) + (dst_negative_scale_constructed_reindexsource)))))) /\ (((((exists ff_h_pvs_constructed_reindexsourcepositive. ff_h_pvs_constructed_reindexsourcepositive + S (dst_positive_constructed_reindexsource) = S ((S (dsr_image_constructed_reindex)) * dst_positive_scale_constructed_reindexsource)) /\ exists ff_q_pvs_constructed_reindexsourcepositive. dst_positive_code_constructed_reindexsource = ff_q_pvs_constructed_reindexsourcepositive * S ((S (dsr_image_constructed_reindex)) * dst_positive_scale_constructed_reindexsource) + (dst_positive_constructed_reindexsource))) /\ (((((exists ff_h_pvs_constructed_reindexsourcenegative. ff_h_pvs_constructed_reindexsourcenegative + S (dst_negative_constructed_reindexsource) = S ((S (dsr_image_constructed_reindex)) * dst_negative_scale_constructed_reindexsource)) /\ exists ff_q_pvs_constructed_reindexsourcenegative. dst_negative_code_constructed_reindexsource = ff_q_pvs_constructed_reindexsourcenegative * S ((S (dsr_image_constructed_reindex)) * dst_negative_scale_constructed_reindexsource) + (dst_negative_constructed_reindexsource))) /\ (exists ge_balance_positive_constructed_reindexsourcevalue ge_balance_negative_constructed_reindexsourcevalue. (((((dsr_value_constructed_reindex) = 2 * (ge_balance_positive_constructed_reindexsourcevalue) /\ (ge_balance_negative_constructed_reindexsourcevalue) = 0) \/ exists ge_signed_half_constructed_reindexsourcevaluedecode. (((dsr_value_constructed_reindex) = 2 * ge_signed_half_constructed_reindexsourcevaluedecode + 1 /\ (ge_balance_positive_constructed_reindexsourcevalue) = 0) /\ (ge_balance_negative_constructed_reindexsourcevalue) = S ge_signed_half_constructed_reindexsourcevaluedecode))) /\ ((dst_positive_constructed_reindexsource) + ge_balance_negative_constructed_reindexsourcevalue = (dst_negative_constructed_reindexsource) + ge_balance_positive_constructed_reindexsourcevalue))))))))) -> (exists dst_positive_code_constructed_reindextarget dst_positive_scale_constructed_reindextarget dst_negative_code_constructed_reindextarget dst_negative_scale_constructed_reindextarget dst_positive_constructed_reindextarget dst_negative_constructed_reindextarget. (((G) = (((((dst_positive_code_constructed_reindextarget) + (dst_positive_scale_constructed_reindextarget)) * S ((dst_positive_code_constructed_reindextarget) + (dst_positive_scale_constructed_reindextarget)) + ((dst_positive_scale_constructed_reindextarget) + (dst_positive_scale_constructed_reindextarget))) + (((dst_negative_code_constructed_reindextarget) + (dst_negative_scale_constructed_reindextarget)) * S ((dst_negative_code_constructed_reindextarget) + (dst_negative_scale_constructed_reindextarget)) + ((dst_negative_scale_constructed_reindextarget) + (dst_negative_scale_constructed_reindextarget)))) * S ((((dst_positive_code_constructed_reindextarget) + (dst_positive_scale_constructed_reindextarget)) * S ((dst_positive_code_constructed_reindextarget) + (dst_positive_scale_constructed_reindextarget)) + ((dst_positive_scale_constructed_reindextarget) + (dst_positive_scale_constructed_reindextarget))) + (((dst_negative_code_constructed_reindextarget) + (dst_negative_scale_constructed_reindextarget)) * S ((dst_negative_code_constructed_reindextarget) + (dst_negative_scale_constructed_reindextarget)) + ((dst_negative_scale_constructed_reindextarget) + (dst_negative_scale_constructed_reindextarget)))) + ((((dst_negative_code_constructed_reindextarget) + (dst_negative_scale_constructed_reindextarget)) * S ((dst_negative_code_constructed_reindextarget) + (dst_negative_scale_constructed_reindextarget)) + ((dst_negative_scale_constructed_reindextarget) + (dst_negative_scale_constructed_reindextarget))) + (((dst_negative_code_constructed_reindextarget) + (dst_negative_scale_constructed_reindextarget)) * S ((dst_negative_code_constructed_reindextarget) + (dst_negative_scale_constructed_reindextarget)) + ((dst_negative_scale_constructed_reindextarget) + (dst_negative_scale_constructed_reindextarget)))))) /\ (((((exists ff_h_pvs_constructed_reindextargetpositive. ff_h_pvs_constructed_reindextargetpositive + S (dst_positive_constructed_reindextarget) = S ((S (dsr_index_constructed_reindex)) * dst_positive_scale_constructed_reindextarget)) /\ exists ff_q_pvs_constructed_reindextargetpositive. dst_positive_code_constructed_reindextarget = ff_q_pvs_constructed_reindextargetpositive * S ((S (dsr_index_constructed_reindex)) * dst_positive_scale_constructed_reindextarget) + (dst_positive_constructed_reindextarget))) /\ (((((exists ff_h_pvs_constructed_reindextargetnegative. ff_h_pvs_constructed_reindextargetnegative + S (dst_negative_constructed_reindextarget) = S ((S (dsr_index_constructed_reindex)) * dst_negative_scale_constructed_reindextarget)) /\ exists ff_q_pvs_constructed_reindextargetnegative. dst_negative_code_constructed_reindextarget = ff_q_pvs_constructed_reindextargetnegative * S ((S (dsr_index_constructed_reindex)) * dst_negative_scale_constructed_reindextarget) + (dst_negative_constructed_reindextarget))) /\ (exists ge_balance_positive_constructed_reindextargetvalue ge_balance_negative_constructed_reindextargetvalue. (((((dsr_value_constructed_reindex) = 2 * (ge_balance_positive_constructed_reindextargetvalue) /\ (ge_balance_negative_constructed_reindextargetvalue) = 0) \/ exists ge_signed_half_constructed_reindextargetvaluedecode. (((dsr_value_constructed_reindex) = 2 * ge_signed_half_constructed_reindextargetvaluedecode + 1 /\ (ge_balance_positive_constructed_reindextargetvalue) = 0) /\ (ge_balance_negative_constructed_reindextargetvalue) = S ge_signed_half_constructed_reindextargetvaluedecode))) /\ ((dst_positive_constructed_reindextarget) + ge_balance_negative_constructed_reindextargetvalue = (dst_negative_constructed_reindextarget) + ge_balance_positive_constructed_reindextargetvalue))))))))))

Constructive proof overview

Generated structural guide

Any actual finite signed table admits a genuinely beta-coded pullback along an actual beta map, with its new table code constructed.

The unchanged tactic script uses 4 declared prerequisites and contains 55 exact native proof lines.

Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; not Stable

Proof neighborhood

Direct dependencies

SS0005 divisor_signed_table_components SS0019 divisor_signed_table_reindex_data_exists SS0003 divisor_signed_table_from_components SS001A divisor_signed_table_reindex_from_components

Direct dependents

none

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. The literal dependency-closed bundle is checked by original HA and the independently compiled Lean verifier. Public delivery grants no Alpha checked-use authority or Stable membership.

Read the argument

Proof checkpoints

55 script commands · 13 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.

Named ingredients (4)
divisor signed table componentsdivisor signed table reindex data existsdivisor signed table from componentsdivisor signed table reindex from components

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

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

  1. L1
    intro N
  2. L2
    intro F
  3. L3
    intro r
  4. L4
    intro s
  5. L5
    intro l
  6. L6
    intro ht
02Establish hrepL7–11

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

  1. L7
    have hrep : exists pb pc nb nc. ((F) = (((((pb) + (pc)) * S ((pb) + (pc)) + ((pc) + (pc))) + (((nb) + (nc)) * S ((nb) + (nc)) + ((nc) + (nc)))) * S ((((pb) + (pc)) * S ((pb) + (pc)) + ((pc) + (pc))) + (((nb) + (nc)) * S ((nb) + (nc)) + ((nc) + (nc)))) + ((((nb) + (nc)) * S ((nb) + (nc)) + ((nc) + (nc))) + (((nb) + (nc)) * S ((nb) + (nc)) + ((nc) + (nc))))))
  2. L8
    specialize divisor_signed_table_components (N)
  3. L9
    specialize divisor_signed_table_components (F)
  4. L10
    apply divisor_signed_table_components
  5. L11
    exact ht
03Separate the logical casesL12–15

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

  1. L12
    cases hrep
  2. L13
    cases hrep_witness
  3. L14
    cases hrep_witness_witness
  4. L15
    cases hrep_witness_witness_witness
04Establish hdataL16–24

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

  1. L16
    have hdata : ∃ qb. ∃ qc. ∃ mb. ∃ mc. (∀ y. ∀ z. ∀ n. Lt(y,l) → BetaAt(r,s,y,z) → BetaAt(x,x1,z,n) → BetaAt(qb,qc,y,n)) ∧ (∀ y. ∀ z. ∀ n. Lt(y,l) → BetaAt(r,s,y,z) → BetaAt(x2,x3,z,n) → BetaAt(mb,mc,y,n))Definitions: LtBetaAt
  2. L17
    specialize divisor_signed_table_reindex_data_exists (x)
  3. L18
    specialize divisor_signed_table_reindex_data_exists (x1)
  4. L19
    specialize divisor_signed_table_reindex_data_exists (x2)
  5. L20
    specialize divisor_signed_table_reindex_data_exists (x3)
  6. L21
    specialize divisor_signed_table_reindex_data_exists (r)
  7. L22
    specialize divisor_signed_table_reindex_data_exists (s)
  8. L23
    specialize divisor_signed_table_reindex_data_exists (l)
  9. L24
    apply divisor_signed_table_reindex_data_exists
05Separate the logical casesL25–28

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

  1. L25
    cases hdata
  2. L26
    cases hdata_witness
  3. L27
    cases hdata_witness_witness
  4. L28
    cases hdata_witness_witness_witness
06Construct an explicit witnessL29–29

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

  1. L29
    exists ((((x4) + (x5)) * S ((x4) + (x5)) + ((x5) + (x5))) + (((x6) + (x7)) * S ((x6) + (x7)) + ((x7) + (x7)))) * S ((((x4) + (x5)) * S ((x4) + (x5)) + ((x5) + (x5))) + (((x6) + (x7)) * S ((x6) + (x7)) + ((x7) + (x7)))) + ((((x6) + (x7)) * S ((x6) + (x7)) + ((x7) + (x7))) + (((x6) + (x7)) * S ((x6) + (x7)) + ((x7) + (x7))))
07Separate the logical casesL30–30

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

  1. L30
    split
08Use earlier factsL31–37

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

  1. L31
    specialize divisor_signed_table_from_components (l)
  2. L32
    specialize divisor_signed_table_from_components (((((x4) + (x5)) * S ((x4) + (x5)) + ((x5) + (x5))) + (((x6) + (x7)) * S ((x6) + (x7)) + ((x7) + (x7)))) * S ((((x4) + (x5)) * S ((x4) + (x5)) + ((x5) + (x5))) + (((x6) + (x7)) * S ((x6) + (x7)) + ((x7) + (x7)))) + ((((x6) + (x7)) * S ((x6) + (x7)) + ((x7) + (x7))) + (((x6) + (x7)) * S ((x6) + (x7)) + ((x7) + (x7)))))
  3. L33
    specialize divisor_signed_table_from_components (x4)
  4. L34
    specialize divisor_signed_table_from_components (x5)
  5. L35
    specialize divisor_signed_table_from_components (x6)
  6. L36
    specialize divisor_signed_table_from_components (x7)
  7. L37
    apply divisor_signed_table_from_components
09Calculate and transport equalitiesL38–38

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

  1. L38
    refl
10Use earlier factsL39–48

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

  1. L39
    specialize divisor_signed_table_reindex_from_components (F)
  2. L40
    specialize divisor_signed_table_reindex_from_components (((((x4) + (x5)) * S ((x4) + (x5)) + ((x5) + (x5))) + (((x6) + (x7)) * S ((x6) + (x7)) + ((x7) + (x7)))) * S ((((x4) + (x5)) * S ((x4) + (x5)) + ((x5) + (x5))) + (((x6) + (x7)) * S ((x6) + (x7)) + ((x7) + (x7)))) + ((((x6) + (x7)) * S ((x6) + (x7)) + ((x7) + (x7))) + (((x6) + (x7)) * S ((x6) + (x7)) + ((x7) + (x7)))))
  3. L41
    specialize divisor_signed_table_reindex_from_components (x)
  4. L42
    specialize divisor_signed_table_reindex_from_components (x1)
  5. L43
    specialize divisor_signed_table_reindex_from_components (x2)
  6. L44
    specialize divisor_signed_table_reindex_from_components (x3)
  7. L45
    specialize divisor_signed_table_reindex_from_components (x4)
  8. L46
    specialize divisor_signed_table_reindex_from_components (x5)
  9. L47
    specialize divisor_signed_table_reindex_from_components (x6)
  10. L48
    specialize divisor_signed_table_reindex_from_components (x7)
11Use earlier factsL49–53

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

  1. L49
    specialize divisor_signed_table_reindex_from_components (r)
  2. L50
    specialize divisor_signed_table_reindex_from_components (s)
  3. L51
    specialize divisor_signed_table_reindex_from_components (l)
  4. L52
    apply divisor_signed_table_reindex_from_components
  5. L53
    exact hrep_witness_witness_witness_witness
12Calculate and transport equalitiesL54–54

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

  1. L54
    refl
13Use earlier factsL55–55

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

  1. L55
    exact hdata_witness_witness_witness_witness

Library-wide reading audit

Original exact command ledger · 55 lines
  1. 0001intro N
  2. 0002intro F
  3. 0003intro r
  4. 0004intro s
  5. 0005intro l
  6. 0006intro ht
  7. 0007have hrep : exists pb pc nb nc. ((F) = (((((pb) + (pc)) * S ((pb) + (pc)) + ((pc) + (pc))) + (((nb) + (nc)) * S ((nb) + (nc)) + ((nc) + (nc)))) * S ((((pb) + (pc)) * S ((pb) + (pc)) + ((pc) + (pc))) + (((nb) + (nc)) * S ((nb) + (nc)) + ((nc) + (nc)))) + ((((nb) + (nc)) * S ((nb) + (nc)) + ((nc) + (nc))) + (((nb) + (nc)) * S ((nb) + (nc)) + ((nc) + (nc))))))
  8. 0008specialize divisor_signed_table_components (N)
  9. 0009specialize divisor_signed_table_components (F)
  10. 0010apply divisor_signed_table_components
  11. 0011exact ht
  12. 0012cases hrep
  13. 0013cases hrep_witness
  14. 0014cases hrep_witness_witness
  15. 0015cases hrep_witness_witness_witness
  16. 0016have hdata : exists qb qc mb mc. (((forall fms_i_construct_datapositive fms_j_construct_datapositive fms_v_construct_datapositive. (exists fms_gap_construct_datapositive. fms_gap_construct_datapositive + S (fms_i_construct_datapositive) = (l)) -> (((exists fs_h_fms_construct_datapositive_index. fs_h_fms_construct_datapositive_index + S (fms_j_construct_datapositive) = S ((S (fms_i_construct_datapositive)) * s)) /\ exists fs_q_fms_construct_datapositive_index. r = fs_q_fms_construct_datapositive_index * S ((S (fms_i_construct_datapositive)) * s) + (fms_j_construct_datapositive))) -> (((exists fs_h_fms_construct_datapositive_source. fs_h_fms_construct_datapositive_source + S (fms_v_construct_datapositive) = S ((S (fms_j_construct_datapositive)) * x1)) /\ exists fs_q_fms_construct_datapositive_source. x = fs_q_fms_construct_datapositive_source * S ((S (fms_j_construct_datapositive)) * x1) + (fms_v_construct_datapositive))) -> (((exists fs_h_fms_construct_datapositive_target. fs_h_fms_construct_datapositive_target + S (fms_v_construct_datapositive) = S ((S (fms_i_construct_datapositive)) * qc)) /\ exists fs_q_fms_construct_datapositive_target. qb = fs_q_fms_construct_datapositive_target * S ((S (fms_i_construct_datapositive)) * qc) + (fms_v_construct_datapositive)))) /\ (forall fms_i_construct_datanegative fms_j_construct_datanegative fms_v_construct_datanegative. (exists fms_gap_construct_datanegative. fms_gap_construct_datanegative + S (fms_i_construct_datanegative) = (l)) -> (((exists fs_h_fms_construct_datanegative_index. fs_h_fms_construct_datanegative_index + S (fms_j_construct_datanegative) = S ((S (fms_i_construct_datanegative)) * s)) /\ exists fs_q_fms_construct_datanegative_index. r = fs_q_fms_construct_datanegative_index * S ((S (fms_i_construct_datanegative)) * s) + (fms_j_construct_datanegative))) -> (((exists fs_h_fms_construct_datanegative_source. fs_h_fms_construct_datanegative_source + S (fms_v_construct_datanegative) = S ((S (fms_j_construct_datanegative)) * x3)) /\ exists fs_q_fms_construct_datanegative_source. x2 = fs_q_fms_construct_datanegative_source * S ((S (fms_j_construct_datanegative)) * x3) + (fms_v_construct_datanegative))) -> (((exists fs_h_fms_construct_datanegative_target. fs_h_fms_construct_datanegative_target + S (fms_v_construct_datanegative) = S ((S (fms_i_construct_datanegative)) * mc)) /\ exists fs_q_fms_construct_datanegative_target. mb = fs_q_fms_construct_datanegative_target * S ((S (fms_i_construct_datanegative)) * mc) + (fms_v_construct_datanegative))))))
  17. 0017specialize divisor_signed_table_reindex_data_exists (x)
  18. 0018specialize divisor_signed_table_reindex_data_exists (x1)
  19. 0019specialize divisor_signed_table_reindex_data_exists (x2)
  20. 0020specialize divisor_signed_table_reindex_data_exists (x3)
  21. 0021specialize divisor_signed_table_reindex_data_exists (r)
  22. 0022specialize divisor_signed_table_reindex_data_exists (s)
  23. 0023specialize divisor_signed_table_reindex_data_exists (l)
  24. 0024apply divisor_signed_table_reindex_data_exists
  25. 0025cases hdata
  26. 0026cases hdata_witness
  27. 0027cases hdata_witness_witness
  28. 0028cases hdata_witness_witness_witness
  29. 0029exists ((((x4) + (x5)) * S ((x4) + (x5)) + ((x5) + (x5))) + (((x6) + (x7)) * S ((x6) + (x7)) + ((x7) + (x7)))) * S ((((x4) + (x5)) * S ((x4) + (x5)) + ((x5) + (x5))) + (((x6) + (x7)) * S ((x6) + (x7)) + ((x7) + (x7)))) + ((((x6) + (x7)) * S ((x6) + (x7)) + ((x7) + (x7))) + (((x6) + (x7)) * S ((x6) + (x7)) + ((x7) + (x7))))
  30. 0030split
  31. 0031specialize divisor_signed_table_from_components (l)
  32. 0032specialize divisor_signed_table_from_components (((((x4) + (x5)) * S ((x4) + (x5)) + ((x5) + (x5))) + (((x6) + (x7)) * S ((x6) + (x7)) + ((x7) + (x7)))) * S ((((x4) + (x5)) * S ((x4) + (x5)) + ((x5) + (x5))) + (((x6) + (x7)) * S ((x6) + (x7)) + ((x7) + (x7)))) + ((((x6) + (x7)) * S ((x6) + (x7)) + ((x7) + (x7))) + (((x6) + (x7)) * S ((x6) + (x7)) + ((x7) + (x7)))))
  33. 0033specialize divisor_signed_table_from_components (x4)
  34. 0034specialize divisor_signed_table_from_components (x5)
  35. 0035specialize divisor_signed_table_from_components (x6)
  36. 0036specialize divisor_signed_table_from_components (x7)
  37. 0037apply divisor_signed_table_from_components
  38. 0038refl
  39. 0039specialize divisor_signed_table_reindex_from_components (F)
  40. 0040specialize divisor_signed_table_reindex_from_components (((((x4) + (x5)) * S ((x4) + (x5)) + ((x5) + (x5))) + (((x6) + (x7)) * S ((x6) + (x7)) + ((x7) + (x7)))) * S ((((x4) + (x5)) * S ((x4) + (x5)) + ((x5) + (x5))) + (((x6) + (x7)) * S ((x6) + (x7)) + ((x7) + (x7)))) + ((((x6) + (x7)) * S ((x6) + (x7)) + ((x7) + (x7))) + (((x6) + (x7)) * S ((x6) + (x7)) + ((x7) + (x7)))))
  41. 0041specialize divisor_signed_table_reindex_from_components (x)
  42. 0042specialize divisor_signed_table_reindex_from_components (x1)
  43. 0043specialize divisor_signed_table_reindex_from_components (x2)
  44. 0044specialize divisor_signed_table_reindex_from_components (x3)
  45. 0045specialize divisor_signed_table_reindex_from_components (x4)
  46. 0046specialize divisor_signed_table_reindex_from_components (x5)
  47. 0047specialize divisor_signed_table_reindex_from_components (x6)
  48. 0048specialize divisor_signed_table_reindex_from_components (x7)
  49. 0049specialize divisor_signed_table_reindex_from_components (r)
  50. 0050specialize divisor_signed_table_reindex_from_components (s)
  51. 0051specialize divisor_signed_table_reindex_from_components (l)
  52. 0052apply divisor_signed_table_reindex_from_components
  53. 0053exact hrep_witness_witness_witness_witness
  54. 0054refl
  55. 0055exact hdata_witness_witness_witness_witness