CD000F

finite_sum_pointwise_balance

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

A pointwise four-prefix balance gives the exact corresponding balance of all four finite sums.

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 original first-admission records.

Exact expanded first-order arithmetic statement

forall b c d e f g h t l n m q r. (exists ff_u_fms_sum ff_v_fms_sum. ((((exists ff_h_fms_sum_start. ff_h_fms_sum_start + S (0) = S ((S (0)) * ff_v_fms_sum)) /\ exists ff_q_fms_sum_start. ff_u_fms_sum = ff_q_fms_sum_start * S ((S (0)) * ff_v_fms_sum) + (0))) /\ ((((exists ff_h_fms_sum_terminal. ff_h_fms_sum_terminal + S ((n)) = S ((S ((l))) * ff_v_fms_sum)) /\ exists ff_q_fms_sum_terminal. ff_u_fms_sum = ff_q_fms_sum_terminal * S ((S ((l))) * ff_v_fms_sum) + ((n)))) /\ forall ff_i_fms_sum. (exists ff_lt_fms_sum_bound. ff_lt_fms_sum_bound + S ff_i_fms_sum = (l)) -> exists ff_a_fms_sum ff_r_fms_sum ff_s_fms_sum. ((((exists ff_h_fms_sum_summand. ff_h_fms_sum_summand + S (ff_a_fms_sum) = S ((S (ff_i_fms_sum)) * (c))) /\ exists ff_q_fms_sum_summand. (b) = ff_q_fms_sum_summand * S ((S (ff_i_fms_sum)) * (c)) + (ff_a_fms_sum))) /\ ((((exists ff_h_fms_sum_partial. ff_h_fms_sum_partial + S (ff_r_fms_sum) = S ((S (ff_i_fms_sum)) * ff_v_fms_sum)) /\ exists ff_q_fms_sum_partial. ff_u_fms_sum = ff_q_fms_sum_partial * S ((S (ff_i_fms_sum)) * ff_v_fms_sum) + (ff_r_fms_sum))) /\ ((((exists ff_h_fms_sum_successor. ff_h_fms_sum_successor + S (ff_s_fms_sum) = S ((S (S ff_i_fms_sum)) * ff_v_fms_sum)) /\ exists ff_q_fms_sum_successor. ff_u_fms_sum = ff_q_fms_sum_successor * S ((S (S ff_i_fms_sum)) * ff_v_fms_sum) + (ff_s_fms_sum))) /\ ff_s_fms_sum = ff_r_fms_sum + ff_a_fms_sum)))))) -> (exists ff_u_fms_sum ff_v_fms_sum. ((((exists ff_h_fms_sum_start. ff_h_fms_sum_start + S (0) = S ((S (0)) * ff_v_fms_sum)) /\ exists ff_q_fms_sum_start. ff_u_fms_sum = ff_q_fms_sum_start * S ((S (0)) * ff_v_fms_sum) + (0))) /\ ((((exists ff_h_fms_sum_terminal. ff_h_fms_sum_terminal + S ((m)) = S ((S ((l))) * ff_v_fms_sum)) /\ exists ff_q_fms_sum_terminal. ff_u_fms_sum = ff_q_fms_sum_terminal * S ((S ((l))) * ff_v_fms_sum) + ((m)))) /\ forall ff_i_fms_sum. (exists ff_lt_fms_sum_bound. ff_lt_fms_sum_bound + S ff_i_fms_sum = (l)) -> exists ff_a_fms_sum ff_r_fms_sum ff_s_fms_sum. ((((exists ff_h_fms_sum_summand. ff_h_fms_sum_summand + S (ff_a_fms_sum) = S ((S (ff_i_fms_sum)) * (e))) /\ exists ff_q_fms_sum_summand. (d) = ff_q_fms_sum_summand * S ((S (ff_i_fms_sum)) * (e)) + (ff_a_fms_sum))) /\ ((((exists ff_h_fms_sum_partial. ff_h_fms_sum_partial + S (ff_r_fms_sum) = S ((S (ff_i_fms_sum)) * ff_v_fms_sum)) /\ exists ff_q_fms_sum_partial. ff_u_fms_sum = ff_q_fms_sum_partial * S ((S (ff_i_fms_sum)) * ff_v_fms_sum) + (ff_r_fms_sum))) /\ ((((exists ff_h_fms_sum_successor. ff_h_fms_sum_successor + S (ff_s_fms_sum) = S ((S (S ff_i_fms_sum)) * ff_v_fms_sum)) /\ exists ff_q_fms_sum_successor. ff_u_fms_sum = ff_q_fms_sum_successor * S ((S (S ff_i_fms_sum)) * ff_v_fms_sum) + (ff_s_fms_sum))) /\ ff_s_fms_sum = ff_r_fms_sum + ff_a_fms_sum)))))) -> (exists ff_u_fms_sum ff_v_fms_sum. ((((exists ff_h_fms_sum_start. ff_h_fms_sum_start + S (0) = S ((S (0)) * ff_v_fms_sum)) /\ exists ff_q_fms_sum_start. ff_u_fms_sum = ff_q_fms_sum_start * S ((S (0)) * ff_v_fms_sum) + (0))) /\ ((((exists ff_h_fms_sum_terminal. ff_h_fms_sum_terminal + S ((q)) = S ((S ((l))) * ff_v_fms_sum)) /\ exists ff_q_fms_sum_terminal. ff_u_fms_sum = ff_q_fms_sum_terminal * S ((S ((l))) * ff_v_fms_sum) + ((q)))) /\ forall ff_i_fms_sum. (exists ff_lt_fms_sum_bound. ff_lt_fms_sum_bound + S ff_i_fms_sum = (l)) -> exists ff_a_fms_sum ff_r_fms_sum ff_s_fms_sum. ((((exists ff_h_fms_sum_summand. ff_h_fms_sum_summand + S (ff_a_fms_sum) = S ((S (ff_i_fms_sum)) * (g))) /\ exists ff_q_fms_sum_summand. (f) = ff_q_fms_sum_summand * S ((S (ff_i_fms_sum)) * (g)) + (ff_a_fms_sum))) /\ ((((exists ff_h_fms_sum_partial. ff_h_fms_sum_partial + S (ff_r_fms_sum) = S ((S (ff_i_fms_sum)) * ff_v_fms_sum)) /\ exists ff_q_fms_sum_partial. ff_u_fms_sum = ff_q_fms_sum_partial * S ((S (ff_i_fms_sum)) * ff_v_fms_sum) + (ff_r_fms_sum))) /\ ((((exists ff_h_fms_sum_successor. ff_h_fms_sum_successor + S (ff_s_fms_sum) = S ((S (S ff_i_fms_sum)) * ff_v_fms_sum)) /\ exists ff_q_fms_sum_successor. ff_u_fms_sum = ff_q_fms_sum_successor * S ((S (S ff_i_fms_sum)) * ff_v_fms_sum) + (ff_s_fms_sum))) /\ ff_s_fms_sum = ff_r_fms_sum + ff_a_fms_sum)))))) -> (exists ff_u_fms_sum ff_v_fms_sum. ((((exists ff_h_fms_sum_start. ff_h_fms_sum_start + S (0) = S ((S (0)) * ff_v_fms_sum)) /\ exists ff_q_fms_sum_start. ff_u_fms_sum = ff_q_fms_sum_start * S ((S (0)) * ff_v_fms_sum) + (0))) /\ ((((exists ff_h_fms_sum_terminal. ff_h_fms_sum_terminal + S ((r)) = S ((S ((l))) * ff_v_fms_sum)) /\ exists ff_q_fms_sum_terminal. ff_u_fms_sum = ff_q_fms_sum_terminal * S ((S ((l))) * ff_v_fms_sum) + ((r)))) /\ forall ff_i_fms_sum. (exists ff_lt_fms_sum_bound. ff_lt_fms_sum_bound + S ff_i_fms_sum = (l)) -> exists ff_a_fms_sum ff_r_fms_sum ff_s_fms_sum. ((((exists ff_h_fms_sum_summand. ff_h_fms_sum_summand + S (ff_a_fms_sum) = S ((S (ff_i_fms_sum)) * (t))) /\ exists ff_q_fms_sum_summand. (h) = ff_q_fms_sum_summand * S ((S (ff_i_fms_sum)) * (t)) + (ff_a_fms_sum))) /\ ((((exists ff_h_fms_sum_partial. ff_h_fms_sum_partial + S (ff_r_fms_sum) = S ((S (ff_i_fms_sum)) * ff_v_fms_sum)) /\ exists ff_q_fms_sum_partial. ff_u_fms_sum = ff_q_fms_sum_partial * S ((S (ff_i_fms_sum)) * ff_v_fms_sum) + (ff_r_fms_sum))) /\ ((((exists ff_h_fms_sum_successor. ff_h_fms_sum_successor + S (ff_s_fms_sum) = S ((S (S ff_i_fms_sum)) * ff_v_fms_sum)) /\ exists ff_q_fms_sum_successor. ff_u_fms_sum = ff_q_fms_sum_successor * S ((S (S ff_i_fms_sum)) * ff_v_fms_sum) + (ff_s_fms_sum))) /\ ff_s_fms_sum = ff_r_fms_sum + ff_a_fms_sum)))))) -> (forall fms_i_balance fms_a_balance fms_v_balance fms_w_balance fms_z_balance. (exists fms_gap_balance. fms_gap_balance + S (fms_i_balance) = (l)) -> (((exists fs_h_fms_balance_a. fs_h_fms_balance_a + S (fms_a_balance) = S ((S (fms_i_balance)) * c)) /\ exists fs_q_fms_balance_a. b = fs_q_fms_balance_a * S ((S (fms_i_balance)) * c) + (fms_a_balance))) -> (((exists fs_h_fms_balance_b. fs_h_fms_balance_b + S (fms_v_balance) = S ((S (fms_i_balance)) * e)) /\ exists fs_q_fms_balance_b. d = fs_q_fms_balance_b * S ((S (fms_i_balance)) * e) + (fms_v_balance))) -> (((exists fs_h_fms_balance_c. fs_h_fms_balance_c + S (fms_w_balance) = S ((S (fms_i_balance)) * g)) /\ exists fs_q_fms_balance_c. f = fs_q_fms_balance_c * S ((S (fms_i_balance)) * g) + (fms_w_balance))) -> (((exists fs_h_fms_balance_d. fs_h_fms_balance_d + S (fms_z_balance) = S ((S (fms_i_balance)) * t)) /\ exists fs_q_fms_balance_d. h = fs_q_fms_balance_d * S ((S (fms_i_balance)) * t) + (fms_z_balance))) -> fms_a_balance+fms_v_balance=fms_w_balance+fms_z_balance) -> n+m=q+r

