DL0065

integer_span_natural_cell_add_right

Each genuine row-by-column multiplication cell distributes over an actual coded sum of coefficient vectors; the old affine row and column slices are aligned at every coordinate.

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

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.

This branch proves the finite determinant/rank/span substrate. It does not claim Smith or Hermite normal form, lattice index equals determinant, determinant multiplicativity, lattice reduction, or geometry-of-numbers theorems.

Exact theorem in conservative defined notation

∀ ab. ∀ ac. ∀ bb. ∀ bc. ∀ cb. ∀ cc. ∀ db. ∀ dc. ∀ w. ∀ row. ∀ L. ∀ M. ∀ N. MatrixPointwiseAdd(bb,bc,cb,cc,db,dc,w) → MatrixProductCell(ab,ac,bb,bc,w,1,row,0,L) → MatrixProductCell(ab,ac,cb,cc,w,1,row,0,M) → MatrixProductCell(ab,ac,db,dc,w,1,row,0,N) → L + M = N

Every linked abbreviation expands hygienically to the identical original native formula.

Definition DAG

MatrixProductCell(lb,lc,rb,rc,w,v,i,j,n) · 3MatrixPointwiseAdd(mb,mc,sb,sc,tb,tc,l) · 1BetaAt(b,c,i,x) · 4

Actual proof prerequisites

