PX0040

beta_sum_pointwise_mod_add

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

Actual pointwise additive congruences lift by finite induction to the three actual Sum endpoints, for every modulus and also for the empty prefix.

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 p ab ac bb bc cb cc L A B C. (exists fs_u_pfc_distribution_sum_a fs_v_pfc_distribution_sum_a. ((((exists fs_h_pfc_distribution_sum_a_body_start. fs_h_pfc_distribution_sum_a_body_start + S (0) = S ((S (0)) * fs_v_pfc_distribution_sum_a)) /\ exists fs_q_pfc_distribution_sum_a_body_start. fs_u_pfc_distribution_sum_a = fs_q_pfc_distribution_sum_a_body_start * S ((S (0)) * fs_v_pfc_distribution_sum_a) + (0))) /\ ((((exists fs_h_pfc_distribution_sum_a_body_terminal. fs_h_pfc_distribution_sum_a_body_terminal + S (A) = S ((S (L)) * fs_v_pfc_distribution_sum_a)) /\ exists fs_q_pfc_distribution_sum_a_body_terminal. fs_u_pfc_distribution_sum_a = fs_q_pfc_distribution_sum_a_body_terminal * S ((S (L)) * fs_v_pfc_distribution_sum_a) + (A))) /\ forall fs_i_pfc_distribution_sum_a_body_steps. (exists fs_lt_pfc_distribution_sum_a_body_steps_bound. fs_lt_pfc_distribution_sum_a_body_steps_bound + S fs_i_pfc_distribution_sum_a_body_steps = L) -> exists fs_a_pfc_distribution_sum_a_body_steps fs_r_pfc_distribution_sum_a_body_steps fs_s_pfc_distribution_sum_a_body_steps. ((((exists fs_h_pfc_distribution_sum_a_body_steps_summand. fs_h_pfc_distribution_sum_a_body_steps_summand + S (fs_a_pfc_distribution_sum_a_body_steps) = S ((S (fs_i_pfc_distribution_sum_a_body_steps)) * ac)) /\ exists fs_q_pfc_distribution_sum_a_body_steps_summand. ab = fs_q_pfc_distribution_sum_a_body_steps_summand * S ((S (fs_i_pfc_distribution_sum_a_body_steps)) * ac) + (fs_a_pfc_distribution_sum_a_body_steps))) /\ ((((exists fs_h_pfc_distribution_sum_a_body_steps_partial. fs_h_pfc_distribution_sum_a_body_steps_partial + S (fs_r_pfc_distribution_sum_a_body_steps) = S ((S (fs_i_pfc_distribution_sum_a_body_steps)) * fs_v_pfc_distribution_sum_a)) /\ exists fs_q_pfc_distribution_sum_a_body_steps_partial. fs_u_pfc_distribution_sum_a = fs_q_pfc_distribution_sum_a_body_steps_partial * S ((S (fs_i_pfc_distribution_sum_a_body_steps)) * fs_v_pfc_distribution_sum_a) + (fs_r_pfc_distribution_sum_a_body_steps))) /\ ((((exists fs_h_pfc_distribution_sum_a_body_steps_successor. fs_h_pfc_distribution_sum_a_body_steps_successor + S (fs_s_pfc_distribution_sum_a_body_steps) = S ((S (S fs_i_pfc_distribution_sum_a_body_steps)) * fs_v_pfc_distribution_sum_a)) /\ exists fs_q_pfc_distribution_sum_a_body_steps_successor. fs_u_pfc_distribution_sum_a = fs_q_pfc_distribution_sum_a_body_steps_successor * S ((S (S fs_i_pfc_distribution_sum_a_body_steps)) * fs_v_pfc_distribution_sum_a) + (fs_s_pfc_distribution_sum_a_body_steps))) /\ fs_s_pfc_distribution_sum_a_body_steps = fs_r_pfc_distribution_sum_a_body_steps + fs_a_pfc_distribution_sum_a_body_steps)))))) -> (exists fs_u_pfc_distribution_sum_b fs_v_pfc_distribution_sum_b. ((((exists fs_h_pfc_distribution_sum_b_body_start. fs_h_pfc_distribution_sum_b_body_start + S (0) = S ((S (0)) * fs_v_pfc_distribution_sum_b)) /\ exists fs_q_pfc_distribution_sum_b_body_start. fs_u_pfc_distribution_sum_b = fs_q_pfc_distribution_sum_b_body_start * S ((S (0)) * fs_v_pfc_distribution_sum_b) + (0))) /\ ((((exists fs_h_pfc_distribution_sum_b_body_terminal. fs_h_pfc_distribution_sum_b_body_terminal + S (B) = S ((S (L)) * fs_v_pfc_distribution_sum_b)) /\ exists fs_q_pfc_distribution_sum_b_body_terminal. fs_u_pfc_distribution_sum_b = fs_q_pfc_distribution_sum_b_body_terminal * S ((S (L)) * fs_v_pfc_distribution_sum_b) + (B))) /\ forall fs_i_pfc_distribution_sum_b_body_steps. (exists fs_lt_pfc_distribution_sum_b_body_steps_bound. fs_lt_pfc_distribution_sum_b_body_steps_bound + S fs_i_pfc_distribution_sum_b_body_steps = L) -> exists fs_a_pfc_distribution_sum_b_body_steps fs_r_pfc_distribution_sum_b_body_steps fs_s_pfc_distribution_sum_b_body_steps. ((((exists fs_h_pfc_distribution_sum_b_body_steps_summand. fs_h_pfc_distribution_sum_b_body_steps_summand + S (fs_a_pfc_distribution_sum_b_body_steps) = S ((S (fs_i_pfc_distribution_sum_b_body_steps)) * bc)) /\ exists fs_q_pfc_distribution_sum_b_body_steps_summand. bb = fs_q_pfc_distribution_sum_b_body_steps_summand * S ((S (fs_i_pfc_distribution_sum_b_body_steps)) * bc) + (fs_a_pfc_distribution_sum_b_body_steps))) /\ ((((exists fs_h_pfc_distribution_sum_b_body_steps_partial. fs_h_pfc_distribution_sum_b_body_steps_partial + S (fs_r_pfc_distribution_sum_b_body_steps) = S ((S (fs_i_pfc_distribution_sum_b_body_steps)) * fs_v_pfc_distribution_sum_b)) /\ exists fs_q_pfc_distribution_sum_b_body_steps_partial. fs_u_pfc_distribution_sum_b = fs_q_pfc_distribution_sum_b_body_steps_partial * S ((S (fs_i_pfc_distribution_sum_b_body_steps)) * fs_v_pfc_distribution_sum_b) + (fs_r_pfc_distribution_sum_b_body_steps))) /\ ((((exists fs_h_pfc_distribution_sum_b_body_steps_successor. fs_h_pfc_distribution_sum_b_body_steps_successor + S (fs_s_pfc_distribution_sum_b_body_steps) = S ((S (S fs_i_pfc_distribution_sum_b_body_steps)) * fs_v_pfc_distribution_sum_b)) /\ exists fs_q_pfc_distribution_sum_b_body_steps_successor. fs_u_pfc_distribution_sum_b = fs_q_pfc_distribution_sum_b_body_steps_successor * S ((S (S fs_i_pfc_distribution_sum_b_body_steps)) * fs_v_pfc_distribution_sum_b) + (fs_s_pfc_distribution_sum_b_body_steps))) /\ fs_s_pfc_distribution_sum_b_body_steps = fs_r_pfc_distribution_sum_b_body_steps + fs_a_pfc_distribution_sum_b_body_steps)))))) -> (exists fs_u_pfc_distribution_sum_c fs_v_pfc_distribution_sum_c. ((((exists fs_h_pfc_distribution_sum_c_body_start. fs_h_pfc_distribution_sum_c_body_start + S (0) = S ((S (0)) * fs_v_pfc_distribution_sum_c)) /\ exists fs_q_pfc_distribution_sum_c_body_start. fs_u_pfc_distribution_sum_c = fs_q_pfc_distribution_sum_c_body_start * S ((S (0)) * fs_v_pfc_distribution_sum_c) + (0))) /\ ((((exists fs_h_pfc_distribution_sum_c_body_terminal. fs_h_pfc_distribution_sum_c_body_terminal + S (C) = S ((S (L)) * fs_v_pfc_distribution_sum_c)) /\ exists fs_q_pfc_distribution_sum_c_body_terminal. fs_u_pfc_distribution_sum_c = fs_q_pfc_distribution_sum_c_body_terminal * S ((S (L)) * fs_v_pfc_distribution_sum_c) + (C))) /\ forall fs_i_pfc_distribution_sum_c_body_steps. (exists fs_lt_pfc_distribution_sum_c_body_steps_bound. fs_lt_pfc_distribution_sum_c_body_steps_bound + S fs_i_pfc_distribution_sum_c_body_steps = L) -> exists fs_a_pfc_distribution_sum_c_body_steps fs_r_pfc_distribution_sum_c_body_steps fs_s_pfc_distribution_sum_c_body_steps. ((((exists fs_h_pfc_distribution_sum_c_body_steps_summand. fs_h_pfc_distribution_sum_c_body_steps_summand + S (fs_a_pfc_distribution_sum_c_body_steps) = S ((S (fs_i_pfc_distribution_sum_c_body_steps)) * cc)) /\ exists fs_q_pfc_distribution_sum_c_body_steps_summand. cb = fs_q_pfc_distribution_sum_c_body_steps_summand * S ((S (fs_i_pfc_distribution_sum_c_body_steps)) * cc) + (fs_a_pfc_distribution_sum_c_body_steps))) /\ ((((exists fs_h_pfc_distribution_sum_c_body_steps_partial. fs_h_pfc_distribution_sum_c_body_steps_partial + S (fs_r_pfc_distribution_sum_c_body_steps) = S ((S (fs_i_pfc_distribution_sum_c_body_steps)) * fs_v_pfc_distribution_sum_c)) /\ exists fs_q_pfc_distribution_sum_c_body_steps_partial. fs_u_pfc_distribution_sum_c = fs_q_pfc_distribution_sum_c_body_steps_partial * S ((S (fs_i_pfc_distribution_sum_c_body_steps)) * fs_v_pfc_distribution_sum_c) + (fs_r_pfc_distribution_sum_c_body_steps))) /\ ((((exists fs_h_pfc_distribution_sum_c_body_steps_successor. fs_h_pfc_distribution_sum_c_body_steps_successor + S (fs_s_pfc_distribution_sum_c_body_steps) = S ((S (S fs_i_pfc_distribution_sum_c_body_steps)) * fs_v_pfc_distribution_sum_c)) /\ exists fs_q_pfc_distribution_sum_c_body_steps_successor. fs_u_pfc_distribution_sum_c = fs_q_pfc_distribution_sum_c_body_steps_successor * S ((S (S fs_i_pfc_distribution_sum_c_body_steps)) * fs_v_pfc_distribution_sum_c) + (fs_s_pfc_distribution_sum_c_body_steps))) /\ fs_s_pfc_distribution_sum_c_body_steps = fs_r_pfc_distribution_sum_c_body_steps + fs_a_pfc_distribution_sum_c_body_steps)))))) -> (forall i a b c. (exists pfa_gap_distribution_sum_pointwise_bound. pfa_gap_distribution_sum_pointwise_bound + S (i) = (L)) -> (((exists ff_h_pfp_distribution_sum_pointwise_a. ff_h_pfp_distribution_sum_pointwise_a + S (a) = S ((S (i)) * ac)) /\ exists ff_q_pfp_distribution_sum_pointwise_a. ab = ff_q_pfp_distribution_sum_pointwise_a * S ((S (i)) * ac) + (a))) -> (((exists ff_h_pfp_distribution_sum_pointwise_b. ff_h_pfp_distribution_sum_pointwise_b + S (b) = S ((S (i)) * bc)) /\ exists ff_q_pfp_distribution_sum_pointwise_b. bb = ff_q_pfp_distribution_sum_pointwise_b * S ((S (i)) * bc) + (b))) -> (((exists ff_h_pfp_distribution_sum_pointwise_c. ff_h_pfp_distribution_sum_pointwise_c + S (c) = S ((S (i)) * cc)) /\ exists ff_q_pfp_distribution_sum_pointwise_c. cb = ff_q_pfp_distribution_sum_pointwise_c * S ((S (i)) * cc) + (c))) -> (exists pfa_offset_left_distribution_sum_pointwise_value pfa_offset_right_distribution_sum_pointwise_value. (a+b) + (p) * pfa_offset_left_distribution_sum_pointwise_value = (c) + (p) * pfa_offset_right_distribution_sum_pointwise_value)) -> (exists pfa_offset_left_distribution_sum_result pfa_offset_right_distribution_sum_result. (A+B) + (p) * pfa_offset_left_distribution_sum_result = (C) + (p) * pfa_offset_right_distribution_sum_result)