Constructive proof overview

Generated structural guide

A pointwise four-prefix balance gives the exact corresponding balance of all four finite sums.

The unchanged tactic script uses 6 declared prerequisites and contains 156 exact native proof lines.

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

Proof neighborhood

Direct dependencies

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

Direct dependents

CD001B finite_bit_union_intersection_count_balance

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

156 script commands · 23 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–8

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

  1. L1
    intro b
  2. L2
    intro c
  3. L3
    intro d
  4. L4
    intro e
  5. L5
    intro f
  6. L6
    intro g
  7. L7
    intro h
  8. L8
    intro t
02Induction on lL9–18

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

  1. L9
    induction l
  2. L10
    intro n
  3. L11
    intro m
  4. L12
    intro q
  5. L13
    intro r
  6. L14
    intro hn
  7. L15
    intro hm
  8. L16
    intro hq
  9. L17
    intro hr
  10. L18
    intro hbalance
03Establish hzero_nL19–24

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

  1. L19
    have hzero_n : n=0
  2. L20
    specialize beta_sum_zero b
  3. L21
    specialize beta_sum_zero c
  4. L22
    specialize beta_sum_zero n
  5. L23
    apply beta_sum_zero
  6. L24
    exact hn
04Establish hzero_mL25–30

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

  1. L25
    have hzero_m : m=0
  2. L26
    specialize beta_sum_zero d
  3. L27
    specialize beta_sum_zero e
  4. L28
    specialize beta_sum_zero m
  5. L29
    apply beta_sum_zero
  6. L30
    exact hm
