integer_matrix_vector_add_constructive

forall ab ac db dc eb ec fb fc gb gc hb hc w r pb pc nb nc qb qc mb mc rb rc sb sc. (exists ics_raw_positive_linear_construct_first ics_raw_positive_scale_linear_construct_first ics_raw_negative_linear_construct_first ics_raw_negative_scale_linear_construct_first. (((exists ff_pp_mcp_smatrix_ics_linear_construct_first_raw ff_pps_mcp_smatrix_ics_linear_construct_first_raw ff_nn_mcp_smatrix_ics_linear_construct_first_raw ff_nns_mcp_smatrix_ics_linear_construct_first_raw ff_pn_mcp_smatrix_ics_linear_construct_first_raw ff_pns_mcp_smatrix_ics_linear_construct_first_raw ff_np_mcp_smatrix_ics_linear_construct_first_raw ff_nps_mcp_smatrix_ics_linear_construct_first_raw. ((forall ff_index_mcp_prefix_ics_linear_construct_first_raw_pp. (exists mcp_gap_ics_linear_construct_first_raw_pp_index. mcp_gap_ics_linear_construct_first_raw_pp_index + S (ff_index_mcp_prefix_ics_linear_construct_first_raw_pp) = ((r) * (1))) -> exists ff_row_mcp_prefix_ics_linear_construct_first_raw_pp ff_column_mcp_prefix_ics_linear_construct_first_raw_pp ff_value_mcp_prefix_ics_linear_construct_first_raw_pp. ((ff_index_mcp_prefix_ics_linear_construct_first_raw_pp) = (1) * ff_row_mcp_prefix_ics_linear_construct_first_raw_pp + ff_column_mcp_prefix_ics_linear_construct_first_raw_pp /\ ((exists mcp_gap_ics_linear_construct_first_raw_pp_column. mcp_gap_ics_linear_construct_first_raw_pp_column + S (ff_column_mcp_prefix_ics_linear_construct_first_raw_pp) = (1)) /\ ((exists ff_left_mcp_cell_ics_linear_construct_first_raw_pp_cell ff_left_scale_mcp_cell_ics_linear_construct_first_raw_pp_cell ff_right_mcp_cell_ics_linear_construct_first_raw_pp_cell ff_right_scale_mcp_cell_ics_linear_construct_first_raw_pp_cell. ((forall ff_index_mcp_ics_linear_construct_first_raw_pp_cell_row ff_source_mcp_ics_linear_construct_first_raw_pp_cell_row ff_target_mcp_ics_linear_construct_first_raw_pp_cell_row. (exists mcp_gap_ics_linear_construct_first_raw_pp_cell_row_bound. mcp_gap_ics_linear_construct_first_raw_pp_cell_row_bound + S (ff_index_mcp_ics_linear_construct_first_raw_pp_cell_row) = (w)) -> (((exists fs_h_mcp_ics_linear_construct_first_raw_pp_cell_row_source. fs_h_mcp_ics_linear_construct_first_raw_pp_cell_row_source + S (ff_source_mcp_ics_linear_construct_first_raw_pp_cell_row) = S ((S (((ff_row_mcp_prefix_ics_linear_construct_first_raw_pp) * (w)) + (1) * ff_index_mcp_ics_linear_construct_first_raw_pp_cell_row)) * ac)) /\ exists fs_q_mcp_ics_linear_construct_first_raw_pp_cell_row_source. ab = fs_q_mcp_ics_linear_construct_first_raw_pp_cell_row_source * S ((S (((ff_row_mcp_prefix_ics_linear_construct_first_raw_pp) * (w)) + (1) * ff_index_mcp_ics_linear_construct_first_raw_pp_cell_row)) * ac) + (ff_source_mcp_ics_linear_construct_first_raw_pp_cell_row))) -> (((exists fs_h_mcp_ics_linear_construct_first_raw_pp_cell_row_target. fs_h_mcp_ics_linear_construct_first_raw_pp_cell_row_target + S (ff_target_mcp_ics_linear_construct_first_raw_pp_cell_row) = S ((S (ff_index_mcp_ics_linear_construct_first_raw_pp_cell_row)) * ff_left_scale_mcp_cell_ics_linear_construct_first_raw_pp_cell)) /\ exists fs_q_mcp_ics_linear_construct_first_raw_pp_cell_row_target. ff_left_mcp_cell_ics_linear_construct_first_raw_pp_cell = fs_q_mcp_ics_linear_construct_first_raw_pp_cell_row_target * S ((S (ff_index_mcp_ics_linear_construct_first_raw_pp_cell_row)) * ff_left_scale_mcp_cell_ics_linear_construct_first_raw_pp_cell) + (ff_target_mcp_ics_linear_construct_first_raw_pp_cell_row))) -> ff_target_mcp_ics_linear_construct_first_raw_pp_cell_row = ff_source_mcp_ics_linear_construct_first_raw_pp_cell_row) /\ ((forall ff_index_mcp_ics_linear_construct_first_raw_pp_cell_column ff_source_mcp_ics_linear_construct_first_raw_pp_cell_column ff_target_mcp_ics_linear_construct_first_raw_pp_cell_column. (exists mcp_gap_ics_linear_construct_first_raw_pp_cell_column_bound. mcp_gap_ics_linear_construct_first_raw_pp_cell_column_bound + S (ff_index_mcp_ics_linear_construct_first_raw_pp_cell_column) = (w)) -> (((exists fs_h_mcp_ics_linear_construct_first_raw_pp_cell_column_source. fs_h_mcp_ics_linear_construct_first_raw_pp_cell_column_source + S (ff_source_mcp_ics_linear_construct_first_raw_pp_cell_column) = S ((S ((ff_column_mcp_prefix_ics_linear_construct_first_raw_pp) + (1) * ff_index_mcp_ics_linear_construct_first_raw_pp_cell_column)) * ec)) /\ exists fs_q_mcp_ics_linear_construct_first_raw_pp_cell_column_source. eb = fs_q_mcp_ics_linear_construct_first_raw_pp_cell_column_source * S ((S ((ff_column_mcp_prefix_ics_linear_construct_first_raw_pp) + (1) * ff_index_mcp_ics_linear_construct_first_raw_pp_cell_column)) * ec) + (ff_source_mcp_ics_linear_construct_first_raw_pp_cell_column))) -> (((exists fs_h_mcp_ics_linear_construct_first_raw_pp_cell_column_target. fs_h_mcp_ics_linear_construct_first_raw_pp_cell_column_target + S (ff_target_mcp_ics_linear_construct_first_raw_pp_cell_column) = S ((S (ff_index_mcp_ics_linear_construct_first_raw_pp_cell_column)) * ff_right_scale_mcp_cell_ics_linear_construct_first_raw_pp_cell)) /\ exists fs_q_mcp_ics_linear_construct_first_raw_pp_cell_column_target. ff_right_mcp_cell_ics_linear_construct_first_raw_pp_cell = fs_q_mcp_ics_linear_construct_first_raw_pp_cell_column_target * S ((S (ff_index_mcp_ics_linear_construct_first_raw_pp_cell_column)) * ff_right_scale_mcp_cell_ics_linear_construct_first_raw_pp_cell) + (ff_target_mcp_ics_linear_construct_first_raw_pp_cell_column))) -> ff_target_mcp_ics_linear_construct_first_raw_pp_cell_column = ff_source_mcp_ics_linear_construct_first_raw_pp_cell_column) /\ (exists ff_code_dot_mcp_ics_linear_construct_first_raw_pp_cell_dot ff_scale_dot_mcp_ics_linear_construct_first_raw_pp_cell_dot. ((forall fpmp_index_dot_mcp_ics_linear_construct_first_raw_pp_cell_dot_pointwise fpmp_left_dot_mcp_ics_linear_construct_first_raw_pp_cell_dot_pointwise fpmp_right_dot_mcp_ics_linear_construct_first_raw_pp_cell_dot_pointwise fpmp_target_dot_mcp_ics_linear_construct_first_raw_pp_cell_dot_pointwise. (exists fpmp_gap_dot_mcp_ics_linear_construct_first_raw_pp_cell_dot_pointwise. fpmp_gap_dot_mcp_ics_linear_construct_first_raw_pp_cell_dot_pointwise + S fpmp_index_dot_mcp_ics_linear_construct_first_raw_pp_cell_dot_pointwise = w) -> (((exists ff_h_fpmp_dot_mcp_ics_linear_construct_first_raw_pp_cell_dot_pointwise_left. ff_h_fpmp_dot_mcp_ics_linear_construct_first_raw_pp_cell_dot_pointwise_left + S (fpmp_left_dot_mcp_ics_linear_construct_first_raw_pp_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_linear_construct_first_raw_pp_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_linear_construct_first_raw_pp_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_linear_construct_first_raw_pp_cell_dot_pointwise_left. ff_left_mcp_cell_ics_linear_construct_first_raw_pp_cell = ff_q_fpmp_dot_mcp_ics_linear_construct_first_raw_pp_cell_dot_pointwise_left * S ((S (fpmp_index_dot_mcp_ics_linear_construct_first_raw_pp_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_linear_construct_first_raw_pp_cell) + (fpmp_left_dot_mcp_ics_linear_construct_first_raw_pp_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_linear_construct_first_raw_pp_cell_dot_pointwise_right. ff_h_fpmp_dot_mcp_ics_linear_construct_first_raw_pp_cell_dot_pointwise_right + S (fpmp_right_dot_mcp_ics_linear_construct_first_raw_pp_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_linear_construct_first_raw_pp_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_linear_construct_first_raw_pp_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_linear_construct_first_raw_pp_cell_dot_pointwise_right. ff_right_mcp_cell_ics_linear_construct_first_raw_pp_cell = ff_q_fpmp_dot_mcp_ics_linear_construct_first_raw_pp_cell_dot_pointwise_right * S ((S (fpmp_index_dot_mcp_ics_linear_construct_first_raw_pp_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_linear_construct_first_raw_pp_cell) + (fpmp_right_dot_mcp_ics_linear_construct_first_raw_pp_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_linear_construct_first_raw_pp_cell_dot_pointwise_target. ff_h_fpmp_dot_mcp_ics_linear_construct_first_raw_pp_cell_dot_pointwise_target + S (fpmp_target_dot_mcp_ics_linear_construct_first_raw_pp_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_linear_construct_first_raw_pp_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_linear_construct_first_raw_pp_cell_dot)) /\ exists ff_q_fpmp_dot_mcp_ics_linear_construct_first_raw_pp_cell_dot_pointwise_target. ff_code_dot_mcp_ics_linear_construct_first_raw_pp_cell_dot = ff_q_fpmp_dot_mcp_ics_linear_construct_first_raw_pp_cell_dot_pointwise_target * S ((S (fpmp_index_dot_mcp_ics_linear_construct_first_raw_pp_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_linear_construct_first_raw_pp_cell_dot) + (fpmp_target_dot_mcp_ics_linear_construct_first_raw_pp_cell_dot_pointwise))) -> fpmp_target_dot_mcp_ics_linear_construct_first_raw_pp_cell_dot_pointwise = fpmp_left_dot_mcp_ics_linear_construct_first_raw_pp_cell_dot_pointwise * fpmp_right_dot_mcp_ics_linear_construct_first_raw_pp_cell_dot_pointwise) /\ (exists ff_u_dot_mcp_ics_linear_construct_first_raw_pp_cell_dot_sum ff_v_dot_mcp_ics_linear_construct_first_raw_pp_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_linear_construct_first_raw_pp_cell_dot_sum_start. ff_h_dot_mcp_ics_linear_construct_first_raw_pp_cell_dot_sum_start + S (0) = S ((S (0)) * ff_v_dot_mcp_ics_linear_construct_first_raw_pp_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_linear_construct_first_raw_pp_cell_dot_sum_start. ff_u_dot_mcp_ics_linear_construct_first_raw_pp_cell_dot_sum = ff_q_dot_mcp_ics_linear_construct_first_raw_pp_cell_dot_sum_start * S ((S (0)) * ff_v_dot_mcp_ics_linear_construct_first_raw_pp_cell_dot_sum) + (0))) /\ ((((exists ff_h_dot_mcp_ics_linear_construct_first_raw_pp_cell_dot_sum_terminal. ff_h_dot_mcp_ics_linear_construct_first_raw_pp_cell_dot_sum_terminal + S (ff_value_mcp_prefix_ics_linear_construct_first_raw_pp) = S ((S (w)) * ff_v_dot_mcp_ics_linear_construct_first_raw_pp_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_linear_construct_first_raw_pp_cell_dot_sum_terminal. ff_u_dot_mcp_ics_linear_construct_first_raw_pp_cell_dot_sum = ff_q_dot_mcp_ics_linear_construct_first_raw_pp_cell_dot_sum_terminal * S ((S (w)) * ff_v_dot_mcp_ics_linear_construct_first_raw_pp_cell_dot_sum) + (ff_value_mcp_prefix_ics_linear_construct_first_raw_pp))) /\ forall ff_i_dot_mcp_ics_linear_construct_first_raw_pp_cell_dot_sum. (exists ff_lt_dot_mcp_ics_linear_construct_first_raw_pp_cell_dot_sum_bound. ff_lt_dot_mcp_ics_linear_construct_first_raw_pp_cell_dot_sum_bound + S ff_i_dot_mcp_ics_linear_construct_first_raw_pp_cell_dot_sum = w) -> exists ff_a_dot_mcp_ics_linear_construct_first_raw_pp_cell_dot_sum ff_r_dot_mcp_ics_linear_construct_first_raw_pp_cell_dot_sum ff_s_dot_mcp_ics_linear_construct_first_raw_pp_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_linear_construct_first_raw_pp_cell_dot_sum_summand. ff_h_dot_mcp_ics_linear_construct_first_raw_pp_cell_dot_sum_summand + S (ff_a_dot_mcp_ics_linear_construct_first_raw_pp_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_linear_construct_first_raw_pp_cell_dot_sum)) * ff_scale_dot_mcp_ics_linear_construct_first_raw_pp_cell_dot)) /\ exists ff_q_dot_mcp_ics_linear_construct_first_raw_pp_cell_dot_sum_summand. ff_code_dot_mcp_ics_linear_construct_first_raw_pp_cell_dot = ff_q_dot_mcp_ics_linear_construct_first_raw_pp_cell_dot_sum_summand * S ((S (ff_i_dot_mcp_ics_linear_construct_first_raw_pp_cell_dot_sum)) * ff_scale_dot_mcp_ics_linear_construct_first_raw_pp_cell_dot) + (ff_a_dot_mcp_ics_linear_construct_first_raw_pp_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_linear_construct_first_raw_pp_cell_dot_sum_partial. ff_h_dot_mcp_ics_linear_construct_first_raw_pp_cell_dot_sum_partial + S (ff_r_dot_mcp_ics_linear_construct_first_raw_pp_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_linear_construct_first_raw_pp_cell_dot_sum)) * ff_v_dot_mcp_ics_linear_construct_first_raw_pp_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_linear_construct_first_raw_pp_cell_dot_sum_partial. ff_u_dot_mcp_ics_linear_construct_first_raw_pp_cell_dot_sum = ff_q_dot_mcp_ics_linear_construct_first_raw_pp_cell_dot_sum_partial * S ((S (ff_i_dot_mcp_ics_linear_construct_first_raw_pp_cell_dot_sum)) * ff_v_dot_mcp_ics_linear_construct_first_raw_pp_cell_dot_sum) + (ff_r_dot_mcp_ics_linear_construct_first_raw_pp_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_linear_construct_first_raw_pp_cell_dot_sum_successor. ff_h_dot_mcp_ics_linear_construct_first_raw_pp_cell_dot_sum_successor + S (ff_s_dot_mcp_ics_linear_construct_first_raw_pp_cell_dot_sum) = S ((S (S ff_i_dot_mcp_ics_linear_construct_first_raw_pp_cell_dot_sum)) * ff_v_dot_mcp_ics_linear_construct_first_raw_pp_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_linear_construct_first_raw_pp_cell_dot_sum_successor. ff_u_dot_mcp_ics_linear_construct_first_raw_pp_cell_dot_sum = ff_q_dot_mcp_ics_linear_construct_first_raw_pp_cell_dot_sum_successor * S ((S (S ff_i_dot_mcp_ics_linear_construct_first_raw_pp_cell_dot_sum)) * ff_v_dot_mcp_ics_linear_construct_first_raw_pp_cell_dot_sum) + (ff_s_dot_mcp_ics_linear_construct_first_raw_pp_cell_dot_sum))) /\ ff_s_dot_mcp_ics_linear_construct_first_raw_pp_cell_dot_sum = ff_r_dot_mcp_ics_linear_construct_first_raw_pp_cell_dot_sum + ff_a_dot_mcp_ics_linear_construct_first_raw_pp_cell_dot_sum))))))))))) /\ (((exists fs_h_mcp_ics_linear_construct_first_raw_pp_entry. fs_h_mcp_ics_linear_construct_first_raw_pp_entry + S (ff_value_mcp_prefix_ics_linear_construct_first_raw_pp) = S ((S (ff_index_mcp_prefix_ics_linear_construct_first_raw_pp)) * ff_pps_mcp_smatrix_ics_linear_construct_first_raw)) /\ exists fs_q_mcp_ics_linear_construct_first_raw_pp_entry. ff_pp_mcp_smatrix_ics_linear_construct_first_raw = fs_q_mcp_ics_linear_construct_first_raw_pp_entry * S ((S (ff_index_mcp_prefix_ics_linear_construct_first_raw_pp)) * ff_pps_mcp_smatrix_ics_linear_construct_first_raw) + (ff_value_mcp_prefix_ics_linear_construct_first_raw_pp))))))) /\ ((forall ff_index_mcp_prefix_ics_linear_construct_first_raw_nn. (exists mcp_gap_ics_linear_construct_first_raw_nn_index. mcp_gap_ics_linear_construct_first_raw_nn_index + S (ff_index_mcp_prefix_ics_linear_construct_first_raw_nn) = ((r) * (1))) -> exists ff_row_mcp_prefix_ics_linear_construct_first_raw_nn ff_column_mcp_prefix_ics_linear_construct_first_raw_nn ff_value_mcp_prefix_ics_linear_construct_first_raw_nn. ((ff_index_mcp_prefix_ics_linear_construct_first_raw_nn) = (1) * ff_row_mcp_prefix_ics_linear_construct_first_raw_nn + ff_column_mcp_prefix_ics_linear_construct_first_raw_nn /\ ((exists mcp_gap_ics_linear_construct_first_raw_nn_column. mcp_gap_ics_linear_construct_first_raw_nn_column + S (ff_column_mcp_prefix_ics_linear_construct_first_raw_nn) = (1)) /\ ((exists ff_left_mcp_cell_ics_linear_construct_first_raw_nn_cell ff_left_scale_mcp_cell_ics_linear_construct_first_raw_nn_cell ff_right_mcp_cell_ics_linear_construct_first_raw_nn_cell ff_right_scale_mcp_cell_ics_linear_construct_first_raw_nn_cell. ((forall ff_index_mcp_ics_linear_construct_first_raw_nn_cell_row ff_source_mcp_ics_linear_construct_first_raw_nn_cell_row ff_target_mcp_ics_linear_construct_first_raw_nn_cell_row. (exists mcp_gap_ics_linear_construct_first_raw_nn_cell_row_bound. mcp_gap_ics_linear_construct_first_raw_nn_cell_row_bound + S (ff_index_mcp_ics_linear_construct_first_raw_nn_cell_row) = (w)) -> (((exists fs_h_mcp_ics_linear_construct_first_raw_nn_cell_row_source. fs_h_mcp_ics_linear_construct_first_raw_nn_cell_row_source + S (ff_source_mcp_ics_linear_construct_first_raw_nn_cell_row) = S ((S (((ff_row_mcp_prefix_ics_linear_construct_first_raw_nn) * (w)) + (1) * ff_index_mcp_ics_linear_construct_first_raw_nn_cell_row)) * dc)) /\ exists fs_q_mcp_ics_linear_construct_first_raw_nn_cell_row_source. db = fs_q_mcp_ics_linear_construct_first_raw_nn_cell_row_source * S ((S (((ff_row_mcp_prefix_ics_linear_construct_first_raw_nn) * (w)) + (1) * ff_index_mcp_ics_linear_construct_first_raw_nn_cell_row)) * dc) + (ff_source_mcp_ics_linear_construct_first_raw_nn_cell_row))) -> (((exists fs_h_mcp_ics_linear_construct_first_raw_nn_cell_row_target. fs_h_mcp_ics_linear_construct_first_raw_nn_cell_row_target + S (ff_target_mcp_ics_linear_construct_first_raw_nn_cell_row) = S ((S (ff_index_mcp_ics_linear_construct_first_raw_nn_cell_row)) * ff_left_scale_mcp_cell_ics_linear_construct_first_raw_nn_cell)) /\ exists fs_q_mcp_ics_linear_construct_first_raw_nn_cell_row_target. ff_left_mcp_cell_ics_linear_construct_first_raw_nn_cell = fs_q_mcp_ics_linear_construct_first_raw_nn_cell_row_target * S ((S (ff_index_mcp_ics_linear_construct_first_raw_nn_cell_row)) * ff_left_scale_mcp_cell_ics_linear_construct_first_raw_nn_cell) + (ff_target_mcp_ics_linear_construct_first_raw_nn_cell_row))) -> ff_target_mcp_ics_linear_construct_first_raw_nn_cell_row = ff_source_mcp_ics_linear_construct_first_raw_nn_cell_row) /\ ((forall ff_index_mcp_ics_linear_construct_first_raw_nn_cell_column ff_source_mcp_ics_linear_construct_first_raw_nn_cell_column ff_target_mcp_ics_linear_construct_first_raw_nn_cell_column. (exists mcp_gap_ics_linear_construct_first_raw_nn_cell_column_bound. mcp_gap_ics_linear_construct_first_raw_nn_cell_column_bound + S (ff_index_mcp_ics_linear_construct_first_raw_nn_cell_column) = (w)) -> (((exists fs_h_mcp_ics_linear_construct_first_raw_nn_cell_column_source. fs_h_mcp_ics_linear_construct_first_raw_nn_cell_column_source + S (ff_source_mcp_ics_linear_construct_first_raw_nn_cell_column) = S ((S ((ff_column_mcp_prefix_ics_linear_construct_first_raw_nn) + (1) * ff_index_mcp_ics_linear_construct_first_raw_nn_cell_column)) * fc)) /\ exists fs_q_mcp_ics_linear_construct_first_raw_nn_cell_column_source. fb = fs_q_mcp_ics_linear_construct_first_raw_nn_cell_column_source * S ((S ((ff_column_mcp_prefix_ics_linear_construct_first_raw_nn) + (1) * ff_index_mcp_ics_linear_construct_first_raw_nn_cell_column)) * fc) + (ff_source_mcp_ics_linear_construct_first_raw_nn_cell_column))) -> (((exists fs_h_mcp_ics_linear_construct_first_raw_nn_cell_column_target. fs_h_mcp_ics_linear_construct_first_raw_nn_cell_column_target + S (ff_target_mcp_ics_linear_construct_first_raw_nn_cell_column) = S ((S (ff_index_mcp_ics_linear_construct_first_raw_nn_cell_column)) * ff_right_scale_mcp_cell_ics_linear_construct_first_raw_nn_cell)) /\ exists fs_q_mcp_ics_linear_construct_first_raw_nn_cell_column_target. ff_right_mcp_cell_ics_linear_construct_first_raw_nn_cell = fs_q_mcp_ics_linear_construct_first_raw_nn_cell_column_target * S ((S (ff_index_mcp_ics_linear_construct_first_raw_nn_cell_column)) * ff_right_scale_mcp_cell_ics_linear_construct_first_raw_nn_cell) + (ff_target_mcp_ics_linear_construct_first_raw_nn_cell_column))) -> ff_target_mcp_ics_linear_construct_first_raw_nn_cell_column = ff_source_mcp_ics_linear_construct_first_raw_nn_cell_column) /\ (exists ff_code_dot_mcp_ics_linear_construct_first_raw_nn_cell_dot ff_scale_dot_mcp_ics_linear_construct_first_raw_nn_cell_dot. ((forall fpmp_index_dot_mcp_ics_linear_construct_first_raw_nn_cell_dot_pointwise fpmp_left_dot_mcp_ics_linear_construct_first_raw_nn_cell_dot_pointwise fpmp_right_dot_mcp_ics_linear_construct_first_raw_nn_cell_dot_pointwise fpmp_target_dot_mcp_ics_linear_construct_first_raw_nn_cell_dot_pointwise. (exists fpmp_gap_dot_mcp_ics_linear_construct_first_raw_nn_cell_dot_pointwise. fpmp_gap_dot_mcp_ics_linear_construct_first_raw_nn_cell_dot_pointwise + S fpmp_index_dot_mcp_ics_linear_construct_first_raw_nn_cell_dot_pointwise = w) -> (((exists ff_h_fpmp_dot_mcp_ics_linear_construct_first_raw_nn_cell_dot_pointwise_left. ff_h_fpmp_dot_mcp_ics_linear_construct_first_raw_nn_cell_dot_pointwise_left + S (fpmp_left_dot_mcp_ics_linear_construct_first_raw_nn_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_linear_construct_first_raw_nn_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_linear_construct_first_raw_nn_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_linear_construct_first_raw_nn_cell_dot_pointwise_left. ff_left_mcp_cell_ics_linear_construct_first_raw_nn_cell = ff_q_fpmp_dot_mcp_ics_linear_construct_first_raw_nn_cell_dot_pointwise_left * S ((S (fpmp_index_dot_mcp_ics_linear_construct_first_raw_nn_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_linear_construct_first_raw_nn_cell) + (fpmp_left_dot_mcp_ics_linear_construct_first_raw_nn_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_linear_construct_first_raw_nn_cell_dot_pointwise_right. ff_h_fpmp_dot_mcp_ics_linear_construct_first_raw_nn_cell_dot_pointwise_right + S (fpmp_right_dot_mcp_ics_linear_construct_first_raw_nn_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_linear_construct_first_raw_nn_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_linear_construct_first_raw_nn_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_linear_construct_first_raw_nn_cell_dot_pointwise_right. ff_right_mcp_cell_ics_linear_construct_first_raw_nn_cell = ff_q_fpmp_dot_mcp_ics_linear_construct_first_raw_nn_cell_dot_pointwise_right * S ((S (fpmp_index_dot_mcp_ics_linear_construct_first_raw_nn_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_linear_construct_first_raw_nn_cell) + (fpmp_right_dot_mcp_ics_linear_construct_first_raw_nn_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_linear_construct_first_raw_nn_cell_dot_pointwise_target. ff_h_fpmp_dot_mcp_ics_linear_construct_first_raw_nn_cell_dot_pointwise_target + S (fpmp_target_dot_mcp_ics_linear_construct_first_raw_nn_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_linear_construct_first_raw_nn_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_linear_construct_first_raw_nn_cell_dot)) /\ exists ff_q_fpmp_dot_mcp_ics_linear_construct_first_raw_nn_cell_dot_pointwise_target. ff_code_dot_mcp_ics_linear_construct_first_raw_nn_cell_dot = ff_q_fpmp_dot_mcp_ics_linear_construct_first_raw_nn_cell_dot_pointwise_target * S ((S (fpmp_index_dot_mcp_ics_linear_construct_first_raw_nn_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_linear_construct_first_raw_nn_cell_dot) + (fpmp_target_dot_mcp_ics_linear_construct_first_raw_nn_cell_dot_pointwise))) -> fpmp_target_dot_mcp_ics_linear_construct_first_raw_nn_cell_dot_pointwise = fpmp_left_dot_mcp_ics_linear_construct_first_raw_nn_cell_dot_pointwise * fpmp_right_dot_mcp_ics_linear_construct_first_raw_nn_cell_dot_pointwise) /\ (exists ff_u_dot_mcp_ics_linear_construct_first_raw_nn_cell_dot_sum ff_v_dot_mcp_ics_linear_construct_first_raw_nn_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_linear_construct_first_raw_nn_cell_dot_sum_start. ff_h_dot_mcp_ics_linear_construct_first_raw_nn_cell_dot_sum_start + S (0) = S ((S (0)) * ff_v_dot_mcp_ics_linear_construct_first_raw_nn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_linear_construct_first_raw_nn_cell_dot_sum_start. ff_u_dot_mcp_ics_linear_construct_first_raw_nn_cell_dot_sum = ff_q_dot_mcp_ics_linear_construct_first_raw_nn_cell_dot_sum_start * S ((S (0)) * ff_v_dot_mcp_ics_linear_construct_first_raw_nn_cell_dot_sum) + (0))) /\ ((((exists ff_h_dot_mcp_ics_linear_construct_first_raw_nn_cell_dot_sum_terminal. ff_h_dot_mcp_ics_linear_construct_first_raw_nn_cell_dot_sum_terminal + S (ff_value_mcp_prefix_ics_linear_construct_first_raw_nn) = S ((S (w)) * ff_v_dot_mcp_ics_linear_construct_first_raw_nn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_linear_construct_first_raw_nn_cell_dot_sum_terminal. ff_u_dot_mcp_ics_linear_construct_first_raw_nn_cell_dot_sum = ff_q_dot_mcp_ics_linear_construct_first_raw_nn_cell_dot_sum_terminal * S ((S (w)) * ff_v_dot_mcp_ics_linear_construct_first_raw_nn_cell_dot_sum) + (ff_value_mcp_prefix_ics_linear_construct_first_raw_nn))) /\ forall ff_i_dot_mcp_ics_linear_construct_first_raw_nn_cell_dot_sum. (exists ff_lt_dot_mcp_ics_linear_construct_first_raw_nn_cell_dot_sum_bound. ff_lt_dot_mcp_ics_linear_construct_first_raw_nn_cell_dot_sum_bound + S ff_i_dot_mcp_ics_linear_construct_first_raw_nn_cell_dot_sum = w) -> exists ff_a_dot_mcp_ics_linear_construct_first_raw_nn_cell_dot_sum ff_r_dot_mcp_ics_linear_construct_first_raw_nn_cell_dot_sum ff_s_dot_mcp_ics_linear_construct_first_raw_nn_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_linear_construct_first_raw_nn_cell_dot_sum_summand. ff_h_dot_mcp_ics_linear_construct_first_raw_nn_cell_dot_sum_summand + S (ff_a_dot_mcp_ics_linear_construct_first_raw_nn_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_linear_construct_first_raw_nn_cell_dot_sum)) * ff_scale_dot_mcp_ics_linear_construct_first_raw_nn_cell_dot)) /\ exists ff_q_dot_mcp_ics_linear_construct_first_raw_nn_cell_dot_sum_summand. ff_code_dot_mcp_ics_linear_construct_first_raw_nn_cell_dot = ff_q_dot_mcp_ics_linear_construct_first_raw_nn_cell_dot_sum_summand * S ((S (ff_i_dot_mcp_ics_linear_construct_first_raw_nn_cell_dot_sum)) * ff_scale_dot_mcp_ics_linear_construct_first_raw_nn_cell_dot) + (ff_a_dot_mcp_ics_linear_construct_first_raw_nn_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_linear_construct_first_raw_nn_cell_dot_sum_partial. ff_h_dot_mcp_ics_linear_construct_first_raw_nn_cell_dot_sum_partial + S (ff_r_dot_mcp_ics_linear_construct_first_raw_nn_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_linear_construct_first_raw_nn_cell_dot_sum)) * ff_v_dot_mcp_ics_linear_construct_first_raw_nn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_linear_construct_first_raw_nn_cell_dot_sum_partial. ff_u_dot_mcp_ics_linear_construct_first_raw_nn_cell_dot_sum = ff_q_dot_mcp_ics_linear_construct_first_raw_nn_cell_dot_sum_partial * S ((S (ff_i_dot_mcp_ics_linear_construct_first_raw_nn_cell_dot_sum)) * ff_v_dot_mcp_ics_linear_construct_first_raw_nn_cell_dot_sum) + (ff_r_dot_mcp_ics_linear_construct_first_raw_nn_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_linear_construct_first_raw_nn_cell_dot_sum_successor. ff_h_dot_mcp_ics_linear_construct_first_raw_nn_cell_dot_sum_successor + S (ff_s_dot_mcp_ics_linear_construct_first_raw_nn_cell_dot_sum) = S ((S (S ff_i_dot_mcp_ics_linear_construct_first_raw_nn_cell_dot_sum)) * ff_v_dot_mcp_ics_linear_construct_first_raw_nn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_linear_construct_first_raw_nn_cell_dot_sum_successor. ff_u_dot_mcp_ics_linear_construct_first_raw_nn_cell_dot_sum = ff_q_dot_mcp_ics_linear_construct_first_raw_nn_cell_dot_sum_successor * S ((S (S ff_i_dot_mcp_ics_linear_construct_first_raw_nn_cell_dot_sum)) * ff_v_dot_mcp_ics_linear_construct_first_raw_nn_cell_dot_sum) + (ff_s_dot_mcp_ics_linear_construct_first_raw_nn_cell_dot_sum))) /\ ff_s_dot_mcp_ics_linear_construct_first_raw_nn_cell_dot_sum = ff_r_dot_mcp_ics_linear_construct_first_raw_nn_cell_dot_sum + ff_a_dot_mcp_ics_linear_construct_first_raw_nn_cell_dot_sum))))))))))) /\ (((exists fs_h_mcp_ics_linear_construct_first_raw_nn_entry. fs_h_mcp_ics_linear_construct_first_raw_nn_entry + S (ff_value_mcp_prefix_ics_linear_construct_first_raw_nn) = S ((S (ff_index_mcp_prefix_ics_linear_construct_first_raw_nn)) * ff_nns_mcp_smatrix_ics_linear_construct_first_raw)) /\ exists fs_q_mcp_ics_linear_construct_first_raw_nn_entry. ff_nn_mcp_smatrix_ics_linear_construct_first_raw = fs_q_mcp_ics_linear_construct_first_raw_nn_entry * S ((S (ff_index_mcp_prefix_ics_linear_construct_first_raw_nn)) * ff_nns_mcp_smatrix_ics_linear_construct_first_raw) + (ff_value_mcp_prefix_ics_linear_construct_first_raw_nn))))))) /\ ((forall ff_index_mcp_prefix_ics_linear_construct_first_raw_pn. (exists mcp_gap_ics_linear_construct_first_raw_pn_index. mcp_gap_ics_linear_construct_first_raw_pn_index + S (ff_index_mcp_prefix_ics_linear_construct_first_raw_pn) = ((r) * (1))) -> exists ff_row_mcp_prefix_ics_linear_construct_first_raw_pn ff_column_mcp_prefix_ics_linear_construct_first_raw_pn ff_value_mcp_prefix_ics_linear_construct_first_raw_pn. ((ff_index_mcp_prefix_ics_linear_construct_first_raw_pn) = (1) * ff_row_mcp_prefix_ics_linear_construct_first_raw_pn + ff_column_mcp_prefix_ics_linear_construct_first_raw_pn /\ ((exists mcp_gap_ics_linear_construct_first_raw_pn_column. mcp_gap_ics_linear_construct_first_raw_pn_column + S (ff_column_mcp_prefix_ics_linear_construct_first_raw_pn) = (1)) /\ ((exists ff_left_mcp_cell_ics_linear_construct_first_raw_pn_cell ff_left_scale_mcp_cell_ics_linear_construct_first_raw_pn_cell ff_right_mcp_cell_ics_linear_construct_first_raw_pn_cell ff_right_scale_mcp_cell_ics_linear_construct_first_raw_pn_cell. ((forall ff_index_mcp_ics_linear_construct_first_raw_pn_cell_row ff_source_mcp_ics_linear_construct_first_raw_pn_cell_row ff_target_mcp_ics_linear_construct_first_raw_pn_cell_row. (exists mcp_gap_ics_linear_construct_first_raw_pn_cell_row_bound. mcp_gap_ics_linear_construct_first_raw_pn_cell_row_bound + S (ff_index_mcp_ics_linear_construct_first_raw_pn_cell_row) = (w)) -> (((exists fs_h_mcp_ics_linear_construct_first_raw_pn_cell_row_source. fs_h_mcp_ics_linear_construct_first_raw_pn_cell_row_source + S (ff_source_mcp_ics_linear_construct_first_raw_pn_cell_row) = S ((S (((ff_row_mcp_prefix_ics_linear_construct_first_raw_pn) * (w)) + (1) * ff_index_mcp_ics_linear_construct_first_raw_pn_cell_row)) * ac)) /\ exists fs_q_mcp_ics_linear_construct_first_raw_pn_cell_row_source. ab = fs_q_mcp_ics_linear_construct_first_raw_pn_cell_row_source * S ((S (((ff_row_mcp_prefix_ics_linear_construct_first_raw_pn) * (w)) + (1) * ff_index_mcp_ics_linear_construct_first_raw_pn_cell_row)) * ac) + (ff_source_mcp_ics_linear_construct_first_raw_pn_cell_row))) -> (((exists fs_h_mcp_ics_linear_construct_first_raw_pn_cell_row_target. fs_h_mcp_ics_linear_construct_first_raw_pn_cell_row_target + S (ff_target_mcp_ics_linear_construct_first_raw_pn_cell_row) = S ((S (ff_index_mcp_ics_linear_construct_first_raw_pn_cell_row)) * ff_left_scale_mcp_cell_ics_linear_construct_first_raw_pn_cell)) /\ exists fs_q_mcp_ics_linear_construct_first_raw_pn_cell_row_target. ff_left_mcp_cell_ics_linear_construct_first_raw_pn_cell = fs_q_mcp_ics_linear_construct_first_raw_pn_cell_row_target * S ((S (ff_index_mcp_ics_linear_construct_first_raw_pn_cell_row)) * ff_left_scale_mcp_cell_ics_linear_construct_first_raw_pn_cell) + (ff_target_mcp_ics_linear_construct_first_raw_pn_cell_row))) -> ff_target_mcp_ics_linear_construct_first_raw_pn_cell_row = ff_source_mcp_ics_linear_construct_first_raw_pn_cell_row) /\ ((forall ff_index_mcp_ics_linear_construct_first_raw_pn_cell_column ff_source_mcp_ics_linear_construct_first_raw_pn_cell_column ff_target_mcp_ics_linear_construct_first_raw_pn_cell_column. (exists mcp_gap_ics_linear_construct_first_raw_pn_cell_column_bound. mcp_gap_ics_linear_construct_first_raw_pn_cell_column_bound + S (ff_index_mcp_ics_linear_construct_first_raw_pn_cell_column) = (w)) -> (((exists fs_h_mcp_ics_linear_construct_first_raw_pn_cell_column_source. fs_h_mcp_ics_linear_construct_first_raw_pn_cell_column_source + S (ff_source_mcp_ics_linear_construct_first_raw_pn_cell_column) = S ((S ((ff_column_mcp_prefix_ics_linear_construct_first_raw_pn) + (1) * ff_index_mcp_ics_linear_construct_first_raw_pn_cell_column)) * fc)) /\ exists fs_q_mcp_ics_linear_construct_first_raw_pn_cell_column_source. fb = fs_q_mcp_ics_linear_construct_first_raw_pn_cell_column_source * S ((S ((ff_column_mcp_prefix_ics_linear_construct_first_raw_pn) + (1) * ff_index_mcp_ics_linear_construct_first_raw_pn_cell_column)) * fc) + (ff_source_mcp_ics_linear_construct_first_raw_pn_cell_column))) -> (((exists fs_h_mcp_ics_linear_construct_first_raw_pn_cell_column_target. fs_h_mcp_ics_linear_construct_first_raw_pn_cell_column_target + S (ff_target_mcp_ics_linear_construct_first_raw_pn_cell_column) = S ((S (ff_index_mcp_ics_linear_construct_first_raw_pn_cell_column)) * ff_right_scale_mcp_cell_ics_linear_construct_first_raw_pn_cell)) /\ exists fs_q_mcp_ics_linear_construct_first_raw_pn_cell_column_target. ff_right_mcp_cell_ics_linear_construct_first_raw_pn_cell = fs_q_mcp_ics_linear_construct_first_raw_pn_cell_column_target * S ((S (ff_index_mcp_ics_linear_construct_first_raw_pn_cell_column)) * ff_right_scale_mcp_cell_ics_linear_construct_first_raw_pn_cell) + (ff_target_mcp_ics_linear_construct_first_raw_pn_cell_column))) -> ff_target_mcp_ics_linear_construct_first_raw_pn_cell_column = ff_source_mcp_ics_linear_construct_first_raw_pn_cell_column) /\ (exists ff_code_dot_mcp_ics_linear_construct_first_raw_pn_cell_dot ff_scale_dot_mcp_ics_linear_construct_first_raw_pn_cell_dot. ((forall fpmp_index_dot_mcp_ics_linear_construct_first_raw_pn_cell_dot_pointwise fpmp_left_dot_mcp_ics_linear_construct_first_raw_pn_cell_dot_pointwise fpmp_right_dot_mcp_ics_linear_construct_first_raw_pn_cell_dot_pointwise fpmp_target_dot_mcp_ics_linear_construct_first_raw_pn_cell_dot_pointwise. (exists fpmp_gap_dot_mcp_ics_linear_construct_first_raw_pn_cell_dot_pointwise. fpmp_gap_dot_mcp_ics_linear_construct_first_raw_pn_cell_dot_pointwise + S fpmp_index_dot_mcp_ics_linear_construct_first_raw_pn_cell_dot_pointwise = w) -> (((exists ff_h_fpmp_dot_mcp_ics_linear_construct_first_raw_pn_cell_dot_pointwise_left. ff_h_fpmp_dot_mcp_ics_linear_construct_first_raw_pn_cell_dot_pointwise_left + S (fpmp_left_dot_mcp_ics_linear_construct_first_raw_pn_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_linear_construct_first_raw_pn_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_linear_construct_first_raw_pn_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_linear_construct_first_raw_pn_cell_dot_pointwise_left. ff_left_mcp_cell_ics_linear_construct_first_raw_pn_cell = ff_q_fpmp_dot_mcp_ics_linear_construct_first_raw_pn_cell_dot_pointwise_left * S ((S (fpmp_index_dot_mcp_ics_linear_construct_first_raw_pn_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_linear_construct_first_raw_pn_cell) + (fpmp_left_dot_mcp_ics_linear_construct_first_raw_pn_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_linear_construct_first_raw_pn_cell_dot_pointwise_right. ff_h_fpmp_dot_mcp_ics_linear_construct_first_raw_pn_cell_dot_pointwise_right + S (fpmp_right_dot_mcp_ics_linear_construct_first_raw_pn_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_linear_construct_first_raw_pn_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_linear_construct_first_raw_pn_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_linear_construct_first_raw_pn_cell_dot_pointwise_right. ff_right_mcp_cell_ics_linear_construct_first_raw_pn_cell = ff_q_fpmp_dot_mcp_ics_linear_construct_first_raw_pn_cell_dot_pointwise_right * S ((S (fpmp_index_dot_mcp_ics_linear_construct_first_raw_pn_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_linear_construct_first_raw_pn_cell) + (fpmp_right_dot_mcp_ics_linear_construct_first_raw_pn_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_linear_construct_first_raw_pn_cell_dot_pointwise_target. ff_h_fpmp_dot_mcp_ics_linear_construct_first_raw_pn_cell_dot_pointwise_target + S (fpmp_target_dot_mcp_ics_linear_construct_first_raw_pn_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_linear_construct_first_raw_pn_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_linear_construct_first_raw_pn_cell_dot)) /\ exists ff_q_fpmp_dot_mcp_ics_linear_construct_first_raw_pn_cell_dot_pointwise_target. ff_code_dot_mcp_ics_linear_construct_first_raw_pn_cell_dot = ff_q_fpmp_dot_mcp_ics_linear_construct_first_raw_pn_cell_dot_pointwise_target * S ((S (fpmp_index_dot_mcp_ics_linear_construct_first_raw_pn_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_linear_construct_first_raw_pn_cell_dot) + (fpmp_target_dot_mcp_ics_linear_construct_first_raw_pn_cell_dot_pointwise))) -> fpmp_target_dot_mcp_ics_linear_construct_first_raw_pn_cell_dot_pointwise = fpmp_left_dot_mcp_ics_linear_construct_first_raw_pn_cell_dot_pointwise * fpmp_right_dot_mcp_ics_linear_construct_first_raw_pn_cell_dot_pointwise) /\ (exists ff_u_dot_mcp_ics_linear_construct_first_raw_pn_cell_dot_sum ff_v_dot_mcp_ics_linear_construct_first_raw_pn_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_linear_construct_first_raw_pn_cell_dot_sum_start. ff_h_dot_mcp_ics_linear_construct_first_raw_pn_cell_dot_sum_start + S (0) = S ((S (0)) * ff_v_dot_mcp_ics_linear_construct_first_raw_pn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_linear_construct_first_raw_pn_cell_dot_sum_start. ff_u_dot_mcp_ics_linear_construct_first_raw_pn_cell_dot_sum = ff_q_dot_mcp_ics_linear_construct_first_raw_pn_cell_dot_sum_start * S ((S (0)) * ff_v_dot_mcp_ics_linear_construct_first_raw_pn_cell_dot_sum) + (0))) /\ ((((exists ff_h_dot_mcp_ics_linear_construct_first_raw_pn_cell_dot_sum_terminal. ff_h_dot_mcp_ics_linear_construct_first_raw_pn_cell_dot_sum_terminal + S (ff_value_mcp_prefix_ics_linear_construct_first_raw_pn) = S ((S (w)) * ff_v_dot_mcp_ics_linear_construct_first_raw_pn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_linear_construct_first_raw_pn_cell_dot_sum_terminal. ff_u_dot_mcp_ics_linear_construct_first_raw_pn_cell_dot_sum = ff_q_dot_mcp_ics_linear_construct_first_raw_pn_cell_dot_sum_terminal * S ((S (w)) * ff_v_dot_mcp_ics_linear_construct_first_raw_pn_cell_dot_sum) + (ff_value_mcp_prefix_ics_linear_construct_first_raw_pn))) /\ forall ff_i_dot_mcp_ics_linear_construct_first_raw_pn_cell_dot_sum. (exists ff_lt_dot_mcp_ics_linear_construct_first_raw_pn_cell_dot_sum_bound. ff_lt_dot_mcp_ics_linear_construct_first_raw_pn_cell_dot_sum_bound + S ff_i_dot_mcp_ics_linear_construct_first_raw_pn_cell_dot_sum = w) -> exists ff_a_dot_mcp_ics_linear_construct_first_raw_pn_cell_dot_sum ff_r_dot_mcp_ics_linear_construct_first_raw_pn_cell_dot_sum ff_s_dot_mcp_ics_linear_construct_first_raw_pn_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_linear_construct_first_raw_pn_cell_dot_sum_summand. ff_h_dot_mcp_ics_linear_construct_first_raw_pn_cell_dot_sum_summand + S (ff_a_dot_mcp_ics_linear_construct_first_raw_pn_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_linear_construct_first_raw_pn_cell_dot_sum)) * ff_scale_dot_mcp_ics_linear_construct_first_raw_pn_cell_dot)) /\ exists ff_q_dot_mcp_ics_linear_construct_first_raw_pn_cell_dot_sum_summand. ff_code_dot_mcp_ics_linear_construct_first_raw_pn_cell_dot = ff_q_dot_mcp_ics_linear_construct_first_raw_pn_cell_dot_sum_summand * S ((S (ff_i_dot_mcp_ics_linear_construct_first_raw_pn_cell_dot_sum)) * ff_scale_dot_mcp_ics_linear_construct_first_raw_pn_cell_dot) + (ff_a_dot_mcp_ics_linear_construct_first_raw_pn_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_linear_construct_first_raw_pn_cell_dot_sum_partial. ff_h_dot_mcp_ics_linear_construct_first_raw_pn_cell_dot_sum_partial + S (ff_r_dot_mcp_ics_linear_construct_first_raw_pn_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_linear_construct_first_raw_pn_cell_dot_sum)) * ff_v_dot_mcp_ics_linear_construct_first_raw_pn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_linear_construct_first_raw_pn_cell_dot_sum_partial. ff_u_dot_mcp_ics_linear_construct_first_raw_pn_cell_dot_sum = ff_q_dot_mcp_ics_linear_construct_first_raw_pn_cell_dot_sum_partial * S ((S (ff_i_dot_mcp_ics_linear_construct_first_raw_pn_cell_dot_sum)) * ff_v_dot_mcp_ics_linear_construct_first_raw_pn_cell_dot_sum) + (ff_r_dot_mcp_ics_linear_construct_first_raw_pn_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_linear_construct_first_raw_pn_cell_dot_sum_successor. ff_h_dot_mcp_ics_linear_construct_first_raw_pn_cell_dot_sum_successor + S (ff_s_dot_mcp_ics_linear_construct_first_raw_pn_cell_dot_sum) = S ((S (S ff_i_dot_mcp_ics_linear_construct_first_raw_pn_cell_dot_sum)) * ff_v_dot_mcp_ics_linear_construct_first_raw_pn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_linear_construct_first_raw_pn_cell_dot_sum_successor. ff_u_dot_mcp_ics_linear_construct_first_raw_pn_cell_dot_sum = ff_q_dot_mcp_ics_linear_construct_first_raw_pn_cell_dot_sum_successor * S ((S (S ff_i_dot_mcp_ics_linear_construct_first_raw_pn_cell_dot_sum)) * ff_v_dot_mcp_ics_linear_construct_first_raw_pn_cell_dot_sum) + (ff_s_dot_mcp_ics_linear_construct_first_raw_pn_cell_dot_sum))) /\ ff_s_dot_mcp_ics_linear_construct_first_raw_pn_cell_dot_sum = ff_r_dot_mcp_ics_linear_construct_first_raw_pn_cell_dot_sum + ff_a_dot_mcp_ics_linear_construct_first_raw_pn_cell_dot_sum))))))))))) /\ (((exists fs_h_mcp_ics_linear_construct_first_raw_pn_entry. fs_h_mcp_ics_linear_construct_first_raw_pn_entry + S (ff_value_mcp_prefix_ics_linear_construct_first_raw_pn) = S ((S (ff_index_mcp_prefix_ics_linear_construct_first_raw_pn)) * ff_pns_mcp_smatrix_ics_linear_construct_first_raw)) /\ exists fs_q_mcp_ics_linear_construct_first_raw_pn_entry. ff_pn_mcp_smatrix_ics_linear_construct_first_raw = fs_q_mcp_ics_linear_construct_first_raw_pn_entry * S ((S (ff_index_mcp_prefix_ics_linear_construct_first_raw_pn)) * ff_pns_mcp_smatrix_ics_linear_construct_first_raw) + (ff_value_mcp_prefix_ics_linear_construct_first_raw_pn))))))) /\ ((forall ff_index_mcp_prefix_ics_linear_construct_first_raw_np. (exists mcp_gap_ics_linear_construct_first_raw_np_index. mcp_gap_ics_linear_construct_first_raw_np_index + S (ff_index_mcp_prefix_ics_linear_construct_first_raw_np) = ((r) * (1))) -> exists ff_row_mcp_prefix_ics_linear_construct_first_raw_np ff_column_mcp_prefix_ics_linear_construct_first_raw_np ff_value_mcp_prefix_ics_linear_construct_first_raw_np. ((ff_index_mcp_prefix_ics_linear_construct_first_raw_np) = (1) * ff_row_mcp_prefix_ics_linear_construct_first_raw_np + ff_column_mcp_prefix_ics_linear_construct_first_raw_np /\ ((exists mcp_gap_ics_linear_construct_first_raw_np_column. mcp_gap_ics_linear_construct_first_raw_np_column + S (ff_column_mcp_prefix_ics_linear_construct_first_raw_np) = (1)) /\ ((exists ff_left_mcp_cell_ics_linear_construct_first_raw_np_cell ff_left_scale_mcp_cell_ics_linear_construct_first_raw_np_cell ff_right_mcp_cell_ics_linear_construct_first_raw_np_cell ff_right_scale_mcp_cell_ics_linear_construct_first_raw_np_cell. ((forall ff_index_mcp_ics_linear_construct_first_raw_np_cell_row ff_source_mcp_ics_linear_construct_first_raw_np_cell_row ff_target_mcp_ics_linear_construct_first_raw_np_cell_row. (exists mcp_gap_ics_linear_construct_first_raw_np_cell_row_bound. mcp_gap_ics_linear_construct_first_raw_np_cell_row_bound + S (ff_index_mcp_ics_linear_construct_first_raw_np_cell_row) = (w)) -> (((exists fs_h_mcp_ics_linear_construct_first_raw_np_cell_row_source. fs_h_mcp_ics_linear_construct_first_raw_np_cell_row_source + S (ff_source_mcp_ics_linear_construct_first_raw_np_cell_row) = S ((S (((ff_row_mcp_prefix_ics_linear_construct_first_raw_np) * (w)) + (1) * ff_index_mcp_ics_linear_construct_first_raw_np_cell_row)) * dc)) /\ exists fs_q_mcp_ics_linear_construct_first_raw_np_cell_row_source. db = fs_q_mcp_ics_linear_construct_first_raw_np_cell_row_source * S ((S (((ff_row_mcp_prefix_ics_linear_construct_first_raw_np) * (w)) + (1) * ff_index_mcp_ics_linear_construct_first_raw_np_cell_row)) * dc) + (ff_source_mcp_ics_linear_construct_first_raw_np_cell_row))) -> (((exists fs_h_mcp_ics_linear_construct_first_raw_np_cell_row_target. fs_h_mcp_ics_linear_construct_first_raw_np_cell_row_target + S (ff_target_mcp_ics_linear_construct_first_raw_np_cell_row) = S ((S (ff_index_mcp_ics_linear_construct_first_raw_np_cell_row)) * ff_left_scale_mcp_cell_ics_linear_construct_first_raw_np_cell)) /\ exists fs_q_mcp_ics_linear_construct_first_raw_np_cell_row_target. ff_left_mcp_cell_ics_linear_construct_first_raw_np_cell = fs_q_mcp_ics_linear_construct_first_raw_np_cell_row_target * S ((S (ff_index_mcp_ics_linear_construct_first_raw_np_cell_row)) * ff_left_scale_mcp_cell_ics_linear_construct_first_raw_np_cell) + (ff_target_mcp_ics_linear_construct_first_raw_np_cell_row))) -> ff_target_mcp_ics_linear_construct_first_raw_np_cell_row = ff_source_mcp_ics_linear_construct_first_raw_np_cell_row) /\ ((forall ff_index_mcp_ics_linear_construct_first_raw_np_cell_column ff_source_mcp_ics_linear_construct_first_raw_np_cell_column ff_target_mcp_ics_linear_construct_first_raw_np_cell_column. (exists mcp_gap_ics_linear_construct_first_raw_np_cell_column_bound. mcp_gap_ics_linear_construct_first_raw_np_cell_column_bound + S (ff_index_mcp_ics_linear_construct_first_raw_np_cell_column) = (w)) -> (((exists fs_h_mcp_ics_linear_construct_first_raw_np_cell_column_source. fs_h_mcp_ics_linear_construct_first_raw_np_cell_column_source + S (ff_source_mcp_ics_linear_construct_first_raw_np_cell_column) = S ((S ((ff_column_mcp_prefix_ics_linear_construct_first_raw_np) + (1) * ff_index_mcp_ics_linear_construct_first_raw_np_cell_column)) * ec)) /\ exists fs_q_mcp_ics_linear_construct_first_raw_np_cell_column_source. eb = fs_q_mcp_ics_linear_construct_first_raw_np_cell_column_source * S ((S ((ff_column_mcp_prefix_ics_linear_construct_first_raw_np) + (1) * ff_index_mcp_ics_linear_construct_first_raw_np_cell_column)) * ec) + (ff_source_mcp_ics_linear_construct_first_raw_np_cell_column))) -> (((exists fs_h_mcp_ics_linear_construct_first_raw_np_cell_column_target. fs_h_mcp_ics_linear_construct_first_raw_np_cell_column_target + S (ff_target_mcp_ics_linear_construct_first_raw_np_cell_column) = S ((S (ff_index_mcp_ics_linear_construct_first_raw_np_cell_column)) * ff_right_scale_mcp_cell_ics_linear_construct_first_raw_np_cell)) /\ exists fs_q_mcp_ics_linear_construct_first_raw_np_cell_column_target. ff_right_mcp_cell_ics_linear_construct_first_raw_np_cell = fs_q_mcp_ics_linear_construct_first_raw_np_cell_column_target * S ((S (ff_index_mcp_ics_linear_construct_first_raw_np_cell_column)) * ff_right_scale_mcp_cell_ics_linear_construct_first_raw_np_cell) + (ff_target_mcp_ics_linear_construct_first_raw_np_cell_column))) -> ff_target_mcp_ics_linear_construct_first_raw_np_cell_column = ff_source_mcp_ics_linear_construct_first_raw_np_cell_column) /\ (exists ff_code_dot_mcp_ics_linear_construct_first_raw_np_cell_dot ff_scale_dot_mcp_ics_linear_construct_first_raw_np_cell_dot. ((forall fpmp_index_dot_mcp_ics_linear_construct_first_raw_np_cell_dot_pointwise fpmp_left_dot_mcp_ics_linear_construct_first_raw_np_cell_dot_pointwise fpmp_right_dot_mcp_ics_linear_construct_first_raw_np_cell_dot_pointwise fpmp_target_dot_mcp_ics_linear_construct_first_raw_np_cell_dot_pointwise. (exists fpmp_gap_dot_mcp_ics_linear_construct_first_raw_np_cell_dot_pointwise. fpmp_gap_dot_mcp_ics_linear_construct_first_raw_np_cell_dot_pointwise + S fpmp_index_dot_mcp_ics_linear_construct_first_raw_np_cell_dot_pointwise = w) -> (((exists ff_h_fpmp_dot_mcp_ics_linear_construct_first_raw_np_cell_dot_pointwise_left. ff_h_fpmp_dot_mcp_ics_linear_construct_first_raw_np_cell_dot_pointwise_left + S (fpmp_left_dot_mcp_ics_linear_construct_first_raw_np_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_linear_construct_first_raw_np_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_linear_construct_first_raw_np_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_linear_construct_first_raw_np_cell_dot_pointwise_left. ff_left_mcp_cell_ics_linear_construct_first_raw_np_cell = ff_q_fpmp_dot_mcp_ics_linear_construct_first_raw_np_cell_dot_pointwise_left * S ((S (fpmp_index_dot_mcp_ics_linear_construct_first_raw_np_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_linear_construct_first_raw_np_cell) + (fpmp_left_dot_mcp_ics_linear_construct_first_raw_np_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_linear_construct_first_raw_np_cell_dot_pointwise_right. ff_h_fpmp_dot_mcp_ics_linear_construct_first_raw_np_cell_dot_pointwise_right + S (fpmp_right_dot_mcp_ics_linear_construct_first_raw_np_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_linear_construct_first_raw_np_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_linear_construct_first_raw_np_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_linear_construct_first_raw_np_cell_dot_pointwise_right. ff_right_mcp_cell_ics_linear_construct_first_raw_np_cell = ff_q_fpmp_dot_mcp_ics_linear_construct_first_raw_np_cell_dot_pointwise_right * S ((S (fpmp_index_dot_mcp_ics_linear_construct_first_raw_np_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_linear_construct_first_raw_np_cell) + (fpmp_right_dot_mcp_ics_linear_construct_first_raw_np_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_linear_construct_first_raw_np_cell_dot_pointwise_target. ff_h_fpmp_dot_mcp_ics_linear_construct_first_raw_np_cell_dot_pointwise_target + S (fpmp_target_dot_mcp_ics_linear_construct_first_raw_np_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_linear_construct_first_raw_np_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_linear_construct_first_raw_np_cell_dot)) /\ exists ff_q_fpmp_dot_mcp_ics_linear_construct_first_raw_np_cell_dot_pointwise_target. ff_code_dot_mcp_ics_linear_construct_first_raw_np_cell_dot = ff_q_fpmp_dot_mcp_ics_linear_construct_first_raw_np_cell_dot_pointwise_target * S ((S (fpmp_index_dot_mcp_ics_linear_construct_first_raw_np_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_linear_construct_first_raw_np_cell_dot) + (fpmp_target_dot_mcp_ics_linear_construct_first_raw_np_cell_dot_pointwise))) -> fpmp_target_dot_mcp_ics_linear_construct_first_raw_np_cell_dot_pointwise = fpmp_left_dot_mcp_ics_linear_construct_first_raw_np_cell_dot_pointwise * fpmp_right_dot_mcp_ics_linear_construct_first_raw_np_cell_dot_pointwise) /\ (exists ff_u_dot_mcp_ics_linear_construct_first_raw_np_cell_dot_sum ff_v_dot_mcp_ics_linear_construct_first_raw_np_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_linear_construct_first_raw_np_cell_dot_sum_start. ff_h_dot_mcp_ics_linear_construct_first_raw_np_cell_dot_sum_start + S (0) = S ((S (0)) * ff_v_dot_mcp_ics_linear_construct_first_raw_np_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_linear_construct_first_raw_np_cell_dot_sum_start. ff_u_dot_mcp_ics_linear_construct_first_raw_np_cell_dot_sum = ff_q_dot_mcp_ics_linear_construct_first_raw_np_cell_dot_sum_start * S ((S (0)) * ff_v_dot_mcp_ics_linear_construct_first_raw_np_cell_dot_sum) + (0))) /\ ((((exists ff_h_dot_mcp_ics_linear_construct_first_raw_np_cell_dot_sum_terminal. ff_h_dot_mcp_ics_linear_construct_first_raw_np_cell_dot_sum_terminal + S (ff_value_mcp_prefix_ics_linear_construct_first_raw_np) = S ((S (w)) * ff_v_dot_mcp_ics_linear_construct_first_raw_np_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_linear_construct_first_raw_np_cell_dot_sum_terminal. ff_u_dot_mcp_ics_linear_construct_first_raw_np_cell_dot_sum = ff_q_dot_mcp_ics_linear_construct_first_raw_np_cell_dot_sum_terminal * S ((S (w)) * ff_v_dot_mcp_ics_linear_construct_first_raw_np_cell_dot_sum) + (ff_value_mcp_prefix_ics_linear_construct_first_raw_np))) /\ forall ff_i_dot_mcp_ics_linear_construct_first_raw_np_cell_dot_sum. (exists ff_lt_dot_mcp_ics_linear_construct_first_raw_np_cell_dot_sum_bound. ff_lt_dot_mcp_ics_linear_construct_first_raw_np_cell_dot_sum_bound + S ff_i_dot_mcp_ics_linear_construct_first_raw_np_cell_dot_sum = w) -> exists ff_a_dot_mcp_ics_linear_construct_first_raw_np_cell_dot_sum ff_r_dot_mcp_ics_linear_construct_first_raw_np_cell_dot_sum ff_s_dot_mcp_ics_linear_construct_first_raw_np_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_linear_construct_first_raw_np_cell_dot_sum_summand. ff_h_dot_mcp_ics_linear_construct_first_raw_np_cell_dot_sum_summand + S (ff_a_dot_mcp_ics_linear_construct_first_raw_np_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_linear_construct_first_raw_np_cell_dot_sum)) * ff_scale_dot_mcp_ics_linear_construct_first_raw_np_cell_dot)) /\ exists ff_q_dot_mcp_ics_linear_construct_first_raw_np_cell_dot_sum_summand. ff_code_dot_mcp_ics_linear_construct_first_raw_np_cell_dot = ff_q_dot_mcp_ics_linear_construct_first_raw_np_cell_dot_sum_summand * S ((S (ff_i_dot_mcp_ics_linear_construct_first_raw_np_cell_dot_sum)) * ff_scale_dot_mcp_ics_linear_construct_first_raw_np_cell_dot) + (ff_a_dot_mcp_ics_linear_construct_first_raw_np_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_linear_construct_first_raw_np_cell_dot_sum_partial. ff_h_dot_mcp_ics_linear_construct_first_raw_np_cell_dot_sum_partial + S (ff_r_dot_mcp_ics_linear_construct_first_raw_np_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_linear_construct_first_raw_np_cell_dot_sum)) * ff_v_dot_mcp_ics_linear_construct_first_raw_np_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_linear_construct_first_raw_np_cell_dot_sum_partial. ff_u_dot_mcp_ics_linear_construct_first_raw_np_cell_dot_sum = ff_q_dot_mcp_ics_linear_construct_first_raw_np_cell_dot_sum_partial * S ((S (ff_i_dot_mcp_ics_linear_construct_first_raw_np_cell_dot_sum)) * ff_v_dot_mcp_ics_linear_construct_first_raw_np_cell_dot_sum) + (ff_r_dot_mcp_ics_linear_construct_first_raw_np_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_linear_construct_first_raw_np_cell_dot_sum_successor. ff_h_dot_mcp_ics_linear_construct_first_raw_np_cell_dot_sum_successor + S (ff_s_dot_mcp_ics_linear_construct_first_raw_np_cell_dot_sum) = S ((S (S ff_i_dot_mcp_ics_linear_construct_first_raw_np_cell_dot_sum)) * ff_v_dot_mcp_ics_linear_construct_first_raw_np_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_linear_construct_first_raw_np_cell_dot_sum_successor. ff_u_dot_mcp_ics_linear_construct_first_raw_np_cell_dot_sum = ff_q_dot_mcp_ics_linear_construct_first_raw_np_cell_dot_sum_successor * S ((S (S ff_i_dot_mcp_ics_linear_construct_first_raw_np_cell_dot_sum)) * ff_v_dot_mcp_ics_linear_construct_first_raw_np_cell_dot_sum) + (ff_s_dot_mcp_ics_linear_construct_first_raw_np_cell_dot_sum))) /\ ff_s_dot_mcp_ics_linear_construct_first_raw_np_cell_dot_sum = ff_r_dot_mcp_ics_linear_construct_first_raw_np_cell_dot_sum + ff_a_dot_mcp_ics_linear_construct_first_raw_np_cell_dot_sum))))))))))) /\ (((exists fs_h_mcp_ics_linear_construct_first_raw_np_entry. fs_h_mcp_ics_linear_construct_first_raw_np_entry + S (ff_value_mcp_prefix_ics_linear_construct_first_raw_np) = S ((S (ff_index_mcp_prefix_ics_linear_construct_first_raw_np)) * ff_nps_mcp_smatrix_ics_linear_construct_first_raw)) /\ exists fs_q_mcp_ics_linear_construct_first_raw_np_entry. ff_np_mcp_smatrix_ics_linear_construct_first_raw = fs_q_mcp_ics_linear_construct_first_raw_np_entry * S ((S (ff_index_mcp_prefix_ics_linear_construct_first_raw_np)) * ff_nps_mcp_smatrix_ics_linear_construct_first_raw) + (ff_value_mcp_prefix_ics_linear_construct_first_raw_np))))))) /\ ((forall ff_index_mcp_add_ics_linear_construct_first_raw_positive ff_left_mcp_add_ics_linear_construct_first_raw_positive ff_right_mcp_add_ics_linear_construct_first_raw_positive ff_target_mcp_add_ics_linear_construct_first_raw_positive. (exists mcp_gap_ics_linear_construct_first_raw_positive_bound. mcp_gap_ics_linear_construct_first_raw_positive_bound + S (ff_index_mcp_add_ics_linear_construct_first_raw_positive) = ((r) * (1))) -> (((exists fs_h_mcp_ics_linear_construct_first_raw_positive_left. fs_h_mcp_ics_linear_construct_first_raw_positive_left + S (ff_left_mcp_add_ics_linear_construct_first_raw_positive) = S ((S (ff_index_mcp_add_ics_linear_construct_first_raw_positive)) * ff_pps_mcp_smatrix_ics_linear_construct_first_raw)) /\ exists fs_q_mcp_ics_linear_construct_first_raw_positive_left. ff_pp_mcp_smatrix_ics_linear_construct_first_raw = fs_q_mcp_ics_linear_construct_first_raw_positive_left * S ((S (ff_index_mcp_add_ics_linear_construct_first_raw_positive)) * ff_pps_mcp_smatrix_ics_linear_construct_first_raw) + (ff_left_mcp_add_ics_linear_construct_first_raw_positive))) -> (((exists fs_h_mcp_ics_linear_construct_first_raw_positive_right. fs_h_mcp_ics_linear_construct_first_raw_positive_right + S (ff_right_mcp_add_ics_linear_construct_first_raw_positive) = S ((S (ff_index_mcp_add_ics_linear_construct_first_raw_positive)) * ff_nns_mcp_smatrix_ics_linear_construct_first_raw)) /\ exists fs_q_mcp_ics_linear_construct_first_raw_positive_right. ff_nn_mcp_smatrix_ics_linear_construct_first_raw = fs_q_mcp_ics_linear_construct_first_raw_positive_right * S ((S (ff_index_mcp_add_ics_linear_construct_first_raw_positive)) * ff_nns_mcp_smatrix_ics_linear_construct_first_raw) + (ff_right_mcp_add_ics_linear_construct_first_raw_positive))) -> (((exists fs_h_mcp_ics_linear_construct_first_raw_positive_target. fs_h_mcp_ics_linear_construct_first_raw_positive_target + S (ff_target_mcp_add_ics_linear_construct_first_raw_positive) = S ((S (ff_index_mcp_add_ics_linear_construct_first_raw_positive)) * ics_raw_positive_scale_linear_construct_first)) /\ exists fs_q_mcp_ics_linear_construct_first_raw_positive_target. ics_raw_positive_linear_construct_first = fs_q_mcp_ics_linear_construct_first_raw_positive_target * S ((S (ff_index_mcp_add_ics_linear_construct_first_raw_positive)) * ics_raw_positive_scale_linear_construct_first) + (ff_target_mcp_add_ics_linear_construct_first_raw_positive))) -> ff_target_mcp_add_ics_linear_construct_first_raw_positive = ff_left_mcp_add_ics_linear_construct_first_raw_positive + ff_right_mcp_add_ics_linear_construct_first_raw_positive) /\ (forall ff_index_mcp_add_ics_linear_construct_first_raw_negative ff_left_mcp_add_ics_linear_construct_first_raw_negative ff_right_mcp_add_ics_linear_construct_first_raw_negative ff_target_mcp_add_ics_linear_construct_first_raw_negative. (exists mcp_gap_ics_linear_construct_first_raw_negative_bound. mcp_gap_ics_linear_construct_first_raw_negative_bound + S (ff_index_mcp_add_ics_linear_construct_first_raw_negative) = ((r) * (1))) -> (((exists fs_h_mcp_ics_linear_construct_first_raw_negative_left. fs_h_mcp_ics_linear_construct_first_raw_negative_left + S (ff_left_mcp_add_ics_linear_construct_first_raw_negative) = S ((S (ff_index_mcp_add_ics_linear_construct_first_raw_negative)) * ff_pns_mcp_smatrix_ics_linear_construct_first_raw)) /\ exists fs_q_mcp_ics_linear_construct_first_raw_negative_left. ff_pn_mcp_smatrix_ics_linear_construct_first_raw = fs_q_mcp_ics_linear_construct_first_raw_negative_left * S ((S (ff_index_mcp_add_ics_linear_construct_first_raw_negative)) * ff_pns_mcp_smatrix_ics_linear_construct_first_raw) + (ff_left_mcp_add_ics_linear_construct_first_raw_negative))) -> (((exists fs_h_mcp_ics_linear_construct_first_raw_negative_right. fs_h_mcp_ics_linear_construct_first_raw_negative_right + S (ff_right_mcp_add_ics_linear_construct_first_raw_negative) = S ((S (ff_index_mcp_add_ics_linear_construct_first_raw_negative)) * ff_nps_mcp_smatrix_ics_linear_construct_first_raw)) /\ exists fs_q_mcp_ics_linear_construct_first_raw_negative_right. ff_np_mcp_smatrix_ics_linear_construct_first_raw = fs_q_mcp_ics_linear_construct_first_raw_negative_right * S ((S (ff_index_mcp_add_ics_linear_construct_first_raw_negative)) * ff_nps_mcp_smatrix_ics_linear_construct_first_raw) + (ff_right_mcp_add_ics_linear_construct_first_raw_negative))) -> (((exists fs_h_mcp_ics_linear_construct_first_raw_negative_target. fs_h_mcp_ics_linear_construct_first_raw_negative_target + S (ff_target_mcp_add_ics_linear_construct_first_raw_negative) = S ((S (ff_index_mcp_add_ics_linear_construct_first_raw_negative)) * ics_raw_negative_scale_linear_construct_first)) /\ exists fs_q_mcp_ics_linear_construct_first_raw_negative_target. ics_raw_negative_linear_construct_first = fs_q_mcp_ics_linear_construct_first_raw_negative_target * S ((S (ff_index_mcp_add_ics_linear_construct_first_raw_negative)) * ics_raw_negative_scale_linear_construct_first) + (ff_target_mcp_add_ics_linear_construct_first_raw_negative))) -> ff_target_mcp_add_ics_linear_construct_first_raw_negative = ff_left_mcp_add_ics_linear_construct_first_raw_negative + ff_right_mcp_add_ics_linear_construct_first_raw_negative))))))) /\ (forall ics_index_linear_construct_first_equal ics_value0_linear_construct_first_equal ics_value1_linear_construct_first_equal ics_value2_linear_construct_first_equal ics_value3_linear_construct_first_equal. (exists ics_gap_linear_construct_first_equal_bound. ics_gap_linear_construct_first_equal_bound + S (ics_index_linear_construct_first_equal) = (r)) -> (((exists fs_h_ics_linear_construct_first_equal_at0. fs_h_ics_linear_construct_first_equal_at0 + S (ics_value0_linear_construct_first_equal) = S ((S (ics_index_linear_construct_first_equal)) * ics_raw_positive_scale_linear_construct_first)) /\ exists fs_q_ics_linear_construct_first_equal_at0. ics_raw_positive_linear_construct_first = fs_q_ics_linear_construct_first_equal_at0 * S ((S (ics_index_linear_construct_first_equal)) * ics_raw_positive_scale_linear_construct_first) + (ics_value0_linear_construct_first_equal))) -> (((exists fs_h_ics_linear_construct_first_equal_at1. fs_h_ics_linear_construct_first_equal_at1 + S (ics_value1_linear_construct_first_equal) = S ((S (ics_index_linear_construct_first_equal)) * ics_raw_negative_scale_linear_construct_first)) /\ exists fs_q_ics_linear_construct_first_equal_at1. ics_raw_negative_linear_construct_first = fs_q_ics_linear_construct_first_equal_at1 * S ((S (ics_index_linear_construct_first_equal)) * ics_raw_negative_scale_linear_construct_first) + (ics_value1_linear_construct_first_equal))) -> (((exists fs_h_ics_linear_construct_first_equal_at2. fs_h_ics_linear_construct_first_equal_at2 + S (ics_value2_linear_construct_first_equal) = S ((S (ics_index_linear_construct_first_equal)) * pc)) /\ exists fs_q_ics_linear_construct_first_equal_at2. pb = fs_q_ics_linear_construct_first_equal_at2 * S ((S (ics_index_linear_construct_first_equal)) * pc) + (ics_value2_linear_construct_first_equal))) -> (((exists fs_h_ics_linear_construct_first_equal_at3. fs_h_ics_linear_construct_first_equal_at3 + S (ics_value3_linear_construct_first_equal) = S ((S (ics_index_linear_construct_first_equal)) * nc)) /\ exists fs_q_ics_linear_construct_first_equal_at3. nb = fs_q_ics_linear_construct_first_equal_at3 * S ((S (ics_index_linear_construct_first_equal)) * nc) + (ics_value3_linear_construct_first_equal))) -> ics_value0_linear_construct_first_equal + ics_value3_linear_construct_first_equal = ics_value2_linear_construct_first_equal + ics_value1_linear_construct_first_equal)))) -> (exists ics_raw_positive_linear_construct_second ics_raw_positive_scale_linear_construct_second ics_raw_negative_linear_construct_second ics_raw_negative_scale_linear_construct_second. (((exists ff_pp_mcp_smatrix_ics_linear_construct_second_raw ff_pps_mcp_smatrix_ics_linear_construct_second_raw ff_nn_mcp_smatrix_ics_linear_construct_second_raw ff_nns_mcp_smatrix_ics_linear_construct_second_raw ff_pn_mcp_smatrix_ics_linear_construct_second_raw ff_pns_mcp_smatrix_ics_linear_construct_second_raw ff_np_mcp_smatrix_ics_linear_construct_second_raw ff_nps_mcp_smatrix_ics_linear_construct_second_raw. ((forall ff_index_mcp_prefix_ics_linear_construct_second_raw_pp. (exists mcp_gap_ics_linear_construct_second_raw_pp_index. mcp_gap_ics_linear_construct_second_raw_pp_index + S (ff_index_mcp_prefix_ics_linear_construct_second_raw_pp) = ((r) * (1))) -> exists ff_row_mcp_prefix_ics_linear_construct_second_raw_pp ff_column_mcp_prefix_ics_linear_construct_second_raw_pp ff_value_mcp_prefix_ics_linear_construct_second_raw_pp. ((ff_index_mcp_prefix_ics_linear_construct_second_raw_pp) = (1) * ff_row_mcp_prefix_ics_linear_construct_second_raw_pp + ff_column_mcp_prefix_ics_linear_construct_second_raw_pp /\ ((exists mcp_gap_ics_linear_construct_second_raw_pp_column. mcp_gap_ics_linear_construct_second_raw_pp_column + S (ff_column_mcp_prefix_ics_linear_construct_second_raw_pp) = (1)) /\ ((exists ff_left_mcp_cell_ics_linear_construct_second_raw_pp_cell ff_left_scale_mcp_cell_ics_linear_construct_second_raw_pp_cell ff_right_mcp_cell_ics_linear_construct_second_raw_pp_cell ff_right_scale_mcp_cell_ics_linear_construct_second_raw_pp_cell. ((forall ff_index_mcp_ics_linear_construct_second_raw_pp_cell_row ff_source_mcp_ics_linear_construct_second_raw_pp_cell_row ff_target_mcp_ics_linear_construct_second_raw_pp_cell_row. (exists mcp_gap_ics_linear_construct_second_raw_pp_cell_row_bound. mcp_gap_ics_linear_construct_second_raw_pp_cell_row_bound + S (ff_index_mcp_ics_linear_construct_second_raw_pp_cell_row) = (w)) -> (((exists fs_h_mcp_ics_linear_construct_second_raw_pp_cell_row_source. fs_h_mcp_ics_linear_construct_second_raw_pp_cell_row_source + S (ff_source_mcp_ics_linear_construct_second_raw_pp_cell_row) = S ((S (((ff_row_mcp_prefix_ics_linear_construct_second_raw_pp) * (w)) + (1) * ff_index_mcp_ics_linear_construct_second_raw_pp_cell_row)) * ac)) /\ exists fs_q_mcp_ics_linear_construct_second_raw_pp_cell_row_source. ab = fs_q_mcp_ics_linear_construct_second_raw_pp_cell_row_source * S ((S (((ff_row_mcp_prefix_ics_linear_construct_second_raw_pp) * (w)) + (1) * ff_index_mcp_ics_linear_construct_second_raw_pp_cell_row)) * ac) + (ff_source_mcp_ics_linear_construct_second_raw_pp_cell_row))) -> (((exists fs_h_mcp_ics_linear_construct_second_raw_pp_cell_row_target. fs_h_mcp_ics_linear_construct_second_raw_pp_cell_row_target + S (ff_target_mcp_ics_linear_construct_second_raw_pp_cell_row) = S ((S (ff_index_mcp_ics_linear_construct_second_raw_pp_cell_row)) * ff_left_scale_mcp_cell_ics_linear_construct_second_raw_pp_cell)) /\ exists fs_q_mcp_ics_linear_construct_second_raw_pp_cell_row_target. ff_left_mcp_cell_ics_linear_construct_second_raw_pp_cell = fs_q_mcp_ics_linear_construct_second_raw_pp_cell_row_target * S ((S (ff_index_mcp_ics_linear_construct_second_raw_pp_cell_row)) * ff_left_scale_mcp_cell_ics_linear_construct_second_raw_pp_cell) + (ff_target_mcp_ics_linear_construct_second_raw_pp_cell_row))) -> ff_target_mcp_ics_linear_construct_second_raw_pp_cell_row = ff_source_mcp_ics_linear_construct_second_raw_pp_cell_row) /\ ((forall ff_index_mcp_ics_linear_construct_second_raw_pp_cell_column ff_source_mcp_ics_linear_construct_second_raw_pp_cell_column ff_target_mcp_ics_linear_construct_second_raw_pp_cell_column. (exists mcp_gap_ics_linear_construct_second_raw_pp_cell_column_bound. mcp_gap_ics_linear_construct_second_raw_pp_cell_column_bound + S (ff_index_mcp_ics_linear_construct_second_raw_pp_cell_column) = (w)) -> (((exists fs_h_mcp_ics_linear_construct_second_raw_pp_cell_column_source. fs_h_mcp_ics_linear_construct_second_raw_pp_cell_column_source + S (ff_source_mcp_ics_linear_construct_second_raw_pp_cell_column) = S ((S ((ff_column_mcp_prefix_ics_linear_construct_second_raw_pp) + (1) * ff_index_mcp_ics_linear_construct_second_raw_pp_cell_column)) * gc)) /\ exists fs_q_mcp_ics_linear_construct_second_raw_pp_cell_column_source. gb = fs_q_mcp_ics_linear_construct_second_raw_pp_cell_column_source * S ((S ((ff_column_mcp_prefix_ics_linear_construct_second_raw_pp) + (1) * ff_index_mcp_ics_linear_construct_second_raw_pp_cell_column)) * gc) + (ff_source_mcp_ics_linear_construct_second_raw_pp_cell_column))) -> (((exists fs_h_mcp_ics_linear_construct_second_raw_pp_cell_column_target. fs_h_mcp_ics_linear_construct_second_raw_pp_cell_column_target + S (ff_target_mcp_ics_linear_construct_second_raw_pp_cell_column) = S ((S (ff_index_mcp_ics_linear_construct_second_raw_pp_cell_column)) * ff_right_scale_mcp_cell_ics_linear_construct_second_raw_pp_cell)) /\ exists fs_q_mcp_ics_linear_construct_second_raw_pp_cell_column_target. ff_right_mcp_cell_ics_linear_construct_second_raw_pp_cell = fs_q_mcp_ics_linear_construct_second_raw_pp_cell_column_target * S ((S (ff_index_mcp_ics_linear_construct_second_raw_pp_cell_column)) * ff_right_scale_mcp_cell_ics_linear_construct_second_raw_pp_cell) + (ff_target_mcp_ics_linear_construct_second_raw_pp_cell_column))) -> ff_target_mcp_ics_linear_construct_second_raw_pp_cell_column = ff_source_mcp_ics_linear_construct_second_raw_pp_cell_column) /\ (exists ff_code_dot_mcp_ics_linear_construct_second_raw_pp_cell_dot ff_scale_dot_mcp_ics_linear_construct_second_raw_pp_cell_dot. ((forall fpmp_index_dot_mcp_ics_linear_construct_second_raw_pp_cell_dot_pointwise fpmp_left_dot_mcp_ics_linear_construct_second_raw_pp_cell_dot_pointwise fpmp_right_dot_mcp_ics_linear_construct_second_raw_pp_cell_dot_pointwise fpmp_target_dot_mcp_ics_linear_construct_second_raw_pp_cell_dot_pointwise. (exists fpmp_gap_dot_mcp_ics_linear_construct_second_raw_pp_cell_dot_pointwise. fpmp_gap_dot_mcp_ics_linear_construct_second_raw_pp_cell_dot_pointwise + S fpmp_index_dot_mcp_ics_linear_construct_second_raw_pp_cell_dot_pointwise = w) -> (((exists ff_h_fpmp_dot_mcp_ics_linear_construct_second_raw_pp_cell_dot_pointwise_left. ff_h_fpmp_dot_mcp_ics_linear_construct_second_raw_pp_cell_dot_pointwise_left + S (fpmp_left_dot_mcp_ics_linear_construct_second_raw_pp_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_linear_construct_second_raw_pp_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_linear_construct_second_raw_pp_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_linear_construct_second_raw_pp_cell_dot_pointwise_left. ff_left_mcp_cell_ics_linear_construct_second_raw_pp_cell = ff_q_fpmp_dot_mcp_ics_linear_construct_second_raw_pp_cell_dot_pointwise_left * S ((S (fpmp_index_dot_mcp_ics_linear_construct_second_raw_pp_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_linear_construct_second_raw_pp_cell) + (fpmp_left_dot_mcp_ics_linear_construct_second_raw_pp_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_linear_construct_second_raw_pp_cell_dot_pointwise_right. ff_h_fpmp_dot_mcp_ics_linear_construct_second_raw_pp_cell_dot_pointwise_right + S (fpmp_right_dot_mcp_ics_linear_construct_second_raw_pp_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_linear_construct_second_raw_pp_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_linear_construct_second_raw_pp_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_linear_construct_second_raw_pp_cell_dot_pointwise_right. ff_right_mcp_cell_ics_linear_construct_second_raw_pp_cell = ff_q_fpmp_dot_mcp_ics_linear_construct_second_raw_pp_cell_dot_pointwise_right * S ((S (fpmp_index_dot_mcp_ics_linear_construct_second_raw_pp_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_linear_construct_second_raw_pp_cell) + (fpmp_right_dot_mcp_ics_linear_construct_second_raw_pp_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_linear_construct_second_raw_pp_cell_dot_pointwise_target. ff_h_fpmp_dot_mcp_ics_linear_construct_second_raw_pp_cell_dot_pointwise_target + S (fpmp_target_dot_mcp_ics_linear_construct_second_raw_pp_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_linear_construct_second_raw_pp_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_linear_construct_second_raw_pp_cell_dot)) /\ exists ff_q_fpmp_dot_mcp_ics_linear_construct_second_raw_pp_cell_dot_pointwise_target. ff_code_dot_mcp_ics_linear_construct_second_raw_pp_cell_dot = ff_q_fpmp_dot_mcp_ics_linear_construct_second_raw_pp_cell_dot_pointwise_target * S ((S (fpmp_index_dot_mcp_ics_linear_construct_second_raw_pp_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_linear_construct_second_raw_pp_cell_dot) + (fpmp_target_dot_mcp_ics_linear_construct_second_raw_pp_cell_dot_pointwise))) -> fpmp_target_dot_mcp_ics_linear_construct_second_raw_pp_cell_dot_pointwise = fpmp_left_dot_mcp_ics_linear_construct_second_raw_pp_cell_dot_pointwise * fpmp_right_dot_mcp_ics_linear_construct_second_raw_pp_cell_dot_pointwise) /\ (exists ff_u_dot_mcp_ics_linear_construct_second_raw_pp_cell_dot_sum ff_v_dot_mcp_ics_linear_construct_second_raw_pp_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_linear_construct_second_raw_pp_cell_dot_sum_start. ff_h_dot_mcp_ics_linear_construct_second_raw_pp_cell_dot_sum_start + S (0) = S ((S (0)) * ff_v_dot_mcp_ics_linear_construct_second_raw_pp_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_linear_construct_second_raw_pp_cell_dot_sum_start. ff_u_dot_mcp_ics_linear_construct_second_raw_pp_cell_dot_sum = ff_q_dot_mcp_ics_linear_construct_second_raw_pp_cell_dot_sum_start * S ((S (0)) * ff_v_dot_mcp_ics_linear_construct_second_raw_pp_cell_dot_sum) + (0))) /\ ((((exists ff_h_dot_mcp_ics_linear_construct_second_raw_pp_cell_dot_sum_terminal. ff_h_dot_mcp_ics_linear_construct_second_raw_pp_cell_dot_sum_terminal + S (ff_value_mcp_prefix_ics_linear_construct_second_raw_pp) = S ((S (w)) * ff_v_dot_mcp_ics_linear_construct_second_raw_pp_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_linear_construct_second_raw_pp_cell_dot_sum_terminal. ff_u_dot_mcp_ics_linear_construct_second_raw_pp_cell_dot_sum = ff_q_dot_mcp_ics_linear_construct_second_raw_pp_cell_dot_sum_terminal * S ((S (w)) * ff_v_dot_mcp_ics_linear_construct_second_raw_pp_cell_dot_sum) + (ff_value_mcp_prefix_ics_linear_construct_second_raw_pp))) /\ forall ff_i_dot_mcp_ics_linear_construct_second_raw_pp_cell_dot_sum. (exists ff_lt_dot_mcp_ics_linear_construct_second_raw_pp_cell_dot_sum_bound. ff_lt_dot_mcp_ics_linear_construct_second_raw_pp_cell_dot_sum_bound + S ff_i_dot_mcp_ics_linear_construct_second_raw_pp_cell_dot_sum = w) -> exists ff_a_dot_mcp_ics_linear_construct_second_raw_pp_cell_dot_sum ff_r_dot_mcp_ics_linear_construct_second_raw_pp_cell_dot_sum ff_s_dot_mcp_ics_linear_construct_second_raw_pp_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_linear_construct_second_raw_pp_cell_dot_sum_summand. ff_h_dot_mcp_ics_linear_construct_second_raw_pp_cell_dot_sum_summand + S (ff_a_dot_mcp_ics_linear_construct_second_raw_pp_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_linear_construct_second_raw_pp_cell_dot_sum)) * ff_scale_dot_mcp_ics_linear_construct_second_raw_pp_cell_dot)) /\ exists ff_q_dot_mcp_ics_linear_construct_second_raw_pp_cell_dot_sum_summand. ff_code_dot_mcp_ics_linear_construct_second_raw_pp_cell_dot = ff_q_dot_mcp_ics_linear_construct_second_raw_pp_cell_dot_sum_summand * S ((S (ff_i_dot_mcp_ics_linear_construct_second_raw_pp_cell_dot_sum)) * ff_scale_dot_mcp_ics_linear_construct_second_raw_pp_cell_dot) + (ff_a_dot_mcp_ics_linear_construct_second_raw_pp_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_linear_construct_second_raw_pp_cell_dot_sum_partial. ff_h_dot_mcp_ics_linear_construct_second_raw_pp_cell_dot_sum_partial + S (ff_r_dot_mcp_ics_linear_construct_second_raw_pp_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_linear_construct_second_raw_pp_cell_dot_sum)) * ff_v_dot_mcp_ics_linear_construct_second_raw_pp_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_linear_construct_second_raw_pp_cell_dot_sum_partial. ff_u_dot_mcp_ics_linear_construct_second_raw_pp_cell_dot_sum = ff_q_dot_mcp_ics_linear_construct_second_raw_pp_cell_dot_sum_partial * S ((S (ff_i_dot_mcp_ics_linear_construct_second_raw_pp_cell_dot_sum)) * ff_v_dot_mcp_ics_linear_construct_second_raw_pp_cell_dot_sum) + (ff_r_dot_mcp_ics_linear_construct_second_raw_pp_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_linear_construct_second_raw_pp_cell_dot_sum_successor. ff_h_dot_mcp_ics_linear_construct_second_raw_pp_cell_dot_sum_successor + S (ff_s_dot_mcp_ics_linear_construct_second_raw_pp_cell_dot_sum) = S ((S (S ff_i_dot_mcp_ics_linear_construct_second_raw_pp_cell_dot_sum)) * ff_v_dot_mcp_ics_linear_construct_second_raw_pp_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_linear_construct_second_raw_pp_cell_dot_sum_successor. ff_u_dot_mcp_ics_linear_construct_second_raw_pp_cell_dot_sum = ff_q_dot_mcp_ics_linear_construct_second_raw_pp_cell_dot_sum_successor * S ((S (S ff_i_dot_mcp_ics_linear_construct_second_raw_pp_cell_dot_sum)) * ff_v_dot_mcp_ics_linear_construct_second_raw_pp_cell_dot_sum) + (ff_s_dot_mcp_ics_linear_construct_second_raw_pp_cell_dot_sum))) /\ ff_s_dot_mcp_ics_linear_construct_second_raw_pp_cell_dot_sum = ff_r_dot_mcp_ics_linear_construct_second_raw_pp_cell_dot_sum + ff_a_dot_mcp_ics_linear_construct_second_raw_pp_cell_dot_sum))))))))))) /\ (((exists fs_h_mcp_ics_linear_construct_second_raw_pp_entry. fs_h_mcp_ics_linear_construct_second_raw_pp_entry + S (ff_value_mcp_prefix_ics_linear_construct_second_raw_pp) = S ((S (ff_index_mcp_prefix_ics_linear_construct_second_raw_pp)) * ff_pps_mcp_smatrix_ics_linear_construct_second_raw)) /\ exists fs_q_mcp_ics_linear_construct_second_raw_pp_entry. ff_pp_mcp_smatrix_ics_linear_construct_second_raw = fs_q_mcp_ics_linear_construct_second_raw_pp_entry * S ((S (ff_index_mcp_prefix_ics_linear_construct_second_raw_pp)) * ff_pps_mcp_smatrix_ics_linear_construct_second_raw) + (ff_value_mcp_prefix_ics_linear_construct_second_raw_pp))))))) /\ ((forall ff_index_mcp_prefix_ics_linear_construct_second_raw_nn. (exists mcp_gap_ics_linear_construct_second_raw_nn_index. mcp_gap_ics_linear_construct_second_raw_nn_index + S (ff_index_mcp_prefix_ics_linear_construct_second_raw_nn) = ((r) * (1))) -> exists ff_row_mcp_prefix_ics_linear_construct_second_raw_nn ff_column_mcp_prefix_ics_linear_construct_second_raw_nn ff_value_mcp_prefix_ics_linear_construct_second_raw_nn. ((ff_index_mcp_prefix_ics_linear_construct_second_raw_nn) = (1) * ff_row_mcp_prefix_ics_linear_construct_second_raw_nn + ff_column_mcp_prefix_ics_linear_construct_second_raw_nn /\ ((exists mcp_gap_ics_linear_construct_second_raw_nn_column. mcp_gap_ics_linear_construct_second_raw_nn_column + S (ff_column_mcp_prefix_ics_linear_construct_second_raw_nn) = (1)) /\ ((exists ff_left_mcp_cell_ics_linear_construct_second_raw_nn_cell ff_left_scale_mcp_cell_ics_linear_construct_second_raw_nn_cell ff_right_mcp_cell_ics_linear_construct_second_raw_nn_cell ff_right_scale_mcp_cell_ics_linear_construct_second_raw_nn_cell. ((forall ff_index_mcp_ics_linear_construct_second_raw_nn_cell_row ff_source_mcp_ics_linear_construct_second_raw_nn_cell_row ff_target_mcp_ics_linear_construct_second_raw_nn_cell_row. (exists mcp_gap_ics_linear_construct_second_raw_nn_cell_row_bound. mcp_gap_ics_linear_construct_second_raw_nn_cell_row_bound + S (ff_index_mcp_ics_linear_construct_second_raw_nn_cell_row) = (w)) -> (((exists fs_h_mcp_ics_linear_construct_second_raw_nn_cell_row_source. fs_h_mcp_ics_linear_construct_second_raw_nn_cell_row_source + S (ff_source_mcp_ics_linear_construct_second_raw_nn_cell_row) = S ((S (((ff_row_mcp_prefix_ics_linear_construct_second_raw_nn) * (w)) + (1) * ff_index_mcp_ics_linear_construct_second_raw_nn_cell_row)) * dc)) /\ exists fs_q_mcp_ics_linear_construct_second_raw_nn_cell_row_source. db = fs_q_mcp_ics_linear_construct_second_raw_nn_cell_row_source * S ((S (((ff_row_mcp_prefix_ics_linear_construct_second_raw_nn) * (w)) + (1) * ff_index_mcp_ics_linear_construct_second_raw_nn_cell_row)) * dc) + (ff_source_mcp_ics_linear_construct_second_raw_nn_cell_row))) -> (((exists fs_h_mcp_ics_linear_construct_second_raw_nn_cell_row_target. fs_h_mcp_ics_linear_construct_second_raw_nn_cell_row_target + S (ff_target_mcp_ics_linear_construct_second_raw_nn_cell_row) = S ((S (ff_index_mcp_ics_linear_construct_second_raw_nn_cell_row)) * ff_left_scale_mcp_cell_ics_linear_construct_second_raw_nn_cell)) /\ exists fs_q_mcp_ics_linear_construct_second_raw_nn_cell_row_target. ff_left_mcp_cell_ics_linear_construct_second_raw_nn_cell = fs_q_mcp_ics_linear_construct_second_raw_nn_cell_row_target * S ((S (ff_index_mcp_ics_linear_construct_second_raw_nn_cell_row)) * ff_left_scale_mcp_cell_ics_linear_construct_second_raw_nn_cell) + (ff_target_mcp_ics_linear_construct_second_raw_nn_cell_row))) -> ff_target_mcp_ics_linear_construct_second_raw_nn_cell_row = ff_source_mcp_ics_linear_construct_second_raw_nn_cell_row) /\ ((forall ff_index_mcp_ics_linear_construct_second_raw_nn_cell_column ff_source_mcp_ics_linear_construct_second_raw_nn_cell_column ff_target_mcp_ics_linear_construct_second_raw_nn_cell_column. (exists mcp_gap_ics_linear_construct_second_raw_nn_cell_column_bound. mcp_gap_ics_linear_construct_second_raw_nn_cell_column_bound + S (ff_index_mcp_ics_linear_construct_second_raw_nn_cell_column) = (w)) -> (((exists fs_h_mcp_ics_linear_construct_second_raw_nn_cell_column_source. fs_h_mcp_ics_linear_construct_second_raw_nn_cell_column_source + S (ff_source_mcp_ics_linear_construct_second_raw_nn_cell_column) = S ((S ((ff_column_mcp_prefix_ics_linear_construct_second_raw_nn) + (1) * ff_index_mcp_ics_linear_construct_second_raw_nn_cell_column)) * hc)) /\ exists fs_q_mcp_ics_linear_construct_second_raw_nn_cell_column_source. hb = fs_q_mcp_ics_linear_construct_second_raw_nn_cell_column_source * S ((S ((ff_column_mcp_prefix_ics_linear_construct_second_raw_nn) + (1) * ff_index_mcp_ics_linear_construct_second_raw_nn_cell_column)) * hc) + (ff_source_mcp_ics_linear_construct_second_raw_nn_cell_column))) -> (((exists fs_h_mcp_ics_linear_construct_second_raw_nn_cell_column_target. fs_h_mcp_ics_linear_construct_second_raw_nn_cell_column_target + S (ff_target_mcp_ics_linear_construct_second_raw_nn_cell_column) = S ((S (ff_index_mcp_ics_linear_construct_second_raw_nn_cell_column)) * ff_right_scale_mcp_cell_ics_linear_construct_second_raw_nn_cell)) /\ exists fs_q_mcp_ics_linear_construct_second_raw_nn_cell_column_target. ff_right_mcp_cell_ics_linear_construct_second_raw_nn_cell = fs_q_mcp_ics_linear_construct_second_raw_nn_cell_column_target * S ((S (ff_index_mcp_ics_linear_construct_second_raw_nn_cell_column)) * ff_right_scale_mcp_cell_ics_linear_construct_second_raw_nn_cell) + (ff_target_mcp_ics_linear_construct_second_raw_nn_cell_column))) -> ff_target_mcp_ics_linear_construct_second_raw_nn_cell_column = ff_source_mcp_ics_linear_construct_second_raw_nn_cell_column) /\ (exists ff_code_dot_mcp_ics_linear_construct_second_raw_nn_cell_dot ff_scale_dot_mcp_ics_linear_construct_second_raw_nn_cell_dot. ((forall fpmp_index_dot_mcp_ics_linear_construct_second_raw_nn_cell_dot_pointwise fpmp_left_dot_mcp_ics_linear_construct_second_raw_nn_cell_dot_pointwise fpmp_right_dot_mcp_ics_linear_construct_second_raw_nn_cell_dot_pointwise fpmp_target_dot_mcp_ics_linear_construct_second_raw_nn_cell_dot_pointwise. (exists fpmp_gap_dot_mcp_ics_linear_construct_second_raw_nn_cell_dot_pointwise. fpmp_gap_dot_mcp_ics_linear_construct_second_raw_nn_cell_dot_pointwise + S fpmp_index_dot_mcp_ics_linear_construct_second_raw_nn_cell_dot_pointwise = w) -> (((exists ff_h_fpmp_dot_mcp_ics_linear_construct_second_raw_nn_cell_dot_pointwise_left. ff_h_fpmp_dot_mcp_ics_linear_construct_second_raw_nn_cell_dot_pointwise_left + S (fpmp_left_dot_mcp_ics_linear_construct_second_raw_nn_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_linear_construct_second_raw_nn_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_linear_construct_second_raw_nn_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_linear_construct_second_raw_nn_cell_dot_pointwise_left. ff_left_mcp_cell_ics_linear_construct_second_raw_nn_cell = ff_q_fpmp_dot_mcp_ics_linear_construct_second_raw_nn_cell_dot_pointwise_left * S ((S (fpmp_index_dot_mcp_ics_linear_construct_second_raw_nn_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_linear_construct_second_raw_nn_cell) + (fpmp_left_dot_mcp_ics_linear_construct_second_raw_nn_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_linear_construct_second_raw_nn_cell_dot_pointwise_right. ff_h_fpmp_dot_mcp_ics_linear_construct_second_raw_nn_cell_dot_pointwise_right + S (fpmp_right_dot_mcp_ics_linear_construct_second_raw_nn_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_linear_construct_second_raw_nn_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_linear_construct_second_raw_nn_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_linear_construct_second_raw_nn_cell_dot_pointwise_right. ff_right_mcp_cell_ics_linear_construct_second_raw_nn_cell = ff_q_fpmp_dot_mcp_ics_linear_construct_second_raw_nn_cell_dot_pointwise_right * S ((S (fpmp_index_dot_mcp_ics_linear_construct_second_raw_nn_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_linear_construct_second_raw_nn_cell) + (fpmp_right_dot_mcp_ics_linear_construct_second_raw_nn_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_linear_construct_second_raw_nn_cell_dot_pointwise_target. ff_h_fpmp_dot_mcp_ics_linear_construct_second_raw_nn_cell_dot_pointwise_target + S (fpmp_target_dot_mcp_ics_linear_construct_second_raw_nn_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_linear_construct_second_raw_nn_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_linear_construct_second_raw_nn_cell_dot)) /\ exists ff_q_fpmp_dot_mcp_ics_linear_construct_second_raw_nn_cell_dot_pointwise_target. ff_code_dot_mcp_ics_linear_construct_second_raw_nn_cell_dot = ff_q_fpmp_dot_mcp_ics_linear_construct_second_raw_nn_cell_dot_pointwise_target * S ((S (fpmp_index_dot_mcp_ics_linear_construct_second_raw_nn_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_linear_construct_second_raw_nn_cell_dot) + (fpmp_target_dot_mcp_ics_linear_construct_second_raw_nn_cell_dot_pointwise))) -> fpmp_target_dot_mcp_ics_linear_construct_second_raw_nn_cell_dot_pointwise = fpmp_left_dot_mcp_ics_linear_construct_second_raw_nn_cell_dot_pointwise * fpmp_right_dot_mcp_ics_linear_construct_second_raw_nn_cell_dot_pointwise) /\ (exists ff_u_dot_mcp_ics_linear_construct_second_raw_nn_cell_dot_sum ff_v_dot_mcp_ics_linear_construct_second_raw_nn_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_linear_construct_second_raw_nn_cell_dot_sum_start. ff_h_dot_mcp_ics_linear_construct_second_raw_nn_cell_dot_sum_start + S (0) = S ((S (0)) * ff_v_dot_mcp_ics_linear_construct_second_raw_nn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_linear_construct_second_raw_nn_cell_dot_sum_start. ff_u_dot_mcp_ics_linear_construct_second_raw_nn_cell_dot_sum = ff_q_dot_mcp_ics_linear_construct_second_raw_nn_cell_dot_sum_start * S ((S (0)) * ff_v_dot_mcp_ics_linear_construct_second_raw_nn_cell_dot_sum) + (0))) /\ ((((exists ff_h_dot_mcp_ics_linear_construct_second_raw_nn_cell_dot_sum_terminal. ff_h_dot_mcp_ics_linear_construct_second_raw_nn_cell_dot_sum_terminal + S (ff_value_mcp_prefix_ics_linear_construct_second_raw_nn) = S ((S (w)) * ff_v_dot_mcp_ics_linear_construct_second_raw_nn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_linear_construct_second_raw_nn_cell_dot_sum_terminal. ff_u_dot_mcp_ics_linear_construct_second_raw_nn_cell_dot_sum = ff_q_dot_mcp_ics_linear_construct_second_raw_nn_cell_dot_sum_terminal * S ((S (w)) * ff_v_dot_mcp_ics_linear_construct_second_raw_nn_cell_dot_sum) + (ff_value_mcp_prefix_ics_linear_construct_second_raw_nn))) /\ forall ff_i_dot_mcp_ics_linear_construct_second_raw_nn_cell_dot_sum. (exists ff_lt_dot_mcp_ics_linear_construct_second_raw_nn_cell_dot_sum_bound. ff_lt_dot_mcp_ics_linear_construct_second_raw_nn_cell_dot_sum_bound + S ff_i_dot_mcp_ics_linear_construct_second_raw_nn_cell_dot_sum = w) -> exists ff_a_dot_mcp_ics_linear_construct_second_raw_nn_cell_dot_sum ff_r_dot_mcp_ics_linear_construct_second_raw_nn_cell_dot_sum ff_s_dot_mcp_ics_linear_construct_second_raw_nn_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_linear_construct_second_raw_nn_cell_dot_sum_summand. ff_h_dot_mcp_ics_linear_construct_second_raw_nn_cell_dot_sum_summand + S (ff_a_dot_mcp_ics_linear_construct_second_raw_nn_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_linear_construct_second_raw_nn_cell_dot_sum)) * ff_scale_dot_mcp_ics_linear_construct_second_raw_nn_cell_dot)) /\ exists ff_q_dot_mcp_ics_linear_construct_second_raw_nn_cell_dot_sum_summand. ff_code_dot_mcp_ics_linear_construct_second_raw_nn_cell_dot = ff_q_dot_mcp_ics_linear_construct_second_raw_nn_cell_dot_sum_summand * S ((S (ff_i_dot_mcp_ics_linear_construct_second_raw_nn_cell_dot_sum)) * ff_scale_dot_mcp_ics_linear_construct_second_raw_nn_cell_dot) + (ff_a_dot_mcp_ics_linear_construct_second_raw_nn_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_linear_construct_second_raw_nn_cell_dot_sum_partial. ff_h_dot_mcp_ics_linear_construct_second_raw_nn_cell_dot_sum_partial + S (ff_r_dot_mcp_ics_linear_construct_second_raw_nn_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_linear_construct_second_raw_nn_cell_dot_sum)) * ff_v_dot_mcp_ics_linear_construct_second_raw_nn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_linear_construct_second_raw_nn_cell_dot_sum_partial. ff_u_dot_mcp_ics_linear_construct_second_raw_nn_cell_dot_sum = ff_q_dot_mcp_ics_linear_construct_second_raw_nn_cell_dot_sum_partial * S ((S (ff_i_dot_mcp_ics_linear_construct_second_raw_nn_cell_dot_sum)) * ff_v_dot_mcp_ics_linear_construct_second_raw_nn_cell_dot_sum) + (ff_r_dot_mcp_ics_linear_construct_second_raw_nn_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_linear_construct_second_raw_nn_cell_dot_sum_successor. ff_h_dot_mcp_ics_linear_construct_second_raw_nn_cell_dot_sum_successor + S (ff_s_dot_mcp_ics_linear_construct_second_raw_nn_cell_dot_sum) = S ((S (S ff_i_dot_mcp_ics_linear_construct_second_raw_nn_cell_dot_sum)) * ff_v_dot_mcp_ics_linear_construct_second_raw_nn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_linear_construct_second_raw_nn_cell_dot_sum_successor. ff_u_dot_mcp_ics_linear_construct_second_raw_nn_cell_dot_sum = ff_q_dot_mcp_ics_linear_construct_second_raw_nn_cell_dot_sum_successor * S ((S (S ff_i_dot_mcp_ics_linear_construct_second_raw_nn_cell_dot_sum)) * ff_v_dot_mcp_ics_linear_construct_second_raw_nn_cell_dot_sum) + (ff_s_dot_mcp_ics_linear_construct_second_raw_nn_cell_dot_sum))) /\ ff_s_dot_mcp_ics_linear_construct_second_raw_nn_cell_dot_sum = ff_r_dot_mcp_ics_linear_construct_second_raw_nn_cell_dot_sum + ff_a_dot_mcp_ics_linear_construct_second_raw_nn_cell_dot_sum))))))))))) /\ (((exists fs_h_mcp_ics_linear_construct_second_raw_nn_entry. fs_h_mcp_ics_linear_construct_second_raw_nn_entry + S (ff_value_mcp_prefix_ics_linear_construct_second_raw_nn) = S ((S (ff_index_mcp_prefix_ics_linear_construct_second_raw_nn)) * ff_nns_mcp_smatrix_ics_linear_construct_second_raw)) /\ exists fs_q_mcp_ics_linear_construct_second_raw_nn_entry. ff_nn_mcp_smatrix_ics_linear_construct_second_raw = fs_q_mcp_ics_linear_construct_second_raw_nn_entry * S ((S (ff_index_mcp_prefix_ics_linear_construct_second_raw_nn)) * ff_nns_mcp_smatrix_ics_linear_construct_second_raw) + (ff_value_mcp_prefix_ics_linear_construct_second_raw_nn))))))) /\ ((forall ff_index_mcp_prefix_ics_linear_construct_second_raw_pn. (exists mcp_gap_ics_linear_construct_second_raw_pn_index. mcp_gap_ics_linear_construct_second_raw_pn_index + S (ff_index_mcp_prefix_ics_linear_construct_second_raw_pn) = ((r) * (1))) -> exists ff_row_mcp_prefix_ics_linear_construct_second_raw_pn ff_column_mcp_prefix_ics_linear_construct_second_raw_pn ff_value_mcp_prefix_ics_linear_construct_second_raw_pn. ((ff_index_mcp_prefix_ics_linear_construct_second_raw_pn) = (1) * ff_row_mcp_prefix_ics_linear_construct_second_raw_pn + ff_column_mcp_prefix_ics_linear_construct_second_raw_pn /\ ((exists mcp_gap_ics_linear_construct_second_raw_pn_column. mcp_gap_ics_linear_construct_second_raw_pn_column + S (ff_column_mcp_prefix_ics_linear_construct_second_raw_pn) = (1)) /\ ((exists ff_left_mcp_cell_ics_linear_construct_second_raw_pn_cell ff_left_scale_mcp_cell_ics_linear_construct_second_raw_pn_cell ff_right_mcp_cell_ics_linear_construct_second_raw_pn_cell ff_right_scale_mcp_cell_ics_linear_construct_second_raw_pn_cell. ((forall ff_index_mcp_ics_linear_construct_second_raw_pn_cell_row ff_source_mcp_ics_linear_construct_second_raw_pn_cell_row ff_target_mcp_ics_linear_construct_second_raw_pn_cell_row. (exists mcp_gap_ics_linear_construct_second_raw_pn_cell_row_bound. mcp_gap_ics_linear_construct_second_raw_pn_cell_row_bound + S (ff_index_mcp_ics_linear_construct_second_raw_pn_cell_row) = (w)) -> (((exists fs_h_mcp_ics_linear_construct_second_raw_pn_cell_row_source. fs_h_mcp_ics_linear_construct_second_raw_pn_cell_row_source + S (ff_source_mcp_ics_linear_construct_second_raw_pn_cell_row) = S ((S (((ff_row_mcp_prefix_ics_linear_construct_second_raw_pn) * (w)) + (1) * ff_index_mcp_ics_linear_construct_second_raw_pn_cell_row)) * ac)) /\ exists fs_q_mcp_ics_linear_construct_second_raw_pn_cell_row_source. ab = fs_q_mcp_ics_linear_construct_second_raw_pn_cell_row_source * S ((S (((ff_row_mcp_prefix_ics_linear_construct_second_raw_pn) * (w)) + (1) * ff_index_mcp_ics_linear_construct_second_raw_pn_cell_row)) * ac) + (ff_source_mcp_ics_linear_construct_second_raw_pn_cell_row))) -> (((exists fs_h_mcp_ics_linear_construct_second_raw_pn_cell_row_target. fs_h_mcp_ics_linear_construct_second_raw_pn_cell_row_target + S (ff_target_mcp_ics_linear_construct_second_raw_pn_cell_row) = S ((S (ff_index_mcp_ics_linear_construct_second_raw_pn_cell_row)) * ff_left_scale_mcp_cell_ics_linear_construct_second_raw_pn_cell)) /\ exists fs_q_mcp_ics_linear_construct_second_raw_pn_cell_row_target. ff_left_mcp_cell_ics_linear_construct_second_raw_pn_cell = fs_q_mcp_ics_linear_construct_second_raw_pn_cell_row_target * S ((S (ff_index_mcp_ics_linear_construct_second_raw_pn_cell_row)) * ff_left_scale_mcp_cell_ics_linear_construct_second_raw_pn_cell) + (ff_target_mcp_ics_linear_construct_second_raw_pn_cell_row))) -> ff_target_mcp_ics_linear_construct_second_raw_pn_cell_row = ff_source_mcp_ics_linear_construct_second_raw_pn_cell_row) /\ ((forall ff_index_mcp_ics_linear_construct_second_raw_pn_cell_column ff_source_mcp_ics_linear_construct_second_raw_pn_cell_column ff_target_mcp_ics_linear_construct_second_raw_pn_cell_column. (exists mcp_gap_ics_linear_construct_second_raw_pn_cell_column_bound. mcp_gap_ics_linear_construct_second_raw_pn_cell_column_bound + S (ff_index_mcp_ics_linear_construct_second_raw_pn_cell_column) = (w)) -> (((exists fs_h_mcp_ics_linear_construct_second_raw_pn_cell_column_source. fs_h_mcp_ics_linear_construct_second_raw_pn_cell_column_source + S (ff_source_mcp_ics_linear_construct_second_raw_pn_cell_column) = S ((S ((ff_column_mcp_prefix_ics_linear_construct_second_raw_pn) + (1) * ff_index_mcp_ics_linear_construct_second_raw_pn_cell_column)) * hc)) /\ exists fs_q_mcp_ics_linear_construct_second_raw_pn_cell_column_source. hb = fs_q_mcp_ics_linear_construct_second_raw_pn_cell_column_source * S ((S ((ff_column_mcp_prefix_ics_linear_construct_second_raw_pn) + (1) * ff_index_mcp_ics_linear_construct_second_raw_pn_cell_column)) * hc) + (ff_source_mcp_ics_linear_construct_second_raw_pn_cell_column))) -> (((exists fs_h_mcp_ics_linear_construct_second_raw_pn_cell_column_target. fs_h_mcp_ics_linear_construct_second_raw_pn_cell_column_target + S (ff_target_mcp_ics_linear_construct_second_raw_pn_cell_column) = S ((S (ff_index_mcp_ics_linear_construct_second_raw_pn_cell_column)) * ff_right_scale_mcp_cell_ics_linear_construct_second_raw_pn_cell)) /\ exists fs_q_mcp_ics_linear_construct_second_raw_pn_cell_column_target. ff_right_mcp_cell_ics_linear_construct_second_raw_pn_cell = fs_q_mcp_ics_linear_construct_second_raw_pn_cell_column_target * S ((S (ff_index_mcp_ics_linear_construct_second_raw_pn_cell_column)) * ff_right_scale_mcp_cell_ics_linear_construct_second_raw_pn_cell) + (ff_target_mcp_ics_linear_construct_second_raw_pn_cell_column))) -> ff_target_mcp_ics_linear_construct_second_raw_pn_cell_column = ff_source_mcp_ics_linear_construct_second_raw_pn_cell_column) /\ (exists ff_code_dot_mcp_ics_linear_construct_second_raw_pn_cell_dot ff_scale_dot_mcp_ics_linear_construct_second_raw_pn_cell_dot. ((forall fpmp_index_dot_mcp_ics_linear_construct_second_raw_pn_cell_dot_pointwise fpmp_left_dot_mcp_ics_linear_construct_second_raw_pn_cell_dot_pointwise fpmp_right_dot_mcp_ics_linear_construct_second_raw_pn_cell_dot_pointwise fpmp_target_dot_mcp_ics_linear_construct_second_raw_pn_cell_dot_pointwise. (exists fpmp_gap_dot_mcp_ics_linear_construct_second_raw_pn_cell_dot_pointwise. fpmp_gap_dot_mcp_ics_linear_construct_second_raw_pn_cell_dot_pointwise + S fpmp_index_dot_mcp_ics_linear_construct_second_raw_pn_cell_dot_pointwise = w) -> (((exists ff_h_fpmp_dot_mcp_ics_linear_construct_second_raw_pn_cell_dot_pointwise_left. ff_h_fpmp_dot_mcp_ics_linear_construct_second_raw_pn_cell_dot_pointwise_left + S (fpmp_left_dot_mcp_ics_linear_construct_second_raw_pn_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_linear_construct_second_raw_pn_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_linear_construct_second_raw_pn_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_linear_construct_second_raw_pn_cell_dot_pointwise_left. ff_left_mcp_cell_ics_linear_construct_second_raw_pn_cell = ff_q_fpmp_dot_mcp_ics_linear_construct_second_raw_pn_cell_dot_pointwise_left * S ((S (fpmp_index_dot_mcp_ics_linear_construct_second_raw_pn_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_linear_construct_second_raw_pn_cell) + (fpmp_left_dot_mcp_ics_linear_construct_second_raw_pn_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_linear_construct_second_raw_pn_cell_dot_pointwise_right. ff_h_fpmp_dot_mcp_ics_linear_construct_second_raw_pn_cell_dot_pointwise_right + S (fpmp_right_dot_mcp_ics_linear_construct_second_raw_pn_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_linear_construct_second_raw_pn_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_linear_construct_second_raw_pn_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_linear_construct_second_raw_pn_cell_dot_pointwise_right. ff_right_mcp_cell_ics_linear_construct_second_raw_pn_cell = ff_q_fpmp_dot_mcp_ics_linear_construct_second_raw_pn_cell_dot_pointwise_right * S ((S (fpmp_index_dot_mcp_ics_linear_construct_second_raw_pn_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_linear_construct_second_raw_pn_cell) + (fpmp_right_dot_mcp_ics_linear_construct_second_raw_pn_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_linear_construct_second_raw_pn_cell_dot_pointwise_target. ff_h_fpmp_dot_mcp_ics_linear_construct_second_raw_pn_cell_dot_pointwise_target + S (fpmp_target_dot_mcp_ics_linear_construct_second_raw_pn_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_linear_construct_second_raw_pn_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_linear_construct_second_raw_pn_cell_dot)) /\ exists ff_q_fpmp_dot_mcp_ics_linear_construct_second_raw_pn_cell_dot_pointwise_target. ff_code_dot_mcp_ics_linear_construct_second_raw_pn_cell_dot = ff_q_fpmp_dot_mcp_ics_linear_construct_second_raw_pn_cell_dot_pointwise_target * S ((S (fpmp_index_dot_mcp_ics_linear_construct_second_raw_pn_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_linear_construct_second_raw_pn_cell_dot) + (fpmp_target_dot_mcp_ics_linear_construct_second_raw_pn_cell_dot_pointwise))) -> fpmp_target_dot_mcp_ics_linear_construct_second_raw_pn_cell_dot_pointwise = fpmp_left_dot_mcp_ics_linear_construct_second_raw_pn_cell_dot_pointwise * fpmp_right_dot_mcp_ics_linear_construct_second_raw_pn_cell_dot_pointwise) /\ (exists ff_u_dot_mcp_ics_linear_construct_second_raw_pn_cell_dot_sum ff_v_dot_mcp_ics_linear_construct_second_raw_pn_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_linear_construct_second_raw_pn_cell_dot_sum_start. ff_h_dot_mcp_ics_linear_construct_second_raw_pn_cell_dot_sum_start + S (0) = S ((S (0)) * ff_v_dot_mcp_ics_linear_construct_second_raw_pn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_linear_construct_second_raw_pn_cell_dot_sum_start. ff_u_dot_mcp_ics_linear_construct_second_raw_pn_cell_dot_sum = ff_q_dot_mcp_ics_linear_construct_second_raw_pn_cell_dot_sum_start * S ((S (0)) * ff_v_dot_mcp_ics_linear_construct_second_raw_pn_cell_dot_sum) + (0))) /\ ((((exists ff_h_dot_mcp_ics_linear_construct_second_raw_pn_cell_dot_sum_terminal. ff_h_dot_mcp_ics_linear_construct_second_raw_pn_cell_dot_sum_terminal + S (ff_value_mcp_prefix_ics_linear_construct_second_raw_pn) = S ((S (w)) * ff_v_dot_mcp_ics_linear_construct_second_raw_pn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_linear_construct_second_raw_pn_cell_dot_sum_terminal. ff_u_dot_mcp_ics_linear_construct_second_raw_pn_cell_dot_sum = ff_q_dot_mcp_ics_linear_construct_second_raw_pn_cell_dot_sum_terminal * S ((S (w)) * ff_v_dot_mcp_ics_linear_construct_second_raw_pn_cell_dot_sum) + (ff_value_mcp_prefix_ics_linear_construct_second_raw_pn))) /\ forall ff_i_dot_mcp_ics_linear_construct_second_raw_pn_cell_dot_sum. (exists ff_lt_dot_mcp_ics_linear_construct_second_raw_pn_cell_dot_sum_bound. ff_lt_dot_mcp_ics_linear_construct_second_raw_pn_cell_dot_sum_bound + S ff_i_dot_mcp_ics_linear_construct_second_raw_pn_cell_dot_sum = w) -> exists ff_a_dot_mcp_ics_linear_construct_second_raw_pn_cell_dot_sum ff_r_dot_mcp_ics_linear_construct_second_raw_pn_cell_dot_sum ff_s_dot_mcp_ics_linear_construct_second_raw_pn_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_linear_construct_second_raw_pn_cell_dot_sum_summand. ff_h_dot_mcp_ics_linear_construct_second_raw_pn_cell_dot_sum_summand + S (ff_a_dot_mcp_ics_linear_construct_second_raw_pn_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_linear_construct_second_raw_pn_cell_dot_sum)) * ff_scale_dot_mcp_ics_linear_construct_second_raw_pn_cell_dot)) /\ exists ff_q_dot_mcp_ics_linear_construct_second_raw_pn_cell_dot_sum_summand. ff_code_dot_mcp_ics_linear_construct_second_raw_pn_cell_dot = ff_q_dot_mcp_ics_linear_construct_second_raw_pn_cell_dot_sum_summand * S ((S (ff_i_dot_mcp_ics_linear_construct_second_raw_pn_cell_dot_sum)) * ff_scale_dot_mcp_ics_linear_construct_second_raw_pn_cell_dot) + (ff_a_dot_mcp_ics_linear_construct_second_raw_pn_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_linear_construct_second_raw_pn_cell_dot_sum_partial. ff_h_dot_mcp_ics_linear_construct_second_raw_pn_cell_dot_sum_partial + S (ff_r_dot_mcp_ics_linear_construct_second_raw_pn_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_linear_construct_second_raw_pn_cell_dot_sum)) * ff_v_dot_mcp_ics_linear_construct_second_raw_pn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_linear_construct_second_raw_pn_cell_dot_sum_partial. ff_u_dot_mcp_ics_linear_construct_second_raw_pn_cell_dot_sum = ff_q_dot_mcp_ics_linear_construct_second_raw_pn_cell_dot_sum_partial * S ((S (ff_i_dot_mcp_ics_linear_construct_second_raw_pn_cell_dot_sum)) * ff_v_dot_mcp_ics_linear_construct_second_raw_pn_cell_dot_sum) + (ff_r_dot_mcp_ics_linear_construct_second_raw_pn_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_linear_construct_second_raw_pn_cell_dot_sum_successor. ff_h_dot_mcp_ics_linear_construct_second_raw_pn_cell_dot_sum_successor + S (ff_s_dot_mcp_ics_linear_construct_second_raw_pn_cell_dot_sum) = S ((S (S ff_i_dot_mcp_ics_linear_construct_second_raw_pn_cell_dot_sum)) * ff_v_dot_mcp_ics_linear_construct_second_raw_pn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_linear_construct_second_raw_pn_cell_dot_sum_successor. ff_u_dot_mcp_ics_linear_construct_second_raw_pn_cell_dot_sum = ff_q_dot_mcp_ics_linear_construct_second_raw_pn_cell_dot_sum_successor * S ((S (S ff_i_dot_mcp_ics_linear_construct_second_raw_pn_cell_dot_sum)) * ff_v_dot_mcp_ics_linear_construct_second_raw_pn_cell_dot_sum) + (ff_s_dot_mcp_ics_linear_construct_second_raw_pn_cell_dot_sum))) /\ ff_s_dot_mcp_ics_linear_construct_second_raw_pn_cell_dot_sum = ff_r_dot_mcp_ics_linear_construct_second_raw_pn_cell_dot_sum + ff_a_dot_mcp_ics_linear_construct_second_raw_pn_cell_dot_sum))))))))))) /\ (((exists fs_h_mcp_ics_linear_construct_second_raw_pn_entry. fs_h_mcp_ics_linear_construct_second_raw_pn_entry + S (ff_value_mcp_prefix_ics_linear_construct_second_raw_pn) = S ((S (ff_index_mcp_prefix_ics_linear_construct_second_raw_pn)) * ff_pns_mcp_smatrix_ics_linear_construct_second_raw)) /\ exists fs_q_mcp_ics_linear_construct_second_raw_pn_entry. ff_pn_mcp_smatrix_ics_linear_construct_second_raw = fs_q_mcp_ics_linear_construct_second_raw_pn_entry * S ((S (ff_index_mcp_prefix_ics_linear_construct_second_raw_pn)) * ff_pns_mcp_smatrix_ics_linear_construct_second_raw) + (ff_value_mcp_prefix_ics_linear_construct_second_raw_pn))))))) /\ ((forall ff_index_mcp_prefix_ics_linear_construct_second_raw_np. (exists mcp_gap_ics_linear_construct_second_raw_np_index. mcp_gap_ics_linear_construct_second_raw_np_index + S (ff_index_mcp_prefix_ics_linear_construct_second_raw_np) = ((r) * (1))) -> exists ff_row_mcp_prefix_ics_linear_construct_second_raw_np ff_column_mcp_prefix_ics_linear_construct_second_raw_np ff_value_mcp_prefix_ics_linear_construct_second_raw_np. ((ff_index_mcp_prefix_ics_linear_construct_second_raw_np) = (1) * ff_row_mcp_prefix_ics_linear_construct_second_raw_np + ff_column_mcp_prefix_ics_linear_construct_second_raw_np /\ ((exists mcp_gap_ics_linear_construct_second_raw_np_column. mcp_gap_ics_linear_construct_second_raw_np_column + S (ff_column_mcp_prefix_ics_linear_construct_second_raw_np) = (1)) /\ ((exists ff_left_mcp_cell_ics_linear_construct_second_raw_np_cell ff_left_scale_mcp_cell_ics_linear_construct_second_raw_np_cell ff_right_mcp_cell_ics_linear_construct_second_raw_np_cell ff_right_scale_mcp_cell_ics_linear_construct_second_raw_np_cell. ((forall ff_index_mcp_ics_linear_construct_second_raw_np_cell_row ff_source_mcp_ics_linear_construct_second_raw_np_cell_row ff_target_mcp_ics_linear_construct_second_raw_np_cell_row. (exists mcp_gap_ics_linear_construct_second_raw_np_cell_row_bound. mcp_gap_ics_linear_construct_second_raw_np_cell_row_bound + S (ff_index_mcp_ics_linear_construct_second_raw_np_cell_row) = (w)) -> (((exists fs_h_mcp_ics_linear_construct_second_raw_np_cell_row_source. fs_h_mcp_ics_linear_construct_second_raw_np_cell_row_source + S (ff_source_mcp_ics_linear_construct_second_raw_np_cell_row) = S ((S (((ff_row_mcp_prefix_ics_linear_construct_second_raw_np) * (w)) + (1) * ff_index_mcp_ics_linear_construct_second_raw_np_cell_row)) * dc)) /\ exists fs_q_mcp_ics_linear_construct_second_raw_np_cell_row_source. db = fs_q_mcp_ics_linear_construct_second_raw_np_cell_row_source * S ((S (((ff_row_mcp_prefix_ics_linear_construct_second_raw_np) * (w)) + (1) * ff_index_mcp_ics_linear_construct_second_raw_np_cell_row)) * dc) + (ff_source_mcp_ics_linear_construct_second_raw_np_cell_row))) -> (((exists fs_h_mcp_ics_linear_construct_second_raw_np_cell_row_target. fs_h_mcp_ics_linear_construct_second_raw_np_cell_row_target + S (ff_target_mcp_ics_linear_construct_second_raw_np_cell_row) = S ((S (ff_index_mcp_ics_linear_construct_second_raw_np_cell_row)) * ff_left_scale_mcp_cell_ics_linear_construct_second_raw_np_cell)) /\ exists fs_q_mcp_ics_linear_construct_second_raw_np_cell_row_target. ff_left_mcp_cell_ics_linear_construct_second_raw_np_cell = fs_q_mcp_ics_linear_construct_second_raw_np_cell_row_target * S ((S (ff_index_mcp_ics_linear_construct_second_raw_np_cell_row)) * ff_left_scale_mcp_cell_ics_linear_construct_second_raw_np_cell) + (ff_target_mcp_ics_linear_construct_second_raw_np_cell_row))) -> ff_target_mcp_ics_linear_construct_second_raw_np_cell_row = ff_source_mcp_ics_linear_construct_second_raw_np_cell_row) /\ ((forall ff_index_mcp_ics_linear_construct_second_raw_np_cell_column ff_source_mcp_ics_linear_construct_second_raw_np_cell_column ff_target_mcp_ics_linear_construct_second_raw_np_cell_column. (exists mcp_gap_ics_linear_construct_second_raw_np_cell_column_bound. mcp_gap_ics_linear_construct_second_raw_np_cell_column_bound + S (ff_index_mcp_ics_linear_construct_second_raw_np_cell_column) = (w)) -> (((exists fs_h_mcp_ics_linear_construct_second_raw_np_cell_column_source. fs_h_mcp_ics_linear_construct_second_raw_np_cell_column_source + S (ff_source_mcp_ics_linear_construct_second_raw_np_cell_column) = S ((S ((ff_column_mcp_prefix_ics_linear_construct_second_raw_np) + (1) * ff_index_mcp_ics_linear_construct_second_raw_np_cell_column)) * gc)) /\ exists fs_q_mcp_ics_linear_construct_second_raw_np_cell_column_source. gb = fs_q_mcp_ics_linear_construct_second_raw_np_cell_column_source * S ((S ((ff_column_mcp_prefix_ics_linear_construct_second_raw_np) + (1) * ff_index_mcp_ics_linear_construct_second_raw_np_cell_column)) * gc) + (ff_source_mcp_ics_linear_construct_second_raw_np_cell_column))) -> (((exists fs_h_mcp_ics_linear_construct_second_raw_np_cell_column_target. fs_h_mcp_ics_linear_construct_second_raw_np_cell_column_target + S (ff_target_mcp_ics_linear_construct_second_raw_np_cell_column) = S ((S (ff_index_mcp_ics_linear_construct_second_raw_np_cell_column)) * ff_right_scale_mcp_cell_ics_linear_construct_second_raw_np_cell)) /\ exists fs_q_mcp_ics_linear_construct_second_raw_np_cell_column_target. ff_right_mcp_cell_ics_linear_construct_second_raw_np_cell = fs_q_mcp_ics_linear_construct_second_raw_np_cell_column_target * S ((S (ff_index_mcp_ics_linear_construct_second_raw_np_cell_column)) * ff_right_scale_mcp_cell_ics_linear_construct_second_raw_np_cell) + (ff_target_mcp_ics_linear_construct_second_raw_np_cell_column))) -> ff_target_mcp_ics_linear_construct_second_raw_np_cell_column = ff_source_mcp_ics_linear_construct_second_raw_np_cell_column) /\ (exists ff_code_dot_mcp_ics_linear_construct_second_raw_np_cell_dot ff_scale_dot_mcp_ics_linear_construct_second_raw_np_cell_dot. ((forall fpmp_index_dot_mcp_ics_linear_construct_second_raw_np_cell_dot_pointwise fpmp_left_dot_mcp_ics_linear_construct_second_raw_np_cell_dot_pointwise fpmp_right_dot_mcp_ics_linear_construct_second_raw_np_cell_dot_pointwise fpmp_target_dot_mcp_ics_linear_construct_second_raw_np_cell_dot_pointwise. (exists fpmp_gap_dot_mcp_ics_linear_construct_second_raw_np_cell_dot_pointwise. fpmp_gap_dot_mcp_ics_linear_construct_second_raw_np_cell_dot_pointwise + S fpmp_index_dot_mcp_ics_linear_construct_second_raw_np_cell_dot_pointwise = w) -> (((exists ff_h_fpmp_dot_mcp_ics_linear_construct_second_raw_np_cell_dot_pointwise_left. ff_h_fpmp_dot_mcp_ics_linear_construct_second_raw_np_cell_dot_pointwise_left + S (fpmp_left_dot_mcp_ics_linear_construct_second_raw_np_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_linear_construct_second_raw_np_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_linear_construct_second_raw_np_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_linear_construct_second_raw_np_cell_dot_pointwise_left. ff_left_mcp_cell_ics_linear_construct_second_raw_np_cell = ff_q_fpmp_dot_mcp_ics_linear_construct_second_raw_np_cell_dot_pointwise_left * S ((S (fpmp_index_dot_mcp_ics_linear_construct_second_raw_np_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_linear_construct_second_raw_np_cell) + (fpmp_left_dot_mcp_ics_linear_construct_second_raw_np_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_linear_construct_second_raw_np_cell_dot_pointwise_right. ff_h_fpmp_dot_mcp_ics_linear_construct_second_raw_np_cell_dot_pointwise_right + S (fpmp_right_dot_mcp_ics_linear_construct_second_raw_np_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_linear_construct_second_raw_np_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_linear_construct_second_raw_np_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_linear_construct_second_raw_np_cell_dot_pointwise_right. ff_right_mcp_cell_ics_linear_construct_second_raw_np_cell = ff_q_fpmp_dot_mcp_ics_linear_construct_second_raw_np_cell_dot_pointwise_right * S ((S (fpmp_index_dot_mcp_ics_linear_construct_second_raw_np_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_linear_construct_second_raw_np_cell) + (fpmp_right_dot_mcp_ics_linear_construct_second_raw_np_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_linear_construct_second_raw_np_cell_dot_pointwise_target. ff_h_fpmp_dot_mcp_ics_linear_construct_second_raw_np_cell_dot_pointwise_target + S (fpmp_target_dot_mcp_ics_linear_construct_second_raw_np_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_linear_construct_second_raw_np_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_linear_construct_second_raw_np_cell_dot)) /\ exists ff_q_fpmp_dot_mcp_ics_linear_construct_second_raw_np_cell_dot_pointwise_target. ff_code_dot_mcp_ics_linear_construct_second_raw_np_cell_dot = ff_q_fpmp_dot_mcp_ics_linear_construct_second_raw_np_cell_dot_pointwise_target * S ((S (fpmp_index_dot_mcp_ics_linear_construct_second_raw_np_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_linear_construct_second_raw_np_cell_dot) + (fpmp_target_dot_mcp_ics_linear_construct_second_raw_np_cell_dot_pointwise))) -> fpmp_target_dot_mcp_ics_linear_construct_second_raw_np_cell_dot_pointwise = fpmp_left_dot_mcp_ics_linear_construct_second_raw_np_cell_dot_pointwise * fpmp_right_dot_mcp_ics_linear_construct_second_raw_np_cell_dot_pointwise) /\ (exists ff_u_dot_mcp_ics_linear_construct_second_raw_np_cell_dot_sum ff_v_dot_mcp_ics_linear_construct_second_raw_np_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_linear_construct_second_raw_np_cell_dot_sum_start. ff_h_dot_mcp_ics_linear_construct_second_raw_np_cell_dot_sum_start + S (0) = S ((S (0)) * ff_v_dot_mcp_ics_linear_construct_second_raw_np_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_linear_construct_second_raw_np_cell_dot_sum_start. ff_u_dot_mcp_ics_linear_construct_second_raw_np_cell_dot_sum = ff_q_dot_mcp_ics_linear_construct_second_raw_np_cell_dot_sum_start * S ((S (0)) * ff_v_dot_mcp_ics_linear_construct_second_raw_np_cell_dot_sum) + (0))) /\ ((((exists ff_h_dot_mcp_ics_linear_construct_second_raw_np_cell_dot_sum_terminal. ff_h_dot_mcp_ics_linear_construct_second_raw_np_cell_dot_sum_terminal + S (ff_value_mcp_prefix_ics_linear_construct_second_raw_np) = S ((S (w)) * ff_v_dot_mcp_ics_linear_construct_second_raw_np_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_linear_construct_second_raw_np_cell_dot_sum_terminal. ff_u_dot_mcp_ics_linear_construct_second_raw_np_cell_dot_sum = ff_q_dot_mcp_ics_linear_construct_second_raw_np_cell_dot_sum_terminal * S ((S (w)) * ff_v_dot_mcp_ics_linear_construct_second_raw_np_cell_dot_sum) + (ff_value_mcp_prefix_ics_linear_construct_second_raw_np))) /\ forall ff_i_dot_mcp_ics_linear_construct_second_raw_np_cell_dot_sum. (exists ff_lt_dot_mcp_ics_linear_construct_second_raw_np_cell_dot_sum_bound. ff_lt_dot_mcp_ics_linear_construct_second_raw_np_cell_dot_sum_bound + S ff_i_dot_mcp_ics_linear_construct_second_raw_np_cell_dot_sum = w) -> exists ff_a_dot_mcp_ics_linear_construct_second_raw_np_cell_dot_sum ff_r_dot_mcp_ics_linear_construct_second_raw_np_cell_dot_sum ff_s_dot_mcp_ics_linear_construct_second_raw_np_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_linear_construct_second_raw_np_cell_dot_sum_summand. ff_h_dot_mcp_ics_linear_construct_second_raw_np_cell_dot_sum_summand + S (ff_a_dot_mcp_ics_linear_construct_second_raw_np_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_linear_construct_second_raw_np_cell_dot_sum)) * ff_scale_dot_mcp_ics_linear_construct_second_raw_np_cell_dot)) /\ exists ff_q_dot_mcp_ics_linear_construct_second_raw_np_cell_dot_sum_summand. ff_code_dot_mcp_ics_linear_construct_second_raw_np_cell_dot = ff_q_dot_mcp_ics_linear_construct_second_raw_np_cell_dot_sum_summand * S ((S (ff_i_dot_mcp_ics_linear_construct_second_raw_np_cell_dot_sum)) * ff_scale_dot_mcp_ics_linear_construct_second_raw_np_cell_dot) + (ff_a_dot_mcp_ics_linear_construct_second_raw_np_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_linear_construct_second_raw_np_cell_dot_sum_partial. ff_h_dot_mcp_ics_linear_construct_second_raw_np_cell_dot_sum_partial + S (ff_r_dot_mcp_ics_linear_construct_second_raw_np_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_linear_construct_second_raw_np_cell_dot_sum)) * ff_v_dot_mcp_ics_linear_construct_second_raw_np_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_linear_construct_second_raw_np_cell_dot_sum_partial. ff_u_dot_mcp_ics_linear_construct_second_raw_np_cell_dot_sum = ff_q_dot_mcp_ics_linear_construct_second_raw_np_cell_dot_sum_partial * S ((S (ff_i_dot_mcp_ics_linear_construct_second_raw_np_cell_dot_sum)) * ff_v_dot_mcp_ics_linear_construct_second_raw_np_cell_dot_sum) + (ff_r_dot_mcp_ics_linear_construct_second_raw_np_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_linear_construct_second_raw_np_cell_dot_sum_successor. ff_h_dot_mcp_ics_linear_construct_second_raw_np_cell_dot_sum_successor + S (ff_s_dot_mcp_ics_linear_construct_second_raw_np_cell_dot_sum) = S ((S (S ff_i_dot_mcp_ics_linear_construct_second_raw_np_cell_dot_sum)) * ff_v_dot_mcp_ics_linear_construct_second_raw_np_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_linear_construct_second_raw_np_cell_dot_sum_successor. ff_u_dot_mcp_ics_linear_construct_second_raw_np_cell_dot_sum = ff_q_dot_mcp_ics_linear_construct_second_raw_np_cell_dot_sum_successor * S ((S (S ff_i_dot_mcp_ics_linear_construct_second_raw_np_cell_dot_sum)) * ff_v_dot_mcp_ics_linear_construct_second_raw_np_cell_dot_sum) + (ff_s_dot_mcp_ics_linear_construct_second_raw_np_cell_dot_sum))) /\ ff_s_dot_mcp_ics_linear_construct_second_raw_np_cell_dot_sum = ff_r_dot_mcp_ics_linear_construct_second_raw_np_cell_dot_sum + ff_a_dot_mcp_ics_linear_construct_second_raw_np_cell_dot_sum))))))))))) /\ (((exists fs_h_mcp_ics_linear_construct_second_raw_np_entry. fs_h_mcp_ics_linear_construct_second_raw_np_entry + S (ff_value_mcp_prefix_ics_linear_construct_second_raw_np) = S ((S (ff_index_mcp_prefix_ics_linear_construct_second_raw_np)) * ff_nps_mcp_smatrix_ics_linear_construct_second_raw)) /\ exists fs_q_mcp_ics_linear_construct_second_raw_np_entry. ff_np_mcp_smatrix_ics_linear_construct_second_raw = fs_q_mcp_ics_linear_construct_second_raw_np_entry * S ((S (ff_index_mcp_prefix_ics_linear_construct_second_raw_np)) * ff_nps_mcp_smatrix_ics_linear_construct_second_raw) + (ff_value_mcp_prefix_ics_linear_construct_second_raw_np))))))) /\ ((forall ff_index_mcp_add_ics_linear_construct_second_raw_positive ff_left_mcp_add_ics_linear_construct_second_raw_positive ff_right_mcp_add_ics_linear_construct_second_raw_positive ff_target_mcp_add_ics_linear_construct_second_raw_positive. (exists mcp_gap_ics_linear_construct_second_raw_positive_bound. mcp_gap_ics_linear_construct_second_raw_positive_bound + S (ff_index_mcp_add_ics_linear_construct_second_raw_positive) = ((r) * (1))) -> (((exists fs_h_mcp_ics_linear_construct_second_raw_positive_left. fs_h_mcp_ics_linear_construct_second_raw_positive_left + S (ff_left_mcp_add_ics_linear_construct_second_raw_positive) = S ((S (ff_index_mcp_add_ics_linear_construct_second_raw_positive)) * ff_pps_mcp_smatrix_ics_linear_construct_second_raw)) /\ exists fs_q_mcp_ics_linear_construct_second_raw_positive_left. ff_pp_mcp_smatrix_ics_linear_construct_second_raw = fs_q_mcp_ics_linear_construct_second_raw_positive_left * S ((S (ff_index_mcp_add_ics_linear_construct_second_raw_positive)) * ff_pps_mcp_smatrix_ics_linear_construct_second_raw) + (ff_left_mcp_add_ics_linear_construct_second_raw_positive))) -> (((exists fs_h_mcp_ics_linear_construct_second_raw_positive_right. fs_h_mcp_ics_linear_construct_second_raw_positive_right + S (ff_right_mcp_add_ics_linear_construct_second_raw_positive) = S ((S (ff_index_mcp_add_ics_linear_construct_second_raw_positive)) * ff_nns_mcp_smatrix_ics_linear_construct_second_raw)) /\ exists fs_q_mcp_ics_linear_construct_second_raw_positive_right. ff_nn_mcp_smatrix_ics_linear_construct_second_raw = fs_q_mcp_ics_linear_construct_second_raw_positive_right * S ((S (ff_index_mcp_add_ics_linear_construct_second_raw_positive)) * ff_nns_mcp_smatrix_ics_linear_construct_second_raw) + (ff_right_mcp_add_ics_linear_construct_second_raw_positive))) -> (((exists fs_h_mcp_ics_linear_construct_second_raw_positive_target. fs_h_mcp_ics_linear_construct_second_raw_positive_target + S (ff_target_mcp_add_ics_linear_construct_second_raw_positive) = S ((S (ff_index_mcp_add_ics_linear_construct_second_raw_positive)) * ics_raw_positive_scale_linear_construct_second)) /\ exists fs_q_mcp_ics_linear_construct_second_raw_positive_target. ics_raw_positive_linear_construct_second = fs_q_mcp_ics_linear_construct_second_raw_positive_target * S ((S (ff_index_mcp_add_ics_linear_construct_second_raw_positive)) * ics_raw_positive_scale_linear_construct_second) + (ff_target_mcp_add_ics_linear_construct_second_raw_positive))) -> ff_target_mcp_add_ics_linear_construct_second_raw_positive = ff_left_mcp_add_ics_linear_construct_second_raw_positive + ff_right_mcp_add_ics_linear_construct_second_raw_positive) /\ (forall ff_index_mcp_add_ics_linear_construct_second_raw_negative ff_left_mcp_add_ics_linear_construct_second_raw_negative ff_right_mcp_add_ics_linear_construct_second_raw_negative ff_target_mcp_add_ics_linear_construct_second_raw_negative. (exists mcp_gap_ics_linear_construct_second_raw_negative_bound. mcp_gap_ics_linear_construct_second_raw_negative_bound + S (ff_index_mcp_add_ics_linear_construct_second_raw_negative) = ((r) * (1))) -> (((exists fs_h_mcp_ics_linear_construct_second_raw_negative_left. fs_h_mcp_ics_linear_construct_second_raw_negative_left + S (ff_left_mcp_add_ics_linear_construct_second_raw_negative) = S ((S (ff_index_mcp_add_ics_linear_construct_second_raw_negative)) * ff_pns_mcp_smatrix_ics_linear_construct_second_raw)) /\ exists fs_q_mcp_ics_linear_construct_second_raw_negative_left. ff_pn_mcp_smatrix_ics_linear_construct_second_raw = fs_q_mcp_ics_linear_construct_second_raw_negative_left * S ((S (ff_index_mcp_add_ics_linear_construct_second_raw_negative)) * ff_pns_mcp_smatrix_ics_linear_construct_second_raw) + (ff_left_mcp_add_ics_linear_construct_second_raw_negative))) -> (((exists fs_h_mcp_ics_linear_construct_second_raw_negative_right. fs_h_mcp_ics_linear_construct_second_raw_negative_right + S (ff_right_mcp_add_ics_linear_construct_second_raw_negative) = S ((S (ff_index_mcp_add_ics_linear_construct_second_raw_negative)) * ff_nps_mcp_smatrix_ics_linear_construct_second_raw)) /\ exists fs_q_mcp_ics_linear_construct_second_raw_negative_right. ff_np_mcp_smatrix_ics_linear_construct_second_raw = fs_q_mcp_ics_linear_construct_second_raw_negative_right * S ((S (ff_index_mcp_add_ics_linear_construct_second_raw_negative)) * ff_nps_mcp_smatrix_ics_linear_construct_second_raw) + (ff_right_mcp_add_ics_linear_construct_second_raw_negative))) -> (((exists fs_h_mcp_ics_linear_construct_second_raw_negative_target. fs_h_mcp_ics_linear_construct_second_raw_negative_target + S (ff_target_mcp_add_ics_linear_construct_second_raw_negative) = S ((S (ff_index_mcp_add_ics_linear_construct_second_raw_negative)) * ics_raw_negative_scale_linear_construct_second)) /\ exists fs_q_mcp_ics_linear_construct_second_raw_negative_target. ics_raw_negative_linear_construct_second = fs_q_mcp_ics_linear_construct_second_raw_negative_target * S ((S (ff_index_mcp_add_ics_linear_construct_second_raw_negative)) * ics_raw_negative_scale_linear_construct_second) + (ff_target_mcp_add_ics_linear_construct_second_raw_negative))) -> ff_target_mcp_add_ics_linear_construct_second_raw_negative = ff_left_mcp_add_ics_linear_construct_second_raw_negative + ff_right_mcp_add_ics_linear_construct_second_raw_negative))))))) /\ (forall ics_index_linear_construct_second_equal ics_value0_linear_construct_second_equal ics_value1_linear_construct_second_equal ics_value2_linear_construct_second_equal ics_value3_linear_construct_second_equal. (exists ics_gap_linear_construct_second_equal_bound. ics_gap_linear_construct_second_equal_bound + S (ics_index_linear_construct_second_equal) = (r)) -> (((exists fs_h_ics_linear_construct_second_equal_at0. fs_h_ics_linear_construct_second_equal_at0 + S (ics_value0_linear_construct_second_equal) = S ((S (ics_index_linear_construct_second_equal)) * ics_raw_positive_scale_linear_construct_second)) /\ exists fs_q_ics_linear_construct_second_equal_at0. ics_raw_positive_linear_construct_second = fs_q_ics_linear_construct_second_equal_at0 * S ((S (ics_index_linear_construct_second_equal)) * ics_raw_positive_scale_linear_construct_second) + (ics_value0_linear_construct_second_equal))) -> (((exists fs_h_ics_linear_construct_second_equal_at1. fs_h_ics_linear_construct_second_equal_at1 + S (ics_value1_linear_construct_second_equal) = S ((S (ics_index_linear_construct_second_equal)) * ics_raw_negative_scale_linear_construct_second)) /\ exists fs_q_ics_linear_construct_second_equal_at1. ics_raw_negative_linear_construct_second = fs_q_ics_linear_construct_second_equal_at1 * S ((S (ics_index_linear_construct_second_equal)) * ics_raw_negative_scale_linear_construct_second) + (ics_value1_linear_construct_second_equal))) -> (((exists fs_h_ics_linear_construct_second_equal_at2. fs_h_ics_linear_construct_second_equal_at2 + S (ics_value2_linear_construct_second_equal) = S ((S (ics_index_linear_construct_second_equal)) * qc)) /\ exists fs_q_ics_linear_construct_second_equal_at2. qb = fs_q_ics_linear_construct_second_equal_at2 * S ((S (ics_index_linear_construct_second_equal)) * qc) + (ics_value2_linear_construct_second_equal))) -> (((exists fs_h_ics_linear_construct_second_equal_at3. fs_h_ics_linear_construct_second_equal_at3 + S (ics_value3_linear_construct_second_equal) = S ((S (ics_index_linear_construct_second_equal)) * mc)) /\ exists fs_q_ics_linear_construct_second_equal_at3. mb = fs_q_ics_linear_construct_second_equal_at3 * S ((S (ics_index_linear_construct_second_equal)) * mc) + (ics_value3_linear_construct_second_equal))) -> ics_value0_linear_construct_second_equal + ics_value3_linear_construct_second_equal = ics_value2_linear_construct_second_equal + ics_value1_linear_construct_second_equal)))) -> (forall ics_index_linear_construct_sum ics_value0_linear_construct_sum ics_value1_linear_construct_sum ics_value2_linear_construct_sum ics_value3_linear_construct_sum ics_value4_linear_construct_sum ics_value5_linear_construct_sum. (exists ics_gap_linear_construct_sum_bound. ics_gap_linear_construct_sum_bound + S (ics_index_linear_construct_sum) = (r)) -> (((exists fs_h_ics_linear_construct_sum_at0. fs_h_ics_linear_construct_sum_at0 + S (ics_value0_linear_construct_sum) = S ((S (ics_index_linear_construct_sum)) * pc)) /\ exists fs_q_ics_linear_construct_sum_at0. pb = fs_q_ics_linear_construct_sum_at0 * S ((S (ics_index_linear_construct_sum)) * pc) + (ics_value0_linear_construct_sum))) -> (((exists fs_h_ics_linear_construct_sum_at1. fs_h_ics_linear_construct_sum_at1 + S (ics_value1_linear_construct_sum) = S ((S (ics_index_linear_construct_sum)) * nc)) /\ exists fs_q_ics_linear_construct_sum_at1. nb = fs_q_ics_linear_construct_sum_at1 * S ((S (ics_index_linear_construct_sum)) * nc) + (ics_value1_linear_construct_sum))) -> (((exists fs_h_ics_linear_construct_sum_at2. fs_h_ics_linear_construct_sum_at2 + S (ics_value2_linear_construct_sum) = S ((S (ics_index_linear_construct_sum)) * qc)) /\ exists fs_q_ics_linear_construct_sum_at2. qb = fs_q_ics_linear_construct_sum_at2 * S ((S (ics_index_linear_construct_sum)) * qc) + (ics_value2_linear_construct_sum))) -> (((exists fs_h_ics_linear_construct_sum_at3. fs_h_ics_linear_construct_sum_at3 + S (ics_value3_linear_construct_sum) = S ((S (ics_index_linear_construct_sum)) * mc)) /\ exists fs_q_ics_linear_construct_sum_at3. mb = fs_q_ics_linear_construct_sum_at3 * S ((S (ics_index_linear_construct_sum)) * mc) + (ics_value3_linear_construct_sum))) -> (((exists fs_h_ics_linear_construct_sum_at4. fs_h_ics_linear_construct_sum_at4 + S (ics_value4_linear_construct_sum) = S ((S (ics_index_linear_construct_sum)) * rc)) /\ exists fs_q_ics_linear_construct_sum_at4. rb = fs_q_ics_linear_construct_sum_at4 * S ((S (ics_index_linear_construct_sum)) * rc) + (ics_value4_linear_construct_sum))) -> (((exists fs_h_ics_linear_construct_sum_at5. fs_h_ics_linear_construct_sum_at5 + S (ics_value5_linear_construct_sum) = S ((S (ics_index_linear_construct_sum)) * sc)) /\ exists fs_q_ics_linear_construct_sum_at5. sb = fs_q_ics_linear_construct_sum_at5 * S ((S (ics_index_linear_construct_sum)) * sc) + (ics_value5_linear_construct_sum))) -> ics_value4_linear_construct_sum + (ics_value1_linear_construct_sum + ics_value3_linear_construct_sum) = (ics_value0_linear_construct_sum + ics_value2_linear_construct_sum) + ics_value5_linear_construct_sum) -> exists ib ic jb jc. (((forall ff_index_mcp_add_ics_linear_constructed_p ff_left_mcp_add_ics_linear_constructed_p ff_right_mcp_add_ics_linear_constructed_p ff_target_mcp_add_ics_linear_constructed_p. (exists mcp_gap_ics_linear_constructed_p_bound. mcp_gap_ics_linear_constructed_p_bound + S (ff_index_mcp_add_ics_linear_constructed_p) = (w)) -> (((exists fs_h_mcp_ics_linear_constructed_p_left. fs_h_mcp_ics_linear_constructed_p_left + S (ff_left_mcp_add_ics_linear_constructed_p) = S ((S (ff_index_mcp_add_ics_linear_constructed_p)) * ec)) /\ exists fs_q_mcp_ics_linear_constructed_p_left. eb = fs_q_mcp_ics_linear_constructed_p_left * S ((S (ff_index_mcp_add_ics_linear_constructed_p)) * ec) + (ff_left_mcp_add_ics_linear_constructed_p))) -> (((exists fs_h_mcp_ics_linear_constructed_p_right. fs_h_mcp_ics_linear_constructed_p_right + S (ff_right_mcp_add_ics_linear_constructed_p) = S ((S (ff_index_mcp_add_ics_linear_constructed_p)) * gc)) /\ exists fs_q_mcp_ics_linear_constructed_p_right. gb = fs_q_mcp_ics_linear_constructed_p_right * S ((S (ff_index_mcp_add_ics_linear_constructed_p)) * gc) + (ff_right_mcp_add_ics_linear_constructed_p))) -> (((exists fs_h_mcp_ics_linear_constructed_p_target. fs_h_mcp_ics_linear_constructed_p_target + S (ff_target_mcp_add_ics_linear_constructed_p) = S ((S (ff_index_mcp_add_ics_linear_constructed_p)) * ic)) /\ exists fs_q_mcp_ics_linear_constructed_p_target. ib = fs_q_mcp_ics_linear_constructed_p_target * S ((S (ff_index_mcp_add_ics_linear_constructed_p)) * ic) + (ff_target_mcp_add_ics_linear_constructed_p))) -> ff_target_mcp_add_ics_linear_constructed_p = ff_left_mcp_add_ics_linear_constructed_p + ff_right_mcp_add_ics_linear_constructed_p) /\ (((forall ff_index_mcp_add_ics_linear_constructed_n ff_left_mcp_add_ics_linear_constructed_n ff_right_mcp_add_ics_linear_constructed_n ff_target_mcp_add_ics_linear_constructed_n. (exists mcp_gap_ics_linear_constructed_n_bound. mcp_gap_ics_linear_constructed_n_bound + S (ff_index_mcp_add_ics_linear_constructed_n) = (w)) -> (((exists fs_h_mcp_ics_linear_constructed_n_left. fs_h_mcp_ics_linear_constructed_n_left + S (ff_left_mcp_add_ics_linear_constructed_n) = S ((S (ff_index_mcp_add_ics_linear_constructed_n)) * fc)) /\ exists fs_q_mcp_ics_linear_constructed_n_left. fb = fs_q_mcp_ics_linear_constructed_n_left * S ((S (ff_index_mcp_add_ics_linear_constructed_n)) * fc) + (ff_left_mcp_add_ics_linear_constructed_n))) -> (((exists fs_h_mcp_ics_linear_constructed_n_right. fs_h_mcp_ics_linear_constructed_n_right + S (ff_right_mcp_add_ics_linear_constructed_n) = S ((S (ff_index_mcp_add_ics_linear_constructed_n)) * hc)) /\ exists fs_q_mcp_ics_linear_constructed_n_right. hb = fs_q_mcp_ics_linear_constructed_n_right * S ((S (ff_index_mcp_add_ics_linear_constructed_n)) * hc) + (ff_right_mcp_add_ics_linear_constructed_n))) -> (((exists fs_h_mcp_ics_linear_constructed_n_target. fs_h_mcp_ics_linear_constructed_n_target + S (ff_target_mcp_add_ics_linear_constructed_n) = S ((S (ff_index_mcp_add_ics_linear_constructed_n)) * jc)) /\ exists fs_q_mcp_ics_linear_constructed_n_target. jb = fs_q_mcp_ics_linear_constructed_n_target * S ((S (ff_index_mcp_add_ics_linear_constructed_n)) * jc) + (ff_target_mcp_add_ics_linear_constructed_n))) -> ff_target_mcp_add_ics_linear_constructed_n = ff_left_mcp_add_ics_linear_constructed_n + ff_right_mcp_add_ics_linear_constructed_n) /\ (exists ics_raw_positive_linear_constructed_image ics_raw_positive_scale_linear_constructed_image ics_raw_negative_linear_constructed_image ics_raw_negative_scale_linear_constructed_image. (((exists ff_pp_mcp_smatrix_ics_linear_constructed_image_raw ff_pps_mcp_smatrix_ics_linear_constructed_image_raw ff_nn_mcp_smatrix_ics_linear_constructed_image_raw ff_nns_mcp_smatrix_ics_linear_constructed_image_raw ff_pn_mcp_smatrix_ics_linear_constructed_image_raw ff_pns_mcp_smatrix_ics_linear_constructed_image_raw ff_np_mcp_smatrix_ics_linear_constructed_image_raw ff_nps_mcp_smatrix_ics_linear_constructed_image_raw. ((forall ff_index_mcp_prefix_ics_linear_constructed_image_raw_pp. (exists mcp_gap_ics_linear_constructed_image_raw_pp_index. mcp_gap_ics_linear_constructed_image_raw_pp_index + S (ff_index_mcp_prefix_ics_linear_constructed_image_raw_pp) = ((r) * (1))) -> exists ff_row_mcp_prefix_ics_linear_constructed_image_raw_pp ff_column_mcp_prefix_ics_linear_constructed_image_raw_pp ff_value_mcp_prefix_ics_linear_constructed_image_raw_pp. ((ff_index_mcp_prefix_ics_linear_constructed_image_raw_pp) = (1) * ff_row_mcp_prefix_ics_linear_constructed_image_raw_pp + ff_column_mcp_prefix_ics_linear_constructed_image_raw_pp /\ ((exists mcp_gap_ics_linear_constructed_image_raw_pp_column. mcp_gap_ics_linear_constructed_image_raw_pp_column + S (ff_column_mcp_prefix_ics_linear_constructed_image_raw_pp) = (1)) /\ ((exists ff_left_mcp_cell_ics_linear_constructed_image_raw_pp_cell ff_left_scale_mcp_cell_ics_linear_constructed_image_raw_pp_cell ff_right_mcp_cell_ics_linear_constructed_image_raw_pp_cell ff_right_scale_mcp_cell_ics_linear_constructed_image_raw_pp_cell. ((forall ff_index_mcp_ics_linear_constructed_image_raw_pp_cell_row ff_source_mcp_ics_linear_constructed_image_raw_pp_cell_row ff_target_mcp_ics_linear_constructed_image_raw_pp_cell_row. (exists mcp_gap_ics_linear_constructed_image_raw_pp_cell_row_bound. mcp_gap_ics_linear_constructed_image_raw_pp_cell_row_bound + S (ff_index_mcp_ics_linear_constructed_image_raw_pp_cell_row) = (w)) -> (((exists fs_h_mcp_ics_linear_constructed_image_raw_pp_cell_row_source. fs_h_mcp_ics_linear_constructed_image_raw_pp_cell_row_source + S (ff_source_mcp_ics_linear_constructed_image_raw_pp_cell_row) = S ((S (((ff_row_mcp_prefix_ics_linear_constructed_image_raw_pp) * (w)) + (1) * ff_index_mcp_ics_linear_constructed_image_raw_pp_cell_row)) * ac)) /\ exists fs_q_mcp_ics_linear_constructed_image_raw_pp_cell_row_source. ab = fs_q_mcp_ics_linear_constructed_image_raw_pp_cell_row_source * S ((S (((ff_row_mcp_prefix_ics_linear_constructed_image_raw_pp) * (w)) + (1) * ff_index_mcp_ics_linear_constructed_image_raw_pp_cell_row)) * ac) + (ff_source_mcp_ics_linear_constructed_image_raw_pp_cell_row))) -> (((exists fs_h_mcp_ics_linear_constructed_image_raw_pp_cell_row_target. fs_h_mcp_ics_linear_constructed_image_raw_pp_cell_row_target + S (ff_target_mcp_ics_linear_constructed_image_raw_pp_cell_row) = S ((S (ff_index_mcp_ics_linear_constructed_image_raw_pp_cell_row)) * ff_left_scale_mcp_cell_ics_linear_constructed_image_raw_pp_cell)) /\ exists fs_q_mcp_ics_linear_constructed_image_raw_pp_cell_row_target. ff_left_mcp_cell_ics_linear_constructed_image_raw_pp_cell = fs_q_mcp_ics_linear_constructed_image_raw_pp_cell_row_target * S ((S (ff_index_mcp_ics_linear_constructed_image_raw_pp_cell_row)) * ff_left_scale_mcp_cell_ics_linear_constructed_image_raw_pp_cell) + (ff_target_mcp_ics_linear_constructed_image_raw_pp_cell_row))) -> ff_target_mcp_ics_linear_constructed_image_raw_pp_cell_row = ff_source_mcp_ics_linear_constructed_image_raw_pp_cell_row) /\ ((forall ff_index_mcp_ics_linear_constructed_image_raw_pp_cell_column ff_source_mcp_ics_linear_constructed_image_raw_pp_cell_column ff_target_mcp_ics_linear_constructed_image_raw_pp_cell_column. (exists mcp_gap_ics_linear_constructed_image_raw_pp_cell_column_bound. mcp_gap_ics_linear_constructed_image_raw_pp_cell_column_bound + S (ff_index_mcp_ics_linear_constructed_image_raw_pp_cell_column) = (w)) -> (((exists fs_h_mcp_ics_linear_constructed_image_raw_pp_cell_column_source. fs_h_mcp_ics_linear_constructed_image_raw_pp_cell_column_source + S (ff_source_mcp_ics_linear_constructed_image_raw_pp_cell_column) = S ((S ((ff_column_mcp_prefix_ics_linear_constructed_image_raw_pp) + (1) * ff_index_mcp_ics_linear_constructed_image_raw_pp_cell_column)) * ic)) /\ exists fs_q_mcp_ics_linear_constructed_image_raw_pp_cell_column_source. ib = fs_q_mcp_ics_linear_constructed_image_raw_pp_cell_column_source * S ((S ((ff_column_mcp_prefix_ics_linear_constructed_image_raw_pp) + (1) * ff_index_mcp_ics_linear_constructed_image_raw_pp_cell_column)) * ic) + (ff_source_mcp_ics_linear_constructed_image_raw_pp_cell_column))) -> (((exists fs_h_mcp_ics_linear_constructed_image_raw_pp_cell_column_target. fs_h_mcp_ics_linear_constructed_image_raw_pp_cell_column_target + S (ff_target_mcp_ics_linear_constructed_image_raw_pp_cell_column) = S ((S (ff_index_mcp_ics_linear_constructed_image_raw_pp_cell_column)) * ff_right_scale_mcp_cell_ics_linear_constructed_image_raw_pp_cell)) /\ exists fs_q_mcp_ics_linear_constructed_image_raw_pp_cell_column_target. ff_right_mcp_cell_ics_linear_constructed_image_raw_pp_cell = fs_q_mcp_ics_linear_constructed_image_raw_pp_cell_column_target * S ((S (ff_index_mcp_ics_linear_constructed_image_raw_pp_cell_column)) * ff_right_scale_mcp_cell_ics_linear_constructed_image_raw_pp_cell) + (ff_target_mcp_ics_linear_constructed_image_raw_pp_cell_column))) -> ff_target_mcp_ics_linear_constructed_image_raw_pp_cell_column = ff_source_mcp_ics_linear_constructed_image_raw_pp_cell_column) /\ (exists ff_code_dot_mcp_ics_linear_constructed_image_raw_pp_cell_dot ff_scale_dot_mcp_ics_linear_constructed_image_raw_pp_cell_dot. ((forall fpmp_index_dot_mcp_ics_linear_constructed_image_raw_pp_cell_dot_pointwise fpmp_left_dot_mcp_ics_linear_constructed_image_raw_pp_cell_dot_pointwise fpmp_right_dot_mcp_ics_linear_constructed_image_raw_pp_cell_dot_pointwise fpmp_target_dot_mcp_ics_linear_constructed_image_raw_pp_cell_dot_pointwise. (exists fpmp_gap_dot_mcp_ics_linear_constructed_image_raw_pp_cell_dot_pointwise. fpmp_gap_dot_mcp_ics_linear_constructed_image_raw_pp_cell_dot_pointwise + S fpmp_index_dot_mcp_ics_linear_constructed_image_raw_pp_cell_dot_pointwise = w) -> (((exists ff_h_fpmp_dot_mcp_ics_linear_constructed_image_raw_pp_cell_dot_pointwise_left. ff_h_fpmp_dot_mcp_ics_linear_constructed_image_raw_pp_cell_dot_pointwise_left + S (fpmp_left_dot_mcp_ics_linear_constructed_image_raw_pp_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_linear_constructed_image_raw_pp_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_linear_constructed_image_raw_pp_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_linear_constructed_image_raw_pp_cell_dot_pointwise_left. ff_left_mcp_cell_ics_linear_constructed_image_raw_pp_cell = ff_q_fpmp_dot_mcp_ics_linear_constructed_image_raw_pp_cell_dot_pointwise_left * S ((S (fpmp_index_dot_mcp_ics_linear_constructed_image_raw_pp_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_linear_constructed_image_raw_pp_cell) + (fpmp_left_dot_mcp_ics_linear_constructed_image_raw_pp_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_linear_constructed_image_raw_pp_cell_dot_pointwise_right. ff_h_fpmp_dot_mcp_ics_linear_constructed_image_raw_pp_cell_dot_pointwise_right + S (fpmp_right_dot_mcp_ics_linear_constructed_image_raw_pp_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_linear_constructed_image_raw_pp_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_linear_constructed_image_raw_pp_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_linear_constructed_image_raw_pp_cell_dot_pointwise_right. ff_right_mcp_cell_ics_linear_constructed_image_raw_pp_cell = ff_q_fpmp_dot_mcp_ics_linear_constructed_image_raw_pp_cell_dot_pointwise_right * S ((S (fpmp_index_dot_mcp_ics_linear_constructed_image_raw_pp_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_linear_constructed_image_raw_pp_cell) + (fpmp_right_dot_mcp_ics_linear_constructed_image_raw_pp_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_linear_constructed_image_raw_pp_cell_dot_pointwise_target. ff_h_fpmp_dot_mcp_ics_linear_constructed_image_raw_pp_cell_dot_pointwise_target + S (fpmp_target_dot_mcp_ics_linear_constructed_image_raw_pp_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_linear_constructed_image_raw_pp_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_linear_constructed_image_raw_pp_cell_dot)) /\ exists ff_q_fpmp_dot_mcp_ics_linear_constructed_image_raw_pp_cell_dot_pointwise_target. ff_code_dot_mcp_ics_linear_constructed_image_raw_pp_cell_dot = ff_q_fpmp_dot_mcp_ics_linear_constructed_image_raw_pp_cell_dot_pointwise_target * S ((S (fpmp_index_dot_mcp_ics_linear_constructed_image_raw_pp_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_linear_constructed_image_raw_pp_cell_dot) + (fpmp_target_dot_mcp_ics_linear_constructed_image_raw_pp_cell_dot_pointwise))) -> fpmp_target_dot_mcp_ics_linear_constructed_image_raw_pp_cell_dot_pointwise = fpmp_left_dot_mcp_ics_linear_constructed_image_raw_pp_cell_dot_pointwise * fpmp_right_dot_mcp_ics_linear_constructed_image_raw_pp_cell_dot_pointwise) /\ (exists ff_u_dot_mcp_ics_linear_constructed_image_raw_pp_cell_dot_sum ff_v_dot_mcp_ics_linear_constructed_image_raw_pp_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_linear_constructed_image_raw_pp_cell_dot_sum_start. ff_h_dot_mcp_ics_linear_constructed_image_raw_pp_cell_dot_sum_start + S (0) = S ((S (0)) * ff_v_dot_mcp_ics_linear_constructed_image_raw_pp_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_linear_constructed_image_raw_pp_cell_dot_sum_start. ff_u_dot_mcp_ics_linear_constructed_image_raw_pp_cell_dot_sum = ff_q_dot_mcp_ics_linear_constructed_image_raw_pp_cell_dot_sum_start * S ((S (0)) * ff_v_dot_mcp_ics_linear_constructed_image_raw_pp_cell_dot_sum) + (0))) /\ ((((exists ff_h_dot_mcp_ics_linear_constructed_image_raw_pp_cell_dot_sum_terminal. ff_h_dot_mcp_ics_linear_constructed_image_raw_pp_cell_dot_sum_terminal + S (ff_value_mcp_prefix_ics_linear_constructed_image_raw_pp) = S ((S (w)) * ff_v_dot_mcp_ics_linear_constructed_image_raw_pp_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_linear_constructed_image_raw_pp_cell_dot_sum_terminal. ff_u_dot_mcp_ics_linear_constructed_image_raw_pp_cell_dot_sum = ff_q_dot_mcp_ics_linear_constructed_image_raw_pp_cell_dot_sum_terminal * S ((S (w)) * ff_v_dot_mcp_ics_linear_constructed_image_raw_pp_cell_dot_sum) + (ff_value_mcp_prefix_ics_linear_constructed_image_raw_pp))) /\ forall ff_i_dot_mcp_ics_linear_constructed_image_raw_pp_cell_dot_sum. (exists ff_lt_dot_mcp_ics_linear_constructed_image_raw_pp_cell_dot_sum_bound. ff_lt_dot_mcp_ics_linear_constructed_image_raw_pp_cell_dot_sum_bound + S ff_i_dot_mcp_ics_linear_constructed_image_raw_pp_cell_dot_sum = w) -> exists ff_a_dot_mcp_ics_linear_constructed_image_raw_pp_cell_dot_sum ff_r_dot_mcp_ics_linear_constructed_image_raw_pp_cell_dot_sum ff_s_dot_mcp_ics_linear_constructed_image_raw_pp_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_linear_constructed_image_raw_pp_cell_dot_sum_summand. ff_h_dot_mcp_ics_linear_constructed_image_raw_pp_cell_dot_sum_summand + S (ff_a_dot_mcp_ics_linear_constructed_image_raw_pp_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_linear_constructed_image_raw_pp_cell_dot_sum)) * ff_scale_dot_mcp_ics_linear_constructed_image_raw_pp_cell_dot)) /\ exists ff_q_dot_mcp_ics_linear_constructed_image_raw_pp_cell_dot_sum_summand. ff_code_dot_mcp_ics_linear_constructed_image_raw_pp_cell_dot = ff_q_dot_mcp_ics_linear_constructed_image_raw_pp_cell_dot_sum_summand * S ((S (ff_i_dot_mcp_ics_linear_constructed_image_raw_pp_cell_dot_sum)) * ff_scale_dot_mcp_ics_linear_constructed_image_raw_pp_cell_dot) + (ff_a_dot_mcp_ics_linear_constructed_image_raw_pp_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_linear_constructed_image_raw_pp_cell_dot_sum_partial. ff_h_dot_mcp_ics_linear_constructed_image_raw_pp_cell_dot_sum_partial + S (ff_r_dot_mcp_ics_linear_constructed_image_raw_pp_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_linear_constructed_image_raw_pp_cell_dot_sum)) * ff_v_dot_mcp_ics_linear_constructed_image_raw_pp_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_linear_constructed_image_raw_pp_cell_dot_sum_partial. ff_u_dot_mcp_ics_linear_constructed_image_raw_pp_cell_dot_sum = ff_q_dot_mcp_ics_linear_constructed_image_raw_pp_cell_dot_sum_partial * S ((S (ff_i_dot_mcp_ics_linear_constructed_image_raw_pp_cell_dot_sum)) * ff_v_dot_mcp_ics_linear_constructed_image_raw_pp_cell_dot_sum) + (ff_r_dot_mcp_ics_linear_constructed_image_raw_pp_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_linear_constructed_image_raw_pp_cell_dot_sum_successor. ff_h_dot_mcp_ics_linear_constructed_image_raw_pp_cell_dot_sum_successor + S (ff_s_dot_mcp_ics_linear_constructed_image_raw_pp_cell_dot_sum) = S ((S (S ff_i_dot_mcp_ics_linear_constructed_image_raw_pp_cell_dot_sum)) * ff_v_dot_mcp_ics_linear_constructed_image_raw_pp_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_linear_constructed_image_raw_pp_cell_dot_sum_successor. ff_u_dot_mcp_ics_linear_constructed_image_raw_pp_cell_dot_sum = ff_q_dot_mcp_ics_linear_constructed_image_raw_pp_cell_dot_sum_successor * S ((S (S ff_i_dot_mcp_ics_linear_constructed_image_raw_pp_cell_dot_sum)) * ff_v_dot_mcp_ics_linear_constructed_image_raw_pp_cell_dot_sum) + (ff_s_dot_mcp_ics_linear_constructed_image_raw_pp_cell_dot_sum))) /\ ff_s_dot_mcp_ics_linear_constructed_image_raw_pp_cell_dot_sum = ff_r_dot_mcp_ics_linear_constructed_image_raw_pp_cell_dot_sum + ff_a_dot_mcp_ics_linear_constructed_image_raw_pp_cell_dot_sum))))))))))) /\ (((exists fs_h_mcp_ics_linear_constructed_image_raw_pp_entry. fs_h_mcp_ics_linear_constructed_image_raw_pp_entry + S (ff_value_mcp_prefix_ics_linear_constructed_image_raw_pp) = S ((S (ff_index_mcp_prefix_ics_linear_constructed_image_raw_pp)) * ff_pps_mcp_smatrix_ics_linear_constructed_image_raw)) /\ exists fs_q_mcp_ics_linear_constructed_image_raw_pp_entry. ff_pp_mcp_smatrix_ics_linear_constructed_image_raw = fs_q_mcp_ics_linear_constructed_image_raw_pp_entry * S ((S (ff_index_mcp_prefix_ics_linear_constructed_image_raw_pp)) * ff_pps_mcp_smatrix_ics_linear_constructed_image_raw) + (ff_value_mcp_prefix_ics_linear_constructed_image_raw_pp))))))) /\ ((forall ff_index_mcp_prefix_ics_linear_constructed_image_raw_nn. (exists mcp_gap_ics_linear_constructed_image_raw_nn_index. mcp_gap_ics_linear_constructed_image_raw_nn_index + S (ff_index_mcp_prefix_ics_linear_constructed_image_raw_nn) = ((r) * (1))) -> exists ff_row_mcp_prefix_ics_linear_constructed_image_raw_nn ff_column_mcp_prefix_ics_linear_constructed_image_raw_nn ff_value_mcp_prefix_ics_linear_constructed_image_raw_nn. ((ff_index_mcp_prefix_ics_linear_constructed_image_raw_nn) = (1) * ff_row_mcp_prefix_ics_linear_constructed_image_raw_nn + ff_column_mcp_prefix_ics_linear_constructed_image_raw_nn /\ ((exists mcp_gap_ics_linear_constructed_image_raw_nn_column. mcp_gap_ics_linear_constructed_image_raw_nn_column + S (ff_column_mcp_prefix_ics_linear_constructed_image_raw_nn) = (1)) /\ ((exists ff_left_mcp_cell_ics_linear_constructed_image_raw_nn_cell ff_left_scale_mcp_cell_ics_linear_constructed_image_raw_nn_cell ff_right_mcp_cell_ics_linear_constructed_image_raw_nn_cell ff_right_scale_mcp_cell_ics_linear_constructed_image_raw_nn_cell. ((forall ff_index_mcp_ics_linear_constructed_image_raw_nn_cell_row ff_source_mcp_ics_linear_constructed_image_raw_nn_cell_row ff_target_mcp_ics_linear_constructed_image_raw_nn_cell_row. (exists mcp_gap_ics_linear_constructed_image_raw_nn_cell_row_bound. mcp_gap_ics_linear_constructed_image_raw_nn_cell_row_bound + S (ff_index_mcp_ics_linear_constructed_image_raw_nn_cell_row) = (w)) -> (((exists fs_h_mcp_ics_linear_constructed_image_raw_nn_cell_row_source. fs_h_mcp_ics_linear_constructed_image_raw_nn_cell_row_source + S (ff_source_mcp_ics_linear_constructed_image_raw_nn_cell_row) = S ((S (((ff_row_mcp_prefix_ics_linear_constructed_image_raw_nn) * (w)) + (1) * ff_index_mcp_ics_linear_constructed_image_raw_nn_cell_row)) * dc)) /\ exists fs_q_mcp_ics_linear_constructed_image_raw_nn_cell_row_source. db = fs_q_mcp_ics_linear_constructed_image_raw_nn_cell_row_source * S ((S (((ff_row_mcp_prefix_ics_linear_constructed_image_raw_nn) * (w)) + (1) * ff_index_mcp_ics_linear_constructed_image_raw_nn_cell_row)) * dc) + (ff_source_mcp_ics_linear_constructed_image_raw_nn_cell_row))) -> (((exists fs_h_mcp_ics_linear_constructed_image_raw_nn_cell_row_target. fs_h_mcp_ics_linear_constructed_image_raw_nn_cell_row_target + S (ff_target_mcp_ics_linear_constructed_image_raw_nn_cell_row) = S ((S (ff_index_mcp_ics_linear_constructed_image_raw_nn_cell_row)) * ff_left_scale_mcp_cell_ics_linear_constructed_image_raw_nn_cell)) /\ exists fs_q_mcp_ics_linear_constructed_image_raw_nn_cell_row_target. ff_left_mcp_cell_ics_linear_constructed_image_raw_nn_cell = fs_q_mcp_ics_linear_constructed_image_raw_nn_cell_row_target * S ((S (ff_index_mcp_ics_linear_constructed_image_raw_nn_cell_row)) * ff_left_scale_mcp_cell_ics_linear_constructed_image_raw_nn_cell) + (ff_target_mcp_ics_linear_constructed_image_raw_nn_cell_row))) -> ff_target_mcp_ics_linear_constructed_image_raw_nn_cell_row = ff_source_mcp_ics_linear_constructed_image_raw_nn_cell_row) /\ ((forall ff_index_mcp_ics_linear_constructed_image_raw_nn_cell_column ff_source_mcp_ics_linear_constructed_image_raw_nn_cell_column ff_target_mcp_ics_linear_constructed_image_raw_nn_cell_column. (exists mcp_gap_ics_linear_constructed_image_raw_nn_cell_column_bound. mcp_gap_ics_linear_constructed_image_raw_nn_cell_column_bound + S (ff_index_mcp_ics_linear_constructed_image_raw_nn_cell_column) = (w)) -> (((exists fs_h_mcp_ics_linear_constructed_image_raw_nn_cell_column_source. fs_h_mcp_ics_linear_constructed_image_raw_nn_cell_column_source + S (ff_source_mcp_ics_linear_constructed_image_raw_nn_cell_column) = S ((S ((ff_column_mcp_prefix_ics_linear_constructed_image_raw_nn) + (1) * ff_index_mcp_ics_linear_constructed_image_raw_nn_cell_column)) * jc)) /\ exists fs_q_mcp_ics_linear_constructed_image_raw_nn_cell_column_source. jb = fs_q_mcp_ics_linear_constructed_image_raw_nn_cell_column_source * S ((S ((ff_column_mcp_prefix_ics_linear_constructed_image_raw_nn) + (1) * ff_index_mcp_ics_linear_constructed_image_raw_nn_cell_column)) * jc) + (ff_source_mcp_ics_linear_constructed_image_raw_nn_cell_column))) -> (((exists fs_h_mcp_ics_linear_constructed_image_raw_nn_cell_column_target. fs_h_mcp_ics_linear_constructed_image_raw_nn_cell_column_target + S (ff_target_mcp_ics_linear_constructed_image_raw_nn_cell_column) = S ((S (ff_index_mcp_ics_linear_constructed_image_raw_nn_cell_column)) * ff_right_scale_mcp_cell_ics_linear_constructed_image_raw_nn_cell)) /\ exists fs_q_mcp_ics_linear_constructed_image_raw_nn_cell_column_target. ff_right_mcp_cell_ics_linear_constructed_image_raw_nn_cell = fs_q_mcp_ics_linear_constructed_image_raw_nn_cell_column_target * S ((S (ff_index_mcp_ics_linear_constructed_image_raw_nn_cell_column)) * ff_right_scale_mcp_cell_ics_linear_constructed_image_raw_nn_cell) + (ff_target_mcp_ics_linear_constructed_image_raw_nn_cell_column))) -> ff_target_mcp_ics_linear_constructed_image_raw_nn_cell_column = ff_source_mcp_ics_linear_constructed_image_raw_nn_cell_column) /\ (exists ff_code_dot_mcp_ics_linear_constructed_image_raw_nn_cell_dot ff_scale_dot_mcp_ics_linear_constructed_image_raw_nn_cell_dot. ((forall fpmp_index_dot_mcp_ics_linear_constructed_image_raw_nn_cell_dot_pointwise fpmp_left_dot_mcp_ics_linear_constructed_image_raw_nn_cell_dot_pointwise fpmp_right_dot_mcp_ics_linear_constructed_image_raw_nn_cell_dot_pointwise fpmp_target_dot_mcp_ics_linear_constructed_image_raw_nn_cell_dot_pointwise. (exists fpmp_gap_dot_mcp_ics_linear_constructed_image_raw_nn_cell_dot_pointwise. fpmp_gap_dot_mcp_ics_linear_constructed_image_raw_nn_cell_dot_pointwise + S fpmp_index_dot_mcp_ics_linear_constructed_image_raw_nn_cell_dot_pointwise = w) -> (((exists ff_h_fpmp_dot_mcp_ics_linear_constructed_image_raw_nn_cell_dot_pointwise_left. ff_h_fpmp_dot_mcp_ics_linear_constructed_image_raw_nn_cell_dot_pointwise_left + S (fpmp_left_dot_mcp_ics_linear_constructed_image_raw_nn_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_linear_constructed_image_raw_nn_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_linear_constructed_image_raw_nn_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_linear_constructed_image_raw_nn_cell_dot_pointwise_left. ff_left_mcp_cell_ics_linear_constructed_image_raw_nn_cell = ff_q_fpmp_dot_mcp_ics_linear_constructed_image_raw_nn_cell_dot_pointwise_left * S ((S (fpmp_index_dot_mcp_ics_linear_constructed_image_raw_nn_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_linear_constructed_image_raw_nn_cell) + (fpmp_left_dot_mcp_ics_linear_constructed_image_raw_nn_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_linear_constructed_image_raw_nn_cell_dot_pointwise_right. ff_h_fpmp_dot_mcp_ics_linear_constructed_image_raw_nn_cell_dot_pointwise_right + S (fpmp_right_dot_mcp_ics_linear_constructed_image_raw_nn_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_linear_constructed_image_raw_nn_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_linear_constructed_image_raw_nn_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_linear_constructed_image_raw_nn_cell_dot_pointwise_right. ff_right_mcp_cell_ics_linear_constructed_image_raw_nn_cell = ff_q_fpmp_dot_mcp_ics_linear_constructed_image_raw_nn_cell_dot_pointwise_right * S ((S (fpmp_index_dot_mcp_ics_linear_constructed_image_raw_nn_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_linear_constructed_image_raw_nn_cell) + (fpmp_right_dot_mcp_ics_linear_constructed_image_raw_nn_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_linear_constructed_image_raw_nn_cell_dot_pointwise_target. ff_h_fpmp_dot_mcp_ics_linear_constructed_image_raw_nn_cell_dot_pointwise_target + S (fpmp_target_dot_mcp_ics_linear_constructed_image_raw_nn_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_linear_constructed_image_raw_nn_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_linear_constructed_image_raw_nn_cell_dot)) /\ exists ff_q_fpmp_dot_mcp_ics_linear_constructed_image_raw_nn_cell_dot_pointwise_target. ff_code_dot_mcp_ics_linear_constructed_image_raw_nn_cell_dot = ff_q_fpmp_dot_mcp_ics_linear_constructed_image_raw_nn_cell_dot_pointwise_target * S ((S (fpmp_index_dot_mcp_ics_linear_constructed_image_raw_nn_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_linear_constructed_image_raw_nn_cell_dot) + (fpmp_target_dot_mcp_ics_linear_constructed_image_raw_nn_cell_dot_pointwise))) -> fpmp_target_dot_mcp_ics_linear_constructed_image_raw_nn_cell_dot_pointwise = fpmp_left_dot_mcp_ics_linear_constructed_image_raw_nn_cell_dot_pointwise * fpmp_right_dot_mcp_ics_linear_constructed_image_raw_nn_cell_dot_pointwise) /\ (exists ff_u_dot_mcp_ics_linear_constructed_image_raw_nn_cell_dot_sum ff_v_dot_mcp_ics_linear_constructed_image_raw_nn_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_linear_constructed_image_raw_nn_cell_dot_sum_start. ff_h_dot_mcp_ics_linear_constructed_image_raw_nn_cell_dot_sum_start + S (0) = S ((S (0)) * ff_v_dot_mcp_ics_linear_constructed_image_raw_nn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_linear_constructed_image_raw_nn_cell_dot_sum_start. ff_u_dot_mcp_ics_linear_constructed_image_raw_nn_cell_dot_sum = ff_q_dot_mcp_ics_linear_constructed_image_raw_nn_cell_dot_sum_start * S ((S (0)) * ff_v_dot_mcp_ics_linear_constructed_image_raw_nn_cell_dot_sum) + (0))) /\ ((((exists ff_h_dot_mcp_ics_linear_constructed_image_raw_nn_cell_dot_sum_terminal. ff_h_dot_mcp_ics_linear_constructed_image_raw_nn_cell_dot_sum_terminal + S (ff_value_mcp_prefix_ics_linear_constructed_image_raw_nn) = S ((S (w)) * ff_v_dot_mcp_ics_linear_constructed_image_raw_nn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_linear_constructed_image_raw_nn_cell_dot_sum_terminal. ff_u_dot_mcp_ics_linear_constructed_image_raw_nn_cell_dot_sum = ff_q_dot_mcp_ics_linear_constructed_image_raw_nn_cell_dot_sum_terminal * S ((S (w)) * ff_v_dot_mcp_ics_linear_constructed_image_raw_nn_cell_dot_sum) + (ff_value_mcp_prefix_ics_linear_constructed_image_raw_nn))) /\ forall ff_i_dot_mcp_ics_linear_constructed_image_raw_nn_cell_dot_sum. (exists ff_lt_dot_mcp_ics_linear_constructed_image_raw_nn_cell_dot_sum_bound. ff_lt_dot_mcp_ics_linear_constructed_image_raw_nn_cell_dot_sum_bound + S ff_i_dot_mcp_ics_linear_constructed_image_raw_nn_cell_dot_sum = w) -> exists ff_a_dot_mcp_ics_linear_constructed_image_raw_nn_cell_dot_sum ff_r_dot_mcp_ics_linear_constructed_image_raw_nn_cell_dot_sum ff_s_dot_mcp_ics_linear_constructed_image_raw_nn_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_linear_constructed_image_raw_nn_cell_dot_sum_summand. ff_h_dot_mcp_ics_linear_constructed_image_raw_nn_cell_dot_sum_summand + S (ff_a_dot_mcp_ics_linear_constructed_image_raw_nn_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_linear_constructed_image_raw_nn_cell_dot_sum)) * ff_scale_dot_mcp_ics_linear_constructed_image_raw_nn_cell_dot)) /\ exists ff_q_dot_mcp_ics_linear_constructed_image_raw_nn_cell_dot_sum_summand. ff_code_dot_mcp_ics_linear_constructed_image_raw_nn_cell_dot = ff_q_dot_mcp_ics_linear_constructed_image_raw_nn_cell_dot_sum_summand * S ((S (ff_i_dot_mcp_ics_linear_constructed_image_raw_nn_cell_dot_sum)) * ff_scale_dot_mcp_ics_linear_constructed_image_raw_nn_cell_dot) + (ff_a_dot_mcp_ics_linear_constructed_image_raw_nn_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_linear_constructed_image_raw_nn_cell_dot_sum_partial. ff_h_dot_mcp_ics_linear_constructed_image_raw_nn_cell_dot_sum_partial + S (ff_r_dot_mcp_ics_linear_constructed_image_raw_nn_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_linear_constructed_image_raw_nn_cell_dot_sum)) * ff_v_dot_mcp_ics_linear_constructed_image_raw_nn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_linear_constructed_image_raw_nn_cell_dot_sum_partial. ff_u_dot_mcp_ics_linear_constructed_image_raw_nn_cell_dot_sum = ff_q_dot_mcp_ics_linear_constructed_image_raw_nn_cell_dot_sum_partial * S ((S (ff_i_dot_mcp_ics_linear_constructed_image_raw_nn_cell_dot_sum)) * ff_v_dot_mcp_ics_linear_constructed_image_raw_nn_cell_dot_sum) + (ff_r_dot_mcp_ics_linear_constructed_image_raw_nn_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_linear_constructed_image_raw_nn_cell_dot_sum_successor. ff_h_dot_mcp_ics_linear_constructed_image_raw_nn_cell_dot_sum_successor + S (ff_s_dot_mcp_ics_linear_constructed_image_raw_nn_cell_dot_sum) = S ((S (S ff_i_dot_mcp_ics_linear_constructed_image_raw_nn_cell_dot_sum)) * ff_v_dot_mcp_ics_linear_constructed_image_raw_nn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_linear_constructed_image_raw_nn_cell_dot_sum_successor. ff_u_dot_mcp_ics_linear_constructed_image_raw_nn_cell_dot_sum = ff_q_dot_mcp_ics_linear_constructed_image_raw_nn_cell_dot_sum_successor * S ((S (S ff_i_dot_mcp_ics_linear_constructed_image_raw_nn_cell_dot_sum)) * ff_v_dot_mcp_ics_linear_constructed_image_raw_nn_cell_dot_sum) + (ff_s_dot_mcp_ics_linear_constructed_image_raw_nn_cell_dot_sum))) /\ ff_s_dot_mcp_ics_linear_constructed_image_raw_nn_cell_dot_sum = ff_r_dot_mcp_ics_linear_constructed_image_raw_nn_cell_dot_sum + ff_a_dot_mcp_ics_linear_constructed_image_raw_nn_cell_dot_sum))))))))))) /\ (((exists fs_h_mcp_ics_linear_constructed_image_raw_nn_entry. fs_h_mcp_ics_linear_constructed_image_raw_nn_entry + S (ff_value_mcp_prefix_ics_linear_constructed_image_raw_nn) = S ((S (ff_index_mcp_prefix_ics_linear_constructed_image_raw_nn)) * ff_nns_mcp_smatrix_ics_linear_constructed_image_raw)) /\ exists fs_q_mcp_ics_linear_constructed_image_raw_nn_entry. ff_nn_mcp_smatrix_ics_linear_constructed_image_raw = fs_q_mcp_ics_linear_constructed_image_raw_nn_entry * S ((S (ff_index_mcp_prefix_ics_linear_constructed_image_raw_nn)) * ff_nns_mcp_smatrix_ics_linear_constructed_image_raw) + (ff_value_mcp_prefix_ics_linear_constructed_image_raw_nn))))))) /\ ((forall ff_index_mcp_prefix_ics_linear_constructed_image_raw_pn. (exists mcp_gap_ics_linear_constructed_image_raw_pn_index. mcp_gap_ics_linear_constructed_image_raw_pn_index + S (ff_index_mcp_prefix_ics_linear_constructed_image_raw_pn) = ((r) * (1))) -> exists ff_row_mcp_prefix_ics_linear_constructed_image_raw_pn ff_column_mcp_prefix_ics_linear_constructed_image_raw_pn ff_value_mcp_prefix_ics_linear_constructed_image_raw_pn. ((ff_index_mcp_prefix_ics_linear_constructed_image_raw_pn) = (1) * ff_row_mcp_prefix_ics_linear_constructed_image_raw_pn + ff_column_mcp_prefix_ics_linear_constructed_image_raw_pn /\ ((exists mcp_gap_ics_linear_constructed_image_raw_pn_column. mcp_gap_ics_linear_constructed_image_raw_pn_column + S (ff_column_mcp_prefix_ics_linear_constructed_image_raw_pn) = (1)) /\ ((exists ff_left_mcp_cell_ics_linear_constructed_image_raw_pn_cell ff_left_scale_mcp_cell_ics_linear_constructed_image_raw_pn_cell ff_right_mcp_cell_ics_linear_constructed_image_raw_pn_cell ff_right_scale_mcp_cell_ics_linear_constructed_image_raw_pn_cell. ((forall ff_index_mcp_ics_linear_constructed_image_raw_pn_cell_row ff_source_mcp_ics_linear_constructed_image_raw_pn_cell_row ff_target_mcp_ics_linear_constructed_image_raw_pn_cell_row. (exists mcp_gap_ics_linear_constructed_image_raw_pn_cell_row_bound. mcp_gap_ics_linear_constructed_image_raw_pn_cell_row_bound + S (ff_index_mcp_ics_linear_constructed_image_raw_pn_cell_row) = (w)) -> (((exists fs_h_mcp_ics_linear_constructed_image_raw_pn_cell_row_source. fs_h_mcp_ics_linear_constructed_image_raw_pn_cell_row_source + S (ff_source_mcp_ics_linear_constructed_image_raw_pn_cell_row) = S ((S (((ff_row_mcp_prefix_ics_linear_constructed_image_raw_pn) * (w)) + (1) * ff_index_mcp_ics_linear_constructed_image_raw_pn_cell_row)) * ac)) /\ exists fs_q_mcp_ics_linear_constructed_image_raw_pn_cell_row_source. ab = fs_q_mcp_ics_linear_constructed_image_raw_pn_cell_row_source * S ((S (((ff_row_mcp_prefix_ics_linear_constructed_image_raw_pn) * (w)) + (1) * ff_index_mcp_ics_linear_constructed_image_raw_pn_cell_row)) * ac) + (ff_source_mcp_ics_linear_constructed_image_raw_pn_cell_row))) -> (((exists fs_h_mcp_ics_linear_constructed_image_raw_pn_cell_row_target. fs_h_mcp_ics_linear_constructed_image_raw_pn_cell_row_target + S (ff_target_mcp_ics_linear_constructed_image_raw_pn_cell_row) = S ((S (ff_index_mcp_ics_linear_constructed_image_raw_pn_cell_row)) * ff_left_scale_mcp_cell_ics_linear_constructed_image_raw_pn_cell)) /\ exists fs_q_mcp_ics_linear_constructed_image_raw_pn_cell_row_target. ff_left_mcp_cell_ics_linear_constructed_image_raw_pn_cell = fs_q_mcp_ics_linear_constructed_image_raw_pn_cell_row_target * S ((S (ff_index_mcp_ics_linear_constructed_image_raw_pn_cell_row)) * ff_left_scale_mcp_cell_ics_linear_constructed_image_raw_pn_cell) + (ff_target_mcp_ics_linear_constructed_image_raw_pn_cell_row))) -> ff_target_mcp_ics_linear_constructed_image_raw_pn_cell_row = ff_source_mcp_ics_linear_constructed_image_raw_pn_cell_row) /\ ((forall ff_index_mcp_ics_linear_constructed_image_raw_pn_cell_column ff_source_mcp_ics_linear_constructed_image_raw_pn_cell_column ff_target_mcp_ics_linear_constructed_image_raw_pn_cell_column. (exists mcp_gap_ics_linear_constructed_image_raw_pn_cell_column_bound. mcp_gap_ics_linear_constructed_image_raw_pn_cell_column_bound + S (ff_index_mcp_ics_linear_constructed_image_raw_pn_cell_column) = (w)) -> (((exists fs_h_mcp_ics_linear_constructed_image_raw_pn_cell_column_source. fs_h_mcp_ics_linear_constructed_image_raw_pn_cell_column_source + S (ff_source_mcp_ics_linear_constructed_image_raw_pn_cell_column) = S ((S ((ff_column_mcp_prefix_ics_linear_constructed_image_raw_pn) + (1) * ff_index_mcp_ics_linear_constructed_image_raw_pn_cell_column)) * jc)) /\ exists fs_q_mcp_ics_linear_constructed_image_raw_pn_cell_column_source. jb = fs_q_mcp_ics_linear_constructed_image_raw_pn_cell_column_source * S ((S ((ff_column_mcp_prefix_ics_linear_constructed_image_raw_pn) + (1) * ff_index_mcp_ics_linear_constructed_image_raw_pn_cell_column)) * jc) + (ff_source_mcp_ics_linear_constructed_image_raw_pn_cell_column))) -> (((exists fs_h_mcp_ics_linear_constructed_image_raw_pn_cell_column_target. fs_h_mcp_ics_linear_constructed_image_raw_pn_cell_column_target + S (ff_target_mcp_ics_linear_constructed_image_raw_pn_cell_column) = S ((S (ff_index_mcp_ics_linear_constructed_image_raw_pn_cell_column)) * ff_right_scale_mcp_cell_ics_linear_constructed_image_raw_pn_cell)) /\ exists fs_q_mcp_ics_linear_constructed_image_raw_pn_cell_column_target. ff_right_mcp_cell_ics_linear_constructed_image_raw_pn_cell = fs_q_mcp_ics_linear_constructed_image_raw_pn_cell_column_target * S ((S (ff_index_mcp_ics_linear_constructed_image_raw_pn_cell_column)) * ff_right_scale_mcp_cell_ics_linear_constructed_image_raw_pn_cell) + (ff_target_mcp_ics_linear_constructed_image_raw_pn_cell_column))) -> ff_target_mcp_ics_linear_constructed_image_raw_pn_cell_column = ff_source_mcp_ics_linear_constructed_image_raw_pn_cell_column) /\ (exists ff_code_dot_mcp_ics_linear_constructed_image_raw_pn_cell_dot ff_scale_dot_mcp_ics_linear_constructed_image_raw_pn_cell_dot. ((forall fpmp_index_dot_mcp_ics_linear_constructed_image_raw_pn_cell_dot_pointwise fpmp_left_dot_mcp_ics_linear_constructed_image_raw_pn_cell_dot_pointwise fpmp_right_dot_mcp_ics_linear_constructed_image_raw_pn_cell_dot_pointwise fpmp_target_dot_mcp_ics_linear_constructed_image_raw_pn_cell_dot_pointwise. (exists fpmp_gap_dot_mcp_ics_linear_constructed_image_raw_pn_cell_dot_pointwise. fpmp_gap_dot_mcp_ics_linear_constructed_image_raw_pn_cell_dot_pointwise + S fpmp_index_dot_mcp_ics_linear_constructed_image_raw_pn_cell_dot_pointwise = w) -> (((exists ff_h_fpmp_dot_mcp_ics_linear_constructed_image_raw_pn_cell_dot_pointwise_left. ff_h_fpmp_dot_mcp_ics_linear_constructed_image_raw_pn_cell_dot_pointwise_left + S (fpmp_left_dot_mcp_ics_linear_constructed_image_raw_pn_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_linear_constructed_image_raw_pn_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_linear_constructed_image_raw_pn_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_linear_constructed_image_raw_pn_cell_dot_pointwise_left. ff_left_mcp_cell_ics_linear_constructed_image_raw_pn_cell = ff_q_fpmp_dot_mcp_ics_linear_constructed_image_raw_pn_cell_dot_pointwise_left * S ((S (fpmp_index_dot_mcp_ics_linear_constructed_image_raw_pn_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_linear_constructed_image_raw_pn_cell) + (fpmp_left_dot_mcp_ics_linear_constructed_image_raw_pn_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_linear_constructed_image_raw_pn_cell_dot_pointwise_right. ff_h_fpmp_dot_mcp_ics_linear_constructed_image_raw_pn_cell_dot_pointwise_right + S (fpmp_right_dot_mcp_ics_linear_constructed_image_raw_pn_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_linear_constructed_image_raw_pn_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_linear_constructed_image_raw_pn_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_linear_constructed_image_raw_pn_cell_dot_pointwise_right. ff_right_mcp_cell_ics_linear_constructed_image_raw_pn_cell = ff_q_fpmp_dot_mcp_ics_linear_constructed_image_raw_pn_cell_dot_pointwise_right * S ((S (fpmp_index_dot_mcp_ics_linear_constructed_image_raw_pn_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_linear_constructed_image_raw_pn_cell) + (fpmp_right_dot_mcp_ics_linear_constructed_image_raw_pn_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_linear_constructed_image_raw_pn_cell_dot_pointwise_target. ff_h_fpmp_dot_mcp_ics_linear_constructed_image_raw_pn_cell_dot_pointwise_target + S (fpmp_target_dot_mcp_ics_linear_constructed_image_raw_pn_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_linear_constructed_image_raw_pn_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_linear_constructed_image_raw_pn_cell_dot)) /\ exists ff_q_fpmp_dot_mcp_ics_linear_constructed_image_raw_pn_cell_dot_pointwise_target. ff_code_dot_mcp_ics_linear_constructed_image_raw_pn_cell_dot = ff_q_fpmp_dot_mcp_ics_linear_constructed_image_raw_pn_cell_dot_pointwise_target * S ((S (fpmp_index_dot_mcp_ics_linear_constructed_image_raw_pn_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_linear_constructed_image_raw_pn_cell_dot) + (fpmp_target_dot_mcp_ics_linear_constructed_image_raw_pn_cell_dot_pointwise))) -> fpmp_target_dot_mcp_ics_linear_constructed_image_raw_pn_cell_dot_pointwise = fpmp_left_dot_mcp_ics_linear_constructed_image_raw_pn_cell_dot_pointwise * fpmp_right_dot_mcp_ics_linear_constructed_image_raw_pn_cell_dot_pointwise) /\ (exists ff_u_dot_mcp_ics_linear_constructed_image_raw_pn_cell_dot_sum ff_v_dot_mcp_ics_linear_constructed_image_raw_pn_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_linear_constructed_image_raw_pn_cell_dot_sum_start. ff_h_dot_mcp_ics_linear_constructed_image_raw_pn_cell_dot_sum_start + S (0) = S ((S (0)) * ff_v_dot_mcp_ics_linear_constructed_image_raw_pn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_linear_constructed_image_raw_pn_cell_dot_sum_start. ff_u_dot_mcp_ics_linear_constructed_image_raw_pn_cell_dot_sum = ff_q_dot_mcp_ics_linear_constructed_image_raw_pn_cell_dot_sum_start * S ((S (0)) * ff_v_dot_mcp_ics_linear_constructed_image_raw_pn_cell_dot_sum) + (0))) /\ ((((exists ff_h_dot_mcp_ics_linear_constructed_image_raw_pn_cell_dot_sum_terminal. ff_h_dot_mcp_ics_linear_constructed_image_raw_pn_cell_dot_sum_terminal + S (ff_value_mcp_prefix_ics_linear_constructed_image_raw_pn) = S ((S (w)) * ff_v_dot_mcp_ics_linear_constructed_image_raw_pn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_linear_constructed_image_raw_pn_cell_dot_sum_terminal. ff_u_dot_mcp_ics_linear_constructed_image_raw_pn_cell_dot_sum = ff_q_dot_mcp_ics_linear_constructed_image_raw_pn_cell_dot_sum_terminal * S ((S (w)) * ff_v_dot_mcp_ics_linear_constructed_image_raw_pn_cell_dot_sum) + (ff_value_mcp_prefix_ics_linear_constructed_image_raw_pn))) /\ forall ff_i_dot_mcp_ics_linear_constructed_image_raw_pn_cell_dot_sum. (exists ff_lt_dot_mcp_ics_linear_constructed_image_raw_pn_cell_dot_sum_bound. ff_lt_dot_mcp_ics_linear_constructed_image_raw_pn_cell_dot_sum_bound + S ff_i_dot_mcp_ics_linear_constructed_image_raw_pn_cell_dot_sum = w) -> exists ff_a_dot_mcp_ics_linear_constructed_image_raw_pn_cell_dot_sum ff_r_dot_mcp_ics_linear_constructed_image_raw_pn_cell_dot_sum ff_s_dot_mcp_ics_linear_constructed_image_raw_pn_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_linear_constructed_image_raw_pn_cell_dot_sum_summand. ff_h_dot_mcp_ics_linear_constructed_image_raw_pn_cell_dot_sum_summand + S (ff_a_dot_mcp_ics_linear_constructed_image_raw_pn_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_linear_constructed_image_raw_pn_cell_dot_sum)) * ff_scale_dot_mcp_ics_linear_constructed_image_raw_pn_cell_dot)) /\ exists ff_q_dot_mcp_ics_linear_constructed_image_raw_pn_cell_dot_sum_summand. ff_code_dot_mcp_ics_linear_constructed_image_raw_pn_cell_dot = ff_q_dot_mcp_ics_linear_constructed_image_raw_pn_cell_dot_sum_summand * S ((S (ff_i_dot_mcp_ics_linear_constructed_image_raw_pn_cell_dot_sum)) * ff_scale_dot_mcp_ics_linear_constructed_image_raw_pn_cell_dot) + (ff_a_dot_mcp_ics_linear_constructed_image_raw_pn_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_linear_constructed_image_raw_pn_cell_dot_sum_partial. ff_h_dot_mcp_ics_linear_constructed_image_raw_pn_cell_dot_sum_partial + S (ff_r_dot_mcp_ics_linear_constructed_image_raw_pn_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_linear_constructed_image_raw_pn_cell_dot_sum)) * ff_v_dot_mcp_ics_linear_constructed_image_raw_pn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_linear_constructed_image_raw_pn_cell_dot_sum_partial. ff_u_dot_mcp_ics_linear_constructed_image_raw_pn_cell_dot_sum = ff_q_dot_mcp_ics_linear_constructed_image_raw_pn_cell_dot_sum_partial * S ((S (ff_i_dot_mcp_ics_linear_constructed_image_raw_pn_cell_dot_sum)) * ff_v_dot_mcp_ics_linear_constructed_image_raw_pn_cell_dot_sum) + (ff_r_dot_mcp_ics_linear_constructed_image_raw_pn_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_linear_constructed_image_raw_pn_cell_dot_sum_successor. ff_h_dot_mcp_ics_linear_constructed_image_raw_pn_cell_dot_sum_successor + S (ff_s_dot_mcp_ics_linear_constructed_image_raw_pn_cell_dot_sum) = S ((S (S ff_i_dot_mcp_ics_linear_constructed_image_raw_pn_cell_dot_sum)) * ff_v_dot_mcp_ics_linear_constructed_image_raw_pn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_linear_constructed_image_raw_pn_cell_dot_sum_successor. ff_u_dot_mcp_ics_linear_constructed_image_raw_pn_cell_dot_sum = ff_q_dot_mcp_ics_linear_constructed_image_raw_pn_cell_dot_sum_successor * S ((S (S ff_i_dot_mcp_ics_linear_constructed_image_raw_pn_cell_dot_sum)) * ff_v_dot_mcp_ics_linear_constructed_image_raw_pn_cell_dot_sum) + (ff_s_dot_mcp_ics_linear_constructed_image_raw_pn_cell_dot_sum))) /\ ff_s_dot_mcp_ics_linear_constructed_image_raw_pn_cell_dot_sum = ff_r_dot_mcp_ics_linear_constructed_image_raw_pn_cell_dot_sum + ff_a_dot_mcp_ics_linear_constructed_image_raw_pn_cell_dot_sum))))))))))) /\ (((exists fs_h_mcp_ics_linear_constructed_image_raw_pn_entry. fs_h_mcp_ics_linear_constructed_image_raw_pn_entry + S (ff_value_mcp_prefix_ics_linear_constructed_image_raw_pn) = S ((S (ff_index_mcp_prefix_ics_linear_constructed_image_raw_pn)) * ff_pns_mcp_smatrix_ics_linear_constructed_image_raw)) /\ exists fs_q_mcp_ics_linear_constructed_image_raw_pn_entry. ff_pn_mcp_smatrix_ics_linear_constructed_image_raw = fs_q_mcp_ics_linear_constructed_image_raw_pn_entry * S ((S (ff_index_mcp_prefix_ics_linear_constructed_image_raw_pn)) * ff_pns_mcp_smatrix_ics_linear_constructed_image_raw) + (ff_value_mcp_prefix_ics_linear_constructed_image_raw_pn))))))) /\ ((forall ff_index_mcp_prefix_ics_linear_constructed_image_raw_np. (exists mcp_gap_ics_linear_constructed_image_raw_np_index. mcp_gap_ics_linear_constructed_image_raw_np_index + S (ff_index_mcp_prefix_ics_linear_constructed_image_raw_np) = ((r) * (1))) -> exists ff_row_mcp_prefix_ics_linear_constructed_image_raw_np ff_column_mcp_prefix_ics_linear_constructed_image_raw_np ff_value_mcp_prefix_ics_linear_constructed_image_raw_np. ((ff_index_mcp_prefix_ics_linear_constructed_image_raw_np) = (1) * ff_row_mcp_prefix_ics_linear_constructed_image_raw_np + ff_column_mcp_prefix_ics_linear_constructed_image_raw_np /\ ((exists mcp_gap_ics_linear_constructed_image_raw_np_column. mcp_gap_ics_linear_constructed_image_raw_np_column + S (ff_column_mcp_prefix_ics_linear_constructed_image_raw_np) = (1)) /\ ((exists ff_left_mcp_cell_ics_linear_constructed_image_raw_np_cell ff_left_scale_mcp_cell_ics_linear_constructed_image_raw_np_cell ff_right_mcp_cell_ics_linear_constructed_image_raw_np_cell ff_right_scale_mcp_cell_ics_linear_constructed_image_raw_np_cell. ((forall ff_index_mcp_ics_linear_constructed_image_raw_np_cell_row ff_source_mcp_ics_linear_constructed_image_raw_np_cell_row ff_target_mcp_ics_linear_constructed_image_raw_np_cell_row. (exists mcp_gap_ics_linear_constructed_image_raw_np_cell_row_bound. mcp_gap_ics_linear_constructed_image_raw_np_cell_row_bound + S (ff_index_mcp_ics_linear_constructed_image_raw_np_cell_row) = (w)) -> (((exists fs_h_mcp_ics_linear_constructed_image_raw_np_cell_row_source. fs_h_mcp_ics_linear_constructed_image_raw_np_cell_row_source + S (ff_source_mcp_ics_linear_constructed_image_raw_np_cell_row) = S ((S (((ff_row_mcp_prefix_ics_linear_constructed_image_raw_np) * (w)) + (1) * ff_index_mcp_ics_linear_constructed_image_raw_np_cell_row)) * dc)) /\ exists fs_q_mcp_ics_linear_constructed_image_raw_np_cell_row_source. db = fs_q_mcp_ics_linear_constructed_image_raw_np_cell_row_source * S ((S (((ff_row_mcp_prefix_ics_linear_constructed_image_raw_np) * (w)) + (1) * ff_index_mcp_ics_linear_constructed_image_raw_np_cell_row)) * dc) + (ff_source_mcp_ics_linear_constructed_image_raw_np_cell_row))) -> (((exists fs_h_mcp_ics_linear_constructed_image_raw_np_cell_row_target. fs_h_mcp_ics_linear_constructed_image_raw_np_cell_row_target + S (ff_target_mcp_ics_linear_constructed_image_raw_np_cell_row) = S ((S (ff_index_mcp_ics_linear_constructed_image_raw_np_cell_row)) * ff_left_scale_mcp_cell_ics_linear_constructed_image_raw_np_cell)) /\ exists fs_q_mcp_ics_linear_constructed_image_raw_np_cell_row_target. ff_left_mcp_cell_ics_linear_constructed_image_raw_np_cell = fs_q_mcp_ics_linear_constructed_image_raw_np_cell_row_target * S ((S (ff_index_mcp_ics_linear_constructed_image_raw_np_cell_row)) * ff_left_scale_mcp_cell_ics_linear_constructed_image_raw_np_cell) + (ff_target_mcp_ics_linear_constructed_image_raw_np_cell_row))) -> ff_target_mcp_ics_linear_constructed_image_raw_np_cell_row = ff_source_mcp_ics_linear_constructed_image_raw_np_cell_row) /\ ((forall ff_index_mcp_ics_linear_constructed_image_raw_np_cell_column ff_source_mcp_ics_linear_constructed_image_raw_np_cell_column ff_target_mcp_ics_linear_constructed_image_raw_np_cell_column. (exists mcp_gap_ics_linear_constructed_image_raw_np_cell_column_bound. mcp_gap_ics_linear_constructed_image_raw_np_cell_column_bound + S (ff_index_mcp_ics_linear_constructed_image_raw_np_cell_column) = (w)) -> (((exists fs_h_mcp_ics_linear_constructed_image_raw_np_cell_column_source. fs_h_mcp_ics_linear_constructed_image_raw_np_cell_column_source + S (ff_source_mcp_ics_linear_constructed_image_raw_np_cell_column) = S ((S ((ff_column_mcp_prefix_ics_linear_constructed_image_raw_np) + (1) * ff_index_mcp_ics_linear_constructed_image_raw_np_cell_column)) * ic)) /\ exists fs_q_mcp_ics_linear_constructed_image_raw_np_cell_column_source. ib = fs_q_mcp_ics_linear_constructed_image_raw_np_cell_column_source * S ((S ((ff_column_mcp_prefix_ics_linear_constructed_image_raw_np) + (1) * ff_index_mcp_ics_linear_constructed_image_raw_np_cell_column)) * ic) + (ff_source_mcp_ics_linear_constructed_image_raw_np_cell_column))) -> (((exists fs_h_mcp_ics_linear_constructed_image_raw_np_cell_column_target. fs_h_mcp_ics_linear_constructed_image_raw_np_cell_column_target + S (ff_target_mcp_ics_linear_constructed_image_raw_np_cell_column) = S ((S (ff_index_mcp_ics_linear_constructed_image_raw_np_cell_column)) * ff_right_scale_mcp_cell_ics_linear_constructed_image_raw_np_cell)) /\ exists fs_q_mcp_ics_linear_constructed_image_raw_np_cell_column_target. ff_right_mcp_cell_ics_linear_constructed_image_raw_np_cell = fs_q_mcp_ics_linear_constructed_image_raw_np_cell_column_target * S ((S (ff_index_mcp_ics_linear_constructed_image_raw_np_cell_column)) * ff_right_scale_mcp_cell_ics_linear_constructed_image_raw_np_cell) + (ff_target_mcp_ics_linear_constructed_image_raw_np_cell_column))) -> ff_target_mcp_ics_linear_constructed_image_raw_np_cell_column = ff_source_mcp_ics_linear_constructed_image_raw_np_cell_column) /\ (exists ff_code_dot_mcp_ics_linear_constructed_image_raw_np_cell_dot ff_scale_dot_mcp_ics_linear_constructed_image_raw_np_cell_dot. ((forall fpmp_index_dot_mcp_ics_linear_constructed_image_raw_np_cell_dot_pointwise fpmp_left_dot_mcp_ics_linear_constructed_image_raw_np_cell_dot_pointwise fpmp_right_dot_mcp_ics_linear_constructed_image_raw_np_cell_dot_pointwise fpmp_target_dot_mcp_ics_linear_constructed_image_raw_np_cell_dot_pointwise. (exists fpmp_gap_dot_mcp_ics_linear_constructed_image_raw_np_cell_dot_pointwise. fpmp_gap_dot_mcp_ics_linear_constructed_image_raw_np_cell_dot_pointwise + S fpmp_index_dot_mcp_ics_linear_constructed_image_raw_np_cell_dot_pointwise = w) -> (((exists ff_h_fpmp_dot_mcp_ics_linear_constructed_image_raw_np_cell_dot_pointwise_left. ff_h_fpmp_dot_mcp_ics_linear_constructed_image_raw_np_cell_dot_pointwise_left + S (fpmp_left_dot_mcp_ics_linear_constructed_image_raw_np_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_linear_constructed_image_raw_np_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_linear_constructed_image_raw_np_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_linear_constructed_image_raw_np_cell_dot_pointwise_left. ff_left_mcp_cell_ics_linear_constructed_image_raw_np_cell = ff_q_fpmp_dot_mcp_ics_linear_constructed_image_raw_np_cell_dot_pointwise_left * S ((S (fpmp_index_dot_mcp_ics_linear_constructed_image_raw_np_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_linear_constructed_image_raw_np_cell) + (fpmp_left_dot_mcp_ics_linear_constructed_image_raw_np_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_linear_constructed_image_raw_np_cell_dot_pointwise_right. ff_h_fpmp_dot_mcp_ics_linear_constructed_image_raw_np_cell_dot_pointwise_right + S (fpmp_right_dot_mcp_ics_linear_constructed_image_raw_np_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_linear_constructed_image_raw_np_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_linear_constructed_image_raw_np_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_linear_constructed_image_raw_np_cell_dot_pointwise_right. ff_right_mcp_cell_ics_linear_constructed_image_raw_np_cell = ff_q_fpmp_dot_mcp_ics_linear_constructed_image_raw_np_cell_dot_pointwise_right * S ((S (fpmp_index_dot_mcp_ics_linear_constructed_image_raw_np_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_linear_constructed_image_raw_np_cell) + (fpmp_right_dot_mcp_ics_linear_constructed_image_raw_np_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_linear_constructed_image_raw_np_cell_dot_pointwise_target. ff_h_fpmp_dot_mcp_ics_linear_constructed_image_raw_np_cell_dot_pointwise_target + S (fpmp_target_dot_mcp_ics_linear_constructed_image_raw_np_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_linear_constructed_image_raw_np_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_linear_constructed_image_raw_np_cell_dot)) /\ exists ff_q_fpmp_dot_mcp_ics_linear_constructed_image_raw_np_cell_dot_pointwise_target. ff_code_dot_mcp_ics_linear_constructed_image_raw_np_cell_dot = ff_q_fpmp_dot_mcp_ics_linear_constructed_image_raw_np_cell_dot_pointwise_target * S ((S (fpmp_index_dot_mcp_ics_linear_constructed_image_raw_np_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_linear_constructed_image_raw_np_cell_dot) + (fpmp_target_dot_mcp_ics_linear_constructed_image_raw_np_cell_dot_pointwise))) -> fpmp_target_dot_mcp_ics_linear_constructed_image_raw_np_cell_dot_pointwise = fpmp_left_dot_mcp_ics_linear_constructed_image_raw_np_cell_dot_pointwise * fpmp_right_dot_mcp_ics_linear_constructed_image_raw_np_cell_dot_pointwise) /\ (exists ff_u_dot_mcp_ics_linear_constructed_image_raw_np_cell_dot_sum ff_v_dot_mcp_ics_linear_constructed_image_raw_np_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_linear_constructed_image_raw_np_cell_dot_sum_start. ff_h_dot_mcp_ics_linear_constructed_image_raw_np_cell_dot_sum_start + S (0) = S ((S (0)) * ff_v_dot_mcp_ics_linear_constructed_image_raw_np_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_linear_constructed_image_raw_np_cell_dot_sum_start. ff_u_dot_mcp_ics_linear_constructed_image_raw_np_cell_dot_sum = ff_q_dot_mcp_ics_linear_constructed_image_raw_np_cell_dot_sum_start * S ((S (0)) * ff_v_dot_mcp_ics_linear_constructed_image_raw_np_cell_dot_sum) + (0))) /\ ((((exists ff_h_dot_mcp_ics_linear_constructed_image_raw_np_cell_dot_sum_terminal. ff_h_dot_mcp_ics_linear_constructed_image_raw_np_cell_dot_sum_terminal + S (ff_value_mcp_prefix_ics_linear_constructed_image_raw_np) = S ((S (w)) * ff_v_dot_mcp_ics_linear_constructed_image_raw_np_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_linear_constructed_image_raw_np_cell_dot_sum_terminal. ff_u_dot_mcp_ics_linear_constructed_image_raw_np_cell_dot_sum = ff_q_dot_mcp_ics_linear_constructed_image_raw_np_cell_dot_sum_terminal * S ((S (w)) * ff_v_dot_mcp_ics_linear_constructed_image_raw_np_cell_dot_sum) + (ff_value_mcp_prefix_ics_linear_constructed_image_raw_np))) /\ forall ff_i_dot_mcp_ics_linear_constructed_image_raw_np_cell_dot_sum. (exists ff_lt_dot_mcp_ics_linear_constructed_image_raw_np_cell_dot_sum_bound. ff_lt_dot_mcp_ics_linear_constructed_image_raw_np_cell_dot_sum_bound + S ff_i_dot_mcp_ics_linear_constructed_image_raw_np_cell_dot_sum = w) -> exists ff_a_dot_mcp_ics_linear_constructed_image_raw_np_cell_dot_sum ff_r_dot_mcp_ics_linear_constructed_image_raw_np_cell_dot_sum ff_s_dot_mcp_ics_linear_constructed_image_raw_np_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_linear_constructed_image_raw_np_cell_dot_sum_summand. ff_h_dot_mcp_ics_linear_constructed_image_raw_np_cell_dot_sum_summand + S (ff_a_dot_mcp_ics_linear_constructed_image_raw_np_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_linear_constructed_image_raw_np_cell_dot_sum)) * ff_scale_dot_mcp_ics_linear_constructed_image_raw_np_cell_dot)) /\ exists ff_q_dot_mcp_ics_linear_constructed_image_raw_np_cell_dot_sum_summand. ff_code_dot_mcp_ics_linear_constructed_image_raw_np_cell_dot = ff_q_dot_mcp_ics_linear_constructed_image_raw_np_cell_dot_sum_summand * S ((S (ff_i_dot_mcp_ics_linear_constructed_image_raw_np_cell_dot_sum)) * ff_scale_dot_mcp_ics_linear_constructed_image_raw_np_cell_dot) + (ff_a_dot_mcp_ics_linear_constructed_image_raw_np_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_linear_constructed_image_raw_np_cell_dot_sum_partial. ff_h_dot_mcp_ics_linear_constructed_image_raw_np_cell_dot_sum_partial + S (ff_r_dot_mcp_ics_linear_constructed_image_raw_np_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_linear_constructed_image_raw_np_cell_dot_sum)) * ff_v_dot_mcp_ics_linear_constructed_image_raw_np_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_linear_constructed_image_raw_np_cell_dot_sum_partial. ff_u_dot_mcp_ics_linear_constructed_image_raw_np_cell_dot_sum = ff_q_dot_mcp_ics_linear_constructed_image_raw_np_cell_dot_sum_partial * S ((S (ff_i_dot_mcp_ics_linear_constructed_image_raw_np_cell_dot_sum)) * ff_v_dot_mcp_ics_linear_constructed_image_raw_np_cell_dot_sum) + (ff_r_dot_mcp_ics_linear_constructed_image_raw_np_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_linear_constructed_image_raw_np_cell_dot_sum_successor. ff_h_dot_mcp_ics_linear_constructed_image_raw_np_cell_dot_sum_successor + S (ff_s_dot_mcp_ics_linear_constructed_image_raw_np_cell_dot_sum) = S ((S (S ff_i_dot_mcp_ics_linear_constructed_image_raw_np_cell_dot_sum)) * ff_v_dot_mcp_ics_linear_constructed_image_raw_np_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_linear_constructed_image_raw_np_cell_dot_sum_successor. ff_u_dot_mcp_ics_linear_constructed_image_raw_np_cell_dot_sum = ff_q_dot_mcp_ics_linear_constructed_image_raw_np_cell_dot_sum_successor * S ((S (S ff_i_dot_mcp_ics_linear_constructed_image_raw_np_cell_dot_sum)) * ff_v_dot_mcp_ics_linear_constructed_image_raw_np_cell_dot_sum) + (ff_s_dot_mcp_ics_linear_constructed_image_raw_np_cell_dot_sum))) /\ ff_s_dot_mcp_ics_linear_constructed_image_raw_np_cell_dot_sum = ff_r_dot_mcp_ics_linear_constructed_image_raw_np_cell_dot_sum + ff_a_dot_mcp_ics_linear_constructed_image_raw_np_cell_dot_sum))))))))))) /\ (((exists fs_h_mcp_ics_linear_constructed_image_raw_np_entry. fs_h_mcp_ics_linear_constructed_image_raw_np_entry + S (ff_value_mcp_prefix_ics_linear_constructed_image_raw_np) = S ((S (ff_index_mcp_prefix_ics_linear_constructed_image_raw_np)) * ff_nps_mcp_smatrix_ics_linear_constructed_image_raw)) /\ exists fs_q_mcp_ics_linear_constructed_image_raw_np_entry. ff_np_mcp_smatrix_ics_linear_constructed_image_raw = fs_q_mcp_ics_linear_constructed_image_raw_np_entry * S ((S (ff_index_mcp_prefix_ics_linear_constructed_image_raw_np)) * ff_nps_mcp_smatrix_ics_linear_constructed_image_raw) + (ff_value_mcp_prefix_ics_linear_constructed_image_raw_np))))))) /\ ((forall ff_index_mcp_add_ics_linear_constructed_image_raw_positive ff_left_mcp_add_ics_linear_constructed_image_raw_positive ff_right_mcp_add_ics_linear_constructed_image_raw_positive ff_target_mcp_add_ics_linear_constructed_image_raw_positive. (exists mcp_gap_ics_linear_constructed_image_raw_positive_bound. mcp_gap_ics_linear_constructed_image_raw_positive_bound + S (ff_index_mcp_add_ics_linear_constructed_image_raw_positive) = ((r) * (1))) -> (((exists fs_h_mcp_ics_linear_constructed_image_raw_positive_left. fs_h_mcp_ics_linear_constructed_image_raw_positive_left + S (ff_left_mcp_add_ics_linear_constructed_image_raw_positive) = S ((S (ff_index_mcp_add_ics_linear_constructed_image_raw_positive)) * ff_pps_mcp_smatrix_ics_linear_constructed_image_raw)) /\ exists fs_q_mcp_ics_linear_constructed_image_raw_positive_left. ff_pp_mcp_smatrix_ics_linear_constructed_image_raw = fs_q_mcp_ics_linear_constructed_image_raw_positive_left * S ((S (ff_index_mcp_add_ics_linear_constructed_image_raw_positive)) * ff_pps_mcp_smatrix_ics_linear_constructed_image_raw) + (ff_left_mcp_add_ics_linear_constructed_image_raw_positive))) -> (((exists fs_h_mcp_ics_linear_constructed_image_raw_positive_right. fs_h_mcp_ics_linear_constructed_image_raw_positive_right + S (ff_right_mcp_add_ics_linear_constructed_image_raw_positive) = S ((S (ff_index_mcp_add_ics_linear_constructed_image_raw_positive)) * ff_nns_mcp_smatrix_ics_linear_constructed_image_raw)) /\ exists fs_q_mcp_ics_linear_constructed_image_raw_positive_right. ff_nn_mcp_smatrix_ics_linear_constructed_image_raw = fs_q_mcp_ics_linear_constructed_image_raw_positive_right * S ((S (ff_index_mcp_add_ics_linear_constructed_image_raw_positive)) * ff_nns_mcp_smatrix_ics_linear_constructed_image_raw) + (ff_right_mcp_add_ics_linear_constructed_image_raw_positive))) -> (((exists fs_h_mcp_ics_linear_constructed_image_raw_positive_target. fs_h_mcp_ics_linear_constructed_image_raw_positive_target + S (ff_target_mcp_add_ics_linear_constructed_image_raw_positive) = S ((S (ff_index_mcp_add_ics_linear_constructed_image_raw_positive)) * ics_raw_positive_scale_linear_constructed_image)) /\ exists fs_q_mcp_ics_linear_constructed_image_raw_positive_target. ics_raw_positive_linear_constructed_image = fs_q_mcp_ics_linear_constructed_image_raw_positive_target * S ((S (ff_index_mcp_add_ics_linear_constructed_image_raw_positive)) * ics_raw_positive_scale_linear_constructed_image) + (ff_target_mcp_add_ics_linear_constructed_image_raw_positive))) -> ff_target_mcp_add_ics_linear_constructed_image_raw_positive = ff_left_mcp_add_ics_linear_constructed_image_raw_positive + ff_right_mcp_add_ics_linear_constructed_image_raw_positive) /\ (forall ff_index_mcp_add_ics_linear_constructed_image_raw_negative ff_left_mcp_add_ics_linear_constructed_image_raw_negative ff_right_mcp_add_ics_linear_constructed_image_raw_negative ff_target_mcp_add_ics_linear_constructed_image_raw_negative. (exists mcp_gap_ics_linear_constructed_image_raw_negative_bound. mcp_gap_ics_linear_constructed_image_raw_negative_bound + S (ff_index_mcp_add_ics_linear_constructed_image_raw_negative) = ((r) * (1))) -> (((exists fs_h_mcp_ics_linear_constructed_image_raw_negative_left. fs_h_mcp_ics_linear_constructed_image_raw_negative_left + S (ff_left_mcp_add_ics_linear_constructed_image_raw_negative) = S ((S (ff_index_mcp_add_ics_linear_constructed_image_raw_negative)) * ff_pns_mcp_smatrix_ics_linear_constructed_image_raw)) /\ exists fs_q_mcp_ics_linear_constructed_image_raw_negative_left. ff_pn_mcp_smatrix_ics_linear_constructed_image_raw = fs_q_mcp_ics_linear_constructed_image_raw_negative_left * S ((S (ff_index_mcp_add_ics_linear_constructed_image_raw_negative)) * ff_pns_mcp_smatrix_ics_linear_constructed_image_raw) + (ff_left_mcp_add_ics_linear_constructed_image_raw_negative))) -> (((exists fs_h_mcp_ics_linear_constructed_image_raw_negative_right. fs_h_mcp_ics_linear_constructed_image_raw_negative_right + S (ff_right_mcp_add_ics_linear_constructed_image_raw_negative) = S ((S (ff_index_mcp_add_ics_linear_constructed_image_raw_negative)) * ff_nps_mcp_smatrix_ics_linear_constructed_image_raw)) /\ exists fs_q_mcp_ics_linear_constructed_image_raw_negative_right. ff_np_mcp_smatrix_ics_linear_constructed_image_raw = fs_q_mcp_ics_linear_constructed_image_raw_negative_right * S ((S (ff_index_mcp_add_ics_linear_constructed_image_raw_negative)) * ff_nps_mcp_smatrix_ics_linear_constructed_image_raw) + (ff_right_mcp_add_ics_linear_constructed_image_raw_negative))) -> (((exists fs_h_mcp_ics_linear_constructed_image_raw_negative_target. fs_h_mcp_ics_linear_constructed_image_raw_negative_target + S (ff_target_mcp_add_ics_linear_constructed_image_raw_negative) = S ((S (ff_index_mcp_add_ics_linear_constructed_image_raw_negative)) * ics_raw_negative_scale_linear_constructed_image)) /\ exists fs_q_mcp_ics_linear_constructed_image_raw_negative_target. ics_raw_negative_linear_constructed_image = fs_q_mcp_ics_linear_constructed_image_raw_negative_target * S ((S (ff_index_mcp_add_ics_linear_constructed_image_raw_negative)) * ics_raw_negative_scale_linear_constructed_image) + (ff_target_mcp_add_ics_linear_constructed_image_raw_negative))) -> ff_target_mcp_add_ics_linear_constructed_image_raw_negative = ff_left_mcp_add_ics_linear_constructed_image_raw_negative + ff_right_mcp_add_ics_linear_constructed_image_raw_negative))))))) /\ (forall ics_index_linear_constructed_image_equal ics_value0_linear_constructed_image_equal ics_value1_linear_constructed_image_equal ics_value2_linear_constructed_image_equal ics_value3_linear_constructed_image_equal. (exists ics_gap_linear_constructed_image_equal_bound. ics_gap_linear_constructed_image_equal_bound + S (ics_index_linear_constructed_image_equal) = (r)) -> (((exists fs_h_ics_linear_constructed_image_equal_at0. fs_h_ics_linear_constructed_image_equal_at0 + S (ics_value0_linear_constructed_image_equal) = S ((S (ics_index_linear_constructed_image_equal)) * ics_raw_positive_scale_linear_constructed_image)) /\ exists fs_q_ics_linear_constructed_image_equal_at0. ics_raw_positive_linear_constructed_image = fs_q_ics_linear_constructed_image_equal_at0 * S ((S (ics_index_linear_constructed_image_equal)) * ics_raw_positive_scale_linear_constructed_image) + (ics_value0_linear_constructed_image_equal))) -> (((exists fs_h_ics_linear_constructed_image_equal_at1. fs_h_ics_linear_constructed_image_equal_at1 + S (ics_value1_linear_constructed_image_equal) = S ((S (ics_index_linear_constructed_image_equal)) * ics_raw_negative_scale_linear_constructed_image)) /\ exists fs_q_ics_linear_constructed_image_equal_at1. ics_raw_negative_linear_constructed_image = fs_q_ics_linear_constructed_image_equal_at1 * S ((S (ics_index_linear_constructed_image_equal)) * ics_raw_negative_scale_linear_constructed_image) + (ics_value1_linear_constructed_image_equal))) -> (((exists fs_h_ics_linear_constructed_image_equal_at2. fs_h_ics_linear_constructed_image_equal_at2 + S (ics_value2_linear_constructed_image_equal) = S ((S (ics_index_linear_constructed_image_equal)) * rc)) /\ exists fs_q_ics_linear_constructed_image_equal_at2. rb = fs_q_ics_linear_constructed_image_equal_at2 * S ((S (ics_index_linear_constructed_image_equal)) * rc) + (ics_value2_linear_constructed_image_equal))) -> (((exists fs_h_ics_linear_constructed_image_equal_at3. fs_h_ics_linear_constructed_image_equal_at3 + S (ics_value3_linear_constructed_image_equal) = S ((S (ics_index_linear_constructed_image_equal)) * sc)) /\ exists fs_q_ics_linear_constructed_image_equal_at3. sb = fs_q_ics_linear_constructed_image_equal_at3 * S ((S (ics_index_linear_constructed_image_equal)) * sc) + (ics_value3_linear_constructed_image_equal))) -> ics_value0_linear_constructed_image_equal + ics_value3_linear_constructed_image_equal = ics_value2_linear_constructed_image_equal + ics_value1_linear_constructed_image_equal))))))))