absolute_recursive_determinant_functional

forall ab ac bb bc d D E. (exists mdr_p_absolute_first mdr_n_absolute_first. ((exists mdr_b_absolute_firstevaluation mdr_c_absolute_firstevaluation mdr_l_absolute_firstevaluation mdr_i_absolute_firstevaluation. ((forall mdr_i_absolute_firstevaluationh. (exists mdr_gap_absolute_firstevaluationhi. mdr_gap_absolute_firstevaluationhi + S (mdr_i_absolute_firstevaluationh) = (mdr_l_absolute_firstevaluation)) -> exists mdr_d_absolute_firstevaluationh mdr_pb_absolute_firstevaluationh mdr_pc_absolute_firstevaluationh mdr_nb_absolute_firstevaluationh mdr_nc_absolute_firstevaluationh mdr_p_absolute_firstevaluationh mdr_n_absolute_firstevaluationh. ((exists mdr_z_absolute_firstevaluationhr. ((exists mdr_a_absolute_firstevaluationhrc mdr_b_absolute_firstevaluationhrc mdr_c_absolute_firstevaluationhrc mdr_e_absolute_firstevaluationhrc mdr_f_absolute_firstevaluationhrc. ((mdr_a_absolute_firstevaluationhrc = ((mdr_d_absolute_firstevaluationh) + (mdr_pb_absolute_firstevaluationh)) * S ((mdr_d_absolute_firstevaluationh) + (mdr_pb_absolute_firstevaluationh)) + ((mdr_pb_absolute_firstevaluationh) + (mdr_pb_absolute_firstevaluationh))) /\ ((mdr_b_absolute_firstevaluationhrc = ((mdr_pc_absolute_firstevaluationh) + (mdr_nb_absolute_firstevaluationh)) * S ((mdr_pc_absolute_firstevaluationh) + (mdr_nb_absolute_firstevaluationh)) + ((mdr_nb_absolute_firstevaluationh) + (mdr_nb_absolute_firstevaluationh))) /\ ((mdr_c_absolute_firstevaluationhrc = ((mdr_a_absolute_firstevaluationhrc) + (mdr_b_absolute_firstevaluationhrc)) * S ((mdr_a_absolute_firstevaluationhrc) + (mdr_b_absolute_firstevaluationhrc)) + ((mdr_b_absolute_firstevaluationhrc) + (mdr_b_absolute_firstevaluationhrc))) /\ ((mdr_e_absolute_firstevaluationhrc = ((mdr_p_absolute_firstevaluationh) + (mdr_n_absolute_firstevaluationh)) * S ((mdr_p_absolute_firstevaluationh) + (mdr_n_absolute_firstevaluationh)) + ((mdr_n_absolute_firstevaluationh) + (mdr_n_absolute_firstevaluationh))) /\ ((mdr_f_absolute_firstevaluationhrc = ((mdr_nc_absolute_firstevaluationh) + (mdr_e_absolute_firstevaluationhrc)) * S ((mdr_nc_absolute_firstevaluationh) + (mdr_e_absolute_firstevaluationhrc)) + ((mdr_e_absolute_firstevaluationhrc) + (mdr_e_absolute_firstevaluationhrc))) /\ ((mdr_z_absolute_firstevaluationhr) = ((mdr_c_absolute_firstevaluationhrc) + (mdr_f_absolute_firstevaluationhrc)) * S ((mdr_c_absolute_firstevaluationhrc) + (mdr_f_absolute_firstevaluationhrc)) + ((mdr_f_absolute_firstevaluationhrc) + (mdr_f_absolute_firstevaluationhrc))))))))) /\ (((exists ff_h_mdr_absolute_firstevaluationhrb. ff_h_mdr_absolute_firstevaluationhrb + S (mdr_z_absolute_firstevaluationhr) = S ((S (mdr_i_absolute_firstevaluationh)) * mdr_c_absolute_firstevaluation)) /\ exists ff_q_mdr_absolute_firstevaluationhrb. mdr_b_absolute_firstevaluation = ff_q_mdr_absolute_firstevaluationhrb * S ((S (mdr_i_absolute_firstevaluationh)) * mdr_c_absolute_firstevaluation) + (mdr_z_absolute_firstevaluationhr))))) /\ (((((mdr_d_absolute_firstevaluationh) = 0) /\ (((mdr_p_absolute_firstevaluationh) = 1) /\ ((mdr_n_absolute_firstevaluationh) = 0))) \/ exists mdr_q_absolute_firstevaluationhs mdr_eb_absolute_firstevaluationhs mdr_ec_absolute_firstevaluationhs mdr_fb_absolute_firstevaluationhs mdr_fc_absolute_firstevaluationhs. (((mdr_d_absolute_firstevaluationh) = S (mdr_q_absolute_firstevaluationhs)) /\ ((forall mdr_j_absolute_firstevaluationhsc. (exists mdr_gap_absolute_firstevaluationhscj. mdr_gap_absolute_firstevaluationhscj + S (mdr_j_absolute_firstevaluationhsc) = (S (mdr_q_absolute_firstevaluationhs))) -> exists mdr_i_absolute_firstevaluationhsc mdr_up_absolute_firstevaluationhsc mdr_us_absolute_firstevaluationhsc mdr_un_absolute_firstevaluationhsc mdr_ut_absolute_firstevaluationhsc mdr_p_absolute_firstevaluationhsc mdr_n_absolute_firstevaluationhsc. ((exists mdr_gap_absolute_firstevaluationhsci. mdr_gap_absolute_firstevaluationhsci + S (mdr_i_absolute_firstevaluationhsc) = (mdr_i_absolute_firstevaluationh)) /\ ((exists mdr_z_absolute_firstevaluationhscr. ((exists mdr_a_absolute_firstevaluationhscrc mdr_b_absolute_firstevaluationhscrc mdr_c_absolute_firstevaluationhscrc mdr_e_absolute_firstevaluationhscrc mdr_f_absolute_firstevaluationhscrc. ((mdr_a_absolute_firstevaluationhscrc = ((mdr_q_absolute_firstevaluationhs) + (mdr_up_absolute_firstevaluationhsc)) * S ((mdr_q_absolute_firstevaluationhs) + (mdr_up_absolute_firstevaluationhsc)) + ((mdr_up_absolute_firstevaluationhsc) + (mdr_up_absolute_firstevaluationhsc))) /\ ((mdr_b_absolute_firstevaluationhscrc = ((mdr_us_absolute_firstevaluationhsc) + (mdr_un_absolute_firstevaluationhsc)) * S ((mdr_us_absolute_firstevaluationhsc) + (mdr_un_absolute_firstevaluationhsc)) + ((mdr_un_absolute_firstevaluationhsc) + (mdr_un_absolute_firstevaluationhsc))) /\ ((mdr_c_absolute_firstevaluationhscrc = ((mdr_a_absolute_firstevaluationhscrc) + (mdr_b_absolute_firstevaluationhscrc)) * S ((mdr_a_absolute_firstevaluationhscrc) + (mdr_b_absolute_firstevaluationhscrc)) + ((mdr_b_absolute_firstevaluationhscrc) + (mdr_b_absolute_firstevaluationhscrc))) /\ ((mdr_e_absolute_firstevaluationhscrc = ((mdr_p_absolute_firstevaluationhsc) + (mdr_n_absolute_firstevaluationhsc)) * S ((mdr_p_absolute_firstevaluationhsc) + (mdr_n_absolute_firstevaluationhsc)) + ((mdr_n_absolute_firstevaluationhsc) + (mdr_n_absolute_firstevaluationhsc))) /\ ((mdr_f_absolute_firstevaluationhscrc = ((mdr_ut_absolute_firstevaluationhsc) + (mdr_e_absolute_firstevaluationhscrc)) * S ((mdr_ut_absolute_firstevaluationhsc) + (mdr_e_absolute_firstevaluationhscrc)) + ((mdr_e_absolute_firstevaluationhscrc) + (mdr_e_absolute_firstevaluationhscrc))) /\ ((mdr_z_absolute_firstevaluationhscr) = ((mdr_c_absolute_firstevaluationhscrc) + (mdr_f_absolute_firstevaluationhscrc)) * S ((mdr_c_absolute_firstevaluationhscrc) + (mdr_f_absolute_firstevaluationhscrc)) + ((mdr_f_absolute_firstevaluationhscrc) + (mdr_f_absolute_firstevaluationhscrc))))))))) /\ (((exists ff_h_mdr_absolute_firstevaluationhscrb. ff_h_mdr_absolute_firstevaluationhscrb + S (mdr_z_absolute_firstevaluationhscr) = S ((S (mdr_i_absolute_firstevaluationhsc)) * mdr_c_absolute_firstevaluation)) /\ exists ff_q_mdr_absolute_firstevaluationhscrb. mdr_b_absolute_firstevaluation = ff_q_mdr_absolute_firstevaluationhscrb * S ((S (mdr_i_absolute_firstevaluationhsc)) * mdr_c_absolute_firstevaluation) + (mdr_z_absolute_firstevaluationhscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_absolute_firstevaluationhscm_positive. (exists ff_gap_mdm_lt_mdr_absolute_firstevaluationhscm_positive_index_bound. ff_gap_mdm_lt_mdr_absolute_firstevaluationhscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_absolute_firstevaluationhscm_positive) = ((mdr_q_absolute_firstevaluationhs) * (mdr_q_absolute_firstevaluationhs))) -> exists ff_row_mdm_prefix_mdr_absolute_firstevaluationhscm_positive ff_column_mdm_prefix_mdr_absolute_firstevaluationhscm_positive ff_value_mdm_prefix_mdr_absolute_firstevaluationhscm_positive. (ff_index_mdm_prefix_mdr_absolute_firstevaluationhscm_positive = (mdr_q_absolute_firstevaluationhs) * ff_row_mdm_prefix_mdr_absolute_firstevaluationhscm_positive + ff_column_mdm_prefix_mdr_absolute_firstevaluationhscm_positive /\ ((exists ff_gap_mdm_lt_mdr_absolute_firstevaluationhscm_positive_column_bound. ff_gap_mdm_lt_mdr_absolute_firstevaluationhscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_absolute_firstevaluationhscm_positive) = (mdr_q_absolute_firstevaluationhs)) /\ ((exists ff_row_mdm_cell_mdr_absolute_firstevaluationhscm_positive_cell ff_column_mdm_cell_mdr_absolute_firstevaluationhscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_absolute_firstevaluationhscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_absolute_firstevaluationhscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_absolute_firstevaluationhscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_absolute_firstevaluationhscm_positive_cell = ff_row_mdm_prefix_mdr_absolute_firstevaluationhscm_positive) \/ ((exists ff_gap_mdm_le_mdr_absolute_firstevaluationhscm_positive_cell_row_after. ff_gap_mdm_le_mdr_absolute_firstevaluationhscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_absolute_firstevaluationhscm_positive)) /\ ff_row_mdm_cell_mdr_absolute_firstevaluationhscm_positive_cell = S ff_row_mdm_prefix_mdr_absolute_firstevaluationhscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_absolute_firstevaluationhscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_absolute_firstevaluationhscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_absolute_firstevaluationhscm_positive) = (mdr_j_absolute_firstevaluationhsc)) /\ ff_column_mdm_cell_mdr_absolute_firstevaluationhscm_positive_cell = ff_column_mdm_prefix_mdr_absolute_firstevaluationhscm_positive) \/ ((exists ff_gap_mdm_le_mdr_absolute_firstevaluationhscm_positive_cell_column_after. ff_gap_mdm_le_mdr_absolute_firstevaluationhscm_positive_cell_column_after + (mdr_j_absolute_firstevaluationhsc) = (ff_column_mdm_prefix_mdr_absolute_firstevaluationhscm_positive)) /\ ff_column_mdm_cell_mdr_absolute_firstevaluationhscm_positive_cell = S ff_column_mdm_prefix_mdr_absolute_firstevaluationhscm_positive))) /\ (((exists ff_h_mdm_mdr_absolute_firstevaluationhscm_positive_cell_source. ff_h_mdm_mdr_absolute_firstevaluationhscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_absolute_firstevaluationhscm_positive) = S ((S ((ff_row_mdm_cell_mdr_absolute_firstevaluationhscm_positive_cell) * (S (mdr_q_absolute_firstevaluationhs)) + (ff_column_mdm_cell_mdr_absolute_firstevaluationhscm_positive_cell))) * mdr_pc_absolute_firstevaluationh)) /\ exists ff_q_mdm_mdr_absolute_firstevaluationhscm_positive_cell_source. mdr_pb_absolute_firstevaluationh = ff_q_mdm_mdr_absolute_firstevaluationhscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_absolute_firstevaluationhscm_positive_cell) * (S (mdr_q_absolute_firstevaluationhs)) + (ff_column_mdm_cell_mdr_absolute_firstevaluationhscm_positive_cell))) * mdr_pc_absolute_firstevaluationh) + (ff_value_mdm_prefix_mdr_absolute_firstevaluationhscm_positive)))))) /\ (((exists ff_h_mdm_mdr_absolute_firstevaluationhscm_positive_target. ff_h_mdm_mdr_absolute_firstevaluationhscm_positive_target + S (ff_value_mdm_prefix_mdr_absolute_firstevaluationhscm_positive) = S ((S (ff_index_mdm_prefix_mdr_absolute_firstevaluationhscm_positive)) * mdr_us_absolute_firstevaluationhsc)) /\ exists ff_q_mdm_mdr_absolute_firstevaluationhscm_positive_target. mdr_up_absolute_firstevaluationhsc = ff_q_mdm_mdr_absolute_firstevaluationhscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_absolute_firstevaluationhscm_positive)) * mdr_us_absolute_firstevaluationhsc) + (ff_value_mdm_prefix_mdr_absolute_firstevaluationhscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_absolute_firstevaluationhscm_negative. (exists ff_gap_mdm_lt_mdr_absolute_firstevaluationhscm_negative_index_bound. ff_gap_mdm_lt_mdr_absolute_firstevaluationhscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_absolute_firstevaluationhscm_negative) = ((mdr_q_absolute_firstevaluationhs) * (mdr_q_absolute_firstevaluationhs))) -> exists ff_row_mdm_prefix_mdr_absolute_firstevaluationhscm_negative ff_column_mdm_prefix_mdr_absolute_firstevaluationhscm_negative ff_value_mdm_prefix_mdr_absolute_firstevaluationhscm_negative. (ff_index_mdm_prefix_mdr_absolute_firstevaluationhscm_negative = (mdr_q_absolute_firstevaluationhs) * ff_row_mdm_prefix_mdr_absolute_firstevaluationhscm_negative + ff_column_mdm_prefix_mdr_absolute_firstevaluationhscm_negative /\ ((exists ff_gap_mdm_lt_mdr_absolute_firstevaluationhscm_negative_column_bound. ff_gap_mdm_lt_mdr_absolute_firstevaluationhscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_absolute_firstevaluationhscm_negative) = (mdr_q_absolute_firstevaluationhs)) /\ ((exists ff_row_mdm_cell_mdr_absolute_firstevaluationhscm_negative_cell ff_column_mdm_cell_mdr_absolute_firstevaluationhscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_absolute_firstevaluationhscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_absolute_firstevaluationhscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_absolute_firstevaluationhscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_absolute_firstevaluationhscm_negative_cell = ff_row_mdm_prefix_mdr_absolute_firstevaluationhscm_negative) \/ ((exists ff_gap_mdm_le_mdr_absolute_firstevaluationhscm_negative_cell_row_after. ff_gap_mdm_le_mdr_absolute_firstevaluationhscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_absolute_firstevaluationhscm_negative)) /\ ff_row_mdm_cell_mdr_absolute_firstevaluationhscm_negative_cell = S ff_row_mdm_prefix_mdr_absolute_firstevaluationhscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_absolute_firstevaluationhscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_absolute_firstevaluationhscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_absolute_firstevaluationhscm_negative) = (mdr_j_absolute_firstevaluationhsc)) /\ ff_column_mdm_cell_mdr_absolute_firstevaluationhscm_negative_cell = ff_column_mdm_prefix_mdr_absolute_firstevaluationhscm_negative) \/ ((exists ff_gap_mdm_le_mdr_absolute_firstevaluationhscm_negative_cell_column_after. ff_gap_mdm_le_mdr_absolute_firstevaluationhscm_negative_cell_column_after + (mdr_j_absolute_firstevaluationhsc) = (ff_column_mdm_prefix_mdr_absolute_firstevaluationhscm_negative)) /\ ff_column_mdm_cell_mdr_absolute_firstevaluationhscm_negative_cell = S ff_column_mdm_prefix_mdr_absolute_firstevaluationhscm_negative))) /\ (((exists ff_h_mdm_mdr_absolute_firstevaluationhscm_negative_cell_source. ff_h_mdm_mdr_absolute_firstevaluationhscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_absolute_firstevaluationhscm_negative) = S ((S ((ff_row_mdm_cell_mdr_absolute_firstevaluationhscm_negative_cell) * (S (mdr_q_absolute_firstevaluationhs)) + (ff_column_mdm_cell_mdr_absolute_firstevaluationhscm_negative_cell))) * mdr_nc_absolute_firstevaluationh)) /\ exists ff_q_mdm_mdr_absolute_firstevaluationhscm_negative_cell_source. mdr_nb_absolute_firstevaluationh = ff_q_mdm_mdr_absolute_firstevaluationhscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_absolute_firstevaluationhscm_negative_cell) * (S (mdr_q_absolute_firstevaluationhs)) + (ff_column_mdm_cell_mdr_absolute_firstevaluationhscm_negative_cell))) * mdr_nc_absolute_firstevaluationh) + (ff_value_mdm_prefix_mdr_absolute_firstevaluationhscm_negative)))))) /\ (((exists ff_h_mdm_mdr_absolute_firstevaluationhscm_negative_target. ff_h_mdm_mdr_absolute_firstevaluationhscm_negative_target + S (ff_value_mdm_prefix_mdr_absolute_firstevaluationhscm_negative) = S ((S (ff_index_mdm_prefix_mdr_absolute_firstevaluationhscm_negative)) * mdr_ut_absolute_firstevaluationhsc)) /\ exists ff_q_mdm_mdr_absolute_firstevaluationhscm_negative_target. mdr_un_absolute_firstevaluationhsc = ff_q_mdm_mdr_absolute_firstevaluationhscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_absolute_firstevaluationhscm_negative)) * mdr_ut_absolute_firstevaluationhsc) + (ff_value_mdm_prefix_mdr_absolute_firstevaluationhscm_negative))))))))) /\ ((((exists ff_h_mdr_absolute_firstevaluationhscp. ff_h_mdr_absolute_firstevaluationhscp + S (mdr_p_absolute_firstevaluationhsc) = S ((S (mdr_j_absolute_firstevaluationhsc)) * mdr_ec_absolute_firstevaluationhs)) /\ exists ff_q_mdr_absolute_firstevaluationhscp. mdr_eb_absolute_firstevaluationhs = ff_q_mdr_absolute_firstevaluationhscp * S ((S (mdr_j_absolute_firstevaluationhsc)) * mdr_ec_absolute_firstevaluationhs) + (mdr_p_absolute_firstevaluationhsc))) /\ (((exists ff_h_mdr_absolute_firstevaluationhscn. ff_h_mdr_absolute_firstevaluationhscn + S (mdr_n_absolute_firstevaluationhsc) = S ((S (mdr_j_absolute_firstevaluationhsc)) * mdr_fc_absolute_firstevaluationhs)) /\ exists ff_q_mdr_absolute_firstevaluationhscn. mdr_fb_absolute_firstevaluationhs = ff_q_mdr_absolute_firstevaluationhscn * S ((S (mdr_j_absolute_firstevaluationhsc)) * mdr_fc_absolute_firstevaluationhs) + (mdr_n_absolute_firstevaluationhsc)))))))) /\ (exists ff_ub_mce_fold_mdr_absolute_firstevaluationhsf ff_uc_mce_fold_mdr_absolute_firstevaluationhsf ff_vb_mce_fold_mdr_absolute_firstevaluationhsf ff_vc_mce_fold_mdr_absolute_firstevaluationhsf. ((forall ff_index_mce_alternating_mdr_absolute_firstevaluationhsf_prefix. (exists ff_gap_mce_mdr_absolute_firstevaluationhsf_prefix_index. ff_gap_mce_mdr_absolute_firstevaluationhsf_prefix_index + S (ff_index_mce_alternating_mdr_absolute_firstevaluationhsf_prefix) = (S (mdr_q_absolute_firstevaluationhs))) -> exists ff_ap_mce_alternating_mdr_absolute_firstevaluationhsf_prefix ff_an_mce_alternating_mdr_absolute_firstevaluationhsf_prefix ff_bp_mce_alternating_mdr_absolute_firstevaluationhsf_prefix ff_bn_mce_alternating_mdr_absolute_firstevaluationhsf_prefix ff_p_mce_alternating_mdr_absolute_firstevaluationhsf_prefix ff_n_mce_alternating_mdr_absolute_firstevaluationhsf_prefix. ((((exists ff_h_mce_mdr_absolute_firstevaluationhsf_prefix_ap. ff_h_mce_mdr_absolute_firstevaluationhsf_prefix_ap + S (ff_ap_mce_alternating_mdr_absolute_firstevaluationhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_absolute_firstevaluationhsf_prefix)) * mdr_pc_absolute_firstevaluationh)) /\ exists ff_q_mce_mdr_absolute_firstevaluationhsf_prefix_ap. mdr_pb_absolute_firstevaluationh = ff_q_mce_mdr_absolute_firstevaluationhsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_absolute_firstevaluationhsf_prefix)) * mdr_pc_absolute_firstevaluationh) + (ff_ap_mce_alternating_mdr_absolute_firstevaluationhsf_prefix))) /\ ((((exists ff_h_mce_mdr_absolute_firstevaluationhsf_prefix_an. ff_h_mce_mdr_absolute_firstevaluationhsf_prefix_an + S (ff_an_mce_alternating_mdr_absolute_firstevaluationhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_absolute_firstevaluationhsf_prefix)) * mdr_nc_absolute_firstevaluationh)) /\ exists ff_q_mce_mdr_absolute_firstevaluationhsf_prefix_an. mdr_nb_absolute_firstevaluationh = ff_q_mce_mdr_absolute_firstevaluationhsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_absolute_firstevaluationhsf_prefix)) * mdr_nc_absolute_firstevaluationh) + (ff_an_mce_alternating_mdr_absolute_firstevaluationhsf_prefix))) /\ ((((exists ff_h_mce_mdr_absolute_firstevaluationhsf_prefix_bp. ff_h_mce_mdr_absolute_firstevaluationhsf_prefix_bp + S (ff_bp_mce_alternating_mdr_absolute_firstevaluationhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_absolute_firstevaluationhsf_prefix)) * mdr_ec_absolute_firstevaluationhs)) /\ exists ff_q_mce_mdr_absolute_firstevaluationhsf_prefix_bp. mdr_eb_absolute_firstevaluationhs = ff_q_mce_mdr_absolute_firstevaluationhsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_absolute_firstevaluationhsf_prefix)) * mdr_ec_absolute_firstevaluationhs) + (ff_bp_mce_alternating_mdr_absolute_firstevaluationhsf_prefix))) /\ ((((exists ff_h_mce_mdr_absolute_firstevaluationhsf_prefix_bn. ff_h_mce_mdr_absolute_firstevaluationhsf_prefix_bn + S (ff_bn_mce_alternating_mdr_absolute_firstevaluationhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_absolute_firstevaluationhsf_prefix)) * mdr_fc_absolute_firstevaluationhs)) /\ exists ff_q_mce_mdr_absolute_firstevaluationhsf_prefix_bn. mdr_fb_absolute_firstevaluationhs = ff_q_mce_mdr_absolute_firstevaluationhsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_absolute_firstevaluationhsf_prefix)) * mdr_fc_absolute_firstevaluationhs) + (ff_bn_mce_alternating_mdr_absolute_firstevaluationhsf_prefix))) /\ ((((exists ff_h_mce_mdr_absolute_firstevaluationhsf_prefix_positive. ff_h_mce_mdr_absolute_firstevaluationhsf_prefix_positive + S (ff_p_mce_alternating_mdr_absolute_firstevaluationhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_absolute_firstevaluationhsf_prefix)) * ff_uc_mce_fold_mdr_absolute_firstevaluationhsf)) /\ exists ff_q_mce_mdr_absolute_firstevaluationhsf_prefix_positive. ff_ub_mce_fold_mdr_absolute_firstevaluationhsf = ff_q_mce_mdr_absolute_firstevaluationhsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_absolute_firstevaluationhsf_prefix)) * ff_uc_mce_fold_mdr_absolute_firstevaluationhsf) + (ff_p_mce_alternating_mdr_absolute_firstevaluationhsf_prefix))) /\ ((((exists ff_h_mce_mdr_absolute_firstevaluationhsf_prefix_negative. ff_h_mce_mdr_absolute_firstevaluationhsf_prefix_negative + S (ff_n_mce_alternating_mdr_absolute_firstevaluationhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_absolute_firstevaluationhsf_prefix)) * ff_vc_mce_fold_mdr_absolute_firstevaluationhsf)) /\ exists ff_q_mce_mdr_absolute_firstevaluationhsf_prefix_negative. ff_vb_mce_fold_mdr_absolute_firstevaluationhsf = ff_q_mce_mdr_absolute_firstevaluationhsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_absolute_firstevaluationhsf_prefix)) * ff_vc_mce_fold_mdr_absolute_firstevaluationhsf) + (ff_n_mce_alternating_mdr_absolute_firstevaluationhsf_prefix))) /\ (((exists ff_even_mce_term_mdr_absolute_firstevaluationhsf_prefix_term. ff_index_mce_alternating_mdr_absolute_firstevaluationhsf_prefix = 2 * ff_even_mce_term_mdr_absolute_firstevaluationhsf_prefix_term) /\ (ff_p_mce_alternating_mdr_absolute_firstevaluationhsf_prefix = (ff_ap_mce_alternating_mdr_absolute_firstevaluationhsf_prefix) * (ff_bp_mce_alternating_mdr_absolute_firstevaluationhsf_prefix) + (ff_an_mce_alternating_mdr_absolute_firstevaluationhsf_prefix) * (ff_bn_mce_alternating_mdr_absolute_firstevaluationhsf_prefix) /\ ff_n_mce_alternating_mdr_absolute_firstevaluationhsf_prefix = (ff_ap_mce_alternating_mdr_absolute_firstevaluationhsf_prefix) * (ff_bn_mce_alternating_mdr_absolute_firstevaluationhsf_prefix) + (ff_an_mce_alternating_mdr_absolute_firstevaluationhsf_prefix) * (ff_bp_mce_alternating_mdr_absolute_firstevaluationhsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_absolute_firstevaluationhsf_prefix_term. ff_index_mce_alternating_mdr_absolute_firstevaluationhsf_prefix = 2 * ff_odd_mce_term_mdr_absolute_firstevaluationhsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_absolute_firstevaluationhsf_prefix = (ff_ap_mce_alternating_mdr_absolute_firstevaluationhsf_prefix) * (ff_bn_mce_alternating_mdr_absolute_firstevaluationhsf_prefix) + (ff_an_mce_alternating_mdr_absolute_firstevaluationhsf_prefix) * (ff_bp_mce_alternating_mdr_absolute_firstevaluationhsf_prefix) /\ ff_n_mce_alternating_mdr_absolute_firstevaluationhsf_prefix = (ff_ap_mce_alternating_mdr_absolute_firstevaluationhsf_prefix) * (ff_bp_mce_alternating_mdr_absolute_firstevaluationhsf_prefix) + (ff_an_mce_alternating_mdr_absolute_firstevaluationhsf_prefix) * (ff_bn_mce_alternating_mdr_absolute_firstevaluationhsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_absolute_firstevaluationhsf_positive ff_v_mce_mdr_absolute_firstevaluationhsf_positive. ((((exists ff_h_mce_mdr_absolute_firstevaluationhsf_positive_start. ff_h_mce_mdr_absolute_firstevaluationhsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_absolute_firstevaluationhsf_positive)) /\ exists ff_q_mce_mdr_absolute_firstevaluationhsf_positive_start. ff_u_mce_mdr_absolute_firstevaluationhsf_positive = ff_q_mce_mdr_absolute_firstevaluationhsf_positive_start * S ((S (0)) * ff_v_mce_mdr_absolute_firstevaluationhsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_absolute_firstevaluationhsf_positive_terminal. ff_h_mce_mdr_absolute_firstevaluationhsf_positive_terminal + S (mdr_p_absolute_firstevaluationh) = S ((S ((S (mdr_q_absolute_firstevaluationhs)))) * ff_v_mce_mdr_absolute_firstevaluationhsf_positive)) /\ exists ff_q_mce_mdr_absolute_firstevaluationhsf_positive_terminal. ff_u_mce_mdr_absolute_firstevaluationhsf_positive = ff_q_mce_mdr_absolute_firstevaluationhsf_positive_terminal * S ((S ((S (mdr_q_absolute_firstevaluationhs)))) * ff_v_mce_mdr_absolute_firstevaluationhsf_positive) + (mdr_p_absolute_firstevaluationh))) /\ forall ff_i_mce_mdr_absolute_firstevaluationhsf_positive. (exists ff_lt_mce_mdr_absolute_firstevaluationhsf_positive_bound. ff_lt_mce_mdr_absolute_firstevaluationhsf_positive_bound + S ff_i_mce_mdr_absolute_firstevaluationhsf_positive = (S (mdr_q_absolute_firstevaluationhs))) -> exists ff_a_mce_mdr_absolute_firstevaluationhsf_positive ff_r_mce_mdr_absolute_firstevaluationhsf_positive ff_s_mce_mdr_absolute_firstevaluationhsf_positive. ((((exists ff_h_mce_mdr_absolute_firstevaluationhsf_positive_summand. ff_h_mce_mdr_absolute_firstevaluationhsf_positive_summand + S (ff_a_mce_mdr_absolute_firstevaluationhsf_positive) = S ((S (ff_i_mce_mdr_absolute_firstevaluationhsf_positive)) * ff_uc_mce_fold_mdr_absolute_firstevaluationhsf)) /\ exists ff_q_mce_mdr_absolute_firstevaluationhsf_positive_summand. ff_ub_mce_fold_mdr_absolute_firstevaluationhsf = ff_q_mce_mdr_absolute_firstevaluationhsf_positive_summand * S ((S (ff_i_mce_mdr_absolute_firstevaluationhsf_positive)) * ff_uc_mce_fold_mdr_absolute_firstevaluationhsf) + (ff_a_mce_mdr_absolute_firstevaluationhsf_positive))) /\ ((((exists ff_h_mce_mdr_absolute_firstevaluationhsf_positive_partial. ff_h_mce_mdr_absolute_firstevaluationhsf_positive_partial + S (ff_r_mce_mdr_absolute_firstevaluationhsf_positive) = S ((S (ff_i_mce_mdr_absolute_firstevaluationhsf_positive)) * ff_v_mce_mdr_absolute_firstevaluationhsf_positive)) /\ exists ff_q_mce_mdr_absolute_firstevaluationhsf_positive_partial. ff_u_mce_mdr_absolute_firstevaluationhsf_positive = ff_q_mce_mdr_absolute_firstevaluationhsf_positive_partial * S ((S (ff_i_mce_mdr_absolute_firstevaluationhsf_positive)) * ff_v_mce_mdr_absolute_firstevaluationhsf_positive) + (ff_r_mce_mdr_absolute_firstevaluationhsf_positive))) /\ ((((exists ff_h_mce_mdr_absolute_firstevaluationhsf_positive_successor. ff_h_mce_mdr_absolute_firstevaluationhsf_positive_successor + S (ff_s_mce_mdr_absolute_firstevaluationhsf_positive) = S ((S (S ff_i_mce_mdr_absolute_firstevaluationhsf_positive)) * ff_v_mce_mdr_absolute_firstevaluationhsf_positive)) /\ exists ff_q_mce_mdr_absolute_firstevaluationhsf_positive_successor. ff_u_mce_mdr_absolute_firstevaluationhsf_positive = ff_q_mce_mdr_absolute_firstevaluationhsf_positive_successor * S ((S (S ff_i_mce_mdr_absolute_firstevaluationhsf_positive)) * ff_v_mce_mdr_absolute_firstevaluationhsf_positive) + (ff_s_mce_mdr_absolute_firstevaluationhsf_positive))) /\ ff_s_mce_mdr_absolute_firstevaluationhsf_positive = ff_r_mce_mdr_absolute_firstevaluationhsf_positive + ff_a_mce_mdr_absolute_firstevaluationhsf_positive)))))) /\ (exists ff_u_mce_mdr_absolute_firstevaluationhsf_negative ff_v_mce_mdr_absolute_firstevaluationhsf_negative. ((((exists ff_h_mce_mdr_absolute_firstevaluationhsf_negative_start. ff_h_mce_mdr_absolute_firstevaluationhsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_absolute_firstevaluationhsf_negative)) /\ exists ff_q_mce_mdr_absolute_firstevaluationhsf_negative_start. ff_u_mce_mdr_absolute_firstevaluationhsf_negative = ff_q_mce_mdr_absolute_firstevaluationhsf_negative_start * S ((S (0)) * ff_v_mce_mdr_absolute_firstevaluationhsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_absolute_firstevaluationhsf_negative_terminal. ff_h_mce_mdr_absolute_firstevaluationhsf_negative_terminal + S (mdr_n_absolute_firstevaluationh) = S ((S ((S (mdr_q_absolute_firstevaluationhs)))) * ff_v_mce_mdr_absolute_firstevaluationhsf_negative)) /\ exists ff_q_mce_mdr_absolute_firstevaluationhsf_negative_terminal. ff_u_mce_mdr_absolute_firstevaluationhsf_negative = ff_q_mce_mdr_absolute_firstevaluationhsf_negative_terminal * S ((S ((S (mdr_q_absolute_firstevaluationhs)))) * ff_v_mce_mdr_absolute_firstevaluationhsf_negative) + (mdr_n_absolute_firstevaluationh))) /\ forall ff_i_mce_mdr_absolute_firstevaluationhsf_negative. (exists ff_lt_mce_mdr_absolute_firstevaluationhsf_negative_bound. ff_lt_mce_mdr_absolute_firstevaluationhsf_negative_bound + S ff_i_mce_mdr_absolute_firstevaluationhsf_negative = (S (mdr_q_absolute_firstevaluationhs))) -> exists ff_a_mce_mdr_absolute_firstevaluationhsf_negative ff_r_mce_mdr_absolute_firstevaluationhsf_negative ff_s_mce_mdr_absolute_firstevaluationhsf_negative. ((((exists ff_h_mce_mdr_absolute_firstevaluationhsf_negative_summand. ff_h_mce_mdr_absolute_firstevaluationhsf_negative_summand + S (ff_a_mce_mdr_absolute_firstevaluationhsf_negative) = S ((S (ff_i_mce_mdr_absolute_firstevaluationhsf_negative)) * ff_vc_mce_fold_mdr_absolute_firstevaluationhsf)) /\ exists ff_q_mce_mdr_absolute_firstevaluationhsf_negative_summand. ff_vb_mce_fold_mdr_absolute_firstevaluationhsf = ff_q_mce_mdr_absolute_firstevaluationhsf_negative_summand * S ((S (ff_i_mce_mdr_absolute_firstevaluationhsf_negative)) * ff_vc_mce_fold_mdr_absolute_firstevaluationhsf) + (ff_a_mce_mdr_absolute_firstevaluationhsf_negative))) /\ ((((exists ff_h_mce_mdr_absolute_firstevaluationhsf_negative_partial. ff_h_mce_mdr_absolute_firstevaluationhsf_negative_partial + S (ff_r_mce_mdr_absolute_firstevaluationhsf_negative) = S ((S (ff_i_mce_mdr_absolute_firstevaluationhsf_negative)) * ff_v_mce_mdr_absolute_firstevaluationhsf_negative)) /\ exists ff_q_mce_mdr_absolute_firstevaluationhsf_negative_partial. ff_u_mce_mdr_absolute_firstevaluationhsf_negative = ff_q_mce_mdr_absolute_firstevaluationhsf_negative_partial * S ((S (ff_i_mce_mdr_absolute_firstevaluationhsf_negative)) * ff_v_mce_mdr_absolute_firstevaluationhsf_negative) + (ff_r_mce_mdr_absolute_firstevaluationhsf_negative))) /\ ((((exists ff_h_mce_mdr_absolute_firstevaluationhsf_negative_successor. ff_h_mce_mdr_absolute_firstevaluationhsf_negative_successor + S (ff_s_mce_mdr_absolute_firstevaluationhsf_negative) = S ((S (S ff_i_mce_mdr_absolute_firstevaluationhsf_negative)) * ff_v_mce_mdr_absolute_firstevaluationhsf_negative)) /\ exists ff_q_mce_mdr_absolute_firstevaluationhsf_negative_successor. ff_u_mce_mdr_absolute_firstevaluationhsf_negative = ff_q_mce_mdr_absolute_firstevaluationhsf_negative_successor * S ((S (S ff_i_mce_mdr_absolute_firstevaluationhsf_negative)) * ff_v_mce_mdr_absolute_firstevaluationhsf_negative) + (ff_s_mce_mdr_absolute_firstevaluationhsf_negative))) /\ ff_s_mce_mdr_absolute_firstevaluationhsf_negative = ff_r_mce_mdr_absolute_firstevaluationhsf_negative + ff_a_mce_mdr_absolute_firstevaluationhsf_negative))))))))))))))) /\ ((exists mdr_gap_absolute_firstevaluationi. mdr_gap_absolute_firstevaluationi + S (mdr_i_absolute_firstevaluation) = (mdr_l_absolute_firstevaluation)) /\ (exists mdr_z_absolute_firstevaluationr. ((exists mdr_a_absolute_firstevaluationrc mdr_b_absolute_firstevaluationrc mdr_c_absolute_firstevaluationrc mdr_e_absolute_firstevaluationrc mdr_f_absolute_firstevaluationrc. ((mdr_a_absolute_firstevaluationrc = ((d) + (ab)) * S ((d) + (ab)) + ((ab) + (ab))) /\ ((mdr_b_absolute_firstevaluationrc = ((ac) + (bb)) * S ((ac) + (bb)) + ((bb) + (bb))) /\ ((mdr_c_absolute_firstevaluationrc = ((mdr_a_absolute_firstevaluationrc) + (mdr_b_absolute_firstevaluationrc)) * S ((mdr_a_absolute_firstevaluationrc) + (mdr_b_absolute_firstevaluationrc)) + ((mdr_b_absolute_firstevaluationrc) + (mdr_b_absolute_firstevaluationrc))) /\ ((mdr_e_absolute_firstevaluationrc = ((mdr_p_absolute_first) + (mdr_n_absolute_first)) * S ((mdr_p_absolute_first) + (mdr_n_absolute_first)) + ((mdr_n_absolute_first) + (mdr_n_absolute_first))) /\ ((mdr_f_absolute_firstevaluationrc = ((bc) + (mdr_e_absolute_firstevaluationrc)) * S ((bc) + (mdr_e_absolute_firstevaluationrc)) + ((mdr_e_absolute_firstevaluationrc) + (mdr_e_absolute_firstevaluationrc))) /\ ((mdr_z_absolute_firstevaluationr) = ((mdr_c_absolute_firstevaluationrc) + (mdr_f_absolute_firstevaluationrc)) * S ((mdr_c_absolute_firstevaluationrc) + (mdr_f_absolute_firstevaluationrc)) + ((mdr_f_absolute_firstevaluationrc) + (mdr_f_absolute_firstevaluationrc))))))))) /\ (((exists ff_h_mdr_absolute_firstevaluationrb. ff_h_mdr_absolute_firstevaluationrb + S (mdr_z_absolute_firstevaluationr) = S ((S (mdr_i_absolute_firstevaluation)) * mdr_c_absolute_firstevaluation)) /\ exists ff_q_mdr_absolute_firstevaluationrb. mdr_b_absolute_firstevaluation = ff_q_mdr_absolute_firstevaluationrb * S ((S (mdr_i_absolute_firstevaluation)) * mdr_c_absolute_firstevaluation) + (mdr_z_absolute_firstevaluationr)))))))) /\ (((mdr_p_absolute_first) = (mdr_n_absolute_first) + (D)) \/ ((mdr_n_absolute_first) = (mdr_p_absolute_first) + (D))))) -> (exists mdr_p_absolute_second mdr_n_absolute_second. ((exists mdr_b_absolute_secondevaluation mdr_c_absolute_secondevaluation mdr_l_absolute_secondevaluation mdr_i_absolute_secondevaluation. ((forall mdr_i_absolute_secondevaluationh. (exists mdr_gap_absolute_secondevaluationhi. mdr_gap_absolute_secondevaluationhi + S (mdr_i_absolute_secondevaluationh) = (mdr_l_absolute_secondevaluation)) -> exists mdr_d_absolute_secondevaluationh mdr_pb_absolute_secondevaluationh mdr_pc_absolute_secondevaluationh mdr_nb_absolute_secondevaluationh mdr_nc_absolute_secondevaluationh mdr_p_absolute_secondevaluationh mdr_n_absolute_secondevaluationh. ((exists mdr_z_absolute_secondevaluationhr. ((exists mdr_a_absolute_secondevaluationhrc mdr_b_absolute_secondevaluationhrc mdr_c_absolute_secondevaluationhrc mdr_e_absolute_secondevaluationhrc mdr_f_absolute_secondevaluationhrc. ((mdr_a_absolute_secondevaluationhrc = ((mdr_d_absolute_secondevaluationh) + (mdr_pb_absolute_secondevaluationh)) * S ((mdr_d_absolute_secondevaluationh) + (mdr_pb_absolute_secondevaluationh)) + ((mdr_pb_absolute_secondevaluationh) + (mdr_pb_absolute_secondevaluationh))) /\ ((mdr_b_absolute_secondevaluationhrc = ((mdr_pc_absolute_secondevaluationh) + (mdr_nb_absolute_secondevaluationh)) * S ((mdr_pc_absolute_secondevaluationh) + (mdr_nb_absolute_secondevaluationh)) + ((mdr_nb_absolute_secondevaluationh) + (mdr_nb_absolute_secondevaluationh))) /\ ((mdr_c_absolute_secondevaluationhrc = ((mdr_a_absolute_secondevaluationhrc) + (mdr_b_absolute_secondevaluationhrc)) * S ((mdr_a_absolute_secondevaluationhrc) + (mdr_b_absolute_secondevaluationhrc)) + ((mdr_b_absolute_secondevaluationhrc) + (mdr_b_absolute_secondevaluationhrc))) /\ ((mdr_e_absolute_secondevaluationhrc = ((mdr_p_absolute_secondevaluationh) + (mdr_n_absolute_secondevaluationh)) * S ((mdr_p_absolute_secondevaluationh) + (mdr_n_absolute_secondevaluationh)) + ((mdr_n_absolute_secondevaluationh) + (mdr_n_absolute_secondevaluationh))) /\ ((mdr_f_absolute_secondevaluationhrc = ((mdr_nc_absolute_secondevaluationh) + (mdr_e_absolute_secondevaluationhrc)) * S ((mdr_nc_absolute_secondevaluationh) + (mdr_e_absolute_secondevaluationhrc)) + ((mdr_e_absolute_secondevaluationhrc) + (mdr_e_absolute_secondevaluationhrc))) /\ ((mdr_z_absolute_secondevaluationhr) = ((mdr_c_absolute_secondevaluationhrc) + (mdr_f_absolute_secondevaluationhrc)) * S ((mdr_c_absolute_secondevaluationhrc) + (mdr_f_absolute_secondevaluationhrc)) + ((mdr_f_absolute_secondevaluationhrc) + (mdr_f_absolute_secondevaluationhrc))))))))) /\ (((exists ff_h_mdr_absolute_secondevaluationhrb. ff_h_mdr_absolute_secondevaluationhrb + S (mdr_z_absolute_secondevaluationhr) = S ((S (mdr_i_absolute_secondevaluationh)) * mdr_c_absolute_secondevaluation)) /\ exists ff_q_mdr_absolute_secondevaluationhrb. mdr_b_absolute_secondevaluation = ff_q_mdr_absolute_secondevaluationhrb * S ((S (mdr_i_absolute_secondevaluationh)) * mdr_c_absolute_secondevaluation) + (mdr_z_absolute_secondevaluationhr))))) /\ (((((mdr_d_absolute_secondevaluationh) = 0) /\ (((mdr_p_absolute_secondevaluationh) = 1) /\ ((mdr_n_absolute_secondevaluationh) = 0))) \/ exists mdr_q_absolute_secondevaluationhs mdr_eb_absolute_secondevaluationhs mdr_ec_absolute_secondevaluationhs mdr_fb_absolute_secondevaluationhs mdr_fc_absolute_secondevaluationhs. (((mdr_d_absolute_secondevaluationh) = S (mdr_q_absolute_secondevaluationhs)) /\ ((forall mdr_j_absolute_secondevaluationhsc. (exists mdr_gap_absolute_secondevaluationhscj. mdr_gap_absolute_secondevaluationhscj + S (mdr_j_absolute_secondevaluationhsc) = (S (mdr_q_absolute_secondevaluationhs))) -> exists mdr_i_absolute_secondevaluationhsc mdr_up_absolute_secondevaluationhsc mdr_us_absolute_secondevaluationhsc mdr_un_absolute_secondevaluationhsc mdr_ut_absolute_secondevaluationhsc mdr_p_absolute_secondevaluationhsc mdr_n_absolute_secondevaluationhsc. ((exists mdr_gap_absolute_secondevaluationhsci. mdr_gap_absolute_secondevaluationhsci + S (mdr_i_absolute_secondevaluationhsc) = (mdr_i_absolute_secondevaluationh)) /\ ((exists mdr_z_absolute_secondevaluationhscr. ((exists mdr_a_absolute_secondevaluationhscrc mdr_b_absolute_secondevaluationhscrc mdr_c_absolute_secondevaluationhscrc mdr_e_absolute_secondevaluationhscrc mdr_f_absolute_secondevaluationhscrc. ((mdr_a_absolute_secondevaluationhscrc = ((mdr_q_absolute_secondevaluationhs) + (mdr_up_absolute_secondevaluationhsc)) * S ((mdr_q_absolute_secondevaluationhs) + (mdr_up_absolute_secondevaluationhsc)) + ((mdr_up_absolute_secondevaluationhsc) + (mdr_up_absolute_secondevaluationhsc))) /\ ((mdr_b_absolute_secondevaluationhscrc = ((mdr_us_absolute_secondevaluationhsc) + (mdr_un_absolute_secondevaluationhsc)) * S ((mdr_us_absolute_secondevaluationhsc) + (mdr_un_absolute_secondevaluationhsc)) + ((mdr_un_absolute_secondevaluationhsc) + (mdr_un_absolute_secondevaluationhsc))) /\ ((mdr_c_absolute_secondevaluationhscrc = ((mdr_a_absolute_secondevaluationhscrc) + (mdr_b_absolute_secondevaluationhscrc)) * S ((mdr_a_absolute_secondevaluationhscrc) + (mdr_b_absolute_secondevaluationhscrc)) + ((mdr_b_absolute_secondevaluationhscrc) + (mdr_b_absolute_secondevaluationhscrc))) /\ ((mdr_e_absolute_secondevaluationhscrc = ((mdr_p_absolute_secondevaluationhsc) + (mdr_n_absolute_secondevaluationhsc)) * S ((mdr_p_absolute_secondevaluationhsc) + (mdr_n_absolute_secondevaluationhsc)) + ((mdr_n_absolute_secondevaluationhsc) + (mdr_n_absolute_secondevaluationhsc))) /\ ((mdr_f_absolute_secondevaluationhscrc = ((mdr_ut_absolute_secondevaluationhsc) + (mdr_e_absolute_secondevaluationhscrc)) * S ((mdr_ut_absolute_secondevaluationhsc) + (mdr_e_absolute_secondevaluationhscrc)) + ((mdr_e_absolute_secondevaluationhscrc) + (mdr_e_absolute_secondevaluationhscrc))) /\ ((mdr_z_absolute_secondevaluationhscr) = ((mdr_c_absolute_secondevaluationhscrc) + (mdr_f_absolute_secondevaluationhscrc)) * S ((mdr_c_absolute_secondevaluationhscrc) + (mdr_f_absolute_secondevaluationhscrc)) + ((mdr_f_absolute_secondevaluationhscrc) + (mdr_f_absolute_secondevaluationhscrc))))))))) /\ (((exists ff_h_mdr_absolute_secondevaluationhscrb. ff_h_mdr_absolute_secondevaluationhscrb + S (mdr_z_absolute_secondevaluationhscr) = S ((S (mdr_i_absolute_secondevaluationhsc)) * mdr_c_absolute_secondevaluation)) /\ exists ff_q_mdr_absolute_secondevaluationhscrb. mdr_b_absolute_secondevaluation = ff_q_mdr_absolute_secondevaluationhscrb * S ((S (mdr_i_absolute_secondevaluationhsc)) * mdr_c_absolute_secondevaluation) + (mdr_z_absolute_secondevaluationhscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_absolute_secondevaluationhscm_positive. (exists ff_gap_mdm_lt_mdr_absolute_secondevaluationhscm_positive_index_bound. ff_gap_mdm_lt_mdr_absolute_secondevaluationhscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_absolute_secondevaluationhscm_positive) = ((mdr_q_absolute_secondevaluationhs) * (mdr_q_absolute_secondevaluationhs))) -> exists ff_row_mdm_prefix_mdr_absolute_secondevaluationhscm_positive ff_column_mdm_prefix_mdr_absolute_secondevaluationhscm_positive ff_value_mdm_prefix_mdr_absolute_secondevaluationhscm_positive. (ff_index_mdm_prefix_mdr_absolute_secondevaluationhscm_positive = (mdr_q_absolute_secondevaluationhs) * ff_row_mdm_prefix_mdr_absolute_secondevaluationhscm_positive + ff_column_mdm_prefix_mdr_absolute_secondevaluationhscm_positive /\ ((exists ff_gap_mdm_lt_mdr_absolute_secondevaluationhscm_positive_column_bound. ff_gap_mdm_lt_mdr_absolute_secondevaluationhscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_absolute_secondevaluationhscm_positive) = (mdr_q_absolute_secondevaluationhs)) /\ ((exists ff_row_mdm_cell_mdr_absolute_secondevaluationhscm_positive_cell ff_column_mdm_cell_mdr_absolute_secondevaluationhscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_absolute_secondevaluationhscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_absolute_secondevaluationhscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_absolute_secondevaluationhscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_absolute_secondevaluationhscm_positive_cell = ff_row_mdm_prefix_mdr_absolute_secondevaluationhscm_positive) \/ ((exists ff_gap_mdm_le_mdr_absolute_secondevaluationhscm_positive_cell_row_after. ff_gap_mdm_le_mdr_absolute_secondevaluationhscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_absolute_secondevaluationhscm_positive)) /\ ff_row_mdm_cell_mdr_absolute_secondevaluationhscm_positive_cell = S ff_row_mdm_prefix_mdr_absolute_secondevaluationhscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_absolute_secondevaluationhscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_absolute_secondevaluationhscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_absolute_secondevaluationhscm_positive) = (mdr_j_absolute_secondevaluationhsc)) /\ ff_column_mdm_cell_mdr_absolute_secondevaluationhscm_positive_cell = ff_column_mdm_prefix_mdr_absolute_secondevaluationhscm_positive) \/ ((exists ff_gap_mdm_le_mdr_absolute_secondevaluationhscm_positive_cell_column_after. ff_gap_mdm_le_mdr_absolute_secondevaluationhscm_positive_cell_column_after + (mdr_j_absolute_secondevaluationhsc) = (ff_column_mdm_prefix_mdr_absolute_secondevaluationhscm_positive)) /\ ff_column_mdm_cell_mdr_absolute_secondevaluationhscm_positive_cell = S ff_column_mdm_prefix_mdr_absolute_secondevaluationhscm_positive))) /\ (((exists ff_h_mdm_mdr_absolute_secondevaluationhscm_positive_cell_source. ff_h_mdm_mdr_absolute_secondevaluationhscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_absolute_secondevaluationhscm_positive) = S ((S ((ff_row_mdm_cell_mdr_absolute_secondevaluationhscm_positive_cell) * (S (mdr_q_absolute_secondevaluationhs)) + (ff_column_mdm_cell_mdr_absolute_secondevaluationhscm_positive_cell))) * mdr_pc_absolute_secondevaluationh)) /\ exists ff_q_mdm_mdr_absolute_secondevaluationhscm_positive_cell_source. mdr_pb_absolute_secondevaluationh = ff_q_mdm_mdr_absolute_secondevaluationhscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_absolute_secondevaluationhscm_positive_cell) * (S (mdr_q_absolute_secondevaluationhs)) + (ff_column_mdm_cell_mdr_absolute_secondevaluationhscm_positive_cell))) * mdr_pc_absolute_secondevaluationh) + (ff_value_mdm_prefix_mdr_absolute_secondevaluationhscm_positive)))))) /\ (((exists ff_h_mdm_mdr_absolute_secondevaluationhscm_positive_target. ff_h_mdm_mdr_absolute_secondevaluationhscm_positive_target + S (ff_value_mdm_prefix_mdr_absolute_secondevaluationhscm_positive) = S ((S (ff_index_mdm_prefix_mdr_absolute_secondevaluationhscm_positive)) * mdr_us_absolute_secondevaluationhsc)) /\ exists ff_q_mdm_mdr_absolute_secondevaluationhscm_positive_target. mdr_up_absolute_secondevaluationhsc = ff_q_mdm_mdr_absolute_secondevaluationhscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_absolute_secondevaluationhscm_positive)) * mdr_us_absolute_secondevaluationhsc) + (ff_value_mdm_prefix_mdr_absolute_secondevaluationhscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_absolute_secondevaluationhscm_negative. (exists ff_gap_mdm_lt_mdr_absolute_secondevaluationhscm_negative_index_bound. ff_gap_mdm_lt_mdr_absolute_secondevaluationhscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_absolute_secondevaluationhscm_negative) = ((mdr_q_absolute_secondevaluationhs) * (mdr_q_absolute_secondevaluationhs))) -> exists ff_row_mdm_prefix_mdr_absolute_secondevaluationhscm_negative ff_column_mdm_prefix_mdr_absolute_secondevaluationhscm_negative ff_value_mdm_prefix_mdr_absolute_secondevaluationhscm_negative. (ff_index_mdm_prefix_mdr_absolute_secondevaluationhscm_negative = (mdr_q_absolute_secondevaluationhs) * ff_row_mdm_prefix_mdr_absolute_secondevaluationhscm_negative + ff_column_mdm_prefix_mdr_absolute_secondevaluationhscm_negative /\ ((exists ff_gap_mdm_lt_mdr_absolute_secondevaluationhscm_negative_column_bound. ff_gap_mdm_lt_mdr_absolute_secondevaluationhscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_absolute_secondevaluationhscm_negative) = (mdr_q_absolute_secondevaluationhs)) /\ ((exists ff_row_mdm_cell_mdr_absolute_secondevaluationhscm_negative_cell ff_column_mdm_cell_mdr_absolute_secondevaluationhscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_absolute_secondevaluationhscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_absolute_secondevaluationhscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_absolute_secondevaluationhscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_absolute_secondevaluationhscm_negative_cell = ff_row_mdm_prefix_mdr_absolute_secondevaluationhscm_negative) \/ ((exists ff_gap_mdm_le_mdr_absolute_secondevaluationhscm_negative_cell_row_after. ff_gap_mdm_le_mdr_absolute_secondevaluationhscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_absolute_secondevaluationhscm_negative)) /\ ff_row_mdm_cell_mdr_absolute_secondevaluationhscm_negative_cell = S ff_row_mdm_prefix_mdr_absolute_secondevaluationhscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_absolute_secondevaluationhscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_absolute_secondevaluationhscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_absolute_secondevaluationhscm_negative) = (mdr_j_absolute_secondevaluationhsc)) /\ ff_column_mdm_cell_mdr_absolute_secondevaluationhscm_negative_cell = ff_column_mdm_prefix_mdr_absolute_secondevaluationhscm_negative) \/ ((exists ff_gap_mdm_le_mdr_absolute_secondevaluationhscm_negative_cell_column_after. ff_gap_mdm_le_mdr_absolute_secondevaluationhscm_negative_cell_column_after + (mdr_j_absolute_secondevaluationhsc) = (ff_column_mdm_prefix_mdr_absolute_secondevaluationhscm_negative)) /\ ff_column_mdm_cell_mdr_absolute_secondevaluationhscm_negative_cell = S ff_column_mdm_prefix_mdr_absolute_secondevaluationhscm_negative))) /\ (((exists ff_h_mdm_mdr_absolute_secondevaluationhscm_negative_cell_source. ff_h_mdm_mdr_absolute_secondevaluationhscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_absolute_secondevaluationhscm_negative) = S ((S ((ff_row_mdm_cell_mdr_absolute_secondevaluationhscm_negative_cell) * (S (mdr_q_absolute_secondevaluationhs)) + (ff_column_mdm_cell_mdr_absolute_secondevaluationhscm_negative_cell))) * mdr_nc_absolute_secondevaluationh)) /\ exists ff_q_mdm_mdr_absolute_secondevaluationhscm_negative_cell_source. mdr_nb_absolute_secondevaluationh = ff_q_mdm_mdr_absolute_secondevaluationhscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_absolute_secondevaluationhscm_negative_cell) * (S (mdr_q_absolute_secondevaluationhs)) + (ff_column_mdm_cell_mdr_absolute_secondevaluationhscm_negative_cell))) * mdr_nc_absolute_secondevaluationh) + (ff_value_mdm_prefix_mdr_absolute_secondevaluationhscm_negative)))))) /\ (((exists ff_h_mdm_mdr_absolute_secondevaluationhscm_negative_target. ff_h_mdm_mdr_absolute_secondevaluationhscm_negative_target + S (ff_value_mdm_prefix_mdr_absolute_secondevaluationhscm_negative) = S ((S (ff_index_mdm_prefix_mdr_absolute_secondevaluationhscm_negative)) * mdr_ut_absolute_secondevaluationhsc)) /\ exists ff_q_mdm_mdr_absolute_secondevaluationhscm_negative_target. mdr_un_absolute_secondevaluationhsc = ff_q_mdm_mdr_absolute_secondevaluationhscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_absolute_secondevaluationhscm_negative)) * mdr_ut_absolute_secondevaluationhsc) + (ff_value_mdm_prefix_mdr_absolute_secondevaluationhscm_negative))))))))) /\ ((((exists ff_h_mdr_absolute_secondevaluationhscp. ff_h_mdr_absolute_secondevaluationhscp + S (mdr_p_absolute_secondevaluationhsc) = S ((S (mdr_j_absolute_secondevaluationhsc)) * mdr_ec_absolute_secondevaluationhs)) /\ exists ff_q_mdr_absolute_secondevaluationhscp. mdr_eb_absolute_secondevaluationhs = ff_q_mdr_absolute_secondevaluationhscp * S ((S (mdr_j_absolute_secondevaluationhsc)) * mdr_ec_absolute_secondevaluationhs) + (mdr_p_absolute_secondevaluationhsc))) /\ (((exists ff_h_mdr_absolute_secondevaluationhscn. ff_h_mdr_absolute_secondevaluationhscn + S (mdr_n_absolute_secondevaluationhsc) = S ((S (mdr_j_absolute_secondevaluationhsc)) * mdr_fc_absolute_secondevaluationhs)) /\ exists ff_q_mdr_absolute_secondevaluationhscn. mdr_fb_absolute_secondevaluationhs = ff_q_mdr_absolute_secondevaluationhscn * S ((S (mdr_j_absolute_secondevaluationhsc)) * mdr_fc_absolute_secondevaluationhs) + (mdr_n_absolute_secondevaluationhsc)))))))) /\ (exists ff_ub_mce_fold_mdr_absolute_secondevaluationhsf ff_uc_mce_fold_mdr_absolute_secondevaluationhsf ff_vb_mce_fold_mdr_absolute_secondevaluationhsf ff_vc_mce_fold_mdr_absolute_secondevaluationhsf. ((forall ff_index_mce_alternating_mdr_absolute_secondevaluationhsf_prefix. (exists ff_gap_mce_mdr_absolute_secondevaluationhsf_prefix_index. ff_gap_mce_mdr_absolute_secondevaluationhsf_prefix_index + S (ff_index_mce_alternating_mdr_absolute_secondevaluationhsf_prefix) = (S (mdr_q_absolute_secondevaluationhs))) -> exists ff_ap_mce_alternating_mdr_absolute_secondevaluationhsf_prefix ff_an_mce_alternating_mdr_absolute_secondevaluationhsf_prefix ff_bp_mce_alternating_mdr_absolute_secondevaluationhsf_prefix ff_bn_mce_alternating_mdr_absolute_secondevaluationhsf_prefix ff_p_mce_alternating_mdr_absolute_secondevaluationhsf_prefix ff_n_mce_alternating_mdr_absolute_secondevaluationhsf_prefix. ((((exists ff_h_mce_mdr_absolute_secondevaluationhsf_prefix_ap. ff_h_mce_mdr_absolute_secondevaluationhsf_prefix_ap + S (ff_ap_mce_alternating_mdr_absolute_secondevaluationhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_absolute_secondevaluationhsf_prefix)) * mdr_pc_absolute_secondevaluationh)) /\ exists ff_q_mce_mdr_absolute_secondevaluationhsf_prefix_ap. mdr_pb_absolute_secondevaluationh = ff_q_mce_mdr_absolute_secondevaluationhsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_absolute_secondevaluationhsf_prefix)) * mdr_pc_absolute_secondevaluationh) + (ff_ap_mce_alternating_mdr_absolute_secondevaluationhsf_prefix))) /\ ((((exists ff_h_mce_mdr_absolute_secondevaluationhsf_prefix_an. ff_h_mce_mdr_absolute_secondevaluationhsf_prefix_an + S (ff_an_mce_alternating_mdr_absolute_secondevaluationhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_absolute_secondevaluationhsf_prefix)) * mdr_nc_absolute_secondevaluationh)) /\ exists ff_q_mce_mdr_absolute_secondevaluationhsf_prefix_an. mdr_nb_absolute_secondevaluationh = ff_q_mce_mdr_absolute_secondevaluationhsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_absolute_secondevaluationhsf_prefix)) * mdr_nc_absolute_secondevaluationh) + (ff_an_mce_alternating_mdr_absolute_secondevaluationhsf_prefix))) /\ ((((exists ff_h_mce_mdr_absolute_secondevaluationhsf_prefix_bp. ff_h_mce_mdr_absolute_secondevaluationhsf_prefix_bp + S (ff_bp_mce_alternating_mdr_absolute_secondevaluationhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_absolute_secondevaluationhsf_prefix)) * mdr_ec_absolute_secondevaluationhs)) /\ exists ff_q_mce_mdr_absolute_secondevaluationhsf_prefix_bp. mdr_eb_absolute_secondevaluationhs = ff_q_mce_mdr_absolute_secondevaluationhsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_absolute_secondevaluationhsf_prefix)) * mdr_ec_absolute_secondevaluationhs) + (ff_bp_mce_alternating_mdr_absolute_secondevaluationhsf_prefix))) /\ ((((exists ff_h_mce_mdr_absolute_secondevaluationhsf_prefix_bn. ff_h_mce_mdr_absolute_secondevaluationhsf_prefix_bn + S (ff_bn_mce_alternating_mdr_absolute_secondevaluationhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_absolute_secondevaluationhsf_prefix)) * mdr_fc_absolute_secondevaluationhs)) /\ exists ff_q_mce_mdr_absolute_secondevaluationhsf_prefix_bn. mdr_fb_absolute_secondevaluationhs = ff_q_mce_mdr_absolute_secondevaluationhsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_absolute_secondevaluationhsf_prefix)) * mdr_fc_absolute_secondevaluationhs) + (ff_bn_mce_alternating_mdr_absolute_secondevaluationhsf_prefix))) /\ ((((exists ff_h_mce_mdr_absolute_secondevaluationhsf_prefix_positive. ff_h_mce_mdr_absolute_secondevaluationhsf_prefix_positive + S (ff_p_mce_alternating_mdr_absolute_secondevaluationhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_absolute_secondevaluationhsf_prefix)) * ff_uc_mce_fold_mdr_absolute_secondevaluationhsf)) /\ exists ff_q_mce_mdr_absolute_secondevaluationhsf_prefix_positive. ff_ub_mce_fold_mdr_absolute_secondevaluationhsf = ff_q_mce_mdr_absolute_secondevaluationhsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_absolute_secondevaluationhsf_prefix)) * ff_uc_mce_fold_mdr_absolute_secondevaluationhsf) + (ff_p_mce_alternating_mdr_absolute_secondevaluationhsf_prefix))) /\ ((((exists ff_h_mce_mdr_absolute_secondevaluationhsf_prefix_negative. ff_h_mce_mdr_absolute_secondevaluationhsf_prefix_negative + S (ff_n_mce_alternating_mdr_absolute_secondevaluationhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_absolute_secondevaluationhsf_prefix)) * ff_vc_mce_fold_mdr_absolute_secondevaluationhsf)) /\ exists ff_q_mce_mdr_absolute_secondevaluationhsf_prefix_negative. ff_vb_mce_fold_mdr_absolute_secondevaluationhsf = ff_q_mce_mdr_absolute_secondevaluationhsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_absolute_secondevaluationhsf_prefix)) * ff_vc_mce_fold_mdr_absolute_secondevaluationhsf) + (ff_n_mce_alternating_mdr_absolute_secondevaluationhsf_prefix))) /\ (((exists ff_even_mce_term_mdr_absolute_secondevaluationhsf_prefix_term. ff_index_mce_alternating_mdr_absolute_secondevaluationhsf_prefix = 2 * ff_even_mce_term_mdr_absolute_secondevaluationhsf_prefix_term) /\ (ff_p_mce_alternating_mdr_absolute_secondevaluationhsf_prefix = (ff_ap_mce_alternating_mdr_absolute_secondevaluationhsf_prefix) * (ff_bp_mce_alternating_mdr_absolute_secondevaluationhsf_prefix) + (ff_an_mce_alternating_mdr_absolute_secondevaluationhsf_prefix) * (ff_bn_mce_alternating_mdr_absolute_secondevaluationhsf_prefix) /\ ff_n_mce_alternating_mdr_absolute_secondevaluationhsf_prefix = (ff_ap_mce_alternating_mdr_absolute_secondevaluationhsf_prefix) * (ff_bn_mce_alternating_mdr_absolute_secondevaluationhsf_prefix) + (ff_an_mce_alternating_mdr_absolute_secondevaluationhsf_prefix) * (ff_bp_mce_alternating_mdr_absolute_secondevaluationhsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_absolute_secondevaluationhsf_prefix_term. ff_index_mce_alternating_mdr_absolute_secondevaluationhsf_prefix = 2 * ff_odd_mce_term_mdr_absolute_secondevaluationhsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_absolute_secondevaluationhsf_prefix = (ff_ap_mce_alternating_mdr_absolute_secondevaluationhsf_prefix) * (ff_bn_mce_alternating_mdr_absolute_secondevaluationhsf_prefix) + (ff_an_mce_alternating_mdr_absolute_secondevaluationhsf_prefix) * (ff_bp_mce_alternating_mdr_absolute_secondevaluationhsf_prefix) /\ ff_n_mce_alternating_mdr_absolute_secondevaluationhsf_prefix = (ff_ap_mce_alternating_mdr_absolute_secondevaluationhsf_prefix) * (ff_bp_mce_alternating_mdr_absolute_secondevaluationhsf_prefix) + (ff_an_mce_alternating_mdr_absolute_secondevaluationhsf_prefix) * (ff_bn_mce_alternating_mdr_absolute_secondevaluationhsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_absolute_secondevaluationhsf_positive ff_v_mce_mdr_absolute_secondevaluationhsf_positive. ((((exists ff_h_mce_mdr_absolute_secondevaluationhsf_positive_start. ff_h_mce_mdr_absolute_secondevaluationhsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_absolute_secondevaluationhsf_positive)) /\ exists ff_q_mce_mdr_absolute_secondevaluationhsf_positive_start. ff_u_mce_mdr_absolute_secondevaluationhsf_positive = ff_q_mce_mdr_absolute_secondevaluationhsf_positive_start * S ((S (0)) * ff_v_mce_mdr_absolute_secondevaluationhsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_absolute_secondevaluationhsf_positive_terminal. ff_h_mce_mdr_absolute_secondevaluationhsf_positive_terminal + S (mdr_p_absolute_secondevaluationh) = S ((S ((S (mdr_q_absolute_secondevaluationhs)))) * ff_v_mce_mdr_absolute_secondevaluationhsf_positive)) /\ exists ff_q_mce_mdr_absolute_secondevaluationhsf_positive_terminal. ff_u_mce_mdr_absolute_secondevaluationhsf_positive = ff_q_mce_mdr_absolute_secondevaluationhsf_positive_terminal * S ((S ((S (mdr_q_absolute_secondevaluationhs)))) * ff_v_mce_mdr_absolute_secondevaluationhsf_positive) + (mdr_p_absolute_secondevaluationh))) /\ forall ff_i_mce_mdr_absolute_secondevaluationhsf_positive. (exists ff_lt_mce_mdr_absolute_secondevaluationhsf_positive_bound. ff_lt_mce_mdr_absolute_secondevaluationhsf_positive_bound + S ff_i_mce_mdr_absolute_secondevaluationhsf_positive = (S (mdr_q_absolute_secondevaluationhs))) -> exists ff_a_mce_mdr_absolute_secondevaluationhsf_positive ff_r_mce_mdr_absolute_secondevaluationhsf_positive ff_s_mce_mdr_absolute_secondevaluationhsf_positive. ((((exists ff_h_mce_mdr_absolute_secondevaluationhsf_positive_summand. ff_h_mce_mdr_absolute_secondevaluationhsf_positive_summand + S (ff_a_mce_mdr_absolute_secondevaluationhsf_positive) = S ((S (ff_i_mce_mdr_absolute_secondevaluationhsf_positive)) * ff_uc_mce_fold_mdr_absolute_secondevaluationhsf)) /\ exists ff_q_mce_mdr_absolute_secondevaluationhsf_positive_summand. ff_ub_mce_fold_mdr_absolute_secondevaluationhsf = ff_q_mce_mdr_absolute_secondevaluationhsf_positive_summand * S ((S (ff_i_mce_mdr_absolute_secondevaluationhsf_positive)) * ff_uc_mce_fold_mdr_absolute_secondevaluationhsf) + (ff_a_mce_mdr_absolute_secondevaluationhsf_positive))) /\ ((((exists ff_h_mce_mdr_absolute_secondevaluationhsf_positive_partial. ff_h_mce_mdr_absolute_secondevaluationhsf_positive_partial + S (ff_r_mce_mdr_absolute_secondevaluationhsf_positive) = S ((S (ff_i_mce_mdr_absolute_secondevaluationhsf_positive)) * ff_v_mce_mdr_absolute_secondevaluationhsf_positive)) /\ exists ff_q_mce_mdr_absolute_secondevaluationhsf_positive_partial. ff_u_mce_mdr_absolute_secondevaluationhsf_positive = ff_q_mce_mdr_absolute_secondevaluationhsf_positive_partial * S ((S (ff_i_mce_mdr_absolute_secondevaluationhsf_positive)) * ff_v_mce_mdr_absolute_secondevaluationhsf_positive) + (ff_r_mce_mdr_absolute_secondevaluationhsf_positive))) /\ ((((exists ff_h_mce_mdr_absolute_secondevaluationhsf_positive_successor. ff_h_mce_mdr_absolute_secondevaluationhsf_positive_successor + S (ff_s_mce_mdr_absolute_secondevaluationhsf_positive) = S ((S (S ff_i_mce_mdr_absolute_secondevaluationhsf_positive)) * ff_v_mce_mdr_absolute_secondevaluationhsf_positive)) /\ exists ff_q_mce_mdr_absolute_secondevaluationhsf_positive_successor. ff_u_mce_mdr_absolute_secondevaluationhsf_positive = ff_q_mce_mdr_absolute_secondevaluationhsf_positive_successor * S ((S (S ff_i_mce_mdr_absolute_secondevaluationhsf_positive)) * ff_v_mce_mdr_absolute_secondevaluationhsf_positive) + (ff_s_mce_mdr_absolute_secondevaluationhsf_positive))) /\ ff_s_mce_mdr_absolute_secondevaluationhsf_positive = ff_r_mce_mdr_absolute_secondevaluationhsf_positive + ff_a_mce_mdr_absolute_secondevaluationhsf_positive)))))) /\ (exists ff_u_mce_mdr_absolute_secondevaluationhsf_negative ff_v_mce_mdr_absolute_secondevaluationhsf_negative. ((((exists ff_h_mce_mdr_absolute_secondevaluationhsf_negative_start. ff_h_mce_mdr_absolute_secondevaluationhsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_absolute_secondevaluationhsf_negative)) /\ exists ff_q_mce_mdr_absolute_secondevaluationhsf_negative_start. ff_u_mce_mdr_absolute_secondevaluationhsf_negative = ff_q_mce_mdr_absolute_secondevaluationhsf_negative_start * S ((S (0)) * ff_v_mce_mdr_absolute_secondevaluationhsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_absolute_secondevaluationhsf_negative_terminal. ff_h_mce_mdr_absolute_secondevaluationhsf_negative_terminal + S (mdr_n_absolute_secondevaluationh) = S ((S ((S (mdr_q_absolute_secondevaluationhs)))) * ff_v_mce_mdr_absolute_secondevaluationhsf_negative)) /\ exists ff_q_mce_mdr_absolute_secondevaluationhsf_negative_terminal. ff_u_mce_mdr_absolute_secondevaluationhsf_negative = ff_q_mce_mdr_absolute_secondevaluationhsf_negative_terminal * S ((S ((S (mdr_q_absolute_secondevaluationhs)))) * ff_v_mce_mdr_absolute_secondevaluationhsf_negative) + (mdr_n_absolute_secondevaluationh))) /\ forall ff_i_mce_mdr_absolute_secondevaluationhsf_negative. (exists ff_lt_mce_mdr_absolute_secondevaluationhsf_negative_bound. ff_lt_mce_mdr_absolute_secondevaluationhsf_negative_bound + S ff_i_mce_mdr_absolute_secondevaluationhsf_negative = (S (mdr_q_absolute_secondevaluationhs))) -> exists ff_a_mce_mdr_absolute_secondevaluationhsf_negative ff_r_mce_mdr_absolute_secondevaluationhsf_negative ff_s_mce_mdr_absolute_secondevaluationhsf_negative. ((((exists ff_h_mce_mdr_absolute_secondevaluationhsf_negative_summand. ff_h_mce_mdr_absolute_secondevaluationhsf_negative_summand + S (ff_a_mce_mdr_absolute_secondevaluationhsf_negative) = S ((S (ff_i_mce_mdr_absolute_secondevaluationhsf_negative)) * ff_vc_mce_fold_mdr_absolute_secondevaluationhsf)) /\ exists ff_q_mce_mdr_absolute_secondevaluationhsf_negative_summand. ff_vb_mce_fold_mdr_absolute_secondevaluationhsf = ff_q_mce_mdr_absolute_secondevaluationhsf_negative_summand * S ((S (ff_i_mce_mdr_absolute_secondevaluationhsf_negative)) * ff_vc_mce_fold_mdr_absolute_secondevaluationhsf) + (ff_a_mce_mdr_absolute_secondevaluationhsf_negative))) /\ ((((exists ff_h_mce_mdr_absolute_secondevaluationhsf_negative_partial. ff_h_mce_mdr_absolute_secondevaluationhsf_negative_partial + S (ff_r_mce_mdr_absolute_secondevaluationhsf_negative) = S ((S (ff_i_mce_mdr_absolute_secondevaluationhsf_negative)) * ff_v_mce_mdr_absolute_secondevaluationhsf_negative)) /\ exists ff_q_mce_mdr_absolute_secondevaluationhsf_negative_partial. ff_u_mce_mdr_absolute_secondevaluationhsf_negative = ff_q_mce_mdr_absolute_secondevaluationhsf_negative_partial * S ((S (ff_i_mce_mdr_absolute_secondevaluationhsf_negative)) * ff_v_mce_mdr_absolute_secondevaluationhsf_negative) + (ff_r_mce_mdr_absolute_secondevaluationhsf_negative))) /\ ((((exists ff_h_mce_mdr_absolute_secondevaluationhsf_negative_successor. ff_h_mce_mdr_absolute_secondevaluationhsf_negative_successor + S (ff_s_mce_mdr_absolute_secondevaluationhsf_negative) = S ((S (S ff_i_mce_mdr_absolute_secondevaluationhsf_negative)) * ff_v_mce_mdr_absolute_secondevaluationhsf_negative)) /\ exists ff_q_mce_mdr_absolute_secondevaluationhsf_negative_successor. ff_u_mce_mdr_absolute_secondevaluationhsf_negative = ff_q_mce_mdr_absolute_secondevaluationhsf_negative_successor * S ((S (S ff_i_mce_mdr_absolute_secondevaluationhsf_negative)) * ff_v_mce_mdr_absolute_secondevaluationhsf_negative) + (ff_s_mce_mdr_absolute_secondevaluationhsf_negative))) /\ ff_s_mce_mdr_absolute_secondevaluationhsf_negative = ff_r_mce_mdr_absolute_secondevaluationhsf_negative + ff_a_mce_mdr_absolute_secondevaluationhsf_negative))))))))))))))) /\ ((exists mdr_gap_absolute_secondevaluationi. mdr_gap_absolute_secondevaluationi + S (mdr_i_absolute_secondevaluation) = (mdr_l_absolute_secondevaluation)) /\ (exists mdr_z_absolute_secondevaluationr. ((exists mdr_a_absolute_secondevaluationrc mdr_b_absolute_secondevaluationrc mdr_c_absolute_secondevaluationrc mdr_e_absolute_secondevaluationrc mdr_f_absolute_secondevaluationrc. ((mdr_a_absolute_secondevaluationrc = ((d) + (ab)) * S ((d) + (ab)) + ((ab) + (ab))) /\ ((mdr_b_absolute_secondevaluationrc = ((ac) + (bb)) * S ((ac) + (bb)) + ((bb) + (bb))) /\ ((mdr_c_absolute_secondevaluationrc = ((mdr_a_absolute_secondevaluationrc) + (mdr_b_absolute_secondevaluationrc)) * S ((mdr_a_absolute_secondevaluationrc) + (mdr_b_absolute_secondevaluationrc)) + ((mdr_b_absolute_secondevaluationrc) + (mdr_b_absolute_secondevaluationrc))) /\ ((mdr_e_absolute_secondevaluationrc = ((mdr_p_absolute_second) + (mdr_n_absolute_second)) * S ((mdr_p_absolute_second) + (mdr_n_absolute_second)) + ((mdr_n_absolute_second) + (mdr_n_absolute_second))) /\ ((mdr_f_absolute_secondevaluationrc = ((bc) + (mdr_e_absolute_secondevaluationrc)) * S ((bc) + (mdr_e_absolute_secondevaluationrc)) + ((mdr_e_absolute_secondevaluationrc) + (mdr_e_absolute_secondevaluationrc))) /\ ((mdr_z_absolute_secondevaluationr) = ((mdr_c_absolute_secondevaluationrc) + (mdr_f_absolute_secondevaluationrc)) * S ((mdr_c_absolute_secondevaluationrc) + (mdr_f_absolute_secondevaluationrc)) + ((mdr_f_absolute_secondevaluationrc) + (mdr_f_absolute_secondevaluationrc))))))))) /\ (((exists ff_h_mdr_absolute_secondevaluationrb. ff_h_mdr_absolute_secondevaluationrb + S (mdr_z_absolute_secondevaluationr) = S ((S (mdr_i_absolute_secondevaluation)) * mdr_c_absolute_secondevaluation)) /\ exists ff_q_mdr_absolute_secondevaluationrb. mdr_b_absolute_secondevaluation = ff_q_mdr_absolute_secondevaluationrb * S ((S (mdr_i_absolute_secondevaluation)) * mdr_c_absolute_secondevaluation) + (mdr_z_absolute_secondevaluationr)))))))) /\ (((mdr_p_absolute_second) = (mdr_n_absolute_second) + (E)) \/ ((mdr_n_absolute_second) = (mdr_p_absolute_second) + (E))))) -> D = E