DL0066

integer_span_natural_product_entry

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

Every actual entry of a one-column coded matrix product is the genuine cell at that same row, by bounded column-zero and beta uniqueness, not an arbitrary output witness.

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 w pb pc l i z. (forall ff_index_mcp_prefix_ics_entry_product. (exists mcp_gap_ics_entry_product_index. mcp_gap_ics_entry_product_index + S (ff_index_mcp_prefix_ics_entry_product) = (l)) -> exists ff_row_mcp_prefix_ics_entry_product ff_column_mcp_prefix_ics_entry_product ff_value_mcp_prefix_ics_entry_product. ((ff_index_mcp_prefix_ics_entry_product) = (1) * ff_row_mcp_prefix_ics_entry_product + ff_column_mcp_prefix_ics_entry_product /\ ((exists mcp_gap_ics_entry_product_column. mcp_gap_ics_entry_product_column + S (ff_column_mcp_prefix_ics_entry_product) = (1)) /\ ((exists ff_left_mcp_cell_ics_entry_product_cell ff_left_scale_mcp_cell_ics_entry_product_cell ff_right_mcp_cell_ics_entry_product_cell ff_right_scale_mcp_cell_ics_entry_product_cell. ((forall ff_index_mcp_ics_entry_product_cell_row ff_source_mcp_ics_entry_product_cell_row ff_target_mcp_ics_entry_product_cell_row. (exists mcp_gap_ics_entry_product_cell_row_bound. mcp_gap_ics_entry_product_cell_row_bound + S (ff_index_mcp_ics_entry_product_cell_row) = (w)) -> (((exists fs_h_mcp_ics_entry_product_cell_row_source. fs_h_mcp_ics_entry_product_cell_row_source + S (ff_source_mcp_ics_entry_product_cell_row) = S ((S (((ff_row_mcp_prefix_ics_entry_product) * (w)) + (1) * ff_index_mcp_ics_entry_product_cell_row)) * ac)) /\ exists fs_q_mcp_ics_entry_product_cell_row_source. ab = fs_q_mcp_ics_entry_product_cell_row_source * S ((S (((ff_row_mcp_prefix_ics_entry_product) * (w)) + (1) * ff_index_mcp_ics_entry_product_cell_row)) * ac) + (ff_source_mcp_ics_entry_product_cell_row))) -> (((exists fs_h_mcp_ics_entry_product_cell_row_target. fs_h_mcp_ics_entry_product_cell_row_target + S (ff_target_mcp_ics_entry_product_cell_row) = S ((S (ff_index_mcp_ics_entry_product_cell_row)) * ff_left_scale_mcp_cell_ics_entry_product_cell)) /\ exists fs_q_mcp_ics_entry_product_cell_row_target. ff_left_mcp_cell_ics_entry_product_cell = fs_q_mcp_ics_entry_product_cell_row_target * S ((S (ff_index_mcp_ics_entry_product_cell_row)) * ff_left_scale_mcp_cell_ics_entry_product_cell) + (ff_target_mcp_ics_entry_product_cell_row))) -> ff_target_mcp_ics_entry_product_cell_row = ff_source_mcp_ics_entry_product_cell_row) /\ ((forall ff_index_mcp_ics_entry_product_cell_column ff_source_mcp_ics_entry_product_cell_column ff_target_mcp_ics_entry_product_cell_column. (exists mcp_gap_ics_entry_product_cell_column_bound. mcp_gap_ics_entry_product_cell_column_bound + S (ff_index_mcp_ics_entry_product_cell_column) = (w)) -> (((exists fs_h_mcp_ics_entry_product_cell_column_source. fs_h_mcp_ics_entry_product_cell_column_source + S (ff_source_mcp_ics_entry_product_cell_column) = S ((S ((ff_column_mcp_prefix_ics_entry_product) + (1) * ff_index_mcp_ics_entry_product_cell_column)) * bc)) /\ exists fs_q_mcp_ics_entry_product_cell_column_source. bb = fs_q_mcp_ics_entry_product_cell_column_source * S ((S ((ff_column_mcp_prefix_ics_entry_product) + (1) * ff_index_mcp_ics_entry_product_cell_column)) * bc) + (ff_source_mcp_ics_entry_product_cell_column))) -> (((exists fs_h_mcp_ics_entry_product_cell_column_target. fs_h_mcp_ics_entry_product_cell_column_target + S (ff_target_mcp_ics_entry_product_cell_column) = S ((S (ff_index_mcp_ics_entry_product_cell_column)) * ff_right_scale_mcp_cell_ics_entry_product_cell)) /\ exists fs_q_mcp_ics_entry_product_cell_column_target. ff_right_mcp_cell_ics_entry_product_cell = fs_q_mcp_ics_entry_product_cell_column_target * S ((S (ff_index_mcp_ics_entry_product_cell_column)) * ff_right_scale_mcp_cell_ics_entry_product_cell) + (ff_target_mcp_ics_entry_product_cell_column))) -> ff_target_mcp_ics_entry_product_cell_column = ff_source_mcp_ics_entry_product_cell_column) /\ (exists ff_code_dot_mcp_ics_entry_product_cell_dot ff_scale_dot_mcp_ics_entry_product_cell_dot. ((forall fpmp_index_dot_mcp_ics_entry_product_cell_dot_pointwise fpmp_left_dot_mcp_ics_entry_product_cell_dot_pointwise fpmp_right_dot_mcp_ics_entry_product_cell_dot_pointwise fpmp_target_dot_mcp_ics_entry_product_cell_dot_pointwise. (exists fpmp_gap_dot_mcp_ics_entry_product_cell_dot_pointwise. fpmp_gap_dot_mcp_ics_entry_product_cell_dot_pointwise + S fpmp_index_dot_mcp_ics_entry_product_cell_dot_pointwise = w) -> (((exists ff_h_fpmp_dot_mcp_ics_entry_product_cell_dot_pointwise_left. ff_h_fpmp_dot_mcp_ics_entry_product_cell_dot_pointwise_left + S (fpmp_left_dot_mcp_ics_entry_product_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_entry_product_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_entry_product_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_entry_product_cell_dot_pointwise_left. ff_left_mcp_cell_ics_entry_product_cell = ff_q_fpmp_dot_mcp_ics_entry_product_cell_dot_pointwise_left * S ((S (fpmp_index_dot_mcp_ics_entry_product_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_entry_product_cell) + (fpmp_left_dot_mcp_ics_entry_product_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_entry_product_cell_dot_pointwise_right. ff_h_fpmp_dot_mcp_ics_entry_product_cell_dot_pointwise_right + S (fpmp_right_dot_mcp_ics_entry_product_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_entry_product_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_entry_product_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_entry_product_cell_dot_pointwise_right. ff_right_mcp_cell_ics_entry_product_cell = ff_q_fpmp_dot_mcp_ics_entry_product_cell_dot_pointwise_right * S ((S (fpmp_index_dot_mcp_ics_entry_product_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_entry_product_cell) + (fpmp_right_dot_mcp_ics_entry_product_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_entry_product_cell_dot_pointwise_target. ff_h_fpmp_dot_mcp_ics_entry_product_cell_dot_pointwise_target + S (fpmp_target_dot_mcp_ics_entry_product_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_entry_product_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_entry_product_cell_dot)) /\ exists ff_q_fpmp_dot_mcp_ics_entry_product_cell_dot_pointwise_target. ff_code_dot_mcp_ics_entry_product_cell_dot = ff_q_fpmp_dot_mcp_ics_entry_product_cell_dot_pointwise_target * S ((S (fpmp_index_dot_mcp_ics_entry_product_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_entry_product_cell_dot) + (fpmp_target_dot_mcp_ics_entry_product_cell_dot_pointwise))) -> fpmp_target_dot_mcp_ics_entry_product_cell_dot_pointwise = fpmp_left_dot_mcp_ics_entry_product_cell_dot_pointwise * fpmp_right_dot_mcp_ics_entry_product_cell_dot_pointwise) /\ (exists ff_u_dot_mcp_ics_entry_product_cell_dot_sum ff_v_dot_mcp_ics_entry_product_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_entry_product_cell_dot_sum_start. ff_h_dot_mcp_ics_entry_product_cell_dot_sum_start + S (0) = S ((S (0)) * ff_v_dot_mcp_ics_entry_product_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_entry_product_cell_dot_sum_start. ff_u_dot_mcp_ics_entry_product_cell_dot_sum = ff_q_dot_mcp_ics_entry_product_cell_dot_sum_start * S ((S (0)) * ff_v_dot_mcp_ics_entry_product_cell_dot_sum) + (0))) /\ ((((exists ff_h_dot_mcp_ics_entry_product_cell_dot_sum_terminal. ff_h_dot_mcp_ics_entry_product_cell_dot_sum_terminal + S (ff_value_mcp_prefix_ics_entry_product) = S ((S (w)) * ff_v_dot_mcp_ics_entry_product_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_entry_product_cell_dot_sum_terminal. ff_u_dot_mcp_ics_entry_product_cell_dot_sum = ff_q_dot_mcp_ics_entry_product_cell_dot_sum_terminal * S ((S (w)) * ff_v_dot_mcp_ics_entry_product_cell_dot_sum) + (ff_value_mcp_prefix_ics_entry_product))) /\ forall ff_i_dot_mcp_ics_entry_product_cell_dot_sum. (exists ff_lt_dot_mcp_ics_entry_product_cell_dot_sum_bound. ff_lt_dot_mcp_ics_entry_product_cell_dot_sum_bound + S ff_i_dot_mcp_ics_entry_product_cell_dot_sum = w) -> exists ff_a_dot_mcp_ics_entry_product_cell_dot_sum ff_r_dot_mcp_ics_entry_product_cell_dot_sum ff_s_dot_mcp_ics_entry_product_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_entry_product_cell_dot_sum_summand. ff_h_dot_mcp_ics_entry_product_cell_dot_sum_summand + S (ff_a_dot_mcp_ics_entry_product_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_entry_product_cell_dot_sum)) * ff_scale_dot_mcp_ics_entry_product_cell_dot)) /\ exists ff_q_dot_mcp_ics_entry_product_cell_dot_sum_summand. ff_code_dot_mcp_ics_entry_product_cell_dot = ff_q_dot_mcp_ics_entry_product_cell_dot_sum_summand * S ((S (ff_i_dot_mcp_ics_entry_product_cell_dot_sum)) * ff_scale_dot_mcp_ics_entry_product_cell_dot) + (ff_a_dot_mcp_ics_entry_product_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_entry_product_cell_dot_sum_partial. ff_h_dot_mcp_ics_entry_product_cell_dot_sum_partial + S (ff_r_dot_mcp_ics_entry_product_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_entry_product_cell_dot_sum)) * ff_v_dot_mcp_ics_entry_product_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_entry_product_cell_dot_sum_partial. ff_u_dot_mcp_ics_entry_product_cell_dot_sum = ff_q_dot_mcp_ics_entry_product_cell_dot_sum_partial * S ((S (ff_i_dot_mcp_ics_entry_product_cell_dot_sum)) * ff_v_dot_mcp_ics_entry_product_cell_dot_sum) + (ff_r_dot_mcp_ics_entry_product_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_entry_product_cell_dot_sum_successor. ff_h_dot_mcp_ics_entry_product_cell_dot_sum_successor + S (ff_s_dot_mcp_ics_entry_product_cell_dot_sum) = S ((S (S ff_i_dot_mcp_ics_entry_product_cell_dot_sum)) * ff_v_dot_mcp_ics_entry_product_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_entry_product_cell_dot_sum_successor. ff_u_dot_mcp_ics_entry_product_cell_dot_sum = ff_q_dot_mcp_ics_entry_product_cell_dot_sum_successor * S ((S (S ff_i_dot_mcp_ics_entry_product_cell_dot_sum)) * ff_v_dot_mcp_ics_entry_product_cell_dot_sum) + (ff_s_dot_mcp_ics_entry_product_cell_dot_sum))) /\ ff_s_dot_mcp_ics_entry_product_cell_dot_sum = ff_r_dot_mcp_ics_entry_product_cell_dot_sum + ff_a_dot_mcp_ics_entry_product_cell_dot_sum))))))))))) /\ (((exists fs_h_mcp_ics_entry_product_entry. fs_h_mcp_ics_entry_product_entry + S (ff_value_mcp_prefix_ics_entry_product) = S ((S (ff_index_mcp_prefix_ics_entry_product)) * pc)) /\ exists fs_q_mcp_ics_entry_product_entry. pb = fs_q_mcp_ics_entry_product_entry * S ((S (ff_index_mcp_prefix_ics_entry_product)) * pc) + (ff_value_mcp_prefix_ics_entry_product))))))) -> (exists ics_gap_entry_bound. ics_gap_entry_bound + S (i) = (l)) -> (((exists fs_h_ics_entry_decoded. fs_h_ics_entry_decoded + S (z) = S ((S (i)) * pc)) /\ exists fs_q_ics_entry_decoded. pb = fs_q_ics_entry_decoded * S ((S (i)) * pc) + (z))) -> (exists ff_left_mcp_cell_ics_entry_result ff_left_scale_mcp_cell_ics_entry_result ff_right_mcp_cell_ics_entry_result ff_right_scale_mcp_cell_ics_entry_result. ((forall ff_index_mcp_ics_entry_result_row ff_source_mcp_ics_entry_result_row ff_target_mcp_ics_entry_result_row. (exists mcp_gap_ics_entry_result_row_bound. mcp_gap_ics_entry_result_row_bound + S (ff_index_mcp_ics_entry_result_row) = (w)) -> (((exists fs_h_mcp_ics_entry_result_row_source. fs_h_mcp_ics_entry_result_row_source + S (ff_source_mcp_ics_entry_result_row) = S ((S (((i) * (w)) + (1) * ff_index_mcp_ics_entry_result_row)) * ac)) /\ exists fs_q_mcp_ics_entry_result_row_source. ab = fs_q_mcp_ics_entry_result_row_source * S ((S (((i) * (w)) + (1) * ff_index_mcp_ics_entry_result_row)) * ac) + (ff_source_mcp_ics_entry_result_row))) -> (((exists fs_h_mcp_ics_entry_result_row_target. fs_h_mcp_ics_entry_result_row_target + S (ff_target_mcp_ics_entry_result_row) = S ((S (ff_index_mcp_ics_entry_result_row)) * ff_left_scale_mcp_cell_ics_entry_result)) /\ exists fs_q_mcp_ics_entry_result_row_target. ff_left_mcp_cell_ics_entry_result = fs_q_mcp_ics_entry_result_row_target * S ((S (ff_index_mcp_ics_entry_result_row)) * ff_left_scale_mcp_cell_ics_entry_result) + (ff_target_mcp_ics_entry_result_row))) -> ff_target_mcp_ics_entry_result_row = ff_source_mcp_ics_entry_result_row) /\ ((forall ff_index_mcp_ics_entry_result_column ff_source_mcp_ics_entry_result_column ff_target_mcp_ics_entry_result_column. (exists mcp_gap_ics_entry_result_column_bound. mcp_gap_ics_entry_result_column_bound + S (ff_index_mcp_ics_entry_result_column) = (w)) -> (((exists fs_h_mcp_ics_entry_result_column_source. fs_h_mcp_ics_entry_result_column_source + S (ff_source_mcp_ics_entry_result_column) = S ((S ((0) + (1) * ff_index_mcp_ics_entry_result_column)) * bc)) /\ exists fs_q_mcp_ics_entry_result_column_source. bb = fs_q_mcp_ics_entry_result_column_source * S ((S ((0) + (1) * ff_index_mcp_ics_entry_result_column)) * bc) + (ff_source_mcp_ics_entry_result_column))) -> (((exists fs_h_mcp_ics_entry_result_column_target. fs_h_mcp_ics_entry_result_column_target + S (ff_target_mcp_ics_entry_result_column) = S ((S (ff_index_mcp_ics_entry_result_column)) * ff_right_scale_mcp_cell_ics_entry_result)) /\ exists fs_q_mcp_ics_entry_result_column_target. ff_right_mcp_cell_ics_entry_result = fs_q_mcp_ics_entry_result_column_target * S ((S (ff_index_mcp_ics_entry_result_column)) * ff_right_scale_mcp_cell_ics_entry_result) + (ff_target_mcp_ics_entry_result_column))) -> ff_target_mcp_ics_entry_result_column = ff_source_mcp_ics_entry_result_column) /\ (exists ff_code_dot_mcp_ics_entry_result_dot ff_scale_dot_mcp_ics_entry_result_dot. ((forall fpmp_index_dot_mcp_ics_entry_result_dot_pointwise fpmp_left_dot_mcp_ics_entry_result_dot_pointwise fpmp_right_dot_mcp_ics_entry_result_dot_pointwise fpmp_target_dot_mcp_ics_entry_result_dot_pointwise. (exists fpmp_gap_dot_mcp_ics_entry_result_dot_pointwise. fpmp_gap_dot_mcp_ics_entry_result_dot_pointwise + S fpmp_index_dot_mcp_ics_entry_result_dot_pointwise = w) -> (((exists ff_h_fpmp_dot_mcp_ics_entry_result_dot_pointwise_left. ff_h_fpmp_dot_mcp_ics_entry_result_dot_pointwise_left + S (fpmp_left_dot_mcp_ics_entry_result_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_entry_result_dot_pointwise)) * ff_left_scale_mcp_cell_ics_entry_result)) /\ exists ff_q_fpmp_dot_mcp_ics_entry_result_dot_pointwise_left. ff_left_mcp_cell_ics_entry_result = ff_q_fpmp_dot_mcp_ics_entry_result_dot_pointwise_left * S ((S (fpmp_index_dot_mcp_ics_entry_result_dot_pointwise)) * ff_left_scale_mcp_cell_ics_entry_result) + (fpmp_left_dot_mcp_ics_entry_result_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_entry_result_dot_pointwise_right. ff_h_fpmp_dot_mcp_ics_entry_result_dot_pointwise_right + S (fpmp_right_dot_mcp_ics_entry_result_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_entry_result_dot_pointwise)) * ff_right_scale_mcp_cell_ics_entry_result)) /\ exists ff_q_fpmp_dot_mcp_ics_entry_result_dot_pointwise_right. ff_right_mcp_cell_ics_entry_result = ff_q_fpmp_dot_mcp_ics_entry_result_dot_pointwise_right * S ((S (fpmp_index_dot_mcp_ics_entry_result_dot_pointwise)) * ff_right_scale_mcp_cell_ics_entry_result) + (fpmp_right_dot_mcp_ics_entry_result_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_entry_result_dot_pointwise_target. ff_h_fpmp_dot_mcp_ics_entry_result_dot_pointwise_target + S (fpmp_target_dot_mcp_ics_entry_result_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_entry_result_dot_pointwise)) * ff_scale_dot_mcp_ics_entry_result_dot)) /\ exists ff_q_fpmp_dot_mcp_ics_entry_result_dot_pointwise_target. ff_code_dot_mcp_ics_entry_result_dot = ff_q_fpmp_dot_mcp_ics_entry_result_dot_pointwise_target * S ((S (fpmp_index_dot_mcp_ics_entry_result_dot_pointwise)) * ff_scale_dot_mcp_ics_entry_result_dot) + (fpmp_target_dot_mcp_ics_entry_result_dot_pointwise))) -> fpmp_target_dot_mcp_ics_entry_result_dot_pointwise = fpmp_left_dot_mcp_ics_entry_result_dot_pointwise * fpmp_right_dot_mcp_ics_entry_result_dot_pointwise) /\ (exists ff_u_dot_mcp_ics_entry_result_dot_sum ff_v_dot_mcp_ics_entry_result_dot_sum. ((((exists ff_h_dot_mcp_ics_entry_result_dot_sum_start. ff_h_dot_mcp_ics_entry_result_dot_sum_start + S (0) = S ((S (0)) * ff_v_dot_mcp_ics_entry_result_dot_sum)) /\ exists ff_q_dot_mcp_ics_entry_result_dot_sum_start. ff_u_dot_mcp_ics_entry_result_dot_sum = ff_q_dot_mcp_ics_entry_result_dot_sum_start * S ((S (0)) * ff_v_dot_mcp_ics_entry_result_dot_sum) + (0))) /\ ((((exists ff_h_dot_mcp_ics_entry_result_dot_sum_terminal. ff_h_dot_mcp_ics_entry_result_dot_sum_terminal + S (z) = S ((S (w)) * ff_v_dot_mcp_ics_entry_result_dot_sum)) /\ exists ff_q_dot_mcp_ics_entry_result_dot_sum_terminal. ff_u_dot_mcp_ics_entry_result_dot_sum = ff_q_dot_mcp_ics_entry_result_dot_sum_terminal * S ((S (w)) * ff_v_dot_mcp_ics_entry_result_dot_sum) + (z))) /\ forall ff_i_dot_mcp_ics_entry_result_dot_sum. (exists ff_lt_dot_mcp_ics_entry_result_dot_sum_bound. ff_lt_dot_mcp_ics_entry_result_dot_sum_bound + S ff_i_dot_mcp_ics_entry_result_dot_sum = w) -> exists ff_a_dot_mcp_ics_entry_result_dot_sum ff_r_dot_mcp_ics_entry_result_dot_sum ff_s_dot_mcp_ics_entry_result_dot_sum. ((((exists ff_h_dot_mcp_ics_entry_result_dot_sum_summand. ff_h_dot_mcp_ics_entry_result_dot_sum_summand + S (ff_a_dot_mcp_ics_entry_result_dot_sum) = S ((S (ff_i_dot_mcp_ics_entry_result_dot_sum)) * ff_scale_dot_mcp_ics_entry_result_dot)) /\ exists ff_q_dot_mcp_ics_entry_result_dot_sum_summand. ff_code_dot_mcp_ics_entry_result_dot = ff_q_dot_mcp_ics_entry_result_dot_sum_summand * S ((S (ff_i_dot_mcp_ics_entry_result_dot_sum)) * ff_scale_dot_mcp_ics_entry_result_dot) + (ff_a_dot_mcp_ics_entry_result_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_entry_result_dot_sum_partial. ff_h_dot_mcp_ics_entry_result_dot_sum_partial + S (ff_r_dot_mcp_ics_entry_result_dot_sum) = S ((S (ff_i_dot_mcp_ics_entry_result_dot_sum)) * ff_v_dot_mcp_ics_entry_result_dot_sum)) /\ exists ff_q_dot_mcp_ics_entry_result_dot_sum_partial. ff_u_dot_mcp_ics_entry_result_dot_sum = ff_q_dot_mcp_ics_entry_result_dot_sum_partial * S ((S (ff_i_dot_mcp_ics_entry_result_dot_sum)) * ff_v_dot_mcp_ics_entry_result_dot_sum) + (ff_r_dot_mcp_ics_entry_result_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_entry_result_dot_sum_successor. ff_h_dot_mcp_ics_entry_result_dot_sum_successor + S (ff_s_dot_mcp_ics_entry_result_dot_sum) = S ((S (S ff_i_dot_mcp_ics_entry_result_dot_sum)) * ff_v_dot_mcp_ics_entry_result_dot_sum)) /\ exists ff_q_dot_mcp_ics_entry_result_dot_sum_successor. ff_u_dot_mcp_ics_entry_result_dot_sum = ff_q_dot_mcp_ics_entry_result_dot_sum_successor * S ((S (S ff_i_dot_mcp_ics_entry_result_dot_sum)) * ff_v_dot_mcp_ics_entry_result_dot_sum) + (ff_s_dot_mcp_ics_entry_result_dot_sum))) /\ ff_s_dot_mcp_ics_entry_result_dot_sum = ff_r_dot_mcp_ics_entry_result_dot_sum + ff_a_dot_mcp_ics_entry_result_dot_sum)))))))))))

