integer_span_natural_product_add_right

Exact expanded first-order arithmetic statement

forall ab ac bb bc cb cc db dc w pb pc qb qc rb rc l. (forall ff_index_mcp_add_ics_product_coeff_add ff_left_mcp_add_ics_product_coeff_add ff_right_mcp_add_ics_product_coeff_add ff_target_mcp_add_ics_product_coeff_add. (exists mcp_gap_ics_product_coeff_add_bound. mcp_gap_ics_product_coeff_add_bound + S (ff_index_mcp_add_ics_product_coeff_add) = (w)) -> (((exists fs_h_mcp_ics_product_coeff_add_left. fs_h_mcp_ics_product_coeff_add_left + S (ff_left_mcp_add_ics_product_coeff_add) = S ((S (ff_index_mcp_add_ics_product_coeff_add)) * bc)) /\ exists fs_q_mcp_ics_product_coeff_add_left. bb = fs_q_mcp_ics_product_coeff_add_left * S ((S (ff_index_mcp_add_ics_product_coeff_add)) * bc) + (ff_left_mcp_add_ics_product_coeff_add))) -> (((exists fs_h_mcp_ics_product_coeff_add_right. fs_h_mcp_ics_product_coeff_add_right + S (ff_right_mcp_add_ics_product_coeff_add) = S ((S (ff_index_mcp_add_ics_product_coeff_add)) * cc)) /\ exists fs_q_mcp_ics_product_coeff_add_right. cb = fs_q_mcp_ics_product_coeff_add_right * S ((S (ff_index_mcp_add_ics_product_coeff_add)) * cc) + (ff_right_mcp_add_ics_product_coeff_add))) -> (((exists fs_h_mcp_ics_product_coeff_add_target. fs_h_mcp_ics_product_coeff_add_target + S (ff_target_mcp_add_ics_product_coeff_add) = S ((S (ff_index_mcp_add_ics_product_coeff_add)) * dc)) /\ exists fs_q_mcp_ics_product_coeff_add_target. db = fs_q_mcp_ics_product_coeff_add_target * S ((S (ff_index_mcp_add_ics_product_coeff_add)) * dc) + (ff_target_mcp_add_ics_product_coeff_add))) -> ff_target_mcp_add_ics_product_coeff_add = ff_left_mcp_add_ics_product_coeff_add + ff_right_mcp_add_ics_product_coeff_add) -> (forall ff_index_mcp_prefix_ics_product_first. (exists mcp_gap_ics_product_first_index. mcp_gap_ics_product_first_index + S (ff_index_mcp_prefix_ics_product_first) = (l)) -> exists ff_row_mcp_prefix_ics_product_first ff_column_mcp_prefix_ics_product_first ff_value_mcp_prefix_ics_product_first. ((ff_index_mcp_prefix_ics_product_first) = (1) * ff_row_mcp_prefix_ics_product_first + ff_column_mcp_prefix_ics_product_first /\ ((exists mcp_gap_ics_product_first_column. mcp_gap_ics_product_first_column + S (ff_column_mcp_prefix_ics_product_first) = (1)) /\ ((exists ff_left_mcp_cell_ics_product_first_cell ff_left_scale_mcp_cell_ics_product_first_cell ff_right_mcp_cell_ics_product_first_cell ff_right_scale_mcp_cell_ics_product_first_cell. ((forall ff_index_mcp_ics_product_first_cell_row ff_source_mcp_ics_product_first_cell_row ff_target_mcp_ics_product_first_cell_row. (exists mcp_gap_ics_product_first_cell_row_bound. mcp_gap_ics_product_first_cell_row_bound + S (ff_index_mcp_ics_product_first_cell_row) = (w)) -> (((exists fs_h_mcp_ics_product_first_cell_row_source. fs_h_mcp_ics_product_first_cell_row_source + S (ff_source_mcp_ics_product_first_cell_row) = S ((S (((ff_row_mcp_prefix_ics_product_first) * (w)) + (1) * ff_index_mcp_ics_product_first_cell_row)) * ac)) /\ exists fs_q_mcp_ics_product_first_cell_row_source. ab = fs_q_mcp_ics_product_first_cell_row_source * S ((S (((ff_row_mcp_prefix_ics_product_first) * (w)) + (1) * ff_index_mcp_ics_product_first_cell_row)) * ac) + (ff_source_mcp_ics_product_first_cell_row))) -> (((exists fs_h_mcp_ics_product_first_cell_row_target. fs_h_mcp_ics_product_first_cell_row_target + S (ff_target_mcp_ics_product_first_cell_row) = S ((S (ff_index_mcp_ics_product_first_cell_row)) * ff_left_scale_mcp_cell_ics_product_first_cell)) /\ exists fs_q_mcp_ics_product_first_cell_row_target. ff_left_mcp_cell_ics_product_first_cell = fs_q_mcp_ics_product_first_cell_row_target * S ((S (ff_index_mcp_ics_product_first_cell_row)) * ff_left_scale_mcp_cell_ics_product_first_cell) + (ff_target_mcp_ics_product_first_cell_row))) -> ff_target_mcp_ics_product_first_cell_row = ff_source_mcp_ics_product_first_cell_row) /\ ((forall ff_index_mcp_ics_product_first_cell_column ff_source_mcp_ics_product_first_cell_column ff_target_mcp_ics_product_first_cell_column. (exists mcp_gap_ics_product_first_cell_column_bound. mcp_gap_ics_product_first_cell_column_bound + S (ff_index_mcp_ics_product_first_cell_column) = (w)) -> (((exists fs_h_mcp_ics_product_first_cell_column_source. fs_h_mcp_ics_product_first_cell_column_source + S (ff_source_mcp_ics_product_first_cell_column) = S ((S ((ff_column_mcp_prefix_ics_product_first) + (1) * ff_index_mcp_ics_product_first_cell_column)) * bc)) /\ exists fs_q_mcp_ics_product_first_cell_column_source. bb = fs_q_mcp_ics_product_first_cell_column_source * S ((S ((ff_column_mcp_prefix_ics_product_first) + (1) * ff_index_mcp_ics_product_first_cell_column)) * bc) + (ff_source_mcp_ics_product_first_cell_column))) -> (((exists fs_h_mcp_ics_product_first_cell_column_target. fs_h_mcp_ics_product_first_cell_column_target + S (ff_target_mcp_ics_product_first_cell_column) = S ((S (ff_index_mcp_ics_product_first_cell_column)) * ff_right_scale_mcp_cell_ics_product_first_cell)) /\ exists fs_q_mcp_ics_product_first_cell_column_target. ff_right_mcp_cell_ics_product_first_cell = fs_q_mcp_ics_product_first_cell_column_target * S ((S (ff_index_mcp_ics_product_first_cell_column)) * ff_right_scale_mcp_cell_ics_product_first_cell) + (ff_target_mcp_ics_product_first_cell_column))) -> ff_target_mcp_ics_product_first_cell_column = ff_source_mcp_ics_product_first_cell_column) /\ (exists ff_code_dot_mcp_ics_product_first_cell_dot ff_scale_dot_mcp_ics_product_first_cell_dot. ((forall fpmp_index_dot_mcp_ics_product_first_cell_dot_pointwise fpmp_left_dot_mcp_ics_product_first_cell_dot_pointwise fpmp_right_dot_mcp_ics_product_first_cell_dot_pointwise fpmp_target_dot_mcp_ics_product_first_cell_dot_pointwise. (exists fpmp_gap_dot_mcp_ics_product_first_cell_dot_pointwise. fpmp_gap_dot_mcp_ics_product_first_cell_dot_pointwise + S fpmp_index_dot_mcp_ics_product_first_cell_dot_pointwise = w) -> (((exists ff_h_fpmp_dot_mcp_ics_product_first_cell_dot_pointwise_left. ff_h_fpmp_dot_mcp_ics_product_first_cell_dot_pointwise_left + S (fpmp_left_dot_mcp_ics_product_first_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_product_first_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_product_first_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_product_first_cell_dot_pointwise_left. ff_left_mcp_cell_ics_product_first_cell = ff_q_fpmp_dot_mcp_ics_product_first_cell_dot_pointwise_left * S ((S (fpmp_index_dot_mcp_ics_product_first_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_product_first_cell) + (fpmp_left_dot_mcp_ics_product_first_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_product_first_cell_dot_pointwise_right. ff_h_fpmp_dot_mcp_ics_product_first_cell_dot_pointwise_right + S (fpmp_right_dot_mcp_ics_product_first_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_product_first_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_product_first_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_product_first_cell_dot_pointwise_right. ff_right_mcp_cell_ics_product_first_cell = ff_q_fpmp_dot_mcp_ics_product_first_cell_dot_pointwise_right * S ((S (fpmp_index_dot_mcp_ics_product_first_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_product_first_cell) + (fpmp_right_dot_mcp_ics_product_first_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_product_first_cell_dot_pointwise_target. ff_h_fpmp_dot_mcp_ics_product_first_cell_dot_pointwise_target + S (fpmp_target_dot_mcp_ics_product_first_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_product_first_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_product_first_cell_dot)) /\ exists ff_q_fpmp_dot_mcp_ics_product_first_cell_dot_pointwise_target. ff_code_dot_mcp_ics_product_first_cell_dot = ff_q_fpmp_dot_mcp_ics_product_first_cell_dot_pointwise_target * S ((S (fpmp_index_dot_mcp_ics_product_first_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_product_first_cell_dot) + (fpmp_target_dot_mcp_ics_product_first_cell_dot_pointwise))) -> fpmp_target_dot_mcp_ics_product_first_cell_dot_pointwise = fpmp_left_dot_mcp_ics_product_first_cell_dot_pointwise * fpmp_right_dot_mcp_ics_product_first_cell_dot_pointwise) /\ (exists ff_u_dot_mcp_ics_product_first_cell_dot_sum ff_v_dot_mcp_ics_product_first_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_product_first_cell_dot_sum_start. ff_h_dot_mcp_ics_product_first_cell_dot_sum_start + S (0) = S ((S (0)) * ff_v_dot_mcp_ics_product_first_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_product_first_cell_dot_sum_start. ff_u_dot_mcp_ics_product_first_cell_dot_sum = ff_q_dot_mcp_ics_product_first_cell_dot_sum_start * S ((S (0)) * ff_v_dot_mcp_ics_product_first_cell_dot_sum) + (0))) /\ ((((exists ff_h_dot_mcp_ics_product_first_cell_dot_sum_terminal. ff_h_dot_mcp_ics_product_first_cell_dot_sum_terminal + S (ff_value_mcp_prefix_ics_product_first) = S ((S (w)) * ff_v_dot_mcp_ics_product_first_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_product_first_cell_dot_sum_terminal. ff_u_dot_mcp_ics_product_first_cell_dot_sum = ff_q_dot_mcp_ics_product_first_cell_dot_sum_terminal * S ((S (w)) * ff_v_dot_mcp_ics_product_first_cell_dot_sum) + (ff_value_mcp_prefix_ics_product_first))) /\ forall ff_i_dot_mcp_ics_product_first_cell_dot_sum. (exists ff_lt_dot_mcp_ics_product_first_cell_dot_sum_bound. ff_lt_dot_mcp_ics_product_first_cell_dot_sum_bound + S ff_i_dot_mcp_ics_product_first_cell_dot_sum = w) -> exists ff_a_dot_mcp_ics_product_first_cell_dot_sum ff_r_dot_mcp_ics_product_first_cell_dot_sum ff_s_dot_mcp_ics_product_first_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_product_first_cell_dot_sum_summand. ff_h_dot_mcp_ics_product_first_cell_dot_sum_summand + S (ff_a_dot_mcp_ics_product_first_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_product_first_cell_dot_sum)) * ff_scale_dot_mcp_ics_product_first_cell_dot)) /\ exists ff_q_dot_mcp_ics_product_first_cell_dot_sum_summand. ff_code_dot_mcp_ics_product_first_cell_dot = ff_q_dot_mcp_ics_product_first_cell_dot_sum_summand * S ((S (ff_i_dot_mcp_ics_product_first_cell_dot_sum)) * ff_scale_dot_mcp_ics_product_first_cell_dot) + (ff_a_dot_mcp_ics_product_first_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_product_first_cell_dot_sum_partial. ff_h_dot_mcp_ics_product_first_cell_dot_sum_partial + S (ff_r_dot_mcp_ics_product_first_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_product_first_cell_dot_sum)) * ff_v_dot_mcp_ics_product_first_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_product_first_cell_dot_sum_partial. ff_u_dot_mcp_ics_product_first_cell_dot_sum = ff_q_dot_mcp_ics_product_first_cell_dot_sum_partial * S ((S (ff_i_dot_mcp_ics_product_first_cell_dot_sum)) * ff_v_dot_mcp_ics_product_first_cell_dot_sum) + (ff_r_dot_mcp_ics_product_first_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_product_first_cell_dot_sum_successor. ff_h_dot_mcp_ics_product_first_cell_dot_sum_successor + S (ff_s_dot_mcp_ics_product_first_cell_dot_sum) = S ((S (S ff_i_dot_mcp_ics_product_first_cell_dot_sum)) * ff_v_dot_mcp_ics_product_first_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_product_first_cell_dot_sum_successor. ff_u_dot_mcp_ics_product_first_cell_dot_sum = ff_q_dot_mcp_ics_product_first_cell_dot_sum_successor * S ((S (S ff_i_dot_mcp_ics_product_first_cell_dot_sum)) * ff_v_dot_mcp_ics_product_first_cell_dot_sum) + (ff_s_dot_mcp_ics_product_first_cell_dot_sum))) /\ ff_s_dot_mcp_ics_product_first_cell_dot_sum = ff_r_dot_mcp_ics_product_first_cell_dot_sum + ff_a_dot_mcp_ics_product_first_cell_dot_sum))))))))))) /\ (((exists fs_h_mcp_ics_product_first_entry. fs_h_mcp_ics_product_first_entry + S (ff_value_mcp_prefix_ics_product_first) = S ((S (ff_index_mcp_prefix_ics_product_first)) * pc)) /\ exists fs_q_mcp_ics_product_first_entry. pb = fs_q_mcp_ics_product_first_entry * S ((S (ff_index_mcp_prefix_ics_product_first)) * pc) + (ff_value_mcp_prefix_ics_product_first))))))) -> (forall ff_index_mcp_prefix_ics_product_second. (exists mcp_gap_ics_product_second_index. mcp_gap_ics_product_second_index + S (ff_index_mcp_prefix_ics_product_second) = (l)) -> exists ff_row_mcp_prefix_ics_product_second ff_column_mcp_prefix_ics_product_second ff_value_mcp_prefix_ics_product_second. ((ff_index_mcp_prefix_ics_product_second) = (1) * ff_row_mcp_prefix_ics_product_second + ff_column_mcp_prefix_ics_product_second /\ ((exists mcp_gap_ics_product_second_column. mcp_gap_ics_product_second_column + S (ff_column_mcp_prefix_ics_product_second) = (1)) /\ ((exists ff_left_mcp_cell_ics_product_second_cell ff_left_scale_mcp_cell_ics_product_second_cell ff_right_mcp_cell_ics_product_second_cell ff_right_scale_mcp_cell_ics_product_second_cell. ((forall ff_index_mcp_ics_product_second_cell_row ff_source_mcp_ics_product_second_cell_row ff_target_mcp_ics_product_second_cell_row. (exists mcp_gap_ics_product_second_cell_row_bound. mcp_gap_ics_product_second_cell_row_bound + S (ff_index_mcp_ics_product_second_cell_row) = (w)) -> (((exists fs_h_mcp_ics_product_second_cell_row_source. fs_h_mcp_ics_product_second_cell_row_source + S (ff_source_mcp_ics_product_second_cell_row) = S ((S (((ff_row_mcp_prefix_ics_product_second) * (w)) + (1) * ff_index_mcp_ics_product_second_cell_row)) * ac)) /\ exists fs_q_mcp_ics_product_second_cell_row_source. ab = fs_q_mcp_ics_product_second_cell_row_source * S ((S (((ff_row_mcp_prefix_ics_product_second) * (w)) + (1) * ff_index_mcp_ics_product_second_cell_row)) * ac) + (ff_source_mcp_ics_product_second_cell_row))) -> (((exists fs_h_mcp_ics_product_second_cell_row_target. fs_h_mcp_ics_product_second_cell_row_target + S (ff_target_mcp_ics_product_second_cell_row) = S ((S (ff_index_mcp_ics_product_second_cell_row)) * ff_left_scale_mcp_cell_ics_product_second_cell)) /\ exists fs_q_mcp_ics_product_second_cell_row_target. ff_left_mcp_cell_ics_product_second_cell = fs_q_mcp_ics_product_second_cell_row_target * S ((S (ff_index_mcp_ics_product_second_cell_row)) * ff_left_scale_mcp_cell_ics_product_second_cell) + (ff_target_mcp_ics_product_second_cell_row))) -> ff_target_mcp_ics_product_second_cell_row = ff_source_mcp_ics_product_second_cell_row) /\ ((forall ff_index_mcp_ics_product_second_cell_column ff_source_mcp_ics_product_second_cell_column ff_target_mcp_ics_product_second_cell_column. (exists mcp_gap_ics_product_second_cell_column_bound. mcp_gap_ics_product_second_cell_column_bound + S (ff_index_mcp_ics_product_second_cell_column) = (w)) -> (((exists fs_h_mcp_ics_product_second_cell_column_source. fs_h_mcp_ics_product_second_cell_column_source + S (ff_source_mcp_ics_product_second_cell_column) = S ((S ((ff_column_mcp_prefix_ics_product_second) + (1) * ff_index_mcp_ics_product_second_cell_column)) * cc)) /\ exists fs_q_mcp_ics_product_second_cell_column_source. cb = fs_q_mcp_ics_product_second_cell_column_source * S ((S ((ff_column_mcp_prefix_ics_product_second) + (1) * ff_index_mcp_ics_product_second_cell_column)) * cc) + (ff_source_mcp_ics_product_second_cell_column))) -> (((exists fs_h_mcp_ics_product_second_cell_column_target. fs_h_mcp_ics_product_second_cell_column_target + S (ff_target_mcp_ics_product_second_cell_column) = S ((S (ff_index_mcp_ics_product_second_cell_column)) * ff_right_scale_mcp_cell_ics_product_second_cell)) /\ exists fs_q_mcp_ics_product_second_cell_column_target. ff_right_mcp_cell_ics_product_second_cell = fs_q_mcp_ics_product_second_cell_column_target * S ((S (ff_index_mcp_ics_product_second_cell_column)) * ff_right_scale_mcp_cell_ics_product_second_cell) + (ff_target_mcp_ics_product_second_cell_column))) -> ff_target_mcp_ics_product_second_cell_column = ff_source_mcp_ics_product_second_cell_column) /\ (exists ff_code_dot_mcp_ics_product_second_cell_dot ff_scale_dot_mcp_ics_product_second_cell_dot. ((forall fpmp_index_dot_mcp_ics_product_second_cell_dot_pointwise fpmp_left_dot_mcp_ics_product_second_cell_dot_pointwise fpmp_right_dot_mcp_ics_product_second_cell_dot_pointwise fpmp_target_dot_mcp_ics_product_second_cell_dot_pointwise. (exists fpmp_gap_dot_mcp_ics_product_second_cell_dot_pointwise. fpmp_gap_dot_mcp_ics_product_second_cell_dot_pointwise + S fpmp_index_dot_mcp_ics_product_second_cell_dot_pointwise = w) -> (((exists ff_h_fpmp_dot_mcp_ics_product_second_cell_dot_pointwise_left. ff_h_fpmp_dot_mcp_ics_product_second_cell_dot_pointwise_left + S (fpmp_left_dot_mcp_ics_product_second_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_product_second_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_product_second_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_product_second_cell_dot_pointwise_left. ff_left_mcp_cell_ics_product_second_cell = ff_q_fpmp_dot_mcp_ics_product_second_cell_dot_pointwise_left * S ((S (fpmp_index_dot_mcp_ics_product_second_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_product_second_cell) + (fpmp_left_dot_mcp_ics_product_second_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_product_second_cell_dot_pointwise_right. ff_h_fpmp_dot_mcp_ics_product_second_cell_dot_pointwise_right + S (fpmp_right_dot_mcp_ics_product_second_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_product_second_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_product_second_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_product_second_cell_dot_pointwise_right. ff_right_mcp_cell_ics_product_second_cell = ff_q_fpmp_dot_mcp_ics_product_second_cell_dot_pointwise_right * S ((S (fpmp_index_dot_mcp_ics_product_second_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_product_second_cell) + (fpmp_right_dot_mcp_ics_product_second_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_product_second_cell_dot_pointwise_target. ff_h_fpmp_dot_mcp_ics_product_second_cell_dot_pointwise_target + S (fpmp_target_dot_mcp_ics_product_second_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_product_second_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_product_second_cell_dot)) /\ exists ff_q_fpmp_dot_mcp_ics_product_second_cell_dot_pointwise_target. ff_code_dot_mcp_ics_product_second_cell_dot = ff_q_fpmp_dot_mcp_ics_product_second_cell_dot_pointwise_target * S ((S (fpmp_index_dot_mcp_ics_product_second_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_product_second_cell_dot) + (fpmp_target_dot_mcp_ics_product_second_cell_dot_pointwise))) -> fpmp_target_dot_mcp_ics_product_second_cell_dot_pointwise = fpmp_left_dot_mcp_ics_product_second_cell_dot_pointwise * fpmp_right_dot_mcp_ics_product_second_cell_dot_pointwise) /\ (exists ff_u_dot_mcp_ics_product_second_cell_dot_sum ff_v_dot_mcp_ics_product_second_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_product_second_cell_dot_sum_start. ff_h_dot_mcp_ics_product_second_cell_dot_sum_start + S (0) = S ((S (0)) * ff_v_dot_mcp_ics_product_second_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_product_second_cell_dot_sum_start. ff_u_dot_mcp_ics_product_second_cell_dot_sum = ff_q_dot_mcp_ics_product_second_cell_dot_sum_start * S ((S (0)) * ff_v_dot_mcp_ics_product_second_cell_dot_sum) + (0))) /\ ((((exists ff_h_dot_mcp_ics_product_second_cell_dot_sum_terminal. ff_h_dot_mcp_ics_product_second_cell_dot_sum_terminal + S (ff_value_mcp_prefix_ics_product_second) = S ((S (w)) * ff_v_dot_mcp_ics_product_second_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_product_second_cell_dot_sum_terminal. ff_u_dot_mcp_ics_product_second_cell_dot_sum = ff_q_dot_mcp_ics_product_second_cell_dot_sum_terminal * S ((S (w)) * ff_v_dot_mcp_ics_product_second_cell_dot_sum) + (ff_value_mcp_prefix_ics_product_second))) /\ forall ff_i_dot_mcp_ics_product_second_cell_dot_sum. (exists ff_lt_dot_mcp_ics_product_second_cell_dot_sum_bound. ff_lt_dot_mcp_ics_product_second_cell_dot_sum_bound + S ff_i_dot_mcp_ics_product_second_cell_dot_sum = w) -> exists ff_a_dot_mcp_ics_product_second_cell_dot_sum ff_r_dot_mcp_ics_product_second_cell_dot_sum ff_s_dot_mcp_ics_product_second_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_product_second_cell_dot_sum_summand. ff_h_dot_mcp_ics_product_second_cell_dot_sum_summand + S (ff_a_dot_mcp_ics_product_second_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_product_second_cell_dot_sum)) * ff_scale_dot_mcp_ics_product_second_cell_dot)) /\ exists ff_q_dot_mcp_ics_product_second_cell_dot_sum_summand. ff_code_dot_mcp_ics_product_second_cell_dot = ff_q_dot_mcp_ics_product_second_cell_dot_sum_summand * S ((S (ff_i_dot_mcp_ics_product_second_cell_dot_sum)) * ff_scale_dot_mcp_ics_product_second_cell_dot) + (ff_a_dot_mcp_ics_product_second_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_product_second_cell_dot_sum_partial. ff_h_dot_mcp_ics_product_second_cell_dot_sum_partial + S (ff_r_dot_mcp_ics_product_second_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_product_second_cell_dot_sum)) * ff_v_dot_mcp_ics_product_second_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_product_second_cell_dot_sum_partial. ff_u_dot_mcp_ics_product_second_cell_dot_sum = ff_q_dot_mcp_ics_product_second_cell_dot_sum_partial * S ((S (ff_i_dot_mcp_ics_product_second_cell_dot_sum)) * ff_v_dot_mcp_ics_product_second_cell_dot_sum) + (ff_r_dot_mcp_ics_product_second_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_product_second_cell_dot_sum_successor. ff_h_dot_mcp_ics_product_second_cell_dot_sum_successor + S (ff_s_dot_mcp_ics_product_second_cell_dot_sum) = S ((S (S ff_i_dot_mcp_ics_product_second_cell_dot_sum)) * ff_v_dot_mcp_ics_product_second_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_product_second_cell_dot_sum_successor. ff_u_dot_mcp_ics_product_second_cell_dot_sum = ff_q_dot_mcp_ics_product_second_cell_dot_sum_successor * S ((S (S ff_i_dot_mcp_ics_product_second_cell_dot_sum)) * ff_v_dot_mcp_ics_product_second_cell_dot_sum) + (ff_s_dot_mcp_ics_product_second_cell_dot_sum))) /\ ff_s_dot_mcp_ics_product_second_cell_dot_sum = ff_r_dot_mcp_ics_product_second_cell_dot_sum + ff_a_dot_mcp_ics_product_second_cell_dot_sum))))))))))) /\ (((exists fs_h_mcp_ics_product_second_entry. fs_h_mcp_ics_product_second_entry + S (ff_value_mcp_prefix_ics_product_second) = S ((S (ff_index_mcp_prefix_ics_product_second)) * qc)) /\ exists fs_q_mcp_ics_product_second_entry. qb = fs_q_mcp_ics_product_second_entry * S ((S (ff_index_mcp_prefix_ics_product_second)) * qc) + (ff_value_mcp_prefix_ics_product_second))))))) -> (forall ff_index_mcp_prefix_ics_product_third. (exists mcp_gap_ics_product_third_index. mcp_gap_ics_product_third_index + S (ff_index_mcp_prefix_ics_product_third) = (l)) -> exists ff_row_mcp_prefix_ics_product_third ff_column_mcp_prefix_ics_product_third ff_value_mcp_prefix_ics_product_third. ((ff_index_mcp_prefix_ics_product_third) = (1) * ff_row_mcp_prefix_ics_product_third + ff_column_mcp_prefix_ics_product_third /\ ((exists mcp_gap_ics_product_third_column. mcp_gap_ics_product_third_column + S (ff_column_mcp_prefix_ics_product_third) = (1)) /\ ((exists ff_left_mcp_cell_ics_product_third_cell ff_left_scale_mcp_cell_ics_product_third_cell ff_right_mcp_cell_ics_product_third_cell ff_right_scale_mcp_cell_ics_product_third_cell. ((forall ff_index_mcp_ics_product_third_cell_row ff_source_mcp_ics_product_third_cell_row ff_target_mcp_ics_product_third_cell_row. (exists mcp_gap_ics_product_third_cell_row_bound. mcp_gap_ics_product_third_cell_row_bound + S (ff_index_mcp_ics_product_third_cell_row) = (w)) -> (((exists fs_h_mcp_ics_product_third_cell_row_source. fs_h_mcp_ics_product_third_cell_row_source + S (ff_source_mcp_ics_product_third_cell_row) = S ((S (((ff_row_mcp_prefix_ics_product_third) * (w)) + (1) * ff_index_mcp_ics_product_third_cell_row)) * ac)) /\ exists fs_q_mcp_ics_product_third_cell_row_source. ab = fs_q_mcp_ics_product_third_cell_row_source * S ((S (((ff_row_mcp_prefix_ics_product_third) * (w)) + (1) * ff_index_mcp_ics_product_third_cell_row)) * ac) + (ff_source_mcp_ics_product_third_cell_row))) -> (((exists fs_h_mcp_ics_product_third_cell_row_target. fs_h_mcp_ics_product_third_cell_row_target + S (ff_target_mcp_ics_product_third_cell_row) = S ((S (ff_index_mcp_ics_product_third_cell_row)) * ff_left_scale_mcp_cell_ics_product_third_cell)) /\ exists fs_q_mcp_ics_product_third_cell_row_target. ff_left_mcp_cell_ics_product_third_cell = fs_q_mcp_ics_product_third_cell_row_target * S ((S (ff_index_mcp_ics_product_third_cell_row)) * ff_left_scale_mcp_cell_ics_product_third_cell) + (ff_target_mcp_ics_product_third_cell_row))) -> ff_target_mcp_ics_product_third_cell_row = ff_source_mcp_ics_product_third_cell_row) /\ ((forall ff_index_mcp_ics_product_third_cell_column ff_source_mcp_ics_product_third_cell_column ff_target_mcp_ics_product_third_cell_column. (exists mcp_gap_ics_product_third_cell_column_bound. mcp_gap_ics_product_third_cell_column_bound + S (ff_index_mcp_ics_product_third_cell_column) = (w)) -> (((exists fs_h_mcp_ics_product_third_cell_column_source. fs_h_mcp_ics_product_third_cell_column_source + S (ff_source_mcp_ics_product_third_cell_column) = S ((S ((ff_column_mcp_prefix_ics_product_third) + (1) * ff_index_mcp_ics_product_third_cell_column)) * dc)) /\ exists fs_q_mcp_ics_product_third_cell_column_source. db = fs_q_mcp_ics_product_third_cell_column_source * S ((S ((ff_column_mcp_prefix_ics_product_third) + (1) * ff_index_mcp_ics_product_third_cell_column)) * dc) + (ff_source_mcp_ics_product_third_cell_column))) -> (((exists fs_h_mcp_ics_product_third_cell_column_target. fs_h_mcp_ics_product_third_cell_column_target + S (ff_target_mcp_ics_product_third_cell_column) = S ((S (ff_index_mcp_ics_product_third_cell_column)) * ff_right_scale_mcp_cell_ics_product_third_cell)) /\ exists fs_q_mcp_ics_product_third_cell_column_target. ff_right_mcp_cell_ics_product_third_cell = fs_q_mcp_ics_product_third_cell_column_target * S ((S (ff_index_mcp_ics_product_third_cell_column)) * ff_right_scale_mcp_cell_ics_product_third_cell) + (ff_target_mcp_ics_product_third_cell_column))) -> ff_target_mcp_ics_product_third_cell_column = ff_source_mcp_ics_product_third_cell_column) /\ (exists ff_code_dot_mcp_ics_product_third_cell_dot ff_scale_dot_mcp_ics_product_third_cell_dot. ((forall fpmp_index_dot_mcp_ics_product_third_cell_dot_pointwise fpmp_left_dot_mcp_ics_product_third_cell_dot_pointwise fpmp_right_dot_mcp_ics_product_third_cell_dot_pointwise fpmp_target_dot_mcp_ics_product_third_cell_dot_pointwise. (exists fpmp_gap_dot_mcp_ics_product_third_cell_dot_pointwise. fpmp_gap_dot_mcp_ics_product_third_cell_dot_pointwise + S fpmp_index_dot_mcp_ics_product_third_cell_dot_pointwise = w) -> (((exists ff_h_fpmp_dot_mcp_ics_product_third_cell_dot_pointwise_left. ff_h_fpmp_dot_mcp_ics_product_third_cell_dot_pointwise_left + S (fpmp_left_dot_mcp_ics_product_third_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_product_third_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_product_third_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_product_third_cell_dot_pointwise_left. ff_left_mcp_cell_ics_product_third_cell = ff_q_fpmp_dot_mcp_ics_product_third_cell_dot_pointwise_left * S ((S (fpmp_index_dot_mcp_ics_product_third_cell_dot_pointwise)) * ff_left_scale_mcp_cell_ics_product_third_cell) + (fpmp_left_dot_mcp_ics_product_third_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_product_third_cell_dot_pointwise_right. ff_h_fpmp_dot_mcp_ics_product_third_cell_dot_pointwise_right + S (fpmp_right_dot_mcp_ics_product_third_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_product_third_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_product_third_cell)) /\ exists ff_q_fpmp_dot_mcp_ics_product_third_cell_dot_pointwise_right. ff_right_mcp_cell_ics_product_third_cell = ff_q_fpmp_dot_mcp_ics_product_third_cell_dot_pointwise_right * S ((S (fpmp_index_dot_mcp_ics_product_third_cell_dot_pointwise)) * ff_right_scale_mcp_cell_ics_product_third_cell) + (fpmp_right_dot_mcp_ics_product_third_cell_dot_pointwise))) -> (((exists ff_h_fpmp_dot_mcp_ics_product_third_cell_dot_pointwise_target. ff_h_fpmp_dot_mcp_ics_product_third_cell_dot_pointwise_target + S (fpmp_target_dot_mcp_ics_product_third_cell_dot_pointwise) = S ((S (fpmp_index_dot_mcp_ics_product_third_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_product_third_cell_dot)) /\ exists ff_q_fpmp_dot_mcp_ics_product_third_cell_dot_pointwise_target. ff_code_dot_mcp_ics_product_third_cell_dot = ff_q_fpmp_dot_mcp_ics_product_third_cell_dot_pointwise_target * S ((S (fpmp_index_dot_mcp_ics_product_third_cell_dot_pointwise)) * ff_scale_dot_mcp_ics_product_third_cell_dot) + (fpmp_target_dot_mcp_ics_product_third_cell_dot_pointwise))) -> fpmp_target_dot_mcp_ics_product_third_cell_dot_pointwise = fpmp_left_dot_mcp_ics_product_third_cell_dot_pointwise * fpmp_right_dot_mcp_ics_product_third_cell_dot_pointwise) /\ (exists ff_u_dot_mcp_ics_product_third_cell_dot_sum ff_v_dot_mcp_ics_product_third_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_product_third_cell_dot_sum_start. ff_h_dot_mcp_ics_product_third_cell_dot_sum_start + S (0) = S ((S (0)) * ff_v_dot_mcp_ics_product_third_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_product_third_cell_dot_sum_start. ff_u_dot_mcp_ics_product_third_cell_dot_sum = ff_q_dot_mcp_ics_product_third_cell_dot_sum_start * S ((S (0)) * ff_v_dot_mcp_ics_product_third_cell_dot_sum) + (0))) /\ ((((exists ff_h_dot_mcp_ics_product_third_cell_dot_sum_terminal. ff_h_dot_mcp_ics_product_third_cell_dot_sum_terminal + S (ff_value_mcp_prefix_ics_product_third) = S ((S (w)) * ff_v_dot_mcp_ics_product_third_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_product_third_cell_dot_sum_terminal. ff_u_dot_mcp_ics_product_third_cell_dot_sum = ff_q_dot_mcp_ics_product_third_cell_dot_sum_terminal * S ((S (w)) * ff_v_dot_mcp_ics_product_third_cell_dot_sum) + (ff_value_mcp_prefix_ics_product_third))) /\ forall ff_i_dot_mcp_ics_product_third_cell_dot_sum. (exists ff_lt_dot_mcp_ics_product_third_cell_dot_sum_bound. ff_lt_dot_mcp_ics_product_third_cell_dot_sum_bound + S ff_i_dot_mcp_ics_product_third_cell_dot_sum = w) -> exists ff_a_dot_mcp_ics_product_third_cell_dot_sum ff_r_dot_mcp_ics_product_third_cell_dot_sum ff_s_dot_mcp_ics_product_third_cell_dot_sum. ((((exists ff_h_dot_mcp_ics_product_third_cell_dot_sum_summand. ff_h_dot_mcp_ics_product_third_cell_dot_sum_summand + S (ff_a_dot_mcp_ics_product_third_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_product_third_cell_dot_sum)) * ff_scale_dot_mcp_ics_product_third_cell_dot)) /\ exists ff_q_dot_mcp_ics_product_third_cell_dot_sum_summand. ff_code_dot_mcp_ics_product_third_cell_dot = ff_q_dot_mcp_ics_product_third_cell_dot_sum_summand * S ((S (ff_i_dot_mcp_ics_product_third_cell_dot_sum)) * ff_scale_dot_mcp_ics_product_third_cell_dot) + (ff_a_dot_mcp_ics_product_third_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_product_third_cell_dot_sum_partial. ff_h_dot_mcp_ics_product_third_cell_dot_sum_partial + S (ff_r_dot_mcp_ics_product_third_cell_dot_sum) = S ((S (ff_i_dot_mcp_ics_product_third_cell_dot_sum)) * ff_v_dot_mcp_ics_product_third_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_product_third_cell_dot_sum_partial. ff_u_dot_mcp_ics_product_third_cell_dot_sum = ff_q_dot_mcp_ics_product_third_cell_dot_sum_partial * S ((S (ff_i_dot_mcp_ics_product_third_cell_dot_sum)) * ff_v_dot_mcp_ics_product_third_cell_dot_sum) + (ff_r_dot_mcp_ics_product_third_cell_dot_sum))) /\ ((((exists ff_h_dot_mcp_ics_product_third_cell_dot_sum_successor. ff_h_dot_mcp_ics_product_third_cell_dot_sum_successor + S (ff_s_dot_mcp_ics_product_third_cell_dot_sum) = S ((S (S ff_i_dot_mcp_ics_product_third_cell_dot_sum)) * ff_v_dot_mcp_ics_product_third_cell_dot_sum)) /\ exists ff_q_dot_mcp_ics_product_third_cell_dot_sum_successor. ff_u_dot_mcp_ics_product_third_cell_dot_sum = ff_q_dot_mcp_ics_product_third_cell_dot_sum_successor * S ((S (S ff_i_dot_mcp_ics_product_third_cell_dot_sum)) * ff_v_dot_mcp_ics_product_third_cell_dot_sum) + (ff_s_dot_mcp_ics_product_third_cell_dot_sum))) /\ ff_s_dot_mcp_ics_product_third_cell_dot_sum = ff_r_dot_mcp_ics_product_third_cell_dot_sum + ff_a_dot_mcp_ics_product_third_cell_dot_sum))))))))))) /\ (((exists fs_h_mcp_ics_product_third_entry. fs_h_mcp_ics_product_third_entry + S (ff_value_mcp_prefix_ics_product_third) = S ((S (ff_index_mcp_prefix_ics_product_third)) * rc)) /\ exists fs_q_mcp_ics_product_third_entry. rb = fs_q_mcp_ics_product_third_entry * S ((S (ff_index_mcp_prefix_ics_product_third)) * rc) + (ff_value_mcp_prefix_ics_product_third))))))) -> (forall ff_index_mcp_add_ics_product_output_add ff_left_mcp_add_ics_product_output_add ff_right_mcp_add_ics_product_output_add ff_target_mcp_add_ics_product_output_add. (exists mcp_gap_ics_product_output_add_bound. mcp_gap_ics_product_output_add_bound + S (ff_index_mcp_add_ics_product_output_add) = (l)) -> (((exists fs_h_mcp_ics_product_output_add_left. fs_h_mcp_ics_product_output_add_left + S (ff_left_mcp_add_ics_product_output_add) = S ((S (ff_index_mcp_add_ics_product_output_add)) * pc)) /\ exists fs_q_mcp_ics_product_output_add_left. pb = fs_q_mcp_ics_product_output_add_left * S ((S (ff_index_mcp_add_ics_product_output_add)) * pc) + (ff_left_mcp_add_ics_product_output_add))) -> (((exists fs_h_mcp_ics_product_output_add_right. fs_h_mcp_ics_product_output_add_right + S (ff_right_mcp_add_ics_product_output_add) = S ((S (ff_index_mcp_add_ics_product_output_add)) * qc)) /\ exists fs_q_mcp_ics_product_output_add_right. qb = fs_q_mcp_ics_product_output_add_right * S ((S (ff_index_mcp_add_ics_product_output_add)) * qc) + (ff_right_mcp_add_ics_product_output_add))) -> (((exists fs_h_mcp_ics_product_output_add_target. fs_h_mcp_ics_product_output_add_target + S (ff_target_mcp_add_ics_product_output_add) = S ((S (ff_index_mcp_add_ics_product_output_add)) * rc)) /\ exists fs_q_mcp_ics_product_output_add_target. rb = fs_q_mcp_ics_product_output_add_target * S ((S (ff_index_mcp_add_ics_product_output_add)) * rc) + (ff_target_mcp_add_ics_product_output_add))) -> ff_target_mcp_add_ics_product_output_add = ff_left_mcp_add_ics_product_output_add + ff_right_mcp_add_ics_product_output_add)