DL008A

matrix_integer_signed_sum_balance

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

Arbitrary genuine finite signed sums preserve integer equality of their entries, via an actually constructed common cross-sum code and checked finite-sum additivity.

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 eb ec fb fc l p n P N. (forall ics_index_sum_pointwise ics_value0_sum_pointwise ics_value1_sum_pointwise ics_value2_sum_pointwise ics_value3_sum_pointwise. (exists ics_gap_sum_pointwise_bound. ics_gap_sum_pointwise_bound + S (ics_index_sum_pointwise) = (l)) -> (((exists fs_h_ics_sum_pointwise_at0. fs_h_ics_sum_pointwise_at0 + S (ics_value0_sum_pointwise) = S ((S (ics_index_sum_pointwise)) * ac)) /\ exists fs_q_ics_sum_pointwise_at0. ab = fs_q_ics_sum_pointwise_at0 * S ((S (ics_index_sum_pointwise)) * ac) + (ics_value0_sum_pointwise))) -> (((exists fs_h_ics_sum_pointwise_at1. fs_h_ics_sum_pointwise_at1 + S (ics_value1_sum_pointwise) = S ((S (ics_index_sum_pointwise)) * bc)) /\ exists fs_q_ics_sum_pointwise_at1. bb = fs_q_ics_sum_pointwise_at1 * S ((S (ics_index_sum_pointwise)) * bc) + (ics_value1_sum_pointwise))) -> (((exists fs_h_ics_sum_pointwise_at2. fs_h_ics_sum_pointwise_at2 + S (ics_value2_sum_pointwise) = S ((S (ics_index_sum_pointwise)) * ec)) /\ exists fs_q_ics_sum_pointwise_at2. eb = fs_q_ics_sum_pointwise_at2 * S ((S (ics_index_sum_pointwise)) * ec) + (ics_value2_sum_pointwise))) -> (((exists fs_h_ics_sum_pointwise_at3. fs_h_ics_sum_pointwise_at3 + S (ics_value3_sum_pointwise) = S ((S (ics_index_sum_pointwise)) * fc)) /\ exists fs_q_ics_sum_pointwise_at3. fb = fs_q_ics_sum_pointwise_at3 * S ((S (ics_index_sum_pointwise)) * fc) + (ics_value3_sum_pointwise))) -> ics_value0_sum_pointwise + ics_value3_sum_pointwise = ics_value2_sum_pointwise + ics_value1_sum_pointwise) -> (exists ff_u_mce_integer_sum_ap ff_v_mce_integer_sum_ap. ((((exists ff_h_mce_integer_sum_ap_start. ff_h_mce_integer_sum_ap_start + S (0) = S ((S (0)) * ff_v_mce_integer_sum_ap)) /\ exists ff_q_mce_integer_sum_ap_start. ff_u_mce_integer_sum_ap = ff_q_mce_integer_sum_ap_start * S ((S (0)) * ff_v_mce_integer_sum_ap) + (0))) /\ ((((exists ff_h_mce_integer_sum_ap_terminal. ff_h_mce_integer_sum_ap_terminal + S (p) = S ((S (l)) * ff_v_mce_integer_sum_ap)) /\ exists ff_q_mce_integer_sum_ap_terminal. ff_u_mce_integer_sum_ap = ff_q_mce_integer_sum_ap_terminal * S ((S (l)) * ff_v_mce_integer_sum_ap) + (p))) /\ forall ff_i_mce_integer_sum_ap. (exists ff_lt_mce_integer_sum_ap_bound. ff_lt_mce_integer_sum_ap_bound + S ff_i_mce_integer_sum_ap = l) -> exists ff_a_mce_integer_sum_ap ff_r_mce_integer_sum_ap ff_s_mce_integer_sum_ap. ((((exists ff_h_mce_integer_sum_ap_summand. ff_h_mce_integer_sum_ap_summand + S (ff_a_mce_integer_sum_ap) = S ((S (ff_i_mce_integer_sum_ap)) * ac)) /\ exists ff_q_mce_integer_sum_ap_summand. ab = ff_q_mce_integer_sum_ap_summand * S ((S (ff_i_mce_integer_sum_ap)) * ac) + (ff_a_mce_integer_sum_ap))) /\ ((((exists ff_h_mce_integer_sum_ap_partial. ff_h_mce_integer_sum_ap_partial + S (ff_r_mce_integer_sum_ap) = S ((S (ff_i_mce_integer_sum_ap)) * ff_v_mce_integer_sum_ap)) /\ exists ff_q_mce_integer_sum_ap_partial. ff_u_mce_integer_sum_ap = ff_q_mce_integer_sum_ap_partial * S ((S (ff_i_mce_integer_sum_ap)) * ff_v_mce_integer_sum_ap) + (ff_r_mce_integer_sum_ap))) /\ ((((exists ff_h_mce_integer_sum_ap_successor. ff_h_mce_integer_sum_ap_successor + S (ff_s_mce_integer_sum_ap) = S ((S (S ff_i_mce_integer_sum_ap)) * ff_v_mce_integer_sum_ap)) /\ exists ff_q_mce_integer_sum_ap_successor. ff_u_mce_integer_sum_ap = ff_q_mce_integer_sum_ap_successor * S ((S (S ff_i_mce_integer_sum_ap)) * ff_v_mce_integer_sum_ap) + (ff_s_mce_integer_sum_ap))) /\ ff_s_mce_integer_sum_ap = ff_r_mce_integer_sum_ap + ff_a_mce_integer_sum_ap)))))) -> (exists ff_u_mce_integer_sum_an ff_v_mce_integer_sum_an. ((((exists ff_h_mce_integer_sum_an_start. ff_h_mce_integer_sum_an_start + S (0) = S ((S (0)) * ff_v_mce_integer_sum_an)) /\ exists ff_q_mce_integer_sum_an_start. ff_u_mce_integer_sum_an = ff_q_mce_integer_sum_an_start * S ((S (0)) * ff_v_mce_integer_sum_an) + (0))) /\ ((((exists ff_h_mce_integer_sum_an_terminal. ff_h_mce_integer_sum_an_terminal + S (n) = S ((S (l)) * ff_v_mce_integer_sum_an)) /\ exists ff_q_mce_integer_sum_an_terminal. ff_u_mce_integer_sum_an = ff_q_mce_integer_sum_an_terminal * S ((S (l)) * ff_v_mce_integer_sum_an) + (n))) /\ forall ff_i_mce_integer_sum_an. (exists ff_lt_mce_integer_sum_an_bound. ff_lt_mce_integer_sum_an_bound + S ff_i_mce_integer_sum_an = l) -> exists ff_a_mce_integer_sum_an ff_r_mce_integer_sum_an ff_s_mce_integer_sum_an. ((((exists ff_h_mce_integer_sum_an_summand. ff_h_mce_integer_sum_an_summand + S (ff_a_mce_integer_sum_an) = S ((S (ff_i_mce_integer_sum_an)) * bc)) /\ exists ff_q_mce_integer_sum_an_summand. bb = ff_q_mce_integer_sum_an_summand * S ((S (ff_i_mce_integer_sum_an)) * bc) + (ff_a_mce_integer_sum_an))) /\ ((((exists ff_h_mce_integer_sum_an_partial. ff_h_mce_integer_sum_an_partial + S (ff_r_mce_integer_sum_an) = S ((S (ff_i_mce_integer_sum_an)) * ff_v_mce_integer_sum_an)) /\ exists ff_q_mce_integer_sum_an_partial. ff_u_mce_integer_sum_an = ff_q_mce_integer_sum_an_partial * S ((S (ff_i_mce_integer_sum_an)) * ff_v_mce_integer_sum_an) + (ff_r_mce_integer_sum_an))) /\ ((((exists ff_h_mce_integer_sum_an_successor. ff_h_mce_integer_sum_an_successor + S (ff_s_mce_integer_sum_an) = S ((S (S ff_i_mce_integer_sum_an)) * ff_v_mce_integer_sum_an)) /\ exists ff_q_mce_integer_sum_an_successor. ff_u_mce_integer_sum_an = ff_q_mce_integer_sum_an_successor * S ((S (S ff_i_mce_integer_sum_an)) * ff_v_mce_integer_sum_an) + (ff_s_mce_integer_sum_an))) /\ ff_s_mce_integer_sum_an = ff_r_mce_integer_sum_an + ff_a_mce_integer_sum_an)))))) -> (exists ff_u_mce_integer_sum_bp ff_v_mce_integer_sum_bp. ((((exists ff_h_mce_integer_sum_bp_start. ff_h_mce_integer_sum_bp_start + S (0) = S ((S (0)) * ff_v_mce_integer_sum_bp)) /\ exists ff_q_mce_integer_sum_bp_start. ff_u_mce_integer_sum_bp = ff_q_mce_integer_sum_bp_start * S ((S (0)) * ff_v_mce_integer_sum_bp) + (0))) /\ ((((exists ff_h_mce_integer_sum_bp_terminal. ff_h_mce_integer_sum_bp_terminal + S (P) = S ((S (l)) * ff_v_mce_integer_sum_bp)) /\ exists ff_q_mce_integer_sum_bp_terminal. ff_u_mce_integer_sum_bp = ff_q_mce_integer_sum_bp_terminal * S ((S (l)) * ff_v_mce_integer_sum_bp) + (P))) /\ forall ff_i_mce_integer_sum_bp. (exists ff_lt_mce_integer_sum_bp_bound. ff_lt_mce_integer_sum_bp_bound + S ff_i_mce_integer_sum_bp = l) -> exists ff_a_mce_integer_sum_bp ff_r_mce_integer_sum_bp ff_s_mce_integer_sum_bp. ((((exists ff_h_mce_integer_sum_bp_summand. ff_h_mce_integer_sum_bp_summand + S (ff_a_mce_integer_sum_bp) = S ((S (ff_i_mce_integer_sum_bp)) * ec)) /\ exists ff_q_mce_integer_sum_bp_summand. eb = ff_q_mce_integer_sum_bp_summand * S ((S (ff_i_mce_integer_sum_bp)) * ec) + (ff_a_mce_integer_sum_bp))) /\ ((((exists ff_h_mce_integer_sum_bp_partial. ff_h_mce_integer_sum_bp_partial + S (ff_r_mce_integer_sum_bp) = S ((S (ff_i_mce_integer_sum_bp)) * ff_v_mce_integer_sum_bp)) /\ exists ff_q_mce_integer_sum_bp_partial. ff_u_mce_integer_sum_bp = ff_q_mce_integer_sum_bp_partial * S ((S (ff_i_mce_integer_sum_bp)) * ff_v_mce_integer_sum_bp) + (ff_r_mce_integer_sum_bp))) /\ ((((exists ff_h_mce_integer_sum_bp_successor. ff_h_mce_integer_sum_bp_successor + S (ff_s_mce_integer_sum_bp) = S ((S (S ff_i_mce_integer_sum_bp)) * ff_v_mce_integer_sum_bp)) /\ exists ff_q_mce_integer_sum_bp_successor. ff_u_mce_integer_sum_bp = ff_q_mce_integer_sum_bp_successor * S ((S (S ff_i_mce_integer_sum_bp)) * ff_v_mce_integer_sum_bp) + (ff_s_mce_integer_sum_bp))) /\ ff_s_mce_integer_sum_bp = ff_r_mce_integer_sum_bp + ff_a_mce_integer_sum_bp)))))) -> (exists ff_u_mce_integer_sum_bn ff_v_mce_integer_sum_bn. ((((exists ff_h_mce_integer_sum_bn_start. ff_h_mce_integer_sum_bn_start + S (0) = S ((S (0)) * ff_v_mce_integer_sum_bn)) /\ exists ff_q_mce_integer_sum_bn_start. ff_u_mce_integer_sum_bn = ff_q_mce_integer_sum_bn_start * S ((S (0)) * ff_v_mce_integer_sum_bn) + (0))) /\ ((((exists ff_h_mce_integer_sum_bn_terminal. ff_h_mce_integer_sum_bn_terminal + S (N) = S ((S (l)) * ff_v_mce_integer_sum_bn)) /\ exists ff_q_mce_integer_sum_bn_terminal. ff_u_mce_integer_sum_bn = ff_q_mce_integer_sum_bn_terminal * S ((S (l)) * ff_v_mce_integer_sum_bn) + (N))) /\ forall ff_i_mce_integer_sum_bn. (exists ff_lt_mce_integer_sum_bn_bound. ff_lt_mce_integer_sum_bn_bound + S ff_i_mce_integer_sum_bn = l) -> exists ff_a_mce_integer_sum_bn ff_r_mce_integer_sum_bn ff_s_mce_integer_sum_bn. ((((exists ff_h_mce_integer_sum_bn_summand. ff_h_mce_integer_sum_bn_summand + S (ff_a_mce_integer_sum_bn) = S ((S (ff_i_mce_integer_sum_bn)) * fc)) /\ exists ff_q_mce_integer_sum_bn_summand. fb = ff_q_mce_integer_sum_bn_summand * S ((S (ff_i_mce_integer_sum_bn)) * fc) + (ff_a_mce_integer_sum_bn))) /\ ((((exists ff_h_mce_integer_sum_bn_partial. ff_h_mce_integer_sum_bn_partial + S (ff_r_mce_integer_sum_bn) = S ((S (ff_i_mce_integer_sum_bn)) * ff_v_mce_integer_sum_bn)) /\ exists ff_q_mce_integer_sum_bn_partial. ff_u_mce_integer_sum_bn = ff_q_mce_integer_sum_bn_partial * S ((S (ff_i_mce_integer_sum_bn)) * ff_v_mce_integer_sum_bn) + (ff_r_mce_integer_sum_bn))) /\ ((((exists ff_h_mce_integer_sum_bn_successor. ff_h_mce_integer_sum_bn_successor + S (ff_s_mce_integer_sum_bn) = S ((S (S ff_i_mce_integer_sum_bn)) * ff_v_mce_integer_sum_bn)) /\ exists ff_q_mce_integer_sum_bn_successor. ff_u_mce_integer_sum_bn = ff_q_mce_integer_sum_bn_successor * S ((S (S ff_i_mce_integer_sum_bn)) * ff_v_mce_integer_sum_bn) + (ff_s_mce_integer_sum_bn))) /\ ff_s_mce_integer_sum_bn = ff_r_mce_integer_sum_bn + ff_a_mce_integer_sum_bn)))))) -> p + N = P + n