Constructive proof overview

Generated structural guide

Every actual entry of a one-column coded matrix product is the genuine cell at that same row, by bounded column-zero and beta uniqueness, not an arbitrary output witness.

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

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

Proof neighborhood

Direct dependencies

le_zero Stable theorem; checked-use authorized le_of_succ_le_succ Stable theorem; checked-use authorized one_mul Stable theorem; checked-use authorized beta_at_unique Stable theorem; checked-use authorized

Direct dependents

DL0067 integer_span_natural_product_add_right

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

Read the argument

Proof checkpoints

54 script commands · 10 reading checkpoints · 5 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 w
  6. L6
    intro pb
  7. L7
    intro pc
  8. L8
    intro l
  9. L9
    intro i
  10. L10
    intro z
02Fix variables and assumptionsL11–13

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

  1. L11
    intro hproduct
  2. L12
    intro hi
  3. L13
    intro hz
03Establish hentryL14–17

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

  1. L14
    have hentry : ∃ row. ∃ column. ∃ value. i = 1 · row + column ∧ (Lt(column,1) ∧ (MatrixProductCell(ab,ac,bb,bc,w,1,row,column,value) ∧ BetaAt(pb,pc,i,value)))Definitions: MatrixProductCellLtBetaAt
  2. L15
    specialize hproduct (i)
  3. L16
    apply hproduct
  4. L17
    exact hi