Constructive proof overview

Generated structural guide

Actual pointwise additive congruences lift by finite induction to the three actual Sum endpoints, for every modulus and also for the empty prefix.

The unchanged tactic script uses 7 declared prerequisites and contains 152 exact native proof lines.

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

Proof neighborhood

Direct dependencies

beta_sum_zero Alpha theorem; checked-use authorized beta_sum_succ_decompose Alpha theorem; checked-use authorized le_succ Alpha theorem; checked-use authorized le_refl Alpha theorem; checked-use authorized mod_eq_add Alpha theorem; checked-use authorized add_assoc Alpha theorem; checked-use authorized add_comm Alpha theorem; checked-use authorized

Direct dependents

PX0044 polynomial_diagonal_sum_left_add_congruent PX0045 polynomial_diagonal_sum_right_add_congruent

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

152 script commands · 30 reading checkpoints · 10 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 p
  2. L2
    intro ab
  3. L3
    intro ac
  4. L4
    intro bb
  5. L5
    intro bc
  6. L6
    intro cb
  7. L7
    intro cc
02Induction on LL8–15

Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.

  1. L8
    induction L
  2. L9
    intro A
  3. L10
    intro B
  4. L11
    intro C
  5. L12
    intro ha
  6. L13
    intro hb
  7. L14
    intro hc
  8. L15
    intro hpw