Constructive proof overview

Generated structural guide

Arbitrary genuine finite signed sums preserve integer equality of their entries, via an actually constructed common cross-sum code and checked finite-sum additivity.

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

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

Proof neighborhood

Direct dependencies

beta_pointwise_add_prefix_exists Alpha theorem; checked-use authorized beta_sum_exists Stable theorem; checked-use authorized beta_sum_pointwise_add Alpha theorem; checked-use authorized beta_at_exists Stable theorem; checked-use authorized

Direct dependents

DL008C matrix_integer_cofactor_fold_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

109 script commands · 22 reading checkpoints · 6 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–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 eb
  6. L6
    intro ec
  7. L7
    intro fb
  8. L8
    intro fc
  9. L9
    intro l
  10. L10
    intro p
02Fix variables and assumptionsL11–18

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

  1. L11
    intro n
  2. L12
    intro P
  3. L13
    intro N
  4. L14
    intro hequal
  5. L15
    intro hap
  6. L16
    intro han
  7. L17
    intro hbp
  8. L18
    intro hbn
03Establish haddL19–25

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

  1. L19
    have hadd : ∃ b. ∃ c. MatrixPointwiseAdd(ab,ac,fb,fc,b,c,l)Definitions: MatrixPointwiseAdd
  2. L20
    specialize beta_pointwise_add_prefix_exists (ab)
  3. L21
    specialize beta_pointwise_add_prefix_exists (ac)
  4. L22
    specialize beta_pointwise_add_prefix_exists (fb)
  5. L23
    specialize beta_pointwise_add_prefix_exists (fc)
  6. L24
    specialize beta_pointwise_add_prefix_exists (l)
  7. L25
    apply beta_pointwise_add_prefix_exists