05Establish hzero_qL31–36

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

  1. L31
    have hzero_q : q=0
  2. L32
    specialize beta_sum_zero f
  3. L33
    specialize beta_sum_zero g
  4. L34
    specialize beta_sum_zero q
  5. L35
    apply beta_sum_zero
  6. L36
    exact hq
06Establish hzero_rL37–46

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

  1. L37
    have hzero_r : r=0
  2. L38
    specialize beta_sum_zero h
  3. L39
    specialize beta_sum_zero t
  4. L40
    specialize beta_sum_zero r
  5. L41
    apply beta_sum_zero
  6. L42
    exact hr
  7. L43
    rewrite hzero_n
  8. L44
    rewrite hzero_m
  9. L45
    rewrite hzero_q
  10. L46
    rewrite hzero_r
07Calculate and transport equalitiesL47–47

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

  1. L47
    refl
08Fix variables and assumptionsL48–56

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

  1. L48
    intro n
  2. L49
    intro m
  3. L50
    intro q
  4. L51
    intro r
  5. L52
    intro hn
  6. L53
    intro hm
  7. L54
    intro hq
  8. L55
    intro hr
  9. L56
    intro hbalance
09Establish hdAL57–63

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

  1. L57
    have hdA : ∃ fms_term_hdA. ∃ fms_sum_hdA. BetaAt(b,c,l,fms_term_hdA) ∧ (Sum(b,c,l,fms_sum_hdA) ∧ n = fms_sum_hdA + fms_term_hdA)Definitions: BetaAtSum
  2. L58
    specialize beta_sum_succ_decompose b
  3. L59
    specialize beta_sum_succ_decompose c
  4. L60
    specialize beta_sum_succ_decompose l
  5. L61
    specialize beta_sum_succ_decompose n
  6. L62
    apply beta_sum_succ_decompose
  7. L63
    exact hn
