DL0064

integer_span_dot_product_pointwise_add

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

Actual finite dot products add whenever their decoded multiplicands satisfy the displayed pointwise distributive equation; checked finite-sum additivity supplies the full arbitrary-length result.

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 l L M N. (exists ff_code_dot_ics_dot_first ff_scale_dot_ics_dot_first. ((forall fpmp_index_dot_ics_dot_first_pointwise fpmp_left_dot_ics_dot_first_pointwise fpmp_right_dot_ics_dot_first_pointwise fpmp_target_dot_ics_dot_first_pointwise. (exists fpmp_gap_dot_ics_dot_first_pointwise. fpmp_gap_dot_ics_dot_first_pointwise + S fpmp_index_dot_ics_dot_first_pointwise = l) -> (((exists ff_h_fpmp_dot_ics_dot_first_pointwise_left. ff_h_fpmp_dot_ics_dot_first_pointwise_left + S (fpmp_left_dot_ics_dot_first_pointwise) = S ((S (fpmp_index_dot_ics_dot_first_pointwise)) * ac)) /\ exists ff_q_fpmp_dot_ics_dot_first_pointwise_left. ab = ff_q_fpmp_dot_ics_dot_first_pointwise_left * S ((S (fpmp_index_dot_ics_dot_first_pointwise)) * ac) + (fpmp_left_dot_ics_dot_first_pointwise))) -> (((exists ff_h_fpmp_dot_ics_dot_first_pointwise_right. ff_h_fpmp_dot_ics_dot_first_pointwise_right + S (fpmp_right_dot_ics_dot_first_pointwise) = S ((S (fpmp_index_dot_ics_dot_first_pointwise)) * bc)) /\ exists ff_q_fpmp_dot_ics_dot_first_pointwise_right. bb = ff_q_fpmp_dot_ics_dot_first_pointwise_right * S ((S (fpmp_index_dot_ics_dot_first_pointwise)) * bc) + (fpmp_right_dot_ics_dot_first_pointwise))) -> (((exists ff_h_fpmp_dot_ics_dot_first_pointwise_target. ff_h_fpmp_dot_ics_dot_first_pointwise_target + S (fpmp_target_dot_ics_dot_first_pointwise) = S ((S (fpmp_index_dot_ics_dot_first_pointwise)) * ff_scale_dot_ics_dot_first)) /\ exists ff_q_fpmp_dot_ics_dot_first_pointwise_target. ff_code_dot_ics_dot_first = ff_q_fpmp_dot_ics_dot_first_pointwise_target * S ((S (fpmp_index_dot_ics_dot_first_pointwise)) * ff_scale_dot_ics_dot_first) + (fpmp_target_dot_ics_dot_first_pointwise))) -> fpmp_target_dot_ics_dot_first_pointwise = fpmp_left_dot_ics_dot_first_pointwise * fpmp_right_dot_ics_dot_first_pointwise) /\ (exists ff_u_dot_ics_dot_first_sum ff_v_dot_ics_dot_first_sum. ((((exists ff_h_dot_ics_dot_first_sum_start. ff_h_dot_ics_dot_first_sum_start + S (0) = S ((S (0)) * ff_v_dot_ics_dot_first_sum)) /\ exists ff_q_dot_ics_dot_first_sum_start. ff_u_dot_ics_dot_first_sum = ff_q_dot_ics_dot_first_sum_start * S ((S (0)) * ff_v_dot_ics_dot_first_sum) + (0))) /\ ((((exists ff_h_dot_ics_dot_first_sum_terminal. ff_h_dot_ics_dot_first_sum_terminal + S (L) = S ((S (l)) * ff_v_dot_ics_dot_first_sum)) /\ exists ff_q_dot_ics_dot_first_sum_terminal. ff_u_dot_ics_dot_first_sum = ff_q_dot_ics_dot_first_sum_terminal * S ((S (l)) * ff_v_dot_ics_dot_first_sum) + (L))) /\ forall ff_i_dot_ics_dot_first_sum. (exists ff_lt_dot_ics_dot_first_sum_bound. ff_lt_dot_ics_dot_first_sum_bound + S ff_i_dot_ics_dot_first_sum = l) -> exists ff_a_dot_ics_dot_first_sum ff_r_dot_ics_dot_first_sum ff_s_dot_ics_dot_first_sum. ((((exists ff_h_dot_ics_dot_first_sum_summand. ff_h_dot_ics_dot_first_sum_summand + S (ff_a_dot_ics_dot_first_sum) = S ((S (ff_i_dot_ics_dot_first_sum)) * ff_scale_dot_ics_dot_first)) /\ exists ff_q_dot_ics_dot_first_sum_summand. ff_code_dot_ics_dot_first = ff_q_dot_ics_dot_first_sum_summand * S ((S (ff_i_dot_ics_dot_first_sum)) * ff_scale_dot_ics_dot_first) + (ff_a_dot_ics_dot_first_sum))) /\ ((((exists ff_h_dot_ics_dot_first_sum_partial. ff_h_dot_ics_dot_first_sum_partial + S (ff_r_dot_ics_dot_first_sum) = S ((S (ff_i_dot_ics_dot_first_sum)) * ff_v_dot_ics_dot_first_sum)) /\ exists ff_q_dot_ics_dot_first_sum_partial. ff_u_dot_ics_dot_first_sum = ff_q_dot_ics_dot_first_sum_partial * S ((S (ff_i_dot_ics_dot_first_sum)) * ff_v_dot_ics_dot_first_sum) + (ff_r_dot_ics_dot_first_sum))) /\ ((((exists ff_h_dot_ics_dot_first_sum_successor. ff_h_dot_ics_dot_first_sum_successor + S (ff_s_dot_ics_dot_first_sum) = S ((S (S ff_i_dot_ics_dot_first_sum)) * ff_v_dot_ics_dot_first_sum)) /\ exists ff_q_dot_ics_dot_first_sum_successor. ff_u_dot_ics_dot_first_sum = ff_q_dot_ics_dot_first_sum_successor * S ((S (S ff_i_dot_ics_dot_first_sum)) * ff_v_dot_ics_dot_first_sum) + (ff_s_dot_ics_dot_first_sum))) /\ ff_s_dot_ics_dot_first_sum = ff_r_dot_ics_dot_first_sum + ff_a_dot_ics_dot_first_sum)))))))) -> (exists ff_code_dot_ics_dot_second ff_scale_dot_ics_dot_second. ((forall fpmp_index_dot_ics_dot_second_pointwise fpmp_left_dot_ics_dot_second_pointwise fpmp_right_dot_ics_dot_second_pointwise fpmp_target_dot_ics_dot_second_pointwise. (exists fpmp_gap_dot_ics_dot_second_pointwise. fpmp_gap_dot_ics_dot_second_pointwise + S fpmp_index_dot_ics_dot_second_pointwise = l) -> (((exists ff_h_fpmp_dot_ics_dot_second_pointwise_left. ff_h_fpmp_dot_ics_dot_second_pointwise_left + S (fpmp_left_dot_ics_dot_second_pointwise) = S ((S (fpmp_index_dot_ics_dot_second_pointwise)) * cc)) /\ exists ff_q_fpmp_dot_ics_dot_second_pointwise_left. cb = ff_q_fpmp_dot_ics_dot_second_pointwise_left * S ((S (fpmp_index_dot_ics_dot_second_pointwise)) * cc) + (fpmp_left_dot_ics_dot_second_pointwise))) -> (((exists ff_h_fpmp_dot_ics_dot_second_pointwise_right. ff_h_fpmp_dot_ics_dot_second_pointwise_right + S (fpmp_right_dot_ics_dot_second_pointwise) = S ((S (fpmp_index_dot_ics_dot_second_pointwise)) * dc)) /\ exists ff_q_fpmp_dot_ics_dot_second_pointwise_right. db = ff_q_fpmp_dot_ics_dot_second_pointwise_right * S ((S (fpmp_index_dot_ics_dot_second_pointwise)) * dc) + (fpmp_right_dot_ics_dot_second_pointwise))) -> (((exists ff_h_fpmp_dot_ics_dot_second_pointwise_target. ff_h_fpmp_dot_ics_dot_second_pointwise_target + S (fpmp_target_dot_ics_dot_second_pointwise) = S ((S (fpmp_index_dot_ics_dot_second_pointwise)) * ff_scale_dot_ics_dot_second)) /\ exists ff_q_fpmp_dot_ics_dot_second_pointwise_target. ff_code_dot_ics_dot_second = ff_q_fpmp_dot_ics_dot_second_pointwise_target * S ((S (fpmp_index_dot_ics_dot_second_pointwise)) * ff_scale_dot_ics_dot_second) + (fpmp_target_dot_ics_dot_second_pointwise))) -> fpmp_target_dot_ics_dot_second_pointwise = fpmp_left_dot_ics_dot_second_pointwise * fpmp_right_dot_ics_dot_second_pointwise) /\ (exists ff_u_dot_ics_dot_second_sum ff_v_dot_ics_dot_second_sum. ((((exists ff_h_dot_ics_dot_second_sum_start. ff_h_dot_ics_dot_second_sum_start + S (0) = S ((S (0)) * ff_v_dot_ics_dot_second_sum)) /\ exists ff_q_dot_ics_dot_second_sum_start. ff_u_dot_ics_dot_second_sum = ff_q_dot_ics_dot_second_sum_start * S ((S (0)) * ff_v_dot_ics_dot_second_sum) + (0))) /\ ((((exists ff_h_dot_ics_dot_second_sum_terminal. ff_h_dot_ics_dot_second_sum_terminal + S (M) = S ((S (l)) * ff_v_dot_ics_dot_second_sum)) /\ exists ff_q_dot_ics_dot_second_sum_terminal. ff_u_dot_ics_dot_second_sum = ff_q_dot_ics_dot_second_sum_terminal * S ((S (l)) * ff_v_dot_ics_dot_second_sum) + (M))) /\ forall ff_i_dot_ics_dot_second_sum. (exists ff_lt_dot_ics_dot_second_sum_bound. ff_lt_dot_ics_dot_second_sum_bound + S ff_i_dot_ics_dot_second_sum = l) -> exists ff_a_dot_ics_dot_second_sum ff_r_dot_ics_dot_second_sum ff_s_dot_ics_dot_second_sum. ((((exists ff_h_dot_ics_dot_second_sum_summand. ff_h_dot_ics_dot_second_sum_summand + S (ff_a_dot_ics_dot_second_sum) = S ((S (ff_i_dot_ics_dot_second_sum)) * ff_scale_dot_ics_dot_second)) /\ exists ff_q_dot_ics_dot_second_sum_summand. ff_code_dot_ics_dot_second = ff_q_dot_ics_dot_second_sum_summand * S ((S (ff_i_dot_ics_dot_second_sum)) * ff_scale_dot_ics_dot_second) + (ff_a_dot_ics_dot_second_sum))) /\ ((((exists ff_h_dot_ics_dot_second_sum_partial. ff_h_dot_ics_dot_second_sum_partial + S (ff_r_dot_ics_dot_second_sum) = S ((S (ff_i_dot_ics_dot_second_sum)) * ff_v_dot_ics_dot_second_sum)) /\ exists ff_q_dot_ics_dot_second_sum_partial. ff_u_dot_ics_dot_second_sum = ff_q_dot_ics_dot_second_sum_partial * S ((S (ff_i_dot_ics_dot_second_sum)) * ff_v_dot_ics_dot_second_sum) + (ff_r_dot_ics_dot_second_sum))) /\ ((((exists ff_h_dot_ics_dot_second_sum_successor. ff_h_dot_ics_dot_second_sum_successor + S (ff_s_dot_ics_dot_second_sum) = S ((S (S ff_i_dot_ics_dot_second_sum)) * ff_v_dot_ics_dot_second_sum)) /\ exists ff_q_dot_ics_dot_second_sum_successor. ff_u_dot_ics_dot_second_sum = ff_q_dot_ics_dot_second_sum_successor * S ((S (S ff_i_dot_ics_dot_second_sum)) * ff_v_dot_ics_dot_second_sum) + (ff_s_dot_ics_dot_second_sum))) /\ ff_s_dot_ics_dot_second_sum = ff_r_dot_ics_dot_second_sum + ff_a_dot_ics_dot_second_sum)))))))) -> (exists ff_code_dot_ics_dot_third ff_scale_dot_ics_dot_third. ((forall fpmp_index_dot_ics_dot_third_pointwise fpmp_left_dot_ics_dot_third_pointwise fpmp_right_dot_ics_dot_third_pointwise fpmp_target_dot_ics_dot_third_pointwise. (exists fpmp_gap_dot_ics_dot_third_pointwise. fpmp_gap_dot_ics_dot_third_pointwise + S fpmp_index_dot_ics_dot_third_pointwise = l) -> (((exists ff_h_fpmp_dot_ics_dot_third_pointwise_left. ff_h_fpmp_dot_ics_dot_third_pointwise_left + S (fpmp_left_dot_ics_dot_third_pointwise) = S ((S (fpmp_index_dot_ics_dot_third_pointwise)) * ec)) /\ exists ff_q_fpmp_dot_ics_dot_third_pointwise_left. eb = ff_q_fpmp_dot_ics_dot_third_pointwise_left * S ((S (fpmp_index_dot_ics_dot_third_pointwise)) * ec) + (fpmp_left_dot_ics_dot_third_pointwise))) -> (((exists ff_h_fpmp_dot_ics_dot_third_pointwise_right. ff_h_fpmp_dot_ics_dot_third_pointwise_right + S (fpmp_right_dot_ics_dot_third_pointwise) = S ((S (fpmp_index_dot_ics_dot_third_pointwise)) * fc)) /\ exists ff_q_fpmp_dot_ics_dot_third_pointwise_right. fb = ff_q_fpmp_dot_ics_dot_third_pointwise_right * S ((S (fpmp_index_dot_ics_dot_third_pointwise)) * fc) + (fpmp_right_dot_ics_dot_third_pointwise))) -> (((exists ff_h_fpmp_dot_ics_dot_third_pointwise_target. ff_h_fpmp_dot_ics_dot_third_pointwise_target + S (fpmp_target_dot_ics_dot_third_pointwise) = S ((S (fpmp_index_dot_ics_dot_third_pointwise)) * ff_scale_dot_ics_dot_third)) /\ exists ff_q_fpmp_dot_ics_dot_third_pointwise_target. ff_code_dot_ics_dot_third = ff_q_fpmp_dot_ics_dot_third_pointwise_target * S ((S (fpmp_index_dot_ics_dot_third_pointwise)) * ff_scale_dot_ics_dot_third) + (fpmp_target_dot_ics_dot_third_pointwise))) -> fpmp_target_dot_ics_dot_third_pointwise = fpmp_left_dot_ics_dot_third_pointwise * fpmp_right_dot_ics_dot_third_pointwise) /\ (exists ff_u_dot_ics_dot_third_sum ff_v_dot_ics_dot_third_sum. ((((exists ff_h_dot_ics_dot_third_sum_start. ff_h_dot_ics_dot_third_sum_start + S (0) = S ((S (0)) * ff_v_dot_ics_dot_third_sum)) /\ exists ff_q_dot_ics_dot_third_sum_start. ff_u_dot_ics_dot_third_sum = ff_q_dot_ics_dot_third_sum_start * S ((S (0)) * ff_v_dot_ics_dot_third_sum) + (0))) /\ ((((exists ff_h_dot_ics_dot_third_sum_terminal. ff_h_dot_ics_dot_third_sum_terminal + S (N) = S ((S (l)) * ff_v_dot_ics_dot_third_sum)) /\ exists ff_q_dot_ics_dot_third_sum_terminal. ff_u_dot_ics_dot_third_sum = ff_q_dot_ics_dot_third_sum_terminal * S ((S (l)) * ff_v_dot_ics_dot_third_sum) + (N))) /\ forall ff_i_dot_ics_dot_third_sum. (exists ff_lt_dot_ics_dot_third_sum_bound. ff_lt_dot_ics_dot_third_sum_bound + S ff_i_dot_ics_dot_third_sum = l) -> exists ff_a_dot_ics_dot_third_sum ff_r_dot_ics_dot_third_sum ff_s_dot_ics_dot_third_sum. ((((exists ff_h_dot_ics_dot_third_sum_summand. ff_h_dot_ics_dot_third_sum_summand + S (ff_a_dot_ics_dot_third_sum) = S ((S (ff_i_dot_ics_dot_third_sum)) * ff_scale_dot_ics_dot_third)) /\ exists ff_q_dot_ics_dot_third_sum_summand. ff_code_dot_ics_dot_third = ff_q_dot_ics_dot_third_sum_summand * S ((S (ff_i_dot_ics_dot_third_sum)) * ff_scale_dot_ics_dot_third) + (ff_a_dot_ics_dot_third_sum))) /\ ((((exists ff_h_dot_ics_dot_third_sum_partial. ff_h_dot_ics_dot_third_sum_partial + S (ff_r_dot_ics_dot_third_sum) = S ((S (ff_i_dot_ics_dot_third_sum)) * ff_v_dot_ics_dot_third_sum)) /\ exists ff_q_dot_ics_dot_third_sum_partial. ff_u_dot_ics_dot_third_sum = ff_q_dot_ics_dot_third_sum_partial * S ((S (ff_i_dot_ics_dot_third_sum)) * ff_v_dot_ics_dot_third_sum) + (ff_r_dot_ics_dot_third_sum))) /\ ((((exists ff_h_dot_ics_dot_third_sum_successor. ff_h_dot_ics_dot_third_sum_successor + S (ff_s_dot_ics_dot_third_sum) = S ((S (S ff_i_dot_ics_dot_third_sum)) * ff_v_dot_ics_dot_third_sum)) /\ exists ff_q_dot_ics_dot_third_sum_successor. ff_u_dot_ics_dot_third_sum = ff_q_dot_ics_dot_third_sum_successor * S ((S (S ff_i_dot_ics_dot_third_sum)) * ff_v_dot_ics_dot_third_sum) + (ff_s_dot_ics_dot_third_sum))) /\ ff_s_dot_ics_dot_third_sum = ff_r_dot_ics_dot_third_sum + ff_a_dot_ics_dot_third_sum)))))))) -> (forall ics_index_dot_alignment ics_value0_dot_alignment ics_value1_dot_alignment ics_value2_dot_alignment ics_value3_dot_alignment ics_value4_dot_alignment ics_value5_dot_alignment. (exists ics_gap_dot_alignment_bound. ics_gap_dot_alignment_bound + S (ics_index_dot_alignment) = (l)) -> (((exists fs_h_ics_dot_alignment_at0. fs_h_ics_dot_alignment_at0 + S (ics_value0_dot_alignment) = S ((S (ics_index_dot_alignment)) * ac)) /\ exists fs_q_ics_dot_alignment_at0. ab = fs_q_ics_dot_alignment_at0 * S ((S (ics_index_dot_alignment)) * ac) + (ics_value0_dot_alignment))) -> (((exists fs_h_ics_dot_alignment_at1. fs_h_ics_dot_alignment_at1 + S (ics_value1_dot_alignment) = S ((S (ics_index_dot_alignment)) * bc)) /\ exists fs_q_ics_dot_alignment_at1. bb = fs_q_ics_dot_alignment_at1 * S ((S (ics_index_dot_alignment)) * bc) + (ics_value1_dot_alignment))) -> (((exists fs_h_ics_dot_alignment_at2. fs_h_ics_dot_alignment_at2 + S (ics_value2_dot_alignment) = S ((S (ics_index_dot_alignment)) * cc)) /\ exists fs_q_ics_dot_alignment_at2. cb = fs_q_ics_dot_alignment_at2 * S ((S (ics_index_dot_alignment)) * cc) + (ics_value2_dot_alignment))) -> (((exists fs_h_ics_dot_alignment_at3. fs_h_ics_dot_alignment_at3 + S (ics_value3_dot_alignment) = S ((S (ics_index_dot_alignment)) * dc)) /\ exists fs_q_ics_dot_alignment_at3. db = fs_q_ics_dot_alignment_at3 * S ((S (ics_index_dot_alignment)) * dc) + (ics_value3_dot_alignment))) -> (((exists fs_h_ics_dot_alignment_at4. fs_h_ics_dot_alignment_at4 + S (ics_value4_dot_alignment) = S ((S (ics_index_dot_alignment)) * ec)) /\ exists fs_q_ics_dot_alignment_at4. eb = fs_q_ics_dot_alignment_at4 * S ((S (ics_index_dot_alignment)) * ec) + (ics_value4_dot_alignment))) -> (((exists fs_h_ics_dot_alignment_at5. fs_h_ics_dot_alignment_at5 + S (ics_value5_dot_alignment) = S ((S (ics_index_dot_alignment)) * fc)) /\ exists fs_q_ics_dot_alignment_at5. fb = fs_q_ics_dot_alignment_at5 * S ((S (ics_index_dot_alignment)) * fc) + (ics_value5_dot_alignment))) -> ics_value4_dot_alignment * ics_value5_dot_alignment = ics_value0_dot_alignment * ics_value1_dot_alignment + ics_value2_dot_alignment * ics_value3_dot_alignment) -> L + M = N