integer_span_dot_product_pointwise_addbeta_at_exists · checked external prerequisitemul_add · checked external prerequisiteone_mul · checked external prerequisitezero_add · checked external prerequisite
Original expanded first-order statement 
forall ab ac bb bc cb cc db dc w row L M N. (forall ff_index_mcp_add_ics_cell_coeff_add ff_left_mcp_add_ics_cell_coeff_add ff_right_mcp_add_ics_cell_coeff_add ff_target_mcp_add_ics_cell_coeff_add. (exists mcp_gap_ics_cell_coeff_add_bound. mcp_gap_ics_cell_coeff_add_bound + S (ff_index_mcp_add_ics_cell_coeff_add) = (w)) -> (((exists fs_h_mcp_ics_cell_coeff_add_left. fs_h_mcp_ics_cell_coeff_add_left + S (ff_left_mcp_add_ics_cell_coeff_add) = S ((S (ff_index_mcp_add_ics_cell_coeff_add)) * bc)) /\ exists fs_q_mcp_ics_cell_coeff_add_left. bb = fs_q_mcp_ics_cell_coeff_add_left * S ((S (ff_index_mcp_add_ics_cell_coeff_add)) * bc) + (ff_left_mcp_add_ics_cell_coeff_add))) -> (((exists fs_h_mcp_ics_cell_coeff_add_right. fs_h_mcp_ics_cell_coeff_add_right + S (ff_right_mcp_add_ics_cell_coeff_add) = S ((S (ff_index_mcp_add_ics_cell_coeff_add)) * cc)) /\ exists fs_q_mcp_ics_cell_coeff_add_right. cb = fs_q_mcp_ics_cell_coeff_add_right * S ((S (ff_index_mcp_add_ics_cell_coeff_add)) * cc) + (ff_right_mcp_add_ics_cell_coeff_add))) -> (((exists fs_h_mcp_ics_cell_coeff_add_target. fs_h_mcp_ics_cell_coeff_add_target + S (ff_target_mcp_add_ics_cell_coeff_add) = S ((S (ff_index_mcp_add_ics_cell_coeff_add)) * dc)) /\ exists fs_q_mcp_ics_cell_coeff_add_target. db = fs_q_mcp_ics_cell_coeff_add_target * S ((S (ff_index_mcp_add_ics_cell_coeff_add)) * dc) + (ff_target_mcp_add_ics_cell_coeff_add))) -> ff_target_mcp_add_ics_cell_coeff_add = ff_left_mcp_add_ics_cell_coeff_add + ff_right_mcp_add_ics_cell_coeff_add) -> (exists ff_left_mcp_cell_ics_cell_first ff_left_scale_mcp_cell_ics_cell_first ff_right_mcp_cell_ics_cell_first ff_right_scale_mcp_cell_ics_cell_first. ((forall ff_index_mcp_ics_cell_first_row ff_source_mcp_ics_cell_first_row ff_target_mcp_ics_cell_first_row. (exists mcp_gap_ics_cell_first_row_bound. mcp_gap_ics_cell_first_row_bound + S (ff_index_mcp_ics_cell_first_row) = (w)) -> (((exists fs_h_mcp_ics_cell_first_row_source. fs_h_mcp_ics_cell_first_row_source + S (ff_source_mcp_ics_cell_first_row) = S ((S (((row) * (w)) + (1) * ff_index_mcp_ics_cell_first_row)) * ac)) /\ exists fs_q_mcp_ics_cell_first_row_source. ab = fs_q_mcp_ics_cell_first_row_source * S ((S (((row) * (w)) + (1) * ff_index_mcp_ics_cell_first_row)) * ac) + (ff_source_mcp_ics_cell_first_row))) -> (((exists fs_h_mcp_ics_cell_first_row_target. fs_h_mcp_ics_cell_first_row_target + S (ff_target_mcp_ics_cell_first_row) = S ((S (ff_index_mcp_ics_cell_first_row)) * ff_left_scale_mcp_cell_ics_cell_first)) /\ exists fs_q_mcp_ics_cell_first_row_target. ff_left_mcp_cell_ics_cell_first = fs_q_mcp_ics_cell_first_row_target * S ((S (ff_index_mcp_ics_cell_first_row)) * ff_left_scale_mcp_cell_ics_cell_first) + (ff_target_mcp_ics_cell_first_row))) -> ff_target_mcp_ics_cell_first_row = ff_source_mcp_ics_cell_first_row) /\ ((forall ff_index_mcp_ics_cell_first_column ff_source_mcp_ics_cell_first_column ff_target_mcp_ics_cell_first_column. (exists mcp_gap_ics_cell_first_column_bound. mcp_gap_ics_cell_first_column_bound + S (ff_index_mcp_ics_cell_first_column) = (w)) -> (((exists fs_h_mcp_ics_cell_first_column_source. fs_h_mcp_ics_cell_first_column_source + S (ff_source_mcp_ics_cell_first_column) = S ((S ((0) + (1) * ff_index_mcp_ics_cell_first_column)) * bc)) /\ exists fs_q_mcp_ics_cell_first_column_source. bb = fs_q_mcp_ics_cell_first_column_source * S ((S ((0) + (1) * ff_index_mcp_ics_cell_first_column)) * bc) + (ff_source_mcp_ics_cell_first_column))) -> (((exists fs_h_mcp_ics_cell_first_column_target. fs_h_mcp_ics_cell_first_column_target + S (ff_target_mcp_ics_cell_first_column) = S ((S (ff_index_mcp_ics_cell_first_column)) * ff_right_scale_mcp_cell_ics_cell_first)) /\ exists fs_q_mcp_ics_cell_first_column_target. ff_right_mcp_cell_ics_cell_first = fs_q_mcp_ics_cell_first_column_target * S ((S (ff_index_mcp_ics_cell_first_column)) * ff_right_scale_mcp_cell_ics_cell_first) + (ff_target_mcp_ics_cell_first_column))) -> ff_target_mcp_ics_cell_first_column = ff_source_mcp_ics_cell_first_column) /\ (exists ff_code_dot_mcp_ics_cell_first_dot ff_scale_dot_mcp_ics_cell_first_dot. ((forall fpmp_index_dot_mcp_ics_cell_first_dot_pointwise fpmp_left_dot_mcp_ics_cell_first_dot_pointwise fpmp_right_dot_mcp_ics_cell_first_dot_pointwise fpmp_target_dot_mcp_ics_cell_first_dot_pointwise. (exists fpmp_gap_dot_mcp_ics_cell_first_dot_pointwise. fpmp_gap_dot_mcp_ics_cell_first_dot_pointwise + S fpmp_index_dot_mcp_ics_cell_first_dot_pointwise = w) -> (((exists ff_h_fpmp_dot_mcp_ics_cell_first_dot_pointwise_left. ff_h_fpmp_dot_mcp_ics_cell_first_dot_pointwise_left + S (fpmp_left_dot_mcp_ics_cell_first_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_cell_first_dot_pointwise)) * ff_left_scale_mcp_cell_ics_cell_first)) /\ exists ff_q_fpmp_dot_mcp_ics_cell_first_dot_pointwise_left. ff_left_mcp_cell_ics_cell_first = ff_q_fpmp_dot_mcp_ics_cell_first_dot_pointwise_left * S ((S (fpmp_index_dot_mcp_ics_cell_first_dot_pointwise)) * ff_left_scale_mcp_cell_ics_cell_first) + (fpmp_left_dot_mcp_ics_cell_first_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_cell_first_dot_pointwise_right. ff_h_fpmp_dot_mcp_ics_cell_first_dot_pointwise_right + S (fpmp_right_dot_mcp_ics_cell_first_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_cell_first_dot_pointwise)) * ff_right_scale_mcp_cell_ics_cell_first)) /\ exists ff_q_fpmp_dot_mcp_ics_cell_first_dot_pointwise_right. ff_right_mcp_cell_ics_cell_first = ff_q_fpmp_dot_mcp_ics_cell_first_dot_pointwise_right * S ((S (fpmp_index_dot_mcp_ics_cell_first_dot_pointwise)) * ff_right_scale_mcp_cell_ics_cell_first) + (fpmp_right_dot_mcp_ics_cell_first_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_cell_first_dot_pointwise_target. ff_h_fpmp_dot_mcp_ics_cell_first_dot_pointwise_target + S (fpmp_target_dot_mcp_ics_cell_first_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_cell_first_dot_pointwise)) * ff_scale_dot_mcp_ics_cell_first_dot)) /\ exists ff_q_fpmp_dot_mcp_ics_cell_first_dot_pointwise_target. ff_code_dot_mcp_ics_cell_first_dot = ff_q_fpmp_dot_mcp_ics_cell_first_dot_pointwise_target * S ((S (fpmp_index_dot_mcp_ics_cell_first_dot_pointwise)) * ff_scale_dot_mcp_ics_cell_first_dot) + (fpmp_target_dot_mcp_ics_cell_first_dot_pointwise))) -> fpmp_target_dot_mcp_ics_cell_first_dot_pointwise = fpmp_left_dot_mcp_ics_cell_first_dot_pointwise * fpmp_right_dot_mcp_ics_cell_first_dot_pointwise) /\ (exists ff_u_dot_mcp_ics_cell_first_dot_sum ff_v_dot_mcp_ics_cell_first_dot_sum. ((((exists ff_h_dot_mcp_ics_cell_first_dot_sum_start. ff_h_dot_mcp_ics_cell_first_dot_sum_start + S (0) = S ((S (0)) * ff_v_dot_mcp_ics_cell_first_dot_sum)) /\ exists ff_q_dot_mcp_ics_cell_first_dot_sum_start. ff_u_dot_mcp_ics_cell_first_dot_sum = ff_q_dot_mcp_ics_cell_first_dot_sum_start * S ((S (0)) * ff_v_dot_mcp_ics_cell_first_dot_sum) + (0))) /\ ((((exists ff_h_dot_mcp_ics_cell_first_dot_sum_terminal. ff_h_dot_mcp_ics_cell_first_dot_sum_terminal + S (L) = S ((S (w)) * ff_v_dot_mcp_ics_cell_first_dot_sum)) /\ exists ff_q_dot_mcp_ics_cell_first_dot_sum_terminal. ff_u_dot_mcp_ics_cell_first_dot_sum = ff_q_dot_mcp_ics_cell_first_dot_sum_terminal * S ((S (w)) * ff_v_dot_mcp_ics_cell_first_dot_sum) + (L))) /\ forall ff_i_dot_mcp_ics_cell_first_dot_sum. (exists ff_lt_dot_mcp_ics_cell_first_dot_sum_bound. ff_lt_dot_mcp_ics_cell_first_dot_sum_bound + S ff_i_dot_mcp_ics_cell_first_dot_sum = w) -> exists ff_a_dot_mcp_ics_cell_first_dot_sum ff_r_dot_mcp_ics_cell_first_dot_sum ff_s_dot_mcp_ics_cell_first_dot_sum. ((((exists ff_h_dot_mcp_ics_cell_first_dot_sum_summand. ff_h_dot_mcp_ics_cell_first_dot_sum_summand + S (ff_a_dot_mcp_ics_cell_first_dot_sum) = S ((S (ff_i_dot_mcp_ics_cell_first_dot_sum)) * ff_scale_dot_mcp_ics_cell_first_dot)) /\ exists ff_q_dot_mcp_ics_cell_first_dot_sum_summand. ff_code_dot_mcp_ics_cell_first_dot = ff_q_dot_mcp_ics_cell_first_dot_sum_summand * S ((S (ff_i_dot_mcp_ics_cell_first_dot_sum)) * ff_scale_dot_mcp_ics_cell_first_dot) + (ff_a_dot_mcp_ics_cell_first_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_cell_first_dot_sum_partial. ff_h_dot_mcp_ics_cell_first_dot_sum_partial + S (ff_r_dot_mcp_ics_cell_first_dot_sum) = S ((S (ff_i_dot_mcp_ics_cell_first_dot_sum)) * ff_v_dot_mcp_ics_cell_first_dot_sum)) /\ exists ff_q_dot_mcp_ics_cell_first_dot_sum_partial. ff_u_dot_mcp_ics_cell_first_dot_sum = ff_q_dot_mcp_ics_cell_first_dot_sum_partial * S ((S (ff_i_dot_mcp_ics_cell_first_dot_sum)) * ff_v_dot_mcp_ics_cell_first_dot_sum) + (ff_r_dot_mcp_ics_cell_first_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_cell_first_dot_sum_successor. ff_h_dot_mcp_ics_cell_first_dot_sum_successor + S (ff_s_dot_mcp_ics_cell_first_dot_sum) = S ((S (S ff_i_dot_mcp_ics_cell_first_dot_sum)) * ff_v_dot_mcp_ics_cell_first_dot_sum)) /\ exists ff_q_dot_mcp_ics_cell_first_dot_sum_successor. ff_u_dot_mcp_ics_cell_first_dot_sum = ff_q_dot_mcp_ics_cell_first_dot_sum_successor * S ((S (S ff_i_dot_mcp_ics_cell_first_dot_sum)) * ff_v_dot_mcp_ics_cell_first_dot_sum) + (ff_s_dot_mcp_ics_cell_first_dot_sum))) /\ ff_s_dot_mcp_ics_cell_first_dot_sum = ff_r_dot_mcp_ics_cell_first_dot_sum + ff_a_dot_mcp_ics_cell_first_dot_sum))))))))))) -> (exists ff_left_mcp_cell_ics_cell_second ff_left_scale_mcp_cell_ics_cell_second ff_right_mcp_cell_ics_cell_second ff_right_scale_mcp_cell_ics_cell_second. ((forall ff_index_mcp_ics_cell_second_row ff_source_mcp_ics_cell_second_row ff_target_mcp_ics_cell_second_row. (exists mcp_gap_ics_cell_second_row_bound. mcp_gap_ics_cell_second_row_bound + S (ff_index_mcp_ics_cell_second_row) = (w)) -> (((exists fs_h_mcp_ics_cell_second_row_source. fs_h_mcp_ics_cell_second_row_source + S (ff_source_mcp_ics_cell_second_row) = S ((S (((row) * (w)) + (1) * ff_index_mcp_ics_cell_second_row)) * ac)) /\ exists fs_q_mcp_ics_cell_second_row_source. ab = fs_q_mcp_ics_cell_second_row_source * S ((S (((row) * (w)) + (1) * ff_index_mcp_ics_cell_second_row)) * ac) + (ff_source_mcp_ics_cell_second_row))) -> (((exists fs_h_mcp_ics_cell_second_row_target. fs_h_mcp_ics_cell_second_row_target + S (ff_target_mcp_ics_cell_second_row) = S ((S (ff_index_mcp_ics_cell_second_row)) * ff_left_scale_mcp_cell_ics_cell_second)) /\ exists fs_q_mcp_ics_cell_second_row_target. ff_left_mcp_cell_ics_cell_second = fs_q_mcp_ics_cell_second_row_target * S ((S (ff_index_mcp_ics_cell_second_row)) * ff_left_scale_mcp_cell_ics_cell_second) + (ff_target_mcp_ics_cell_second_row))) -> ff_target_mcp_ics_cell_second_row = ff_source_mcp_ics_cell_second_row) /\ ((forall ff_index_mcp_ics_cell_second_column ff_source_mcp_ics_cell_second_column ff_target_mcp_ics_cell_second_column. (exists mcp_gap_ics_cell_second_column_bound. mcp_gap_ics_cell_second_column_bound + S (ff_index_mcp_ics_cell_second_column) = (w)) -> (((exists fs_h_mcp_ics_cell_second_column_source. fs_h_mcp_ics_cell_second_column_source + S (ff_source_mcp_ics_cell_second_column) = S ((S ((0) + (1) * ff_index_mcp_ics_cell_second_column)) * cc)) /\ exists fs_q_mcp_ics_cell_second_column_source. cb = fs_q_mcp_ics_cell_second_column_source * S ((S ((0) + (1) * ff_index_mcp_ics_cell_second_column)) * cc) + (ff_source_mcp_ics_cell_second_column))) -> (((exists fs_h_mcp_ics_cell_second_column_target. fs_h_mcp_ics_cell_second_column_target + S (ff_target_mcp_ics_cell_second_column) = S ((S (ff_index_mcp_ics_cell_second_column)) * ff_right_scale_mcp_cell_ics_cell_second)) /\ exists fs_q_mcp_ics_cell_second_column_target. ff_right_mcp_cell_ics_cell_second = fs_q_mcp_ics_cell_second_column_target * S ((S (ff_index_mcp_ics_cell_second_column)) * ff_right_scale_mcp_cell_ics_cell_second) + (ff_target_mcp_ics_cell_second_column))) -> ff_target_mcp_ics_cell_second_column = ff_source_mcp_ics_cell_second_column) /\ (exists ff_code_dot_mcp_ics_cell_second_dot ff_scale_dot_mcp_ics_cell_second_dot. ((forall fpmp_index_dot_mcp_ics_cell_second_dot_pointwise fpmp_left_dot_mcp_ics_cell_second_dot_pointwise fpmp_right_dot_mcp_ics_cell_second_dot_pointwise fpmp_target_dot_mcp_ics_cell_second_dot_pointwise. (exists fpmp_gap_dot_mcp_ics_cell_second_dot_pointwise. fpmp_gap_dot_mcp_ics_cell_second_dot_pointwise + S fpmp_index_dot_mcp_ics_cell_second_dot_pointwise = w) -> (((exists ff_h_fpmp_dot_mcp_ics_cell_second_dot_pointwise_left. ff_h_fpmp_dot_mcp_ics_cell_second_dot_pointwise_left + S (fpmp_left_dot_mcp_ics_cell_second_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_cell_second_dot_pointwise)) * ff_left_scale_mcp_cell_ics_cell_second)) /\ exists ff_q_fpmp_dot_mcp_ics_cell_second_dot_pointwise_left. ff_left_mcp_cell_ics_cell_second = ff_q_fpmp_dot_mcp_ics_cell_second_dot_pointwise_left * S ((S (fpmp_index_dot_mcp_ics_cell_second_dot_pointwise)) * ff_left_scale_mcp_cell_ics_cell_second) + (fpmp_left_dot_mcp_ics_cell_second_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_cell_second_dot_pointwise_right. ff_h_fpmp_dot_mcp_ics_cell_second_dot_pointwise_right + S (fpmp_right_dot_mcp_ics_cell_second_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_cell_second_dot_pointwise)) * ff_right_scale_mcp_cell_ics_cell_second)) /\ exists ff_q_fpmp_dot_mcp_ics_cell_second_dot_pointwise_right. ff_right_mcp_cell_ics_cell_second = ff_q_fpmp_dot_mcp_ics_cell_second_dot_pointwise_right * S ((S (fpmp_index_dot_mcp_ics_cell_second_dot_pointwise)) * ff_right_scale_mcp_cell_ics_cell_second) + (fpmp_right_dot_mcp_ics_cell_second_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_cell_second_dot_pointwise_target. ff_h_fpmp_dot_mcp_ics_cell_second_dot_pointwise_target + S (fpmp_target_dot_mcp_ics_cell_second_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_cell_second_dot_pointwise)) * ff_scale_dot_mcp_ics_cell_second_dot)) /\ exists ff_q_fpmp_dot_mcp_ics_cell_second_dot_pointwise_target. ff_code_dot_mcp_ics_cell_second_dot = ff_q_fpmp_dot_mcp_ics_cell_second_dot_pointwise_target * S ((S (fpmp_index_dot_mcp_ics_cell_second_dot_pointwise)) * ff_scale_dot_mcp_ics_cell_second_dot) + (fpmp_target_dot_mcp_ics_cell_second_dot_pointwise))) -> fpmp_target_dot_mcp_ics_cell_second_dot_pointwise = fpmp_left_dot_mcp_ics_cell_second_dot_pointwise * fpmp_right_dot_mcp_ics_cell_second_dot_pointwise) /\ (exists ff_u_dot_mcp_ics_cell_second_dot_sum ff_v_dot_mcp_ics_cell_second_dot_sum. ((((exists ff_h_dot_mcp_ics_cell_second_dot_sum_start. ff_h_dot_mcp_ics_cell_second_dot_sum_start + S (0) = S ((S (0)) * ff_v_dot_mcp_ics_cell_second_dot_sum)) /\ exists ff_q_dot_mcp_ics_cell_second_dot_sum_start. ff_u_dot_mcp_ics_cell_second_dot_sum = ff_q_dot_mcp_ics_cell_second_dot_sum_start * S ((S (0)) * ff_v_dot_mcp_ics_cell_second_dot_sum) + (0))) /\ ((((exists ff_h_dot_mcp_ics_cell_second_dot_sum_terminal. ff_h_dot_mcp_ics_cell_second_dot_sum_terminal + S (M) = S ((S (w)) * ff_v_dot_mcp_ics_cell_second_dot_sum)) /\ exists ff_q_dot_mcp_ics_cell_second_dot_sum_terminal. ff_u_dot_mcp_ics_cell_second_dot_sum = ff_q_dot_mcp_ics_cell_second_dot_sum_terminal * S ((S (w)) * ff_v_dot_mcp_ics_cell_second_dot_sum) + (M))) /\ forall ff_i_dot_mcp_ics_cell_second_dot_sum. (exists ff_lt_dot_mcp_ics_cell_second_dot_sum_bound. ff_lt_dot_mcp_ics_cell_second_dot_sum_bound + S ff_i_dot_mcp_ics_cell_second_dot_sum = w) -> exists ff_a_dot_mcp_ics_cell_second_dot_sum ff_r_dot_mcp_ics_cell_second_dot_sum ff_s_dot_mcp_ics_cell_second_dot_sum. ((((exists ff_h_dot_mcp_ics_cell_second_dot_sum_summand. ff_h_dot_mcp_ics_cell_second_dot_sum_summand + S (ff_a_dot_mcp_ics_cell_second_dot_sum) = S ((S (ff_i_dot_mcp_ics_cell_second_dot_sum)) * ff_scale_dot_mcp_ics_cell_second_dot)) /\ exists ff_q_dot_mcp_ics_cell_second_dot_sum_summand. ff_code_dot_mcp_ics_cell_second_dot = ff_q_dot_mcp_ics_cell_second_dot_sum_summand * S ((S (ff_i_dot_mcp_ics_cell_second_dot_sum)) * ff_scale_dot_mcp_ics_cell_second_dot) + (ff_a_dot_mcp_ics_cell_second_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_cell_second_dot_sum_partial. ff_h_dot_mcp_ics_cell_second_dot_sum_partial + S (ff_r_dot_mcp_ics_cell_second_dot_sum) = S ((S (ff_i_dot_mcp_ics_cell_second_dot_sum)) * ff_v_dot_mcp_ics_cell_second_dot_sum)) /\ exists ff_q_dot_mcp_ics_cell_second_dot_sum_partial. ff_u_dot_mcp_ics_cell_second_dot_sum = ff_q_dot_mcp_ics_cell_second_dot_sum_partial * S ((S (ff_i_dot_mcp_ics_cell_second_dot_sum)) * ff_v_dot_mcp_ics_cell_second_dot_sum) + (ff_r_dot_mcp_ics_cell_second_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_cell_second_dot_sum_successor. ff_h_dot_mcp_ics_cell_second_dot_sum_successor + S (ff_s_dot_mcp_ics_cell_second_dot_sum) = S ((S (S ff_i_dot_mcp_ics_cell_second_dot_sum)) * ff_v_dot_mcp_ics_cell_second_dot_sum)) /\ exists ff_q_dot_mcp_ics_cell_second_dot_sum_successor. ff_u_dot_mcp_ics_cell_second_dot_sum = ff_q_dot_mcp_ics_cell_second_dot_sum_successor * S ((S (S ff_i_dot_mcp_ics_cell_second_dot_sum)) * ff_v_dot_mcp_ics_cell_second_dot_sum) + (ff_s_dot_mcp_ics_cell_second_dot_sum))) /\ ff_s_dot_mcp_ics_cell_second_dot_sum = ff_r_dot_mcp_ics_cell_second_dot_sum + ff_a_dot_mcp_ics_cell_second_dot_sum))))))))))) -> (exists ff_left_mcp_cell_ics_cell_third ff_left_scale_mcp_cell_ics_cell_third ff_right_mcp_cell_ics_cell_third ff_right_scale_mcp_cell_ics_cell_third. ((forall ff_index_mcp_ics_cell_third_row ff_source_mcp_ics_cell_third_row ff_target_mcp_ics_cell_third_row. (exists mcp_gap_ics_cell_third_row_bound. mcp_gap_ics_cell_third_row_bound + S (ff_index_mcp_ics_cell_third_row) = (w)) -> (((exists fs_h_mcp_ics_cell_third_row_source. fs_h_mcp_ics_cell_third_row_source + S (ff_source_mcp_ics_cell_third_row) = S ((S (((row) * (w)) + (1) * ff_index_mcp_ics_cell_third_row)) * ac)) /\ exists fs_q_mcp_ics_cell_third_row_source. ab = fs_q_mcp_ics_cell_third_row_source * S ((S (((row) * (w)) + (1) * ff_index_mcp_ics_cell_third_row)) * ac) + (ff_source_mcp_ics_cell_third_row))) -> (((exists fs_h_mcp_ics_cell_third_row_target. fs_h_mcp_ics_cell_third_row_target + S (ff_target_mcp_ics_cell_third_row) = S ((S (ff_index_mcp_ics_cell_third_row)) * ff_left_scale_mcp_cell_ics_cell_third)) /\ exists fs_q_mcp_ics_cell_third_row_target. ff_left_mcp_cell_ics_cell_third = fs_q_mcp_ics_cell_third_row_target * S ((S (ff_index_mcp_ics_cell_third_row)) * ff_left_scale_mcp_cell_ics_cell_third) + (ff_target_mcp_ics_cell_third_row))) -> ff_target_mcp_ics_cell_third_row = ff_source_mcp_ics_cell_third_row) /\ ((forall ff_index_mcp_ics_cell_third_column ff_source_mcp_ics_cell_third_column ff_target_mcp_ics_cell_third_column. (exists mcp_gap_ics_cell_third_column_bound. mcp_gap_ics_cell_third_column_bound + S (ff_index_mcp_ics_cell_third_column) = (w)) -> (((exists fs_h_mcp_ics_cell_third_column_source. fs_h_mcp_ics_cell_third_column_source + S (ff_source_mcp_ics_cell_third_column) = S ((S ((0) + (1) * ff_index_mcp_ics_cell_third_column)) * dc)) /\ exists fs_q_mcp_ics_cell_third_column_source. db = fs_q_mcp_ics_cell_third_column_source * S ((S ((0) + (1) * ff_index_mcp_ics_cell_third_column)) * dc) + (ff_source_mcp_ics_cell_third_column))) -> (((exists fs_h_mcp_ics_cell_third_column_target. fs_h_mcp_ics_cell_third_column_target + S (ff_target_mcp_ics_cell_third_column) = S ((S (ff_index_mcp_ics_cell_third_column)) * ff_right_scale_mcp_cell_ics_cell_third)) /\ exists fs_q_mcp_ics_cell_third_column_target. ff_right_mcp_cell_ics_cell_third = fs_q_mcp_ics_cell_third_column_target * S ((S (ff_index_mcp_ics_cell_third_column)) * ff_right_scale_mcp_cell_ics_cell_third) + (ff_target_mcp_ics_cell_third_column))) -> ff_target_mcp_ics_cell_third_column = ff_source_mcp_ics_cell_third_column) /\ (exists ff_code_dot_mcp_ics_cell_third_dot ff_scale_dot_mcp_ics_cell_third_dot. ((forall fpmp_index_dot_mcp_ics_cell_third_dot_pointwise fpmp_left_dot_mcp_ics_cell_third_dot_pointwise fpmp_right_dot_mcp_ics_cell_third_dot_pointwise fpmp_target_dot_mcp_ics_cell_third_dot_pointwise. (exists fpmp_gap_dot_mcp_ics_cell_third_dot_pointwise. fpmp_gap_dot_mcp_ics_cell_third_dot_pointwise + S fpmp_index_dot_mcp_ics_cell_third_dot_pointwise = w) -> (((exists ff_h_fpmp_dot_mcp_ics_cell_third_dot_pointwise_left. ff_h_fpmp_dot_mcp_ics_cell_third_dot_pointwise_left + S (fpmp_left_dot_mcp_ics_cell_third_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_cell_third_dot_pointwise)) * ff_left_scale_mcp_cell_ics_cell_third)) /\ exists ff_q_fpmp_dot_mcp_ics_cell_third_dot_pointwise_left. ff_left_mcp_cell_ics_cell_third = ff_q_fpmp_dot_mcp_ics_cell_third_dot_pointwise_left * S ((S (fpmp_index_dot_mcp_ics_cell_third_dot_pointwise)) * ff_left_scale_mcp_cell_ics_cell_third) + (fpmp_left_dot_mcp_ics_cell_third_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_cell_third_dot_pointwise_right. ff_h_fpmp_dot_mcp_ics_cell_third_dot_pointwise_right + S (fpmp_right_dot_mcp_ics_cell_third_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_cell_third_dot_pointwise)) * ff_right_scale_mcp_cell_ics_cell_third)) /\ exists ff_q_fpmp_dot_mcp_ics_cell_third_dot_pointwise_right. ff_right_mcp_cell_ics_cell_third = ff_q_fpmp_dot_mcp_ics_cell_third_dot_pointwise_right * S ((S (fpmp_index_dot_mcp_ics_cell_third_dot_pointwise)) * ff_right_scale_mcp_cell_ics_cell_third) + (fpmp_right_dot_mcp_ics_cell_third_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_cell_third_dot_pointwise_target. ff_h_fpmp_dot_mcp_ics_cell_third_dot_pointwise_target + S (fpmp_target_dot_mcp_ics_cell_third_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_cell_third_dot_pointwise)) * ff_scale_dot_mcp_ics_cell_third_dot)) /\ exists ff_q_fpmp_dot_mcp_ics_cell_third_dot_pointwise_target. ff_code_dot_mcp_ics_cell_third_dot = ff_q_fpmp_dot_mcp_ics_cell_third_dot_pointwise_target * S ((S (fpmp_index_dot_mcp_ics_cell_third_dot_pointwise)) * ff_scale_dot_mcp_ics_cell_third_dot) + (fpmp_target_dot_mcp_ics_cell_third_dot_pointwise))) -> fpmp_target_dot_mcp_ics_cell_third_dot_pointwise = fpmp_left_dot_mcp_ics_cell_third_dot_pointwise * fpmp_right_dot_mcp_ics_cell_third_dot_pointwise) /\ (exists ff_u_dot_mcp_ics_cell_third_dot_sum ff_v_dot_mcp_ics_cell_third_dot_sum. ((((exists ff_h_dot_mcp_ics_cell_third_dot_sum_start. ff_h_dot_mcp_ics_cell_third_dot_sum_start + S (0) = S ((S (0)) * ff_v_dot_mcp_ics_cell_third_dot_sum)) /\ exists ff_q_dot_mcp_ics_cell_third_dot_sum_start. ff_u_dot_mcp_ics_cell_third_dot_sum = ff_q_dot_mcp_ics_cell_third_dot_sum_start * S ((S (0)) * ff_v_dot_mcp_ics_cell_third_dot_sum) + (0))) /\ ((((exists ff_h_dot_mcp_ics_cell_third_dot_sum_terminal. ff_h_dot_mcp_ics_cell_third_dot_sum_terminal + S (N) = S ((S (w)) * ff_v_dot_mcp_ics_cell_third_dot_sum)) /\ exists ff_q_dot_mcp_ics_cell_third_dot_sum_terminal. ff_u_dot_mcp_ics_cell_third_dot_sum = ff_q_dot_mcp_ics_cell_third_dot_sum_terminal * S ((S (w)) * ff_v_dot_mcp_ics_cell_third_dot_sum) + (N))) /\ forall ff_i_dot_mcp_ics_cell_third_dot_sum. (exists ff_lt_dot_mcp_ics_cell_third_dot_sum_bound. ff_lt_dot_mcp_ics_cell_third_dot_sum_bound + S ff_i_dot_mcp_ics_cell_third_dot_sum = w) -> exists ff_a_dot_mcp_ics_cell_third_dot_sum ff_r_dot_mcp_ics_cell_third_dot_sum ff_s_dot_mcp_ics_cell_third_dot_sum. ((((exists ff_h_dot_mcp_ics_cell_third_dot_sum_summand. ff_h_dot_mcp_ics_cell_third_dot_sum_summand + S (ff_a_dot_mcp_ics_cell_third_dot_sum) = S ((S (ff_i_dot_mcp_ics_cell_third_dot_sum)) * ff_scale_dot_mcp_ics_cell_third_dot)) /\ exists ff_q_dot_mcp_ics_cell_third_dot_sum_summand. ff_code_dot_mcp_ics_cell_third_dot = ff_q_dot_mcp_ics_cell_third_dot_sum_summand * S ((S (ff_i_dot_mcp_ics_cell_third_dot_sum)) * ff_scale_dot_mcp_ics_cell_third_dot) + (ff_a_dot_mcp_ics_cell_third_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_cell_third_dot_sum_partial. ff_h_dot_mcp_ics_cell_third_dot_sum_partial + S (ff_r_dot_mcp_ics_cell_third_dot_sum) = S ((S (ff_i_dot_mcp_ics_cell_third_dot_sum)) * ff_v_dot_mcp_ics_cell_third_dot_sum)) /\ exists ff_q_dot_mcp_ics_cell_third_dot_sum_partial. ff_u_dot_mcp_ics_cell_third_dot_sum = ff_q_dot_mcp_ics_cell_third_dot_sum_partial * S ((S (ff_i_dot_mcp_ics_cell_third_dot_sum)) * ff_v_dot_mcp_ics_cell_third_dot_sum) + (ff_r_dot_mcp_ics_cell_third_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_cell_third_dot_sum_successor. ff_h_dot_mcp_ics_cell_third_dot_sum_successor + S (ff_s_dot_mcp_ics_cell_third_dot_sum) = S ((S (S ff_i_dot_mcp_ics_cell_third_dot_sum)) * ff_v_dot_mcp_ics_cell_third_dot_sum)) /\ exists ff_q_dot_mcp_ics_cell_third_dot_sum_successor. ff_u_dot_mcp_ics_cell_third_dot_sum = ff_q_dot_mcp_ics_cell_third_dot_sum_successor * S ((S (S ff_i_dot_mcp_ics_cell_third_dot_sum)) * ff_v_dot_mcp_ics_cell_third_dot_sum) + (ff_s_dot_mcp_ics_cell_third_dot_sum))) /\ ff_s_dot_mcp_ics_cell_third_dot_sum = ff_r_dot_mcp_ics_cell_third_dot_sum + ff_a_dot_mcp_ics_cell_third_dot_sum))))))))))) -> L + M = N