10Separate the logical casesL64–67

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

  1. L64
    cases hdA
  2. L65
    cases hdA_witness
  3. L66
    cases hdA_witness_witness
  4. L67
    cases hdA_witness_witness_right
11Establish hdBL68–74

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

  1. L68
    have hdB : ∃ fms_term_hdB. ∃ fms_sum_hdB. BetaAt(d,e,l,fms_term_hdB) ∧ (Sum(d,e,l,fms_sum_hdB) ∧ m = fms_sum_hdB + fms_term_hdB)Definitions: BetaAtSum
  2. L69
    specialize beta_sum_succ_decompose d
  3. L70
    specialize beta_sum_succ_decompose e
  4. L71
    specialize beta_sum_succ_decompose l
  5. L72
    specialize beta_sum_succ_decompose m
  6. L73
    apply beta_sum_succ_decompose
  7. L74
    exact hm
12Separate the logical casesL75–78

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

  1. L75
    cases hdB
  2. L76
    cases hdB_witness
  3. L77
    cases hdB_witness_witness
  4. L78
    cases hdB_witness_witness_right
13Establish hdCL79–85

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

  1. L79
    have hdC : ∃ fms_term_hdC. ∃ fms_sum_hdC. BetaAt(f,g,l,fms_term_hdC) ∧ (Sum(f,g,l,fms_sum_hdC) ∧ q = fms_sum_hdC + fms_term_hdC)Definitions: BetaAtSum
  2. L80
    specialize beta_sum_succ_decompose f
  3. L81
    specialize beta_sum_succ_decompose g
  4. L82
    specialize beta_sum_succ_decompose l
  5. L83
    specialize beta_sum_succ_decompose q
  6. L84
    apply beta_sum_succ_decompose
  7. L85
    exact hq
14Separate the logical casesL86–89

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

  1. L86
    cases hdC
  2. L87
    cases hdC_witness
  3. L88
    cases hdC_witness_witness
  4. L89
    cases hdC_witness_witness_right
15Establish hdDL90–96

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

  1. L90
    have hdD : ∃ fms_term_hdD. ∃ fms_sum_hdD. BetaAt(h,t,l,fms_term_hdD) ∧ (Sum(h,t,l,fms_sum_hdD) ∧ r = fms_sum_hdD + fms_term_hdD)Definitions: BetaAtSum
  2. L91
    specialize beta_sum_succ_decompose h
  3. L92
    specialize beta_sum_succ_decompose t
  4. L93
    specialize beta_sum_succ_decompose l
  5. L94
    specialize beta_sum_succ_decompose r
  6. L95
    apply beta_sum_succ_decompose
  7. L96
    exact hr
16Separate the logical casesL97–100

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

  1. L97
    cases hdD
  2. L98
    cases hdD_witness
  3. L99
    cases hdD_witness_witness
  4. L100
    cases hdD_witness_witness_right
17Establish hprefixL101–110

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

  1. L101
    have hprefix : x1+x3=x5+x7
  2. L102
    specialize IH x1
  3. L103
    specialize IH x3
  4. L104
    specialize IH x5
  5. L105
    specialize IH x7
  6. L106
    apply IH
  7. L107
    exact hdA_witness_witness_right_left
  8. L108
    exact hdB_witness_witness_right_left
  9. L109
    exact hdC_witness_witness_right_left
  10. L110
    exact hdD_witness_witness_right_left
18Fix variables and assumptionsL111–120

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

  1. L111
    intro i
  2. L112
    intro a
  3. L113
    intro v
  4. L114
    intro w
  5. L115
    intro z
  6. L116
    intro hi
  7. L117
    intro ha
  8. L118
    intro hv
  9. L119
    intro hw
  10. L120
    intro hz
19Use earlier factsL121–130

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

  1. L121
    specialize hbalance i
  2. L122
    specialize hbalance a
  3. L123
    specialize hbalance v
  4. L124
    specialize hbalance w
  5. L125
    specialize hbalance z
  6. L126
    apply hbalance
  7. L127
    specialize le_succ S i
  8. L128
    specialize le_succ l
  9. L129
    apply le_succ
  10. L130
    exact hi
20Use earlier factsL131–134

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

  1. L131
    exact ha
  2. L132
    exact hv
  3. L133
    exact hw
  4. L134
    exact hz
