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(pb,pc,nb,nc,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_transport_source ics_coefficient_positive_scale_span_transport_source ics_coefficient_negative_span_transport_source ics_coefficient_negative_scale_span_transport_source. (exists ics_raw_positive_span_transport_source_image ics_raw_positive_scale_span_transport_source_image ics_raw_negative_span_transport_source_image ics_raw_negative_scale_span_transport_source_image. (((exists ff_pp_mcp_smatrix_ics_span_transport_source_image_raw ff_pps_mcp_smatrix_ics_span_transport_source_image_raw ff_nn_mcp_smatrix_ics_span_transport_source_image_raw ff_nns_mcp_smatrix_ics_span_transport_source_image_raw ff_pn_mcp_smatrix_ics_span_transport_source_image_raw ff_pns_mcp_smatrix_ics_span_transport_source_image_raw ff_np_mcp_smatrix_ics_span_transport_source_image_raw ff_nps_mcp_smatrix_ics_span_transport_source_image_raw. ((forall ff_index_mcp_prefix_ics_span_transport_source_image_raw_pp. (exists mcp_gap_ics_span_transport_source_image_raw_pp_index. mcp_gap_ics_span_transport_source_image_raw_pp_index + S (ff_index_mcp_prefix_ics_span_transport_source_image_raw_pp) = ((r) * (1))) -> exists ff_row_mcp_prefix_ics_span_transport_source_image_raw_pp ff_column_mcp_prefix_ics_span_transport_source_image_raw_pp ff_value_mcp_prefix_ics_span_transport_source_image_raw_pp. ((ff_index_mcp_prefix_ics_span_transport_source_image_raw_pp) = (1) * ff_row_mcp_prefix_ics_span_transport_source_image_raw_pp + ff_column_mcp_prefix_ics_span_transport_source_image_raw_pp /\ ((exists mcp_gap_ics_span_transport_source_image_raw_pp_column. mcp_gap_ics_span_transport_source_image_raw_pp_column + S (ff_column_mcp_prefix_ics_span_transport_source_image_raw_pp) = (1)) /\ ((exists ff_left_mcp_cell_ics_span_transport_source_image_raw_pp_cell ff_left_scale_mcp_cell_ics_span_transport_source_image_raw_pp_cell ff_right_mcp_cell_ics_span_transport_source_image_raw_pp_cell ff_right_scale_mcp_cell_ics_span_transport_source_image_raw_pp_cell. ((forall ff_index_mcp_ics_span_transport_source_image_raw_pp_cell_row ff_source_mcp_ics_span_transport_source_image_raw_pp_cell_row ff_target_mcp_ics_span_transport_source_image_raw_pp_cell_row. (exists mcp_gap_ics_span_transport_source_image_raw_pp_cell_row_bound. mcp_gap_ics_span_transport_source_image_raw_pp_cell_row_bound + S (ff_index_mcp_ics_span_transport_source_image_raw_pp_cell_row) = (w)) -> (((exists fs_h_mcp_ics_span_transport_source_image_raw_pp_cell_row_source. fs_h_mcp_ics_span_transport_source_image_raw_pp_cell_row_source + S (ff_source_mcp_ics_span_transport_source_image_raw_pp_cell_row) = S ((S (((ff_row_mcp_prefix_ics_span_transport_source_image_raw_pp) * (w)) + (1) * ff_index_mcp_ics_span_transport_source_image_raw_pp_cell_row)) * ac)) /\ exists fs_q_mcp_ics_span_transport_source_image_raw_pp_cell_row_source. ab = fs_q_mcp_ics_span_transport_source_image_raw_pp_cell_row_source * S ((S (((ff_row_mcp_prefix_ics_span_transport_source_image_raw_pp) * (w)) + (1) * ff_index_mcp_ics_span_transport_source_image_raw_pp_cell_row)) * ac) + (ff_source_mcp_ics_span_transport_source_image_raw_pp_cell_row))) -> (((exists fs_h_mcp_ics_span_transport_source_image_raw_pp_cell_row_target. fs_h_mcp_ics_span_transport_source_image_raw_pp_cell_row_target + S (ff_target_mcp_ics_span_transport_source_image_raw_pp_cell_row) = S ((S (ff_index_mcp_ics_span_transport_source_image_raw_pp_cell_row)) * ff_left_scale_mcp_cell_ics_span_transport_source_image_raw_pp_cell)) /\ exists fs_q_mcp_ics_span_transport_source_image_raw_pp_cell_row_target. ff_left_mcp_cell_ics_span_transport_source_image_raw_pp_cell = fs_q_mcp_ics_span_transport_source_image_raw_pp_cell_row_target * S ((S (ff_index_mcp_ics_span_transport_source_image_raw_pp_cell_row)) * ff_left_scale_mcp_cell_ics_span_transport_source_image_raw_pp_cell) + (ff_target_mcp_ics_span_transport_source_image_raw_pp_cell_row))) -> ff_target_mcp_ics_span_transport_source_image_raw_pp_cell_row = ff_source_mcp_ics_span_transport_source_image_raw_pp_cell_row) /\ ((forall ff_index_mcp_ics_span_transport_source_image_raw_pp_cell_column ff_source_mcp_ics_span_transport_source_image_raw_pp_cell_column ff_target_mcp_ics_span_transport_source_image_raw_pp_cell_column. (exists mcp_gap_ics_span_transport_source_image_raw_pp_cell_column_bound. mcp_gap_ics_span_transport_source_image_raw_pp_cell_column_bound + S (ff_index_mcp_ics_span_transport_source_image_raw_pp_cell_column) = (w)) -> (((exists fs_h_mcp_ics_span_transport_source_image_raw_pp_cell_column_source. fs_h_mcp_ics_span_transport_source_image_raw_pp_cell_column_source + S (ff_source_mcp_ics_span_transport_source_image_raw_pp_cell_column) = S ((S ((ff_column_mcp_prefix_ics_span_transport_source_image_raw_pp) + (1) * ff_index_mcp_ics_span_transport_source_image_raw_pp_cell_column)) * ics_coefficient_positive_scale_span_transport_source)) /\ exists fs_q_mcp_ics_span_transport_source_image_raw_pp_cell_column_source. ics_coefficient_positive_span_transport_source = fs_q_mcp_ics_span_transport_source_image_raw_pp_cell_column_source * S ((S ((ff_column_mcp_prefix_ics_span_transport_source_image_raw_pp) + (1) * ff_index_mcp_ics_span_transport_source_image_raw_pp_cell_column)) * ics_coefficient_positive_scale_span_transport_source) + (ff_source_mcp_ics_span_transport_source_image_raw_pp_cell_column))) -> (((exists fs_h_mcp_ics_span_transport_source_image_raw_pp_cell_column_target. fs_h_mcp_ics_span_transport_source_image_raw_pp_cell_column_target + S (ff_target_mcp_ics_span_transport_source_image_raw_pp_cell_column) = S ((S (ff_index_mcp_ics_span_transport_source_image_raw_pp_cell_column)) * ff_right_scale_mcp_cell_ics_span_transport_source_image_raw_pp_cell)) /\ exists fs_q_mcp_ics_span_transport_source_image_raw_pp_cell_column_target. ff_right_mcp_cell_ics_span_transport_source_image_raw_pp_cell = fs_q_mcp_ics_span_transport_source_image_raw_pp_cell_column_target * S ((S (ff_index_mcp_ics_span_transport_source_image_raw_pp_cell_column)) * ff_right_scale_mcp_cell_ics_span_transport_source_image_raw_pp_cell) + (ff_target_mcp_ics_span_transport_source_image_raw_pp_cell_column))) -> ff_target_mcp_ics_span_transport_source_image_raw_pp_cell_column = ff_source_mcp_ics_span_transport_source_image_raw_pp_cell_column) /\ (exists ff_code_dot_mcp_ics_span_transport_source_image_raw_pp_cell_dot ff_scale_dot_mcp_ics_span_transport_source_image_raw_pp_cell_dot. ((forall fpmp_index_dot_mcp_ics_span_transport_source_image_raw_pp_cell_dot_pointwise fpmp_left_dot_mcp_ics_span_transport_source_image_raw_pp_cell_dot_pointwise fpmp_right_dot_mcp_ics_span_transport_source_image_raw_pp_cell_dot_pointwise fpmp_target_dot_mcp_ics_span_transport_source_image_raw_pp_cell_dot_pointwise. (exists fpmp_gap_dot_mcp_ics_span_transport_source_image_raw_pp_cell_dot_pointwise. fpmp_gap_dot_mcp_ics_span_transport_source_image_raw_pp_cell_dot_pointwise + S fpmp_index_dot_mcp_ics_span_transport_source_image_raw_pp_cell_dot_pointwise = w) -> (((exists ff_h_fpmp_dot_mcp_ics_span_transport_source_image_raw_pp_cell_dot_pointwise_left. ff_h_fpmp_dot_mcp_ics_span_transport_source_image_raw_pp_cell_dot_pointwise_left + S (fpmp_left_dot_mcp_ics_span_transport_source_image_raw_pp_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_span_transport_source_image_raw_pp_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_span_transport_source_image_raw_pp_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_span_transport_source_image_raw_pp_cell_dot_pointwise_left. ff_left_mcp_cell_ics_span_transport_source_image_raw_pp_cell = ff_q_fpmp_dot_mcp_ics_span_transport_source_image_raw_pp_cell_dot_pointwise_left * S ((S (fpmp_index_dot_mcp_ics_span_transport_source_image_raw_pp_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_span_transport_source_image_raw_pp_cell) + (fpmp_left_dot_mcp_ics_span_transport_source_image_raw_pp_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_span_transport_source_image_raw_pp_cell_dot_pointwise_right. ff_h_fpmp_dot_mcp_ics_span_transport_source_image_raw_pp_cell_dot_pointwise_right + S (fpmp_right_dot_mcp_ics_span_transport_source_image_raw_pp_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_span_transport_source_image_raw_pp_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_span_transport_source_image_raw_pp_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_span_transport_source_image_raw_pp_cell_dot_pointwise_right. ff_right_mcp_cell_ics_span_transport_source_image_raw_pp_cell = ff_q_fpmp_dot_mcp_ics_span_transport_source_image_raw_pp_cell_dot_pointwise_right * S ((S (fpmp_index_dot_mcp_ics_span_transport_source_image_raw_pp_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_span_transport_source_image_raw_pp_cell) + (fpmp_right_dot_mcp_ics_span_transport_source_image_raw_pp_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_span_transport_source_image_raw_pp_cell_dot_pointwise_target. ff_h_fpmp_dot_mcp_ics_span_transport_source_image_raw_pp_cell_dot_pointwise_target + S (fpmp_target_dot_mcp_ics_span_transport_source_image_raw_pp_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_span_transport_source_image_raw_pp_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_span_transport_source_image_raw_pp_cell_dot)) /\ exists ff_q_fpmp_dot_mcp_ics_span_transport_source_image_raw_pp_cell_dot_pointwise_target. ff_code_dot_mcp_ics_span_transport_source_image_raw_pp_cell_dot = ff_q_fpmp_dot_mcp_ics_span_transport_source_image_raw_pp_cell_dot_pointwise_target * S ((S (fpmp_index_dot_mcp_ics_span_transport_source_image_raw_pp_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_span_transport_source_image_raw_pp_cell_dot) + (fpmp_target_dot_mcp_ics_span_transport_source_image_raw_pp_cell_dot_pointwise))) -> fpmp_target_dot_mcp_ics_span_transport_source_image_raw_pp_cell_dot_pointwise = fpmp_left_dot_mcp_ics_span_transport_source_image_raw_pp_cell_dot_pointwise * fpmp_right_dot_mcp_ics_span_transport_source_image_raw_pp_cell_dot_pointwise) /\ (exists ff_u_dot_mcp_ics_span_transport_source_image_raw_pp_cell_dot_sum ff_v_dot_mcp_ics_span_transport_source_image_raw_pp_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_span_transport_source_image_raw_pp_cell_dot_sum_start. ff_h_dot_mcp_ics_span_transport_source_image_raw_pp_cell_dot_sum_start + S (0) = S ((S (0)) * ff_v_dot_mcp_ics_span_transport_source_image_raw_pp_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_span_transport_source_image_raw_pp_cell_dot_sum_start. ff_u_dot_mcp_ics_span_transport_source_image_raw_pp_cell_dot_sum = ff_q_dot_mcp_ics_span_transport_source_image_raw_pp_cell_dot_sum_start * S ((S (0)) * ff_v_dot_mcp_ics_span_transport_source_image_raw_pp_cell_dot_sum) + (0))) /\ ((((exists ff_h_dot_mcp_ics_span_transport_source_image_raw_pp_cell_dot_sum_terminal. ff_h_dot_mcp_ics_span_transport_source_image_raw_pp_cell_dot_sum_terminal + S (ff_value_mcp_prefix_ics_span_transport_source_image_raw_pp) = S ((S (w)) * ff_v_dot_mcp_ics_span_transport_source_image_raw_pp_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_span_transport_source_image_raw_pp_cell_dot_sum_terminal. ff_u_dot_mcp_ics_span_transport_source_image_raw_pp_cell_dot_sum = ff_q_dot_mcp_ics_span_transport_source_image_raw_pp_cell_dot_sum_terminal * S ((S (w)) * ff_v_dot_mcp_ics_span_transport_source_image_raw_pp_cell_dot_sum) + (ff_value_mcp_prefix_ics_span_transport_source_image_raw_pp))) /\ forall ff_i_dot_mcp_ics_span_transport_source_image_raw_pp_cell_dot_sum. (exists ff_lt_dot_mcp_ics_span_transport_source_image_raw_pp_cell_dot_sum_bound. ff_lt_dot_mcp_ics_span_transport_source_image_raw_pp_cell_dot_sum_bound + S ff_i_dot_mcp_ics_span_transport_source_image_raw_pp_cell_dot_sum = w) -> exists ff_a_dot_mcp_ics_span_transport_source_image_raw_pp_cell_dot_sum ff_r_dot_mcp_ics_span_transport_source_image_raw_pp_cell_dot_sum ff_s_dot_mcp_ics_span_transport_source_image_raw_pp_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_span_transport_source_image_raw_pp_cell_dot_sum_summand. ff_h_dot_mcp_ics_span_transport_source_image_raw_pp_cell_dot_sum_summand + S (ff_a_dot_mcp_ics_span_transport_source_image_raw_pp_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_span_transport_source_image_raw_pp_cell_dot_sum)) * ff_scale_dot_mcp_ics_span_transport_source_image_raw_pp_cell_dot)) /\ exists ff_q_dot_mcp_ics_span_transport_source_image_raw_pp_cell_dot_sum_summand. ff_code_dot_mcp_ics_span_transport_source_image_raw_pp_cell_dot = ff_q_dot_mcp_ics_span_transport_source_image_raw_pp_cell_dot_sum_summand * S ((S (ff_i_dot_mcp_ics_span_transport_source_image_raw_pp_cell_dot_sum)) * ff_scale_dot_mcp_ics_span_transport_source_image_raw_pp_cell_dot) + (ff_a_dot_mcp_ics_span_transport_source_image_raw_pp_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_span_transport_source_image_raw_pp_cell_dot_sum_partial. ff_h_dot_mcp_ics_span_transport_source_image_raw_pp_cell_dot_sum_partial + S (ff_r_dot_mcp_ics_span_transport_source_image_raw_pp_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_span_transport_source_image_raw_pp_cell_dot_sum)) * ff_v_dot_mcp_ics_span_transport_source_image_raw_pp_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_span_transport_source_image_raw_pp_cell_dot_sum_partial. ff_u_dot_mcp_ics_span_transport_source_image_raw_pp_cell_dot_sum = ff_q_dot_mcp_ics_span_transport_source_image_raw_pp_cell_dot_sum_partial * S ((S (ff_i_dot_mcp_ics_span_transport_source_image_raw_pp_cell_dot_sum)) * ff_v_dot_mcp_ics_span_transport_source_image_raw_pp_cell_dot_sum) + (ff_r_dot_mcp_ics_span_transport_source_image_raw_pp_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_span_transport_source_image_raw_pp_cell_dot_sum_successor. ff_h_dot_mcp_ics_span_transport_source_image_raw_pp_cell_dot_sum_successor + S (ff_s_dot_mcp_ics_span_transport_source_image_raw_pp_cell_dot_sum) = S ((S (S ff_i_dot_mcp_ics_span_transport_source_image_raw_pp_cell_dot_sum)) * ff_v_dot_mcp_ics_span_transport_source_image_raw_pp_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_span_transport_source_image_raw_pp_cell_dot_sum_successor. ff_u_dot_mcp_ics_span_transport_source_image_raw_pp_cell_dot_sum = ff_q_dot_mcp_ics_span_transport_source_image_raw_pp_cell_dot_sum_successor * S ((S (S ff_i_dot_mcp_ics_span_transport_source_image_raw_pp_cell_dot_sum)) * ff_v_dot_mcp_ics_span_transport_source_image_raw_pp_cell_dot_sum) + (ff_s_dot_mcp_ics_span_transport_source_image_raw_pp_cell_dot_sum))) /\ ff_s_dot_mcp_ics_span_transport_source_image_raw_pp_cell_dot_sum = ff_r_dot_mcp_ics_span_transport_source_image_raw_pp_cell_dot_sum + ff_a_dot_mcp_ics_span_transport_source_image_raw_pp_cell_dot_sum))))))))))) /\ (((exists fs_h_mcp_ics_span_transport_source_image_raw_pp_entry. fs_h_mcp_ics_span_transport_source_image_raw_pp_entry + S (ff_value_mcp_prefix_ics_span_transport_source_image_raw_pp) = S ((S (ff_index_mcp_prefix_ics_span_transport_source_image_raw_pp)) * ff_pps_mcp_smatrix_ics_span_transport_source_image_raw)) /\ exists fs_q_mcp_ics_span_transport_source_image_raw_pp_entry. ff_pp_mcp_smatrix_ics_span_transport_source_image_raw = fs_q_mcp_ics_span_transport_source_image_raw_pp_entry * S ((S (ff_index_mcp_prefix_ics_span_transport_source_image_raw_pp)) * ff_pps_mcp_smatrix_ics_span_transport_source_image_raw) + (ff_value_mcp_prefix_ics_span_transport_source_image_raw_pp))))))) /\ ((forall ff_index_mcp_prefix_ics_span_transport_source_image_raw_nn. (exists mcp_gap_ics_span_transport_source_image_raw_nn_index. mcp_gap_ics_span_transport_source_image_raw_nn_index + S (ff_index_mcp_prefix_ics_span_transport_source_image_raw_nn) = ((r) * (1))) -> exists ff_row_mcp_prefix_ics_span_transport_source_image_raw_nn ff_column_mcp_prefix_ics_span_transport_source_image_raw_nn ff_value_mcp_prefix_ics_span_transport_source_image_raw_nn. ((ff_index_mcp_prefix_ics_span_transport_source_image_raw_nn) = (1) * ff_row_mcp_prefix_ics_span_transport_source_image_raw_nn + ff_column_mcp_prefix_ics_span_transport_source_image_raw_nn /\ ((exists mcp_gap_ics_span_transport_source_image_raw_nn_column. mcp_gap_ics_span_transport_source_image_raw_nn_column + S (ff_column_mcp_prefix_ics_span_transport_source_image_raw_nn) = (1)) /\ ((exists ff_left_mcp_cell_ics_span_transport_source_image_raw_nn_cell ff_left_scale_mcp_cell_ics_span_transport_source_image_raw_nn_cell ff_right_mcp_cell_ics_span_transport_source_image_raw_nn_cell ff_right_scale_mcp_cell_ics_span_transport_source_image_raw_nn_cell. ((forall ff_index_mcp_ics_span_transport_source_image_raw_nn_cell_row ff_source_mcp_ics_span_transport_source_image_raw_nn_cell_row ff_target_mcp_ics_span_transport_source_image_raw_nn_cell_row. (exists mcp_gap_ics_span_transport_source_image_raw_nn_cell_row_bound. mcp_gap_ics_span_transport_source_image_raw_nn_cell_row_bound + S (ff_index_mcp_ics_span_transport_source_image_raw_nn_cell_row) = (w)) -> (((exists fs_h_mcp_ics_span_transport_source_image_raw_nn_cell_row_source. fs_h_mcp_ics_span_transport_source_image_raw_nn_cell_row_source + S (ff_source_mcp_ics_span_transport_source_image_raw_nn_cell_row) = S ((S (((ff_row_mcp_prefix_ics_span_transport_source_image_raw_nn) * (w)) + (1) * ff_index_mcp_ics_span_transport_source_image_raw_nn_cell_row)) * dc)) /\ exists fs_q_mcp_ics_span_transport_source_image_raw_nn_cell_row_source. db = fs_q_mcp_ics_span_transport_source_image_raw_nn_cell_row_source * S ((S (((ff_row_mcp_prefix_ics_span_transport_source_image_raw_nn) * (w)) + (1) * ff_index_mcp_ics_span_transport_source_image_raw_nn_cell_row)) * dc) + (ff_source_mcp_ics_span_transport_source_image_raw_nn_cell_row))) -> (((exists fs_h_mcp_ics_span_transport_source_image_raw_nn_cell_row_target. fs_h_mcp_ics_span_transport_source_image_raw_nn_cell_row_target + S (ff_target_mcp_ics_span_transport_source_image_raw_nn_cell_row) = S ((S (ff_index_mcp_ics_span_transport_source_image_raw_nn_cell_row)) * ff_left_scale_mcp_cell_ics_span_transport_source_image_raw_nn_cell)) /\ exists fs_q_mcp_ics_span_transport_source_image_raw_nn_cell_row_target. ff_left_mcp_cell_ics_span_transport_source_image_raw_nn_cell = fs_q_mcp_ics_span_transport_source_image_raw_nn_cell_row_target * S ((S (ff_index_mcp_ics_span_transport_source_image_raw_nn_cell_row)) * ff_left_scale_mcp_cell_ics_span_transport_source_image_raw_nn_cell) + (ff_target_mcp_ics_span_transport_source_image_raw_nn_cell_row))) -> ff_target_mcp_ics_span_transport_source_image_raw_nn_cell_row = ff_source_mcp_ics_span_transport_source_image_raw_nn_cell_row) /\ ((forall ff_index_mcp_ics_span_transport_source_image_raw_nn_cell_column ff_source_mcp_ics_span_transport_source_image_raw_nn_cell_column ff_target_mcp_ics_span_transport_source_image_raw_nn_cell_column. (exists mcp_gap_ics_span_transport_source_image_raw_nn_cell_column_bound. mcp_gap_ics_span_transport_source_image_raw_nn_cell_column_bound + S (ff_index_mcp_ics_span_transport_source_image_raw_nn_cell_column) = (w)) -> (((exists fs_h_mcp_ics_span_transport_source_image_raw_nn_cell_column_source. fs_h_mcp_ics_span_transport_source_image_raw_nn_cell_column_source + S (ff_source_mcp_ics_span_transport_source_image_raw_nn_cell_column) = S ((S ((ff_column_mcp_prefix_ics_span_transport_source_image_raw_nn) + (1) * ff_index_mcp_ics_span_transport_source_image_raw_nn_cell_column)) * ics_coefficient_negative_scale_span_transport_source)) /\ exists fs_q_mcp_ics_span_transport_source_image_raw_nn_cell_column_source. ics_coefficient_negative_span_transport_source = fs_q_mcp_ics_span_transport_source_image_raw_nn_cell_column_source * S ((S ((ff_column_mcp_prefix_ics_span_transport_source_image_raw_nn) + (1) * ff_index_mcp_ics_span_transport_source_image_raw_nn_cell_column)) * ics_coefficient_negative_scale_span_transport_source) + (ff_source_mcp_ics_span_transport_source_image_raw_nn_cell_column))) -> (((exists fs_h_mcp_ics_span_transport_source_image_raw_nn_cell_column_target. fs_h_mcp_ics_span_transport_source_image_raw_nn_cell_column_target + S (ff_target_mcp_ics_span_transport_source_image_raw_nn_cell_column) = S ((S (ff_index_mcp_ics_span_transport_source_image_raw_nn_cell_column)) * ff_right_scale_mcp_cell_ics_span_transport_source_image_raw_nn_cell)) /\ exists fs_q_mcp_ics_span_transport_source_image_raw_nn_cell_column_target. ff_right_mcp_cell_ics_span_transport_source_image_raw_nn_cell = fs_q_mcp_ics_span_transport_source_image_raw_nn_cell_column_target * S ((S (ff_index_mcp_ics_span_transport_source_image_raw_nn_cell_column)) * ff_right_scale_mcp_cell_ics_span_transport_source_image_raw_nn_cell) + (ff_target_mcp_ics_span_transport_source_image_raw_nn_cell_column))) -> ff_target_mcp_ics_span_transport_source_image_raw_nn_cell_column = ff_source_mcp_ics_span_transport_source_image_raw_nn_cell_column) /\ (exists ff_code_dot_mcp_ics_span_transport_source_image_raw_nn_cell_dot ff_scale_dot_mcp_ics_span_transport_source_image_raw_nn_cell_dot. ((forall fpmp_index_dot_mcp_ics_span_transport_source_image_raw_nn_cell_dot_pointwise fpmp_left_dot_mcp_ics_span_transport_source_image_raw_nn_cell_dot_pointwise fpmp_right_dot_mcp_ics_span_transport_source_image_raw_nn_cell_dot_pointwise fpmp_target_dot_mcp_ics_span_transport_source_image_raw_nn_cell_dot_pointwise. (exists fpmp_gap_dot_mcp_ics_span_transport_source_image_raw_nn_cell_dot_pointwise. fpmp_gap_dot_mcp_ics_span_transport_source_image_raw_nn_cell_dot_pointwise + S fpmp_index_dot_mcp_ics_span_transport_source_image_raw_nn_cell_dot_pointwise = w) -> (((exists ff_h_fpmp_dot_mcp_ics_span_transport_source_image_raw_nn_cell_dot_pointwise_left. ff_h_fpmp_dot_mcp_ics_span_transport_source_image_raw_nn_cell_dot_pointwise_left + S (fpmp_left_dot_mcp_ics_span_transport_source_image_raw_nn_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_span_transport_source_image_raw_nn_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_span_transport_source_image_raw_nn_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_span_transport_source_image_raw_nn_cell_dot_pointwise_left. ff_left_mcp_cell_ics_span_transport_source_image_raw_nn_cell = ff_q_fpmp_dot_mcp_ics_span_transport_source_image_raw_nn_cell_dot_pointwise_left * S ((S (fpmp_index_dot_mcp_ics_span_transport_source_image_raw_nn_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_span_transport_source_image_raw_nn_cell) + (fpmp_left_dot_mcp_ics_span_transport_source_image_raw_nn_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_span_transport_source_image_raw_nn_cell_dot_pointwise_right. ff_h_fpmp_dot_mcp_ics_span_transport_source_image_raw_nn_cell_dot_pointwise_right + S (fpmp_right_dot_mcp_ics_span_transport_source_image_raw_nn_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_span_transport_source_image_raw_nn_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_span_transport_source_image_raw_nn_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_span_transport_source_image_raw_nn_cell_dot_pointwise_right. ff_right_mcp_cell_ics_span_transport_source_image_raw_nn_cell = ff_q_fpmp_dot_mcp_ics_span_transport_source_image_raw_nn_cell_dot_pointwise_right * S ((S (fpmp_index_dot_mcp_ics_span_transport_source_image_raw_nn_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_span_transport_source_image_raw_nn_cell) + (fpmp_right_dot_mcp_ics_span_transport_source_image_raw_nn_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_span_transport_source_image_raw_nn_cell_dot_pointwise_target. ff_h_fpmp_dot_mcp_ics_span_transport_source_image_raw_nn_cell_dot_pointwise_target + S (fpmp_target_dot_mcp_ics_span_transport_source_image_raw_nn_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_span_transport_source_image_raw_nn_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_span_transport_source_image_raw_nn_cell_dot)) /\ exists ff_q_fpmp_dot_mcp_ics_span_transport_source_image_raw_nn_cell_dot_pointwise_target. ff_code_dot_mcp_ics_span_transport_source_image_raw_nn_cell_dot = ff_q_fpmp_dot_mcp_ics_span_transport_source_image_raw_nn_cell_dot_pointwise_target * S ((S (fpmp_index_dot_mcp_ics_span_transport_source_image_raw_nn_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_span_transport_source_image_raw_nn_cell_dot) + (fpmp_target_dot_mcp_ics_span_transport_source_image_raw_nn_cell_dot_pointwise))) -> fpmp_target_dot_mcp_ics_span_transport_source_image_raw_nn_cell_dot_pointwise = fpmp_left_dot_mcp_ics_span_transport_source_image_raw_nn_cell_dot_pointwise * fpmp_right_dot_mcp_ics_span_transport_source_image_raw_nn_cell_dot_pointwise) /\ (exists ff_u_dot_mcp_ics_span_transport_source_image_raw_nn_cell_dot_sum ff_v_dot_mcp_ics_span_transport_source_image_raw_nn_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_span_transport_source_image_raw_nn_cell_dot_sum_start. ff_h_dot_mcp_ics_span_transport_source_image_raw_nn_cell_dot_sum_start + S (0) = S ((S (0)) * ff_v_dot_mcp_ics_span_transport_source_image_raw_nn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_span_transport_source_image_raw_nn_cell_dot_sum_start. ff_u_dot_mcp_ics_span_transport_source_image_raw_nn_cell_dot_sum = ff_q_dot_mcp_ics_span_transport_source_image_raw_nn_cell_dot_sum_start * S ((S (0)) * ff_v_dot_mcp_ics_span_transport_source_image_raw_nn_cell_dot_sum) + (0))) /\ ((((exists ff_h_dot_mcp_ics_span_transport_source_image_raw_nn_cell_dot_sum_terminal. ff_h_dot_mcp_ics_span_transport_source_image_raw_nn_cell_dot_sum_terminal + S (ff_value_mcp_prefix_ics_span_transport_source_image_raw_nn) = S ((S (w)) * ff_v_dot_mcp_ics_span_transport_source_image_raw_nn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_span_transport_source_image_raw_nn_cell_dot_sum_terminal. ff_u_dot_mcp_ics_span_transport_source_image_raw_nn_cell_dot_sum = ff_q_dot_mcp_ics_span_transport_source_image_raw_nn_cell_dot_sum_terminal * S ((S (w)) * ff_v_dot_mcp_ics_span_transport_source_image_raw_nn_cell_dot_sum) + (ff_value_mcp_prefix_ics_span_transport_source_image_raw_nn))) /\ forall ff_i_dot_mcp_ics_span_transport_source_image_raw_nn_cell_dot_sum. (exists ff_lt_dot_mcp_ics_span_transport_source_image_raw_nn_cell_dot_sum_bound. ff_lt_dot_mcp_ics_span_transport_source_image_raw_nn_cell_dot_sum_bound + S ff_i_dot_mcp_ics_span_transport_source_image_raw_nn_cell_dot_sum = w) -> exists ff_a_dot_mcp_ics_span_transport_source_image_raw_nn_cell_dot_sum ff_r_dot_mcp_ics_span_transport_source_image_raw_nn_cell_dot_sum ff_s_dot_mcp_ics_span_transport_source_image_raw_nn_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_span_transport_source_image_raw_nn_cell_dot_sum_summand. ff_h_dot_mcp_ics_span_transport_source_image_raw_nn_cell_dot_sum_summand + S (ff_a_dot_mcp_ics_span_transport_source_image_raw_nn_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_span_transport_source_image_raw_nn_cell_dot_sum)) * ff_scale_dot_mcp_ics_span_transport_source_image_raw_nn_cell_dot)) /\ exists ff_q_dot_mcp_ics_span_transport_source_image_raw_nn_cell_dot_sum_summand. ff_code_dot_mcp_ics_span_transport_source_image_raw_nn_cell_dot = ff_q_dot_mcp_ics_span_transport_source_image_raw_nn_cell_dot_sum_summand * S ((S (ff_i_dot_mcp_ics_span_transport_source_image_raw_nn_cell_dot_sum)) * ff_scale_dot_mcp_ics_span_transport_source_image_raw_nn_cell_dot) + (ff_a_dot_mcp_ics_span_transport_source_image_raw_nn_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_span_transport_source_image_raw_nn_cell_dot_sum_partial. ff_h_dot_mcp_ics_span_transport_source_image_raw_nn_cell_dot_sum_partial + S (ff_r_dot_mcp_ics_span_transport_source_image_raw_nn_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_span_transport_source_image_raw_nn_cell_dot_sum)) * ff_v_dot_mcp_ics_span_transport_source_image_raw_nn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_span_transport_source_image_raw_nn_cell_dot_sum_partial. ff_u_dot_mcp_ics_span_transport_source_image_raw_nn_cell_dot_sum = ff_q_dot_mcp_ics_span_transport_source_image_raw_nn_cell_dot_sum_partial * S ((S (ff_i_dot_mcp_ics_span_transport_source_image_raw_nn_cell_dot_sum)) * ff_v_dot_mcp_ics_span_transport_source_image_raw_nn_cell_dot_sum) + (ff_r_dot_mcp_ics_span_transport_source_image_raw_nn_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_span_transport_source_image_raw_nn_cell_dot_sum_successor. ff_h_dot_mcp_ics_span_transport_source_image_raw_nn_cell_dot_sum_successor + S (ff_s_dot_mcp_ics_span_transport_source_image_raw_nn_cell_dot_sum) = S ((S (S ff_i_dot_mcp_ics_span_transport_source_image_raw_nn_cell_dot_sum)) * ff_v_dot_mcp_ics_span_transport_source_image_raw_nn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_span_transport_source_image_raw_nn_cell_dot_sum_successor. ff_u_dot_mcp_ics_span_transport_source_image_raw_nn_cell_dot_sum = ff_q_dot_mcp_ics_span_transport_source_image_raw_nn_cell_dot_sum_successor * S ((S (S ff_i_dot_mcp_ics_span_transport_source_image_raw_nn_cell_dot_sum)) * ff_v_dot_mcp_ics_span_transport_source_image_raw_nn_cell_dot_sum) + (ff_s_dot_mcp_ics_span_transport_source_image_raw_nn_cell_dot_sum))) /\ ff_s_dot_mcp_ics_span_transport_source_image_raw_nn_cell_dot_sum = ff_r_dot_mcp_ics_span_transport_source_image_raw_nn_cell_dot_sum + ff_a_dot_mcp_ics_span_transport_source_image_raw_nn_cell_dot_sum))))))))))) /\ (((exists fs_h_mcp_ics_span_transport_source_image_raw_nn_entry. fs_h_mcp_ics_span_transport_source_image_raw_nn_entry + S (ff_value_mcp_prefix_ics_span_transport_source_image_raw_nn) = S ((S (ff_index_mcp_prefix_ics_span_transport_source_image_raw_nn)) * ff_nns_mcp_smatrix_ics_span_transport_source_image_raw)) /\ exists fs_q_mcp_ics_span_transport_source_image_raw_nn_entry. ff_nn_mcp_smatrix_ics_span_transport_source_image_raw = fs_q_mcp_ics_span_transport_source_image_raw_nn_entry * S ((S (ff_index_mcp_prefix_ics_span_transport_source_image_raw_nn)) * ff_nns_mcp_smatrix_ics_span_transport_source_image_raw) + (ff_value_mcp_prefix_ics_span_transport_source_image_raw_nn))))))) /\ ((forall ff_index_mcp_prefix_ics_span_transport_source_image_raw_pn. (exists mcp_gap_ics_span_transport_source_image_raw_pn_index. mcp_gap_ics_span_transport_source_image_raw_pn_index + S (ff_index_mcp_prefix_ics_span_transport_source_image_raw_pn) = ((r) * (1))) -> exists ff_row_mcp_prefix_ics_span_transport_source_image_raw_pn ff_column_mcp_prefix_ics_span_transport_source_image_raw_pn ff_value_mcp_prefix_ics_span_transport_source_image_raw_pn. ((ff_index_mcp_prefix_ics_span_transport_source_image_raw_pn) = (1) * ff_row_mcp_prefix_ics_span_transport_source_image_raw_pn + ff_column_mcp_prefix_ics_span_transport_source_image_raw_pn /\ ((exists mcp_gap_ics_span_transport_source_image_raw_pn_column. mcp_gap_ics_span_transport_source_image_raw_pn_column + S (ff_column_mcp_prefix_ics_span_transport_source_image_raw_pn) = (1)) /\ ((exists ff_left_mcp_cell_ics_span_transport_source_image_raw_pn_cell ff_left_scale_mcp_cell_ics_span_transport_source_image_raw_pn_cell ff_right_mcp_cell_ics_span_transport_source_image_raw_pn_cell ff_right_scale_mcp_cell_ics_span_transport_source_image_raw_pn_cell. ((forall ff_index_mcp_ics_span_transport_source_image_raw_pn_cell_row ff_source_mcp_ics_span_transport_source_image_raw_pn_cell_row ff_target_mcp_ics_span_transport_source_image_raw_pn_cell_row. (exists mcp_gap_ics_span_transport_source_image_raw_pn_cell_row_bound. mcp_gap_ics_span_transport_source_image_raw_pn_cell_row_bound + S (ff_index_mcp_ics_span_transport_source_image_raw_pn_cell_row) = (w)) -> (((exists fs_h_mcp_ics_span_transport_source_image_raw_pn_cell_row_source. fs_h_mcp_ics_span_transport_source_image_raw_pn_cell_row_source + S (ff_source_mcp_ics_span_transport_source_image_raw_pn_cell_row) = S ((S (((ff_row_mcp_prefix_ics_span_transport_source_image_raw_pn) * (w)) + (1) * ff_index_mcp_ics_span_transport_source_image_raw_pn_cell_row)) * ac)) /\ exists fs_q_mcp_ics_span_transport_source_image_raw_pn_cell_row_source. ab = fs_q_mcp_ics_span_transport_source_image_raw_pn_cell_row_source * S ((S (((ff_row_mcp_prefix_ics_span_transport_source_image_raw_pn) * (w)) + (1) * ff_index_mcp_ics_span_transport_source_image_raw_pn_cell_row)) * ac) + (ff_source_mcp_ics_span_transport_source_image_raw_pn_cell_row))) -> (((exists fs_h_mcp_ics_span_transport_source_image_raw_pn_cell_row_target. fs_h_mcp_ics_span_transport_source_image_raw_pn_cell_row_target + S (ff_target_mcp_ics_span_transport_source_image_raw_pn_cell_row) = S ((S (ff_index_mcp_ics_span_transport_source_image_raw_pn_cell_row)) * ff_left_scale_mcp_cell_ics_span_transport_source_image_raw_pn_cell)) /\ exists fs_q_mcp_ics_span_transport_source_image_raw_pn_cell_row_target. ff_left_mcp_cell_ics_span_transport_source_image_raw_pn_cell = fs_q_mcp_ics_span_transport_source_image_raw_pn_cell_row_target * S ((S (ff_index_mcp_ics_span_transport_source_image_raw_pn_cell_row)) * ff_left_scale_mcp_cell_ics_span_transport_source_image_raw_pn_cell) + (ff_target_mcp_ics_span_transport_source_image_raw_pn_cell_row))) -> ff_target_mcp_ics_span_transport_source_image_raw_pn_cell_row = ff_source_mcp_ics_span_transport_source_image_raw_pn_cell_row) /\ ((forall ff_index_mcp_ics_span_transport_source_image_raw_pn_cell_column ff_source_mcp_ics_span_transport_source_image_raw_pn_cell_column ff_target_mcp_ics_span_transport_source_image_raw_pn_cell_column. (exists mcp_gap_ics_span_transport_source_image_raw_pn_cell_column_bound. mcp_gap_ics_span_transport_source_image_raw_pn_cell_column_bound + S (ff_index_mcp_ics_span_transport_source_image_raw_pn_cell_column) = (w)) -> (((exists fs_h_mcp_ics_span_transport_source_image_raw_pn_cell_column_source. fs_h_mcp_ics_span_transport_source_image_raw_pn_cell_column_source + S (ff_source_mcp_ics_span_transport_source_image_raw_pn_cell_column) = S ((S ((ff_column_mcp_prefix_ics_span_transport_source_image_raw_pn) + (1) * ff_index_mcp_ics_span_transport_source_image_raw_pn_cell_column)) * ics_coefficient_negative_scale_span_transport_source)) /\ exists fs_q_mcp_ics_span_transport_source_image_raw_pn_cell_column_source. ics_coefficient_negative_span_transport_source = fs_q_mcp_ics_span_transport_source_image_raw_pn_cell_column_source * S ((S ((ff_column_mcp_prefix_ics_span_transport_source_image_raw_pn) + (1) * ff_index_mcp_ics_span_transport_source_image_raw_pn_cell_column)) * ics_coefficient_negative_scale_span_transport_source) + (ff_source_mcp_ics_span_transport_source_image_raw_pn_cell_column))) -> (((exists fs_h_mcp_ics_span_transport_source_image_raw_pn_cell_column_target. fs_h_mcp_ics_span_transport_source_image_raw_pn_cell_column_target + S (ff_target_mcp_ics_span_transport_source_image_raw_pn_cell_column) = S ((S (ff_index_mcp_ics_span_transport_source_image_raw_pn_cell_column)) * ff_right_scale_mcp_cell_ics_span_transport_source_image_raw_pn_cell)) /\ exists fs_q_mcp_ics_span_transport_source_image_raw_pn_cell_column_target. ff_right_mcp_cell_ics_span_transport_source_image_raw_pn_cell = fs_q_mcp_ics_span_transport_source_image_raw_pn_cell_column_target * S ((S (ff_index_mcp_ics_span_transport_source_image_raw_pn_cell_column)) * ff_right_scale_mcp_cell_ics_span_transport_source_image_raw_pn_cell) + (ff_target_mcp_ics_span_transport_source_image_raw_pn_cell_column))) -> ff_target_mcp_ics_span_transport_source_image_raw_pn_cell_column = ff_source_mcp_ics_span_transport_source_image_raw_pn_cell_column) /\ (exists ff_code_dot_mcp_ics_span_transport_source_image_raw_pn_cell_dot ff_scale_dot_mcp_ics_span_transport_source_image_raw_pn_cell_dot. ((forall fpmp_index_dot_mcp_ics_span_transport_source_image_raw_pn_cell_dot_pointwise fpmp_left_dot_mcp_ics_span_transport_source_image_raw_pn_cell_dot_pointwise fpmp_right_dot_mcp_ics_span_transport_source_image_raw_pn_cell_dot_pointwise fpmp_target_dot_mcp_ics_span_transport_source_image_raw_pn_cell_dot_pointwise. (exists fpmp_gap_dot_mcp_ics_span_transport_source_image_raw_pn_cell_dot_pointwise. fpmp_gap_dot_mcp_ics_span_transport_source_image_raw_pn_cell_dot_pointwise + S fpmp_index_dot_mcp_ics_span_transport_source_image_raw_pn_cell_dot_pointwise = w) -> (((exists ff_h_fpmp_dot_mcp_ics_span_transport_source_image_raw_pn_cell_dot_pointwise_left. ff_h_fpmp_dot_mcp_ics_span_transport_source_image_raw_pn_cell_dot_pointwise_left + S (fpmp_left_dot_mcp_ics_span_transport_source_image_raw_pn_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_span_transport_source_image_raw_pn_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_span_transport_source_image_raw_pn_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_span_transport_source_image_raw_pn_cell_dot_pointwise_left. ff_left_mcp_cell_ics_span_transport_source_image_raw_pn_cell = ff_q_fpmp_dot_mcp_ics_span_transport_source_image_raw_pn_cell_dot_pointwise_left * S ((S (fpmp_index_dot_mcp_ics_span_transport_source_image_raw_pn_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_span_transport_source_image_raw_pn_cell) + (fpmp_left_dot_mcp_ics_span_transport_source_image_raw_pn_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_span_transport_source_image_raw_pn_cell_dot_pointwise_right. ff_h_fpmp_dot_mcp_ics_span_transport_source_image_raw_pn_cell_dot_pointwise_right + S (fpmp_right_dot_mcp_ics_span_transport_source_image_raw_pn_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_span_transport_source_image_raw_pn_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_span_transport_source_image_raw_pn_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_span_transport_source_image_raw_pn_cell_dot_pointwise_right. ff_right_mcp_cell_ics_span_transport_source_image_raw_pn_cell = ff_q_fpmp_dot_mcp_ics_span_transport_source_image_raw_pn_cell_dot_pointwise_right * S ((S (fpmp_index_dot_mcp_ics_span_transport_source_image_raw_pn_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_span_transport_source_image_raw_pn_cell) + (fpmp_right_dot_mcp_ics_span_transport_source_image_raw_pn_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_span_transport_source_image_raw_pn_cell_dot_pointwise_target. ff_h_fpmp_dot_mcp_ics_span_transport_source_image_raw_pn_cell_dot_pointwise_target + S (fpmp_target_dot_mcp_ics_span_transport_source_image_raw_pn_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_span_transport_source_image_raw_pn_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_span_transport_source_image_raw_pn_cell_dot)) /\ exists ff_q_fpmp_dot_mcp_ics_span_transport_source_image_raw_pn_cell_dot_pointwise_target. ff_code_dot_mcp_ics_span_transport_source_image_raw_pn_cell_dot = ff_q_fpmp_dot_mcp_ics_span_transport_source_image_raw_pn_cell_dot_pointwise_target * S ((S (fpmp_index_dot_mcp_ics_span_transport_source_image_raw_pn_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_span_transport_source_image_raw_pn_cell_dot) + (fpmp_target_dot_mcp_ics_span_transport_source_image_raw_pn_cell_dot_pointwise))) -> fpmp_target_dot_mcp_ics_span_transport_source_image_raw_pn_cell_dot_pointwise = fpmp_left_dot_mcp_ics_span_transport_source_image_raw_pn_cell_dot_pointwise * fpmp_right_dot_mcp_ics_span_transport_source_image_raw_pn_cell_dot_pointwise) /\ (exists ff_u_dot_mcp_ics_span_transport_source_image_raw_pn_cell_dot_sum ff_v_dot_mcp_ics_span_transport_source_image_raw_pn_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_span_transport_source_image_raw_pn_cell_dot_sum_start. ff_h_dot_mcp_ics_span_transport_source_image_raw_pn_cell_dot_sum_start + S (0) = S ((S (0)) * ff_v_dot_mcp_ics_span_transport_source_image_raw_pn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_span_transport_source_image_raw_pn_cell_dot_sum_start. ff_u_dot_mcp_ics_span_transport_source_image_raw_pn_cell_dot_sum = ff_q_dot_mcp_ics_span_transport_source_image_raw_pn_cell_dot_sum_start * S ((S (0)) * ff_v_dot_mcp_ics_span_transport_source_image_raw_pn_cell_dot_sum) + (0))) /\ ((((exists ff_h_dot_mcp_ics_span_transport_source_image_raw_pn_cell_dot_sum_terminal. ff_h_dot_mcp_ics_span_transport_source_image_raw_pn_cell_dot_sum_terminal + S (ff_value_mcp_prefix_ics_span_transport_source_image_raw_pn) = S ((S (w)) * ff_v_dot_mcp_ics_span_transport_source_image_raw_pn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_span_transport_source_image_raw_pn_cell_dot_sum_terminal. ff_u_dot_mcp_ics_span_transport_source_image_raw_pn_cell_dot_sum = ff_q_dot_mcp_ics_span_transport_source_image_raw_pn_cell_dot_sum_terminal * S ((S (w)) * ff_v_dot_mcp_ics_span_transport_source_image_raw_pn_cell_dot_sum) + (ff_value_mcp_prefix_ics_span_transport_source_image_raw_pn))) /\ forall ff_i_dot_mcp_ics_span_transport_source_image_raw_pn_cell_dot_sum. (exists ff_lt_dot_mcp_ics_span_transport_source_image_raw_pn_cell_dot_sum_bound. ff_lt_dot_mcp_ics_span_transport_source_image_raw_pn_cell_dot_sum_bound + S ff_i_dot_mcp_ics_span_transport_source_image_raw_pn_cell_dot_sum = w) -> exists ff_a_dot_mcp_ics_span_transport_source_image_raw_pn_cell_dot_sum ff_r_dot_mcp_ics_span_transport_source_image_raw_pn_cell_dot_sum ff_s_dot_mcp_ics_span_transport_source_image_raw_pn_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_span_transport_source_image_raw_pn_cell_dot_sum_summand. ff_h_dot_mcp_ics_span_transport_source_image_raw_pn_cell_dot_sum_summand + S (ff_a_dot_mcp_ics_span_transport_source_image_raw_pn_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_span_transport_source_image_raw_pn_cell_dot_sum)) * ff_scale_dot_mcp_ics_span_transport_source_image_raw_pn_cell_dot)) /\ exists ff_q_dot_mcp_ics_span_transport_source_image_raw_pn_cell_dot_sum_summand. ff_code_dot_mcp_ics_span_transport_source_image_raw_pn_cell_dot = ff_q_dot_mcp_ics_span_transport_source_image_raw_pn_cell_dot_sum_summand * S ((S (ff_i_dot_mcp_ics_span_transport_source_image_raw_pn_cell_dot_sum)) * ff_scale_dot_mcp_ics_span_transport_source_image_raw_pn_cell_dot) + (ff_a_dot_mcp_ics_span_transport_source_image_raw_pn_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_span_transport_source_image_raw_pn_cell_dot_sum_partial. ff_h_dot_mcp_ics_span_transport_source_image_raw_pn_cell_dot_sum_partial + S (ff_r_dot_mcp_ics_span_transport_source_image_raw_pn_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_span_transport_source_image_raw_pn_cell_dot_sum)) * ff_v_dot_mcp_ics_span_transport_source_image_raw_pn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_span_transport_source_image_raw_pn_cell_dot_sum_partial. ff_u_dot_mcp_ics_span_transport_source_image_raw_pn_cell_dot_sum = ff_q_dot_mcp_ics_span_transport_source_image_raw_pn_cell_dot_sum_partial * S ((S (ff_i_dot_mcp_ics_span_transport_source_image_raw_pn_cell_dot_sum)) * ff_v_dot_mcp_ics_span_transport_source_image_raw_pn_cell_dot_sum) + (ff_r_dot_mcp_ics_span_transport_source_image_raw_pn_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_span_transport_source_image_raw_pn_cell_dot_sum_successor. ff_h_dot_mcp_ics_span_transport_source_image_raw_pn_cell_dot_sum_successor + S (ff_s_dot_mcp_ics_span_transport_source_image_raw_pn_cell_dot_sum) = S ((S (S ff_i_dot_mcp_ics_span_transport_source_image_raw_pn_cell_dot_sum)) * ff_v_dot_mcp_ics_span_transport_source_image_raw_pn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_span_transport_source_image_raw_pn_cell_dot_sum_successor. ff_u_dot_mcp_ics_span_transport_source_image_raw_pn_cell_dot_sum = ff_q_dot_mcp_ics_span_transport_source_image_raw_pn_cell_dot_sum_successor * S ((S (S ff_i_dot_mcp_ics_span_transport_source_image_raw_pn_cell_dot_sum)) * ff_v_dot_mcp_ics_span_transport_source_image_raw_pn_cell_dot_sum) + (ff_s_dot_mcp_ics_span_transport_source_image_raw_pn_cell_dot_sum))) /\ ff_s_dot_mcp_ics_span_transport_source_image_raw_pn_cell_dot_sum = ff_r_dot_mcp_ics_span_transport_source_image_raw_pn_cell_dot_sum + ff_a_dot_mcp_ics_span_transport_source_image_raw_pn_cell_dot_sum))))))))))) /\ (((exists fs_h_mcp_ics_span_transport_source_image_raw_pn_entry. fs_h_mcp_ics_span_transport_source_image_raw_pn_entry + S (ff_value_mcp_prefix_ics_span_transport_source_image_raw_pn) = S ((S (ff_index_mcp_prefix_ics_span_transport_source_image_raw_pn)) * ff_pns_mcp_smatrix_ics_span_transport_source_image_raw)) /\ exists fs_q_mcp_ics_span_transport_source_image_raw_pn_entry. ff_pn_mcp_smatrix_ics_span_transport_source_image_raw = fs_q_mcp_ics_span_transport_source_image_raw_pn_entry * S ((S (ff_index_mcp_prefix_ics_span_transport_source_image_raw_pn)) * ff_pns_mcp_smatrix_ics_span_transport_source_image_raw) + (ff_value_mcp_prefix_ics_span_transport_source_image_raw_pn))))))) /\ ((forall ff_index_mcp_prefix_ics_span_transport_source_image_raw_np. (exists mcp_gap_ics_span_transport_source_image_raw_np_index. mcp_gap_ics_span_transport_source_image_raw_np_index + S (ff_index_mcp_prefix_ics_span_transport_source_image_raw_np) = ((r) * (1))) -> exists ff_row_mcp_prefix_ics_span_transport_source_image_raw_np ff_column_mcp_prefix_ics_span_transport_source_image_raw_np ff_value_mcp_prefix_ics_span_transport_source_image_raw_np. ((ff_index_mcp_prefix_ics_span_transport_source_image_raw_np) = (1) * ff_row_mcp_prefix_ics_span_transport_source_image_raw_np + ff_column_mcp_prefix_ics_span_transport_source_image_raw_np /\ ((exists mcp_gap_ics_span_transport_source_image_raw_np_column. mcp_gap_ics_span_transport_source_image_raw_np_column + S (ff_column_mcp_prefix_ics_span_transport_source_image_raw_np) = (1)) /\ ((exists ff_left_mcp_cell_ics_span_transport_source_image_raw_np_cell ff_left_scale_mcp_cell_ics_span_transport_source_image_raw_np_cell ff_right_mcp_cell_ics_span_transport_source_image_raw_np_cell ff_right_scale_mcp_cell_ics_span_transport_source_image_raw_np_cell. ((forall ff_index_mcp_ics_span_transport_source_image_raw_np_cell_row ff_source_mcp_ics_span_transport_source_image_raw_np_cell_row ff_target_mcp_ics_span_transport_source_image_raw_np_cell_row. (exists mcp_gap_ics_span_transport_source_image_raw_np_cell_row_bound. mcp_gap_ics_span_transport_source_image_raw_np_cell_row_bound + S (ff_index_mcp_ics_span_transport_source_image_raw_np_cell_row) = (w)) -> (((exists fs_h_mcp_ics_span_transport_source_image_raw_np_cell_row_source. fs_h_mcp_ics_span_transport_source_image_raw_np_cell_row_source + S (ff_source_mcp_ics_span_transport_source_image_raw_np_cell_row) = S ((S (((ff_row_mcp_prefix_ics_span_transport_source_image_raw_np) * (w)) + (1) * ff_index_mcp_ics_span_transport_source_image_raw_np_cell_row)) * dc)) /\ exists fs_q_mcp_ics_span_transport_source_image_raw_np_cell_row_source. db = fs_q_mcp_ics_span_transport_source_image_raw_np_cell_row_source * S ((S (((ff_row_mcp_prefix_ics_span_transport_source_image_raw_np) * (w)) + (1) * ff_index_mcp_ics_span_transport_source_image_raw_np_cell_row)) * dc) + (ff_source_mcp_ics_span_transport_source_image_raw_np_cell_row))) -> (((exists fs_h_mcp_ics_span_transport_source_image_raw_np_cell_row_target. fs_h_mcp_ics_span_transport_source_image_raw_np_cell_row_target + S (ff_target_mcp_ics_span_transport_source_image_raw_np_cell_row) = S ((S (ff_index_mcp_ics_span_transport_source_image_raw_np_cell_row)) * ff_left_scale_mcp_cell_ics_span_transport_source_image_raw_np_cell)) /\ exists fs_q_mcp_ics_span_transport_source_image_raw_np_cell_row_target. ff_left_mcp_cell_ics_span_transport_source_image_raw_np_cell = fs_q_mcp_ics_span_transport_source_image_raw_np_cell_row_target * S ((S (ff_index_mcp_ics_span_transport_source_image_raw_np_cell_row)) * ff_left_scale_mcp_cell_ics_span_transport_source_image_raw_np_cell) + (ff_target_mcp_ics_span_transport_source_image_raw_np_cell_row))) -> ff_target_mcp_ics_span_transport_source_image_raw_np_cell_row = ff_source_mcp_ics_span_transport_source_image_raw_np_cell_row) /\ ((forall ff_index_mcp_ics_span_transport_source_image_raw_np_cell_column ff_source_mcp_ics_span_transport_source_image_raw_np_cell_column ff_target_mcp_ics_span_transport_source_image_raw_np_cell_column. (exists mcp_gap_ics_span_transport_source_image_raw_np_cell_column_bound. mcp_gap_ics_span_transport_source_image_raw_np_cell_column_bound + S (ff_index_mcp_ics_span_transport_source_image_raw_np_cell_column) = (w)) -> (((exists fs_h_mcp_ics_span_transport_source_image_raw_np_cell_column_source. fs_h_mcp_ics_span_transport_source_image_raw_np_cell_column_source + S (ff_source_mcp_ics_span_transport_source_image_raw_np_cell_column) = S ((S ((ff_column_mcp_prefix_ics_span_transport_source_image_raw_np) + (1) * ff_index_mcp_ics_span_transport_source_image_raw_np_cell_column)) * ics_coefficient_positive_scale_span_transport_source)) /\ exists fs_q_mcp_ics_span_transport_source_image_raw_np_cell_column_source. ics_coefficient_positive_span_transport_source = fs_q_mcp_ics_span_transport_source_image_raw_np_cell_column_source * S ((S ((ff_column_mcp_prefix_ics_span_transport_source_image_raw_np) + (1) * ff_index_mcp_ics_span_transport_source_image_raw_np_cell_column)) * ics_coefficient_positive_scale_span_transport_source) + (ff_source_mcp_ics_span_transport_source_image_raw_np_cell_column))) -> (((exists fs_h_mcp_ics_span_transport_source_image_raw_np_cell_column_target. fs_h_mcp_ics_span_transport_source_image_raw_np_cell_column_target + S (ff_target_mcp_ics_span_transport_source_image_raw_np_cell_column) = S ((S (ff_index_mcp_ics_span_transport_source_image_raw_np_cell_column)) * ff_right_scale_mcp_cell_ics_span_transport_source_image_raw_np_cell)) /\ exists fs_q_mcp_ics_span_transport_source_image_raw_np_cell_column_target. ff_right_mcp_cell_ics_span_transport_source_image_raw_np_cell = fs_q_mcp_ics_span_transport_source_image_raw_np_cell_column_target * S ((S (ff_index_mcp_ics_span_transport_source_image_raw_np_cell_column)) * ff_right_scale_mcp_cell_ics_span_transport_source_image_raw_np_cell) + (ff_target_mcp_ics_span_transport_source_image_raw_np_cell_column))) -> ff_target_mcp_ics_span_transport_source_image_raw_np_cell_column = ff_source_mcp_ics_span_transport_source_image_raw_np_cell_column) /\ (exists ff_code_dot_mcp_ics_span_transport_source_image_raw_np_cell_dot ff_scale_dot_mcp_ics_span_transport_source_image_raw_np_cell_dot. ((forall fpmp_index_dot_mcp_ics_span_transport_source_image_raw_np_cell_dot_pointwise fpmp_left_dot_mcp_ics_span_transport_source_image_raw_np_cell_dot_pointwise fpmp_right_dot_mcp_ics_span_transport_source_image_raw_np_cell_dot_pointwise fpmp_target_dot_mcp_ics_span_transport_source_image_raw_np_cell_dot_pointwise. (exists fpmp_gap_dot_mcp_ics_span_transport_source_image_raw_np_cell_dot_pointwise. fpmp_gap_dot_mcp_ics_span_transport_source_image_raw_np_cell_dot_pointwise + S fpmp_index_dot_mcp_ics_span_transport_source_image_raw_np_cell_dot_pointwise = w) -> (((exists ff_h_fpmp_dot_mcp_ics_span_transport_source_image_raw_np_cell_dot_pointwise_left. ff_h_fpmp_dot_mcp_ics_span_transport_source_image_raw_np_cell_dot_pointwise_left + S (fpmp_left_dot_mcp_ics_span_transport_source_image_raw_np_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_span_transport_source_image_raw_np_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_span_transport_source_image_raw_np_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_span_transport_source_image_raw_np_cell_dot_pointwise_left. ff_left_mcp_cell_ics_span_transport_source_image_raw_np_cell = ff_q_fpmp_dot_mcp_ics_span_transport_source_image_raw_np_cell_dot_pointwise_left * S ((S (fpmp_index_dot_mcp_ics_span_transport_source_image_raw_np_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_span_transport_source_image_raw_np_cell) + (fpmp_left_dot_mcp_ics_span_transport_source_image_raw_np_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_span_transport_source_image_raw_np_cell_dot_pointwise_right. ff_h_fpmp_dot_mcp_ics_span_transport_source_image_raw_np_cell_dot_pointwise_right + S (fpmp_right_dot_mcp_ics_span_transport_source_image_raw_np_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_span_transport_source_image_raw_np_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_span_transport_source_image_raw_np_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_span_transport_source_image_raw_np_cell_dot_pointwise_right. ff_right_mcp_cell_ics_span_transport_source_image_raw_np_cell = ff_q_fpmp_dot_mcp_ics_span_transport_source_image_raw_np_cell_dot_pointwise_right * S ((S (fpmp_index_dot_mcp_ics_span_transport_source_image_raw_np_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_span_transport_source_image_raw_np_cell) + (fpmp_right_dot_mcp_ics_span_transport_source_image_raw_np_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_span_transport_source_image_raw_np_cell_dot_pointwise_target. ff_h_fpmp_dot_mcp_ics_span_transport_source_image_raw_np_cell_dot_pointwise_target + S (fpmp_target_dot_mcp_ics_span_transport_source_image_raw_np_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_span_transport_source_image_raw_np_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_span_transport_source_image_raw_np_cell_dot)) /\ exists ff_q_fpmp_dot_mcp_ics_span_transport_source_image_raw_np_cell_dot_pointwise_target. ff_code_dot_mcp_ics_span_transport_source_image_raw_np_cell_dot = ff_q_fpmp_dot_mcp_ics_span_transport_source_image_raw_np_cell_dot_pointwise_target * S ((S (fpmp_index_dot_mcp_ics_span_transport_source_image_raw_np_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_span_transport_source_image_raw_np_cell_dot) + (fpmp_target_dot_mcp_ics_span_transport_source_image_raw_np_cell_dot_pointwise))) -> fpmp_target_dot_mcp_ics_span_transport_source_image_raw_np_cell_dot_pointwise = fpmp_left_dot_mcp_ics_span_transport_source_image_raw_np_cell_dot_pointwise * fpmp_right_dot_mcp_ics_span_transport_source_image_raw_np_cell_dot_pointwise) /\ (exists ff_u_dot_mcp_ics_span_transport_source_image_raw_np_cell_dot_sum ff_v_dot_mcp_ics_span_transport_source_image_raw_np_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_span_transport_source_image_raw_np_cell_dot_sum_start. ff_h_dot_mcp_ics_span_transport_source_image_raw_np_cell_dot_sum_start + S (0) = S ((S (0)) * ff_v_dot_mcp_ics_span_transport_source_image_raw_np_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_span_transport_source_image_raw_np_cell_dot_sum_start. ff_u_dot_mcp_ics_span_transport_source_image_raw_np_cell_dot_sum = ff_q_dot_mcp_ics_span_transport_source_image_raw_np_cell_dot_sum_start * S ((S (0)) * ff_v_dot_mcp_ics_span_transport_source_image_raw_np_cell_dot_sum) + (0))) /\ ((((exists ff_h_dot_mcp_ics_span_transport_source_image_raw_np_cell_dot_sum_terminal. ff_h_dot_mcp_ics_span_transport_source_image_raw_np_cell_dot_sum_terminal + S (ff_value_mcp_prefix_ics_span_transport_source_image_raw_np) = S ((S (w)) * ff_v_dot_mcp_ics_span_transport_source_image_raw_np_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_span_transport_source_image_raw_np_cell_dot_sum_terminal. ff_u_dot_mcp_ics_span_transport_source_image_raw_np_cell_dot_sum = ff_q_dot_mcp_ics_span_transport_source_image_raw_np_cell_dot_sum_terminal * S ((S (w)) * ff_v_dot_mcp_ics_span_transport_source_image_raw_np_cell_dot_sum) + (ff_value_mcp_prefix_ics_span_transport_source_image_raw_np))) /\ forall ff_i_dot_mcp_ics_span_transport_source_image_raw_np_cell_dot_sum. (exists ff_lt_dot_mcp_ics_span_transport_source_image_raw_np_cell_dot_sum_bound. ff_lt_dot_mcp_ics_span_transport_source_image_raw_np_cell_dot_sum_bound + S ff_i_dot_mcp_ics_span_transport_source_image_raw_np_cell_dot_sum = w) -> exists ff_a_dot_mcp_ics_span_transport_source_image_raw_np_cell_dot_sum ff_r_dot_mcp_ics_span_transport_source_image_raw_np_cell_dot_sum ff_s_dot_mcp_ics_span_transport_source_image_raw_np_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_span_transport_source_image_raw_np_cell_dot_sum_summand. ff_h_dot_mcp_ics_span_transport_source_image_raw_np_cell_dot_sum_summand + S (ff_a_dot_mcp_ics_span_transport_source_image_raw_np_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_span_transport_source_image_raw_np_cell_dot_sum)) * ff_scale_dot_mcp_ics_span_transport_source_image_raw_np_cell_dot)) /\ exists ff_q_dot_mcp_ics_span_transport_source_image_raw_np_cell_dot_sum_summand. ff_code_dot_mcp_ics_span_transport_source_image_raw_np_cell_dot = ff_q_dot_mcp_ics_span_transport_source_image_raw_np_cell_dot_sum_summand * S ((S (ff_i_dot_mcp_ics_span_transport_source_image_raw_np_cell_dot_sum)) * ff_scale_dot_mcp_ics_span_transport_source_image_raw_np_cell_dot) + (ff_a_dot_mcp_ics_span_transport_source_image_raw_np_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_span_transport_source_image_raw_np_cell_dot_sum_partial. ff_h_dot_mcp_ics_span_transport_source_image_raw_np_cell_dot_sum_partial + S (ff_r_dot_mcp_ics_span_transport_source_image_raw_np_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_span_transport_source_image_raw_np_cell_dot_sum)) * ff_v_dot_mcp_ics_span_transport_source_image_raw_np_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_span_transport_source_image_raw_np_cell_dot_sum_partial. ff_u_dot_mcp_ics_span_transport_source_image_raw_np_cell_dot_sum = ff_q_dot_mcp_ics_span_transport_source_image_raw_np_cell_dot_sum_partial * S ((S (ff_i_dot_mcp_ics_span_transport_source_image_raw_np_cell_dot_sum)) * ff_v_dot_mcp_ics_span_transport_source_image_raw_np_cell_dot_sum) + (ff_r_dot_mcp_ics_span_transport_source_image_raw_np_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_span_transport_source_image_raw_np_cell_dot_sum_successor. ff_h_dot_mcp_ics_span_transport_source_image_raw_np_cell_dot_sum_successor + S (ff_s_dot_mcp_ics_span_transport_source_image_raw_np_cell_dot_sum) = S ((S (S ff_i_dot_mcp_ics_span_transport_source_image_raw_np_cell_dot_sum)) * ff_v_dot_mcp_ics_span_transport_source_image_raw_np_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_span_transport_source_image_raw_np_cell_dot_sum_successor. ff_u_dot_mcp_ics_span_transport_source_image_raw_np_cell_dot_sum = ff_q_dot_mcp_ics_span_transport_source_image_raw_np_cell_dot_sum_successor * S ((S (S ff_i_dot_mcp_ics_span_transport_source_image_raw_np_cell_dot_sum)) * ff_v_dot_mcp_ics_span_transport_source_image_raw_np_cell_dot_sum) + (ff_s_dot_mcp_ics_span_transport_source_image_raw_np_cell_dot_sum))) /\ ff_s_dot_mcp_ics_span_transport_source_image_raw_np_cell_dot_sum = ff_r_dot_mcp_ics_span_transport_source_image_raw_np_cell_dot_sum + ff_a_dot_mcp_ics_span_transport_source_image_raw_np_cell_dot_sum))))))))))) /\ (((exists fs_h_mcp_ics_span_transport_source_image_raw_np_entry. fs_h_mcp_ics_span_transport_source_image_raw_np_entry + S (ff_value_mcp_prefix_ics_span_transport_source_image_raw_np) = S ((S (ff_index_mcp_prefix_ics_span_transport_source_image_raw_np)) * ff_nps_mcp_smatrix_ics_span_transport_source_image_raw)) /\ exists fs_q_mcp_ics_span_transport_source_image_raw_np_entry. ff_np_mcp_smatrix_ics_span_transport_source_image_raw = fs_q_mcp_ics_span_transport_source_image_raw_np_entry * S ((S (ff_index_mcp_prefix_ics_span_transport_source_image_raw_np)) * ff_nps_mcp_smatrix_ics_span_transport_source_image_raw) + (ff_value_mcp_prefix_ics_span_transport_source_image_raw_np))))))) /\ ((forall ff_index_mcp_add_ics_span_transport_source_image_raw_positive ff_left_mcp_add_ics_span_transport_source_image_raw_positive ff_right_mcp_add_ics_span_transport_source_image_raw_positive ff_target_mcp_add_ics_span_transport_source_image_raw_positive. (exists mcp_gap_ics_span_transport_source_image_raw_positive_bound. mcp_gap_ics_span_transport_source_image_raw_positive_bound + S (ff_index_mcp_add_ics_span_transport_source_image_raw_positive) = ((r) * (1))) -> (((exists fs_h_mcp_ics_span_transport_source_image_raw_positive_left. fs_h_mcp_ics_span_transport_source_image_raw_positive_left + S (ff_left_mcp_add_ics_span_transport_source_image_raw_positive) = S ((S (ff_index_mcp_add_ics_span_transport_source_image_raw_positive)) * ff_pps_mcp_smatrix_ics_span_transport_source_image_raw)) /\ exists fs_q_mcp_ics_span_transport_source_image_raw_positive_left. ff_pp_mcp_smatrix_ics_span_transport_source_image_raw = fs_q_mcp_ics_span_transport_source_image_raw_positive_left * S ((S (ff_index_mcp_add_ics_span_transport_source_image_raw_positive)) * ff_pps_mcp_smatrix_ics_span_transport_source_image_raw) + (ff_left_mcp_add_ics_span_transport_source_image_raw_positive))) -> (((exists fs_h_mcp_ics_span_transport_source_image_raw_positive_right. fs_h_mcp_ics_span_transport_source_image_raw_positive_right + S (ff_right_mcp_add_ics_span_transport_source_image_raw_positive) = S ((S (ff_index_mcp_add_ics_span_transport_source_image_raw_positive)) * ff_nns_mcp_smatrix_ics_span_transport_source_image_raw)) /\ exists fs_q_mcp_ics_span_transport_source_image_raw_positive_right. ff_nn_mcp_smatrix_ics_span_transport_source_image_raw = fs_q_mcp_ics_span_transport_source_image_raw_positive_right * S ((S (ff_index_mcp_add_ics_span_transport_source_image_raw_positive)) * ff_nns_mcp_smatrix_ics_span_transport_source_image_raw) + (ff_right_mcp_add_ics_span_transport_source_image_raw_positive))) -> (((exists fs_h_mcp_ics_span_transport_source_image_raw_positive_target. fs_h_mcp_ics_span_transport_source_image_raw_positive_target + S (ff_target_mcp_add_ics_span_transport_source_image_raw_positive) = S ((S (ff_index_mcp_add_ics_span_transport_source_image_raw_positive)) * ics_raw_positive_scale_span_transport_source_image)) /\ exists fs_q_mcp_ics_span_transport_source_image_raw_positive_target. ics_raw_positive_span_transport_source_image = fs_q_mcp_ics_span_transport_source_image_raw_positive_target * S ((S (ff_index_mcp_add_ics_span_transport_source_image_raw_positive)) * ics_raw_positive_scale_span_transport_source_image) + (ff_target_mcp_add_ics_span_transport_source_image_raw_positive))) -> ff_target_mcp_add_ics_span_transport_source_image_raw_positive = ff_left_mcp_add_ics_span_transport_source_image_raw_positive + ff_right_mcp_add_ics_span_transport_source_image_raw_positive) /\ (forall ff_index_mcp_add_ics_span_transport_source_image_raw_negative ff_left_mcp_add_ics_span_transport_source_image_raw_negative ff_right_mcp_add_ics_span_transport_source_image_raw_negative ff_target_mcp_add_ics_span_transport_source_image_raw_negative. (exists mcp_gap_ics_span_transport_source_image_raw_negative_bound. mcp_gap_ics_span_transport_source_image_raw_negative_bound + S (ff_index_mcp_add_ics_span_transport_source_image_raw_negative) = ((r) * (1))) -> (((exists fs_h_mcp_ics_span_transport_source_image_raw_negative_left. fs_h_mcp_ics_span_transport_source_image_raw_negative_left + S (ff_left_mcp_add_ics_span_transport_source_image_raw_negative) = S ((S (ff_index_mcp_add_ics_span_transport_source_image_raw_negative)) * ff_pns_mcp_smatrix_ics_span_transport_source_image_raw)) /\ exists fs_q_mcp_ics_span_transport_source_image_raw_negative_left. ff_pn_mcp_smatrix_ics_span_transport_source_image_raw = fs_q_mcp_ics_span_transport_source_image_raw_negative_left * S ((S (ff_index_mcp_add_ics_span_transport_source_image_raw_negative)) * ff_pns_mcp_smatrix_ics_span_transport_source_image_raw) + (ff_left_mcp_add_ics_span_transport_source_image_raw_negative))) -> (((exists fs_h_mcp_ics_span_transport_source_image_raw_negative_right. fs_h_mcp_ics_span_transport_source_image_raw_negative_right + S (ff_right_mcp_add_ics_span_transport_source_image_raw_negative) = S ((S (ff_index_mcp_add_ics_span_transport_source_image_raw_negative)) * ff_nps_mcp_smatrix_ics_span_transport_source_image_raw)) /\ exists fs_q_mcp_ics_span_transport_source_image_raw_negative_right. ff_np_mcp_smatrix_ics_span_transport_source_image_raw = fs_q_mcp_ics_span_transport_source_image_raw_negative_right * S ((S (ff_index_mcp_add_ics_span_transport_source_image_raw_negative)) * ff_nps_mcp_smatrix_ics_span_transport_source_image_raw) + (ff_right_mcp_add_ics_span_transport_source_image_raw_negative))) -> (((exists fs_h_mcp_ics_span_transport_source_image_raw_negative_target. fs_h_mcp_ics_span_transport_source_image_raw_negative_target + S (ff_target_mcp_add_ics_span_transport_source_image_raw_negative) = S ((S (ff_index_mcp_add_ics_span_transport_source_image_raw_negative)) * ics_raw_negative_scale_span_transport_source_image)) /\ exists fs_q_mcp_ics_span_transport_source_image_raw_negative_target. ics_raw_negative_span_transport_source_image = fs_q_mcp_ics_span_transport_source_image_raw_negative_target * S ((S (ff_index_mcp_add_ics_span_transport_source_image_raw_negative)) * ics_raw_negative_scale_span_transport_source_image) + (ff_target_mcp_add_ics_span_transport_source_image_raw_negative))) -> ff_target_mcp_add_ics_span_transport_source_image_raw_negative = ff_left_mcp_add_ics_span_transport_source_image_raw_negative + ff_right_mcp_add_ics_span_transport_source_image_raw_negative))))))) /\ (forall ics_index_span_transport_source_image_equal ics_value0_span_transport_source_image_equal ics_value1_span_transport_source_image_equal ics_value2_span_transport_source_image_equal ics_value3_span_transport_source_image_equal. (exists ics_gap_span_transport_source_image_equal_bound. ics_gap_span_transport_source_image_equal_bound + S (ics_index_span_transport_source_image_equal) = (r)) -> (((exists fs_h_ics_span_transport_source_image_equal_at0. fs_h_ics_span_transport_source_image_equal_at0 + S (ics_value0_span_transport_source_image_equal) = S ((S (ics_index_span_transport_source_image_equal)) * ics_raw_positive_scale_span_transport_source_image)) /\ exists fs_q_ics_span_transport_source_image_equal_at0. ics_raw_positive_span_transport_source_image = fs_q_ics_span_transport_source_image_equal_at0 * S ((S (ics_index_span_transport_source_image_equal)) * ics_raw_positive_scale_span_transport_source_image) + (ics_value0_span_transport_source_image_equal))) -> (((exists fs_h_ics_span_transport_source_image_equal_at1. fs_h_ics_span_transport_source_image_equal_at1 + S (ics_value1_span_transport_source_image_equal) = S ((S (ics_index_span_transport_source_image_equal)) * ics_raw_negative_scale_span_transport_source_image)) /\ exists fs_q_ics_span_transport_source_image_equal_at1. ics_raw_negative_span_transport_source_image = fs_q_ics_span_transport_source_image_equal_at1 * S ((S (ics_index_span_transport_source_image_equal)) * ics_raw_negative_scale_span_transport_source_image) + (ics_value1_span_transport_source_image_equal))) -> (((exists fs_h_ics_span_transport_source_image_equal_at2. fs_h_ics_span_transport_source_image_equal_at2 + S (ics_value2_span_transport_source_image_equal) = S ((S (ics_index_span_transport_source_image_equal)) * pc)) /\ exists fs_q_ics_span_transport_source_image_equal_at2. pb = fs_q_ics_span_transport_source_image_equal_at2 * S ((S (ics_index_span_transport_source_image_equal)) * pc) + (ics_value2_span_transport_source_image_equal))) -> (((exists fs_h_ics_span_transport_source_image_equal_at3. fs_h_ics_span_transport_source_image_equal_at3 + S (ics_value3_span_transport_source_image_equal) = S ((S (ics_index_span_transport_source_image_equal)) * nc)) /\ exists fs_q_ics_span_transport_source_image_equal_at3. nb = fs_q_ics_span_transport_source_image_equal_at3 * S ((S (ics_index_span_transport_source_image_equal)) * nc) + (ics_value3_span_transport_source_image_equal))) -> ics_value0_span_transport_source_image_equal + ics_value3_span_transport_source_image_equal = ics_value2_span_transport_source_image_equal + ics_value1_span_transport_source_image_equal))))) -> (forall ics_index_span_transport_equal ics_value0_span_transport_equal ics_value1_span_transport_equal ics_value2_span_transport_equal ics_value3_span_transport_equal. (exists ics_gap_span_transport_equal_bound. ics_gap_span_transport_equal_bound + S (ics_index_span_transport_equal) = (r)) -> (((exists fs_h_ics_span_transport_equal_at0. fs_h_ics_span_transport_equal_at0 + S (ics_value0_span_transport_equal) = S ((S (ics_index_span_transport_equal)) * pc)) /\ exists fs_q_ics_span_transport_equal_at0. pb = fs_q_ics_span_transport_equal_at0 * S ((S (ics_index_span_transport_equal)) * pc) + (ics_value0_span_transport_equal))) -> (((exists fs_h_ics_span_transport_equal_at1. fs_h_ics_span_transport_equal_at1 + S (ics_value1_span_transport_equal) = S ((S (ics_index_span_transport_equal)) * nc)) /\ exists fs_q_ics_span_transport_equal_at1. nb = fs_q_ics_span_transport_equal_at1 * S ((S (ics_index_span_transport_equal)) * nc) + (ics_value1_span_transport_equal))) -> (((exists fs_h_ics_span_transport_equal_at2. fs_h_ics_span_transport_equal_at2 + S (ics_value2_span_transport_equal) = S ((S (ics_index_span_transport_equal)) * qc)) /\ exists fs_q_ics_span_transport_equal_at2. qb = fs_q_ics_span_transport_equal_at2 * S ((S (ics_index_span_transport_equal)) * qc) + (ics_value2_span_transport_equal))) -> (((exists fs_h_ics_span_transport_equal_at3. fs_h_ics_span_transport_equal_at3 + S (ics_value3_span_transport_equal) = S ((S (ics_index_span_transport_equal)) * mc)) /\ exists fs_q_ics_span_transport_equal_at3. mb = fs_q_ics_span_transport_equal_at3 * S ((S (ics_index_span_transport_equal)) * mc) + (ics_value3_span_transport_equal))) -> ics_value0_span_transport_equal + ics_value3_span_transport_equal = ics_value2_span_transport_equal + ics_value1_span_transport_equal) -> (exists ics_coefficient_positive_span_transport_result ics_coefficient_positive_scale_span_transport_result ics_coefficient_negative_span_transport_result ics_coefficient_negative_scale_span_transport_result. (exists ics_raw_positive_span_transport_result_image ics_raw_positive_scale_span_transport_result_image ics_raw_negative_span_transport_result_image ics_raw_negative_scale_span_transport_result_image. (((exists ff_pp_mcp_smatrix_ics_span_transport_result_image_raw ff_pps_mcp_smatrix_ics_span_transport_result_image_raw ff_nn_mcp_smatrix_ics_span_transport_result_image_raw ff_nns_mcp_smatrix_ics_span_transport_result_image_raw ff_pn_mcp_smatrix_ics_span_transport_result_image_raw ff_pns_mcp_smatrix_ics_span_transport_result_image_raw ff_np_mcp_smatrix_ics_span_transport_result_image_raw ff_nps_mcp_smatrix_ics_span_transport_result_image_raw. ((forall ff_index_mcp_prefix_ics_span_transport_result_image_raw_pp. (exists mcp_gap_ics_span_transport_result_image_raw_pp_index. mcp_gap_ics_span_transport_result_image_raw_pp_index + S (ff_index_mcp_prefix_ics_span_transport_result_image_raw_pp) = ((r) * (1))) -> exists ff_row_mcp_prefix_ics_span_transport_result_image_raw_pp ff_column_mcp_prefix_ics_span_transport_result_image_raw_pp ff_value_mcp_prefix_ics_span_transport_result_image_raw_pp. ((ff_index_mcp_prefix_ics_span_transport_result_image_raw_pp) = (1) * ff_row_mcp_prefix_ics_span_transport_result_image_raw_pp + ff_column_mcp_prefix_ics_span_transport_result_image_raw_pp /\ ((exists mcp_gap_ics_span_transport_result_image_raw_pp_column. mcp_gap_ics_span_transport_result_image_raw_pp_column + S (ff_column_mcp_prefix_ics_span_transport_result_image_raw_pp) = (1)) /\ ((exists ff_left_mcp_cell_ics_span_transport_result_image_raw_pp_cell ff_left_scale_mcp_cell_ics_span_transport_result_image_raw_pp_cell ff_right_mcp_cell_ics_span_transport_result_image_raw_pp_cell ff_right_scale_mcp_cell_ics_span_transport_result_image_raw_pp_cell. ((forall ff_index_mcp_ics_span_transport_result_image_raw_pp_cell_row ff_source_mcp_ics_span_transport_result_image_raw_pp_cell_row ff_target_mcp_ics_span_transport_result_image_raw_pp_cell_row. (exists mcp_gap_ics_span_transport_result_image_raw_pp_cell_row_bound. mcp_gap_ics_span_transport_result_image_raw_pp_cell_row_bound + S (ff_index_mcp_ics_span_transport_result_image_raw_pp_cell_row) = (w)) -> (((exists fs_h_mcp_ics_span_transport_result_image_raw_pp_cell_row_source. fs_h_mcp_ics_span_transport_result_image_raw_pp_cell_row_source + S (ff_source_mcp_ics_span_transport_result_image_raw_pp_cell_row) = S ((S (((ff_row_mcp_prefix_ics_span_transport_result_image_raw_pp) * (w)) + (1) * ff_index_mcp_ics_span_transport_result_image_raw_pp_cell_row)) * ac)) /\ exists fs_q_mcp_ics_span_transport_result_image_raw_pp_cell_row_source. ab = fs_q_mcp_ics_span_transport_result_image_raw_pp_cell_row_source * S ((S (((ff_row_mcp_prefix_ics_span_transport_result_image_raw_pp) * (w)) + (1) * ff_index_mcp_ics_span_transport_result_image_raw_pp_cell_row)) * ac) + (ff_source_mcp_ics_span_transport_result_image_raw_pp_cell_row))) -> (((exists fs_h_mcp_ics_span_transport_result_image_raw_pp_cell_row_target. fs_h_mcp_ics_span_transport_result_image_raw_pp_cell_row_target + S (ff_target_mcp_ics_span_transport_result_image_raw_pp_cell_row) = S ((S (ff_index_mcp_ics_span_transport_result_image_raw_pp_cell_row)) * ff_left_scale_mcp_cell_ics_span_transport_result_image_raw_pp_cell)) /\ exists fs_q_mcp_ics_span_transport_result_image_raw_pp_cell_row_target. ff_left_mcp_cell_ics_span_transport_result_image_raw_pp_cell = fs_q_mcp_ics_span_transport_result_image_raw_pp_cell_row_target * S ((S (ff_index_mcp_ics_span_transport_result_image_raw_pp_cell_row)) * ff_left_scale_mcp_cell_ics_span_transport_result_image_raw_pp_cell) + (ff_target_mcp_ics_span_transport_result_image_raw_pp_cell_row))) -> ff_target_mcp_ics_span_transport_result_image_raw_pp_cell_row = ff_source_mcp_ics_span_transport_result_image_raw_pp_cell_row) /\ ((forall ff_index_mcp_ics_span_transport_result_image_raw_pp_cell_column ff_source_mcp_ics_span_transport_result_image_raw_pp_cell_column ff_target_mcp_ics_span_transport_result_image_raw_pp_cell_column. (exists mcp_gap_ics_span_transport_result_image_raw_pp_cell_column_bound. mcp_gap_ics_span_transport_result_image_raw_pp_cell_column_bound + S (ff_index_mcp_ics_span_transport_result_image_raw_pp_cell_column) = (w)) -> (((exists fs_h_mcp_ics_span_transport_result_image_raw_pp_cell_column_source. fs_h_mcp_ics_span_transport_result_image_raw_pp_cell_column_source + S (ff_source_mcp_ics_span_transport_result_image_raw_pp_cell_column) = S ((S ((ff_column_mcp_prefix_ics_span_transport_result_image_raw_pp) + (1) * ff_index_mcp_ics_span_transport_result_image_raw_pp_cell_column)) * ics_coefficient_positive_scale_span_transport_result)) /\ exists fs_q_mcp_ics_span_transport_result_image_raw_pp_cell_column_source. ics_coefficient_positive_span_transport_result = fs_q_mcp_ics_span_transport_result_image_raw_pp_cell_column_source * S ((S ((ff_column_mcp_prefix_ics_span_transport_result_image_raw_pp) + (1) * ff_index_mcp_ics_span_transport_result_image_raw_pp_cell_column)) * ics_coefficient_positive_scale_span_transport_result) + (ff_source_mcp_ics_span_transport_result_image_raw_pp_cell_column))) -> (((exists fs_h_mcp_ics_span_transport_result_image_raw_pp_cell_column_target. fs_h_mcp_ics_span_transport_result_image_raw_pp_cell_column_target + S (ff_target_mcp_ics_span_transport_result_image_raw_pp_cell_column) = S ((S (ff_index_mcp_ics_span_transport_result_image_raw_pp_cell_column)) * ff_right_scale_mcp_cell_ics_span_transport_result_image_raw_pp_cell)) /\ exists fs_q_mcp_ics_span_transport_result_image_raw_pp_cell_column_target. ff_right_mcp_cell_ics_span_transport_result_image_raw_pp_cell = fs_q_mcp_ics_span_transport_result_image_raw_pp_cell_column_target * S ((S (ff_index_mcp_ics_span_transport_result_image_raw_pp_cell_column)) * ff_right_scale_mcp_cell_ics_span_transport_result_image_raw_pp_cell) + (ff_target_mcp_ics_span_transport_result_image_raw_pp_cell_column))) -> ff_target_mcp_ics_span_transport_result_image_raw_pp_cell_column = ff_source_mcp_ics_span_transport_result_image_raw_pp_cell_column) /\ (exists ff_code_dot_mcp_ics_span_transport_result_image_raw_pp_cell_dot ff_scale_dot_mcp_ics_span_transport_result_image_raw_pp_cell_dot. ((forall fpmp_index_dot_mcp_ics_span_transport_result_image_raw_pp_cell_dot_pointwise fpmp_left_dot_mcp_ics_span_transport_result_image_raw_pp_cell_dot_pointwise fpmp_right_dot_mcp_ics_span_transport_result_image_raw_pp_cell_dot_pointwise fpmp_target_dot_mcp_ics_span_transport_result_image_raw_pp_cell_dot_pointwise. (exists fpmp_gap_dot_mcp_ics_span_transport_result_image_raw_pp_cell_dot_pointwise. fpmp_gap_dot_mcp_ics_span_transport_result_image_raw_pp_cell_dot_pointwise + S fpmp_index_dot_mcp_ics_span_transport_result_image_raw_pp_cell_dot_pointwise = w) -> (((exists ff_h_fpmp_dot_mcp_ics_span_transport_result_image_raw_pp_cell_dot_pointwise_left. ff_h_fpmp_dot_mcp_ics_span_transport_result_image_raw_pp_cell_dot_pointwise_left + S (fpmp_left_dot_mcp_ics_span_transport_result_image_raw_pp_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_span_transport_result_image_raw_pp_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_span_transport_result_image_raw_pp_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_span_transport_result_image_raw_pp_cell_dot_pointwise_left. ff_left_mcp_cell_ics_span_transport_result_image_raw_pp_cell = ff_q_fpmp_dot_mcp_ics_span_transport_result_image_raw_pp_cell_dot_pointwise_left * S ((S (fpmp_index_dot_mcp_ics_span_transport_result_image_raw_pp_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_span_transport_result_image_raw_pp_cell) + (fpmp_left_dot_mcp_ics_span_transport_result_image_raw_pp_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_span_transport_result_image_raw_pp_cell_dot_pointwise_right. ff_h_fpmp_dot_mcp_ics_span_transport_result_image_raw_pp_cell_dot_pointwise_right + S (fpmp_right_dot_mcp_ics_span_transport_result_image_raw_pp_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_span_transport_result_image_raw_pp_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_span_transport_result_image_raw_pp_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_span_transport_result_image_raw_pp_cell_dot_pointwise_right. ff_right_mcp_cell_ics_span_transport_result_image_raw_pp_cell = ff_q_fpmp_dot_mcp_ics_span_transport_result_image_raw_pp_cell_dot_pointwise_right * S ((S (fpmp_index_dot_mcp_ics_span_transport_result_image_raw_pp_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_span_transport_result_image_raw_pp_cell) + (fpmp_right_dot_mcp_ics_span_transport_result_image_raw_pp_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_span_transport_result_image_raw_pp_cell_dot_pointwise_target. ff_h_fpmp_dot_mcp_ics_span_transport_result_image_raw_pp_cell_dot_pointwise_target + S (fpmp_target_dot_mcp_ics_span_transport_result_image_raw_pp_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_span_transport_result_image_raw_pp_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_span_transport_result_image_raw_pp_cell_dot)) /\ exists ff_q_fpmp_dot_mcp_ics_span_transport_result_image_raw_pp_cell_dot_pointwise_target. ff_code_dot_mcp_ics_span_transport_result_image_raw_pp_cell_dot = ff_q_fpmp_dot_mcp_ics_span_transport_result_image_raw_pp_cell_dot_pointwise_target * S ((S (fpmp_index_dot_mcp_ics_span_transport_result_image_raw_pp_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_span_transport_result_image_raw_pp_cell_dot) + (fpmp_target_dot_mcp_ics_span_transport_result_image_raw_pp_cell_dot_pointwise))) -> fpmp_target_dot_mcp_ics_span_transport_result_image_raw_pp_cell_dot_pointwise = fpmp_left_dot_mcp_ics_span_transport_result_image_raw_pp_cell_dot_pointwise * fpmp_right_dot_mcp_ics_span_transport_result_image_raw_pp_cell_dot_pointwise) /\ (exists ff_u_dot_mcp_ics_span_transport_result_image_raw_pp_cell_dot_sum ff_v_dot_mcp_ics_span_transport_result_image_raw_pp_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_span_transport_result_image_raw_pp_cell_dot_sum_start. ff_h_dot_mcp_ics_span_transport_result_image_raw_pp_cell_dot_sum_start + S (0) = S ((S (0)) * ff_v_dot_mcp_ics_span_transport_result_image_raw_pp_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_span_transport_result_image_raw_pp_cell_dot_sum_start. ff_u_dot_mcp_ics_span_transport_result_image_raw_pp_cell_dot_sum = ff_q_dot_mcp_ics_span_transport_result_image_raw_pp_cell_dot_sum_start * S ((S (0)) * ff_v_dot_mcp_ics_span_transport_result_image_raw_pp_cell_dot_sum) + (0))) /\ ((((exists ff_h_dot_mcp_ics_span_transport_result_image_raw_pp_cell_dot_sum_terminal. ff_h_dot_mcp_ics_span_transport_result_image_raw_pp_cell_dot_sum_terminal + S (ff_value_mcp_prefix_ics_span_transport_result_image_raw_pp) = S ((S (w)) * ff_v_dot_mcp_ics_span_transport_result_image_raw_pp_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_span_transport_result_image_raw_pp_cell_dot_sum_terminal. ff_u_dot_mcp_ics_span_transport_result_image_raw_pp_cell_dot_sum = ff_q_dot_mcp_ics_span_transport_result_image_raw_pp_cell_dot_sum_terminal * S ((S (w)) * ff_v_dot_mcp_ics_span_transport_result_image_raw_pp_cell_dot_sum) + (ff_value_mcp_prefix_ics_span_transport_result_image_raw_pp))) /\ forall ff_i_dot_mcp_ics_span_transport_result_image_raw_pp_cell_dot_sum. (exists ff_lt_dot_mcp_ics_span_transport_result_image_raw_pp_cell_dot_sum_bound. ff_lt_dot_mcp_ics_span_transport_result_image_raw_pp_cell_dot_sum_bound + S ff_i_dot_mcp_ics_span_transport_result_image_raw_pp_cell_dot_sum = w) -> exists ff_a_dot_mcp_ics_span_transport_result_image_raw_pp_cell_dot_sum ff_r_dot_mcp_ics_span_transport_result_image_raw_pp_cell_dot_sum ff_s_dot_mcp_ics_span_transport_result_image_raw_pp_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_span_transport_result_image_raw_pp_cell_dot_sum_summand. ff_h_dot_mcp_ics_span_transport_result_image_raw_pp_cell_dot_sum_summand + S (ff_a_dot_mcp_ics_span_transport_result_image_raw_pp_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_span_transport_result_image_raw_pp_cell_dot_sum)) * ff_scale_dot_mcp_ics_span_transport_result_image_raw_pp_cell_dot)) /\ exists ff_q_dot_mcp_ics_span_transport_result_image_raw_pp_cell_dot_sum_summand. ff_code_dot_mcp_ics_span_transport_result_image_raw_pp_cell_dot = ff_q_dot_mcp_ics_span_transport_result_image_raw_pp_cell_dot_sum_summand * S ((S (ff_i_dot_mcp_ics_span_transport_result_image_raw_pp_cell_dot_sum)) * ff_scale_dot_mcp_ics_span_transport_result_image_raw_pp_cell_dot) + (ff_a_dot_mcp_ics_span_transport_result_image_raw_pp_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_span_transport_result_image_raw_pp_cell_dot_sum_partial. ff_h_dot_mcp_ics_span_transport_result_image_raw_pp_cell_dot_sum_partial + S (ff_r_dot_mcp_ics_span_transport_result_image_raw_pp_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_span_transport_result_image_raw_pp_cell_dot_sum)) * ff_v_dot_mcp_ics_span_transport_result_image_raw_pp_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_span_transport_result_image_raw_pp_cell_dot_sum_partial. ff_u_dot_mcp_ics_span_transport_result_image_raw_pp_cell_dot_sum = ff_q_dot_mcp_ics_span_transport_result_image_raw_pp_cell_dot_sum_partial * S ((S (ff_i_dot_mcp_ics_span_transport_result_image_raw_pp_cell_dot_sum)) * ff_v_dot_mcp_ics_span_transport_result_image_raw_pp_cell_dot_sum) + (ff_r_dot_mcp_ics_span_transport_result_image_raw_pp_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_span_transport_result_image_raw_pp_cell_dot_sum_successor. ff_h_dot_mcp_ics_span_transport_result_image_raw_pp_cell_dot_sum_successor + S (ff_s_dot_mcp_ics_span_transport_result_image_raw_pp_cell_dot_sum) = S ((S (S ff_i_dot_mcp_ics_span_transport_result_image_raw_pp_cell_dot_sum)) * ff_v_dot_mcp_ics_span_transport_result_image_raw_pp_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_span_transport_result_image_raw_pp_cell_dot_sum_successor. ff_u_dot_mcp_ics_span_transport_result_image_raw_pp_cell_dot_sum = ff_q_dot_mcp_ics_span_transport_result_image_raw_pp_cell_dot_sum_successor * S ((S (S ff_i_dot_mcp_ics_span_transport_result_image_raw_pp_cell_dot_sum)) * ff_v_dot_mcp_ics_span_transport_result_image_raw_pp_cell_dot_sum) + (ff_s_dot_mcp_ics_span_transport_result_image_raw_pp_cell_dot_sum))) /\ ff_s_dot_mcp_ics_span_transport_result_image_raw_pp_cell_dot_sum = ff_r_dot_mcp_ics_span_transport_result_image_raw_pp_cell_dot_sum + ff_a_dot_mcp_ics_span_transport_result_image_raw_pp_cell_dot_sum))))))))))) /\ (((exists fs_h_mcp_ics_span_transport_result_image_raw_pp_entry. fs_h_mcp_ics_span_transport_result_image_raw_pp_entry + S (ff_value_mcp_prefix_ics_span_transport_result_image_raw_pp) = S ((S (ff_index_mcp_prefix_ics_span_transport_result_image_raw_pp)) * ff_pps_mcp_smatrix_ics_span_transport_result_image_raw)) /\ exists fs_q_mcp_ics_span_transport_result_image_raw_pp_entry. ff_pp_mcp_smatrix_ics_span_transport_result_image_raw = fs_q_mcp_ics_span_transport_result_image_raw_pp_entry * S ((S (ff_index_mcp_prefix_ics_span_transport_result_image_raw_pp)) * ff_pps_mcp_smatrix_ics_span_transport_result_image_raw) + (ff_value_mcp_prefix_ics_span_transport_result_image_raw_pp))))))) /\ ((forall ff_index_mcp_prefix_ics_span_transport_result_image_raw_nn. (exists mcp_gap_ics_span_transport_result_image_raw_nn_index. mcp_gap_ics_span_transport_result_image_raw_nn_index + S (ff_index_mcp_prefix_ics_span_transport_result_image_raw_nn) = ((r) * (1))) -> exists ff_row_mcp_prefix_ics_span_transport_result_image_raw_nn ff_column_mcp_prefix_ics_span_transport_result_image_raw_nn ff_value_mcp_prefix_ics_span_transport_result_image_raw_nn. ((ff_index_mcp_prefix_ics_span_transport_result_image_raw_nn) = (1) * ff_row_mcp_prefix_ics_span_transport_result_image_raw_nn + ff_column_mcp_prefix_ics_span_transport_result_image_raw_nn /\ ((exists mcp_gap_ics_span_transport_result_image_raw_nn_column. mcp_gap_ics_span_transport_result_image_raw_nn_column + S (ff_column_mcp_prefix_ics_span_transport_result_image_raw_nn) = (1)) /\ ((exists ff_left_mcp_cell_ics_span_transport_result_image_raw_nn_cell ff_left_scale_mcp_cell_ics_span_transport_result_image_raw_nn_cell ff_right_mcp_cell_ics_span_transport_result_image_raw_nn_cell ff_right_scale_mcp_cell_ics_span_transport_result_image_raw_nn_cell. ((forall ff_index_mcp_ics_span_transport_result_image_raw_nn_cell_row ff_source_mcp_ics_span_transport_result_image_raw_nn_cell_row ff_target_mcp_ics_span_transport_result_image_raw_nn_cell_row. (exists mcp_gap_ics_span_transport_result_image_raw_nn_cell_row_bound. mcp_gap_ics_span_transport_result_image_raw_nn_cell_row_bound + S (ff_index_mcp_ics_span_transport_result_image_raw_nn_cell_row) = (w)) -> (((exists fs_h_mcp_ics_span_transport_result_image_raw_nn_cell_row_source. fs_h_mcp_ics_span_transport_result_image_raw_nn_cell_row_source + S (ff_source_mcp_ics_span_transport_result_image_raw_nn_cell_row) = S ((S (((ff_row_mcp_prefix_ics_span_transport_result_image_raw_nn) * (w)) + (1) * ff_index_mcp_ics_span_transport_result_image_raw_nn_cell_row)) * dc)) /\ exists fs_q_mcp_ics_span_transport_result_image_raw_nn_cell_row_source. db = fs_q_mcp_ics_span_transport_result_image_raw_nn_cell_row_source * S ((S (((ff_row_mcp_prefix_ics_span_transport_result_image_raw_nn) * (w)) + (1) * ff_index_mcp_ics_span_transport_result_image_raw_nn_cell_row)) * dc) + (ff_source_mcp_ics_span_transport_result_image_raw_nn_cell_row))) -> (((exists fs_h_mcp_ics_span_transport_result_image_raw_nn_cell_row_target. fs_h_mcp_ics_span_transport_result_image_raw_nn_cell_row_target + S (ff_target_mcp_ics_span_transport_result_image_raw_nn_cell_row) = S ((S (ff_index_mcp_ics_span_transport_result_image_raw_nn_cell_row)) * ff_left_scale_mcp_cell_ics_span_transport_result_image_raw_nn_cell)) /\ exists fs_q_mcp_ics_span_transport_result_image_raw_nn_cell_row_target. ff_left_mcp_cell_ics_span_transport_result_image_raw_nn_cell = fs_q_mcp_ics_span_transport_result_image_raw_nn_cell_row_target * S ((S (ff_index_mcp_ics_span_transport_result_image_raw_nn_cell_row)) * ff_left_scale_mcp_cell_ics_span_transport_result_image_raw_nn_cell) + (ff_target_mcp_ics_span_transport_result_image_raw_nn_cell_row))) -> ff_target_mcp_ics_span_transport_result_image_raw_nn_cell_row = ff_source_mcp_ics_span_transport_result_image_raw_nn_cell_row) /\ ((forall ff_index_mcp_ics_span_transport_result_image_raw_nn_cell_column ff_source_mcp_ics_span_transport_result_image_raw_nn_cell_column ff_target_mcp_ics_span_transport_result_image_raw_nn_cell_column. (exists mcp_gap_ics_span_transport_result_image_raw_nn_cell_column_bound. mcp_gap_ics_span_transport_result_image_raw_nn_cell_column_bound + S (ff_index_mcp_ics_span_transport_result_image_raw_nn_cell_column) = (w)) -> (((exists fs_h_mcp_ics_span_transport_result_image_raw_nn_cell_column_source. fs_h_mcp_ics_span_transport_result_image_raw_nn_cell_column_source + S (ff_source_mcp_ics_span_transport_result_image_raw_nn_cell_column) = S ((S ((ff_column_mcp_prefix_ics_span_transport_result_image_raw_nn) + (1) * ff_index_mcp_ics_span_transport_result_image_raw_nn_cell_column)) * ics_coefficient_negative_scale_span_transport_result)) /\ exists fs_q_mcp_ics_span_transport_result_image_raw_nn_cell_column_source. ics_coefficient_negative_span_transport_result = fs_q_mcp_ics_span_transport_result_image_raw_nn_cell_column_source * S ((S ((ff_column_mcp_prefix_ics_span_transport_result_image_raw_nn) + (1) * ff_index_mcp_ics_span_transport_result_image_raw_nn_cell_column)) * ics_coefficient_negative_scale_span_transport_result) + (ff_source_mcp_ics_span_transport_result_image_raw_nn_cell_column))) -> (((exists fs_h_mcp_ics_span_transport_result_image_raw_nn_cell_column_target. fs_h_mcp_ics_span_transport_result_image_raw_nn_cell_column_target + S (ff_target_mcp_ics_span_transport_result_image_raw_nn_cell_column) = S ((S (ff_index_mcp_ics_span_transport_result_image_raw_nn_cell_column)) * ff_right_scale_mcp_cell_ics_span_transport_result_image_raw_nn_cell)) /\ exists fs_q_mcp_ics_span_transport_result_image_raw_nn_cell_column_target. ff_right_mcp_cell_ics_span_transport_result_image_raw_nn_cell = fs_q_mcp_ics_span_transport_result_image_raw_nn_cell_column_target * S ((S (ff_index_mcp_ics_span_transport_result_image_raw_nn_cell_column)) * ff_right_scale_mcp_cell_ics_span_transport_result_image_raw_nn_cell) + (ff_target_mcp_ics_span_transport_result_image_raw_nn_cell_column))) -> ff_target_mcp_ics_span_transport_result_image_raw_nn_cell_column = ff_source_mcp_ics_span_transport_result_image_raw_nn_cell_column) /\ (exists ff_code_dot_mcp_ics_span_transport_result_image_raw_nn_cell_dot ff_scale_dot_mcp_ics_span_transport_result_image_raw_nn_cell_dot. ((forall fpmp_index_dot_mcp_ics_span_transport_result_image_raw_nn_cell_dot_pointwise fpmp_left_dot_mcp_ics_span_transport_result_image_raw_nn_cell_dot_pointwise fpmp_right_dot_mcp_ics_span_transport_result_image_raw_nn_cell_dot_pointwise fpmp_target_dot_mcp_ics_span_transport_result_image_raw_nn_cell_dot_pointwise. (exists fpmp_gap_dot_mcp_ics_span_transport_result_image_raw_nn_cell_dot_pointwise. fpmp_gap_dot_mcp_ics_span_transport_result_image_raw_nn_cell_dot_pointwise + S fpmp_index_dot_mcp_ics_span_transport_result_image_raw_nn_cell_dot_pointwise = w) -> (((exists ff_h_fpmp_dot_mcp_ics_span_transport_result_image_raw_nn_cell_dot_pointwise_left. ff_h_fpmp_dot_mcp_ics_span_transport_result_image_raw_nn_cell_dot_pointwise_left + S (fpmp_left_dot_mcp_ics_span_transport_result_image_raw_nn_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_span_transport_result_image_raw_nn_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_span_transport_result_image_raw_nn_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_span_transport_result_image_raw_nn_cell_dot_pointwise_left. ff_left_mcp_cell_ics_span_transport_result_image_raw_nn_cell = ff_q_fpmp_dot_mcp_ics_span_transport_result_image_raw_nn_cell_dot_pointwise_left * S ((S (fpmp_index_dot_mcp_ics_span_transport_result_image_raw_nn_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_span_transport_result_image_raw_nn_cell) + (fpmp_left_dot_mcp_ics_span_transport_result_image_raw_nn_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_span_transport_result_image_raw_nn_cell_dot_pointwise_right. ff_h_fpmp_dot_mcp_ics_span_transport_result_image_raw_nn_cell_dot_pointwise_right + S (fpmp_right_dot_mcp_ics_span_transport_result_image_raw_nn_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_span_transport_result_image_raw_nn_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_span_transport_result_image_raw_nn_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_span_transport_result_image_raw_nn_cell_dot_pointwise_right. ff_right_mcp_cell_ics_span_transport_result_image_raw_nn_cell = ff_q_fpmp_dot_mcp_ics_span_transport_result_image_raw_nn_cell_dot_pointwise_right * S ((S (fpmp_index_dot_mcp_ics_span_transport_result_image_raw_nn_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_span_transport_result_image_raw_nn_cell) + (fpmp_right_dot_mcp_ics_span_transport_result_image_raw_nn_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_span_transport_result_image_raw_nn_cell_dot_pointwise_target. ff_h_fpmp_dot_mcp_ics_span_transport_result_image_raw_nn_cell_dot_pointwise_target + S (fpmp_target_dot_mcp_ics_span_transport_result_image_raw_nn_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_span_transport_result_image_raw_nn_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_span_transport_result_image_raw_nn_cell_dot)) /\ exists ff_q_fpmp_dot_mcp_ics_span_transport_result_image_raw_nn_cell_dot_pointwise_target. ff_code_dot_mcp_ics_span_transport_result_image_raw_nn_cell_dot = ff_q_fpmp_dot_mcp_ics_span_transport_result_image_raw_nn_cell_dot_pointwise_target * S ((S (fpmp_index_dot_mcp_ics_span_transport_result_image_raw_nn_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_span_transport_result_image_raw_nn_cell_dot) + (fpmp_target_dot_mcp_ics_span_transport_result_image_raw_nn_cell_dot_pointwise))) -> fpmp_target_dot_mcp_ics_span_transport_result_image_raw_nn_cell_dot_pointwise = fpmp_left_dot_mcp_ics_span_transport_result_image_raw_nn_cell_dot_pointwise * fpmp_right_dot_mcp_ics_span_transport_result_image_raw_nn_cell_dot_pointwise) /\ (exists ff_u_dot_mcp_ics_span_transport_result_image_raw_nn_cell_dot_sum ff_v_dot_mcp_ics_span_transport_result_image_raw_nn_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_span_transport_result_image_raw_nn_cell_dot_sum_start. ff_h_dot_mcp_ics_span_transport_result_image_raw_nn_cell_dot_sum_start + S (0) = S ((S (0)) * ff_v_dot_mcp_ics_span_transport_result_image_raw_nn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_span_transport_result_image_raw_nn_cell_dot_sum_start. ff_u_dot_mcp_ics_span_transport_result_image_raw_nn_cell_dot_sum = ff_q_dot_mcp_ics_span_transport_result_image_raw_nn_cell_dot_sum_start * S ((S (0)) * ff_v_dot_mcp_ics_span_transport_result_image_raw_nn_cell_dot_sum) + (0))) /\ ((((exists ff_h_dot_mcp_ics_span_transport_result_image_raw_nn_cell_dot_sum_terminal. ff_h_dot_mcp_ics_span_transport_result_image_raw_nn_cell_dot_sum_terminal + S (ff_value_mcp_prefix_ics_span_transport_result_image_raw_nn) = S ((S (w)) * ff_v_dot_mcp_ics_span_transport_result_image_raw_nn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_span_transport_result_image_raw_nn_cell_dot_sum_terminal. ff_u_dot_mcp_ics_span_transport_result_image_raw_nn_cell_dot_sum = ff_q_dot_mcp_ics_span_transport_result_image_raw_nn_cell_dot_sum_terminal * S ((S (w)) * ff_v_dot_mcp_ics_span_transport_result_image_raw_nn_cell_dot_sum) + (ff_value_mcp_prefix_ics_span_transport_result_image_raw_nn))) /\ forall ff_i_dot_mcp_ics_span_transport_result_image_raw_nn_cell_dot_sum. (exists ff_lt_dot_mcp_ics_span_transport_result_image_raw_nn_cell_dot_sum_bound. ff_lt_dot_mcp_ics_span_transport_result_image_raw_nn_cell_dot_sum_bound + S ff_i_dot_mcp_ics_span_transport_result_image_raw_nn_cell_dot_sum = w) -> exists ff_a_dot_mcp_ics_span_transport_result_image_raw_nn_cell_dot_sum ff_r_dot_mcp_ics_span_transport_result_image_raw_nn_cell_dot_sum ff_s_dot_mcp_ics_span_transport_result_image_raw_nn_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_span_transport_result_image_raw_nn_cell_dot_sum_summand. ff_h_dot_mcp_ics_span_transport_result_image_raw_nn_cell_dot_sum_summand + S (ff_a_dot_mcp_ics_span_transport_result_image_raw_nn_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_span_transport_result_image_raw_nn_cell_dot_sum)) * ff_scale_dot_mcp_ics_span_transport_result_image_raw_nn_cell_dot)) /\ exists ff_q_dot_mcp_ics_span_transport_result_image_raw_nn_cell_dot_sum_summand. ff_code_dot_mcp_ics_span_transport_result_image_raw_nn_cell_dot = ff_q_dot_mcp_ics_span_transport_result_image_raw_nn_cell_dot_sum_summand * S ((S (ff_i_dot_mcp_ics_span_transport_result_image_raw_nn_cell_dot_sum)) * ff_scale_dot_mcp_ics_span_transport_result_image_raw_nn_cell_dot) + (ff_a_dot_mcp_ics_span_transport_result_image_raw_nn_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_span_transport_result_image_raw_nn_cell_dot_sum_partial. ff_h_dot_mcp_ics_span_transport_result_image_raw_nn_cell_dot_sum_partial + S (ff_r_dot_mcp_ics_span_transport_result_image_raw_nn_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_span_transport_result_image_raw_nn_cell_dot_sum)) * ff_v_dot_mcp_ics_span_transport_result_image_raw_nn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_span_transport_result_image_raw_nn_cell_dot_sum_partial. ff_u_dot_mcp_ics_span_transport_result_image_raw_nn_cell_dot_sum = ff_q_dot_mcp_ics_span_transport_result_image_raw_nn_cell_dot_sum_partial * S ((S (ff_i_dot_mcp_ics_span_transport_result_image_raw_nn_cell_dot_sum)) * ff_v_dot_mcp_ics_span_transport_result_image_raw_nn_cell_dot_sum) + (ff_r_dot_mcp_ics_span_transport_result_image_raw_nn_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_span_transport_result_image_raw_nn_cell_dot_sum_successor. ff_h_dot_mcp_ics_span_transport_result_image_raw_nn_cell_dot_sum_successor + S (ff_s_dot_mcp_ics_span_transport_result_image_raw_nn_cell_dot_sum) = S ((S (S ff_i_dot_mcp_ics_span_transport_result_image_raw_nn_cell_dot_sum)) * ff_v_dot_mcp_ics_span_transport_result_image_raw_nn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_span_transport_result_image_raw_nn_cell_dot_sum_successor. ff_u_dot_mcp_ics_span_transport_result_image_raw_nn_cell_dot_sum = ff_q_dot_mcp_ics_span_transport_result_image_raw_nn_cell_dot_sum_successor * S ((S (S ff_i_dot_mcp_ics_span_transport_result_image_raw_nn_cell_dot_sum)) * ff_v_dot_mcp_ics_span_transport_result_image_raw_nn_cell_dot_sum) + (ff_s_dot_mcp_ics_span_transport_result_image_raw_nn_cell_dot_sum))) /\ ff_s_dot_mcp_ics_span_transport_result_image_raw_nn_cell_dot_sum = ff_r_dot_mcp_ics_span_transport_result_image_raw_nn_cell_dot_sum + ff_a_dot_mcp_ics_span_transport_result_image_raw_nn_cell_dot_sum))))))))))) /\ (((exists fs_h_mcp_ics_span_transport_result_image_raw_nn_entry. fs_h_mcp_ics_span_transport_result_image_raw_nn_entry + S (ff_value_mcp_prefix_ics_span_transport_result_image_raw_nn) = S ((S (ff_index_mcp_prefix_ics_span_transport_result_image_raw_nn)) * ff_nns_mcp_smatrix_ics_span_transport_result_image_raw)) /\ exists fs_q_mcp_ics_span_transport_result_image_raw_nn_entry. ff_nn_mcp_smatrix_ics_span_transport_result_image_raw = fs_q_mcp_ics_span_transport_result_image_raw_nn_entry * S ((S (ff_index_mcp_prefix_ics_span_transport_result_image_raw_nn)) * ff_nns_mcp_smatrix_ics_span_transport_result_image_raw) + (ff_value_mcp_prefix_ics_span_transport_result_image_raw_nn))))))) /\ ((forall ff_index_mcp_prefix_ics_span_transport_result_image_raw_pn. (exists mcp_gap_ics_span_transport_result_image_raw_pn_index. mcp_gap_ics_span_transport_result_image_raw_pn_index + S (ff_index_mcp_prefix_ics_span_transport_result_image_raw_pn) = ((r) * (1))) -> exists ff_row_mcp_prefix_ics_span_transport_result_image_raw_pn ff_column_mcp_prefix_ics_span_transport_result_image_raw_pn ff_value_mcp_prefix_ics_span_transport_result_image_raw_pn. ((ff_index_mcp_prefix_ics_span_transport_result_image_raw_pn) = (1) * ff_row_mcp_prefix_ics_span_transport_result_image_raw_pn + ff_column_mcp_prefix_ics_span_transport_result_image_raw_pn /\ ((exists mcp_gap_ics_span_transport_result_image_raw_pn_column. mcp_gap_ics_span_transport_result_image_raw_pn_column + S (ff_column_mcp_prefix_ics_span_transport_result_image_raw_pn) = (1)) /\ ((exists ff_left_mcp_cell_ics_span_transport_result_image_raw_pn_cell ff_left_scale_mcp_cell_ics_span_transport_result_image_raw_pn_cell ff_right_mcp_cell_ics_span_transport_result_image_raw_pn_cell ff_right_scale_mcp_cell_ics_span_transport_result_image_raw_pn_cell. ((forall ff_index_mcp_ics_span_transport_result_image_raw_pn_cell_row ff_source_mcp_ics_span_transport_result_image_raw_pn_cell_row ff_target_mcp_ics_span_transport_result_image_raw_pn_cell_row. (exists mcp_gap_ics_span_transport_result_image_raw_pn_cell_row_bound. mcp_gap_ics_span_transport_result_image_raw_pn_cell_row_bound + S (ff_index_mcp_ics_span_transport_result_image_raw_pn_cell_row) = (w)) -> (((exists fs_h_mcp_ics_span_transport_result_image_raw_pn_cell_row_source. fs_h_mcp_ics_span_transport_result_image_raw_pn_cell_row_source + S (ff_source_mcp_ics_span_transport_result_image_raw_pn_cell_row) = S ((S (((ff_row_mcp_prefix_ics_span_transport_result_image_raw_pn) * (w)) + (1) * ff_index_mcp_ics_span_transport_result_image_raw_pn_cell_row)) * ac)) /\ exists fs_q_mcp_ics_span_transport_result_image_raw_pn_cell_row_source. ab = fs_q_mcp_ics_span_transport_result_image_raw_pn_cell_row_source * S ((S (((ff_row_mcp_prefix_ics_span_transport_result_image_raw_pn) * (w)) + (1) * ff_index_mcp_ics_span_transport_result_image_raw_pn_cell_row)) * ac) + (ff_source_mcp_ics_span_transport_result_image_raw_pn_cell_row))) -> (((exists fs_h_mcp_ics_span_transport_result_image_raw_pn_cell_row_target. fs_h_mcp_ics_span_transport_result_image_raw_pn_cell_row_target + S (ff_target_mcp_ics_span_transport_result_image_raw_pn_cell_row) = S ((S (ff_index_mcp_ics_span_transport_result_image_raw_pn_cell_row)) * ff_left_scale_mcp_cell_ics_span_transport_result_image_raw_pn_cell)) /\ exists fs_q_mcp_ics_span_transport_result_image_raw_pn_cell_row_target. ff_left_mcp_cell_ics_span_transport_result_image_raw_pn_cell = fs_q_mcp_ics_span_transport_result_image_raw_pn_cell_row_target * S ((S (ff_index_mcp_ics_span_transport_result_image_raw_pn_cell_row)) * ff_left_scale_mcp_cell_ics_span_transport_result_image_raw_pn_cell) + (ff_target_mcp_ics_span_transport_result_image_raw_pn_cell_row))) -> ff_target_mcp_ics_span_transport_result_image_raw_pn_cell_row = ff_source_mcp_ics_span_transport_result_image_raw_pn_cell_row) /\ ((forall ff_index_mcp_ics_span_transport_result_image_raw_pn_cell_column ff_source_mcp_ics_span_transport_result_image_raw_pn_cell_column ff_target_mcp_ics_span_transport_result_image_raw_pn_cell_column. (exists mcp_gap_ics_span_transport_result_image_raw_pn_cell_column_bound. mcp_gap_ics_span_transport_result_image_raw_pn_cell_column_bound + S (ff_index_mcp_ics_span_transport_result_image_raw_pn_cell_column) = (w)) -> (((exists fs_h_mcp_ics_span_transport_result_image_raw_pn_cell_column_source. fs_h_mcp_ics_span_transport_result_image_raw_pn_cell_column_source + S (ff_source_mcp_ics_span_transport_result_image_raw_pn_cell_column) = S ((S ((ff_column_mcp_prefix_ics_span_transport_result_image_raw_pn) + (1) * ff_index_mcp_ics_span_transport_result_image_raw_pn_cell_column)) * ics_coefficient_negative_scale_span_transport_result)) /\ exists fs_q_mcp_ics_span_transport_result_image_raw_pn_cell_column_source. ics_coefficient_negative_span_transport_result = fs_q_mcp_ics_span_transport_result_image_raw_pn_cell_column_source * S ((S ((ff_column_mcp_prefix_ics_span_transport_result_image_raw_pn) + (1) * ff_index_mcp_ics_span_transport_result_image_raw_pn_cell_column)) * ics_coefficient_negative_scale_span_transport_result) + (ff_source_mcp_ics_span_transport_result_image_raw_pn_cell_column))) -> (((exists fs_h_mcp_ics_span_transport_result_image_raw_pn_cell_column_target. fs_h_mcp_ics_span_transport_result_image_raw_pn_cell_column_target + S (ff_target_mcp_ics_span_transport_result_image_raw_pn_cell_column) = S ((S (ff_index_mcp_ics_span_transport_result_image_raw_pn_cell_column)) * ff_right_scale_mcp_cell_ics_span_transport_result_image_raw_pn_cell)) /\ exists fs_q_mcp_ics_span_transport_result_image_raw_pn_cell_column_target. ff_right_mcp_cell_ics_span_transport_result_image_raw_pn_cell = fs_q_mcp_ics_span_transport_result_image_raw_pn_cell_column_target * S ((S (ff_index_mcp_ics_span_transport_result_image_raw_pn_cell_column)) * ff_right_scale_mcp_cell_ics_span_transport_result_image_raw_pn_cell) + (ff_target_mcp_ics_span_transport_result_image_raw_pn_cell_column))) -> ff_target_mcp_ics_span_transport_result_image_raw_pn_cell_column = ff_source_mcp_ics_span_transport_result_image_raw_pn_cell_column) /\ (exists ff_code_dot_mcp_ics_span_transport_result_image_raw_pn_cell_dot ff_scale_dot_mcp_ics_span_transport_result_image_raw_pn_cell_dot. ((forall fpmp_index_dot_mcp_ics_span_transport_result_image_raw_pn_cell_dot_pointwise fpmp_left_dot_mcp_ics_span_transport_result_image_raw_pn_cell_dot_pointwise fpmp_right_dot_mcp_ics_span_transport_result_image_raw_pn_cell_dot_pointwise fpmp_target_dot_mcp_ics_span_transport_result_image_raw_pn_cell_dot_pointwise. (exists fpmp_gap_dot_mcp_ics_span_transport_result_image_raw_pn_cell_dot_pointwise. fpmp_gap_dot_mcp_ics_span_transport_result_image_raw_pn_cell_dot_pointwise + S fpmp_index_dot_mcp_ics_span_transport_result_image_raw_pn_cell_dot_pointwise = w) -> (((exists ff_h_fpmp_dot_mcp_ics_span_transport_result_image_raw_pn_cell_dot_pointwise_left. ff_h_fpmp_dot_mcp_ics_span_transport_result_image_raw_pn_cell_dot_pointwise_left + S (fpmp_left_dot_mcp_ics_span_transport_result_image_raw_pn_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_span_transport_result_image_raw_pn_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_span_transport_result_image_raw_pn_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_span_transport_result_image_raw_pn_cell_dot_pointwise_left. ff_left_mcp_cell_ics_span_transport_result_image_raw_pn_cell = ff_q_fpmp_dot_mcp_ics_span_transport_result_image_raw_pn_cell_dot_pointwise_left * S ((S (fpmp_index_dot_mcp_ics_span_transport_result_image_raw_pn_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_span_transport_result_image_raw_pn_cell) + (fpmp_left_dot_mcp_ics_span_transport_result_image_raw_pn_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_span_transport_result_image_raw_pn_cell_dot_pointwise_right. ff_h_fpmp_dot_mcp_ics_span_transport_result_image_raw_pn_cell_dot_pointwise_right + S (fpmp_right_dot_mcp_ics_span_transport_result_image_raw_pn_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_span_transport_result_image_raw_pn_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_span_transport_result_image_raw_pn_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_span_transport_result_image_raw_pn_cell_dot_pointwise_right. ff_right_mcp_cell_ics_span_transport_result_image_raw_pn_cell = ff_q_fpmp_dot_mcp_ics_span_transport_result_image_raw_pn_cell_dot_pointwise_right * S ((S (fpmp_index_dot_mcp_ics_span_transport_result_image_raw_pn_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_span_transport_result_image_raw_pn_cell) + (fpmp_right_dot_mcp_ics_span_transport_result_image_raw_pn_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_span_transport_result_image_raw_pn_cell_dot_pointwise_target. ff_h_fpmp_dot_mcp_ics_span_transport_result_image_raw_pn_cell_dot_pointwise_target + S (fpmp_target_dot_mcp_ics_span_transport_result_image_raw_pn_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_span_transport_result_image_raw_pn_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_span_transport_result_image_raw_pn_cell_dot)) /\ exists ff_q_fpmp_dot_mcp_ics_span_transport_result_image_raw_pn_cell_dot_pointwise_target. ff_code_dot_mcp_ics_span_transport_result_image_raw_pn_cell_dot = ff_q_fpmp_dot_mcp_ics_span_transport_result_image_raw_pn_cell_dot_pointwise_target * S ((S (fpmp_index_dot_mcp_ics_span_transport_result_image_raw_pn_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_span_transport_result_image_raw_pn_cell_dot) + (fpmp_target_dot_mcp_ics_span_transport_result_image_raw_pn_cell_dot_pointwise))) -> fpmp_target_dot_mcp_ics_span_transport_result_image_raw_pn_cell_dot_pointwise = fpmp_left_dot_mcp_ics_span_transport_result_image_raw_pn_cell_dot_pointwise * fpmp_right_dot_mcp_ics_span_transport_result_image_raw_pn_cell_dot_pointwise) /\ (exists ff_u_dot_mcp_ics_span_transport_result_image_raw_pn_cell_dot_sum ff_v_dot_mcp_ics_span_transport_result_image_raw_pn_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_span_transport_result_image_raw_pn_cell_dot_sum_start. ff_h_dot_mcp_ics_span_transport_result_image_raw_pn_cell_dot_sum_start + S (0) = S ((S (0)) * ff_v_dot_mcp_ics_span_transport_result_image_raw_pn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_span_transport_result_image_raw_pn_cell_dot_sum_start. ff_u_dot_mcp_ics_span_transport_result_image_raw_pn_cell_dot_sum = ff_q_dot_mcp_ics_span_transport_result_image_raw_pn_cell_dot_sum_start * S ((S (0)) * ff_v_dot_mcp_ics_span_transport_result_image_raw_pn_cell_dot_sum) + (0))) /\ ((((exists ff_h_dot_mcp_ics_span_transport_result_image_raw_pn_cell_dot_sum_terminal. ff_h_dot_mcp_ics_span_transport_result_image_raw_pn_cell_dot_sum_terminal + S (ff_value_mcp_prefix_ics_span_transport_result_image_raw_pn) = S ((S (w)) * ff_v_dot_mcp_ics_span_transport_result_image_raw_pn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_span_transport_result_image_raw_pn_cell_dot_sum_terminal. ff_u_dot_mcp_ics_span_transport_result_image_raw_pn_cell_dot_sum = ff_q_dot_mcp_ics_span_transport_result_image_raw_pn_cell_dot_sum_terminal * S ((S (w)) * ff_v_dot_mcp_ics_span_transport_result_image_raw_pn_cell_dot_sum) + (ff_value_mcp_prefix_ics_span_transport_result_image_raw_pn))) /\ forall ff_i_dot_mcp_ics_span_transport_result_image_raw_pn_cell_dot_sum. (exists ff_lt_dot_mcp_ics_span_transport_result_image_raw_pn_cell_dot_sum_bound. ff_lt_dot_mcp_ics_span_transport_result_image_raw_pn_cell_dot_sum_bound + S ff_i_dot_mcp_ics_span_transport_result_image_raw_pn_cell_dot_sum = w) -> exists ff_a_dot_mcp_ics_span_transport_result_image_raw_pn_cell_dot_sum ff_r_dot_mcp_ics_span_transport_result_image_raw_pn_cell_dot_sum ff_s_dot_mcp_ics_span_transport_result_image_raw_pn_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_span_transport_result_image_raw_pn_cell_dot_sum_summand. ff_h_dot_mcp_ics_span_transport_result_image_raw_pn_cell_dot_sum_summand + S (ff_a_dot_mcp_ics_span_transport_result_image_raw_pn_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_span_transport_result_image_raw_pn_cell_dot_sum)) * ff_scale_dot_mcp_ics_span_transport_result_image_raw_pn_cell_dot)) /\ exists ff_q_dot_mcp_ics_span_transport_result_image_raw_pn_cell_dot_sum_summand. ff_code_dot_mcp_ics_span_transport_result_image_raw_pn_cell_dot = ff_q_dot_mcp_ics_span_transport_result_image_raw_pn_cell_dot_sum_summand * S ((S (ff_i_dot_mcp_ics_span_transport_result_image_raw_pn_cell_dot_sum)) * ff_scale_dot_mcp_ics_span_transport_result_image_raw_pn_cell_dot) + (ff_a_dot_mcp_ics_span_transport_result_image_raw_pn_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_span_transport_result_image_raw_pn_cell_dot_sum_partial. ff_h_dot_mcp_ics_span_transport_result_image_raw_pn_cell_dot_sum_partial + S (ff_r_dot_mcp_ics_span_transport_result_image_raw_pn_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_span_transport_result_image_raw_pn_cell_dot_sum)) * ff_v_dot_mcp_ics_span_transport_result_image_raw_pn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_span_transport_result_image_raw_pn_cell_dot_sum_partial. ff_u_dot_mcp_ics_span_transport_result_image_raw_pn_cell_dot_sum = ff_q_dot_mcp_ics_span_transport_result_image_raw_pn_cell_dot_sum_partial * S ((S (ff_i_dot_mcp_ics_span_transport_result_image_raw_pn_cell_dot_sum)) * ff_v_dot_mcp_ics_span_transport_result_image_raw_pn_cell_dot_sum) + (ff_r_dot_mcp_ics_span_transport_result_image_raw_pn_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_span_transport_result_image_raw_pn_cell_dot_sum_successor. ff_h_dot_mcp_ics_span_transport_result_image_raw_pn_cell_dot_sum_successor + S (ff_s_dot_mcp_ics_span_transport_result_image_raw_pn_cell_dot_sum) = S ((S (S ff_i_dot_mcp_ics_span_transport_result_image_raw_pn_cell_dot_sum)) * ff_v_dot_mcp_ics_span_transport_result_image_raw_pn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_span_transport_result_image_raw_pn_cell_dot_sum_successor. ff_u_dot_mcp_ics_span_transport_result_image_raw_pn_cell_dot_sum = ff_q_dot_mcp_ics_span_transport_result_image_raw_pn_cell_dot_sum_successor * S ((S (S ff_i_dot_mcp_ics_span_transport_result_image_raw_pn_cell_dot_sum)) * ff_v_dot_mcp_ics_span_transport_result_image_raw_pn_cell_dot_sum) + (ff_s_dot_mcp_ics_span_transport_result_image_raw_pn_cell_dot_sum))) /\ ff_s_dot_mcp_ics_span_transport_result_image_raw_pn_cell_dot_sum = ff_r_dot_mcp_ics_span_transport_result_image_raw_pn_cell_dot_sum + ff_a_dot_mcp_ics_span_transport_result_image_raw_pn_cell_dot_sum))))))))))) /\ (((exists fs_h_mcp_ics_span_transport_result_image_raw_pn_entry. fs_h_mcp_ics_span_transport_result_image_raw_pn_entry + S (ff_value_mcp_prefix_ics_span_transport_result_image_raw_pn) = S ((S (ff_index_mcp_prefix_ics_span_transport_result_image_raw_pn)) * ff_pns_mcp_smatrix_ics_span_transport_result_image_raw)) /\ exists fs_q_mcp_ics_span_transport_result_image_raw_pn_entry. ff_pn_mcp_smatrix_ics_span_transport_result_image_raw = fs_q_mcp_ics_span_transport_result_image_raw_pn_entry * S ((S (ff_index_mcp_prefix_ics_span_transport_result_image_raw_pn)) * ff_pns_mcp_smatrix_ics_span_transport_result_image_raw) + (ff_value_mcp_prefix_ics_span_transport_result_image_raw_pn))))))) /\ ((forall ff_index_mcp_prefix_ics_span_transport_result_image_raw_np. (exists mcp_gap_ics_span_transport_result_image_raw_np_index. mcp_gap_ics_span_transport_result_image_raw_np_index + S (ff_index_mcp_prefix_ics_span_transport_result_image_raw_np) = ((r) * (1))) -> exists ff_row_mcp_prefix_ics_span_transport_result_image_raw_np ff_column_mcp_prefix_ics_span_transport_result_image_raw_np ff_value_mcp_prefix_ics_span_transport_result_image_raw_np. ((ff_index_mcp_prefix_ics_span_transport_result_image_raw_np) = (1) * ff_row_mcp_prefix_ics_span_transport_result_image_raw_np + ff_column_mcp_prefix_ics_span_transport_result_image_raw_np /\ ((exists mcp_gap_ics_span_transport_result_image_raw_np_column. mcp_gap_ics_span_transport_result_image_raw_np_column + S (ff_column_mcp_prefix_ics_span_transport_result_image_raw_np) = (1)) /\ ((exists ff_left_mcp_cell_ics_span_transport_result_image_raw_np_cell ff_left_scale_mcp_cell_ics_span_transport_result_image_raw_np_cell ff_right_mcp_cell_ics_span_transport_result_image_raw_np_cell ff_right_scale_mcp_cell_ics_span_transport_result_image_raw_np_cell. ((forall ff_index_mcp_ics_span_transport_result_image_raw_np_cell_row ff_source_mcp_ics_span_transport_result_image_raw_np_cell_row ff_target_mcp_ics_span_transport_result_image_raw_np_cell_row. (exists mcp_gap_ics_span_transport_result_image_raw_np_cell_row_bound. mcp_gap_ics_span_transport_result_image_raw_np_cell_row_bound + S (ff_index_mcp_ics_span_transport_result_image_raw_np_cell_row) = (w)) -> (((exists fs_h_mcp_ics_span_transport_result_image_raw_np_cell_row_source. fs_h_mcp_ics_span_transport_result_image_raw_np_cell_row_source + S (ff_source_mcp_ics_span_transport_result_image_raw_np_cell_row) = S ((S (((ff_row_mcp_prefix_ics_span_transport_result_image_raw_np) * (w)) + (1) * ff_index_mcp_ics_span_transport_result_image_raw_np_cell_row)) * dc)) /\ exists fs_q_mcp_ics_span_transport_result_image_raw_np_cell_row_source. db = fs_q_mcp_ics_span_transport_result_image_raw_np_cell_row_source * S ((S (((ff_row_mcp_prefix_ics_span_transport_result_image_raw_np) * (w)) + (1) * ff_index_mcp_ics_span_transport_result_image_raw_np_cell_row)) * dc) + (ff_source_mcp_ics_span_transport_result_image_raw_np_cell_row))) -> (((exists fs_h_mcp_ics_span_transport_result_image_raw_np_cell_row_target. fs_h_mcp_ics_span_transport_result_image_raw_np_cell_row_target + S (ff_target_mcp_ics_span_transport_result_image_raw_np_cell_row) = S ((S (ff_index_mcp_ics_span_transport_result_image_raw_np_cell_row)) * ff_left_scale_mcp_cell_ics_span_transport_result_image_raw_np_cell)) /\ exists fs_q_mcp_ics_span_transport_result_image_raw_np_cell_row_target. ff_left_mcp_cell_ics_span_transport_result_image_raw_np_cell = fs_q_mcp_ics_span_transport_result_image_raw_np_cell_row_target * S ((S (ff_index_mcp_ics_span_transport_result_image_raw_np_cell_row)) * ff_left_scale_mcp_cell_ics_span_transport_result_image_raw_np_cell) + (ff_target_mcp_ics_span_transport_result_image_raw_np_cell_row))) -> ff_target_mcp_ics_span_transport_result_image_raw_np_cell_row = ff_source_mcp_ics_span_transport_result_image_raw_np_cell_row) /\ ((forall ff_index_mcp_ics_span_transport_result_image_raw_np_cell_column ff_source_mcp_ics_span_transport_result_image_raw_np_cell_column ff_target_mcp_ics_span_transport_result_image_raw_np_cell_column. (exists mcp_gap_ics_span_transport_result_image_raw_np_cell_column_bound. mcp_gap_ics_span_transport_result_image_raw_np_cell_column_bound + S (ff_index_mcp_ics_span_transport_result_image_raw_np_cell_column) = (w)) -> (((exists fs_h_mcp_ics_span_transport_result_image_raw_np_cell_column_source. fs_h_mcp_ics_span_transport_result_image_raw_np_cell_column_source + S (ff_source_mcp_ics_span_transport_result_image_raw_np_cell_column) = S ((S ((ff_column_mcp_prefix_ics_span_transport_result_image_raw_np) + (1) * ff_index_mcp_ics_span_transport_result_image_raw_np_cell_column)) * ics_coefficient_positive_scale_span_transport_result)) /\ exists fs_q_mcp_ics_span_transport_result_image_raw_np_cell_column_source. ics_coefficient_positive_span_transport_result = fs_q_mcp_ics_span_transport_result_image_raw_np_cell_column_source * S ((S ((ff_column_mcp_prefix_ics_span_transport_result_image_raw_np) + (1) * ff_index_mcp_ics_span_transport_result_image_raw_np_cell_column)) * ics_coefficient_positive_scale_span_transport_result) + (ff_source_mcp_ics_span_transport_result_image_raw_np_cell_column))) -> (((exists fs_h_mcp_ics_span_transport_result_image_raw_np_cell_column_target. fs_h_mcp_ics_span_transport_result_image_raw_np_cell_column_target + S (ff_target_mcp_ics_span_transport_result_image_raw_np_cell_column) = S ((S (ff_index_mcp_ics_span_transport_result_image_raw_np_cell_column)) * ff_right_scale_mcp_cell_ics_span_transport_result_image_raw_np_cell)) /\ exists fs_q_mcp_ics_span_transport_result_image_raw_np_cell_column_target. ff_right_mcp_cell_ics_span_transport_result_image_raw_np_cell = fs_q_mcp_ics_span_transport_result_image_raw_np_cell_column_target * S ((S (ff_index_mcp_ics_span_transport_result_image_raw_np_cell_column)) * ff_right_scale_mcp_cell_ics_span_transport_result_image_raw_np_cell) + (ff_target_mcp_ics_span_transport_result_image_raw_np_cell_column))) -> ff_target_mcp_ics_span_transport_result_image_raw_np_cell_column = ff_source_mcp_ics_span_transport_result_image_raw_np_cell_column) /\ (exists ff_code_dot_mcp_ics_span_transport_result_image_raw_np_cell_dot ff_scale_dot_mcp_ics_span_transport_result_image_raw_np_cell_dot. ((forall fpmp_index_dot_mcp_ics_span_transport_result_image_raw_np_cell_dot_pointwise fpmp_left_dot_mcp_ics_span_transport_result_image_raw_np_cell_dot_pointwise fpmp_right_dot_mcp_ics_span_transport_result_image_raw_np_cell_dot_pointwise fpmp_target_dot_mcp_ics_span_transport_result_image_raw_np_cell_dot_pointwise. (exists fpmp_gap_dot_mcp_ics_span_transport_result_image_raw_np_cell_dot_pointwise. fpmp_gap_dot_mcp_ics_span_transport_result_image_raw_np_cell_dot_pointwise + S fpmp_index_dot_mcp_ics_span_transport_result_image_raw_np_cell_dot_pointwise = w) -> (((exists ff_h_fpmp_dot_mcp_ics_span_transport_result_image_raw_np_cell_dot_pointwise_left. ff_h_fpmp_dot_mcp_ics_span_transport_result_image_raw_np_cell_dot_pointwise_left + S (fpmp_left_dot_mcp_ics_span_transport_result_image_raw_np_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_span_transport_result_image_raw_np_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_span_transport_result_image_raw_np_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_span_transport_result_image_raw_np_cell_dot_pointwise_left. ff_left_mcp_cell_ics_span_transport_result_image_raw_np_cell = ff_q_fpmp_dot_mcp_ics_span_transport_result_image_raw_np_cell_dot_pointwise_left * S ((S (fpmp_index_dot_mcp_ics_span_transport_result_image_raw_np_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_span_transport_result_image_raw_np_cell) + (fpmp_left_dot_mcp_ics_span_transport_result_image_raw_np_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_span_transport_result_image_raw_np_cell_dot_pointwise_right. ff_h_fpmp_dot_mcp_ics_span_transport_result_image_raw_np_cell_dot_pointwise_right + S (fpmp_right_dot_mcp_ics_span_transport_result_image_raw_np_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_span_transport_result_image_raw_np_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_span_transport_result_image_raw_np_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_span_transport_result_image_raw_np_cell_dot_pointwise_right. ff_right_mcp_cell_ics_span_transport_result_image_raw_np_cell = ff_q_fpmp_dot_mcp_ics_span_transport_result_image_raw_np_cell_dot_pointwise_right * S ((S (fpmp_index_dot_mcp_ics_span_transport_result_image_raw_np_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_span_transport_result_image_raw_np_cell) + (fpmp_right_dot_mcp_ics_span_transport_result_image_raw_np_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_span_transport_result_image_raw_np_cell_dot_pointwise_target. ff_h_fpmp_dot_mcp_ics_span_transport_result_image_raw_np_cell_dot_pointwise_target + S (fpmp_target_dot_mcp_ics_span_transport_result_image_raw_np_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_span_transport_result_image_raw_np_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_span_transport_result_image_raw_np_cell_dot)) /\ exists ff_q_fpmp_dot_mcp_ics_span_transport_result_image_raw_np_cell_dot_pointwise_target. ff_code_dot_mcp_ics_span_transport_result_image_raw_np_cell_dot = ff_q_fpmp_dot_mcp_ics_span_transport_result_image_raw_np_cell_dot_pointwise_target * S ((S (fpmp_index_dot_mcp_ics_span_transport_result_image_raw_np_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_span_transport_result_image_raw_np_cell_dot) + (fpmp_target_dot_mcp_ics_span_transport_result_image_raw_np_cell_dot_pointwise))) -> fpmp_target_dot_mcp_ics_span_transport_result_image_raw_np_cell_dot_pointwise = fpmp_left_dot_mcp_ics_span_transport_result_image_raw_np_cell_dot_pointwise * fpmp_right_dot_mcp_ics_span_transport_result_image_raw_np_cell_dot_pointwise) /\ (exists ff_u_dot_mcp_ics_span_transport_result_image_raw_np_cell_dot_sum ff_v_dot_mcp_ics_span_transport_result_image_raw_np_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_span_transport_result_image_raw_np_cell_dot_sum_start. ff_h_dot_mcp_ics_span_transport_result_image_raw_np_cell_dot_sum_start + S (0) = S ((S (0)) * ff_v_dot_mcp_ics_span_transport_result_image_raw_np_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_span_transport_result_image_raw_np_cell_dot_sum_start. ff_u_dot_mcp_ics_span_transport_result_image_raw_np_cell_dot_sum = ff_q_dot_mcp_ics_span_transport_result_image_raw_np_cell_dot_sum_start * S ((S (0)) * ff_v_dot_mcp_ics_span_transport_result_image_raw_np_cell_dot_sum) + (0))) /\ ((((exists ff_h_dot_mcp_ics_span_transport_result_image_raw_np_cell_dot_sum_terminal. ff_h_dot_mcp_ics_span_transport_result_image_raw_np_cell_dot_sum_terminal + S (ff_value_mcp_prefix_ics_span_transport_result_image_raw_np) = S ((S (w)) * ff_v_dot_mcp_ics_span_transport_result_image_raw_np_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_span_transport_result_image_raw_np_cell_dot_sum_terminal. ff_u_dot_mcp_ics_span_transport_result_image_raw_np_cell_dot_sum = ff_q_dot_mcp_ics_span_transport_result_image_raw_np_cell_dot_sum_terminal * S ((S (w)) * ff_v_dot_mcp_ics_span_transport_result_image_raw_np_cell_dot_sum) + (ff_value_mcp_prefix_ics_span_transport_result_image_raw_np))) /\ forall ff_i_dot_mcp_ics_span_transport_result_image_raw_np_cell_dot_sum. (exists ff_lt_dot_mcp_ics_span_transport_result_image_raw_np_cell_dot_sum_bound. ff_lt_dot_mcp_ics_span_transport_result_image_raw_np_cell_dot_sum_bound + S ff_i_dot_mcp_ics_span_transport_result_image_raw_np_cell_dot_sum = w) -> exists ff_a_dot_mcp_ics_span_transport_result_image_raw_np_cell_dot_sum ff_r_dot_mcp_ics_span_transport_result_image_raw_np_cell_dot_sum ff_s_dot_mcp_ics_span_transport_result_image_raw_np_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_span_transport_result_image_raw_np_cell_dot_sum_summand. ff_h_dot_mcp_ics_span_transport_result_image_raw_np_cell_dot_sum_summand + S (ff_a_dot_mcp_ics_span_transport_result_image_raw_np_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_span_transport_result_image_raw_np_cell_dot_sum)) * ff_scale_dot_mcp_ics_span_transport_result_image_raw_np_cell_dot)) /\ exists ff_q_dot_mcp_ics_span_transport_result_image_raw_np_cell_dot_sum_summand. ff_code_dot_mcp_ics_span_transport_result_image_raw_np_cell_dot = ff_q_dot_mcp_ics_span_transport_result_image_raw_np_cell_dot_sum_summand * S ((S (ff_i_dot_mcp_ics_span_transport_result_image_raw_np_cell_dot_sum)) * ff_scale_dot_mcp_ics_span_transport_result_image_raw_np_cell_dot) + (ff_a_dot_mcp_ics_span_transport_result_image_raw_np_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_span_transport_result_image_raw_np_cell_dot_sum_partial. ff_h_dot_mcp_ics_span_transport_result_image_raw_np_cell_dot_sum_partial + S (ff_r_dot_mcp_ics_span_transport_result_image_raw_np_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_span_transport_result_image_raw_np_cell_dot_sum)) * ff_v_dot_mcp_ics_span_transport_result_image_raw_np_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_span_transport_result_image_raw_np_cell_dot_sum_partial. ff_u_dot_mcp_ics_span_transport_result_image_raw_np_cell_dot_sum = ff_q_dot_mcp_ics_span_transport_result_image_raw_np_cell_dot_sum_partial * S ((S (ff_i_dot_mcp_ics_span_transport_result_image_raw_np_cell_dot_sum)) * ff_v_dot_mcp_ics_span_transport_result_image_raw_np_cell_dot_sum) + (ff_r_dot_mcp_ics_span_transport_result_image_raw_np_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_span_transport_result_image_raw_np_cell_dot_sum_successor. ff_h_dot_mcp_ics_span_transport_result_image_raw_np_cell_dot_sum_successor + S (ff_s_dot_mcp_ics_span_transport_result_image_raw_np_cell_dot_sum) = S ((S (S ff_i_dot_mcp_ics_span_transport_result_image_raw_np_cell_dot_sum)) * ff_v_dot_mcp_ics_span_transport_result_image_raw_np_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_span_transport_result_image_raw_np_cell_dot_sum_successor. ff_u_dot_mcp_ics_span_transport_result_image_raw_np_cell_dot_sum = ff_q_dot_mcp_ics_span_transport_result_image_raw_np_cell_dot_sum_successor * S ((S (S ff_i_dot_mcp_ics_span_transport_result_image_raw_np_cell_dot_sum)) * ff_v_dot_mcp_ics_span_transport_result_image_raw_np_cell_dot_sum) + (ff_s_dot_mcp_ics_span_transport_result_image_raw_np_cell_dot_sum))) /\ ff_s_dot_mcp_ics_span_transport_result_image_raw_np_cell_dot_sum = ff_r_dot_mcp_ics_span_transport_result_image_raw_np_cell_dot_sum + ff_a_dot_mcp_ics_span_transport_result_image_raw_np_cell_dot_sum))))))))))) /\ (((exists fs_h_mcp_ics_span_transport_result_image_raw_np_entry. fs_h_mcp_ics_span_transport_result_image_raw_np_entry + S (ff_value_mcp_prefix_ics_span_transport_result_image_raw_np) = S ((S (ff_index_mcp_prefix_ics_span_transport_result_image_raw_np)) * ff_nps_mcp_smatrix_ics_span_transport_result_image_raw)) /\ exists fs_q_mcp_ics_span_transport_result_image_raw_np_entry. ff_np_mcp_smatrix_ics_span_transport_result_image_raw = fs_q_mcp_ics_span_transport_result_image_raw_np_entry * S ((S (ff_index_mcp_prefix_ics_span_transport_result_image_raw_np)) * ff_nps_mcp_smatrix_ics_span_transport_result_image_raw) + (ff_value_mcp_prefix_ics_span_transport_result_image_raw_np))))))) /\ ((forall ff_index_mcp_add_ics_span_transport_result_image_raw_positive ff_left_mcp_add_ics_span_transport_result_image_raw_positive ff_right_mcp_add_ics_span_transport_result_image_raw_positive ff_target_mcp_add_ics_span_transport_result_image_raw_positive. (exists mcp_gap_ics_span_transport_result_image_raw_positive_bound. mcp_gap_ics_span_transport_result_image_raw_positive_bound + S (ff_index_mcp_add_ics_span_transport_result_image_raw_positive) = ((r) * (1))) -> (((exists fs_h_mcp_ics_span_transport_result_image_raw_positive_left. fs_h_mcp_ics_span_transport_result_image_raw_positive_left + S (ff_left_mcp_add_ics_span_transport_result_image_raw_positive) = S ((S (ff_index_mcp_add_ics_span_transport_result_image_raw_positive)) * ff_pps_mcp_smatrix_ics_span_transport_result_image_raw)) /\ exists fs_q_mcp_ics_span_transport_result_image_raw_positive_left. ff_pp_mcp_smatrix_ics_span_transport_result_image_raw = fs_q_mcp_ics_span_transport_result_image_raw_positive_left * S ((S (ff_index_mcp_add_ics_span_transport_result_image_raw_positive)) * ff_pps_mcp_smatrix_ics_span_transport_result_image_raw) + (ff_left_mcp_add_ics_span_transport_result_image_raw_positive))) -> (((exists fs_h_mcp_ics_span_transport_result_image_raw_positive_right. fs_h_mcp_ics_span_transport_result_image_raw_positive_right + S (ff_right_mcp_add_ics_span_transport_result_image_raw_positive) = S ((S (ff_index_mcp_add_ics_span_transport_result_image_raw_positive)) * ff_nns_mcp_smatrix_ics_span_transport_result_image_raw)) /\ exists fs_q_mcp_ics_span_transport_result_image_raw_positive_right. ff_nn_mcp_smatrix_ics_span_transport_result_image_raw = fs_q_mcp_ics_span_transport_result_image_raw_positive_right * S ((S (ff_index_mcp_add_ics_span_transport_result_image_raw_positive)) * ff_nns_mcp_smatrix_ics_span_transport_result_image_raw) + (ff_right_mcp_add_ics_span_transport_result_image_raw_positive))) -> (((exists fs_h_mcp_ics_span_transport_result_image_raw_positive_target. fs_h_mcp_ics_span_transport_result_image_raw_positive_target + S (ff_target_mcp_add_ics_span_transport_result_image_raw_positive) = S ((S (ff_index_mcp_add_ics_span_transport_result_image_raw_positive)) * ics_raw_positive_scale_span_transport_result_image)) /\ exists fs_q_mcp_ics_span_transport_result_image_raw_positive_target. ics_raw_positive_span_transport_result_image = fs_q_mcp_ics_span_transport_result_image_raw_positive_target * S ((S (ff_index_mcp_add_ics_span_transport_result_image_raw_positive)) * ics_raw_positive_scale_span_transport_result_image) + (ff_target_mcp_add_ics_span_transport_result_image_raw_positive))) -> ff_target_mcp_add_ics_span_transport_result_image_raw_positive = ff_left_mcp_add_ics_span_transport_result_image_raw_positive + ff_right_mcp_add_ics_span_transport_result_image_raw_positive) /\ (forall ff_index_mcp_add_ics_span_transport_result_image_raw_negative ff_left_mcp_add_ics_span_transport_result_image_raw_negative ff_right_mcp_add_ics_span_transport_result_image_raw_negative ff_target_mcp_add_ics_span_transport_result_image_raw_negative. (exists mcp_gap_ics_span_transport_result_image_raw_negative_bound. mcp_gap_ics_span_transport_result_image_raw_negative_bound + S (ff_index_mcp_add_ics_span_transport_result_image_raw_negative) = ((r) * (1))) -> (((exists fs_h_mcp_ics_span_transport_result_image_raw_negative_left. fs_h_mcp_ics_span_transport_result_image_raw_negative_left + S (ff_left_mcp_add_ics_span_transport_result_image_raw_negative) = S ((S (ff_index_mcp_add_ics_span_transport_result_image_raw_negative)) * ff_pns_mcp_smatrix_ics_span_transport_result_image_raw)) /\ exists fs_q_mcp_ics_span_transport_result_image_raw_negative_left. ff_pn_mcp_smatrix_ics_span_transport_result_image_raw = fs_q_mcp_ics_span_transport_result_image_raw_negative_left * S ((S (ff_index_mcp_add_ics_span_transport_result_image_raw_negative)) * ff_pns_mcp_smatrix_ics_span_transport_result_image_raw) + (ff_left_mcp_add_ics_span_transport_result_image_raw_negative))) -> (((exists fs_h_mcp_ics_span_transport_result_image_raw_negative_right. fs_h_mcp_ics_span_transport_result_image_raw_negative_right + S (ff_right_mcp_add_ics_span_transport_result_image_raw_negative) = S ((S (ff_index_mcp_add_ics_span_transport_result_image_raw_negative)) * ff_nps_mcp_smatrix_ics_span_transport_result_image_raw)) /\ exists fs_q_mcp_ics_span_transport_result_image_raw_negative_right. ff_np_mcp_smatrix_ics_span_transport_result_image_raw = fs_q_mcp_ics_span_transport_result_image_raw_negative_right * S ((S (ff_index_mcp_add_ics_span_transport_result_image_raw_negative)) * ff_nps_mcp_smatrix_ics_span_transport_result_image_raw) + (ff_right_mcp_add_ics_span_transport_result_image_raw_negative))) -> (((exists fs_h_mcp_ics_span_transport_result_image_raw_negative_target. fs_h_mcp_ics_span_transport_result_image_raw_negative_target + S (ff_target_mcp_add_ics_span_transport_result_image_raw_negative) = S ((S (ff_index_mcp_add_ics_span_transport_result_image_raw_negative)) * ics_raw_negative_scale_span_transport_result_image)) /\ exists fs_q_mcp_ics_span_transport_result_image_raw_negative_target. ics_raw_negative_span_transport_result_image = fs_q_mcp_ics_span_transport_result_image_raw_negative_target * S ((S (ff_index_mcp_add_ics_span_transport_result_image_raw_negative)) * ics_raw_negative_scale_span_transport_result_image) + (ff_target_mcp_add_ics_span_transport_result_image_raw_negative))) -> ff_target_mcp_add_ics_span_transport_result_image_raw_negative = ff_left_mcp_add_ics_span_transport_result_image_raw_negative + ff_right_mcp_add_ics_span_transport_result_image_raw_negative))))))) /\ (forall ics_index_span_transport_result_image_equal ics_value0_span_transport_result_image_equal ics_value1_span_transport_result_image_equal ics_value2_span_transport_result_image_equal ics_value3_span_transport_result_image_equal. (exists ics_gap_span_transport_result_image_equal_bound. ics_gap_span_transport_result_image_equal_bound + S (ics_index_span_transport_result_image_equal) = (r)) -> (((exists fs_h_ics_span_transport_result_image_equal_at0. fs_h_ics_span_transport_result_image_equal_at0 + S (ics_value0_span_transport_result_image_equal) = S ((S (ics_index_span_transport_result_image_equal)) * ics_raw_positive_scale_span_transport_result_image)) /\ exists fs_q_ics_span_transport_result_image_equal_at0. ics_raw_positive_span_transport_result_image = fs_q_ics_span_transport_result_image_equal_at0 * S ((S (ics_index_span_transport_result_image_equal)) * ics_raw_positive_scale_span_transport_result_image) + (ics_value0_span_transport_result_image_equal))) -> (((exists fs_h_ics_span_transport_result_image_equal_at1. fs_h_ics_span_transport_result_image_equal_at1 + S (ics_value1_span_transport_result_image_equal) = S ((S (ics_index_span_transport_result_image_equal)) * ics_raw_negative_scale_span_transport_result_image)) /\ exists fs_q_ics_span_transport_result_image_equal_at1. ics_raw_negative_span_transport_result_image = fs_q_ics_span_transport_result_image_equal_at1 * S ((S (ics_index_span_transport_result_image_equal)) * ics_raw_negative_scale_span_transport_result_image) + (ics_value1_span_transport_result_image_equal))) -> (((exists fs_h_ics_span_transport_result_image_equal_at2. fs_h_ics_span_transport_result_image_equal_at2 + S (ics_value2_span_transport_result_image_equal) = S ((S (ics_index_span_transport_result_image_equal)) * qc)) /\ exists fs_q_ics_span_transport_result_image_equal_at2. qb = fs_q_ics_span_transport_result_image_equal_at2 * S ((S (ics_index_span_transport_result_image_equal)) * qc) + (ics_value2_span_transport_result_image_equal))) -> (((exists fs_h_ics_span_transport_result_image_equal_at3. fs_h_ics_span_transport_result_image_equal_at3 + S (ics_value3_span_transport_result_image_equal) = S ((S (ics_index_span_transport_result_image_equal)) * mc)) /\ exists fs_q_ics_span_transport_result_image_equal_at3. mb = fs_q_ics_span_transport_result_image_equal_at3 * S ((S (ics_index_span_transport_result_image_equal)) * mc) + (ics_value3_span_transport_result_image_equal))) -> ics_value0_span_transport_result_image_equal + ics_value3_span_transport_result_image_equal = ics_value2_span_transport_result_image_equal + ics_value1_span_transport_result_image_equal)))))Complete tactic proof in conservative notation
All 45 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
45 script commands · 7 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 (1)
01Fix variables and assumptionsL1–10
02Fix variables and assumptionsL11–16
03Separate the logical casesL17–20
04Construct an explicit witnessL21–24
05Use earlier factsL25–34
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L25
specialize integer_matrix_vector_product_transport (ab) - L26
specialize integer_matrix_vector_product_transport (ac) - L27
specialize integer_matrix_vector_product_transport (db) - L28
specialize integer_matrix_vector_product_transport (dc) - L29
specialize integer_matrix_vector_product_transport (x) - L30
specialize integer_matrix_vector_product_transport (x1) - L31
specialize integer_matrix_vector_product_transport (x2) - L32
specialize integer_matrix_vector_product_transport (x3) - L33
specialize integer_matrix_vector_product_transport (w) - L34
specialize integer_matrix_vector_product_transport (r)
06Use earlier factsL35–44
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L35
specialize integer_matrix_vector_product_transport (pb) - L36
specialize integer_matrix_vector_product_transport (pc) - L37
specialize integer_matrix_vector_product_transport (nb) - L38
specialize integer_matrix_vector_product_transport (nc) - L39
specialize integer_matrix_vector_product_transport (qb) - L40
specialize integer_matrix_vector_product_transport (qc) - L41
specialize integer_matrix_vector_product_transport (mb) - L42
specialize integer_matrix_vector_product_transport (mc) - L43
apply integer_matrix_vector_product_transport - L44
exact hspan_witness_witness_witness_witness
07Use earlier factsL45–45
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L45
exact hequal
Original defined command ledger · 45 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 hequal - 0017
cases hspan - 0018
cases hspan_witness - 0019
cases hspan_witness_witness - 0020
cases hspan_witness_witness_witness - 0021
exists x - 0022
exists x1 - 0023
exists x2 - 0024
exists x3 - 0025
specialize integer_matrix_vector_product_transport (ab) - 0026
specialize integer_matrix_vector_product_transport (ac) - 0027
specialize integer_matrix_vector_product_transport (db) - 0028
specialize integer_matrix_vector_product_transport (dc) - 0029
specialize integer_matrix_vector_product_transport (x) - 0030
specialize integer_matrix_vector_product_transport (x1) - 0031
specialize integer_matrix_vector_product_transport (x2) - 0032
specialize integer_matrix_vector_product_transport (x3) - 0033
specialize integer_matrix_vector_product_transport (w) - 0034
specialize integer_matrix_vector_product_transport (r) - 0035
specialize integer_matrix_vector_product_transport (pb) - 0036
specialize integer_matrix_vector_product_transport (pc) - 0037
specialize integer_matrix_vector_product_transport (nb) - 0038
specialize integer_matrix_vector_product_transport (nc) - 0039
specialize integer_matrix_vector_product_transport (qb) - 0040
specialize integer_matrix_vector_product_transport (qc) - 0041
specialize integer_matrix_vector_product_transport (mb) - 0042
specialize integer_matrix_vector_product_transport (mc) - 0043
apply integer_matrix_vector_product_transport - 0044
exact hspan_witness_witness_witness_witness - 0045
exact hequal