Constructive proof overview

Generated structural guide

Actual finite dot products add whenever their decoded multiplicands satisfy the displayed pointwise distributive equation; checked finite-sum additivity supplies the full arbitrary-length result.

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

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

Proof neighborhood

Direct dependencies

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

Direct dependents

DL0065 integer_span_natural_cell_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

136 script commands · 28 reading checkpoints · 7 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 l
  4. L14
    intro L
  5. L15
    intro M
  6. L16
    intro N
  7. L17
    intro hf
  8. L18
    intro hg
  9. L19
    intro hh
  10. L20
    intro hpoint
03Separate the logical casesL21–29

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

  1. L21
    cases hf
  2. L22
    cases hf_witness
  3. L23
    cases hf_witness_witness
  4. L24
    cases hg
  5. L25
    cases hg_witness
  6. L26
    cases hg_witness_witness
  7. L27
    cases hh
  8. L28
    cases hh_witness
  9. L29
    cases hh_witness_witness
04Use earlier factsL30–39

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

  1. L30
    specialize beta_sum_pointwise_add (x)
  2. L31
    specialize beta_sum_pointwise_add (x1)
  3. L32
    specialize beta_sum_pointwise_add (x2)
  4. L33
    specialize beta_sum_pointwise_add (x3)
  5. L34
    specialize beta_sum_pointwise_add (x4)
  6. L35
    specialize beta_sum_pointwise_add (x5)
  7. L36
    specialize beta_sum_pointwise_add (l)
  8. L37
    specialize beta_sum_pointwise_add (L)
  9. L38
    specialize beta_sum_pointwise_add (M)
  10. L39
    specialize beta_sum_pointwise_add (N)