03Establish hAL16–21

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

  1. L16
    have hA : A=0
  2. L17
    specialize beta_sum_zero (ab)
  3. L18
    specialize beta_sum_zero (ac)
  4. L19
    specialize beta_sum_zero (A)
  5. L20
    apply beta_sum_zero
  6. L21
    exact ha
04Establish hBL22–27

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

  1. L22
    have hB : B=0
  2. L23
    specialize beta_sum_zero (bb)
  3. L24
    specialize beta_sum_zero (bc)
  4. L25
    specialize beta_sum_zero (B)
  5. L26
    apply beta_sum_zero
  6. L27
    exact hb
05Establish hCL28–36

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

  1. L28
    have hC : C=0
  2. L29
    specialize beta_sum_zero (cb)
  3. L30
    specialize beta_sum_zero (cc)
  4. L31
    specialize beta_sum_zero (C)
  5. L32
    apply beta_sum_zero
  6. L33
    exact hc
  7. L34
    rewrite hA
  8. L35
    rewrite hB
  9. L36
    rewrite hC
06Construct an explicit witnessL37–38

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

  1. L37
    exists 0
  2. L38
    exists 0
07Calculate and transport equalitiesL39–39

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

  1. L39
    simp
08Fix variables and assumptionsL40–46

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

  1. L40
    intro A
  2. L41
    intro B
  3. L42
    intro C
  4. L43
    intro ha
  5. L44
    intro hb
  6. L45
    intro hc
  7. L46
    intro hpw
