Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.
This branch proves the finite determinant/rank/span substrate. It does not claim Smith or Hermite normal form, lattice index equals determinant, determinant multiplicativity, lattice reduction, or geometry-of-numbers theorems.
Exact theorem in conservative defined notation
∀ ab. ∀ ac. ∀ db. ∀ dc. ∀ eb. ∀ ec. ∀ fb. ∀ fc. ∀ w. ∀ r. ∀ pb. ∀ pc. ∀ nb. ∀ nc. ∀ qb. ∀ qc. ∀ mb. ∀ mc. IntegerMatrixVectorProduct(ab,ac,db,dc,eb,ec,fb,fc,w,r,pb,pc,nb,nc) → IntegerVectorEqual(pb,pc,nb,nc,qb,qc,mb,mc,r) → IntegerMatrixVectorProduct(ab,ac,db,dc,eb,ec,fb,fc,w,r,qb,qc,mb,mc)Every linked abbreviation expands hygienically to the identical original native formula.
Definition DAG
Actual proof prerequisites
Original expanded first-order statement
forall ab ac db dc eb ec fb fc w r pb pc nb nc qb qc mb mc. (exists ics_raw_positive_linear_transport_source ics_raw_positive_scale_linear_transport_source ics_raw_negative_linear_transport_source ics_raw_negative_scale_linear_transport_source. (((exists ff_pp_mcp_smatrix_ics_linear_transport_source_raw ff_pps_mcp_smatrix_ics_linear_transport_source_raw ff_nn_mcp_smatrix_ics_linear_transport_source_raw ff_nns_mcp_smatrix_ics_linear_transport_source_raw ff_pn_mcp_smatrix_ics_linear_transport_source_raw ff_pns_mcp_smatrix_ics_linear_transport_source_raw ff_np_mcp_smatrix_ics_linear_transport_source_raw ff_nps_mcp_smatrix_ics_linear_transport_source_raw. ((forall ff_index_mcp_prefix_ics_linear_transport_source_raw_pp. (exists mcp_gap_ics_linear_transport_source_raw_pp_index. mcp_gap_ics_linear_transport_source_raw_pp_index + S (ff_index_mcp_prefix_ics_linear_transport_source_raw_pp) = ((r) * (1))) -> exists ff_row_mcp_prefix_ics_linear_transport_source_raw_pp ff_column_mcp_prefix_ics_linear_transport_source_raw_pp ff_value_mcp_prefix_ics_linear_transport_source_raw_pp. ((ff_index_mcp_prefix_ics_linear_transport_source_raw_pp) = (1) * ff_row_mcp_prefix_ics_linear_transport_source_raw_pp + ff_column_mcp_prefix_ics_linear_transport_source_raw_pp /\ ((exists mcp_gap_ics_linear_transport_source_raw_pp_column. mcp_gap_ics_linear_transport_source_raw_pp_column + S (ff_column_mcp_prefix_ics_linear_transport_source_raw_pp) = (1)) /\ ((exists ff_left_mcp_cell_ics_linear_transport_source_raw_pp_cell ff_left_scale_mcp_cell_ics_linear_transport_source_raw_pp_cell ff_right_mcp_cell_ics_linear_transport_source_raw_pp_cell ff_right_scale_mcp_cell_ics_linear_transport_source_raw_pp_cell. ((forall ff_index_mcp_ics_linear_transport_source_raw_pp_cell_row ff_source_mcp_ics_linear_transport_source_raw_pp_cell_row ff_target_mcp_ics_linear_transport_source_raw_pp_cell_row. (exists mcp_gap_ics_linear_transport_source_raw_pp_cell_row_bound. mcp_gap_ics_linear_transport_source_raw_pp_cell_row_bound + S (ff_index_mcp_ics_linear_transport_source_raw_pp_cell_row) = (w)) -> (((exists fs_h_mcp_ics_linear_transport_source_raw_pp_cell_row_source. fs_h_mcp_ics_linear_transport_source_raw_pp_cell_row_source + S (ff_source_mcp_ics_linear_transport_source_raw_pp_cell_row) = S ((S (((ff_row_mcp_prefix_ics_linear_transport_source_raw_pp) * (w)) + (1) * ff_index_mcp_ics_linear_transport_source_raw_pp_cell_row)) * ac)) /\ exists fs_q_mcp_ics_linear_transport_source_raw_pp_cell_row_source. ab = fs_q_mcp_ics_linear_transport_source_raw_pp_cell_row_source * S ((S (((ff_row_mcp_prefix_ics_linear_transport_source_raw_pp) * (w)) + (1) * ff_index_mcp_ics_linear_transport_source_raw_pp_cell_row)) * ac) + (ff_source_mcp_ics_linear_transport_source_raw_pp_cell_row))) -> (((exists fs_h_mcp_ics_linear_transport_source_raw_pp_cell_row_target. fs_h_mcp_ics_linear_transport_source_raw_pp_cell_row_target + S (ff_target_mcp_ics_linear_transport_source_raw_pp_cell_row) = S ((S (ff_index_mcp_ics_linear_transport_source_raw_pp_cell_row)) * ff_left_scale_mcp_cell_ics_linear_transport_source_raw_pp_cell)) /\ exists fs_q_mcp_ics_linear_transport_source_raw_pp_cell_row_target. ff_left_mcp_cell_ics_linear_transport_source_raw_pp_cell = fs_q_mcp_ics_linear_transport_source_raw_pp_cell_row_target * S ((S (ff_index_mcp_ics_linear_transport_source_raw_pp_cell_row)) * ff_left_scale_mcp_cell_ics_linear_transport_source_raw_pp_cell) + (ff_target_mcp_ics_linear_transport_source_raw_pp_cell_row))) -> ff_target_mcp_ics_linear_transport_source_raw_pp_cell_row = ff_source_mcp_ics_linear_transport_source_raw_pp_cell_row) /\ ((forall ff_index_mcp_ics_linear_transport_source_raw_pp_cell_column ff_source_mcp_ics_linear_transport_source_raw_pp_cell_column ff_target_mcp_ics_linear_transport_source_raw_pp_cell_column. (exists mcp_gap_ics_linear_transport_source_raw_pp_cell_column_bound. mcp_gap_ics_linear_transport_source_raw_pp_cell_column_bound + S (ff_index_mcp_ics_linear_transport_source_raw_pp_cell_column) = (w)) -> (((exists fs_h_mcp_ics_linear_transport_source_raw_pp_cell_column_source. fs_h_mcp_ics_linear_transport_source_raw_pp_cell_column_source + S (ff_source_mcp_ics_linear_transport_source_raw_pp_cell_column) = S ((S ((ff_column_mcp_prefix_ics_linear_transport_source_raw_pp) + (1) * ff_index_mcp_ics_linear_transport_source_raw_pp_cell_column)) * ec)) /\ exists fs_q_mcp_ics_linear_transport_source_raw_pp_cell_column_source. eb = fs_q_mcp_ics_linear_transport_source_raw_pp_cell_column_source * S ((S ((ff_column_mcp_prefix_ics_linear_transport_source_raw_pp) + (1) * ff_index_mcp_ics_linear_transport_source_raw_pp_cell_column)) * ec) + (ff_source_mcp_ics_linear_transport_source_raw_pp_cell_column))) -> (((exists fs_h_mcp_ics_linear_transport_source_raw_pp_cell_column_target. fs_h_mcp_ics_linear_transport_source_raw_pp_cell_column_target + S (ff_target_mcp_ics_linear_transport_source_raw_pp_cell_column) = S ((S (ff_index_mcp_ics_linear_transport_source_raw_pp_cell_column)) * ff_right_scale_mcp_cell_ics_linear_transport_source_raw_pp_cell)) /\ exists fs_q_mcp_ics_linear_transport_source_raw_pp_cell_column_target. ff_right_mcp_cell_ics_linear_transport_source_raw_pp_cell = fs_q_mcp_ics_linear_transport_source_raw_pp_cell_column_target * S ((S (ff_index_mcp_ics_linear_transport_source_raw_pp_cell_column)) * ff_right_scale_mcp_cell_ics_linear_transport_source_raw_pp_cell) + (ff_target_mcp_ics_linear_transport_source_raw_pp_cell_column))) -> ff_target_mcp_ics_linear_transport_source_raw_pp_cell_column = ff_source_mcp_ics_linear_transport_source_raw_pp_cell_column) /\ (exists ff_code_dot_mcp_ics_linear_transport_source_raw_pp_cell_dot ff_scale_dot_mcp_ics_linear_transport_source_raw_pp_cell_dot. ((forall fpmp_index_dot_mcp_ics_linear_transport_source_raw_pp_cell_dot_pointwise fpmp_left_dot_mcp_ics_linear_transport_source_raw_pp_cell_dot_pointwise fpmp_right_dot_mcp_ics_linear_transport_source_raw_pp_cell_dot_pointwise fpmp_target_dot_mcp_ics_linear_transport_source_raw_pp_cell_dot_pointwise. (exists fpmp_gap_dot_mcp_ics_linear_transport_source_raw_pp_cell_dot_pointwise. fpmp_gap_dot_mcp_ics_linear_transport_source_raw_pp_cell_dot_pointwise + S fpmp_index_dot_mcp_ics_linear_transport_source_raw_pp_cell_dot_pointwise = w) -> (((exists ff_h_fpmp_dot_mcp_ics_linear_transport_source_raw_pp_cell_dot_pointwise_left. ff_h_fpmp_dot_mcp_ics_linear_transport_source_raw_pp_cell_dot_pointwise_left + S (fpmp_left_dot_mcp_ics_linear_transport_source_raw_pp_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_linear_transport_source_raw_pp_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_linear_transport_source_raw_pp_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_linear_transport_source_raw_pp_cell_dot_pointwise_left. ff_left_mcp_cell_ics_linear_transport_source_raw_pp_cell = ff_q_fpmp_dot_mcp_ics_linear_transport_source_raw_pp_cell_dot_pointwise_left * S ((S (fpmp_index_dot_mcp_ics_linear_transport_source_raw_pp_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_linear_transport_source_raw_pp_cell) + (fpmp_left_dot_mcp_ics_linear_transport_source_raw_pp_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_linear_transport_source_raw_pp_cell_dot_pointwise_right. ff_h_fpmp_dot_mcp_ics_linear_transport_source_raw_pp_cell_dot_pointwise_right + S (fpmp_right_dot_mcp_ics_linear_transport_source_raw_pp_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_linear_transport_source_raw_pp_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_linear_transport_source_raw_pp_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_linear_transport_source_raw_pp_cell_dot_pointwise_right. ff_right_mcp_cell_ics_linear_transport_source_raw_pp_cell = ff_q_fpmp_dot_mcp_ics_linear_transport_source_raw_pp_cell_dot_pointwise_right * S ((S (fpmp_index_dot_mcp_ics_linear_transport_source_raw_pp_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_linear_transport_source_raw_pp_cell) + (fpmp_right_dot_mcp_ics_linear_transport_source_raw_pp_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_linear_transport_source_raw_pp_cell_dot_pointwise_target. ff_h_fpmp_dot_mcp_ics_linear_transport_source_raw_pp_cell_dot_pointwise_target + S (fpmp_target_dot_mcp_ics_linear_transport_source_raw_pp_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_linear_transport_source_raw_pp_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_linear_transport_source_raw_pp_cell_dot)) /\ exists ff_q_fpmp_dot_mcp_ics_linear_transport_source_raw_pp_cell_dot_pointwise_target. ff_code_dot_mcp_ics_linear_transport_source_raw_pp_cell_dot = ff_q_fpmp_dot_mcp_ics_linear_transport_source_raw_pp_cell_dot_pointwise_target * S ((S (fpmp_index_dot_mcp_ics_linear_transport_source_raw_pp_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_linear_transport_source_raw_pp_cell_dot) + (fpmp_target_dot_mcp_ics_linear_transport_source_raw_pp_cell_dot_pointwise))) -> fpmp_target_dot_mcp_ics_linear_transport_source_raw_pp_cell_dot_pointwise = fpmp_left_dot_mcp_ics_linear_transport_source_raw_pp_cell_dot_pointwise * fpmp_right_dot_mcp_ics_linear_transport_source_raw_pp_cell_dot_pointwise) /\ (exists ff_u_dot_mcp_ics_linear_transport_source_raw_pp_cell_dot_sum ff_v_dot_mcp_ics_linear_transport_source_raw_pp_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_linear_transport_source_raw_pp_cell_dot_sum_start. ff_h_dot_mcp_ics_linear_transport_source_raw_pp_cell_dot_sum_start + S (0) = S ((S (0)) * ff_v_dot_mcp_ics_linear_transport_source_raw_pp_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_linear_transport_source_raw_pp_cell_dot_sum_start. ff_u_dot_mcp_ics_linear_transport_source_raw_pp_cell_dot_sum = ff_q_dot_mcp_ics_linear_transport_source_raw_pp_cell_dot_sum_start * S ((S (0)) * ff_v_dot_mcp_ics_linear_transport_source_raw_pp_cell_dot_sum) + (0))) /\ ((((exists ff_h_dot_mcp_ics_linear_transport_source_raw_pp_cell_dot_sum_terminal. ff_h_dot_mcp_ics_linear_transport_source_raw_pp_cell_dot_sum_terminal + S (ff_value_mcp_prefix_ics_linear_transport_source_raw_pp) = S ((S (w)) * ff_v_dot_mcp_ics_linear_transport_source_raw_pp_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_linear_transport_source_raw_pp_cell_dot_sum_terminal. ff_u_dot_mcp_ics_linear_transport_source_raw_pp_cell_dot_sum = ff_q_dot_mcp_ics_linear_transport_source_raw_pp_cell_dot_sum_terminal * S ((S (w)) * ff_v_dot_mcp_ics_linear_transport_source_raw_pp_cell_dot_sum) + (ff_value_mcp_prefix_ics_linear_transport_source_raw_pp))) /\ forall ff_i_dot_mcp_ics_linear_transport_source_raw_pp_cell_dot_sum. (exists ff_lt_dot_mcp_ics_linear_transport_source_raw_pp_cell_dot_sum_bound. ff_lt_dot_mcp_ics_linear_transport_source_raw_pp_cell_dot_sum_bound + S ff_i_dot_mcp_ics_linear_transport_source_raw_pp_cell_dot_sum = w) -> exists ff_a_dot_mcp_ics_linear_transport_source_raw_pp_cell_dot_sum ff_r_dot_mcp_ics_linear_transport_source_raw_pp_cell_dot_sum ff_s_dot_mcp_ics_linear_transport_source_raw_pp_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_linear_transport_source_raw_pp_cell_dot_sum_summand. ff_h_dot_mcp_ics_linear_transport_source_raw_pp_cell_dot_sum_summand + S (ff_a_dot_mcp_ics_linear_transport_source_raw_pp_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_linear_transport_source_raw_pp_cell_dot_sum)) * ff_scale_dot_mcp_ics_linear_transport_source_raw_pp_cell_dot)) /\ exists ff_q_dot_mcp_ics_linear_transport_source_raw_pp_cell_dot_sum_summand. ff_code_dot_mcp_ics_linear_transport_source_raw_pp_cell_dot = ff_q_dot_mcp_ics_linear_transport_source_raw_pp_cell_dot_sum_summand * S ((S (ff_i_dot_mcp_ics_linear_transport_source_raw_pp_cell_dot_sum)) * ff_scale_dot_mcp_ics_linear_transport_source_raw_pp_cell_dot) + (ff_a_dot_mcp_ics_linear_transport_source_raw_pp_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_linear_transport_source_raw_pp_cell_dot_sum_partial. ff_h_dot_mcp_ics_linear_transport_source_raw_pp_cell_dot_sum_partial + S (ff_r_dot_mcp_ics_linear_transport_source_raw_pp_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_linear_transport_source_raw_pp_cell_dot_sum)) * ff_v_dot_mcp_ics_linear_transport_source_raw_pp_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_linear_transport_source_raw_pp_cell_dot_sum_partial. ff_u_dot_mcp_ics_linear_transport_source_raw_pp_cell_dot_sum = ff_q_dot_mcp_ics_linear_transport_source_raw_pp_cell_dot_sum_partial * S ((S (ff_i_dot_mcp_ics_linear_transport_source_raw_pp_cell_dot_sum)) * ff_v_dot_mcp_ics_linear_transport_source_raw_pp_cell_dot_sum) + (ff_r_dot_mcp_ics_linear_transport_source_raw_pp_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_linear_transport_source_raw_pp_cell_dot_sum_successor. ff_h_dot_mcp_ics_linear_transport_source_raw_pp_cell_dot_sum_successor + S (ff_s_dot_mcp_ics_linear_transport_source_raw_pp_cell_dot_sum) = S ((S (S ff_i_dot_mcp_ics_linear_transport_source_raw_pp_cell_dot_sum)) * ff_v_dot_mcp_ics_linear_transport_source_raw_pp_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_linear_transport_source_raw_pp_cell_dot_sum_successor. ff_u_dot_mcp_ics_linear_transport_source_raw_pp_cell_dot_sum = ff_q_dot_mcp_ics_linear_transport_source_raw_pp_cell_dot_sum_successor * S ((S (S ff_i_dot_mcp_ics_linear_transport_source_raw_pp_cell_dot_sum)) * ff_v_dot_mcp_ics_linear_transport_source_raw_pp_cell_dot_sum) + (ff_s_dot_mcp_ics_linear_transport_source_raw_pp_cell_dot_sum))) /\ ff_s_dot_mcp_ics_linear_transport_source_raw_pp_cell_dot_sum = ff_r_dot_mcp_ics_linear_transport_source_raw_pp_cell_dot_sum + ff_a_dot_mcp_ics_linear_transport_source_raw_pp_cell_dot_sum))))))))))) /\ (((exists fs_h_mcp_ics_linear_transport_source_raw_pp_entry. fs_h_mcp_ics_linear_transport_source_raw_pp_entry + S (ff_value_mcp_prefix_ics_linear_transport_source_raw_pp) = S ((S (ff_index_mcp_prefix_ics_linear_transport_source_raw_pp)) * ff_pps_mcp_smatrix_ics_linear_transport_source_raw)) /\ exists fs_q_mcp_ics_linear_transport_source_raw_pp_entry. ff_pp_mcp_smatrix_ics_linear_transport_source_raw = fs_q_mcp_ics_linear_transport_source_raw_pp_entry * S ((S (ff_index_mcp_prefix_ics_linear_transport_source_raw_pp)) * ff_pps_mcp_smatrix_ics_linear_transport_source_raw) + (ff_value_mcp_prefix_ics_linear_transport_source_raw_pp))))))) /\ ((forall ff_index_mcp_prefix_ics_linear_transport_source_raw_nn. (exists mcp_gap_ics_linear_transport_source_raw_nn_index. mcp_gap_ics_linear_transport_source_raw_nn_index + S (ff_index_mcp_prefix_ics_linear_transport_source_raw_nn) = ((r) * (1))) -> exists ff_row_mcp_prefix_ics_linear_transport_source_raw_nn ff_column_mcp_prefix_ics_linear_transport_source_raw_nn ff_value_mcp_prefix_ics_linear_transport_source_raw_nn. ((ff_index_mcp_prefix_ics_linear_transport_source_raw_nn) = (1) * ff_row_mcp_prefix_ics_linear_transport_source_raw_nn + ff_column_mcp_prefix_ics_linear_transport_source_raw_nn /\ ((exists mcp_gap_ics_linear_transport_source_raw_nn_column. mcp_gap_ics_linear_transport_source_raw_nn_column + S (ff_column_mcp_prefix_ics_linear_transport_source_raw_nn) = (1)) /\ ((exists ff_left_mcp_cell_ics_linear_transport_source_raw_nn_cell ff_left_scale_mcp_cell_ics_linear_transport_source_raw_nn_cell ff_right_mcp_cell_ics_linear_transport_source_raw_nn_cell ff_right_scale_mcp_cell_ics_linear_transport_source_raw_nn_cell. ((forall ff_index_mcp_ics_linear_transport_source_raw_nn_cell_row ff_source_mcp_ics_linear_transport_source_raw_nn_cell_row ff_target_mcp_ics_linear_transport_source_raw_nn_cell_row. (exists mcp_gap_ics_linear_transport_source_raw_nn_cell_row_bound. mcp_gap_ics_linear_transport_source_raw_nn_cell_row_bound + S (ff_index_mcp_ics_linear_transport_source_raw_nn_cell_row) = (w)) -> (((exists fs_h_mcp_ics_linear_transport_source_raw_nn_cell_row_source. fs_h_mcp_ics_linear_transport_source_raw_nn_cell_row_source + S (ff_source_mcp_ics_linear_transport_source_raw_nn_cell_row) = S ((S (((ff_row_mcp_prefix_ics_linear_transport_source_raw_nn) * (w)) + (1) * ff_index_mcp_ics_linear_transport_source_raw_nn_cell_row)) * dc)) /\ exists fs_q_mcp_ics_linear_transport_source_raw_nn_cell_row_source. db = fs_q_mcp_ics_linear_transport_source_raw_nn_cell_row_source * S ((S (((ff_row_mcp_prefix_ics_linear_transport_source_raw_nn) * (w)) + (1) * ff_index_mcp_ics_linear_transport_source_raw_nn_cell_row)) * dc) + (ff_source_mcp_ics_linear_transport_source_raw_nn_cell_row))) -> (((exists fs_h_mcp_ics_linear_transport_source_raw_nn_cell_row_target. fs_h_mcp_ics_linear_transport_source_raw_nn_cell_row_target + S (ff_target_mcp_ics_linear_transport_source_raw_nn_cell_row) = S ((S (ff_index_mcp_ics_linear_transport_source_raw_nn_cell_row)) * ff_left_scale_mcp_cell_ics_linear_transport_source_raw_nn_cell)) /\ exists fs_q_mcp_ics_linear_transport_source_raw_nn_cell_row_target. ff_left_mcp_cell_ics_linear_transport_source_raw_nn_cell = fs_q_mcp_ics_linear_transport_source_raw_nn_cell_row_target * S ((S (ff_index_mcp_ics_linear_transport_source_raw_nn_cell_row)) * ff_left_scale_mcp_cell_ics_linear_transport_source_raw_nn_cell) + (ff_target_mcp_ics_linear_transport_source_raw_nn_cell_row))) -> ff_target_mcp_ics_linear_transport_source_raw_nn_cell_row = ff_source_mcp_ics_linear_transport_source_raw_nn_cell_row) /\ ((forall ff_index_mcp_ics_linear_transport_source_raw_nn_cell_column ff_source_mcp_ics_linear_transport_source_raw_nn_cell_column ff_target_mcp_ics_linear_transport_source_raw_nn_cell_column. (exists mcp_gap_ics_linear_transport_source_raw_nn_cell_column_bound. mcp_gap_ics_linear_transport_source_raw_nn_cell_column_bound + S (ff_index_mcp_ics_linear_transport_source_raw_nn_cell_column) = (w)) -> (((exists fs_h_mcp_ics_linear_transport_source_raw_nn_cell_column_source. fs_h_mcp_ics_linear_transport_source_raw_nn_cell_column_source + S (ff_source_mcp_ics_linear_transport_source_raw_nn_cell_column) = S ((S ((ff_column_mcp_prefix_ics_linear_transport_source_raw_nn) + (1) * ff_index_mcp_ics_linear_transport_source_raw_nn_cell_column)) * fc)) /\ exists fs_q_mcp_ics_linear_transport_source_raw_nn_cell_column_source. fb = fs_q_mcp_ics_linear_transport_source_raw_nn_cell_column_source * S ((S ((ff_column_mcp_prefix_ics_linear_transport_source_raw_nn) + (1) * ff_index_mcp_ics_linear_transport_source_raw_nn_cell_column)) * fc) + (ff_source_mcp_ics_linear_transport_source_raw_nn_cell_column))) -> (((exists fs_h_mcp_ics_linear_transport_source_raw_nn_cell_column_target. fs_h_mcp_ics_linear_transport_source_raw_nn_cell_column_target + S (ff_target_mcp_ics_linear_transport_source_raw_nn_cell_column) = S ((S (ff_index_mcp_ics_linear_transport_source_raw_nn_cell_column)) * ff_right_scale_mcp_cell_ics_linear_transport_source_raw_nn_cell)) /\ exists fs_q_mcp_ics_linear_transport_source_raw_nn_cell_column_target. ff_right_mcp_cell_ics_linear_transport_source_raw_nn_cell = fs_q_mcp_ics_linear_transport_source_raw_nn_cell_column_target * S ((S (ff_index_mcp_ics_linear_transport_source_raw_nn_cell_column)) * ff_right_scale_mcp_cell_ics_linear_transport_source_raw_nn_cell) + (ff_target_mcp_ics_linear_transport_source_raw_nn_cell_column))) -> ff_target_mcp_ics_linear_transport_source_raw_nn_cell_column = ff_source_mcp_ics_linear_transport_source_raw_nn_cell_column) /\ (exists ff_code_dot_mcp_ics_linear_transport_source_raw_nn_cell_dot ff_scale_dot_mcp_ics_linear_transport_source_raw_nn_cell_dot. ((forall fpmp_index_dot_mcp_ics_linear_transport_source_raw_nn_cell_dot_pointwise fpmp_left_dot_mcp_ics_linear_transport_source_raw_nn_cell_dot_pointwise fpmp_right_dot_mcp_ics_linear_transport_source_raw_nn_cell_dot_pointwise fpmp_target_dot_mcp_ics_linear_transport_source_raw_nn_cell_dot_pointwise. (exists fpmp_gap_dot_mcp_ics_linear_transport_source_raw_nn_cell_dot_pointwise. fpmp_gap_dot_mcp_ics_linear_transport_source_raw_nn_cell_dot_pointwise + S fpmp_index_dot_mcp_ics_linear_transport_source_raw_nn_cell_dot_pointwise = w) -> (((exists ff_h_fpmp_dot_mcp_ics_linear_transport_source_raw_nn_cell_dot_pointwise_left. ff_h_fpmp_dot_mcp_ics_linear_transport_source_raw_nn_cell_dot_pointwise_left + S (fpmp_left_dot_mcp_ics_linear_transport_source_raw_nn_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_linear_transport_source_raw_nn_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_linear_transport_source_raw_nn_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_linear_transport_source_raw_nn_cell_dot_pointwise_left. ff_left_mcp_cell_ics_linear_transport_source_raw_nn_cell = ff_q_fpmp_dot_mcp_ics_linear_transport_source_raw_nn_cell_dot_pointwise_left * S ((S (fpmp_index_dot_mcp_ics_linear_transport_source_raw_nn_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_linear_transport_source_raw_nn_cell) + (fpmp_left_dot_mcp_ics_linear_transport_source_raw_nn_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_linear_transport_source_raw_nn_cell_dot_pointwise_right. ff_h_fpmp_dot_mcp_ics_linear_transport_source_raw_nn_cell_dot_pointwise_right + S (fpmp_right_dot_mcp_ics_linear_transport_source_raw_nn_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_linear_transport_source_raw_nn_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_linear_transport_source_raw_nn_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_linear_transport_source_raw_nn_cell_dot_pointwise_right. ff_right_mcp_cell_ics_linear_transport_source_raw_nn_cell = ff_q_fpmp_dot_mcp_ics_linear_transport_source_raw_nn_cell_dot_pointwise_right * S ((S (fpmp_index_dot_mcp_ics_linear_transport_source_raw_nn_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_linear_transport_source_raw_nn_cell) + (fpmp_right_dot_mcp_ics_linear_transport_source_raw_nn_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_linear_transport_source_raw_nn_cell_dot_pointwise_target. ff_h_fpmp_dot_mcp_ics_linear_transport_source_raw_nn_cell_dot_pointwise_target + S (fpmp_target_dot_mcp_ics_linear_transport_source_raw_nn_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_linear_transport_source_raw_nn_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_linear_transport_source_raw_nn_cell_dot)) /\ exists ff_q_fpmp_dot_mcp_ics_linear_transport_source_raw_nn_cell_dot_pointwise_target. ff_code_dot_mcp_ics_linear_transport_source_raw_nn_cell_dot = ff_q_fpmp_dot_mcp_ics_linear_transport_source_raw_nn_cell_dot_pointwise_target * S ((S (fpmp_index_dot_mcp_ics_linear_transport_source_raw_nn_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_linear_transport_source_raw_nn_cell_dot) + (fpmp_target_dot_mcp_ics_linear_transport_source_raw_nn_cell_dot_pointwise))) -> fpmp_target_dot_mcp_ics_linear_transport_source_raw_nn_cell_dot_pointwise = fpmp_left_dot_mcp_ics_linear_transport_source_raw_nn_cell_dot_pointwise * fpmp_right_dot_mcp_ics_linear_transport_source_raw_nn_cell_dot_pointwise) /\ (exists ff_u_dot_mcp_ics_linear_transport_source_raw_nn_cell_dot_sum ff_v_dot_mcp_ics_linear_transport_source_raw_nn_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_linear_transport_source_raw_nn_cell_dot_sum_start. ff_h_dot_mcp_ics_linear_transport_source_raw_nn_cell_dot_sum_start + S (0) = S ((S (0)) * ff_v_dot_mcp_ics_linear_transport_source_raw_nn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_linear_transport_source_raw_nn_cell_dot_sum_start. ff_u_dot_mcp_ics_linear_transport_source_raw_nn_cell_dot_sum = ff_q_dot_mcp_ics_linear_transport_source_raw_nn_cell_dot_sum_start * S ((S (0)) * ff_v_dot_mcp_ics_linear_transport_source_raw_nn_cell_dot_sum) + (0))) /\ ((((exists ff_h_dot_mcp_ics_linear_transport_source_raw_nn_cell_dot_sum_terminal. ff_h_dot_mcp_ics_linear_transport_source_raw_nn_cell_dot_sum_terminal + S (ff_value_mcp_prefix_ics_linear_transport_source_raw_nn) = S ((S (w)) * ff_v_dot_mcp_ics_linear_transport_source_raw_nn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_linear_transport_source_raw_nn_cell_dot_sum_terminal. ff_u_dot_mcp_ics_linear_transport_source_raw_nn_cell_dot_sum = ff_q_dot_mcp_ics_linear_transport_source_raw_nn_cell_dot_sum_terminal * S ((S (w)) * ff_v_dot_mcp_ics_linear_transport_source_raw_nn_cell_dot_sum) + (ff_value_mcp_prefix_ics_linear_transport_source_raw_nn))) /\ forall ff_i_dot_mcp_ics_linear_transport_source_raw_nn_cell_dot_sum. (exists ff_lt_dot_mcp_ics_linear_transport_source_raw_nn_cell_dot_sum_bound. ff_lt_dot_mcp_ics_linear_transport_source_raw_nn_cell_dot_sum_bound + S ff_i_dot_mcp_ics_linear_transport_source_raw_nn_cell_dot_sum = w) -> exists ff_a_dot_mcp_ics_linear_transport_source_raw_nn_cell_dot_sum ff_r_dot_mcp_ics_linear_transport_source_raw_nn_cell_dot_sum ff_s_dot_mcp_ics_linear_transport_source_raw_nn_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_linear_transport_source_raw_nn_cell_dot_sum_summand. ff_h_dot_mcp_ics_linear_transport_source_raw_nn_cell_dot_sum_summand + S (ff_a_dot_mcp_ics_linear_transport_source_raw_nn_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_linear_transport_source_raw_nn_cell_dot_sum)) * ff_scale_dot_mcp_ics_linear_transport_source_raw_nn_cell_dot)) /\ exists ff_q_dot_mcp_ics_linear_transport_source_raw_nn_cell_dot_sum_summand. ff_code_dot_mcp_ics_linear_transport_source_raw_nn_cell_dot = ff_q_dot_mcp_ics_linear_transport_source_raw_nn_cell_dot_sum_summand * S ((S (ff_i_dot_mcp_ics_linear_transport_source_raw_nn_cell_dot_sum)) * ff_scale_dot_mcp_ics_linear_transport_source_raw_nn_cell_dot) + (ff_a_dot_mcp_ics_linear_transport_source_raw_nn_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_linear_transport_source_raw_nn_cell_dot_sum_partial. ff_h_dot_mcp_ics_linear_transport_source_raw_nn_cell_dot_sum_partial + S (ff_r_dot_mcp_ics_linear_transport_source_raw_nn_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_linear_transport_source_raw_nn_cell_dot_sum)) * ff_v_dot_mcp_ics_linear_transport_source_raw_nn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_linear_transport_source_raw_nn_cell_dot_sum_partial. ff_u_dot_mcp_ics_linear_transport_source_raw_nn_cell_dot_sum = ff_q_dot_mcp_ics_linear_transport_source_raw_nn_cell_dot_sum_partial * S ((S (ff_i_dot_mcp_ics_linear_transport_source_raw_nn_cell_dot_sum)) * ff_v_dot_mcp_ics_linear_transport_source_raw_nn_cell_dot_sum) + (ff_r_dot_mcp_ics_linear_transport_source_raw_nn_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_linear_transport_source_raw_nn_cell_dot_sum_successor. ff_h_dot_mcp_ics_linear_transport_source_raw_nn_cell_dot_sum_successor + S (ff_s_dot_mcp_ics_linear_transport_source_raw_nn_cell_dot_sum) = S ((S (S ff_i_dot_mcp_ics_linear_transport_source_raw_nn_cell_dot_sum)) * ff_v_dot_mcp_ics_linear_transport_source_raw_nn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_linear_transport_source_raw_nn_cell_dot_sum_successor. ff_u_dot_mcp_ics_linear_transport_source_raw_nn_cell_dot_sum = ff_q_dot_mcp_ics_linear_transport_source_raw_nn_cell_dot_sum_successor * S ((S (S ff_i_dot_mcp_ics_linear_transport_source_raw_nn_cell_dot_sum)) * ff_v_dot_mcp_ics_linear_transport_source_raw_nn_cell_dot_sum) + (ff_s_dot_mcp_ics_linear_transport_source_raw_nn_cell_dot_sum))) /\ ff_s_dot_mcp_ics_linear_transport_source_raw_nn_cell_dot_sum = ff_r_dot_mcp_ics_linear_transport_source_raw_nn_cell_dot_sum + ff_a_dot_mcp_ics_linear_transport_source_raw_nn_cell_dot_sum))))))))))) /\ (((exists fs_h_mcp_ics_linear_transport_source_raw_nn_entry. fs_h_mcp_ics_linear_transport_source_raw_nn_entry + S (ff_value_mcp_prefix_ics_linear_transport_source_raw_nn) = S ((S (ff_index_mcp_prefix_ics_linear_transport_source_raw_nn)) * ff_nns_mcp_smatrix_ics_linear_transport_source_raw)) /\ exists fs_q_mcp_ics_linear_transport_source_raw_nn_entry. ff_nn_mcp_smatrix_ics_linear_transport_source_raw = fs_q_mcp_ics_linear_transport_source_raw_nn_entry * S ((S (ff_index_mcp_prefix_ics_linear_transport_source_raw_nn)) * ff_nns_mcp_smatrix_ics_linear_transport_source_raw) + (ff_value_mcp_prefix_ics_linear_transport_source_raw_nn))))))) /\ ((forall ff_index_mcp_prefix_ics_linear_transport_source_raw_pn. (exists mcp_gap_ics_linear_transport_source_raw_pn_index. mcp_gap_ics_linear_transport_source_raw_pn_index + S (ff_index_mcp_prefix_ics_linear_transport_source_raw_pn) = ((r) * (1))) -> exists ff_row_mcp_prefix_ics_linear_transport_source_raw_pn ff_column_mcp_prefix_ics_linear_transport_source_raw_pn ff_value_mcp_prefix_ics_linear_transport_source_raw_pn. ((ff_index_mcp_prefix_ics_linear_transport_source_raw_pn) = (1) * ff_row_mcp_prefix_ics_linear_transport_source_raw_pn + ff_column_mcp_prefix_ics_linear_transport_source_raw_pn /\ ((exists mcp_gap_ics_linear_transport_source_raw_pn_column. mcp_gap_ics_linear_transport_source_raw_pn_column + S (ff_column_mcp_prefix_ics_linear_transport_source_raw_pn) = (1)) /\ ((exists ff_left_mcp_cell_ics_linear_transport_source_raw_pn_cell ff_left_scale_mcp_cell_ics_linear_transport_source_raw_pn_cell ff_right_mcp_cell_ics_linear_transport_source_raw_pn_cell ff_right_scale_mcp_cell_ics_linear_transport_source_raw_pn_cell. ((forall ff_index_mcp_ics_linear_transport_source_raw_pn_cell_row ff_source_mcp_ics_linear_transport_source_raw_pn_cell_row ff_target_mcp_ics_linear_transport_source_raw_pn_cell_row. (exists mcp_gap_ics_linear_transport_source_raw_pn_cell_row_bound. mcp_gap_ics_linear_transport_source_raw_pn_cell_row_bound + S (ff_index_mcp_ics_linear_transport_source_raw_pn_cell_row) = (w)) -> (((exists fs_h_mcp_ics_linear_transport_source_raw_pn_cell_row_source. fs_h_mcp_ics_linear_transport_source_raw_pn_cell_row_source + S (ff_source_mcp_ics_linear_transport_source_raw_pn_cell_row) = S ((S (((ff_row_mcp_prefix_ics_linear_transport_source_raw_pn) * (w)) + (1) * ff_index_mcp_ics_linear_transport_source_raw_pn_cell_row)) * ac)) /\ exists fs_q_mcp_ics_linear_transport_source_raw_pn_cell_row_source. ab = fs_q_mcp_ics_linear_transport_source_raw_pn_cell_row_source * S ((S (((ff_row_mcp_prefix_ics_linear_transport_source_raw_pn) * (w)) + (1) * ff_index_mcp_ics_linear_transport_source_raw_pn_cell_row)) * ac) + (ff_source_mcp_ics_linear_transport_source_raw_pn_cell_row))) -> (((exists fs_h_mcp_ics_linear_transport_source_raw_pn_cell_row_target. fs_h_mcp_ics_linear_transport_source_raw_pn_cell_row_target + S (ff_target_mcp_ics_linear_transport_source_raw_pn_cell_row) = S ((S (ff_index_mcp_ics_linear_transport_source_raw_pn_cell_row)) * ff_left_scale_mcp_cell_ics_linear_transport_source_raw_pn_cell)) /\ exists fs_q_mcp_ics_linear_transport_source_raw_pn_cell_row_target. ff_left_mcp_cell_ics_linear_transport_source_raw_pn_cell = fs_q_mcp_ics_linear_transport_source_raw_pn_cell_row_target * S ((S (ff_index_mcp_ics_linear_transport_source_raw_pn_cell_row)) * ff_left_scale_mcp_cell_ics_linear_transport_source_raw_pn_cell) + (ff_target_mcp_ics_linear_transport_source_raw_pn_cell_row))) -> ff_target_mcp_ics_linear_transport_source_raw_pn_cell_row = ff_source_mcp_ics_linear_transport_source_raw_pn_cell_row) /\ ((forall ff_index_mcp_ics_linear_transport_source_raw_pn_cell_column ff_source_mcp_ics_linear_transport_source_raw_pn_cell_column ff_target_mcp_ics_linear_transport_source_raw_pn_cell_column. (exists mcp_gap_ics_linear_transport_source_raw_pn_cell_column_bound. mcp_gap_ics_linear_transport_source_raw_pn_cell_column_bound + S (ff_index_mcp_ics_linear_transport_source_raw_pn_cell_column) = (w)) -> (((exists fs_h_mcp_ics_linear_transport_source_raw_pn_cell_column_source. fs_h_mcp_ics_linear_transport_source_raw_pn_cell_column_source + S (ff_source_mcp_ics_linear_transport_source_raw_pn_cell_column) = S ((S ((ff_column_mcp_prefix_ics_linear_transport_source_raw_pn) + (1) * ff_index_mcp_ics_linear_transport_source_raw_pn_cell_column)) * fc)) /\ exists fs_q_mcp_ics_linear_transport_source_raw_pn_cell_column_source. fb = fs_q_mcp_ics_linear_transport_source_raw_pn_cell_column_source * S ((S ((ff_column_mcp_prefix_ics_linear_transport_source_raw_pn) + (1) * ff_index_mcp_ics_linear_transport_source_raw_pn_cell_column)) * fc) + (ff_source_mcp_ics_linear_transport_source_raw_pn_cell_column))) -> (((exists fs_h_mcp_ics_linear_transport_source_raw_pn_cell_column_target. fs_h_mcp_ics_linear_transport_source_raw_pn_cell_column_target + S (ff_target_mcp_ics_linear_transport_source_raw_pn_cell_column) = S ((S (ff_index_mcp_ics_linear_transport_source_raw_pn_cell_column)) * ff_right_scale_mcp_cell_ics_linear_transport_source_raw_pn_cell)) /\ exists fs_q_mcp_ics_linear_transport_source_raw_pn_cell_column_target. ff_right_mcp_cell_ics_linear_transport_source_raw_pn_cell = fs_q_mcp_ics_linear_transport_source_raw_pn_cell_column_target * S ((S (ff_index_mcp_ics_linear_transport_source_raw_pn_cell_column)) * ff_right_scale_mcp_cell_ics_linear_transport_source_raw_pn_cell) + (ff_target_mcp_ics_linear_transport_source_raw_pn_cell_column))) -> ff_target_mcp_ics_linear_transport_source_raw_pn_cell_column = ff_source_mcp_ics_linear_transport_source_raw_pn_cell_column) /\ (exists ff_code_dot_mcp_ics_linear_transport_source_raw_pn_cell_dot ff_scale_dot_mcp_ics_linear_transport_source_raw_pn_cell_dot. ((forall fpmp_index_dot_mcp_ics_linear_transport_source_raw_pn_cell_dot_pointwise fpmp_left_dot_mcp_ics_linear_transport_source_raw_pn_cell_dot_pointwise fpmp_right_dot_mcp_ics_linear_transport_source_raw_pn_cell_dot_pointwise fpmp_target_dot_mcp_ics_linear_transport_source_raw_pn_cell_dot_pointwise. (exists fpmp_gap_dot_mcp_ics_linear_transport_source_raw_pn_cell_dot_pointwise. fpmp_gap_dot_mcp_ics_linear_transport_source_raw_pn_cell_dot_pointwise + S fpmp_index_dot_mcp_ics_linear_transport_source_raw_pn_cell_dot_pointwise = w) -> (((exists ff_h_fpmp_dot_mcp_ics_linear_transport_source_raw_pn_cell_dot_pointwise_left. ff_h_fpmp_dot_mcp_ics_linear_transport_source_raw_pn_cell_dot_pointwise_left + S (fpmp_left_dot_mcp_ics_linear_transport_source_raw_pn_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_linear_transport_source_raw_pn_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_linear_transport_source_raw_pn_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_linear_transport_source_raw_pn_cell_dot_pointwise_left. ff_left_mcp_cell_ics_linear_transport_source_raw_pn_cell = ff_q_fpmp_dot_mcp_ics_linear_transport_source_raw_pn_cell_dot_pointwise_left * S ((S (fpmp_index_dot_mcp_ics_linear_transport_source_raw_pn_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_linear_transport_source_raw_pn_cell) + (fpmp_left_dot_mcp_ics_linear_transport_source_raw_pn_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_linear_transport_source_raw_pn_cell_dot_pointwise_right. ff_h_fpmp_dot_mcp_ics_linear_transport_source_raw_pn_cell_dot_pointwise_right + S (fpmp_right_dot_mcp_ics_linear_transport_source_raw_pn_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_linear_transport_source_raw_pn_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_linear_transport_source_raw_pn_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_linear_transport_source_raw_pn_cell_dot_pointwise_right. ff_right_mcp_cell_ics_linear_transport_source_raw_pn_cell = ff_q_fpmp_dot_mcp_ics_linear_transport_source_raw_pn_cell_dot_pointwise_right * S ((S (fpmp_index_dot_mcp_ics_linear_transport_source_raw_pn_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_linear_transport_source_raw_pn_cell) + (fpmp_right_dot_mcp_ics_linear_transport_source_raw_pn_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_linear_transport_source_raw_pn_cell_dot_pointwise_target. ff_h_fpmp_dot_mcp_ics_linear_transport_source_raw_pn_cell_dot_pointwise_target + S (fpmp_target_dot_mcp_ics_linear_transport_source_raw_pn_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_linear_transport_source_raw_pn_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_linear_transport_source_raw_pn_cell_dot)) /\ exists ff_q_fpmp_dot_mcp_ics_linear_transport_source_raw_pn_cell_dot_pointwise_target. ff_code_dot_mcp_ics_linear_transport_source_raw_pn_cell_dot = ff_q_fpmp_dot_mcp_ics_linear_transport_source_raw_pn_cell_dot_pointwise_target * S ((S (fpmp_index_dot_mcp_ics_linear_transport_source_raw_pn_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_linear_transport_source_raw_pn_cell_dot) + (fpmp_target_dot_mcp_ics_linear_transport_source_raw_pn_cell_dot_pointwise))) -> fpmp_target_dot_mcp_ics_linear_transport_source_raw_pn_cell_dot_pointwise = fpmp_left_dot_mcp_ics_linear_transport_source_raw_pn_cell_dot_pointwise * fpmp_right_dot_mcp_ics_linear_transport_source_raw_pn_cell_dot_pointwise) /\ (exists ff_u_dot_mcp_ics_linear_transport_source_raw_pn_cell_dot_sum ff_v_dot_mcp_ics_linear_transport_source_raw_pn_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_linear_transport_source_raw_pn_cell_dot_sum_start. ff_h_dot_mcp_ics_linear_transport_source_raw_pn_cell_dot_sum_start + S (0) = S ((S (0)) * ff_v_dot_mcp_ics_linear_transport_source_raw_pn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_linear_transport_source_raw_pn_cell_dot_sum_start. ff_u_dot_mcp_ics_linear_transport_source_raw_pn_cell_dot_sum = ff_q_dot_mcp_ics_linear_transport_source_raw_pn_cell_dot_sum_start * S ((S (0)) * ff_v_dot_mcp_ics_linear_transport_source_raw_pn_cell_dot_sum) + (0))) /\ ((((exists ff_h_dot_mcp_ics_linear_transport_source_raw_pn_cell_dot_sum_terminal. ff_h_dot_mcp_ics_linear_transport_source_raw_pn_cell_dot_sum_terminal + S (ff_value_mcp_prefix_ics_linear_transport_source_raw_pn) = S ((S (w)) * ff_v_dot_mcp_ics_linear_transport_source_raw_pn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_linear_transport_source_raw_pn_cell_dot_sum_terminal. ff_u_dot_mcp_ics_linear_transport_source_raw_pn_cell_dot_sum = ff_q_dot_mcp_ics_linear_transport_source_raw_pn_cell_dot_sum_terminal * S ((S (w)) * ff_v_dot_mcp_ics_linear_transport_source_raw_pn_cell_dot_sum) + (ff_value_mcp_prefix_ics_linear_transport_source_raw_pn))) /\ forall ff_i_dot_mcp_ics_linear_transport_source_raw_pn_cell_dot_sum. (exists ff_lt_dot_mcp_ics_linear_transport_source_raw_pn_cell_dot_sum_bound. ff_lt_dot_mcp_ics_linear_transport_source_raw_pn_cell_dot_sum_bound + S ff_i_dot_mcp_ics_linear_transport_source_raw_pn_cell_dot_sum = w) -> exists ff_a_dot_mcp_ics_linear_transport_source_raw_pn_cell_dot_sum ff_r_dot_mcp_ics_linear_transport_source_raw_pn_cell_dot_sum ff_s_dot_mcp_ics_linear_transport_source_raw_pn_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_linear_transport_source_raw_pn_cell_dot_sum_summand. ff_h_dot_mcp_ics_linear_transport_source_raw_pn_cell_dot_sum_summand + S (ff_a_dot_mcp_ics_linear_transport_source_raw_pn_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_linear_transport_source_raw_pn_cell_dot_sum)) * ff_scale_dot_mcp_ics_linear_transport_source_raw_pn_cell_dot)) /\ exists ff_q_dot_mcp_ics_linear_transport_source_raw_pn_cell_dot_sum_summand. ff_code_dot_mcp_ics_linear_transport_source_raw_pn_cell_dot = ff_q_dot_mcp_ics_linear_transport_source_raw_pn_cell_dot_sum_summand * S ((S (ff_i_dot_mcp_ics_linear_transport_source_raw_pn_cell_dot_sum)) * ff_scale_dot_mcp_ics_linear_transport_source_raw_pn_cell_dot) + (ff_a_dot_mcp_ics_linear_transport_source_raw_pn_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_linear_transport_source_raw_pn_cell_dot_sum_partial. ff_h_dot_mcp_ics_linear_transport_source_raw_pn_cell_dot_sum_partial + S (ff_r_dot_mcp_ics_linear_transport_source_raw_pn_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_linear_transport_source_raw_pn_cell_dot_sum)) * ff_v_dot_mcp_ics_linear_transport_source_raw_pn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_linear_transport_source_raw_pn_cell_dot_sum_partial. ff_u_dot_mcp_ics_linear_transport_source_raw_pn_cell_dot_sum = ff_q_dot_mcp_ics_linear_transport_source_raw_pn_cell_dot_sum_partial * S ((S (ff_i_dot_mcp_ics_linear_transport_source_raw_pn_cell_dot_sum)) * ff_v_dot_mcp_ics_linear_transport_source_raw_pn_cell_dot_sum) + (ff_r_dot_mcp_ics_linear_transport_source_raw_pn_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_linear_transport_source_raw_pn_cell_dot_sum_successor. ff_h_dot_mcp_ics_linear_transport_source_raw_pn_cell_dot_sum_successor + S (ff_s_dot_mcp_ics_linear_transport_source_raw_pn_cell_dot_sum) = S ((S (S ff_i_dot_mcp_ics_linear_transport_source_raw_pn_cell_dot_sum)) * ff_v_dot_mcp_ics_linear_transport_source_raw_pn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_linear_transport_source_raw_pn_cell_dot_sum_successor. ff_u_dot_mcp_ics_linear_transport_source_raw_pn_cell_dot_sum = ff_q_dot_mcp_ics_linear_transport_source_raw_pn_cell_dot_sum_successor * S ((S (S ff_i_dot_mcp_ics_linear_transport_source_raw_pn_cell_dot_sum)) * ff_v_dot_mcp_ics_linear_transport_source_raw_pn_cell_dot_sum) + (ff_s_dot_mcp_ics_linear_transport_source_raw_pn_cell_dot_sum))) /\ ff_s_dot_mcp_ics_linear_transport_source_raw_pn_cell_dot_sum = ff_r_dot_mcp_ics_linear_transport_source_raw_pn_cell_dot_sum + ff_a_dot_mcp_ics_linear_transport_source_raw_pn_cell_dot_sum))))))))))) /\ (((exists fs_h_mcp_ics_linear_transport_source_raw_pn_entry. fs_h_mcp_ics_linear_transport_source_raw_pn_entry + S (ff_value_mcp_prefix_ics_linear_transport_source_raw_pn) = S ((S (ff_index_mcp_prefix_ics_linear_transport_source_raw_pn)) * ff_pns_mcp_smatrix_ics_linear_transport_source_raw)) /\ exists fs_q_mcp_ics_linear_transport_source_raw_pn_entry. ff_pn_mcp_smatrix_ics_linear_transport_source_raw = fs_q_mcp_ics_linear_transport_source_raw_pn_entry * S ((S (ff_index_mcp_prefix_ics_linear_transport_source_raw_pn)) * ff_pns_mcp_smatrix_ics_linear_transport_source_raw) + (ff_value_mcp_prefix_ics_linear_transport_source_raw_pn))))))) /\ ((forall ff_index_mcp_prefix_ics_linear_transport_source_raw_np. (exists mcp_gap_ics_linear_transport_source_raw_np_index. mcp_gap_ics_linear_transport_source_raw_np_index + S (ff_index_mcp_prefix_ics_linear_transport_source_raw_np) = ((r) * (1))) -> exists ff_row_mcp_prefix_ics_linear_transport_source_raw_np ff_column_mcp_prefix_ics_linear_transport_source_raw_np ff_value_mcp_prefix_ics_linear_transport_source_raw_np. ((ff_index_mcp_prefix_ics_linear_transport_source_raw_np) = (1) * ff_row_mcp_prefix_ics_linear_transport_source_raw_np + ff_column_mcp_prefix_ics_linear_transport_source_raw_np /\ ((exists mcp_gap_ics_linear_transport_source_raw_np_column. mcp_gap_ics_linear_transport_source_raw_np_column + S (ff_column_mcp_prefix_ics_linear_transport_source_raw_np) = (1)) /\ ((exists ff_left_mcp_cell_ics_linear_transport_source_raw_np_cell ff_left_scale_mcp_cell_ics_linear_transport_source_raw_np_cell ff_right_mcp_cell_ics_linear_transport_source_raw_np_cell ff_right_scale_mcp_cell_ics_linear_transport_source_raw_np_cell. ((forall ff_index_mcp_ics_linear_transport_source_raw_np_cell_row ff_source_mcp_ics_linear_transport_source_raw_np_cell_row ff_target_mcp_ics_linear_transport_source_raw_np_cell_row. (exists mcp_gap_ics_linear_transport_source_raw_np_cell_row_bound. mcp_gap_ics_linear_transport_source_raw_np_cell_row_bound + S (ff_index_mcp_ics_linear_transport_source_raw_np_cell_row) = (w)) -> (((exists fs_h_mcp_ics_linear_transport_source_raw_np_cell_row_source. fs_h_mcp_ics_linear_transport_source_raw_np_cell_row_source + S (ff_source_mcp_ics_linear_transport_source_raw_np_cell_row) = S ((S (((ff_row_mcp_prefix_ics_linear_transport_source_raw_np) * (w)) + (1) * ff_index_mcp_ics_linear_transport_source_raw_np_cell_row)) * dc)) /\ exists fs_q_mcp_ics_linear_transport_source_raw_np_cell_row_source. db = fs_q_mcp_ics_linear_transport_source_raw_np_cell_row_source * S ((S (((ff_row_mcp_prefix_ics_linear_transport_source_raw_np) * (w)) + (1) * ff_index_mcp_ics_linear_transport_source_raw_np_cell_row)) * dc) + (ff_source_mcp_ics_linear_transport_source_raw_np_cell_row))) -> (((exists fs_h_mcp_ics_linear_transport_source_raw_np_cell_row_target. fs_h_mcp_ics_linear_transport_source_raw_np_cell_row_target + S (ff_target_mcp_ics_linear_transport_source_raw_np_cell_row) = S ((S (ff_index_mcp_ics_linear_transport_source_raw_np_cell_row)) * ff_left_scale_mcp_cell_ics_linear_transport_source_raw_np_cell)) /\ exists fs_q_mcp_ics_linear_transport_source_raw_np_cell_row_target. ff_left_mcp_cell_ics_linear_transport_source_raw_np_cell = fs_q_mcp_ics_linear_transport_source_raw_np_cell_row_target * S ((S (ff_index_mcp_ics_linear_transport_source_raw_np_cell_row)) * ff_left_scale_mcp_cell_ics_linear_transport_source_raw_np_cell) + (ff_target_mcp_ics_linear_transport_source_raw_np_cell_row))) -> ff_target_mcp_ics_linear_transport_source_raw_np_cell_row = ff_source_mcp_ics_linear_transport_source_raw_np_cell_row) /\ ((forall ff_index_mcp_ics_linear_transport_source_raw_np_cell_column ff_source_mcp_ics_linear_transport_source_raw_np_cell_column ff_target_mcp_ics_linear_transport_source_raw_np_cell_column. (exists mcp_gap_ics_linear_transport_source_raw_np_cell_column_bound. mcp_gap_ics_linear_transport_source_raw_np_cell_column_bound + S (ff_index_mcp_ics_linear_transport_source_raw_np_cell_column) = (w)) -> (((exists fs_h_mcp_ics_linear_transport_source_raw_np_cell_column_source. fs_h_mcp_ics_linear_transport_source_raw_np_cell_column_source + S (ff_source_mcp_ics_linear_transport_source_raw_np_cell_column) = S ((S ((ff_column_mcp_prefix_ics_linear_transport_source_raw_np) + (1) * ff_index_mcp_ics_linear_transport_source_raw_np_cell_column)) * ec)) /\ exists fs_q_mcp_ics_linear_transport_source_raw_np_cell_column_source. eb = fs_q_mcp_ics_linear_transport_source_raw_np_cell_column_source * S ((S ((ff_column_mcp_prefix_ics_linear_transport_source_raw_np) + (1) * ff_index_mcp_ics_linear_transport_source_raw_np_cell_column)) * ec) + (ff_source_mcp_ics_linear_transport_source_raw_np_cell_column))) -> (((exists fs_h_mcp_ics_linear_transport_source_raw_np_cell_column_target. fs_h_mcp_ics_linear_transport_source_raw_np_cell_column_target + S (ff_target_mcp_ics_linear_transport_source_raw_np_cell_column) = S ((S (ff_index_mcp_ics_linear_transport_source_raw_np_cell_column)) * ff_right_scale_mcp_cell_ics_linear_transport_source_raw_np_cell)) /\ exists fs_q_mcp_ics_linear_transport_source_raw_np_cell_column_target. ff_right_mcp_cell_ics_linear_transport_source_raw_np_cell = fs_q_mcp_ics_linear_transport_source_raw_np_cell_column_target * S ((S (ff_index_mcp_ics_linear_transport_source_raw_np_cell_column)) * ff_right_scale_mcp_cell_ics_linear_transport_source_raw_np_cell) + (ff_target_mcp_ics_linear_transport_source_raw_np_cell_column))) -> ff_target_mcp_ics_linear_transport_source_raw_np_cell_column = ff_source_mcp_ics_linear_transport_source_raw_np_cell_column) /\ (exists ff_code_dot_mcp_ics_linear_transport_source_raw_np_cell_dot ff_scale_dot_mcp_ics_linear_transport_source_raw_np_cell_dot. ((forall fpmp_index_dot_mcp_ics_linear_transport_source_raw_np_cell_dot_pointwise fpmp_left_dot_mcp_ics_linear_transport_source_raw_np_cell_dot_pointwise fpmp_right_dot_mcp_ics_linear_transport_source_raw_np_cell_dot_pointwise fpmp_target_dot_mcp_ics_linear_transport_source_raw_np_cell_dot_pointwise. (exists fpmp_gap_dot_mcp_ics_linear_transport_source_raw_np_cell_dot_pointwise. fpmp_gap_dot_mcp_ics_linear_transport_source_raw_np_cell_dot_pointwise + S fpmp_index_dot_mcp_ics_linear_transport_source_raw_np_cell_dot_pointwise = w) -> (((exists ff_h_fpmp_dot_mcp_ics_linear_transport_source_raw_np_cell_dot_pointwise_left. ff_h_fpmp_dot_mcp_ics_linear_transport_source_raw_np_cell_dot_pointwise_left + S (fpmp_left_dot_mcp_ics_linear_transport_source_raw_np_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_linear_transport_source_raw_np_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_linear_transport_source_raw_np_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_linear_transport_source_raw_np_cell_dot_pointwise_left. ff_left_mcp_cell_ics_linear_transport_source_raw_np_cell = ff_q_fpmp_dot_mcp_ics_linear_transport_source_raw_np_cell_dot_pointwise_left * S ((S (fpmp_index_dot_mcp_ics_linear_transport_source_raw_np_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_linear_transport_source_raw_np_cell) + (fpmp_left_dot_mcp_ics_linear_transport_source_raw_np_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_linear_transport_source_raw_np_cell_dot_pointwise_right. ff_h_fpmp_dot_mcp_ics_linear_transport_source_raw_np_cell_dot_pointwise_right + S (fpmp_right_dot_mcp_ics_linear_transport_source_raw_np_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_linear_transport_source_raw_np_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_linear_transport_source_raw_np_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_linear_transport_source_raw_np_cell_dot_pointwise_right. ff_right_mcp_cell_ics_linear_transport_source_raw_np_cell = ff_q_fpmp_dot_mcp_ics_linear_transport_source_raw_np_cell_dot_pointwise_right * S ((S (fpmp_index_dot_mcp_ics_linear_transport_source_raw_np_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_linear_transport_source_raw_np_cell) + (fpmp_right_dot_mcp_ics_linear_transport_source_raw_np_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_linear_transport_source_raw_np_cell_dot_pointwise_target. ff_h_fpmp_dot_mcp_ics_linear_transport_source_raw_np_cell_dot_pointwise_target + S (fpmp_target_dot_mcp_ics_linear_transport_source_raw_np_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_linear_transport_source_raw_np_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_linear_transport_source_raw_np_cell_dot)) /\ exists ff_q_fpmp_dot_mcp_ics_linear_transport_source_raw_np_cell_dot_pointwise_target. ff_code_dot_mcp_ics_linear_transport_source_raw_np_cell_dot = ff_q_fpmp_dot_mcp_ics_linear_transport_source_raw_np_cell_dot_pointwise_target * S ((S (fpmp_index_dot_mcp_ics_linear_transport_source_raw_np_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_linear_transport_source_raw_np_cell_dot) + (fpmp_target_dot_mcp_ics_linear_transport_source_raw_np_cell_dot_pointwise))) -> fpmp_target_dot_mcp_ics_linear_transport_source_raw_np_cell_dot_pointwise = fpmp_left_dot_mcp_ics_linear_transport_source_raw_np_cell_dot_pointwise * fpmp_right_dot_mcp_ics_linear_transport_source_raw_np_cell_dot_pointwise) /\ (exists ff_u_dot_mcp_ics_linear_transport_source_raw_np_cell_dot_sum ff_v_dot_mcp_ics_linear_transport_source_raw_np_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_linear_transport_source_raw_np_cell_dot_sum_start. ff_h_dot_mcp_ics_linear_transport_source_raw_np_cell_dot_sum_start + S (0) = S ((S (0)) * ff_v_dot_mcp_ics_linear_transport_source_raw_np_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_linear_transport_source_raw_np_cell_dot_sum_start. ff_u_dot_mcp_ics_linear_transport_source_raw_np_cell_dot_sum = ff_q_dot_mcp_ics_linear_transport_source_raw_np_cell_dot_sum_start * S ((S (0)) * ff_v_dot_mcp_ics_linear_transport_source_raw_np_cell_dot_sum) + (0))) /\ ((((exists ff_h_dot_mcp_ics_linear_transport_source_raw_np_cell_dot_sum_terminal. ff_h_dot_mcp_ics_linear_transport_source_raw_np_cell_dot_sum_terminal + S (ff_value_mcp_prefix_ics_linear_transport_source_raw_np) = S ((S (w)) * ff_v_dot_mcp_ics_linear_transport_source_raw_np_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_linear_transport_source_raw_np_cell_dot_sum_terminal. ff_u_dot_mcp_ics_linear_transport_source_raw_np_cell_dot_sum = ff_q_dot_mcp_ics_linear_transport_source_raw_np_cell_dot_sum_terminal * S ((S (w)) * ff_v_dot_mcp_ics_linear_transport_source_raw_np_cell_dot_sum) + (ff_value_mcp_prefix_ics_linear_transport_source_raw_np))) /\ forall ff_i_dot_mcp_ics_linear_transport_source_raw_np_cell_dot_sum. (exists ff_lt_dot_mcp_ics_linear_transport_source_raw_np_cell_dot_sum_bound. ff_lt_dot_mcp_ics_linear_transport_source_raw_np_cell_dot_sum_bound + S ff_i_dot_mcp_ics_linear_transport_source_raw_np_cell_dot_sum = w) -> exists ff_a_dot_mcp_ics_linear_transport_source_raw_np_cell_dot_sum ff_r_dot_mcp_ics_linear_transport_source_raw_np_cell_dot_sum ff_s_dot_mcp_ics_linear_transport_source_raw_np_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_linear_transport_source_raw_np_cell_dot_sum_summand. ff_h_dot_mcp_ics_linear_transport_source_raw_np_cell_dot_sum_summand + S (ff_a_dot_mcp_ics_linear_transport_source_raw_np_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_linear_transport_source_raw_np_cell_dot_sum)) * ff_scale_dot_mcp_ics_linear_transport_source_raw_np_cell_dot)) /\ exists ff_q_dot_mcp_ics_linear_transport_source_raw_np_cell_dot_sum_summand. ff_code_dot_mcp_ics_linear_transport_source_raw_np_cell_dot = ff_q_dot_mcp_ics_linear_transport_source_raw_np_cell_dot_sum_summand * S ((S (ff_i_dot_mcp_ics_linear_transport_source_raw_np_cell_dot_sum)) * ff_scale_dot_mcp_ics_linear_transport_source_raw_np_cell_dot) + (ff_a_dot_mcp_ics_linear_transport_source_raw_np_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_linear_transport_source_raw_np_cell_dot_sum_partial. ff_h_dot_mcp_ics_linear_transport_source_raw_np_cell_dot_sum_partial + S (ff_r_dot_mcp_ics_linear_transport_source_raw_np_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_linear_transport_source_raw_np_cell_dot_sum)) * ff_v_dot_mcp_ics_linear_transport_source_raw_np_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_linear_transport_source_raw_np_cell_dot_sum_partial. ff_u_dot_mcp_ics_linear_transport_source_raw_np_cell_dot_sum = ff_q_dot_mcp_ics_linear_transport_source_raw_np_cell_dot_sum_partial * S ((S (ff_i_dot_mcp_ics_linear_transport_source_raw_np_cell_dot_sum)) * ff_v_dot_mcp_ics_linear_transport_source_raw_np_cell_dot_sum) + (ff_r_dot_mcp_ics_linear_transport_source_raw_np_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_linear_transport_source_raw_np_cell_dot_sum_successor. ff_h_dot_mcp_ics_linear_transport_source_raw_np_cell_dot_sum_successor + S (ff_s_dot_mcp_ics_linear_transport_source_raw_np_cell_dot_sum) = S ((S (S ff_i_dot_mcp_ics_linear_transport_source_raw_np_cell_dot_sum)) * ff_v_dot_mcp_ics_linear_transport_source_raw_np_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_linear_transport_source_raw_np_cell_dot_sum_successor. ff_u_dot_mcp_ics_linear_transport_source_raw_np_cell_dot_sum = ff_q_dot_mcp_ics_linear_transport_source_raw_np_cell_dot_sum_successor * S ((S (S ff_i_dot_mcp_ics_linear_transport_source_raw_np_cell_dot_sum)) * ff_v_dot_mcp_ics_linear_transport_source_raw_np_cell_dot_sum) + (ff_s_dot_mcp_ics_linear_transport_source_raw_np_cell_dot_sum))) /\ ff_s_dot_mcp_ics_linear_transport_source_raw_np_cell_dot_sum = ff_r_dot_mcp_ics_linear_transport_source_raw_np_cell_dot_sum + ff_a_dot_mcp_ics_linear_transport_source_raw_np_cell_dot_sum))))))))))) /\ (((exists fs_h_mcp_ics_linear_transport_source_raw_np_entry. fs_h_mcp_ics_linear_transport_source_raw_np_entry + S (ff_value_mcp_prefix_ics_linear_transport_source_raw_np) = S ((S (ff_index_mcp_prefix_ics_linear_transport_source_raw_np)) * ff_nps_mcp_smatrix_ics_linear_transport_source_raw)) /\ exists fs_q_mcp_ics_linear_transport_source_raw_np_entry. ff_np_mcp_smatrix_ics_linear_transport_source_raw = fs_q_mcp_ics_linear_transport_source_raw_np_entry * S ((S (ff_index_mcp_prefix_ics_linear_transport_source_raw_np)) * ff_nps_mcp_smatrix_ics_linear_transport_source_raw) + (ff_value_mcp_prefix_ics_linear_transport_source_raw_np))))))) /\ ((forall ff_index_mcp_add_ics_linear_transport_source_raw_positive ff_left_mcp_add_ics_linear_transport_source_raw_positive ff_right_mcp_add_ics_linear_transport_source_raw_positive ff_target_mcp_add_ics_linear_transport_source_raw_positive. (exists mcp_gap_ics_linear_transport_source_raw_positive_bound. mcp_gap_ics_linear_transport_source_raw_positive_bound + S (ff_index_mcp_add_ics_linear_transport_source_raw_positive) = ((r) * (1))) -> (((exists fs_h_mcp_ics_linear_transport_source_raw_positive_left. fs_h_mcp_ics_linear_transport_source_raw_positive_left + S (ff_left_mcp_add_ics_linear_transport_source_raw_positive) = S ((S (ff_index_mcp_add_ics_linear_transport_source_raw_positive)) * ff_pps_mcp_smatrix_ics_linear_transport_source_raw)) /\ exists fs_q_mcp_ics_linear_transport_source_raw_positive_left. ff_pp_mcp_smatrix_ics_linear_transport_source_raw = fs_q_mcp_ics_linear_transport_source_raw_positive_left * S ((S (ff_index_mcp_add_ics_linear_transport_source_raw_positive)) * ff_pps_mcp_smatrix_ics_linear_transport_source_raw) + (ff_left_mcp_add_ics_linear_transport_source_raw_positive))) -> (((exists fs_h_mcp_ics_linear_transport_source_raw_positive_right. fs_h_mcp_ics_linear_transport_source_raw_positive_right + S (ff_right_mcp_add_ics_linear_transport_source_raw_positive) = S ((S (ff_index_mcp_add_ics_linear_transport_source_raw_positive)) * ff_nns_mcp_smatrix_ics_linear_transport_source_raw)) /\ exists fs_q_mcp_ics_linear_transport_source_raw_positive_right. ff_nn_mcp_smatrix_ics_linear_transport_source_raw = fs_q_mcp_ics_linear_transport_source_raw_positive_right * S ((S (ff_index_mcp_add_ics_linear_transport_source_raw_positive)) * ff_nns_mcp_smatrix_ics_linear_transport_source_raw) + (ff_right_mcp_add_ics_linear_transport_source_raw_positive))) -> (((exists fs_h_mcp_ics_linear_transport_source_raw_positive_target. fs_h_mcp_ics_linear_transport_source_raw_positive_target + S (ff_target_mcp_add_ics_linear_transport_source_raw_positive) = S ((S (ff_index_mcp_add_ics_linear_transport_source_raw_positive)) * ics_raw_positive_scale_linear_transport_source)) /\ exists fs_q_mcp_ics_linear_transport_source_raw_positive_target. ics_raw_positive_linear_transport_source = fs_q_mcp_ics_linear_transport_source_raw_positive_target * S ((S (ff_index_mcp_add_ics_linear_transport_source_raw_positive)) * ics_raw_positive_scale_linear_transport_source) + (ff_target_mcp_add_ics_linear_transport_source_raw_positive))) -> ff_target_mcp_add_ics_linear_transport_source_raw_positive = ff_left_mcp_add_ics_linear_transport_source_raw_positive + ff_right_mcp_add_ics_linear_transport_source_raw_positive) /\ (forall ff_index_mcp_add_ics_linear_transport_source_raw_negative ff_left_mcp_add_ics_linear_transport_source_raw_negative ff_right_mcp_add_ics_linear_transport_source_raw_negative ff_target_mcp_add_ics_linear_transport_source_raw_negative. (exists mcp_gap_ics_linear_transport_source_raw_negative_bound. mcp_gap_ics_linear_transport_source_raw_negative_bound + S (ff_index_mcp_add_ics_linear_transport_source_raw_negative) = ((r) * (1))) -> (((exists fs_h_mcp_ics_linear_transport_source_raw_negative_left. fs_h_mcp_ics_linear_transport_source_raw_negative_left + S (ff_left_mcp_add_ics_linear_transport_source_raw_negative) = S ((S (ff_index_mcp_add_ics_linear_transport_source_raw_negative)) * ff_pns_mcp_smatrix_ics_linear_transport_source_raw)) /\ exists fs_q_mcp_ics_linear_transport_source_raw_negative_left. ff_pn_mcp_smatrix_ics_linear_transport_source_raw = fs_q_mcp_ics_linear_transport_source_raw_negative_left * S ((S (ff_index_mcp_add_ics_linear_transport_source_raw_negative)) * ff_pns_mcp_smatrix_ics_linear_transport_source_raw) + (ff_left_mcp_add_ics_linear_transport_source_raw_negative))) -> (((exists fs_h_mcp_ics_linear_transport_source_raw_negative_right. fs_h_mcp_ics_linear_transport_source_raw_negative_right + S (ff_right_mcp_add_ics_linear_transport_source_raw_negative) = S ((S (ff_index_mcp_add_ics_linear_transport_source_raw_negative)) * ff_nps_mcp_smatrix_ics_linear_transport_source_raw)) /\ exists fs_q_mcp_ics_linear_transport_source_raw_negative_right. ff_np_mcp_smatrix_ics_linear_transport_source_raw = fs_q_mcp_ics_linear_transport_source_raw_negative_right * S ((S (ff_index_mcp_add_ics_linear_transport_source_raw_negative)) * ff_nps_mcp_smatrix_ics_linear_transport_source_raw) + (ff_right_mcp_add_ics_linear_transport_source_raw_negative))) -> (((exists fs_h_mcp_ics_linear_transport_source_raw_negative_target. fs_h_mcp_ics_linear_transport_source_raw_negative_target + S (ff_target_mcp_add_ics_linear_transport_source_raw_negative) = S ((S (ff_index_mcp_add_ics_linear_transport_source_raw_negative)) * ics_raw_negative_scale_linear_transport_source)) /\ exists fs_q_mcp_ics_linear_transport_source_raw_negative_target. ics_raw_negative_linear_transport_source = fs_q_mcp_ics_linear_transport_source_raw_negative_target * S ((S (ff_index_mcp_add_ics_linear_transport_source_raw_negative)) * ics_raw_negative_scale_linear_transport_source) + (ff_target_mcp_add_ics_linear_transport_source_raw_negative))) -> ff_target_mcp_add_ics_linear_transport_source_raw_negative = ff_left_mcp_add_ics_linear_transport_source_raw_negative + ff_right_mcp_add_ics_linear_transport_source_raw_negative))))))) /\ (forall ics_index_linear_transport_source_equal ics_value0_linear_transport_source_equal ics_value1_linear_transport_source_equal ics_value2_linear_transport_source_equal ics_value3_linear_transport_source_equal. (exists ics_gap_linear_transport_source_equal_bound. ics_gap_linear_transport_source_equal_bound + S (ics_index_linear_transport_source_equal) = (r)) -> (((exists fs_h_ics_linear_transport_source_equal_at0. fs_h_ics_linear_transport_source_equal_at0 + S (ics_value0_linear_transport_source_equal) = S ((S (ics_index_linear_transport_source_equal)) * ics_raw_positive_scale_linear_transport_source)) /\ exists fs_q_ics_linear_transport_source_equal_at0. ics_raw_positive_linear_transport_source = fs_q_ics_linear_transport_source_equal_at0 * S ((S (ics_index_linear_transport_source_equal)) * ics_raw_positive_scale_linear_transport_source) + (ics_value0_linear_transport_source_equal))) -> (((exists fs_h_ics_linear_transport_source_equal_at1. fs_h_ics_linear_transport_source_equal_at1 + S (ics_value1_linear_transport_source_equal) = S ((S (ics_index_linear_transport_source_equal)) * ics_raw_negative_scale_linear_transport_source)) /\ exists fs_q_ics_linear_transport_source_equal_at1. ics_raw_negative_linear_transport_source = fs_q_ics_linear_transport_source_equal_at1 * S ((S (ics_index_linear_transport_source_equal)) * ics_raw_negative_scale_linear_transport_source) + (ics_value1_linear_transport_source_equal))) -> (((exists fs_h_ics_linear_transport_source_equal_at2. fs_h_ics_linear_transport_source_equal_at2 + S (ics_value2_linear_transport_source_equal) = S ((S (ics_index_linear_transport_source_equal)) * pc)) /\ exists fs_q_ics_linear_transport_source_equal_at2. pb = fs_q_ics_linear_transport_source_equal_at2 * S ((S (ics_index_linear_transport_source_equal)) * pc) + (ics_value2_linear_transport_source_equal))) -> (((exists fs_h_ics_linear_transport_source_equal_at3. fs_h_ics_linear_transport_source_equal_at3 + S (ics_value3_linear_transport_source_equal) = S ((S (ics_index_linear_transport_source_equal)) * nc)) /\ exists fs_q_ics_linear_transport_source_equal_at3. nb = fs_q_ics_linear_transport_source_equal_at3 * S ((S (ics_index_linear_transport_source_equal)) * nc) + (ics_value3_linear_transport_source_equal))) -> ics_value0_linear_transport_source_equal + ics_value3_linear_transport_source_equal = ics_value2_linear_transport_source_equal + ics_value1_linear_transport_source_equal)))) -> (forall ics_index_linear_transport_equal ics_value0_linear_transport_equal ics_value1_linear_transport_equal ics_value2_linear_transport_equal ics_value3_linear_transport_equal. (exists ics_gap_linear_transport_equal_bound. ics_gap_linear_transport_equal_bound + S (ics_index_linear_transport_equal) = (r)) -> (((exists fs_h_ics_linear_transport_equal_at0. fs_h_ics_linear_transport_equal_at0 + S (ics_value0_linear_transport_equal) = S ((S (ics_index_linear_transport_equal)) * pc)) /\ exists fs_q_ics_linear_transport_equal_at0. pb = fs_q_ics_linear_transport_equal_at0 * S ((S (ics_index_linear_transport_equal)) * pc) + (ics_value0_linear_transport_equal))) -> (((exists fs_h_ics_linear_transport_equal_at1. fs_h_ics_linear_transport_equal_at1 + S (ics_value1_linear_transport_equal) = S ((S (ics_index_linear_transport_equal)) * nc)) /\ exists fs_q_ics_linear_transport_equal_at1. nb = fs_q_ics_linear_transport_equal_at1 * S ((S (ics_index_linear_transport_equal)) * nc) + (ics_value1_linear_transport_equal))) -> (((exists fs_h_ics_linear_transport_equal_at2. fs_h_ics_linear_transport_equal_at2 + S (ics_value2_linear_transport_equal) = S ((S (ics_index_linear_transport_equal)) * qc)) /\ exists fs_q_ics_linear_transport_equal_at2. qb = fs_q_ics_linear_transport_equal_at2 * S ((S (ics_index_linear_transport_equal)) * qc) + (ics_value2_linear_transport_equal))) -> (((exists fs_h_ics_linear_transport_equal_at3. fs_h_ics_linear_transport_equal_at3 + S (ics_value3_linear_transport_equal) = S ((S (ics_index_linear_transport_equal)) * mc)) /\ exists fs_q_ics_linear_transport_equal_at3. mb = fs_q_ics_linear_transport_equal_at3 * S ((S (ics_index_linear_transport_equal)) * mc) + (ics_value3_linear_transport_equal))) -> ics_value0_linear_transport_equal + ics_value3_linear_transport_equal = ics_value2_linear_transport_equal + ics_value1_linear_transport_equal) -> (exists ics_raw_positive_linear_transport_result ics_raw_positive_scale_linear_transport_result ics_raw_negative_linear_transport_result ics_raw_negative_scale_linear_transport_result. (((exists ff_pp_mcp_smatrix_ics_linear_transport_result_raw ff_pps_mcp_smatrix_ics_linear_transport_result_raw ff_nn_mcp_smatrix_ics_linear_transport_result_raw ff_nns_mcp_smatrix_ics_linear_transport_result_raw ff_pn_mcp_smatrix_ics_linear_transport_result_raw ff_pns_mcp_smatrix_ics_linear_transport_result_raw ff_np_mcp_smatrix_ics_linear_transport_result_raw ff_nps_mcp_smatrix_ics_linear_transport_result_raw. ((forall ff_index_mcp_prefix_ics_linear_transport_result_raw_pp. (exists mcp_gap_ics_linear_transport_result_raw_pp_index. mcp_gap_ics_linear_transport_result_raw_pp_index + S (ff_index_mcp_prefix_ics_linear_transport_result_raw_pp) = ((r) * (1))) -> exists ff_row_mcp_prefix_ics_linear_transport_result_raw_pp ff_column_mcp_prefix_ics_linear_transport_result_raw_pp ff_value_mcp_prefix_ics_linear_transport_result_raw_pp. ((ff_index_mcp_prefix_ics_linear_transport_result_raw_pp) = (1) * ff_row_mcp_prefix_ics_linear_transport_result_raw_pp + ff_column_mcp_prefix_ics_linear_transport_result_raw_pp /\ ((exists mcp_gap_ics_linear_transport_result_raw_pp_column. mcp_gap_ics_linear_transport_result_raw_pp_column + S (ff_column_mcp_prefix_ics_linear_transport_result_raw_pp) = (1)) /\ ((exists ff_left_mcp_cell_ics_linear_transport_result_raw_pp_cell ff_left_scale_mcp_cell_ics_linear_transport_result_raw_pp_cell ff_right_mcp_cell_ics_linear_transport_result_raw_pp_cell ff_right_scale_mcp_cell_ics_linear_transport_result_raw_pp_cell. ((forall ff_index_mcp_ics_linear_transport_result_raw_pp_cell_row ff_source_mcp_ics_linear_transport_result_raw_pp_cell_row ff_target_mcp_ics_linear_transport_result_raw_pp_cell_row. (exists mcp_gap_ics_linear_transport_result_raw_pp_cell_row_bound. mcp_gap_ics_linear_transport_result_raw_pp_cell_row_bound + S (ff_index_mcp_ics_linear_transport_result_raw_pp_cell_row) = (w)) -> (((exists fs_h_mcp_ics_linear_transport_result_raw_pp_cell_row_source. fs_h_mcp_ics_linear_transport_result_raw_pp_cell_row_source + S (ff_source_mcp_ics_linear_transport_result_raw_pp_cell_row) = S ((S (((ff_row_mcp_prefix_ics_linear_transport_result_raw_pp) * (w)) + (1) * ff_index_mcp_ics_linear_transport_result_raw_pp_cell_row)) * ac)) /\ exists fs_q_mcp_ics_linear_transport_result_raw_pp_cell_row_source. ab = fs_q_mcp_ics_linear_transport_result_raw_pp_cell_row_source * S ((S (((ff_row_mcp_prefix_ics_linear_transport_result_raw_pp) * (w)) + (1) * ff_index_mcp_ics_linear_transport_result_raw_pp_cell_row)) * ac) + (ff_source_mcp_ics_linear_transport_result_raw_pp_cell_row))) -> (((exists fs_h_mcp_ics_linear_transport_result_raw_pp_cell_row_target. fs_h_mcp_ics_linear_transport_result_raw_pp_cell_row_target + S (ff_target_mcp_ics_linear_transport_result_raw_pp_cell_row) = S ((S (ff_index_mcp_ics_linear_transport_result_raw_pp_cell_row)) * ff_left_scale_mcp_cell_ics_linear_transport_result_raw_pp_cell)) /\ exists fs_q_mcp_ics_linear_transport_result_raw_pp_cell_row_target. ff_left_mcp_cell_ics_linear_transport_result_raw_pp_cell = fs_q_mcp_ics_linear_transport_result_raw_pp_cell_row_target * S ((S (ff_index_mcp_ics_linear_transport_result_raw_pp_cell_row)) * ff_left_scale_mcp_cell_ics_linear_transport_result_raw_pp_cell) + (ff_target_mcp_ics_linear_transport_result_raw_pp_cell_row))) -> ff_target_mcp_ics_linear_transport_result_raw_pp_cell_row = ff_source_mcp_ics_linear_transport_result_raw_pp_cell_row) /\ ((forall ff_index_mcp_ics_linear_transport_result_raw_pp_cell_column ff_source_mcp_ics_linear_transport_result_raw_pp_cell_column ff_target_mcp_ics_linear_transport_result_raw_pp_cell_column. (exists mcp_gap_ics_linear_transport_result_raw_pp_cell_column_bound. mcp_gap_ics_linear_transport_result_raw_pp_cell_column_bound + S (ff_index_mcp_ics_linear_transport_result_raw_pp_cell_column) = (w)) -> (((exists fs_h_mcp_ics_linear_transport_result_raw_pp_cell_column_source. fs_h_mcp_ics_linear_transport_result_raw_pp_cell_column_source + S (ff_source_mcp_ics_linear_transport_result_raw_pp_cell_column) = S ((S ((ff_column_mcp_prefix_ics_linear_transport_result_raw_pp) + (1) * ff_index_mcp_ics_linear_transport_result_raw_pp_cell_column)) * ec)) /\ exists fs_q_mcp_ics_linear_transport_result_raw_pp_cell_column_source. eb = fs_q_mcp_ics_linear_transport_result_raw_pp_cell_column_source * S ((S ((ff_column_mcp_prefix_ics_linear_transport_result_raw_pp) + (1) * ff_index_mcp_ics_linear_transport_result_raw_pp_cell_column)) * ec) + (ff_source_mcp_ics_linear_transport_result_raw_pp_cell_column))) -> (((exists fs_h_mcp_ics_linear_transport_result_raw_pp_cell_column_target. fs_h_mcp_ics_linear_transport_result_raw_pp_cell_column_target + S (ff_target_mcp_ics_linear_transport_result_raw_pp_cell_column) = S ((S (ff_index_mcp_ics_linear_transport_result_raw_pp_cell_column)) * ff_right_scale_mcp_cell_ics_linear_transport_result_raw_pp_cell)) /\ exists fs_q_mcp_ics_linear_transport_result_raw_pp_cell_column_target. ff_right_mcp_cell_ics_linear_transport_result_raw_pp_cell = fs_q_mcp_ics_linear_transport_result_raw_pp_cell_column_target * S ((S (ff_index_mcp_ics_linear_transport_result_raw_pp_cell_column)) * ff_right_scale_mcp_cell_ics_linear_transport_result_raw_pp_cell) + (ff_target_mcp_ics_linear_transport_result_raw_pp_cell_column))) -> ff_target_mcp_ics_linear_transport_result_raw_pp_cell_column = ff_source_mcp_ics_linear_transport_result_raw_pp_cell_column) /\ (exists ff_code_dot_mcp_ics_linear_transport_result_raw_pp_cell_dot ff_scale_dot_mcp_ics_linear_transport_result_raw_pp_cell_dot. ((forall fpmp_index_dot_mcp_ics_linear_transport_result_raw_pp_cell_dot_pointwise fpmp_left_dot_mcp_ics_linear_transport_result_raw_pp_cell_dot_pointwise fpmp_right_dot_mcp_ics_linear_transport_result_raw_pp_cell_dot_pointwise fpmp_target_dot_mcp_ics_linear_transport_result_raw_pp_cell_dot_pointwise. (exists fpmp_gap_dot_mcp_ics_linear_transport_result_raw_pp_cell_dot_pointwise. fpmp_gap_dot_mcp_ics_linear_transport_result_raw_pp_cell_dot_pointwise + S fpmp_index_dot_mcp_ics_linear_transport_result_raw_pp_cell_dot_pointwise = w) -> (((exists ff_h_fpmp_dot_mcp_ics_linear_transport_result_raw_pp_cell_dot_pointwise_left. ff_h_fpmp_dot_mcp_ics_linear_transport_result_raw_pp_cell_dot_pointwise_left + S (fpmp_left_dot_mcp_ics_linear_transport_result_raw_pp_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_linear_transport_result_raw_pp_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_linear_transport_result_raw_pp_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_linear_transport_result_raw_pp_cell_dot_pointwise_left. ff_left_mcp_cell_ics_linear_transport_result_raw_pp_cell = ff_q_fpmp_dot_mcp_ics_linear_transport_result_raw_pp_cell_dot_pointwise_left * S ((S (fpmp_index_dot_mcp_ics_linear_transport_result_raw_pp_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_linear_transport_result_raw_pp_cell) + (fpmp_left_dot_mcp_ics_linear_transport_result_raw_pp_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_linear_transport_result_raw_pp_cell_dot_pointwise_right. ff_h_fpmp_dot_mcp_ics_linear_transport_result_raw_pp_cell_dot_pointwise_right + S (fpmp_right_dot_mcp_ics_linear_transport_result_raw_pp_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_linear_transport_result_raw_pp_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_linear_transport_result_raw_pp_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_linear_transport_result_raw_pp_cell_dot_pointwise_right. ff_right_mcp_cell_ics_linear_transport_result_raw_pp_cell = ff_q_fpmp_dot_mcp_ics_linear_transport_result_raw_pp_cell_dot_pointwise_right * S ((S (fpmp_index_dot_mcp_ics_linear_transport_result_raw_pp_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_linear_transport_result_raw_pp_cell) + (fpmp_right_dot_mcp_ics_linear_transport_result_raw_pp_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_linear_transport_result_raw_pp_cell_dot_pointwise_target. ff_h_fpmp_dot_mcp_ics_linear_transport_result_raw_pp_cell_dot_pointwise_target + S (fpmp_target_dot_mcp_ics_linear_transport_result_raw_pp_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_linear_transport_result_raw_pp_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_linear_transport_result_raw_pp_cell_dot)) /\ exists ff_q_fpmp_dot_mcp_ics_linear_transport_result_raw_pp_cell_dot_pointwise_target. ff_code_dot_mcp_ics_linear_transport_result_raw_pp_cell_dot = ff_q_fpmp_dot_mcp_ics_linear_transport_result_raw_pp_cell_dot_pointwise_target * S ((S (fpmp_index_dot_mcp_ics_linear_transport_result_raw_pp_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_linear_transport_result_raw_pp_cell_dot) + (fpmp_target_dot_mcp_ics_linear_transport_result_raw_pp_cell_dot_pointwise))) -> fpmp_target_dot_mcp_ics_linear_transport_result_raw_pp_cell_dot_pointwise = fpmp_left_dot_mcp_ics_linear_transport_result_raw_pp_cell_dot_pointwise * fpmp_right_dot_mcp_ics_linear_transport_result_raw_pp_cell_dot_pointwise) /\ (exists ff_u_dot_mcp_ics_linear_transport_result_raw_pp_cell_dot_sum ff_v_dot_mcp_ics_linear_transport_result_raw_pp_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_linear_transport_result_raw_pp_cell_dot_sum_start. ff_h_dot_mcp_ics_linear_transport_result_raw_pp_cell_dot_sum_start + S (0) = S ((S (0)) * ff_v_dot_mcp_ics_linear_transport_result_raw_pp_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_linear_transport_result_raw_pp_cell_dot_sum_start. ff_u_dot_mcp_ics_linear_transport_result_raw_pp_cell_dot_sum = ff_q_dot_mcp_ics_linear_transport_result_raw_pp_cell_dot_sum_start * S ((S (0)) * ff_v_dot_mcp_ics_linear_transport_result_raw_pp_cell_dot_sum) + (0))) /\ ((((exists ff_h_dot_mcp_ics_linear_transport_result_raw_pp_cell_dot_sum_terminal. ff_h_dot_mcp_ics_linear_transport_result_raw_pp_cell_dot_sum_terminal + S (ff_value_mcp_prefix_ics_linear_transport_result_raw_pp) = S ((S (w)) * ff_v_dot_mcp_ics_linear_transport_result_raw_pp_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_linear_transport_result_raw_pp_cell_dot_sum_terminal. ff_u_dot_mcp_ics_linear_transport_result_raw_pp_cell_dot_sum = ff_q_dot_mcp_ics_linear_transport_result_raw_pp_cell_dot_sum_terminal * S ((S (w)) * ff_v_dot_mcp_ics_linear_transport_result_raw_pp_cell_dot_sum) + (ff_value_mcp_prefix_ics_linear_transport_result_raw_pp))) /\ forall ff_i_dot_mcp_ics_linear_transport_result_raw_pp_cell_dot_sum. (exists ff_lt_dot_mcp_ics_linear_transport_result_raw_pp_cell_dot_sum_bound. ff_lt_dot_mcp_ics_linear_transport_result_raw_pp_cell_dot_sum_bound + S ff_i_dot_mcp_ics_linear_transport_result_raw_pp_cell_dot_sum = w) -> exists ff_a_dot_mcp_ics_linear_transport_result_raw_pp_cell_dot_sum ff_r_dot_mcp_ics_linear_transport_result_raw_pp_cell_dot_sum ff_s_dot_mcp_ics_linear_transport_result_raw_pp_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_linear_transport_result_raw_pp_cell_dot_sum_summand. ff_h_dot_mcp_ics_linear_transport_result_raw_pp_cell_dot_sum_summand + S (ff_a_dot_mcp_ics_linear_transport_result_raw_pp_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_linear_transport_result_raw_pp_cell_dot_sum)) * ff_scale_dot_mcp_ics_linear_transport_result_raw_pp_cell_dot)) /\ exists ff_q_dot_mcp_ics_linear_transport_result_raw_pp_cell_dot_sum_summand. ff_code_dot_mcp_ics_linear_transport_result_raw_pp_cell_dot = ff_q_dot_mcp_ics_linear_transport_result_raw_pp_cell_dot_sum_summand * S ((S (ff_i_dot_mcp_ics_linear_transport_result_raw_pp_cell_dot_sum)) * ff_scale_dot_mcp_ics_linear_transport_result_raw_pp_cell_dot) + (ff_a_dot_mcp_ics_linear_transport_result_raw_pp_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_linear_transport_result_raw_pp_cell_dot_sum_partial. ff_h_dot_mcp_ics_linear_transport_result_raw_pp_cell_dot_sum_partial + S (ff_r_dot_mcp_ics_linear_transport_result_raw_pp_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_linear_transport_result_raw_pp_cell_dot_sum)) * ff_v_dot_mcp_ics_linear_transport_result_raw_pp_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_linear_transport_result_raw_pp_cell_dot_sum_partial. ff_u_dot_mcp_ics_linear_transport_result_raw_pp_cell_dot_sum = ff_q_dot_mcp_ics_linear_transport_result_raw_pp_cell_dot_sum_partial * S ((S (ff_i_dot_mcp_ics_linear_transport_result_raw_pp_cell_dot_sum)) * ff_v_dot_mcp_ics_linear_transport_result_raw_pp_cell_dot_sum) + (ff_r_dot_mcp_ics_linear_transport_result_raw_pp_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_linear_transport_result_raw_pp_cell_dot_sum_successor. ff_h_dot_mcp_ics_linear_transport_result_raw_pp_cell_dot_sum_successor + S (ff_s_dot_mcp_ics_linear_transport_result_raw_pp_cell_dot_sum) = S ((S (S ff_i_dot_mcp_ics_linear_transport_result_raw_pp_cell_dot_sum)) * ff_v_dot_mcp_ics_linear_transport_result_raw_pp_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_linear_transport_result_raw_pp_cell_dot_sum_successor. ff_u_dot_mcp_ics_linear_transport_result_raw_pp_cell_dot_sum = ff_q_dot_mcp_ics_linear_transport_result_raw_pp_cell_dot_sum_successor * S ((S (S ff_i_dot_mcp_ics_linear_transport_result_raw_pp_cell_dot_sum)) * ff_v_dot_mcp_ics_linear_transport_result_raw_pp_cell_dot_sum) + (ff_s_dot_mcp_ics_linear_transport_result_raw_pp_cell_dot_sum))) /\ ff_s_dot_mcp_ics_linear_transport_result_raw_pp_cell_dot_sum = ff_r_dot_mcp_ics_linear_transport_result_raw_pp_cell_dot_sum + ff_a_dot_mcp_ics_linear_transport_result_raw_pp_cell_dot_sum))))))))))) /\ (((exists fs_h_mcp_ics_linear_transport_result_raw_pp_entry. fs_h_mcp_ics_linear_transport_result_raw_pp_entry + S (ff_value_mcp_prefix_ics_linear_transport_result_raw_pp) = S ((S (ff_index_mcp_prefix_ics_linear_transport_result_raw_pp)) * ff_pps_mcp_smatrix_ics_linear_transport_result_raw)) /\ exists fs_q_mcp_ics_linear_transport_result_raw_pp_entry. ff_pp_mcp_smatrix_ics_linear_transport_result_raw = fs_q_mcp_ics_linear_transport_result_raw_pp_entry * S ((S (ff_index_mcp_prefix_ics_linear_transport_result_raw_pp)) * ff_pps_mcp_smatrix_ics_linear_transport_result_raw) + (ff_value_mcp_prefix_ics_linear_transport_result_raw_pp))))))) /\ ((forall ff_index_mcp_prefix_ics_linear_transport_result_raw_nn. (exists mcp_gap_ics_linear_transport_result_raw_nn_index. mcp_gap_ics_linear_transport_result_raw_nn_index + S (ff_index_mcp_prefix_ics_linear_transport_result_raw_nn) = ((r) * (1))) -> exists ff_row_mcp_prefix_ics_linear_transport_result_raw_nn ff_column_mcp_prefix_ics_linear_transport_result_raw_nn ff_value_mcp_prefix_ics_linear_transport_result_raw_nn. ((ff_index_mcp_prefix_ics_linear_transport_result_raw_nn) = (1) * ff_row_mcp_prefix_ics_linear_transport_result_raw_nn + ff_column_mcp_prefix_ics_linear_transport_result_raw_nn /\ ((exists mcp_gap_ics_linear_transport_result_raw_nn_column. mcp_gap_ics_linear_transport_result_raw_nn_column + S (ff_column_mcp_prefix_ics_linear_transport_result_raw_nn) = (1)) /\ ((exists ff_left_mcp_cell_ics_linear_transport_result_raw_nn_cell ff_left_scale_mcp_cell_ics_linear_transport_result_raw_nn_cell ff_right_mcp_cell_ics_linear_transport_result_raw_nn_cell ff_right_scale_mcp_cell_ics_linear_transport_result_raw_nn_cell. ((forall ff_index_mcp_ics_linear_transport_result_raw_nn_cell_row ff_source_mcp_ics_linear_transport_result_raw_nn_cell_row ff_target_mcp_ics_linear_transport_result_raw_nn_cell_row. (exists mcp_gap_ics_linear_transport_result_raw_nn_cell_row_bound. mcp_gap_ics_linear_transport_result_raw_nn_cell_row_bound + S (ff_index_mcp_ics_linear_transport_result_raw_nn_cell_row) = (w)) -> (((exists fs_h_mcp_ics_linear_transport_result_raw_nn_cell_row_source. fs_h_mcp_ics_linear_transport_result_raw_nn_cell_row_source + S (ff_source_mcp_ics_linear_transport_result_raw_nn_cell_row) = S ((S (((ff_row_mcp_prefix_ics_linear_transport_result_raw_nn) * (w)) + (1) * ff_index_mcp_ics_linear_transport_result_raw_nn_cell_row)) * dc)) /\ exists fs_q_mcp_ics_linear_transport_result_raw_nn_cell_row_source. db = fs_q_mcp_ics_linear_transport_result_raw_nn_cell_row_source * S ((S (((ff_row_mcp_prefix_ics_linear_transport_result_raw_nn) * (w)) + (1) * ff_index_mcp_ics_linear_transport_result_raw_nn_cell_row)) * dc) + (ff_source_mcp_ics_linear_transport_result_raw_nn_cell_row))) -> (((exists fs_h_mcp_ics_linear_transport_result_raw_nn_cell_row_target. fs_h_mcp_ics_linear_transport_result_raw_nn_cell_row_target + S (ff_target_mcp_ics_linear_transport_result_raw_nn_cell_row) = S ((S (ff_index_mcp_ics_linear_transport_result_raw_nn_cell_row)) * ff_left_scale_mcp_cell_ics_linear_transport_result_raw_nn_cell)) /\ exists fs_q_mcp_ics_linear_transport_result_raw_nn_cell_row_target. ff_left_mcp_cell_ics_linear_transport_result_raw_nn_cell = fs_q_mcp_ics_linear_transport_result_raw_nn_cell_row_target * S ((S (ff_index_mcp_ics_linear_transport_result_raw_nn_cell_row)) * ff_left_scale_mcp_cell_ics_linear_transport_result_raw_nn_cell) + (ff_target_mcp_ics_linear_transport_result_raw_nn_cell_row))) -> ff_target_mcp_ics_linear_transport_result_raw_nn_cell_row = ff_source_mcp_ics_linear_transport_result_raw_nn_cell_row) /\ ((forall ff_index_mcp_ics_linear_transport_result_raw_nn_cell_column ff_source_mcp_ics_linear_transport_result_raw_nn_cell_column ff_target_mcp_ics_linear_transport_result_raw_nn_cell_column. (exists mcp_gap_ics_linear_transport_result_raw_nn_cell_column_bound. mcp_gap_ics_linear_transport_result_raw_nn_cell_column_bound + S (ff_index_mcp_ics_linear_transport_result_raw_nn_cell_column) = (w)) -> (((exists fs_h_mcp_ics_linear_transport_result_raw_nn_cell_column_source. fs_h_mcp_ics_linear_transport_result_raw_nn_cell_column_source + S (ff_source_mcp_ics_linear_transport_result_raw_nn_cell_column) = S ((S ((ff_column_mcp_prefix_ics_linear_transport_result_raw_nn) + (1) * ff_index_mcp_ics_linear_transport_result_raw_nn_cell_column)) * fc)) /\ exists fs_q_mcp_ics_linear_transport_result_raw_nn_cell_column_source. fb = fs_q_mcp_ics_linear_transport_result_raw_nn_cell_column_source * S ((S ((ff_column_mcp_prefix_ics_linear_transport_result_raw_nn) + (1) * ff_index_mcp_ics_linear_transport_result_raw_nn_cell_column)) * fc) + (ff_source_mcp_ics_linear_transport_result_raw_nn_cell_column))) -> (((exists fs_h_mcp_ics_linear_transport_result_raw_nn_cell_column_target. fs_h_mcp_ics_linear_transport_result_raw_nn_cell_column_target + S (ff_target_mcp_ics_linear_transport_result_raw_nn_cell_column) = S ((S (ff_index_mcp_ics_linear_transport_result_raw_nn_cell_column)) * ff_right_scale_mcp_cell_ics_linear_transport_result_raw_nn_cell)) /\ exists fs_q_mcp_ics_linear_transport_result_raw_nn_cell_column_target. ff_right_mcp_cell_ics_linear_transport_result_raw_nn_cell = fs_q_mcp_ics_linear_transport_result_raw_nn_cell_column_target * S ((S (ff_index_mcp_ics_linear_transport_result_raw_nn_cell_column)) * ff_right_scale_mcp_cell_ics_linear_transport_result_raw_nn_cell) + (ff_target_mcp_ics_linear_transport_result_raw_nn_cell_column))) -> ff_target_mcp_ics_linear_transport_result_raw_nn_cell_column = ff_source_mcp_ics_linear_transport_result_raw_nn_cell_column) /\ (exists ff_code_dot_mcp_ics_linear_transport_result_raw_nn_cell_dot ff_scale_dot_mcp_ics_linear_transport_result_raw_nn_cell_dot. ((forall fpmp_index_dot_mcp_ics_linear_transport_result_raw_nn_cell_dot_pointwise fpmp_left_dot_mcp_ics_linear_transport_result_raw_nn_cell_dot_pointwise fpmp_right_dot_mcp_ics_linear_transport_result_raw_nn_cell_dot_pointwise fpmp_target_dot_mcp_ics_linear_transport_result_raw_nn_cell_dot_pointwise. (exists fpmp_gap_dot_mcp_ics_linear_transport_result_raw_nn_cell_dot_pointwise. fpmp_gap_dot_mcp_ics_linear_transport_result_raw_nn_cell_dot_pointwise + S fpmp_index_dot_mcp_ics_linear_transport_result_raw_nn_cell_dot_pointwise = w) -> (((exists ff_h_fpmp_dot_mcp_ics_linear_transport_result_raw_nn_cell_dot_pointwise_left. ff_h_fpmp_dot_mcp_ics_linear_transport_result_raw_nn_cell_dot_pointwise_left + S (fpmp_left_dot_mcp_ics_linear_transport_result_raw_nn_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_linear_transport_result_raw_nn_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_linear_transport_result_raw_nn_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_linear_transport_result_raw_nn_cell_dot_pointwise_left. ff_left_mcp_cell_ics_linear_transport_result_raw_nn_cell = ff_q_fpmp_dot_mcp_ics_linear_transport_result_raw_nn_cell_dot_pointwise_left * S ((S (fpmp_index_dot_mcp_ics_linear_transport_result_raw_nn_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_linear_transport_result_raw_nn_cell) + (fpmp_left_dot_mcp_ics_linear_transport_result_raw_nn_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_linear_transport_result_raw_nn_cell_dot_pointwise_right. ff_h_fpmp_dot_mcp_ics_linear_transport_result_raw_nn_cell_dot_pointwise_right + S (fpmp_right_dot_mcp_ics_linear_transport_result_raw_nn_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_linear_transport_result_raw_nn_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_linear_transport_result_raw_nn_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_linear_transport_result_raw_nn_cell_dot_pointwise_right. ff_right_mcp_cell_ics_linear_transport_result_raw_nn_cell = ff_q_fpmp_dot_mcp_ics_linear_transport_result_raw_nn_cell_dot_pointwise_right * S ((S (fpmp_index_dot_mcp_ics_linear_transport_result_raw_nn_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_linear_transport_result_raw_nn_cell) + (fpmp_right_dot_mcp_ics_linear_transport_result_raw_nn_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_linear_transport_result_raw_nn_cell_dot_pointwise_target. ff_h_fpmp_dot_mcp_ics_linear_transport_result_raw_nn_cell_dot_pointwise_target + S (fpmp_target_dot_mcp_ics_linear_transport_result_raw_nn_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_linear_transport_result_raw_nn_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_linear_transport_result_raw_nn_cell_dot)) /\ exists ff_q_fpmp_dot_mcp_ics_linear_transport_result_raw_nn_cell_dot_pointwise_target. ff_code_dot_mcp_ics_linear_transport_result_raw_nn_cell_dot = ff_q_fpmp_dot_mcp_ics_linear_transport_result_raw_nn_cell_dot_pointwise_target * S ((S (fpmp_index_dot_mcp_ics_linear_transport_result_raw_nn_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_linear_transport_result_raw_nn_cell_dot) + (fpmp_target_dot_mcp_ics_linear_transport_result_raw_nn_cell_dot_pointwise))) -> fpmp_target_dot_mcp_ics_linear_transport_result_raw_nn_cell_dot_pointwise = fpmp_left_dot_mcp_ics_linear_transport_result_raw_nn_cell_dot_pointwise * fpmp_right_dot_mcp_ics_linear_transport_result_raw_nn_cell_dot_pointwise) /\ (exists ff_u_dot_mcp_ics_linear_transport_result_raw_nn_cell_dot_sum ff_v_dot_mcp_ics_linear_transport_result_raw_nn_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_linear_transport_result_raw_nn_cell_dot_sum_start. ff_h_dot_mcp_ics_linear_transport_result_raw_nn_cell_dot_sum_start + S (0) = S ((S (0)) * ff_v_dot_mcp_ics_linear_transport_result_raw_nn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_linear_transport_result_raw_nn_cell_dot_sum_start. ff_u_dot_mcp_ics_linear_transport_result_raw_nn_cell_dot_sum = ff_q_dot_mcp_ics_linear_transport_result_raw_nn_cell_dot_sum_start * S ((S (0)) * ff_v_dot_mcp_ics_linear_transport_result_raw_nn_cell_dot_sum) + (0))) /\ ((((exists ff_h_dot_mcp_ics_linear_transport_result_raw_nn_cell_dot_sum_terminal. ff_h_dot_mcp_ics_linear_transport_result_raw_nn_cell_dot_sum_terminal + S (ff_value_mcp_prefix_ics_linear_transport_result_raw_nn) = S ((S (w)) * ff_v_dot_mcp_ics_linear_transport_result_raw_nn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_linear_transport_result_raw_nn_cell_dot_sum_terminal. ff_u_dot_mcp_ics_linear_transport_result_raw_nn_cell_dot_sum = ff_q_dot_mcp_ics_linear_transport_result_raw_nn_cell_dot_sum_terminal * S ((S (w)) * ff_v_dot_mcp_ics_linear_transport_result_raw_nn_cell_dot_sum) + (ff_value_mcp_prefix_ics_linear_transport_result_raw_nn))) /\ forall ff_i_dot_mcp_ics_linear_transport_result_raw_nn_cell_dot_sum. (exists ff_lt_dot_mcp_ics_linear_transport_result_raw_nn_cell_dot_sum_bound. ff_lt_dot_mcp_ics_linear_transport_result_raw_nn_cell_dot_sum_bound + S ff_i_dot_mcp_ics_linear_transport_result_raw_nn_cell_dot_sum = w) -> exists ff_a_dot_mcp_ics_linear_transport_result_raw_nn_cell_dot_sum ff_r_dot_mcp_ics_linear_transport_result_raw_nn_cell_dot_sum ff_s_dot_mcp_ics_linear_transport_result_raw_nn_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_linear_transport_result_raw_nn_cell_dot_sum_summand. ff_h_dot_mcp_ics_linear_transport_result_raw_nn_cell_dot_sum_summand + S (ff_a_dot_mcp_ics_linear_transport_result_raw_nn_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_linear_transport_result_raw_nn_cell_dot_sum)) * ff_scale_dot_mcp_ics_linear_transport_result_raw_nn_cell_dot)) /\ exists ff_q_dot_mcp_ics_linear_transport_result_raw_nn_cell_dot_sum_summand. ff_code_dot_mcp_ics_linear_transport_result_raw_nn_cell_dot = ff_q_dot_mcp_ics_linear_transport_result_raw_nn_cell_dot_sum_summand * S ((S (ff_i_dot_mcp_ics_linear_transport_result_raw_nn_cell_dot_sum)) * ff_scale_dot_mcp_ics_linear_transport_result_raw_nn_cell_dot) + (ff_a_dot_mcp_ics_linear_transport_result_raw_nn_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_linear_transport_result_raw_nn_cell_dot_sum_partial. ff_h_dot_mcp_ics_linear_transport_result_raw_nn_cell_dot_sum_partial + S (ff_r_dot_mcp_ics_linear_transport_result_raw_nn_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_linear_transport_result_raw_nn_cell_dot_sum)) * ff_v_dot_mcp_ics_linear_transport_result_raw_nn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_linear_transport_result_raw_nn_cell_dot_sum_partial. ff_u_dot_mcp_ics_linear_transport_result_raw_nn_cell_dot_sum = ff_q_dot_mcp_ics_linear_transport_result_raw_nn_cell_dot_sum_partial * S ((S (ff_i_dot_mcp_ics_linear_transport_result_raw_nn_cell_dot_sum)) * ff_v_dot_mcp_ics_linear_transport_result_raw_nn_cell_dot_sum) + (ff_r_dot_mcp_ics_linear_transport_result_raw_nn_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_linear_transport_result_raw_nn_cell_dot_sum_successor. ff_h_dot_mcp_ics_linear_transport_result_raw_nn_cell_dot_sum_successor + S (ff_s_dot_mcp_ics_linear_transport_result_raw_nn_cell_dot_sum) = S ((S (S ff_i_dot_mcp_ics_linear_transport_result_raw_nn_cell_dot_sum)) * ff_v_dot_mcp_ics_linear_transport_result_raw_nn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_linear_transport_result_raw_nn_cell_dot_sum_successor. ff_u_dot_mcp_ics_linear_transport_result_raw_nn_cell_dot_sum = ff_q_dot_mcp_ics_linear_transport_result_raw_nn_cell_dot_sum_successor * S ((S (S ff_i_dot_mcp_ics_linear_transport_result_raw_nn_cell_dot_sum)) * ff_v_dot_mcp_ics_linear_transport_result_raw_nn_cell_dot_sum) + (ff_s_dot_mcp_ics_linear_transport_result_raw_nn_cell_dot_sum))) /\ ff_s_dot_mcp_ics_linear_transport_result_raw_nn_cell_dot_sum = ff_r_dot_mcp_ics_linear_transport_result_raw_nn_cell_dot_sum + ff_a_dot_mcp_ics_linear_transport_result_raw_nn_cell_dot_sum))))))))))) /\ (((exists fs_h_mcp_ics_linear_transport_result_raw_nn_entry. fs_h_mcp_ics_linear_transport_result_raw_nn_entry + S (ff_value_mcp_prefix_ics_linear_transport_result_raw_nn) = S ((S (ff_index_mcp_prefix_ics_linear_transport_result_raw_nn)) * ff_nns_mcp_smatrix_ics_linear_transport_result_raw)) /\ exists fs_q_mcp_ics_linear_transport_result_raw_nn_entry. ff_nn_mcp_smatrix_ics_linear_transport_result_raw = fs_q_mcp_ics_linear_transport_result_raw_nn_entry * S ((S (ff_index_mcp_prefix_ics_linear_transport_result_raw_nn)) * ff_nns_mcp_smatrix_ics_linear_transport_result_raw) + (ff_value_mcp_prefix_ics_linear_transport_result_raw_nn))))))) /\ ((forall ff_index_mcp_prefix_ics_linear_transport_result_raw_pn. (exists mcp_gap_ics_linear_transport_result_raw_pn_index. mcp_gap_ics_linear_transport_result_raw_pn_index + S (ff_index_mcp_prefix_ics_linear_transport_result_raw_pn) = ((r) * (1))) -> exists ff_row_mcp_prefix_ics_linear_transport_result_raw_pn ff_column_mcp_prefix_ics_linear_transport_result_raw_pn ff_value_mcp_prefix_ics_linear_transport_result_raw_pn. ((ff_index_mcp_prefix_ics_linear_transport_result_raw_pn) = (1) * ff_row_mcp_prefix_ics_linear_transport_result_raw_pn + ff_column_mcp_prefix_ics_linear_transport_result_raw_pn /\ ((exists mcp_gap_ics_linear_transport_result_raw_pn_column. mcp_gap_ics_linear_transport_result_raw_pn_column + S (ff_column_mcp_prefix_ics_linear_transport_result_raw_pn) = (1)) /\ ((exists ff_left_mcp_cell_ics_linear_transport_result_raw_pn_cell ff_left_scale_mcp_cell_ics_linear_transport_result_raw_pn_cell ff_right_mcp_cell_ics_linear_transport_result_raw_pn_cell ff_right_scale_mcp_cell_ics_linear_transport_result_raw_pn_cell. ((forall ff_index_mcp_ics_linear_transport_result_raw_pn_cell_row ff_source_mcp_ics_linear_transport_result_raw_pn_cell_row ff_target_mcp_ics_linear_transport_result_raw_pn_cell_row. (exists mcp_gap_ics_linear_transport_result_raw_pn_cell_row_bound. mcp_gap_ics_linear_transport_result_raw_pn_cell_row_bound + S (ff_index_mcp_ics_linear_transport_result_raw_pn_cell_row) = (w)) -> (((exists fs_h_mcp_ics_linear_transport_result_raw_pn_cell_row_source. fs_h_mcp_ics_linear_transport_result_raw_pn_cell_row_source + S (ff_source_mcp_ics_linear_transport_result_raw_pn_cell_row) = S ((S (((ff_row_mcp_prefix_ics_linear_transport_result_raw_pn) * (w)) + (1) * ff_index_mcp_ics_linear_transport_result_raw_pn_cell_row)) * ac)) /\ exists fs_q_mcp_ics_linear_transport_result_raw_pn_cell_row_source. ab = fs_q_mcp_ics_linear_transport_result_raw_pn_cell_row_source * S ((S (((ff_row_mcp_prefix_ics_linear_transport_result_raw_pn) * (w)) + (1) * ff_index_mcp_ics_linear_transport_result_raw_pn_cell_row)) * ac) + (ff_source_mcp_ics_linear_transport_result_raw_pn_cell_row))) -> (((exists fs_h_mcp_ics_linear_transport_result_raw_pn_cell_row_target. fs_h_mcp_ics_linear_transport_result_raw_pn_cell_row_target + S (ff_target_mcp_ics_linear_transport_result_raw_pn_cell_row) = S ((S (ff_index_mcp_ics_linear_transport_result_raw_pn_cell_row)) * ff_left_scale_mcp_cell_ics_linear_transport_result_raw_pn_cell)) /\ exists fs_q_mcp_ics_linear_transport_result_raw_pn_cell_row_target. ff_left_mcp_cell_ics_linear_transport_result_raw_pn_cell = fs_q_mcp_ics_linear_transport_result_raw_pn_cell_row_target * S ((S (ff_index_mcp_ics_linear_transport_result_raw_pn_cell_row)) * ff_left_scale_mcp_cell_ics_linear_transport_result_raw_pn_cell) + (ff_target_mcp_ics_linear_transport_result_raw_pn_cell_row))) -> ff_target_mcp_ics_linear_transport_result_raw_pn_cell_row = ff_source_mcp_ics_linear_transport_result_raw_pn_cell_row) /\ ((forall ff_index_mcp_ics_linear_transport_result_raw_pn_cell_column ff_source_mcp_ics_linear_transport_result_raw_pn_cell_column ff_target_mcp_ics_linear_transport_result_raw_pn_cell_column. (exists mcp_gap_ics_linear_transport_result_raw_pn_cell_column_bound. mcp_gap_ics_linear_transport_result_raw_pn_cell_column_bound + S (ff_index_mcp_ics_linear_transport_result_raw_pn_cell_column) = (w)) -> (((exists fs_h_mcp_ics_linear_transport_result_raw_pn_cell_column_source. fs_h_mcp_ics_linear_transport_result_raw_pn_cell_column_source + S (ff_source_mcp_ics_linear_transport_result_raw_pn_cell_column) = S ((S ((ff_column_mcp_prefix_ics_linear_transport_result_raw_pn) + (1) * ff_index_mcp_ics_linear_transport_result_raw_pn_cell_column)) * fc)) /\ exists fs_q_mcp_ics_linear_transport_result_raw_pn_cell_column_source. fb = fs_q_mcp_ics_linear_transport_result_raw_pn_cell_column_source * S ((S ((ff_column_mcp_prefix_ics_linear_transport_result_raw_pn) + (1) * ff_index_mcp_ics_linear_transport_result_raw_pn_cell_column)) * fc) + (ff_source_mcp_ics_linear_transport_result_raw_pn_cell_column))) -> (((exists fs_h_mcp_ics_linear_transport_result_raw_pn_cell_column_target. fs_h_mcp_ics_linear_transport_result_raw_pn_cell_column_target + S (ff_target_mcp_ics_linear_transport_result_raw_pn_cell_column) = S ((S (ff_index_mcp_ics_linear_transport_result_raw_pn_cell_column)) * ff_right_scale_mcp_cell_ics_linear_transport_result_raw_pn_cell)) /\ exists fs_q_mcp_ics_linear_transport_result_raw_pn_cell_column_target. ff_right_mcp_cell_ics_linear_transport_result_raw_pn_cell = fs_q_mcp_ics_linear_transport_result_raw_pn_cell_column_target * S ((S (ff_index_mcp_ics_linear_transport_result_raw_pn_cell_column)) * ff_right_scale_mcp_cell_ics_linear_transport_result_raw_pn_cell) + (ff_target_mcp_ics_linear_transport_result_raw_pn_cell_column))) -> ff_target_mcp_ics_linear_transport_result_raw_pn_cell_column = ff_source_mcp_ics_linear_transport_result_raw_pn_cell_column) /\ (exists ff_code_dot_mcp_ics_linear_transport_result_raw_pn_cell_dot ff_scale_dot_mcp_ics_linear_transport_result_raw_pn_cell_dot. ((forall fpmp_index_dot_mcp_ics_linear_transport_result_raw_pn_cell_dot_pointwise fpmp_left_dot_mcp_ics_linear_transport_result_raw_pn_cell_dot_pointwise fpmp_right_dot_mcp_ics_linear_transport_result_raw_pn_cell_dot_pointwise fpmp_target_dot_mcp_ics_linear_transport_result_raw_pn_cell_dot_pointwise. (exists fpmp_gap_dot_mcp_ics_linear_transport_result_raw_pn_cell_dot_pointwise. fpmp_gap_dot_mcp_ics_linear_transport_result_raw_pn_cell_dot_pointwise + S fpmp_index_dot_mcp_ics_linear_transport_result_raw_pn_cell_dot_pointwise = w) -> (((exists ff_h_fpmp_dot_mcp_ics_linear_transport_result_raw_pn_cell_dot_pointwise_left. ff_h_fpmp_dot_mcp_ics_linear_transport_result_raw_pn_cell_dot_pointwise_left + S (fpmp_left_dot_mcp_ics_linear_transport_result_raw_pn_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_linear_transport_result_raw_pn_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_linear_transport_result_raw_pn_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_linear_transport_result_raw_pn_cell_dot_pointwise_left. ff_left_mcp_cell_ics_linear_transport_result_raw_pn_cell = ff_q_fpmp_dot_mcp_ics_linear_transport_result_raw_pn_cell_dot_pointwise_left * S ((S (fpmp_index_dot_mcp_ics_linear_transport_result_raw_pn_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_linear_transport_result_raw_pn_cell) + (fpmp_left_dot_mcp_ics_linear_transport_result_raw_pn_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_linear_transport_result_raw_pn_cell_dot_pointwise_right. ff_h_fpmp_dot_mcp_ics_linear_transport_result_raw_pn_cell_dot_pointwise_right + S (fpmp_right_dot_mcp_ics_linear_transport_result_raw_pn_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_linear_transport_result_raw_pn_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_linear_transport_result_raw_pn_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_linear_transport_result_raw_pn_cell_dot_pointwise_right. ff_right_mcp_cell_ics_linear_transport_result_raw_pn_cell = ff_q_fpmp_dot_mcp_ics_linear_transport_result_raw_pn_cell_dot_pointwise_right * S ((S (fpmp_index_dot_mcp_ics_linear_transport_result_raw_pn_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_linear_transport_result_raw_pn_cell) + (fpmp_right_dot_mcp_ics_linear_transport_result_raw_pn_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_linear_transport_result_raw_pn_cell_dot_pointwise_target. ff_h_fpmp_dot_mcp_ics_linear_transport_result_raw_pn_cell_dot_pointwise_target + S (fpmp_target_dot_mcp_ics_linear_transport_result_raw_pn_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_linear_transport_result_raw_pn_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_linear_transport_result_raw_pn_cell_dot)) /\ exists ff_q_fpmp_dot_mcp_ics_linear_transport_result_raw_pn_cell_dot_pointwise_target. ff_code_dot_mcp_ics_linear_transport_result_raw_pn_cell_dot = ff_q_fpmp_dot_mcp_ics_linear_transport_result_raw_pn_cell_dot_pointwise_target * S ((S (fpmp_index_dot_mcp_ics_linear_transport_result_raw_pn_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_linear_transport_result_raw_pn_cell_dot) + (fpmp_target_dot_mcp_ics_linear_transport_result_raw_pn_cell_dot_pointwise))) -> fpmp_target_dot_mcp_ics_linear_transport_result_raw_pn_cell_dot_pointwise = fpmp_left_dot_mcp_ics_linear_transport_result_raw_pn_cell_dot_pointwise * fpmp_right_dot_mcp_ics_linear_transport_result_raw_pn_cell_dot_pointwise) /\ (exists ff_u_dot_mcp_ics_linear_transport_result_raw_pn_cell_dot_sum ff_v_dot_mcp_ics_linear_transport_result_raw_pn_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_linear_transport_result_raw_pn_cell_dot_sum_start. ff_h_dot_mcp_ics_linear_transport_result_raw_pn_cell_dot_sum_start + S (0) = S ((S (0)) * ff_v_dot_mcp_ics_linear_transport_result_raw_pn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_linear_transport_result_raw_pn_cell_dot_sum_start. ff_u_dot_mcp_ics_linear_transport_result_raw_pn_cell_dot_sum = ff_q_dot_mcp_ics_linear_transport_result_raw_pn_cell_dot_sum_start * S ((S (0)) * ff_v_dot_mcp_ics_linear_transport_result_raw_pn_cell_dot_sum) + (0))) /\ ((((exists ff_h_dot_mcp_ics_linear_transport_result_raw_pn_cell_dot_sum_terminal. ff_h_dot_mcp_ics_linear_transport_result_raw_pn_cell_dot_sum_terminal + S (ff_value_mcp_prefix_ics_linear_transport_result_raw_pn) = S ((S (w)) * ff_v_dot_mcp_ics_linear_transport_result_raw_pn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_linear_transport_result_raw_pn_cell_dot_sum_terminal. ff_u_dot_mcp_ics_linear_transport_result_raw_pn_cell_dot_sum = ff_q_dot_mcp_ics_linear_transport_result_raw_pn_cell_dot_sum_terminal * S ((S (w)) * ff_v_dot_mcp_ics_linear_transport_result_raw_pn_cell_dot_sum) + (ff_value_mcp_prefix_ics_linear_transport_result_raw_pn))) /\ forall ff_i_dot_mcp_ics_linear_transport_result_raw_pn_cell_dot_sum. (exists ff_lt_dot_mcp_ics_linear_transport_result_raw_pn_cell_dot_sum_bound. ff_lt_dot_mcp_ics_linear_transport_result_raw_pn_cell_dot_sum_bound + S ff_i_dot_mcp_ics_linear_transport_result_raw_pn_cell_dot_sum = w) -> exists ff_a_dot_mcp_ics_linear_transport_result_raw_pn_cell_dot_sum ff_r_dot_mcp_ics_linear_transport_result_raw_pn_cell_dot_sum ff_s_dot_mcp_ics_linear_transport_result_raw_pn_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_linear_transport_result_raw_pn_cell_dot_sum_summand. ff_h_dot_mcp_ics_linear_transport_result_raw_pn_cell_dot_sum_summand + S (ff_a_dot_mcp_ics_linear_transport_result_raw_pn_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_linear_transport_result_raw_pn_cell_dot_sum)) * ff_scale_dot_mcp_ics_linear_transport_result_raw_pn_cell_dot)) /\ exists ff_q_dot_mcp_ics_linear_transport_result_raw_pn_cell_dot_sum_summand. ff_code_dot_mcp_ics_linear_transport_result_raw_pn_cell_dot = ff_q_dot_mcp_ics_linear_transport_result_raw_pn_cell_dot_sum_summand * S ((S (ff_i_dot_mcp_ics_linear_transport_result_raw_pn_cell_dot_sum)) * ff_scale_dot_mcp_ics_linear_transport_result_raw_pn_cell_dot) + (ff_a_dot_mcp_ics_linear_transport_result_raw_pn_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_linear_transport_result_raw_pn_cell_dot_sum_partial. ff_h_dot_mcp_ics_linear_transport_result_raw_pn_cell_dot_sum_partial + S (ff_r_dot_mcp_ics_linear_transport_result_raw_pn_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_linear_transport_result_raw_pn_cell_dot_sum)) * ff_v_dot_mcp_ics_linear_transport_result_raw_pn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_linear_transport_result_raw_pn_cell_dot_sum_partial. ff_u_dot_mcp_ics_linear_transport_result_raw_pn_cell_dot_sum = ff_q_dot_mcp_ics_linear_transport_result_raw_pn_cell_dot_sum_partial * S ((S (ff_i_dot_mcp_ics_linear_transport_result_raw_pn_cell_dot_sum)) * ff_v_dot_mcp_ics_linear_transport_result_raw_pn_cell_dot_sum) + (ff_r_dot_mcp_ics_linear_transport_result_raw_pn_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_linear_transport_result_raw_pn_cell_dot_sum_successor. ff_h_dot_mcp_ics_linear_transport_result_raw_pn_cell_dot_sum_successor + S (ff_s_dot_mcp_ics_linear_transport_result_raw_pn_cell_dot_sum) = S ((S (S ff_i_dot_mcp_ics_linear_transport_result_raw_pn_cell_dot_sum)) * ff_v_dot_mcp_ics_linear_transport_result_raw_pn_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_linear_transport_result_raw_pn_cell_dot_sum_successor. ff_u_dot_mcp_ics_linear_transport_result_raw_pn_cell_dot_sum = ff_q_dot_mcp_ics_linear_transport_result_raw_pn_cell_dot_sum_successor * S ((S (S ff_i_dot_mcp_ics_linear_transport_result_raw_pn_cell_dot_sum)) * ff_v_dot_mcp_ics_linear_transport_result_raw_pn_cell_dot_sum) + (ff_s_dot_mcp_ics_linear_transport_result_raw_pn_cell_dot_sum))) /\ ff_s_dot_mcp_ics_linear_transport_result_raw_pn_cell_dot_sum = ff_r_dot_mcp_ics_linear_transport_result_raw_pn_cell_dot_sum + ff_a_dot_mcp_ics_linear_transport_result_raw_pn_cell_dot_sum))))))))))) /\ (((exists fs_h_mcp_ics_linear_transport_result_raw_pn_entry. fs_h_mcp_ics_linear_transport_result_raw_pn_entry + S (ff_value_mcp_prefix_ics_linear_transport_result_raw_pn) = S ((S (ff_index_mcp_prefix_ics_linear_transport_result_raw_pn)) * ff_pns_mcp_smatrix_ics_linear_transport_result_raw)) /\ exists fs_q_mcp_ics_linear_transport_result_raw_pn_entry. ff_pn_mcp_smatrix_ics_linear_transport_result_raw = fs_q_mcp_ics_linear_transport_result_raw_pn_entry * S ((S (ff_index_mcp_prefix_ics_linear_transport_result_raw_pn)) * ff_pns_mcp_smatrix_ics_linear_transport_result_raw) + (ff_value_mcp_prefix_ics_linear_transport_result_raw_pn))))))) /\ ((forall ff_index_mcp_prefix_ics_linear_transport_result_raw_np. (exists mcp_gap_ics_linear_transport_result_raw_np_index. mcp_gap_ics_linear_transport_result_raw_np_index + S (ff_index_mcp_prefix_ics_linear_transport_result_raw_np) = ((r) * (1))) -> exists ff_row_mcp_prefix_ics_linear_transport_result_raw_np ff_column_mcp_prefix_ics_linear_transport_result_raw_np ff_value_mcp_prefix_ics_linear_transport_result_raw_np. ((ff_index_mcp_prefix_ics_linear_transport_result_raw_np) = (1) * ff_row_mcp_prefix_ics_linear_transport_result_raw_np + ff_column_mcp_prefix_ics_linear_transport_result_raw_np /\ ((exists mcp_gap_ics_linear_transport_result_raw_np_column. mcp_gap_ics_linear_transport_result_raw_np_column + S (ff_column_mcp_prefix_ics_linear_transport_result_raw_np) = (1)) /\ ((exists ff_left_mcp_cell_ics_linear_transport_result_raw_np_cell ff_left_scale_mcp_cell_ics_linear_transport_result_raw_np_cell ff_right_mcp_cell_ics_linear_transport_result_raw_np_cell ff_right_scale_mcp_cell_ics_linear_transport_result_raw_np_cell. ((forall ff_index_mcp_ics_linear_transport_result_raw_np_cell_row ff_source_mcp_ics_linear_transport_result_raw_np_cell_row ff_target_mcp_ics_linear_transport_result_raw_np_cell_row. (exists mcp_gap_ics_linear_transport_result_raw_np_cell_row_bound. mcp_gap_ics_linear_transport_result_raw_np_cell_row_bound + S (ff_index_mcp_ics_linear_transport_result_raw_np_cell_row) = (w)) -> (((exists fs_h_mcp_ics_linear_transport_result_raw_np_cell_row_source. fs_h_mcp_ics_linear_transport_result_raw_np_cell_row_source + S (ff_source_mcp_ics_linear_transport_result_raw_np_cell_row) = S ((S (((ff_row_mcp_prefix_ics_linear_transport_result_raw_np) * (w)) + (1) * ff_index_mcp_ics_linear_transport_result_raw_np_cell_row)) * dc)) /\ exists fs_q_mcp_ics_linear_transport_result_raw_np_cell_row_source. db = fs_q_mcp_ics_linear_transport_result_raw_np_cell_row_source * S ((S (((ff_row_mcp_prefix_ics_linear_transport_result_raw_np) * (w)) + (1) * ff_index_mcp_ics_linear_transport_result_raw_np_cell_row)) * dc) + (ff_source_mcp_ics_linear_transport_result_raw_np_cell_row))) -> (((exists fs_h_mcp_ics_linear_transport_result_raw_np_cell_row_target. fs_h_mcp_ics_linear_transport_result_raw_np_cell_row_target + S (ff_target_mcp_ics_linear_transport_result_raw_np_cell_row) = S ((S (ff_index_mcp_ics_linear_transport_result_raw_np_cell_row)) * ff_left_scale_mcp_cell_ics_linear_transport_result_raw_np_cell)) /\ exists fs_q_mcp_ics_linear_transport_result_raw_np_cell_row_target. ff_left_mcp_cell_ics_linear_transport_result_raw_np_cell = fs_q_mcp_ics_linear_transport_result_raw_np_cell_row_target * S ((S (ff_index_mcp_ics_linear_transport_result_raw_np_cell_row)) * ff_left_scale_mcp_cell_ics_linear_transport_result_raw_np_cell) + (ff_target_mcp_ics_linear_transport_result_raw_np_cell_row))) -> ff_target_mcp_ics_linear_transport_result_raw_np_cell_row = ff_source_mcp_ics_linear_transport_result_raw_np_cell_row) /\ ((forall ff_index_mcp_ics_linear_transport_result_raw_np_cell_column ff_source_mcp_ics_linear_transport_result_raw_np_cell_column ff_target_mcp_ics_linear_transport_result_raw_np_cell_column. (exists mcp_gap_ics_linear_transport_result_raw_np_cell_column_bound. mcp_gap_ics_linear_transport_result_raw_np_cell_column_bound + S (ff_index_mcp_ics_linear_transport_result_raw_np_cell_column) = (w)) -> (((exists fs_h_mcp_ics_linear_transport_result_raw_np_cell_column_source. fs_h_mcp_ics_linear_transport_result_raw_np_cell_column_source + S (ff_source_mcp_ics_linear_transport_result_raw_np_cell_column) = S ((S ((ff_column_mcp_prefix_ics_linear_transport_result_raw_np) + (1) * ff_index_mcp_ics_linear_transport_result_raw_np_cell_column)) * ec)) /\ exists fs_q_mcp_ics_linear_transport_result_raw_np_cell_column_source. eb = fs_q_mcp_ics_linear_transport_result_raw_np_cell_column_source * S ((S ((ff_column_mcp_prefix_ics_linear_transport_result_raw_np) + (1) * ff_index_mcp_ics_linear_transport_result_raw_np_cell_column)) * ec) + (ff_source_mcp_ics_linear_transport_result_raw_np_cell_column))) -> (((exists fs_h_mcp_ics_linear_transport_result_raw_np_cell_column_target. fs_h_mcp_ics_linear_transport_result_raw_np_cell_column_target + S (ff_target_mcp_ics_linear_transport_result_raw_np_cell_column) = S ((S (ff_index_mcp_ics_linear_transport_result_raw_np_cell_column)) * ff_right_scale_mcp_cell_ics_linear_transport_result_raw_np_cell)) /\ exists fs_q_mcp_ics_linear_transport_result_raw_np_cell_column_target. ff_right_mcp_cell_ics_linear_transport_result_raw_np_cell = fs_q_mcp_ics_linear_transport_result_raw_np_cell_column_target * S ((S (ff_index_mcp_ics_linear_transport_result_raw_np_cell_column)) * ff_right_scale_mcp_cell_ics_linear_transport_result_raw_np_cell) + (ff_target_mcp_ics_linear_transport_result_raw_np_cell_column))) -> ff_target_mcp_ics_linear_transport_result_raw_np_cell_column = ff_source_mcp_ics_linear_transport_result_raw_np_cell_column) /\ (exists ff_code_dot_mcp_ics_linear_transport_result_raw_np_cell_dot ff_scale_dot_mcp_ics_linear_transport_result_raw_np_cell_dot. ((forall fpmp_index_dot_mcp_ics_linear_transport_result_raw_np_cell_dot_pointwise fpmp_left_dot_mcp_ics_linear_transport_result_raw_np_cell_dot_pointwise fpmp_right_dot_mcp_ics_linear_transport_result_raw_np_cell_dot_pointwise fpmp_target_dot_mcp_ics_linear_transport_result_raw_np_cell_dot_pointwise. (exists fpmp_gap_dot_mcp_ics_linear_transport_result_raw_np_cell_dot_pointwise. fpmp_gap_dot_mcp_ics_linear_transport_result_raw_np_cell_dot_pointwise + S fpmp_index_dot_mcp_ics_linear_transport_result_raw_np_cell_dot_pointwise = w) -> (((exists ff_h_fpmp_dot_mcp_ics_linear_transport_result_raw_np_cell_dot_pointwise_left. ff_h_fpmp_dot_mcp_ics_linear_transport_result_raw_np_cell_dot_pointwise_left + S (fpmp_left_dot_mcp_ics_linear_transport_result_raw_np_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_linear_transport_result_raw_np_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_linear_transport_result_raw_np_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_linear_transport_result_raw_np_cell_dot_pointwise_left. ff_left_mcp_cell_ics_linear_transport_result_raw_np_cell = ff_q_fpmp_dot_mcp_ics_linear_transport_result_raw_np_cell_dot_pointwise_left * S ((S (fpmp_index_dot_mcp_ics_linear_transport_result_raw_np_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_linear_transport_result_raw_np_cell) + (fpmp_left_dot_mcp_ics_linear_transport_result_raw_np_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_linear_transport_result_raw_np_cell_dot_pointwise_right. ff_h_fpmp_dot_mcp_ics_linear_transport_result_raw_np_cell_dot_pointwise_right + S (fpmp_right_dot_mcp_ics_linear_transport_result_raw_np_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_linear_transport_result_raw_np_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_linear_transport_result_raw_np_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_linear_transport_result_raw_np_cell_dot_pointwise_right. ff_right_mcp_cell_ics_linear_transport_result_raw_np_cell = ff_q_fpmp_dot_mcp_ics_linear_transport_result_raw_np_cell_dot_pointwise_right * S ((S (fpmp_index_dot_mcp_ics_linear_transport_result_raw_np_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_linear_transport_result_raw_np_cell) + (fpmp_right_dot_mcp_ics_linear_transport_result_raw_np_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_linear_transport_result_raw_np_cell_dot_pointwise_target. ff_h_fpmp_dot_mcp_ics_linear_transport_result_raw_np_cell_dot_pointwise_target + S (fpmp_target_dot_mcp_ics_linear_transport_result_raw_np_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_linear_transport_result_raw_np_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_linear_transport_result_raw_np_cell_dot)) /\ exists ff_q_fpmp_dot_mcp_ics_linear_transport_result_raw_np_cell_dot_pointwise_target. ff_code_dot_mcp_ics_linear_transport_result_raw_np_cell_dot = ff_q_fpmp_dot_mcp_ics_linear_transport_result_raw_np_cell_dot_pointwise_target * S ((S (fpmp_index_dot_mcp_ics_linear_transport_result_raw_np_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_linear_transport_result_raw_np_cell_dot) + (fpmp_target_dot_mcp_ics_linear_transport_result_raw_np_cell_dot_pointwise))) -> fpmp_target_dot_mcp_ics_linear_transport_result_raw_np_cell_dot_pointwise = fpmp_left_dot_mcp_ics_linear_transport_result_raw_np_cell_dot_pointwise * fpmp_right_dot_mcp_ics_linear_transport_result_raw_np_cell_dot_pointwise) /\ (exists ff_u_dot_mcp_ics_linear_transport_result_raw_np_cell_dot_sum ff_v_dot_mcp_ics_linear_transport_result_raw_np_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_linear_transport_result_raw_np_cell_dot_sum_start. ff_h_dot_mcp_ics_linear_transport_result_raw_np_cell_dot_sum_start + S (0) = S ((S (0)) * ff_v_dot_mcp_ics_linear_transport_result_raw_np_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_linear_transport_result_raw_np_cell_dot_sum_start. ff_u_dot_mcp_ics_linear_transport_result_raw_np_cell_dot_sum = ff_q_dot_mcp_ics_linear_transport_result_raw_np_cell_dot_sum_start * S ((S (0)) * ff_v_dot_mcp_ics_linear_transport_result_raw_np_cell_dot_sum) + (0))) /\ ((((exists ff_h_dot_mcp_ics_linear_transport_result_raw_np_cell_dot_sum_terminal. ff_h_dot_mcp_ics_linear_transport_result_raw_np_cell_dot_sum_terminal + S (ff_value_mcp_prefix_ics_linear_transport_result_raw_np) = S ((S (w)) * ff_v_dot_mcp_ics_linear_transport_result_raw_np_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_linear_transport_result_raw_np_cell_dot_sum_terminal. ff_u_dot_mcp_ics_linear_transport_result_raw_np_cell_dot_sum = ff_q_dot_mcp_ics_linear_transport_result_raw_np_cell_dot_sum_terminal * S ((S (w)) * ff_v_dot_mcp_ics_linear_transport_result_raw_np_cell_dot_sum) + (ff_value_mcp_prefix_ics_linear_transport_result_raw_np))) /\ forall ff_i_dot_mcp_ics_linear_transport_result_raw_np_cell_dot_sum. (exists ff_lt_dot_mcp_ics_linear_transport_result_raw_np_cell_dot_sum_bound. ff_lt_dot_mcp_ics_linear_transport_result_raw_np_cell_dot_sum_bound + S ff_i_dot_mcp_ics_linear_transport_result_raw_np_cell_dot_sum = w) -> exists ff_a_dot_mcp_ics_linear_transport_result_raw_np_cell_dot_sum ff_r_dot_mcp_ics_linear_transport_result_raw_np_cell_dot_sum ff_s_dot_mcp_ics_linear_transport_result_raw_np_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_linear_transport_result_raw_np_cell_dot_sum_summand. ff_h_dot_mcp_ics_linear_transport_result_raw_np_cell_dot_sum_summand + S (ff_a_dot_mcp_ics_linear_transport_result_raw_np_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_linear_transport_result_raw_np_cell_dot_sum)) * ff_scale_dot_mcp_ics_linear_transport_result_raw_np_cell_dot)) /\ exists ff_q_dot_mcp_ics_linear_transport_result_raw_np_cell_dot_sum_summand. ff_code_dot_mcp_ics_linear_transport_result_raw_np_cell_dot = ff_q_dot_mcp_ics_linear_transport_result_raw_np_cell_dot_sum_summand * S ((S (ff_i_dot_mcp_ics_linear_transport_result_raw_np_cell_dot_sum)) * ff_scale_dot_mcp_ics_linear_transport_result_raw_np_cell_dot) + (ff_a_dot_mcp_ics_linear_transport_result_raw_np_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_linear_transport_result_raw_np_cell_dot_sum_partial. ff_h_dot_mcp_ics_linear_transport_result_raw_np_cell_dot_sum_partial + S (ff_r_dot_mcp_ics_linear_transport_result_raw_np_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_linear_transport_result_raw_np_cell_dot_sum)) * ff_v_dot_mcp_ics_linear_transport_result_raw_np_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_linear_transport_result_raw_np_cell_dot_sum_partial. ff_u_dot_mcp_ics_linear_transport_result_raw_np_cell_dot_sum = ff_q_dot_mcp_ics_linear_transport_result_raw_np_cell_dot_sum_partial * S ((S (ff_i_dot_mcp_ics_linear_transport_result_raw_np_cell_dot_sum)) * ff_v_dot_mcp_ics_linear_transport_result_raw_np_cell_dot_sum) + (ff_r_dot_mcp_ics_linear_transport_result_raw_np_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_linear_transport_result_raw_np_cell_dot_sum_successor. ff_h_dot_mcp_ics_linear_transport_result_raw_np_cell_dot_sum_successor + S (ff_s_dot_mcp_ics_linear_transport_result_raw_np_cell_dot_sum) = S ((S (S ff_i_dot_mcp_ics_linear_transport_result_raw_np_cell_dot_sum)) * ff_v_dot_mcp_ics_linear_transport_result_raw_np_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_linear_transport_result_raw_np_cell_dot_sum_successor. ff_u_dot_mcp_ics_linear_transport_result_raw_np_cell_dot_sum = ff_q_dot_mcp_ics_linear_transport_result_raw_np_cell_dot_sum_successor * S ((S (S ff_i_dot_mcp_ics_linear_transport_result_raw_np_cell_dot_sum)) * ff_v_dot_mcp_ics_linear_transport_result_raw_np_cell_dot_sum) + (ff_s_dot_mcp_ics_linear_transport_result_raw_np_cell_dot_sum))) /\ ff_s_dot_mcp_ics_linear_transport_result_raw_np_cell_dot_sum = ff_r_dot_mcp_ics_linear_transport_result_raw_np_cell_dot_sum + ff_a_dot_mcp_ics_linear_transport_result_raw_np_cell_dot_sum))))))))))) /\ (((exists fs_h_mcp_ics_linear_transport_result_raw_np_entry. fs_h_mcp_ics_linear_transport_result_raw_np_entry + S (ff_value_mcp_prefix_ics_linear_transport_result_raw_np) = S ((S (ff_index_mcp_prefix_ics_linear_transport_result_raw_np)) * ff_nps_mcp_smatrix_ics_linear_transport_result_raw)) /\ exists fs_q_mcp_ics_linear_transport_result_raw_np_entry. ff_np_mcp_smatrix_ics_linear_transport_result_raw = fs_q_mcp_ics_linear_transport_result_raw_np_entry * S ((S (ff_index_mcp_prefix_ics_linear_transport_result_raw_np)) * ff_nps_mcp_smatrix_ics_linear_transport_result_raw) + (ff_value_mcp_prefix_ics_linear_transport_result_raw_np))))))) /\ ((forall ff_index_mcp_add_ics_linear_transport_result_raw_positive ff_left_mcp_add_ics_linear_transport_result_raw_positive ff_right_mcp_add_ics_linear_transport_result_raw_positive ff_target_mcp_add_ics_linear_transport_result_raw_positive. (exists mcp_gap_ics_linear_transport_result_raw_positive_bound. mcp_gap_ics_linear_transport_result_raw_positive_bound + S (ff_index_mcp_add_ics_linear_transport_result_raw_positive) = ((r) * (1))) -> (((exists fs_h_mcp_ics_linear_transport_result_raw_positive_left. fs_h_mcp_ics_linear_transport_result_raw_positive_left + S (ff_left_mcp_add_ics_linear_transport_result_raw_positive) = S ((S (ff_index_mcp_add_ics_linear_transport_result_raw_positive)) * ff_pps_mcp_smatrix_ics_linear_transport_result_raw)) /\ exists fs_q_mcp_ics_linear_transport_result_raw_positive_left. ff_pp_mcp_smatrix_ics_linear_transport_result_raw = fs_q_mcp_ics_linear_transport_result_raw_positive_left * S ((S (ff_index_mcp_add_ics_linear_transport_result_raw_positive)) * ff_pps_mcp_smatrix_ics_linear_transport_result_raw) + (ff_left_mcp_add_ics_linear_transport_result_raw_positive))) -> (((exists fs_h_mcp_ics_linear_transport_result_raw_positive_right. fs_h_mcp_ics_linear_transport_result_raw_positive_right + S (ff_right_mcp_add_ics_linear_transport_result_raw_positive) = S ((S (ff_index_mcp_add_ics_linear_transport_result_raw_positive)) * ff_nns_mcp_smatrix_ics_linear_transport_result_raw)) /\ exists fs_q_mcp_ics_linear_transport_result_raw_positive_right. ff_nn_mcp_smatrix_ics_linear_transport_result_raw = fs_q_mcp_ics_linear_transport_result_raw_positive_right * S ((S (ff_index_mcp_add_ics_linear_transport_result_raw_positive)) * ff_nns_mcp_smatrix_ics_linear_transport_result_raw) + (ff_right_mcp_add_ics_linear_transport_result_raw_positive))) -> (((exists fs_h_mcp_ics_linear_transport_result_raw_positive_target. fs_h_mcp_ics_linear_transport_result_raw_positive_target + S (ff_target_mcp_add_ics_linear_transport_result_raw_positive) = S ((S (ff_index_mcp_add_ics_linear_transport_result_raw_positive)) * ics_raw_positive_scale_linear_transport_result)) /\ exists fs_q_mcp_ics_linear_transport_result_raw_positive_target. ics_raw_positive_linear_transport_result = fs_q_mcp_ics_linear_transport_result_raw_positive_target * S ((S (ff_index_mcp_add_ics_linear_transport_result_raw_positive)) * ics_raw_positive_scale_linear_transport_result) + (ff_target_mcp_add_ics_linear_transport_result_raw_positive))) -> ff_target_mcp_add_ics_linear_transport_result_raw_positive = ff_left_mcp_add_ics_linear_transport_result_raw_positive + ff_right_mcp_add_ics_linear_transport_result_raw_positive) /\ (forall ff_index_mcp_add_ics_linear_transport_result_raw_negative ff_left_mcp_add_ics_linear_transport_result_raw_negative ff_right_mcp_add_ics_linear_transport_result_raw_negative ff_target_mcp_add_ics_linear_transport_result_raw_negative. (exists mcp_gap_ics_linear_transport_result_raw_negative_bound. mcp_gap_ics_linear_transport_result_raw_negative_bound + S (ff_index_mcp_add_ics_linear_transport_result_raw_negative) = ((r) * (1))) -> (((exists fs_h_mcp_ics_linear_transport_result_raw_negative_left. fs_h_mcp_ics_linear_transport_result_raw_negative_left + S (ff_left_mcp_add_ics_linear_transport_result_raw_negative) = S ((S (ff_index_mcp_add_ics_linear_transport_result_raw_negative)) * ff_pns_mcp_smatrix_ics_linear_transport_result_raw)) /\ exists fs_q_mcp_ics_linear_transport_result_raw_negative_left. ff_pn_mcp_smatrix_ics_linear_transport_result_raw = fs_q_mcp_ics_linear_transport_result_raw_negative_left * S ((S (ff_index_mcp_add_ics_linear_transport_result_raw_negative)) * ff_pns_mcp_smatrix_ics_linear_transport_result_raw) + (ff_left_mcp_add_ics_linear_transport_result_raw_negative))) -> (((exists fs_h_mcp_ics_linear_transport_result_raw_negative_right. fs_h_mcp_ics_linear_transport_result_raw_negative_right + S (ff_right_mcp_add_ics_linear_transport_result_raw_negative) = S ((S (ff_index_mcp_add_ics_linear_transport_result_raw_negative)) * ff_nps_mcp_smatrix_ics_linear_transport_result_raw)) /\ exists fs_q_mcp_ics_linear_transport_result_raw_negative_right. ff_np_mcp_smatrix_ics_linear_transport_result_raw = fs_q_mcp_ics_linear_transport_result_raw_negative_right * S ((S (ff_index_mcp_add_ics_linear_transport_result_raw_negative)) * ff_nps_mcp_smatrix_ics_linear_transport_result_raw) + (ff_right_mcp_add_ics_linear_transport_result_raw_negative))) -> (((exists fs_h_mcp_ics_linear_transport_result_raw_negative_target. fs_h_mcp_ics_linear_transport_result_raw_negative_target + S (ff_target_mcp_add_ics_linear_transport_result_raw_negative) = S ((S (ff_index_mcp_add_ics_linear_transport_result_raw_negative)) * ics_raw_negative_scale_linear_transport_result)) /\ exists fs_q_mcp_ics_linear_transport_result_raw_negative_target. ics_raw_negative_linear_transport_result = fs_q_mcp_ics_linear_transport_result_raw_negative_target * S ((S (ff_index_mcp_add_ics_linear_transport_result_raw_negative)) * ics_raw_negative_scale_linear_transport_result) + (ff_target_mcp_add_ics_linear_transport_result_raw_negative))) -> ff_target_mcp_add_ics_linear_transport_result_raw_negative = ff_left_mcp_add_ics_linear_transport_result_raw_negative + ff_right_mcp_add_ics_linear_transport_result_raw_negative))))))) /\ (forall ics_index_linear_transport_result_equal ics_value0_linear_transport_result_equal ics_value1_linear_transport_result_equal ics_value2_linear_transport_result_equal ics_value3_linear_transport_result_equal. (exists ics_gap_linear_transport_result_equal_bound. ics_gap_linear_transport_result_equal_bound + S (ics_index_linear_transport_result_equal) = (r)) -> (((exists fs_h_ics_linear_transport_result_equal_at0. fs_h_ics_linear_transport_result_equal_at0 + S (ics_value0_linear_transport_result_equal) = S ((S (ics_index_linear_transport_result_equal)) * ics_raw_positive_scale_linear_transport_result)) /\ exists fs_q_ics_linear_transport_result_equal_at0. ics_raw_positive_linear_transport_result = fs_q_ics_linear_transport_result_equal_at0 * S ((S (ics_index_linear_transport_result_equal)) * ics_raw_positive_scale_linear_transport_result) + (ics_value0_linear_transport_result_equal))) -> (((exists fs_h_ics_linear_transport_result_equal_at1. fs_h_ics_linear_transport_result_equal_at1 + S (ics_value1_linear_transport_result_equal) = S ((S (ics_index_linear_transport_result_equal)) * ics_raw_negative_scale_linear_transport_result)) /\ exists fs_q_ics_linear_transport_result_equal_at1. ics_raw_negative_linear_transport_result = fs_q_ics_linear_transport_result_equal_at1 * S ((S (ics_index_linear_transport_result_equal)) * ics_raw_negative_scale_linear_transport_result) + (ics_value1_linear_transport_result_equal))) -> (((exists fs_h_ics_linear_transport_result_equal_at2. fs_h_ics_linear_transport_result_equal_at2 + S (ics_value2_linear_transport_result_equal) = S ((S (ics_index_linear_transport_result_equal)) * qc)) /\ exists fs_q_ics_linear_transport_result_equal_at2. qb = fs_q_ics_linear_transport_result_equal_at2 * S ((S (ics_index_linear_transport_result_equal)) * qc) + (ics_value2_linear_transport_result_equal))) -> (((exists fs_h_ics_linear_transport_result_equal_at3. fs_h_ics_linear_transport_result_equal_at3 + S (ics_value3_linear_transport_result_equal) = S ((S (ics_index_linear_transport_result_equal)) * mc)) /\ exists fs_q_ics_linear_transport_result_equal_at3. mb = fs_q_ics_linear_transport_result_equal_at3 * S ((S (ics_index_linear_transport_result_equal)) * mc) + (ics_value3_linear_transport_result_equal))) -> ics_value0_linear_transport_result_equal + ics_value3_linear_transport_result_equal = ics_value2_linear_transport_result_equal + ics_value1_linear_transport_result_equal))))Complete tactic proof in conservative notation
All 47 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.
Read the argument
Proof checkpoints
47 script commands · 7 reading checkpoints · 0 local claims
This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.
Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.
Named ingredients (1)
01Fix variables and assumptionsL1–10
02Fix variables and assumptionsL11–20
03Separate the logical casesL21–25
04Construct an explicit witnessL26–29
05Separate the logical casesL30–30
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L30
split
06Use earlier factsL31–40
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L31
exact himage_witness_witness_witness_witness_left - L32
specialize integer_vector_equal_transitive (x) - L33
specialize integer_vector_equal_transitive (x1) - L34
specialize integer_vector_equal_transitive (x2) - L35
specialize integer_vector_equal_transitive (x3) - L36
specialize integer_vector_equal_transitive (pb) - L37
specialize integer_vector_equal_transitive (pc) - L38
specialize integer_vector_equal_transitive (nb) - L39
specialize integer_vector_equal_transitive (nc) - L40
specialize integer_vector_equal_transitive (qb)
07Use earlier factsL41–47
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L41
specialize integer_vector_equal_transitive (qc) - L42
specialize integer_vector_equal_transitive (mb) - L43
specialize integer_vector_equal_transitive (mc) - L44
specialize integer_vector_equal_transitive (r) - L45
apply integer_vector_equal_transitive - L46
exact himage_witness_witness_witness_witness_right - L47
exact hequal
Original defined command ledger · 47 lines
- 0001
intro ab - 0002
intro ac - 0003
intro db - 0004
intro dc - 0005
intro eb - 0006
intro ec - 0007
intro fb - 0008
intro fc - 0009
intro w - 0010
intro r - 0011
intro pb - 0012
intro pc - 0013
intro nb - 0014
intro nc - 0015
intro qb - 0016
intro qc - 0017
intro mb - 0018
intro mc - 0019
intro himage - 0020
intro hequal - 0021
cases himage - 0022
cases himage_witness - 0023
cases himage_witness_witness - 0024
cases himage_witness_witness_witness - 0025
cases himage_witness_witness_witness_witness - 0026
exists x - 0027
exists x1 - 0028
exists x2 - 0029
exists x3 - 0030
split - 0031
exact himage_witness_witness_witness_witness_left - 0032
specialize integer_vector_equal_transitive (x) - 0033
specialize integer_vector_equal_transitive (x1) - 0034
specialize integer_vector_equal_transitive (x2) - 0035
specialize integer_vector_equal_transitive (x3) - 0036
specialize integer_vector_equal_transitive (pb) - 0037
specialize integer_vector_equal_transitive (pc) - 0038
specialize integer_vector_equal_transitive (nb) - 0039
specialize integer_vector_equal_transitive (nc) - 0040
specialize integer_vector_equal_transitive (qb) - 0041
specialize integer_vector_equal_transitive (qc) - 0042
specialize integer_vector_equal_transitive (mb) - 0043
specialize integer_vector_equal_transitive (mc) - 0044
specialize integer_vector_equal_transitive (r) - 0045
apply integer_vector_equal_transitive - 0046
exact himage_witness_witness_witness_witness_right - 0047
exact hequal