05Use earlier factsL40–43

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

  1. L40
    apply beta_sum_pointwise_add
  2. L41
    exact hf_witness_witness_right
  3. L42
    exact hg_witness_witness_right
  4. L43
    exact hh_witness_witness_right
06Fix variables and assumptionsL44–51

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

  1. L44
    intro i
  2. L45
    intro v
  3. L46
    intro w
  4. L47
    intro z
  5. L48
    intro hi
  6. L49
    intro hv
  7. L50
    intro hw
  8. L51
    intro hz
07Establish ha0L52–56

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

  1. L52
    have ha0 : exists value. (((exists fs_h_ics_dot_value0. fs_h_ics_dot_value0 + S (value) = S ((S (i)) * ac)) /\ exists fs_q_ics_dot_value0. ab = fs_q_ics_dot_value0 * S ((S (i)) * ac) + (value)))
  2. L53
    specialize beta_at_exists (ab)
  3. L54
    specialize beta_at_exists (ac)
  4. L55
    specialize beta_at_exists (i)
  5. L56
    apply beta_at_exists
08Separate the logical casesL57–57

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

  1. L57
    cases ha0
09Establish ha1L58–62

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

  1. L58
    have ha1 : exists value. (((exists fs_h_ics_dot_value1. fs_h_ics_dot_value1 + S (value) = S ((S (i)) * bc)) /\ exists fs_q_ics_dot_value1. bb = fs_q_ics_dot_value1 * S ((S (i)) * bc) + (value)))
  2. L59
    specialize beta_at_exists (bb)
  3. L60
    specialize beta_at_exists (bc)
  4. L61
    specialize beta_at_exists (i)
  5. L62
    apply beta_at_exists
