absolute_recursive_determinant_exists_unique

Exact expanded first-order arithmetic statement

forall ab ac bb bc d. exists D. (((exists mdr_p_unique_absolute mdr_n_unique_absolute. ((exists mdr_b_unique_absoluteevaluation mdr_c_unique_absoluteevaluation mdr_l_unique_absoluteevaluation mdr_i_unique_absoluteevaluation. ((forall mdr_i_unique_absoluteevaluationh. (exists mdr_gap_unique_absoluteevaluationhi. mdr_gap_unique_absoluteevaluationhi + S (mdr_i_unique_absoluteevaluationh) = (mdr_l_unique_absoluteevaluation)) -> exists mdr_d_unique_absoluteevaluationh mdr_pb_unique_absoluteevaluationh mdr_pc_unique_absoluteevaluationh mdr_nb_unique_absoluteevaluationh mdr_nc_unique_absoluteevaluationh mdr_p_unique_absoluteevaluationh mdr_n_unique_absoluteevaluationh. ((exists mdr_z_unique_absoluteevaluationhr. ((exists mdr_a_unique_absoluteevaluationhrc mdr_b_unique_absoluteevaluationhrc mdr_c_unique_absoluteevaluationhrc mdr_e_unique_absoluteevaluationhrc mdr_f_unique_absoluteevaluationhrc. ((mdr_a_unique_absoluteevaluationhrc = ((mdr_d_unique_absoluteevaluationh) + (mdr_pb_unique_absoluteevaluationh)) * S ((mdr_d_unique_absoluteevaluationh) + (mdr_pb_unique_absoluteevaluationh)) + ((mdr_pb_unique_absoluteevaluationh) + (mdr_pb_unique_absoluteevaluationh))) /\ ((mdr_b_unique_absoluteevaluationhrc = ((mdr_pc_unique_absoluteevaluationh) + (mdr_nb_unique_absoluteevaluationh)) * S ((mdr_pc_unique_absoluteevaluationh) + (mdr_nb_unique_absoluteevaluationh)) + ((mdr_nb_unique_absoluteevaluationh) + (mdr_nb_unique_absoluteevaluationh))) /\ ((mdr_c_unique_absoluteevaluationhrc = ((mdr_a_unique_absoluteevaluationhrc) + (mdr_b_unique_absoluteevaluationhrc)) * S ((mdr_a_unique_absoluteevaluationhrc) + (mdr_b_unique_absoluteevaluationhrc)) + ((mdr_b_unique_absoluteevaluationhrc) + (mdr_b_unique_absoluteevaluationhrc))) /\ ((mdr_e_unique_absoluteevaluationhrc = ((mdr_p_unique_absoluteevaluationh) + (mdr_n_unique_absoluteevaluationh)) * S ((mdr_p_unique_absoluteevaluationh) + (mdr_n_unique_absoluteevaluationh)) + ((mdr_n_unique_absoluteevaluationh) + (mdr_n_unique_absoluteevaluationh))) /\ ((mdr_f_unique_absoluteevaluationhrc = ((mdr_nc_unique_absoluteevaluationh) + (mdr_e_unique_absoluteevaluationhrc)) * S ((mdr_nc_unique_absoluteevaluationh) + (mdr_e_unique_absoluteevaluationhrc)) + ((mdr_e_unique_absoluteevaluationhrc) + (mdr_e_unique_absoluteevaluationhrc))) /\ ((mdr_z_unique_absoluteevaluationhr) = ((mdr_c_unique_absoluteevaluationhrc) + (mdr_f_unique_absoluteevaluationhrc)) * S ((mdr_c_unique_absoluteevaluationhrc) + (mdr_f_unique_absoluteevaluationhrc)) + ((mdr_f_unique_absoluteevaluationhrc) + (mdr_f_unique_absoluteevaluationhrc))))))))) /\ (((exists ff_h_mdr_unique_absoluteevaluationhrb. ff_h_mdr_unique_absoluteevaluationhrb + S (mdr_z_unique_absoluteevaluationhr) = S ((S (mdr_i_unique_absoluteevaluationh)) * mdr_c_unique_absoluteevaluation)) /\ exists ff_q_mdr_unique_absoluteevaluationhrb. mdr_b_unique_absoluteevaluation = ff_q_mdr_unique_absoluteevaluationhrb * S ((S (mdr_i_unique_absoluteevaluationh)) * mdr_c_unique_absoluteevaluation) + (mdr_z_unique_absoluteevaluationhr))))) /\ (((((mdr_d_unique_absoluteevaluationh) = 0) /\ (((mdr_p_unique_absoluteevaluationh) = 1) /\ ((mdr_n_unique_absoluteevaluationh) = 0))) \/ exists mdr_q_unique_absoluteevaluationhs mdr_eb_unique_absoluteevaluationhs mdr_ec_unique_absoluteevaluationhs mdr_fb_unique_absoluteevaluationhs mdr_fc_unique_absoluteevaluationhs. (((mdr_d_unique_absoluteevaluationh) = S (mdr_q_unique_absoluteevaluationhs)) /\ ((forall mdr_j_unique_absoluteevaluationhsc. (exists mdr_gap_unique_absoluteevaluationhscj. mdr_gap_unique_absoluteevaluationhscj + S (mdr_j_unique_absoluteevaluationhsc) = (S (mdr_q_unique_absoluteevaluationhs))) -> exists mdr_i_unique_absoluteevaluationhsc mdr_up_unique_absoluteevaluationhsc mdr_us_unique_absoluteevaluationhsc mdr_un_unique_absoluteevaluationhsc mdr_ut_unique_absoluteevaluationhsc mdr_p_unique_absoluteevaluationhsc mdr_n_unique_absoluteevaluationhsc. ((exists mdr_gap_unique_absoluteevaluationhsci. mdr_gap_unique_absoluteevaluationhsci + S (mdr_i_unique_absoluteevaluationhsc) = (mdr_i_unique_absoluteevaluationh)) /\ ((exists mdr_z_unique_absoluteevaluationhscr. ((exists mdr_a_unique_absoluteevaluationhscrc mdr_b_unique_absoluteevaluationhscrc mdr_c_unique_absoluteevaluationhscrc mdr_e_unique_absoluteevaluationhscrc mdr_f_unique_absoluteevaluationhscrc. ((mdr_a_unique_absoluteevaluationhscrc = ((mdr_q_unique_absoluteevaluationhs) + (mdr_up_unique_absoluteevaluationhsc)) * S ((mdr_q_unique_absoluteevaluationhs) + (mdr_up_unique_absoluteevaluationhsc)) + ((mdr_up_unique_absoluteevaluationhsc) + (mdr_up_unique_absoluteevaluationhsc))) /\ ((mdr_b_unique_absoluteevaluationhscrc = ((mdr_us_unique_absoluteevaluationhsc) + (mdr_un_unique_absoluteevaluationhsc)) * S ((mdr_us_unique_absoluteevaluationhsc) + (mdr_un_unique_absoluteevaluationhsc)) + ((mdr_un_unique_absoluteevaluationhsc) + (mdr_un_unique_absoluteevaluationhsc))) /\ ((mdr_c_unique_absoluteevaluationhscrc = ((mdr_a_unique_absoluteevaluationhscrc) + (mdr_b_unique_absoluteevaluationhscrc)) * S ((mdr_a_unique_absoluteevaluationhscrc) + (mdr_b_unique_absoluteevaluationhscrc)) + ((mdr_b_unique_absoluteevaluationhscrc) + (mdr_b_unique_absoluteevaluationhscrc))) /\ ((mdr_e_unique_absoluteevaluationhscrc = ((mdr_p_unique_absoluteevaluationhsc) + (mdr_n_unique_absoluteevaluationhsc)) * S ((mdr_p_unique_absoluteevaluationhsc) + (mdr_n_unique_absoluteevaluationhsc)) + ((mdr_n_unique_absoluteevaluationhsc) + (mdr_n_unique_absoluteevaluationhsc))) /\ ((mdr_f_unique_absoluteevaluationhscrc = ((mdr_ut_unique_absoluteevaluationhsc) + (mdr_e_unique_absoluteevaluationhscrc)) * S ((mdr_ut_unique_absoluteevaluationhsc) + (mdr_e_unique_absoluteevaluationhscrc)) + ((mdr_e_unique_absoluteevaluationhscrc) + (mdr_e_unique_absoluteevaluationhscrc))) /\ ((mdr_z_unique_absoluteevaluationhscr) = ((mdr_c_unique_absoluteevaluationhscrc) + (mdr_f_unique_absoluteevaluationhscrc)) * S ((mdr_c_unique_absoluteevaluationhscrc) + (mdr_f_unique_absoluteevaluationhscrc)) + ((mdr_f_unique_absoluteevaluationhscrc) + (mdr_f_unique_absoluteevaluationhscrc))))))))) /\ (((exists ff_h_mdr_unique_absoluteevaluationhscrb. ff_h_mdr_unique_absoluteevaluationhscrb + S (mdr_z_unique_absoluteevaluationhscr) = S ((S (mdr_i_unique_absoluteevaluationhsc)) * mdr_c_unique_absoluteevaluation)) /\ exists ff_q_mdr_unique_absoluteevaluationhscrb. mdr_b_unique_absoluteevaluation = ff_q_mdr_unique_absoluteevaluationhscrb * S ((S (mdr_i_unique_absoluteevaluationhsc)) * mdr_c_unique_absoluteevaluation) + (mdr_z_unique_absoluteevaluationhscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_unique_absoluteevaluationhscm_positive. (exists ff_gap_mdm_lt_mdr_unique_absoluteevaluationhscm_positive_index_bound. ff_gap_mdm_lt_mdr_unique_absoluteevaluationhscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_unique_absoluteevaluationhscm_positive) = ((mdr_q_unique_absoluteevaluationhs) * (mdr_q_unique_absoluteevaluationhs))) -> exists ff_row_mdm_prefix_mdr_unique_absoluteevaluationhscm_positive ff_column_mdm_prefix_mdr_unique_absoluteevaluationhscm_positive ff_value_mdm_prefix_mdr_unique_absoluteevaluationhscm_positive. (ff_index_mdm_prefix_mdr_unique_absoluteevaluationhscm_positive = (mdr_q_unique_absoluteevaluationhs) * ff_row_mdm_prefix_mdr_unique_absoluteevaluationhscm_positive + ff_column_mdm_prefix_mdr_unique_absoluteevaluationhscm_positive /\ ((exists ff_gap_mdm_lt_mdr_unique_absoluteevaluationhscm_positive_column_bound. ff_gap_mdm_lt_mdr_unique_absoluteevaluationhscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_unique_absoluteevaluationhscm_positive) = (mdr_q_unique_absoluteevaluationhs)) /\ ((exists ff_row_mdm_cell_mdr_unique_absoluteevaluationhscm_positive_cell ff_column_mdm_cell_mdr_unique_absoluteevaluationhscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_unique_absoluteevaluationhscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_unique_absoluteevaluationhscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_unique_absoluteevaluationhscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_unique_absoluteevaluationhscm_positive_cell = ff_row_mdm_prefix_mdr_unique_absoluteevaluationhscm_positive) \/ ((exists ff_gap_mdm_le_mdr_unique_absoluteevaluationhscm_positive_cell_row_after. ff_gap_mdm_le_mdr_unique_absoluteevaluationhscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_unique_absoluteevaluationhscm_positive)) /\ ff_row_mdm_cell_mdr_unique_absoluteevaluationhscm_positive_cell = S ff_row_mdm_prefix_mdr_unique_absoluteevaluationhscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_unique_absoluteevaluationhscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_unique_absoluteevaluationhscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_unique_absoluteevaluationhscm_positive) = (mdr_j_unique_absoluteevaluationhsc)) /\ ff_column_mdm_cell_mdr_unique_absoluteevaluationhscm_positive_cell = ff_column_mdm_prefix_mdr_unique_absoluteevaluationhscm_positive) \/ ((exists ff_gap_mdm_le_mdr_unique_absoluteevaluationhscm_positive_cell_column_after. ff_gap_mdm_le_mdr_unique_absoluteevaluationhscm_positive_cell_column_after + (mdr_j_unique_absoluteevaluationhsc) = (ff_column_mdm_prefix_mdr_unique_absoluteevaluationhscm_positive)) /\ ff_column_mdm_cell_mdr_unique_absoluteevaluationhscm_positive_cell = S ff_column_mdm_prefix_mdr_unique_absoluteevaluationhscm_positive))) /\ (((exists ff_h_mdm_mdr_unique_absoluteevaluationhscm_positive_cell_source. ff_h_mdm_mdr_unique_absoluteevaluationhscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_unique_absoluteevaluationhscm_positive) = S ((S ((ff_row_mdm_cell_mdr_unique_absoluteevaluationhscm_positive_cell) * (S (mdr_q_unique_absoluteevaluationhs)) + (ff_column_mdm_cell_mdr_unique_absoluteevaluationhscm_positive_cell))) * mdr_pc_unique_absoluteevaluationh)) /\ exists ff_q_mdm_mdr_unique_absoluteevaluationhscm_positive_cell_source. mdr_pb_unique_absoluteevaluationh = ff_q_mdm_mdr_unique_absoluteevaluationhscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_unique_absoluteevaluationhscm_positive_cell) * (S (mdr_q_unique_absoluteevaluationhs)) + (ff_column_mdm_cell_mdr_unique_absoluteevaluationhscm_positive_cell))) * mdr_pc_unique_absoluteevaluationh) + (ff_value_mdm_prefix_mdr_unique_absoluteevaluationhscm_positive)))))) /\ (((exists ff_h_mdm_mdr_unique_absoluteevaluationhscm_positive_target. ff_h_mdm_mdr_unique_absoluteevaluationhscm_positive_target + S (ff_value_mdm_prefix_mdr_unique_absoluteevaluationhscm_positive) = S ((S (ff_index_mdm_prefix_mdr_unique_absoluteevaluationhscm_positive)) * mdr_us_unique_absoluteevaluationhsc)) /\ exists ff_q_mdm_mdr_unique_absoluteevaluationhscm_positive_target. mdr_up_unique_absoluteevaluationhsc = ff_q_mdm_mdr_unique_absoluteevaluationhscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_unique_absoluteevaluationhscm_positive)) * mdr_us_unique_absoluteevaluationhsc) + (ff_value_mdm_prefix_mdr_unique_absoluteevaluationhscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_unique_absoluteevaluationhscm_negative. (exists ff_gap_mdm_lt_mdr_unique_absoluteevaluationhscm_negative_index_bound. ff_gap_mdm_lt_mdr_unique_absoluteevaluationhscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_unique_absoluteevaluationhscm_negative) = ((mdr_q_unique_absoluteevaluationhs) * (mdr_q_unique_absoluteevaluationhs))) -> exists ff_row_mdm_prefix_mdr_unique_absoluteevaluationhscm_negative ff_column_mdm_prefix_mdr_unique_absoluteevaluationhscm_negative ff_value_mdm_prefix_mdr_unique_absoluteevaluationhscm_negative. (ff_index_mdm_prefix_mdr_unique_absoluteevaluationhscm_negative = (mdr_q_unique_absoluteevaluationhs) * ff_row_mdm_prefix_mdr_unique_absoluteevaluationhscm_negative + ff_column_mdm_prefix_mdr_unique_absoluteevaluationhscm_negative /\ ((exists ff_gap_mdm_lt_mdr_unique_absoluteevaluationhscm_negative_column_bound. ff_gap_mdm_lt_mdr_unique_absoluteevaluationhscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_unique_absoluteevaluationhscm_negative) = (mdr_q_unique_absoluteevaluationhs)) /\ ((exists ff_row_mdm_cell_mdr_unique_absoluteevaluationhscm_negative_cell ff_column_mdm_cell_mdr_unique_absoluteevaluationhscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_unique_absoluteevaluationhscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_unique_absoluteevaluationhscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_unique_absoluteevaluationhscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_unique_absoluteevaluationhscm_negative_cell = ff_row_mdm_prefix_mdr_unique_absoluteevaluationhscm_negative) \/ ((exists ff_gap_mdm_le_mdr_unique_absoluteevaluationhscm_negative_cell_row_after. ff_gap_mdm_le_mdr_unique_absoluteevaluationhscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_unique_absoluteevaluationhscm_negative)) /\ ff_row_mdm_cell_mdr_unique_absoluteevaluationhscm_negative_cell = S ff_row_mdm_prefix_mdr_unique_absoluteevaluationhscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_unique_absoluteevaluationhscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_unique_absoluteevaluationhscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_unique_absoluteevaluationhscm_negative) = (mdr_j_unique_absoluteevaluationhsc)) /\ ff_column_mdm_cell_mdr_unique_absoluteevaluationhscm_negative_cell = ff_column_mdm_prefix_mdr_unique_absoluteevaluationhscm_negative) \/ ((exists ff_gap_mdm_le_mdr_unique_absoluteevaluationhscm_negative_cell_column_after. ff_gap_mdm_le_mdr_unique_absoluteevaluationhscm_negative_cell_column_after + (mdr_j_unique_absoluteevaluationhsc) = (ff_column_mdm_prefix_mdr_unique_absoluteevaluationhscm_negative)) /\ ff_column_mdm_cell_mdr_unique_absoluteevaluationhscm_negative_cell = S ff_column_mdm_prefix_mdr_unique_absoluteevaluationhscm_negative))) /\ (((exists ff_h_mdm_mdr_unique_absoluteevaluationhscm_negative_cell_source. ff_h_mdm_mdr_unique_absoluteevaluationhscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_unique_absoluteevaluationhscm_negative) = S ((S ((ff_row_mdm_cell_mdr_unique_absoluteevaluationhscm_negative_cell) * (S (mdr_q_unique_absoluteevaluationhs)) + (ff_column_mdm_cell_mdr_unique_absoluteevaluationhscm_negative_cell))) * mdr_nc_unique_absoluteevaluationh)) /\ exists ff_q_mdm_mdr_unique_absoluteevaluationhscm_negative_cell_source. mdr_nb_unique_absoluteevaluationh = ff_q_mdm_mdr_unique_absoluteevaluationhscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_unique_absoluteevaluationhscm_negative_cell) * (S (mdr_q_unique_absoluteevaluationhs)) + (ff_column_mdm_cell_mdr_unique_absoluteevaluationhscm_negative_cell))) * mdr_nc_unique_absoluteevaluationh) + (ff_value_mdm_prefix_mdr_unique_absoluteevaluationhscm_negative)))))) /\ (((exists ff_h_mdm_mdr_unique_absoluteevaluationhscm_negative_target. ff_h_mdm_mdr_unique_absoluteevaluationhscm_negative_target + S (ff_value_mdm_prefix_mdr_unique_absoluteevaluationhscm_negative) = S ((S (ff_index_mdm_prefix_mdr_unique_absoluteevaluationhscm_negative)) * mdr_ut_unique_absoluteevaluationhsc)) /\ exists ff_q_mdm_mdr_unique_absoluteevaluationhscm_negative_target. mdr_un_unique_absoluteevaluationhsc = ff_q_mdm_mdr_unique_absoluteevaluationhscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_unique_absoluteevaluationhscm_negative)) * mdr_ut_unique_absoluteevaluationhsc) + (ff_value_mdm_prefix_mdr_unique_absoluteevaluationhscm_negative))))))))) /\ ((((exists ff_h_mdr_unique_absoluteevaluationhscp. ff_h_mdr_unique_absoluteevaluationhscp + S (mdr_p_unique_absoluteevaluationhsc) = S ((S (mdr_j_unique_absoluteevaluationhsc)) * mdr_ec_unique_absoluteevaluationhs)) /\ exists ff_q_mdr_unique_absoluteevaluationhscp. mdr_eb_unique_absoluteevaluationhs = ff_q_mdr_unique_absoluteevaluationhscp * S ((S (mdr_j_unique_absoluteevaluationhsc)) * mdr_ec_unique_absoluteevaluationhs) + (mdr_p_unique_absoluteevaluationhsc))) /\ (((exists ff_h_mdr_unique_absoluteevaluationhscn. ff_h_mdr_unique_absoluteevaluationhscn + S (mdr_n_unique_absoluteevaluationhsc) = S ((S (mdr_j_unique_absoluteevaluationhsc)) * mdr_fc_unique_absoluteevaluationhs)) /\ exists ff_q_mdr_unique_absoluteevaluationhscn. mdr_fb_unique_absoluteevaluationhs = ff_q_mdr_unique_absoluteevaluationhscn * S ((S (mdr_j_unique_absoluteevaluationhsc)) * mdr_fc_unique_absoluteevaluationhs) + (mdr_n_unique_absoluteevaluationhsc)))))))) /\ (exists ff_ub_mce_fold_mdr_unique_absoluteevaluationhsf ff_uc_mce_fold_mdr_unique_absoluteevaluationhsf ff_vb_mce_fold_mdr_unique_absoluteevaluationhsf ff_vc_mce_fold_mdr_unique_absoluteevaluationhsf. ((forall ff_index_mce_alternating_mdr_unique_absoluteevaluationhsf_prefix. (exists ff_gap_mce_mdr_unique_absoluteevaluationhsf_prefix_index. ff_gap_mce_mdr_unique_absoluteevaluationhsf_prefix_index + S (ff_index_mce_alternating_mdr_unique_absoluteevaluationhsf_prefix) = (S (mdr_q_unique_absoluteevaluationhs))) -> exists ff_ap_mce_alternating_mdr_unique_absoluteevaluationhsf_prefix ff_an_mce_alternating_mdr_unique_absoluteevaluationhsf_prefix ff_bp_mce_alternating_mdr_unique_absoluteevaluationhsf_prefix ff_bn_mce_alternating_mdr_unique_absoluteevaluationhsf_prefix ff_p_mce_alternating_mdr_unique_absoluteevaluationhsf_prefix ff_n_mce_alternating_mdr_unique_absoluteevaluationhsf_prefix. ((((exists ff_h_mce_mdr_unique_absoluteevaluationhsf_prefix_ap. ff_h_mce_mdr_unique_absoluteevaluationhsf_prefix_ap + S (ff_ap_mce_alternating_mdr_unique_absoluteevaluationhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_unique_absoluteevaluationhsf_prefix)) * mdr_pc_unique_absoluteevaluationh)) /\ exists ff_q_mce_mdr_unique_absoluteevaluationhsf_prefix_ap. mdr_pb_unique_absoluteevaluationh = ff_q_mce_mdr_unique_absoluteevaluationhsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_unique_absoluteevaluationhsf_prefix)) * mdr_pc_unique_absoluteevaluationh) + (ff_ap_mce_alternating_mdr_unique_absoluteevaluationhsf_prefix))) /\ ((((exists ff_h_mce_mdr_unique_absoluteevaluationhsf_prefix_an. ff_h_mce_mdr_unique_absoluteevaluationhsf_prefix_an + S (ff_an_mce_alternating_mdr_unique_absoluteevaluationhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_unique_absoluteevaluationhsf_prefix)) * mdr_nc_unique_absoluteevaluationh)) /\ exists ff_q_mce_mdr_unique_absoluteevaluationhsf_prefix_an. mdr_nb_unique_absoluteevaluationh = ff_q_mce_mdr_unique_absoluteevaluationhsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_unique_absoluteevaluationhsf_prefix)) * mdr_nc_unique_absoluteevaluationh) + (ff_an_mce_alternating_mdr_unique_absoluteevaluationhsf_prefix))) /\ ((((exists ff_h_mce_mdr_unique_absoluteevaluationhsf_prefix_bp. ff_h_mce_mdr_unique_absoluteevaluationhsf_prefix_bp + S (ff_bp_mce_alternating_mdr_unique_absoluteevaluationhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_unique_absoluteevaluationhsf_prefix)) * mdr_ec_unique_absoluteevaluationhs)) /\ exists ff_q_mce_mdr_unique_absoluteevaluationhsf_prefix_bp. mdr_eb_unique_absoluteevaluationhs = ff_q_mce_mdr_unique_absoluteevaluationhsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_unique_absoluteevaluationhsf_prefix)) * mdr_ec_unique_absoluteevaluationhs) + (ff_bp_mce_alternating_mdr_unique_absoluteevaluationhsf_prefix))) /\ ((((exists ff_h_mce_mdr_unique_absoluteevaluationhsf_prefix_bn. ff_h_mce_mdr_unique_absoluteevaluationhsf_prefix_bn + S (ff_bn_mce_alternating_mdr_unique_absoluteevaluationhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_unique_absoluteevaluationhsf_prefix)) * mdr_fc_unique_absoluteevaluationhs)) /\ exists ff_q_mce_mdr_unique_absoluteevaluationhsf_prefix_bn. mdr_fb_unique_absoluteevaluationhs = ff_q_mce_mdr_unique_absoluteevaluationhsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_unique_absoluteevaluationhsf_prefix)) * mdr_fc_unique_absoluteevaluationhs) + (ff_bn_mce_alternating_mdr_unique_absoluteevaluationhsf_prefix))) /\ ((((exists ff_h_mce_mdr_unique_absoluteevaluationhsf_prefix_positive. ff_h_mce_mdr_unique_absoluteevaluationhsf_prefix_positive + S (ff_p_mce_alternating_mdr_unique_absoluteevaluationhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_unique_absoluteevaluationhsf_prefix)) * ff_uc_mce_fold_mdr_unique_absoluteevaluationhsf)) /\ exists ff_q_mce_mdr_unique_absoluteevaluationhsf_prefix_positive. ff_ub_mce_fold_mdr_unique_absoluteevaluationhsf = ff_q_mce_mdr_unique_absoluteevaluationhsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_unique_absoluteevaluationhsf_prefix)) * ff_uc_mce_fold_mdr_unique_absoluteevaluationhsf) + (ff_p_mce_alternating_mdr_unique_absoluteevaluationhsf_prefix))) /\ ((((exists ff_h_mce_mdr_unique_absoluteevaluationhsf_prefix_negative. ff_h_mce_mdr_unique_absoluteevaluationhsf_prefix_negative + S (ff_n_mce_alternating_mdr_unique_absoluteevaluationhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_unique_absoluteevaluationhsf_prefix)) * ff_vc_mce_fold_mdr_unique_absoluteevaluationhsf)) /\ exists ff_q_mce_mdr_unique_absoluteevaluationhsf_prefix_negative. ff_vb_mce_fold_mdr_unique_absoluteevaluationhsf = ff_q_mce_mdr_unique_absoluteevaluationhsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_unique_absoluteevaluationhsf_prefix)) * ff_vc_mce_fold_mdr_unique_absoluteevaluationhsf) + (ff_n_mce_alternating_mdr_unique_absoluteevaluationhsf_prefix))) /\ (((exists ff_even_mce_term_mdr_unique_absoluteevaluationhsf_prefix_term. ff_index_mce_alternating_mdr_unique_absoluteevaluationhsf_prefix = 2 * ff_even_mce_term_mdr_unique_absoluteevaluationhsf_prefix_term) /\ (ff_p_mce_alternating_mdr_unique_absoluteevaluationhsf_prefix = (ff_ap_mce_alternating_mdr_unique_absoluteevaluationhsf_prefix) * (ff_bp_mce_alternating_mdr_unique_absoluteevaluationhsf_prefix) + (ff_an_mce_alternating_mdr_unique_absoluteevaluationhsf_prefix) * (ff_bn_mce_alternating_mdr_unique_absoluteevaluationhsf_prefix) /\ ff_n_mce_alternating_mdr_unique_absoluteevaluationhsf_prefix = (ff_ap_mce_alternating_mdr_unique_absoluteevaluationhsf_prefix) * (ff_bn_mce_alternating_mdr_unique_absoluteevaluationhsf_prefix) + (ff_an_mce_alternating_mdr_unique_absoluteevaluationhsf_prefix) * (ff_bp_mce_alternating_mdr_unique_absoluteevaluationhsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_unique_absoluteevaluationhsf_prefix_term. ff_index_mce_alternating_mdr_unique_absoluteevaluationhsf_prefix = 2 * ff_odd_mce_term_mdr_unique_absoluteevaluationhsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_unique_absoluteevaluationhsf_prefix = (ff_ap_mce_alternating_mdr_unique_absoluteevaluationhsf_prefix) * (ff_bn_mce_alternating_mdr_unique_absoluteevaluationhsf_prefix) + (ff_an_mce_alternating_mdr_unique_absoluteevaluationhsf_prefix) * (ff_bp_mce_alternating_mdr_unique_absoluteevaluationhsf_prefix) /\ ff_n_mce_alternating_mdr_unique_absoluteevaluationhsf_prefix = (ff_ap_mce_alternating_mdr_unique_absoluteevaluationhsf_prefix) * (ff_bp_mce_alternating_mdr_unique_absoluteevaluationhsf_prefix) + (ff_an_mce_alternating_mdr_unique_absoluteevaluationhsf_prefix) * (ff_bn_mce_alternating_mdr_unique_absoluteevaluationhsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_unique_absoluteevaluationhsf_positive ff_v_mce_mdr_unique_absoluteevaluationhsf_positive. ((((exists ff_h_mce_mdr_unique_absoluteevaluationhsf_positive_start. ff_h_mce_mdr_unique_absoluteevaluationhsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_unique_absoluteevaluationhsf_positive)) /\ exists ff_q_mce_mdr_unique_absoluteevaluationhsf_positive_start. ff_u_mce_mdr_unique_absoluteevaluationhsf_positive = ff_q_mce_mdr_unique_absoluteevaluationhsf_positive_start * S ((S (0)) * ff_v_mce_mdr_unique_absoluteevaluationhsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_unique_absoluteevaluationhsf_positive_terminal. ff_h_mce_mdr_unique_absoluteevaluationhsf_positive_terminal + S (mdr_p_unique_absoluteevaluationh) = S ((S ((S (mdr_q_unique_absoluteevaluationhs)))) * ff_v_mce_mdr_unique_absoluteevaluationhsf_positive)) /\ exists ff_q_mce_mdr_unique_absoluteevaluationhsf_positive_terminal. ff_u_mce_mdr_unique_absoluteevaluationhsf_positive = ff_q_mce_mdr_unique_absoluteevaluationhsf_positive_terminal * S ((S ((S (mdr_q_unique_absoluteevaluationhs)))) * ff_v_mce_mdr_unique_absoluteevaluationhsf_positive) + (mdr_p_unique_absoluteevaluationh))) /\ forall ff_i_mce_mdr_unique_absoluteevaluationhsf_positive. (exists ff_lt_mce_mdr_unique_absoluteevaluationhsf_positive_bound. ff_lt_mce_mdr_unique_absoluteevaluationhsf_positive_bound + S ff_i_mce_mdr_unique_absoluteevaluationhsf_positive = (S (mdr_q_unique_absoluteevaluationhs))) -> exists ff_a_mce_mdr_unique_absoluteevaluationhsf_positive ff_r_mce_mdr_unique_absoluteevaluationhsf_positive ff_s_mce_mdr_unique_absoluteevaluationhsf_positive. ((((exists ff_h_mce_mdr_unique_absoluteevaluationhsf_positive_summand. ff_h_mce_mdr_unique_absoluteevaluationhsf_positive_summand + S (ff_a_mce_mdr_unique_absoluteevaluationhsf_positive) = S ((S (ff_i_mce_mdr_unique_absoluteevaluationhsf_positive)) * ff_uc_mce_fold_mdr_unique_absoluteevaluationhsf)) /\ exists ff_q_mce_mdr_unique_absoluteevaluationhsf_positive_summand. ff_ub_mce_fold_mdr_unique_absoluteevaluationhsf = ff_q_mce_mdr_unique_absoluteevaluationhsf_positive_summand * S ((S (ff_i_mce_mdr_unique_absoluteevaluationhsf_positive)) * ff_uc_mce_fold_mdr_unique_absoluteevaluationhsf) + (ff_a_mce_mdr_unique_absoluteevaluationhsf_positive))) /\ ((((exists ff_h_mce_mdr_unique_absoluteevaluationhsf_positive_partial. ff_h_mce_mdr_unique_absoluteevaluationhsf_positive_partial + S (ff_r_mce_mdr_unique_absoluteevaluationhsf_positive) = S ((S (ff_i_mce_mdr_unique_absoluteevaluationhsf_positive)) * ff_v_mce_mdr_unique_absoluteevaluationhsf_positive)) /\ exists ff_q_mce_mdr_unique_absoluteevaluationhsf_positive_partial. ff_u_mce_mdr_unique_absoluteevaluationhsf_positive = ff_q_mce_mdr_unique_absoluteevaluationhsf_positive_partial * S ((S (ff_i_mce_mdr_unique_absoluteevaluationhsf_positive)) * ff_v_mce_mdr_unique_absoluteevaluationhsf_positive) + (ff_r_mce_mdr_unique_absoluteevaluationhsf_positive))) /\ ((((exists ff_h_mce_mdr_unique_absoluteevaluationhsf_positive_successor. ff_h_mce_mdr_unique_absoluteevaluationhsf_positive_successor + S (ff_s_mce_mdr_unique_absoluteevaluationhsf_positive) = S ((S (S ff_i_mce_mdr_unique_absoluteevaluationhsf_positive)) * ff_v_mce_mdr_unique_absoluteevaluationhsf_positive)) /\ exists ff_q_mce_mdr_unique_absoluteevaluationhsf_positive_successor. ff_u_mce_mdr_unique_absoluteevaluationhsf_positive = ff_q_mce_mdr_unique_absoluteevaluationhsf_positive_successor * S ((S (S ff_i_mce_mdr_unique_absoluteevaluationhsf_positive)) * ff_v_mce_mdr_unique_absoluteevaluationhsf_positive) + (ff_s_mce_mdr_unique_absoluteevaluationhsf_positive))) /\ ff_s_mce_mdr_unique_absoluteevaluationhsf_positive = ff_r_mce_mdr_unique_absoluteevaluationhsf_positive + ff_a_mce_mdr_unique_absoluteevaluationhsf_positive)))))) /\ (exists ff_u_mce_mdr_unique_absoluteevaluationhsf_negative ff_v_mce_mdr_unique_absoluteevaluationhsf_negative. ((((exists ff_h_mce_mdr_unique_absoluteevaluationhsf_negative_start. ff_h_mce_mdr_unique_absoluteevaluationhsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_unique_absoluteevaluationhsf_negative)) /\ exists ff_q_mce_mdr_unique_absoluteevaluationhsf_negative_start. ff_u_mce_mdr_unique_absoluteevaluationhsf_negative = ff_q_mce_mdr_unique_absoluteevaluationhsf_negative_start * S ((S (0)) * ff_v_mce_mdr_unique_absoluteevaluationhsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_unique_absoluteevaluationhsf_negative_terminal. ff_h_mce_mdr_unique_absoluteevaluationhsf_negative_terminal + S (mdr_n_unique_absoluteevaluationh) = S ((S ((S (mdr_q_unique_absoluteevaluationhs)))) * ff_v_mce_mdr_unique_absoluteevaluationhsf_negative)) /\ exists ff_q_mce_mdr_unique_absoluteevaluationhsf_negative_terminal. ff_u_mce_mdr_unique_absoluteevaluationhsf_negative = ff_q_mce_mdr_unique_absoluteevaluationhsf_negative_terminal * S ((S ((S (mdr_q_unique_absoluteevaluationhs)))) * ff_v_mce_mdr_unique_absoluteevaluationhsf_negative) + (mdr_n_unique_absoluteevaluationh))) /\ forall ff_i_mce_mdr_unique_absoluteevaluationhsf_negative. (exists ff_lt_mce_mdr_unique_absoluteevaluationhsf_negative_bound. ff_lt_mce_mdr_unique_absoluteevaluationhsf_negative_bound + S ff_i_mce_mdr_unique_absoluteevaluationhsf_negative = (S (mdr_q_unique_absoluteevaluationhs))) -> exists ff_a_mce_mdr_unique_absoluteevaluationhsf_negative ff_r_mce_mdr_unique_absoluteevaluationhsf_negative ff_s_mce_mdr_unique_absoluteevaluationhsf_negative. ((((exists ff_h_mce_mdr_unique_absoluteevaluationhsf_negative_summand. ff_h_mce_mdr_unique_absoluteevaluationhsf_negative_summand + S (ff_a_mce_mdr_unique_absoluteevaluationhsf_negative) = S ((S (ff_i_mce_mdr_unique_absoluteevaluationhsf_negative)) * ff_vc_mce_fold_mdr_unique_absoluteevaluationhsf)) /\ exists ff_q_mce_mdr_unique_absoluteevaluationhsf_negative_summand. ff_vb_mce_fold_mdr_unique_absoluteevaluationhsf = ff_q_mce_mdr_unique_absoluteevaluationhsf_negative_summand * S ((S (ff_i_mce_mdr_unique_absoluteevaluationhsf_negative)) * ff_vc_mce_fold_mdr_unique_absoluteevaluationhsf) + (ff_a_mce_mdr_unique_absoluteevaluationhsf_negative))) /\ ((((exists ff_h_mce_mdr_unique_absoluteevaluationhsf_negative_partial. ff_h_mce_mdr_unique_absoluteevaluationhsf_negative_partial + S (ff_r_mce_mdr_unique_absoluteevaluationhsf_negative) = S ((S (ff_i_mce_mdr_unique_absoluteevaluationhsf_negative)) * ff_v_mce_mdr_unique_absoluteevaluationhsf_negative)) /\ exists ff_q_mce_mdr_unique_absoluteevaluationhsf_negative_partial. ff_u_mce_mdr_unique_absoluteevaluationhsf_negative = ff_q_mce_mdr_unique_absoluteevaluationhsf_negative_partial * S ((S (ff_i_mce_mdr_unique_absoluteevaluationhsf_negative)) * ff_v_mce_mdr_unique_absoluteevaluationhsf_negative) + (ff_r_mce_mdr_unique_absoluteevaluationhsf_negative))) /\ ((((exists ff_h_mce_mdr_unique_absoluteevaluationhsf_negative_successor. ff_h_mce_mdr_unique_absoluteevaluationhsf_negative_successor + S (ff_s_mce_mdr_unique_absoluteevaluationhsf_negative) = S ((S (S ff_i_mce_mdr_unique_absoluteevaluationhsf_negative)) * ff_v_mce_mdr_unique_absoluteevaluationhsf_negative)) /\ exists ff_q_mce_mdr_unique_absoluteevaluationhsf_negative_successor. ff_u_mce_mdr_unique_absoluteevaluationhsf_negative = ff_q_mce_mdr_unique_absoluteevaluationhsf_negative_successor * S ((S (S ff_i_mce_mdr_unique_absoluteevaluationhsf_negative)) * ff_v_mce_mdr_unique_absoluteevaluationhsf_negative) + (ff_s_mce_mdr_unique_absoluteevaluationhsf_negative))) /\ ff_s_mce_mdr_unique_absoluteevaluationhsf_negative = ff_r_mce_mdr_unique_absoluteevaluationhsf_negative + ff_a_mce_mdr_unique_absoluteevaluationhsf_negative))))))))))))))) /\ ((exists mdr_gap_unique_absoluteevaluationi. mdr_gap_unique_absoluteevaluationi + S (mdr_i_unique_absoluteevaluation) = (mdr_l_unique_absoluteevaluation)) /\ (exists mdr_z_unique_absoluteevaluationr. ((exists mdr_a_unique_absoluteevaluationrc mdr_b_unique_absoluteevaluationrc mdr_c_unique_absoluteevaluationrc mdr_e_unique_absoluteevaluationrc mdr_f_unique_absoluteevaluationrc. ((mdr_a_unique_absoluteevaluationrc = ((d) + (ab)) * S ((d) + (ab)) + ((ab) + (ab))) /\ ((mdr_b_unique_absoluteevaluationrc = ((ac) + (bb)) * S ((ac) + (bb)) + ((bb) + (bb))) /\ ((mdr_c_unique_absoluteevaluationrc = ((mdr_a_unique_absoluteevaluationrc) + (mdr_b_unique_absoluteevaluationrc)) * S ((mdr_a_unique_absoluteevaluationrc) + (mdr_b_unique_absoluteevaluationrc)) + ((mdr_b_unique_absoluteevaluationrc) + (mdr_b_unique_absoluteevaluationrc))) /\ ((mdr_e_unique_absoluteevaluationrc = ((mdr_p_unique_absolute) + (mdr_n_unique_absolute)) * S ((mdr_p_unique_absolute) + (mdr_n_unique_absolute)) + ((mdr_n_unique_absolute) + (mdr_n_unique_absolute))) /\ ((mdr_f_unique_absoluteevaluationrc = ((bc) + (mdr_e_unique_absoluteevaluationrc)) * S ((bc) + (mdr_e_unique_absoluteevaluationrc)) + ((mdr_e_unique_absoluteevaluationrc) + (mdr_e_unique_absoluteevaluationrc))) /\ ((mdr_z_unique_absoluteevaluationr) = ((mdr_c_unique_absoluteevaluationrc) + (mdr_f_unique_absoluteevaluationrc)) * S ((mdr_c_unique_absoluteevaluationrc) + (mdr_f_unique_absoluteevaluationrc)) + ((mdr_f_unique_absoluteevaluationrc) + (mdr_f_unique_absoluteevaluationrc))))))))) /\ (((exists ff_h_mdr_unique_absoluteevaluationrb. ff_h_mdr_unique_absoluteevaluationrb + S (mdr_z_unique_absoluteevaluationr) = S ((S (mdr_i_unique_absoluteevaluation)) * mdr_c_unique_absoluteevaluation)) /\ exists ff_q_mdr_unique_absoluteevaluationrb. mdr_b_unique_absoluteevaluation = ff_q_mdr_unique_absoluteevaluationrb * S ((S (mdr_i_unique_absoluteevaluation)) * mdr_c_unique_absoluteevaluation) + (mdr_z_unique_absoluteevaluationr)))))))) /\ (((mdr_p_unique_absolute) = (mdr_n_unique_absolute) + (D)) \/ ((mdr_n_unique_absolute) = (mdr_p_unique_absolute) + (D))))) /\ (forall E. (exists mdr_p_other_absolute mdr_n_other_absolute. ((exists mdr_b_other_absoluteevaluation mdr_c_other_absoluteevaluation mdr_l_other_absoluteevaluation mdr_i_other_absoluteevaluation. ((forall mdr_i_other_absoluteevaluationh. (exists mdr_gap_other_absoluteevaluationhi. mdr_gap_other_absoluteevaluationhi + S (mdr_i_other_absoluteevaluationh) = (mdr_l_other_absoluteevaluation)) -> exists mdr_d_other_absoluteevaluationh mdr_pb_other_absoluteevaluationh mdr_pc_other_absoluteevaluationh mdr_nb_other_absoluteevaluationh mdr_nc_other_absoluteevaluationh mdr_p_other_absoluteevaluationh mdr_n_other_absoluteevaluationh. ((exists mdr_z_other_absoluteevaluationhr. ((exists mdr_a_other_absoluteevaluationhrc mdr_b_other_absoluteevaluationhrc mdr_c_other_absoluteevaluationhrc mdr_e_other_absoluteevaluationhrc mdr_f_other_absoluteevaluationhrc. ((mdr_a_other_absoluteevaluationhrc = ((mdr_d_other_absoluteevaluationh) + (mdr_pb_other_absoluteevaluationh)) * S ((mdr_d_other_absoluteevaluationh) + (mdr_pb_other_absoluteevaluationh)) + ((mdr_pb_other_absoluteevaluationh) + (mdr_pb_other_absoluteevaluationh))) /\ ((mdr_b_other_absoluteevaluationhrc = ((mdr_pc_other_absoluteevaluationh) + (mdr_nb_other_absoluteevaluationh)) * S ((mdr_pc_other_absoluteevaluationh) + (mdr_nb_other_absoluteevaluationh)) + ((mdr_nb_other_absoluteevaluationh) + (mdr_nb_other_absoluteevaluationh))) /\ ((mdr_c_other_absoluteevaluationhrc = ((mdr_a_other_absoluteevaluationhrc) + (mdr_b_other_absoluteevaluationhrc)) * S ((mdr_a_other_absoluteevaluationhrc) + (mdr_b_other_absoluteevaluationhrc)) + ((mdr_b_other_absoluteevaluationhrc) + (mdr_b_other_absoluteevaluationhrc))) /\ ((mdr_e_other_absoluteevaluationhrc = ((mdr_p_other_absoluteevaluationh) + (mdr_n_other_absoluteevaluationh)) * S ((mdr_p_other_absoluteevaluationh) + (mdr_n_other_absoluteevaluationh)) + ((mdr_n_other_absoluteevaluationh) + (mdr_n_other_absoluteevaluationh))) /\ ((mdr_f_other_absoluteevaluationhrc = ((mdr_nc_other_absoluteevaluationh) + (mdr_e_other_absoluteevaluationhrc)) * S ((mdr_nc_other_absoluteevaluationh) + (mdr_e_other_absoluteevaluationhrc)) + ((mdr_e_other_absoluteevaluationhrc) + (mdr_e_other_absoluteevaluationhrc))) /\ ((mdr_z_other_absoluteevaluationhr) = ((mdr_c_other_absoluteevaluationhrc) + (mdr_f_other_absoluteevaluationhrc)) * S ((mdr_c_other_absoluteevaluationhrc) + (mdr_f_other_absoluteevaluationhrc)) + ((mdr_f_other_absoluteevaluationhrc) + (mdr_f_other_absoluteevaluationhrc))))))))) /\ (((exists ff_h_mdr_other_absoluteevaluationhrb. ff_h_mdr_other_absoluteevaluationhrb + S (mdr_z_other_absoluteevaluationhr) = S ((S (mdr_i_other_absoluteevaluationh)) * mdr_c_other_absoluteevaluation)) /\ exists ff_q_mdr_other_absoluteevaluationhrb. mdr_b_other_absoluteevaluation = ff_q_mdr_other_absoluteevaluationhrb * S ((S (mdr_i_other_absoluteevaluationh)) * mdr_c_other_absoluteevaluation) + (mdr_z_other_absoluteevaluationhr))))) /\ (((((mdr_d_other_absoluteevaluationh) = 0) /\ (((mdr_p_other_absoluteevaluationh) = 1) /\ ((mdr_n_other_absoluteevaluationh) = 0))) \/ exists mdr_q_other_absoluteevaluationhs mdr_eb_other_absoluteevaluationhs mdr_ec_other_absoluteevaluationhs mdr_fb_other_absoluteevaluationhs mdr_fc_other_absoluteevaluationhs. (((mdr_d_other_absoluteevaluationh) = S (mdr_q_other_absoluteevaluationhs)) /\ ((forall mdr_j_other_absoluteevaluationhsc. (exists mdr_gap_other_absoluteevaluationhscj. mdr_gap_other_absoluteevaluationhscj + S (mdr_j_other_absoluteevaluationhsc) = (S (mdr_q_other_absoluteevaluationhs))) -> exists mdr_i_other_absoluteevaluationhsc mdr_up_other_absoluteevaluationhsc mdr_us_other_absoluteevaluationhsc mdr_un_other_absoluteevaluationhsc mdr_ut_other_absoluteevaluationhsc mdr_p_other_absoluteevaluationhsc mdr_n_other_absoluteevaluationhsc. ((exists mdr_gap_other_absoluteevaluationhsci. mdr_gap_other_absoluteevaluationhsci + S (mdr_i_other_absoluteevaluationhsc) = (mdr_i_other_absoluteevaluationh)) /\ ((exists mdr_z_other_absoluteevaluationhscr. ((exists mdr_a_other_absoluteevaluationhscrc mdr_b_other_absoluteevaluationhscrc mdr_c_other_absoluteevaluationhscrc mdr_e_other_absoluteevaluationhscrc mdr_f_other_absoluteevaluationhscrc. ((mdr_a_other_absoluteevaluationhscrc = ((mdr_q_other_absoluteevaluationhs) + (mdr_up_other_absoluteevaluationhsc)) * S ((mdr_q_other_absoluteevaluationhs) + (mdr_up_other_absoluteevaluationhsc)) + ((mdr_up_other_absoluteevaluationhsc) + (mdr_up_other_absoluteevaluationhsc))) /\ ((mdr_b_other_absoluteevaluationhscrc = ((mdr_us_other_absoluteevaluationhsc) + (mdr_un_other_absoluteevaluationhsc)) * S ((mdr_us_other_absoluteevaluationhsc) + (mdr_un_other_absoluteevaluationhsc)) + ((mdr_un_other_absoluteevaluationhsc) + (mdr_un_other_absoluteevaluationhsc))) /\ ((mdr_c_other_absoluteevaluationhscrc = ((mdr_a_other_absoluteevaluationhscrc) + (mdr_b_other_absoluteevaluationhscrc)) * S ((mdr_a_other_absoluteevaluationhscrc) + (mdr_b_other_absoluteevaluationhscrc)) + ((mdr_b_other_absoluteevaluationhscrc) + (mdr_b_other_absoluteevaluationhscrc))) /\ ((mdr_e_other_absoluteevaluationhscrc = ((mdr_p_other_absoluteevaluationhsc) + (mdr_n_other_absoluteevaluationhsc)) * S ((mdr_p_other_absoluteevaluationhsc) + (mdr_n_other_absoluteevaluationhsc)) + ((mdr_n_other_absoluteevaluationhsc) + (mdr_n_other_absoluteevaluationhsc))) /\ ((mdr_f_other_absoluteevaluationhscrc = ((mdr_ut_other_absoluteevaluationhsc) + (mdr_e_other_absoluteevaluationhscrc)) * S ((mdr_ut_other_absoluteevaluationhsc) + (mdr_e_other_absoluteevaluationhscrc)) + ((mdr_e_other_absoluteevaluationhscrc) + (mdr_e_other_absoluteevaluationhscrc))) /\ ((mdr_z_other_absoluteevaluationhscr) = ((mdr_c_other_absoluteevaluationhscrc) + (mdr_f_other_absoluteevaluationhscrc)) * S ((mdr_c_other_absoluteevaluationhscrc) + (mdr_f_other_absoluteevaluationhscrc)) + ((mdr_f_other_absoluteevaluationhscrc) + (mdr_f_other_absoluteevaluationhscrc))))))))) /\ (((exists ff_h_mdr_other_absoluteevaluationhscrb. ff_h_mdr_other_absoluteevaluationhscrb + S (mdr_z_other_absoluteevaluationhscr) = S ((S (mdr_i_other_absoluteevaluationhsc)) * mdr_c_other_absoluteevaluation)) /\ exists ff_q_mdr_other_absoluteevaluationhscrb. mdr_b_other_absoluteevaluation = ff_q_mdr_other_absoluteevaluationhscrb * S ((S (mdr_i_other_absoluteevaluationhsc)) * mdr_c_other_absoluteevaluation) + (mdr_z_other_absoluteevaluationhscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_other_absoluteevaluationhscm_positive. (exists ff_gap_mdm_lt_mdr_other_absoluteevaluationhscm_positive_index_bound. ff_gap_mdm_lt_mdr_other_absoluteevaluationhscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_other_absoluteevaluationhscm_positive) = ((mdr_q_other_absoluteevaluationhs) * (mdr_q_other_absoluteevaluationhs))) -> exists ff_row_mdm_prefix_mdr_other_absoluteevaluationhscm_positive ff_column_mdm_prefix_mdr_other_absoluteevaluationhscm_positive ff_value_mdm_prefix_mdr_other_absoluteevaluationhscm_positive. (ff_index_mdm_prefix_mdr_other_absoluteevaluationhscm_positive = (mdr_q_other_absoluteevaluationhs) * ff_row_mdm_prefix_mdr_other_absoluteevaluationhscm_positive + ff_column_mdm_prefix_mdr_other_absoluteevaluationhscm_positive /\ ((exists ff_gap_mdm_lt_mdr_other_absoluteevaluationhscm_positive_column_bound. ff_gap_mdm_lt_mdr_other_absoluteevaluationhscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_other_absoluteevaluationhscm_positive) = (mdr_q_other_absoluteevaluationhs)) /\ ((exists ff_row_mdm_cell_mdr_other_absoluteevaluationhscm_positive_cell ff_column_mdm_cell_mdr_other_absoluteevaluationhscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_other_absoluteevaluationhscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_other_absoluteevaluationhscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_other_absoluteevaluationhscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_other_absoluteevaluationhscm_positive_cell = ff_row_mdm_prefix_mdr_other_absoluteevaluationhscm_positive) \/ ((exists ff_gap_mdm_le_mdr_other_absoluteevaluationhscm_positive_cell_row_after. ff_gap_mdm_le_mdr_other_absoluteevaluationhscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_other_absoluteevaluationhscm_positive)) /\ ff_row_mdm_cell_mdr_other_absoluteevaluationhscm_positive_cell = S ff_row_mdm_prefix_mdr_other_absoluteevaluationhscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_other_absoluteevaluationhscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_other_absoluteevaluationhscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_other_absoluteevaluationhscm_positive) = (mdr_j_other_absoluteevaluationhsc)) /\ ff_column_mdm_cell_mdr_other_absoluteevaluationhscm_positive_cell = ff_column_mdm_prefix_mdr_other_absoluteevaluationhscm_positive) \/ ((exists ff_gap_mdm_le_mdr_other_absoluteevaluationhscm_positive_cell_column_after. ff_gap_mdm_le_mdr_other_absoluteevaluationhscm_positive_cell_column_after + (mdr_j_other_absoluteevaluationhsc) = (ff_column_mdm_prefix_mdr_other_absoluteevaluationhscm_positive)) /\ ff_column_mdm_cell_mdr_other_absoluteevaluationhscm_positive_cell = S ff_column_mdm_prefix_mdr_other_absoluteevaluationhscm_positive))) /\ (((exists ff_h_mdm_mdr_other_absoluteevaluationhscm_positive_cell_source. ff_h_mdm_mdr_other_absoluteevaluationhscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_other_absoluteevaluationhscm_positive) = S ((S ((ff_row_mdm_cell_mdr_other_absoluteevaluationhscm_positive_cell) * (S (mdr_q_other_absoluteevaluationhs)) + (ff_column_mdm_cell_mdr_other_absoluteevaluationhscm_positive_cell))) * mdr_pc_other_absoluteevaluationh)) /\ exists ff_q_mdm_mdr_other_absoluteevaluationhscm_positive_cell_source. mdr_pb_other_absoluteevaluationh = ff_q_mdm_mdr_other_absoluteevaluationhscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_other_absoluteevaluationhscm_positive_cell) * (S (mdr_q_other_absoluteevaluationhs)) + (ff_column_mdm_cell_mdr_other_absoluteevaluationhscm_positive_cell))) * mdr_pc_other_absoluteevaluationh) + (ff_value_mdm_prefix_mdr_other_absoluteevaluationhscm_positive)))))) /\ (((exists ff_h_mdm_mdr_other_absoluteevaluationhscm_positive_target. ff_h_mdm_mdr_other_absoluteevaluationhscm_positive_target + S (ff_value_mdm_prefix_mdr_other_absoluteevaluationhscm_positive) = S ((S (ff_index_mdm_prefix_mdr_other_absoluteevaluationhscm_positive)) * mdr_us_other_absoluteevaluationhsc)) /\ exists ff_q_mdm_mdr_other_absoluteevaluationhscm_positive_target. mdr_up_other_absoluteevaluationhsc = ff_q_mdm_mdr_other_absoluteevaluationhscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_other_absoluteevaluationhscm_positive)) * mdr_us_other_absoluteevaluationhsc) + (ff_value_mdm_prefix_mdr_other_absoluteevaluationhscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_other_absoluteevaluationhscm_negative. (exists ff_gap_mdm_lt_mdr_other_absoluteevaluationhscm_negative_index_bound. ff_gap_mdm_lt_mdr_other_absoluteevaluationhscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_other_absoluteevaluationhscm_negative) = ((mdr_q_other_absoluteevaluationhs) * (mdr_q_other_absoluteevaluationhs))) -> exists ff_row_mdm_prefix_mdr_other_absoluteevaluationhscm_negative ff_column_mdm_prefix_mdr_other_absoluteevaluationhscm_negative ff_value_mdm_prefix_mdr_other_absoluteevaluationhscm_negative. (ff_index_mdm_prefix_mdr_other_absoluteevaluationhscm_negative = (mdr_q_other_absoluteevaluationhs) * ff_row_mdm_prefix_mdr_other_absoluteevaluationhscm_negative + ff_column_mdm_prefix_mdr_other_absoluteevaluationhscm_negative /\ ((exists ff_gap_mdm_lt_mdr_other_absoluteevaluationhscm_negative_column_bound. ff_gap_mdm_lt_mdr_other_absoluteevaluationhscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_other_absoluteevaluationhscm_negative) = (mdr_q_other_absoluteevaluationhs)) /\ ((exists ff_row_mdm_cell_mdr_other_absoluteevaluationhscm_negative_cell ff_column_mdm_cell_mdr_other_absoluteevaluationhscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_other_absoluteevaluationhscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_other_absoluteevaluationhscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_other_absoluteevaluationhscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_other_absoluteevaluationhscm_negative_cell = ff_row_mdm_prefix_mdr_other_absoluteevaluationhscm_negative) \/ ((exists ff_gap_mdm_le_mdr_other_absoluteevaluationhscm_negative_cell_row_after. ff_gap_mdm_le_mdr_other_absoluteevaluationhscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_other_absoluteevaluationhscm_negative)) /\ ff_row_mdm_cell_mdr_other_absoluteevaluationhscm_negative_cell = S ff_row_mdm_prefix_mdr_other_absoluteevaluationhscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_other_absoluteevaluationhscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_other_absoluteevaluationhscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_other_absoluteevaluationhscm_negative) = (mdr_j_other_absoluteevaluationhsc)) /\ ff_column_mdm_cell_mdr_other_absoluteevaluationhscm_negative_cell = ff_column_mdm_prefix_mdr_other_absoluteevaluationhscm_negative) \/ ((exists ff_gap_mdm_le_mdr_other_absoluteevaluationhscm_negative_cell_column_after. ff_gap_mdm_le_mdr_other_absoluteevaluationhscm_negative_cell_column_after + (mdr_j_other_absoluteevaluationhsc) = (ff_column_mdm_prefix_mdr_other_absoluteevaluationhscm_negative)) /\ ff_column_mdm_cell_mdr_other_absoluteevaluationhscm_negative_cell = S ff_column_mdm_prefix_mdr_other_absoluteevaluationhscm_negative))) /\ (((exists ff_h_mdm_mdr_other_absoluteevaluationhscm_negative_cell_source. ff_h_mdm_mdr_other_absoluteevaluationhscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_other_absoluteevaluationhscm_negative) = S ((S ((ff_row_mdm_cell_mdr_other_absoluteevaluationhscm_negative_cell) * (S (mdr_q_other_absoluteevaluationhs)) + (ff_column_mdm_cell_mdr_other_absoluteevaluationhscm_negative_cell))) * mdr_nc_other_absoluteevaluationh)) /\ exists ff_q_mdm_mdr_other_absoluteevaluationhscm_negative_cell_source. mdr_nb_other_absoluteevaluationh = ff_q_mdm_mdr_other_absoluteevaluationhscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_other_absoluteevaluationhscm_negative_cell) * (S (mdr_q_other_absoluteevaluationhs)) + (ff_column_mdm_cell_mdr_other_absoluteevaluationhscm_negative_cell))) * mdr_nc_other_absoluteevaluationh) + (ff_value_mdm_prefix_mdr_other_absoluteevaluationhscm_negative)))))) /\ (((exists ff_h_mdm_mdr_other_absoluteevaluationhscm_negative_target. ff_h_mdm_mdr_other_absoluteevaluationhscm_negative_target + S (ff_value_mdm_prefix_mdr_other_absoluteevaluationhscm_negative) = S ((S (ff_index_mdm_prefix_mdr_other_absoluteevaluationhscm_negative)) * mdr_ut_other_absoluteevaluationhsc)) /\ exists ff_q_mdm_mdr_other_absoluteevaluationhscm_negative_target. mdr_un_other_absoluteevaluationhsc = ff_q_mdm_mdr_other_absoluteevaluationhscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_other_absoluteevaluationhscm_negative)) * mdr_ut_other_absoluteevaluationhsc) + (ff_value_mdm_prefix_mdr_other_absoluteevaluationhscm_negative))))))))) /\ ((((exists ff_h_mdr_other_absoluteevaluationhscp. ff_h_mdr_other_absoluteevaluationhscp + S (mdr_p_other_absoluteevaluationhsc) = S ((S (mdr_j_other_absoluteevaluationhsc)) * mdr_ec_other_absoluteevaluationhs)) /\ exists ff_q_mdr_other_absoluteevaluationhscp. mdr_eb_other_absoluteevaluationhs = ff_q_mdr_other_absoluteevaluationhscp * S ((S (mdr_j_other_absoluteevaluationhsc)) * mdr_ec_other_absoluteevaluationhs) + (mdr_p_other_absoluteevaluationhsc))) /\ (((exists ff_h_mdr_other_absoluteevaluationhscn. ff_h_mdr_other_absoluteevaluationhscn + S (mdr_n_other_absoluteevaluationhsc) = S ((S (mdr_j_other_absoluteevaluationhsc)) * mdr_fc_other_absoluteevaluationhs)) /\ exists ff_q_mdr_other_absoluteevaluationhscn. mdr_fb_other_absoluteevaluationhs = ff_q_mdr_other_absoluteevaluationhscn * S ((S (mdr_j_other_absoluteevaluationhsc)) * mdr_fc_other_absoluteevaluationhs) + (mdr_n_other_absoluteevaluationhsc)))))))) /\ (exists ff_ub_mce_fold_mdr_other_absoluteevaluationhsf ff_uc_mce_fold_mdr_other_absoluteevaluationhsf ff_vb_mce_fold_mdr_other_absoluteevaluationhsf ff_vc_mce_fold_mdr_other_absoluteevaluationhsf. ((forall ff_index_mce_alternating_mdr_other_absoluteevaluationhsf_prefix. (exists ff_gap_mce_mdr_other_absoluteevaluationhsf_prefix_index. ff_gap_mce_mdr_other_absoluteevaluationhsf_prefix_index + S (ff_index_mce_alternating_mdr_other_absoluteevaluationhsf_prefix) = (S (mdr_q_other_absoluteevaluationhs))) -> exists ff_ap_mce_alternating_mdr_other_absoluteevaluationhsf_prefix ff_an_mce_alternating_mdr_other_absoluteevaluationhsf_prefix ff_bp_mce_alternating_mdr_other_absoluteevaluationhsf_prefix ff_bn_mce_alternating_mdr_other_absoluteevaluationhsf_prefix ff_p_mce_alternating_mdr_other_absoluteevaluationhsf_prefix ff_n_mce_alternating_mdr_other_absoluteevaluationhsf_prefix. ((((exists ff_h_mce_mdr_other_absoluteevaluationhsf_prefix_ap. ff_h_mce_mdr_other_absoluteevaluationhsf_prefix_ap + S (ff_ap_mce_alternating_mdr_other_absoluteevaluationhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_other_absoluteevaluationhsf_prefix)) * mdr_pc_other_absoluteevaluationh)) /\ exists ff_q_mce_mdr_other_absoluteevaluationhsf_prefix_ap. mdr_pb_other_absoluteevaluationh = ff_q_mce_mdr_other_absoluteevaluationhsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_other_absoluteevaluationhsf_prefix)) * mdr_pc_other_absoluteevaluationh) + (ff_ap_mce_alternating_mdr_other_absoluteevaluationhsf_prefix))) /\ ((((exists ff_h_mce_mdr_other_absoluteevaluationhsf_prefix_an. ff_h_mce_mdr_other_absoluteevaluationhsf_prefix_an + S (ff_an_mce_alternating_mdr_other_absoluteevaluationhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_other_absoluteevaluationhsf_prefix)) * mdr_nc_other_absoluteevaluationh)) /\ exists ff_q_mce_mdr_other_absoluteevaluationhsf_prefix_an. mdr_nb_other_absoluteevaluationh = ff_q_mce_mdr_other_absoluteevaluationhsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_other_absoluteevaluationhsf_prefix)) * mdr_nc_other_absoluteevaluationh) + (ff_an_mce_alternating_mdr_other_absoluteevaluationhsf_prefix))) /\ ((((exists ff_h_mce_mdr_other_absoluteevaluationhsf_prefix_bp. ff_h_mce_mdr_other_absoluteevaluationhsf_prefix_bp + S (ff_bp_mce_alternating_mdr_other_absoluteevaluationhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_other_absoluteevaluationhsf_prefix)) * mdr_ec_other_absoluteevaluationhs)) /\ exists ff_q_mce_mdr_other_absoluteevaluationhsf_prefix_bp. mdr_eb_other_absoluteevaluationhs = ff_q_mce_mdr_other_absoluteevaluationhsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_other_absoluteevaluationhsf_prefix)) * mdr_ec_other_absoluteevaluationhs) + (ff_bp_mce_alternating_mdr_other_absoluteevaluationhsf_prefix))) /\ ((((exists ff_h_mce_mdr_other_absoluteevaluationhsf_prefix_bn. ff_h_mce_mdr_other_absoluteevaluationhsf_prefix_bn + S (ff_bn_mce_alternating_mdr_other_absoluteevaluationhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_other_absoluteevaluationhsf_prefix)) * mdr_fc_other_absoluteevaluationhs)) /\ exists ff_q_mce_mdr_other_absoluteevaluationhsf_prefix_bn. mdr_fb_other_absoluteevaluationhs = ff_q_mce_mdr_other_absoluteevaluationhsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_other_absoluteevaluationhsf_prefix)) * mdr_fc_other_absoluteevaluationhs) + (ff_bn_mce_alternating_mdr_other_absoluteevaluationhsf_prefix))) /\ ((((exists ff_h_mce_mdr_other_absoluteevaluationhsf_prefix_positive. ff_h_mce_mdr_other_absoluteevaluationhsf_prefix_positive + S (ff_p_mce_alternating_mdr_other_absoluteevaluationhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_other_absoluteevaluationhsf_prefix)) * ff_uc_mce_fold_mdr_other_absoluteevaluationhsf)) /\ exists ff_q_mce_mdr_other_absoluteevaluationhsf_prefix_positive. ff_ub_mce_fold_mdr_other_absoluteevaluationhsf = ff_q_mce_mdr_other_absoluteevaluationhsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_other_absoluteevaluationhsf_prefix)) * ff_uc_mce_fold_mdr_other_absoluteevaluationhsf) + (ff_p_mce_alternating_mdr_other_absoluteevaluationhsf_prefix))) /\ ((((exists ff_h_mce_mdr_other_absoluteevaluationhsf_prefix_negative. ff_h_mce_mdr_other_absoluteevaluationhsf_prefix_negative + S (ff_n_mce_alternating_mdr_other_absoluteevaluationhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_other_absoluteevaluationhsf_prefix)) * ff_vc_mce_fold_mdr_other_absoluteevaluationhsf)) /\ exists ff_q_mce_mdr_other_absoluteevaluationhsf_prefix_negative. ff_vb_mce_fold_mdr_other_absoluteevaluationhsf = ff_q_mce_mdr_other_absoluteevaluationhsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_other_absoluteevaluationhsf_prefix)) * ff_vc_mce_fold_mdr_other_absoluteevaluationhsf) + (ff_n_mce_alternating_mdr_other_absoluteevaluationhsf_prefix))) /\ (((exists ff_even_mce_term_mdr_other_absoluteevaluationhsf_prefix_term. ff_index_mce_alternating_mdr_other_absoluteevaluationhsf_prefix = 2 * ff_even_mce_term_mdr_other_absoluteevaluationhsf_prefix_term) /\ (ff_p_mce_alternating_mdr_other_absoluteevaluationhsf_prefix = (ff_ap_mce_alternating_mdr_other_absoluteevaluationhsf_prefix) * (ff_bp_mce_alternating_mdr_other_absoluteevaluationhsf_prefix) + (ff_an_mce_alternating_mdr_other_absoluteevaluationhsf_prefix) * (ff_bn_mce_alternating_mdr_other_absoluteevaluationhsf_prefix) /\ ff_n_mce_alternating_mdr_other_absoluteevaluationhsf_prefix = (ff_ap_mce_alternating_mdr_other_absoluteevaluationhsf_prefix) * (ff_bn_mce_alternating_mdr_other_absoluteevaluationhsf_prefix) + (ff_an_mce_alternating_mdr_other_absoluteevaluationhsf_prefix) * (ff_bp_mce_alternating_mdr_other_absoluteevaluationhsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_other_absoluteevaluationhsf_prefix_term. ff_index_mce_alternating_mdr_other_absoluteevaluationhsf_prefix = 2 * ff_odd_mce_term_mdr_other_absoluteevaluationhsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_other_absoluteevaluationhsf_prefix = (ff_ap_mce_alternating_mdr_other_absoluteevaluationhsf_prefix) * (ff_bn_mce_alternating_mdr_other_absoluteevaluationhsf_prefix) + (ff_an_mce_alternating_mdr_other_absoluteevaluationhsf_prefix) * (ff_bp_mce_alternating_mdr_other_absoluteevaluationhsf_prefix) /\ ff_n_mce_alternating_mdr_other_absoluteevaluationhsf_prefix = (ff_ap_mce_alternating_mdr_other_absoluteevaluationhsf_prefix) * (ff_bp_mce_alternating_mdr_other_absoluteevaluationhsf_prefix) + (ff_an_mce_alternating_mdr_other_absoluteevaluationhsf_prefix) * (ff_bn_mce_alternating_mdr_other_absoluteevaluationhsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_other_absoluteevaluationhsf_positive ff_v_mce_mdr_other_absoluteevaluationhsf_positive. ((((exists ff_h_mce_mdr_other_absoluteevaluationhsf_positive_start. ff_h_mce_mdr_other_absoluteevaluationhsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_other_absoluteevaluationhsf_positive)) /\ exists ff_q_mce_mdr_other_absoluteevaluationhsf_positive_start. ff_u_mce_mdr_other_absoluteevaluationhsf_positive = ff_q_mce_mdr_other_absoluteevaluationhsf_positive_start * S ((S (0)) * ff_v_mce_mdr_other_absoluteevaluationhsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_other_absoluteevaluationhsf_positive_terminal. ff_h_mce_mdr_other_absoluteevaluationhsf_positive_terminal + S (mdr_p_other_absoluteevaluationh) = S ((S ((S (mdr_q_other_absoluteevaluationhs)))) * ff_v_mce_mdr_other_absoluteevaluationhsf_positive)) /\ exists ff_q_mce_mdr_other_absoluteevaluationhsf_positive_terminal. ff_u_mce_mdr_other_absoluteevaluationhsf_positive = ff_q_mce_mdr_other_absoluteevaluationhsf_positive_terminal * S ((S ((S (mdr_q_other_absoluteevaluationhs)))) * ff_v_mce_mdr_other_absoluteevaluationhsf_positive) + (mdr_p_other_absoluteevaluationh))) /\ forall ff_i_mce_mdr_other_absoluteevaluationhsf_positive. (exists ff_lt_mce_mdr_other_absoluteevaluationhsf_positive_bound. ff_lt_mce_mdr_other_absoluteevaluationhsf_positive_bound + S ff_i_mce_mdr_other_absoluteevaluationhsf_positive = (S (mdr_q_other_absoluteevaluationhs))) -> exists ff_a_mce_mdr_other_absoluteevaluationhsf_positive ff_r_mce_mdr_other_absoluteevaluationhsf_positive ff_s_mce_mdr_other_absoluteevaluationhsf_positive. ((((exists ff_h_mce_mdr_other_absoluteevaluationhsf_positive_summand. ff_h_mce_mdr_other_absoluteevaluationhsf_positive_summand + S (ff_a_mce_mdr_other_absoluteevaluationhsf_positive) = S ((S (ff_i_mce_mdr_other_absoluteevaluationhsf_positive)) * ff_uc_mce_fold_mdr_other_absoluteevaluationhsf)) /\ exists ff_q_mce_mdr_other_absoluteevaluationhsf_positive_summand. ff_ub_mce_fold_mdr_other_absoluteevaluationhsf = ff_q_mce_mdr_other_absoluteevaluationhsf_positive_summand * S ((S (ff_i_mce_mdr_other_absoluteevaluationhsf_positive)) * ff_uc_mce_fold_mdr_other_absoluteevaluationhsf) + (ff_a_mce_mdr_other_absoluteevaluationhsf_positive))) /\ ((((exists ff_h_mce_mdr_other_absoluteevaluationhsf_positive_partial. ff_h_mce_mdr_other_absoluteevaluationhsf_positive_partial + S (ff_r_mce_mdr_other_absoluteevaluationhsf_positive) = S ((S (ff_i_mce_mdr_other_absoluteevaluationhsf_positive)) * ff_v_mce_mdr_other_absoluteevaluationhsf_positive)) /\ exists ff_q_mce_mdr_other_absoluteevaluationhsf_positive_partial. ff_u_mce_mdr_other_absoluteevaluationhsf_positive = ff_q_mce_mdr_other_absoluteevaluationhsf_positive_partial * S ((S (ff_i_mce_mdr_other_absoluteevaluationhsf_positive)) * ff_v_mce_mdr_other_absoluteevaluationhsf_positive) + (ff_r_mce_mdr_other_absoluteevaluationhsf_positive))) /\ ((((exists ff_h_mce_mdr_other_absoluteevaluationhsf_positive_successor. ff_h_mce_mdr_other_absoluteevaluationhsf_positive_successor + S (ff_s_mce_mdr_other_absoluteevaluationhsf_positive) = S ((S (S ff_i_mce_mdr_other_absoluteevaluationhsf_positive)) * ff_v_mce_mdr_other_absoluteevaluationhsf_positive)) /\ exists ff_q_mce_mdr_other_absoluteevaluationhsf_positive_successor. ff_u_mce_mdr_other_absoluteevaluationhsf_positive = ff_q_mce_mdr_other_absoluteevaluationhsf_positive_successor * S ((S (S ff_i_mce_mdr_other_absoluteevaluationhsf_positive)) * ff_v_mce_mdr_other_absoluteevaluationhsf_positive) + (ff_s_mce_mdr_other_absoluteevaluationhsf_positive))) /\ ff_s_mce_mdr_other_absoluteevaluationhsf_positive = ff_r_mce_mdr_other_absoluteevaluationhsf_positive + ff_a_mce_mdr_other_absoluteevaluationhsf_positive)))))) /\ (exists ff_u_mce_mdr_other_absoluteevaluationhsf_negative ff_v_mce_mdr_other_absoluteevaluationhsf_negative. ((((exists ff_h_mce_mdr_other_absoluteevaluationhsf_negative_start. ff_h_mce_mdr_other_absoluteevaluationhsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_other_absoluteevaluationhsf_negative)) /\ exists ff_q_mce_mdr_other_absoluteevaluationhsf_negative_start. ff_u_mce_mdr_other_absoluteevaluationhsf_negative = ff_q_mce_mdr_other_absoluteevaluationhsf_negative_start * S ((S (0)) * ff_v_mce_mdr_other_absoluteevaluationhsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_other_absoluteevaluationhsf_negative_terminal. ff_h_mce_mdr_other_absoluteevaluationhsf_negative_terminal + S (mdr_n_other_absoluteevaluationh) = S ((S ((S (mdr_q_other_absoluteevaluationhs)))) * ff_v_mce_mdr_other_absoluteevaluationhsf_negative)) /\ exists ff_q_mce_mdr_other_absoluteevaluationhsf_negative_terminal. ff_u_mce_mdr_other_absoluteevaluationhsf_negative = ff_q_mce_mdr_other_absoluteevaluationhsf_negative_terminal * S ((S ((S (mdr_q_other_absoluteevaluationhs)))) * ff_v_mce_mdr_other_absoluteevaluationhsf_negative) + (mdr_n_other_absoluteevaluationh))) /\ forall ff_i_mce_mdr_other_absoluteevaluationhsf_negative. (exists ff_lt_mce_mdr_other_absoluteevaluationhsf_negative_bound. ff_lt_mce_mdr_other_absoluteevaluationhsf_negative_bound + S ff_i_mce_mdr_other_absoluteevaluationhsf_negative = (S (mdr_q_other_absoluteevaluationhs))) -> exists ff_a_mce_mdr_other_absoluteevaluationhsf_negative ff_r_mce_mdr_other_absoluteevaluationhsf_negative ff_s_mce_mdr_other_absoluteevaluationhsf_negative. ((((exists ff_h_mce_mdr_other_absoluteevaluationhsf_negative_summand. ff_h_mce_mdr_other_absoluteevaluationhsf_negative_summand + S (ff_a_mce_mdr_other_absoluteevaluationhsf_negative) = S ((S (ff_i_mce_mdr_other_absoluteevaluationhsf_negative)) * ff_vc_mce_fold_mdr_other_absoluteevaluationhsf)) /\ exists ff_q_mce_mdr_other_absoluteevaluationhsf_negative_summand. ff_vb_mce_fold_mdr_other_absoluteevaluationhsf = ff_q_mce_mdr_other_absoluteevaluationhsf_negative_summand * S ((S (ff_i_mce_mdr_other_absoluteevaluationhsf_negative)) * ff_vc_mce_fold_mdr_other_absoluteevaluationhsf) + (ff_a_mce_mdr_other_absoluteevaluationhsf_negative))) /\ ((((exists ff_h_mce_mdr_other_absoluteevaluationhsf_negative_partial. ff_h_mce_mdr_other_absoluteevaluationhsf_negative_partial + S (ff_r_mce_mdr_other_absoluteevaluationhsf_negative) = S ((S (ff_i_mce_mdr_other_absoluteevaluationhsf_negative)) * ff_v_mce_mdr_other_absoluteevaluationhsf_negative)) /\ exists ff_q_mce_mdr_other_absoluteevaluationhsf_negative_partial. ff_u_mce_mdr_other_absoluteevaluationhsf_negative = ff_q_mce_mdr_other_absoluteevaluationhsf_negative_partial * S ((S (ff_i_mce_mdr_other_absoluteevaluationhsf_negative)) * ff_v_mce_mdr_other_absoluteevaluationhsf_negative) + (ff_r_mce_mdr_other_absoluteevaluationhsf_negative))) /\ ((((exists ff_h_mce_mdr_other_absoluteevaluationhsf_negative_successor. ff_h_mce_mdr_other_absoluteevaluationhsf_negative_successor + S (ff_s_mce_mdr_other_absoluteevaluationhsf_negative) = S ((S (S ff_i_mce_mdr_other_absoluteevaluationhsf_negative)) * ff_v_mce_mdr_other_absoluteevaluationhsf_negative)) /\ exists ff_q_mce_mdr_other_absoluteevaluationhsf_negative_successor. ff_u_mce_mdr_other_absoluteevaluationhsf_negative = ff_q_mce_mdr_other_absoluteevaluationhsf_negative_successor * S ((S (S ff_i_mce_mdr_other_absoluteevaluationhsf_negative)) * ff_v_mce_mdr_other_absoluteevaluationhsf_negative) + (ff_s_mce_mdr_other_absoluteevaluationhsf_negative))) /\ ff_s_mce_mdr_other_absoluteevaluationhsf_negative = ff_r_mce_mdr_other_absoluteevaluationhsf_negative + ff_a_mce_mdr_other_absoluteevaluationhsf_negative))))))))))))))) /\ ((exists mdr_gap_other_absoluteevaluationi. mdr_gap_other_absoluteevaluationi + S (mdr_i_other_absoluteevaluation) = (mdr_l_other_absoluteevaluation)) /\ (exists mdr_z_other_absoluteevaluationr. ((exists mdr_a_other_absoluteevaluationrc mdr_b_other_absoluteevaluationrc mdr_c_other_absoluteevaluationrc mdr_e_other_absoluteevaluationrc mdr_f_other_absoluteevaluationrc. ((mdr_a_other_absoluteevaluationrc = ((d) + (ab)) * S ((d) + (ab)) + ((ab) + (ab))) /\ ((mdr_b_other_absoluteevaluationrc = ((ac) + (bb)) * S ((ac) + (bb)) + ((bb) + (bb))) /\ ((mdr_c_other_absoluteevaluationrc = ((mdr_a_other_absoluteevaluationrc) + (mdr_b_other_absoluteevaluationrc)) * S ((mdr_a_other_absoluteevaluationrc) + (mdr_b_other_absoluteevaluationrc)) + ((mdr_b_other_absoluteevaluationrc) + (mdr_b_other_absoluteevaluationrc))) /\ ((mdr_e_other_absoluteevaluationrc = ((mdr_p_other_absolute) + (mdr_n_other_absolute)) * S ((mdr_p_other_absolute) + (mdr_n_other_absolute)) + ((mdr_n_other_absolute) + (mdr_n_other_absolute))) /\ ((mdr_f_other_absoluteevaluationrc = ((bc) + (mdr_e_other_absoluteevaluationrc)) * S ((bc) + (mdr_e_other_absoluteevaluationrc)) + ((mdr_e_other_absoluteevaluationrc) + (mdr_e_other_absoluteevaluationrc))) /\ ((mdr_z_other_absoluteevaluationr) = ((mdr_c_other_absoluteevaluationrc) + (mdr_f_other_absoluteevaluationrc)) * S ((mdr_c_other_absoluteevaluationrc) + (mdr_f_other_absoluteevaluationrc)) + ((mdr_f_other_absoluteevaluationrc) + (mdr_f_other_absoluteevaluationrc))))))))) /\ (((exists ff_h_mdr_other_absoluteevaluationrb. ff_h_mdr_other_absoluteevaluationrb + S (mdr_z_other_absoluteevaluationr) = S ((S (mdr_i_other_absoluteevaluation)) * mdr_c_other_absoluteevaluation)) /\ exists ff_q_mdr_other_absoluteevaluationrb. mdr_b_other_absoluteevaluation = ff_q_mdr_other_absoluteevaluationrb * S ((S (mdr_i_other_absoluteevaluation)) * mdr_c_other_absoluteevaluation) + (mdr_z_other_absoluteevaluationr)))))))) /\ (((mdr_p_other_absolute) = (mdr_n_other_absolute) + (E)) \/ ((mdr_n_other_absolute) = (mdr_p_other_absolute) + (E))))) -> E = D)))