SignedDeterminantLocalStep(b,c,i,d,pb,pc,nb,nc,p,n)

((((d) = 0) /\ (((p) = 1) /\ ((n) = 0))) \/ exists mdr_q_secondwave mdr_eb_secondwave mdr_ec_secondwave mdr_fb_secondwave mdr_fc_secondwave. (((d) = S (mdr_q_secondwave)) /\ ((forall mdr_j_secondwavec. (exists mdr_gap_secondwavecj. mdr_gap_secondwavecj + S (mdr_j_secondwavec) = (S (mdr_q_secondwave))) -> exists mdr_i_secondwavec mdr_up_secondwavec mdr_us_secondwavec mdr_un_secondwavec mdr_ut_secondwavec mdr_p_secondwavec mdr_n_secondwavec. ((exists mdr_gap_secondwaveci. mdr_gap_secondwaveci + S (mdr_i_secondwavec) = (i)) /\ ((exists mdr_z_secondwavecr. ((exists mdr_a_secondwavecrc mdr_b_secondwavecrc mdr_c_secondwavecrc mdr_e_secondwavecrc mdr_f_secondwavecrc. ((mdr_a_secondwavecrc = ((mdr_q_secondwave) + (mdr_up_secondwavec)) * S ((mdr_q_secondwave) + (mdr_up_secondwavec)) + ((mdr_up_secondwavec) + (mdr_up_secondwavec))) /\ ((mdr_b_secondwavecrc = ((mdr_us_secondwavec) + (mdr_un_secondwavec)) * S ((mdr_us_secondwavec) + (mdr_un_secondwavec)) + ((mdr_un_secondwavec) + (mdr_un_secondwavec))) /\ ((mdr_c_secondwavecrc = ((mdr_a_secondwavecrc) + (mdr_b_secondwavecrc)) * S ((mdr_a_secondwavecrc) + (mdr_b_secondwavecrc)) + ((mdr_b_secondwavecrc) + (mdr_b_secondwavecrc))) /\ ((mdr_e_secondwavecrc = ((mdr_p_secondwavec) + (mdr_n_secondwavec)) * S ((mdr_p_secondwavec) + (mdr_n_secondwavec)) + ((mdr_n_secondwavec) + (mdr_n_secondwavec))) /\ ((mdr_f_secondwavecrc = ((mdr_ut_secondwavec) + (mdr_e_secondwavecrc)) * S ((mdr_ut_secondwavec) + (mdr_e_secondwavecrc)) + ((mdr_e_secondwavecrc) + (mdr_e_secondwavecrc))) /\ ((mdr_z_secondwavecr) = ((mdr_c_secondwavecrc) + (mdr_f_secondwavecrc)) * S ((mdr_c_secondwavecrc) + (mdr_f_secondwavecrc)) + ((mdr_f_secondwavecrc) + (mdr_f_secondwavecrc))))))))) /\ (((exists ff_h_mdr_secondwavecrb. ff_h_mdr_secondwavecrb + S (mdr_z_secondwavecr) = S ((S (mdr_i_secondwavec)) * c)) /\ exists ff_q_mdr_secondwavecrb. b = ff_q_mdr_secondwavecrb * S ((S (mdr_i_secondwavec)) * c) + (mdr_z_secondwavecr))))) /\ ((((forall ff_index_mdm_prefix_mdr_secondwavecm_positive. (exists ff_gap_mdm_lt_mdr_secondwavecm_positive_index_bound. ff_gap_mdm_lt_mdr_secondwavecm_positive_index_bound + S (ff_index_mdm_prefix_mdr_secondwavecm_positive) = ((mdr_q_secondwave) * (mdr_q_secondwave))) -> exists ff_row_mdm_prefix_mdr_secondwavecm_positive ff_column_mdm_prefix_mdr_secondwavecm_positive ff_value_mdm_prefix_mdr_secondwavecm_positive. (ff_index_mdm_prefix_mdr_secondwavecm_positive = (mdr_q_secondwave) * ff_row_mdm_prefix_mdr_secondwavecm_positive + ff_column_mdm_prefix_mdr_secondwavecm_positive /\ ((exists ff_gap_mdm_lt_mdr_secondwavecm_positive_column_bound. ff_gap_mdm_lt_mdr_secondwavecm_positive_column_bound + S (ff_column_mdm_prefix_mdr_secondwavecm_positive) = (mdr_q_secondwave)) /\ ((exists ff_row_mdm_cell_mdr_secondwavecm_positive_cell ff_column_mdm_cell_mdr_secondwavecm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_secondwavecm_positive_cell_row_before. ff_gap_mdm_lt_mdr_secondwavecm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_secondwavecm_positive) = (0)) /\ ff_row_mdm_cell_mdr_secondwavecm_positive_cell = ff_row_mdm_prefix_mdr_secondwavecm_positive) \/ ((exists ff_gap_mdm_le_mdr_secondwavecm_positive_cell_row_after. ff_gap_mdm_le_mdr_secondwavecm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_secondwavecm_positive)) /\ ff_row_mdm_cell_mdr_secondwavecm_positive_cell = S ff_row_mdm_prefix_mdr_secondwavecm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_secondwavecm_positive_cell_column_before. ff_gap_mdm_lt_mdr_secondwavecm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_secondwavecm_positive) = (mdr_j_secondwavec)) /\ ff_column_mdm_cell_mdr_secondwavecm_positive_cell = ff_column_mdm_prefix_mdr_secondwavecm_positive) \/ ((exists ff_gap_mdm_le_mdr_secondwavecm_positive_cell_column_after. ff_gap_mdm_le_mdr_secondwavecm_positive_cell_column_after + (mdr_j_secondwavec) = (ff_column_mdm_prefix_mdr_secondwavecm_positive)) /\ ff_column_mdm_cell_mdr_secondwavecm_positive_cell = S ff_column_mdm_prefix_mdr_secondwavecm_positive))) /\ (((exists ff_h_mdm_mdr_secondwavecm_positive_cell_source. ff_h_mdm_mdr_secondwavecm_positive_cell_source + S (ff_value_mdm_prefix_mdr_secondwavecm_positive) = S ((S ((ff_row_mdm_cell_mdr_secondwavecm_positive_cell) * (S (mdr_q_secondwave)) + (ff_column_mdm_cell_mdr_secondwavecm_positive_cell))) * pc)) /\ exists ff_q_mdm_mdr_secondwavecm_positive_cell_source. pb = ff_q_mdm_mdr_secondwavecm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_secondwavecm_positive_cell) * (S (mdr_q_secondwave)) + (ff_column_mdm_cell_mdr_secondwavecm_positive_cell))) * pc) + (ff_value_mdm_prefix_mdr_secondwavecm_positive)))))) /\ (((exists ff_h_mdm_mdr_secondwavecm_positive_target. ff_h_mdm_mdr_secondwavecm_positive_target + S (ff_value_mdm_prefix_mdr_secondwavecm_positive) = S ((S (ff_index_mdm_prefix_mdr_secondwavecm_positive)) * mdr_us_secondwavec)) /\ exists ff_q_mdm_mdr_secondwavecm_positive_target. mdr_up_secondwavec = ff_q_mdm_mdr_secondwavecm_positive_target * S ((S (ff_index_mdm_prefix_mdr_secondwavecm_positive)) * mdr_us_secondwavec) + (ff_value_mdm_prefix_mdr_secondwavecm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_secondwavecm_negative. (exists ff_gap_mdm_lt_mdr_secondwavecm_negative_index_bound. ff_gap_mdm_lt_mdr_secondwavecm_negative_index_bound + S (ff_index_mdm_prefix_mdr_secondwavecm_negative) = ((mdr_q_secondwave) * (mdr_q_secondwave))) -> exists ff_row_mdm_prefix_mdr_secondwavecm_negative ff_column_mdm_prefix_mdr_secondwavecm_negative ff_value_mdm_prefix_mdr_secondwavecm_negative. (ff_index_mdm_prefix_mdr_secondwavecm_negative = (mdr_q_secondwave) * ff_row_mdm_prefix_mdr_secondwavecm_negative + ff_column_mdm_prefix_mdr_secondwavecm_negative /\ ((exists ff_gap_mdm_lt_mdr_secondwavecm_negative_column_bound. ff_gap_mdm_lt_mdr_secondwavecm_negative_column_bound + S (ff_column_mdm_prefix_mdr_secondwavecm_negative) = (mdr_q_secondwave)) /\ ((exists ff_row_mdm_cell_mdr_secondwavecm_negative_cell ff_column_mdm_cell_mdr_secondwavecm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_secondwavecm_negative_cell_row_before. ff_gap_mdm_lt_mdr_secondwavecm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_secondwavecm_negative) = (0)) /\ ff_row_mdm_cell_mdr_secondwavecm_negative_cell = ff_row_mdm_prefix_mdr_secondwavecm_negative) \/ ((exists ff_gap_mdm_le_mdr_secondwavecm_negative_cell_row_after. ff_gap_mdm_le_mdr_secondwavecm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_secondwavecm_negative)) /\ ff_row_mdm_cell_mdr_secondwavecm_negative_cell = S ff_row_mdm_prefix_mdr_secondwavecm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_secondwavecm_negative_cell_column_before. ff_gap_mdm_lt_mdr_secondwavecm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_secondwavecm_negative) = (mdr_j_secondwavec)) /\ ff_column_mdm_cell_mdr_secondwavecm_negative_cell = ff_column_mdm_prefix_mdr_secondwavecm_negative) \/ ((exists ff_gap_mdm_le_mdr_secondwavecm_negative_cell_column_after. ff_gap_mdm_le_mdr_secondwavecm_negative_cell_column_after + (mdr_j_secondwavec) = (ff_column_mdm_prefix_mdr_secondwavecm_negative)) /\ ff_column_mdm_cell_mdr_secondwavecm_negative_cell = S ff_column_mdm_prefix_mdr_secondwavecm_negative))) /\ (((exists ff_h_mdm_mdr_secondwavecm_negative_cell_source. ff_h_mdm_mdr_secondwavecm_negative_cell_source + S (ff_value_mdm_prefix_mdr_secondwavecm_negative) = S ((S ((ff_row_mdm_cell_mdr_secondwavecm_negative_cell) * (S (mdr_q_secondwave)) + (ff_column_mdm_cell_mdr_secondwavecm_negative_cell))) * nc)) /\ exists ff_q_mdm_mdr_secondwavecm_negative_cell_source. nb = ff_q_mdm_mdr_secondwavecm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_secondwavecm_negative_cell) * (S (mdr_q_secondwave)) + (ff_column_mdm_cell_mdr_secondwavecm_negative_cell))) * nc) + (ff_value_mdm_prefix_mdr_secondwavecm_negative)))))) /\ (((exists ff_h_mdm_mdr_secondwavecm_negative_target. ff_h_mdm_mdr_secondwavecm_negative_target + S (ff_value_mdm_prefix_mdr_secondwavecm_negative) = S ((S (ff_index_mdm_prefix_mdr_secondwavecm_negative)) * mdr_ut_secondwavec)) /\ exists ff_q_mdm_mdr_secondwavecm_negative_target. mdr_un_secondwavec = ff_q_mdm_mdr_secondwavecm_negative_target * S ((S (ff_index_mdm_prefix_mdr_secondwavecm_negative)) * mdr_ut_secondwavec) + (ff_value_mdm_prefix_mdr_secondwavecm_negative))))))))) /\ ((((exists ff_h_mdr_secondwavecp. ff_h_mdr_secondwavecp + S (mdr_p_secondwavec) = S ((S (mdr_j_secondwavec)) * mdr_ec_secondwave)) /\ exists ff_q_mdr_secondwavecp. mdr_eb_secondwave = ff_q_mdr_secondwavecp * S ((S (mdr_j_secondwavec)) * mdr_ec_secondwave) + (mdr_p_secondwavec))) /\ (((exists ff_h_mdr_secondwavecn. ff_h_mdr_secondwavecn + S (mdr_n_secondwavec) = S ((S (mdr_j_secondwavec)) * mdr_fc_secondwave)) /\ exists ff_q_mdr_secondwavecn. mdr_fb_secondwave = ff_q_mdr_secondwavecn * S ((S (mdr_j_secondwavec)) * mdr_fc_secondwave) + (mdr_n_secondwavec)))))))) /\ (exists ff_ub_mce_fold_mdr_secondwavef ff_uc_mce_fold_mdr_secondwavef ff_vb_mce_fold_mdr_secondwavef ff_vc_mce_fold_mdr_secondwavef. ((forall ff_index_mce_alternating_mdr_secondwavef_prefix. (exists ff_gap_mce_mdr_secondwavef_prefix_index. ff_gap_mce_mdr_secondwavef_prefix_index + S (ff_index_mce_alternating_mdr_secondwavef_prefix) = (S (mdr_q_secondwave))) -> exists ff_ap_mce_alternating_mdr_secondwavef_prefix ff_an_mce_alternating_mdr_secondwavef_prefix ff_bp_mce_alternating_mdr_secondwavef_prefix ff_bn_mce_alternating_mdr_secondwavef_prefix ff_p_mce_alternating_mdr_secondwavef_prefix ff_n_mce_alternating_mdr_secondwavef_prefix. ((((exists ff_h_mce_mdr_secondwavef_prefix_ap. ff_h_mce_mdr_secondwavef_prefix_ap + S (ff_ap_mce_alternating_mdr_secondwavef_prefix) = S ((S (ff_index_mce_alternating_mdr_secondwavef_prefix)) * pc)) /\ exists ff_q_mce_mdr_secondwavef_prefix_ap. pb = ff_q_mce_mdr_secondwavef_prefix_ap * S ((S (ff_index_mce_alternating_mdr_secondwavef_prefix)) * pc) + (ff_ap_mce_alternating_mdr_secondwavef_prefix))) /\ ((((exists ff_h_mce_mdr_secondwavef_prefix_an. ff_h_mce_mdr_secondwavef_prefix_an + S (ff_an_mce_alternating_mdr_secondwavef_prefix) = S ((S (ff_index_mce_alternating_mdr_secondwavef_prefix)) * nc)) /\ exists ff_q_mce_mdr_secondwavef_prefix_an. nb = ff_q_mce_mdr_secondwavef_prefix_an * S ((S (ff_index_mce_alternating_mdr_secondwavef_prefix)) * nc) + (ff_an_mce_alternating_mdr_secondwavef_prefix))) /\ ((((exists ff_h_mce_mdr_secondwavef_prefix_bp. ff_h_mce_mdr_secondwavef_prefix_bp + S (ff_bp_mce_alternating_mdr_secondwavef_prefix) = S ((S (ff_index_mce_alternating_mdr_secondwavef_prefix)) * mdr_ec_secondwave)) /\ exists ff_q_mce_mdr_secondwavef_prefix_bp. mdr_eb_secondwave = ff_q_mce_mdr_secondwavef_prefix_bp * S ((S (ff_index_mce_alternating_mdr_secondwavef_prefix)) * mdr_ec_secondwave) + (ff_bp_mce_alternating_mdr_secondwavef_prefix))) /\ ((((exists ff_h_mce_mdr_secondwavef_prefix_bn. ff_h_mce_mdr_secondwavef_prefix_bn + S (ff_bn_mce_alternating_mdr_secondwavef_prefix) = S ((S (ff_index_mce_alternating_mdr_secondwavef_prefix)) * mdr_fc_secondwave)) /\ exists ff_q_mce_mdr_secondwavef_prefix_bn. mdr_fb_secondwave = ff_q_mce_mdr_secondwavef_prefix_bn * S ((S (ff_index_mce_alternating_mdr_secondwavef_prefix)) * mdr_fc_secondwave) + (ff_bn_mce_alternating_mdr_secondwavef_prefix))) /\ ((((exists ff_h_mce_mdr_secondwavef_prefix_positive. ff_h_mce_mdr_secondwavef_prefix_positive + S (ff_p_mce_alternating_mdr_secondwavef_prefix) = S ((S (ff_index_mce_alternating_mdr_secondwavef_prefix)) * ff_uc_mce_fold_mdr_secondwavef)) /\ exists ff_q_mce_mdr_secondwavef_prefix_positive. ff_ub_mce_fold_mdr_secondwavef = ff_q_mce_mdr_secondwavef_prefix_positive * S ((S (ff_index_mce_alternating_mdr_secondwavef_prefix)) * ff_uc_mce_fold_mdr_secondwavef) + (ff_p_mce_alternating_mdr_secondwavef_prefix))) /\ ((((exists ff_h_mce_mdr_secondwavef_prefix_negative. ff_h_mce_mdr_secondwavef_prefix_negative + S (ff_n_mce_alternating_mdr_secondwavef_prefix) = S ((S (ff_index_mce_alternating_mdr_secondwavef_prefix)) * ff_vc_mce_fold_mdr_secondwavef)) /\ exists ff_q_mce_mdr_secondwavef_prefix_negative. ff_vb_mce_fold_mdr_secondwavef = ff_q_mce_mdr_secondwavef_prefix_negative * S ((S (ff_index_mce_alternating_mdr_secondwavef_prefix)) * ff_vc_mce_fold_mdr_secondwavef) + (ff_n_mce_alternating_mdr_secondwavef_prefix))) /\ (((exists ff_even_mce_term_mdr_secondwavef_prefix_term. ff_index_mce_alternating_mdr_secondwavef_prefix = 2 * ff_even_mce_term_mdr_secondwavef_prefix_term) /\ (ff_p_mce_alternating_mdr_secondwavef_prefix = (ff_ap_mce_alternating_mdr_secondwavef_prefix) * (ff_bp_mce_alternating_mdr_secondwavef_prefix) + (ff_an_mce_alternating_mdr_secondwavef_prefix) * (ff_bn_mce_alternating_mdr_secondwavef_prefix) /\ ff_n_mce_alternating_mdr_secondwavef_prefix = (ff_ap_mce_alternating_mdr_secondwavef_prefix) * (ff_bn_mce_alternating_mdr_secondwavef_prefix) + (ff_an_mce_alternating_mdr_secondwavef_prefix) * (ff_bp_mce_alternating_mdr_secondwavef_prefix))) \/ ((exists ff_odd_mce_term_mdr_secondwavef_prefix_term. ff_index_mce_alternating_mdr_secondwavef_prefix = 2 * ff_odd_mce_term_mdr_secondwavef_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_secondwavef_prefix = (ff_ap_mce_alternating_mdr_secondwavef_prefix) * (ff_bn_mce_alternating_mdr_secondwavef_prefix) + (ff_an_mce_alternating_mdr_secondwavef_prefix) * (ff_bp_mce_alternating_mdr_secondwavef_prefix) /\ ff_n_mce_alternating_mdr_secondwavef_prefix = (ff_ap_mce_alternating_mdr_secondwavef_prefix) * (ff_bp_mce_alternating_mdr_secondwavef_prefix) + (ff_an_mce_alternating_mdr_secondwavef_prefix) * (ff_bn_mce_alternating_mdr_secondwavef_prefix))))))))))) /\ ((exists ff_u_mce_mdr_secondwavef_positive ff_v_mce_mdr_secondwavef_positive. ((((exists ff_h_mce_mdr_secondwavef_positive_start. ff_h_mce_mdr_secondwavef_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_secondwavef_positive)) /\ exists ff_q_mce_mdr_secondwavef_positive_start. ff_u_mce_mdr_secondwavef_positive = ff_q_mce_mdr_secondwavef_positive_start * S ((S (0)) * ff_v_mce_mdr_secondwavef_positive) + (0))) /\ ((((exists ff_h_mce_mdr_secondwavef_positive_terminal. ff_h_mce_mdr_secondwavef_positive_terminal + S (p) = S ((S ((S (mdr_q_secondwave)))) * ff_v_mce_mdr_secondwavef_positive)) /\ exists ff_q_mce_mdr_secondwavef_positive_terminal. ff_u_mce_mdr_secondwavef_positive = ff_q_mce_mdr_secondwavef_positive_terminal * S ((S ((S (mdr_q_secondwave)))) * ff_v_mce_mdr_secondwavef_positive) + (p))) /\ forall ff_i_mce_mdr_secondwavef_positive. (exists ff_lt_mce_mdr_secondwavef_positive_bound. ff_lt_mce_mdr_secondwavef_positive_bound + S ff_i_mce_mdr_secondwavef_positive = (S (mdr_q_secondwave))) -> exists ff_a_mce_mdr_secondwavef_positive ff_r_mce_mdr_secondwavef_positive ff_s_mce_mdr_secondwavef_positive. ((((exists ff_h_mce_mdr_secondwavef_positive_summand. ff_h_mce_mdr_secondwavef_positive_summand + S (ff_a_mce_mdr_secondwavef_positive) = S ((S (ff_i_mce_mdr_secondwavef_positive)) * ff_uc_mce_fold_mdr_secondwavef)) /\ exists ff_q_mce_mdr_secondwavef_positive_summand. ff_ub_mce_fold_mdr_secondwavef = ff_q_mce_mdr_secondwavef_positive_summand * S ((S (ff_i_mce_mdr_secondwavef_positive)) * ff_uc_mce_fold_mdr_secondwavef) + (ff_a_mce_mdr_secondwavef_positive))) /\ ((((exists ff_h_mce_mdr_secondwavef_positive_partial. ff_h_mce_mdr_secondwavef_positive_partial + S (ff_r_mce_mdr_secondwavef_positive) = S ((S (ff_i_mce_mdr_secondwavef_positive)) * ff_v_mce_mdr_secondwavef_positive)) /\ exists ff_q_mce_mdr_secondwavef_positive_partial. ff_u_mce_mdr_secondwavef_positive = ff_q_mce_mdr_secondwavef_positive_partial * S ((S (ff_i_mce_mdr_secondwavef_positive)) * ff_v_mce_mdr_secondwavef_positive) + (ff_r_mce_mdr_secondwavef_positive))) /\ ((((exists ff_h_mce_mdr_secondwavef_positive_successor. ff_h_mce_mdr_secondwavef_positive_successor + S (ff_s_mce_mdr_secondwavef_positive) = S ((S (S ff_i_mce_mdr_secondwavef_positive)) * ff_v_mce_mdr_secondwavef_positive)) /\ exists ff_q_mce_mdr_secondwavef_positive_successor. ff_u_mce_mdr_secondwavef_positive = ff_q_mce_mdr_secondwavef_positive_successor * S ((S (S ff_i_mce_mdr_secondwavef_positive)) * ff_v_mce_mdr_secondwavef_positive) + (ff_s_mce_mdr_secondwavef_positive))) /\ ff_s_mce_mdr_secondwavef_positive = ff_r_mce_mdr_secondwavef_positive + ff_a_mce_mdr_secondwavef_positive)))))) /\ (exists ff_u_mce_mdr_secondwavef_negative ff_v_mce_mdr_secondwavef_negative. ((((exists ff_h_mce_mdr_secondwavef_negative_start. ff_h_mce_mdr_secondwavef_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_secondwavef_negative)) /\ exists ff_q_mce_mdr_secondwavef_negative_start. ff_u_mce_mdr_secondwavef_negative = ff_q_mce_mdr_secondwavef_negative_start * S ((S (0)) * ff_v_mce_mdr_secondwavef_negative) + (0))) /\ ((((exists ff_h_mce_mdr_secondwavef_negative_terminal. ff_h_mce_mdr_secondwavef_negative_terminal + S (n) = S ((S ((S (mdr_q_secondwave)))) * ff_v_mce_mdr_secondwavef_negative)) /\ exists ff_q_mce_mdr_secondwavef_negative_terminal. ff_u_mce_mdr_secondwavef_negative = ff_q_mce_mdr_secondwavef_negative_terminal * S ((S ((S (mdr_q_secondwave)))) * ff_v_mce_mdr_secondwavef_negative) + (n))) /\ forall ff_i_mce_mdr_secondwavef_negative. (exists ff_lt_mce_mdr_secondwavef_negative_bound. ff_lt_mce_mdr_secondwavef_negative_bound + S ff_i_mce_mdr_secondwavef_negative = (S (mdr_q_secondwave))) -> exists ff_a_mce_mdr_secondwavef_negative ff_r_mce_mdr_secondwavef_negative ff_s_mce_mdr_secondwavef_negative. ((((exists ff_h_mce_mdr_secondwavef_negative_summand. ff_h_mce_mdr_secondwavef_negative_summand + S (ff_a_mce_mdr_secondwavef_negative) = S ((S (ff_i_mce_mdr_secondwavef_negative)) * ff_vc_mce_fold_mdr_secondwavef)) /\ exists ff_q_mce_mdr_secondwavef_negative_summand. ff_vb_mce_fold_mdr_secondwavef = ff_q_mce_mdr_secondwavef_negative_summand * S ((S (ff_i_mce_mdr_secondwavef_negative)) * ff_vc_mce_fold_mdr_secondwavef) + (ff_a_mce_mdr_secondwavef_negative))) /\ ((((exists ff_h_mce_mdr_secondwavef_negative_partial. ff_h_mce_mdr_secondwavef_negative_partial + S (ff_r_mce_mdr_secondwavef_negative) = S ((S (ff_i_mce_mdr_secondwavef_negative)) * ff_v_mce_mdr_secondwavef_negative)) /\ exists ff_q_mce_mdr_secondwavef_negative_partial. ff_u_mce_mdr_secondwavef_negative = ff_q_mce_mdr_secondwavef_negative_partial * S ((S (ff_i_mce_mdr_secondwavef_negative)) * ff_v_mce_mdr_secondwavef_negative) + (ff_r_mce_mdr_secondwavef_negative))) /\ ((((exists ff_h_mce_mdr_secondwavef_negative_successor. ff_h_mce_mdr_secondwavef_negative_successor + S (ff_s_mce_mdr_secondwavef_negative) = S ((S (S ff_i_mce_mdr_secondwavef_negative)) * ff_v_mce_mdr_secondwavef_negative)) /\ exists ff_q_mce_mdr_secondwavef_negative_successor. ff_u_mce_mdr_secondwavef_negative = ff_q_mce_mdr_secondwavef_negative_successor * S ((S (S ff_i_mce_mdr_secondwavef_negative)) * ff_v_mce_mdr_secondwavef_negative) + (ff_s_mce_mdr_secondwavef_negative))) /\ ff_s_mce_mdr_secondwavef_negative = ff_r_mce_mdr_secondwavef_negative + ff_a_mce_mdr_secondwavef_negative))))))))))))

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