matrix_recursive_cofactor_prefix_from_recursion

Exact expanded first-order arithmetic statement

forall q pb pc nb nc b c l k. (forall mdr_pb_recursion mdr_pc_recursion mdr_nb_recursion mdr_nc_recursion mdr_b_recursion mdr_c_recursion mdr_l_recursion. (forall mdr_i_recursionh. (exists mdr_gap_recursionhi. mdr_gap_recursionhi + S (mdr_i_recursionh) = (mdr_l_recursion)) -> exists mdr_d_recursionh mdr_pb_recursionh mdr_pc_recursionh mdr_nb_recursionh mdr_nc_recursionh mdr_p_recursionh mdr_n_recursionh. ((exists mdr_z_recursionhr. ((exists mdr_a_recursionhrc mdr_b_recursionhrc mdr_c_recursionhrc mdr_e_recursionhrc mdr_f_recursionhrc. ((mdr_a_recursionhrc = ((mdr_d_recursionh) + (mdr_pb_recursionh)) * S ((mdr_d_recursionh) + (mdr_pb_recursionh)) + ((mdr_pb_recursionh) + (mdr_pb_recursionh))) /\ ((mdr_b_recursionhrc = ((mdr_pc_recursionh) + (mdr_nb_recursionh)) * S ((mdr_pc_recursionh) + (mdr_nb_recursionh)) + ((mdr_nb_recursionh) + (mdr_nb_recursionh))) /\ ((mdr_c_recursionhrc = ((mdr_a_recursionhrc) + (mdr_b_recursionhrc)) * S ((mdr_a_recursionhrc) + (mdr_b_recursionhrc)) + ((mdr_b_recursionhrc) + (mdr_b_recursionhrc))) /\ ((mdr_e_recursionhrc = ((mdr_p_recursionh) + (mdr_n_recursionh)) * S ((mdr_p_recursionh) + (mdr_n_recursionh)) + ((mdr_n_recursionh) + (mdr_n_recursionh))) /\ ((mdr_f_recursionhrc = ((mdr_nc_recursionh) + (mdr_e_recursionhrc)) * S ((mdr_nc_recursionh) + (mdr_e_recursionhrc)) + ((mdr_e_recursionhrc) + (mdr_e_recursionhrc))) /\ ((mdr_z_recursionhr) = ((mdr_c_recursionhrc) + (mdr_f_recursionhrc)) * S ((mdr_c_recursionhrc) + (mdr_f_recursionhrc)) + ((mdr_f_recursionhrc) + (mdr_f_recursionhrc))))))))) /\ (((exists ff_h_mdr_recursionhrb. ff_h_mdr_recursionhrb + S (mdr_z_recursionhr) = S ((S (mdr_i_recursionh)) * mdr_c_recursion)) /\ exists ff_q_mdr_recursionhrb. mdr_b_recursion = ff_q_mdr_recursionhrb * S ((S (mdr_i_recursionh)) * mdr_c_recursion) + (mdr_z_recursionhr))))) /\ (((((mdr_d_recursionh) = 0) /\ (((mdr_p_recursionh) = 1) /\ ((mdr_n_recursionh) = 0))) \/ exists mdr_q_recursionhs mdr_eb_recursionhs mdr_ec_recursionhs mdr_fb_recursionhs mdr_fc_recursionhs. (((mdr_d_recursionh) = S (mdr_q_recursionhs)) /\ ((forall mdr_j_recursionhsc. (exists mdr_gap_recursionhscj. mdr_gap_recursionhscj + S (mdr_j_recursionhsc) = (S (mdr_q_recursionhs))) -> exists mdr_i_recursionhsc mdr_up_recursionhsc mdr_us_recursionhsc mdr_un_recursionhsc mdr_ut_recursionhsc mdr_p_recursionhsc mdr_n_recursionhsc. ((exists mdr_gap_recursionhsci. mdr_gap_recursionhsci + S (mdr_i_recursionhsc) = (mdr_i_recursionh)) /\ ((exists mdr_z_recursionhscr. ((exists mdr_a_recursionhscrc mdr_b_recursionhscrc mdr_c_recursionhscrc mdr_e_recursionhscrc mdr_f_recursionhscrc. ((mdr_a_recursionhscrc = ((mdr_q_recursionhs) + (mdr_up_recursionhsc)) * S ((mdr_q_recursionhs) + (mdr_up_recursionhsc)) + ((mdr_up_recursionhsc) + (mdr_up_recursionhsc))) /\ ((mdr_b_recursionhscrc = ((mdr_us_recursionhsc) + (mdr_un_recursionhsc)) * S ((mdr_us_recursionhsc) + (mdr_un_recursionhsc)) + ((mdr_un_recursionhsc) + (mdr_un_recursionhsc))) /\ ((mdr_c_recursionhscrc = ((mdr_a_recursionhscrc) + (mdr_b_recursionhscrc)) * S ((mdr_a_recursionhscrc) + (mdr_b_recursionhscrc)) + ((mdr_b_recursionhscrc) + (mdr_b_recursionhscrc))) /\ ((mdr_e_recursionhscrc = ((mdr_p_recursionhsc) + (mdr_n_recursionhsc)) * S ((mdr_p_recursionhsc) + (mdr_n_recursionhsc)) + ((mdr_n_recursionhsc) + (mdr_n_recursionhsc))) /\ ((mdr_f_recursionhscrc = ((mdr_ut_recursionhsc) + (mdr_e_recursionhscrc)) * S ((mdr_ut_recursionhsc) + (mdr_e_recursionhscrc)) + ((mdr_e_recursionhscrc) + (mdr_e_recursionhscrc))) /\ ((mdr_z_recursionhscr) = ((mdr_c_recursionhscrc) + (mdr_f_recursionhscrc)) * S ((mdr_c_recursionhscrc) + (mdr_f_recursionhscrc)) + ((mdr_f_recursionhscrc) + (mdr_f_recursionhscrc))))))))) /\ (((exists ff_h_mdr_recursionhscrb. ff_h_mdr_recursionhscrb + S (mdr_z_recursionhscr) = S ((S (mdr_i_recursionhsc)) * mdr_c_recursion)) /\ exists ff_q_mdr_recursionhscrb. mdr_b_recursion = ff_q_mdr_recursionhscrb * S ((S (mdr_i_recursionhsc)) * mdr_c_recursion) + (mdr_z_recursionhscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_recursionhscm_positive. (exists ff_gap_mdm_lt_mdr_recursionhscm_positive_index_bound. ff_gap_mdm_lt_mdr_recursionhscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_recursionhscm_positive) = ((mdr_q_recursionhs) * (mdr_q_recursionhs))) -> exists ff_row_mdm_prefix_mdr_recursionhscm_positive ff_column_mdm_prefix_mdr_recursionhscm_positive ff_value_mdm_prefix_mdr_recursionhscm_positive. (ff_index_mdm_prefix_mdr_recursionhscm_positive = (mdr_q_recursionhs) * ff_row_mdm_prefix_mdr_recursionhscm_positive + ff_column_mdm_prefix_mdr_recursionhscm_positive /\ ((exists ff_gap_mdm_lt_mdr_recursionhscm_positive_column_bound. ff_gap_mdm_lt_mdr_recursionhscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_recursionhscm_positive) = (mdr_q_recursionhs)) /\ ((exists ff_row_mdm_cell_mdr_recursionhscm_positive_cell ff_column_mdm_cell_mdr_recursionhscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_recursionhscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_recursionhscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_recursionhscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_recursionhscm_positive_cell = ff_row_mdm_prefix_mdr_recursionhscm_positive) \/ ((exists ff_gap_mdm_le_mdr_recursionhscm_positive_cell_row_after. ff_gap_mdm_le_mdr_recursionhscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_recursionhscm_positive)) /\ ff_row_mdm_cell_mdr_recursionhscm_positive_cell = S ff_row_mdm_prefix_mdr_recursionhscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_recursionhscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_recursionhscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_recursionhscm_positive) = (mdr_j_recursionhsc)) /\ ff_column_mdm_cell_mdr_recursionhscm_positive_cell = ff_column_mdm_prefix_mdr_recursionhscm_positive) \/ ((exists ff_gap_mdm_le_mdr_recursionhscm_positive_cell_column_after. ff_gap_mdm_le_mdr_recursionhscm_positive_cell_column_after + (mdr_j_recursionhsc) = (ff_column_mdm_prefix_mdr_recursionhscm_positive)) /\ ff_column_mdm_cell_mdr_recursionhscm_positive_cell = S ff_column_mdm_prefix_mdr_recursionhscm_positive))) /\ (((exists ff_h_mdm_mdr_recursionhscm_positive_cell_source. ff_h_mdm_mdr_recursionhscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_recursionhscm_positive) = S ((S ((ff_row_mdm_cell_mdr_recursionhscm_positive_cell) * (S (mdr_q_recursionhs)) + (ff_column_mdm_cell_mdr_recursionhscm_positive_cell))) * mdr_pc_recursionh)) /\ exists ff_q_mdm_mdr_recursionhscm_positive_cell_source. mdr_pb_recursionh = ff_q_mdm_mdr_recursionhscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_recursionhscm_positive_cell) * (S (mdr_q_recursionhs)) + (ff_column_mdm_cell_mdr_recursionhscm_positive_cell))) * mdr_pc_recursionh) + (ff_value_mdm_prefix_mdr_recursionhscm_positive)))))) /\ (((exists ff_h_mdm_mdr_recursionhscm_positive_target. ff_h_mdm_mdr_recursionhscm_positive_target + S (ff_value_mdm_prefix_mdr_recursionhscm_positive) = S ((S (ff_index_mdm_prefix_mdr_recursionhscm_positive)) * mdr_us_recursionhsc)) /\ exists ff_q_mdm_mdr_recursionhscm_positive_target. mdr_up_recursionhsc = ff_q_mdm_mdr_recursionhscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_recursionhscm_positive)) * mdr_us_recursionhsc) + (ff_value_mdm_prefix_mdr_recursionhscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_recursionhscm_negative. (exists ff_gap_mdm_lt_mdr_recursionhscm_negative_index_bound. ff_gap_mdm_lt_mdr_recursionhscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_recursionhscm_negative) = ((mdr_q_recursionhs) * (mdr_q_recursionhs))) -> exists ff_row_mdm_prefix_mdr_recursionhscm_negative ff_column_mdm_prefix_mdr_recursionhscm_negative ff_value_mdm_prefix_mdr_recursionhscm_negative. (ff_index_mdm_prefix_mdr_recursionhscm_negative = (mdr_q_recursionhs) * ff_row_mdm_prefix_mdr_recursionhscm_negative + ff_column_mdm_prefix_mdr_recursionhscm_negative /\ ((exists ff_gap_mdm_lt_mdr_recursionhscm_negative_column_bound. ff_gap_mdm_lt_mdr_recursionhscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_recursionhscm_negative) = (mdr_q_recursionhs)) /\ ((exists ff_row_mdm_cell_mdr_recursionhscm_negative_cell ff_column_mdm_cell_mdr_recursionhscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_recursionhscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_recursionhscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_recursionhscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_recursionhscm_negative_cell = ff_row_mdm_prefix_mdr_recursionhscm_negative) \/ ((exists ff_gap_mdm_le_mdr_recursionhscm_negative_cell_row_after. ff_gap_mdm_le_mdr_recursionhscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_recursionhscm_negative)) /\ ff_row_mdm_cell_mdr_recursionhscm_negative_cell = S ff_row_mdm_prefix_mdr_recursionhscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_recursionhscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_recursionhscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_recursionhscm_negative) = (mdr_j_recursionhsc)) /\ ff_column_mdm_cell_mdr_recursionhscm_negative_cell = ff_column_mdm_prefix_mdr_recursionhscm_negative) \/ ((exists ff_gap_mdm_le_mdr_recursionhscm_negative_cell_column_after. ff_gap_mdm_le_mdr_recursionhscm_negative_cell_column_after + (mdr_j_recursionhsc) = (ff_column_mdm_prefix_mdr_recursionhscm_negative)) /\ ff_column_mdm_cell_mdr_recursionhscm_negative_cell = S ff_column_mdm_prefix_mdr_recursionhscm_negative))) /\ (((exists ff_h_mdm_mdr_recursionhscm_negative_cell_source. ff_h_mdm_mdr_recursionhscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_recursionhscm_negative) = S ((S ((ff_row_mdm_cell_mdr_recursionhscm_negative_cell) * (S (mdr_q_recursionhs)) + (ff_column_mdm_cell_mdr_recursionhscm_negative_cell))) * mdr_nc_recursionh)) /\ exists ff_q_mdm_mdr_recursionhscm_negative_cell_source. mdr_nb_recursionh = ff_q_mdm_mdr_recursionhscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_recursionhscm_negative_cell) * (S (mdr_q_recursionhs)) + (ff_column_mdm_cell_mdr_recursionhscm_negative_cell))) * mdr_nc_recursionh) + (ff_value_mdm_prefix_mdr_recursionhscm_negative)))))) /\ (((exists ff_h_mdm_mdr_recursionhscm_negative_target. ff_h_mdm_mdr_recursionhscm_negative_target + S (ff_value_mdm_prefix_mdr_recursionhscm_negative) = S ((S (ff_index_mdm_prefix_mdr_recursionhscm_negative)) * mdr_ut_recursionhsc)) /\ exists ff_q_mdm_mdr_recursionhscm_negative_target. mdr_un_recursionhsc = ff_q_mdm_mdr_recursionhscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_recursionhscm_negative)) * mdr_ut_recursionhsc) + (ff_value_mdm_prefix_mdr_recursionhscm_negative))))))))) /\ ((((exists ff_h_mdr_recursionhscp. ff_h_mdr_recursionhscp + S (mdr_p_recursionhsc) = S ((S (mdr_j_recursionhsc)) * mdr_ec_recursionhs)) /\ exists ff_q_mdr_recursionhscp. mdr_eb_recursionhs = ff_q_mdr_recursionhscp * S ((S (mdr_j_recursionhsc)) * mdr_ec_recursionhs) + (mdr_p_recursionhsc))) /\ (((exists ff_h_mdr_recursionhscn. ff_h_mdr_recursionhscn + S (mdr_n_recursionhsc) = S ((S (mdr_j_recursionhsc)) * mdr_fc_recursionhs)) /\ exists ff_q_mdr_recursionhscn. mdr_fb_recursionhs = ff_q_mdr_recursionhscn * S ((S (mdr_j_recursionhsc)) * mdr_fc_recursionhs) + (mdr_n_recursionhsc)))))))) /\ (exists ff_ub_mce_fold_mdr_recursionhsf ff_uc_mce_fold_mdr_recursionhsf ff_vb_mce_fold_mdr_recursionhsf ff_vc_mce_fold_mdr_recursionhsf. ((forall ff_index_mce_alternating_mdr_recursionhsf_prefix. (exists ff_gap_mce_mdr_recursionhsf_prefix_index. ff_gap_mce_mdr_recursionhsf_prefix_index + S (ff_index_mce_alternating_mdr_recursionhsf_prefix) = (S (mdr_q_recursionhs))) -> exists ff_ap_mce_alternating_mdr_recursionhsf_prefix ff_an_mce_alternating_mdr_recursionhsf_prefix ff_bp_mce_alternating_mdr_recursionhsf_prefix ff_bn_mce_alternating_mdr_recursionhsf_prefix ff_p_mce_alternating_mdr_recursionhsf_prefix ff_n_mce_alternating_mdr_recursionhsf_prefix. ((((exists ff_h_mce_mdr_recursionhsf_prefix_ap. ff_h_mce_mdr_recursionhsf_prefix_ap + S (ff_ap_mce_alternating_mdr_recursionhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_recursionhsf_prefix)) * mdr_pc_recursionh)) /\ exists ff_q_mce_mdr_recursionhsf_prefix_ap. mdr_pb_recursionh = ff_q_mce_mdr_recursionhsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_recursionhsf_prefix)) * mdr_pc_recursionh) + (ff_ap_mce_alternating_mdr_recursionhsf_prefix))) /\ ((((exists ff_h_mce_mdr_recursionhsf_prefix_an. ff_h_mce_mdr_recursionhsf_prefix_an + S (ff_an_mce_alternating_mdr_recursionhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_recursionhsf_prefix)) * mdr_nc_recursionh)) /\ exists ff_q_mce_mdr_recursionhsf_prefix_an. mdr_nb_recursionh = ff_q_mce_mdr_recursionhsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_recursionhsf_prefix)) * mdr_nc_recursionh) + (ff_an_mce_alternating_mdr_recursionhsf_prefix))) /\ ((((exists ff_h_mce_mdr_recursionhsf_prefix_bp. ff_h_mce_mdr_recursionhsf_prefix_bp + S (ff_bp_mce_alternating_mdr_recursionhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_recursionhsf_prefix)) * mdr_ec_recursionhs)) /\ exists ff_q_mce_mdr_recursionhsf_prefix_bp. mdr_eb_recursionhs = ff_q_mce_mdr_recursionhsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_recursionhsf_prefix)) * mdr_ec_recursionhs) + (ff_bp_mce_alternating_mdr_recursionhsf_prefix))) /\ ((((exists ff_h_mce_mdr_recursionhsf_prefix_bn. ff_h_mce_mdr_recursionhsf_prefix_bn + S (ff_bn_mce_alternating_mdr_recursionhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_recursionhsf_prefix)) * mdr_fc_recursionhs)) /\ exists ff_q_mce_mdr_recursionhsf_prefix_bn. mdr_fb_recursionhs = ff_q_mce_mdr_recursionhsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_recursionhsf_prefix)) * mdr_fc_recursionhs) + (ff_bn_mce_alternating_mdr_recursionhsf_prefix))) /\ ((((exists ff_h_mce_mdr_recursionhsf_prefix_positive. ff_h_mce_mdr_recursionhsf_prefix_positive + S (ff_p_mce_alternating_mdr_recursionhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_recursionhsf_prefix)) * ff_uc_mce_fold_mdr_recursionhsf)) /\ exists ff_q_mce_mdr_recursionhsf_prefix_positive. ff_ub_mce_fold_mdr_recursionhsf = ff_q_mce_mdr_recursionhsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_recursionhsf_prefix)) * ff_uc_mce_fold_mdr_recursionhsf) + (ff_p_mce_alternating_mdr_recursionhsf_prefix))) /\ ((((exists ff_h_mce_mdr_recursionhsf_prefix_negative. ff_h_mce_mdr_recursionhsf_prefix_negative + S (ff_n_mce_alternating_mdr_recursionhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_recursionhsf_prefix)) * ff_vc_mce_fold_mdr_recursionhsf)) /\ exists ff_q_mce_mdr_recursionhsf_prefix_negative. ff_vb_mce_fold_mdr_recursionhsf = ff_q_mce_mdr_recursionhsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_recursionhsf_prefix)) * ff_vc_mce_fold_mdr_recursionhsf) + (ff_n_mce_alternating_mdr_recursionhsf_prefix))) /\ (((exists ff_even_mce_term_mdr_recursionhsf_prefix_term. ff_index_mce_alternating_mdr_recursionhsf_prefix = 2 * ff_even_mce_term_mdr_recursionhsf_prefix_term) /\ (ff_p_mce_alternating_mdr_recursionhsf_prefix = (ff_ap_mce_alternating_mdr_recursionhsf_prefix) * (ff_bp_mce_alternating_mdr_recursionhsf_prefix) + (ff_an_mce_alternating_mdr_recursionhsf_prefix) * (ff_bn_mce_alternating_mdr_recursionhsf_prefix) /\ ff_n_mce_alternating_mdr_recursionhsf_prefix = (ff_ap_mce_alternating_mdr_recursionhsf_prefix) * (ff_bn_mce_alternating_mdr_recursionhsf_prefix) + (ff_an_mce_alternating_mdr_recursionhsf_prefix) * (ff_bp_mce_alternating_mdr_recursionhsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_recursionhsf_prefix_term. ff_index_mce_alternating_mdr_recursionhsf_prefix = 2 * ff_odd_mce_term_mdr_recursionhsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_recursionhsf_prefix = (ff_ap_mce_alternating_mdr_recursionhsf_prefix) * (ff_bn_mce_alternating_mdr_recursionhsf_prefix) + (ff_an_mce_alternating_mdr_recursionhsf_prefix) * (ff_bp_mce_alternating_mdr_recursionhsf_prefix) /\ ff_n_mce_alternating_mdr_recursionhsf_prefix = (ff_ap_mce_alternating_mdr_recursionhsf_prefix) * (ff_bp_mce_alternating_mdr_recursionhsf_prefix) + (ff_an_mce_alternating_mdr_recursionhsf_prefix) * (ff_bn_mce_alternating_mdr_recursionhsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_recursionhsf_positive ff_v_mce_mdr_recursionhsf_positive. ((((exists ff_h_mce_mdr_recursionhsf_positive_start. ff_h_mce_mdr_recursionhsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_recursionhsf_positive)) /\ exists ff_q_mce_mdr_recursionhsf_positive_start. ff_u_mce_mdr_recursionhsf_positive = ff_q_mce_mdr_recursionhsf_positive_start * S ((S (0)) * ff_v_mce_mdr_recursionhsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_recursionhsf_positive_terminal. ff_h_mce_mdr_recursionhsf_positive_terminal + S (mdr_p_recursionh) = S ((S ((S (mdr_q_recursionhs)))) * ff_v_mce_mdr_recursionhsf_positive)) /\ exists ff_q_mce_mdr_recursionhsf_positive_terminal. ff_u_mce_mdr_recursionhsf_positive = ff_q_mce_mdr_recursionhsf_positive_terminal * S ((S ((S (mdr_q_recursionhs)))) * ff_v_mce_mdr_recursionhsf_positive) + (mdr_p_recursionh))) /\ forall ff_i_mce_mdr_recursionhsf_positive. (exists ff_lt_mce_mdr_recursionhsf_positive_bound. ff_lt_mce_mdr_recursionhsf_positive_bound + S ff_i_mce_mdr_recursionhsf_positive = (S (mdr_q_recursionhs))) -> exists ff_a_mce_mdr_recursionhsf_positive ff_r_mce_mdr_recursionhsf_positive ff_s_mce_mdr_recursionhsf_positive. ((((exists ff_h_mce_mdr_recursionhsf_positive_summand. ff_h_mce_mdr_recursionhsf_positive_summand + S (ff_a_mce_mdr_recursionhsf_positive) = S ((S (ff_i_mce_mdr_recursionhsf_positive)) * ff_uc_mce_fold_mdr_recursionhsf)) /\ exists ff_q_mce_mdr_recursionhsf_positive_summand. ff_ub_mce_fold_mdr_recursionhsf = ff_q_mce_mdr_recursionhsf_positive_summand * S ((S (ff_i_mce_mdr_recursionhsf_positive)) * ff_uc_mce_fold_mdr_recursionhsf) + (ff_a_mce_mdr_recursionhsf_positive))) /\ ((((exists ff_h_mce_mdr_recursionhsf_positive_partial. ff_h_mce_mdr_recursionhsf_positive_partial + S (ff_r_mce_mdr_recursionhsf_positive) = S ((S (ff_i_mce_mdr_recursionhsf_positive)) * ff_v_mce_mdr_recursionhsf_positive)) /\ exists ff_q_mce_mdr_recursionhsf_positive_partial. ff_u_mce_mdr_recursionhsf_positive = ff_q_mce_mdr_recursionhsf_positive_partial * S ((S (ff_i_mce_mdr_recursionhsf_positive)) * ff_v_mce_mdr_recursionhsf_positive) + (ff_r_mce_mdr_recursionhsf_positive))) /\ ((((exists ff_h_mce_mdr_recursionhsf_positive_successor. ff_h_mce_mdr_recursionhsf_positive_successor + S (ff_s_mce_mdr_recursionhsf_positive) = S ((S (S ff_i_mce_mdr_recursionhsf_positive)) * ff_v_mce_mdr_recursionhsf_positive)) /\ exists ff_q_mce_mdr_recursionhsf_positive_successor. ff_u_mce_mdr_recursionhsf_positive = ff_q_mce_mdr_recursionhsf_positive_successor * S ((S (S ff_i_mce_mdr_recursionhsf_positive)) * ff_v_mce_mdr_recursionhsf_positive) + (ff_s_mce_mdr_recursionhsf_positive))) /\ ff_s_mce_mdr_recursionhsf_positive = ff_r_mce_mdr_recursionhsf_positive + ff_a_mce_mdr_recursionhsf_positive)))))) /\ (exists ff_u_mce_mdr_recursionhsf_negative ff_v_mce_mdr_recursionhsf_negative. ((((exists ff_h_mce_mdr_recursionhsf_negative_start. ff_h_mce_mdr_recursionhsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_recursionhsf_negative)) /\ exists ff_q_mce_mdr_recursionhsf_negative_start. ff_u_mce_mdr_recursionhsf_negative = ff_q_mce_mdr_recursionhsf_negative_start * S ((S (0)) * ff_v_mce_mdr_recursionhsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_recursionhsf_negative_terminal. ff_h_mce_mdr_recursionhsf_negative_terminal + S (mdr_n_recursionh) = S ((S ((S (mdr_q_recursionhs)))) * ff_v_mce_mdr_recursionhsf_negative)) /\ exists ff_q_mce_mdr_recursionhsf_negative_terminal. ff_u_mce_mdr_recursionhsf_negative = ff_q_mce_mdr_recursionhsf_negative_terminal * S ((S ((S (mdr_q_recursionhs)))) * ff_v_mce_mdr_recursionhsf_negative) + (mdr_n_recursionh))) /\ forall ff_i_mce_mdr_recursionhsf_negative. (exists ff_lt_mce_mdr_recursionhsf_negative_bound. ff_lt_mce_mdr_recursionhsf_negative_bound + S ff_i_mce_mdr_recursionhsf_negative = (S (mdr_q_recursionhs))) -> exists ff_a_mce_mdr_recursionhsf_negative ff_r_mce_mdr_recursionhsf_negative ff_s_mce_mdr_recursionhsf_negative. ((((exists ff_h_mce_mdr_recursionhsf_negative_summand. ff_h_mce_mdr_recursionhsf_negative_summand + S (ff_a_mce_mdr_recursionhsf_negative) = S ((S (ff_i_mce_mdr_recursionhsf_negative)) * ff_vc_mce_fold_mdr_recursionhsf)) /\ exists ff_q_mce_mdr_recursionhsf_negative_summand. ff_vb_mce_fold_mdr_recursionhsf = ff_q_mce_mdr_recursionhsf_negative_summand * S ((S (ff_i_mce_mdr_recursionhsf_negative)) * ff_vc_mce_fold_mdr_recursionhsf) + (ff_a_mce_mdr_recursionhsf_negative))) /\ ((((exists ff_h_mce_mdr_recursionhsf_negative_partial. ff_h_mce_mdr_recursionhsf_negative_partial + S (ff_r_mce_mdr_recursionhsf_negative) = S ((S (ff_i_mce_mdr_recursionhsf_negative)) * ff_v_mce_mdr_recursionhsf_negative)) /\ exists ff_q_mce_mdr_recursionhsf_negative_partial. ff_u_mce_mdr_recursionhsf_negative = ff_q_mce_mdr_recursionhsf_negative_partial * S ((S (ff_i_mce_mdr_recursionhsf_negative)) * ff_v_mce_mdr_recursionhsf_negative) + (ff_r_mce_mdr_recursionhsf_negative))) /\ ((((exists ff_h_mce_mdr_recursionhsf_negative_successor. ff_h_mce_mdr_recursionhsf_negative_successor + S (ff_s_mce_mdr_recursionhsf_negative) = S ((S (S ff_i_mce_mdr_recursionhsf_negative)) * ff_v_mce_mdr_recursionhsf_negative)) /\ exists ff_q_mce_mdr_recursionhsf_negative_successor. ff_u_mce_mdr_recursionhsf_negative = ff_q_mce_mdr_recursionhsf_negative_successor * S ((S (S ff_i_mce_mdr_recursionhsf_negative)) * ff_v_mce_mdr_recursionhsf_negative) + (ff_s_mce_mdr_recursionhsf_negative))) /\ ff_s_mce_mdr_recursionhsf_negative = ff_r_mce_mdr_recursionhsf_negative + ff_a_mce_mdr_recursionhsf_negative))))))))))))))) -> exists mdr_u_recursion mdr_v_recursion mdr_t_recursion mdr_p_recursion mdr_n_recursion. ((forall mdr_i_recursionrp mdr_a_recursionrp. (exists mdr_gap_recursionrpb. mdr_gap_recursionrpb + S (mdr_i_recursionrp) = (mdr_l_recursion)) -> (((exists ff_h_mdr_recursionrpo. ff_h_mdr_recursionrpo + S (mdr_a_recursionrp) = S ((S (mdr_i_recursionrp)) * mdr_c_recursion)) /\ exists ff_q_mdr_recursionrpo. mdr_b_recursion = ff_q_mdr_recursionrpo * S ((S (mdr_i_recursionrp)) * mdr_c_recursion) + (mdr_a_recursionrp))) -> (((exists ff_h_mdr_recursionrpn. ff_h_mdr_recursionrpn + S (mdr_a_recursionrp) = S ((S (mdr_i_recursionrp)) * mdr_v_recursion)) /\ exists ff_q_mdr_recursionrpn. mdr_u_recursion = ff_q_mdr_recursionrpn * S ((S (mdr_i_recursionrp)) * mdr_v_recursion) + (mdr_a_recursionrp)))) /\ ((exists mdr_gap_recursionrl. mdr_gap_recursionrl + (mdr_l_recursion) = (mdr_t_recursion)) /\ ((forall mdr_i_recursionrh. (exists mdr_gap_recursionrhi. mdr_gap_recursionrhi + S (mdr_i_recursionrh) = (S (mdr_t_recursion))) -> exists mdr_d_recursionrh mdr_pb_recursionrh mdr_pc_recursionrh mdr_nb_recursionrh mdr_nc_recursionrh mdr_p_recursionrh mdr_n_recursionrh. ((exists mdr_z_recursionrhr. ((exists mdr_a_recursionrhrc mdr_b_recursionrhrc mdr_c_recursionrhrc mdr_e_recursionrhrc mdr_f_recursionrhrc. ((mdr_a_recursionrhrc = ((mdr_d_recursionrh) + (mdr_pb_recursionrh)) * S ((mdr_d_recursionrh) + (mdr_pb_recursionrh)) + ((mdr_pb_recursionrh) + (mdr_pb_recursionrh))) /\ ((mdr_b_recursionrhrc = ((mdr_pc_recursionrh) + (mdr_nb_recursionrh)) * S ((mdr_pc_recursionrh) + (mdr_nb_recursionrh)) + ((mdr_nb_recursionrh) + (mdr_nb_recursionrh))) /\ ((mdr_c_recursionrhrc = ((mdr_a_recursionrhrc) + (mdr_b_recursionrhrc)) * S ((mdr_a_recursionrhrc) + (mdr_b_recursionrhrc)) + ((mdr_b_recursionrhrc) + (mdr_b_recursionrhrc))) /\ ((mdr_e_recursionrhrc = ((mdr_p_recursionrh) + (mdr_n_recursionrh)) * S ((mdr_p_recursionrh) + (mdr_n_recursionrh)) + ((mdr_n_recursionrh) + (mdr_n_recursionrh))) /\ ((mdr_f_recursionrhrc = ((mdr_nc_recursionrh) + (mdr_e_recursionrhrc)) * S ((mdr_nc_recursionrh) + (mdr_e_recursionrhrc)) + ((mdr_e_recursionrhrc) + (mdr_e_recursionrhrc))) /\ ((mdr_z_recursionrhr) = ((mdr_c_recursionrhrc) + (mdr_f_recursionrhrc)) * S ((mdr_c_recursionrhrc) + (mdr_f_recursionrhrc)) + ((mdr_f_recursionrhrc) + (mdr_f_recursionrhrc))))))))) /\ (((exists ff_h_mdr_recursionrhrb. ff_h_mdr_recursionrhrb + S (mdr_z_recursionrhr) = S ((S (mdr_i_recursionrh)) * mdr_v_recursion)) /\ exists ff_q_mdr_recursionrhrb. mdr_u_recursion = ff_q_mdr_recursionrhrb * S ((S (mdr_i_recursionrh)) * mdr_v_recursion) + (mdr_z_recursionrhr))))) /\ (((((mdr_d_recursionrh) = 0) /\ (((mdr_p_recursionrh) = 1) /\ ((mdr_n_recursionrh) = 0))) \/ exists mdr_q_recursionrhs mdr_eb_recursionrhs mdr_ec_recursionrhs mdr_fb_recursionrhs mdr_fc_recursionrhs. (((mdr_d_recursionrh) = S (mdr_q_recursionrhs)) /\ ((forall mdr_j_recursionrhsc. (exists mdr_gap_recursionrhscj. mdr_gap_recursionrhscj + S (mdr_j_recursionrhsc) = (S (mdr_q_recursionrhs))) -> exists mdr_i_recursionrhsc mdr_up_recursionrhsc mdr_us_recursionrhsc mdr_un_recursionrhsc mdr_ut_recursionrhsc mdr_p_recursionrhsc mdr_n_recursionrhsc. ((exists mdr_gap_recursionrhsci. mdr_gap_recursionrhsci + S (mdr_i_recursionrhsc) = (mdr_i_recursionrh)) /\ ((exists mdr_z_recursionrhscr. ((exists mdr_a_recursionrhscrc mdr_b_recursionrhscrc mdr_c_recursionrhscrc mdr_e_recursionrhscrc mdr_f_recursionrhscrc. ((mdr_a_recursionrhscrc = ((mdr_q_recursionrhs) + (mdr_up_recursionrhsc)) * S ((mdr_q_recursionrhs) + (mdr_up_recursionrhsc)) + ((mdr_up_recursionrhsc) + (mdr_up_recursionrhsc))) /\ ((mdr_b_recursionrhscrc = ((mdr_us_recursionrhsc) + (mdr_un_recursionrhsc)) * S ((mdr_us_recursionrhsc) + (mdr_un_recursionrhsc)) + ((mdr_un_recursionrhsc) + (mdr_un_recursionrhsc))) /\ ((mdr_c_recursionrhscrc = ((mdr_a_recursionrhscrc) + (mdr_b_recursionrhscrc)) * S ((mdr_a_recursionrhscrc) + (mdr_b_recursionrhscrc)) + ((mdr_b_recursionrhscrc) + (mdr_b_recursionrhscrc))) /\ ((mdr_e_recursionrhscrc = ((mdr_p_recursionrhsc) + (mdr_n_recursionrhsc)) * S ((mdr_p_recursionrhsc) + (mdr_n_recursionrhsc)) + ((mdr_n_recursionrhsc) + (mdr_n_recursionrhsc))) /\ ((mdr_f_recursionrhscrc = ((mdr_ut_recursionrhsc) + (mdr_e_recursionrhscrc)) * S ((mdr_ut_recursionrhsc) + (mdr_e_recursionrhscrc)) + ((mdr_e_recursionrhscrc) + (mdr_e_recursionrhscrc))) /\ ((mdr_z_recursionrhscr) = ((mdr_c_recursionrhscrc) + (mdr_f_recursionrhscrc)) * S ((mdr_c_recursionrhscrc) + (mdr_f_recursionrhscrc)) + ((mdr_f_recursionrhscrc) + (mdr_f_recursionrhscrc))))))))) /\ (((exists ff_h_mdr_recursionrhscrb. ff_h_mdr_recursionrhscrb + S (mdr_z_recursionrhscr) = S ((S (mdr_i_recursionrhsc)) * mdr_v_recursion)) /\ exists ff_q_mdr_recursionrhscrb. mdr_u_recursion = ff_q_mdr_recursionrhscrb * S ((S (mdr_i_recursionrhsc)) * mdr_v_recursion) + (mdr_z_recursionrhscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_recursionrhscm_positive. (exists ff_gap_mdm_lt_mdr_recursionrhscm_positive_index_bound. ff_gap_mdm_lt_mdr_recursionrhscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_recursionrhscm_positive) = ((mdr_q_recursionrhs) * (mdr_q_recursionrhs))) -> exists ff_row_mdm_prefix_mdr_recursionrhscm_positive ff_column_mdm_prefix_mdr_recursionrhscm_positive ff_value_mdm_prefix_mdr_recursionrhscm_positive. (ff_index_mdm_prefix_mdr_recursionrhscm_positive = (mdr_q_recursionrhs) * ff_row_mdm_prefix_mdr_recursionrhscm_positive + ff_column_mdm_prefix_mdr_recursionrhscm_positive /\ ((exists ff_gap_mdm_lt_mdr_recursionrhscm_positive_column_bound. ff_gap_mdm_lt_mdr_recursionrhscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_recursionrhscm_positive) = (mdr_q_recursionrhs)) /\ ((exists ff_row_mdm_cell_mdr_recursionrhscm_positive_cell ff_column_mdm_cell_mdr_recursionrhscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_recursionrhscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_recursionrhscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_recursionrhscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_recursionrhscm_positive_cell = ff_row_mdm_prefix_mdr_recursionrhscm_positive) \/ ((exists ff_gap_mdm_le_mdr_recursionrhscm_positive_cell_row_after. ff_gap_mdm_le_mdr_recursionrhscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_recursionrhscm_positive)) /\ ff_row_mdm_cell_mdr_recursionrhscm_positive_cell = S ff_row_mdm_prefix_mdr_recursionrhscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_recursionrhscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_recursionrhscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_recursionrhscm_positive) = (mdr_j_recursionrhsc)) /\ ff_column_mdm_cell_mdr_recursionrhscm_positive_cell = ff_column_mdm_prefix_mdr_recursionrhscm_positive) \/ ((exists ff_gap_mdm_le_mdr_recursionrhscm_positive_cell_column_after. ff_gap_mdm_le_mdr_recursionrhscm_positive_cell_column_after + (mdr_j_recursionrhsc) = (ff_column_mdm_prefix_mdr_recursionrhscm_positive)) /\ ff_column_mdm_cell_mdr_recursionrhscm_positive_cell = S ff_column_mdm_prefix_mdr_recursionrhscm_positive))) /\ (((exists ff_h_mdm_mdr_recursionrhscm_positive_cell_source. ff_h_mdm_mdr_recursionrhscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_recursionrhscm_positive) = S ((S ((ff_row_mdm_cell_mdr_recursionrhscm_positive_cell) * (S (mdr_q_recursionrhs)) + (ff_column_mdm_cell_mdr_recursionrhscm_positive_cell))) * mdr_pc_recursionrh)) /\ exists ff_q_mdm_mdr_recursionrhscm_positive_cell_source. mdr_pb_recursionrh = ff_q_mdm_mdr_recursionrhscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_recursionrhscm_positive_cell) * (S (mdr_q_recursionrhs)) + (ff_column_mdm_cell_mdr_recursionrhscm_positive_cell))) * mdr_pc_recursionrh) + (ff_value_mdm_prefix_mdr_recursionrhscm_positive)))))) /\ (((exists ff_h_mdm_mdr_recursionrhscm_positive_target. ff_h_mdm_mdr_recursionrhscm_positive_target + S (ff_value_mdm_prefix_mdr_recursionrhscm_positive) = S ((S (ff_index_mdm_prefix_mdr_recursionrhscm_positive)) * mdr_us_recursionrhsc)) /\ exists ff_q_mdm_mdr_recursionrhscm_positive_target. mdr_up_recursionrhsc = ff_q_mdm_mdr_recursionrhscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_recursionrhscm_positive)) * mdr_us_recursionrhsc) + (ff_value_mdm_prefix_mdr_recursionrhscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_recursionrhscm_negative. (exists ff_gap_mdm_lt_mdr_recursionrhscm_negative_index_bound. ff_gap_mdm_lt_mdr_recursionrhscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_recursionrhscm_negative) = ((mdr_q_recursionrhs) * (mdr_q_recursionrhs))) -> exists ff_row_mdm_prefix_mdr_recursionrhscm_negative ff_column_mdm_prefix_mdr_recursionrhscm_negative ff_value_mdm_prefix_mdr_recursionrhscm_negative. (ff_index_mdm_prefix_mdr_recursionrhscm_negative = (mdr_q_recursionrhs) * ff_row_mdm_prefix_mdr_recursionrhscm_negative + ff_column_mdm_prefix_mdr_recursionrhscm_negative /\ ((exists ff_gap_mdm_lt_mdr_recursionrhscm_negative_column_bound. ff_gap_mdm_lt_mdr_recursionrhscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_recursionrhscm_negative) = (mdr_q_recursionrhs)) /\ ((exists ff_row_mdm_cell_mdr_recursionrhscm_negative_cell ff_column_mdm_cell_mdr_recursionrhscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_recursionrhscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_recursionrhscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_recursionrhscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_recursionrhscm_negative_cell = ff_row_mdm_prefix_mdr_recursionrhscm_negative) \/ ((exists ff_gap_mdm_le_mdr_recursionrhscm_negative_cell_row_after. ff_gap_mdm_le_mdr_recursionrhscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_recursionrhscm_negative)) /\ ff_row_mdm_cell_mdr_recursionrhscm_negative_cell = S ff_row_mdm_prefix_mdr_recursionrhscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_recursionrhscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_recursionrhscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_recursionrhscm_negative) = (mdr_j_recursionrhsc)) /\ ff_column_mdm_cell_mdr_recursionrhscm_negative_cell = ff_column_mdm_prefix_mdr_recursionrhscm_negative) \/ ((exists ff_gap_mdm_le_mdr_recursionrhscm_negative_cell_column_after. ff_gap_mdm_le_mdr_recursionrhscm_negative_cell_column_after + (mdr_j_recursionrhsc) = (ff_column_mdm_prefix_mdr_recursionrhscm_negative)) /\ ff_column_mdm_cell_mdr_recursionrhscm_negative_cell = S ff_column_mdm_prefix_mdr_recursionrhscm_negative))) /\ (((exists ff_h_mdm_mdr_recursionrhscm_negative_cell_source. ff_h_mdm_mdr_recursionrhscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_recursionrhscm_negative) = S ((S ((ff_row_mdm_cell_mdr_recursionrhscm_negative_cell) * (S (mdr_q_recursionrhs)) + (ff_column_mdm_cell_mdr_recursionrhscm_negative_cell))) * mdr_nc_recursionrh)) /\ exists ff_q_mdm_mdr_recursionrhscm_negative_cell_source. mdr_nb_recursionrh = ff_q_mdm_mdr_recursionrhscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_recursionrhscm_negative_cell) * (S (mdr_q_recursionrhs)) + (ff_column_mdm_cell_mdr_recursionrhscm_negative_cell))) * mdr_nc_recursionrh) + (ff_value_mdm_prefix_mdr_recursionrhscm_negative)))))) /\ (((exists ff_h_mdm_mdr_recursionrhscm_negative_target. ff_h_mdm_mdr_recursionrhscm_negative_target + S (ff_value_mdm_prefix_mdr_recursionrhscm_negative) = S ((S (ff_index_mdm_prefix_mdr_recursionrhscm_negative)) * mdr_ut_recursionrhsc)) /\ exists ff_q_mdm_mdr_recursionrhscm_negative_target. mdr_un_recursionrhsc = ff_q_mdm_mdr_recursionrhscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_recursionrhscm_negative)) * mdr_ut_recursionrhsc) + (ff_value_mdm_prefix_mdr_recursionrhscm_negative))))))))) /\ ((((exists ff_h_mdr_recursionrhscp. ff_h_mdr_recursionrhscp + S (mdr_p_recursionrhsc) = S ((S (mdr_j_recursionrhsc)) * mdr_ec_recursionrhs)) /\ exists ff_q_mdr_recursionrhscp. mdr_eb_recursionrhs = ff_q_mdr_recursionrhscp * S ((S (mdr_j_recursionrhsc)) * mdr_ec_recursionrhs) + (mdr_p_recursionrhsc))) /\ (((exists ff_h_mdr_recursionrhscn. ff_h_mdr_recursionrhscn + S (mdr_n_recursionrhsc) = S ((S (mdr_j_recursionrhsc)) * mdr_fc_recursionrhs)) /\ exists ff_q_mdr_recursionrhscn. mdr_fb_recursionrhs = ff_q_mdr_recursionrhscn * S ((S (mdr_j_recursionrhsc)) * mdr_fc_recursionrhs) + (mdr_n_recursionrhsc)))))))) /\ (exists ff_ub_mce_fold_mdr_recursionrhsf ff_uc_mce_fold_mdr_recursionrhsf ff_vb_mce_fold_mdr_recursionrhsf ff_vc_mce_fold_mdr_recursionrhsf. ((forall ff_index_mce_alternating_mdr_recursionrhsf_prefix. (exists ff_gap_mce_mdr_recursionrhsf_prefix_index. ff_gap_mce_mdr_recursionrhsf_prefix_index + S (ff_index_mce_alternating_mdr_recursionrhsf_prefix) = (S (mdr_q_recursionrhs))) -> exists ff_ap_mce_alternating_mdr_recursionrhsf_prefix ff_an_mce_alternating_mdr_recursionrhsf_prefix ff_bp_mce_alternating_mdr_recursionrhsf_prefix ff_bn_mce_alternating_mdr_recursionrhsf_prefix ff_p_mce_alternating_mdr_recursionrhsf_prefix ff_n_mce_alternating_mdr_recursionrhsf_prefix. ((((exists ff_h_mce_mdr_recursionrhsf_prefix_ap. ff_h_mce_mdr_recursionrhsf_prefix_ap + S (ff_ap_mce_alternating_mdr_recursionrhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_recursionrhsf_prefix)) * mdr_pc_recursionrh)) /\ exists ff_q_mce_mdr_recursionrhsf_prefix_ap. mdr_pb_recursionrh = ff_q_mce_mdr_recursionrhsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_recursionrhsf_prefix)) * mdr_pc_recursionrh) + (ff_ap_mce_alternating_mdr_recursionrhsf_prefix))) /\ ((((exists ff_h_mce_mdr_recursionrhsf_prefix_an. ff_h_mce_mdr_recursionrhsf_prefix_an + S (ff_an_mce_alternating_mdr_recursionrhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_recursionrhsf_prefix)) * mdr_nc_recursionrh)) /\ exists ff_q_mce_mdr_recursionrhsf_prefix_an. mdr_nb_recursionrh = ff_q_mce_mdr_recursionrhsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_recursionrhsf_prefix)) * mdr_nc_recursionrh) + (ff_an_mce_alternating_mdr_recursionrhsf_prefix))) /\ ((((exists ff_h_mce_mdr_recursionrhsf_prefix_bp. ff_h_mce_mdr_recursionrhsf_prefix_bp + S (ff_bp_mce_alternating_mdr_recursionrhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_recursionrhsf_prefix)) * mdr_ec_recursionrhs)) /\ exists ff_q_mce_mdr_recursionrhsf_prefix_bp. mdr_eb_recursionrhs = ff_q_mce_mdr_recursionrhsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_recursionrhsf_prefix)) * mdr_ec_recursionrhs) + (ff_bp_mce_alternating_mdr_recursionrhsf_prefix))) /\ ((((exists ff_h_mce_mdr_recursionrhsf_prefix_bn. ff_h_mce_mdr_recursionrhsf_prefix_bn + S (ff_bn_mce_alternating_mdr_recursionrhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_recursionrhsf_prefix)) * mdr_fc_recursionrhs)) /\ exists ff_q_mce_mdr_recursionrhsf_prefix_bn. mdr_fb_recursionrhs = ff_q_mce_mdr_recursionrhsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_recursionrhsf_prefix)) * mdr_fc_recursionrhs) + (ff_bn_mce_alternating_mdr_recursionrhsf_prefix))) /\ ((((exists ff_h_mce_mdr_recursionrhsf_prefix_positive. ff_h_mce_mdr_recursionrhsf_prefix_positive + S (ff_p_mce_alternating_mdr_recursionrhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_recursionrhsf_prefix)) * ff_uc_mce_fold_mdr_recursionrhsf)) /\ exists ff_q_mce_mdr_recursionrhsf_prefix_positive. ff_ub_mce_fold_mdr_recursionrhsf = ff_q_mce_mdr_recursionrhsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_recursionrhsf_prefix)) * ff_uc_mce_fold_mdr_recursionrhsf) + (ff_p_mce_alternating_mdr_recursionrhsf_prefix))) /\ ((((exists ff_h_mce_mdr_recursionrhsf_prefix_negative. ff_h_mce_mdr_recursionrhsf_prefix_negative + S (ff_n_mce_alternating_mdr_recursionrhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_recursionrhsf_prefix)) * ff_vc_mce_fold_mdr_recursionrhsf)) /\ exists ff_q_mce_mdr_recursionrhsf_prefix_negative. ff_vb_mce_fold_mdr_recursionrhsf = ff_q_mce_mdr_recursionrhsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_recursionrhsf_prefix)) * ff_vc_mce_fold_mdr_recursionrhsf) + (ff_n_mce_alternating_mdr_recursionrhsf_prefix))) /\ (((exists ff_even_mce_term_mdr_recursionrhsf_prefix_term. ff_index_mce_alternating_mdr_recursionrhsf_prefix = 2 * ff_even_mce_term_mdr_recursionrhsf_prefix_term) /\ (ff_p_mce_alternating_mdr_recursionrhsf_prefix = (ff_ap_mce_alternating_mdr_recursionrhsf_prefix) * (ff_bp_mce_alternating_mdr_recursionrhsf_prefix) + (ff_an_mce_alternating_mdr_recursionrhsf_prefix) * (ff_bn_mce_alternating_mdr_recursionrhsf_prefix) /\ ff_n_mce_alternating_mdr_recursionrhsf_prefix = (ff_ap_mce_alternating_mdr_recursionrhsf_prefix) * (ff_bn_mce_alternating_mdr_recursionrhsf_prefix) + (ff_an_mce_alternating_mdr_recursionrhsf_prefix) * (ff_bp_mce_alternating_mdr_recursionrhsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_recursionrhsf_prefix_term. ff_index_mce_alternating_mdr_recursionrhsf_prefix = 2 * ff_odd_mce_term_mdr_recursionrhsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_recursionrhsf_prefix = (ff_ap_mce_alternating_mdr_recursionrhsf_prefix) * (ff_bn_mce_alternating_mdr_recursionrhsf_prefix) + (ff_an_mce_alternating_mdr_recursionrhsf_prefix) * (ff_bp_mce_alternating_mdr_recursionrhsf_prefix) /\ ff_n_mce_alternating_mdr_recursionrhsf_prefix = (ff_ap_mce_alternating_mdr_recursionrhsf_prefix) * (ff_bp_mce_alternating_mdr_recursionrhsf_prefix) + (ff_an_mce_alternating_mdr_recursionrhsf_prefix) * (ff_bn_mce_alternating_mdr_recursionrhsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_recursionrhsf_positive ff_v_mce_mdr_recursionrhsf_positive. ((((exists ff_h_mce_mdr_recursionrhsf_positive_start. ff_h_mce_mdr_recursionrhsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_recursionrhsf_positive)) /\ exists ff_q_mce_mdr_recursionrhsf_positive_start. ff_u_mce_mdr_recursionrhsf_positive = ff_q_mce_mdr_recursionrhsf_positive_start * S ((S (0)) * ff_v_mce_mdr_recursionrhsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_recursionrhsf_positive_terminal. ff_h_mce_mdr_recursionrhsf_positive_terminal + S (mdr_p_recursionrh) = S ((S ((S (mdr_q_recursionrhs)))) * ff_v_mce_mdr_recursionrhsf_positive)) /\ exists ff_q_mce_mdr_recursionrhsf_positive_terminal. ff_u_mce_mdr_recursionrhsf_positive = ff_q_mce_mdr_recursionrhsf_positive_terminal * S ((S ((S (mdr_q_recursionrhs)))) * ff_v_mce_mdr_recursionrhsf_positive) + (mdr_p_recursionrh))) /\ forall ff_i_mce_mdr_recursionrhsf_positive. (exists ff_lt_mce_mdr_recursionrhsf_positive_bound. ff_lt_mce_mdr_recursionrhsf_positive_bound + S ff_i_mce_mdr_recursionrhsf_positive = (S (mdr_q_recursionrhs))) -> exists ff_a_mce_mdr_recursionrhsf_positive ff_r_mce_mdr_recursionrhsf_positive ff_s_mce_mdr_recursionrhsf_positive. ((((exists ff_h_mce_mdr_recursionrhsf_positive_summand. ff_h_mce_mdr_recursionrhsf_positive_summand + S (ff_a_mce_mdr_recursionrhsf_positive) = S ((S (ff_i_mce_mdr_recursionrhsf_positive)) * ff_uc_mce_fold_mdr_recursionrhsf)) /\ exists ff_q_mce_mdr_recursionrhsf_positive_summand. ff_ub_mce_fold_mdr_recursionrhsf = ff_q_mce_mdr_recursionrhsf_positive_summand * S ((S (ff_i_mce_mdr_recursionrhsf_positive)) * ff_uc_mce_fold_mdr_recursionrhsf) + (ff_a_mce_mdr_recursionrhsf_positive))) /\ ((((exists ff_h_mce_mdr_recursionrhsf_positive_partial. ff_h_mce_mdr_recursionrhsf_positive_partial + S (ff_r_mce_mdr_recursionrhsf_positive) = S ((S (ff_i_mce_mdr_recursionrhsf_positive)) * ff_v_mce_mdr_recursionrhsf_positive)) /\ exists ff_q_mce_mdr_recursionrhsf_positive_partial. ff_u_mce_mdr_recursionrhsf_positive = ff_q_mce_mdr_recursionrhsf_positive_partial * S ((S (ff_i_mce_mdr_recursionrhsf_positive)) * ff_v_mce_mdr_recursionrhsf_positive) + (ff_r_mce_mdr_recursionrhsf_positive))) /\ ((((exists ff_h_mce_mdr_recursionrhsf_positive_successor. ff_h_mce_mdr_recursionrhsf_positive_successor + S (ff_s_mce_mdr_recursionrhsf_positive) = S ((S (S ff_i_mce_mdr_recursionrhsf_positive)) * ff_v_mce_mdr_recursionrhsf_positive)) /\ exists ff_q_mce_mdr_recursionrhsf_positive_successor. ff_u_mce_mdr_recursionrhsf_positive = ff_q_mce_mdr_recursionrhsf_positive_successor * S ((S (S ff_i_mce_mdr_recursionrhsf_positive)) * ff_v_mce_mdr_recursionrhsf_positive) + (ff_s_mce_mdr_recursionrhsf_positive))) /\ ff_s_mce_mdr_recursionrhsf_positive = ff_r_mce_mdr_recursionrhsf_positive + ff_a_mce_mdr_recursionrhsf_positive)))))) /\ (exists ff_u_mce_mdr_recursionrhsf_negative ff_v_mce_mdr_recursionrhsf_negative. ((((exists ff_h_mce_mdr_recursionrhsf_negative_start. ff_h_mce_mdr_recursionrhsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_recursionrhsf_negative)) /\ exists ff_q_mce_mdr_recursionrhsf_negative_start. ff_u_mce_mdr_recursionrhsf_negative = ff_q_mce_mdr_recursionrhsf_negative_start * S ((S (0)) * ff_v_mce_mdr_recursionrhsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_recursionrhsf_negative_terminal. ff_h_mce_mdr_recursionrhsf_negative_terminal + S (mdr_n_recursionrh) = S ((S ((S (mdr_q_recursionrhs)))) * ff_v_mce_mdr_recursionrhsf_negative)) /\ exists ff_q_mce_mdr_recursionrhsf_negative_terminal. ff_u_mce_mdr_recursionrhsf_negative = ff_q_mce_mdr_recursionrhsf_negative_terminal * S ((S ((S (mdr_q_recursionrhs)))) * ff_v_mce_mdr_recursionrhsf_negative) + (mdr_n_recursionrh))) /\ forall ff_i_mce_mdr_recursionrhsf_negative. (exists ff_lt_mce_mdr_recursionrhsf_negative_bound. ff_lt_mce_mdr_recursionrhsf_negative_bound + S ff_i_mce_mdr_recursionrhsf_negative = (S (mdr_q_recursionrhs))) -> exists ff_a_mce_mdr_recursionrhsf_negative ff_r_mce_mdr_recursionrhsf_negative ff_s_mce_mdr_recursionrhsf_negative. ((((exists ff_h_mce_mdr_recursionrhsf_negative_summand. ff_h_mce_mdr_recursionrhsf_negative_summand + S (ff_a_mce_mdr_recursionrhsf_negative) = S ((S (ff_i_mce_mdr_recursionrhsf_negative)) * ff_vc_mce_fold_mdr_recursionrhsf)) /\ exists ff_q_mce_mdr_recursionrhsf_negative_summand. ff_vb_mce_fold_mdr_recursionrhsf = ff_q_mce_mdr_recursionrhsf_negative_summand * S ((S (ff_i_mce_mdr_recursionrhsf_negative)) * ff_vc_mce_fold_mdr_recursionrhsf) + (ff_a_mce_mdr_recursionrhsf_negative))) /\ ((((exists ff_h_mce_mdr_recursionrhsf_negative_partial. ff_h_mce_mdr_recursionrhsf_negative_partial + S (ff_r_mce_mdr_recursionrhsf_negative) = S ((S (ff_i_mce_mdr_recursionrhsf_negative)) * ff_v_mce_mdr_recursionrhsf_negative)) /\ exists ff_q_mce_mdr_recursionrhsf_negative_partial. ff_u_mce_mdr_recursionrhsf_negative = ff_q_mce_mdr_recursionrhsf_negative_partial * S ((S (ff_i_mce_mdr_recursionrhsf_negative)) * ff_v_mce_mdr_recursionrhsf_negative) + (ff_r_mce_mdr_recursionrhsf_negative))) /\ ((((exists ff_h_mce_mdr_recursionrhsf_negative_successor. ff_h_mce_mdr_recursionrhsf_negative_successor + S (ff_s_mce_mdr_recursionrhsf_negative) = S ((S (S ff_i_mce_mdr_recursionrhsf_negative)) * ff_v_mce_mdr_recursionrhsf_negative)) /\ exists ff_q_mce_mdr_recursionrhsf_negative_successor. ff_u_mce_mdr_recursionrhsf_negative = ff_q_mce_mdr_recursionrhsf_negative_successor * S ((S (S ff_i_mce_mdr_recursionrhsf_negative)) * ff_v_mce_mdr_recursionrhsf_negative) + (ff_s_mce_mdr_recursionrhsf_negative))) /\ ff_s_mce_mdr_recursionrhsf_negative = ff_r_mce_mdr_recursionrhsf_negative + ff_a_mce_mdr_recursionrhsf_negative))))))))))))))) /\ (exists mdr_z_recursionrr. ((exists mdr_a_recursionrrc mdr_b_recursionrrc mdr_c_recursionrrc mdr_e_recursionrrc mdr_f_recursionrrc. ((mdr_a_recursionrrc = ((q) + (mdr_pb_recursion)) * S ((q) + (mdr_pb_recursion)) + ((mdr_pb_recursion) + (mdr_pb_recursion))) /\ ((mdr_b_recursionrrc = ((mdr_pc_recursion) + (mdr_nb_recursion)) * S ((mdr_pc_recursion) + (mdr_nb_recursion)) + ((mdr_nb_recursion) + (mdr_nb_recursion))) /\ ((mdr_c_recursionrrc = ((mdr_a_recursionrrc) + (mdr_b_recursionrrc)) * S ((mdr_a_recursionrrc) + (mdr_b_recursionrrc)) + ((mdr_b_recursionrrc) + (mdr_b_recursionrrc))) /\ ((mdr_e_recursionrrc = ((mdr_p_recursion) + (mdr_n_recursion)) * S ((mdr_p_recursion) + (mdr_n_recursion)) + ((mdr_n_recursion) + (mdr_n_recursion))) /\ ((mdr_f_recursionrrc = ((mdr_nc_recursion) + (mdr_e_recursionrrc)) * S ((mdr_nc_recursion) + (mdr_e_recursionrrc)) + ((mdr_e_recursionrrc) + (mdr_e_recursionrrc))) /\ ((mdr_z_recursionrr) = ((mdr_c_recursionrrc) + (mdr_f_recursionrrc)) * S ((mdr_c_recursionrrc) + (mdr_f_recursionrrc)) + ((mdr_f_recursionrrc) + (mdr_f_recursionrrc))))))))) /\ (((exists ff_h_mdr_recursionrrb. ff_h_mdr_recursionrrb + S (mdr_z_recursionrr) = S ((S (mdr_t_recursion)) * mdr_v_recursion)) /\ exists ff_q_mdr_recursionrrb. mdr_u_recursion = ff_q_mdr_recursionrrb * S ((S (mdr_t_recursion)) * mdr_v_recursion) + (mdr_z_recursionrr))))))))) -> (exists mdr_gap_columns. mdr_gap_columns + (k) = (S q)) -> (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))))))))))))))) -> exists u v m eb ec fb fc. (((forall mdr_i_family_resultp mdr_a_family_resultp. (exists mdr_gap_family_resultpb. mdr_gap_family_resultpb + S (mdr_i_family_resultp) = (l)) -> (((exists ff_h_mdr_family_resultpo. ff_h_mdr_family_resultpo + S (mdr_a_family_resultp) = S ((S (mdr_i_family_resultp)) * c)) /\ exists ff_q_mdr_family_resultpo. b = ff_q_mdr_family_resultpo * S ((S (mdr_i_family_resultp)) * c) + (mdr_a_family_resultp))) -> (((exists ff_h_mdr_family_resultpn. ff_h_mdr_family_resultpn + S (mdr_a_family_resultp) = S ((S (mdr_i_family_resultp)) * v)) /\ exists ff_q_mdr_family_resultpn. u = ff_q_mdr_family_resultpn * S ((S (mdr_i_family_resultp)) * v) + (mdr_a_family_resultp)))) /\ ((exists mdr_gap_family_resultl. mdr_gap_family_resultl + (l) = (m)) /\ ((forall mdr_i_family_resulth. (exists mdr_gap_family_resulthi. mdr_gap_family_resulthi + S (mdr_i_family_resulth) = (m)) -> exists mdr_d_family_resulth mdr_pb_family_resulth mdr_pc_family_resulth mdr_nb_family_resulth mdr_nc_family_resulth mdr_p_family_resulth mdr_n_family_resulth. ((exists mdr_z_family_resulthr. ((exists mdr_a_family_resulthrc mdr_b_family_resulthrc mdr_c_family_resulthrc mdr_e_family_resulthrc mdr_f_family_resulthrc. ((mdr_a_family_resulthrc = ((mdr_d_family_resulth) + (mdr_pb_family_resulth)) * S ((mdr_d_family_resulth) + (mdr_pb_family_resulth)) + ((mdr_pb_family_resulth) + (mdr_pb_family_resulth))) /\ ((mdr_b_family_resulthrc = ((mdr_pc_family_resulth) + (mdr_nb_family_resulth)) * S ((mdr_pc_family_resulth) + (mdr_nb_family_resulth)) + ((mdr_nb_family_resulth) + (mdr_nb_family_resulth))) /\ ((mdr_c_family_resulthrc = ((mdr_a_family_resulthrc) + (mdr_b_family_resulthrc)) * S ((mdr_a_family_resulthrc) + (mdr_b_family_resulthrc)) + ((mdr_b_family_resulthrc) + (mdr_b_family_resulthrc))) /\ ((mdr_e_family_resulthrc = ((mdr_p_family_resulth) + (mdr_n_family_resulth)) * S ((mdr_p_family_resulth) + (mdr_n_family_resulth)) + ((mdr_n_family_resulth) + (mdr_n_family_resulth))) /\ ((mdr_f_family_resulthrc = ((mdr_nc_family_resulth) + (mdr_e_family_resulthrc)) * S ((mdr_nc_family_resulth) + (mdr_e_family_resulthrc)) + ((mdr_e_family_resulthrc) + (mdr_e_family_resulthrc))) /\ ((mdr_z_family_resulthr) = ((mdr_c_family_resulthrc) + (mdr_f_family_resulthrc)) * S ((mdr_c_family_resulthrc) + (mdr_f_family_resulthrc)) + ((mdr_f_family_resulthrc) + (mdr_f_family_resulthrc))))))))) /\ (((exists ff_h_mdr_family_resulthrb. ff_h_mdr_family_resulthrb + S (mdr_z_family_resulthr) = S ((S (mdr_i_family_resulth)) * v)) /\ exists ff_q_mdr_family_resulthrb. u = ff_q_mdr_family_resulthrb * S ((S (mdr_i_family_resulth)) * v) + (mdr_z_family_resulthr))))) /\ (((((mdr_d_family_resulth) = 0) /\ (((mdr_p_family_resulth) = 1) /\ ((mdr_n_family_resulth) = 0))) \/ exists mdr_q_family_resulths mdr_eb_family_resulths mdr_ec_family_resulths mdr_fb_family_resulths mdr_fc_family_resulths. (((mdr_d_family_resulth) = S (mdr_q_family_resulths)) /\ ((forall mdr_j_family_resulthsc. (exists mdr_gap_family_resulthscj. mdr_gap_family_resulthscj + S (mdr_j_family_resulthsc) = (S (mdr_q_family_resulths))) -> exists mdr_i_family_resulthsc mdr_up_family_resulthsc mdr_us_family_resulthsc mdr_un_family_resulthsc mdr_ut_family_resulthsc mdr_p_family_resulthsc mdr_n_family_resulthsc. ((exists mdr_gap_family_resulthsci. mdr_gap_family_resulthsci + S (mdr_i_family_resulthsc) = (mdr_i_family_resulth)) /\ ((exists mdr_z_family_resulthscr. ((exists mdr_a_family_resulthscrc mdr_b_family_resulthscrc mdr_c_family_resulthscrc mdr_e_family_resulthscrc mdr_f_family_resulthscrc. ((mdr_a_family_resulthscrc = ((mdr_q_family_resulths) + (mdr_up_family_resulthsc)) * S ((mdr_q_family_resulths) + (mdr_up_family_resulthsc)) + ((mdr_up_family_resulthsc) + (mdr_up_family_resulthsc))) /\ ((mdr_b_family_resulthscrc = ((mdr_us_family_resulthsc) + (mdr_un_family_resulthsc)) * S ((mdr_us_family_resulthsc) + (mdr_un_family_resulthsc)) + ((mdr_un_family_resulthsc) + (mdr_un_family_resulthsc))) /\ ((mdr_c_family_resulthscrc = ((mdr_a_family_resulthscrc) + (mdr_b_family_resulthscrc)) * S ((mdr_a_family_resulthscrc) + (mdr_b_family_resulthscrc)) + ((mdr_b_family_resulthscrc) + (mdr_b_family_resulthscrc))) /\ ((mdr_e_family_resulthscrc = ((mdr_p_family_resulthsc) + (mdr_n_family_resulthsc)) * S ((mdr_p_family_resulthsc) + (mdr_n_family_resulthsc)) + ((mdr_n_family_resulthsc) + (mdr_n_family_resulthsc))) /\ ((mdr_f_family_resulthscrc = ((mdr_ut_family_resulthsc) + (mdr_e_family_resulthscrc)) * S ((mdr_ut_family_resulthsc) + (mdr_e_family_resulthscrc)) + ((mdr_e_family_resulthscrc) + (mdr_e_family_resulthscrc))) /\ ((mdr_z_family_resulthscr) = ((mdr_c_family_resulthscrc) + (mdr_f_family_resulthscrc)) * S ((mdr_c_family_resulthscrc) + (mdr_f_family_resulthscrc)) + ((mdr_f_family_resulthscrc) + (mdr_f_family_resulthscrc))))))))) /\ (((exists ff_h_mdr_family_resulthscrb. ff_h_mdr_family_resulthscrb + S (mdr_z_family_resulthscr) = S ((S (mdr_i_family_resulthsc)) * v)) /\ exists ff_q_mdr_family_resulthscrb. u = ff_q_mdr_family_resulthscrb * S ((S (mdr_i_family_resulthsc)) * v) + (mdr_z_family_resulthscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_family_resulthscm_positive. (exists ff_gap_mdm_lt_mdr_family_resulthscm_positive_index_bound. ff_gap_mdm_lt_mdr_family_resulthscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_family_resulthscm_positive) = ((mdr_q_family_resulths) * (mdr_q_family_resulths))) -> exists ff_row_mdm_prefix_mdr_family_resulthscm_positive ff_column_mdm_prefix_mdr_family_resulthscm_positive ff_value_mdm_prefix_mdr_family_resulthscm_positive. (ff_index_mdm_prefix_mdr_family_resulthscm_positive = (mdr_q_family_resulths) * ff_row_mdm_prefix_mdr_family_resulthscm_positive + ff_column_mdm_prefix_mdr_family_resulthscm_positive /\ ((exists ff_gap_mdm_lt_mdr_family_resulthscm_positive_column_bound. ff_gap_mdm_lt_mdr_family_resulthscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_family_resulthscm_positive) = (mdr_q_family_resulths)) /\ ((exists ff_row_mdm_cell_mdr_family_resulthscm_positive_cell ff_column_mdm_cell_mdr_family_resulthscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_family_resulthscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_family_resulthscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_family_resulthscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_family_resulthscm_positive_cell = ff_row_mdm_prefix_mdr_family_resulthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_family_resulthscm_positive_cell_row_after. ff_gap_mdm_le_mdr_family_resulthscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_family_resulthscm_positive)) /\ ff_row_mdm_cell_mdr_family_resulthscm_positive_cell = S ff_row_mdm_prefix_mdr_family_resulthscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_family_resulthscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_family_resulthscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_family_resulthscm_positive) = (mdr_j_family_resulthsc)) /\ ff_column_mdm_cell_mdr_family_resulthscm_positive_cell = ff_column_mdm_prefix_mdr_family_resulthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_family_resulthscm_positive_cell_column_after. ff_gap_mdm_le_mdr_family_resulthscm_positive_cell_column_after + (mdr_j_family_resulthsc) = (ff_column_mdm_prefix_mdr_family_resulthscm_positive)) /\ ff_column_mdm_cell_mdr_family_resulthscm_positive_cell = S ff_column_mdm_prefix_mdr_family_resulthscm_positive))) /\ (((exists ff_h_mdm_mdr_family_resulthscm_positive_cell_source. ff_h_mdm_mdr_family_resulthscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_family_resulthscm_positive) = S ((S ((ff_row_mdm_cell_mdr_family_resulthscm_positive_cell) * (S (mdr_q_family_resulths)) + (ff_column_mdm_cell_mdr_family_resulthscm_positive_cell))) * mdr_pc_family_resulth)) /\ exists ff_q_mdm_mdr_family_resulthscm_positive_cell_source. mdr_pb_family_resulth = ff_q_mdm_mdr_family_resulthscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_family_resulthscm_positive_cell) * (S (mdr_q_family_resulths)) + (ff_column_mdm_cell_mdr_family_resulthscm_positive_cell))) * mdr_pc_family_resulth) + (ff_value_mdm_prefix_mdr_family_resulthscm_positive)))))) /\ (((exists ff_h_mdm_mdr_family_resulthscm_positive_target. ff_h_mdm_mdr_family_resulthscm_positive_target + S (ff_value_mdm_prefix_mdr_family_resulthscm_positive) = S ((S (ff_index_mdm_prefix_mdr_family_resulthscm_positive)) * mdr_us_family_resulthsc)) /\ exists ff_q_mdm_mdr_family_resulthscm_positive_target. mdr_up_family_resulthsc = ff_q_mdm_mdr_family_resulthscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_family_resulthscm_positive)) * mdr_us_family_resulthsc) + (ff_value_mdm_prefix_mdr_family_resulthscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_family_resulthscm_negative. (exists ff_gap_mdm_lt_mdr_family_resulthscm_negative_index_bound. ff_gap_mdm_lt_mdr_family_resulthscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_family_resulthscm_negative) = ((mdr_q_family_resulths) * (mdr_q_family_resulths))) -> exists ff_row_mdm_prefix_mdr_family_resulthscm_negative ff_column_mdm_prefix_mdr_family_resulthscm_negative ff_value_mdm_prefix_mdr_family_resulthscm_negative. (ff_index_mdm_prefix_mdr_family_resulthscm_negative = (mdr_q_family_resulths) * ff_row_mdm_prefix_mdr_family_resulthscm_negative + ff_column_mdm_prefix_mdr_family_resulthscm_negative /\ ((exists ff_gap_mdm_lt_mdr_family_resulthscm_negative_column_bound. ff_gap_mdm_lt_mdr_family_resulthscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_family_resulthscm_negative) = (mdr_q_family_resulths)) /\ ((exists ff_row_mdm_cell_mdr_family_resulthscm_negative_cell ff_column_mdm_cell_mdr_family_resulthscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_family_resulthscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_family_resulthscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_family_resulthscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_family_resulthscm_negative_cell = ff_row_mdm_prefix_mdr_family_resulthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_family_resulthscm_negative_cell_row_after. ff_gap_mdm_le_mdr_family_resulthscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_family_resulthscm_negative)) /\ ff_row_mdm_cell_mdr_family_resulthscm_negative_cell = S ff_row_mdm_prefix_mdr_family_resulthscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_family_resulthscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_family_resulthscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_family_resulthscm_negative) = (mdr_j_family_resulthsc)) /\ ff_column_mdm_cell_mdr_family_resulthscm_negative_cell = ff_column_mdm_prefix_mdr_family_resulthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_family_resulthscm_negative_cell_column_after. ff_gap_mdm_le_mdr_family_resulthscm_negative_cell_column_after + (mdr_j_family_resulthsc) = (ff_column_mdm_prefix_mdr_family_resulthscm_negative)) /\ ff_column_mdm_cell_mdr_family_resulthscm_negative_cell = S ff_column_mdm_prefix_mdr_family_resulthscm_negative))) /\ (((exists ff_h_mdm_mdr_family_resulthscm_negative_cell_source. ff_h_mdm_mdr_family_resulthscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_family_resulthscm_negative) = S ((S ((ff_row_mdm_cell_mdr_family_resulthscm_negative_cell) * (S (mdr_q_family_resulths)) + (ff_column_mdm_cell_mdr_family_resulthscm_negative_cell))) * mdr_nc_family_resulth)) /\ exists ff_q_mdm_mdr_family_resulthscm_negative_cell_source. mdr_nb_family_resulth = ff_q_mdm_mdr_family_resulthscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_family_resulthscm_negative_cell) * (S (mdr_q_family_resulths)) + (ff_column_mdm_cell_mdr_family_resulthscm_negative_cell))) * mdr_nc_family_resulth) + (ff_value_mdm_prefix_mdr_family_resulthscm_negative)))))) /\ (((exists ff_h_mdm_mdr_family_resulthscm_negative_target. ff_h_mdm_mdr_family_resulthscm_negative_target + S (ff_value_mdm_prefix_mdr_family_resulthscm_negative) = S ((S (ff_index_mdm_prefix_mdr_family_resulthscm_negative)) * mdr_ut_family_resulthsc)) /\ exists ff_q_mdm_mdr_family_resulthscm_negative_target. mdr_un_family_resulthsc = ff_q_mdm_mdr_family_resulthscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_family_resulthscm_negative)) * mdr_ut_family_resulthsc) + (ff_value_mdm_prefix_mdr_family_resulthscm_negative))))))))) /\ ((((exists ff_h_mdr_family_resulthscp. ff_h_mdr_family_resulthscp + S (mdr_p_family_resulthsc) = S ((S (mdr_j_family_resulthsc)) * mdr_ec_family_resulths)) /\ exists ff_q_mdr_family_resulthscp. mdr_eb_family_resulths = ff_q_mdr_family_resulthscp * S ((S (mdr_j_family_resulthsc)) * mdr_ec_family_resulths) + (mdr_p_family_resulthsc))) /\ (((exists ff_h_mdr_family_resulthscn. ff_h_mdr_family_resulthscn + S (mdr_n_family_resulthsc) = S ((S (mdr_j_family_resulthsc)) * mdr_fc_family_resulths)) /\ exists ff_q_mdr_family_resulthscn. mdr_fb_family_resulths = ff_q_mdr_family_resulthscn * S ((S (mdr_j_family_resulthsc)) * mdr_fc_family_resulths) + (mdr_n_family_resulthsc)))))))) /\ (exists ff_ub_mce_fold_mdr_family_resulthsf ff_uc_mce_fold_mdr_family_resulthsf ff_vb_mce_fold_mdr_family_resulthsf ff_vc_mce_fold_mdr_family_resulthsf. ((forall ff_index_mce_alternating_mdr_family_resulthsf_prefix. (exists ff_gap_mce_mdr_family_resulthsf_prefix_index. ff_gap_mce_mdr_family_resulthsf_prefix_index + S (ff_index_mce_alternating_mdr_family_resulthsf_prefix) = (S (mdr_q_family_resulths))) -> exists ff_ap_mce_alternating_mdr_family_resulthsf_prefix ff_an_mce_alternating_mdr_family_resulthsf_prefix ff_bp_mce_alternating_mdr_family_resulthsf_prefix ff_bn_mce_alternating_mdr_family_resulthsf_prefix ff_p_mce_alternating_mdr_family_resulthsf_prefix ff_n_mce_alternating_mdr_family_resulthsf_prefix. ((((exists ff_h_mce_mdr_family_resulthsf_prefix_ap. ff_h_mce_mdr_family_resulthsf_prefix_ap + S (ff_ap_mce_alternating_mdr_family_resulthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_family_resulthsf_prefix)) * mdr_pc_family_resulth)) /\ exists ff_q_mce_mdr_family_resulthsf_prefix_ap. mdr_pb_family_resulth = ff_q_mce_mdr_family_resulthsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_family_resulthsf_prefix)) * mdr_pc_family_resulth) + (ff_ap_mce_alternating_mdr_family_resulthsf_prefix))) /\ ((((exists ff_h_mce_mdr_family_resulthsf_prefix_an. ff_h_mce_mdr_family_resulthsf_prefix_an + S (ff_an_mce_alternating_mdr_family_resulthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_family_resulthsf_prefix)) * mdr_nc_family_resulth)) /\ exists ff_q_mce_mdr_family_resulthsf_prefix_an. mdr_nb_family_resulth = ff_q_mce_mdr_family_resulthsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_family_resulthsf_prefix)) * mdr_nc_family_resulth) + (ff_an_mce_alternating_mdr_family_resulthsf_prefix))) /\ ((((exists ff_h_mce_mdr_family_resulthsf_prefix_bp. ff_h_mce_mdr_family_resulthsf_prefix_bp + S (ff_bp_mce_alternating_mdr_family_resulthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_family_resulthsf_prefix)) * mdr_ec_family_resulths)) /\ exists ff_q_mce_mdr_family_resulthsf_prefix_bp. mdr_eb_family_resulths = ff_q_mce_mdr_family_resulthsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_family_resulthsf_prefix)) * mdr_ec_family_resulths) + (ff_bp_mce_alternating_mdr_family_resulthsf_prefix))) /\ ((((exists ff_h_mce_mdr_family_resulthsf_prefix_bn. ff_h_mce_mdr_family_resulthsf_prefix_bn + S (ff_bn_mce_alternating_mdr_family_resulthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_family_resulthsf_prefix)) * mdr_fc_family_resulths)) /\ exists ff_q_mce_mdr_family_resulthsf_prefix_bn. mdr_fb_family_resulths = ff_q_mce_mdr_family_resulthsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_family_resulthsf_prefix)) * mdr_fc_family_resulths) + (ff_bn_mce_alternating_mdr_family_resulthsf_prefix))) /\ ((((exists ff_h_mce_mdr_family_resulthsf_prefix_positive. ff_h_mce_mdr_family_resulthsf_prefix_positive + S (ff_p_mce_alternating_mdr_family_resulthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_family_resulthsf_prefix)) * ff_uc_mce_fold_mdr_family_resulthsf)) /\ exists ff_q_mce_mdr_family_resulthsf_prefix_positive. ff_ub_mce_fold_mdr_family_resulthsf = ff_q_mce_mdr_family_resulthsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_family_resulthsf_prefix)) * ff_uc_mce_fold_mdr_family_resulthsf) + (ff_p_mce_alternating_mdr_family_resulthsf_prefix))) /\ ((((exists ff_h_mce_mdr_family_resulthsf_prefix_negative. ff_h_mce_mdr_family_resulthsf_prefix_negative + S (ff_n_mce_alternating_mdr_family_resulthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_family_resulthsf_prefix)) * ff_vc_mce_fold_mdr_family_resulthsf)) /\ exists ff_q_mce_mdr_family_resulthsf_prefix_negative. ff_vb_mce_fold_mdr_family_resulthsf = ff_q_mce_mdr_family_resulthsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_family_resulthsf_prefix)) * ff_vc_mce_fold_mdr_family_resulthsf) + (ff_n_mce_alternating_mdr_family_resulthsf_prefix))) /\ (((exists ff_even_mce_term_mdr_family_resulthsf_prefix_term. ff_index_mce_alternating_mdr_family_resulthsf_prefix = 2 * ff_even_mce_term_mdr_family_resulthsf_prefix_term) /\ (ff_p_mce_alternating_mdr_family_resulthsf_prefix = (ff_ap_mce_alternating_mdr_family_resulthsf_prefix) * (ff_bp_mce_alternating_mdr_family_resulthsf_prefix) + (ff_an_mce_alternating_mdr_family_resulthsf_prefix) * (ff_bn_mce_alternating_mdr_family_resulthsf_prefix) /\ ff_n_mce_alternating_mdr_family_resulthsf_prefix = (ff_ap_mce_alternating_mdr_family_resulthsf_prefix) * (ff_bn_mce_alternating_mdr_family_resulthsf_prefix) + (ff_an_mce_alternating_mdr_family_resulthsf_prefix) * (ff_bp_mce_alternating_mdr_family_resulthsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_family_resulthsf_prefix_term. ff_index_mce_alternating_mdr_family_resulthsf_prefix = 2 * ff_odd_mce_term_mdr_family_resulthsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_family_resulthsf_prefix = (ff_ap_mce_alternating_mdr_family_resulthsf_prefix) * (ff_bn_mce_alternating_mdr_family_resulthsf_prefix) + (ff_an_mce_alternating_mdr_family_resulthsf_prefix) * (ff_bp_mce_alternating_mdr_family_resulthsf_prefix) /\ ff_n_mce_alternating_mdr_family_resulthsf_prefix = (ff_ap_mce_alternating_mdr_family_resulthsf_prefix) * (ff_bp_mce_alternating_mdr_family_resulthsf_prefix) + (ff_an_mce_alternating_mdr_family_resulthsf_prefix) * (ff_bn_mce_alternating_mdr_family_resulthsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_family_resulthsf_positive ff_v_mce_mdr_family_resulthsf_positive. ((((exists ff_h_mce_mdr_family_resulthsf_positive_start. ff_h_mce_mdr_family_resulthsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_family_resulthsf_positive)) /\ exists ff_q_mce_mdr_family_resulthsf_positive_start. ff_u_mce_mdr_family_resulthsf_positive = ff_q_mce_mdr_family_resulthsf_positive_start * S ((S (0)) * ff_v_mce_mdr_family_resulthsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_family_resulthsf_positive_terminal. ff_h_mce_mdr_family_resulthsf_positive_terminal + S (mdr_p_family_resulth) = S ((S ((S (mdr_q_family_resulths)))) * ff_v_mce_mdr_family_resulthsf_positive)) /\ exists ff_q_mce_mdr_family_resulthsf_positive_terminal. ff_u_mce_mdr_family_resulthsf_positive = ff_q_mce_mdr_family_resulthsf_positive_terminal * S ((S ((S (mdr_q_family_resulths)))) * ff_v_mce_mdr_family_resulthsf_positive) + (mdr_p_family_resulth))) /\ forall ff_i_mce_mdr_family_resulthsf_positive. (exists ff_lt_mce_mdr_family_resulthsf_positive_bound. ff_lt_mce_mdr_family_resulthsf_positive_bound + S ff_i_mce_mdr_family_resulthsf_positive = (S (mdr_q_family_resulths))) -> exists ff_a_mce_mdr_family_resulthsf_positive ff_r_mce_mdr_family_resulthsf_positive ff_s_mce_mdr_family_resulthsf_positive. ((((exists ff_h_mce_mdr_family_resulthsf_positive_summand. ff_h_mce_mdr_family_resulthsf_positive_summand + S (ff_a_mce_mdr_family_resulthsf_positive) = S ((S (ff_i_mce_mdr_family_resulthsf_positive)) * ff_uc_mce_fold_mdr_family_resulthsf)) /\ exists ff_q_mce_mdr_family_resulthsf_positive_summand. ff_ub_mce_fold_mdr_family_resulthsf = ff_q_mce_mdr_family_resulthsf_positive_summand * S ((S (ff_i_mce_mdr_family_resulthsf_positive)) * ff_uc_mce_fold_mdr_family_resulthsf) + (ff_a_mce_mdr_family_resulthsf_positive))) /\ ((((exists ff_h_mce_mdr_family_resulthsf_positive_partial. ff_h_mce_mdr_family_resulthsf_positive_partial + S (ff_r_mce_mdr_family_resulthsf_positive) = S ((S (ff_i_mce_mdr_family_resulthsf_positive)) * ff_v_mce_mdr_family_resulthsf_positive)) /\ exists ff_q_mce_mdr_family_resulthsf_positive_partial. ff_u_mce_mdr_family_resulthsf_positive = ff_q_mce_mdr_family_resulthsf_positive_partial * S ((S (ff_i_mce_mdr_family_resulthsf_positive)) * ff_v_mce_mdr_family_resulthsf_positive) + (ff_r_mce_mdr_family_resulthsf_positive))) /\ ((((exists ff_h_mce_mdr_family_resulthsf_positive_successor. ff_h_mce_mdr_family_resulthsf_positive_successor + S (ff_s_mce_mdr_family_resulthsf_positive) = S ((S (S ff_i_mce_mdr_family_resulthsf_positive)) * ff_v_mce_mdr_family_resulthsf_positive)) /\ exists ff_q_mce_mdr_family_resulthsf_positive_successor. ff_u_mce_mdr_family_resulthsf_positive = ff_q_mce_mdr_family_resulthsf_positive_successor * S ((S (S ff_i_mce_mdr_family_resulthsf_positive)) * ff_v_mce_mdr_family_resulthsf_positive) + (ff_s_mce_mdr_family_resulthsf_positive))) /\ ff_s_mce_mdr_family_resulthsf_positive = ff_r_mce_mdr_family_resulthsf_positive + ff_a_mce_mdr_family_resulthsf_positive)))))) /\ (exists ff_u_mce_mdr_family_resulthsf_negative ff_v_mce_mdr_family_resulthsf_negative. ((((exists ff_h_mce_mdr_family_resulthsf_negative_start. ff_h_mce_mdr_family_resulthsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_family_resulthsf_negative)) /\ exists ff_q_mce_mdr_family_resulthsf_negative_start. ff_u_mce_mdr_family_resulthsf_negative = ff_q_mce_mdr_family_resulthsf_negative_start * S ((S (0)) * ff_v_mce_mdr_family_resulthsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_family_resulthsf_negative_terminal. ff_h_mce_mdr_family_resulthsf_negative_terminal + S (mdr_n_family_resulth) = S ((S ((S (mdr_q_family_resulths)))) * ff_v_mce_mdr_family_resulthsf_negative)) /\ exists ff_q_mce_mdr_family_resulthsf_negative_terminal. ff_u_mce_mdr_family_resulthsf_negative = ff_q_mce_mdr_family_resulthsf_negative_terminal * S ((S ((S (mdr_q_family_resulths)))) * ff_v_mce_mdr_family_resulthsf_negative) + (mdr_n_family_resulth))) /\ forall ff_i_mce_mdr_family_resulthsf_negative. (exists ff_lt_mce_mdr_family_resulthsf_negative_bound. ff_lt_mce_mdr_family_resulthsf_negative_bound + S ff_i_mce_mdr_family_resulthsf_negative = (S (mdr_q_family_resulths))) -> exists ff_a_mce_mdr_family_resulthsf_negative ff_r_mce_mdr_family_resulthsf_negative ff_s_mce_mdr_family_resulthsf_negative. ((((exists ff_h_mce_mdr_family_resulthsf_negative_summand. ff_h_mce_mdr_family_resulthsf_negative_summand + S (ff_a_mce_mdr_family_resulthsf_negative) = S ((S (ff_i_mce_mdr_family_resulthsf_negative)) * ff_vc_mce_fold_mdr_family_resulthsf)) /\ exists ff_q_mce_mdr_family_resulthsf_negative_summand. ff_vb_mce_fold_mdr_family_resulthsf = ff_q_mce_mdr_family_resulthsf_negative_summand * S ((S (ff_i_mce_mdr_family_resulthsf_negative)) * ff_vc_mce_fold_mdr_family_resulthsf) + (ff_a_mce_mdr_family_resulthsf_negative))) /\ ((((exists ff_h_mce_mdr_family_resulthsf_negative_partial. ff_h_mce_mdr_family_resulthsf_negative_partial + S (ff_r_mce_mdr_family_resulthsf_negative) = S ((S (ff_i_mce_mdr_family_resulthsf_negative)) * ff_v_mce_mdr_family_resulthsf_negative)) /\ exists ff_q_mce_mdr_family_resulthsf_negative_partial. ff_u_mce_mdr_family_resulthsf_negative = ff_q_mce_mdr_family_resulthsf_negative_partial * S ((S (ff_i_mce_mdr_family_resulthsf_negative)) * ff_v_mce_mdr_family_resulthsf_negative) + (ff_r_mce_mdr_family_resulthsf_negative))) /\ ((((exists ff_h_mce_mdr_family_resulthsf_negative_successor. ff_h_mce_mdr_family_resulthsf_negative_successor + S (ff_s_mce_mdr_family_resulthsf_negative) = S ((S (S ff_i_mce_mdr_family_resulthsf_negative)) * ff_v_mce_mdr_family_resulthsf_negative)) /\ exists ff_q_mce_mdr_family_resulthsf_negative_successor. ff_u_mce_mdr_family_resulthsf_negative = ff_q_mce_mdr_family_resulthsf_negative_successor * S ((S (S ff_i_mce_mdr_family_resulthsf_negative)) * ff_v_mce_mdr_family_resulthsf_negative) + (ff_s_mce_mdr_family_resulthsf_negative))) /\ ff_s_mce_mdr_family_resulthsf_negative = ff_r_mce_mdr_family_resulthsf_negative + ff_a_mce_mdr_family_resulthsf_negative))))))))))))))) /\ (forall mdr_j_family_resultc. (exists mdr_gap_family_resultcj. mdr_gap_family_resultcj + S (mdr_j_family_resultc) = (k)) -> exists mdr_i_family_resultc mdr_up_family_resultc mdr_us_family_resultc mdr_un_family_resultc mdr_ut_family_resultc mdr_p_family_resultc mdr_n_family_resultc. ((exists mdr_gap_family_resultci. mdr_gap_family_resultci + S (mdr_i_family_resultc) = (m)) /\ ((exists mdr_z_family_resultcr. ((exists mdr_a_family_resultcrc mdr_b_family_resultcrc mdr_c_family_resultcrc mdr_e_family_resultcrc mdr_f_family_resultcrc. ((mdr_a_family_resultcrc = ((q) + (mdr_up_family_resultc)) * S ((q) + (mdr_up_family_resultc)) + ((mdr_up_family_resultc) + (mdr_up_family_resultc))) /\ ((mdr_b_family_resultcrc = ((mdr_us_family_resultc) + (mdr_un_family_resultc)) * S ((mdr_us_family_resultc) + (mdr_un_family_resultc)) + ((mdr_un_family_resultc) + (mdr_un_family_resultc))) /\ ((mdr_c_family_resultcrc = ((mdr_a_family_resultcrc) + (mdr_b_family_resultcrc)) * S ((mdr_a_family_resultcrc) + (mdr_b_family_resultcrc)) + ((mdr_b_family_resultcrc) + (mdr_b_family_resultcrc))) /\ ((mdr_e_family_resultcrc = ((mdr_p_family_resultc) + (mdr_n_family_resultc)) * S ((mdr_p_family_resultc) + (mdr_n_family_resultc)) + ((mdr_n_family_resultc) + (mdr_n_family_resultc))) /\ ((mdr_f_family_resultcrc = ((mdr_ut_family_resultc) + (mdr_e_family_resultcrc)) * S ((mdr_ut_family_resultc) + (mdr_e_family_resultcrc)) + ((mdr_e_family_resultcrc) + (mdr_e_family_resultcrc))) /\ ((mdr_z_family_resultcr) = ((mdr_c_family_resultcrc) + (mdr_f_family_resultcrc)) * S ((mdr_c_family_resultcrc) + (mdr_f_family_resultcrc)) + ((mdr_f_family_resultcrc) + (mdr_f_family_resultcrc))))))))) /\ (((exists ff_h_mdr_family_resultcrb. ff_h_mdr_family_resultcrb + S (mdr_z_family_resultcr) = S ((S (mdr_i_family_resultc)) * v)) /\ exists ff_q_mdr_family_resultcrb. u = ff_q_mdr_family_resultcrb * S ((S (mdr_i_family_resultc)) * v) + (mdr_z_family_resultcr))))) /\ ((((forall ff_index_mdm_prefix_mdr_family_resultcm_positive. (exists ff_gap_mdm_lt_mdr_family_resultcm_positive_index_bound. ff_gap_mdm_lt_mdr_family_resultcm_positive_index_bound + S (ff_index_mdm_prefix_mdr_family_resultcm_positive) = ((q) * (q))) -> exists ff_row_mdm_prefix_mdr_family_resultcm_positive ff_column_mdm_prefix_mdr_family_resultcm_positive ff_value_mdm_prefix_mdr_family_resultcm_positive. (ff_index_mdm_prefix_mdr_family_resultcm_positive = (q) * ff_row_mdm_prefix_mdr_family_resultcm_positive + ff_column_mdm_prefix_mdr_family_resultcm_positive /\ ((exists ff_gap_mdm_lt_mdr_family_resultcm_positive_column_bound. ff_gap_mdm_lt_mdr_family_resultcm_positive_column_bound + S (ff_column_mdm_prefix_mdr_family_resultcm_positive) = (q)) /\ ((exists ff_row_mdm_cell_mdr_family_resultcm_positive_cell ff_column_mdm_cell_mdr_family_resultcm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_family_resultcm_positive_cell_row_before. ff_gap_mdm_lt_mdr_family_resultcm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_family_resultcm_positive) = (0)) /\ ff_row_mdm_cell_mdr_family_resultcm_positive_cell = ff_row_mdm_prefix_mdr_family_resultcm_positive) \/ ((exists ff_gap_mdm_le_mdr_family_resultcm_positive_cell_row_after. ff_gap_mdm_le_mdr_family_resultcm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_family_resultcm_positive)) /\ ff_row_mdm_cell_mdr_family_resultcm_positive_cell = S ff_row_mdm_prefix_mdr_family_resultcm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_family_resultcm_positive_cell_column_before. ff_gap_mdm_lt_mdr_family_resultcm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_family_resultcm_positive) = (mdr_j_family_resultc)) /\ ff_column_mdm_cell_mdr_family_resultcm_positive_cell = ff_column_mdm_prefix_mdr_family_resultcm_positive) \/ ((exists ff_gap_mdm_le_mdr_family_resultcm_positive_cell_column_after. ff_gap_mdm_le_mdr_family_resultcm_positive_cell_column_after + (mdr_j_family_resultc) = (ff_column_mdm_prefix_mdr_family_resultcm_positive)) /\ ff_column_mdm_cell_mdr_family_resultcm_positive_cell = S ff_column_mdm_prefix_mdr_family_resultcm_positive))) /\ (((exists ff_h_mdm_mdr_family_resultcm_positive_cell_source. ff_h_mdm_mdr_family_resultcm_positive_cell_source + S (ff_value_mdm_prefix_mdr_family_resultcm_positive) = S ((S ((ff_row_mdm_cell_mdr_family_resultcm_positive_cell) * (S (q)) + (ff_column_mdm_cell_mdr_family_resultcm_positive_cell))) * pc)) /\ exists ff_q_mdm_mdr_family_resultcm_positive_cell_source. pb = ff_q_mdm_mdr_family_resultcm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_family_resultcm_positive_cell) * (S (q)) + (ff_column_mdm_cell_mdr_family_resultcm_positive_cell))) * pc) + (ff_value_mdm_prefix_mdr_family_resultcm_positive)))))) /\ (((exists ff_h_mdm_mdr_family_resultcm_positive_target. ff_h_mdm_mdr_family_resultcm_positive_target + S (ff_value_mdm_prefix_mdr_family_resultcm_positive) = S ((S (ff_index_mdm_prefix_mdr_family_resultcm_positive)) * mdr_us_family_resultc)) /\ exists ff_q_mdm_mdr_family_resultcm_positive_target. mdr_up_family_resultc = ff_q_mdm_mdr_family_resultcm_positive_target * S ((S (ff_index_mdm_prefix_mdr_family_resultcm_positive)) * mdr_us_family_resultc) + (ff_value_mdm_prefix_mdr_family_resultcm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_family_resultcm_negative. (exists ff_gap_mdm_lt_mdr_family_resultcm_negative_index_bound. ff_gap_mdm_lt_mdr_family_resultcm_negative_index_bound + S (ff_index_mdm_prefix_mdr_family_resultcm_negative) = ((q) * (q))) -> exists ff_row_mdm_prefix_mdr_family_resultcm_negative ff_column_mdm_prefix_mdr_family_resultcm_negative ff_value_mdm_prefix_mdr_family_resultcm_negative. (ff_index_mdm_prefix_mdr_family_resultcm_negative = (q) * ff_row_mdm_prefix_mdr_family_resultcm_negative + ff_column_mdm_prefix_mdr_family_resultcm_negative /\ ((exists ff_gap_mdm_lt_mdr_family_resultcm_negative_column_bound. ff_gap_mdm_lt_mdr_family_resultcm_negative_column_bound + S (ff_column_mdm_prefix_mdr_family_resultcm_negative) = (q)) /\ ((exists ff_row_mdm_cell_mdr_family_resultcm_negative_cell ff_column_mdm_cell_mdr_family_resultcm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_family_resultcm_negative_cell_row_before. ff_gap_mdm_lt_mdr_family_resultcm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_family_resultcm_negative) = (0)) /\ ff_row_mdm_cell_mdr_family_resultcm_negative_cell = ff_row_mdm_prefix_mdr_family_resultcm_negative) \/ ((exists ff_gap_mdm_le_mdr_family_resultcm_negative_cell_row_after. ff_gap_mdm_le_mdr_family_resultcm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_family_resultcm_negative)) /\ ff_row_mdm_cell_mdr_family_resultcm_negative_cell = S ff_row_mdm_prefix_mdr_family_resultcm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_family_resultcm_negative_cell_column_before. ff_gap_mdm_lt_mdr_family_resultcm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_family_resultcm_negative) = (mdr_j_family_resultc)) /\ ff_column_mdm_cell_mdr_family_resultcm_negative_cell = ff_column_mdm_prefix_mdr_family_resultcm_negative) \/ ((exists ff_gap_mdm_le_mdr_family_resultcm_negative_cell_column_after. ff_gap_mdm_le_mdr_family_resultcm_negative_cell_column_after + (mdr_j_family_resultc) = (ff_column_mdm_prefix_mdr_family_resultcm_negative)) /\ ff_column_mdm_cell_mdr_family_resultcm_negative_cell = S ff_column_mdm_prefix_mdr_family_resultcm_negative))) /\ (((exists ff_h_mdm_mdr_family_resultcm_negative_cell_source. ff_h_mdm_mdr_family_resultcm_negative_cell_source + S (ff_value_mdm_prefix_mdr_family_resultcm_negative) = S ((S ((ff_row_mdm_cell_mdr_family_resultcm_negative_cell) * (S (q)) + (ff_column_mdm_cell_mdr_family_resultcm_negative_cell))) * nc)) /\ exists ff_q_mdm_mdr_family_resultcm_negative_cell_source. nb = ff_q_mdm_mdr_family_resultcm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_family_resultcm_negative_cell) * (S (q)) + (ff_column_mdm_cell_mdr_family_resultcm_negative_cell))) * nc) + (ff_value_mdm_prefix_mdr_family_resultcm_negative)))))) /\ (((exists ff_h_mdm_mdr_family_resultcm_negative_target. ff_h_mdm_mdr_family_resultcm_negative_target + S (ff_value_mdm_prefix_mdr_family_resultcm_negative) = S ((S (ff_index_mdm_prefix_mdr_family_resultcm_negative)) * mdr_ut_family_resultc)) /\ exists ff_q_mdm_mdr_family_resultcm_negative_target. mdr_un_family_resultc = ff_q_mdm_mdr_family_resultcm_negative_target * S ((S (ff_index_mdm_prefix_mdr_family_resultcm_negative)) * mdr_ut_family_resultc) + (ff_value_mdm_prefix_mdr_family_resultcm_negative))))))))) /\ ((((exists ff_h_mdr_family_resultcp. ff_h_mdr_family_resultcp + S (mdr_p_family_resultc) = S ((S (mdr_j_family_resultc)) * ec)) /\ exists ff_q_mdr_family_resultcp. eb = ff_q_mdr_family_resultcp * S ((S (mdr_j_family_resultc)) * ec) + (mdr_p_family_resultc))) /\ (((exists ff_h_mdr_family_resultcn. ff_h_mdr_family_resultcn + S (mdr_n_family_resultc) = S ((S (mdr_j_family_resultc)) * fc)) /\ exists ff_q_mdr_family_resultcn. fb = ff_q_mdr_family_resultcn * S ((S (mdr_j_family_resultc)) * fc) + (mdr_n_family_resultc))))))))))))