DL0068

integer_span_pointwise_add_interchange

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

Five actual pointwise sum relations imply the regrouped sixth relation at every coordinate, with no assumption about canonical beta encodings.

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 ab ac bb bc cb cc db dc eb ec fb fc pb pc qb qc rb rc l. (forall ff_index_mcp_add_ics_interchange_first ff_left_mcp_add_ics_interchange_first ff_right_mcp_add_ics_interchange_first ff_target_mcp_add_ics_interchange_first. (exists mcp_gap_ics_interchange_first_bound. mcp_gap_ics_interchange_first_bound + S (ff_index_mcp_add_ics_interchange_first) = (l)) -> (((exists fs_h_mcp_ics_interchange_first_left. fs_h_mcp_ics_interchange_first_left + S (ff_left_mcp_add_ics_interchange_first) = S ((S (ff_index_mcp_add_ics_interchange_first)) * ac)) /\ exists fs_q_mcp_ics_interchange_first_left. ab = fs_q_mcp_ics_interchange_first_left * S ((S (ff_index_mcp_add_ics_interchange_first)) * ac) + (ff_left_mcp_add_ics_interchange_first))) -> (((exists fs_h_mcp_ics_interchange_first_right. fs_h_mcp_ics_interchange_first_right + S (ff_right_mcp_add_ics_interchange_first) = S ((S (ff_index_mcp_add_ics_interchange_first)) * bc)) /\ exists fs_q_mcp_ics_interchange_first_right. bb = fs_q_mcp_ics_interchange_first_right * S ((S (ff_index_mcp_add_ics_interchange_first)) * bc) + (ff_right_mcp_add_ics_interchange_first))) -> (((exists fs_h_mcp_ics_interchange_first_target. fs_h_mcp_ics_interchange_first_target + S (ff_target_mcp_add_ics_interchange_first) = S ((S (ff_index_mcp_add_ics_interchange_first)) * pc)) /\ exists fs_q_mcp_ics_interchange_first_target. pb = fs_q_mcp_ics_interchange_first_target * S ((S (ff_index_mcp_add_ics_interchange_first)) * pc) + (ff_target_mcp_add_ics_interchange_first))) -> ff_target_mcp_add_ics_interchange_first = ff_left_mcp_add_ics_interchange_first + ff_right_mcp_add_ics_interchange_first) -> (forall ff_index_mcp_add_ics_interchange_second ff_left_mcp_add_ics_interchange_second ff_right_mcp_add_ics_interchange_second ff_target_mcp_add_ics_interchange_second. (exists mcp_gap_ics_interchange_second_bound. mcp_gap_ics_interchange_second_bound + S (ff_index_mcp_add_ics_interchange_second) = (l)) -> (((exists fs_h_mcp_ics_interchange_second_left. fs_h_mcp_ics_interchange_second_left + S (ff_left_mcp_add_ics_interchange_second) = S ((S (ff_index_mcp_add_ics_interchange_second)) * cc)) /\ exists fs_q_mcp_ics_interchange_second_left. cb = fs_q_mcp_ics_interchange_second_left * S ((S (ff_index_mcp_add_ics_interchange_second)) * cc) + (ff_left_mcp_add_ics_interchange_second))) -> (((exists fs_h_mcp_ics_interchange_second_right. fs_h_mcp_ics_interchange_second_right + S (ff_right_mcp_add_ics_interchange_second) = S ((S (ff_index_mcp_add_ics_interchange_second)) * dc)) /\ exists fs_q_mcp_ics_interchange_second_right. db = fs_q_mcp_ics_interchange_second_right * S ((S (ff_index_mcp_add_ics_interchange_second)) * dc) + (ff_right_mcp_add_ics_interchange_second))) -> (((exists fs_h_mcp_ics_interchange_second_target. fs_h_mcp_ics_interchange_second_target + S (ff_target_mcp_add_ics_interchange_second) = S ((S (ff_index_mcp_add_ics_interchange_second)) * qc)) /\ exists fs_q_mcp_ics_interchange_second_target. qb = fs_q_mcp_ics_interchange_second_target * S ((S (ff_index_mcp_add_ics_interchange_second)) * qc) + (ff_target_mcp_add_ics_interchange_second))) -> ff_target_mcp_add_ics_interchange_second = ff_left_mcp_add_ics_interchange_second + ff_right_mcp_add_ics_interchange_second) -> (forall ff_index_mcp_add_ics_interchange_total ff_left_mcp_add_ics_interchange_total ff_right_mcp_add_ics_interchange_total ff_target_mcp_add_ics_interchange_total. (exists mcp_gap_ics_interchange_total_bound. mcp_gap_ics_interchange_total_bound + S (ff_index_mcp_add_ics_interchange_total) = (l)) -> (((exists fs_h_mcp_ics_interchange_total_left. fs_h_mcp_ics_interchange_total_left + S (ff_left_mcp_add_ics_interchange_total) = S ((S (ff_index_mcp_add_ics_interchange_total)) * ec)) /\ exists fs_q_mcp_ics_interchange_total_left. eb = fs_q_mcp_ics_interchange_total_left * S ((S (ff_index_mcp_add_ics_interchange_total)) * ec) + (ff_left_mcp_add_ics_interchange_total))) -> (((exists fs_h_mcp_ics_interchange_total_right. fs_h_mcp_ics_interchange_total_right + S (ff_right_mcp_add_ics_interchange_total) = S ((S (ff_index_mcp_add_ics_interchange_total)) * fc)) /\ exists fs_q_mcp_ics_interchange_total_right. fb = fs_q_mcp_ics_interchange_total_right * S ((S (ff_index_mcp_add_ics_interchange_total)) * fc) + (ff_right_mcp_add_ics_interchange_total))) -> (((exists fs_h_mcp_ics_interchange_total_target. fs_h_mcp_ics_interchange_total_target + S (ff_target_mcp_add_ics_interchange_total) = S ((S (ff_index_mcp_add_ics_interchange_total)) * rc)) /\ exists fs_q_mcp_ics_interchange_total_target. rb = fs_q_mcp_ics_interchange_total_target * S ((S (ff_index_mcp_add_ics_interchange_total)) * rc) + (ff_target_mcp_add_ics_interchange_total))) -> ff_target_mcp_add_ics_interchange_total = ff_left_mcp_add_ics_interchange_total + ff_right_mcp_add_ics_interchange_total) -> (forall ff_index_mcp_add_ics_interchange_vertical_first ff_left_mcp_add_ics_interchange_vertical_first ff_right_mcp_add_ics_interchange_vertical_first ff_target_mcp_add_ics_interchange_vertical_first. (exists mcp_gap_ics_interchange_vertical_first_bound. mcp_gap_ics_interchange_vertical_first_bound + S (ff_index_mcp_add_ics_interchange_vertical_first) = (l)) -> (((exists fs_h_mcp_ics_interchange_vertical_first_left. fs_h_mcp_ics_interchange_vertical_first_left + S (ff_left_mcp_add_ics_interchange_vertical_first) = S ((S (ff_index_mcp_add_ics_interchange_vertical_first)) * ac)) /\ exists fs_q_mcp_ics_interchange_vertical_first_left. ab = fs_q_mcp_ics_interchange_vertical_first_left * S ((S (ff_index_mcp_add_ics_interchange_vertical_first)) * ac) + (ff_left_mcp_add_ics_interchange_vertical_first))) -> (((exists fs_h_mcp_ics_interchange_vertical_first_right. fs_h_mcp_ics_interchange_vertical_first_right + S (ff_right_mcp_add_ics_interchange_vertical_first) = S ((S (ff_index_mcp_add_ics_interchange_vertical_first)) * cc)) /\ exists fs_q_mcp_ics_interchange_vertical_first_right. cb = fs_q_mcp_ics_interchange_vertical_first_right * S ((S (ff_index_mcp_add_ics_interchange_vertical_first)) * cc) + (ff_right_mcp_add_ics_interchange_vertical_first))) -> (((exists fs_h_mcp_ics_interchange_vertical_first_target. fs_h_mcp_ics_interchange_vertical_first_target + S (ff_target_mcp_add_ics_interchange_vertical_first) = S ((S (ff_index_mcp_add_ics_interchange_vertical_first)) * ec)) /\ exists fs_q_mcp_ics_interchange_vertical_first_target. eb = fs_q_mcp_ics_interchange_vertical_first_target * S ((S (ff_index_mcp_add_ics_interchange_vertical_first)) * ec) + (ff_target_mcp_add_ics_interchange_vertical_first))) -> ff_target_mcp_add_ics_interchange_vertical_first = ff_left_mcp_add_ics_interchange_vertical_first + ff_right_mcp_add_ics_interchange_vertical_first) -> (forall ff_index_mcp_add_ics_interchange_vertical_second ff_left_mcp_add_ics_interchange_vertical_second ff_right_mcp_add_ics_interchange_vertical_second ff_target_mcp_add_ics_interchange_vertical_second. (exists mcp_gap_ics_interchange_vertical_second_bound. mcp_gap_ics_interchange_vertical_second_bound + S (ff_index_mcp_add_ics_interchange_vertical_second) = (l)) -> (((exists fs_h_mcp_ics_interchange_vertical_second_left. fs_h_mcp_ics_interchange_vertical_second_left + S (ff_left_mcp_add_ics_interchange_vertical_second) = S ((S (ff_index_mcp_add_ics_interchange_vertical_second)) * bc)) /\ exists fs_q_mcp_ics_interchange_vertical_second_left. bb = fs_q_mcp_ics_interchange_vertical_second_left * S ((S (ff_index_mcp_add_ics_interchange_vertical_second)) * bc) + (ff_left_mcp_add_ics_interchange_vertical_second))) -> (((exists fs_h_mcp_ics_interchange_vertical_second_right. fs_h_mcp_ics_interchange_vertical_second_right + S (ff_right_mcp_add_ics_interchange_vertical_second) = S ((S (ff_index_mcp_add_ics_interchange_vertical_second)) * dc)) /\ exists fs_q_mcp_ics_interchange_vertical_second_right. db = fs_q_mcp_ics_interchange_vertical_second_right * S ((S (ff_index_mcp_add_ics_interchange_vertical_second)) * dc) + (ff_right_mcp_add_ics_interchange_vertical_second))) -> (((exists fs_h_mcp_ics_interchange_vertical_second_target. fs_h_mcp_ics_interchange_vertical_second_target + S (ff_target_mcp_add_ics_interchange_vertical_second) = S ((S (ff_index_mcp_add_ics_interchange_vertical_second)) * fc)) /\ exists fs_q_mcp_ics_interchange_vertical_second_target. fb = fs_q_mcp_ics_interchange_vertical_second_target * S ((S (ff_index_mcp_add_ics_interchange_vertical_second)) * fc) + (ff_target_mcp_add_ics_interchange_vertical_second))) -> ff_target_mcp_add_ics_interchange_vertical_second = ff_left_mcp_add_ics_interchange_vertical_second + ff_right_mcp_add_ics_interchange_vertical_second) -> (forall ff_index_mcp_add_ics_interchange_result ff_left_mcp_add_ics_interchange_result ff_right_mcp_add_ics_interchange_result ff_target_mcp_add_ics_interchange_result. (exists mcp_gap_ics_interchange_result_bound. mcp_gap_ics_interchange_result_bound + S (ff_index_mcp_add_ics_interchange_result) = (l)) -> (((exists fs_h_mcp_ics_interchange_result_left. fs_h_mcp_ics_interchange_result_left + S (ff_left_mcp_add_ics_interchange_result) = S ((S (ff_index_mcp_add_ics_interchange_result)) * pc)) /\ exists fs_q_mcp_ics_interchange_result_left. pb = fs_q_mcp_ics_interchange_result_left * S ((S (ff_index_mcp_add_ics_interchange_result)) * pc) + (ff_left_mcp_add_ics_interchange_result))) -> (((exists fs_h_mcp_ics_interchange_result_right. fs_h_mcp_ics_interchange_result_right + S (ff_right_mcp_add_ics_interchange_result) = S ((S (ff_index_mcp_add_ics_interchange_result)) * qc)) /\ exists fs_q_mcp_ics_interchange_result_right. qb = fs_q_mcp_ics_interchange_result_right * S ((S (ff_index_mcp_add_ics_interchange_result)) * qc) + (ff_right_mcp_add_ics_interchange_result))) -> (((exists fs_h_mcp_ics_interchange_result_target. fs_h_mcp_ics_interchange_result_target + S (ff_target_mcp_add_ics_interchange_result) = S ((S (ff_index_mcp_add_ics_interchange_result)) * rc)) /\ exists fs_q_mcp_ics_interchange_result_target. rb = fs_q_mcp_ics_interchange_result_target * S ((S (ff_index_mcp_add_ics_interchange_result)) * rc) + (ff_target_mcp_add_ics_interchange_result))) -> ff_target_mcp_add_ics_interchange_result = ff_left_mcp_add_ics_interchange_result + ff_right_mcp_add_ics_interchange_result)