Complete tactic proof in conservative notation

All 167 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.

Read the argument

Proof checkpoints

167 script commands · 26 reading checkpoints · 12 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.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

Named ingredients (1)
integer span dot product pointwise add
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 w
  10. L10
    intro row
02Fix variables and assumptionsL11–17

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

  1. L11
    intro L
  2. L12
    intro M
  3. L13
    intro N
  4. L14
    intro hadd
  5. L15
    intro hfirst
  6. L16
    intro hsecond
  7. L17
    intro hthird
03Separate the logical casesL18–27

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

  1. L18
    cases hfirst
  2. L19
    cases hfirst_witness
  3. L20
    cases hfirst_witness_witness
  4. L21
    cases hfirst_witness_witness_witness
  5. L22
    cases hfirst_witness_witness_witness_witness
  6. L23
    cases hfirst_witness_witness_witness_witness_right
  7. L24
    cases hsecond
  8. L25
    cases hsecond_witness
  9. L26
    cases hsecond_witness_witness
  10. L27
    cases hsecond_witness_witness_witness
04Separate the logical casesL28–35

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

  1. L28
    cases hsecond_witness_witness_witness_witness
  2. L29
    cases hsecond_witness_witness_witness_witness_right
  3. L30
    cases hthird
  4. L31
    cases hthird_witness
  5. L32
    cases hthird_witness_witness
  6. L33
    cases hthird_witness_witness_witness
  7. L34
    cases hthird_witness_witness_witness_witness
  8. L35
    cases hthird_witness_witness_witness_witness_right
