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. SignedMatrixProduct(ab,ac,db,dc,eb,ec,fb,fc,w,1,r,pb,pc,nb,nc) → SignedMatrixProduct(ab,ac,db,dc,fb,fc,eb,ec,w,1,r,nb,nc,pb,pc)Every linked abbreviation expands hygienically to the identical original native formula.
Definition DAG
Actual proof prerequisites
none
Original expanded first-order statement
forall ab ac db dc eb ec fb fc w r pb pc nb nc. (exists ff_pp_mcp_smatrix_ics_negate_source ff_pps_mcp_smatrix_ics_negate_source ff_nn_mcp_smatrix_ics_negate_source ff_nns_mcp_smatrix_ics_negate_source ff_pn_mcp_smatrix_ics_negate_source ff_pns_mcp_smatrix_ics_negate_source ff_np_mcp_smatrix_ics_negate_source ff_nps_mcp_smatrix_ics_negate_source. ((forall ff_index_mcp_prefix_ics_negate_source_pp. (exists mcp_gap_ics_negate_source_pp_index. mcp_gap_ics_negate_source_pp_index + S (ff_index_mcp_prefix_ics_negate_source_pp) = ((r) * (1))) -> exists ff_row_mcp_prefix_ics_negate_source_pp ff_column_mcp_prefix_ics_negate_source_pp ff_value_mcp_prefix_ics_negate_source_pp. ((ff_index_mcp_prefix_ics_negate_source_pp) = (1) * ff_row_mcp_prefix_ics_negate_source_pp + ff_column_mcp_prefix_ics_negate_source_pp /\ ((exists mcp_gap_ics_negate_source_pp_column. mcp_gap_ics_negate_source_pp_column + S (ff_column_mcp_prefix_ics_negate_source_pp) = (1)) /\ ((exists ff_left_mcp_cell_ics_negate_source_pp_cell ff_left_scale_mcp_cell_ics_negate_source_pp_cell ff_right_mcp_cell_ics_negate_source_pp_cell ff_right_scale_mcp_cell_ics_negate_source_pp_cell. ((forall ff_index_mcp_ics_negate_source_pp_cell_row ff_source_mcp_ics_negate_source_pp_cell_row ff_target_mcp_ics_negate_source_pp_cell_row. (exists mcp_gap_ics_negate_source_pp_cell_row_bound. mcp_gap_ics_negate_source_pp_cell_row_bound + S (ff_index_mcp_ics_negate_source_pp_cell_row) = (w)) -> (((exists fs_h_mcp_ics_negate_source_pp_cell_row_source. fs_h_mcp_ics_negate_source_pp_cell_row_source + S (ff_source_mcp_ics_negate_source_pp_cell_row) = S ((S (((ff_row_mcp_prefix_ics_negate_source_pp) * (w)) + (1) * ff_index_mcp_ics_negate_source_pp_cell_row)) * ac)) /\ exists fs_q_mcp_ics_negate_source_pp_cell_row_source. ab = fs_q_mcp_ics_negate_source_pp_cell_row_source * S ((S (((ff_row_mcp_prefix_ics_negate_source_pp) * (w)) + (1) * ff_index_mcp_ics_negate_source_pp_cell_row)) * ac) + (ff_source_mcp_ics_negate_source_pp_cell_row))) -> (((exists fs_h_mcp_ics_negate_source_pp_cell_row_target. fs_h_mcp_ics_negate_source_pp_cell_row_target + S (ff_target_mcp_ics_negate_source_pp_cell_row) = S ((S (ff_index_mcp_ics_negate_source_pp_cell_row)) * ff_left_scale_mcp_cell_ics_negate_source_pp_cell)) /\ exists fs_q_mcp_ics_negate_source_pp_cell_row_target. ff_left_mcp_cell_ics_negate_source_pp_cell = fs_q_mcp_ics_negate_source_pp_cell_row_target * S ((S (ff_index_mcp_ics_negate_source_pp_cell_row)) * ff_left_scale_mcp_cell_ics_negate_source_pp_cell) + (ff_target_mcp_ics_negate_source_pp_cell_row))) -> ff_target_mcp_ics_negate_source_pp_cell_row = ff_source_mcp_ics_negate_source_pp_cell_row) /\ ((forall ff_index_mcp_ics_negate_source_pp_cell_column ff_source_mcp_ics_negate_source_pp_cell_column ff_target_mcp_ics_negate_source_pp_cell_column. (exists mcp_gap_ics_negate_source_pp_cell_column_bound. mcp_gap_ics_negate_source_pp_cell_column_bound + S (ff_index_mcp_ics_negate_source_pp_cell_column) = (w)) -> (((exists fs_h_mcp_ics_negate_source_pp_cell_column_source. fs_h_mcp_ics_negate_source_pp_cell_column_source + S (ff_source_mcp_ics_negate_source_pp_cell_column) = S ((S ((ff_column_mcp_prefix_ics_negate_source_pp) + (1) * ff_index_mcp_ics_negate_source_pp_cell_column)) * ec)) /\ exists fs_q_mcp_ics_negate_source_pp_cell_column_source. eb = fs_q_mcp_ics_negate_source_pp_cell_column_source * S ((S ((ff_column_mcp_prefix_ics_negate_source_pp) + (1) * ff_index_mcp_ics_negate_source_pp_cell_column)) * ec) + (ff_source_mcp_ics_negate_source_pp_cell_column))) -> (((exists fs_h_mcp_ics_negate_source_pp_cell_column_target. fs_h_mcp_ics_negate_source_pp_cell_column_target + S (ff_target_mcp_ics_negate_source_pp_cell_column) = S ((S (ff_index_mcp_ics_negate_source_pp_cell_column)) * ff_right_scale_mcp_cell_ics_negate_source_pp_cell)) /\ exists fs_q_mcp_ics_negate_source_pp_cell_column_target. ff_right_mcp_cell_ics_negate_source_pp_cell = fs_q_mcp_ics_negate_source_pp_cell_column_target * S ((S (ff_index_mcp_ics_negate_source_pp_cell_column)) * ff_right_scale_mcp_cell_ics_negate_source_pp_cell) + (ff_target_mcp_ics_negate_source_pp_cell_column))) -> ff_target_mcp_ics_negate_source_pp_cell_column = ff_source_mcp_ics_negate_source_pp_cell_column) /\ (exists ff_code_dot_mcp_ics_negate_source_pp_cell_dot ff_scale_dot_mcp_ics_negate_source_pp_cell_dot. ((forall fpmp_index_dot_mcp_ics_negate_source_pp_cell_dot_pointwise fpmp_left_dot_mcp_ics_negate_source_pp_cell_dot_pointwise fpmp_right_dot_mcp_ics_negate_source_pp_cell_dot_pointwise fpmp_target_dot_mcp_ics_negate_source_pp_cell_dot_pointwise. (exists fpmp_gap_dot_mcp_ics_negate_source_pp_cell_dot_pointwise. fpmp_gap_dot_mcp_ics_negate_source_pp_cell_dot_pointwise + S fpmp_index_dot_mcp_ics_negate_source_pp_cell_dot_pointwise = w) -> (((exists ff_h_fpmp_dot_mcp_ics_negate_source_pp_cell_dot_pointwise_left. ff_h_fpmp_dot_mcp_ics_negate_source_pp_cell_dot_pointwise_left + S (fpmp_left_dot_mcp_ics_negate_source_pp_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_negate_source_pp_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_negate_source_pp_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_negate_source_pp_cell_dot_pointwise_left. ff_left_mcp_cell_ics_negate_source_pp_cell = ff_q_fpmp_dot_mcp_ics_negate_source_pp_cell_dot_pointwise_left * S ((S (fpmp_index_dot_mcp_ics_negate_source_pp_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_negate_source_pp_cell) + (fpmp_left_dot_mcp_ics_negate_source_pp_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_negate_source_pp_cell_dot_pointwise_right. ff_h_fpmp_dot_mcp_ics_negate_source_pp_cell_dot_pointwise_right + S (fpmp_right_dot_mcp_ics_negate_source_pp_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_negate_source_pp_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_negate_source_pp_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_negate_source_pp_cell_dot_pointwise_right. ff_right_mcp_cell_ics_negate_source_pp_cell = ff_q_fpmp_dot_mcp_ics_negate_source_pp_cell_dot_pointwise_right * S ((S (fpmp_index_dot_mcp_ics_negate_source_pp_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_negate_source_pp_cell) + (fpmp_right_dot_mcp_ics_negate_source_pp_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_negate_source_pp_cell_dot_pointwise_target. ff_h_fpmp_dot_mcp_ics_negate_source_pp_cell_dot_pointwise_target + S (fpmp_target_dot_mcp_ics_negate_source_pp_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_negate_source_pp_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_negate_source_pp_cell_dot)) /\ exists ff_q_fpmp_dot_mcp_ics_negate_source_pp_cell_dot_pointwise_target. ff_code_dot_mcp_ics_negate_source_pp_cell_dot = ff_q_fpmp_dot_mcp_ics_negate_source_pp_cell_dot_pointwise_target * S ((S (fpmp_index_dot_mcp_ics_negate_source_pp_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_negate_source_pp_cell_dot) + (fpmp_target_dot_mcp_ics_negate_source_pp_cell_dot_pointwise))) -> fpmp_target_dot_mcp_ics_negate_source_pp_cell_dot_pointwise = fpmp_left_dot_mcp_ics_negate_source_pp_cell_dot_pointwise * fpmp_right_dot_mcp_ics_negate_source_pp_cell_dot_pointwise) /\ (exists ff_u_dot_mcp_ics_negate_source_pp_cell_dot_sum ff_v_dot_mcp_ics_negate_source_pp_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_negate_source_pp_cell_dot_sum_start. ff_h_dot_mcp_ics_negate_source_pp_cell_dot_sum_start + S (0) = S ((S (0)) * ff_v_dot_mcp_ics_negate_source_pp_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_negate_source_pp_cell_dot_sum_start. ff_u_dot_mcp_ics_negate_source_pp_cell_dot_sum = ff_q_dot_mcp_ics_negate_source_pp_cell_dot_sum_start * S ((S (0)) * ff_v_dot_mcp_ics_negate_source_pp_cell_dot_sum) + (0))) /\ ((((exists ff_h_dot_mcp_ics_negate_source_pp_cell_dot_sum_terminal. ff_h_dot_mcp_ics_negate_source_pp_cell_dot_sum_terminal + S (ff_value_mcp_prefix_ics_negate_source_pp) = S ((S (w)) * ff_v_dot_mcp_ics_negate_source_pp_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_negate_source_pp_cell_dot_sum_terminal. ff_u_dot_mcp_ics_negate_source_pp_cell_dot_sum = ff_q_dot_mcp_ics_negate_source_pp_cell_dot_sum_terminal * S ((S (w)) * ff_v_dot_mcp_ics_negate_source_pp_cell_dot_sum) + (ff_value_mcp_prefix_ics_negate_source_pp))) /\ forall ff_i_dot_mcp_ics_negate_source_pp_cell_dot_sum. (exists ff_lt_dot_mcp_ics_negate_source_pp_cell_dot_sum_bound. ff_lt_dot_mcp_ics_negate_source_pp_cell_dot_sum_bound + S ff_i_dot_mcp_ics_negate_source_pp_cell_dot_sum = w) -> exists ff_a_dot_mcp_ics_negate_source_pp_cell_dot_sum ff_r_dot_mcp_ics_negate_source_pp_cell_dot_sum ff_s_dot_mcp_ics_negate_source_pp_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_negate_source_pp_cell_dot_sum_summand. ff_h_dot_mcp_ics_negate_source_pp_cell_dot_sum_summand + S (ff_a_dot_mcp_ics_negate_source_pp_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_negate_source_pp_cell_dot_sum)) * ff_scale_dot_mcp_ics_negate_source_pp_cell_dot)) /\ exists ff_q_dot_mcp_ics_negate_source_pp_cell_dot_sum_summand. ff_code_dot_mcp_ics_negate_source_pp_cell_dot = ff_q_dot_mcp_ics_negate_source_pp_cell_dot_sum_summand * S ((S (ff_i_dot_mcp_ics_negate_source_pp_cell_dot_sum)) * ff_scale_dot_mcp_ics_negate_source_pp_cell_dot) + (ff_a_dot_mcp_ics_negate_source_pp_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_negate_source_pp_cell_dot_sum_partial. ff_h_dot_mcp_ics_negate_source_pp_cell_dot_sum_partial + S (ff_r_dot_mcp_ics_negate_source_pp_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_negate_source_pp_cell_dot_sum)) * ff_v_dot_mcp_ics_negate_source_pp_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_negate_source_pp_cell_dot_sum_partial. ff_u_dot_mcp_ics_negate_source_pp_cell_dot_sum = ff_q_dot_mcp_ics_negate_source_pp_cell_dot_sum_partial * S ((S (ff_i_dot_mcp_ics_negate_source_pp_cell_dot_sum)) * ff_v_dot_mcp_ics_negate_source_pp_cell_dot_sum) + (ff_r_dot_mcp_ics_negate_source_pp_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_negate_source_pp_cell_dot_sum_successor. ff_h_dot_mcp_ics_negate_source_pp_cell_dot_sum_successor + S (ff_s_dot_mcp_ics_negate_source_pp_cell_dot_sum) = S ((S (S ff_i_dot_mcp_ics_negate_source_pp_cell_dot_sum)) * ff_v_dot_mcp_ics_negate_source_pp_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_negate_source_pp_cell_dot_sum_successor. ff_u_dot_mcp_ics_negate_source_pp_cell_dot_sum = ff_q_dot_mcp_ics_negate_source_pp_cell_dot_sum_successor * S ((S (S ff_i_dot_mcp_ics_negate_source_pp_cell_dot_sum)) * ff_v_dot_mcp_ics_negate_source_pp_cell_dot_sum) + (ff_s_dot_mcp_ics_negate_source_pp_cell_dot_sum))) /\ ff_s_dot_mcp_ics_negate_source_pp_cell_dot_sum = ff_r_dot_mcp_ics_negate_source_pp_cell_dot_sum + ff_a_dot_mcp_ics_negate_source_pp_cell_dot_sum))))))))))) /\ (((exists fs_h_mcp_ics_negate_source_pp_entry. fs_h_mcp_ics_negate_source_pp_entry + S (ff_value_mcp_prefix_ics_negate_source_pp) = S ((S (ff_index_mcp_prefix_ics_negate_source_pp)) * ff_pps_mcp_smatrix_ics_negate_source)) /\ exists fs_q_mcp_ics_negate_source_pp_entry. ff_pp_mcp_smatrix_ics_negate_source = fs_q_mcp_ics_negate_source_pp_entry * S ((S (ff_index_mcp_prefix_ics_negate_source_pp)) * ff_pps_mcp_smatrix_ics_negate_source) + (ff_value_mcp_prefix_ics_negate_source_pp))))))) /\ ((forall ff_index_mcp_prefix_ics_negate_source_nn. (exists mcp_gap_ics_negate_source_nn_index. mcp_gap_ics_negate_source_nn_index + S (ff_index_mcp_prefix_ics_negate_source_nn) = ((r) * (1))) -> exists ff_row_mcp_prefix_ics_negate_source_nn ff_column_mcp_prefix_ics_negate_source_nn ff_value_mcp_prefix_ics_negate_source_nn. ((ff_index_mcp_prefix_ics_negate_source_nn) = (1) * ff_row_mcp_prefix_ics_negate_source_nn + ff_column_mcp_prefix_ics_negate_source_nn /\ ((exists mcp_gap_ics_negate_source_nn_column. mcp_gap_ics_negate_source_nn_column + S (ff_column_mcp_prefix_ics_negate_source_nn) = (1)) /\ ((exists ff_left_mcp_cell_ics_negate_source_nn_cell ff_left_scale_mcp_cell_ics_negate_source_nn_cell ff_right_mcp_cell_ics_negate_source_nn_cell ff_right_scale_mcp_cell_ics_negate_source_nn_cell. ((forall ff_index_mcp_ics_negate_source_nn_cell_row ff_source_mcp_ics_negate_source_nn_cell_row ff_target_mcp_ics_negate_source_nn_cell_row. (exists mcp_gap_ics_negate_source_nn_cell_row_bound. mcp_gap_ics_negate_source_nn_cell_row_bound + S (ff_index_mcp_ics_negate_source_nn_cell_row) = (w)) -> (((exists fs_h_mcp_ics_negate_source_nn_cell_row_source. fs_h_mcp_ics_negate_source_nn_cell_row_source + S (ff_source_mcp_ics_negate_source_nn_cell_row) = S ((S (((ff_row_mcp_prefix_ics_negate_source_nn) * (w)) + (1) * ff_index_mcp_ics_negate_source_nn_cell_row)) * dc)) /\ exists fs_q_mcp_ics_negate_source_nn_cell_row_source. db = fs_q_mcp_ics_negate_source_nn_cell_row_source * S ((S (((ff_row_mcp_prefix_ics_negate_source_nn) * (w)) + (1) * ff_index_mcp_ics_negate_source_nn_cell_row)) * dc) + (ff_source_mcp_ics_negate_source_nn_cell_row))) -> (((exists fs_h_mcp_ics_negate_source_nn_cell_row_target. fs_h_mcp_ics_negate_source_nn_cell_row_target + S (ff_target_mcp_ics_negate_source_nn_cell_row) = S ((S (ff_index_mcp_ics_negate_source_nn_cell_row)) * ff_left_scale_mcp_cell_ics_negate_source_nn_cell)) /\ exists fs_q_mcp_ics_negate_source_nn_cell_row_target. ff_left_mcp_cell_ics_negate_source_nn_cell = fs_q_mcp_ics_negate_source_nn_cell_row_target * S ((S (ff_index_mcp_ics_negate_source_nn_cell_row)) * ff_left_scale_mcp_cell_ics_negate_source_nn_cell) + (ff_target_mcp_ics_negate_source_nn_cell_row))) -> ff_target_mcp_ics_negate_source_nn_cell_row = ff_source_mcp_ics_negate_source_nn_cell_row) /\ ((forall ff_index_mcp_ics_negate_source_nn_cell_column ff_source_mcp_ics_negate_source_nn_cell_column ff_target_mcp_ics_negate_source_nn_cell_column. (exists mcp_gap_ics_negate_source_nn_cell_column_bound. mcp_gap_ics_negate_source_nn_cell_column_bound + S (ff_index_mcp_ics_negate_source_nn_cell_column) = (w)) -> (((exists fs_h_mcp_ics_negate_source_nn_cell_column_source. fs_h_mcp_ics_negate_source_nn_cell_column_source + S (ff_source_mcp_ics_negate_source_nn_cell_column) = S ((S ((ff_column_mcp_prefix_ics_negate_source_nn) + (1) * ff_index_mcp_ics_negate_source_nn_cell_column)) * fc)) /\ exists fs_q_mcp_ics_negate_source_nn_cell_column_source. fb = fs_q_mcp_ics_negate_source_nn_cell_column_source * S ((S ((ff_column_mcp_prefix_ics_negate_source_nn) + (1) * ff_index_mcp_ics_negate_source_nn_cell_column)) * fc) + (ff_source_mcp_ics_negate_source_nn_cell_column))) -> (((exists fs_h_mcp_ics_negate_source_nn_cell_column_target. fs_h_mcp_ics_negate_source_nn_cell_column_target + S (ff_target_mcp_ics_negate_source_nn_cell_column) = S ((S (ff_index_mcp_ics_negate_source_nn_cell_column)) * ff_right_scale_mcp_cell_ics_negate_source_nn_cell)) /\ exists fs_q_mcp_ics_negate_source_nn_cell_column_target. ff_right_mcp_cell_ics_negate_source_nn_cell = fs_q_mcp_ics_negate_source_nn_cell_column_target * S ((S (ff_index_mcp_ics_negate_source_nn_cell_column)) * ff_right_scale_mcp_cell_ics_negate_source_nn_cell) + (ff_target_mcp_ics_negate_source_nn_cell_column))) -> ff_target_mcp_ics_negate_source_nn_cell_column = ff_source_mcp_ics_negate_source_nn_cell_column) /\ (exists ff_code_dot_mcp_ics_negate_source_nn_cell_dot ff_scale_dot_mcp_ics_negate_source_nn_cell_dot. ((forall fpmp_index_dot_mcp_ics_negate_source_nn_cell_dot_pointwise fpmp_left_dot_mcp_ics_negate_source_nn_cell_dot_pointwise fpmp_right_dot_mcp_ics_negate_source_nn_cell_dot_pointwise fpmp_target_dot_mcp_ics_negate_source_nn_cell_dot_pointwise. (exists fpmp_gap_dot_mcp_ics_negate_source_nn_cell_dot_pointwise. fpmp_gap_dot_mcp_ics_negate_source_nn_cell_dot_pointwise + S fpmp_index_dot_mcp_ics_negate_source_nn_cell_dot_pointwise = w) -> (((exists ff_h_fpmp_dot_mcp_ics_negate_source_nn_cell_dot_pointwise_left. ff_h_fpmp_dot_mcp_ics_negate_source_nn_cell_dot_pointwise_left + S (fpmp_left_dot_mcp_ics_negate_source_nn_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_negate_source_nn_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_negate_source_nn_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_negate_source_nn_cell_dot_pointwise_left. ff_left_mcp_cell_ics_negate_source_nn_cell = ff_q_fpmp_dot_mcp_ics_negate_source_nn_cell_dot_pointwise_left * S ((S (fpmp_index_dot_mcp_ics_negate_source_nn_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_negate_source_nn_cell) + (fpmp_left_dot_mcp_ics_negate_source_nn_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_negate_source_nn_cell_dot_pointwise_right. ff_h_fpmp_dot_mcp_ics_negate_source_nn_cell_dot_pointwise_right + S (fpmp_right_dot_mcp_ics_negate_source_nn_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_negate_source_nn_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_negate_source_nn_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_negate_source_nn_cell_dot_pointwise_right. ff_right_mcp_cell_ics_negate_source_nn_cell = ff_q_fpmp_dot_mcp_ics_negate_source_nn_cell_dot_pointwise_right * S ((S (fpmp_index_dot_mcp_ics_negate_source_nn_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_negate_source_nn_cell) + (fpmp_right_dot_mcp_ics_negate_source_nn_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_negate_source_nn_cell_dot_pointwise_target. ff_h_fpmp_dot_mcp_ics_negate_source_nn_cell_dot_pointwise_target + S (fpmp_target_dot_mcp_ics_negate_source_nn_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_negate_source_nn_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_negate_source_nn_cell_dot)) /\ exists ff_q_fpmp_dot_mcp_ics_negate_source_nn_cell_dot_pointwise_target. ff_code_dot_mcp_ics_negate_source_nn_cell_dot = ff_q_fpmp_dot_mcp_ics_negate_source_nn_cell_dot_pointwise_target * S ((S (fpmp_index_dot_mcp_ics_negate_source_nn_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_negate_source_nn_cell_dot) + (fpmp_target_dot_mcp_ics_negate_source_nn_cell_dot_pointwise))) -> fpmp_target_dot_mcp_ics_negate_source_nn_cell_dot_pointwise = fpmp_left_dot_mcp_ics_negate_source_nn_cell_dot_pointwise * fpmp_right_dot_mcp_ics_negate_source_nn_cell_dot_pointwise) /\ (exists ff_u_dot_mcp_ics_negate_source_nn_cell_dot_sum ff_v_dot_mcp_ics_negate_source_nn_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_negate_source_nn_cell_dot_sum_start. ff_h_dot_mcp_ics_negate_source_nn_cell_dot_sum_start + S (0) = S ((S (0)) * ff_v_dot_mcp_ics_negate_source_nn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_negate_source_nn_cell_dot_sum_start. ff_u_dot_mcp_ics_negate_source_nn_cell_dot_sum = ff_q_dot_mcp_ics_negate_source_nn_cell_dot_sum_start * S ((S (0)) * ff_v_dot_mcp_ics_negate_source_nn_cell_dot_sum) + (0))) /\ ((((exists ff_h_dot_mcp_ics_negate_source_nn_cell_dot_sum_terminal. ff_h_dot_mcp_ics_negate_source_nn_cell_dot_sum_terminal + S (ff_value_mcp_prefix_ics_negate_source_nn) = S ((S (w)) * ff_v_dot_mcp_ics_negate_source_nn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_negate_source_nn_cell_dot_sum_terminal. ff_u_dot_mcp_ics_negate_source_nn_cell_dot_sum = ff_q_dot_mcp_ics_negate_source_nn_cell_dot_sum_terminal * S ((S (w)) * ff_v_dot_mcp_ics_negate_source_nn_cell_dot_sum) + (ff_value_mcp_prefix_ics_negate_source_nn))) /\ forall ff_i_dot_mcp_ics_negate_source_nn_cell_dot_sum. (exists ff_lt_dot_mcp_ics_negate_source_nn_cell_dot_sum_bound. ff_lt_dot_mcp_ics_negate_source_nn_cell_dot_sum_bound + S ff_i_dot_mcp_ics_negate_source_nn_cell_dot_sum = w) -> exists ff_a_dot_mcp_ics_negate_source_nn_cell_dot_sum ff_r_dot_mcp_ics_negate_source_nn_cell_dot_sum ff_s_dot_mcp_ics_negate_source_nn_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_negate_source_nn_cell_dot_sum_summand. ff_h_dot_mcp_ics_negate_source_nn_cell_dot_sum_summand + S (ff_a_dot_mcp_ics_negate_source_nn_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_negate_source_nn_cell_dot_sum)) * ff_scale_dot_mcp_ics_negate_source_nn_cell_dot)) /\ exists ff_q_dot_mcp_ics_negate_source_nn_cell_dot_sum_summand. ff_code_dot_mcp_ics_negate_source_nn_cell_dot = ff_q_dot_mcp_ics_negate_source_nn_cell_dot_sum_summand * S ((S (ff_i_dot_mcp_ics_negate_source_nn_cell_dot_sum)) * ff_scale_dot_mcp_ics_negate_source_nn_cell_dot) + (ff_a_dot_mcp_ics_negate_source_nn_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_negate_source_nn_cell_dot_sum_partial. ff_h_dot_mcp_ics_negate_source_nn_cell_dot_sum_partial + S (ff_r_dot_mcp_ics_negate_source_nn_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_negate_source_nn_cell_dot_sum)) * ff_v_dot_mcp_ics_negate_source_nn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_negate_source_nn_cell_dot_sum_partial. ff_u_dot_mcp_ics_negate_source_nn_cell_dot_sum = ff_q_dot_mcp_ics_negate_source_nn_cell_dot_sum_partial * S ((S (ff_i_dot_mcp_ics_negate_source_nn_cell_dot_sum)) * ff_v_dot_mcp_ics_negate_source_nn_cell_dot_sum) + (ff_r_dot_mcp_ics_negate_source_nn_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_negate_source_nn_cell_dot_sum_successor. ff_h_dot_mcp_ics_negate_source_nn_cell_dot_sum_successor + S (ff_s_dot_mcp_ics_negate_source_nn_cell_dot_sum) = S ((S (S ff_i_dot_mcp_ics_negate_source_nn_cell_dot_sum)) * ff_v_dot_mcp_ics_negate_source_nn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_negate_source_nn_cell_dot_sum_successor. ff_u_dot_mcp_ics_negate_source_nn_cell_dot_sum = ff_q_dot_mcp_ics_negate_source_nn_cell_dot_sum_successor * S ((S (S ff_i_dot_mcp_ics_negate_source_nn_cell_dot_sum)) * ff_v_dot_mcp_ics_negate_source_nn_cell_dot_sum) + (ff_s_dot_mcp_ics_negate_source_nn_cell_dot_sum))) /\ ff_s_dot_mcp_ics_negate_source_nn_cell_dot_sum = ff_r_dot_mcp_ics_negate_source_nn_cell_dot_sum + ff_a_dot_mcp_ics_negate_source_nn_cell_dot_sum))))))))))) /\ (((exists fs_h_mcp_ics_negate_source_nn_entry. fs_h_mcp_ics_negate_source_nn_entry + S (ff_value_mcp_prefix_ics_negate_source_nn) = S ((S (ff_index_mcp_prefix_ics_negate_source_nn)) * ff_nns_mcp_smatrix_ics_negate_source)) /\ exists fs_q_mcp_ics_negate_source_nn_entry. ff_nn_mcp_smatrix_ics_negate_source = fs_q_mcp_ics_negate_source_nn_entry * S ((S (ff_index_mcp_prefix_ics_negate_source_nn)) * ff_nns_mcp_smatrix_ics_negate_source) + (ff_value_mcp_prefix_ics_negate_source_nn))))))) /\ ((forall ff_index_mcp_prefix_ics_negate_source_pn. (exists mcp_gap_ics_negate_source_pn_index. mcp_gap_ics_negate_source_pn_index + S (ff_index_mcp_prefix_ics_negate_source_pn) = ((r) * (1))) -> exists ff_row_mcp_prefix_ics_negate_source_pn ff_column_mcp_prefix_ics_negate_source_pn ff_value_mcp_prefix_ics_negate_source_pn. ((ff_index_mcp_prefix_ics_negate_source_pn) = (1) * ff_row_mcp_prefix_ics_negate_source_pn + ff_column_mcp_prefix_ics_negate_source_pn /\ ((exists mcp_gap_ics_negate_source_pn_column. mcp_gap_ics_negate_source_pn_column + S (ff_column_mcp_prefix_ics_negate_source_pn) = (1)) /\ ((exists ff_left_mcp_cell_ics_negate_source_pn_cell ff_left_scale_mcp_cell_ics_negate_source_pn_cell ff_right_mcp_cell_ics_negate_source_pn_cell ff_right_scale_mcp_cell_ics_negate_source_pn_cell. ((forall ff_index_mcp_ics_negate_source_pn_cell_row ff_source_mcp_ics_negate_source_pn_cell_row ff_target_mcp_ics_negate_source_pn_cell_row. (exists mcp_gap_ics_negate_source_pn_cell_row_bound. mcp_gap_ics_negate_source_pn_cell_row_bound + S (ff_index_mcp_ics_negate_source_pn_cell_row) = (w)) -> (((exists fs_h_mcp_ics_negate_source_pn_cell_row_source. fs_h_mcp_ics_negate_source_pn_cell_row_source + S (ff_source_mcp_ics_negate_source_pn_cell_row) = S ((S (((ff_row_mcp_prefix_ics_negate_source_pn) * (w)) + (1) * ff_index_mcp_ics_negate_source_pn_cell_row)) * ac)) /\ exists fs_q_mcp_ics_negate_source_pn_cell_row_source. ab = fs_q_mcp_ics_negate_source_pn_cell_row_source * S ((S (((ff_row_mcp_prefix_ics_negate_source_pn) * (w)) + (1) * ff_index_mcp_ics_negate_source_pn_cell_row)) * ac) + (ff_source_mcp_ics_negate_source_pn_cell_row))) -> (((exists fs_h_mcp_ics_negate_source_pn_cell_row_target. fs_h_mcp_ics_negate_source_pn_cell_row_target + S (ff_target_mcp_ics_negate_source_pn_cell_row) = S ((S (ff_index_mcp_ics_negate_source_pn_cell_row)) * ff_left_scale_mcp_cell_ics_negate_source_pn_cell)) /\ exists fs_q_mcp_ics_negate_source_pn_cell_row_target. ff_left_mcp_cell_ics_negate_source_pn_cell = fs_q_mcp_ics_negate_source_pn_cell_row_target * S ((S (ff_index_mcp_ics_negate_source_pn_cell_row)) * ff_left_scale_mcp_cell_ics_negate_source_pn_cell) + (ff_target_mcp_ics_negate_source_pn_cell_row))) -> ff_target_mcp_ics_negate_source_pn_cell_row = ff_source_mcp_ics_negate_source_pn_cell_row) /\ ((forall ff_index_mcp_ics_negate_source_pn_cell_column ff_source_mcp_ics_negate_source_pn_cell_column ff_target_mcp_ics_negate_source_pn_cell_column. (exists mcp_gap_ics_negate_source_pn_cell_column_bound. mcp_gap_ics_negate_source_pn_cell_column_bound + S (ff_index_mcp_ics_negate_source_pn_cell_column) = (w)) -> (((exists fs_h_mcp_ics_negate_source_pn_cell_column_source. fs_h_mcp_ics_negate_source_pn_cell_column_source + S (ff_source_mcp_ics_negate_source_pn_cell_column) = S ((S ((ff_column_mcp_prefix_ics_negate_source_pn) + (1) * ff_index_mcp_ics_negate_source_pn_cell_column)) * fc)) /\ exists fs_q_mcp_ics_negate_source_pn_cell_column_source. fb = fs_q_mcp_ics_negate_source_pn_cell_column_source * S ((S ((ff_column_mcp_prefix_ics_negate_source_pn) + (1) * ff_index_mcp_ics_negate_source_pn_cell_column)) * fc) + (ff_source_mcp_ics_negate_source_pn_cell_column))) -> (((exists fs_h_mcp_ics_negate_source_pn_cell_column_target. fs_h_mcp_ics_negate_source_pn_cell_column_target + S (ff_target_mcp_ics_negate_source_pn_cell_column) = S ((S (ff_index_mcp_ics_negate_source_pn_cell_column)) * ff_right_scale_mcp_cell_ics_negate_source_pn_cell)) /\ exists fs_q_mcp_ics_negate_source_pn_cell_column_target. ff_right_mcp_cell_ics_negate_source_pn_cell = fs_q_mcp_ics_negate_source_pn_cell_column_target * S ((S (ff_index_mcp_ics_negate_source_pn_cell_column)) * ff_right_scale_mcp_cell_ics_negate_source_pn_cell) + (ff_target_mcp_ics_negate_source_pn_cell_column))) -> ff_target_mcp_ics_negate_source_pn_cell_column = ff_source_mcp_ics_negate_source_pn_cell_column) /\ (exists ff_code_dot_mcp_ics_negate_source_pn_cell_dot ff_scale_dot_mcp_ics_negate_source_pn_cell_dot. ((forall fpmp_index_dot_mcp_ics_negate_source_pn_cell_dot_pointwise fpmp_left_dot_mcp_ics_negate_source_pn_cell_dot_pointwise fpmp_right_dot_mcp_ics_negate_source_pn_cell_dot_pointwise fpmp_target_dot_mcp_ics_negate_source_pn_cell_dot_pointwise. (exists fpmp_gap_dot_mcp_ics_negate_source_pn_cell_dot_pointwise. fpmp_gap_dot_mcp_ics_negate_source_pn_cell_dot_pointwise + S fpmp_index_dot_mcp_ics_negate_source_pn_cell_dot_pointwise = w) -> (((exists ff_h_fpmp_dot_mcp_ics_negate_source_pn_cell_dot_pointwise_left. ff_h_fpmp_dot_mcp_ics_negate_source_pn_cell_dot_pointwise_left + S (fpmp_left_dot_mcp_ics_negate_source_pn_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_negate_source_pn_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_negate_source_pn_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_negate_source_pn_cell_dot_pointwise_left. ff_left_mcp_cell_ics_negate_source_pn_cell = ff_q_fpmp_dot_mcp_ics_negate_source_pn_cell_dot_pointwise_left * S ((S (fpmp_index_dot_mcp_ics_negate_source_pn_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_negate_source_pn_cell) + (fpmp_left_dot_mcp_ics_negate_source_pn_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_negate_source_pn_cell_dot_pointwise_right. ff_h_fpmp_dot_mcp_ics_negate_source_pn_cell_dot_pointwise_right + S (fpmp_right_dot_mcp_ics_negate_source_pn_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_negate_source_pn_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_negate_source_pn_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_negate_source_pn_cell_dot_pointwise_right. ff_right_mcp_cell_ics_negate_source_pn_cell = ff_q_fpmp_dot_mcp_ics_negate_source_pn_cell_dot_pointwise_right * S ((S (fpmp_index_dot_mcp_ics_negate_source_pn_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_negate_source_pn_cell) + (fpmp_right_dot_mcp_ics_negate_source_pn_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_negate_source_pn_cell_dot_pointwise_target. ff_h_fpmp_dot_mcp_ics_negate_source_pn_cell_dot_pointwise_target + S (fpmp_target_dot_mcp_ics_negate_source_pn_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_negate_source_pn_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_negate_source_pn_cell_dot)) /\ exists ff_q_fpmp_dot_mcp_ics_negate_source_pn_cell_dot_pointwise_target. ff_code_dot_mcp_ics_negate_source_pn_cell_dot = ff_q_fpmp_dot_mcp_ics_negate_source_pn_cell_dot_pointwise_target * S ((S (fpmp_index_dot_mcp_ics_negate_source_pn_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_negate_source_pn_cell_dot) + (fpmp_target_dot_mcp_ics_negate_source_pn_cell_dot_pointwise))) -> fpmp_target_dot_mcp_ics_negate_source_pn_cell_dot_pointwise = fpmp_left_dot_mcp_ics_negate_source_pn_cell_dot_pointwise * fpmp_right_dot_mcp_ics_negate_source_pn_cell_dot_pointwise) /\ (exists ff_u_dot_mcp_ics_negate_source_pn_cell_dot_sum ff_v_dot_mcp_ics_negate_source_pn_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_negate_source_pn_cell_dot_sum_start. ff_h_dot_mcp_ics_negate_source_pn_cell_dot_sum_start + S (0) = S ((S (0)) * ff_v_dot_mcp_ics_negate_source_pn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_negate_source_pn_cell_dot_sum_start. ff_u_dot_mcp_ics_negate_source_pn_cell_dot_sum = ff_q_dot_mcp_ics_negate_source_pn_cell_dot_sum_start * S ((S (0)) * ff_v_dot_mcp_ics_negate_source_pn_cell_dot_sum) + (0))) /\ ((((exists ff_h_dot_mcp_ics_negate_source_pn_cell_dot_sum_terminal. ff_h_dot_mcp_ics_negate_source_pn_cell_dot_sum_terminal + S (ff_value_mcp_prefix_ics_negate_source_pn) = S ((S (w)) * ff_v_dot_mcp_ics_negate_source_pn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_negate_source_pn_cell_dot_sum_terminal. ff_u_dot_mcp_ics_negate_source_pn_cell_dot_sum = ff_q_dot_mcp_ics_negate_source_pn_cell_dot_sum_terminal * S ((S (w)) * ff_v_dot_mcp_ics_negate_source_pn_cell_dot_sum) + (ff_value_mcp_prefix_ics_negate_source_pn))) /\ forall ff_i_dot_mcp_ics_negate_source_pn_cell_dot_sum. (exists ff_lt_dot_mcp_ics_negate_source_pn_cell_dot_sum_bound. ff_lt_dot_mcp_ics_negate_source_pn_cell_dot_sum_bound + S ff_i_dot_mcp_ics_negate_source_pn_cell_dot_sum = w) -> exists ff_a_dot_mcp_ics_negate_source_pn_cell_dot_sum ff_r_dot_mcp_ics_negate_source_pn_cell_dot_sum ff_s_dot_mcp_ics_negate_source_pn_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_negate_source_pn_cell_dot_sum_summand. ff_h_dot_mcp_ics_negate_source_pn_cell_dot_sum_summand + S (ff_a_dot_mcp_ics_negate_source_pn_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_negate_source_pn_cell_dot_sum)) * ff_scale_dot_mcp_ics_negate_source_pn_cell_dot)) /\ exists ff_q_dot_mcp_ics_negate_source_pn_cell_dot_sum_summand. ff_code_dot_mcp_ics_negate_source_pn_cell_dot = ff_q_dot_mcp_ics_negate_source_pn_cell_dot_sum_summand * S ((S (ff_i_dot_mcp_ics_negate_source_pn_cell_dot_sum)) * ff_scale_dot_mcp_ics_negate_source_pn_cell_dot) + (ff_a_dot_mcp_ics_negate_source_pn_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_negate_source_pn_cell_dot_sum_partial. ff_h_dot_mcp_ics_negate_source_pn_cell_dot_sum_partial + S (ff_r_dot_mcp_ics_negate_source_pn_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_negate_source_pn_cell_dot_sum)) * ff_v_dot_mcp_ics_negate_source_pn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_negate_source_pn_cell_dot_sum_partial. ff_u_dot_mcp_ics_negate_source_pn_cell_dot_sum = ff_q_dot_mcp_ics_negate_source_pn_cell_dot_sum_partial * S ((S (ff_i_dot_mcp_ics_negate_source_pn_cell_dot_sum)) * ff_v_dot_mcp_ics_negate_source_pn_cell_dot_sum) + (ff_r_dot_mcp_ics_negate_source_pn_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_negate_source_pn_cell_dot_sum_successor. ff_h_dot_mcp_ics_negate_source_pn_cell_dot_sum_successor + S (ff_s_dot_mcp_ics_negate_source_pn_cell_dot_sum) = S ((S (S ff_i_dot_mcp_ics_negate_source_pn_cell_dot_sum)) * ff_v_dot_mcp_ics_negate_source_pn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_negate_source_pn_cell_dot_sum_successor. ff_u_dot_mcp_ics_negate_source_pn_cell_dot_sum = ff_q_dot_mcp_ics_negate_source_pn_cell_dot_sum_successor * S ((S (S ff_i_dot_mcp_ics_negate_source_pn_cell_dot_sum)) * ff_v_dot_mcp_ics_negate_source_pn_cell_dot_sum) + (ff_s_dot_mcp_ics_negate_source_pn_cell_dot_sum))) /\ ff_s_dot_mcp_ics_negate_source_pn_cell_dot_sum = ff_r_dot_mcp_ics_negate_source_pn_cell_dot_sum + ff_a_dot_mcp_ics_negate_source_pn_cell_dot_sum))))))))))) /\ (((exists fs_h_mcp_ics_negate_source_pn_entry. fs_h_mcp_ics_negate_source_pn_entry + S (ff_value_mcp_prefix_ics_negate_source_pn) = S ((S (ff_index_mcp_prefix_ics_negate_source_pn)) * ff_pns_mcp_smatrix_ics_negate_source)) /\ exists fs_q_mcp_ics_negate_source_pn_entry. ff_pn_mcp_smatrix_ics_negate_source = fs_q_mcp_ics_negate_source_pn_entry * S ((S (ff_index_mcp_prefix_ics_negate_source_pn)) * ff_pns_mcp_smatrix_ics_negate_source) + (ff_value_mcp_prefix_ics_negate_source_pn))))))) /\ ((forall ff_index_mcp_prefix_ics_negate_source_np. (exists mcp_gap_ics_negate_source_np_index. mcp_gap_ics_negate_source_np_index + S (ff_index_mcp_prefix_ics_negate_source_np) = ((r) * (1))) -> exists ff_row_mcp_prefix_ics_negate_source_np ff_column_mcp_prefix_ics_negate_source_np ff_value_mcp_prefix_ics_negate_source_np. ((ff_index_mcp_prefix_ics_negate_source_np) = (1) * ff_row_mcp_prefix_ics_negate_source_np + ff_column_mcp_prefix_ics_negate_source_np /\ ((exists mcp_gap_ics_negate_source_np_column. mcp_gap_ics_negate_source_np_column + S (ff_column_mcp_prefix_ics_negate_source_np) = (1)) /\ ((exists ff_left_mcp_cell_ics_negate_source_np_cell ff_left_scale_mcp_cell_ics_negate_source_np_cell ff_right_mcp_cell_ics_negate_source_np_cell ff_right_scale_mcp_cell_ics_negate_source_np_cell. ((forall ff_index_mcp_ics_negate_source_np_cell_row ff_source_mcp_ics_negate_source_np_cell_row ff_target_mcp_ics_negate_source_np_cell_row. (exists mcp_gap_ics_negate_source_np_cell_row_bound. mcp_gap_ics_negate_source_np_cell_row_bound + S (ff_index_mcp_ics_negate_source_np_cell_row) = (w)) -> (((exists fs_h_mcp_ics_negate_source_np_cell_row_source. fs_h_mcp_ics_negate_source_np_cell_row_source + S (ff_source_mcp_ics_negate_source_np_cell_row) = S ((S (((ff_row_mcp_prefix_ics_negate_source_np) * (w)) + (1) * ff_index_mcp_ics_negate_source_np_cell_row)) * dc)) /\ exists fs_q_mcp_ics_negate_source_np_cell_row_source. db = fs_q_mcp_ics_negate_source_np_cell_row_source * S ((S (((ff_row_mcp_prefix_ics_negate_source_np) * (w)) + (1) * ff_index_mcp_ics_negate_source_np_cell_row)) * dc) + (ff_source_mcp_ics_negate_source_np_cell_row))) -> (((exists fs_h_mcp_ics_negate_source_np_cell_row_target. fs_h_mcp_ics_negate_source_np_cell_row_target + S (ff_target_mcp_ics_negate_source_np_cell_row) = S ((S (ff_index_mcp_ics_negate_source_np_cell_row)) * ff_left_scale_mcp_cell_ics_negate_source_np_cell)) /\ exists fs_q_mcp_ics_negate_source_np_cell_row_target. ff_left_mcp_cell_ics_negate_source_np_cell = fs_q_mcp_ics_negate_source_np_cell_row_target * S ((S (ff_index_mcp_ics_negate_source_np_cell_row)) * ff_left_scale_mcp_cell_ics_negate_source_np_cell) + (ff_target_mcp_ics_negate_source_np_cell_row))) -> ff_target_mcp_ics_negate_source_np_cell_row = ff_source_mcp_ics_negate_source_np_cell_row) /\ ((forall ff_index_mcp_ics_negate_source_np_cell_column ff_source_mcp_ics_negate_source_np_cell_column ff_target_mcp_ics_negate_source_np_cell_column. (exists mcp_gap_ics_negate_source_np_cell_column_bound. mcp_gap_ics_negate_source_np_cell_column_bound + S (ff_index_mcp_ics_negate_source_np_cell_column) = (w)) -> (((exists fs_h_mcp_ics_negate_source_np_cell_column_source. fs_h_mcp_ics_negate_source_np_cell_column_source + S (ff_source_mcp_ics_negate_source_np_cell_column) = S ((S ((ff_column_mcp_prefix_ics_negate_source_np) + (1) * ff_index_mcp_ics_negate_source_np_cell_column)) * ec)) /\ exists fs_q_mcp_ics_negate_source_np_cell_column_source. eb = fs_q_mcp_ics_negate_source_np_cell_column_source * S ((S ((ff_column_mcp_prefix_ics_negate_source_np) + (1) * ff_index_mcp_ics_negate_source_np_cell_column)) * ec) + (ff_source_mcp_ics_negate_source_np_cell_column))) -> (((exists fs_h_mcp_ics_negate_source_np_cell_column_target. fs_h_mcp_ics_negate_source_np_cell_column_target + S (ff_target_mcp_ics_negate_source_np_cell_column) = S ((S (ff_index_mcp_ics_negate_source_np_cell_column)) * ff_right_scale_mcp_cell_ics_negate_source_np_cell)) /\ exists fs_q_mcp_ics_negate_source_np_cell_column_target. ff_right_mcp_cell_ics_negate_source_np_cell = fs_q_mcp_ics_negate_source_np_cell_column_target * S ((S (ff_index_mcp_ics_negate_source_np_cell_column)) * ff_right_scale_mcp_cell_ics_negate_source_np_cell) + (ff_target_mcp_ics_negate_source_np_cell_column))) -> ff_target_mcp_ics_negate_source_np_cell_column = ff_source_mcp_ics_negate_source_np_cell_column) /\ (exists ff_code_dot_mcp_ics_negate_source_np_cell_dot ff_scale_dot_mcp_ics_negate_source_np_cell_dot. ((forall fpmp_index_dot_mcp_ics_negate_source_np_cell_dot_pointwise fpmp_left_dot_mcp_ics_negate_source_np_cell_dot_pointwise fpmp_right_dot_mcp_ics_negate_source_np_cell_dot_pointwise fpmp_target_dot_mcp_ics_negate_source_np_cell_dot_pointwise. (exists fpmp_gap_dot_mcp_ics_negate_source_np_cell_dot_pointwise. fpmp_gap_dot_mcp_ics_negate_source_np_cell_dot_pointwise + S fpmp_index_dot_mcp_ics_negate_source_np_cell_dot_pointwise = w) -> (((exists ff_h_fpmp_dot_mcp_ics_negate_source_np_cell_dot_pointwise_left. ff_h_fpmp_dot_mcp_ics_negate_source_np_cell_dot_pointwise_left + S (fpmp_left_dot_mcp_ics_negate_source_np_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_negate_source_np_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_negate_source_np_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_negate_source_np_cell_dot_pointwise_left. ff_left_mcp_cell_ics_negate_source_np_cell = ff_q_fpmp_dot_mcp_ics_negate_source_np_cell_dot_pointwise_left * S ((S (fpmp_index_dot_mcp_ics_negate_source_np_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_negate_source_np_cell) + (fpmp_left_dot_mcp_ics_negate_source_np_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_negate_source_np_cell_dot_pointwise_right. ff_h_fpmp_dot_mcp_ics_negate_source_np_cell_dot_pointwise_right + S (fpmp_right_dot_mcp_ics_negate_source_np_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_negate_source_np_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_negate_source_np_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_negate_source_np_cell_dot_pointwise_right. ff_right_mcp_cell_ics_negate_source_np_cell = ff_q_fpmp_dot_mcp_ics_negate_source_np_cell_dot_pointwise_right * S ((S (fpmp_index_dot_mcp_ics_negate_source_np_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_negate_source_np_cell) + (fpmp_right_dot_mcp_ics_negate_source_np_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_negate_source_np_cell_dot_pointwise_target. ff_h_fpmp_dot_mcp_ics_negate_source_np_cell_dot_pointwise_target + S (fpmp_target_dot_mcp_ics_negate_source_np_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_negate_source_np_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_negate_source_np_cell_dot)) /\ exists ff_q_fpmp_dot_mcp_ics_negate_source_np_cell_dot_pointwise_target. ff_code_dot_mcp_ics_negate_source_np_cell_dot = ff_q_fpmp_dot_mcp_ics_negate_source_np_cell_dot_pointwise_target * S ((S (fpmp_index_dot_mcp_ics_negate_source_np_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_negate_source_np_cell_dot) + (fpmp_target_dot_mcp_ics_negate_source_np_cell_dot_pointwise))) -> fpmp_target_dot_mcp_ics_negate_source_np_cell_dot_pointwise = fpmp_left_dot_mcp_ics_negate_source_np_cell_dot_pointwise * fpmp_right_dot_mcp_ics_negate_source_np_cell_dot_pointwise) /\ (exists ff_u_dot_mcp_ics_negate_source_np_cell_dot_sum ff_v_dot_mcp_ics_negate_source_np_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_negate_source_np_cell_dot_sum_start. ff_h_dot_mcp_ics_negate_source_np_cell_dot_sum_start + S (0) = S ((S (0)) * ff_v_dot_mcp_ics_negate_source_np_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_negate_source_np_cell_dot_sum_start. ff_u_dot_mcp_ics_negate_source_np_cell_dot_sum = ff_q_dot_mcp_ics_negate_source_np_cell_dot_sum_start * S ((S (0)) * ff_v_dot_mcp_ics_negate_source_np_cell_dot_sum) + (0))) /\ ((((exists ff_h_dot_mcp_ics_negate_source_np_cell_dot_sum_terminal. ff_h_dot_mcp_ics_negate_source_np_cell_dot_sum_terminal + S (ff_value_mcp_prefix_ics_negate_source_np) = S ((S (w)) * ff_v_dot_mcp_ics_negate_source_np_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_negate_source_np_cell_dot_sum_terminal. ff_u_dot_mcp_ics_negate_source_np_cell_dot_sum = ff_q_dot_mcp_ics_negate_source_np_cell_dot_sum_terminal * S ((S (w)) * ff_v_dot_mcp_ics_negate_source_np_cell_dot_sum) + (ff_value_mcp_prefix_ics_negate_source_np))) /\ forall ff_i_dot_mcp_ics_negate_source_np_cell_dot_sum. (exists ff_lt_dot_mcp_ics_negate_source_np_cell_dot_sum_bound. ff_lt_dot_mcp_ics_negate_source_np_cell_dot_sum_bound + S ff_i_dot_mcp_ics_negate_source_np_cell_dot_sum = w) -> exists ff_a_dot_mcp_ics_negate_source_np_cell_dot_sum ff_r_dot_mcp_ics_negate_source_np_cell_dot_sum ff_s_dot_mcp_ics_negate_source_np_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_negate_source_np_cell_dot_sum_summand. ff_h_dot_mcp_ics_negate_source_np_cell_dot_sum_summand + S (ff_a_dot_mcp_ics_negate_source_np_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_negate_source_np_cell_dot_sum)) * ff_scale_dot_mcp_ics_negate_source_np_cell_dot)) /\ exists ff_q_dot_mcp_ics_negate_source_np_cell_dot_sum_summand. ff_code_dot_mcp_ics_negate_source_np_cell_dot = ff_q_dot_mcp_ics_negate_source_np_cell_dot_sum_summand * S ((S (ff_i_dot_mcp_ics_negate_source_np_cell_dot_sum)) * ff_scale_dot_mcp_ics_negate_source_np_cell_dot) + (ff_a_dot_mcp_ics_negate_source_np_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_negate_source_np_cell_dot_sum_partial. ff_h_dot_mcp_ics_negate_source_np_cell_dot_sum_partial + S (ff_r_dot_mcp_ics_negate_source_np_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_negate_source_np_cell_dot_sum)) * ff_v_dot_mcp_ics_negate_source_np_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_negate_source_np_cell_dot_sum_partial. ff_u_dot_mcp_ics_negate_source_np_cell_dot_sum = ff_q_dot_mcp_ics_negate_source_np_cell_dot_sum_partial * S ((S (ff_i_dot_mcp_ics_negate_source_np_cell_dot_sum)) * ff_v_dot_mcp_ics_negate_source_np_cell_dot_sum) + (ff_r_dot_mcp_ics_negate_source_np_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_negate_source_np_cell_dot_sum_successor. ff_h_dot_mcp_ics_negate_source_np_cell_dot_sum_successor + S (ff_s_dot_mcp_ics_negate_source_np_cell_dot_sum) = S ((S (S ff_i_dot_mcp_ics_negate_source_np_cell_dot_sum)) * ff_v_dot_mcp_ics_negate_source_np_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_negate_source_np_cell_dot_sum_successor. ff_u_dot_mcp_ics_negate_source_np_cell_dot_sum = ff_q_dot_mcp_ics_negate_source_np_cell_dot_sum_successor * S ((S (S ff_i_dot_mcp_ics_negate_source_np_cell_dot_sum)) * ff_v_dot_mcp_ics_negate_source_np_cell_dot_sum) + (ff_s_dot_mcp_ics_negate_source_np_cell_dot_sum))) /\ ff_s_dot_mcp_ics_negate_source_np_cell_dot_sum = ff_r_dot_mcp_ics_negate_source_np_cell_dot_sum + ff_a_dot_mcp_ics_negate_source_np_cell_dot_sum))))))))))) /\ (((exists fs_h_mcp_ics_negate_source_np_entry. fs_h_mcp_ics_negate_source_np_entry + S (ff_value_mcp_prefix_ics_negate_source_np) = S ((S (ff_index_mcp_prefix_ics_negate_source_np)) * ff_nps_mcp_smatrix_ics_negate_source)) /\ exists fs_q_mcp_ics_negate_source_np_entry. ff_np_mcp_smatrix_ics_negate_source = fs_q_mcp_ics_negate_source_np_entry * S ((S (ff_index_mcp_prefix_ics_negate_source_np)) * ff_nps_mcp_smatrix_ics_negate_source) + (ff_value_mcp_prefix_ics_negate_source_np))))))) /\ ((forall ff_index_mcp_add_ics_negate_source_positive ff_left_mcp_add_ics_negate_source_positive ff_right_mcp_add_ics_negate_source_positive ff_target_mcp_add_ics_negate_source_positive. (exists mcp_gap_ics_negate_source_positive_bound. mcp_gap_ics_negate_source_positive_bound + S (ff_index_mcp_add_ics_negate_source_positive) = ((r) * (1))) -> (((exists fs_h_mcp_ics_negate_source_positive_left. fs_h_mcp_ics_negate_source_positive_left + S (ff_left_mcp_add_ics_negate_source_positive) = S ((S (ff_index_mcp_add_ics_negate_source_positive)) * ff_pps_mcp_smatrix_ics_negate_source)) /\ exists fs_q_mcp_ics_negate_source_positive_left. ff_pp_mcp_smatrix_ics_negate_source = fs_q_mcp_ics_negate_source_positive_left * S ((S (ff_index_mcp_add_ics_negate_source_positive)) * ff_pps_mcp_smatrix_ics_negate_source) + (ff_left_mcp_add_ics_negate_source_positive))) -> (((exists fs_h_mcp_ics_negate_source_positive_right. fs_h_mcp_ics_negate_source_positive_right + S (ff_right_mcp_add_ics_negate_source_positive) = S ((S (ff_index_mcp_add_ics_negate_source_positive)) * ff_nns_mcp_smatrix_ics_negate_source)) /\ exists fs_q_mcp_ics_negate_source_positive_right. ff_nn_mcp_smatrix_ics_negate_source = fs_q_mcp_ics_negate_source_positive_right * S ((S (ff_index_mcp_add_ics_negate_source_positive)) * ff_nns_mcp_smatrix_ics_negate_source) + (ff_right_mcp_add_ics_negate_source_positive))) -> (((exists fs_h_mcp_ics_negate_source_positive_target. fs_h_mcp_ics_negate_source_positive_target + S (ff_target_mcp_add_ics_negate_source_positive) = S ((S (ff_index_mcp_add_ics_negate_source_positive)) * pc)) /\ exists fs_q_mcp_ics_negate_source_positive_target. pb = fs_q_mcp_ics_negate_source_positive_target * S ((S (ff_index_mcp_add_ics_negate_source_positive)) * pc) + (ff_target_mcp_add_ics_negate_source_positive))) -> ff_target_mcp_add_ics_negate_source_positive = ff_left_mcp_add_ics_negate_source_positive + ff_right_mcp_add_ics_negate_source_positive) /\ (forall ff_index_mcp_add_ics_negate_source_negative ff_left_mcp_add_ics_negate_source_negative ff_right_mcp_add_ics_negate_source_negative ff_target_mcp_add_ics_negate_source_negative. (exists mcp_gap_ics_negate_source_negative_bound. mcp_gap_ics_negate_source_negative_bound + S (ff_index_mcp_add_ics_negate_source_negative) = ((r) * (1))) -> (((exists fs_h_mcp_ics_negate_source_negative_left. fs_h_mcp_ics_negate_source_negative_left + S (ff_left_mcp_add_ics_negate_source_negative) = S ((S (ff_index_mcp_add_ics_negate_source_negative)) * ff_pns_mcp_smatrix_ics_negate_source)) /\ exists fs_q_mcp_ics_negate_source_negative_left. ff_pn_mcp_smatrix_ics_negate_source = fs_q_mcp_ics_negate_source_negative_left * S ((S (ff_index_mcp_add_ics_negate_source_negative)) * ff_pns_mcp_smatrix_ics_negate_source) + (ff_left_mcp_add_ics_negate_source_negative))) -> (((exists fs_h_mcp_ics_negate_source_negative_right. fs_h_mcp_ics_negate_source_negative_right + S (ff_right_mcp_add_ics_negate_source_negative) = S ((S (ff_index_mcp_add_ics_negate_source_negative)) * ff_nps_mcp_smatrix_ics_negate_source)) /\ exists fs_q_mcp_ics_negate_source_negative_right. ff_np_mcp_smatrix_ics_negate_source = fs_q_mcp_ics_negate_source_negative_right * S ((S (ff_index_mcp_add_ics_negate_source_negative)) * ff_nps_mcp_smatrix_ics_negate_source) + (ff_right_mcp_add_ics_negate_source_negative))) -> (((exists fs_h_mcp_ics_negate_source_negative_target. fs_h_mcp_ics_negate_source_negative_target + S (ff_target_mcp_add_ics_negate_source_negative) = S ((S (ff_index_mcp_add_ics_negate_source_negative)) * nc)) /\ exists fs_q_mcp_ics_negate_source_negative_target. nb = fs_q_mcp_ics_negate_source_negative_target * S ((S (ff_index_mcp_add_ics_negate_source_negative)) * nc) + (ff_target_mcp_add_ics_negate_source_negative))) -> ff_target_mcp_add_ics_negate_source_negative = ff_left_mcp_add_ics_negate_source_negative + ff_right_mcp_add_ics_negate_source_negative))))))) -> (exists ff_pp_mcp_smatrix_ics_negate_result ff_pps_mcp_smatrix_ics_negate_result ff_nn_mcp_smatrix_ics_negate_result ff_nns_mcp_smatrix_ics_negate_result ff_pn_mcp_smatrix_ics_negate_result ff_pns_mcp_smatrix_ics_negate_result ff_np_mcp_smatrix_ics_negate_result ff_nps_mcp_smatrix_ics_negate_result. ((forall ff_index_mcp_prefix_ics_negate_result_pp. (exists mcp_gap_ics_negate_result_pp_index. mcp_gap_ics_negate_result_pp_index + S (ff_index_mcp_prefix_ics_negate_result_pp) = ((r) * (1))) -> exists ff_row_mcp_prefix_ics_negate_result_pp ff_column_mcp_prefix_ics_negate_result_pp ff_value_mcp_prefix_ics_negate_result_pp. ((ff_index_mcp_prefix_ics_negate_result_pp) = (1) * ff_row_mcp_prefix_ics_negate_result_pp + ff_column_mcp_prefix_ics_negate_result_pp /\ ((exists mcp_gap_ics_negate_result_pp_column. mcp_gap_ics_negate_result_pp_column + S (ff_column_mcp_prefix_ics_negate_result_pp) = (1)) /\ ((exists ff_left_mcp_cell_ics_negate_result_pp_cell ff_left_scale_mcp_cell_ics_negate_result_pp_cell ff_right_mcp_cell_ics_negate_result_pp_cell ff_right_scale_mcp_cell_ics_negate_result_pp_cell. ((forall ff_index_mcp_ics_negate_result_pp_cell_row ff_source_mcp_ics_negate_result_pp_cell_row ff_target_mcp_ics_negate_result_pp_cell_row. (exists mcp_gap_ics_negate_result_pp_cell_row_bound. mcp_gap_ics_negate_result_pp_cell_row_bound + S (ff_index_mcp_ics_negate_result_pp_cell_row) = (w)) -> (((exists fs_h_mcp_ics_negate_result_pp_cell_row_source. fs_h_mcp_ics_negate_result_pp_cell_row_source + S (ff_source_mcp_ics_negate_result_pp_cell_row) = S ((S (((ff_row_mcp_prefix_ics_negate_result_pp) * (w)) + (1) * ff_index_mcp_ics_negate_result_pp_cell_row)) * ac)) /\ exists fs_q_mcp_ics_negate_result_pp_cell_row_source. ab = fs_q_mcp_ics_negate_result_pp_cell_row_source * S ((S (((ff_row_mcp_prefix_ics_negate_result_pp) * (w)) + (1) * ff_index_mcp_ics_negate_result_pp_cell_row)) * ac) + (ff_source_mcp_ics_negate_result_pp_cell_row))) -> (((exists fs_h_mcp_ics_negate_result_pp_cell_row_target. fs_h_mcp_ics_negate_result_pp_cell_row_target + S (ff_target_mcp_ics_negate_result_pp_cell_row) = S ((S (ff_index_mcp_ics_negate_result_pp_cell_row)) * ff_left_scale_mcp_cell_ics_negate_result_pp_cell)) /\ exists fs_q_mcp_ics_negate_result_pp_cell_row_target. ff_left_mcp_cell_ics_negate_result_pp_cell = fs_q_mcp_ics_negate_result_pp_cell_row_target * S ((S (ff_index_mcp_ics_negate_result_pp_cell_row)) * ff_left_scale_mcp_cell_ics_negate_result_pp_cell) + (ff_target_mcp_ics_negate_result_pp_cell_row))) -> ff_target_mcp_ics_negate_result_pp_cell_row = ff_source_mcp_ics_negate_result_pp_cell_row) /\ ((forall ff_index_mcp_ics_negate_result_pp_cell_column ff_source_mcp_ics_negate_result_pp_cell_column ff_target_mcp_ics_negate_result_pp_cell_column. (exists mcp_gap_ics_negate_result_pp_cell_column_bound. mcp_gap_ics_negate_result_pp_cell_column_bound + S (ff_index_mcp_ics_negate_result_pp_cell_column) = (w)) -> (((exists fs_h_mcp_ics_negate_result_pp_cell_column_source. fs_h_mcp_ics_negate_result_pp_cell_column_source + S (ff_source_mcp_ics_negate_result_pp_cell_column) = S ((S ((ff_column_mcp_prefix_ics_negate_result_pp) + (1) * ff_index_mcp_ics_negate_result_pp_cell_column)) * fc)) /\ exists fs_q_mcp_ics_negate_result_pp_cell_column_source. fb = fs_q_mcp_ics_negate_result_pp_cell_column_source * S ((S ((ff_column_mcp_prefix_ics_negate_result_pp) + (1) * ff_index_mcp_ics_negate_result_pp_cell_column)) * fc) + (ff_source_mcp_ics_negate_result_pp_cell_column))) -> (((exists fs_h_mcp_ics_negate_result_pp_cell_column_target. fs_h_mcp_ics_negate_result_pp_cell_column_target + S (ff_target_mcp_ics_negate_result_pp_cell_column) = S ((S (ff_index_mcp_ics_negate_result_pp_cell_column)) * ff_right_scale_mcp_cell_ics_negate_result_pp_cell)) /\ exists fs_q_mcp_ics_negate_result_pp_cell_column_target. ff_right_mcp_cell_ics_negate_result_pp_cell = fs_q_mcp_ics_negate_result_pp_cell_column_target * S ((S (ff_index_mcp_ics_negate_result_pp_cell_column)) * ff_right_scale_mcp_cell_ics_negate_result_pp_cell) + (ff_target_mcp_ics_negate_result_pp_cell_column))) -> ff_target_mcp_ics_negate_result_pp_cell_column = ff_source_mcp_ics_negate_result_pp_cell_column) /\ (exists ff_code_dot_mcp_ics_negate_result_pp_cell_dot ff_scale_dot_mcp_ics_negate_result_pp_cell_dot. ((forall fpmp_index_dot_mcp_ics_negate_result_pp_cell_dot_pointwise fpmp_left_dot_mcp_ics_negate_result_pp_cell_dot_pointwise fpmp_right_dot_mcp_ics_negate_result_pp_cell_dot_pointwise fpmp_target_dot_mcp_ics_negate_result_pp_cell_dot_pointwise. (exists fpmp_gap_dot_mcp_ics_negate_result_pp_cell_dot_pointwise. fpmp_gap_dot_mcp_ics_negate_result_pp_cell_dot_pointwise + S fpmp_index_dot_mcp_ics_negate_result_pp_cell_dot_pointwise = w) -> (((exists ff_h_fpmp_dot_mcp_ics_negate_result_pp_cell_dot_pointwise_left. ff_h_fpmp_dot_mcp_ics_negate_result_pp_cell_dot_pointwise_left + S (fpmp_left_dot_mcp_ics_negate_result_pp_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_negate_result_pp_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_negate_result_pp_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_negate_result_pp_cell_dot_pointwise_left. ff_left_mcp_cell_ics_negate_result_pp_cell = ff_q_fpmp_dot_mcp_ics_negate_result_pp_cell_dot_pointwise_left * S ((S (fpmp_index_dot_mcp_ics_negate_result_pp_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_negate_result_pp_cell) + (fpmp_left_dot_mcp_ics_negate_result_pp_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_negate_result_pp_cell_dot_pointwise_right. ff_h_fpmp_dot_mcp_ics_negate_result_pp_cell_dot_pointwise_right + S (fpmp_right_dot_mcp_ics_negate_result_pp_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_negate_result_pp_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_negate_result_pp_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_negate_result_pp_cell_dot_pointwise_right. ff_right_mcp_cell_ics_negate_result_pp_cell = ff_q_fpmp_dot_mcp_ics_negate_result_pp_cell_dot_pointwise_right * S ((S (fpmp_index_dot_mcp_ics_negate_result_pp_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_negate_result_pp_cell) + (fpmp_right_dot_mcp_ics_negate_result_pp_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_negate_result_pp_cell_dot_pointwise_target. ff_h_fpmp_dot_mcp_ics_negate_result_pp_cell_dot_pointwise_target + S (fpmp_target_dot_mcp_ics_negate_result_pp_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_negate_result_pp_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_negate_result_pp_cell_dot)) /\ exists ff_q_fpmp_dot_mcp_ics_negate_result_pp_cell_dot_pointwise_target. ff_code_dot_mcp_ics_negate_result_pp_cell_dot = ff_q_fpmp_dot_mcp_ics_negate_result_pp_cell_dot_pointwise_target * S ((S (fpmp_index_dot_mcp_ics_negate_result_pp_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_negate_result_pp_cell_dot) + (fpmp_target_dot_mcp_ics_negate_result_pp_cell_dot_pointwise))) -> fpmp_target_dot_mcp_ics_negate_result_pp_cell_dot_pointwise = fpmp_left_dot_mcp_ics_negate_result_pp_cell_dot_pointwise * fpmp_right_dot_mcp_ics_negate_result_pp_cell_dot_pointwise) /\ (exists ff_u_dot_mcp_ics_negate_result_pp_cell_dot_sum ff_v_dot_mcp_ics_negate_result_pp_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_negate_result_pp_cell_dot_sum_start. ff_h_dot_mcp_ics_negate_result_pp_cell_dot_sum_start + S (0) = S ((S (0)) * ff_v_dot_mcp_ics_negate_result_pp_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_negate_result_pp_cell_dot_sum_start. ff_u_dot_mcp_ics_negate_result_pp_cell_dot_sum = ff_q_dot_mcp_ics_negate_result_pp_cell_dot_sum_start * S ((S (0)) * ff_v_dot_mcp_ics_negate_result_pp_cell_dot_sum) + (0))) /\ ((((exists ff_h_dot_mcp_ics_negate_result_pp_cell_dot_sum_terminal. ff_h_dot_mcp_ics_negate_result_pp_cell_dot_sum_terminal + S (ff_value_mcp_prefix_ics_negate_result_pp) = S ((S (w)) * ff_v_dot_mcp_ics_negate_result_pp_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_negate_result_pp_cell_dot_sum_terminal. ff_u_dot_mcp_ics_negate_result_pp_cell_dot_sum = ff_q_dot_mcp_ics_negate_result_pp_cell_dot_sum_terminal * S ((S (w)) * ff_v_dot_mcp_ics_negate_result_pp_cell_dot_sum) + (ff_value_mcp_prefix_ics_negate_result_pp))) /\ forall ff_i_dot_mcp_ics_negate_result_pp_cell_dot_sum. (exists ff_lt_dot_mcp_ics_negate_result_pp_cell_dot_sum_bound. ff_lt_dot_mcp_ics_negate_result_pp_cell_dot_sum_bound + S ff_i_dot_mcp_ics_negate_result_pp_cell_dot_sum = w) -> exists ff_a_dot_mcp_ics_negate_result_pp_cell_dot_sum ff_r_dot_mcp_ics_negate_result_pp_cell_dot_sum ff_s_dot_mcp_ics_negate_result_pp_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_negate_result_pp_cell_dot_sum_summand. ff_h_dot_mcp_ics_negate_result_pp_cell_dot_sum_summand + S (ff_a_dot_mcp_ics_negate_result_pp_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_negate_result_pp_cell_dot_sum)) * ff_scale_dot_mcp_ics_negate_result_pp_cell_dot)) /\ exists ff_q_dot_mcp_ics_negate_result_pp_cell_dot_sum_summand. ff_code_dot_mcp_ics_negate_result_pp_cell_dot = ff_q_dot_mcp_ics_negate_result_pp_cell_dot_sum_summand * S ((S (ff_i_dot_mcp_ics_negate_result_pp_cell_dot_sum)) * ff_scale_dot_mcp_ics_negate_result_pp_cell_dot) + (ff_a_dot_mcp_ics_negate_result_pp_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_negate_result_pp_cell_dot_sum_partial. ff_h_dot_mcp_ics_negate_result_pp_cell_dot_sum_partial + S (ff_r_dot_mcp_ics_negate_result_pp_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_negate_result_pp_cell_dot_sum)) * ff_v_dot_mcp_ics_negate_result_pp_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_negate_result_pp_cell_dot_sum_partial. ff_u_dot_mcp_ics_negate_result_pp_cell_dot_sum = ff_q_dot_mcp_ics_negate_result_pp_cell_dot_sum_partial * S ((S (ff_i_dot_mcp_ics_negate_result_pp_cell_dot_sum)) * ff_v_dot_mcp_ics_negate_result_pp_cell_dot_sum) + (ff_r_dot_mcp_ics_negate_result_pp_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_negate_result_pp_cell_dot_sum_successor. ff_h_dot_mcp_ics_negate_result_pp_cell_dot_sum_successor + S (ff_s_dot_mcp_ics_negate_result_pp_cell_dot_sum) = S ((S (S ff_i_dot_mcp_ics_negate_result_pp_cell_dot_sum)) * ff_v_dot_mcp_ics_negate_result_pp_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_negate_result_pp_cell_dot_sum_successor. ff_u_dot_mcp_ics_negate_result_pp_cell_dot_sum = ff_q_dot_mcp_ics_negate_result_pp_cell_dot_sum_successor * S ((S (S ff_i_dot_mcp_ics_negate_result_pp_cell_dot_sum)) * ff_v_dot_mcp_ics_negate_result_pp_cell_dot_sum) + (ff_s_dot_mcp_ics_negate_result_pp_cell_dot_sum))) /\ ff_s_dot_mcp_ics_negate_result_pp_cell_dot_sum = ff_r_dot_mcp_ics_negate_result_pp_cell_dot_sum + ff_a_dot_mcp_ics_negate_result_pp_cell_dot_sum))))))))))) /\ (((exists fs_h_mcp_ics_negate_result_pp_entry. fs_h_mcp_ics_negate_result_pp_entry + S (ff_value_mcp_prefix_ics_negate_result_pp) = S ((S (ff_index_mcp_prefix_ics_negate_result_pp)) * ff_pps_mcp_smatrix_ics_negate_result)) /\ exists fs_q_mcp_ics_negate_result_pp_entry. ff_pp_mcp_smatrix_ics_negate_result = fs_q_mcp_ics_negate_result_pp_entry * S ((S (ff_index_mcp_prefix_ics_negate_result_pp)) * ff_pps_mcp_smatrix_ics_negate_result) + (ff_value_mcp_prefix_ics_negate_result_pp))))))) /\ ((forall ff_index_mcp_prefix_ics_negate_result_nn. (exists mcp_gap_ics_negate_result_nn_index. mcp_gap_ics_negate_result_nn_index + S (ff_index_mcp_prefix_ics_negate_result_nn) = ((r) * (1))) -> exists ff_row_mcp_prefix_ics_negate_result_nn ff_column_mcp_prefix_ics_negate_result_nn ff_value_mcp_prefix_ics_negate_result_nn. ((ff_index_mcp_prefix_ics_negate_result_nn) = (1) * ff_row_mcp_prefix_ics_negate_result_nn + ff_column_mcp_prefix_ics_negate_result_nn /\ ((exists mcp_gap_ics_negate_result_nn_column. mcp_gap_ics_negate_result_nn_column + S (ff_column_mcp_prefix_ics_negate_result_nn) = (1)) /\ ((exists ff_left_mcp_cell_ics_negate_result_nn_cell ff_left_scale_mcp_cell_ics_negate_result_nn_cell ff_right_mcp_cell_ics_negate_result_nn_cell ff_right_scale_mcp_cell_ics_negate_result_nn_cell. ((forall ff_index_mcp_ics_negate_result_nn_cell_row ff_source_mcp_ics_negate_result_nn_cell_row ff_target_mcp_ics_negate_result_nn_cell_row. (exists mcp_gap_ics_negate_result_nn_cell_row_bound. mcp_gap_ics_negate_result_nn_cell_row_bound + S (ff_index_mcp_ics_negate_result_nn_cell_row) = (w)) -> (((exists fs_h_mcp_ics_negate_result_nn_cell_row_source. fs_h_mcp_ics_negate_result_nn_cell_row_source + S (ff_source_mcp_ics_negate_result_nn_cell_row) = S ((S (((ff_row_mcp_prefix_ics_negate_result_nn) * (w)) + (1) * ff_index_mcp_ics_negate_result_nn_cell_row)) * dc)) /\ exists fs_q_mcp_ics_negate_result_nn_cell_row_source. db = fs_q_mcp_ics_negate_result_nn_cell_row_source * S ((S (((ff_row_mcp_prefix_ics_negate_result_nn) * (w)) + (1) * ff_index_mcp_ics_negate_result_nn_cell_row)) * dc) + (ff_source_mcp_ics_negate_result_nn_cell_row))) -> (((exists fs_h_mcp_ics_negate_result_nn_cell_row_target. fs_h_mcp_ics_negate_result_nn_cell_row_target + S (ff_target_mcp_ics_negate_result_nn_cell_row) = S ((S (ff_index_mcp_ics_negate_result_nn_cell_row)) * ff_left_scale_mcp_cell_ics_negate_result_nn_cell)) /\ exists fs_q_mcp_ics_negate_result_nn_cell_row_target. ff_left_mcp_cell_ics_negate_result_nn_cell = fs_q_mcp_ics_negate_result_nn_cell_row_target * S ((S (ff_index_mcp_ics_negate_result_nn_cell_row)) * ff_left_scale_mcp_cell_ics_negate_result_nn_cell) + (ff_target_mcp_ics_negate_result_nn_cell_row))) -> ff_target_mcp_ics_negate_result_nn_cell_row = ff_source_mcp_ics_negate_result_nn_cell_row) /\ ((forall ff_index_mcp_ics_negate_result_nn_cell_column ff_source_mcp_ics_negate_result_nn_cell_column ff_target_mcp_ics_negate_result_nn_cell_column. (exists mcp_gap_ics_negate_result_nn_cell_column_bound. mcp_gap_ics_negate_result_nn_cell_column_bound + S (ff_index_mcp_ics_negate_result_nn_cell_column) = (w)) -> (((exists fs_h_mcp_ics_negate_result_nn_cell_column_source. fs_h_mcp_ics_negate_result_nn_cell_column_source + S (ff_source_mcp_ics_negate_result_nn_cell_column) = S ((S ((ff_column_mcp_prefix_ics_negate_result_nn) + (1) * ff_index_mcp_ics_negate_result_nn_cell_column)) * ec)) /\ exists fs_q_mcp_ics_negate_result_nn_cell_column_source. eb = fs_q_mcp_ics_negate_result_nn_cell_column_source * S ((S ((ff_column_mcp_prefix_ics_negate_result_nn) + (1) * ff_index_mcp_ics_negate_result_nn_cell_column)) * ec) + (ff_source_mcp_ics_negate_result_nn_cell_column))) -> (((exists fs_h_mcp_ics_negate_result_nn_cell_column_target. fs_h_mcp_ics_negate_result_nn_cell_column_target + S (ff_target_mcp_ics_negate_result_nn_cell_column) = S ((S (ff_index_mcp_ics_negate_result_nn_cell_column)) * ff_right_scale_mcp_cell_ics_negate_result_nn_cell)) /\ exists fs_q_mcp_ics_negate_result_nn_cell_column_target. ff_right_mcp_cell_ics_negate_result_nn_cell = fs_q_mcp_ics_negate_result_nn_cell_column_target * S ((S (ff_index_mcp_ics_negate_result_nn_cell_column)) * ff_right_scale_mcp_cell_ics_negate_result_nn_cell) + (ff_target_mcp_ics_negate_result_nn_cell_column))) -> ff_target_mcp_ics_negate_result_nn_cell_column = ff_source_mcp_ics_negate_result_nn_cell_column) /\ (exists ff_code_dot_mcp_ics_negate_result_nn_cell_dot ff_scale_dot_mcp_ics_negate_result_nn_cell_dot. ((forall fpmp_index_dot_mcp_ics_negate_result_nn_cell_dot_pointwise fpmp_left_dot_mcp_ics_negate_result_nn_cell_dot_pointwise fpmp_right_dot_mcp_ics_negate_result_nn_cell_dot_pointwise fpmp_target_dot_mcp_ics_negate_result_nn_cell_dot_pointwise. (exists fpmp_gap_dot_mcp_ics_negate_result_nn_cell_dot_pointwise. fpmp_gap_dot_mcp_ics_negate_result_nn_cell_dot_pointwise + S fpmp_index_dot_mcp_ics_negate_result_nn_cell_dot_pointwise = w) -> (((exists ff_h_fpmp_dot_mcp_ics_negate_result_nn_cell_dot_pointwise_left. ff_h_fpmp_dot_mcp_ics_negate_result_nn_cell_dot_pointwise_left + S (fpmp_left_dot_mcp_ics_negate_result_nn_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_negate_result_nn_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_negate_result_nn_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_negate_result_nn_cell_dot_pointwise_left. ff_left_mcp_cell_ics_negate_result_nn_cell = ff_q_fpmp_dot_mcp_ics_negate_result_nn_cell_dot_pointwise_left * S ((S (fpmp_index_dot_mcp_ics_negate_result_nn_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_negate_result_nn_cell) + (fpmp_left_dot_mcp_ics_negate_result_nn_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_negate_result_nn_cell_dot_pointwise_right. ff_h_fpmp_dot_mcp_ics_negate_result_nn_cell_dot_pointwise_right + S (fpmp_right_dot_mcp_ics_negate_result_nn_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_negate_result_nn_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_negate_result_nn_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_negate_result_nn_cell_dot_pointwise_right. ff_right_mcp_cell_ics_negate_result_nn_cell = ff_q_fpmp_dot_mcp_ics_negate_result_nn_cell_dot_pointwise_right * S ((S (fpmp_index_dot_mcp_ics_negate_result_nn_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_negate_result_nn_cell) + (fpmp_right_dot_mcp_ics_negate_result_nn_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_negate_result_nn_cell_dot_pointwise_target. ff_h_fpmp_dot_mcp_ics_negate_result_nn_cell_dot_pointwise_target + S (fpmp_target_dot_mcp_ics_negate_result_nn_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_negate_result_nn_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_negate_result_nn_cell_dot)) /\ exists ff_q_fpmp_dot_mcp_ics_negate_result_nn_cell_dot_pointwise_target. ff_code_dot_mcp_ics_negate_result_nn_cell_dot = ff_q_fpmp_dot_mcp_ics_negate_result_nn_cell_dot_pointwise_target * S ((S (fpmp_index_dot_mcp_ics_negate_result_nn_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_negate_result_nn_cell_dot) + (fpmp_target_dot_mcp_ics_negate_result_nn_cell_dot_pointwise))) -> fpmp_target_dot_mcp_ics_negate_result_nn_cell_dot_pointwise = fpmp_left_dot_mcp_ics_negate_result_nn_cell_dot_pointwise * fpmp_right_dot_mcp_ics_negate_result_nn_cell_dot_pointwise) /\ (exists ff_u_dot_mcp_ics_negate_result_nn_cell_dot_sum ff_v_dot_mcp_ics_negate_result_nn_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_negate_result_nn_cell_dot_sum_start. ff_h_dot_mcp_ics_negate_result_nn_cell_dot_sum_start + S (0) = S ((S (0)) * ff_v_dot_mcp_ics_negate_result_nn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_negate_result_nn_cell_dot_sum_start. ff_u_dot_mcp_ics_negate_result_nn_cell_dot_sum = ff_q_dot_mcp_ics_negate_result_nn_cell_dot_sum_start * S ((S (0)) * ff_v_dot_mcp_ics_negate_result_nn_cell_dot_sum) + (0))) /\ ((((exists ff_h_dot_mcp_ics_negate_result_nn_cell_dot_sum_terminal. ff_h_dot_mcp_ics_negate_result_nn_cell_dot_sum_terminal + S (ff_value_mcp_prefix_ics_negate_result_nn) = S ((S (w)) * ff_v_dot_mcp_ics_negate_result_nn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_negate_result_nn_cell_dot_sum_terminal. ff_u_dot_mcp_ics_negate_result_nn_cell_dot_sum = ff_q_dot_mcp_ics_negate_result_nn_cell_dot_sum_terminal * S ((S (w)) * ff_v_dot_mcp_ics_negate_result_nn_cell_dot_sum) + (ff_value_mcp_prefix_ics_negate_result_nn))) /\ forall ff_i_dot_mcp_ics_negate_result_nn_cell_dot_sum. (exists ff_lt_dot_mcp_ics_negate_result_nn_cell_dot_sum_bound. ff_lt_dot_mcp_ics_negate_result_nn_cell_dot_sum_bound + S ff_i_dot_mcp_ics_negate_result_nn_cell_dot_sum = w) -> exists ff_a_dot_mcp_ics_negate_result_nn_cell_dot_sum ff_r_dot_mcp_ics_negate_result_nn_cell_dot_sum ff_s_dot_mcp_ics_negate_result_nn_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_negate_result_nn_cell_dot_sum_summand. ff_h_dot_mcp_ics_negate_result_nn_cell_dot_sum_summand + S (ff_a_dot_mcp_ics_negate_result_nn_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_negate_result_nn_cell_dot_sum)) * ff_scale_dot_mcp_ics_negate_result_nn_cell_dot)) /\ exists ff_q_dot_mcp_ics_negate_result_nn_cell_dot_sum_summand. ff_code_dot_mcp_ics_negate_result_nn_cell_dot = ff_q_dot_mcp_ics_negate_result_nn_cell_dot_sum_summand * S ((S (ff_i_dot_mcp_ics_negate_result_nn_cell_dot_sum)) * ff_scale_dot_mcp_ics_negate_result_nn_cell_dot) + (ff_a_dot_mcp_ics_negate_result_nn_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_negate_result_nn_cell_dot_sum_partial. ff_h_dot_mcp_ics_negate_result_nn_cell_dot_sum_partial + S (ff_r_dot_mcp_ics_negate_result_nn_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_negate_result_nn_cell_dot_sum)) * ff_v_dot_mcp_ics_negate_result_nn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_negate_result_nn_cell_dot_sum_partial. ff_u_dot_mcp_ics_negate_result_nn_cell_dot_sum = ff_q_dot_mcp_ics_negate_result_nn_cell_dot_sum_partial * S ((S (ff_i_dot_mcp_ics_negate_result_nn_cell_dot_sum)) * ff_v_dot_mcp_ics_negate_result_nn_cell_dot_sum) + (ff_r_dot_mcp_ics_negate_result_nn_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_negate_result_nn_cell_dot_sum_successor. ff_h_dot_mcp_ics_negate_result_nn_cell_dot_sum_successor + S (ff_s_dot_mcp_ics_negate_result_nn_cell_dot_sum) = S ((S (S ff_i_dot_mcp_ics_negate_result_nn_cell_dot_sum)) * ff_v_dot_mcp_ics_negate_result_nn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_negate_result_nn_cell_dot_sum_successor. ff_u_dot_mcp_ics_negate_result_nn_cell_dot_sum = ff_q_dot_mcp_ics_negate_result_nn_cell_dot_sum_successor * S ((S (S ff_i_dot_mcp_ics_negate_result_nn_cell_dot_sum)) * ff_v_dot_mcp_ics_negate_result_nn_cell_dot_sum) + (ff_s_dot_mcp_ics_negate_result_nn_cell_dot_sum))) /\ ff_s_dot_mcp_ics_negate_result_nn_cell_dot_sum = ff_r_dot_mcp_ics_negate_result_nn_cell_dot_sum + ff_a_dot_mcp_ics_negate_result_nn_cell_dot_sum))))))))))) /\ (((exists fs_h_mcp_ics_negate_result_nn_entry. fs_h_mcp_ics_negate_result_nn_entry + S (ff_value_mcp_prefix_ics_negate_result_nn) = S ((S (ff_index_mcp_prefix_ics_negate_result_nn)) * ff_nns_mcp_smatrix_ics_negate_result)) /\ exists fs_q_mcp_ics_negate_result_nn_entry. ff_nn_mcp_smatrix_ics_negate_result = fs_q_mcp_ics_negate_result_nn_entry * S ((S (ff_index_mcp_prefix_ics_negate_result_nn)) * ff_nns_mcp_smatrix_ics_negate_result) + (ff_value_mcp_prefix_ics_negate_result_nn))))))) /\ ((forall ff_index_mcp_prefix_ics_negate_result_pn. (exists mcp_gap_ics_negate_result_pn_index. mcp_gap_ics_negate_result_pn_index + S (ff_index_mcp_prefix_ics_negate_result_pn) = ((r) * (1))) -> exists ff_row_mcp_prefix_ics_negate_result_pn ff_column_mcp_prefix_ics_negate_result_pn ff_value_mcp_prefix_ics_negate_result_pn. ((ff_index_mcp_prefix_ics_negate_result_pn) = (1) * ff_row_mcp_prefix_ics_negate_result_pn + ff_column_mcp_prefix_ics_negate_result_pn /\ ((exists mcp_gap_ics_negate_result_pn_column. mcp_gap_ics_negate_result_pn_column + S (ff_column_mcp_prefix_ics_negate_result_pn) = (1)) /\ ((exists ff_left_mcp_cell_ics_negate_result_pn_cell ff_left_scale_mcp_cell_ics_negate_result_pn_cell ff_right_mcp_cell_ics_negate_result_pn_cell ff_right_scale_mcp_cell_ics_negate_result_pn_cell. ((forall ff_index_mcp_ics_negate_result_pn_cell_row ff_source_mcp_ics_negate_result_pn_cell_row ff_target_mcp_ics_negate_result_pn_cell_row. (exists mcp_gap_ics_negate_result_pn_cell_row_bound. mcp_gap_ics_negate_result_pn_cell_row_bound + S (ff_index_mcp_ics_negate_result_pn_cell_row) = (w)) -> (((exists fs_h_mcp_ics_negate_result_pn_cell_row_source. fs_h_mcp_ics_negate_result_pn_cell_row_source + S (ff_source_mcp_ics_negate_result_pn_cell_row) = S ((S (((ff_row_mcp_prefix_ics_negate_result_pn) * (w)) + (1) * ff_index_mcp_ics_negate_result_pn_cell_row)) * ac)) /\ exists fs_q_mcp_ics_negate_result_pn_cell_row_source. ab = fs_q_mcp_ics_negate_result_pn_cell_row_source * S ((S (((ff_row_mcp_prefix_ics_negate_result_pn) * (w)) + (1) * ff_index_mcp_ics_negate_result_pn_cell_row)) * ac) + (ff_source_mcp_ics_negate_result_pn_cell_row))) -> (((exists fs_h_mcp_ics_negate_result_pn_cell_row_target. fs_h_mcp_ics_negate_result_pn_cell_row_target + S (ff_target_mcp_ics_negate_result_pn_cell_row) = S ((S (ff_index_mcp_ics_negate_result_pn_cell_row)) * ff_left_scale_mcp_cell_ics_negate_result_pn_cell)) /\ exists fs_q_mcp_ics_negate_result_pn_cell_row_target. ff_left_mcp_cell_ics_negate_result_pn_cell = fs_q_mcp_ics_negate_result_pn_cell_row_target * S ((S (ff_index_mcp_ics_negate_result_pn_cell_row)) * ff_left_scale_mcp_cell_ics_negate_result_pn_cell) + (ff_target_mcp_ics_negate_result_pn_cell_row))) -> ff_target_mcp_ics_negate_result_pn_cell_row = ff_source_mcp_ics_negate_result_pn_cell_row) /\ ((forall ff_index_mcp_ics_negate_result_pn_cell_column ff_source_mcp_ics_negate_result_pn_cell_column ff_target_mcp_ics_negate_result_pn_cell_column. (exists mcp_gap_ics_negate_result_pn_cell_column_bound. mcp_gap_ics_negate_result_pn_cell_column_bound + S (ff_index_mcp_ics_negate_result_pn_cell_column) = (w)) -> (((exists fs_h_mcp_ics_negate_result_pn_cell_column_source. fs_h_mcp_ics_negate_result_pn_cell_column_source + S (ff_source_mcp_ics_negate_result_pn_cell_column) = S ((S ((ff_column_mcp_prefix_ics_negate_result_pn) + (1) * ff_index_mcp_ics_negate_result_pn_cell_column)) * ec)) /\ exists fs_q_mcp_ics_negate_result_pn_cell_column_source. eb = fs_q_mcp_ics_negate_result_pn_cell_column_source * S ((S ((ff_column_mcp_prefix_ics_negate_result_pn) + (1) * ff_index_mcp_ics_negate_result_pn_cell_column)) * ec) + (ff_source_mcp_ics_negate_result_pn_cell_column))) -> (((exists fs_h_mcp_ics_negate_result_pn_cell_column_target. fs_h_mcp_ics_negate_result_pn_cell_column_target + S (ff_target_mcp_ics_negate_result_pn_cell_column) = S ((S (ff_index_mcp_ics_negate_result_pn_cell_column)) * ff_right_scale_mcp_cell_ics_negate_result_pn_cell)) /\ exists fs_q_mcp_ics_negate_result_pn_cell_column_target. ff_right_mcp_cell_ics_negate_result_pn_cell = fs_q_mcp_ics_negate_result_pn_cell_column_target * S ((S (ff_index_mcp_ics_negate_result_pn_cell_column)) * ff_right_scale_mcp_cell_ics_negate_result_pn_cell) + (ff_target_mcp_ics_negate_result_pn_cell_column))) -> ff_target_mcp_ics_negate_result_pn_cell_column = ff_source_mcp_ics_negate_result_pn_cell_column) /\ (exists ff_code_dot_mcp_ics_negate_result_pn_cell_dot ff_scale_dot_mcp_ics_negate_result_pn_cell_dot. ((forall fpmp_index_dot_mcp_ics_negate_result_pn_cell_dot_pointwise fpmp_left_dot_mcp_ics_negate_result_pn_cell_dot_pointwise fpmp_right_dot_mcp_ics_negate_result_pn_cell_dot_pointwise fpmp_target_dot_mcp_ics_negate_result_pn_cell_dot_pointwise. (exists fpmp_gap_dot_mcp_ics_negate_result_pn_cell_dot_pointwise. fpmp_gap_dot_mcp_ics_negate_result_pn_cell_dot_pointwise + S fpmp_index_dot_mcp_ics_negate_result_pn_cell_dot_pointwise = w) -> (((exists ff_h_fpmp_dot_mcp_ics_negate_result_pn_cell_dot_pointwise_left. ff_h_fpmp_dot_mcp_ics_negate_result_pn_cell_dot_pointwise_left + S (fpmp_left_dot_mcp_ics_negate_result_pn_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_negate_result_pn_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_negate_result_pn_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_negate_result_pn_cell_dot_pointwise_left. ff_left_mcp_cell_ics_negate_result_pn_cell = ff_q_fpmp_dot_mcp_ics_negate_result_pn_cell_dot_pointwise_left * S ((S (fpmp_index_dot_mcp_ics_negate_result_pn_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_negate_result_pn_cell) + (fpmp_left_dot_mcp_ics_negate_result_pn_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_negate_result_pn_cell_dot_pointwise_right. ff_h_fpmp_dot_mcp_ics_negate_result_pn_cell_dot_pointwise_right + S (fpmp_right_dot_mcp_ics_negate_result_pn_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_negate_result_pn_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_negate_result_pn_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_negate_result_pn_cell_dot_pointwise_right. ff_right_mcp_cell_ics_negate_result_pn_cell = ff_q_fpmp_dot_mcp_ics_negate_result_pn_cell_dot_pointwise_right * S ((S (fpmp_index_dot_mcp_ics_negate_result_pn_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_negate_result_pn_cell) + (fpmp_right_dot_mcp_ics_negate_result_pn_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_negate_result_pn_cell_dot_pointwise_target. ff_h_fpmp_dot_mcp_ics_negate_result_pn_cell_dot_pointwise_target + S (fpmp_target_dot_mcp_ics_negate_result_pn_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_negate_result_pn_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_negate_result_pn_cell_dot)) /\ exists ff_q_fpmp_dot_mcp_ics_negate_result_pn_cell_dot_pointwise_target. ff_code_dot_mcp_ics_negate_result_pn_cell_dot = ff_q_fpmp_dot_mcp_ics_negate_result_pn_cell_dot_pointwise_target * S ((S (fpmp_index_dot_mcp_ics_negate_result_pn_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_negate_result_pn_cell_dot) + (fpmp_target_dot_mcp_ics_negate_result_pn_cell_dot_pointwise))) -> fpmp_target_dot_mcp_ics_negate_result_pn_cell_dot_pointwise = fpmp_left_dot_mcp_ics_negate_result_pn_cell_dot_pointwise * fpmp_right_dot_mcp_ics_negate_result_pn_cell_dot_pointwise) /\ (exists ff_u_dot_mcp_ics_negate_result_pn_cell_dot_sum ff_v_dot_mcp_ics_negate_result_pn_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_negate_result_pn_cell_dot_sum_start. ff_h_dot_mcp_ics_negate_result_pn_cell_dot_sum_start + S (0) = S ((S (0)) * ff_v_dot_mcp_ics_negate_result_pn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_negate_result_pn_cell_dot_sum_start. ff_u_dot_mcp_ics_negate_result_pn_cell_dot_sum = ff_q_dot_mcp_ics_negate_result_pn_cell_dot_sum_start * S ((S (0)) * ff_v_dot_mcp_ics_negate_result_pn_cell_dot_sum) + (0))) /\ ((((exists ff_h_dot_mcp_ics_negate_result_pn_cell_dot_sum_terminal. ff_h_dot_mcp_ics_negate_result_pn_cell_dot_sum_terminal + S (ff_value_mcp_prefix_ics_negate_result_pn) = S ((S (w)) * ff_v_dot_mcp_ics_negate_result_pn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_negate_result_pn_cell_dot_sum_terminal. ff_u_dot_mcp_ics_negate_result_pn_cell_dot_sum = ff_q_dot_mcp_ics_negate_result_pn_cell_dot_sum_terminal * S ((S (w)) * ff_v_dot_mcp_ics_negate_result_pn_cell_dot_sum) + (ff_value_mcp_prefix_ics_negate_result_pn))) /\ forall ff_i_dot_mcp_ics_negate_result_pn_cell_dot_sum. (exists ff_lt_dot_mcp_ics_negate_result_pn_cell_dot_sum_bound. ff_lt_dot_mcp_ics_negate_result_pn_cell_dot_sum_bound + S ff_i_dot_mcp_ics_negate_result_pn_cell_dot_sum = w) -> exists ff_a_dot_mcp_ics_negate_result_pn_cell_dot_sum ff_r_dot_mcp_ics_negate_result_pn_cell_dot_sum ff_s_dot_mcp_ics_negate_result_pn_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_negate_result_pn_cell_dot_sum_summand. ff_h_dot_mcp_ics_negate_result_pn_cell_dot_sum_summand + S (ff_a_dot_mcp_ics_negate_result_pn_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_negate_result_pn_cell_dot_sum)) * ff_scale_dot_mcp_ics_negate_result_pn_cell_dot)) /\ exists ff_q_dot_mcp_ics_negate_result_pn_cell_dot_sum_summand. ff_code_dot_mcp_ics_negate_result_pn_cell_dot = ff_q_dot_mcp_ics_negate_result_pn_cell_dot_sum_summand * S ((S (ff_i_dot_mcp_ics_negate_result_pn_cell_dot_sum)) * ff_scale_dot_mcp_ics_negate_result_pn_cell_dot) + (ff_a_dot_mcp_ics_negate_result_pn_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_negate_result_pn_cell_dot_sum_partial. ff_h_dot_mcp_ics_negate_result_pn_cell_dot_sum_partial + S (ff_r_dot_mcp_ics_negate_result_pn_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_negate_result_pn_cell_dot_sum)) * ff_v_dot_mcp_ics_negate_result_pn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_negate_result_pn_cell_dot_sum_partial. ff_u_dot_mcp_ics_negate_result_pn_cell_dot_sum = ff_q_dot_mcp_ics_negate_result_pn_cell_dot_sum_partial * S ((S (ff_i_dot_mcp_ics_negate_result_pn_cell_dot_sum)) * ff_v_dot_mcp_ics_negate_result_pn_cell_dot_sum) + (ff_r_dot_mcp_ics_negate_result_pn_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_negate_result_pn_cell_dot_sum_successor. ff_h_dot_mcp_ics_negate_result_pn_cell_dot_sum_successor + S (ff_s_dot_mcp_ics_negate_result_pn_cell_dot_sum) = S ((S (S ff_i_dot_mcp_ics_negate_result_pn_cell_dot_sum)) * ff_v_dot_mcp_ics_negate_result_pn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_negate_result_pn_cell_dot_sum_successor. ff_u_dot_mcp_ics_negate_result_pn_cell_dot_sum = ff_q_dot_mcp_ics_negate_result_pn_cell_dot_sum_successor * S ((S (S ff_i_dot_mcp_ics_negate_result_pn_cell_dot_sum)) * ff_v_dot_mcp_ics_negate_result_pn_cell_dot_sum) + (ff_s_dot_mcp_ics_negate_result_pn_cell_dot_sum))) /\ ff_s_dot_mcp_ics_negate_result_pn_cell_dot_sum = ff_r_dot_mcp_ics_negate_result_pn_cell_dot_sum + ff_a_dot_mcp_ics_negate_result_pn_cell_dot_sum))))))))))) /\ (((exists fs_h_mcp_ics_negate_result_pn_entry. fs_h_mcp_ics_negate_result_pn_entry + S (ff_value_mcp_prefix_ics_negate_result_pn) = S ((S (ff_index_mcp_prefix_ics_negate_result_pn)) * ff_pns_mcp_smatrix_ics_negate_result)) /\ exists fs_q_mcp_ics_negate_result_pn_entry. ff_pn_mcp_smatrix_ics_negate_result = fs_q_mcp_ics_negate_result_pn_entry * S ((S (ff_index_mcp_prefix_ics_negate_result_pn)) * ff_pns_mcp_smatrix_ics_negate_result) + (ff_value_mcp_prefix_ics_negate_result_pn))))))) /\ ((forall ff_index_mcp_prefix_ics_negate_result_np. (exists mcp_gap_ics_negate_result_np_index. mcp_gap_ics_negate_result_np_index + S (ff_index_mcp_prefix_ics_negate_result_np) = ((r) * (1))) -> exists ff_row_mcp_prefix_ics_negate_result_np ff_column_mcp_prefix_ics_negate_result_np ff_value_mcp_prefix_ics_negate_result_np. ((ff_index_mcp_prefix_ics_negate_result_np) = (1) * ff_row_mcp_prefix_ics_negate_result_np + ff_column_mcp_prefix_ics_negate_result_np /\ ((exists mcp_gap_ics_negate_result_np_column. mcp_gap_ics_negate_result_np_column + S (ff_column_mcp_prefix_ics_negate_result_np) = (1)) /\ ((exists ff_left_mcp_cell_ics_negate_result_np_cell ff_left_scale_mcp_cell_ics_negate_result_np_cell ff_right_mcp_cell_ics_negate_result_np_cell ff_right_scale_mcp_cell_ics_negate_result_np_cell. ((forall ff_index_mcp_ics_negate_result_np_cell_row ff_source_mcp_ics_negate_result_np_cell_row ff_target_mcp_ics_negate_result_np_cell_row. (exists mcp_gap_ics_negate_result_np_cell_row_bound. mcp_gap_ics_negate_result_np_cell_row_bound + S (ff_index_mcp_ics_negate_result_np_cell_row) = (w)) -> (((exists fs_h_mcp_ics_negate_result_np_cell_row_source. fs_h_mcp_ics_negate_result_np_cell_row_source + S (ff_source_mcp_ics_negate_result_np_cell_row) = S ((S (((ff_row_mcp_prefix_ics_negate_result_np) * (w)) + (1) * ff_index_mcp_ics_negate_result_np_cell_row)) * dc)) /\ exists fs_q_mcp_ics_negate_result_np_cell_row_source. db = fs_q_mcp_ics_negate_result_np_cell_row_source * S ((S (((ff_row_mcp_prefix_ics_negate_result_np) * (w)) + (1) * ff_index_mcp_ics_negate_result_np_cell_row)) * dc) + (ff_source_mcp_ics_negate_result_np_cell_row))) -> (((exists fs_h_mcp_ics_negate_result_np_cell_row_target. fs_h_mcp_ics_negate_result_np_cell_row_target + S (ff_target_mcp_ics_negate_result_np_cell_row) = S ((S (ff_index_mcp_ics_negate_result_np_cell_row)) * ff_left_scale_mcp_cell_ics_negate_result_np_cell)) /\ exists fs_q_mcp_ics_negate_result_np_cell_row_target. ff_left_mcp_cell_ics_negate_result_np_cell = fs_q_mcp_ics_negate_result_np_cell_row_target * S ((S (ff_index_mcp_ics_negate_result_np_cell_row)) * ff_left_scale_mcp_cell_ics_negate_result_np_cell) + (ff_target_mcp_ics_negate_result_np_cell_row))) -> ff_target_mcp_ics_negate_result_np_cell_row = ff_source_mcp_ics_negate_result_np_cell_row) /\ ((forall ff_index_mcp_ics_negate_result_np_cell_column ff_source_mcp_ics_negate_result_np_cell_column ff_target_mcp_ics_negate_result_np_cell_column. (exists mcp_gap_ics_negate_result_np_cell_column_bound. mcp_gap_ics_negate_result_np_cell_column_bound + S (ff_index_mcp_ics_negate_result_np_cell_column) = (w)) -> (((exists fs_h_mcp_ics_negate_result_np_cell_column_source. fs_h_mcp_ics_negate_result_np_cell_column_source + S (ff_source_mcp_ics_negate_result_np_cell_column) = S ((S ((ff_column_mcp_prefix_ics_negate_result_np) + (1) * ff_index_mcp_ics_negate_result_np_cell_column)) * fc)) /\ exists fs_q_mcp_ics_negate_result_np_cell_column_source. fb = fs_q_mcp_ics_negate_result_np_cell_column_source * S ((S ((ff_column_mcp_prefix_ics_negate_result_np) + (1) * ff_index_mcp_ics_negate_result_np_cell_column)) * fc) + (ff_source_mcp_ics_negate_result_np_cell_column))) -> (((exists fs_h_mcp_ics_negate_result_np_cell_column_target. fs_h_mcp_ics_negate_result_np_cell_column_target + S (ff_target_mcp_ics_negate_result_np_cell_column) = S ((S (ff_index_mcp_ics_negate_result_np_cell_column)) * ff_right_scale_mcp_cell_ics_negate_result_np_cell)) /\ exists fs_q_mcp_ics_negate_result_np_cell_column_target. ff_right_mcp_cell_ics_negate_result_np_cell = fs_q_mcp_ics_negate_result_np_cell_column_target * S ((S (ff_index_mcp_ics_negate_result_np_cell_column)) * ff_right_scale_mcp_cell_ics_negate_result_np_cell) + (ff_target_mcp_ics_negate_result_np_cell_column))) -> ff_target_mcp_ics_negate_result_np_cell_column = ff_source_mcp_ics_negate_result_np_cell_column) /\ (exists ff_code_dot_mcp_ics_negate_result_np_cell_dot ff_scale_dot_mcp_ics_negate_result_np_cell_dot. ((forall fpmp_index_dot_mcp_ics_negate_result_np_cell_dot_pointwise fpmp_left_dot_mcp_ics_negate_result_np_cell_dot_pointwise fpmp_right_dot_mcp_ics_negate_result_np_cell_dot_pointwise fpmp_target_dot_mcp_ics_negate_result_np_cell_dot_pointwise. (exists fpmp_gap_dot_mcp_ics_negate_result_np_cell_dot_pointwise. fpmp_gap_dot_mcp_ics_negate_result_np_cell_dot_pointwise + S fpmp_index_dot_mcp_ics_negate_result_np_cell_dot_pointwise = w) -> (((exists ff_h_fpmp_dot_mcp_ics_negate_result_np_cell_dot_pointwise_left. ff_h_fpmp_dot_mcp_ics_negate_result_np_cell_dot_pointwise_left + S (fpmp_left_dot_mcp_ics_negate_result_np_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_negate_result_np_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_negate_result_np_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_negate_result_np_cell_dot_pointwise_left. ff_left_mcp_cell_ics_negate_result_np_cell = ff_q_fpmp_dot_mcp_ics_negate_result_np_cell_dot_pointwise_left * S ((S (fpmp_index_dot_mcp_ics_negate_result_np_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_negate_result_np_cell) + (fpmp_left_dot_mcp_ics_negate_result_np_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_negate_result_np_cell_dot_pointwise_right. ff_h_fpmp_dot_mcp_ics_negate_result_np_cell_dot_pointwise_right + S (fpmp_right_dot_mcp_ics_negate_result_np_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_negate_result_np_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_negate_result_np_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_negate_result_np_cell_dot_pointwise_right. ff_right_mcp_cell_ics_negate_result_np_cell = ff_q_fpmp_dot_mcp_ics_negate_result_np_cell_dot_pointwise_right * S ((S (fpmp_index_dot_mcp_ics_negate_result_np_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_negate_result_np_cell) + (fpmp_right_dot_mcp_ics_negate_result_np_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_negate_result_np_cell_dot_pointwise_target. ff_h_fpmp_dot_mcp_ics_negate_result_np_cell_dot_pointwise_target + S (fpmp_target_dot_mcp_ics_negate_result_np_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_negate_result_np_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_negate_result_np_cell_dot)) /\ exists ff_q_fpmp_dot_mcp_ics_negate_result_np_cell_dot_pointwise_target. ff_code_dot_mcp_ics_negate_result_np_cell_dot = ff_q_fpmp_dot_mcp_ics_negate_result_np_cell_dot_pointwise_target * S ((S (fpmp_index_dot_mcp_ics_negate_result_np_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_negate_result_np_cell_dot) + (fpmp_target_dot_mcp_ics_negate_result_np_cell_dot_pointwise))) -> fpmp_target_dot_mcp_ics_negate_result_np_cell_dot_pointwise = fpmp_left_dot_mcp_ics_negate_result_np_cell_dot_pointwise * fpmp_right_dot_mcp_ics_negate_result_np_cell_dot_pointwise) /\ (exists ff_u_dot_mcp_ics_negate_result_np_cell_dot_sum ff_v_dot_mcp_ics_negate_result_np_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_negate_result_np_cell_dot_sum_start. ff_h_dot_mcp_ics_negate_result_np_cell_dot_sum_start + S (0) = S ((S (0)) * ff_v_dot_mcp_ics_negate_result_np_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_negate_result_np_cell_dot_sum_start. ff_u_dot_mcp_ics_negate_result_np_cell_dot_sum = ff_q_dot_mcp_ics_negate_result_np_cell_dot_sum_start * S ((S (0)) * ff_v_dot_mcp_ics_negate_result_np_cell_dot_sum) + (0))) /\ ((((exists ff_h_dot_mcp_ics_negate_result_np_cell_dot_sum_terminal. ff_h_dot_mcp_ics_negate_result_np_cell_dot_sum_terminal + S (ff_value_mcp_prefix_ics_negate_result_np) = S ((S (w)) * ff_v_dot_mcp_ics_negate_result_np_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_negate_result_np_cell_dot_sum_terminal. ff_u_dot_mcp_ics_negate_result_np_cell_dot_sum = ff_q_dot_mcp_ics_negate_result_np_cell_dot_sum_terminal * S ((S (w)) * ff_v_dot_mcp_ics_negate_result_np_cell_dot_sum) + (ff_value_mcp_prefix_ics_negate_result_np))) /\ forall ff_i_dot_mcp_ics_negate_result_np_cell_dot_sum. (exists ff_lt_dot_mcp_ics_negate_result_np_cell_dot_sum_bound. ff_lt_dot_mcp_ics_negate_result_np_cell_dot_sum_bound + S ff_i_dot_mcp_ics_negate_result_np_cell_dot_sum = w) -> exists ff_a_dot_mcp_ics_negate_result_np_cell_dot_sum ff_r_dot_mcp_ics_negate_result_np_cell_dot_sum ff_s_dot_mcp_ics_negate_result_np_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_negate_result_np_cell_dot_sum_summand. ff_h_dot_mcp_ics_negate_result_np_cell_dot_sum_summand + S (ff_a_dot_mcp_ics_negate_result_np_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_negate_result_np_cell_dot_sum)) * ff_scale_dot_mcp_ics_negate_result_np_cell_dot)) /\ exists ff_q_dot_mcp_ics_negate_result_np_cell_dot_sum_summand. ff_code_dot_mcp_ics_negate_result_np_cell_dot = ff_q_dot_mcp_ics_negate_result_np_cell_dot_sum_summand * S ((S (ff_i_dot_mcp_ics_negate_result_np_cell_dot_sum)) * ff_scale_dot_mcp_ics_negate_result_np_cell_dot) + (ff_a_dot_mcp_ics_negate_result_np_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_negate_result_np_cell_dot_sum_partial. ff_h_dot_mcp_ics_negate_result_np_cell_dot_sum_partial + S (ff_r_dot_mcp_ics_negate_result_np_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_negate_result_np_cell_dot_sum)) * ff_v_dot_mcp_ics_negate_result_np_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_negate_result_np_cell_dot_sum_partial. ff_u_dot_mcp_ics_negate_result_np_cell_dot_sum = ff_q_dot_mcp_ics_negate_result_np_cell_dot_sum_partial * S ((S (ff_i_dot_mcp_ics_negate_result_np_cell_dot_sum)) * ff_v_dot_mcp_ics_negate_result_np_cell_dot_sum) + (ff_r_dot_mcp_ics_negate_result_np_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_negate_result_np_cell_dot_sum_successor. ff_h_dot_mcp_ics_negate_result_np_cell_dot_sum_successor + S (ff_s_dot_mcp_ics_negate_result_np_cell_dot_sum) = S ((S (S ff_i_dot_mcp_ics_negate_result_np_cell_dot_sum)) * ff_v_dot_mcp_ics_negate_result_np_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_negate_result_np_cell_dot_sum_successor. ff_u_dot_mcp_ics_negate_result_np_cell_dot_sum = ff_q_dot_mcp_ics_negate_result_np_cell_dot_sum_successor * S ((S (S ff_i_dot_mcp_ics_negate_result_np_cell_dot_sum)) * ff_v_dot_mcp_ics_negate_result_np_cell_dot_sum) + (ff_s_dot_mcp_ics_negate_result_np_cell_dot_sum))) /\ ff_s_dot_mcp_ics_negate_result_np_cell_dot_sum = ff_r_dot_mcp_ics_negate_result_np_cell_dot_sum + ff_a_dot_mcp_ics_negate_result_np_cell_dot_sum))))))))))) /\ (((exists fs_h_mcp_ics_negate_result_np_entry. fs_h_mcp_ics_negate_result_np_entry + S (ff_value_mcp_prefix_ics_negate_result_np) = S ((S (ff_index_mcp_prefix_ics_negate_result_np)) * ff_nps_mcp_smatrix_ics_negate_result)) /\ exists fs_q_mcp_ics_negate_result_np_entry. ff_np_mcp_smatrix_ics_negate_result = fs_q_mcp_ics_negate_result_np_entry * S ((S (ff_index_mcp_prefix_ics_negate_result_np)) * ff_nps_mcp_smatrix_ics_negate_result) + (ff_value_mcp_prefix_ics_negate_result_np))))))) /\ ((forall ff_index_mcp_add_ics_negate_result_positive ff_left_mcp_add_ics_negate_result_positive ff_right_mcp_add_ics_negate_result_positive ff_target_mcp_add_ics_negate_result_positive. (exists mcp_gap_ics_negate_result_positive_bound. mcp_gap_ics_negate_result_positive_bound + S (ff_index_mcp_add_ics_negate_result_positive) = ((r) * (1))) -> (((exists fs_h_mcp_ics_negate_result_positive_left. fs_h_mcp_ics_negate_result_positive_left + S (ff_left_mcp_add_ics_negate_result_positive) = S ((S (ff_index_mcp_add_ics_negate_result_positive)) * ff_pps_mcp_smatrix_ics_negate_result)) /\ exists fs_q_mcp_ics_negate_result_positive_left. ff_pp_mcp_smatrix_ics_negate_result = fs_q_mcp_ics_negate_result_positive_left * S ((S (ff_index_mcp_add_ics_negate_result_positive)) * ff_pps_mcp_smatrix_ics_negate_result) + (ff_left_mcp_add_ics_negate_result_positive))) -> (((exists fs_h_mcp_ics_negate_result_positive_right. fs_h_mcp_ics_negate_result_positive_right + S (ff_right_mcp_add_ics_negate_result_positive) = S ((S (ff_index_mcp_add_ics_negate_result_positive)) * ff_nns_mcp_smatrix_ics_negate_result)) /\ exists fs_q_mcp_ics_negate_result_positive_right. ff_nn_mcp_smatrix_ics_negate_result = fs_q_mcp_ics_negate_result_positive_right * S ((S (ff_index_mcp_add_ics_negate_result_positive)) * ff_nns_mcp_smatrix_ics_negate_result) + (ff_right_mcp_add_ics_negate_result_positive))) -> (((exists fs_h_mcp_ics_negate_result_positive_target. fs_h_mcp_ics_negate_result_positive_target + S (ff_target_mcp_add_ics_negate_result_positive) = S ((S (ff_index_mcp_add_ics_negate_result_positive)) * nc)) /\ exists fs_q_mcp_ics_negate_result_positive_target. nb = fs_q_mcp_ics_negate_result_positive_target * S ((S (ff_index_mcp_add_ics_negate_result_positive)) * nc) + (ff_target_mcp_add_ics_negate_result_positive))) -> ff_target_mcp_add_ics_negate_result_positive = ff_left_mcp_add_ics_negate_result_positive + ff_right_mcp_add_ics_negate_result_positive) /\ (forall ff_index_mcp_add_ics_negate_result_negative ff_left_mcp_add_ics_negate_result_negative ff_right_mcp_add_ics_negate_result_negative ff_target_mcp_add_ics_negate_result_negative. (exists mcp_gap_ics_negate_result_negative_bound. mcp_gap_ics_negate_result_negative_bound + S (ff_index_mcp_add_ics_negate_result_negative) = ((r) * (1))) -> (((exists fs_h_mcp_ics_negate_result_negative_left. fs_h_mcp_ics_negate_result_negative_left + S (ff_left_mcp_add_ics_negate_result_negative) = S ((S (ff_index_mcp_add_ics_negate_result_negative)) * ff_pns_mcp_smatrix_ics_negate_result)) /\ exists fs_q_mcp_ics_negate_result_negative_left. ff_pn_mcp_smatrix_ics_negate_result = fs_q_mcp_ics_negate_result_negative_left * S ((S (ff_index_mcp_add_ics_negate_result_negative)) * ff_pns_mcp_smatrix_ics_negate_result) + (ff_left_mcp_add_ics_negate_result_negative))) -> (((exists fs_h_mcp_ics_negate_result_negative_right. fs_h_mcp_ics_negate_result_negative_right + S (ff_right_mcp_add_ics_negate_result_negative) = S ((S (ff_index_mcp_add_ics_negate_result_negative)) * ff_nps_mcp_smatrix_ics_negate_result)) /\ exists fs_q_mcp_ics_negate_result_negative_right. ff_np_mcp_smatrix_ics_negate_result = fs_q_mcp_ics_negate_result_negative_right * S ((S (ff_index_mcp_add_ics_negate_result_negative)) * ff_nps_mcp_smatrix_ics_negate_result) + (ff_right_mcp_add_ics_negate_result_negative))) -> (((exists fs_h_mcp_ics_negate_result_negative_target. fs_h_mcp_ics_negate_result_negative_target + S (ff_target_mcp_add_ics_negate_result_negative) = S ((S (ff_index_mcp_add_ics_negate_result_negative)) * pc)) /\ exists fs_q_mcp_ics_negate_result_negative_target. pb = fs_q_mcp_ics_negate_result_negative_target * S ((S (ff_index_mcp_add_ics_negate_result_negative)) * pc) + (ff_target_mcp_add_ics_negate_result_negative))) -> ff_target_mcp_add_ics_negate_result_negative = ff_left_mcp_add_ics_negate_result_negative + ff_right_mcp_add_ics_negate_result_negative)))))))Complete tactic proof in conservative notation
All 47 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
47 script commands · 15 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.
01Fix variables and assumptionsL1–10
02Fix variables and assumptionsL11–15
03Separate the logical casesL16–25
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L16
cases hproduct - L17
cases hproduct_witness - L18
cases hproduct_witness_witness - L19
cases hproduct_witness_witness_witness - L20
cases hproduct_witness_witness_witness_witness - L21
cases hproduct_witness_witness_witness_witness_witness - L22
cases hproduct_witness_witness_witness_witness_witness_witness - L23
cases hproduct_witness_witness_witness_witness_witness_witness_witness - L24
cases hproduct_witness_witness_witness_witness_witness_witness_witness_witness - L25
cases hproduct_witness_witness_witness_witness_witness_witness_witness_witness_right
04Separate the logical casesL26–28
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
05Construct an explicit witnessL29–36
06Separate the logical casesL37–37
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L37
split
07Use earlier factsL38–38
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L38
exact hproduct_witness_witness_witness_witness_witness_witness_witness_witness_right_right_left
08Separate the logical casesL39–39
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L39
split
09Use earlier factsL40–40
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L40
exact hproduct_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_left
10Separate the logical casesL41–41
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L41
split
11Use earlier factsL42–42
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L42
exact hproduct_witness_witness_witness_witness_witness_witness_witness_witness_left
12Separate the logical casesL43–43
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L43
split
13Use earlier factsL44–44
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L44
exact hproduct_witness_witness_witness_witness_witness_witness_witness_witness_right_left
14Separate the logical casesL45–45
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L45
split
15Use earlier factsL46–47
Instantiate or apply named facts and discharge the corresponding proof obligations.
Original defined command ledger · 47 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 hproduct - 0016
cases hproduct - 0017
cases hproduct_witness - 0018
cases hproduct_witness_witness - 0019
cases hproduct_witness_witness_witness - 0020
cases hproduct_witness_witness_witness_witness - 0021
cases hproduct_witness_witness_witness_witness_witness - 0022
cases hproduct_witness_witness_witness_witness_witness_witness - 0023
cases hproduct_witness_witness_witness_witness_witness_witness_witness - 0024
cases hproduct_witness_witness_witness_witness_witness_witness_witness_witness - 0025
cases hproduct_witness_witness_witness_witness_witness_witness_witness_witness_right - 0026
cases hproduct_witness_witness_witness_witness_witness_witness_witness_witness_right_right - 0027
cases hproduct_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right - 0028
cases hproduct_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_right - 0029
exists x4 - 0030
exists x5 - 0031
exists x6 - 0032
exists x7 - 0033
exists x - 0034
exists x1 - 0035
exists x2 - 0036
exists x3 - 0037
split - 0038
exact hproduct_witness_witness_witness_witness_witness_witness_witness_witness_right_right_left - 0039
split - 0040
exact hproduct_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_left - 0041
split - 0042
exact hproduct_witness_witness_witness_witness_witness_witness_witness_witness_left - 0043
split - 0044
exact hproduct_witness_witness_witness_witness_witness_witness_witness_witness_right_left - 0045
split - 0046
exact hproduct_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_right_right - 0047
exact hproduct_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_right_left