Constructive proof overview

Generated structural guide

Five actual pointwise sum relations imply the regrouped sixth relation at every coordinate, with no assumption about canonical beta encodings.

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

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

Proof neighborhood

Direct dependencies

beta_at_exists Stable theorem; checked-use authorized add_shuffle_middle Alpha theorem; checked-use authorized

Direct dependents

DL006B integer_span_signed_product_add_right

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

131 script commands · 31 reading checkpoints · 11 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

01Fix variables and assumptionsL1–10

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

  1. L1
    intro ab
  2. L2
    intro ac
  3. L3
    intro bb
  4. L4
    intro bc
  5. L5
    intro cb
  6. L6
    intro cc
  7. L7
    intro db
  8. L8
    intro dc
  9. L9
    intro eb
  10. L10
    intro ec
02Fix variables and assumptionsL11–20

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

  1. L11
    intro fb
  2. L12
    intro fc
  3. L13
    intro pb
  4. L14
    intro pc
  5. L15
    intro qb
  6. L16
    intro qc
  7. L17
    intro rb
  8. L18
    intro rc
  9. L19
    intro l
  10. L20
    intro hfirst
03Fix variables and assumptionsL21–30

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

  1. L21
    intro hsecond
  2. L22
    intro htotal
  3. L23
    intro hleft
  4. L24
    intro hright
  5. L25
    intro i
  6. L26
    intro v
  7. L27
    intro w
  8. L28
    intro z
  9. L29
    intro hi
  10. L30
    intro hv
