NonzeroSelectedMinor(pb,pc,nb,nc,r,w,q,rb,rc,cb,cc)

((((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)) * rc)) /\ exists fom_beta_quotient_mrf_secondwaverowsbound_entry. rb = fom_beta_quotient_mrf_secondwaverowsbound_entry * S ((S (fom_index_mrf_secondwaverowsbound)) * rc) + (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)) * rc)) /\ exists ff_q_mdr_secondwaverowsdistinctfirst. rb = ff_q_mdr_secondwaverowsdistinctfirst * S ((S (mdr_i_secondwaverowsdistinct)) * rc) + (mdr_a_secondwaverowsdistinct))) -> (((exists ff_h_mdr_secondwaverowsdistinctsecond. ff_h_mdr_secondwaverowsdistinctsecond + S (mdr_a_secondwaverowsdistinct) = S ((S (mdr_j_secondwaverowsdistinct)) * rc)) /\ exists ff_q_mdr_secondwaverowsdistinctsecond. rb = ff_q_mdr_secondwaverowsdistinctsecond * S ((S (mdr_j_secondwaverowsdistinct)) * rc) + (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)) * cc)) /\ exists fom_beta_quotient_mrf_secondwavecolumnsbound_entry. cb = fom_beta_quotient_mrf_secondwavecolumnsbound_entry * S ((S (fom_index_mrf_secondwavecolumnsbound)) * cc) + (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)) * cc)) /\ exists ff_q_mdr_secondwavecolumnsdistinctfirst. cb = ff_q_mdr_secondwavecolumnsdistinctfirst * S ((S (mdr_i_secondwavecolumnsdistinct)) * cc) + (mdr_a_secondwavecolumnsdistinct))) -> (((exists ff_h_mdr_secondwavecolumnsdistinctsecond. ff_h_mdr_secondwavecolumnsdistinctsecond + S (mdr_a_secondwavecolumnsdistinct) = S ((S (mdr_j_secondwavecolumnsdistinct)) * cc)) /\ exists ff_q_mdr_secondwavecolumnsdistinctsecond. cb = ff_q_mdr_secondwavecolumnsdistinctsecond * S ((S (mdr_j_secondwavecolumnsdistinct)) * cc) + (mdr_a_secondwavecolumnsdistinct))) -> mdr_i_secondwavecolumnsdistinct = mdr_j_secondwavecolumnsdistinct))) /\ (exists mdr_p_secondwavenonzero mdr_n_secondwavenonzero. ((exists mdr_ub_secondwavenonzeroevaluation mdr_uc_secondwavenonzeroevaluation mdr_vb_secondwavenonzeroevaluation mdr_vc_secondwavenonzeroevaluation. ((((forall mdr_i_secondwavenonzeroevaluationmatrixpositive. (exists mdr_gap_secondwavenonzeroevaluationmatrixpositivebound. mdr_gap_secondwavenonzeroevaluationmatrixpositivebound + S (mdr_i_secondwavenonzeroevaluationmatrixpositive) = ((q) * (q))) -> exists mdr_a_secondwavenonzeroevaluationmatrixpositive. (((exists mdr_r_secondwavenonzeroevaluationmatrixpositivepoint mdr_s_secondwavenonzeroevaluationmatrixpositivepoint mdr_u_secondwavenonzeroevaluationmatrixpositivepoint mdr_v_secondwavenonzeroevaluationmatrixpositivepoint. ((mdr_i_secondwavenonzeroevaluationmatrixpositive = (q) * mdr_r_secondwavenonzeroevaluationmatrixpositivepoint + mdr_s_secondwavenonzeroevaluationmatrixpositivepoint) /\ ((exists mdr_gap_secondwavenonzeroevaluationmatrixpositivepointcolumn. mdr_gap_secondwavenonzeroevaluationmatrixpositivepointcolumn + S (mdr_s_secondwavenonzeroevaluationmatrixpositivepoint) = (q)) /\ ((((exists ff_h_mdr_secondwavenonzeroevaluationmatrixpositivepointrow_index. ff_h_mdr_secondwavenonzeroevaluationmatrixpositivepointrow_index + S (mdr_u_secondwavenonzeroevaluationmatrixpositivepoint) = S ((S (mdr_r_secondwavenonzeroevaluationmatrixpositivepoint)) * rc)) /\ exists ff_q_mdr_secondwavenonzeroevaluationmatrixpositivepointrow_index. rb = ff_q_mdr_secondwavenonzeroevaluationmatrixpositivepointrow_index * S ((S (mdr_r_secondwavenonzeroevaluationmatrixpositivepoint)) * rc) + (mdr_u_secondwavenonzeroevaluationmatrixpositivepoint))) /\ ((((exists ff_h_mdr_secondwavenonzeroevaluationmatrixpositivepointcolumn_index. ff_h_mdr_secondwavenonzeroevaluationmatrixpositivepointcolumn_index + S (mdr_v_secondwavenonzeroevaluationmatrixpositivepoint) = S ((S (mdr_s_secondwavenonzeroevaluationmatrixpositivepoint)) * cc)) /\ exists ff_q_mdr_secondwavenonzeroevaluationmatrixpositivepointcolumn_index. cb = ff_q_mdr_secondwavenonzeroevaluationmatrixpositivepointcolumn_index * S ((S (mdr_s_secondwavenonzeroevaluationmatrixpositivepoint)) * cc) + (mdr_v_secondwavenonzeroevaluationmatrixpositivepoint))) /\ (((exists ff_h_mdr_secondwavenonzeroevaluationmatrixpositivepointsource. ff_h_mdr_secondwavenonzeroevaluationmatrixpositivepointsource + S (mdr_a_secondwavenonzeroevaluationmatrixpositive) = S ((S ((mdr_u_secondwavenonzeroevaluationmatrixpositivepoint) * (w) + (mdr_v_secondwavenonzeroevaluationmatrixpositivepoint))) * pc)) /\ exists ff_q_mdr_secondwavenonzeroevaluationmatrixpositivepointsource. pb = ff_q_mdr_secondwavenonzeroevaluationmatrixpositivepointsource * S ((S ((mdr_u_secondwavenonzeroevaluationmatrixpositivepoint) * (w) + (mdr_v_secondwavenonzeroevaluationmatrixpositivepoint))) * pc) + (mdr_a_secondwavenonzeroevaluationmatrixpositive)))))))) /\ (((exists ff_h_mdr_secondwavenonzeroevaluationmatrixpositiveoutput. ff_h_mdr_secondwavenonzeroevaluationmatrixpositiveoutput + S (mdr_a_secondwavenonzeroevaluationmatrixpositive) = S ((S (mdr_i_secondwavenonzeroevaluationmatrixpositive)) * mdr_uc_secondwavenonzeroevaluation)) /\ exists ff_q_mdr_secondwavenonzeroevaluationmatrixpositiveoutput. mdr_ub_secondwavenonzeroevaluation = ff_q_mdr_secondwavenonzeroevaluationmatrixpositiveoutput * S ((S (mdr_i_secondwavenonzeroevaluationmatrixpositive)) * mdr_uc_secondwavenonzeroevaluation) + (mdr_a_secondwavenonzeroevaluationmatrixpositive)))))) /\ (forall mdr_i_secondwavenonzeroevaluationmatrixnegative. (exists mdr_gap_secondwavenonzeroevaluationmatrixnegativebound. mdr_gap_secondwavenonzeroevaluationmatrixnegativebound + S (mdr_i_secondwavenonzeroevaluationmatrixnegative) = ((q) * (q))) -> exists mdr_a_secondwavenonzeroevaluationmatrixnegative. (((exists mdr_r_secondwavenonzeroevaluationmatrixnegativepoint mdr_s_secondwavenonzeroevaluationmatrixnegativepoint mdr_u_secondwavenonzeroevaluationmatrixnegativepoint mdr_v_secondwavenonzeroevaluationmatrixnegativepoint. ((mdr_i_secondwavenonzeroevaluationmatrixnegative = (q) * mdr_r_secondwavenonzeroevaluationmatrixnegativepoint + mdr_s_secondwavenonzeroevaluationmatrixnegativepoint) /\ ((exists mdr_gap_secondwavenonzeroevaluationmatrixnegativepointcolumn. mdr_gap_secondwavenonzeroevaluationmatrixnegativepointcolumn + S (mdr_s_secondwavenonzeroevaluationmatrixnegativepoint) = (q)) /\ ((((exists ff_h_mdr_secondwavenonzeroevaluationmatrixnegativepointrow_index. ff_h_mdr_secondwavenonzeroevaluationmatrixnegativepointrow_index + S (mdr_u_secondwavenonzeroevaluationmatrixnegativepoint) = S ((S (mdr_r_secondwavenonzeroevaluationmatrixnegativepoint)) * rc)) /\ exists ff_q_mdr_secondwavenonzeroevaluationmatrixnegativepointrow_index. rb = ff_q_mdr_secondwavenonzeroevaluationmatrixnegativepointrow_index * S ((S (mdr_r_secondwavenonzeroevaluationmatrixnegativepoint)) * rc) + (mdr_u_secondwavenonzeroevaluationmatrixnegativepoint))) /\ ((((exists ff_h_mdr_secondwavenonzeroevaluationmatrixnegativepointcolumn_index. ff_h_mdr_secondwavenonzeroevaluationmatrixnegativepointcolumn_index + S (mdr_v_secondwavenonzeroevaluationmatrixnegativepoint) = S ((S (mdr_s_secondwavenonzeroevaluationmatrixnegativepoint)) * cc)) /\ exists ff_q_mdr_secondwavenonzeroevaluationmatrixnegativepointcolumn_index. cb = ff_q_mdr_secondwavenonzeroevaluationmatrixnegativepointcolumn_index * S ((S (mdr_s_secondwavenonzeroevaluationmatrixnegativepoint)) * cc) + (mdr_v_secondwavenonzeroevaluationmatrixnegativepoint))) /\ (((exists ff_h_mdr_secondwavenonzeroevaluationmatrixnegativepointsource. ff_h_mdr_secondwavenonzeroevaluationmatrixnegativepointsource + S (mdr_a_secondwavenonzeroevaluationmatrixnegative) = S ((S ((mdr_u_secondwavenonzeroevaluationmatrixnegativepoint) * (w) + (mdr_v_secondwavenonzeroevaluationmatrixnegativepoint))) * nc)) /\ exists ff_q_mdr_secondwavenonzeroevaluationmatrixnegativepointsource. nb = ff_q_mdr_secondwavenonzeroevaluationmatrixnegativepointsource * S ((S ((mdr_u_secondwavenonzeroevaluationmatrixnegativepoint) * (w) + (mdr_v_secondwavenonzeroevaluationmatrixnegativepoint))) * nc) + (mdr_a_secondwavenonzeroevaluationmatrixnegative)))))))) /\ (((exists ff_h_mdr_secondwavenonzeroevaluationmatrixnegativeoutput. ff_h_mdr_secondwavenonzeroevaluationmatrixnegativeoutput + S (mdr_a_secondwavenonzeroevaluationmatrixnegative) = S ((S (mdr_i_secondwavenonzeroevaluationmatrixnegative)) * mdr_vc_secondwavenonzeroevaluation)) /\ exists ff_q_mdr_secondwavenonzeroevaluationmatrixnegativeoutput. mdr_vb_secondwavenonzeroevaluation = ff_q_mdr_secondwavenonzeroevaluationmatrixnegativeoutput * S ((S (mdr_i_secondwavenonzeroevaluationmatrixnegative)) * mdr_vc_secondwavenonzeroevaluation) + (mdr_a_secondwavenonzeroevaluationmatrixnegative)))))))) /\ (exists mdr_b_secondwavenonzeroevaluationdeterminant mdr_c_secondwavenonzeroevaluationdeterminant mdr_l_secondwavenonzeroevaluationdeterminant mdr_i_secondwavenonzeroevaluationdeterminant. ((forall mdr_i_secondwavenonzeroevaluationdeterminanth. (exists mdr_gap_secondwavenonzeroevaluationdeterminanthi. mdr_gap_secondwavenonzeroevaluationdeterminanthi + S (mdr_i_secondwavenonzeroevaluationdeterminanth) = (mdr_l_secondwavenonzeroevaluationdeterminant)) -> exists mdr_d_secondwavenonzeroevaluationdeterminanth mdr_pb_secondwavenonzeroevaluationdeterminanth mdr_pc_secondwavenonzeroevaluationdeterminanth mdr_nb_secondwavenonzeroevaluationdeterminanth mdr_nc_secondwavenonzeroevaluationdeterminanth mdr_p_secondwavenonzeroevaluationdeterminanth mdr_n_secondwavenonzeroevaluationdeterminanth. ((exists mdr_z_secondwavenonzeroevaluationdeterminanthr. ((exists mdr_a_secondwavenonzeroevaluationdeterminanthrc mdr_b_secondwavenonzeroevaluationdeterminanthrc mdr_c_secondwavenonzeroevaluationdeterminanthrc mdr_e_secondwavenonzeroevaluationdeterminanthrc mdr_f_secondwavenonzeroevaluationdeterminanthrc. ((mdr_a_secondwavenonzeroevaluationdeterminanthrc = ((mdr_d_secondwavenonzeroevaluationdeterminanth) + (mdr_pb_secondwavenonzeroevaluationdeterminanth)) * S ((mdr_d_secondwavenonzeroevaluationdeterminanth) + (mdr_pb_secondwavenonzeroevaluationdeterminanth)) + ((mdr_pb_secondwavenonzeroevaluationdeterminanth) + (mdr_pb_secondwavenonzeroevaluationdeterminanth))) /\ ((mdr_b_secondwavenonzeroevaluationdeterminanthrc = ((mdr_pc_secondwavenonzeroevaluationdeterminanth) + (mdr_nb_secondwavenonzeroevaluationdeterminanth)) * S ((mdr_pc_secondwavenonzeroevaluationdeterminanth) + (mdr_nb_secondwavenonzeroevaluationdeterminanth)) + ((mdr_nb_secondwavenonzeroevaluationdeterminanth) + (mdr_nb_secondwavenonzeroevaluationdeterminanth))) /\ ((mdr_c_secondwavenonzeroevaluationdeterminanthrc = ((mdr_a_secondwavenonzeroevaluationdeterminanthrc) + (mdr_b_secondwavenonzeroevaluationdeterminanthrc)) * S ((mdr_a_secondwavenonzeroevaluationdeterminanthrc) + (mdr_b_secondwavenonzeroevaluationdeterminanthrc)) + ((mdr_b_secondwavenonzeroevaluationdeterminanthrc) + (mdr_b_secondwavenonzeroevaluationdeterminanthrc))) /\ ((mdr_e_secondwavenonzeroevaluationdeterminanthrc = ((mdr_p_secondwavenonzeroevaluationdeterminanth) + (mdr_n_secondwavenonzeroevaluationdeterminanth)) * S ((mdr_p_secondwavenonzeroevaluationdeterminanth) + (mdr_n_secondwavenonzeroevaluationdeterminanth)) + ((mdr_n_secondwavenonzeroevaluationdeterminanth) + (mdr_n_secondwavenonzeroevaluationdeterminanth))) /\ ((mdr_f_secondwavenonzeroevaluationdeterminanthrc = ((mdr_nc_secondwavenonzeroevaluationdeterminanth) + (mdr_e_secondwavenonzeroevaluationdeterminanthrc)) * S ((mdr_nc_secondwavenonzeroevaluationdeterminanth) + (mdr_e_secondwavenonzeroevaluationdeterminanthrc)) + ((mdr_e_secondwavenonzeroevaluationdeterminanthrc) + (mdr_e_secondwavenonzeroevaluationdeterminanthrc))) /\ ((mdr_z_secondwavenonzeroevaluationdeterminanthr) = ((mdr_c_secondwavenonzeroevaluationdeterminanthrc) + (mdr_f_secondwavenonzeroevaluationdeterminanthrc)) * S ((mdr_c_secondwavenonzeroevaluationdeterminanthrc) + (mdr_f_secondwavenonzeroevaluationdeterminanthrc)) + ((mdr_f_secondwavenonzeroevaluationdeterminanthrc) + (mdr_f_secondwavenonzeroevaluationdeterminanthrc))))))))) /\ (((exists ff_h_mdr_secondwavenonzeroevaluationdeterminanthrb. ff_h_mdr_secondwavenonzeroevaluationdeterminanthrb + S (mdr_z_secondwavenonzeroevaluationdeterminanthr) = S ((S (mdr_i_secondwavenonzeroevaluationdeterminanth)) * mdr_c_secondwavenonzeroevaluationdeterminant)) /\ exists ff_q_mdr_secondwavenonzeroevaluationdeterminanthrb. mdr_b_secondwavenonzeroevaluationdeterminant = ff_q_mdr_secondwavenonzeroevaluationdeterminanthrb * S ((S (mdr_i_secondwavenonzeroevaluationdeterminanth)) * mdr_c_secondwavenonzeroevaluationdeterminant) + (mdr_z_secondwavenonzeroevaluationdeterminanthr))))) /\ (((((mdr_d_secondwavenonzeroevaluationdeterminanth) = 0) /\ (((mdr_p_secondwavenonzeroevaluationdeterminanth) = 1) /\ ((mdr_n_secondwavenonzeroevaluationdeterminanth) = 0))) \/ exists mdr_q_secondwavenonzeroevaluationdeterminanths mdr_eb_secondwavenonzeroevaluationdeterminanths mdr_ec_secondwavenonzeroevaluationdeterminanths mdr_fb_secondwavenonzeroevaluationdeterminanths mdr_fc_secondwavenonzeroevaluationdeterminanths. (((mdr_d_secondwavenonzeroevaluationdeterminanth) = S (mdr_q_secondwavenonzeroevaluationdeterminanths)) /\ ((forall mdr_j_secondwavenonzeroevaluationdeterminanthsc. (exists mdr_gap_secondwavenonzeroevaluationdeterminanthscj. mdr_gap_secondwavenonzeroevaluationdeterminanthscj + S (mdr_j_secondwavenonzeroevaluationdeterminanthsc) = (S (mdr_q_secondwavenonzeroevaluationdeterminanths))) -> exists mdr_i_secondwavenonzeroevaluationdeterminanthsc mdr_up_secondwavenonzeroevaluationdeterminanthsc mdr_us_secondwavenonzeroevaluationdeterminanthsc mdr_un_secondwavenonzeroevaluationdeterminanthsc mdr_ut_secondwavenonzeroevaluationdeterminanthsc mdr_p_secondwavenonzeroevaluationdeterminanthsc mdr_n_secondwavenonzeroevaluationdeterminanthsc. ((exists mdr_gap_secondwavenonzeroevaluationdeterminanthsci. mdr_gap_secondwavenonzeroevaluationdeterminanthsci + S (mdr_i_secondwavenonzeroevaluationdeterminanthsc) = (mdr_i_secondwavenonzeroevaluationdeterminanth)) /\ ((exists mdr_z_secondwavenonzeroevaluationdeterminanthscr. ((exists mdr_a_secondwavenonzeroevaluationdeterminanthscrc mdr_b_secondwavenonzeroevaluationdeterminanthscrc mdr_c_secondwavenonzeroevaluationdeterminanthscrc mdr_e_secondwavenonzeroevaluationdeterminanthscrc mdr_f_secondwavenonzeroevaluationdeterminanthscrc. ((mdr_a_secondwavenonzeroevaluationdeterminanthscrc = ((mdr_q_secondwavenonzeroevaluationdeterminanths) + (mdr_up_secondwavenonzeroevaluationdeterminanthsc)) * S ((mdr_q_secondwavenonzeroevaluationdeterminanths) + (mdr_up_secondwavenonzeroevaluationdeterminanthsc)) + ((mdr_up_secondwavenonzeroevaluationdeterminanthsc) + (mdr_up_secondwavenonzeroevaluationdeterminanthsc))) /\ ((mdr_b_secondwavenonzeroevaluationdeterminanthscrc = ((mdr_us_secondwavenonzeroevaluationdeterminanthsc) + (mdr_un_secondwavenonzeroevaluationdeterminanthsc)) * S ((mdr_us_secondwavenonzeroevaluationdeterminanthsc) + (mdr_un_secondwavenonzeroevaluationdeterminanthsc)) + ((mdr_un_secondwavenonzeroevaluationdeterminanthsc) + (mdr_un_secondwavenonzeroevaluationdeterminanthsc))) /\ ((mdr_c_secondwavenonzeroevaluationdeterminanthscrc = ((mdr_a_secondwavenonzeroevaluationdeterminanthscrc) + (mdr_b_secondwavenonzeroevaluationdeterminanthscrc)) * S ((mdr_a_secondwavenonzeroevaluationdeterminanthscrc) + (mdr_b_secondwavenonzeroevaluationdeterminanthscrc)) + ((mdr_b_secondwavenonzeroevaluationdeterminanthscrc) + (mdr_b_secondwavenonzeroevaluationdeterminanthscrc))) /\ ((mdr_e_secondwavenonzeroevaluationdeterminanthscrc = ((mdr_p_secondwavenonzeroevaluationdeterminanthsc) + (mdr_n_secondwavenonzeroevaluationdeterminanthsc)) * S ((mdr_p_secondwavenonzeroevaluationdeterminanthsc) + (mdr_n_secondwavenonzeroevaluationdeterminanthsc)) + ((mdr_n_secondwavenonzeroevaluationdeterminanthsc) + (mdr_n_secondwavenonzeroevaluationdeterminanthsc))) /\ ((mdr_f_secondwavenonzeroevaluationdeterminanthscrc = ((mdr_ut_secondwavenonzeroevaluationdeterminanthsc) + (mdr_e_secondwavenonzeroevaluationdeterminanthscrc)) * S ((mdr_ut_secondwavenonzeroevaluationdeterminanthsc) + (mdr_e_secondwavenonzeroevaluationdeterminanthscrc)) + ((mdr_e_secondwavenonzeroevaluationdeterminanthscrc) + (mdr_e_secondwavenonzeroevaluationdeterminanthscrc))) /\ ((mdr_z_secondwavenonzeroevaluationdeterminanthscr) = ((mdr_c_secondwavenonzeroevaluationdeterminanthscrc) + (mdr_f_secondwavenonzeroevaluationdeterminanthscrc)) * S ((mdr_c_secondwavenonzeroevaluationdeterminanthscrc) + (mdr_f_secondwavenonzeroevaluationdeterminanthscrc)) + ((mdr_f_secondwavenonzeroevaluationdeterminanthscrc) + (mdr_f_secondwavenonzeroevaluationdeterminanthscrc))))))))) /\ (((exists ff_h_mdr_secondwavenonzeroevaluationdeterminanthscrb. ff_h_mdr_secondwavenonzeroevaluationdeterminanthscrb + S (mdr_z_secondwavenonzeroevaluationdeterminanthscr) = S ((S (mdr_i_secondwavenonzeroevaluationdeterminanthsc)) * mdr_c_secondwavenonzeroevaluationdeterminant)) /\ exists ff_q_mdr_secondwavenonzeroevaluationdeterminanthscrb. mdr_b_secondwavenonzeroevaluationdeterminant = ff_q_mdr_secondwavenonzeroevaluationdeterminanthscrb * S ((S (mdr_i_secondwavenonzeroevaluationdeterminanthsc)) * mdr_c_secondwavenonzeroevaluationdeterminant) + (mdr_z_secondwavenonzeroevaluationdeterminanthscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_secondwavenonzeroevaluationdeterminanthscm_positive. (exists ff_gap_mdm_lt_mdr_secondwavenonzeroevaluationdeterminanthscm_positive_index_bound. ff_gap_mdm_lt_mdr_secondwavenonzeroevaluationdeterminanthscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_secondwavenonzeroevaluationdeterminanthscm_positive) = ((mdr_q_secondwavenonzeroevaluationdeterminanths) * (mdr_q_secondwavenonzeroevaluationdeterminanths))) -> exists ff_row_mdm_prefix_mdr_secondwavenonzeroevaluationdeterminanthscm_positive ff_column_mdm_prefix_mdr_secondwavenonzeroevaluationdeterminanthscm_positive ff_value_mdm_prefix_mdr_secondwavenonzeroevaluationdeterminanthscm_positive. (ff_index_mdm_prefix_mdr_secondwavenonzeroevaluationdeterminanthscm_positive = (mdr_q_secondwavenonzeroevaluationdeterminanths) * ff_row_mdm_prefix_mdr_secondwavenonzeroevaluationdeterminanthscm_positive + ff_column_mdm_prefix_mdr_secondwavenonzeroevaluationdeterminanthscm_positive /\ ((exists ff_gap_mdm_lt_mdr_secondwavenonzeroevaluationdeterminanthscm_positive_column_bound. ff_gap_mdm_lt_mdr_secondwavenonzeroevaluationdeterminanthscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_secondwavenonzeroevaluationdeterminanthscm_positive) = (mdr_q_secondwavenonzeroevaluationdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_secondwavenonzeroevaluationdeterminanthscm_positive_cell ff_column_mdm_cell_mdr_secondwavenonzeroevaluationdeterminanthscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_secondwavenonzeroevaluationdeterminanthscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_secondwavenonzeroevaluationdeterminanthscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_secondwavenonzeroevaluationdeterminanthscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_secondwavenonzeroevaluationdeterminanthscm_positive_cell = ff_row_mdm_prefix_mdr_secondwavenonzeroevaluationdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_secondwavenonzeroevaluationdeterminanthscm_positive_cell_row_after. ff_gap_mdm_le_mdr_secondwavenonzeroevaluationdeterminanthscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_secondwavenonzeroevaluationdeterminanthscm_positive)) /\ ff_row_mdm_cell_mdr_secondwavenonzeroevaluationdeterminanthscm_positive_cell = S ff_row_mdm_prefix_mdr_secondwavenonzeroevaluationdeterminanthscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_secondwavenonzeroevaluationdeterminanthscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_secondwavenonzeroevaluationdeterminanthscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_secondwavenonzeroevaluationdeterminanthscm_positive) = (mdr_j_secondwavenonzeroevaluationdeterminanthsc)) /\ ff_column_mdm_cell_mdr_secondwavenonzeroevaluationdeterminanthscm_positive_cell = ff_column_mdm_prefix_mdr_secondwavenonzeroevaluationdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_secondwavenonzeroevaluationdeterminanthscm_positive_cell_column_after. ff_gap_mdm_le_mdr_secondwavenonzeroevaluationdeterminanthscm_positive_cell_column_after + (mdr_j_secondwavenonzeroevaluationdeterminanthsc) = (ff_column_mdm_prefix_mdr_secondwavenonzeroevaluationdeterminanthscm_positive)) /\ ff_column_mdm_cell_mdr_secondwavenonzeroevaluationdeterminanthscm_positive_cell = S ff_column_mdm_prefix_mdr_secondwavenonzeroevaluationdeterminanthscm_positive))) /\ (((exists ff_h_mdm_mdr_secondwavenonzeroevaluationdeterminanthscm_positive_cell_source. ff_h_mdm_mdr_secondwavenonzeroevaluationdeterminanthscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_secondwavenonzeroevaluationdeterminanthscm_positive) = S ((S ((ff_row_mdm_cell_mdr_secondwavenonzeroevaluationdeterminanthscm_positive_cell) * (S (mdr_q_secondwavenonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_secondwavenonzeroevaluationdeterminanthscm_positive_cell))) * mdr_pc_secondwavenonzeroevaluationdeterminanth)) /\ exists ff_q_mdm_mdr_secondwavenonzeroevaluationdeterminanthscm_positive_cell_source. mdr_pb_secondwavenonzeroevaluationdeterminanth = ff_q_mdm_mdr_secondwavenonzeroevaluationdeterminanthscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_secondwavenonzeroevaluationdeterminanthscm_positive_cell) * (S (mdr_q_secondwavenonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_secondwavenonzeroevaluationdeterminanthscm_positive_cell))) * mdr_pc_secondwavenonzeroevaluationdeterminanth) + (ff_value_mdm_prefix_mdr_secondwavenonzeroevaluationdeterminanthscm_positive)))))) /\ (((exists ff_h_mdm_mdr_secondwavenonzeroevaluationdeterminanthscm_positive_target. ff_h_mdm_mdr_secondwavenonzeroevaluationdeterminanthscm_positive_target + S (ff_value_mdm_prefix_mdr_secondwavenonzeroevaluationdeterminanthscm_positive) = S ((S (ff_index_mdm_prefix_mdr_secondwavenonzeroevaluationdeterminanthscm_positive)) * mdr_us_secondwavenonzeroevaluationdeterminanthsc)) /\ exists ff_q_mdm_mdr_secondwavenonzeroevaluationdeterminanthscm_positive_target. mdr_up_secondwavenonzeroevaluationdeterminanthsc = ff_q_mdm_mdr_secondwavenonzeroevaluationdeterminanthscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_secondwavenonzeroevaluationdeterminanthscm_positive)) * mdr_us_secondwavenonzeroevaluationdeterminanthsc) + (ff_value_mdm_prefix_mdr_secondwavenonzeroevaluationdeterminanthscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_secondwavenonzeroevaluationdeterminanthscm_negative. (exists ff_gap_mdm_lt_mdr_secondwavenonzeroevaluationdeterminanthscm_negative_index_bound. ff_gap_mdm_lt_mdr_secondwavenonzeroevaluationdeterminanthscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_secondwavenonzeroevaluationdeterminanthscm_negative) = ((mdr_q_secondwavenonzeroevaluationdeterminanths) * (mdr_q_secondwavenonzeroevaluationdeterminanths))) -> exists ff_row_mdm_prefix_mdr_secondwavenonzeroevaluationdeterminanthscm_negative ff_column_mdm_prefix_mdr_secondwavenonzeroevaluationdeterminanthscm_negative ff_value_mdm_prefix_mdr_secondwavenonzeroevaluationdeterminanthscm_negative. (ff_index_mdm_prefix_mdr_secondwavenonzeroevaluationdeterminanthscm_negative = (mdr_q_secondwavenonzeroevaluationdeterminanths) * ff_row_mdm_prefix_mdr_secondwavenonzeroevaluationdeterminanthscm_negative + ff_column_mdm_prefix_mdr_secondwavenonzeroevaluationdeterminanthscm_negative /\ ((exists ff_gap_mdm_lt_mdr_secondwavenonzeroevaluationdeterminanthscm_negative_column_bound. ff_gap_mdm_lt_mdr_secondwavenonzeroevaluationdeterminanthscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_secondwavenonzeroevaluationdeterminanthscm_negative) = (mdr_q_secondwavenonzeroevaluationdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_secondwavenonzeroevaluationdeterminanthscm_negative_cell ff_column_mdm_cell_mdr_secondwavenonzeroevaluationdeterminanthscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_secondwavenonzeroevaluationdeterminanthscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_secondwavenonzeroevaluationdeterminanthscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_secondwavenonzeroevaluationdeterminanthscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_secondwavenonzeroevaluationdeterminanthscm_negative_cell = ff_row_mdm_prefix_mdr_secondwavenonzeroevaluationdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_secondwavenonzeroevaluationdeterminanthscm_negative_cell_row_after. ff_gap_mdm_le_mdr_secondwavenonzeroevaluationdeterminanthscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_secondwavenonzeroevaluationdeterminanthscm_negative)) /\ ff_row_mdm_cell_mdr_secondwavenonzeroevaluationdeterminanthscm_negative_cell = S ff_row_mdm_prefix_mdr_secondwavenonzeroevaluationdeterminanthscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_secondwavenonzeroevaluationdeterminanthscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_secondwavenonzeroevaluationdeterminanthscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_secondwavenonzeroevaluationdeterminanthscm_negative) = (mdr_j_secondwavenonzeroevaluationdeterminanthsc)) /\ ff_column_mdm_cell_mdr_secondwavenonzeroevaluationdeterminanthscm_negative_cell = ff_column_mdm_prefix_mdr_secondwavenonzeroevaluationdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_secondwavenonzeroevaluationdeterminanthscm_negative_cell_column_after. ff_gap_mdm_le_mdr_secondwavenonzeroevaluationdeterminanthscm_negative_cell_column_after + (mdr_j_secondwavenonzeroevaluationdeterminanthsc) = (ff_column_mdm_prefix_mdr_secondwavenonzeroevaluationdeterminanthscm_negative)) /\ ff_column_mdm_cell_mdr_secondwavenonzeroevaluationdeterminanthscm_negative_cell = S ff_column_mdm_prefix_mdr_secondwavenonzeroevaluationdeterminanthscm_negative))) /\ (((exists ff_h_mdm_mdr_secondwavenonzeroevaluationdeterminanthscm_negative_cell_source. ff_h_mdm_mdr_secondwavenonzeroevaluationdeterminanthscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_secondwavenonzeroevaluationdeterminanthscm_negative) = S ((S ((ff_row_mdm_cell_mdr_secondwavenonzeroevaluationdeterminanthscm_negative_cell) * (S (mdr_q_secondwavenonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_secondwavenonzeroevaluationdeterminanthscm_negative_cell))) * mdr_nc_secondwavenonzeroevaluationdeterminanth)) /\ exists ff_q_mdm_mdr_secondwavenonzeroevaluationdeterminanthscm_negative_cell_source. mdr_nb_secondwavenonzeroevaluationdeterminanth = ff_q_mdm_mdr_secondwavenonzeroevaluationdeterminanthscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_secondwavenonzeroevaluationdeterminanthscm_negative_cell) * (S (mdr_q_secondwavenonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_secondwavenonzeroevaluationdeterminanthscm_negative_cell))) * mdr_nc_secondwavenonzeroevaluationdeterminanth) + (ff_value_mdm_prefix_mdr_secondwavenonzeroevaluationdeterminanthscm_negative)))))) /\ (((exists ff_h_mdm_mdr_secondwavenonzeroevaluationdeterminanthscm_negative_target. ff_h_mdm_mdr_secondwavenonzeroevaluationdeterminanthscm_negative_target + S (ff_value_mdm_prefix_mdr_secondwavenonzeroevaluationdeterminanthscm_negative) = S ((S (ff_index_mdm_prefix_mdr_secondwavenonzeroevaluationdeterminanthscm_negative)) * mdr_ut_secondwavenonzeroevaluationdeterminanthsc)) /\ exists ff_q_mdm_mdr_secondwavenonzeroevaluationdeterminanthscm_negative_target. mdr_un_secondwavenonzeroevaluationdeterminanthsc = ff_q_mdm_mdr_secondwavenonzeroevaluationdeterminanthscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_secondwavenonzeroevaluationdeterminanthscm_negative)) * mdr_ut_secondwavenonzeroevaluationdeterminanthsc) + (ff_value_mdm_prefix_mdr_secondwavenonzeroevaluationdeterminanthscm_negative))))))))) /\ ((((exists ff_h_mdr_secondwavenonzeroevaluationdeterminanthscp. ff_h_mdr_secondwavenonzeroevaluationdeterminanthscp + S (mdr_p_secondwavenonzeroevaluationdeterminanthsc) = S ((S (mdr_j_secondwavenonzeroevaluationdeterminanthsc)) * mdr_ec_secondwavenonzeroevaluationdeterminanths)) /\ exists ff_q_mdr_secondwavenonzeroevaluationdeterminanthscp. mdr_eb_secondwavenonzeroevaluationdeterminanths = ff_q_mdr_secondwavenonzeroevaluationdeterminanthscp * S ((S (mdr_j_secondwavenonzeroevaluationdeterminanthsc)) * mdr_ec_secondwavenonzeroevaluationdeterminanths) + (mdr_p_secondwavenonzeroevaluationdeterminanthsc))) /\ (((exists ff_h_mdr_secondwavenonzeroevaluationdeterminanthscn. ff_h_mdr_secondwavenonzeroevaluationdeterminanthscn + S (mdr_n_secondwavenonzeroevaluationdeterminanthsc) = S ((S (mdr_j_secondwavenonzeroevaluationdeterminanthsc)) * mdr_fc_secondwavenonzeroevaluationdeterminanths)) /\ exists ff_q_mdr_secondwavenonzeroevaluationdeterminanthscn. mdr_fb_secondwavenonzeroevaluationdeterminanths = ff_q_mdr_secondwavenonzeroevaluationdeterminanthscn * S ((S (mdr_j_secondwavenonzeroevaluationdeterminanthsc)) * mdr_fc_secondwavenonzeroevaluationdeterminanths) + (mdr_n_secondwavenonzeroevaluationdeterminanthsc)))))))) /\ (exists ff_ub_mce_fold_mdr_secondwavenonzeroevaluationdeterminanthsf ff_uc_mce_fold_mdr_secondwavenonzeroevaluationdeterminanthsf ff_vb_mce_fold_mdr_secondwavenonzeroevaluationdeterminanthsf ff_vc_mce_fold_mdr_secondwavenonzeroevaluationdeterminanthsf. ((forall ff_index_mce_alternating_mdr_secondwavenonzeroevaluationdeterminanthsf_prefix. (exists ff_gap_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_prefix_index. ff_gap_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_prefix_index + S (ff_index_mce_alternating_mdr_secondwavenonzeroevaluationdeterminanthsf_prefix) = (S (mdr_q_secondwavenonzeroevaluationdeterminanths))) -> exists ff_ap_mce_alternating_mdr_secondwavenonzeroevaluationdeterminanthsf_prefix ff_an_mce_alternating_mdr_secondwavenonzeroevaluationdeterminanthsf_prefix ff_bp_mce_alternating_mdr_secondwavenonzeroevaluationdeterminanthsf_prefix ff_bn_mce_alternating_mdr_secondwavenonzeroevaluationdeterminanthsf_prefix ff_p_mce_alternating_mdr_secondwavenonzeroevaluationdeterminanthsf_prefix ff_n_mce_alternating_mdr_secondwavenonzeroevaluationdeterminanthsf_prefix. ((((exists ff_h_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_prefix_ap. ff_h_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_prefix_ap + S (ff_ap_mce_alternating_mdr_secondwavenonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_secondwavenonzeroevaluationdeterminanthsf_prefix)) * mdr_pc_secondwavenonzeroevaluationdeterminanth)) /\ exists ff_q_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_prefix_ap. mdr_pb_secondwavenonzeroevaluationdeterminanth = ff_q_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_secondwavenonzeroevaluationdeterminanthsf_prefix)) * mdr_pc_secondwavenonzeroevaluationdeterminanth) + (ff_ap_mce_alternating_mdr_secondwavenonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_prefix_an. ff_h_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_prefix_an + S (ff_an_mce_alternating_mdr_secondwavenonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_secondwavenonzeroevaluationdeterminanthsf_prefix)) * mdr_nc_secondwavenonzeroevaluationdeterminanth)) /\ exists ff_q_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_prefix_an. mdr_nb_secondwavenonzeroevaluationdeterminanth = ff_q_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_secondwavenonzeroevaluationdeterminanthsf_prefix)) * mdr_nc_secondwavenonzeroevaluationdeterminanth) + (ff_an_mce_alternating_mdr_secondwavenonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_prefix_bp. ff_h_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_prefix_bp + S (ff_bp_mce_alternating_mdr_secondwavenonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_secondwavenonzeroevaluationdeterminanthsf_prefix)) * mdr_ec_secondwavenonzeroevaluationdeterminanths)) /\ exists ff_q_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_prefix_bp. mdr_eb_secondwavenonzeroevaluationdeterminanths = ff_q_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_secondwavenonzeroevaluationdeterminanthsf_prefix)) * mdr_ec_secondwavenonzeroevaluationdeterminanths) + (ff_bp_mce_alternating_mdr_secondwavenonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_prefix_bn. ff_h_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_prefix_bn + S (ff_bn_mce_alternating_mdr_secondwavenonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_secondwavenonzeroevaluationdeterminanthsf_prefix)) * mdr_fc_secondwavenonzeroevaluationdeterminanths)) /\ exists ff_q_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_prefix_bn. mdr_fb_secondwavenonzeroevaluationdeterminanths = ff_q_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_secondwavenonzeroevaluationdeterminanthsf_prefix)) * mdr_fc_secondwavenonzeroevaluationdeterminanths) + (ff_bn_mce_alternating_mdr_secondwavenonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_prefix_positive. ff_h_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_prefix_positive + S (ff_p_mce_alternating_mdr_secondwavenonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_secondwavenonzeroevaluationdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_secondwavenonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_prefix_positive. ff_ub_mce_fold_mdr_secondwavenonzeroevaluationdeterminanthsf = ff_q_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_secondwavenonzeroevaluationdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_secondwavenonzeroevaluationdeterminanthsf) + (ff_p_mce_alternating_mdr_secondwavenonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_prefix_negative. ff_h_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_prefix_negative + S (ff_n_mce_alternating_mdr_secondwavenonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_secondwavenonzeroevaluationdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_secondwavenonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_prefix_negative. ff_vb_mce_fold_mdr_secondwavenonzeroevaluationdeterminanthsf = ff_q_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_secondwavenonzeroevaluationdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_secondwavenonzeroevaluationdeterminanthsf) + (ff_n_mce_alternating_mdr_secondwavenonzeroevaluationdeterminanthsf_prefix))) /\ (((exists ff_even_mce_term_mdr_secondwavenonzeroevaluationdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_secondwavenonzeroevaluationdeterminanthsf_prefix = 2 * ff_even_mce_term_mdr_secondwavenonzeroevaluationdeterminanthsf_prefix_term) /\ (ff_p_mce_alternating_mdr_secondwavenonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_secondwavenonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_secondwavenonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_secondwavenonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_secondwavenonzeroevaluationdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_secondwavenonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_secondwavenonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_secondwavenonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_secondwavenonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_secondwavenonzeroevaluationdeterminanthsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_secondwavenonzeroevaluationdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_secondwavenonzeroevaluationdeterminanthsf_prefix = 2 * ff_odd_mce_term_mdr_secondwavenonzeroevaluationdeterminanthsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_secondwavenonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_secondwavenonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_secondwavenonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_secondwavenonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_secondwavenonzeroevaluationdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_secondwavenonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_secondwavenonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_secondwavenonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_secondwavenonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_secondwavenonzeroevaluationdeterminanthsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_positive ff_v_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_positive. ((((exists ff_h_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_positive_start. ff_h_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_positive_start. ff_u_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_positive_start * S ((S (0)) * ff_v_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_positive_terminal. ff_h_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_positive_terminal + S (mdr_p_secondwavenonzeroevaluationdeterminanth) = S ((S ((S (mdr_q_secondwavenonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_positive_terminal. ff_u_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_positive_terminal * S ((S ((S (mdr_q_secondwavenonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_positive) + (mdr_p_secondwavenonzeroevaluationdeterminanth))) /\ forall ff_i_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_positive. (exists ff_lt_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_positive_bound. ff_lt_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_positive_bound + S ff_i_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_positive = (S (mdr_q_secondwavenonzeroevaluationdeterminanths))) -> exists ff_a_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_positive ff_r_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_positive ff_s_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_positive. ((((exists ff_h_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_positive_summand. ff_h_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_positive_summand + S (ff_a_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_secondwavenonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_positive_summand. ff_ub_mce_fold_mdr_secondwavenonzeroevaluationdeterminanthsf = ff_q_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_positive_summand * S ((S (ff_i_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_secondwavenonzeroevaluationdeterminanthsf) + (ff_a_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_positive_partial. ff_h_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_positive_partial + S (ff_r_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_positive_partial. ff_u_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_positive_partial * S ((S (ff_i_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_positive) + (ff_r_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_positive_successor. ff_h_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_positive_successor + S (ff_s_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_positive) = S ((S (S ff_i_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_positive_successor. ff_u_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_positive_successor * S ((S (S ff_i_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_positive) + (ff_s_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_positive))) /\ ff_s_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_positive = ff_r_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_positive + ff_a_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_positive)))))) /\ (exists ff_u_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_negative ff_v_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_negative. ((((exists ff_h_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_negative_start. ff_h_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_negative_start. ff_u_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_negative_start * S ((S (0)) * ff_v_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_negative_terminal. ff_h_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_negative_terminal + S (mdr_n_secondwavenonzeroevaluationdeterminanth) = S ((S ((S (mdr_q_secondwavenonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_negative_terminal. ff_u_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_negative_terminal * S ((S ((S (mdr_q_secondwavenonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_negative) + (mdr_n_secondwavenonzeroevaluationdeterminanth))) /\ forall ff_i_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_negative. (exists ff_lt_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_negative_bound. ff_lt_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_negative_bound + S ff_i_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_negative = (S (mdr_q_secondwavenonzeroevaluationdeterminanths))) -> exists ff_a_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_negative ff_r_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_negative ff_s_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_negative. ((((exists ff_h_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_negative_summand. ff_h_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_negative_summand + S (ff_a_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_secondwavenonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_negative_summand. ff_vb_mce_fold_mdr_secondwavenonzeroevaluationdeterminanthsf = ff_q_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_negative_summand * S ((S (ff_i_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_secondwavenonzeroevaluationdeterminanthsf) + (ff_a_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_negative_partial. ff_h_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_negative_partial + S (ff_r_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_negative_partial. ff_u_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_negative_partial * S ((S (ff_i_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_negative) + (ff_r_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_negative_successor. ff_h_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_negative_successor + S (ff_s_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_negative) = S ((S (S ff_i_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_negative_successor. ff_u_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_negative_successor * S ((S (S ff_i_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_negative) + (ff_s_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_negative))) /\ ff_s_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_negative = ff_r_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_negative + ff_a_mce_mdr_secondwavenonzeroevaluationdeterminanthsf_negative))))))))))))))) /\ ((exists mdr_gap_secondwavenonzeroevaluationdeterminanti. mdr_gap_secondwavenonzeroevaluationdeterminanti + S (mdr_i_secondwavenonzeroevaluationdeterminant) = (mdr_l_secondwavenonzeroevaluationdeterminant)) /\ (exists mdr_z_secondwavenonzeroevaluationdeterminantr. ((exists mdr_a_secondwavenonzeroevaluationdeterminantrc mdr_b_secondwavenonzeroevaluationdeterminantrc mdr_c_secondwavenonzeroevaluationdeterminantrc mdr_e_secondwavenonzeroevaluationdeterminantrc mdr_f_secondwavenonzeroevaluationdeterminantrc. ((mdr_a_secondwavenonzeroevaluationdeterminantrc = ((q) + (mdr_ub_secondwavenonzeroevaluation)) * S ((q) + (mdr_ub_secondwavenonzeroevaluation)) + ((mdr_ub_secondwavenonzeroevaluation) + (mdr_ub_secondwavenonzeroevaluation))) /\ ((mdr_b_secondwavenonzeroevaluationdeterminantrc = ((mdr_uc_secondwavenonzeroevaluation) + (mdr_vb_secondwavenonzeroevaluation)) * S ((mdr_uc_secondwavenonzeroevaluation) + (mdr_vb_secondwavenonzeroevaluation)) + ((mdr_vb_secondwavenonzeroevaluation) + (mdr_vb_secondwavenonzeroevaluation))) /\ ((mdr_c_secondwavenonzeroevaluationdeterminantrc = ((mdr_a_secondwavenonzeroevaluationdeterminantrc) + (mdr_b_secondwavenonzeroevaluationdeterminantrc)) * S ((mdr_a_secondwavenonzeroevaluationdeterminantrc) + (mdr_b_secondwavenonzeroevaluationdeterminantrc)) + ((mdr_b_secondwavenonzeroevaluationdeterminantrc) + (mdr_b_secondwavenonzeroevaluationdeterminantrc))) /\ ((mdr_e_secondwavenonzeroevaluationdeterminantrc = ((mdr_p_secondwavenonzero) + (mdr_n_secondwavenonzero)) * S ((mdr_p_secondwavenonzero) + (mdr_n_secondwavenonzero)) + ((mdr_n_secondwavenonzero) + (mdr_n_secondwavenonzero))) /\ ((mdr_f_secondwavenonzeroevaluationdeterminantrc = ((mdr_vc_secondwavenonzeroevaluation) + (mdr_e_secondwavenonzeroevaluationdeterminantrc)) * S ((mdr_vc_secondwavenonzeroevaluation) + (mdr_e_secondwavenonzeroevaluationdeterminantrc)) + ((mdr_e_secondwavenonzeroevaluationdeterminantrc) + (mdr_e_secondwavenonzeroevaluationdeterminantrc))) /\ ((mdr_z_secondwavenonzeroevaluationdeterminantr) = ((mdr_c_secondwavenonzeroevaluationdeterminantrc) + (mdr_f_secondwavenonzeroevaluationdeterminantrc)) * S ((mdr_c_secondwavenonzeroevaluationdeterminantrc) + (mdr_f_secondwavenonzeroevaluationdeterminantrc)) + ((mdr_f_secondwavenonzeroevaluationdeterminantrc) + (mdr_f_secondwavenonzeroevaluationdeterminantrc))))))))) /\ (((exists ff_h_mdr_secondwavenonzeroevaluationdeterminantrb. ff_h_mdr_secondwavenonzeroevaluationdeterminantrb + S (mdr_z_secondwavenonzeroevaluationdeterminantr) = S ((S (mdr_i_secondwavenonzeroevaluationdeterminant)) * mdr_c_secondwavenonzeroevaluationdeterminant)) /\ exists ff_q_mdr_secondwavenonzeroevaluationdeterminantrb. mdr_b_secondwavenonzeroevaluationdeterminant = ff_q_mdr_secondwavenonzeroevaluationdeterminantrb * S ((S (mdr_i_secondwavenonzeroevaluationdeterminant)) * mdr_c_secondwavenonzeroevaluationdeterminant) + (mdr_z_secondwavenonzeroevaluationdeterminantr)))))))))) /\ (~(mdr_p_secondwavenonzero = mdr_n_secondwavenonzero))))))

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