04Separate the logical casesL18–23

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

  1. L18
    cases hentry
  2. L19
    cases hentry_witness
  3. L20
    cases hentry_witness_witness
  4. L21
    cases hentry_witness_witness_witness
  5. L22
    cases hentry_witness_witness_witness_right
  6. L23
    cases hentry_witness_witness_witness_right_right
05Establish hcolL24–30

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

  1. L24
    have hcol : x1 = 0
  2. L25
    specialize le_zero (x1)
  3. L26
    apply le_zero
  4. L27
    specialize le_of_succ_le_succ (x1)
  5. L28
    specialize le_of_succ_le_succ (0)
  6. L29
    apply le_of_succ_le_succ
  7. L30
    exact hentry_witness_witness_witness_right_left
06Establish hrowL31–36

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

  1. L31
    have hrow : x = i
  2. L32
    symm
  3. L33
    trans 1 * x + x1
  4. L34
    exact hentry_witness_witness_witness_left
  5. L35
    rewrite hcol
  6. L36
    simp [one_mul]
07Establish hcL37–42

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

  1. L37
    have hc : MatrixProductCell(ab,ac,bb,bc,w,1,x,x1,x2)Definitions: MatrixProductCell
  2. L38
    exact hentry_witness_witness_witness_right_right_left
  3. L39
    rewrite hcol at hc
  4. L40
    rewrite hcol at hc
  5. L41
    rewrite hrow at hc
  6. L42
    rewrite hrow at hc