04Fix variables and assumptionsL31–32

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

  1. L31
    intro hw
  2. L32
    intro hz
05Establish ha0L33–37

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

  1. L33
    have ha0 : exists value. (((exists fs_h_ics_interchange_value0. fs_h_ics_interchange_value0 + S (value) = S ((S (i)) * ac)) /\ exists fs_q_ics_interchange_value0. ab = fs_q_ics_interchange_value0 * S ((S (i)) * ac) + (value)))
  2. L34
    specialize beta_at_exists (ab)
  3. L35
    specialize beta_at_exists (ac)
  4. L36
    specialize beta_at_exists (i)
  5. L37
    apply beta_at_exists
06Separate the logical casesL38–38

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

  1. L38
    cases ha0
07Establish ha1L39–43

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

  1. L39
    have ha1 : exists value. (((exists fs_h_ics_interchange_value1. fs_h_ics_interchange_value1 + S (value) = S ((S (i)) * bc)) /\ exists fs_q_ics_interchange_value1. bb = fs_q_ics_interchange_value1 * S ((S (i)) * bc) + (value)))
  2. L40
    specialize beta_at_exists (bb)
  3. L41
    specialize beta_at_exists (bc)
  4. L42
    specialize beta_at_exists (i)
  5. L43
    apply beta_at_exists
