matrix_recursive_history_transport

Exact expanded first-order arithmetic statement

forall b c u v l. (forall mdr_i_source mdr_a_source. (exists mdr_gap_sourceb. mdr_gap_sourceb + S (mdr_i_source) = (l)) -> (((exists ff_h_mdr_sourceo. ff_h_mdr_sourceo + S (mdr_a_source) = S ((S (mdr_i_source)) * c)) /\ exists ff_q_mdr_sourceo. b = ff_q_mdr_sourceo * S ((S (mdr_i_source)) * c) + (mdr_a_source))) -> (((exists ff_h_mdr_sourcen. ff_h_mdr_sourcen + S (mdr_a_source) = S ((S (mdr_i_source)) * v)) /\ exists ff_q_mdr_sourcen. u = ff_q_mdr_sourcen * S ((S (mdr_i_source)) * v) + (mdr_a_source)))) -> (forall mdr_i_old. (exists mdr_gap_oldi. mdr_gap_oldi + S (mdr_i_old) = (l)) -> exists mdr_d_old mdr_pb_old mdr_pc_old mdr_nb_old mdr_nc_old mdr_p_old mdr_n_old. ((exists mdr_z_oldr. ((exists mdr_a_oldrc mdr_b_oldrc mdr_c_oldrc mdr_e_oldrc mdr_f_oldrc. ((mdr_a_oldrc = ((mdr_d_old) + (mdr_pb_old)) * S ((mdr_d_old) + (mdr_pb_old)) + ((mdr_pb_old) + (mdr_pb_old))) /\ ((mdr_b_oldrc = ((mdr_pc_old) + (mdr_nb_old)) * S ((mdr_pc_old) + (mdr_nb_old)) + ((mdr_nb_old) + (mdr_nb_old))) /\ ((mdr_c_oldrc = ((mdr_a_oldrc) + (mdr_b_oldrc)) * S ((mdr_a_oldrc) + (mdr_b_oldrc)) + ((mdr_b_oldrc) + (mdr_b_oldrc))) /\ ((mdr_e_oldrc = ((mdr_p_old) + (mdr_n_old)) * S ((mdr_p_old) + (mdr_n_old)) + ((mdr_n_old) + (mdr_n_old))) /\ ((mdr_f_oldrc = ((mdr_nc_old) + (mdr_e_oldrc)) * S ((mdr_nc_old) + (mdr_e_oldrc)) + ((mdr_e_oldrc) + (mdr_e_oldrc))) /\ ((mdr_z_oldr) = ((mdr_c_oldrc) + (mdr_f_oldrc)) * S ((mdr_c_oldrc) + (mdr_f_oldrc)) + ((mdr_f_oldrc) + (mdr_f_oldrc))))))))) /\ (((exists ff_h_mdr_oldrb. ff_h_mdr_oldrb + S (mdr_z_oldr) = S ((S (mdr_i_old)) * c)) /\ exists ff_q_mdr_oldrb. b = ff_q_mdr_oldrb * S ((S (mdr_i_old)) * c) + (mdr_z_oldr))))) /\ (((((mdr_d_old) = 0) /\ (((mdr_p_old) = 1) /\ ((mdr_n_old) = 0))) \/ exists mdr_q_olds mdr_eb_olds mdr_ec_olds mdr_fb_olds mdr_fc_olds. (((mdr_d_old) = S (mdr_q_olds)) /\ ((forall mdr_j_oldsc. (exists mdr_gap_oldscj. mdr_gap_oldscj + S (mdr_j_oldsc) = (S (mdr_q_olds))) -> exists mdr_i_oldsc mdr_up_oldsc mdr_us_oldsc mdr_un_oldsc mdr_ut_oldsc mdr_p_oldsc mdr_n_oldsc. ((exists mdr_gap_oldsci. mdr_gap_oldsci + S (mdr_i_oldsc) = (mdr_i_old)) /\ ((exists mdr_z_oldscr. ((exists mdr_a_oldscrc mdr_b_oldscrc mdr_c_oldscrc mdr_e_oldscrc mdr_f_oldscrc. ((mdr_a_oldscrc = ((mdr_q_olds) + (mdr_up_oldsc)) * S ((mdr_q_olds) + (mdr_up_oldsc)) + ((mdr_up_oldsc) + (mdr_up_oldsc))) /\ ((mdr_b_oldscrc = ((mdr_us_oldsc) + (mdr_un_oldsc)) * S ((mdr_us_oldsc) + (mdr_un_oldsc)) + ((mdr_un_oldsc) + (mdr_un_oldsc))) /\ ((mdr_c_oldscrc = ((mdr_a_oldscrc) + (mdr_b_oldscrc)) * S ((mdr_a_oldscrc) + (mdr_b_oldscrc)) + ((mdr_b_oldscrc) + (mdr_b_oldscrc))) /\ ((mdr_e_oldscrc = ((mdr_p_oldsc) + (mdr_n_oldsc)) * S ((mdr_p_oldsc) + (mdr_n_oldsc)) + ((mdr_n_oldsc) + (mdr_n_oldsc))) /\ ((mdr_f_oldscrc = ((mdr_ut_oldsc) + (mdr_e_oldscrc)) * S ((mdr_ut_oldsc) + (mdr_e_oldscrc)) + ((mdr_e_oldscrc) + (mdr_e_oldscrc))) /\ ((mdr_z_oldscr) = ((mdr_c_oldscrc) + (mdr_f_oldscrc)) * S ((mdr_c_oldscrc) + (mdr_f_oldscrc)) + ((mdr_f_oldscrc) + (mdr_f_oldscrc))))))))) /\ (((exists ff_h_mdr_oldscrb. ff_h_mdr_oldscrb + S (mdr_z_oldscr) = S ((S (mdr_i_oldsc)) * c)) /\ exists ff_q_mdr_oldscrb. b = ff_q_mdr_oldscrb * S ((S (mdr_i_oldsc)) * c) + (mdr_z_oldscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_oldscm_positive. (exists ff_gap_mdm_lt_mdr_oldscm_positive_index_bound. ff_gap_mdm_lt_mdr_oldscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_oldscm_positive) = ((mdr_q_olds) * (mdr_q_olds))) -> exists ff_row_mdm_prefix_mdr_oldscm_positive ff_column_mdm_prefix_mdr_oldscm_positive ff_value_mdm_prefix_mdr_oldscm_positive. (ff_index_mdm_prefix_mdr_oldscm_positive = (mdr_q_olds) * ff_row_mdm_prefix_mdr_oldscm_positive + ff_column_mdm_prefix_mdr_oldscm_positive /\ ((exists ff_gap_mdm_lt_mdr_oldscm_positive_column_bound. ff_gap_mdm_lt_mdr_oldscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_oldscm_positive) = (mdr_q_olds)) /\ ((exists ff_row_mdm_cell_mdr_oldscm_positive_cell ff_column_mdm_cell_mdr_oldscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_oldscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_oldscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_oldscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_oldscm_positive_cell = ff_row_mdm_prefix_mdr_oldscm_positive) \/ ((exists ff_gap_mdm_le_mdr_oldscm_positive_cell_row_after. ff_gap_mdm_le_mdr_oldscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_oldscm_positive)) /\ ff_row_mdm_cell_mdr_oldscm_positive_cell = S ff_row_mdm_prefix_mdr_oldscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_oldscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_oldscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_oldscm_positive) = (mdr_j_oldsc)) /\ ff_column_mdm_cell_mdr_oldscm_positive_cell = ff_column_mdm_prefix_mdr_oldscm_positive) \/ ((exists ff_gap_mdm_le_mdr_oldscm_positive_cell_column_after. ff_gap_mdm_le_mdr_oldscm_positive_cell_column_after + (mdr_j_oldsc) = (ff_column_mdm_prefix_mdr_oldscm_positive)) /\ ff_column_mdm_cell_mdr_oldscm_positive_cell = S ff_column_mdm_prefix_mdr_oldscm_positive))) /\ (((exists ff_h_mdm_mdr_oldscm_positive_cell_source. ff_h_mdm_mdr_oldscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_oldscm_positive) = S ((S ((ff_row_mdm_cell_mdr_oldscm_positive_cell) * (S (mdr_q_olds)) + (ff_column_mdm_cell_mdr_oldscm_positive_cell))) * mdr_pc_old)) /\ exists ff_q_mdm_mdr_oldscm_positive_cell_source. mdr_pb_old = ff_q_mdm_mdr_oldscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_oldscm_positive_cell) * (S (mdr_q_olds)) + (ff_column_mdm_cell_mdr_oldscm_positive_cell))) * mdr_pc_old) + (ff_value_mdm_prefix_mdr_oldscm_positive)))))) /\ (((exists ff_h_mdm_mdr_oldscm_positive_target. ff_h_mdm_mdr_oldscm_positive_target + S (ff_value_mdm_prefix_mdr_oldscm_positive) = S ((S (ff_index_mdm_prefix_mdr_oldscm_positive)) * mdr_us_oldsc)) /\ exists ff_q_mdm_mdr_oldscm_positive_target. mdr_up_oldsc = ff_q_mdm_mdr_oldscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_oldscm_positive)) * mdr_us_oldsc) + (ff_value_mdm_prefix_mdr_oldscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_oldscm_negative. (exists ff_gap_mdm_lt_mdr_oldscm_negative_index_bound. ff_gap_mdm_lt_mdr_oldscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_oldscm_negative) = ((mdr_q_olds) * (mdr_q_olds))) -> exists ff_row_mdm_prefix_mdr_oldscm_negative ff_column_mdm_prefix_mdr_oldscm_negative ff_value_mdm_prefix_mdr_oldscm_negative. (ff_index_mdm_prefix_mdr_oldscm_negative = (mdr_q_olds) * ff_row_mdm_prefix_mdr_oldscm_negative + ff_column_mdm_prefix_mdr_oldscm_negative /\ ((exists ff_gap_mdm_lt_mdr_oldscm_negative_column_bound. ff_gap_mdm_lt_mdr_oldscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_oldscm_negative) = (mdr_q_olds)) /\ ((exists ff_row_mdm_cell_mdr_oldscm_negative_cell ff_column_mdm_cell_mdr_oldscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_oldscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_oldscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_oldscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_oldscm_negative_cell = ff_row_mdm_prefix_mdr_oldscm_negative) \/ ((exists ff_gap_mdm_le_mdr_oldscm_negative_cell_row_after. ff_gap_mdm_le_mdr_oldscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_oldscm_negative)) /\ ff_row_mdm_cell_mdr_oldscm_negative_cell = S ff_row_mdm_prefix_mdr_oldscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_oldscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_oldscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_oldscm_negative) = (mdr_j_oldsc)) /\ ff_column_mdm_cell_mdr_oldscm_negative_cell = ff_column_mdm_prefix_mdr_oldscm_negative) \/ ((exists ff_gap_mdm_le_mdr_oldscm_negative_cell_column_after. ff_gap_mdm_le_mdr_oldscm_negative_cell_column_after + (mdr_j_oldsc) = (ff_column_mdm_prefix_mdr_oldscm_negative)) /\ ff_column_mdm_cell_mdr_oldscm_negative_cell = S ff_column_mdm_prefix_mdr_oldscm_negative))) /\ (((exists ff_h_mdm_mdr_oldscm_negative_cell_source. ff_h_mdm_mdr_oldscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_oldscm_negative) = S ((S ((ff_row_mdm_cell_mdr_oldscm_negative_cell) * (S (mdr_q_olds)) + (ff_column_mdm_cell_mdr_oldscm_negative_cell))) * mdr_nc_old)) /\ exists ff_q_mdm_mdr_oldscm_negative_cell_source. mdr_nb_old = ff_q_mdm_mdr_oldscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_oldscm_negative_cell) * (S (mdr_q_olds)) + (ff_column_mdm_cell_mdr_oldscm_negative_cell))) * mdr_nc_old) + (ff_value_mdm_prefix_mdr_oldscm_negative)))))) /\ (((exists ff_h_mdm_mdr_oldscm_negative_target. ff_h_mdm_mdr_oldscm_negative_target + S (ff_value_mdm_prefix_mdr_oldscm_negative) = S ((S (ff_index_mdm_prefix_mdr_oldscm_negative)) * mdr_ut_oldsc)) /\ exists ff_q_mdm_mdr_oldscm_negative_target. mdr_un_oldsc = ff_q_mdm_mdr_oldscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_oldscm_negative)) * mdr_ut_oldsc) + (ff_value_mdm_prefix_mdr_oldscm_negative))))))))) /\ ((((exists ff_h_mdr_oldscp. ff_h_mdr_oldscp + S (mdr_p_oldsc) = S ((S (mdr_j_oldsc)) * mdr_ec_olds)) /\ exists ff_q_mdr_oldscp. mdr_eb_olds = ff_q_mdr_oldscp * S ((S (mdr_j_oldsc)) * mdr_ec_olds) + (mdr_p_oldsc))) /\ (((exists ff_h_mdr_oldscn. ff_h_mdr_oldscn + S (mdr_n_oldsc) = S ((S (mdr_j_oldsc)) * mdr_fc_olds)) /\ exists ff_q_mdr_oldscn. mdr_fb_olds = ff_q_mdr_oldscn * S ((S (mdr_j_oldsc)) * mdr_fc_olds) + (mdr_n_oldsc)))))))) /\ (exists ff_ub_mce_fold_mdr_oldsf ff_uc_mce_fold_mdr_oldsf ff_vb_mce_fold_mdr_oldsf ff_vc_mce_fold_mdr_oldsf. ((forall ff_index_mce_alternating_mdr_oldsf_prefix. (exists ff_gap_mce_mdr_oldsf_prefix_index. ff_gap_mce_mdr_oldsf_prefix_index + S (ff_index_mce_alternating_mdr_oldsf_prefix) = (S (mdr_q_olds))) -> exists ff_ap_mce_alternating_mdr_oldsf_prefix ff_an_mce_alternating_mdr_oldsf_prefix ff_bp_mce_alternating_mdr_oldsf_prefix ff_bn_mce_alternating_mdr_oldsf_prefix ff_p_mce_alternating_mdr_oldsf_prefix ff_n_mce_alternating_mdr_oldsf_prefix. ((((exists ff_h_mce_mdr_oldsf_prefix_ap. ff_h_mce_mdr_oldsf_prefix_ap + S (ff_ap_mce_alternating_mdr_oldsf_prefix) = S ((S (ff_index_mce_alternating_mdr_oldsf_prefix)) * mdr_pc_old)) /\ exists ff_q_mce_mdr_oldsf_prefix_ap. mdr_pb_old = ff_q_mce_mdr_oldsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_oldsf_prefix)) * mdr_pc_old) + (ff_ap_mce_alternating_mdr_oldsf_prefix))) /\ ((((exists ff_h_mce_mdr_oldsf_prefix_an. ff_h_mce_mdr_oldsf_prefix_an + S (ff_an_mce_alternating_mdr_oldsf_prefix) = S ((S (ff_index_mce_alternating_mdr_oldsf_prefix)) * mdr_nc_old)) /\ exists ff_q_mce_mdr_oldsf_prefix_an. mdr_nb_old = ff_q_mce_mdr_oldsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_oldsf_prefix)) * mdr_nc_old) + (ff_an_mce_alternating_mdr_oldsf_prefix))) /\ ((((exists ff_h_mce_mdr_oldsf_prefix_bp. ff_h_mce_mdr_oldsf_prefix_bp + S (ff_bp_mce_alternating_mdr_oldsf_prefix) = S ((S (ff_index_mce_alternating_mdr_oldsf_prefix)) * mdr_ec_olds)) /\ exists ff_q_mce_mdr_oldsf_prefix_bp. mdr_eb_olds = ff_q_mce_mdr_oldsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_oldsf_prefix)) * mdr_ec_olds) + (ff_bp_mce_alternating_mdr_oldsf_prefix))) /\ ((((exists ff_h_mce_mdr_oldsf_prefix_bn. ff_h_mce_mdr_oldsf_prefix_bn + S (ff_bn_mce_alternating_mdr_oldsf_prefix) = S ((S (ff_index_mce_alternating_mdr_oldsf_prefix)) * mdr_fc_olds)) /\ exists ff_q_mce_mdr_oldsf_prefix_bn. mdr_fb_olds = ff_q_mce_mdr_oldsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_oldsf_prefix)) * mdr_fc_olds) + (ff_bn_mce_alternating_mdr_oldsf_prefix))) /\ ((((exists ff_h_mce_mdr_oldsf_prefix_positive. ff_h_mce_mdr_oldsf_prefix_positive + S (ff_p_mce_alternating_mdr_oldsf_prefix) = S ((S (ff_index_mce_alternating_mdr_oldsf_prefix)) * ff_uc_mce_fold_mdr_oldsf)) /\ exists ff_q_mce_mdr_oldsf_prefix_positive. ff_ub_mce_fold_mdr_oldsf = ff_q_mce_mdr_oldsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_oldsf_prefix)) * ff_uc_mce_fold_mdr_oldsf) + (ff_p_mce_alternating_mdr_oldsf_prefix))) /\ ((((exists ff_h_mce_mdr_oldsf_prefix_negative. ff_h_mce_mdr_oldsf_prefix_negative + S (ff_n_mce_alternating_mdr_oldsf_prefix) = S ((S (ff_index_mce_alternating_mdr_oldsf_prefix)) * ff_vc_mce_fold_mdr_oldsf)) /\ exists ff_q_mce_mdr_oldsf_prefix_negative. ff_vb_mce_fold_mdr_oldsf = ff_q_mce_mdr_oldsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_oldsf_prefix)) * ff_vc_mce_fold_mdr_oldsf) + (ff_n_mce_alternating_mdr_oldsf_prefix))) /\ (((exists ff_even_mce_term_mdr_oldsf_prefix_term. ff_index_mce_alternating_mdr_oldsf_prefix = 2 * ff_even_mce_term_mdr_oldsf_prefix_term) /\ (ff_p_mce_alternating_mdr_oldsf_prefix = (ff_ap_mce_alternating_mdr_oldsf_prefix) * (ff_bp_mce_alternating_mdr_oldsf_prefix) + (ff_an_mce_alternating_mdr_oldsf_prefix) * (ff_bn_mce_alternating_mdr_oldsf_prefix) /\ ff_n_mce_alternating_mdr_oldsf_prefix = (ff_ap_mce_alternating_mdr_oldsf_prefix) * (ff_bn_mce_alternating_mdr_oldsf_prefix) + (ff_an_mce_alternating_mdr_oldsf_prefix) * (ff_bp_mce_alternating_mdr_oldsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_oldsf_prefix_term. ff_index_mce_alternating_mdr_oldsf_prefix = 2 * ff_odd_mce_term_mdr_oldsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_oldsf_prefix = (ff_ap_mce_alternating_mdr_oldsf_prefix) * (ff_bn_mce_alternating_mdr_oldsf_prefix) + (ff_an_mce_alternating_mdr_oldsf_prefix) * (ff_bp_mce_alternating_mdr_oldsf_prefix) /\ ff_n_mce_alternating_mdr_oldsf_prefix = (ff_ap_mce_alternating_mdr_oldsf_prefix) * (ff_bp_mce_alternating_mdr_oldsf_prefix) + (ff_an_mce_alternating_mdr_oldsf_prefix) * (ff_bn_mce_alternating_mdr_oldsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_oldsf_positive ff_v_mce_mdr_oldsf_positive. ((((exists ff_h_mce_mdr_oldsf_positive_start. ff_h_mce_mdr_oldsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_oldsf_positive)) /\ exists ff_q_mce_mdr_oldsf_positive_start. ff_u_mce_mdr_oldsf_positive = ff_q_mce_mdr_oldsf_positive_start * S ((S (0)) * ff_v_mce_mdr_oldsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_oldsf_positive_terminal. ff_h_mce_mdr_oldsf_positive_terminal + S (mdr_p_old) = S ((S ((S (mdr_q_olds)))) * ff_v_mce_mdr_oldsf_positive)) /\ exists ff_q_mce_mdr_oldsf_positive_terminal. ff_u_mce_mdr_oldsf_positive = ff_q_mce_mdr_oldsf_positive_terminal * S ((S ((S (mdr_q_olds)))) * ff_v_mce_mdr_oldsf_positive) + (mdr_p_old))) /\ forall ff_i_mce_mdr_oldsf_positive. (exists ff_lt_mce_mdr_oldsf_positive_bound. ff_lt_mce_mdr_oldsf_positive_bound + S ff_i_mce_mdr_oldsf_positive = (S (mdr_q_olds))) -> exists ff_a_mce_mdr_oldsf_positive ff_r_mce_mdr_oldsf_positive ff_s_mce_mdr_oldsf_positive. ((((exists ff_h_mce_mdr_oldsf_positive_summand. ff_h_mce_mdr_oldsf_positive_summand + S (ff_a_mce_mdr_oldsf_positive) = S ((S (ff_i_mce_mdr_oldsf_positive)) * ff_uc_mce_fold_mdr_oldsf)) /\ exists ff_q_mce_mdr_oldsf_positive_summand. ff_ub_mce_fold_mdr_oldsf = ff_q_mce_mdr_oldsf_positive_summand * S ((S (ff_i_mce_mdr_oldsf_positive)) * ff_uc_mce_fold_mdr_oldsf) + (ff_a_mce_mdr_oldsf_positive))) /\ ((((exists ff_h_mce_mdr_oldsf_positive_partial. ff_h_mce_mdr_oldsf_positive_partial + S (ff_r_mce_mdr_oldsf_positive) = S ((S (ff_i_mce_mdr_oldsf_positive)) * ff_v_mce_mdr_oldsf_positive)) /\ exists ff_q_mce_mdr_oldsf_positive_partial. ff_u_mce_mdr_oldsf_positive = ff_q_mce_mdr_oldsf_positive_partial * S ((S (ff_i_mce_mdr_oldsf_positive)) * ff_v_mce_mdr_oldsf_positive) + (ff_r_mce_mdr_oldsf_positive))) /\ ((((exists ff_h_mce_mdr_oldsf_positive_successor. ff_h_mce_mdr_oldsf_positive_successor + S (ff_s_mce_mdr_oldsf_positive) = S ((S (S ff_i_mce_mdr_oldsf_positive)) * ff_v_mce_mdr_oldsf_positive)) /\ exists ff_q_mce_mdr_oldsf_positive_successor. ff_u_mce_mdr_oldsf_positive = ff_q_mce_mdr_oldsf_positive_successor * S ((S (S ff_i_mce_mdr_oldsf_positive)) * ff_v_mce_mdr_oldsf_positive) + (ff_s_mce_mdr_oldsf_positive))) /\ ff_s_mce_mdr_oldsf_positive = ff_r_mce_mdr_oldsf_positive + ff_a_mce_mdr_oldsf_positive)))))) /\ (exists ff_u_mce_mdr_oldsf_negative ff_v_mce_mdr_oldsf_negative. ((((exists ff_h_mce_mdr_oldsf_negative_start. ff_h_mce_mdr_oldsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_oldsf_negative)) /\ exists ff_q_mce_mdr_oldsf_negative_start. ff_u_mce_mdr_oldsf_negative = ff_q_mce_mdr_oldsf_negative_start * S ((S (0)) * ff_v_mce_mdr_oldsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_oldsf_negative_terminal. ff_h_mce_mdr_oldsf_negative_terminal + S (mdr_n_old) = S ((S ((S (mdr_q_olds)))) * ff_v_mce_mdr_oldsf_negative)) /\ exists ff_q_mce_mdr_oldsf_negative_terminal. ff_u_mce_mdr_oldsf_negative = ff_q_mce_mdr_oldsf_negative_terminal * S ((S ((S (mdr_q_olds)))) * ff_v_mce_mdr_oldsf_negative) + (mdr_n_old))) /\ forall ff_i_mce_mdr_oldsf_negative. (exists ff_lt_mce_mdr_oldsf_negative_bound. ff_lt_mce_mdr_oldsf_negative_bound + S ff_i_mce_mdr_oldsf_negative = (S (mdr_q_olds))) -> exists ff_a_mce_mdr_oldsf_negative ff_r_mce_mdr_oldsf_negative ff_s_mce_mdr_oldsf_negative. ((((exists ff_h_mce_mdr_oldsf_negative_summand. ff_h_mce_mdr_oldsf_negative_summand + S (ff_a_mce_mdr_oldsf_negative) = S ((S (ff_i_mce_mdr_oldsf_negative)) * ff_vc_mce_fold_mdr_oldsf)) /\ exists ff_q_mce_mdr_oldsf_negative_summand. ff_vb_mce_fold_mdr_oldsf = ff_q_mce_mdr_oldsf_negative_summand * S ((S (ff_i_mce_mdr_oldsf_negative)) * ff_vc_mce_fold_mdr_oldsf) + (ff_a_mce_mdr_oldsf_negative))) /\ ((((exists ff_h_mce_mdr_oldsf_negative_partial. ff_h_mce_mdr_oldsf_negative_partial + S (ff_r_mce_mdr_oldsf_negative) = S ((S (ff_i_mce_mdr_oldsf_negative)) * ff_v_mce_mdr_oldsf_negative)) /\ exists ff_q_mce_mdr_oldsf_negative_partial. ff_u_mce_mdr_oldsf_negative = ff_q_mce_mdr_oldsf_negative_partial * S ((S (ff_i_mce_mdr_oldsf_negative)) * ff_v_mce_mdr_oldsf_negative) + (ff_r_mce_mdr_oldsf_negative))) /\ ((((exists ff_h_mce_mdr_oldsf_negative_successor. ff_h_mce_mdr_oldsf_negative_successor + S (ff_s_mce_mdr_oldsf_negative) = S ((S (S ff_i_mce_mdr_oldsf_negative)) * ff_v_mce_mdr_oldsf_negative)) /\ exists ff_q_mce_mdr_oldsf_negative_successor. ff_u_mce_mdr_oldsf_negative = ff_q_mce_mdr_oldsf_negative_successor * S ((S (S ff_i_mce_mdr_oldsf_negative)) * ff_v_mce_mdr_oldsf_negative) + (ff_s_mce_mdr_oldsf_negative))) /\ ff_s_mce_mdr_oldsf_negative = ff_r_mce_mdr_oldsf_negative + ff_a_mce_mdr_oldsf_negative))))))))))))))) -> (forall mdr_i_new. (exists mdr_gap_newi. mdr_gap_newi + S (mdr_i_new) = (l)) -> exists mdr_d_new mdr_pb_new mdr_pc_new mdr_nb_new mdr_nc_new mdr_p_new mdr_n_new. ((exists mdr_z_newr. ((exists mdr_a_newrc mdr_b_newrc mdr_c_newrc mdr_e_newrc mdr_f_newrc. ((mdr_a_newrc = ((mdr_d_new) + (mdr_pb_new)) * S ((mdr_d_new) + (mdr_pb_new)) + ((mdr_pb_new) + (mdr_pb_new))) /\ ((mdr_b_newrc = ((mdr_pc_new) + (mdr_nb_new)) * S ((mdr_pc_new) + (mdr_nb_new)) + ((mdr_nb_new) + (mdr_nb_new))) /\ ((mdr_c_newrc = ((mdr_a_newrc) + (mdr_b_newrc)) * S ((mdr_a_newrc) + (mdr_b_newrc)) + ((mdr_b_newrc) + (mdr_b_newrc))) /\ ((mdr_e_newrc = ((mdr_p_new) + (mdr_n_new)) * S ((mdr_p_new) + (mdr_n_new)) + ((mdr_n_new) + (mdr_n_new))) /\ ((mdr_f_newrc = ((mdr_nc_new) + (mdr_e_newrc)) * S ((mdr_nc_new) + (mdr_e_newrc)) + ((mdr_e_newrc) + (mdr_e_newrc))) /\ ((mdr_z_newr) = ((mdr_c_newrc) + (mdr_f_newrc)) * S ((mdr_c_newrc) + (mdr_f_newrc)) + ((mdr_f_newrc) + (mdr_f_newrc))))))))) /\ (((exists ff_h_mdr_newrb. ff_h_mdr_newrb + S (mdr_z_newr) = S ((S (mdr_i_new)) * v)) /\ exists ff_q_mdr_newrb. u = ff_q_mdr_newrb * S ((S (mdr_i_new)) * v) + (mdr_z_newr))))) /\ (((((mdr_d_new) = 0) /\ (((mdr_p_new) = 1) /\ ((mdr_n_new) = 0))) \/ exists mdr_q_news mdr_eb_news mdr_ec_news mdr_fb_news mdr_fc_news. (((mdr_d_new) = S (mdr_q_news)) /\ ((forall mdr_j_newsc. (exists mdr_gap_newscj. mdr_gap_newscj + S (mdr_j_newsc) = (S (mdr_q_news))) -> exists mdr_i_newsc mdr_up_newsc mdr_us_newsc mdr_un_newsc mdr_ut_newsc mdr_p_newsc mdr_n_newsc. ((exists mdr_gap_newsci. mdr_gap_newsci + S (mdr_i_newsc) = (mdr_i_new)) /\ ((exists mdr_z_newscr. ((exists mdr_a_newscrc mdr_b_newscrc mdr_c_newscrc mdr_e_newscrc mdr_f_newscrc. ((mdr_a_newscrc = ((mdr_q_news) + (mdr_up_newsc)) * S ((mdr_q_news) + (mdr_up_newsc)) + ((mdr_up_newsc) + (mdr_up_newsc))) /\ ((mdr_b_newscrc = ((mdr_us_newsc) + (mdr_un_newsc)) * S ((mdr_us_newsc) + (mdr_un_newsc)) + ((mdr_un_newsc) + (mdr_un_newsc))) /\ ((mdr_c_newscrc = ((mdr_a_newscrc) + (mdr_b_newscrc)) * S ((mdr_a_newscrc) + (mdr_b_newscrc)) + ((mdr_b_newscrc) + (mdr_b_newscrc))) /\ ((mdr_e_newscrc = ((mdr_p_newsc) + (mdr_n_newsc)) * S ((mdr_p_newsc) + (mdr_n_newsc)) + ((mdr_n_newsc) + (mdr_n_newsc))) /\ ((mdr_f_newscrc = ((mdr_ut_newsc) + (mdr_e_newscrc)) * S ((mdr_ut_newsc) + (mdr_e_newscrc)) + ((mdr_e_newscrc) + (mdr_e_newscrc))) /\ ((mdr_z_newscr) = ((mdr_c_newscrc) + (mdr_f_newscrc)) * S ((mdr_c_newscrc) + (mdr_f_newscrc)) + ((mdr_f_newscrc) + (mdr_f_newscrc))))))))) /\ (((exists ff_h_mdr_newscrb. ff_h_mdr_newscrb + S (mdr_z_newscr) = S ((S (mdr_i_newsc)) * v)) /\ exists ff_q_mdr_newscrb. u = ff_q_mdr_newscrb * S ((S (mdr_i_newsc)) * v) + (mdr_z_newscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_newscm_positive. (exists ff_gap_mdm_lt_mdr_newscm_positive_index_bound. ff_gap_mdm_lt_mdr_newscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_newscm_positive) = ((mdr_q_news) * (mdr_q_news))) -> exists ff_row_mdm_prefix_mdr_newscm_positive ff_column_mdm_prefix_mdr_newscm_positive ff_value_mdm_prefix_mdr_newscm_positive. (ff_index_mdm_prefix_mdr_newscm_positive = (mdr_q_news) * ff_row_mdm_prefix_mdr_newscm_positive + ff_column_mdm_prefix_mdr_newscm_positive /\ ((exists ff_gap_mdm_lt_mdr_newscm_positive_column_bound. ff_gap_mdm_lt_mdr_newscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_newscm_positive) = (mdr_q_news)) /\ ((exists ff_row_mdm_cell_mdr_newscm_positive_cell ff_column_mdm_cell_mdr_newscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_newscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_newscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_newscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_newscm_positive_cell = ff_row_mdm_prefix_mdr_newscm_positive) \/ ((exists ff_gap_mdm_le_mdr_newscm_positive_cell_row_after. ff_gap_mdm_le_mdr_newscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_newscm_positive)) /\ ff_row_mdm_cell_mdr_newscm_positive_cell = S ff_row_mdm_prefix_mdr_newscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_newscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_newscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_newscm_positive) = (mdr_j_newsc)) /\ ff_column_mdm_cell_mdr_newscm_positive_cell = ff_column_mdm_prefix_mdr_newscm_positive) \/ ((exists ff_gap_mdm_le_mdr_newscm_positive_cell_column_after. ff_gap_mdm_le_mdr_newscm_positive_cell_column_after + (mdr_j_newsc) = (ff_column_mdm_prefix_mdr_newscm_positive)) /\ ff_column_mdm_cell_mdr_newscm_positive_cell = S ff_column_mdm_prefix_mdr_newscm_positive))) /\ (((exists ff_h_mdm_mdr_newscm_positive_cell_source. ff_h_mdm_mdr_newscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_newscm_positive) = S ((S ((ff_row_mdm_cell_mdr_newscm_positive_cell) * (S (mdr_q_news)) + (ff_column_mdm_cell_mdr_newscm_positive_cell))) * mdr_pc_new)) /\ exists ff_q_mdm_mdr_newscm_positive_cell_source. mdr_pb_new = ff_q_mdm_mdr_newscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_newscm_positive_cell) * (S (mdr_q_news)) + (ff_column_mdm_cell_mdr_newscm_positive_cell))) * mdr_pc_new) + (ff_value_mdm_prefix_mdr_newscm_positive)))))) /\ (((exists ff_h_mdm_mdr_newscm_positive_target. ff_h_mdm_mdr_newscm_positive_target + S (ff_value_mdm_prefix_mdr_newscm_positive) = S ((S (ff_index_mdm_prefix_mdr_newscm_positive)) * mdr_us_newsc)) /\ exists ff_q_mdm_mdr_newscm_positive_target. mdr_up_newsc = ff_q_mdm_mdr_newscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_newscm_positive)) * mdr_us_newsc) + (ff_value_mdm_prefix_mdr_newscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_newscm_negative. (exists ff_gap_mdm_lt_mdr_newscm_negative_index_bound. ff_gap_mdm_lt_mdr_newscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_newscm_negative) = ((mdr_q_news) * (mdr_q_news))) -> exists ff_row_mdm_prefix_mdr_newscm_negative ff_column_mdm_prefix_mdr_newscm_negative ff_value_mdm_prefix_mdr_newscm_negative. (ff_index_mdm_prefix_mdr_newscm_negative = (mdr_q_news) * ff_row_mdm_prefix_mdr_newscm_negative + ff_column_mdm_prefix_mdr_newscm_negative /\ ((exists ff_gap_mdm_lt_mdr_newscm_negative_column_bound. ff_gap_mdm_lt_mdr_newscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_newscm_negative) = (mdr_q_news)) /\ ((exists ff_row_mdm_cell_mdr_newscm_negative_cell ff_column_mdm_cell_mdr_newscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_newscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_newscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_newscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_newscm_negative_cell = ff_row_mdm_prefix_mdr_newscm_negative) \/ ((exists ff_gap_mdm_le_mdr_newscm_negative_cell_row_after. ff_gap_mdm_le_mdr_newscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_newscm_negative)) /\ ff_row_mdm_cell_mdr_newscm_negative_cell = S ff_row_mdm_prefix_mdr_newscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_newscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_newscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_newscm_negative) = (mdr_j_newsc)) /\ ff_column_mdm_cell_mdr_newscm_negative_cell = ff_column_mdm_prefix_mdr_newscm_negative) \/ ((exists ff_gap_mdm_le_mdr_newscm_negative_cell_column_after. ff_gap_mdm_le_mdr_newscm_negative_cell_column_after + (mdr_j_newsc) = (ff_column_mdm_prefix_mdr_newscm_negative)) /\ ff_column_mdm_cell_mdr_newscm_negative_cell = S ff_column_mdm_prefix_mdr_newscm_negative))) /\ (((exists ff_h_mdm_mdr_newscm_negative_cell_source. ff_h_mdm_mdr_newscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_newscm_negative) = S ((S ((ff_row_mdm_cell_mdr_newscm_negative_cell) * (S (mdr_q_news)) + (ff_column_mdm_cell_mdr_newscm_negative_cell))) * mdr_nc_new)) /\ exists ff_q_mdm_mdr_newscm_negative_cell_source. mdr_nb_new = ff_q_mdm_mdr_newscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_newscm_negative_cell) * (S (mdr_q_news)) + (ff_column_mdm_cell_mdr_newscm_negative_cell))) * mdr_nc_new) + (ff_value_mdm_prefix_mdr_newscm_negative)))))) /\ (((exists ff_h_mdm_mdr_newscm_negative_target. ff_h_mdm_mdr_newscm_negative_target + S (ff_value_mdm_prefix_mdr_newscm_negative) = S ((S (ff_index_mdm_prefix_mdr_newscm_negative)) * mdr_ut_newsc)) /\ exists ff_q_mdm_mdr_newscm_negative_target. mdr_un_newsc = ff_q_mdm_mdr_newscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_newscm_negative)) * mdr_ut_newsc) + (ff_value_mdm_prefix_mdr_newscm_negative))))))))) /\ ((((exists ff_h_mdr_newscp. ff_h_mdr_newscp + S (mdr_p_newsc) = S ((S (mdr_j_newsc)) * mdr_ec_news)) /\ exists ff_q_mdr_newscp. mdr_eb_news = ff_q_mdr_newscp * S ((S (mdr_j_newsc)) * mdr_ec_news) + (mdr_p_newsc))) /\ (((exists ff_h_mdr_newscn. ff_h_mdr_newscn + S (mdr_n_newsc) = S ((S (mdr_j_newsc)) * mdr_fc_news)) /\ exists ff_q_mdr_newscn. mdr_fb_news = ff_q_mdr_newscn * S ((S (mdr_j_newsc)) * mdr_fc_news) + (mdr_n_newsc)))))))) /\ (exists ff_ub_mce_fold_mdr_newsf ff_uc_mce_fold_mdr_newsf ff_vb_mce_fold_mdr_newsf ff_vc_mce_fold_mdr_newsf. ((forall ff_index_mce_alternating_mdr_newsf_prefix. (exists ff_gap_mce_mdr_newsf_prefix_index. ff_gap_mce_mdr_newsf_prefix_index + S (ff_index_mce_alternating_mdr_newsf_prefix) = (S (mdr_q_news))) -> exists ff_ap_mce_alternating_mdr_newsf_prefix ff_an_mce_alternating_mdr_newsf_prefix ff_bp_mce_alternating_mdr_newsf_prefix ff_bn_mce_alternating_mdr_newsf_prefix ff_p_mce_alternating_mdr_newsf_prefix ff_n_mce_alternating_mdr_newsf_prefix. ((((exists ff_h_mce_mdr_newsf_prefix_ap. ff_h_mce_mdr_newsf_prefix_ap + S (ff_ap_mce_alternating_mdr_newsf_prefix) = S ((S (ff_index_mce_alternating_mdr_newsf_prefix)) * mdr_pc_new)) /\ exists ff_q_mce_mdr_newsf_prefix_ap. mdr_pb_new = ff_q_mce_mdr_newsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_newsf_prefix)) * mdr_pc_new) + (ff_ap_mce_alternating_mdr_newsf_prefix))) /\ ((((exists ff_h_mce_mdr_newsf_prefix_an. ff_h_mce_mdr_newsf_prefix_an + S (ff_an_mce_alternating_mdr_newsf_prefix) = S ((S (ff_index_mce_alternating_mdr_newsf_prefix)) * mdr_nc_new)) /\ exists ff_q_mce_mdr_newsf_prefix_an. mdr_nb_new = ff_q_mce_mdr_newsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_newsf_prefix)) * mdr_nc_new) + (ff_an_mce_alternating_mdr_newsf_prefix))) /\ ((((exists ff_h_mce_mdr_newsf_prefix_bp. ff_h_mce_mdr_newsf_prefix_bp + S (ff_bp_mce_alternating_mdr_newsf_prefix) = S ((S (ff_index_mce_alternating_mdr_newsf_prefix)) * mdr_ec_news)) /\ exists ff_q_mce_mdr_newsf_prefix_bp. mdr_eb_news = ff_q_mce_mdr_newsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_newsf_prefix)) * mdr_ec_news) + (ff_bp_mce_alternating_mdr_newsf_prefix))) /\ ((((exists ff_h_mce_mdr_newsf_prefix_bn. ff_h_mce_mdr_newsf_prefix_bn + S (ff_bn_mce_alternating_mdr_newsf_prefix) = S ((S (ff_index_mce_alternating_mdr_newsf_prefix)) * mdr_fc_news)) /\ exists ff_q_mce_mdr_newsf_prefix_bn. mdr_fb_news = ff_q_mce_mdr_newsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_newsf_prefix)) * mdr_fc_news) + (ff_bn_mce_alternating_mdr_newsf_prefix))) /\ ((((exists ff_h_mce_mdr_newsf_prefix_positive. ff_h_mce_mdr_newsf_prefix_positive + S (ff_p_mce_alternating_mdr_newsf_prefix) = S ((S (ff_index_mce_alternating_mdr_newsf_prefix)) * ff_uc_mce_fold_mdr_newsf)) /\ exists ff_q_mce_mdr_newsf_prefix_positive. ff_ub_mce_fold_mdr_newsf = ff_q_mce_mdr_newsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_newsf_prefix)) * ff_uc_mce_fold_mdr_newsf) + (ff_p_mce_alternating_mdr_newsf_prefix))) /\ ((((exists ff_h_mce_mdr_newsf_prefix_negative. ff_h_mce_mdr_newsf_prefix_negative + S (ff_n_mce_alternating_mdr_newsf_prefix) = S ((S (ff_index_mce_alternating_mdr_newsf_prefix)) * ff_vc_mce_fold_mdr_newsf)) /\ exists ff_q_mce_mdr_newsf_prefix_negative. ff_vb_mce_fold_mdr_newsf = ff_q_mce_mdr_newsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_newsf_prefix)) * ff_vc_mce_fold_mdr_newsf) + (ff_n_mce_alternating_mdr_newsf_prefix))) /\ (((exists ff_even_mce_term_mdr_newsf_prefix_term. ff_index_mce_alternating_mdr_newsf_prefix = 2 * ff_even_mce_term_mdr_newsf_prefix_term) /\ (ff_p_mce_alternating_mdr_newsf_prefix = (ff_ap_mce_alternating_mdr_newsf_prefix) * (ff_bp_mce_alternating_mdr_newsf_prefix) + (ff_an_mce_alternating_mdr_newsf_prefix) * (ff_bn_mce_alternating_mdr_newsf_prefix) /\ ff_n_mce_alternating_mdr_newsf_prefix = (ff_ap_mce_alternating_mdr_newsf_prefix) * (ff_bn_mce_alternating_mdr_newsf_prefix) + (ff_an_mce_alternating_mdr_newsf_prefix) * (ff_bp_mce_alternating_mdr_newsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_newsf_prefix_term. ff_index_mce_alternating_mdr_newsf_prefix = 2 * ff_odd_mce_term_mdr_newsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_newsf_prefix = (ff_ap_mce_alternating_mdr_newsf_prefix) * (ff_bn_mce_alternating_mdr_newsf_prefix) + (ff_an_mce_alternating_mdr_newsf_prefix) * (ff_bp_mce_alternating_mdr_newsf_prefix) /\ ff_n_mce_alternating_mdr_newsf_prefix = (ff_ap_mce_alternating_mdr_newsf_prefix) * (ff_bp_mce_alternating_mdr_newsf_prefix) + (ff_an_mce_alternating_mdr_newsf_prefix) * (ff_bn_mce_alternating_mdr_newsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_newsf_positive ff_v_mce_mdr_newsf_positive. ((((exists ff_h_mce_mdr_newsf_positive_start. ff_h_mce_mdr_newsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_newsf_positive)) /\ exists ff_q_mce_mdr_newsf_positive_start. ff_u_mce_mdr_newsf_positive = ff_q_mce_mdr_newsf_positive_start * S ((S (0)) * ff_v_mce_mdr_newsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_newsf_positive_terminal. ff_h_mce_mdr_newsf_positive_terminal + S (mdr_p_new) = S ((S ((S (mdr_q_news)))) * ff_v_mce_mdr_newsf_positive)) /\ exists ff_q_mce_mdr_newsf_positive_terminal. ff_u_mce_mdr_newsf_positive = ff_q_mce_mdr_newsf_positive_terminal * S ((S ((S (mdr_q_news)))) * ff_v_mce_mdr_newsf_positive) + (mdr_p_new))) /\ forall ff_i_mce_mdr_newsf_positive. (exists ff_lt_mce_mdr_newsf_positive_bound. ff_lt_mce_mdr_newsf_positive_bound + S ff_i_mce_mdr_newsf_positive = (S (mdr_q_news))) -> exists ff_a_mce_mdr_newsf_positive ff_r_mce_mdr_newsf_positive ff_s_mce_mdr_newsf_positive. ((((exists ff_h_mce_mdr_newsf_positive_summand. ff_h_mce_mdr_newsf_positive_summand + S (ff_a_mce_mdr_newsf_positive) = S ((S (ff_i_mce_mdr_newsf_positive)) * ff_uc_mce_fold_mdr_newsf)) /\ exists ff_q_mce_mdr_newsf_positive_summand. ff_ub_mce_fold_mdr_newsf = ff_q_mce_mdr_newsf_positive_summand * S ((S (ff_i_mce_mdr_newsf_positive)) * ff_uc_mce_fold_mdr_newsf) + (ff_a_mce_mdr_newsf_positive))) /\ ((((exists ff_h_mce_mdr_newsf_positive_partial. ff_h_mce_mdr_newsf_positive_partial + S (ff_r_mce_mdr_newsf_positive) = S ((S (ff_i_mce_mdr_newsf_positive)) * ff_v_mce_mdr_newsf_positive)) /\ exists ff_q_mce_mdr_newsf_positive_partial. ff_u_mce_mdr_newsf_positive = ff_q_mce_mdr_newsf_positive_partial * S ((S (ff_i_mce_mdr_newsf_positive)) * ff_v_mce_mdr_newsf_positive) + (ff_r_mce_mdr_newsf_positive))) /\ ((((exists ff_h_mce_mdr_newsf_positive_successor. ff_h_mce_mdr_newsf_positive_successor + S (ff_s_mce_mdr_newsf_positive) = S ((S (S ff_i_mce_mdr_newsf_positive)) * ff_v_mce_mdr_newsf_positive)) /\ exists ff_q_mce_mdr_newsf_positive_successor. ff_u_mce_mdr_newsf_positive = ff_q_mce_mdr_newsf_positive_successor * S ((S (S ff_i_mce_mdr_newsf_positive)) * ff_v_mce_mdr_newsf_positive) + (ff_s_mce_mdr_newsf_positive))) /\ ff_s_mce_mdr_newsf_positive = ff_r_mce_mdr_newsf_positive + ff_a_mce_mdr_newsf_positive)))))) /\ (exists ff_u_mce_mdr_newsf_negative ff_v_mce_mdr_newsf_negative. ((((exists ff_h_mce_mdr_newsf_negative_start. ff_h_mce_mdr_newsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_newsf_negative)) /\ exists ff_q_mce_mdr_newsf_negative_start. ff_u_mce_mdr_newsf_negative = ff_q_mce_mdr_newsf_negative_start * S ((S (0)) * ff_v_mce_mdr_newsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_newsf_negative_terminal. ff_h_mce_mdr_newsf_negative_terminal + S (mdr_n_new) = S ((S ((S (mdr_q_news)))) * ff_v_mce_mdr_newsf_negative)) /\ exists ff_q_mce_mdr_newsf_negative_terminal. ff_u_mce_mdr_newsf_negative = ff_q_mce_mdr_newsf_negative_terminal * S ((S ((S (mdr_q_news)))) * ff_v_mce_mdr_newsf_negative) + (mdr_n_new))) /\ forall ff_i_mce_mdr_newsf_negative. (exists ff_lt_mce_mdr_newsf_negative_bound. ff_lt_mce_mdr_newsf_negative_bound + S ff_i_mce_mdr_newsf_negative = (S (mdr_q_news))) -> exists ff_a_mce_mdr_newsf_negative ff_r_mce_mdr_newsf_negative ff_s_mce_mdr_newsf_negative. ((((exists ff_h_mce_mdr_newsf_negative_summand. ff_h_mce_mdr_newsf_negative_summand + S (ff_a_mce_mdr_newsf_negative) = S ((S (ff_i_mce_mdr_newsf_negative)) * ff_vc_mce_fold_mdr_newsf)) /\ exists ff_q_mce_mdr_newsf_negative_summand. ff_vb_mce_fold_mdr_newsf = ff_q_mce_mdr_newsf_negative_summand * S ((S (ff_i_mce_mdr_newsf_negative)) * ff_vc_mce_fold_mdr_newsf) + (ff_a_mce_mdr_newsf_negative))) /\ ((((exists ff_h_mce_mdr_newsf_negative_partial. ff_h_mce_mdr_newsf_negative_partial + S (ff_r_mce_mdr_newsf_negative) = S ((S (ff_i_mce_mdr_newsf_negative)) * ff_v_mce_mdr_newsf_negative)) /\ exists ff_q_mce_mdr_newsf_negative_partial. ff_u_mce_mdr_newsf_negative = ff_q_mce_mdr_newsf_negative_partial * S ((S (ff_i_mce_mdr_newsf_negative)) * ff_v_mce_mdr_newsf_negative) + (ff_r_mce_mdr_newsf_negative))) /\ ((((exists ff_h_mce_mdr_newsf_negative_successor. ff_h_mce_mdr_newsf_negative_successor + S (ff_s_mce_mdr_newsf_negative) = S ((S (S ff_i_mce_mdr_newsf_negative)) * ff_v_mce_mdr_newsf_negative)) /\ exists ff_q_mce_mdr_newsf_negative_successor. ff_u_mce_mdr_newsf_negative = ff_q_mce_mdr_newsf_negative_successor * S ((S (S ff_i_mce_mdr_newsf_negative)) * ff_v_mce_mdr_newsf_negative) + (ff_s_mce_mdr_newsf_negative))) /\ ff_s_mce_mdr_newsf_negative = ff_r_mce_mdr_newsf_negative + ff_a_mce_mdr_newsf_negative)))))))))))))))