04Separate the logical casesL26–27

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

  1. L26
    cases hadd
  2. L27
    cases hadd_witness
05Establish hsumL28–32

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

  1. L28
    have hsum : ∃ s. Sum(x,x1,l,s)Definitions: Sum
  2. L29
    specialize beta_sum_exists (x)
  3. L30
    specialize beta_sum_exists (x1)
  4. L31
    specialize beta_sum_exists (l)
  5. L32
    apply beta_sum_exists
06Separate the logical casesL33–33

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

  1. L33
    cases hsum
07Establish hfirstL34–43

Establish this local claim before using it. It is not an additional assumption.

  1. L34
    have hfirst : p + N = x2
  2. L35
    specialize beta_sum_pointwise_add (ab)
  3. L36
    specialize beta_sum_pointwise_add (ac)
  4. L37
    specialize beta_sum_pointwise_add (fb)
  5. L38
    specialize beta_sum_pointwise_add (fc)
  6. L39
    specialize beta_sum_pointwise_add (x)
  7. L40
    specialize beta_sum_pointwise_add (x1)
  8. L41
    specialize beta_sum_pointwise_add (l)
  9. L42
    specialize beta_sum_pointwise_add (p)
  10. L43
    specialize beta_sum_pointwise_add (N)
08Use earlier factsL44–49

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

  1. L44
    specialize beta_sum_pointwise_add (x2)
  2. L45
    apply beta_sum_pointwise_add
  3. L46
    exact hap
  4. L47
    exact hbn
  5. L48
    exact hsum_witness
  6. L49
    exact hadd_witness_witness
