Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.
Definition in prerequisite notation
Le(rank,r) ∧ (Le(rank,w) ∧ (NonzeroMatrixMinor(pb,pc,nb,nc,r,w,rank) ∧ (∀ x. Lt(rank,x) → AllSignedMinorsZero(pb,pc,nb,nc,r,w,x))))Only definitions earlier in this acyclic notation graph are used here.
Hygienic expanded first-order definition
((exists mdr_gap_secondwaverows_bound. mdr_gap_secondwaverows_bound + (rank) = (r)) /\ ((exists mdr_gap_secondwavecolumns_bound. mdr_gap_secondwavecolumns_bound + (rank) = (w)) /\ ((exists mdr_rb_secondwavewitness mdr_rc_secondwavewitness mdr_cb_secondwavewitness mdr_cc_secondwavewitness. (((((forall fom_index_mrf_secondwavewitnessminorrowsbound. (exists fom_gap_mrf_secondwavewitnessminorrowsbound_index_bound. fom_gap_mrf_secondwavewitnessminorrowsbound_index_bound + S (fom_index_mrf_secondwavewitnessminorrowsbound) = rank) -> exists fom_value_mrf_secondwavewitnessminorrowsbound. ((((exists fom_beta_height_mrf_secondwavewitnessminorrowsbound_entry. fom_beta_height_mrf_secondwavewitnessminorrowsbound_entry + S (fom_value_mrf_secondwavewitnessminorrowsbound) = S ((S (fom_index_mrf_secondwavewitnessminorrowsbound)) * mdr_rc_secondwavewitness)) /\ exists fom_beta_quotient_mrf_secondwavewitnessminorrowsbound_entry. mdr_rb_secondwavewitness = fom_beta_quotient_mrf_secondwavewitnessminorrowsbound_entry * S ((S (fom_index_mrf_secondwavewitnessminorrowsbound)) * mdr_rc_secondwavewitness) + (fom_value_mrf_secondwavewitnessminorrowsbound))) /\ (exists fom_gap_mrf_secondwavewitnessminorrowsbound_value_bound. fom_gap_mrf_secondwavewitnessminorrowsbound_value_bound + S (fom_value_mrf_secondwavewitnessminorrowsbound) = r))) /\ (forall mdr_i_secondwavewitnessminorrowsdistinct mdr_j_secondwavewitnessminorrowsdistinct mdr_a_secondwavewitnessminorrowsdistinct. (exists mdr_gap_secondwavewitnessminorrowsdistincti. mdr_gap_secondwavewitnessminorrowsdistincti + S (mdr_i_secondwavewitnessminorrowsdistinct) = (rank)) -> (exists mdr_gap_secondwavewitnessminorrowsdistinctj. mdr_gap_secondwavewitnessminorrowsdistinctj + S (mdr_j_secondwavewitnessminorrowsdistinct) = (rank)) -> (((exists ff_h_mdr_secondwavewitnessminorrowsdistinctfirst. ff_h_mdr_secondwavewitnessminorrowsdistinctfirst + S (mdr_a_secondwavewitnessminorrowsdistinct) = S ((S (mdr_i_secondwavewitnessminorrowsdistinct)) * mdr_rc_secondwavewitness)) /\ exists ff_q_mdr_secondwavewitnessminorrowsdistinctfirst. mdr_rb_secondwavewitness = ff_q_mdr_secondwavewitnessminorrowsdistinctfirst * S ((S (mdr_i_secondwavewitnessminorrowsdistinct)) * mdr_rc_secondwavewitness) + (mdr_a_secondwavewitnessminorrowsdistinct))) -> (((exists ff_h_mdr_secondwavewitnessminorrowsdistinctsecond. ff_h_mdr_secondwavewitnessminorrowsdistinctsecond + S (mdr_a_secondwavewitnessminorrowsdistinct) = S ((S (mdr_j_secondwavewitnessminorrowsdistinct)) * mdr_rc_secondwavewitness)) /\ exists ff_q_mdr_secondwavewitnessminorrowsdistinctsecond. mdr_rb_secondwavewitness = ff_q_mdr_secondwavewitnessminorrowsdistinctsecond * S ((S (mdr_j_secondwavewitnessminorrowsdistinct)) * mdr_rc_secondwavewitness) + (mdr_a_secondwavewitnessminorrowsdistinct))) -> mdr_i_secondwavewitnessminorrowsdistinct = mdr_j_secondwavewitnessminorrowsdistinct))) /\ ((((forall fom_index_mrf_secondwavewitnessminorcolumnsbound. (exists fom_gap_mrf_secondwavewitnessminorcolumnsbound_index_bound. fom_gap_mrf_secondwavewitnessminorcolumnsbound_index_bound + S (fom_index_mrf_secondwavewitnessminorcolumnsbound) = rank) -> exists fom_value_mrf_secondwavewitnessminorcolumnsbound. ((((exists fom_beta_height_mrf_secondwavewitnessminorcolumnsbound_entry. fom_beta_height_mrf_secondwavewitnessminorcolumnsbound_entry + S (fom_value_mrf_secondwavewitnessminorcolumnsbound) = S ((S (fom_index_mrf_secondwavewitnessminorcolumnsbound)) * mdr_cc_secondwavewitness)) /\ exists fom_beta_quotient_mrf_secondwavewitnessminorcolumnsbound_entry. mdr_cb_secondwavewitness = fom_beta_quotient_mrf_secondwavewitnessminorcolumnsbound_entry * S ((S (fom_index_mrf_secondwavewitnessminorcolumnsbound)) * mdr_cc_secondwavewitness) + (fom_value_mrf_secondwavewitnessminorcolumnsbound))) /\ (exists fom_gap_mrf_secondwavewitnessminorcolumnsbound_value_bound. fom_gap_mrf_secondwavewitnessminorcolumnsbound_value_bound + S (fom_value_mrf_secondwavewitnessminorcolumnsbound) = w))) /\ (forall mdr_i_secondwavewitnessminorcolumnsdistinct mdr_j_secondwavewitnessminorcolumnsdistinct mdr_a_secondwavewitnessminorcolumnsdistinct. (exists mdr_gap_secondwavewitnessminorcolumnsdistincti. mdr_gap_secondwavewitnessminorcolumnsdistincti + S (mdr_i_secondwavewitnessminorcolumnsdistinct) = (rank)) -> (exists mdr_gap_secondwavewitnessminorcolumnsdistinctj. mdr_gap_secondwavewitnessminorcolumnsdistinctj + S (mdr_j_secondwavewitnessminorcolumnsdistinct) = (rank)) -> (((exists ff_h_mdr_secondwavewitnessminorcolumnsdistinctfirst. ff_h_mdr_secondwavewitnessminorcolumnsdistinctfirst + S (mdr_a_secondwavewitnessminorcolumnsdistinct) = S ((S (mdr_i_secondwavewitnessminorcolumnsdistinct)) * mdr_cc_secondwavewitness)) /\ exists ff_q_mdr_secondwavewitnessminorcolumnsdistinctfirst. mdr_cb_secondwavewitness = ff_q_mdr_secondwavewitnessminorcolumnsdistinctfirst * S ((S (mdr_i_secondwavewitnessminorcolumnsdistinct)) * mdr_cc_secondwavewitness) + (mdr_a_secondwavewitnessminorcolumnsdistinct))) -> (((exists ff_h_mdr_secondwavewitnessminorcolumnsdistinctsecond. ff_h_mdr_secondwavewitnessminorcolumnsdistinctsecond + S (mdr_a_secondwavewitnessminorcolumnsdistinct) = S ((S (mdr_j_secondwavewitnessminorcolumnsdistinct)) * mdr_cc_secondwavewitness)) /\ exists ff_q_mdr_secondwavewitnessminorcolumnsdistinctsecond. mdr_cb_secondwavewitness = ff_q_mdr_secondwavewitnessminorcolumnsdistinctsecond * S ((S (mdr_j_secondwavewitnessminorcolumnsdistinct)) * mdr_cc_secondwavewitness) + (mdr_a_secondwavewitnessminorcolumnsdistinct))) -> mdr_i_secondwavewitnessminorcolumnsdistinct = mdr_j_secondwavewitnessminorcolumnsdistinct))) /\ (exists mdr_p_secondwavewitnessminornonzero mdr_n_secondwavewitnessminornonzero. ((exists mdr_ub_secondwavewitnessminornonzeroevaluation mdr_uc_secondwavewitnessminornonzeroevaluation mdr_vb_secondwavewitnessminornonzeroevaluation mdr_vc_secondwavewitnessminornonzeroevaluation. ((((forall mdr_i_secondwavewitnessminornonzeroevaluationmatrixpositive. (exists mdr_gap_secondwavewitnessminornonzeroevaluationmatrixpositivebound. mdr_gap_secondwavewitnessminornonzeroevaluationmatrixpositivebound + S (mdr_i_secondwavewitnessminornonzeroevaluationmatrixpositive) = ((rank) * (rank))) -> exists mdr_a_secondwavewitnessminornonzeroevaluationmatrixpositive. (((exists mdr_r_secondwavewitnessminornonzeroevaluationmatrixpositivepoint mdr_s_secondwavewitnessminornonzeroevaluationmatrixpositivepoint mdr_u_secondwavewitnessminornonzeroevaluationmatrixpositivepoint mdr_v_secondwavewitnessminornonzeroevaluationmatrixpositivepoint. ((mdr_i_secondwavewitnessminornonzeroevaluationmatrixpositive = (rank) * mdr_r_secondwavewitnessminornonzeroevaluationmatrixpositivepoint + mdr_s_secondwavewitnessminornonzeroevaluationmatrixpositivepoint) /\ ((exists mdr_gap_secondwavewitnessminornonzeroevaluationmatrixpositivepointcolumn. mdr_gap_secondwavewitnessminornonzeroevaluationmatrixpositivepointcolumn + S (mdr_s_secondwavewitnessminornonzeroevaluationmatrixpositivepoint) = (rank)) /\ ((((exists ff_h_mdr_secondwavewitnessminornonzeroevaluationmatrixpositivepointrow_index. ff_h_mdr_secondwavewitnessminornonzeroevaluationmatrixpositivepointrow_index + S (mdr_u_secondwavewitnessminornonzeroevaluationmatrixpositivepoint) = S ((S (mdr_r_secondwavewitnessminornonzeroevaluationmatrixpositivepoint)) * mdr_rc_secondwavewitness)) /\ exists ff_q_mdr_secondwavewitnessminornonzeroevaluationmatrixpositivepointrow_index. mdr_rb_secondwavewitness = ff_q_mdr_secondwavewitnessminornonzeroevaluationmatrixpositivepointrow_index * S ((S (mdr_r_secondwavewitnessminornonzeroevaluationmatrixpositivepoint)) * mdr_rc_secondwavewitness) + (mdr_u_secondwavewitnessminornonzeroevaluationmatrixpositivepoint))) /\ ((((exists ff_h_mdr_secondwavewitnessminornonzeroevaluationmatrixpositivepointcolumn_index. ff_h_mdr_secondwavewitnessminornonzeroevaluationmatrixpositivepointcolumn_index + S (mdr_v_secondwavewitnessminornonzeroevaluationmatrixpositivepoint) = S ((S (mdr_s_secondwavewitnessminornonzeroevaluationmatrixpositivepoint)) * mdr_cc_secondwavewitness)) /\ exists ff_q_mdr_secondwavewitnessminornonzeroevaluationmatrixpositivepointcolumn_index. mdr_cb_secondwavewitness = ff_q_mdr_secondwavewitnessminornonzeroevaluationmatrixpositivepointcolumn_index * S ((S (mdr_s_secondwavewitnessminornonzeroevaluationmatrixpositivepoint)) * mdr_cc_secondwavewitness) + (mdr_v_secondwavewitnessminornonzeroevaluationmatrixpositivepoint))) /\ (((exists ff_h_mdr_secondwavewitnessminornonzeroevaluationmatrixpositivepointsource. ff_h_mdr_secondwavewitnessminornonzeroevaluationmatrixpositivepointsource + S (mdr_a_secondwavewitnessminornonzeroevaluationmatrixpositive) = S ((S ((mdr_u_secondwavewitnessminornonzeroevaluationmatrixpositivepoint) * (w) + (mdr_v_secondwavewitnessminornonzeroevaluationmatrixpositivepoint))) * pc)) /\ exists ff_q_mdr_secondwavewitnessminornonzeroevaluationmatrixpositivepointsource. pb = ff_q_mdr_secondwavewitnessminornonzeroevaluationmatrixpositivepointsource * S ((S ((mdr_u_secondwavewitnessminornonzeroevaluationmatrixpositivepoint) * (w) + (mdr_v_secondwavewitnessminornonzeroevaluationmatrixpositivepoint))) * pc) + (mdr_a_secondwavewitnessminornonzeroevaluationmatrixpositive)))))))) /\ (((exists ff_h_mdr_secondwavewitnessminornonzeroevaluationmatrixpositiveoutput. ff_h_mdr_secondwavewitnessminornonzeroevaluationmatrixpositiveoutput + S (mdr_a_secondwavewitnessminornonzeroevaluationmatrixpositive) = S ((S (mdr_i_secondwavewitnessminornonzeroevaluationmatrixpositive)) * mdr_uc_secondwavewitnessminornonzeroevaluation)) /\ exists ff_q_mdr_secondwavewitnessminornonzeroevaluationmatrixpositiveoutput. mdr_ub_secondwavewitnessminornonzeroevaluation = ff_q_mdr_secondwavewitnessminornonzeroevaluationmatrixpositiveoutput * S ((S (mdr_i_secondwavewitnessminornonzeroevaluationmatrixpositive)) * mdr_uc_secondwavewitnessminornonzeroevaluation) + (mdr_a_secondwavewitnessminornonzeroevaluationmatrixpositive)))))) /\ (forall mdr_i_secondwavewitnessminornonzeroevaluationmatrixnegative. (exists mdr_gap_secondwavewitnessminornonzeroevaluationmatrixnegativebound. mdr_gap_secondwavewitnessminornonzeroevaluationmatrixnegativebound + S (mdr_i_secondwavewitnessminornonzeroevaluationmatrixnegative) = ((rank) * (rank))) -> exists mdr_a_secondwavewitnessminornonzeroevaluationmatrixnegative. (((exists mdr_r_secondwavewitnessminornonzeroevaluationmatrixnegativepoint mdr_s_secondwavewitnessminornonzeroevaluationmatrixnegativepoint mdr_u_secondwavewitnessminornonzeroevaluationmatrixnegativepoint mdr_v_secondwavewitnessminornonzeroevaluationmatrixnegativepoint. ((mdr_i_secondwavewitnessminornonzeroevaluationmatrixnegative = (rank) * mdr_r_secondwavewitnessminornonzeroevaluationmatrixnegativepoint + mdr_s_secondwavewitnessminornonzeroevaluationmatrixnegativepoint) /\ ((exists mdr_gap_secondwavewitnessminornonzeroevaluationmatrixnegativepointcolumn. mdr_gap_secondwavewitnessminornonzeroevaluationmatrixnegativepointcolumn + S (mdr_s_secondwavewitnessminornonzeroevaluationmatrixnegativepoint) = (rank)) /\ ((((exists ff_h_mdr_secondwavewitnessminornonzeroevaluationmatrixnegativepointrow_index. ff_h_mdr_secondwavewitnessminornonzeroevaluationmatrixnegativepointrow_index + S (mdr_u_secondwavewitnessminornonzeroevaluationmatrixnegativepoint) = S ((S (mdr_r_secondwavewitnessminornonzeroevaluationmatrixnegativepoint)) * mdr_rc_secondwavewitness)) /\ exists ff_q_mdr_secondwavewitnessminornonzeroevaluationmatrixnegativepointrow_index. mdr_rb_secondwavewitness = ff_q_mdr_secondwavewitnessminornonzeroevaluationmatrixnegativepointrow_index * S ((S (mdr_r_secondwavewitnessminornonzeroevaluationmatrixnegativepoint)) * mdr_rc_secondwavewitness) + (mdr_u_secondwavewitnessminornonzeroevaluationmatrixnegativepoint))) /\ ((((exists ff_h_mdr_secondwavewitnessminornonzeroevaluationmatrixnegativepointcolumn_index. ff_h_mdr_secondwavewitnessminornonzeroevaluationmatrixnegativepointcolumn_index + S (mdr_v_secondwavewitnessminornonzeroevaluationmatrixnegativepoint) = S ((S (mdr_s_secondwavewitnessminornonzeroevaluationmatrixnegativepoint)) * mdr_cc_secondwavewitness)) /\ exists ff_q_mdr_secondwavewitnessminornonzeroevaluationmatrixnegativepointcolumn_index. mdr_cb_secondwavewitness = ff_q_mdr_secondwavewitnessminornonzeroevaluationmatrixnegativepointcolumn_index * S ((S (mdr_s_secondwavewitnessminornonzeroevaluationmatrixnegativepoint)) * mdr_cc_secondwavewitness) + (mdr_v_secondwavewitnessminornonzeroevaluationmatrixnegativepoint))) /\ (((exists ff_h_mdr_secondwavewitnessminornonzeroevaluationmatrixnegativepointsource. ff_h_mdr_secondwavewitnessminornonzeroevaluationmatrixnegativepointsource + S (mdr_a_secondwavewitnessminornonzeroevaluationmatrixnegative) = S ((S ((mdr_u_secondwavewitnessminornonzeroevaluationmatrixnegativepoint) * (w) + (mdr_v_secondwavewitnessminornonzeroevaluationmatrixnegativepoint))) * nc)) /\ exists ff_q_mdr_secondwavewitnessminornonzeroevaluationmatrixnegativepointsource. nb = ff_q_mdr_secondwavewitnessminornonzeroevaluationmatrixnegativepointsource * S ((S ((mdr_u_secondwavewitnessminornonzeroevaluationmatrixnegativepoint) * (w) + (mdr_v_secondwavewitnessminornonzeroevaluationmatrixnegativepoint))) * nc) + (mdr_a_secondwavewitnessminornonzeroevaluationmatrixnegative)))))))) /\ (((exists ff_h_mdr_secondwavewitnessminornonzeroevaluationmatrixnegativeoutput. ff_h_mdr_secondwavewitnessminornonzeroevaluationmatrixnegativeoutput + S (mdr_a_secondwavewitnessminornonzeroevaluationmatrixnegative) = S ((S (mdr_i_secondwavewitnessminornonzeroevaluationmatrixnegative)) * mdr_vc_secondwavewitnessminornonzeroevaluation)) /\ exists ff_q_mdr_secondwavewitnessminornonzeroevaluationmatrixnegativeoutput. mdr_vb_secondwavewitnessminornonzeroevaluation = ff_q_mdr_secondwavewitnessminornonzeroevaluationmatrixnegativeoutput * S ((S (mdr_i_secondwavewitnessminornonzeroevaluationmatrixnegative)) * mdr_vc_secondwavewitnessminornonzeroevaluation) + (mdr_a_secondwavewitnessminornonzeroevaluationmatrixnegative)))))))) /\ (exists mdr_b_secondwavewitnessminornonzeroevaluationdeterminant mdr_c_secondwavewitnessminornonzeroevaluationdeterminant mdr_l_secondwavewitnessminornonzeroevaluationdeterminant mdr_i_secondwavewitnessminornonzeroevaluationdeterminant. ((forall mdr_i_secondwavewitnessminornonzeroevaluationdeterminanth. (exists mdr_gap_secondwavewitnessminornonzeroevaluationdeterminanthi. mdr_gap_secondwavewitnessminornonzeroevaluationdeterminanthi + S (mdr_i_secondwavewitnessminornonzeroevaluationdeterminanth) = (mdr_l_secondwavewitnessminornonzeroevaluationdeterminant)) -> exists mdr_d_secondwavewitnessminornonzeroevaluationdeterminanth mdr_pb_secondwavewitnessminornonzeroevaluationdeterminanth mdr_pc_secondwavewitnessminornonzeroevaluationdeterminanth mdr_nb_secondwavewitnessminornonzeroevaluationdeterminanth mdr_nc_secondwavewitnessminornonzeroevaluationdeterminanth mdr_p_secondwavewitnessminornonzeroevaluationdeterminanth mdr_n_secondwavewitnessminornonzeroevaluationdeterminanth. ((exists mdr_z_secondwavewitnessminornonzeroevaluationdeterminanthr. ((exists mdr_a_secondwavewitnessminornonzeroevaluationdeterminanthrc mdr_b_secondwavewitnessminornonzeroevaluationdeterminanthrc mdr_c_secondwavewitnessminornonzeroevaluationdeterminanthrc mdr_e_secondwavewitnessminornonzeroevaluationdeterminanthrc mdr_f_secondwavewitnessminornonzeroevaluationdeterminanthrc. ((mdr_a_secondwavewitnessminornonzeroevaluationdeterminanthrc = ((mdr_d_secondwavewitnessminornonzeroevaluationdeterminanth) + (mdr_pb_secondwavewitnessminornonzeroevaluationdeterminanth)) * S ((mdr_d_secondwavewitnessminornonzeroevaluationdeterminanth) + (mdr_pb_secondwavewitnessminornonzeroevaluationdeterminanth)) + ((mdr_pb_secondwavewitnessminornonzeroevaluationdeterminanth) + (mdr_pb_secondwavewitnessminornonzeroevaluationdeterminanth))) /\ ((mdr_b_secondwavewitnessminornonzeroevaluationdeterminanthrc = ((mdr_pc_secondwavewitnessminornonzeroevaluationdeterminanth) + (mdr_nb_secondwavewitnessminornonzeroevaluationdeterminanth)) * S ((mdr_pc_secondwavewitnessminornonzeroevaluationdeterminanth) + (mdr_nb_secondwavewitnessminornonzeroevaluationdeterminanth)) + ((mdr_nb_secondwavewitnessminornonzeroevaluationdeterminanth) + (mdr_nb_secondwavewitnessminornonzeroevaluationdeterminanth))) /\ ((mdr_c_secondwavewitnessminornonzeroevaluationdeterminanthrc = ((mdr_a_secondwavewitnessminornonzeroevaluationdeterminanthrc) + (mdr_b_secondwavewitnessminornonzeroevaluationdeterminanthrc)) * S ((mdr_a_secondwavewitnessminornonzeroevaluationdeterminanthrc) + (mdr_b_secondwavewitnessminornonzeroevaluationdeterminanthrc)) + ((mdr_b_secondwavewitnessminornonzeroevaluationdeterminanthrc) + (mdr_b_secondwavewitnessminornonzeroevaluationdeterminanthrc))) /\ ((mdr_e_secondwavewitnessminornonzeroevaluationdeterminanthrc = ((mdr_p_secondwavewitnessminornonzeroevaluationdeterminanth) + (mdr_n_secondwavewitnessminornonzeroevaluationdeterminanth)) * S ((mdr_p_secondwavewitnessminornonzeroevaluationdeterminanth) + (mdr_n_secondwavewitnessminornonzeroevaluationdeterminanth)) + ((mdr_n_secondwavewitnessminornonzeroevaluationdeterminanth) + (mdr_n_secondwavewitnessminornonzeroevaluationdeterminanth))) /\ ((mdr_f_secondwavewitnessminornonzeroevaluationdeterminanthrc = ((mdr_nc_secondwavewitnessminornonzeroevaluationdeterminanth) + (mdr_e_secondwavewitnessminornonzeroevaluationdeterminanthrc)) * S ((mdr_nc_secondwavewitnessminornonzeroevaluationdeterminanth) + (mdr_e_secondwavewitnessminornonzeroevaluationdeterminanthrc)) + ((mdr_e_secondwavewitnessminornonzeroevaluationdeterminanthrc) + (mdr_e_secondwavewitnessminornonzeroevaluationdeterminanthrc))) /\ ((mdr_z_secondwavewitnessminornonzeroevaluationdeterminanthr) = ((mdr_c_secondwavewitnessminornonzeroevaluationdeterminanthrc) + (mdr_f_secondwavewitnessminornonzeroevaluationdeterminanthrc)) * S ((mdr_c_secondwavewitnessminornonzeroevaluationdeterminanthrc) + (mdr_f_secondwavewitnessminornonzeroevaluationdeterminanthrc)) + ((mdr_f_secondwavewitnessminornonzeroevaluationdeterminanthrc) + (mdr_f_secondwavewitnessminornonzeroevaluationdeterminanthrc))))))))) /\ (((exists ff_h_mdr_secondwavewitnessminornonzeroevaluationdeterminanthrb. ff_h_mdr_secondwavewitnessminornonzeroevaluationdeterminanthrb + S (mdr_z_secondwavewitnessminornonzeroevaluationdeterminanthr) = S ((S (mdr_i_secondwavewitnessminornonzeroevaluationdeterminanth)) * mdr_c_secondwavewitnessminornonzeroevaluationdeterminant)) /\ exists ff_q_mdr_secondwavewitnessminornonzeroevaluationdeterminanthrb. mdr_b_secondwavewitnessminornonzeroevaluationdeterminant = ff_q_mdr_secondwavewitnessminornonzeroevaluationdeterminanthrb * S ((S (mdr_i_secondwavewitnessminornonzeroevaluationdeterminanth)) * mdr_c_secondwavewitnessminornonzeroevaluationdeterminant) + (mdr_z_secondwavewitnessminornonzeroevaluationdeterminanthr))))) /\ (((((mdr_d_secondwavewitnessminornonzeroevaluationdeterminanth) = 0) /\ (((mdr_p_secondwavewitnessminornonzeroevaluationdeterminanth) = 1) /\ ((mdr_n_secondwavewitnessminornonzeroevaluationdeterminanth) = 0))) \/ exists mdr_q_secondwavewitnessminornonzeroevaluationdeterminanths mdr_eb_secondwavewitnessminornonzeroevaluationdeterminanths mdr_ec_secondwavewitnessminornonzeroevaluationdeterminanths mdr_fb_secondwavewitnessminornonzeroevaluationdeterminanths mdr_fc_secondwavewitnessminornonzeroevaluationdeterminanths. (((mdr_d_secondwavewitnessminornonzeroevaluationdeterminanth) = S (mdr_q_secondwavewitnessminornonzeroevaluationdeterminanths)) /\ ((forall mdr_j_secondwavewitnessminornonzeroevaluationdeterminanthsc. (exists mdr_gap_secondwavewitnessminornonzeroevaluationdeterminanthscj. mdr_gap_secondwavewitnessminornonzeroevaluationdeterminanthscj + S (mdr_j_secondwavewitnessminornonzeroevaluationdeterminanthsc) = (S (mdr_q_secondwavewitnessminornonzeroevaluationdeterminanths))) -> exists mdr_i_secondwavewitnessminornonzeroevaluationdeterminanthsc mdr_up_secondwavewitnessminornonzeroevaluationdeterminanthsc mdr_us_secondwavewitnessminornonzeroevaluationdeterminanthsc mdr_un_secondwavewitnessminornonzeroevaluationdeterminanthsc mdr_ut_secondwavewitnessminornonzeroevaluationdeterminanthsc mdr_p_secondwavewitnessminornonzeroevaluationdeterminanthsc mdr_n_secondwavewitnessminornonzeroevaluationdeterminanthsc. ((exists mdr_gap_secondwavewitnessminornonzeroevaluationdeterminanthsci. mdr_gap_secondwavewitnessminornonzeroevaluationdeterminanthsci + S (mdr_i_secondwavewitnessminornonzeroevaluationdeterminanthsc) = (mdr_i_secondwavewitnessminornonzeroevaluationdeterminanth)) /\ ((exists mdr_z_secondwavewitnessminornonzeroevaluationdeterminanthscr. ((exists mdr_a_secondwavewitnessminornonzeroevaluationdeterminanthscrc mdr_b_secondwavewitnessminornonzeroevaluationdeterminanthscrc mdr_c_secondwavewitnessminornonzeroevaluationdeterminanthscrc mdr_e_secondwavewitnessminornonzeroevaluationdeterminanthscrc mdr_f_secondwavewitnessminornonzeroevaluationdeterminanthscrc. ((mdr_a_secondwavewitnessminornonzeroevaluationdeterminanthscrc = ((mdr_q_secondwavewitnessminornonzeroevaluationdeterminanths) + (mdr_up_secondwavewitnessminornonzeroevaluationdeterminanthsc)) * S ((mdr_q_secondwavewitnessminornonzeroevaluationdeterminanths) + (mdr_up_secondwavewitnessminornonzeroevaluationdeterminanthsc)) + ((mdr_up_secondwavewitnessminornonzeroevaluationdeterminanthsc) + (mdr_up_secondwavewitnessminornonzeroevaluationdeterminanthsc))) /\ ((mdr_b_secondwavewitnessminornonzeroevaluationdeterminanthscrc = ((mdr_us_secondwavewitnessminornonzeroevaluationdeterminanthsc) + (mdr_un_secondwavewitnessminornonzeroevaluationdeterminanthsc)) * S ((mdr_us_secondwavewitnessminornonzeroevaluationdeterminanthsc) + (mdr_un_secondwavewitnessminornonzeroevaluationdeterminanthsc)) + ((mdr_un_secondwavewitnessminornonzeroevaluationdeterminanthsc) + (mdr_un_secondwavewitnessminornonzeroevaluationdeterminanthsc))) /\ ((mdr_c_secondwavewitnessminornonzeroevaluationdeterminanthscrc = ((mdr_a_secondwavewitnessminornonzeroevaluationdeterminanthscrc) + (mdr_b_secondwavewitnessminornonzeroevaluationdeterminanthscrc)) * S ((mdr_a_secondwavewitnessminornonzeroevaluationdeterminanthscrc) + (mdr_b_secondwavewitnessminornonzeroevaluationdeterminanthscrc)) + ((mdr_b_secondwavewitnessminornonzeroevaluationdeterminanthscrc) + (mdr_b_secondwavewitnessminornonzeroevaluationdeterminanthscrc))) /\ ((mdr_e_secondwavewitnessminornonzeroevaluationdeterminanthscrc = ((mdr_p_secondwavewitnessminornonzeroevaluationdeterminanthsc) + (mdr_n_secondwavewitnessminornonzeroevaluationdeterminanthsc)) * S ((mdr_p_secondwavewitnessminornonzeroevaluationdeterminanthsc) + (mdr_n_secondwavewitnessminornonzeroevaluationdeterminanthsc)) + ((mdr_n_secondwavewitnessminornonzeroevaluationdeterminanthsc) + (mdr_n_secondwavewitnessminornonzeroevaluationdeterminanthsc))) /\ ((mdr_f_secondwavewitnessminornonzeroevaluationdeterminanthscrc = ((mdr_ut_secondwavewitnessminornonzeroevaluationdeterminanthsc) + (mdr_e_secondwavewitnessminornonzeroevaluationdeterminanthscrc)) * S ((mdr_ut_secondwavewitnessminornonzeroevaluationdeterminanthsc) + (mdr_e_secondwavewitnessminornonzeroevaluationdeterminanthscrc)) + ((mdr_e_secondwavewitnessminornonzeroevaluationdeterminanthscrc) + (mdr_e_secondwavewitnessminornonzeroevaluationdeterminanthscrc))) /\ ((mdr_z_secondwavewitnessminornonzeroevaluationdeterminanthscr) = ((mdr_c_secondwavewitnessminornonzeroevaluationdeterminanthscrc) + (mdr_f_secondwavewitnessminornonzeroevaluationdeterminanthscrc)) * S ((mdr_c_secondwavewitnessminornonzeroevaluationdeterminanthscrc) + (mdr_f_secondwavewitnessminornonzeroevaluationdeterminanthscrc)) + ((mdr_f_secondwavewitnessminornonzeroevaluationdeterminanthscrc) + (mdr_f_secondwavewitnessminornonzeroevaluationdeterminanthscrc))))))))) /\ (((exists ff_h_mdr_secondwavewitnessminornonzeroevaluationdeterminanthscrb. ff_h_mdr_secondwavewitnessminornonzeroevaluationdeterminanthscrb + S (mdr_z_secondwavewitnessminornonzeroevaluationdeterminanthscr) = S ((S (mdr_i_secondwavewitnessminornonzeroevaluationdeterminanthsc)) * mdr_c_secondwavewitnessminornonzeroevaluationdeterminant)) /\ exists ff_q_mdr_secondwavewitnessminornonzeroevaluationdeterminanthscrb. mdr_b_secondwavewitnessminornonzeroevaluationdeterminant = ff_q_mdr_secondwavewitnessminornonzeroevaluationdeterminanthscrb * S ((S (mdr_i_secondwavewitnessminornonzeroevaluationdeterminanthsc)) * mdr_c_secondwavewitnessminornonzeroevaluationdeterminant) + (mdr_z_secondwavewitnessminornonzeroevaluationdeterminanthscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_secondwavewitnessminornonzeroevaluationdeterminanthscm_positive. (exists ff_gap_mdm_lt_mdr_secondwavewitnessminornonzeroevaluationdeterminanthscm_positive_index_bound. ff_gap_mdm_lt_mdr_secondwavewitnessminornonzeroevaluationdeterminanthscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_secondwavewitnessminornonzeroevaluationdeterminanthscm_positive) = ((mdr_q_secondwavewitnessminornonzeroevaluationdeterminanths) * (mdr_q_secondwavewitnessminornonzeroevaluationdeterminanths))) -> exists ff_row_mdm_prefix_mdr_secondwavewitnessminornonzeroevaluationdeterminanthscm_positive ff_column_mdm_prefix_mdr_secondwavewitnessminornonzeroevaluationdeterminanthscm_positive ff_value_mdm_prefix_mdr_secondwavewitnessminornonzeroevaluationdeterminanthscm_positive. (ff_index_mdm_prefix_mdr_secondwavewitnessminornonzeroevaluationdeterminanthscm_positive = (mdr_q_secondwavewitnessminornonzeroevaluationdeterminanths) * ff_row_mdm_prefix_mdr_secondwavewitnessminornonzeroevaluationdeterminanthscm_positive + ff_column_mdm_prefix_mdr_secondwavewitnessminornonzeroevaluationdeterminanthscm_positive /\ ((exists ff_gap_mdm_lt_mdr_secondwavewitnessminornonzeroevaluationdeterminanthscm_positive_column_bound. ff_gap_mdm_lt_mdr_secondwavewitnessminornonzeroevaluationdeterminanthscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_secondwavewitnessminornonzeroevaluationdeterminanthscm_positive) = (mdr_q_secondwavewitnessminornonzeroevaluationdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_secondwavewitnessminornonzeroevaluationdeterminanthscm_positive_cell ff_column_mdm_cell_mdr_secondwavewitnessminornonzeroevaluationdeterminanthscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_secondwavewitnessminornonzeroevaluationdeterminanthscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_secondwavewitnessminornonzeroevaluationdeterminanthscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_secondwavewitnessminornonzeroevaluationdeterminanthscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_secondwavewitnessminornonzeroevaluationdeterminanthscm_positive_cell = ff_row_mdm_prefix_mdr_secondwavewitnessminornonzeroevaluationdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_secondwavewitnessminornonzeroevaluationdeterminanthscm_positive_cell_row_after. ff_gap_mdm_le_mdr_secondwavewitnessminornonzeroevaluationdeterminanthscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_secondwavewitnessminornonzeroevaluationdeterminanthscm_positive)) /\ ff_row_mdm_cell_mdr_secondwavewitnessminornonzeroevaluationdeterminanthscm_positive_cell = S ff_row_mdm_prefix_mdr_secondwavewitnessminornonzeroevaluationdeterminanthscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_secondwavewitnessminornonzeroevaluationdeterminanthscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_secondwavewitnessminornonzeroevaluationdeterminanthscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_secondwavewitnessminornonzeroevaluationdeterminanthscm_positive) = (mdr_j_secondwavewitnessminornonzeroevaluationdeterminanthsc)) /\ ff_column_mdm_cell_mdr_secondwavewitnessminornonzeroevaluationdeterminanthscm_positive_cell = ff_column_mdm_prefix_mdr_secondwavewitnessminornonzeroevaluationdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_secondwavewitnessminornonzeroevaluationdeterminanthscm_positive_cell_column_after. ff_gap_mdm_le_mdr_secondwavewitnessminornonzeroevaluationdeterminanthscm_positive_cell_column_after + (mdr_j_secondwavewitnessminornonzeroevaluationdeterminanthsc) = (ff_column_mdm_prefix_mdr_secondwavewitnessminornonzeroevaluationdeterminanthscm_positive)) /\ ff_column_mdm_cell_mdr_secondwavewitnessminornonzeroevaluationdeterminanthscm_positive_cell = S ff_column_mdm_prefix_mdr_secondwavewitnessminornonzeroevaluationdeterminanthscm_positive))) /\ (((exists ff_h_mdm_mdr_secondwavewitnessminornonzeroevaluationdeterminanthscm_positive_cell_source. ff_h_mdm_mdr_secondwavewitnessminornonzeroevaluationdeterminanthscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_secondwavewitnessminornonzeroevaluationdeterminanthscm_positive) = S ((S ((ff_row_mdm_cell_mdr_secondwavewitnessminornonzeroevaluationdeterminanthscm_positive_cell) * (S (mdr_q_secondwavewitnessminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_secondwavewitnessminornonzeroevaluationdeterminanthscm_positive_cell))) * mdr_pc_secondwavewitnessminornonzeroevaluationdeterminanth)) /\ exists ff_q_mdm_mdr_secondwavewitnessminornonzeroevaluationdeterminanthscm_positive_cell_source. mdr_pb_secondwavewitnessminornonzeroevaluationdeterminanth = ff_q_mdm_mdr_secondwavewitnessminornonzeroevaluationdeterminanthscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_secondwavewitnessminornonzeroevaluationdeterminanthscm_positive_cell) * (S (mdr_q_secondwavewitnessminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_secondwavewitnessminornonzeroevaluationdeterminanthscm_positive_cell))) * mdr_pc_secondwavewitnessminornonzeroevaluationdeterminanth) + (ff_value_mdm_prefix_mdr_secondwavewitnessminornonzeroevaluationdeterminanthscm_positive)))))) /\ (((exists ff_h_mdm_mdr_secondwavewitnessminornonzeroevaluationdeterminanthscm_positive_target. ff_h_mdm_mdr_secondwavewitnessminornonzeroevaluationdeterminanthscm_positive_target + S (ff_value_mdm_prefix_mdr_secondwavewitnessminornonzeroevaluationdeterminanthscm_positive) = S ((S (ff_index_mdm_prefix_mdr_secondwavewitnessminornonzeroevaluationdeterminanthscm_positive)) * mdr_us_secondwavewitnessminornonzeroevaluationdeterminanthsc)) /\ exists ff_q_mdm_mdr_secondwavewitnessminornonzeroevaluationdeterminanthscm_positive_target. mdr_up_secondwavewitnessminornonzeroevaluationdeterminanthsc = ff_q_mdm_mdr_secondwavewitnessminornonzeroevaluationdeterminanthscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_secondwavewitnessminornonzeroevaluationdeterminanthscm_positive)) * mdr_us_secondwavewitnessminornonzeroevaluationdeterminanthsc) + (ff_value_mdm_prefix_mdr_secondwavewitnessminornonzeroevaluationdeterminanthscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_secondwavewitnessminornonzeroevaluationdeterminanthscm_negative. (exists ff_gap_mdm_lt_mdr_secondwavewitnessminornonzeroevaluationdeterminanthscm_negative_index_bound. ff_gap_mdm_lt_mdr_secondwavewitnessminornonzeroevaluationdeterminanthscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_secondwavewitnessminornonzeroevaluationdeterminanthscm_negative) = ((mdr_q_secondwavewitnessminornonzeroevaluationdeterminanths) * (mdr_q_secondwavewitnessminornonzeroevaluationdeterminanths))) -> exists ff_row_mdm_prefix_mdr_secondwavewitnessminornonzeroevaluationdeterminanthscm_negative ff_column_mdm_prefix_mdr_secondwavewitnessminornonzeroevaluationdeterminanthscm_negative ff_value_mdm_prefix_mdr_secondwavewitnessminornonzeroevaluationdeterminanthscm_negative. (ff_index_mdm_prefix_mdr_secondwavewitnessminornonzeroevaluationdeterminanthscm_negative = (mdr_q_secondwavewitnessminornonzeroevaluationdeterminanths) * ff_row_mdm_prefix_mdr_secondwavewitnessminornonzeroevaluationdeterminanthscm_negative + ff_column_mdm_prefix_mdr_secondwavewitnessminornonzeroevaluationdeterminanthscm_negative /\ ((exists ff_gap_mdm_lt_mdr_secondwavewitnessminornonzeroevaluationdeterminanthscm_negative_column_bound. ff_gap_mdm_lt_mdr_secondwavewitnessminornonzeroevaluationdeterminanthscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_secondwavewitnessminornonzeroevaluationdeterminanthscm_negative) = (mdr_q_secondwavewitnessminornonzeroevaluationdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_secondwavewitnessminornonzeroevaluationdeterminanthscm_negative_cell ff_column_mdm_cell_mdr_secondwavewitnessminornonzeroevaluationdeterminanthscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_secondwavewitnessminornonzeroevaluationdeterminanthscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_secondwavewitnessminornonzeroevaluationdeterminanthscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_secondwavewitnessminornonzeroevaluationdeterminanthscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_secondwavewitnessminornonzeroevaluationdeterminanthscm_negative_cell = ff_row_mdm_prefix_mdr_secondwavewitnessminornonzeroevaluationdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_secondwavewitnessminornonzeroevaluationdeterminanthscm_negative_cell_row_after. ff_gap_mdm_le_mdr_secondwavewitnessminornonzeroevaluationdeterminanthscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_secondwavewitnessminornonzeroevaluationdeterminanthscm_negative)) /\ ff_row_mdm_cell_mdr_secondwavewitnessminornonzeroevaluationdeterminanthscm_negative_cell = S ff_row_mdm_prefix_mdr_secondwavewitnessminornonzeroevaluationdeterminanthscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_secondwavewitnessminornonzeroevaluationdeterminanthscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_secondwavewitnessminornonzeroevaluationdeterminanthscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_secondwavewitnessminornonzeroevaluationdeterminanthscm_negative) = (mdr_j_secondwavewitnessminornonzeroevaluationdeterminanthsc)) /\ ff_column_mdm_cell_mdr_secondwavewitnessminornonzeroevaluationdeterminanthscm_negative_cell = ff_column_mdm_prefix_mdr_secondwavewitnessminornonzeroevaluationdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_secondwavewitnessminornonzeroevaluationdeterminanthscm_negative_cell_column_after. ff_gap_mdm_le_mdr_secondwavewitnessminornonzeroevaluationdeterminanthscm_negative_cell_column_after + (mdr_j_secondwavewitnessminornonzeroevaluationdeterminanthsc) = (ff_column_mdm_prefix_mdr_secondwavewitnessminornonzeroevaluationdeterminanthscm_negative)) /\ ff_column_mdm_cell_mdr_secondwavewitnessminornonzeroevaluationdeterminanthscm_negative_cell = S ff_column_mdm_prefix_mdr_secondwavewitnessminornonzeroevaluationdeterminanthscm_negative))) /\ (((exists ff_h_mdm_mdr_secondwavewitnessminornonzeroevaluationdeterminanthscm_negative_cell_source. ff_h_mdm_mdr_secondwavewitnessminornonzeroevaluationdeterminanthscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_secondwavewitnessminornonzeroevaluationdeterminanthscm_negative) = S ((S ((ff_row_mdm_cell_mdr_secondwavewitnessminornonzeroevaluationdeterminanthscm_negative_cell) * (S (mdr_q_secondwavewitnessminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_secondwavewitnessminornonzeroevaluationdeterminanthscm_negative_cell))) * mdr_nc_secondwavewitnessminornonzeroevaluationdeterminanth)) /\ exists ff_q_mdm_mdr_secondwavewitnessminornonzeroevaluationdeterminanthscm_negative_cell_source. mdr_nb_secondwavewitnessminornonzeroevaluationdeterminanth = ff_q_mdm_mdr_secondwavewitnessminornonzeroevaluationdeterminanthscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_secondwavewitnessminornonzeroevaluationdeterminanthscm_negative_cell) * (S (mdr_q_secondwavewitnessminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_secondwavewitnessminornonzeroevaluationdeterminanthscm_negative_cell))) * mdr_nc_secondwavewitnessminornonzeroevaluationdeterminanth) + (ff_value_mdm_prefix_mdr_secondwavewitnessminornonzeroevaluationdeterminanthscm_negative)))))) /\ (((exists ff_h_mdm_mdr_secondwavewitnessminornonzeroevaluationdeterminanthscm_negative_target. ff_h_mdm_mdr_secondwavewitnessminornonzeroevaluationdeterminanthscm_negative_target + S (ff_value_mdm_prefix_mdr_secondwavewitnessminornonzeroevaluationdeterminanthscm_negative) = S ((S (ff_index_mdm_prefix_mdr_secondwavewitnessminornonzeroevaluationdeterminanthscm_negative)) * mdr_ut_secondwavewitnessminornonzeroevaluationdeterminanthsc)) /\ exists ff_q_mdm_mdr_secondwavewitnessminornonzeroevaluationdeterminanthscm_negative_target. mdr_un_secondwavewitnessminornonzeroevaluationdeterminanthsc = ff_q_mdm_mdr_secondwavewitnessminornonzeroevaluationdeterminanthscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_secondwavewitnessminornonzeroevaluationdeterminanthscm_negative)) * mdr_ut_secondwavewitnessminornonzeroevaluationdeterminanthsc) + (ff_value_mdm_prefix_mdr_secondwavewitnessminornonzeroevaluationdeterminanthscm_negative))))))))) /\ ((((exists ff_h_mdr_secondwavewitnessminornonzeroevaluationdeterminanthscp. ff_h_mdr_secondwavewitnessminornonzeroevaluationdeterminanthscp + S (mdr_p_secondwavewitnessminornonzeroevaluationdeterminanthsc) = S ((S (mdr_j_secondwavewitnessminornonzeroevaluationdeterminanthsc)) * mdr_ec_secondwavewitnessminornonzeroevaluationdeterminanths)) /\ exists ff_q_mdr_secondwavewitnessminornonzeroevaluationdeterminanthscp. mdr_eb_secondwavewitnessminornonzeroevaluationdeterminanths = ff_q_mdr_secondwavewitnessminornonzeroevaluationdeterminanthscp * S ((S (mdr_j_secondwavewitnessminornonzeroevaluationdeterminanthsc)) * mdr_ec_secondwavewitnessminornonzeroevaluationdeterminanths) + (mdr_p_secondwavewitnessminornonzeroevaluationdeterminanthsc))) /\ (((exists ff_h_mdr_secondwavewitnessminornonzeroevaluationdeterminanthscn. ff_h_mdr_secondwavewitnessminornonzeroevaluationdeterminanthscn + S (mdr_n_secondwavewitnessminornonzeroevaluationdeterminanthsc) = S ((S (mdr_j_secondwavewitnessminornonzeroevaluationdeterminanthsc)) * mdr_fc_secondwavewitnessminornonzeroevaluationdeterminanths)) /\ exists ff_q_mdr_secondwavewitnessminornonzeroevaluationdeterminanthscn. mdr_fb_secondwavewitnessminornonzeroevaluationdeterminanths = ff_q_mdr_secondwavewitnessminornonzeroevaluationdeterminanthscn * S ((S (mdr_j_secondwavewitnessminornonzeroevaluationdeterminanthsc)) * mdr_fc_secondwavewitnessminornonzeroevaluationdeterminanths) + (mdr_n_secondwavewitnessminornonzeroevaluationdeterminanthsc)))))))) /\ (exists ff_ub_mce_fold_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf ff_uc_mce_fold_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf ff_vb_mce_fold_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf ff_vc_mce_fold_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf. ((forall ff_index_mce_alternating_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_prefix. (exists ff_gap_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_prefix_index. ff_gap_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_prefix_index + S (ff_index_mce_alternating_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_prefix) = (S (mdr_q_secondwavewitnessminornonzeroevaluationdeterminanths))) -> exists ff_ap_mce_alternating_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_prefix ff_an_mce_alternating_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_prefix ff_bp_mce_alternating_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_prefix ff_bn_mce_alternating_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_prefix ff_p_mce_alternating_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_prefix ff_n_mce_alternating_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_prefix. ((((exists ff_h_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_prefix_ap. ff_h_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_prefix_ap + S (ff_ap_mce_alternating_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_prefix)) * mdr_pc_secondwavewitnessminornonzeroevaluationdeterminanth)) /\ exists ff_q_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_prefix_ap. mdr_pb_secondwavewitnessminornonzeroevaluationdeterminanth = ff_q_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_prefix)) * mdr_pc_secondwavewitnessminornonzeroevaluationdeterminanth) + (ff_ap_mce_alternating_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_prefix_an. ff_h_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_prefix_an + S (ff_an_mce_alternating_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_prefix)) * mdr_nc_secondwavewitnessminornonzeroevaluationdeterminanth)) /\ exists ff_q_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_prefix_an. mdr_nb_secondwavewitnessminornonzeroevaluationdeterminanth = ff_q_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_prefix)) * mdr_nc_secondwavewitnessminornonzeroevaluationdeterminanth) + (ff_an_mce_alternating_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_prefix_bp. ff_h_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_prefix_bp + S (ff_bp_mce_alternating_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_prefix)) * mdr_ec_secondwavewitnessminornonzeroevaluationdeterminanths)) /\ exists ff_q_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_prefix_bp. mdr_eb_secondwavewitnessminornonzeroevaluationdeterminanths = ff_q_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_prefix)) * mdr_ec_secondwavewitnessminornonzeroevaluationdeterminanths) + (ff_bp_mce_alternating_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_prefix_bn. ff_h_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_prefix_bn + S (ff_bn_mce_alternating_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_prefix)) * mdr_fc_secondwavewitnessminornonzeroevaluationdeterminanths)) /\ exists ff_q_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_prefix_bn. mdr_fb_secondwavewitnessminornonzeroevaluationdeterminanths = ff_q_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_prefix)) * mdr_fc_secondwavewitnessminornonzeroevaluationdeterminanths) + (ff_bn_mce_alternating_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_prefix_positive. ff_h_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_prefix_positive + S (ff_p_mce_alternating_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_prefix_positive. ff_ub_mce_fold_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf) + (ff_p_mce_alternating_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_prefix_negative. ff_h_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_prefix_negative + S (ff_n_mce_alternating_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_prefix_negative. ff_vb_mce_fold_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf) + (ff_n_mce_alternating_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_prefix))) /\ (((exists ff_even_mce_term_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_prefix = 2 * ff_even_mce_term_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_prefix_term) /\ (ff_p_mce_alternating_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_prefix = 2 * ff_odd_mce_term_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_positive ff_v_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_positive. ((((exists ff_h_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_positive_start. ff_h_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_positive_start. ff_u_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_positive_start * S ((S (0)) * ff_v_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_positive_terminal. ff_h_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_positive_terminal + S (mdr_p_secondwavewitnessminornonzeroevaluationdeterminanth) = S ((S ((S (mdr_q_secondwavewitnessminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_positive_terminal. ff_u_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_positive_terminal * S ((S ((S (mdr_q_secondwavewitnessminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_positive) + (mdr_p_secondwavewitnessminornonzeroevaluationdeterminanth))) /\ forall ff_i_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_positive. (exists ff_lt_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_positive_bound. ff_lt_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_positive_bound + S ff_i_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_positive = (S (mdr_q_secondwavewitnessminornonzeroevaluationdeterminanths))) -> exists ff_a_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_positive ff_r_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_positive ff_s_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_positive. ((((exists ff_h_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_positive_summand. ff_h_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_positive_summand + S (ff_a_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_positive_summand. ff_ub_mce_fold_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_positive_summand * S ((S (ff_i_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf) + (ff_a_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_positive_partial. ff_h_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_positive_partial + S (ff_r_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_positive_partial. ff_u_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_positive_partial * S ((S (ff_i_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_positive) + (ff_r_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_positive_successor. ff_h_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_positive_successor + S (ff_s_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_positive) = S ((S (S ff_i_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_positive_successor. ff_u_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_positive_successor * S ((S (S ff_i_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_positive) + (ff_s_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_positive))) /\ ff_s_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_positive = ff_r_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_positive + ff_a_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_positive)))))) /\ (exists ff_u_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_negative ff_v_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_negative. ((((exists ff_h_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_negative_start. ff_h_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_negative_start. ff_u_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_negative_start * S ((S (0)) * ff_v_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_negative_terminal. ff_h_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_negative_terminal + S (mdr_n_secondwavewitnessminornonzeroevaluationdeterminanth) = S ((S ((S (mdr_q_secondwavewitnessminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_negative_terminal. ff_u_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_negative_terminal * S ((S ((S (mdr_q_secondwavewitnessminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_negative) + (mdr_n_secondwavewitnessminornonzeroevaluationdeterminanth))) /\ forall ff_i_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_negative. (exists ff_lt_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_negative_bound. ff_lt_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_negative_bound + S ff_i_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_negative = (S (mdr_q_secondwavewitnessminornonzeroevaluationdeterminanths))) -> exists ff_a_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_negative ff_r_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_negative ff_s_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_negative. ((((exists ff_h_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_negative_summand. ff_h_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_negative_summand + S (ff_a_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_negative_summand. ff_vb_mce_fold_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_negative_summand * S ((S (ff_i_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf) + (ff_a_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_negative_partial. ff_h_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_negative_partial + S (ff_r_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_negative_partial. ff_u_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_negative_partial * S ((S (ff_i_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_negative) + (ff_r_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_negative_successor. ff_h_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_negative_successor + S (ff_s_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_negative) = S ((S (S ff_i_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_negative_successor. ff_u_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_negative_successor * S ((S (S ff_i_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_negative) + (ff_s_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_negative))) /\ ff_s_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_negative = ff_r_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_negative + ff_a_mce_mdr_secondwavewitnessminornonzeroevaluationdeterminanthsf_negative))))))))))))))) /\ ((exists mdr_gap_secondwavewitnessminornonzeroevaluationdeterminanti. mdr_gap_secondwavewitnessminornonzeroevaluationdeterminanti + S (mdr_i_secondwavewitnessminornonzeroevaluationdeterminant) = (mdr_l_secondwavewitnessminornonzeroevaluationdeterminant)) /\ (exists mdr_z_secondwavewitnessminornonzeroevaluationdeterminantr. ((exists mdr_a_secondwavewitnessminornonzeroevaluationdeterminantrc mdr_b_secondwavewitnessminornonzeroevaluationdeterminantrc mdr_c_secondwavewitnessminornonzeroevaluationdeterminantrc mdr_e_secondwavewitnessminornonzeroevaluationdeterminantrc mdr_f_secondwavewitnessminornonzeroevaluationdeterminantrc. ((mdr_a_secondwavewitnessminornonzeroevaluationdeterminantrc = ((rank) + (mdr_ub_secondwavewitnessminornonzeroevaluation)) * S ((rank) + (mdr_ub_secondwavewitnessminornonzeroevaluation)) + ((mdr_ub_secondwavewitnessminornonzeroevaluation) + (mdr_ub_secondwavewitnessminornonzeroevaluation))) /\ ((mdr_b_secondwavewitnessminornonzeroevaluationdeterminantrc = ((mdr_uc_secondwavewitnessminornonzeroevaluation) + (mdr_vb_secondwavewitnessminornonzeroevaluation)) * S ((mdr_uc_secondwavewitnessminornonzeroevaluation) + (mdr_vb_secondwavewitnessminornonzeroevaluation)) + ((mdr_vb_secondwavewitnessminornonzeroevaluation) + (mdr_vb_secondwavewitnessminornonzeroevaluation))) /\ ((mdr_c_secondwavewitnessminornonzeroevaluationdeterminantrc = ((mdr_a_secondwavewitnessminornonzeroevaluationdeterminantrc) + (mdr_b_secondwavewitnessminornonzeroevaluationdeterminantrc)) * S ((mdr_a_secondwavewitnessminornonzeroevaluationdeterminantrc) + (mdr_b_secondwavewitnessminornonzeroevaluationdeterminantrc)) + ((mdr_b_secondwavewitnessminornonzeroevaluationdeterminantrc) + (mdr_b_secondwavewitnessminornonzeroevaluationdeterminantrc))) /\ ((mdr_e_secondwavewitnessminornonzeroevaluationdeterminantrc = ((mdr_p_secondwavewitnessminornonzero) + (mdr_n_secondwavewitnessminornonzero)) * S ((mdr_p_secondwavewitnessminornonzero) + (mdr_n_secondwavewitnessminornonzero)) + ((mdr_n_secondwavewitnessminornonzero) + (mdr_n_secondwavewitnessminornonzero))) /\ ((mdr_f_secondwavewitnessminornonzeroevaluationdeterminantrc = ((mdr_vc_secondwavewitnessminornonzeroevaluation) + (mdr_e_secondwavewitnessminornonzeroevaluationdeterminantrc)) * S ((mdr_vc_secondwavewitnessminornonzeroevaluation) + (mdr_e_secondwavewitnessminornonzeroevaluationdeterminantrc)) + ((mdr_e_secondwavewitnessminornonzeroevaluationdeterminantrc) + (mdr_e_secondwavewitnessminornonzeroevaluationdeterminantrc))) /\ ((mdr_z_secondwavewitnessminornonzeroevaluationdeterminantr) = ((mdr_c_secondwavewitnessminornonzeroevaluationdeterminantrc) + (mdr_f_secondwavewitnessminornonzeroevaluationdeterminantrc)) * S ((mdr_c_secondwavewitnessminornonzeroevaluationdeterminantrc) + (mdr_f_secondwavewitnessminornonzeroevaluationdeterminantrc)) + ((mdr_f_secondwavewitnessminornonzeroevaluationdeterminantrc) + (mdr_f_secondwavewitnessminornonzeroevaluationdeterminantrc))))))))) /\ (((exists ff_h_mdr_secondwavewitnessminornonzeroevaluationdeterminantrb. ff_h_mdr_secondwavewitnessminornonzeroevaluationdeterminantrb + S (mdr_z_secondwavewitnessminornonzeroevaluationdeterminantr) = S ((S (mdr_i_secondwavewitnessminornonzeroevaluationdeterminant)) * mdr_c_secondwavewitnessminornonzeroevaluationdeterminant)) /\ exists ff_q_mdr_secondwavewitnessminornonzeroevaluationdeterminantrb. mdr_b_secondwavewitnessminornonzeroevaluationdeterminant = ff_q_mdr_secondwavewitnessminornonzeroevaluationdeterminantrb * S ((S (mdr_i_secondwavewitnessminornonzeroevaluationdeterminant)) * mdr_c_secondwavewitnessminornonzeroevaluationdeterminant) + (mdr_z_secondwavewitnessminornonzeroevaluationdeterminantr)))))))))) /\ (~(mdr_p_secondwavewitnessminornonzero = mdr_n_secondwavewitnessminornonzero)))))))) /\ (forall mdr_q_secondwave. (exists mdr_gap_secondwavehigher. mdr_gap_secondwavehigher + S (rank) = (mdr_q_secondwave)) -> (forall mdr_rb_secondwavezero mdr_rc_secondwavezero mdr_cb_secondwavezero mdr_cc_secondwavezero mdr_p_secondwavezero mdr_n_secondwavezero. (((forall fom_index_mrf_secondwavezerorowsbound. (exists fom_gap_mrf_secondwavezerorowsbound_index_bound. fom_gap_mrf_secondwavezerorowsbound_index_bound + S (fom_index_mrf_secondwavezerorowsbound) = mdr_q_secondwave) -> exists fom_value_mrf_secondwavezerorowsbound. ((((exists fom_beta_height_mrf_secondwavezerorowsbound_entry. fom_beta_height_mrf_secondwavezerorowsbound_entry + S (fom_value_mrf_secondwavezerorowsbound) = S ((S (fom_index_mrf_secondwavezerorowsbound)) * mdr_rc_secondwavezero)) /\ exists fom_beta_quotient_mrf_secondwavezerorowsbound_entry. mdr_rb_secondwavezero = fom_beta_quotient_mrf_secondwavezerorowsbound_entry * S ((S (fom_index_mrf_secondwavezerorowsbound)) * mdr_rc_secondwavezero) + (fom_value_mrf_secondwavezerorowsbound))) /\ (exists fom_gap_mrf_secondwavezerorowsbound_value_bound. fom_gap_mrf_secondwavezerorowsbound_value_bound + S (fom_value_mrf_secondwavezerorowsbound) = r))) /\ (forall mdr_i_secondwavezerorowsdistinct mdr_j_secondwavezerorowsdistinct mdr_a_secondwavezerorowsdistinct. (exists mdr_gap_secondwavezerorowsdistincti. mdr_gap_secondwavezerorowsdistincti + S (mdr_i_secondwavezerorowsdistinct) = (mdr_q_secondwave)) -> (exists mdr_gap_secondwavezerorowsdistinctj. mdr_gap_secondwavezerorowsdistinctj + S (mdr_j_secondwavezerorowsdistinct) = (mdr_q_secondwave)) -> (((exists ff_h_mdr_secondwavezerorowsdistinctfirst. ff_h_mdr_secondwavezerorowsdistinctfirst + S (mdr_a_secondwavezerorowsdistinct) = S ((S (mdr_i_secondwavezerorowsdistinct)) * mdr_rc_secondwavezero)) /\ exists ff_q_mdr_secondwavezerorowsdistinctfirst. mdr_rb_secondwavezero = ff_q_mdr_secondwavezerorowsdistinctfirst * S ((S (mdr_i_secondwavezerorowsdistinct)) * mdr_rc_secondwavezero) + (mdr_a_secondwavezerorowsdistinct))) -> (((exists ff_h_mdr_secondwavezerorowsdistinctsecond. ff_h_mdr_secondwavezerorowsdistinctsecond + S (mdr_a_secondwavezerorowsdistinct) = S ((S (mdr_j_secondwavezerorowsdistinct)) * mdr_rc_secondwavezero)) /\ exists ff_q_mdr_secondwavezerorowsdistinctsecond. mdr_rb_secondwavezero = ff_q_mdr_secondwavezerorowsdistinctsecond * S ((S (mdr_j_secondwavezerorowsdistinct)) * mdr_rc_secondwavezero) + (mdr_a_secondwavezerorowsdistinct))) -> mdr_i_secondwavezerorowsdistinct = mdr_j_secondwavezerorowsdistinct))) -> (((forall fom_index_mrf_secondwavezerocolumnsbound. (exists fom_gap_mrf_secondwavezerocolumnsbound_index_bound. fom_gap_mrf_secondwavezerocolumnsbound_index_bound + S (fom_index_mrf_secondwavezerocolumnsbound) = mdr_q_secondwave) -> exists fom_value_mrf_secondwavezerocolumnsbound. ((((exists fom_beta_height_mrf_secondwavezerocolumnsbound_entry. fom_beta_height_mrf_secondwavezerocolumnsbound_entry + S (fom_value_mrf_secondwavezerocolumnsbound) = S ((S (fom_index_mrf_secondwavezerocolumnsbound)) * mdr_cc_secondwavezero)) /\ exists fom_beta_quotient_mrf_secondwavezerocolumnsbound_entry. mdr_cb_secondwavezero = fom_beta_quotient_mrf_secondwavezerocolumnsbound_entry * S ((S (fom_index_mrf_secondwavezerocolumnsbound)) * mdr_cc_secondwavezero) + (fom_value_mrf_secondwavezerocolumnsbound))) /\ (exists fom_gap_mrf_secondwavezerocolumnsbound_value_bound. fom_gap_mrf_secondwavezerocolumnsbound_value_bound + S (fom_value_mrf_secondwavezerocolumnsbound) = w))) /\ (forall mdr_i_secondwavezerocolumnsdistinct mdr_j_secondwavezerocolumnsdistinct mdr_a_secondwavezerocolumnsdistinct. (exists mdr_gap_secondwavezerocolumnsdistincti. mdr_gap_secondwavezerocolumnsdistincti + S (mdr_i_secondwavezerocolumnsdistinct) = (mdr_q_secondwave)) -> (exists mdr_gap_secondwavezerocolumnsdistinctj. mdr_gap_secondwavezerocolumnsdistinctj + S (mdr_j_secondwavezerocolumnsdistinct) = (mdr_q_secondwave)) -> (((exists ff_h_mdr_secondwavezerocolumnsdistinctfirst. ff_h_mdr_secondwavezerocolumnsdistinctfirst + S (mdr_a_secondwavezerocolumnsdistinct) = S ((S (mdr_i_secondwavezerocolumnsdistinct)) * mdr_cc_secondwavezero)) /\ exists ff_q_mdr_secondwavezerocolumnsdistinctfirst. mdr_cb_secondwavezero = ff_q_mdr_secondwavezerocolumnsdistinctfirst * S ((S (mdr_i_secondwavezerocolumnsdistinct)) * mdr_cc_secondwavezero) + (mdr_a_secondwavezerocolumnsdistinct))) -> (((exists ff_h_mdr_secondwavezerocolumnsdistinctsecond. ff_h_mdr_secondwavezerocolumnsdistinctsecond + S (mdr_a_secondwavezerocolumnsdistinct) = S ((S (mdr_j_secondwavezerocolumnsdistinct)) * mdr_cc_secondwavezero)) /\ exists ff_q_mdr_secondwavezerocolumnsdistinctsecond. mdr_cb_secondwavezero = ff_q_mdr_secondwavezerocolumnsdistinctsecond * S ((S (mdr_j_secondwavezerocolumnsdistinct)) * mdr_cc_secondwavezero) + (mdr_a_secondwavezerocolumnsdistinct))) -> mdr_i_secondwavezerocolumnsdistinct = mdr_j_secondwavezerocolumnsdistinct))) -> (exists mdr_ub_secondwavezeroevaluation mdr_uc_secondwavezeroevaluation mdr_vb_secondwavezeroevaluation mdr_vc_secondwavezeroevaluation. ((((forall mdr_i_secondwavezeroevaluationmatrixpositive. (exists mdr_gap_secondwavezeroevaluationmatrixpositivebound. mdr_gap_secondwavezeroevaluationmatrixpositivebound + S (mdr_i_secondwavezeroevaluationmatrixpositive) = ((mdr_q_secondwave) * (mdr_q_secondwave))) -> exists mdr_a_secondwavezeroevaluationmatrixpositive. (((exists mdr_r_secondwavezeroevaluationmatrixpositivepoint mdr_s_secondwavezeroevaluationmatrixpositivepoint mdr_u_secondwavezeroevaluationmatrixpositivepoint mdr_v_secondwavezeroevaluationmatrixpositivepoint. ((mdr_i_secondwavezeroevaluationmatrixpositive = (mdr_q_secondwave) * mdr_r_secondwavezeroevaluationmatrixpositivepoint + mdr_s_secondwavezeroevaluationmatrixpositivepoint) /\ ((exists mdr_gap_secondwavezeroevaluationmatrixpositivepointcolumn. mdr_gap_secondwavezeroevaluationmatrixpositivepointcolumn + S (mdr_s_secondwavezeroevaluationmatrixpositivepoint) = (mdr_q_secondwave)) /\ ((((exists ff_h_mdr_secondwavezeroevaluationmatrixpositivepointrow_index. ff_h_mdr_secondwavezeroevaluationmatrixpositivepointrow_index + S (mdr_u_secondwavezeroevaluationmatrixpositivepoint) = S ((S (mdr_r_secondwavezeroevaluationmatrixpositivepoint)) * mdr_rc_secondwavezero)) /\ exists ff_q_mdr_secondwavezeroevaluationmatrixpositivepointrow_index. mdr_rb_secondwavezero = ff_q_mdr_secondwavezeroevaluationmatrixpositivepointrow_index * S ((S (mdr_r_secondwavezeroevaluationmatrixpositivepoint)) * mdr_rc_secondwavezero) + (mdr_u_secondwavezeroevaluationmatrixpositivepoint))) /\ ((((exists ff_h_mdr_secondwavezeroevaluationmatrixpositivepointcolumn_index. ff_h_mdr_secondwavezeroevaluationmatrixpositivepointcolumn_index + S (mdr_v_secondwavezeroevaluationmatrixpositivepoint) = S ((S (mdr_s_secondwavezeroevaluationmatrixpositivepoint)) * mdr_cc_secondwavezero)) /\ exists ff_q_mdr_secondwavezeroevaluationmatrixpositivepointcolumn_index. mdr_cb_secondwavezero = ff_q_mdr_secondwavezeroevaluationmatrixpositivepointcolumn_index * S ((S (mdr_s_secondwavezeroevaluationmatrixpositivepoint)) * mdr_cc_secondwavezero) + (mdr_v_secondwavezeroevaluationmatrixpositivepoint))) /\ (((exists ff_h_mdr_secondwavezeroevaluationmatrixpositivepointsource. ff_h_mdr_secondwavezeroevaluationmatrixpositivepointsource + S (mdr_a_secondwavezeroevaluationmatrixpositive) = S ((S ((mdr_u_secondwavezeroevaluationmatrixpositivepoint) * (w) + (mdr_v_secondwavezeroevaluationmatrixpositivepoint))) * pc)) /\ exists ff_q_mdr_secondwavezeroevaluationmatrixpositivepointsource. pb = ff_q_mdr_secondwavezeroevaluationmatrixpositivepointsource * S ((S ((mdr_u_secondwavezeroevaluationmatrixpositivepoint) * (w) + (mdr_v_secondwavezeroevaluationmatrixpositivepoint))) * pc) + (mdr_a_secondwavezeroevaluationmatrixpositive)))))))) /\ (((exists ff_h_mdr_secondwavezeroevaluationmatrixpositiveoutput. ff_h_mdr_secondwavezeroevaluationmatrixpositiveoutput + S (mdr_a_secondwavezeroevaluationmatrixpositive) = S ((S (mdr_i_secondwavezeroevaluationmatrixpositive)) * mdr_uc_secondwavezeroevaluation)) /\ exists ff_q_mdr_secondwavezeroevaluationmatrixpositiveoutput. mdr_ub_secondwavezeroevaluation = ff_q_mdr_secondwavezeroevaluationmatrixpositiveoutput * S ((S (mdr_i_secondwavezeroevaluationmatrixpositive)) * mdr_uc_secondwavezeroevaluation) + (mdr_a_secondwavezeroevaluationmatrixpositive)))))) /\ (forall mdr_i_secondwavezeroevaluationmatrixnegative. (exists mdr_gap_secondwavezeroevaluationmatrixnegativebound. mdr_gap_secondwavezeroevaluationmatrixnegativebound + S (mdr_i_secondwavezeroevaluationmatrixnegative) = ((mdr_q_secondwave) * (mdr_q_secondwave))) -> exists mdr_a_secondwavezeroevaluationmatrixnegative. (((exists mdr_r_secondwavezeroevaluationmatrixnegativepoint mdr_s_secondwavezeroevaluationmatrixnegativepoint mdr_u_secondwavezeroevaluationmatrixnegativepoint mdr_v_secondwavezeroevaluationmatrixnegativepoint. ((mdr_i_secondwavezeroevaluationmatrixnegative = (mdr_q_secondwave) * mdr_r_secondwavezeroevaluationmatrixnegativepoint + mdr_s_secondwavezeroevaluationmatrixnegativepoint) /\ ((exists mdr_gap_secondwavezeroevaluationmatrixnegativepointcolumn. mdr_gap_secondwavezeroevaluationmatrixnegativepointcolumn + S (mdr_s_secondwavezeroevaluationmatrixnegativepoint) = (mdr_q_secondwave)) /\ ((((exists ff_h_mdr_secondwavezeroevaluationmatrixnegativepointrow_index. ff_h_mdr_secondwavezeroevaluationmatrixnegativepointrow_index + S (mdr_u_secondwavezeroevaluationmatrixnegativepoint) = S ((S (mdr_r_secondwavezeroevaluationmatrixnegativepoint)) * mdr_rc_secondwavezero)) /\ exists ff_q_mdr_secondwavezeroevaluationmatrixnegativepointrow_index. mdr_rb_secondwavezero = ff_q_mdr_secondwavezeroevaluationmatrixnegativepointrow_index * S ((S (mdr_r_secondwavezeroevaluationmatrixnegativepoint)) * mdr_rc_secondwavezero) + (mdr_u_secondwavezeroevaluationmatrixnegativepoint))) /\ ((((exists ff_h_mdr_secondwavezeroevaluationmatrixnegativepointcolumn_index. ff_h_mdr_secondwavezeroevaluationmatrixnegativepointcolumn_index + S (mdr_v_secondwavezeroevaluationmatrixnegativepoint) = S ((S (mdr_s_secondwavezeroevaluationmatrixnegativepoint)) * mdr_cc_secondwavezero)) /\ exists ff_q_mdr_secondwavezeroevaluationmatrixnegativepointcolumn_index. mdr_cb_secondwavezero = ff_q_mdr_secondwavezeroevaluationmatrixnegativepointcolumn_index * S ((S (mdr_s_secondwavezeroevaluationmatrixnegativepoint)) * mdr_cc_secondwavezero) + (mdr_v_secondwavezeroevaluationmatrixnegativepoint))) /\ (((exists ff_h_mdr_secondwavezeroevaluationmatrixnegativepointsource. ff_h_mdr_secondwavezeroevaluationmatrixnegativepointsource + S (mdr_a_secondwavezeroevaluationmatrixnegative) = S ((S ((mdr_u_secondwavezeroevaluationmatrixnegativepoint) * (w) + (mdr_v_secondwavezeroevaluationmatrixnegativepoint))) * nc)) /\ exists ff_q_mdr_secondwavezeroevaluationmatrixnegativepointsource. nb = ff_q_mdr_secondwavezeroevaluationmatrixnegativepointsource * S ((S ((mdr_u_secondwavezeroevaluationmatrixnegativepoint) * (w) + (mdr_v_secondwavezeroevaluationmatrixnegativepoint))) * nc) + (mdr_a_secondwavezeroevaluationmatrixnegative)))))))) /\ (((exists ff_h_mdr_secondwavezeroevaluationmatrixnegativeoutput. ff_h_mdr_secondwavezeroevaluationmatrixnegativeoutput + S (mdr_a_secondwavezeroevaluationmatrixnegative) = S ((S (mdr_i_secondwavezeroevaluationmatrixnegative)) * mdr_vc_secondwavezeroevaluation)) /\ exists ff_q_mdr_secondwavezeroevaluationmatrixnegativeoutput. mdr_vb_secondwavezeroevaluation = ff_q_mdr_secondwavezeroevaluationmatrixnegativeoutput * S ((S (mdr_i_secondwavezeroevaluationmatrixnegative)) * mdr_vc_secondwavezeroevaluation) + (mdr_a_secondwavezeroevaluationmatrixnegative)))))))) /\ (exists mdr_b_secondwavezeroevaluationdeterminant mdr_c_secondwavezeroevaluationdeterminant mdr_l_secondwavezeroevaluationdeterminant mdr_i_secondwavezeroevaluationdeterminant. ((forall mdr_i_secondwavezeroevaluationdeterminanth. (exists mdr_gap_secondwavezeroevaluationdeterminanthi. mdr_gap_secondwavezeroevaluationdeterminanthi + S (mdr_i_secondwavezeroevaluationdeterminanth) = (mdr_l_secondwavezeroevaluationdeterminant)) -> exists mdr_d_secondwavezeroevaluationdeterminanth mdr_pb_secondwavezeroevaluationdeterminanth mdr_pc_secondwavezeroevaluationdeterminanth mdr_nb_secondwavezeroevaluationdeterminanth mdr_nc_secondwavezeroevaluationdeterminanth mdr_p_secondwavezeroevaluationdeterminanth mdr_n_secondwavezeroevaluationdeterminanth. ((exists mdr_z_secondwavezeroevaluationdeterminanthr. ((exists mdr_a_secondwavezeroevaluationdeterminanthrc mdr_b_secondwavezeroevaluationdeterminanthrc mdr_c_secondwavezeroevaluationdeterminanthrc mdr_e_secondwavezeroevaluationdeterminanthrc mdr_f_secondwavezeroevaluationdeterminanthrc. ((mdr_a_secondwavezeroevaluationdeterminanthrc = ((mdr_d_secondwavezeroevaluationdeterminanth) + (mdr_pb_secondwavezeroevaluationdeterminanth)) * S ((mdr_d_secondwavezeroevaluationdeterminanth) + (mdr_pb_secondwavezeroevaluationdeterminanth)) + ((mdr_pb_secondwavezeroevaluationdeterminanth) + (mdr_pb_secondwavezeroevaluationdeterminanth))) /\ ((mdr_b_secondwavezeroevaluationdeterminanthrc = ((mdr_pc_secondwavezeroevaluationdeterminanth) + (mdr_nb_secondwavezeroevaluationdeterminanth)) * S ((mdr_pc_secondwavezeroevaluationdeterminanth) + (mdr_nb_secondwavezeroevaluationdeterminanth)) + ((mdr_nb_secondwavezeroevaluationdeterminanth) + (mdr_nb_secondwavezeroevaluationdeterminanth))) /\ ((mdr_c_secondwavezeroevaluationdeterminanthrc = ((mdr_a_secondwavezeroevaluationdeterminanthrc) + (mdr_b_secondwavezeroevaluationdeterminanthrc)) * S ((mdr_a_secondwavezeroevaluationdeterminanthrc) + (mdr_b_secondwavezeroevaluationdeterminanthrc)) + ((mdr_b_secondwavezeroevaluationdeterminanthrc) + (mdr_b_secondwavezeroevaluationdeterminanthrc))) /\ ((mdr_e_secondwavezeroevaluationdeterminanthrc = ((mdr_p_secondwavezeroevaluationdeterminanth) + (mdr_n_secondwavezeroevaluationdeterminanth)) * S ((mdr_p_secondwavezeroevaluationdeterminanth) + (mdr_n_secondwavezeroevaluationdeterminanth)) + ((mdr_n_secondwavezeroevaluationdeterminanth) + (mdr_n_secondwavezeroevaluationdeterminanth))) /\ ((mdr_f_secondwavezeroevaluationdeterminanthrc = ((mdr_nc_secondwavezeroevaluationdeterminanth) + (mdr_e_secondwavezeroevaluationdeterminanthrc)) * S ((mdr_nc_secondwavezeroevaluationdeterminanth) + (mdr_e_secondwavezeroevaluationdeterminanthrc)) + ((mdr_e_secondwavezeroevaluationdeterminanthrc) + (mdr_e_secondwavezeroevaluationdeterminanthrc))) /\ ((mdr_z_secondwavezeroevaluationdeterminanthr) = ((mdr_c_secondwavezeroevaluationdeterminanthrc) + (mdr_f_secondwavezeroevaluationdeterminanthrc)) * S ((mdr_c_secondwavezeroevaluationdeterminanthrc) + (mdr_f_secondwavezeroevaluationdeterminanthrc)) + ((mdr_f_secondwavezeroevaluationdeterminanthrc) + (mdr_f_secondwavezeroevaluationdeterminanthrc))))))))) /\ (((exists ff_h_mdr_secondwavezeroevaluationdeterminanthrb. ff_h_mdr_secondwavezeroevaluationdeterminanthrb + S (mdr_z_secondwavezeroevaluationdeterminanthr) = S ((S (mdr_i_secondwavezeroevaluationdeterminanth)) * mdr_c_secondwavezeroevaluationdeterminant)) /\ exists ff_q_mdr_secondwavezeroevaluationdeterminanthrb. mdr_b_secondwavezeroevaluationdeterminant = ff_q_mdr_secondwavezeroevaluationdeterminanthrb * S ((S (mdr_i_secondwavezeroevaluationdeterminanth)) * mdr_c_secondwavezeroevaluationdeterminant) + (mdr_z_secondwavezeroevaluationdeterminanthr))))) /\ (((((mdr_d_secondwavezeroevaluationdeterminanth) = 0) /\ (((mdr_p_secondwavezeroevaluationdeterminanth) = 1) /\ ((mdr_n_secondwavezeroevaluationdeterminanth) = 0))) \/ exists mdr_q_secondwavezeroevaluationdeterminanths mdr_eb_secondwavezeroevaluationdeterminanths mdr_ec_secondwavezeroevaluationdeterminanths mdr_fb_secondwavezeroevaluationdeterminanths mdr_fc_secondwavezeroevaluationdeterminanths. (((mdr_d_secondwavezeroevaluationdeterminanth) = S (mdr_q_secondwavezeroevaluationdeterminanths)) /\ ((forall mdr_j_secondwavezeroevaluationdeterminanthsc. (exists mdr_gap_secondwavezeroevaluationdeterminanthscj. mdr_gap_secondwavezeroevaluationdeterminanthscj + S (mdr_j_secondwavezeroevaluationdeterminanthsc) = (S (mdr_q_secondwavezeroevaluationdeterminanths))) -> exists mdr_i_secondwavezeroevaluationdeterminanthsc mdr_up_secondwavezeroevaluationdeterminanthsc mdr_us_secondwavezeroevaluationdeterminanthsc mdr_un_secondwavezeroevaluationdeterminanthsc mdr_ut_secondwavezeroevaluationdeterminanthsc mdr_p_secondwavezeroevaluationdeterminanthsc mdr_n_secondwavezeroevaluationdeterminanthsc. ((exists mdr_gap_secondwavezeroevaluationdeterminanthsci. mdr_gap_secondwavezeroevaluationdeterminanthsci + S (mdr_i_secondwavezeroevaluationdeterminanthsc) = (mdr_i_secondwavezeroevaluationdeterminanth)) /\ ((exists mdr_z_secondwavezeroevaluationdeterminanthscr. ((exists mdr_a_secondwavezeroevaluationdeterminanthscrc mdr_b_secondwavezeroevaluationdeterminanthscrc mdr_c_secondwavezeroevaluationdeterminanthscrc mdr_e_secondwavezeroevaluationdeterminanthscrc mdr_f_secondwavezeroevaluationdeterminanthscrc. ((mdr_a_secondwavezeroevaluationdeterminanthscrc = ((mdr_q_secondwavezeroevaluationdeterminanths) + (mdr_up_secondwavezeroevaluationdeterminanthsc)) * S ((mdr_q_secondwavezeroevaluationdeterminanths) + (mdr_up_secondwavezeroevaluationdeterminanthsc)) + ((mdr_up_secondwavezeroevaluationdeterminanthsc) + (mdr_up_secondwavezeroevaluationdeterminanthsc))) /\ ((mdr_b_secondwavezeroevaluationdeterminanthscrc = ((mdr_us_secondwavezeroevaluationdeterminanthsc) + (mdr_un_secondwavezeroevaluationdeterminanthsc)) * S ((mdr_us_secondwavezeroevaluationdeterminanthsc) + (mdr_un_secondwavezeroevaluationdeterminanthsc)) + ((mdr_un_secondwavezeroevaluationdeterminanthsc) + (mdr_un_secondwavezeroevaluationdeterminanthsc))) /\ ((mdr_c_secondwavezeroevaluationdeterminanthscrc = ((mdr_a_secondwavezeroevaluationdeterminanthscrc) + (mdr_b_secondwavezeroevaluationdeterminanthscrc)) * S ((mdr_a_secondwavezeroevaluationdeterminanthscrc) + (mdr_b_secondwavezeroevaluationdeterminanthscrc)) + ((mdr_b_secondwavezeroevaluationdeterminanthscrc) + (mdr_b_secondwavezeroevaluationdeterminanthscrc))) /\ ((mdr_e_secondwavezeroevaluationdeterminanthscrc = ((mdr_p_secondwavezeroevaluationdeterminanthsc) + (mdr_n_secondwavezeroevaluationdeterminanthsc)) * S ((mdr_p_secondwavezeroevaluationdeterminanthsc) + (mdr_n_secondwavezeroevaluationdeterminanthsc)) + ((mdr_n_secondwavezeroevaluationdeterminanthsc) + (mdr_n_secondwavezeroevaluationdeterminanthsc))) /\ ((mdr_f_secondwavezeroevaluationdeterminanthscrc = ((mdr_ut_secondwavezeroevaluationdeterminanthsc) + (mdr_e_secondwavezeroevaluationdeterminanthscrc)) * S ((mdr_ut_secondwavezeroevaluationdeterminanthsc) + (mdr_e_secondwavezeroevaluationdeterminanthscrc)) + ((mdr_e_secondwavezeroevaluationdeterminanthscrc) + (mdr_e_secondwavezeroevaluationdeterminanthscrc))) /\ ((mdr_z_secondwavezeroevaluationdeterminanthscr) = ((mdr_c_secondwavezeroevaluationdeterminanthscrc) + (mdr_f_secondwavezeroevaluationdeterminanthscrc)) * S ((mdr_c_secondwavezeroevaluationdeterminanthscrc) + (mdr_f_secondwavezeroevaluationdeterminanthscrc)) + ((mdr_f_secondwavezeroevaluationdeterminanthscrc) + (mdr_f_secondwavezeroevaluationdeterminanthscrc))))))))) /\ (((exists ff_h_mdr_secondwavezeroevaluationdeterminanthscrb. ff_h_mdr_secondwavezeroevaluationdeterminanthscrb + S (mdr_z_secondwavezeroevaluationdeterminanthscr) = S ((S (mdr_i_secondwavezeroevaluationdeterminanthsc)) * mdr_c_secondwavezeroevaluationdeterminant)) /\ exists ff_q_mdr_secondwavezeroevaluationdeterminanthscrb. mdr_b_secondwavezeroevaluationdeterminant = ff_q_mdr_secondwavezeroevaluationdeterminanthscrb * S ((S (mdr_i_secondwavezeroevaluationdeterminanthsc)) * mdr_c_secondwavezeroevaluationdeterminant) + (mdr_z_secondwavezeroevaluationdeterminanthscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_secondwavezeroevaluationdeterminanthscm_positive. (exists ff_gap_mdm_lt_mdr_secondwavezeroevaluationdeterminanthscm_positive_index_bound. ff_gap_mdm_lt_mdr_secondwavezeroevaluationdeterminanthscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_secondwavezeroevaluationdeterminanthscm_positive) = ((mdr_q_secondwavezeroevaluationdeterminanths) * (mdr_q_secondwavezeroevaluationdeterminanths))) -> exists ff_row_mdm_prefix_mdr_secondwavezeroevaluationdeterminanthscm_positive ff_column_mdm_prefix_mdr_secondwavezeroevaluationdeterminanthscm_positive ff_value_mdm_prefix_mdr_secondwavezeroevaluationdeterminanthscm_positive. (ff_index_mdm_prefix_mdr_secondwavezeroevaluationdeterminanthscm_positive = (mdr_q_secondwavezeroevaluationdeterminanths) * ff_row_mdm_prefix_mdr_secondwavezeroevaluationdeterminanthscm_positive + ff_column_mdm_prefix_mdr_secondwavezeroevaluationdeterminanthscm_positive /\ ((exists ff_gap_mdm_lt_mdr_secondwavezeroevaluationdeterminanthscm_positive_column_bound. ff_gap_mdm_lt_mdr_secondwavezeroevaluationdeterminanthscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_secondwavezeroevaluationdeterminanthscm_positive) = (mdr_q_secondwavezeroevaluationdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_secondwavezeroevaluationdeterminanthscm_positive_cell ff_column_mdm_cell_mdr_secondwavezeroevaluationdeterminanthscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_secondwavezeroevaluationdeterminanthscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_secondwavezeroevaluationdeterminanthscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_secondwavezeroevaluationdeterminanthscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_secondwavezeroevaluationdeterminanthscm_positive_cell = ff_row_mdm_prefix_mdr_secondwavezeroevaluationdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_secondwavezeroevaluationdeterminanthscm_positive_cell_row_after. ff_gap_mdm_le_mdr_secondwavezeroevaluationdeterminanthscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_secondwavezeroevaluationdeterminanthscm_positive)) /\ ff_row_mdm_cell_mdr_secondwavezeroevaluationdeterminanthscm_positive_cell = S ff_row_mdm_prefix_mdr_secondwavezeroevaluationdeterminanthscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_secondwavezeroevaluationdeterminanthscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_secondwavezeroevaluationdeterminanthscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_secondwavezeroevaluationdeterminanthscm_positive) = (mdr_j_secondwavezeroevaluationdeterminanthsc)) /\ ff_column_mdm_cell_mdr_secondwavezeroevaluationdeterminanthscm_positive_cell = ff_column_mdm_prefix_mdr_secondwavezeroevaluationdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_secondwavezeroevaluationdeterminanthscm_positive_cell_column_after. ff_gap_mdm_le_mdr_secondwavezeroevaluationdeterminanthscm_positive_cell_column_after + (mdr_j_secondwavezeroevaluationdeterminanthsc) = (ff_column_mdm_prefix_mdr_secondwavezeroevaluationdeterminanthscm_positive)) /\ ff_column_mdm_cell_mdr_secondwavezeroevaluationdeterminanthscm_positive_cell = S ff_column_mdm_prefix_mdr_secondwavezeroevaluationdeterminanthscm_positive))) /\ (((exists ff_h_mdm_mdr_secondwavezeroevaluationdeterminanthscm_positive_cell_source. ff_h_mdm_mdr_secondwavezeroevaluationdeterminanthscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_secondwavezeroevaluationdeterminanthscm_positive) = S ((S ((ff_row_mdm_cell_mdr_secondwavezeroevaluationdeterminanthscm_positive_cell) * (S (mdr_q_secondwavezeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_secondwavezeroevaluationdeterminanthscm_positive_cell))) * mdr_pc_secondwavezeroevaluationdeterminanth)) /\ exists ff_q_mdm_mdr_secondwavezeroevaluationdeterminanthscm_positive_cell_source. mdr_pb_secondwavezeroevaluationdeterminanth = ff_q_mdm_mdr_secondwavezeroevaluationdeterminanthscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_secondwavezeroevaluationdeterminanthscm_positive_cell) * (S (mdr_q_secondwavezeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_secondwavezeroevaluationdeterminanthscm_positive_cell))) * mdr_pc_secondwavezeroevaluationdeterminanth) + (ff_value_mdm_prefix_mdr_secondwavezeroevaluationdeterminanthscm_positive)))))) /\ (((exists ff_h_mdm_mdr_secondwavezeroevaluationdeterminanthscm_positive_target. ff_h_mdm_mdr_secondwavezeroevaluationdeterminanthscm_positive_target + S (ff_value_mdm_prefix_mdr_secondwavezeroevaluationdeterminanthscm_positive) = S ((S (ff_index_mdm_prefix_mdr_secondwavezeroevaluationdeterminanthscm_positive)) * mdr_us_secondwavezeroevaluationdeterminanthsc)) /\ exists ff_q_mdm_mdr_secondwavezeroevaluationdeterminanthscm_positive_target. mdr_up_secondwavezeroevaluationdeterminanthsc = ff_q_mdm_mdr_secondwavezeroevaluationdeterminanthscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_secondwavezeroevaluationdeterminanthscm_positive)) * mdr_us_secondwavezeroevaluationdeterminanthsc) + (ff_value_mdm_prefix_mdr_secondwavezeroevaluationdeterminanthscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_secondwavezeroevaluationdeterminanthscm_negative. (exists ff_gap_mdm_lt_mdr_secondwavezeroevaluationdeterminanthscm_negative_index_bound. ff_gap_mdm_lt_mdr_secondwavezeroevaluationdeterminanthscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_secondwavezeroevaluationdeterminanthscm_negative) = ((mdr_q_secondwavezeroevaluationdeterminanths) * (mdr_q_secondwavezeroevaluationdeterminanths))) -> exists ff_row_mdm_prefix_mdr_secondwavezeroevaluationdeterminanthscm_negative ff_column_mdm_prefix_mdr_secondwavezeroevaluationdeterminanthscm_negative ff_value_mdm_prefix_mdr_secondwavezeroevaluationdeterminanthscm_negative. (ff_index_mdm_prefix_mdr_secondwavezeroevaluationdeterminanthscm_negative = (mdr_q_secondwavezeroevaluationdeterminanths) * ff_row_mdm_prefix_mdr_secondwavezeroevaluationdeterminanthscm_negative + ff_column_mdm_prefix_mdr_secondwavezeroevaluationdeterminanthscm_negative /\ ((exists ff_gap_mdm_lt_mdr_secondwavezeroevaluationdeterminanthscm_negative_column_bound. ff_gap_mdm_lt_mdr_secondwavezeroevaluationdeterminanthscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_secondwavezeroevaluationdeterminanthscm_negative) = (mdr_q_secondwavezeroevaluationdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_secondwavezeroevaluationdeterminanthscm_negative_cell ff_column_mdm_cell_mdr_secondwavezeroevaluationdeterminanthscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_secondwavezeroevaluationdeterminanthscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_secondwavezeroevaluationdeterminanthscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_secondwavezeroevaluationdeterminanthscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_secondwavezeroevaluationdeterminanthscm_negative_cell = ff_row_mdm_prefix_mdr_secondwavezeroevaluationdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_secondwavezeroevaluationdeterminanthscm_negative_cell_row_after. ff_gap_mdm_le_mdr_secondwavezeroevaluationdeterminanthscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_secondwavezeroevaluationdeterminanthscm_negative)) /\ ff_row_mdm_cell_mdr_secondwavezeroevaluationdeterminanthscm_negative_cell = S ff_row_mdm_prefix_mdr_secondwavezeroevaluationdeterminanthscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_secondwavezeroevaluationdeterminanthscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_secondwavezeroevaluationdeterminanthscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_secondwavezeroevaluationdeterminanthscm_negative) = (mdr_j_secondwavezeroevaluationdeterminanthsc)) /\ ff_column_mdm_cell_mdr_secondwavezeroevaluationdeterminanthscm_negative_cell = ff_column_mdm_prefix_mdr_secondwavezeroevaluationdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_secondwavezeroevaluationdeterminanthscm_negative_cell_column_after. ff_gap_mdm_le_mdr_secondwavezeroevaluationdeterminanthscm_negative_cell_column_after + (mdr_j_secondwavezeroevaluationdeterminanthsc) = (ff_column_mdm_prefix_mdr_secondwavezeroevaluationdeterminanthscm_negative)) /\ ff_column_mdm_cell_mdr_secondwavezeroevaluationdeterminanthscm_negative_cell = S ff_column_mdm_prefix_mdr_secondwavezeroevaluationdeterminanthscm_negative))) /\ (((exists ff_h_mdm_mdr_secondwavezeroevaluationdeterminanthscm_negative_cell_source. ff_h_mdm_mdr_secondwavezeroevaluationdeterminanthscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_secondwavezeroevaluationdeterminanthscm_negative) = S ((S ((ff_row_mdm_cell_mdr_secondwavezeroevaluationdeterminanthscm_negative_cell) * (S (mdr_q_secondwavezeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_secondwavezeroevaluationdeterminanthscm_negative_cell))) * mdr_nc_secondwavezeroevaluationdeterminanth)) /\ exists ff_q_mdm_mdr_secondwavezeroevaluationdeterminanthscm_negative_cell_source. mdr_nb_secondwavezeroevaluationdeterminanth = ff_q_mdm_mdr_secondwavezeroevaluationdeterminanthscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_secondwavezeroevaluationdeterminanthscm_negative_cell) * (S (mdr_q_secondwavezeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_secondwavezeroevaluationdeterminanthscm_negative_cell))) * mdr_nc_secondwavezeroevaluationdeterminanth) + (ff_value_mdm_prefix_mdr_secondwavezeroevaluationdeterminanthscm_negative)))))) /\ (((exists ff_h_mdm_mdr_secondwavezeroevaluationdeterminanthscm_negative_target. ff_h_mdm_mdr_secondwavezeroevaluationdeterminanthscm_negative_target + S (ff_value_mdm_prefix_mdr_secondwavezeroevaluationdeterminanthscm_negative) = S ((S (ff_index_mdm_prefix_mdr_secondwavezeroevaluationdeterminanthscm_negative)) * mdr_ut_secondwavezeroevaluationdeterminanthsc)) /\ exists ff_q_mdm_mdr_secondwavezeroevaluationdeterminanthscm_negative_target. mdr_un_secondwavezeroevaluationdeterminanthsc = ff_q_mdm_mdr_secondwavezeroevaluationdeterminanthscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_secondwavezeroevaluationdeterminanthscm_negative)) * mdr_ut_secondwavezeroevaluationdeterminanthsc) + (ff_value_mdm_prefix_mdr_secondwavezeroevaluationdeterminanthscm_negative))))))))) /\ ((((exists ff_h_mdr_secondwavezeroevaluationdeterminanthscp. ff_h_mdr_secondwavezeroevaluationdeterminanthscp + S (mdr_p_secondwavezeroevaluationdeterminanthsc) = S ((S (mdr_j_secondwavezeroevaluationdeterminanthsc)) * mdr_ec_secondwavezeroevaluationdeterminanths)) /\ exists ff_q_mdr_secondwavezeroevaluationdeterminanthscp. mdr_eb_secondwavezeroevaluationdeterminanths = ff_q_mdr_secondwavezeroevaluationdeterminanthscp * S ((S (mdr_j_secondwavezeroevaluationdeterminanthsc)) * mdr_ec_secondwavezeroevaluationdeterminanths) + (mdr_p_secondwavezeroevaluationdeterminanthsc))) /\ (((exists ff_h_mdr_secondwavezeroevaluationdeterminanthscn. ff_h_mdr_secondwavezeroevaluationdeterminanthscn + S (mdr_n_secondwavezeroevaluationdeterminanthsc) = S ((S (mdr_j_secondwavezeroevaluationdeterminanthsc)) * mdr_fc_secondwavezeroevaluationdeterminanths)) /\ exists ff_q_mdr_secondwavezeroevaluationdeterminanthscn. mdr_fb_secondwavezeroevaluationdeterminanths = ff_q_mdr_secondwavezeroevaluationdeterminanthscn * S ((S (mdr_j_secondwavezeroevaluationdeterminanthsc)) * mdr_fc_secondwavezeroevaluationdeterminanths) + (mdr_n_secondwavezeroevaluationdeterminanthsc)))))))) /\ (exists ff_ub_mce_fold_mdr_secondwavezeroevaluationdeterminanthsf ff_uc_mce_fold_mdr_secondwavezeroevaluationdeterminanthsf ff_vb_mce_fold_mdr_secondwavezeroevaluationdeterminanthsf ff_vc_mce_fold_mdr_secondwavezeroevaluationdeterminanthsf. ((forall ff_index_mce_alternating_mdr_secondwavezeroevaluationdeterminanthsf_prefix. (exists ff_gap_mce_mdr_secondwavezeroevaluationdeterminanthsf_prefix_index. ff_gap_mce_mdr_secondwavezeroevaluationdeterminanthsf_prefix_index + S (ff_index_mce_alternating_mdr_secondwavezeroevaluationdeterminanthsf_prefix) = (S (mdr_q_secondwavezeroevaluationdeterminanths))) -> exists ff_ap_mce_alternating_mdr_secondwavezeroevaluationdeterminanthsf_prefix ff_an_mce_alternating_mdr_secondwavezeroevaluationdeterminanthsf_prefix ff_bp_mce_alternating_mdr_secondwavezeroevaluationdeterminanthsf_prefix ff_bn_mce_alternating_mdr_secondwavezeroevaluationdeterminanthsf_prefix ff_p_mce_alternating_mdr_secondwavezeroevaluationdeterminanthsf_prefix ff_n_mce_alternating_mdr_secondwavezeroevaluationdeterminanthsf_prefix. ((((exists ff_h_mce_mdr_secondwavezeroevaluationdeterminanthsf_prefix_ap. ff_h_mce_mdr_secondwavezeroevaluationdeterminanthsf_prefix_ap + S (ff_ap_mce_alternating_mdr_secondwavezeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_secondwavezeroevaluationdeterminanthsf_prefix)) * mdr_pc_secondwavezeroevaluationdeterminanth)) /\ exists ff_q_mce_mdr_secondwavezeroevaluationdeterminanthsf_prefix_ap. mdr_pb_secondwavezeroevaluationdeterminanth = ff_q_mce_mdr_secondwavezeroevaluationdeterminanthsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_secondwavezeroevaluationdeterminanthsf_prefix)) * mdr_pc_secondwavezeroevaluationdeterminanth) + (ff_ap_mce_alternating_mdr_secondwavezeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_secondwavezeroevaluationdeterminanthsf_prefix_an. ff_h_mce_mdr_secondwavezeroevaluationdeterminanthsf_prefix_an + S (ff_an_mce_alternating_mdr_secondwavezeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_secondwavezeroevaluationdeterminanthsf_prefix)) * mdr_nc_secondwavezeroevaluationdeterminanth)) /\ exists ff_q_mce_mdr_secondwavezeroevaluationdeterminanthsf_prefix_an. mdr_nb_secondwavezeroevaluationdeterminanth = ff_q_mce_mdr_secondwavezeroevaluationdeterminanthsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_secondwavezeroevaluationdeterminanthsf_prefix)) * mdr_nc_secondwavezeroevaluationdeterminanth) + (ff_an_mce_alternating_mdr_secondwavezeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_secondwavezeroevaluationdeterminanthsf_prefix_bp. ff_h_mce_mdr_secondwavezeroevaluationdeterminanthsf_prefix_bp + S (ff_bp_mce_alternating_mdr_secondwavezeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_secondwavezeroevaluationdeterminanthsf_prefix)) * mdr_ec_secondwavezeroevaluationdeterminanths)) /\ exists ff_q_mce_mdr_secondwavezeroevaluationdeterminanthsf_prefix_bp. mdr_eb_secondwavezeroevaluationdeterminanths = ff_q_mce_mdr_secondwavezeroevaluationdeterminanthsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_secondwavezeroevaluationdeterminanthsf_prefix)) * mdr_ec_secondwavezeroevaluationdeterminanths) + (ff_bp_mce_alternating_mdr_secondwavezeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_secondwavezeroevaluationdeterminanthsf_prefix_bn. ff_h_mce_mdr_secondwavezeroevaluationdeterminanthsf_prefix_bn + S (ff_bn_mce_alternating_mdr_secondwavezeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_secondwavezeroevaluationdeterminanthsf_prefix)) * mdr_fc_secondwavezeroevaluationdeterminanths)) /\ exists ff_q_mce_mdr_secondwavezeroevaluationdeterminanthsf_prefix_bn. mdr_fb_secondwavezeroevaluationdeterminanths = ff_q_mce_mdr_secondwavezeroevaluationdeterminanthsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_secondwavezeroevaluationdeterminanthsf_prefix)) * mdr_fc_secondwavezeroevaluationdeterminanths) + (ff_bn_mce_alternating_mdr_secondwavezeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_secondwavezeroevaluationdeterminanthsf_prefix_positive. ff_h_mce_mdr_secondwavezeroevaluationdeterminanthsf_prefix_positive + S (ff_p_mce_alternating_mdr_secondwavezeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_secondwavezeroevaluationdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_secondwavezeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_secondwavezeroevaluationdeterminanthsf_prefix_positive. ff_ub_mce_fold_mdr_secondwavezeroevaluationdeterminanthsf = ff_q_mce_mdr_secondwavezeroevaluationdeterminanthsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_secondwavezeroevaluationdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_secondwavezeroevaluationdeterminanthsf) + (ff_p_mce_alternating_mdr_secondwavezeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_secondwavezeroevaluationdeterminanthsf_prefix_negative. ff_h_mce_mdr_secondwavezeroevaluationdeterminanthsf_prefix_negative + S (ff_n_mce_alternating_mdr_secondwavezeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_secondwavezeroevaluationdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_secondwavezeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_secondwavezeroevaluationdeterminanthsf_prefix_negative. ff_vb_mce_fold_mdr_secondwavezeroevaluationdeterminanthsf = ff_q_mce_mdr_secondwavezeroevaluationdeterminanthsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_secondwavezeroevaluationdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_secondwavezeroevaluationdeterminanthsf) + (ff_n_mce_alternating_mdr_secondwavezeroevaluationdeterminanthsf_prefix))) /\ (((exists ff_even_mce_term_mdr_secondwavezeroevaluationdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_secondwavezeroevaluationdeterminanthsf_prefix = 2 * ff_even_mce_term_mdr_secondwavezeroevaluationdeterminanthsf_prefix_term) /\ (ff_p_mce_alternating_mdr_secondwavezeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_secondwavezeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_secondwavezeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_secondwavezeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_secondwavezeroevaluationdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_secondwavezeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_secondwavezeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_secondwavezeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_secondwavezeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_secondwavezeroevaluationdeterminanthsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_secondwavezeroevaluationdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_secondwavezeroevaluationdeterminanthsf_prefix = 2 * ff_odd_mce_term_mdr_secondwavezeroevaluationdeterminanthsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_secondwavezeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_secondwavezeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_secondwavezeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_secondwavezeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_secondwavezeroevaluationdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_secondwavezeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_secondwavezeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_secondwavezeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_secondwavezeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_secondwavezeroevaluationdeterminanthsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_secondwavezeroevaluationdeterminanthsf_positive ff_v_mce_mdr_secondwavezeroevaluationdeterminanthsf_positive. ((((exists ff_h_mce_mdr_secondwavezeroevaluationdeterminanthsf_positive_start. ff_h_mce_mdr_secondwavezeroevaluationdeterminanthsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_secondwavezeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_secondwavezeroevaluationdeterminanthsf_positive_start. ff_u_mce_mdr_secondwavezeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_secondwavezeroevaluationdeterminanthsf_positive_start * S ((S (0)) * ff_v_mce_mdr_secondwavezeroevaluationdeterminanthsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_secondwavezeroevaluationdeterminanthsf_positive_terminal. ff_h_mce_mdr_secondwavezeroevaluationdeterminanthsf_positive_terminal + S (mdr_p_secondwavezeroevaluationdeterminanth) = S ((S ((S (mdr_q_secondwavezeroevaluationdeterminanths)))) * ff_v_mce_mdr_secondwavezeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_secondwavezeroevaluationdeterminanthsf_positive_terminal. ff_u_mce_mdr_secondwavezeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_secondwavezeroevaluationdeterminanthsf_positive_terminal * S ((S ((S (mdr_q_secondwavezeroevaluationdeterminanths)))) * ff_v_mce_mdr_secondwavezeroevaluationdeterminanthsf_positive) + (mdr_p_secondwavezeroevaluationdeterminanth))) /\ forall ff_i_mce_mdr_secondwavezeroevaluationdeterminanthsf_positive. (exists ff_lt_mce_mdr_secondwavezeroevaluationdeterminanthsf_positive_bound. ff_lt_mce_mdr_secondwavezeroevaluationdeterminanthsf_positive_bound + S ff_i_mce_mdr_secondwavezeroevaluationdeterminanthsf_positive = (S (mdr_q_secondwavezeroevaluationdeterminanths))) -> exists ff_a_mce_mdr_secondwavezeroevaluationdeterminanthsf_positive ff_r_mce_mdr_secondwavezeroevaluationdeterminanthsf_positive ff_s_mce_mdr_secondwavezeroevaluationdeterminanthsf_positive. ((((exists ff_h_mce_mdr_secondwavezeroevaluationdeterminanthsf_positive_summand. ff_h_mce_mdr_secondwavezeroevaluationdeterminanthsf_positive_summand + S (ff_a_mce_mdr_secondwavezeroevaluationdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_secondwavezeroevaluationdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_secondwavezeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_secondwavezeroevaluationdeterminanthsf_positive_summand. ff_ub_mce_fold_mdr_secondwavezeroevaluationdeterminanthsf = ff_q_mce_mdr_secondwavezeroevaluationdeterminanthsf_positive_summand * S ((S (ff_i_mce_mdr_secondwavezeroevaluationdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_secondwavezeroevaluationdeterminanthsf) + (ff_a_mce_mdr_secondwavezeroevaluationdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_secondwavezeroevaluationdeterminanthsf_positive_partial. ff_h_mce_mdr_secondwavezeroevaluationdeterminanthsf_positive_partial + S (ff_r_mce_mdr_secondwavezeroevaluationdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_secondwavezeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_secondwavezeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_secondwavezeroevaluationdeterminanthsf_positive_partial. ff_u_mce_mdr_secondwavezeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_secondwavezeroevaluationdeterminanthsf_positive_partial * S ((S (ff_i_mce_mdr_secondwavezeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_secondwavezeroevaluationdeterminanthsf_positive) + (ff_r_mce_mdr_secondwavezeroevaluationdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_secondwavezeroevaluationdeterminanthsf_positive_successor. ff_h_mce_mdr_secondwavezeroevaluationdeterminanthsf_positive_successor + S (ff_s_mce_mdr_secondwavezeroevaluationdeterminanthsf_positive) = S ((S (S ff_i_mce_mdr_secondwavezeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_secondwavezeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_secondwavezeroevaluationdeterminanthsf_positive_successor. ff_u_mce_mdr_secondwavezeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_secondwavezeroevaluationdeterminanthsf_positive_successor * S ((S (S ff_i_mce_mdr_secondwavezeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_secondwavezeroevaluationdeterminanthsf_positive) + (ff_s_mce_mdr_secondwavezeroevaluationdeterminanthsf_positive))) /\ ff_s_mce_mdr_secondwavezeroevaluationdeterminanthsf_positive = ff_r_mce_mdr_secondwavezeroevaluationdeterminanthsf_positive + ff_a_mce_mdr_secondwavezeroevaluationdeterminanthsf_positive)))))) /\ (exists ff_u_mce_mdr_secondwavezeroevaluationdeterminanthsf_negative ff_v_mce_mdr_secondwavezeroevaluationdeterminanthsf_negative. ((((exists ff_h_mce_mdr_secondwavezeroevaluationdeterminanthsf_negative_start. ff_h_mce_mdr_secondwavezeroevaluationdeterminanthsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_secondwavezeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_secondwavezeroevaluationdeterminanthsf_negative_start. ff_u_mce_mdr_secondwavezeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_secondwavezeroevaluationdeterminanthsf_negative_start * S ((S (0)) * ff_v_mce_mdr_secondwavezeroevaluationdeterminanthsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_secondwavezeroevaluationdeterminanthsf_negative_terminal. ff_h_mce_mdr_secondwavezeroevaluationdeterminanthsf_negative_terminal + S (mdr_n_secondwavezeroevaluationdeterminanth) = S ((S ((S (mdr_q_secondwavezeroevaluationdeterminanths)))) * ff_v_mce_mdr_secondwavezeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_secondwavezeroevaluationdeterminanthsf_negative_terminal. ff_u_mce_mdr_secondwavezeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_secondwavezeroevaluationdeterminanthsf_negative_terminal * S ((S ((S (mdr_q_secondwavezeroevaluationdeterminanths)))) * ff_v_mce_mdr_secondwavezeroevaluationdeterminanthsf_negative) + (mdr_n_secondwavezeroevaluationdeterminanth))) /\ forall ff_i_mce_mdr_secondwavezeroevaluationdeterminanthsf_negative. (exists ff_lt_mce_mdr_secondwavezeroevaluationdeterminanthsf_negative_bound. ff_lt_mce_mdr_secondwavezeroevaluationdeterminanthsf_negative_bound + S ff_i_mce_mdr_secondwavezeroevaluationdeterminanthsf_negative = (S (mdr_q_secondwavezeroevaluationdeterminanths))) -> exists ff_a_mce_mdr_secondwavezeroevaluationdeterminanthsf_negative ff_r_mce_mdr_secondwavezeroevaluationdeterminanthsf_negative ff_s_mce_mdr_secondwavezeroevaluationdeterminanthsf_negative. ((((exists ff_h_mce_mdr_secondwavezeroevaluationdeterminanthsf_negative_summand. ff_h_mce_mdr_secondwavezeroevaluationdeterminanthsf_negative_summand + S (ff_a_mce_mdr_secondwavezeroevaluationdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_secondwavezeroevaluationdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_secondwavezeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_secondwavezeroevaluationdeterminanthsf_negative_summand. ff_vb_mce_fold_mdr_secondwavezeroevaluationdeterminanthsf = ff_q_mce_mdr_secondwavezeroevaluationdeterminanthsf_negative_summand * S ((S (ff_i_mce_mdr_secondwavezeroevaluationdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_secondwavezeroevaluationdeterminanthsf) + (ff_a_mce_mdr_secondwavezeroevaluationdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_secondwavezeroevaluationdeterminanthsf_negative_partial. ff_h_mce_mdr_secondwavezeroevaluationdeterminanthsf_negative_partial + S (ff_r_mce_mdr_secondwavezeroevaluationdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_secondwavezeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_secondwavezeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_secondwavezeroevaluationdeterminanthsf_negative_partial. ff_u_mce_mdr_secondwavezeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_secondwavezeroevaluationdeterminanthsf_negative_partial * S ((S (ff_i_mce_mdr_secondwavezeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_secondwavezeroevaluationdeterminanthsf_negative) + (ff_r_mce_mdr_secondwavezeroevaluationdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_secondwavezeroevaluationdeterminanthsf_negative_successor. ff_h_mce_mdr_secondwavezeroevaluationdeterminanthsf_negative_successor + S (ff_s_mce_mdr_secondwavezeroevaluationdeterminanthsf_negative) = S ((S (S ff_i_mce_mdr_secondwavezeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_secondwavezeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_secondwavezeroevaluationdeterminanthsf_negative_successor. ff_u_mce_mdr_secondwavezeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_secondwavezeroevaluationdeterminanthsf_negative_successor * S ((S (S ff_i_mce_mdr_secondwavezeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_secondwavezeroevaluationdeterminanthsf_negative) + (ff_s_mce_mdr_secondwavezeroevaluationdeterminanthsf_negative))) /\ ff_s_mce_mdr_secondwavezeroevaluationdeterminanthsf_negative = ff_r_mce_mdr_secondwavezeroevaluationdeterminanthsf_negative + ff_a_mce_mdr_secondwavezeroevaluationdeterminanthsf_negative))))))))))))))) /\ ((exists mdr_gap_secondwavezeroevaluationdeterminanti. mdr_gap_secondwavezeroevaluationdeterminanti + S (mdr_i_secondwavezeroevaluationdeterminant) = (mdr_l_secondwavezeroevaluationdeterminant)) /\ (exists mdr_z_secondwavezeroevaluationdeterminantr. ((exists mdr_a_secondwavezeroevaluationdeterminantrc mdr_b_secondwavezeroevaluationdeterminantrc mdr_c_secondwavezeroevaluationdeterminantrc mdr_e_secondwavezeroevaluationdeterminantrc mdr_f_secondwavezeroevaluationdeterminantrc. ((mdr_a_secondwavezeroevaluationdeterminantrc = ((mdr_q_secondwave) + (mdr_ub_secondwavezeroevaluation)) * S ((mdr_q_secondwave) + (mdr_ub_secondwavezeroevaluation)) + ((mdr_ub_secondwavezeroevaluation) + (mdr_ub_secondwavezeroevaluation))) /\ ((mdr_b_secondwavezeroevaluationdeterminantrc = ((mdr_uc_secondwavezeroevaluation) + (mdr_vb_secondwavezeroevaluation)) * S ((mdr_uc_secondwavezeroevaluation) + (mdr_vb_secondwavezeroevaluation)) + ((mdr_vb_secondwavezeroevaluation) + (mdr_vb_secondwavezeroevaluation))) /\ ((mdr_c_secondwavezeroevaluationdeterminantrc = ((mdr_a_secondwavezeroevaluationdeterminantrc) + (mdr_b_secondwavezeroevaluationdeterminantrc)) * S ((mdr_a_secondwavezeroevaluationdeterminantrc) + (mdr_b_secondwavezeroevaluationdeterminantrc)) + ((mdr_b_secondwavezeroevaluationdeterminantrc) + (mdr_b_secondwavezeroevaluationdeterminantrc))) /\ ((mdr_e_secondwavezeroevaluationdeterminantrc = ((mdr_p_secondwavezero) + (mdr_n_secondwavezero)) * S ((mdr_p_secondwavezero) + (mdr_n_secondwavezero)) + ((mdr_n_secondwavezero) + (mdr_n_secondwavezero))) /\ ((mdr_f_secondwavezeroevaluationdeterminantrc = ((mdr_vc_secondwavezeroevaluation) + (mdr_e_secondwavezeroevaluationdeterminantrc)) * S ((mdr_vc_secondwavezeroevaluation) + (mdr_e_secondwavezeroevaluationdeterminantrc)) + ((mdr_e_secondwavezeroevaluationdeterminantrc) + (mdr_e_secondwavezeroevaluationdeterminantrc))) /\ ((mdr_z_secondwavezeroevaluationdeterminantr) = ((mdr_c_secondwavezeroevaluationdeterminantrc) + (mdr_f_secondwavezeroevaluationdeterminantrc)) * S ((mdr_c_secondwavezeroevaluationdeterminantrc) + (mdr_f_secondwavezeroevaluationdeterminantrc)) + ((mdr_f_secondwavezeroevaluationdeterminantrc) + (mdr_f_secondwavezeroevaluationdeterminantrc))))))))) /\ (((exists ff_h_mdr_secondwavezeroevaluationdeterminantrb. ff_h_mdr_secondwavezeroevaluationdeterminantrb + S (mdr_z_secondwavezeroevaluationdeterminantr) = S ((S (mdr_i_secondwavezeroevaluationdeterminant)) * mdr_c_secondwavezeroevaluationdeterminant)) /\ exists ff_q_mdr_secondwavezeroevaluationdeterminantrb. mdr_b_secondwavezeroevaluationdeterminant = ff_q_mdr_secondwavezeroevaluationdeterminantrb * S ((S (mdr_i_secondwavezeroevaluationdeterminant)) * mdr_c_secondwavezeroevaluationdeterminant) + (mdr_z_secondwavezeroevaluationdeterminantr)))))))))) -> mdr_p_secondwavezero = mdr_n_secondwavezero)))))The unchanged native kernel never receives this surface symbol. Binder-safe expansion produces only its existing first-order syntax.
Direct definition dependencies
Definitions depending on this notation
none
Checked theorems using this definition
DL005E · rectangular_matrix_rank_certificate_existsDL005F · rectangular_matrix_rank_functionalDL0060 · rectangular_matrix_rank_exists_uniqueDL0061 · rectangular_matrix_rank_successor_minors_zeroDL0062 · rectangular_matrix_rank_zero_rowsDL0063 · rectangular_matrix_rank_zero_columnsDL009E · rectangular_matrix_rank_integer_transportDL009F · rectangular_matrix_rank_integer_invariantDL00B3 · square_matrix_full_rank_from_nonzero_determinantDL00B4 · positive_determinant_matrix_data_full_rank