PositiveDeterminantMatrixData(ab,ac,bb,bc,d,D)

((~(d = 0)) /\ ((~(D = 0)) /\ (exists mdr_p_secondwaveabsolute mdr_n_secondwaveabsolute. ((exists mdr_b_secondwaveabsoluteevaluation mdr_c_secondwaveabsoluteevaluation mdr_l_secondwaveabsoluteevaluation mdr_i_secondwaveabsoluteevaluation. ((forall mdr_i_secondwaveabsoluteevaluationh. (exists mdr_gap_secondwaveabsoluteevaluationhi. mdr_gap_secondwaveabsoluteevaluationhi + S (mdr_i_secondwaveabsoluteevaluationh) = (mdr_l_secondwaveabsoluteevaluation)) -> exists mdr_d_secondwaveabsoluteevaluationh mdr_pb_secondwaveabsoluteevaluationh mdr_pc_secondwaveabsoluteevaluationh mdr_nb_secondwaveabsoluteevaluationh mdr_nc_secondwaveabsoluteevaluationh mdr_p_secondwaveabsoluteevaluationh mdr_n_secondwaveabsoluteevaluationh. ((exists mdr_z_secondwaveabsoluteevaluationhr. ((exists mdr_a_secondwaveabsoluteevaluationhrc mdr_b_secondwaveabsoluteevaluationhrc mdr_c_secondwaveabsoluteevaluationhrc mdr_e_secondwaveabsoluteevaluationhrc mdr_f_secondwaveabsoluteevaluationhrc. ((mdr_a_secondwaveabsoluteevaluationhrc = ((mdr_d_secondwaveabsoluteevaluationh) + (mdr_pb_secondwaveabsoluteevaluationh)) * S ((mdr_d_secondwaveabsoluteevaluationh) + (mdr_pb_secondwaveabsoluteevaluationh)) + ((mdr_pb_secondwaveabsoluteevaluationh) + (mdr_pb_secondwaveabsoluteevaluationh))) /\ ((mdr_b_secondwaveabsoluteevaluationhrc = ((mdr_pc_secondwaveabsoluteevaluationh) + (mdr_nb_secondwaveabsoluteevaluationh)) * S ((mdr_pc_secondwaveabsoluteevaluationh) + (mdr_nb_secondwaveabsoluteevaluationh)) + ((mdr_nb_secondwaveabsoluteevaluationh) + (mdr_nb_secondwaveabsoluteevaluationh))) /\ ((mdr_c_secondwaveabsoluteevaluationhrc = ((mdr_a_secondwaveabsoluteevaluationhrc) + (mdr_b_secondwaveabsoluteevaluationhrc)) * S ((mdr_a_secondwaveabsoluteevaluationhrc) + (mdr_b_secondwaveabsoluteevaluationhrc)) + ((mdr_b_secondwaveabsoluteevaluationhrc) + (mdr_b_secondwaveabsoluteevaluationhrc))) /\ ((mdr_e_secondwaveabsoluteevaluationhrc = ((mdr_p_secondwaveabsoluteevaluationh) + (mdr_n_secondwaveabsoluteevaluationh)) * S ((mdr_p_secondwaveabsoluteevaluationh) + (mdr_n_secondwaveabsoluteevaluationh)) + ((mdr_n_secondwaveabsoluteevaluationh) + (mdr_n_secondwaveabsoluteevaluationh))) /\ ((mdr_f_secondwaveabsoluteevaluationhrc = ((mdr_nc_secondwaveabsoluteevaluationh) + (mdr_e_secondwaveabsoluteevaluationhrc)) * S ((mdr_nc_secondwaveabsoluteevaluationh) + (mdr_e_secondwaveabsoluteevaluationhrc)) + ((mdr_e_secondwaveabsoluteevaluationhrc) + (mdr_e_secondwaveabsoluteevaluationhrc))) /\ ((mdr_z_secondwaveabsoluteevaluationhr) = ((mdr_c_secondwaveabsoluteevaluationhrc) + (mdr_f_secondwaveabsoluteevaluationhrc)) * S ((mdr_c_secondwaveabsoluteevaluationhrc) + (mdr_f_secondwaveabsoluteevaluationhrc)) + ((mdr_f_secondwaveabsoluteevaluationhrc) + (mdr_f_secondwaveabsoluteevaluationhrc))))))))) /\ (((exists ff_h_mdr_secondwaveabsoluteevaluationhrb. ff_h_mdr_secondwaveabsoluteevaluationhrb + S (mdr_z_secondwaveabsoluteevaluationhr) = S ((S (mdr_i_secondwaveabsoluteevaluationh)) * mdr_c_secondwaveabsoluteevaluation)) /\ exists ff_q_mdr_secondwaveabsoluteevaluationhrb. mdr_b_secondwaveabsoluteevaluation = ff_q_mdr_secondwaveabsoluteevaluationhrb * S ((S (mdr_i_secondwaveabsoluteevaluationh)) * mdr_c_secondwaveabsoluteevaluation) + (mdr_z_secondwaveabsoluteevaluationhr))))) /\ (((((mdr_d_secondwaveabsoluteevaluationh) = 0) /\ (((mdr_p_secondwaveabsoluteevaluationh) = 1) /\ ((mdr_n_secondwaveabsoluteevaluationh) = 0))) \/ exists mdr_q_secondwaveabsoluteevaluationhs mdr_eb_secondwaveabsoluteevaluationhs mdr_ec_secondwaveabsoluteevaluationhs mdr_fb_secondwaveabsoluteevaluationhs mdr_fc_secondwaveabsoluteevaluationhs. (((mdr_d_secondwaveabsoluteevaluationh) = S (mdr_q_secondwaveabsoluteevaluationhs)) /\ ((forall mdr_j_secondwaveabsoluteevaluationhsc. (exists mdr_gap_secondwaveabsoluteevaluationhscj. mdr_gap_secondwaveabsoluteevaluationhscj + S (mdr_j_secondwaveabsoluteevaluationhsc) = (S (mdr_q_secondwaveabsoluteevaluationhs))) -> exists mdr_i_secondwaveabsoluteevaluationhsc mdr_up_secondwaveabsoluteevaluationhsc mdr_us_secondwaveabsoluteevaluationhsc mdr_un_secondwaveabsoluteevaluationhsc mdr_ut_secondwaveabsoluteevaluationhsc mdr_p_secondwaveabsoluteevaluationhsc mdr_n_secondwaveabsoluteevaluationhsc. ((exists mdr_gap_secondwaveabsoluteevaluationhsci. mdr_gap_secondwaveabsoluteevaluationhsci + S (mdr_i_secondwaveabsoluteevaluationhsc) = (mdr_i_secondwaveabsoluteevaluationh)) /\ ((exists mdr_z_secondwaveabsoluteevaluationhscr. ((exists mdr_a_secondwaveabsoluteevaluationhscrc mdr_b_secondwaveabsoluteevaluationhscrc mdr_c_secondwaveabsoluteevaluationhscrc mdr_e_secondwaveabsoluteevaluationhscrc mdr_f_secondwaveabsoluteevaluationhscrc. ((mdr_a_secondwaveabsoluteevaluationhscrc = ((mdr_q_secondwaveabsoluteevaluationhs) + (mdr_up_secondwaveabsoluteevaluationhsc)) * S ((mdr_q_secondwaveabsoluteevaluationhs) + (mdr_up_secondwaveabsoluteevaluationhsc)) + ((mdr_up_secondwaveabsoluteevaluationhsc) + (mdr_up_secondwaveabsoluteevaluationhsc))) /\ ((mdr_b_secondwaveabsoluteevaluationhscrc = ((mdr_us_secondwaveabsoluteevaluationhsc) + (mdr_un_secondwaveabsoluteevaluationhsc)) * S ((mdr_us_secondwaveabsoluteevaluationhsc) + (mdr_un_secondwaveabsoluteevaluationhsc)) + ((mdr_un_secondwaveabsoluteevaluationhsc) + (mdr_un_secondwaveabsoluteevaluationhsc))) /\ ((mdr_c_secondwaveabsoluteevaluationhscrc = ((mdr_a_secondwaveabsoluteevaluationhscrc) + (mdr_b_secondwaveabsoluteevaluationhscrc)) * S ((mdr_a_secondwaveabsoluteevaluationhscrc) + (mdr_b_secondwaveabsoluteevaluationhscrc)) + ((mdr_b_secondwaveabsoluteevaluationhscrc) + (mdr_b_secondwaveabsoluteevaluationhscrc))) /\ ((mdr_e_secondwaveabsoluteevaluationhscrc = ((mdr_p_secondwaveabsoluteevaluationhsc) + (mdr_n_secondwaveabsoluteevaluationhsc)) * S ((mdr_p_secondwaveabsoluteevaluationhsc) + (mdr_n_secondwaveabsoluteevaluationhsc)) + ((mdr_n_secondwaveabsoluteevaluationhsc) + (mdr_n_secondwaveabsoluteevaluationhsc))) /\ ((mdr_f_secondwaveabsoluteevaluationhscrc = ((mdr_ut_secondwaveabsoluteevaluationhsc) + (mdr_e_secondwaveabsoluteevaluationhscrc)) * S ((mdr_ut_secondwaveabsoluteevaluationhsc) + (mdr_e_secondwaveabsoluteevaluationhscrc)) + ((mdr_e_secondwaveabsoluteevaluationhscrc) + (mdr_e_secondwaveabsoluteevaluationhscrc))) /\ ((mdr_z_secondwaveabsoluteevaluationhscr) = ((mdr_c_secondwaveabsoluteevaluationhscrc) + (mdr_f_secondwaveabsoluteevaluationhscrc)) * S ((mdr_c_secondwaveabsoluteevaluationhscrc) + (mdr_f_secondwaveabsoluteevaluationhscrc)) + ((mdr_f_secondwaveabsoluteevaluationhscrc) + (mdr_f_secondwaveabsoluteevaluationhscrc))))))))) /\ (((exists ff_h_mdr_secondwaveabsoluteevaluationhscrb. ff_h_mdr_secondwaveabsoluteevaluationhscrb + S (mdr_z_secondwaveabsoluteevaluationhscr) = S ((S (mdr_i_secondwaveabsoluteevaluationhsc)) * mdr_c_secondwaveabsoluteevaluation)) /\ exists ff_q_mdr_secondwaveabsoluteevaluationhscrb. mdr_b_secondwaveabsoluteevaluation = ff_q_mdr_secondwaveabsoluteevaluationhscrb * S ((S (mdr_i_secondwaveabsoluteevaluationhsc)) * mdr_c_secondwaveabsoluteevaluation) + (mdr_z_secondwaveabsoluteevaluationhscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_secondwaveabsoluteevaluationhscm_positive. (exists ff_gap_mdm_lt_mdr_secondwaveabsoluteevaluationhscm_positive_index_bound. ff_gap_mdm_lt_mdr_secondwaveabsoluteevaluationhscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_secondwaveabsoluteevaluationhscm_positive) = ((mdr_q_secondwaveabsoluteevaluationhs) * (mdr_q_secondwaveabsoluteevaluationhs))) -> exists ff_row_mdm_prefix_mdr_secondwaveabsoluteevaluationhscm_positive ff_column_mdm_prefix_mdr_secondwaveabsoluteevaluationhscm_positive ff_value_mdm_prefix_mdr_secondwaveabsoluteevaluationhscm_positive. (ff_index_mdm_prefix_mdr_secondwaveabsoluteevaluationhscm_positive = (mdr_q_secondwaveabsoluteevaluationhs) * ff_row_mdm_prefix_mdr_secondwaveabsoluteevaluationhscm_positive + ff_column_mdm_prefix_mdr_secondwaveabsoluteevaluationhscm_positive /\ ((exists ff_gap_mdm_lt_mdr_secondwaveabsoluteevaluationhscm_positive_column_bound. ff_gap_mdm_lt_mdr_secondwaveabsoluteevaluationhscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_secondwaveabsoluteevaluationhscm_positive) = (mdr_q_secondwaveabsoluteevaluationhs)) /\ ((exists ff_row_mdm_cell_mdr_secondwaveabsoluteevaluationhscm_positive_cell ff_column_mdm_cell_mdr_secondwaveabsoluteevaluationhscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_secondwaveabsoluteevaluationhscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_secondwaveabsoluteevaluationhscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_secondwaveabsoluteevaluationhscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_secondwaveabsoluteevaluationhscm_positive_cell = ff_row_mdm_prefix_mdr_secondwaveabsoluteevaluationhscm_positive) \/ ((exists ff_gap_mdm_le_mdr_secondwaveabsoluteevaluationhscm_positive_cell_row_after. ff_gap_mdm_le_mdr_secondwaveabsoluteevaluationhscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_secondwaveabsoluteevaluationhscm_positive)) /\ ff_row_mdm_cell_mdr_secondwaveabsoluteevaluationhscm_positive_cell = S ff_row_mdm_prefix_mdr_secondwaveabsoluteevaluationhscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_secondwaveabsoluteevaluationhscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_secondwaveabsoluteevaluationhscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_secondwaveabsoluteevaluationhscm_positive) = (mdr_j_secondwaveabsoluteevaluationhsc)) /\ ff_column_mdm_cell_mdr_secondwaveabsoluteevaluationhscm_positive_cell = ff_column_mdm_prefix_mdr_secondwaveabsoluteevaluationhscm_positive) \/ ((exists ff_gap_mdm_le_mdr_secondwaveabsoluteevaluationhscm_positive_cell_column_after. ff_gap_mdm_le_mdr_secondwaveabsoluteevaluationhscm_positive_cell_column_after + (mdr_j_secondwaveabsoluteevaluationhsc) = (ff_column_mdm_prefix_mdr_secondwaveabsoluteevaluationhscm_positive)) /\ ff_column_mdm_cell_mdr_secondwaveabsoluteevaluationhscm_positive_cell = S ff_column_mdm_prefix_mdr_secondwaveabsoluteevaluationhscm_positive))) /\ (((exists ff_h_mdm_mdr_secondwaveabsoluteevaluationhscm_positive_cell_source. ff_h_mdm_mdr_secondwaveabsoluteevaluationhscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_secondwaveabsoluteevaluationhscm_positive) = S ((S ((ff_row_mdm_cell_mdr_secondwaveabsoluteevaluationhscm_positive_cell) * (S (mdr_q_secondwaveabsoluteevaluationhs)) + (ff_column_mdm_cell_mdr_secondwaveabsoluteevaluationhscm_positive_cell))) * mdr_pc_secondwaveabsoluteevaluationh)) /\ exists ff_q_mdm_mdr_secondwaveabsoluteevaluationhscm_positive_cell_source. mdr_pb_secondwaveabsoluteevaluationh = ff_q_mdm_mdr_secondwaveabsoluteevaluationhscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_secondwaveabsoluteevaluationhscm_positive_cell) * (S (mdr_q_secondwaveabsoluteevaluationhs)) + (ff_column_mdm_cell_mdr_secondwaveabsoluteevaluationhscm_positive_cell))) * mdr_pc_secondwaveabsoluteevaluationh) + (ff_value_mdm_prefix_mdr_secondwaveabsoluteevaluationhscm_positive)))))) /\ (((exists ff_h_mdm_mdr_secondwaveabsoluteevaluationhscm_positive_target. ff_h_mdm_mdr_secondwaveabsoluteevaluationhscm_positive_target + S (ff_value_mdm_prefix_mdr_secondwaveabsoluteevaluationhscm_positive) = S ((S (ff_index_mdm_prefix_mdr_secondwaveabsoluteevaluationhscm_positive)) * mdr_us_secondwaveabsoluteevaluationhsc)) /\ exists ff_q_mdm_mdr_secondwaveabsoluteevaluationhscm_positive_target. mdr_up_secondwaveabsoluteevaluationhsc = ff_q_mdm_mdr_secondwaveabsoluteevaluationhscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_secondwaveabsoluteevaluationhscm_positive)) * mdr_us_secondwaveabsoluteevaluationhsc) + (ff_value_mdm_prefix_mdr_secondwaveabsoluteevaluationhscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_secondwaveabsoluteevaluationhscm_negative. (exists ff_gap_mdm_lt_mdr_secondwaveabsoluteevaluationhscm_negative_index_bound. ff_gap_mdm_lt_mdr_secondwaveabsoluteevaluationhscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_secondwaveabsoluteevaluationhscm_negative) = ((mdr_q_secondwaveabsoluteevaluationhs) * (mdr_q_secondwaveabsoluteevaluationhs))) -> exists ff_row_mdm_prefix_mdr_secondwaveabsoluteevaluationhscm_negative ff_column_mdm_prefix_mdr_secondwaveabsoluteevaluationhscm_negative ff_value_mdm_prefix_mdr_secondwaveabsoluteevaluationhscm_negative. (ff_index_mdm_prefix_mdr_secondwaveabsoluteevaluationhscm_negative = (mdr_q_secondwaveabsoluteevaluationhs) * ff_row_mdm_prefix_mdr_secondwaveabsoluteevaluationhscm_negative + ff_column_mdm_prefix_mdr_secondwaveabsoluteevaluationhscm_negative /\ ((exists ff_gap_mdm_lt_mdr_secondwaveabsoluteevaluationhscm_negative_column_bound. ff_gap_mdm_lt_mdr_secondwaveabsoluteevaluationhscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_secondwaveabsoluteevaluationhscm_negative) = (mdr_q_secondwaveabsoluteevaluationhs)) /\ ((exists ff_row_mdm_cell_mdr_secondwaveabsoluteevaluationhscm_negative_cell ff_column_mdm_cell_mdr_secondwaveabsoluteevaluationhscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_secondwaveabsoluteevaluationhscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_secondwaveabsoluteevaluationhscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_secondwaveabsoluteevaluationhscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_secondwaveabsoluteevaluationhscm_negative_cell = ff_row_mdm_prefix_mdr_secondwaveabsoluteevaluationhscm_negative) \/ ((exists ff_gap_mdm_le_mdr_secondwaveabsoluteevaluationhscm_negative_cell_row_after. ff_gap_mdm_le_mdr_secondwaveabsoluteevaluationhscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_secondwaveabsoluteevaluationhscm_negative)) /\ ff_row_mdm_cell_mdr_secondwaveabsoluteevaluationhscm_negative_cell = S ff_row_mdm_prefix_mdr_secondwaveabsoluteevaluationhscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_secondwaveabsoluteevaluationhscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_secondwaveabsoluteevaluationhscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_secondwaveabsoluteevaluationhscm_negative) = (mdr_j_secondwaveabsoluteevaluationhsc)) /\ ff_column_mdm_cell_mdr_secondwaveabsoluteevaluationhscm_negative_cell = ff_column_mdm_prefix_mdr_secondwaveabsoluteevaluationhscm_negative) \/ ((exists ff_gap_mdm_le_mdr_secondwaveabsoluteevaluationhscm_negative_cell_column_after. ff_gap_mdm_le_mdr_secondwaveabsoluteevaluationhscm_negative_cell_column_after + (mdr_j_secondwaveabsoluteevaluationhsc) = (ff_column_mdm_prefix_mdr_secondwaveabsoluteevaluationhscm_negative)) /\ ff_column_mdm_cell_mdr_secondwaveabsoluteevaluationhscm_negative_cell = S ff_column_mdm_prefix_mdr_secondwaveabsoluteevaluationhscm_negative))) /\ (((exists ff_h_mdm_mdr_secondwaveabsoluteevaluationhscm_negative_cell_source. ff_h_mdm_mdr_secondwaveabsoluteevaluationhscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_secondwaveabsoluteevaluationhscm_negative) = S ((S ((ff_row_mdm_cell_mdr_secondwaveabsoluteevaluationhscm_negative_cell) * (S (mdr_q_secondwaveabsoluteevaluationhs)) + (ff_column_mdm_cell_mdr_secondwaveabsoluteevaluationhscm_negative_cell))) * mdr_nc_secondwaveabsoluteevaluationh)) /\ exists ff_q_mdm_mdr_secondwaveabsoluteevaluationhscm_negative_cell_source. mdr_nb_secondwaveabsoluteevaluationh = ff_q_mdm_mdr_secondwaveabsoluteevaluationhscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_secondwaveabsoluteevaluationhscm_negative_cell) * (S (mdr_q_secondwaveabsoluteevaluationhs)) + (ff_column_mdm_cell_mdr_secondwaveabsoluteevaluationhscm_negative_cell))) * mdr_nc_secondwaveabsoluteevaluationh) + (ff_value_mdm_prefix_mdr_secondwaveabsoluteevaluationhscm_negative)))))) /\ (((exists ff_h_mdm_mdr_secondwaveabsoluteevaluationhscm_negative_target. ff_h_mdm_mdr_secondwaveabsoluteevaluationhscm_negative_target + S (ff_value_mdm_prefix_mdr_secondwaveabsoluteevaluationhscm_negative) = S ((S (ff_index_mdm_prefix_mdr_secondwaveabsoluteevaluationhscm_negative)) * mdr_ut_secondwaveabsoluteevaluationhsc)) /\ exists ff_q_mdm_mdr_secondwaveabsoluteevaluationhscm_negative_target. mdr_un_secondwaveabsoluteevaluationhsc = ff_q_mdm_mdr_secondwaveabsoluteevaluationhscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_secondwaveabsoluteevaluationhscm_negative)) * mdr_ut_secondwaveabsoluteevaluationhsc) + (ff_value_mdm_prefix_mdr_secondwaveabsoluteevaluationhscm_negative))))))))) /\ ((((exists ff_h_mdr_secondwaveabsoluteevaluationhscp. ff_h_mdr_secondwaveabsoluteevaluationhscp + S (mdr_p_secondwaveabsoluteevaluationhsc) = S ((S (mdr_j_secondwaveabsoluteevaluationhsc)) * mdr_ec_secondwaveabsoluteevaluationhs)) /\ exists ff_q_mdr_secondwaveabsoluteevaluationhscp. mdr_eb_secondwaveabsoluteevaluationhs = ff_q_mdr_secondwaveabsoluteevaluationhscp * S ((S (mdr_j_secondwaveabsoluteevaluationhsc)) * mdr_ec_secondwaveabsoluteevaluationhs) + (mdr_p_secondwaveabsoluteevaluationhsc))) /\ (((exists ff_h_mdr_secondwaveabsoluteevaluationhscn. ff_h_mdr_secondwaveabsoluteevaluationhscn + S (mdr_n_secondwaveabsoluteevaluationhsc) = S ((S (mdr_j_secondwaveabsoluteevaluationhsc)) * mdr_fc_secondwaveabsoluteevaluationhs)) /\ exists ff_q_mdr_secondwaveabsoluteevaluationhscn. mdr_fb_secondwaveabsoluteevaluationhs = ff_q_mdr_secondwaveabsoluteevaluationhscn * S ((S (mdr_j_secondwaveabsoluteevaluationhsc)) * mdr_fc_secondwaveabsoluteevaluationhs) + (mdr_n_secondwaveabsoluteevaluationhsc)))))))) /\ (exists ff_ub_mce_fold_mdr_secondwaveabsoluteevaluationhsf ff_uc_mce_fold_mdr_secondwaveabsoluteevaluationhsf ff_vb_mce_fold_mdr_secondwaveabsoluteevaluationhsf ff_vc_mce_fold_mdr_secondwaveabsoluteevaluationhsf. ((forall ff_index_mce_alternating_mdr_secondwaveabsoluteevaluationhsf_prefix. (exists ff_gap_mce_mdr_secondwaveabsoluteevaluationhsf_prefix_index. ff_gap_mce_mdr_secondwaveabsoluteevaluationhsf_prefix_index + S (ff_index_mce_alternating_mdr_secondwaveabsoluteevaluationhsf_prefix) = (S (mdr_q_secondwaveabsoluteevaluationhs))) -> exists ff_ap_mce_alternating_mdr_secondwaveabsoluteevaluationhsf_prefix ff_an_mce_alternating_mdr_secondwaveabsoluteevaluationhsf_prefix ff_bp_mce_alternating_mdr_secondwaveabsoluteevaluationhsf_prefix ff_bn_mce_alternating_mdr_secondwaveabsoluteevaluationhsf_prefix ff_p_mce_alternating_mdr_secondwaveabsoluteevaluationhsf_prefix ff_n_mce_alternating_mdr_secondwaveabsoluteevaluationhsf_prefix. ((((exists ff_h_mce_mdr_secondwaveabsoluteevaluationhsf_prefix_ap. ff_h_mce_mdr_secondwaveabsoluteevaluationhsf_prefix_ap + S (ff_ap_mce_alternating_mdr_secondwaveabsoluteevaluationhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_secondwaveabsoluteevaluationhsf_prefix)) * mdr_pc_secondwaveabsoluteevaluationh)) /\ exists ff_q_mce_mdr_secondwaveabsoluteevaluationhsf_prefix_ap. mdr_pb_secondwaveabsoluteevaluationh = ff_q_mce_mdr_secondwaveabsoluteevaluationhsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_secondwaveabsoluteevaluationhsf_prefix)) * mdr_pc_secondwaveabsoluteevaluationh) + (ff_ap_mce_alternating_mdr_secondwaveabsoluteevaluationhsf_prefix))) /\ ((((exists ff_h_mce_mdr_secondwaveabsoluteevaluationhsf_prefix_an. ff_h_mce_mdr_secondwaveabsoluteevaluationhsf_prefix_an + S (ff_an_mce_alternating_mdr_secondwaveabsoluteevaluationhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_secondwaveabsoluteevaluationhsf_prefix)) * mdr_nc_secondwaveabsoluteevaluationh)) /\ exists ff_q_mce_mdr_secondwaveabsoluteevaluationhsf_prefix_an. mdr_nb_secondwaveabsoluteevaluationh = ff_q_mce_mdr_secondwaveabsoluteevaluationhsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_secondwaveabsoluteevaluationhsf_prefix)) * mdr_nc_secondwaveabsoluteevaluationh) + (ff_an_mce_alternating_mdr_secondwaveabsoluteevaluationhsf_prefix))) /\ ((((exists ff_h_mce_mdr_secondwaveabsoluteevaluationhsf_prefix_bp. ff_h_mce_mdr_secondwaveabsoluteevaluationhsf_prefix_bp + S (ff_bp_mce_alternating_mdr_secondwaveabsoluteevaluationhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_secondwaveabsoluteevaluationhsf_prefix)) * mdr_ec_secondwaveabsoluteevaluationhs)) /\ exists ff_q_mce_mdr_secondwaveabsoluteevaluationhsf_prefix_bp. mdr_eb_secondwaveabsoluteevaluationhs = ff_q_mce_mdr_secondwaveabsoluteevaluationhsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_secondwaveabsoluteevaluationhsf_prefix)) * mdr_ec_secondwaveabsoluteevaluationhs) + (ff_bp_mce_alternating_mdr_secondwaveabsoluteevaluationhsf_prefix))) /\ ((((exists ff_h_mce_mdr_secondwaveabsoluteevaluationhsf_prefix_bn. ff_h_mce_mdr_secondwaveabsoluteevaluationhsf_prefix_bn + S (ff_bn_mce_alternating_mdr_secondwaveabsoluteevaluationhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_secondwaveabsoluteevaluationhsf_prefix)) * mdr_fc_secondwaveabsoluteevaluationhs)) /\ exists ff_q_mce_mdr_secondwaveabsoluteevaluationhsf_prefix_bn. mdr_fb_secondwaveabsoluteevaluationhs = ff_q_mce_mdr_secondwaveabsoluteevaluationhsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_secondwaveabsoluteevaluationhsf_prefix)) * mdr_fc_secondwaveabsoluteevaluationhs) + (ff_bn_mce_alternating_mdr_secondwaveabsoluteevaluationhsf_prefix))) /\ ((((exists ff_h_mce_mdr_secondwaveabsoluteevaluationhsf_prefix_positive. ff_h_mce_mdr_secondwaveabsoluteevaluationhsf_prefix_positive + S (ff_p_mce_alternating_mdr_secondwaveabsoluteevaluationhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_secondwaveabsoluteevaluationhsf_prefix)) * ff_uc_mce_fold_mdr_secondwaveabsoluteevaluationhsf)) /\ exists ff_q_mce_mdr_secondwaveabsoluteevaluationhsf_prefix_positive. ff_ub_mce_fold_mdr_secondwaveabsoluteevaluationhsf = ff_q_mce_mdr_secondwaveabsoluteevaluationhsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_secondwaveabsoluteevaluationhsf_prefix)) * ff_uc_mce_fold_mdr_secondwaveabsoluteevaluationhsf) + (ff_p_mce_alternating_mdr_secondwaveabsoluteevaluationhsf_prefix))) /\ ((((exists ff_h_mce_mdr_secondwaveabsoluteevaluationhsf_prefix_negative. ff_h_mce_mdr_secondwaveabsoluteevaluationhsf_prefix_negative + S (ff_n_mce_alternating_mdr_secondwaveabsoluteevaluationhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_secondwaveabsoluteevaluationhsf_prefix)) * ff_vc_mce_fold_mdr_secondwaveabsoluteevaluationhsf)) /\ exists ff_q_mce_mdr_secondwaveabsoluteevaluationhsf_prefix_negative. ff_vb_mce_fold_mdr_secondwaveabsoluteevaluationhsf = ff_q_mce_mdr_secondwaveabsoluteevaluationhsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_secondwaveabsoluteevaluationhsf_prefix)) * ff_vc_mce_fold_mdr_secondwaveabsoluteevaluationhsf) + (ff_n_mce_alternating_mdr_secondwaveabsoluteevaluationhsf_prefix))) /\ (((exists ff_even_mce_term_mdr_secondwaveabsoluteevaluationhsf_prefix_term. ff_index_mce_alternating_mdr_secondwaveabsoluteevaluationhsf_prefix = 2 * ff_even_mce_term_mdr_secondwaveabsoluteevaluationhsf_prefix_term) /\ (ff_p_mce_alternating_mdr_secondwaveabsoluteevaluationhsf_prefix = (ff_ap_mce_alternating_mdr_secondwaveabsoluteevaluationhsf_prefix) * (ff_bp_mce_alternating_mdr_secondwaveabsoluteevaluationhsf_prefix) + (ff_an_mce_alternating_mdr_secondwaveabsoluteevaluationhsf_prefix) * (ff_bn_mce_alternating_mdr_secondwaveabsoluteevaluationhsf_prefix) /\ ff_n_mce_alternating_mdr_secondwaveabsoluteevaluationhsf_prefix = (ff_ap_mce_alternating_mdr_secondwaveabsoluteevaluationhsf_prefix) * (ff_bn_mce_alternating_mdr_secondwaveabsoluteevaluationhsf_prefix) + (ff_an_mce_alternating_mdr_secondwaveabsoluteevaluationhsf_prefix) * (ff_bp_mce_alternating_mdr_secondwaveabsoluteevaluationhsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_secondwaveabsoluteevaluationhsf_prefix_term. ff_index_mce_alternating_mdr_secondwaveabsoluteevaluationhsf_prefix = 2 * ff_odd_mce_term_mdr_secondwaveabsoluteevaluationhsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_secondwaveabsoluteevaluationhsf_prefix = (ff_ap_mce_alternating_mdr_secondwaveabsoluteevaluationhsf_prefix) * (ff_bn_mce_alternating_mdr_secondwaveabsoluteevaluationhsf_prefix) + (ff_an_mce_alternating_mdr_secondwaveabsoluteevaluationhsf_prefix) * (ff_bp_mce_alternating_mdr_secondwaveabsoluteevaluationhsf_prefix) /\ ff_n_mce_alternating_mdr_secondwaveabsoluteevaluationhsf_prefix = (ff_ap_mce_alternating_mdr_secondwaveabsoluteevaluationhsf_prefix) * (ff_bp_mce_alternating_mdr_secondwaveabsoluteevaluationhsf_prefix) + (ff_an_mce_alternating_mdr_secondwaveabsoluteevaluationhsf_prefix) * (ff_bn_mce_alternating_mdr_secondwaveabsoluteevaluationhsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_secondwaveabsoluteevaluationhsf_positive ff_v_mce_mdr_secondwaveabsoluteevaluationhsf_positive. ((((exists ff_h_mce_mdr_secondwaveabsoluteevaluationhsf_positive_start. ff_h_mce_mdr_secondwaveabsoluteevaluationhsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_secondwaveabsoluteevaluationhsf_positive)) /\ exists ff_q_mce_mdr_secondwaveabsoluteevaluationhsf_positive_start. ff_u_mce_mdr_secondwaveabsoluteevaluationhsf_positive = ff_q_mce_mdr_secondwaveabsoluteevaluationhsf_positive_start * S ((S (0)) * ff_v_mce_mdr_secondwaveabsoluteevaluationhsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_secondwaveabsoluteevaluationhsf_positive_terminal. ff_h_mce_mdr_secondwaveabsoluteevaluationhsf_positive_terminal + S (mdr_p_secondwaveabsoluteevaluationh) = S ((S ((S (mdr_q_secondwaveabsoluteevaluationhs)))) * ff_v_mce_mdr_secondwaveabsoluteevaluationhsf_positive)) /\ exists ff_q_mce_mdr_secondwaveabsoluteevaluationhsf_positive_terminal. ff_u_mce_mdr_secondwaveabsoluteevaluationhsf_positive = ff_q_mce_mdr_secondwaveabsoluteevaluationhsf_positive_terminal * S ((S ((S (mdr_q_secondwaveabsoluteevaluationhs)))) * ff_v_mce_mdr_secondwaveabsoluteevaluationhsf_positive) + (mdr_p_secondwaveabsoluteevaluationh))) /\ forall ff_i_mce_mdr_secondwaveabsoluteevaluationhsf_positive. (exists ff_lt_mce_mdr_secondwaveabsoluteevaluationhsf_positive_bound. ff_lt_mce_mdr_secondwaveabsoluteevaluationhsf_positive_bound + S ff_i_mce_mdr_secondwaveabsoluteevaluationhsf_positive = (S (mdr_q_secondwaveabsoluteevaluationhs))) -> exists ff_a_mce_mdr_secondwaveabsoluteevaluationhsf_positive ff_r_mce_mdr_secondwaveabsoluteevaluationhsf_positive ff_s_mce_mdr_secondwaveabsoluteevaluationhsf_positive. ((((exists ff_h_mce_mdr_secondwaveabsoluteevaluationhsf_positive_summand. ff_h_mce_mdr_secondwaveabsoluteevaluationhsf_positive_summand + S (ff_a_mce_mdr_secondwaveabsoluteevaluationhsf_positive) = S ((S (ff_i_mce_mdr_secondwaveabsoluteevaluationhsf_positive)) * ff_uc_mce_fold_mdr_secondwaveabsoluteevaluationhsf)) /\ exists ff_q_mce_mdr_secondwaveabsoluteevaluationhsf_positive_summand. ff_ub_mce_fold_mdr_secondwaveabsoluteevaluationhsf = ff_q_mce_mdr_secondwaveabsoluteevaluationhsf_positive_summand * S ((S (ff_i_mce_mdr_secondwaveabsoluteevaluationhsf_positive)) * ff_uc_mce_fold_mdr_secondwaveabsoluteevaluationhsf) + (ff_a_mce_mdr_secondwaveabsoluteevaluationhsf_positive))) /\ ((((exists ff_h_mce_mdr_secondwaveabsoluteevaluationhsf_positive_partial. ff_h_mce_mdr_secondwaveabsoluteevaluationhsf_positive_partial + S (ff_r_mce_mdr_secondwaveabsoluteevaluationhsf_positive) = S ((S (ff_i_mce_mdr_secondwaveabsoluteevaluationhsf_positive)) * ff_v_mce_mdr_secondwaveabsoluteevaluationhsf_positive)) /\ exists ff_q_mce_mdr_secondwaveabsoluteevaluationhsf_positive_partial. ff_u_mce_mdr_secondwaveabsoluteevaluationhsf_positive = ff_q_mce_mdr_secondwaveabsoluteevaluationhsf_positive_partial * S ((S (ff_i_mce_mdr_secondwaveabsoluteevaluationhsf_positive)) * ff_v_mce_mdr_secondwaveabsoluteevaluationhsf_positive) + (ff_r_mce_mdr_secondwaveabsoluteevaluationhsf_positive))) /\ ((((exists ff_h_mce_mdr_secondwaveabsoluteevaluationhsf_positive_successor. ff_h_mce_mdr_secondwaveabsoluteevaluationhsf_positive_successor + S (ff_s_mce_mdr_secondwaveabsoluteevaluationhsf_positive) = S ((S (S ff_i_mce_mdr_secondwaveabsoluteevaluationhsf_positive)) * ff_v_mce_mdr_secondwaveabsoluteevaluationhsf_positive)) /\ exists ff_q_mce_mdr_secondwaveabsoluteevaluationhsf_positive_successor. ff_u_mce_mdr_secondwaveabsoluteevaluationhsf_positive = ff_q_mce_mdr_secondwaveabsoluteevaluationhsf_positive_successor * S ((S (S ff_i_mce_mdr_secondwaveabsoluteevaluationhsf_positive)) * ff_v_mce_mdr_secondwaveabsoluteevaluationhsf_positive) + (ff_s_mce_mdr_secondwaveabsoluteevaluationhsf_positive))) /\ ff_s_mce_mdr_secondwaveabsoluteevaluationhsf_positive = ff_r_mce_mdr_secondwaveabsoluteevaluationhsf_positive + ff_a_mce_mdr_secondwaveabsoluteevaluationhsf_positive)))))) /\ (exists ff_u_mce_mdr_secondwaveabsoluteevaluationhsf_negative ff_v_mce_mdr_secondwaveabsoluteevaluationhsf_negative. ((((exists ff_h_mce_mdr_secondwaveabsoluteevaluationhsf_negative_start. ff_h_mce_mdr_secondwaveabsoluteevaluationhsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_secondwaveabsoluteevaluationhsf_negative)) /\ exists ff_q_mce_mdr_secondwaveabsoluteevaluationhsf_negative_start. ff_u_mce_mdr_secondwaveabsoluteevaluationhsf_negative = ff_q_mce_mdr_secondwaveabsoluteevaluationhsf_negative_start * S ((S (0)) * ff_v_mce_mdr_secondwaveabsoluteevaluationhsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_secondwaveabsoluteevaluationhsf_negative_terminal. ff_h_mce_mdr_secondwaveabsoluteevaluationhsf_negative_terminal + S (mdr_n_secondwaveabsoluteevaluationh) = S ((S ((S (mdr_q_secondwaveabsoluteevaluationhs)))) * ff_v_mce_mdr_secondwaveabsoluteevaluationhsf_negative)) /\ exists ff_q_mce_mdr_secondwaveabsoluteevaluationhsf_negative_terminal. ff_u_mce_mdr_secondwaveabsoluteevaluationhsf_negative = ff_q_mce_mdr_secondwaveabsoluteevaluationhsf_negative_terminal * S ((S ((S (mdr_q_secondwaveabsoluteevaluationhs)))) * ff_v_mce_mdr_secondwaveabsoluteevaluationhsf_negative) + (mdr_n_secondwaveabsoluteevaluationh))) /\ forall ff_i_mce_mdr_secondwaveabsoluteevaluationhsf_negative. (exists ff_lt_mce_mdr_secondwaveabsoluteevaluationhsf_negative_bound. ff_lt_mce_mdr_secondwaveabsoluteevaluationhsf_negative_bound + S ff_i_mce_mdr_secondwaveabsoluteevaluationhsf_negative = (S (mdr_q_secondwaveabsoluteevaluationhs))) -> exists ff_a_mce_mdr_secondwaveabsoluteevaluationhsf_negative ff_r_mce_mdr_secondwaveabsoluteevaluationhsf_negative ff_s_mce_mdr_secondwaveabsoluteevaluationhsf_negative. ((((exists ff_h_mce_mdr_secondwaveabsoluteevaluationhsf_negative_summand. ff_h_mce_mdr_secondwaveabsoluteevaluationhsf_negative_summand + S (ff_a_mce_mdr_secondwaveabsoluteevaluationhsf_negative) = S ((S (ff_i_mce_mdr_secondwaveabsoluteevaluationhsf_negative)) * ff_vc_mce_fold_mdr_secondwaveabsoluteevaluationhsf)) /\ exists ff_q_mce_mdr_secondwaveabsoluteevaluationhsf_negative_summand. ff_vb_mce_fold_mdr_secondwaveabsoluteevaluationhsf = ff_q_mce_mdr_secondwaveabsoluteevaluationhsf_negative_summand * S ((S (ff_i_mce_mdr_secondwaveabsoluteevaluationhsf_negative)) * ff_vc_mce_fold_mdr_secondwaveabsoluteevaluationhsf) + (ff_a_mce_mdr_secondwaveabsoluteevaluationhsf_negative))) /\ ((((exists ff_h_mce_mdr_secondwaveabsoluteevaluationhsf_negative_partial. ff_h_mce_mdr_secondwaveabsoluteevaluationhsf_negative_partial + S (ff_r_mce_mdr_secondwaveabsoluteevaluationhsf_negative) = S ((S (ff_i_mce_mdr_secondwaveabsoluteevaluationhsf_negative)) * ff_v_mce_mdr_secondwaveabsoluteevaluationhsf_negative)) /\ exists ff_q_mce_mdr_secondwaveabsoluteevaluationhsf_negative_partial. ff_u_mce_mdr_secondwaveabsoluteevaluationhsf_negative = ff_q_mce_mdr_secondwaveabsoluteevaluationhsf_negative_partial * S ((S (ff_i_mce_mdr_secondwaveabsoluteevaluationhsf_negative)) * ff_v_mce_mdr_secondwaveabsoluteevaluationhsf_negative) + (ff_r_mce_mdr_secondwaveabsoluteevaluationhsf_negative))) /\ ((((exists ff_h_mce_mdr_secondwaveabsoluteevaluationhsf_negative_successor. ff_h_mce_mdr_secondwaveabsoluteevaluationhsf_negative_successor + S (ff_s_mce_mdr_secondwaveabsoluteevaluationhsf_negative) = S ((S (S ff_i_mce_mdr_secondwaveabsoluteevaluationhsf_negative)) * ff_v_mce_mdr_secondwaveabsoluteevaluationhsf_negative)) /\ exists ff_q_mce_mdr_secondwaveabsoluteevaluationhsf_negative_successor. ff_u_mce_mdr_secondwaveabsoluteevaluationhsf_negative = ff_q_mce_mdr_secondwaveabsoluteevaluationhsf_negative_successor * S ((S (S ff_i_mce_mdr_secondwaveabsoluteevaluationhsf_negative)) * ff_v_mce_mdr_secondwaveabsoluteevaluationhsf_negative) + (ff_s_mce_mdr_secondwaveabsoluteevaluationhsf_negative))) /\ ff_s_mce_mdr_secondwaveabsoluteevaluationhsf_negative = ff_r_mce_mdr_secondwaveabsoluteevaluationhsf_negative + ff_a_mce_mdr_secondwaveabsoluteevaluationhsf_negative))))))))))))))) /\ ((exists mdr_gap_secondwaveabsoluteevaluationi. mdr_gap_secondwaveabsoluteevaluationi + S (mdr_i_secondwaveabsoluteevaluation) = (mdr_l_secondwaveabsoluteevaluation)) /\ (exists mdr_z_secondwaveabsoluteevaluationr. ((exists mdr_a_secondwaveabsoluteevaluationrc mdr_b_secondwaveabsoluteevaluationrc mdr_c_secondwaveabsoluteevaluationrc mdr_e_secondwaveabsoluteevaluationrc mdr_f_secondwaveabsoluteevaluationrc. ((mdr_a_secondwaveabsoluteevaluationrc = ((d) + (ab)) * S ((d) + (ab)) + ((ab) + (ab))) /\ ((mdr_b_secondwaveabsoluteevaluationrc = ((ac) + (bb)) * S ((ac) + (bb)) + ((bb) + (bb))) /\ ((mdr_c_secondwaveabsoluteevaluationrc = ((mdr_a_secondwaveabsoluteevaluationrc) + (mdr_b_secondwaveabsoluteevaluationrc)) * S ((mdr_a_secondwaveabsoluteevaluationrc) + (mdr_b_secondwaveabsoluteevaluationrc)) + ((mdr_b_secondwaveabsoluteevaluationrc) + (mdr_b_secondwaveabsoluteevaluationrc))) /\ ((mdr_e_secondwaveabsoluteevaluationrc = ((mdr_p_secondwaveabsolute) + (mdr_n_secondwaveabsolute)) * S ((mdr_p_secondwaveabsolute) + (mdr_n_secondwaveabsolute)) + ((mdr_n_secondwaveabsolute) + (mdr_n_secondwaveabsolute))) /\ ((mdr_f_secondwaveabsoluteevaluationrc = ((bc) + (mdr_e_secondwaveabsoluteevaluationrc)) * S ((bc) + (mdr_e_secondwaveabsoluteevaluationrc)) + ((mdr_e_secondwaveabsoluteevaluationrc) + (mdr_e_secondwaveabsoluteevaluationrc))) /\ ((mdr_z_secondwaveabsoluteevaluationr) = ((mdr_c_secondwaveabsoluteevaluationrc) + (mdr_f_secondwaveabsoluteevaluationrc)) * S ((mdr_c_secondwaveabsoluteevaluationrc) + (mdr_f_secondwaveabsoluteevaluationrc)) + ((mdr_f_secondwaveabsoluteevaluationrc) + (mdr_f_secondwaveabsoluteevaluationrc))))))))) /\ (((exists ff_h_mdr_secondwaveabsoluteevaluationrb. ff_h_mdr_secondwaveabsoluteevaluationrb + S (mdr_z_secondwaveabsoluteevaluationr) = S ((S (mdr_i_secondwaveabsoluteevaluation)) * mdr_c_secondwaveabsoluteevaluation)) /\ exists ff_q_mdr_secondwaveabsoluteevaluationrb. mdr_b_secondwaveabsoluteevaluation = ff_q_mdr_secondwaveabsoluteevaluationrb * S ((S (mdr_i_secondwaveabsoluteevaluation)) * mdr_c_secondwaveabsoluteevaluation) + (mdr_z_secondwaveabsoluteevaluationr)))))))) /\ (((mdr_p_secondwaveabsolute) = (mdr_n_secondwaveabsolute) + (D)) \/ ((mdr_n_secondwaveabsolute) = (mdr_p_secondwaveabsolute) + (D)))))))

The unchanged native kernel never receives this surface symbol. Binder-safe expansion produces only its existing first-order syntax.