10Separate the logical casesL63–63

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

  1. L63
    cases ha1
11Establish ha2L64–68

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

  1. L64
    have ha2 : exists value. (((exists fs_h_ics_dot_value2. fs_h_ics_dot_value2 + S (value) = S ((S (i)) * cc)) /\ exists fs_q_ics_dot_value2. cb = fs_q_ics_dot_value2 * S ((S (i)) * cc) + (value)))
  2. L65
    specialize beta_at_exists (cb)
  3. L66
    specialize beta_at_exists (cc)
  4. L67
    specialize beta_at_exists (i)
  5. L68
    apply beta_at_exists
12Separate the logical casesL69–69

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

  1. L69
    cases ha2
13Establish ha3L70–74

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

  1. L70
    have ha3 : exists value. (((exists fs_h_ics_dot_value3. fs_h_ics_dot_value3 + S (value) = S ((S (i)) * dc)) /\ exists fs_q_ics_dot_value3. db = fs_q_ics_dot_value3 * S ((S (i)) * dc) + (value)))
  2. L71
    specialize beta_at_exists (db)
  3. L72
    specialize beta_at_exists (dc)
  4. L73
    specialize beta_at_exists (i)
  5. L74
    apply beta_at_exists
14Separate the logical casesL75–75

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

  1. L75
    cases ha3
