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

exists mdr_p_secondwave mdr_n_secondwave. ((exists mdr_b_secondwaveevaluation mdr_c_secondwaveevaluation mdr_l_secondwaveevaluation mdr_i_secondwaveevaluation. ((forall mdr_i_secondwaveevaluationh. (exists mdr_gap_secondwaveevaluationhi. mdr_gap_secondwaveevaluationhi + S (mdr_i_secondwaveevaluationh) = (mdr_l_secondwaveevaluation)) -> exists mdr_d_secondwaveevaluationh mdr_pb_secondwaveevaluationh mdr_pc_secondwaveevaluationh mdr_nb_secondwaveevaluationh mdr_nc_secondwaveevaluationh mdr_p_secondwaveevaluationh mdr_n_secondwaveevaluationh. ((exists mdr_z_secondwaveevaluationhr. ((exists mdr_a_secondwaveevaluationhrc mdr_b_secondwaveevaluationhrc mdr_c_secondwaveevaluationhrc mdr_e_secondwaveevaluationhrc mdr_f_secondwaveevaluationhrc. ((mdr_a_secondwaveevaluationhrc = ((mdr_d_secondwaveevaluationh) + (mdr_pb_secondwaveevaluationh)) * S ((mdr_d_secondwaveevaluationh) + (mdr_pb_secondwaveevaluationh)) + ((mdr_pb_secondwaveevaluationh) + (mdr_pb_secondwaveevaluationh))) /\ ((mdr_b_secondwaveevaluationhrc = ((mdr_pc_secondwaveevaluationh) + (mdr_nb_secondwaveevaluationh)) * S ((mdr_pc_secondwaveevaluationh) + (mdr_nb_secondwaveevaluationh)) + ((mdr_nb_secondwaveevaluationh) + (mdr_nb_secondwaveevaluationh))) /\ ((mdr_c_secondwaveevaluationhrc = ((mdr_a_secondwaveevaluationhrc) + (mdr_b_secondwaveevaluationhrc)) * S ((mdr_a_secondwaveevaluationhrc) + (mdr_b_secondwaveevaluationhrc)) + ((mdr_b_secondwaveevaluationhrc) + (mdr_b_secondwaveevaluationhrc))) /\ ((mdr_e_secondwaveevaluationhrc = ((mdr_p_secondwaveevaluationh) + (mdr_n_secondwaveevaluationh)) * S ((mdr_p_secondwaveevaluationh) + (mdr_n_secondwaveevaluationh)) + ((mdr_n_secondwaveevaluationh) + (mdr_n_secondwaveevaluationh))) /\ ((mdr_f_secondwaveevaluationhrc = ((mdr_nc_secondwaveevaluationh) + (mdr_e_secondwaveevaluationhrc)) * S ((mdr_nc_secondwaveevaluationh) + (mdr_e_secondwaveevaluationhrc)) + ((mdr_e_secondwaveevaluationhrc) + (mdr_e_secondwaveevaluationhrc))) /\ ((mdr_z_secondwaveevaluationhr) = ((mdr_c_secondwaveevaluationhrc) + (mdr_f_secondwaveevaluationhrc)) * S ((mdr_c_secondwaveevaluationhrc) + (mdr_f_secondwaveevaluationhrc)) + ((mdr_f_secondwaveevaluationhrc) + (mdr_f_secondwaveevaluationhrc))))))))) /\ (((exists ff_h_mdr_secondwaveevaluationhrb. ff_h_mdr_secondwaveevaluationhrb + S (mdr_z_secondwaveevaluationhr) = S ((S (mdr_i_secondwaveevaluationh)) * mdr_c_secondwaveevaluation)) /\ exists ff_q_mdr_secondwaveevaluationhrb. mdr_b_secondwaveevaluation = ff_q_mdr_secondwaveevaluationhrb * S ((S (mdr_i_secondwaveevaluationh)) * mdr_c_secondwaveevaluation) + (mdr_z_secondwaveevaluationhr))))) /\ (((((mdr_d_secondwaveevaluationh) = 0) /\ (((mdr_p_secondwaveevaluationh) = 1) /\ ((mdr_n_secondwaveevaluationh) = 0))) \/ exists mdr_q_secondwaveevaluationhs mdr_eb_secondwaveevaluationhs mdr_ec_secondwaveevaluationhs mdr_fb_secondwaveevaluationhs mdr_fc_secondwaveevaluationhs. (((mdr_d_secondwaveevaluationh) = S (mdr_q_secondwaveevaluationhs)) /\ ((forall mdr_j_secondwaveevaluationhsc. (exists mdr_gap_secondwaveevaluationhscj. mdr_gap_secondwaveevaluationhscj + S (mdr_j_secondwaveevaluationhsc) = (S (mdr_q_secondwaveevaluationhs))) -> exists mdr_i_secondwaveevaluationhsc mdr_up_secondwaveevaluationhsc mdr_us_secondwaveevaluationhsc mdr_un_secondwaveevaluationhsc mdr_ut_secondwaveevaluationhsc mdr_p_secondwaveevaluationhsc mdr_n_secondwaveevaluationhsc. ((exists mdr_gap_secondwaveevaluationhsci. mdr_gap_secondwaveevaluationhsci + S (mdr_i_secondwaveevaluationhsc) = (mdr_i_secondwaveevaluationh)) /\ ((exists mdr_z_secondwaveevaluationhscr. ((exists mdr_a_secondwaveevaluationhscrc mdr_b_secondwaveevaluationhscrc mdr_c_secondwaveevaluationhscrc mdr_e_secondwaveevaluationhscrc mdr_f_secondwaveevaluationhscrc. ((mdr_a_secondwaveevaluationhscrc = ((mdr_q_secondwaveevaluationhs) + (mdr_up_secondwaveevaluationhsc)) * S ((mdr_q_secondwaveevaluationhs) + (mdr_up_secondwaveevaluationhsc)) + ((mdr_up_secondwaveevaluationhsc) + (mdr_up_secondwaveevaluationhsc))) /\ ((mdr_b_secondwaveevaluationhscrc = ((mdr_us_secondwaveevaluationhsc) + (mdr_un_secondwaveevaluationhsc)) * S ((mdr_us_secondwaveevaluationhsc) + (mdr_un_secondwaveevaluationhsc)) + ((mdr_un_secondwaveevaluationhsc) + (mdr_un_secondwaveevaluationhsc))) /\ ((mdr_c_secondwaveevaluationhscrc = ((mdr_a_secondwaveevaluationhscrc) + (mdr_b_secondwaveevaluationhscrc)) * S ((mdr_a_secondwaveevaluationhscrc) + (mdr_b_secondwaveevaluationhscrc)) + ((mdr_b_secondwaveevaluationhscrc) + (mdr_b_secondwaveevaluationhscrc))) /\ ((mdr_e_secondwaveevaluationhscrc = ((mdr_p_secondwaveevaluationhsc) + (mdr_n_secondwaveevaluationhsc)) * S ((mdr_p_secondwaveevaluationhsc) + (mdr_n_secondwaveevaluationhsc)) + ((mdr_n_secondwaveevaluationhsc) + (mdr_n_secondwaveevaluationhsc))) /\ ((mdr_f_secondwaveevaluationhscrc = ((mdr_ut_secondwaveevaluationhsc) + (mdr_e_secondwaveevaluationhscrc)) * S ((mdr_ut_secondwaveevaluationhsc) + (mdr_e_secondwaveevaluationhscrc)) + ((mdr_e_secondwaveevaluationhscrc) + (mdr_e_secondwaveevaluationhscrc))) /\ ((mdr_z_secondwaveevaluationhscr) = ((mdr_c_secondwaveevaluationhscrc) + (mdr_f_secondwaveevaluationhscrc)) * S ((mdr_c_secondwaveevaluationhscrc) + (mdr_f_secondwaveevaluationhscrc)) + ((mdr_f_secondwaveevaluationhscrc) + (mdr_f_secondwaveevaluationhscrc))))))))) /\ (((exists ff_h_mdr_secondwaveevaluationhscrb. ff_h_mdr_secondwaveevaluationhscrb + S (mdr_z_secondwaveevaluationhscr) = S ((S (mdr_i_secondwaveevaluationhsc)) * mdr_c_secondwaveevaluation)) /\ exists ff_q_mdr_secondwaveevaluationhscrb. mdr_b_secondwaveevaluation = ff_q_mdr_secondwaveevaluationhscrb * S ((S (mdr_i_secondwaveevaluationhsc)) * mdr_c_secondwaveevaluation) + (mdr_z_secondwaveevaluationhscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_secondwaveevaluationhscm_positive. (exists ff_gap_mdm_lt_mdr_secondwaveevaluationhscm_positive_index_bound. ff_gap_mdm_lt_mdr_secondwaveevaluationhscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_secondwaveevaluationhscm_positive) = ((mdr_q_secondwaveevaluationhs) * (mdr_q_secondwaveevaluationhs))) -> exists ff_row_mdm_prefix_mdr_secondwaveevaluationhscm_positive ff_column_mdm_prefix_mdr_secondwaveevaluationhscm_positive ff_value_mdm_prefix_mdr_secondwaveevaluationhscm_positive. (ff_index_mdm_prefix_mdr_secondwaveevaluationhscm_positive = (mdr_q_secondwaveevaluationhs) * ff_row_mdm_prefix_mdr_secondwaveevaluationhscm_positive + ff_column_mdm_prefix_mdr_secondwaveevaluationhscm_positive /\ ((exists ff_gap_mdm_lt_mdr_secondwaveevaluationhscm_positive_column_bound. ff_gap_mdm_lt_mdr_secondwaveevaluationhscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_secondwaveevaluationhscm_positive) = (mdr_q_secondwaveevaluationhs)) /\ ((exists ff_row_mdm_cell_mdr_secondwaveevaluationhscm_positive_cell ff_column_mdm_cell_mdr_secondwaveevaluationhscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_secondwaveevaluationhscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_secondwaveevaluationhscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_secondwaveevaluationhscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_secondwaveevaluationhscm_positive_cell = ff_row_mdm_prefix_mdr_secondwaveevaluationhscm_positive) \/ ((exists ff_gap_mdm_le_mdr_secondwaveevaluationhscm_positive_cell_row_after. ff_gap_mdm_le_mdr_secondwaveevaluationhscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_secondwaveevaluationhscm_positive)) /\ ff_row_mdm_cell_mdr_secondwaveevaluationhscm_positive_cell = S ff_row_mdm_prefix_mdr_secondwaveevaluationhscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_secondwaveevaluationhscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_secondwaveevaluationhscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_secondwaveevaluationhscm_positive) = (mdr_j_secondwaveevaluationhsc)) /\ ff_column_mdm_cell_mdr_secondwaveevaluationhscm_positive_cell = ff_column_mdm_prefix_mdr_secondwaveevaluationhscm_positive) \/ ((exists ff_gap_mdm_le_mdr_secondwaveevaluationhscm_positive_cell_column_after. ff_gap_mdm_le_mdr_secondwaveevaluationhscm_positive_cell_column_after + (mdr_j_secondwaveevaluationhsc) = (ff_column_mdm_prefix_mdr_secondwaveevaluationhscm_positive)) /\ ff_column_mdm_cell_mdr_secondwaveevaluationhscm_positive_cell = S ff_column_mdm_prefix_mdr_secondwaveevaluationhscm_positive))) /\ (((exists ff_h_mdm_mdr_secondwaveevaluationhscm_positive_cell_source. ff_h_mdm_mdr_secondwaveevaluationhscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_secondwaveevaluationhscm_positive) = S ((S ((ff_row_mdm_cell_mdr_secondwaveevaluationhscm_positive_cell) * (S (mdr_q_secondwaveevaluationhs)) + (ff_column_mdm_cell_mdr_secondwaveevaluationhscm_positive_cell))) * mdr_pc_secondwaveevaluationh)) /\ exists ff_q_mdm_mdr_secondwaveevaluationhscm_positive_cell_source. mdr_pb_secondwaveevaluationh = ff_q_mdm_mdr_secondwaveevaluationhscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_secondwaveevaluationhscm_positive_cell) * (S (mdr_q_secondwaveevaluationhs)) + (ff_column_mdm_cell_mdr_secondwaveevaluationhscm_positive_cell))) * mdr_pc_secondwaveevaluationh) + (ff_value_mdm_prefix_mdr_secondwaveevaluationhscm_positive)))))) /\ (((exists ff_h_mdm_mdr_secondwaveevaluationhscm_positive_target. ff_h_mdm_mdr_secondwaveevaluationhscm_positive_target + S (ff_value_mdm_prefix_mdr_secondwaveevaluationhscm_positive) = S ((S (ff_index_mdm_prefix_mdr_secondwaveevaluationhscm_positive)) * mdr_us_secondwaveevaluationhsc)) /\ exists ff_q_mdm_mdr_secondwaveevaluationhscm_positive_target. mdr_up_secondwaveevaluationhsc = ff_q_mdm_mdr_secondwaveevaluationhscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_secondwaveevaluationhscm_positive)) * mdr_us_secondwaveevaluationhsc) + (ff_value_mdm_prefix_mdr_secondwaveevaluationhscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_secondwaveevaluationhscm_negative. (exists ff_gap_mdm_lt_mdr_secondwaveevaluationhscm_negative_index_bound. ff_gap_mdm_lt_mdr_secondwaveevaluationhscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_secondwaveevaluationhscm_negative) = ((mdr_q_secondwaveevaluationhs) * (mdr_q_secondwaveevaluationhs))) -> exists ff_row_mdm_prefix_mdr_secondwaveevaluationhscm_negative ff_column_mdm_prefix_mdr_secondwaveevaluationhscm_negative ff_value_mdm_prefix_mdr_secondwaveevaluationhscm_negative. (ff_index_mdm_prefix_mdr_secondwaveevaluationhscm_negative = (mdr_q_secondwaveevaluationhs) * ff_row_mdm_prefix_mdr_secondwaveevaluationhscm_negative + ff_column_mdm_prefix_mdr_secondwaveevaluationhscm_negative /\ ((exists ff_gap_mdm_lt_mdr_secondwaveevaluationhscm_negative_column_bound. ff_gap_mdm_lt_mdr_secondwaveevaluationhscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_secondwaveevaluationhscm_negative) = (mdr_q_secondwaveevaluationhs)) /\ ((exists ff_row_mdm_cell_mdr_secondwaveevaluationhscm_negative_cell ff_column_mdm_cell_mdr_secondwaveevaluationhscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_secondwaveevaluationhscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_secondwaveevaluationhscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_secondwaveevaluationhscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_secondwaveevaluationhscm_negative_cell = ff_row_mdm_prefix_mdr_secondwaveevaluationhscm_negative) \/ ((exists ff_gap_mdm_le_mdr_secondwaveevaluationhscm_negative_cell_row_after. ff_gap_mdm_le_mdr_secondwaveevaluationhscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_secondwaveevaluationhscm_negative)) /\ ff_row_mdm_cell_mdr_secondwaveevaluationhscm_negative_cell = S ff_row_mdm_prefix_mdr_secondwaveevaluationhscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_secondwaveevaluationhscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_secondwaveevaluationhscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_secondwaveevaluationhscm_negative) = (mdr_j_secondwaveevaluationhsc)) /\ ff_column_mdm_cell_mdr_secondwaveevaluationhscm_negative_cell = ff_column_mdm_prefix_mdr_secondwaveevaluationhscm_negative) \/ ((exists ff_gap_mdm_le_mdr_secondwaveevaluationhscm_negative_cell_column_after. ff_gap_mdm_le_mdr_secondwaveevaluationhscm_negative_cell_column_after + (mdr_j_secondwaveevaluationhsc) = (ff_column_mdm_prefix_mdr_secondwaveevaluationhscm_negative)) /\ ff_column_mdm_cell_mdr_secondwaveevaluationhscm_negative_cell = S ff_column_mdm_prefix_mdr_secondwaveevaluationhscm_negative))) /\ (((exists ff_h_mdm_mdr_secondwaveevaluationhscm_negative_cell_source. ff_h_mdm_mdr_secondwaveevaluationhscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_secondwaveevaluationhscm_negative) = S ((S ((ff_row_mdm_cell_mdr_secondwaveevaluationhscm_negative_cell) * (S (mdr_q_secondwaveevaluationhs)) + (ff_column_mdm_cell_mdr_secondwaveevaluationhscm_negative_cell))) * mdr_nc_secondwaveevaluationh)) /\ exists ff_q_mdm_mdr_secondwaveevaluationhscm_negative_cell_source. mdr_nb_secondwaveevaluationh = ff_q_mdm_mdr_secondwaveevaluationhscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_secondwaveevaluationhscm_negative_cell) * (S (mdr_q_secondwaveevaluationhs)) + (ff_column_mdm_cell_mdr_secondwaveevaluationhscm_negative_cell))) * mdr_nc_secondwaveevaluationh) + (ff_value_mdm_prefix_mdr_secondwaveevaluationhscm_negative)))))) /\ (((exists ff_h_mdm_mdr_secondwaveevaluationhscm_negative_target. ff_h_mdm_mdr_secondwaveevaluationhscm_negative_target + S (ff_value_mdm_prefix_mdr_secondwaveevaluationhscm_negative) = S ((S (ff_index_mdm_prefix_mdr_secondwaveevaluationhscm_negative)) * mdr_ut_secondwaveevaluationhsc)) /\ exists ff_q_mdm_mdr_secondwaveevaluationhscm_negative_target. mdr_un_secondwaveevaluationhsc = ff_q_mdm_mdr_secondwaveevaluationhscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_secondwaveevaluationhscm_negative)) * mdr_ut_secondwaveevaluationhsc) + (ff_value_mdm_prefix_mdr_secondwaveevaluationhscm_negative))))))))) /\ ((((exists ff_h_mdr_secondwaveevaluationhscp. ff_h_mdr_secondwaveevaluationhscp + S (mdr_p_secondwaveevaluationhsc) = S ((S (mdr_j_secondwaveevaluationhsc)) * mdr_ec_secondwaveevaluationhs)) /\ exists ff_q_mdr_secondwaveevaluationhscp. mdr_eb_secondwaveevaluationhs = ff_q_mdr_secondwaveevaluationhscp * S ((S (mdr_j_secondwaveevaluationhsc)) * mdr_ec_secondwaveevaluationhs) + (mdr_p_secondwaveevaluationhsc))) /\ (((exists ff_h_mdr_secondwaveevaluationhscn. ff_h_mdr_secondwaveevaluationhscn + S (mdr_n_secondwaveevaluationhsc) = S ((S (mdr_j_secondwaveevaluationhsc)) * mdr_fc_secondwaveevaluationhs)) /\ exists ff_q_mdr_secondwaveevaluationhscn. mdr_fb_secondwaveevaluationhs = ff_q_mdr_secondwaveevaluationhscn * S ((S (mdr_j_secondwaveevaluationhsc)) * mdr_fc_secondwaveevaluationhs) + (mdr_n_secondwaveevaluationhsc)))))))) /\ (exists ff_ub_mce_fold_mdr_secondwaveevaluationhsf ff_uc_mce_fold_mdr_secondwaveevaluationhsf ff_vb_mce_fold_mdr_secondwaveevaluationhsf ff_vc_mce_fold_mdr_secondwaveevaluationhsf. ((forall ff_index_mce_alternating_mdr_secondwaveevaluationhsf_prefix. (exists ff_gap_mce_mdr_secondwaveevaluationhsf_prefix_index. ff_gap_mce_mdr_secondwaveevaluationhsf_prefix_index + S (ff_index_mce_alternating_mdr_secondwaveevaluationhsf_prefix) = (S (mdr_q_secondwaveevaluationhs))) -> exists ff_ap_mce_alternating_mdr_secondwaveevaluationhsf_prefix ff_an_mce_alternating_mdr_secondwaveevaluationhsf_prefix ff_bp_mce_alternating_mdr_secondwaveevaluationhsf_prefix ff_bn_mce_alternating_mdr_secondwaveevaluationhsf_prefix ff_p_mce_alternating_mdr_secondwaveevaluationhsf_prefix ff_n_mce_alternating_mdr_secondwaveevaluationhsf_prefix. ((((exists ff_h_mce_mdr_secondwaveevaluationhsf_prefix_ap. ff_h_mce_mdr_secondwaveevaluationhsf_prefix_ap + S (ff_ap_mce_alternating_mdr_secondwaveevaluationhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_secondwaveevaluationhsf_prefix)) * mdr_pc_secondwaveevaluationh)) /\ exists ff_q_mce_mdr_secondwaveevaluationhsf_prefix_ap. mdr_pb_secondwaveevaluationh = ff_q_mce_mdr_secondwaveevaluationhsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_secondwaveevaluationhsf_prefix)) * mdr_pc_secondwaveevaluationh) + (ff_ap_mce_alternating_mdr_secondwaveevaluationhsf_prefix))) /\ ((((exists ff_h_mce_mdr_secondwaveevaluationhsf_prefix_an. ff_h_mce_mdr_secondwaveevaluationhsf_prefix_an + S (ff_an_mce_alternating_mdr_secondwaveevaluationhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_secondwaveevaluationhsf_prefix)) * mdr_nc_secondwaveevaluationh)) /\ exists ff_q_mce_mdr_secondwaveevaluationhsf_prefix_an. mdr_nb_secondwaveevaluationh = ff_q_mce_mdr_secondwaveevaluationhsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_secondwaveevaluationhsf_prefix)) * mdr_nc_secondwaveevaluationh) + (ff_an_mce_alternating_mdr_secondwaveevaluationhsf_prefix))) /\ ((((exists ff_h_mce_mdr_secondwaveevaluationhsf_prefix_bp. ff_h_mce_mdr_secondwaveevaluationhsf_prefix_bp + S (ff_bp_mce_alternating_mdr_secondwaveevaluationhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_secondwaveevaluationhsf_prefix)) * mdr_ec_secondwaveevaluationhs)) /\ exists ff_q_mce_mdr_secondwaveevaluationhsf_prefix_bp. mdr_eb_secondwaveevaluationhs = ff_q_mce_mdr_secondwaveevaluationhsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_secondwaveevaluationhsf_prefix)) * mdr_ec_secondwaveevaluationhs) + (ff_bp_mce_alternating_mdr_secondwaveevaluationhsf_prefix))) /\ ((((exists ff_h_mce_mdr_secondwaveevaluationhsf_prefix_bn. ff_h_mce_mdr_secondwaveevaluationhsf_prefix_bn + S (ff_bn_mce_alternating_mdr_secondwaveevaluationhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_secondwaveevaluationhsf_prefix)) * mdr_fc_secondwaveevaluationhs)) /\ exists ff_q_mce_mdr_secondwaveevaluationhsf_prefix_bn. mdr_fb_secondwaveevaluationhs = ff_q_mce_mdr_secondwaveevaluationhsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_secondwaveevaluationhsf_prefix)) * mdr_fc_secondwaveevaluationhs) + (ff_bn_mce_alternating_mdr_secondwaveevaluationhsf_prefix))) /\ ((((exists ff_h_mce_mdr_secondwaveevaluationhsf_prefix_positive. ff_h_mce_mdr_secondwaveevaluationhsf_prefix_positive + S (ff_p_mce_alternating_mdr_secondwaveevaluationhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_secondwaveevaluationhsf_prefix)) * ff_uc_mce_fold_mdr_secondwaveevaluationhsf)) /\ exists ff_q_mce_mdr_secondwaveevaluationhsf_prefix_positive. ff_ub_mce_fold_mdr_secondwaveevaluationhsf = ff_q_mce_mdr_secondwaveevaluationhsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_secondwaveevaluationhsf_prefix)) * ff_uc_mce_fold_mdr_secondwaveevaluationhsf) + (ff_p_mce_alternating_mdr_secondwaveevaluationhsf_prefix))) /\ ((((exists ff_h_mce_mdr_secondwaveevaluationhsf_prefix_negative. ff_h_mce_mdr_secondwaveevaluationhsf_prefix_negative + S (ff_n_mce_alternating_mdr_secondwaveevaluationhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_secondwaveevaluationhsf_prefix)) * ff_vc_mce_fold_mdr_secondwaveevaluationhsf)) /\ exists ff_q_mce_mdr_secondwaveevaluationhsf_prefix_negative. ff_vb_mce_fold_mdr_secondwaveevaluationhsf = ff_q_mce_mdr_secondwaveevaluationhsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_secondwaveevaluationhsf_prefix)) * ff_vc_mce_fold_mdr_secondwaveevaluationhsf) + (ff_n_mce_alternating_mdr_secondwaveevaluationhsf_prefix))) /\ (((exists ff_even_mce_term_mdr_secondwaveevaluationhsf_prefix_term. ff_index_mce_alternating_mdr_secondwaveevaluationhsf_prefix = 2 * ff_even_mce_term_mdr_secondwaveevaluationhsf_prefix_term) /\ (ff_p_mce_alternating_mdr_secondwaveevaluationhsf_prefix = (ff_ap_mce_alternating_mdr_secondwaveevaluationhsf_prefix) * (ff_bp_mce_alternating_mdr_secondwaveevaluationhsf_prefix) + (ff_an_mce_alternating_mdr_secondwaveevaluationhsf_prefix) * (ff_bn_mce_alternating_mdr_secondwaveevaluationhsf_prefix) /\ ff_n_mce_alternating_mdr_secondwaveevaluationhsf_prefix = (ff_ap_mce_alternating_mdr_secondwaveevaluationhsf_prefix) * (ff_bn_mce_alternating_mdr_secondwaveevaluationhsf_prefix) + (ff_an_mce_alternating_mdr_secondwaveevaluationhsf_prefix) * (ff_bp_mce_alternating_mdr_secondwaveevaluationhsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_secondwaveevaluationhsf_prefix_term. ff_index_mce_alternating_mdr_secondwaveevaluationhsf_prefix = 2 * ff_odd_mce_term_mdr_secondwaveevaluationhsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_secondwaveevaluationhsf_prefix = (ff_ap_mce_alternating_mdr_secondwaveevaluationhsf_prefix) * (ff_bn_mce_alternating_mdr_secondwaveevaluationhsf_prefix) + (ff_an_mce_alternating_mdr_secondwaveevaluationhsf_prefix) * (ff_bp_mce_alternating_mdr_secondwaveevaluationhsf_prefix) /\ ff_n_mce_alternating_mdr_secondwaveevaluationhsf_prefix = (ff_ap_mce_alternating_mdr_secondwaveevaluationhsf_prefix) * (ff_bp_mce_alternating_mdr_secondwaveevaluationhsf_prefix) + (ff_an_mce_alternating_mdr_secondwaveevaluationhsf_prefix) * (ff_bn_mce_alternating_mdr_secondwaveevaluationhsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_secondwaveevaluationhsf_positive ff_v_mce_mdr_secondwaveevaluationhsf_positive. ((((exists ff_h_mce_mdr_secondwaveevaluationhsf_positive_start. ff_h_mce_mdr_secondwaveevaluationhsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_secondwaveevaluationhsf_positive)) /\ exists ff_q_mce_mdr_secondwaveevaluationhsf_positive_start. ff_u_mce_mdr_secondwaveevaluationhsf_positive = ff_q_mce_mdr_secondwaveevaluationhsf_positive_start * S ((S (0)) * ff_v_mce_mdr_secondwaveevaluationhsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_secondwaveevaluationhsf_positive_terminal. ff_h_mce_mdr_secondwaveevaluationhsf_positive_terminal + S (mdr_p_secondwaveevaluationh) = S ((S ((S (mdr_q_secondwaveevaluationhs)))) * ff_v_mce_mdr_secondwaveevaluationhsf_positive)) /\ exists ff_q_mce_mdr_secondwaveevaluationhsf_positive_terminal. ff_u_mce_mdr_secondwaveevaluationhsf_positive = ff_q_mce_mdr_secondwaveevaluationhsf_positive_terminal * S ((S ((S (mdr_q_secondwaveevaluationhs)))) * ff_v_mce_mdr_secondwaveevaluationhsf_positive) + (mdr_p_secondwaveevaluationh))) /\ forall ff_i_mce_mdr_secondwaveevaluationhsf_positive. (exists ff_lt_mce_mdr_secondwaveevaluationhsf_positive_bound. ff_lt_mce_mdr_secondwaveevaluationhsf_positive_bound + S ff_i_mce_mdr_secondwaveevaluationhsf_positive = (S (mdr_q_secondwaveevaluationhs))) -> exists ff_a_mce_mdr_secondwaveevaluationhsf_positive ff_r_mce_mdr_secondwaveevaluationhsf_positive ff_s_mce_mdr_secondwaveevaluationhsf_positive. ((((exists ff_h_mce_mdr_secondwaveevaluationhsf_positive_summand. ff_h_mce_mdr_secondwaveevaluationhsf_positive_summand + S (ff_a_mce_mdr_secondwaveevaluationhsf_positive) = S ((S (ff_i_mce_mdr_secondwaveevaluationhsf_positive)) * ff_uc_mce_fold_mdr_secondwaveevaluationhsf)) /\ exists ff_q_mce_mdr_secondwaveevaluationhsf_positive_summand. ff_ub_mce_fold_mdr_secondwaveevaluationhsf = ff_q_mce_mdr_secondwaveevaluationhsf_positive_summand * S ((S (ff_i_mce_mdr_secondwaveevaluationhsf_positive)) * ff_uc_mce_fold_mdr_secondwaveevaluationhsf) + (ff_a_mce_mdr_secondwaveevaluationhsf_positive))) /\ ((((exists ff_h_mce_mdr_secondwaveevaluationhsf_positive_partial. ff_h_mce_mdr_secondwaveevaluationhsf_positive_partial + S (ff_r_mce_mdr_secondwaveevaluationhsf_positive) = S ((S (ff_i_mce_mdr_secondwaveevaluationhsf_positive)) * ff_v_mce_mdr_secondwaveevaluationhsf_positive)) /\ exists ff_q_mce_mdr_secondwaveevaluationhsf_positive_partial. ff_u_mce_mdr_secondwaveevaluationhsf_positive = ff_q_mce_mdr_secondwaveevaluationhsf_positive_partial * S ((S (ff_i_mce_mdr_secondwaveevaluationhsf_positive)) * ff_v_mce_mdr_secondwaveevaluationhsf_positive) + (ff_r_mce_mdr_secondwaveevaluationhsf_positive))) /\ ((((exists ff_h_mce_mdr_secondwaveevaluationhsf_positive_successor. ff_h_mce_mdr_secondwaveevaluationhsf_positive_successor + S (ff_s_mce_mdr_secondwaveevaluationhsf_positive) = S ((S (S ff_i_mce_mdr_secondwaveevaluationhsf_positive)) * ff_v_mce_mdr_secondwaveevaluationhsf_positive)) /\ exists ff_q_mce_mdr_secondwaveevaluationhsf_positive_successor. ff_u_mce_mdr_secondwaveevaluationhsf_positive = ff_q_mce_mdr_secondwaveevaluationhsf_positive_successor * S ((S (S ff_i_mce_mdr_secondwaveevaluationhsf_positive)) * ff_v_mce_mdr_secondwaveevaluationhsf_positive) + (ff_s_mce_mdr_secondwaveevaluationhsf_positive))) /\ ff_s_mce_mdr_secondwaveevaluationhsf_positive = ff_r_mce_mdr_secondwaveevaluationhsf_positive + ff_a_mce_mdr_secondwaveevaluationhsf_positive)))))) /\ (exists ff_u_mce_mdr_secondwaveevaluationhsf_negative ff_v_mce_mdr_secondwaveevaluationhsf_negative. ((((exists ff_h_mce_mdr_secondwaveevaluationhsf_negative_start. ff_h_mce_mdr_secondwaveevaluationhsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_secondwaveevaluationhsf_negative)) /\ exists ff_q_mce_mdr_secondwaveevaluationhsf_negative_start. ff_u_mce_mdr_secondwaveevaluationhsf_negative = ff_q_mce_mdr_secondwaveevaluationhsf_negative_start * S ((S (0)) * ff_v_mce_mdr_secondwaveevaluationhsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_secondwaveevaluationhsf_negative_terminal. ff_h_mce_mdr_secondwaveevaluationhsf_negative_terminal + S (mdr_n_secondwaveevaluationh) = S ((S ((S (mdr_q_secondwaveevaluationhs)))) * ff_v_mce_mdr_secondwaveevaluationhsf_negative)) /\ exists ff_q_mce_mdr_secondwaveevaluationhsf_negative_terminal. ff_u_mce_mdr_secondwaveevaluationhsf_negative = ff_q_mce_mdr_secondwaveevaluationhsf_negative_terminal * S ((S ((S (mdr_q_secondwaveevaluationhs)))) * ff_v_mce_mdr_secondwaveevaluationhsf_negative) + (mdr_n_secondwaveevaluationh))) /\ forall ff_i_mce_mdr_secondwaveevaluationhsf_negative. (exists ff_lt_mce_mdr_secondwaveevaluationhsf_negative_bound. ff_lt_mce_mdr_secondwaveevaluationhsf_negative_bound + S ff_i_mce_mdr_secondwaveevaluationhsf_negative = (S (mdr_q_secondwaveevaluationhs))) -> exists ff_a_mce_mdr_secondwaveevaluationhsf_negative ff_r_mce_mdr_secondwaveevaluationhsf_negative ff_s_mce_mdr_secondwaveevaluationhsf_negative. ((((exists ff_h_mce_mdr_secondwaveevaluationhsf_negative_summand. ff_h_mce_mdr_secondwaveevaluationhsf_negative_summand + S (ff_a_mce_mdr_secondwaveevaluationhsf_negative) = S ((S (ff_i_mce_mdr_secondwaveevaluationhsf_negative)) * ff_vc_mce_fold_mdr_secondwaveevaluationhsf)) /\ exists ff_q_mce_mdr_secondwaveevaluationhsf_negative_summand. ff_vb_mce_fold_mdr_secondwaveevaluationhsf = ff_q_mce_mdr_secondwaveevaluationhsf_negative_summand * S ((S (ff_i_mce_mdr_secondwaveevaluationhsf_negative)) * ff_vc_mce_fold_mdr_secondwaveevaluationhsf) + (ff_a_mce_mdr_secondwaveevaluationhsf_negative))) /\ ((((exists ff_h_mce_mdr_secondwaveevaluationhsf_negative_partial. ff_h_mce_mdr_secondwaveevaluationhsf_negative_partial + S (ff_r_mce_mdr_secondwaveevaluationhsf_negative) = S ((S (ff_i_mce_mdr_secondwaveevaluationhsf_negative)) * ff_v_mce_mdr_secondwaveevaluationhsf_negative)) /\ exists ff_q_mce_mdr_secondwaveevaluationhsf_negative_partial. ff_u_mce_mdr_secondwaveevaluationhsf_negative = ff_q_mce_mdr_secondwaveevaluationhsf_negative_partial * S ((S (ff_i_mce_mdr_secondwaveevaluationhsf_negative)) * ff_v_mce_mdr_secondwaveevaluationhsf_negative) + (ff_r_mce_mdr_secondwaveevaluationhsf_negative))) /\ ((((exists ff_h_mce_mdr_secondwaveevaluationhsf_negative_successor. ff_h_mce_mdr_secondwaveevaluationhsf_negative_successor + S (ff_s_mce_mdr_secondwaveevaluationhsf_negative) = S ((S (S ff_i_mce_mdr_secondwaveevaluationhsf_negative)) * ff_v_mce_mdr_secondwaveevaluationhsf_negative)) /\ exists ff_q_mce_mdr_secondwaveevaluationhsf_negative_successor. ff_u_mce_mdr_secondwaveevaluationhsf_negative = ff_q_mce_mdr_secondwaveevaluationhsf_negative_successor * S ((S (S ff_i_mce_mdr_secondwaveevaluationhsf_negative)) * ff_v_mce_mdr_secondwaveevaluationhsf_negative) + (ff_s_mce_mdr_secondwaveevaluationhsf_negative))) /\ ff_s_mce_mdr_secondwaveevaluationhsf_negative = ff_r_mce_mdr_secondwaveevaluationhsf_negative + ff_a_mce_mdr_secondwaveevaluationhsf_negative))))))))))))))) /\ ((exists mdr_gap_secondwaveevaluationi. mdr_gap_secondwaveevaluationi + S (mdr_i_secondwaveevaluation) = (mdr_l_secondwaveevaluation)) /\ (exists mdr_z_secondwaveevaluationr. ((exists mdr_a_secondwaveevaluationrc mdr_b_secondwaveevaluationrc mdr_c_secondwaveevaluationrc mdr_e_secondwaveevaluationrc mdr_f_secondwaveevaluationrc. ((mdr_a_secondwaveevaluationrc = ((d) + (ab)) * S ((d) + (ab)) + ((ab) + (ab))) /\ ((mdr_b_secondwaveevaluationrc = ((ac) + (bb)) * S ((ac) + (bb)) + ((bb) + (bb))) /\ ((mdr_c_secondwaveevaluationrc = ((mdr_a_secondwaveevaluationrc) + (mdr_b_secondwaveevaluationrc)) * S ((mdr_a_secondwaveevaluationrc) + (mdr_b_secondwaveevaluationrc)) + ((mdr_b_secondwaveevaluationrc) + (mdr_b_secondwaveevaluationrc))) /\ ((mdr_e_secondwaveevaluationrc = ((mdr_p_secondwave) + (mdr_n_secondwave)) * S ((mdr_p_secondwave) + (mdr_n_secondwave)) + ((mdr_n_secondwave) + (mdr_n_secondwave))) /\ ((mdr_f_secondwaveevaluationrc = ((bc) + (mdr_e_secondwaveevaluationrc)) * S ((bc) + (mdr_e_secondwaveevaluationrc)) + ((mdr_e_secondwaveevaluationrc) + (mdr_e_secondwaveevaluationrc))) /\ ((mdr_z_secondwaveevaluationr) = ((mdr_c_secondwaveevaluationrc) + (mdr_f_secondwaveevaluationrc)) * S ((mdr_c_secondwaveevaluationrc) + (mdr_f_secondwaveevaluationrc)) + ((mdr_f_secondwaveevaluationrc) + (mdr_f_secondwaveevaluationrc))))))))) /\ (((exists ff_h_mdr_secondwaveevaluationrb. ff_h_mdr_secondwaveevaluationrb + S (mdr_z_secondwaveevaluationr) = S ((S (mdr_i_secondwaveevaluation)) * mdr_c_secondwaveevaluation)) /\ exists ff_q_mdr_secondwaveevaluationrb. mdr_b_secondwaveevaluation = ff_q_mdr_secondwaveevaluationrb * S ((S (mdr_i_secondwaveevaluation)) * mdr_c_secondwaveevaluation) + (mdr_z_secondwaveevaluationr)))))))) /\ (((mdr_p_secondwave) = (mdr_n_secondwave) + (D)) \/ ((mdr_n_secondwave) = (mdr_p_secondwave) + (D))))

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