05Use earlier factsL36–45

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

  1. L36
    specialize integer_span_dot_product_pointwise_add (x)
  2. L37
    specialize integer_span_dot_product_pointwise_add (x1)
  3. L38
    specialize integer_span_dot_product_pointwise_add (x2)
  4. L39
    specialize integer_span_dot_product_pointwise_add (x3)
  5. L40
    specialize integer_span_dot_product_pointwise_add (x4)
  6. L41
    specialize integer_span_dot_product_pointwise_add (x5)
  7. L42
    specialize integer_span_dot_product_pointwise_add (x6)
  8. L43
    specialize integer_span_dot_product_pointwise_add (x7)
  9. L44
    specialize integer_span_dot_product_pointwise_add (x8)
  10. L45
    specialize integer_span_dot_product_pointwise_add (x9)
06Use earlier factsL46–55

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

  1. L46
    specialize integer_span_dot_product_pointwise_add (x10)
  2. L47
    specialize integer_span_dot_product_pointwise_add (x11)
  3. L48
    specialize integer_span_dot_product_pointwise_add (w)
  4. L49
    specialize integer_span_dot_product_pointwise_add (L)
  5. L50
    specialize integer_span_dot_product_pointwise_add (M)
  6. L51
    specialize integer_span_dot_product_pointwise_add (N)
  7. L52
    apply integer_span_dot_product_pointwise_add
  8. L53
    exact hfirst_witness_witness_witness_witness_right_right
  9. L54
    exact hsecond_witness_witness_witness_witness_right_right
  10. L55
    exact hthird_witness_witness_witness_witness_right_right
