SignedEvaluatedCofactors(pb,pc,nb,nc,q,eb,ec,fb,fc)

forall mdr_j_secondwave. (exists mdr_gap_secondwavej. mdr_gap_secondwavej + S (mdr_j_secondwave) = (S (q))) -> exists mdr_up_secondwave mdr_us_secondwave mdr_un_secondwave mdr_ut_secondwave mdr_p_secondwave mdr_n_secondwave. ((((forall ff_index_mdm_prefix_mdr_secondwavem_positive. (exists ff_gap_mdm_lt_mdr_secondwavem_positive_index_bound. ff_gap_mdm_lt_mdr_secondwavem_positive_index_bound + S (ff_index_mdm_prefix_mdr_secondwavem_positive) = ((q) * (q))) -> exists ff_row_mdm_prefix_mdr_secondwavem_positive ff_column_mdm_prefix_mdr_secondwavem_positive ff_value_mdm_prefix_mdr_secondwavem_positive. (ff_index_mdm_prefix_mdr_secondwavem_positive = (q) * ff_row_mdm_prefix_mdr_secondwavem_positive + ff_column_mdm_prefix_mdr_secondwavem_positive /\ ((exists ff_gap_mdm_lt_mdr_secondwavem_positive_column_bound. ff_gap_mdm_lt_mdr_secondwavem_positive_column_bound + S (ff_column_mdm_prefix_mdr_secondwavem_positive) = (q)) /\ ((exists ff_row_mdm_cell_mdr_secondwavem_positive_cell ff_column_mdm_cell_mdr_secondwavem_positive_cell. (((((exists ff_gap_mdm_lt_mdr_secondwavem_positive_cell_row_before. ff_gap_mdm_lt_mdr_secondwavem_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_secondwavem_positive) = (0)) /\ ff_row_mdm_cell_mdr_secondwavem_positive_cell = ff_row_mdm_prefix_mdr_secondwavem_positive) \/ ((exists ff_gap_mdm_le_mdr_secondwavem_positive_cell_row_after. ff_gap_mdm_le_mdr_secondwavem_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_secondwavem_positive)) /\ ff_row_mdm_cell_mdr_secondwavem_positive_cell = S ff_row_mdm_prefix_mdr_secondwavem_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_secondwavem_positive_cell_column_before. ff_gap_mdm_lt_mdr_secondwavem_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_secondwavem_positive) = (mdr_j_secondwave)) /\ ff_column_mdm_cell_mdr_secondwavem_positive_cell = ff_column_mdm_prefix_mdr_secondwavem_positive) \/ ((exists ff_gap_mdm_le_mdr_secondwavem_positive_cell_column_after. ff_gap_mdm_le_mdr_secondwavem_positive_cell_column_after + (mdr_j_secondwave) = (ff_column_mdm_prefix_mdr_secondwavem_positive)) /\ ff_column_mdm_cell_mdr_secondwavem_positive_cell = S ff_column_mdm_prefix_mdr_secondwavem_positive))) /\ (((exists ff_h_mdm_mdr_secondwavem_positive_cell_source. ff_h_mdm_mdr_secondwavem_positive_cell_source + S (ff_value_mdm_prefix_mdr_secondwavem_positive) = S ((S ((ff_row_mdm_cell_mdr_secondwavem_positive_cell) * (S (q)) + (ff_column_mdm_cell_mdr_secondwavem_positive_cell))) * pc)) /\ exists ff_q_mdm_mdr_secondwavem_positive_cell_source. pb = ff_q_mdm_mdr_secondwavem_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_secondwavem_positive_cell) * (S (q)) + (ff_column_mdm_cell_mdr_secondwavem_positive_cell))) * pc) + (ff_value_mdm_prefix_mdr_secondwavem_positive)))))) /\ (((exists ff_h_mdm_mdr_secondwavem_positive_target. ff_h_mdm_mdr_secondwavem_positive_target + S (ff_value_mdm_prefix_mdr_secondwavem_positive) = S ((S (ff_index_mdm_prefix_mdr_secondwavem_positive)) * mdr_us_secondwave)) /\ exists ff_q_mdm_mdr_secondwavem_positive_target. mdr_up_secondwave = ff_q_mdm_mdr_secondwavem_positive_target * S ((S (ff_index_mdm_prefix_mdr_secondwavem_positive)) * mdr_us_secondwave) + (ff_value_mdm_prefix_mdr_secondwavem_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_secondwavem_negative. (exists ff_gap_mdm_lt_mdr_secondwavem_negative_index_bound. ff_gap_mdm_lt_mdr_secondwavem_negative_index_bound + S (ff_index_mdm_prefix_mdr_secondwavem_negative) = ((q) * (q))) -> exists ff_row_mdm_prefix_mdr_secondwavem_negative ff_column_mdm_prefix_mdr_secondwavem_negative ff_value_mdm_prefix_mdr_secondwavem_negative. (ff_index_mdm_prefix_mdr_secondwavem_negative = (q) * ff_row_mdm_prefix_mdr_secondwavem_negative + ff_column_mdm_prefix_mdr_secondwavem_negative /\ ((exists ff_gap_mdm_lt_mdr_secondwavem_negative_column_bound. ff_gap_mdm_lt_mdr_secondwavem_negative_column_bound + S (ff_column_mdm_prefix_mdr_secondwavem_negative) = (q)) /\ ((exists ff_row_mdm_cell_mdr_secondwavem_negative_cell ff_column_mdm_cell_mdr_secondwavem_negative_cell. (((((exists ff_gap_mdm_lt_mdr_secondwavem_negative_cell_row_before. ff_gap_mdm_lt_mdr_secondwavem_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_secondwavem_negative) = (0)) /\ ff_row_mdm_cell_mdr_secondwavem_negative_cell = ff_row_mdm_prefix_mdr_secondwavem_negative) \/ ((exists ff_gap_mdm_le_mdr_secondwavem_negative_cell_row_after. ff_gap_mdm_le_mdr_secondwavem_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_secondwavem_negative)) /\ ff_row_mdm_cell_mdr_secondwavem_negative_cell = S ff_row_mdm_prefix_mdr_secondwavem_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_secondwavem_negative_cell_column_before. ff_gap_mdm_lt_mdr_secondwavem_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_secondwavem_negative) = (mdr_j_secondwave)) /\ ff_column_mdm_cell_mdr_secondwavem_negative_cell = ff_column_mdm_prefix_mdr_secondwavem_negative) \/ ((exists ff_gap_mdm_le_mdr_secondwavem_negative_cell_column_after. ff_gap_mdm_le_mdr_secondwavem_negative_cell_column_after + (mdr_j_secondwave) = (ff_column_mdm_prefix_mdr_secondwavem_negative)) /\ ff_column_mdm_cell_mdr_secondwavem_negative_cell = S ff_column_mdm_prefix_mdr_secondwavem_negative))) /\ (((exists ff_h_mdm_mdr_secondwavem_negative_cell_source. ff_h_mdm_mdr_secondwavem_negative_cell_source + S (ff_value_mdm_prefix_mdr_secondwavem_negative) = S ((S ((ff_row_mdm_cell_mdr_secondwavem_negative_cell) * (S (q)) + (ff_column_mdm_cell_mdr_secondwavem_negative_cell))) * nc)) /\ exists ff_q_mdm_mdr_secondwavem_negative_cell_source. nb = ff_q_mdm_mdr_secondwavem_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_secondwavem_negative_cell) * (S (q)) + (ff_column_mdm_cell_mdr_secondwavem_negative_cell))) * nc) + (ff_value_mdm_prefix_mdr_secondwavem_negative)))))) /\ (((exists ff_h_mdm_mdr_secondwavem_negative_target. ff_h_mdm_mdr_secondwavem_negative_target + S (ff_value_mdm_prefix_mdr_secondwavem_negative) = S ((S (ff_index_mdm_prefix_mdr_secondwavem_negative)) * mdr_ut_secondwave)) /\ exists ff_q_mdm_mdr_secondwavem_negative_target. mdr_un_secondwave = ff_q_mdm_mdr_secondwavem_negative_target * S ((S (ff_index_mdm_prefix_mdr_secondwavem_negative)) * mdr_ut_secondwave) + (ff_value_mdm_prefix_mdr_secondwavem_negative))))))))) /\ ((exists mdr_b_secondwaved mdr_c_secondwaved mdr_l_secondwaved mdr_i_secondwaved. ((forall mdr_i_secondwavedh. (exists mdr_gap_secondwavedhi. mdr_gap_secondwavedhi + S (mdr_i_secondwavedh) = (mdr_l_secondwaved)) -> exists mdr_d_secondwavedh mdr_pb_secondwavedh mdr_pc_secondwavedh mdr_nb_secondwavedh mdr_nc_secondwavedh mdr_p_secondwavedh mdr_n_secondwavedh. ((exists mdr_z_secondwavedhr. ((exists mdr_a_secondwavedhrc mdr_b_secondwavedhrc mdr_c_secondwavedhrc mdr_e_secondwavedhrc mdr_f_secondwavedhrc. ((mdr_a_secondwavedhrc = ((mdr_d_secondwavedh) + (mdr_pb_secondwavedh)) * S ((mdr_d_secondwavedh) + (mdr_pb_secondwavedh)) + ((mdr_pb_secondwavedh) + (mdr_pb_secondwavedh))) /\ ((mdr_b_secondwavedhrc = ((mdr_pc_secondwavedh) + (mdr_nb_secondwavedh)) * S ((mdr_pc_secondwavedh) + (mdr_nb_secondwavedh)) + ((mdr_nb_secondwavedh) + (mdr_nb_secondwavedh))) /\ ((mdr_c_secondwavedhrc = ((mdr_a_secondwavedhrc) + (mdr_b_secondwavedhrc)) * S ((mdr_a_secondwavedhrc) + (mdr_b_secondwavedhrc)) + ((mdr_b_secondwavedhrc) + (mdr_b_secondwavedhrc))) /\ ((mdr_e_secondwavedhrc = ((mdr_p_secondwavedh) + (mdr_n_secondwavedh)) * S ((mdr_p_secondwavedh) + (mdr_n_secondwavedh)) + ((mdr_n_secondwavedh) + (mdr_n_secondwavedh))) /\ ((mdr_f_secondwavedhrc = ((mdr_nc_secondwavedh) + (mdr_e_secondwavedhrc)) * S ((mdr_nc_secondwavedh) + (mdr_e_secondwavedhrc)) + ((mdr_e_secondwavedhrc) + (mdr_e_secondwavedhrc))) /\ ((mdr_z_secondwavedhr) = ((mdr_c_secondwavedhrc) + (mdr_f_secondwavedhrc)) * S ((mdr_c_secondwavedhrc) + (mdr_f_secondwavedhrc)) + ((mdr_f_secondwavedhrc) + (mdr_f_secondwavedhrc))))))))) /\ (((exists ff_h_mdr_secondwavedhrb. ff_h_mdr_secondwavedhrb + S (mdr_z_secondwavedhr) = S ((S (mdr_i_secondwavedh)) * mdr_c_secondwaved)) /\ exists ff_q_mdr_secondwavedhrb. mdr_b_secondwaved = ff_q_mdr_secondwavedhrb * S ((S (mdr_i_secondwavedh)) * mdr_c_secondwaved) + (mdr_z_secondwavedhr))))) /\ (((((mdr_d_secondwavedh) = 0) /\ (((mdr_p_secondwavedh) = 1) /\ ((mdr_n_secondwavedh) = 0))) \/ exists mdr_q_secondwavedhs mdr_eb_secondwavedhs mdr_ec_secondwavedhs mdr_fb_secondwavedhs mdr_fc_secondwavedhs. (((mdr_d_secondwavedh) = S (mdr_q_secondwavedhs)) /\ ((forall mdr_j_secondwavedhsc. (exists mdr_gap_secondwavedhscj. mdr_gap_secondwavedhscj + S (mdr_j_secondwavedhsc) = (S (mdr_q_secondwavedhs))) -> exists mdr_i_secondwavedhsc mdr_up_secondwavedhsc mdr_us_secondwavedhsc mdr_un_secondwavedhsc mdr_ut_secondwavedhsc mdr_p_secondwavedhsc mdr_n_secondwavedhsc. ((exists mdr_gap_secondwavedhsci. mdr_gap_secondwavedhsci + S (mdr_i_secondwavedhsc) = (mdr_i_secondwavedh)) /\ ((exists mdr_z_secondwavedhscr. ((exists mdr_a_secondwavedhscrc mdr_b_secondwavedhscrc mdr_c_secondwavedhscrc mdr_e_secondwavedhscrc mdr_f_secondwavedhscrc. ((mdr_a_secondwavedhscrc = ((mdr_q_secondwavedhs) + (mdr_up_secondwavedhsc)) * S ((mdr_q_secondwavedhs) + (mdr_up_secondwavedhsc)) + ((mdr_up_secondwavedhsc) + (mdr_up_secondwavedhsc))) /\ ((mdr_b_secondwavedhscrc = ((mdr_us_secondwavedhsc) + (mdr_un_secondwavedhsc)) * S ((mdr_us_secondwavedhsc) + (mdr_un_secondwavedhsc)) + ((mdr_un_secondwavedhsc) + (mdr_un_secondwavedhsc))) /\ ((mdr_c_secondwavedhscrc = ((mdr_a_secondwavedhscrc) + (mdr_b_secondwavedhscrc)) * S ((mdr_a_secondwavedhscrc) + (mdr_b_secondwavedhscrc)) + ((mdr_b_secondwavedhscrc) + (mdr_b_secondwavedhscrc))) /\ ((mdr_e_secondwavedhscrc = ((mdr_p_secondwavedhsc) + (mdr_n_secondwavedhsc)) * S ((mdr_p_secondwavedhsc) + (mdr_n_secondwavedhsc)) + ((mdr_n_secondwavedhsc) + (mdr_n_secondwavedhsc))) /\ ((mdr_f_secondwavedhscrc = ((mdr_ut_secondwavedhsc) + (mdr_e_secondwavedhscrc)) * S ((mdr_ut_secondwavedhsc) + (mdr_e_secondwavedhscrc)) + ((mdr_e_secondwavedhscrc) + (mdr_e_secondwavedhscrc))) /\ ((mdr_z_secondwavedhscr) = ((mdr_c_secondwavedhscrc) + (mdr_f_secondwavedhscrc)) * S ((mdr_c_secondwavedhscrc) + (mdr_f_secondwavedhscrc)) + ((mdr_f_secondwavedhscrc) + (mdr_f_secondwavedhscrc))))))))) /\ (((exists ff_h_mdr_secondwavedhscrb. ff_h_mdr_secondwavedhscrb + S (mdr_z_secondwavedhscr) = S ((S (mdr_i_secondwavedhsc)) * mdr_c_secondwaved)) /\ exists ff_q_mdr_secondwavedhscrb. mdr_b_secondwaved = ff_q_mdr_secondwavedhscrb * S ((S (mdr_i_secondwavedhsc)) * mdr_c_secondwaved) + (mdr_z_secondwavedhscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_secondwavedhscm_positive. (exists ff_gap_mdm_lt_mdr_secondwavedhscm_positive_index_bound. ff_gap_mdm_lt_mdr_secondwavedhscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_secondwavedhscm_positive) = ((mdr_q_secondwavedhs) * (mdr_q_secondwavedhs))) -> exists ff_row_mdm_prefix_mdr_secondwavedhscm_positive ff_column_mdm_prefix_mdr_secondwavedhscm_positive ff_value_mdm_prefix_mdr_secondwavedhscm_positive. (ff_index_mdm_prefix_mdr_secondwavedhscm_positive = (mdr_q_secondwavedhs) * ff_row_mdm_prefix_mdr_secondwavedhscm_positive + ff_column_mdm_prefix_mdr_secondwavedhscm_positive /\ ((exists ff_gap_mdm_lt_mdr_secondwavedhscm_positive_column_bound. ff_gap_mdm_lt_mdr_secondwavedhscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_secondwavedhscm_positive) = (mdr_q_secondwavedhs)) /\ ((exists ff_row_mdm_cell_mdr_secondwavedhscm_positive_cell ff_column_mdm_cell_mdr_secondwavedhscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_secondwavedhscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_secondwavedhscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_secondwavedhscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_secondwavedhscm_positive_cell = ff_row_mdm_prefix_mdr_secondwavedhscm_positive) \/ ((exists ff_gap_mdm_le_mdr_secondwavedhscm_positive_cell_row_after. ff_gap_mdm_le_mdr_secondwavedhscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_secondwavedhscm_positive)) /\ ff_row_mdm_cell_mdr_secondwavedhscm_positive_cell = S ff_row_mdm_prefix_mdr_secondwavedhscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_secondwavedhscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_secondwavedhscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_secondwavedhscm_positive) = (mdr_j_secondwavedhsc)) /\ ff_column_mdm_cell_mdr_secondwavedhscm_positive_cell = ff_column_mdm_prefix_mdr_secondwavedhscm_positive) \/ ((exists ff_gap_mdm_le_mdr_secondwavedhscm_positive_cell_column_after. ff_gap_mdm_le_mdr_secondwavedhscm_positive_cell_column_after + (mdr_j_secondwavedhsc) = (ff_column_mdm_prefix_mdr_secondwavedhscm_positive)) /\ ff_column_mdm_cell_mdr_secondwavedhscm_positive_cell = S ff_column_mdm_prefix_mdr_secondwavedhscm_positive))) /\ (((exists ff_h_mdm_mdr_secondwavedhscm_positive_cell_source. ff_h_mdm_mdr_secondwavedhscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_secondwavedhscm_positive) = S ((S ((ff_row_mdm_cell_mdr_secondwavedhscm_positive_cell) * (S (mdr_q_secondwavedhs)) + (ff_column_mdm_cell_mdr_secondwavedhscm_positive_cell))) * mdr_pc_secondwavedh)) /\ exists ff_q_mdm_mdr_secondwavedhscm_positive_cell_source. mdr_pb_secondwavedh = ff_q_mdm_mdr_secondwavedhscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_secondwavedhscm_positive_cell) * (S (mdr_q_secondwavedhs)) + (ff_column_mdm_cell_mdr_secondwavedhscm_positive_cell))) * mdr_pc_secondwavedh) + (ff_value_mdm_prefix_mdr_secondwavedhscm_positive)))))) /\ (((exists ff_h_mdm_mdr_secondwavedhscm_positive_target. ff_h_mdm_mdr_secondwavedhscm_positive_target + S (ff_value_mdm_prefix_mdr_secondwavedhscm_positive) = S ((S (ff_index_mdm_prefix_mdr_secondwavedhscm_positive)) * mdr_us_secondwavedhsc)) /\ exists ff_q_mdm_mdr_secondwavedhscm_positive_target. mdr_up_secondwavedhsc = ff_q_mdm_mdr_secondwavedhscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_secondwavedhscm_positive)) * mdr_us_secondwavedhsc) + (ff_value_mdm_prefix_mdr_secondwavedhscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_secondwavedhscm_negative. (exists ff_gap_mdm_lt_mdr_secondwavedhscm_negative_index_bound. ff_gap_mdm_lt_mdr_secondwavedhscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_secondwavedhscm_negative) = ((mdr_q_secondwavedhs) * (mdr_q_secondwavedhs))) -> exists ff_row_mdm_prefix_mdr_secondwavedhscm_negative ff_column_mdm_prefix_mdr_secondwavedhscm_negative ff_value_mdm_prefix_mdr_secondwavedhscm_negative. (ff_index_mdm_prefix_mdr_secondwavedhscm_negative = (mdr_q_secondwavedhs) * ff_row_mdm_prefix_mdr_secondwavedhscm_negative + ff_column_mdm_prefix_mdr_secondwavedhscm_negative /\ ((exists ff_gap_mdm_lt_mdr_secondwavedhscm_negative_column_bound. ff_gap_mdm_lt_mdr_secondwavedhscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_secondwavedhscm_negative) = (mdr_q_secondwavedhs)) /\ ((exists ff_row_mdm_cell_mdr_secondwavedhscm_negative_cell ff_column_mdm_cell_mdr_secondwavedhscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_secondwavedhscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_secondwavedhscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_secondwavedhscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_secondwavedhscm_negative_cell = ff_row_mdm_prefix_mdr_secondwavedhscm_negative) \/ ((exists ff_gap_mdm_le_mdr_secondwavedhscm_negative_cell_row_after. ff_gap_mdm_le_mdr_secondwavedhscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_secondwavedhscm_negative)) /\ ff_row_mdm_cell_mdr_secondwavedhscm_negative_cell = S ff_row_mdm_prefix_mdr_secondwavedhscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_secondwavedhscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_secondwavedhscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_secondwavedhscm_negative) = (mdr_j_secondwavedhsc)) /\ ff_column_mdm_cell_mdr_secondwavedhscm_negative_cell = ff_column_mdm_prefix_mdr_secondwavedhscm_negative) \/ ((exists ff_gap_mdm_le_mdr_secondwavedhscm_negative_cell_column_after. ff_gap_mdm_le_mdr_secondwavedhscm_negative_cell_column_after + (mdr_j_secondwavedhsc) = (ff_column_mdm_prefix_mdr_secondwavedhscm_negative)) /\ ff_column_mdm_cell_mdr_secondwavedhscm_negative_cell = S ff_column_mdm_prefix_mdr_secondwavedhscm_negative))) /\ (((exists ff_h_mdm_mdr_secondwavedhscm_negative_cell_source. ff_h_mdm_mdr_secondwavedhscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_secondwavedhscm_negative) = S ((S ((ff_row_mdm_cell_mdr_secondwavedhscm_negative_cell) * (S (mdr_q_secondwavedhs)) + (ff_column_mdm_cell_mdr_secondwavedhscm_negative_cell))) * mdr_nc_secondwavedh)) /\ exists ff_q_mdm_mdr_secondwavedhscm_negative_cell_source. mdr_nb_secondwavedh = ff_q_mdm_mdr_secondwavedhscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_secondwavedhscm_negative_cell) * (S (mdr_q_secondwavedhs)) + (ff_column_mdm_cell_mdr_secondwavedhscm_negative_cell))) * mdr_nc_secondwavedh) + (ff_value_mdm_prefix_mdr_secondwavedhscm_negative)))))) /\ (((exists ff_h_mdm_mdr_secondwavedhscm_negative_target. ff_h_mdm_mdr_secondwavedhscm_negative_target + S (ff_value_mdm_prefix_mdr_secondwavedhscm_negative) = S ((S (ff_index_mdm_prefix_mdr_secondwavedhscm_negative)) * mdr_ut_secondwavedhsc)) /\ exists ff_q_mdm_mdr_secondwavedhscm_negative_target. mdr_un_secondwavedhsc = ff_q_mdm_mdr_secondwavedhscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_secondwavedhscm_negative)) * mdr_ut_secondwavedhsc) + (ff_value_mdm_prefix_mdr_secondwavedhscm_negative))))))))) /\ ((((exists ff_h_mdr_secondwavedhscp. ff_h_mdr_secondwavedhscp + S (mdr_p_secondwavedhsc) = S ((S (mdr_j_secondwavedhsc)) * mdr_ec_secondwavedhs)) /\ exists ff_q_mdr_secondwavedhscp. mdr_eb_secondwavedhs = ff_q_mdr_secondwavedhscp * S ((S (mdr_j_secondwavedhsc)) * mdr_ec_secondwavedhs) + (mdr_p_secondwavedhsc))) /\ (((exists ff_h_mdr_secondwavedhscn. ff_h_mdr_secondwavedhscn + S (mdr_n_secondwavedhsc) = S ((S (mdr_j_secondwavedhsc)) * mdr_fc_secondwavedhs)) /\ exists ff_q_mdr_secondwavedhscn. mdr_fb_secondwavedhs = ff_q_mdr_secondwavedhscn * S ((S (mdr_j_secondwavedhsc)) * mdr_fc_secondwavedhs) + (mdr_n_secondwavedhsc)))))))) /\ (exists ff_ub_mce_fold_mdr_secondwavedhsf ff_uc_mce_fold_mdr_secondwavedhsf ff_vb_mce_fold_mdr_secondwavedhsf ff_vc_mce_fold_mdr_secondwavedhsf. ((forall ff_index_mce_alternating_mdr_secondwavedhsf_prefix. (exists ff_gap_mce_mdr_secondwavedhsf_prefix_index. ff_gap_mce_mdr_secondwavedhsf_prefix_index + S (ff_index_mce_alternating_mdr_secondwavedhsf_prefix) = (S (mdr_q_secondwavedhs))) -> exists ff_ap_mce_alternating_mdr_secondwavedhsf_prefix ff_an_mce_alternating_mdr_secondwavedhsf_prefix ff_bp_mce_alternating_mdr_secondwavedhsf_prefix ff_bn_mce_alternating_mdr_secondwavedhsf_prefix ff_p_mce_alternating_mdr_secondwavedhsf_prefix ff_n_mce_alternating_mdr_secondwavedhsf_prefix. ((((exists ff_h_mce_mdr_secondwavedhsf_prefix_ap. ff_h_mce_mdr_secondwavedhsf_prefix_ap + S (ff_ap_mce_alternating_mdr_secondwavedhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_secondwavedhsf_prefix)) * mdr_pc_secondwavedh)) /\ exists ff_q_mce_mdr_secondwavedhsf_prefix_ap. mdr_pb_secondwavedh = ff_q_mce_mdr_secondwavedhsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_secondwavedhsf_prefix)) * mdr_pc_secondwavedh) + (ff_ap_mce_alternating_mdr_secondwavedhsf_prefix))) /\ ((((exists ff_h_mce_mdr_secondwavedhsf_prefix_an. ff_h_mce_mdr_secondwavedhsf_prefix_an + S (ff_an_mce_alternating_mdr_secondwavedhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_secondwavedhsf_prefix)) * mdr_nc_secondwavedh)) /\ exists ff_q_mce_mdr_secondwavedhsf_prefix_an. mdr_nb_secondwavedh = ff_q_mce_mdr_secondwavedhsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_secondwavedhsf_prefix)) * mdr_nc_secondwavedh) + (ff_an_mce_alternating_mdr_secondwavedhsf_prefix))) /\ ((((exists ff_h_mce_mdr_secondwavedhsf_prefix_bp. ff_h_mce_mdr_secondwavedhsf_prefix_bp + S (ff_bp_mce_alternating_mdr_secondwavedhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_secondwavedhsf_prefix)) * mdr_ec_secondwavedhs)) /\ exists ff_q_mce_mdr_secondwavedhsf_prefix_bp. mdr_eb_secondwavedhs = ff_q_mce_mdr_secondwavedhsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_secondwavedhsf_prefix)) * mdr_ec_secondwavedhs) + (ff_bp_mce_alternating_mdr_secondwavedhsf_prefix))) /\ ((((exists ff_h_mce_mdr_secondwavedhsf_prefix_bn. ff_h_mce_mdr_secondwavedhsf_prefix_bn + S (ff_bn_mce_alternating_mdr_secondwavedhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_secondwavedhsf_prefix)) * mdr_fc_secondwavedhs)) /\ exists ff_q_mce_mdr_secondwavedhsf_prefix_bn. mdr_fb_secondwavedhs = ff_q_mce_mdr_secondwavedhsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_secondwavedhsf_prefix)) * mdr_fc_secondwavedhs) + (ff_bn_mce_alternating_mdr_secondwavedhsf_prefix))) /\ ((((exists ff_h_mce_mdr_secondwavedhsf_prefix_positive. ff_h_mce_mdr_secondwavedhsf_prefix_positive + S (ff_p_mce_alternating_mdr_secondwavedhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_secondwavedhsf_prefix)) * ff_uc_mce_fold_mdr_secondwavedhsf)) /\ exists ff_q_mce_mdr_secondwavedhsf_prefix_positive. ff_ub_mce_fold_mdr_secondwavedhsf = ff_q_mce_mdr_secondwavedhsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_secondwavedhsf_prefix)) * ff_uc_mce_fold_mdr_secondwavedhsf) + (ff_p_mce_alternating_mdr_secondwavedhsf_prefix))) /\ ((((exists ff_h_mce_mdr_secondwavedhsf_prefix_negative. ff_h_mce_mdr_secondwavedhsf_prefix_negative + S (ff_n_mce_alternating_mdr_secondwavedhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_secondwavedhsf_prefix)) * ff_vc_mce_fold_mdr_secondwavedhsf)) /\ exists ff_q_mce_mdr_secondwavedhsf_prefix_negative. ff_vb_mce_fold_mdr_secondwavedhsf = ff_q_mce_mdr_secondwavedhsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_secondwavedhsf_prefix)) * ff_vc_mce_fold_mdr_secondwavedhsf) + (ff_n_mce_alternating_mdr_secondwavedhsf_prefix))) /\ (((exists ff_even_mce_term_mdr_secondwavedhsf_prefix_term. ff_index_mce_alternating_mdr_secondwavedhsf_prefix = 2 * ff_even_mce_term_mdr_secondwavedhsf_prefix_term) /\ (ff_p_mce_alternating_mdr_secondwavedhsf_prefix = (ff_ap_mce_alternating_mdr_secondwavedhsf_prefix) * (ff_bp_mce_alternating_mdr_secondwavedhsf_prefix) + (ff_an_mce_alternating_mdr_secondwavedhsf_prefix) * (ff_bn_mce_alternating_mdr_secondwavedhsf_prefix) /\ ff_n_mce_alternating_mdr_secondwavedhsf_prefix = (ff_ap_mce_alternating_mdr_secondwavedhsf_prefix) * (ff_bn_mce_alternating_mdr_secondwavedhsf_prefix) + (ff_an_mce_alternating_mdr_secondwavedhsf_prefix) * (ff_bp_mce_alternating_mdr_secondwavedhsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_secondwavedhsf_prefix_term. ff_index_mce_alternating_mdr_secondwavedhsf_prefix = 2 * ff_odd_mce_term_mdr_secondwavedhsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_secondwavedhsf_prefix = (ff_ap_mce_alternating_mdr_secondwavedhsf_prefix) * (ff_bn_mce_alternating_mdr_secondwavedhsf_prefix) + (ff_an_mce_alternating_mdr_secondwavedhsf_prefix) * (ff_bp_mce_alternating_mdr_secondwavedhsf_prefix) /\ ff_n_mce_alternating_mdr_secondwavedhsf_prefix = (ff_ap_mce_alternating_mdr_secondwavedhsf_prefix) * (ff_bp_mce_alternating_mdr_secondwavedhsf_prefix) + (ff_an_mce_alternating_mdr_secondwavedhsf_prefix) * (ff_bn_mce_alternating_mdr_secondwavedhsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_secondwavedhsf_positive ff_v_mce_mdr_secondwavedhsf_positive. ((((exists ff_h_mce_mdr_secondwavedhsf_positive_start. ff_h_mce_mdr_secondwavedhsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_secondwavedhsf_positive)) /\ exists ff_q_mce_mdr_secondwavedhsf_positive_start. ff_u_mce_mdr_secondwavedhsf_positive = ff_q_mce_mdr_secondwavedhsf_positive_start * S ((S (0)) * ff_v_mce_mdr_secondwavedhsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_secondwavedhsf_positive_terminal. ff_h_mce_mdr_secondwavedhsf_positive_terminal + S (mdr_p_secondwavedh) = S ((S ((S (mdr_q_secondwavedhs)))) * ff_v_mce_mdr_secondwavedhsf_positive)) /\ exists ff_q_mce_mdr_secondwavedhsf_positive_terminal. ff_u_mce_mdr_secondwavedhsf_positive = ff_q_mce_mdr_secondwavedhsf_positive_terminal * S ((S ((S (mdr_q_secondwavedhs)))) * ff_v_mce_mdr_secondwavedhsf_positive) + (mdr_p_secondwavedh))) /\ forall ff_i_mce_mdr_secondwavedhsf_positive. (exists ff_lt_mce_mdr_secondwavedhsf_positive_bound. ff_lt_mce_mdr_secondwavedhsf_positive_bound + S ff_i_mce_mdr_secondwavedhsf_positive = (S (mdr_q_secondwavedhs))) -> exists ff_a_mce_mdr_secondwavedhsf_positive ff_r_mce_mdr_secondwavedhsf_positive ff_s_mce_mdr_secondwavedhsf_positive. ((((exists ff_h_mce_mdr_secondwavedhsf_positive_summand. ff_h_mce_mdr_secondwavedhsf_positive_summand + S (ff_a_mce_mdr_secondwavedhsf_positive) = S ((S (ff_i_mce_mdr_secondwavedhsf_positive)) * ff_uc_mce_fold_mdr_secondwavedhsf)) /\ exists ff_q_mce_mdr_secondwavedhsf_positive_summand. ff_ub_mce_fold_mdr_secondwavedhsf = ff_q_mce_mdr_secondwavedhsf_positive_summand * S ((S (ff_i_mce_mdr_secondwavedhsf_positive)) * ff_uc_mce_fold_mdr_secondwavedhsf) + (ff_a_mce_mdr_secondwavedhsf_positive))) /\ ((((exists ff_h_mce_mdr_secondwavedhsf_positive_partial. ff_h_mce_mdr_secondwavedhsf_positive_partial + S (ff_r_mce_mdr_secondwavedhsf_positive) = S ((S (ff_i_mce_mdr_secondwavedhsf_positive)) * ff_v_mce_mdr_secondwavedhsf_positive)) /\ exists ff_q_mce_mdr_secondwavedhsf_positive_partial. ff_u_mce_mdr_secondwavedhsf_positive = ff_q_mce_mdr_secondwavedhsf_positive_partial * S ((S (ff_i_mce_mdr_secondwavedhsf_positive)) * ff_v_mce_mdr_secondwavedhsf_positive) + (ff_r_mce_mdr_secondwavedhsf_positive))) /\ ((((exists ff_h_mce_mdr_secondwavedhsf_positive_successor. ff_h_mce_mdr_secondwavedhsf_positive_successor + S (ff_s_mce_mdr_secondwavedhsf_positive) = S ((S (S ff_i_mce_mdr_secondwavedhsf_positive)) * ff_v_mce_mdr_secondwavedhsf_positive)) /\ exists ff_q_mce_mdr_secondwavedhsf_positive_successor. ff_u_mce_mdr_secondwavedhsf_positive = ff_q_mce_mdr_secondwavedhsf_positive_successor * S ((S (S ff_i_mce_mdr_secondwavedhsf_positive)) * ff_v_mce_mdr_secondwavedhsf_positive) + (ff_s_mce_mdr_secondwavedhsf_positive))) /\ ff_s_mce_mdr_secondwavedhsf_positive = ff_r_mce_mdr_secondwavedhsf_positive + ff_a_mce_mdr_secondwavedhsf_positive)))))) /\ (exists ff_u_mce_mdr_secondwavedhsf_negative ff_v_mce_mdr_secondwavedhsf_negative. ((((exists ff_h_mce_mdr_secondwavedhsf_negative_start. ff_h_mce_mdr_secondwavedhsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_secondwavedhsf_negative)) /\ exists ff_q_mce_mdr_secondwavedhsf_negative_start. ff_u_mce_mdr_secondwavedhsf_negative = ff_q_mce_mdr_secondwavedhsf_negative_start * S ((S (0)) * ff_v_mce_mdr_secondwavedhsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_secondwavedhsf_negative_terminal. ff_h_mce_mdr_secondwavedhsf_negative_terminal + S (mdr_n_secondwavedh) = S ((S ((S (mdr_q_secondwavedhs)))) * ff_v_mce_mdr_secondwavedhsf_negative)) /\ exists ff_q_mce_mdr_secondwavedhsf_negative_terminal. ff_u_mce_mdr_secondwavedhsf_negative = ff_q_mce_mdr_secondwavedhsf_negative_terminal * S ((S ((S (mdr_q_secondwavedhs)))) * ff_v_mce_mdr_secondwavedhsf_negative) + (mdr_n_secondwavedh))) /\ forall ff_i_mce_mdr_secondwavedhsf_negative. (exists ff_lt_mce_mdr_secondwavedhsf_negative_bound. ff_lt_mce_mdr_secondwavedhsf_negative_bound + S ff_i_mce_mdr_secondwavedhsf_negative = (S (mdr_q_secondwavedhs))) -> exists ff_a_mce_mdr_secondwavedhsf_negative ff_r_mce_mdr_secondwavedhsf_negative ff_s_mce_mdr_secondwavedhsf_negative. ((((exists ff_h_mce_mdr_secondwavedhsf_negative_summand. ff_h_mce_mdr_secondwavedhsf_negative_summand + S (ff_a_mce_mdr_secondwavedhsf_negative) = S ((S (ff_i_mce_mdr_secondwavedhsf_negative)) * ff_vc_mce_fold_mdr_secondwavedhsf)) /\ exists ff_q_mce_mdr_secondwavedhsf_negative_summand. ff_vb_mce_fold_mdr_secondwavedhsf = ff_q_mce_mdr_secondwavedhsf_negative_summand * S ((S (ff_i_mce_mdr_secondwavedhsf_negative)) * ff_vc_mce_fold_mdr_secondwavedhsf) + (ff_a_mce_mdr_secondwavedhsf_negative))) /\ ((((exists ff_h_mce_mdr_secondwavedhsf_negative_partial. ff_h_mce_mdr_secondwavedhsf_negative_partial + S (ff_r_mce_mdr_secondwavedhsf_negative) = S ((S (ff_i_mce_mdr_secondwavedhsf_negative)) * ff_v_mce_mdr_secondwavedhsf_negative)) /\ exists ff_q_mce_mdr_secondwavedhsf_negative_partial. ff_u_mce_mdr_secondwavedhsf_negative = ff_q_mce_mdr_secondwavedhsf_negative_partial * S ((S (ff_i_mce_mdr_secondwavedhsf_negative)) * ff_v_mce_mdr_secondwavedhsf_negative) + (ff_r_mce_mdr_secondwavedhsf_negative))) /\ ((((exists ff_h_mce_mdr_secondwavedhsf_negative_successor. ff_h_mce_mdr_secondwavedhsf_negative_successor + S (ff_s_mce_mdr_secondwavedhsf_negative) = S ((S (S ff_i_mce_mdr_secondwavedhsf_negative)) * ff_v_mce_mdr_secondwavedhsf_negative)) /\ exists ff_q_mce_mdr_secondwavedhsf_negative_successor. ff_u_mce_mdr_secondwavedhsf_negative = ff_q_mce_mdr_secondwavedhsf_negative_successor * S ((S (S ff_i_mce_mdr_secondwavedhsf_negative)) * ff_v_mce_mdr_secondwavedhsf_negative) + (ff_s_mce_mdr_secondwavedhsf_negative))) /\ ff_s_mce_mdr_secondwavedhsf_negative = ff_r_mce_mdr_secondwavedhsf_negative + ff_a_mce_mdr_secondwavedhsf_negative))))))))))))))) /\ ((exists mdr_gap_secondwavedi. mdr_gap_secondwavedi + S (mdr_i_secondwaved) = (mdr_l_secondwaved)) /\ (exists mdr_z_secondwavedr. ((exists mdr_a_secondwavedrc mdr_b_secondwavedrc mdr_c_secondwavedrc mdr_e_secondwavedrc mdr_f_secondwavedrc. ((mdr_a_secondwavedrc = ((q) + (mdr_up_secondwave)) * S ((q) + (mdr_up_secondwave)) + ((mdr_up_secondwave) + (mdr_up_secondwave))) /\ ((mdr_b_secondwavedrc = ((mdr_us_secondwave) + (mdr_un_secondwave)) * S ((mdr_us_secondwave) + (mdr_un_secondwave)) + ((mdr_un_secondwave) + (mdr_un_secondwave))) /\ ((mdr_c_secondwavedrc = ((mdr_a_secondwavedrc) + (mdr_b_secondwavedrc)) * S ((mdr_a_secondwavedrc) + (mdr_b_secondwavedrc)) + ((mdr_b_secondwavedrc) + (mdr_b_secondwavedrc))) /\ ((mdr_e_secondwavedrc = ((mdr_p_secondwave) + (mdr_n_secondwave)) * S ((mdr_p_secondwave) + (mdr_n_secondwave)) + ((mdr_n_secondwave) + (mdr_n_secondwave))) /\ ((mdr_f_secondwavedrc = ((mdr_ut_secondwave) + (mdr_e_secondwavedrc)) * S ((mdr_ut_secondwave) + (mdr_e_secondwavedrc)) + ((mdr_e_secondwavedrc) + (mdr_e_secondwavedrc))) /\ ((mdr_z_secondwavedr) = ((mdr_c_secondwavedrc) + (mdr_f_secondwavedrc)) * S ((mdr_c_secondwavedrc) + (mdr_f_secondwavedrc)) + ((mdr_f_secondwavedrc) + (mdr_f_secondwavedrc))))))))) /\ (((exists ff_h_mdr_secondwavedrb. ff_h_mdr_secondwavedrb + S (mdr_z_secondwavedr) = S ((S (mdr_i_secondwaved)) * mdr_c_secondwaved)) /\ exists ff_q_mdr_secondwavedrb. mdr_b_secondwaved = ff_q_mdr_secondwavedrb * S ((S (mdr_i_secondwaved)) * mdr_c_secondwaved) + (mdr_z_secondwavedr)))))))) /\ ((((exists ff_h_mdr_secondwavep. ff_h_mdr_secondwavep + S (mdr_p_secondwave) = S ((S (mdr_j_secondwave)) * ec)) /\ exists ff_q_mdr_secondwavep. eb = ff_q_mdr_secondwavep * S ((S (mdr_j_secondwave)) * ec) + (mdr_p_secondwave))) /\ (((exists ff_h_mdr_secondwaven. ff_h_mdr_secondwaven + S (mdr_n_secondwave) = S ((S (mdr_j_secondwave)) * fc)) /\ exists ff_q_mdr_secondwaven. fb = ff_q_mdr_secondwaven * S ((S (mdr_j_secondwave)) * fc) + (mdr_n_secondwave))))))

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