08Separate the logical casesL44–44

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

  1. L44
    cases ha1
09Establish ha2L45–49

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

  1. L45
    have ha2 : exists value. (((exists fs_h_ics_interchange_value2. fs_h_ics_interchange_value2 + S (value) = S ((S (i)) * cc)) /\ exists fs_q_ics_interchange_value2. cb = fs_q_ics_interchange_value2 * S ((S (i)) * cc) + (value)))
  2. L46
    specialize beta_at_exists (cb)
  3. L47
    specialize beta_at_exists (cc)
  4. L48
    specialize beta_at_exists (i)
  5. L49
    apply beta_at_exists
10Separate the logical casesL50–50

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

  1. L50
    cases ha2
11Establish ha3L51–55

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

  1. L51
    have ha3 : exists value. (((exists fs_h_ics_interchange_value3. fs_h_ics_interchange_value3 + S (value) = S ((S (i)) * dc)) /\ exists fs_q_ics_interchange_value3. db = fs_q_ics_interchange_value3 * S ((S (i)) * dc) + (value)))
  2. L52
    specialize beta_at_exists (db)
  3. L53
    specialize beta_at_exists (dc)
  4. L54
    specialize beta_at_exists (i)
  5. L55
    apply beta_at_exists
12Separate the logical casesL56–56

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

  1. L56
    cases ha3
