absolute_recursive_determinant_integer_transport

Exact expanded first-order arithmetic statement

forall ab ac bb bc eb ec fb fc d D. (forall ics_index_absolute_parent_equality ics_value0_absolute_parent_equality ics_value1_absolute_parent_equality ics_value2_absolute_parent_equality ics_value3_absolute_parent_equality. (exists ics_gap_absolute_parent_equality_bound. ics_gap_absolute_parent_equality_bound + S (ics_index_absolute_parent_equality) = ((d) * (d))) -> (((exists fs_h_ics_absolute_parent_equality_at0. fs_h_ics_absolute_parent_equality_at0 + S (ics_value0_absolute_parent_equality) = S ((S (ics_index_absolute_parent_equality)) * ac)) /\ exists fs_q_ics_absolute_parent_equality_at0. ab = fs_q_ics_absolute_parent_equality_at0 * S ((S (ics_index_absolute_parent_equality)) * ac) + (ics_value0_absolute_parent_equality))) -> (((exists fs_h_ics_absolute_parent_equality_at1. fs_h_ics_absolute_parent_equality_at1 + S (ics_value1_absolute_parent_equality) = S ((S (ics_index_absolute_parent_equality)) * bc)) /\ exists fs_q_ics_absolute_parent_equality_at1. bb = fs_q_ics_absolute_parent_equality_at1 * S ((S (ics_index_absolute_parent_equality)) * bc) + (ics_value1_absolute_parent_equality))) -> (((exists fs_h_ics_absolute_parent_equality_at2. fs_h_ics_absolute_parent_equality_at2 + S (ics_value2_absolute_parent_equality) = S ((S (ics_index_absolute_parent_equality)) * ec)) /\ exists fs_q_ics_absolute_parent_equality_at2. eb = fs_q_ics_absolute_parent_equality_at2 * S ((S (ics_index_absolute_parent_equality)) * ec) + (ics_value2_absolute_parent_equality))) -> (((exists fs_h_ics_absolute_parent_equality_at3. fs_h_ics_absolute_parent_equality_at3 + S (ics_value3_absolute_parent_equality) = S ((S (ics_index_absolute_parent_equality)) * fc)) /\ exists fs_q_ics_absolute_parent_equality_at3. fb = fs_q_ics_absolute_parent_equality_at3 * S ((S (ics_index_absolute_parent_equality)) * fc) + (ics_value3_absolute_parent_equality))) -> ics_value0_absolute_parent_equality + ics_value3_absolute_parent_equality = ics_value2_absolute_parent_equality + ics_value1_absolute_parent_equality) -> (exists mdr_p_absolute_source mdr_n_absolute_source. ((exists mdr_b_absolute_sourceevaluation mdr_c_absolute_sourceevaluation mdr_l_absolute_sourceevaluation mdr_i_absolute_sourceevaluation. ((forall mdr_i_absolute_sourceevaluationh. (exists mdr_gap_absolute_sourceevaluationhi. mdr_gap_absolute_sourceevaluationhi + S (mdr_i_absolute_sourceevaluationh) = (mdr_l_absolute_sourceevaluation)) -> exists mdr_d_absolute_sourceevaluationh mdr_pb_absolute_sourceevaluationh mdr_pc_absolute_sourceevaluationh mdr_nb_absolute_sourceevaluationh mdr_nc_absolute_sourceevaluationh mdr_p_absolute_sourceevaluationh mdr_n_absolute_sourceevaluationh. ((exists mdr_z_absolute_sourceevaluationhr. ((exists mdr_a_absolute_sourceevaluationhrc mdr_b_absolute_sourceevaluationhrc mdr_c_absolute_sourceevaluationhrc mdr_e_absolute_sourceevaluationhrc mdr_f_absolute_sourceevaluationhrc. ((mdr_a_absolute_sourceevaluationhrc = ((mdr_d_absolute_sourceevaluationh) + (mdr_pb_absolute_sourceevaluationh)) * S ((mdr_d_absolute_sourceevaluationh) + (mdr_pb_absolute_sourceevaluationh)) + ((mdr_pb_absolute_sourceevaluationh) + (mdr_pb_absolute_sourceevaluationh))) /\ ((mdr_b_absolute_sourceevaluationhrc = ((mdr_pc_absolute_sourceevaluationh) + (mdr_nb_absolute_sourceevaluationh)) * S ((mdr_pc_absolute_sourceevaluationh) + (mdr_nb_absolute_sourceevaluationh)) + ((mdr_nb_absolute_sourceevaluationh) + (mdr_nb_absolute_sourceevaluationh))) /\ ((mdr_c_absolute_sourceevaluationhrc = ((mdr_a_absolute_sourceevaluationhrc) + (mdr_b_absolute_sourceevaluationhrc)) * S ((mdr_a_absolute_sourceevaluationhrc) + (mdr_b_absolute_sourceevaluationhrc)) + ((mdr_b_absolute_sourceevaluationhrc) + (mdr_b_absolute_sourceevaluationhrc))) /\ ((mdr_e_absolute_sourceevaluationhrc = ((mdr_p_absolute_sourceevaluationh) + (mdr_n_absolute_sourceevaluationh)) * S ((mdr_p_absolute_sourceevaluationh) + (mdr_n_absolute_sourceevaluationh)) + ((mdr_n_absolute_sourceevaluationh) + (mdr_n_absolute_sourceevaluationh))) /\ ((mdr_f_absolute_sourceevaluationhrc = ((mdr_nc_absolute_sourceevaluationh) + (mdr_e_absolute_sourceevaluationhrc)) * S ((mdr_nc_absolute_sourceevaluationh) + (mdr_e_absolute_sourceevaluationhrc)) + ((mdr_e_absolute_sourceevaluationhrc) + (mdr_e_absolute_sourceevaluationhrc))) /\ ((mdr_z_absolute_sourceevaluationhr) = ((mdr_c_absolute_sourceevaluationhrc) + (mdr_f_absolute_sourceevaluationhrc)) * S ((mdr_c_absolute_sourceevaluationhrc) + (mdr_f_absolute_sourceevaluationhrc)) + ((mdr_f_absolute_sourceevaluationhrc) + (mdr_f_absolute_sourceevaluationhrc))))))))) /\ (((exists ff_h_mdr_absolute_sourceevaluationhrb. ff_h_mdr_absolute_sourceevaluationhrb + S (mdr_z_absolute_sourceevaluationhr) = S ((S (mdr_i_absolute_sourceevaluationh)) * mdr_c_absolute_sourceevaluation)) /\ exists ff_q_mdr_absolute_sourceevaluationhrb. mdr_b_absolute_sourceevaluation = ff_q_mdr_absolute_sourceevaluationhrb * S ((S (mdr_i_absolute_sourceevaluationh)) * mdr_c_absolute_sourceevaluation) + (mdr_z_absolute_sourceevaluationhr))))) /\ (((((mdr_d_absolute_sourceevaluationh) = 0) /\ (((mdr_p_absolute_sourceevaluationh) = 1) /\ ((mdr_n_absolute_sourceevaluationh) = 0))) \/ exists mdr_q_absolute_sourceevaluationhs mdr_eb_absolute_sourceevaluationhs mdr_ec_absolute_sourceevaluationhs mdr_fb_absolute_sourceevaluationhs mdr_fc_absolute_sourceevaluationhs. (((mdr_d_absolute_sourceevaluationh) = S (mdr_q_absolute_sourceevaluationhs)) /\ ((forall mdr_j_absolute_sourceevaluationhsc. (exists mdr_gap_absolute_sourceevaluationhscj. mdr_gap_absolute_sourceevaluationhscj + S (mdr_j_absolute_sourceevaluationhsc) = (S (mdr_q_absolute_sourceevaluationhs))) -> exists mdr_i_absolute_sourceevaluationhsc mdr_up_absolute_sourceevaluationhsc mdr_us_absolute_sourceevaluationhsc mdr_un_absolute_sourceevaluationhsc mdr_ut_absolute_sourceevaluationhsc mdr_p_absolute_sourceevaluationhsc mdr_n_absolute_sourceevaluationhsc. ((exists mdr_gap_absolute_sourceevaluationhsci. mdr_gap_absolute_sourceevaluationhsci + S (mdr_i_absolute_sourceevaluationhsc) = (mdr_i_absolute_sourceevaluationh)) /\ ((exists mdr_z_absolute_sourceevaluationhscr. ((exists mdr_a_absolute_sourceevaluationhscrc mdr_b_absolute_sourceevaluationhscrc mdr_c_absolute_sourceevaluationhscrc mdr_e_absolute_sourceevaluationhscrc mdr_f_absolute_sourceevaluationhscrc. ((mdr_a_absolute_sourceevaluationhscrc = ((mdr_q_absolute_sourceevaluationhs) + (mdr_up_absolute_sourceevaluationhsc)) * S ((mdr_q_absolute_sourceevaluationhs) + (mdr_up_absolute_sourceevaluationhsc)) + ((mdr_up_absolute_sourceevaluationhsc) + (mdr_up_absolute_sourceevaluationhsc))) /\ ((mdr_b_absolute_sourceevaluationhscrc = ((mdr_us_absolute_sourceevaluationhsc) + (mdr_un_absolute_sourceevaluationhsc)) * S ((mdr_us_absolute_sourceevaluationhsc) + (mdr_un_absolute_sourceevaluationhsc)) + ((mdr_un_absolute_sourceevaluationhsc) + (mdr_un_absolute_sourceevaluationhsc))) /\ ((mdr_c_absolute_sourceevaluationhscrc = ((mdr_a_absolute_sourceevaluationhscrc) + (mdr_b_absolute_sourceevaluationhscrc)) * S ((mdr_a_absolute_sourceevaluationhscrc) + (mdr_b_absolute_sourceevaluationhscrc)) + ((mdr_b_absolute_sourceevaluationhscrc) + (mdr_b_absolute_sourceevaluationhscrc))) /\ ((mdr_e_absolute_sourceevaluationhscrc = ((mdr_p_absolute_sourceevaluationhsc) + (mdr_n_absolute_sourceevaluationhsc)) * S ((mdr_p_absolute_sourceevaluationhsc) + (mdr_n_absolute_sourceevaluationhsc)) + ((mdr_n_absolute_sourceevaluationhsc) + (mdr_n_absolute_sourceevaluationhsc))) /\ ((mdr_f_absolute_sourceevaluationhscrc = ((mdr_ut_absolute_sourceevaluationhsc) + (mdr_e_absolute_sourceevaluationhscrc)) * S ((mdr_ut_absolute_sourceevaluationhsc) + (mdr_e_absolute_sourceevaluationhscrc)) + ((mdr_e_absolute_sourceevaluationhscrc) + (mdr_e_absolute_sourceevaluationhscrc))) /\ ((mdr_z_absolute_sourceevaluationhscr) = ((mdr_c_absolute_sourceevaluationhscrc) + (mdr_f_absolute_sourceevaluationhscrc)) * S ((mdr_c_absolute_sourceevaluationhscrc) + (mdr_f_absolute_sourceevaluationhscrc)) + ((mdr_f_absolute_sourceevaluationhscrc) + (mdr_f_absolute_sourceevaluationhscrc))))))))) /\ (((exists ff_h_mdr_absolute_sourceevaluationhscrb. ff_h_mdr_absolute_sourceevaluationhscrb + S (mdr_z_absolute_sourceevaluationhscr) = S ((S (mdr_i_absolute_sourceevaluationhsc)) * mdr_c_absolute_sourceevaluation)) /\ exists ff_q_mdr_absolute_sourceevaluationhscrb. mdr_b_absolute_sourceevaluation = ff_q_mdr_absolute_sourceevaluationhscrb * S ((S (mdr_i_absolute_sourceevaluationhsc)) * mdr_c_absolute_sourceevaluation) + (mdr_z_absolute_sourceevaluationhscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_absolute_sourceevaluationhscm_positive. (exists ff_gap_mdm_lt_mdr_absolute_sourceevaluationhscm_positive_index_bound. ff_gap_mdm_lt_mdr_absolute_sourceevaluationhscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_absolute_sourceevaluationhscm_positive) = ((mdr_q_absolute_sourceevaluationhs) * (mdr_q_absolute_sourceevaluationhs))) -> exists ff_row_mdm_prefix_mdr_absolute_sourceevaluationhscm_positive ff_column_mdm_prefix_mdr_absolute_sourceevaluationhscm_positive ff_value_mdm_prefix_mdr_absolute_sourceevaluationhscm_positive. (ff_index_mdm_prefix_mdr_absolute_sourceevaluationhscm_positive = (mdr_q_absolute_sourceevaluationhs) * ff_row_mdm_prefix_mdr_absolute_sourceevaluationhscm_positive + ff_column_mdm_prefix_mdr_absolute_sourceevaluationhscm_positive /\ ((exists ff_gap_mdm_lt_mdr_absolute_sourceevaluationhscm_positive_column_bound. ff_gap_mdm_lt_mdr_absolute_sourceevaluationhscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_absolute_sourceevaluationhscm_positive) = (mdr_q_absolute_sourceevaluationhs)) /\ ((exists ff_row_mdm_cell_mdr_absolute_sourceevaluationhscm_positive_cell ff_column_mdm_cell_mdr_absolute_sourceevaluationhscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_absolute_sourceevaluationhscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_absolute_sourceevaluationhscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_absolute_sourceevaluationhscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_absolute_sourceevaluationhscm_positive_cell = ff_row_mdm_prefix_mdr_absolute_sourceevaluationhscm_positive) \/ ((exists ff_gap_mdm_le_mdr_absolute_sourceevaluationhscm_positive_cell_row_after. ff_gap_mdm_le_mdr_absolute_sourceevaluationhscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_absolute_sourceevaluationhscm_positive)) /\ ff_row_mdm_cell_mdr_absolute_sourceevaluationhscm_positive_cell = S ff_row_mdm_prefix_mdr_absolute_sourceevaluationhscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_absolute_sourceevaluationhscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_absolute_sourceevaluationhscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_absolute_sourceevaluationhscm_positive) = (mdr_j_absolute_sourceevaluationhsc)) /\ ff_column_mdm_cell_mdr_absolute_sourceevaluationhscm_positive_cell = ff_column_mdm_prefix_mdr_absolute_sourceevaluationhscm_positive) \/ ((exists ff_gap_mdm_le_mdr_absolute_sourceevaluationhscm_positive_cell_column_after. ff_gap_mdm_le_mdr_absolute_sourceevaluationhscm_positive_cell_column_after + (mdr_j_absolute_sourceevaluationhsc) = (ff_column_mdm_prefix_mdr_absolute_sourceevaluationhscm_positive)) /\ ff_column_mdm_cell_mdr_absolute_sourceevaluationhscm_positive_cell = S ff_column_mdm_prefix_mdr_absolute_sourceevaluationhscm_positive))) /\ (((exists ff_h_mdm_mdr_absolute_sourceevaluationhscm_positive_cell_source. ff_h_mdm_mdr_absolute_sourceevaluationhscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_absolute_sourceevaluationhscm_positive) = S ((S ((ff_row_mdm_cell_mdr_absolute_sourceevaluationhscm_positive_cell) * (S (mdr_q_absolute_sourceevaluationhs)) + (ff_column_mdm_cell_mdr_absolute_sourceevaluationhscm_positive_cell))) * mdr_pc_absolute_sourceevaluationh)) /\ exists ff_q_mdm_mdr_absolute_sourceevaluationhscm_positive_cell_source. mdr_pb_absolute_sourceevaluationh = ff_q_mdm_mdr_absolute_sourceevaluationhscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_absolute_sourceevaluationhscm_positive_cell) * (S (mdr_q_absolute_sourceevaluationhs)) + (ff_column_mdm_cell_mdr_absolute_sourceevaluationhscm_positive_cell))) * mdr_pc_absolute_sourceevaluationh) + (ff_value_mdm_prefix_mdr_absolute_sourceevaluationhscm_positive)))))) /\ (((exists ff_h_mdm_mdr_absolute_sourceevaluationhscm_positive_target. ff_h_mdm_mdr_absolute_sourceevaluationhscm_positive_target + S (ff_value_mdm_prefix_mdr_absolute_sourceevaluationhscm_positive) = S ((S (ff_index_mdm_prefix_mdr_absolute_sourceevaluationhscm_positive)) * mdr_us_absolute_sourceevaluationhsc)) /\ exists ff_q_mdm_mdr_absolute_sourceevaluationhscm_positive_target. mdr_up_absolute_sourceevaluationhsc = ff_q_mdm_mdr_absolute_sourceevaluationhscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_absolute_sourceevaluationhscm_positive)) * mdr_us_absolute_sourceevaluationhsc) + (ff_value_mdm_prefix_mdr_absolute_sourceevaluationhscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_absolute_sourceevaluationhscm_negative. (exists ff_gap_mdm_lt_mdr_absolute_sourceevaluationhscm_negative_index_bound. ff_gap_mdm_lt_mdr_absolute_sourceevaluationhscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_absolute_sourceevaluationhscm_negative) = ((mdr_q_absolute_sourceevaluationhs) * (mdr_q_absolute_sourceevaluationhs))) -> exists ff_row_mdm_prefix_mdr_absolute_sourceevaluationhscm_negative ff_column_mdm_prefix_mdr_absolute_sourceevaluationhscm_negative ff_value_mdm_prefix_mdr_absolute_sourceevaluationhscm_negative. (ff_index_mdm_prefix_mdr_absolute_sourceevaluationhscm_negative = (mdr_q_absolute_sourceevaluationhs) * ff_row_mdm_prefix_mdr_absolute_sourceevaluationhscm_negative + ff_column_mdm_prefix_mdr_absolute_sourceevaluationhscm_negative /\ ((exists ff_gap_mdm_lt_mdr_absolute_sourceevaluationhscm_negative_column_bound. ff_gap_mdm_lt_mdr_absolute_sourceevaluationhscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_absolute_sourceevaluationhscm_negative) = (mdr_q_absolute_sourceevaluationhs)) /\ ((exists ff_row_mdm_cell_mdr_absolute_sourceevaluationhscm_negative_cell ff_column_mdm_cell_mdr_absolute_sourceevaluationhscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_absolute_sourceevaluationhscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_absolute_sourceevaluationhscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_absolute_sourceevaluationhscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_absolute_sourceevaluationhscm_negative_cell = ff_row_mdm_prefix_mdr_absolute_sourceevaluationhscm_negative) \/ ((exists ff_gap_mdm_le_mdr_absolute_sourceevaluationhscm_negative_cell_row_after. ff_gap_mdm_le_mdr_absolute_sourceevaluationhscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_absolute_sourceevaluationhscm_negative)) /\ ff_row_mdm_cell_mdr_absolute_sourceevaluationhscm_negative_cell = S ff_row_mdm_prefix_mdr_absolute_sourceevaluationhscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_absolute_sourceevaluationhscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_absolute_sourceevaluationhscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_absolute_sourceevaluationhscm_negative) = (mdr_j_absolute_sourceevaluationhsc)) /\ ff_column_mdm_cell_mdr_absolute_sourceevaluationhscm_negative_cell = ff_column_mdm_prefix_mdr_absolute_sourceevaluationhscm_negative) \/ ((exists ff_gap_mdm_le_mdr_absolute_sourceevaluationhscm_negative_cell_column_after. ff_gap_mdm_le_mdr_absolute_sourceevaluationhscm_negative_cell_column_after + (mdr_j_absolute_sourceevaluationhsc) = (ff_column_mdm_prefix_mdr_absolute_sourceevaluationhscm_negative)) /\ ff_column_mdm_cell_mdr_absolute_sourceevaluationhscm_negative_cell = S ff_column_mdm_prefix_mdr_absolute_sourceevaluationhscm_negative))) /\ (((exists ff_h_mdm_mdr_absolute_sourceevaluationhscm_negative_cell_source. ff_h_mdm_mdr_absolute_sourceevaluationhscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_absolute_sourceevaluationhscm_negative) = S ((S ((ff_row_mdm_cell_mdr_absolute_sourceevaluationhscm_negative_cell) * (S (mdr_q_absolute_sourceevaluationhs)) + (ff_column_mdm_cell_mdr_absolute_sourceevaluationhscm_negative_cell))) * mdr_nc_absolute_sourceevaluationh)) /\ exists ff_q_mdm_mdr_absolute_sourceevaluationhscm_negative_cell_source. mdr_nb_absolute_sourceevaluationh = ff_q_mdm_mdr_absolute_sourceevaluationhscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_absolute_sourceevaluationhscm_negative_cell) * (S (mdr_q_absolute_sourceevaluationhs)) + (ff_column_mdm_cell_mdr_absolute_sourceevaluationhscm_negative_cell))) * mdr_nc_absolute_sourceevaluationh) + (ff_value_mdm_prefix_mdr_absolute_sourceevaluationhscm_negative)))))) /\ (((exists ff_h_mdm_mdr_absolute_sourceevaluationhscm_negative_target. ff_h_mdm_mdr_absolute_sourceevaluationhscm_negative_target + S (ff_value_mdm_prefix_mdr_absolute_sourceevaluationhscm_negative) = S ((S (ff_index_mdm_prefix_mdr_absolute_sourceevaluationhscm_negative)) * mdr_ut_absolute_sourceevaluationhsc)) /\ exists ff_q_mdm_mdr_absolute_sourceevaluationhscm_negative_target. mdr_un_absolute_sourceevaluationhsc = ff_q_mdm_mdr_absolute_sourceevaluationhscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_absolute_sourceevaluationhscm_negative)) * mdr_ut_absolute_sourceevaluationhsc) + (ff_value_mdm_prefix_mdr_absolute_sourceevaluationhscm_negative))))))))) /\ ((((exists ff_h_mdr_absolute_sourceevaluationhscp. ff_h_mdr_absolute_sourceevaluationhscp + S (mdr_p_absolute_sourceevaluationhsc) = S ((S (mdr_j_absolute_sourceevaluationhsc)) * mdr_ec_absolute_sourceevaluationhs)) /\ exists ff_q_mdr_absolute_sourceevaluationhscp. mdr_eb_absolute_sourceevaluationhs = ff_q_mdr_absolute_sourceevaluationhscp * S ((S (mdr_j_absolute_sourceevaluationhsc)) * mdr_ec_absolute_sourceevaluationhs) + (mdr_p_absolute_sourceevaluationhsc))) /\ (((exists ff_h_mdr_absolute_sourceevaluationhscn. ff_h_mdr_absolute_sourceevaluationhscn + S (mdr_n_absolute_sourceevaluationhsc) = S ((S (mdr_j_absolute_sourceevaluationhsc)) * mdr_fc_absolute_sourceevaluationhs)) /\ exists ff_q_mdr_absolute_sourceevaluationhscn. mdr_fb_absolute_sourceevaluationhs = ff_q_mdr_absolute_sourceevaluationhscn * S ((S (mdr_j_absolute_sourceevaluationhsc)) * mdr_fc_absolute_sourceevaluationhs) + (mdr_n_absolute_sourceevaluationhsc)))))))) /\ (exists ff_ub_mce_fold_mdr_absolute_sourceevaluationhsf ff_uc_mce_fold_mdr_absolute_sourceevaluationhsf ff_vb_mce_fold_mdr_absolute_sourceevaluationhsf ff_vc_mce_fold_mdr_absolute_sourceevaluationhsf. ((forall ff_index_mce_alternating_mdr_absolute_sourceevaluationhsf_prefix. (exists ff_gap_mce_mdr_absolute_sourceevaluationhsf_prefix_index. ff_gap_mce_mdr_absolute_sourceevaluationhsf_prefix_index + S (ff_index_mce_alternating_mdr_absolute_sourceevaluationhsf_prefix) = (S (mdr_q_absolute_sourceevaluationhs))) -> exists ff_ap_mce_alternating_mdr_absolute_sourceevaluationhsf_prefix ff_an_mce_alternating_mdr_absolute_sourceevaluationhsf_prefix ff_bp_mce_alternating_mdr_absolute_sourceevaluationhsf_prefix ff_bn_mce_alternating_mdr_absolute_sourceevaluationhsf_prefix ff_p_mce_alternating_mdr_absolute_sourceevaluationhsf_prefix ff_n_mce_alternating_mdr_absolute_sourceevaluationhsf_prefix. ((((exists ff_h_mce_mdr_absolute_sourceevaluationhsf_prefix_ap. ff_h_mce_mdr_absolute_sourceevaluationhsf_prefix_ap + S (ff_ap_mce_alternating_mdr_absolute_sourceevaluationhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_absolute_sourceevaluationhsf_prefix)) * mdr_pc_absolute_sourceevaluationh)) /\ exists ff_q_mce_mdr_absolute_sourceevaluationhsf_prefix_ap. mdr_pb_absolute_sourceevaluationh = ff_q_mce_mdr_absolute_sourceevaluationhsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_absolute_sourceevaluationhsf_prefix)) * mdr_pc_absolute_sourceevaluationh) + (ff_ap_mce_alternating_mdr_absolute_sourceevaluationhsf_prefix))) /\ ((((exists ff_h_mce_mdr_absolute_sourceevaluationhsf_prefix_an. ff_h_mce_mdr_absolute_sourceevaluationhsf_prefix_an + S (ff_an_mce_alternating_mdr_absolute_sourceevaluationhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_absolute_sourceevaluationhsf_prefix)) * mdr_nc_absolute_sourceevaluationh)) /\ exists ff_q_mce_mdr_absolute_sourceevaluationhsf_prefix_an. mdr_nb_absolute_sourceevaluationh = ff_q_mce_mdr_absolute_sourceevaluationhsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_absolute_sourceevaluationhsf_prefix)) * mdr_nc_absolute_sourceevaluationh) + (ff_an_mce_alternating_mdr_absolute_sourceevaluationhsf_prefix))) /\ ((((exists ff_h_mce_mdr_absolute_sourceevaluationhsf_prefix_bp. ff_h_mce_mdr_absolute_sourceevaluationhsf_prefix_bp + S (ff_bp_mce_alternating_mdr_absolute_sourceevaluationhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_absolute_sourceevaluationhsf_prefix)) * mdr_ec_absolute_sourceevaluationhs)) /\ exists ff_q_mce_mdr_absolute_sourceevaluationhsf_prefix_bp. mdr_eb_absolute_sourceevaluationhs = ff_q_mce_mdr_absolute_sourceevaluationhsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_absolute_sourceevaluationhsf_prefix)) * mdr_ec_absolute_sourceevaluationhs) + (ff_bp_mce_alternating_mdr_absolute_sourceevaluationhsf_prefix))) /\ ((((exists ff_h_mce_mdr_absolute_sourceevaluationhsf_prefix_bn. ff_h_mce_mdr_absolute_sourceevaluationhsf_prefix_bn + S (ff_bn_mce_alternating_mdr_absolute_sourceevaluationhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_absolute_sourceevaluationhsf_prefix)) * mdr_fc_absolute_sourceevaluationhs)) /\ exists ff_q_mce_mdr_absolute_sourceevaluationhsf_prefix_bn. mdr_fb_absolute_sourceevaluationhs = ff_q_mce_mdr_absolute_sourceevaluationhsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_absolute_sourceevaluationhsf_prefix)) * mdr_fc_absolute_sourceevaluationhs) + (ff_bn_mce_alternating_mdr_absolute_sourceevaluationhsf_prefix))) /\ ((((exists ff_h_mce_mdr_absolute_sourceevaluationhsf_prefix_positive. ff_h_mce_mdr_absolute_sourceevaluationhsf_prefix_positive + S (ff_p_mce_alternating_mdr_absolute_sourceevaluationhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_absolute_sourceevaluationhsf_prefix)) * ff_uc_mce_fold_mdr_absolute_sourceevaluationhsf)) /\ exists ff_q_mce_mdr_absolute_sourceevaluationhsf_prefix_positive. ff_ub_mce_fold_mdr_absolute_sourceevaluationhsf = ff_q_mce_mdr_absolute_sourceevaluationhsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_absolute_sourceevaluationhsf_prefix)) * ff_uc_mce_fold_mdr_absolute_sourceevaluationhsf) + (ff_p_mce_alternating_mdr_absolute_sourceevaluationhsf_prefix))) /\ ((((exists ff_h_mce_mdr_absolute_sourceevaluationhsf_prefix_negative. ff_h_mce_mdr_absolute_sourceevaluationhsf_prefix_negative + S (ff_n_mce_alternating_mdr_absolute_sourceevaluationhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_absolute_sourceevaluationhsf_prefix)) * ff_vc_mce_fold_mdr_absolute_sourceevaluationhsf)) /\ exists ff_q_mce_mdr_absolute_sourceevaluationhsf_prefix_negative. ff_vb_mce_fold_mdr_absolute_sourceevaluationhsf = ff_q_mce_mdr_absolute_sourceevaluationhsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_absolute_sourceevaluationhsf_prefix)) * ff_vc_mce_fold_mdr_absolute_sourceevaluationhsf) + (ff_n_mce_alternating_mdr_absolute_sourceevaluationhsf_prefix))) /\ (((exists ff_even_mce_term_mdr_absolute_sourceevaluationhsf_prefix_term. ff_index_mce_alternating_mdr_absolute_sourceevaluationhsf_prefix = 2 * ff_even_mce_term_mdr_absolute_sourceevaluationhsf_prefix_term) /\ (ff_p_mce_alternating_mdr_absolute_sourceevaluationhsf_prefix = (ff_ap_mce_alternating_mdr_absolute_sourceevaluationhsf_prefix) * (ff_bp_mce_alternating_mdr_absolute_sourceevaluationhsf_prefix) + (ff_an_mce_alternating_mdr_absolute_sourceevaluationhsf_prefix) * (ff_bn_mce_alternating_mdr_absolute_sourceevaluationhsf_prefix) /\ ff_n_mce_alternating_mdr_absolute_sourceevaluationhsf_prefix = (ff_ap_mce_alternating_mdr_absolute_sourceevaluationhsf_prefix) * (ff_bn_mce_alternating_mdr_absolute_sourceevaluationhsf_prefix) + (ff_an_mce_alternating_mdr_absolute_sourceevaluationhsf_prefix) * (ff_bp_mce_alternating_mdr_absolute_sourceevaluationhsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_absolute_sourceevaluationhsf_prefix_term. ff_index_mce_alternating_mdr_absolute_sourceevaluationhsf_prefix = 2 * ff_odd_mce_term_mdr_absolute_sourceevaluationhsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_absolute_sourceevaluationhsf_prefix = (ff_ap_mce_alternating_mdr_absolute_sourceevaluationhsf_prefix) * (ff_bn_mce_alternating_mdr_absolute_sourceevaluationhsf_prefix) + (ff_an_mce_alternating_mdr_absolute_sourceevaluationhsf_prefix) * (ff_bp_mce_alternating_mdr_absolute_sourceevaluationhsf_prefix) /\ ff_n_mce_alternating_mdr_absolute_sourceevaluationhsf_prefix = (ff_ap_mce_alternating_mdr_absolute_sourceevaluationhsf_prefix) * (ff_bp_mce_alternating_mdr_absolute_sourceevaluationhsf_prefix) + (ff_an_mce_alternating_mdr_absolute_sourceevaluationhsf_prefix) * (ff_bn_mce_alternating_mdr_absolute_sourceevaluationhsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_absolute_sourceevaluationhsf_positive ff_v_mce_mdr_absolute_sourceevaluationhsf_positive. ((((exists ff_h_mce_mdr_absolute_sourceevaluationhsf_positive_start. ff_h_mce_mdr_absolute_sourceevaluationhsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_absolute_sourceevaluationhsf_positive)) /\ exists ff_q_mce_mdr_absolute_sourceevaluationhsf_positive_start. ff_u_mce_mdr_absolute_sourceevaluationhsf_positive = ff_q_mce_mdr_absolute_sourceevaluationhsf_positive_start * S ((S (0)) * ff_v_mce_mdr_absolute_sourceevaluationhsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_absolute_sourceevaluationhsf_positive_terminal. ff_h_mce_mdr_absolute_sourceevaluationhsf_positive_terminal + S (mdr_p_absolute_sourceevaluationh) = S ((S ((S (mdr_q_absolute_sourceevaluationhs)))) * ff_v_mce_mdr_absolute_sourceevaluationhsf_positive)) /\ exists ff_q_mce_mdr_absolute_sourceevaluationhsf_positive_terminal. ff_u_mce_mdr_absolute_sourceevaluationhsf_positive = ff_q_mce_mdr_absolute_sourceevaluationhsf_positive_terminal * S ((S ((S (mdr_q_absolute_sourceevaluationhs)))) * ff_v_mce_mdr_absolute_sourceevaluationhsf_positive) + (mdr_p_absolute_sourceevaluationh))) /\ forall ff_i_mce_mdr_absolute_sourceevaluationhsf_positive. (exists ff_lt_mce_mdr_absolute_sourceevaluationhsf_positive_bound. ff_lt_mce_mdr_absolute_sourceevaluationhsf_positive_bound + S ff_i_mce_mdr_absolute_sourceevaluationhsf_positive = (S (mdr_q_absolute_sourceevaluationhs))) -> exists ff_a_mce_mdr_absolute_sourceevaluationhsf_positive ff_r_mce_mdr_absolute_sourceevaluationhsf_positive ff_s_mce_mdr_absolute_sourceevaluationhsf_positive. ((((exists ff_h_mce_mdr_absolute_sourceevaluationhsf_positive_summand. ff_h_mce_mdr_absolute_sourceevaluationhsf_positive_summand + S (ff_a_mce_mdr_absolute_sourceevaluationhsf_positive) = S ((S (ff_i_mce_mdr_absolute_sourceevaluationhsf_positive)) * ff_uc_mce_fold_mdr_absolute_sourceevaluationhsf)) /\ exists ff_q_mce_mdr_absolute_sourceevaluationhsf_positive_summand. ff_ub_mce_fold_mdr_absolute_sourceevaluationhsf = ff_q_mce_mdr_absolute_sourceevaluationhsf_positive_summand * S ((S (ff_i_mce_mdr_absolute_sourceevaluationhsf_positive)) * ff_uc_mce_fold_mdr_absolute_sourceevaluationhsf) + (ff_a_mce_mdr_absolute_sourceevaluationhsf_positive))) /\ ((((exists ff_h_mce_mdr_absolute_sourceevaluationhsf_positive_partial. ff_h_mce_mdr_absolute_sourceevaluationhsf_positive_partial + S (ff_r_mce_mdr_absolute_sourceevaluationhsf_positive) = S ((S (ff_i_mce_mdr_absolute_sourceevaluationhsf_positive)) * ff_v_mce_mdr_absolute_sourceevaluationhsf_positive)) /\ exists ff_q_mce_mdr_absolute_sourceevaluationhsf_positive_partial. ff_u_mce_mdr_absolute_sourceevaluationhsf_positive = ff_q_mce_mdr_absolute_sourceevaluationhsf_positive_partial * S ((S (ff_i_mce_mdr_absolute_sourceevaluationhsf_positive)) * ff_v_mce_mdr_absolute_sourceevaluationhsf_positive) + (ff_r_mce_mdr_absolute_sourceevaluationhsf_positive))) /\ ((((exists ff_h_mce_mdr_absolute_sourceevaluationhsf_positive_successor. ff_h_mce_mdr_absolute_sourceevaluationhsf_positive_successor + S (ff_s_mce_mdr_absolute_sourceevaluationhsf_positive) = S ((S (S ff_i_mce_mdr_absolute_sourceevaluationhsf_positive)) * ff_v_mce_mdr_absolute_sourceevaluationhsf_positive)) /\ exists ff_q_mce_mdr_absolute_sourceevaluationhsf_positive_successor. ff_u_mce_mdr_absolute_sourceevaluationhsf_positive = ff_q_mce_mdr_absolute_sourceevaluationhsf_positive_successor * S ((S (S ff_i_mce_mdr_absolute_sourceevaluationhsf_positive)) * ff_v_mce_mdr_absolute_sourceevaluationhsf_positive) + (ff_s_mce_mdr_absolute_sourceevaluationhsf_positive))) /\ ff_s_mce_mdr_absolute_sourceevaluationhsf_positive = ff_r_mce_mdr_absolute_sourceevaluationhsf_positive + ff_a_mce_mdr_absolute_sourceevaluationhsf_positive)))))) /\ (exists ff_u_mce_mdr_absolute_sourceevaluationhsf_negative ff_v_mce_mdr_absolute_sourceevaluationhsf_negative. ((((exists ff_h_mce_mdr_absolute_sourceevaluationhsf_negative_start. ff_h_mce_mdr_absolute_sourceevaluationhsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_absolute_sourceevaluationhsf_negative)) /\ exists ff_q_mce_mdr_absolute_sourceevaluationhsf_negative_start. ff_u_mce_mdr_absolute_sourceevaluationhsf_negative = ff_q_mce_mdr_absolute_sourceevaluationhsf_negative_start * S ((S (0)) * ff_v_mce_mdr_absolute_sourceevaluationhsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_absolute_sourceevaluationhsf_negative_terminal. ff_h_mce_mdr_absolute_sourceevaluationhsf_negative_terminal + S (mdr_n_absolute_sourceevaluationh) = S ((S ((S (mdr_q_absolute_sourceevaluationhs)))) * ff_v_mce_mdr_absolute_sourceevaluationhsf_negative)) /\ exists ff_q_mce_mdr_absolute_sourceevaluationhsf_negative_terminal. ff_u_mce_mdr_absolute_sourceevaluationhsf_negative = ff_q_mce_mdr_absolute_sourceevaluationhsf_negative_terminal * S ((S ((S (mdr_q_absolute_sourceevaluationhs)))) * ff_v_mce_mdr_absolute_sourceevaluationhsf_negative) + (mdr_n_absolute_sourceevaluationh))) /\ forall ff_i_mce_mdr_absolute_sourceevaluationhsf_negative. (exists ff_lt_mce_mdr_absolute_sourceevaluationhsf_negative_bound. ff_lt_mce_mdr_absolute_sourceevaluationhsf_negative_bound + S ff_i_mce_mdr_absolute_sourceevaluationhsf_negative = (S (mdr_q_absolute_sourceevaluationhs))) -> exists ff_a_mce_mdr_absolute_sourceevaluationhsf_negative ff_r_mce_mdr_absolute_sourceevaluationhsf_negative ff_s_mce_mdr_absolute_sourceevaluationhsf_negative. ((((exists ff_h_mce_mdr_absolute_sourceevaluationhsf_negative_summand. ff_h_mce_mdr_absolute_sourceevaluationhsf_negative_summand + S (ff_a_mce_mdr_absolute_sourceevaluationhsf_negative) = S ((S (ff_i_mce_mdr_absolute_sourceevaluationhsf_negative)) * ff_vc_mce_fold_mdr_absolute_sourceevaluationhsf)) /\ exists ff_q_mce_mdr_absolute_sourceevaluationhsf_negative_summand. ff_vb_mce_fold_mdr_absolute_sourceevaluationhsf = ff_q_mce_mdr_absolute_sourceevaluationhsf_negative_summand * S ((S (ff_i_mce_mdr_absolute_sourceevaluationhsf_negative)) * ff_vc_mce_fold_mdr_absolute_sourceevaluationhsf) + (ff_a_mce_mdr_absolute_sourceevaluationhsf_negative))) /\ ((((exists ff_h_mce_mdr_absolute_sourceevaluationhsf_negative_partial. ff_h_mce_mdr_absolute_sourceevaluationhsf_negative_partial + S (ff_r_mce_mdr_absolute_sourceevaluationhsf_negative) = S ((S (ff_i_mce_mdr_absolute_sourceevaluationhsf_negative)) * ff_v_mce_mdr_absolute_sourceevaluationhsf_negative)) /\ exists ff_q_mce_mdr_absolute_sourceevaluationhsf_negative_partial. ff_u_mce_mdr_absolute_sourceevaluationhsf_negative = ff_q_mce_mdr_absolute_sourceevaluationhsf_negative_partial * S ((S (ff_i_mce_mdr_absolute_sourceevaluationhsf_negative)) * ff_v_mce_mdr_absolute_sourceevaluationhsf_negative) + (ff_r_mce_mdr_absolute_sourceevaluationhsf_negative))) /\ ((((exists ff_h_mce_mdr_absolute_sourceevaluationhsf_negative_successor. ff_h_mce_mdr_absolute_sourceevaluationhsf_negative_successor + S (ff_s_mce_mdr_absolute_sourceevaluationhsf_negative) = S ((S (S ff_i_mce_mdr_absolute_sourceevaluationhsf_negative)) * ff_v_mce_mdr_absolute_sourceevaluationhsf_negative)) /\ exists ff_q_mce_mdr_absolute_sourceevaluationhsf_negative_successor. ff_u_mce_mdr_absolute_sourceevaluationhsf_negative = ff_q_mce_mdr_absolute_sourceevaluationhsf_negative_successor * S ((S (S ff_i_mce_mdr_absolute_sourceevaluationhsf_negative)) * ff_v_mce_mdr_absolute_sourceevaluationhsf_negative) + (ff_s_mce_mdr_absolute_sourceevaluationhsf_negative))) /\ ff_s_mce_mdr_absolute_sourceevaluationhsf_negative = ff_r_mce_mdr_absolute_sourceevaluationhsf_negative + ff_a_mce_mdr_absolute_sourceevaluationhsf_negative))))))))))))))) /\ ((exists mdr_gap_absolute_sourceevaluationi. mdr_gap_absolute_sourceevaluationi + S (mdr_i_absolute_sourceevaluation) = (mdr_l_absolute_sourceevaluation)) /\ (exists mdr_z_absolute_sourceevaluationr. ((exists mdr_a_absolute_sourceevaluationrc mdr_b_absolute_sourceevaluationrc mdr_c_absolute_sourceevaluationrc mdr_e_absolute_sourceevaluationrc mdr_f_absolute_sourceevaluationrc. ((mdr_a_absolute_sourceevaluationrc = ((d) + (ab)) * S ((d) + (ab)) + ((ab) + (ab))) /\ ((mdr_b_absolute_sourceevaluationrc = ((ac) + (bb)) * S ((ac) + (bb)) + ((bb) + (bb))) /\ ((mdr_c_absolute_sourceevaluationrc = ((mdr_a_absolute_sourceevaluationrc) + (mdr_b_absolute_sourceevaluationrc)) * S ((mdr_a_absolute_sourceevaluationrc) + (mdr_b_absolute_sourceevaluationrc)) + ((mdr_b_absolute_sourceevaluationrc) + (mdr_b_absolute_sourceevaluationrc))) /\ ((mdr_e_absolute_sourceevaluationrc = ((mdr_p_absolute_source) + (mdr_n_absolute_source)) * S ((mdr_p_absolute_source) + (mdr_n_absolute_source)) + ((mdr_n_absolute_source) + (mdr_n_absolute_source))) /\ ((mdr_f_absolute_sourceevaluationrc = ((bc) + (mdr_e_absolute_sourceevaluationrc)) * S ((bc) + (mdr_e_absolute_sourceevaluationrc)) + ((mdr_e_absolute_sourceevaluationrc) + (mdr_e_absolute_sourceevaluationrc))) /\ ((mdr_z_absolute_sourceevaluationr) = ((mdr_c_absolute_sourceevaluationrc) + (mdr_f_absolute_sourceevaluationrc)) * S ((mdr_c_absolute_sourceevaluationrc) + (mdr_f_absolute_sourceevaluationrc)) + ((mdr_f_absolute_sourceevaluationrc) + (mdr_f_absolute_sourceevaluationrc))))))))) /\ (((exists ff_h_mdr_absolute_sourceevaluationrb. ff_h_mdr_absolute_sourceevaluationrb + S (mdr_z_absolute_sourceevaluationr) = S ((S (mdr_i_absolute_sourceevaluation)) * mdr_c_absolute_sourceevaluation)) /\ exists ff_q_mdr_absolute_sourceevaluationrb. mdr_b_absolute_sourceevaluation = ff_q_mdr_absolute_sourceevaluationrb * S ((S (mdr_i_absolute_sourceevaluation)) * mdr_c_absolute_sourceevaluation) + (mdr_z_absolute_sourceevaluationr)))))))) /\ (((mdr_p_absolute_source) = (mdr_n_absolute_source) + (D)) \/ ((mdr_n_absolute_source) = (mdr_p_absolute_source) + (D))))) -> (exists mdr_p_absolute_target mdr_n_absolute_target. ((exists mdr_b_absolute_targetevaluation mdr_c_absolute_targetevaluation mdr_l_absolute_targetevaluation mdr_i_absolute_targetevaluation. ((forall mdr_i_absolute_targetevaluationh. (exists mdr_gap_absolute_targetevaluationhi. mdr_gap_absolute_targetevaluationhi + S (mdr_i_absolute_targetevaluationh) = (mdr_l_absolute_targetevaluation)) -> exists mdr_d_absolute_targetevaluationh mdr_pb_absolute_targetevaluationh mdr_pc_absolute_targetevaluationh mdr_nb_absolute_targetevaluationh mdr_nc_absolute_targetevaluationh mdr_p_absolute_targetevaluationh mdr_n_absolute_targetevaluationh. ((exists mdr_z_absolute_targetevaluationhr. ((exists mdr_a_absolute_targetevaluationhrc mdr_b_absolute_targetevaluationhrc mdr_c_absolute_targetevaluationhrc mdr_e_absolute_targetevaluationhrc mdr_f_absolute_targetevaluationhrc. ((mdr_a_absolute_targetevaluationhrc = ((mdr_d_absolute_targetevaluationh) + (mdr_pb_absolute_targetevaluationh)) * S ((mdr_d_absolute_targetevaluationh) + (mdr_pb_absolute_targetevaluationh)) + ((mdr_pb_absolute_targetevaluationh) + (mdr_pb_absolute_targetevaluationh))) /\ ((mdr_b_absolute_targetevaluationhrc = ((mdr_pc_absolute_targetevaluationh) + (mdr_nb_absolute_targetevaluationh)) * S ((mdr_pc_absolute_targetevaluationh) + (mdr_nb_absolute_targetevaluationh)) + ((mdr_nb_absolute_targetevaluationh) + (mdr_nb_absolute_targetevaluationh))) /\ ((mdr_c_absolute_targetevaluationhrc = ((mdr_a_absolute_targetevaluationhrc) + (mdr_b_absolute_targetevaluationhrc)) * S ((mdr_a_absolute_targetevaluationhrc) + (mdr_b_absolute_targetevaluationhrc)) + ((mdr_b_absolute_targetevaluationhrc) + (mdr_b_absolute_targetevaluationhrc))) /\ ((mdr_e_absolute_targetevaluationhrc = ((mdr_p_absolute_targetevaluationh) + (mdr_n_absolute_targetevaluationh)) * S ((mdr_p_absolute_targetevaluationh) + (mdr_n_absolute_targetevaluationh)) + ((mdr_n_absolute_targetevaluationh) + (mdr_n_absolute_targetevaluationh))) /\ ((mdr_f_absolute_targetevaluationhrc = ((mdr_nc_absolute_targetevaluationh) + (mdr_e_absolute_targetevaluationhrc)) * S ((mdr_nc_absolute_targetevaluationh) + (mdr_e_absolute_targetevaluationhrc)) + ((mdr_e_absolute_targetevaluationhrc) + (mdr_e_absolute_targetevaluationhrc))) /\ ((mdr_z_absolute_targetevaluationhr) = ((mdr_c_absolute_targetevaluationhrc) + (mdr_f_absolute_targetevaluationhrc)) * S ((mdr_c_absolute_targetevaluationhrc) + (mdr_f_absolute_targetevaluationhrc)) + ((mdr_f_absolute_targetevaluationhrc) + (mdr_f_absolute_targetevaluationhrc))))))))) /\ (((exists ff_h_mdr_absolute_targetevaluationhrb. ff_h_mdr_absolute_targetevaluationhrb + S (mdr_z_absolute_targetevaluationhr) = S ((S (mdr_i_absolute_targetevaluationh)) * mdr_c_absolute_targetevaluation)) /\ exists ff_q_mdr_absolute_targetevaluationhrb. mdr_b_absolute_targetevaluation = ff_q_mdr_absolute_targetevaluationhrb * S ((S (mdr_i_absolute_targetevaluationh)) * mdr_c_absolute_targetevaluation) + (mdr_z_absolute_targetevaluationhr))))) /\ (((((mdr_d_absolute_targetevaluationh) = 0) /\ (((mdr_p_absolute_targetevaluationh) = 1) /\ ((mdr_n_absolute_targetevaluationh) = 0))) \/ exists mdr_q_absolute_targetevaluationhs mdr_eb_absolute_targetevaluationhs mdr_ec_absolute_targetevaluationhs mdr_fb_absolute_targetevaluationhs mdr_fc_absolute_targetevaluationhs. (((mdr_d_absolute_targetevaluationh) = S (mdr_q_absolute_targetevaluationhs)) /\ ((forall mdr_j_absolute_targetevaluationhsc. (exists mdr_gap_absolute_targetevaluationhscj. mdr_gap_absolute_targetevaluationhscj + S (mdr_j_absolute_targetevaluationhsc) = (S (mdr_q_absolute_targetevaluationhs))) -> exists mdr_i_absolute_targetevaluationhsc mdr_up_absolute_targetevaluationhsc mdr_us_absolute_targetevaluationhsc mdr_un_absolute_targetevaluationhsc mdr_ut_absolute_targetevaluationhsc mdr_p_absolute_targetevaluationhsc mdr_n_absolute_targetevaluationhsc. ((exists mdr_gap_absolute_targetevaluationhsci. mdr_gap_absolute_targetevaluationhsci + S (mdr_i_absolute_targetevaluationhsc) = (mdr_i_absolute_targetevaluationh)) /\ ((exists mdr_z_absolute_targetevaluationhscr. ((exists mdr_a_absolute_targetevaluationhscrc mdr_b_absolute_targetevaluationhscrc mdr_c_absolute_targetevaluationhscrc mdr_e_absolute_targetevaluationhscrc mdr_f_absolute_targetevaluationhscrc. ((mdr_a_absolute_targetevaluationhscrc = ((mdr_q_absolute_targetevaluationhs) + (mdr_up_absolute_targetevaluationhsc)) * S ((mdr_q_absolute_targetevaluationhs) + (mdr_up_absolute_targetevaluationhsc)) + ((mdr_up_absolute_targetevaluationhsc) + (mdr_up_absolute_targetevaluationhsc))) /\ ((mdr_b_absolute_targetevaluationhscrc = ((mdr_us_absolute_targetevaluationhsc) + (mdr_un_absolute_targetevaluationhsc)) * S ((mdr_us_absolute_targetevaluationhsc) + (mdr_un_absolute_targetevaluationhsc)) + ((mdr_un_absolute_targetevaluationhsc) + (mdr_un_absolute_targetevaluationhsc))) /\ ((mdr_c_absolute_targetevaluationhscrc = ((mdr_a_absolute_targetevaluationhscrc) + (mdr_b_absolute_targetevaluationhscrc)) * S ((mdr_a_absolute_targetevaluationhscrc) + (mdr_b_absolute_targetevaluationhscrc)) + ((mdr_b_absolute_targetevaluationhscrc) + (mdr_b_absolute_targetevaluationhscrc))) /\ ((mdr_e_absolute_targetevaluationhscrc = ((mdr_p_absolute_targetevaluationhsc) + (mdr_n_absolute_targetevaluationhsc)) * S ((mdr_p_absolute_targetevaluationhsc) + (mdr_n_absolute_targetevaluationhsc)) + ((mdr_n_absolute_targetevaluationhsc) + (mdr_n_absolute_targetevaluationhsc))) /\ ((mdr_f_absolute_targetevaluationhscrc = ((mdr_ut_absolute_targetevaluationhsc) + (mdr_e_absolute_targetevaluationhscrc)) * S ((mdr_ut_absolute_targetevaluationhsc) + (mdr_e_absolute_targetevaluationhscrc)) + ((mdr_e_absolute_targetevaluationhscrc) + (mdr_e_absolute_targetevaluationhscrc))) /\ ((mdr_z_absolute_targetevaluationhscr) = ((mdr_c_absolute_targetevaluationhscrc) + (mdr_f_absolute_targetevaluationhscrc)) * S ((mdr_c_absolute_targetevaluationhscrc) + (mdr_f_absolute_targetevaluationhscrc)) + ((mdr_f_absolute_targetevaluationhscrc) + (mdr_f_absolute_targetevaluationhscrc))))))))) /\ (((exists ff_h_mdr_absolute_targetevaluationhscrb. ff_h_mdr_absolute_targetevaluationhscrb + S (mdr_z_absolute_targetevaluationhscr) = S ((S (mdr_i_absolute_targetevaluationhsc)) * mdr_c_absolute_targetevaluation)) /\ exists ff_q_mdr_absolute_targetevaluationhscrb. mdr_b_absolute_targetevaluation = ff_q_mdr_absolute_targetevaluationhscrb * S ((S (mdr_i_absolute_targetevaluationhsc)) * mdr_c_absolute_targetevaluation) + (mdr_z_absolute_targetevaluationhscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_absolute_targetevaluationhscm_positive. (exists ff_gap_mdm_lt_mdr_absolute_targetevaluationhscm_positive_index_bound. ff_gap_mdm_lt_mdr_absolute_targetevaluationhscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_absolute_targetevaluationhscm_positive) = ((mdr_q_absolute_targetevaluationhs) * (mdr_q_absolute_targetevaluationhs))) -> exists ff_row_mdm_prefix_mdr_absolute_targetevaluationhscm_positive ff_column_mdm_prefix_mdr_absolute_targetevaluationhscm_positive ff_value_mdm_prefix_mdr_absolute_targetevaluationhscm_positive. (ff_index_mdm_prefix_mdr_absolute_targetevaluationhscm_positive = (mdr_q_absolute_targetevaluationhs) * ff_row_mdm_prefix_mdr_absolute_targetevaluationhscm_positive + ff_column_mdm_prefix_mdr_absolute_targetevaluationhscm_positive /\ ((exists ff_gap_mdm_lt_mdr_absolute_targetevaluationhscm_positive_column_bound. ff_gap_mdm_lt_mdr_absolute_targetevaluationhscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_absolute_targetevaluationhscm_positive) = (mdr_q_absolute_targetevaluationhs)) /\ ((exists ff_row_mdm_cell_mdr_absolute_targetevaluationhscm_positive_cell ff_column_mdm_cell_mdr_absolute_targetevaluationhscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_absolute_targetevaluationhscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_absolute_targetevaluationhscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_absolute_targetevaluationhscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_absolute_targetevaluationhscm_positive_cell = ff_row_mdm_prefix_mdr_absolute_targetevaluationhscm_positive) \/ ((exists ff_gap_mdm_le_mdr_absolute_targetevaluationhscm_positive_cell_row_after. ff_gap_mdm_le_mdr_absolute_targetevaluationhscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_absolute_targetevaluationhscm_positive)) /\ ff_row_mdm_cell_mdr_absolute_targetevaluationhscm_positive_cell = S ff_row_mdm_prefix_mdr_absolute_targetevaluationhscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_absolute_targetevaluationhscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_absolute_targetevaluationhscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_absolute_targetevaluationhscm_positive) = (mdr_j_absolute_targetevaluationhsc)) /\ ff_column_mdm_cell_mdr_absolute_targetevaluationhscm_positive_cell = ff_column_mdm_prefix_mdr_absolute_targetevaluationhscm_positive) \/ ((exists ff_gap_mdm_le_mdr_absolute_targetevaluationhscm_positive_cell_column_after. ff_gap_mdm_le_mdr_absolute_targetevaluationhscm_positive_cell_column_after + (mdr_j_absolute_targetevaluationhsc) = (ff_column_mdm_prefix_mdr_absolute_targetevaluationhscm_positive)) /\ ff_column_mdm_cell_mdr_absolute_targetevaluationhscm_positive_cell = S ff_column_mdm_prefix_mdr_absolute_targetevaluationhscm_positive))) /\ (((exists ff_h_mdm_mdr_absolute_targetevaluationhscm_positive_cell_source. ff_h_mdm_mdr_absolute_targetevaluationhscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_absolute_targetevaluationhscm_positive) = S ((S ((ff_row_mdm_cell_mdr_absolute_targetevaluationhscm_positive_cell) * (S (mdr_q_absolute_targetevaluationhs)) + (ff_column_mdm_cell_mdr_absolute_targetevaluationhscm_positive_cell))) * mdr_pc_absolute_targetevaluationh)) /\ exists ff_q_mdm_mdr_absolute_targetevaluationhscm_positive_cell_source. mdr_pb_absolute_targetevaluationh = ff_q_mdm_mdr_absolute_targetevaluationhscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_absolute_targetevaluationhscm_positive_cell) * (S (mdr_q_absolute_targetevaluationhs)) + (ff_column_mdm_cell_mdr_absolute_targetevaluationhscm_positive_cell))) * mdr_pc_absolute_targetevaluationh) + (ff_value_mdm_prefix_mdr_absolute_targetevaluationhscm_positive)))))) /\ (((exists ff_h_mdm_mdr_absolute_targetevaluationhscm_positive_target. ff_h_mdm_mdr_absolute_targetevaluationhscm_positive_target + S (ff_value_mdm_prefix_mdr_absolute_targetevaluationhscm_positive) = S ((S (ff_index_mdm_prefix_mdr_absolute_targetevaluationhscm_positive)) * mdr_us_absolute_targetevaluationhsc)) /\ exists ff_q_mdm_mdr_absolute_targetevaluationhscm_positive_target. mdr_up_absolute_targetevaluationhsc = ff_q_mdm_mdr_absolute_targetevaluationhscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_absolute_targetevaluationhscm_positive)) * mdr_us_absolute_targetevaluationhsc) + (ff_value_mdm_prefix_mdr_absolute_targetevaluationhscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_absolute_targetevaluationhscm_negative. (exists ff_gap_mdm_lt_mdr_absolute_targetevaluationhscm_negative_index_bound. ff_gap_mdm_lt_mdr_absolute_targetevaluationhscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_absolute_targetevaluationhscm_negative) = ((mdr_q_absolute_targetevaluationhs) * (mdr_q_absolute_targetevaluationhs))) -> exists ff_row_mdm_prefix_mdr_absolute_targetevaluationhscm_negative ff_column_mdm_prefix_mdr_absolute_targetevaluationhscm_negative ff_value_mdm_prefix_mdr_absolute_targetevaluationhscm_negative. (ff_index_mdm_prefix_mdr_absolute_targetevaluationhscm_negative = (mdr_q_absolute_targetevaluationhs) * ff_row_mdm_prefix_mdr_absolute_targetevaluationhscm_negative + ff_column_mdm_prefix_mdr_absolute_targetevaluationhscm_negative /\ ((exists ff_gap_mdm_lt_mdr_absolute_targetevaluationhscm_negative_column_bound. ff_gap_mdm_lt_mdr_absolute_targetevaluationhscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_absolute_targetevaluationhscm_negative) = (mdr_q_absolute_targetevaluationhs)) /\ ((exists ff_row_mdm_cell_mdr_absolute_targetevaluationhscm_negative_cell ff_column_mdm_cell_mdr_absolute_targetevaluationhscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_absolute_targetevaluationhscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_absolute_targetevaluationhscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_absolute_targetevaluationhscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_absolute_targetevaluationhscm_negative_cell = ff_row_mdm_prefix_mdr_absolute_targetevaluationhscm_negative) \/ ((exists ff_gap_mdm_le_mdr_absolute_targetevaluationhscm_negative_cell_row_after. ff_gap_mdm_le_mdr_absolute_targetevaluationhscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_absolute_targetevaluationhscm_negative)) /\ ff_row_mdm_cell_mdr_absolute_targetevaluationhscm_negative_cell = S ff_row_mdm_prefix_mdr_absolute_targetevaluationhscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_absolute_targetevaluationhscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_absolute_targetevaluationhscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_absolute_targetevaluationhscm_negative) = (mdr_j_absolute_targetevaluationhsc)) /\ ff_column_mdm_cell_mdr_absolute_targetevaluationhscm_negative_cell = ff_column_mdm_prefix_mdr_absolute_targetevaluationhscm_negative) \/ ((exists ff_gap_mdm_le_mdr_absolute_targetevaluationhscm_negative_cell_column_after. ff_gap_mdm_le_mdr_absolute_targetevaluationhscm_negative_cell_column_after + (mdr_j_absolute_targetevaluationhsc) = (ff_column_mdm_prefix_mdr_absolute_targetevaluationhscm_negative)) /\ ff_column_mdm_cell_mdr_absolute_targetevaluationhscm_negative_cell = S ff_column_mdm_prefix_mdr_absolute_targetevaluationhscm_negative))) /\ (((exists ff_h_mdm_mdr_absolute_targetevaluationhscm_negative_cell_source. ff_h_mdm_mdr_absolute_targetevaluationhscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_absolute_targetevaluationhscm_negative) = S ((S ((ff_row_mdm_cell_mdr_absolute_targetevaluationhscm_negative_cell) * (S (mdr_q_absolute_targetevaluationhs)) + (ff_column_mdm_cell_mdr_absolute_targetevaluationhscm_negative_cell))) * mdr_nc_absolute_targetevaluationh)) /\ exists ff_q_mdm_mdr_absolute_targetevaluationhscm_negative_cell_source. mdr_nb_absolute_targetevaluationh = ff_q_mdm_mdr_absolute_targetevaluationhscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_absolute_targetevaluationhscm_negative_cell) * (S (mdr_q_absolute_targetevaluationhs)) + (ff_column_mdm_cell_mdr_absolute_targetevaluationhscm_negative_cell))) * mdr_nc_absolute_targetevaluationh) + (ff_value_mdm_prefix_mdr_absolute_targetevaluationhscm_negative)))))) /\ (((exists ff_h_mdm_mdr_absolute_targetevaluationhscm_negative_target. ff_h_mdm_mdr_absolute_targetevaluationhscm_negative_target + S (ff_value_mdm_prefix_mdr_absolute_targetevaluationhscm_negative) = S ((S (ff_index_mdm_prefix_mdr_absolute_targetevaluationhscm_negative)) * mdr_ut_absolute_targetevaluationhsc)) /\ exists ff_q_mdm_mdr_absolute_targetevaluationhscm_negative_target. mdr_un_absolute_targetevaluationhsc = ff_q_mdm_mdr_absolute_targetevaluationhscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_absolute_targetevaluationhscm_negative)) * mdr_ut_absolute_targetevaluationhsc) + (ff_value_mdm_prefix_mdr_absolute_targetevaluationhscm_negative))))))))) /\ ((((exists ff_h_mdr_absolute_targetevaluationhscp. ff_h_mdr_absolute_targetevaluationhscp + S (mdr_p_absolute_targetevaluationhsc) = S ((S (mdr_j_absolute_targetevaluationhsc)) * mdr_ec_absolute_targetevaluationhs)) /\ exists ff_q_mdr_absolute_targetevaluationhscp. mdr_eb_absolute_targetevaluationhs = ff_q_mdr_absolute_targetevaluationhscp * S ((S (mdr_j_absolute_targetevaluationhsc)) * mdr_ec_absolute_targetevaluationhs) + (mdr_p_absolute_targetevaluationhsc))) /\ (((exists ff_h_mdr_absolute_targetevaluationhscn. ff_h_mdr_absolute_targetevaluationhscn + S (mdr_n_absolute_targetevaluationhsc) = S ((S (mdr_j_absolute_targetevaluationhsc)) * mdr_fc_absolute_targetevaluationhs)) /\ exists ff_q_mdr_absolute_targetevaluationhscn. mdr_fb_absolute_targetevaluationhs = ff_q_mdr_absolute_targetevaluationhscn * S ((S (mdr_j_absolute_targetevaluationhsc)) * mdr_fc_absolute_targetevaluationhs) + (mdr_n_absolute_targetevaluationhsc)))))))) /\ (exists ff_ub_mce_fold_mdr_absolute_targetevaluationhsf ff_uc_mce_fold_mdr_absolute_targetevaluationhsf ff_vb_mce_fold_mdr_absolute_targetevaluationhsf ff_vc_mce_fold_mdr_absolute_targetevaluationhsf. ((forall ff_index_mce_alternating_mdr_absolute_targetevaluationhsf_prefix. (exists ff_gap_mce_mdr_absolute_targetevaluationhsf_prefix_index. ff_gap_mce_mdr_absolute_targetevaluationhsf_prefix_index + S (ff_index_mce_alternating_mdr_absolute_targetevaluationhsf_prefix) = (S (mdr_q_absolute_targetevaluationhs))) -> exists ff_ap_mce_alternating_mdr_absolute_targetevaluationhsf_prefix ff_an_mce_alternating_mdr_absolute_targetevaluationhsf_prefix ff_bp_mce_alternating_mdr_absolute_targetevaluationhsf_prefix ff_bn_mce_alternating_mdr_absolute_targetevaluationhsf_prefix ff_p_mce_alternating_mdr_absolute_targetevaluationhsf_prefix ff_n_mce_alternating_mdr_absolute_targetevaluationhsf_prefix. ((((exists ff_h_mce_mdr_absolute_targetevaluationhsf_prefix_ap. ff_h_mce_mdr_absolute_targetevaluationhsf_prefix_ap + S (ff_ap_mce_alternating_mdr_absolute_targetevaluationhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_absolute_targetevaluationhsf_prefix)) * mdr_pc_absolute_targetevaluationh)) /\ exists ff_q_mce_mdr_absolute_targetevaluationhsf_prefix_ap. mdr_pb_absolute_targetevaluationh = ff_q_mce_mdr_absolute_targetevaluationhsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_absolute_targetevaluationhsf_prefix)) * mdr_pc_absolute_targetevaluationh) + (ff_ap_mce_alternating_mdr_absolute_targetevaluationhsf_prefix))) /\ ((((exists ff_h_mce_mdr_absolute_targetevaluationhsf_prefix_an. ff_h_mce_mdr_absolute_targetevaluationhsf_prefix_an + S (ff_an_mce_alternating_mdr_absolute_targetevaluationhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_absolute_targetevaluationhsf_prefix)) * mdr_nc_absolute_targetevaluationh)) /\ exists ff_q_mce_mdr_absolute_targetevaluationhsf_prefix_an. mdr_nb_absolute_targetevaluationh = ff_q_mce_mdr_absolute_targetevaluationhsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_absolute_targetevaluationhsf_prefix)) * mdr_nc_absolute_targetevaluationh) + (ff_an_mce_alternating_mdr_absolute_targetevaluationhsf_prefix))) /\ ((((exists ff_h_mce_mdr_absolute_targetevaluationhsf_prefix_bp. ff_h_mce_mdr_absolute_targetevaluationhsf_prefix_bp + S (ff_bp_mce_alternating_mdr_absolute_targetevaluationhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_absolute_targetevaluationhsf_prefix)) * mdr_ec_absolute_targetevaluationhs)) /\ exists ff_q_mce_mdr_absolute_targetevaluationhsf_prefix_bp. mdr_eb_absolute_targetevaluationhs = ff_q_mce_mdr_absolute_targetevaluationhsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_absolute_targetevaluationhsf_prefix)) * mdr_ec_absolute_targetevaluationhs) + (ff_bp_mce_alternating_mdr_absolute_targetevaluationhsf_prefix))) /\ ((((exists ff_h_mce_mdr_absolute_targetevaluationhsf_prefix_bn. ff_h_mce_mdr_absolute_targetevaluationhsf_prefix_bn + S (ff_bn_mce_alternating_mdr_absolute_targetevaluationhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_absolute_targetevaluationhsf_prefix)) * mdr_fc_absolute_targetevaluationhs)) /\ exists ff_q_mce_mdr_absolute_targetevaluationhsf_prefix_bn. mdr_fb_absolute_targetevaluationhs = ff_q_mce_mdr_absolute_targetevaluationhsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_absolute_targetevaluationhsf_prefix)) * mdr_fc_absolute_targetevaluationhs) + (ff_bn_mce_alternating_mdr_absolute_targetevaluationhsf_prefix))) /\ ((((exists ff_h_mce_mdr_absolute_targetevaluationhsf_prefix_positive. ff_h_mce_mdr_absolute_targetevaluationhsf_prefix_positive + S (ff_p_mce_alternating_mdr_absolute_targetevaluationhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_absolute_targetevaluationhsf_prefix)) * ff_uc_mce_fold_mdr_absolute_targetevaluationhsf)) /\ exists ff_q_mce_mdr_absolute_targetevaluationhsf_prefix_positive. ff_ub_mce_fold_mdr_absolute_targetevaluationhsf = ff_q_mce_mdr_absolute_targetevaluationhsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_absolute_targetevaluationhsf_prefix)) * ff_uc_mce_fold_mdr_absolute_targetevaluationhsf) + (ff_p_mce_alternating_mdr_absolute_targetevaluationhsf_prefix))) /\ ((((exists ff_h_mce_mdr_absolute_targetevaluationhsf_prefix_negative. ff_h_mce_mdr_absolute_targetevaluationhsf_prefix_negative + S (ff_n_mce_alternating_mdr_absolute_targetevaluationhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_absolute_targetevaluationhsf_prefix)) * ff_vc_mce_fold_mdr_absolute_targetevaluationhsf)) /\ exists ff_q_mce_mdr_absolute_targetevaluationhsf_prefix_negative. ff_vb_mce_fold_mdr_absolute_targetevaluationhsf = ff_q_mce_mdr_absolute_targetevaluationhsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_absolute_targetevaluationhsf_prefix)) * ff_vc_mce_fold_mdr_absolute_targetevaluationhsf) + (ff_n_mce_alternating_mdr_absolute_targetevaluationhsf_prefix))) /\ (((exists ff_even_mce_term_mdr_absolute_targetevaluationhsf_prefix_term. ff_index_mce_alternating_mdr_absolute_targetevaluationhsf_prefix = 2 * ff_even_mce_term_mdr_absolute_targetevaluationhsf_prefix_term) /\ (ff_p_mce_alternating_mdr_absolute_targetevaluationhsf_prefix = (ff_ap_mce_alternating_mdr_absolute_targetevaluationhsf_prefix) * (ff_bp_mce_alternating_mdr_absolute_targetevaluationhsf_prefix) + (ff_an_mce_alternating_mdr_absolute_targetevaluationhsf_prefix) * (ff_bn_mce_alternating_mdr_absolute_targetevaluationhsf_prefix) /\ ff_n_mce_alternating_mdr_absolute_targetevaluationhsf_prefix = (ff_ap_mce_alternating_mdr_absolute_targetevaluationhsf_prefix) * (ff_bn_mce_alternating_mdr_absolute_targetevaluationhsf_prefix) + (ff_an_mce_alternating_mdr_absolute_targetevaluationhsf_prefix) * (ff_bp_mce_alternating_mdr_absolute_targetevaluationhsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_absolute_targetevaluationhsf_prefix_term. ff_index_mce_alternating_mdr_absolute_targetevaluationhsf_prefix = 2 * ff_odd_mce_term_mdr_absolute_targetevaluationhsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_absolute_targetevaluationhsf_prefix = (ff_ap_mce_alternating_mdr_absolute_targetevaluationhsf_prefix) * (ff_bn_mce_alternating_mdr_absolute_targetevaluationhsf_prefix) + (ff_an_mce_alternating_mdr_absolute_targetevaluationhsf_prefix) * (ff_bp_mce_alternating_mdr_absolute_targetevaluationhsf_prefix) /\ ff_n_mce_alternating_mdr_absolute_targetevaluationhsf_prefix = (ff_ap_mce_alternating_mdr_absolute_targetevaluationhsf_prefix) * (ff_bp_mce_alternating_mdr_absolute_targetevaluationhsf_prefix) + (ff_an_mce_alternating_mdr_absolute_targetevaluationhsf_prefix) * (ff_bn_mce_alternating_mdr_absolute_targetevaluationhsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_absolute_targetevaluationhsf_positive ff_v_mce_mdr_absolute_targetevaluationhsf_positive. ((((exists ff_h_mce_mdr_absolute_targetevaluationhsf_positive_start. ff_h_mce_mdr_absolute_targetevaluationhsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_absolute_targetevaluationhsf_positive)) /\ exists ff_q_mce_mdr_absolute_targetevaluationhsf_positive_start. ff_u_mce_mdr_absolute_targetevaluationhsf_positive = ff_q_mce_mdr_absolute_targetevaluationhsf_positive_start * S ((S (0)) * ff_v_mce_mdr_absolute_targetevaluationhsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_absolute_targetevaluationhsf_positive_terminal. ff_h_mce_mdr_absolute_targetevaluationhsf_positive_terminal + S (mdr_p_absolute_targetevaluationh) = S ((S ((S (mdr_q_absolute_targetevaluationhs)))) * ff_v_mce_mdr_absolute_targetevaluationhsf_positive)) /\ exists ff_q_mce_mdr_absolute_targetevaluationhsf_positive_terminal. ff_u_mce_mdr_absolute_targetevaluationhsf_positive = ff_q_mce_mdr_absolute_targetevaluationhsf_positive_terminal * S ((S ((S (mdr_q_absolute_targetevaluationhs)))) * ff_v_mce_mdr_absolute_targetevaluationhsf_positive) + (mdr_p_absolute_targetevaluationh))) /\ forall ff_i_mce_mdr_absolute_targetevaluationhsf_positive. (exists ff_lt_mce_mdr_absolute_targetevaluationhsf_positive_bound. ff_lt_mce_mdr_absolute_targetevaluationhsf_positive_bound + S ff_i_mce_mdr_absolute_targetevaluationhsf_positive = (S (mdr_q_absolute_targetevaluationhs))) -> exists ff_a_mce_mdr_absolute_targetevaluationhsf_positive ff_r_mce_mdr_absolute_targetevaluationhsf_positive ff_s_mce_mdr_absolute_targetevaluationhsf_positive. ((((exists ff_h_mce_mdr_absolute_targetevaluationhsf_positive_summand. ff_h_mce_mdr_absolute_targetevaluationhsf_positive_summand + S (ff_a_mce_mdr_absolute_targetevaluationhsf_positive) = S ((S (ff_i_mce_mdr_absolute_targetevaluationhsf_positive)) * ff_uc_mce_fold_mdr_absolute_targetevaluationhsf)) /\ exists ff_q_mce_mdr_absolute_targetevaluationhsf_positive_summand. ff_ub_mce_fold_mdr_absolute_targetevaluationhsf = ff_q_mce_mdr_absolute_targetevaluationhsf_positive_summand * S ((S (ff_i_mce_mdr_absolute_targetevaluationhsf_positive)) * ff_uc_mce_fold_mdr_absolute_targetevaluationhsf) + (ff_a_mce_mdr_absolute_targetevaluationhsf_positive))) /\ ((((exists ff_h_mce_mdr_absolute_targetevaluationhsf_positive_partial. ff_h_mce_mdr_absolute_targetevaluationhsf_positive_partial + S (ff_r_mce_mdr_absolute_targetevaluationhsf_positive) = S ((S (ff_i_mce_mdr_absolute_targetevaluationhsf_positive)) * ff_v_mce_mdr_absolute_targetevaluationhsf_positive)) /\ exists ff_q_mce_mdr_absolute_targetevaluationhsf_positive_partial. ff_u_mce_mdr_absolute_targetevaluationhsf_positive = ff_q_mce_mdr_absolute_targetevaluationhsf_positive_partial * S ((S (ff_i_mce_mdr_absolute_targetevaluationhsf_positive)) * ff_v_mce_mdr_absolute_targetevaluationhsf_positive) + (ff_r_mce_mdr_absolute_targetevaluationhsf_positive))) /\ ((((exists ff_h_mce_mdr_absolute_targetevaluationhsf_positive_successor. ff_h_mce_mdr_absolute_targetevaluationhsf_positive_successor + S (ff_s_mce_mdr_absolute_targetevaluationhsf_positive) = S ((S (S ff_i_mce_mdr_absolute_targetevaluationhsf_positive)) * ff_v_mce_mdr_absolute_targetevaluationhsf_positive)) /\ exists ff_q_mce_mdr_absolute_targetevaluationhsf_positive_successor. ff_u_mce_mdr_absolute_targetevaluationhsf_positive = ff_q_mce_mdr_absolute_targetevaluationhsf_positive_successor * S ((S (S ff_i_mce_mdr_absolute_targetevaluationhsf_positive)) * ff_v_mce_mdr_absolute_targetevaluationhsf_positive) + (ff_s_mce_mdr_absolute_targetevaluationhsf_positive))) /\ ff_s_mce_mdr_absolute_targetevaluationhsf_positive = ff_r_mce_mdr_absolute_targetevaluationhsf_positive + ff_a_mce_mdr_absolute_targetevaluationhsf_positive)))))) /\ (exists ff_u_mce_mdr_absolute_targetevaluationhsf_negative ff_v_mce_mdr_absolute_targetevaluationhsf_negative. ((((exists ff_h_mce_mdr_absolute_targetevaluationhsf_negative_start. ff_h_mce_mdr_absolute_targetevaluationhsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_absolute_targetevaluationhsf_negative)) /\ exists ff_q_mce_mdr_absolute_targetevaluationhsf_negative_start. ff_u_mce_mdr_absolute_targetevaluationhsf_negative = ff_q_mce_mdr_absolute_targetevaluationhsf_negative_start * S ((S (0)) * ff_v_mce_mdr_absolute_targetevaluationhsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_absolute_targetevaluationhsf_negative_terminal. ff_h_mce_mdr_absolute_targetevaluationhsf_negative_terminal + S (mdr_n_absolute_targetevaluationh) = S ((S ((S (mdr_q_absolute_targetevaluationhs)))) * ff_v_mce_mdr_absolute_targetevaluationhsf_negative)) /\ exists ff_q_mce_mdr_absolute_targetevaluationhsf_negative_terminal. ff_u_mce_mdr_absolute_targetevaluationhsf_negative = ff_q_mce_mdr_absolute_targetevaluationhsf_negative_terminal * S ((S ((S (mdr_q_absolute_targetevaluationhs)))) * ff_v_mce_mdr_absolute_targetevaluationhsf_negative) + (mdr_n_absolute_targetevaluationh))) /\ forall ff_i_mce_mdr_absolute_targetevaluationhsf_negative. (exists ff_lt_mce_mdr_absolute_targetevaluationhsf_negative_bound. ff_lt_mce_mdr_absolute_targetevaluationhsf_negative_bound + S ff_i_mce_mdr_absolute_targetevaluationhsf_negative = (S (mdr_q_absolute_targetevaluationhs))) -> exists ff_a_mce_mdr_absolute_targetevaluationhsf_negative ff_r_mce_mdr_absolute_targetevaluationhsf_negative ff_s_mce_mdr_absolute_targetevaluationhsf_negative. ((((exists ff_h_mce_mdr_absolute_targetevaluationhsf_negative_summand. ff_h_mce_mdr_absolute_targetevaluationhsf_negative_summand + S (ff_a_mce_mdr_absolute_targetevaluationhsf_negative) = S ((S (ff_i_mce_mdr_absolute_targetevaluationhsf_negative)) * ff_vc_mce_fold_mdr_absolute_targetevaluationhsf)) /\ exists ff_q_mce_mdr_absolute_targetevaluationhsf_negative_summand. ff_vb_mce_fold_mdr_absolute_targetevaluationhsf = ff_q_mce_mdr_absolute_targetevaluationhsf_negative_summand * S ((S (ff_i_mce_mdr_absolute_targetevaluationhsf_negative)) * ff_vc_mce_fold_mdr_absolute_targetevaluationhsf) + (ff_a_mce_mdr_absolute_targetevaluationhsf_negative))) /\ ((((exists ff_h_mce_mdr_absolute_targetevaluationhsf_negative_partial. ff_h_mce_mdr_absolute_targetevaluationhsf_negative_partial + S (ff_r_mce_mdr_absolute_targetevaluationhsf_negative) = S ((S (ff_i_mce_mdr_absolute_targetevaluationhsf_negative)) * ff_v_mce_mdr_absolute_targetevaluationhsf_negative)) /\ exists ff_q_mce_mdr_absolute_targetevaluationhsf_negative_partial. ff_u_mce_mdr_absolute_targetevaluationhsf_negative = ff_q_mce_mdr_absolute_targetevaluationhsf_negative_partial * S ((S (ff_i_mce_mdr_absolute_targetevaluationhsf_negative)) * ff_v_mce_mdr_absolute_targetevaluationhsf_negative) + (ff_r_mce_mdr_absolute_targetevaluationhsf_negative))) /\ ((((exists ff_h_mce_mdr_absolute_targetevaluationhsf_negative_successor. ff_h_mce_mdr_absolute_targetevaluationhsf_negative_successor + S (ff_s_mce_mdr_absolute_targetevaluationhsf_negative) = S ((S (S ff_i_mce_mdr_absolute_targetevaluationhsf_negative)) * ff_v_mce_mdr_absolute_targetevaluationhsf_negative)) /\ exists ff_q_mce_mdr_absolute_targetevaluationhsf_negative_successor. ff_u_mce_mdr_absolute_targetevaluationhsf_negative = ff_q_mce_mdr_absolute_targetevaluationhsf_negative_successor * S ((S (S ff_i_mce_mdr_absolute_targetevaluationhsf_negative)) * ff_v_mce_mdr_absolute_targetevaluationhsf_negative) + (ff_s_mce_mdr_absolute_targetevaluationhsf_negative))) /\ ff_s_mce_mdr_absolute_targetevaluationhsf_negative = ff_r_mce_mdr_absolute_targetevaluationhsf_negative + ff_a_mce_mdr_absolute_targetevaluationhsf_negative))))))))))))))) /\ ((exists mdr_gap_absolute_targetevaluationi. mdr_gap_absolute_targetevaluationi + S (mdr_i_absolute_targetevaluation) = (mdr_l_absolute_targetevaluation)) /\ (exists mdr_z_absolute_targetevaluationr. ((exists mdr_a_absolute_targetevaluationrc mdr_b_absolute_targetevaluationrc mdr_c_absolute_targetevaluationrc mdr_e_absolute_targetevaluationrc mdr_f_absolute_targetevaluationrc. ((mdr_a_absolute_targetevaluationrc = ((d) + (eb)) * S ((d) + (eb)) + ((eb) + (eb))) /\ ((mdr_b_absolute_targetevaluationrc = ((ec) + (fb)) * S ((ec) + (fb)) + ((fb) + (fb))) /\ ((mdr_c_absolute_targetevaluationrc = ((mdr_a_absolute_targetevaluationrc) + (mdr_b_absolute_targetevaluationrc)) * S ((mdr_a_absolute_targetevaluationrc) + (mdr_b_absolute_targetevaluationrc)) + ((mdr_b_absolute_targetevaluationrc) + (mdr_b_absolute_targetevaluationrc))) /\ ((mdr_e_absolute_targetevaluationrc = ((mdr_p_absolute_target) + (mdr_n_absolute_target)) * S ((mdr_p_absolute_target) + (mdr_n_absolute_target)) + ((mdr_n_absolute_target) + (mdr_n_absolute_target))) /\ ((mdr_f_absolute_targetevaluationrc = ((fc) + (mdr_e_absolute_targetevaluationrc)) * S ((fc) + (mdr_e_absolute_targetevaluationrc)) + ((mdr_e_absolute_targetevaluationrc) + (mdr_e_absolute_targetevaluationrc))) /\ ((mdr_z_absolute_targetevaluationr) = ((mdr_c_absolute_targetevaluationrc) + (mdr_f_absolute_targetevaluationrc)) * S ((mdr_c_absolute_targetevaluationrc) + (mdr_f_absolute_targetevaluationrc)) + ((mdr_f_absolute_targetevaluationrc) + (mdr_f_absolute_targetevaluationrc))))))))) /\ (((exists ff_h_mdr_absolute_targetevaluationrb. ff_h_mdr_absolute_targetevaluationrb + S (mdr_z_absolute_targetevaluationr) = S ((S (mdr_i_absolute_targetevaluation)) * mdr_c_absolute_targetevaluation)) /\ exists ff_q_mdr_absolute_targetevaluationrb. mdr_b_absolute_targetevaluation = ff_q_mdr_absolute_targetevaluationrb * S ((S (mdr_i_absolute_targetevaluation)) * mdr_c_absolute_targetevaluation) + (mdr_z_absolute_targetevaluationr)))))))) /\ (((mdr_p_absolute_target) = (mdr_n_absolute_target) + (D)) \/ ((mdr_n_absolute_target) = (mdr_p_absolute_target) + (D)))))