Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.
This branch proves the finite determinant/rank/span substrate. It does not claim Smith or Hermite normal form, lattice index equals determinant, determinant multiplicativity, lattice reduction, or geometry-of-numbers theorems.
Exact theorem in conservative defined notation
∀ ab. ∀ ac. ∀ db. ∀ dc. ∀ eb. ∀ ec. ∀ fb. ∀ fc. ∀ w. ∀ r. ∀ pb. ∀ pc. ∀ nb. ∀ nc. IntegerMatrixVectorProduct(ab,ac,db,dc,eb,ec,fb,fc,w,r,pb,pc,nb,nc) → IntegerMatrixVectorProduct(ab,ac,db,dc,fb,fc,eb,ec,w,r,nb,nc,pb,pc)Every linked abbreviation expands hygienically to the identical original native formula.
Definition DAG
Actual proof prerequisites
Original expanded first-order statement
forall ab ac db dc eb ec fb fc w r pb pc nb nc. (exists ics_raw_positive_linear_neg_source ics_raw_positive_scale_linear_neg_source ics_raw_negative_linear_neg_source ics_raw_negative_scale_linear_neg_source. (((exists ff_pp_mcp_smatrix_ics_linear_neg_source_raw ff_pps_mcp_smatrix_ics_linear_neg_source_raw ff_nn_mcp_smatrix_ics_linear_neg_source_raw ff_nns_mcp_smatrix_ics_linear_neg_source_raw ff_pn_mcp_smatrix_ics_linear_neg_source_raw ff_pns_mcp_smatrix_ics_linear_neg_source_raw ff_np_mcp_smatrix_ics_linear_neg_source_raw ff_nps_mcp_smatrix_ics_linear_neg_source_raw. ((forall ff_index_mcp_prefix_ics_linear_neg_source_raw_pp. (exists mcp_gap_ics_linear_neg_source_raw_pp_index. mcp_gap_ics_linear_neg_source_raw_pp_index + S (ff_index_mcp_prefix_ics_linear_neg_source_raw_pp) = ((r) * (1))) -> exists ff_row_mcp_prefix_ics_linear_neg_source_raw_pp ff_column_mcp_prefix_ics_linear_neg_source_raw_pp ff_value_mcp_prefix_ics_linear_neg_source_raw_pp. ((ff_index_mcp_prefix_ics_linear_neg_source_raw_pp) = (1) * ff_row_mcp_prefix_ics_linear_neg_source_raw_pp + ff_column_mcp_prefix_ics_linear_neg_source_raw_pp /\ ((exists mcp_gap_ics_linear_neg_source_raw_pp_column. mcp_gap_ics_linear_neg_source_raw_pp_column + S (ff_column_mcp_prefix_ics_linear_neg_source_raw_pp) = (1)) /\ ((exists ff_left_mcp_cell_ics_linear_neg_source_raw_pp_cell ff_left_scale_mcp_cell_ics_linear_neg_source_raw_pp_cell ff_right_mcp_cell_ics_linear_neg_source_raw_pp_cell ff_right_scale_mcp_cell_ics_linear_neg_source_raw_pp_cell. ((forall ff_index_mcp_ics_linear_neg_source_raw_pp_cell_row ff_source_mcp_ics_linear_neg_source_raw_pp_cell_row ff_target_mcp_ics_linear_neg_source_raw_pp_cell_row. (exists mcp_gap_ics_linear_neg_source_raw_pp_cell_row_bound. mcp_gap_ics_linear_neg_source_raw_pp_cell_row_bound + S (ff_index_mcp_ics_linear_neg_source_raw_pp_cell_row) = (w)) -> (((exists fs_h_mcp_ics_linear_neg_source_raw_pp_cell_row_source. fs_h_mcp_ics_linear_neg_source_raw_pp_cell_row_source + S (ff_source_mcp_ics_linear_neg_source_raw_pp_cell_row) = S ((S (((ff_row_mcp_prefix_ics_linear_neg_source_raw_pp) * (w)) + (1) * ff_index_mcp_ics_linear_neg_source_raw_pp_cell_row)) * ac)) /\ exists fs_q_mcp_ics_linear_neg_source_raw_pp_cell_row_source. ab = fs_q_mcp_ics_linear_neg_source_raw_pp_cell_row_source * S ((S (((ff_row_mcp_prefix_ics_linear_neg_source_raw_pp) * (w)) + (1) * ff_index_mcp_ics_linear_neg_source_raw_pp_cell_row)) * ac) + (ff_source_mcp_ics_linear_neg_source_raw_pp_cell_row))) -> (((exists fs_h_mcp_ics_linear_neg_source_raw_pp_cell_row_target. fs_h_mcp_ics_linear_neg_source_raw_pp_cell_row_target + S (ff_target_mcp_ics_linear_neg_source_raw_pp_cell_row) = S ((S (ff_index_mcp_ics_linear_neg_source_raw_pp_cell_row)) * ff_left_scale_mcp_cell_ics_linear_neg_source_raw_pp_cell)) /\ exists fs_q_mcp_ics_linear_neg_source_raw_pp_cell_row_target. ff_left_mcp_cell_ics_linear_neg_source_raw_pp_cell = fs_q_mcp_ics_linear_neg_source_raw_pp_cell_row_target * S ((S (ff_index_mcp_ics_linear_neg_source_raw_pp_cell_row)) * ff_left_scale_mcp_cell_ics_linear_neg_source_raw_pp_cell) + (ff_target_mcp_ics_linear_neg_source_raw_pp_cell_row))) -> ff_target_mcp_ics_linear_neg_source_raw_pp_cell_row = ff_source_mcp_ics_linear_neg_source_raw_pp_cell_row) /\ ((forall ff_index_mcp_ics_linear_neg_source_raw_pp_cell_column ff_source_mcp_ics_linear_neg_source_raw_pp_cell_column ff_target_mcp_ics_linear_neg_source_raw_pp_cell_column. (exists mcp_gap_ics_linear_neg_source_raw_pp_cell_column_bound. mcp_gap_ics_linear_neg_source_raw_pp_cell_column_bound + S (ff_index_mcp_ics_linear_neg_source_raw_pp_cell_column) = (w)) -> (((exists fs_h_mcp_ics_linear_neg_source_raw_pp_cell_column_source. fs_h_mcp_ics_linear_neg_source_raw_pp_cell_column_source + S (ff_source_mcp_ics_linear_neg_source_raw_pp_cell_column) = S ((S ((ff_column_mcp_prefix_ics_linear_neg_source_raw_pp) + (1) * ff_index_mcp_ics_linear_neg_source_raw_pp_cell_column)) * ec)) /\ exists fs_q_mcp_ics_linear_neg_source_raw_pp_cell_column_source. eb = fs_q_mcp_ics_linear_neg_source_raw_pp_cell_column_source * S ((S ((ff_column_mcp_prefix_ics_linear_neg_source_raw_pp) + (1) * ff_index_mcp_ics_linear_neg_source_raw_pp_cell_column)) * ec) + (ff_source_mcp_ics_linear_neg_source_raw_pp_cell_column))) -> (((exists fs_h_mcp_ics_linear_neg_source_raw_pp_cell_column_target. fs_h_mcp_ics_linear_neg_source_raw_pp_cell_column_target + S (ff_target_mcp_ics_linear_neg_source_raw_pp_cell_column) = S ((S (ff_index_mcp_ics_linear_neg_source_raw_pp_cell_column)) * ff_right_scale_mcp_cell_ics_linear_neg_source_raw_pp_cell)) /\ exists fs_q_mcp_ics_linear_neg_source_raw_pp_cell_column_target. ff_right_mcp_cell_ics_linear_neg_source_raw_pp_cell = fs_q_mcp_ics_linear_neg_source_raw_pp_cell_column_target * S ((S (ff_index_mcp_ics_linear_neg_source_raw_pp_cell_column)) * ff_right_scale_mcp_cell_ics_linear_neg_source_raw_pp_cell) + (ff_target_mcp_ics_linear_neg_source_raw_pp_cell_column))) -> ff_target_mcp_ics_linear_neg_source_raw_pp_cell_column = ff_source_mcp_ics_linear_neg_source_raw_pp_cell_column) /\ (exists ff_code_dot_mcp_ics_linear_neg_source_raw_pp_cell_dot ff_scale_dot_mcp_ics_linear_neg_source_raw_pp_cell_dot. ((forall fpmp_index_dot_mcp_ics_linear_neg_source_raw_pp_cell_dot_pointwise fpmp_left_dot_mcp_ics_linear_neg_source_raw_pp_cell_dot_pointwise fpmp_right_dot_mcp_ics_linear_neg_source_raw_pp_cell_dot_pointwise fpmp_target_dot_mcp_ics_linear_neg_source_raw_pp_cell_dot_pointwise. (exists fpmp_gap_dot_mcp_ics_linear_neg_source_raw_pp_cell_dot_pointwise. fpmp_gap_dot_mcp_ics_linear_neg_source_raw_pp_cell_dot_pointwise + S fpmp_index_dot_mcp_ics_linear_neg_source_raw_pp_cell_dot_pointwise = w) -> (((exists ff_h_fpmp_dot_mcp_ics_linear_neg_source_raw_pp_cell_dot_pointwise_left. ff_h_fpmp_dot_mcp_ics_linear_neg_source_raw_pp_cell_dot_pointwise_left + S (fpmp_left_dot_mcp_ics_linear_neg_source_raw_pp_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_linear_neg_source_raw_pp_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_linear_neg_source_raw_pp_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_linear_neg_source_raw_pp_cell_dot_pointwise_left. ff_left_mcp_cell_ics_linear_neg_source_raw_pp_cell = ff_q_fpmp_dot_mcp_ics_linear_neg_source_raw_pp_cell_dot_pointwise_left * S ((S (fpmp_index_dot_mcp_ics_linear_neg_source_raw_pp_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_linear_neg_source_raw_pp_cell) + (fpmp_left_dot_mcp_ics_linear_neg_source_raw_pp_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_linear_neg_source_raw_pp_cell_dot_pointwise_right. ff_h_fpmp_dot_mcp_ics_linear_neg_source_raw_pp_cell_dot_pointwise_right + S (fpmp_right_dot_mcp_ics_linear_neg_source_raw_pp_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_linear_neg_source_raw_pp_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_linear_neg_source_raw_pp_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_linear_neg_source_raw_pp_cell_dot_pointwise_right. ff_right_mcp_cell_ics_linear_neg_source_raw_pp_cell = ff_q_fpmp_dot_mcp_ics_linear_neg_source_raw_pp_cell_dot_pointwise_right * S ((S (fpmp_index_dot_mcp_ics_linear_neg_source_raw_pp_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_linear_neg_source_raw_pp_cell) + (fpmp_right_dot_mcp_ics_linear_neg_source_raw_pp_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_linear_neg_source_raw_pp_cell_dot_pointwise_target. ff_h_fpmp_dot_mcp_ics_linear_neg_source_raw_pp_cell_dot_pointwise_target + S (fpmp_target_dot_mcp_ics_linear_neg_source_raw_pp_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_linear_neg_source_raw_pp_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_linear_neg_source_raw_pp_cell_dot)) /\ exists ff_q_fpmp_dot_mcp_ics_linear_neg_source_raw_pp_cell_dot_pointwise_target. ff_code_dot_mcp_ics_linear_neg_source_raw_pp_cell_dot = ff_q_fpmp_dot_mcp_ics_linear_neg_source_raw_pp_cell_dot_pointwise_target * S ((S (fpmp_index_dot_mcp_ics_linear_neg_source_raw_pp_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_linear_neg_source_raw_pp_cell_dot) + (fpmp_target_dot_mcp_ics_linear_neg_source_raw_pp_cell_dot_pointwise))) -> fpmp_target_dot_mcp_ics_linear_neg_source_raw_pp_cell_dot_pointwise = fpmp_left_dot_mcp_ics_linear_neg_source_raw_pp_cell_dot_pointwise * fpmp_right_dot_mcp_ics_linear_neg_source_raw_pp_cell_dot_pointwise) /\ (exists ff_u_dot_mcp_ics_linear_neg_source_raw_pp_cell_dot_sum ff_v_dot_mcp_ics_linear_neg_source_raw_pp_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_linear_neg_source_raw_pp_cell_dot_sum_start. ff_h_dot_mcp_ics_linear_neg_source_raw_pp_cell_dot_sum_start + S (0) = S ((S (0)) * ff_v_dot_mcp_ics_linear_neg_source_raw_pp_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_linear_neg_source_raw_pp_cell_dot_sum_start. ff_u_dot_mcp_ics_linear_neg_source_raw_pp_cell_dot_sum = ff_q_dot_mcp_ics_linear_neg_source_raw_pp_cell_dot_sum_start * S ((S (0)) * ff_v_dot_mcp_ics_linear_neg_source_raw_pp_cell_dot_sum) + (0))) /\ ((((exists ff_h_dot_mcp_ics_linear_neg_source_raw_pp_cell_dot_sum_terminal. ff_h_dot_mcp_ics_linear_neg_source_raw_pp_cell_dot_sum_terminal + S (ff_value_mcp_prefix_ics_linear_neg_source_raw_pp) = S ((S (w)) * ff_v_dot_mcp_ics_linear_neg_source_raw_pp_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_linear_neg_source_raw_pp_cell_dot_sum_terminal. ff_u_dot_mcp_ics_linear_neg_source_raw_pp_cell_dot_sum = ff_q_dot_mcp_ics_linear_neg_source_raw_pp_cell_dot_sum_terminal * S ((S (w)) * ff_v_dot_mcp_ics_linear_neg_source_raw_pp_cell_dot_sum) + (ff_value_mcp_prefix_ics_linear_neg_source_raw_pp))) /\ forall ff_i_dot_mcp_ics_linear_neg_source_raw_pp_cell_dot_sum. (exists ff_lt_dot_mcp_ics_linear_neg_source_raw_pp_cell_dot_sum_bound. ff_lt_dot_mcp_ics_linear_neg_source_raw_pp_cell_dot_sum_bound + S ff_i_dot_mcp_ics_linear_neg_source_raw_pp_cell_dot_sum = w) -> exists ff_a_dot_mcp_ics_linear_neg_source_raw_pp_cell_dot_sum ff_r_dot_mcp_ics_linear_neg_source_raw_pp_cell_dot_sum ff_s_dot_mcp_ics_linear_neg_source_raw_pp_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_linear_neg_source_raw_pp_cell_dot_sum_summand. ff_h_dot_mcp_ics_linear_neg_source_raw_pp_cell_dot_sum_summand + S (ff_a_dot_mcp_ics_linear_neg_source_raw_pp_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_linear_neg_source_raw_pp_cell_dot_sum)) * ff_scale_dot_mcp_ics_linear_neg_source_raw_pp_cell_dot)) /\ exists ff_q_dot_mcp_ics_linear_neg_source_raw_pp_cell_dot_sum_summand. ff_code_dot_mcp_ics_linear_neg_source_raw_pp_cell_dot = ff_q_dot_mcp_ics_linear_neg_source_raw_pp_cell_dot_sum_summand * S ((S (ff_i_dot_mcp_ics_linear_neg_source_raw_pp_cell_dot_sum)) * ff_scale_dot_mcp_ics_linear_neg_source_raw_pp_cell_dot) + (ff_a_dot_mcp_ics_linear_neg_source_raw_pp_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_linear_neg_source_raw_pp_cell_dot_sum_partial. ff_h_dot_mcp_ics_linear_neg_source_raw_pp_cell_dot_sum_partial + S (ff_r_dot_mcp_ics_linear_neg_source_raw_pp_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_linear_neg_source_raw_pp_cell_dot_sum)) * ff_v_dot_mcp_ics_linear_neg_source_raw_pp_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_linear_neg_source_raw_pp_cell_dot_sum_partial. ff_u_dot_mcp_ics_linear_neg_source_raw_pp_cell_dot_sum = ff_q_dot_mcp_ics_linear_neg_source_raw_pp_cell_dot_sum_partial * S ((S (ff_i_dot_mcp_ics_linear_neg_source_raw_pp_cell_dot_sum)) * ff_v_dot_mcp_ics_linear_neg_source_raw_pp_cell_dot_sum) + (ff_r_dot_mcp_ics_linear_neg_source_raw_pp_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_linear_neg_source_raw_pp_cell_dot_sum_successor. ff_h_dot_mcp_ics_linear_neg_source_raw_pp_cell_dot_sum_successor + S (ff_s_dot_mcp_ics_linear_neg_source_raw_pp_cell_dot_sum) = S ((S (S ff_i_dot_mcp_ics_linear_neg_source_raw_pp_cell_dot_sum)) * ff_v_dot_mcp_ics_linear_neg_source_raw_pp_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_linear_neg_source_raw_pp_cell_dot_sum_successor. ff_u_dot_mcp_ics_linear_neg_source_raw_pp_cell_dot_sum = ff_q_dot_mcp_ics_linear_neg_source_raw_pp_cell_dot_sum_successor * S ((S (S ff_i_dot_mcp_ics_linear_neg_source_raw_pp_cell_dot_sum)) * ff_v_dot_mcp_ics_linear_neg_source_raw_pp_cell_dot_sum) + (ff_s_dot_mcp_ics_linear_neg_source_raw_pp_cell_dot_sum))) /\ ff_s_dot_mcp_ics_linear_neg_source_raw_pp_cell_dot_sum = ff_r_dot_mcp_ics_linear_neg_source_raw_pp_cell_dot_sum + ff_a_dot_mcp_ics_linear_neg_source_raw_pp_cell_dot_sum))))))))))) /\ (((exists fs_h_mcp_ics_linear_neg_source_raw_pp_entry. fs_h_mcp_ics_linear_neg_source_raw_pp_entry + S (ff_value_mcp_prefix_ics_linear_neg_source_raw_pp) = S ((S (ff_index_mcp_prefix_ics_linear_neg_source_raw_pp)) * ff_pps_mcp_smatrix_ics_linear_neg_source_raw)) /\ exists fs_q_mcp_ics_linear_neg_source_raw_pp_entry. ff_pp_mcp_smatrix_ics_linear_neg_source_raw = fs_q_mcp_ics_linear_neg_source_raw_pp_entry * S ((S (ff_index_mcp_prefix_ics_linear_neg_source_raw_pp)) * ff_pps_mcp_smatrix_ics_linear_neg_source_raw) + (ff_value_mcp_prefix_ics_linear_neg_source_raw_pp))))))) /\ ((forall ff_index_mcp_prefix_ics_linear_neg_source_raw_nn. (exists mcp_gap_ics_linear_neg_source_raw_nn_index. mcp_gap_ics_linear_neg_source_raw_nn_index + S (ff_index_mcp_prefix_ics_linear_neg_source_raw_nn) = ((r) * (1))) -> exists ff_row_mcp_prefix_ics_linear_neg_source_raw_nn ff_column_mcp_prefix_ics_linear_neg_source_raw_nn ff_value_mcp_prefix_ics_linear_neg_source_raw_nn. ((ff_index_mcp_prefix_ics_linear_neg_source_raw_nn) = (1) * ff_row_mcp_prefix_ics_linear_neg_source_raw_nn + ff_column_mcp_prefix_ics_linear_neg_source_raw_nn /\ ((exists mcp_gap_ics_linear_neg_source_raw_nn_column. mcp_gap_ics_linear_neg_source_raw_nn_column + S (ff_column_mcp_prefix_ics_linear_neg_source_raw_nn) = (1)) /\ ((exists ff_left_mcp_cell_ics_linear_neg_source_raw_nn_cell ff_left_scale_mcp_cell_ics_linear_neg_source_raw_nn_cell ff_right_mcp_cell_ics_linear_neg_source_raw_nn_cell ff_right_scale_mcp_cell_ics_linear_neg_source_raw_nn_cell. ((forall ff_index_mcp_ics_linear_neg_source_raw_nn_cell_row ff_source_mcp_ics_linear_neg_source_raw_nn_cell_row ff_target_mcp_ics_linear_neg_source_raw_nn_cell_row. (exists mcp_gap_ics_linear_neg_source_raw_nn_cell_row_bound. mcp_gap_ics_linear_neg_source_raw_nn_cell_row_bound + S (ff_index_mcp_ics_linear_neg_source_raw_nn_cell_row) = (w)) -> (((exists fs_h_mcp_ics_linear_neg_source_raw_nn_cell_row_source. fs_h_mcp_ics_linear_neg_source_raw_nn_cell_row_source + S (ff_source_mcp_ics_linear_neg_source_raw_nn_cell_row) = S ((S (((ff_row_mcp_prefix_ics_linear_neg_source_raw_nn) * (w)) + (1) * ff_index_mcp_ics_linear_neg_source_raw_nn_cell_row)) * dc)) /\ exists fs_q_mcp_ics_linear_neg_source_raw_nn_cell_row_source. db = fs_q_mcp_ics_linear_neg_source_raw_nn_cell_row_source * S ((S (((ff_row_mcp_prefix_ics_linear_neg_source_raw_nn) * (w)) + (1) * ff_index_mcp_ics_linear_neg_source_raw_nn_cell_row)) * dc) + (ff_source_mcp_ics_linear_neg_source_raw_nn_cell_row))) -> (((exists fs_h_mcp_ics_linear_neg_source_raw_nn_cell_row_target. fs_h_mcp_ics_linear_neg_source_raw_nn_cell_row_target + S (ff_target_mcp_ics_linear_neg_source_raw_nn_cell_row) = S ((S (ff_index_mcp_ics_linear_neg_source_raw_nn_cell_row)) * ff_left_scale_mcp_cell_ics_linear_neg_source_raw_nn_cell)) /\ exists fs_q_mcp_ics_linear_neg_source_raw_nn_cell_row_target. ff_left_mcp_cell_ics_linear_neg_source_raw_nn_cell = fs_q_mcp_ics_linear_neg_source_raw_nn_cell_row_target * S ((S (ff_index_mcp_ics_linear_neg_source_raw_nn_cell_row)) * ff_left_scale_mcp_cell_ics_linear_neg_source_raw_nn_cell) + (ff_target_mcp_ics_linear_neg_source_raw_nn_cell_row))) -> ff_target_mcp_ics_linear_neg_source_raw_nn_cell_row = ff_source_mcp_ics_linear_neg_source_raw_nn_cell_row) /\ ((forall ff_index_mcp_ics_linear_neg_source_raw_nn_cell_column ff_source_mcp_ics_linear_neg_source_raw_nn_cell_column ff_target_mcp_ics_linear_neg_source_raw_nn_cell_column. (exists mcp_gap_ics_linear_neg_source_raw_nn_cell_column_bound. mcp_gap_ics_linear_neg_source_raw_nn_cell_column_bound + S (ff_index_mcp_ics_linear_neg_source_raw_nn_cell_column) = (w)) -> (((exists fs_h_mcp_ics_linear_neg_source_raw_nn_cell_column_source. fs_h_mcp_ics_linear_neg_source_raw_nn_cell_column_source + S (ff_source_mcp_ics_linear_neg_source_raw_nn_cell_column) = S ((S ((ff_column_mcp_prefix_ics_linear_neg_source_raw_nn) + (1) * ff_index_mcp_ics_linear_neg_source_raw_nn_cell_column)) * fc)) /\ exists fs_q_mcp_ics_linear_neg_source_raw_nn_cell_column_source. fb = fs_q_mcp_ics_linear_neg_source_raw_nn_cell_column_source * S ((S ((ff_column_mcp_prefix_ics_linear_neg_source_raw_nn) + (1) * ff_index_mcp_ics_linear_neg_source_raw_nn_cell_column)) * fc) + (ff_source_mcp_ics_linear_neg_source_raw_nn_cell_column))) -> (((exists fs_h_mcp_ics_linear_neg_source_raw_nn_cell_column_target. fs_h_mcp_ics_linear_neg_source_raw_nn_cell_column_target + S (ff_target_mcp_ics_linear_neg_source_raw_nn_cell_column) = S ((S (ff_index_mcp_ics_linear_neg_source_raw_nn_cell_column)) * ff_right_scale_mcp_cell_ics_linear_neg_source_raw_nn_cell)) /\ exists fs_q_mcp_ics_linear_neg_source_raw_nn_cell_column_target. ff_right_mcp_cell_ics_linear_neg_source_raw_nn_cell = fs_q_mcp_ics_linear_neg_source_raw_nn_cell_column_target * S ((S (ff_index_mcp_ics_linear_neg_source_raw_nn_cell_column)) * ff_right_scale_mcp_cell_ics_linear_neg_source_raw_nn_cell) + (ff_target_mcp_ics_linear_neg_source_raw_nn_cell_column))) -> ff_target_mcp_ics_linear_neg_source_raw_nn_cell_column = ff_source_mcp_ics_linear_neg_source_raw_nn_cell_column) /\ (exists ff_code_dot_mcp_ics_linear_neg_source_raw_nn_cell_dot ff_scale_dot_mcp_ics_linear_neg_source_raw_nn_cell_dot. ((forall fpmp_index_dot_mcp_ics_linear_neg_source_raw_nn_cell_dot_pointwise fpmp_left_dot_mcp_ics_linear_neg_source_raw_nn_cell_dot_pointwise fpmp_right_dot_mcp_ics_linear_neg_source_raw_nn_cell_dot_pointwise fpmp_target_dot_mcp_ics_linear_neg_source_raw_nn_cell_dot_pointwise. (exists fpmp_gap_dot_mcp_ics_linear_neg_source_raw_nn_cell_dot_pointwise. fpmp_gap_dot_mcp_ics_linear_neg_source_raw_nn_cell_dot_pointwise + S fpmp_index_dot_mcp_ics_linear_neg_source_raw_nn_cell_dot_pointwise = w) -> (((exists ff_h_fpmp_dot_mcp_ics_linear_neg_source_raw_nn_cell_dot_pointwise_left. ff_h_fpmp_dot_mcp_ics_linear_neg_source_raw_nn_cell_dot_pointwise_left + S (fpmp_left_dot_mcp_ics_linear_neg_source_raw_nn_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_linear_neg_source_raw_nn_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_linear_neg_source_raw_nn_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_linear_neg_source_raw_nn_cell_dot_pointwise_left. ff_left_mcp_cell_ics_linear_neg_source_raw_nn_cell = ff_q_fpmp_dot_mcp_ics_linear_neg_source_raw_nn_cell_dot_pointwise_left * S ((S (fpmp_index_dot_mcp_ics_linear_neg_source_raw_nn_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_linear_neg_source_raw_nn_cell) + (fpmp_left_dot_mcp_ics_linear_neg_source_raw_nn_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_linear_neg_source_raw_nn_cell_dot_pointwise_right. ff_h_fpmp_dot_mcp_ics_linear_neg_source_raw_nn_cell_dot_pointwise_right + S (fpmp_right_dot_mcp_ics_linear_neg_source_raw_nn_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_linear_neg_source_raw_nn_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_linear_neg_source_raw_nn_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_linear_neg_source_raw_nn_cell_dot_pointwise_right. ff_right_mcp_cell_ics_linear_neg_source_raw_nn_cell = ff_q_fpmp_dot_mcp_ics_linear_neg_source_raw_nn_cell_dot_pointwise_right * S ((S (fpmp_index_dot_mcp_ics_linear_neg_source_raw_nn_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_linear_neg_source_raw_nn_cell) + (fpmp_right_dot_mcp_ics_linear_neg_source_raw_nn_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_linear_neg_source_raw_nn_cell_dot_pointwise_target. ff_h_fpmp_dot_mcp_ics_linear_neg_source_raw_nn_cell_dot_pointwise_target + S (fpmp_target_dot_mcp_ics_linear_neg_source_raw_nn_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_linear_neg_source_raw_nn_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_linear_neg_source_raw_nn_cell_dot)) /\ exists ff_q_fpmp_dot_mcp_ics_linear_neg_source_raw_nn_cell_dot_pointwise_target. ff_code_dot_mcp_ics_linear_neg_source_raw_nn_cell_dot = ff_q_fpmp_dot_mcp_ics_linear_neg_source_raw_nn_cell_dot_pointwise_target * S ((S (fpmp_index_dot_mcp_ics_linear_neg_source_raw_nn_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_linear_neg_source_raw_nn_cell_dot) + (fpmp_target_dot_mcp_ics_linear_neg_source_raw_nn_cell_dot_pointwise))) -> fpmp_target_dot_mcp_ics_linear_neg_source_raw_nn_cell_dot_pointwise = fpmp_left_dot_mcp_ics_linear_neg_source_raw_nn_cell_dot_pointwise * fpmp_right_dot_mcp_ics_linear_neg_source_raw_nn_cell_dot_pointwise) /\ (exists ff_u_dot_mcp_ics_linear_neg_source_raw_nn_cell_dot_sum ff_v_dot_mcp_ics_linear_neg_source_raw_nn_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_linear_neg_source_raw_nn_cell_dot_sum_start. ff_h_dot_mcp_ics_linear_neg_source_raw_nn_cell_dot_sum_start + S (0) = S ((S (0)) * ff_v_dot_mcp_ics_linear_neg_source_raw_nn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_linear_neg_source_raw_nn_cell_dot_sum_start. ff_u_dot_mcp_ics_linear_neg_source_raw_nn_cell_dot_sum = ff_q_dot_mcp_ics_linear_neg_source_raw_nn_cell_dot_sum_start * S ((S (0)) * ff_v_dot_mcp_ics_linear_neg_source_raw_nn_cell_dot_sum) + (0))) /\ ((((exists ff_h_dot_mcp_ics_linear_neg_source_raw_nn_cell_dot_sum_terminal. ff_h_dot_mcp_ics_linear_neg_source_raw_nn_cell_dot_sum_terminal + S (ff_value_mcp_prefix_ics_linear_neg_source_raw_nn) = S ((S (w)) * ff_v_dot_mcp_ics_linear_neg_source_raw_nn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_linear_neg_source_raw_nn_cell_dot_sum_terminal. ff_u_dot_mcp_ics_linear_neg_source_raw_nn_cell_dot_sum = ff_q_dot_mcp_ics_linear_neg_source_raw_nn_cell_dot_sum_terminal * S ((S (w)) * ff_v_dot_mcp_ics_linear_neg_source_raw_nn_cell_dot_sum) + (ff_value_mcp_prefix_ics_linear_neg_source_raw_nn))) /\ forall ff_i_dot_mcp_ics_linear_neg_source_raw_nn_cell_dot_sum. (exists ff_lt_dot_mcp_ics_linear_neg_source_raw_nn_cell_dot_sum_bound. ff_lt_dot_mcp_ics_linear_neg_source_raw_nn_cell_dot_sum_bound + S ff_i_dot_mcp_ics_linear_neg_source_raw_nn_cell_dot_sum = w) -> exists ff_a_dot_mcp_ics_linear_neg_source_raw_nn_cell_dot_sum ff_r_dot_mcp_ics_linear_neg_source_raw_nn_cell_dot_sum ff_s_dot_mcp_ics_linear_neg_source_raw_nn_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_linear_neg_source_raw_nn_cell_dot_sum_summand. ff_h_dot_mcp_ics_linear_neg_source_raw_nn_cell_dot_sum_summand + S (ff_a_dot_mcp_ics_linear_neg_source_raw_nn_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_linear_neg_source_raw_nn_cell_dot_sum)) * ff_scale_dot_mcp_ics_linear_neg_source_raw_nn_cell_dot)) /\ exists ff_q_dot_mcp_ics_linear_neg_source_raw_nn_cell_dot_sum_summand. ff_code_dot_mcp_ics_linear_neg_source_raw_nn_cell_dot = ff_q_dot_mcp_ics_linear_neg_source_raw_nn_cell_dot_sum_summand * S ((S (ff_i_dot_mcp_ics_linear_neg_source_raw_nn_cell_dot_sum)) * ff_scale_dot_mcp_ics_linear_neg_source_raw_nn_cell_dot) + (ff_a_dot_mcp_ics_linear_neg_source_raw_nn_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_linear_neg_source_raw_nn_cell_dot_sum_partial. ff_h_dot_mcp_ics_linear_neg_source_raw_nn_cell_dot_sum_partial + S (ff_r_dot_mcp_ics_linear_neg_source_raw_nn_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_linear_neg_source_raw_nn_cell_dot_sum)) * ff_v_dot_mcp_ics_linear_neg_source_raw_nn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_linear_neg_source_raw_nn_cell_dot_sum_partial. ff_u_dot_mcp_ics_linear_neg_source_raw_nn_cell_dot_sum = ff_q_dot_mcp_ics_linear_neg_source_raw_nn_cell_dot_sum_partial * S ((S (ff_i_dot_mcp_ics_linear_neg_source_raw_nn_cell_dot_sum)) * ff_v_dot_mcp_ics_linear_neg_source_raw_nn_cell_dot_sum) + (ff_r_dot_mcp_ics_linear_neg_source_raw_nn_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_linear_neg_source_raw_nn_cell_dot_sum_successor. ff_h_dot_mcp_ics_linear_neg_source_raw_nn_cell_dot_sum_successor + S (ff_s_dot_mcp_ics_linear_neg_source_raw_nn_cell_dot_sum) = S ((S (S ff_i_dot_mcp_ics_linear_neg_source_raw_nn_cell_dot_sum)) * ff_v_dot_mcp_ics_linear_neg_source_raw_nn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_linear_neg_source_raw_nn_cell_dot_sum_successor. ff_u_dot_mcp_ics_linear_neg_source_raw_nn_cell_dot_sum = ff_q_dot_mcp_ics_linear_neg_source_raw_nn_cell_dot_sum_successor * S ((S (S ff_i_dot_mcp_ics_linear_neg_source_raw_nn_cell_dot_sum)) * ff_v_dot_mcp_ics_linear_neg_source_raw_nn_cell_dot_sum) + (ff_s_dot_mcp_ics_linear_neg_source_raw_nn_cell_dot_sum))) /\ ff_s_dot_mcp_ics_linear_neg_source_raw_nn_cell_dot_sum = ff_r_dot_mcp_ics_linear_neg_source_raw_nn_cell_dot_sum + ff_a_dot_mcp_ics_linear_neg_source_raw_nn_cell_dot_sum))))))))))) /\ (((exists fs_h_mcp_ics_linear_neg_source_raw_nn_entry. fs_h_mcp_ics_linear_neg_source_raw_nn_entry + S (ff_value_mcp_prefix_ics_linear_neg_source_raw_nn) = S ((S (ff_index_mcp_prefix_ics_linear_neg_source_raw_nn)) * ff_nns_mcp_smatrix_ics_linear_neg_source_raw)) /\ exists fs_q_mcp_ics_linear_neg_source_raw_nn_entry. ff_nn_mcp_smatrix_ics_linear_neg_source_raw = fs_q_mcp_ics_linear_neg_source_raw_nn_entry * S ((S (ff_index_mcp_prefix_ics_linear_neg_source_raw_nn)) * ff_nns_mcp_smatrix_ics_linear_neg_source_raw) + (ff_value_mcp_prefix_ics_linear_neg_source_raw_nn))))))) /\ ((forall ff_index_mcp_prefix_ics_linear_neg_source_raw_pn. (exists mcp_gap_ics_linear_neg_source_raw_pn_index. mcp_gap_ics_linear_neg_source_raw_pn_index + S (ff_index_mcp_prefix_ics_linear_neg_source_raw_pn) = ((r) * (1))) -> exists ff_row_mcp_prefix_ics_linear_neg_source_raw_pn ff_column_mcp_prefix_ics_linear_neg_source_raw_pn ff_value_mcp_prefix_ics_linear_neg_source_raw_pn. ((ff_index_mcp_prefix_ics_linear_neg_source_raw_pn) = (1) * ff_row_mcp_prefix_ics_linear_neg_source_raw_pn + ff_column_mcp_prefix_ics_linear_neg_source_raw_pn /\ ((exists mcp_gap_ics_linear_neg_source_raw_pn_column. mcp_gap_ics_linear_neg_source_raw_pn_column + S (ff_column_mcp_prefix_ics_linear_neg_source_raw_pn) = (1)) /\ ((exists ff_left_mcp_cell_ics_linear_neg_source_raw_pn_cell ff_left_scale_mcp_cell_ics_linear_neg_source_raw_pn_cell ff_right_mcp_cell_ics_linear_neg_source_raw_pn_cell ff_right_scale_mcp_cell_ics_linear_neg_source_raw_pn_cell. ((forall ff_index_mcp_ics_linear_neg_source_raw_pn_cell_row ff_source_mcp_ics_linear_neg_source_raw_pn_cell_row ff_target_mcp_ics_linear_neg_source_raw_pn_cell_row. (exists mcp_gap_ics_linear_neg_source_raw_pn_cell_row_bound. mcp_gap_ics_linear_neg_source_raw_pn_cell_row_bound + S (ff_index_mcp_ics_linear_neg_source_raw_pn_cell_row) = (w)) -> (((exists fs_h_mcp_ics_linear_neg_source_raw_pn_cell_row_source. fs_h_mcp_ics_linear_neg_source_raw_pn_cell_row_source + S (ff_source_mcp_ics_linear_neg_source_raw_pn_cell_row) = S ((S (((ff_row_mcp_prefix_ics_linear_neg_source_raw_pn) * (w)) + (1) * ff_index_mcp_ics_linear_neg_source_raw_pn_cell_row)) * ac)) /\ exists fs_q_mcp_ics_linear_neg_source_raw_pn_cell_row_source. ab = fs_q_mcp_ics_linear_neg_source_raw_pn_cell_row_source * S ((S (((ff_row_mcp_prefix_ics_linear_neg_source_raw_pn) * (w)) + (1) * ff_index_mcp_ics_linear_neg_source_raw_pn_cell_row)) * ac) + (ff_source_mcp_ics_linear_neg_source_raw_pn_cell_row))) -> (((exists fs_h_mcp_ics_linear_neg_source_raw_pn_cell_row_target. fs_h_mcp_ics_linear_neg_source_raw_pn_cell_row_target + S (ff_target_mcp_ics_linear_neg_source_raw_pn_cell_row) = S ((S (ff_index_mcp_ics_linear_neg_source_raw_pn_cell_row)) * ff_left_scale_mcp_cell_ics_linear_neg_source_raw_pn_cell)) /\ exists fs_q_mcp_ics_linear_neg_source_raw_pn_cell_row_target. ff_left_mcp_cell_ics_linear_neg_source_raw_pn_cell = fs_q_mcp_ics_linear_neg_source_raw_pn_cell_row_target * S ((S (ff_index_mcp_ics_linear_neg_source_raw_pn_cell_row)) * ff_left_scale_mcp_cell_ics_linear_neg_source_raw_pn_cell) + (ff_target_mcp_ics_linear_neg_source_raw_pn_cell_row))) -> ff_target_mcp_ics_linear_neg_source_raw_pn_cell_row = ff_source_mcp_ics_linear_neg_source_raw_pn_cell_row) /\ ((forall ff_index_mcp_ics_linear_neg_source_raw_pn_cell_column ff_source_mcp_ics_linear_neg_source_raw_pn_cell_column ff_target_mcp_ics_linear_neg_source_raw_pn_cell_column. (exists mcp_gap_ics_linear_neg_source_raw_pn_cell_column_bound. mcp_gap_ics_linear_neg_source_raw_pn_cell_column_bound + S (ff_index_mcp_ics_linear_neg_source_raw_pn_cell_column) = (w)) -> (((exists fs_h_mcp_ics_linear_neg_source_raw_pn_cell_column_source. fs_h_mcp_ics_linear_neg_source_raw_pn_cell_column_source + S (ff_source_mcp_ics_linear_neg_source_raw_pn_cell_column) = S ((S ((ff_column_mcp_prefix_ics_linear_neg_source_raw_pn) + (1) * ff_index_mcp_ics_linear_neg_source_raw_pn_cell_column)) * fc)) /\ exists fs_q_mcp_ics_linear_neg_source_raw_pn_cell_column_source. fb = fs_q_mcp_ics_linear_neg_source_raw_pn_cell_column_source * S ((S ((ff_column_mcp_prefix_ics_linear_neg_source_raw_pn) + (1) * ff_index_mcp_ics_linear_neg_source_raw_pn_cell_column)) * fc) + (ff_source_mcp_ics_linear_neg_source_raw_pn_cell_column))) -> (((exists fs_h_mcp_ics_linear_neg_source_raw_pn_cell_column_target. fs_h_mcp_ics_linear_neg_source_raw_pn_cell_column_target + S (ff_target_mcp_ics_linear_neg_source_raw_pn_cell_column) = S ((S (ff_index_mcp_ics_linear_neg_source_raw_pn_cell_column)) * ff_right_scale_mcp_cell_ics_linear_neg_source_raw_pn_cell)) /\ exists fs_q_mcp_ics_linear_neg_source_raw_pn_cell_column_target. ff_right_mcp_cell_ics_linear_neg_source_raw_pn_cell = fs_q_mcp_ics_linear_neg_source_raw_pn_cell_column_target * S ((S (ff_index_mcp_ics_linear_neg_source_raw_pn_cell_column)) * ff_right_scale_mcp_cell_ics_linear_neg_source_raw_pn_cell) + (ff_target_mcp_ics_linear_neg_source_raw_pn_cell_column))) -> ff_target_mcp_ics_linear_neg_source_raw_pn_cell_column = ff_source_mcp_ics_linear_neg_source_raw_pn_cell_column) /\ (exists ff_code_dot_mcp_ics_linear_neg_source_raw_pn_cell_dot ff_scale_dot_mcp_ics_linear_neg_source_raw_pn_cell_dot. ((forall fpmp_index_dot_mcp_ics_linear_neg_source_raw_pn_cell_dot_pointwise fpmp_left_dot_mcp_ics_linear_neg_source_raw_pn_cell_dot_pointwise fpmp_right_dot_mcp_ics_linear_neg_source_raw_pn_cell_dot_pointwise fpmp_target_dot_mcp_ics_linear_neg_source_raw_pn_cell_dot_pointwise. (exists fpmp_gap_dot_mcp_ics_linear_neg_source_raw_pn_cell_dot_pointwise. fpmp_gap_dot_mcp_ics_linear_neg_source_raw_pn_cell_dot_pointwise + S fpmp_index_dot_mcp_ics_linear_neg_source_raw_pn_cell_dot_pointwise = w) -> (((exists ff_h_fpmp_dot_mcp_ics_linear_neg_source_raw_pn_cell_dot_pointwise_left. ff_h_fpmp_dot_mcp_ics_linear_neg_source_raw_pn_cell_dot_pointwise_left + S (fpmp_left_dot_mcp_ics_linear_neg_source_raw_pn_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_linear_neg_source_raw_pn_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_linear_neg_source_raw_pn_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_linear_neg_source_raw_pn_cell_dot_pointwise_left. ff_left_mcp_cell_ics_linear_neg_source_raw_pn_cell = ff_q_fpmp_dot_mcp_ics_linear_neg_source_raw_pn_cell_dot_pointwise_left * S ((S (fpmp_index_dot_mcp_ics_linear_neg_source_raw_pn_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_linear_neg_source_raw_pn_cell) + (fpmp_left_dot_mcp_ics_linear_neg_source_raw_pn_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_linear_neg_source_raw_pn_cell_dot_pointwise_right. ff_h_fpmp_dot_mcp_ics_linear_neg_source_raw_pn_cell_dot_pointwise_right + S (fpmp_right_dot_mcp_ics_linear_neg_source_raw_pn_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_linear_neg_source_raw_pn_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_linear_neg_source_raw_pn_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_linear_neg_source_raw_pn_cell_dot_pointwise_right. ff_right_mcp_cell_ics_linear_neg_source_raw_pn_cell = ff_q_fpmp_dot_mcp_ics_linear_neg_source_raw_pn_cell_dot_pointwise_right * S ((S (fpmp_index_dot_mcp_ics_linear_neg_source_raw_pn_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_linear_neg_source_raw_pn_cell) + (fpmp_right_dot_mcp_ics_linear_neg_source_raw_pn_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_linear_neg_source_raw_pn_cell_dot_pointwise_target. ff_h_fpmp_dot_mcp_ics_linear_neg_source_raw_pn_cell_dot_pointwise_target + S (fpmp_target_dot_mcp_ics_linear_neg_source_raw_pn_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_linear_neg_source_raw_pn_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_linear_neg_source_raw_pn_cell_dot)) /\ exists ff_q_fpmp_dot_mcp_ics_linear_neg_source_raw_pn_cell_dot_pointwise_target. ff_code_dot_mcp_ics_linear_neg_source_raw_pn_cell_dot = ff_q_fpmp_dot_mcp_ics_linear_neg_source_raw_pn_cell_dot_pointwise_target * S ((S (fpmp_index_dot_mcp_ics_linear_neg_source_raw_pn_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_linear_neg_source_raw_pn_cell_dot) + (fpmp_target_dot_mcp_ics_linear_neg_source_raw_pn_cell_dot_pointwise))) -> fpmp_target_dot_mcp_ics_linear_neg_source_raw_pn_cell_dot_pointwise = fpmp_left_dot_mcp_ics_linear_neg_source_raw_pn_cell_dot_pointwise * fpmp_right_dot_mcp_ics_linear_neg_source_raw_pn_cell_dot_pointwise) /\ (exists ff_u_dot_mcp_ics_linear_neg_source_raw_pn_cell_dot_sum ff_v_dot_mcp_ics_linear_neg_source_raw_pn_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_linear_neg_source_raw_pn_cell_dot_sum_start. ff_h_dot_mcp_ics_linear_neg_source_raw_pn_cell_dot_sum_start + S (0) = S ((S (0)) * ff_v_dot_mcp_ics_linear_neg_source_raw_pn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_linear_neg_source_raw_pn_cell_dot_sum_start. ff_u_dot_mcp_ics_linear_neg_source_raw_pn_cell_dot_sum = ff_q_dot_mcp_ics_linear_neg_source_raw_pn_cell_dot_sum_start * S ((S (0)) * ff_v_dot_mcp_ics_linear_neg_source_raw_pn_cell_dot_sum) + (0))) /\ ((((exists ff_h_dot_mcp_ics_linear_neg_source_raw_pn_cell_dot_sum_terminal. ff_h_dot_mcp_ics_linear_neg_source_raw_pn_cell_dot_sum_terminal + S (ff_value_mcp_prefix_ics_linear_neg_source_raw_pn) = S ((S (w)) * ff_v_dot_mcp_ics_linear_neg_source_raw_pn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_linear_neg_source_raw_pn_cell_dot_sum_terminal. ff_u_dot_mcp_ics_linear_neg_source_raw_pn_cell_dot_sum = ff_q_dot_mcp_ics_linear_neg_source_raw_pn_cell_dot_sum_terminal * S ((S (w)) * ff_v_dot_mcp_ics_linear_neg_source_raw_pn_cell_dot_sum) + (ff_value_mcp_prefix_ics_linear_neg_source_raw_pn))) /\ forall ff_i_dot_mcp_ics_linear_neg_source_raw_pn_cell_dot_sum. (exists ff_lt_dot_mcp_ics_linear_neg_source_raw_pn_cell_dot_sum_bound. ff_lt_dot_mcp_ics_linear_neg_source_raw_pn_cell_dot_sum_bound + S ff_i_dot_mcp_ics_linear_neg_source_raw_pn_cell_dot_sum = w) -> exists ff_a_dot_mcp_ics_linear_neg_source_raw_pn_cell_dot_sum ff_r_dot_mcp_ics_linear_neg_source_raw_pn_cell_dot_sum ff_s_dot_mcp_ics_linear_neg_source_raw_pn_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_linear_neg_source_raw_pn_cell_dot_sum_summand. ff_h_dot_mcp_ics_linear_neg_source_raw_pn_cell_dot_sum_summand + S (ff_a_dot_mcp_ics_linear_neg_source_raw_pn_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_linear_neg_source_raw_pn_cell_dot_sum)) * ff_scale_dot_mcp_ics_linear_neg_source_raw_pn_cell_dot)) /\ exists ff_q_dot_mcp_ics_linear_neg_source_raw_pn_cell_dot_sum_summand. ff_code_dot_mcp_ics_linear_neg_source_raw_pn_cell_dot = ff_q_dot_mcp_ics_linear_neg_source_raw_pn_cell_dot_sum_summand * S ((S (ff_i_dot_mcp_ics_linear_neg_source_raw_pn_cell_dot_sum)) * ff_scale_dot_mcp_ics_linear_neg_source_raw_pn_cell_dot) + (ff_a_dot_mcp_ics_linear_neg_source_raw_pn_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_linear_neg_source_raw_pn_cell_dot_sum_partial. ff_h_dot_mcp_ics_linear_neg_source_raw_pn_cell_dot_sum_partial + S (ff_r_dot_mcp_ics_linear_neg_source_raw_pn_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_linear_neg_source_raw_pn_cell_dot_sum)) * ff_v_dot_mcp_ics_linear_neg_source_raw_pn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_linear_neg_source_raw_pn_cell_dot_sum_partial. ff_u_dot_mcp_ics_linear_neg_source_raw_pn_cell_dot_sum = ff_q_dot_mcp_ics_linear_neg_source_raw_pn_cell_dot_sum_partial * S ((S (ff_i_dot_mcp_ics_linear_neg_source_raw_pn_cell_dot_sum)) * ff_v_dot_mcp_ics_linear_neg_source_raw_pn_cell_dot_sum) + (ff_r_dot_mcp_ics_linear_neg_source_raw_pn_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_linear_neg_source_raw_pn_cell_dot_sum_successor. ff_h_dot_mcp_ics_linear_neg_source_raw_pn_cell_dot_sum_successor + S (ff_s_dot_mcp_ics_linear_neg_source_raw_pn_cell_dot_sum) = S ((S (S ff_i_dot_mcp_ics_linear_neg_source_raw_pn_cell_dot_sum)) * ff_v_dot_mcp_ics_linear_neg_source_raw_pn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_linear_neg_source_raw_pn_cell_dot_sum_successor. ff_u_dot_mcp_ics_linear_neg_source_raw_pn_cell_dot_sum = ff_q_dot_mcp_ics_linear_neg_source_raw_pn_cell_dot_sum_successor * S ((S (S ff_i_dot_mcp_ics_linear_neg_source_raw_pn_cell_dot_sum)) * ff_v_dot_mcp_ics_linear_neg_source_raw_pn_cell_dot_sum) + (ff_s_dot_mcp_ics_linear_neg_source_raw_pn_cell_dot_sum))) /\ ff_s_dot_mcp_ics_linear_neg_source_raw_pn_cell_dot_sum = ff_r_dot_mcp_ics_linear_neg_source_raw_pn_cell_dot_sum + ff_a_dot_mcp_ics_linear_neg_source_raw_pn_cell_dot_sum))))))))))) /\ (((exists fs_h_mcp_ics_linear_neg_source_raw_pn_entry. fs_h_mcp_ics_linear_neg_source_raw_pn_entry + S (ff_value_mcp_prefix_ics_linear_neg_source_raw_pn) = S ((S (ff_index_mcp_prefix_ics_linear_neg_source_raw_pn)) * ff_pns_mcp_smatrix_ics_linear_neg_source_raw)) /\ exists fs_q_mcp_ics_linear_neg_source_raw_pn_entry. ff_pn_mcp_smatrix_ics_linear_neg_source_raw = fs_q_mcp_ics_linear_neg_source_raw_pn_entry * S ((S (ff_index_mcp_prefix_ics_linear_neg_source_raw_pn)) * ff_pns_mcp_smatrix_ics_linear_neg_source_raw) + (ff_value_mcp_prefix_ics_linear_neg_source_raw_pn))))))) /\ ((forall ff_index_mcp_prefix_ics_linear_neg_source_raw_np. (exists mcp_gap_ics_linear_neg_source_raw_np_index. mcp_gap_ics_linear_neg_source_raw_np_index + S (ff_index_mcp_prefix_ics_linear_neg_source_raw_np) = ((r) * (1))) -> exists ff_row_mcp_prefix_ics_linear_neg_source_raw_np ff_column_mcp_prefix_ics_linear_neg_source_raw_np ff_value_mcp_prefix_ics_linear_neg_source_raw_np. ((ff_index_mcp_prefix_ics_linear_neg_source_raw_np) = (1) * ff_row_mcp_prefix_ics_linear_neg_source_raw_np + ff_column_mcp_prefix_ics_linear_neg_source_raw_np /\ ((exists mcp_gap_ics_linear_neg_source_raw_np_column. mcp_gap_ics_linear_neg_source_raw_np_column + S (ff_column_mcp_prefix_ics_linear_neg_source_raw_np) = (1)) /\ ((exists ff_left_mcp_cell_ics_linear_neg_source_raw_np_cell ff_left_scale_mcp_cell_ics_linear_neg_source_raw_np_cell ff_right_mcp_cell_ics_linear_neg_source_raw_np_cell ff_right_scale_mcp_cell_ics_linear_neg_source_raw_np_cell. ((forall ff_index_mcp_ics_linear_neg_source_raw_np_cell_row ff_source_mcp_ics_linear_neg_source_raw_np_cell_row ff_target_mcp_ics_linear_neg_source_raw_np_cell_row. (exists mcp_gap_ics_linear_neg_source_raw_np_cell_row_bound. mcp_gap_ics_linear_neg_source_raw_np_cell_row_bound + S (ff_index_mcp_ics_linear_neg_source_raw_np_cell_row) = (w)) -> (((exists fs_h_mcp_ics_linear_neg_source_raw_np_cell_row_source. fs_h_mcp_ics_linear_neg_source_raw_np_cell_row_source + S (ff_source_mcp_ics_linear_neg_source_raw_np_cell_row) = S ((S (((ff_row_mcp_prefix_ics_linear_neg_source_raw_np) * (w)) + (1) * ff_index_mcp_ics_linear_neg_source_raw_np_cell_row)) * dc)) /\ exists fs_q_mcp_ics_linear_neg_source_raw_np_cell_row_source. db = fs_q_mcp_ics_linear_neg_source_raw_np_cell_row_source * S ((S (((ff_row_mcp_prefix_ics_linear_neg_source_raw_np) * (w)) + (1) * ff_index_mcp_ics_linear_neg_source_raw_np_cell_row)) * dc) + (ff_source_mcp_ics_linear_neg_source_raw_np_cell_row))) -> (((exists fs_h_mcp_ics_linear_neg_source_raw_np_cell_row_target. fs_h_mcp_ics_linear_neg_source_raw_np_cell_row_target + S (ff_target_mcp_ics_linear_neg_source_raw_np_cell_row) = S ((S (ff_index_mcp_ics_linear_neg_source_raw_np_cell_row)) * ff_left_scale_mcp_cell_ics_linear_neg_source_raw_np_cell)) /\ exists fs_q_mcp_ics_linear_neg_source_raw_np_cell_row_target. ff_left_mcp_cell_ics_linear_neg_source_raw_np_cell = fs_q_mcp_ics_linear_neg_source_raw_np_cell_row_target * S ((S (ff_index_mcp_ics_linear_neg_source_raw_np_cell_row)) * ff_left_scale_mcp_cell_ics_linear_neg_source_raw_np_cell) + (ff_target_mcp_ics_linear_neg_source_raw_np_cell_row))) -> ff_target_mcp_ics_linear_neg_source_raw_np_cell_row = ff_source_mcp_ics_linear_neg_source_raw_np_cell_row) /\ ((forall ff_index_mcp_ics_linear_neg_source_raw_np_cell_column ff_source_mcp_ics_linear_neg_source_raw_np_cell_column ff_target_mcp_ics_linear_neg_source_raw_np_cell_column. (exists mcp_gap_ics_linear_neg_source_raw_np_cell_column_bound. mcp_gap_ics_linear_neg_source_raw_np_cell_column_bound + S (ff_index_mcp_ics_linear_neg_source_raw_np_cell_column) = (w)) -> (((exists fs_h_mcp_ics_linear_neg_source_raw_np_cell_column_source. fs_h_mcp_ics_linear_neg_source_raw_np_cell_column_source + S (ff_source_mcp_ics_linear_neg_source_raw_np_cell_column) = S ((S ((ff_column_mcp_prefix_ics_linear_neg_source_raw_np) + (1) * ff_index_mcp_ics_linear_neg_source_raw_np_cell_column)) * ec)) /\ exists fs_q_mcp_ics_linear_neg_source_raw_np_cell_column_source. eb = fs_q_mcp_ics_linear_neg_source_raw_np_cell_column_source * S ((S ((ff_column_mcp_prefix_ics_linear_neg_source_raw_np) + (1) * ff_index_mcp_ics_linear_neg_source_raw_np_cell_column)) * ec) + (ff_source_mcp_ics_linear_neg_source_raw_np_cell_column))) -> (((exists fs_h_mcp_ics_linear_neg_source_raw_np_cell_column_target. fs_h_mcp_ics_linear_neg_source_raw_np_cell_column_target + S (ff_target_mcp_ics_linear_neg_source_raw_np_cell_column) = S ((S (ff_index_mcp_ics_linear_neg_source_raw_np_cell_column)) * ff_right_scale_mcp_cell_ics_linear_neg_source_raw_np_cell)) /\ exists fs_q_mcp_ics_linear_neg_source_raw_np_cell_column_target. ff_right_mcp_cell_ics_linear_neg_source_raw_np_cell = fs_q_mcp_ics_linear_neg_source_raw_np_cell_column_target * S ((S (ff_index_mcp_ics_linear_neg_source_raw_np_cell_column)) * ff_right_scale_mcp_cell_ics_linear_neg_source_raw_np_cell) + (ff_target_mcp_ics_linear_neg_source_raw_np_cell_column))) -> ff_target_mcp_ics_linear_neg_source_raw_np_cell_column = ff_source_mcp_ics_linear_neg_source_raw_np_cell_column) /\ (exists ff_code_dot_mcp_ics_linear_neg_source_raw_np_cell_dot ff_scale_dot_mcp_ics_linear_neg_source_raw_np_cell_dot. ((forall fpmp_index_dot_mcp_ics_linear_neg_source_raw_np_cell_dot_pointwise fpmp_left_dot_mcp_ics_linear_neg_source_raw_np_cell_dot_pointwise fpmp_right_dot_mcp_ics_linear_neg_source_raw_np_cell_dot_pointwise fpmp_target_dot_mcp_ics_linear_neg_source_raw_np_cell_dot_pointwise. (exists fpmp_gap_dot_mcp_ics_linear_neg_source_raw_np_cell_dot_pointwise. fpmp_gap_dot_mcp_ics_linear_neg_source_raw_np_cell_dot_pointwise + S fpmp_index_dot_mcp_ics_linear_neg_source_raw_np_cell_dot_pointwise = w) -> (((exists ff_h_fpmp_dot_mcp_ics_linear_neg_source_raw_np_cell_dot_pointwise_left. ff_h_fpmp_dot_mcp_ics_linear_neg_source_raw_np_cell_dot_pointwise_left + S (fpmp_left_dot_mcp_ics_linear_neg_source_raw_np_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_linear_neg_source_raw_np_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_linear_neg_source_raw_np_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_linear_neg_source_raw_np_cell_dot_pointwise_left. ff_left_mcp_cell_ics_linear_neg_source_raw_np_cell = ff_q_fpmp_dot_mcp_ics_linear_neg_source_raw_np_cell_dot_pointwise_left * S ((S (fpmp_index_dot_mcp_ics_linear_neg_source_raw_np_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_linear_neg_source_raw_np_cell) + (fpmp_left_dot_mcp_ics_linear_neg_source_raw_np_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_linear_neg_source_raw_np_cell_dot_pointwise_right. ff_h_fpmp_dot_mcp_ics_linear_neg_source_raw_np_cell_dot_pointwise_right + S (fpmp_right_dot_mcp_ics_linear_neg_source_raw_np_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_linear_neg_source_raw_np_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_linear_neg_source_raw_np_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_linear_neg_source_raw_np_cell_dot_pointwise_right. ff_right_mcp_cell_ics_linear_neg_source_raw_np_cell = ff_q_fpmp_dot_mcp_ics_linear_neg_source_raw_np_cell_dot_pointwise_right * S ((S (fpmp_index_dot_mcp_ics_linear_neg_source_raw_np_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_linear_neg_source_raw_np_cell) + (fpmp_right_dot_mcp_ics_linear_neg_source_raw_np_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_linear_neg_source_raw_np_cell_dot_pointwise_target. ff_h_fpmp_dot_mcp_ics_linear_neg_source_raw_np_cell_dot_pointwise_target + S (fpmp_target_dot_mcp_ics_linear_neg_source_raw_np_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_linear_neg_source_raw_np_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_linear_neg_source_raw_np_cell_dot)) /\ exists ff_q_fpmp_dot_mcp_ics_linear_neg_source_raw_np_cell_dot_pointwise_target. ff_code_dot_mcp_ics_linear_neg_source_raw_np_cell_dot = ff_q_fpmp_dot_mcp_ics_linear_neg_source_raw_np_cell_dot_pointwise_target * S ((S (fpmp_index_dot_mcp_ics_linear_neg_source_raw_np_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_linear_neg_source_raw_np_cell_dot) + (fpmp_target_dot_mcp_ics_linear_neg_source_raw_np_cell_dot_pointwise))) -> fpmp_target_dot_mcp_ics_linear_neg_source_raw_np_cell_dot_pointwise = fpmp_left_dot_mcp_ics_linear_neg_source_raw_np_cell_dot_pointwise * fpmp_right_dot_mcp_ics_linear_neg_source_raw_np_cell_dot_pointwise) /\ (exists ff_u_dot_mcp_ics_linear_neg_source_raw_np_cell_dot_sum ff_v_dot_mcp_ics_linear_neg_source_raw_np_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_linear_neg_source_raw_np_cell_dot_sum_start. ff_h_dot_mcp_ics_linear_neg_source_raw_np_cell_dot_sum_start + S (0) = S ((S (0)) * ff_v_dot_mcp_ics_linear_neg_source_raw_np_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_linear_neg_source_raw_np_cell_dot_sum_start. ff_u_dot_mcp_ics_linear_neg_source_raw_np_cell_dot_sum = ff_q_dot_mcp_ics_linear_neg_source_raw_np_cell_dot_sum_start * S ((S (0)) * ff_v_dot_mcp_ics_linear_neg_source_raw_np_cell_dot_sum) + (0))) /\ ((((exists ff_h_dot_mcp_ics_linear_neg_source_raw_np_cell_dot_sum_terminal. ff_h_dot_mcp_ics_linear_neg_source_raw_np_cell_dot_sum_terminal + S (ff_value_mcp_prefix_ics_linear_neg_source_raw_np) = S ((S (w)) * ff_v_dot_mcp_ics_linear_neg_source_raw_np_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_linear_neg_source_raw_np_cell_dot_sum_terminal. ff_u_dot_mcp_ics_linear_neg_source_raw_np_cell_dot_sum = ff_q_dot_mcp_ics_linear_neg_source_raw_np_cell_dot_sum_terminal * S ((S (w)) * ff_v_dot_mcp_ics_linear_neg_source_raw_np_cell_dot_sum) + (ff_value_mcp_prefix_ics_linear_neg_source_raw_np))) /\ forall ff_i_dot_mcp_ics_linear_neg_source_raw_np_cell_dot_sum. (exists ff_lt_dot_mcp_ics_linear_neg_source_raw_np_cell_dot_sum_bound. ff_lt_dot_mcp_ics_linear_neg_source_raw_np_cell_dot_sum_bound + S ff_i_dot_mcp_ics_linear_neg_source_raw_np_cell_dot_sum = w) -> exists ff_a_dot_mcp_ics_linear_neg_source_raw_np_cell_dot_sum ff_r_dot_mcp_ics_linear_neg_source_raw_np_cell_dot_sum ff_s_dot_mcp_ics_linear_neg_source_raw_np_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_linear_neg_source_raw_np_cell_dot_sum_summand. ff_h_dot_mcp_ics_linear_neg_source_raw_np_cell_dot_sum_summand + S (ff_a_dot_mcp_ics_linear_neg_source_raw_np_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_linear_neg_source_raw_np_cell_dot_sum)) * ff_scale_dot_mcp_ics_linear_neg_source_raw_np_cell_dot)) /\ exists ff_q_dot_mcp_ics_linear_neg_source_raw_np_cell_dot_sum_summand. ff_code_dot_mcp_ics_linear_neg_source_raw_np_cell_dot = ff_q_dot_mcp_ics_linear_neg_source_raw_np_cell_dot_sum_summand * S ((S (ff_i_dot_mcp_ics_linear_neg_source_raw_np_cell_dot_sum)) * ff_scale_dot_mcp_ics_linear_neg_source_raw_np_cell_dot) + (ff_a_dot_mcp_ics_linear_neg_source_raw_np_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_linear_neg_source_raw_np_cell_dot_sum_partial. ff_h_dot_mcp_ics_linear_neg_source_raw_np_cell_dot_sum_partial + S (ff_r_dot_mcp_ics_linear_neg_source_raw_np_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_linear_neg_source_raw_np_cell_dot_sum)) * ff_v_dot_mcp_ics_linear_neg_source_raw_np_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_linear_neg_source_raw_np_cell_dot_sum_partial. ff_u_dot_mcp_ics_linear_neg_source_raw_np_cell_dot_sum = ff_q_dot_mcp_ics_linear_neg_source_raw_np_cell_dot_sum_partial * S ((S (ff_i_dot_mcp_ics_linear_neg_source_raw_np_cell_dot_sum)) * ff_v_dot_mcp_ics_linear_neg_source_raw_np_cell_dot_sum) + (ff_r_dot_mcp_ics_linear_neg_source_raw_np_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_linear_neg_source_raw_np_cell_dot_sum_successor. ff_h_dot_mcp_ics_linear_neg_source_raw_np_cell_dot_sum_successor + S (ff_s_dot_mcp_ics_linear_neg_source_raw_np_cell_dot_sum) = S ((S (S ff_i_dot_mcp_ics_linear_neg_source_raw_np_cell_dot_sum)) * ff_v_dot_mcp_ics_linear_neg_source_raw_np_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_linear_neg_source_raw_np_cell_dot_sum_successor. ff_u_dot_mcp_ics_linear_neg_source_raw_np_cell_dot_sum = ff_q_dot_mcp_ics_linear_neg_source_raw_np_cell_dot_sum_successor * S ((S (S ff_i_dot_mcp_ics_linear_neg_source_raw_np_cell_dot_sum)) * ff_v_dot_mcp_ics_linear_neg_source_raw_np_cell_dot_sum) + (ff_s_dot_mcp_ics_linear_neg_source_raw_np_cell_dot_sum))) /\ ff_s_dot_mcp_ics_linear_neg_source_raw_np_cell_dot_sum = ff_r_dot_mcp_ics_linear_neg_source_raw_np_cell_dot_sum + ff_a_dot_mcp_ics_linear_neg_source_raw_np_cell_dot_sum))))))))))) /\ (((exists fs_h_mcp_ics_linear_neg_source_raw_np_entry. fs_h_mcp_ics_linear_neg_source_raw_np_entry + S (ff_value_mcp_prefix_ics_linear_neg_source_raw_np) = S ((S (ff_index_mcp_prefix_ics_linear_neg_source_raw_np)) * ff_nps_mcp_smatrix_ics_linear_neg_source_raw)) /\ exists fs_q_mcp_ics_linear_neg_source_raw_np_entry. ff_np_mcp_smatrix_ics_linear_neg_source_raw = fs_q_mcp_ics_linear_neg_source_raw_np_entry * S ((S (ff_index_mcp_prefix_ics_linear_neg_source_raw_np)) * ff_nps_mcp_smatrix_ics_linear_neg_source_raw) + (ff_value_mcp_prefix_ics_linear_neg_source_raw_np))))))) /\ ((forall ff_index_mcp_add_ics_linear_neg_source_raw_positive ff_left_mcp_add_ics_linear_neg_source_raw_positive ff_right_mcp_add_ics_linear_neg_source_raw_positive ff_target_mcp_add_ics_linear_neg_source_raw_positive. (exists mcp_gap_ics_linear_neg_source_raw_positive_bound. mcp_gap_ics_linear_neg_source_raw_positive_bound + S (ff_index_mcp_add_ics_linear_neg_source_raw_positive) = ((r) * (1))) -> (((exists fs_h_mcp_ics_linear_neg_source_raw_positive_left. fs_h_mcp_ics_linear_neg_source_raw_positive_left + S (ff_left_mcp_add_ics_linear_neg_source_raw_positive) = S ((S (ff_index_mcp_add_ics_linear_neg_source_raw_positive)) * ff_pps_mcp_smatrix_ics_linear_neg_source_raw)) /\ exists fs_q_mcp_ics_linear_neg_source_raw_positive_left. ff_pp_mcp_smatrix_ics_linear_neg_source_raw = fs_q_mcp_ics_linear_neg_source_raw_positive_left * S ((S (ff_index_mcp_add_ics_linear_neg_source_raw_positive)) * ff_pps_mcp_smatrix_ics_linear_neg_source_raw) + (ff_left_mcp_add_ics_linear_neg_source_raw_positive))) -> (((exists fs_h_mcp_ics_linear_neg_source_raw_positive_right. fs_h_mcp_ics_linear_neg_source_raw_positive_right + S (ff_right_mcp_add_ics_linear_neg_source_raw_positive) = S ((S (ff_index_mcp_add_ics_linear_neg_source_raw_positive)) * ff_nns_mcp_smatrix_ics_linear_neg_source_raw)) /\ exists fs_q_mcp_ics_linear_neg_source_raw_positive_right. ff_nn_mcp_smatrix_ics_linear_neg_source_raw = fs_q_mcp_ics_linear_neg_source_raw_positive_right * S ((S (ff_index_mcp_add_ics_linear_neg_source_raw_positive)) * ff_nns_mcp_smatrix_ics_linear_neg_source_raw) + (ff_right_mcp_add_ics_linear_neg_source_raw_positive))) -> (((exists fs_h_mcp_ics_linear_neg_source_raw_positive_target. fs_h_mcp_ics_linear_neg_source_raw_positive_target + S (ff_target_mcp_add_ics_linear_neg_source_raw_positive) = S ((S (ff_index_mcp_add_ics_linear_neg_source_raw_positive)) * ics_raw_positive_scale_linear_neg_source)) /\ exists fs_q_mcp_ics_linear_neg_source_raw_positive_target. ics_raw_positive_linear_neg_source = fs_q_mcp_ics_linear_neg_source_raw_positive_target * S ((S (ff_index_mcp_add_ics_linear_neg_source_raw_positive)) * ics_raw_positive_scale_linear_neg_source) + (ff_target_mcp_add_ics_linear_neg_source_raw_positive))) -> ff_target_mcp_add_ics_linear_neg_source_raw_positive = ff_left_mcp_add_ics_linear_neg_source_raw_positive + ff_right_mcp_add_ics_linear_neg_source_raw_positive) /\ (forall ff_index_mcp_add_ics_linear_neg_source_raw_negative ff_left_mcp_add_ics_linear_neg_source_raw_negative ff_right_mcp_add_ics_linear_neg_source_raw_negative ff_target_mcp_add_ics_linear_neg_source_raw_negative. (exists mcp_gap_ics_linear_neg_source_raw_negative_bound. mcp_gap_ics_linear_neg_source_raw_negative_bound + S (ff_index_mcp_add_ics_linear_neg_source_raw_negative) = ((r) * (1))) -> (((exists fs_h_mcp_ics_linear_neg_source_raw_negative_left. fs_h_mcp_ics_linear_neg_source_raw_negative_left + S (ff_left_mcp_add_ics_linear_neg_source_raw_negative) = S ((S (ff_index_mcp_add_ics_linear_neg_source_raw_negative)) * ff_pns_mcp_smatrix_ics_linear_neg_source_raw)) /\ exists fs_q_mcp_ics_linear_neg_source_raw_negative_left. ff_pn_mcp_smatrix_ics_linear_neg_source_raw = fs_q_mcp_ics_linear_neg_source_raw_negative_left * S ((S (ff_index_mcp_add_ics_linear_neg_source_raw_negative)) * ff_pns_mcp_smatrix_ics_linear_neg_source_raw) + (ff_left_mcp_add_ics_linear_neg_source_raw_negative))) -> (((exists fs_h_mcp_ics_linear_neg_source_raw_negative_right. fs_h_mcp_ics_linear_neg_source_raw_negative_right + S (ff_right_mcp_add_ics_linear_neg_source_raw_negative) = S ((S (ff_index_mcp_add_ics_linear_neg_source_raw_negative)) * ff_nps_mcp_smatrix_ics_linear_neg_source_raw)) /\ exists fs_q_mcp_ics_linear_neg_source_raw_negative_right. ff_np_mcp_smatrix_ics_linear_neg_source_raw = fs_q_mcp_ics_linear_neg_source_raw_negative_right * S ((S (ff_index_mcp_add_ics_linear_neg_source_raw_negative)) * ff_nps_mcp_smatrix_ics_linear_neg_source_raw) + (ff_right_mcp_add_ics_linear_neg_source_raw_negative))) -> (((exists fs_h_mcp_ics_linear_neg_source_raw_negative_target. fs_h_mcp_ics_linear_neg_source_raw_negative_target + S (ff_target_mcp_add_ics_linear_neg_source_raw_negative) = S ((S (ff_index_mcp_add_ics_linear_neg_source_raw_negative)) * ics_raw_negative_scale_linear_neg_source)) /\ exists fs_q_mcp_ics_linear_neg_source_raw_negative_target. ics_raw_negative_linear_neg_source = fs_q_mcp_ics_linear_neg_source_raw_negative_target * S ((S (ff_index_mcp_add_ics_linear_neg_source_raw_negative)) * ics_raw_negative_scale_linear_neg_source) + (ff_target_mcp_add_ics_linear_neg_source_raw_negative))) -> ff_target_mcp_add_ics_linear_neg_source_raw_negative = ff_left_mcp_add_ics_linear_neg_source_raw_negative + ff_right_mcp_add_ics_linear_neg_source_raw_negative))))))) /\ (forall ics_index_linear_neg_source_equal ics_value0_linear_neg_source_equal ics_value1_linear_neg_source_equal ics_value2_linear_neg_source_equal ics_value3_linear_neg_source_equal. (exists ics_gap_linear_neg_source_equal_bound. ics_gap_linear_neg_source_equal_bound + S (ics_index_linear_neg_source_equal) = (r)) -> (((exists fs_h_ics_linear_neg_source_equal_at0. fs_h_ics_linear_neg_source_equal_at0 + S (ics_value0_linear_neg_source_equal) = S ((S (ics_index_linear_neg_source_equal)) * ics_raw_positive_scale_linear_neg_source)) /\ exists fs_q_ics_linear_neg_source_equal_at0. ics_raw_positive_linear_neg_source = fs_q_ics_linear_neg_source_equal_at0 * S ((S (ics_index_linear_neg_source_equal)) * ics_raw_positive_scale_linear_neg_source) + (ics_value0_linear_neg_source_equal))) -> (((exists fs_h_ics_linear_neg_source_equal_at1. fs_h_ics_linear_neg_source_equal_at1 + S (ics_value1_linear_neg_source_equal) = S ((S (ics_index_linear_neg_source_equal)) * ics_raw_negative_scale_linear_neg_source)) /\ exists fs_q_ics_linear_neg_source_equal_at1. ics_raw_negative_linear_neg_source = fs_q_ics_linear_neg_source_equal_at1 * S ((S (ics_index_linear_neg_source_equal)) * ics_raw_negative_scale_linear_neg_source) + (ics_value1_linear_neg_source_equal))) -> (((exists fs_h_ics_linear_neg_source_equal_at2. fs_h_ics_linear_neg_source_equal_at2 + S (ics_value2_linear_neg_source_equal) = S ((S (ics_index_linear_neg_source_equal)) * pc)) /\ exists fs_q_ics_linear_neg_source_equal_at2. pb = fs_q_ics_linear_neg_source_equal_at2 * S ((S (ics_index_linear_neg_source_equal)) * pc) + (ics_value2_linear_neg_source_equal))) -> (((exists fs_h_ics_linear_neg_source_equal_at3. fs_h_ics_linear_neg_source_equal_at3 + S (ics_value3_linear_neg_source_equal) = S ((S (ics_index_linear_neg_source_equal)) * nc)) /\ exists fs_q_ics_linear_neg_source_equal_at3. nb = fs_q_ics_linear_neg_source_equal_at3 * S ((S (ics_index_linear_neg_source_equal)) * nc) + (ics_value3_linear_neg_source_equal))) -> ics_value0_linear_neg_source_equal + ics_value3_linear_neg_source_equal = ics_value2_linear_neg_source_equal + ics_value1_linear_neg_source_equal)))) -> (exists ics_raw_positive_linear_neg_result ics_raw_positive_scale_linear_neg_result ics_raw_negative_linear_neg_result ics_raw_negative_scale_linear_neg_result. (((exists ff_pp_mcp_smatrix_ics_linear_neg_result_raw ff_pps_mcp_smatrix_ics_linear_neg_result_raw ff_nn_mcp_smatrix_ics_linear_neg_result_raw ff_nns_mcp_smatrix_ics_linear_neg_result_raw ff_pn_mcp_smatrix_ics_linear_neg_result_raw ff_pns_mcp_smatrix_ics_linear_neg_result_raw ff_np_mcp_smatrix_ics_linear_neg_result_raw ff_nps_mcp_smatrix_ics_linear_neg_result_raw. ((forall ff_index_mcp_prefix_ics_linear_neg_result_raw_pp. (exists mcp_gap_ics_linear_neg_result_raw_pp_index. mcp_gap_ics_linear_neg_result_raw_pp_index + S (ff_index_mcp_prefix_ics_linear_neg_result_raw_pp) = ((r) * (1))) -> exists ff_row_mcp_prefix_ics_linear_neg_result_raw_pp ff_column_mcp_prefix_ics_linear_neg_result_raw_pp ff_value_mcp_prefix_ics_linear_neg_result_raw_pp. ((ff_index_mcp_prefix_ics_linear_neg_result_raw_pp) = (1) * ff_row_mcp_prefix_ics_linear_neg_result_raw_pp + ff_column_mcp_prefix_ics_linear_neg_result_raw_pp /\ ((exists mcp_gap_ics_linear_neg_result_raw_pp_column. mcp_gap_ics_linear_neg_result_raw_pp_column + S (ff_column_mcp_prefix_ics_linear_neg_result_raw_pp) = (1)) /\ ((exists ff_left_mcp_cell_ics_linear_neg_result_raw_pp_cell ff_left_scale_mcp_cell_ics_linear_neg_result_raw_pp_cell ff_right_mcp_cell_ics_linear_neg_result_raw_pp_cell ff_right_scale_mcp_cell_ics_linear_neg_result_raw_pp_cell. ((forall ff_index_mcp_ics_linear_neg_result_raw_pp_cell_row ff_source_mcp_ics_linear_neg_result_raw_pp_cell_row ff_target_mcp_ics_linear_neg_result_raw_pp_cell_row. (exists mcp_gap_ics_linear_neg_result_raw_pp_cell_row_bound. mcp_gap_ics_linear_neg_result_raw_pp_cell_row_bound + S (ff_index_mcp_ics_linear_neg_result_raw_pp_cell_row) = (w)) -> (((exists fs_h_mcp_ics_linear_neg_result_raw_pp_cell_row_source. fs_h_mcp_ics_linear_neg_result_raw_pp_cell_row_source + S (ff_source_mcp_ics_linear_neg_result_raw_pp_cell_row) = S ((S (((ff_row_mcp_prefix_ics_linear_neg_result_raw_pp) * (w)) + (1) * ff_index_mcp_ics_linear_neg_result_raw_pp_cell_row)) * ac)) /\ exists fs_q_mcp_ics_linear_neg_result_raw_pp_cell_row_source. ab = fs_q_mcp_ics_linear_neg_result_raw_pp_cell_row_source * S ((S (((ff_row_mcp_prefix_ics_linear_neg_result_raw_pp) * (w)) + (1) * ff_index_mcp_ics_linear_neg_result_raw_pp_cell_row)) * ac) + (ff_source_mcp_ics_linear_neg_result_raw_pp_cell_row))) -> (((exists fs_h_mcp_ics_linear_neg_result_raw_pp_cell_row_target. fs_h_mcp_ics_linear_neg_result_raw_pp_cell_row_target + S (ff_target_mcp_ics_linear_neg_result_raw_pp_cell_row) = S ((S (ff_index_mcp_ics_linear_neg_result_raw_pp_cell_row)) * ff_left_scale_mcp_cell_ics_linear_neg_result_raw_pp_cell)) /\ exists fs_q_mcp_ics_linear_neg_result_raw_pp_cell_row_target. ff_left_mcp_cell_ics_linear_neg_result_raw_pp_cell = fs_q_mcp_ics_linear_neg_result_raw_pp_cell_row_target * S ((S (ff_index_mcp_ics_linear_neg_result_raw_pp_cell_row)) * ff_left_scale_mcp_cell_ics_linear_neg_result_raw_pp_cell) + (ff_target_mcp_ics_linear_neg_result_raw_pp_cell_row))) -> ff_target_mcp_ics_linear_neg_result_raw_pp_cell_row = ff_source_mcp_ics_linear_neg_result_raw_pp_cell_row) /\ ((forall ff_index_mcp_ics_linear_neg_result_raw_pp_cell_column ff_source_mcp_ics_linear_neg_result_raw_pp_cell_column ff_target_mcp_ics_linear_neg_result_raw_pp_cell_column. (exists mcp_gap_ics_linear_neg_result_raw_pp_cell_column_bound. mcp_gap_ics_linear_neg_result_raw_pp_cell_column_bound + S (ff_index_mcp_ics_linear_neg_result_raw_pp_cell_column) = (w)) -> (((exists fs_h_mcp_ics_linear_neg_result_raw_pp_cell_column_source. fs_h_mcp_ics_linear_neg_result_raw_pp_cell_column_source + S (ff_source_mcp_ics_linear_neg_result_raw_pp_cell_column) = S ((S ((ff_column_mcp_prefix_ics_linear_neg_result_raw_pp) + (1) * ff_index_mcp_ics_linear_neg_result_raw_pp_cell_column)) * fc)) /\ exists fs_q_mcp_ics_linear_neg_result_raw_pp_cell_column_source. fb = fs_q_mcp_ics_linear_neg_result_raw_pp_cell_column_source * S ((S ((ff_column_mcp_prefix_ics_linear_neg_result_raw_pp) + (1) * ff_index_mcp_ics_linear_neg_result_raw_pp_cell_column)) * fc) + (ff_source_mcp_ics_linear_neg_result_raw_pp_cell_column))) -> (((exists fs_h_mcp_ics_linear_neg_result_raw_pp_cell_column_target. fs_h_mcp_ics_linear_neg_result_raw_pp_cell_column_target + S (ff_target_mcp_ics_linear_neg_result_raw_pp_cell_column) = S ((S (ff_index_mcp_ics_linear_neg_result_raw_pp_cell_column)) * ff_right_scale_mcp_cell_ics_linear_neg_result_raw_pp_cell)) /\ exists fs_q_mcp_ics_linear_neg_result_raw_pp_cell_column_target. ff_right_mcp_cell_ics_linear_neg_result_raw_pp_cell = fs_q_mcp_ics_linear_neg_result_raw_pp_cell_column_target * S ((S (ff_index_mcp_ics_linear_neg_result_raw_pp_cell_column)) * ff_right_scale_mcp_cell_ics_linear_neg_result_raw_pp_cell) + (ff_target_mcp_ics_linear_neg_result_raw_pp_cell_column))) -> ff_target_mcp_ics_linear_neg_result_raw_pp_cell_column = ff_source_mcp_ics_linear_neg_result_raw_pp_cell_column) /\ (exists ff_code_dot_mcp_ics_linear_neg_result_raw_pp_cell_dot ff_scale_dot_mcp_ics_linear_neg_result_raw_pp_cell_dot. ((forall fpmp_index_dot_mcp_ics_linear_neg_result_raw_pp_cell_dot_pointwise fpmp_left_dot_mcp_ics_linear_neg_result_raw_pp_cell_dot_pointwise fpmp_right_dot_mcp_ics_linear_neg_result_raw_pp_cell_dot_pointwise fpmp_target_dot_mcp_ics_linear_neg_result_raw_pp_cell_dot_pointwise. (exists fpmp_gap_dot_mcp_ics_linear_neg_result_raw_pp_cell_dot_pointwise. fpmp_gap_dot_mcp_ics_linear_neg_result_raw_pp_cell_dot_pointwise + S fpmp_index_dot_mcp_ics_linear_neg_result_raw_pp_cell_dot_pointwise = w) -> (((exists ff_h_fpmp_dot_mcp_ics_linear_neg_result_raw_pp_cell_dot_pointwise_left. ff_h_fpmp_dot_mcp_ics_linear_neg_result_raw_pp_cell_dot_pointwise_left + S (fpmp_left_dot_mcp_ics_linear_neg_result_raw_pp_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_linear_neg_result_raw_pp_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_linear_neg_result_raw_pp_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_linear_neg_result_raw_pp_cell_dot_pointwise_left. ff_left_mcp_cell_ics_linear_neg_result_raw_pp_cell = ff_q_fpmp_dot_mcp_ics_linear_neg_result_raw_pp_cell_dot_pointwise_left * S ((S (fpmp_index_dot_mcp_ics_linear_neg_result_raw_pp_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_linear_neg_result_raw_pp_cell) + (fpmp_left_dot_mcp_ics_linear_neg_result_raw_pp_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_linear_neg_result_raw_pp_cell_dot_pointwise_right. ff_h_fpmp_dot_mcp_ics_linear_neg_result_raw_pp_cell_dot_pointwise_right + S (fpmp_right_dot_mcp_ics_linear_neg_result_raw_pp_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_linear_neg_result_raw_pp_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_linear_neg_result_raw_pp_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_linear_neg_result_raw_pp_cell_dot_pointwise_right. ff_right_mcp_cell_ics_linear_neg_result_raw_pp_cell = ff_q_fpmp_dot_mcp_ics_linear_neg_result_raw_pp_cell_dot_pointwise_right * S ((S (fpmp_index_dot_mcp_ics_linear_neg_result_raw_pp_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_linear_neg_result_raw_pp_cell) + (fpmp_right_dot_mcp_ics_linear_neg_result_raw_pp_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_linear_neg_result_raw_pp_cell_dot_pointwise_target. ff_h_fpmp_dot_mcp_ics_linear_neg_result_raw_pp_cell_dot_pointwise_target + S (fpmp_target_dot_mcp_ics_linear_neg_result_raw_pp_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_linear_neg_result_raw_pp_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_linear_neg_result_raw_pp_cell_dot)) /\ exists ff_q_fpmp_dot_mcp_ics_linear_neg_result_raw_pp_cell_dot_pointwise_target. ff_code_dot_mcp_ics_linear_neg_result_raw_pp_cell_dot = ff_q_fpmp_dot_mcp_ics_linear_neg_result_raw_pp_cell_dot_pointwise_target * S ((S (fpmp_index_dot_mcp_ics_linear_neg_result_raw_pp_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_linear_neg_result_raw_pp_cell_dot) + (fpmp_target_dot_mcp_ics_linear_neg_result_raw_pp_cell_dot_pointwise))) -> fpmp_target_dot_mcp_ics_linear_neg_result_raw_pp_cell_dot_pointwise = fpmp_left_dot_mcp_ics_linear_neg_result_raw_pp_cell_dot_pointwise * fpmp_right_dot_mcp_ics_linear_neg_result_raw_pp_cell_dot_pointwise) /\ (exists ff_u_dot_mcp_ics_linear_neg_result_raw_pp_cell_dot_sum ff_v_dot_mcp_ics_linear_neg_result_raw_pp_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_linear_neg_result_raw_pp_cell_dot_sum_start. ff_h_dot_mcp_ics_linear_neg_result_raw_pp_cell_dot_sum_start + S (0) = S ((S (0)) * ff_v_dot_mcp_ics_linear_neg_result_raw_pp_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_linear_neg_result_raw_pp_cell_dot_sum_start. ff_u_dot_mcp_ics_linear_neg_result_raw_pp_cell_dot_sum = ff_q_dot_mcp_ics_linear_neg_result_raw_pp_cell_dot_sum_start * S ((S (0)) * ff_v_dot_mcp_ics_linear_neg_result_raw_pp_cell_dot_sum) + (0))) /\ ((((exists ff_h_dot_mcp_ics_linear_neg_result_raw_pp_cell_dot_sum_terminal. ff_h_dot_mcp_ics_linear_neg_result_raw_pp_cell_dot_sum_terminal + S (ff_value_mcp_prefix_ics_linear_neg_result_raw_pp) = S ((S (w)) * ff_v_dot_mcp_ics_linear_neg_result_raw_pp_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_linear_neg_result_raw_pp_cell_dot_sum_terminal. ff_u_dot_mcp_ics_linear_neg_result_raw_pp_cell_dot_sum = ff_q_dot_mcp_ics_linear_neg_result_raw_pp_cell_dot_sum_terminal * S ((S (w)) * ff_v_dot_mcp_ics_linear_neg_result_raw_pp_cell_dot_sum) + (ff_value_mcp_prefix_ics_linear_neg_result_raw_pp))) /\ forall ff_i_dot_mcp_ics_linear_neg_result_raw_pp_cell_dot_sum. (exists ff_lt_dot_mcp_ics_linear_neg_result_raw_pp_cell_dot_sum_bound. ff_lt_dot_mcp_ics_linear_neg_result_raw_pp_cell_dot_sum_bound + S ff_i_dot_mcp_ics_linear_neg_result_raw_pp_cell_dot_sum = w) -> exists ff_a_dot_mcp_ics_linear_neg_result_raw_pp_cell_dot_sum ff_r_dot_mcp_ics_linear_neg_result_raw_pp_cell_dot_sum ff_s_dot_mcp_ics_linear_neg_result_raw_pp_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_linear_neg_result_raw_pp_cell_dot_sum_summand. ff_h_dot_mcp_ics_linear_neg_result_raw_pp_cell_dot_sum_summand + S (ff_a_dot_mcp_ics_linear_neg_result_raw_pp_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_linear_neg_result_raw_pp_cell_dot_sum)) * ff_scale_dot_mcp_ics_linear_neg_result_raw_pp_cell_dot)) /\ exists ff_q_dot_mcp_ics_linear_neg_result_raw_pp_cell_dot_sum_summand. ff_code_dot_mcp_ics_linear_neg_result_raw_pp_cell_dot = ff_q_dot_mcp_ics_linear_neg_result_raw_pp_cell_dot_sum_summand * S ((S (ff_i_dot_mcp_ics_linear_neg_result_raw_pp_cell_dot_sum)) * ff_scale_dot_mcp_ics_linear_neg_result_raw_pp_cell_dot) + (ff_a_dot_mcp_ics_linear_neg_result_raw_pp_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_linear_neg_result_raw_pp_cell_dot_sum_partial. ff_h_dot_mcp_ics_linear_neg_result_raw_pp_cell_dot_sum_partial + S (ff_r_dot_mcp_ics_linear_neg_result_raw_pp_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_linear_neg_result_raw_pp_cell_dot_sum)) * ff_v_dot_mcp_ics_linear_neg_result_raw_pp_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_linear_neg_result_raw_pp_cell_dot_sum_partial. ff_u_dot_mcp_ics_linear_neg_result_raw_pp_cell_dot_sum = ff_q_dot_mcp_ics_linear_neg_result_raw_pp_cell_dot_sum_partial * S ((S (ff_i_dot_mcp_ics_linear_neg_result_raw_pp_cell_dot_sum)) * ff_v_dot_mcp_ics_linear_neg_result_raw_pp_cell_dot_sum) + (ff_r_dot_mcp_ics_linear_neg_result_raw_pp_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_linear_neg_result_raw_pp_cell_dot_sum_successor. ff_h_dot_mcp_ics_linear_neg_result_raw_pp_cell_dot_sum_successor + S (ff_s_dot_mcp_ics_linear_neg_result_raw_pp_cell_dot_sum) = S ((S (S ff_i_dot_mcp_ics_linear_neg_result_raw_pp_cell_dot_sum)) * ff_v_dot_mcp_ics_linear_neg_result_raw_pp_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_linear_neg_result_raw_pp_cell_dot_sum_successor. ff_u_dot_mcp_ics_linear_neg_result_raw_pp_cell_dot_sum = ff_q_dot_mcp_ics_linear_neg_result_raw_pp_cell_dot_sum_successor * S ((S (S ff_i_dot_mcp_ics_linear_neg_result_raw_pp_cell_dot_sum)) * ff_v_dot_mcp_ics_linear_neg_result_raw_pp_cell_dot_sum) + (ff_s_dot_mcp_ics_linear_neg_result_raw_pp_cell_dot_sum))) /\ ff_s_dot_mcp_ics_linear_neg_result_raw_pp_cell_dot_sum = ff_r_dot_mcp_ics_linear_neg_result_raw_pp_cell_dot_sum + ff_a_dot_mcp_ics_linear_neg_result_raw_pp_cell_dot_sum))))))))))) /\ (((exists fs_h_mcp_ics_linear_neg_result_raw_pp_entry. fs_h_mcp_ics_linear_neg_result_raw_pp_entry + S (ff_value_mcp_prefix_ics_linear_neg_result_raw_pp) = S ((S (ff_index_mcp_prefix_ics_linear_neg_result_raw_pp)) * ff_pps_mcp_smatrix_ics_linear_neg_result_raw)) /\ exists fs_q_mcp_ics_linear_neg_result_raw_pp_entry. ff_pp_mcp_smatrix_ics_linear_neg_result_raw = fs_q_mcp_ics_linear_neg_result_raw_pp_entry * S ((S (ff_index_mcp_prefix_ics_linear_neg_result_raw_pp)) * ff_pps_mcp_smatrix_ics_linear_neg_result_raw) + (ff_value_mcp_prefix_ics_linear_neg_result_raw_pp))))))) /\ ((forall ff_index_mcp_prefix_ics_linear_neg_result_raw_nn. (exists mcp_gap_ics_linear_neg_result_raw_nn_index. mcp_gap_ics_linear_neg_result_raw_nn_index + S (ff_index_mcp_prefix_ics_linear_neg_result_raw_nn) = ((r) * (1))) -> exists ff_row_mcp_prefix_ics_linear_neg_result_raw_nn ff_column_mcp_prefix_ics_linear_neg_result_raw_nn ff_value_mcp_prefix_ics_linear_neg_result_raw_nn. ((ff_index_mcp_prefix_ics_linear_neg_result_raw_nn) = (1) * ff_row_mcp_prefix_ics_linear_neg_result_raw_nn + ff_column_mcp_prefix_ics_linear_neg_result_raw_nn /\ ((exists mcp_gap_ics_linear_neg_result_raw_nn_column. mcp_gap_ics_linear_neg_result_raw_nn_column + S (ff_column_mcp_prefix_ics_linear_neg_result_raw_nn) = (1)) /\ ((exists ff_left_mcp_cell_ics_linear_neg_result_raw_nn_cell ff_left_scale_mcp_cell_ics_linear_neg_result_raw_nn_cell ff_right_mcp_cell_ics_linear_neg_result_raw_nn_cell ff_right_scale_mcp_cell_ics_linear_neg_result_raw_nn_cell. ((forall ff_index_mcp_ics_linear_neg_result_raw_nn_cell_row ff_source_mcp_ics_linear_neg_result_raw_nn_cell_row ff_target_mcp_ics_linear_neg_result_raw_nn_cell_row. (exists mcp_gap_ics_linear_neg_result_raw_nn_cell_row_bound. mcp_gap_ics_linear_neg_result_raw_nn_cell_row_bound + S (ff_index_mcp_ics_linear_neg_result_raw_nn_cell_row) = (w)) -> (((exists fs_h_mcp_ics_linear_neg_result_raw_nn_cell_row_source. fs_h_mcp_ics_linear_neg_result_raw_nn_cell_row_source + S (ff_source_mcp_ics_linear_neg_result_raw_nn_cell_row) = S ((S (((ff_row_mcp_prefix_ics_linear_neg_result_raw_nn) * (w)) + (1) * ff_index_mcp_ics_linear_neg_result_raw_nn_cell_row)) * dc)) /\ exists fs_q_mcp_ics_linear_neg_result_raw_nn_cell_row_source. db = fs_q_mcp_ics_linear_neg_result_raw_nn_cell_row_source * S ((S (((ff_row_mcp_prefix_ics_linear_neg_result_raw_nn) * (w)) + (1) * ff_index_mcp_ics_linear_neg_result_raw_nn_cell_row)) * dc) + (ff_source_mcp_ics_linear_neg_result_raw_nn_cell_row))) -> (((exists fs_h_mcp_ics_linear_neg_result_raw_nn_cell_row_target. fs_h_mcp_ics_linear_neg_result_raw_nn_cell_row_target + S (ff_target_mcp_ics_linear_neg_result_raw_nn_cell_row) = S ((S (ff_index_mcp_ics_linear_neg_result_raw_nn_cell_row)) * ff_left_scale_mcp_cell_ics_linear_neg_result_raw_nn_cell)) /\ exists fs_q_mcp_ics_linear_neg_result_raw_nn_cell_row_target. ff_left_mcp_cell_ics_linear_neg_result_raw_nn_cell = fs_q_mcp_ics_linear_neg_result_raw_nn_cell_row_target * S ((S (ff_index_mcp_ics_linear_neg_result_raw_nn_cell_row)) * ff_left_scale_mcp_cell_ics_linear_neg_result_raw_nn_cell) + (ff_target_mcp_ics_linear_neg_result_raw_nn_cell_row))) -> ff_target_mcp_ics_linear_neg_result_raw_nn_cell_row = ff_source_mcp_ics_linear_neg_result_raw_nn_cell_row) /\ ((forall ff_index_mcp_ics_linear_neg_result_raw_nn_cell_column ff_source_mcp_ics_linear_neg_result_raw_nn_cell_column ff_target_mcp_ics_linear_neg_result_raw_nn_cell_column. (exists mcp_gap_ics_linear_neg_result_raw_nn_cell_column_bound. mcp_gap_ics_linear_neg_result_raw_nn_cell_column_bound + S (ff_index_mcp_ics_linear_neg_result_raw_nn_cell_column) = (w)) -> (((exists fs_h_mcp_ics_linear_neg_result_raw_nn_cell_column_source. fs_h_mcp_ics_linear_neg_result_raw_nn_cell_column_source + S (ff_source_mcp_ics_linear_neg_result_raw_nn_cell_column) = S ((S ((ff_column_mcp_prefix_ics_linear_neg_result_raw_nn) + (1) * ff_index_mcp_ics_linear_neg_result_raw_nn_cell_column)) * ec)) /\ exists fs_q_mcp_ics_linear_neg_result_raw_nn_cell_column_source. eb = fs_q_mcp_ics_linear_neg_result_raw_nn_cell_column_source * S ((S ((ff_column_mcp_prefix_ics_linear_neg_result_raw_nn) + (1) * ff_index_mcp_ics_linear_neg_result_raw_nn_cell_column)) * ec) + (ff_source_mcp_ics_linear_neg_result_raw_nn_cell_column))) -> (((exists fs_h_mcp_ics_linear_neg_result_raw_nn_cell_column_target. fs_h_mcp_ics_linear_neg_result_raw_nn_cell_column_target + S (ff_target_mcp_ics_linear_neg_result_raw_nn_cell_column) = S ((S (ff_index_mcp_ics_linear_neg_result_raw_nn_cell_column)) * ff_right_scale_mcp_cell_ics_linear_neg_result_raw_nn_cell)) /\ exists fs_q_mcp_ics_linear_neg_result_raw_nn_cell_column_target. ff_right_mcp_cell_ics_linear_neg_result_raw_nn_cell = fs_q_mcp_ics_linear_neg_result_raw_nn_cell_column_target * S ((S (ff_index_mcp_ics_linear_neg_result_raw_nn_cell_column)) * ff_right_scale_mcp_cell_ics_linear_neg_result_raw_nn_cell) + (ff_target_mcp_ics_linear_neg_result_raw_nn_cell_column))) -> ff_target_mcp_ics_linear_neg_result_raw_nn_cell_column = ff_source_mcp_ics_linear_neg_result_raw_nn_cell_column) /\ (exists ff_code_dot_mcp_ics_linear_neg_result_raw_nn_cell_dot ff_scale_dot_mcp_ics_linear_neg_result_raw_nn_cell_dot. ((forall fpmp_index_dot_mcp_ics_linear_neg_result_raw_nn_cell_dot_pointwise fpmp_left_dot_mcp_ics_linear_neg_result_raw_nn_cell_dot_pointwise fpmp_right_dot_mcp_ics_linear_neg_result_raw_nn_cell_dot_pointwise fpmp_target_dot_mcp_ics_linear_neg_result_raw_nn_cell_dot_pointwise. (exists fpmp_gap_dot_mcp_ics_linear_neg_result_raw_nn_cell_dot_pointwise. fpmp_gap_dot_mcp_ics_linear_neg_result_raw_nn_cell_dot_pointwise + S fpmp_index_dot_mcp_ics_linear_neg_result_raw_nn_cell_dot_pointwise = w) -> (((exists ff_h_fpmp_dot_mcp_ics_linear_neg_result_raw_nn_cell_dot_pointwise_left. ff_h_fpmp_dot_mcp_ics_linear_neg_result_raw_nn_cell_dot_pointwise_left + S (fpmp_left_dot_mcp_ics_linear_neg_result_raw_nn_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_linear_neg_result_raw_nn_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_linear_neg_result_raw_nn_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_linear_neg_result_raw_nn_cell_dot_pointwise_left. ff_left_mcp_cell_ics_linear_neg_result_raw_nn_cell = ff_q_fpmp_dot_mcp_ics_linear_neg_result_raw_nn_cell_dot_pointwise_left * S ((S (fpmp_index_dot_mcp_ics_linear_neg_result_raw_nn_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_linear_neg_result_raw_nn_cell) + (fpmp_left_dot_mcp_ics_linear_neg_result_raw_nn_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_linear_neg_result_raw_nn_cell_dot_pointwise_right. ff_h_fpmp_dot_mcp_ics_linear_neg_result_raw_nn_cell_dot_pointwise_right + S (fpmp_right_dot_mcp_ics_linear_neg_result_raw_nn_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_linear_neg_result_raw_nn_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_linear_neg_result_raw_nn_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_linear_neg_result_raw_nn_cell_dot_pointwise_right. ff_right_mcp_cell_ics_linear_neg_result_raw_nn_cell = ff_q_fpmp_dot_mcp_ics_linear_neg_result_raw_nn_cell_dot_pointwise_right * S ((S (fpmp_index_dot_mcp_ics_linear_neg_result_raw_nn_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_linear_neg_result_raw_nn_cell) + (fpmp_right_dot_mcp_ics_linear_neg_result_raw_nn_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_linear_neg_result_raw_nn_cell_dot_pointwise_target. ff_h_fpmp_dot_mcp_ics_linear_neg_result_raw_nn_cell_dot_pointwise_target + S (fpmp_target_dot_mcp_ics_linear_neg_result_raw_nn_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_linear_neg_result_raw_nn_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_linear_neg_result_raw_nn_cell_dot)) /\ exists ff_q_fpmp_dot_mcp_ics_linear_neg_result_raw_nn_cell_dot_pointwise_target. ff_code_dot_mcp_ics_linear_neg_result_raw_nn_cell_dot = ff_q_fpmp_dot_mcp_ics_linear_neg_result_raw_nn_cell_dot_pointwise_target * S ((S (fpmp_index_dot_mcp_ics_linear_neg_result_raw_nn_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_linear_neg_result_raw_nn_cell_dot) + (fpmp_target_dot_mcp_ics_linear_neg_result_raw_nn_cell_dot_pointwise))) -> fpmp_target_dot_mcp_ics_linear_neg_result_raw_nn_cell_dot_pointwise = fpmp_left_dot_mcp_ics_linear_neg_result_raw_nn_cell_dot_pointwise * fpmp_right_dot_mcp_ics_linear_neg_result_raw_nn_cell_dot_pointwise) /\ (exists ff_u_dot_mcp_ics_linear_neg_result_raw_nn_cell_dot_sum ff_v_dot_mcp_ics_linear_neg_result_raw_nn_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_linear_neg_result_raw_nn_cell_dot_sum_start. ff_h_dot_mcp_ics_linear_neg_result_raw_nn_cell_dot_sum_start + S (0) = S ((S (0)) * ff_v_dot_mcp_ics_linear_neg_result_raw_nn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_linear_neg_result_raw_nn_cell_dot_sum_start. ff_u_dot_mcp_ics_linear_neg_result_raw_nn_cell_dot_sum = ff_q_dot_mcp_ics_linear_neg_result_raw_nn_cell_dot_sum_start * S ((S (0)) * ff_v_dot_mcp_ics_linear_neg_result_raw_nn_cell_dot_sum) + (0))) /\ ((((exists ff_h_dot_mcp_ics_linear_neg_result_raw_nn_cell_dot_sum_terminal. ff_h_dot_mcp_ics_linear_neg_result_raw_nn_cell_dot_sum_terminal + S (ff_value_mcp_prefix_ics_linear_neg_result_raw_nn) = S ((S (w)) * ff_v_dot_mcp_ics_linear_neg_result_raw_nn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_linear_neg_result_raw_nn_cell_dot_sum_terminal. ff_u_dot_mcp_ics_linear_neg_result_raw_nn_cell_dot_sum = ff_q_dot_mcp_ics_linear_neg_result_raw_nn_cell_dot_sum_terminal * S ((S (w)) * ff_v_dot_mcp_ics_linear_neg_result_raw_nn_cell_dot_sum) + (ff_value_mcp_prefix_ics_linear_neg_result_raw_nn))) /\ forall ff_i_dot_mcp_ics_linear_neg_result_raw_nn_cell_dot_sum. (exists ff_lt_dot_mcp_ics_linear_neg_result_raw_nn_cell_dot_sum_bound. ff_lt_dot_mcp_ics_linear_neg_result_raw_nn_cell_dot_sum_bound + S ff_i_dot_mcp_ics_linear_neg_result_raw_nn_cell_dot_sum = w) -> exists ff_a_dot_mcp_ics_linear_neg_result_raw_nn_cell_dot_sum ff_r_dot_mcp_ics_linear_neg_result_raw_nn_cell_dot_sum ff_s_dot_mcp_ics_linear_neg_result_raw_nn_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_linear_neg_result_raw_nn_cell_dot_sum_summand. ff_h_dot_mcp_ics_linear_neg_result_raw_nn_cell_dot_sum_summand + S (ff_a_dot_mcp_ics_linear_neg_result_raw_nn_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_linear_neg_result_raw_nn_cell_dot_sum)) * ff_scale_dot_mcp_ics_linear_neg_result_raw_nn_cell_dot)) /\ exists ff_q_dot_mcp_ics_linear_neg_result_raw_nn_cell_dot_sum_summand. ff_code_dot_mcp_ics_linear_neg_result_raw_nn_cell_dot = ff_q_dot_mcp_ics_linear_neg_result_raw_nn_cell_dot_sum_summand * S ((S (ff_i_dot_mcp_ics_linear_neg_result_raw_nn_cell_dot_sum)) * ff_scale_dot_mcp_ics_linear_neg_result_raw_nn_cell_dot) + (ff_a_dot_mcp_ics_linear_neg_result_raw_nn_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_linear_neg_result_raw_nn_cell_dot_sum_partial. ff_h_dot_mcp_ics_linear_neg_result_raw_nn_cell_dot_sum_partial + S (ff_r_dot_mcp_ics_linear_neg_result_raw_nn_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_linear_neg_result_raw_nn_cell_dot_sum)) * ff_v_dot_mcp_ics_linear_neg_result_raw_nn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_linear_neg_result_raw_nn_cell_dot_sum_partial. ff_u_dot_mcp_ics_linear_neg_result_raw_nn_cell_dot_sum = ff_q_dot_mcp_ics_linear_neg_result_raw_nn_cell_dot_sum_partial * S ((S (ff_i_dot_mcp_ics_linear_neg_result_raw_nn_cell_dot_sum)) * ff_v_dot_mcp_ics_linear_neg_result_raw_nn_cell_dot_sum) + (ff_r_dot_mcp_ics_linear_neg_result_raw_nn_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_linear_neg_result_raw_nn_cell_dot_sum_successor. ff_h_dot_mcp_ics_linear_neg_result_raw_nn_cell_dot_sum_successor + S (ff_s_dot_mcp_ics_linear_neg_result_raw_nn_cell_dot_sum) = S ((S (S ff_i_dot_mcp_ics_linear_neg_result_raw_nn_cell_dot_sum)) * ff_v_dot_mcp_ics_linear_neg_result_raw_nn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_linear_neg_result_raw_nn_cell_dot_sum_successor. ff_u_dot_mcp_ics_linear_neg_result_raw_nn_cell_dot_sum = ff_q_dot_mcp_ics_linear_neg_result_raw_nn_cell_dot_sum_successor * S ((S (S ff_i_dot_mcp_ics_linear_neg_result_raw_nn_cell_dot_sum)) * ff_v_dot_mcp_ics_linear_neg_result_raw_nn_cell_dot_sum) + (ff_s_dot_mcp_ics_linear_neg_result_raw_nn_cell_dot_sum))) /\ ff_s_dot_mcp_ics_linear_neg_result_raw_nn_cell_dot_sum = ff_r_dot_mcp_ics_linear_neg_result_raw_nn_cell_dot_sum + ff_a_dot_mcp_ics_linear_neg_result_raw_nn_cell_dot_sum))))))))))) /\ (((exists fs_h_mcp_ics_linear_neg_result_raw_nn_entry. fs_h_mcp_ics_linear_neg_result_raw_nn_entry + S (ff_value_mcp_prefix_ics_linear_neg_result_raw_nn) = S ((S (ff_index_mcp_prefix_ics_linear_neg_result_raw_nn)) * ff_nns_mcp_smatrix_ics_linear_neg_result_raw)) /\ exists fs_q_mcp_ics_linear_neg_result_raw_nn_entry. ff_nn_mcp_smatrix_ics_linear_neg_result_raw = fs_q_mcp_ics_linear_neg_result_raw_nn_entry * S ((S (ff_index_mcp_prefix_ics_linear_neg_result_raw_nn)) * ff_nns_mcp_smatrix_ics_linear_neg_result_raw) + (ff_value_mcp_prefix_ics_linear_neg_result_raw_nn))))))) /\ ((forall ff_index_mcp_prefix_ics_linear_neg_result_raw_pn. (exists mcp_gap_ics_linear_neg_result_raw_pn_index. mcp_gap_ics_linear_neg_result_raw_pn_index + S (ff_index_mcp_prefix_ics_linear_neg_result_raw_pn) = ((r) * (1))) -> exists ff_row_mcp_prefix_ics_linear_neg_result_raw_pn ff_column_mcp_prefix_ics_linear_neg_result_raw_pn ff_value_mcp_prefix_ics_linear_neg_result_raw_pn. ((ff_index_mcp_prefix_ics_linear_neg_result_raw_pn) = (1) * ff_row_mcp_prefix_ics_linear_neg_result_raw_pn + ff_column_mcp_prefix_ics_linear_neg_result_raw_pn /\ ((exists mcp_gap_ics_linear_neg_result_raw_pn_column. mcp_gap_ics_linear_neg_result_raw_pn_column + S (ff_column_mcp_prefix_ics_linear_neg_result_raw_pn) = (1)) /\ ((exists ff_left_mcp_cell_ics_linear_neg_result_raw_pn_cell ff_left_scale_mcp_cell_ics_linear_neg_result_raw_pn_cell ff_right_mcp_cell_ics_linear_neg_result_raw_pn_cell ff_right_scale_mcp_cell_ics_linear_neg_result_raw_pn_cell. ((forall ff_index_mcp_ics_linear_neg_result_raw_pn_cell_row ff_source_mcp_ics_linear_neg_result_raw_pn_cell_row ff_target_mcp_ics_linear_neg_result_raw_pn_cell_row. (exists mcp_gap_ics_linear_neg_result_raw_pn_cell_row_bound. mcp_gap_ics_linear_neg_result_raw_pn_cell_row_bound + S (ff_index_mcp_ics_linear_neg_result_raw_pn_cell_row) = (w)) -> (((exists fs_h_mcp_ics_linear_neg_result_raw_pn_cell_row_source. fs_h_mcp_ics_linear_neg_result_raw_pn_cell_row_source + S (ff_source_mcp_ics_linear_neg_result_raw_pn_cell_row) = S ((S (((ff_row_mcp_prefix_ics_linear_neg_result_raw_pn) * (w)) + (1) * ff_index_mcp_ics_linear_neg_result_raw_pn_cell_row)) * ac)) /\ exists fs_q_mcp_ics_linear_neg_result_raw_pn_cell_row_source. ab = fs_q_mcp_ics_linear_neg_result_raw_pn_cell_row_source * S ((S (((ff_row_mcp_prefix_ics_linear_neg_result_raw_pn) * (w)) + (1) * ff_index_mcp_ics_linear_neg_result_raw_pn_cell_row)) * ac) + (ff_source_mcp_ics_linear_neg_result_raw_pn_cell_row))) -> (((exists fs_h_mcp_ics_linear_neg_result_raw_pn_cell_row_target. fs_h_mcp_ics_linear_neg_result_raw_pn_cell_row_target + S (ff_target_mcp_ics_linear_neg_result_raw_pn_cell_row) = S ((S (ff_index_mcp_ics_linear_neg_result_raw_pn_cell_row)) * ff_left_scale_mcp_cell_ics_linear_neg_result_raw_pn_cell)) /\ exists fs_q_mcp_ics_linear_neg_result_raw_pn_cell_row_target. ff_left_mcp_cell_ics_linear_neg_result_raw_pn_cell = fs_q_mcp_ics_linear_neg_result_raw_pn_cell_row_target * S ((S (ff_index_mcp_ics_linear_neg_result_raw_pn_cell_row)) * ff_left_scale_mcp_cell_ics_linear_neg_result_raw_pn_cell) + (ff_target_mcp_ics_linear_neg_result_raw_pn_cell_row))) -> ff_target_mcp_ics_linear_neg_result_raw_pn_cell_row = ff_source_mcp_ics_linear_neg_result_raw_pn_cell_row) /\ ((forall ff_index_mcp_ics_linear_neg_result_raw_pn_cell_column ff_source_mcp_ics_linear_neg_result_raw_pn_cell_column ff_target_mcp_ics_linear_neg_result_raw_pn_cell_column. (exists mcp_gap_ics_linear_neg_result_raw_pn_cell_column_bound. mcp_gap_ics_linear_neg_result_raw_pn_cell_column_bound + S (ff_index_mcp_ics_linear_neg_result_raw_pn_cell_column) = (w)) -> (((exists fs_h_mcp_ics_linear_neg_result_raw_pn_cell_column_source. fs_h_mcp_ics_linear_neg_result_raw_pn_cell_column_source + S (ff_source_mcp_ics_linear_neg_result_raw_pn_cell_column) = S ((S ((ff_column_mcp_prefix_ics_linear_neg_result_raw_pn) + (1) * ff_index_mcp_ics_linear_neg_result_raw_pn_cell_column)) * ec)) /\ exists fs_q_mcp_ics_linear_neg_result_raw_pn_cell_column_source. eb = fs_q_mcp_ics_linear_neg_result_raw_pn_cell_column_source * S ((S ((ff_column_mcp_prefix_ics_linear_neg_result_raw_pn) + (1) * ff_index_mcp_ics_linear_neg_result_raw_pn_cell_column)) * ec) + (ff_source_mcp_ics_linear_neg_result_raw_pn_cell_column))) -> (((exists fs_h_mcp_ics_linear_neg_result_raw_pn_cell_column_target. fs_h_mcp_ics_linear_neg_result_raw_pn_cell_column_target + S (ff_target_mcp_ics_linear_neg_result_raw_pn_cell_column) = S ((S (ff_index_mcp_ics_linear_neg_result_raw_pn_cell_column)) * ff_right_scale_mcp_cell_ics_linear_neg_result_raw_pn_cell)) /\ exists fs_q_mcp_ics_linear_neg_result_raw_pn_cell_column_target. ff_right_mcp_cell_ics_linear_neg_result_raw_pn_cell = fs_q_mcp_ics_linear_neg_result_raw_pn_cell_column_target * S ((S (ff_index_mcp_ics_linear_neg_result_raw_pn_cell_column)) * ff_right_scale_mcp_cell_ics_linear_neg_result_raw_pn_cell) + (ff_target_mcp_ics_linear_neg_result_raw_pn_cell_column))) -> ff_target_mcp_ics_linear_neg_result_raw_pn_cell_column = ff_source_mcp_ics_linear_neg_result_raw_pn_cell_column) /\ (exists ff_code_dot_mcp_ics_linear_neg_result_raw_pn_cell_dot ff_scale_dot_mcp_ics_linear_neg_result_raw_pn_cell_dot. ((forall fpmp_index_dot_mcp_ics_linear_neg_result_raw_pn_cell_dot_pointwise fpmp_left_dot_mcp_ics_linear_neg_result_raw_pn_cell_dot_pointwise fpmp_right_dot_mcp_ics_linear_neg_result_raw_pn_cell_dot_pointwise fpmp_target_dot_mcp_ics_linear_neg_result_raw_pn_cell_dot_pointwise. (exists fpmp_gap_dot_mcp_ics_linear_neg_result_raw_pn_cell_dot_pointwise. fpmp_gap_dot_mcp_ics_linear_neg_result_raw_pn_cell_dot_pointwise + S fpmp_index_dot_mcp_ics_linear_neg_result_raw_pn_cell_dot_pointwise = w) -> (((exists ff_h_fpmp_dot_mcp_ics_linear_neg_result_raw_pn_cell_dot_pointwise_left. ff_h_fpmp_dot_mcp_ics_linear_neg_result_raw_pn_cell_dot_pointwise_left + S (fpmp_left_dot_mcp_ics_linear_neg_result_raw_pn_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_linear_neg_result_raw_pn_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_linear_neg_result_raw_pn_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_linear_neg_result_raw_pn_cell_dot_pointwise_left. ff_left_mcp_cell_ics_linear_neg_result_raw_pn_cell = ff_q_fpmp_dot_mcp_ics_linear_neg_result_raw_pn_cell_dot_pointwise_left * S ((S (fpmp_index_dot_mcp_ics_linear_neg_result_raw_pn_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_linear_neg_result_raw_pn_cell) + (fpmp_left_dot_mcp_ics_linear_neg_result_raw_pn_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_linear_neg_result_raw_pn_cell_dot_pointwise_right. ff_h_fpmp_dot_mcp_ics_linear_neg_result_raw_pn_cell_dot_pointwise_right + S (fpmp_right_dot_mcp_ics_linear_neg_result_raw_pn_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_linear_neg_result_raw_pn_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_linear_neg_result_raw_pn_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_linear_neg_result_raw_pn_cell_dot_pointwise_right. ff_right_mcp_cell_ics_linear_neg_result_raw_pn_cell = ff_q_fpmp_dot_mcp_ics_linear_neg_result_raw_pn_cell_dot_pointwise_right * S ((S (fpmp_index_dot_mcp_ics_linear_neg_result_raw_pn_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_linear_neg_result_raw_pn_cell) + (fpmp_right_dot_mcp_ics_linear_neg_result_raw_pn_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_linear_neg_result_raw_pn_cell_dot_pointwise_target. ff_h_fpmp_dot_mcp_ics_linear_neg_result_raw_pn_cell_dot_pointwise_target + S (fpmp_target_dot_mcp_ics_linear_neg_result_raw_pn_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_linear_neg_result_raw_pn_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_linear_neg_result_raw_pn_cell_dot)) /\ exists ff_q_fpmp_dot_mcp_ics_linear_neg_result_raw_pn_cell_dot_pointwise_target. ff_code_dot_mcp_ics_linear_neg_result_raw_pn_cell_dot = ff_q_fpmp_dot_mcp_ics_linear_neg_result_raw_pn_cell_dot_pointwise_target * S ((S (fpmp_index_dot_mcp_ics_linear_neg_result_raw_pn_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_linear_neg_result_raw_pn_cell_dot) + (fpmp_target_dot_mcp_ics_linear_neg_result_raw_pn_cell_dot_pointwise))) -> fpmp_target_dot_mcp_ics_linear_neg_result_raw_pn_cell_dot_pointwise = fpmp_left_dot_mcp_ics_linear_neg_result_raw_pn_cell_dot_pointwise * fpmp_right_dot_mcp_ics_linear_neg_result_raw_pn_cell_dot_pointwise) /\ (exists ff_u_dot_mcp_ics_linear_neg_result_raw_pn_cell_dot_sum ff_v_dot_mcp_ics_linear_neg_result_raw_pn_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_linear_neg_result_raw_pn_cell_dot_sum_start. ff_h_dot_mcp_ics_linear_neg_result_raw_pn_cell_dot_sum_start + S (0) = S ((S (0)) * ff_v_dot_mcp_ics_linear_neg_result_raw_pn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_linear_neg_result_raw_pn_cell_dot_sum_start. ff_u_dot_mcp_ics_linear_neg_result_raw_pn_cell_dot_sum = ff_q_dot_mcp_ics_linear_neg_result_raw_pn_cell_dot_sum_start * S ((S (0)) * ff_v_dot_mcp_ics_linear_neg_result_raw_pn_cell_dot_sum) + (0))) /\ ((((exists ff_h_dot_mcp_ics_linear_neg_result_raw_pn_cell_dot_sum_terminal. ff_h_dot_mcp_ics_linear_neg_result_raw_pn_cell_dot_sum_terminal + S (ff_value_mcp_prefix_ics_linear_neg_result_raw_pn) = S ((S (w)) * ff_v_dot_mcp_ics_linear_neg_result_raw_pn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_linear_neg_result_raw_pn_cell_dot_sum_terminal. ff_u_dot_mcp_ics_linear_neg_result_raw_pn_cell_dot_sum = ff_q_dot_mcp_ics_linear_neg_result_raw_pn_cell_dot_sum_terminal * S ((S (w)) * ff_v_dot_mcp_ics_linear_neg_result_raw_pn_cell_dot_sum) + (ff_value_mcp_prefix_ics_linear_neg_result_raw_pn))) /\ forall ff_i_dot_mcp_ics_linear_neg_result_raw_pn_cell_dot_sum. (exists ff_lt_dot_mcp_ics_linear_neg_result_raw_pn_cell_dot_sum_bound. ff_lt_dot_mcp_ics_linear_neg_result_raw_pn_cell_dot_sum_bound + S ff_i_dot_mcp_ics_linear_neg_result_raw_pn_cell_dot_sum = w) -> exists ff_a_dot_mcp_ics_linear_neg_result_raw_pn_cell_dot_sum ff_r_dot_mcp_ics_linear_neg_result_raw_pn_cell_dot_sum ff_s_dot_mcp_ics_linear_neg_result_raw_pn_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_linear_neg_result_raw_pn_cell_dot_sum_summand. ff_h_dot_mcp_ics_linear_neg_result_raw_pn_cell_dot_sum_summand + S (ff_a_dot_mcp_ics_linear_neg_result_raw_pn_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_linear_neg_result_raw_pn_cell_dot_sum)) * ff_scale_dot_mcp_ics_linear_neg_result_raw_pn_cell_dot)) /\ exists ff_q_dot_mcp_ics_linear_neg_result_raw_pn_cell_dot_sum_summand. ff_code_dot_mcp_ics_linear_neg_result_raw_pn_cell_dot = ff_q_dot_mcp_ics_linear_neg_result_raw_pn_cell_dot_sum_summand * S ((S (ff_i_dot_mcp_ics_linear_neg_result_raw_pn_cell_dot_sum)) * ff_scale_dot_mcp_ics_linear_neg_result_raw_pn_cell_dot) + (ff_a_dot_mcp_ics_linear_neg_result_raw_pn_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_linear_neg_result_raw_pn_cell_dot_sum_partial. ff_h_dot_mcp_ics_linear_neg_result_raw_pn_cell_dot_sum_partial + S (ff_r_dot_mcp_ics_linear_neg_result_raw_pn_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_linear_neg_result_raw_pn_cell_dot_sum)) * ff_v_dot_mcp_ics_linear_neg_result_raw_pn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_linear_neg_result_raw_pn_cell_dot_sum_partial. ff_u_dot_mcp_ics_linear_neg_result_raw_pn_cell_dot_sum = ff_q_dot_mcp_ics_linear_neg_result_raw_pn_cell_dot_sum_partial * S ((S (ff_i_dot_mcp_ics_linear_neg_result_raw_pn_cell_dot_sum)) * ff_v_dot_mcp_ics_linear_neg_result_raw_pn_cell_dot_sum) + (ff_r_dot_mcp_ics_linear_neg_result_raw_pn_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_linear_neg_result_raw_pn_cell_dot_sum_successor. ff_h_dot_mcp_ics_linear_neg_result_raw_pn_cell_dot_sum_successor + S (ff_s_dot_mcp_ics_linear_neg_result_raw_pn_cell_dot_sum) = S ((S (S ff_i_dot_mcp_ics_linear_neg_result_raw_pn_cell_dot_sum)) * ff_v_dot_mcp_ics_linear_neg_result_raw_pn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_linear_neg_result_raw_pn_cell_dot_sum_successor. ff_u_dot_mcp_ics_linear_neg_result_raw_pn_cell_dot_sum = ff_q_dot_mcp_ics_linear_neg_result_raw_pn_cell_dot_sum_successor * S ((S (S ff_i_dot_mcp_ics_linear_neg_result_raw_pn_cell_dot_sum)) * ff_v_dot_mcp_ics_linear_neg_result_raw_pn_cell_dot_sum) + (ff_s_dot_mcp_ics_linear_neg_result_raw_pn_cell_dot_sum))) /\ ff_s_dot_mcp_ics_linear_neg_result_raw_pn_cell_dot_sum = ff_r_dot_mcp_ics_linear_neg_result_raw_pn_cell_dot_sum + ff_a_dot_mcp_ics_linear_neg_result_raw_pn_cell_dot_sum))))))))))) /\ (((exists fs_h_mcp_ics_linear_neg_result_raw_pn_entry. fs_h_mcp_ics_linear_neg_result_raw_pn_entry + S (ff_value_mcp_prefix_ics_linear_neg_result_raw_pn) = S ((S (ff_index_mcp_prefix_ics_linear_neg_result_raw_pn)) * ff_pns_mcp_smatrix_ics_linear_neg_result_raw)) /\ exists fs_q_mcp_ics_linear_neg_result_raw_pn_entry. ff_pn_mcp_smatrix_ics_linear_neg_result_raw = fs_q_mcp_ics_linear_neg_result_raw_pn_entry * S ((S (ff_index_mcp_prefix_ics_linear_neg_result_raw_pn)) * ff_pns_mcp_smatrix_ics_linear_neg_result_raw) + (ff_value_mcp_prefix_ics_linear_neg_result_raw_pn))))))) /\ ((forall ff_index_mcp_prefix_ics_linear_neg_result_raw_np. (exists mcp_gap_ics_linear_neg_result_raw_np_index. mcp_gap_ics_linear_neg_result_raw_np_index + S (ff_index_mcp_prefix_ics_linear_neg_result_raw_np) = ((r) * (1))) -> exists ff_row_mcp_prefix_ics_linear_neg_result_raw_np ff_column_mcp_prefix_ics_linear_neg_result_raw_np ff_value_mcp_prefix_ics_linear_neg_result_raw_np. ((ff_index_mcp_prefix_ics_linear_neg_result_raw_np) = (1) * ff_row_mcp_prefix_ics_linear_neg_result_raw_np + ff_column_mcp_prefix_ics_linear_neg_result_raw_np /\ ((exists mcp_gap_ics_linear_neg_result_raw_np_column. mcp_gap_ics_linear_neg_result_raw_np_column + S (ff_column_mcp_prefix_ics_linear_neg_result_raw_np) = (1)) /\ ((exists ff_left_mcp_cell_ics_linear_neg_result_raw_np_cell ff_left_scale_mcp_cell_ics_linear_neg_result_raw_np_cell ff_right_mcp_cell_ics_linear_neg_result_raw_np_cell ff_right_scale_mcp_cell_ics_linear_neg_result_raw_np_cell. ((forall ff_index_mcp_ics_linear_neg_result_raw_np_cell_row ff_source_mcp_ics_linear_neg_result_raw_np_cell_row ff_target_mcp_ics_linear_neg_result_raw_np_cell_row. (exists mcp_gap_ics_linear_neg_result_raw_np_cell_row_bound. mcp_gap_ics_linear_neg_result_raw_np_cell_row_bound + S (ff_index_mcp_ics_linear_neg_result_raw_np_cell_row) = (w)) -> (((exists fs_h_mcp_ics_linear_neg_result_raw_np_cell_row_source. fs_h_mcp_ics_linear_neg_result_raw_np_cell_row_source + S (ff_source_mcp_ics_linear_neg_result_raw_np_cell_row) = S ((S (((ff_row_mcp_prefix_ics_linear_neg_result_raw_np) * (w)) + (1) * ff_index_mcp_ics_linear_neg_result_raw_np_cell_row)) * dc)) /\ exists fs_q_mcp_ics_linear_neg_result_raw_np_cell_row_source. db = fs_q_mcp_ics_linear_neg_result_raw_np_cell_row_source * S ((S (((ff_row_mcp_prefix_ics_linear_neg_result_raw_np) * (w)) + (1) * ff_index_mcp_ics_linear_neg_result_raw_np_cell_row)) * dc) + (ff_source_mcp_ics_linear_neg_result_raw_np_cell_row))) -> (((exists fs_h_mcp_ics_linear_neg_result_raw_np_cell_row_target. fs_h_mcp_ics_linear_neg_result_raw_np_cell_row_target + S (ff_target_mcp_ics_linear_neg_result_raw_np_cell_row) = S ((S (ff_index_mcp_ics_linear_neg_result_raw_np_cell_row)) * ff_left_scale_mcp_cell_ics_linear_neg_result_raw_np_cell)) /\ exists fs_q_mcp_ics_linear_neg_result_raw_np_cell_row_target. ff_left_mcp_cell_ics_linear_neg_result_raw_np_cell = fs_q_mcp_ics_linear_neg_result_raw_np_cell_row_target * S ((S (ff_index_mcp_ics_linear_neg_result_raw_np_cell_row)) * ff_left_scale_mcp_cell_ics_linear_neg_result_raw_np_cell) + (ff_target_mcp_ics_linear_neg_result_raw_np_cell_row))) -> ff_target_mcp_ics_linear_neg_result_raw_np_cell_row = ff_source_mcp_ics_linear_neg_result_raw_np_cell_row) /\ ((forall ff_index_mcp_ics_linear_neg_result_raw_np_cell_column ff_source_mcp_ics_linear_neg_result_raw_np_cell_column ff_target_mcp_ics_linear_neg_result_raw_np_cell_column. (exists mcp_gap_ics_linear_neg_result_raw_np_cell_column_bound. mcp_gap_ics_linear_neg_result_raw_np_cell_column_bound + S (ff_index_mcp_ics_linear_neg_result_raw_np_cell_column) = (w)) -> (((exists fs_h_mcp_ics_linear_neg_result_raw_np_cell_column_source. fs_h_mcp_ics_linear_neg_result_raw_np_cell_column_source + S (ff_source_mcp_ics_linear_neg_result_raw_np_cell_column) = S ((S ((ff_column_mcp_prefix_ics_linear_neg_result_raw_np) + (1) * ff_index_mcp_ics_linear_neg_result_raw_np_cell_column)) * fc)) /\ exists fs_q_mcp_ics_linear_neg_result_raw_np_cell_column_source. fb = fs_q_mcp_ics_linear_neg_result_raw_np_cell_column_source * S ((S ((ff_column_mcp_prefix_ics_linear_neg_result_raw_np) + (1) * ff_index_mcp_ics_linear_neg_result_raw_np_cell_column)) * fc) + (ff_source_mcp_ics_linear_neg_result_raw_np_cell_column))) -> (((exists fs_h_mcp_ics_linear_neg_result_raw_np_cell_column_target. fs_h_mcp_ics_linear_neg_result_raw_np_cell_column_target + S (ff_target_mcp_ics_linear_neg_result_raw_np_cell_column) = S ((S (ff_index_mcp_ics_linear_neg_result_raw_np_cell_column)) * ff_right_scale_mcp_cell_ics_linear_neg_result_raw_np_cell)) /\ exists fs_q_mcp_ics_linear_neg_result_raw_np_cell_column_target. ff_right_mcp_cell_ics_linear_neg_result_raw_np_cell = fs_q_mcp_ics_linear_neg_result_raw_np_cell_column_target * S ((S (ff_index_mcp_ics_linear_neg_result_raw_np_cell_column)) * ff_right_scale_mcp_cell_ics_linear_neg_result_raw_np_cell) + (ff_target_mcp_ics_linear_neg_result_raw_np_cell_column))) -> ff_target_mcp_ics_linear_neg_result_raw_np_cell_column = ff_source_mcp_ics_linear_neg_result_raw_np_cell_column) /\ (exists ff_code_dot_mcp_ics_linear_neg_result_raw_np_cell_dot ff_scale_dot_mcp_ics_linear_neg_result_raw_np_cell_dot. ((forall fpmp_index_dot_mcp_ics_linear_neg_result_raw_np_cell_dot_pointwise fpmp_left_dot_mcp_ics_linear_neg_result_raw_np_cell_dot_pointwise fpmp_right_dot_mcp_ics_linear_neg_result_raw_np_cell_dot_pointwise fpmp_target_dot_mcp_ics_linear_neg_result_raw_np_cell_dot_pointwise. (exists fpmp_gap_dot_mcp_ics_linear_neg_result_raw_np_cell_dot_pointwise. fpmp_gap_dot_mcp_ics_linear_neg_result_raw_np_cell_dot_pointwise + S fpmp_index_dot_mcp_ics_linear_neg_result_raw_np_cell_dot_pointwise = w) -> (((exists ff_h_fpmp_dot_mcp_ics_linear_neg_result_raw_np_cell_dot_pointwise_left. ff_h_fpmp_dot_mcp_ics_linear_neg_result_raw_np_cell_dot_pointwise_left + S (fpmp_left_dot_mcp_ics_linear_neg_result_raw_np_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_linear_neg_result_raw_np_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_linear_neg_result_raw_np_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_linear_neg_result_raw_np_cell_dot_pointwise_left. ff_left_mcp_cell_ics_linear_neg_result_raw_np_cell = ff_q_fpmp_dot_mcp_ics_linear_neg_result_raw_np_cell_dot_pointwise_left * S ((S (fpmp_index_dot_mcp_ics_linear_neg_result_raw_np_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_linear_neg_result_raw_np_cell) + (fpmp_left_dot_mcp_ics_linear_neg_result_raw_np_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_linear_neg_result_raw_np_cell_dot_pointwise_right. ff_h_fpmp_dot_mcp_ics_linear_neg_result_raw_np_cell_dot_pointwise_right + S (fpmp_right_dot_mcp_ics_linear_neg_result_raw_np_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_linear_neg_result_raw_np_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_linear_neg_result_raw_np_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_linear_neg_result_raw_np_cell_dot_pointwise_right. ff_right_mcp_cell_ics_linear_neg_result_raw_np_cell = ff_q_fpmp_dot_mcp_ics_linear_neg_result_raw_np_cell_dot_pointwise_right * S ((S (fpmp_index_dot_mcp_ics_linear_neg_result_raw_np_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_linear_neg_result_raw_np_cell) + (fpmp_right_dot_mcp_ics_linear_neg_result_raw_np_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_linear_neg_result_raw_np_cell_dot_pointwise_target. ff_h_fpmp_dot_mcp_ics_linear_neg_result_raw_np_cell_dot_pointwise_target + S (fpmp_target_dot_mcp_ics_linear_neg_result_raw_np_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_linear_neg_result_raw_np_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_linear_neg_result_raw_np_cell_dot)) /\ exists ff_q_fpmp_dot_mcp_ics_linear_neg_result_raw_np_cell_dot_pointwise_target. ff_code_dot_mcp_ics_linear_neg_result_raw_np_cell_dot = ff_q_fpmp_dot_mcp_ics_linear_neg_result_raw_np_cell_dot_pointwise_target * S ((S (fpmp_index_dot_mcp_ics_linear_neg_result_raw_np_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_linear_neg_result_raw_np_cell_dot) + (fpmp_target_dot_mcp_ics_linear_neg_result_raw_np_cell_dot_pointwise))) -> fpmp_target_dot_mcp_ics_linear_neg_result_raw_np_cell_dot_pointwise = fpmp_left_dot_mcp_ics_linear_neg_result_raw_np_cell_dot_pointwise * fpmp_right_dot_mcp_ics_linear_neg_result_raw_np_cell_dot_pointwise) /\ (exists ff_u_dot_mcp_ics_linear_neg_result_raw_np_cell_dot_sum ff_v_dot_mcp_ics_linear_neg_result_raw_np_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_linear_neg_result_raw_np_cell_dot_sum_start. ff_h_dot_mcp_ics_linear_neg_result_raw_np_cell_dot_sum_start + S (0) = S ((S (0)) * ff_v_dot_mcp_ics_linear_neg_result_raw_np_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_linear_neg_result_raw_np_cell_dot_sum_start. ff_u_dot_mcp_ics_linear_neg_result_raw_np_cell_dot_sum = ff_q_dot_mcp_ics_linear_neg_result_raw_np_cell_dot_sum_start * S ((S (0)) * ff_v_dot_mcp_ics_linear_neg_result_raw_np_cell_dot_sum) + (0))) /\ ((((exists ff_h_dot_mcp_ics_linear_neg_result_raw_np_cell_dot_sum_terminal. ff_h_dot_mcp_ics_linear_neg_result_raw_np_cell_dot_sum_terminal + S (ff_value_mcp_prefix_ics_linear_neg_result_raw_np) = S ((S (w)) * ff_v_dot_mcp_ics_linear_neg_result_raw_np_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_linear_neg_result_raw_np_cell_dot_sum_terminal. ff_u_dot_mcp_ics_linear_neg_result_raw_np_cell_dot_sum = ff_q_dot_mcp_ics_linear_neg_result_raw_np_cell_dot_sum_terminal * S ((S (w)) * ff_v_dot_mcp_ics_linear_neg_result_raw_np_cell_dot_sum) + (ff_value_mcp_prefix_ics_linear_neg_result_raw_np))) /\ forall ff_i_dot_mcp_ics_linear_neg_result_raw_np_cell_dot_sum. (exists ff_lt_dot_mcp_ics_linear_neg_result_raw_np_cell_dot_sum_bound. ff_lt_dot_mcp_ics_linear_neg_result_raw_np_cell_dot_sum_bound + S ff_i_dot_mcp_ics_linear_neg_result_raw_np_cell_dot_sum = w) -> exists ff_a_dot_mcp_ics_linear_neg_result_raw_np_cell_dot_sum ff_r_dot_mcp_ics_linear_neg_result_raw_np_cell_dot_sum ff_s_dot_mcp_ics_linear_neg_result_raw_np_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_linear_neg_result_raw_np_cell_dot_sum_summand. ff_h_dot_mcp_ics_linear_neg_result_raw_np_cell_dot_sum_summand + S (ff_a_dot_mcp_ics_linear_neg_result_raw_np_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_linear_neg_result_raw_np_cell_dot_sum)) * ff_scale_dot_mcp_ics_linear_neg_result_raw_np_cell_dot)) /\ exists ff_q_dot_mcp_ics_linear_neg_result_raw_np_cell_dot_sum_summand. ff_code_dot_mcp_ics_linear_neg_result_raw_np_cell_dot = ff_q_dot_mcp_ics_linear_neg_result_raw_np_cell_dot_sum_summand * S ((S (ff_i_dot_mcp_ics_linear_neg_result_raw_np_cell_dot_sum)) * ff_scale_dot_mcp_ics_linear_neg_result_raw_np_cell_dot) + (ff_a_dot_mcp_ics_linear_neg_result_raw_np_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_linear_neg_result_raw_np_cell_dot_sum_partial. ff_h_dot_mcp_ics_linear_neg_result_raw_np_cell_dot_sum_partial + S (ff_r_dot_mcp_ics_linear_neg_result_raw_np_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_linear_neg_result_raw_np_cell_dot_sum)) * ff_v_dot_mcp_ics_linear_neg_result_raw_np_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_linear_neg_result_raw_np_cell_dot_sum_partial. ff_u_dot_mcp_ics_linear_neg_result_raw_np_cell_dot_sum = ff_q_dot_mcp_ics_linear_neg_result_raw_np_cell_dot_sum_partial * S ((S (ff_i_dot_mcp_ics_linear_neg_result_raw_np_cell_dot_sum)) * ff_v_dot_mcp_ics_linear_neg_result_raw_np_cell_dot_sum) + (ff_r_dot_mcp_ics_linear_neg_result_raw_np_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_linear_neg_result_raw_np_cell_dot_sum_successor. ff_h_dot_mcp_ics_linear_neg_result_raw_np_cell_dot_sum_successor + S (ff_s_dot_mcp_ics_linear_neg_result_raw_np_cell_dot_sum) = S ((S (S ff_i_dot_mcp_ics_linear_neg_result_raw_np_cell_dot_sum)) * ff_v_dot_mcp_ics_linear_neg_result_raw_np_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_linear_neg_result_raw_np_cell_dot_sum_successor. ff_u_dot_mcp_ics_linear_neg_result_raw_np_cell_dot_sum = ff_q_dot_mcp_ics_linear_neg_result_raw_np_cell_dot_sum_successor * S ((S (S ff_i_dot_mcp_ics_linear_neg_result_raw_np_cell_dot_sum)) * ff_v_dot_mcp_ics_linear_neg_result_raw_np_cell_dot_sum) + (ff_s_dot_mcp_ics_linear_neg_result_raw_np_cell_dot_sum))) /\ ff_s_dot_mcp_ics_linear_neg_result_raw_np_cell_dot_sum = ff_r_dot_mcp_ics_linear_neg_result_raw_np_cell_dot_sum + ff_a_dot_mcp_ics_linear_neg_result_raw_np_cell_dot_sum))))))))))) /\ (((exists fs_h_mcp_ics_linear_neg_result_raw_np_entry. fs_h_mcp_ics_linear_neg_result_raw_np_entry + S (ff_value_mcp_prefix_ics_linear_neg_result_raw_np) = S ((S (ff_index_mcp_prefix_ics_linear_neg_result_raw_np)) * ff_nps_mcp_smatrix_ics_linear_neg_result_raw)) /\ exists fs_q_mcp_ics_linear_neg_result_raw_np_entry. ff_np_mcp_smatrix_ics_linear_neg_result_raw = fs_q_mcp_ics_linear_neg_result_raw_np_entry * S ((S (ff_index_mcp_prefix_ics_linear_neg_result_raw_np)) * ff_nps_mcp_smatrix_ics_linear_neg_result_raw) + (ff_value_mcp_prefix_ics_linear_neg_result_raw_np))))))) /\ ((forall ff_index_mcp_add_ics_linear_neg_result_raw_positive ff_left_mcp_add_ics_linear_neg_result_raw_positive ff_right_mcp_add_ics_linear_neg_result_raw_positive ff_target_mcp_add_ics_linear_neg_result_raw_positive. (exists mcp_gap_ics_linear_neg_result_raw_positive_bound. mcp_gap_ics_linear_neg_result_raw_positive_bound + S (ff_index_mcp_add_ics_linear_neg_result_raw_positive) = ((r) * (1))) -> (((exists fs_h_mcp_ics_linear_neg_result_raw_positive_left. fs_h_mcp_ics_linear_neg_result_raw_positive_left + S (ff_left_mcp_add_ics_linear_neg_result_raw_positive) = S ((S (ff_index_mcp_add_ics_linear_neg_result_raw_positive)) * ff_pps_mcp_smatrix_ics_linear_neg_result_raw)) /\ exists fs_q_mcp_ics_linear_neg_result_raw_positive_left. ff_pp_mcp_smatrix_ics_linear_neg_result_raw = fs_q_mcp_ics_linear_neg_result_raw_positive_left * S ((S (ff_index_mcp_add_ics_linear_neg_result_raw_positive)) * ff_pps_mcp_smatrix_ics_linear_neg_result_raw) + (ff_left_mcp_add_ics_linear_neg_result_raw_positive))) -> (((exists fs_h_mcp_ics_linear_neg_result_raw_positive_right. fs_h_mcp_ics_linear_neg_result_raw_positive_right + S (ff_right_mcp_add_ics_linear_neg_result_raw_positive) = S ((S (ff_index_mcp_add_ics_linear_neg_result_raw_positive)) * ff_nns_mcp_smatrix_ics_linear_neg_result_raw)) /\ exists fs_q_mcp_ics_linear_neg_result_raw_positive_right. ff_nn_mcp_smatrix_ics_linear_neg_result_raw = fs_q_mcp_ics_linear_neg_result_raw_positive_right * S ((S (ff_index_mcp_add_ics_linear_neg_result_raw_positive)) * ff_nns_mcp_smatrix_ics_linear_neg_result_raw) + (ff_right_mcp_add_ics_linear_neg_result_raw_positive))) -> (((exists fs_h_mcp_ics_linear_neg_result_raw_positive_target. fs_h_mcp_ics_linear_neg_result_raw_positive_target + S (ff_target_mcp_add_ics_linear_neg_result_raw_positive) = S ((S (ff_index_mcp_add_ics_linear_neg_result_raw_positive)) * ics_raw_positive_scale_linear_neg_result)) /\ exists fs_q_mcp_ics_linear_neg_result_raw_positive_target. ics_raw_positive_linear_neg_result = fs_q_mcp_ics_linear_neg_result_raw_positive_target * S ((S (ff_index_mcp_add_ics_linear_neg_result_raw_positive)) * ics_raw_positive_scale_linear_neg_result) + (ff_target_mcp_add_ics_linear_neg_result_raw_positive))) -> ff_target_mcp_add_ics_linear_neg_result_raw_positive = ff_left_mcp_add_ics_linear_neg_result_raw_positive + ff_right_mcp_add_ics_linear_neg_result_raw_positive) /\ (forall ff_index_mcp_add_ics_linear_neg_result_raw_negative ff_left_mcp_add_ics_linear_neg_result_raw_negative ff_right_mcp_add_ics_linear_neg_result_raw_negative ff_target_mcp_add_ics_linear_neg_result_raw_negative. (exists mcp_gap_ics_linear_neg_result_raw_negative_bound. mcp_gap_ics_linear_neg_result_raw_negative_bound + S (ff_index_mcp_add_ics_linear_neg_result_raw_negative) = ((r) * (1))) -> (((exists fs_h_mcp_ics_linear_neg_result_raw_negative_left. fs_h_mcp_ics_linear_neg_result_raw_negative_left + S (ff_left_mcp_add_ics_linear_neg_result_raw_negative) = S ((S (ff_index_mcp_add_ics_linear_neg_result_raw_negative)) * ff_pns_mcp_smatrix_ics_linear_neg_result_raw)) /\ exists fs_q_mcp_ics_linear_neg_result_raw_negative_left. ff_pn_mcp_smatrix_ics_linear_neg_result_raw = fs_q_mcp_ics_linear_neg_result_raw_negative_left * S ((S (ff_index_mcp_add_ics_linear_neg_result_raw_negative)) * ff_pns_mcp_smatrix_ics_linear_neg_result_raw) + (ff_left_mcp_add_ics_linear_neg_result_raw_negative))) -> (((exists fs_h_mcp_ics_linear_neg_result_raw_negative_right. fs_h_mcp_ics_linear_neg_result_raw_negative_right + S (ff_right_mcp_add_ics_linear_neg_result_raw_negative) = S ((S (ff_index_mcp_add_ics_linear_neg_result_raw_negative)) * ff_nps_mcp_smatrix_ics_linear_neg_result_raw)) /\ exists fs_q_mcp_ics_linear_neg_result_raw_negative_right. ff_np_mcp_smatrix_ics_linear_neg_result_raw = fs_q_mcp_ics_linear_neg_result_raw_negative_right * S ((S (ff_index_mcp_add_ics_linear_neg_result_raw_negative)) * ff_nps_mcp_smatrix_ics_linear_neg_result_raw) + (ff_right_mcp_add_ics_linear_neg_result_raw_negative))) -> (((exists fs_h_mcp_ics_linear_neg_result_raw_negative_target. fs_h_mcp_ics_linear_neg_result_raw_negative_target + S (ff_target_mcp_add_ics_linear_neg_result_raw_negative) = S ((S (ff_index_mcp_add_ics_linear_neg_result_raw_negative)) * ics_raw_negative_scale_linear_neg_result)) /\ exists fs_q_mcp_ics_linear_neg_result_raw_negative_target. ics_raw_negative_linear_neg_result = fs_q_mcp_ics_linear_neg_result_raw_negative_target * S ((S (ff_index_mcp_add_ics_linear_neg_result_raw_negative)) * ics_raw_negative_scale_linear_neg_result) + (ff_target_mcp_add_ics_linear_neg_result_raw_negative))) -> ff_target_mcp_add_ics_linear_neg_result_raw_negative = ff_left_mcp_add_ics_linear_neg_result_raw_negative + ff_right_mcp_add_ics_linear_neg_result_raw_negative))))))) /\ (forall ics_index_linear_neg_result_equal ics_value0_linear_neg_result_equal ics_value1_linear_neg_result_equal ics_value2_linear_neg_result_equal ics_value3_linear_neg_result_equal. (exists ics_gap_linear_neg_result_equal_bound. ics_gap_linear_neg_result_equal_bound + S (ics_index_linear_neg_result_equal) = (r)) -> (((exists fs_h_ics_linear_neg_result_equal_at0. fs_h_ics_linear_neg_result_equal_at0 + S (ics_value0_linear_neg_result_equal) = S ((S (ics_index_linear_neg_result_equal)) * ics_raw_positive_scale_linear_neg_result)) /\ exists fs_q_ics_linear_neg_result_equal_at0. ics_raw_positive_linear_neg_result = fs_q_ics_linear_neg_result_equal_at0 * S ((S (ics_index_linear_neg_result_equal)) * ics_raw_positive_scale_linear_neg_result) + (ics_value0_linear_neg_result_equal))) -> (((exists fs_h_ics_linear_neg_result_equal_at1. fs_h_ics_linear_neg_result_equal_at1 + S (ics_value1_linear_neg_result_equal) = S ((S (ics_index_linear_neg_result_equal)) * ics_raw_negative_scale_linear_neg_result)) /\ exists fs_q_ics_linear_neg_result_equal_at1. ics_raw_negative_linear_neg_result = fs_q_ics_linear_neg_result_equal_at1 * S ((S (ics_index_linear_neg_result_equal)) * ics_raw_negative_scale_linear_neg_result) + (ics_value1_linear_neg_result_equal))) -> (((exists fs_h_ics_linear_neg_result_equal_at2. fs_h_ics_linear_neg_result_equal_at2 + S (ics_value2_linear_neg_result_equal) = S ((S (ics_index_linear_neg_result_equal)) * nc)) /\ exists fs_q_ics_linear_neg_result_equal_at2. nb = fs_q_ics_linear_neg_result_equal_at2 * S ((S (ics_index_linear_neg_result_equal)) * nc) + (ics_value2_linear_neg_result_equal))) -> (((exists fs_h_ics_linear_neg_result_equal_at3. fs_h_ics_linear_neg_result_equal_at3 + S (ics_value3_linear_neg_result_equal) = S ((S (ics_index_linear_neg_result_equal)) * pc)) /\ exists fs_q_ics_linear_neg_result_equal_at3. pb = fs_q_ics_linear_neg_result_equal_at3 * S ((S (ics_index_linear_neg_result_equal)) * pc) + (ics_value3_linear_neg_result_equal))) -> ics_value0_linear_neg_result_equal + ics_value3_linear_neg_result_equal = ics_value2_linear_neg_result_equal + ics_value1_linear_neg_result_equal))))Complete tactic proof in conservative notation
All 52 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.
Read the argument
Proof checkpoints
52 script commands · 8 reading checkpoints · 0 local claims
This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.
Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.
Named ingredients (2)
01Fix variables and assumptionsL1–10
02Fix variables and assumptionsL11–15
03Separate the logical casesL16–20
04Construct an explicit witnessL21–24
05Separate the logical casesL25–25
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L25
split
06Use earlier factsL26–35
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L26
specialize integer_span_signed_product_negate (ab) - L27
specialize integer_span_signed_product_negate (ac) - L28
specialize integer_span_signed_product_negate (db) - L29
specialize integer_span_signed_product_negate (dc) - L30
specialize integer_span_signed_product_negate (eb) - L31
specialize integer_span_signed_product_negate (ec) - L32
specialize integer_span_signed_product_negate (fb) - L33
specialize integer_span_signed_product_negate (fc) - L34
specialize integer_span_signed_product_negate (w) - L35
specialize integer_span_signed_product_negate (r)
07Use earlier factsL36–45
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L36
specialize integer_span_signed_product_negate (x) - L37
specialize integer_span_signed_product_negate (x1) - L38
specialize integer_span_signed_product_negate (x2) - L39
specialize integer_span_signed_product_negate (x3) - L40
apply integer_span_signed_product_negate - L41
exact himage_witness_witness_witness_witness_left - L42
specialize integer_vector_equal_negated (x) - L43
specialize integer_vector_equal_negated (x1) - L44
specialize integer_vector_equal_negated (x2) - L45
specialize integer_vector_equal_negated (x3)
08Use earlier factsL46–52
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L46
specialize integer_vector_equal_negated (pb) - L47
specialize integer_vector_equal_negated (pc) - L48
specialize integer_vector_equal_negated (nb) - L49
specialize integer_vector_equal_negated (nc) - L50
specialize integer_vector_equal_negated (r) - L51
apply integer_vector_equal_negated - L52
exact himage_witness_witness_witness_witness_right
Original defined command ledger · 52 lines
- 0001
intro ab - 0002
intro ac - 0003
intro db - 0004
intro dc - 0005
intro eb - 0006
intro ec - 0007
intro fb - 0008
intro fc - 0009
intro w - 0010
intro r - 0011
intro pb - 0012
intro pc - 0013
intro nb - 0014
intro nc - 0015
intro himage - 0016
cases himage - 0017
cases himage_witness - 0018
cases himage_witness_witness - 0019
cases himage_witness_witness_witness - 0020
cases himage_witness_witness_witness_witness - 0021
exists x2 - 0022
exists x3 - 0023
exists x - 0024
exists x1 - 0025
split - 0026
specialize integer_span_signed_product_negate (ab) - 0027
specialize integer_span_signed_product_negate (ac) - 0028
specialize integer_span_signed_product_negate (db) - 0029
specialize integer_span_signed_product_negate (dc) - 0030
specialize integer_span_signed_product_negate (eb) - 0031
specialize integer_span_signed_product_negate (ec) - 0032
specialize integer_span_signed_product_negate (fb) - 0033
specialize integer_span_signed_product_negate (fc) - 0034
specialize integer_span_signed_product_negate (w) - 0035
specialize integer_span_signed_product_negate (r) - 0036
specialize integer_span_signed_product_negate (x) - 0037
specialize integer_span_signed_product_negate (x1) - 0038
specialize integer_span_signed_product_negate (x2) - 0039
specialize integer_span_signed_product_negate (x3) - 0040
apply integer_span_signed_product_negate - 0041
exact himage_witness_witness_witness_witness_left - 0042
specialize integer_vector_equal_negated (x) - 0043
specialize integer_vector_equal_negated (x1) - 0044
specialize integer_vector_equal_negated (x2) - 0045
specialize integer_vector_equal_negated (x3) - 0046
specialize integer_vector_equal_negated (pb) - 0047
specialize integer_vector_equal_negated (pc) - 0048
specialize integer_vector_equal_negated (nb) - 0049
specialize integer_vector_equal_negated (nc) - 0050
specialize integer_vector_equal_negated (r) - 0051
apply integer_vector_equal_negated - 0052
exact himage_witness_witness_witness_witness_right