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.
Definition in prerequisite notation
∃ ff_left_mcp_cell_advanced. ∃ ff_left_scale_mcp_cell_advanced. ∃ ff_right_mcp_cell_advanced. ∃ ff_right_scale_mcp_cell_advanced. MatrixAffineSlice(lb,lc,i · w,1,ff_left_mcp_cell_advanced,ff_left_scale_mcp_cell_advanced,w) ∧ (MatrixAffineSlice(rb,rc,j,v,ff_right_mcp_cell_advanced,ff_right_scale_mcp_cell_advanced,w) ∧ DotProduct(ff_left_mcp_cell_advanced,ff_left_scale_mcp_cell_advanced,ff_right_mcp_cell_advanced,ff_right_scale_mcp_cell_advanced,w,n))Only definitions earlier in this acyclic notation graph are used here.
Hygienic expanded first-order definition
exists ff_left_mcp_cell_advanced ff_left_scale_mcp_cell_advanced ff_right_mcp_cell_advanced ff_right_scale_mcp_cell_advanced. ((forall ff_index_mcp_advanced_row ff_source_mcp_advanced_row ff_target_mcp_advanced_row. (exists mcp_gap_advanced_row_bound. mcp_gap_advanced_row_bound + S (ff_index_mcp_advanced_row) = (w)) -> (((exists fs_h_mcp_advanced_row_source. fs_h_mcp_advanced_row_source + S (ff_source_mcp_advanced_row) = S ((S (((i) * (w)) + (1) * ff_index_mcp_advanced_row)) * lc)) /\ exists fs_q_mcp_advanced_row_source. lb = fs_q_mcp_advanced_row_source * S ((S (((i) * (w)) + (1) * ff_index_mcp_advanced_row)) * lc) + (ff_source_mcp_advanced_row))) -> (((exists fs_h_mcp_advanced_row_target. fs_h_mcp_advanced_row_target + S (ff_target_mcp_advanced_row) = S ((S (ff_index_mcp_advanced_row)) * ff_left_scale_mcp_cell_advanced)) /\ exists fs_q_mcp_advanced_row_target. ff_left_mcp_cell_advanced = fs_q_mcp_advanced_row_target * S ((S (ff_index_mcp_advanced_row)) * ff_left_scale_mcp_cell_advanced) + (ff_target_mcp_advanced_row))) -> ff_target_mcp_advanced_row = ff_source_mcp_advanced_row) /\ ((forall ff_index_mcp_advanced_column ff_source_mcp_advanced_column ff_target_mcp_advanced_column. (exists mcp_gap_advanced_column_bound. mcp_gap_advanced_column_bound + S (ff_index_mcp_advanced_column) = (w)) -> (((exists fs_h_mcp_advanced_column_source. fs_h_mcp_advanced_column_source + S (ff_source_mcp_advanced_column) = S ((S ((j) + (v) * ff_index_mcp_advanced_column)) * rc)) /\ exists fs_q_mcp_advanced_column_source. rb = fs_q_mcp_advanced_column_source * S ((S ((j) + (v) * ff_index_mcp_advanced_column)) * rc) + (ff_source_mcp_advanced_column))) -> (((exists fs_h_mcp_advanced_column_target. fs_h_mcp_advanced_column_target + S (ff_target_mcp_advanced_column) = S ((S (ff_index_mcp_advanced_column)) * ff_right_scale_mcp_cell_advanced)) /\ exists fs_q_mcp_advanced_column_target. ff_right_mcp_cell_advanced = fs_q_mcp_advanced_column_target * S ((S (ff_index_mcp_advanced_column)) * ff_right_scale_mcp_cell_advanced) + (ff_target_mcp_advanced_column))) -> ff_target_mcp_advanced_column = ff_source_mcp_advanced_column) /\ (exists ff_code_dot_mcp_advanced_dot ff_scale_dot_mcp_advanced_dot. ((forall fpmp_index_dot_mcp_advanced_dot_pointwise fpmp_left_dot_mcp_advanced_dot_pointwise fpmp_right_dot_mcp_advanced_dot_pointwise fpmp_target_dot_mcp_advanced_dot_pointwise. (exists fpmp_gap_dot_mcp_advanced_dot_pointwise. fpmp_gap_dot_mcp_advanced_dot_pointwise + S fpmp_index_dot_mcp_advanced_dot_pointwise = w) -> (((exists ff_h_fpmp_dot_mcp_advanced_dot_pointwise_left. ff_h_fpmp_dot_mcp_advanced_dot_pointwise_left + S (fpmp_left_dot_mcp_advanced_dot_pointwise) = S ((S (fpmp_index_dot_mcp_advanced_dot_pointwise)) * ff_left_scale_mcp_cell_advanced)) /\ exists ff_q_fpmp_dot_mcp_advanced_dot_pointwise_left. ff_left_mcp_cell_advanced = ff_q_fpmp_dot_mcp_advanced_dot_pointwise_left * S ((S (fpmp_index_dot_mcp_advanced_dot_pointwise)) * ff_left_scale_mcp_cell_advanced) + (fpmp_left_dot_mcp_advanced_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_advanced_dot_pointwise_right. ff_h_fpmp_dot_mcp_advanced_dot_pointwise_right + S (fpmp_right_dot_mcp_advanced_dot_pointwise) = S ((S (fpmp_index_dot_mcp_advanced_dot_pointwise)) * ff_right_scale_mcp_cell_advanced)) /\ exists ff_q_fpmp_dot_mcp_advanced_dot_pointwise_right. ff_right_mcp_cell_advanced = ff_q_fpmp_dot_mcp_advanced_dot_pointwise_right * S ((S (fpmp_index_dot_mcp_advanced_dot_pointwise)) * ff_right_scale_mcp_cell_advanced) + (fpmp_right_dot_mcp_advanced_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_advanced_dot_pointwise_target. ff_h_fpmp_dot_mcp_advanced_dot_pointwise_target + S (fpmp_target_dot_mcp_advanced_dot_pointwise) = S ((S (fpmp_index_dot_mcp_advanced_dot_pointwise)) * ff_scale_dot_mcp_advanced_dot)) /\ exists ff_q_fpmp_dot_mcp_advanced_dot_pointwise_target. ff_code_dot_mcp_advanced_dot = ff_q_fpmp_dot_mcp_advanced_dot_pointwise_target * S ((S (fpmp_index_dot_mcp_advanced_dot_pointwise)) * ff_scale_dot_mcp_advanced_dot) + (fpmp_target_dot_mcp_advanced_dot_pointwise))) -> fpmp_target_dot_mcp_advanced_dot_pointwise = fpmp_left_dot_mcp_advanced_dot_pointwise * fpmp_right_dot_mcp_advanced_dot_pointwise) /\ (exists ff_u_dot_mcp_advanced_dot_sum ff_v_dot_mcp_advanced_dot_sum. ((((exists ff_h_dot_mcp_advanced_dot_sum_start. ff_h_dot_mcp_advanced_dot_sum_start + S (0) = S ((S (0)) * ff_v_dot_mcp_advanced_dot_sum)) /\ exists ff_q_dot_mcp_advanced_dot_sum_start. ff_u_dot_mcp_advanced_dot_sum = ff_q_dot_mcp_advanced_dot_sum_start * S ((S (0)) * ff_v_dot_mcp_advanced_dot_sum) + (0))) /\ ((((exists ff_h_dot_mcp_advanced_dot_sum_terminal. ff_h_dot_mcp_advanced_dot_sum_terminal + S (n) = S ((S (w)) * ff_v_dot_mcp_advanced_dot_sum)) /\ exists ff_q_dot_mcp_advanced_dot_sum_terminal. ff_u_dot_mcp_advanced_dot_sum = ff_q_dot_mcp_advanced_dot_sum_terminal * S ((S (w)) * ff_v_dot_mcp_advanced_dot_sum) + (n))) /\ forall ff_i_dot_mcp_advanced_dot_sum. (exists ff_lt_dot_mcp_advanced_dot_sum_bound. ff_lt_dot_mcp_advanced_dot_sum_bound + S ff_i_dot_mcp_advanced_dot_sum = w) -> exists ff_a_dot_mcp_advanced_dot_sum ff_r_dot_mcp_advanced_dot_sum ff_s_dot_mcp_advanced_dot_sum. ((((exists ff_h_dot_mcp_advanced_dot_sum_summand. ff_h_dot_mcp_advanced_dot_sum_summand + S (ff_a_dot_mcp_advanced_dot_sum) = S ((S (ff_i_dot_mcp_advanced_dot_sum)) * ff_scale_dot_mcp_advanced_dot)) /\ exists ff_q_dot_mcp_advanced_dot_sum_summand. ff_code_dot_mcp_advanced_dot = ff_q_dot_mcp_advanced_dot_sum_summand * S ((S (ff_i_dot_mcp_advanced_dot_sum)) * ff_scale_dot_mcp_advanced_dot) + (ff_a_dot_mcp_advanced_dot_sum))) /\ ((((exists ff_h_dot_mcp_advanced_dot_sum_partial. ff_h_dot_mcp_advanced_dot_sum_partial + S (ff_r_dot_mcp_advanced_dot_sum) = S ((S (ff_i_dot_mcp_advanced_dot_sum)) * ff_v_dot_mcp_advanced_dot_sum)) /\ exists ff_q_dot_mcp_advanced_dot_sum_partial. ff_u_dot_mcp_advanced_dot_sum = ff_q_dot_mcp_advanced_dot_sum_partial * S ((S (ff_i_dot_mcp_advanced_dot_sum)) * ff_v_dot_mcp_advanced_dot_sum) + (ff_r_dot_mcp_advanced_dot_sum))) /\ ((((exists ff_h_dot_mcp_advanced_dot_sum_successor. ff_h_dot_mcp_advanced_dot_sum_successor + S (ff_s_dot_mcp_advanced_dot_sum) = S ((S (S ff_i_dot_mcp_advanced_dot_sum)) * ff_v_dot_mcp_advanced_dot_sum)) /\ exists ff_q_dot_mcp_advanced_dot_sum_successor. ff_u_dot_mcp_advanced_dot_sum = ff_q_dot_mcp_advanced_dot_sum_successor * S ((S (S ff_i_dot_mcp_advanced_dot_sum)) * ff_v_dot_mcp_advanced_dot_sum) + (ff_s_dot_mcp_advanced_dot_sum))) /\ ff_s_dot_mcp_advanced_dot_sum = ff_r_dot_mcp_advanced_dot_sum + ff_a_dot_mcp_advanced_dot_sum))))))))))The unchanged native kernel never receives this surface symbol. Binder-safe expansion produces only its existing first-order syntax.