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 eb ec fb fc gb gc hb hc ib ic jb jc w r pb pc nb nc qb qc mb mc rb rc sb sc. (forall ff_index_mcp_add_ics_sp_cofp ff_left_mcp_add_ics_sp_cofp ff_right_mcp_add_ics_sp_cofp ff_target_mcp_add_ics_sp_cofp. (exists mcp_gap_ics_sp_cofp_bound. mcp_gap_ics_sp_cofp_bound + S (ff_index_mcp_add_ics_sp_cofp) = (w)) -> (((exists fs_h_mcp_ics_sp_cofp_left. fs_h_mcp_ics_sp_cofp_left + S (ff_left_mcp_add_ics_sp_cofp) = S ((S (ff_index_mcp_add_ics_sp_cofp)) * ec)) /\ exists fs_q_mcp_ics_sp_cofp_left. eb = fs_q_mcp_ics_sp_cofp_left * S ((S (ff_index_mcp_add_ics_sp_cofp)) * ec) + (ff_left_mcp_add_ics_sp_cofp))) -> (((exists fs_h_mcp_ics_sp_cofp_right. fs_h_mcp_ics_sp_cofp_right + S (ff_right_mcp_add_ics_sp_cofp) = S ((S (ff_index_mcp_add_ics_sp_cofp)) * gc)) /\ exists fs_q_mcp_ics_sp_cofp_right. gb = fs_q_mcp_ics_sp_cofp_right * S ((S (ff_index_mcp_add_ics_sp_cofp)) * gc) + (ff_right_mcp_add_ics_sp_cofp))) -> (((exists fs_h_mcp_ics_sp_cofp_target. fs_h_mcp_ics_sp_cofp_target + S (ff_target_mcp_add_ics_sp_cofp) = S ((S (ff_index_mcp_add_ics_sp_cofp)) * ic)) /\ exists fs_q_mcp_ics_sp_cofp_target. ib = fs_q_mcp_ics_sp_cofp_target * S ((S (ff_index_mcp_add_ics_sp_cofp)) * ic) + (ff_target_mcp_add_ics_sp_cofp))) -> ff_target_mcp_add_ics_sp_cofp = ff_left_mcp_add_ics_sp_cofp + ff_right_mcp_add_ics_sp_cofp) -> (forall ff_index_mcp_add_ics_sp_cofn ff_left_mcp_add_ics_sp_cofn ff_right_mcp_add_ics_sp_cofn ff_target_mcp_add_ics_sp_cofn. (exists mcp_gap_ics_sp_cofn_bound. mcp_gap_ics_sp_cofn_bound + S (ff_index_mcp_add_ics_sp_cofn) = (w)) -> (((exists fs_h_mcp_ics_sp_cofn_left. fs_h_mcp_ics_sp_cofn_left + S (ff_left_mcp_add_ics_sp_cofn) = S ((S (ff_index_mcp_add_ics_sp_cofn)) * fc)) /\ exists fs_q_mcp_ics_sp_cofn_left. fb = fs_q_mcp_ics_sp_cofn_left * S ((S (ff_index_mcp_add_ics_sp_cofn)) * fc) + (ff_left_mcp_add_ics_sp_cofn))) -> (((exists fs_h_mcp_ics_sp_cofn_right. fs_h_mcp_ics_sp_cofn_right + S (ff_right_mcp_add_ics_sp_cofn) = S ((S (ff_index_mcp_add_ics_sp_cofn)) * hc)) /\ exists fs_q_mcp_ics_sp_cofn_right. hb = fs_q_mcp_ics_sp_cofn_right * S ((S (ff_index_mcp_add_ics_sp_cofn)) * hc) + (ff_right_mcp_add_ics_sp_cofn))) -> (((exists fs_h_mcp_ics_sp_cofn_target. fs_h_mcp_ics_sp_cofn_target + S (ff_target_mcp_add_ics_sp_cofn) = S ((S (ff_index_mcp_add_ics_sp_cofn)) * jc)) /\ exists fs_q_mcp_ics_sp_cofn_target. jb = fs_q_mcp_ics_sp_cofn_target * S ((S (ff_index_mcp_add_ics_sp_cofn)) * jc) + (ff_target_mcp_add_ics_sp_cofn))) -> ff_target_mcp_add_ics_sp_cofn = ff_left_mcp_add_ics_sp_cofn + ff_right_mcp_add_ics_sp_cofn) -> (exists ff_pp_mcp_smatrix_ics_sp0 ff_pps_mcp_smatrix_ics_sp0 ff_nn_mcp_smatrix_ics_sp0 ff_nns_mcp_smatrix_ics_sp0 ff_pn_mcp_smatrix_ics_sp0 ff_pns_mcp_smatrix_ics_sp0 ff_np_mcp_smatrix_ics_sp0 ff_nps_mcp_smatrix_ics_sp0. ((forall ff_index_mcp_prefix_ics_sp0_pp. (exists mcp_gap_ics_sp0_pp_index. mcp_gap_ics_sp0_pp_index + S (ff_index_mcp_prefix_ics_sp0_pp) = ((r) * (1))) -> exists ff_row_mcp_prefix_ics_sp0_pp ff_column_mcp_prefix_ics_sp0_pp ff_value_mcp_prefix_ics_sp0_pp. ((ff_index_mcp_prefix_ics_sp0_pp) = (1) * ff_row_mcp_prefix_ics_sp0_pp + ff_column_mcp_prefix_ics_sp0_pp /\ ((exists mcp_gap_ics_sp0_pp_column. mcp_gap_ics_sp0_pp_column + S (ff_column_mcp_prefix_ics_sp0_pp) = (1)) /\ ((exists ff_left_mcp_cell_ics_sp0_pp_cell ff_left_scale_mcp_cell_ics_sp0_pp_cell ff_right_mcp_cell_ics_sp0_pp_cell ff_right_scale_mcp_cell_ics_sp0_pp_cell. ((forall ff_index_mcp_ics_sp0_pp_cell_row ff_source_mcp_ics_sp0_pp_cell_row ff_target_mcp_ics_sp0_pp_cell_row. (exists mcp_gap_ics_sp0_pp_cell_row_bound. mcp_gap_ics_sp0_pp_cell_row_bound + S (ff_index_mcp_ics_sp0_pp_cell_row) = (w)) -> (((exists fs_h_mcp_ics_sp0_pp_cell_row_source. fs_h_mcp_ics_sp0_pp_cell_row_source + S (ff_source_mcp_ics_sp0_pp_cell_row) = S ((S (((ff_row_mcp_prefix_ics_sp0_pp) * (w)) + (1) * ff_index_mcp_ics_sp0_pp_cell_row)) * ac)) /\ exists fs_q_mcp_ics_sp0_pp_cell_row_source. ab = fs_q_mcp_ics_sp0_pp_cell_row_source * S ((S (((ff_row_mcp_prefix_ics_sp0_pp) * (w)) + (1) * ff_index_mcp_ics_sp0_pp_cell_row)) * ac) + (ff_source_mcp_ics_sp0_pp_cell_row))) -> (((exists fs_h_mcp_ics_sp0_pp_cell_row_target. fs_h_mcp_ics_sp0_pp_cell_row_target + S (ff_target_mcp_ics_sp0_pp_cell_row) = S ((S (ff_index_mcp_ics_sp0_pp_cell_row)) * ff_left_scale_mcp_cell_ics_sp0_pp_cell)) /\ exists fs_q_mcp_ics_sp0_pp_cell_row_target. ff_left_mcp_cell_ics_sp0_pp_cell = fs_q_mcp_ics_sp0_pp_cell_row_target * S ((S (ff_index_mcp_ics_sp0_pp_cell_row)) * ff_left_scale_mcp_cell_ics_sp0_pp_cell) + (ff_target_mcp_ics_sp0_pp_cell_row))) -> ff_target_mcp_ics_sp0_pp_cell_row = ff_source_mcp_ics_sp0_pp_cell_row) /\ ((forall ff_index_mcp_ics_sp0_pp_cell_column ff_source_mcp_ics_sp0_pp_cell_column ff_target_mcp_ics_sp0_pp_cell_column. (exists mcp_gap_ics_sp0_pp_cell_column_bound. mcp_gap_ics_sp0_pp_cell_column_bound + S (ff_index_mcp_ics_sp0_pp_cell_column) = (w)) -> (((exists fs_h_mcp_ics_sp0_pp_cell_column_source. fs_h_mcp_ics_sp0_pp_cell_column_source + S (ff_source_mcp_ics_sp0_pp_cell_column) = S ((S ((ff_column_mcp_prefix_ics_sp0_pp) + (1) * ff_index_mcp_ics_sp0_pp_cell_column)) * ec)) /\ exists fs_q_mcp_ics_sp0_pp_cell_column_source. eb = fs_q_mcp_ics_sp0_pp_cell_column_source * S ((S ((ff_column_mcp_prefix_ics_sp0_pp) + (1) * ff_index_mcp_ics_sp0_pp_cell_column)) * ec) + (ff_source_mcp_ics_sp0_pp_cell_column))) -> (((exists fs_h_mcp_ics_sp0_pp_cell_column_target. fs_h_mcp_ics_sp0_pp_cell_column_target + S (ff_target_mcp_ics_sp0_pp_cell_column) = S ((S (ff_index_mcp_ics_sp0_pp_cell_column)) * ff_right_scale_mcp_cell_ics_sp0_pp_cell)) /\ exists fs_q_mcp_ics_sp0_pp_cell_column_target. ff_right_mcp_cell_ics_sp0_pp_cell = fs_q_mcp_ics_sp0_pp_cell_column_target * S ((S (ff_index_mcp_ics_sp0_pp_cell_column)) * ff_right_scale_mcp_cell_ics_sp0_pp_cell) + (ff_target_mcp_ics_sp0_pp_cell_column))) -> ff_target_mcp_ics_sp0_pp_cell_column = ff_source_mcp_ics_sp0_pp_cell_column) /\ (exists ff_code_dot_mcp_ics_sp0_pp_cell_dot ff_scale_dot_mcp_ics_sp0_pp_cell_dot. ((forall fpmp_index_dot_mcp_ics_sp0_pp_cell_dot_pointwise fpmp_left_dot_mcp_ics_sp0_pp_cell_dot_pointwise fpmp_right_dot_mcp_ics_sp0_pp_cell_dot_pointwise fpmp_target_dot_mcp_ics_sp0_pp_cell_dot_pointwise. (exists fpmp_gap_dot_mcp_ics_sp0_pp_cell_dot_pointwise. fpmp_gap_dot_mcp_ics_sp0_pp_cell_dot_pointwise + S fpmp_index_dot_mcp_ics_sp0_pp_cell_dot_pointwise = w) -> (((exists ff_h_fpmp_dot_mcp_ics_sp0_pp_cell_dot_pointwise_left. ff_h_fpmp_dot_mcp_ics_sp0_pp_cell_dot_pointwise_left + S (fpmp_left_dot_mcp_ics_sp0_pp_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_sp0_pp_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_sp0_pp_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_sp0_pp_cell_dot_pointwise_left. ff_left_mcp_cell_ics_sp0_pp_cell = ff_q_fpmp_dot_mcp_ics_sp0_pp_cell_dot_pointwise_left * S ((S (fpmp_index_dot_mcp_ics_sp0_pp_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_sp0_pp_cell) + (fpmp_left_dot_mcp_ics_sp0_pp_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_sp0_pp_cell_dot_pointwise_right. ff_h_fpmp_dot_mcp_ics_sp0_pp_cell_dot_pointwise_right + S (fpmp_right_dot_mcp_ics_sp0_pp_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_sp0_pp_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_sp0_pp_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_sp0_pp_cell_dot_pointwise_right. ff_right_mcp_cell_ics_sp0_pp_cell = ff_q_fpmp_dot_mcp_ics_sp0_pp_cell_dot_pointwise_right * S ((S (fpmp_index_dot_mcp_ics_sp0_pp_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_sp0_pp_cell) + (fpmp_right_dot_mcp_ics_sp0_pp_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_sp0_pp_cell_dot_pointwise_target. ff_h_fpmp_dot_mcp_ics_sp0_pp_cell_dot_pointwise_target + S (fpmp_target_dot_mcp_ics_sp0_pp_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_sp0_pp_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_sp0_pp_cell_dot)) /\ exists ff_q_fpmp_dot_mcp_ics_sp0_pp_cell_dot_pointwise_target. ff_code_dot_mcp_ics_sp0_pp_cell_dot = ff_q_fpmp_dot_mcp_ics_sp0_pp_cell_dot_pointwise_target * S ((S (fpmp_index_dot_mcp_ics_sp0_pp_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_sp0_pp_cell_dot) + (fpmp_target_dot_mcp_ics_sp0_pp_cell_dot_pointwise))) -> fpmp_target_dot_mcp_ics_sp0_pp_cell_dot_pointwise = fpmp_left_dot_mcp_ics_sp0_pp_cell_dot_pointwise * fpmp_right_dot_mcp_ics_sp0_pp_cell_dot_pointwise) /\ (exists ff_u_dot_mcp_ics_sp0_pp_cell_dot_sum ff_v_dot_mcp_ics_sp0_pp_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_sp0_pp_cell_dot_sum_start. ff_h_dot_mcp_ics_sp0_pp_cell_dot_sum_start + S (0) = S ((S (0)) * ff_v_dot_mcp_ics_sp0_pp_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_sp0_pp_cell_dot_sum_start. ff_u_dot_mcp_ics_sp0_pp_cell_dot_sum = ff_q_dot_mcp_ics_sp0_pp_cell_dot_sum_start * S ((S (0)) * ff_v_dot_mcp_ics_sp0_pp_cell_dot_sum) + (0))) /\ ((((exists ff_h_dot_mcp_ics_sp0_pp_cell_dot_sum_terminal. ff_h_dot_mcp_ics_sp0_pp_cell_dot_sum_terminal + S (ff_value_mcp_prefix_ics_sp0_pp) = S ((S (w)) * ff_v_dot_mcp_ics_sp0_pp_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_sp0_pp_cell_dot_sum_terminal. ff_u_dot_mcp_ics_sp0_pp_cell_dot_sum = ff_q_dot_mcp_ics_sp0_pp_cell_dot_sum_terminal * S ((S (w)) * ff_v_dot_mcp_ics_sp0_pp_cell_dot_sum) + (ff_value_mcp_prefix_ics_sp0_pp))) /\ forall ff_i_dot_mcp_ics_sp0_pp_cell_dot_sum. (exists ff_lt_dot_mcp_ics_sp0_pp_cell_dot_sum_bound. ff_lt_dot_mcp_ics_sp0_pp_cell_dot_sum_bound + S ff_i_dot_mcp_ics_sp0_pp_cell_dot_sum = w) -> exists ff_a_dot_mcp_ics_sp0_pp_cell_dot_sum ff_r_dot_mcp_ics_sp0_pp_cell_dot_sum ff_s_dot_mcp_ics_sp0_pp_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_sp0_pp_cell_dot_sum_summand. ff_h_dot_mcp_ics_sp0_pp_cell_dot_sum_summand + S (ff_a_dot_mcp_ics_sp0_pp_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_sp0_pp_cell_dot_sum)) * ff_scale_dot_mcp_ics_sp0_pp_cell_dot)) /\ exists ff_q_dot_mcp_ics_sp0_pp_cell_dot_sum_summand. ff_code_dot_mcp_ics_sp0_pp_cell_dot = ff_q_dot_mcp_ics_sp0_pp_cell_dot_sum_summand * S ((S (ff_i_dot_mcp_ics_sp0_pp_cell_dot_sum)) * ff_scale_dot_mcp_ics_sp0_pp_cell_dot) + (ff_a_dot_mcp_ics_sp0_pp_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_sp0_pp_cell_dot_sum_partial. ff_h_dot_mcp_ics_sp0_pp_cell_dot_sum_partial + S (ff_r_dot_mcp_ics_sp0_pp_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_sp0_pp_cell_dot_sum)) * ff_v_dot_mcp_ics_sp0_pp_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_sp0_pp_cell_dot_sum_partial. ff_u_dot_mcp_ics_sp0_pp_cell_dot_sum = ff_q_dot_mcp_ics_sp0_pp_cell_dot_sum_partial * S ((S (ff_i_dot_mcp_ics_sp0_pp_cell_dot_sum)) * ff_v_dot_mcp_ics_sp0_pp_cell_dot_sum) + (ff_r_dot_mcp_ics_sp0_pp_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_sp0_pp_cell_dot_sum_successor. ff_h_dot_mcp_ics_sp0_pp_cell_dot_sum_successor + S (ff_s_dot_mcp_ics_sp0_pp_cell_dot_sum) = S ((S (S ff_i_dot_mcp_ics_sp0_pp_cell_dot_sum)) * ff_v_dot_mcp_ics_sp0_pp_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_sp0_pp_cell_dot_sum_successor. ff_u_dot_mcp_ics_sp0_pp_cell_dot_sum = ff_q_dot_mcp_ics_sp0_pp_cell_dot_sum_successor * S ((S (S ff_i_dot_mcp_ics_sp0_pp_cell_dot_sum)) * ff_v_dot_mcp_ics_sp0_pp_cell_dot_sum) + (ff_s_dot_mcp_ics_sp0_pp_cell_dot_sum))) /\ ff_s_dot_mcp_ics_sp0_pp_cell_dot_sum = ff_r_dot_mcp_ics_sp0_pp_cell_dot_sum + ff_a_dot_mcp_ics_sp0_pp_cell_dot_sum))))))))))) /\ (((exists fs_h_mcp_ics_sp0_pp_entry. fs_h_mcp_ics_sp0_pp_entry + S (ff_value_mcp_prefix_ics_sp0_pp) = S ((S (ff_index_mcp_prefix_ics_sp0_pp)) * ff_pps_mcp_smatrix_ics_sp0)) /\ exists fs_q_mcp_ics_sp0_pp_entry. ff_pp_mcp_smatrix_ics_sp0 = fs_q_mcp_ics_sp0_pp_entry * S ((S (ff_index_mcp_prefix_ics_sp0_pp)) * ff_pps_mcp_smatrix_ics_sp0) + (ff_value_mcp_prefix_ics_sp0_pp))))))) /\ ((forall ff_index_mcp_prefix_ics_sp0_nn. (exists mcp_gap_ics_sp0_nn_index. mcp_gap_ics_sp0_nn_index + S (ff_index_mcp_prefix_ics_sp0_nn) = ((r) * (1))) -> exists ff_row_mcp_prefix_ics_sp0_nn ff_column_mcp_prefix_ics_sp0_nn ff_value_mcp_prefix_ics_sp0_nn. ((ff_index_mcp_prefix_ics_sp0_nn) = (1) * ff_row_mcp_prefix_ics_sp0_nn + ff_column_mcp_prefix_ics_sp0_nn /\ ((exists mcp_gap_ics_sp0_nn_column. mcp_gap_ics_sp0_nn_column + S (ff_column_mcp_prefix_ics_sp0_nn) = (1)) /\ ((exists ff_left_mcp_cell_ics_sp0_nn_cell ff_left_scale_mcp_cell_ics_sp0_nn_cell ff_right_mcp_cell_ics_sp0_nn_cell ff_right_scale_mcp_cell_ics_sp0_nn_cell. ((forall ff_index_mcp_ics_sp0_nn_cell_row ff_source_mcp_ics_sp0_nn_cell_row ff_target_mcp_ics_sp0_nn_cell_row. (exists mcp_gap_ics_sp0_nn_cell_row_bound. mcp_gap_ics_sp0_nn_cell_row_bound + S (ff_index_mcp_ics_sp0_nn_cell_row) = (w)) -> (((exists fs_h_mcp_ics_sp0_nn_cell_row_source. fs_h_mcp_ics_sp0_nn_cell_row_source + S (ff_source_mcp_ics_sp0_nn_cell_row) = S ((S (((ff_row_mcp_prefix_ics_sp0_nn) * (w)) + (1) * ff_index_mcp_ics_sp0_nn_cell_row)) * dc)) /\ exists fs_q_mcp_ics_sp0_nn_cell_row_source. db = fs_q_mcp_ics_sp0_nn_cell_row_source * S ((S (((ff_row_mcp_prefix_ics_sp0_nn) * (w)) + (1) * ff_index_mcp_ics_sp0_nn_cell_row)) * dc) + (ff_source_mcp_ics_sp0_nn_cell_row))) -> (((exists fs_h_mcp_ics_sp0_nn_cell_row_target. fs_h_mcp_ics_sp0_nn_cell_row_target + S (ff_target_mcp_ics_sp0_nn_cell_row) = S ((S (ff_index_mcp_ics_sp0_nn_cell_row)) * ff_left_scale_mcp_cell_ics_sp0_nn_cell)) /\ exists fs_q_mcp_ics_sp0_nn_cell_row_target. ff_left_mcp_cell_ics_sp0_nn_cell = fs_q_mcp_ics_sp0_nn_cell_row_target * S ((S (ff_index_mcp_ics_sp0_nn_cell_row)) * ff_left_scale_mcp_cell_ics_sp0_nn_cell) + (ff_target_mcp_ics_sp0_nn_cell_row))) -> ff_target_mcp_ics_sp0_nn_cell_row = ff_source_mcp_ics_sp0_nn_cell_row) /\ ((forall ff_index_mcp_ics_sp0_nn_cell_column ff_source_mcp_ics_sp0_nn_cell_column ff_target_mcp_ics_sp0_nn_cell_column. (exists mcp_gap_ics_sp0_nn_cell_column_bound. mcp_gap_ics_sp0_nn_cell_column_bound + S (ff_index_mcp_ics_sp0_nn_cell_column) = (w)) -> (((exists fs_h_mcp_ics_sp0_nn_cell_column_source. fs_h_mcp_ics_sp0_nn_cell_column_source + S (ff_source_mcp_ics_sp0_nn_cell_column) = S ((S ((ff_column_mcp_prefix_ics_sp0_nn) + (1) * ff_index_mcp_ics_sp0_nn_cell_column)) * fc)) /\ exists fs_q_mcp_ics_sp0_nn_cell_column_source. fb = fs_q_mcp_ics_sp0_nn_cell_column_source * S ((S ((ff_column_mcp_prefix_ics_sp0_nn) + (1) * ff_index_mcp_ics_sp0_nn_cell_column)) * fc) + (ff_source_mcp_ics_sp0_nn_cell_column))) -> (((exists fs_h_mcp_ics_sp0_nn_cell_column_target. fs_h_mcp_ics_sp0_nn_cell_column_target + S (ff_target_mcp_ics_sp0_nn_cell_column) = S ((S (ff_index_mcp_ics_sp0_nn_cell_column)) * ff_right_scale_mcp_cell_ics_sp0_nn_cell)) /\ exists fs_q_mcp_ics_sp0_nn_cell_column_target. ff_right_mcp_cell_ics_sp0_nn_cell = fs_q_mcp_ics_sp0_nn_cell_column_target * S ((S (ff_index_mcp_ics_sp0_nn_cell_column)) * ff_right_scale_mcp_cell_ics_sp0_nn_cell) + (ff_target_mcp_ics_sp0_nn_cell_column))) -> ff_target_mcp_ics_sp0_nn_cell_column = ff_source_mcp_ics_sp0_nn_cell_column) /\ (exists ff_code_dot_mcp_ics_sp0_nn_cell_dot ff_scale_dot_mcp_ics_sp0_nn_cell_dot. ((forall fpmp_index_dot_mcp_ics_sp0_nn_cell_dot_pointwise fpmp_left_dot_mcp_ics_sp0_nn_cell_dot_pointwise fpmp_right_dot_mcp_ics_sp0_nn_cell_dot_pointwise fpmp_target_dot_mcp_ics_sp0_nn_cell_dot_pointwise. (exists fpmp_gap_dot_mcp_ics_sp0_nn_cell_dot_pointwise. fpmp_gap_dot_mcp_ics_sp0_nn_cell_dot_pointwise + S fpmp_index_dot_mcp_ics_sp0_nn_cell_dot_pointwise = w) -> (((exists ff_h_fpmp_dot_mcp_ics_sp0_nn_cell_dot_pointwise_left. ff_h_fpmp_dot_mcp_ics_sp0_nn_cell_dot_pointwise_left + S (fpmp_left_dot_mcp_ics_sp0_nn_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_sp0_nn_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_sp0_nn_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_sp0_nn_cell_dot_pointwise_left. ff_left_mcp_cell_ics_sp0_nn_cell = ff_q_fpmp_dot_mcp_ics_sp0_nn_cell_dot_pointwise_left * S ((S (fpmp_index_dot_mcp_ics_sp0_nn_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_sp0_nn_cell) + (fpmp_left_dot_mcp_ics_sp0_nn_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_sp0_nn_cell_dot_pointwise_right. ff_h_fpmp_dot_mcp_ics_sp0_nn_cell_dot_pointwise_right + S (fpmp_right_dot_mcp_ics_sp0_nn_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_sp0_nn_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_sp0_nn_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_sp0_nn_cell_dot_pointwise_right. ff_right_mcp_cell_ics_sp0_nn_cell = ff_q_fpmp_dot_mcp_ics_sp0_nn_cell_dot_pointwise_right * S ((S (fpmp_index_dot_mcp_ics_sp0_nn_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_sp0_nn_cell) + (fpmp_right_dot_mcp_ics_sp0_nn_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_sp0_nn_cell_dot_pointwise_target. ff_h_fpmp_dot_mcp_ics_sp0_nn_cell_dot_pointwise_target + S (fpmp_target_dot_mcp_ics_sp0_nn_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_sp0_nn_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_sp0_nn_cell_dot)) /\ exists ff_q_fpmp_dot_mcp_ics_sp0_nn_cell_dot_pointwise_target. ff_code_dot_mcp_ics_sp0_nn_cell_dot = ff_q_fpmp_dot_mcp_ics_sp0_nn_cell_dot_pointwise_target * S ((S (fpmp_index_dot_mcp_ics_sp0_nn_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_sp0_nn_cell_dot) + (fpmp_target_dot_mcp_ics_sp0_nn_cell_dot_pointwise))) -> fpmp_target_dot_mcp_ics_sp0_nn_cell_dot_pointwise = fpmp_left_dot_mcp_ics_sp0_nn_cell_dot_pointwise * fpmp_right_dot_mcp_ics_sp0_nn_cell_dot_pointwise) /\ (exists ff_u_dot_mcp_ics_sp0_nn_cell_dot_sum ff_v_dot_mcp_ics_sp0_nn_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_sp0_nn_cell_dot_sum_start. ff_h_dot_mcp_ics_sp0_nn_cell_dot_sum_start + S (0) = S ((S (0)) * ff_v_dot_mcp_ics_sp0_nn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_sp0_nn_cell_dot_sum_start. ff_u_dot_mcp_ics_sp0_nn_cell_dot_sum = ff_q_dot_mcp_ics_sp0_nn_cell_dot_sum_start * S ((S (0)) * ff_v_dot_mcp_ics_sp0_nn_cell_dot_sum) + (0))) /\ ((((exists ff_h_dot_mcp_ics_sp0_nn_cell_dot_sum_terminal. ff_h_dot_mcp_ics_sp0_nn_cell_dot_sum_terminal + S (ff_value_mcp_prefix_ics_sp0_nn) = S ((S (w)) * ff_v_dot_mcp_ics_sp0_nn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_sp0_nn_cell_dot_sum_terminal. ff_u_dot_mcp_ics_sp0_nn_cell_dot_sum = ff_q_dot_mcp_ics_sp0_nn_cell_dot_sum_terminal * S ((S (w)) * ff_v_dot_mcp_ics_sp0_nn_cell_dot_sum) + (ff_value_mcp_prefix_ics_sp0_nn))) /\ forall ff_i_dot_mcp_ics_sp0_nn_cell_dot_sum. (exists ff_lt_dot_mcp_ics_sp0_nn_cell_dot_sum_bound. ff_lt_dot_mcp_ics_sp0_nn_cell_dot_sum_bound + S ff_i_dot_mcp_ics_sp0_nn_cell_dot_sum = w) -> exists ff_a_dot_mcp_ics_sp0_nn_cell_dot_sum ff_r_dot_mcp_ics_sp0_nn_cell_dot_sum ff_s_dot_mcp_ics_sp0_nn_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_sp0_nn_cell_dot_sum_summand. ff_h_dot_mcp_ics_sp0_nn_cell_dot_sum_summand + S (ff_a_dot_mcp_ics_sp0_nn_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_sp0_nn_cell_dot_sum)) * ff_scale_dot_mcp_ics_sp0_nn_cell_dot)) /\ exists ff_q_dot_mcp_ics_sp0_nn_cell_dot_sum_summand. ff_code_dot_mcp_ics_sp0_nn_cell_dot = ff_q_dot_mcp_ics_sp0_nn_cell_dot_sum_summand * S ((S (ff_i_dot_mcp_ics_sp0_nn_cell_dot_sum)) * ff_scale_dot_mcp_ics_sp0_nn_cell_dot) + (ff_a_dot_mcp_ics_sp0_nn_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_sp0_nn_cell_dot_sum_partial. ff_h_dot_mcp_ics_sp0_nn_cell_dot_sum_partial + S (ff_r_dot_mcp_ics_sp0_nn_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_sp0_nn_cell_dot_sum)) * ff_v_dot_mcp_ics_sp0_nn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_sp0_nn_cell_dot_sum_partial. ff_u_dot_mcp_ics_sp0_nn_cell_dot_sum = ff_q_dot_mcp_ics_sp0_nn_cell_dot_sum_partial * S ((S (ff_i_dot_mcp_ics_sp0_nn_cell_dot_sum)) * ff_v_dot_mcp_ics_sp0_nn_cell_dot_sum) + (ff_r_dot_mcp_ics_sp0_nn_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_sp0_nn_cell_dot_sum_successor. ff_h_dot_mcp_ics_sp0_nn_cell_dot_sum_successor + S (ff_s_dot_mcp_ics_sp0_nn_cell_dot_sum) = S ((S (S ff_i_dot_mcp_ics_sp0_nn_cell_dot_sum)) * ff_v_dot_mcp_ics_sp0_nn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_sp0_nn_cell_dot_sum_successor. ff_u_dot_mcp_ics_sp0_nn_cell_dot_sum = ff_q_dot_mcp_ics_sp0_nn_cell_dot_sum_successor * S ((S (S ff_i_dot_mcp_ics_sp0_nn_cell_dot_sum)) * ff_v_dot_mcp_ics_sp0_nn_cell_dot_sum) + (ff_s_dot_mcp_ics_sp0_nn_cell_dot_sum))) /\ ff_s_dot_mcp_ics_sp0_nn_cell_dot_sum = ff_r_dot_mcp_ics_sp0_nn_cell_dot_sum + ff_a_dot_mcp_ics_sp0_nn_cell_dot_sum))))))))))) /\ (((exists fs_h_mcp_ics_sp0_nn_entry. fs_h_mcp_ics_sp0_nn_entry + S (ff_value_mcp_prefix_ics_sp0_nn) = S ((S (ff_index_mcp_prefix_ics_sp0_nn)) * ff_nns_mcp_smatrix_ics_sp0)) /\ exists fs_q_mcp_ics_sp0_nn_entry. ff_nn_mcp_smatrix_ics_sp0 = fs_q_mcp_ics_sp0_nn_entry * S ((S (ff_index_mcp_prefix_ics_sp0_nn)) * ff_nns_mcp_smatrix_ics_sp0) + (ff_value_mcp_prefix_ics_sp0_nn))))))) /\ ((forall ff_index_mcp_prefix_ics_sp0_pn. (exists mcp_gap_ics_sp0_pn_index. mcp_gap_ics_sp0_pn_index + S (ff_index_mcp_prefix_ics_sp0_pn) = ((r) * (1))) -> exists ff_row_mcp_prefix_ics_sp0_pn ff_column_mcp_prefix_ics_sp0_pn ff_value_mcp_prefix_ics_sp0_pn. ((ff_index_mcp_prefix_ics_sp0_pn) = (1) * ff_row_mcp_prefix_ics_sp0_pn + ff_column_mcp_prefix_ics_sp0_pn /\ ((exists mcp_gap_ics_sp0_pn_column. mcp_gap_ics_sp0_pn_column + S (ff_column_mcp_prefix_ics_sp0_pn) = (1)) /\ ((exists ff_left_mcp_cell_ics_sp0_pn_cell ff_left_scale_mcp_cell_ics_sp0_pn_cell ff_right_mcp_cell_ics_sp0_pn_cell ff_right_scale_mcp_cell_ics_sp0_pn_cell. ((forall ff_index_mcp_ics_sp0_pn_cell_row ff_source_mcp_ics_sp0_pn_cell_row ff_target_mcp_ics_sp0_pn_cell_row. (exists mcp_gap_ics_sp0_pn_cell_row_bound. mcp_gap_ics_sp0_pn_cell_row_bound + S (ff_index_mcp_ics_sp0_pn_cell_row) = (w)) -> (((exists fs_h_mcp_ics_sp0_pn_cell_row_source. fs_h_mcp_ics_sp0_pn_cell_row_source + S (ff_source_mcp_ics_sp0_pn_cell_row) = S ((S (((ff_row_mcp_prefix_ics_sp0_pn) * (w)) + (1) * ff_index_mcp_ics_sp0_pn_cell_row)) * ac)) /\ exists fs_q_mcp_ics_sp0_pn_cell_row_source. ab = fs_q_mcp_ics_sp0_pn_cell_row_source * S ((S (((ff_row_mcp_prefix_ics_sp0_pn) * (w)) + (1) * ff_index_mcp_ics_sp0_pn_cell_row)) * ac) + (ff_source_mcp_ics_sp0_pn_cell_row))) -> (((exists fs_h_mcp_ics_sp0_pn_cell_row_target. fs_h_mcp_ics_sp0_pn_cell_row_target + S (ff_target_mcp_ics_sp0_pn_cell_row) = S ((S (ff_index_mcp_ics_sp0_pn_cell_row)) * ff_left_scale_mcp_cell_ics_sp0_pn_cell)) /\ exists fs_q_mcp_ics_sp0_pn_cell_row_target. ff_left_mcp_cell_ics_sp0_pn_cell = fs_q_mcp_ics_sp0_pn_cell_row_target * S ((S (ff_index_mcp_ics_sp0_pn_cell_row)) * ff_left_scale_mcp_cell_ics_sp0_pn_cell) + (ff_target_mcp_ics_sp0_pn_cell_row))) -> ff_target_mcp_ics_sp0_pn_cell_row = ff_source_mcp_ics_sp0_pn_cell_row) /\ ((forall ff_index_mcp_ics_sp0_pn_cell_column ff_source_mcp_ics_sp0_pn_cell_column ff_target_mcp_ics_sp0_pn_cell_column. (exists mcp_gap_ics_sp0_pn_cell_column_bound. mcp_gap_ics_sp0_pn_cell_column_bound + S (ff_index_mcp_ics_sp0_pn_cell_column) = (w)) -> (((exists fs_h_mcp_ics_sp0_pn_cell_column_source. fs_h_mcp_ics_sp0_pn_cell_column_source + S (ff_source_mcp_ics_sp0_pn_cell_column) = S ((S ((ff_column_mcp_prefix_ics_sp0_pn) + (1) * ff_index_mcp_ics_sp0_pn_cell_column)) * fc)) /\ exists fs_q_mcp_ics_sp0_pn_cell_column_source. fb = fs_q_mcp_ics_sp0_pn_cell_column_source * S ((S ((ff_column_mcp_prefix_ics_sp0_pn) + (1) * ff_index_mcp_ics_sp0_pn_cell_column)) * fc) + (ff_source_mcp_ics_sp0_pn_cell_column))) -> (((exists fs_h_mcp_ics_sp0_pn_cell_column_target. fs_h_mcp_ics_sp0_pn_cell_column_target + S (ff_target_mcp_ics_sp0_pn_cell_column) = S ((S (ff_index_mcp_ics_sp0_pn_cell_column)) * ff_right_scale_mcp_cell_ics_sp0_pn_cell)) /\ exists fs_q_mcp_ics_sp0_pn_cell_column_target. ff_right_mcp_cell_ics_sp0_pn_cell = fs_q_mcp_ics_sp0_pn_cell_column_target * S ((S (ff_index_mcp_ics_sp0_pn_cell_column)) * ff_right_scale_mcp_cell_ics_sp0_pn_cell) + (ff_target_mcp_ics_sp0_pn_cell_column))) -> ff_target_mcp_ics_sp0_pn_cell_column = ff_source_mcp_ics_sp0_pn_cell_column) /\ (exists ff_code_dot_mcp_ics_sp0_pn_cell_dot ff_scale_dot_mcp_ics_sp0_pn_cell_dot. ((forall fpmp_index_dot_mcp_ics_sp0_pn_cell_dot_pointwise fpmp_left_dot_mcp_ics_sp0_pn_cell_dot_pointwise fpmp_right_dot_mcp_ics_sp0_pn_cell_dot_pointwise fpmp_target_dot_mcp_ics_sp0_pn_cell_dot_pointwise. (exists fpmp_gap_dot_mcp_ics_sp0_pn_cell_dot_pointwise. fpmp_gap_dot_mcp_ics_sp0_pn_cell_dot_pointwise + S fpmp_index_dot_mcp_ics_sp0_pn_cell_dot_pointwise = w) -> (((exists ff_h_fpmp_dot_mcp_ics_sp0_pn_cell_dot_pointwise_left. ff_h_fpmp_dot_mcp_ics_sp0_pn_cell_dot_pointwise_left + S (fpmp_left_dot_mcp_ics_sp0_pn_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_sp0_pn_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_sp0_pn_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_sp0_pn_cell_dot_pointwise_left. ff_left_mcp_cell_ics_sp0_pn_cell = ff_q_fpmp_dot_mcp_ics_sp0_pn_cell_dot_pointwise_left * S ((S (fpmp_index_dot_mcp_ics_sp0_pn_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_sp0_pn_cell) + (fpmp_left_dot_mcp_ics_sp0_pn_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_sp0_pn_cell_dot_pointwise_right. ff_h_fpmp_dot_mcp_ics_sp0_pn_cell_dot_pointwise_right + S (fpmp_right_dot_mcp_ics_sp0_pn_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_sp0_pn_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_sp0_pn_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_sp0_pn_cell_dot_pointwise_right. ff_right_mcp_cell_ics_sp0_pn_cell = ff_q_fpmp_dot_mcp_ics_sp0_pn_cell_dot_pointwise_right * S ((S (fpmp_index_dot_mcp_ics_sp0_pn_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_sp0_pn_cell) + (fpmp_right_dot_mcp_ics_sp0_pn_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_sp0_pn_cell_dot_pointwise_target. ff_h_fpmp_dot_mcp_ics_sp0_pn_cell_dot_pointwise_target + S (fpmp_target_dot_mcp_ics_sp0_pn_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_sp0_pn_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_sp0_pn_cell_dot)) /\ exists ff_q_fpmp_dot_mcp_ics_sp0_pn_cell_dot_pointwise_target. ff_code_dot_mcp_ics_sp0_pn_cell_dot = ff_q_fpmp_dot_mcp_ics_sp0_pn_cell_dot_pointwise_target * S ((S (fpmp_index_dot_mcp_ics_sp0_pn_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_sp0_pn_cell_dot) + (fpmp_target_dot_mcp_ics_sp0_pn_cell_dot_pointwise))) -> fpmp_target_dot_mcp_ics_sp0_pn_cell_dot_pointwise = fpmp_left_dot_mcp_ics_sp0_pn_cell_dot_pointwise * fpmp_right_dot_mcp_ics_sp0_pn_cell_dot_pointwise) /\ (exists ff_u_dot_mcp_ics_sp0_pn_cell_dot_sum ff_v_dot_mcp_ics_sp0_pn_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_sp0_pn_cell_dot_sum_start. ff_h_dot_mcp_ics_sp0_pn_cell_dot_sum_start + S (0) = S ((S (0)) * ff_v_dot_mcp_ics_sp0_pn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_sp0_pn_cell_dot_sum_start. ff_u_dot_mcp_ics_sp0_pn_cell_dot_sum = ff_q_dot_mcp_ics_sp0_pn_cell_dot_sum_start * S ((S (0)) * ff_v_dot_mcp_ics_sp0_pn_cell_dot_sum) + (0))) /\ ((((exists ff_h_dot_mcp_ics_sp0_pn_cell_dot_sum_terminal. ff_h_dot_mcp_ics_sp0_pn_cell_dot_sum_terminal + S (ff_value_mcp_prefix_ics_sp0_pn) = S ((S (w)) * ff_v_dot_mcp_ics_sp0_pn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_sp0_pn_cell_dot_sum_terminal. ff_u_dot_mcp_ics_sp0_pn_cell_dot_sum = ff_q_dot_mcp_ics_sp0_pn_cell_dot_sum_terminal * S ((S (w)) * ff_v_dot_mcp_ics_sp0_pn_cell_dot_sum) + (ff_value_mcp_prefix_ics_sp0_pn))) /\ forall ff_i_dot_mcp_ics_sp0_pn_cell_dot_sum. (exists ff_lt_dot_mcp_ics_sp0_pn_cell_dot_sum_bound. ff_lt_dot_mcp_ics_sp0_pn_cell_dot_sum_bound + S ff_i_dot_mcp_ics_sp0_pn_cell_dot_sum = w) -> exists ff_a_dot_mcp_ics_sp0_pn_cell_dot_sum ff_r_dot_mcp_ics_sp0_pn_cell_dot_sum ff_s_dot_mcp_ics_sp0_pn_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_sp0_pn_cell_dot_sum_summand. ff_h_dot_mcp_ics_sp0_pn_cell_dot_sum_summand + S (ff_a_dot_mcp_ics_sp0_pn_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_sp0_pn_cell_dot_sum)) * ff_scale_dot_mcp_ics_sp0_pn_cell_dot)) /\ exists ff_q_dot_mcp_ics_sp0_pn_cell_dot_sum_summand. ff_code_dot_mcp_ics_sp0_pn_cell_dot = ff_q_dot_mcp_ics_sp0_pn_cell_dot_sum_summand * S ((S (ff_i_dot_mcp_ics_sp0_pn_cell_dot_sum)) * ff_scale_dot_mcp_ics_sp0_pn_cell_dot) + (ff_a_dot_mcp_ics_sp0_pn_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_sp0_pn_cell_dot_sum_partial. ff_h_dot_mcp_ics_sp0_pn_cell_dot_sum_partial + S (ff_r_dot_mcp_ics_sp0_pn_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_sp0_pn_cell_dot_sum)) * ff_v_dot_mcp_ics_sp0_pn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_sp0_pn_cell_dot_sum_partial. ff_u_dot_mcp_ics_sp0_pn_cell_dot_sum = ff_q_dot_mcp_ics_sp0_pn_cell_dot_sum_partial * S ((S (ff_i_dot_mcp_ics_sp0_pn_cell_dot_sum)) * ff_v_dot_mcp_ics_sp0_pn_cell_dot_sum) + (ff_r_dot_mcp_ics_sp0_pn_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_sp0_pn_cell_dot_sum_successor. ff_h_dot_mcp_ics_sp0_pn_cell_dot_sum_successor + S (ff_s_dot_mcp_ics_sp0_pn_cell_dot_sum) = S ((S (S ff_i_dot_mcp_ics_sp0_pn_cell_dot_sum)) * ff_v_dot_mcp_ics_sp0_pn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_sp0_pn_cell_dot_sum_successor. ff_u_dot_mcp_ics_sp0_pn_cell_dot_sum = ff_q_dot_mcp_ics_sp0_pn_cell_dot_sum_successor * S ((S (S ff_i_dot_mcp_ics_sp0_pn_cell_dot_sum)) * ff_v_dot_mcp_ics_sp0_pn_cell_dot_sum) + (ff_s_dot_mcp_ics_sp0_pn_cell_dot_sum))) /\ ff_s_dot_mcp_ics_sp0_pn_cell_dot_sum = ff_r_dot_mcp_ics_sp0_pn_cell_dot_sum + ff_a_dot_mcp_ics_sp0_pn_cell_dot_sum))))))))))) /\ (((exists fs_h_mcp_ics_sp0_pn_entry. fs_h_mcp_ics_sp0_pn_entry + S (ff_value_mcp_prefix_ics_sp0_pn) = S ((S (ff_index_mcp_prefix_ics_sp0_pn)) * ff_pns_mcp_smatrix_ics_sp0)) /\ exists fs_q_mcp_ics_sp0_pn_entry. ff_pn_mcp_smatrix_ics_sp0 = fs_q_mcp_ics_sp0_pn_entry * S ((S (ff_index_mcp_prefix_ics_sp0_pn)) * ff_pns_mcp_smatrix_ics_sp0) + (ff_value_mcp_prefix_ics_sp0_pn))))))) /\ ((forall ff_index_mcp_prefix_ics_sp0_np. (exists mcp_gap_ics_sp0_np_index. mcp_gap_ics_sp0_np_index + S (ff_index_mcp_prefix_ics_sp0_np) = ((r) * (1))) -> exists ff_row_mcp_prefix_ics_sp0_np ff_column_mcp_prefix_ics_sp0_np ff_value_mcp_prefix_ics_sp0_np. ((ff_index_mcp_prefix_ics_sp0_np) = (1) * ff_row_mcp_prefix_ics_sp0_np + ff_column_mcp_prefix_ics_sp0_np /\ ((exists mcp_gap_ics_sp0_np_column. mcp_gap_ics_sp0_np_column + S (ff_column_mcp_prefix_ics_sp0_np) = (1)) /\ ((exists ff_left_mcp_cell_ics_sp0_np_cell ff_left_scale_mcp_cell_ics_sp0_np_cell ff_right_mcp_cell_ics_sp0_np_cell ff_right_scale_mcp_cell_ics_sp0_np_cell. ((forall ff_index_mcp_ics_sp0_np_cell_row ff_source_mcp_ics_sp0_np_cell_row ff_target_mcp_ics_sp0_np_cell_row. (exists mcp_gap_ics_sp0_np_cell_row_bound. mcp_gap_ics_sp0_np_cell_row_bound + S (ff_index_mcp_ics_sp0_np_cell_row) = (w)) -> (((exists fs_h_mcp_ics_sp0_np_cell_row_source. fs_h_mcp_ics_sp0_np_cell_row_source + S (ff_source_mcp_ics_sp0_np_cell_row) = S ((S (((ff_row_mcp_prefix_ics_sp0_np) * (w)) + (1) * ff_index_mcp_ics_sp0_np_cell_row)) * dc)) /\ exists fs_q_mcp_ics_sp0_np_cell_row_source. db = fs_q_mcp_ics_sp0_np_cell_row_source * S ((S (((ff_row_mcp_prefix_ics_sp0_np) * (w)) + (1) * ff_index_mcp_ics_sp0_np_cell_row)) * dc) + (ff_source_mcp_ics_sp0_np_cell_row))) -> (((exists fs_h_mcp_ics_sp0_np_cell_row_target. fs_h_mcp_ics_sp0_np_cell_row_target + S (ff_target_mcp_ics_sp0_np_cell_row) = S ((S (ff_index_mcp_ics_sp0_np_cell_row)) * ff_left_scale_mcp_cell_ics_sp0_np_cell)) /\ exists fs_q_mcp_ics_sp0_np_cell_row_target. ff_left_mcp_cell_ics_sp0_np_cell = fs_q_mcp_ics_sp0_np_cell_row_target * S ((S (ff_index_mcp_ics_sp0_np_cell_row)) * ff_left_scale_mcp_cell_ics_sp0_np_cell) + (ff_target_mcp_ics_sp0_np_cell_row))) -> ff_target_mcp_ics_sp0_np_cell_row = ff_source_mcp_ics_sp0_np_cell_row) /\ ((forall ff_index_mcp_ics_sp0_np_cell_column ff_source_mcp_ics_sp0_np_cell_column ff_target_mcp_ics_sp0_np_cell_column. (exists mcp_gap_ics_sp0_np_cell_column_bound. mcp_gap_ics_sp0_np_cell_column_bound + S (ff_index_mcp_ics_sp0_np_cell_column) = (w)) -> (((exists fs_h_mcp_ics_sp0_np_cell_column_source. fs_h_mcp_ics_sp0_np_cell_column_source + S (ff_source_mcp_ics_sp0_np_cell_column) = S ((S ((ff_column_mcp_prefix_ics_sp0_np) + (1) * ff_index_mcp_ics_sp0_np_cell_column)) * ec)) /\ exists fs_q_mcp_ics_sp0_np_cell_column_source. eb = fs_q_mcp_ics_sp0_np_cell_column_source * S ((S ((ff_column_mcp_prefix_ics_sp0_np) + (1) * ff_index_mcp_ics_sp0_np_cell_column)) * ec) + (ff_source_mcp_ics_sp0_np_cell_column))) -> (((exists fs_h_mcp_ics_sp0_np_cell_column_target. fs_h_mcp_ics_sp0_np_cell_column_target + S (ff_target_mcp_ics_sp0_np_cell_column) = S ((S (ff_index_mcp_ics_sp0_np_cell_column)) * ff_right_scale_mcp_cell_ics_sp0_np_cell)) /\ exists fs_q_mcp_ics_sp0_np_cell_column_target. ff_right_mcp_cell_ics_sp0_np_cell = fs_q_mcp_ics_sp0_np_cell_column_target * S ((S (ff_index_mcp_ics_sp0_np_cell_column)) * ff_right_scale_mcp_cell_ics_sp0_np_cell) + (ff_target_mcp_ics_sp0_np_cell_column))) -> ff_target_mcp_ics_sp0_np_cell_column = ff_source_mcp_ics_sp0_np_cell_column) /\ (exists ff_code_dot_mcp_ics_sp0_np_cell_dot ff_scale_dot_mcp_ics_sp0_np_cell_dot. ((forall fpmp_index_dot_mcp_ics_sp0_np_cell_dot_pointwise fpmp_left_dot_mcp_ics_sp0_np_cell_dot_pointwise fpmp_right_dot_mcp_ics_sp0_np_cell_dot_pointwise fpmp_target_dot_mcp_ics_sp0_np_cell_dot_pointwise. (exists fpmp_gap_dot_mcp_ics_sp0_np_cell_dot_pointwise. fpmp_gap_dot_mcp_ics_sp0_np_cell_dot_pointwise + S fpmp_index_dot_mcp_ics_sp0_np_cell_dot_pointwise = w) -> (((exists ff_h_fpmp_dot_mcp_ics_sp0_np_cell_dot_pointwise_left. ff_h_fpmp_dot_mcp_ics_sp0_np_cell_dot_pointwise_left + S (fpmp_left_dot_mcp_ics_sp0_np_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_sp0_np_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_sp0_np_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_sp0_np_cell_dot_pointwise_left. ff_left_mcp_cell_ics_sp0_np_cell = ff_q_fpmp_dot_mcp_ics_sp0_np_cell_dot_pointwise_left * S ((S (fpmp_index_dot_mcp_ics_sp0_np_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_sp0_np_cell) + (fpmp_left_dot_mcp_ics_sp0_np_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_sp0_np_cell_dot_pointwise_right. ff_h_fpmp_dot_mcp_ics_sp0_np_cell_dot_pointwise_right + S (fpmp_right_dot_mcp_ics_sp0_np_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_sp0_np_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_sp0_np_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_sp0_np_cell_dot_pointwise_right. ff_right_mcp_cell_ics_sp0_np_cell = ff_q_fpmp_dot_mcp_ics_sp0_np_cell_dot_pointwise_right * S ((S (fpmp_index_dot_mcp_ics_sp0_np_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_sp0_np_cell) + (fpmp_right_dot_mcp_ics_sp0_np_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_sp0_np_cell_dot_pointwise_target. ff_h_fpmp_dot_mcp_ics_sp0_np_cell_dot_pointwise_target + S (fpmp_target_dot_mcp_ics_sp0_np_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_sp0_np_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_sp0_np_cell_dot)) /\ exists ff_q_fpmp_dot_mcp_ics_sp0_np_cell_dot_pointwise_target. ff_code_dot_mcp_ics_sp0_np_cell_dot = ff_q_fpmp_dot_mcp_ics_sp0_np_cell_dot_pointwise_target * S ((S (fpmp_index_dot_mcp_ics_sp0_np_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_sp0_np_cell_dot) + (fpmp_target_dot_mcp_ics_sp0_np_cell_dot_pointwise))) -> fpmp_target_dot_mcp_ics_sp0_np_cell_dot_pointwise = fpmp_left_dot_mcp_ics_sp0_np_cell_dot_pointwise * fpmp_right_dot_mcp_ics_sp0_np_cell_dot_pointwise) /\ (exists ff_u_dot_mcp_ics_sp0_np_cell_dot_sum ff_v_dot_mcp_ics_sp0_np_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_sp0_np_cell_dot_sum_start. ff_h_dot_mcp_ics_sp0_np_cell_dot_sum_start + S (0) = S ((S (0)) * ff_v_dot_mcp_ics_sp0_np_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_sp0_np_cell_dot_sum_start. ff_u_dot_mcp_ics_sp0_np_cell_dot_sum = ff_q_dot_mcp_ics_sp0_np_cell_dot_sum_start * S ((S (0)) * ff_v_dot_mcp_ics_sp0_np_cell_dot_sum) + (0))) /\ ((((exists ff_h_dot_mcp_ics_sp0_np_cell_dot_sum_terminal. ff_h_dot_mcp_ics_sp0_np_cell_dot_sum_terminal + S (ff_value_mcp_prefix_ics_sp0_np) = S ((S (w)) * ff_v_dot_mcp_ics_sp0_np_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_sp0_np_cell_dot_sum_terminal. ff_u_dot_mcp_ics_sp0_np_cell_dot_sum = ff_q_dot_mcp_ics_sp0_np_cell_dot_sum_terminal * S ((S (w)) * ff_v_dot_mcp_ics_sp0_np_cell_dot_sum) + (ff_value_mcp_prefix_ics_sp0_np))) /\ forall ff_i_dot_mcp_ics_sp0_np_cell_dot_sum. (exists ff_lt_dot_mcp_ics_sp0_np_cell_dot_sum_bound. ff_lt_dot_mcp_ics_sp0_np_cell_dot_sum_bound + S ff_i_dot_mcp_ics_sp0_np_cell_dot_sum = w) -> exists ff_a_dot_mcp_ics_sp0_np_cell_dot_sum ff_r_dot_mcp_ics_sp0_np_cell_dot_sum ff_s_dot_mcp_ics_sp0_np_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_sp0_np_cell_dot_sum_summand. ff_h_dot_mcp_ics_sp0_np_cell_dot_sum_summand + S (ff_a_dot_mcp_ics_sp0_np_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_sp0_np_cell_dot_sum)) * ff_scale_dot_mcp_ics_sp0_np_cell_dot)) /\ exists ff_q_dot_mcp_ics_sp0_np_cell_dot_sum_summand. ff_code_dot_mcp_ics_sp0_np_cell_dot = ff_q_dot_mcp_ics_sp0_np_cell_dot_sum_summand * S ((S (ff_i_dot_mcp_ics_sp0_np_cell_dot_sum)) * ff_scale_dot_mcp_ics_sp0_np_cell_dot) + (ff_a_dot_mcp_ics_sp0_np_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_sp0_np_cell_dot_sum_partial. ff_h_dot_mcp_ics_sp0_np_cell_dot_sum_partial + S (ff_r_dot_mcp_ics_sp0_np_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_sp0_np_cell_dot_sum)) * ff_v_dot_mcp_ics_sp0_np_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_sp0_np_cell_dot_sum_partial. ff_u_dot_mcp_ics_sp0_np_cell_dot_sum = ff_q_dot_mcp_ics_sp0_np_cell_dot_sum_partial * S ((S (ff_i_dot_mcp_ics_sp0_np_cell_dot_sum)) * ff_v_dot_mcp_ics_sp0_np_cell_dot_sum) + (ff_r_dot_mcp_ics_sp0_np_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_sp0_np_cell_dot_sum_successor. ff_h_dot_mcp_ics_sp0_np_cell_dot_sum_successor + S (ff_s_dot_mcp_ics_sp0_np_cell_dot_sum) = S ((S (S ff_i_dot_mcp_ics_sp0_np_cell_dot_sum)) * ff_v_dot_mcp_ics_sp0_np_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_sp0_np_cell_dot_sum_successor. ff_u_dot_mcp_ics_sp0_np_cell_dot_sum = ff_q_dot_mcp_ics_sp0_np_cell_dot_sum_successor * S ((S (S ff_i_dot_mcp_ics_sp0_np_cell_dot_sum)) * ff_v_dot_mcp_ics_sp0_np_cell_dot_sum) + (ff_s_dot_mcp_ics_sp0_np_cell_dot_sum))) /\ ff_s_dot_mcp_ics_sp0_np_cell_dot_sum = ff_r_dot_mcp_ics_sp0_np_cell_dot_sum + ff_a_dot_mcp_ics_sp0_np_cell_dot_sum))))))))))) /\ (((exists fs_h_mcp_ics_sp0_np_entry. fs_h_mcp_ics_sp0_np_entry + S (ff_value_mcp_prefix_ics_sp0_np) = S ((S (ff_index_mcp_prefix_ics_sp0_np)) * ff_nps_mcp_smatrix_ics_sp0)) /\ exists fs_q_mcp_ics_sp0_np_entry. ff_np_mcp_smatrix_ics_sp0 = fs_q_mcp_ics_sp0_np_entry * S ((S (ff_index_mcp_prefix_ics_sp0_np)) * ff_nps_mcp_smatrix_ics_sp0) + (ff_value_mcp_prefix_ics_sp0_np))))))) /\ ((forall ff_index_mcp_add_ics_sp0_positive ff_left_mcp_add_ics_sp0_positive ff_right_mcp_add_ics_sp0_positive ff_target_mcp_add_ics_sp0_positive. (exists mcp_gap_ics_sp0_positive_bound. mcp_gap_ics_sp0_positive_bound + S (ff_index_mcp_add_ics_sp0_positive) = ((r) * (1))) -> (((exists fs_h_mcp_ics_sp0_positive_left. fs_h_mcp_ics_sp0_positive_left + S (ff_left_mcp_add_ics_sp0_positive) = S ((S (ff_index_mcp_add_ics_sp0_positive)) * ff_pps_mcp_smatrix_ics_sp0)) /\ exists fs_q_mcp_ics_sp0_positive_left. ff_pp_mcp_smatrix_ics_sp0 = fs_q_mcp_ics_sp0_positive_left * S ((S (ff_index_mcp_add_ics_sp0_positive)) * ff_pps_mcp_smatrix_ics_sp0) + (ff_left_mcp_add_ics_sp0_positive))) -> (((exists fs_h_mcp_ics_sp0_positive_right. fs_h_mcp_ics_sp0_positive_right + S (ff_right_mcp_add_ics_sp0_positive) = S ((S (ff_index_mcp_add_ics_sp0_positive)) * ff_nns_mcp_smatrix_ics_sp0)) /\ exists fs_q_mcp_ics_sp0_positive_right. ff_nn_mcp_smatrix_ics_sp0 = fs_q_mcp_ics_sp0_positive_right * S ((S (ff_index_mcp_add_ics_sp0_positive)) * ff_nns_mcp_smatrix_ics_sp0) + (ff_right_mcp_add_ics_sp0_positive))) -> (((exists fs_h_mcp_ics_sp0_positive_target. fs_h_mcp_ics_sp0_positive_target + S (ff_target_mcp_add_ics_sp0_positive) = S ((S (ff_index_mcp_add_ics_sp0_positive)) * pc)) /\ exists fs_q_mcp_ics_sp0_positive_target. pb = fs_q_mcp_ics_sp0_positive_target * S ((S (ff_index_mcp_add_ics_sp0_positive)) * pc) + (ff_target_mcp_add_ics_sp0_positive))) -> ff_target_mcp_add_ics_sp0_positive = ff_left_mcp_add_ics_sp0_positive + ff_right_mcp_add_ics_sp0_positive) /\ (forall ff_index_mcp_add_ics_sp0_negative ff_left_mcp_add_ics_sp0_negative ff_right_mcp_add_ics_sp0_negative ff_target_mcp_add_ics_sp0_negative. (exists mcp_gap_ics_sp0_negative_bound. mcp_gap_ics_sp0_negative_bound + S (ff_index_mcp_add_ics_sp0_negative) = ((r) * (1))) -> (((exists fs_h_mcp_ics_sp0_negative_left. fs_h_mcp_ics_sp0_negative_left + S (ff_left_mcp_add_ics_sp0_negative) = S ((S (ff_index_mcp_add_ics_sp0_negative)) * ff_pns_mcp_smatrix_ics_sp0)) /\ exists fs_q_mcp_ics_sp0_negative_left. ff_pn_mcp_smatrix_ics_sp0 = fs_q_mcp_ics_sp0_negative_left * S ((S (ff_index_mcp_add_ics_sp0_negative)) * ff_pns_mcp_smatrix_ics_sp0) + (ff_left_mcp_add_ics_sp0_negative))) -> (((exists fs_h_mcp_ics_sp0_negative_right. fs_h_mcp_ics_sp0_negative_right + S (ff_right_mcp_add_ics_sp0_negative) = S ((S (ff_index_mcp_add_ics_sp0_negative)) * ff_nps_mcp_smatrix_ics_sp0)) /\ exists fs_q_mcp_ics_sp0_negative_right. ff_np_mcp_smatrix_ics_sp0 = fs_q_mcp_ics_sp0_negative_right * S ((S (ff_index_mcp_add_ics_sp0_negative)) * ff_nps_mcp_smatrix_ics_sp0) + (ff_right_mcp_add_ics_sp0_negative))) -> (((exists fs_h_mcp_ics_sp0_negative_target. fs_h_mcp_ics_sp0_negative_target + S (ff_target_mcp_add_ics_sp0_negative) = S ((S (ff_index_mcp_add_ics_sp0_negative)) * nc)) /\ exists fs_q_mcp_ics_sp0_negative_target. nb = fs_q_mcp_ics_sp0_negative_target * S ((S (ff_index_mcp_add_ics_sp0_negative)) * nc) + (ff_target_mcp_add_ics_sp0_negative))) -> ff_target_mcp_add_ics_sp0_negative = ff_left_mcp_add_ics_sp0_negative + ff_right_mcp_add_ics_sp0_negative))))))) -> (exists ff_pp_mcp_smatrix_ics_sp1 ff_pps_mcp_smatrix_ics_sp1 ff_nn_mcp_smatrix_ics_sp1 ff_nns_mcp_smatrix_ics_sp1 ff_pn_mcp_smatrix_ics_sp1 ff_pns_mcp_smatrix_ics_sp1 ff_np_mcp_smatrix_ics_sp1 ff_nps_mcp_smatrix_ics_sp1. ((forall ff_index_mcp_prefix_ics_sp1_pp. (exists mcp_gap_ics_sp1_pp_index. mcp_gap_ics_sp1_pp_index + S (ff_index_mcp_prefix_ics_sp1_pp) = ((r) * (1))) -> exists ff_row_mcp_prefix_ics_sp1_pp ff_column_mcp_prefix_ics_sp1_pp ff_value_mcp_prefix_ics_sp1_pp. ((ff_index_mcp_prefix_ics_sp1_pp) = (1) * ff_row_mcp_prefix_ics_sp1_pp + ff_column_mcp_prefix_ics_sp1_pp /\ ((exists mcp_gap_ics_sp1_pp_column. mcp_gap_ics_sp1_pp_column + S (ff_column_mcp_prefix_ics_sp1_pp) = (1)) /\ ((exists ff_left_mcp_cell_ics_sp1_pp_cell ff_left_scale_mcp_cell_ics_sp1_pp_cell ff_right_mcp_cell_ics_sp1_pp_cell ff_right_scale_mcp_cell_ics_sp1_pp_cell. ((forall ff_index_mcp_ics_sp1_pp_cell_row ff_source_mcp_ics_sp1_pp_cell_row ff_target_mcp_ics_sp1_pp_cell_row. (exists mcp_gap_ics_sp1_pp_cell_row_bound. mcp_gap_ics_sp1_pp_cell_row_bound + S (ff_index_mcp_ics_sp1_pp_cell_row) = (w)) -> (((exists fs_h_mcp_ics_sp1_pp_cell_row_source. fs_h_mcp_ics_sp1_pp_cell_row_source + S (ff_source_mcp_ics_sp1_pp_cell_row) = S ((S (((ff_row_mcp_prefix_ics_sp1_pp) * (w)) + (1) * ff_index_mcp_ics_sp1_pp_cell_row)) * ac)) /\ exists fs_q_mcp_ics_sp1_pp_cell_row_source. ab = fs_q_mcp_ics_sp1_pp_cell_row_source * S ((S (((ff_row_mcp_prefix_ics_sp1_pp) * (w)) + (1) * ff_index_mcp_ics_sp1_pp_cell_row)) * ac) + (ff_source_mcp_ics_sp1_pp_cell_row))) -> (((exists fs_h_mcp_ics_sp1_pp_cell_row_target. fs_h_mcp_ics_sp1_pp_cell_row_target + S (ff_target_mcp_ics_sp1_pp_cell_row) = S ((S (ff_index_mcp_ics_sp1_pp_cell_row)) * ff_left_scale_mcp_cell_ics_sp1_pp_cell)) /\ exists fs_q_mcp_ics_sp1_pp_cell_row_target. ff_left_mcp_cell_ics_sp1_pp_cell = fs_q_mcp_ics_sp1_pp_cell_row_target * S ((S (ff_index_mcp_ics_sp1_pp_cell_row)) * ff_left_scale_mcp_cell_ics_sp1_pp_cell) + (ff_target_mcp_ics_sp1_pp_cell_row))) -> ff_target_mcp_ics_sp1_pp_cell_row = ff_source_mcp_ics_sp1_pp_cell_row) /\ ((forall ff_index_mcp_ics_sp1_pp_cell_column ff_source_mcp_ics_sp1_pp_cell_column ff_target_mcp_ics_sp1_pp_cell_column. (exists mcp_gap_ics_sp1_pp_cell_column_bound. mcp_gap_ics_sp1_pp_cell_column_bound + S (ff_index_mcp_ics_sp1_pp_cell_column) = (w)) -> (((exists fs_h_mcp_ics_sp1_pp_cell_column_source. fs_h_mcp_ics_sp1_pp_cell_column_source + S (ff_source_mcp_ics_sp1_pp_cell_column) = S ((S ((ff_column_mcp_prefix_ics_sp1_pp) + (1) * ff_index_mcp_ics_sp1_pp_cell_column)) * gc)) /\ exists fs_q_mcp_ics_sp1_pp_cell_column_source. gb = fs_q_mcp_ics_sp1_pp_cell_column_source * S ((S ((ff_column_mcp_prefix_ics_sp1_pp) + (1) * ff_index_mcp_ics_sp1_pp_cell_column)) * gc) + (ff_source_mcp_ics_sp1_pp_cell_column))) -> (((exists fs_h_mcp_ics_sp1_pp_cell_column_target. fs_h_mcp_ics_sp1_pp_cell_column_target + S (ff_target_mcp_ics_sp1_pp_cell_column) = S ((S (ff_index_mcp_ics_sp1_pp_cell_column)) * ff_right_scale_mcp_cell_ics_sp1_pp_cell)) /\ exists fs_q_mcp_ics_sp1_pp_cell_column_target. ff_right_mcp_cell_ics_sp1_pp_cell = fs_q_mcp_ics_sp1_pp_cell_column_target * S ((S (ff_index_mcp_ics_sp1_pp_cell_column)) * ff_right_scale_mcp_cell_ics_sp1_pp_cell) + (ff_target_mcp_ics_sp1_pp_cell_column))) -> ff_target_mcp_ics_sp1_pp_cell_column = ff_source_mcp_ics_sp1_pp_cell_column) /\ (exists ff_code_dot_mcp_ics_sp1_pp_cell_dot ff_scale_dot_mcp_ics_sp1_pp_cell_dot. ((forall fpmp_index_dot_mcp_ics_sp1_pp_cell_dot_pointwise fpmp_left_dot_mcp_ics_sp1_pp_cell_dot_pointwise fpmp_right_dot_mcp_ics_sp1_pp_cell_dot_pointwise fpmp_target_dot_mcp_ics_sp1_pp_cell_dot_pointwise. (exists fpmp_gap_dot_mcp_ics_sp1_pp_cell_dot_pointwise. fpmp_gap_dot_mcp_ics_sp1_pp_cell_dot_pointwise + S fpmp_index_dot_mcp_ics_sp1_pp_cell_dot_pointwise = w) -> (((exists ff_h_fpmp_dot_mcp_ics_sp1_pp_cell_dot_pointwise_left. ff_h_fpmp_dot_mcp_ics_sp1_pp_cell_dot_pointwise_left + S (fpmp_left_dot_mcp_ics_sp1_pp_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_sp1_pp_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_sp1_pp_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_sp1_pp_cell_dot_pointwise_left. ff_left_mcp_cell_ics_sp1_pp_cell = ff_q_fpmp_dot_mcp_ics_sp1_pp_cell_dot_pointwise_left * S ((S (fpmp_index_dot_mcp_ics_sp1_pp_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_sp1_pp_cell) + (fpmp_left_dot_mcp_ics_sp1_pp_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_sp1_pp_cell_dot_pointwise_right. ff_h_fpmp_dot_mcp_ics_sp1_pp_cell_dot_pointwise_right + S (fpmp_right_dot_mcp_ics_sp1_pp_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_sp1_pp_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_sp1_pp_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_sp1_pp_cell_dot_pointwise_right. ff_right_mcp_cell_ics_sp1_pp_cell = ff_q_fpmp_dot_mcp_ics_sp1_pp_cell_dot_pointwise_right * S ((S (fpmp_index_dot_mcp_ics_sp1_pp_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_sp1_pp_cell) + (fpmp_right_dot_mcp_ics_sp1_pp_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_sp1_pp_cell_dot_pointwise_target. ff_h_fpmp_dot_mcp_ics_sp1_pp_cell_dot_pointwise_target + S (fpmp_target_dot_mcp_ics_sp1_pp_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_sp1_pp_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_sp1_pp_cell_dot)) /\ exists ff_q_fpmp_dot_mcp_ics_sp1_pp_cell_dot_pointwise_target. ff_code_dot_mcp_ics_sp1_pp_cell_dot = ff_q_fpmp_dot_mcp_ics_sp1_pp_cell_dot_pointwise_target * S ((S (fpmp_index_dot_mcp_ics_sp1_pp_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_sp1_pp_cell_dot) + (fpmp_target_dot_mcp_ics_sp1_pp_cell_dot_pointwise))) -> fpmp_target_dot_mcp_ics_sp1_pp_cell_dot_pointwise = fpmp_left_dot_mcp_ics_sp1_pp_cell_dot_pointwise * fpmp_right_dot_mcp_ics_sp1_pp_cell_dot_pointwise) /\ (exists ff_u_dot_mcp_ics_sp1_pp_cell_dot_sum ff_v_dot_mcp_ics_sp1_pp_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_sp1_pp_cell_dot_sum_start. ff_h_dot_mcp_ics_sp1_pp_cell_dot_sum_start + S (0) = S ((S (0)) * ff_v_dot_mcp_ics_sp1_pp_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_sp1_pp_cell_dot_sum_start. ff_u_dot_mcp_ics_sp1_pp_cell_dot_sum = ff_q_dot_mcp_ics_sp1_pp_cell_dot_sum_start * S ((S (0)) * ff_v_dot_mcp_ics_sp1_pp_cell_dot_sum) + (0))) /\ ((((exists ff_h_dot_mcp_ics_sp1_pp_cell_dot_sum_terminal. ff_h_dot_mcp_ics_sp1_pp_cell_dot_sum_terminal + S (ff_value_mcp_prefix_ics_sp1_pp) = S ((S (w)) * ff_v_dot_mcp_ics_sp1_pp_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_sp1_pp_cell_dot_sum_terminal. ff_u_dot_mcp_ics_sp1_pp_cell_dot_sum = ff_q_dot_mcp_ics_sp1_pp_cell_dot_sum_terminal * S ((S (w)) * ff_v_dot_mcp_ics_sp1_pp_cell_dot_sum) + (ff_value_mcp_prefix_ics_sp1_pp))) /\ forall ff_i_dot_mcp_ics_sp1_pp_cell_dot_sum. (exists ff_lt_dot_mcp_ics_sp1_pp_cell_dot_sum_bound. ff_lt_dot_mcp_ics_sp1_pp_cell_dot_sum_bound + S ff_i_dot_mcp_ics_sp1_pp_cell_dot_sum = w) -> exists ff_a_dot_mcp_ics_sp1_pp_cell_dot_sum ff_r_dot_mcp_ics_sp1_pp_cell_dot_sum ff_s_dot_mcp_ics_sp1_pp_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_sp1_pp_cell_dot_sum_summand. ff_h_dot_mcp_ics_sp1_pp_cell_dot_sum_summand + S (ff_a_dot_mcp_ics_sp1_pp_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_sp1_pp_cell_dot_sum)) * ff_scale_dot_mcp_ics_sp1_pp_cell_dot)) /\ exists ff_q_dot_mcp_ics_sp1_pp_cell_dot_sum_summand. ff_code_dot_mcp_ics_sp1_pp_cell_dot = ff_q_dot_mcp_ics_sp1_pp_cell_dot_sum_summand * S ((S (ff_i_dot_mcp_ics_sp1_pp_cell_dot_sum)) * ff_scale_dot_mcp_ics_sp1_pp_cell_dot) + (ff_a_dot_mcp_ics_sp1_pp_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_sp1_pp_cell_dot_sum_partial. ff_h_dot_mcp_ics_sp1_pp_cell_dot_sum_partial + S (ff_r_dot_mcp_ics_sp1_pp_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_sp1_pp_cell_dot_sum)) * ff_v_dot_mcp_ics_sp1_pp_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_sp1_pp_cell_dot_sum_partial. ff_u_dot_mcp_ics_sp1_pp_cell_dot_sum = ff_q_dot_mcp_ics_sp1_pp_cell_dot_sum_partial * S ((S (ff_i_dot_mcp_ics_sp1_pp_cell_dot_sum)) * ff_v_dot_mcp_ics_sp1_pp_cell_dot_sum) + (ff_r_dot_mcp_ics_sp1_pp_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_sp1_pp_cell_dot_sum_successor. ff_h_dot_mcp_ics_sp1_pp_cell_dot_sum_successor + S (ff_s_dot_mcp_ics_sp1_pp_cell_dot_sum) = S ((S (S ff_i_dot_mcp_ics_sp1_pp_cell_dot_sum)) * ff_v_dot_mcp_ics_sp1_pp_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_sp1_pp_cell_dot_sum_successor. ff_u_dot_mcp_ics_sp1_pp_cell_dot_sum = ff_q_dot_mcp_ics_sp1_pp_cell_dot_sum_successor * S ((S (S ff_i_dot_mcp_ics_sp1_pp_cell_dot_sum)) * ff_v_dot_mcp_ics_sp1_pp_cell_dot_sum) + (ff_s_dot_mcp_ics_sp1_pp_cell_dot_sum))) /\ ff_s_dot_mcp_ics_sp1_pp_cell_dot_sum = ff_r_dot_mcp_ics_sp1_pp_cell_dot_sum + ff_a_dot_mcp_ics_sp1_pp_cell_dot_sum))))))))))) /\ (((exists fs_h_mcp_ics_sp1_pp_entry. fs_h_mcp_ics_sp1_pp_entry + S (ff_value_mcp_prefix_ics_sp1_pp) = S ((S (ff_index_mcp_prefix_ics_sp1_pp)) * ff_pps_mcp_smatrix_ics_sp1)) /\ exists fs_q_mcp_ics_sp1_pp_entry. ff_pp_mcp_smatrix_ics_sp1 = fs_q_mcp_ics_sp1_pp_entry * S ((S (ff_index_mcp_prefix_ics_sp1_pp)) * ff_pps_mcp_smatrix_ics_sp1) + (ff_value_mcp_prefix_ics_sp1_pp))))))) /\ ((forall ff_index_mcp_prefix_ics_sp1_nn. (exists mcp_gap_ics_sp1_nn_index. mcp_gap_ics_sp1_nn_index + S (ff_index_mcp_prefix_ics_sp1_nn) = ((r) * (1))) -> exists ff_row_mcp_prefix_ics_sp1_nn ff_column_mcp_prefix_ics_sp1_nn ff_value_mcp_prefix_ics_sp1_nn. ((ff_index_mcp_prefix_ics_sp1_nn) = (1) * ff_row_mcp_prefix_ics_sp1_nn + ff_column_mcp_prefix_ics_sp1_nn /\ ((exists mcp_gap_ics_sp1_nn_column. mcp_gap_ics_sp1_nn_column + S (ff_column_mcp_prefix_ics_sp1_nn) = (1)) /\ ((exists ff_left_mcp_cell_ics_sp1_nn_cell ff_left_scale_mcp_cell_ics_sp1_nn_cell ff_right_mcp_cell_ics_sp1_nn_cell ff_right_scale_mcp_cell_ics_sp1_nn_cell. ((forall ff_index_mcp_ics_sp1_nn_cell_row ff_source_mcp_ics_sp1_nn_cell_row ff_target_mcp_ics_sp1_nn_cell_row. (exists mcp_gap_ics_sp1_nn_cell_row_bound. mcp_gap_ics_sp1_nn_cell_row_bound + S (ff_index_mcp_ics_sp1_nn_cell_row) = (w)) -> (((exists fs_h_mcp_ics_sp1_nn_cell_row_source. fs_h_mcp_ics_sp1_nn_cell_row_source + S (ff_source_mcp_ics_sp1_nn_cell_row) = S ((S (((ff_row_mcp_prefix_ics_sp1_nn) * (w)) + (1) * ff_index_mcp_ics_sp1_nn_cell_row)) * dc)) /\ exists fs_q_mcp_ics_sp1_nn_cell_row_source. db = fs_q_mcp_ics_sp1_nn_cell_row_source * S ((S (((ff_row_mcp_prefix_ics_sp1_nn) * (w)) + (1) * ff_index_mcp_ics_sp1_nn_cell_row)) * dc) + (ff_source_mcp_ics_sp1_nn_cell_row))) -> (((exists fs_h_mcp_ics_sp1_nn_cell_row_target. fs_h_mcp_ics_sp1_nn_cell_row_target + S (ff_target_mcp_ics_sp1_nn_cell_row) = S ((S (ff_index_mcp_ics_sp1_nn_cell_row)) * ff_left_scale_mcp_cell_ics_sp1_nn_cell)) /\ exists fs_q_mcp_ics_sp1_nn_cell_row_target. ff_left_mcp_cell_ics_sp1_nn_cell = fs_q_mcp_ics_sp1_nn_cell_row_target * S ((S (ff_index_mcp_ics_sp1_nn_cell_row)) * ff_left_scale_mcp_cell_ics_sp1_nn_cell) + (ff_target_mcp_ics_sp1_nn_cell_row))) -> ff_target_mcp_ics_sp1_nn_cell_row = ff_source_mcp_ics_sp1_nn_cell_row) /\ ((forall ff_index_mcp_ics_sp1_nn_cell_column ff_source_mcp_ics_sp1_nn_cell_column ff_target_mcp_ics_sp1_nn_cell_column. (exists mcp_gap_ics_sp1_nn_cell_column_bound. mcp_gap_ics_sp1_nn_cell_column_bound + S (ff_index_mcp_ics_sp1_nn_cell_column) = (w)) -> (((exists fs_h_mcp_ics_sp1_nn_cell_column_source. fs_h_mcp_ics_sp1_nn_cell_column_source + S (ff_source_mcp_ics_sp1_nn_cell_column) = S ((S ((ff_column_mcp_prefix_ics_sp1_nn) + (1) * ff_index_mcp_ics_sp1_nn_cell_column)) * hc)) /\ exists fs_q_mcp_ics_sp1_nn_cell_column_source. hb = fs_q_mcp_ics_sp1_nn_cell_column_source * S ((S ((ff_column_mcp_prefix_ics_sp1_nn) + (1) * ff_index_mcp_ics_sp1_nn_cell_column)) * hc) + (ff_source_mcp_ics_sp1_nn_cell_column))) -> (((exists fs_h_mcp_ics_sp1_nn_cell_column_target. fs_h_mcp_ics_sp1_nn_cell_column_target + S (ff_target_mcp_ics_sp1_nn_cell_column) = S ((S (ff_index_mcp_ics_sp1_nn_cell_column)) * ff_right_scale_mcp_cell_ics_sp1_nn_cell)) /\ exists fs_q_mcp_ics_sp1_nn_cell_column_target. ff_right_mcp_cell_ics_sp1_nn_cell = fs_q_mcp_ics_sp1_nn_cell_column_target * S ((S (ff_index_mcp_ics_sp1_nn_cell_column)) * ff_right_scale_mcp_cell_ics_sp1_nn_cell) + (ff_target_mcp_ics_sp1_nn_cell_column))) -> ff_target_mcp_ics_sp1_nn_cell_column = ff_source_mcp_ics_sp1_nn_cell_column) /\ (exists ff_code_dot_mcp_ics_sp1_nn_cell_dot ff_scale_dot_mcp_ics_sp1_nn_cell_dot. ((forall fpmp_index_dot_mcp_ics_sp1_nn_cell_dot_pointwise fpmp_left_dot_mcp_ics_sp1_nn_cell_dot_pointwise fpmp_right_dot_mcp_ics_sp1_nn_cell_dot_pointwise fpmp_target_dot_mcp_ics_sp1_nn_cell_dot_pointwise. (exists fpmp_gap_dot_mcp_ics_sp1_nn_cell_dot_pointwise. fpmp_gap_dot_mcp_ics_sp1_nn_cell_dot_pointwise + S fpmp_index_dot_mcp_ics_sp1_nn_cell_dot_pointwise = w) -> (((exists ff_h_fpmp_dot_mcp_ics_sp1_nn_cell_dot_pointwise_left. ff_h_fpmp_dot_mcp_ics_sp1_nn_cell_dot_pointwise_left + S (fpmp_left_dot_mcp_ics_sp1_nn_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_sp1_nn_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_sp1_nn_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_sp1_nn_cell_dot_pointwise_left. ff_left_mcp_cell_ics_sp1_nn_cell = ff_q_fpmp_dot_mcp_ics_sp1_nn_cell_dot_pointwise_left * S ((S (fpmp_index_dot_mcp_ics_sp1_nn_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_sp1_nn_cell) + (fpmp_left_dot_mcp_ics_sp1_nn_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_sp1_nn_cell_dot_pointwise_right. ff_h_fpmp_dot_mcp_ics_sp1_nn_cell_dot_pointwise_right + S (fpmp_right_dot_mcp_ics_sp1_nn_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_sp1_nn_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_sp1_nn_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_sp1_nn_cell_dot_pointwise_right. ff_right_mcp_cell_ics_sp1_nn_cell = ff_q_fpmp_dot_mcp_ics_sp1_nn_cell_dot_pointwise_right * S ((S (fpmp_index_dot_mcp_ics_sp1_nn_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_sp1_nn_cell) + (fpmp_right_dot_mcp_ics_sp1_nn_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_sp1_nn_cell_dot_pointwise_target. ff_h_fpmp_dot_mcp_ics_sp1_nn_cell_dot_pointwise_target + S (fpmp_target_dot_mcp_ics_sp1_nn_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_sp1_nn_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_sp1_nn_cell_dot)) /\ exists ff_q_fpmp_dot_mcp_ics_sp1_nn_cell_dot_pointwise_target. ff_code_dot_mcp_ics_sp1_nn_cell_dot = ff_q_fpmp_dot_mcp_ics_sp1_nn_cell_dot_pointwise_target * S ((S (fpmp_index_dot_mcp_ics_sp1_nn_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_sp1_nn_cell_dot) + (fpmp_target_dot_mcp_ics_sp1_nn_cell_dot_pointwise))) -> fpmp_target_dot_mcp_ics_sp1_nn_cell_dot_pointwise = fpmp_left_dot_mcp_ics_sp1_nn_cell_dot_pointwise * fpmp_right_dot_mcp_ics_sp1_nn_cell_dot_pointwise) /\ (exists ff_u_dot_mcp_ics_sp1_nn_cell_dot_sum ff_v_dot_mcp_ics_sp1_nn_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_sp1_nn_cell_dot_sum_start. ff_h_dot_mcp_ics_sp1_nn_cell_dot_sum_start + S (0) = S ((S (0)) * ff_v_dot_mcp_ics_sp1_nn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_sp1_nn_cell_dot_sum_start. ff_u_dot_mcp_ics_sp1_nn_cell_dot_sum = ff_q_dot_mcp_ics_sp1_nn_cell_dot_sum_start * S ((S (0)) * ff_v_dot_mcp_ics_sp1_nn_cell_dot_sum) + (0))) /\ ((((exists ff_h_dot_mcp_ics_sp1_nn_cell_dot_sum_terminal. ff_h_dot_mcp_ics_sp1_nn_cell_dot_sum_terminal + S (ff_value_mcp_prefix_ics_sp1_nn) = S ((S (w)) * ff_v_dot_mcp_ics_sp1_nn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_sp1_nn_cell_dot_sum_terminal. ff_u_dot_mcp_ics_sp1_nn_cell_dot_sum = ff_q_dot_mcp_ics_sp1_nn_cell_dot_sum_terminal * S ((S (w)) * ff_v_dot_mcp_ics_sp1_nn_cell_dot_sum) + (ff_value_mcp_prefix_ics_sp1_nn))) /\ forall ff_i_dot_mcp_ics_sp1_nn_cell_dot_sum. (exists ff_lt_dot_mcp_ics_sp1_nn_cell_dot_sum_bound. ff_lt_dot_mcp_ics_sp1_nn_cell_dot_sum_bound + S ff_i_dot_mcp_ics_sp1_nn_cell_dot_sum = w) -> exists ff_a_dot_mcp_ics_sp1_nn_cell_dot_sum ff_r_dot_mcp_ics_sp1_nn_cell_dot_sum ff_s_dot_mcp_ics_sp1_nn_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_sp1_nn_cell_dot_sum_summand. ff_h_dot_mcp_ics_sp1_nn_cell_dot_sum_summand + S (ff_a_dot_mcp_ics_sp1_nn_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_sp1_nn_cell_dot_sum)) * ff_scale_dot_mcp_ics_sp1_nn_cell_dot)) /\ exists ff_q_dot_mcp_ics_sp1_nn_cell_dot_sum_summand. ff_code_dot_mcp_ics_sp1_nn_cell_dot = ff_q_dot_mcp_ics_sp1_nn_cell_dot_sum_summand * S ((S (ff_i_dot_mcp_ics_sp1_nn_cell_dot_sum)) * ff_scale_dot_mcp_ics_sp1_nn_cell_dot) + (ff_a_dot_mcp_ics_sp1_nn_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_sp1_nn_cell_dot_sum_partial. ff_h_dot_mcp_ics_sp1_nn_cell_dot_sum_partial + S (ff_r_dot_mcp_ics_sp1_nn_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_sp1_nn_cell_dot_sum)) * ff_v_dot_mcp_ics_sp1_nn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_sp1_nn_cell_dot_sum_partial. ff_u_dot_mcp_ics_sp1_nn_cell_dot_sum = ff_q_dot_mcp_ics_sp1_nn_cell_dot_sum_partial * S ((S (ff_i_dot_mcp_ics_sp1_nn_cell_dot_sum)) * ff_v_dot_mcp_ics_sp1_nn_cell_dot_sum) + (ff_r_dot_mcp_ics_sp1_nn_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_sp1_nn_cell_dot_sum_successor. ff_h_dot_mcp_ics_sp1_nn_cell_dot_sum_successor + S (ff_s_dot_mcp_ics_sp1_nn_cell_dot_sum) = S ((S (S ff_i_dot_mcp_ics_sp1_nn_cell_dot_sum)) * ff_v_dot_mcp_ics_sp1_nn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_sp1_nn_cell_dot_sum_successor. ff_u_dot_mcp_ics_sp1_nn_cell_dot_sum = ff_q_dot_mcp_ics_sp1_nn_cell_dot_sum_successor * S ((S (S ff_i_dot_mcp_ics_sp1_nn_cell_dot_sum)) * ff_v_dot_mcp_ics_sp1_nn_cell_dot_sum) + (ff_s_dot_mcp_ics_sp1_nn_cell_dot_sum))) /\ ff_s_dot_mcp_ics_sp1_nn_cell_dot_sum = ff_r_dot_mcp_ics_sp1_nn_cell_dot_sum + ff_a_dot_mcp_ics_sp1_nn_cell_dot_sum))))))))))) /\ (((exists fs_h_mcp_ics_sp1_nn_entry. fs_h_mcp_ics_sp1_nn_entry + S (ff_value_mcp_prefix_ics_sp1_nn) = S ((S (ff_index_mcp_prefix_ics_sp1_nn)) * ff_nns_mcp_smatrix_ics_sp1)) /\ exists fs_q_mcp_ics_sp1_nn_entry. ff_nn_mcp_smatrix_ics_sp1 = fs_q_mcp_ics_sp1_nn_entry * S ((S (ff_index_mcp_prefix_ics_sp1_nn)) * ff_nns_mcp_smatrix_ics_sp1) + (ff_value_mcp_prefix_ics_sp1_nn))))))) /\ ((forall ff_index_mcp_prefix_ics_sp1_pn. (exists mcp_gap_ics_sp1_pn_index. mcp_gap_ics_sp1_pn_index + S (ff_index_mcp_prefix_ics_sp1_pn) = ((r) * (1))) -> exists ff_row_mcp_prefix_ics_sp1_pn ff_column_mcp_prefix_ics_sp1_pn ff_value_mcp_prefix_ics_sp1_pn. ((ff_index_mcp_prefix_ics_sp1_pn) = (1) * ff_row_mcp_prefix_ics_sp1_pn + ff_column_mcp_prefix_ics_sp1_pn /\ ((exists mcp_gap_ics_sp1_pn_column. mcp_gap_ics_sp1_pn_column + S (ff_column_mcp_prefix_ics_sp1_pn) = (1)) /\ ((exists ff_left_mcp_cell_ics_sp1_pn_cell ff_left_scale_mcp_cell_ics_sp1_pn_cell ff_right_mcp_cell_ics_sp1_pn_cell ff_right_scale_mcp_cell_ics_sp1_pn_cell. ((forall ff_index_mcp_ics_sp1_pn_cell_row ff_source_mcp_ics_sp1_pn_cell_row ff_target_mcp_ics_sp1_pn_cell_row. (exists mcp_gap_ics_sp1_pn_cell_row_bound. mcp_gap_ics_sp1_pn_cell_row_bound + S (ff_index_mcp_ics_sp1_pn_cell_row) = (w)) -> (((exists fs_h_mcp_ics_sp1_pn_cell_row_source. fs_h_mcp_ics_sp1_pn_cell_row_source + S (ff_source_mcp_ics_sp1_pn_cell_row) = S ((S (((ff_row_mcp_prefix_ics_sp1_pn) * (w)) + (1) * ff_index_mcp_ics_sp1_pn_cell_row)) * ac)) /\ exists fs_q_mcp_ics_sp1_pn_cell_row_source. ab = fs_q_mcp_ics_sp1_pn_cell_row_source * S ((S (((ff_row_mcp_prefix_ics_sp1_pn) * (w)) + (1) * ff_index_mcp_ics_sp1_pn_cell_row)) * ac) + (ff_source_mcp_ics_sp1_pn_cell_row))) -> (((exists fs_h_mcp_ics_sp1_pn_cell_row_target. fs_h_mcp_ics_sp1_pn_cell_row_target + S (ff_target_mcp_ics_sp1_pn_cell_row) = S ((S (ff_index_mcp_ics_sp1_pn_cell_row)) * ff_left_scale_mcp_cell_ics_sp1_pn_cell)) /\ exists fs_q_mcp_ics_sp1_pn_cell_row_target. ff_left_mcp_cell_ics_sp1_pn_cell = fs_q_mcp_ics_sp1_pn_cell_row_target * S ((S (ff_index_mcp_ics_sp1_pn_cell_row)) * ff_left_scale_mcp_cell_ics_sp1_pn_cell) + (ff_target_mcp_ics_sp1_pn_cell_row))) -> ff_target_mcp_ics_sp1_pn_cell_row = ff_source_mcp_ics_sp1_pn_cell_row) /\ ((forall ff_index_mcp_ics_sp1_pn_cell_column ff_source_mcp_ics_sp1_pn_cell_column ff_target_mcp_ics_sp1_pn_cell_column. (exists mcp_gap_ics_sp1_pn_cell_column_bound. mcp_gap_ics_sp1_pn_cell_column_bound + S (ff_index_mcp_ics_sp1_pn_cell_column) = (w)) -> (((exists fs_h_mcp_ics_sp1_pn_cell_column_source. fs_h_mcp_ics_sp1_pn_cell_column_source + S (ff_source_mcp_ics_sp1_pn_cell_column) = S ((S ((ff_column_mcp_prefix_ics_sp1_pn) + (1) * ff_index_mcp_ics_sp1_pn_cell_column)) * hc)) /\ exists fs_q_mcp_ics_sp1_pn_cell_column_source. hb = fs_q_mcp_ics_sp1_pn_cell_column_source * S ((S ((ff_column_mcp_prefix_ics_sp1_pn) + (1) * ff_index_mcp_ics_sp1_pn_cell_column)) * hc) + (ff_source_mcp_ics_sp1_pn_cell_column))) -> (((exists fs_h_mcp_ics_sp1_pn_cell_column_target. fs_h_mcp_ics_sp1_pn_cell_column_target + S (ff_target_mcp_ics_sp1_pn_cell_column) = S ((S (ff_index_mcp_ics_sp1_pn_cell_column)) * ff_right_scale_mcp_cell_ics_sp1_pn_cell)) /\ exists fs_q_mcp_ics_sp1_pn_cell_column_target. ff_right_mcp_cell_ics_sp1_pn_cell = fs_q_mcp_ics_sp1_pn_cell_column_target * S ((S (ff_index_mcp_ics_sp1_pn_cell_column)) * ff_right_scale_mcp_cell_ics_sp1_pn_cell) + (ff_target_mcp_ics_sp1_pn_cell_column))) -> ff_target_mcp_ics_sp1_pn_cell_column = ff_source_mcp_ics_sp1_pn_cell_column) /\ (exists ff_code_dot_mcp_ics_sp1_pn_cell_dot ff_scale_dot_mcp_ics_sp1_pn_cell_dot. ((forall fpmp_index_dot_mcp_ics_sp1_pn_cell_dot_pointwise fpmp_left_dot_mcp_ics_sp1_pn_cell_dot_pointwise fpmp_right_dot_mcp_ics_sp1_pn_cell_dot_pointwise fpmp_target_dot_mcp_ics_sp1_pn_cell_dot_pointwise. (exists fpmp_gap_dot_mcp_ics_sp1_pn_cell_dot_pointwise. fpmp_gap_dot_mcp_ics_sp1_pn_cell_dot_pointwise + S fpmp_index_dot_mcp_ics_sp1_pn_cell_dot_pointwise = w) -> (((exists ff_h_fpmp_dot_mcp_ics_sp1_pn_cell_dot_pointwise_left. ff_h_fpmp_dot_mcp_ics_sp1_pn_cell_dot_pointwise_left + S (fpmp_left_dot_mcp_ics_sp1_pn_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_sp1_pn_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_sp1_pn_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_sp1_pn_cell_dot_pointwise_left. ff_left_mcp_cell_ics_sp1_pn_cell = ff_q_fpmp_dot_mcp_ics_sp1_pn_cell_dot_pointwise_left * S ((S (fpmp_index_dot_mcp_ics_sp1_pn_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_sp1_pn_cell) + (fpmp_left_dot_mcp_ics_sp1_pn_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_sp1_pn_cell_dot_pointwise_right. ff_h_fpmp_dot_mcp_ics_sp1_pn_cell_dot_pointwise_right + S (fpmp_right_dot_mcp_ics_sp1_pn_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_sp1_pn_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_sp1_pn_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_sp1_pn_cell_dot_pointwise_right. ff_right_mcp_cell_ics_sp1_pn_cell = ff_q_fpmp_dot_mcp_ics_sp1_pn_cell_dot_pointwise_right * S ((S (fpmp_index_dot_mcp_ics_sp1_pn_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_sp1_pn_cell) + (fpmp_right_dot_mcp_ics_sp1_pn_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_sp1_pn_cell_dot_pointwise_target. ff_h_fpmp_dot_mcp_ics_sp1_pn_cell_dot_pointwise_target + S (fpmp_target_dot_mcp_ics_sp1_pn_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_sp1_pn_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_sp1_pn_cell_dot)) /\ exists ff_q_fpmp_dot_mcp_ics_sp1_pn_cell_dot_pointwise_target. ff_code_dot_mcp_ics_sp1_pn_cell_dot = ff_q_fpmp_dot_mcp_ics_sp1_pn_cell_dot_pointwise_target * S ((S (fpmp_index_dot_mcp_ics_sp1_pn_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_sp1_pn_cell_dot) + (fpmp_target_dot_mcp_ics_sp1_pn_cell_dot_pointwise))) -> fpmp_target_dot_mcp_ics_sp1_pn_cell_dot_pointwise = fpmp_left_dot_mcp_ics_sp1_pn_cell_dot_pointwise * fpmp_right_dot_mcp_ics_sp1_pn_cell_dot_pointwise) /\ (exists ff_u_dot_mcp_ics_sp1_pn_cell_dot_sum ff_v_dot_mcp_ics_sp1_pn_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_sp1_pn_cell_dot_sum_start. ff_h_dot_mcp_ics_sp1_pn_cell_dot_sum_start + S (0) = S ((S (0)) * ff_v_dot_mcp_ics_sp1_pn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_sp1_pn_cell_dot_sum_start. ff_u_dot_mcp_ics_sp1_pn_cell_dot_sum = ff_q_dot_mcp_ics_sp1_pn_cell_dot_sum_start * S ((S (0)) * ff_v_dot_mcp_ics_sp1_pn_cell_dot_sum) + (0))) /\ ((((exists ff_h_dot_mcp_ics_sp1_pn_cell_dot_sum_terminal. ff_h_dot_mcp_ics_sp1_pn_cell_dot_sum_terminal + S (ff_value_mcp_prefix_ics_sp1_pn) = S ((S (w)) * ff_v_dot_mcp_ics_sp1_pn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_sp1_pn_cell_dot_sum_terminal. ff_u_dot_mcp_ics_sp1_pn_cell_dot_sum = ff_q_dot_mcp_ics_sp1_pn_cell_dot_sum_terminal * S ((S (w)) * ff_v_dot_mcp_ics_sp1_pn_cell_dot_sum) + (ff_value_mcp_prefix_ics_sp1_pn))) /\ forall ff_i_dot_mcp_ics_sp1_pn_cell_dot_sum. (exists ff_lt_dot_mcp_ics_sp1_pn_cell_dot_sum_bound. ff_lt_dot_mcp_ics_sp1_pn_cell_dot_sum_bound + S ff_i_dot_mcp_ics_sp1_pn_cell_dot_sum = w) -> exists ff_a_dot_mcp_ics_sp1_pn_cell_dot_sum ff_r_dot_mcp_ics_sp1_pn_cell_dot_sum ff_s_dot_mcp_ics_sp1_pn_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_sp1_pn_cell_dot_sum_summand. ff_h_dot_mcp_ics_sp1_pn_cell_dot_sum_summand + S (ff_a_dot_mcp_ics_sp1_pn_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_sp1_pn_cell_dot_sum)) * ff_scale_dot_mcp_ics_sp1_pn_cell_dot)) /\ exists ff_q_dot_mcp_ics_sp1_pn_cell_dot_sum_summand. ff_code_dot_mcp_ics_sp1_pn_cell_dot = ff_q_dot_mcp_ics_sp1_pn_cell_dot_sum_summand * S ((S (ff_i_dot_mcp_ics_sp1_pn_cell_dot_sum)) * ff_scale_dot_mcp_ics_sp1_pn_cell_dot) + (ff_a_dot_mcp_ics_sp1_pn_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_sp1_pn_cell_dot_sum_partial. ff_h_dot_mcp_ics_sp1_pn_cell_dot_sum_partial + S (ff_r_dot_mcp_ics_sp1_pn_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_sp1_pn_cell_dot_sum)) * ff_v_dot_mcp_ics_sp1_pn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_sp1_pn_cell_dot_sum_partial. ff_u_dot_mcp_ics_sp1_pn_cell_dot_sum = ff_q_dot_mcp_ics_sp1_pn_cell_dot_sum_partial * S ((S (ff_i_dot_mcp_ics_sp1_pn_cell_dot_sum)) * ff_v_dot_mcp_ics_sp1_pn_cell_dot_sum) + (ff_r_dot_mcp_ics_sp1_pn_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_sp1_pn_cell_dot_sum_successor. ff_h_dot_mcp_ics_sp1_pn_cell_dot_sum_successor + S (ff_s_dot_mcp_ics_sp1_pn_cell_dot_sum) = S ((S (S ff_i_dot_mcp_ics_sp1_pn_cell_dot_sum)) * ff_v_dot_mcp_ics_sp1_pn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_sp1_pn_cell_dot_sum_successor. ff_u_dot_mcp_ics_sp1_pn_cell_dot_sum = ff_q_dot_mcp_ics_sp1_pn_cell_dot_sum_successor * S ((S (S ff_i_dot_mcp_ics_sp1_pn_cell_dot_sum)) * ff_v_dot_mcp_ics_sp1_pn_cell_dot_sum) + (ff_s_dot_mcp_ics_sp1_pn_cell_dot_sum))) /\ ff_s_dot_mcp_ics_sp1_pn_cell_dot_sum = ff_r_dot_mcp_ics_sp1_pn_cell_dot_sum + ff_a_dot_mcp_ics_sp1_pn_cell_dot_sum))))))))))) /\ (((exists fs_h_mcp_ics_sp1_pn_entry. fs_h_mcp_ics_sp1_pn_entry + S (ff_value_mcp_prefix_ics_sp1_pn) = S ((S (ff_index_mcp_prefix_ics_sp1_pn)) * ff_pns_mcp_smatrix_ics_sp1)) /\ exists fs_q_mcp_ics_sp1_pn_entry. ff_pn_mcp_smatrix_ics_sp1 = fs_q_mcp_ics_sp1_pn_entry * S ((S (ff_index_mcp_prefix_ics_sp1_pn)) * ff_pns_mcp_smatrix_ics_sp1) + (ff_value_mcp_prefix_ics_sp1_pn))))))) /\ ((forall ff_index_mcp_prefix_ics_sp1_np. (exists mcp_gap_ics_sp1_np_index. mcp_gap_ics_sp1_np_index + S (ff_index_mcp_prefix_ics_sp1_np) = ((r) * (1))) -> exists ff_row_mcp_prefix_ics_sp1_np ff_column_mcp_prefix_ics_sp1_np ff_value_mcp_prefix_ics_sp1_np. ((ff_index_mcp_prefix_ics_sp1_np) = (1) * ff_row_mcp_prefix_ics_sp1_np + ff_column_mcp_prefix_ics_sp1_np /\ ((exists mcp_gap_ics_sp1_np_column. mcp_gap_ics_sp1_np_column + S (ff_column_mcp_prefix_ics_sp1_np) = (1)) /\ ((exists ff_left_mcp_cell_ics_sp1_np_cell ff_left_scale_mcp_cell_ics_sp1_np_cell ff_right_mcp_cell_ics_sp1_np_cell ff_right_scale_mcp_cell_ics_sp1_np_cell. ((forall ff_index_mcp_ics_sp1_np_cell_row ff_source_mcp_ics_sp1_np_cell_row ff_target_mcp_ics_sp1_np_cell_row. (exists mcp_gap_ics_sp1_np_cell_row_bound. mcp_gap_ics_sp1_np_cell_row_bound + S (ff_index_mcp_ics_sp1_np_cell_row) = (w)) -> (((exists fs_h_mcp_ics_sp1_np_cell_row_source. fs_h_mcp_ics_sp1_np_cell_row_source + S (ff_source_mcp_ics_sp1_np_cell_row) = S ((S (((ff_row_mcp_prefix_ics_sp1_np) * (w)) + (1) * ff_index_mcp_ics_sp1_np_cell_row)) * dc)) /\ exists fs_q_mcp_ics_sp1_np_cell_row_source. db = fs_q_mcp_ics_sp1_np_cell_row_source * S ((S (((ff_row_mcp_prefix_ics_sp1_np) * (w)) + (1) * ff_index_mcp_ics_sp1_np_cell_row)) * dc) + (ff_source_mcp_ics_sp1_np_cell_row))) -> (((exists fs_h_mcp_ics_sp1_np_cell_row_target. fs_h_mcp_ics_sp1_np_cell_row_target + S (ff_target_mcp_ics_sp1_np_cell_row) = S ((S (ff_index_mcp_ics_sp1_np_cell_row)) * ff_left_scale_mcp_cell_ics_sp1_np_cell)) /\ exists fs_q_mcp_ics_sp1_np_cell_row_target. ff_left_mcp_cell_ics_sp1_np_cell = fs_q_mcp_ics_sp1_np_cell_row_target * S ((S (ff_index_mcp_ics_sp1_np_cell_row)) * ff_left_scale_mcp_cell_ics_sp1_np_cell) + (ff_target_mcp_ics_sp1_np_cell_row))) -> ff_target_mcp_ics_sp1_np_cell_row = ff_source_mcp_ics_sp1_np_cell_row) /\ ((forall ff_index_mcp_ics_sp1_np_cell_column ff_source_mcp_ics_sp1_np_cell_column ff_target_mcp_ics_sp1_np_cell_column. (exists mcp_gap_ics_sp1_np_cell_column_bound. mcp_gap_ics_sp1_np_cell_column_bound + S (ff_index_mcp_ics_sp1_np_cell_column) = (w)) -> (((exists fs_h_mcp_ics_sp1_np_cell_column_source. fs_h_mcp_ics_sp1_np_cell_column_source + S (ff_source_mcp_ics_sp1_np_cell_column) = S ((S ((ff_column_mcp_prefix_ics_sp1_np) + (1) * ff_index_mcp_ics_sp1_np_cell_column)) * gc)) /\ exists fs_q_mcp_ics_sp1_np_cell_column_source. gb = fs_q_mcp_ics_sp1_np_cell_column_source * S ((S ((ff_column_mcp_prefix_ics_sp1_np) + (1) * ff_index_mcp_ics_sp1_np_cell_column)) * gc) + (ff_source_mcp_ics_sp1_np_cell_column))) -> (((exists fs_h_mcp_ics_sp1_np_cell_column_target. fs_h_mcp_ics_sp1_np_cell_column_target + S (ff_target_mcp_ics_sp1_np_cell_column) = S ((S (ff_index_mcp_ics_sp1_np_cell_column)) * ff_right_scale_mcp_cell_ics_sp1_np_cell)) /\ exists fs_q_mcp_ics_sp1_np_cell_column_target. ff_right_mcp_cell_ics_sp1_np_cell = fs_q_mcp_ics_sp1_np_cell_column_target * S ((S (ff_index_mcp_ics_sp1_np_cell_column)) * ff_right_scale_mcp_cell_ics_sp1_np_cell) + (ff_target_mcp_ics_sp1_np_cell_column))) -> ff_target_mcp_ics_sp1_np_cell_column = ff_source_mcp_ics_sp1_np_cell_column) /\ (exists ff_code_dot_mcp_ics_sp1_np_cell_dot ff_scale_dot_mcp_ics_sp1_np_cell_dot. ((forall fpmp_index_dot_mcp_ics_sp1_np_cell_dot_pointwise fpmp_left_dot_mcp_ics_sp1_np_cell_dot_pointwise fpmp_right_dot_mcp_ics_sp1_np_cell_dot_pointwise fpmp_target_dot_mcp_ics_sp1_np_cell_dot_pointwise. (exists fpmp_gap_dot_mcp_ics_sp1_np_cell_dot_pointwise. fpmp_gap_dot_mcp_ics_sp1_np_cell_dot_pointwise + S fpmp_index_dot_mcp_ics_sp1_np_cell_dot_pointwise = w) -> (((exists ff_h_fpmp_dot_mcp_ics_sp1_np_cell_dot_pointwise_left. ff_h_fpmp_dot_mcp_ics_sp1_np_cell_dot_pointwise_left + S (fpmp_left_dot_mcp_ics_sp1_np_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_sp1_np_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_sp1_np_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_sp1_np_cell_dot_pointwise_left. ff_left_mcp_cell_ics_sp1_np_cell = ff_q_fpmp_dot_mcp_ics_sp1_np_cell_dot_pointwise_left * S ((S (fpmp_index_dot_mcp_ics_sp1_np_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_sp1_np_cell) + (fpmp_left_dot_mcp_ics_sp1_np_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_sp1_np_cell_dot_pointwise_right. ff_h_fpmp_dot_mcp_ics_sp1_np_cell_dot_pointwise_right + S (fpmp_right_dot_mcp_ics_sp1_np_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_sp1_np_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_sp1_np_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_sp1_np_cell_dot_pointwise_right. ff_right_mcp_cell_ics_sp1_np_cell = ff_q_fpmp_dot_mcp_ics_sp1_np_cell_dot_pointwise_right * S ((S (fpmp_index_dot_mcp_ics_sp1_np_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_sp1_np_cell) + (fpmp_right_dot_mcp_ics_sp1_np_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_sp1_np_cell_dot_pointwise_target. ff_h_fpmp_dot_mcp_ics_sp1_np_cell_dot_pointwise_target + S (fpmp_target_dot_mcp_ics_sp1_np_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_sp1_np_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_sp1_np_cell_dot)) /\ exists ff_q_fpmp_dot_mcp_ics_sp1_np_cell_dot_pointwise_target. ff_code_dot_mcp_ics_sp1_np_cell_dot = ff_q_fpmp_dot_mcp_ics_sp1_np_cell_dot_pointwise_target * S ((S (fpmp_index_dot_mcp_ics_sp1_np_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_sp1_np_cell_dot) + (fpmp_target_dot_mcp_ics_sp1_np_cell_dot_pointwise))) -> fpmp_target_dot_mcp_ics_sp1_np_cell_dot_pointwise = fpmp_left_dot_mcp_ics_sp1_np_cell_dot_pointwise * fpmp_right_dot_mcp_ics_sp1_np_cell_dot_pointwise) /\ (exists ff_u_dot_mcp_ics_sp1_np_cell_dot_sum ff_v_dot_mcp_ics_sp1_np_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_sp1_np_cell_dot_sum_start. ff_h_dot_mcp_ics_sp1_np_cell_dot_sum_start + S (0) = S ((S (0)) * ff_v_dot_mcp_ics_sp1_np_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_sp1_np_cell_dot_sum_start. ff_u_dot_mcp_ics_sp1_np_cell_dot_sum = ff_q_dot_mcp_ics_sp1_np_cell_dot_sum_start * S ((S (0)) * ff_v_dot_mcp_ics_sp1_np_cell_dot_sum) + (0))) /\ ((((exists ff_h_dot_mcp_ics_sp1_np_cell_dot_sum_terminal. ff_h_dot_mcp_ics_sp1_np_cell_dot_sum_terminal + S (ff_value_mcp_prefix_ics_sp1_np) = S ((S (w)) * ff_v_dot_mcp_ics_sp1_np_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_sp1_np_cell_dot_sum_terminal. ff_u_dot_mcp_ics_sp1_np_cell_dot_sum = ff_q_dot_mcp_ics_sp1_np_cell_dot_sum_terminal * S ((S (w)) * ff_v_dot_mcp_ics_sp1_np_cell_dot_sum) + (ff_value_mcp_prefix_ics_sp1_np))) /\ forall ff_i_dot_mcp_ics_sp1_np_cell_dot_sum. (exists ff_lt_dot_mcp_ics_sp1_np_cell_dot_sum_bound. ff_lt_dot_mcp_ics_sp1_np_cell_dot_sum_bound + S ff_i_dot_mcp_ics_sp1_np_cell_dot_sum = w) -> exists ff_a_dot_mcp_ics_sp1_np_cell_dot_sum ff_r_dot_mcp_ics_sp1_np_cell_dot_sum ff_s_dot_mcp_ics_sp1_np_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_sp1_np_cell_dot_sum_summand. ff_h_dot_mcp_ics_sp1_np_cell_dot_sum_summand + S (ff_a_dot_mcp_ics_sp1_np_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_sp1_np_cell_dot_sum)) * ff_scale_dot_mcp_ics_sp1_np_cell_dot)) /\ exists ff_q_dot_mcp_ics_sp1_np_cell_dot_sum_summand. ff_code_dot_mcp_ics_sp1_np_cell_dot = ff_q_dot_mcp_ics_sp1_np_cell_dot_sum_summand * S ((S (ff_i_dot_mcp_ics_sp1_np_cell_dot_sum)) * ff_scale_dot_mcp_ics_sp1_np_cell_dot) + (ff_a_dot_mcp_ics_sp1_np_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_sp1_np_cell_dot_sum_partial. ff_h_dot_mcp_ics_sp1_np_cell_dot_sum_partial + S (ff_r_dot_mcp_ics_sp1_np_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_sp1_np_cell_dot_sum)) * ff_v_dot_mcp_ics_sp1_np_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_sp1_np_cell_dot_sum_partial. ff_u_dot_mcp_ics_sp1_np_cell_dot_sum = ff_q_dot_mcp_ics_sp1_np_cell_dot_sum_partial * S ((S (ff_i_dot_mcp_ics_sp1_np_cell_dot_sum)) * ff_v_dot_mcp_ics_sp1_np_cell_dot_sum) + (ff_r_dot_mcp_ics_sp1_np_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_sp1_np_cell_dot_sum_successor. ff_h_dot_mcp_ics_sp1_np_cell_dot_sum_successor + S (ff_s_dot_mcp_ics_sp1_np_cell_dot_sum) = S ((S (S ff_i_dot_mcp_ics_sp1_np_cell_dot_sum)) * ff_v_dot_mcp_ics_sp1_np_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_sp1_np_cell_dot_sum_successor. ff_u_dot_mcp_ics_sp1_np_cell_dot_sum = ff_q_dot_mcp_ics_sp1_np_cell_dot_sum_successor * S ((S (S ff_i_dot_mcp_ics_sp1_np_cell_dot_sum)) * ff_v_dot_mcp_ics_sp1_np_cell_dot_sum) + (ff_s_dot_mcp_ics_sp1_np_cell_dot_sum))) /\ ff_s_dot_mcp_ics_sp1_np_cell_dot_sum = ff_r_dot_mcp_ics_sp1_np_cell_dot_sum + ff_a_dot_mcp_ics_sp1_np_cell_dot_sum))))))))))) /\ (((exists fs_h_mcp_ics_sp1_np_entry. fs_h_mcp_ics_sp1_np_entry + S (ff_value_mcp_prefix_ics_sp1_np) = S ((S (ff_index_mcp_prefix_ics_sp1_np)) * ff_nps_mcp_smatrix_ics_sp1)) /\ exists fs_q_mcp_ics_sp1_np_entry. ff_np_mcp_smatrix_ics_sp1 = fs_q_mcp_ics_sp1_np_entry * S ((S (ff_index_mcp_prefix_ics_sp1_np)) * ff_nps_mcp_smatrix_ics_sp1) + (ff_value_mcp_prefix_ics_sp1_np))))))) /\ ((forall ff_index_mcp_add_ics_sp1_positive ff_left_mcp_add_ics_sp1_positive ff_right_mcp_add_ics_sp1_positive ff_target_mcp_add_ics_sp1_positive. (exists mcp_gap_ics_sp1_positive_bound. mcp_gap_ics_sp1_positive_bound + S (ff_index_mcp_add_ics_sp1_positive) = ((r) * (1))) -> (((exists fs_h_mcp_ics_sp1_positive_left. fs_h_mcp_ics_sp1_positive_left + S (ff_left_mcp_add_ics_sp1_positive) = S ((S (ff_index_mcp_add_ics_sp1_positive)) * ff_pps_mcp_smatrix_ics_sp1)) /\ exists fs_q_mcp_ics_sp1_positive_left. ff_pp_mcp_smatrix_ics_sp1 = fs_q_mcp_ics_sp1_positive_left * S ((S (ff_index_mcp_add_ics_sp1_positive)) * ff_pps_mcp_smatrix_ics_sp1) + (ff_left_mcp_add_ics_sp1_positive))) -> (((exists fs_h_mcp_ics_sp1_positive_right. fs_h_mcp_ics_sp1_positive_right + S (ff_right_mcp_add_ics_sp1_positive) = S ((S (ff_index_mcp_add_ics_sp1_positive)) * ff_nns_mcp_smatrix_ics_sp1)) /\ exists fs_q_mcp_ics_sp1_positive_right. ff_nn_mcp_smatrix_ics_sp1 = fs_q_mcp_ics_sp1_positive_right * S ((S (ff_index_mcp_add_ics_sp1_positive)) * ff_nns_mcp_smatrix_ics_sp1) + (ff_right_mcp_add_ics_sp1_positive))) -> (((exists fs_h_mcp_ics_sp1_positive_target. fs_h_mcp_ics_sp1_positive_target + S (ff_target_mcp_add_ics_sp1_positive) = S ((S (ff_index_mcp_add_ics_sp1_positive)) * qc)) /\ exists fs_q_mcp_ics_sp1_positive_target. qb = fs_q_mcp_ics_sp1_positive_target * S ((S (ff_index_mcp_add_ics_sp1_positive)) * qc) + (ff_target_mcp_add_ics_sp1_positive))) -> ff_target_mcp_add_ics_sp1_positive = ff_left_mcp_add_ics_sp1_positive + ff_right_mcp_add_ics_sp1_positive) /\ (forall ff_index_mcp_add_ics_sp1_negative ff_left_mcp_add_ics_sp1_negative ff_right_mcp_add_ics_sp1_negative ff_target_mcp_add_ics_sp1_negative. (exists mcp_gap_ics_sp1_negative_bound. mcp_gap_ics_sp1_negative_bound + S (ff_index_mcp_add_ics_sp1_negative) = ((r) * (1))) -> (((exists fs_h_mcp_ics_sp1_negative_left. fs_h_mcp_ics_sp1_negative_left + S (ff_left_mcp_add_ics_sp1_negative) = S ((S (ff_index_mcp_add_ics_sp1_negative)) * ff_pns_mcp_smatrix_ics_sp1)) /\ exists fs_q_mcp_ics_sp1_negative_left. ff_pn_mcp_smatrix_ics_sp1 = fs_q_mcp_ics_sp1_negative_left * S ((S (ff_index_mcp_add_ics_sp1_negative)) * ff_pns_mcp_smatrix_ics_sp1) + (ff_left_mcp_add_ics_sp1_negative))) -> (((exists fs_h_mcp_ics_sp1_negative_right. fs_h_mcp_ics_sp1_negative_right + S (ff_right_mcp_add_ics_sp1_negative) = S ((S (ff_index_mcp_add_ics_sp1_negative)) * ff_nps_mcp_smatrix_ics_sp1)) /\ exists fs_q_mcp_ics_sp1_negative_right. ff_np_mcp_smatrix_ics_sp1 = fs_q_mcp_ics_sp1_negative_right * S ((S (ff_index_mcp_add_ics_sp1_negative)) * ff_nps_mcp_smatrix_ics_sp1) + (ff_right_mcp_add_ics_sp1_negative))) -> (((exists fs_h_mcp_ics_sp1_negative_target. fs_h_mcp_ics_sp1_negative_target + S (ff_target_mcp_add_ics_sp1_negative) = S ((S (ff_index_mcp_add_ics_sp1_negative)) * mc)) /\ exists fs_q_mcp_ics_sp1_negative_target. mb = fs_q_mcp_ics_sp1_negative_target * S ((S (ff_index_mcp_add_ics_sp1_negative)) * mc) + (ff_target_mcp_add_ics_sp1_negative))) -> ff_target_mcp_add_ics_sp1_negative = ff_left_mcp_add_ics_sp1_negative + ff_right_mcp_add_ics_sp1_negative))))))) -> (exists ff_pp_mcp_smatrix_ics_sp2 ff_pps_mcp_smatrix_ics_sp2 ff_nn_mcp_smatrix_ics_sp2 ff_nns_mcp_smatrix_ics_sp2 ff_pn_mcp_smatrix_ics_sp2 ff_pns_mcp_smatrix_ics_sp2 ff_np_mcp_smatrix_ics_sp2 ff_nps_mcp_smatrix_ics_sp2. ((forall ff_index_mcp_prefix_ics_sp2_pp. (exists mcp_gap_ics_sp2_pp_index. mcp_gap_ics_sp2_pp_index + S (ff_index_mcp_prefix_ics_sp2_pp) = ((r) * (1))) -> exists ff_row_mcp_prefix_ics_sp2_pp ff_column_mcp_prefix_ics_sp2_pp ff_value_mcp_prefix_ics_sp2_pp. ((ff_index_mcp_prefix_ics_sp2_pp) = (1) * ff_row_mcp_prefix_ics_sp2_pp + ff_column_mcp_prefix_ics_sp2_pp /\ ((exists mcp_gap_ics_sp2_pp_column. mcp_gap_ics_sp2_pp_column + S (ff_column_mcp_prefix_ics_sp2_pp) = (1)) /\ ((exists ff_left_mcp_cell_ics_sp2_pp_cell ff_left_scale_mcp_cell_ics_sp2_pp_cell ff_right_mcp_cell_ics_sp2_pp_cell ff_right_scale_mcp_cell_ics_sp2_pp_cell. ((forall ff_index_mcp_ics_sp2_pp_cell_row ff_source_mcp_ics_sp2_pp_cell_row ff_target_mcp_ics_sp2_pp_cell_row. (exists mcp_gap_ics_sp2_pp_cell_row_bound. mcp_gap_ics_sp2_pp_cell_row_bound + S (ff_index_mcp_ics_sp2_pp_cell_row) = (w)) -> (((exists fs_h_mcp_ics_sp2_pp_cell_row_source. fs_h_mcp_ics_sp2_pp_cell_row_source + S (ff_source_mcp_ics_sp2_pp_cell_row) = S ((S (((ff_row_mcp_prefix_ics_sp2_pp) * (w)) + (1) * ff_index_mcp_ics_sp2_pp_cell_row)) * ac)) /\ exists fs_q_mcp_ics_sp2_pp_cell_row_source. ab = fs_q_mcp_ics_sp2_pp_cell_row_source * S ((S (((ff_row_mcp_prefix_ics_sp2_pp) * (w)) + (1) * ff_index_mcp_ics_sp2_pp_cell_row)) * ac) + (ff_source_mcp_ics_sp2_pp_cell_row))) -> (((exists fs_h_mcp_ics_sp2_pp_cell_row_target. fs_h_mcp_ics_sp2_pp_cell_row_target + S (ff_target_mcp_ics_sp2_pp_cell_row) = S ((S (ff_index_mcp_ics_sp2_pp_cell_row)) * ff_left_scale_mcp_cell_ics_sp2_pp_cell)) /\ exists fs_q_mcp_ics_sp2_pp_cell_row_target. ff_left_mcp_cell_ics_sp2_pp_cell = fs_q_mcp_ics_sp2_pp_cell_row_target * S ((S (ff_index_mcp_ics_sp2_pp_cell_row)) * ff_left_scale_mcp_cell_ics_sp2_pp_cell) + (ff_target_mcp_ics_sp2_pp_cell_row))) -> ff_target_mcp_ics_sp2_pp_cell_row = ff_source_mcp_ics_sp2_pp_cell_row) /\ ((forall ff_index_mcp_ics_sp2_pp_cell_column ff_source_mcp_ics_sp2_pp_cell_column ff_target_mcp_ics_sp2_pp_cell_column. (exists mcp_gap_ics_sp2_pp_cell_column_bound. mcp_gap_ics_sp2_pp_cell_column_bound + S (ff_index_mcp_ics_sp2_pp_cell_column) = (w)) -> (((exists fs_h_mcp_ics_sp2_pp_cell_column_source. fs_h_mcp_ics_sp2_pp_cell_column_source + S (ff_source_mcp_ics_sp2_pp_cell_column) = S ((S ((ff_column_mcp_prefix_ics_sp2_pp) + (1) * ff_index_mcp_ics_sp2_pp_cell_column)) * ic)) /\ exists fs_q_mcp_ics_sp2_pp_cell_column_source. ib = fs_q_mcp_ics_sp2_pp_cell_column_source * S ((S ((ff_column_mcp_prefix_ics_sp2_pp) + (1) * ff_index_mcp_ics_sp2_pp_cell_column)) * ic) + (ff_source_mcp_ics_sp2_pp_cell_column))) -> (((exists fs_h_mcp_ics_sp2_pp_cell_column_target. fs_h_mcp_ics_sp2_pp_cell_column_target + S (ff_target_mcp_ics_sp2_pp_cell_column) = S ((S (ff_index_mcp_ics_sp2_pp_cell_column)) * ff_right_scale_mcp_cell_ics_sp2_pp_cell)) /\ exists fs_q_mcp_ics_sp2_pp_cell_column_target. ff_right_mcp_cell_ics_sp2_pp_cell = fs_q_mcp_ics_sp2_pp_cell_column_target * S ((S (ff_index_mcp_ics_sp2_pp_cell_column)) * ff_right_scale_mcp_cell_ics_sp2_pp_cell) + (ff_target_mcp_ics_sp2_pp_cell_column))) -> ff_target_mcp_ics_sp2_pp_cell_column = ff_source_mcp_ics_sp2_pp_cell_column) /\ (exists ff_code_dot_mcp_ics_sp2_pp_cell_dot ff_scale_dot_mcp_ics_sp2_pp_cell_dot. ((forall fpmp_index_dot_mcp_ics_sp2_pp_cell_dot_pointwise fpmp_left_dot_mcp_ics_sp2_pp_cell_dot_pointwise fpmp_right_dot_mcp_ics_sp2_pp_cell_dot_pointwise fpmp_target_dot_mcp_ics_sp2_pp_cell_dot_pointwise. (exists fpmp_gap_dot_mcp_ics_sp2_pp_cell_dot_pointwise. fpmp_gap_dot_mcp_ics_sp2_pp_cell_dot_pointwise + S fpmp_index_dot_mcp_ics_sp2_pp_cell_dot_pointwise = w) -> (((exists ff_h_fpmp_dot_mcp_ics_sp2_pp_cell_dot_pointwise_left. ff_h_fpmp_dot_mcp_ics_sp2_pp_cell_dot_pointwise_left + S (fpmp_left_dot_mcp_ics_sp2_pp_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_sp2_pp_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_sp2_pp_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_sp2_pp_cell_dot_pointwise_left. ff_left_mcp_cell_ics_sp2_pp_cell = ff_q_fpmp_dot_mcp_ics_sp2_pp_cell_dot_pointwise_left * S ((S (fpmp_index_dot_mcp_ics_sp2_pp_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_sp2_pp_cell) + (fpmp_left_dot_mcp_ics_sp2_pp_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_sp2_pp_cell_dot_pointwise_right. ff_h_fpmp_dot_mcp_ics_sp2_pp_cell_dot_pointwise_right + S (fpmp_right_dot_mcp_ics_sp2_pp_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_sp2_pp_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_sp2_pp_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_sp2_pp_cell_dot_pointwise_right. ff_right_mcp_cell_ics_sp2_pp_cell = ff_q_fpmp_dot_mcp_ics_sp2_pp_cell_dot_pointwise_right * S ((S (fpmp_index_dot_mcp_ics_sp2_pp_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_sp2_pp_cell) + (fpmp_right_dot_mcp_ics_sp2_pp_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_sp2_pp_cell_dot_pointwise_target. ff_h_fpmp_dot_mcp_ics_sp2_pp_cell_dot_pointwise_target + S (fpmp_target_dot_mcp_ics_sp2_pp_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_sp2_pp_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_sp2_pp_cell_dot)) /\ exists ff_q_fpmp_dot_mcp_ics_sp2_pp_cell_dot_pointwise_target. ff_code_dot_mcp_ics_sp2_pp_cell_dot = ff_q_fpmp_dot_mcp_ics_sp2_pp_cell_dot_pointwise_target * S ((S (fpmp_index_dot_mcp_ics_sp2_pp_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_sp2_pp_cell_dot) + (fpmp_target_dot_mcp_ics_sp2_pp_cell_dot_pointwise))) -> fpmp_target_dot_mcp_ics_sp2_pp_cell_dot_pointwise = fpmp_left_dot_mcp_ics_sp2_pp_cell_dot_pointwise * fpmp_right_dot_mcp_ics_sp2_pp_cell_dot_pointwise) /\ (exists ff_u_dot_mcp_ics_sp2_pp_cell_dot_sum ff_v_dot_mcp_ics_sp2_pp_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_sp2_pp_cell_dot_sum_start. ff_h_dot_mcp_ics_sp2_pp_cell_dot_sum_start + S (0) = S ((S (0)) * ff_v_dot_mcp_ics_sp2_pp_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_sp2_pp_cell_dot_sum_start. ff_u_dot_mcp_ics_sp2_pp_cell_dot_sum = ff_q_dot_mcp_ics_sp2_pp_cell_dot_sum_start * S ((S (0)) * ff_v_dot_mcp_ics_sp2_pp_cell_dot_sum) + (0))) /\ ((((exists ff_h_dot_mcp_ics_sp2_pp_cell_dot_sum_terminal. ff_h_dot_mcp_ics_sp2_pp_cell_dot_sum_terminal + S (ff_value_mcp_prefix_ics_sp2_pp) = S ((S (w)) * ff_v_dot_mcp_ics_sp2_pp_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_sp2_pp_cell_dot_sum_terminal. ff_u_dot_mcp_ics_sp2_pp_cell_dot_sum = ff_q_dot_mcp_ics_sp2_pp_cell_dot_sum_terminal * S ((S (w)) * ff_v_dot_mcp_ics_sp2_pp_cell_dot_sum) + (ff_value_mcp_prefix_ics_sp2_pp))) /\ forall ff_i_dot_mcp_ics_sp2_pp_cell_dot_sum. (exists ff_lt_dot_mcp_ics_sp2_pp_cell_dot_sum_bound. ff_lt_dot_mcp_ics_sp2_pp_cell_dot_sum_bound + S ff_i_dot_mcp_ics_sp2_pp_cell_dot_sum = w) -> exists ff_a_dot_mcp_ics_sp2_pp_cell_dot_sum ff_r_dot_mcp_ics_sp2_pp_cell_dot_sum ff_s_dot_mcp_ics_sp2_pp_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_sp2_pp_cell_dot_sum_summand. ff_h_dot_mcp_ics_sp2_pp_cell_dot_sum_summand + S (ff_a_dot_mcp_ics_sp2_pp_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_sp2_pp_cell_dot_sum)) * ff_scale_dot_mcp_ics_sp2_pp_cell_dot)) /\ exists ff_q_dot_mcp_ics_sp2_pp_cell_dot_sum_summand. ff_code_dot_mcp_ics_sp2_pp_cell_dot = ff_q_dot_mcp_ics_sp2_pp_cell_dot_sum_summand * S ((S (ff_i_dot_mcp_ics_sp2_pp_cell_dot_sum)) * ff_scale_dot_mcp_ics_sp2_pp_cell_dot) + (ff_a_dot_mcp_ics_sp2_pp_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_sp2_pp_cell_dot_sum_partial. ff_h_dot_mcp_ics_sp2_pp_cell_dot_sum_partial + S (ff_r_dot_mcp_ics_sp2_pp_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_sp2_pp_cell_dot_sum)) * ff_v_dot_mcp_ics_sp2_pp_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_sp2_pp_cell_dot_sum_partial. ff_u_dot_mcp_ics_sp2_pp_cell_dot_sum = ff_q_dot_mcp_ics_sp2_pp_cell_dot_sum_partial * S ((S (ff_i_dot_mcp_ics_sp2_pp_cell_dot_sum)) * ff_v_dot_mcp_ics_sp2_pp_cell_dot_sum) + (ff_r_dot_mcp_ics_sp2_pp_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_sp2_pp_cell_dot_sum_successor. ff_h_dot_mcp_ics_sp2_pp_cell_dot_sum_successor + S (ff_s_dot_mcp_ics_sp2_pp_cell_dot_sum) = S ((S (S ff_i_dot_mcp_ics_sp2_pp_cell_dot_sum)) * ff_v_dot_mcp_ics_sp2_pp_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_sp2_pp_cell_dot_sum_successor. ff_u_dot_mcp_ics_sp2_pp_cell_dot_sum = ff_q_dot_mcp_ics_sp2_pp_cell_dot_sum_successor * S ((S (S ff_i_dot_mcp_ics_sp2_pp_cell_dot_sum)) * ff_v_dot_mcp_ics_sp2_pp_cell_dot_sum) + (ff_s_dot_mcp_ics_sp2_pp_cell_dot_sum))) /\ ff_s_dot_mcp_ics_sp2_pp_cell_dot_sum = ff_r_dot_mcp_ics_sp2_pp_cell_dot_sum + ff_a_dot_mcp_ics_sp2_pp_cell_dot_sum))))))))))) /\ (((exists fs_h_mcp_ics_sp2_pp_entry. fs_h_mcp_ics_sp2_pp_entry + S (ff_value_mcp_prefix_ics_sp2_pp) = S ((S (ff_index_mcp_prefix_ics_sp2_pp)) * ff_pps_mcp_smatrix_ics_sp2)) /\ exists fs_q_mcp_ics_sp2_pp_entry. ff_pp_mcp_smatrix_ics_sp2 = fs_q_mcp_ics_sp2_pp_entry * S ((S (ff_index_mcp_prefix_ics_sp2_pp)) * ff_pps_mcp_smatrix_ics_sp2) + (ff_value_mcp_prefix_ics_sp2_pp))))))) /\ ((forall ff_index_mcp_prefix_ics_sp2_nn. (exists mcp_gap_ics_sp2_nn_index. mcp_gap_ics_sp2_nn_index + S (ff_index_mcp_prefix_ics_sp2_nn) = ((r) * (1))) -> exists ff_row_mcp_prefix_ics_sp2_nn ff_column_mcp_prefix_ics_sp2_nn ff_value_mcp_prefix_ics_sp2_nn. ((ff_index_mcp_prefix_ics_sp2_nn) = (1) * ff_row_mcp_prefix_ics_sp2_nn + ff_column_mcp_prefix_ics_sp2_nn /\ ((exists mcp_gap_ics_sp2_nn_column. mcp_gap_ics_sp2_nn_column + S (ff_column_mcp_prefix_ics_sp2_nn) = (1)) /\ ((exists ff_left_mcp_cell_ics_sp2_nn_cell ff_left_scale_mcp_cell_ics_sp2_nn_cell ff_right_mcp_cell_ics_sp2_nn_cell ff_right_scale_mcp_cell_ics_sp2_nn_cell. ((forall ff_index_mcp_ics_sp2_nn_cell_row ff_source_mcp_ics_sp2_nn_cell_row ff_target_mcp_ics_sp2_nn_cell_row. (exists mcp_gap_ics_sp2_nn_cell_row_bound. mcp_gap_ics_sp2_nn_cell_row_bound + S (ff_index_mcp_ics_sp2_nn_cell_row) = (w)) -> (((exists fs_h_mcp_ics_sp2_nn_cell_row_source. fs_h_mcp_ics_sp2_nn_cell_row_source + S (ff_source_mcp_ics_sp2_nn_cell_row) = S ((S (((ff_row_mcp_prefix_ics_sp2_nn) * (w)) + (1) * ff_index_mcp_ics_sp2_nn_cell_row)) * dc)) /\ exists fs_q_mcp_ics_sp2_nn_cell_row_source. db = fs_q_mcp_ics_sp2_nn_cell_row_source * S ((S (((ff_row_mcp_prefix_ics_sp2_nn) * (w)) + (1) * ff_index_mcp_ics_sp2_nn_cell_row)) * dc) + (ff_source_mcp_ics_sp2_nn_cell_row))) -> (((exists fs_h_mcp_ics_sp2_nn_cell_row_target. fs_h_mcp_ics_sp2_nn_cell_row_target + S (ff_target_mcp_ics_sp2_nn_cell_row) = S ((S (ff_index_mcp_ics_sp2_nn_cell_row)) * ff_left_scale_mcp_cell_ics_sp2_nn_cell)) /\ exists fs_q_mcp_ics_sp2_nn_cell_row_target. ff_left_mcp_cell_ics_sp2_nn_cell = fs_q_mcp_ics_sp2_nn_cell_row_target * S ((S (ff_index_mcp_ics_sp2_nn_cell_row)) * ff_left_scale_mcp_cell_ics_sp2_nn_cell) + (ff_target_mcp_ics_sp2_nn_cell_row))) -> ff_target_mcp_ics_sp2_nn_cell_row = ff_source_mcp_ics_sp2_nn_cell_row) /\ ((forall ff_index_mcp_ics_sp2_nn_cell_column ff_source_mcp_ics_sp2_nn_cell_column ff_target_mcp_ics_sp2_nn_cell_column. (exists mcp_gap_ics_sp2_nn_cell_column_bound. mcp_gap_ics_sp2_nn_cell_column_bound + S (ff_index_mcp_ics_sp2_nn_cell_column) = (w)) -> (((exists fs_h_mcp_ics_sp2_nn_cell_column_source. fs_h_mcp_ics_sp2_nn_cell_column_source + S (ff_source_mcp_ics_sp2_nn_cell_column) = S ((S ((ff_column_mcp_prefix_ics_sp2_nn) + (1) * ff_index_mcp_ics_sp2_nn_cell_column)) * jc)) /\ exists fs_q_mcp_ics_sp2_nn_cell_column_source. jb = fs_q_mcp_ics_sp2_nn_cell_column_source * S ((S ((ff_column_mcp_prefix_ics_sp2_nn) + (1) * ff_index_mcp_ics_sp2_nn_cell_column)) * jc) + (ff_source_mcp_ics_sp2_nn_cell_column))) -> (((exists fs_h_mcp_ics_sp2_nn_cell_column_target. fs_h_mcp_ics_sp2_nn_cell_column_target + S (ff_target_mcp_ics_sp2_nn_cell_column) = S ((S (ff_index_mcp_ics_sp2_nn_cell_column)) * ff_right_scale_mcp_cell_ics_sp2_nn_cell)) /\ exists fs_q_mcp_ics_sp2_nn_cell_column_target. ff_right_mcp_cell_ics_sp2_nn_cell = fs_q_mcp_ics_sp2_nn_cell_column_target * S ((S (ff_index_mcp_ics_sp2_nn_cell_column)) * ff_right_scale_mcp_cell_ics_sp2_nn_cell) + (ff_target_mcp_ics_sp2_nn_cell_column))) -> ff_target_mcp_ics_sp2_nn_cell_column = ff_source_mcp_ics_sp2_nn_cell_column) /\ (exists ff_code_dot_mcp_ics_sp2_nn_cell_dot ff_scale_dot_mcp_ics_sp2_nn_cell_dot. ((forall fpmp_index_dot_mcp_ics_sp2_nn_cell_dot_pointwise fpmp_left_dot_mcp_ics_sp2_nn_cell_dot_pointwise fpmp_right_dot_mcp_ics_sp2_nn_cell_dot_pointwise fpmp_target_dot_mcp_ics_sp2_nn_cell_dot_pointwise. (exists fpmp_gap_dot_mcp_ics_sp2_nn_cell_dot_pointwise. fpmp_gap_dot_mcp_ics_sp2_nn_cell_dot_pointwise + S fpmp_index_dot_mcp_ics_sp2_nn_cell_dot_pointwise = w) -> (((exists ff_h_fpmp_dot_mcp_ics_sp2_nn_cell_dot_pointwise_left. ff_h_fpmp_dot_mcp_ics_sp2_nn_cell_dot_pointwise_left + S (fpmp_left_dot_mcp_ics_sp2_nn_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_sp2_nn_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_sp2_nn_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_sp2_nn_cell_dot_pointwise_left. ff_left_mcp_cell_ics_sp2_nn_cell = ff_q_fpmp_dot_mcp_ics_sp2_nn_cell_dot_pointwise_left * S ((S (fpmp_index_dot_mcp_ics_sp2_nn_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_sp2_nn_cell) + (fpmp_left_dot_mcp_ics_sp2_nn_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_sp2_nn_cell_dot_pointwise_right. ff_h_fpmp_dot_mcp_ics_sp2_nn_cell_dot_pointwise_right + S (fpmp_right_dot_mcp_ics_sp2_nn_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_sp2_nn_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_sp2_nn_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_sp2_nn_cell_dot_pointwise_right. ff_right_mcp_cell_ics_sp2_nn_cell = ff_q_fpmp_dot_mcp_ics_sp2_nn_cell_dot_pointwise_right * S ((S (fpmp_index_dot_mcp_ics_sp2_nn_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_sp2_nn_cell) + (fpmp_right_dot_mcp_ics_sp2_nn_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_sp2_nn_cell_dot_pointwise_target. ff_h_fpmp_dot_mcp_ics_sp2_nn_cell_dot_pointwise_target + S (fpmp_target_dot_mcp_ics_sp2_nn_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_sp2_nn_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_sp2_nn_cell_dot)) /\ exists ff_q_fpmp_dot_mcp_ics_sp2_nn_cell_dot_pointwise_target. ff_code_dot_mcp_ics_sp2_nn_cell_dot = ff_q_fpmp_dot_mcp_ics_sp2_nn_cell_dot_pointwise_target * S ((S (fpmp_index_dot_mcp_ics_sp2_nn_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_sp2_nn_cell_dot) + (fpmp_target_dot_mcp_ics_sp2_nn_cell_dot_pointwise))) -> fpmp_target_dot_mcp_ics_sp2_nn_cell_dot_pointwise = fpmp_left_dot_mcp_ics_sp2_nn_cell_dot_pointwise * fpmp_right_dot_mcp_ics_sp2_nn_cell_dot_pointwise) /\ (exists ff_u_dot_mcp_ics_sp2_nn_cell_dot_sum ff_v_dot_mcp_ics_sp2_nn_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_sp2_nn_cell_dot_sum_start. ff_h_dot_mcp_ics_sp2_nn_cell_dot_sum_start + S (0) = S ((S (0)) * ff_v_dot_mcp_ics_sp2_nn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_sp2_nn_cell_dot_sum_start. ff_u_dot_mcp_ics_sp2_nn_cell_dot_sum = ff_q_dot_mcp_ics_sp2_nn_cell_dot_sum_start * S ((S (0)) * ff_v_dot_mcp_ics_sp2_nn_cell_dot_sum) + (0))) /\ ((((exists ff_h_dot_mcp_ics_sp2_nn_cell_dot_sum_terminal. ff_h_dot_mcp_ics_sp2_nn_cell_dot_sum_terminal + S (ff_value_mcp_prefix_ics_sp2_nn) = S ((S (w)) * ff_v_dot_mcp_ics_sp2_nn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_sp2_nn_cell_dot_sum_terminal. ff_u_dot_mcp_ics_sp2_nn_cell_dot_sum = ff_q_dot_mcp_ics_sp2_nn_cell_dot_sum_terminal * S ((S (w)) * ff_v_dot_mcp_ics_sp2_nn_cell_dot_sum) + (ff_value_mcp_prefix_ics_sp2_nn))) /\ forall ff_i_dot_mcp_ics_sp2_nn_cell_dot_sum. (exists ff_lt_dot_mcp_ics_sp2_nn_cell_dot_sum_bound. ff_lt_dot_mcp_ics_sp2_nn_cell_dot_sum_bound + S ff_i_dot_mcp_ics_sp2_nn_cell_dot_sum = w) -> exists ff_a_dot_mcp_ics_sp2_nn_cell_dot_sum ff_r_dot_mcp_ics_sp2_nn_cell_dot_sum ff_s_dot_mcp_ics_sp2_nn_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_sp2_nn_cell_dot_sum_summand. ff_h_dot_mcp_ics_sp2_nn_cell_dot_sum_summand + S (ff_a_dot_mcp_ics_sp2_nn_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_sp2_nn_cell_dot_sum)) * ff_scale_dot_mcp_ics_sp2_nn_cell_dot)) /\ exists ff_q_dot_mcp_ics_sp2_nn_cell_dot_sum_summand. ff_code_dot_mcp_ics_sp2_nn_cell_dot = ff_q_dot_mcp_ics_sp2_nn_cell_dot_sum_summand * S ((S (ff_i_dot_mcp_ics_sp2_nn_cell_dot_sum)) * ff_scale_dot_mcp_ics_sp2_nn_cell_dot) + (ff_a_dot_mcp_ics_sp2_nn_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_sp2_nn_cell_dot_sum_partial. ff_h_dot_mcp_ics_sp2_nn_cell_dot_sum_partial + S (ff_r_dot_mcp_ics_sp2_nn_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_sp2_nn_cell_dot_sum)) * ff_v_dot_mcp_ics_sp2_nn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_sp2_nn_cell_dot_sum_partial. ff_u_dot_mcp_ics_sp2_nn_cell_dot_sum = ff_q_dot_mcp_ics_sp2_nn_cell_dot_sum_partial * S ((S (ff_i_dot_mcp_ics_sp2_nn_cell_dot_sum)) * ff_v_dot_mcp_ics_sp2_nn_cell_dot_sum) + (ff_r_dot_mcp_ics_sp2_nn_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_sp2_nn_cell_dot_sum_successor. ff_h_dot_mcp_ics_sp2_nn_cell_dot_sum_successor + S (ff_s_dot_mcp_ics_sp2_nn_cell_dot_sum) = S ((S (S ff_i_dot_mcp_ics_sp2_nn_cell_dot_sum)) * ff_v_dot_mcp_ics_sp2_nn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_sp2_nn_cell_dot_sum_successor. ff_u_dot_mcp_ics_sp2_nn_cell_dot_sum = ff_q_dot_mcp_ics_sp2_nn_cell_dot_sum_successor * S ((S (S ff_i_dot_mcp_ics_sp2_nn_cell_dot_sum)) * ff_v_dot_mcp_ics_sp2_nn_cell_dot_sum) + (ff_s_dot_mcp_ics_sp2_nn_cell_dot_sum))) /\ ff_s_dot_mcp_ics_sp2_nn_cell_dot_sum = ff_r_dot_mcp_ics_sp2_nn_cell_dot_sum + ff_a_dot_mcp_ics_sp2_nn_cell_dot_sum))))))))))) /\ (((exists fs_h_mcp_ics_sp2_nn_entry. fs_h_mcp_ics_sp2_nn_entry + S (ff_value_mcp_prefix_ics_sp2_nn) = S ((S (ff_index_mcp_prefix_ics_sp2_nn)) * ff_nns_mcp_smatrix_ics_sp2)) /\ exists fs_q_mcp_ics_sp2_nn_entry. ff_nn_mcp_smatrix_ics_sp2 = fs_q_mcp_ics_sp2_nn_entry * S ((S (ff_index_mcp_prefix_ics_sp2_nn)) * ff_nns_mcp_smatrix_ics_sp2) + (ff_value_mcp_prefix_ics_sp2_nn))))))) /\ ((forall ff_index_mcp_prefix_ics_sp2_pn. (exists mcp_gap_ics_sp2_pn_index. mcp_gap_ics_sp2_pn_index + S (ff_index_mcp_prefix_ics_sp2_pn) = ((r) * (1))) -> exists ff_row_mcp_prefix_ics_sp2_pn ff_column_mcp_prefix_ics_sp2_pn ff_value_mcp_prefix_ics_sp2_pn. ((ff_index_mcp_prefix_ics_sp2_pn) = (1) * ff_row_mcp_prefix_ics_sp2_pn + ff_column_mcp_prefix_ics_sp2_pn /\ ((exists mcp_gap_ics_sp2_pn_column. mcp_gap_ics_sp2_pn_column + S (ff_column_mcp_prefix_ics_sp2_pn) = (1)) /\ ((exists ff_left_mcp_cell_ics_sp2_pn_cell ff_left_scale_mcp_cell_ics_sp2_pn_cell ff_right_mcp_cell_ics_sp2_pn_cell ff_right_scale_mcp_cell_ics_sp2_pn_cell. ((forall ff_index_mcp_ics_sp2_pn_cell_row ff_source_mcp_ics_sp2_pn_cell_row ff_target_mcp_ics_sp2_pn_cell_row. (exists mcp_gap_ics_sp2_pn_cell_row_bound. mcp_gap_ics_sp2_pn_cell_row_bound + S (ff_index_mcp_ics_sp2_pn_cell_row) = (w)) -> (((exists fs_h_mcp_ics_sp2_pn_cell_row_source. fs_h_mcp_ics_sp2_pn_cell_row_source + S (ff_source_mcp_ics_sp2_pn_cell_row) = S ((S (((ff_row_mcp_prefix_ics_sp2_pn) * (w)) + (1) * ff_index_mcp_ics_sp2_pn_cell_row)) * ac)) /\ exists fs_q_mcp_ics_sp2_pn_cell_row_source. ab = fs_q_mcp_ics_sp2_pn_cell_row_source * S ((S (((ff_row_mcp_prefix_ics_sp2_pn) * (w)) + (1) * ff_index_mcp_ics_sp2_pn_cell_row)) * ac) + (ff_source_mcp_ics_sp2_pn_cell_row))) -> (((exists fs_h_mcp_ics_sp2_pn_cell_row_target. fs_h_mcp_ics_sp2_pn_cell_row_target + S (ff_target_mcp_ics_sp2_pn_cell_row) = S ((S (ff_index_mcp_ics_sp2_pn_cell_row)) * ff_left_scale_mcp_cell_ics_sp2_pn_cell)) /\ exists fs_q_mcp_ics_sp2_pn_cell_row_target. ff_left_mcp_cell_ics_sp2_pn_cell = fs_q_mcp_ics_sp2_pn_cell_row_target * S ((S (ff_index_mcp_ics_sp2_pn_cell_row)) * ff_left_scale_mcp_cell_ics_sp2_pn_cell) + (ff_target_mcp_ics_sp2_pn_cell_row))) -> ff_target_mcp_ics_sp2_pn_cell_row = ff_source_mcp_ics_sp2_pn_cell_row) /\ ((forall ff_index_mcp_ics_sp2_pn_cell_column ff_source_mcp_ics_sp2_pn_cell_column ff_target_mcp_ics_sp2_pn_cell_column. (exists mcp_gap_ics_sp2_pn_cell_column_bound. mcp_gap_ics_sp2_pn_cell_column_bound + S (ff_index_mcp_ics_sp2_pn_cell_column) = (w)) -> (((exists fs_h_mcp_ics_sp2_pn_cell_column_source. fs_h_mcp_ics_sp2_pn_cell_column_source + S (ff_source_mcp_ics_sp2_pn_cell_column) = S ((S ((ff_column_mcp_prefix_ics_sp2_pn) + (1) * ff_index_mcp_ics_sp2_pn_cell_column)) * jc)) /\ exists fs_q_mcp_ics_sp2_pn_cell_column_source. jb = fs_q_mcp_ics_sp2_pn_cell_column_source * S ((S ((ff_column_mcp_prefix_ics_sp2_pn) + (1) * ff_index_mcp_ics_sp2_pn_cell_column)) * jc) + (ff_source_mcp_ics_sp2_pn_cell_column))) -> (((exists fs_h_mcp_ics_sp2_pn_cell_column_target. fs_h_mcp_ics_sp2_pn_cell_column_target + S (ff_target_mcp_ics_sp2_pn_cell_column) = S ((S (ff_index_mcp_ics_sp2_pn_cell_column)) * ff_right_scale_mcp_cell_ics_sp2_pn_cell)) /\ exists fs_q_mcp_ics_sp2_pn_cell_column_target. ff_right_mcp_cell_ics_sp2_pn_cell = fs_q_mcp_ics_sp2_pn_cell_column_target * S ((S (ff_index_mcp_ics_sp2_pn_cell_column)) * ff_right_scale_mcp_cell_ics_sp2_pn_cell) + (ff_target_mcp_ics_sp2_pn_cell_column))) -> ff_target_mcp_ics_sp2_pn_cell_column = ff_source_mcp_ics_sp2_pn_cell_column) /\ (exists ff_code_dot_mcp_ics_sp2_pn_cell_dot ff_scale_dot_mcp_ics_sp2_pn_cell_dot. ((forall fpmp_index_dot_mcp_ics_sp2_pn_cell_dot_pointwise fpmp_left_dot_mcp_ics_sp2_pn_cell_dot_pointwise fpmp_right_dot_mcp_ics_sp2_pn_cell_dot_pointwise fpmp_target_dot_mcp_ics_sp2_pn_cell_dot_pointwise. (exists fpmp_gap_dot_mcp_ics_sp2_pn_cell_dot_pointwise. fpmp_gap_dot_mcp_ics_sp2_pn_cell_dot_pointwise + S fpmp_index_dot_mcp_ics_sp2_pn_cell_dot_pointwise = w) -> (((exists ff_h_fpmp_dot_mcp_ics_sp2_pn_cell_dot_pointwise_left. ff_h_fpmp_dot_mcp_ics_sp2_pn_cell_dot_pointwise_left + S (fpmp_left_dot_mcp_ics_sp2_pn_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_sp2_pn_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_sp2_pn_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_sp2_pn_cell_dot_pointwise_left. ff_left_mcp_cell_ics_sp2_pn_cell = ff_q_fpmp_dot_mcp_ics_sp2_pn_cell_dot_pointwise_left * S ((S (fpmp_index_dot_mcp_ics_sp2_pn_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_sp2_pn_cell) + (fpmp_left_dot_mcp_ics_sp2_pn_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_sp2_pn_cell_dot_pointwise_right. ff_h_fpmp_dot_mcp_ics_sp2_pn_cell_dot_pointwise_right + S (fpmp_right_dot_mcp_ics_sp2_pn_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_sp2_pn_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_sp2_pn_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_sp2_pn_cell_dot_pointwise_right. ff_right_mcp_cell_ics_sp2_pn_cell = ff_q_fpmp_dot_mcp_ics_sp2_pn_cell_dot_pointwise_right * S ((S (fpmp_index_dot_mcp_ics_sp2_pn_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_sp2_pn_cell) + (fpmp_right_dot_mcp_ics_sp2_pn_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_sp2_pn_cell_dot_pointwise_target. ff_h_fpmp_dot_mcp_ics_sp2_pn_cell_dot_pointwise_target + S (fpmp_target_dot_mcp_ics_sp2_pn_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_sp2_pn_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_sp2_pn_cell_dot)) /\ exists ff_q_fpmp_dot_mcp_ics_sp2_pn_cell_dot_pointwise_target. ff_code_dot_mcp_ics_sp2_pn_cell_dot = ff_q_fpmp_dot_mcp_ics_sp2_pn_cell_dot_pointwise_target * S ((S (fpmp_index_dot_mcp_ics_sp2_pn_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_sp2_pn_cell_dot) + (fpmp_target_dot_mcp_ics_sp2_pn_cell_dot_pointwise))) -> fpmp_target_dot_mcp_ics_sp2_pn_cell_dot_pointwise = fpmp_left_dot_mcp_ics_sp2_pn_cell_dot_pointwise * fpmp_right_dot_mcp_ics_sp2_pn_cell_dot_pointwise) /\ (exists ff_u_dot_mcp_ics_sp2_pn_cell_dot_sum ff_v_dot_mcp_ics_sp2_pn_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_sp2_pn_cell_dot_sum_start. ff_h_dot_mcp_ics_sp2_pn_cell_dot_sum_start + S (0) = S ((S (0)) * ff_v_dot_mcp_ics_sp2_pn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_sp2_pn_cell_dot_sum_start. ff_u_dot_mcp_ics_sp2_pn_cell_dot_sum = ff_q_dot_mcp_ics_sp2_pn_cell_dot_sum_start * S ((S (0)) * ff_v_dot_mcp_ics_sp2_pn_cell_dot_sum) + (0))) /\ ((((exists ff_h_dot_mcp_ics_sp2_pn_cell_dot_sum_terminal. ff_h_dot_mcp_ics_sp2_pn_cell_dot_sum_terminal + S (ff_value_mcp_prefix_ics_sp2_pn) = S ((S (w)) * ff_v_dot_mcp_ics_sp2_pn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_sp2_pn_cell_dot_sum_terminal. ff_u_dot_mcp_ics_sp2_pn_cell_dot_sum = ff_q_dot_mcp_ics_sp2_pn_cell_dot_sum_terminal * S ((S (w)) * ff_v_dot_mcp_ics_sp2_pn_cell_dot_sum) + (ff_value_mcp_prefix_ics_sp2_pn))) /\ forall ff_i_dot_mcp_ics_sp2_pn_cell_dot_sum. (exists ff_lt_dot_mcp_ics_sp2_pn_cell_dot_sum_bound. ff_lt_dot_mcp_ics_sp2_pn_cell_dot_sum_bound + S ff_i_dot_mcp_ics_sp2_pn_cell_dot_sum = w) -> exists ff_a_dot_mcp_ics_sp2_pn_cell_dot_sum ff_r_dot_mcp_ics_sp2_pn_cell_dot_sum ff_s_dot_mcp_ics_sp2_pn_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_sp2_pn_cell_dot_sum_summand. ff_h_dot_mcp_ics_sp2_pn_cell_dot_sum_summand + S (ff_a_dot_mcp_ics_sp2_pn_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_sp2_pn_cell_dot_sum)) * ff_scale_dot_mcp_ics_sp2_pn_cell_dot)) /\ exists ff_q_dot_mcp_ics_sp2_pn_cell_dot_sum_summand. ff_code_dot_mcp_ics_sp2_pn_cell_dot = ff_q_dot_mcp_ics_sp2_pn_cell_dot_sum_summand * S ((S (ff_i_dot_mcp_ics_sp2_pn_cell_dot_sum)) * ff_scale_dot_mcp_ics_sp2_pn_cell_dot) + (ff_a_dot_mcp_ics_sp2_pn_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_sp2_pn_cell_dot_sum_partial. ff_h_dot_mcp_ics_sp2_pn_cell_dot_sum_partial + S (ff_r_dot_mcp_ics_sp2_pn_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_sp2_pn_cell_dot_sum)) * ff_v_dot_mcp_ics_sp2_pn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_sp2_pn_cell_dot_sum_partial. ff_u_dot_mcp_ics_sp2_pn_cell_dot_sum = ff_q_dot_mcp_ics_sp2_pn_cell_dot_sum_partial * S ((S (ff_i_dot_mcp_ics_sp2_pn_cell_dot_sum)) * ff_v_dot_mcp_ics_sp2_pn_cell_dot_sum) + (ff_r_dot_mcp_ics_sp2_pn_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_sp2_pn_cell_dot_sum_successor. ff_h_dot_mcp_ics_sp2_pn_cell_dot_sum_successor + S (ff_s_dot_mcp_ics_sp2_pn_cell_dot_sum) = S ((S (S ff_i_dot_mcp_ics_sp2_pn_cell_dot_sum)) * ff_v_dot_mcp_ics_sp2_pn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_sp2_pn_cell_dot_sum_successor. ff_u_dot_mcp_ics_sp2_pn_cell_dot_sum = ff_q_dot_mcp_ics_sp2_pn_cell_dot_sum_successor * S ((S (S ff_i_dot_mcp_ics_sp2_pn_cell_dot_sum)) * ff_v_dot_mcp_ics_sp2_pn_cell_dot_sum) + (ff_s_dot_mcp_ics_sp2_pn_cell_dot_sum))) /\ ff_s_dot_mcp_ics_sp2_pn_cell_dot_sum = ff_r_dot_mcp_ics_sp2_pn_cell_dot_sum + ff_a_dot_mcp_ics_sp2_pn_cell_dot_sum))))))))))) /\ (((exists fs_h_mcp_ics_sp2_pn_entry. fs_h_mcp_ics_sp2_pn_entry + S (ff_value_mcp_prefix_ics_sp2_pn) = S ((S (ff_index_mcp_prefix_ics_sp2_pn)) * ff_pns_mcp_smatrix_ics_sp2)) /\ exists fs_q_mcp_ics_sp2_pn_entry. ff_pn_mcp_smatrix_ics_sp2 = fs_q_mcp_ics_sp2_pn_entry * S ((S (ff_index_mcp_prefix_ics_sp2_pn)) * ff_pns_mcp_smatrix_ics_sp2) + (ff_value_mcp_prefix_ics_sp2_pn))))))) /\ ((forall ff_index_mcp_prefix_ics_sp2_np. (exists mcp_gap_ics_sp2_np_index. mcp_gap_ics_sp2_np_index + S (ff_index_mcp_prefix_ics_sp2_np) = ((r) * (1))) -> exists ff_row_mcp_prefix_ics_sp2_np ff_column_mcp_prefix_ics_sp2_np ff_value_mcp_prefix_ics_sp2_np. ((ff_index_mcp_prefix_ics_sp2_np) = (1) * ff_row_mcp_prefix_ics_sp2_np + ff_column_mcp_prefix_ics_sp2_np /\ ((exists mcp_gap_ics_sp2_np_column. mcp_gap_ics_sp2_np_column + S (ff_column_mcp_prefix_ics_sp2_np) = (1)) /\ ((exists ff_left_mcp_cell_ics_sp2_np_cell ff_left_scale_mcp_cell_ics_sp2_np_cell ff_right_mcp_cell_ics_sp2_np_cell ff_right_scale_mcp_cell_ics_sp2_np_cell. ((forall ff_index_mcp_ics_sp2_np_cell_row ff_source_mcp_ics_sp2_np_cell_row ff_target_mcp_ics_sp2_np_cell_row. (exists mcp_gap_ics_sp2_np_cell_row_bound. mcp_gap_ics_sp2_np_cell_row_bound + S (ff_index_mcp_ics_sp2_np_cell_row) = (w)) -> (((exists fs_h_mcp_ics_sp2_np_cell_row_source. fs_h_mcp_ics_sp2_np_cell_row_source + S (ff_source_mcp_ics_sp2_np_cell_row) = S ((S (((ff_row_mcp_prefix_ics_sp2_np) * (w)) + (1) * ff_index_mcp_ics_sp2_np_cell_row)) * dc)) /\ exists fs_q_mcp_ics_sp2_np_cell_row_source. db = fs_q_mcp_ics_sp2_np_cell_row_source * S ((S (((ff_row_mcp_prefix_ics_sp2_np) * (w)) + (1) * ff_index_mcp_ics_sp2_np_cell_row)) * dc) + (ff_source_mcp_ics_sp2_np_cell_row))) -> (((exists fs_h_mcp_ics_sp2_np_cell_row_target. fs_h_mcp_ics_sp2_np_cell_row_target + S (ff_target_mcp_ics_sp2_np_cell_row) = S ((S (ff_index_mcp_ics_sp2_np_cell_row)) * ff_left_scale_mcp_cell_ics_sp2_np_cell)) /\ exists fs_q_mcp_ics_sp2_np_cell_row_target. ff_left_mcp_cell_ics_sp2_np_cell = fs_q_mcp_ics_sp2_np_cell_row_target * S ((S (ff_index_mcp_ics_sp2_np_cell_row)) * ff_left_scale_mcp_cell_ics_sp2_np_cell) + (ff_target_mcp_ics_sp2_np_cell_row))) -> ff_target_mcp_ics_sp2_np_cell_row = ff_source_mcp_ics_sp2_np_cell_row) /\ ((forall ff_index_mcp_ics_sp2_np_cell_column ff_source_mcp_ics_sp2_np_cell_column ff_target_mcp_ics_sp2_np_cell_column. (exists mcp_gap_ics_sp2_np_cell_column_bound. mcp_gap_ics_sp2_np_cell_column_bound + S (ff_index_mcp_ics_sp2_np_cell_column) = (w)) -> (((exists fs_h_mcp_ics_sp2_np_cell_column_source. fs_h_mcp_ics_sp2_np_cell_column_source + S (ff_source_mcp_ics_sp2_np_cell_column) = S ((S ((ff_column_mcp_prefix_ics_sp2_np) + (1) * ff_index_mcp_ics_sp2_np_cell_column)) * ic)) /\ exists fs_q_mcp_ics_sp2_np_cell_column_source. ib = fs_q_mcp_ics_sp2_np_cell_column_source * S ((S ((ff_column_mcp_prefix_ics_sp2_np) + (1) * ff_index_mcp_ics_sp2_np_cell_column)) * ic) + (ff_source_mcp_ics_sp2_np_cell_column))) -> (((exists fs_h_mcp_ics_sp2_np_cell_column_target. fs_h_mcp_ics_sp2_np_cell_column_target + S (ff_target_mcp_ics_sp2_np_cell_column) = S ((S (ff_index_mcp_ics_sp2_np_cell_column)) * ff_right_scale_mcp_cell_ics_sp2_np_cell)) /\ exists fs_q_mcp_ics_sp2_np_cell_column_target. ff_right_mcp_cell_ics_sp2_np_cell = fs_q_mcp_ics_sp2_np_cell_column_target * S ((S (ff_index_mcp_ics_sp2_np_cell_column)) * ff_right_scale_mcp_cell_ics_sp2_np_cell) + (ff_target_mcp_ics_sp2_np_cell_column))) -> ff_target_mcp_ics_sp2_np_cell_column = ff_source_mcp_ics_sp2_np_cell_column) /\ (exists ff_code_dot_mcp_ics_sp2_np_cell_dot ff_scale_dot_mcp_ics_sp2_np_cell_dot. ((forall fpmp_index_dot_mcp_ics_sp2_np_cell_dot_pointwise fpmp_left_dot_mcp_ics_sp2_np_cell_dot_pointwise fpmp_right_dot_mcp_ics_sp2_np_cell_dot_pointwise fpmp_target_dot_mcp_ics_sp2_np_cell_dot_pointwise. (exists fpmp_gap_dot_mcp_ics_sp2_np_cell_dot_pointwise. fpmp_gap_dot_mcp_ics_sp2_np_cell_dot_pointwise + S fpmp_index_dot_mcp_ics_sp2_np_cell_dot_pointwise = w) -> (((exists ff_h_fpmp_dot_mcp_ics_sp2_np_cell_dot_pointwise_left. ff_h_fpmp_dot_mcp_ics_sp2_np_cell_dot_pointwise_left + S (fpmp_left_dot_mcp_ics_sp2_np_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_sp2_np_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_sp2_np_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_sp2_np_cell_dot_pointwise_left. ff_left_mcp_cell_ics_sp2_np_cell = ff_q_fpmp_dot_mcp_ics_sp2_np_cell_dot_pointwise_left * S ((S (fpmp_index_dot_mcp_ics_sp2_np_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_sp2_np_cell) + (fpmp_left_dot_mcp_ics_sp2_np_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_sp2_np_cell_dot_pointwise_right. ff_h_fpmp_dot_mcp_ics_sp2_np_cell_dot_pointwise_right + S (fpmp_right_dot_mcp_ics_sp2_np_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_sp2_np_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_sp2_np_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_sp2_np_cell_dot_pointwise_right. ff_right_mcp_cell_ics_sp2_np_cell = ff_q_fpmp_dot_mcp_ics_sp2_np_cell_dot_pointwise_right * S ((S (fpmp_index_dot_mcp_ics_sp2_np_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_sp2_np_cell) + (fpmp_right_dot_mcp_ics_sp2_np_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_sp2_np_cell_dot_pointwise_target. ff_h_fpmp_dot_mcp_ics_sp2_np_cell_dot_pointwise_target + S (fpmp_target_dot_mcp_ics_sp2_np_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_sp2_np_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_sp2_np_cell_dot)) /\ exists ff_q_fpmp_dot_mcp_ics_sp2_np_cell_dot_pointwise_target. ff_code_dot_mcp_ics_sp2_np_cell_dot = ff_q_fpmp_dot_mcp_ics_sp2_np_cell_dot_pointwise_target * S ((S (fpmp_index_dot_mcp_ics_sp2_np_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_sp2_np_cell_dot) + (fpmp_target_dot_mcp_ics_sp2_np_cell_dot_pointwise))) -> fpmp_target_dot_mcp_ics_sp2_np_cell_dot_pointwise = fpmp_left_dot_mcp_ics_sp2_np_cell_dot_pointwise * fpmp_right_dot_mcp_ics_sp2_np_cell_dot_pointwise) /\ (exists ff_u_dot_mcp_ics_sp2_np_cell_dot_sum ff_v_dot_mcp_ics_sp2_np_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_sp2_np_cell_dot_sum_start. ff_h_dot_mcp_ics_sp2_np_cell_dot_sum_start + S (0) = S ((S (0)) * ff_v_dot_mcp_ics_sp2_np_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_sp2_np_cell_dot_sum_start. ff_u_dot_mcp_ics_sp2_np_cell_dot_sum = ff_q_dot_mcp_ics_sp2_np_cell_dot_sum_start * S ((S (0)) * ff_v_dot_mcp_ics_sp2_np_cell_dot_sum) + (0))) /\ ((((exists ff_h_dot_mcp_ics_sp2_np_cell_dot_sum_terminal. ff_h_dot_mcp_ics_sp2_np_cell_dot_sum_terminal + S (ff_value_mcp_prefix_ics_sp2_np) = S ((S (w)) * ff_v_dot_mcp_ics_sp2_np_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_sp2_np_cell_dot_sum_terminal. ff_u_dot_mcp_ics_sp2_np_cell_dot_sum = ff_q_dot_mcp_ics_sp2_np_cell_dot_sum_terminal * S ((S (w)) * ff_v_dot_mcp_ics_sp2_np_cell_dot_sum) + (ff_value_mcp_prefix_ics_sp2_np))) /\ forall ff_i_dot_mcp_ics_sp2_np_cell_dot_sum. (exists ff_lt_dot_mcp_ics_sp2_np_cell_dot_sum_bound. ff_lt_dot_mcp_ics_sp2_np_cell_dot_sum_bound + S ff_i_dot_mcp_ics_sp2_np_cell_dot_sum = w) -> exists ff_a_dot_mcp_ics_sp2_np_cell_dot_sum ff_r_dot_mcp_ics_sp2_np_cell_dot_sum ff_s_dot_mcp_ics_sp2_np_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_sp2_np_cell_dot_sum_summand. ff_h_dot_mcp_ics_sp2_np_cell_dot_sum_summand + S (ff_a_dot_mcp_ics_sp2_np_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_sp2_np_cell_dot_sum)) * ff_scale_dot_mcp_ics_sp2_np_cell_dot)) /\ exists ff_q_dot_mcp_ics_sp2_np_cell_dot_sum_summand. ff_code_dot_mcp_ics_sp2_np_cell_dot = ff_q_dot_mcp_ics_sp2_np_cell_dot_sum_summand * S ((S (ff_i_dot_mcp_ics_sp2_np_cell_dot_sum)) * ff_scale_dot_mcp_ics_sp2_np_cell_dot) + (ff_a_dot_mcp_ics_sp2_np_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_sp2_np_cell_dot_sum_partial. ff_h_dot_mcp_ics_sp2_np_cell_dot_sum_partial + S (ff_r_dot_mcp_ics_sp2_np_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_sp2_np_cell_dot_sum)) * ff_v_dot_mcp_ics_sp2_np_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_sp2_np_cell_dot_sum_partial. ff_u_dot_mcp_ics_sp2_np_cell_dot_sum = ff_q_dot_mcp_ics_sp2_np_cell_dot_sum_partial * S ((S (ff_i_dot_mcp_ics_sp2_np_cell_dot_sum)) * ff_v_dot_mcp_ics_sp2_np_cell_dot_sum) + (ff_r_dot_mcp_ics_sp2_np_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_sp2_np_cell_dot_sum_successor. ff_h_dot_mcp_ics_sp2_np_cell_dot_sum_successor + S (ff_s_dot_mcp_ics_sp2_np_cell_dot_sum) = S ((S (S ff_i_dot_mcp_ics_sp2_np_cell_dot_sum)) * ff_v_dot_mcp_ics_sp2_np_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_sp2_np_cell_dot_sum_successor. ff_u_dot_mcp_ics_sp2_np_cell_dot_sum = ff_q_dot_mcp_ics_sp2_np_cell_dot_sum_successor * S ((S (S ff_i_dot_mcp_ics_sp2_np_cell_dot_sum)) * ff_v_dot_mcp_ics_sp2_np_cell_dot_sum) + (ff_s_dot_mcp_ics_sp2_np_cell_dot_sum))) /\ ff_s_dot_mcp_ics_sp2_np_cell_dot_sum = ff_r_dot_mcp_ics_sp2_np_cell_dot_sum + ff_a_dot_mcp_ics_sp2_np_cell_dot_sum))))))))))) /\ (((exists fs_h_mcp_ics_sp2_np_entry. fs_h_mcp_ics_sp2_np_entry + S (ff_value_mcp_prefix_ics_sp2_np) = S ((S (ff_index_mcp_prefix_ics_sp2_np)) * ff_nps_mcp_smatrix_ics_sp2)) /\ exists fs_q_mcp_ics_sp2_np_entry. ff_np_mcp_smatrix_ics_sp2 = fs_q_mcp_ics_sp2_np_entry * S ((S (ff_index_mcp_prefix_ics_sp2_np)) * ff_nps_mcp_smatrix_ics_sp2) + (ff_value_mcp_prefix_ics_sp2_np))))))) /\ ((forall ff_index_mcp_add_ics_sp2_positive ff_left_mcp_add_ics_sp2_positive ff_right_mcp_add_ics_sp2_positive ff_target_mcp_add_ics_sp2_positive. (exists mcp_gap_ics_sp2_positive_bound. mcp_gap_ics_sp2_positive_bound + S (ff_index_mcp_add_ics_sp2_positive) = ((r) * (1))) -> (((exists fs_h_mcp_ics_sp2_positive_left. fs_h_mcp_ics_sp2_positive_left + S (ff_left_mcp_add_ics_sp2_positive) = S ((S (ff_index_mcp_add_ics_sp2_positive)) * ff_pps_mcp_smatrix_ics_sp2)) /\ exists fs_q_mcp_ics_sp2_positive_left. ff_pp_mcp_smatrix_ics_sp2 = fs_q_mcp_ics_sp2_positive_left * S ((S (ff_index_mcp_add_ics_sp2_positive)) * ff_pps_mcp_smatrix_ics_sp2) + (ff_left_mcp_add_ics_sp2_positive))) -> (((exists fs_h_mcp_ics_sp2_positive_right. fs_h_mcp_ics_sp2_positive_right + S (ff_right_mcp_add_ics_sp2_positive) = S ((S (ff_index_mcp_add_ics_sp2_positive)) * ff_nns_mcp_smatrix_ics_sp2)) /\ exists fs_q_mcp_ics_sp2_positive_right. ff_nn_mcp_smatrix_ics_sp2 = fs_q_mcp_ics_sp2_positive_right * S ((S (ff_index_mcp_add_ics_sp2_positive)) * ff_nns_mcp_smatrix_ics_sp2) + (ff_right_mcp_add_ics_sp2_positive))) -> (((exists fs_h_mcp_ics_sp2_positive_target. fs_h_mcp_ics_sp2_positive_target + S (ff_target_mcp_add_ics_sp2_positive) = S ((S (ff_index_mcp_add_ics_sp2_positive)) * rc)) /\ exists fs_q_mcp_ics_sp2_positive_target. rb = fs_q_mcp_ics_sp2_positive_target * S ((S (ff_index_mcp_add_ics_sp2_positive)) * rc) + (ff_target_mcp_add_ics_sp2_positive))) -> ff_target_mcp_add_ics_sp2_positive = ff_left_mcp_add_ics_sp2_positive + ff_right_mcp_add_ics_sp2_positive) /\ (forall ff_index_mcp_add_ics_sp2_negative ff_left_mcp_add_ics_sp2_negative ff_right_mcp_add_ics_sp2_negative ff_target_mcp_add_ics_sp2_negative. (exists mcp_gap_ics_sp2_negative_bound. mcp_gap_ics_sp2_negative_bound + S (ff_index_mcp_add_ics_sp2_negative) = ((r) * (1))) -> (((exists fs_h_mcp_ics_sp2_negative_left. fs_h_mcp_ics_sp2_negative_left + S (ff_left_mcp_add_ics_sp2_negative) = S ((S (ff_index_mcp_add_ics_sp2_negative)) * ff_pns_mcp_smatrix_ics_sp2)) /\ exists fs_q_mcp_ics_sp2_negative_left. ff_pn_mcp_smatrix_ics_sp2 = fs_q_mcp_ics_sp2_negative_left * S ((S (ff_index_mcp_add_ics_sp2_negative)) * ff_pns_mcp_smatrix_ics_sp2) + (ff_left_mcp_add_ics_sp2_negative))) -> (((exists fs_h_mcp_ics_sp2_negative_right. fs_h_mcp_ics_sp2_negative_right + S (ff_right_mcp_add_ics_sp2_negative) = S ((S (ff_index_mcp_add_ics_sp2_negative)) * ff_nps_mcp_smatrix_ics_sp2)) /\ exists fs_q_mcp_ics_sp2_negative_right. ff_np_mcp_smatrix_ics_sp2 = fs_q_mcp_ics_sp2_negative_right * S ((S (ff_index_mcp_add_ics_sp2_negative)) * ff_nps_mcp_smatrix_ics_sp2) + (ff_right_mcp_add_ics_sp2_negative))) -> (((exists fs_h_mcp_ics_sp2_negative_target. fs_h_mcp_ics_sp2_negative_target + S (ff_target_mcp_add_ics_sp2_negative) = S ((S (ff_index_mcp_add_ics_sp2_negative)) * sc)) /\ exists fs_q_mcp_ics_sp2_negative_target. sb = fs_q_mcp_ics_sp2_negative_target * S ((S (ff_index_mcp_add_ics_sp2_negative)) * sc) + (ff_target_mcp_add_ics_sp2_negative))) -> ff_target_mcp_add_ics_sp2_negative = ff_left_mcp_add_ics_sp2_negative + ff_right_mcp_add_ics_sp2_negative))))))) -> ((forall ff_index_mcp_add_ics_sp_output_p ff_left_mcp_add_ics_sp_output_p ff_right_mcp_add_ics_sp_output_p ff_target_mcp_add_ics_sp_output_p. (exists mcp_gap_ics_sp_output_p_bound. mcp_gap_ics_sp_output_p_bound + S (ff_index_mcp_add_ics_sp_output_p) = (r * 1)) -> (((exists fs_h_mcp_ics_sp_output_p_left. fs_h_mcp_ics_sp_output_p_left + S (ff_left_mcp_add_ics_sp_output_p) = S ((S (ff_index_mcp_add_ics_sp_output_p)) * pc)) /\ exists fs_q_mcp_ics_sp_output_p_left. pb = fs_q_mcp_ics_sp_output_p_left * S ((S (ff_index_mcp_add_ics_sp_output_p)) * pc) + (ff_left_mcp_add_ics_sp_output_p))) -> (((exists fs_h_mcp_ics_sp_output_p_right. fs_h_mcp_ics_sp_output_p_right + S (ff_right_mcp_add_ics_sp_output_p) = S ((S (ff_index_mcp_add_ics_sp_output_p)) * qc)) /\ exists fs_q_mcp_ics_sp_output_p_right. qb = fs_q_mcp_ics_sp_output_p_right * S ((S (ff_index_mcp_add_ics_sp_output_p)) * qc) + (ff_right_mcp_add_ics_sp_output_p))) -> (((exists fs_h_mcp_ics_sp_output_p_target. fs_h_mcp_ics_sp_output_p_target + S (ff_target_mcp_add_ics_sp_output_p) = S ((S (ff_index_mcp_add_ics_sp_output_p)) * rc)) /\ exists fs_q_mcp_ics_sp_output_p_target. rb = fs_q_mcp_ics_sp_output_p_target * S ((S (ff_index_mcp_add_ics_sp_output_p)) * rc) + (ff_target_mcp_add_ics_sp_output_p))) -> ff_target_mcp_add_ics_sp_output_p = ff_left_mcp_add_ics_sp_output_p + ff_right_mcp_add_ics_sp_output_p) /\ (forall ff_index_mcp_add_ics_sp_output_n ff_left_mcp_add_ics_sp_output_n ff_right_mcp_add_ics_sp_output_n ff_target_mcp_add_ics_sp_output_n. (exists mcp_gap_ics_sp_output_n_bound. mcp_gap_ics_sp_output_n_bound + S (ff_index_mcp_add_ics_sp_output_n) = (r * 1)) -> (((exists fs_h_mcp_ics_sp_output_n_left. fs_h_mcp_ics_sp_output_n_left + S (ff_left_mcp_add_ics_sp_output_n) = S ((S (ff_index_mcp_add_ics_sp_output_n)) * nc)) /\ exists fs_q_mcp_ics_sp_output_n_left. nb = fs_q_mcp_ics_sp_output_n_left * S ((S (ff_index_mcp_add_ics_sp_output_n)) * nc) + (ff_left_mcp_add_ics_sp_output_n))) -> (((exists fs_h_mcp_ics_sp_output_n_right. fs_h_mcp_ics_sp_output_n_right + S (ff_right_mcp_add_ics_sp_output_n) = S ((S (ff_index_mcp_add_ics_sp_output_n)) * mc)) /\ exists fs_q_mcp_ics_sp_output_n_right. mb = fs_q_mcp_ics_sp_output_n_right * S ((S (ff_index_mcp_add_ics_sp_output_n)) * mc) + (ff_right_mcp_add_ics_sp_output_n))) -> (((exists fs_h_mcp_ics_sp_output_n_target. fs_h_mcp_ics_sp_output_n_target + S (ff_target_mcp_add_ics_sp_output_n) = S ((S (ff_index_mcp_add_ics_sp_output_n)) * sc)) /\ exists fs_q_mcp_ics_sp_output_n_target. sb = fs_q_mcp_ics_sp_output_n_target * S ((S (ff_index_mcp_add_ics_sp_output_n)) * sc) + (ff_target_mcp_add_ics_sp_output_n))) -> ff_target_mcp_add_ics_sp_output_n = ff_left_mcp_add_ics_sp_output_n + ff_right_mcp_add_ics_sp_output_n))Constructive proof overview
Generated structural guide
The actual signed coded matrix product is componentwise additive in actual componentwise coefficient sums, by all four proved natural matrix-vector products and exact pointwise regrouping.
The unchanged tactic script uses 2 declared prerequisites and contains 213 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 (2)
01Fix variables and assumptionsL1–10
02Fix variables and assumptionsL11–20
03Fix variables and assumptionsL21–30
04Fix variables and assumptionsL31–35
05Separate the logical casesL36–45
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L36
cases hfirst - L37
cases hfirst_witness - L38
cases hfirst_witness_witness - L39
cases hfirst_witness_witness_witness - L40
cases hfirst_witness_witness_witness_witness - L41
cases hfirst_witness_witness_witness_witness_witness - L42
cases hfirst_witness_witness_witness_witness_witness_witness - L43
cases hfirst_witness_witness_witness_witness_witness_witness_witness - L44
cases hfirst_witness_witness_witness_witness_witness_witness_witness_witness - L45
cases hfirst_witness_witness_witness_witness_witness_witness_witness_witness_right
06Separate the logical casesL46–55
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L46
cases hfirst_witness_witness_witness_witness_witness_witness_witness_witness_right_right - L47
cases hfirst_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right - L48
cases hfirst_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_right - L49
cases hsecond - L50
cases hsecond_witness - L51
cases hsecond_witness_witness - L52
cases hsecond_witness_witness_witness - L53
cases hsecond_witness_witness_witness_witness - L54
cases hsecond_witness_witness_witness_witness_witness - L55
cases hsecond_witness_witness_witness_witness_witness_witness
07Separate the logical casesL56–65
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L56
cases hsecond_witness_witness_witness_witness_witness_witness_witness - L57
cases hsecond_witness_witness_witness_witness_witness_witness_witness_witness - L58
cases hsecond_witness_witness_witness_witness_witness_witness_witness_witness_right - L59
cases hsecond_witness_witness_witness_witness_witness_witness_witness_witness_right_right - L60
cases hsecond_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right - L61
cases hsecond_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_right - L62
cases hthird - L63
cases hthird_witness - L64
cases hthird_witness_witness - L65
cases hthird_witness_witness_witness
08Separate the logical casesL66–74
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L66
cases hthird_witness_witness_witness_witness - L67
cases hthird_witness_witness_witness_witness_witness - L68
cases hthird_witness_witness_witness_witness_witness_witness - L69
cases hthird_witness_witness_witness_witness_witness_witness_witness - L70
cases hthird_witness_witness_witness_witness_witness_witness_witness_witness - L71
cases hthird_witness_witness_witness_witness_witness_witness_witness_witness_right - L72
cases hthird_witness_witness_witness_witness_witness_witness_witness_witness_right_right - L73
cases hthird_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right - L74
cases hthird_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_right
09Establish hnew0L75–84
Establish this local claim before using it. It is not an additional assumption.
- L75
have hnew0 : MatrixPointwiseAdd(x,x1,x8,x9,x16,x17,r · 1)Definitions: MatrixPointwiseAdd - L76
specialize integer_span_natural_product_add_right (ab) - L77
specialize integer_span_natural_product_add_right (ac) - L78
specialize integer_span_natural_product_add_right (eb) - L79
specialize integer_span_natural_product_add_right (ec) - L80
specialize integer_span_natural_product_add_right (gb) - L81
specialize integer_span_natural_product_add_right (gc) - L82
specialize integer_span_natural_product_add_right (ib) - L83
specialize integer_span_natural_product_add_right (ic) - L84
specialize integer_span_natural_product_add_right (w)
10Use earlier factsL85–94
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L85
specialize integer_span_natural_product_add_right (x) - L86
specialize integer_span_natural_product_add_right (x1) - L87
specialize integer_span_natural_product_add_right (x8) - L88
specialize integer_span_natural_product_add_right (x9) - L89
specialize integer_span_natural_product_add_right (x16) - L90
specialize integer_span_natural_product_add_right (x17) - L91
specialize integer_span_natural_product_add_right (r * 1) - L92
apply integer_span_natural_product_add_right - L93
exact haddp - L94
exact hfirst_witness_witness_witness_witness_witness_witness_witness_witness_left
11Use earlier factsL95–96
12Establish hnew1L97–106
Establish this local claim before using it. It is not an additional assumption.
- L97
have hnew1 : MatrixPointwiseAdd(x2,x3,x10,x11,x18,x19,r · 1)Definitions: MatrixPointwiseAdd - L98
specialize integer_span_natural_product_add_right (db) - L99
specialize integer_span_natural_product_add_right (dc) - L100
specialize integer_span_natural_product_add_right (fb) - L101
specialize integer_span_natural_product_add_right (fc) - L102
specialize integer_span_natural_product_add_right (hb) - L103
specialize integer_span_natural_product_add_right (hc) - L104
specialize integer_span_natural_product_add_right (jb) - L105
specialize integer_span_natural_product_add_right (jc) - L106
specialize integer_span_natural_product_add_right (w)
13Use earlier factsL107–116
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L107
specialize integer_span_natural_product_add_right (x2) - L108
specialize integer_span_natural_product_add_right (x3) - L109
specialize integer_span_natural_product_add_right (x10) - L110
specialize integer_span_natural_product_add_right (x11) - L111
specialize integer_span_natural_product_add_right (x18) - L112
specialize integer_span_natural_product_add_right (x19) - L113
specialize integer_span_natural_product_add_right (r * 1) - L114
apply integer_span_natural_product_add_right - L115
exact haddn - L116
exact hfirst_witness_witness_witness_witness_witness_witness_witness_witness_right_left
14Use earlier factsL117–118
15Establish hnew2L119–128
Establish this local claim before using it. It is not an additional assumption.
- L119
have hnew2 : MatrixPointwiseAdd(x4,x5,x12,x13,x20,x21,r · 1)Definitions: MatrixPointwiseAdd - L120
specialize integer_span_natural_product_add_right (ab) - L121
specialize integer_span_natural_product_add_right (ac) - L122
specialize integer_span_natural_product_add_right (fb) - L123
specialize integer_span_natural_product_add_right (fc) - L124
specialize integer_span_natural_product_add_right (hb) - L125
specialize integer_span_natural_product_add_right (hc) - L126
specialize integer_span_natural_product_add_right (jb) - L127
specialize integer_span_natural_product_add_right (jc) - L128
specialize integer_span_natural_product_add_right (w)
16Use earlier factsL129–138
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L129
specialize integer_span_natural_product_add_right (x4) - L130
specialize integer_span_natural_product_add_right (x5) - L131
specialize integer_span_natural_product_add_right (x12) - L132
specialize integer_span_natural_product_add_right (x13) - L133
specialize integer_span_natural_product_add_right (x20) - L134
specialize integer_span_natural_product_add_right (x21) - L135
specialize integer_span_natural_product_add_right (r * 1) - L136
apply integer_span_natural_product_add_right - L137
exact haddn - L138
exact hfirst_witness_witness_witness_witness_witness_witness_witness_witness_right_right_left
17Use earlier factsL139–140
18Establish hnew3L141–150
Establish this local claim before using it. It is not an additional assumption.
- L141
have hnew3 : MatrixPointwiseAdd(x6,x7,x14,x15,x22,x23,r · 1)Definitions: MatrixPointwiseAdd - L142
specialize integer_span_natural_product_add_right (db) - L143
specialize integer_span_natural_product_add_right (dc) - L144
specialize integer_span_natural_product_add_right (eb) - L145
specialize integer_span_natural_product_add_right (ec) - L146
specialize integer_span_natural_product_add_right (gb) - L147
specialize integer_span_natural_product_add_right (gc) - L148
specialize integer_span_natural_product_add_right (ib) - L149
specialize integer_span_natural_product_add_right (ic) - L150
specialize integer_span_natural_product_add_right (w)
19Use earlier factsL151–160
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L151
specialize integer_span_natural_product_add_right (x6) - L152
specialize integer_span_natural_product_add_right (x7) - L153
specialize integer_span_natural_product_add_right (x14) - L154
specialize integer_span_natural_product_add_right (x15) - L155
specialize integer_span_natural_product_add_right (x22) - L156
specialize integer_span_natural_product_add_right (x23) - L157
specialize integer_span_natural_product_add_right (r * 1) - L158
apply integer_span_natural_product_add_right - L159
exact haddp - L160
exact hfirst_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_left
20Use earlier factsL161–162
21Separate the logical casesL163–163
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L163
split
22Use earlier factsL164–173
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L164
specialize integer_span_pointwise_add_interchange (x) - L165
specialize integer_span_pointwise_add_interchange (x1) - L166
specialize integer_span_pointwise_add_interchange (x2) - L167
specialize integer_span_pointwise_add_interchange (x3) - L168
specialize integer_span_pointwise_add_interchange (x8) - L169
specialize integer_span_pointwise_add_interchange (x9) - L170
specialize integer_span_pointwise_add_interchange (x10) - L171
specialize integer_span_pointwise_add_interchange (x11) - L172
specialize integer_span_pointwise_add_interchange (x16) - L173
specialize integer_span_pointwise_add_interchange (x17)
23Use earlier factsL174–183
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L174
specialize integer_span_pointwise_add_interchange (x18) - L175
specialize integer_span_pointwise_add_interchange (x19) - L176
specialize integer_span_pointwise_add_interchange (pb) - L177
specialize integer_span_pointwise_add_interchange (pc) - L178
specialize integer_span_pointwise_add_interchange (qb) - L179
specialize integer_span_pointwise_add_interchange (qc) - L180
specialize integer_span_pointwise_add_interchange (rb) - L181
specialize integer_span_pointwise_add_interchange (rc) - L182
specialize integer_span_pointwise_add_interchange (r * 1) - L183
apply integer_span_pointwise_add_interchange
24Use earlier factsL184–193
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L184
exact hfirst_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_right_left - L185
exact hsecond_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_right_left - L186
exact hthird_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_right_left - L187
exact hnew0 - L188
exact hnew1 - L189
specialize integer_span_pointwise_add_interchange (x4) - L190
specialize integer_span_pointwise_add_interchange (x5) - L191
specialize integer_span_pointwise_add_interchange (x6) - L192
specialize integer_span_pointwise_add_interchange (x7) - L193
specialize integer_span_pointwise_add_interchange (x12)
25Use earlier factsL194–203
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L194
specialize integer_span_pointwise_add_interchange (x13) - L195
specialize integer_span_pointwise_add_interchange (x14) - L196
specialize integer_span_pointwise_add_interchange (x15) - L197
specialize integer_span_pointwise_add_interchange (x20) - L198
specialize integer_span_pointwise_add_interchange (x21) - L199
specialize integer_span_pointwise_add_interchange (x22) - L200
specialize integer_span_pointwise_add_interchange (x23) - L201
specialize integer_span_pointwise_add_interchange (nb) - L202
specialize integer_span_pointwise_add_interchange (nc) - L203
specialize integer_span_pointwise_add_interchange (mb)
26Use earlier factsL204–213
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L204
specialize integer_span_pointwise_add_interchange (mc) - L205
specialize integer_span_pointwise_add_interchange (sb) - L206
specialize integer_span_pointwise_add_interchange (sc) - L207
specialize integer_span_pointwise_add_interchange (r * 1) - L208
apply integer_span_pointwise_add_interchange - L209
exact hfirst_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_right_right - L210
exact hsecond_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_right_right - L211
exact hthird_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_right_right - L212
exact hnew2 - L213
exact hnew3
Original exact command ledger · 213 lines
- 0001
intro ab - 0002
intro ac - 0003
intro db - 0004
intro dc - 0005
intro eb - 0006
intro ec - 0007
intro fb - 0008
intro fc - 0009
intro gb - 0010
intro gc - 0011
intro hb - 0012
intro hc - 0013
intro ib - 0014
intro ic - 0015
intro jb - 0016
intro jc - 0017
intro w - 0018
intro r - 0019
intro pb - 0020
intro pc - 0021
intro nb - 0022
intro nc - 0023
intro qb - 0024
intro qc - 0025
intro mb - 0026
intro mc - 0027
intro rb - 0028
intro rc - 0029
intro sb - 0030
intro sc - 0031
intro haddp - 0032
intro haddn - 0033
intro hfirst - 0034
intro hsecond - 0035
intro hthird - 0036
cases hfirst - 0037
cases hfirst_witness - 0038
cases hfirst_witness_witness - 0039
cases hfirst_witness_witness_witness - 0040
cases hfirst_witness_witness_witness_witness - 0041
cases hfirst_witness_witness_witness_witness_witness - 0042
cases hfirst_witness_witness_witness_witness_witness_witness - 0043
cases hfirst_witness_witness_witness_witness_witness_witness_witness - 0044
cases hfirst_witness_witness_witness_witness_witness_witness_witness_witness - 0045
cases hfirst_witness_witness_witness_witness_witness_witness_witness_witness_right - 0046
cases hfirst_witness_witness_witness_witness_witness_witness_witness_witness_right_right - 0047
cases hfirst_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right - 0048
cases hfirst_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_right - 0049
cases hsecond - 0050
cases hsecond_witness - 0051
cases hsecond_witness_witness - 0052
cases hsecond_witness_witness_witness - 0053
cases hsecond_witness_witness_witness_witness - 0054
cases hsecond_witness_witness_witness_witness_witness - 0055
cases hsecond_witness_witness_witness_witness_witness_witness - 0056
cases hsecond_witness_witness_witness_witness_witness_witness_witness - 0057
cases hsecond_witness_witness_witness_witness_witness_witness_witness_witness - 0058
cases hsecond_witness_witness_witness_witness_witness_witness_witness_witness_right - 0059
cases hsecond_witness_witness_witness_witness_witness_witness_witness_witness_right_right - 0060
cases hsecond_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right - 0061
cases hsecond_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_right - 0062
cases hthird - 0063
cases hthird_witness - 0064
cases hthird_witness_witness - 0065
cases hthird_witness_witness_witness - 0066
cases hthird_witness_witness_witness_witness - 0067
cases hthird_witness_witness_witness_witness_witness - 0068
cases hthird_witness_witness_witness_witness_witness_witness - 0069
cases hthird_witness_witness_witness_witness_witness_witness_witness - 0070
cases hthird_witness_witness_witness_witness_witness_witness_witness_witness - 0071
cases hthird_witness_witness_witness_witness_witness_witness_witness_witness_right - 0072
cases hthird_witness_witness_witness_witness_witness_witness_witness_witness_right_right - 0073
cases hthird_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right - 0074
cases hthird_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_right - 0075
have hnew0 : forall ff_index_mcp_add_ics_sp_new0 ff_left_mcp_add_ics_sp_new0 ff_right_mcp_add_ics_sp_new0 ff_target_mcp_add_ics_sp_new0. (exists mcp_gap_ics_sp_new0_bound. mcp_gap_ics_sp_new0_bound + S (ff_index_mcp_add_ics_sp_new0) = (r * 1)) -> (((exists fs_h_mcp_ics_sp_new0_left. fs_h_mcp_ics_sp_new0_left + S (ff_left_mcp_add_ics_sp_new0) = S ((S (ff_index_mcp_add_ics_sp_new0)) * x1)) /\ exists fs_q_mcp_ics_sp_new0_left. x = fs_q_mcp_ics_sp_new0_left * S ((S (ff_index_mcp_add_ics_sp_new0)) * x1) + (ff_left_mcp_add_ics_sp_new0))) -> (((exists fs_h_mcp_ics_sp_new0_right. fs_h_mcp_ics_sp_new0_right + S (ff_right_mcp_add_ics_sp_new0) = S ((S (ff_index_mcp_add_ics_sp_new0)) * x9)) /\ exists fs_q_mcp_ics_sp_new0_right. x8 = fs_q_mcp_ics_sp_new0_right * S ((S (ff_index_mcp_add_ics_sp_new0)) * x9) + (ff_right_mcp_add_ics_sp_new0))) -> (((exists fs_h_mcp_ics_sp_new0_target. fs_h_mcp_ics_sp_new0_target + S (ff_target_mcp_add_ics_sp_new0) = S ((S (ff_index_mcp_add_ics_sp_new0)) * x17)) /\ exists fs_q_mcp_ics_sp_new0_target. x16 = fs_q_mcp_ics_sp_new0_target * S ((S (ff_index_mcp_add_ics_sp_new0)) * x17) + (ff_target_mcp_add_ics_sp_new0))) -> ff_target_mcp_add_ics_sp_new0 = ff_left_mcp_add_ics_sp_new0 + ff_right_mcp_add_ics_sp_new0 - 0076
specialize integer_span_natural_product_add_right (ab) - 0077
specialize integer_span_natural_product_add_right (ac) - 0078
specialize integer_span_natural_product_add_right (eb) - 0079
specialize integer_span_natural_product_add_right (ec) - 0080
specialize integer_span_natural_product_add_right (gb) - 0081
specialize integer_span_natural_product_add_right (gc) - 0082
specialize integer_span_natural_product_add_right (ib) - 0083
specialize integer_span_natural_product_add_right (ic) - 0084
specialize integer_span_natural_product_add_right (w) - 0085
specialize integer_span_natural_product_add_right (x) - 0086
specialize integer_span_natural_product_add_right (x1) - 0087
specialize integer_span_natural_product_add_right (x8) - 0088
specialize integer_span_natural_product_add_right (x9) - 0089
specialize integer_span_natural_product_add_right (x16) - 0090
specialize integer_span_natural_product_add_right (x17) - 0091
specialize integer_span_natural_product_add_right (r * 1) - 0092
apply integer_span_natural_product_add_right - 0093
exact haddp - 0094
exact hfirst_witness_witness_witness_witness_witness_witness_witness_witness_left - 0095
exact hsecond_witness_witness_witness_witness_witness_witness_witness_witness_left - 0096
exact hthird_witness_witness_witness_witness_witness_witness_witness_witness_left - 0097
have hnew1 : forall ff_index_mcp_add_ics_sp_new1 ff_left_mcp_add_ics_sp_new1 ff_right_mcp_add_ics_sp_new1 ff_target_mcp_add_ics_sp_new1. (exists mcp_gap_ics_sp_new1_bound. mcp_gap_ics_sp_new1_bound + S (ff_index_mcp_add_ics_sp_new1) = (r * 1)) -> (((exists fs_h_mcp_ics_sp_new1_left. fs_h_mcp_ics_sp_new1_left + S (ff_left_mcp_add_ics_sp_new1) = S ((S (ff_index_mcp_add_ics_sp_new1)) * x3)) /\ exists fs_q_mcp_ics_sp_new1_left. x2 = fs_q_mcp_ics_sp_new1_left * S ((S (ff_index_mcp_add_ics_sp_new1)) * x3) + (ff_left_mcp_add_ics_sp_new1))) -> (((exists fs_h_mcp_ics_sp_new1_right. fs_h_mcp_ics_sp_new1_right + S (ff_right_mcp_add_ics_sp_new1) = S ((S (ff_index_mcp_add_ics_sp_new1)) * x11)) /\ exists fs_q_mcp_ics_sp_new1_right. x10 = fs_q_mcp_ics_sp_new1_right * S ((S (ff_index_mcp_add_ics_sp_new1)) * x11) + (ff_right_mcp_add_ics_sp_new1))) -> (((exists fs_h_mcp_ics_sp_new1_target. fs_h_mcp_ics_sp_new1_target + S (ff_target_mcp_add_ics_sp_new1) = S ((S (ff_index_mcp_add_ics_sp_new1)) * x19)) /\ exists fs_q_mcp_ics_sp_new1_target. x18 = fs_q_mcp_ics_sp_new1_target * S ((S (ff_index_mcp_add_ics_sp_new1)) * x19) + (ff_target_mcp_add_ics_sp_new1))) -> ff_target_mcp_add_ics_sp_new1 = ff_left_mcp_add_ics_sp_new1 + ff_right_mcp_add_ics_sp_new1 - 0098
specialize integer_span_natural_product_add_right (db) - 0099
specialize integer_span_natural_product_add_right (dc) - 0100
specialize integer_span_natural_product_add_right (fb) - 0101
specialize integer_span_natural_product_add_right (fc) - 0102
specialize integer_span_natural_product_add_right (hb) - 0103
specialize integer_span_natural_product_add_right (hc) - 0104
specialize integer_span_natural_product_add_right (jb) - 0105
specialize integer_span_natural_product_add_right (jc) - 0106
specialize integer_span_natural_product_add_right (w) - 0107
specialize integer_span_natural_product_add_right (x2) - 0108
specialize integer_span_natural_product_add_right (x3) - 0109
specialize integer_span_natural_product_add_right (x10) - 0110
specialize integer_span_natural_product_add_right (x11) - 0111
specialize integer_span_natural_product_add_right (x18) - 0112
specialize integer_span_natural_product_add_right (x19) - 0113
specialize integer_span_natural_product_add_right (r * 1) - 0114
apply integer_span_natural_product_add_right - 0115
exact haddn - 0116
exact hfirst_witness_witness_witness_witness_witness_witness_witness_witness_right_left - 0117
exact hsecond_witness_witness_witness_witness_witness_witness_witness_witness_right_left - 0118
exact hthird_witness_witness_witness_witness_witness_witness_witness_witness_right_left - 0119
have hnew2 : forall ff_index_mcp_add_ics_sp_new2 ff_left_mcp_add_ics_sp_new2 ff_right_mcp_add_ics_sp_new2 ff_target_mcp_add_ics_sp_new2. (exists mcp_gap_ics_sp_new2_bound. mcp_gap_ics_sp_new2_bound + S (ff_index_mcp_add_ics_sp_new2) = (r * 1)) -> (((exists fs_h_mcp_ics_sp_new2_left. fs_h_mcp_ics_sp_new2_left + S (ff_left_mcp_add_ics_sp_new2) = S ((S (ff_index_mcp_add_ics_sp_new2)) * x5)) /\ exists fs_q_mcp_ics_sp_new2_left. x4 = fs_q_mcp_ics_sp_new2_left * S ((S (ff_index_mcp_add_ics_sp_new2)) * x5) + (ff_left_mcp_add_ics_sp_new2))) -> (((exists fs_h_mcp_ics_sp_new2_right. fs_h_mcp_ics_sp_new2_right + S (ff_right_mcp_add_ics_sp_new2) = S ((S (ff_index_mcp_add_ics_sp_new2)) * x13)) /\ exists fs_q_mcp_ics_sp_new2_right. x12 = fs_q_mcp_ics_sp_new2_right * S ((S (ff_index_mcp_add_ics_sp_new2)) * x13) + (ff_right_mcp_add_ics_sp_new2))) -> (((exists fs_h_mcp_ics_sp_new2_target. fs_h_mcp_ics_sp_new2_target + S (ff_target_mcp_add_ics_sp_new2) = S ((S (ff_index_mcp_add_ics_sp_new2)) * x21)) /\ exists fs_q_mcp_ics_sp_new2_target. x20 = fs_q_mcp_ics_sp_new2_target * S ((S (ff_index_mcp_add_ics_sp_new2)) * x21) + (ff_target_mcp_add_ics_sp_new2))) -> ff_target_mcp_add_ics_sp_new2 = ff_left_mcp_add_ics_sp_new2 + ff_right_mcp_add_ics_sp_new2 - 0120
specialize integer_span_natural_product_add_right (ab) - 0121
specialize integer_span_natural_product_add_right (ac) - 0122
specialize integer_span_natural_product_add_right (fb) - 0123
specialize integer_span_natural_product_add_right (fc) - 0124
specialize integer_span_natural_product_add_right (hb) - 0125
specialize integer_span_natural_product_add_right (hc) - 0126
specialize integer_span_natural_product_add_right (jb) - 0127
specialize integer_span_natural_product_add_right (jc) - 0128
specialize integer_span_natural_product_add_right (w) - 0129
specialize integer_span_natural_product_add_right (x4) - 0130
specialize integer_span_natural_product_add_right (x5) - 0131
specialize integer_span_natural_product_add_right (x12) - 0132
specialize integer_span_natural_product_add_right (x13) - 0133
specialize integer_span_natural_product_add_right (x20) - 0134
specialize integer_span_natural_product_add_right (x21) - 0135
specialize integer_span_natural_product_add_right (r * 1) - 0136
apply integer_span_natural_product_add_right - 0137
exact haddn - 0138
exact hfirst_witness_witness_witness_witness_witness_witness_witness_witness_right_right_left - 0139
exact hsecond_witness_witness_witness_witness_witness_witness_witness_witness_right_right_left - 0140
exact hthird_witness_witness_witness_witness_witness_witness_witness_witness_right_right_left - 0141
have hnew3 : forall ff_index_mcp_add_ics_sp_new3 ff_left_mcp_add_ics_sp_new3 ff_right_mcp_add_ics_sp_new3 ff_target_mcp_add_ics_sp_new3. (exists mcp_gap_ics_sp_new3_bound. mcp_gap_ics_sp_new3_bound + S (ff_index_mcp_add_ics_sp_new3) = (r * 1)) -> (((exists fs_h_mcp_ics_sp_new3_left. fs_h_mcp_ics_sp_new3_left + S (ff_left_mcp_add_ics_sp_new3) = S ((S (ff_index_mcp_add_ics_sp_new3)) * x7)) /\ exists fs_q_mcp_ics_sp_new3_left. x6 = fs_q_mcp_ics_sp_new3_left * S ((S (ff_index_mcp_add_ics_sp_new3)) * x7) + (ff_left_mcp_add_ics_sp_new3))) -> (((exists fs_h_mcp_ics_sp_new3_right. fs_h_mcp_ics_sp_new3_right + S (ff_right_mcp_add_ics_sp_new3) = S ((S (ff_index_mcp_add_ics_sp_new3)) * x15)) /\ exists fs_q_mcp_ics_sp_new3_right. x14 = fs_q_mcp_ics_sp_new3_right * S ((S (ff_index_mcp_add_ics_sp_new3)) * x15) + (ff_right_mcp_add_ics_sp_new3))) -> (((exists fs_h_mcp_ics_sp_new3_target. fs_h_mcp_ics_sp_new3_target + S (ff_target_mcp_add_ics_sp_new3) = S ((S (ff_index_mcp_add_ics_sp_new3)) * x23)) /\ exists fs_q_mcp_ics_sp_new3_target. x22 = fs_q_mcp_ics_sp_new3_target * S ((S (ff_index_mcp_add_ics_sp_new3)) * x23) + (ff_target_mcp_add_ics_sp_new3))) -> ff_target_mcp_add_ics_sp_new3 = ff_left_mcp_add_ics_sp_new3 + ff_right_mcp_add_ics_sp_new3 - 0142
specialize integer_span_natural_product_add_right (db) - 0143
specialize integer_span_natural_product_add_right (dc) - 0144
specialize integer_span_natural_product_add_right (eb) - 0145
specialize integer_span_natural_product_add_right (ec) - 0146
specialize integer_span_natural_product_add_right (gb) - 0147
specialize integer_span_natural_product_add_right (gc) - 0148
specialize integer_span_natural_product_add_right (ib) - 0149
specialize integer_span_natural_product_add_right (ic) - 0150
specialize integer_span_natural_product_add_right (w) - 0151
specialize integer_span_natural_product_add_right (x6) - 0152
specialize integer_span_natural_product_add_right (x7) - 0153
specialize integer_span_natural_product_add_right (x14) - 0154
specialize integer_span_natural_product_add_right (x15) - 0155
specialize integer_span_natural_product_add_right (x22) - 0156
specialize integer_span_natural_product_add_right (x23) - 0157
specialize integer_span_natural_product_add_right (r * 1) - 0158
apply integer_span_natural_product_add_right - 0159
exact haddp - 0160
exact hfirst_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_left - 0161
exact hsecond_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_left - 0162
exact hthird_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_left - 0163
split - 0164
specialize integer_span_pointwise_add_interchange (x) - 0165
specialize integer_span_pointwise_add_interchange (x1) - 0166
specialize integer_span_pointwise_add_interchange (x2) - 0167
specialize integer_span_pointwise_add_interchange (x3) - 0168
specialize integer_span_pointwise_add_interchange (x8) - 0169
specialize integer_span_pointwise_add_interchange (x9) - 0170
specialize integer_span_pointwise_add_interchange (x10) - 0171
specialize integer_span_pointwise_add_interchange (x11) - 0172
specialize integer_span_pointwise_add_interchange (x16) - 0173
specialize integer_span_pointwise_add_interchange (x17) - 0174
specialize integer_span_pointwise_add_interchange (x18) - 0175
specialize integer_span_pointwise_add_interchange (x19) - 0176
specialize integer_span_pointwise_add_interchange (pb) - 0177
specialize integer_span_pointwise_add_interchange (pc) - 0178
specialize integer_span_pointwise_add_interchange (qb) - 0179
specialize integer_span_pointwise_add_interchange (qc) - 0180
specialize integer_span_pointwise_add_interchange (rb) - 0181
specialize integer_span_pointwise_add_interchange (rc) - 0182
specialize integer_span_pointwise_add_interchange (r * 1) - 0183
apply integer_span_pointwise_add_interchange - 0184
exact hfirst_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_right_left - 0185
exact hsecond_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_right_left - 0186
exact hthird_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_right_left - 0187
exact hnew0 - 0188
exact hnew1 - 0189
specialize integer_span_pointwise_add_interchange (x4) - 0190
specialize integer_span_pointwise_add_interchange (x5) - 0191
specialize integer_span_pointwise_add_interchange (x6) - 0192
specialize integer_span_pointwise_add_interchange (x7) - 0193
specialize integer_span_pointwise_add_interchange (x12) - 0194
specialize integer_span_pointwise_add_interchange (x13) - 0195
specialize integer_span_pointwise_add_interchange (x14) - 0196
specialize integer_span_pointwise_add_interchange (x15) - 0197
specialize integer_span_pointwise_add_interchange (x20) - 0198
specialize integer_span_pointwise_add_interchange (x21) - 0199
specialize integer_span_pointwise_add_interchange (x22) - 0200
specialize integer_span_pointwise_add_interchange (x23) - 0201
specialize integer_span_pointwise_add_interchange (nb) - 0202
specialize integer_span_pointwise_add_interchange (nc) - 0203
specialize integer_span_pointwise_add_interchange (mb) - 0204
specialize integer_span_pointwise_add_interchange (mc) - 0205
specialize integer_span_pointwise_add_interchange (sb) - 0206
specialize integer_span_pointwise_add_interchange (sc) - 0207
specialize integer_span_pointwise_add_interchange (r * 1) - 0208
apply integer_span_pointwise_add_interchange - 0209
exact hfirst_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_right_right - 0210
exact hsecond_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_right_right - 0211
exact hthird_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_right_right - 0212
exact hnew2 - 0213
exact hnew3