08Establish hvalueL43–52

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

  1. L43
    have hvalue : x2 = z
  2. L44
    specialize beta_at_unique (pb)
  3. L45
    specialize beta_at_unique (pc)
  4. L46
    specialize beta_at_unique (i)
  5. L47
    specialize beta_at_unique (x2)
  6. L48
    specialize beta_at_unique (z)
  7. L49
    apply beta_at_unique
  8. L50
    exact hentry_witness_witness_witness_right_right_right
  9. L51
    exact hz
  10. L52
    rewrite hvalue at hc
09Calculate and transport equalitiesL53–53

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

  1. L53
    rewrite hvalue at hc
10Use earlier factsL54–54

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

  1. L54
    exact hc

Library-wide reading audit

Original exact command ledger · 54 lines
  1. 0001intro ab
  2. 0002intro ac
  3. 0003intro bb
  4. 0004intro bc
  5. 0005intro w
  6. 0006intro pb
  7. 0007intro pc
  8. 0008intro l
  9. 0009intro i
  10. 0010intro z
  11. 0011intro hproduct
  12. 0012intro hi
  13. 0013intro hz
  14. 0014have hentry : exists row column value. ((i = 1 * row + column) /\ (((exists ics_gap_entry_column. ics_gap_entry_column + S (column) = (1)) /\ (((exists ff_left_mcp_cell_ics_entry_cell ff_left_scale_mcp_cell_ics_entry_cell ff_right_mcp_cell_ics_entry_cell ff_right_scale_mcp_cell_ics_entry_cell. ((forall ff_index_mcp_ics_entry_cell_row ff_source_mcp_ics_entry_cell_row ff_target_mcp_ics_entry_cell_row. (exists mcp_gap_ics_entry_cell_row_bound. mcp_gap_ics_entry_cell_row_bound + S (ff_index_mcp_ics_entry_cell_row) = (w)) -> (((exists fs_h_mcp_ics_entry_cell_row_source. fs_h_mcp_ics_entry_cell_row_source + S (ff_source_mcp_ics_entry_cell_row) = S ((S (((row) * (w)) + (1) * ff_index_mcp_ics_entry_cell_row)) * ac)) /\ exists fs_q_mcp_ics_entry_cell_row_source. ab = fs_q_mcp_ics_entry_cell_row_source * S ((S (((row) * (w)) + (1) * ff_index_mcp_ics_entry_cell_row)) * ac) + (ff_source_mcp_ics_entry_cell_row))) -> (((exists fs_h_mcp_ics_entry_cell_row_target. fs_h_mcp_ics_entry_cell_row_target + S (ff_target_mcp_ics_entry_cell_row) = S ((S (ff_index_mcp_ics_entry_cell_row)) * ff_left_scale_mcp_cell_ics_entry_cell)) /\ exists fs_q_mcp_ics_entry_cell_row_target. ff_left_mcp_cell_ics_entry_cell = fs_q_mcp_ics_entry_cell_row_target * S ((S (ff_index_mcp_ics_entry_cell_row)) * ff_left_scale_mcp_cell_ics_entry_cell) + (ff_target_mcp_ics_entry_cell_row))) -> ff_target_mcp_ics_entry_cell_row = ff_source_mcp_ics_entry_cell_row) /\ ((forall ff_index_mcp_ics_entry_cell_column ff_source_mcp_ics_entry_cell_column ff_target_mcp_ics_entry_cell_column. (exists mcp_gap_ics_entry_cell_column_bound. mcp_gap_ics_entry_cell_column_bound + S (ff_index_mcp_ics_entry_cell_column) = (w)) -> (((exists fs_h_mcp_ics_entry_cell_column_source. fs_h_mcp_ics_entry_cell_column_source + S (ff_source_mcp_ics_entry_cell_column) = S ((S ((column) + (1) * ff_index_mcp_ics_entry_cell_column)) * bc)) /\ exists fs_q_mcp_ics_entry_cell_column_source. bb = fs_q_mcp_ics_entry_cell_column_source * S ((S ((column) + (1) * ff_index_mcp_ics_entry_cell_column)) * bc) + (ff_source_mcp_ics_entry_cell_column))) -> (((exists fs_h_mcp_ics_entry_cell_column_target. fs_h_mcp_ics_entry_cell_column_target + S (ff_target_mcp_ics_entry_cell_column) = S ((S (ff_index_mcp_ics_entry_cell_column)) * ff_right_scale_mcp_cell_ics_entry_cell)) /\ exists fs_q_mcp_ics_entry_cell_column_target. ff_right_mcp_cell_ics_entry_cell = fs_q_mcp_ics_entry_cell_column_target * S ((S (ff_index_mcp_ics_entry_cell_column)) * ff_right_scale_mcp_cell_ics_entry_cell) + (ff_target_mcp_ics_entry_cell_column))) -> ff_target_mcp_ics_entry_cell_column = ff_source_mcp_ics_entry_cell_column) /\ (exists ff_code_dot_mcp_ics_entry_cell_dot ff_scale_dot_mcp_ics_entry_cell_dot. ((forall fpmp_index_dot_mcp_ics_entry_cell_dot_pointwise fpmp_left_dot_mcp_ics_entry_cell_dot_pointwise fpmp_right_dot_mcp_ics_entry_cell_dot_pointwise fpmp_target_dot_mcp_ics_entry_cell_dot_pointwise. (exists fpmp_gap_dot_mcp_ics_entry_cell_dot_pointwise. fpmp_gap_dot_mcp_ics_entry_cell_dot_pointwise + S fpmp_index_dot_mcp_ics_entry_cell_dot_pointwise = w) -> (((exists ff_h_fpmp_dot_mcp_ics_entry_cell_dot_pointwise_left. ff_h_fpmp_dot_mcp_ics_entry_cell_dot_pointwise_left + S (fpmp_left_dot_mcp_ics_entry_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_entry_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_entry_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_entry_cell_dot_pointwise_left. ff_left_mcp_cell_ics_entry_cell = ff_q_fpmp_dot_mcp_ics_entry_cell_dot_pointwise_left * S ((S (fpmp_index_dot_mcp_ics_entry_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_entry_cell) + (fpmp_left_dot_mcp_ics_entry_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_entry_cell_dot_pointwise_right. ff_h_fpmp_dot_mcp_ics_entry_cell_dot_pointwise_right + S (fpmp_right_dot_mcp_ics_entry_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_entry_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_entry_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_entry_cell_dot_pointwise_right. ff_right_mcp_cell_ics_entry_cell = ff_q_fpmp_dot_mcp_ics_entry_cell_dot_pointwise_right * S ((S (fpmp_index_dot_mcp_ics_entry_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_entry_cell) + (fpmp_right_dot_mcp_ics_entry_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_entry_cell_dot_pointwise_target. ff_h_fpmp_dot_mcp_ics_entry_cell_dot_pointwise_target + S (fpmp_target_dot_mcp_ics_entry_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_entry_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_entry_cell_dot)) /\ exists ff_q_fpmp_dot_mcp_ics_entry_cell_dot_pointwise_target. ff_code_dot_mcp_ics_entry_cell_dot = ff_q_fpmp_dot_mcp_ics_entry_cell_dot_pointwise_target * S ((S (fpmp_index_dot_mcp_ics_entry_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_entry_cell_dot) + (fpmp_target_dot_mcp_ics_entry_cell_dot_pointwise))) -> fpmp_target_dot_mcp_ics_entry_cell_dot_pointwise = fpmp_left_dot_mcp_ics_entry_cell_dot_pointwise * fpmp_right_dot_mcp_ics_entry_cell_dot_pointwise) /\ (exists ff_u_dot_mcp_ics_entry_cell_dot_sum ff_v_dot_mcp_ics_entry_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_entry_cell_dot_sum_start. ff_h_dot_mcp_ics_entry_cell_dot_sum_start + S (0) = S ((S (0)) * ff_v_dot_mcp_ics_entry_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_entry_cell_dot_sum_start. ff_u_dot_mcp_ics_entry_cell_dot_sum = ff_q_dot_mcp_ics_entry_cell_dot_sum_start * S ((S (0)) * ff_v_dot_mcp_ics_entry_cell_dot_sum) + (0))) /\ ((((exists ff_h_dot_mcp_ics_entry_cell_dot_sum_terminal. ff_h_dot_mcp_ics_entry_cell_dot_sum_terminal + S (value) = S ((S (w)) * ff_v_dot_mcp_ics_entry_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_entry_cell_dot_sum_terminal. ff_u_dot_mcp_ics_entry_cell_dot_sum = ff_q_dot_mcp_ics_entry_cell_dot_sum_terminal * S ((S (w)) * ff_v_dot_mcp_ics_entry_cell_dot_sum) + (value))) /\ forall ff_i_dot_mcp_ics_entry_cell_dot_sum. (exists ff_lt_dot_mcp_ics_entry_cell_dot_sum_bound. ff_lt_dot_mcp_ics_entry_cell_dot_sum_bound + S ff_i_dot_mcp_ics_entry_cell_dot_sum = w) -> exists ff_a_dot_mcp_ics_entry_cell_dot_sum ff_r_dot_mcp_ics_entry_cell_dot_sum ff_s_dot_mcp_ics_entry_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_entry_cell_dot_sum_summand. ff_h_dot_mcp_ics_entry_cell_dot_sum_summand + S (ff_a_dot_mcp_ics_entry_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_entry_cell_dot_sum)) * ff_scale_dot_mcp_ics_entry_cell_dot)) /\ exists ff_q_dot_mcp_ics_entry_cell_dot_sum_summand. ff_code_dot_mcp_ics_entry_cell_dot = ff_q_dot_mcp_ics_entry_cell_dot_sum_summand * S ((S (ff_i_dot_mcp_ics_entry_cell_dot_sum)) * ff_scale_dot_mcp_ics_entry_cell_dot) + (ff_a_dot_mcp_ics_entry_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_entry_cell_dot_sum_partial. ff_h_dot_mcp_ics_entry_cell_dot_sum_partial + S (ff_r_dot_mcp_ics_entry_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_entry_cell_dot_sum)) * ff_v_dot_mcp_ics_entry_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_entry_cell_dot_sum_partial. ff_u_dot_mcp_ics_entry_cell_dot_sum = ff_q_dot_mcp_ics_entry_cell_dot_sum_partial * S ((S (ff_i_dot_mcp_ics_entry_cell_dot_sum)) * ff_v_dot_mcp_ics_entry_cell_dot_sum) + (ff_r_dot_mcp_ics_entry_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_entry_cell_dot_sum_successor. ff_h_dot_mcp_ics_entry_cell_dot_sum_successor + S (ff_s_dot_mcp_ics_entry_cell_dot_sum) = S ((S (S ff_i_dot_mcp_ics_entry_cell_dot_sum)) * ff_v_dot_mcp_ics_entry_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_entry_cell_dot_sum_successor. ff_u_dot_mcp_ics_entry_cell_dot_sum = ff_q_dot_mcp_ics_entry_cell_dot_sum_successor * S ((S (S ff_i_dot_mcp_ics_entry_cell_dot_sum)) * ff_v_dot_mcp_ics_entry_cell_dot_sum) + (ff_s_dot_mcp_ics_entry_cell_dot_sum))) /\ ff_s_dot_mcp_ics_entry_cell_dot_sum = ff_r_dot_mcp_ics_entry_cell_dot_sum + ff_a_dot_mcp_ics_entry_cell_dot_sum))))))))))) /\ (((exists fs_h_ics_entry_value. fs_h_ics_entry_value + S (value) = S ((S (i)) * pc)) /\ exists fs_q_ics_entry_value. pb = fs_q_ics_entry_value * S ((S (i)) * pc) + (value))))))))
  15. 0015specialize hproduct (i)
  16. 0016apply hproduct
  17. 0017exact hi
  18. 0018cases hentry
  19. 0019cases hentry_witness
  20. 0020cases hentry_witness_witness
  21. 0021cases hentry_witness_witness_witness
  22. 0022cases hentry_witness_witness_witness_right
  23. 0023cases hentry_witness_witness_witness_right_right
  24. 0024have hcol : x1 = 0
  25. 0025specialize le_zero (x1)
  26. 0026apply le_zero
  27. 0027specialize le_of_succ_le_succ (x1)
  28. 0028specialize le_of_succ_le_succ (0)
  29. 0029apply le_of_succ_le_succ
  30. 0030exact hentry_witness_witness_witness_right_left
  31. 0031have hrow : x = i
  32. 0032symm
  33. 0033trans 1 * x + x1
  34. 0034exact hentry_witness_witness_witness_left
  35. 0035rewrite hcol
  36. 0036simp [one_mul]
  37. 0037have hc : exists ff_left_mcp_cell_ics_entry_actual ff_left_scale_mcp_cell_ics_entry_actual ff_right_mcp_cell_ics_entry_actual ff_right_scale_mcp_cell_ics_entry_actual. ((forall ff_index_mcp_ics_entry_actual_row ff_source_mcp_ics_entry_actual_row ff_target_mcp_ics_entry_actual_row. (exists mcp_gap_ics_entry_actual_row_bound. mcp_gap_ics_entry_actual_row_bound + S (ff_index_mcp_ics_entry_actual_row) = (w)) -> (((exists fs_h_mcp_ics_entry_actual_row_source. fs_h_mcp_ics_entry_actual_row_source + S (ff_source_mcp_ics_entry_actual_row) = S ((S (((x) * (w)) + (1) * ff_index_mcp_ics_entry_actual_row)) * ac)) /\ exists fs_q_mcp_ics_entry_actual_row_source. ab = fs_q_mcp_ics_entry_actual_row_source * S ((S (((x) * (w)) + (1) * ff_index_mcp_ics_entry_actual_row)) * ac) + (ff_source_mcp_ics_entry_actual_row))) -> (((exists fs_h_mcp_ics_entry_actual_row_target. fs_h_mcp_ics_entry_actual_row_target + S (ff_target_mcp_ics_entry_actual_row) = S ((S (ff_index_mcp_ics_entry_actual_row)) * ff_left_scale_mcp_cell_ics_entry_actual)) /\ exists fs_q_mcp_ics_entry_actual_row_target. ff_left_mcp_cell_ics_entry_actual = fs_q_mcp_ics_entry_actual_row_target * S ((S (ff_index_mcp_ics_entry_actual_row)) * ff_left_scale_mcp_cell_ics_entry_actual) + (ff_target_mcp_ics_entry_actual_row))) -> ff_target_mcp_ics_entry_actual_row = ff_source_mcp_ics_entry_actual_row) /\ ((forall ff_index_mcp_ics_entry_actual_column ff_source_mcp_ics_entry_actual_column ff_target_mcp_ics_entry_actual_column. (exists mcp_gap_ics_entry_actual_column_bound. mcp_gap_ics_entry_actual_column_bound + S (ff_index_mcp_ics_entry_actual_column) = (w)) -> (((exists fs_h_mcp_ics_entry_actual_column_source. fs_h_mcp_ics_entry_actual_column_source + S (ff_source_mcp_ics_entry_actual_column) = S ((S ((x1) + (1) * ff_index_mcp_ics_entry_actual_column)) * bc)) /\ exists fs_q_mcp_ics_entry_actual_column_source. bb = fs_q_mcp_ics_entry_actual_column_source * S ((S ((x1) + (1) * ff_index_mcp_ics_entry_actual_column)) * bc) + (ff_source_mcp_ics_entry_actual_column))) -> (((exists fs_h_mcp_ics_entry_actual_column_target. fs_h_mcp_ics_entry_actual_column_target + S (ff_target_mcp_ics_entry_actual_column) = S ((S (ff_index_mcp_ics_entry_actual_column)) * ff_right_scale_mcp_cell_ics_entry_actual)) /\ exists fs_q_mcp_ics_entry_actual_column_target. ff_right_mcp_cell_ics_entry_actual = fs_q_mcp_ics_entry_actual_column_target * S ((S (ff_index_mcp_ics_entry_actual_column)) * ff_right_scale_mcp_cell_ics_entry_actual) + (ff_target_mcp_ics_entry_actual_column))) -> ff_target_mcp_ics_entry_actual_column = ff_source_mcp_ics_entry_actual_column) /\ (exists ff_code_dot_mcp_ics_entry_actual_dot ff_scale_dot_mcp_ics_entry_actual_dot. ((forall fpmp_index_dot_mcp_ics_entry_actual_dot_pointwise fpmp_left_dot_mcp_ics_entry_actual_dot_pointwise fpmp_right_dot_mcp_ics_entry_actual_dot_pointwise fpmp_target_dot_mcp_ics_entry_actual_dot_pointwise. (exists fpmp_gap_dot_mcp_ics_entry_actual_dot_pointwise. fpmp_gap_dot_mcp_ics_entry_actual_dot_pointwise + S fpmp_index_dot_mcp_ics_entry_actual_dot_pointwise = w) -> (((exists ff_h_fpmp_dot_mcp_ics_entry_actual_dot_pointwise_left. ff_h_fpmp_dot_mcp_ics_entry_actual_dot_pointwise_left + S (fpmp_left_dot_mcp_ics_entry_actual_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_entry_actual_dot_pointwise)) * ff_left_scale_mcp_cell_ics_entry_actual)) /\ exists ff_q_fpmp_dot_mcp_ics_entry_actual_dot_pointwise_left. ff_left_mcp_cell_ics_entry_actual = ff_q_fpmp_dot_mcp_ics_entry_actual_dot_pointwise_left * S ((S (fpmp_index_dot_mcp_ics_entry_actual_dot_pointwise)) * ff_left_scale_mcp_cell_ics_entry_actual) + (fpmp_left_dot_mcp_ics_entry_actual_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_entry_actual_dot_pointwise_right. ff_h_fpmp_dot_mcp_ics_entry_actual_dot_pointwise_right + S (fpmp_right_dot_mcp_ics_entry_actual_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_entry_actual_dot_pointwise)) * ff_right_scale_mcp_cell_ics_entry_actual)) /\ exists ff_q_fpmp_dot_mcp_ics_entry_actual_dot_pointwise_right. ff_right_mcp_cell_ics_entry_actual = ff_q_fpmp_dot_mcp_ics_entry_actual_dot_pointwise_right * S ((S (fpmp_index_dot_mcp_ics_entry_actual_dot_pointwise)) * ff_right_scale_mcp_cell_ics_entry_actual) + (fpmp_right_dot_mcp_ics_entry_actual_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_entry_actual_dot_pointwise_target. ff_h_fpmp_dot_mcp_ics_entry_actual_dot_pointwise_target + S (fpmp_target_dot_mcp_ics_entry_actual_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_entry_actual_dot_pointwise)) * ff_scale_dot_mcp_ics_entry_actual_dot)) /\ exists ff_q_fpmp_dot_mcp_ics_entry_actual_dot_pointwise_target. ff_code_dot_mcp_ics_entry_actual_dot = ff_q_fpmp_dot_mcp_ics_entry_actual_dot_pointwise_target * S ((S (fpmp_index_dot_mcp_ics_entry_actual_dot_pointwise)) * ff_scale_dot_mcp_ics_entry_actual_dot) + (fpmp_target_dot_mcp_ics_entry_actual_dot_pointwise))) -> fpmp_target_dot_mcp_ics_entry_actual_dot_pointwise = fpmp_left_dot_mcp_ics_entry_actual_dot_pointwise * fpmp_right_dot_mcp_ics_entry_actual_dot_pointwise) /\ (exists ff_u_dot_mcp_ics_entry_actual_dot_sum ff_v_dot_mcp_ics_entry_actual_dot_sum. ((((exists ff_h_dot_mcp_ics_entry_actual_dot_sum_start. ff_h_dot_mcp_ics_entry_actual_dot_sum_start + S (0) = S ((S (0)) * ff_v_dot_mcp_ics_entry_actual_dot_sum)) /\ exists ff_q_dot_mcp_ics_entry_actual_dot_sum_start. ff_u_dot_mcp_ics_entry_actual_dot_sum = ff_q_dot_mcp_ics_entry_actual_dot_sum_start * S ((S (0)) * ff_v_dot_mcp_ics_entry_actual_dot_sum) + (0))) /\ ((((exists ff_h_dot_mcp_ics_entry_actual_dot_sum_terminal. ff_h_dot_mcp_ics_entry_actual_dot_sum_terminal + S (x2) = S ((S (w)) * ff_v_dot_mcp_ics_entry_actual_dot_sum)) /\ exists ff_q_dot_mcp_ics_entry_actual_dot_sum_terminal. ff_u_dot_mcp_ics_entry_actual_dot_sum = ff_q_dot_mcp_ics_entry_actual_dot_sum_terminal * S ((S (w)) * ff_v_dot_mcp_ics_entry_actual_dot_sum) + (x2))) /\ forall ff_i_dot_mcp_ics_entry_actual_dot_sum. (exists ff_lt_dot_mcp_ics_entry_actual_dot_sum_bound. ff_lt_dot_mcp_ics_entry_actual_dot_sum_bound + S ff_i_dot_mcp_ics_entry_actual_dot_sum = w) -> exists ff_a_dot_mcp_ics_entry_actual_dot_sum ff_r_dot_mcp_ics_entry_actual_dot_sum ff_s_dot_mcp_ics_entry_actual_dot_sum. ((((exists ff_h_dot_mcp_ics_entry_actual_dot_sum_summand. ff_h_dot_mcp_ics_entry_actual_dot_sum_summand + S (ff_a_dot_mcp_ics_entry_actual_dot_sum) = S ((S (ff_i_dot_mcp_ics_entry_actual_dot_sum)) * ff_scale_dot_mcp_ics_entry_actual_dot)) /\ exists ff_q_dot_mcp_ics_entry_actual_dot_sum_summand. ff_code_dot_mcp_ics_entry_actual_dot = ff_q_dot_mcp_ics_entry_actual_dot_sum_summand * S ((S (ff_i_dot_mcp_ics_entry_actual_dot_sum)) * ff_scale_dot_mcp_ics_entry_actual_dot) + (ff_a_dot_mcp_ics_entry_actual_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_entry_actual_dot_sum_partial. ff_h_dot_mcp_ics_entry_actual_dot_sum_partial + S (ff_r_dot_mcp_ics_entry_actual_dot_sum) = S ((S (ff_i_dot_mcp_ics_entry_actual_dot_sum)) * ff_v_dot_mcp_ics_entry_actual_dot_sum)) /\ exists ff_q_dot_mcp_ics_entry_actual_dot_sum_partial. ff_u_dot_mcp_ics_entry_actual_dot_sum = ff_q_dot_mcp_ics_entry_actual_dot_sum_partial * S ((S (ff_i_dot_mcp_ics_entry_actual_dot_sum)) * ff_v_dot_mcp_ics_entry_actual_dot_sum) + (ff_r_dot_mcp_ics_entry_actual_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_entry_actual_dot_sum_successor. ff_h_dot_mcp_ics_entry_actual_dot_sum_successor + S (ff_s_dot_mcp_ics_entry_actual_dot_sum) = S ((S (S ff_i_dot_mcp_ics_entry_actual_dot_sum)) * ff_v_dot_mcp_ics_entry_actual_dot_sum)) /\ exists ff_q_dot_mcp_ics_entry_actual_dot_sum_successor. ff_u_dot_mcp_ics_entry_actual_dot_sum = ff_q_dot_mcp_ics_entry_actual_dot_sum_successor * S ((S (S ff_i_dot_mcp_ics_entry_actual_dot_sum)) * ff_v_dot_mcp_ics_entry_actual_dot_sum) + (ff_s_dot_mcp_ics_entry_actual_dot_sum))) /\ ff_s_dot_mcp_ics_entry_actual_dot_sum = ff_r_dot_mcp_ics_entry_actual_dot_sum + ff_a_dot_mcp_ics_entry_actual_dot_sum))))))))))
  38. 0038exact hentry_witness_witness_witness_right_right_left
  39. 0039rewrite hcol at hc
  40. 0040rewrite hcol at hc
  41. 0041rewrite hrow at hc
  42. 0042rewrite hrow at hc
  43. 0043have hvalue : x2 = z
  44. 0044specialize beta_at_unique (pb)
  45. 0045specialize beta_at_unique (pc)
  46. 0046specialize beta_at_unique (i)
  47. 0047specialize beta_at_unique (x2)
  48. 0048specialize beta_at_unique (z)
  49. 0049apply beta_at_unique
  50. 0050exact hentry_witness_witness_witness_right_right_right
  51. 0051exact hz
  52. 0052rewrite hvalue at hc
  53. 0053rewrite hvalue at hc
  54. 0054exact hc