07Fix variables and assumptionsL56–65

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

  1. L56
    intro i
  2. L57
    intro a
  3. L58
    intro b
  4. L59
    intro c
  5. L60
    intro d
  6. L61
    intro e
  7. L62
    intro f
  8. L63
    intro hi
  9. L64
    intro ha
  10. L65
    intro hb
08Fix variables and assumptionsL66–69

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

  1. L66
    intro hc
  2. L67
    intro hd
  3. L68
    intro he
  4. L69
    intro hf
09Establish hmatrixL70–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 hmatrix : ∃ value. BetaAt(ab,ac,row · w + 1 · i,value)Definitions: BetaAt(ab,ac,row · w + 1 · i,value)Original native command in the exact edition
  2. L71
    specialize beta_at_exists (ab)
  3. L72
    specialize beta_at_exists (ac)
  4. L73
    specialize beta_at_exists (row * w + 1 * i)
  5. L74
    apply beta_at_exists
10Separate the logical casesL75–75

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

  1. L75
    cases hmatrix
11Establish hleftL76–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 hleft : ∃ value. BetaAt(bb,bc,i,value)Definitions: BetaAt(bb,bc,i,value)Original native command in the exact edition
  2. L77
    specialize beta_at_exists (bb)
  3. L78
    specialize beta_at_exists (bc)
  4. L79
    specialize beta_at_exists (i)
  5. L80
    apply beta_at_exists