09Establish hsecondL50–59

Establish this local claim before using it. It is not an additional assumption.

  1. L50
    have hsecond : P + n = x2
  2. L51
    specialize beta_sum_pointwise_add (eb)
  3. L52
    specialize beta_sum_pointwise_add (ec)
  4. L53
    specialize beta_sum_pointwise_add (bb)
  5. L54
    specialize beta_sum_pointwise_add (bc)
  6. L55
    specialize beta_sum_pointwise_add (x)
  7. L56
    specialize beta_sum_pointwise_add (x1)
  8. L57
    specialize beta_sum_pointwise_add (l)
  9. L58
    specialize beta_sum_pointwise_add (P)
  10. L59
    specialize beta_sum_pointwise_add (n)
10Use earlier factsL60–64

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

  1. L60
    specialize beta_sum_pointwise_add (x2)
  2. L61
    apply beta_sum_pointwise_add
  3. L62
    exact hbp
  4. L63
    exact han
  5. L64
    exact hsum_witness
11Fix variables and assumptionsL65–72

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

  1. L65
    intro i
  2. L66
    intro a
  3. L67
    intro b
  4. L68
    intro t
  5. L69
    intro hi
  6. L70
    intro ha
  7. L71
    intro hb
  8. L72
    intro ht
12Establish hleftL73–77

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

  1. L73
    have hleft : exists c. ((exists ff_h_mdr_integer_sum_left. ff_h_mdr_integer_sum_left + S (c) = S ((S (i)) * ac)) /\ exists ff_q_mdr_integer_sum_left. ab = ff_q_mdr_integer_sum_left * S ((S (i)) * ac) + (c))
  2. L74
    specialize beta_at_exists (ab)
  3. L75
    specialize beta_at_exists (ac)
  4. L76
    specialize beta_at_exists (i)
  5. L77
    apply beta_at_exists