09Establish hdaL47–53

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta sum succ decompose.

  1. L47
    have hda : ∃ a. ∃ r. BetaAt(ab,ac,L,a) ∧ (Sum(ab,ac,L,r) ∧ A = r + a)Definitions: BetaAtSum
  2. L48
    specialize beta_sum_succ_decompose (ab)
  3. L49
    specialize beta_sum_succ_decompose (ac)
  4. L50
    specialize beta_sum_succ_decompose (L)
  5. L51
    specialize beta_sum_succ_decompose (A)
  6. L52
    apply beta_sum_succ_decompose
  7. L53
    exact ha
10Separate the logical casesL54–57

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

  1. L54
    cases hda
  2. L55
    cases hda_witness
  3. L56
    cases hda_witness_witness
  4. L57
    cases hda_witness_witness_right
11Establish hdbL58–64

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta sum succ decompose.

  1. L58
    have hdb : ∃ a. ∃ r. BetaAt(bb,bc,L,a) ∧ (Sum(bb,bc,L,r) ∧ B = r + a)Definitions: BetaAtSum
  2. L59
    specialize beta_sum_succ_decompose (bb)
  3. L60
    specialize beta_sum_succ_decompose (bc)
  4. L61
    specialize beta_sum_succ_decompose (L)
  5. L62
    specialize beta_sum_succ_decompose (B)
  6. L63
    apply beta_sum_succ_decompose
  7. L64
    exact hb
12Separate the logical casesL65–68

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

  1. L65
    cases hdb
  2. L66
    cases hdb_witness
  3. L67
    cases hdb_witness_witness
  4. L68
    cases hdb_witness_witness_right
13Establish hdcL69–75

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta sum succ decompose.

  1. L69
    have hdc : ∃ a. ∃ r. BetaAt(cb,cc,L,a) ∧ (Sum(cb,cc,L,r) ∧ C = r + a)Definitions: BetaAtSum
  2. L70
    specialize beta_sum_succ_decompose (cb)
  3. L71
    specialize beta_sum_succ_decompose (cc)
  4. L72
    specialize beta_sum_succ_decompose (L)
  5. L73
    specialize beta_sum_succ_decompose (C)
  6. L74
    apply beta_sum_succ_decompose
  7. L75
    exact hc
14Separate the logical casesL76–79

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

  1. L76
    cases hdc
  2. L77
    cases hdc_witness
  3. L78
    cases hdc_witness_witness
  4. L79
    cases hdc_witness_witness_right
15Establish hprefixL80–89

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

  1. L80
    have hprefix : exists pfa_offset_left_distribution_sum_prefix pfa_offset_right_distribution_sum_prefix. (x1+x3) + (p) * pfa_offset_left_distribution_sum_prefix = (x5) + (p) * pfa_offset_right_distribution_sum_prefix
  2. L81
    specialize IH (x1)
  3. L82
    specialize IH (x3)
  4. L83
    specialize IH (x5)
  5. L84
    apply IH
  6. L85
    exact hda_witness_witness_right_left
  7. L86
    exact hdb_witness_witness_right_left
  8. L87
    exact hdc_witness_witness_right_left
  9. L88
    intro i
  10. L89
    intro a
16Fix variables and assumptionsL90–95

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

  1. L90
    intro b
  2. L91
    intro c
  3. L92
    intro hi
  4. L93
    intro hea
  5. L94
    intro heb
  6. L95
    intro hec
17Use earlier factsL96–105

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

  1. L96
    specialize hpw (i)
  2. L97
    specialize hpw (a)
  3. L98
    specialize hpw (b)
  4. L99
    specialize hpw (c)
  5. L100
    apply hpw
  6. L101
    specialize le_succ (S i)
  7. L102
    specialize le_succ (L)
  8. L103
    apply le_succ
  9. L104
    exact hi
  10. L105
    exact hea
18Use earlier factsL106–107

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

  1. L106
    exact heb
  2. L107
    exact hec
19Establish hlastL108–117

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

  1. L108
    have hlast : exists pfa_offset_left_distribution_sum_last pfa_offset_right_distribution_sum_last. (x+x2) + (p) * pfa_offset_left_distribution_sum_last = (x4) + (p) * pfa_offset_right_distribution_sum_last
  2. L109
    specialize hpw (L)
  3. L110
    specialize hpw (x)
  4. L111
    specialize hpw (x2)
  5. L112
    specialize hpw (x4)
  6. L113
    apply hpw
  7. L114
    specialize le_refl (S L)
  8. L115
    apply le_refl
  9. L116
    exact hda_witness_witness_left
  10. L117
    exact hdb_witness_witness_left
