matrix_recursive_step_transport

Exact expanded first-order arithmetic statement

forall b c u v i d pb pc nb nc p n. (forall mdr_i_step_prefix mdr_a_step_prefix. (exists mdr_gap_step_prefixb. mdr_gap_step_prefixb + S (mdr_i_step_prefix) = (i)) -> (((exists ff_h_mdr_step_prefixo. ff_h_mdr_step_prefixo + S (mdr_a_step_prefix) = S ((S (mdr_i_step_prefix)) * c)) /\ exists ff_q_mdr_step_prefixo. b = ff_q_mdr_step_prefixo * S ((S (mdr_i_step_prefix)) * c) + (mdr_a_step_prefix))) -> (((exists ff_h_mdr_step_prefixn. ff_h_mdr_step_prefixn + S (mdr_a_step_prefix) = S ((S (mdr_i_step_prefix)) * v)) /\ exists ff_q_mdr_step_prefixn. u = ff_q_mdr_step_prefixn * S ((S (mdr_i_step_prefix)) * v) + (mdr_a_step_prefix)))) -> (((((d) = 0) /\ (((p) = 1) /\ ((n) = 0))) \/ exists mdr_q_old_step mdr_eb_old_step mdr_ec_old_step mdr_fb_old_step mdr_fc_old_step. (((d) = S (mdr_q_old_step)) /\ ((forall mdr_j_old_stepc. (exists mdr_gap_old_stepcj. mdr_gap_old_stepcj + S (mdr_j_old_stepc) = (S (mdr_q_old_step))) -> exists mdr_i_old_stepc mdr_up_old_stepc mdr_us_old_stepc mdr_un_old_stepc mdr_ut_old_stepc mdr_p_old_stepc mdr_n_old_stepc. ((exists mdr_gap_old_stepci. mdr_gap_old_stepci + S (mdr_i_old_stepc) = (i)) /\ ((exists mdr_z_old_stepcr. ((exists mdr_a_old_stepcrc mdr_b_old_stepcrc mdr_c_old_stepcrc mdr_e_old_stepcrc mdr_f_old_stepcrc. ((mdr_a_old_stepcrc = ((mdr_q_old_step) + (mdr_up_old_stepc)) * S ((mdr_q_old_step) + (mdr_up_old_stepc)) + ((mdr_up_old_stepc) + (mdr_up_old_stepc))) /\ ((mdr_b_old_stepcrc = ((mdr_us_old_stepc) + (mdr_un_old_stepc)) * S ((mdr_us_old_stepc) + (mdr_un_old_stepc)) + ((mdr_un_old_stepc) + (mdr_un_old_stepc))) /\ ((mdr_c_old_stepcrc = ((mdr_a_old_stepcrc) + (mdr_b_old_stepcrc)) * S ((mdr_a_old_stepcrc) + (mdr_b_old_stepcrc)) + ((mdr_b_old_stepcrc) + (mdr_b_old_stepcrc))) /\ ((mdr_e_old_stepcrc = ((mdr_p_old_stepc) + (mdr_n_old_stepc)) * S ((mdr_p_old_stepc) + (mdr_n_old_stepc)) + ((mdr_n_old_stepc) + (mdr_n_old_stepc))) /\ ((mdr_f_old_stepcrc = ((mdr_ut_old_stepc) + (mdr_e_old_stepcrc)) * S ((mdr_ut_old_stepc) + (mdr_e_old_stepcrc)) + ((mdr_e_old_stepcrc) + (mdr_e_old_stepcrc))) /\ ((mdr_z_old_stepcr) = ((mdr_c_old_stepcrc) + (mdr_f_old_stepcrc)) * S ((mdr_c_old_stepcrc) + (mdr_f_old_stepcrc)) + ((mdr_f_old_stepcrc) + (mdr_f_old_stepcrc))))))))) /\ (((exists ff_h_mdr_old_stepcrb. ff_h_mdr_old_stepcrb + S (mdr_z_old_stepcr) = S ((S (mdr_i_old_stepc)) * c)) /\ exists ff_q_mdr_old_stepcrb. b = ff_q_mdr_old_stepcrb * S ((S (mdr_i_old_stepc)) * c) + (mdr_z_old_stepcr))))) /\ ((((forall ff_index_mdm_prefix_mdr_old_stepcm_positive. (exists ff_gap_mdm_lt_mdr_old_stepcm_positive_index_bound. ff_gap_mdm_lt_mdr_old_stepcm_positive_index_bound + S (ff_index_mdm_prefix_mdr_old_stepcm_positive) = ((mdr_q_old_step) * (mdr_q_old_step))) -> exists ff_row_mdm_prefix_mdr_old_stepcm_positive ff_column_mdm_prefix_mdr_old_stepcm_positive ff_value_mdm_prefix_mdr_old_stepcm_positive. (ff_index_mdm_prefix_mdr_old_stepcm_positive = (mdr_q_old_step) * ff_row_mdm_prefix_mdr_old_stepcm_positive + ff_column_mdm_prefix_mdr_old_stepcm_positive /\ ((exists ff_gap_mdm_lt_mdr_old_stepcm_positive_column_bound. ff_gap_mdm_lt_mdr_old_stepcm_positive_column_bound + S (ff_column_mdm_prefix_mdr_old_stepcm_positive) = (mdr_q_old_step)) /\ ((exists ff_row_mdm_cell_mdr_old_stepcm_positive_cell ff_column_mdm_cell_mdr_old_stepcm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_old_stepcm_positive_cell_row_before. ff_gap_mdm_lt_mdr_old_stepcm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_old_stepcm_positive) = (0)) /\ ff_row_mdm_cell_mdr_old_stepcm_positive_cell = ff_row_mdm_prefix_mdr_old_stepcm_positive) \/ ((exists ff_gap_mdm_le_mdr_old_stepcm_positive_cell_row_after. ff_gap_mdm_le_mdr_old_stepcm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_old_stepcm_positive)) /\ ff_row_mdm_cell_mdr_old_stepcm_positive_cell = S ff_row_mdm_prefix_mdr_old_stepcm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_old_stepcm_positive_cell_column_before. ff_gap_mdm_lt_mdr_old_stepcm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_old_stepcm_positive) = (mdr_j_old_stepc)) /\ ff_column_mdm_cell_mdr_old_stepcm_positive_cell = ff_column_mdm_prefix_mdr_old_stepcm_positive) \/ ((exists ff_gap_mdm_le_mdr_old_stepcm_positive_cell_column_after. ff_gap_mdm_le_mdr_old_stepcm_positive_cell_column_after + (mdr_j_old_stepc) = (ff_column_mdm_prefix_mdr_old_stepcm_positive)) /\ ff_column_mdm_cell_mdr_old_stepcm_positive_cell = S ff_column_mdm_prefix_mdr_old_stepcm_positive))) /\ (((exists ff_h_mdm_mdr_old_stepcm_positive_cell_source. ff_h_mdm_mdr_old_stepcm_positive_cell_source + S (ff_value_mdm_prefix_mdr_old_stepcm_positive) = S ((S ((ff_row_mdm_cell_mdr_old_stepcm_positive_cell) * (S (mdr_q_old_step)) + (ff_column_mdm_cell_mdr_old_stepcm_positive_cell))) * pc)) /\ exists ff_q_mdm_mdr_old_stepcm_positive_cell_source. pb = ff_q_mdm_mdr_old_stepcm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_old_stepcm_positive_cell) * (S (mdr_q_old_step)) + (ff_column_mdm_cell_mdr_old_stepcm_positive_cell))) * pc) + (ff_value_mdm_prefix_mdr_old_stepcm_positive)))))) /\ (((exists ff_h_mdm_mdr_old_stepcm_positive_target. ff_h_mdm_mdr_old_stepcm_positive_target + S (ff_value_mdm_prefix_mdr_old_stepcm_positive) = S ((S (ff_index_mdm_prefix_mdr_old_stepcm_positive)) * mdr_us_old_stepc)) /\ exists ff_q_mdm_mdr_old_stepcm_positive_target. mdr_up_old_stepc = ff_q_mdm_mdr_old_stepcm_positive_target * S ((S (ff_index_mdm_prefix_mdr_old_stepcm_positive)) * mdr_us_old_stepc) + (ff_value_mdm_prefix_mdr_old_stepcm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_old_stepcm_negative. (exists ff_gap_mdm_lt_mdr_old_stepcm_negative_index_bound. ff_gap_mdm_lt_mdr_old_stepcm_negative_index_bound + S (ff_index_mdm_prefix_mdr_old_stepcm_negative) = ((mdr_q_old_step) * (mdr_q_old_step))) -> exists ff_row_mdm_prefix_mdr_old_stepcm_negative ff_column_mdm_prefix_mdr_old_stepcm_negative ff_value_mdm_prefix_mdr_old_stepcm_negative. (ff_index_mdm_prefix_mdr_old_stepcm_negative = (mdr_q_old_step) * ff_row_mdm_prefix_mdr_old_stepcm_negative + ff_column_mdm_prefix_mdr_old_stepcm_negative /\ ((exists ff_gap_mdm_lt_mdr_old_stepcm_negative_column_bound. ff_gap_mdm_lt_mdr_old_stepcm_negative_column_bound + S (ff_column_mdm_prefix_mdr_old_stepcm_negative) = (mdr_q_old_step)) /\ ((exists ff_row_mdm_cell_mdr_old_stepcm_negative_cell ff_column_mdm_cell_mdr_old_stepcm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_old_stepcm_negative_cell_row_before. ff_gap_mdm_lt_mdr_old_stepcm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_old_stepcm_negative) = (0)) /\ ff_row_mdm_cell_mdr_old_stepcm_negative_cell = ff_row_mdm_prefix_mdr_old_stepcm_negative) \/ ((exists ff_gap_mdm_le_mdr_old_stepcm_negative_cell_row_after. ff_gap_mdm_le_mdr_old_stepcm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_old_stepcm_negative)) /\ ff_row_mdm_cell_mdr_old_stepcm_negative_cell = S ff_row_mdm_prefix_mdr_old_stepcm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_old_stepcm_negative_cell_column_before. ff_gap_mdm_lt_mdr_old_stepcm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_old_stepcm_negative) = (mdr_j_old_stepc)) /\ ff_column_mdm_cell_mdr_old_stepcm_negative_cell = ff_column_mdm_prefix_mdr_old_stepcm_negative) \/ ((exists ff_gap_mdm_le_mdr_old_stepcm_negative_cell_column_after. ff_gap_mdm_le_mdr_old_stepcm_negative_cell_column_after + (mdr_j_old_stepc) = (ff_column_mdm_prefix_mdr_old_stepcm_negative)) /\ ff_column_mdm_cell_mdr_old_stepcm_negative_cell = S ff_column_mdm_prefix_mdr_old_stepcm_negative))) /\ (((exists ff_h_mdm_mdr_old_stepcm_negative_cell_source. ff_h_mdm_mdr_old_stepcm_negative_cell_source + S (ff_value_mdm_prefix_mdr_old_stepcm_negative) = S ((S ((ff_row_mdm_cell_mdr_old_stepcm_negative_cell) * (S (mdr_q_old_step)) + (ff_column_mdm_cell_mdr_old_stepcm_negative_cell))) * nc)) /\ exists ff_q_mdm_mdr_old_stepcm_negative_cell_source. nb = ff_q_mdm_mdr_old_stepcm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_old_stepcm_negative_cell) * (S (mdr_q_old_step)) + (ff_column_mdm_cell_mdr_old_stepcm_negative_cell))) * nc) + (ff_value_mdm_prefix_mdr_old_stepcm_negative)))))) /\ (((exists ff_h_mdm_mdr_old_stepcm_negative_target. ff_h_mdm_mdr_old_stepcm_negative_target + S (ff_value_mdm_prefix_mdr_old_stepcm_negative) = S ((S (ff_index_mdm_prefix_mdr_old_stepcm_negative)) * mdr_ut_old_stepc)) /\ exists ff_q_mdm_mdr_old_stepcm_negative_target. mdr_un_old_stepc = ff_q_mdm_mdr_old_stepcm_negative_target * S ((S (ff_index_mdm_prefix_mdr_old_stepcm_negative)) * mdr_ut_old_stepc) + (ff_value_mdm_prefix_mdr_old_stepcm_negative))))))))) /\ ((((exists ff_h_mdr_old_stepcp. ff_h_mdr_old_stepcp + S (mdr_p_old_stepc) = S ((S (mdr_j_old_stepc)) * mdr_ec_old_step)) /\ exists ff_q_mdr_old_stepcp. mdr_eb_old_step = ff_q_mdr_old_stepcp * S ((S (mdr_j_old_stepc)) * mdr_ec_old_step) + (mdr_p_old_stepc))) /\ (((exists ff_h_mdr_old_stepcn. ff_h_mdr_old_stepcn + S (mdr_n_old_stepc) = S ((S (mdr_j_old_stepc)) * mdr_fc_old_step)) /\ exists ff_q_mdr_old_stepcn. mdr_fb_old_step = ff_q_mdr_old_stepcn * S ((S (mdr_j_old_stepc)) * mdr_fc_old_step) + (mdr_n_old_stepc)))))))) /\ (exists ff_ub_mce_fold_mdr_old_stepf ff_uc_mce_fold_mdr_old_stepf ff_vb_mce_fold_mdr_old_stepf ff_vc_mce_fold_mdr_old_stepf. ((forall ff_index_mce_alternating_mdr_old_stepf_prefix. (exists ff_gap_mce_mdr_old_stepf_prefix_index. ff_gap_mce_mdr_old_stepf_prefix_index + S (ff_index_mce_alternating_mdr_old_stepf_prefix) = (S (mdr_q_old_step))) -> exists ff_ap_mce_alternating_mdr_old_stepf_prefix ff_an_mce_alternating_mdr_old_stepf_prefix ff_bp_mce_alternating_mdr_old_stepf_prefix ff_bn_mce_alternating_mdr_old_stepf_prefix ff_p_mce_alternating_mdr_old_stepf_prefix ff_n_mce_alternating_mdr_old_stepf_prefix. ((((exists ff_h_mce_mdr_old_stepf_prefix_ap. ff_h_mce_mdr_old_stepf_prefix_ap + S (ff_ap_mce_alternating_mdr_old_stepf_prefix) = S ((S (ff_index_mce_alternating_mdr_old_stepf_prefix)) * pc)) /\ exists ff_q_mce_mdr_old_stepf_prefix_ap. pb = ff_q_mce_mdr_old_stepf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_old_stepf_prefix)) * pc) + (ff_ap_mce_alternating_mdr_old_stepf_prefix))) /\ ((((exists ff_h_mce_mdr_old_stepf_prefix_an. ff_h_mce_mdr_old_stepf_prefix_an + S (ff_an_mce_alternating_mdr_old_stepf_prefix) = S ((S (ff_index_mce_alternating_mdr_old_stepf_prefix)) * nc)) /\ exists ff_q_mce_mdr_old_stepf_prefix_an. nb = ff_q_mce_mdr_old_stepf_prefix_an * S ((S (ff_index_mce_alternating_mdr_old_stepf_prefix)) * nc) + (ff_an_mce_alternating_mdr_old_stepf_prefix))) /\ ((((exists ff_h_mce_mdr_old_stepf_prefix_bp. ff_h_mce_mdr_old_stepf_prefix_bp + S (ff_bp_mce_alternating_mdr_old_stepf_prefix) = S ((S (ff_index_mce_alternating_mdr_old_stepf_prefix)) * mdr_ec_old_step)) /\ exists ff_q_mce_mdr_old_stepf_prefix_bp. mdr_eb_old_step = ff_q_mce_mdr_old_stepf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_old_stepf_prefix)) * mdr_ec_old_step) + (ff_bp_mce_alternating_mdr_old_stepf_prefix))) /\ ((((exists ff_h_mce_mdr_old_stepf_prefix_bn. ff_h_mce_mdr_old_stepf_prefix_bn + S (ff_bn_mce_alternating_mdr_old_stepf_prefix) = S ((S (ff_index_mce_alternating_mdr_old_stepf_prefix)) * mdr_fc_old_step)) /\ exists ff_q_mce_mdr_old_stepf_prefix_bn. mdr_fb_old_step = ff_q_mce_mdr_old_stepf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_old_stepf_prefix)) * mdr_fc_old_step) + (ff_bn_mce_alternating_mdr_old_stepf_prefix))) /\ ((((exists ff_h_mce_mdr_old_stepf_prefix_positive. ff_h_mce_mdr_old_stepf_prefix_positive + S (ff_p_mce_alternating_mdr_old_stepf_prefix) = S ((S (ff_index_mce_alternating_mdr_old_stepf_prefix)) * ff_uc_mce_fold_mdr_old_stepf)) /\ exists ff_q_mce_mdr_old_stepf_prefix_positive. ff_ub_mce_fold_mdr_old_stepf = ff_q_mce_mdr_old_stepf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_old_stepf_prefix)) * ff_uc_mce_fold_mdr_old_stepf) + (ff_p_mce_alternating_mdr_old_stepf_prefix))) /\ ((((exists ff_h_mce_mdr_old_stepf_prefix_negative. ff_h_mce_mdr_old_stepf_prefix_negative + S (ff_n_mce_alternating_mdr_old_stepf_prefix) = S ((S (ff_index_mce_alternating_mdr_old_stepf_prefix)) * ff_vc_mce_fold_mdr_old_stepf)) /\ exists ff_q_mce_mdr_old_stepf_prefix_negative. ff_vb_mce_fold_mdr_old_stepf = ff_q_mce_mdr_old_stepf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_old_stepf_prefix)) * ff_vc_mce_fold_mdr_old_stepf) + (ff_n_mce_alternating_mdr_old_stepf_prefix))) /\ (((exists ff_even_mce_term_mdr_old_stepf_prefix_term. ff_index_mce_alternating_mdr_old_stepf_prefix = 2 * ff_even_mce_term_mdr_old_stepf_prefix_term) /\ (ff_p_mce_alternating_mdr_old_stepf_prefix = (ff_ap_mce_alternating_mdr_old_stepf_prefix) * (ff_bp_mce_alternating_mdr_old_stepf_prefix) + (ff_an_mce_alternating_mdr_old_stepf_prefix) * (ff_bn_mce_alternating_mdr_old_stepf_prefix) /\ ff_n_mce_alternating_mdr_old_stepf_prefix = (ff_ap_mce_alternating_mdr_old_stepf_prefix) * (ff_bn_mce_alternating_mdr_old_stepf_prefix) + (ff_an_mce_alternating_mdr_old_stepf_prefix) * (ff_bp_mce_alternating_mdr_old_stepf_prefix))) \/ ((exists ff_odd_mce_term_mdr_old_stepf_prefix_term. ff_index_mce_alternating_mdr_old_stepf_prefix = 2 * ff_odd_mce_term_mdr_old_stepf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_old_stepf_prefix = (ff_ap_mce_alternating_mdr_old_stepf_prefix) * (ff_bn_mce_alternating_mdr_old_stepf_prefix) + (ff_an_mce_alternating_mdr_old_stepf_prefix) * (ff_bp_mce_alternating_mdr_old_stepf_prefix) /\ ff_n_mce_alternating_mdr_old_stepf_prefix = (ff_ap_mce_alternating_mdr_old_stepf_prefix) * (ff_bp_mce_alternating_mdr_old_stepf_prefix) + (ff_an_mce_alternating_mdr_old_stepf_prefix) * (ff_bn_mce_alternating_mdr_old_stepf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_old_stepf_positive ff_v_mce_mdr_old_stepf_positive. ((((exists ff_h_mce_mdr_old_stepf_positive_start. ff_h_mce_mdr_old_stepf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_old_stepf_positive)) /\ exists ff_q_mce_mdr_old_stepf_positive_start. ff_u_mce_mdr_old_stepf_positive = ff_q_mce_mdr_old_stepf_positive_start * S ((S (0)) * ff_v_mce_mdr_old_stepf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_old_stepf_positive_terminal. ff_h_mce_mdr_old_stepf_positive_terminal + S (p) = S ((S ((S (mdr_q_old_step)))) * ff_v_mce_mdr_old_stepf_positive)) /\ exists ff_q_mce_mdr_old_stepf_positive_terminal. ff_u_mce_mdr_old_stepf_positive = ff_q_mce_mdr_old_stepf_positive_terminal * S ((S ((S (mdr_q_old_step)))) * ff_v_mce_mdr_old_stepf_positive) + (p))) /\ forall ff_i_mce_mdr_old_stepf_positive. (exists ff_lt_mce_mdr_old_stepf_positive_bound. ff_lt_mce_mdr_old_stepf_positive_bound + S ff_i_mce_mdr_old_stepf_positive = (S (mdr_q_old_step))) -> exists ff_a_mce_mdr_old_stepf_positive ff_r_mce_mdr_old_stepf_positive ff_s_mce_mdr_old_stepf_positive. ((((exists ff_h_mce_mdr_old_stepf_positive_summand. ff_h_mce_mdr_old_stepf_positive_summand + S (ff_a_mce_mdr_old_stepf_positive) = S ((S (ff_i_mce_mdr_old_stepf_positive)) * ff_uc_mce_fold_mdr_old_stepf)) /\ exists ff_q_mce_mdr_old_stepf_positive_summand. ff_ub_mce_fold_mdr_old_stepf = ff_q_mce_mdr_old_stepf_positive_summand * S ((S (ff_i_mce_mdr_old_stepf_positive)) * ff_uc_mce_fold_mdr_old_stepf) + (ff_a_mce_mdr_old_stepf_positive))) /\ ((((exists ff_h_mce_mdr_old_stepf_positive_partial. ff_h_mce_mdr_old_stepf_positive_partial + S (ff_r_mce_mdr_old_stepf_positive) = S ((S (ff_i_mce_mdr_old_stepf_positive)) * ff_v_mce_mdr_old_stepf_positive)) /\ exists ff_q_mce_mdr_old_stepf_positive_partial. ff_u_mce_mdr_old_stepf_positive = ff_q_mce_mdr_old_stepf_positive_partial * S ((S (ff_i_mce_mdr_old_stepf_positive)) * ff_v_mce_mdr_old_stepf_positive) + (ff_r_mce_mdr_old_stepf_positive))) /\ ((((exists ff_h_mce_mdr_old_stepf_positive_successor. ff_h_mce_mdr_old_stepf_positive_successor + S (ff_s_mce_mdr_old_stepf_positive) = S ((S (S ff_i_mce_mdr_old_stepf_positive)) * ff_v_mce_mdr_old_stepf_positive)) /\ exists ff_q_mce_mdr_old_stepf_positive_successor. ff_u_mce_mdr_old_stepf_positive = ff_q_mce_mdr_old_stepf_positive_successor * S ((S (S ff_i_mce_mdr_old_stepf_positive)) * ff_v_mce_mdr_old_stepf_positive) + (ff_s_mce_mdr_old_stepf_positive))) /\ ff_s_mce_mdr_old_stepf_positive = ff_r_mce_mdr_old_stepf_positive + ff_a_mce_mdr_old_stepf_positive)))))) /\ (exists ff_u_mce_mdr_old_stepf_negative ff_v_mce_mdr_old_stepf_negative. ((((exists ff_h_mce_mdr_old_stepf_negative_start. ff_h_mce_mdr_old_stepf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_old_stepf_negative)) /\ exists ff_q_mce_mdr_old_stepf_negative_start. ff_u_mce_mdr_old_stepf_negative = ff_q_mce_mdr_old_stepf_negative_start * S ((S (0)) * ff_v_mce_mdr_old_stepf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_old_stepf_negative_terminal. ff_h_mce_mdr_old_stepf_negative_terminal + S (n) = S ((S ((S (mdr_q_old_step)))) * ff_v_mce_mdr_old_stepf_negative)) /\ exists ff_q_mce_mdr_old_stepf_negative_terminal. ff_u_mce_mdr_old_stepf_negative = ff_q_mce_mdr_old_stepf_negative_terminal * S ((S ((S (mdr_q_old_step)))) * ff_v_mce_mdr_old_stepf_negative) + (n))) /\ forall ff_i_mce_mdr_old_stepf_negative. (exists ff_lt_mce_mdr_old_stepf_negative_bound. ff_lt_mce_mdr_old_stepf_negative_bound + S ff_i_mce_mdr_old_stepf_negative = (S (mdr_q_old_step))) -> exists ff_a_mce_mdr_old_stepf_negative ff_r_mce_mdr_old_stepf_negative ff_s_mce_mdr_old_stepf_negative. ((((exists ff_h_mce_mdr_old_stepf_negative_summand. ff_h_mce_mdr_old_stepf_negative_summand + S (ff_a_mce_mdr_old_stepf_negative) = S ((S (ff_i_mce_mdr_old_stepf_negative)) * ff_vc_mce_fold_mdr_old_stepf)) /\ exists ff_q_mce_mdr_old_stepf_negative_summand. ff_vb_mce_fold_mdr_old_stepf = ff_q_mce_mdr_old_stepf_negative_summand * S ((S (ff_i_mce_mdr_old_stepf_negative)) * ff_vc_mce_fold_mdr_old_stepf) + (ff_a_mce_mdr_old_stepf_negative))) /\ ((((exists ff_h_mce_mdr_old_stepf_negative_partial. ff_h_mce_mdr_old_stepf_negative_partial + S (ff_r_mce_mdr_old_stepf_negative) = S ((S (ff_i_mce_mdr_old_stepf_negative)) * ff_v_mce_mdr_old_stepf_negative)) /\ exists ff_q_mce_mdr_old_stepf_negative_partial. ff_u_mce_mdr_old_stepf_negative = ff_q_mce_mdr_old_stepf_negative_partial * S ((S (ff_i_mce_mdr_old_stepf_negative)) * ff_v_mce_mdr_old_stepf_negative) + (ff_r_mce_mdr_old_stepf_negative))) /\ ((((exists ff_h_mce_mdr_old_stepf_negative_successor. ff_h_mce_mdr_old_stepf_negative_successor + S (ff_s_mce_mdr_old_stepf_negative) = S ((S (S ff_i_mce_mdr_old_stepf_negative)) * ff_v_mce_mdr_old_stepf_negative)) /\ exists ff_q_mce_mdr_old_stepf_negative_successor. ff_u_mce_mdr_old_stepf_negative = ff_q_mce_mdr_old_stepf_negative_successor * S ((S (S ff_i_mce_mdr_old_stepf_negative)) * ff_v_mce_mdr_old_stepf_negative) + (ff_s_mce_mdr_old_stepf_negative))) /\ ff_s_mce_mdr_old_stepf_negative = ff_r_mce_mdr_old_stepf_negative + ff_a_mce_mdr_old_stepf_negative))))))))))))) -> (((((d) = 0) /\ (((p) = 1) /\ ((n) = 0))) \/ exists mdr_q_new_step mdr_eb_new_step mdr_ec_new_step mdr_fb_new_step mdr_fc_new_step. (((d) = S (mdr_q_new_step)) /\ ((forall mdr_j_new_stepc. (exists mdr_gap_new_stepcj. mdr_gap_new_stepcj + S (mdr_j_new_stepc) = (S (mdr_q_new_step))) -> exists mdr_i_new_stepc mdr_up_new_stepc mdr_us_new_stepc mdr_un_new_stepc mdr_ut_new_stepc mdr_p_new_stepc mdr_n_new_stepc. ((exists mdr_gap_new_stepci. mdr_gap_new_stepci + S (mdr_i_new_stepc) = (i)) /\ ((exists mdr_z_new_stepcr. ((exists mdr_a_new_stepcrc mdr_b_new_stepcrc mdr_c_new_stepcrc mdr_e_new_stepcrc mdr_f_new_stepcrc. ((mdr_a_new_stepcrc = ((mdr_q_new_step) + (mdr_up_new_stepc)) * S ((mdr_q_new_step) + (mdr_up_new_stepc)) + ((mdr_up_new_stepc) + (mdr_up_new_stepc))) /\ ((mdr_b_new_stepcrc = ((mdr_us_new_stepc) + (mdr_un_new_stepc)) * S ((mdr_us_new_stepc) + (mdr_un_new_stepc)) + ((mdr_un_new_stepc) + (mdr_un_new_stepc))) /\ ((mdr_c_new_stepcrc = ((mdr_a_new_stepcrc) + (mdr_b_new_stepcrc)) * S ((mdr_a_new_stepcrc) + (mdr_b_new_stepcrc)) + ((mdr_b_new_stepcrc) + (mdr_b_new_stepcrc))) /\ ((mdr_e_new_stepcrc = ((mdr_p_new_stepc) + (mdr_n_new_stepc)) * S ((mdr_p_new_stepc) + (mdr_n_new_stepc)) + ((mdr_n_new_stepc) + (mdr_n_new_stepc))) /\ ((mdr_f_new_stepcrc = ((mdr_ut_new_stepc) + (mdr_e_new_stepcrc)) * S ((mdr_ut_new_stepc) + (mdr_e_new_stepcrc)) + ((mdr_e_new_stepcrc) + (mdr_e_new_stepcrc))) /\ ((mdr_z_new_stepcr) = ((mdr_c_new_stepcrc) + (mdr_f_new_stepcrc)) * S ((mdr_c_new_stepcrc) + (mdr_f_new_stepcrc)) + ((mdr_f_new_stepcrc) + (mdr_f_new_stepcrc))))))))) /\ (((exists ff_h_mdr_new_stepcrb. ff_h_mdr_new_stepcrb + S (mdr_z_new_stepcr) = S ((S (mdr_i_new_stepc)) * v)) /\ exists ff_q_mdr_new_stepcrb. u = ff_q_mdr_new_stepcrb * S ((S (mdr_i_new_stepc)) * v) + (mdr_z_new_stepcr))))) /\ ((((forall ff_index_mdm_prefix_mdr_new_stepcm_positive. (exists ff_gap_mdm_lt_mdr_new_stepcm_positive_index_bound. ff_gap_mdm_lt_mdr_new_stepcm_positive_index_bound + S (ff_index_mdm_prefix_mdr_new_stepcm_positive) = ((mdr_q_new_step) * (mdr_q_new_step))) -> exists ff_row_mdm_prefix_mdr_new_stepcm_positive ff_column_mdm_prefix_mdr_new_stepcm_positive ff_value_mdm_prefix_mdr_new_stepcm_positive. (ff_index_mdm_prefix_mdr_new_stepcm_positive = (mdr_q_new_step) * ff_row_mdm_prefix_mdr_new_stepcm_positive + ff_column_mdm_prefix_mdr_new_stepcm_positive /\ ((exists ff_gap_mdm_lt_mdr_new_stepcm_positive_column_bound. ff_gap_mdm_lt_mdr_new_stepcm_positive_column_bound + S (ff_column_mdm_prefix_mdr_new_stepcm_positive) = (mdr_q_new_step)) /\ ((exists ff_row_mdm_cell_mdr_new_stepcm_positive_cell ff_column_mdm_cell_mdr_new_stepcm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_new_stepcm_positive_cell_row_before. ff_gap_mdm_lt_mdr_new_stepcm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_new_stepcm_positive) = (0)) /\ ff_row_mdm_cell_mdr_new_stepcm_positive_cell = ff_row_mdm_prefix_mdr_new_stepcm_positive) \/ ((exists ff_gap_mdm_le_mdr_new_stepcm_positive_cell_row_after. ff_gap_mdm_le_mdr_new_stepcm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_new_stepcm_positive)) /\ ff_row_mdm_cell_mdr_new_stepcm_positive_cell = S ff_row_mdm_prefix_mdr_new_stepcm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_new_stepcm_positive_cell_column_before. ff_gap_mdm_lt_mdr_new_stepcm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_new_stepcm_positive) = (mdr_j_new_stepc)) /\ ff_column_mdm_cell_mdr_new_stepcm_positive_cell = ff_column_mdm_prefix_mdr_new_stepcm_positive) \/ ((exists ff_gap_mdm_le_mdr_new_stepcm_positive_cell_column_after. ff_gap_mdm_le_mdr_new_stepcm_positive_cell_column_after + (mdr_j_new_stepc) = (ff_column_mdm_prefix_mdr_new_stepcm_positive)) /\ ff_column_mdm_cell_mdr_new_stepcm_positive_cell = S ff_column_mdm_prefix_mdr_new_stepcm_positive))) /\ (((exists ff_h_mdm_mdr_new_stepcm_positive_cell_source. ff_h_mdm_mdr_new_stepcm_positive_cell_source + S (ff_value_mdm_prefix_mdr_new_stepcm_positive) = S ((S ((ff_row_mdm_cell_mdr_new_stepcm_positive_cell) * (S (mdr_q_new_step)) + (ff_column_mdm_cell_mdr_new_stepcm_positive_cell))) * pc)) /\ exists ff_q_mdm_mdr_new_stepcm_positive_cell_source. pb = ff_q_mdm_mdr_new_stepcm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_new_stepcm_positive_cell) * (S (mdr_q_new_step)) + (ff_column_mdm_cell_mdr_new_stepcm_positive_cell))) * pc) + (ff_value_mdm_prefix_mdr_new_stepcm_positive)))))) /\ (((exists ff_h_mdm_mdr_new_stepcm_positive_target. ff_h_mdm_mdr_new_stepcm_positive_target + S (ff_value_mdm_prefix_mdr_new_stepcm_positive) = S ((S (ff_index_mdm_prefix_mdr_new_stepcm_positive)) * mdr_us_new_stepc)) /\ exists ff_q_mdm_mdr_new_stepcm_positive_target. mdr_up_new_stepc = ff_q_mdm_mdr_new_stepcm_positive_target * S ((S (ff_index_mdm_prefix_mdr_new_stepcm_positive)) * mdr_us_new_stepc) + (ff_value_mdm_prefix_mdr_new_stepcm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_new_stepcm_negative. (exists ff_gap_mdm_lt_mdr_new_stepcm_negative_index_bound. ff_gap_mdm_lt_mdr_new_stepcm_negative_index_bound + S (ff_index_mdm_prefix_mdr_new_stepcm_negative) = ((mdr_q_new_step) * (mdr_q_new_step))) -> exists ff_row_mdm_prefix_mdr_new_stepcm_negative ff_column_mdm_prefix_mdr_new_stepcm_negative ff_value_mdm_prefix_mdr_new_stepcm_negative. (ff_index_mdm_prefix_mdr_new_stepcm_negative = (mdr_q_new_step) * ff_row_mdm_prefix_mdr_new_stepcm_negative + ff_column_mdm_prefix_mdr_new_stepcm_negative /\ ((exists ff_gap_mdm_lt_mdr_new_stepcm_negative_column_bound. ff_gap_mdm_lt_mdr_new_stepcm_negative_column_bound + S (ff_column_mdm_prefix_mdr_new_stepcm_negative) = (mdr_q_new_step)) /\ ((exists ff_row_mdm_cell_mdr_new_stepcm_negative_cell ff_column_mdm_cell_mdr_new_stepcm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_new_stepcm_negative_cell_row_before. ff_gap_mdm_lt_mdr_new_stepcm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_new_stepcm_negative) = (0)) /\ ff_row_mdm_cell_mdr_new_stepcm_negative_cell = ff_row_mdm_prefix_mdr_new_stepcm_negative) \/ ((exists ff_gap_mdm_le_mdr_new_stepcm_negative_cell_row_after. ff_gap_mdm_le_mdr_new_stepcm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_new_stepcm_negative)) /\ ff_row_mdm_cell_mdr_new_stepcm_negative_cell = S ff_row_mdm_prefix_mdr_new_stepcm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_new_stepcm_negative_cell_column_before. ff_gap_mdm_lt_mdr_new_stepcm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_new_stepcm_negative) = (mdr_j_new_stepc)) /\ ff_column_mdm_cell_mdr_new_stepcm_negative_cell = ff_column_mdm_prefix_mdr_new_stepcm_negative) \/ ((exists ff_gap_mdm_le_mdr_new_stepcm_negative_cell_column_after. ff_gap_mdm_le_mdr_new_stepcm_negative_cell_column_after + (mdr_j_new_stepc) = (ff_column_mdm_prefix_mdr_new_stepcm_negative)) /\ ff_column_mdm_cell_mdr_new_stepcm_negative_cell = S ff_column_mdm_prefix_mdr_new_stepcm_negative))) /\ (((exists ff_h_mdm_mdr_new_stepcm_negative_cell_source. ff_h_mdm_mdr_new_stepcm_negative_cell_source + S (ff_value_mdm_prefix_mdr_new_stepcm_negative) = S ((S ((ff_row_mdm_cell_mdr_new_stepcm_negative_cell) * (S (mdr_q_new_step)) + (ff_column_mdm_cell_mdr_new_stepcm_negative_cell))) * nc)) /\ exists ff_q_mdm_mdr_new_stepcm_negative_cell_source. nb = ff_q_mdm_mdr_new_stepcm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_new_stepcm_negative_cell) * (S (mdr_q_new_step)) + (ff_column_mdm_cell_mdr_new_stepcm_negative_cell))) * nc) + (ff_value_mdm_prefix_mdr_new_stepcm_negative)))))) /\ (((exists ff_h_mdm_mdr_new_stepcm_negative_target. ff_h_mdm_mdr_new_stepcm_negative_target + S (ff_value_mdm_prefix_mdr_new_stepcm_negative) = S ((S (ff_index_mdm_prefix_mdr_new_stepcm_negative)) * mdr_ut_new_stepc)) /\ exists ff_q_mdm_mdr_new_stepcm_negative_target. mdr_un_new_stepc = ff_q_mdm_mdr_new_stepcm_negative_target * S ((S (ff_index_mdm_prefix_mdr_new_stepcm_negative)) * mdr_ut_new_stepc) + (ff_value_mdm_prefix_mdr_new_stepcm_negative))))))))) /\ ((((exists ff_h_mdr_new_stepcp. ff_h_mdr_new_stepcp + S (mdr_p_new_stepc) = S ((S (mdr_j_new_stepc)) * mdr_ec_new_step)) /\ exists ff_q_mdr_new_stepcp. mdr_eb_new_step = ff_q_mdr_new_stepcp * S ((S (mdr_j_new_stepc)) * mdr_ec_new_step) + (mdr_p_new_stepc))) /\ (((exists ff_h_mdr_new_stepcn. ff_h_mdr_new_stepcn + S (mdr_n_new_stepc) = S ((S (mdr_j_new_stepc)) * mdr_fc_new_step)) /\ exists ff_q_mdr_new_stepcn. mdr_fb_new_step = ff_q_mdr_new_stepcn * S ((S (mdr_j_new_stepc)) * mdr_fc_new_step) + (mdr_n_new_stepc)))))))) /\ (exists ff_ub_mce_fold_mdr_new_stepf ff_uc_mce_fold_mdr_new_stepf ff_vb_mce_fold_mdr_new_stepf ff_vc_mce_fold_mdr_new_stepf. ((forall ff_index_mce_alternating_mdr_new_stepf_prefix. (exists ff_gap_mce_mdr_new_stepf_prefix_index. ff_gap_mce_mdr_new_stepf_prefix_index + S (ff_index_mce_alternating_mdr_new_stepf_prefix) = (S (mdr_q_new_step))) -> exists ff_ap_mce_alternating_mdr_new_stepf_prefix ff_an_mce_alternating_mdr_new_stepf_prefix ff_bp_mce_alternating_mdr_new_stepf_prefix ff_bn_mce_alternating_mdr_new_stepf_prefix ff_p_mce_alternating_mdr_new_stepf_prefix ff_n_mce_alternating_mdr_new_stepf_prefix. ((((exists ff_h_mce_mdr_new_stepf_prefix_ap. ff_h_mce_mdr_new_stepf_prefix_ap + S (ff_ap_mce_alternating_mdr_new_stepf_prefix) = S ((S (ff_index_mce_alternating_mdr_new_stepf_prefix)) * pc)) /\ exists ff_q_mce_mdr_new_stepf_prefix_ap. pb = ff_q_mce_mdr_new_stepf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_new_stepf_prefix)) * pc) + (ff_ap_mce_alternating_mdr_new_stepf_prefix))) /\ ((((exists ff_h_mce_mdr_new_stepf_prefix_an. ff_h_mce_mdr_new_stepf_prefix_an + S (ff_an_mce_alternating_mdr_new_stepf_prefix) = S ((S (ff_index_mce_alternating_mdr_new_stepf_prefix)) * nc)) /\ exists ff_q_mce_mdr_new_stepf_prefix_an. nb = ff_q_mce_mdr_new_stepf_prefix_an * S ((S (ff_index_mce_alternating_mdr_new_stepf_prefix)) * nc) + (ff_an_mce_alternating_mdr_new_stepf_prefix))) /\ ((((exists ff_h_mce_mdr_new_stepf_prefix_bp. ff_h_mce_mdr_new_stepf_prefix_bp + S (ff_bp_mce_alternating_mdr_new_stepf_prefix) = S ((S (ff_index_mce_alternating_mdr_new_stepf_prefix)) * mdr_ec_new_step)) /\ exists ff_q_mce_mdr_new_stepf_prefix_bp. mdr_eb_new_step = ff_q_mce_mdr_new_stepf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_new_stepf_prefix)) * mdr_ec_new_step) + (ff_bp_mce_alternating_mdr_new_stepf_prefix))) /\ ((((exists ff_h_mce_mdr_new_stepf_prefix_bn. ff_h_mce_mdr_new_stepf_prefix_bn + S (ff_bn_mce_alternating_mdr_new_stepf_prefix) = S ((S (ff_index_mce_alternating_mdr_new_stepf_prefix)) * mdr_fc_new_step)) /\ exists ff_q_mce_mdr_new_stepf_prefix_bn. mdr_fb_new_step = ff_q_mce_mdr_new_stepf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_new_stepf_prefix)) * mdr_fc_new_step) + (ff_bn_mce_alternating_mdr_new_stepf_prefix))) /\ ((((exists ff_h_mce_mdr_new_stepf_prefix_positive. ff_h_mce_mdr_new_stepf_prefix_positive + S (ff_p_mce_alternating_mdr_new_stepf_prefix) = S ((S (ff_index_mce_alternating_mdr_new_stepf_prefix)) * ff_uc_mce_fold_mdr_new_stepf)) /\ exists ff_q_mce_mdr_new_stepf_prefix_positive. ff_ub_mce_fold_mdr_new_stepf = ff_q_mce_mdr_new_stepf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_new_stepf_prefix)) * ff_uc_mce_fold_mdr_new_stepf) + (ff_p_mce_alternating_mdr_new_stepf_prefix))) /\ ((((exists ff_h_mce_mdr_new_stepf_prefix_negative. ff_h_mce_mdr_new_stepf_prefix_negative + S (ff_n_mce_alternating_mdr_new_stepf_prefix) = S ((S (ff_index_mce_alternating_mdr_new_stepf_prefix)) * ff_vc_mce_fold_mdr_new_stepf)) /\ exists ff_q_mce_mdr_new_stepf_prefix_negative. ff_vb_mce_fold_mdr_new_stepf = ff_q_mce_mdr_new_stepf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_new_stepf_prefix)) * ff_vc_mce_fold_mdr_new_stepf) + (ff_n_mce_alternating_mdr_new_stepf_prefix))) /\ (((exists ff_even_mce_term_mdr_new_stepf_prefix_term. ff_index_mce_alternating_mdr_new_stepf_prefix = 2 * ff_even_mce_term_mdr_new_stepf_prefix_term) /\ (ff_p_mce_alternating_mdr_new_stepf_prefix = (ff_ap_mce_alternating_mdr_new_stepf_prefix) * (ff_bp_mce_alternating_mdr_new_stepf_prefix) + (ff_an_mce_alternating_mdr_new_stepf_prefix) * (ff_bn_mce_alternating_mdr_new_stepf_prefix) /\ ff_n_mce_alternating_mdr_new_stepf_prefix = (ff_ap_mce_alternating_mdr_new_stepf_prefix) * (ff_bn_mce_alternating_mdr_new_stepf_prefix) + (ff_an_mce_alternating_mdr_new_stepf_prefix) * (ff_bp_mce_alternating_mdr_new_stepf_prefix))) \/ ((exists ff_odd_mce_term_mdr_new_stepf_prefix_term. ff_index_mce_alternating_mdr_new_stepf_prefix = 2 * ff_odd_mce_term_mdr_new_stepf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_new_stepf_prefix = (ff_ap_mce_alternating_mdr_new_stepf_prefix) * (ff_bn_mce_alternating_mdr_new_stepf_prefix) + (ff_an_mce_alternating_mdr_new_stepf_prefix) * (ff_bp_mce_alternating_mdr_new_stepf_prefix) /\ ff_n_mce_alternating_mdr_new_stepf_prefix = (ff_ap_mce_alternating_mdr_new_stepf_prefix) * (ff_bp_mce_alternating_mdr_new_stepf_prefix) + (ff_an_mce_alternating_mdr_new_stepf_prefix) * (ff_bn_mce_alternating_mdr_new_stepf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_new_stepf_positive ff_v_mce_mdr_new_stepf_positive. ((((exists ff_h_mce_mdr_new_stepf_positive_start. ff_h_mce_mdr_new_stepf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_new_stepf_positive)) /\ exists ff_q_mce_mdr_new_stepf_positive_start. ff_u_mce_mdr_new_stepf_positive = ff_q_mce_mdr_new_stepf_positive_start * S ((S (0)) * ff_v_mce_mdr_new_stepf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_new_stepf_positive_terminal. ff_h_mce_mdr_new_stepf_positive_terminal + S (p) = S ((S ((S (mdr_q_new_step)))) * ff_v_mce_mdr_new_stepf_positive)) /\ exists ff_q_mce_mdr_new_stepf_positive_terminal. ff_u_mce_mdr_new_stepf_positive = ff_q_mce_mdr_new_stepf_positive_terminal * S ((S ((S (mdr_q_new_step)))) * ff_v_mce_mdr_new_stepf_positive) + (p))) /\ forall ff_i_mce_mdr_new_stepf_positive. (exists ff_lt_mce_mdr_new_stepf_positive_bound. ff_lt_mce_mdr_new_stepf_positive_bound + S ff_i_mce_mdr_new_stepf_positive = (S (mdr_q_new_step))) -> exists ff_a_mce_mdr_new_stepf_positive ff_r_mce_mdr_new_stepf_positive ff_s_mce_mdr_new_stepf_positive. ((((exists ff_h_mce_mdr_new_stepf_positive_summand. ff_h_mce_mdr_new_stepf_positive_summand + S (ff_a_mce_mdr_new_stepf_positive) = S ((S (ff_i_mce_mdr_new_stepf_positive)) * ff_uc_mce_fold_mdr_new_stepf)) /\ exists ff_q_mce_mdr_new_stepf_positive_summand. ff_ub_mce_fold_mdr_new_stepf = ff_q_mce_mdr_new_stepf_positive_summand * S ((S (ff_i_mce_mdr_new_stepf_positive)) * ff_uc_mce_fold_mdr_new_stepf) + (ff_a_mce_mdr_new_stepf_positive))) /\ ((((exists ff_h_mce_mdr_new_stepf_positive_partial. ff_h_mce_mdr_new_stepf_positive_partial + S (ff_r_mce_mdr_new_stepf_positive) = S ((S (ff_i_mce_mdr_new_stepf_positive)) * ff_v_mce_mdr_new_stepf_positive)) /\ exists ff_q_mce_mdr_new_stepf_positive_partial. ff_u_mce_mdr_new_stepf_positive = ff_q_mce_mdr_new_stepf_positive_partial * S ((S (ff_i_mce_mdr_new_stepf_positive)) * ff_v_mce_mdr_new_stepf_positive) + (ff_r_mce_mdr_new_stepf_positive))) /\ ((((exists ff_h_mce_mdr_new_stepf_positive_successor. ff_h_mce_mdr_new_stepf_positive_successor + S (ff_s_mce_mdr_new_stepf_positive) = S ((S (S ff_i_mce_mdr_new_stepf_positive)) * ff_v_mce_mdr_new_stepf_positive)) /\ exists ff_q_mce_mdr_new_stepf_positive_successor. ff_u_mce_mdr_new_stepf_positive = ff_q_mce_mdr_new_stepf_positive_successor * S ((S (S ff_i_mce_mdr_new_stepf_positive)) * ff_v_mce_mdr_new_stepf_positive) + (ff_s_mce_mdr_new_stepf_positive))) /\ ff_s_mce_mdr_new_stepf_positive = ff_r_mce_mdr_new_stepf_positive + ff_a_mce_mdr_new_stepf_positive)))))) /\ (exists ff_u_mce_mdr_new_stepf_negative ff_v_mce_mdr_new_stepf_negative. ((((exists ff_h_mce_mdr_new_stepf_negative_start. ff_h_mce_mdr_new_stepf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_new_stepf_negative)) /\ exists ff_q_mce_mdr_new_stepf_negative_start. ff_u_mce_mdr_new_stepf_negative = ff_q_mce_mdr_new_stepf_negative_start * S ((S (0)) * ff_v_mce_mdr_new_stepf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_new_stepf_negative_terminal. ff_h_mce_mdr_new_stepf_negative_terminal + S (n) = S ((S ((S (mdr_q_new_step)))) * ff_v_mce_mdr_new_stepf_negative)) /\ exists ff_q_mce_mdr_new_stepf_negative_terminal. ff_u_mce_mdr_new_stepf_negative = ff_q_mce_mdr_new_stepf_negative_terminal * S ((S ((S (mdr_q_new_step)))) * ff_v_mce_mdr_new_stepf_negative) + (n))) /\ forall ff_i_mce_mdr_new_stepf_negative. (exists ff_lt_mce_mdr_new_stepf_negative_bound. ff_lt_mce_mdr_new_stepf_negative_bound + S ff_i_mce_mdr_new_stepf_negative = (S (mdr_q_new_step))) -> exists ff_a_mce_mdr_new_stepf_negative ff_r_mce_mdr_new_stepf_negative ff_s_mce_mdr_new_stepf_negative. ((((exists ff_h_mce_mdr_new_stepf_negative_summand. ff_h_mce_mdr_new_stepf_negative_summand + S (ff_a_mce_mdr_new_stepf_negative) = S ((S (ff_i_mce_mdr_new_stepf_negative)) * ff_vc_mce_fold_mdr_new_stepf)) /\ exists ff_q_mce_mdr_new_stepf_negative_summand. ff_vb_mce_fold_mdr_new_stepf = ff_q_mce_mdr_new_stepf_negative_summand * S ((S (ff_i_mce_mdr_new_stepf_negative)) * ff_vc_mce_fold_mdr_new_stepf) + (ff_a_mce_mdr_new_stepf_negative))) /\ ((((exists ff_h_mce_mdr_new_stepf_negative_partial. ff_h_mce_mdr_new_stepf_negative_partial + S (ff_r_mce_mdr_new_stepf_negative) = S ((S (ff_i_mce_mdr_new_stepf_negative)) * ff_v_mce_mdr_new_stepf_negative)) /\ exists ff_q_mce_mdr_new_stepf_negative_partial. ff_u_mce_mdr_new_stepf_negative = ff_q_mce_mdr_new_stepf_negative_partial * S ((S (ff_i_mce_mdr_new_stepf_negative)) * ff_v_mce_mdr_new_stepf_negative) + (ff_r_mce_mdr_new_stepf_negative))) /\ ((((exists ff_h_mce_mdr_new_stepf_negative_successor. ff_h_mce_mdr_new_stepf_negative_successor + S (ff_s_mce_mdr_new_stepf_negative) = S ((S (S ff_i_mce_mdr_new_stepf_negative)) * ff_v_mce_mdr_new_stepf_negative)) /\ exists ff_q_mce_mdr_new_stepf_negative_successor. ff_u_mce_mdr_new_stepf_negative = ff_q_mce_mdr_new_stepf_negative_successor * S ((S (S ff_i_mce_mdr_new_stepf_negative)) * ff_v_mce_mdr_new_stepf_negative) + (ff_s_mce_mdr_new_stepf_negative))) /\ ff_s_mce_mdr_new_stepf_negative = ff_r_mce_mdr_new_stepf_negative + ff_a_mce_mdr_new_stepf_negative)))))))))))))