15Establish ha4L76–80

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

  1. L76
    have ha4 : exists value. (((exists fs_h_ics_dot_value4. fs_h_ics_dot_value4 + S (value) = S ((S (i)) * ec)) /\ exists fs_q_ics_dot_value4. eb = fs_q_ics_dot_value4 * S ((S (i)) * ec) + (value)))
  2. L77
    specialize beta_at_exists (eb)
  3. L78
    specialize beta_at_exists (ec)
  4. L79
    specialize beta_at_exists (i)
  5. L80
    apply beta_at_exists
16Separate the logical casesL81–81

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

  1. L81
    cases ha4
17Establish ha5L82–86

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

  1. L82
    have ha5 : exists value. (((exists fs_h_ics_dot_value5. fs_h_ics_dot_value5 + S (value) = S ((S (i)) * fc)) /\ exists fs_q_ics_dot_value5. fb = fs_q_ics_dot_value5 * S ((S (i)) * fc) + (value)))
  2. L83
    specialize beta_at_exists (fb)
  3. L84
    specialize beta_at_exists (fc)
  4. L85
    specialize beta_at_exists (i)
  5. L86
    apply beta_at_exists
18Separate the logical casesL87–87

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

  1. L87
    cases ha5
19Establish heqL88–97

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

  1. L88
    have heq : x10 * x11 = x6 * x7 + x8 * x9
  2. L89
    specialize hpoint (i)
  3. L90
    specialize hpoint (x6)
  4. L91
    specialize hpoint (x7)
  5. L92
    specialize hpoint (x8)
  6. L93
    specialize hpoint (x9)
  7. L94
    specialize hpoint (x10)
  8. L95
    specialize hpoint (x11)
  9. L96
    apply hpoint
  10. L97
    exact hi