20Use earlier factsL118–118

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

  1. L118
    exact hdc_witness_witness_left
21Establish hcombinedL119–127

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

  1. L119
    have hcombined : exists pfa_offset_left_distribution_sum_combined pfa_offset_right_distribution_sum_combined. ((x1+x3)+(x+x2)) + (p) * pfa_offset_left_distribution_sum_combined = (x5+x4) + (p) * pfa_offset_right_distribution_sum_combined
  2. L120
    specialize mod_eq_add (p)
  3. L121
    specialize mod_eq_add (x1+x3)
  4. L122
    specialize mod_eq_add (x5)
  5. L123
    specialize mod_eq_add (x+x2)
  6. L124
    specialize mod_eq_add (x4)
  7. L125
    apply mod_eq_add
  8. L126
    exact hprefix
  9. L127
    exact hlast
22Establish hshuffleL128–137

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

  1. L128
    have hshuffle : (x1+x)+(x3+x2)=(x1+x3)+(x+x2)
  2. L129
    trans x1+(x+(x3+x2))
  3. L130
    apply add_assoc
  4. L131
    trans x1+((x+x3)+x2)
  5. L132
    congr
  6. L133
    refl
  7. L134
    symm
  8. L135
    apply add_assoc
  9. L136
    trans x1+((x3+x)+x2)
  10. L137
    congr
23Calculate and transport equalitiesL138–139

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

  1. L138
    refl
  2. L139
    congr
24Use earlier factsL140–140

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

  1. L140
    apply add_comm
25Calculate and transport equalitiesL141–144

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

  1. L141
    refl
  2. L142
    trans x1+(x3+(x+x2))
  3. L143
    congr
  4. L144
    refl
26Use earlier factsL145–145

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

  1. L145
    apply add_assoc
27Calculate and transport equalitiesL146–146

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

  1. L146
    symm
28Use earlier factsL147–147

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

  1. L147
    apply add_assoc
29Calculate and transport equalitiesL148–151

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

  1. L148
    rewrite hda_witness_witness_right_right
  2. L149
    rewrite hdb_witness_witness_right_right
  3. L150
    rewrite hdc_witness_witness_right_right
  4. L151
    rewrite hshuffle
30Use earlier factsL152–152

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

  1. L152
    exact hcombined

Library-wide reading audit