13Establish ha4L57–61

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

  1. L57
    have ha4 : exists value. (((exists fs_h_ics_interchange_value4. fs_h_ics_interchange_value4 + S (value) = S ((S (i)) * ec)) /\ exists fs_q_ics_interchange_value4. eb = fs_q_ics_interchange_value4 * S ((S (i)) * ec) + (value)))
  2. L58
    specialize beta_at_exists (eb)
  3. L59
    specialize beta_at_exists (ec)
  4. L60
    specialize beta_at_exists (i)
  5. L61
    apply beta_at_exists
14Separate the logical casesL62–62

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

  1. L62
    cases ha4
15Establish ha5L63–67

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

  1. L63
    have ha5 : exists value. (((exists fs_h_ics_interchange_value5. fs_h_ics_interchange_value5 + S (value) = S ((S (i)) * fc)) /\ exists fs_q_ics_interchange_value5. fb = fs_q_ics_interchange_value5 * S ((S (i)) * fc) + (value)))
  2. L64
    specialize beta_at_exists (fb)
  3. L65
    specialize beta_at_exists (fc)
  4. L66
    specialize beta_at_exists (i)
  5. L67
    apply beta_at_exists
16Separate the logical casesL68–68

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

  1. L68
    cases ha5
17Establish heqvL69–78

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

  1. L69
    have heqv : v = x + x1
  2. L70
    specialize hfirst (i)
  3. L71
    specialize hfirst (x)
  4. L72
    specialize hfirst (x1)
  5. L73
    specialize hfirst (v)
  6. L74
    apply hfirst
  7. L75
    exact hi
  8. L76
    exact ha0_witness
  9. L77
    exact ha1_witness
  10. L78
    exact hv
18Establish heqwL79–88

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

  1. L79
    have heqw : w = x2 + x3
  2. L80
    specialize hsecond (i)
  3. L81
    specialize hsecond (x2)
  4. L82
    specialize hsecond (x3)
  5. L83
    specialize hsecond (w)
  6. L84
    apply hsecond
  7. L85
    exact hi
  8. L86
    exact ha2_witness
  9. L87
    exact ha3_witness
  10. L88
    exact hw
19Establish heqzL89–98

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

  1. L89
    have heqz : z = x4 + x5
  2. L90
    specialize htotal (i)
  3. L91
    specialize htotal (x4)
  4. L92
    specialize htotal (x5)
  5. L93
    specialize htotal (z)
  6. L94
    apply htotal
  7. L95
    exact hi
  8. L96
    exact ha4_witness
  9. L97
    exact ha5_witness
  10. L98
    exact hz
20Establish heqleftL99–108

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

  1. L99
    have heqleft : x4 = x + x2
  2. L100
    specialize hleft (i)
  3. L101
    specialize hleft (x)
  4. L102
    specialize hleft (x2)
  5. L103
    specialize hleft (x4)
  6. L104
    apply hleft
  7. L105
    exact hi
  8. L106
    exact ha0_witness
  9. L107
    exact ha2_witness
  10. L108
    exact ha4_witness