12Separate the logical casesL81–81

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

  1. L81
    cases hleft
13Establish hrightL82–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 hright : ∃ value. BetaAt(cb,cc,i,value)Definitions: BetaAt(cb,cc,i,value)Original native command in the exact edition
  2. L83
    specialize beta_at_exists (cb)
  3. L84
    specialize beta_at_exists (cc)
  4. L85
    specialize beta_at_exists (i)
  5. L86
    apply beta_at_exists
14Separate the logical casesL87–87

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

  1. L87
    cases hright
15Establish htotalL88–92

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

  1. L88
    have htotal : ∃ value. BetaAt(db,dc,i,value)Definitions: BetaAt(db,dc,i,value)Original native command in the exact edition
  2. L89
    specialize beta_at_exists (db)
  3. L90
    specialize beta_at_exists (dc)
  4. L91
    specialize beta_at_exists (i)
  5. L92
    apply beta_at_exists
16Separate the logical casesL93–93

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

  1. L93
    cases htotal
17Establish haeqL94–101

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

  1. L94
    have haeq : a = x12
  2. L95
    specialize hfirst_witness_witness_witness_witness_left (i)
  3. L96
    specialize hfirst_witness_witness_witness_witness_left (x12)
  4. L97
    specialize hfirst_witness_witness_witness_witness_left (a)
  5. L98
    apply hfirst_witness_witness_witness_witness_left
  6. L99
    exact hi
  7. L100
    exact hmatrix_witness
  8. L101
    exact ha