20Use earlier factsL98–103

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

  1. L98
    exact ha0_witness
  2. L99
    exact ha1_witness
  3. L100
    exact ha2_witness
  4. L101
    exact ha3_witness
  5. L102
    exact ha4_witness
  6. L103
    exact ha5_witness
21Calculate and transport equalitiesL104–104

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

  1. L104
    trans x10 * x11
22Use earlier factsL105–113

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

  1. L105
    specialize hh_witness_witness_left (i)
  2. L106
    specialize hh_witness_witness_left (x10)
  3. L107
    specialize hh_witness_witness_left (x11)
  4. L108
    specialize hh_witness_witness_left (z)
  5. L109
    apply hh_witness_witness_left
  6. L110
    exact hi
  7. L111
    exact ha4_witness
  8. L112
    exact ha5_witness
  9. L113
    exact hz
23Calculate and transport equalitiesL114–114

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

  1. L114
    trans x6 * x7 + x8 * x9
24Use earlier factsL115–115

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

  1. L115
    exact heq
25Calculate and transport equalitiesL116–117

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

  1. L116
    congr
  2. L117
    symm
26Use earlier factsL118–126

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

  1. L118
    specialize hf_witness_witness_left (i)
  2. L119
    specialize hf_witness_witness_left (x6)
  3. L120
    specialize hf_witness_witness_left (x7)
  4. L121
    specialize hf_witness_witness_left (v)
  5. L122
    apply hf_witness_witness_left
  6. L123
    exact hi
  7. L124
    exact ha0_witness
  8. L125
    exact ha1_witness
  9. L126
    exact hv