21Establish heqrightL109–118

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

  1. L109
    have heqright : x5 = x1 + x3
  2. L110
    specialize hright (i)
  3. L111
    specialize hright (x1)
  4. L112
    specialize hright (x3)
  5. L113
    specialize hright (x5)
  6. L114
    apply hright
  7. L115
    exact hi
  8. L116
    exact ha1_witness
  9. L117
    exact ha3_witness
  10. L118
    exact ha5_witness
22Calculate and transport equalitiesL119–119

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

  1. L119
    trans x4 + x5
23Use earlier factsL120–120

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

  1. L120
    exact heqz
24Calculate and transport equalitiesL121–122

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

  1. L121
    trans (x + x2) + (x1 + x3)
  2. L122
    congr
25Use earlier factsL123–124

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

  1. L123
    exact heqleft
  2. L124
    exact heqright
26Calculate and transport equalitiesL125–125

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

  1. L125
    trans (x + x1) + (x2 + x3)
27Use earlier factsL126–126

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

  1. L126
    apply add_shuffle_middle
28Calculate and transport equalitiesL127–128

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

  1. L127
    congr
  2. L128
    symm
29Use earlier factsL129–129

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

  1. L129
    exact heqv
30Calculate and transport equalitiesL130–130

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

  1. L130
    symm
31Use earlier factsL131–131

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

  1. L131
    exact heqw

Library-wide reading audit