13Separate the logical casesL78–78

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

  1. L78
    cases hleft
14Establish hrightL79–83

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

  1. L79
    have hright : exists d. ((exists ff_h_mdr_integer_sum_right. ff_h_mdr_integer_sum_right + S (d) = S ((S (i)) * fc)) /\ exists ff_q_mdr_integer_sum_right. fb = ff_q_mdr_integer_sum_right * S ((S (i)) * fc) + (d))
  2. L80
    specialize beta_at_exists (fb)
  3. L81
    specialize beta_at_exists (fc)
  4. L82
    specialize beta_at_exists (i)
  5. L83
    apply beta_at_exists
15Separate the logical casesL84–84

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

  1. L84
    cases hright
16Calculate and transport equalitiesL85–85

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

  1. L85
    trans x3 + x4
17Use earlier factsL86–95

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

  1. L86
    specialize hadd_witness_witness (i)
  2. L87
    specialize hadd_witness_witness (x3)
  3. L88
    specialize hadd_witness_witness (x4)
  4. L89
    specialize hadd_witness_witness (t)
  5. L90
    apply hadd_witness_witness
  6. L91
    exact hi
  7. L92
    exact hleft_witness
  8. L93
    exact hright_witness
  9. L94
    exact ht
  10. L95
    specialize hequal (i)