Original exact command ledger · 152 lines
  1. 0001intro p
  2. 0002intro ab
  3. 0003intro ac
  4. 0004intro bb
  5. 0005intro bc
  6. 0006intro cb
  7. 0007intro cc
  8. 0008induction L
  9. 0009intro A
  10. 0010intro B
  11. 0011intro C
  12. 0012intro ha
  13. 0013intro hb
  14. 0014intro hc
  15. 0015intro hpw
  16. 0016have hA : A=0
  17. 0017specialize beta_sum_zero (ab)
  18. 0018specialize beta_sum_zero (ac)
  19. 0019specialize beta_sum_zero (A)
  20. 0020apply beta_sum_zero
  21. 0021exact ha
  22. 0022have hB : B=0
  23. 0023specialize beta_sum_zero (bb)
  24. 0024specialize beta_sum_zero (bc)
  25. 0025specialize beta_sum_zero (B)
  26. 0026apply beta_sum_zero
  27. 0027exact hb
  28. 0028have hC : C=0
  29. 0029specialize beta_sum_zero (cb)
  30. 0030specialize beta_sum_zero (cc)
  31. 0031specialize beta_sum_zero (C)
  32. 0032apply beta_sum_zero
  33. 0033exact hc
  34. 0034rewrite hA
  35. 0035rewrite hB
  36. 0036rewrite hC
  37. 0037exists 0
  38. 0038exists 0
  39. 0039simp
  40. 0040intro A
  41. 0041intro B
  42. 0042intro C
  43. 0043intro ha
  44. 0044intro hb
  45. 0045intro hc
  46. 0046intro hpw
  47. 0047have hda : exists a r. ((((exists ff_h_pfp_hda_entry. ff_h_pfp_hda_entry + S (a) = S ((S (L)) * ac)) /\ exists ff_q_pfp_hda_entry. ab = ff_q_pfp_hda_entry * S ((S (L)) * ac) + (a))) /\ (((exists fs_u_pfc_hda_prefix fs_v_pfc_hda_prefix. ((((exists fs_h_pfc_hda_prefix_body_start. fs_h_pfc_hda_prefix_body_start + S (0) = S ((S (0)) * fs_v_pfc_hda_prefix)) /\ exists fs_q_pfc_hda_prefix_body_start. fs_u_pfc_hda_prefix = fs_q_pfc_hda_prefix_body_start * S ((S (0)) * fs_v_pfc_hda_prefix) + (0))) /\ ((((exists fs_h_pfc_hda_prefix_body_terminal. fs_h_pfc_hda_prefix_body_terminal + S (r) = S ((S (L)) * fs_v_pfc_hda_prefix)) /\ exists fs_q_pfc_hda_prefix_body_terminal. fs_u_pfc_hda_prefix = fs_q_pfc_hda_prefix_body_terminal * S ((S (L)) * fs_v_pfc_hda_prefix) + (r))) /\ forall fs_i_pfc_hda_prefix_body_steps. (exists fs_lt_pfc_hda_prefix_body_steps_bound. fs_lt_pfc_hda_prefix_body_steps_bound + S fs_i_pfc_hda_prefix_body_steps = L) -> exists fs_a_pfc_hda_prefix_body_steps fs_r_pfc_hda_prefix_body_steps fs_s_pfc_hda_prefix_body_steps. ((((exists fs_h_pfc_hda_prefix_body_steps_summand. fs_h_pfc_hda_prefix_body_steps_summand + S (fs_a_pfc_hda_prefix_body_steps) = S ((S (fs_i_pfc_hda_prefix_body_steps)) * ac)) /\ exists fs_q_pfc_hda_prefix_body_steps_summand. ab = fs_q_pfc_hda_prefix_body_steps_summand * S ((S (fs_i_pfc_hda_prefix_body_steps)) * ac) + (fs_a_pfc_hda_prefix_body_steps))) /\ ((((exists fs_h_pfc_hda_prefix_body_steps_partial. fs_h_pfc_hda_prefix_body_steps_partial + S (fs_r_pfc_hda_prefix_body_steps) = S ((S (fs_i_pfc_hda_prefix_body_steps)) * fs_v_pfc_hda_prefix)) /\ exists fs_q_pfc_hda_prefix_body_steps_partial. fs_u_pfc_hda_prefix = fs_q_pfc_hda_prefix_body_steps_partial * S ((S (fs_i_pfc_hda_prefix_body_steps)) * fs_v_pfc_hda_prefix) + (fs_r_pfc_hda_prefix_body_steps))) /\ ((((exists fs_h_pfc_hda_prefix_body_steps_successor. fs_h_pfc_hda_prefix_body_steps_successor + S (fs_s_pfc_hda_prefix_body_steps) = S ((S (S fs_i_pfc_hda_prefix_body_steps)) * fs_v_pfc_hda_prefix)) /\ exists fs_q_pfc_hda_prefix_body_steps_successor. fs_u_pfc_hda_prefix = fs_q_pfc_hda_prefix_body_steps_successor * S ((S (S fs_i_pfc_hda_prefix_body_steps)) * fs_v_pfc_hda_prefix) + (fs_s_pfc_hda_prefix_body_steps))) /\ fs_s_pfc_hda_prefix_body_steps = fs_r_pfc_hda_prefix_body_steps + fs_a_pfc_hda_prefix_body_steps)))))) /\ ((A=r+a)))))
  48. 0048specialize beta_sum_succ_decompose (ab)
  49. 0049specialize beta_sum_succ_decompose (ac)
  50. 0050specialize beta_sum_succ_decompose (L)
  51. 0051specialize beta_sum_succ_decompose (A)
  52. 0052apply beta_sum_succ_decompose
  53. 0053exact ha
  54. 0054cases hda
  55. 0055cases hda_witness
  56. 0056cases hda_witness_witness
  57. 0057cases hda_witness_witness_right
  58. 0058have hdb : exists a r. ((((exists ff_h_pfp_hdb_entry. ff_h_pfp_hdb_entry + S (a) = S ((S (L)) * bc)) /\ exists ff_q_pfp_hdb_entry. bb = ff_q_pfp_hdb_entry * S ((S (L)) * bc) + (a))) /\ (((exists fs_u_pfc_hdb_prefix fs_v_pfc_hdb_prefix. ((((exists fs_h_pfc_hdb_prefix_body_start. fs_h_pfc_hdb_prefix_body_start + S (0) = S ((S (0)) * fs_v_pfc_hdb_prefix)) /\ exists fs_q_pfc_hdb_prefix_body_start. fs_u_pfc_hdb_prefix = fs_q_pfc_hdb_prefix_body_start * S ((S (0)) * fs_v_pfc_hdb_prefix) + (0))) /\ ((((exists fs_h_pfc_hdb_prefix_body_terminal. fs_h_pfc_hdb_prefix_body_terminal + S (r) = S ((S (L)) * fs_v_pfc_hdb_prefix)) /\ exists fs_q_pfc_hdb_prefix_body_terminal. fs_u_pfc_hdb_prefix = fs_q_pfc_hdb_prefix_body_terminal * S ((S (L)) * fs_v_pfc_hdb_prefix) + (r))) /\ forall fs_i_pfc_hdb_prefix_body_steps. (exists fs_lt_pfc_hdb_prefix_body_steps_bound. fs_lt_pfc_hdb_prefix_body_steps_bound + S fs_i_pfc_hdb_prefix_body_steps = L) -> exists fs_a_pfc_hdb_prefix_body_steps fs_r_pfc_hdb_prefix_body_steps fs_s_pfc_hdb_prefix_body_steps. ((((exists fs_h_pfc_hdb_prefix_body_steps_summand. fs_h_pfc_hdb_prefix_body_steps_summand + S (fs_a_pfc_hdb_prefix_body_steps) = S ((S (fs_i_pfc_hdb_prefix_body_steps)) * bc)) /\ exists fs_q_pfc_hdb_prefix_body_steps_summand. bb = fs_q_pfc_hdb_prefix_body_steps_summand * S ((S (fs_i_pfc_hdb_prefix_body_steps)) * bc) + (fs_a_pfc_hdb_prefix_body_steps))) /\ ((((exists fs_h_pfc_hdb_prefix_body_steps_partial. fs_h_pfc_hdb_prefix_body_steps_partial + S (fs_r_pfc_hdb_prefix_body_steps) = S ((S (fs_i_pfc_hdb_prefix_body_steps)) * fs_v_pfc_hdb_prefix)) /\ exists fs_q_pfc_hdb_prefix_body_steps_partial. fs_u_pfc_hdb_prefix = fs_q_pfc_hdb_prefix_body_steps_partial * S ((S (fs_i_pfc_hdb_prefix_body_steps)) * fs_v_pfc_hdb_prefix) + (fs_r_pfc_hdb_prefix_body_steps))) /\ ((((exists fs_h_pfc_hdb_prefix_body_steps_successor. fs_h_pfc_hdb_prefix_body_steps_successor + S (fs_s_pfc_hdb_prefix_body_steps) = S ((S (S fs_i_pfc_hdb_prefix_body_steps)) * fs_v_pfc_hdb_prefix)) /\ exists fs_q_pfc_hdb_prefix_body_steps_successor. fs_u_pfc_hdb_prefix = fs_q_pfc_hdb_prefix_body_steps_successor * S ((S (S fs_i_pfc_hdb_prefix_body_steps)) * fs_v_pfc_hdb_prefix) + (fs_s_pfc_hdb_prefix_body_steps))) /\ fs_s_pfc_hdb_prefix_body_steps = fs_r_pfc_hdb_prefix_body_steps + fs_a_pfc_hdb_prefix_body_steps)))))) /\ ((B=r+a)))))
  59. 0059specialize beta_sum_succ_decompose (bb)
  60. 0060specialize beta_sum_succ_decompose (bc)
  61. 0061specialize beta_sum_succ_decompose (L)
  62. 0062specialize beta_sum_succ_decompose (B)
  63. 0063apply beta_sum_succ_decompose
  64. 0064exact hb
  65. 0065cases hdb
  66. 0066cases hdb_witness
  67. 0067cases hdb_witness_witness
  68. 0068cases hdb_witness_witness_right
  69. 0069have hdc : exists a r. ((((exists ff_h_pfp_hdc_entry. ff_h_pfp_hdc_entry + S (a) = S ((S (L)) * cc)) /\ exists ff_q_pfp_hdc_entry. cb = ff_q_pfp_hdc_entry * S ((S (L)) * cc) + (a))) /\ (((exists fs_u_pfc_hdc_prefix fs_v_pfc_hdc_prefix. ((((exists fs_h_pfc_hdc_prefix_body_start. fs_h_pfc_hdc_prefix_body_start + S (0) = S ((S (0)) * fs_v_pfc_hdc_prefix)) /\ exists fs_q_pfc_hdc_prefix_body_start. fs_u_pfc_hdc_prefix = fs_q_pfc_hdc_prefix_body_start * S ((S (0)) * fs_v_pfc_hdc_prefix) + (0))) /\ ((((exists fs_h_pfc_hdc_prefix_body_terminal. fs_h_pfc_hdc_prefix_body_terminal + S (r) = S ((S (L)) * fs_v_pfc_hdc_prefix)) /\ exists fs_q_pfc_hdc_prefix_body_terminal. fs_u_pfc_hdc_prefix = fs_q_pfc_hdc_prefix_body_terminal * S ((S (L)) * fs_v_pfc_hdc_prefix) + (r))) /\ forall fs_i_pfc_hdc_prefix_body_steps. (exists fs_lt_pfc_hdc_prefix_body_steps_bound. fs_lt_pfc_hdc_prefix_body_steps_bound + S fs_i_pfc_hdc_prefix_body_steps = L) -> exists fs_a_pfc_hdc_prefix_body_steps fs_r_pfc_hdc_prefix_body_steps fs_s_pfc_hdc_prefix_body_steps. ((((exists fs_h_pfc_hdc_prefix_body_steps_summand. fs_h_pfc_hdc_prefix_body_steps_summand + S (fs_a_pfc_hdc_prefix_body_steps) = S ((S (fs_i_pfc_hdc_prefix_body_steps)) * cc)) /\ exists fs_q_pfc_hdc_prefix_body_steps_summand. cb = fs_q_pfc_hdc_prefix_body_steps_summand * S ((S (fs_i_pfc_hdc_prefix_body_steps)) * cc) + (fs_a_pfc_hdc_prefix_body_steps))) /\ ((((exists fs_h_pfc_hdc_prefix_body_steps_partial. fs_h_pfc_hdc_prefix_body_steps_partial + S (fs_r_pfc_hdc_prefix_body_steps) = S ((S (fs_i_pfc_hdc_prefix_body_steps)) * fs_v_pfc_hdc_prefix)) /\ exists fs_q_pfc_hdc_prefix_body_steps_partial. fs_u_pfc_hdc_prefix = fs_q_pfc_hdc_prefix_body_steps_partial * S ((S (fs_i_pfc_hdc_prefix_body_steps)) * fs_v_pfc_hdc_prefix) + (fs_r_pfc_hdc_prefix_body_steps))) /\ ((((exists fs_h_pfc_hdc_prefix_body_steps_successor. fs_h_pfc_hdc_prefix_body_steps_successor + S (fs_s_pfc_hdc_prefix_body_steps) = S ((S (S fs_i_pfc_hdc_prefix_body_steps)) * fs_v_pfc_hdc_prefix)) /\ exists fs_q_pfc_hdc_prefix_body_steps_successor. fs_u_pfc_hdc_prefix = fs_q_pfc_hdc_prefix_body_steps_successor * S ((S (S fs_i_pfc_hdc_prefix_body_steps)) * fs_v_pfc_hdc_prefix) + (fs_s_pfc_hdc_prefix_body_steps))) /\ fs_s_pfc_hdc_prefix_body_steps = fs_r_pfc_hdc_prefix_body_steps + fs_a_pfc_hdc_prefix_body_steps)))))) /\ ((C=r+a)))))
  70. 0070specialize beta_sum_succ_decompose (cb)
  71. 0071specialize beta_sum_succ_decompose (cc)
  72. 0072specialize beta_sum_succ_decompose (L)
  73. 0073specialize beta_sum_succ_decompose (C)
  74. 0074apply beta_sum_succ_decompose
  75. 0075exact hc
  76. 0076cases hdc
  77. 0077cases hdc_witness
  78. 0078cases hdc_witness_witness
  79. 0079cases hdc_witness_witness_right
  80. 0080have hprefix : exists pfa_offset_left_distribution_sum_prefix pfa_offset_right_distribution_sum_prefix. (x1+x3) + (p) * pfa_offset_left_distribution_sum_prefix = (x5) + (p) * pfa_offset_right_distribution_sum_prefix
  81. 0081specialize IH (x1)
  82. 0082specialize IH (x3)
  83. 0083specialize IH (x5)
  84. 0084apply IH
  85. 0085exact hda_witness_witness_right_left
  86. 0086exact hdb_witness_witness_right_left
  87. 0087exact hdc_witness_witness_right_left
  88. 0088intro i
  89. 0089intro a
  90. 0090intro b
  91. 0091intro c
  92. 0092intro hi
  93. 0093intro hea
  94. 0094intro heb
  95. 0095intro hec
  96. 0096specialize hpw (i)
  97. 0097specialize hpw (a)
  98. 0098specialize hpw (b)
  99. 0099specialize hpw (c)
  100. 0100apply hpw
  101. 0101specialize le_succ (S i)
  102. 0102specialize le_succ (L)
  103. 0103apply le_succ
  104. 0104exact hi
  105. 0105exact hea
  106. 0106exact heb
  107. 0107exact hec
  108. 0108have hlast : exists pfa_offset_left_distribution_sum_last pfa_offset_right_distribution_sum_last. (x+x2) + (p) * pfa_offset_left_distribution_sum_last = (x4) + (p) * pfa_offset_right_distribution_sum_last
  109. 0109specialize hpw (L)
  110. 0110specialize hpw (x)
  111. 0111specialize hpw (x2)
  112. 0112specialize hpw (x4)
  113. 0113apply hpw
  114. 0114specialize le_refl (S L)
  115. 0115apply le_refl
  116. 0116exact hda_witness_witness_left
  117. 0117exact hdb_witness_witness_left
  118. 0118exact hdc_witness_witness_left
  119. 0119have hcombined : exists pfa_offset_left_distribution_sum_combined pfa_offset_right_distribution_sum_combined. ((x1+x3)+(x+x2)) + (p) * pfa_offset_left_distribution_sum_combined = (x5+x4) + (p) * pfa_offset_right_distribution_sum_combined
  120. 0120specialize mod_eq_add (p)
  121. 0121specialize mod_eq_add (x1+x3)
  122. 0122specialize mod_eq_add (x5)
  123. 0123specialize mod_eq_add (x+x2)
  124. 0124specialize mod_eq_add (x4)
  125. 0125apply mod_eq_add
  126. 0126exact hprefix
  127. 0127exact hlast
  128. 0128have hshuffle : (x1+x)+(x3+x2)=(x1+x3)+(x+x2)
  129. 0129trans x1+(x+(x3+x2))
  130. 0130apply add_assoc
  131. 0131trans x1+((x+x3)+x2)
  132. 0132congr
  133. 0133refl
  134. 0134symm
  135. 0135apply add_assoc
  136. 0136trans x1+((x3+x)+x2)
  137. 0137congr
  138. 0138refl
  139. 0139congr
  140. 0140apply add_comm
  141. 0141refl
  142. 0142trans x1+(x3+(x+x2))
  143. 0143congr
  144. 0144refl
  145. 0145apply add_assoc
  146. 0146symm
  147. 0147apply add_assoc
  148. 0148rewrite hda_witness_witness_right_right
  149. 0149rewrite hdb_witness_witness_right_right
  150. 0150rewrite hdc_witness_witness_right_right
  151. 0151rewrite hshuffle
  152. 0152exact hcombined