18Establish hceqL102–109

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

  1. L102
    have hceq : c = x12
  2. L103
    specialize hsecond_witness_witness_witness_witness_left (i)
  3. L104
    specialize hsecond_witness_witness_witness_witness_left (x12)
  4. L105
    specialize hsecond_witness_witness_witness_witness_left (c)
  5. L106
    apply hsecond_witness_witness_witness_witness_left
  6. L107
    exact hi
  7. L108
    exact hmatrix_witness
  8. L109
    exact hc
19Establish heeqL110–117

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

  1. L110
    have heeq : e = x12
  2. L111
    specialize hthird_witness_witness_witness_witness_left (i)
  3. L112
    specialize hthird_witness_witness_witness_witness_left (x12)
  4. L113
    specialize hthird_witness_witness_witness_witness_left (e)
  5. L114
    apply hthird_witness_witness_witness_witness_left
  6. L115
    exact hi
  7. L116
    exact hmatrix_witness
  8. L117
    exact he
20Establish hindexL118–119

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

  1. L118
    have hindex : 0 + 1 * i = i
  2. L119
    simp [one_mul, zero_add]
21Establish hbeqL120–129

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

  1. L120
    have hbeq : b = x13
  2. L121
    specialize hfirst_witness_witness_witness_witness_right_left (i)
  3. L122
    specialize hfirst_witness_witness_witness_witness_right_left (x13)
  4. L123
    specialize hfirst_witness_witness_witness_witness_right_left (b)
  5. L124
    apply hfirst_witness_witness_witness_witness_right_left
  6. L125
    exact hi
  7. L126
    rewrite hindex
  8. L127
    rewrite hindex
  9. L128
    exact hleft_witness
  10. L129
    exact hb
22Establish hdeqL130–139

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

  1. L130
    have hdeq : d = x14
  2. L131
    specialize hsecond_witness_witness_witness_witness_right_left (i)
  3. L132
    specialize hsecond_witness_witness_witness_witness_right_left (x14)
  4. L133
    specialize hsecond_witness_witness_witness_witness_right_left (d)
  5. L134
    apply hsecond_witness_witness_witness_witness_right_left
  6. L135
    exact hi
  7. L136
    rewrite hindex
  8. L137
    rewrite hindex
  9. L138
    exact hright_witness
  10. L139
    exact hd
23Establish hfeqL140–149

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hthird witness witness witness witness right left.

  1. L140
    have hfeq : f = x15
  2. L141
    specialize hthird_witness_witness_witness_witness_right_left (i)
  3. L142
    specialize hthird_witness_witness_witness_witness_right_left (x15)
  4. L143
    specialize hthird_witness_witness_witness_witness_right_left (f)
  5. L144
    apply hthird_witness_witness_witness_witness_right_left
  6. L145
    exact hi
  7. L146
    rewrite hindex
  8. L147
    rewrite hindex
  9. L148
    exact htotal_witness
  10. L149
    exact hf
24Establish hcoeffL150–159

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

  1. L150
    have hcoeff : x15 = x13 + x14
  2. L151
    specialize hadd (i)
  3. L152
    specialize hadd (x13)
  4. L153
    specialize hadd (x14)
  5. L154
    specialize hadd (x15)
  6. L155
    apply hadd
  7. L156
    exact hi
  8. L157
    exact hleft_witness
  9. L158
    exact hright_witness
  10. L159
    exact htotal_witness
25Calculate and transport equalitiesL160–166

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

  1. L160
    rewrite haeq
  2. L161
    rewrite hbeq
  3. L162
    rewrite hceq
  4. L163
    rewrite hdeq
  5. L164
    rewrite heeq
  6. L165
    rewrite hfeq
  7. L166
    rewrite hcoeff
26Use earlier factsL167–167

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

  1. L167
    apply mul_add

Library-wide reading audit