18Use earlier factsL96–105

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

  1. L96
    specialize hequal (x3)
  2. L97
    specialize hequal (b)
  3. L98
    specialize hequal (a)
  4. L99
    specialize hequal (x4)
  5. L100
    apply hequal
  6. L101
    exact hi
  7. L102
    exact hleft_witness
  8. L103
    exact hb
  9. L104
    exact ha
  10. L105
    exact hright_witness
19Calculate and transport equalitiesL106–106

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

  1. L106
    trans x2
20Use earlier factsL107–107

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

  1. L107
    exact hfirst
21Calculate and transport equalitiesL108–108

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

  1. L108
    symm
22Use earlier factsL109–109

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

  1. L109
    exact hsecond

Library-wide reading audit

Original exact command ledger · 109 lines
  1. 0001intro ab
  2. 0002intro ac
  3. 0003intro bb
  4. 0004intro bc
  5. 0005intro eb
  6. 0006intro ec
  7. 0007intro fb
  8. 0008intro fc
  9. 0009intro l
  10. 0010intro p
  11. 0011intro n
  12. 0012intro P
  13. 0013intro N
  14. 0014intro hequal
  15. 0015intro hap
  16. 0016intro han
  17. 0017intro hbp
  18. 0018intro hbn
  19. 0019have hadd : exists b c. (forall ff_index_mcp_add_ics_integer_cross_code ff_left_mcp_add_ics_integer_cross_code ff_right_mcp_add_ics_integer_cross_code ff_target_mcp_add_ics_integer_cross_code. (exists mcp_gap_ics_integer_cross_code_bound. mcp_gap_ics_integer_cross_code_bound + S (ff_index_mcp_add_ics_integer_cross_code) = (l)) -> (((exists fs_h_mcp_ics_integer_cross_code_left. fs_h_mcp_ics_integer_cross_code_left + S (ff_left_mcp_add_ics_integer_cross_code) = S ((S (ff_index_mcp_add_ics_integer_cross_code)) * ac)) /\ exists fs_q_mcp_ics_integer_cross_code_left. ab = fs_q_mcp_ics_integer_cross_code_left * S ((S (ff_index_mcp_add_ics_integer_cross_code)) * ac) + (ff_left_mcp_add_ics_integer_cross_code))) -> (((exists fs_h_mcp_ics_integer_cross_code_right. fs_h_mcp_ics_integer_cross_code_right + S (ff_right_mcp_add_ics_integer_cross_code) = S ((S (ff_index_mcp_add_ics_integer_cross_code)) * fc)) /\ exists fs_q_mcp_ics_integer_cross_code_right. fb = fs_q_mcp_ics_integer_cross_code_right * S ((S (ff_index_mcp_add_ics_integer_cross_code)) * fc) + (ff_right_mcp_add_ics_integer_cross_code))) -> (((exists fs_h_mcp_ics_integer_cross_code_target. fs_h_mcp_ics_integer_cross_code_target + S (ff_target_mcp_add_ics_integer_cross_code) = S ((S (ff_index_mcp_add_ics_integer_cross_code)) * c)) /\ exists fs_q_mcp_ics_integer_cross_code_target. b = fs_q_mcp_ics_integer_cross_code_target * S ((S (ff_index_mcp_add_ics_integer_cross_code)) * c) + (ff_target_mcp_add_ics_integer_cross_code))) -> ff_target_mcp_add_ics_integer_cross_code = ff_left_mcp_add_ics_integer_cross_code + ff_right_mcp_add_ics_integer_cross_code)
  20. 0020specialize beta_pointwise_add_prefix_exists (ab)
  21. 0021specialize beta_pointwise_add_prefix_exists (ac)
  22. 0022specialize beta_pointwise_add_prefix_exists (fb)
  23. 0023specialize beta_pointwise_add_prefix_exists (fc)
  24. 0024specialize beta_pointwise_add_prefix_exists (l)
  25. 0025apply beta_pointwise_add_prefix_exists
  26. 0026cases hadd
  27. 0027cases hadd_witness
  28. 0028have hsum : exists s. (exists ff_u_mce_integer_cross_sum ff_v_mce_integer_cross_sum. ((((exists ff_h_mce_integer_cross_sum_start. ff_h_mce_integer_cross_sum_start + S (0) = S ((S (0)) * ff_v_mce_integer_cross_sum)) /\ exists ff_q_mce_integer_cross_sum_start. ff_u_mce_integer_cross_sum = ff_q_mce_integer_cross_sum_start * S ((S (0)) * ff_v_mce_integer_cross_sum) + (0))) /\ ((((exists ff_h_mce_integer_cross_sum_terminal. ff_h_mce_integer_cross_sum_terminal + S (s) = S ((S (l)) * ff_v_mce_integer_cross_sum)) /\ exists ff_q_mce_integer_cross_sum_terminal. ff_u_mce_integer_cross_sum = ff_q_mce_integer_cross_sum_terminal * S ((S (l)) * ff_v_mce_integer_cross_sum) + (s))) /\ forall ff_i_mce_integer_cross_sum. (exists ff_lt_mce_integer_cross_sum_bound. ff_lt_mce_integer_cross_sum_bound + S ff_i_mce_integer_cross_sum = l) -> exists ff_a_mce_integer_cross_sum ff_r_mce_integer_cross_sum ff_s_mce_integer_cross_sum. ((((exists ff_h_mce_integer_cross_sum_summand. ff_h_mce_integer_cross_sum_summand + S (ff_a_mce_integer_cross_sum) = S ((S (ff_i_mce_integer_cross_sum)) * x1)) /\ exists ff_q_mce_integer_cross_sum_summand. x = ff_q_mce_integer_cross_sum_summand * S ((S (ff_i_mce_integer_cross_sum)) * x1) + (ff_a_mce_integer_cross_sum))) /\ ((((exists ff_h_mce_integer_cross_sum_partial. ff_h_mce_integer_cross_sum_partial + S (ff_r_mce_integer_cross_sum) = S ((S (ff_i_mce_integer_cross_sum)) * ff_v_mce_integer_cross_sum)) /\ exists ff_q_mce_integer_cross_sum_partial. ff_u_mce_integer_cross_sum = ff_q_mce_integer_cross_sum_partial * S ((S (ff_i_mce_integer_cross_sum)) * ff_v_mce_integer_cross_sum) + (ff_r_mce_integer_cross_sum))) /\ ((((exists ff_h_mce_integer_cross_sum_successor. ff_h_mce_integer_cross_sum_successor + S (ff_s_mce_integer_cross_sum) = S ((S (S ff_i_mce_integer_cross_sum)) * ff_v_mce_integer_cross_sum)) /\ exists ff_q_mce_integer_cross_sum_successor. ff_u_mce_integer_cross_sum = ff_q_mce_integer_cross_sum_successor * S ((S (S ff_i_mce_integer_cross_sum)) * ff_v_mce_integer_cross_sum) + (ff_s_mce_integer_cross_sum))) /\ ff_s_mce_integer_cross_sum = ff_r_mce_integer_cross_sum + ff_a_mce_integer_cross_sum))))))
  29. 0029specialize beta_sum_exists (x)
  30. 0030specialize beta_sum_exists (x1)
  31. 0031specialize beta_sum_exists (l)
  32. 0032apply beta_sum_exists
  33. 0033cases hsum
  34. 0034have hfirst : p + N = x2
  35. 0035specialize beta_sum_pointwise_add (ab)
  36. 0036specialize beta_sum_pointwise_add (ac)
  37. 0037specialize beta_sum_pointwise_add (fb)
  38. 0038specialize beta_sum_pointwise_add (fc)
  39. 0039specialize beta_sum_pointwise_add (x)
  40. 0040specialize beta_sum_pointwise_add (x1)
  41. 0041specialize beta_sum_pointwise_add (l)
  42. 0042specialize beta_sum_pointwise_add (p)
  43. 0043specialize beta_sum_pointwise_add (N)
  44. 0044specialize beta_sum_pointwise_add (x2)
  45. 0045apply beta_sum_pointwise_add
  46. 0046exact hap
  47. 0047exact hbn
  48. 0048exact hsum_witness
  49. 0049exact hadd_witness_witness
  50. 0050have hsecond : P + n = x2
  51. 0051specialize beta_sum_pointwise_add (eb)
  52. 0052specialize beta_sum_pointwise_add (ec)
  53. 0053specialize beta_sum_pointwise_add (bb)
  54. 0054specialize beta_sum_pointwise_add (bc)
  55. 0055specialize beta_sum_pointwise_add (x)
  56. 0056specialize beta_sum_pointwise_add (x1)
  57. 0057specialize beta_sum_pointwise_add (l)
  58. 0058specialize beta_sum_pointwise_add (P)
  59. 0059specialize beta_sum_pointwise_add (n)
  60. 0060specialize beta_sum_pointwise_add (x2)
  61. 0061apply beta_sum_pointwise_add
  62. 0062exact hbp
  63. 0063exact han
  64. 0064exact hsum_witness
  65. 0065intro i
  66. 0066intro a
  67. 0067intro b
  68. 0068intro t
  69. 0069intro hi
  70. 0070intro ha
  71. 0071intro hb
  72. 0072intro ht
  73. 0073have hleft : exists c. ((exists ff_h_mdr_integer_sum_left. ff_h_mdr_integer_sum_left + S (c) = S ((S (i)) * ac)) /\ exists ff_q_mdr_integer_sum_left. ab = ff_q_mdr_integer_sum_left * S ((S (i)) * ac) + (c))
  74. 0074specialize beta_at_exists (ab)
  75. 0075specialize beta_at_exists (ac)
  76. 0076specialize beta_at_exists (i)
  77. 0077apply beta_at_exists
  78. 0078cases hleft
  79. 0079have hright : exists d. ((exists ff_h_mdr_integer_sum_right. ff_h_mdr_integer_sum_right + S (d) = S ((S (i)) * fc)) /\ exists ff_q_mdr_integer_sum_right. fb = ff_q_mdr_integer_sum_right * S ((S (i)) * fc) + (d))
  80. 0080specialize beta_at_exists (fb)
  81. 0081specialize beta_at_exists (fc)
  82. 0082specialize beta_at_exists (i)
  83. 0083apply beta_at_exists
  84. 0084cases hright
  85. 0085trans x3 + x4
  86. 0086specialize hadd_witness_witness (i)
  87. 0087specialize hadd_witness_witness (x3)
  88. 0088specialize hadd_witness_witness (x4)
  89. 0089specialize hadd_witness_witness (t)
  90. 0090apply hadd_witness_witness
  91. 0091exact hi
  92. 0092exact hleft_witness
  93. 0093exact hright_witness
  94. 0094exact ht
  95. 0095specialize hequal (i)
  96. 0096specialize hequal (x3)
  97. 0097specialize hequal (b)
  98. 0098specialize hequal (a)
  99. 0099specialize hequal (x4)
  100. 0100apply hequal
  101. 0101exact hi
  102. 0102exact hleft_witness
  103. 0103exact hb
  104. 0104exact ha
  105. 0105exact hright_witness
  106. 0106trans x2
  107. 0107exact hfirst
  108. 0108symm
  109. 0109exact hsecond