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. ∀ db. ∀ dc. ∀ w. ∀ r. ∀ pb. ∀ pc. ∀ nb. ∀ nc. ∀ qb. ∀ qc. ∀ mb. ∀ mc. IntegerColumnSpan(ab,ac,db,dc,w,r,pb,pc,nb,nc) → IntegerVectorEqual(nb,nc,pb,pc,qb,qc,mb,mc,r) → IntegerColumnSpan(ab,ac,db,dc,w,r,qb,qc,mb,mc)Every linked abbreviation expands hygienically to the identical original native formula.
Definition DAG
Actual proof prerequisites
Original expanded first-order statement
forall ab ac db dc w r pb pc nb nc qb qc mb mc. (exists ics_coefficient_positive_span_negative_source ics_coefficient_positive_scale_span_negative_source ics_coefficient_negative_span_negative_source ics_coefficient_negative_scale_span_negative_source. (exists ics_raw_positive_span_negative_source_image ics_raw_positive_scale_span_negative_source_image ics_raw_negative_span_negative_source_image ics_raw_negative_scale_span_negative_source_image. (((exists ff_pp_mcp_smatrix_ics_span_negative_source_image_raw ff_pps_mcp_smatrix_ics_span_negative_source_image_raw ff_nn_mcp_smatrix_ics_span_negative_source_image_raw ff_nns_mcp_smatrix_ics_span_negative_source_image_raw ff_pn_mcp_smatrix_ics_span_negative_source_image_raw ff_pns_mcp_smatrix_ics_span_negative_source_image_raw ff_np_mcp_smatrix_ics_span_negative_source_image_raw ff_nps_mcp_smatrix_ics_span_negative_source_image_raw. ((forall ff_index_mcp_prefix_ics_span_negative_source_image_raw_pp. (exists mcp_gap_ics_span_negative_source_image_raw_pp_index. mcp_gap_ics_span_negative_source_image_raw_pp_index + S (ff_index_mcp_prefix_ics_span_negative_source_image_raw_pp) = ((r) * (1))) -> exists ff_row_mcp_prefix_ics_span_negative_source_image_raw_pp ff_column_mcp_prefix_ics_span_negative_source_image_raw_pp ff_value_mcp_prefix_ics_span_negative_source_image_raw_pp. ((ff_index_mcp_prefix_ics_span_negative_source_image_raw_pp) = (1) * ff_row_mcp_prefix_ics_span_negative_source_image_raw_pp + ff_column_mcp_prefix_ics_span_negative_source_image_raw_pp /\ ((exists mcp_gap_ics_span_negative_source_image_raw_pp_column. mcp_gap_ics_span_negative_source_image_raw_pp_column + S (ff_column_mcp_prefix_ics_span_negative_source_image_raw_pp) = (1)) /\ ((exists ff_left_mcp_cell_ics_span_negative_source_image_raw_pp_cell ff_left_scale_mcp_cell_ics_span_negative_source_image_raw_pp_cell ff_right_mcp_cell_ics_span_negative_source_image_raw_pp_cell ff_right_scale_mcp_cell_ics_span_negative_source_image_raw_pp_cell. ((forall ff_index_mcp_ics_span_negative_source_image_raw_pp_cell_row ff_source_mcp_ics_span_negative_source_image_raw_pp_cell_row ff_target_mcp_ics_span_negative_source_image_raw_pp_cell_row. (exists mcp_gap_ics_span_negative_source_image_raw_pp_cell_row_bound. mcp_gap_ics_span_negative_source_image_raw_pp_cell_row_bound + S (ff_index_mcp_ics_span_negative_source_image_raw_pp_cell_row) = (w)) -> (((exists fs_h_mcp_ics_span_negative_source_image_raw_pp_cell_row_source. fs_h_mcp_ics_span_negative_source_image_raw_pp_cell_row_source + S (ff_source_mcp_ics_span_negative_source_image_raw_pp_cell_row) = S ((S (((ff_row_mcp_prefix_ics_span_negative_source_image_raw_pp) * (w)) + (1) * ff_index_mcp_ics_span_negative_source_image_raw_pp_cell_row)) * ac)) /\ exists fs_q_mcp_ics_span_negative_source_image_raw_pp_cell_row_source. ab = fs_q_mcp_ics_span_negative_source_image_raw_pp_cell_row_source * S ((S (((ff_row_mcp_prefix_ics_span_negative_source_image_raw_pp) * (w)) + (1) * ff_index_mcp_ics_span_negative_source_image_raw_pp_cell_row)) * ac) + (ff_source_mcp_ics_span_negative_source_image_raw_pp_cell_row))) -> (((exists fs_h_mcp_ics_span_negative_source_image_raw_pp_cell_row_target. fs_h_mcp_ics_span_negative_source_image_raw_pp_cell_row_target + S (ff_target_mcp_ics_span_negative_source_image_raw_pp_cell_row) = S ((S (ff_index_mcp_ics_span_negative_source_image_raw_pp_cell_row)) * ff_left_scale_mcp_cell_ics_span_negative_source_image_raw_pp_cell)) /\ exists fs_q_mcp_ics_span_negative_source_image_raw_pp_cell_row_target. ff_left_mcp_cell_ics_span_negative_source_image_raw_pp_cell = fs_q_mcp_ics_span_negative_source_image_raw_pp_cell_row_target * S ((S (ff_index_mcp_ics_span_negative_source_image_raw_pp_cell_row)) * ff_left_scale_mcp_cell_ics_span_negative_source_image_raw_pp_cell) + (ff_target_mcp_ics_span_negative_source_image_raw_pp_cell_row))) -> ff_target_mcp_ics_span_negative_source_image_raw_pp_cell_row = ff_source_mcp_ics_span_negative_source_image_raw_pp_cell_row) /\ ((forall ff_index_mcp_ics_span_negative_source_image_raw_pp_cell_column ff_source_mcp_ics_span_negative_source_image_raw_pp_cell_column ff_target_mcp_ics_span_negative_source_image_raw_pp_cell_column. (exists mcp_gap_ics_span_negative_source_image_raw_pp_cell_column_bound. mcp_gap_ics_span_negative_source_image_raw_pp_cell_column_bound + S (ff_index_mcp_ics_span_negative_source_image_raw_pp_cell_column) = (w)) -> (((exists fs_h_mcp_ics_span_negative_source_image_raw_pp_cell_column_source. fs_h_mcp_ics_span_negative_source_image_raw_pp_cell_column_source + S (ff_source_mcp_ics_span_negative_source_image_raw_pp_cell_column) = S ((S ((ff_column_mcp_prefix_ics_span_negative_source_image_raw_pp) + (1) * ff_index_mcp_ics_span_negative_source_image_raw_pp_cell_column)) * ics_coefficient_positive_scale_span_negative_source)) /\ exists fs_q_mcp_ics_span_negative_source_image_raw_pp_cell_column_source. ics_coefficient_positive_span_negative_source = fs_q_mcp_ics_span_negative_source_image_raw_pp_cell_column_source * S ((S ((ff_column_mcp_prefix_ics_span_negative_source_image_raw_pp) + (1) * ff_index_mcp_ics_span_negative_source_image_raw_pp_cell_column)) * ics_coefficient_positive_scale_span_negative_source) + (ff_source_mcp_ics_span_negative_source_image_raw_pp_cell_column))) -> (((exists fs_h_mcp_ics_span_negative_source_image_raw_pp_cell_column_target. fs_h_mcp_ics_span_negative_source_image_raw_pp_cell_column_target + S (ff_target_mcp_ics_span_negative_source_image_raw_pp_cell_column) = S ((S (ff_index_mcp_ics_span_negative_source_image_raw_pp_cell_column)) * ff_right_scale_mcp_cell_ics_span_negative_source_image_raw_pp_cell)) /\ exists fs_q_mcp_ics_span_negative_source_image_raw_pp_cell_column_target. ff_right_mcp_cell_ics_span_negative_source_image_raw_pp_cell = fs_q_mcp_ics_span_negative_source_image_raw_pp_cell_column_target * S ((S (ff_index_mcp_ics_span_negative_source_image_raw_pp_cell_column)) * ff_right_scale_mcp_cell_ics_span_negative_source_image_raw_pp_cell) + (ff_target_mcp_ics_span_negative_source_image_raw_pp_cell_column))) -> ff_target_mcp_ics_span_negative_source_image_raw_pp_cell_column = ff_source_mcp_ics_span_negative_source_image_raw_pp_cell_column) /\ (exists ff_code_dot_mcp_ics_span_negative_source_image_raw_pp_cell_dot ff_scale_dot_mcp_ics_span_negative_source_image_raw_pp_cell_dot. ((forall fpmp_index_dot_mcp_ics_span_negative_source_image_raw_pp_cell_dot_pointwise fpmp_left_dot_mcp_ics_span_negative_source_image_raw_pp_cell_dot_pointwise fpmp_right_dot_mcp_ics_span_negative_source_image_raw_pp_cell_dot_pointwise fpmp_target_dot_mcp_ics_span_negative_source_image_raw_pp_cell_dot_pointwise. (exists fpmp_gap_dot_mcp_ics_span_negative_source_image_raw_pp_cell_dot_pointwise. fpmp_gap_dot_mcp_ics_span_negative_source_image_raw_pp_cell_dot_pointwise + S fpmp_index_dot_mcp_ics_span_negative_source_image_raw_pp_cell_dot_pointwise = w) -> (((exists ff_h_fpmp_dot_mcp_ics_span_negative_source_image_raw_pp_cell_dot_pointwise_left. ff_h_fpmp_dot_mcp_ics_span_negative_source_image_raw_pp_cell_dot_pointwise_left + S (fpmp_left_dot_mcp_ics_span_negative_source_image_raw_pp_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_span_negative_source_image_raw_pp_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_span_negative_source_image_raw_pp_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_span_negative_source_image_raw_pp_cell_dot_pointwise_left. ff_left_mcp_cell_ics_span_negative_source_image_raw_pp_cell = ff_q_fpmp_dot_mcp_ics_span_negative_source_image_raw_pp_cell_dot_pointwise_left * S ((S (fpmp_index_dot_mcp_ics_span_negative_source_image_raw_pp_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_span_negative_source_image_raw_pp_cell) + (fpmp_left_dot_mcp_ics_span_negative_source_image_raw_pp_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_span_negative_source_image_raw_pp_cell_dot_pointwise_right. ff_h_fpmp_dot_mcp_ics_span_negative_source_image_raw_pp_cell_dot_pointwise_right + S (fpmp_right_dot_mcp_ics_span_negative_source_image_raw_pp_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_span_negative_source_image_raw_pp_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_span_negative_source_image_raw_pp_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_span_negative_source_image_raw_pp_cell_dot_pointwise_right. ff_right_mcp_cell_ics_span_negative_source_image_raw_pp_cell = ff_q_fpmp_dot_mcp_ics_span_negative_source_image_raw_pp_cell_dot_pointwise_right * S ((S (fpmp_index_dot_mcp_ics_span_negative_source_image_raw_pp_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_span_negative_source_image_raw_pp_cell) + (fpmp_right_dot_mcp_ics_span_negative_source_image_raw_pp_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_span_negative_source_image_raw_pp_cell_dot_pointwise_target. ff_h_fpmp_dot_mcp_ics_span_negative_source_image_raw_pp_cell_dot_pointwise_target + S (fpmp_target_dot_mcp_ics_span_negative_source_image_raw_pp_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_span_negative_source_image_raw_pp_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_span_negative_source_image_raw_pp_cell_dot)) /\ exists ff_q_fpmp_dot_mcp_ics_span_negative_source_image_raw_pp_cell_dot_pointwise_target. ff_code_dot_mcp_ics_span_negative_source_image_raw_pp_cell_dot = ff_q_fpmp_dot_mcp_ics_span_negative_source_image_raw_pp_cell_dot_pointwise_target * S ((S (fpmp_index_dot_mcp_ics_span_negative_source_image_raw_pp_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_span_negative_source_image_raw_pp_cell_dot) + (fpmp_target_dot_mcp_ics_span_negative_source_image_raw_pp_cell_dot_pointwise))) -> fpmp_target_dot_mcp_ics_span_negative_source_image_raw_pp_cell_dot_pointwise = fpmp_left_dot_mcp_ics_span_negative_source_image_raw_pp_cell_dot_pointwise * fpmp_right_dot_mcp_ics_span_negative_source_image_raw_pp_cell_dot_pointwise) /\ (exists ff_u_dot_mcp_ics_span_negative_source_image_raw_pp_cell_dot_sum ff_v_dot_mcp_ics_span_negative_source_image_raw_pp_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_span_negative_source_image_raw_pp_cell_dot_sum_start. ff_h_dot_mcp_ics_span_negative_source_image_raw_pp_cell_dot_sum_start + S (0) = S ((S (0)) * ff_v_dot_mcp_ics_span_negative_source_image_raw_pp_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_span_negative_source_image_raw_pp_cell_dot_sum_start. ff_u_dot_mcp_ics_span_negative_source_image_raw_pp_cell_dot_sum = ff_q_dot_mcp_ics_span_negative_source_image_raw_pp_cell_dot_sum_start * S ((S (0)) * ff_v_dot_mcp_ics_span_negative_source_image_raw_pp_cell_dot_sum) + (0))) /\ ((((exists ff_h_dot_mcp_ics_span_negative_source_image_raw_pp_cell_dot_sum_terminal. ff_h_dot_mcp_ics_span_negative_source_image_raw_pp_cell_dot_sum_terminal + S (ff_value_mcp_prefix_ics_span_negative_source_image_raw_pp) = S ((S (w)) * ff_v_dot_mcp_ics_span_negative_source_image_raw_pp_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_span_negative_source_image_raw_pp_cell_dot_sum_terminal. ff_u_dot_mcp_ics_span_negative_source_image_raw_pp_cell_dot_sum = ff_q_dot_mcp_ics_span_negative_source_image_raw_pp_cell_dot_sum_terminal * S ((S (w)) * ff_v_dot_mcp_ics_span_negative_source_image_raw_pp_cell_dot_sum) + (ff_value_mcp_prefix_ics_span_negative_source_image_raw_pp))) /\ forall ff_i_dot_mcp_ics_span_negative_source_image_raw_pp_cell_dot_sum. (exists ff_lt_dot_mcp_ics_span_negative_source_image_raw_pp_cell_dot_sum_bound. ff_lt_dot_mcp_ics_span_negative_source_image_raw_pp_cell_dot_sum_bound + S ff_i_dot_mcp_ics_span_negative_source_image_raw_pp_cell_dot_sum = w) -> exists ff_a_dot_mcp_ics_span_negative_source_image_raw_pp_cell_dot_sum ff_r_dot_mcp_ics_span_negative_source_image_raw_pp_cell_dot_sum ff_s_dot_mcp_ics_span_negative_source_image_raw_pp_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_span_negative_source_image_raw_pp_cell_dot_sum_summand. ff_h_dot_mcp_ics_span_negative_source_image_raw_pp_cell_dot_sum_summand + S (ff_a_dot_mcp_ics_span_negative_source_image_raw_pp_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_span_negative_source_image_raw_pp_cell_dot_sum)) * ff_scale_dot_mcp_ics_span_negative_source_image_raw_pp_cell_dot)) /\ exists ff_q_dot_mcp_ics_span_negative_source_image_raw_pp_cell_dot_sum_summand. ff_code_dot_mcp_ics_span_negative_source_image_raw_pp_cell_dot = ff_q_dot_mcp_ics_span_negative_source_image_raw_pp_cell_dot_sum_summand * S ((S (ff_i_dot_mcp_ics_span_negative_source_image_raw_pp_cell_dot_sum)) * ff_scale_dot_mcp_ics_span_negative_source_image_raw_pp_cell_dot) + (ff_a_dot_mcp_ics_span_negative_source_image_raw_pp_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_span_negative_source_image_raw_pp_cell_dot_sum_partial. ff_h_dot_mcp_ics_span_negative_source_image_raw_pp_cell_dot_sum_partial + S (ff_r_dot_mcp_ics_span_negative_source_image_raw_pp_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_span_negative_source_image_raw_pp_cell_dot_sum)) * ff_v_dot_mcp_ics_span_negative_source_image_raw_pp_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_span_negative_source_image_raw_pp_cell_dot_sum_partial. ff_u_dot_mcp_ics_span_negative_source_image_raw_pp_cell_dot_sum = ff_q_dot_mcp_ics_span_negative_source_image_raw_pp_cell_dot_sum_partial * S ((S (ff_i_dot_mcp_ics_span_negative_source_image_raw_pp_cell_dot_sum)) * ff_v_dot_mcp_ics_span_negative_source_image_raw_pp_cell_dot_sum) + (ff_r_dot_mcp_ics_span_negative_source_image_raw_pp_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_span_negative_source_image_raw_pp_cell_dot_sum_successor. ff_h_dot_mcp_ics_span_negative_source_image_raw_pp_cell_dot_sum_successor + S (ff_s_dot_mcp_ics_span_negative_source_image_raw_pp_cell_dot_sum) = S ((S (S ff_i_dot_mcp_ics_span_negative_source_image_raw_pp_cell_dot_sum)) * ff_v_dot_mcp_ics_span_negative_source_image_raw_pp_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_span_negative_source_image_raw_pp_cell_dot_sum_successor. ff_u_dot_mcp_ics_span_negative_source_image_raw_pp_cell_dot_sum = ff_q_dot_mcp_ics_span_negative_source_image_raw_pp_cell_dot_sum_successor * S ((S (S ff_i_dot_mcp_ics_span_negative_source_image_raw_pp_cell_dot_sum)) * ff_v_dot_mcp_ics_span_negative_source_image_raw_pp_cell_dot_sum) + (ff_s_dot_mcp_ics_span_negative_source_image_raw_pp_cell_dot_sum))) /\ ff_s_dot_mcp_ics_span_negative_source_image_raw_pp_cell_dot_sum = ff_r_dot_mcp_ics_span_negative_source_image_raw_pp_cell_dot_sum + ff_a_dot_mcp_ics_span_negative_source_image_raw_pp_cell_dot_sum))))))))))) /\ (((exists fs_h_mcp_ics_span_negative_source_image_raw_pp_entry. fs_h_mcp_ics_span_negative_source_image_raw_pp_entry + S (ff_value_mcp_prefix_ics_span_negative_source_image_raw_pp) = S ((S (ff_index_mcp_prefix_ics_span_negative_source_image_raw_pp)) * ff_pps_mcp_smatrix_ics_span_negative_source_image_raw)) /\ exists fs_q_mcp_ics_span_negative_source_image_raw_pp_entry. ff_pp_mcp_smatrix_ics_span_negative_source_image_raw = fs_q_mcp_ics_span_negative_source_image_raw_pp_entry * S ((S (ff_index_mcp_prefix_ics_span_negative_source_image_raw_pp)) * ff_pps_mcp_smatrix_ics_span_negative_source_image_raw) + (ff_value_mcp_prefix_ics_span_negative_source_image_raw_pp))))))) /\ ((forall ff_index_mcp_prefix_ics_span_negative_source_image_raw_nn. (exists mcp_gap_ics_span_negative_source_image_raw_nn_index. mcp_gap_ics_span_negative_source_image_raw_nn_index + S (ff_index_mcp_prefix_ics_span_negative_source_image_raw_nn) = ((r) * (1))) -> exists ff_row_mcp_prefix_ics_span_negative_source_image_raw_nn ff_column_mcp_prefix_ics_span_negative_source_image_raw_nn ff_value_mcp_prefix_ics_span_negative_source_image_raw_nn. ((ff_index_mcp_prefix_ics_span_negative_source_image_raw_nn) = (1) * ff_row_mcp_prefix_ics_span_negative_source_image_raw_nn + ff_column_mcp_prefix_ics_span_negative_source_image_raw_nn /\ ((exists mcp_gap_ics_span_negative_source_image_raw_nn_column. mcp_gap_ics_span_negative_source_image_raw_nn_column + S (ff_column_mcp_prefix_ics_span_negative_source_image_raw_nn) = (1)) /\ ((exists ff_left_mcp_cell_ics_span_negative_source_image_raw_nn_cell ff_left_scale_mcp_cell_ics_span_negative_source_image_raw_nn_cell ff_right_mcp_cell_ics_span_negative_source_image_raw_nn_cell ff_right_scale_mcp_cell_ics_span_negative_source_image_raw_nn_cell. ((forall ff_index_mcp_ics_span_negative_source_image_raw_nn_cell_row ff_source_mcp_ics_span_negative_source_image_raw_nn_cell_row ff_target_mcp_ics_span_negative_source_image_raw_nn_cell_row. (exists mcp_gap_ics_span_negative_source_image_raw_nn_cell_row_bound. mcp_gap_ics_span_negative_source_image_raw_nn_cell_row_bound + S (ff_index_mcp_ics_span_negative_source_image_raw_nn_cell_row) = (w)) -> (((exists fs_h_mcp_ics_span_negative_source_image_raw_nn_cell_row_source. fs_h_mcp_ics_span_negative_source_image_raw_nn_cell_row_source + S (ff_source_mcp_ics_span_negative_source_image_raw_nn_cell_row) = S ((S (((ff_row_mcp_prefix_ics_span_negative_source_image_raw_nn) * (w)) + (1) * ff_index_mcp_ics_span_negative_source_image_raw_nn_cell_row)) * dc)) /\ exists fs_q_mcp_ics_span_negative_source_image_raw_nn_cell_row_source. db = fs_q_mcp_ics_span_negative_source_image_raw_nn_cell_row_source * S ((S (((ff_row_mcp_prefix_ics_span_negative_source_image_raw_nn) * (w)) + (1) * ff_index_mcp_ics_span_negative_source_image_raw_nn_cell_row)) * dc) + (ff_source_mcp_ics_span_negative_source_image_raw_nn_cell_row))) -> (((exists fs_h_mcp_ics_span_negative_source_image_raw_nn_cell_row_target. fs_h_mcp_ics_span_negative_source_image_raw_nn_cell_row_target + S (ff_target_mcp_ics_span_negative_source_image_raw_nn_cell_row) = S ((S (ff_index_mcp_ics_span_negative_source_image_raw_nn_cell_row)) * ff_left_scale_mcp_cell_ics_span_negative_source_image_raw_nn_cell)) /\ exists fs_q_mcp_ics_span_negative_source_image_raw_nn_cell_row_target. ff_left_mcp_cell_ics_span_negative_source_image_raw_nn_cell = fs_q_mcp_ics_span_negative_source_image_raw_nn_cell_row_target * S ((S (ff_index_mcp_ics_span_negative_source_image_raw_nn_cell_row)) * ff_left_scale_mcp_cell_ics_span_negative_source_image_raw_nn_cell) + (ff_target_mcp_ics_span_negative_source_image_raw_nn_cell_row))) -> ff_target_mcp_ics_span_negative_source_image_raw_nn_cell_row = ff_source_mcp_ics_span_negative_source_image_raw_nn_cell_row) /\ ((forall ff_index_mcp_ics_span_negative_source_image_raw_nn_cell_column ff_source_mcp_ics_span_negative_source_image_raw_nn_cell_column ff_target_mcp_ics_span_negative_source_image_raw_nn_cell_column. (exists mcp_gap_ics_span_negative_source_image_raw_nn_cell_column_bound. mcp_gap_ics_span_negative_source_image_raw_nn_cell_column_bound + S (ff_index_mcp_ics_span_negative_source_image_raw_nn_cell_column) = (w)) -> (((exists fs_h_mcp_ics_span_negative_source_image_raw_nn_cell_column_source. fs_h_mcp_ics_span_negative_source_image_raw_nn_cell_column_source + S (ff_source_mcp_ics_span_negative_source_image_raw_nn_cell_column) = S ((S ((ff_column_mcp_prefix_ics_span_negative_source_image_raw_nn) + (1) * ff_index_mcp_ics_span_negative_source_image_raw_nn_cell_column)) * ics_coefficient_negative_scale_span_negative_source)) /\ exists fs_q_mcp_ics_span_negative_source_image_raw_nn_cell_column_source. ics_coefficient_negative_span_negative_source = fs_q_mcp_ics_span_negative_source_image_raw_nn_cell_column_source * S ((S ((ff_column_mcp_prefix_ics_span_negative_source_image_raw_nn) + (1) * ff_index_mcp_ics_span_negative_source_image_raw_nn_cell_column)) * ics_coefficient_negative_scale_span_negative_source) + (ff_source_mcp_ics_span_negative_source_image_raw_nn_cell_column))) -> (((exists fs_h_mcp_ics_span_negative_source_image_raw_nn_cell_column_target. fs_h_mcp_ics_span_negative_source_image_raw_nn_cell_column_target + S (ff_target_mcp_ics_span_negative_source_image_raw_nn_cell_column) = S ((S (ff_index_mcp_ics_span_negative_source_image_raw_nn_cell_column)) * ff_right_scale_mcp_cell_ics_span_negative_source_image_raw_nn_cell)) /\ exists fs_q_mcp_ics_span_negative_source_image_raw_nn_cell_column_target. ff_right_mcp_cell_ics_span_negative_source_image_raw_nn_cell = fs_q_mcp_ics_span_negative_source_image_raw_nn_cell_column_target * S ((S (ff_index_mcp_ics_span_negative_source_image_raw_nn_cell_column)) * ff_right_scale_mcp_cell_ics_span_negative_source_image_raw_nn_cell) + (ff_target_mcp_ics_span_negative_source_image_raw_nn_cell_column))) -> ff_target_mcp_ics_span_negative_source_image_raw_nn_cell_column = ff_source_mcp_ics_span_negative_source_image_raw_nn_cell_column) /\ (exists ff_code_dot_mcp_ics_span_negative_source_image_raw_nn_cell_dot ff_scale_dot_mcp_ics_span_negative_source_image_raw_nn_cell_dot. ((forall fpmp_index_dot_mcp_ics_span_negative_source_image_raw_nn_cell_dot_pointwise fpmp_left_dot_mcp_ics_span_negative_source_image_raw_nn_cell_dot_pointwise fpmp_right_dot_mcp_ics_span_negative_source_image_raw_nn_cell_dot_pointwise fpmp_target_dot_mcp_ics_span_negative_source_image_raw_nn_cell_dot_pointwise. (exists fpmp_gap_dot_mcp_ics_span_negative_source_image_raw_nn_cell_dot_pointwise. fpmp_gap_dot_mcp_ics_span_negative_source_image_raw_nn_cell_dot_pointwise + S fpmp_index_dot_mcp_ics_span_negative_source_image_raw_nn_cell_dot_pointwise = w) -> (((exists ff_h_fpmp_dot_mcp_ics_span_negative_source_image_raw_nn_cell_dot_pointwise_left. ff_h_fpmp_dot_mcp_ics_span_negative_source_image_raw_nn_cell_dot_pointwise_left + S (fpmp_left_dot_mcp_ics_span_negative_source_image_raw_nn_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_span_negative_source_image_raw_nn_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_span_negative_source_image_raw_nn_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_span_negative_source_image_raw_nn_cell_dot_pointwise_left. ff_left_mcp_cell_ics_span_negative_source_image_raw_nn_cell = ff_q_fpmp_dot_mcp_ics_span_negative_source_image_raw_nn_cell_dot_pointwise_left * S ((S (fpmp_index_dot_mcp_ics_span_negative_source_image_raw_nn_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_span_negative_source_image_raw_nn_cell) + (fpmp_left_dot_mcp_ics_span_negative_source_image_raw_nn_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_span_negative_source_image_raw_nn_cell_dot_pointwise_right. ff_h_fpmp_dot_mcp_ics_span_negative_source_image_raw_nn_cell_dot_pointwise_right + S (fpmp_right_dot_mcp_ics_span_negative_source_image_raw_nn_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_span_negative_source_image_raw_nn_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_span_negative_source_image_raw_nn_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_span_negative_source_image_raw_nn_cell_dot_pointwise_right. ff_right_mcp_cell_ics_span_negative_source_image_raw_nn_cell = ff_q_fpmp_dot_mcp_ics_span_negative_source_image_raw_nn_cell_dot_pointwise_right * S ((S (fpmp_index_dot_mcp_ics_span_negative_source_image_raw_nn_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_span_negative_source_image_raw_nn_cell) + (fpmp_right_dot_mcp_ics_span_negative_source_image_raw_nn_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_span_negative_source_image_raw_nn_cell_dot_pointwise_target. ff_h_fpmp_dot_mcp_ics_span_negative_source_image_raw_nn_cell_dot_pointwise_target + S (fpmp_target_dot_mcp_ics_span_negative_source_image_raw_nn_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_span_negative_source_image_raw_nn_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_span_negative_source_image_raw_nn_cell_dot)) /\ exists ff_q_fpmp_dot_mcp_ics_span_negative_source_image_raw_nn_cell_dot_pointwise_target. ff_code_dot_mcp_ics_span_negative_source_image_raw_nn_cell_dot = ff_q_fpmp_dot_mcp_ics_span_negative_source_image_raw_nn_cell_dot_pointwise_target * S ((S (fpmp_index_dot_mcp_ics_span_negative_source_image_raw_nn_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_span_negative_source_image_raw_nn_cell_dot) + (fpmp_target_dot_mcp_ics_span_negative_source_image_raw_nn_cell_dot_pointwise))) -> fpmp_target_dot_mcp_ics_span_negative_source_image_raw_nn_cell_dot_pointwise = fpmp_left_dot_mcp_ics_span_negative_source_image_raw_nn_cell_dot_pointwise * fpmp_right_dot_mcp_ics_span_negative_source_image_raw_nn_cell_dot_pointwise) /\ (exists ff_u_dot_mcp_ics_span_negative_source_image_raw_nn_cell_dot_sum ff_v_dot_mcp_ics_span_negative_source_image_raw_nn_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_span_negative_source_image_raw_nn_cell_dot_sum_start. ff_h_dot_mcp_ics_span_negative_source_image_raw_nn_cell_dot_sum_start + S (0) = S ((S (0)) * ff_v_dot_mcp_ics_span_negative_source_image_raw_nn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_span_negative_source_image_raw_nn_cell_dot_sum_start. ff_u_dot_mcp_ics_span_negative_source_image_raw_nn_cell_dot_sum = ff_q_dot_mcp_ics_span_negative_source_image_raw_nn_cell_dot_sum_start * S ((S (0)) * ff_v_dot_mcp_ics_span_negative_source_image_raw_nn_cell_dot_sum) + (0))) /\ ((((exists ff_h_dot_mcp_ics_span_negative_source_image_raw_nn_cell_dot_sum_terminal. ff_h_dot_mcp_ics_span_negative_source_image_raw_nn_cell_dot_sum_terminal + S (ff_value_mcp_prefix_ics_span_negative_source_image_raw_nn) = S ((S (w)) * ff_v_dot_mcp_ics_span_negative_source_image_raw_nn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_span_negative_source_image_raw_nn_cell_dot_sum_terminal. ff_u_dot_mcp_ics_span_negative_source_image_raw_nn_cell_dot_sum = ff_q_dot_mcp_ics_span_negative_source_image_raw_nn_cell_dot_sum_terminal * S ((S (w)) * ff_v_dot_mcp_ics_span_negative_source_image_raw_nn_cell_dot_sum) + (ff_value_mcp_prefix_ics_span_negative_source_image_raw_nn))) /\ forall ff_i_dot_mcp_ics_span_negative_source_image_raw_nn_cell_dot_sum. (exists ff_lt_dot_mcp_ics_span_negative_source_image_raw_nn_cell_dot_sum_bound. ff_lt_dot_mcp_ics_span_negative_source_image_raw_nn_cell_dot_sum_bound + S ff_i_dot_mcp_ics_span_negative_source_image_raw_nn_cell_dot_sum = w) -> exists ff_a_dot_mcp_ics_span_negative_source_image_raw_nn_cell_dot_sum ff_r_dot_mcp_ics_span_negative_source_image_raw_nn_cell_dot_sum ff_s_dot_mcp_ics_span_negative_source_image_raw_nn_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_span_negative_source_image_raw_nn_cell_dot_sum_summand. ff_h_dot_mcp_ics_span_negative_source_image_raw_nn_cell_dot_sum_summand + S (ff_a_dot_mcp_ics_span_negative_source_image_raw_nn_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_span_negative_source_image_raw_nn_cell_dot_sum)) * ff_scale_dot_mcp_ics_span_negative_source_image_raw_nn_cell_dot)) /\ exists ff_q_dot_mcp_ics_span_negative_source_image_raw_nn_cell_dot_sum_summand. ff_code_dot_mcp_ics_span_negative_source_image_raw_nn_cell_dot = ff_q_dot_mcp_ics_span_negative_source_image_raw_nn_cell_dot_sum_summand * S ((S (ff_i_dot_mcp_ics_span_negative_source_image_raw_nn_cell_dot_sum)) * ff_scale_dot_mcp_ics_span_negative_source_image_raw_nn_cell_dot) + (ff_a_dot_mcp_ics_span_negative_source_image_raw_nn_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_span_negative_source_image_raw_nn_cell_dot_sum_partial. ff_h_dot_mcp_ics_span_negative_source_image_raw_nn_cell_dot_sum_partial + S (ff_r_dot_mcp_ics_span_negative_source_image_raw_nn_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_span_negative_source_image_raw_nn_cell_dot_sum)) * ff_v_dot_mcp_ics_span_negative_source_image_raw_nn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_span_negative_source_image_raw_nn_cell_dot_sum_partial. ff_u_dot_mcp_ics_span_negative_source_image_raw_nn_cell_dot_sum = ff_q_dot_mcp_ics_span_negative_source_image_raw_nn_cell_dot_sum_partial * S ((S (ff_i_dot_mcp_ics_span_negative_source_image_raw_nn_cell_dot_sum)) * ff_v_dot_mcp_ics_span_negative_source_image_raw_nn_cell_dot_sum) + (ff_r_dot_mcp_ics_span_negative_source_image_raw_nn_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_span_negative_source_image_raw_nn_cell_dot_sum_successor. ff_h_dot_mcp_ics_span_negative_source_image_raw_nn_cell_dot_sum_successor + S (ff_s_dot_mcp_ics_span_negative_source_image_raw_nn_cell_dot_sum) = S ((S (S ff_i_dot_mcp_ics_span_negative_source_image_raw_nn_cell_dot_sum)) * ff_v_dot_mcp_ics_span_negative_source_image_raw_nn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_span_negative_source_image_raw_nn_cell_dot_sum_successor. ff_u_dot_mcp_ics_span_negative_source_image_raw_nn_cell_dot_sum = ff_q_dot_mcp_ics_span_negative_source_image_raw_nn_cell_dot_sum_successor * S ((S (S ff_i_dot_mcp_ics_span_negative_source_image_raw_nn_cell_dot_sum)) * ff_v_dot_mcp_ics_span_negative_source_image_raw_nn_cell_dot_sum) + (ff_s_dot_mcp_ics_span_negative_source_image_raw_nn_cell_dot_sum))) /\ ff_s_dot_mcp_ics_span_negative_source_image_raw_nn_cell_dot_sum = ff_r_dot_mcp_ics_span_negative_source_image_raw_nn_cell_dot_sum + ff_a_dot_mcp_ics_span_negative_source_image_raw_nn_cell_dot_sum))))))))))) /\ (((exists fs_h_mcp_ics_span_negative_source_image_raw_nn_entry. fs_h_mcp_ics_span_negative_source_image_raw_nn_entry + S (ff_value_mcp_prefix_ics_span_negative_source_image_raw_nn) = S ((S (ff_index_mcp_prefix_ics_span_negative_source_image_raw_nn)) * ff_nns_mcp_smatrix_ics_span_negative_source_image_raw)) /\ exists fs_q_mcp_ics_span_negative_source_image_raw_nn_entry. ff_nn_mcp_smatrix_ics_span_negative_source_image_raw = fs_q_mcp_ics_span_negative_source_image_raw_nn_entry * S ((S (ff_index_mcp_prefix_ics_span_negative_source_image_raw_nn)) * ff_nns_mcp_smatrix_ics_span_negative_source_image_raw) + (ff_value_mcp_prefix_ics_span_negative_source_image_raw_nn))))))) /\ ((forall ff_index_mcp_prefix_ics_span_negative_source_image_raw_pn. (exists mcp_gap_ics_span_negative_source_image_raw_pn_index. mcp_gap_ics_span_negative_source_image_raw_pn_index + S (ff_index_mcp_prefix_ics_span_negative_source_image_raw_pn) = ((r) * (1))) -> exists ff_row_mcp_prefix_ics_span_negative_source_image_raw_pn ff_column_mcp_prefix_ics_span_negative_source_image_raw_pn ff_value_mcp_prefix_ics_span_negative_source_image_raw_pn. ((ff_index_mcp_prefix_ics_span_negative_source_image_raw_pn) = (1) * ff_row_mcp_prefix_ics_span_negative_source_image_raw_pn + ff_column_mcp_prefix_ics_span_negative_source_image_raw_pn /\ ((exists mcp_gap_ics_span_negative_source_image_raw_pn_column. mcp_gap_ics_span_negative_source_image_raw_pn_column + S (ff_column_mcp_prefix_ics_span_negative_source_image_raw_pn) = (1)) /\ ((exists ff_left_mcp_cell_ics_span_negative_source_image_raw_pn_cell ff_left_scale_mcp_cell_ics_span_negative_source_image_raw_pn_cell ff_right_mcp_cell_ics_span_negative_source_image_raw_pn_cell ff_right_scale_mcp_cell_ics_span_negative_source_image_raw_pn_cell. ((forall ff_index_mcp_ics_span_negative_source_image_raw_pn_cell_row ff_source_mcp_ics_span_negative_source_image_raw_pn_cell_row ff_target_mcp_ics_span_negative_source_image_raw_pn_cell_row. (exists mcp_gap_ics_span_negative_source_image_raw_pn_cell_row_bound. mcp_gap_ics_span_negative_source_image_raw_pn_cell_row_bound + S (ff_index_mcp_ics_span_negative_source_image_raw_pn_cell_row) = (w)) -> (((exists fs_h_mcp_ics_span_negative_source_image_raw_pn_cell_row_source. fs_h_mcp_ics_span_negative_source_image_raw_pn_cell_row_source + S (ff_source_mcp_ics_span_negative_source_image_raw_pn_cell_row) = S ((S (((ff_row_mcp_prefix_ics_span_negative_source_image_raw_pn) * (w)) + (1) * ff_index_mcp_ics_span_negative_source_image_raw_pn_cell_row)) * ac)) /\ exists fs_q_mcp_ics_span_negative_source_image_raw_pn_cell_row_source. ab = fs_q_mcp_ics_span_negative_source_image_raw_pn_cell_row_source * S ((S (((ff_row_mcp_prefix_ics_span_negative_source_image_raw_pn) * (w)) + (1) * ff_index_mcp_ics_span_negative_source_image_raw_pn_cell_row)) * ac) + (ff_source_mcp_ics_span_negative_source_image_raw_pn_cell_row))) -> (((exists fs_h_mcp_ics_span_negative_source_image_raw_pn_cell_row_target. fs_h_mcp_ics_span_negative_source_image_raw_pn_cell_row_target + S (ff_target_mcp_ics_span_negative_source_image_raw_pn_cell_row) = S ((S (ff_index_mcp_ics_span_negative_source_image_raw_pn_cell_row)) * ff_left_scale_mcp_cell_ics_span_negative_source_image_raw_pn_cell)) /\ exists fs_q_mcp_ics_span_negative_source_image_raw_pn_cell_row_target. ff_left_mcp_cell_ics_span_negative_source_image_raw_pn_cell = fs_q_mcp_ics_span_negative_source_image_raw_pn_cell_row_target * S ((S (ff_index_mcp_ics_span_negative_source_image_raw_pn_cell_row)) * ff_left_scale_mcp_cell_ics_span_negative_source_image_raw_pn_cell) + (ff_target_mcp_ics_span_negative_source_image_raw_pn_cell_row))) -> ff_target_mcp_ics_span_negative_source_image_raw_pn_cell_row = ff_source_mcp_ics_span_negative_source_image_raw_pn_cell_row) /\ ((forall ff_index_mcp_ics_span_negative_source_image_raw_pn_cell_column ff_source_mcp_ics_span_negative_source_image_raw_pn_cell_column ff_target_mcp_ics_span_negative_source_image_raw_pn_cell_column. (exists mcp_gap_ics_span_negative_source_image_raw_pn_cell_column_bound. mcp_gap_ics_span_negative_source_image_raw_pn_cell_column_bound + S (ff_index_mcp_ics_span_negative_source_image_raw_pn_cell_column) = (w)) -> (((exists fs_h_mcp_ics_span_negative_source_image_raw_pn_cell_column_source. fs_h_mcp_ics_span_negative_source_image_raw_pn_cell_column_source + S (ff_source_mcp_ics_span_negative_source_image_raw_pn_cell_column) = S ((S ((ff_column_mcp_prefix_ics_span_negative_source_image_raw_pn) + (1) * ff_index_mcp_ics_span_negative_source_image_raw_pn_cell_column)) * ics_coefficient_negative_scale_span_negative_source)) /\ exists fs_q_mcp_ics_span_negative_source_image_raw_pn_cell_column_source. ics_coefficient_negative_span_negative_source = fs_q_mcp_ics_span_negative_source_image_raw_pn_cell_column_source * S ((S ((ff_column_mcp_prefix_ics_span_negative_source_image_raw_pn) + (1) * ff_index_mcp_ics_span_negative_source_image_raw_pn_cell_column)) * ics_coefficient_negative_scale_span_negative_source) + (ff_source_mcp_ics_span_negative_source_image_raw_pn_cell_column))) -> (((exists fs_h_mcp_ics_span_negative_source_image_raw_pn_cell_column_target. fs_h_mcp_ics_span_negative_source_image_raw_pn_cell_column_target + S (ff_target_mcp_ics_span_negative_source_image_raw_pn_cell_column) = S ((S (ff_index_mcp_ics_span_negative_source_image_raw_pn_cell_column)) * ff_right_scale_mcp_cell_ics_span_negative_source_image_raw_pn_cell)) /\ exists fs_q_mcp_ics_span_negative_source_image_raw_pn_cell_column_target. ff_right_mcp_cell_ics_span_negative_source_image_raw_pn_cell = fs_q_mcp_ics_span_negative_source_image_raw_pn_cell_column_target * S ((S (ff_index_mcp_ics_span_negative_source_image_raw_pn_cell_column)) * ff_right_scale_mcp_cell_ics_span_negative_source_image_raw_pn_cell) + (ff_target_mcp_ics_span_negative_source_image_raw_pn_cell_column))) -> ff_target_mcp_ics_span_negative_source_image_raw_pn_cell_column = ff_source_mcp_ics_span_negative_source_image_raw_pn_cell_column) /\ (exists ff_code_dot_mcp_ics_span_negative_source_image_raw_pn_cell_dot ff_scale_dot_mcp_ics_span_negative_source_image_raw_pn_cell_dot. ((forall fpmp_index_dot_mcp_ics_span_negative_source_image_raw_pn_cell_dot_pointwise fpmp_left_dot_mcp_ics_span_negative_source_image_raw_pn_cell_dot_pointwise fpmp_right_dot_mcp_ics_span_negative_source_image_raw_pn_cell_dot_pointwise fpmp_target_dot_mcp_ics_span_negative_source_image_raw_pn_cell_dot_pointwise. (exists fpmp_gap_dot_mcp_ics_span_negative_source_image_raw_pn_cell_dot_pointwise. fpmp_gap_dot_mcp_ics_span_negative_source_image_raw_pn_cell_dot_pointwise + S fpmp_index_dot_mcp_ics_span_negative_source_image_raw_pn_cell_dot_pointwise = w) -> (((exists ff_h_fpmp_dot_mcp_ics_span_negative_source_image_raw_pn_cell_dot_pointwise_left. ff_h_fpmp_dot_mcp_ics_span_negative_source_image_raw_pn_cell_dot_pointwise_left + S (fpmp_left_dot_mcp_ics_span_negative_source_image_raw_pn_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_span_negative_source_image_raw_pn_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_span_negative_source_image_raw_pn_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_span_negative_source_image_raw_pn_cell_dot_pointwise_left. ff_left_mcp_cell_ics_span_negative_source_image_raw_pn_cell = ff_q_fpmp_dot_mcp_ics_span_negative_source_image_raw_pn_cell_dot_pointwise_left * S ((S (fpmp_index_dot_mcp_ics_span_negative_source_image_raw_pn_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_span_negative_source_image_raw_pn_cell) + (fpmp_left_dot_mcp_ics_span_negative_source_image_raw_pn_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_span_negative_source_image_raw_pn_cell_dot_pointwise_right. ff_h_fpmp_dot_mcp_ics_span_negative_source_image_raw_pn_cell_dot_pointwise_right + S (fpmp_right_dot_mcp_ics_span_negative_source_image_raw_pn_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_span_negative_source_image_raw_pn_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_span_negative_source_image_raw_pn_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_span_negative_source_image_raw_pn_cell_dot_pointwise_right. ff_right_mcp_cell_ics_span_negative_source_image_raw_pn_cell = ff_q_fpmp_dot_mcp_ics_span_negative_source_image_raw_pn_cell_dot_pointwise_right * S ((S (fpmp_index_dot_mcp_ics_span_negative_source_image_raw_pn_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_span_negative_source_image_raw_pn_cell) + (fpmp_right_dot_mcp_ics_span_negative_source_image_raw_pn_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_span_negative_source_image_raw_pn_cell_dot_pointwise_target. ff_h_fpmp_dot_mcp_ics_span_negative_source_image_raw_pn_cell_dot_pointwise_target + S (fpmp_target_dot_mcp_ics_span_negative_source_image_raw_pn_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_span_negative_source_image_raw_pn_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_span_negative_source_image_raw_pn_cell_dot)) /\ exists ff_q_fpmp_dot_mcp_ics_span_negative_source_image_raw_pn_cell_dot_pointwise_target. ff_code_dot_mcp_ics_span_negative_source_image_raw_pn_cell_dot = ff_q_fpmp_dot_mcp_ics_span_negative_source_image_raw_pn_cell_dot_pointwise_target * S ((S (fpmp_index_dot_mcp_ics_span_negative_source_image_raw_pn_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_span_negative_source_image_raw_pn_cell_dot) + (fpmp_target_dot_mcp_ics_span_negative_source_image_raw_pn_cell_dot_pointwise))) -> fpmp_target_dot_mcp_ics_span_negative_source_image_raw_pn_cell_dot_pointwise = fpmp_left_dot_mcp_ics_span_negative_source_image_raw_pn_cell_dot_pointwise * fpmp_right_dot_mcp_ics_span_negative_source_image_raw_pn_cell_dot_pointwise) /\ (exists ff_u_dot_mcp_ics_span_negative_source_image_raw_pn_cell_dot_sum ff_v_dot_mcp_ics_span_negative_source_image_raw_pn_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_span_negative_source_image_raw_pn_cell_dot_sum_start. ff_h_dot_mcp_ics_span_negative_source_image_raw_pn_cell_dot_sum_start + S (0) = S ((S (0)) * ff_v_dot_mcp_ics_span_negative_source_image_raw_pn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_span_negative_source_image_raw_pn_cell_dot_sum_start. ff_u_dot_mcp_ics_span_negative_source_image_raw_pn_cell_dot_sum = ff_q_dot_mcp_ics_span_negative_source_image_raw_pn_cell_dot_sum_start * S ((S (0)) * ff_v_dot_mcp_ics_span_negative_source_image_raw_pn_cell_dot_sum) + (0))) /\ ((((exists ff_h_dot_mcp_ics_span_negative_source_image_raw_pn_cell_dot_sum_terminal. ff_h_dot_mcp_ics_span_negative_source_image_raw_pn_cell_dot_sum_terminal + S (ff_value_mcp_prefix_ics_span_negative_source_image_raw_pn) = S ((S (w)) * ff_v_dot_mcp_ics_span_negative_source_image_raw_pn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_span_negative_source_image_raw_pn_cell_dot_sum_terminal. ff_u_dot_mcp_ics_span_negative_source_image_raw_pn_cell_dot_sum = ff_q_dot_mcp_ics_span_negative_source_image_raw_pn_cell_dot_sum_terminal * S ((S (w)) * ff_v_dot_mcp_ics_span_negative_source_image_raw_pn_cell_dot_sum) + (ff_value_mcp_prefix_ics_span_negative_source_image_raw_pn))) /\ forall ff_i_dot_mcp_ics_span_negative_source_image_raw_pn_cell_dot_sum. (exists ff_lt_dot_mcp_ics_span_negative_source_image_raw_pn_cell_dot_sum_bound. ff_lt_dot_mcp_ics_span_negative_source_image_raw_pn_cell_dot_sum_bound + S ff_i_dot_mcp_ics_span_negative_source_image_raw_pn_cell_dot_sum = w) -> exists ff_a_dot_mcp_ics_span_negative_source_image_raw_pn_cell_dot_sum ff_r_dot_mcp_ics_span_negative_source_image_raw_pn_cell_dot_sum ff_s_dot_mcp_ics_span_negative_source_image_raw_pn_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_span_negative_source_image_raw_pn_cell_dot_sum_summand. ff_h_dot_mcp_ics_span_negative_source_image_raw_pn_cell_dot_sum_summand + S (ff_a_dot_mcp_ics_span_negative_source_image_raw_pn_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_span_negative_source_image_raw_pn_cell_dot_sum)) * ff_scale_dot_mcp_ics_span_negative_source_image_raw_pn_cell_dot)) /\ exists ff_q_dot_mcp_ics_span_negative_source_image_raw_pn_cell_dot_sum_summand. ff_code_dot_mcp_ics_span_negative_source_image_raw_pn_cell_dot = ff_q_dot_mcp_ics_span_negative_source_image_raw_pn_cell_dot_sum_summand * S ((S (ff_i_dot_mcp_ics_span_negative_source_image_raw_pn_cell_dot_sum)) * ff_scale_dot_mcp_ics_span_negative_source_image_raw_pn_cell_dot) + (ff_a_dot_mcp_ics_span_negative_source_image_raw_pn_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_span_negative_source_image_raw_pn_cell_dot_sum_partial. ff_h_dot_mcp_ics_span_negative_source_image_raw_pn_cell_dot_sum_partial + S (ff_r_dot_mcp_ics_span_negative_source_image_raw_pn_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_span_negative_source_image_raw_pn_cell_dot_sum)) * ff_v_dot_mcp_ics_span_negative_source_image_raw_pn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_span_negative_source_image_raw_pn_cell_dot_sum_partial. ff_u_dot_mcp_ics_span_negative_source_image_raw_pn_cell_dot_sum = ff_q_dot_mcp_ics_span_negative_source_image_raw_pn_cell_dot_sum_partial * S ((S (ff_i_dot_mcp_ics_span_negative_source_image_raw_pn_cell_dot_sum)) * ff_v_dot_mcp_ics_span_negative_source_image_raw_pn_cell_dot_sum) + (ff_r_dot_mcp_ics_span_negative_source_image_raw_pn_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_span_negative_source_image_raw_pn_cell_dot_sum_successor. ff_h_dot_mcp_ics_span_negative_source_image_raw_pn_cell_dot_sum_successor + S (ff_s_dot_mcp_ics_span_negative_source_image_raw_pn_cell_dot_sum) = S ((S (S ff_i_dot_mcp_ics_span_negative_source_image_raw_pn_cell_dot_sum)) * ff_v_dot_mcp_ics_span_negative_source_image_raw_pn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_span_negative_source_image_raw_pn_cell_dot_sum_successor. ff_u_dot_mcp_ics_span_negative_source_image_raw_pn_cell_dot_sum = ff_q_dot_mcp_ics_span_negative_source_image_raw_pn_cell_dot_sum_successor * S ((S (S ff_i_dot_mcp_ics_span_negative_source_image_raw_pn_cell_dot_sum)) * ff_v_dot_mcp_ics_span_negative_source_image_raw_pn_cell_dot_sum) + (ff_s_dot_mcp_ics_span_negative_source_image_raw_pn_cell_dot_sum))) /\ ff_s_dot_mcp_ics_span_negative_source_image_raw_pn_cell_dot_sum = ff_r_dot_mcp_ics_span_negative_source_image_raw_pn_cell_dot_sum + ff_a_dot_mcp_ics_span_negative_source_image_raw_pn_cell_dot_sum))))))))))) /\ (((exists fs_h_mcp_ics_span_negative_source_image_raw_pn_entry. fs_h_mcp_ics_span_negative_source_image_raw_pn_entry + S (ff_value_mcp_prefix_ics_span_negative_source_image_raw_pn) = S ((S (ff_index_mcp_prefix_ics_span_negative_source_image_raw_pn)) * ff_pns_mcp_smatrix_ics_span_negative_source_image_raw)) /\ exists fs_q_mcp_ics_span_negative_source_image_raw_pn_entry. ff_pn_mcp_smatrix_ics_span_negative_source_image_raw = fs_q_mcp_ics_span_negative_source_image_raw_pn_entry * S ((S (ff_index_mcp_prefix_ics_span_negative_source_image_raw_pn)) * ff_pns_mcp_smatrix_ics_span_negative_source_image_raw) + (ff_value_mcp_prefix_ics_span_negative_source_image_raw_pn))))))) /\ ((forall ff_index_mcp_prefix_ics_span_negative_source_image_raw_np. (exists mcp_gap_ics_span_negative_source_image_raw_np_index. mcp_gap_ics_span_negative_source_image_raw_np_index + S (ff_index_mcp_prefix_ics_span_negative_source_image_raw_np) = ((r) * (1))) -> exists ff_row_mcp_prefix_ics_span_negative_source_image_raw_np ff_column_mcp_prefix_ics_span_negative_source_image_raw_np ff_value_mcp_prefix_ics_span_negative_source_image_raw_np. ((ff_index_mcp_prefix_ics_span_negative_source_image_raw_np) = (1) * ff_row_mcp_prefix_ics_span_negative_source_image_raw_np + ff_column_mcp_prefix_ics_span_negative_source_image_raw_np /\ ((exists mcp_gap_ics_span_negative_source_image_raw_np_column. mcp_gap_ics_span_negative_source_image_raw_np_column + S (ff_column_mcp_prefix_ics_span_negative_source_image_raw_np) = (1)) /\ ((exists ff_left_mcp_cell_ics_span_negative_source_image_raw_np_cell ff_left_scale_mcp_cell_ics_span_negative_source_image_raw_np_cell ff_right_mcp_cell_ics_span_negative_source_image_raw_np_cell ff_right_scale_mcp_cell_ics_span_negative_source_image_raw_np_cell. ((forall ff_index_mcp_ics_span_negative_source_image_raw_np_cell_row ff_source_mcp_ics_span_negative_source_image_raw_np_cell_row ff_target_mcp_ics_span_negative_source_image_raw_np_cell_row. (exists mcp_gap_ics_span_negative_source_image_raw_np_cell_row_bound. mcp_gap_ics_span_negative_source_image_raw_np_cell_row_bound + S (ff_index_mcp_ics_span_negative_source_image_raw_np_cell_row) = (w)) -> (((exists fs_h_mcp_ics_span_negative_source_image_raw_np_cell_row_source. fs_h_mcp_ics_span_negative_source_image_raw_np_cell_row_source + S (ff_source_mcp_ics_span_negative_source_image_raw_np_cell_row) = S ((S (((ff_row_mcp_prefix_ics_span_negative_source_image_raw_np) * (w)) + (1) * ff_index_mcp_ics_span_negative_source_image_raw_np_cell_row)) * dc)) /\ exists fs_q_mcp_ics_span_negative_source_image_raw_np_cell_row_source. db = fs_q_mcp_ics_span_negative_source_image_raw_np_cell_row_source * S ((S (((ff_row_mcp_prefix_ics_span_negative_source_image_raw_np) * (w)) + (1) * ff_index_mcp_ics_span_negative_source_image_raw_np_cell_row)) * dc) + (ff_source_mcp_ics_span_negative_source_image_raw_np_cell_row))) -> (((exists fs_h_mcp_ics_span_negative_source_image_raw_np_cell_row_target. fs_h_mcp_ics_span_negative_source_image_raw_np_cell_row_target + S (ff_target_mcp_ics_span_negative_source_image_raw_np_cell_row) = S ((S (ff_index_mcp_ics_span_negative_source_image_raw_np_cell_row)) * ff_left_scale_mcp_cell_ics_span_negative_source_image_raw_np_cell)) /\ exists fs_q_mcp_ics_span_negative_source_image_raw_np_cell_row_target. ff_left_mcp_cell_ics_span_negative_source_image_raw_np_cell = fs_q_mcp_ics_span_negative_source_image_raw_np_cell_row_target * S ((S (ff_index_mcp_ics_span_negative_source_image_raw_np_cell_row)) * ff_left_scale_mcp_cell_ics_span_negative_source_image_raw_np_cell) + (ff_target_mcp_ics_span_negative_source_image_raw_np_cell_row))) -> ff_target_mcp_ics_span_negative_source_image_raw_np_cell_row = ff_source_mcp_ics_span_negative_source_image_raw_np_cell_row) /\ ((forall ff_index_mcp_ics_span_negative_source_image_raw_np_cell_column ff_source_mcp_ics_span_negative_source_image_raw_np_cell_column ff_target_mcp_ics_span_negative_source_image_raw_np_cell_column. (exists mcp_gap_ics_span_negative_source_image_raw_np_cell_column_bound. mcp_gap_ics_span_negative_source_image_raw_np_cell_column_bound + S (ff_index_mcp_ics_span_negative_source_image_raw_np_cell_column) = (w)) -> (((exists fs_h_mcp_ics_span_negative_source_image_raw_np_cell_column_source. fs_h_mcp_ics_span_negative_source_image_raw_np_cell_column_source + S (ff_source_mcp_ics_span_negative_source_image_raw_np_cell_column) = S ((S ((ff_column_mcp_prefix_ics_span_negative_source_image_raw_np) + (1) * ff_index_mcp_ics_span_negative_source_image_raw_np_cell_column)) * ics_coefficient_positive_scale_span_negative_source)) /\ exists fs_q_mcp_ics_span_negative_source_image_raw_np_cell_column_source. ics_coefficient_positive_span_negative_source = fs_q_mcp_ics_span_negative_source_image_raw_np_cell_column_source * S ((S ((ff_column_mcp_prefix_ics_span_negative_source_image_raw_np) + (1) * ff_index_mcp_ics_span_negative_source_image_raw_np_cell_column)) * ics_coefficient_positive_scale_span_negative_source) + (ff_source_mcp_ics_span_negative_source_image_raw_np_cell_column))) -> (((exists fs_h_mcp_ics_span_negative_source_image_raw_np_cell_column_target. fs_h_mcp_ics_span_negative_source_image_raw_np_cell_column_target + S (ff_target_mcp_ics_span_negative_source_image_raw_np_cell_column) = S ((S (ff_index_mcp_ics_span_negative_source_image_raw_np_cell_column)) * ff_right_scale_mcp_cell_ics_span_negative_source_image_raw_np_cell)) /\ exists fs_q_mcp_ics_span_negative_source_image_raw_np_cell_column_target. ff_right_mcp_cell_ics_span_negative_source_image_raw_np_cell = fs_q_mcp_ics_span_negative_source_image_raw_np_cell_column_target * S ((S (ff_index_mcp_ics_span_negative_source_image_raw_np_cell_column)) * ff_right_scale_mcp_cell_ics_span_negative_source_image_raw_np_cell) + (ff_target_mcp_ics_span_negative_source_image_raw_np_cell_column))) -> ff_target_mcp_ics_span_negative_source_image_raw_np_cell_column = ff_source_mcp_ics_span_negative_source_image_raw_np_cell_column) /\ (exists ff_code_dot_mcp_ics_span_negative_source_image_raw_np_cell_dot ff_scale_dot_mcp_ics_span_negative_source_image_raw_np_cell_dot. ((forall fpmp_index_dot_mcp_ics_span_negative_source_image_raw_np_cell_dot_pointwise fpmp_left_dot_mcp_ics_span_negative_source_image_raw_np_cell_dot_pointwise fpmp_right_dot_mcp_ics_span_negative_source_image_raw_np_cell_dot_pointwise fpmp_target_dot_mcp_ics_span_negative_source_image_raw_np_cell_dot_pointwise. (exists fpmp_gap_dot_mcp_ics_span_negative_source_image_raw_np_cell_dot_pointwise. fpmp_gap_dot_mcp_ics_span_negative_source_image_raw_np_cell_dot_pointwise + S fpmp_index_dot_mcp_ics_span_negative_source_image_raw_np_cell_dot_pointwise = w) -> (((exists ff_h_fpmp_dot_mcp_ics_span_negative_source_image_raw_np_cell_dot_pointwise_left. ff_h_fpmp_dot_mcp_ics_span_negative_source_image_raw_np_cell_dot_pointwise_left + S (fpmp_left_dot_mcp_ics_span_negative_source_image_raw_np_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_span_negative_source_image_raw_np_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_span_negative_source_image_raw_np_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_span_negative_source_image_raw_np_cell_dot_pointwise_left. ff_left_mcp_cell_ics_span_negative_source_image_raw_np_cell = ff_q_fpmp_dot_mcp_ics_span_negative_source_image_raw_np_cell_dot_pointwise_left * S ((S (fpmp_index_dot_mcp_ics_span_negative_source_image_raw_np_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_span_negative_source_image_raw_np_cell) + (fpmp_left_dot_mcp_ics_span_negative_source_image_raw_np_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_span_negative_source_image_raw_np_cell_dot_pointwise_right. ff_h_fpmp_dot_mcp_ics_span_negative_source_image_raw_np_cell_dot_pointwise_right + S (fpmp_right_dot_mcp_ics_span_negative_source_image_raw_np_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_span_negative_source_image_raw_np_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_span_negative_source_image_raw_np_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_span_negative_source_image_raw_np_cell_dot_pointwise_right. ff_right_mcp_cell_ics_span_negative_source_image_raw_np_cell = ff_q_fpmp_dot_mcp_ics_span_negative_source_image_raw_np_cell_dot_pointwise_right * S ((S (fpmp_index_dot_mcp_ics_span_negative_source_image_raw_np_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_span_negative_source_image_raw_np_cell) + (fpmp_right_dot_mcp_ics_span_negative_source_image_raw_np_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_span_negative_source_image_raw_np_cell_dot_pointwise_target. ff_h_fpmp_dot_mcp_ics_span_negative_source_image_raw_np_cell_dot_pointwise_target + S (fpmp_target_dot_mcp_ics_span_negative_source_image_raw_np_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_span_negative_source_image_raw_np_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_span_negative_source_image_raw_np_cell_dot)) /\ exists ff_q_fpmp_dot_mcp_ics_span_negative_source_image_raw_np_cell_dot_pointwise_target. ff_code_dot_mcp_ics_span_negative_source_image_raw_np_cell_dot = ff_q_fpmp_dot_mcp_ics_span_negative_source_image_raw_np_cell_dot_pointwise_target * S ((S (fpmp_index_dot_mcp_ics_span_negative_source_image_raw_np_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_span_negative_source_image_raw_np_cell_dot) + (fpmp_target_dot_mcp_ics_span_negative_source_image_raw_np_cell_dot_pointwise))) -> fpmp_target_dot_mcp_ics_span_negative_source_image_raw_np_cell_dot_pointwise = fpmp_left_dot_mcp_ics_span_negative_source_image_raw_np_cell_dot_pointwise * fpmp_right_dot_mcp_ics_span_negative_source_image_raw_np_cell_dot_pointwise) /\ (exists ff_u_dot_mcp_ics_span_negative_source_image_raw_np_cell_dot_sum ff_v_dot_mcp_ics_span_negative_source_image_raw_np_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_span_negative_source_image_raw_np_cell_dot_sum_start. ff_h_dot_mcp_ics_span_negative_source_image_raw_np_cell_dot_sum_start + S (0) = S ((S (0)) * ff_v_dot_mcp_ics_span_negative_source_image_raw_np_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_span_negative_source_image_raw_np_cell_dot_sum_start. ff_u_dot_mcp_ics_span_negative_source_image_raw_np_cell_dot_sum = ff_q_dot_mcp_ics_span_negative_source_image_raw_np_cell_dot_sum_start * S ((S (0)) * ff_v_dot_mcp_ics_span_negative_source_image_raw_np_cell_dot_sum) + (0))) /\ ((((exists ff_h_dot_mcp_ics_span_negative_source_image_raw_np_cell_dot_sum_terminal. ff_h_dot_mcp_ics_span_negative_source_image_raw_np_cell_dot_sum_terminal + S (ff_value_mcp_prefix_ics_span_negative_source_image_raw_np) = S ((S (w)) * ff_v_dot_mcp_ics_span_negative_source_image_raw_np_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_span_negative_source_image_raw_np_cell_dot_sum_terminal. ff_u_dot_mcp_ics_span_negative_source_image_raw_np_cell_dot_sum = ff_q_dot_mcp_ics_span_negative_source_image_raw_np_cell_dot_sum_terminal * S ((S (w)) * ff_v_dot_mcp_ics_span_negative_source_image_raw_np_cell_dot_sum) + (ff_value_mcp_prefix_ics_span_negative_source_image_raw_np))) /\ forall ff_i_dot_mcp_ics_span_negative_source_image_raw_np_cell_dot_sum. (exists ff_lt_dot_mcp_ics_span_negative_source_image_raw_np_cell_dot_sum_bound. ff_lt_dot_mcp_ics_span_negative_source_image_raw_np_cell_dot_sum_bound + S ff_i_dot_mcp_ics_span_negative_source_image_raw_np_cell_dot_sum = w) -> exists ff_a_dot_mcp_ics_span_negative_source_image_raw_np_cell_dot_sum ff_r_dot_mcp_ics_span_negative_source_image_raw_np_cell_dot_sum ff_s_dot_mcp_ics_span_negative_source_image_raw_np_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_span_negative_source_image_raw_np_cell_dot_sum_summand. ff_h_dot_mcp_ics_span_negative_source_image_raw_np_cell_dot_sum_summand + S (ff_a_dot_mcp_ics_span_negative_source_image_raw_np_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_span_negative_source_image_raw_np_cell_dot_sum)) * ff_scale_dot_mcp_ics_span_negative_source_image_raw_np_cell_dot)) /\ exists ff_q_dot_mcp_ics_span_negative_source_image_raw_np_cell_dot_sum_summand. ff_code_dot_mcp_ics_span_negative_source_image_raw_np_cell_dot = ff_q_dot_mcp_ics_span_negative_source_image_raw_np_cell_dot_sum_summand * S ((S (ff_i_dot_mcp_ics_span_negative_source_image_raw_np_cell_dot_sum)) * ff_scale_dot_mcp_ics_span_negative_source_image_raw_np_cell_dot) + (ff_a_dot_mcp_ics_span_negative_source_image_raw_np_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_span_negative_source_image_raw_np_cell_dot_sum_partial. ff_h_dot_mcp_ics_span_negative_source_image_raw_np_cell_dot_sum_partial + S (ff_r_dot_mcp_ics_span_negative_source_image_raw_np_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_span_negative_source_image_raw_np_cell_dot_sum)) * ff_v_dot_mcp_ics_span_negative_source_image_raw_np_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_span_negative_source_image_raw_np_cell_dot_sum_partial. ff_u_dot_mcp_ics_span_negative_source_image_raw_np_cell_dot_sum = ff_q_dot_mcp_ics_span_negative_source_image_raw_np_cell_dot_sum_partial * S ((S (ff_i_dot_mcp_ics_span_negative_source_image_raw_np_cell_dot_sum)) * ff_v_dot_mcp_ics_span_negative_source_image_raw_np_cell_dot_sum) + (ff_r_dot_mcp_ics_span_negative_source_image_raw_np_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_span_negative_source_image_raw_np_cell_dot_sum_successor. ff_h_dot_mcp_ics_span_negative_source_image_raw_np_cell_dot_sum_successor + S (ff_s_dot_mcp_ics_span_negative_source_image_raw_np_cell_dot_sum) = S ((S (S ff_i_dot_mcp_ics_span_negative_source_image_raw_np_cell_dot_sum)) * ff_v_dot_mcp_ics_span_negative_source_image_raw_np_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_span_negative_source_image_raw_np_cell_dot_sum_successor. ff_u_dot_mcp_ics_span_negative_source_image_raw_np_cell_dot_sum = ff_q_dot_mcp_ics_span_negative_source_image_raw_np_cell_dot_sum_successor * S ((S (S ff_i_dot_mcp_ics_span_negative_source_image_raw_np_cell_dot_sum)) * ff_v_dot_mcp_ics_span_negative_source_image_raw_np_cell_dot_sum) + (ff_s_dot_mcp_ics_span_negative_source_image_raw_np_cell_dot_sum))) /\ ff_s_dot_mcp_ics_span_negative_source_image_raw_np_cell_dot_sum = ff_r_dot_mcp_ics_span_negative_source_image_raw_np_cell_dot_sum + ff_a_dot_mcp_ics_span_negative_source_image_raw_np_cell_dot_sum))))))))))) /\ (((exists fs_h_mcp_ics_span_negative_source_image_raw_np_entry. fs_h_mcp_ics_span_negative_source_image_raw_np_entry + S (ff_value_mcp_prefix_ics_span_negative_source_image_raw_np) = S ((S (ff_index_mcp_prefix_ics_span_negative_source_image_raw_np)) * ff_nps_mcp_smatrix_ics_span_negative_source_image_raw)) /\ exists fs_q_mcp_ics_span_negative_source_image_raw_np_entry. ff_np_mcp_smatrix_ics_span_negative_source_image_raw = fs_q_mcp_ics_span_negative_source_image_raw_np_entry * S ((S (ff_index_mcp_prefix_ics_span_negative_source_image_raw_np)) * ff_nps_mcp_smatrix_ics_span_negative_source_image_raw) + (ff_value_mcp_prefix_ics_span_negative_source_image_raw_np))))))) /\ ((forall ff_index_mcp_add_ics_span_negative_source_image_raw_positive ff_left_mcp_add_ics_span_negative_source_image_raw_positive ff_right_mcp_add_ics_span_negative_source_image_raw_positive ff_target_mcp_add_ics_span_negative_source_image_raw_positive. (exists mcp_gap_ics_span_negative_source_image_raw_positive_bound. mcp_gap_ics_span_negative_source_image_raw_positive_bound + S (ff_index_mcp_add_ics_span_negative_source_image_raw_positive) = ((r) * (1))) -> (((exists fs_h_mcp_ics_span_negative_source_image_raw_positive_left. fs_h_mcp_ics_span_negative_source_image_raw_positive_left + S (ff_left_mcp_add_ics_span_negative_source_image_raw_positive) = S ((S (ff_index_mcp_add_ics_span_negative_source_image_raw_positive)) * ff_pps_mcp_smatrix_ics_span_negative_source_image_raw)) /\ exists fs_q_mcp_ics_span_negative_source_image_raw_positive_left. ff_pp_mcp_smatrix_ics_span_negative_source_image_raw = fs_q_mcp_ics_span_negative_source_image_raw_positive_left * S ((S (ff_index_mcp_add_ics_span_negative_source_image_raw_positive)) * ff_pps_mcp_smatrix_ics_span_negative_source_image_raw) + (ff_left_mcp_add_ics_span_negative_source_image_raw_positive))) -> (((exists fs_h_mcp_ics_span_negative_source_image_raw_positive_right. fs_h_mcp_ics_span_negative_source_image_raw_positive_right + S (ff_right_mcp_add_ics_span_negative_source_image_raw_positive) = S ((S (ff_index_mcp_add_ics_span_negative_source_image_raw_positive)) * ff_nns_mcp_smatrix_ics_span_negative_source_image_raw)) /\ exists fs_q_mcp_ics_span_negative_source_image_raw_positive_right. ff_nn_mcp_smatrix_ics_span_negative_source_image_raw = fs_q_mcp_ics_span_negative_source_image_raw_positive_right * S ((S (ff_index_mcp_add_ics_span_negative_source_image_raw_positive)) * ff_nns_mcp_smatrix_ics_span_negative_source_image_raw) + (ff_right_mcp_add_ics_span_negative_source_image_raw_positive))) -> (((exists fs_h_mcp_ics_span_negative_source_image_raw_positive_target. fs_h_mcp_ics_span_negative_source_image_raw_positive_target + S (ff_target_mcp_add_ics_span_negative_source_image_raw_positive) = S ((S (ff_index_mcp_add_ics_span_negative_source_image_raw_positive)) * ics_raw_positive_scale_span_negative_source_image)) /\ exists fs_q_mcp_ics_span_negative_source_image_raw_positive_target. ics_raw_positive_span_negative_source_image = fs_q_mcp_ics_span_negative_source_image_raw_positive_target * S ((S (ff_index_mcp_add_ics_span_negative_source_image_raw_positive)) * ics_raw_positive_scale_span_negative_source_image) + (ff_target_mcp_add_ics_span_negative_source_image_raw_positive))) -> ff_target_mcp_add_ics_span_negative_source_image_raw_positive = ff_left_mcp_add_ics_span_negative_source_image_raw_positive + ff_right_mcp_add_ics_span_negative_source_image_raw_positive) /\ (forall ff_index_mcp_add_ics_span_negative_source_image_raw_negative ff_left_mcp_add_ics_span_negative_source_image_raw_negative ff_right_mcp_add_ics_span_negative_source_image_raw_negative ff_target_mcp_add_ics_span_negative_source_image_raw_negative. (exists mcp_gap_ics_span_negative_source_image_raw_negative_bound. mcp_gap_ics_span_negative_source_image_raw_negative_bound + S (ff_index_mcp_add_ics_span_negative_source_image_raw_negative) = ((r) * (1))) -> (((exists fs_h_mcp_ics_span_negative_source_image_raw_negative_left. fs_h_mcp_ics_span_negative_source_image_raw_negative_left + S (ff_left_mcp_add_ics_span_negative_source_image_raw_negative) = S ((S (ff_index_mcp_add_ics_span_negative_source_image_raw_negative)) * ff_pns_mcp_smatrix_ics_span_negative_source_image_raw)) /\ exists fs_q_mcp_ics_span_negative_source_image_raw_negative_left. ff_pn_mcp_smatrix_ics_span_negative_source_image_raw = fs_q_mcp_ics_span_negative_source_image_raw_negative_left * S ((S (ff_index_mcp_add_ics_span_negative_source_image_raw_negative)) * ff_pns_mcp_smatrix_ics_span_negative_source_image_raw) + (ff_left_mcp_add_ics_span_negative_source_image_raw_negative))) -> (((exists fs_h_mcp_ics_span_negative_source_image_raw_negative_right. fs_h_mcp_ics_span_negative_source_image_raw_negative_right + S (ff_right_mcp_add_ics_span_negative_source_image_raw_negative) = S ((S (ff_index_mcp_add_ics_span_negative_source_image_raw_negative)) * ff_nps_mcp_smatrix_ics_span_negative_source_image_raw)) /\ exists fs_q_mcp_ics_span_negative_source_image_raw_negative_right. ff_np_mcp_smatrix_ics_span_negative_source_image_raw = fs_q_mcp_ics_span_negative_source_image_raw_negative_right * S ((S (ff_index_mcp_add_ics_span_negative_source_image_raw_negative)) * ff_nps_mcp_smatrix_ics_span_negative_source_image_raw) + (ff_right_mcp_add_ics_span_negative_source_image_raw_negative))) -> (((exists fs_h_mcp_ics_span_negative_source_image_raw_negative_target. fs_h_mcp_ics_span_negative_source_image_raw_negative_target + S (ff_target_mcp_add_ics_span_negative_source_image_raw_negative) = S ((S (ff_index_mcp_add_ics_span_negative_source_image_raw_negative)) * ics_raw_negative_scale_span_negative_source_image)) /\ exists fs_q_mcp_ics_span_negative_source_image_raw_negative_target. ics_raw_negative_span_negative_source_image = fs_q_mcp_ics_span_negative_source_image_raw_negative_target * S ((S (ff_index_mcp_add_ics_span_negative_source_image_raw_negative)) * ics_raw_negative_scale_span_negative_source_image) + (ff_target_mcp_add_ics_span_negative_source_image_raw_negative))) -> ff_target_mcp_add_ics_span_negative_source_image_raw_negative = ff_left_mcp_add_ics_span_negative_source_image_raw_negative + ff_right_mcp_add_ics_span_negative_source_image_raw_negative))))))) /\ (forall ics_index_span_negative_source_image_equal ics_value0_span_negative_source_image_equal ics_value1_span_negative_source_image_equal ics_value2_span_negative_source_image_equal ics_value3_span_negative_source_image_equal. (exists ics_gap_span_negative_source_image_equal_bound. ics_gap_span_negative_source_image_equal_bound + S (ics_index_span_negative_source_image_equal) = (r)) -> (((exists fs_h_ics_span_negative_source_image_equal_at0. fs_h_ics_span_negative_source_image_equal_at0 + S (ics_value0_span_negative_source_image_equal) = S ((S (ics_index_span_negative_source_image_equal)) * ics_raw_positive_scale_span_negative_source_image)) /\ exists fs_q_ics_span_negative_source_image_equal_at0. ics_raw_positive_span_negative_source_image = fs_q_ics_span_negative_source_image_equal_at0 * S ((S (ics_index_span_negative_source_image_equal)) * ics_raw_positive_scale_span_negative_source_image) + (ics_value0_span_negative_source_image_equal))) -> (((exists fs_h_ics_span_negative_source_image_equal_at1. fs_h_ics_span_negative_source_image_equal_at1 + S (ics_value1_span_negative_source_image_equal) = S ((S (ics_index_span_negative_source_image_equal)) * ics_raw_negative_scale_span_negative_source_image)) /\ exists fs_q_ics_span_negative_source_image_equal_at1. ics_raw_negative_span_negative_source_image = fs_q_ics_span_negative_source_image_equal_at1 * S ((S (ics_index_span_negative_source_image_equal)) * ics_raw_negative_scale_span_negative_source_image) + (ics_value1_span_negative_source_image_equal))) -> (((exists fs_h_ics_span_negative_source_image_equal_at2. fs_h_ics_span_negative_source_image_equal_at2 + S (ics_value2_span_negative_source_image_equal) = S ((S (ics_index_span_negative_source_image_equal)) * pc)) /\ exists fs_q_ics_span_negative_source_image_equal_at2. pb = fs_q_ics_span_negative_source_image_equal_at2 * S ((S (ics_index_span_negative_source_image_equal)) * pc) + (ics_value2_span_negative_source_image_equal))) -> (((exists fs_h_ics_span_negative_source_image_equal_at3. fs_h_ics_span_negative_source_image_equal_at3 + S (ics_value3_span_negative_source_image_equal) = S ((S (ics_index_span_negative_source_image_equal)) * nc)) /\ exists fs_q_ics_span_negative_source_image_equal_at3. nb = fs_q_ics_span_negative_source_image_equal_at3 * S ((S (ics_index_span_negative_source_image_equal)) * nc) + (ics_value3_span_negative_source_image_equal))) -> ics_value0_span_negative_source_image_equal + ics_value3_span_negative_source_image_equal = ics_value2_span_negative_source_image_equal + ics_value1_span_negative_source_image_equal))))) -> (forall ics_index_span_negative_relation ics_value0_span_negative_relation ics_value1_span_negative_relation ics_value2_span_negative_relation ics_value3_span_negative_relation. (exists ics_gap_span_negative_relation_bound. ics_gap_span_negative_relation_bound + S (ics_index_span_negative_relation) = (r)) -> (((exists fs_h_ics_span_negative_relation_at0. fs_h_ics_span_negative_relation_at0 + S (ics_value0_span_negative_relation) = S ((S (ics_index_span_negative_relation)) * nc)) /\ exists fs_q_ics_span_negative_relation_at0. nb = fs_q_ics_span_negative_relation_at0 * S ((S (ics_index_span_negative_relation)) * nc) + (ics_value0_span_negative_relation))) -> (((exists fs_h_ics_span_negative_relation_at1. fs_h_ics_span_negative_relation_at1 + S (ics_value1_span_negative_relation) = S ((S (ics_index_span_negative_relation)) * pc)) /\ exists fs_q_ics_span_negative_relation_at1. pb = fs_q_ics_span_negative_relation_at1 * S ((S (ics_index_span_negative_relation)) * pc) + (ics_value1_span_negative_relation))) -> (((exists fs_h_ics_span_negative_relation_at2. fs_h_ics_span_negative_relation_at2 + S (ics_value2_span_negative_relation) = S ((S (ics_index_span_negative_relation)) * qc)) /\ exists fs_q_ics_span_negative_relation_at2. qb = fs_q_ics_span_negative_relation_at2 * S ((S (ics_index_span_negative_relation)) * qc) + (ics_value2_span_negative_relation))) -> (((exists fs_h_ics_span_negative_relation_at3. fs_h_ics_span_negative_relation_at3 + S (ics_value3_span_negative_relation) = S ((S (ics_index_span_negative_relation)) * mc)) /\ exists fs_q_ics_span_negative_relation_at3. mb = fs_q_ics_span_negative_relation_at3 * S ((S (ics_index_span_negative_relation)) * mc) + (ics_value3_span_negative_relation))) -> ics_value0_span_negative_relation + ics_value3_span_negative_relation = ics_value2_span_negative_relation + ics_value1_span_negative_relation) -> (exists ics_coefficient_positive_span_negative_result ics_coefficient_positive_scale_span_negative_result ics_coefficient_negative_span_negative_result ics_coefficient_negative_scale_span_negative_result. (exists ics_raw_positive_span_negative_result_image ics_raw_positive_scale_span_negative_result_image ics_raw_negative_span_negative_result_image ics_raw_negative_scale_span_negative_result_image. (((exists ff_pp_mcp_smatrix_ics_span_negative_result_image_raw ff_pps_mcp_smatrix_ics_span_negative_result_image_raw ff_nn_mcp_smatrix_ics_span_negative_result_image_raw ff_nns_mcp_smatrix_ics_span_negative_result_image_raw ff_pn_mcp_smatrix_ics_span_negative_result_image_raw ff_pns_mcp_smatrix_ics_span_negative_result_image_raw ff_np_mcp_smatrix_ics_span_negative_result_image_raw ff_nps_mcp_smatrix_ics_span_negative_result_image_raw. ((forall ff_index_mcp_prefix_ics_span_negative_result_image_raw_pp. (exists mcp_gap_ics_span_negative_result_image_raw_pp_index. mcp_gap_ics_span_negative_result_image_raw_pp_index + S (ff_index_mcp_prefix_ics_span_negative_result_image_raw_pp) = ((r) * (1))) -> exists ff_row_mcp_prefix_ics_span_negative_result_image_raw_pp ff_column_mcp_prefix_ics_span_negative_result_image_raw_pp ff_value_mcp_prefix_ics_span_negative_result_image_raw_pp. ((ff_index_mcp_prefix_ics_span_negative_result_image_raw_pp) = (1) * ff_row_mcp_prefix_ics_span_negative_result_image_raw_pp + ff_column_mcp_prefix_ics_span_negative_result_image_raw_pp /\ ((exists mcp_gap_ics_span_negative_result_image_raw_pp_column. mcp_gap_ics_span_negative_result_image_raw_pp_column + S (ff_column_mcp_prefix_ics_span_negative_result_image_raw_pp) = (1)) /\ ((exists ff_left_mcp_cell_ics_span_negative_result_image_raw_pp_cell ff_left_scale_mcp_cell_ics_span_negative_result_image_raw_pp_cell ff_right_mcp_cell_ics_span_negative_result_image_raw_pp_cell ff_right_scale_mcp_cell_ics_span_negative_result_image_raw_pp_cell. ((forall ff_index_mcp_ics_span_negative_result_image_raw_pp_cell_row ff_source_mcp_ics_span_negative_result_image_raw_pp_cell_row ff_target_mcp_ics_span_negative_result_image_raw_pp_cell_row. (exists mcp_gap_ics_span_negative_result_image_raw_pp_cell_row_bound. mcp_gap_ics_span_negative_result_image_raw_pp_cell_row_bound + S (ff_index_mcp_ics_span_negative_result_image_raw_pp_cell_row) = (w)) -> (((exists fs_h_mcp_ics_span_negative_result_image_raw_pp_cell_row_source. fs_h_mcp_ics_span_negative_result_image_raw_pp_cell_row_source + S (ff_source_mcp_ics_span_negative_result_image_raw_pp_cell_row) = S ((S (((ff_row_mcp_prefix_ics_span_negative_result_image_raw_pp) * (w)) + (1) * ff_index_mcp_ics_span_negative_result_image_raw_pp_cell_row)) * ac)) /\ exists fs_q_mcp_ics_span_negative_result_image_raw_pp_cell_row_source. ab = fs_q_mcp_ics_span_negative_result_image_raw_pp_cell_row_source * S ((S (((ff_row_mcp_prefix_ics_span_negative_result_image_raw_pp) * (w)) + (1) * ff_index_mcp_ics_span_negative_result_image_raw_pp_cell_row)) * ac) + (ff_source_mcp_ics_span_negative_result_image_raw_pp_cell_row))) -> (((exists fs_h_mcp_ics_span_negative_result_image_raw_pp_cell_row_target. fs_h_mcp_ics_span_negative_result_image_raw_pp_cell_row_target + S (ff_target_mcp_ics_span_negative_result_image_raw_pp_cell_row) = S ((S (ff_index_mcp_ics_span_negative_result_image_raw_pp_cell_row)) * ff_left_scale_mcp_cell_ics_span_negative_result_image_raw_pp_cell)) /\ exists fs_q_mcp_ics_span_negative_result_image_raw_pp_cell_row_target. ff_left_mcp_cell_ics_span_negative_result_image_raw_pp_cell = fs_q_mcp_ics_span_negative_result_image_raw_pp_cell_row_target * S ((S (ff_index_mcp_ics_span_negative_result_image_raw_pp_cell_row)) * ff_left_scale_mcp_cell_ics_span_negative_result_image_raw_pp_cell) + (ff_target_mcp_ics_span_negative_result_image_raw_pp_cell_row))) -> ff_target_mcp_ics_span_negative_result_image_raw_pp_cell_row = ff_source_mcp_ics_span_negative_result_image_raw_pp_cell_row) /\ ((forall ff_index_mcp_ics_span_negative_result_image_raw_pp_cell_column ff_source_mcp_ics_span_negative_result_image_raw_pp_cell_column ff_target_mcp_ics_span_negative_result_image_raw_pp_cell_column. (exists mcp_gap_ics_span_negative_result_image_raw_pp_cell_column_bound. mcp_gap_ics_span_negative_result_image_raw_pp_cell_column_bound + S (ff_index_mcp_ics_span_negative_result_image_raw_pp_cell_column) = (w)) -> (((exists fs_h_mcp_ics_span_negative_result_image_raw_pp_cell_column_source. fs_h_mcp_ics_span_negative_result_image_raw_pp_cell_column_source + S (ff_source_mcp_ics_span_negative_result_image_raw_pp_cell_column) = S ((S ((ff_column_mcp_prefix_ics_span_negative_result_image_raw_pp) + (1) * ff_index_mcp_ics_span_negative_result_image_raw_pp_cell_column)) * ics_coefficient_positive_scale_span_negative_result)) /\ exists fs_q_mcp_ics_span_negative_result_image_raw_pp_cell_column_source. ics_coefficient_positive_span_negative_result = fs_q_mcp_ics_span_negative_result_image_raw_pp_cell_column_source * S ((S ((ff_column_mcp_prefix_ics_span_negative_result_image_raw_pp) + (1) * ff_index_mcp_ics_span_negative_result_image_raw_pp_cell_column)) * ics_coefficient_positive_scale_span_negative_result) + (ff_source_mcp_ics_span_negative_result_image_raw_pp_cell_column))) -> (((exists fs_h_mcp_ics_span_negative_result_image_raw_pp_cell_column_target. fs_h_mcp_ics_span_negative_result_image_raw_pp_cell_column_target + S (ff_target_mcp_ics_span_negative_result_image_raw_pp_cell_column) = S ((S (ff_index_mcp_ics_span_negative_result_image_raw_pp_cell_column)) * ff_right_scale_mcp_cell_ics_span_negative_result_image_raw_pp_cell)) /\ exists fs_q_mcp_ics_span_negative_result_image_raw_pp_cell_column_target. ff_right_mcp_cell_ics_span_negative_result_image_raw_pp_cell = fs_q_mcp_ics_span_negative_result_image_raw_pp_cell_column_target * S ((S (ff_index_mcp_ics_span_negative_result_image_raw_pp_cell_column)) * ff_right_scale_mcp_cell_ics_span_negative_result_image_raw_pp_cell) + (ff_target_mcp_ics_span_negative_result_image_raw_pp_cell_column))) -> ff_target_mcp_ics_span_negative_result_image_raw_pp_cell_column = ff_source_mcp_ics_span_negative_result_image_raw_pp_cell_column) /\ (exists ff_code_dot_mcp_ics_span_negative_result_image_raw_pp_cell_dot ff_scale_dot_mcp_ics_span_negative_result_image_raw_pp_cell_dot. ((forall fpmp_index_dot_mcp_ics_span_negative_result_image_raw_pp_cell_dot_pointwise fpmp_left_dot_mcp_ics_span_negative_result_image_raw_pp_cell_dot_pointwise fpmp_right_dot_mcp_ics_span_negative_result_image_raw_pp_cell_dot_pointwise fpmp_target_dot_mcp_ics_span_negative_result_image_raw_pp_cell_dot_pointwise. (exists fpmp_gap_dot_mcp_ics_span_negative_result_image_raw_pp_cell_dot_pointwise. fpmp_gap_dot_mcp_ics_span_negative_result_image_raw_pp_cell_dot_pointwise + S fpmp_index_dot_mcp_ics_span_negative_result_image_raw_pp_cell_dot_pointwise = w) -> (((exists ff_h_fpmp_dot_mcp_ics_span_negative_result_image_raw_pp_cell_dot_pointwise_left. ff_h_fpmp_dot_mcp_ics_span_negative_result_image_raw_pp_cell_dot_pointwise_left + S (fpmp_left_dot_mcp_ics_span_negative_result_image_raw_pp_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_span_negative_result_image_raw_pp_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_span_negative_result_image_raw_pp_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_span_negative_result_image_raw_pp_cell_dot_pointwise_left. ff_left_mcp_cell_ics_span_negative_result_image_raw_pp_cell = ff_q_fpmp_dot_mcp_ics_span_negative_result_image_raw_pp_cell_dot_pointwise_left * S ((S (fpmp_index_dot_mcp_ics_span_negative_result_image_raw_pp_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_span_negative_result_image_raw_pp_cell) + (fpmp_left_dot_mcp_ics_span_negative_result_image_raw_pp_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_span_negative_result_image_raw_pp_cell_dot_pointwise_right. ff_h_fpmp_dot_mcp_ics_span_negative_result_image_raw_pp_cell_dot_pointwise_right + S (fpmp_right_dot_mcp_ics_span_negative_result_image_raw_pp_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_span_negative_result_image_raw_pp_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_span_negative_result_image_raw_pp_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_span_negative_result_image_raw_pp_cell_dot_pointwise_right. ff_right_mcp_cell_ics_span_negative_result_image_raw_pp_cell = ff_q_fpmp_dot_mcp_ics_span_negative_result_image_raw_pp_cell_dot_pointwise_right * S ((S (fpmp_index_dot_mcp_ics_span_negative_result_image_raw_pp_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_span_negative_result_image_raw_pp_cell) + (fpmp_right_dot_mcp_ics_span_negative_result_image_raw_pp_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_span_negative_result_image_raw_pp_cell_dot_pointwise_target. ff_h_fpmp_dot_mcp_ics_span_negative_result_image_raw_pp_cell_dot_pointwise_target + S (fpmp_target_dot_mcp_ics_span_negative_result_image_raw_pp_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_span_negative_result_image_raw_pp_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_span_negative_result_image_raw_pp_cell_dot)) /\ exists ff_q_fpmp_dot_mcp_ics_span_negative_result_image_raw_pp_cell_dot_pointwise_target. ff_code_dot_mcp_ics_span_negative_result_image_raw_pp_cell_dot = ff_q_fpmp_dot_mcp_ics_span_negative_result_image_raw_pp_cell_dot_pointwise_target * S ((S (fpmp_index_dot_mcp_ics_span_negative_result_image_raw_pp_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_span_negative_result_image_raw_pp_cell_dot) + (fpmp_target_dot_mcp_ics_span_negative_result_image_raw_pp_cell_dot_pointwise))) -> fpmp_target_dot_mcp_ics_span_negative_result_image_raw_pp_cell_dot_pointwise = fpmp_left_dot_mcp_ics_span_negative_result_image_raw_pp_cell_dot_pointwise * fpmp_right_dot_mcp_ics_span_negative_result_image_raw_pp_cell_dot_pointwise) /\ (exists ff_u_dot_mcp_ics_span_negative_result_image_raw_pp_cell_dot_sum ff_v_dot_mcp_ics_span_negative_result_image_raw_pp_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_span_negative_result_image_raw_pp_cell_dot_sum_start. ff_h_dot_mcp_ics_span_negative_result_image_raw_pp_cell_dot_sum_start + S (0) = S ((S (0)) * ff_v_dot_mcp_ics_span_negative_result_image_raw_pp_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_span_negative_result_image_raw_pp_cell_dot_sum_start. ff_u_dot_mcp_ics_span_negative_result_image_raw_pp_cell_dot_sum = ff_q_dot_mcp_ics_span_negative_result_image_raw_pp_cell_dot_sum_start * S ((S (0)) * ff_v_dot_mcp_ics_span_negative_result_image_raw_pp_cell_dot_sum) + (0))) /\ ((((exists ff_h_dot_mcp_ics_span_negative_result_image_raw_pp_cell_dot_sum_terminal. ff_h_dot_mcp_ics_span_negative_result_image_raw_pp_cell_dot_sum_terminal + S (ff_value_mcp_prefix_ics_span_negative_result_image_raw_pp) = S ((S (w)) * ff_v_dot_mcp_ics_span_negative_result_image_raw_pp_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_span_negative_result_image_raw_pp_cell_dot_sum_terminal. ff_u_dot_mcp_ics_span_negative_result_image_raw_pp_cell_dot_sum = ff_q_dot_mcp_ics_span_negative_result_image_raw_pp_cell_dot_sum_terminal * S ((S (w)) * ff_v_dot_mcp_ics_span_negative_result_image_raw_pp_cell_dot_sum) + (ff_value_mcp_prefix_ics_span_negative_result_image_raw_pp))) /\ forall ff_i_dot_mcp_ics_span_negative_result_image_raw_pp_cell_dot_sum. (exists ff_lt_dot_mcp_ics_span_negative_result_image_raw_pp_cell_dot_sum_bound. ff_lt_dot_mcp_ics_span_negative_result_image_raw_pp_cell_dot_sum_bound + S ff_i_dot_mcp_ics_span_negative_result_image_raw_pp_cell_dot_sum = w) -> exists ff_a_dot_mcp_ics_span_negative_result_image_raw_pp_cell_dot_sum ff_r_dot_mcp_ics_span_negative_result_image_raw_pp_cell_dot_sum ff_s_dot_mcp_ics_span_negative_result_image_raw_pp_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_span_negative_result_image_raw_pp_cell_dot_sum_summand. ff_h_dot_mcp_ics_span_negative_result_image_raw_pp_cell_dot_sum_summand + S (ff_a_dot_mcp_ics_span_negative_result_image_raw_pp_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_span_negative_result_image_raw_pp_cell_dot_sum)) * ff_scale_dot_mcp_ics_span_negative_result_image_raw_pp_cell_dot)) /\ exists ff_q_dot_mcp_ics_span_negative_result_image_raw_pp_cell_dot_sum_summand. ff_code_dot_mcp_ics_span_negative_result_image_raw_pp_cell_dot = ff_q_dot_mcp_ics_span_negative_result_image_raw_pp_cell_dot_sum_summand * S ((S (ff_i_dot_mcp_ics_span_negative_result_image_raw_pp_cell_dot_sum)) * ff_scale_dot_mcp_ics_span_negative_result_image_raw_pp_cell_dot) + (ff_a_dot_mcp_ics_span_negative_result_image_raw_pp_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_span_negative_result_image_raw_pp_cell_dot_sum_partial. ff_h_dot_mcp_ics_span_negative_result_image_raw_pp_cell_dot_sum_partial + S (ff_r_dot_mcp_ics_span_negative_result_image_raw_pp_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_span_negative_result_image_raw_pp_cell_dot_sum)) * ff_v_dot_mcp_ics_span_negative_result_image_raw_pp_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_span_negative_result_image_raw_pp_cell_dot_sum_partial. ff_u_dot_mcp_ics_span_negative_result_image_raw_pp_cell_dot_sum = ff_q_dot_mcp_ics_span_negative_result_image_raw_pp_cell_dot_sum_partial * S ((S (ff_i_dot_mcp_ics_span_negative_result_image_raw_pp_cell_dot_sum)) * ff_v_dot_mcp_ics_span_negative_result_image_raw_pp_cell_dot_sum) + (ff_r_dot_mcp_ics_span_negative_result_image_raw_pp_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_span_negative_result_image_raw_pp_cell_dot_sum_successor. ff_h_dot_mcp_ics_span_negative_result_image_raw_pp_cell_dot_sum_successor + S (ff_s_dot_mcp_ics_span_negative_result_image_raw_pp_cell_dot_sum) = S ((S (S ff_i_dot_mcp_ics_span_negative_result_image_raw_pp_cell_dot_sum)) * ff_v_dot_mcp_ics_span_negative_result_image_raw_pp_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_span_negative_result_image_raw_pp_cell_dot_sum_successor. ff_u_dot_mcp_ics_span_negative_result_image_raw_pp_cell_dot_sum = ff_q_dot_mcp_ics_span_negative_result_image_raw_pp_cell_dot_sum_successor * S ((S (S ff_i_dot_mcp_ics_span_negative_result_image_raw_pp_cell_dot_sum)) * ff_v_dot_mcp_ics_span_negative_result_image_raw_pp_cell_dot_sum) + (ff_s_dot_mcp_ics_span_negative_result_image_raw_pp_cell_dot_sum))) /\ ff_s_dot_mcp_ics_span_negative_result_image_raw_pp_cell_dot_sum = ff_r_dot_mcp_ics_span_negative_result_image_raw_pp_cell_dot_sum + ff_a_dot_mcp_ics_span_negative_result_image_raw_pp_cell_dot_sum))))))))))) /\ (((exists fs_h_mcp_ics_span_negative_result_image_raw_pp_entry. fs_h_mcp_ics_span_negative_result_image_raw_pp_entry + S (ff_value_mcp_prefix_ics_span_negative_result_image_raw_pp) = S ((S (ff_index_mcp_prefix_ics_span_negative_result_image_raw_pp)) * ff_pps_mcp_smatrix_ics_span_negative_result_image_raw)) /\ exists fs_q_mcp_ics_span_negative_result_image_raw_pp_entry. ff_pp_mcp_smatrix_ics_span_negative_result_image_raw = fs_q_mcp_ics_span_negative_result_image_raw_pp_entry * S ((S (ff_index_mcp_prefix_ics_span_negative_result_image_raw_pp)) * ff_pps_mcp_smatrix_ics_span_negative_result_image_raw) + (ff_value_mcp_prefix_ics_span_negative_result_image_raw_pp))))))) /\ ((forall ff_index_mcp_prefix_ics_span_negative_result_image_raw_nn. (exists mcp_gap_ics_span_negative_result_image_raw_nn_index. mcp_gap_ics_span_negative_result_image_raw_nn_index + S (ff_index_mcp_prefix_ics_span_negative_result_image_raw_nn) = ((r) * (1))) -> exists ff_row_mcp_prefix_ics_span_negative_result_image_raw_nn ff_column_mcp_prefix_ics_span_negative_result_image_raw_nn ff_value_mcp_prefix_ics_span_negative_result_image_raw_nn. ((ff_index_mcp_prefix_ics_span_negative_result_image_raw_nn) = (1) * ff_row_mcp_prefix_ics_span_negative_result_image_raw_nn + ff_column_mcp_prefix_ics_span_negative_result_image_raw_nn /\ ((exists mcp_gap_ics_span_negative_result_image_raw_nn_column. mcp_gap_ics_span_negative_result_image_raw_nn_column + S (ff_column_mcp_prefix_ics_span_negative_result_image_raw_nn) = (1)) /\ ((exists ff_left_mcp_cell_ics_span_negative_result_image_raw_nn_cell ff_left_scale_mcp_cell_ics_span_negative_result_image_raw_nn_cell ff_right_mcp_cell_ics_span_negative_result_image_raw_nn_cell ff_right_scale_mcp_cell_ics_span_negative_result_image_raw_nn_cell. ((forall ff_index_mcp_ics_span_negative_result_image_raw_nn_cell_row ff_source_mcp_ics_span_negative_result_image_raw_nn_cell_row ff_target_mcp_ics_span_negative_result_image_raw_nn_cell_row. (exists mcp_gap_ics_span_negative_result_image_raw_nn_cell_row_bound. mcp_gap_ics_span_negative_result_image_raw_nn_cell_row_bound + S (ff_index_mcp_ics_span_negative_result_image_raw_nn_cell_row) = (w)) -> (((exists fs_h_mcp_ics_span_negative_result_image_raw_nn_cell_row_source. fs_h_mcp_ics_span_negative_result_image_raw_nn_cell_row_source + S (ff_source_mcp_ics_span_negative_result_image_raw_nn_cell_row) = S ((S (((ff_row_mcp_prefix_ics_span_negative_result_image_raw_nn) * (w)) + (1) * ff_index_mcp_ics_span_negative_result_image_raw_nn_cell_row)) * dc)) /\ exists fs_q_mcp_ics_span_negative_result_image_raw_nn_cell_row_source. db = fs_q_mcp_ics_span_negative_result_image_raw_nn_cell_row_source * S ((S (((ff_row_mcp_prefix_ics_span_negative_result_image_raw_nn) * (w)) + (1) * ff_index_mcp_ics_span_negative_result_image_raw_nn_cell_row)) * dc) + (ff_source_mcp_ics_span_negative_result_image_raw_nn_cell_row))) -> (((exists fs_h_mcp_ics_span_negative_result_image_raw_nn_cell_row_target. fs_h_mcp_ics_span_negative_result_image_raw_nn_cell_row_target + S (ff_target_mcp_ics_span_negative_result_image_raw_nn_cell_row) = S ((S (ff_index_mcp_ics_span_negative_result_image_raw_nn_cell_row)) * ff_left_scale_mcp_cell_ics_span_negative_result_image_raw_nn_cell)) /\ exists fs_q_mcp_ics_span_negative_result_image_raw_nn_cell_row_target. ff_left_mcp_cell_ics_span_negative_result_image_raw_nn_cell = fs_q_mcp_ics_span_negative_result_image_raw_nn_cell_row_target * S ((S (ff_index_mcp_ics_span_negative_result_image_raw_nn_cell_row)) * ff_left_scale_mcp_cell_ics_span_negative_result_image_raw_nn_cell) + (ff_target_mcp_ics_span_negative_result_image_raw_nn_cell_row))) -> ff_target_mcp_ics_span_negative_result_image_raw_nn_cell_row = ff_source_mcp_ics_span_negative_result_image_raw_nn_cell_row) /\ ((forall ff_index_mcp_ics_span_negative_result_image_raw_nn_cell_column ff_source_mcp_ics_span_negative_result_image_raw_nn_cell_column ff_target_mcp_ics_span_negative_result_image_raw_nn_cell_column. (exists mcp_gap_ics_span_negative_result_image_raw_nn_cell_column_bound. mcp_gap_ics_span_negative_result_image_raw_nn_cell_column_bound + S (ff_index_mcp_ics_span_negative_result_image_raw_nn_cell_column) = (w)) -> (((exists fs_h_mcp_ics_span_negative_result_image_raw_nn_cell_column_source. fs_h_mcp_ics_span_negative_result_image_raw_nn_cell_column_source + S (ff_source_mcp_ics_span_negative_result_image_raw_nn_cell_column) = S ((S ((ff_column_mcp_prefix_ics_span_negative_result_image_raw_nn) + (1) * ff_index_mcp_ics_span_negative_result_image_raw_nn_cell_column)) * ics_coefficient_negative_scale_span_negative_result)) /\ exists fs_q_mcp_ics_span_negative_result_image_raw_nn_cell_column_source. ics_coefficient_negative_span_negative_result = fs_q_mcp_ics_span_negative_result_image_raw_nn_cell_column_source * S ((S ((ff_column_mcp_prefix_ics_span_negative_result_image_raw_nn) + (1) * ff_index_mcp_ics_span_negative_result_image_raw_nn_cell_column)) * ics_coefficient_negative_scale_span_negative_result) + (ff_source_mcp_ics_span_negative_result_image_raw_nn_cell_column))) -> (((exists fs_h_mcp_ics_span_negative_result_image_raw_nn_cell_column_target. fs_h_mcp_ics_span_negative_result_image_raw_nn_cell_column_target + S (ff_target_mcp_ics_span_negative_result_image_raw_nn_cell_column) = S ((S (ff_index_mcp_ics_span_negative_result_image_raw_nn_cell_column)) * ff_right_scale_mcp_cell_ics_span_negative_result_image_raw_nn_cell)) /\ exists fs_q_mcp_ics_span_negative_result_image_raw_nn_cell_column_target. ff_right_mcp_cell_ics_span_negative_result_image_raw_nn_cell = fs_q_mcp_ics_span_negative_result_image_raw_nn_cell_column_target * S ((S (ff_index_mcp_ics_span_negative_result_image_raw_nn_cell_column)) * ff_right_scale_mcp_cell_ics_span_negative_result_image_raw_nn_cell) + (ff_target_mcp_ics_span_negative_result_image_raw_nn_cell_column))) -> ff_target_mcp_ics_span_negative_result_image_raw_nn_cell_column = ff_source_mcp_ics_span_negative_result_image_raw_nn_cell_column) /\ (exists ff_code_dot_mcp_ics_span_negative_result_image_raw_nn_cell_dot ff_scale_dot_mcp_ics_span_negative_result_image_raw_nn_cell_dot. ((forall fpmp_index_dot_mcp_ics_span_negative_result_image_raw_nn_cell_dot_pointwise fpmp_left_dot_mcp_ics_span_negative_result_image_raw_nn_cell_dot_pointwise fpmp_right_dot_mcp_ics_span_negative_result_image_raw_nn_cell_dot_pointwise fpmp_target_dot_mcp_ics_span_negative_result_image_raw_nn_cell_dot_pointwise. (exists fpmp_gap_dot_mcp_ics_span_negative_result_image_raw_nn_cell_dot_pointwise. fpmp_gap_dot_mcp_ics_span_negative_result_image_raw_nn_cell_dot_pointwise + S fpmp_index_dot_mcp_ics_span_negative_result_image_raw_nn_cell_dot_pointwise = w) -> (((exists ff_h_fpmp_dot_mcp_ics_span_negative_result_image_raw_nn_cell_dot_pointwise_left. ff_h_fpmp_dot_mcp_ics_span_negative_result_image_raw_nn_cell_dot_pointwise_left + S (fpmp_left_dot_mcp_ics_span_negative_result_image_raw_nn_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_span_negative_result_image_raw_nn_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_span_negative_result_image_raw_nn_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_span_negative_result_image_raw_nn_cell_dot_pointwise_left. ff_left_mcp_cell_ics_span_negative_result_image_raw_nn_cell = ff_q_fpmp_dot_mcp_ics_span_negative_result_image_raw_nn_cell_dot_pointwise_left * S ((S (fpmp_index_dot_mcp_ics_span_negative_result_image_raw_nn_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_span_negative_result_image_raw_nn_cell) + (fpmp_left_dot_mcp_ics_span_negative_result_image_raw_nn_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_span_negative_result_image_raw_nn_cell_dot_pointwise_right. ff_h_fpmp_dot_mcp_ics_span_negative_result_image_raw_nn_cell_dot_pointwise_right + S (fpmp_right_dot_mcp_ics_span_negative_result_image_raw_nn_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_span_negative_result_image_raw_nn_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_span_negative_result_image_raw_nn_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_span_negative_result_image_raw_nn_cell_dot_pointwise_right. ff_right_mcp_cell_ics_span_negative_result_image_raw_nn_cell = ff_q_fpmp_dot_mcp_ics_span_negative_result_image_raw_nn_cell_dot_pointwise_right * S ((S (fpmp_index_dot_mcp_ics_span_negative_result_image_raw_nn_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_span_negative_result_image_raw_nn_cell) + (fpmp_right_dot_mcp_ics_span_negative_result_image_raw_nn_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_span_negative_result_image_raw_nn_cell_dot_pointwise_target. ff_h_fpmp_dot_mcp_ics_span_negative_result_image_raw_nn_cell_dot_pointwise_target + S (fpmp_target_dot_mcp_ics_span_negative_result_image_raw_nn_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_span_negative_result_image_raw_nn_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_span_negative_result_image_raw_nn_cell_dot)) /\ exists ff_q_fpmp_dot_mcp_ics_span_negative_result_image_raw_nn_cell_dot_pointwise_target. ff_code_dot_mcp_ics_span_negative_result_image_raw_nn_cell_dot = ff_q_fpmp_dot_mcp_ics_span_negative_result_image_raw_nn_cell_dot_pointwise_target * S ((S (fpmp_index_dot_mcp_ics_span_negative_result_image_raw_nn_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_span_negative_result_image_raw_nn_cell_dot) + (fpmp_target_dot_mcp_ics_span_negative_result_image_raw_nn_cell_dot_pointwise))) -> fpmp_target_dot_mcp_ics_span_negative_result_image_raw_nn_cell_dot_pointwise = fpmp_left_dot_mcp_ics_span_negative_result_image_raw_nn_cell_dot_pointwise * fpmp_right_dot_mcp_ics_span_negative_result_image_raw_nn_cell_dot_pointwise) /\ (exists ff_u_dot_mcp_ics_span_negative_result_image_raw_nn_cell_dot_sum ff_v_dot_mcp_ics_span_negative_result_image_raw_nn_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_span_negative_result_image_raw_nn_cell_dot_sum_start. ff_h_dot_mcp_ics_span_negative_result_image_raw_nn_cell_dot_sum_start + S (0) = S ((S (0)) * ff_v_dot_mcp_ics_span_negative_result_image_raw_nn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_span_negative_result_image_raw_nn_cell_dot_sum_start. ff_u_dot_mcp_ics_span_negative_result_image_raw_nn_cell_dot_sum = ff_q_dot_mcp_ics_span_negative_result_image_raw_nn_cell_dot_sum_start * S ((S (0)) * ff_v_dot_mcp_ics_span_negative_result_image_raw_nn_cell_dot_sum) + (0))) /\ ((((exists ff_h_dot_mcp_ics_span_negative_result_image_raw_nn_cell_dot_sum_terminal. ff_h_dot_mcp_ics_span_negative_result_image_raw_nn_cell_dot_sum_terminal + S (ff_value_mcp_prefix_ics_span_negative_result_image_raw_nn) = S ((S (w)) * ff_v_dot_mcp_ics_span_negative_result_image_raw_nn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_span_negative_result_image_raw_nn_cell_dot_sum_terminal. ff_u_dot_mcp_ics_span_negative_result_image_raw_nn_cell_dot_sum = ff_q_dot_mcp_ics_span_negative_result_image_raw_nn_cell_dot_sum_terminal * S ((S (w)) * ff_v_dot_mcp_ics_span_negative_result_image_raw_nn_cell_dot_sum) + (ff_value_mcp_prefix_ics_span_negative_result_image_raw_nn))) /\ forall ff_i_dot_mcp_ics_span_negative_result_image_raw_nn_cell_dot_sum. (exists ff_lt_dot_mcp_ics_span_negative_result_image_raw_nn_cell_dot_sum_bound. ff_lt_dot_mcp_ics_span_negative_result_image_raw_nn_cell_dot_sum_bound + S ff_i_dot_mcp_ics_span_negative_result_image_raw_nn_cell_dot_sum = w) -> exists ff_a_dot_mcp_ics_span_negative_result_image_raw_nn_cell_dot_sum ff_r_dot_mcp_ics_span_negative_result_image_raw_nn_cell_dot_sum ff_s_dot_mcp_ics_span_negative_result_image_raw_nn_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_span_negative_result_image_raw_nn_cell_dot_sum_summand. ff_h_dot_mcp_ics_span_negative_result_image_raw_nn_cell_dot_sum_summand + S (ff_a_dot_mcp_ics_span_negative_result_image_raw_nn_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_span_negative_result_image_raw_nn_cell_dot_sum)) * ff_scale_dot_mcp_ics_span_negative_result_image_raw_nn_cell_dot)) /\ exists ff_q_dot_mcp_ics_span_negative_result_image_raw_nn_cell_dot_sum_summand. ff_code_dot_mcp_ics_span_negative_result_image_raw_nn_cell_dot = ff_q_dot_mcp_ics_span_negative_result_image_raw_nn_cell_dot_sum_summand * S ((S (ff_i_dot_mcp_ics_span_negative_result_image_raw_nn_cell_dot_sum)) * ff_scale_dot_mcp_ics_span_negative_result_image_raw_nn_cell_dot) + (ff_a_dot_mcp_ics_span_negative_result_image_raw_nn_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_span_negative_result_image_raw_nn_cell_dot_sum_partial. ff_h_dot_mcp_ics_span_negative_result_image_raw_nn_cell_dot_sum_partial + S (ff_r_dot_mcp_ics_span_negative_result_image_raw_nn_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_span_negative_result_image_raw_nn_cell_dot_sum)) * ff_v_dot_mcp_ics_span_negative_result_image_raw_nn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_span_negative_result_image_raw_nn_cell_dot_sum_partial. ff_u_dot_mcp_ics_span_negative_result_image_raw_nn_cell_dot_sum = ff_q_dot_mcp_ics_span_negative_result_image_raw_nn_cell_dot_sum_partial * S ((S (ff_i_dot_mcp_ics_span_negative_result_image_raw_nn_cell_dot_sum)) * ff_v_dot_mcp_ics_span_negative_result_image_raw_nn_cell_dot_sum) + (ff_r_dot_mcp_ics_span_negative_result_image_raw_nn_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_span_negative_result_image_raw_nn_cell_dot_sum_successor. ff_h_dot_mcp_ics_span_negative_result_image_raw_nn_cell_dot_sum_successor + S (ff_s_dot_mcp_ics_span_negative_result_image_raw_nn_cell_dot_sum) = S ((S (S ff_i_dot_mcp_ics_span_negative_result_image_raw_nn_cell_dot_sum)) * ff_v_dot_mcp_ics_span_negative_result_image_raw_nn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_span_negative_result_image_raw_nn_cell_dot_sum_successor. ff_u_dot_mcp_ics_span_negative_result_image_raw_nn_cell_dot_sum = ff_q_dot_mcp_ics_span_negative_result_image_raw_nn_cell_dot_sum_successor * S ((S (S ff_i_dot_mcp_ics_span_negative_result_image_raw_nn_cell_dot_sum)) * ff_v_dot_mcp_ics_span_negative_result_image_raw_nn_cell_dot_sum) + (ff_s_dot_mcp_ics_span_negative_result_image_raw_nn_cell_dot_sum))) /\ ff_s_dot_mcp_ics_span_negative_result_image_raw_nn_cell_dot_sum = ff_r_dot_mcp_ics_span_negative_result_image_raw_nn_cell_dot_sum + ff_a_dot_mcp_ics_span_negative_result_image_raw_nn_cell_dot_sum))))))))))) /\ (((exists fs_h_mcp_ics_span_negative_result_image_raw_nn_entry. fs_h_mcp_ics_span_negative_result_image_raw_nn_entry + S (ff_value_mcp_prefix_ics_span_negative_result_image_raw_nn) = S ((S (ff_index_mcp_prefix_ics_span_negative_result_image_raw_nn)) * ff_nns_mcp_smatrix_ics_span_negative_result_image_raw)) /\ exists fs_q_mcp_ics_span_negative_result_image_raw_nn_entry. ff_nn_mcp_smatrix_ics_span_negative_result_image_raw = fs_q_mcp_ics_span_negative_result_image_raw_nn_entry * S ((S (ff_index_mcp_prefix_ics_span_negative_result_image_raw_nn)) * ff_nns_mcp_smatrix_ics_span_negative_result_image_raw) + (ff_value_mcp_prefix_ics_span_negative_result_image_raw_nn))))))) /\ ((forall ff_index_mcp_prefix_ics_span_negative_result_image_raw_pn. (exists mcp_gap_ics_span_negative_result_image_raw_pn_index. mcp_gap_ics_span_negative_result_image_raw_pn_index + S (ff_index_mcp_prefix_ics_span_negative_result_image_raw_pn) = ((r) * (1))) -> exists ff_row_mcp_prefix_ics_span_negative_result_image_raw_pn ff_column_mcp_prefix_ics_span_negative_result_image_raw_pn ff_value_mcp_prefix_ics_span_negative_result_image_raw_pn. ((ff_index_mcp_prefix_ics_span_negative_result_image_raw_pn) = (1) * ff_row_mcp_prefix_ics_span_negative_result_image_raw_pn + ff_column_mcp_prefix_ics_span_negative_result_image_raw_pn /\ ((exists mcp_gap_ics_span_negative_result_image_raw_pn_column. mcp_gap_ics_span_negative_result_image_raw_pn_column + S (ff_column_mcp_prefix_ics_span_negative_result_image_raw_pn) = (1)) /\ ((exists ff_left_mcp_cell_ics_span_negative_result_image_raw_pn_cell ff_left_scale_mcp_cell_ics_span_negative_result_image_raw_pn_cell ff_right_mcp_cell_ics_span_negative_result_image_raw_pn_cell ff_right_scale_mcp_cell_ics_span_negative_result_image_raw_pn_cell. ((forall ff_index_mcp_ics_span_negative_result_image_raw_pn_cell_row ff_source_mcp_ics_span_negative_result_image_raw_pn_cell_row ff_target_mcp_ics_span_negative_result_image_raw_pn_cell_row. (exists mcp_gap_ics_span_negative_result_image_raw_pn_cell_row_bound. mcp_gap_ics_span_negative_result_image_raw_pn_cell_row_bound + S (ff_index_mcp_ics_span_negative_result_image_raw_pn_cell_row) = (w)) -> (((exists fs_h_mcp_ics_span_negative_result_image_raw_pn_cell_row_source. fs_h_mcp_ics_span_negative_result_image_raw_pn_cell_row_source + S (ff_source_mcp_ics_span_negative_result_image_raw_pn_cell_row) = S ((S (((ff_row_mcp_prefix_ics_span_negative_result_image_raw_pn) * (w)) + (1) * ff_index_mcp_ics_span_negative_result_image_raw_pn_cell_row)) * ac)) /\ exists fs_q_mcp_ics_span_negative_result_image_raw_pn_cell_row_source. ab = fs_q_mcp_ics_span_negative_result_image_raw_pn_cell_row_source * S ((S (((ff_row_mcp_prefix_ics_span_negative_result_image_raw_pn) * (w)) + (1) * ff_index_mcp_ics_span_negative_result_image_raw_pn_cell_row)) * ac) + (ff_source_mcp_ics_span_negative_result_image_raw_pn_cell_row))) -> (((exists fs_h_mcp_ics_span_negative_result_image_raw_pn_cell_row_target. fs_h_mcp_ics_span_negative_result_image_raw_pn_cell_row_target + S (ff_target_mcp_ics_span_negative_result_image_raw_pn_cell_row) = S ((S (ff_index_mcp_ics_span_negative_result_image_raw_pn_cell_row)) * ff_left_scale_mcp_cell_ics_span_negative_result_image_raw_pn_cell)) /\ exists fs_q_mcp_ics_span_negative_result_image_raw_pn_cell_row_target. ff_left_mcp_cell_ics_span_negative_result_image_raw_pn_cell = fs_q_mcp_ics_span_negative_result_image_raw_pn_cell_row_target * S ((S (ff_index_mcp_ics_span_negative_result_image_raw_pn_cell_row)) * ff_left_scale_mcp_cell_ics_span_negative_result_image_raw_pn_cell) + (ff_target_mcp_ics_span_negative_result_image_raw_pn_cell_row))) -> ff_target_mcp_ics_span_negative_result_image_raw_pn_cell_row = ff_source_mcp_ics_span_negative_result_image_raw_pn_cell_row) /\ ((forall ff_index_mcp_ics_span_negative_result_image_raw_pn_cell_column ff_source_mcp_ics_span_negative_result_image_raw_pn_cell_column ff_target_mcp_ics_span_negative_result_image_raw_pn_cell_column. (exists mcp_gap_ics_span_negative_result_image_raw_pn_cell_column_bound. mcp_gap_ics_span_negative_result_image_raw_pn_cell_column_bound + S (ff_index_mcp_ics_span_negative_result_image_raw_pn_cell_column) = (w)) -> (((exists fs_h_mcp_ics_span_negative_result_image_raw_pn_cell_column_source. fs_h_mcp_ics_span_negative_result_image_raw_pn_cell_column_source + S (ff_source_mcp_ics_span_negative_result_image_raw_pn_cell_column) = S ((S ((ff_column_mcp_prefix_ics_span_negative_result_image_raw_pn) + (1) * ff_index_mcp_ics_span_negative_result_image_raw_pn_cell_column)) * ics_coefficient_negative_scale_span_negative_result)) /\ exists fs_q_mcp_ics_span_negative_result_image_raw_pn_cell_column_source. ics_coefficient_negative_span_negative_result = fs_q_mcp_ics_span_negative_result_image_raw_pn_cell_column_source * S ((S ((ff_column_mcp_prefix_ics_span_negative_result_image_raw_pn) + (1) * ff_index_mcp_ics_span_negative_result_image_raw_pn_cell_column)) * ics_coefficient_negative_scale_span_negative_result) + (ff_source_mcp_ics_span_negative_result_image_raw_pn_cell_column))) -> (((exists fs_h_mcp_ics_span_negative_result_image_raw_pn_cell_column_target. fs_h_mcp_ics_span_negative_result_image_raw_pn_cell_column_target + S (ff_target_mcp_ics_span_negative_result_image_raw_pn_cell_column) = S ((S (ff_index_mcp_ics_span_negative_result_image_raw_pn_cell_column)) * ff_right_scale_mcp_cell_ics_span_negative_result_image_raw_pn_cell)) /\ exists fs_q_mcp_ics_span_negative_result_image_raw_pn_cell_column_target. ff_right_mcp_cell_ics_span_negative_result_image_raw_pn_cell = fs_q_mcp_ics_span_negative_result_image_raw_pn_cell_column_target * S ((S (ff_index_mcp_ics_span_negative_result_image_raw_pn_cell_column)) * ff_right_scale_mcp_cell_ics_span_negative_result_image_raw_pn_cell) + (ff_target_mcp_ics_span_negative_result_image_raw_pn_cell_column))) -> ff_target_mcp_ics_span_negative_result_image_raw_pn_cell_column = ff_source_mcp_ics_span_negative_result_image_raw_pn_cell_column) /\ (exists ff_code_dot_mcp_ics_span_negative_result_image_raw_pn_cell_dot ff_scale_dot_mcp_ics_span_negative_result_image_raw_pn_cell_dot. ((forall fpmp_index_dot_mcp_ics_span_negative_result_image_raw_pn_cell_dot_pointwise fpmp_left_dot_mcp_ics_span_negative_result_image_raw_pn_cell_dot_pointwise fpmp_right_dot_mcp_ics_span_negative_result_image_raw_pn_cell_dot_pointwise fpmp_target_dot_mcp_ics_span_negative_result_image_raw_pn_cell_dot_pointwise. (exists fpmp_gap_dot_mcp_ics_span_negative_result_image_raw_pn_cell_dot_pointwise. fpmp_gap_dot_mcp_ics_span_negative_result_image_raw_pn_cell_dot_pointwise + S fpmp_index_dot_mcp_ics_span_negative_result_image_raw_pn_cell_dot_pointwise = w) -> (((exists ff_h_fpmp_dot_mcp_ics_span_negative_result_image_raw_pn_cell_dot_pointwise_left. ff_h_fpmp_dot_mcp_ics_span_negative_result_image_raw_pn_cell_dot_pointwise_left + S (fpmp_left_dot_mcp_ics_span_negative_result_image_raw_pn_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_span_negative_result_image_raw_pn_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_span_negative_result_image_raw_pn_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_span_negative_result_image_raw_pn_cell_dot_pointwise_left. ff_left_mcp_cell_ics_span_negative_result_image_raw_pn_cell = ff_q_fpmp_dot_mcp_ics_span_negative_result_image_raw_pn_cell_dot_pointwise_left * S ((S (fpmp_index_dot_mcp_ics_span_negative_result_image_raw_pn_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_span_negative_result_image_raw_pn_cell) + (fpmp_left_dot_mcp_ics_span_negative_result_image_raw_pn_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_span_negative_result_image_raw_pn_cell_dot_pointwise_right. ff_h_fpmp_dot_mcp_ics_span_negative_result_image_raw_pn_cell_dot_pointwise_right + S (fpmp_right_dot_mcp_ics_span_negative_result_image_raw_pn_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_span_negative_result_image_raw_pn_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_span_negative_result_image_raw_pn_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_span_negative_result_image_raw_pn_cell_dot_pointwise_right. ff_right_mcp_cell_ics_span_negative_result_image_raw_pn_cell = ff_q_fpmp_dot_mcp_ics_span_negative_result_image_raw_pn_cell_dot_pointwise_right * S ((S (fpmp_index_dot_mcp_ics_span_negative_result_image_raw_pn_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_span_negative_result_image_raw_pn_cell) + (fpmp_right_dot_mcp_ics_span_negative_result_image_raw_pn_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_span_negative_result_image_raw_pn_cell_dot_pointwise_target. ff_h_fpmp_dot_mcp_ics_span_negative_result_image_raw_pn_cell_dot_pointwise_target + S (fpmp_target_dot_mcp_ics_span_negative_result_image_raw_pn_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_span_negative_result_image_raw_pn_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_span_negative_result_image_raw_pn_cell_dot)) /\ exists ff_q_fpmp_dot_mcp_ics_span_negative_result_image_raw_pn_cell_dot_pointwise_target. ff_code_dot_mcp_ics_span_negative_result_image_raw_pn_cell_dot = ff_q_fpmp_dot_mcp_ics_span_negative_result_image_raw_pn_cell_dot_pointwise_target * S ((S (fpmp_index_dot_mcp_ics_span_negative_result_image_raw_pn_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_span_negative_result_image_raw_pn_cell_dot) + (fpmp_target_dot_mcp_ics_span_negative_result_image_raw_pn_cell_dot_pointwise))) -> fpmp_target_dot_mcp_ics_span_negative_result_image_raw_pn_cell_dot_pointwise = fpmp_left_dot_mcp_ics_span_negative_result_image_raw_pn_cell_dot_pointwise * fpmp_right_dot_mcp_ics_span_negative_result_image_raw_pn_cell_dot_pointwise) /\ (exists ff_u_dot_mcp_ics_span_negative_result_image_raw_pn_cell_dot_sum ff_v_dot_mcp_ics_span_negative_result_image_raw_pn_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_span_negative_result_image_raw_pn_cell_dot_sum_start. ff_h_dot_mcp_ics_span_negative_result_image_raw_pn_cell_dot_sum_start + S (0) = S ((S (0)) * ff_v_dot_mcp_ics_span_negative_result_image_raw_pn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_span_negative_result_image_raw_pn_cell_dot_sum_start. ff_u_dot_mcp_ics_span_negative_result_image_raw_pn_cell_dot_sum = ff_q_dot_mcp_ics_span_negative_result_image_raw_pn_cell_dot_sum_start * S ((S (0)) * ff_v_dot_mcp_ics_span_negative_result_image_raw_pn_cell_dot_sum) + (0))) /\ ((((exists ff_h_dot_mcp_ics_span_negative_result_image_raw_pn_cell_dot_sum_terminal. ff_h_dot_mcp_ics_span_negative_result_image_raw_pn_cell_dot_sum_terminal + S (ff_value_mcp_prefix_ics_span_negative_result_image_raw_pn) = S ((S (w)) * ff_v_dot_mcp_ics_span_negative_result_image_raw_pn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_span_negative_result_image_raw_pn_cell_dot_sum_terminal. ff_u_dot_mcp_ics_span_negative_result_image_raw_pn_cell_dot_sum = ff_q_dot_mcp_ics_span_negative_result_image_raw_pn_cell_dot_sum_terminal * S ((S (w)) * ff_v_dot_mcp_ics_span_negative_result_image_raw_pn_cell_dot_sum) + (ff_value_mcp_prefix_ics_span_negative_result_image_raw_pn))) /\ forall ff_i_dot_mcp_ics_span_negative_result_image_raw_pn_cell_dot_sum. (exists ff_lt_dot_mcp_ics_span_negative_result_image_raw_pn_cell_dot_sum_bound. ff_lt_dot_mcp_ics_span_negative_result_image_raw_pn_cell_dot_sum_bound + S ff_i_dot_mcp_ics_span_negative_result_image_raw_pn_cell_dot_sum = w) -> exists ff_a_dot_mcp_ics_span_negative_result_image_raw_pn_cell_dot_sum ff_r_dot_mcp_ics_span_negative_result_image_raw_pn_cell_dot_sum ff_s_dot_mcp_ics_span_negative_result_image_raw_pn_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_span_negative_result_image_raw_pn_cell_dot_sum_summand. ff_h_dot_mcp_ics_span_negative_result_image_raw_pn_cell_dot_sum_summand + S (ff_a_dot_mcp_ics_span_negative_result_image_raw_pn_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_span_negative_result_image_raw_pn_cell_dot_sum)) * ff_scale_dot_mcp_ics_span_negative_result_image_raw_pn_cell_dot)) /\ exists ff_q_dot_mcp_ics_span_negative_result_image_raw_pn_cell_dot_sum_summand. ff_code_dot_mcp_ics_span_negative_result_image_raw_pn_cell_dot = ff_q_dot_mcp_ics_span_negative_result_image_raw_pn_cell_dot_sum_summand * S ((S (ff_i_dot_mcp_ics_span_negative_result_image_raw_pn_cell_dot_sum)) * ff_scale_dot_mcp_ics_span_negative_result_image_raw_pn_cell_dot) + (ff_a_dot_mcp_ics_span_negative_result_image_raw_pn_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_span_negative_result_image_raw_pn_cell_dot_sum_partial. ff_h_dot_mcp_ics_span_negative_result_image_raw_pn_cell_dot_sum_partial + S (ff_r_dot_mcp_ics_span_negative_result_image_raw_pn_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_span_negative_result_image_raw_pn_cell_dot_sum)) * ff_v_dot_mcp_ics_span_negative_result_image_raw_pn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_span_negative_result_image_raw_pn_cell_dot_sum_partial. ff_u_dot_mcp_ics_span_negative_result_image_raw_pn_cell_dot_sum = ff_q_dot_mcp_ics_span_negative_result_image_raw_pn_cell_dot_sum_partial * S ((S (ff_i_dot_mcp_ics_span_negative_result_image_raw_pn_cell_dot_sum)) * ff_v_dot_mcp_ics_span_negative_result_image_raw_pn_cell_dot_sum) + (ff_r_dot_mcp_ics_span_negative_result_image_raw_pn_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_span_negative_result_image_raw_pn_cell_dot_sum_successor. ff_h_dot_mcp_ics_span_negative_result_image_raw_pn_cell_dot_sum_successor + S (ff_s_dot_mcp_ics_span_negative_result_image_raw_pn_cell_dot_sum) = S ((S (S ff_i_dot_mcp_ics_span_negative_result_image_raw_pn_cell_dot_sum)) * ff_v_dot_mcp_ics_span_negative_result_image_raw_pn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_span_negative_result_image_raw_pn_cell_dot_sum_successor. ff_u_dot_mcp_ics_span_negative_result_image_raw_pn_cell_dot_sum = ff_q_dot_mcp_ics_span_negative_result_image_raw_pn_cell_dot_sum_successor * S ((S (S ff_i_dot_mcp_ics_span_negative_result_image_raw_pn_cell_dot_sum)) * ff_v_dot_mcp_ics_span_negative_result_image_raw_pn_cell_dot_sum) + (ff_s_dot_mcp_ics_span_negative_result_image_raw_pn_cell_dot_sum))) /\ ff_s_dot_mcp_ics_span_negative_result_image_raw_pn_cell_dot_sum = ff_r_dot_mcp_ics_span_negative_result_image_raw_pn_cell_dot_sum + ff_a_dot_mcp_ics_span_negative_result_image_raw_pn_cell_dot_sum))))))))))) /\ (((exists fs_h_mcp_ics_span_negative_result_image_raw_pn_entry. fs_h_mcp_ics_span_negative_result_image_raw_pn_entry + S (ff_value_mcp_prefix_ics_span_negative_result_image_raw_pn) = S ((S (ff_index_mcp_prefix_ics_span_negative_result_image_raw_pn)) * ff_pns_mcp_smatrix_ics_span_negative_result_image_raw)) /\ exists fs_q_mcp_ics_span_negative_result_image_raw_pn_entry. ff_pn_mcp_smatrix_ics_span_negative_result_image_raw = fs_q_mcp_ics_span_negative_result_image_raw_pn_entry * S ((S (ff_index_mcp_prefix_ics_span_negative_result_image_raw_pn)) * ff_pns_mcp_smatrix_ics_span_negative_result_image_raw) + (ff_value_mcp_prefix_ics_span_negative_result_image_raw_pn))))))) /\ ((forall ff_index_mcp_prefix_ics_span_negative_result_image_raw_np. (exists mcp_gap_ics_span_negative_result_image_raw_np_index. mcp_gap_ics_span_negative_result_image_raw_np_index + S (ff_index_mcp_prefix_ics_span_negative_result_image_raw_np) = ((r) * (1))) -> exists ff_row_mcp_prefix_ics_span_negative_result_image_raw_np ff_column_mcp_prefix_ics_span_negative_result_image_raw_np ff_value_mcp_prefix_ics_span_negative_result_image_raw_np. ((ff_index_mcp_prefix_ics_span_negative_result_image_raw_np) = (1) * ff_row_mcp_prefix_ics_span_negative_result_image_raw_np + ff_column_mcp_prefix_ics_span_negative_result_image_raw_np /\ ((exists mcp_gap_ics_span_negative_result_image_raw_np_column. mcp_gap_ics_span_negative_result_image_raw_np_column + S (ff_column_mcp_prefix_ics_span_negative_result_image_raw_np) = (1)) /\ ((exists ff_left_mcp_cell_ics_span_negative_result_image_raw_np_cell ff_left_scale_mcp_cell_ics_span_negative_result_image_raw_np_cell ff_right_mcp_cell_ics_span_negative_result_image_raw_np_cell ff_right_scale_mcp_cell_ics_span_negative_result_image_raw_np_cell. ((forall ff_index_mcp_ics_span_negative_result_image_raw_np_cell_row ff_source_mcp_ics_span_negative_result_image_raw_np_cell_row ff_target_mcp_ics_span_negative_result_image_raw_np_cell_row. (exists mcp_gap_ics_span_negative_result_image_raw_np_cell_row_bound. mcp_gap_ics_span_negative_result_image_raw_np_cell_row_bound + S (ff_index_mcp_ics_span_negative_result_image_raw_np_cell_row) = (w)) -> (((exists fs_h_mcp_ics_span_negative_result_image_raw_np_cell_row_source. fs_h_mcp_ics_span_negative_result_image_raw_np_cell_row_source + S (ff_source_mcp_ics_span_negative_result_image_raw_np_cell_row) = S ((S (((ff_row_mcp_prefix_ics_span_negative_result_image_raw_np) * (w)) + (1) * ff_index_mcp_ics_span_negative_result_image_raw_np_cell_row)) * dc)) /\ exists fs_q_mcp_ics_span_negative_result_image_raw_np_cell_row_source. db = fs_q_mcp_ics_span_negative_result_image_raw_np_cell_row_source * S ((S (((ff_row_mcp_prefix_ics_span_negative_result_image_raw_np) * (w)) + (1) * ff_index_mcp_ics_span_negative_result_image_raw_np_cell_row)) * dc) + (ff_source_mcp_ics_span_negative_result_image_raw_np_cell_row))) -> (((exists fs_h_mcp_ics_span_negative_result_image_raw_np_cell_row_target. fs_h_mcp_ics_span_negative_result_image_raw_np_cell_row_target + S (ff_target_mcp_ics_span_negative_result_image_raw_np_cell_row) = S ((S (ff_index_mcp_ics_span_negative_result_image_raw_np_cell_row)) * ff_left_scale_mcp_cell_ics_span_negative_result_image_raw_np_cell)) /\ exists fs_q_mcp_ics_span_negative_result_image_raw_np_cell_row_target. ff_left_mcp_cell_ics_span_negative_result_image_raw_np_cell = fs_q_mcp_ics_span_negative_result_image_raw_np_cell_row_target * S ((S (ff_index_mcp_ics_span_negative_result_image_raw_np_cell_row)) * ff_left_scale_mcp_cell_ics_span_negative_result_image_raw_np_cell) + (ff_target_mcp_ics_span_negative_result_image_raw_np_cell_row))) -> ff_target_mcp_ics_span_negative_result_image_raw_np_cell_row = ff_source_mcp_ics_span_negative_result_image_raw_np_cell_row) /\ ((forall ff_index_mcp_ics_span_negative_result_image_raw_np_cell_column ff_source_mcp_ics_span_negative_result_image_raw_np_cell_column ff_target_mcp_ics_span_negative_result_image_raw_np_cell_column. (exists mcp_gap_ics_span_negative_result_image_raw_np_cell_column_bound. mcp_gap_ics_span_negative_result_image_raw_np_cell_column_bound + S (ff_index_mcp_ics_span_negative_result_image_raw_np_cell_column) = (w)) -> (((exists fs_h_mcp_ics_span_negative_result_image_raw_np_cell_column_source. fs_h_mcp_ics_span_negative_result_image_raw_np_cell_column_source + S (ff_source_mcp_ics_span_negative_result_image_raw_np_cell_column) = S ((S ((ff_column_mcp_prefix_ics_span_negative_result_image_raw_np) + (1) * ff_index_mcp_ics_span_negative_result_image_raw_np_cell_column)) * ics_coefficient_positive_scale_span_negative_result)) /\ exists fs_q_mcp_ics_span_negative_result_image_raw_np_cell_column_source. ics_coefficient_positive_span_negative_result = fs_q_mcp_ics_span_negative_result_image_raw_np_cell_column_source * S ((S ((ff_column_mcp_prefix_ics_span_negative_result_image_raw_np) + (1) * ff_index_mcp_ics_span_negative_result_image_raw_np_cell_column)) * ics_coefficient_positive_scale_span_negative_result) + (ff_source_mcp_ics_span_negative_result_image_raw_np_cell_column))) -> (((exists fs_h_mcp_ics_span_negative_result_image_raw_np_cell_column_target. fs_h_mcp_ics_span_negative_result_image_raw_np_cell_column_target + S (ff_target_mcp_ics_span_negative_result_image_raw_np_cell_column) = S ((S (ff_index_mcp_ics_span_negative_result_image_raw_np_cell_column)) * ff_right_scale_mcp_cell_ics_span_negative_result_image_raw_np_cell)) /\ exists fs_q_mcp_ics_span_negative_result_image_raw_np_cell_column_target. ff_right_mcp_cell_ics_span_negative_result_image_raw_np_cell = fs_q_mcp_ics_span_negative_result_image_raw_np_cell_column_target * S ((S (ff_index_mcp_ics_span_negative_result_image_raw_np_cell_column)) * ff_right_scale_mcp_cell_ics_span_negative_result_image_raw_np_cell) + (ff_target_mcp_ics_span_negative_result_image_raw_np_cell_column))) -> ff_target_mcp_ics_span_negative_result_image_raw_np_cell_column = ff_source_mcp_ics_span_negative_result_image_raw_np_cell_column) /\ (exists ff_code_dot_mcp_ics_span_negative_result_image_raw_np_cell_dot ff_scale_dot_mcp_ics_span_negative_result_image_raw_np_cell_dot. ((forall fpmp_index_dot_mcp_ics_span_negative_result_image_raw_np_cell_dot_pointwise fpmp_left_dot_mcp_ics_span_negative_result_image_raw_np_cell_dot_pointwise fpmp_right_dot_mcp_ics_span_negative_result_image_raw_np_cell_dot_pointwise fpmp_target_dot_mcp_ics_span_negative_result_image_raw_np_cell_dot_pointwise. (exists fpmp_gap_dot_mcp_ics_span_negative_result_image_raw_np_cell_dot_pointwise. fpmp_gap_dot_mcp_ics_span_negative_result_image_raw_np_cell_dot_pointwise + S fpmp_index_dot_mcp_ics_span_negative_result_image_raw_np_cell_dot_pointwise = w) -> (((exists ff_h_fpmp_dot_mcp_ics_span_negative_result_image_raw_np_cell_dot_pointwise_left. ff_h_fpmp_dot_mcp_ics_span_negative_result_image_raw_np_cell_dot_pointwise_left + S (fpmp_left_dot_mcp_ics_span_negative_result_image_raw_np_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_span_negative_result_image_raw_np_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_span_negative_result_image_raw_np_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_span_negative_result_image_raw_np_cell_dot_pointwise_left. ff_left_mcp_cell_ics_span_negative_result_image_raw_np_cell = ff_q_fpmp_dot_mcp_ics_span_negative_result_image_raw_np_cell_dot_pointwise_left * S ((S (fpmp_index_dot_mcp_ics_span_negative_result_image_raw_np_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_span_negative_result_image_raw_np_cell) + (fpmp_left_dot_mcp_ics_span_negative_result_image_raw_np_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_span_negative_result_image_raw_np_cell_dot_pointwise_right. ff_h_fpmp_dot_mcp_ics_span_negative_result_image_raw_np_cell_dot_pointwise_right + S (fpmp_right_dot_mcp_ics_span_negative_result_image_raw_np_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_span_negative_result_image_raw_np_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_span_negative_result_image_raw_np_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_span_negative_result_image_raw_np_cell_dot_pointwise_right. ff_right_mcp_cell_ics_span_negative_result_image_raw_np_cell = ff_q_fpmp_dot_mcp_ics_span_negative_result_image_raw_np_cell_dot_pointwise_right * S ((S (fpmp_index_dot_mcp_ics_span_negative_result_image_raw_np_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_span_negative_result_image_raw_np_cell) + (fpmp_right_dot_mcp_ics_span_negative_result_image_raw_np_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_span_negative_result_image_raw_np_cell_dot_pointwise_target. ff_h_fpmp_dot_mcp_ics_span_negative_result_image_raw_np_cell_dot_pointwise_target + S (fpmp_target_dot_mcp_ics_span_negative_result_image_raw_np_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_span_negative_result_image_raw_np_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_span_negative_result_image_raw_np_cell_dot)) /\ exists ff_q_fpmp_dot_mcp_ics_span_negative_result_image_raw_np_cell_dot_pointwise_target. ff_code_dot_mcp_ics_span_negative_result_image_raw_np_cell_dot = ff_q_fpmp_dot_mcp_ics_span_negative_result_image_raw_np_cell_dot_pointwise_target * S ((S (fpmp_index_dot_mcp_ics_span_negative_result_image_raw_np_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_span_negative_result_image_raw_np_cell_dot) + (fpmp_target_dot_mcp_ics_span_negative_result_image_raw_np_cell_dot_pointwise))) -> fpmp_target_dot_mcp_ics_span_negative_result_image_raw_np_cell_dot_pointwise = fpmp_left_dot_mcp_ics_span_negative_result_image_raw_np_cell_dot_pointwise * fpmp_right_dot_mcp_ics_span_negative_result_image_raw_np_cell_dot_pointwise) /\ (exists ff_u_dot_mcp_ics_span_negative_result_image_raw_np_cell_dot_sum ff_v_dot_mcp_ics_span_negative_result_image_raw_np_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_span_negative_result_image_raw_np_cell_dot_sum_start. ff_h_dot_mcp_ics_span_negative_result_image_raw_np_cell_dot_sum_start + S (0) = S ((S (0)) * ff_v_dot_mcp_ics_span_negative_result_image_raw_np_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_span_negative_result_image_raw_np_cell_dot_sum_start. ff_u_dot_mcp_ics_span_negative_result_image_raw_np_cell_dot_sum = ff_q_dot_mcp_ics_span_negative_result_image_raw_np_cell_dot_sum_start * S ((S (0)) * ff_v_dot_mcp_ics_span_negative_result_image_raw_np_cell_dot_sum) + (0))) /\ ((((exists ff_h_dot_mcp_ics_span_negative_result_image_raw_np_cell_dot_sum_terminal. ff_h_dot_mcp_ics_span_negative_result_image_raw_np_cell_dot_sum_terminal + S (ff_value_mcp_prefix_ics_span_negative_result_image_raw_np) = S ((S (w)) * ff_v_dot_mcp_ics_span_negative_result_image_raw_np_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_span_negative_result_image_raw_np_cell_dot_sum_terminal. ff_u_dot_mcp_ics_span_negative_result_image_raw_np_cell_dot_sum = ff_q_dot_mcp_ics_span_negative_result_image_raw_np_cell_dot_sum_terminal * S ((S (w)) * ff_v_dot_mcp_ics_span_negative_result_image_raw_np_cell_dot_sum) + (ff_value_mcp_prefix_ics_span_negative_result_image_raw_np))) /\ forall ff_i_dot_mcp_ics_span_negative_result_image_raw_np_cell_dot_sum. (exists ff_lt_dot_mcp_ics_span_negative_result_image_raw_np_cell_dot_sum_bound. ff_lt_dot_mcp_ics_span_negative_result_image_raw_np_cell_dot_sum_bound + S ff_i_dot_mcp_ics_span_negative_result_image_raw_np_cell_dot_sum = w) -> exists ff_a_dot_mcp_ics_span_negative_result_image_raw_np_cell_dot_sum ff_r_dot_mcp_ics_span_negative_result_image_raw_np_cell_dot_sum ff_s_dot_mcp_ics_span_negative_result_image_raw_np_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_span_negative_result_image_raw_np_cell_dot_sum_summand. ff_h_dot_mcp_ics_span_negative_result_image_raw_np_cell_dot_sum_summand + S (ff_a_dot_mcp_ics_span_negative_result_image_raw_np_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_span_negative_result_image_raw_np_cell_dot_sum)) * ff_scale_dot_mcp_ics_span_negative_result_image_raw_np_cell_dot)) /\ exists ff_q_dot_mcp_ics_span_negative_result_image_raw_np_cell_dot_sum_summand. ff_code_dot_mcp_ics_span_negative_result_image_raw_np_cell_dot = ff_q_dot_mcp_ics_span_negative_result_image_raw_np_cell_dot_sum_summand * S ((S (ff_i_dot_mcp_ics_span_negative_result_image_raw_np_cell_dot_sum)) * ff_scale_dot_mcp_ics_span_negative_result_image_raw_np_cell_dot) + (ff_a_dot_mcp_ics_span_negative_result_image_raw_np_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_span_negative_result_image_raw_np_cell_dot_sum_partial. ff_h_dot_mcp_ics_span_negative_result_image_raw_np_cell_dot_sum_partial + S (ff_r_dot_mcp_ics_span_negative_result_image_raw_np_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_span_negative_result_image_raw_np_cell_dot_sum)) * ff_v_dot_mcp_ics_span_negative_result_image_raw_np_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_span_negative_result_image_raw_np_cell_dot_sum_partial. ff_u_dot_mcp_ics_span_negative_result_image_raw_np_cell_dot_sum = ff_q_dot_mcp_ics_span_negative_result_image_raw_np_cell_dot_sum_partial * S ((S (ff_i_dot_mcp_ics_span_negative_result_image_raw_np_cell_dot_sum)) * ff_v_dot_mcp_ics_span_negative_result_image_raw_np_cell_dot_sum) + (ff_r_dot_mcp_ics_span_negative_result_image_raw_np_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_span_negative_result_image_raw_np_cell_dot_sum_successor. ff_h_dot_mcp_ics_span_negative_result_image_raw_np_cell_dot_sum_successor + S (ff_s_dot_mcp_ics_span_negative_result_image_raw_np_cell_dot_sum) = S ((S (S ff_i_dot_mcp_ics_span_negative_result_image_raw_np_cell_dot_sum)) * ff_v_dot_mcp_ics_span_negative_result_image_raw_np_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_span_negative_result_image_raw_np_cell_dot_sum_successor. ff_u_dot_mcp_ics_span_negative_result_image_raw_np_cell_dot_sum = ff_q_dot_mcp_ics_span_negative_result_image_raw_np_cell_dot_sum_successor * S ((S (S ff_i_dot_mcp_ics_span_negative_result_image_raw_np_cell_dot_sum)) * ff_v_dot_mcp_ics_span_negative_result_image_raw_np_cell_dot_sum) + (ff_s_dot_mcp_ics_span_negative_result_image_raw_np_cell_dot_sum))) /\ ff_s_dot_mcp_ics_span_negative_result_image_raw_np_cell_dot_sum = ff_r_dot_mcp_ics_span_negative_result_image_raw_np_cell_dot_sum + ff_a_dot_mcp_ics_span_negative_result_image_raw_np_cell_dot_sum))))))))))) /\ (((exists fs_h_mcp_ics_span_negative_result_image_raw_np_entry. fs_h_mcp_ics_span_negative_result_image_raw_np_entry + S (ff_value_mcp_prefix_ics_span_negative_result_image_raw_np) = S ((S (ff_index_mcp_prefix_ics_span_negative_result_image_raw_np)) * ff_nps_mcp_smatrix_ics_span_negative_result_image_raw)) /\ exists fs_q_mcp_ics_span_negative_result_image_raw_np_entry. ff_np_mcp_smatrix_ics_span_negative_result_image_raw = fs_q_mcp_ics_span_negative_result_image_raw_np_entry * S ((S (ff_index_mcp_prefix_ics_span_negative_result_image_raw_np)) * ff_nps_mcp_smatrix_ics_span_negative_result_image_raw) + (ff_value_mcp_prefix_ics_span_negative_result_image_raw_np))))))) /\ ((forall ff_index_mcp_add_ics_span_negative_result_image_raw_positive ff_left_mcp_add_ics_span_negative_result_image_raw_positive ff_right_mcp_add_ics_span_negative_result_image_raw_positive ff_target_mcp_add_ics_span_negative_result_image_raw_positive. (exists mcp_gap_ics_span_negative_result_image_raw_positive_bound. mcp_gap_ics_span_negative_result_image_raw_positive_bound + S (ff_index_mcp_add_ics_span_negative_result_image_raw_positive) = ((r) * (1))) -> (((exists fs_h_mcp_ics_span_negative_result_image_raw_positive_left. fs_h_mcp_ics_span_negative_result_image_raw_positive_left + S (ff_left_mcp_add_ics_span_negative_result_image_raw_positive) = S ((S (ff_index_mcp_add_ics_span_negative_result_image_raw_positive)) * ff_pps_mcp_smatrix_ics_span_negative_result_image_raw)) /\ exists fs_q_mcp_ics_span_negative_result_image_raw_positive_left. ff_pp_mcp_smatrix_ics_span_negative_result_image_raw = fs_q_mcp_ics_span_negative_result_image_raw_positive_left * S ((S (ff_index_mcp_add_ics_span_negative_result_image_raw_positive)) * ff_pps_mcp_smatrix_ics_span_negative_result_image_raw) + (ff_left_mcp_add_ics_span_negative_result_image_raw_positive))) -> (((exists fs_h_mcp_ics_span_negative_result_image_raw_positive_right. fs_h_mcp_ics_span_negative_result_image_raw_positive_right + S (ff_right_mcp_add_ics_span_negative_result_image_raw_positive) = S ((S (ff_index_mcp_add_ics_span_negative_result_image_raw_positive)) * ff_nns_mcp_smatrix_ics_span_negative_result_image_raw)) /\ exists fs_q_mcp_ics_span_negative_result_image_raw_positive_right. ff_nn_mcp_smatrix_ics_span_negative_result_image_raw = fs_q_mcp_ics_span_negative_result_image_raw_positive_right * S ((S (ff_index_mcp_add_ics_span_negative_result_image_raw_positive)) * ff_nns_mcp_smatrix_ics_span_negative_result_image_raw) + (ff_right_mcp_add_ics_span_negative_result_image_raw_positive))) -> (((exists fs_h_mcp_ics_span_negative_result_image_raw_positive_target. fs_h_mcp_ics_span_negative_result_image_raw_positive_target + S (ff_target_mcp_add_ics_span_negative_result_image_raw_positive) = S ((S (ff_index_mcp_add_ics_span_negative_result_image_raw_positive)) * ics_raw_positive_scale_span_negative_result_image)) /\ exists fs_q_mcp_ics_span_negative_result_image_raw_positive_target. ics_raw_positive_span_negative_result_image = fs_q_mcp_ics_span_negative_result_image_raw_positive_target * S ((S (ff_index_mcp_add_ics_span_negative_result_image_raw_positive)) * ics_raw_positive_scale_span_negative_result_image) + (ff_target_mcp_add_ics_span_negative_result_image_raw_positive))) -> ff_target_mcp_add_ics_span_negative_result_image_raw_positive = ff_left_mcp_add_ics_span_negative_result_image_raw_positive + ff_right_mcp_add_ics_span_negative_result_image_raw_positive) /\ (forall ff_index_mcp_add_ics_span_negative_result_image_raw_negative ff_left_mcp_add_ics_span_negative_result_image_raw_negative ff_right_mcp_add_ics_span_negative_result_image_raw_negative ff_target_mcp_add_ics_span_negative_result_image_raw_negative. (exists mcp_gap_ics_span_negative_result_image_raw_negative_bound. mcp_gap_ics_span_negative_result_image_raw_negative_bound + S (ff_index_mcp_add_ics_span_negative_result_image_raw_negative) = ((r) * (1))) -> (((exists fs_h_mcp_ics_span_negative_result_image_raw_negative_left. fs_h_mcp_ics_span_negative_result_image_raw_negative_left + S (ff_left_mcp_add_ics_span_negative_result_image_raw_negative) = S ((S (ff_index_mcp_add_ics_span_negative_result_image_raw_negative)) * ff_pns_mcp_smatrix_ics_span_negative_result_image_raw)) /\ exists fs_q_mcp_ics_span_negative_result_image_raw_negative_left. ff_pn_mcp_smatrix_ics_span_negative_result_image_raw = fs_q_mcp_ics_span_negative_result_image_raw_negative_left * S ((S (ff_index_mcp_add_ics_span_negative_result_image_raw_negative)) * ff_pns_mcp_smatrix_ics_span_negative_result_image_raw) + (ff_left_mcp_add_ics_span_negative_result_image_raw_negative))) -> (((exists fs_h_mcp_ics_span_negative_result_image_raw_negative_right. fs_h_mcp_ics_span_negative_result_image_raw_negative_right + S (ff_right_mcp_add_ics_span_negative_result_image_raw_negative) = S ((S (ff_index_mcp_add_ics_span_negative_result_image_raw_negative)) * ff_nps_mcp_smatrix_ics_span_negative_result_image_raw)) /\ exists fs_q_mcp_ics_span_negative_result_image_raw_negative_right. ff_np_mcp_smatrix_ics_span_negative_result_image_raw = fs_q_mcp_ics_span_negative_result_image_raw_negative_right * S ((S (ff_index_mcp_add_ics_span_negative_result_image_raw_negative)) * ff_nps_mcp_smatrix_ics_span_negative_result_image_raw) + (ff_right_mcp_add_ics_span_negative_result_image_raw_negative))) -> (((exists fs_h_mcp_ics_span_negative_result_image_raw_negative_target. fs_h_mcp_ics_span_negative_result_image_raw_negative_target + S (ff_target_mcp_add_ics_span_negative_result_image_raw_negative) = S ((S (ff_index_mcp_add_ics_span_negative_result_image_raw_negative)) * ics_raw_negative_scale_span_negative_result_image)) /\ exists fs_q_mcp_ics_span_negative_result_image_raw_negative_target. ics_raw_negative_span_negative_result_image = fs_q_mcp_ics_span_negative_result_image_raw_negative_target * S ((S (ff_index_mcp_add_ics_span_negative_result_image_raw_negative)) * ics_raw_negative_scale_span_negative_result_image) + (ff_target_mcp_add_ics_span_negative_result_image_raw_negative))) -> ff_target_mcp_add_ics_span_negative_result_image_raw_negative = ff_left_mcp_add_ics_span_negative_result_image_raw_negative + ff_right_mcp_add_ics_span_negative_result_image_raw_negative))))))) /\ (forall ics_index_span_negative_result_image_equal ics_value0_span_negative_result_image_equal ics_value1_span_negative_result_image_equal ics_value2_span_negative_result_image_equal ics_value3_span_negative_result_image_equal. (exists ics_gap_span_negative_result_image_equal_bound. ics_gap_span_negative_result_image_equal_bound + S (ics_index_span_negative_result_image_equal) = (r)) -> (((exists fs_h_ics_span_negative_result_image_equal_at0. fs_h_ics_span_negative_result_image_equal_at0 + S (ics_value0_span_negative_result_image_equal) = S ((S (ics_index_span_negative_result_image_equal)) * ics_raw_positive_scale_span_negative_result_image)) /\ exists fs_q_ics_span_negative_result_image_equal_at0. ics_raw_positive_span_negative_result_image = fs_q_ics_span_negative_result_image_equal_at0 * S ((S (ics_index_span_negative_result_image_equal)) * ics_raw_positive_scale_span_negative_result_image) + (ics_value0_span_negative_result_image_equal))) -> (((exists fs_h_ics_span_negative_result_image_equal_at1. fs_h_ics_span_negative_result_image_equal_at1 + S (ics_value1_span_negative_result_image_equal) = S ((S (ics_index_span_negative_result_image_equal)) * ics_raw_negative_scale_span_negative_result_image)) /\ exists fs_q_ics_span_negative_result_image_equal_at1. ics_raw_negative_span_negative_result_image = fs_q_ics_span_negative_result_image_equal_at1 * S ((S (ics_index_span_negative_result_image_equal)) * ics_raw_negative_scale_span_negative_result_image) + (ics_value1_span_negative_result_image_equal))) -> (((exists fs_h_ics_span_negative_result_image_equal_at2. fs_h_ics_span_negative_result_image_equal_at2 + S (ics_value2_span_negative_result_image_equal) = S ((S (ics_index_span_negative_result_image_equal)) * qc)) /\ exists fs_q_ics_span_negative_result_image_equal_at2. qb = fs_q_ics_span_negative_result_image_equal_at2 * S ((S (ics_index_span_negative_result_image_equal)) * qc) + (ics_value2_span_negative_result_image_equal))) -> (((exists fs_h_ics_span_negative_result_image_equal_at3. fs_h_ics_span_negative_result_image_equal_at3 + S (ics_value3_span_negative_result_image_equal) = S ((S (ics_index_span_negative_result_image_equal)) * mc)) /\ exists fs_q_ics_span_negative_result_image_equal_at3. mb = fs_q_ics_span_negative_result_image_equal_at3 * S ((S (ics_index_span_negative_result_image_equal)) * mc) + (ics_value3_span_negative_result_image_equal))) -> ics_value0_span_negative_result_image_equal + ics_value3_span_negative_result_image_equal = ics_value2_span_negative_result_image_equal + ics_value1_span_negative_result_image_equal)))))Complete tactic proof in conservative notation
All 44 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
44 script commands · 5 reading checkpoints · 0 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 (2)
01Fix variables and assumptionsL1–10
02Fix variables and assumptionsL11–16
03Use earlier factsL17–26
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L17
specialize integer_column_span_transport (ab) - L18
specialize integer_column_span_transport (ac) - L19
specialize integer_column_span_transport (db) - L20
specialize integer_column_span_transport (dc) - L21
specialize integer_column_span_transport (w) - L22
specialize integer_column_span_transport (r) - L23
specialize integer_column_span_transport (nb) - L24
specialize integer_column_span_transport (nc) - L25
specialize integer_column_span_transport (pb) - L26
specialize integer_column_span_transport (pc)
04Use earlier factsL27–36
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L27
specialize integer_column_span_transport (qb) - L28
specialize integer_column_span_transport (qc) - L29
specialize integer_column_span_transport (mb) - L30
specialize integer_column_span_transport (mc) - L31
apply integer_column_span_transport - L32
specialize integer_column_span_negated (ab) - L33
specialize integer_column_span_negated (ac) - L34
specialize integer_column_span_negated (db) - L35
specialize integer_column_span_negated (dc) - L36
specialize integer_column_span_negated (w)
05Use earlier factsL37–44
Instantiate or apply named facts and discharge the corresponding proof obligations.
Original defined command ledger · 44 lines
- 0001
intro ab - 0002
intro ac - 0003
intro db - 0004
intro dc - 0005
intro w - 0006
intro r - 0007
intro pb - 0008
intro pc - 0009
intro nb - 0010
intro nc - 0011
intro qb - 0012
intro qc - 0013
intro mb - 0014
intro mc - 0015
intro hspan - 0016
intro hnegative - 0017
specialize integer_column_span_transport (ab) - 0018
specialize integer_column_span_transport (ac) - 0019
specialize integer_column_span_transport (db) - 0020
specialize integer_column_span_transport (dc) - 0021
specialize integer_column_span_transport (w) - 0022
specialize integer_column_span_transport (r) - 0023
specialize integer_column_span_transport (nb) - 0024
specialize integer_column_span_transport (nc) - 0025
specialize integer_column_span_transport (pb) - 0026
specialize integer_column_span_transport (pc) - 0027
specialize integer_column_span_transport (qb) - 0028
specialize integer_column_span_transport (qc) - 0029
specialize integer_column_span_transport (mb) - 0030
specialize integer_column_span_transport (mc) - 0031
apply integer_column_span_transport - 0032
specialize integer_column_span_negated (ab) - 0033
specialize integer_column_span_negated (ac) - 0034
specialize integer_column_span_negated (db) - 0035
specialize integer_column_span_negated (dc) - 0036
specialize integer_column_span_negated (w) - 0037
specialize integer_column_span_negated (r) - 0038
specialize integer_column_span_negated (pb) - 0039
specialize integer_column_span_negated (pc) - 0040
specialize integer_column_span_negated (nb) - 0041
specialize integer_column_span_negated (nc) - 0042
apply integer_column_span_negated - 0043
exact hspan - 0044
exact hnegative