21Establish hlastL135–144

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

  1. L135
    have hlast : x+x2=x4+x6
  2. L136
    specialize hbalance l
  3. L137
    specialize hbalance x
  4. L138
    specialize hbalance x2
  5. L139
    specialize hbalance x4
  6. L140
    specialize hbalance x6
  7. L141
    apply hbalance
  8. L142
    specialize le_refl S l
  9. L143
    apply le_refl
  10. L144
    exact hdA_witness_witness_left
22Use earlier factsL145–147

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

  1. L145
    exact hdB_witness_witness_left
  2. L146
    exact hdC_witness_witness_left
  3. L147
    exact hdD_witness_witness_left
23Calculate and transport equalitiesL148–156

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 hdD_witness_witness_right_right
  5. L152
    trans (x1+x3)+(x+x2)
  6. L153
    simp [add_assoc, add_comm]
  7. L154
    rewrite hprefix
  8. L155
    rewrite hlast
  9. L156
    simp [add_assoc, add_comm]

Library-wide reading audit

Original exact command ledger · 156 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro d
  4. 0004intro e
  5. 0005intro f
  6. 0006intro g
  7. 0007intro h
  8. 0008intro t
  9. 0009induction l
  10. 0010intro n
  11. 0011intro m
  12. 0012intro q
  13. 0013intro r
  14. 0014intro hn
  15. 0015intro hm
  16. 0016intro hq
  17. 0017intro hr
  18. 0018intro hbalance
  19. 0019have hzero_n : n=0
  20. 0020specialize beta_sum_zero b
  21. 0021specialize beta_sum_zero c
  22. 0022specialize beta_sum_zero n
  23. 0023apply beta_sum_zero
  24. 0024exact hn
  25. 0025have hzero_m : m=0
  26. 0026specialize beta_sum_zero d
  27. 0027specialize beta_sum_zero e
  28. 0028specialize beta_sum_zero m
  29. 0029apply beta_sum_zero
  30. 0030exact hm
  31. 0031have hzero_q : q=0
  32. 0032specialize beta_sum_zero f
  33. 0033specialize beta_sum_zero g
  34. 0034specialize beta_sum_zero q
  35. 0035apply beta_sum_zero
  36. 0036exact hq
  37. 0037have hzero_r : r=0
  38. 0038specialize beta_sum_zero h
  39. 0039specialize beta_sum_zero t
  40. 0040specialize beta_sum_zero r
  41. 0041apply beta_sum_zero
  42. 0042exact hr
  43. 0043rewrite hzero_n
  44. 0044rewrite hzero_m
  45. 0045rewrite hzero_q
  46. 0046rewrite hzero_r
  47. 0047refl
  48. 0048intro n
  49. 0049intro m
  50. 0050intro q
  51. 0051intro r
  52. 0052intro hn
  53. 0053intro hm
  54. 0054intro hq
  55. 0055intro hr
  56. 0056intro hbalance
  57. 0057have hdA : exists fms_term_hdA fms_sum_hdA. (((exists fs_h_fms_hdA. fs_h_fms_hdA + S (fms_term_hdA) = S ((S (l)) * c)) /\ exists fs_q_fms_hdA. b = fs_q_fms_hdA * S ((S (l)) * c) + (fms_term_hdA))) /\ ((exists ff_u_fms_hdA ff_v_fms_hdA. ((((exists ff_h_fms_hdA_start. ff_h_fms_hdA_start + S (0) = S ((S (0)) * ff_v_fms_hdA)) /\ exists ff_q_fms_hdA_start. ff_u_fms_hdA = ff_q_fms_hdA_start * S ((S (0)) * ff_v_fms_hdA) + (0))) /\ ((((exists ff_h_fms_hdA_terminal. ff_h_fms_hdA_terminal + S ((fms_sum_hdA)) = S ((S ((l))) * ff_v_fms_hdA)) /\ exists ff_q_fms_hdA_terminal. ff_u_fms_hdA = ff_q_fms_hdA_terminal * S ((S ((l))) * ff_v_fms_hdA) + ((fms_sum_hdA)))) /\ forall ff_i_fms_hdA. (exists ff_lt_fms_hdA_bound. ff_lt_fms_hdA_bound + S ff_i_fms_hdA = (l)) -> exists ff_a_fms_hdA ff_r_fms_hdA ff_s_fms_hdA. ((((exists ff_h_fms_hdA_summand. ff_h_fms_hdA_summand + S (ff_a_fms_hdA) = S ((S (ff_i_fms_hdA)) * (c))) /\ exists ff_q_fms_hdA_summand. (b) = ff_q_fms_hdA_summand * S ((S (ff_i_fms_hdA)) * (c)) + (ff_a_fms_hdA))) /\ ((((exists ff_h_fms_hdA_partial. ff_h_fms_hdA_partial + S (ff_r_fms_hdA) = S ((S (ff_i_fms_hdA)) * ff_v_fms_hdA)) /\ exists ff_q_fms_hdA_partial. ff_u_fms_hdA = ff_q_fms_hdA_partial * S ((S (ff_i_fms_hdA)) * ff_v_fms_hdA) + (ff_r_fms_hdA))) /\ ((((exists ff_h_fms_hdA_successor. ff_h_fms_hdA_successor + S (ff_s_fms_hdA) = S ((S (S ff_i_fms_hdA)) * ff_v_fms_hdA)) /\ exists ff_q_fms_hdA_successor. ff_u_fms_hdA = ff_q_fms_hdA_successor * S ((S (S ff_i_fms_hdA)) * ff_v_fms_hdA) + (ff_s_fms_hdA))) /\ ff_s_fms_hdA = ff_r_fms_hdA + ff_a_fms_hdA)))))) /\ n=fms_sum_hdA+fms_term_hdA)
  58. 0058specialize beta_sum_succ_decompose b
  59. 0059specialize beta_sum_succ_decompose c
  60. 0060specialize beta_sum_succ_decompose l
  61. 0061specialize beta_sum_succ_decompose n
  62. 0062apply beta_sum_succ_decompose
  63. 0063exact hn
  64. 0064cases hdA
  65. 0065cases hdA_witness
  66. 0066cases hdA_witness_witness
  67. 0067cases hdA_witness_witness_right
  68. 0068have hdB : exists fms_term_hdB fms_sum_hdB. (((exists fs_h_fms_hdB. fs_h_fms_hdB + S (fms_term_hdB) = S ((S (l)) * e)) /\ exists fs_q_fms_hdB. d = fs_q_fms_hdB * S ((S (l)) * e) + (fms_term_hdB))) /\ ((exists ff_u_fms_hdB ff_v_fms_hdB. ((((exists ff_h_fms_hdB_start. ff_h_fms_hdB_start + S (0) = S ((S (0)) * ff_v_fms_hdB)) /\ exists ff_q_fms_hdB_start. ff_u_fms_hdB = ff_q_fms_hdB_start * S ((S (0)) * ff_v_fms_hdB) + (0))) /\ ((((exists ff_h_fms_hdB_terminal. ff_h_fms_hdB_terminal + S ((fms_sum_hdB)) = S ((S ((l))) * ff_v_fms_hdB)) /\ exists ff_q_fms_hdB_terminal. ff_u_fms_hdB = ff_q_fms_hdB_terminal * S ((S ((l))) * ff_v_fms_hdB) + ((fms_sum_hdB)))) /\ forall ff_i_fms_hdB. (exists ff_lt_fms_hdB_bound. ff_lt_fms_hdB_bound + S ff_i_fms_hdB = (l)) -> exists ff_a_fms_hdB ff_r_fms_hdB ff_s_fms_hdB. ((((exists ff_h_fms_hdB_summand. ff_h_fms_hdB_summand + S (ff_a_fms_hdB) = S ((S (ff_i_fms_hdB)) * (e))) /\ exists ff_q_fms_hdB_summand. (d) = ff_q_fms_hdB_summand * S ((S (ff_i_fms_hdB)) * (e)) + (ff_a_fms_hdB))) /\ ((((exists ff_h_fms_hdB_partial. ff_h_fms_hdB_partial + S (ff_r_fms_hdB) = S ((S (ff_i_fms_hdB)) * ff_v_fms_hdB)) /\ exists ff_q_fms_hdB_partial. ff_u_fms_hdB = ff_q_fms_hdB_partial * S ((S (ff_i_fms_hdB)) * ff_v_fms_hdB) + (ff_r_fms_hdB))) /\ ((((exists ff_h_fms_hdB_successor. ff_h_fms_hdB_successor + S (ff_s_fms_hdB) = S ((S (S ff_i_fms_hdB)) * ff_v_fms_hdB)) /\ exists ff_q_fms_hdB_successor. ff_u_fms_hdB = ff_q_fms_hdB_successor * S ((S (S ff_i_fms_hdB)) * ff_v_fms_hdB) + (ff_s_fms_hdB))) /\ ff_s_fms_hdB = ff_r_fms_hdB + ff_a_fms_hdB)))))) /\ m=fms_sum_hdB+fms_term_hdB)
  69. 0069specialize beta_sum_succ_decompose d
  70. 0070specialize beta_sum_succ_decompose e
  71. 0071specialize beta_sum_succ_decompose l
  72. 0072specialize beta_sum_succ_decompose m
  73. 0073apply beta_sum_succ_decompose
  74. 0074exact hm
  75. 0075cases hdB
  76. 0076cases hdB_witness
  77. 0077cases hdB_witness_witness
  78. 0078cases hdB_witness_witness_right
  79. 0079have hdC : exists fms_term_hdC fms_sum_hdC. (((exists fs_h_fms_hdC. fs_h_fms_hdC + S (fms_term_hdC) = S ((S (l)) * g)) /\ exists fs_q_fms_hdC. f = fs_q_fms_hdC * S ((S (l)) * g) + (fms_term_hdC))) /\ ((exists ff_u_fms_hdC ff_v_fms_hdC. ((((exists ff_h_fms_hdC_start. ff_h_fms_hdC_start + S (0) = S ((S (0)) * ff_v_fms_hdC)) /\ exists ff_q_fms_hdC_start. ff_u_fms_hdC = ff_q_fms_hdC_start * S ((S (0)) * ff_v_fms_hdC) + (0))) /\ ((((exists ff_h_fms_hdC_terminal. ff_h_fms_hdC_terminal + S ((fms_sum_hdC)) = S ((S ((l))) * ff_v_fms_hdC)) /\ exists ff_q_fms_hdC_terminal. ff_u_fms_hdC = ff_q_fms_hdC_terminal * S ((S ((l))) * ff_v_fms_hdC) + ((fms_sum_hdC)))) /\ forall ff_i_fms_hdC. (exists ff_lt_fms_hdC_bound. ff_lt_fms_hdC_bound + S ff_i_fms_hdC = (l)) -> exists ff_a_fms_hdC ff_r_fms_hdC ff_s_fms_hdC. ((((exists ff_h_fms_hdC_summand. ff_h_fms_hdC_summand + S (ff_a_fms_hdC) = S ((S (ff_i_fms_hdC)) * (g))) /\ exists ff_q_fms_hdC_summand. (f) = ff_q_fms_hdC_summand * S ((S (ff_i_fms_hdC)) * (g)) + (ff_a_fms_hdC))) /\ ((((exists ff_h_fms_hdC_partial. ff_h_fms_hdC_partial + S (ff_r_fms_hdC) = S ((S (ff_i_fms_hdC)) * ff_v_fms_hdC)) /\ exists ff_q_fms_hdC_partial. ff_u_fms_hdC = ff_q_fms_hdC_partial * S ((S (ff_i_fms_hdC)) * ff_v_fms_hdC) + (ff_r_fms_hdC))) /\ ((((exists ff_h_fms_hdC_successor. ff_h_fms_hdC_successor + S (ff_s_fms_hdC) = S ((S (S ff_i_fms_hdC)) * ff_v_fms_hdC)) /\ exists ff_q_fms_hdC_successor. ff_u_fms_hdC = ff_q_fms_hdC_successor * S ((S (S ff_i_fms_hdC)) * ff_v_fms_hdC) + (ff_s_fms_hdC))) /\ ff_s_fms_hdC = ff_r_fms_hdC + ff_a_fms_hdC)))))) /\ q=fms_sum_hdC+fms_term_hdC)
  80. 0080specialize beta_sum_succ_decompose f
  81. 0081specialize beta_sum_succ_decompose g
  82. 0082specialize beta_sum_succ_decompose l
  83. 0083specialize beta_sum_succ_decompose q
  84. 0084apply beta_sum_succ_decompose
  85. 0085exact hq
  86. 0086cases hdC
  87. 0087cases hdC_witness
  88. 0088cases hdC_witness_witness
  89. 0089cases hdC_witness_witness_right
  90. 0090have hdD : exists fms_term_hdD fms_sum_hdD. (((exists fs_h_fms_hdD. fs_h_fms_hdD + S (fms_term_hdD) = S ((S (l)) * t)) /\ exists fs_q_fms_hdD. h = fs_q_fms_hdD * S ((S (l)) * t) + (fms_term_hdD))) /\ ((exists ff_u_fms_hdD ff_v_fms_hdD. ((((exists ff_h_fms_hdD_start. ff_h_fms_hdD_start + S (0) = S ((S (0)) * ff_v_fms_hdD)) /\ exists ff_q_fms_hdD_start. ff_u_fms_hdD = ff_q_fms_hdD_start * S ((S (0)) * ff_v_fms_hdD) + (0))) /\ ((((exists ff_h_fms_hdD_terminal. ff_h_fms_hdD_terminal + S ((fms_sum_hdD)) = S ((S ((l))) * ff_v_fms_hdD)) /\ exists ff_q_fms_hdD_terminal. ff_u_fms_hdD = ff_q_fms_hdD_terminal * S ((S ((l))) * ff_v_fms_hdD) + ((fms_sum_hdD)))) /\ forall ff_i_fms_hdD. (exists ff_lt_fms_hdD_bound. ff_lt_fms_hdD_bound + S ff_i_fms_hdD = (l)) -> exists ff_a_fms_hdD ff_r_fms_hdD ff_s_fms_hdD. ((((exists ff_h_fms_hdD_summand. ff_h_fms_hdD_summand + S (ff_a_fms_hdD) = S ((S (ff_i_fms_hdD)) * (t))) /\ exists ff_q_fms_hdD_summand. (h) = ff_q_fms_hdD_summand * S ((S (ff_i_fms_hdD)) * (t)) + (ff_a_fms_hdD))) /\ ((((exists ff_h_fms_hdD_partial. ff_h_fms_hdD_partial + S (ff_r_fms_hdD) = S ((S (ff_i_fms_hdD)) * ff_v_fms_hdD)) /\ exists ff_q_fms_hdD_partial. ff_u_fms_hdD = ff_q_fms_hdD_partial * S ((S (ff_i_fms_hdD)) * ff_v_fms_hdD) + (ff_r_fms_hdD))) /\ ((((exists ff_h_fms_hdD_successor. ff_h_fms_hdD_successor + S (ff_s_fms_hdD) = S ((S (S ff_i_fms_hdD)) * ff_v_fms_hdD)) /\ exists ff_q_fms_hdD_successor. ff_u_fms_hdD = ff_q_fms_hdD_successor * S ((S (S ff_i_fms_hdD)) * ff_v_fms_hdD) + (ff_s_fms_hdD))) /\ ff_s_fms_hdD = ff_r_fms_hdD + ff_a_fms_hdD)))))) /\ r=fms_sum_hdD+fms_term_hdD)
  91. 0091specialize beta_sum_succ_decompose h
  92. 0092specialize beta_sum_succ_decompose t
  93. 0093specialize beta_sum_succ_decompose l
  94. 0094specialize beta_sum_succ_decompose r
  95. 0095apply beta_sum_succ_decompose
  96. 0096exact hr
  97. 0097cases hdD
  98. 0098cases hdD_witness
  99. 0099cases hdD_witness_witness
  100. 0100cases hdD_witness_witness_right
  101. 0101have hprefix : x1+x3=x5+x7
  102. 0102specialize IH x1
  103. 0103specialize IH x3
  104. 0104specialize IH x5
  105. 0105specialize IH x7
  106. 0106apply IH
  107. 0107exact hdA_witness_witness_right_left
  108. 0108exact hdB_witness_witness_right_left
  109. 0109exact hdC_witness_witness_right_left
  110. 0110exact hdD_witness_witness_right_left
  111. 0111intro i
  112. 0112intro a
  113. 0113intro v
  114. 0114intro w
  115. 0115intro z
  116. 0116intro hi
  117. 0117intro ha
  118. 0118intro hv
  119. 0119intro hw
  120. 0120intro hz
  121. 0121specialize hbalance i
  122. 0122specialize hbalance a
  123. 0123specialize hbalance v
  124. 0124specialize hbalance w
  125. 0125specialize hbalance z
  126. 0126apply hbalance
  127. 0127specialize le_succ S i
  128. 0128specialize le_succ l
  129. 0129apply le_succ
  130. 0130exact hi
  131. 0131exact ha
  132. 0132exact hv
  133. 0133exact hw
  134. 0134exact hz
  135. 0135have hlast : x+x2=x4+x6
  136. 0136specialize hbalance l
  137. 0137specialize hbalance x
  138. 0138specialize hbalance x2
  139. 0139specialize hbalance x4
  140. 0140specialize hbalance x6
  141. 0141apply hbalance
  142. 0142specialize le_refl S l
  143. 0143apply le_refl
  144. 0144exact hdA_witness_witness_left
  145. 0145exact hdB_witness_witness_left
  146. 0146exact hdC_witness_witness_left
  147. 0147exact hdD_witness_witness_left
  148. 0148rewrite hdA_witness_witness_right_right
  149. 0149rewrite hdB_witness_witness_right_right
  150. 0150rewrite hdC_witness_witness_right_right
  151. 0151rewrite hdD_witness_witness_right_right
  152. 0152trans (x1+x3)+(x+x2)
  153. 0153simp [add_assoc, add_comm]
  154. 0154rewrite hprefix
  155. 0155rewrite hlast
  156. 0156simp [add_assoc, add_comm]