matrix_recursive_history_extend

forall b c l d pb pc nb nc p n. (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))))))))))))))) -> (((((d) = 0) /\ (((p) = 1) /\ ((n) = 0))) \/ exists mdr_q_append_s mdr_eb_append_s mdr_ec_append_s mdr_fb_append_s mdr_fc_append_s. (((d) = S (mdr_q_append_s)) /\ ((forall mdr_j_append_sc. (exists mdr_gap_append_scj. mdr_gap_append_scj + S (mdr_j_append_sc) = (S (mdr_q_append_s))) -> exists mdr_i_append_sc mdr_up_append_sc mdr_us_append_sc mdr_un_append_sc mdr_ut_append_sc mdr_p_append_sc mdr_n_append_sc. ((exists mdr_gap_append_sci. mdr_gap_append_sci + S (mdr_i_append_sc) = (l)) /\ ((exists mdr_z_append_scr. ((exists mdr_a_append_scrc mdr_b_append_scrc mdr_c_append_scrc mdr_e_append_scrc mdr_f_append_scrc. ((mdr_a_append_scrc = ((mdr_q_append_s) + (mdr_up_append_sc)) * S ((mdr_q_append_s) + (mdr_up_append_sc)) + ((mdr_up_append_sc) + (mdr_up_append_sc))) /\ ((mdr_b_append_scrc = ((mdr_us_append_sc) + (mdr_un_append_sc)) * S ((mdr_us_append_sc) + (mdr_un_append_sc)) + ((mdr_un_append_sc) + (mdr_un_append_sc))) /\ ((mdr_c_append_scrc = ((mdr_a_append_scrc) + (mdr_b_append_scrc)) * S ((mdr_a_append_scrc) + (mdr_b_append_scrc)) + ((mdr_b_append_scrc) + (mdr_b_append_scrc))) /\ ((mdr_e_append_scrc = ((mdr_p_append_sc) + (mdr_n_append_sc)) * S ((mdr_p_append_sc) + (mdr_n_append_sc)) + ((mdr_n_append_sc) + (mdr_n_append_sc))) /\ ((mdr_f_append_scrc = ((mdr_ut_append_sc) + (mdr_e_append_scrc)) * S ((mdr_ut_append_sc) + (mdr_e_append_scrc)) + ((mdr_e_append_scrc) + (mdr_e_append_scrc))) /\ ((mdr_z_append_scr) = ((mdr_c_append_scrc) + (mdr_f_append_scrc)) * S ((mdr_c_append_scrc) + (mdr_f_append_scrc)) + ((mdr_f_append_scrc) + (mdr_f_append_scrc))))))))) /\ (((exists ff_h_mdr_append_scrb. ff_h_mdr_append_scrb + S (mdr_z_append_scr) = S ((S (mdr_i_append_sc)) * c)) /\ exists ff_q_mdr_append_scrb. b = ff_q_mdr_append_scrb * S ((S (mdr_i_append_sc)) * c) + (mdr_z_append_scr))))) /\ ((((forall ff_index_mdm_prefix_mdr_append_scm_positive. (exists ff_gap_mdm_lt_mdr_append_scm_positive_index_bound. ff_gap_mdm_lt_mdr_append_scm_positive_index_bound + S (ff_index_mdm_prefix_mdr_append_scm_positive) = ((mdr_q_append_s) * (mdr_q_append_s))) -> exists ff_row_mdm_prefix_mdr_append_scm_positive ff_column_mdm_prefix_mdr_append_scm_positive ff_value_mdm_prefix_mdr_append_scm_positive. (ff_index_mdm_prefix_mdr_append_scm_positive = (mdr_q_append_s) * ff_row_mdm_prefix_mdr_append_scm_positive + ff_column_mdm_prefix_mdr_append_scm_positive /\ ((exists ff_gap_mdm_lt_mdr_append_scm_positive_column_bound. ff_gap_mdm_lt_mdr_append_scm_positive_column_bound + S (ff_column_mdm_prefix_mdr_append_scm_positive) = (mdr_q_append_s)) /\ ((exists ff_row_mdm_cell_mdr_append_scm_positive_cell ff_column_mdm_cell_mdr_append_scm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_append_scm_positive_cell_row_before. ff_gap_mdm_lt_mdr_append_scm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_append_scm_positive) = (0)) /\ ff_row_mdm_cell_mdr_append_scm_positive_cell = ff_row_mdm_prefix_mdr_append_scm_positive) \/ ((exists ff_gap_mdm_le_mdr_append_scm_positive_cell_row_after. ff_gap_mdm_le_mdr_append_scm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_append_scm_positive)) /\ ff_row_mdm_cell_mdr_append_scm_positive_cell = S ff_row_mdm_prefix_mdr_append_scm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_append_scm_positive_cell_column_before. ff_gap_mdm_lt_mdr_append_scm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_append_scm_positive) = (mdr_j_append_sc)) /\ ff_column_mdm_cell_mdr_append_scm_positive_cell = ff_column_mdm_prefix_mdr_append_scm_positive) \/ ((exists ff_gap_mdm_le_mdr_append_scm_positive_cell_column_after. ff_gap_mdm_le_mdr_append_scm_positive_cell_column_after + (mdr_j_append_sc) = (ff_column_mdm_prefix_mdr_append_scm_positive)) /\ ff_column_mdm_cell_mdr_append_scm_positive_cell = S ff_column_mdm_prefix_mdr_append_scm_positive))) /\ (((exists ff_h_mdm_mdr_append_scm_positive_cell_source. ff_h_mdm_mdr_append_scm_positive_cell_source + S (ff_value_mdm_prefix_mdr_append_scm_positive) = S ((S ((ff_row_mdm_cell_mdr_append_scm_positive_cell) * (S (mdr_q_append_s)) + (ff_column_mdm_cell_mdr_append_scm_positive_cell))) * pc)) /\ exists ff_q_mdm_mdr_append_scm_positive_cell_source. pb = ff_q_mdm_mdr_append_scm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_append_scm_positive_cell) * (S (mdr_q_append_s)) + (ff_column_mdm_cell_mdr_append_scm_positive_cell))) * pc) + (ff_value_mdm_prefix_mdr_append_scm_positive)))))) /\ (((exists ff_h_mdm_mdr_append_scm_positive_target. ff_h_mdm_mdr_append_scm_positive_target + S (ff_value_mdm_prefix_mdr_append_scm_positive) = S ((S (ff_index_mdm_prefix_mdr_append_scm_positive)) * mdr_us_append_sc)) /\ exists ff_q_mdm_mdr_append_scm_positive_target. mdr_up_append_sc = ff_q_mdm_mdr_append_scm_positive_target * S ((S (ff_index_mdm_prefix_mdr_append_scm_positive)) * mdr_us_append_sc) + (ff_value_mdm_prefix_mdr_append_scm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_append_scm_negative. (exists ff_gap_mdm_lt_mdr_append_scm_negative_index_bound. ff_gap_mdm_lt_mdr_append_scm_negative_index_bound + S (ff_index_mdm_prefix_mdr_append_scm_negative) = ((mdr_q_append_s) * (mdr_q_append_s))) -> exists ff_row_mdm_prefix_mdr_append_scm_negative ff_column_mdm_prefix_mdr_append_scm_negative ff_value_mdm_prefix_mdr_append_scm_negative. (ff_index_mdm_prefix_mdr_append_scm_negative = (mdr_q_append_s) * ff_row_mdm_prefix_mdr_append_scm_negative + ff_column_mdm_prefix_mdr_append_scm_negative /\ ((exists ff_gap_mdm_lt_mdr_append_scm_negative_column_bound. ff_gap_mdm_lt_mdr_append_scm_negative_column_bound + S (ff_column_mdm_prefix_mdr_append_scm_negative) = (mdr_q_append_s)) /\ ((exists ff_row_mdm_cell_mdr_append_scm_negative_cell ff_column_mdm_cell_mdr_append_scm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_append_scm_negative_cell_row_before. ff_gap_mdm_lt_mdr_append_scm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_append_scm_negative) = (0)) /\ ff_row_mdm_cell_mdr_append_scm_negative_cell = ff_row_mdm_prefix_mdr_append_scm_negative) \/ ((exists ff_gap_mdm_le_mdr_append_scm_negative_cell_row_after. ff_gap_mdm_le_mdr_append_scm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_append_scm_negative)) /\ ff_row_mdm_cell_mdr_append_scm_negative_cell = S ff_row_mdm_prefix_mdr_append_scm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_append_scm_negative_cell_column_before. ff_gap_mdm_lt_mdr_append_scm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_append_scm_negative) = (mdr_j_append_sc)) /\ ff_column_mdm_cell_mdr_append_scm_negative_cell = ff_column_mdm_prefix_mdr_append_scm_negative) \/ ((exists ff_gap_mdm_le_mdr_append_scm_negative_cell_column_after. ff_gap_mdm_le_mdr_append_scm_negative_cell_column_after + (mdr_j_append_sc) = (ff_column_mdm_prefix_mdr_append_scm_negative)) /\ ff_column_mdm_cell_mdr_append_scm_negative_cell = S ff_column_mdm_prefix_mdr_append_scm_negative))) /\ (((exists ff_h_mdm_mdr_append_scm_negative_cell_source. ff_h_mdm_mdr_append_scm_negative_cell_source + S (ff_value_mdm_prefix_mdr_append_scm_negative) = S ((S ((ff_row_mdm_cell_mdr_append_scm_negative_cell) * (S (mdr_q_append_s)) + (ff_column_mdm_cell_mdr_append_scm_negative_cell))) * nc)) /\ exists ff_q_mdm_mdr_append_scm_negative_cell_source. nb = ff_q_mdm_mdr_append_scm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_append_scm_negative_cell) * (S (mdr_q_append_s)) + (ff_column_mdm_cell_mdr_append_scm_negative_cell))) * nc) + (ff_value_mdm_prefix_mdr_append_scm_negative)))))) /\ (((exists ff_h_mdm_mdr_append_scm_negative_target. ff_h_mdm_mdr_append_scm_negative_target + S (ff_value_mdm_prefix_mdr_append_scm_negative) = S ((S (ff_index_mdm_prefix_mdr_append_scm_negative)) * mdr_ut_append_sc)) /\ exists ff_q_mdm_mdr_append_scm_negative_target. mdr_un_append_sc = ff_q_mdm_mdr_append_scm_negative_target * S ((S (ff_index_mdm_prefix_mdr_append_scm_negative)) * mdr_ut_append_sc) + (ff_value_mdm_prefix_mdr_append_scm_negative))))))))) /\ ((((exists ff_h_mdr_append_scp. ff_h_mdr_append_scp + S (mdr_p_append_sc) = S ((S (mdr_j_append_sc)) * mdr_ec_append_s)) /\ exists ff_q_mdr_append_scp. mdr_eb_append_s = ff_q_mdr_append_scp * S ((S (mdr_j_append_sc)) * mdr_ec_append_s) + (mdr_p_append_sc))) /\ (((exists ff_h_mdr_append_scn. ff_h_mdr_append_scn + S (mdr_n_append_sc) = S ((S (mdr_j_append_sc)) * mdr_fc_append_s)) /\ exists ff_q_mdr_append_scn. mdr_fb_append_s = ff_q_mdr_append_scn * S ((S (mdr_j_append_sc)) * mdr_fc_append_s) + (mdr_n_append_sc)))))))) /\ (exists ff_ub_mce_fold_mdr_append_sf ff_uc_mce_fold_mdr_append_sf ff_vb_mce_fold_mdr_append_sf ff_vc_mce_fold_mdr_append_sf. ((forall ff_index_mce_alternating_mdr_append_sf_prefix. (exists ff_gap_mce_mdr_append_sf_prefix_index. ff_gap_mce_mdr_append_sf_prefix_index + S (ff_index_mce_alternating_mdr_append_sf_prefix) = (S (mdr_q_append_s))) -> exists ff_ap_mce_alternating_mdr_append_sf_prefix ff_an_mce_alternating_mdr_append_sf_prefix ff_bp_mce_alternating_mdr_append_sf_prefix ff_bn_mce_alternating_mdr_append_sf_prefix ff_p_mce_alternating_mdr_append_sf_prefix ff_n_mce_alternating_mdr_append_sf_prefix. ((((exists ff_h_mce_mdr_append_sf_prefix_ap. ff_h_mce_mdr_append_sf_prefix_ap + S (ff_ap_mce_alternating_mdr_append_sf_prefix) = S ((S (ff_index_mce_alternating_mdr_append_sf_prefix)) * pc)) /\ exists ff_q_mce_mdr_append_sf_prefix_ap. pb = ff_q_mce_mdr_append_sf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_append_sf_prefix)) * pc) + (ff_ap_mce_alternating_mdr_append_sf_prefix))) /\ ((((exists ff_h_mce_mdr_append_sf_prefix_an. ff_h_mce_mdr_append_sf_prefix_an + S (ff_an_mce_alternating_mdr_append_sf_prefix) = S ((S (ff_index_mce_alternating_mdr_append_sf_prefix)) * nc)) /\ exists ff_q_mce_mdr_append_sf_prefix_an. nb = ff_q_mce_mdr_append_sf_prefix_an * S ((S (ff_index_mce_alternating_mdr_append_sf_prefix)) * nc) + (ff_an_mce_alternating_mdr_append_sf_prefix))) /\ ((((exists ff_h_mce_mdr_append_sf_prefix_bp. ff_h_mce_mdr_append_sf_prefix_bp + S (ff_bp_mce_alternating_mdr_append_sf_prefix) = S ((S (ff_index_mce_alternating_mdr_append_sf_prefix)) * mdr_ec_append_s)) /\ exists ff_q_mce_mdr_append_sf_prefix_bp. mdr_eb_append_s = ff_q_mce_mdr_append_sf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_append_sf_prefix)) * mdr_ec_append_s) + (ff_bp_mce_alternating_mdr_append_sf_prefix))) /\ ((((exists ff_h_mce_mdr_append_sf_prefix_bn. ff_h_mce_mdr_append_sf_prefix_bn + S (ff_bn_mce_alternating_mdr_append_sf_prefix) = S ((S (ff_index_mce_alternating_mdr_append_sf_prefix)) * mdr_fc_append_s)) /\ exists ff_q_mce_mdr_append_sf_prefix_bn. mdr_fb_append_s = ff_q_mce_mdr_append_sf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_append_sf_prefix)) * mdr_fc_append_s) + (ff_bn_mce_alternating_mdr_append_sf_prefix))) /\ ((((exists ff_h_mce_mdr_append_sf_prefix_positive. ff_h_mce_mdr_append_sf_prefix_positive + S (ff_p_mce_alternating_mdr_append_sf_prefix) = S ((S (ff_index_mce_alternating_mdr_append_sf_prefix)) * ff_uc_mce_fold_mdr_append_sf)) /\ exists ff_q_mce_mdr_append_sf_prefix_positive. ff_ub_mce_fold_mdr_append_sf = ff_q_mce_mdr_append_sf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_append_sf_prefix)) * ff_uc_mce_fold_mdr_append_sf) + (ff_p_mce_alternating_mdr_append_sf_prefix))) /\ ((((exists ff_h_mce_mdr_append_sf_prefix_negative. ff_h_mce_mdr_append_sf_prefix_negative + S (ff_n_mce_alternating_mdr_append_sf_prefix) = S ((S (ff_index_mce_alternating_mdr_append_sf_prefix)) * ff_vc_mce_fold_mdr_append_sf)) /\ exists ff_q_mce_mdr_append_sf_prefix_negative. ff_vb_mce_fold_mdr_append_sf = ff_q_mce_mdr_append_sf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_append_sf_prefix)) * ff_vc_mce_fold_mdr_append_sf) + (ff_n_mce_alternating_mdr_append_sf_prefix))) /\ (((exists ff_even_mce_term_mdr_append_sf_prefix_term. ff_index_mce_alternating_mdr_append_sf_prefix = 2 * ff_even_mce_term_mdr_append_sf_prefix_term) /\ (ff_p_mce_alternating_mdr_append_sf_prefix = (ff_ap_mce_alternating_mdr_append_sf_prefix) * (ff_bp_mce_alternating_mdr_append_sf_prefix) + (ff_an_mce_alternating_mdr_append_sf_prefix) * (ff_bn_mce_alternating_mdr_append_sf_prefix) /\ ff_n_mce_alternating_mdr_append_sf_prefix = (ff_ap_mce_alternating_mdr_append_sf_prefix) * (ff_bn_mce_alternating_mdr_append_sf_prefix) + (ff_an_mce_alternating_mdr_append_sf_prefix) * (ff_bp_mce_alternating_mdr_append_sf_prefix))) \/ ((exists ff_odd_mce_term_mdr_append_sf_prefix_term. ff_index_mce_alternating_mdr_append_sf_prefix = 2 * ff_odd_mce_term_mdr_append_sf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_append_sf_prefix = (ff_ap_mce_alternating_mdr_append_sf_prefix) * (ff_bn_mce_alternating_mdr_append_sf_prefix) + (ff_an_mce_alternating_mdr_append_sf_prefix) * (ff_bp_mce_alternating_mdr_append_sf_prefix) /\ ff_n_mce_alternating_mdr_append_sf_prefix = (ff_ap_mce_alternating_mdr_append_sf_prefix) * (ff_bp_mce_alternating_mdr_append_sf_prefix) + (ff_an_mce_alternating_mdr_append_sf_prefix) * (ff_bn_mce_alternating_mdr_append_sf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_append_sf_positive ff_v_mce_mdr_append_sf_positive. ((((exists ff_h_mce_mdr_append_sf_positive_start. ff_h_mce_mdr_append_sf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_append_sf_positive)) /\ exists ff_q_mce_mdr_append_sf_positive_start. ff_u_mce_mdr_append_sf_positive = ff_q_mce_mdr_append_sf_positive_start * S ((S (0)) * ff_v_mce_mdr_append_sf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_append_sf_positive_terminal. ff_h_mce_mdr_append_sf_positive_terminal + S (p) = S ((S ((S (mdr_q_append_s)))) * ff_v_mce_mdr_append_sf_positive)) /\ exists ff_q_mce_mdr_append_sf_positive_terminal. ff_u_mce_mdr_append_sf_positive = ff_q_mce_mdr_append_sf_positive_terminal * S ((S ((S (mdr_q_append_s)))) * ff_v_mce_mdr_append_sf_positive) + (p))) /\ forall ff_i_mce_mdr_append_sf_positive. (exists ff_lt_mce_mdr_append_sf_positive_bound. ff_lt_mce_mdr_append_sf_positive_bound + S ff_i_mce_mdr_append_sf_positive = (S (mdr_q_append_s))) -> exists ff_a_mce_mdr_append_sf_positive ff_r_mce_mdr_append_sf_positive ff_s_mce_mdr_append_sf_positive. ((((exists ff_h_mce_mdr_append_sf_positive_summand. ff_h_mce_mdr_append_sf_positive_summand + S (ff_a_mce_mdr_append_sf_positive) = S ((S (ff_i_mce_mdr_append_sf_positive)) * ff_uc_mce_fold_mdr_append_sf)) /\ exists ff_q_mce_mdr_append_sf_positive_summand. ff_ub_mce_fold_mdr_append_sf = ff_q_mce_mdr_append_sf_positive_summand * S ((S (ff_i_mce_mdr_append_sf_positive)) * ff_uc_mce_fold_mdr_append_sf) + (ff_a_mce_mdr_append_sf_positive))) /\ ((((exists ff_h_mce_mdr_append_sf_positive_partial. ff_h_mce_mdr_append_sf_positive_partial + S (ff_r_mce_mdr_append_sf_positive) = S ((S (ff_i_mce_mdr_append_sf_positive)) * ff_v_mce_mdr_append_sf_positive)) /\ exists ff_q_mce_mdr_append_sf_positive_partial. ff_u_mce_mdr_append_sf_positive = ff_q_mce_mdr_append_sf_positive_partial * S ((S (ff_i_mce_mdr_append_sf_positive)) * ff_v_mce_mdr_append_sf_positive) + (ff_r_mce_mdr_append_sf_positive))) /\ ((((exists ff_h_mce_mdr_append_sf_positive_successor. ff_h_mce_mdr_append_sf_positive_successor + S (ff_s_mce_mdr_append_sf_positive) = S ((S (S ff_i_mce_mdr_append_sf_positive)) * ff_v_mce_mdr_append_sf_positive)) /\ exists ff_q_mce_mdr_append_sf_positive_successor. ff_u_mce_mdr_append_sf_positive = ff_q_mce_mdr_append_sf_positive_successor * S ((S (S ff_i_mce_mdr_append_sf_positive)) * ff_v_mce_mdr_append_sf_positive) + (ff_s_mce_mdr_append_sf_positive))) /\ ff_s_mce_mdr_append_sf_positive = ff_r_mce_mdr_append_sf_positive + ff_a_mce_mdr_append_sf_positive)))))) /\ (exists ff_u_mce_mdr_append_sf_negative ff_v_mce_mdr_append_sf_negative. ((((exists ff_h_mce_mdr_append_sf_negative_start. ff_h_mce_mdr_append_sf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_append_sf_negative)) /\ exists ff_q_mce_mdr_append_sf_negative_start. ff_u_mce_mdr_append_sf_negative = ff_q_mce_mdr_append_sf_negative_start * S ((S (0)) * ff_v_mce_mdr_append_sf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_append_sf_negative_terminal. ff_h_mce_mdr_append_sf_negative_terminal + S (n) = S ((S ((S (mdr_q_append_s)))) * ff_v_mce_mdr_append_sf_negative)) /\ exists ff_q_mce_mdr_append_sf_negative_terminal. ff_u_mce_mdr_append_sf_negative = ff_q_mce_mdr_append_sf_negative_terminal * S ((S ((S (mdr_q_append_s)))) * ff_v_mce_mdr_append_sf_negative) + (n))) /\ forall ff_i_mce_mdr_append_sf_negative. (exists ff_lt_mce_mdr_append_sf_negative_bound. ff_lt_mce_mdr_append_sf_negative_bound + S ff_i_mce_mdr_append_sf_negative = (S (mdr_q_append_s))) -> exists ff_a_mce_mdr_append_sf_negative ff_r_mce_mdr_append_sf_negative ff_s_mce_mdr_append_sf_negative. ((((exists ff_h_mce_mdr_append_sf_negative_summand. ff_h_mce_mdr_append_sf_negative_summand + S (ff_a_mce_mdr_append_sf_negative) = S ((S (ff_i_mce_mdr_append_sf_negative)) * ff_vc_mce_fold_mdr_append_sf)) /\ exists ff_q_mce_mdr_append_sf_negative_summand. ff_vb_mce_fold_mdr_append_sf = ff_q_mce_mdr_append_sf_negative_summand * S ((S (ff_i_mce_mdr_append_sf_negative)) * ff_vc_mce_fold_mdr_append_sf) + (ff_a_mce_mdr_append_sf_negative))) /\ ((((exists ff_h_mce_mdr_append_sf_negative_partial. ff_h_mce_mdr_append_sf_negative_partial + S (ff_r_mce_mdr_append_sf_negative) = S ((S (ff_i_mce_mdr_append_sf_negative)) * ff_v_mce_mdr_append_sf_negative)) /\ exists ff_q_mce_mdr_append_sf_negative_partial. ff_u_mce_mdr_append_sf_negative = ff_q_mce_mdr_append_sf_negative_partial * S ((S (ff_i_mce_mdr_append_sf_negative)) * ff_v_mce_mdr_append_sf_negative) + (ff_r_mce_mdr_append_sf_negative))) /\ ((((exists ff_h_mce_mdr_append_sf_negative_successor. ff_h_mce_mdr_append_sf_negative_successor + S (ff_s_mce_mdr_append_sf_negative) = S ((S (S ff_i_mce_mdr_append_sf_negative)) * ff_v_mce_mdr_append_sf_negative)) /\ exists ff_q_mce_mdr_append_sf_negative_successor. ff_u_mce_mdr_append_sf_negative = ff_q_mce_mdr_append_sf_negative_successor * S ((S (S ff_i_mce_mdr_append_sf_negative)) * ff_v_mce_mdr_append_sf_negative) + (ff_s_mce_mdr_append_sf_negative))) /\ ff_s_mce_mdr_append_sf_negative = ff_r_mce_mdr_append_sf_negative + ff_a_mce_mdr_append_sf_negative))))))))))))) -> exists u v. ((forall mdr_i_append_p mdr_a_append_p. (exists mdr_gap_append_pb. mdr_gap_append_pb + S (mdr_i_append_p) = (l)) -> (((exists ff_h_mdr_append_po. ff_h_mdr_append_po + S (mdr_a_append_p) = S ((S (mdr_i_append_p)) * c)) /\ exists ff_q_mdr_append_po. b = ff_q_mdr_append_po * S ((S (mdr_i_append_p)) * c) + (mdr_a_append_p))) -> (((exists ff_h_mdr_append_pn. ff_h_mdr_append_pn + S (mdr_a_append_p) = S ((S (mdr_i_append_p)) * v)) /\ exists ff_q_mdr_append_pn. u = ff_q_mdr_append_pn * S ((S (mdr_i_append_p)) * v) + (mdr_a_append_p)))) /\ ((forall mdr_i_append_h. (exists mdr_gap_append_hi. mdr_gap_append_hi + S (mdr_i_append_h) = (S l)) -> exists mdr_d_append_h mdr_pb_append_h mdr_pc_append_h mdr_nb_append_h mdr_nc_append_h mdr_p_append_h mdr_n_append_h. ((exists mdr_z_append_hr. ((exists mdr_a_append_hrc mdr_b_append_hrc mdr_c_append_hrc mdr_e_append_hrc mdr_f_append_hrc. ((mdr_a_append_hrc = ((mdr_d_append_h) + (mdr_pb_append_h)) * S ((mdr_d_append_h) + (mdr_pb_append_h)) + ((mdr_pb_append_h) + (mdr_pb_append_h))) /\ ((mdr_b_append_hrc = ((mdr_pc_append_h) + (mdr_nb_append_h)) * S ((mdr_pc_append_h) + (mdr_nb_append_h)) + ((mdr_nb_append_h) + (mdr_nb_append_h))) /\ ((mdr_c_append_hrc = ((mdr_a_append_hrc) + (mdr_b_append_hrc)) * S ((mdr_a_append_hrc) + (mdr_b_append_hrc)) + ((mdr_b_append_hrc) + (mdr_b_append_hrc))) /\ ((mdr_e_append_hrc = ((mdr_p_append_h) + (mdr_n_append_h)) * S ((mdr_p_append_h) + (mdr_n_append_h)) + ((mdr_n_append_h) + (mdr_n_append_h))) /\ ((mdr_f_append_hrc = ((mdr_nc_append_h) + (mdr_e_append_hrc)) * S ((mdr_nc_append_h) + (mdr_e_append_hrc)) + ((mdr_e_append_hrc) + (mdr_e_append_hrc))) /\ ((mdr_z_append_hr) = ((mdr_c_append_hrc) + (mdr_f_append_hrc)) * S ((mdr_c_append_hrc) + (mdr_f_append_hrc)) + ((mdr_f_append_hrc) + (mdr_f_append_hrc))))))))) /\ (((exists ff_h_mdr_append_hrb. ff_h_mdr_append_hrb + S (mdr_z_append_hr) = S ((S (mdr_i_append_h)) * v)) /\ exists ff_q_mdr_append_hrb. u = ff_q_mdr_append_hrb * S ((S (mdr_i_append_h)) * v) + (mdr_z_append_hr))))) /\ (((((mdr_d_append_h) = 0) /\ (((mdr_p_append_h) = 1) /\ ((mdr_n_append_h) = 0))) \/ exists mdr_q_append_hs mdr_eb_append_hs mdr_ec_append_hs mdr_fb_append_hs mdr_fc_append_hs. (((mdr_d_append_h) = S (mdr_q_append_hs)) /\ ((forall mdr_j_append_hsc. (exists mdr_gap_append_hscj. mdr_gap_append_hscj + S (mdr_j_append_hsc) = (S (mdr_q_append_hs))) -> exists mdr_i_append_hsc mdr_up_append_hsc mdr_us_append_hsc mdr_un_append_hsc mdr_ut_append_hsc mdr_p_append_hsc mdr_n_append_hsc. ((exists mdr_gap_append_hsci. mdr_gap_append_hsci + S (mdr_i_append_hsc) = (mdr_i_append_h)) /\ ((exists mdr_z_append_hscr. ((exists mdr_a_append_hscrc mdr_b_append_hscrc mdr_c_append_hscrc mdr_e_append_hscrc mdr_f_append_hscrc. ((mdr_a_append_hscrc = ((mdr_q_append_hs) + (mdr_up_append_hsc)) * S ((mdr_q_append_hs) + (mdr_up_append_hsc)) + ((mdr_up_append_hsc) + (mdr_up_append_hsc))) /\ ((mdr_b_append_hscrc = ((mdr_us_append_hsc) + (mdr_un_append_hsc)) * S ((mdr_us_append_hsc) + (mdr_un_append_hsc)) + ((mdr_un_append_hsc) + (mdr_un_append_hsc))) /\ ((mdr_c_append_hscrc = ((mdr_a_append_hscrc) + (mdr_b_append_hscrc)) * S ((mdr_a_append_hscrc) + (mdr_b_append_hscrc)) + ((mdr_b_append_hscrc) + (mdr_b_append_hscrc))) /\ ((mdr_e_append_hscrc = ((mdr_p_append_hsc) + (mdr_n_append_hsc)) * S ((mdr_p_append_hsc) + (mdr_n_append_hsc)) + ((mdr_n_append_hsc) + (mdr_n_append_hsc))) /\ ((mdr_f_append_hscrc = ((mdr_ut_append_hsc) + (mdr_e_append_hscrc)) * S ((mdr_ut_append_hsc) + (mdr_e_append_hscrc)) + ((mdr_e_append_hscrc) + (mdr_e_append_hscrc))) /\ ((mdr_z_append_hscr) = ((mdr_c_append_hscrc) + (mdr_f_append_hscrc)) * S ((mdr_c_append_hscrc) + (mdr_f_append_hscrc)) + ((mdr_f_append_hscrc) + (mdr_f_append_hscrc))))))))) /\ (((exists ff_h_mdr_append_hscrb. ff_h_mdr_append_hscrb + S (mdr_z_append_hscr) = S ((S (mdr_i_append_hsc)) * v)) /\ exists ff_q_mdr_append_hscrb. u = ff_q_mdr_append_hscrb * S ((S (mdr_i_append_hsc)) * v) + (mdr_z_append_hscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_append_hscm_positive. (exists ff_gap_mdm_lt_mdr_append_hscm_positive_index_bound. ff_gap_mdm_lt_mdr_append_hscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_append_hscm_positive) = ((mdr_q_append_hs) * (mdr_q_append_hs))) -> exists ff_row_mdm_prefix_mdr_append_hscm_positive ff_column_mdm_prefix_mdr_append_hscm_positive ff_value_mdm_prefix_mdr_append_hscm_positive. (ff_index_mdm_prefix_mdr_append_hscm_positive = (mdr_q_append_hs) * ff_row_mdm_prefix_mdr_append_hscm_positive + ff_column_mdm_prefix_mdr_append_hscm_positive /\ ((exists ff_gap_mdm_lt_mdr_append_hscm_positive_column_bound. ff_gap_mdm_lt_mdr_append_hscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_append_hscm_positive) = (mdr_q_append_hs)) /\ ((exists ff_row_mdm_cell_mdr_append_hscm_positive_cell ff_column_mdm_cell_mdr_append_hscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_append_hscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_append_hscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_append_hscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_append_hscm_positive_cell = ff_row_mdm_prefix_mdr_append_hscm_positive) \/ ((exists ff_gap_mdm_le_mdr_append_hscm_positive_cell_row_after. ff_gap_mdm_le_mdr_append_hscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_append_hscm_positive)) /\ ff_row_mdm_cell_mdr_append_hscm_positive_cell = S ff_row_mdm_prefix_mdr_append_hscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_append_hscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_append_hscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_append_hscm_positive) = (mdr_j_append_hsc)) /\ ff_column_mdm_cell_mdr_append_hscm_positive_cell = ff_column_mdm_prefix_mdr_append_hscm_positive) \/ ((exists ff_gap_mdm_le_mdr_append_hscm_positive_cell_column_after. ff_gap_mdm_le_mdr_append_hscm_positive_cell_column_after + (mdr_j_append_hsc) = (ff_column_mdm_prefix_mdr_append_hscm_positive)) /\ ff_column_mdm_cell_mdr_append_hscm_positive_cell = S ff_column_mdm_prefix_mdr_append_hscm_positive))) /\ (((exists ff_h_mdm_mdr_append_hscm_positive_cell_source. ff_h_mdm_mdr_append_hscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_append_hscm_positive) = S ((S ((ff_row_mdm_cell_mdr_append_hscm_positive_cell) * (S (mdr_q_append_hs)) + (ff_column_mdm_cell_mdr_append_hscm_positive_cell))) * mdr_pc_append_h)) /\ exists ff_q_mdm_mdr_append_hscm_positive_cell_source. mdr_pb_append_h = ff_q_mdm_mdr_append_hscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_append_hscm_positive_cell) * (S (mdr_q_append_hs)) + (ff_column_mdm_cell_mdr_append_hscm_positive_cell))) * mdr_pc_append_h) + (ff_value_mdm_prefix_mdr_append_hscm_positive)))))) /\ (((exists ff_h_mdm_mdr_append_hscm_positive_target. ff_h_mdm_mdr_append_hscm_positive_target + S (ff_value_mdm_prefix_mdr_append_hscm_positive) = S ((S (ff_index_mdm_prefix_mdr_append_hscm_positive)) * mdr_us_append_hsc)) /\ exists ff_q_mdm_mdr_append_hscm_positive_target. mdr_up_append_hsc = ff_q_mdm_mdr_append_hscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_append_hscm_positive)) * mdr_us_append_hsc) + (ff_value_mdm_prefix_mdr_append_hscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_append_hscm_negative. (exists ff_gap_mdm_lt_mdr_append_hscm_negative_index_bound. ff_gap_mdm_lt_mdr_append_hscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_append_hscm_negative) = ((mdr_q_append_hs) * (mdr_q_append_hs))) -> exists ff_row_mdm_prefix_mdr_append_hscm_negative ff_column_mdm_prefix_mdr_append_hscm_negative ff_value_mdm_prefix_mdr_append_hscm_negative. (ff_index_mdm_prefix_mdr_append_hscm_negative = (mdr_q_append_hs) * ff_row_mdm_prefix_mdr_append_hscm_negative + ff_column_mdm_prefix_mdr_append_hscm_negative /\ ((exists ff_gap_mdm_lt_mdr_append_hscm_negative_column_bound. ff_gap_mdm_lt_mdr_append_hscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_append_hscm_negative) = (mdr_q_append_hs)) /\ ((exists ff_row_mdm_cell_mdr_append_hscm_negative_cell ff_column_mdm_cell_mdr_append_hscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_append_hscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_append_hscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_append_hscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_append_hscm_negative_cell = ff_row_mdm_prefix_mdr_append_hscm_negative) \/ ((exists ff_gap_mdm_le_mdr_append_hscm_negative_cell_row_after. ff_gap_mdm_le_mdr_append_hscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_append_hscm_negative)) /\ ff_row_mdm_cell_mdr_append_hscm_negative_cell = S ff_row_mdm_prefix_mdr_append_hscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_append_hscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_append_hscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_append_hscm_negative) = (mdr_j_append_hsc)) /\ ff_column_mdm_cell_mdr_append_hscm_negative_cell = ff_column_mdm_prefix_mdr_append_hscm_negative) \/ ((exists ff_gap_mdm_le_mdr_append_hscm_negative_cell_column_after. ff_gap_mdm_le_mdr_append_hscm_negative_cell_column_after + (mdr_j_append_hsc) = (ff_column_mdm_prefix_mdr_append_hscm_negative)) /\ ff_column_mdm_cell_mdr_append_hscm_negative_cell = S ff_column_mdm_prefix_mdr_append_hscm_negative))) /\ (((exists ff_h_mdm_mdr_append_hscm_negative_cell_source. ff_h_mdm_mdr_append_hscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_append_hscm_negative) = S ((S ((ff_row_mdm_cell_mdr_append_hscm_negative_cell) * (S (mdr_q_append_hs)) + (ff_column_mdm_cell_mdr_append_hscm_negative_cell))) * mdr_nc_append_h)) /\ exists ff_q_mdm_mdr_append_hscm_negative_cell_source. mdr_nb_append_h = ff_q_mdm_mdr_append_hscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_append_hscm_negative_cell) * (S (mdr_q_append_hs)) + (ff_column_mdm_cell_mdr_append_hscm_negative_cell))) * mdr_nc_append_h) + (ff_value_mdm_prefix_mdr_append_hscm_negative)))))) /\ (((exists ff_h_mdm_mdr_append_hscm_negative_target. ff_h_mdm_mdr_append_hscm_negative_target + S (ff_value_mdm_prefix_mdr_append_hscm_negative) = S ((S (ff_index_mdm_prefix_mdr_append_hscm_negative)) * mdr_ut_append_hsc)) /\ exists ff_q_mdm_mdr_append_hscm_negative_target. mdr_un_append_hsc = ff_q_mdm_mdr_append_hscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_append_hscm_negative)) * mdr_ut_append_hsc) + (ff_value_mdm_prefix_mdr_append_hscm_negative))))))))) /\ ((((exists ff_h_mdr_append_hscp. ff_h_mdr_append_hscp + S (mdr_p_append_hsc) = S ((S (mdr_j_append_hsc)) * mdr_ec_append_hs)) /\ exists ff_q_mdr_append_hscp. mdr_eb_append_hs = ff_q_mdr_append_hscp * S ((S (mdr_j_append_hsc)) * mdr_ec_append_hs) + (mdr_p_append_hsc))) /\ (((exists ff_h_mdr_append_hscn. ff_h_mdr_append_hscn + S (mdr_n_append_hsc) = S ((S (mdr_j_append_hsc)) * mdr_fc_append_hs)) /\ exists ff_q_mdr_append_hscn. mdr_fb_append_hs = ff_q_mdr_append_hscn * S ((S (mdr_j_append_hsc)) * mdr_fc_append_hs) + (mdr_n_append_hsc)))))))) /\ (exists ff_ub_mce_fold_mdr_append_hsf ff_uc_mce_fold_mdr_append_hsf ff_vb_mce_fold_mdr_append_hsf ff_vc_mce_fold_mdr_append_hsf. ((forall ff_index_mce_alternating_mdr_append_hsf_prefix. (exists ff_gap_mce_mdr_append_hsf_prefix_index. ff_gap_mce_mdr_append_hsf_prefix_index + S (ff_index_mce_alternating_mdr_append_hsf_prefix) = (S (mdr_q_append_hs))) -> exists ff_ap_mce_alternating_mdr_append_hsf_prefix ff_an_mce_alternating_mdr_append_hsf_prefix ff_bp_mce_alternating_mdr_append_hsf_prefix ff_bn_mce_alternating_mdr_append_hsf_prefix ff_p_mce_alternating_mdr_append_hsf_prefix ff_n_mce_alternating_mdr_append_hsf_prefix. ((((exists ff_h_mce_mdr_append_hsf_prefix_ap. ff_h_mce_mdr_append_hsf_prefix_ap + S (ff_ap_mce_alternating_mdr_append_hsf_prefix) = S ((S (ff_index_mce_alternating_mdr_append_hsf_prefix)) * mdr_pc_append_h)) /\ exists ff_q_mce_mdr_append_hsf_prefix_ap. mdr_pb_append_h = ff_q_mce_mdr_append_hsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_append_hsf_prefix)) * mdr_pc_append_h) + (ff_ap_mce_alternating_mdr_append_hsf_prefix))) /\ ((((exists ff_h_mce_mdr_append_hsf_prefix_an. ff_h_mce_mdr_append_hsf_prefix_an + S (ff_an_mce_alternating_mdr_append_hsf_prefix) = S ((S (ff_index_mce_alternating_mdr_append_hsf_prefix)) * mdr_nc_append_h)) /\ exists ff_q_mce_mdr_append_hsf_prefix_an. mdr_nb_append_h = ff_q_mce_mdr_append_hsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_append_hsf_prefix)) * mdr_nc_append_h) + (ff_an_mce_alternating_mdr_append_hsf_prefix))) /\ ((((exists ff_h_mce_mdr_append_hsf_prefix_bp. ff_h_mce_mdr_append_hsf_prefix_bp + S (ff_bp_mce_alternating_mdr_append_hsf_prefix) = S ((S (ff_index_mce_alternating_mdr_append_hsf_prefix)) * mdr_ec_append_hs)) /\ exists ff_q_mce_mdr_append_hsf_prefix_bp. mdr_eb_append_hs = ff_q_mce_mdr_append_hsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_append_hsf_prefix)) * mdr_ec_append_hs) + (ff_bp_mce_alternating_mdr_append_hsf_prefix))) /\ ((((exists ff_h_mce_mdr_append_hsf_prefix_bn. ff_h_mce_mdr_append_hsf_prefix_bn + S (ff_bn_mce_alternating_mdr_append_hsf_prefix) = S ((S (ff_index_mce_alternating_mdr_append_hsf_prefix)) * mdr_fc_append_hs)) /\ exists ff_q_mce_mdr_append_hsf_prefix_bn. mdr_fb_append_hs = ff_q_mce_mdr_append_hsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_append_hsf_prefix)) * mdr_fc_append_hs) + (ff_bn_mce_alternating_mdr_append_hsf_prefix))) /\ ((((exists ff_h_mce_mdr_append_hsf_prefix_positive. ff_h_mce_mdr_append_hsf_prefix_positive + S (ff_p_mce_alternating_mdr_append_hsf_prefix) = S ((S (ff_index_mce_alternating_mdr_append_hsf_prefix)) * ff_uc_mce_fold_mdr_append_hsf)) /\ exists ff_q_mce_mdr_append_hsf_prefix_positive. ff_ub_mce_fold_mdr_append_hsf = ff_q_mce_mdr_append_hsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_append_hsf_prefix)) * ff_uc_mce_fold_mdr_append_hsf) + (ff_p_mce_alternating_mdr_append_hsf_prefix))) /\ ((((exists ff_h_mce_mdr_append_hsf_prefix_negative. ff_h_mce_mdr_append_hsf_prefix_negative + S (ff_n_mce_alternating_mdr_append_hsf_prefix) = S ((S (ff_index_mce_alternating_mdr_append_hsf_prefix)) * ff_vc_mce_fold_mdr_append_hsf)) /\ exists ff_q_mce_mdr_append_hsf_prefix_negative. ff_vb_mce_fold_mdr_append_hsf = ff_q_mce_mdr_append_hsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_append_hsf_prefix)) * ff_vc_mce_fold_mdr_append_hsf) + (ff_n_mce_alternating_mdr_append_hsf_prefix))) /\ (((exists ff_even_mce_term_mdr_append_hsf_prefix_term. ff_index_mce_alternating_mdr_append_hsf_prefix = 2 * ff_even_mce_term_mdr_append_hsf_prefix_term) /\ (ff_p_mce_alternating_mdr_append_hsf_prefix = (ff_ap_mce_alternating_mdr_append_hsf_prefix) * (ff_bp_mce_alternating_mdr_append_hsf_prefix) + (ff_an_mce_alternating_mdr_append_hsf_prefix) * (ff_bn_mce_alternating_mdr_append_hsf_prefix) /\ ff_n_mce_alternating_mdr_append_hsf_prefix = (ff_ap_mce_alternating_mdr_append_hsf_prefix) * (ff_bn_mce_alternating_mdr_append_hsf_prefix) + (ff_an_mce_alternating_mdr_append_hsf_prefix) * (ff_bp_mce_alternating_mdr_append_hsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_append_hsf_prefix_term. ff_index_mce_alternating_mdr_append_hsf_prefix = 2 * ff_odd_mce_term_mdr_append_hsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_append_hsf_prefix = (ff_ap_mce_alternating_mdr_append_hsf_prefix) * (ff_bn_mce_alternating_mdr_append_hsf_prefix) + (ff_an_mce_alternating_mdr_append_hsf_prefix) * (ff_bp_mce_alternating_mdr_append_hsf_prefix) /\ ff_n_mce_alternating_mdr_append_hsf_prefix = (ff_ap_mce_alternating_mdr_append_hsf_prefix) * (ff_bp_mce_alternating_mdr_append_hsf_prefix) + (ff_an_mce_alternating_mdr_append_hsf_prefix) * (ff_bn_mce_alternating_mdr_append_hsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_append_hsf_positive ff_v_mce_mdr_append_hsf_positive. ((((exists ff_h_mce_mdr_append_hsf_positive_start. ff_h_mce_mdr_append_hsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_append_hsf_positive)) /\ exists ff_q_mce_mdr_append_hsf_positive_start. ff_u_mce_mdr_append_hsf_positive = ff_q_mce_mdr_append_hsf_positive_start * S ((S (0)) * ff_v_mce_mdr_append_hsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_append_hsf_positive_terminal. ff_h_mce_mdr_append_hsf_positive_terminal + S (mdr_p_append_h) = S ((S ((S (mdr_q_append_hs)))) * ff_v_mce_mdr_append_hsf_positive)) /\ exists ff_q_mce_mdr_append_hsf_positive_terminal. ff_u_mce_mdr_append_hsf_positive = ff_q_mce_mdr_append_hsf_positive_terminal * S ((S ((S (mdr_q_append_hs)))) * ff_v_mce_mdr_append_hsf_positive) + (mdr_p_append_h))) /\ forall ff_i_mce_mdr_append_hsf_positive. (exists ff_lt_mce_mdr_append_hsf_positive_bound. ff_lt_mce_mdr_append_hsf_positive_bound + S ff_i_mce_mdr_append_hsf_positive = (S (mdr_q_append_hs))) -> exists ff_a_mce_mdr_append_hsf_positive ff_r_mce_mdr_append_hsf_positive ff_s_mce_mdr_append_hsf_positive. ((((exists ff_h_mce_mdr_append_hsf_positive_summand. ff_h_mce_mdr_append_hsf_positive_summand + S (ff_a_mce_mdr_append_hsf_positive) = S ((S (ff_i_mce_mdr_append_hsf_positive)) * ff_uc_mce_fold_mdr_append_hsf)) /\ exists ff_q_mce_mdr_append_hsf_positive_summand. ff_ub_mce_fold_mdr_append_hsf = ff_q_mce_mdr_append_hsf_positive_summand * S ((S (ff_i_mce_mdr_append_hsf_positive)) * ff_uc_mce_fold_mdr_append_hsf) + (ff_a_mce_mdr_append_hsf_positive))) /\ ((((exists ff_h_mce_mdr_append_hsf_positive_partial. ff_h_mce_mdr_append_hsf_positive_partial + S (ff_r_mce_mdr_append_hsf_positive) = S ((S (ff_i_mce_mdr_append_hsf_positive)) * ff_v_mce_mdr_append_hsf_positive)) /\ exists ff_q_mce_mdr_append_hsf_positive_partial. ff_u_mce_mdr_append_hsf_positive = ff_q_mce_mdr_append_hsf_positive_partial * S ((S (ff_i_mce_mdr_append_hsf_positive)) * ff_v_mce_mdr_append_hsf_positive) + (ff_r_mce_mdr_append_hsf_positive))) /\ ((((exists ff_h_mce_mdr_append_hsf_positive_successor. ff_h_mce_mdr_append_hsf_positive_successor + S (ff_s_mce_mdr_append_hsf_positive) = S ((S (S ff_i_mce_mdr_append_hsf_positive)) * ff_v_mce_mdr_append_hsf_positive)) /\ exists ff_q_mce_mdr_append_hsf_positive_successor. ff_u_mce_mdr_append_hsf_positive = ff_q_mce_mdr_append_hsf_positive_successor * S ((S (S ff_i_mce_mdr_append_hsf_positive)) * ff_v_mce_mdr_append_hsf_positive) + (ff_s_mce_mdr_append_hsf_positive))) /\ ff_s_mce_mdr_append_hsf_positive = ff_r_mce_mdr_append_hsf_positive + ff_a_mce_mdr_append_hsf_positive)))))) /\ (exists ff_u_mce_mdr_append_hsf_negative ff_v_mce_mdr_append_hsf_negative. ((((exists ff_h_mce_mdr_append_hsf_negative_start. ff_h_mce_mdr_append_hsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_append_hsf_negative)) /\ exists ff_q_mce_mdr_append_hsf_negative_start. ff_u_mce_mdr_append_hsf_negative = ff_q_mce_mdr_append_hsf_negative_start * S ((S (0)) * ff_v_mce_mdr_append_hsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_append_hsf_negative_terminal. ff_h_mce_mdr_append_hsf_negative_terminal + S (mdr_n_append_h) = S ((S ((S (mdr_q_append_hs)))) * ff_v_mce_mdr_append_hsf_negative)) /\ exists ff_q_mce_mdr_append_hsf_negative_terminal. ff_u_mce_mdr_append_hsf_negative = ff_q_mce_mdr_append_hsf_negative_terminal * S ((S ((S (mdr_q_append_hs)))) * ff_v_mce_mdr_append_hsf_negative) + (mdr_n_append_h))) /\ forall ff_i_mce_mdr_append_hsf_negative. (exists ff_lt_mce_mdr_append_hsf_negative_bound. ff_lt_mce_mdr_append_hsf_negative_bound + S ff_i_mce_mdr_append_hsf_negative = (S (mdr_q_append_hs))) -> exists ff_a_mce_mdr_append_hsf_negative ff_r_mce_mdr_append_hsf_negative ff_s_mce_mdr_append_hsf_negative. ((((exists ff_h_mce_mdr_append_hsf_negative_summand. ff_h_mce_mdr_append_hsf_negative_summand + S (ff_a_mce_mdr_append_hsf_negative) = S ((S (ff_i_mce_mdr_append_hsf_negative)) * ff_vc_mce_fold_mdr_append_hsf)) /\ exists ff_q_mce_mdr_append_hsf_negative_summand. ff_vb_mce_fold_mdr_append_hsf = ff_q_mce_mdr_append_hsf_negative_summand * S ((S (ff_i_mce_mdr_append_hsf_negative)) * ff_vc_mce_fold_mdr_append_hsf) + (ff_a_mce_mdr_append_hsf_negative))) /\ ((((exists ff_h_mce_mdr_append_hsf_negative_partial. ff_h_mce_mdr_append_hsf_negative_partial + S (ff_r_mce_mdr_append_hsf_negative) = S ((S (ff_i_mce_mdr_append_hsf_negative)) * ff_v_mce_mdr_append_hsf_negative)) /\ exists ff_q_mce_mdr_append_hsf_negative_partial. ff_u_mce_mdr_append_hsf_negative = ff_q_mce_mdr_append_hsf_negative_partial * S ((S (ff_i_mce_mdr_append_hsf_negative)) * ff_v_mce_mdr_append_hsf_negative) + (ff_r_mce_mdr_append_hsf_negative))) /\ ((((exists ff_h_mce_mdr_append_hsf_negative_successor. ff_h_mce_mdr_append_hsf_negative_successor + S (ff_s_mce_mdr_append_hsf_negative) = S ((S (S ff_i_mce_mdr_append_hsf_negative)) * ff_v_mce_mdr_append_hsf_negative)) /\ exists ff_q_mce_mdr_append_hsf_negative_successor. ff_u_mce_mdr_append_hsf_negative = ff_q_mce_mdr_append_hsf_negative_successor * S ((S (S ff_i_mce_mdr_append_hsf_negative)) * ff_v_mce_mdr_append_hsf_negative) + (ff_s_mce_mdr_append_hsf_negative))) /\ ff_s_mce_mdr_append_hsf_negative = ff_r_mce_mdr_append_hsf_negative + ff_a_mce_mdr_append_hsf_negative))))))))))))))) /\ (exists mdr_z_append_r. ((exists mdr_a_append_rc mdr_b_append_rc mdr_c_append_rc mdr_e_append_rc mdr_f_append_rc. ((mdr_a_append_rc = ((d) + (pb)) * S ((d) + (pb)) + ((pb) + (pb))) /\ ((mdr_b_append_rc = ((pc) + (nb)) * S ((pc) + (nb)) + ((nb) + (nb))) /\ ((mdr_c_append_rc = ((mdr_a_append_rc) + (mdr_b_append_rc)) * S ((mdr_a_append_rc) + (mdr_b_append_rc)) + ((mdr_b_append_rc) + (mdr_b_append_rc))) /\ ((mdr_e_append_rc = ((p) + (n)) * S ((p) + (n)) + ((n) + (n))) /\ ((mdr_f_append_rc = ((nc) + (mdr_e_append_rc)) * S ((nc) + (mdr_e_append_rc)) + ((mdr_e_append_rc) + (mdr_e_append_rc))) /\ ((mdr_z_append_r) = ((mdr_c_append_rc) + (mdr_f_append_rc)) * S ((mdr_c_append_rc) + (mdr_f_append_rc)) + ((mdr_f_append_rc) + (mdr_f_append_rc))))))))) /\ (((exists ff_h_mdr_append_rb. ff_h_mdr_append_rb + S (mdr_z_append_r) = S ((S (l)) * v)) /\ exists ff_q_mdr_append_rb. u = ff_q_mdr_append_rb * S ((S (l)) * v) + (mdr_z_append_r)))))))