Original exact command ledger · 131 lines
  1. 0001intro ab
  2. 0002intro ac
  3. 0003intro bb
  4. 0004intro bc
  5. 0005intro cb
  6. 0006intro cc
  7. 0007intro db
  8. 0008intro dc
  9. 0009intro eb
  10. 0010intro ec
  11. 0011intro fb
  12. 0012intro fc
  13. 0013intro pb
  14. 0014intro pc
  15. 0015intro qb
  16. 0016intro qc
  17. 0017intro rb
  18. 0018intro rc
  19. 0019intro l
  20. 0020intro hfirst
  21. 0021intro hsecond
  22. 0022intro htotal
  23. 0023intro hleft
  24. 0024intro hright
  25. 0025intro i
  26. 0026intro v
  27. 0027intro w
  28. 0028intro z
  29. 0029intro hi
  30. 0030intro hv
  31. 0031intro hw
  32. 0032intro hz
  33. 0033have ha0 : exists value. (((exists fs_h_ics_interchange_value0. fs_h_ics_interchange_value0 + S (value) = S ((S (i)) * ac)) /\ exists fs_q_ics_interchange_value0. ab = fs_q_ics_interchange_value0 * S ((S (i)) * ac) + (value)))
  34. 0034specialize beta_at_exists (ab)
  35. 0035specialize beta_at_exists (ac)
  36. 0036specialize beta_at_exists (i)
  37. 0037apply beta_at_exists
  38. 0038cases ha0
  39. 0039have ha1 : exists value. (((exists fs_h_ics_interchange_value1. fs_h_ics_interchange_value1 + S (value) = S ((S (i)) * bc)) /\ exists fs_q_ics_interchange_value1. bb = fs_q_ics_interchange_value1 * S ((S (i)) * bc) + (value)))
  40. 0040specialize beta_at_exists (bb)
  41. 0041specialize beta_at_exists (bc)
  42. 0042specialize beta_at_exists (i)
  43. 0043apply beta_at_exists
  44. 0044cases ha1
  45. 0045have ha2 : exists value. (((exists fs_h_ics_interchange_value2. fs_h_ics_interchange_value2 + S (value) = S ((S (i)) * cc)) /\ exists fs_q_ics_interchange_value2. cb = fs_q_ics_interchange_value2 * S ((S (i)) * cc) + (value)))
  46. 0046specialize beta_at_exists (cb)
  47. 0047specialize beta_at_exists (cc)
  48. 0048specialize beta_at_exists (i)
  49. 0049apply beta_at_exists
  50. 0050cases ha2
  51. 0051have ha3 : exists value. (((exists fs_h_ics_interchange_value3. fs_h_ics_interchange_value3 + S (value) = S ((S (i)) * dc)) /\ exists fs_q_ics_interchange_value3. db = fs_q_ics_interchange_value3 * S ((S (i)) * dc) + (value)))
  52. 0052specialize beta_at_exists (db)
  53. 0053specialize beta_at_exists (dc)
  54. 0054specialize beta_at_exists (i)
  55. 0055apply beta_at_exists
  56. 0056cases ha3
  57. 0057have ha4 : exists value. (((exists fs_h_ics_interchange_value4. fs_h_ics_interchange_value4 + S (value) = S ((S (i)) * ec)) /\ exists fs_q_ics_interchange_value4. eb = fs_q_ics_interchange_value4 * S ((S (i)) * ec) + (value)))
  58. 0058specialize beta_at_exists (eb)
  59. 0059specialize beta_at_exists (ec)
  60. 0060specialize beta_at_exists (i)
  61. 0061apply beta_at_exists
  62. 0062cases ha4
  63. 0063have ha5 : exists value. (((exists fs_h_ics_interchange_value5. fs_h_ics_interchange_value5 + S (value) = S ((S (i)) * fc)) /\ exists fs_q_ics_interchange_value5. fb = fs_q_ics_interchange_value5 * S ((S (i)) * fc) + (value)))
  64. 0064specialize beta_at_exists (fb)
  65. 0065specialize beta_at_exists (fc)
  66. 0066specialize beta_at_exists (i)
  67. 0067apply beta_at_exists
  68. 0068cases ha5
  69. 0069have heqv : v = x + x1
  70. 0070specialize hfirst (i)
  71. 0071specialize hfirst (x)
  72. 0072specialize hfirst (x1)
  73. 0073specialize hfirst (v)
  74. 0074apply hfirst
  75. 0075exact hi
  76. 0076exact ha0_witness
  77. 0077exact ha1_witness
  78. 0078exact hv
  79. 0079have heqw : w = x2 + x3
  80. 0080specialize hsecond (i)
  81. 0081specialize hsecond (x2)
  82. 0082specialize hsecond (x3)
  83. 0083specialize hsecond (w)
  84. 0084apply hsecond
  85. 0085exact hi
  86. 0086exact ha2_witness
  87. 0087exact ha3_witness
  88. 0088exact hw
  89. 0089have heqz : z = x4 + x5
  90. 0090specialize htotal (i)
  91. 0091specialize htotal (x4)
  92. 0092specialize htotal (x5)
  93. 0093specialize htotal (z)
  94. 0094apply htotal
  95. 0095exact hi
  96. 0096exact ha4_witness
  97. 0097exact ha5_witness
  98. 0098exact hz
  99. 0099have heqleft : x4 = x + x2
  100. 0100specialize hleft (i)
  101. 0101specialize hleft (x)
  102. 0102specialize hleft (x2)
  103. 0103specialize hleft (x4)
  104. 0104apply hleft
  105. 0105exact hi
  106. 0106exact ha0_witness
  107. 0107exact ha2_witness
  108. 0108exact ha4_witness
  109. 0109have heqright : x5 = x1 + x3
  110. 0110specialize hright (i)
  111. 0111specialize hright (x1)
  112. 0112specialize hright (x3)
  113. 0113specialize hright (x5)
  114. 0114apply hright
  115. 0115exact hi
  116. 0116exact ha1_witness
  117. 0117exact ha3_witness
  118. 0118exact ha5_witness
  119. 0119trans x4 + x5
  120. 0120exact heqz
  121. 0121trans (x + x2) + (x1 + x3)
  122. 0122congr
  123. 0123exact heqleft
  124. 0124exact heqright
  125. 0125trans (x + x1) + (x2 + x3)
  126. 0126apply add_shuffle_middle
  127. 0127congr
  128. 0128symm
  129. 0129exact heqv
  130. 0130symm
  131. 0131exact heqw