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. ∀ gb. ∀ gc. ∀ hb. ∀ hc. ∀ ib. ∀ ic. ∀ jb. ∀ jc. ∀ w. ∀ r. ∀ pb. ∀ pc. ∀ nb. ∀ nc. ∀ qb. ∀ qc. ∀ mb. ∀ mc. ∀ rb. ∀ rc. ∀ sb. ∀ sc. MatrixPointwiseAdd(eb,ec,gb,gc,ib,ic,w) → MatrixPointwiseAdd(fb,fc,hb,hc,jb,jc,w) → SignedMatrixProduct(ab,ac,db,dc,eb,ec,fb,fc,w,1,r,pb,pc,nb,nc) → SignedMatrixProduct(ab,ac,db,dc,gb,gc,hb,hc,w,1,r,qb,qc,mb,mc) → SignedMatrixProduct(ab,ac,db,dc,ib,ic,jb,jc,w,1,r,rb,rc,sb,sc) → MatrixPointwiseAdd(pb,pc,qb,qc,rb,rc,r · 1) ∧ MatrixPointwiseAdd(nb,nc,mb,mc,sb,sc,r · 1) Every linked abbreviation expands hygienically to the identical original native formula.
Definition DAG MatrixPointwiseAdd(mb,mc,sb,sc,tb,tc,l) · 8 SignedMatrixProduct(ab,ac,db,dc,eb,ec,fb,fc,w,v,r,pb,pc,nb,nc) · 3 Actual proof prerequisites Original expanded first-order statement
forall ab ac db dc eb ec fb fc gb gc hb hc ib ic jb jc w r pb pc nb nc qb qc mb mc rb rc sb sc. (forall ff_index_mcp_add_ics_sp_cofp ff_left_mcp_add_ics_sp_cofp ff_right_mcp_add_ics_sp_cofp ff_target_mcp_add_ics_sp_cofp. (exists mcp_gap_ics_sp_cofp_bound. mcp_gap_ics_sp_cofp_bound + S (ff_index_mcp_add_ics_sp_cofp) = (w)) -> (((exists fs_h_mcp_ics_sp_cofp_left. fs_h_mcp_ics_sp_cofp_left + S (ff_left_mcp_add_ics_sp_cofp) = S ((S (ff_index_mcp_add_ics_sp_cofp)) * ec)) /\ exists fs_q_mcp_ics_sp_cofp_left. eb = fs_q_mcp_ics_sp_cofp_left * S ((S (ff_index_mcp_add_ics_sp_cofp)) * ec) + (ff_left_mcp_add_ics_sp_cofp))) -> (((exists fs_h_mcp_ics_sp_cofp_right. fs_h_mcp_ics_sp_cofp_right + S (ff_right_mcp_add_ics_sp_cofp) = S ((S (ff_index_mcp_add_ics_sp_cofp)) * gc)) /\ exists fs_q_mcp_ics_sp_cofp_right. gb = fs_q_mcp_ics_sp_cofp_right * S ((S (ff_index_mcp_add_ics_sp_cofp)) * gc) + (ff_right_mcp_add_ics_sp_cofp))) -> (((exists fs_h_mcp_ics_sp_cofp_target. fs_h_mcp_ics_sp_cofp_target + S (ff_target_mcp_add_ics_sp_cofp) = S ((S (ff_index_mcp_add_ics_sp_cofp)) * ic)) /\ exists fs_q_mcp_ics_sp_cofp_target. ib = fs_q_mcp_ics_sp_cofp_target * S ((S (ff_index_mcp_add_ics_sp_cofp)) * ic) + (ff_target_mcp_add_ics_sp_cofp))) -> ff_target_mcp_add_ics_sp_cofp = ff_left_mcp_add_ics_sp_cofp + ff_right_mcp_add_ics_sp_cofp) -> (forall ff_index_mcp_add_ics_sp_cofn ff_left_mcp_add_ics_sp_cofn ff_right_mcp_add_ics_sp_cofn ff_target_mcp_add_ics_sp_cofn. (exists mcp_gap_ics_sp_cofn_bound. mcp_gap_ics_sp_cofn_bound + S (ff_index_mcp_add_ics_sp_cofn) = (w)) -> (((exists fs_h_mcp_ics_sp_cofn_left. fs_h_mcp_ics_sp_cofn_left + S (ff_left_mcp_add_ics_sp_cofn) = S ((S (ff_index_mcp_add_ics_sp_cofn)) * fc)) /\ exists fs_q_mcp_ics_sp_cofn_left. fb = fs_q_mcp_ics_sp_cofn_left * S ((S (ff_index_mcp_add_ics_sp_cofn)) * fc) + (ff_left_mcp_add_ics_sp_cofn))) -> (((exists fs_h_mcp_ics_sp_cofn_right. fs_h_mcp_ics_sp_cofn_right + S (ff_right_mcp_add_ics_sp_cofn) = S ((S (ff_index_mcp_add_ics_sp_cofn)) * hc)) /\ exists fs_q_mcp_ics_sp_cofn_right. hb = fs_q_mcp_ics_sp_cofn_right * S ((S (ff_index_mcp_add_ics_sp_cofn)) * hc) + (ff_right_mcp_add_ics_sp_cofn))) -> (((exists fs_h_mcp_ics_sp_cofn_target. fs_h_mcp_ics_sp_cofn_target + S (ff_target_mcp_add_ics_sp_cofn) = S ((S (ff_index_mcp_add_ics_sp_cofn)) * jc)) /\ exists fs_q_mcp_ics_sp_cofn_target. jb = fs_q_mcp_ics_sp_cofn_target * S ((S (ff_index_mcp_add_ics_sp_cofn)) * jc) + (ff_target_mcp_add_ics_sp_cofn))) -> ff_target_mcp_add_ics_sp_cofn = ff_left_mcp_add_ics_sp_cofn + ff_right_mcp_add_ics_sp_cofn) -> (exists ff_pp_mcp_smatrix_ics_sp0 ff_pps_mcp_smatrix_ics_sp0 ff_nn_mcp_smatrix_ics_sp0 ff_nns_mcp_smatrix_ics_sp0 ff_pn_mcp_smatrix_ics_sp0 ff_pns_mcp_smatrix_ics_sp0 ff_np_mcp_smatrix_ics_sp0 ff_nps_mcp_smatrix_ics_sp0. ((forall ff_index_mcp_prefix_ics_sp0_pp. (exists mcp_gap_ics_sp0_pp_index. mcp_gap_ics_sp0_pp_index + S (ff_index_mcp_prefix_ics_sp0_pp) = ((r) * (1))) -> exists ff_row_mcp_prefix_ics_sp0_pp ff_column_mcp_prefix_ics_sp0_pp ff_value_mcp_prefix_ics_sp0_pp. ((ff_index_mcp_prefix_ics_sp0_pp) = (1) * ff_row_mcp_prefix_ics_sp0_pp + ff_column_mcp_prefix_ics_sp0_pp /\ ((exists mcp_gap_ics_sp0_pp_column. mcp_gap_ics_sp0_pp_column + S (ff_column_mcp_prefix_ics_sp0_pp) = (1)) /\ ((exists ff_left_mcp_cell_ics_sp0_pp_cell ff_left_scale_mcp_cell_ics_sp0_pp_cell ff_right_mcp_cell_ics_sp0_pp_cell ff_right_scale_mcp_cell_ics_sp0_pp_cell. ((forall ff_index_mcp_ics_sp0_pp_cell_row ff_source_mcp_ics_sp0_pp_cell_row ff_target_mcp_ics_sp0_pp_cell_row. (exists mcp_gap_ics_sp0_pp_cell_row_bound. mcp_gap_ics_sp0_pp_cell_row_bound + S (ff_index_mcp_ics_sp0_pp_cell_row) = (w)) -> (((exists fs_h_mcp_ics_sp0_pp_cell_row_source. fs_h_mcp_ics_sp0_pp_cell_row_source + S (ff_source_mcp_ics_sp0_pp_cell_row) = S ((S (((ff_row_mcp_prefix_ics_sp0_pp) * (w)) + (1) * ff_index_mcp_ics_sp0_pp_cell_row)) * ac)) /\ exists fs_q_mcp_ics_sp0_pp_cell_row_source. ab = fs_q_mcp_ics_sp0_pp_cell_row_source * S ((S (((ff_row_mcp_prefix_ics_sp0_pp) * (w)) + (1) * ff_index_mcp_ics_sp0_pp_cell_row)) * ac) + (ff_source_mcp_ics_sp0_pp_cell_row))) -> (((exists fs_h_mcp_ics_sp0_pp_cell_row_target. fs_h_mcp_ics_sp0_pp_cell_row_target + S (ff_target_mcp_ics_sp0_pp_cell_row) = S ((S (ff_index_mcp_ics_sp0_pp_cell_row)) * ff_left_scale_mcp_cell_ics_sp0_pp_cell)) /\ exists fs_q_mcp_ics_sp0_pp_cell_row_target. ff_left_mcp_cell_ics_sp0_pp_cell = fs_q_mcp_ics_sp0_pp_cell_row_target * S ((S (ff_index_mcp_ics_sp0_pp_cell_row)) * ff_left_scale_mcp_cell_ics_sp0_pp_cell) + (ff_target_mcp_ics_sp0_pp_cell_row))) -> ff_target_mcp_ics_sp0_pp_cell_row = ff_source_mcp_ics_sp0_pp_cell_row) /\ ((forall ff_index_mcp_ics_sp0_pp_cell_column ff_source_mcp_ics_sp0_pp_cell_column ff_target_mcp_ics_sp0_pp_cell_column. (exists mcp_gap_ics_sp0_pp_cell_column_bound. mcp_gap_ics_sp0_pp_cell_column_bound + S (ff_index_mcp_ics_sp0_pp_cell_column) = (w)) -> (((exists fs_h_mcp_ics_sp0_pp_cell_column_source. fs_h_mcp_ics_sp0_pp_cell_column_source + S (ff_source_mcp_ics_sp0_pp_cell_column) = S ((S ((ff_column_mcp_prefix_ics_sp0_pp) + (1) * ff_index_mcp_ics_sp0_pp_cell_column)) * ec)) /\ exists fs_q_mcp_ics_sp0_pp_cell_column_source. eb = fs_q_mcp_ics_sp0_pp_cell_column_source * S ((S ((ff_column_mcp_prefix_ics_sp0_pp) + (1) * ff_index_mcp_ics_sp0_pp_cell_column)) * ec) + (ff_source_mcp_ics_sp0_pp_cell_column))) -> (((exists fs_h_mcp_ics_sp0_pp_cell_column_target. fs_h_mcp_ics_sp0_pp_cell_column_target + S (ff_target_mcp_ics_sp0_pp_cell_column) = S ((S (ff_index_mcp_ics_sp0_pp_cell_column)) * ff_right_scale_mcp_cell_ics_sp0_pp_cell)) /\ exists fs_q_mcp_ics_sp0_pp_cell_column_target. ff_right_mcp_cell_ics_sp0_pp_cell = fs_q_mcp_ics_sp0_pp_cell_column_target * S ((S (ff_index_mcp_ics_sp0_pp_cell_column)) * ff_right_scale_mcp_cell_ics_sp0_pp_cell) + (ff_target_mcp_ics_sp0_pp_cell_column))) -> ff_target_mcp_ics_sp0_pp_cell_column = ff_source_mcp_ics_sp0_pp_cell_column) /\ (exists ff_code_dot_mcp_ics_sp0_pp_cell_dot ff_scale_dot_mcp_ics_sp0_pp_cell_dot. ((forall fpmp_index_dot_mcp_ics_sp0_pp_cell_dot_pointwise fpmp_left_dot_mcp_ics_sp0_pp_cell_dot_pointwise fpmp_right_dot_mcp_ics_sp0_pp_cell_dot_pointwise fpmp_target_dot_mcp_ics_sp0_pp_cell_dot_pointwise. (exists fpmp_gap_dot_mcp_ics_sp0_pp_cell_dot_pointwise. fpmp_gap_dot_mcp_ics_sp0_pp_cell_dot_pointwise + S fpmp_index_dot_mcp_ics_sp0_pp_cell_dot_pointwise = w) -> (((exists ff_h_fpmp_dot_mcp_ics_sp0_pp_cell_dot_pointwise_left. ff_h_fpmp_dot_mcp_ics_sp0_pp_cell_dot_pointwise_left + S (fpmp_left_dot_mcp_ics_sp0_pp_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_sp0_pp_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_sp0_pp_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_sp0_pp_cell_dot_pointwise_left. ff_left_mcp_cell_ics_sp0_pp_cell = ff_q_fpmp_dot_mcp_ics_sp0_pp_cell_dot_pointwise_left * S ((S (fpmp_index_dot_mcp_ics_sp0_pp_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_sp0_pp_cell) + (fpmp_left_dot_mcp_ics_sp0_pp_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_sp0_pp_cell_dot_pointwise_right. ff_h_fpmp_dot_mcp_ics_sp0_pp_cell_dot_pointwise_right + S (fpmp_right_dot_mcp_ics_sp0_pp_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_sp0_pp_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_sp0_pp_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_sp0_pp_cell_dot_pointwise_right. ff_right_mcp_cell_ics_sp0_pp_cell = ff_q_fpmp_dot_mcp_ics_sp0_pp_cell_dot_pointwise_right * S ((S (fpmp_index_dot_mcp_ics_sp0_pp_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_sp0_pp_cell) + (fpmp_right_dot_mcp_ics_sp0_pp_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_sp0_pp_cell_dot_pointwise_target. ff_h_fpmp_dot_mcp_ics_sp0_pp_cell_dot_pointwise_target + S (fpmp_target_dot_mcp_ics_sp0_pp_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_sp0_pp_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_sp0_pp_cell_dot)) /\ exists ff_q_fpmp_dot_mcp_ics_sp0_pp_cell_dot_pointwise_target. ff_code_dot_mcp_ics_sp0_pp_cell_dot = ff_q_fpmp_dot_mcp_ics_sp0_pp_cell_dot_pointwise_target * S ((S (fpmp_index_dot_mcp_ics_sp0_pp_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_sp0_pp_cell_dot) + (fpmp_target_dot_mcp_ics_sp0_pp_cell_dot_pointwise))) -> fpmp_target_dot_mcp_ics_sp0_pp_cell_dot_pointwise = fpmp_left_dot_mcp_ics_sp0_pp_cell_dot_pointwise * fpmp_right_dot_mcp_ics_sp0_pp_cell_dot_pointwise) /\ (exists ff_u_dot_mcp_ics_sp0_pp_cell_dot_sum ff_v_dot_mcp_ics_sp0_pp_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_sp0_pp_cell_dot_sum_start. ff_h_dot_mcp_ics_sp0_pp_cell_dot_sum_start + S (0) = S ((S (0)) * ff_v_dot_mcp_ics_sp0_pp_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_sp0_pp_cell_dot_sum_start. ff_u_dot_mcp_ics_sp0_pp_cell_dot_sum = ff_q_dot_mcp_ics_sp0_pp_cell_dot_sum_start * S ((S (0)) * ff_v_dot_mcp_ics_sp0_pp_cell_dot_sum) + (0))) /\ ((((exists ff_h_dot_mcp_ics_sp0_pp_cell_dot_sum_terminal. ff_h_dot_mcp_ics_sp0_pp_cell_dot_sum_terminal + S (ff_value_mcp_prefix_ics_sp0_pp) = S ((S (w)) * ff_v_dot_mcp_ics_sp0_pp_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_sp0_pp_cell_dot_sum_terminal. ff_u_dot_mcp_ics_sp0_pp_cell_dot_sum = ff_q_dot_mcp_ics_sp0_pp_cell_dot_sum_terminal * S ((S (w)) * ff_v_dot_mcp_ics_sp0_pp_cell_dot_sum) + (ff_value_mcp_prefix_ics_sp0_pp))) /\ forall ff_i_dot_mcp_ics_sp0_pp_cell_dot_sum. (exists ff_lt_dot_mcp_ics_sp0_pp_cell_dot_sum_bound. ff_lt_dot_mcp_ics_sp0_pp_cell_dot_sum_bound + S ff_i_dot_mcp_ics_sp0_pp_cell_dot_sum = w) -> exists ff_a_dot_mcp_ics_sp0_pp_cell_dot_sum ff_r_dot_mcp_ics_sp0_pp_cell_dot_sum ff_s_dot_mcp_ics_sp0_pp_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_sp0_pp_cell_dot_sum_summand. ff_h_dot_mcp_ics_sp0_pp_cell_dot_sum_summand + S (ff_a_dot_mcp_ics_sp0_pp_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_sp0_pp_cell_dot_sum)) * ff_scale_dot_mcp_ics_sp0_pp_cell_dot)) /\ exists ff_q_dot_mcp_ics_sp0_pp_cell_dot_sum_summand. ff_code_dot_mcp_ics_sp0_pp_cell_dot = ff_q_dot_mcp_ics_sp0_pp_cell_dot_sum_summand * S ((S (ff_i_dot_mcp_ics_sp0_pp_cell_dot_sum)) * ff_scale_dot_mcp_ics_sp0_pp_cell_dot) + (ff_a_dot_mcp_ics_sp0_pp_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_sp0_pp_cell_dot_sum_partial. ff_h_dot_mcp_ics_sp0_pp_cell_dot_sum_partial + S (ff_r_dot_mcp_ics_sp0_pp_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_sp0_pp_cell_dot_sum)) * ff_v_dot_mcp_ics_sp0_pp_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_sp0_pp_cell_dot_sum_partial. ff_u_dot_mcp_ics_sp0_pp_cell_dot_sum = ff_q_dot_mcp_ics_sp0_pp_cell_dot_sum_partial * S ((S (ff_i_dot_mcp_ics_sp0_pp_cell_dot_sum)) * ff_v_dot_mcp_ics_sp0_pp_cell_dot_sum) + (ff_r_dot_mcp_ics_sp0_pp_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_sp0_pp_cell_dot_sum_successor. ff_h_dot_mcp_ics_sp0_pp_cell_dot_sum_successor + S (ff_s_dot_mcp_ics_sp0_pp_cell_dot_sum) = S ((S (S ff_i_dot_mcp_ics_sp0_pp_cell_dot_sum)) * ff_v_dot_mcp_ics_sp0_pp_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_sp0_pp_cell_dot_sum_successor. ff_u_dot_mcp_ics_sp0_pp_cell_dot_sum = ff_q_dot_mcp_ics_sp0_pp_cell_dot_sum_successor * S ((S (S ff_i_dot_mcp_ics_sp0_pp_cell_dot_sum)) * ff_v_dot_mcp_ics_sp0_pp_cell_dot_sum) + (ff_s_dot_mcp_ics_sp0_pp_cell_dot_sum))) /\ ff_s_dot_mcp_ics_sp0_pp_cell_dot_sum = ff_r_dot_mcp_ics_sp0_pp_cell_dot_sum + ff_a_dot_mcp_ics_sp0_pp_cell_dot_sum))))))))))) /\ (((exists fs_h_mcp_ics_sp0_pp_entry. fs_h_mcp_ics_sp0_pp_entry + S (ff_value_mcp_prefix_ics_sp0_pp) = S ((S (ff_index_mcp_prefix_ics_sp0_pp)) * ff_pps_mcp_smatrix_ics_sp0)) /\ exists fs_q_mcp_ics_sp0_pp_entry. ff_pp_mcp_smatrix_ics_sp0 = fs_q_mcp_ics_sp0_pp_entry * S ((S (ff_index_mcp_prefix_ics_sp0_pp)) * ff_pps_mcp_smatrix_ics_sp0) + (ff_value_mcp_prefix_ics_sp0_pp))))))) /\ ((forall ff_index_mcp_prefix_ics_sp0_nn. (exists mcp_gap_ics_sp0_nn_index. mcp_gap_ics_sp0_nn_index + S (ff_index_mcp_prefix_ics_sp0_nn) = ((r) * (1))) -> exists ff_row_mcp_prefix_ics_sp0_nn ff_column_mcp_prefix_ics_sp0_nn ff_value_mcp_prefix_ics_sp0_nn. ((ff_index_mcp_prefix_ics_sp0_nn) = (1) * ff_row_mcp_prefix_ics_sp0_nn + ff_column_mcp_prefix_ics_sp0_nn /\ ((exists mcp_gap_ics_sp0_nn_column. mcp_gap_ics_sp0_nn_column + S (ff_column_mcp_prefix_ics_sp0_nn) = (1)) /\ ((exists ff_left_mcp_cell_ics_sp0_nn_cell ff_left_scale_mcp_cell_ics_sp0_nn_cell ff_right_mcp_cell_ics_sp0_nn_cell ff_right_scale_mcp_cell_ics_sp0_nn_cell. ((forall ff_index_mcp_ics_sp0_nn_cell_row ff_source_mcp_ics_sp0_nn_cell_row ff_target_mcp_ics_sp0_nn_cell_row. (exists mcp_gap_ics_sp0_nn_cell_row_bound. mcp_gap_ics_sp0_nn_cell_row_bound + S (ff_index_mcp_ics_sp0_nn_cell_row) = (w)) -> (((exists fs_h_mcp_ics_sp0_nn_cell_row_source. fs_h_mcp_ics_sp0_nn_cell_row_source + S (ff_source_mcp_ics_sp0_nn_cell_row) = S ((S (((ff_row_mcp_prefix_ics_sp0_nn) * (w)) + (1) * ff_index_mcp_ics_sp0_nn_cell_row)) * dc)) /\ exists fs_q_mcp_ics_sp0_nn_cell_row_source. db = fs_q_mcp_ics_sp0_nn_cell_row_source * S ((S (((ff_row_mcp_prefix_ics_sp0_nn) * (w)) + (1) * ff_index_mcp_ics_sp0_nn_cell_row)) * dc) + (ff_source_mcp_ics_sp0_nn_cell_row))) -> (((exists fs_h_mcp_ics_sp0_nn_cell_row_target. fs_h_mcp_ics_sp0_nn_cell_row_target + S (ff_target_mcp_ics_sp0_nn_cell_row) = S ((S (ff_index_mcp_ics_sp0_nn_cell_row)) * ff_left_scale_mcp_cell_ics_sp0_nn_cell)) /\ exists fs_q_mcp_ics_sp0_nn_cell_row_target. ff_left_mcp_cell_ics_sp0_nn_cell = fs_q_mcp_ics_sp0_nn_cell_row_target * S ((S (ff_index_mcp_ics_sp0_nn_cell_row)) * ff_left_scale_mcp_cell_ics_sp0_nn_cell) + (ff_target_mcp_ics_sp0_nn_cell_row))) -> ff_target_mcp_ics_sp0_nn_cell_row = ff_source_mcp_ics_sp0_nn_cell_row) /\ ((forall ff_index_mcp_ics_sp0_nn_cell_column ff_source_mcp_ics_sp0_nn_cell_column ff_target_mcp_ics_sp0_nn_cell_column. (exists mcp_gap_ics_sp0_nn_cell_column_bound. mcp_gap_ics_sp0_nn_cell_column_bound + S (ff_index_mcp_ics_sp0_nn_cell_column) = (w)) -> (((exists fs_h_mcp_ics_sp0_nn_cell_column_source. fs_h_mcp_ics_sp0_nn_cell_column_source + S (ff_source_mcp_ics_sp0_nn_cell_column) = S ((S ((ff_column_mcp_prefix_ics_sp0_nn) + (1) * ff_index_mcp_ics_sp0_nn_cell_column)) * fc)) /\ exists fs_q_mcp_ics_sp0_nn_cell_column_source. fb = fs_q_mcp_ics_sp0_nn_cell_column_source * S ((S ((ff_column_mcp_prefix_ics_sp0_nn) + (1) * ff_index_mcp_ics_sp0_nn_cell_column)) * fc) + (ff_source_mcp_ics_sp0_nn_cell_column))) -> (((exists fs_h_mcp_ics_sp0_nn_cell_column_target. fs_h_mcp_ics_sp0_nn_cell_column_target + S (ff_target_mcp_ics_sp0_nn_cell_column) = S ((S (ff_index_mcp_ics_sp0_nn_cell_column)) * ff_right_scale_mcp_cell_ics_sp0_nn_cell)) /\ exists fs_q_mcp_ics_sp0_nn_cell_column_target. ff_right_mcp_cell_ics_sp0_nn_cell = fs_q_mcp_ics_sp0_nn_cell_column_target * S ((S (ff_index_mcp_ics_sp0_nn_cell_column)) * ff_right_scale_mcp_cell_ics_sp0_nn_cell) + (ff_target_mcp_ics_sp0_nn_cell_column))) -> ff_target_mcp_ics_sp0_nn_cell_column = ff_source_mcp_ics_sp0_nn_cell_column) /\ (exists ff_code_dot_mcp_ics_sp0_nn_cell_dot ff_scale_dot_mcp_ics_sp0_nn_cell_dot. ((forall fpmp_index_dot_mcp_ics_sp0_nn_cell_dot_pointwise fpmp_left_dot_mcp_ics_sp0_nn_cell_dot_pointwise fpmp_right_dot_mcp_ics_sp0_nn_cell_dot_pointwise fpmp_target_dot_mcp_ics_sp0_nn_cell_dot_pointwise. (exists fpmp_gap_dot_mcp_ics_sp0_nn_cell_dot_pointwise. fpmp_gap_dot_mcp_ics_sp0_nn_cell_dot_pointwise + S fpmp_index_dot_mcp_ics_sp0_nn_cell_dot_pointwise = w) -> (((exists ff_h_fpmp_dot_mcp_ics_sp0_nn_cell_dot_pointwise_left. ff_h_fpmp_dot_mcp_ics_sp0_nn_cell_dot_pointwise_left + S (fpmp_left_dot_mcp_ics_sp0_nn_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_sp0_nn_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_sp0_nn_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_sp0_nn_cell_dot_pointwise_left. ff_left_mcp_cell_ics_sp0_nn_cell = ff_q_fpmp_dot_mcp_ics_sp0_nn_cell_dot_pointwise_left * S ((S (fpmp_index_dot_mcp_ics_sp0_nn_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_sp0_nn_cell) + (fpmp_left_dot_mcp_ics_sp0_nn_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_sp0_nn_cell_dot_pointwise_right. ff_h_fpmp_dot_mcp_ics_sp0_nn_cell_dot_pointwise_right + S (fpmp_right_dot_mcp_ics_sp0_nn_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_sp0_nn_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_sp0_nn_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_sp0_nn_cell_dot_pointwise_right. ff_right_mcp_cell_ics_sp0_nn_cell = ff_q_fpmp_dot_mcp_ics_sp0_nn_cell_dot_pointwise_right * S ((S (fpmp_index_dot_mcp_ics_sp0_nn_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_sp0_nn_cell) + (fpmp_right_dot_mcp_ics_sp0_nn_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_sp0_nn_cell_dot_pointwise_target. ff_h_fpmp_dot_mcp_ics_sp0_nn_cell_dot_pointwise_target + S (fpmp_target_dot_mcp_ics_sp0_nn_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_sp0_nn_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_sp0_nn_cell_dot)) /\ exists ff_q_fpmp_dot_mcp_ics_sp0_nn_cell_dot_pointwise_target. ff_code_dot_mcp_ics_sp0_nn_cell_dot = ff_q_fpmp_dot_mcp_ics_sp0_nn_cell_dot_pointwise_target * S ((S (fpmp_index_dot_mcp_ics_sp0_nn_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_sp0_nn_cell_dot) + (fpmp_target_dot_mcp_ics_sp0_nn_cell_dot_pointwise))) -> fpmp_target_dot_mcp_ics_sp0_nn_cell_dot_pointwise = fpmp_left_dot_mcp_ics_sp0_nn_cell_dot_pointwise * fpmp_right_dot_mcp_ics_sp0_nn_cell_dot_pointwise) /\ (exists ff_u_dot_mcp_ics_sp0_nn_cell_dot_sum ff_v_dot_mcp_ics_sp0_nn_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_sp0_nn_cell_dot_sum_start. ff_h_dot_mcp_ics_sp0_nn_cell_dot_sum_start + S (0) = S ((S (0)) * ff_v_dot_mcp_ics_sp0_nn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_sp0_nn_cell_dot_sum_start. ff_u_dot_mcp_ics_sp0_nn_cell_dot_sum = ff_q_dot_mcp_ics_sp0_nn_cell_dot_sum_start * S ((S (0)) * ff_v_dot_mcp_ics_sp0_nn_cell_dot_sum) + (0))) /\ ((((exists ff_h_dot_mcp_ics_sp0_nn_cell_dot_sum_terminal. ff_h_dot_mcp_ics_sp0_nn_cell_dot_sum_terminal + S (ff_value_mcp_prefix_ics_sp0_nn) = S ((S (w)) * ff_v_dot_mcp_ics_sp0_nn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_sp0_nn_cell_dot_sum_terminal. ff_u_dot_mcp_ics_sp0_nn_cell_dot_sum = ff_q_dot_mcp_ics_sp0_nn_cell_dot_sum_terminal * S ((S (w)) * ff_v_dot_mcp_ics_sp0_nn_cell_dot_sum) + (ff_value_mcp_prefix_ics_sp0_nn))) /\ forall ff_i_dot_mcp_ics_sp0_nn_cell_dot_sum. (exists ff_lt_dot_mcp_ics_sp0_nn_cell_dot_sum_bound. ff_lt_dot_mcp_ics_sp0_nn_cell_dot_sum_bound + S ff_i_dot_mcp_ics_sp0_nn_cell_dot_sum = w) -> exists ff_a_dot_mcp_ics_sp0_nn_cell_dot_sum ff_r_dot_mcp_ics_sp0_nn_cell_dot_sum ff_s_dot_mcp_ics_sp0_nn_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_sp0_nn_cell_dot_sum_summand. ff_h_dot_mcp_ics_sp0_nn_cell_dot_sum_summand + S (ff_a_dot_mcp_ics_sp0_nn_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_sp0_nn_cell_dot_sum)) * ff_scale_dot_mcp_ics_sp0_nn_cell_dot)) /\ exists ff_q_dot_mcp_ics_sp0_nn_cell_dot_sum_summand. ff_code_dot_mcp_ics_sp0_nn_cell_dot = ff_q_dot_mcp_ics_sp0_nn_cell_dot_sum_summand * S ((S (ff_i_dot_mcp_ics_sp0_nn_cell_dot_sum)) * ff_scale_dot_mcp_ics_sp0_nn_cell_dot) + (ff_a_dot_mcp_ics_sp0_nn_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_sp0_nn_cell_dot_sum_partial. ff_h_dot_mcp_ics_sp0_nn_cell_dot_sum_partial + S (ff_r_dot_mcp_ics_sp0_nn_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_sp0_nn_cell_dot_sum)) * ff_v_dot_mcp_ics_sp0_nn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_sp0_nn_cell_dot_sum_partial. ff_u_dot_mcp_ics_sp0_nn_cell_dot_sum = ff_q_dot_mcp_ics_sp0_nn_cell_dot_sum_partial * S ((S (ff_i_dot_mcp_ics_sp0_nn_cell_dot_sum)) * ff_v_dot_mcp_ics_sp0_nn_cell_dot_sum) + (ff_r_dot_mcp_ics_sp0_nn_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_sp0_nn_cell_dot_sum_successor. ff_h_dot_mcp_ics_sp0_nn_cell_dot_sum_successor + S (ff_s_dot_mcp_ics_sp0_nn_cell_dot_sum) = S ((S (S ff_i_dot_mcp_ics_sp0_nn_cell_dot_sum)) * ff_v_dot_mcp_ics_sp0_nn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_sp0_nn_cell_dot_sum_successor. ff_u_dot_mcp_ics_sp0_nn_cell_dot_sum = ff_q_dot_mcp_ics_sp0_nn_cell_dot_sum_successor * S ((S (S ff_i_dot_mcp_ics_sp0_nn_cell_dot_sum)) * ff_v_dot_mcp_ics_sp0_nn_cell_dot_sum) + (ff_s_dot_mcp_ics_sp0_nn_cell_dot_sum))) /\ ff_s_dot_mcp_ics_sp0_nn_cell_dot_sum = ff_r_dot_mcp_ics_sp0_nn_cell_dot_sum + ff_a_dot_mcp_ics_sp0_nn_cell_dot_sum))))))))))) /\ (((exists fs_h_mcp_ics_sp0_nn_entry. fs_h_mcp_ics_sp0_nn_entry + S (ff_value_mcp_prefix_ics_sp0_nn) = S ((S (ff_index_mcp_prefix_ics_sp0_nn)) * ff_nns_mcp_smatrix_ics_sp0)) /\ exists fs_q_mcp_ics_sp0_nn_entry. ff_nn_mcp_smatrix_ics_sp0 = fs_q_mcp_ics_sp0_nn_entry * S ((S (ff_index_mcp_prefix_ics_sp0_nn)) * ff_nns_mcp_smatrix_ics_sp0) + (ff_value_mcp_prefix_ics_sp0_nn))))))) /\ ((forall ff_index_mcp_prefix_ics_sp0_pn. (exists mcp_gap_ics_sp0_pn_index. mcp_gap_ics_sp0_pn_index + S (ff_index_mcp_prefix_ics_sp0_pn) = ((r) * (1))) -> exists ff_row_mcp_prefix_ics_sp0_pn ff_column_mcp_prefix_ics_sp0_pn ff_value_mcp_prefix_ics_sp0_pn. ((ff_index_mcp_prefix_ics_sp0_pn) = (1) * ff_row_mcp_prefix_ics_sp0_pn + ff_column_mcp_prefix_ics_sp0_pn /\ ((exists mcp_gap_ics_sp0_pn_column. mcp_gap_ics_sp0_pn_column + S (ff_column_mcp_prefix_ics_sp0_pn) = (1)) /\ ((exists ff_left_mcp_cell_ics_sp0_pn_cell ff_left_scale_mcp_cell_ics_sp0_pn_cell ff_right_mcp_cell_ics_sp0_pn_cell ff_right_scale_mcp_cell_ics_sp0_pn_cell. ((forall ff_index_mcp_ics_sp0_pn_cell_row ff_source_mcp_ics_sp0_pn_cell_row ff_target_mcp_ics_sp0_pn_cell_row. (exists mcp_gap_ics_sp0_pn_cell_row_bound. mcp_gap_ics_sp0_pn_cell_row_bound + S (ff_index_mcp_ics_sp0_pn_cell_row) = (w)) -> (((exists fs_h_mcp_ics_sp0_pn_cell_row_source. fs_h_mcp_ics_sp0_pn_cell_row_source + S (ff_source_mcp_ics_sp0_pn_cell_row) = S ((S (((ff_row_mcp_prefix_ics_sp0_pn) * (w)) + (1) * ff_index_mcp_ics_sp0_pn_cell_row)) * ac)) /\ exists fs_q_mcp_ics_sp0_pn_cell_row_source. ab = fs_q_mcp_ics_sp0_pn_cell_row_source * S ((S (((ff_row_mcp_prefix_ics_sp0_pn) * (w)) + (1) * ff_index_mcp_ics_sp0_pn_cell_row)) * ac) + (ff_source_mcp_ics_sp0_pn_cell_row))) -> (((exists fs_h_mcp_ics_sp0_pn_cell_row_target. fs_h_mcp_ics_sp0_pn_cell_row_target + S (ff_target_mcp_ics_sp0_pn_cell_row) = S ((S (ff_index_mcp_ics_sp0_pn_cell_row)) * ff_left_scale_mcp_cell_ics_sp0_pn_cell)) /\ exists fs_q_mcp_ics_sp0_pn_cell_row_target. ff_left_mcp_cell_ics_sp0_pn_cell = fs_q_mcp_ics_sp0_pn_cell_row_target * S ((S (ff_index_mcp_ics_sp0_pn_cell_row)) * ff_left_scale_mcp_cell_ics_sp0_pn_cell) + (ff_target_mcp_ics_sp0_pn_cell_row))) -> ff_target_mcp_ics_sp0_pn_cell_row = ff_source_mcp_ics_sp0_pn_cell_row) /\ ((forall ff_index_mcp_ics_sp0_pn_cell_column ff_source_mcp_ics_sp0_pn_cell_column ff_target_mcp_ics_sp0_pn_cell_column. (exists mcp_gap_ics_sp0_pn_cell_column_bound. mcp_gap_ics_sp0_pn_cell_column_bound + S (ff_index_mcp_ics_sp0_pn_cell_column) = (w)) -> (((exists fs_h_mcp_ics_sp0_pn_cell_column_source. fs_h_mcp_ics_sp0_pn_cell_column_source + S (ff_source_mcp_ics_sp0_pn_cell_column) = S ((S ((ff_column_mcp_prefix_ics_sp0_pn) + (1) * ff_index_mcp_ics_sp0_pn_cell_column)) * fc)) /\ exists fs_q_mcp_ics_sp0_pn_cell_column_source. fb = fs_q_mcp_ics_sp0_pn_cell_column_source * S ((S ((ff_column_mcp_prefix_ics_sp0_pn) + (1) * ff_index_mcp_ics_sp0_pn_cell_column)) * fc) + (ff_source_mcp_ics_sp0_pn_cell_column))) -> (((exists fs_h_mcp_ics_sp0_pn_cell_column_target. fs_h_mcp_ics_sp0_pn_cell_column_target + S (ff_target_mcp_ics_sp0_pn_cell_column) = S ((S (ff_index_mcp_ics_sp0_pn_cell_column)) * ff_right_scale_mcp_cell_ics_sp0_pn_cell)) /\ exists fs_q_mcp_ics_sp0_pn_cell_column_target. ff_right_mcp_cell_ics_sp0_pn_cell = fs_q_mcp_ics_sp0_pn_cell_column_target * S ((S (ff_index_mcp_ics_sp0_pn_cell_column)) * ff_right_scale_mcp_cell_ics_sp0_pn_cell) + (ff_target_mcp_ics_sp0_pn_cell_column))) -> ff_target_mcp_ics_sp0_pn_cell_column = ff_source_mcp_ics_sp0_pn_cell_column) /\ (exists ff_code_dot_mcp_ics_sp0_pn_cell_dot ff_scale_dot_mcp_ics_sp0_pn_cell_dot. ((forall fpmp_index_dot_mcp_ics_sp0_pn_cell_dot_pointwise fpmp_left_dot_mcp_ics_sp0_pn_cell_dot_pointwise fpmp_right_dot_mcp_ics_sp0_pn_cell_dot_pointwise fpmp_target_dot_mcp_ics_sp0_pn_cell_dot_pointwise. (exists fpmp_gap_dot_mcp_ics_sp0_pn_cell_dot_pointwise. fpmp_gap_dot_mcp_ics_sp0_pn_cell_dot_pointwise + S fpmp_index_dot_mcp_ics_sp0_pn_cell_dot_pointwise = w) -> (((exists ff_h_fpmp_dot_mcp_ics_sp0_pn_cell_dot_pointwise_left. ff_h_fpmp_dot_mcp_ics_sp0_pn_cell_dot_pointwise_left + S (fpmp_left_dot_mcp_ics_sp0_pn_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_sp0_pn_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_sp0_pn_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_sp0_pn_cell_dot_pointwise_left. ff_left_mcp_cell_ics_sp0_pn_cell = ff_q_fpmp_dot_mcp_ics_sp0_pn_cell_dot_pointwise_left * S ((S (fpmp_index_dot_mcp_ics_sp0_pn_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_sp0_pn_cell) + (fpmp_left_dot_mcp_ics_sp0_pn_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_sp0_pn_cell_dot_pointwise_right. ff_h_fpmp_dot_mcp_ics_sp0_pn_cell_dot_pointwise_right + S (fpmp_right_dot_mcp_ics_sp0_pn_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_sp0_pn_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_sp0_pn_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_sp0_pn_cell_dot_pointwise_right. ff_right_mcp_cell_ics_sp0_pn_cell = ff_q_fpmp_dot_mcp_ics_sp0_pn_cell_dot_pointwise_right * S ((S (fpmp_index_dot_mcp_ics_sp0_pn_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_sp0_pn_cell) + (fpmp_right_dot_mcp_ics_sp0_pn_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_sp0_pn_cell_dot_pointwise_target. ff_h_fpmp_dot_mcp_ics_sp0_pn_cell_dot_pointwise_target + S (fpmp_target_dot_mcp_ics_sp0_pn_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_sp0_pn_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_sp0_pn_cell_dot)) /\ exists ff_q_fpmp_dot_mcp_ics_sp0_pn_cell_dot_pointwise_target. ff_code_dot_mcp_ics_sp0_pn_cell_dot = ff_q_fpmp_dot_mcp_ics_sp0_pn_cell_dot_pointwise_target * S ((S (fpmp_index_dot_mcp_ics_sp0_pn_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_sp0_pn_cell_dot) + (fpmp_target_dot_mcp_ics_sp0_pn_cell_dot_pointwise))) -> fpmp_target_dot_mcp_ics_sp0_pn_cell_dot_pointwise = fpmp_left_dot_mcp_ics_sp0_pn_cell_dot_pointwise * fpmp_right_dot_mcp_ics_sp0_pn_cell_dot_pointwise) /\ (exists ff_u_dot_mcp_ics_sp0_pn_cell_dot_sum ff_v_dot_mcp_ics_sp0_pn_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_sp0_pn_cell_dot_sum_start. ff_h_dot_mcp_ics_sp0_pn_cell_dot_sum_start + S (0) = S ((S (0)) * ff_v_dot_mcp_ics_sp0_pn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_sp0_pn_cell_dot_sum_start. ff_u_dot_mcp_ics_sp0_pn_cell_dot_sum = ff_q_dot_mcp_ics_sp0_pn_cell_dot_sum_start * S ((S (0)) * ff_v_dot_mcp_ics_sp0_pn_cell_dot_sum) + (0))) /\ ((((exists ff_h_dot_mcp_ics_sp0_pn_cell_dot_sum_terminal. ff_h_dot_mcp_ics_sp0_pn_cell_dot_sum_terminal + S (ff_value_mcp_prefix_ics_sp0_pn) = S ((S (w)) * ff_v_dot_mcp_ics_sp0_pn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_sp0_pn_cell_dot_sum_terminal. ff_u_dot_mcp_ics_sp0_pn_cell_dot_sum = ff_q_dot_mcp_ics_sp0_pn_cell_dot_sum_terminal * S ((S (w)) * ff_v_dot_mcp_ics_sp0_pn_cell_dot_sum) + (ff_value_mcp_prefix_ics_sp0_pn))) /\ forall ff_i_dot_mcp_ics_sp0_pn_cell_dot_sum. (exists ff_lt_dot_mcp_ics_sp0_pn_cell_dot_sum_bound. ff_lt_dot_mcp_ics_sp0_pn_cell_dot_sum_bound + S ff_i_dot_mcp_ics_sp0_pn_cell_dot_sum = w) -> exists ff_a_dot_mcp_ics_sp0_pn_cell_dot_sum ff_r_dot_mcp_ics_sp0_pn_cell_dot_sum ff_s_dot_mcp_ics_sp0_pn_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_sp0_pn_cell_dot_sum_summand. ff_h_dot_mcp_ics_sp0_pn_cell_dot_sum_summand + S (ff_a_dot_mcp_ics_sp0_pn_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_sp0_pn_cell_dot_sum)) * ff_scale_dot_mcp_ics_sp0_pn_cell_dot)) /\ exists ff_q_dot_mcp_ics_sp0_pn_cell_dot_sum_summand. ff_code_dot_mcp_ics_sp0_pn_cell_dot = ff_q_dot_mcp_ics_sp0_pn_cell_dot_sum_summand * S ((S (ff_i_dot_mcp_ics_sp0_pn_cell_dot_sum)) * ff_scale_dot_mcp_ics_sp0_pn_cell_dot) + (ff_a_dot_mcp_ics_sp0_pn_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_sp0_pn_cell_dot_sum_partial. ff_h_dot_mcp_ics_sp0_pn_cell_dot_sum_partial + S (ff_r_dot_mcp_ics_sp0_pn_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_sp0_pn_cell_dot_sum)) * ff_v_dot_mcp_ics_sp0_pn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_sp0_pn_cell_dot_sum_partial. ff_u_dot_mcp_ics_sp0_pn_cell_dot_sum = ff_q_dot_mcp_ics_sp0_pn_cell_dot_sum_partial * S ((S (ff_i_dot_mcp_ics_sp0_pn_cell_dot_sum)) * ff_v_dot_mcp_ics_sp0_pn_cell_dot_sum) + (ff_r_dot_mcp_ics_sp0_pn_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_sp0_pn_cell_dot_sum_successor. ff_h_dot_mcp_ics_sp0_pn_cell_dot_sum_successor + S (ff_s_dot_mcp_ics_sp0_pn_cell_dot_sum) = S ((S (S ff_i_dot_mcp_ics_sp0_pn_cell_dot_sum)) * ff_v_dot_mcp_ics_sp0_pn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_sp0_pn_cell_dot_sum_successor. ff_u_dot_mcp_ics_sp0_pn_cell_dot_sum = ff_q_dot_mcp_ics_sp0_pn_cell_dot_sum_successor * S ((S (S ff_i_dot_mcp_ics_sp0_pn_cell_dot_sum)) * ff_v_dot_mcp_ics_sp0_pn_cell_dot_sum) + (ff_s_dot_mcp_ics_sp0_pn_cell_dot_sum))) /\ ff_s_dot_mcp_ics_sp0_pn_cell_dot_sum = ff_r_dot_mcp_ics_sp0_pn_cell_dot_sum + ff_a_dot_mcp_ics_sp0_pn_cell_dot_sum))))))))))) /\ (((exists fs_h_mcp_ics_sp0_pn_entry. fs_h_mcp_ics_sp0_pn_entry + S (ff_value_mcp_prefix_ics_sp0_pn) = S ((S (ff_index_mcp_prefix_ics_sp0_pn)) * ff_pns_mcp_smatrix_ics_sp0)) /\ exists fs_q_mcp_ics_sp0_pn_entry. ff_pn_mcp_smatrix_ics_sp0 = fs_q_mcp_ics_sp0_pn_entry * S ((S (ff_index_mcp_prefix_ics_sp0_pn)) * ff_pns_mcp_smatrix_ics_sp0) + (ff_value_mcp_prefix_ics_sp0_pn))))))) /\ ((forall ff_index_mcp_prefix_ics_sp0_np. (exists mcp_gap_ics_sp0_np_index. mcp_gap_ics_sp0_np_index + S (ff_index_mcp_prefix_ics_sp0_np) = ((r) * (1))) -> exists ff_row_mcp_prefix_ics_sp0_np ff_column_mcp_prefix_ics_sp0_np ff_value_mcp_prefix_ics_sp0_np. ((ff_index_mcp_prefix_ics_sp0_np) = (1) * ff_row_mcp_prefix_ics_sp0_np + ff_column_mcp_prefix_ics_sp0_np /\ ((exists mcp_gap_ics_sp0_np_column. mcp_gap_ics_sp0_np_column + S (ff_column_mcp_prefix_ics_sp0_np) = (1)) /\ ((exists ff_left_mcp_cell_ics_sp0_np_cell ff_left_scale_mcp_cell_ics_sp0_np_cell ff_right_mcp_cell_ics_sp0_np_cell ff_right_scale_mcp_cell_ics_sp0_np_cell. ((forall ff_index_mcp_ics_sp0_np_cell_row ff_source_mcp_ics_sp0_np_cell_row ff_target_mcp_ics_sp0_np_cell_row. (exists mcp_gap_ics_sp0_np_cell_row_bound. mcp_gap_ics_sp0_np_cell_row_bound + S (ff_index_mcp_ics_sp0_np_cell_row) = (w)) -> (((exists fs_h_mcp_ics_sp0_np_cell_row_source. fs_h_mcp_ics_sp0_np_cell_row_source + S (ff_source_mcp_ics_sp0_np_cell_row) = S ((S (((ff_row_mcp_prefix_ics_sp0_np) * (w)) + (1) * ff_index_mcp_ics_sp0_np_cell_row)) * dc)) /\ exists fs_q_mcp_ics_sp0_np_cell_row_source. db = fs_q_mcp_ics_sp0_np_cell_row_source * S ((S (((ff_row_mcp_prefix_ics_sp0_np) * (w)) + (1) * ff_index_mcp_ics_sp0_np_cell_row)) * dc) + (ff_source_mcp_ics_sp0_np_cell_row))) -> (((exists fs_h_mcp_ics_sp0_np_cell_row_target. fs_h_mcp_ics_sp0_np_cell_row_target + S (ff_target_mcp_ics_sp0_np_cell_row) = S ((S (ff_index_mcp_ics_sp0_np_cell_row)) * ff_left_scale_mcp_cell_ics_sp0_np_cell)) /\ exists fs_q_mcp_ics_sp0_np_cell_row_target. ff_left_mcp_cell_ics_sp0_np_cell = fs_q_mcp_ics_sp0_np_cell_row_target * S ((S (ff_index_mcp_ics_sp0_np_cell_row)) * ff_left_scale_mcp_cell_ics_sp0_np_cell) + (ff_target_mcp_ics_sp0_np_cell_row))) -> ff_target_mcp_ics_sp0_np_cell_row = ff_source_mcp_ics_sp0_np_cell_row) /\ ((forall ff_index_mcp_ics_sp0_np_cell_column ff_source_mcp_ics_sp0_np_cell_column ff_target_mcp_ics_sp0_np_cell_column. (exists mcp_gap_ics_sp0_np_cell_column_bound. mcp_gap_ics_sp0_np_cell_column_bound + S (ff_index_mcp_ics_sp0_np_cell_column) = (w)) -> (((exists fs_h_mcp_ics_sp0_np_cell_column_source. fs_h_mcp_ics_sp0_np_cell_column_source + S (ff_source_mcp_ics_sp0_np_cell_column) = S ((S ((ff_column_mcp_prefix_ics_sp0_np) + (1) * ff_index_mcp_ics_sp0_np_cell_column)) * ec)) /\ exists fs_q_mcp_ics_sp0_np_cell_column_source. eb = fs_q_mcp_ics_sp0_np_cell_column_source * S ((S ((ff_column_mcp_prefix_ics_sp0_np) + (1) * ff_index_mcp_ics_sp0_np_cell_column)) * ec) + (ff_source_mcp_ics_sp0_np_cell_column))) -> (((exists fs_h_mcp_ics_sp0_np_cell_column_target. fs_h_mcp_ics_sp0_np_cell_column_target + S (ff_target_mcp_ics_sp0_np_cell_column) = S ((S (ff_index_mcp_ics_sp0_np_cell_column)) * ff_right_scale_mcp_cell_ics_sp0_np_cell)) /\ exists fs_q_mcp_ics_sp0_np_cell_column_target. ff_right_mcp_cell_ics_sp0_np_cell = fs_q_mcp_ics_sp0_np_cell_column_target * S ((S (ff_index_mcp_ics_sp0_np_cell_column)) * ff_right_scale_mcp_cell_ics_sp0_np_cell) + (ff_target_mcp_ics_sp0_np_cell_column))) -> ff_target_mcp_ics_sp0_np_cell_column = ff_source_mcp_ics_sp0_np_cell_column) /\ (exists ff_code_dot_mcp_ics_sp0_np_cell_dot ff_scale_dot_mcp_ics_sp0_np_cell_dot. ((forall fpmp_index_dot_mcp_ics_sp0_np_cell_dot_pointwise fpmp_left_dot_mcp_ics_sp0_np_cell_dot_pointwise fpmp_right_dot_mcp_ics_sp0_np_cell_dot_pointwise fpmp_target_dot_mcp_ics_sp0_np_cell_dot_pointwise. (exists fpmp_gap_dot_mcp_ics_sp0_np_cell_dot_pointwise. fpmp_gap_dot_mcp_ics_sp0_np_cell_dot_pointwise + S fpmp_index_dot_mcp_ics_sp0_np_cell_dot_pointwise = w) -> (((exists ff_h_fpmp_dot_mcp_ics_sp0_np_cell_dot_pointwise_left. ff_h_fpmp_dot_mcp_ics_sp0_np_cell_dot_pointwise_left + S (fpmp_left_dot_mcp_ics_sp0_np_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_sp0_np_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_sp0_np_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_sp0_np_cell_dot_pointwise_left. ff_left_mcp_cell_ics_sp0_np_cell = ff_q_fpmp_dot_mcp_ics_sp0_np_cell_dot_pointwise_left * S ((S (fpmp_index_dot_mcp_ics_sp0_np_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_sp0_np_cell) + (fpmp_left_dot_mcp_ics_sp0_np_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_sp0_np_cell_dot_pointwise_right. ff_h_fpmp_dot_mcp_ics_sp0_np_cell_dot_pointwise_right + S (fpmp_right_dot_mcp_ics_sp0_np_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_sp0_np_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_sp0_np_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_sp0_np_cell_dot_pointwise_right. ff_right_mcp_cell_ics_sp0_np_cell = ff_q_fpmp_dot_mcp_ics_sp0_np_cell_dot_pointwise_right * S ((S (fpmp_index_dot_mcp_ics_sp0_np_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_sp0_np_cell) + (fpmp_right_dot_mcp_ics_sp0_np_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_sp0_np_cell_dot_pointwise_target. ff_h_fpmp_dot_mcp_ics_sp0_np_cell_dot_pointwise_target + S (fpmp_target_dot_mcp_ics_sp0_np_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_sp0_np_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_sp0_np_cell_dot)) /\ exists ff_q_fpmp_dot_mcp_ics_sp0_np_cell_dot_pointwise_target. ff_code_dot_mcp_ics_sp0_np_cell_dot = ff_q_fpmp_dot_mcp_ics_sp0_np_cell_dot_pointwise_target * S ((S (fpmp_index_dot_mcp_ics_sp0_np_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_sp0_np_cell_dot) + (fpmp_target_dot_mcp_ics_sp0_np_cell_dot_pointwise))) -> fpmp_target_dot_mcp_ics_sp0_np_cell_dot_pointwise = fpmp_left_dot_mcp_ics_sp0_np_cell_dot_pointwise * fpmp_right_dot_mcp_ics_sp0_np_cell_dot_pointwise) /\ (exists ff_u_dot_mcp_ics_sp0_np_cell_dot_sum ff_v_dot_mcp_ics_sp0_np_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_sp0_np_cell_dot_sum_start. ff_h_dot_mcp_ics_sp0_np_cell_dot_sum_start + S (0) = S ((S (0)) * ff_v_dot_mcp_ics_sp0_np_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_sp0_np_cell_dot_sum_start. ff_u_dot_mcp_ics_sp0_np_cell_dot_sum = ff_q_dot_mcp_ics_sp0_np_cell_dot_sum_start * S ((S (0)) * ff_v_dot_mcp_ics_sp0_np_cell_dot_sum) + (0))) /\ ((((exists ff_h_dot_mcp_ics_sp0_np_cell_dot_sum_terminal. ff_h_dot_mcp_ics_sp0_np_cell_dot_sum_terminal + S (ff_value_mcp_prefix_ics_sp0_np) = S ((S (w)) * ff_v_dot_mcp_ics_sp0_np_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_sp0_np_cell_dot_sum_terminal. ff_u_dot_mcp_ics_sp0_np_cell_dot_sum = ff_q_dot_mcp_ics_sp0_np_cell_dot_sum_terminal * S ((S (w)) * ff_v_dot_mcp_ics_sp0_np_cell_dot_sum) + (ff_value_mcp_prefix_ics_sp0_np))) /\ forall ff_i_dot_mcp_ics_sp0_np_cell_dot_sum. (exists ff_lt_dot_mcp_ics_sp0_np_cell_dot_sum_bound. ff_lt_dot_mcp_ics_sp0_np_cell_dot_sum_bound + S ff_i_dot_mcp_ics_sp0_np_cell_dot_sum = w) -> exists ff_a_dot_mcp_ics_sp0_np_cell_dot_sum ff_r_dot_mcp_ics_sp0_np_cell_dot_sum ff_s_dot_mcp_ics_sp0_np_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_sp0_np_cell_dot_sum_summand. ff_h_dot_mcp_ics_sp0_np_cell_dot_sum_summand + S (ff_a_dot_mcp_ics_sp0_np_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_sp0_np_cell_dot_sum)) * ff_scale_dot_mcp_ics_sp0_np_cell_dot)) /\ exists ff_q_dot_mcp_ics_sp0_np_cell_dot_sum_summand. ff_code_dot_mcp_ics_sp0_np_cell_dot = ff_q_dot_mcp_ics_sp0_np_cell_dot_sum_summand * S ((S (ff_i_dot_mcp_ics_sp0_np_cell_dot_sum)) * ff_scale_dot_mcp_ics_sp0_np_cell_dot) + (ff_a_dot_mcp_ics_sp0_np_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_sp0_np_cell_dot_sum_partial. ff_h_dot_mcp_ics_sp0_np_cell_dot_sum_partial + S (ff_r_dot_mcp_ics_sp0_np_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_sp0_np_cell_dot_sum)) * ff_v_dot_mcp_ics_sp0_np_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_sp0_np_cell_dot_sum_partial. ff_u_dot_mcp_ics_sp0_np_cell_dot_sum = ff_q_dot_mcp_ics_sp0_np_cell_dot_sum_partial * S ((S (ff_i_dot_mcp_ics_sp0_np_cell_dot_sum)) * ff_v_dot_mcp_ics_sp0_np_cell_dot_sum) + (ff_r_dot_mcp_ics_sp0_np_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_sp0_np_cell_dot_sum_successor. ff_h_dot_mcp_ics_sp0_np_cell_dot_sum_successor + S (ff_s_dot_mcp_ics_sp0_np_cell_dot_sum) = S ((S (S ff_i_dot_mcp_ics_sp0_np_cell_dot_sum)) * ff_v_dot_mcp_ics_sp0_np_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_sp0_np_cell_dot_sum_successor. ff_u_dot_mcp_ics_sp0_np_cell_dot_sum = ff_q_dot_mcp_ics_sp0_np_cell_dot_sum_successor * S ((S (S ff_i_dot_mcp_ics_sp0_np_cell_dot_sum)) * ff_v_dot_mcp_ics_sp0_np_cell_dot_sum) + (ff_s_dot_mcp_ics_sp0_np_cell_dot_sum))) /\ ff_s_dot_mcp_ics_sp0_np_cell_dot_sum = ff_r_dot_mcp_ics_sp0_np_cell_dot_sum + ff_a_dot_mcp_ics_sp0_np_cell_dot_sum))))))))))) /\ (((exists fs_h_mcp_ics_sp0_np_entry. fs_h_mcp_ics_sp0_np_entry + S (ff_value_mcp_prefix_ics_sp0_np) = S ((S (ff_index_mcp_prefix_ics_sp0_np)) * ff_nps_mcp_smatrix_ics_sp0)) /\ exists fs_q_mcp_ics_sp0_np_entry. ff_np_mcp_smatrix_ics_sp0 = fs_q_mcp_ics_sp0_np_entry * S ((S (ff_index_mcp_prefix_ics_sp0_np)) * ff_nps_mcp_smatrix_ics_sp0) + (ff_value_mcp_prefix_ics_sp0_np))))))) /\ ((forall ff_index_mcp_add_ics_sp0_positive ff_left_mcp_add_ics_sp0_positive ff_right_mcp_add_ics_sp0_positive ff_target_mcp_add_ics_sp0_positive. (exists mcp_gap_ics_sp0_positive_bound. mcp_gap_ics_sp0_positive_bound + S (ff_index_mcp_add_ics_sp0_positive) = ((r) * (1))) -> (((exists fs_h_mcp_ics_sp0_positive_left. fs_h_mcp_ics_sp0_positive_left + S (ff_left_mcp_add_ics_sp0_positive) = S ((S (ff_index_mcp_add_ics_sp0_positive)) * ff_pps_mcp_smatrix_ics_sp0)) /\ exists fs_q_mcp_ics_sp0_positive_left. ff_pp_mcp_smatrix_ics_sp0 = fs_q_mcp_ics_sp0_positive_left * S ((S (ff_index_mcp_add_ics_sp0_positive)) * ff_pps_mcp_smatrix_ics_sp0) + (ff_left_mcp_add_ics_sp0_positive))) -> (((exists fs_h_mcp_ics_sp0_positive_right. fs_h_mcp_ics_sp0_positive_right + S (ff_right_mcp_add_ics_sp0_positive) = S ((S (ff_index_mcp_add_ics_sp0_positive)) * ff_nns_mcp_smatrix_ics_sp0)) /\ exists fs_q_mcp_ics_sp0_positive_right. ff_nn_mcp_smatrix_ics_sp0 = fs_q_mcp_ics_sp0_positive_right * S ((S (ff_index_mcp_add_ics_sp0_positive)) * ff_nns_mcp_smatrix_ics_sp0) + (ff_right_mcp_add_ics_sp0_positive))) -> (((exists fs_h_mcp_ics_sp0_positive_target. fs_h_mcp_ics_sp0_positive_target + S (ff_target_mcp_add_ics_sp0_positive) = S ((S (ff_index_mcp_add_ics_sp0_positive)) * pc)) /\ exists fs_q_mcp_ics_sp0_positive_target. pb = fs_q_mcp_ics_sp0_positive_target * S ((S (ff_index_mcp_add_ics_sp0_positive)) * pc) + (ff_target_mcp_add_ics_sp0_positive))) -> ff_target_mcp_add_ics_sp0_positive = ff_left_mcp_add_ics_sp0_positive + ff_right_mcp_add_ics_sp0_positive) /\ (forall ff_index_mcp_add_ics_sp0_negative ff_left_mcp_add_ics_sp0_negative ff_right_mcp_add_ics_sp0_negative ff_target_mcp_add_ics_sp0_negative. (exists mcp_gap_ics_sp0_negative_bound. mcp_gap_ics_sp0_negative_bound + S (ff_index_mcp_add_ics_sp0_negative) = ((r) * (1))) -> (((exists fs_h_mcp_ics_sp0_negative_left. fs_h_mcp_ics_sp0_negative_left + S (ff_left_mcp_add_ics_sp0_negative) = S ((S (ff_index_mcp_add_ics_sp0_negative)) * ff_pns_mcp_smatrix_ics_sp0)) /\ exists fs_q_mcp_ics_sp0_negative_left. ff_pn_mcp_smatrix_ics_sp0 = fs_q_mcp_ics_sp0_negative_left * S ((S (ff_index_mcp_add_ics_sp0_negative)) * ff_pns_mcp_smatrix_ics_sp0) + (ff_left_mcp_add_ics_sp0_negative))) -> (((exists fs_h_mcp_ics_sp0_negative_right. fs_h_mcp_ics_sp0_negative_right + S (ff_right_mcp_add_ics_sp0_negative) = S ((S (ff_index_mcp_add_ics_sp0_negative)) * ff_nps_mcp_smatrix_ics_sp0)) /\ exists fs_q_mcp_ics_sp0_negative_right. ff_np_mcp_smatrix_ics_sp0 = fs_q_mcp_ics_sp0_negative_right * S ((S (ff_index_mcp_add_ics_sp0_negative)) * ff_nps_mcp_smatrix_ics_sp0) + (ff_right_mcp_add_ics_sp0_negative))) -> (((exists fs_h_mcp_ics_sp0_negative_target. fs_h_mcp_ics_sp0_negative_target + S (ff_target_mcp_add_ics_sp0_negative) = S ((S (ff_index_mcp_add_ics_sp0_negative)) * nc)) /\ exists fs_q_mcp_ics_sp0_negative_target. nb = fs_q_mcp_ics_sp0_negative_target * S ((S (ff_index_mcp_add_ics_sp0_negative)) * nc) + (ff_target_mcp_add_ics_sp0_negative))) -> ff_target_mcp_add_ics_sp0_negative = ff_left_mcp_add_ics_sp0_negative + ff_right_mcp_add_ics_sp0_negative))))))) -> (exists ff_pp_mcp_smatrix_ics_sp1 ff_pps_mcp_smatrix_ics_sp1 ff_nn_mcp_smatrix_ics_sp1 ff_nns_mcp_smatrix_ics_sp1 ff_pn_mcp_smatrix_ics_sp1 ff_pns_mcp_smatrix_ics_sp1 ff_np_mcp_smatrix_ics_sp1 ff_nps_mcp_smatrix_ics_sp1. ((forall ff_index_mcp_prefix_ics_sp1_pp. (exists mcp_gap_ics_sp1_pp_index. mcp_gap_ics_sp1_pp_index + S (ff_index_mcp_prefix_ics_sp1_pp) = ((r) * (1))) -> exists ff_row_mcp_prefix_ics_sp1_pp ff_column_mcp_prefix_ics_sp1_pp ff_value_mcp_prefix_ics_sp1_pp. ((ff_index_mcp_prefix_ics_sp1_pp) = (1) * ff_row_mcp_prefix_ics_sp1_pp + ff_column_mcp_prefix_ics_sp1_pp /\ ((exists mcp_gap_ics_sp1_pp_column. mcp_gap_ics_sp1_pp_column + S (ff_column_mcp_prefix_ics_sp1_pp) = (1)) /\ ((exists ff_left_mcp_cell_ics_sp1_pp_cell ff_left_scale_mcp_cell_ics_sp1_pp_cell ff_right_mcp_cell_ics_sp1_pp_cell ff_right_scale_mcp_cell_ics_sp1_pp_cell. ((forall ff_index_mcp_ics_sp1_pp_cell_row ff_source_mcp_ics_sp1_pp_cell_row ff_target_mcp_ics_sp1_pp_cell_row. (exists mcp_gap_ics_sp1_pp_cell_row_bound. mcp_gap_ics_sp1_pp_cell_row_bound + S (ff_index_mcp_ics_sp1_pp_cell_row) = (w)) -> (((exists fs_h_mcp_ics_sp1_pp_cell_row_source. fs_h_mcp_ics_sp1_pp_cell_row_source + S (ff_source_mcp_ics_sp1_pp_cell_row) = S ((S (((ff_row_mcp_prefix_ics_sp1_pp) * (w)) + (1) * ff_index_mcp_ics_sp1_pp_cell_row)) * ac)) /\ exists fs_q_mcp_ics_sp1_pp_cell_row_source. ab = fs_q_mcp_ics_sp1_pp_cell_row_source * S ((S (((ff_row_mcp_prefix_ics_sp1_pp) * (w)) + (1) * ff_index_mcp_ics_sp1_pp_cell_row)) * ac) + (ff_source_mcp_ics_sp1_pp_cell_row))) -> (((exists fs_h_mcp_ics_sp1_pp_cell_row_target. fs_h_mcp_ics_sp1_pp_cell_row_target + S (ff_target_mcp_ics_sp1_pp_cell_row) = S ((S (ff_index_mcp_ics_sp1_pp_cell_row)) * ff_left_scale_mcp_cell_ics_sp1_pp_cell)) /\ exists fs_q_mcp_ics_sp1_pp_cell_row_target. ff_left_mcp_cell_ics_sp1_pp_cell = fs_q_mcp_ics_sp1_pp_cell_row_target * S ((S (ff_index_mcp_ics_sp1_pp_cell_row)) * ff_left_scale_mcp_cell_ics_sp1_pp_cell) + (ff_target_mcp_ics_sp1_pp_cell_row))) -> ff_target_mcp_ics_sp1_pp_cell_row = ff_source_mcp_ics_sp1_pp_cell_row) /\ ((forall ff_index_mcp_ics_sp1_pp_cell_column ff_source_mcp_ics_sp1_pp_cell_column ff_target_mcp_ics_sp1_pp_cell_column. (exists mcp_gap_ics_sp1_pp_cell_column_bound. mcp_gap_ics_sp1_pp_cell_column_bound + S (ff_index_mcp_ics_sp1_pp_cell_column) = (w)) -> (((exists fs_h_mcp_ics_sp1_pp_cell_column_source. fs_h_mcp_ics_sp1_pp_cell_column_source + S (ff_source_mcp_ics_sp1_pp_cell_column) = S ((S ((ff_column_mcp_prefix_ics_sp1_pp) + (1) * ff_index_mcp_ics_sp1_pp_cell_column)) * gc)) /\ exists fs_q_mcp_ics_sp1_pp_cell_column_source. gb = fs_q_mcp_ics_sp1_pp_cell_column_source * S ((S ((ff_column_mcp_prefix_ics_sp1_pp) + (1) * ff_index_mcp_ics_sp1_pp_cell_column)) * gc) + (ff_source_mcp_ics_sp1_pp_cell_column))) -> (((exists fs_h_mcp_ics_sp1_pp_cell_column_target. fs_h_mcp_ics_sp1_pp_cell_column_target + S (ff_target_mcp_ics_sp1_pp_cell_column) = S ((S (ff_index_mcp_ics_sp1_pp_cell_column)) * ff_right_scale_mcp_cell_ics_sp1_pp_cell)) /\ exists fs_q_mcp_ics_sp1_pp_cell_column_target. ff_right_mcp_cell_ics_sp1_pp_cell = fs_q_mcp_ics_sp1_pp_cell_column_target * S ((S (ff_index_mcp_ics_sp1_pp_cell_column)) * ff_right_scale_mcp_cell_ics_sp1_pp_cell) + (ff_target_mcp_ics_sp1_pp_cell_column))) -> ff_target_mcp_ics_sp1_pp_cell_column = ff_source_mcp_ics_sp1_pp_cell_column) /\ (exists ff_code_dot_mcp_ics_sp1_pp_cell_dot ff_scale_dot_mcp_ics_sp1_pp_cell_dot. ((forall fpmp_index_dot_mcp_ics_sp1_pp_cell_dot_pointwise fpmp_left_dot_mcp_ics_sp1_pp_cell_dot_pointwise fpmp_right_dot_mcp_ics_sp1_pp_cell_dot_pointwise fpmp_target_dot_mcp_ics_sp1_pp_cell_dot_pointwise. (exists fpmp_gap_dot_mcp_ics_sp1_pp_cell_dot_pointwise. fpmp_gap_dot_mcp_ics_sp1_pp_cell_dot_pointwise + S fpmp_index_dot_mcp_ics_sp1_pp_cell_dot_pointwise = w) -> (((exists ff_h_fpmp_dot_mcp_ics_sp1_pp_cell_dot_pointwise_left. ff_h_fpmp_dot_mcp_ics_sp1_pp_cell_dot_pointwise_left + S (fpmp_left_dot_mcp_ics_sp1_pp_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_sp1_pp_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_sp1_pp_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_sp1_pp_cell_dot_pointwise_left. ff_left_mcp_cell_ics_sp1_pp_cell = ff_q_fpmp_dot_mcp_ics_sp1_pp_cell_dot_pointwise_left * S ((S (fpmp_index_dot_mcp_ics_sp1_pp_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_sp1_pp_cell) + (fpmp_left_dot_mcp_ics_sp1_pp_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_sp1_pp_cell_dot_pointwise_right. ff_h_fpmp_dot_mcp_ics_sp1_pp_cell_dot_pointwise_right + S (fpmp_right_dot_mcp_ics_sp1_pp_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_sp1_pp_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_sp1_pp_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_sp1_pp_cell_dot_pointwise_right. ff_right_mcp_cell_ics_sp1_pp_cell = ff_q_fpmp_dot_mcp_ics_sp1_pp_cell_dot_pointwise_right * S ((S (fpmp_index_dot_mcp_ics_sp1_pp_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_sp1_pp_cell) + (fpmp_right_dot_mcp_ics_sp1_pp_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_sp1_pp_cell_dot_pointwise_target. ff_h_fpmp_dot_mcp_ics_sp1_pp_cell_dot_pointwise_target + S (fpmp_target_dot_mcp_ics_sp1_pp_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_sp1_pp_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_sp1_pp_cell_dot)) /\ exists ff_q_fpmp_dot_mcp_ics_sp1_pp_cell_dot_pointwise_target. ff_code_dot_mcp_ics_sp1_pp_cell_dot = ff_q_fpmp_dot_mcp_ics_sp1_pp_cell_dot_pointwise_target * S ((S (fpmp_index_dot_mcp_ics_sp1_pp_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_sp1_pp_cell_dot) + (fpmp_target_dot_mcp_ics_sp1_pp_cell_dot_pointwise))) -> fpmp_target_dot_mcp_ics_sp1_pp_cell_dot_pointwise = fpmp_left_dot_mcp_ics_sp1_pp_cell_dot_pointwise * fpmp_right_dot_mcp_ics_sp1_pp_cell_dot_pointwise) /\ (exists ff_u_dot_mcp_ics_sp1_pp_cell_dot_sum ff_v_dot_mcp_ics_sp1_pp_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_sp1_pp_cell_dot_sum_start. ff_h_dot_mcp_ics_sp1_pp_cell_dot_sum_start + S (0) = S ((S (0)) * ff_v_dot_mcp_ics_sp1_pp_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_sp1_pp_cell_dot_sum_start. ff_u_dot_mcp_ics_sp1_pp_cell_dot_sum = ff_q_dot_mcp_ics_sp1_pp_cell_dot_sum_start * S ((S (0)) * ff_v_dot_mcp_ics_sp1_pp_cell_dot_sum) + (0))) /\ ((((exists ff_h_dot_mcp_ics_sp1_pp_cell_dot_sum_terminal. ff_h_dot_mcp_ics_sp1_pp_cell_dot_sum_terminal + S (ff_value_mcp_prefix_ics_sp1_pp) = S ((S (w)) * ff_v_dot_mcp_ics_sp1_pp_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_sp1_pp_cell_dot_sum_terminal. ff_u_dot_mcp_ics_sp1_pp_cell_dot_sum = ff_q_dot_mcp_ics_sp1_pp_cell_dot_sum_terminal * S ((S (w)) * ff_v_dot_mcp_ics_sp1_pp_cell_dot_sum) + (ff_value_mcp_prefix_ics_sp1_pp))) /\ forall ff_i_dot_mcp_ics_sp1_pp_cell_dot_sum. (exists ff_lt_dot_mcp_ics_sp1_pp_cell_dot_sum_bound. ff_lt_dot_mcp_ics_sp1_pp_cell_dot_sum_bound + S ff_i_dot_mcp_ics_sp1_pp_cell_dot_sum = w) -> exists ff_a_dot_mcp_ics_sp1_pp_cell_dot_sum ff_r_dot_mcp_ics_sp1_pp_cell_dot_sum ff_s_dot_mcp_ics_sp1_pp_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_sp1_pp_cell_dot_sum_summand. ff_h_dot_mcp_ics_sp1_pp_cell_dot_sum_summand + S (ff_a_dot_mcp_ics_sp1_pp_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_sp1_pp_cell_dot_sum)) * ff_scale_dot_mcp_ics_sp1_pp_cell_dot)) /\ exists ff_q_dot_mcp_ics_sp1_pp_cell_dot_sum_summand. ff_code_dot_mcp_ics_sp1_pp_cell_dot = ff_q_dot_mcp_ics_sp1_pp_cell_dot_sum_summand * S ((S (ff_i_dot_mcp_ics_sp1_pp_cell_dot_sum)) * ff_scale_dot_mcp_ics_sp1_pp_cell_dot) + (ff_a_dot_mcp_ics_sp1_pp_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_sp1_pp_cell_dot_sum_partial. ff_h_dot_mcp_ics_sp1_pp_cell_dot_sum_partial + S (ff_r_dot_mcp_ics_sp1_pp_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_sp1_pp_cell_dot_sum)) * ff_v_dot_mcp_ics_sp1_pp_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_sp1_pp_cell_dot_sum_partial. ff_u_dot_mcp_ics_sp1_pp_cell_dot_sum = ff_q_dot_mcp_ics_sp1_pp_cell_dot_sum_partial * S ((S (ff_i_dot_mcp_ics_sp1_pp_cell_dot_sum)) * ff_v_dot_mcp_ics_sp1_pp_cell_dot_sum) + (ff_r_dot_mcp_ics_sp1_pp_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_sp1_pp_cell_dot_sum_successor. ff_h_dot_mcp_ics_sp1_pp_cell_dot_sum_successor + S (ff_s_dot_mcp_ics_sp1_pp_cell_dot_sum) = S ((S (S ff_i_dot_mcp_ics_sp1_pp_cell_dot_sum)) * ff_v_dot_mcp_ics_sp1_pp_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_sp1_pp_cell_dot_sum_successor. ff_u_dot_mcp_ics_sp1_pp_cell_dot_sum = ff_q_dot_mcp_ics_sp1_pp_cell_dot_sum_successor * S ((S (S ff_i_dot_mcp_ics_sp1_pp_cell_dot_sum)) * ff_v_dot_mcp_ics_sp1_pp_cell_dot_sum) + (ff_s_dot_mcp_ics_sp1_pp_cell_dot_sum))) /\ ff_s_dot_mcp_ics_sp1_pp_cell_dot_sum = ff_r_dot_mcp_ics_sp1_pp_cell_dot_sum + ff_a_dot_mcp_ics_sp1_pp_cell_dot_sum))))))))))) /\ (((exists fs_h_mcp_ics_sp1_pp_entry. fs_h_mcp_ics_sp1_pp_entry + S (ff_value_mcp_prefix_ics_sp1_pp) = S ((S (ff_index_mcp_prefix_ics_sp1_pp)) * ff_pps_mcp_smatrix_ics_sp1)) /\ exists fs_q_mcp_ics_sp1_pp_entry. ff_pp_mcp_smatrix_ics_sp1 = fs_q_mcp_ics_sp1_pp_entry * S ((S (ff_index_mcp_prefix_ics_sp1_pp)) * ff_pps_mcp_smatrix_ics_sp1) + (ff_value_mcp_prefix_ics_sp1_pp))))))) /\ ((forall ff_index_mcp_prefix_ics_sp1_nn. (exists mcp_gap_ics_sp1_nn_index. mcp_gap_ics_sp1_nn_index + S (ff_index_mcp_prefix_ics_sp1_nn) = ((r) * (1))) -> exists ff_row_mcp_prefix_ics_sp1_nn ff_column_mcp_prefix_ics_sp1_nn ff_value_mcp_prefix_ics_sp1_nn. ((ff_index_mcp_prefix_ics_sp1_nn) = (1) * ff_row_mcp_prefix_ics_sp1_nn + ff_column_mcp_prefix_ics_sp1_nn /\ ((exists mcp_gap_ics_sp1_nn_column. mcp_gap_ics_sp1_nn_column + S (ff_column_mcp_prefix_ics_sp1_nn) = (1)) /\ ((exists ff_left_mcp_cell_ics_sp1_nn_cell ff_left_scale_mcp_cell_ics_sp1_nn_cell ff_right_mcp_cell_ics_sp1_nn_cell ff_right_scale_mcp_cell_ics_sp1_nn_cell. ((forall ff_index_mcp_ics_sp1_nn_cell_row ff_source_mcp_ics_sp1_nn_cell_row ff_target_mcp_ics_sp1_nn_cell_row. (exists mcp_gap_ics_sp1_nn_cell_row_bound. mcp_gap_ics_sp1_nn_cell_row_bound + S (ff_index_mcp_ics_sp1_nn_cell_row) = (w)) -> (((exists fs_h_mcp_ics_sp1_nn_cell_row_source. fs_h_mcp_ics_sp1_nn_cell_row_source + S (ff_source_mcp_ics_sp1_nn_cell_row) = S ((S (((ff_row_mcp_prefix_ics_sp1_nn) * (w)) + (1) * ff_index_mcp_ics_sp1_nn_cell_row)) * dc)) /\ exists fs_q_mcp_ics_sp1_nn_cell_row_source. db = fs_q_mcp_ics_sp1_nn_cell_row_source * S ((S (((ff_row_mcp_prefix_ics_sp1_nn) * (w)) + (1) * ff_index_mcp_ics_sp1_nn_cell_row)) * dc) + (ff_source_mcp_ics_sp1_nn_cell_row))) -> (((exists fs_h_mcp_ics_sp1_nn_cell_row_target. fs_h_mcp_ics_sp1_nn_cell_row_target + S (ff_target_mcp_ics_sp1_nn_cell_row) = S ((S (ff_index_mcp_ics_sp1_nn_cell_row)) * ff_left_scale_mcp_cell_ics_sp1_nn_cell)) /\ exists fs_q_mcp_ics_sp1_nn_cell_row_target. ff_left_mcp_cell_ics_sp1_nn_cell = fs_q_mcp_ics_sp1_nn_cell_row_target * S ((S (ff_index_mcp_ics_sp1_nn_cell_row)) * ff_left_scale_mcp_cell_ics_sp1_nn_cell) + (ff_target_mcp_ics_sp1_nn_cell_row))) -> ff_target_mcp_ics_sp1_nn_cell_row = ff_source_mcp_ics_sp1_nn_cell_row) /\ ((forall ff_index_mcp_ics_sp1_nn_cell_column ff_source_mcp_ics_sp1_nn_cell_column ff_target_mcp_ics_sp1_nn_cell_column. (exists mcp_gap_ics_sp1_nn_cell_column_bound. mcp_gap_ics_sp1_nn_cell_column_bound + S (ff_index_mcp_ics_sp1_nn_cell_column) = (w)) -> (((exists fs_h_mcp_ics_sp1_nn_cell_column_source. fs_h_mcp_ics_sp1_nn_cell_column_source + S (ff_source_mcp_ics_sp1_nn_cell_column) = S ((S ((ff_column_mcp_prefix_ics_sp1_nn) + (1) * ff_index_mcp_ics_sp1_nn_cell_column)) * hc)) /\ exists fs_q_mcp_ics_sp1_nn_cell_column_source. hb = fs_q_mcp_ics_sp1_nn_cell_column_source * S ((S ((ff_column_mcp_prefix_ics_sp1_nn) + (1) * ff_index_mcp_ics_sp1_nn_cell_column)) * hc) + (ff_source_mcp_ics_sp1_nn_cell_column))) -> (((exists fs_h_mcp_ics_sp1_nn_cell_column_target. fs_h_mcp_ics_sp1_nn_cell_column_target + S (ff_target_mcp_ics_sp1_nn_cell_column) = S ((S (ff_index_mcp_ics_sp1_nn_cell_column)) * ff_right_scale_mcp_cell_ics_sp1_nn_cell)) /\ exists fs_q_mcp_ics_sp1_nn_cell_column_target. ff_right_mcp_cell_ics_sp1_nn_cell = fs_q_mcp_ics_sp1_nn_cell_column_target * S ((S (ff_index_mcp_ics_sp1_nn_cell_column)) * ff_right_scale_mcp_cell_ics_sp1_nn_cell) + (ff_target_mcp_ics_sp1_nn_cell_column))) -> ff_target_mcp_ics_sp1_nn_cell_column = ff_source_mcp_ics_sp1_nn_cell_column) /\ (exists ff_code_dot_mcp_ics_sp1_nn_cell_dot ff_scale_dot_mcp_ics_sp1_nn_cell_dot. ((forall fpmp_index_dot_mcp_ics_sp1_nn_cell_dot_pointwise fpmp_left_dot_mcp_ics_sp1_nn_cell_dot_pointwise fpmp_right_dot_mcp_ics_sp1_nn_cell_dot_pointwise fpmp_target_dot_mcp_ics_sp1_nn_cell_dot_pointwise. (exists fpmp_gap_dot_mcp_ics_sp1_nn_cell_dot_pointwise. fpmp_gap_dot_mcp_ics_sp1_nn_cell_dot_pointwise + S fpmp_index_dot_mcp_ics_sp1_nn_cell_dot_pointwise = w) -> (((exists ff_h_fpmp_dot_mcp_ics_sp1_nn_cell_dot_pointwise_left. ff_h_fpmp_dot_mcp_ics_sp1_nn_cell_dot_pointwise_left + S (fpmp_left_dot_mcp_ics_sp1_nn_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_sp1_nn_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_sp1_nn_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_sp1_nn_cell_dot_pointwise_left. ff_left_mcp_cell_ics_sp1_nn_cell = ff_q_fpmp_dot_mcp_ics_sp1_nn_cell_dot_pointwise_left * S ((S (fpmp_index_dot_mcp_ics_sp1_nn_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_sp1_nn_cell) + (fpmp_left_dot_mcp_ics_sp1_nn_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_sp1_nn_cell_dot_pointwise_right. ff_h_fpmp_dot_mcp_ics_sp1_nn_cell_dot_pointwise_right + S (fpmp_right_dot_mcp_ics_sp1_nn_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_sp1_nn_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_sp1_nn_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_sp1_nn_cell_dot_pointwise_right. ff_right_mcp_cell_ics_sp1_nn_cell = ff_q_fpmp_dot_mcp_ics_sp1_nn_cell_dot_pointwise_right * S ((S (fpmp_index_dot_mcp_ics_sp1_nn_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_sp1_nn_cell) + (fpmp_right_dot_mcp_ics_sp1_nn_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_sp1_nn_cell_dot_pointwise_target. ff_h_fpmp_dot_mcp_ics_sp1_nn_cell_dot_pointwise_target + S (fpmp_target_dot_mcp_ics_sp1_nn_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_sp1_nn_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_sp1_nn_cell_dot)) /\ exists ff_q_fpmp_dot_mcp_ics_sp1_nn_cell_dot_pointwise_target. ff_code_dot_mcp_ics_sp1_nn_cell_dot = ff_q_fpmp_dot_mcp_ics_sp1_nn_cell_dot_pointwise_target * S ((S (fpmp_index_dot_mcp_ics_sp1_nn_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_sp1_nn_cell_dot) + (fpmp_target_dot_mcp_ics_sp1_nn_cell_dot_pointwise))) -> fpmp_target_dot_mcp_ics_sp1_nn_cell_dot_pointwise = fpmp_left_dot_mcp_ics_sp1_nn_cell_dot_pointwise * fpmp_right_dot_mcp_ics_sp1_nn_cell_dot_pointwise) /\ (exists ff_u_dot_mcp_ics_sp1_nn_cell_dot_sum ff_v_dot_mcp_ics_sp1_nn_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_sp1_nn_cell_dot_sum_start. ff_h_dot_mcp_ics_sp1_nn_cell_dot_sum_start + S (0) = S ((S (0)) * ff_v_dot_mcp_ics_sp1_nn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_sp1_nn_cell_dot_sum_start. ff_u_dot_mcp_ics_sp1_nn_cell_dot_sum = ff_q_dot_mcp_ics_sp1_nn_cell_dot_sum_start * S ((S (0)) * ff_v_dot_mcp_ics_sp1_nn_cell_dot_sum) + (0))) /\ ((((exists ff_h_dot_mcp_ics_sp1_nn_cell_dot_sum_terminal. ff_h_dot_mcp_ics_sp1_nn_cell_dot_sum_terminal + S (ff_value_mcp_prefix_ics_sp1_nn) = S ((S (w)) * ff_v_dot_mcp_ics_sp1_nn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_sp1_nn_cell_dot_sum_terminal. ff_u_dot_mcp_ics_sp1_nn_cell_dot_sum = ff_q_dot_mcp_ics_sp1_nn_cell_dot_sum_terminal * S ((S (w)) * ff_v_dot_mcp_ics_sp1_nn_cell_dot_sum) + (ff_value_mcp_prefix_ics_sp1_nn))) /\ forall ff_i_dot_mcp_ics_sp1_nn_cell_dot_sum. (exists ff_lt_dot_mcp_ics_sp1_nn_cell_dot_sum_bound. ff_lt_dot_mcp_ics_sp1_nn_cell_dot_sum_bound + S ff_i_dot_mcp_ics_sp1_nn_cell_dot_sum = w) -> exists ff_a_dot_mcp_ics_sp1_nn_cell_dot_sum ff_r_dot_mcp_ics_sp1_nn_cell_dot_sum ff_s_dot_mcp_ics_sp1_nn_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_sp1_nn_cell_dot_sum_summand. ff_h_dot_mcp_ics_sp1_nn_cell_dot_sum_summand + S (ff_a_dot_mcp_ics_sp1_nn_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_sp1_nn_cell_dot_sum)) * ff_scale_dot_mcp_ics_sp1_nn_cell_dot)) /\ exists ff_q_dot_mcp_ics_sp1_nn_cell_dot_sum_summand. ff_code_dot_mcp_ics_sp1_nn_cell_dot = ff_q_dot_mcp_ics_sp1_nn_cell_dot_sum_summand * S ((S (ff_i_dot_mcp_ics_sp1_nn_cell_dot_sum)) * ff_scale_dot_mcp_ics_sp1_nn_cell_dot) + (ff_a_dot_mcp_ics_sp1_nn_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_sp1_nn_cell_dot_sum_partial. ff_h_dot_mcp_ics_sp1_nn_cell_dot_sum_partial + S (ff_r_dot_mcp_ics_sp1_nn_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_sp1_nn_cell_dot_sum)) * ff_v_dot_mcp_ics_sp1_nn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_sp1_nn_cell_dot_sum_partial. ff_u_dot_mcp_ics_sp1_nn_cell_dot_sum = ff_q_dot_mcp_ics_sp1_nn_cell_dot_sum_partial * S ((S (ff_i_dot_mcp_ics_sp1_nn_cell_dot_sum)) * ff_v_dot_mcp_ics_sp1_nn_cell_dot_sum) + (ff_r_dot_mcp_ics_sp1_nn_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_sp1_nn_cell_dot_sum_successor. ff_h_dot_mcp_ics_sp1_nn_cell_dot_sum_successor + S (ff_s_dot_mcp_ics_sp1_nn_cell_dot_sum) = S ((S (S ff_i_dot_mcp_ics_sp1_nn_cell_dot_sum)) * ff_v_dot_mcp_ics_sp1_nn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_sp1_nn_cell_dot_sum_successor. ff_u_dot_mcp_ics_sp1_nn_cell_dot_sum = ff_q_dot_mcp_ics_sp1_nn_cell_dot_sum_successor * S ((S (S ff_i_dot_mcp_ics_sp1_nn_cell_dot_sum)) * ff_v_dot_mcp_ics_sp1_nn_cell_dot_sum) + (ff_s_dot_mcp_ics_sp1_nn_cell_dot_sum))) /\ ff_s_dot_mcp_ics_sp1_nn_cell_dot_sum = ff_r_dot_mcp_ics_sp1_nn_cell_dot_sum + ff_a_dot_mcp_ics_sp1_nn_cell_dot_sum))))))))))) /\ (((exists fs_h_mcp_ics_sp1_nn_entry. fs_h_mcp_ics_sp1_nn_entry + S (ff_value_mcp_prefix_ics_sp1_nn) = S ((S (ff_index_mcp_prefix_ics_sp1_nn)) * ff_nns_mcp_smatrix_ics_sp1)) /\ exists fs_q_mcp_ics_sp1_nn_entry. ff_nn_mcp_smatrix_ics_sp1 = fs_q_mcp_ics_sp1_nn_entry * S ((S (ff_index_mcp_prefix_ics_sp1_nn)) * ff_nns_mcp_smatrix_ics_sp1) + (ff_value_mcp_prefix_ics_sp1_nn))))))) /\ ((forall ff_index_mcp_prefix_ics_sp1_pn. (exists mcp_gap_ics_sp1_pn_index. mcp_gap_ics_sp1_pn_index + S (ff_index_mcp_prefix_ics_sp1_pn) = ((r) * (1))) -> exists ff_row_mcp_prefix_ics_sp1_pn ff_column_mcp_prefix_ics_sp1_pn ff_value_mcp_prefix_ics_sp1_pn. ((ff_index_mcp_prefix_ics_sp1_pn) = (1) * ff_row_mcp_prefix_ics_sp1_pn + ff_column_mcp_prefix_ics_sp1_pn /\ ((exists mcp_gap_ics_sp1_pn_column. mcp_gap_ics_sp1_pn_column + S (ff_column_mcp_prefix_ics_sp1_pn) = (1)) /\ ((exists ff_left_mcp_cell_ics_sp1_pn_cell ff_left_scale_mcp_cell_ics_sp1_pn_cell ff_right_mcp_cell_ics_sp1_pn_cell ff_right_scale_mcp_cell_ics_sp1_pn_cell. ((forall ff_index_mcp_ics_sp1_pn_cell_row ff_source_mcp_ics_sp1_pn_cell_row ff_target_mcp_ics_sp1_pn_cell_row. (exists mcp_gap_ics_sp1_pn_cell_row_bound. mcp_gap_ics_sp1_pn_cell_row_bound + S (ff_index_mcp_ics_sp1_pn_cell_row) = (w)) -> (((exists fs_h_mcp_ics_sp1_pn_cell_row_source. fs_h_mcp_ics_sp1_pn_cell_row_source + S (ff_source_mcp_ics_sp1_pn_cell_row) = S ((S (((ff_row_mcp_prefix_ics_sp1_pn) * (w)) + (1) * ff_index_mcp_ics_sp1_pn_cell_row)) * ac)) /\ exists fs_q_mcp_ics_sp1_pn_cell_row_source. ab = fs_q_mcp_ics_sp1_pn_cell_row_source * S ((S (((ff_row_mcp_prefix_ics_sp1_pn) * (w)) + (1) * ff_index_mcp_ics_sp1_pn_cell_row)) * ac) + (ff_source_mcp_ics_sp1_pn_cell_row))) -> (((exists fs_h_mcp_ics_sp1_pn_cell_row_target. fs_h_mcp_ics_sp1_pn_cell_row_target + S (ff_target_mcp_ics_sp1_pn_cell_row) = S ((S (ff_index_mcp_ics_sp1_pn_cell_row)) * ff_left_scale_mcp_cell_ics_sp1_pn_cell)) /\ exists fs_q_mcp_ics_sp1_pn_cell_row_target. ff_left_mcp_cell_ics_sp1_pn_cell = fs_q_mcp_ics_sp1_pn_cell_row_target * S ((S (ff_index_mcp_ics_sp1_pn_cell_row)) * ff_left_scale_mcp_cell_ics_sp1_pn_cell) + (ff_target_mcp_ics_sp1_pn_cell_row))) -> ff_target_mcp_ics_sp1_pn_cell_row = ff_source_mcp_ics_sp1_pn_cell_row) /\ ((forall ff_index_mcp_ics_sp1_pn_cell_column ff_source_mcp_ics_sp1_pn_cell_column ff_target_mcp_ics_sp1_pn_cell_column. (exists mcp_gap_ics_sp1_pn_cell_column_bound. mcp_gap_ics_sp1_pn_cell_column_bound + S (ff_index_mcp_ics_sp1_pn_cell_column) = (w)) -> (((exists fs_h_mcp_ics_sp1_pn_cell_column_source. fs_h_mcp_ics_sp1_pn_cell_column_source + S (ff_source_mcp_ics_sp1_pn_cell_column) = S ((S ((ff_column_mcp_prefix_ics_sp1_pn) + (1) * ff_index_mcp_ics_sp1_pn_cell_column)) * hc)) /\ exists fs_q_mcp_ics_sp1_pn_cell_column_source. hb = fs_q_mcp_ics_sp1_pn_cell_column_source * S ((S ((ff_column_mcp_prefix_ics_sp1_pn) + (1) * ff_index_mcp_ics_sp1_pn_cell_column)) * hc) + (ff_source_mcp_ics_sp1_pn_cell_column))) -> (((exists fs_h_mcp_ics_sp1_pn_cell_column_target. fs_h_mcp_ics_sp1_pn_cell_column_target + S (ff_target_mcp_ics_sp1_pn_cell_column) = S ((S (ff_index_mcp_ics_sp1_pn_cell_column)) * ff_right_scale_mcp_cell_ics_sp1_pn_cell)) /\ exists fs_q_mcp_ics_sp1_pn_cell_column_target. ff_right_mcp_cell_ics_sp1_pn_cell = fs_q_mcp_ics_sp1_pn_cell_column_target * S ((S (ff_index_mcp_ics_sp1_pn_cell_column)) * ff_right_scale_mcp_cell_ics_sp1_pn_cell) + (ff_target_mcp_ics_sp1_pn_cell_column))) -> ff_target_mcp_ics_sp1_pn_cell_column = ff_source_mcp_ics_sp1_pn_cell_column) /\ (exists ff_code_dot_mcp_ics_sp1_pn_cell_dot ff_scale_dot_mcp_ics_sp1_pn_cell_dot. ((forall fpmp_index_dot_mcp_ics_sp1_pn_cell_dot_pointwise fpmp_left_dot_mcp_ics_sp1_pn_cell_dot_pointwise fpmp_right_dot_mcp_ics_sp1_pn_cell_dot_pointwise fpmp_target_dot_mcp_ics_sp1_pn_cell_dot_pointwise. (exists fpmp_gap_dot_mcp_ics_sp1_pn_cell_dot_pointwise. fpmp_gap_dot_mcp_ics_sp1_pn_cell_dot_pointwise + S fpmp_index_dot_mcp_ics_sp1_pn_cell_dot_pointwise = w) -> (((exists ff_h_fpmp_dot_mcp_ics_sp1_pn_cell_dot_pointwise_left. ff_h_fpmp_dot_mcp_ics_sp1_pn_cell_dot_pointwise_left + S (fpmp_left_dot_mcp_ics_sp1_pn_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_sp1_pn_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_sp1_pn_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_sp1_pn_cell_dot_pointwise_left. ff_left_mcp_cell_ics_sp1_pn_cell = ff_q_fpmp_dot_mcp_ics_sp1_pn_cell_dot_pointwise_left * S ((S (fpmp_index_dot_mcp_ics_sp1_pn_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_sp1_pn_cell) + (fpmp_left_dot_mcp_ics_sp1_pn_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_sp1_pn_cell_dot_pointwise_right. ff_h_fpmp_dot_mcp_ics_sp1_pn_cell_dot_pointwise_right + S (fpmp_right_dot_mcp_ics_sp1_pn_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_sp1_pn_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_sp1_pn_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_sp1_pn_cell_dot_pointwise_right. ff_right_mcp_cell_ics_sp1_pn_cell = ff_q_fpmp_dot_mcp_ics_sp1_pn_cell_dot_pointwise_right * S ((S (fpmp_index_dot_mcp_ics_sp1_pn_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_sp1_pn_cell) + (fpmp_right_dot_mcp_ics_sp1_pn_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_sp1_pn_cell_dot_pointwise_target. ff_h_fpmp_dot_mcp_ics_sp1_pn_cell_dot_pointwise_target + S (fpmp_target_dot_mcp_ics_sp1_pn_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_sp1_pn_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_sp1_pn_cell_dot)) /\ exists ff_q_fpmp_dot_mcp_ics_sp1_pn_cell_dot_pointwise_target. ff_code_dot_mcp_ics_sp1_pn_cell_dot = ff_q_fpmp_dot_mcp_ics_sp1_pn_cell_dot_pointwise_target * S ((S (fpmp_index_dot_mcp_ics_sp1_pn_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_sp1_pn_cell_dot) + (fpmp_target_dot_mcp_ics_sp1_pn_cell_dot_pointwise))) -> fpmp_target_dot_mcp_ics_sp1_pn_cell_dot_pointwise = fpmp_left_dot_mcp_ics_sp1_pn_cell_dot_pointwise * fpmp_right_dot_mcp_ics_sp1_pn_cell_dot_pointwise) /\ (exists ff_u_dot_mcp_ics_sp1_pn_cell_dot_sum ff_v_dot_mcp_ics_sp1_pn_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_sp1_pn_cell_dot_sum_start. ff_h_dot_mcp_ics_sp1_pn_cell_dot_sum_start + S (0) = S ((S (0)) * ff_v_dot_mcp_ics_sp1_pn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_sp1_pn_cell_dot_sum_start. ff_u_dot_mcp_ics_sp1_pn_cell_dot_sum = ff_q_dot_mcp_ics_sp1_pn_cell_dot_sum_start * S ((S (0)) * ff_v_dot_mcp_ics_sp1_pn_cell_dot_sum) + (0))) /\ ((((exists ff_h_dot_mcp_ics_sp1_pn_cell_dot_sum_terminal. ff_h_dot_mcp_ics_sp1_pn_cell_dot_sum_terminal + S (ff_value_mcp_prefix_ics_sp1_pn) = S ((S (w)) * ff_v_dot_mcp_ics_sp1_pn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_sp1_pn_cell_dot_sum_terminal. ff_u_dot_mcp_ics_sp1_pn_cell_dot_sum = ff_q_dot_mcp_ics_sp1_pn_cell_dot_sum_terminal * S ((S (w)) * ff_v_dot_mcp_ics_sp1_pn_cell_dot_sum) + (ff_value_mcp_prefix_ics_sp1_pn))) /\ forall ff_i_dot_mcp_ics_sp1_pn_cell_dot_sum. (exists ff_lt_dot_mcp_ics_sp1_pn_cell_dot_sum_bound. ff_lt_dot_mcp_ics_sp1_pn_cell_dot_sum_bound + S ff_i_dot_mcp_ics_sp1_pn_cell_dot_sum = w) -> exists ff_a_dot_mcp_ics_sp1_pn_cell_dot_sum ff_r_dot_mcp_ics_sp1_pn_cell_dot_sum ff_s_dot_mcp_ics_sp1_pn_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_sp1_pn_cell_dot_sum_summand. ff_h_dot_mcp_ics_sp1_pn_cell_dot_sum_summand + S (ff_a_dot_mcp_ics_sp1_pn_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_sp1_pn_cell_dot_sum)) * ff_scale_dot_mcp_ics_sp1_pn_cell_dot)) /\ exists ff_q_dot_mcp_ics_sp1_pn_cell_dot_sum_summand. ff_code_dot_mcp_ics_sp1_pn_cell_dot = ff_q_dot_mcp_ics_sp1_pn_cell_dot_sum_summand * S ((S (ff_i_dot_mcp_ics_sp1_pn_cell_dot_sum)) * ff_scale_dot_mcp_ics_sp1_pn_cell_dot) + (ff_a_dot_mcp_ics_sp1_pn_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_sp1_pn_cell_dot_sum_partial. ff_h_dot_mcp_ics_sp1_pn_cell_dot_sum_partial + S (ff_r_dot_mcp_ics_sp1_pn_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_sp1_pn_cell_dot_sum)) * ff_v_dot_mcp_ics_sp1_pn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_sp1_pn_cell_dot_sum_partial. ff_u_dot_mcp_ics_sp1_pn_cell_dot_sum = ff_q_dot_mcp_ics_sp1_pn_cell_dot_sum_partial * S ((S (ff_i_dot_mcp_ics_sp1_pn_cell_dot_sum)) * ff_v_dot_mcp_ics_sp1_pn_cell_dot_sum) + (ff_r_dot_mcp_ics_sp1_pn_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_sp1_pn_cell_dot_sum_successor. ff_h_dot_mcp_ics_sp1_pn_cell_dot_sum_successor + S (ff_s_dot_mcp_ics_sp1_pn_cell_dot_sum) = S ((S (S ff_i_dot_mcp_ics_sp1_pn_cell_dot_sum)) * ff_v_dot_mcp_ics_sp1_pn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_sp1_pn_cell_dot_sum_successor. ff_u_dot_mcp_ics_sp1_pn_cell_dot_sum = ff_q_dot_mcp_ics_sp1_pn_cell_dot_sum_successor * S ((S (S ff_i_dot_mcp_ics_sp1_pn_cell_dot_sum)) * ff_v_dot_mcp_ics_sp1_pn_cell_dot_sum) + (ff_s_dot_mcp_ics_sp1_pn_cell_dot_sum))) /\ ff_s_dot_mcp_ics_sp1_pn_cell_dot_sum = ff_r_dot_mcp_ics_sp1_pn_cell_dot_sum + ff_a_dot_mcp_ics_sp1_pn_cell_dot_sum))))))))))) /\ (((exists fs_h_mcp_ics_sp1_pn_entry. fs_h_mcp_ics_sp1_pn_entry + S (ff_value_mcp_prefix_ics_sp1_pn) = S ((S (ff_index_mcp_prefix_ics_sp1_pn)) * ff_pns_mcp_smatrix_ics_sp1)) /\ exists fs_q_mcp_ics_sp1_pn_entry. ff_pn_mcp_smatrix_ics_sp1 = fs_q_mcp_ics_sp1_pn_entry * S ((S (ff_index_mcp_prefix_ics_sp1_pn)) * ff_pns_mcp_smatrix_ics_sp1) + (ff_value_mcp_prefix_ics_sp1_pn))))))) /\ ((forall ff_index_mcp_prefix_ics_sp1_np. (exists mcp_gap_ics_sp1_np_index. mcp_gap_ics_sp1_np_index + S (ff_index_mcp_prefix_ics_sp1_np) = ((r) * (1))) -> exists ff_row_mcp_prefix_ics_sp1_np ff_column_mcp_prefix_ics_sp1_np ff_value_mcp_prefix_ics_sp1_np. ((ff_index_mcp_prefix_ics_sp1_np) = (1) * ff_row_mcp_prefix_ics_sp1_np + ff_column_mcp_prefix_ics_sp1_np /\ ((exists mcp_gap_ics_sp1_np_column. mcp_gap_ics_sp1_np_column + S (ff_column_mcp_prefix_ics_sp1_np) = (1)) /\ ((exists ff_left_mcp_cell_ics_sp1_np_cell ff_left_scale_mcp_cell_ics_sp1_np_cell ff_right_mcp_cell_ics_sp1_np_cell ff_right_scale_mcp_cell_ics_sp1_np_cell. ((forall ff_index_mcp_ics_sp1_np_cell_row ff_source_mcp_ics_sp1_np_cell_row ff_target_mcp_ics_sp1_np_cell_row. (exists mcp_gap_ics_sp1_np_cell_row_bound. mcp_gap_ics_sp1_np_cell_row_bound + S (ff_index_mcp_ics_sp1_np_cell_row) = (w)) -> (((exists fs_h_mcp_ics_sp1_np_cell_row_source. fs_h_mcp_ics_sp1_np_cell_row_source + S (ff_source_mcp_ics_sp1_np_cell_row) = S ((S (((ff_row_mcp_prefix_ics_sp1_np) * (w)) + (1) * ff_index_mcp_ics_sp1_np_cell_row)) * dc)) /\ exists fs_q_mcp_ics_sp1_np_cell_row_source. db = fs_q_mcp_ics_sp1_np_cell_row_source * S ((S (((ff_row_mcp_prefix_ics_sp1_np) * (w)) + (1) * ff_index_mcp_ics_sp1_np_cell_row)) * dc) + (ff_source_mcp_ics_sp1_np_cell_row))) -> (((exists fs_h_mcp_ics_sp1_np_cell_row_target. fs_h_mcp_ics_sp1_np_cell_row_target + S (ff_target_mcp_ics_sp1_np_cell_row) = S ((S (ff_index_mcp_ics_sp1_np_cell_row)) * ff_left_scale_mcp_cell_ics_sp1_np_cell)) /\ exists fs_q_mcp_ics_sp1_np_cell_row_target. ff_left_mcp_cell_ics_sp1_np_cell = fs_q_mcp_ics_sp1_np_cell_row_target * S ((S (ff_index_mcp_ics_sp1_np_cell_row)) * ff_left_scale_mcp_cell_ics_sp1_np_cell) + (ff_target_mcp_ics_sp1_np_cell_row))) -> ff_target_mcp_ics_sp1_np_cell_row = ff_source_mcp_ics_sp1_np_cell_row) /\ ((forall ff_index_mcp_ics_sp1_np_cell_column ff_source_mcp_ics_sp1_np_cell_column ff_target_mcp_ics_sp1_np_cell_column. (exists mcp_gap_ics_sp1_np_cell_column_bound. mcp_gap_ics_sp1_np_cell_column_bound + S (ff_index_mcp_ics_sp1_np_cell_column) = (w)) -> (((exists fs_h_mcp_ics_sp1_np_cell_column_source. fs_h_mcp_ics_sp1_np_cell_column_source + S (ff_source_mcp_ics_sp1_np_cell_column) = S ((S ((ff_column_mcp_prefix_ics_sp1_np) + (1) * ff_index_mcp_ics_sp1_np_cell_column)) * gc)) /\ exists fs_q_mcp_ics_sp1_np_cell_column_source. gb = fs_q_mcp_ics_sp1_np_cell_column_source * S ((S ((ff_column_mcp_prefix_ics_sp1_np) + (1) * ff_index_mcp_ics_sp1_np_cell_column)) * gc) + (ff_source_mcp_ics_sp1_np_cell_column))) -> (((exists fs_h_mcp_ics_sp1_np_cell_column_target. fs_h_mcp_ics_sp1_np_cell_column_target + S (ff_target_mcp_ics_sp1_np_cell_column) = S ((S (ff_index_mcp_ics_sp1_np_cell_column)) * ff_right_scale_mcp_cell_ics_sp1_np_cell)) /\ exists fs_q_mcp_ics_sp1_np_cell_column_target. ff_right_mcp_cell_ics_sp1_np_cell = fs_q_mcp_ics_sp1_np_cell_column_target * S ((S (ff_index_mcp_ics_sp1_np_cell_column)) * ff_right_scale_mcp_cell_ics_sp1_np_cell) + (ff_target_mcp_ics_sp1_np_cell_column))) -> ff_target_mcp_ics_sp1_np_cell_column = ff_source_mcp_ics_sp1_np_cell_column) /\ (exists ff_code_dot_mcp_ics_sp1_np_cell_dot ff_scale_dot_mcp_ics_sp1_np_cell_dot. ((forall fpmp_index_dot_mcp_ics_sp1_np_cell_dot_pointwise fpmp_left_dot_mcp_ics_sp1_np_cell_dot_pointwise fpmp_right_dot_mcp_ics_sp1_np_cell_dot_pointwise fpmp_target_dot_mcp_ics_sp1_np_cell_dot_pointwise. (exists fpmp_gap_dot_mcp_ics_sp1_np_cell_dot_pointwise. fpmp_gap_dot_mcp_ics_sp1_np_cell_dot_pointwise + S fpmp_index_dot_mcp_ics_sp1_np_cell_dot_pointwise = w) -> (((exists ff_h_fpmp_dot_mcp_ics_sp1_np_cell_dot_pointwise_left. ff_h_fpmp_dot_mcp_ics_sp1_np_cell_dot_pointwise_left + S (fpmp_left_dot_mcp_ics_sp1_np_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_sp1_np_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_sp1_np_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_sp1_np_cell_dot_pointwise_left. ff_left_mcp_cell_ics_sp1_np_cell = ff_q_fpmp_dot_mcp_ics_sp1_np_cell_dot_pointwise_left * S ((S (fpmp_index_dot_mcp_ics_sp1_np_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_sp1_np_cell) + (fpmp_left_dot_mcp_ics_sp1_np_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_sp1_np_cell_dot_pointwise_right. ff_h_fpmp_dot_mcp_ics_sp1_np_cell_dot_pointwise_right + S (fpmp_right_dot_mcp_ics_sp1_np_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_sp1_np_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_sp1_np_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_sp1_np_cell_dot_pointwise_right. ff_right_mcp_cell_ics_sp1_np_cell = ff_q_fpmp_dot_mcp_ics_sp1_np_cell_dot_pointwise_right * S ((S (fpmp_index_dot_mcp_ics_sp1_np_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_sp1_np_cell) + (fpmp_right_dot_mcp_ics_sp1_np_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_sp1_np_cell_dot_pointwise_target. ff_h_fpmp_dot_mcp_ics_sp1_np_cell_dot_pointwise_target + S (fpmp_target_dot_mcp_ics_sp1_np_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_sp1_np_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_sp1_np_cell_dot)) /\ exists ff_q_fpmp_dot_mcp_ics_sp1_np_cell_dot_pointwise_target. ff_code_dot_mcp_ics_sp1_np_cell_dot = ff_q_fpmp_dot_mcp_ics_sp1_np_cell_dot_pointwise_target * S ((S (fpmp_index_dot_mcp_ics_sp1_np_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_sp1_np_cell_dot) + (fpmp_target_dot_mcp_ics_sp1_np_cell_dot_pointwise))) -> fpmp_target_dot_mcp_ics_sp1_np_cell_dot_pointwise = fpmp_left_dot_mcp_ics_sp1_np_cell_dot_pointwise * fpmp_right_dot_mcp_ics_sp1_np_cell_dot_pointwise) /\ (exists ff_u_dot_mcp_ics_sp1_np_cell_dot_sum ff_v_dot_mcp_ics_sp1_np_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_sp1_np_cell_dot_sum_start. ff_h_dot_mcp_ics_sp1_np_cell_dot_sum_start + S (0) = S ((S (0)) * ff_v_dot_mcp_ics_sp1_np_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_sp1_np_cell_dot_sum_start. ff_u_dot_mcp_ics_sp1_np_cell_dot_sum = ff_q_dot_mcp_ics_sp1_np_cell_dot_sum_start * S ((S (0)) * ff_v_dot_mcp_ics_sp1_np_cell_dot_sum) + (0))) /\ ((((exists ff_h_dot_mcp_ics_sp1_np_cell_dot_sum_terminal. ff_h_dot_mcp_ics_sp1_np_cell_dot_sum_terminal + S (ff_value_mcp_prefix_ics_sp1_np) = S ((S (w)) * ff_v_dot_mcp_ics_sp1_np_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_sp1_np_cell_dot_sum_terminal. ff_u_dot_mcp_ics_sp1_np_cell_dot_sum = ff_q_dot_mcp_ics_sp1_np_cell_dot_sum_terminal * S ((S (w)) * ff_v_dot_mcp_ics_sp1_np_cell_dot_sum) + (ff_value_mcp_prefix_ics_sp1_np))) /\ forall ff_i_dot_mcp_ics_sp1_np_cell_dot_sum. (exists ff_lt_dot_mcp_ics_sp1_np_cell_dot_sum_bound. ff_lt_dot_mcp_ics_sp1_np_cell_dot_sum_bound + S ff_i_dot_mcp_ics_sp1_np_cell_dot_sum = w) -> exists ff_a_dot_mcp_ics_sp1_np_cell_dot_sum ff_r_dot_mcp_ics_sp1_np_cell_dot_sum ff_s_dot_mcp_ics_sp1_np_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_sp1_np_cell_dot_sum_summand. ff_h_dot_mcp_ics_sp1_np_cell_dot_sum_summand + S (ff_a_dot_mcp_ics_sp1_np_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_sp1_np_cell_dot_sum)) * ff_scale_dot_mcp_ics_sp1_np_cell_dot)) /\ exists ff_q_dot_mcp_ics_sp1_np_cell_dot_sum_summand. ff_code_dot_mcp_ics_sp1_np_cell_dot = ff_q_dot_mcp_ics_sp1_np_cell_dot_sum_summand * S ((S (ff_i_dot_mcp_ics_sp1_np_cell_dot_sum)) * ff_scale_dot_mcp_ics_sp1_np_cell_dot) + (ff_a_dot_mcp_ics_sp1_np_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_sp1_np_cell_dot_sum_partial. ff_h_dot_mcp_ics_sp1_np_cell_dot_sum_partial + S (ff_r_dot_mcp_ics_sp1_np_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_sp1_np_cell_dot_sum)) * ff_v_dot_mcp_ics_sp1_np_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_sp1_np_cell_dot_sum_partial. ff_u_dot_mcp_ics_sp1_np_cell_dot_sum = ff_q_dot_mcp_ics_sp1_np_cell_dot_sum_partial * S ((S (ff_i_dot_mcp_ics_sp1_np_cell_dot_sum)) * ff_v_dot_mcp_ics_sp1_np_cell_dot_sum) + (ff_r_dot_mcp_ics_sp1_np_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_sp1_np_cell_dot_sum_successor. ff_h_dot_mcp_ics_sp1_np_cell_dot_sum_successor + S (ff_s_dot_mcp_ics_sp1_np_cell_dot_sum) = S ((S (S ff_i_dot_mcp_ics_sp1_np_cell_dot_sum)) * ff_v_dot_mcp_ics_sp1_np_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_sp1_np_cell_dot_sum_successor. ff_u_dot_mcp_ics_sp1_np_cell_dot_sum = ff_q_dot_mcp_ics_sp1_np_cell_dot_sum_successor * S ((S (S ff_i_dot_mcp_ics_sp1_np_cell_dot_sum)) * ff_v_dot_mcp_ics_sp1_np_cell_dot_sum) + (ff_s_dot_mcp_ics_sp1_np_cell_dot_sum))) /\ ff_s_dot_mcp_ics_sp1_np_cell_dot_sum = ff_r_dot_mcp_ics_sp1_np_cell_dot_sum + ff_a_dot_mcp_ics_sp1_np_cell_dot_sum))))))))))) /\ (((exists fs_h_mcp_ics_sp1_np_entry. fs_h_mcp_ics_sp1_np_entry + S (ff_value_mcp_prefix_ics_sp1_np) = S ((S (ff_index_mcp_prefix_ics_sp1_np)) * ff_nps_mcp_smatrix_ics_sp1)) /\ exists fs_q_mcp_ics_sp1_np_entry. ff_np_mcp_smatrix_ics_sp1 = fs_q_mcp_ics_sp1_np_entry * S ((S (ff_index_mcp_prefix_ics_sp1_np)) * ff_nps_mcp_smatrix_ics_sp1) + (ff_value_mcp_prefix_ics_sp1_np))))))) /\ ((forall ff_index_mcp_add_ics_sp1_positive ff_left_mcp_add_ics_sp1_positive ff_right_mcp_add_ics_sp1_positive ff_target_mcp_add_ics_sp1_positive. (exists mcp_gap_ics_sp1_positive_bound. mcp_gap_ics_sp1_positive_bound + S (ff_index_mcp_add_ics_sp1_positive) = ((r) * (1))) -> (((exists fs_h_mcp_ics_sp1_positive_left. fs_h_mcp_ics_sp1_positive_left + S (ff_left_mcp_add_ics_sp1_positive) = S ((S (ff_index_mcp_add_ics_sp1_positive)) * ff_pps_mcp_smatrix_ics_sp1)) /\ exists fs_q_mcp_ics_sp1_positive_left. ff_pp_mcp_smatrix_ics_sp1 = fs_q_mcp_ics_sp1_positive_left * S ((S (ff_index_mcp_add_ics_sp1_positive)) * ff_pps_mcp_smatrix_ics_sp1) + (ff_left_mcp_add_ics_sp1_positive))) -> (((exists fs_h_mcp_ics_sp1_positive_right. fs_h_mcp_ics_sp1_positive_right + S (ff_right_mcp_add_ics_sp1_positive) = S ((S (ff_index_mcp_add_ics_sp1_positive)) * ff_nns_mcp_smatrix_ics_sp1)) /\ exists fs_q_mcp_ics_sp1_positive_right. ff_nn_mcp_smatrix_ics_sp1 = fs_q_mcp_ics_sp1_positive_right * S ((S (ff_index_mcp_add_ics_sp1_positive)) * ff_nns_mcp_smatrix_ics_sp1) + (ff_right_mcp_add_ics_sp1_positive))) -> (((exists fs_h_mcp_ics_sp1_positive_target. fs_h_mcp_ics_sp1_positive_target + S (ff_target_mcp_add_ics_sp1_positive) = S ((S (ff_index_mcp_add_ics_sp1_positive)) * qc)) /\ exists fs_q_mcp_ics_sp1_positive_target. qb = fs_q_mcp_ics_sp1_positive_target * S ((S (ff_index_mcp_add_ics_sp1_positive)) * qc) + (ff_target_mcp_add_ics_sp1_positive))) -> ff_target_mcp_add_ics_sp1_positive = ff_left_mcp_add_ics_sp1_positive + ff_right_mcp_add_ics_sp1_positive) /\ (forall ff_index_mcp_add_ics_sp1_negative ff_left_mcp_add_ics_sp1_negative ff_right_mcp_add_ics_sp1_negative ff_target_mcp_add_ics_sp1_negative. (exists mcp_gap_ics_sp1_negative_bound. mcp_gap_ics_sp1_negative_bound + S (ff_index_mcp_add_ics_sp1_negative) = ((r) * (1))) -> (((exists fs_h_mcp_ics_sp1_negative_left. fs_h_mcp_ics_sp1_negative_left + S (ff_left_mcp_add_ics_sp1_negative) = S ((S (ff_index_mcp_add_ics_sp1_negative)) * ff_pns_mcp_smatrix_ics_sp1)) /\ exists fs_q_mcp_ics_sp1_negative_left. ff_pn_mcp_smatrix_ics_sp1 = fs_q_mcp_ics_sp1_negative_left * S ((S (ff_index_mcp_add_ics_sp1_negative)) * ff_pns_mcp_smatrix_ics_sp1) + (ff_left_mcp_add_ics_sp1_negative))) -> (((exists fs_h_mcp_ics_sp1_negative_right. fs_h_mcp_ics_sp1_negative_right + S (ff_right_mcp_add_ics_sp1_negative) = S ((S (ff_index_mcp_add_ics_sp1_negative)) * ff_nps_mcp_smatrix_ics_sp1)) /\ exists fs_q_mcp_ics_sp1_negative_right. ff_np_mcp_smatrix_ics_sp1 = fs_q_mcp_ics_sp1_negative_right * S ((S (ff_index_mcp_add_ics_sp1_negative)) * ff_nps_mcp_smatrix_ics_sp1) + (ff_right_mcp_add_ics_sp1_negative))) -> (((exists fs_h_mcp_ics_sp1_negative_target. fs_h_mcp_ics_sp1_negative_target + S (ff_target_mcp_add_ics_sp1_negative) = S ((S (ff_index_mcp_add_ics_sp1_negative)) * mc)) /\ exists fs_q_mcp_ics_sp1_negative_target. mb = fs_q_mcp_ics_sp1_negative_target * S ((S (ff_index_mcp_add_ics_sp1_negative)) * mc) + (ff_target_mcp_add_ics_sp1_negative))) -> ff_target_mcp_add_ics_sp1_negative = ff_left_mcp_add_ics_sp1_negative + ff_right_mcp_add_ics_sp1_negative))))))) -> (exists ff_pp_mcp_smatrix_ics_sp2 ff_pps_mcp_smatrix_ics_sp2 ff_nn_mcp_smatrix_ics_sp2 ff_nns_mcp_smatrix_ics_sp2 ff_pn_mcp_smatrix_ics_sp2 ff_pns_mcp_smatrix_ics_sp2 ff_np_mcp_smatrix_ics_sp2 ff_nps_mcp_smatrix_ics_sp2. ((forall ff_index_mcp_prefix_ics_sp2_pp. (exists mcp_gap_ics_sp2_pp_index. mcp_gap_ics_sp2_pp_index + S (ff_index_mcp_prefix_ics_sp2_pp) = ((r) * (1))) -> exists ff_row_mcp_prefix_ics_sp2_pp ff_column_mcp_prefix_ics_sp2_pp ff_value_mcp_prefix_ics_sp2_pp. ((ff_index_mcp_prefix_ics_sp2_pp) = (1) * ff_row_mcp_prefix_ics_sp2_pp + ff_column_mcp_prefix_ics_sp2_pp /\ ((exists mcp_gap_ics_sp2_pp_column. mcp_gap_ics_sp2_pp_column + S (ff_column_mcp_prefix_ics_sp2_pp) = (1)) /\ ((exists ff_left_mcp_cell_ics_sp2_pp_cell ff_left_scale_mcp_cell_ics_sp2_pp_cell ff_right_mcp_cell_ics_sp2_pp_cell ff_right_scale_mcp_cell_ics_sp2_pp_cell. ((forall ff_index_mcp_ics_sp2_pp_cell_row ff_source_mcp_ics_sp2_pp_cell_row ff_target_mcp_ics_sp2_pp_cell_row. (exists mcp_gap_ics_sp2_pp_cell_row_bound. mcp_gap_ics_sp2_pp_cell_row_bound + S (ff_index_mcp_ics_sp2_pp_cell_row) = (w)) -> (((exists fs_h_mcp_ics_sp2_pp_cell_row_source. fs_h_mcp_ics_sp2_pp_cell_row_source + S (ff_source_mcp_ics_sp2_pp_cell_row) = S ((S (((ff_row_mcp_prefix_ics_sp2_pp) * (w)) + (1) * ff_index_mcp_ics_sp2_pp_cell_row)) * ac)) /\ exists fs_q_mcp_ics_sp2_pp_cell_row_source. ab = fs_q_mcp_ics_sp2_pp_cell_row_source * S ((S (((ff_row_mcp_prefix_ics_sp2_pp) * (w)) + (1) * ff_index_mcp_ics_sp2_pp_cell_row)) * ac) + (ff_source_mcp_ics_sp2_pp_cell_row))) -> (((exists fs_h_mcp_ics_sp2_pp_cell_row_target. fs_h_mcp_ics_sp2_pp_cell_row_target + S (ff_target_mcp_ics_sp2_pp_cell_row) = S ((S (ff_index_mcp_ics_sp2_pp_cell_row)) * ff_left_scale_mcp_cell_ics_sp2_pp_cell)) /\ exists fs_q_mcp_ics_sp2_pp_cell_row_target. ff_left_mcp_cell_ics_sp2_pp_cell = fs_q_mcp_ics_sp2_pp_cell_row_target * S ((S (ff_index_mcp_ics_sp2_pp_cell_row)) * ff_left_scale_mcp_cell_ics_sp2_pp_cell) + (ff_target_mcp_ics_sp2_pp_cell_row))) -> ff_target_mcp_ics_sp2_pp_cell_row = ff_source_mcp_ics_sp2_pp_cell_row) /\ ((forall ff_index_mcp_ics_sp2_pp_cell_column ff_source_mcp_ics_sp2_pp_cell_column ff_target_mcp_ics_sp2_pp_cell_column. (exists mcp_gap_ics_sp2_pp_cell_column_bound. mcp_gap_ics_sp2_pp_cell_column_bound + S (ff_index_mcp_ics_sp2_pp_cell_column) = (w)) -> (((exists fs_h_mcp_ics_sp2_pp_cell_column_source. fs_h_mcp_ics_sp2_pp_cell_column_source + S (ff_source_mcp_ics_sp2_pp_cell_column) = S ((S ((ff_column_mcp_prefix_ics_sp2_pp) + (1) * ff_index_mcp_ics_sp2_pp_cell_column)) * ic)) /\ exists fs_q_mcp_ics_sp2_pp_cell_column_source. ib = fs_q_mcp_ics_sp2_pp_cell_column_source * S ((S ((ff_column_mcp_prefix_ics_sp2_pp) + (1) * ff_index_mcp_ics_sp2_pp_cell_column)) * ic) + (ff_source_mcp_ics_sp2_pp_cell_column))) -> (((exists fs_h_mcp_ics_sp2_pp_cell_column_target. fs_h_mcp_ics_sp2_pp_cell_column_target + S (ff_target_mcp_ics_sp2_pp_cell_column) = S ((S (ff_index_mcp_ics_sp2_pp_cell_column)) * ff_right_scale_mcp_cell_ics_sp2_pp_cell)) /\ exists fs_q_mcp_ics_sp2_pp_cell_column_target. ff_right_mcp_cell_ics_sp2_pp_cell = fs_q_mcp_ics_sp2_pp_cell_column_target * S ((S (ff_index_mcp_ics_sp2_pp_cell_column)) * ff_right_scale_mcp_cell_ics_sp2_pp_cell) + (ff_target_mcp_ics_sp2_pp_cell_column))) -> ff_target_mcp_ics_sp2_pp_cell_column = ff_source_mcp_ics_sp2_pp_cell_column) /\ (exists ff_code_dot_mcp_ics_sp2_pp_cell_dot ff_scale_dot_mcp_ics_sp2_pp_cell_dot. ((forall fpmp_index_dot_mcp_ics_sp2_pp_cell_dot_pointwise fpmp_left_dot_mcp_ics_sp2_pp_cell_dot_pointwise fpmp_right_dot_mcp_ics_sp2_pp_cell_dot_pointwise fpmp_target_dot_mcp_ics_sp2_pp_cell_dot_pointwise. (exists fpmp_gap_dot_mcp_ics_sp2_pp_cell_dot_pointwise. fpmp_gap_dot_mcp_ics_sp2_pp_cell_dot_pointwise + S fpmp_index_dot_mcp_ics_sp2_pp_cell_dot_pointwise = w) -> (((exists ff_h_fpmp_dot_mcp_ics_sp2_pp_cell_dot_pointwise_left. ff_h_fpmp_dot_mcp_ics_sp2_pp_cell_dot_pointwise_left + S (fpmp_left_dot_mcp_ics_sp2_pp_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_sp2_pp_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_sp2_pp_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_sp2_pp_cell_dot_pointwise_left. ff_left_mcp_cell_ics_sp2_pp_cell = ff_q_fpmp_dot_mcp_ics_sp2_pp_cell_dot_pointwise_left * S ((S (fpmp_index_dot_mcp_ics_sp2_pp_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_sp2_pp_cell) + (fpmp_left_dot_mcp_ics_sp2_pp_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_sp2_pp_cell_dot_pointwise_right. ff_h_fpmp_dot_mcp_ics_sp2_pp_cell_dot_pointwise_right + S (fpmp_right_dot_mcp_ics_sp2_pp_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_sp2_pp_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_sp2_pp_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_sp2_pp_cell_dot_pointwise_right. ff_right_mcp_cell_ics_sp2_pp_cell = ff_q_fpmp_dot_mcp_ics_sp2_pp_cell_dot_pointwise_right * S ((S (fpmp_index_dot_mcp_ics_sp2_pp_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_sp2_pp_cell) + (fpmp_right_dot_mcp_ics_sp2_pp_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_sp2_pp_cell_dot_pointwise_target. ff_h_fpmp_dot_mcp_ics_sp2_pp_cell_dot_pointwise_target + S (fpmp_target_dot_mcp_ics_sp2_pp_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_sp2_pp_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_sp2_pp_cell_dot)) /\ exists ff_q_fpmp_dot_mcp_ics_sp2_pp_cell_dot_pointwise_target. ff_code_dot_mcp_ics_sp2_pp_cell_dot = ff_q_fpmp_dot_mcp_ics_sp2_pp_cell_dot_pointwise_target * S ((S (fpmp_index_dot_mcp_ics_sp2_pp_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_sp2_pp_cell_dot) + (fpmp_target_dot_mcp_ics_sp2_pp_cell_dot_pointwise))) -> fpmp_target_dot_mcp_ics_sp2_pp_cell_dot_pointwise = fpmp_left_dot_mcp_ics_sp2_pp_cell_dot_pointwise * fpmp_right_dot_mcp_ics_sp2_pp_cell_dot_pointwise) /\ (exists ff_u_dot_mcp_ics_sp2_pp_cell_dot_sum ff_v_dot_mcp_ics_sp2_pp_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_sp2_pp_cell_dot_sum_start. ff_h_dot_mcp_ics_sp2_pp_cell_dot_sum_start + S (0) = S ((S (0)) * ff_v_dot_mcp_ics_sp2_pp_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_sp2_pp_cell_dot_sum_start. ff_u_dot_mcp_ics_sp2_pp_cell_dot_sum = ff_q_dot_mcp_ics_sp2_pp_cell_dot_sum_start * S ((S (0)) * ff_v_dot_mcp_ics_sp2_pp_cell_dot_sum) + (0))) /\ ((((exists ff_h_dot_mcp_ics_sp2_pp_cell_dot_sum_terminal. ff_h_dot_mcp_ics_sp2_pp_cell_dot_sum_terminal + S (ff_value_mcp_prefix_ics_sp2_pp) = S ((S (w)) * ff_v_dot_mcp_ics_sp2_pp_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_sp2_pp_cell_dot_sum_terminal. ff_u_dot_mcp_ics_sp2_pp_cell_dot_sum = ff_q_dot_mcp_ics_sp2_pp_cell_dot_sum_terminal * S ((S (w)) * ff_v_dot_mcp_ics_sp2_pp_cell_dot_sum) + (ff_value_mcp_prefix_ics_sp2_pp))) /\ forall ff_i_dot_mcp_ics_sp2_pp_cell_dot_sum. (exists ff_lt_dot_mcp_ics_sp2_pp_cell_dot_sum_bound. ff_lt_dot_mcp_ics_sp2_pp_cell_dot_sum_bound + S ff_i_dot_mcp_ics_sp2_pp_cell_dot_sum = w) -> exists ff_a_dot_mcp_ics_sp2_pp_cell_dot_sum ff_r_dot_mcp_ics_sp2_pp_cell_dot_sum ff_s_dot_mcp_ics_sp2_pp_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_sp2_pp_cell_dot_sum_summand. ff_h_dot_mcp_ics_sp2_pp_cell_dot_sum_summand + S (ff_a_dot_mcp_ics_sp2_pp_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_sp2_pp_cell_dot_sum)) * ff_scale_dot_mcp_ics_sp2_pp_cell_dot)) /\ exists ff_q_dot_mcp_ics_sp2_pp_cell_dot_sum_summand. ff_code_dot_mcp_ics_sp2_pp_cell_dot = ff_q_dot_mcp_ics_sp2_pp_cell_dot_sum_summand * S ((S (ff_i_dot_mcp_ics_sp2_pp_cell_dot_sum)) * ff_scale_dot_mcp_ics_sp2_pp_cell_dot) + (ff_a_dot_mcp_ics_sp2_pp_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_sp2_pp_cell_dot_sum_partial. ff_h_dot_mcp_ics_sp2_pp_cell_dot_sum_partial + S (ff_r_dot_mcp_ics_sp2_pp_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_sp2_pp_cell_dot_sum)) * ff_v_dot_mcp_ics_sp2_pp_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_sp2_pp_cell_dot_sum_partial. ff_u_dot_mcp_ics_sp2_pp_cell_dot_sum = ff_q_dot_mcp_ics_sp2_pp_cell_dot_sum_partial * S ((S (ff_i_dot_mcp_ics_sp2_pp_cell_dot_sum)) * ff_v_dot_mcp_ics_sp2_pp_cell_dot_sum) + (ff_r_dot_mcp_ics_sp2_pp_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_sp2_pp_cell_dot_sum_successor. ff_h_dot_mcp_ics_sp2_pp_cell_dot_sum_successor + S (ff_s_dot_mcp_ics_sp2_pp_cell_dot_sum) = S ((S (S ff_i_dot_mcp_ics_sp2_pp_cell_dot_sum)) * ff_v_dot_mcp_ics_sp2_pp_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_sp2_pp_cell_dot_sum_successor. ff_u_dot_mcp_ics_sp2_pp_cell_dot_sum = ff_q_dot_mcp_ics_sp2_pp_cell_dot_sum_successor * S ((S (S ff_i_dot_mcp_ics_sp2_pp_cell_dot_sum)) * ff_v_dot_mcp_ics_sp2_pp_cell_dot_sum) + (ff_s_dot_mcp_ics_sp2_pp_cell_dot_sum))) /\ ff_s_dot_mcp_ics_sp2_pp_cell_dot_sum = ff_r_dot_mcp_ics_sp2_pp_cell_dot_sum + ff_a_dot_mcp_ics_sp2_pp_cell_dot_sum))))))))))) /\ (((exists fs_h_mcp_ics_sp2_pp_entry. fs_h_mcp_ics_sp2_pp_entry + S (ff_value_mcp_prefix_ics_sp2_pp) = S ((S (ff_index_mcp_prefix_ics_sp2_pp)) * ff_pps_mcp_smatrix_ics_sp2)) /\ exists fs_q_mcp_ics_sp2_pp_entry. ff_pp_mcp_smatrix_ics_sp2 = fs_q_mcp_ics_sp2_pp_entry * S ((S (ff_index_mcp_prefix_ics_sp2_pp)) * ff_pps_mcp_smatrix_ics_sp2) + (ff_value_mcp_prefix_ics_sp2_pp))))))) /\ ((forall ff_index_mcp_prefix_ics_sp2_nn. (exists mcp_gap_ics_sp2_nn_index. mcp_gap_ics_sp2_nn_index + S (ff_index_mcp_prefix_ics_sp2_nn) = ((r) * (1))) -> exists ff_row_mcp_prefix_ics_sp2_nn ff_column_mcp_prefix_ics_sp2_nn ff_value_mcp_prefix_ics_sp2_nn. ((ff_index_mcp_prefix_ics_sp2_nn) = (1) * ff_row_mcp_prefix_ics_sp2_nn + ff_column_mcp_prefix_ics_sp2_nn /\ ((exists mcp_gap_ics_sp2_nn_column. mcp_gap_ics_sp2_nn_column + S (ff_column_mcp_prefix_ics_sp2_nn) = (1)) /\ ((exists ff_left_mcp_cell_ics_sp2_nn_cell ff_left_scale_mcp_cell_ics_sp2_nn_cell ff_right_mcp_cell_ics_sp2_nn_cell ff_right_scale_mcp_cell_ics_sp2_nn_cell. ((forall ff_index_mcp_ics_sp2_nn_cell_row ff_source_mcp_ics_sp2_nn_cell_row ff_target_mcp_ics_sp2_nn_cell_row. (exists mcp_gap_ics_sp2_nn_cell_row_bound. mcp_gap_ics_sp2_nn_cell_row_bound + S (ff_index_mcp_ics_sp2_nn_cell_row) = (w)) -> (((exists fs_h_mcp_ics_sp2_nn_cell_row_source. fs_h_mcp_ics_sp2_nn_cell_row_source + S (ff_source_mcp_ics_sp2_nn_cell_row) = S ((S (((ff_row_mcp_prefix_ics_sp2_nn) * (w)) + (1) * ff_index_mcp_ics_sp2_nn_cell_row)) * dc)) /\ exists fs_q_mcp_ics_sp2_nn_cell_row_source. db = fs_q_mcp_ics_sp2_nn_cell_row_source * S ((S (((ff_row_mcp_prefix_ics_sp2_nn) * (w)) + (1) * ff_index_mcp_ics_sp2_nn_cell_row)) * dc) + (ff_source_mcp_ics_sp2_nn_cell_row))) -> (((exists fs_h_mcp_ics_sp2_nn_cell_row_target. fs_h_mcp_ics_sp2_nn_cell_row_target + S (ff_target_mcp_ics_sp2_nn_cell_row) = S ((S (ff_index_mcp_ics_sp2_nn_cell_row)) * ff_left_scale_mcp_cell_ics_sp2_nn_cell)) /\ exists fs_q_mcp_ics_sp2_nn_cell_row_target. ff_left_mcp_cell_ics_sp2_nn_cell = fs_q_mcp_ics_sp2_nn_cell_row_target * S ((S (ff_index_mcp_ics_sp2_nn_cell_row)) * ff_left_scale_mcp_cell_ics_sp2_nn_cell) + (ff_target_mcp_ics_sp2_nn_cell_row))) -> ff_target_mcp_ics_sp2_nn_cell_row = ff_source_mcp_ics_sp2_nn_cell_row) /\ ((forall ff_index_mcp_ics_sp2_nn_cell_column ff_source_mcp_ics_sp2_nn_cell_column ff_target_mcp_ics_sp2_nn_cell_column. (exists mcp_gap_ics_sp2_nn_cell_column_bound. mcp_gap_ics_sp2_nn_cell_column_bound + S (ff_index_mcp_ics_sp2_nn_cell_column) = (w)) -> (((exists fs_h_mcp_ics_sp2_nn_cell_column_source. fs_h_mcp_ics_sp2_nn_cell_column_source + S (ff_source_mcp_ics_sp2_nn_cell_column) = S ((S ((ff_column_mcp_prefix_ics_sp2_nn) + (1) * ff_index_mcp_ics_sp2_nn_cell_column)) * jc)) /\ exists fs_q_mcp_ics_sp2_nn_cell_column_source. jb = fs_q_mcp_ics_sp2_nn_cell_column_source * S ((S ((ff_column_mcp_prefix_ics_sp2_nn) + (1) * ff_index_mcp_ics_sp2_nn_cell_column)) * jc) + (ff_source_mcp_ics_sp2_nn_cell_column))) -> (((exists fs_h_mcp_ics_sp2_nn_cell_column_target. fs_h_mcp_ics_sp2_nn_cell_column_target + S (ff_target_mcp_ics_sp2_nn_cell_column) = S ((S (ff_index_mcp_ics_sp2_nn_cell_column)) * ff_right_scale_mcp_cell_ics_sp2_nn_cell)) /\ exists fs_q_mcp_ics_sp2_nn_cell_column_target. ff_right_mcp_cell_ics_sp2_nn_cell = fs_q_mcp_ics_sp2_nn_cell_column_target * S ((S (ff_index_mcp_ics_sp2_nn_cell_column)) * ff_right_scale_mcp_cell_ics_sp2_nn_cell) + (ff_target_mcp_ics_sp2_nn_cell_column))) -> ff_target_mcp_ics_sp2_nn_cell_column = ff_source_mcp_ics_sp2_nn_cell_column) /\ (exists ff_code_dot_mcp_ics_sp2_nn_cell_dot ff_scale_dot_mcp_ics_sp2_nn_cell_dot. ((forall fpmp_index_dot_mcp_ics_sp2_nn_cell_dot_pointwise fpmp_left_dot_mcp_ics_sp2_nn_cell_dot_pointwise fpmp_right_dot_mcp_ics_sp2_nn_cell_dot_pointwise fpmp_target_dot_mcp_ics_sp2_nn_cell_dot_pointwise. (exists fpmp_gap_dot_mcp_ics_sp2_nn_cell_dot_pointwise. fpmp_gap_dot_mcp_ics_sp2_nn_cell_dot_pointwise + S fpmp_index_dot_mcp_ics_sp2_nn_cell_dot_pointwise = w) -> (((exists ff_h_fpmp_dot_mcp_ics_sp2_nn_cell_dot_pointwise_left. ff_h_fpmp_dot_mcp_ics_sp2_nn_cell_dot_pointwise_left + S (fpmp_left_dot_mcp_ics_sp2_nn_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_sp2_nn_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_sp2_nn_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_sp2_nn_cell_dot_pointwise_left. ff_left_mcp_cell_ics_sp2_nn_cell = ff_q_fpmp_dot_mcp_ics_sp2_nn_cell_dot_pointwise_left * S ((S (fpmp_index_dot_mcp_ics_sp2_nn_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_sp2_nn_cell) + (fpmp_left_dot_mcp_ics_sp2_nn_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_sp2_nn_cell_dot_pointwise_right. ff_h_fpmp_dot_mcp_ics_sp2_nn_cell_dot_pointwise_right + S (fpmp_right_dot_mcp_ics_sp2_nn_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_sp2_nn_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_sp2_nn_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_sp2_nn_cell_dot_pointwise_right. ff_right_mcp_cell_ics_sp2_nn_cell = ff_q_fpmp_dot_mcp_ics_sp2_nn_cell_dot_pointwise_right * S ((S (fpmp_index_dot_mcp_ics_sp2_nn_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_sp2_nn_cell) + (fpmp_right_dot_mcp_ics_sp2_nn_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_sp2_nn_cell_dot_pointwise_target. ff_h_fpmp_dot_mcp_ics_sp2_nn_cell_dot_pointwise_target + S (fpmp_target_dot_mcp_ics_sp2_nn_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_sp2_nn_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_sp2_nn_cell_dot)) /\ exists ff_q_fpmp_dot_mcp_ics_sp2_nn_cell_dot_pointwise_target. ff_code_dot_mcp_ics_sp2_nn_cell_dot = ff_q_fpmp_dot_mcp_ics_sp2_nn_cell_dot_pointwise_target * S ((S (fpmp_index_dot_mcp_ics_sp2_nn_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_sp2_nn_cell_dot) + (fpmp_target_dot_mcp_ics_sp2_nn_cell_dot_pointwise))) -> fpmp_target_dot_mcp_ics_sp2_nn_cell_dot_pointwise = fpmp_left_dot_mcp_ics_sp2_nn_cell_dot_pointwise * fpmp_right_dot_mcp_ics_sp2_nn_cell_dot_pointwise) /\ (exists ff_u_dot_mcp_ics_sp2_nn_cell_dot_sum ff_v_dot_mcp_ics_sp2_nn_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_sp2_nn_cell_dot_sum_start. ff_h_dot_mcp_ics_sp2_nn_cell_dot_sum_start + S (0) = S ((S (0)) * ff_v_dot_mcp_ics_sp2_nn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_sp2_nn_cell_dot_sum_start. ff_u_dot_mcp_ics_sp2_nn_cell_dot_sum = ff_q_dot_mcp_ics_sp2_nn_cell_dot_sum_start * S ((S (0)) * ff_v_dot_mcp_ics_sp2_nn_cell_dot_sum) + (0))) /\ ((((exists ff_h_dot_mcp_ics_sp2_nn_cell_dot_sum_terminal. ff_h_dot_mcp_ics_sp2_nn_cell_dot_sum_terminal + S (ff_value_mcp_prefix_ics_sp2_nn) = S ((S (w)) * ff_v_dot_mcp_ics_sp2_nn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_sp2_nn_cell_dot_sum_terminal. ff_u_dot_mcp_ics_sp2_nn_cell_dot_sum = ff_q_dot_mcp_ics_sp2_nn_cell_dot_sum_terminal * S ((S (w)) * ff_v_dot_mcp_ics_sp2_nn_cell_dot_sum) + (ff_value_mcp_prefix_ics_sp2_nn))) /\ forall ff_i_dot_mcp_ics_sp2_nn_cell_dot_sum. (exists ff_lt_dot_mcp_ics_sp2_nn_cell_dot_sum_bound. ff_lt_dot_mcp_ics_sp2_nn_cell_dot_sum_bound + S ff_i_dot_mcp_ics_sp2_nn_cell_dot_sum = w) -> exists ff_a_dot_mcp_ics_sp2_nn_cell_dot_sum ff_r_dot_mcp_ics_sp2_nn_cell_dot_sum ff_s_dot_mcp_ics_sp2_nn_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_sp2_nn_cell_dot_sum_summand. ff_h_dot_mcp_ics_sp2_nn_cell_dot_sum_summand + S (ff_a_dot_mcp_ics_sp2_nn_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_sp2_nn_cell_dot_sum)) * ff_scale_dot_mcp_ics_sp2_nn_cell_dot)) /\ exists ff_q_dot_mcp_ics_sp2_nn_cell_dot_sum_summand. ff_code_dot_mcp_ics_sp2_nn_cell_dot = ff_q_dot_mcp_ics_sp2_nn_cell_dot_sum_summand * S ((S (ff_i_dot_mcp_ics_sp2_nn_cell_dot_sum)) * ff_scale_dot_mcp_ics_sp2_nn_cell_dot) + (ff_a_dot_mcp_ics_sp2_nn_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_sp2_nn_cell_dot_sum_partial. ff_h_dot_mcp_ics_sp2_nn_cell_dot_sum_partial + S (ff_r_dot_mcp_ics_sp2_nn_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_sp2_nn_cell_dot_sum)) * ff_v_dot_mcp_ics_sp2_nn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_sp2_nn_cell_dot_sum_partial. ff_u_dot_mcp_ics_sp2_nn_cell_dot_sum = ff_q_dot_mcp_ics_sp2_nn_cell_dot_sum_partial * S ((S (ff_i_dot_mcp_ics_sp2_nn_cell_dot_sum)) * ff_v_dot_mcp_ics_sp2_nn_cell_dot_sum) + (ff_r_dot_mcp_ics_sp2_nn_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_sp2_nn_cell_dot_sum_successor. ff_h_dot_mcp_ics_sp2_nn_cell_dot_sum_successor + S (ff_s_dot_mcp_ics_sp2_nn_cell_dot_sum) = S ((S (S ff_i_dot_mcp_ics_sp2_nn_cell_dot_sum)) * ff_v_dot_mcp_ics_sp2_nn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_sp2_nn_cell_dot_sum_successor. ff_u_dot_mcp_ics_sp2_nn_cell_dot_sum = ff_q_dot_mcp_ics_sp2_nn_cell_dot_sum_successor * S ((S (S ff_i_dot_mcp_ics_sp2_nn_cell_dot_sum)) * ff_v_dot_mcp_ics_sp2_nn_cell_dot_sum) + (ff_s_dot_mcp_ics_sp2_nn_cell_dot_sum))) /\ ff_s_dot_mcp_ics_sp2_nn_cell_dot_sum = ff_r_dot_mcp_ics_sp2_nn_cell_dot_sum + ff_a_dot_mcp_ics_sp2_nn_cell_dot_sum))))))))))) /\ (((exists fs_h_mcp_ics_sp2_nn_entry. fs_h_mcp_ics_sp2_nn_entry + S (ff_value_mcp_prefix_ics_sp2_nn) = S ((S (ff_index_mcp_prefix_ics_sp2_nn)) * ff_nns_mcp_smatrix_ics_sp2)) /\ exists fs_q_mcp_ics_sp2_nn_entry. ff_nn_mcp_smatrix_ics_sp2 = fs_q_mcp_ics_sp2_nn_entry * S ((S (ff_index_mcp_prefix_ics_sp2_nn)) * ff_nns_mcp_smatrix_ics_sp2) + (ff_value_mcp_prefix_ics_sp2_nn))))))) /\ ((forall ff_index_mcp_prefix_ics_sp2_pn. (exists mcp_gap_ics_sp2_pn_index. mcp_gap_ics_sp2_pn_index + S (ff_index_mcp_prefix_ics_sp2_pn) = ((r) * (1))) -> exists ff_row_mcp_prefix_ics_sp2_pn ff_column_mcp_prefix_ics_sp2_pn ff_value_mcp_prefix_ics_sp2_pn. ((ff_index_mcp_prefix_ics_sp2_pn) = (1) * ff_row_mcp_prefix_ics_sp2_pn + ff_column_mcp_prefix_ics_sp2_pn /\ ((exists mcp_gap_ics_sp2_pn_column. mcp_gap_ics_sp2_pn_column + S (ff_column_mcp_prefix_ics_sp2_pn) = (1)) /\ ((exists ff_left_mcp_cell_ics_sp2_pn_cell ff_left_scale_mcp_cell_ics_sp2_pn_cell ff_right_mcp_cell_ics_sp2_pn_cell ff_right_scale_mcp_cell_ics_sp2_pn_cell. ((forall ff_index_mcp_ics_sp2_pn_cell_row ff_source_mcp_ics_sp2_pn_cell_row ff_target_mcp_ics_sp2_pn_cell_row. (exists mcp_gap_ics_sp2_pn_cell_row_bound. mcp_gap_ics_sp2_pn_cell_row_bound + S (ff_index_mcp_ics_sp2_pn_cell_row) = (w)) -> (((exists fs_h_mcp_ics_sp2_pn_cell_row_source. fs_h_mcp_ics_sp2_pn_cell_row_source + S (ff_source_mcp_ics_sp2_pn_cell_row) = S ((S (((ff_row_mcp_prefix_ics_sp2_pn) * (w)) + (1) * ff_index_mcp_ics_sp2_pn_cell_row)) * ac)) /\ exists fs_q_mcp_ics_sp2_pn_cell_row_source. ab = fs_q_mcp_ics_sp2_pn_cell_row_source * S ((S (((ff_row_mcp_prefix_ics_sp2_pn) * (w)) + (1) * ff_index_mcp_ics_sp2_pn_cell_row)) * ac) + (ff_source_mcp_ics_sp2_pn_cell_row))) -> (((exists fs_h_mcp_ics_sp2_pn_cell_row_target. fs_h_mcp_ics_sp2_pn_cell_row_target + S (ff_target_mcp_ics_sp2_pn_cell_row) = S ((S (ff_index_mcp_ics_sp2_pn_cell_row)) * ff_left_scale_mcp_cell_ics_sp2_pn_cell)) /\ exists fs_q_mcp_ics_sp2_pn_cell_row_target. ff_left_mcp_cell_ics_sp2_pn_cell = fs_q_mcp_ics_sp2_pn_cell_row_target * S ((S (ff_index_mcp_ics_sp2_pn_cell_row)) * ff_left_scale_mcp_cell_ics_sp2_pn_cell) + (ff_target_mcp_ics_sp2_pn_cell_row))) -> ff_target_mcp_ics_sp2_pn_cell_row = ff_source_mcp_ics_sp2_pn_cell_row) /\ ((forall ff_index_mcp_ics_sp2_pn_cell_column ff_source_mcp_ics_sp2_pn_cell_column ff_target_mcp_ics_sp2_pn_cell_column. (exists mcp_gap_ics_sp2_pn_cell_column_bound. mcp_gap_ics_sp2_pn_cell_column_bound + S (ff_index_mcp_ics_sp2_pn_cell_column) = (w)) -> (((exists fs_h_mcp_ics_sp2_pn_cell_column_source. fs_h_mcp_ics_sp2_pn_cell_column_source + S (ff_source_mcp_ics_sp2_pn_cell_column) = S ((S ((ff_column_mcp_prefix_ics_sp2_pn) + (1) * ff_index_mcp_ics_sp2_pn_cell_column)) * jc)) /\ exists fs_q_mcp_ics_sp2_pn_cell_column_source. jb = fs_q_mcp_ics_sp2_pn_cell_column_source * S ((S ((ff_column_mcp_prefix_ics_sp2_pn) + (1) * ff_index_mcp_ics_sp2_pn_cell_column)) * jc) + (ff_source_mcp_ics_sp2_pn_cell_column))) -> (((exists fs_h_mcp_ics_sp2_pn_cell_column_target. fs_h_mcp_ics_sp2_pn_cell_column_target + S (ff_target_mcp_ics_sp2_pn_cell_column) = S ((S (ff_index_mcp_ics_sp2_pn_cell_column)) * ff_right_scale_mcp_cell_ics_sp2_pn_cell)) /\ exists fs_q_mcp_ics_sp2_pn_cell_column_target. ff_right_mcp_cell_ics_sp2_pn_cell = fs_q_mcp_ics_sp2_pn_cell_column_target * S ((S (ff_index_mcp_ics_sp2_pn_cell_column)) * ff_right_scale_mcp_cell_ics_sp2_pn_cell) + (ff_target_mcp_ics_sp2_pn_cell_column))) -> ff_target_mcp_ics_sp2_pn_cell_column = ff_source_mcp_ics_sp2_pn_cell_column) /\ (exists ff_code_dot_mcp_ics_sp2_pn_cell_dot ff_scale_dot_mcp_ics_sp2_pn_cell_dot. ((forall fpmp_index_dot_mcp_ics_sp2_pn_cell_dot_pointwise fpmp_left_dot_mcp_ics_sp2_pn_cell_dot_pointwise fpmp_right_dot_mcp_ics_sp2_pn_cell_dot_pointwise fpmp_target_dot_mcp_ics_sp2_pn_cell_dot_pointwise. (exists fpmp_gap_dot_mcp_ics_sp2_pn_cell_dot_pointwise. fpmp_gap_dot_mcp_ics_sp2_pn_cell_dot_pointwise + S fpmp_index_dot_mcp_ics_sp2_pn_cell_dot_pointwise = w) -> (((exists ff_h_fpmp_dot_mcp_ics_sp2_pn_cell_dot_pointwise_left. ff_h_fpmp_dot_mcp_ics_sp2_pn_cell_dot_pointwise_left + S (fpmp_left_dot_mcp_ics_sp2_pn_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_sp2_pn_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_sp2_pn_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_sp2_pn_cell_dot_pointwise_left. ff_left_mcp_cell_ics_sp2_pn_cell = ff_q_fpmp_dot_mcp_ics_sp2_pn_cell_dot_pointwise_left * S ((S (fpmp_index_dot_mcp_ics_sp2_pn_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_sp2_pn_cell) + (fpmp_left_dot_mcp_ics_sp2_pn_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_sp2_pn_cell_dot_pointwise_right. ff_h_fpmp_dot_mcp_ics_sp2_pn_cell_dot_pointwise_right + S (fpmp_right_dot_mcp_ics_sp2_pn_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_sp2_pn_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_sp2_pn_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_sp2_pn_cell_dot_pointwise_right. ff_right_mcp_cell_ics_sp2_pn_cell = ff_q_fpmp_dot_mcp_ics_sp2_pn_cell_dot_pointwise_right * S ((S (fpmp_index_dot_mcp_ics_sp2_pn_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_sp2_pn_cell) + (fpmp_right_dot_mcp_ics_sp2_pn_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_sp2_pn_cell_dot_pointwise_target. ff_h_fpmp_dot_mcp_ics_sp2_pn_cell_dot_pointwise_target + S (fpmp_target_dot_mcp_ics_sp2_pn_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_sp2_pn_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_sp2_pn_cell_dot)) /\ exists ff_q_fpmp_dot_mcp_ics_sp2_pn_cell_dot_pointwise_target. ff_code_dot_mcp_ics_sp2_pn_cell_dot = ff_q_fpmp_dot_mcp_ics_sp2_pn_cell_dot_pointwise_target * S ((S (fpmp_index_dot_mcp_ics_sp2_pn_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_sp2_pn_cell_dot) + (fpmp_target_dot_mcp_ics_sp2_pn_cell_dot_pointwise))) -> fpmp_target_dot_mcp_ics_sp2_pn_cell_dot_pointwise = fpmp_left_dot_mcp_ics_sp2_pn_cell_dot_pointwise * fpmp_right_dot_mcp_ics_sp2_pn_cell_dot_pointwise) /\ (exists ff_u_dot_mcp_ics_sp2_pn_cell_dot_sum ff_v_dot_mcp_ics_sp2_pn_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_sp2_pn_cell_dot_sum_start. ff_h_dot_mcp_ics_sp2_pn_cell_dot_sum_start + S (0) = S ((S (0)) * ff_v_dot_mcp_ics_sp2_pn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_sp2_pn_cell_dot_sum_start. ff_u_dot_mcp_ics_sp2_pn_cell_dot_sum = ff_q_dot_mcp_ics_sp2_pn_cell_dot_sum_start * S ((S (0)) * ff_v_dot_mcp_ics_sp2_pn_cell_dot_sum) + (0))) /\ ((((exists ff_h_dot_mcp_ics_sp2_pn_cell_dot_sum_terminal. ff_h_dot_mcp_ics_sp2_pn_cell_dot_sum_terminal + S (ff_value_mcp_prefix_ics_sp2_pn) = S ((S (w)) * ff_v_dot_mcp_ics_sp2_pn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_sp2_pn_cell_dot_sum_terminal. ff_u_dot_mcp_ics_sp2_pn_cell_dot_sum = ff_q_dot_mcp_ics_sp2_pn_cell_dot_sum_terminal * S ((S (w)) * ff_v_dot_mcp_ics_sp2_pn_cell_dot_sum) + (ff_value_mcp_prefix_ics_sp2_pn))) /\ forall ff_i_dot_mcp_ics_sp2_pn_cell_dot_sum. (exists ff_lt_dot_mcp_ics_sp2_pn_cell_dot_sum_bound. ff_lt_dot_mcp_ics_sp2_pn_cell_dot_sum_bound + S ff_i_dot_mcp_ics_sp2_pn_cell_dot_sum = w) -> exists ff_a_dot_mcp_ics_sp2_pn_cell_dot_sum ff_r_dot_mcp_ics_sp2_pn_cell_dot_sum ff_s_dot_mcp_ics_sp2_pn_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_sp2_pn_cell_dot_sum_summand. ff_h_dot_mcp_ics_sp2_pn_cell_dot_sum_summand + S (ff_a_dot_mcp_ics_sp2_pn_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_sp2_pn_cell_dot_sum)) * ff_scale_dot_mcp_ics_sp2_pn_cell_dot)) /\ exists ff_q_dot_mcp_ics_sp2_pn_cell_dot_sum_summand. ff_code_dot_mcp_ics_sp2_pn_cell_dot = ff_q_dot_mcp_ics_sp2_pn_cell_dot_sum_summand * S ((S (ff_i_dot_mcp_ics_sp2_pn_cell_dot_sum)) * ff_scale_dot_mcp_ics_sp2_pn_cell_dot) + (ff_a_dot_mcp_ics_sp2_pn_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_sp2_pn_cell_dot_sum_partial. ff_h_dot_mcp_ics_sp2_pn_cell_dot_sum_partial + S (ff_r_dot_mcp_ics_sp2_pn_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_sp2_pn_cell_dot_sum)) * ff_v_dot_mcp_ics_sp2_pn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_sp2_pn_cell_dot_sum_partial. ff_u_dot_mcp_ics_sp2_pn_cell_dot_sum = ff_q_dot_mcp_ics_sp2_pn_cell_dot_sum_partial * S ((S (ff_i_dot_mcp_ics_sp2_pn_cell_dot_sum)) * ff_v_dot_mcp_ics_sp2_pn_cell_dot_sum) + (ff_r_dot_mcp_ics_sp2_pn_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_sp2_pn_cell_dot_sum_successor. ff_h_dot_mcp_ics_sp2_pn_cell_dot_sum_successor + S (ff_s_dot_mcp_ics_sp2_pn_cell_dot_sum) = S ((S (S ff_i_dot_mcp_ics_sp2_pn_cell_dot_sum)) * ff_v_dot_mcp_ics_sp2_pn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_sp2_pn_cell_dot_sum_successor. ff_u_dot_mcp_ics_sp2_pn_cell_dot_sum = ff_q_dot_mcp_ics_sp2_pn_cell_dot_sum_successor * S ((S (S ff_i_dot_mcp_ics_sp2_pn_cell_dot_sum)) * ff_v_dot_mcp_ics_sp2_pn_cell_dot_sum) + (ff_s_dot_mcp_ics_sp2_pn_cell_dot_sum))) /\ ff_s_dot_mcp_ics_sp2_pn_cell_dot_sum = ff_r_dot_mcp_ics_sp2_pn_cell_dot_sum + ff_a_dot_mcp_ics_sp2_pn_cell_dot_sum))))))))))) /\ (((exists fs_h_mcp_ics_sp2_pn_entry. fs_h_mcp_ics_sp2_pn_entry + S (ff_value_mcp_prefix_ics_sp2_pn) = S ((S (ff_index_mcp_prefix_ics_sp2_pn)) * ff_pns_mcp_smatrix_ics_sp2)) /\ exists fs_q_mcp_ics_sp2_pn_entry. ff_pn_mcp_smatrix_ics_sp2 = fs_q_mcp_ics_sp2_pn_entry * S ((S (ff_index_mcp_prefix_ics_sp2_pn)) * ff_pns_mcp_smatrix_ics_sp2) + (ff_value_mcp_prefix_ics_sp2_pn))))))) /\ ((forall ff_index_mcp_prefix_ics_sp2_np. (exists mcp_gap_ics_sp2_np_index. mcp_gap_ics_sp2_np_index + S (ff_index_mcp_prefix_ics_sp2_np) = ((r) * (1))) -> exists ff_row_mcp_prefix_ics_sp2_np ff_column_mcp_prefix_ics_sp2_np ff_value_mcp_prefix_ics_sp2_np. ((ff_index_mcp_prefix_ics_sp2_np) = (1) * ff_row_mcp_prefix_ics_sp2_np + ff_column_mcp_prefix_ics_sp2_np /\ ((exists mcp_gap_ics_sp2_np_column. mcp_gap_ics_sp2_np_column + S (ff_column_mcp_prefix_ics_sp2_np) = (1)) /\ ((exists ff_left_mcp_cell_ics_sp2_np_cell ff_left_scale_mcp_cell_ics_sp2_np_cell ff_right_mcp_cell_ics_sp2_np_cell ff_right_scale_mcp_cell_ics_sp2_np_cell. ((forall ff_index_mcp_ics_sp2_np_cell_row ff_source_mcp_ics_sp2_np_cell_row ff_target_mcp_ics_sp2_np_cell_row. (exists mcp_gap_ics_sp2_np_cell_row_bound. mcp_gap_ics_sp2_np_cell_row_bound + S (ff_index_mcp_ics_sp2_np_cell_row) = (w)) -> (((exists fs_h_mcp_ics_sp2_np_cell_row_source. fs_h_mcp_ics_sp2_np_cell_row_source + S (ff_source_mcp_ics_sp2_np_cell_row) = S ((S (((ff_row_mcp_prefix_ics_sp2_np) * (w)) + (1) * ff_index_mcp_ics_sp2_np_cell_row)) * dc)) /\ exists fs_q_mcp_ics_sp2_np_cell_row_source. db = fs_q_mcp_ics_sp2_np_cell_row_source * S ((S (((ff_row_mcp_prefix_ics_sp2_np) * (w)) + (1) * ff_index_mcp_ics_sp2_np_cell_row)) * dc) + (ff_source_mcp_ics_sp2_np_cell_row))) -> (((exists fs_h_mcp_ics_sp2_np_cell_row_target. fs_h_mcp_ics_sp2_np_cell_row_target + S (ff_target_mcp_ics_sp2_np_cell_row) = S ((S (ff_index_mcp_ics_sp2_np_cell_row)) * ff_left_scale_mcp_cell_ics_sp2_np_cell)) /\ exists fs_q_mcp_ics_sp2_np_cell_row_target. ff_left_mcp_cell_ics_sp2_np_cell = fs_q_mcp_ics_sp2_np_cell_row_target * S ((S (ff_index_mcp_ics_sp2_np_cell_row)) * ff_left_scale_mcp_cell_ics_sp2_np_cell) + (ff_target_mcp_ics_sp2_np_cell_row))) -> ff_target_mcp_ics_sp2_np_cell_row = ff_source_mcp_ics_sp2_np_cell_row) /\ ((forall ff_index_mcp_ics_sp2_np_cell_column ff_source_mcp_ics_sp2_np_cell_column ff_target_mcp_ics_sp2_np_cell_column. (exists mcp_gap_ics_sp2_np_cell_column_bound. mcp_gap_ics_sp2_np_cell_column_bound + S (ff_index_mcp_ics_sp2_np_cell_column) = (w)) -> (((exists fs_h_mcp_ics_sp2_np_cell_column_source. fs_h_mcp_ics_sp2_np_cell_column_source + S (ff_source_mcp_ics_sp2_np_cell_column) = S ((S ((ff_column_mcp_prefix_ics_sp2_np) + (1) * ff_index_mcp_ics_sp2_np_cell_column)) * ic)) /\ exists fs_q_mcp_ics_sp2_np_cell_column_source. ib = fs_q_mcp_ics_sp2_np_cell_column_source * S ((S ((ff_column_mcp_prefix_ics_sp2_np) + (1) * ff_index_mcp_ics_sp2_np_cell_column)) * ic) + (ff_source_mcp_ics_sp2_np_cell_column))) -> (((exists fs_h_mcp_ics_sp2_np_cell_column_target. fs_h_mcp_ics_sp2_np_cell_column_target + S (ff_target_mcp_ics_sp2_np_cell_column) = S ((S (ff_index_mcp_ics_sp2_np_cell_column)) * ff_right_scale_mcp_cell_ics_sp2_np_cell)) /\ exists fs_q_mcp_ics_sp2_np_cell_column_target. ff_right_mcp_cell_ics_sp2_np_cell = fs_q_mcp_ics_sp2_np_cell_column_target * S ((S (ff_index_mcp_ics_sp2_np_cell_column)) * ff_right_scale_mcp_cell_ics_sp2_np_cell) + (ff_target_mcp_ics_sp2_np_cell_column))) -> ff_target_mcp_ics_sp2_np_cell_column = ff_source_mcp_ics_sp2_np_cell_column) /\ (exists ff_code_dot_mcp_ics_sp2_np_cell_dot ff_scale_dot_mcp_ics_sp2_np_cell_dot. ((forall fpmp_index_dot_mcp_ics_sp2_np_cell_dot_pointwise fpmp_left_dot_mcp_ics_sp2_np_cell_dot_pointwise fpmp_right_dot_mcp_ics_sp2_np_cell_dot_pointwise fpmp_target_dot_mcp_ics_sp2_np_cell_dot_pointwise. (exists fpmp_gap_dot_mcp_ics_sp2_np_cell_dot_pointwise. fpmp_gap_dot_mcp_ics_sp2_np_cell_dot_pointwise + S fpmp_index_dot_mcp_ics_sp2_np_cell_dot_pointwise = w) -> (((exists ff_h_fpmp_dot_mcp_ics_sp2_np_cell_dot_pointwise_left. ff_h_fpmp_dot_mcp_ics_sp2_np_cell_dot_pointwise_left + S (fpmp_left_dot_mcp_ics_sp2_np_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_sp2_np_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_sp2_np_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_sp2_np_cell_dot_pointwise_left. ff_left_mcp_cell_ics_sp2_np_cell = ff_q_fpmp_dot_mcp_ics_sp2_np_cell_dot_pointwise_left * S ((S (fpmp_index_dot_mcp_ics_sp2_np_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_sp2_np_cell) + (fpmp_left_dot_mcp_ics_sp2_np_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_sp2_np_cell_dot_pointwise_right. ff_h_fpmp_dot_mcp_ics_sp2_np_cell_dot_pointwise_right + S (fpmp_right_dot_mcp_ics_sp2_np_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_sp2_np_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_sp2_np_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_sp2_np_cell_dot_pointwise_right. ff_right_mcp_cell_ics_sp2_np_cell = ff_q_fpmp_dot_mcp_ics_sp2_np_cell_dot_pointwise_right * S ((S (fpmp_index_dot_mcp_ics_sp2_np_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_sp2_np_cell) + (fpmp_right_dot_mcp_ics_sp2_np_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_sp2_np_cell_dot_pointwise_target. ff_h_fpmp_dot_mcp_ics_sp2_np_cell_dot_pointwise_target + S (fpmp_target_dot_mcp_ics_sp2_np_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_sp2_np_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_sp2_np_cell_dot)) /\ exists ff_q_fpmp_dot_mcp_ics_sp2_np_cell_dot_pointwise_target. ff_code_dot_mcp_ics_sp2_np_cell_dot = ff_q_fpmp_dot_mcp_ics_sp2_np_cell_dot_pointwise_target * S ((S (fpmp_index_dot_mcp_ics_sp2_np_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_sp2_np_cell_dot) + (fpmp_target_dot_mcp_ics_sp2_np_cell_dot_pointwise))) -> fpmp_target_dot_mcp_ics_sp2_np_cell_dot_pointwise = fpmp_left_dot_mcp_ics_sp2_np_cell_dot_pointwise * fpmp_right_dot_mcp_ics_sp2_np_cell_dot_pointwise) /\ (exists ff_u_dot_mcp_ics_sp2_np_cell_dot_sum ff_v_dot_mcp_ics_sp2_np_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_sp2_np_cell_dot_sum_start. ff_h_dot_mcp_ics_sp2_np_cell_dot_sum_start + S (0) = S ((S (0)) * ff_v_dot_mcp_ics_sp2_np_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_sp2_np_cell_dot_sum_start. ff_u_dot_mcp_ics_sp2_np_cell_dot_sum = ff_q_dot_mcp_ics_sp2_np_cell_dot_sum_start * S ((S (0)) * ff_v_dot_mcp_ics_sp2_np_cell_dot_sum) + (0))) /\ ((((exists ff_h_dot_mcp_ics_sp2_np_cell_dot_sum_terminal. ff_h_dot_mcp_ics_sp2_np_cell_dot_sum_terminal + S (ff_value_mcp_prefix_ics_sp2_np) = S ((S (w)) * ff_v_dot_mcp_ics_sp2_np_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_sp2_np_cell_dot_sum_terminal. ff_u_dot_mcp_ics_sp2_np_cell_dot_sum = ff_q_dot_mcp_ics_sp2_np_cell_dot_sum_terminal * S ((S (w)) * ff_v_dot_mcp_ics_sp2_np_cell_dot_sum) + (ff_value_mcp_prefix_ics_sp2_np))) /\ forall ff_i_dot_mcp_ics_sp2_np_cell_dot_sum. (exists ff_lt_dot_mcp_ics_sp2_np_cell_dot_sum_bound. ff_lt_dot_mcp_ics_sp2_np_cell_dot_sum_bound + S ff_i_dot_mcp_ics_sp2_np_cell_dot_sum = w) -> exists ff_a_dot_mcp_ics_sp2_np_cell_dot_sum ff_r_dot_mcp_ics_sp2_np_cell_dot_sum ff_s_dot_mcp_ics_sp2_np_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_sp2_np_cell_dot_sum_summand. ff_h_dot_mcp_ics_sp2_np_cell_dot_sum_summand + S (ff_a_dot_mcp_ics_sp2_np_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_sp2_np_cell_dot_sum)) * ff_scale_dot_mcp_ics_sp2_np_cell_dot)) /\ exists ff_q_dot_mcp_ics_sp2_np_cell_dot_sum_summand. ff_code_dot_mcp_ics_sp2_np_cell_dot = ff_q_dot_mcp_ics_sp2_np_cell_dot_sum_summand * S ((S (ff_i_dot_mcp_ics_sp2_np_cell_dot_sum)) * ff_scale_dot_mcp_ics_sp2_np_cell_dot) + (ff_a_dot_mcp_ics_sp2_np_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_sp2_np_cell_dot_sum_partial. ff_h_dot_mcp_ics_sp2_np_cell_dot_sum_partial + S (ff_r_dot_mcp_ics_sp2_np_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_sp2_np_cell_dot_sum)) * ff_v_dot_mcp_ics_sp2_np_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_sp2_np_cell_dot_sum_partial. ff_u_dot_mcp_ics_sp2_np_cell_dot_sum = ff_q_dot_mcp_ics_sp2_np_cell_dot_sum_partial * S ((S (ff_i_dot_mcp_ics_sp2_np_cell_dot_sum)) * ff_v_dot_mcp_ics_sp2_np_cell_dot_sum) + (ff_r_dot_mcp_ics_sp2_np_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_sp2_np_cell_dot_sum_successor. ff_h_dot_mcp_ics_sp2_np_cell_dot_sum_successor + S (ff_s_dot_mcp_ics_sp2_np_cell_dot_sum) = S ((S (S ff_i_dot_mcp_ics_sp2_np_cell_dot_sum)) * ff_v_dot_mcp_ics_sp2_np_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_sp2_np_cell_dot_sum_successor. ff_u_dot_mcp_ics_sp2_np_cell_dot_sum = ff_q_dot_mcp_ics_sp2_np_cell_dot_sum_successor * S ((S (S ff_i_dot_mcp_ics_sp2_np_cell_dot_sum)) * ff_v_dot_mcp_ics_sp2_np_cell_dot_sum) + (ff_s_dot_mcp_ics_sp2_np_cell_dot_sum))) /\ ff_s_dot_mcp_ics_sp2_np_cell_dot_sum = ff_r_dot_mcp_ics_sp2_np_cell_dot_sum + ff_a_dot_mcp_ics_sp2_np_cell_dot_sum))))))))))) /\ (((exists fs_h_mcp_ics_sp2_np_entry. fs_h_mcp_ics_sp2_np_entry + S (ff_value_mcp_prefix_ics_sp2_np) = S ((S (ff_index_mcp_prefix_ics_sp2_np)) * ff_nps_mcp_smatrix_ics_sp2)) /\ exists fs_q_mcp_ics_sp2_np_entry. ff_np_mcp_smatrix_ics_sp2 = fs_q_mcp_ics_sp2_np_entry * S ((S (ff_index_mcp_prefix_ics_sp2_np)) * ff_nps_mcp_smatrix_ics_sp2) + (ff_value_mcp_prefix_ics_sp2_np))))))) /\ ((forall ff_index_mcp_add_ics_sp2_positive ff_left_mcp_add_ics_sp2_positive ff_right_mcp_add_ics_sp2_positive ff_target_mcp_add_ics_sp2_positive. (exists mcp_gap_ics_sp2_positive_bound. mcp_gap_ics_sp2_positive_bound + S (ff_index_mcp_add_ics_sp2_positive) = ((r) * (1))) -> (((exists fs_h_mcp_ics_sp2_positive_left. fs_h_mcp_ics_sp2_positive_left + S (ff_left_mcp_add_ics_sp2_positive) = S ((S (ff_index_mcp_add_ics_sp2_positive)) * ff_pps_mcp_smatrix_ics_sp2)) /\ exists fs_q_mcp_ics_sp2_positive_left. ff_pp_mcp_smatrix_ics_sp2 = fs_q_mcp_ics_sp2_positive_left * S ((S (ff_index_mcp_add_ics_sp2_positive)) * ff_pps_mcp_smatrix_ics_sp2) + (ff_left_mcp_add_ics_sp2_positive))) -> (((exists fs_h_mcp_ics_sp2_positive_right. fs_h_mcp_ics_sp2_positive_right + S (ff_right_mcp_add_ics_sp2_positive) = S ((S (ff_index_mcp_add_ics_sp2_positive)) * ff_nns_mcp_smatrix_ics_sp2)) /\ exists fs_q_mcp_ics_sp2_positive_right. ff_nn_mcp_smatrix_ics_sp2 = fs_q_mcp_ics_sp2_positive_right * S ((S (ff_index_mcp_add_ics_sp2_positive)) * ff_nns_mcp_smatrix_ics_sp2) + (ff_right_mcp_add_ics_sp2_positive))) -> (((exists fs_h_mcp_ics_sp2_positive_target. fs_h_mcp_ics_sp2_positive_target + S (ff_target_mcp_add_ics_sp2_positive) = S ((S (ff_index_mcp_add_ics_sp2_positive)) * rc)) /\ exists fs_q_mcp_ics_sp2_positive_target. rb = fs_q_mcp_ics_sp2_positive_target * S ((S (ff_index_mcp_add_ics_sp2_positive)) * rc) + (ff_target_mcp_add_ics_sp2_positive))) -> ff_target_mcp_add_ics_sp2_positive = ff_left_mcp_add_ics_sp2_positive + ff_right_mcp_add_ics_sp2_positive) /\ (forall ff_index_mcp_add_ics_sp2_negative ff_left_mcp_add_ics_sp2_negative ff_right_mcp_add_ics_sp2_negative ff_target_mcp_add_ics_sp2_negative. (exists mcp_gap_ics_sp2_negative_bound. mcp_gap_ics_sp2_negative_bound + S (ff_index_mcp_add_ics_sp2_negative) = ((r) * (1))) -> (((exists fs_h_mcp_ics_sp2_negative_left. fs_h_mcp_ics_sp2_negative_left + S (ff_left_mcp_add_ics_sp2_negative) = S ((S (ff_index_mcp_add_ics_sp2_negative)) * ff_pns_mcp_smatrix_ics_sp2)) /\ exists fs_q_mcp_ics_sp2_negative_left. ff_pn_mcp_smatrix_ics_sp2 = fs_q_mcp_ics_sp2_negative_left * S ((S (ff_index_mcp_add_ics_sp2_negative)) * ff_pns_mcp_smatrix_ics_sp2) + (ff_left_mcp_add_ics_sp2_negative))) -> (((exists fs_h_mcp_ics_sp2_negative_right. fs_h_mcp_ics_sp2_negative_right + S (ff_right_mcp_add_ics_sp2_negative) = S ((S (ff_index_mcp_add_ics_sp2_negative)) * ff_nps_mcp_smatrix_ics_sp2)) /\ exists fs_q_mcp_ics_sp2_negative_right. ff_np_mcp_smatrix_ics_sp2 = fs_q_mcp_ics_sp2_negative_right * S ((S (ff_index_mcp_add_ics_sp2_negative)) * ff_nps_mcp_smatrix_ics_sp2) + (ff_right_mcp_add_ics_sp2_negative))) -> (((exists fs_h_mcp_ics_sp2_negative_target. fs_h_mcp_ics_sp2_negative_target + S (ff_target_mcp_add_ics_sp2_negative) = S ((S (ff_index_mcp_add_ics_sp2_negative)) * sc)) /\ exists fs_q_mcp_ics_sp2_negative_target. sb = fs_q_mcp_ics_sp2_negative_target * S ((S (ff_index_mcp_add_ics_sp2_negative)) * sc) + (ff_target_mcp_add_ics_sp2_negative))) -> ff_target_mcp_add_ics_sp2_negative = ff_left_mcp_add_ics_sp2_negative + ff_right_mcp_add_ics_sp2_negative))))))) -> ((forall ff_index_mcp_add_ics_sp_output_p ff_left_mcp_add_ics_sp_output_p ff_right_mcp_add_ics_sp_output_p ff_target_mcp_add_ics_sp_output_p. (exists mcp_gap_ics_sp_output_p_bound. mcp_gap_ics_sp_output_p_bound + S (ff_index_mcp_add_ics_sp_output_p) = (r * 1)) -> (((exists fs_h_mcp_ics_sp_output_p_left. fs_h_mcp_ics_sp_output_p_left + S (ff_left_mcp_add_ics_sp_output_p) = S ((S (ff_index_mcp_add_ics_sp_output_p)) * pc)) /\ exists fs_q_mcp_ics_sp_output_p_left. pb = fs_q_mcp_ics_sp_output_p_left * S ((S (ff_index_mcp_add_ics_sp_output_p)) * pc) + (ff_left_mcp_add_ics_sp_output_p))) -> (((exists fs_h_mcp_ics_sp_output_p_right. fs_h_mcp_ics_sp_output_p_right + S (ff_right_mcp_add_ics_sp_output_p) = S ((S (ff_index_mcp_add_ics_sp_output_p)) * qc)) /\ exists fs_q_mcp_ics_sp_output_p_right. qb = fs_q_mcp_ics_sp_output_p_right * S ((S (ff_index_mcp_add_ics_sp_output_p)) * qc) + (ff_right_mcp_add_ics_sp_output_p))) -> (((exists fs_h_mcp_ics_sp_output_p_target. fs_h_mcp_ics_sp_output_p_target + S (ff_target_mcp_add_ics_sp_output_p) = S ((S (ff_index_mcp_add_ics_sp_output_p)) * rc)) /\ exists fs_q_mcp_ics_sp_output_p_target. rb = fs_q_mcp_ics_sp_output_p_target * S ((S (ff_index_mcp_add_ics_sp_output_p)) * rc) + (ff_target_mcp_add_ics_sp_output_p))) -> ff_target_mcp_add_ics_sp_output_p = ff_left_mcp_add_ics_sp_output_p + ff_right_mcp_add_ics_sp_output_p) /\ (forall ff_index_mcp_add_ics_sp_output_n ff_left_mcp_add_ics_sp_output_n ff_right_mcp_add_ics_sp_output_n ff_target_mcp_add_ics_sp_output_n. (exists mcp_gap_ics_sp_output_n_bound. mcp_gap_ics_sp_output_n_bound + S (ff_index_mcp_add_ics_sp_output_n) = (r * 1)) -> (((exists fs_h_mcp_ics_sp_output_n_left. fs_h_mcp_ics_sp_output_n_left + S (ff_left_mcp_add_ics_sp_output_n) = S ((S (ff_index_mcp_add_ics_sp_output_n)) * nc)) /\ exists fs_q_mcp_ics_sp_output_n_left. nb = fs_q_mcp_ics_sp_output_n_left * S ((S (ff_index_mcp_add_ics_sp_output_n)) * nc) + (ff_left_mcp_add_ics_sp_output_n))) -> (((exists fs_h_mcp_ics_sp_output_n_right. fs_h_mcp_ics_sp_output_n_right + S (ff_right_mcp_add_ics_sp_output_n) = S ((S (ff_index_mcp_add_ics_sp_output_n)) * mc)) /\ exists fs_q_mcp_ics_sp_output_n_right. mb = fs_q_mcp_ics_sp_output_n_right * S ((S (ff_index_mcp_add_ics_sp_output_n)) * mc) + (ff_right_mcp_add_ics_sp_output_n))) -> (((exists fs_h_mcp_ics_sp_output_n_target. fs_h_mcp_ics_sp_output_n_target + S (ff_target_mcp_add_ics_sp_output_n) = S ((S (ff_index_mcp_add_ics_sp_output_n)) * sc)) /\ exists fs_q_mcp_ics_sp_output_n_target. sb = fs_q_mcp_ics_sp_output_n_target * S ((S (ff_index_mcp_add_ics_sp_output_n)) * sc) + (ff_target_mcp_add_ics_sp_output_n))) -> ff_target_mcp_add_ics_sp_output_n = ff_left_mcp_add_ics_sp_output_n + ff_right_mcp_add_ics_sp_output_n))Complete tactic proof in conservative notation
All 213 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 213 script commands · 26 reading checkpoints · 4 local claims
This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.
Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.
Named ingredients (2) Expand checkpoints Collapse checkpoints Show original steps Find a step
01 Fix variables and assumptions L1–10 Work with arbitrary variables or the premises of the current implication.
L1 intro ab
L2 intro ac
L3 intro db
L4 intro dc
L5 intro eb
L6 intro ec
L7 intro fb
L8 intro fc
L9 intro gb
L10 intro gc
02 Fix variables and assumptions L11–20 Work with arbitrary variables or the premises of the current implication.
L11 intro hb
L12 intro hc
L13 intro ib
L14 intro ic
L15 intro jb
L16 intro jc
L17 intro w
L18 intro r
L19 intro pb
L20 intro pc
03 Fix variables and assumptions L21–30 Work with arbitrary variables or the premises of the current implication.
L21 intro nb
L22 intro nc
L23 intro qb
L24 intro qc
L25 intro mb
L26 intro mc
L27 intro rb
L28 intro rc
L29 intro sb
L30 intro sc
04 Fix variables and assumptions L31–35 Work with arbitrary variables or the premises of the current implication.
L31 intro haddp
L32 intro haddn
L33 intro hfirst
L34 intro hsecond
L35 intro hthird
05 Separate the logical cases L36–45 Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
L36 cases hfirst
L37 cases hfirst_witness
L38 cases hfirst_witness_witness
L39 cases hfirst_witness_witness_witness
L40 cases hfirst_witness_witness_witness_witness
L41 cases hfirst_witness_witness_witness_witness_witness
L42 cases hfirst_witness_witness_witness_witness_witness_witness
L43 cases hfirst_witness_witness_witness_witness_witness_witness_witness
L44 cases hfirst_witness_witness_witness_witness_witness_witness_witness_witness
L45 cases hfirst_witness_witness_witness_witness_witness_witness_witness_witness_right
06 Separate the logical cases L46–55 Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
L46 cases hfirst_witness_witness_witness_witness_witness_witness_witness_witness_right_right
L47 cases hfirst_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right
L48 cases hfirst_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_right
L49 cases hsecond
L50 cases hsecond_witness
L51 cases hsecond_witness_witness
L52 cases hsecond_witness_witness_witness
L53 cases hsecond_witness_witness_witness_witness
L54 cases hsecond_witness_witness_witness_witness_witness
L55 cases hsecond_witness_witness_witness_witness_witness_witness
07 Separate the logical cases L56–65 Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
L56 cases hsecond_witness_witness_witness_witness_witness_witness_witness
L57 cases hsecond_witness_witness_witness_witness_witness_witness_witness_witness
L58 cases hsecond_witness_witness_witness_witness_witness_witness_witness_witness_right
L59 cases hsecond_witness_witness_witness_witness_witness_witness_witness_witness_right_right
L60 cases hsecond_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right
L61 cases hsecond_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_right
L62 cases hthird
L63 cases hthird_witness
L64 cases hthird_witness_witness
L65 cases hthird_witness_witness_witness
08 Separate the logical cases L66–74 Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
L66 cases hthird_witness_witness_witness_witness
L67 cases hthird_witness_witness_witness_witness_witness
L68 cases hthird_witness_witness_witness_witness_witness_witness
L69 cases hthird_witness_witness_witness_witness_witness_witness_witness
L70 cases hthird_witness_witness_witness_witness_witness_witness_witness_witness
L71 cases hthird_witness_witness_witness_witness_witness_witness_witness_witness_right
L72 cases hthird_witness_witness_witness_witness_witness_witness_witness_witness_right_right
L73 cases hthird_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right
L74 cases hthird_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_right
09 Establish hnew0 L75–84 Establish this local claim before using it. It is not an additional assumption.
L75 have hnew0 : MatrixPointwiseAdd(x,x1,x8,x9,x16,x17,r · 1)Definitions: MatrixPointwiseAdd(x,x1,x8,x9,x16,x17,r · 1) Original native command in the exact edition L76 specialize integer_span_natural_product_add_right (ab)
L77 specialize integer_span_natural_product_add_right (ac)
L78 specialize integer_span_natural_product_add_right (eb)
L79 specialize integer_span_natural_product_add_right (ec)
L80 specialize integer_span_natural_product_add_right (gb)
L81 specialize integer_span_natural_product_add_right (gc)
L82 specialize integer_span_natural_product_add_right (ib)
L83 specialize integer_span_natural_product_add_right (ic)
L84 specialize integer_span_natural_product_add_right (w)
10 Use earlier facts L85–94 Instantiate or apply named facts and discharge the corresponding proof obligations.
L85 specialize integer_span_natural_product_add_right (x)
L86 specialize integer_span_natural_product_add_right (x1)
L87 specialize integer_span_natural_product_add_right (x8)
L88 specialize integer_span_natural_product_add_right (x9)
L89 specialize integer_span_natural_product_add_right (x16)
L90 specialize integer_span_natural_product_add_right (x17)
L91 specialize integer_span_natural_product_add_right (r * 1)
L92 apply integer_span_natural_product_add_right
L93 exact haddp
L94 exact hfirst_witness_witness_witness_witness_witness_witness_witness_witness_left
11 Use earlier facts L95–96 Instantiate or apply named facts and discharge the corresponding proof obligations.
L95 exact hsecond_witness_witness_witness_witness_witness_witness_witness_witness_left
L96 exact hthird_witness_witness_witness_witness_witness_witness_witness_witness_left
12 Establish hnew1 L97–106 Establish this local claim before using it. It is not an additional assumption.
L97 have hnew1 : MatrixPointwiseAdd(x2,x3,x10,x11,x18,x19,r · 1)Definitions: MatrixPointwiseAdd(x2,x3,x10,x11,x18,x19,r · 1) Original native command in the exact edition L98 specialize integer_span_natural_product_add_right (db)
L99 specialize integer_span_natural_product_add_right (dc)
L100 specialize integer_span_natural_product_add_right (fb)
L101 specialize integer_span_natural_product_add_right (fc)
L102 specialize integer_span_natural_product_add_right (hb)
L103 specialize integer_span_natural_product_add_right (hc)
L104 specialize integer_span_natural_product_add_right (jb)
L105 specialize integer_span_natural_product_add_right (jc)
L106 specialize integer_span_natural_product_add_right (w)
13 Use earlier facts L107–116 Instantiate or apply named facts and discharge the corresponding proof obligations.
L107 specialize integer_span_natural_product_add_right (x2)
L108 specialize integer_span_natural_product_add_right (x3)
L109 specialize integer_span_natural_product_add_right (x10)
L110 specialize integer_span_natural_product_add_right (x11)
L111 specialize integer_span_natural_product_add_right (x18)
L112 specialize integer_span_natural_product_add_right (x19)
L113 specialize integer_span_natural_product_add_right (r * 1)
L114 apply integer_span_natural_product_add_right
L115 exact haddn
L116 exact hfirst_witness_witness_witness_witness_witness_witness_witness_witness_right_left
14 Use earlier facts L117–118 Instantiate or apply named facts and discharge the corresponding proof obligations.
L117 exact hsecond_witness_witness_witness_witness_witness_witness_witness_witness_right_left
L118 exact hthird_witness_witness_witness_witness_witness_witness_witness_witness_right_left
15 Establish hnew2 L119–128 Establish this local claim before using it. It is not an additional assumption.
L119 have hnew2 : MatrixPointwiseAdd(x4,x5,x12,x13,x20,x21,r · 1)Definitions: MatrixPointwiseAdd(x4,x5,x12,x13,x20,x21,r · 1) Original native command in the exact edition L120 specialize integer_span_natural_product_add_right (ab)
L121 specialize integer_span_natural_product_add_right (ac)
L122 specialize integer_span_natural_product_add_right (fb)
L123 specialize integer_span_natural_product_add_right (fc)
L124 specialize integer_span_natural_product_add_right (hb)
L125 specialize integer_span_natural_product_add_right (hc)
L126 specialize integer_span_natural_product_add_right (jb)
L127 specialize integer_span_natural_product_add_right (jc)
L128 specialize integer_span_natural_product_add_right (w)
16 Use earlier facts L129–138 Instantiate or apply named facts and discharge the corresponding proof obligations.
L129 specialize integer_span_natural_product_add_right (x4)
L130 specialize integer_span_natural_product_add_right (x5)
L131 specialize integer_span_natural_product_add_right (x12)
L132 specialize integer_span_natural_product_add_right (x13)
L133 specialize integer_span_natural_product_add_right (x20)
L134 specialize integer_span_natural_product_add_right (x21)
L135 specialize integer_span_natural_product_add_right (r * 1)
L136 apply integer_span_natural_product_add_right
L137 exact haddn
L138 exact hfirst_witness_witness_witness_witness_witness_witness_witness_witness_right_right_left
17 Use earlier facts L139–140 Instantiate or apply named facts and discharge the corresponding proof obligations.
L139 exact hsecond_witness_witness_witness_witness_witness_witness_witness_witness_right_right_left
L140 exact hthird_witness_witness_witness_witness_witness_witness_witness_witness_right_right_left
18 Establish hnew3 L141–150 Establish this local claim before using it. It is not an additional assumption.
L141 have hnew3 : MatrixPointwiseAdd(x6,x7,x14,x15,x22,x23,r · 1)Definitions: MatrixPointwiseAdd(x6,x7,x14,x15,x22,x23,r · 1) Original native command in the exact edition L142 specialize integer_span_natural_product_add_right (db)
L143 specialize integer_span_natural_product_add_right (dc)
L144 specialize integer_span_natural_product_add_right (eb)
L145 specialize integer_span_natural_product_add_right (ec)
L146 specialize integer_span_natural_product_add_right (gb)
L147 specialize integer_span_natural_product_add_right (gc)
L148 specialize integer_span_natural_product_add_right (ib)
L149 specialize integer_span_natural_product_add_right (ic)
L150 specialize integer_span_natural_product_add_right (w)
19 Use earlier facts L151–160 Instantiate or apply named facts and discharge the corresponding proof obligations.
L151 specialize integer_span_natural_product_add_right (x6)
L152 specialize integer_span_natural_product_add_right (x7)
L153 specialize integer_span_natural_product_add_right (x14)
L154 specialize integer_span_natural_product_add_right (x15)
L155 specialize integer_span_natural_product_add_right (x22)
L156 specialize integer_span_natural_product_add_right (x23)
L157 specialize integer_span_natural_product_add_right (r * 1)
L158 apply integer_span_natural_product_add_right
L159 exact haddp
L160 exact hfirst_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_left
20 Use earlier facts L161–162 Instantiate or apply named facts and discharge the corresponding proof obligations.
L161 exact hsecond_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_left
L162 exact hthird_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_left
21 Separate the logical cases L163–163 Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
L163 split
22 Use earlier facts L164–173 Instantiate or apply named facts and discharge the corresponding proof obligations.
L164 specialize integer_span_pointwise_add_interchange (x)
L165 specialize integer_span_pointwise_add_interchange (x1)
L166 specialize integer_span_pointwise_add_interchange (x2)
L167 specialize integer_span_pointwise_add_interchange (x3)
L168 specialize integer_span_pointwise_add_interchange (x8)
L169 specialize integer_span_pointwise_add_interchange (x9)
L170 specialize integer_span_pointwise_add_interchange (x10)
L171 specialize integer_span_pointwise_add_interchange (x11)
L172 specialize integer_span_pointwise_add_interchange (x16)
L173 specialize integer_span_pointwise_add_interchange (x17)
23 Use earlier facts L174–183 Instantiate or apply named facts and discharge the corresponding proof obligations.
L174 specialize integer_span_pointwise_add_interchange (x18)
L175 specialize integer_span_pointwise_add_interchange (x19)
L176 specialize integer_span_pointwise_add_interchange (pb)
L177 specialize integer_span_pointwise_add_interchange (pc)
L178 specialize integer_span_pointwise_add_interchange (qb)
L179 specialize integer_span_pointwise_add_interchange (qc)
L180 specialize integer_span_pointwise_add_interchange (rb)
L181 specialize integer_span_pointwise_add_interchange (rc)
L182 specialize integer_span_pointwise_add_interchange (r * 1)
L183 apply integer_span_pointwise_add_interchange
24 Use earlier facts L184–193 Instantiate or apply named facts and discharge the corresponding proof obligations.
L184 exact hfirst_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_right_left
L185 exact hsecond_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_right_left
L186 exact hthird_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_right_left
L187 exact hnew0
L188 exact hnew1
L189 specialize integer_span_pointwise_add_interchange (x4)
L190 specialize integer_span_pointwise_add_interchange (x5)
L191 specialize integer_span_pointwise_add_interchange (x6)
L192 specialize integer_span_pointwise_add_interchange (x7)
L193 specialize integer_span_pointwise_add_interchange (x12)
25 Use earlier facts L194–203 Instantiate or apply named facts and discharge the corresponding proof obligations.
L194 specialize integer_span_pointwise_add_interchange (x13)
L195 specialize integer_span_pointwise_add_interchange (x14)
L196 specialize integer_span_pointwise_add_interchange (x15)
L197 specialize integer_span_pointwise_add_interchange (x20)
L198 specialize integer_span_pointwise_add_interchange (x21)
L199 specialize integer_span_pointwise_add_interchange (x22)
L200 specialize integer_span_pointwise_add_interchange (x23)
L201 specialize integer_span_pointwise_add_interchange (nb)
L202 specialize integer_span_pointwise_add_interchange (nc)
L203 specialize integer_span_pointwise_add_interchange (mb)
26 Use earlier facts L204–213 Instantiate or apply named facts and discharge the corresponding proof obligations.
L204 specialize integer_span_pointwise_add_interchange (mc)
L205 specialize integer_span_pointwise_add_interchange (sb)
L206 specialize integer_span_pointwise_add_interchange (sc)
L207 specialize integer_span_pointwise_add_interchange (r * 1)
L208 apply integer_span_pointwise_add_interchange
L209 exact hfirst_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_right_right
L210 exact hsecond_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_right_right
L211 exact hthird_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_right_right
L212 exact hnew2
L213 exact hnew3
Library-wide reading audit
Original defined command ledger · 213 lines 0001 intro ab0002 intro ac0003 intro db0004 intro dc0005 intro eb0006 intro ec0007 intro fb0008 intro fc0009 intro gb0010 intro gc0011 intro hb0012 intro hc0013 intro ib0014 intro ic0015 intro jb0016 intro jc0017 intro w0018 intro r0019 intro pb0020 intro pc0021 intro nb0022 intro nc0023 intro qb0024 intro qc0025 intro mb0026 intro mc0027 intro rb0028 intro rc0029 intro sb0030 intro sc0031 intro haddp0032 intro haddn0033 intro hfirst0034 intro hsecond0035 intro hthird0036 cases hfirst0037 cases hfirst_witness0038 cases hfirst_witness_witness0039 cases hfirst_witness_witness_witness0040 cases hfirst_witness_witness_witness_witness0041 cases hfirst_witness_witness_witness_witness_witness0042 cases hfirst_witness_witness_witness_witness_witness_witness0043 cases hfirst_witness_witness_witness_witness_witness_witness_witness0044 cases hfirst_witness_witness_witness_witness_witness_witness_witness_witness0045 cases hfirst_witness_witness_witness_witness_witness_witness_witness_witness_right0046 cases hfirst_witness_witness_witness_witness_witness_witness_witness_witness_right_right0047 cases hfirst_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right0048 cases hfirst_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_right0049 cases hsecond0050 cases hsecond_witness0051 cases hsecond_witness_witness0052 cases hsecond_witness_witness_witness0053 cases hsecond_witness_witness_witness_witness0054 cases hsecond_witness_witness_witness_witness_witness0055 cases hsecond_witness_witness_witness_witness_witness_witness0056 cases hsecond_witness_witness_witness_witness_witness_witness_witness0057 cases hsecond_witness_witness_witness_witness_witness_witness_witness_witness0058 cases hsecond_witness_witness_witness_witness_witness_witness_witness_witness_right0059 cases hsecond_witness_witness_witness_witness_witness_witness_witness_witness_right_right0060 cases hsecond_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right0061 cases hsecond_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_right0062 cases hthird0063 cases hthird_witness0064 cases hthird_witness_witness0065 cases hthird_witness_witness_witness0066 cases hthird_witness_witness_witness_witness0067 cases hthird_witness_witness_witness_witness_witness0068 cases hthird_witness_witness_witness_witness_witness_witness0069 cases hthird_witness_witness_witness_witness_witness_witness_witness0070 cases hthird_witness_witness_witness_witness_witness_witness_witness_witness0071 cases hthird_witness_witness_witness_witness_witness_witness_witness_witness_right0072 cases hthird_witness_witness_witness_witness_witness_witness_witness_witness_right_right0073 cases hthird_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right0074 cases hthird_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_right0075 have hnew0 : MatrixPointwiseAdd(x,x1,x8,x9,x16,x17,r · 1) 0076 specialize integer_span_natural_product_add_right (ab)0077 specialize integer_span_natural_product_add_right (ac)0078 specialize integer_span_natural_product_add_right (eb)0079 specialize integer_span_natural_product_add_right (ec)0080 specialize integer_span_natural_product_add_right (gb)0081 specialize integer_span_natural_product_add_right (gc)0082 specialize integer_span_natural_product_add_right (ib)0083 specialize integer_span_natural_product_add_right (ic)0084 specialize integer_span_natural_product_add_right (w)0085 specialize integer_span_natural_product_add_right (x)0086 specialize integer_span_natural_product_add_right (x1)0087 specialize integer_span_natural_product_add_right (x8)0088 specialize integer_span_natural_product_add_right (x9)0089 specialize integer_span_natural_product_add_right (x16)0090 specialize integer_span_natural_product_add_right (x17)0091 specialize integer_span_natural_product_add_right (r * 1)0092 apply integer_span_natural_product_add_right 0093 exact haddp0094 exact hfirst_witness_witness_witness_witness_witness_witness_witness_witness_left0095 exact hsecond_witness_witness_witness_witness_witness_witness_witness_witness_left0096 exact hthird_witness_witness_witness_witness_witness_witness_witness_witness_left0097 have hnew1 : MatrixPointwiseAdd(x2,x3,x10,x11,x18,x19,r · 1) 0098 specialize integer_span_natural_product_add_right (db)0099 specialize integer_span_natural_product_add_right (dc)0100 specialize integer_span_natural_product_add_right (fb)0101 specialize integer_span_natural_product_add_right (fc)0102 specialize integer_span_natural_product_add_right (hb)0103 specialize integer_span_natural_product_add_right (hc)0104 specialize integer_span_natural_product_add_right (jb)0105 specialize integer_span_natural_product_add_right (jc)0106 specialize integer_span_natural_product_add_right (w)0107 specialize integer_span_natural_product_add_right (x2)0108 specialize integer_span_natural_product_add_right (x3)0109 specialize integer_span_natural_product_add_right (x10)0110 specialize integer_span_natural_product_add_right (x11)0111 specialize integer_span_natural_product_add_right (x18)0112 specialize integer_span_natural_product_add_right (x19)0113 specialize integer_span_natural_product_add_right (r * 1)0114 apply integer_span_natural_product_add_right 0115 exact haddn0116 exact hfirst_witness_witness_witness_witness_witness_witness_witness_witness_right_left0117 exact hsecond_witness_witness_witness_witness_witness_witness_witness_witness_right_left0118 exact hthird_witness_witness_witness_witness_witness_witness_witness_witness_right_left0119 have hnew2 : MatrixPointwiseAdd(x4,x5,x12,x13,x20,x21,r · 1) 0120 specialize integer_span_natural_product_add_right (ab)0121 specialize integer_span_natural_product_add_right (ac)0122 specialize integer_span_natural_product_add_right (fb)0123 specialize integer_span_natural_product_add_right (fc)0124 specialize integer_span_natural_product_add_right (hb)0125 specialize integer_span_natural_product_add_right (hc)0126 specialize integer_span_natural_product_add_right (jb)0127 specialize integer_span_natural_product_add_right (jc)0128 specialize integer_span_natural_product_add_right (w)0129 specialize integer_span_natural_product_add_right (x4)0130 specialize integer_span_natural_product_add_right (x5)0131 specialize integer_span_natural_product_add_right (x12)0132 specialize integer_span_natural_product_add_right (x13)0133 specialize integer_span_natural_product_add_right (x20)0134 specialize integer_span_natural_product_add_right (x21)0135 specialize integer_span_natural_product_add_right (r * 1)0136 apply integer_span_natural_product_add_right 0137 exact haddn0138 exact hfirst_witness_witness_witness_witness_witness_witness_witness_witness_right_right_left0139 exact hsecond_witness_witness_witness_witness_witness_witness_witness_witness_right_right_left0140 exact hthird_witness_witness_witness_witness_witness_witness_witness_witness_right_right_left0141 have hnew3 : MatrixPointwiseAdd(x6,x7,x14,x15,x22,x23,r · 1) 0142 specialize integer_span_natural_product_add_right (db)0143 specialize integer_span_natural_product_add_right (dc)0144 specialize integer_span_natural_product_add_right (eb)0145 specialize integer_span_natural_product_add_right (ec)0146 specialize integer_span_natural_product_add_right (gb)0147 specialize integer_span_natural_product_add_right (gc)0148 specialize integer_span_natural_product_add_right (ib)0149 specialize integer_span_natural_product_add_right (ic)0150 specialize integer_span_natural_product_add_right (w)0151 specialize integer_span_natural_product_add_right (x6)0152 specialize integer_span_natural_product_add_right (x7)0153 specialize integer_span_natural_product_add_right (x14)0154 specialize integer_span_natural_product_add_right (x15)0155 specialize integer_span_natural_product_add_right (x22)0156 specialize integer_span_natural_product_add_right (x23)0157 specialize integer_span_natural_product_add_right (r * 1)0158 apply integer_span_natural_product_add_right 0159 exact haddp0160 exact hfirst_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_left0161 exact hsecond_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_left0162 exact hthird_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_left0163 split0164 specialize integer_span_pointwise_add_interchange (x)0165 specialize integer_span_pointwise_add_interchange (x1)0166 specialize integer_span_pointwise_add_interchange (x2)0167 specialize integer_span_pointwise_add_interchange (x3)0168 specialize integer_span_pointwise_add_interchange (x8)0169 specialize integer_span_pointwise_add_interchange (x9)0170 specialize integer_span_pointwise_add_interchange (x10)0171 specialize integer_span_pointwise_add_interchange (x11)0172 specialize integer_span_pointwise_add_interchange (x16)0173 specialize integer_span_pointwise_add_interchange (x17)0174 specialize integer_span_pointwise_add_interchange (x18)0175 specialize integer_span_pointwise_add_interchange (x19)0176 specialize integer_span_pointwise_add_interchange (pb)0177 specialize integer_span_pointwise_add_interchange (pc)0178 specialize integer_span_pointwise_add_interchange (qb)0179 specialize integer_span_pointwise_add_interchange (qc)0180 specialize integer_span_pointwise_add_interchange (rb)0181 specialize integer_span_pointwise_add_interchange (rc)0182 specialize integer_span_pointwise_add_interchange (r * 1)0183 apply integer_span_pointwise_add_interchange 0184 exact hfirst_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_right_left0185 exact hsecond_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_right_left0186 exact hthird_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_right_left0187 exact hnew00188 exact hnew10189 specialize integer_span_pointwise_add_interchange (x4)0190 specialize integer_span_pointwise_add_interchange (x5)0191 specialize integer_span_pointwise_add_interchange (x6)0192 specialize integer_span_pointwise_add_interchange (x7)0193 specialize integer_span_pointwise_add_interchange (x12)0194 specialize integer_span_pointwise_add_interchange (x13)0195 specialize integer_span_pointwise_add_interchange (x14)0196 specialize integer_span_pointwise_add_interchange (x15)0197 specialize integer_span_pointwise_add_interchange (x20)0198 specialize integer_span_pointwise_add_interchange (x21)0199 specialize integer_span_pointwise_add_interchange (x22)0200 specialize integer_span_pointwise_add_interchange (x23)0201 specialize integer_span_pointwise_add_interchange (nb)0202 specialize integer_span_pointwise_add_interchange (nc)0203 specialize integer_span_pointwise_add_interchange (mb)0204 specialize integer_span_pointwise_add_interchange (mc)0205 specialize integer_span_pointwise_add_interchange (sb)0206 specialize integer_span_pointwise_add_interchange (sc)0207 specialize integer_span_pointwise_add_interchange (r * 1)0208 apply integer_span_pointwise_add_interchange 0209 exact hfirst_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_right_right0210 exact hsecond_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_right_right0211 exact hthird_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_right_right0212 exact hnew20213 exact hnew3