SignedRecursiveDeterminant(pb,pc,nb,nc,d,p,n)

exists mdr_b_secondwave mdr_c_secondwave mdr_l_secondwave mdr_i_secondwave. ((forall mdr_i_secondwaveh. (exists mdr_gap_secondwavehi. mdr_gap_secondwavehi + S (mdr_i_secondwaveh) = (mdr_l_secondwave)) -> exists mdr_d_secondwaveh mdr_pb_secondwaveh mdr_pc_secondwaveh mdr_nb_secondwaveh mdr_nc_secondwaveh mdr_p_secondwaveh mdr_n_secondwaveh. ((exists mdr_z_secondwavehr. ((exists mdr_a_secondwavehrc mdr_b_secondwavehrc mdr_c_secondwavehrc mdr_e_secondwavehrc mdr_f_secondwavehrc. ((mdr_a_secondwavehrc = ((mdr_d_secondwaveh) + (mdr_pb_secondwaveh)) * S ((mdr_d_secondwaveh) + (mdr_pb_secondwaveh)) + ((mdr_pb_secondwaveh) + (mdr_pb_secondwaveh))) /\ ((mdr_b_secondwavehrc = ((mdr_pc_secondwaveh) + (mdr_nb_secondwaveh)) * S ((mdr_pc_secondwaveh) + (mdr_nb_secondwaveh)) + ((mdr_nb_secondwaveh) + (mdr_nb_secondwaveh))) /\ ((mdr_c_secondwavehrc = ((mdr_a_secondwavehrc) + (mdr_b_secondwavehrc)) * S ((mdr_a_secondwavehrc) + (mdr_b_secondwavehrc)) + ((mdr_b_secondwavehrc) + (mdr_b_secondwavehrc))) /\ ((mdr_e_secondwavehrc = ((mdr_p_secondwaveh) + (mdr_n_secondwaveh)) * S ((mdr_p_secondwaveh) + (mdr_n_secondwaveh)) + ((mdr_n_secondwaveh) + (mdr_n_secondwaveh))) /\ ((mdr_f_secondwavehrc = ((mdr_nc_secondwaveh) + (mdr_e_secondwavehrc)) * S ((mdr_nc_secondwaveh) + (mdr_e_secondwavehrc)) + ((mdr_e_secondwavehrc) + (mdr_e_secondwavehrc))) /\ ((mdr_z_secondwavehr) = ((mdr_c_secondwavehrc) + (mdr_f_secondwavehrc)) * S ((mdr_c_secondwavehrc) + (mdr_f_secondwavehrc)) + ((mdr_f_secondwavehrc) + (mdr_f_secondwavehrc))))))))) /\ (((exists ff_h_mdr_secondwavehrb. ff_h_mdr_secondwavehrb + S (mdr_z_secondwavehr) = S ((S (mdr_i_secondwaveh)) * mdr_c_secondwave)) /\ exists ff_q_mdr_secondwavehrb. mdr_b_secondwave = ff_q_mdr_secondwavehrb * S ((S (mdr_i_secondwaveh)) * mdr_c_secondwave) + (mdr_z_secondwavehr))))) /\ (((((mdr_d_secondwaveh) = 0) /\ (((mdr_p_secondwaveh) = 1) /\ ((mdr_n_secondwaveh) = 0))) \/ exists mdr_q_secondwavehs mdr_eb_secondwavehs mdr_ec_secondwavehs mdr_fb_secondwavehs mdr_fc_secondwavehs. (((mdr_d_secondwaveh) = S (mdr_q_secondwavehs)) /\ ((forall mdr_j_secondwavehsc. (exists mdr_gap_secondwavehscj. mdr_gap_secondwavehscj + S (mdr_j_secondwavehsc) = (S (mdr_q_secondwavehs))) -> exists mdr_i_secondwavehsc mdr_up_secondwavehsc mdr_us_secondwavehsc mdr_un_secondwavehsc mdr_ut_secondwavehsc mdr_p_secondwavehsc mdr_n_secondwavehsc. ((exists mdr_gap_secondwavehsci. mdr_gap_secondwavehsci + S (mdr_i_secondwavehsc) = (mdr_i_secondwaveh)) /\ ((exists mdr_z_secondwavehscr. ((exists mdr_a_secondwavehscrc mdr_b_secondwavehscrc mdr_c_secondwavehscrc mdr_e_secondwavehscrc mdr_f_secondwavehscrc. ((mdr_a_secondwavehscrc = ((mdr_q_secondwavehs) + (mdr_up_secondwavehsc)) * S ((mdr_q_secondwavehs) + (mdr_up_secondwavehsc)) + ((mdr_up_secondwavehsc) + (mdr_up_secondwavehsc))) /\ ((mdr_b_secondwavehscrc = ((mdr_us_secondwavehsc) + (mdr_un_secondwavehsc)) * S ((mdr_us_secondwavehsc) + (mdr_un_secondwavehsc)) + ((mdr_un_secondwavehsc) + (mdr_un_secondwavehsc))) /\ ((mdr_c_secondwavehscrc = ((mdr_a_secondwavehscrc) + (mdr_b_secondwavehscrc)) * S ((mdr_a_secondwavehscrc) + (mdr_b_secondwavehscrc)) + ((mdr_b_secondwavehscrc) + (mdr_b_secondwavehscrc))) /\ ((mdr_e_secondwavehscrc = ((mdr_p_secondwavehsc) + (mdr_n_secondwavehsc)) * S ((mdr_p_secondwavehsc) + (mdr_n_secondwavehsc)) + ((mdr_n_secondwavehsc) + (mdr_n_secondwavehsc))) /\ ((mdr_f_secondwavehscrc = ((mdr_ut_secondwavehsc) + (mdr_e_secondwavehscrc)) * S ((mdr_ut_secondwavehsc) + (mdr_e_secondwavehscrc)) + ((mdr_e_secondwavehscrc) + (mdr_e_secondwavehscrc))) /\ ((mdr_z_secondwavehscr) = ((mdr_c_secondwavehscrc) + (mdr_f_secondwavehscrc)) * S ((mdr_c_secondwavehscrc) + (mdr_f_secondwavehscrc)) + ((mdr_f_secondwavehscrc) + (mdr_f_secondwavehscrc))))))))) /\ (((exists ff_h_mdr_secondwavehscrb. ff_h_mdr_secondwavehscrb + S (mdr_z_secondwavehscr) = S ((S (mdr_i_secondwavehsc)) * mdr_c_secondwave)) /\ exists ff_q_mdr_secondwavehscrb. mdr_b_secondwave = ff_q_mdr_secondwavehscrb * S ((S (mdr_i_secondwavehsc)) * mdr_c_secondwave) + (mdr_z_secondwavehscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_secondwavehscm_positive. (exists ff_gap_mdm_lt_mdr_secondwavehscm_positive_index_bound. ff_gap_mdm_lt_mdr_secondwavehscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_secondwavehscm_positive) = ((mdr_q_secondwavehs) * (mdr_q_secondwavehs))) -> exists ff_row_mdm_prefix_mdr_secondwavehscm_positive ff_column_mdm_prefix_mdr_secondwavehscm_positive ff_value_mdm_prefix_mdr_secondwavehscm_positive. (ff_index_mdm_prefix_mdr_secondwavehscm_positive = (mdr_q_secondwavehs) * ff_row_mdm_prefix_mdr_secondwavehscm_positive + ff_column_mdm_prefix_mdr_secondwavehscm_positive /\ ((exists ff_gap_mdm_lt_mdr_secondwavehscm_positive_column_bound. ff_gap_mdm_lt_mdr_secondwavehscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_secondwavehscm_positive) = (mdr_q_secondwavehs)) /\ ((exists ff_row_mdm_cell_mdr_secondwavehscm_positive_cell ff_column_mdm_cell_mdr_secondwavehscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_secondwavehscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_secondwavehscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_secondwavehscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_secondwavehscm_positive_cell = ff_row_mdm_prefix_mdr_secondwavehscm_positive) \/ ((exists ff_gap_mdm_le_mdr_secondwavehscm_positive_cell_row_after. ff_gap_mdm_le_mdr_secondwavehscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_secondwavehscm_positive)) /\ ff_row_mdm_cell_mdr_secondwavehscm_positive_cell = S ff_row_mdm_prefix_mdr_secondwavehscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_secondwavehscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_secondwavehscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_secondwavehscm_positive) = (mdr_j_secondwavehsc)) /\ ff_column_mdm_cell_mdr_secondwavehscm_positive_cell = ff_column_mdm_prefix_mdr_secondwavehscm_positive) \/ ((exists ff_gap_mdm_le_mdr_secondwavehscm_positive_cell_column_after. ff_gap_mdm_le_mdr_secondwavehscm_positive_cell_column_after + (mdr_j_secondwavehsc) = (ff_column_mdm_prefix_mdr_secondwavehscm_positive)) /\ ff_column_mdm_cell_mdr_secondwavehscm_positive_cell = S ff_column_mdm_prefix_mdr_secondwavehscm_positive))) /\ (((exists ff_h_mdm_mdr_secondwavehscm_positive_cell_source. ff_h_mdm_mdr_secondwavehscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_secondwavehscm_positive) = S ((S ((ff_row_mdm_cell_mdr_secondwavehscm_positive_cell) * (S (mdr_q_secondwavehs)) + (ff_column_mdm_cell_mdr_secondwavehscm_positive_cell))) * mdr_pc_secondwaveh)) /\ exists ff_q_mdm_mdr_secondwavehscm_positive_cell_source. mdr_pb_secondwaveh = ff_q_mdm_mdr_secondwavehscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_secondwavehscm_positive_cell) * (S (mdr_q_secondwavehs)) + (ff_column_mdm_cell_mdr_secondwavehscm_positive_cell))) * mdr_pc_secondwaveh) + (ff_value_mdm_prefix_mdr_secondwavehscm_positive)))))) /\ (((exists ff_h_mdm_mdr_secondwavehscm_positive_target. ff_h_mdm_mdr_secondwavehscm_positive_target + S (ff_value_mdm_prefix_mdr_secondwavehscm_positive) = S ((S (ff_index_mdm_prefix_mdr_secondwavehscm_positive)) * mdr_us_secondwavehsc)) /\ exists ff_q_mdm_mdr_secondwavehscm_positive_target. mdr_up_secondwavehsc = ff_q_mdm_mdr_secondwavehscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_secondwavehscm_positive)) * mdr_us_secondwavehsc) + (ff_value_mdm_prefix_mdr_secondwavehscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_secondwavehscm_negative. (exists ff_gap_mdm_lt_mdr_secondwavehscm_negative_index_bound. ff_gap_mdm_lt_mdr_secondwavehscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_secondwavehscm_negative) = ((mdr_q_secondwavehs) * (mdr_q_secondwavehs))) -> exists ff_row_mdm_prefix_mdr_secondwavehscm_negative ff_column_mdm_prefix_mdr_secondwavehscm_negative ff_value_mdm_prefix_mdr_secondwavehscm_negative. (ff_index_mdm_prefix_mdr_secondwavehscm_negative = (mdr_q_secondwavehs) * ff_row_mdm_prefix_mdr_secondwavehscm_negative + ff_column_mdm_prefix_mdr_secondwavehscm_negative /\ ((exists ff_gap_mdm_lt_mdr_secondwavehscm_negative_column_bound. ff_gap_mdm_lt_mdr_secondwavehscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_secondwavehscm_negative) = (mdr_q_secondwavehs)) /\ ((exists ff_row_mdm_cell_mdr_secondwavehscm_negative_cell ff_column_mdm_cell_mdr_secondwavehscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_secondwavehscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_secondwavehscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_secondwavehscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_secondwavehscm_negative_cell = ff_row_mdm_prefix_mdr_secondwavehscm_negative) \/ ((exists ff_gap_mdm_le_mdr_secondwavehscm_negative_cell_row_after. ff_gap_mdm_le_mdr_secondwavehscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_secondwavehscm_negative)) /\ ff_row_mdm_cell_mdr_secondwavehscm_negative_cell = S ff_row_mdm_prefix_mdr_secondwavehscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_secondwavehscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_secondwavehscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_secondwavehscm_negative) = (mdr_j_secondwavehsc)) /\ ff_column_mdm_cell_mdr_secondwavehscm_negative_cell = ff_column_mdm_prefix_mdr_secondwavehscm_negative) \/ ((exists ff_gap_mdm_le_mdr_secondwavehscm_negative_cell_column_after. ff_gap_mdm_le_mdr_secondwavehscm_negative_cell_column_after + (mdr_j_secondwavehsc) = (ff_column_mdm_prefix_mdr_secondwavehscm_negative)) /\ ff_column_mdm_cell_mdr_secondwavehscm_negative_cell = S ff_column_mdm_prefix_mdr_secondwavehscm_negative))) /\ (((exists ff_h_mdm_mdr_secondwavehscm_negative_cell_source. ff_h_mdm_mdr_secondwavehscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_secondwavehscm_negative) = S ((S ((ff_row_mdm_cell_mdr_secondwavehscm_negative_cell) * (S (mdr_q_secondwavehs)) + (ff_column_mdm_cell_mdr_secondwavehscm_negative_cell))) * mdr_nc_secondwaveh)) /\ exists ff_q_mdm_mdr_secondwavehscm_negative_cell_source. mdr_nb_secondwaveh = ff_q_mdm_mdr_secondwavehscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_secondwavehscm_negative_cell) * (S (mdr_q_secondwavehs)) + (ff_column_mdm_cell_mdr_secondwavehscm_negative_cell))) * mdr_nc_secondwaveh) + (ff_value_mdm_prefix_mdr_secondwavehscm_negative)))))) /\ (((exists ff_h_mdm_mdr_secondwavehscm_negative_target. ff_h_mdm_mdr_secondwavehscm_negative_target + S (ff_value_mdm_prefix_mdr_secondwavehscm_negative) = S ((S (ff_index_mdm_prefix_mdr_secondwavehscm_negative)) * mdr_ut_secondwavehsc)) /\ exists ff_q_mdm_mdr_secondwavehscm_negative_target. mdr_un_secondwavehsc = ff_q_mdm_mdr_secondwavehscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_secondwavehscm_negative)) * mdr_ut_secondwavehsc) + (ff_value_mdm_prefix_mdr_secondwavehscm_negative))))))))) /\ ((((exists ff_h_mdr_secondwavehscp. ff_h_mdr_secondwavehscp + S (mdr_p_secondwavehsc) = S ((S (mdr_j_secondwavehsc)) * mdr_ec_secondwavehs)) /\ exists ff_q_mdr_secondwavehscp. mdr_eb_secondwavehs = ff_q_mdr_secondwavehscp * S ((S (mdr_j_secondwavehsc)) * mdr_ec_secondwavehs) + (mdr_p_secondwavehsc))) /\ (((exists ff_h_mdr_secondwavehscn. ff_h_mdr_secondwavehscn + S (mdr_n_secondwavehsc) = S ((S (mdr_j_secondwavehsc)) * mdr_fc_secondwavehs)) /\ exists ff_q_mdr_secondwavehscn. mdr_fb_secondwavehs = ff_q_mdr_secondwavehscn * S ((S (mdr_j_secondwavehsc)) * mdr_fc_secondwavehs) + (mdr_n_secondwavehsc)))))))) /\ (exists ff_ub_mce_fold_mdr_secondwavehsf ff_uc_mce_fold_mdr_secondwavehsf ff_vb_mce_fold_mdr_secondwavehsf ff_vc_mce_fold_mdr_secondwavehsf. ((forall ff_index_mce_alternating_mdr_secondwavehsf_prefix. (exists ff_gap_mce_mdr_secondwavehsf_prefix_index. ff_gap_mce_mdr_secondwavehsf_prefix_index + S (ff_index_mce_alternating_mdr_secondwavehsf_prefix) = (S (mdr_q_secondwavehs))) -> exists ff_ap_mce_alternating_mdr_secondwavehsf_prefix ff_an_mce_alternating_mdr_secondwavehsf_prefix ff_bp_mce_alternating_mdr_secondwavehsf_prefix ff_bn_mce_alternating_mdr_secondwavehsf_prefix ff_p_mce_alternating_mdr_secondwavehsf_prefix ff_n_mce_alternating_mdr_secondwavehsf_prefix. ((((exists ff_h_mce_mdr_secondwavehsf_prefix_ap. ff_h_mce_mdr_secondwavehsf_prefix_ap + S (ff_ap_mce_alternating_mdr_secondwavehsf_prefix) = S ((S (ff_index_mce_alternating_mdr_secondwavehsf_prefix)) * mdr_pc_secondwaveh)) /\ exists ff_q_mce_mdr_secondwavehsf_prefix_ap. mdr_pb_secondwaveh = ff_q_mce_mdr_secondwavehsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_secondwavehsf_prefix)) * mdr_pc_secondwaveh) + (ff_ap_mce_alternating_mdr_secondwavehsf_prefix))) /\ ((((exists ff_h_mce_mdr_secondwavehsf_prefix_an. ff_h_mce_mdr_secondwavehsf_prefix_an + S (ff_an_mce_alternating_mdr_secondwavehsf_prefix) = S ((S (ff_index_mce_alternating_mdr_secondwavehsf_prefix)) * mdr_nc_secondwaveh)) /\ exists ff_q_mce_mdr_secondwavehsf_prefix_an. mdr_nb_secondwaveh = ff_q_mce_mdr_secondwavehsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_secondwavehsf_prefix)) * mdr_nc_secondwaveh) + (ff_an_mce_alternating_mdr_secondwavehsf_prefix))) /\ ((((exists ff_h_mce_mdr_secondwavehsf_prefix_bp. ff_h_mce_mdr_secondwavehsf_prefix_bp + S (ff_bp_mce_alternating_mdr_secondwavehsf_prefix) = S ((S (ff_index_mce_alternating_mdr_secondwavehsf_prefix)) * mdr_ec_secondwavehs)) /\ exists ff_q_mce_mdr_secondwavehsf_prefix_bp. mdr_eb_secondwavehs = ff_q_mce_mdr_secondwavehsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_secondwavehsf_prefix)) * mdr_ec_secondwavehs) + (ff_bp_mce_alternating_mdr_secondwavehsf_prefix))) /\ ((((exists ff_h_mce_mdr_secondwavehsf_prefix_bn. ff_h_mce_mdr_secondwavehsf_prefix_bn + S (ff_bn_mce_alternating_mdr_secondwavehsf_prefix) = S ((S (ff_index_mce_alternating_mdr_secondwavehsf_prefix)) * mdr_fc_secondwavehs)) /\ exists ff_q_mce_mdr_secondwavehsf_prefix_bn. mdr_fb_secondwavehs = ff_q_mce_mdr_secondwavehsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_secondwavehsf_prefix)) * mdr_fc_secondwavehs) + (ff_bn_mce_alternating_mdr_secondwavehsf_prefix))) /\ ((((exists ff_h_mce_mdr_secondwavehsf_prefix_positive. ff_h_mce_mdr_secondwavehsf_prefix_positive + S (ff_p_mce_alternating_mdr_secondwavehsf_prefix) = S ((S (ff_index_mce_alternating_mdr_secondwavehsf_prefix)) * ff_uc_mce_fold_mdr_secondwavehsf)) /\ exists ff_q_mce_mdr_secondwavehsf_prefix_positive. ff_ub_mce_fold_mdr_secondwavehsf = ff_q_mce_mdr_secondwavehsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_secondwavehsf_prefix)) * ff_uc_mce_fold_mdr_secondwavehsf) + (ff_p_mce_alternating_mdr_secondwavehsf_prefix))) /\ ((((exists ff_h_mce_mdr_secondwavehsf_prefix_negative. ff_h_mce_mdr_secondwavehsf_prefix_negative + S (ff_n_mce_alternating_mdr_secondwavehsf_prefix) = S ((S (ff_index_mce_alternating_mdr_secondwavehsf_prefix)) * ff_vc_mce_fold_mdr_secondwavehsf)) /\ exists ff_q_mce_mdr_secondwavehsf_prefix_negative. ff_vb_mce_fold_mdr_secondwavehsf = ff_q_mce_mdr_secondwavehsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_secondwavehsf_prefix)) * ff_vc_mce_fold_mdr_secondwavehsf) + (ff_n_mce_alternating_mdr_secondwavehsf_prefix))) /\ (((exists ff_even_mce_term_mdr_secondwavehsf_prefix_term. ff_index_mce_alternating_mdr_secondwavehsf_prefix = 2 * ff_even_mce_term_mdr_secondwavehsf_prefix_term) /\ (ff_p_mce_alternating_mdr_secondwavehsf_prefix = (ff_ap_mce_alternating_mdr_secondwavehsf_prefix) * (ff_bp_mce_alternating_mdr_secondwavehsf_prefix) + (ff_an_mce_alternating_mdr_secondwavehsf_prefix) * (ff_bn_mce_alternating_mdr_secondwavehsf_prefix) /\ ff_n_mce_alternating_mdr_secondwavehsf_prefix = (ff_ap_mce_alternating_mdr_secondwavehsf_prefix) * (ff_bn_mce_alternating_mdr_secondwavehsf_prefix) + (ff_an_mce_alternating_mdr_secondwavehsf_prefix) * (ff_bp_mce_alternating_mdr_secondwavehsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_secondwavehsf_prefix_term. ff_index_mce_alternating_mdr_secondwavehsf_prefix = 2 * ff_odd_mce_term_mdr_secondwavehsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_secondwavehsf_prefix = (ff_ap_mce_alternating_mdr_secondwavehsf_prefix) * (ff_bn_mce_alternating_mdr_secondwavehsf_prefix) + (ff_an_mce_alternating_mdr_secondwavehsf_prefix) * (ff_bp_mce_alternating_mdr_secondwavehsf_prefix) /\ ff_n_mce_alternating_mdr_secondwavehsf_prefix = (ff_ap_mce_alternating_mdr_secondwavehsf_prefix) * (ff_bp_mce_alternating_mdr_secondwavehsf_prefix) + (ff_an_mce_alternating_mdr_secondwavehsf_prefix) * (ff_bn_mce_alternating_mdr_secondwavehsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_secondwavehsf_positive ff_v_mce_mdr_secondwavehsf_positive. ((((exists ff_h_mce_mdr_secondwavehsf_positive_start. ff_h_mce_mdr_secondwavehsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_secondwavehsf_positive)) /\ exists ff_q_mce_mdr_secondwavehsf_positive_start. ff_u_mce_mdr_secondwavehsf_positive = ff_q_mce_mdr_secondwavehsf_positive_start * S ((S (0)) * ff_v_mce_mdr_secondwavehsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_secondwavehsf_positive_terminal. ff_h_mce_mdr_secondwavehsf_positive_terminal + S (mdr_p_secondwaveh) = S ((S ((S (mdr_q_secondwavehs)))) * ff_v_mce_mdr_secondwavehsf_positive)) /\ exists ff_q_mce_mdr_secondwavehsf_positive_terminal. ff_u_mce_mdr_secondwavehsf_positive = ff_q_mce_mdr_secondwavehsf_positive_terminal * S ((S ((S (mdr_q_secondwavehs)))) * ff_v_mce_mdr_secondwavehsf_positive) + (mdr_p_secondwaveh))) /\ forall ff_i_mce_mdr_secondwavehsf_positive. (exists ff_lt_mce_mdr_secondwavehsf_positive_bound. ff_lt_mce_mdr_secondwavehsf_positive_bound + S ff_i_mce_mdr_secondwavehsf_positive = (S (mdr_q_secondwavehs))) -> exists ff_a_mce_mdr_secondwavehsf_positive ff_r_mce_mdr_secondwavehsf_positive ff_s_mce_mdr_secondwavehsf_positive. ((((exists ff_h_mce_mdr_secondwavehsf_positive_summand. ff_h_mce_mdr_secondwavehsf_positive_summand + S (ff_a_mce_mdr_secondwavehsf_positive) = S ((S (ff_i_mce_mdr_secondwavehsf_positive)) * ff_uc_mce_fold_mdr_secondwavehsf)) /\ exists ff_q_mce_mdr_secondwavehsf_positive_summand. ff_ub_mce_fold_mdr_secondwavehsf = ff_q_mce_mdr_secondwavehsf_positive_summand * S ((S (ff_i_mce_mdr_secondwavehsf_positive)) * ff_uc_mce_fold_mdr_secondwavehsf) + (ff_a_mce_mdr_secondwavehsf_positive))) /\ ((((exists ff_h_mce_mdr_secondwavehsf_positive_partial. ff_h_mce_mdr_secondwavehsf_positive_partial + S (ff_r_mce_mdr_secondwavehsf_positive) = S ((S (ff_i_mce_mdr_secondwavehsf_positive)) * ff_v_mce_mdr_secondwavehsf_positive)) /\ exists ff_q_mce_mdr_secondwavehsf_positive_partial. ff_u_mce_mdr_secondwavehsf_positive = ff_q_mce_mdr_secondwavehsf_positive_partial * S ((S (ff_i_mce_mdr_secondwavehsf_positive)) * ff_v_mce_mdr_secondwavehsf_positive) + (ff_r_mce_mdr_secondwavehsf_positive))) /\ ((((exists ff_h_mce_mdr_secondwavehsf_positive_successor. ff_h_mce_mdr_secondwavehsf_positive_successor + S (ff_s_mce_mdr_secondwavehsf_positive) = S ((S (S ff_i_mce_mdr_secondwavehsf_positive)) * ff_v_mce_mdr_secondwavehsf_positive)) /\ exists ff_q_mce_mdr_secondwavehsf_positive_successor. ff_u_mce_mdr_secondwavehsf_positive = ff_q_mce_mdr_secondwavehsf_positive_successor * S ((S (S ff_i_mce_mdr_secondwavehsf_positive)) * ff_v_mce_mdr_secondwavehsf_positive) + (ff_s_mce_mdr_secondwavehsf_positive))) /\ ff_s_mce_mdr_secondwavehsf_positive = ff_r_mce_mdr_secondwavehsf_positive + ff_a_mce_mdr_secondwavehsf_positive)))))) /\ (exists ff_u_mce_mdr_secondwavehsf_negative ff_v_mce_mdr_secondwavehsf_negative. ((((exists ff_h_mce_mdr_secondwavehsf_negative_start. ff_h_mce_mdr_secondwavehsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_secondwavehsf_negative)) /\ exists ff_q_mce_mdr_secondwavehsf_negative_start. ff_u_mce_mdr_secondwavehsf_negative = ff_q_mce_mdr_secondwavehsf_negative_start * S ((S (0)) * ff_v_mce_mdr_secondwavehsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_secondwavehsf_negative_terminal. ff_h_mce_mdr_secondwavehsf_negative_terminal + S (mdr_n_secondwaveh) = S ((S ((S (mdr_q_secondwavehs)))) * ff_v_mce_mdr_secondwavehsf_negative)) /\ exists ff_q_mce_mdr_secondwavehsf_negative_terminal. ff_u_mce_mdr_secondwavehsf_negative = ff_q_mce_mdr_secondwavehsf_negative_terminal * S ((S ((S (mdr_q_secondwavehs)))) * ff_v_mce_mdr_secondwavehsf_negative) + (mdr_n_secondwaveh))) /\ forall ff_i_mce_mdr_secondwavehsf_negative. (exists ff_lt_mce_mdr_secondwavehsf_negative_bound. ff_lt_mce_mdr_secondwavehsf_negative_bound + S ff_i_mce_mdr_secondwavehsf_negative = (S (mdr_q_secondwavehs))) -> exists ff_a_mce_mdr_secondwavehsf_negative ff_r_mce_mdr_secondwavehsf_negative ff_s_mce_mdr_secondwavehsf_negative. ((((exists ff_h_mce_mdr_secondwavehsf_negative_summand. ff_h_mce_mdr_secondwavehsf_negative_summand + S (ff_a_mce_mdr_secondwavehsf_negative) = S ((S (ff_i_mce_mdr_secondwavehsf_negative)) * ff_vc_mce_fold_mdr_secondwavehsf)) /\ exists ff_q_mce_mdr_secondwavehsf_negative_summand. ff_vb_mce_fold_mdr_secondwavehsf = ff_q_mce_mdr_secondwavehsf_negative_summand * S ((S (ff_i_mce_mdr_secondwavehsf_negative)) * ff_vc_mce_fold_mdr_secondwavehsf) + (ff_a_mce_mdr_secondwavehsf_negative))) /\ ((((exists ff_h_mce_mdr_secondwavehsf_negative_partial. ff_h_mce_mdr_secondwavehsf_negative_partial + S (ff_r_mce_mdr_secondwavehsf_negative) = S ((S (ff_i_mce_mdr_secondwavehsf_negative)) * ff_v_mce_mdr_secondwavehsf_negative)) /\ exists ff_q_mce_mdr_secondwavehsf_negative_partial. ff_u_mce_mdr_secondwavehsf_negative = ff_q_mce_mdr_secondwavehsf_negative_partial * S ((S (ff_i_mce_mdr_secondwavehsf_negative)) * ff_v_mce_mdr_secondwavehsf_negative) + (ff_r_mce_mdr_secondwavehsf_negative))) /\ ((((exists ff_h_mce_mdr_secondwavehsf_negative_successor. ff_h_mce_mdr_secondwavehsf_negative_successor + S (ff_s_mce_mdr_secondwavehsf_negative) = S ((S (S ff_i_mce_mdr_secondwavehsf_negative)) * ff_v_mce_mdr_secondwavehsf_negative)) /\ exists ff_q_mce_mdr_secondwavehsf_negative_successor. ff_u_mce_mdr_secondwavehsf_negative = ff_q_mce_mdr_secondwavehsf_negative_successor * S ((S (S ff_i_mce_mdr_secondwavehsf_negative)) * ff_v_mce_mdr_secondwavehsf_negative) + (ff_s_mce_mdr_secondwavehsf_negative))) /\ ff_s_mce_mdr_secondwavehsf_negative = ff_r_mce_mdr_secondwavehsf_negative + ff_a_mce_mdr_secondwavehsf_negative))))))))))))))) /\ ((exists mdr_gap_secondwavei. mdr_gap_secondwavei + S (mdr_i_secondwave) = (mdr_l_secondwave)) /\ (exists mdr_z_secondwaver. ((exists mdr_a_secondwaverc mdr_b_secondwaverc mdr_c_secondwaverc mdr_e_secondwaverc mdr_f_secondwaverc. ((mdr_a_secondwaverc = ((d) + (pb)) * S ((d) + (pb)) + ((pb) + (pb))) /\ ((mdr_b_secondwaverc = ((pc) + (nb)) * S ((pc) + (nb)) + ((nb) + (nb))) /\ ((mdr_c_secondwaverc = ((mdr_a_secondwaverc) + (mdr_b_secondwaverc)) * S ((mdr_a_secondwaverc) + (mdr_b_secondwaverc)) + ((mdr_b_secondwaverc) + (mdr_b_secondwaverc))) /\ ((mdr_e_secondwaverc = ((p) + (n)) * S ((p) + (n)) + ((n) + (n))) /\ ((mdr_f_secondwaverc = ((nc) + (mdr_e_secondwaverc)) * S ((nc) + (mdr_e_secondwaverc)) + ((mdr_e_secondwaverc) + (mdr_e_secondwaverc))) /\ ((mdr_z_secondwaver) = ((mdr_c_secondwaverc) + (mdr_f_secondwaverc)) * S ((mdr_c_secondwaverc) + (mdr_f_secondwaverc)) + ((mdr_f_secondwaverc) + (mdr_f_secondwaverc))))))))) /\ (((exists ff_h_mdr_secondwaverb. ff_h_mdr_secondwaverb + S (mdr_z_secondwaver) = S ((S (mdr_i_secondwave)) * mdr_c_secondwave)) /\ exists ff_q_mdr_secondwaverb. mdr_b_secondwave = ff_q_mdr_secondwaverb * S ((S (mdr_i_secondwave)) * mdr_c_secondwave) + (mdr_z_secondwaver)))))))

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