AllSignedMinorsZero(pb,pc,nb,nc,r,w,q)

forall mdr_rb_secondwave mdr_rc_secondwave mdr_cb_secondwave mdr_cc_secondwave mdr_p_secondwave mdr_n_secondwave. (((forall fom_index_mrf_secondwaverowsbound. (exists fom_gap_mrf_secondwaverowsbound_index_bound. fom_gap_mrf_secondwaverowsbound_index_bound + S (fom_index_mrf_secondwaverowsbound) = q) -> exists fom_value_mrf_secondwaverowsbound. ((((exists fom_beta_height_mrf_secondwaverowsbound_entry. fom_beta_height_mrf_secondwaverowsbound_entry + S (fom_value_mrf_secondwaverowsbound) = S ((S (fom_index_mrf_secondwaverowsbound)) * mdr_rc_secondwave)) /\ exists fom_beta_quotient_mrf_secondwaverowsbound_entry. mdr_rb_secondwave = fom_beta_quotient_mrf_secondwaverowsbound_entry * S ((S (fom_index_mrf_secondwaverowsbound)) * mdr_rc_secondwave) + (fom_value_mrf_secondwaverowsbound))) /\ (exists fom_gap_mrf_secondwaverowsbound_value_bound. fom_gap_mrf_secondwaverowsbound_value_bound + S (fom_value_mrf_secondwaverowsbound) = r))) /\ (forall mdr_i_secondwaverowsdistinct mdr_j_secondwaverowsdistinct mdr_a_secondwaverowsdistinct. (exists mdr_gap_secondwaverowsdistincti. mdr_gap_secondwaverowsdistincti + S (mdr_i_secondwaverowsdistinct) = (q)) -> (exists mdr_gap_secondwaverowsdistinctj. mdr_gap_secondwaverowsdistinctj + S (mdr_j_secondwaverowsdistinct) = (q)) -> (((exists ff_h_mdr_secondwaverowsdistinctfirst. ff_h_mdr_secondwaverowsdistinctfirst + S (mdr_a_secondwaverowsdistinct) = S ((S (mdr_i_secondwaverowsdistinct)) * mdr_rc_secondwave)) /\ exists ff_q_mdr_secondwaverowsdistinctfirst. mdr_rb_secondwave = ff_q_mdr_secondwaverowsdistinctfirst * S ((S (mdr_i_secondwaverowsdistinct)) * mdr_rc_secondwave) + (mdr_a_secondwaverowsdistinct))) -> (((exists ff_h_mdr_secondwaverowsdistinctsecond. ff_h_mdr_secondwaverowsdistinctsecond + S (mdr_a_secondwaverowsdistinct) = S ((S (mdr_j_secondwaverowsdistinct)) * mdr_rc_secondwave)) /\ exists ff_q_mdr_secondwaverowsdistinctsecond. mdr_rb_secondwave = ff_q_mdr_secondwaverowsdistinctsecond * S ((S (mdr_j_secondwaverowsdistinct)) * mdr_rc_secondwave) + (mdr_a_secondwaverowsdistinct))) -> mdr_i_secondwaverowsdistinct = mdr_j_secondwaverowsdistinct))) -> (((forall fom_index_mrf_secondwavecolumnsbound. (exists fom_gap_mrf_secondwavecolumnsbound_index_bound. fom_gap_mrf_secondwavecolumnsbound_index_bound + S (fom_index_mrf_secondwavecolumnsbound) = q) -> exists fom_value_mrf_secondwavecolumnsbound. ((((exists fom_beta_height_mrf_secondwavecolumnsbound_entry. fom_beta_height_mrf_secondwavecolumnsbound_entry + S (fom_value_mrf_secondwavecolumnsbound) = S ((S (fom_index_mrf_secondwavecolumnsbound)) * mdr_cc_secondwave)) /\ exists fom_beta_quotient_mrf_secondwavecolumnsbound_entry. mdr_cb_secondwave = fom_beta_quotient_mrf_secondwavecolumnsbound_entry * S ((S (fom_index_mrf_secondwavecolumnsbound)) * mdr_cc_secondwave) + (fom_value_mrf_secondwavecolumnsbound))) /\ (exists fom_gap_mrf_secondwavecolumnsbound_value_bound. fom_gap_mrf_secondwavecolumnsbound_value_bound + S (fom_value_mrf_secondwavecolumnsbound) = w))) /\ (forall mdr_i_secondwavecolumnsdistinct mdr_j_secondwavecolumnsdistinct mdr_a_secondwavecolumnsdistinct. (exists mdr_gap_secondwavecolumnsdistincti. mdr_gap_secondwavecolumnsdistincti + S (mdr_i_secondwavecolumnsdistinct) = (q)) -> (exists mdr_gap_secondwavecolumnsdistinctj. mdr_gap_secondwavecolumnsdistinctj + S (mdr_j_secondwavecolumnsdistinct) = (q)) -> (((exists ff_h_mdr_secondwavecolumnsdistinctfirst. ff_h_mdr_secondwavecolumnsdistinctfirst + S (mdr_a_secondwavecolumnsdistinct) = S ((S (mdr_i_secondwavecolumnsdistinct)) * mdr_cc_secondwave)) /\ exists ff_q_mdr_secondwavecolumnsdistinctfirst. mdr_cb_secondwave = ff_q_mdr_secondwavecolumnsdistinctfirst * S ((S (mdr_i_secondwavecolumnsdistinct)) * mdr_cc_secondwave) + (mdr_a_secondwavecolumnsdistinct))) -> (((exists ff_h_mdr_secondwavecolumnsdistinctsecond. ff_h_mdr_secondwavecolumnsdistinctsecond + S (mdr_a_secondwavecolumnsdistinct) = S ((S (mdr_j_secondwavecolumnsdistinct)) * mdr_cc_secondwave)) /\ exists ff_q_mdr_secondwavecolumnsdistinctsecond. mdr_cb_secondwave = ff_q_mdr_secondwavecolumnsdistinctsecond * S ((S (mdr_j_secondwavecolumnsdistinct)) * mdr_cc_secondwave) + (mdr_a_secondwavecolumnsdistinct))) -> mdr_i_secondwavecolumnsdistinct = mdr_j_secondwavecolumnsdistinct))) -> (exists mdr_ub_secondwaveevaluation mdr_uc_secondwaveevaluation mdr_vb_secondwaveevaluation mdr_vc_secondwaveevaluation. ((((forall mdr_i_secondwaveevaluationmatrixpositive. (exists mdr_gap_secondwaveevaluationmatrixpositivebound. mdr_gap_secondwaveevaluationmatrixpositivebound + S (mdr_i_secondwaveevaluationmatrixpositive) = ((q) * (q))) -> exists mdr_a_secondwaveevaluationmatrixpositive. (((exists mdr_r_secondwaveevaluationmatrixpositivepoint mdr_s_secondwaveevaluationmatrixpositivepoint mdr_u_secondwaveevaluationmatrixpositivepoint mdr_v_secondwaveevaluationmatrixpositivepoint. ((mdr_i_secondwaveevaluationmatrixpositive = (q) * mdr_r_secondwaveevaluationmatrixpositivepoint + mdr_s_secondwaveevaluationmatrixpositivepoint) /\ ((exists mdr_gap_secondwaveevaluationmatrixpositivepointcolumn. mdr_gap_secondwaveevaluationmatrixpositivepointcolumn + S (mdr_s_secondwaveevaluationmatrixpositivepoint) = (q)) /\ ((((exists ff_h_mdr_secondwaveevaluationmatrixpositivepointrow_index. ff_h_mdr_secondwaveevaluationmatrixpositivepointrow_index + S (mdr_u_secondwaveevaluationmatrixpositivepoint) = S ((S (mdr_r_secondwaveevaluationmatrixpositivepoint)) * mdr_rc_secondwave)) /\ exists ff_q_mdr_secondwaveevaluationmatrixpositivepointrow_index. mdr_rb_secondwave = ff_q_mdr_secondwaveevaluationmatrixpositivepointrow_index * S ((S (mdr_r_secondwaveevaluationmatrixpositivepoint)) * mdr_rc_secondwave) + (mdr_u_secondwaveevaluationmatrixpositivepoint))) /\ ((((exists ff_h_mdr_secondwaveevaluationmatrixpositivepointcolumn_index. ff_h_mdr_secondwaveevaluationmatrixpositivepointcolumn_index + S (mdr_v_secondwaveevaluationmatrixpositivepoint) = S ((S (mdr_s_secondwaveevaluationmatrixpositivepoint)) * mdr_cc_secondwave)) /\ exists ff_q_mdr_secondwaveevaluationmatrixpositivepointcolumn_index. mdr_cb_secondwave = ff_q_mdr_secondwaveevaluationmatrixpositivepointcolumn_index * S ((S (mdr_s_secondwaveevaluationmatrixpositivepoint)) * mdr_cc_secondwave) + (mdr_v_secondwaveevaluationmatrixpositivepoint))) /\ (((exists ff_h_mdr_secondwaveevaluationmatrixpositivepointsource. ff_h_mdr_secondwaveevaluationmatrixpositivepointsource + S (mdr_a_secondwaveevaluationmatrixpositive) = S ((S ((mdr_u_secondwaveevaluationmatrixpositivepoint) * (w) + (mdr_v_secondwaveevaluationmatrixpositivepoint))) * pc)) /\ exists ff_q_mdr_secondwaveevaluationmatrixpositivepointsource. pb = ff_q_mdr_secondwaveevaluationmatrixpositivepointsource * S ((S ((mdr_u_secondwaveevaluationmatrixpositivepoint) * (w) + (mdr_v_secondwaveevaluationmatrixpositivepoint))) * pc) + (mdr_a_secondwaveevaluationmatrixpositive)))))))) /\ (((exists ff_h_mdr_secondwaveevaluationmatrixpositiveoutput. ff_h_mdr_secondwaveevaluationmatrixpositiveoutput + S (mdr_a_secondwaveevaluationmatrixpositive) = S ((S (mdr_i_secondwaveevaluationmatrixpositive)) * mdr_uc_secondwaveevaluation)) /\ exists ff_q_mdr_secondwaveevaluationmatrixpositiveoutput. mdr_ub_secondwaveevaluation = ff_q_mdr_secondwaveevaluationmatrixpositiveoutput * S ((S (mdr_i_secondwaveevaluationmatrixpositive)) * mdr_uc_secondwaveevaluation) + (mdr_a_secondwaveevaluationmatrixpositive)))))) /\ (forall mdr_i_secondwaveevaluationmatrixnegative. (exists mdr_gap_secondwaveevaluationmatrixnegativebound. mdr_gap_secondwaveevaluationmatrixnegativebound + S (mdr_i_secondwaveevaluationmatrixnegative) = ((q) * (q))) -> exists mdr_a_secondwaveevaluationmatrixnegative. (((exists mdr_r_secondwaveevaluationmatrixnegativepoint mdr_s_secondwaveevaluationmatrixnegativepoint mdr_u_secondwaveevaluationmatrixnegativepoint mdr_v_secondwaveevaluationmatrixnegativepoint. ((mdr_i_secondwaveevaluationmatrixnegative = (q) * mdr_r_secondwaveevaluationmatrixnegativepoint + mdr_s_secondwaveevaluationmatrixnegativepoint) /\ ((exists mdr_gap_secondwaveevaluationmatrixnegativepointcolumn. mdr_gap_secondwaveevaluationmatrixnegativepointcolumn + S (mdr_s_secondwaveevaluationmatrixnegativepoint) = (q)) /\ ((((exists ff_h_mdr_secondwaveevaluationmatrixnegativepointrow_index. ff_h_mdr_secondwaveevaluationmatrixnegativepointrow_index + S (mdr_u_secondwaveevaluationmatrixnegativepoint) = S ((S (mdr_r_secondwaveevaluationmatrixnegativepoint)) * mdr_rc_secondwave)) /\ exists ff_q_mdr_secondwaveevaluationmatrixnegativepointrow_index. mdr_rb_secondwave = ff_q_mdr_secondwaveevaluationmatrixnegativepointrow_index * S ((S (mdr_r_secondwaveevaluationmatrixnegativepoint)) * mdr_rc_secondwave) + (mdr_u_secondwaveevaluationmatrixnegativepoint))) /\ ((((exists ff_h_mdr_secondwaveevaluationmatrixnegativepointcolumn_index. ff_h_mdr_secondwaveevaluationmatrixnegativepointcolumn_index + S (mdr_v_secondwaveevaluationmatrixnegativepoint) = S ((S (mdr_s_secondwaveevaluationmatrixnegativepoint)) * mdr_cc_secondwave)) /\ exists ff_q_mdr_secondwaveevaluationmatrixnegativepointcolumn_index. mdr_cb_secondwave = ff_q_mdr_secondwaveevaluationmatrixnegativepointcolumn_index * S ((S (mdr_s_secondwaveevaluationmatrixnegativepoint)) * mdr_cc_secondwave) + (mdr_v_secondwaveevaluationmatrixnegativepoint))) /\ (((exists ff_h_mdr_secondwaveevaluationmatrixnegativepointsource. ff_h_mdr_secondwaveevaluationmatrixnegativepointsource + S (mdr_a_secondwaveevaluationmatrixnegative) = S ((S ((mdr_u_secondwaveevaluationmatrixnegativepoint) * (w) + (mdr_v_secondwaveevaluationmatrixnegativepoint))) * nc)) /\ exists ff_q_mdr_secondwaveevaluationmatrixnegativepointsource. nb = ff_q_mdr_secondwaveevaluationmatrixnegativepointsource * S ((S ((mdr_u_secondwaveevaluationmatrixnegativepoint) * (w) + (mdr_v_secondwaveevaluationmatrixnegativepoint))) * nc) + (mdr_a_secondwaveevaluationmatrixnegative)))))))) /\ (((exists ff_h_mdr_secondwaveevaluationmatrixnegativeoutput. ff_h_mdr_secondwaveevaluationmatrixnegativeoutput + S (mdr_a_secondwaveevaluationmatrixnegative) = S ((S (mdr_i_secondwaveevaluationmatrixnegative)) * mdr_vc_secondwaveevaluation)) /\ exists ff_q_mdr_secondwaveevaluationmatrixnegativeoutput. mdr_vb_secondwaveevaluation = ff_q_mdr_secondwaveevaluationmatrixnegativeoutput * S ((S (mdr_i_secondwaveevaluationmatrixnegative)) * mdr_vc_secondwaveevaluation) + (mdr_a_secondwaveevaluationmatrixnegative)))))))) /\ (exists mdr_b_secondwaveevaluationdeterminant mdr_c_secondwaveevaluationdeterminant mdr_l_secondwaveevaluationdeterminant mdr_i_secondwaveevaluationdeterminant. ((forall mdr_i_secondwaveevaluationdeterminanth. (exists mdr_gap_secondwaveevaluationdeterminanthi. mdr_gap_secondwaveevaluationdeterminanthi + S (mdr_i_secondwaveevaluationdeterminanth) = (mdr_l_secondwaveevaluationdeterminant)) -> exists mdr_d_secondwaveevaluationdeterminanth mdr_pb_secondwaveevaluationdeterminanth mdr_pc_secondwaveevaluationdeterminanth mdr_nb_secondwaveevaluationdeterminanth mdr_nc_secondwaveevaluationdeterminanth mdr_p_secondwaveevaluationdeterminanth mdr_n_secondwaveevaluationdeterminanth. ((exists mdr_z_secondwaveevaluationdeterminanthr. ((exists mdr_a_secondwaveevaluationdeterminanthrc mdr_b_secondwaveevaluationdeterminanthrc mdr_c_secondwaveevaluationdeterminanthrc mdr_e_secondwaveevaluationdeterminanthrc mdr_f_secondwaveevaluationdeterminanthrc. ((mdr_a_secondwaveevaluationdeterminanthrc = ((mdr_d_secondwaveevaluationdeterminanth) + (mdr_pb_secondwaveevaluationdeterminanth)) * S ((mdr_d_secondwaveevaluationdeterminanth) + (mdr_pb_secondwaveevaluationdeterminanth)) + ((mdr_pb_secondwaveevaluationdeterminanth) + (mdr_pb_secondwaveevaluationdeterminanth))) /\ ((mdr_b_secondwaveevaluationdeterminanthrc = ((mdr_pc_secondwaveevaluationdeterminanth) + (mdr_nb_secondwaveevaluationdeterminanth)) * S ((mdr_pc_secondwaveevaluationdeterminanth) + (mdr_nb_secondwaveevaluationdeterminanth)) + ((mdr_nb_secondwaveevaluationdeterminanth) + (mdr_nb_secondwaveevaluationdeterminanth))) /\ ((mdr_c_secondwaveevaluationdeterminanthrc = ((mdr_a_secondwaveevaluationdeterminanthrc) + (mdr_b_secondwaveevaluationdeterminanthrc)) * S ((mdr_a_secondwaveevaluationdeterminanthrc) + (mdr_b_secondwaveevaluationdeterminanthrc)) + ((mdr_b_secondwaveevaluationdeterminanthrc) + (mdr_b_secondwaveevaluationdeterminanthrc))) /\ ((mdr_e_secondwaveevaluationdeterminanthrc = ((mdr_p_secondwaveevaluationdeterminanth) + (mdr_n_secondwaveevaluationdeterminanth)) * S ((mdr_p_secondwaveevaluationdeterminanth) + (mdr_n_secondwaveevaluationdeterminanth)) + ((mdr_n_secondwaveevaluationdeterminanth) + (mdr_n_secondwaveevaluationdeterminanth))) /\ ((mdr_f_secondwaveevaluationdeterminanthrc = ((mdr_nc_secondwaveevaluationdeterminanth) + (mdr_e_secondwaveevaluationdeterminanthrc)) * S ((mdr_nc_secondwaveevaluationdeterminanth) + (mdr_e_secondwaveevaluationdeterminanthrc)) + ((mdr_e_secondwaveevaluationdeterminanthrc) + (mdr_e_secondwaveevaluationdeterminanthrc))) /\ ((mdr_z_secondwaveevaluationdeterminanthr) = ((mdr_c_secondwaveevaluationdeterminanthrc) + (mdr_f_secondwaveevaluationdeterminanthrc)) * S ((mdr_c_secondwaveevaluationdeterminanthrc) + (mdr_f_secondwaveevaluationdeterminanthrc)) + ((mdr_f_secondwaveevaluationdeterminanthrc) + (mdr_f_secondwaveevaluationdeterminanthrc))))))))) /\ (((exists ff_h_mdr_secondwaveevaluationdeterminanthrb. ff_h_mdr_secondwaveevaluationdeterminanthrb + S (mdr_z_secondwaveevaluationdeterminanthr) = S ((S (mdr_i_secondwaveevaluationdeterminanth)) * mdr_c_secondwaveevaluationdeterminant)) /\ exists ff_q_mdr_secondwaveevaluationdeterminanthrb. mdr_b_secondwaveevaluationdeterminant = ff_q_mdr_secondwaveevaluationdeterminanthrb * S ((S (mdr_i_secondwaveevaluationdeterminanth)) * mdr_c_secondwaveevaluationdeterminant) + (mdr_z_secondwaveevaluationdeterminanthr))))) /\ (((((mdr_d_secondwaveevaluationdeterminanth) = 0) /\ (((mdr_p_secondwaveevaluationdeterminanth) = 1) /\ ((mdr_n_secondwaveevaluationdeterminanth) = 0))) \/ exists mdr_q_secondwaveevaluationdeterminanths mdr_eb_secondwaveevaluationdeterminanths mdr_ec_secondwaveevaluationdeterminanths mdr_fb_secondwaveevaluationdeterminanths mdr_fc_secondwaveevaluationdeterminanths. (((mdr_d_secondwaveevaluationdeterminanth) = S (mdr_q_secondwaveevaluationdeterminanths)) /\ ((forall mdr_j_secondwaveevaluationdeterminanthsc. (exists mdr_gap_secondwaveevaluationdeterminanthscj. mdr_gap_secondwaveevaluationdeterminanthscj + S (mdr_j_secondwaveevaluationdeterminanthsc) = (S (mdr_q_secondwaveevaluationdeterminanths))) -> exists mdr_i_secondwaveevaluationdeterminanthsc mdr_up_secondwaveevaluationdeterminanthsc mdr_us_secondwaveevaluationdeterminanthsc mdr_un_secondwaveevaluationdeterminanthsc mdr_ut_secondwaveevaluationdeterminanthsc mdr_p_secondwaveevaluationdeterminanthsc mdr_n_secondwaveevaluationdeterminanthsc. ((exists mdr_gap_secondwaveevaluationdeterminanthsci. mdr_gap_secondwaveevaluationdeterminanthsci + S (mdr_i_secondwaveevaluationdeterminanthsc) = (mdr_i_secondwaveevaluationdeterminanth)) /\ ((exists mdr_z_secondwaveevaluationdeterminanthscr. ((exists mdr_a_secondwaveevaluationdeterminanthscrc mdr_b_secondwaveevaluationdeterminanthscrc mdr_c_secondwaveevaluationdeterminanthscrc mdr_e_secondwaveevaluationdeterminanthscrc mdr_f_secondwaveevaluationdeterminanthscrc. ((mdr_a_secondwaveevaluationdeterminanthscrc = ((mdr_q_secondwaveevaluationdeterminanths) + (mdr_up_secondwaveevaluationdeterminanthsc)) * S ((mdr_q_secondwaveevaluationdeterminanths) + (mdr_up_secondwaveevaluationdeterminanthsc)) + ((mdr_up_secondwaveevaluationdeterminanthsc) + (mdr_up_secondwaveevaluationdeterminanthsc))) /\ ((mdr_b_secondwaveevaluationdeterminanthscrc = ((mdr_us_secondwaveevaluationdeterminanthsc) + (mdr_un_secondwaveevaluationdeterminanthsc)) * S ((mdr_us_secondwaveevaluationdeterminanthsc) + (mdr_un_secondwaveevaluationdeterminanthsc)) + ((mdr_un_secondwaveevaluationdeterminanthsc) + (mdr_un_secondwaveevaluationdeterminanthsc))) /\ ((mdr_c_secondwaveevaluationdeterminanthscrc = ((mdr_a_secondwaveevaluationdeterminanthscrc) + (mdr_b_secondwaveevaluationdeterminanthscrc)) * S ((mdr_a_secondwaveevaluationdeterminanthscrc) + (mdr_b_secondwaveevaluationdeterminanthscrc)) + ((mdr_b_secondwaveevaluationdeterminanthscrc) + (mdr_b_secondwaveevaluationdeterminanthscrc))) /\ ((mdr_e_secondwaveevaluationdeterminanthscrc = ((mdr_p_secondwaveevaluationdeterminanthsc) + (mdr_n_secondwaveevaluationdeterminanthsc)) * S ((mdr_p_secondwaveevaluationdeterminanthsc) + (mdr_n_secondwaveevaluationdeterminanthsc)) + ((mdr_n_secondwaveevaluationdeterminanthsc) + (mdr_n_secondwaveevaluationdeterminanthsc))) /\ ((mdr_f_secondwaveevaluationdeterminanthscrc = ((mdr_ut_secondwaveevaluationdeterminanthsc) + (mdr_e_secondwaveevaluationdeterminanthscrc)) * S ((mdr_ut_secondwaveevaluationdeterminanthsc) + (mdr_e_secondwaveevaluationdeterminanthscrc)) + ((mdr_e_secondwaveevaluationdeterminanthscrc) + (mdr_e_secondwaveevaluationdeterminanthscrc))) /\ ((mdr_z_secondwaveevaluationdeterminanthscr) = ((mdr_c_secondwaveevaluationdeterminanthscrc) + (mdr_f_secondwaveevaluationdeterminanthscrc)) * S ((mdr_c_secondwaveevaluationdeterminanthscrc) + (mdr_f_secondwaveevaluationdeterminanthscrc)) + ((mdr_f_secondwaveevaluationdeterminanthscrc) + (mdr_f_secondwaveevaluationdeterminanthscrc))))))))) /\ (((exists ff_h_mdr_secondwaveevaluationdeterminanthscrb. ff_h_mdr_secondwaveevaluationdeterminanthscrb + S (mdr_z_secondwaveevaluationdeterminanthscr) = S ((S (mdr_i_secondwaveevaluationdeterminanthsc)) * mdr_c_secondwaveevaluationdeterminant)) /\ exists ff_q_mdr_secondwaveevaluationdeterminanthscrb. mdr_b_secondwaveevaluationdeterminant = ff_q_mdr_secondwaveevaluationdeterminanthscrb * S ((S (mdr_i_secondwaveevaluationdeterminanthsc)) * mdr_c_secondwaveevaluationdeterminant) + (mdr_z_secondwaveevaluationdeterminanthscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_secondwaveevaluationdeterminanthscm_positive. (exists ff_gap_mdm_lt_mdr_secondwaveevaluationdeterminanthscm_positive_index_bound. ff_gap_mdm_lt_mdr_secondwaveevaluationdeterminanthscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_secondwaveevaluationdeterminanthscm_positive) = ((mdr_q_secondwaveevaluationdeterminanths) * (mdr_q_secondwaveevaluationdeterminanths))) -> exists ff_row_mdm_prefix_mdr_secondwaveevaluationdeterminanthscm_positive ff_column_mdm_prefix_mdr_secondwaveevaluationdeterminanthscm_positive ff_value_mdm_prefix_mdr_secondwaveevaluationdeterminanthscm_positive. (ff_index_mdm_prefix_mdr_secondwaveevaluationdeterminanthscm_positive = (mdr_q_secondwaveevaluationdeterminanths) * ff_row_mdm_prefix_mdr_secondwaveevaluationdeterminanthscm_positive + ff_column_mdm_prefix_mdr_secondwaveevaluationdeterminanthscm_positive /\ ((exists ff_gap_mdm_lt_mdr_secondwaveevaluationdeterminanthscm_positive_column_bound. ff_gap_mdm_lt_mdr_secondwaveevaluationdeterminanthscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_secondwaveevaluationdeterminanthscm_positive) = (mdr_q_secondwaveevaluationdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_secondwaveevaluationdeterminanthscm_positive_cell ff_column_mdm_cell_mdr_secondwaveevaluationdeterminanthscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_secondwaveevaluationdeterminanthscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_secondwaveevaluationdeterminanthscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_secondwaveevaluationdeterminanthscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_secondwaveevaluationdeterminanthscm_positive_cell = ff_row_mdm_prefix_mdr_secondwaveevaluationdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_secondwaveevaluationdeterminanthscm_positive_cell_row_after. ff_gap_mdm_le_mdr_secondwaveevaluationdeterminanthscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_secondwaveevaluationdeterminanthscm_positive)) /\ ff_row_mdm_cell_mdr_secondwaveevaluationdeterminanthscm_positive_cell = S ff_row_mdm_prefix_mdr_secondwaveevaluationdeterminanthscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_secondwaveevaluationdeterminanthscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_secondwaveevaluationdeterminanthscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_secondwaveevaluationdeterminanthscm_positive) = (mdr_j_secondwaveevaluationdeterminanthsc)) /\ ff_column_mdm_cell_mdr_secondwaveevaluationdeterminanthscm_positive_cell = ff_column_mdm_prefix_mdr_secondwaveevaluationdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_secondwaveevaluationdeterminanthscm_positive_cell_column_after. ff_gap_mdm_le_mdr_secondwaveevaluationdeterminanthscm_positive_cell_column_after + (mdr_j_secondwaveevaluationdeterminanthsc) = (ff_column_mdm_prefix_mdr_secondwaveevaluationdeterminanthscm_positive)) /\ ff_column_mdm_cell_mdr_secondwaveevaluationdeterminanthscm_positive_cell = S ff_column_mdm_prefix_mdr_secondwaveevaluationdeterminanthscm_positive))) /\ (((exists ff_h_mdm_mdr_secondwaveevaluationdeterminanthscm_positive_cell_source. ff_h_mdm_mdr_secondwaveevaluationdeterminanthscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_secondwaveevaluationdeterminanthscm_positive) = S ((S ((ff_row_mdm_cell_mdr_secondwaveevaluationdeterminanthscm_positive_cell) * (S (mdr_q_secondwaveevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_secondwaveevaluationdeterminanthscm_positive_cell))) * mdr_pc_secondwaveevaluationdeterminanth)) /\ exists ff_q_mdm_mdr_secondwaveevaluationdeterminanthscm_positive_cell_source. mdr_pb_secondwaveevaluationdeterminanth = ff_q_mdm_mdr_secondwaveevaluationdeterminanthscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_secondwaveevaluationdeterminanthscm_positive_cell) * (S (mdr_q_secondwaveevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_secondwaveevaluationdeterminanthscm_positive_cell))) * mdr_pc_secondwaveevaluationdeterminanth) + (ff_value_mdm_prefix_mdr_secondwaveevaluationdeterminanthscm_positive)))))) /\ (((exists ff_h_mdm_mdr_secondwaveevaluationdeterminanthscm_positive_target. ff_h_mdm_mdr_secondwaveevaluationdeterminanthscm_positive_target + S (ff_value_mdm_prefix_mdr_secondwaveevaluationdeterminanthscm_positive) = S ((S (ff_index_mdm_prefix_mdr_secondwaveevaluationdeterminanthscm_positive)) * mdr_us_secondwaveevaluationdeterminanthsc)) /\ exists ff_q_mdm_mdr_secondwaveevaluationdeterminanthscm_positive_target. mdr_up_secondwaveevaluationdeterminanthsc = ff_q_mdm_mdr_secondwaveevaluationdeterminanthscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_secondwaveevaluationdeterminanthscm_positive)) * mdr_us_secondwaveevaluationdeterminanthsc) + (ff_value_mdm_prefix_mdr_secondwaveevaluationdeterminanthscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_secondwaveevaluationdeterminanthscm_negative. (exists ff_gap_mdm_lt_mdr_secondwaveevaluationdeterminanthscm_negative_index_bound. ff_gap_mdm_lt_mdr_secondwaveevaluationdeterminanthscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_secondwaveevaluationdeterminanthscm_negative) = ((mdr_q_secondwaveevaluationdeterminanths) * (mdr_q_secondwaveevaluationdeterminanths))) -> exists ff_row_mdm_prefix_mdr_secondwaveevaluationdeterminanthscm_negative ff_column_mdm_prefix_mdr_secondwaveevaluationdeterminanthscm_negative ff_value_mdm_prefix_mdr_secondwaveevaluationdeterminanthscm_negative. (ff_index_mdm_prefix_mdr_secondwaveevaluationdeterminanthscm_negative = (mdr_q_secondwaveevaluationdeterminanths) * ff_row_mdm_prefix_mdr_secondwaveevaluationdeterminanthscm_negative + ff_column_mdm_prefix_mdr_secondwaveevaluationdeterminanthscm_negative /\ ((exists ff_gap_mdm_lt_mdr_secondwaveevaluationdeterminanthscm_negative_column_bound. ff_gap_mdm_lt_mdr_secondwaveevaluationdeterminanthscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_secondwaveevaluationdeterminanthscm_negative) = (mdr_q_secondwaveevaluationdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_secondwaveevaluationdeterminanthscm_negative_cell ff_column_mdm_cell_mdr_secondwaveevaluationdeterminanthscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_secondwaveevaluationdeterminanthscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_secondwaveevaluationdeterminanthscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_secondwaveevaluationdeterminanthscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_secondwaveevaluationdeterminanthscm_negative_cell = ff_row_mdm_prefix_mdr_secondwaveevaluationdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_secondwaveevaluationdeterminanthscm_negative_cell_row_after. ff_gap_mdm_le_mdr_secondwaveevaluationdeterminanthscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_secondwaveevaluationdeterminanthscm_negative)) /\ ff_row_mdm_cell_mdr_secondwaveevaluationdeterminanthscm_negative_cell = S ff_row_mdm_prefix_mdr_secondwaveevaluationdeterminanthscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_secondwaveevaluationdeterminanthscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_secondwaveevaluationdeterminanthscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_secondwaveevaluationdeterminanthscm_negative) = (mdr_j_secondwaveevaluationdeterminanthsc)) /\ ff_column_mdm_cell_mdr_secondwaveevaluationdeterminanthscm_negative_cell = ff_column_mdm_prefix_mdr_secondwaveevaluationdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_secondwaveevaluationdeterminanthscm_negative_cell_column_after. ff_gap_mdm_le_mdr_secondwaveevaluationdeterminanthscm_negative_cell_column_after + (mdr_j_secondwaveevaluationdeterminanthsc) = (ff_column_mdm_prefix_mdr_secondwaveevaluationdeterminanthscm_negative)) /\ ff_column_mdm_cell_mdr_secondwaveevaluationdeterminanthscm_negative_cell = S ff_column_mdm_prefix_mdr_secondwaveevaluationdeterminanthscm_negative))) /\ (((exists ff_h_mdm_mdr_secondwaveevaluationdeterminanthscm_negative_cell_source. ff_h_mdm_mdr_secondwaveevaluationdeterminanthscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_secondwaveevaluationdeterminanthscm_negative) = S ((S ((ff_row_mdm_cell_mdr_secondwaveevaluationdeterminanthscm_negative_cell) * (S (mdr_q_secondwaveevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_secondwaveevaluationdeterminanthscm_negative_cell))) * mdr_nc_secondwaveevaluationdeterminanth)) /\ exists ff_q_mdm_mdr_secondwaveevaluationdeterminanthscm_negative_cell_source. mdr_nb_secondwaveevaluationdeterminanth = ff_q_mdm_mdr_secondwaveevaluationdeterminanthscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_secondwaveevaluationdeterminanthscm_negative_cell) * (S (mdr_q_secondwaveevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_secondwaveevaluationdeterminanthscm_negative_cell))) * mdr_nc_secondwaveevaluationdeterminanth) + (ff_value_mdm_prefix_mdr_secondwaveevaluationdeterminanthscm_negative)))))) /\ (((exists ff_h_mdm_mdr_secondwaveevaluationdeterminanthscm_negative_target. ff_h_mdm_mdr_secondwaveevaluationdeterminanthscm_negative_target + S (ff_value_mdm_prefix_mdr_secondwaveevaluationdeterminanthscm_negative) = S ((S (ff_index_mdm_prefix_mdr_secondwaveevaluationdeterminanthscm_negative)) * mdr_ut_secondwaveevaluationdeterminanthsc)) /\ exists ff_q_mdm_mdr_secondwaveevaluationdeterminanthscm_negative_target. mdr_un_secondwaveevaluationdeterminanthsc = ff_q_mdm_mdr_secondwaveevaluationdeterminanthscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_secondwaveevaluationdeterminanthscm_negative)) * mdr_ut_secondwaveevaluationdeterminanthsc) + (ff_value_mdm_prefix_mdr_secondwaveevaluationdeterminanthscm_negative))))))))) /\ ((((exists ff_h_mdr_secondwaveevaluationdeterminanthscp. ff_h_mdr_secondwaveevaluationdeterminanthscp + S (mdr_p_secondwaveevaluationdeterminanthsc) = S ((S (mdr_j_secondwaveevaluationdeterminanthsc)) * mdr_ec_secondwaveevaluationdeterminanths)) /\ exists ff_q_mdr_secondwaveevaluationdeterminanthscp. mdr_eb_secondwaveevaluationdeterminanths = ff_q_mdr_secondwaveevaluationdeterminanthscp * S ((S (mdr_j_secondwaveevaluationdeterminanthsc)) * mdr_ec_secondwaveevaluationdeterminanths) + (mdr_p_secondwaveevaluationdeterminanthsc))) /\ (((exists ff_h_mdr_secondwaveevaluationdeterminanthscn. ff_h_mdr_secondwaveevaluationdeterminanthscn + S (mdr_n_secondwaveevaluationdeterminanthsc) = S ((S (mdr_j_secondwaveevaluationdeterminanthsc)) * mdr_fc_secondwaveevaluationdeterminanths)) /\ exists ff_q_mdr_secondwaveevaluationdeterminanthscn. mdr_fb_secondwaveevaluationdeterminanths = ff_q_mdr_secondwaveevaluationdeterminanthscn * S ((S (mdr_j_secondwaveevaluationdeterminanthsc)) * mdr_fc_secondwaveevaluationdeterminanths) + (mdr_n_secondwaveevaluationdeterminanthsc)))))))) /\ (exists ff_ub_mce_fold_mdr_secondwaveevaluationdeterminanthsf ff_uc_mce_fold_mdr_secondwaveevaluationdeterminanthsf ff_vb_mce_fold_mdr_secondwaveevaluationdeterminanthsf ff_vc_mce_fold_mdr_secondwaveevaluationdeterminanthsf. ((forall ff_index_mce_alternating_mdr_secondwaveevaluationdeterminanthsf_prefix. (exists ff_gap_mce_mdr_secondwaveevaluationdeterminanthsf_prefix_index. ff_gap_mce_mdr_secondwaveevaluationdeterminanthsf_prefix_index + S (ff_index_mce_alternating_mdr_secondwaveevaluationdeterminanthsf_prefix) = (S (mdr_q_secondwaveevaluationdeterminanths))) -> exists ff_ap_mce_alternating_mdr_secondwaveevaluationdeterminanthsf_prefix ff_an_mce_alternating_mdr_secondwaveevaluationdeterminanthsf_prefix ff_bp_mce_alternating_mdr_secondwaveevaluationdeterminanthsf_prefix ff_bn_mce_alternating_mdr_secondwaveevaluationdeterminanthsf_prefix ff_p_mce_alternating_mdr_secondwaveevaluationdeterminanthsf_prefix ff_n_mce_alternating_mdr_secondwaveevaluationdeterminanthsf_prefix. ((((exists ff_h_mce_mdr_secondwaveevaluationdeterminanthsf_prefix_ap. ff_h_mce_mdr_secondwaveevaluationdeterminanthsf_prefix_ap + S (ff_ap_mce_alternating_mdr_secondwaveevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_secondwaveevaluationdeterminanthsf_prefix)) * mdr_pc_secondwaveevaluationdeterminanth)) /\ exists ff_q_mce_mdr_secondwaveevaluationdeterminanthsf_prefix_ap. mdr_pb_secondwaveevaluationdeterminanth = ff_q_mce_mdr_secondwaveevaluationdeterminanthsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_secondwaveevaluationdeterminanthsf_prefix)) * mdr_pc_secondwaveevaluationdeterminanth) + (ff_ap_mce_alternating_mdr_secondwaveevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_secondwaveevaluationdeterminanthsf_prefix_an. ff_h_mce_mdr_secondwaveevaluationdeterminanthsf_prefix_an + S (ff_an_mce_alternating_mdr_secondwaveevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_secondwaveevaluationdeterminanthsf_prefix)) * mdr_nc_secondwaveevaluationdeterminanth)) /\ exists ff_q_mce_mdr_secondwaveevaluationdeterminanthsf_prefix_an. mdr_nb_secondwaveevaluationdeterminanth = ff_q_mce_mdr_secondwaveevaluationdeterminanthsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_secondwaveevaluationdeterminanthsf_prefix)) * mdr_nc_secondwaveevaluationdeterminanth) + (ff_an_mce_alternating_mdr_secondwaveevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_secondwaveevaluationdeterminanthsf_prefix_bp. ff_h_mce_mdr_secondwaveevaluationdeterminanthsf_prefix_bp + S (ff_bp_mce_alternating_mdr_secondwaveevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_secondwaveevaluationdeterminanthsf_prefix)) * mdr_ec_secondwaveevaluationdeterminanths)) /\ exists ff_q_mce_mdr_secondwaveevaluationdeterminanthsf_prefix_bp. mdr_eb_secondwaveevaluationdeterminanths = ff_q_mce_mdr_secondwaveevaluationdeterminanthsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_secondwaveevaluationdeterminanthsf_prefix)) * mdr_ec_secondwaveevaluationdeterminanths) + (ff_bp_mce_alternating_mdr_secondwaveevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_secondwaveevaluationdeterminanthsf_prefix_bn. ff_h_mce_mdr_secondwaveevaluationdeterminanthsf_prefix_bn + S (ff_bn_mce_alternating_mdr_secondwaveevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_secondwaveevaluationdeterminanthsf_prefix)) * mdr_fc_secondwaveevaluationdeterminanths)) /\ exists ff_q_mce_mdr_secondwaveevaluationdeterminanthsf_prefix_bn. mdr_fb_secondwaveevaluationdeterminanths = ff_q_mce_mdr_secondwaveevaluationdeterminanthsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_secondwaveevaluationdeterminanthsf_prefix)) * mdr_fc_secondwaveevaluationdeterminanths) + (ff_bn_mce_alternating_mdr_secondwaveevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_secondwaveevaluationdeterminanthsf_prefix_positive. ff_h_mce_mdr_secondwaveevaluationdeterminanthsf_prefix_positive + S (ff_p_mce_alternating_mdr_secondwaveevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_secondwaveevaluationdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_secondwaveevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_secondwaveevaluationdeterminanthsf_prefix_positive. ff_ub_mce_fold_mdr_secondwaveevaluationdeterminanthsf = ff_q_mce_mdr_secondwaveevaluationdeterminanthsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_secondwaveevaluationdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_secondwaveevaluationdeterminanthsf) + (ff_p_mce_alternating_mdr_secondwaveevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_secondwaveevaluationdeterminanthsf_prefix_negative. ff_h_mce_mdr_secondwaveevaluationdeterminanthsf_prefix_negative + S (ff_n_mce_alternating_mdr_secondwaveevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_secondwaveevaluationdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_secondwaveevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_secondwaveevaluationdeterminanthsf_prefix_negative. ff_vb_mce_fold_mdr_secondwaveevaluationdeterminanthsf = ff_q_mce_mdr_secondwaveevaluationdeterminanthsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_secondwaveevaluationdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_secondwaveevaluationdeterminanthsf) + (ff_n_mce_alternating_mdr_secondwaveevaluationdeterminanthsf_prefix))) /\ (((exists ff_even_mce_term_mdr_secondwaveevaluationdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_secondwaveevaluationdeterminanthsf_prefix = 2 * ff_even_mce_term_mdr_secondwaveevaluationdeterminanthsf_prefix_term) /\ (ff_p_mce_alternating_mdr_secondwaveevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_secondwaveevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_secondwaveevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_secondwaveevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_secondwaveevaluationdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_secondwaveevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_secondwaveevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_secondwaveevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_secondwaveevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_secondwaveevaluationdeterminanthsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_secondwaveevaluationdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_secondwaveevaluationdeterminanthsf_prefix = 2 * ff_odd_mce_term_mdr_secondwaveevaluationdeterminanthsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_secondwaveevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_secondwaveevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_secondwaveevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_secondwaveevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_secondwaveevaluationdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_secondwaveevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_secondwaveevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_secondwaveevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_secondwaveevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_secondwaveevaluationdeterminanthsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_secondwaveevaluationdeterminanthsf_positive ff_v_mce_mdr_secondwaveevaluationdeterminanthsf_positive. ((((exists ff_h_mce_mdr_secondwaveevaluationdeterminanthsf_positive_start. ff_h_mce_mdr_secondwaveevaluationdeterminanthsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_secondwaveevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_secondwaveevaluationdeterminanthsf_positive_start. ff_u_mce_mdr_secondwaveevaluationdeterminanthsf_positive = ff_q_mce_mdr_secondwaveevaluationdeterminanthsf_positive_start * S ((S (0)) * ff_v_mce_mdr_secondwaveevaluationdeterminanthsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_secondwaveevaluationdeterminanthsf_positive_terminal. ff_h_mce_mdr_secondwaveevaluationdeterminanthsf_positive_terminal + S (mdr_p_secondwaveevaluationdeterminanth) = S ((S ((S (mdr_q_secondwaveevaluationdeterminanths)))) * ff_v_mce_mdr_secondwaveevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_secondwaveevaluationdeterminanthsf_positive_terminal. ff_u_mce_mdr_secondwaveevaluationdeterminanthsf_positive = ff_q_mce_mdr_secondwaveevaluationdeterminanthsf_positive_terminal * S ((S ((S (mdr_q_secondwaveevaluationdeterminanths)))) * ff_v_mce_mdr_secondwaveevaluationdeterminanthsf_positive) + (mdr_p_secondwaveevaluationdeterminanth))) /\ forall ff_i_mce_mdr_secondwaveevaluationdeterminanthsf_positive. (exists ff_lt_mce_mdr_secondwaveevaluationdeterminanthsf_positive_bound. ff_lt_mce_mdr_secondwaveevaluationdeterminanthsf_positive_bound + S ff_i_mce_mdr_secondwaveevaluationdeterminanthsf_positive = (S (mdr_q_secondwaveevaluationdeterminanths))) -> exists ff_a_mce_mdr_secondwaveevaluationdeterminanthsf_positive ff_r_mce_mdr_secondwaveevaluationdeterminanthsf_positive ff_s_mce_mdr_secondwaveevaluationdeterminanthsf_positive. ((((exists ff_h_mce_mdr_secondwaveevaluationdeterminanthsf_positive_summand. ff_h_mce_mdr_secondwaveevaluationdeterminanthsf_positive_summand + S (ff_a_mce_mdr_secondwaveevaluationdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_secondwaveevaluationdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_secondwaveevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_secondwaveevaluationdeterminanthsf_positive_summand. ff_ub_mce_fold_mdr_secondwaveevaluationdeterminanthsf = ff_q_mce_mdr_secondwaveevaluationdeterminanthsf_positive_summand * S ((S (ff_i_mce_mdr_secondwaveevaluationdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_secondwaveevaluationdeterminanthsf) + (ff_a_mce_mdr_secondwaveevaluationdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_secondwaveevaluationdeterminanthsf_positive_partial. ff_h_mce_mdr_secondwaveevaluationdeterminanthsf_positive_partial + S (ff_r_mce_mdr_secondwaveevaluationdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_secondwaveevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_secondwaveevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_secondwaveevaluationdeterminanthsf_positive_partial. ff_u_mce_mdr_secondwaveevaluationdeterminanthsf_positive = ff_q_mce_mdr_secondwaveevaluationdeterminanthsf_positive_partial * S ((S (ff_i_mce_mdr_secondwaveevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_secondwaveevaluationdeterminanthsf_positive) + (ff_r_mce_mdr_secondwaveevaluationdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_secondwaveevaluationdeterminanthsf_positive_successor. ff_h_mce_mdr_secondwaveevaluationdeterminanthsf_positive_successor + S (ff_s_mce_mdr_secondwaveevaluationdeterminanthsf_positive) = S ((S (S ff_i_mce_mdr_secondwaveevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_secondwaveevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_secondwaveevaluationdeterminanthsf_positive_successor. ff_u_mce_mdr_secondwaveevaluationdeterminanthsf_positive = ff_q_mce_mdr_secondwaveevaluationdeterminanthsf_positive_successor * S ((S (S ff_i_mce_mdr_secondwaveevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_secondwaveevaluationdeterminanthsf_positive) + (ff_s_mce_mdr_secondwaveevaluationdeterminanthsf_positive))) /\ ff_s_mce_mdr_secondwaveevaluationdeterminanthsf_positive = ff_r_mce_mdr_secondwaveevaluationdeterminanthsf_positive + ff_a_mce_mdr_secondwaveevaluationdeterminanthsf_positive)))))) /\ (exists ff_u_mce_mdr_secondwaveevaluationdeterminanthsf_negative ff_v_mce_mdr_secondwaveevaluationdeterminanthsf_negative. ((((exists ff_h_mce_mdr_secondwaveevaluationdeterminanthsf_negative_start. ff_h_mce_mdr_secondwaveevaluationdeterminanthsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_secondwaveevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_secondwaveevaluationdeterminanthsf_negative_start. ff_u_mce_mdr_secondwaveevaluationdeterminanthsf_negative = ff_q_mce_mdr_secondwaveevaluationdeterminanthsf_negative_start * S ((S (0)) * ff_v_mce_mdr_secondwaveevaluationdeterminanthsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_secondwaveevaluationdeterminanthsf_negative_terminal. ff_h_mce_mdr_secondwaveevaluationdeterminanthsf_negative_terminal + S (mdr_n_secondwaveevaluationdeterminanth) = S ((S ((S (mdr_q_secondwaveevaluationdeterminanths)))) * ff_v_mce_mdr_secondwaveevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_secondwaveevaluationdeterminanthsf_negative_terminal. ff_u_mce_mdr_secondwaveevaluationdeterminanthsf_negative = ff_q_mce_mdr_secondwaveevaluationdeterminanthsf_negative_terminal * S ((S ((S (mdr_q_secondwaveevaluationdeterminanths)))) * ff_v_mce_mdr_secondwaveevaluationdeterminanthsf_negative) + (mdr_n_secondwaveevaluationdeterminanth))) /\ forall ff_i_mce_mdr_secondwaveevaluationdeterminanthsf_negative. (exists ff_lt_mce_mdr_secondwaveevaluationdeterminanthsf_negative_bound. ff_lt_mce_mdr_secondwaveevaluationdeterminanthsf_negative_bound + S ff_i_mce_mdr_secondwaveevaluationdeterminanthsf_negative = (S (mdr_q_secondwaveevaluationdeterminanths))) -> exists ff_a_mce_mdr_secondwaveevaluationdeterminanthsf_negative ff_r_mce_mdr_secondwaveevaluationdeterminanthsf_negative ff_s_mce_mdr_secondwaveevaluationdeterminanthsf_negative. ((((exists ff_h_mce_mdr_secondwaveevaluationdeterminanthsf_negative_summand. ff_h_mce_mdr_secondwaveevaluationdeterminanthsf_negative_summand + S (ff_a_mce_mdr_secondwaveevaluationdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_secondwaveevaluationdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_secondwaveevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_secondwaveevaluationdeterminanthsf_negative_summand. ff_vb_mce_fold_mdr_secondwaveevaluationdeterminanthsf = ff_q_mce_mdr_secondwaveevaluationdeterminanthsf_negative_summand * S ((S (ff_i_mce_mdr_secondwaveevaluationdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_secondwaveevaluationdeterminanthsf) + (ff_a_mce_mdr_secondwaveevaluationdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_secondwaveevaluationdeterminanthsf_negative_partial. ff_h_mce_mdr_secondwaveevaluationdeterminanthsf_negative_partial + S (ff_r_mce_mdr_secondwaveevaluationdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_secondwaveevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_secondwaveevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_secondwaveevaluationdeterminanthsf_negative_partial. ff_u_mce_mdr_secondwaveevaluationdeterminanthsf_negative = ff_q_mce_mdr_secondwaveevaluationdeterminanthsf_negative_partial * S ((S (ff_i_mce_mdr_secondwaveevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_secondwaveevaluationdeterminanthsf_negative) + (ff_r_mce_mdr_secondwaveevaluationdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_secondwaveevaluationdeterminanthsf_negative_successor. ff_h_mce_mdr_secondwaveevaluationdeterminanthsf_negative_successor + S (ff_s_mce_mdr_secondwaveevaluationdeterminanthsf_negative) = S ((S (S ff_i_mce_mdr_secondwaveevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_secondwaveevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_secondwaveevaluationdeterminanthsf_negative_successor. ff_u_mce_mdr_secondwaveevaluationdeterminanthsf_negative = ff_q_mce_mdr_secondwaveevaluationdeterminanthsf_negative_successor * S ((S (S ff_i_mce_mdr_secondwaveevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_secondwaveevaluationdeterminanthsf_negative) + (ff_s_mce_mdr_secondwaveevaluationdeterminanthsf_negative))) /\ ff_s_mce_mdr_secondwaveevaluationdeterminanthsf_negative = ff_r_mce_mdr_secondwaveevaluationdeterminanthsf_negative + ff_a_mce_mdr_secondwaveevaluationdeterminanthsf_negative))))))))))))))) /\ ((exists mdr_gap_secondwaveevaluationdeterminanti. mdr_gap_secondwaveevaluationdeterminanti + S (mdr_i_secondwaveevaluationdeterminant) = (mdr_l_secondwaveevaluationdeterminant)) /\ (exists mdr_z_secondwaveevaluationdeterminantr. ((exists mdr_a_secondwaveevaluationdeterminantrc mdr_b_secondwaveevaluationdeterminantrc mdr_c_secondwaveevaluationdeterminantrc mdr_e_secondwaveevaluationdeterminantrc mdr_f_secondwaveevaluationdeterminantrc. ((mdr_a_secondwaveevaluationdeterminantrc = ((q) + (mdr_ub_secondwaveevaluation)) * S ((q) + (mdr_ub_secondwaveevaluation)) + ((mdr_ub_secondwaveevaluation) + (mdr_ub_secondwaveevaluation))) /\ ((mdr_b_secondwaveevaluationdeterminantrc = ((mdr_uc_secondwaveevaluation) + (mdr_vb_secondwaveevaluation)) * S ((mdr_uc_secondwaveevaluation) + (mdr_vb_secondwaveevaluation)) + ((mdr_vb_secondwaveevaluation) + (mdr_vb_secondwaveevaluation))) /\ ((mdr_c_secondwaveevaluationdeterminantrc = ((mdr_a_secondwaveevaluationdeterminantrc) + (mdr_b_secondwaveevaluationdeterminantrc)) * S ((mdr_a_secondwaveevaluationdeterminantrc) + (mdr_b_secondwaveevaluationdeterminantrc)) + ((mdr_b_secondwaveevaluationdeterminantrc) + (mdr_b_secondwaveevaluationdeterminantrc))) /\ ((mdr_e_secondwaveevaluationdeterminantrc = ((mdr_p_secondwave) + (mdr_n_secondwave)) * S ((mdr_p_secondwave) + (mdr_n_secondwave)) + ((mdr_n_secondwave) + (mdr_n_secondwave))) /\ ((mdr_f_secondwaveevaluationdeterminantrc = ((mdr_vc_secondwaveevaluation) + (mdr_e_secondwaveevaluationdeterminantrc)) * S ((mdr_vc_secondwaveevaluation) + (mdr_e_secondwaveevaluationdeterminantrc)) + ((mdr_e_secondwaveevaluationdeterminantrc) + (mdr_e_secondwaveevaluationdeterminantrc))) /\ ((mdr_z_secondwaveevaluationdeterminantr) = ((mdr_c_secondwaveevaluationdeterminantrc) + (mdr_f_secondwaveevaluationdeterminantrc)) * S ((mdr_c_secondwaveevaluationdeterminantrc) + (mdr_f_secondwaveevaluationdeterminantrc)) + ((mdr_f_secondwaveevaluationdeterminantrc) + (mdr_f_secondwaveevaluationdeterminantrc))))))))) /\ (((exists ff_h_mdr_secondwaveevaluationdeterminantrb. ff_h_mdr_secondwaveevaluationdeterminantrb + S (mdr_z_secondwaveevaluationdeterminantr) = S ((S (mdr_i_secondwaveevaluationdeterminant)) * mdr_c_secondwaveevaluationdeterminant)) /\ exists ff_q_mdr_secondwaveevaluationdeterminantrb. mdr_b_secondwaveevaluationdeterminant = ff_q_mdr_secondwaveevaluationdeterminantrb * S ((S (mdr_i_secondwaveevaluationdeterminant)) * mdr_c_secondwaveevaluationdeterminant) + (mdr_z_secondwaveevaluationdeterminantr)))))))))) -> mdr_p_secondwave = mdr_n_secondwave

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