Original defined command ledger · 167 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 w
  10. 0010intro row
  11. 0011intro L
  12. 0012intro M
  13. 0013intro N
  14. 0014intro hadd
  15. 0015intro hfirst
  16. 0016intro hsecond
  17. 0017intro hthird
  18. 0018cases hfirst
  19. 0019cases hfirst_witness
  20. 0020cases hfirst_witness_witness
  21. 0021cases hfirst_witness_witness_witness
  22. 0022cases hfirst_witness_witness_witness_witness
  23. 0023cases hfirst_witness_witness_witness_witness_right
  24. 0024cases hsecond
  25. 0025cases hsecond_witness
  26. 0026cases hsecond_witness_witness
  27. 0027cases hsecond_witness_witness_witness
  28. 0028cases hsecond_witness_witness_witness_witness
  29. 0029cases hsecond_witness_witness_witness_witness_right
  30. 0030cases hthird
  31. 0031cases hthird_witness
  32. 0032cases hthird_witness_witness
  33. 0033cases hthird_witness_witness_witness
  34. 0034cases hthird_witness_witness_witness_witness
  35. 0035cases hthird_witness_witness_witness_witness_right
  36. 0036specialize integer_span_dot_product_pointwise_add (x)
  37. 0037specialize integer_span_dot_product_pointwise_add (x1)
  38. 0038specialize integer_span_dot_product_pointwise_add (x2)
  39. 0039specialize integer_span_dot_product_pointwise_add (x3)
  40. 0040specialize integer_span_dot_product_pointwise_add (x4)
  41. 0041specialize integer_span_dot_product_pointwise_add (x5)
  42. 0042specialize integer_span_dot_product_pointwise_add (x6)
  43. 0043specialize integer_span_dot_product_pointwise_add (x7)
  44. 0044specialize integer_span_dot_product_pointwise_add (x8)
  45. 0045specialize integer_span_dot_product_pointwise_add (x9)
  46. 0046specialize integer_span_dot_product_pointwise_add (x10)
  47. 0047specialize integer_span_dot_product_pointwise_add (x11)
  48. 0048specialize integer_span_dot_product_pointwise_add (w)
  49. 0049specialize integer_span_dot_product_pointwise_add (L)
  50. 0050specialize integer_span_dot_product_pointwise_add (M)
  51. 0051specialize integer_span_dot_product_pointwise_add (N)
  52. 0052apply integer_span_dot_product_pointwise_add
  53. 0053exact hfirst_witness_witness_witness_witness_right_right
  54. 0054exact hsecond_witness_witness_witness_witness_right_right
  55. 0055exact hthird_witness_witness_witness_witness_right_right
  56. 0056intro i
  57. 0057intro a
  58. 0058intro b
  59. 0059intro c
  60. 0060intro d
  61. 0061intro e
  62. 0062intro f
  63. 0063intro hi
  64. 0064intro ha
  65. 0065intro hb
  66. 0066intro hc
  67. 0067intro hd
  68. 0068intro he
  69. 0069intro hf
  70. 0070have hmatrix : ∃ value. BetaAt(ab,ac,row · w + 1 · i,value)
  71. 0071specialize beta_at_exists (ab)
  72. 0072specialize beta_at_exists (ac)
  73. 0073specialize beta_at_exists (row * w + 1 * i)
  74. 0074apply beta_at_exists
  75. 0075cases hmatrix
  76. 0076have hleft : ∃ value. BetaAt(bb,bc,i,value)
  77. 0077specialize beta_at_exists (bb)
  78. 0078specialize beta_at_exists (bc)
  79. 0079specialize beta_at_exists (i)
  80. 0080apply beta_at_exists
  81. 0081cases hleft
  82. 0082have hright : ∃ value. BetaAt(cb,cc,i,value)
  83. 0083specialize beta_at_exists (cb)
  84. 0084specialize beta_at_exists (cc)
  85. 0085specialize beta_at_exists (i)
  86. 0086apply beta_at_exists
  87. 0087cases hright
  88. 0088have htotal : ∃ value. BetaAt(db,dc,i,value)
  89. 0089specialize beta_at_exists (db)
  90. 0090specialize beta_at_exists (dc)
  91. 0091specialize beta_at_exists (i)
  92. 0092apply beta_at_exists
  93. 0093cases htotal
  94. 0094have haeq : a = x12
  95. 0095specialize hfirst_witness_witness_witness_witness_left (i)
  96. 0096specialize hfirst_witness_witness_witness_witness_left (x12)
  97. 0097specialize hfirst_witness_witness_witness_witness_left (a)
  98. 0098apply hfirst_witness_witness_witness_witness_left
  99. 0099exact hi
  100. 0100exact hmatrix_witness
  101. 0101exact ha
  102. 0102have hceq : c = x12
  103. 0103specialize hsecond_witness_witness_witness_witness_left (i)
  104. 0104specialize hsecond_witness_witness_witness_witness_left (x12)
  105. 0105specialize hsecond_witness_witness_witness_witness_left (c)
  106. 0106apply hsecond_witness_witness_witness_witness_left
  107. 0107exact hi
  108. 0108exact hmatrix_witness
  109. 0109exact hc
  110. 0110have heeq : e = x12
  111. 0111specialize hthird_witness_witness_witness_witness_left (i)
  112. 0112specialize hthird_witness_witness_witness_witness_left (x12)
  113. 0113specialize hthird_witness_witness_witness_witness_left (e)
  114. 0114apply hthird_witness_witness_witness_witness_left
  115. 0115exact hi
  116. 0116exact hmatrix_witness
  117. 0117exact he
  118. 0118have hindex : 0 + 1 * i = i
  119. 0119simp [one_mul, zero_add]
  120. 0120have hbeq : b = x13
  121. 0121specialize hfirst_witness_witness_witness_witness_right_left (i)
  122. 0122specialize hfirst_witness_witness_witness_witness_right_left (x13)
  123. 0123specialize hfirst_witness_witness_witness_witness_right_left (b)
  124. 0124apply hfirst_witness_witness_witness_witness_right_left
  125. 0125exact hi
  126. 0126rewrite hindex
  127. 0127rewrite hindex
  128. 0128exact hleft_witness
  129. 0129exact hb
  130. 0130have hdeq : d = x14
  131. 0131specialize hsecond_witness_witness_witness_witness_right_left (i)
  132. 0132specialize hsecond_witness_witness_witness_witness_right_left (x14)
  133. 0133specialize hsecond_witness_witness_witness_witness_right_left (d)
  134. 0134apply hsecond_witness_witness_witness_witness_right_left
  135. 0135exact hi
  136. 0136rewrite hindex
  137. 0137rewrite hindex
  138. 0138exact hright_witness
  139. 0139exact hd
  140. 0140have hfeq : f = x15
  141. 0141specialize hthird_witness_witness_witness_witness_right_left (i)
  142. 0142specialize hthird_witness_witness_witness_witness_right_left (x15)
  143. 0143specialize hthird_witness_witness_witness_witness_right_left (f)
  144. 0144apply hthird_witness_witness_witness_witness_right_left
  145. 0145exact hi
  146. 0146rewrite hindex
  147. 0147rewrite hindex
  148. 0148exact htotal_witness
  149. 0149exact hf
  150. 0150have hcoeff : x15 = x13 + x14
  151. 0151specialize hadd (i)
  152. 0152specialize hadd (x13)
  153. 0153specialize hadd (x14)
  154. 0154specialize hadd (x15)
  155. 0155apply hadd
  156. 0156exact hi
  157. 0157exact hleft_witness
  158. 0158exact hright_witness
  159. 0159exact htotal_witness
  160. 0160rewrite haeq
  161. 0161rewrite hbeq
  162. 0162rewrite hceq
  163. 0163rewrite hdeq
  164. 0164rewrite heeq
  165. 0165rewrite hfeq
  166. 0166rewrite hcoeff
  167. 0167apply mul_add