27Calculate and transport equalitiesL127–127

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

  1. L127
    symm
28Use earlier factsL128–136

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

  1. L128
    specialize hg_witness_witness_left (i)
  2. L129
    specialize hg_witness_witness_left (x8)
  3. L130
    specialize hg_witness_witness_left (x9)
  4. L131
    specialize hg_witness_witness_left (w)
  5. L132
    apply hg_witness_witness_left
  6. L133
    exact hi
  7. L134
    exact ha2_witness
  8. L135
    exact ha3_witness
  9. L136
    exact hw

Library-wide reading audit

Original exact command ledger · 136 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 l
  14. 0014intro L
  15. 0015intro M
  16. 0016intro N
  17. 0017intro hf
  18. 0018intro hg
  19. 0019intro hh
  20. 0020intro hpoint
  21. 0021cases hf
  22. 0022cases hf_witness
  23. 0023cases hf_witness_witness
  24. 0024cases hg
  25. 0025cases hg_witness
  26. 0026cases hg_witness_witness
  27. 0027cases hh
  28. 0028cases hh_witness
  29. 0029cases hh_witness_witness
  30. 0030specialize beta_sum_pointwise_add (x)
  31. 0031specialize beta_sum_pointwise_add (x1)
  32. 0032specialize beta_sum_pointwise_add (x2)
  33. 0033specialize beta_sum_pointwise_add (x3)
  34. 0034specialize beta_sum_pointwise_add (x4)
  35. 0035specialize beta_sum_pointwise_add (x5)
  36. 0036specialize beta_sum_pointwise_add (l)
  37. 0037specialize beta_sum_pointwise_add (L)
  38. 0038specialize beta_sum_pointwise_add (M)
  39. 0039specialize beta_sum_pointwise_add (N)
  40. 0040apply beta_sum_pointwise_add
  41. 0041exact hf_witness_witness_right
  42. 0042exact hg_witness_witness_right
  43. 0043exact hh_witness_witness_right
  44. 0044intro i
  45. 0045intro v
  46. 0046intro w
  47. 0047intro z
  48. 0048intro hi
  49. 0049intro hv
  50. 0050intro hw
  51. 0051intro hz
  52. 0052have ha0 : exists value. (((exists fs_h_ics_dot_value0. fs_h_ics_dot_value0 + S (value) = S ((S (i)) * ac)) /\ exists fs_q_ics_dot_value0. ab = fs_q_ics_dot_value0 * S ((S (i)) * ac) + (value)))
  53. 0053specialize beta_at_exists (ab)
  54. 0054specialize beta_at_exists (ac)
  55. 0055specialize beta_at_exists (i)
  56. 0056apply beta_at_exists
  57. 0057cases ha0
  58. 0058have ha1 : exists value. (((exists fs_h_ics_dot_value1. fs_h_ics_dot_value1 + S (value) = S ((S (i)) * bc)) /\ exists fs_q_ics_dot_value1. bb = fs_q_ics_dot_value1 * S ((S (i)) * bc) + (value)))
  59. 0059specialize beta_at_exists (bb)
  60. 0060specialize beta_at_exists (bc)
  61. 0061specialize beta_at_exists (i)
  62. 0062apply beta_at_exists
  63. 0063cases ha1
  64. 0064have ha2 : exists value. (((exists fs_h_ics_dot_value2. fs_h_ics_dot_value2 + S (value) = S ((S (i)) * cc)) /\ exists fs_q_ics_dot_value2. cb = fs_q_ics_dot_value2 * S ((S (i)) * cc) + (value)))
  65. 0065specialize beta_at_exists (cb)
  66. 0066specialize beta_at_exists (cc)
  67. 0067specialize beta_at_exists (i)
  68. 0068apply beta_at_exists
  69. 0069cases ha2
  70. 0070have ha3 : exists value. (((exists fs_h_ics_dot_value3. fs_h_ics_dot_value3 + S (value) = S ((S (i)) * dc)) /\ exists fs_q_ics_dot_value3. db = fs_q_ics_dot_value3 * S ((S (i)) * dc) + (value)))
  71. 0071specialize beta_at_exists (db)
  72. 0072specialize beta_at_exists (dc)
  73. 0073specialize beta_at_exists (i)
  74. 0074apply beta_at_exists
  75. 0075cases ha3
  76. 0076have ha4 : exists value. (((exists fs_h_ics_dot_value4. fs_h_ics_dot_value4 + S (value) = S ((S (i)) * ec)) /\ exists fs_q_ics_dot_value4. eb = fs_q_ics_dot_value4 * S ((S (i)) * ec) + (value)))
  77. 0077specialize beta_at_exists (eb)
  78. 0078specialize beta_at_exists (ec)
  79. 0079specialize beta_at_exists (i)
  80. 0080apply beta_at_exists
  81. 0081cases ha4
  82. 0082have ha5 : exists value. (((exists fs_h_ics_dot_value5. fs_h_ics_dot_value5 + S (value) = S ((S (i)) * fc)) /\ exists fs_q_ics_dot_value5. fb = fs_q_ics_dot_value5 * S ((S (i)) * fc) + (value)))
  83. 0083specialize beta_at_exists (fb)
  84. 0084specialize beta_at_exists (fc)
  85. 0085specialize beta_at_exists (i)
  86. 0086apply beta_at_exists
  87. 0087cases ha5
  88. 0088have heq : x10 * x11 = x6 * x7 + x8 * x9
  89. 0089specialize hpoint (i)
  90. 0090specialize hpoint (x6)
  91. 0091specialize hpoint (x7)
  92. 0092specialize hpoint (x8)
  93. 0093specialize hpoint (x9)
  94. 0094specialize hpoint (x10)
  95. 0095specialize hpoint (x11)
  96. 0096apply hpoint
  97. 0097exact hi
  98. 0098exact ha0_witness
  99. 0099exact ha1_witness
  100. 0100exact ha2_witness
  101. 0101exact ha3_witness
  102. 0102exact ha4_witness
  103. 0103exact ha5_witness
  104. 0104trans x10 * x11
  105. 0105specialize hh_witness_witness_left (i)
  106. 0106specialize hh_witness_witness_left (x10)
  107. 0107specialize hh_witness_witness_left (x11)
  108. 0108specialize hh_witness_witness_left (z)
  109. 0109apply hh_witness_witness_left
  110. 0110exact hi
  111. 0111exact ha4_witness
  112. 0112exact ha5_witness
  113. 0113exact hz
  114. 0114trans x6 * x7 + x8 * x9
  115. 0115exact heq
  116. 0116congr
  117. 0117symm
  118. 0118specialize hf_witness_witness_left (i)
  119. 0119specialize hf_witness_witness_left (x6)
  120. 0120specialize hf_witness_witness_left (x7)
  121. 0121specialize hf_witness_witness_left (v)
  122. 0122apply hf_witness_witness_left
  123. 0123exact hi
  124. 0124exact ha0_witness
  125. 0125exact ha1_witness
  126. 0126exact hv
  127. 0127symm
  128. 0128specialize hg_witness_witness_left (i)
  129. 0129specialize hg_witness_witness_left (x8)
  130. 0130specialize hg_witness_witness_left (x9)
  131. 0131specialize hg_witness_witness_left (w)
  132. 0132apply hg_witness_witness_left
  133. 0133exact hi
  134. 0134exact ha2_witness
  135. 0135exact ha3_witness
  136. 0136exact hw