Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.
Exact expanded first-order arithmetic statement
forall ab ac 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)))))Constructive proof overview
Generated structural guide
Column-span membership depends on the represented integer vector, not on its beta codes or its separate positive and negative components.
The unchanged tactic script uses 1 declared prerequisite and contains 45 exact native proof lines.
Alpha v34 checked-use · first admitted v27 · independently kernel and Lean verified; not Stable
Proof neighborhood
Direct dependencies
Direct dependents
Formal native tactic body
Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.
Read the argument
Proof checkpoints
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.
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 exact 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