rectangular_matrix_rank_functional

forall pb pc nb nc r w rank other. (((exists mdr_gap_first_rankrows_bound. mdr_gap_first_rankrows_bound + (rank) = (r)) /\ ((exists mdr_gap_first_rankcolumns_bound. mdr_gap_first_rankcolumns_bound + (rank) = (w)) /\ ((exists mdr_rb_first_rankwitness mdr_rc_first_rankwitness mdr_cb_first_rankwitness mdr_cc_first_rankwitness. (((((forall fom_index_mrf_first_rankwitnessminorrowsbound. (exists fom_gap_mrf_first_rankwitnessminorrowsbound_index_bound. fom_gap_mrf_first_rankwitnessminorrowsbound_index_bound + S (fom_index_mrf_first_rankwitnessminorrowsbound) = rank) -> exists fom_value_mrf_first_rankwitnessminorrowsbound. ((((exists fom_beta_height_mrf_first_rankwitnessminorrowsbound_entry. fom_beta_height_mrf_first_rankwitnessminorrowsbound_entry + S (fom_value_mrf_first_rankwitnessminorrowsbound) = S ((S (fom_index_mrf_first_rankwitnessminorrowsbound)) * mdr_rc_first_rankwitness)) /\ exists fom_beta_quotient_mrf_first_rankwitnessminorrowsbound_entry. mdr_rb_first_rankwitness = fom_beta_quotient_mrf_first_rankwitnessminorrowsbound_entry * S ((S (fom_index_mrf_first_rankwitnessminorrowsbound)) * mdr_rc_first_rankwitness) + (fom_value_mrf_first_rankwitnessminorrowsbound))) /\ (exists fom_gap_mrf_first_rankwitnessminorrowsbound_value_bound. fom_gap_mrf_first_rankwitnessminorrowsbound_value_bound + S (fom_value_mrf_first_rankwitnessminorrowsbound) = r))) /\ (forall mdr_i_first_rankwitnessminorrowsdistinct mdr_j_first_rankwitnessminorrowsdistinct mdr_a_first_rankwitnessminorrowsdistinct. (exists mdr_gap_first_rankwitnessminorrowsdistincti. mdr_gap_first_rankwitnessminorrowsdistincti + S (mdr_i_first_rankwitnessminorrowsdistinct) = (rank)) -> (exists mdr_gap_first_rankwitnessminorrowsdistinctj. mdr_gap_first_rankwitnessminorrowsdistinctj + S (mdr_j_first_rankwitnessminorrowsdistinct) = (rank)) -> (((exists ff_h_mdr_first_rankwitnessminorrowsdistinctfirst. ff_h_mdr_first_rankwitnessminorrowsdistinctfirst + S (mdr_a_first_rankwitnessminorrowsdistinct) = S ((S (mdr_i_first_rankwitnessminorrowsdistinct)) * mdr_rc_first_rankwitness)) /\ exists ff_q_mdr_first_rankwitnessminorrowsdistinctfirst. mdr_rb_first_rankwitness = ff_q_mdr_first_rankwitnessminorrowsdistinctfirst * S ((S (mdr_i_first_rankwitnessminorrowsdistinct)) * mdr_rc_first_rankwitness) + (mdr_a_first_rankwitnessminorrowsdistinct))) -> (((exists ff_h_mdr_first_rankwitnessminorrowsdistinctsecond. ff_h_mdr_first_rankwitnessminorrowsdistinctsecond + S (mdr_a_first_rankwitnessminorrowsdistinct) = S ((S (mdr_j_first_rankwitnessminorrowsdistinct)) * mdr_rc_first_rankwitness)) /\ exists ff_q_mdr_first_rankwitnessminorrowsdistinctsecond. mdr_rb_first_rankwitness = ff_q_mdr_first_rankwitnessminorrowsdistinctsecond * S ((S (mdr_j_first_rankwitnessminorrowsdistinct)) * mdr_rc_first_rankwitness) + (mdr_a_first_rankwitnessminorrowsdistinct))) -> mdr_i_first_rankwitnessminorrowsdistinct = mdr_j_first_rankwitnessminorrowsdistinct))) /\ ((((forall fom_index_mrf_first_rankwitnessminorcolumnsbound. (exists fom_gap_mrf_first_rankwitnessminorcolumnsbound_index_bound. fom_gap_mrf_first_rankwitnessminorcolumnsbound_index_bound + S (fom_index_mrf_first_rankwitnessminorcolumnsbound) = rank) -> exists fom_value_mrf_first_rankwitnessminorcolumnsbound. ((((exists fom_beta_height_mrf_first_rankwitnessminorcolumnsbound_entry. fom_beta_height_mrf_first_rankwitnessminorcolumnsbound_entry + S (fom_value_mrf_first_rankwitnessminorcolumnsbound) = S ((S (fom_index_mrf_first_rankwitnessminorcolumnsbound)) * mdr_cc_first_rankwitness)) /\ exists fom_beta_quotient_mrf_first_rankwitnessminorcolumnsbound_entry. mdr_cb_first_rankwitness = fom_beta_quotient_mrf_first_rankwitnessminorcolumnsbound_entry * S ((S (fom_index_mrf_first_rankwitnessminorcolumnsbound)) * mdr_cc_first_rankwitness) + (fom_value_mrf_first_rankwitnessminorcolumnsbound))) /\ (exists fom_gap_mrf_first_rankwitnessminorcolumnsbound_value_bound. fom_gap_mrf_first_rankwitnessminorcolumnsbound_value_bound + S (fom_value_mrf_first_rankwitnessminorcolumnsbound) = w))) /\ (forall mdr_i_first_rankwitnessminorcolumnsdistinct mdr_j_first_rankwitnessminorcolumnsdistinct mdr_a_first_rankwitnessminorcolumnsdistinct. (exists mdr_gap_first_rankwitnessminorcolumnsdistincti. mdr_gap_first_rankwitnessminorcolumnsdistincti + S (mdr_i_first_rankwitnessminorcolumnsdistinct) = (rank)) -> (exists mdr_gap_first_rankwitnessminorcolumnsdistinctj. mdr_gap_first_rankwitnessminorcolumnsdistinctj + S (mdr_j_first_rankwitnessminorcolumnsdistinct) = (rank)) -> (((exists ff_h_mdr_first_rankwitnessminorcolumnsdistinctfirst. ff_h_mdr_first_rankwitnessminorcolumnsdistinctfirst + S (mdr_a_first_rankwitnessminorcolumnsdistinct) = S ((S (mdr_i_first_rankwitnessminorcolumnsdistinct)) * mdr_cc_first_rankwitness)) /\ exists ff_q_mdr_first_rankwitnessminorcolumnsdistinctfirst. mdr_cb_first_rankwitness = ff_q_mdr_first_rankwitnessminorcolumnsdistinctfirst * S ((S (mdr_i_first_rankwitnessminorcolumnsdistinct)) * mdr_cc_first_rankwitness) + (mdr_a_first_rankwitnessminorcolumnsdistinct))) -> (((exists ff_h_mdr_first_rankwitnessminorcolumnsdistinctsecond. ff_h_mdr_first_rankwitnessminorcolumnsdistinctsecond + S (mdr_a_first_rankwitnessminorcolumnsdistinct) = S ((S (mdr_j_first_rankwitnessminorcolumnsdistinct)) * mdr_cc_first_rankwitness)) /\ exists ff_q_mdr_first_rankwitnessminorcolumnsdistinctsecond. mdr_cb_first_rankwitness = ff_q_mdr_first_rankwitnessminorcolumnsdistinctsecond * S ((S (mdr_j_first_rankwitnessminorcolumnsdistinct)) * mdr_cc_first_rankwitness) + (mdr_a_first_rankwitnessminorcolumnsdistinct))) -> mdr_i_first_rankwitnessminorcolumnsdistinct = mdr_j_first_rankwitnessminorcolumnsdistinct))) /\ (exists mdr_p_first_rankwitnessminornonzero mdr_n_first_rankwitnessminornonzero. ((exists mdr_ub_first_rankwitnessminornonzeroevaluation mdr_uc_first_rankwitnessminornonzeroevaluation mdr_vb_first_rankwitnessminornonzeroevaluation mdr_vc_first_rankwitnessminornonzeroevaluation. ((((forall mdr_i_first_rankwitnessminornonzeroevaluationmatrixpositive. (exists mdr_gap_first_rankwitnessminornonzeroevaluationmatrixpositivebound. mdr_gap_first_rankwitnessminornonzeroevaluationmatrixpositivebound + S (mdr_i_first_rankwitnessminornonzeroevaluationmatrixpositive) = ((rank) * (rank))) -> exists mdr_a_first_rankwitnessminornonzeroevaluationmatrixpositive. (((exists mdr_r_first_rankwitnessminornonzeroevaluationmatrixpositivepoint mdr_s_first_rankwitnessminornonzeroevaluationmatrixpositivepoint mdr_u_first_rankwitnessminornonzeroevaluationmatrixpositivepoint mdr_v_first_rankwitnessminornonzeroevaluationmatrixpositivepoint. ((mdr_i_first_rankwitnessminornonzeroevaluationmatrixpositive = (rank) * mdr_r_first_rankwitnessminornonzeroevaluationmatrixpositivepoint + mdr_s_first_rankwitnessminornonzeroevaluationmatrixpositivepoint) /\ ((exists mdr_gap_first_rankwitnessminornonzeroevaluationmatrixpositivepointcolumn. mdr_gap_first_rankwitnessminornonzeroevaluationmatrixpositivepointcolumn + S (mdr_s_first_rankwitnessminornonzeroevaluationmatrixpositivepoint) = (rank)) /\ ((((exists ff_h_mdr_first_rankwitnessminornonzeroevaluationmatrixpositivepointrow_index. ff_h_mdr_first_rankwitnessminornonzeroevaluationmatrixpositivepointrow_index + S (mdr_u_first_rankwitnessminornonzeroevaluationmatrixpositivepoint) = S ((S (mdr_r_first_rankwitnessminornonzeroevaluationmatrixpositivepoint)) * mdr_rc_first_rankwitness)) /\ exists ff_q_mdr_first_rankwitnessminornonzeroevaluationmatrixpositivepointrow_index. mdr_rb_first_rankwitness = ff_q_mdr_first_rankwitnessminornonzeroevaluationmatrixpositivepointrow_index * S ((S (mdr_r_first_rankwitnessminornonzeroevaluationmatrixpositivepoint)) * mdr_rc_first_rankwitness) + (mdr_u_first_rankwitnessminornonzeroevaluationmatrixpositivepoint))) /\ ((((exists ff_h_mdr_first_rankwitnessminornonzeroevaluationmatrixpositivepointcolumn_index. ff_h_mdr_first_rankwitnessminornonzeroevaluationmatrixpositivepointcolumn_index + S (mdr_v_first_rankwitnessminornonzeroevaluationmatrixpositivepoint) = S ((S (mdr_s_first_rankwitnessminornonzeroevaluationmatrixpositivepoint)) * mdr_cc_first_rankwitness)) /\ exists ff_q_mdr_first_rankwitnessminornonzeroevaluationmatrixpositivepointcolumn_index. mdr_cb_first_rankwitness = ff_q_mdr_first_rankwitnessminornonzeroevaluationmatrixpositivepointcolumn_index * S ((S (mdr_s_first_rankwitnessminornonzeroevaluationmatrixpositivepoint)) * mdr_cc_first_rankwitness) + (mdr_v_first_rankwitnessminornonzeroevaluationmatrixpositivepoint))) /\ (((exists ff_h_mdr_first_rankwitnessminornonzeroevaluationmatrixpositivepointsource. ff_h_mdr_first_rankwitnessminornonzeroevaluationmatrixpositivepointsource + S (mdr_a_first_rankwitnessminornonzeroevaluationmatrixpositive) = S ((S ((mdr_u_first_rankwitnessminornonzeroevaluationmatrixpositivepoint) * (w) + (mdr_v_first_rankwitnessminornonzeroevaluationmatrixpositivepoint))) * pc)) /\ exists ff_q_mdr_first_rankwitnessminornonzeroevaluationmatrixpositivepointsource. pb = ff_q_mdr_first_rankwitnessminornonzeroevaluationmatrixpositivepointsource * S ((S ((mdr_u_first_rankwitnessminornonzeroevaluationmatrixpositivepoint) * (w) + (mdr_v_first_rankwitnessminornonzeroevaluationmatrixpositivepoint))) * pc) + (mdr_a_first_rankwitnessminornonzeroevaluationmatrixpositive)))))))) /\ (((exists ff_h_mdr_first_rankwitnessminornonzeroevaluationmatrixpositiveoutput. ff_h_mdr_first_rankwitnessminornonzeroevaluationmatrixpositiveoutput + S (mdr_a_first_rankwitnessminornonzeroevaluationmatrixpositive) = S ((S (mdr_i_first_rankwitnessminornonzeroevaluationmatrixpositive)) * mdr_uc_first_rankwitnessminornonzeroevaluation)) /\ exists ff_q_mdr_first_rankwitnessminornonzeroevaluationmatrixpositiveoutput. mdr_ub_first_rankwitnessminornonzeroevaluation = ff_q_mdr_first_rankwitnessminornonzeroevaluationmatrixpositiveoutput * S ((S (mdr_i_first_rankwitnessminornonzeroevaluationmatrixpositive)) * mdr_uc_first_rankwitnessminornonzeroevaluation) + (mdr_a_first_rankwitnessminornonzeroevaluationmatrixpositive)))))) /\ (forall mdr_i_first_rankwitnessminornonzeroevaluationmatrixnegative. (exists mdr_gap_first_rankwitnessminornonzeroevaluationmatrixnegativebound. mdr_gap_first_rankwitnessminornonzeroevaluationmatrixnegativebound + S (mdr_i_first_rankwitnessminornonzeroevaluationmatrixnegative) = ((rank) * (rank))) -> exists mdr_a_first_rankwitnessminornonzeroevaluationmatrixnegative. (((exists mdr_r_first_rankwitnessminornonzeroevaluationmatrixnegativepoint mdr_s_first_rankwitnessminornonzeroevaluationmatrixnegativepoint mdr_u_first_rankwitnessminornonzeroevaluationmatrixnegativepoint mdr_v_first_rankwitnessminornonzeroevaluationmatrixnegativepoint. ((mdr_i_first_rankwitnessminornonzeroevaluationmatrixnegative = (rank) * mdr_r_first_rankwitnessminornonzeroevaluationmatrixnegativepoint + mdr_s_first_rankwitnessminornonzeroevaluationmatrixnegativepoint) /\ ((exists mdr_gap_first_rankwitnessminornonzeroevaluationmatrixnegativepointcolumn. mdr_gap_first_rankwitnessminornonzeroevaluationmatrixnegativepointcolumn + S (mdr_s_first_rankwitnessminornonzeroevaluationmatrixnegativepoint) = (rank)) /\ ((((exists ff_h_mdr_first_rankwitnessminornonzeroevaluationmatrixnegativepointrow_index. ff_h_mdr_first_rankwitnessminornonzeroevaluationmatrixnegativepointrow_index + S (mdr_u_first_rankwitnessminornonzeroevaluationmatrixnegativepoint) = S ((S (mdr_r_first_rankwitnessminornonzeroevaluationmatrixnegativepoint)) * mdr_rc_first_rankwitness)) /\ exists ff_q_mdr_first_rankwitnessminornonzeroevaluationmatrixnegativepointrow_index. mdr_rb_first_rankwitness = ff_q_mdr_first_rankwitnessminornonzeroevaluationmatrixnegativepointrow_index * S ((S (mdr_r_first_rankwitnessminornonzeroevaluationmatrixnegativepoint)) * mdr_rc_first_rankwitness) + (mdr_u_first_rankwitnessminornonzeroevaluationmatrixnegativepoint))) /\ ((((exists ff_h_mdr_first_rankwitnessminornonzeroevaluationmatrixnegativepointcolumn_index. ff_h_mdr_first_rankwitnessminornonzeroevaluationmatrixnegativepointcolumn_index + S (mdr_v_first_rankwitnessminornonzeroevaluationmatrixnegativepoint) = S ((S (mdr_s_first_rankwitnessminornonzeroevaluationmatrixnegativepoint)) * mdr_cc_first_rankwitness)) /\ exists ff_q_mdr_first_rankwitnessminornonzeroevaluationmatrixnegativepointcolumn_index. mdr_cb_first_rankwitness = ff_q_mdr_first_rankwitnessminornonzeroevaluationmatrixnegativepointcolumn_index * S ((S (mdr_s_first_rankwitnessminornonzeroevaluationmatrixnegativepoint)) * mdr_cc_first_rankwitness) + (mdr_v_first_rankwitnessminornonzeroevaluationmatrixnegativepoint))) /\ (((exists ff_h_mdr_first_rankwitnessminornonzeroevaluationmatrixnegativepointsource. ff_h_mdr_first_rankwitnessminornonzeroevaluationmatrixnegativepointsource + S (mdr_a_first_rankwitnessminornonzeroevaluationmatrixnegative) = S ((S ((mdr_u_first_rankwitnessminornonzeroevaluationmatrixnegativepoint) * (w) + (mdr_v_first_rankwitnessminornonzeroevaluationmatrixnegativepoint))) * nc)) /\ exists ff_q_mdr_first_rankwitnessminornonzeroevaluationmatrixnegativepointsource. nb = ff_q_mdr_first_rankwitnessminornonzeroevaluationmatrixnegativepointsource * S ((S ((mdr_u_first_rankwitnessminornonzeroevaluationmatrixnegativepoint) * (w) + (mdr_v_first_rankwitnessminornonzeroevaluationmatrixnegativepoint))) * nc) + (mdr_a_first_rankwitnessminornonzeroevaluationmatrixnegative)))))))) /\ (((exists ff_h_mdr_first_rankwitnessminornonzeroevaluationmatrixnegativeoutput. ff_h_mdr_first_rankwitnessminornonzeroevaluationmatrixnegativeoutput + S (mdr_a_first_rankwitnessminornonzeroevaluationmatrixnegative) = S ((S (mdr_i_first_rankwitnessminornonzeroevaluationmatrixnegative)) * mdr_vc_first_rankwitnessminornonzeroevaluation)) /\ exists ff_q_mdr_first_rankwitnessminornonzeroevaluationmatrixnegativeoutput. mdr_vb_first_rankwitnessminornonzeroevaluation = ff_q_mdr_first_rankwitnessminornonzeroevaluationmatrixnegativeoutput * S ((S (mdr_i_first_rankwitnessminornonzeroevaluationmatrixnegative)) * mdr_vc_first_rankwitnessminornonzeroevaluation) + (mdr_a_first_rankwitnessminornonzeroevaluationmatrixnegative)))))))) /\ (exists mdr_b_first_rankwitnessminornonzeroevaluationdeterminant mdr_c_first_rankwitnessminornonzeroevaluationdeterminant mdr_l_first_rankwitnessminornonzeroevaluationdeterminant mdr_i_first_rankwitnessminornonzeroevaluationdeterminant. ((forall mdr_i_first_rankwitnessminornonzeroevaluationdeterminanth. (exists mdr_gap_first_rankwitnessminornonzeroevaluationdeterminanthi. mdr_gap_first_rankwitnessminornonzeroevaluationdeterminanthi + S (mdr_i_first_rankwitnessminornonzeroevaluationdeterminanth) = (mdr_l_first_rankwitnessminornonzeroevaluationdeterminant)) -> exists mdr_d_first_rankwitnessminornonzeroevaluationdeterminanth mdr_pb_first_rankwitnessminornonzeroevaluationdeterminanth mdr_pc_first_rankwitnessminornonzeroevaluationdeterminanth mdr_nb_first_rankwitnessminornonzeroevaluationdeterminanth mdr_nc_first_rankwitnessminornonzeroevaluationdeterminanth mdr_p_first_rankwitnessminornonzeroevaluationdeterminanth mdr_n_first_rankwitnessminornonzeroevaluationdeterminanth. ((exists mdr_z_first_rankwitnessminornonzeroevaluationdeterminanthr. ((exists mdr_a_first_rankwitnessminornonzeroevaluationdeterminanthrc mdr_b_first_rankwitnessminornonzeroevaluationdeterminanthrc mdr_c_first_rankwitnessminornonzeroevaluationdeterminanthrc mdr_e_first_rankwitnessminornonzeroevaluationdeterminanthrc mdr_f_first_rankwitnessminornonzeroevaluationdeterminanthrc. ((mdr_a_first_rankwitnessminornonzeroevaluationdeterminanthrc = ((mdr_d_first_rankwitnessminornonzeroevaluationdeterminanth) + (mdr_pb_first_rankwitnessminornonzeroevaluationdeterminanth)) * S ((mdr_d_first_rankwitnessminornonzeroevaluationdeterminanth) + (mdr_pb_first_rankwitnessminornonzeroevaluationdeterminanth)) + ((mdr_pb_first_rankwitnessminornonzeroevaluationdeterminanth) + (mdr_pb_first_rankwitnessminornonzeroevaluationdeterminanth))) /\ ((mdr_b_first_rankwitnessminornonzeroevaluationdeterminanthrc = ((mdr_pc_first_rankwitnessminornonzeroevaluationdeterminanth) + (mdr_nb_first_rankwitnessminornonzeroevaluationdeterminanth)) * S ((mdr_pc_first_rankwitnessminornonzeroevaluationdeterminanth) + (mdr_nb_first_rankwitnessminornonzeroevaluationdeterminanth)) + ((mdr_nb_first_rankwitnessminornonzeroevaluationdeterminanth) + (mdr_nb_first_rankwitnessminornonzeroevaluationdeterminanth))) /\ ((mdr_c_first_rankwitnessminornonzeroevaluationdeterminanthrc = ((mdr_a_first_rankwitnessminornonzeroevaluationdeterminanthrc) + (mdr_b_first_rankwitnessminornonzeroevaluationdeterminanthrc)) * S ((mdr_a_first_rankwitnessminornonzeroevaluationdeterminanthrc) + (mdr_b_first_rankwitnessminornonzeroevaluationdeterminanthrc)) + ((mdr_b_first_rankwitnessminornonzeroevaluationdeterminanthrc) + (mdr_b_first_rankwitnessminornonzeroevaluationdeterminanthrc))) /\ ((mdr_e_first_rankwitnessminornonzeroevaluationdeterminanthrc = ((mdr_p_first_rankwitnessminornonzeroevaluationdeterminanth) + (mdr_n_first_rankwitnessminornonzeroevaluationdeterminanth)) * S ((mdr_p_first_rankwitnessminornonzeroevaluationdeterminanth) + (mdr_n_first_rankwitnessminornonzeroevaluationdeterminanth)) + ((mdr_n_first_rankwitnessminornonzeroevaluationdeterminanth) + (mdr_n_first_rankwitnessminornonzeroevaluationdeterminanth))) /\ ((mdr_f_first_rankwitnessminornonzeroevaluationdeterminanthrc = ((mdr_nc_first_rankwitnessminornonzeroevaluationdeterminanth) + (mdr_e_first_rankwitnessminornonzeroevaluationdeterminanthrc)) * S ((mdr_nc_first_rankwitnessminornonzeroevaluationdeterminanth) + (mdr_e_first_rankwitnessminornonzeroevaluationdeterminanthrc)) + ((mdr_e_first_rankwitnessminornonzeroevaluationdeterminanthrc) + (mdr_e_first_rankwitnessminornonzeroevaluationdeterminanthrc))) /\ ((mdr_z_first_rankwitnessminornonzeroevaluationdeterminanthr) = ((mdr_c_first_rankwitnessminornonzeroevaluationdeterminanthrc) + (mdr_f_first_rankwitnessminornonzeroevaluationdeterminanthrc)) * S ((mdr_c_first_rankwitnessminornonzeroevaluationdeterminanthrc) + (mdr_f_first_rankwitnessminornonzeroevaluationdeterminanthrc)) + ((mdr_f_first_rankwitnessminornonzeroevaluationdeterminanthrc) + (mdr_f_first_rankwitnessminornonzeroevaluationdeterminanthrc))))))))) /\ (((exists ff_h_mdr_first_rankwitnessminornonzeroevaluationdeterminanthrb. ff_h_mdr_first_rankwitnessminornonzeroevaluationdeterminanthrb + S (mdr_z_first_rankwitnessminornonzeroevaluationdeterminanthr) = S ((S (mdr_i_first_rankwitnessminornonzeroevaluationdeterminanth)) * mdr_c_first_rankwitnessminornonzeroevaluationdeterminant)) /\ exists ff_q_mdr_first_rankwitnessminornonzeroevaluationdeterminanthrb. mdr_b_first_rankwitnessminornonzeroevaluationdeterminant = ff_q_mdr_first_rankwitnessminornonzeroevaluationdeterminanthrb * S ((S (mdr_i_first_rankwitnessminornonzeroevaluationdeterminanth)) * mdr_c_first_rankwitnessminornonzeroevaluationdeterminant) + (mdr_z_first_rankwitnessminornonzeroevaluationdeterminanthr))))) /\ (((((mdr_d_first_rankwitnessminornonzeroevaluationdeterminanth) = 0) /\ (((mdr_p_first_rankwitnessminornonzeroevaluationdeterminanth) = 1) /\ ((mdr_n_first_rankwitnessminornonzeroevaluationdeterminanth) = 0))) \/ exists mdr_q_first_rankwitnessminornonzeroevaluationdeterminanths mdr_eb_first_rankwitnessminornonzeroevaluationdeterminanths mdr_ec_first_rankwitnessminornonzeroevaluationdeterminanths mdr_fb_first_rankwitnessminornonzeroevaluationdeterminanths mdr_fc_first_rankwitnessminornonzeroevaluationdeterminanths. (((mdr_d_first_rankwitnessminornonzeroevaluationdeterminanth) = S (mdr_q_first_rankwitnessminornonzeroevaluationdeterminanths)) /\ ((forall mdr_j_first_rankwitnessminornonzeroevaluationdeterminanthsc. (exists mdr_gap_first_rankwitnessminornonzeroevaluationdeterminanthscj. mdr_gap_first_rankwitnessminornonzeroevaluationdeterminanthscj + S (mdr_j_first_rankwitnessminornonzeroevaluationdeterminanthsc) = (S (mdr_q_first_rankwitnessminornonzeroevaluationdeterminanths))) -> exists mdr_i_first_rankwitnessminornonzeroevaluationdeterminanthsc mdr_up_first_rankwitnessminornonzeroevaluationdeterminanthsc mdr_us_first_rankwitnessminornonzeroevaluationdeterminanthsc mdr_un_first_rankwitnessminornonzeroevaluationdeterminanthsc mdr_ut_first_rankwitnessminornonzeroevaluationdeterminanthsc mdr_p_first_rankwitnessminornonzeroevaluationdeterminanthsc mdr_n_first_rankwitnessminornonzeroevaluationdeterminanthsc. ((exists mdr_gap_first_rankwitnessminornonzeroevaluationdeterminanthsci. mdr_gap_first_rankwitnessminornonzeroevaluationdeterminanthsci + S (mdr_i_first_rankwitnessminornonzeroevaluationdeterminanthsc) = (mdr_i_first_rankwitnessminornonzeroevaluationdeterminanth)) /\ ((exists mdr_z_first_rankwitnessminornonzeroevaluationdeterminanthscr. ((exists mdr_a_first_rankwitnessminornonzeroevaluationdeterminanthscrc mdr_b_first_rankwitnessminornonzeroevaluationdeterminanthscrc mdr_c_first_rankwitnessminornonzeroevaluationdeterminanthscrc mdr_e_first_rankwitnessminornonzeroevaluationdeterminanthscrc mdr_f_first_rankwitnessminornonzeroevaluationdeterminanthscrc. ((mdr_a_first_rankwitnessminornonzeroevaluationdeterminanthscrc = ((mdr_q_first_rankwitnessminornonzeroevaluationdeterminanths) + (mdr_up_first_rankwitnessminornonzeroevaluationdeterminanthsc)) * S ((mdr_q_first_rankwitnessminornonzeroevaluationdeterminanths) + (mdr_up_first_rankwitnessminornonzeroevaluationdeterminanthsc)) + ((mdr_up_first_rankwitnessminornonzeroevaluationdeterminanthsc) + (mdr_up_first_rankwitnessminornonzeroevaluationdeterminanthsc))) /\ ((mdr_b_first_rankwitnessminornonzeroevaluationdeterminanthscrc = ((mdr_us_first_rankwitnessminornonzeroevaluationdeterminanthsc) + (mdr_un_first_rankwitnessminornonzeroevaluationdeterminanthsc)) * S ((mdr_us_first_rankwitnessminornonzeroevaluationdeterminanthsc) + (mdr_un_first_rankwitnessminornonzeroevaluationdeterminanthsc)) + ((mdr_un_first_rankwitnessminornonzeroevaluationdeterminanthsc) + (mdr_un_first_rankwitnessminornonzeroevaluationdeterminanthsc))) /\ ((mdr_c_first_rankwitnessminornonzeroevaluationdeterminanthscrc = ((mdr_a_first_rankwitnessminornonzeroevaluationdeterminanthscrc) + (mdr_b_first_rankwitnessminornonzeroevaluationdeterminanthscrc)) * S ((mdr_a_first_rankwitnessminornonzeroevaluationdeterminanthscrc) + (mdr_b_first_rankwitnessminornonzeroevaluationdeterminanthscrc)) + ((mdr_b_first_rankwitnessminornonzeroevaluationdeterminanthscrc) + (mdr_b_first_rankwitnessminornonzeroevaluationdeterminanthscrc))) /\ ((mdr_e_first_rankwitnessminornonzeroevaluationdeterminanthscrc = ((mdr_p_first_rankwitnessminornonzeroevaluationdeterminanthsc) + (mdr_n_first_rankwitnessminornonzeroevaluationdeterminanthsc)) * S ((mdr_p_first_rankwitnessminornonzeroevaluationdeterminanthsc) + (mdr_n_first_rankwitnessminornonzeroevaluationdeterminanthsc)) + ((mdr_n_first_rankwitnessminornonzeroevaluationdeterminanthsc) + (mdr_n_first_rankwitnessminornonzeroevaluationdeterminanthsc))) /\ ((mdr_f_first_rankwitnessminornonzeroevaluationdeterminanthscrc = ((mdr_ut_first_rankwitnessminornonzeroevaluationdeterminanthsc) + (mdr_e_first_rankwitnessminornonzeroevaluationdeterminanthscrc)) * S ((mdr_ut_first_rankwitnessminornonzeroevaluationdeterminanthsc) + (mdr_e_first_rankwitnessminornonzeroevaluationdeterminanthscrc)) + ((mdr_e_first_rankwitnessminornonzeroevaluationdeterminanthscrc) + (mdr_e_first_rankwitnessminornonzeroevaluationdeterminanthscrc))) /\ ((mdr_z_first_rankwitnessminornonzeroevaluationdeterminanthscr) = ((mdr_c_first_rankwitnessminornonzeroevaluationdeterminanthscrc) + (mdr_f_first_rankwitnessminornonzeroevaluationdeterminanthscrc)) * S ((mdr_c_first_rankwitnessminornonzeroevaluationdeterminanthscrc) + (mdr_f_first_rankwitnessminornonzeroevaluationdeterminanthscrc)) + ((mdr_f_first_rankwitnessminornonzeroevaluationdeterminanthscrc) + (mdr_f_first_rankwitnessminornonzeroevaluationdeterminanthscrc))))))))) /\ (((exists ff_h_mdr_first_rankwitnessminornonzeroevaluationdeterminanthscrb. ff_h_mdr_first_rankwitnessminornonzeroevaluationdeterminanthscrb + S (mdr_z_first_rankwitnessminornonzeroevaluationdeterminanthscr) = S ((S (mdr_i_first_rankwitnessminornonzeroevaluationdeterminanthsc)) * mdr_c_first_rankwitnessminornonzeroevaluationdeterminant)) /\ exists ff_q_mdr_first_rankwitnessminornonzeroevaluationdeterminanthscrb. mdr_b_first_rankwitnessminornonzeroevaluationdeterminant = ff_q_mdr_first_rankwitnessminornonzeroevaluationdeterminanthscrb * S ((S (mdr_i_first_rankwitnessminornonzeroevaluationdeterminanthsc)) * mdr_c_first_rankwitnessminornonzeroevaluationdeterminant) + (mdr_z_first_rankwitnessminornonzeroevaluationdeterminanthscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_first_rankwitnessminornonzeroevaluationdeterminanthscm_positive. (exists ff_gap_mdm_lt_mdr_first_rankwitnessminornonzeroevaluationdeterminanthscm_positive_index_bound. ff_gap_mdm_lt_mdr_first_rankwitnessminornonzeroevaluationdeterminanthscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_first_rankwitnessminornonzeroevaluationdeterminanthscm_positive) = ((mdr_q_first_rankwitnessminornonzeroevaluationdeterminanths) * (mdr_q_first_rankwitnessminornonzeroevaluationdeterminanths))) -> exists ff_row_mdm_prefix_mdr_first_rankwitnessminornonzeroevaluationdeterminanthscm_positive ff_column_mdm_prefix_mdr_first_rankwitnessminornonzeroevaluationdeterminanthscm_positive ff_value_mdm_prefix_mdr_first_rankwitnessminornonzeroevaluationdeterminanthscm_positive. (ff_index_mdm_prefix_mdr_first_rankwitnessminornonzeroevaluationdeterminanthscm_positive = (mdr_q_first_rankwitnessminornonzeroevaluationdeterminanths) * ff_row_mdm_prefix_mdr_first_rankwitnessminornonzeroevaluationdeterminanthscm_positive + ff_column_mdm_prefix_mdr_first_rankwitnessminornonzeroevaluationdeterminanthscm_positive /\ ((exists ff_gap_mdm_lt_mdr_first_rankwitnessminornonzeroevaluationdeterminanthscm_positive_column_bound. ff_gap_mdm_lt_mdr_first_rankwitnessminornonzeroevaluationdeterminanthscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_first_rankwitnessminornonzeroevaluationdeterminanthscm_positive) = (mdr_q_first_rankwitnessminornonzeroevaluationdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_first_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell ff_column_mdm_cell_mdr_first_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_first_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_first_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_first_rankwitnessminornonzeroevaluationdeterminanthscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_first_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell = ff_row_mdm_prefix_mdr_first_rankwitnessminornonzeroevaluationdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_first_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell_row_after. ff_gap_mdm_le_mdr_first_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_first_rankwitnessminornonzeroevaluationdeterminanthscm_positive)) /\ ff_row_mdm_cell_mdr_first_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell = S ff_row_mdm_prefix_mdr_first_rankwitnessminornonzeroevaluationdeterminanthscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_first_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_first_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_first_rankwitnessminornonzeroevaluationdeterminanthscm_positive) = (mdr_j_first_rankwitnessminornonzeroevaluationdeterminanthsc)) /\ ff_column_mdm_cell_mdr_first_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell = ff_column_mdm_prefix_mdr_first_rankwitnessminornonzeroevaluationdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_first_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell_column_after. ff_gap_mdm_le_mdr_first_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell_column_after + (mdr_j_first_rankwitnessminornonzeroevaluationdeterminanthsc) = (ff_column_mdm_prefix_mdr_first_rankwitnessminornonzeroevaluationdeterminanthscm_positive)) /\ ff_column_mdm_cell_mdr_first_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell = S ff_column_mdm_prefix_mdr_first_rankwitnessminornonzeroevaluationdeterminanthscm_positive))) /\ (((exists ff_h_mdm_mdr_first_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell_source. ff_h_mdm_mdr_first_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_first_rankwitnessminornonzeroevaluationdeterminanthscm_positive) = S ((S ((ff_row_mdm_cell_mdr_first_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell) * (S (mdr_q_first_rankwitnessminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_first_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell))) * mdr_pc_first_rankwitnessminornonzeroevaluationdeterminanth)) /\ exists ff_q_mdm_mdr_first_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell_source. mdr_pb_first_rankwitnessminornonzeroevaluationdeterminanth = ff_q_mdm_mdr_first_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_first_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell) * (S (mdr_q_first_rankwitnessminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_first_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell))) * mdr_pc_first_rankwitnessminornonzeroevaluationdeterminanth) + (ff_value_mdm_prefix_mdr_first_rankwitnessminornonzeroevaluationdeterminanthscm_positive)))))) /\ (((exists ff_h_mdm_mdr_first_rankwitnessminornonzeroevaluationdeterminanthscm_positive_target. ff_h_mdm_mdr_first_rankwitnessminornonzeroevaluationdeterminanthscm_positive_target + S (ff_value_mdm_prefix_mdr_first_rankwitnessminornonzeroevaluationdeterminanthscm_positive) = S ((S (ff_index_mdm_prefix_mdr_first_rankwitnessminornonzeroevaluationdeterminanthscm_positive)) * mdr_us_first_rankwitnessminornonzeroevaluationdeterminanthsc)) /\ exists ff_q_mdm_mdr_first_rankwitnessminornonzeroevaluationdeterminanthscm_positive_target. mdr_up_first_rankwitnessminornonzeroevaluationdeterminanthsc = ff_q_mdm_mdr_first_rankwitnessminornonzeroevaluationdeterminanthscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_first_rankwitnessminornonzeroevaluationdeterminanthscm_positive)) * mdr_us_first_rankwitnessminornonzeroevaluationdeterminanthsc) + (ff_value_mdm_prefix_mdr_first_rankwitnessminornonzeroevaluationdeterminanthscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_first_rankwitnessminornonzeroevaluationdeterminanthscm_negative. (exists ff_gap_mdm_lt_mdr_first_rankwitnessminornonzeroevaluationdeterminanthscm_negative_index_bound. ff_gap_mdm_lt_mdr_first_rankwitnessminornonzeroevaluationdeterminanthscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_first_rankwitnessminornonzeroevaluationdeterminanthscm_negative) = ((mdr_q_first_rankwitnessminornonzeroevaluationdeterminanths) * (mdr_q_first_rankwitnessminornonzeroevaluationdeterminanths))) -> exists ff_row_mdm_prefix_mdr_first_rankwitnessminornonzeroevaluationdeterminanthscm_negative ff_column_mdm_prefix_mdr_first_rankwitnessminornonzeroevaluationdeterminanthscm_negative ff_value_mdm_prefix_mdr_first_rankwitnessminornonzeroevaluationdeterminanthscm_negative. (ff_index_mdm_prefix_mdr_first_rankwitnessminornonzeroevaluationdeterminanthscm_negative = (mdr_q_first_rankwitnessminornonzeroevaluationdeterminanths) * ff_row_mdm_prefix_mdr_first_rankwitnessminornonzeroevaluationdeterminanthscm_negative + ff_column_mdm_prefix_mdr_first_rankwitnessminornonzeroevaluationdeterminanthscm_negative /\ ((exists ff_gap_mdm_lt_mdr_first_rankwitnessminornonzeroevaluationdeterminanthscm_negative_column_bound. ff_gap_mdm_lt_mdr_first_rankwitnessminornonzeroevaluationdeterminanthscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_first_rankwitnessminornonzeroevaluationdeterminanthscm_negative) = (mdr_q_first_rankwitnessminornonzeroevaluationdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_first_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell ff_column_mdm_cell_mdr_first_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_first_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_first_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_first_rankwitnessminornonzeroevaluationdeterminanthscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_first_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell = ff_row_mdm_prefix_mdr_first_rankwitnessminornonzeroevaluationdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_first_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell_row_after. ff_gap_mdm_le_mdr_first_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_first_rankwitnessminornonzeroevaluationdeterminanthscm_negative)) /\ ff_row_mdm_cell_mdr_first_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell = S ff_row_mdm_prefix_mdr_first_rankwitnessminornonzeroevaluationdeterminanthscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_first_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_first_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_first_rankwitnessminornonzeroevaluationdeterminanthscm_negative) = (mdr_j_first_rankwitnessminornonzeroevaluationdeterminanthsc)) /\ ff_column_mdm_cell_mdr_first_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell = ff_column_mdm_prefix_mdr_first_rankwitnessminornonzeroevaluationdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_first_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell_column_after. ff_gap_mdm_le_mdr_first_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell_column_after + (mdr_j_first_rankwitnessminornonzeroevaluationdeterminanthsc) = (ff_column_mdm_prefix_mdr_first_rankwitnessminornonzeroevaluationdeterminanthscm_negative)) /\ ff_column_mdm_cell_mdr_first_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell = S ff_column_mdm_prefix_mdr_first_rankwitnessminornonzeroevaluationdeterminanthscm_negative))) /\ (((exists ff_h_mdm_mdr_first_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell_source. ff_h_mdm_mdr_first_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_first_rankwitnessminornonzeroevaluationdeterminanthscm_negative) = S ((S ((ff_row_mdm_cell_mdr_first_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell) * (S (mdr_q_first_rankwitnessminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_first_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell))) * mdr_nc_first_rankwitnessminornonzeroevaluationdeterminanth)) /\ exists ff_q_mdm_mdr_first_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell_source. mdr_nb_first_rankwitnessminornonzeroevaluationdeterminanth = ff_q_mdm_mdr_first_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_first_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell) * (S (mdr_q_first_rankwitnessminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_first_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell))) * mdr_nc_first_rankwitnessminornonzeroevaluationdeterminanth) + (ff_value_mdm_prefix_mdr_first_rankwitnessminornonzeroevaluationdeterminanthscm_negative)))))) /\ (((exists ff_h_mdm_mdr_first_rankwitnessminornonzeroevaluationdeterminanthscm_negative_target. ff_h_mdm_mdr_first_rankwitnessminornonzeroevaluationdeterminanthscm_negative_target + S (ff_value_mdm_prefix_mdr_first_rankwitnessminornonzeroevaluationdeterminanthscm_negative) = S ((S (ff_index_mdm_prefix_mdr_first_rankwitnessminornonzeroevaluationdeterminanthscm_negative)) * mdr_ut_first_rankwitnessminornonzeroevaluationdeterminanthsc)) /\ exists ff_q_mdm_mdr_first_rankwitnessminornonzeroevaluationdeterminanthscm_negative_target. mdr_un_first_rankwitnessminornonzeroevaluationdeterminanthsc = ff_q_mdm_mdr_first_rankwitnessminornonzeroevaluationdeterminanthscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_first_rankwitnessminornonzeroevaluationdeterminanthscm_negative)) * mdr_ut_first_rankwitnessminornonzeroevaluationdeterminanthsc) + (ff_value_mdm_prefix_mdr_first_rankwitnessminornonzeroevaluationdeterminanthscm_negative))))))))) /\ ((((exists ff_h_mdr_first_rankwitnessminornonzeroevaluationdeterminanthscp. ff_h_mdr_first_rankwitnessminornonzeroevaluationdeterminanthscp + S (mdr_p_first_rankwitnessminornonzeroevaluationdeterminanthsc) = S ((S (mdr_j_first_rankwitnessminornonzeroevaluationdeterminanthsc)) * mdr_ec_first_rankwitnessminornonzeroevaluationdeterminanths)) /\ exists ff_q_mdr_first_rankwitnessminornonzeroevaluationdeterminanthscp. mdr_eb_first_rankwitnessminornonzeroevaluationdeterminanths = ff_q_mdr_first_rankwitnessminornonzeroevaluationdeterminanthscp * S ((S (mdr_j_first_rankwitnessminornonzeroevaluationdeterminanthsc)) * mdr_ec_first_rankwitnessminornonzeroevaluationdeterminanths) + (mdr_p_first_rankwitnessminornonzeroevaluationdeterminanthsc))) /\ (((exists ff_h_mdr_first_rankwitnessminornonzeroevaluationdeterminanthscn. ff_h_mdr_first_rankwitnessminornonzeroevaluationdeterminanthscn + S (mdr_n_first_rankwitnessminornonzeroevaluationdeterminanthsc) = S ((S (mdr_j_first_rankwitnessminornonzeroevaluationdeterminanthsc)) * mdr_fc_first_rankwitnessminornonzeroevaluationdeterminanths)) /\ exists ff_q_mdr_first_rankwitnessminornonzeroevaluationdeterminanthscn. mdr_fb_first_rankwitnessminornonzeroevaluationdeterminanths = ff_q_mdr_first_rankwitnessminornonzeroevaluationdeterminanthscn * S ((S (mdr_j_first_rankwitnessminornonzeroevaluationdeterminanthsc)) * mdr_fc_first_rankwitnessminornonzeroevaluationdeterminanths) + (mdr_n_first_rankwitnessminornonzeroevaluationdeterminanthsc)))))))) /\ (exists ff_ub_mce_fold_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf ff_uc_mce_fold_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf ff_vb_mce_fold_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf ff_vc_mce_fold_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf. ((forall ff_index_mce_alternating_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_prefix. (exists ff_gap_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_index. ff_gap_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_index + S (ff_index_mce_alternating_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) = (S (mdr_q_first_rankwitnessminornonzeroevaluationdeterminanths))) -> exists ff_ap_mce_alternating_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_prefix ff_an_mce_alternating_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_prefix ff_bp_mce_alternating_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_prefix ff_bn_mce_alternating_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_prefix ff_p_mce_alternating_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_prefix ff_n_mce_alternating_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_prefix. ((((exists ff_h_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_ap. ff_h_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_ap + S (ff_ap_mce_alternating_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_prefix)) * mdr_pc_first_rankwitnessminornonzeroevaluationdeterminanth)) /\ exists ff_q_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_ap. mdr_pb_first_rankwitnessminornonzeroevaluationdeterminanth = ff_q_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_prefix)) * mdr_pc_first_rankwitnessminornonzeroevaluationdeterminanth) + (ff_ap_mce_alternating_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_an. ff_h_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_an + S (ff_an_mce_alternating_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_prefix)) * mdr_nc_first_rankwitnessminornonzeroevaluationdeterminanth)) /\ exists ff_q_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_an. mdr_nb_first_rankwitnessminornonzeroevaluationdeterminanth = ff_q_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_prefix)) * mdr_nc_first_rankwitnessminornonzeroevaluationdeterminanth) + (ff_an_mce_alternating_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_bp. ff_h_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_bp + S (ff_bp_mce_alternating_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_prefix)) * mdr_ec_first_rankwitnessminornonzeroevaluationdeterminanths)) /\ exists ff_q_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_bp. mdr_eb_first_rankwitnessminornonzeroevaluationdeterminanths = ff_q_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_prefix)) * mdr_ec_first_rankwitnessminornonzeroevaluationdeterminanths) + (ff_bp_mce_alternating_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_bn. ff_h_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_bn + S (ff_bn_mce_alternating_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_prefix)) * mdr_fc_first_rankwitnessminornonzeroevaluationdeterminanths)) /\ exists ff_q_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_bn. mdr_fb_first_rankwitnessminornonzeroevaluationdeterminanths = ff_q_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_prefix)) * mdr_fc_first_rankwitnessminornonzeroevaluationdeterminanths) + (ff_bn_mce_alternating_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_positive. ff_h_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_positive + S (ff_p_mce_alternating_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_positive. ff_ub_mce_fold_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf) + (ff_p_mce_alternating_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_negative. ff_h_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_negative + S (ff_n_mce_alternating_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_negative. ff_vb_mce_fold_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf) + (ff_n_mce_alternating_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_prefix))) /\ (((exists ff_even_mce_term_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_prefix = 2 * ff_even_mce_term_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_term) /\ (ff_p_mce_alternating_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_prefix = 2 * ff_odd_mce_term_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_positive ff_v_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_positive. ((((exists ff_h_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_positive_start. ff_h_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_positive_start. ff_u_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_positive_start * S ((S (0)) * ff_v_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_positive_terminal. ff_h_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_positive_terminal + S (mdr_p_first_rankwitnessminornonzeroevaluationdeterminanth) = S ((S ((S (mdr_q_first_rankwitnessminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_positive_terminal. ff_u_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_positive_terminal * S ((S ((S (mdr_q_first_rankwitnessminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_positive) + (mdr_p_first_rankwitnessminornonzeroevaluationdeterminanth))) /\ forall ff_i_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_positive. (exists ff_lt_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_positive_bound. ff_lt_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_positive_bound + S ff_i_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_positive = (S (mdr_q_first_rankwitnessminornonzeroevaluationdeterminanths))) -> exists ff_a_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_positive ff_r_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_positive ff_s_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_positive. ((((exists ff_h_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_positive_summand. ff_h_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_positive_summand + S (ff_a_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_positive_summand. ff_ub_mce_fold_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_positive_summand * S ((S (ff_i_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf) + (ff_a_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_positive_partial. ff_h_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_positive_partial + S (ff_r_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_positive_partial. ff_u_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_positive_partial * S ((S (ff_i_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_positive) + (ff_r_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_positive_successor. ff_h_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_positive_successor + S (ff_s_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_positive) = S ((S (S ff_i_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_positive_successor. ff_u_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_positive_successor * S ((S (S ff_i_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_positive) + (ff_s_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_positive))) /\ ff_s_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_positive = ff_r_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_positive + ff_a_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_positive)))))) /\ (exists ff_u_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_negative ff_v_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_negative. ((((exists ff_h_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_negative_start. ff_h_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_negative_start. ff_u_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_negative_start * S ((S (0)) * ff_v_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_negative_terminal. ff_h_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_negative_terminal + S (mdr_n_first_rankwitnessminornonzeroevaluationdeterminanth) = S ((S ((S (mdr_q_first_rankwitnessminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_negative_terminal. ff_u_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_negative_terminal * S ((S ((S (mdr_q_first_rankwitnessminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_negative) + (mdr_n_first_rankwitnessminornonzeroevaluationdeterminanth))) /\ forall ff_i_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_negative. (exists ff_lt_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_negative_bound. ff_lt_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_negative_bound + S ff_i_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_negative = (S (mdr_q_first_rankwitnessminornonzeroevaluationdeterminanths))) -> exists ff_a_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_negative ff_r_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_negative ff_s_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_negative. ((((exists ff_h_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_negative_summand. ff_h_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_negative_summand + S (ff_a_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_negative_summand. ff_vb_mce_fold_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_negative_summand * S ((S (ff_i_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf) + (ff_a_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_negative_partial. ff_h_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_negative_partial + S (ff_r_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_negative_partial. ff_u_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_negative_partial * S ((S (ff_i_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_negative) + (ff_r_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_negative_successor. ff_h_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_negative_successor + S (ff_s_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_negative) = S ((S (S ff_i_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_negative_successor. ff_u_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_negative_successor * S ((S (S ff_i_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_negative) + (ff_s_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_negative))) /\ ff_s_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_negative = ff_r_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_negative + ff_a_mce_mdr_first_rankwitnessminornonzeroevaluationdeterminanthsf_negative))))))))))))))) /\ ((exists mdr_gap_first_rankwitnessminornonzeroevaluationdeterminanti. mdr_gap_first_rankwitnessminornonzeroevaluationdeterminanti + S (mdr_i_first_rankwitnessminornonzeroevaluationdeterminant) = (mdr_l_first_rankwitnessminornonzeroevaluationdeterminant)) /\ (exists mdr_z_first_rankwitnessminornonzeroevaluationdeterminantr. ((exists mdr_a_first_rankwitnessminornonzeroevaluationdeterminantrc mdr_b_first_rankwitnessminornonzeroevaluationdeterminantrc mdr_c_first_rankwitnessminornonzeroevaluationdeterminantrc mdr_e_first_rankwitnessminornonzeroevaluationdeterminantrc mdr_f_first_rankwitnessminornonzeroevaluationdeterminantrc. ((mdr_a_first_rankwitnessminornonzeroevaluationdeterminantrc = ((rank) + (mdr_ub_first_rankwitnessminornonzeroevaluation)) * S ((rank) + (mdr_ub_first_rankwitnessminornonzeroevaluation)) + ((mdr_ub_first_rankwitnessminornonzeroevaluation) + (mdr_ub_first_rankwitnessminornonzeroevaluation))) /\ ((mdr_b_first_rankwitnessminornonzeroevaluationdeterminantrc = ((mdr_uc_first_rankwitnessminornonzeroevaluation) + (mdr_vb_first_rankwitnessminornonzeroevaluation)) * S ((mdr_uc_first_rankwitnessminornonzeroevaluation) + (mdr_vb_first_rankwitnessminornonzeroevaluation)) + ((mdr_vb_first_rankwitnessminornonzeroevaluation) + (mdr_vb_first_rankwitnessminornonzeroevaluation))) /\ ((mdr_c_first_rankwitnessminornonzeroevaluationdeterminantrc = ((mdr_a_first_rankwitnessminornonzeroevaluationdeterminantrc) + (mdr_b_first_rankwitnessminornonzeroevaluationdeterminantrc)) * S ((mdr_a_first_rankwitnessminornonzeroevaluationdeterminantrc) + (mdr_b_first_rankwitnessminornonzeroevaluationdeterminantrc)) + ((mdr_b_first_rankwitnessminornonzeroevaluationdeterminantrc) + (mdr_b_first_rankwitnessminornonzeroevaluationdeterminantrc))) /\ ((mdr_e_first_rankwitnessminornonzeroevaluationdeterminantrc = ((mdr_p_first_rankwitnessminornonzero) + (mdr_n_first_rankwitnessminornonzero)) * S ((mdr_p_first_rankwitnessminornonzero) + (mdr_n_first_rankwitnessminornonzero)) + ((mdr_n_first_rankwitnessminornonzero) + (mdr_n_first_rankwitnessminornonzero))) /\ ((mdr_f_first_rankwitnessminornonzeroevaluationdeterminantrc = ((mdr_vc_first_rankwitnessminornonzeroevaluation) + (mdr_e_first_rankwitnessminornonzeroevaluationdeterminantrc)) * S ((mdr_vc_first_rankwitnessminornonzeroevaluation) + (mdr_e_first_rankwitnessminornonzeroevaluationdeterminantrc)) + ((mdr_e_first_rankwitnessminornonzeroevaluationdeterminantrc) + (mdr_e_first_rankwitnessminornonzeroevaluationdeterminantrc))) /\ ((mdr_z_first_rankwitnessminornonzeroevaluationdeterminantr) = ((mdr_c_first_rankwitnessminornonzeroevaluationdeterminantrc) + (mdr_f_first_rankwitnessminornonzeroevaluationdeterminantrc)) * S ((mdr_c_first_rankwitnessminornonzeroevaluationdeterminantrc) + (mdr_f_first_rankwitnessminornonzeroevaluationdeterminantrc)) + ((mdr_f_first_rankwitnessminornonzeroevaluationdeterminantrc) + (mdr_f_first_rankwitnessminornonzeroevaluationdeterminantrc))))))))) /\ (((exists ff_h_mdr_first_rankwitnessminornonzeroevaluationdeterminantrb. ff_h_mdr_first_rankwitnessminornonzeroevaluationdeterminantrb + S (mdr_z_first_rankwitnessminornonzeroevaluationdeterminantr) = S ((S (mdr_i_first_rankwitnessminornonzeroevaluationdeterminant)) * mdr_c_first_rankwitnessminornonzeroevaluationdeterminant)) /\ exists ff_q_mdr_first_rankwitnessminornonzeroevaluationdeterminantrb. mdr_b_first_rankwitnessminornonzeroevaluationdeterminant = ff_q_mdr_first_rankwitnessminornonzeroevaluationdeterminantrb * S ((S (mdr_i_first_rankwitnessminornonzeroevaluationdeterminant)) * mdr_c_first_rankwitnessminornonzeroevaluationdeterminant) + (mdr_z_first_rankwitnessminornonzeroevaluationdeterminantr)))))))))) /\ (~(mdr_p_first_rankwitnessminornonzero = mdr_n_first_rankwitnessminornonzero)))))))) /\ (forall mdr_q_first_rank. (exists mdr_gap_first_rankhigher. mdr_gap_first_rankhigher + S (rank) = (mdr_q_first_rank)) -> (forall mdr_rb_first_rankzero mdr_rc_first_rankzero mdr_cb_first_rankzero mdr_cc_first_rankzero mdr_p_first_rankzero mdr_n_first_rankzero. (((forall fom_index_mrf_first_rankzerorowsbound. (exists fom_gap_mrf_first_rankzerorowsbound_index_bound. fom_gap_mrf_first_rankzerorowsbound_index_bound + S (fom_index_mrf_first_rankzerorowsbound) = mdr_q_first_rank) -> exists fom_value_mrf_first_rankzerorowsbound. ((((exists fom_beta_height_mrf_first_rankzerorowsbound_entry. fom_beta_height_mrf_first_rankzerorowsbound_entry + S (fom_value_mrf_first_rankzerorowsbound) = S ((S (fom_index_mrf_first_rankzerorowsbound)) * mdr_rc_first_rankzero)) /\ exists fom_beta_quotient_mrf_first_rankzerorowsbound_entry. mdr_rb_first_rankzero = fom_beta_quotient_mrf_first_rankzerorowsbound_entry * S ((S (fom_index_mrf_first_rankzerorowsbound)) * mdr_rc_first_rankzero) + (fom_value_mrf_first_rankzerorowsbound))) /\ (exists fom_gap_mrf_first_rankzerorowsbound_value_bound. fom_gap_mrf_first_rankzerorowsbound_value_bound + S (fom_value_mrf_first_rankzerorowsbound) = r))) /\ (forall mdr_i_first_rankzerorowsdistinct mdr_j_first_rankzerorowsdistinct mdr_a_first_rankzerorowsdistinct. (exists mdr_gap_first_rankzerorowsdistincti. mdr_gap_first_rankzerorowsdistincti + S (mdr_i_first_rankzerorowsdistinct) = (mdr_q_first_rank)) -> (exists mdr_gap_first_rankzerorowsdistinctj. mdr_gap_first_rankzerorowsdistinctj + S (mdr_j_first_rankzerorowsdistinct) = (mdr_q_first_rank)) -> (((exists ff_h_mdr_first_rankzerorowsdistinctfirst. ff_h_mdr_first_rankzerorowsdistinctfirst + S (mdr_a_first_rankzerorowsdistinct) = S ((S (mdr_i_first_rankzerorowsdistinct)) * mdr_rc_first_rankzero)) /\ exists ff_q_mdr_first_rankzerorowsdistinctfirst. mdr_rb_first_rankzero = ff_q_mdr_first_rankzerorowsdistinctfirst * S ((S (mdr_i_first_rankzerorowsdistinct)) * mdr_rc_first_rankzero) + (mdr_a_first_rankzerorowsdistinct))) -> (((exists ff_h_mdr_first_rankzerorowsdistinctsecond. ff_h_mdr_first_rankzerorowsdistinctsecond + S (mdr_a_first_rankzerorowsdistinct) = S ((S (mdr_j_first_rankzerorowsdistinct)) * mdr_rc_first_rankzero)) /\ exists ff_q_mdr_first_rankzerorowsdistinctsecond. mdr_rb_first_rankzero = ff_q_mdr_first_rankzerorowsdistinctsecond * S ((S (mdr_j_first_rankzerorowsdistinct)) * mdr_rc_first_rankzero) + (mdr_a_first_rankzerorowsdistinct))) -> mdr_i_first_rankzerorowsdistinct = mdr_j_first_rankzerorowsdistinct))) -> (((forall fom_index_mrf_first_rankzerocolumnsbound. (exists fom_gap_mrf_first_rankzerocolumnsbound_index_bound. fom_gap_mrf_first_rankzerocolumnsbound_index_bound + S (fom_index_mrf_first_rankzerocolumnsbound) = mdr_q_first_rank) -> exists fom_value_mrf_first_rankzerocolumnsbound. ((((exists fom_beta_height_mrf_first_rankzerocolumnsbound_entry. fom_beta_height_mrf_first_rankzerocolumnsbound_entry + S (fom_value_mrf_first_rankzerocolumnsbound) = S ((S (fom_index_mrf_first_rankzerocolumnsbound)) * mdr_cc_first_rankzero)) /\ exists fom_beta_quotient_mrf_first_rankzerocolumnsbound_entry. mdr_cb_first_rankzero = fom_beta_quotient_mrf_first_rankzerocolumnsbound_entry * S ((S (fom_index_mrf_first_rankzerocolumnsbound)) * mdr_cc_first_rankzero) + (fom_value_mrf_first_rankzerocolumnsbound))) /\ (exists fom_gap_mrf_first_rankzerocolumnsbound_value_bound. fom_gap_mrf_first_rankzerocolumnsbound_value_bound + S (fom_value_mrf_first_rankzerocolumnsbound) = w))) /\ (forall mdr_i_first_rankzerocolumnsdistinct mdr_j_first_rankzerocolumnsdistinct mdr_a_first_rankzerocolumnsdistinct. (exists mdr_gap_first_rankzerocolumnsdistincti. mdr_gap_first_rankzerocolumnsdistincti + S (mdr_i_first_rankzerocolumnsdistinct) = (mdr_q_first_rank)) -> (exists mdr_gap_first_rankzerocolumnsdistinctj. mdr_gap_first_rankzerocolumnsdistinctj + S (mdr_j_first_rankzerocolumnsdistinct) = (mdr_q_first_rank)) -> (((exists ff_h_mdr_first_rankzerocolumnsdistinctfirst. ff_h_mdr_first_rankzerocolumnsdistinctfirst + S (mdr_a_first_rankzerocolumnsdistinct) = S ((S (mdr_i_first_rankzerocolumnsdistinct)) * mdr_cc_first_rankzero)) /\ exists ff_q_mdr_first_rankzerocolumnsdistinctfirst. mdr_cb_first_rankzero = ff_q_mdr_first_rankzerocolumnsdistinctfirst * S ((S (mdr_i_first_rankzerocolumnsdistinct)) * mdr_cc_first_rankzero) + (mdr_a_first_rankzerocolumnsdistinct))) -> (((exists ff_h_mdr_first_rankzerocolumnsdistinctsecond. ff_h_mdr_first_rankzerocolumnsdistinctsecond + S (mdr_a_first_rankzerocolumnsdistinct) = S ((S (mdr_j_first_rankzerocolumnsdistinct)) * mdr_cc_first_rankzero)) /\ exists ff_q_mdr_first_rankzerocolumnsdistinctsecond. mdr_cb_first_rankzero = ff_q_mdr_first_rankzerocolumnsdistinctsecond * S ((S (mdr_j_first_rankzerocolumnsdistinct)) * mdr_cc_first_rankzero) + (mdr_a_first_rankzerocolumnsdistinct))) -> mdr_i_first_rankzerocolumnsdistinct = mdr_j_first_rankzerocolumnsdistinct))) -> (exists mdr_ub_first_rankzeroevaluation mdr_uc_first_rankzeroevaluation mdr_vb_first_rankzeroevaluation mdr_vc_first_rankzeroevaluation. ((((forall mdr_i_first_rankzeroevaluationmatrixpositive. (exists mdr_gap_first_rankzeroevaluationmatrixpositivebound. mdr_gap_first_rankzeroevaluationmatrixpositivebound + S (mdr_i_first_rankzeroevaluationmatrixpositive) = ((mdr_q_first_rank) * (mdr_q_first_rank))) -> exists mdr_a_first_rankzeroevaluationmatrixpositive. (((exists mdr_r_first_rankzeroevaluationmatrixpositivepoint mdr_s_first_rankzeroevaluationmatrixpositivepoint mdr_u_first_rankzeroevaluationmatrixpositivepoint mdr_v_first_rankzeroevaluationmatrixpositivepoint. ((mdr_i_first_rankzeroevaluationmatrixpositive = (mdr_q_first_rank) * mdr_r_first_rankzeroevaluationmatrixpositivepoint + mdr_s_first_rankzeroevaluationmatrixpositivepoint) /\ ((exists mdr_gap_first_rankzeroevaluationmatrixpositivepointcolumn. mdr_gap_first_rankzeroevaluationmatrixpositivepointcolumn + S (mdr_s_first_rankzeroevaluationmatrixpositivepoint) = (mdr_q_first_rank)) /\ ((((exists ff_h_mdr_first_rankzeroevaluationmatrixpositivepointrow_index. ff_h_mdr_first_rankzeroevaluationmatrixpositivepointrow_index + S (mdr_u_first_rankzeroevaluationmatrixpositivepoint) = S ((S (mdr_r_first_rankzeroevaluationmatrixpositivepoint)) * mdr_rc_first_rankzero)) /\ exists ff_q_mdr_first_rankzeroevaluationmatrixpositivepointrow_index. mdr_rb_first_rankzero = ff_q_mdr_first_rankzeroevaluationmatrixpositivepointrow_index * S ((S (mdr_r_first_rankzeroevaluationmatrixpositivepoint)) * mdr_rc_first_rankzero) + (mdr_u_first_rankzeroevaluationmatrixpositivepoint))) /\ ((((exists ff_h_mdr_first_rankzeroevaluationmatrixpositivepointcolumn_index. ff_h_mdr_first_rankzeroevaluationmatrixpositivepointcolumn_index + S (mdr_v_first_rankzeroevaluationmatrixpositivepoint) = S ((S (mdr_s_first_rankzeroevaluationmatrixpositivepoint)) * mdr_cc_first_rankzero)) /\ exists ff_q_mdr_first_rankzeroevaluationmatrixpositivepointcolumn_index. mdr_cb_first_rankzero = ff_q_mdr_first_rankzeroevaluationmatrixpositivepointcolumn_index * S ((S (mdr_s_first_rankzeroevaluationmatrixpositivepoint)) * mdr_cc_first_rankzero) + (mdr_v_first_rankzeroevaluationmatrixpositivepoint))) /\ (((exists ff_h_mdr_first_rankzeroevaluationmatrixpositivepointsource. ff_h_mdr_first_rankzeroevaluationmatrixpositivepointsource + S (mdr_a_first_rankzeroevaluationmatrixpositive) = S ((S ((mdr_u_first_rankzeroevaluationmatrixpositivepoint) * (w) + (mdr_v_first_rankzeroevaluationmatrixpositivepoint))) * pc)) /\ exists ff_q_mdr_first_rankzeroevaluationmatrixpositivepointsource. pb = ff_q_mdr_first_rankzeroevaluationmatrixpositivepointsource * S ((S ((mdr_u_first_rankzeroevaluationmatrixpositivepoint) * (w) + (mdr_v_first_rankzeroevaluationmatrixpositivepoint))) * pc) + (mdr_a_first_rankzeroevaluationmatrixpositive)))))))) /\ (((exists ff_h_mdr_first_rankzeroevaluationmatrixpositiveoutput. ff_h_mdr_first_rankzeroevaluationmatrixpositiveoutput + S (mdr_a_first_rankzeroevaluationmatrixpositive) = S ((S (mdr_i_first_rankzeroevaluationmatrixpositive)) * mdr_uc_first_rankzeroevaluation)) /\ exists ff_q_mdr_first_rankzeroevaluationmatrixpositiveoutput. mdr_ub_first_rankzeroevaluation = ff_q_mdr_first_rankzeroevaluationmatrixpositiveoutput * S ((S (mdr_i_first_rankzeroevaluationmatrixpositive)) * mdr_uc_first_rankzeroevaluation) + (mdr_a_first_rankzeroevaluationmatrixpositive)))))) /\ (forall mdr_i_first_rankzeroevaluationmatrixnegative. (exists mdr_gap_first_rankzeroevaluationmatrixnegativebound. mdr_gap_first_rankzeroevaluationmatrixnegativebound + S (mdr_i_first_rankzeroevaluationmatrixnegative) = ((mdr_q_first_rank) * (mdr_q_first_rank))) -> exists mdr_a_first_rankzeroevaluationmatrixnegative. (((exists mdr_r_first_rankzeroevaluationmatrixnegativepoint mdr_s_first_rankzeroevaluationmatrixnegativepoint mdr_u_first_rankzeroevaluationmatrixnegativepoint mdr_v_first_rankzeroevaluationmatrixnegativepoint. ((mdr_i_first_rankzeroevaluationmatrixnegative = (mdr_q_first_rank) * mdr_r_first_rankzeroevaluationmatrixnegativepoint + mdr_s_first_rankzeroevaluationmatrixnegativepoint) /\ ((exists mdr_gap_first_rankzeroevaluationmatrixnegativepointcolumn. mdr_gap_first_rankzeroevaluationmatrixnegativepointcolumn + S (mdr_s_first_rankzeroevaluationmatrixnegativepoint) = (mdr_q_first_rank)) /\ ((((exists ff_h_mdr_first_rankzeroevaluationmatrixnegativepointrow_index. ff_h_mdr_first_rankzeroevaluationmatrixnegativepointrow_index + S (mdr_u_first_rankzeroevaluationmatrixnegativepoint) = S ((S (mdr_r_first_rankzeroevaluationmatrixnegativepoint)) * mdr_rc_first_rankzero)) /\ exists ff_q_mdr_first_rankzeroevaluationmatrixnegativepointrow_index. mdr_rb_first_rankzero = ff_q_mdr_first_rankzeroevaluationmatrixnegativepointrow_index * S ((S (mdr_r_first_rankzeroevaluationmatrixnegativepoint)) * mdr_rc_first_rankzero) + (mdr_u_first_rankzeroevaluationmatrixnegativepoint))) /\ ((((exists ff_h_mdr_first_rankzeroevaluationmatrixnegativepointcolumn_index. ff_h_mdr_first_rankzeroevaluationmatrixnegativepointcolumn_index + S (mdr_v_first_rankzeroevaluationmatrixnegativepoint) = S ((S (mdr_s_first_rankzeroevaluationmatrixnegativepoint)) * mdr_cc_first_rankzero)) /\ exists ff_q_mdr_first_rankzeroevaluationmatrixnegativepointcolumn_index. mdr_cb_first_rankzero = ff_q_mdr_first_rankzeroevaluationmatrixnegativepointcolumn_index * S ((S (mdr_s_first_rankzeroevaluationmatrixnegativepoint)) * mdr_cc_first_rankzero) + (mdr_v_first_rankzeroevaluationmatrixnegativepoint))) /\ (((exists ff_h_mdr_first_rankzeroevaluationmatrixnegativepointsource. ff_h_mdr_first_rankzeroevaluationmatrixnegativepointsource + S (mdr_a_first_rankzeroevaluationmatrixnegative) = S ((S ((mdr_u_first_rankzeroevaluationmatrixnegativepoint) * (w) + (mdr_v_first_rankzeroevaluationmatrixnegativepoint))) * nc)) /\ exists ff_q_mdr_first_rankzeroevaluationmatrixnegativepointsource. nb = ff_q_mdr_first_rankzeroevaluationmatrixnegativepointsource * S ((S ((mdr_u_first_rankzeroevaluationmatrixnegativepoint) * (w) + (mdr_v_first_rankzeroevaluationmatrixnegativepoint))) * nc) + (mdr_a_first_rankzeroevaluationmatrixnegative)))))))) /\ (((exists ff_h_mdr_first_rankzeroevaluationmatrixnegativeoutput. ff_h_mdr_first_rankzeroevaluationmatrixnegativeoutput + S (mdr_a_first_rankzeroevaluationmatrixnegative) = S ((S (mdr_i_first_rankzeroevaluationmatrixnegative)) * mdr_vc_first_rankzeroevaluation)) /\ exists ff_q_mdr_first_rankzeroevaluationmatrixnegativeoutput. mdr_vb_first_rankzeroevaluation = ff_q_mdr_first_rankzeroevaluationmatrixnegativeoutput * S ((S (mdr_i_first_rankzeroevaluationmatrixnegative)) * mdr_vc_first_rankzeroevaluation) + (mdr_a_first_rankzeroevaluationmatrixnegative)))))))) /\ (exists mdr_b_first_rankzeroevaluationdeterminant mdr_c_first_rankzeroevaluationdeterminant mdr_l_first_rankzeroevaluationdeterminant mdr_i_first_rankzeroevaluationdeterminant. ((forall mdr_i_first_rankzeroevaluationdeterminanth. (exists mdr_gap_first_rankzeroevaluationdeterminanthi. mdr_gap_first_rankzeroevaluationdeterminanthi + S (mdr_i_first_rankzeroevaluationdeterminanth) = (mdr_l_first_rankzeroevaluationdeterminant)) -> exists mdr_d_first_rankzeroevaluationdeterminanth mdr_pb_first_rankzeroevaluationdeterminanth mdr_pc_first_rankzeroevaluationdeterminanth mdr_nb_first_rankzeroevaluationdeterminanth mdr_nc_first_rankzeroevaluationdeterminanth mdr_p_first_rankzeroevaluationdeterminanth mdr_n_first_rankzeroevaluationdeterminanth. ((exists mdr_z_first_rankzeroevaluationdeterminanthr. ((exists mdr_a_first_rankzeroevaluationdeterminanthrc mdr_b_first_rankzeroevaluationdeterminanthrc mdr_c_first_rankzeroevaluationdeterminanthrc mdr_e_first_rankzeroevaluationdeterminanthrc mdr_f_first_rankzeroevaluationdeterminanthrc. ((mdr_a_first_rankzeroevaluationdeterminanthrc = ((mdr_d_first_rankzeroevaluationdeterminanth) + (mdr_pb_first_rankzeroevaluationdeterminanth)) * S ((mdr_d_first_rankzeroevaluationdeterminanth) + (mdr_pb_first_rankzeroevaluationdeterminanth)) + ((mdr_pb_first_rankzeroevaluationdeterminanth) + (mdr_pb_first_rankzeroevaluationdeterminanth))) /\ ((mdr_b_first_rankzeroevaluationdeterminanthrc = ((mdr_pc_first_rankzeroevaluationdeterminanth) + (mdr_nb_first_rankzeroevaluationdeterminanth)) * S ((mdr_pc_first_rankzeroevaluationdeterminanth) + (mdr_nb_first_rankzeroevaluationdeterminanth)) + ((mdr_nb_first_rankzeroevaluationdeterminanth) + (mdr_nb_first_rankzeroevaluationdeterminanth))) /\ ((mdr_c_first_rankzeroevaluationdeterminanthrc = ((mdr_a_first_rankzeroevaluationdeterminanthrc) + (mdr_b_first_rankzeroevaluationdeterminanthrc)) * S ((mdr_a_first_rankzeroevaluationdeterminanthrc) + (mdr_b_first_rankzeroevaluationdeterminanthrc)) + ((mdr_b_first_rankzeroevaluationdeterminanthrc) + (mdr_b_first_rankzeroevaluationdeterminanthrc))) /\ ((mdr_e_first_rankzeroevaluationdeterminanthrc = ((mdr_p_first_rankzeroevaluationdeterminanth) + (mdr_n_first_rankzeroevaluationdeterminanth)) * S ((mdr_p_first_rankzeroevaluationdeterminanth) + (mdr_n_first_rankzeroevaluationdeterminanth)) + ((mdr_n_first_rankzeroevaluationdeterminanth) + (mdr_n_first_rankzeroevaluationdeterminanth))) /\ ((mdr_f_first_rankzeroevaluationdeterminanthrc = ((mdr_nc_first_rankzeroevaluationdeterminanth) + (mdr_e_first_rankzeroevaluationdeterminanthrc)) * S ((mdr_nc_first_rankzeroevaluationdeterminanth) + (mdr_e_first_rankzeroevaluationdeterminanthrc)) + ((mdr_e_first_rankzeroevaluationdeterminanthrc) + (mdr_e_first_rankzeroevaluationdeterminanthrc))) /\ ((mdr_z_first_rankzeroevaluationdeterminanthr) = ((mdr_c_first_rankzeroevaluationdeterminanthrc) + (mdr_f_first_rankzeroevaluationdeterminanthrc)) * S ((mdr_c_first_rankzeroevaluationdeterminanthrc) + (mdr_f_first_rankzeroevaluationdeterminanthrc)) + ((mdr_f_first_rankzeroevaluationdeterminanthrc) + (mdr_f_first_rankzeroevaluationdeterminanthrc))))))))) /\ (((exists ff_h_mdr_first_rankzeroevaluationdeterminanthrb. ff_h_mdr_first_rankzeroevaluationdeterminanthrb + S (mdr_z_first_rankzeroevaluationdeterminanthr) = S ((S (mdr_i_first_rankzeroevaluationdeterminanth)) * mdr_c_first_rankzeroevaluationdeterminant)) /\ exists ff_q_mdr_first_rankzeroevaluationdeterminanthrb. mdr_b_first_rankzeroevaluationdeterminant = ff_q_mdr_first_rankzeroevaluationdeterminanthrb * S ((S (mdr_i_first_rankzeroevaluationdeterminanth)) * mdr_c_first_rankzeroevaluationdeterminant) + (mdr_z_first_rankzeroevaluationdeterminanthr))))) /\ (((((mdr_d_first_rankzeroevaluationdeterminanth) = 0) /\ (((mdr_p_first_rankzeroevaluationdeterminanth) = 1) /\ ((mdr_n_first_rankzeroevaluationdeterminanth) = 0))) \/ exists mdr_q_first_rankzeroevaluationdeterminanths mdr_eb_first_rankzeroevaluationdeterminanths mdr_ec_first_rankzeroevaluationdeterminanths mdr_fb_first_rankzeroevaluationdeterminanths mdr_fc_first_rankzeroevaluationdeterminanths. (((mdr_d_first_rankzeroevaluationdeterminanth) = S (mdr_q_first_rankzeroevaluationdeterminanths)) /\ ((forall mdr_j_first_rankzeroevaluationdeterminanthsc. (exists mdr_gap_first_rankzeroevaluationdeterminanthscj. mdr_gap_first_rankzeroevaluationdeterminanthscj + S (mdr_j_first_rankzeroevaluationdeterminanthsc) = (S (mdr_q_first_rankzeroevaluationdeterminanths))) -> exists mdr_i_first_rankzeroevaluationdeterminanthsc mdr_up_first_rankzeroevaluationdeterminanthsc mdr_us_first_rankzeroevaluationdeterminanthsc mdr_un_first_rankzeroevaluationdeterminanthsc mdr_ut_first_rankzeroevaluationdeterminanthsc mdr_p_first_rankzeroevaluationdeterminanthsc mdr_n_first_rankzeroevaluationdeterminanthsc. ((exists mdr_gap_first_rankzeroevaluationdeterminanthsci. mdr_gap_first_rankzeroevaluationdeterminanthsci + S (mdr_i_first_rankzeroevaluationdeterminanthsc) = (mdr_i_first_rankzeroevaluationdeterminanth)) /\ ((exists mdr_z_first_rankzeroevaluationdeterminanthscr. ((exists mdr_a_first_rankzeroevaluationdeterminanthscrc mdr_b_first_rankzeroevaluationdeterminanthscrc mdr_c_first_rankzeroevaluationdeterminanthscrc mdr_e_first_rankzeroevaluationdeterminanthscrc mdr_f_first_rankzeroevaluationdeterminanthscrc. ((mdr_a_first_rankzeroevaluationdeterminanthscrc = ((mdr_q_first_rankzeroevaluationdeterminanths) + (mdr_up_first_rankzeroevaluationdeterminanthsc)) * S ((mdr_q_first_rankzeroevaluationdeterminanths) + (mdr_up_first_rankzeroevaluationdeterminanthsc)) + ((mdr_up_first_rankzeroevaluationdeterminanthsc) + (mdr_up_first_rankzeroevaluationdeterminanthsc))) /\ ((mdr_b_first_rankzeroevaluationdeterminanthscrc = ((mdr_us_first_rankzeroevaluationdeterminanthsc) + (mdr_un_first_rankzeroevaluationdeterminanthsc)) * S ((mdr_us_first_rankzeroevaluationdeterminanthsc) + (mdr_un_first_rankzeroevaluationdeterminanthsc)) + ((mdr_un_first_rankzeroevaluationdeterminanthsc) + (mdr_un_first_rankzeroevaluationdeterminanthsc))) /\ ((mdr_c_first_rankzeroevaluationdeterminanthscrc = ((mdr_a_first_rankzeroevaluationdeterminanthscrc) + (mdr_b_first_rankzeroevaluationdeterminanthscrc)) * S ((mdr_a_first_rankzeroevaluationdeterminanthscrc) + (mdr_b_first_rankzeroevaluationdeterminanthscrc)) + ((mdr_b_first_rankzeroevaluationdeterminanthscrc) + (mdr_b_first_rankzeroevaluationdeterminanthscrc))) /\ ((mdr_e_first_rankzeroevaluationdeterminanthscrc = ((mdr_p_first_rankzeroevaluationdeterminanthsc) + (mdr_n_first_rankzeroevaluationdeterminanthsc)) * S ((mdr_p_first_rankzeroevaluationdeterminanthsc) + (mdr_n_first_rankzeroevaluationdeterminanthsc)) + ((mdr_n_first_rankzeroevaluationdeterminanthsc) + (mdr_n_first_rankzeroevaluationdeterminanthsc))) /\ ((mdr_f_first_rankzeroevaluationdeterminanthscrc = ((mdr_ut_first_rankzeroevaluationdeterminanthsc) + (mdr_e_first_rankzeroevaluationdeterminanthscrc)) * S ((mdr_ut_first_rankzeroevaluationdeterminanthsc) + (mdr_e_first_rankzeroevaluationdeterminanthscrc)) + ((mdr_e_first_rankzeroevaluationdeterminanthscrc) + (mdr_e_first_rankzeroevaluationdeterminanthscrc))) /\ ((mdr_z_first_rankzeroevaluationdeterminanthscr) = ((mdr_c_first_rankzeroevaluationdeterminanthscrc) + (mdr_f_first_rankzeroevaluationdeterminanthscrc)) * S ((mdr_c_first_rankzeroevaluationdeterminanthscrc) + (mdr_f_first_rankzeroevaluationdeterminanthscrc)) + ((mdr_f_first_rankzeroevaluationdeterminanthscrc) + (mdr_f_first_rankzeroevaluationdeterminanthscrc))))))))) /\ (((exists ff_h_mdr_first_rankzeroevaluationdeterminanthscrb. ff_h_mdr_first_rankzeroevaluationdeterminanthscrb + S (mdr_z_first_rankzeroevaluationdeterminanthscr) = S ((S (mdr_i_first_rankzeroevaluationdeterminanthsc)) * mdr_c_first_rankzeroevaluationdeterminant)) /\ exists ff_q_mdr_first_rankzeroevaluationdeterminanthscrb. mdr_b_first_rankzeroevaluationdeterminant = ff_q_mdr_first_rankzeroevaluationdeterminanthscrb * S ((S (mdr_i_first_rankzeroevaluationdeterminanthsc)) * mdr_c_first_rankzeroevaluationdeterminant) + (mdr_z_first_rankzeroevaluationdeterminanthscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_first_rankzeroevaluationdeterminanthscm_positive. (exists ff_gap_mdm_lt_mdr_first_rankzeroevaluationdeterminanthscm_positive_index_bound. ff_gap_mdm_lt_mdr_first_rankzeroevaluationdeterminanthscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_first_rankzeroevaluationdeterminanthscm_positive) = ((mdr_q_first_rankzeroevaluationdeterminanths) * (mdr_q_first_rankzeroevaluationdeterminanths))) -> exists ff_row_mdm_prefix_mdr_first_rankzeroevaluationdeterminanthscm_positive ff_column_mdm_prefix_mdr_first_rankzeroevaluationdeterminanthscm_positive ff_value_mdm_prefix_mdr_first_rankzeroevaluationdeterminanthscm_positive. (ff_index_mdm_prefix_mdr_first_rankzeroevaluationdeterminanthscm_positive = (mdr_q_first_rankzeroevaluationdeterminanths) * ff_row_mdm_prefix_mdr_first_rankzeroevaluationdeterminanthscm_positive + ff_column_mdm_prefix_mdr_first_rankzeroevaluationdeterminanthscm_positive /\ ((exists ff_gap_mdm_lt_mdr_first_rankzeroevaluationdeterminanthscm_positive_column_bound. ff_gap_mdm_lt_mdr_first_rankzeroevaluationdeterminanthscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_first_rankzeroevaluationdeterminanthscm_positive) = (mdr_q_first_rankzeroevaluationdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_first_rankzeroevaluationdeterminanthscm_positive_cell ff_column_mdm_cell_mdr_first_rankzeroevaluationdeterminanthscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_first_rankzeroevaluationdeterminanthscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_first_rankzeroevaluationdeterminanthscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_first_rankzeroevaluationdeterminanthscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_first_rankzeroevaluationdeterminanthscm_positive_cell = ff_row_mdm_prefix_mdr_first_rankzeroevaluationdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_first_rankzeroevaluationdeterminanthscm_positive_cell_row_after. ff_gap_mdm_le_mdr_first_rankzeroevaluationdeterminanthscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_first_rankzeroevaluationdeterminanthscm_positive)) /\ ff_row_mdm_cell_mdr_first_rankzeroevaluationdeterminanthscm_positive_cell = S ff_row_mdm_prefix_mdr_first_rankzeroevaluationdeterminanthscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_first_rankzeroevaluationdeterminanthscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_first_rankzeroevaluationdeterminanthscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_first_rankzeroevaluationdeterminanthscm_positive) = (mdr_j_first_rankzeroevaluationdeterminanthsc)) /\ ff_column_mdm_cell_mdr_first_rankzeroevaluationdeterminanthscm_positive_cell = ff_column_mdm_prefix_mdr_first_rankzeroevaluationdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_first_rankzeroevaluationdeterminanthscm_positive_cell_column_after. ff_gap_mdm_le_mdr_first_rankzeroevaluationdeterminanthscm_positive_cell_column_after + (mdr_j_first_rankzeroevaluationdeterminanthsc) = (ff_column_mdm_prefix_mdr_first_rankzeroevaluationdeterminanthscm_positive)) /\ ff_column_mdm_cell_mdr_first_rankzeroevaluationdeterminanthscm_positive_cell = S ff_column_mdm_prefix_mdr_first_rankzeroevaluationdeterminanthscm_positive))) /\ (((exists ff_h_mdm_mdr_first_rankzeroevaluationdeterminanthscm_positive_cell_source. ff_h_mdm_mdr_first_rankzeroevaluationdeterminanthscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_first_rankzeroevaluationdeterminanthscm_positive) = S ((S ((ff_row_mdm_cell_mdr_first_rankzeroevaluationdeterminanthscm_positive_cell) * (S (mdr_q_first_rankzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_first_rankzeroevaluationdeterminanthscm_positive_cell))) * mdr_pc_first_rankzeroevaluationdeterminanth)) /\ exists ff_q_mdm_mdr_first_rankzeroevaluationdeterminanthscm_positive_cell_source. mdr_pb_first_rankzeroevaluationdeterminanth = ff_q_mdm_mdr_first_rankzeroevaluationdeterminanthscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_first_rankzeroevaluationdeterminanthscm_positive_cell) * (S (mdr_q_first_rankzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_first_rankzeroevaluationdeterminanthscm_positive_cell))) * mdr_pc_first_rankzeroevaluationdeterminanth) + (ff_value_mdm_prefix_mdr_first_rankzeroevaluationdeterminanthscm_positive)))))) /\ (((exists ff_h_mdm_mdr_first_rankzeroevaluationdeterminanthscm_positive_target. ff_h_mdm_mdr_first_rankzeroevaluationdeterminanthscm_positive_target + S (ff_value_mdm_prefix_mdr_first_rankzeroevaluationdeterminanthscm_positive) = S ((S (ff_index_mdm_prefix_mdr_first_rankzeroevaluationdeterminanthscm_positive)) * mdr_us_first_rankzeroevaluationdeterminanthsc)) /\ exists ff_q_mdm_mdr_first_rankzeroevaluationdeterminanthscm_positive_target. mdr_up_first_rankzeroevaluationdeterminanthsc = ff_q_mdm_mdr_first_rankzeroevaluationdeterminanthscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_first_rankzeroevaluationdeterminanthscm_positive)) * mdr_us_first_rankzeroevaluationdeterminanthsc) + (ff_value_mdm_prefix_mdr_first_rankzeroevaluationdeterminanthscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_first_rankzeroevaluationdeterminanthscm_negative. (exists ff_gap_mdm_lt_mdr_first_rankzeroevaluationdeterminanthscm_negative_index_bound. ff_gap_mdm_lt_mdr_first_rankzeroevaluationdeterminanthscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_first_rankzeroevaluationdeterminanthscm_negative) = ((mdr_q_first_rankzeroevaluationdeterminanths) * (mdr_q_first_rankzeroevaluationdeterminanths))) -> exists ff_row_mdm_prefix_mdr_first_rankzeroevaluationdeterminanthscm_negative ff_column_mdm_prefix_mdr_first_rankzeroevaluationdeterminanthscm_negative ff_value_mdm_prefix_mdr_first_rankzeroevaluationdeterminanthscm_negative. (ff_index_mdm_prefix_mdr_first_rankzeroevaluationdeterminanthscm_negative = (mdr_q_first_rankzeroevaluationdeterminanths) * ff_row_mdm_prefix_mdr_first_rankzeroevaluationdeterminanthscm_negative + ff_column_mdm_prefix_mdr_first_rankzeroevaluationdeterminanthscm_negative /\ ((exists ff_gap_mdm_lt_mdr_first_rankzeroevaluationdeterminanthscm_negative_column_bound. ff_gap_mdm_lt_mdr_first_rankzeroevaluationdeterminanthscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_first_rankzeroevaluationdeterminanthscm_negative) = (mdr_q_first_rankzeroevaluationdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_first_rankzeroevaluationdeterminanthscm_negative_cell ff_column_mdm_cell_mdr_first_rankzeroevaluationdeterminanthscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_first_rankzeroevaluationdeterminanthscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_first_rankzeroevaluationdeterminanthscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_first_rankzeroevaluationdeterminanthscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_first_rankzeroevaluationdeterminanthscm_negative_cell = ff_row_mdm_prefix_mdr_first_rankzeroevaluationdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_first_rankzeroevaluationdeterminanthscm_negative_cell_row_after. ff_gap_mdm_le_mdr_first_rankzeroevaluationdeterminanthscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_first_rankzeroevaluationdeterminanthscm_negative)) /\ ff_row_mdm_cell_mdr_first_rankzeroevaluationdeterminanthscm_negative_cell = S ff_row_mdm_prefix_mdr_first_rankzeroevaluationdeterminanthscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_first_rankzeroevaluationdeterminanthscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_first_rankzeroevaluationdeterminanthscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_first_rankzeroevaluationdeterminanthscm_negative) = (mdr_j_first_rankzeroevaluationdeterminanthsc)) /\ ff_column_mdm_cell_mdr_first_rankzeroevaluationdeterminanthscm_negative_cell = ff_column_mdm_prefix_mdr_first_rankzeroevaluationdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_first_rankzeroevaluationdeterminanthscm_negative_cell_column_after. ff_gap_mdm_le_mdr_first_rankzeroevaluationdeterminanthscm_negative_cell_column_after + (mdr_j_first_rankzeroevaluationdeterminanthsc) = (ff_column_mdm_prefix_mdr_first_rankzeroevaluationdeterminanthscm_negative)) /\ ff_column_mdm_cell_mdr_first_rankzeroevaluationdeterminanthscm_negative_cell = S ff_column_mdm_prefix_mdr_first_rankzeroevaluationdeterminanthscm_negative))) /\ (((exists ff_h_mdm_mdr_first_rankzeroevaluationdeterminanthscm_negative_cell_source. ff_h_mdm_mdr_first_rankzeroevaluationdeterminanthscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_first_rankzeroevaluationdeterminanthscm_negative) = S ((S ((ff_row_mdm_cell_mdr_first_rankzeroevaluationdeterminanthscm_negative_cell) * (S (mdr_q_first_rankzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_first_rankzeroevaluationdeterminanthscm_negative_cell))) * mdr_nc_first_rankzeroevaluationdeterminanth)) /\ exists ff_q_mdm_mdr_first_rankzeroevaluationdeterminanthscm_negative_cell_source. mdr_nb_first_rankzeroevaluationdeterminanth = ff_q_mdm_mdr_first_rankzeroevaluationdeterminanthscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_first_rankzeroevaluationdeterminanthscm_negative_cell) * (S (mdr_q_first_rankzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_first_rankzeroevaluationdeterminanthscm_negative_cell))) * mdr_nc_first_rankzeroevaluationdeterminanth) + (ff_value_mdm_prefix_mdr_first_rankzeroevaluationdeterminanthscm_negative)))))) /\ (((exists ff_h_mdm_mdr_first_rankzeroevaluationdeterminanthscm_negative_target. ff_h_mdm_mdr_first_rankzeroevaluationdeterminanthscm_negative_target + S (ff_value_mdm_prefix_mdr_first_rankzeroevaluationdeterminanthscm_negative) = S ((S (ff_index_mdm_prefix_mdr_first_rankzeroevaluationdeterminanthscm_negative)) * mdr_ut_first_rankzeroevaluationdeterminanthsc)) /\ exists ff_q_mdm_mdr_first_rankzeroevaluationdeterminanthscm_negative_target. mdr_un_first_rankzeroevaluationdeterminanthsc = ff_q_mdm_mdr_first_rankzeroevaluationdeterminanthscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_first_rankzeroevaluationdeterminanthscm_negative)) * mdr_ut_first_rankzeroevaluationdeterminanthsc) + (ff_value_mdm_prefix_mdr_first_rankzeroevaluationdeterminanthscm_negative))))))))) /\ ((((exists ff_h_mdr_first_rankzeroevaluationdeterminanthscp. ff_h_mdr_first_rankzeroevaluationdeterminanthscp + S (mdr_p_first_rankzeroevaluationdeterminanthsc) = S ((S (mdr_j_first_rankzeroevaluationdeterminanthsc)) * mdr_ec_first_rankzeroevaluationdeterminanths)) /\ exists ff_q_mdr_first_rankzeroevaluationdeterminanthscp. mdr_eb_first_rankzeroevaluationdeterminanths = ff_q_mdr_first_rankzeroevaluationdeterminanthscp * S ((S (mdr_j_first_rankzeroevaluationdeterminanthsc)) * mdr_ec_first_rankzeroevaluationdeterminanths) + (mdr_p_first_rankzeroevaluationdeterminanthsc))) /\ (((exists ff_h_mdr_first_rankzeroevaluationdeterminanthscn. ff_h_mdr_first_rankzeroevaluationdeterminanthscn + S (mdr_n_first_rankzeroevaluationdeterminanthsc) = S ((S (mdr_j_first_rankzeroevaluationdeterminanthsc)) * mdr_fc_first_rankzeroevaluationdeterminanths)) /\ exists ff_q_mdr_first_rankzeroevaluationdeterminanthscn. mdr_fb_first_rankzeroevaluationdeterminanths = ff_q_mdr_first_rankzeroevaluationdeterminanthscn * S ((S (mdr_j_first_rankzeroevaluationdeterminanthsc)) * mdr_fc_first_rankzeroevaluationdeterminanths) + (mdr_n_first_rankzeroevaluationdeterminanthsc)))))))) /\ (exists ff_ub_mce_fold_mdr_first_rankzeroevaluationdeterminanthsf ff_uc_mce_fold_mdr_first_rankzeroevaluationdeterminanthsf ff_vb_mce_fold_mdr_first_rankzeroevaluationdeterminanthsf ff_vc_mce_fold_mdr_first_rankzeroevaluationdeterminanthsf. ((forall ff_index_mce_alternating_mdr_first_rankzeroevaluationdeterminanthsf_prefix. (exists ff_gap_mce_mdr_first_rankzeroevaluationdeterminanthsf_prefix_index. ff_gap_mce_mdr_first_rankzeroevaluationdeterminanthsf_prefix_index + S (ff_index_mce_alternating_mdr_first_rankzeroevaluationdeterminanthsf_prefix) = (S (mdr_q_first_rankzeroevaluationdeterminanths))) -> exists ff_ap_mce_alternating_mdr_first_rankzeroevaluationdeterminanthsf_prefix ff_an_mce_alternating_mdr_first_rankzeroevaluationdeterminanthsf_prefix ff_bp_mce_alternating_mdr_first_rankzeroevaluationdeterminanthsf_prefix ff_bn_mce_alternating_mdr_first_rankzeroevaluationdeterminanthsf_prefix ff_p_mce_alternating_mdr_first_rankzeroevaluationdeterminanthsf_prefix ff_n_mce_alternating_mdr_first_rankzeroevaluationdeterminanthsf_prefix. ((((exists ff_h_mce_mdr_first_rankzeroevaluationdeterminanthsf_prefix_ap. ff_h_mce_mdr_first_rankzeroevaluationdeterminanthsf_prefix_ap + S (ff_ap_mce_alternating_mdr_first_rankzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_first_rankzeroevaluationdeterminanthsf_prefix)) * mdr_pc_first_rankzeroevaluationdeterminanth)) /\ exists ff_q_mce_mdr_first_rankzeroevaluationdeterminanthsf_prefix_ap. mdr_pb_first_rankzeroevaluationdeterminanth = ff_q_mce_mdr_first_rankzeroevaluationdeterminanthsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_first_rankzeroevaluationdeterminanthsf_prefix)) * mdr_pc_first_rankzeroevaluationdeterminanth) + (ff_ap_mce_alternating_mdr_first_rankzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_first_rankzeroevaluationdeterminanthsf_prefix_an. ff_h_mce_mdr_first_rankzeroevaluationdeterminanthsf_prefix_an + S (ff_an_mce_alternating_mdr_first_rankzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_first_rankzeroevaluationdeterminanthsf_prefix)) * mdr_nc_first_rankzeroevaluationdeterminanth)) /\ exists ff_q_mce_mdr_first_rankzeroevaluationdeterminanthsf_prefix_an. mdr_nb_first_rankzeroevaluationdeterminanth = ff_q_mce_mdr_first_rankzeroevaluationdeterminanthsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_first_rankzeroevaluationdeterminanthsf_prefix)) * mdr_nc_first_rankzeroevaluationdeterminanth) + (ff_an_mce_alternating_mdr_first_rankzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_first_rankzeroevaluationdeterminanthsf_prefix_bp. ff_h_mce_mdr_first_rankzeroevaluationdeterminanthsf_prefix_bp + S (ff_bp_mce_alternating_mdr_first_rankzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_first_rankzeroevaluationdeterminanthsf_prefix)) * mdr_ec_first_rankzeroevaluationdeterminanths)) /\ exists ff_q_mce_mdr_first_rankzeroevaluationdeterminanthsf_prefix_bp. mdr_eb_first_rankzeroevaluationdeterminanths = ff_q_mce_mdr_first_rankzeroevaluationdeterminanthsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_first_rankzeroevaluationdeterminanthsf_prefix)) * mdr_ec_first_rankzeroevaluationdeterminanths) + (ff_bp_mce_alternating_mdr_first_rankzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_first_rankzeroevaluationdeterminanthsf_prefix_bn. ff_h_mce_mdr_first_rankzeroevaluationdeterminanthsf_prefix_bn + S (ff_bn_mce_alternating_mdr_first_rankzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_first_rankzeroevaluationdeterminanthsf_prefix)) * mdr_fc_first_rankzeroevaluationdeterminanths)) /\ exists ff_q_mce_mdr_first_rankzeroevaluationdeterminanthsf_prefix_bn. mdr_fb_first_rankzeroevaluationdeterminanths = ff_q_mce_mdr_first_rankzeroevaluationdeterminanthsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_first_rankzeroevaluationdeterminanthsf_prefix)) * mdr_fc_first_rankzeroevaluationdeterminanths) + (ff_bn_mce_alternating_mdr_first_rankzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_first_rankzeroevaluationdeterminanthsf_prefix_positive. ff_h_mce_mdr_first_rankzeroevaluationdeterminanthsf_prefix_positive + S (ff_p_mce_alternating_mdr_first_rankzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_first_rankzeroevaluationdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_first_rankzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_first_rankzeroevaluationdeterminanthsf_prefix_positive. ff_ub_mce_fold_mdr_first_rankzeroevaluationdeterminanthsf = ff_q_mce_mdr_first_rankzeroevaluationdeterminanthsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_first_rankzeroevaluationdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_first_rankzeroevaluationdeterminanthsf) + (ff_p_mce_alternating_mdr_first_rankzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_first_rankzeroevaluationdeterminanthsf_prefix_negative. ff_h_mce_mdr_first_rankzeroevaluationdeterminanthsf_prefix_negative + S (ff_n_mce_alternating_mdr_first_rankzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_first_rankzeroevaluationdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_first_rankzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_first_rankzeroevaluationdeterminanthsf_prefix_negative. ff_vb_mce_fold_mdr_first_rankzeroevaluationdeterminanthsf = ff_q_mce_mdr_first_rankzeroevaluationdeterminanthsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_first_rankzeroevaluationdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_first_rankzeroevaluationdeterminanthsf) + (ff_n_mce_alternating_mdr_first_rankzeroevaluationdeterminanthsf_prefix))) /\ (((exists ff_even_mce_term_mdr_first_rankzeroevaluationdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_first_rankzeroevaluationdeterminanthsf_prefix = 2 * ff_even_mce_term_mdr_first_rankzeroevaluationdeterminanthsf_prefix_term) /\ (ff_p_mce_alternating_mdr_first_rankzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_first_rankzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_first_rankzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_first_rankzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_first_rankzeroevaluationdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_first_rankzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_first_rankzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_first_rankzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_first_rankzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_first_rankzeroevaluationdeterminanthsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_first_rankzeroevaluationdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_first_rankzeroevaluationdeterminanthsf_prefix = 2 * ff_odd_mce_term_mdr_first_rankzeroevaluationdeterminanthsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_first_rankzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_first_rankzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_first_rankzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_first_rankzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_first_rankzeroevaluationdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_first_rankzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_first_rankzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_first_rankzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_first_rankzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_first_rankzeroevaluationdeterminanthsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_first_rankzeroevaluationdeterminanthsf_positive ff_v_mce_mdr_first_rankzeroevaluationdeterminanthsf_positive. ((((exists ff_h_mce_mdr_first_rankzeroevaluationdeterminanthsf_positive_start. ff_h_mce_mdr_first_rankzeroevaluationdeterminanthsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_first_rankzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_first_rankzeroevaluationdeterminanthsf_positive_start. ff_u_mce_mdr_first_rankzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_first_rankzeroevaluationdeterminanthsf_positive_start * S ((S (0)) * ff_v_mce_mdr_first_rankzeroevaluationdeterminanthsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_first_rankzeroevaluationdeterminanthsf_positive_terminal. ff_h_mce_mdr_first_rankzeroevaluationdeterminanthsf_positive_terminal + S (mdr_p_first_rankzeroevaluationdeterminanth) = S ((S ((S (mdr_q_first_rankzeroevaluationdeterminanths)))) * ff_v_mce_mdr_first_rankzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_first_rankzeroevaluationdeterminanthsf_positive_terminal. ff_u_mce_mdr_first_rankzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_first_rankzeroevaluationdeterminanthsf_positive_terminal * S ((S ((S (mdr_q_first_rankzeroevaluationdeterminanths)))) * ff_v_mce_mdr_first_rankzeroevaluationdeterminanthsf_positive) + (mdr_p_first_rankzeroevaluationdeterminanth))) /\ forall ff_i_mce_mdr_first_rankzeroevaluationdeterminanthsf_positive. (exists ff_lt_mce_mdr_first_rankzeroevaluationdeterminanthsf_positive_bound. ff_lt_mce_mdr_first_rankzeroevaluationdeterminanthsf_positive_bound + S ff_i_mce_mdr_first_rankzeroevaluationdeterminanthsf_positive = (S (mdr_q_first_rankzeroevaluationdeterminanths))) -> exists ff_a_mce_mdr_first_rankzeroevaluationdeterminanthsf_positive ff_r_mce_mdr_first_rankzeroevaluationdeterminanthsf_positive ff_s_mce_mdr_first_rankzeroevaluationdeterminanthsf_positive. ((((exists ff_h_mce_mdr_first_rankzeroevaluationdeterminanthsf_positive_summand. ff_h_mce_mdr_first_rankzeroevaluationdeterminanthsf_positive_summand + S (ff_a_mce_mdr_first_rankzeroevaluationdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_first_rankzeroevaluationdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_first_rankzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_first_rankzeroevaluationdeterminanthsf_positive_summand. ff_ub_mce_fold_mdr_first_rankzeroevaluationdeterminanthsf = ff_q_mce_mdr_first_rankzeroevaluationdeterminanthsf_positive_summand * S ((S (ff_i_mce_mdr_first_rankzeroevaluationdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_first_rankzeroevaluationdeterminanthsf) + (ff_a_mce_mdr_first_rankzeroevaluationdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_first_rankzeroevaluationdeterminanthsf_positive_partial. ff_h_mce_mdr_first_rankzeroevaluationdeterminanthsf_positive_partial + S (ff_r_mce_mdr_first_rankzeroevaluationdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_first_rankzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_first_rankzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_first_rankzeroevaluationdeterminanthsf_positive_partial. ff_u_mce_mdr_first_rankzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_first_rankzeroevaluationdeterminanthsf_positive_partial * S ((S (ff_i_mce_mdr_first_rankzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_first_rankzeroevaluationdeterminanthsf_positive) + (ff_r_mce_mdr_first_rankzeroevaluationdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_first_rankzeroevaluationdeterminanthsf_positive_successor. ff_h_mce_mdr_first_rankzeroevaluationdeterminanthsf_positive_successor + S (ff_s_mce_mdr_first_rankzeroevaluationdeterminanthsf_positive) = S ((S (S ff_i_mce_mdr_first_rankzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_first_rankzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_first_rankzeroevaluationdeterminanthsf_positive_successor. ff_u_mce_mdr_first_rankzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_first_rankzeroevaluationdeterminanthsf_positive_successor * S ((S (S ff_i_mce_mdr_first_rankzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_first_rankzeroevaluationdeterminanthsf_positive) + (ff_s_mce_mdr_first_rankzeroevaluationdeterminanthsf_positive))) /\ ff_s_mce_mdr_first_rankzeroevaluationdeterminanthsf_positive = ff_r_mce_mdr_first_rankzeroevaluationdeterminanthsf_positive + ff_a_mce_mdr_first_rankzeroevaluationdeterminanthsf_positive)))))) /\ (exists ff_u_mce_mdr_first_rankzeroevaluationdeterminanthsf_negative ff_v_mce_mdr_first_rankzeroevaluationdeterminanthsf_negative. ((((exists ff_h_mce_mdr_first_rankzeroevaluationdeterminanthsf_negative_start. ff_h_mce_mdr_first_rankzeroevaluationdeterminanthsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_first_rankzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_first_rankzeroevaluationdeterminanthsf_negative_start. ff_u_mce_mdr_first_rankzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_first_rankzeroevaluationdeterminanthsf_negative_start * S ((S (0)) * ff_v_mce_mdr_first_rankzeroevaluationdeterminanthsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_first_rankzeroevaluationdeterminanthsf_negative_terminal. ff_h_mce_mdr_first_rankzeroevaluationdeterminanthsf_negative_terminal + S (mdr_n_first_rankzeroevaluationdeterminanth) = S ((S ((S (mdr_q_first_rankzeroevaluationdeterminanths)))) * ff_v_mce_mdr_first_rankzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_first_rankzeroevaluationdeterminanthsf_negative_terminal. ff_u_mce_mdr_first_rankzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_first_rankzeroevaluationdeterminanthsf_negative_terminal * S ((S ((S (mdr_q_first_rankzeroevaluationdeterminanths)))) * ff_v_mce_mdr_first_rankzeroevaluationdeterminanthsf_negative) + (mdr_n_first_rankzeroevaluationdeterminanth))) /\ forall ff_i_mce_mdr_first_rankzeroevaluationdeterminanthsf_negative. (exists ff_lt_mce_mdr_first_rankzeroevaluationdeterminanthsf_negative_bound. ff_lt_mce_mdr_first_rankzeroevaluationdeterminanthsf_negative_bound + S ff_i_mce_mdr_first_rankzeroevaluationdeterminanthsf_negative = (S (mdr_q_first_rankzeroevaluationdeterminanths))) -> exists ff_a_mce_mdr_first_rankzeroevaluationdeterminanthsf_negative ff_r_mce_mdr_first_rankzeroevaluationdeterminanthsf_negative ff_s_mce_mdr_first_rankzeroevaluationdeterminanthsf_negative. ((((exists ff_h_mce_mdr_first_rankzeroevaluationdeterminanthsf_negative_summand. ff_h_mce_mdr_first_rankzeroevaluationdeterminanthsf_negative_summand + S (ff_a_mce_mdr_first_rankzeroevaluationdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_first_rankzeroevaluationdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_first_rankzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_first_rankzeroevaluationdeterminanthsf_negative_summand. ff_vb_mce_fold_mdr_first_rankzeroevaluationdeterminanthsf = ff_q_mce_mdr_first_rankzeroevaluationdeterminanthsf_negative_summand * S ((S (ff_i_mce_mdr_first_rankzeroevaluationdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_first_rankzeroevaluationdeterminanthsf) + (ff_a_mce_mdr_first_rankzeroevaluationdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_first_rankzeroevaluationdeterminanthsf_negative_partial. ff_h_mce_mdr_first_rankzeroevaluationdeterminanthsf_negative_partial + S (ff_r_mce_mdr_first_rankzeroevaluationdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_first_rankzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_first_rankzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_first_rankzeroevaluationdeterminanthsf_negative_partial. ff_u_mce_mdr_first_rankzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_first_rankzeroevaluationdeterminanthsf_negative_partial * S ((S (ff_i_mce_mdr_first_rankzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_first_rankzeroevaluationdeterminanthsf_negative) + (ff_r_mce_mdr_first_rankzeroevaluationdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_first_rankzeroevaluationdeterminanthsf_negative_successor. ff_h_mce_mdr_first_rankzeroevaluationdeterminanthsf_negative_successor + S (ff_s_mce_mdr_first_rankzeroevaluationdeterminanthsf_negative) = S ((S (S ff_i_mce_mdr_first_rankzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_first_rankzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_first_rankzeroevaluationdeterminanthsf_negative_successor. ff_u_mce_mdr_first_rankzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_first_rankzeroevaluationdeterminanthsf_negative_successor * S ((S (S ff_i_mce_mdr_first_rankzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_first_rankzeroevaluationdeterminanthsf_negative) + (ff_s_mce_mdr_first_rankzeroevaluationdeterminanthsf_negative))) /\ ff_s_mce_mdr_first_rankzeroevaluationdeterminanthsf_negative = ff_r_mce_mdr_first_rankzeroevaluationdeterminanthsf_negative + ff_a_mce_mdr_first_rankzeroevaluationdeterminanthsf_negative))))))))))))))) /\ ((exists mdr_gap_first_rankzeroevaluationdeterminanti. mdr_gap_first_rankzeroevaluationdeterminanti + S (mdr_i_first_rankzeroevaluationdeterminant) = (mdr_l_first_rankzeroevaluationdeterminant)) /\ (exists mdr_z_first_rankzeroevaluationdeterminantr. ((exists mdr_a_first_rankzeroevaluationdeterminantrc mdr_b_first_rankzeroevaluationdeterminantrc mdr_c_first_rankzeroevaluationdeterminantrc mdr_e_first_rankzeroevaluationdeterminantrc mdr_f_first_rankzeroevaluationdeterminantrc. ((mdr_a_first_rankzeroevaluationdeterminantrc = ((mdr_q_first_rank) + (mdr_ub_first_rankzeroevaluation)) * S ((mdr_q_first_rank) + (mdr_ub_first_rankzeroevaluation)) + ((mdr_ub_first_rankzeroevaluation) + (mdr_ub_first_rankzeroevaluation))) /\ ((mdr_b_first_rankzeroevaluationdeterminantrc = ((mdr_uc_first_rankzeroevaluation) + (mdr_vb_first_rankzeroevaluation)) * S ((mdr_uc_first_rankzeroevaluation) + (mdr_vb_first_rankzeroevaluation)) + ((mdr_vb_first_rankzeroevaluation) + (mdr_vb_first_rankzeroevaluation))) /\ ((mdr_c_first_rankzeroevaluationdeterminantrc = ((mdr_a_first_rankzeroevaluationdeterminantrc) + (mdr_b_first_rankzeroevaluationdeterminantrc)) * S ((mdr_a_first_rankzeroevaluationdeterminantrc) + (mdr_b_first_rankzeroevaluationdeterminantrc)) + ((mdr_b_first_rankzeroevaluationdeterminantrc) + (mdr_b_first_rankzeroevaluationdeterminantrc))) /\ ((mdr_e_first_rankzeroevaluationdeterminantrc = ((mdr_p_first_rankzero) + (mdr_n_first_rankzero)) * S ((mdr_p_first_rankzero) + (mdr_n_first_rankzero)) + ((mdr_n_first_rankzero) + (mdr_n_first_rankzero))) /\ ((mdr_f_first_rankzeroevaluationdeterminantrc = ((mdr_vc_first_rankzeroevaluation) + (mdr_e_first_rankzeroevaluationdeterminantrc)) * S ((mdr_vc_first_rankzeroevaluation) + (mdr_e_first_rankzeroevaluationdeterminantrc)) + ((mdr_e_first_rankzeroevaluationdeterminantrc) + (mdr_e_first_rankzeroevaluationdeterminantrc))) /\ ((mdr_z_first_rankzeroevaluationdeterminantr) = ((mdr_c_first_rankzeroevaluationdeterminantrc) + (mdr_f_first_rankzeroevaluationdeterminantrc)) * S ((mdr_c_first_rankzeroevaluationdeterminantrc) + (mdr_f_first_rankzeroevaluationdeterminantrc)) + ((mdr_f_first_rankzeroevaluationdeterminantrc) + (mdr_f_first_rankzeroevaluationdeterminantrc))))))))) /\ (((exists ff_h_mdr_first_rankzeroevaluationdeterminantrb. ff_h_mdr_first_rankzeroevaluationdeterminantrb + S (mdr_z_first_rankzeroevaluationdeterminantr) = S ((S (mdr_i_first_rankzeroevaluationdeterminant)) * mdr_c_first_rankzeroevaluationdeterminant)) /\ exists ff_q_mdr_first_rankzeroevaluationdeterminantrb. mdr_b_first_rankzeroevaluationdeterminant = ff_q_mdr_first_rankzeroevaluationdeterminantrb * S ((S (mdr_i_first_rankzeroevaluationdeterminant)) * mdr_c_first_rankzeroevaluationdeterminant) + (mdr_z_first_rankzeroevaluationdeterminantr)))))))))) -> mdr_p_first_rankzero = mdr_n_first_rankzero)))))) -> (((exists mdr_gap_second_rankrows_bound. mdr_gap_second_rankrows_bound + (other) = (r)) /\ ((exists mdr_gap_second_rankcolumns_bound. mdr_gap_second_rankcolumns_bound + (other) = (w)) /\ ((exists mdr_rb_second_rankwitness mdr_rc_second_rankwitness mdr_cb_second_rankwitness mdr_cc_second_rankwitness. (((((forall fom_index_mrf_second_rankwitnessminorrowsbound. (exists fom_gap_mrf_second_rankwitnessminorrowsbound_index_bound. fom_gap_mrf_second_rankwitnessminorrowsbound_index_bound + S (fom_index_mrf_second_rankwitnessminorrowsbound) = other) -> exists fom_value_mrf_second_rankwitnessminorrowsbound. ((((exists fom_beta_height_mrf_second_rankwitnessminorrowsbound_entry. fom_beta_height_mrf_second_rankwitnessminorrowsbound_entry + S (fom_value_mrf_second_rankwitnessminorrowsbound) = S ((S (fom_index_mrf_second_rankwitnessminorrowsbound)) * mdr_rc_second_rankwitness)) /\ exists fom_beta_quotient_mrf_second_rankwitnessminorrowsbound_entry. mdr_rb_second_rankwitness = fom_beta_quotient_mrf_second_rankwitnessminorrowsbound_entry * S ((S (fom_index_mrf_second_rankwitnessminorrowsbound)) * mdr_rc_second_rankwitness) + (fom_value_mrf_second_rankwitnessminorrowsbound))) /\ (exists fom_gap_mrf_second_rankwitnessminorrowsbound_value_bound. fom_gap_mrf_second_rankwitnessminorrowsbound_value_bound + S (fom_value_mrf_second_rankwitnessminorrowsbound) = r))) /\ (forall mdr_i_second_rankwitnessminorrowsdistinct mdr_j_second_rankwitnessminorrowsdistinct mdr_a_second_rankwitnessminorrowsdistinct. (exists mdr_gap_second_rankwitnessminorrowsdistincti. mdr_gap_second_rankwitnessminorrowsdistincti + S (mdr_i_second_rankwitnessminorrowsdistinct) = (other)) -> (exists mdr_gap_second_rankwitnessminorrowsdistinctj. mdr_gap_second_rankwitnessminorrowsdistinctj + S (mdr_j_second_rankwitnessminorrowsdistinct) = (other)) -> (((exists ff_h_mdr_second_rankwitnessminorrowsdistinctfirst. ff_h_mdr_second_rankwitnessminorrowsdistinctfirst + S (mdr_a_second_rankwitnessminorrowsdistinct) = S ((S (mdr_i_second_rankwitnessminorrowsdistinct)) * mdr_rc_second_rankwitness)) /\ exists ff_q_mdr_second_rankwitnessminorrowsdistinctfirst. mdr_rb_second_rankwitness = ff_q_mdr_second_rankwitnessminorrowsdistinctfirst * S ((S (mdr_i_second_rankwitnessminorrowsdistinct)) * mdr_rc_second_rankwitness) + (mdr_a_second_rankwitnessminorrowsdistinct))) -> (((exists ff_h_mdr_second_rankwitnessminorrowsdistinctsecond. ff_h_mdr_second_rankwitnessminorrowsdistinctsecond + S (mdr_a_second_rankwitnessminorrowsdistinct) = S ((S (mdr_j_second_rankwitnessminorrowsdistinct)) * mdr_rc_second_rankwitness)) /\ exists ff_q_mdr_second_rankwitnessminorrowsdistinctsecond. mdr_rb_second_rankwitness = ff_q_mdr_second_rankwitnessminorrowsdistinctsecond * S ((S (mdr_j_second_rankwitnessminorrowsdistinct)) * mdr_rc_second_rankwitness) + (mdr_a_second_rankwitnessminorrowsdistinct))) -> mdr_i_second_rankwitnessminorrowsdistinct = mdr_j_second_rankwitnessminorrowsdistinct))) /\ ((((forall fom_index_mrf_second_rankwitnessminorcolumnsbound. (exists fom_gap_mrf_second_rankwitnessminorcolumnsbound_index_bound. fom_gap_mrf_second_rankwitnessminorcolumnsbound_index_bound + S (fom_index_mrf_second_rankwitnessminorcolumnsbound) = other) -> exists fom_value_mrf_second_rankwitnessminorcolumnsbound. ((((exists fom_beta_height_mrf_second_rankwitnessminorcolumnsbound_entry. fom_beta_height_mrf_second_rankwitnessminorcolumnsbound_entry + S (fom_value_mrf_second_rankwitnessminorcolumnsbound) = S ((S (fom_index_mrf_second_rankwitnessminorcolumnsbound)) * mdr_cc_second_rankwitness)) /\ exists fom_beta_quotient_mrf_second_rankwitnessminorcolumnsbound_entry. mdr_cb_second_rankwitness = fom_beta_quotient_mrf_second_rankwitnessminorcolumnsbound_entry * S ((S (fom_index_mrf_second_rankwitnessminorcolumnsbound)) * mdr_cc_second_rankwitness) + (fom_value_mrf_second_rankwitnessminorcolumnsbound))) /\ (exists fom_gap_mrf_second_rankwitnessminorcolumnsbound_value_bound. fom_gap_mrf_second_rankwitnessminorcolumnsbound_value_bound + S (fom_value_mrf_second_rankwitnessminorcolumnsbound) = w))) /\ (forall mdr_i_second_rankwitnessminorcolumnsdistinct mdr_j_second_rankwitnessminorcolumnsdistinct mdr_a_second_rankwitnessminorcolumnsdistinct. (exists mdr_gap_second_rankwitnessminorcolumnsdistincti. mdr_gap_second_rankwitnessminorcolumnsdistincti + S (mdr_i_second_rankwitnessminorcolumnsdistinct) = (other)) -> (exists mdr_gap_second_rankwitnessminorcolumnsdistinctj. mdr_gap_second_rankwitnessminorcolumnsdistinctj + S (mdr_j_second_rankwitnessminorcolumnsdistinct) = (other)) -> (((exists ff_h_mdr_second_rankwitnessminorcolumnsdistinctfirst. ff_h_mdr_second_rankwitnessminorcolumnsdistinctfirst + S (mdr_a_second_rankwitnessminorcolumnsdistinct) = S ((S (mdr_i_second_rankwitnessminorcolumnsdistinct)) * mdr_cc_second_rankwitness)) /\ exists ff_q_mdr_second_rankwitnessminorcolumnsdistinctfirst. mdr_cb_second_rankwitness = ff_q_mdr_second_rankwitnessminorcolumnsdistinctfirst * S ((S (mdr_i_second_rankwitnessminorcolumnsdistinct)) * mdr_cc_second_rankwitness) + (mdr_a_second_rankwitnessminorcolumnsdistinct))) -> (((exists ff_h_mdr_second_rankwitnessminorcolumnsdistinctsecond. ff_h_mdr_second_rankwitnessminorcolumnsdistinctsecond + S (mdr_a_second_rankwitnessminorcolumnsdistinct) = S ((S (mdr_j_second_rankwitnessminorcolumnsdistinct)) * mdr_cc_second_rankwitness)) /\ exists ff_q_mdr_second_rankwitnessminorcolumnsdistinctsecond. mdr_cb_second_rankwitness = ff_q_mdr_second_rankwitnessminorcolumnsdistinctsecond * S ((S (mdr_j_second_rankwitnessminorcolumnsdistinct)) * mdr_cc_second_rankwitness) + (mdr_a_second_rankwitnessminorcolumnsdistinct))) -> mdr_i_second_rankwitnessminorcolumnsdistinct = mdr_j_second_rankwitnessminorcolumnsdistinct))) /\ (exists mdr_p_second_rankwitnessminornonzero mdr_n_second_rankwitnessminornonzero. ((exists mdr_ub_second_rankwitnessminornonzeroevaluation mdr_uc_second_rankwitnessminornonzeroevaluation mdr_vb_second_rankwitnessminornonzeroevaluation mdr_vc_second_rankwitnessminornonzeroevaluation. ((((forall mdr_i_second_rankwitnessminornonzeroevaluationmatrixpositive. (exists mdr_gap_second_rankwitnessminornonzeroevaluationmatrixpositivebound. mdr_gap_second_rankwitnessminornonzeroevaluationmatrixpositivebound + S (mdr_i_second_rankwitnessminornonzeroevaluationmatrixpositive) = ((other) * (other))) -> exists mdr_a_second_rankwitnessminornonzeroevaluationmatrixpositive. (((exists mdr_r_second_rankwitnessminornonzeroevaluationmatrixpositivepoint mdr_s_second_rankwitnessminornonzeroevaluationmatrixpositivepoint mdr_u_second_rankwitnessminornonzeroevaluationmatrixpositivepoint mdr_v_second_rankwitnessminornonzeroevaluationmatrixpositivepoint. ((mdr_i_second_rankwitnessminornonzeroevaluationmatrixpositive = (other) * mdr_r_second_rankwitnessminornonzeroevaluationmatrixpositivepoint + mdr_s_second_rankwitnessminornonzeroevaluationmatrixpositivepoint) /\ ((exists mdr_gap_second_rankwitnessminornonzeroevaluationmatrixpositivepointcolumn. mdr_gap_second_rankwitnessminornonzeroevaluationmatrixpositivepointcolumn + S (mdr_s_second_rankwitnessminornonzeroevaluationmatrixpositivepoint) = (other)) /\ ((((exists ff_h_mdr_second_rankwitnessminornonzeroevaluationmatrixpositivepointrow_index. ff_h_mdr_second_rankwitnessminornonzeroevaluationmatrixpositivepointrow_index + S (mdr_u_second_rankwitnessminornonzeroevaluationmatrixpositivepoint) = S ((S (mdr_r_second_rankwitnessminornonzeroevaluationmatrixpositivepoint)) * mdr_rc_second_rankwitness)) /\ exists ff_q_mdr_second_rankwitnessminornonzeroevaluationmatrixpositivepointrow_index. mdr_rb_second_rankwitness = ff_q_mdr_second_rankwitnessminornonzeroevaluationmatrixpositivepointrow_index * S ((S (mdr_r_second_rankwitnessminornonzeroevaluationmatrixpositivepoint)) * mdr_rc_second_rankwitness) + (mdr_u_second_rankwitnessminornonzeroevaluationmatrixpositivepoint))) /\ ((((exists ff_h_mdr_second_rankwitnessminornonzeroevaluationmatrixpositivepointcolumn_index. ff_h_mdr_second_rankwitnessminornonzeroevaluationmatrixpositivepointcolumn_index + S (mdr_v_second_rankwitnessminornonzeroevaluationmatrixpositivepoint) = S ((S (mdr_s_second_rankwitnessminornonzeroevaluationmatrixpositivepoint)) * mdr_cc_second_rankwitness)) /\ exists ff_q_mdr_second_rankwitnessminornonzeroevaluationmatrixpositivepointcolumn_index. mdr_cb_second_rankwitness = ff_q_mdr_second_rankwitnessminornonzeroevaluationmatrixpositivepointcolumn_index * S ((S (mdr_s_second_rankwitnessminornonzeroevaluationmatrixpositivepoint)) * mdr_cc_second_rankwitness) + (mdr_v_second_rankwitnessminornonzeroevaluationmatrixpositivepoint))) /\ (((exists ff_h_mdr_second_rankwitnessminornonzeroevaluationmatrixpositivepointsource. ff_h_mdr_second_rankwitnessminornonzeroevaluationmatrixpositivepointsource + S (mdr_a_second_rankwitnessminornonzeroevaluationmatrixpositive) = S ((S ((mdr_u_second_rankwitnessminornonzeroevaluationmatrixpositivepoint) * (w) + (mdr_v_second_rankwitnessminornonzeroevaluationmatrixpositivepoint))) * pc)) /\ exists ff_q_mdr_second_rankwitnessminornonzeroevaluationmatrixpositivepointsource. pb = ff_q_mdr_second_rankwitnessminornonzeroevaluationmatrixpositivepointsource * S ((S ((mdr_u_second_rankwitnessminornonzeroevaluationmatrixpositivepoint) * (w) + (mdr_v_second_rankwitnessminornonzeroevaluationmatrixpositivepoint))) * pc) + (mdr_a_second_rankwitnessminornonzeroevaluationmatrixpositive)))))))) /\ (((exists ff_h_mdr_second_rankwitnessminornonzeroevaluationmatrixpositiveoutput. ff_h_mdr_second_rankwitnessminornonzeroevaluationmatrixpositiveoutput + S (mdr_a_second_rankwitnessminornonzeroevaluationmatrixpositive) = S ((S (mdr_i_second_rankwitnessminornonzeroevaluationmatrixpositive)) * mdr_uc_second_rankwitnessminornonzeroevaluation)) /\ exists ff_q_mdr_second_rankwitnessminornonzeroevaluationmatrixpositiveoutput. mdr_ub_second_rankwitnessminornonzeroevaluation = ff_q_mdr_second_rankwitnessminornonzeroevaluationmatrixpositiveoutput * S ((S (mdr_i_second_rankwitnessminornonzeroevaluationmatrixpositive)) * mdr_uc_second_rankwitnessminornonzeroevaluation) + (mdr_a_second_rankwitnessminornonzeroevaluationmatrixpositive)))))) /\ (forall mdr_i_second_rankwitnessminornonzeroevaluationmatrixnegative. (exists mdr_gap_second_rankwitnessminornonzeroevaluationmatrixnegativebound. mdr_gap_second_rankwitnessminornonzeroevaluationmatrixnegativebound + S (mdr_i_second_rankwitnessminornonzeroevaluationmatrixnegative) = ((other) * (other))) -> exists mdr_a_second_rankwitnessminornonzeroevaluationmatrixnegative. (((exists mdr_r_second_rankwitnessminornonzeroevaluationmatrixnegativepoint mdr_s_second_rankwitnessminornonzeroevaluationmatrixnegativepoint mdr_u_second_rankwitnessminornonzeroevaluationmatrixnegativepoint mdr_v_second_rankwitnessminornonzeroevaluationmatrixnegativepoint. ((mdr_i_second_rankwitnessminornonzeroevaluationmatrixnegative = (other) * mdr_r_second_rankwitnessminornonzeroevaluationmatrixnegativepoint + mdr_s_second_rankwitnessminornonzeroevaluationmatrixnegativepoint) /\ ((exists mdr_gap_second_rankwitnessminornonzeroevaluationmatrixnegativepointcolumn. mdr_gap_second_rankwitnessminornonzeroevaluationmatrixnegativepointcolumn + S (mdr_s_second_rankwitnessminornonzeroevaluationmatrixnegativepoint) = (other)) /\ ((((exists ff_h_mdr_second_rankwitnessminornonzeroevaluationmatrixnegativepointrow_index. ff_h_mdr_second_rankwitnessminornonzeroevaluationmatrixnegativepointrow_index + S (mdr_u_second_rankwitnessminornonzeroevaluationmatrixnegativepoint) = S ((S (mdr_r_second_rankwitnessminornonzeroevaluationmatrixnegativepoint)) * mdr_rc_second_rankwitness)) /\ exists ff_q_mdr_second_rankwitnessminornonzeroevaluationmatrixnegativepointrow_index. mdr_rb_second_rankwitness = ff_q_mdr_second_rankwitnessminornonzeroevaluationmatrixnegativepointrow_index * S ((S (mdr_r_second_rankwitnessminornonzeroevaluationmatrixnegativepoint)) * mdr_rc_second_rankwitness) + (mdr_u_second_rankwitnessminornonzeroevaluationmatrixnegativepoint))) /\ ((((exists ff_h_mdr_second_rankwitnessminornonzeroevaluationmatrixnegativepointcolumn_index. ff_h_mdr_second_rankwitnessminornonzeroevaluationmatrixnegativepointcolumn_index + S (mdr_v_second_rankwitnessminornonzeroevaluationmatrixnegativepoint) = S ((S (mdr_s_second_rankwitnessminornonzeroevaluationmatrixnegativepoint)) * mdr_cc_second_rankwitness)) /\ exists ff_q_mdr_second_rankwitnessminornonzeroevaluationmatrixnegativepointcolumn_index. mdr_cb_second_rankwitness = ff_q_mdr_second_rankwitnessminornonzeroevaluationmatrixnegativepointcolumn_index * S ((S (mdr_s_second_rankwitnessminornonzeroevaluationmatrixnegativepoint)) * mdr_cc_second_rankwitness) + (mdr_v_second_rankwitnessminornonzeroevaluationmatrixnegativepoint))) /\ (((exists ff_h_mdr_second_rankwitnessminornonzeroevaluationmatrixnegativepointsource. ff_h_mdr_second_rankwitnessminornonzeroevaluationmatrixnegativepointsource + S (mdr_a_second_rankwitnessminornonzeroevaluationmatrixnegative) = S ((S ((mdr_u_second_rankwitnessminornonzeroevaluationmatrixnegativepoint) * (w) + (mdr_v_second_rankwitnessminornonzeroevaluationmatrixnegativepoint))) * nc)) /\ exists ff_q_mdr_second_rankwitnessminornonzeroevaluationmatrixnegativepointsource. nb = ff_q_mdr_second_rankwitnessminornonzeroevaluationmatrixnegativepointsource * S ((S ((mdr_u_second_rankwitnessminornonzeroevaluationmatrixnegativepoint) * (w) + (mdr_v_second_rankwitnessminornonzeroevaluationmatrixnegativepoint))) * nc) + (mdr_a_second_rankwitnessminornonzeroevaluationmatrixnegative)))))))) /\ (((exists ff_h_mdr_second_rankwitnessminornonzeroevaluationmatrixnegativeoutput. ff_h_mdr_second_rankwitnessminornonzeroevaluationmatrixnegativeoutput + S (mdr_a_second_rankwitnessminornonzeroevaluationmatrixnegative) = S ((S (mdr_i_second_rankwitnessminornonzeroevaluationmatrixnegative)) * mdr_vc_second_rankwitnessminornonzeroevaluation)) /\ exists ff_q_mdr_second_rankwitnessminornonzeroevaluationmatrixnegativeoutput. mdr_vb_second_rankwitnessminornonzeroevaluation = ff_q_mdr_second_rankwitnessminornonzeroevaluationmatrixnegativeoutput * S ((S (mdr_i_second_rankwitnessminornonzeroevaluationmatrixnegative)) * mdr_vc_second_rankwitnessminornonzeroevaluation) + (mdr_a_second_rankwitnessminornonzeroevaluationmatrixnegative)))))))) /\ (exists mdr_b_second_rankwitnessminornonzeroevaluationdeterminant mdr_c_second_rankwitnessminornonzeroevaluationdeterminant mdr_l_second_rankwitnessminornonzeroevaluationdeterminant mdr_i_second_rankwitnessminornonzeroevaluationdeterminant. ((forall mdr_i_second_rankwitnessminornonzeroevaluationdeterminanth. (exists mdr_gap_second_rankwitnessminornonzeroevaluationdeterminanthi. mdr_gap_second_rankwitnessminornonzeroevaluationdeterminanthi + S (mdr_i_second_rankwitnessminornonzeroevaluationdeterminanth) = (mdr_l_second_rankwitnessminornonzeroevaluationdeterminant)) -> exists mdr_d_second_rankwitnessminornonzeroevaluationdeterminanth mdr_pb_second_rankwitnessminornonzeroevaluationdeterminanth mdr_pc_second_rankwitnessminornonzeroevaluationdeterminanth mdr_nb_second_rankwitnessminornonzeroevaluationdeterminanth mdr_nc_second_rankwitnessminornonzeroevaluationdeterminanth mdr_p_second_rankwitnessminornonzeroevaluationdeterminanth mdr_n_second_rankwitnessminornonzeroevaluationdeterminanth. ((exists mdr_z_second_rankwitnessminornonzeroevaluationdeterminanthr. ((exists mdr_a_second_rankwitnessminornonzeroevaluationdeterminanthrc mdr_b_second_rankwitnessminornonzeroevaluationdeterminanthrc mdr_c_second_rankwitnessminornonzeroevaluationdeterminanthrc mdr_e_second_rankwitnessminornonzeroevaluationdeterminanthrc mdr_f_second_rankwitnessminornonzeroevaluationdeterminanthrc. ((mdr_a_second_rankwitnessminornonzeroevaluationdeterminanthrc = ((mdr_d_second_rankwitnessminornonzeroevaluationdeterminanth) + (mdr_pb_second_rankwitnessminornonzeroevaluationdeterminanth)) * S ((mdr_d_second_rankwitnessminornonzeroevaluationdeterminanth) + (mdr_pb_second_rankwitnessminornonzeroevaluationdeterminanth)) + ((mdr_pb_second_rankwitnessminornonzeroevaluationdeterminanth) + (mdr_pb_second_rankwitnessminornonzeroevaluationdeterminanth))) /\ ((mdr_b_second_rankwitnessminornonzeroevaluationdeterminanthrc = ((mdr_pc_second_rankwitnessminornonzeroevaluationdeterminanth) + (mdr_nb_second_rankwitnessminornonzeroevaluationdeterminanth)) * S ((mdr_pc_second_rankwitnessminornonzeroevaluationdeterminanth) + (mdr_nb_second_rankwitnessminornonzeroevaluationdeterminanth)) + ((mdr_nb_second_rankwitnessminornonzeroevaluationdeterminanth) + (mdr_nb_second_rankwitnessminornonzeroevaluationdeterminanth))) /\ ((mdr_c_second_rankwitnessminornonzeroevaluationdeterminanthrc = ((mdr_a_second_rankwitnessminornonzeroevaluationdeterminanthrc) + (mdr_b_second_rankwitnessminornonzeroevaluationdeterminanthrc)) * S ((mdr_a_second_rankwitnessminornonzeroevaluationdeterminanthrc) + (mdr_b_second_rankwitnessminornonzeroevaluationdeterminanthrc)) + ((mdr_b_second_rankwitnessminornonzeroevaluationdeterminanthrc) + (mdr_b_second_rankwitnessminornonzeroevaluationdeterminanthrc))) /\ ((mdr_e_second_rankwitnessminornonzeroevaluationdeterminanthrc = ((mdr_p_second_rankwitnessminornonzeroevaluationdeterminanth) + (mdr_n_second_rankwitnessminornonzeroevaluationdeterminanth)) * S ((mdr_p_second_rankwitnessminornonzeroevaluationdeterminanth) + (mdr_n_second_rankwitnessminornonzeroevaluationdeterminanth)) + ((mdr_n_second_rankwitnessminornonzeroevaluationdeterminanth) + (mdr_n_second_rankwitnessminornonzeroevaluationdeterminanth))) /\ ((mdr_f_second_rankwitnessminornonzeroevaluationdeterminanthrc = ((mdr_nc_second_rankwitnessminornonzeroevaluationdeterminanth) + (mdr_e_second_rankwitnessminornonzeroevaluationdeterminanthrc)) * S ((mdr_nc_second_rankwitnessminornonzeroevaluationdeterminanth) + (mdr_e_second_rankwitnessminornonzeroevaluationdeterminanthrc)) + ((mdr_e_second_rankwitnessminornonzeroevaluationdeterminanthrc) + (mdr_e_second_rankwitnessminornonzeroevaluationdeterminanthrc))) /\ ((mdr_z_second_rankwitnessminornonzeroevaluationdeterminanthr) = ((mdr_c_second_rankwitnessminornonzeroevaluationdeterminanthrc) + (mdr_f_second_rankwitnessminornonzeroevaluationdeterminanthrc)) * S ((mdr_c_second_rankwitnessminornonzeroevaluationdeterminanthrc) + (mdr_f_second_rankwitnessminornonzeroevaluationdeterminanthrc)) + ((mdr_f_second_rankwitnessminornonzeroevaluationdeterminanthrc) + (mdr_f_second_rankwitnessminornonzeroevaluationdeterminanthrc))))))))) /\ (((exists ff_h_mdr_second_rankwitnessminornonzeroevaluationdeterminanthrb. ff_h_mdr_second_rankwitnessminornonzeroevaluationdeterminanthrb + S (mdr_z_second_rankwitnessminornonzeroevaluationdeterminanthr) = S ((S (mdr_i_second_rankwitnessminornonzeroevaluationdeterminanth)) * mdr_c_second_rankwitnessminornonzeroevaluationdeterminant)) /\ exists ff_q_mdr_second_rankwitnessminornonzeroevaluationdeterminanthrb. mdr_b_second_rankwitnessminornonzeroevaluationdeterminant = ff_q_mdr_second_rankwitnessminornonzeroevaluationdeterminanthrb * S ((S (mdr_i_second_rankwitnessminornonzeroevaluationdeterminanth)) * mdr_c_second_rankwitnessminornonzeroevaluationdeterminant) + (mdr_z_second_rankwitnessminornonzeroevaluationdeterminanthr))))) /\ (((((mdr_d_second_rankwitnessminornonzeroevaluationdeterminanth) = 0) /\ (((mdr_p_second_rankwitnessminornonzeroevaluationdeterminanth) = 1) /\ ((mdr_n_second_rankwitnessminornonzeroevaluationdeterminanth) = 0))) \/ exists mdr_q_second_rankwitnessminornonzeroevaluationdeterminanths mdr_eb_second_rankwitnessminornonzeroevaluationdeterminanths mdr_ec_second_rankwitnessminornonzeroevaluationdeterminanths mdr_fb_second_rankwitnessminornonzeroevaluationdeterminanths mdr_fc_second_rankwitnessminornonzeroevaluationdeterminanths. (((mdr_d_second_rankwitnessminornonzeroevaluationdeterminanth) = S (mdr_q_second_rankwitnessminornonzeroevaluationdeterminanths)) /\ ((forall mdr_j_second_rankwitnessminornonzeroevaluationdeterminanthsc. (exists mdr_gap_second_rankwitnessminornonzeroevaluationdeterminanthscj. mdr_gap_second_rankwitnessminornonzeroevaluationdeterminanthscj + S (mdr_j_second_rankwitnessminornonzeroevaluationdeterminanthsc) = (S (mdr_q_second_rankwitnessminornonzeroevaluationdeterminanths))) -> exists mdr_i_second_rankwitnessminornonzeroevaluationdeterminanthsc mdr_up_second_rankwitnessminornonzeroevaluationdeterminanthsc mdr_us_second_rankwitnessminornonzeroevaluationdeterminanthsc mdr_un_second_rankwitnessminornonzeroevaluationdeterminanthsc mdr_ut_second_rankwitnessminornonzeroevaluationdeterminanthsc mdr_p_second_rankwitnessminornonzeroevaluationdeterminanthsc mdr_n_second_rankwitnessminornonzeroevaluationdeterminanthsc. ((exists mdr_gap_second_rankwitnessminornonzeroevaluationdeterminanthsci. mdr_gap_second_rankwitnessminornonzeroevaluationdeterminanthsci + S (mdr_i_second_rankwitnessminornonzeroevaluationdeterminanthsc) = (mdr_i_second_rankwitnessminornonzeroevaluationdeterminanth)) /\ ((exists mdr_z_second_rankwitnessminornonzeroevaluationdeterminanthscr. ((exists mdr_a_second_rankwitnessminornonzeroevaluationdeterminanthscrc mdr_b_second_rankwitnessminornonzeroevaluationdeterminanthscrc mdr_c_second_rankwitnessminornonzeroevaluationdeterminanthscrc mdr_e_second_rankwitnessminornonzeroevaluationdeterminanthscrc mdr_f_second_rankwitnessminornonzeroevaluationdeterminanthscrc. ((mdr_a_second_rankwitnessminornonzeroevaluationdeterminanthscrc = ((mdr_q_second_rankwitnessminornonzeroevaluationdeterminanths) + (mdr_up_second_rankwitnessminornonzeroevaluationdeterminanthsc)) * S ((mdr_q_second_rankwitnessminornonzeroevaluationdeterminanths) + (mdr_up_second_rankwitnessminornonzeroevaluationdeterminanthsc)) + ((mdr_up_second_rankwitnessminornonzeroevaluationdeterminanthsc) + (mdr_up_second_rankwitnessminornonzeroevaluationdeterminanthsc))) /\ ((mdr_b_second_rankwitnessminornonzeroevaluationdeterminanthscrc = ((mdr_us_second_rankwitnessminornonzeroevaluationdeterminanthsc) + (mdr_un_second_rankwitnessminornonzeroevaluationdeterminanthsc)) * S ((mdr_us_second_rankwitnessminornonzeroevaluationdeterminanthsc) + (mdr_un_second_rankwitnessminornonzeroevaluationdeterminanthsc)) + ((mdr_un_second_rankwitnessminornonzeroevaluationdeterminanthsc) + (mdr_un_second_rankwitnessminornonzeroevaluationdeterminanthsc))) /\ ((mdr_c_second_rankwitnessminornonzeroevaluationdeterminanthscrc = ((mdr_a_second_rankwitnessminornonzeroevaluationdeterminanthscrc) + (mdr_b_second_rankwitnessminornonzeroevaluationdeterminanthscrc)) * S ((mdr_a_second_rankwitnessminornonzeroevaluationdeterminanthscrc) + (mdr_b_second_rankwitnessminornonzeroevaluationdeterminanthscrc)) + ((mdr_b_second_rankwitnessminornonzeroevaluationdeterminanthscrc) + (mdr_b_second_rankwitnessminornonzeroevaluationdeterminanthscrc))) /\ ((mdr_e_second_rankwitnessminornonzeroevaluationdeterminanthscrc = ((mdr_p_second_rankwitnessminornonzeroevaluationdeterminanthsc) + (mdr_n_second_rankwitnessminornonzeroevaluationdeterminanthsc)) * S ((mdr_p_second_rankwitnessminornonzeroevaluationdeterminanthsc) + (mdr_n_second_rankwitnessminornonzeroevaluationdeterminanthsc)) + ((mdr_n_second_rankwitnessminornonzeroevaluationdeterminanthsc) + (mdr_n_second_rankwitnessminornonzeroevaluationdeterminanthsc))) /\ ((mdr_f_second_rankwitnessminornonzeroevaluationdeterminanthscrc = ((mdr_ut_second_rankwitnessminornonzeroevaluationdeterminanthsc) + (mdr_e_second_rankwitnessminornonzeroevaluationdeterminanthscrc)) * S ((mdr_ut_second_rankwitnessminornonzeroevaluationdeterminanthsc) + (mdr_e_second_rankwitnessminornonzeroevaluationdeterminanthscrc)) + ((mdr_e_second_rankwitnessminornonzeroevaluationdeterminanthscrc) + (mdr_e_second_rankwitnessminornonzeroevaluationdeterminanthscrc))) /\ ((mdr_z_second_rankwitnessminornonzeroevaluationdeterminanthscr) = ((mdr_c_second_rankwitnessminornonzeroevaluationdeterminanthscrc) + (mdr_f_second_rankwitnessminornonzeroevaluationdeterminanthscrc)) * S ((mdr_c_second_rankwitnessminornonzeroevaluationdeterminanthscrc) + (mdr_f_second_rankwitnessminornonzeroevaluationdeterminanthscrc)) + ((mdr_f_second_rankwitnessminornonzeroevaluationdeterminanthscrc) + (mdr_f_second_rankwitnessminornonzeroevaluationdeterminanthscrc))))))))) /\ (((exists ff_h_mdr_second_rankwitnessminornonzeroevaluationdeterminanthscrb. ff_h_mdr_second_rankwitnessminornonzeroevaluationdeterminanthscrb + S (mdr_z_second_rankwitnessminornonzeroevaluationdeterminanthscr) = S ((S (mdr_i_second_rankwitnessminornonzeroevaluationdeterminanthsc)) * mdr_c_second_rankwitnessminornonzeroevaluationdeterminant)) /\ exists ff_q_mdr_second_rankwitnessminornonzeroevaluationdeterminanthscrb. mdr_b_second_rankwitnessminornonzeroevaluationdeterminant = ff_q_mdr_second_rankwitnessminornonzeroevaluationdeterminanthscrb * S ((S (mdr_i_second_rankwitnessminornonzeroevaluationdeterminanthsc)) * mdr_c_second_rankwitnessminornonzeroevaluationdeterminant) + (mdr_z_second_rankwitnessminornonzeroevaluationdeterminanthscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_second_rankwitnessminornonzeroevaluationdeterminanthscm_positive. (exists ff_gap_mdm_lt_mdr_second_rankwitnessminornonzeroevaluationdeterminanthscm_positive_index_bound. ff_gap_mdm_lt_mdr_second_rankwitnessminornonzeroevaluationdeterminanthscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_second_rankwitnessminornonzeroevaluationdeterminanthscm_positive) = ((mdr_q_second_rankwitnessminornonzeroevaluationdeterminanths) * (mdr_q_second_rankwitnessminornonzeroevaluationdeterminanths))) -> exists ff_row_mdm_prefix_mdr_second_rankwitnessminornonzeroevaluationdeterminanthscm_positive ff_column_mdm_prefix_mdr_second_rankwitnessminornonzeroevaluationdeterminanthscm_positive ff_value_mdm_prefix_mdr_second_rankwitnessminornonzeroevaluationdeterminanthscm_positive. (ff_index_mdm_prefix_mdr_second_rankwitnessminornonzeroevaluationdeterminanthscm_positive = (mdr_q_second_rankwitnessminornonzeroevaluationdeterminanths) * ff_row_mdm_prefix_mdr_second_rankwitnessminornonzeroevaluationdeterminanthscm_positive + ff_column_mdm_prefix_mdr_second_rankwitnessminornonzeroevaluationdeterminanthscm_positive /\ ((exists ff_gap_mdm_lt_mdr_second_rankwitnessminornonzeroevaluationdeterminanthscm_positive_column_bound. ff_gap_mdm_lt_mdr_second_rankwitnessminornonzeroevaluationdeterminanthscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_second_rankwitnessminornonzeroevaluationdeterminanthscm_positive) = (mdr_q_second_rankwitnessminornonzeroevaluationdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_second_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell ff_column_mdm_cell_mdr_second_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_second_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_second_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_second_rankwitnessminornonzeroevaluationdeterminanthscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_second_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell = ff_row_mdm_prefix_mdr_second_rankwitnessminornonzeroevaluationdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_second_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell_row_after. ff_gap_mdm_le_mdr_second_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_second_rankwitnessminornonzeroevaluationdeterminanthscm_positive)) /\ ff_row_mdm_cell_mdr_second_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell = S ff_row_mdm_prefix_mdr_second_rankwitnessminornonzeroevaluationdeterminanthscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_second_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_second_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_second_rankwitnessminornonzeroevaluationdeterminanthscm_positive) = (mdr_j_second_rankwitnessminornonzeroevaluationdeterminanthsc)) /\ ff_column_mdm_cell_mdr_second_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell = ff_column_mdm_prefix_mdr_second_rankwitnessminornonzeroevaluationdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_second_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell_column_after. ff_gap_mdm_le_mdr_second_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell_column_after + (mdr_j_second_rankwitnessminornonzeroevaluationdeterminanthsc) = (ff_column_mdm_prefix_mdr_second_rankwitnessminornonzeroevaluationdeterminanthscm_positive)) /\ ff_column_mdm_cell_mdr_second_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell = S ff_column_mdm_prefix_mdr_second_rankwitnessminornonzeroevaluationdeterminanthscm_positive))) /\ (((exists ff_h_mdm_mdr_second_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell_source. ff_h_mdm_mdr_second_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_second_rankwitnessminornonzeroevaluationdeterminanthscm_positive) = S ((S ((ff_row_mdm_cell_mdr_second_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell) * (S (mdr_q_second_rankwitnessminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_second_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell))) * mdr_pc_second_rankwitnessminornonzeroevaluationdeterminanth)) /\ exists ff_q_mdm_mdr_second_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell_source. mdr_pb_second_rankwitnessminornonzeroevaluationdeterminanth = ff_q_mdm_mdr_second_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_second_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell) * (S (mdr_q_second_rankwitnessminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_second_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell))) * mdr_pc_second_rankwitnessminornonzeroevaluationdeterminanth) + (ff_value_mdm_prefix_mdr_second_rankwitnessminornonzeroevaluationdeterminanthscm_positive)))))) /\ (((exists ff_h_mdm_mdr_second_rankwitnessminornonzeroevaluationdeterminanthscm_positive_target. ff_h_mdm_mdr_second_rankwitnessminornonzeroevaluationdeterminanthscm_positive_target + S (ff_value_mdm_prefix_mdr_second_rankwitnessminornonzeroevaluationdeterminanthscm_positive) = S ((S (ff_index_mdm_prefix_mdr_second_rankwitnessminornonzeroevaluationdeterminanthscm_positive)) * mdr_us_second_rankwitnessminornonzeroevaluationdeterminanthsc)) /\ exists ff_q_mdm_mdr_second_rankwitnessminornonzeroevaluationdeterminanthscm_positive_target. mdr_up_second_rankwitnessminornonzeroevaluationdeterminanthsc = ff_q_mdm_mdr_second_rankwitnessminornonzeroevaluationdeterminanthscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_second_rankwitnessminornonzeroevaluationdeterminanthscm_positive)) * mdr_us_second_rankwitnessminornonzeroevaluationdeterminanthsc) + (ff_value_mdm_prefix_mdr_second_rankwitnessminornonzeroevaluationdeterminanthscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_second_rankwitnessminornonzeroevaluationdeterminanthscm_negative. (exists ff_gap_mdm_lt_mdr_second_rankwitnessminornonzeroevaluationdeterminanthscm_negative_index_bound. ff_gap_mdm_lt_mdr_second_rankwitnessminornonzeroevaluationdeterminanthscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_second_rankwitnessminornonzeroevaluationdeterminanthscm_negative) = ((mdr_q_second_rankwitnessminornonzeroevaluationdeterminanths) * (mdr_q_second_rankwitnessminornonzeroevaluationdeterminanths))) -> exists ff_row_mdm_prefix_mdr_second_rankwitnessminornonzeroevaluationdeterminanthscm_negative ff_column_mdm_prefix_mdr_second_rankwitnessminornonzeroevaluationdeterminanthscm_negative ff_value_mdm_prefix_mdr_second_rankwitnessminornonzeroevaluationdeterminanthscm_negative. (ff_index_mdm_prefix_mdr_second_rankwitnessminornonzeroevaluationdeterminanthscm_negative = (mdr_q_second_rankwitnessminornonzeroevaluationdeterminanths) * ff_row_mdm_prefix_mdr_second_rankwitnessminornonzeroevaluationdeterminanthscm_negative + ff_column_mdm_prefix_mdr_second_rankwitnessminornonzeroevaluationdeterminanthscm_negative /\ ((exists ff_gap_mdm_lt_mdr_second_rankwitnessminornonzeroevaluationdeterminanthscm_negative_column_bound. ff_gap_mdm_lt_mdr_second_rankwitnessminornonzeroevaluationdeterminanthscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_second_rankwitnessminornonzeroevaluationdeterminanthscm_negative) = (mdr_q_second_rankwitnessminornonzeroevaluationdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_second_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell ff_column_mdm_cell_mdr_second_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_second_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_second_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_second_rankwitnessminornonzeroevaluationdeterminanthscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_second_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell = ff_row_mdm_prefix_mdr_second_rankwitnessminornonzeroevaluationdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_second_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell_row_after. ff_gap_mdm_le_mdr_second_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_second_rankwitnessminornonzeroevaluationdeterminanthscm_negative)) /\ ff_row_mdm_cell_mdr_second_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell = S ff_row_mdm_prefix_mdr_second_rankwitnessminornonzeroevaluationdeterminanthscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_second_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_second_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_second_rankwitnessminornonzeroevaluationdeterminanthscm_negative) = (mdr_j_second_rankwitnessminornonzeroevaluationdeterminanthsc)) /\ ff_column_mdm_cell_mdr_second_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell = ff_column_mdm_prefix_mdr_second_rankwitnessminornonzeroevaluationdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_second_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell_column_after. ff_gap_mdm_le_mdr_second_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell_column_after + (mdr_j_second_rankwitnessminornonzeroevaluationdeterminanthsc) = (ff_column_mdm_prefix_mdr_second_rankwitnessminornonzeroevaluationdeterminanthscm_negative)) /\ ff_column_mdm_cell_mdr_second_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell = S ff_column_mdm_prefix_mdr_second_rankwitnessminornonzeroevaluationdeterminanthscm_negative))) /\ (((exists ff_h_mdm_mdr_second_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell_source. ff_h_mdm_mdr_second_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_second_rankwitnessminornonzeroevaluationdeterminanthscm_negative) = S ((S ((ff_row_mdm_cell_mdr_second_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell) * (S (mdr_q_second_rankwitnessminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_second_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell))) * mdr_nc_second_rankwitnessminornonzeroevaluationdeterminanth)) /\ exists ff_q_mdm_mdr_second_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell_source. mdr_nb_second_rankwitnessminornonzeroevaluationdeterminanth = ff_q_mdm_mdr_second_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_second_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell) * (S (mdr_q_second_rankwitnessminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_second_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell))) * mdr_nc_second_rankwitnessminornonzeroevaluationdeterminanth) + (ff_value_mdm_prefix_mdr_second_rankwitnessminornonzeroevaluationdeterminanthscm_negative)))))) /\ (((exists ff_h_mdm_mdr_second_rankwitnessminornonzeroevaluationdeterminanthscm_negative_target. ff_h_mdm_mdr_second_rankwitnessminornonzeroevaluationdeterminanthscm_negative_target + S (ff_value_mdm_prefix_mdr_second_rankwitnessminornonzeroevaluationdeterminanthscm_negative) = S ((S (ff_index_mdm_prefix_mdr_second_rankwitnessminornonzeroevaluationdeterminanthscm_negative)) * mdr_ut_second_rankwitnessminornonzeroevaluationdeterminanthsc)) /\ exists ff_q_mdm_mdr_second_rankwitnessminornonzeroevaluationdeterminanthscm_negative_target. mdr_un_second_rankwitnessminornonzeroevaluationdeterminanthsc = ff_q_mdm_mdr_second_rankwitnessminornonzeroevaluationdeterminanthscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_second_rankwitnessminornonzeroevaluationdeterminanthscm_negative)) * mdr_ut_second_rankwitnessminornonzeroevaluationdeterminanthsc) + (ff_value_mdm_prefix_mdr_second_rankwitnessminornonzeroevaluationdeterminanthscm_negative))))))))) /\ ((((exists ff_h_mdr_second_rankwitnessminornonzeroevaluationdeterminanthscp. ff_h_mdr_second_rankwitnessminornonzeroevaluationdeterminanthscp + S (mdr_p_second_rankwitnessminornonzeroevaluationdeterminanthsc) = S ((S (mdr_j_second_rankwitnessminornonzeroevaluationdeterminanthsc)) * mdr_ec_second_rankwitnessminornonzeroevaluationdeterminanths)) /\ exists ff_q_mdr_second_rankwitnessminornonzeroevaluationdeterminanthscp. mdr_eb_second_rankwitnessminornonzeroevaluationdeterminanths = ff_q_mdr_second_rankwitnessminornonzeroevaluationdeterminanthscp * S ((S (mdr_j_second_rankwitnessminornonzeroevaluationdeterminanthsc)) * mdr_ec_second_rankwitnessminornonzeroevaluationdeterminanths) + (mdr_p_second_rankwitnessminornonzeroevaluationdeterminanthsc))) /\ (((exists ff_h_mdr_second_rankwitnessminornonzeroevaluationdeterminanthscn. ff_h_mdr_second_rankwitnessminornonzeroevaluationdeterminanthscn + S (mdr_n_second_rankwitnessminornonzeroevaluationdeterminanthsc) = S ((S (mdr_j_second_rankwitnessminornonzeroevaluationdeterminanthsc)) * mdr_fc_second_rankwitnessminornonzeroevaluationdeterminanths)) /\ exists ff_q_mdr_second_rankwitnessminornonzeroevaluationdeterminanthscn. mdr_fb_second_rankwitnessminornonzeroevaluationdeterminanths = ff_q_mdr_second_rankwitnessminornonzeroevaluationdeterminanthscn * S ((S (mdr_j_second_rankwitnessminornonzeroevaluationdeterminanthsc)) * mdr_fc_second_rankwitnessminornonzeroevaluationdeterminanths) + (mdr_n_second_rankwitnessminornonzeroevaluationdeterminanthsc)))))))) /\ (exists ff_ub_mce_fold_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf ff_uc_mce_fold_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf ff_vb_mce_fold_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf ff_vc_mce_fold_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf. ((forall ff_index_mce_alternating_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_prefix. (exists ff_gap_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_index. ff_gap_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_index + S (ff_index_mce_alternating_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) = (S (mdr_q_second_rankwitnessminornonzeroevaluationdeterminanths))) -> exists ff_ap_mce_alternating_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_prefix ff_an_mce_alternating_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_prefix ff_bp_mce_alternating_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_prefix ff_bn_mce_alternating_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_prefix ff_p_mce_alternating_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_prefix ff_n_mce_alternating_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_prefix. ((((exists ff_h_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_ap. ff_h_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_ap + S (ff_ap_mce_alternating_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_prefix)) * mdr_pc_second_rankwitnessminornonzeroevaluationdeterminanth)) /\ exists ff_q_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_ap. mdr_pb_second_rankwitnessminornonzeroevaluationdeterminanth = ff_q_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_prefix)) * mdr_pc_second_rankwitnessminornonzeroevaluationdeterminanth) + (ff_ap_mce_alternating_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_an. ff_h_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_an + S (ff_an_mce_alternating_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_prefix)) * mdr_nc_second_rankwitnessminornonzeroevaluationdeterminanth)) /\ exists ff_q_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_an. mdr_nb_second_rankwitnessminornonzeroevaluationdeterminanth = ff_q_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_prefix)) * mdr_nc_second_rankwitnessminornonzeroevaluationdeterminanth) + (ff_an_mce_alternating_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_bp. ff_h_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_bp + S (ff_bp_mce_alternating_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_prefix)) * mdr_ec_second_rankwitnessminornonzeroevaluationdeterminanths)) /\ exists ff_q_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_bp. mdr_eb_second_rankwitnessminornonzeroevaluationdeterminanths = ff_q_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_prefix)) * mdr_ec_second_rankwitnessminornonzeroevaluationdeterminanths) + (ff_bp_mce_alternating_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_bn. ff_h_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_bn + S (ff_bn_mce_alternating_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_prefix)) * mdr_fc_second_rankwitnessminornonzeroevaluationdeterminanths)) /\ exists ff_q_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_bn. mdr_fb_second_rankwitnessminornonzeroevaluationdeterminanths = ff_q_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_prefix)) * mdr_fc_second_rankwitnessminornonzeroevaluationdeterminanths) + (ff_bn_mce_alternating_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_positive. ff_h_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_positive + S (ff_p_mce_alternating_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_positive. ff_ub_mce_fold_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf) + (ff_p_mce_alternating_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_negative. ff_h_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_negative + S (ff_n_mce_alternating_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_negative. ff_vb_mce_fold_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf) + (ff_n_mce_alternating_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_prefix))) /\ (((exists ff_even_mce_term_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_prefix = 2 * ff_even_mce_term_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_term) /\ (ff_p_mce_alternating_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_prefix = 2 * ff_odd_mce_term_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_positive ff_v_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_positive. ((((exists ff_h_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_positive_start. ff_h_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_positive_start. ff_u_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_positive_start * S ((S (0)) * ff_v_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_positive_terminal. ff_h_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_positive_terminal + S (mdr_p_second_rankwitnessminornonzeroevaluationdeterminanth) = S ((S ((S (mdr_q_second_rankwitnessminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_positive_terminal. ff_u_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_positive_terminal * S ((S ((S (mdr_q_second_rankwitnessminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_positive) + (mdr_p_second_rankwitnessminornonzeroevaluationdeterminanth))) /\ forall ff_i_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_positive. (exists ff_lt_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_positive_bound. ff_lt_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_positive_bound + S ff_i_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_positive = (S (mdr_q_second_rankwitnessminornonzeroevaluationdeterminanths))) -> exists ff_a_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_positive ff_r_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_positive ff_s_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_positive. ((((exists ff_h_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_positive_summand. ff_h_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_positive_summand + S (ff_a_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_positive_summand. ff_ub_mce_fold_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_positive_summand * S ((S (ff_i_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf) + (ff_a_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_positive_partial. ff_h_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_positive_partial + S (ff_r_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_positive_partial. ff_u_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_positive_partial * S ((S (ff_i_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_positive) + (ff_r_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_positive_successor. ff_h_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_positive_successor + S (ff_s_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_positive) = S ((S (S ff_i_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_positive_successor. ff_u_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_positive_successor * S ((S (S ff_i_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_positive) + (ff_s_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_positive))) /\ ff_s_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_positive = ff_r_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_positive + ff_a_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_positive)))))) /\ (exists ff_u_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_negative ff_v_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_negative. ((((exists ff_h_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_negative_start. ff_h_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_negative_start. ff_u_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_negative_start * S ((S (0)) * ff_v_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_negative_terminal. ff_h_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_negative_terminal + S (mdr_n_second_rankwitnessminornonzeroevaluationdeterminanth) = S ((S ((S (mdr_q_second_rankwitnessminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_negative_terminal. ff_u_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_negative_terminal * S ((S ((S (mdr_q_second_rankwitnessminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_negative) + (mdr_n_second_rankwitnessminornonzeroevaluationdeterminanth))) /\ forall ff_i_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_negative. (exists ff_lt_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_negative_bound. ff_lt_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_negative_bound + S ff_i_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_negative = (S (mdr_q_second_rankwitnessminornonzeroevaluationdeterminanths))) -> exists ff_a_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_negative ff_r_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_negative ff_s_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_negative. ((((exists ff_h_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_negative_summand. ff_h_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_negative_summand + S (ff_a_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_negative_summand. ff_vb_mce_fold_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_negative_summand * S ((S (ff_i_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf) + (ff_a_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_negative_partial. ff_h_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_negative_partial + S (ff_r_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_negative_partial. ff_u_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_negative_partial * S ((S (ff_i_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_negative) + (ff_r_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_negative_successor. ff_h_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_negative_successor + S (ff_s_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_negative) = S ((S (S ff_i_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_negative_successor. ff_u_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_negative_successor * S ((S (S ff_i_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_negative) + (ff_s_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_negative))) /\ ff_s_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_negative = ff_r_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_negative + ff_a_mce_mdr_second_rankwitnessminornonzeroevaluationdeterminanthsf_negative))))))))))))))) /\ ((exists mdr_gap_second_rankwitnessminornonzeroevaluationdeterminanti. mdr_gap_second_rankwitnessminornonzeroevaluationdeterminanti + S (mdr_i_second_rankwitnessminornonzeroevaluationdeterminant) = (mdr_l_second_rankwitnessminornonzeroevaluationdeterminant)) /\ (exists mdr_z_second_rankwitnessminornonzeroevaluationdeterminantr. ((exists mdr_a_second_rankwitnessminornonzeroevaluationdeterminantrc mdr_b_second_rankwitnessminornonzeroevaluationdeterminantrc mdr_c_second_rankwitnessminornonzeroevaluationdeterminantrc mdr_e_second_rankwitnessminornonzeroevaluationdeterminantrc mdr_f_second_rankwitnessminornonzeroevaluationdeterminantrc. ((mdr_a_second_rankwitnessminornonzeroevaluationdeterminantrc = ((other) + (mdr_ub_second_rankwitnessminornonzeroevaluation)) * S ((other) + (mdr_ub_second_rankwitnessminornonzeroevaluation)) + ((mdr_ub_second_rankwitnessminornonzeroevaluation) + (mdr_ub_second_rankwitnessminornonzeroevaluation))) /\ ((mdr_b_second_rankwitnessminornonzeroevaluationdeterminantrc = ((mdr_uc_second_rankwitnessminornonzeroevaluation) + (mdr_vb_second_rankwitnessminornonzeroevaluation)) * S ((mdr_uc_second_rankwitnessminornonzeroevaluation) + (mdr_vb_second_rankwitnessminornonzeroevaluation)) + ((mdr_vb_second_rankwitnessminornonzeroevaluation) + (mdr_vb_second_rankwitnessminornonzeroevaluation))) /\ ((mdr_c_second_rankwitnessminornonzeroevaluationdeterminantrc = ((mdr_a_second_rankwitnessminornonzeroevaluationdeterminantrc) + (mdr_b_second_rankwitnessminornonzeroevaluationdeterminantrc)) * S ((mdr_a_second_rankwitnessminornonzeroevaluationdeterminantrc) + (mdr_b_second_rankwitnessminornonzeroevaluationdeterminantrc)) + ((mdr_b_second_rankwitnessminornonzeroevaluationdeterminantrc) + (mdr_b_second_rankwitnessminornonzeroevaluationdeterminantrc))) /\ ((mdr_e_second_rankwitnessminornonzeroevaluationdeterminantrc = ((mdr_p_second_rankwitnessminornonzero) + (mdr_n_second_rankwitnessminornonzero)) * S ((mdr_p_second_rankwitnessminornonzero) + (mdr_n_second_rankwitnessminornonzero)) + ((mdr_n_second_rankwitnessminornonzero) + (mdr_n_second_rankwitnessminornonzero))) /\ ((mdr_f_second_rankwitnessminornonzeroevaluationdeterminantrc = ((mdr_vc_second_rankwitnessminornonzeroevaluation) + (mdr_e_second_rankwitnessminornonzeroevaluationdeterminantrc)) * S ((mdr_vc_second_rankwitnessminornonzeroevaluation) + (mdr_e_second_rankwitnessminornonzeroevaluationdeterminantrc)) + ((mdr_e_second_rankwitnessminornonzeroevaluationdeterminantrc) + (mdr_e_second_rankwitnessminornonzeroevaluationdeterminantrc))) /\ ((mdr_z_second_rankwitnessminornonzeroevaluationdeterminantr) = ((mdr_c_second_rankwitnessminornonzeroevaluationdeterminantrc) + (mdr_f_second_rankwitnessminornonzeroevaluationdeterminantrc)) * S ((mdr_c_second_rankwitnessminornonzeroevaluationdeterminantrc) + (mdr_f_second_rankwitnessminornonzeroevaluationdeterminantrc)) + ((mdr_f_second_rankwitnessminornonzeroevaluationdeterminantrc) + (mdr_f_second_rankwitnessminornonzeroevaluationdeterminantrc))))))))) /\ (((exists ff_h_mdr_second_rankwitnessminornonzeroevaluationdeterminantrb. ff_h_mdr_second_rankwitnessminornonzeroevaluationdeterminantrb + S (mdr_z_second_rankwitnessminornonzeroevaluationdeterminantr) = S ((S (mdr_i_second_rankwitnessminornonzeroevaluationdeterminant)) * mdr_c_second_rankwitnessminornonzeroevaluationdeterminant)) /\ exists ff_q_mdr_second_rankwitnessminornonzeroevaluationdeterminantrb. mdr_b_second_rankwitnessminornonzeroevaluationdeterminant = ff_q_mdr_second_rankwitnessminornonzeroevaluationdeterminantrb * S ((S (mdr_i_second_rankwitnessminornonzeroevaluationdeterminant)) * mdr_c_second_rankwitnessminornonzeroevaluationdeterminant) + (mdr_z_second_rankwitnessminornonzeroevaluationdeterminantr)))))))))) /\ (~(mdr_p_second_rankwitnessminornonzero = mdr_n_second_rankwitnessminornonzero)))))))) /\ (forall mdr_q_second_rank. (exists mdr_gap_second_rankhigher. mdr_gap_second_rankhigher + S (other) = (mdr_q_second_rank)) -> (forall mdr_rb_second_rankzero mdr_rc_second_rankzero mdr_cb_second_rankzero mdr_cc_second_rankzero mdr_p_second_rankzero mdr_n_second_rankzero. (((forall fom_index_mrf_second_rankzerorowsbound. (exists fom_gap_mrf_second_rankzerorowsbound_index_bound. fom_gap_mrf_second_rankzerorowsbound_index_bound + S (fom_index_mrf_second_rankzerorowsbound) = mdr_q_second_rank) -> exists fom_value_mrf_second_rankzerorowsbound. ((((exists fom_beta_height_mrf_second_rankzerorowsbound_entry. fom_beta_height_mrf_second_rankzerorowsbound_entry + S (fom_value_mrf_second_rankzerorowsbound) = S ((S (fom_index_mrf_second_rankzerorowsbound)) * mdr_rc_second_rankzero)) /\ exists fom_beta_quotient_mrf_second_rankzerorowsbound_entry. mdr_rb_second_rankzero = fom_beta_quotient_mrf_second_rankzerorowsbound_entry * S ((S (fom_index_mrf_second_rankzerorowsbound)) * mdr_rc_second_rankzero) + (fom_value_mrf_second_rankzerorowsbound))) /\ (exists fom_gap_mrf_second_rankzerorowsbound_value_bound. fom_gap_mrf_second_rankzerorowsbound_value_bound + S (fom_value_mrf_second_rankzerorowsbound) = r))) /\ (forall mdr_i_second_rankzerorowsdistinct mdr_j_second_rankzerorowsdistinct mdr_a_second_rankzerorowsdistinct. (exists mdr_gap_second_rankzerorowsdistincti. mdr_gap_second_rankzerorowsdistincti + S (mdr_i_second_rankzerorowsdistinct) = (mdr_q_second_rank)) -> (exists mdr_gap_second_rankzerorowsdistinctj. mdr_gap_second_rankzerorowsdistinctj + S (mdr_j_second_rankzerorowsdistinct) = (mdr_q_second_rank)) -> (((exists ff_h_mdr_second_rankzerorowsdistinctfirst. ff_h_mdr_second_rankzerorowsdistinctfirst + S (mdr_a_second_rankzerorowsdistinct) = S ((S (mdr_i_second_rankzerorowsdistinct)) * mdr_rc_second_rankzero)) /\ exists ff_q_mdr_second_rankzerorowsdistinctfirst. mdr_rb_second_rankzero = ff_q_mdr_second_rankzerorowsdistinctfirst * S ((S (mdr_i_second_rankzerorowsdistinct)) * mdr_rc_second_rankzero) + (mdr_a_second_rankzerorowsdistinct))) -> (((exists ff_h_mdr_second_rankzerorowsdistinctsecond. ff_h_mdr_second_rankzerorowsdistinctsecond + S (mdr_a_second_rankzerorowsdistinct) = S ((S (mdr_j_second_rankzerorowsdistinct)) * mdr_rc_second_rankzero)) /\ exists ff_q_mdr_second_rankzerorowsdistinctsecond. mdr_rb_second_rankzero = ff_q_mdr_second_rankzerorowsdistinctsecond * S ((S (mdr_j_second_rankzerorowsdistinct)) * mdr_rc_second_rankzero) + (mdr_a_second_rankzerorowsdistinct))) -> mdr_i_second_rankzerorowsdistinct = mdr_j_second_rankzerorowsdistinct))) -> (((forall fom_index_mrf_second_rankzerocolumnsbound. (exists fom_gap_mrf_second_rankzerocolumnsbound_index_bound. fom_gap_mrf_second_rankzerocolumnsbound_index_bound + S (fom_index_mrf_second_rankzerocolumnsbound) = mdr_q_second_rank) -> exists fom_value_mrf_second_rankzerocolumnsbound. ((((exists fom_beta_height_mrf_second_rankzerocolumnsbound_entry. fom_beta_height_mrf_second_rankzerocolumnsbound_entry + S (fom_value_mrf_second_rankzerocolumnsbound) = S ((S (fom_index_mrf_second_rankzerocolumnsbound)) * mdr_cc_second_rankzero)) /\ exists fom_beta_quotient_mrf_second_rankzerocolumnsbound_entry. mdr_cb_second_rankzero = fom_beta_quotient_mrf_second_rankzerocolumnsbound_entry * S ((S (fom_index_mrf_second_rankzerocolumnsbound)) * mdr_cc_second_rankzero) + (fom_value_mrf_second_rankzerocolumnsbound))) /\ (exists fom_gap_mrf_second_rankzerocolumnsbound_value_bound. fom_gap_mrf_second_rankzerocolumnsbound_value_bound + S (fom_value_mrf_second_rankzerocolumnsbound) = w))) /\ (forall mdr_i_second_rankzerocolumnsdistinct mdr_j_second_rankzerocolumnsdistinct mdr_a_second_rankzerocolumnsdistinct. (exists mdr_gap_second_rankzerocolumnsdistincti. mdr_gap_second_rankzerocolumnsdistincti + S (mdr_i_second_rankzerocolumnsdistinct) = (mdr_q_second_rank)) -> (exists mdr_gap_second_rankzerocolumnsdistinctj. mdr_gap_second_rankzerocolumnsdistinctj + S (mdr_j_second_rankzerocolumnsdistinct) = (mdr_q_second_rank)) -> (((exists ff_h_mdr_second_rankzerocolumnsdistinctfirst. ff_h_mdr_second_rankzerocolumnsdistinctfirst + S (mdr_a_second_rankzerocolumnsdistinct) = S ((S (mdr_i_second_rankzerocolumnsdistinct)) * mdr_cc_second_rankzero)) /\ exists ff_q_mdr_second_rankzerocolumnsdistinctfirst. mdr_cb_second_rankzero = ff_q_mdr_second_rankzerocolumnsdistinctfirst * S ((S (mdr_i_second_rankzerocolumnsdistinct)) * mdr_cc_second_rankzero) + (mdr_a_second_rankzerocolumnsdistinct))) -> (((exists ff_h_mdr_second_rankzerocolumnsdistinctsecond. ff_h_mdr_second_rankzerocolumnsdistinctsecond + S (mdr_a_second_rankzerocolumnsdistinct) = S ((S (mdr_j_second_rankzerocolumnsdistinct)) * mdr_cc_second_rankzero)) /\ exists ff_q_mdr_second_rankzerocolumnsdistinctsecond. mdr_cb_second_rankzero = ff_q_mdr_second_rankzerocolumnsdistinctsecond * S ((S (mdr_j_second_rankzerocolumnsdistinct)) * mdr_cc_second_rankzero) + (mdr_a_second_rankzerocolumnsdistinct))) -> mdr_i_second_rankzerocolumnsdistinct = mdr_j_second_rankzerocolumnsdistinct))) -> (exists mdr_ub_second_rankzeroevaluation mdr_uc_second_rankzeroevaluation mdr_vb_second_rankzeroevaluation mdr_vc_second_rankzeroevaluation. ((((forall mdr_i_second_rankzeroevaluationmatrixpositive. (exists mdr_gap_second_rankzeroevaluationmatrixpositivebound. mdr_gap_second_rankzeroevaluationmatrixpositivebound + S (mdr_i_second_rankzeroevaluationmatrixpositive) = ((mdr_q_second_rank) * (mdr_q_second_rank))) -> exists mdr_a_second_rankzeroevaluationmatrixpositive. (((exists mdr_r_second_rankzeroevaluationmatrixpositivepoint mdr_s_second_rankzeroevaluationmatrixpositivepoint mdr_u_second_rankzeroevaluationmatrixpositivepoint mdr_v_second_rankzeroevaluationmatrixpositivepoint. ((mdr_i_second_rankzeroevaluationmatrixpositive = (mdr_q_second_rank) * mdr_r_second_rankzeroevaluationmatrixpositivepoint + mdr_s_second_rankzeroevaluationmatrixpositivepoint) /\ ((exists mdr_gap_second_rankzeroevaluationmatrixpositivepointcolumn. mdr_gap_second_rankzeroevaluationmatrixpositivepointcolumn + S (mdr_s_second_rankzeroevaluationmatrixpositivepoint) = (mdr_q_second_rank)) /\ ((((exists ff_h_mdr_second_rankzeroevaluationmatrixpositivepointrow_index. ff_h_mdr_second_rankzeroevaluationmatrixpositivepointrow_index + S (mdr_u_second_rankzeroevaluationmatrixpositivepoint) = S ((S (mdr_r_second_rankzeroevaluationmatrixpositivepoint)) * mdr_rc_second_rankzero)) /\ exists ff_q_mdr_second_rankzeroevaluationmatrixpositivepointrow_index. mdr_rb_second_rankzero = ff_q_mdr_second_rankzeroevaluationmatrixpositivepointrow_index * S ((S (mdr_r_second_rankzeroevaluationmatrixpositivepoint)) * mdr_rc_second_rankzero) + (mdr_u_second_rankzeroevaluationmatrixpositivepoint))) /\ ((((exists ff_h_mdr_second_rankzeroevaluationmatrixpositivepointcolumn_index. ff_h_mdr_second_rankzeroevaluationmatrixpositivepointcolumn_index + S (mdr_v_second_rankzeroevaluationmatrixpositivepoint) = S ((S (mdr_s_second_rankzeroevaluationmatrixpositivepoint)) * mdr_cc_second_rankzero)) /\ exists ff_q_mdr_second_rankzeroevaluationmatrixpositivepointcolumn_index. mdr_cb_second_rankzero = ff_q_mdr_second_rankzeroevaluationmatrixpositivepointcolumn_index * S ((S (mdr_s_second_rankzeroevaluationmatrixpositivepoint)) * mdr_cc_second_rankzero) + (mdr_v_second_rankzeroevaluationmatrixpositivepoint))) /\ (((exists ff_h_mdr_second_rankzeroevaluationmatrixpositivepointsource. ff_h_mdr_second_rankzeroevaluationmatrixpositivepointsource + S (mdr_a_second_rankzeroevaluationmatrixpositive) = S ((S ((mdr_u_second_rankzeroevaluationmatrixpositivepoint) * (w) + (mdr_v_second_rankzeroevaluationmatrixpositivepoint))) * pc)) /\ exists ff_q_mdr_second_rankzeroevaluationmatrixpositivepointsource. pb = ff_q_mdr_second_rankzeroevaluationmatrixpositivepointsource * S ((S ((mdr_u_second_rankzeroevaluationmatrixpositivepoint) * (w) + (mdr_v_second_rankzeroevaluationmatrixpositivepoint))) * pc) + (mdr_a_second_rankzeroevaluationmatrixpositive)))))))) /\ (((exists ff_h_mdr_second_rankzeroevaluationmatrixpositiveoutput. ff_h_mdr_second_rankzeroevaluationmatrixpositiveoutput + S (mdr_a_second_rankzeroevaluationmatrixpositive) = S ((S (mdr_i_second_rankzeroevaluationmatrixpositive)) * mdr_uc_second_rankzeroevaluation)) /\ exists ff_q_mdr_second_rankzeroevaluationmatrixpositiveoutput. mdr_ub_second_rankzeroevaluation = ff_q_mdr_second_rankzeroevaluationmatrixpositiveoutput * S ((S (mdr_i_second_rankzeroevaluationmatrixpositive)) * mdr_uc_second_rankzeroevaluation) + (mdr_a_second_rankzeroevaluationmatrixpositive)))))) /\ (forall mdr_i_second_rankzeroevaluationmatrixnegative. (exists mdr_gap_second_rankzeroevaluationmatrixnegativebound. mdr_gap_second_rankzeroevaluationmatrixnegativebound + S (mdr_i_second_rankzeroevaluationmatrixnegative) = ((mdr_q_second_rank) * (mdr_q_second_rank))) -> exists mdr_a_second_rankzeroevaluationmatrixnegative. (((exists mdr_r_second_rankzeroevaluationmatrixnegativepoint mdr_s_second_rankzeroevaluationmatrixnegativepoint mdr_u_second_rankzeroevaluationmatrixnegativepoint mdr_v_second_rankzeroevaluationmatrixnegativepoint. ((mdr_i_second_rankzeroevaluationmatrixnegative = (mdr_q_second_rank) * mdr_r_second_rankzeroevaluationmatrixnegativepoint + mdr_s_second_rankzeroevaluationmatrixnegativepoint) /\ ((exists mdr_gap_second_rankzeroevaluationmatrixnegativepointcolumn. mdr_gap_second_rankzeroevaluationmatrixnegativepointcolumn + S (mdr_s_second_rankzeroevaluationmatrixnegativepoint) = (mdr_q_second_rank)) /\ ((((exists ff_h_mdr_second_rankzeroevaluationmatrixnegativepointrow_index. ff_h_mdr_second_rankzeroevaluationmatrixnegativepointrow_index + S (mdr_u_second_rankzeroevaluationmatrixnegativepoint) = S ((S (mdr_r_second_rankzeroevaluationmatrixnegativepoint)) * mdr_rc_second_rankzero)) /\ exists ff_q_mdr_second_rankzeroevaluationmatrixnegativepointrow_index. mdr_rb_second_rankzero = ff_q_mdr_second_rankzeroevaluationmatrixnegativepointrow_index * S ((S (mdr_r_second_rankzeroevaluationmatrixnegativepoint)) * mdr_rc_second_rankzero) + (mdr_u_second_rankzeroevaluationmatrixnegativepoint))) /\ ((((exists ff_h_mdr_second_rankzeroevaluationmatrixnegativepointcolumn_index. ff_h_mdr_second_rankzeroevaluationmatrixnegativepointcolumn_index + S (mdr_v_second_rankzeroevaluationmatrixnegativepoint) = S ((S (mdr_s_second_rankzeroevaluationmatrixnegativepoint)) * mdr_cc_second_rankzero)) /\ exists ff_q_mdr_second_rankzeroevaluationmatrixnegativepointcolumn_index. mdr_cb_second_rankzero = ff_q_mdr_second_rankzeroevaluationmatrixnegativepointcolumn_index * S ((S (mdr_s_second_rankzeroevaluationmatrixnegativepoint)) * mdr_cc_second_rankzero) + (mdr_v_second_rankzeroevaluationmatrixnegativepoint))) /\ (((exists ff_h_mdr_second_rankzeroevaluationmatrixnegativepointsource. ff_h_mdr_second_rankzeroevaluationmatrixnegativepointsource + S (mdr_a_second_rankzeroevaluationmatrixnegative) = S ((S ((mdr_u_second_rankzeroevaluationmatrixnegativepoint) * (w) + (mdr_v_second_rankzeroevaluationmatrixnegativepoint))) * nc)) /\ exists ff_q_mdr_second_rankzeroevaluationmatrixnegativepointsource. nb = ff_q_mdr_second_rankzeroevaluationmatrixnegativepointsource * S ((S ((mdr_u_second_rankzeroevaluationmatrixnegativepoint) * (w) + (mdr_v_second_rankzeroevaluationmatrixnegativepoint))) * nc) + (mdr_a_second_rankzeroevaluationmatrixnegative)))))))) /\ (((exists ff_h_mdr_second_rankzeroevaluationmatrixnegativeoutput. ff_h_mdr_second_rankzeroevaluationmatrixnegativeoutput + S (mdr_a_second_rankzeroevaluationmatrixnegative) = S ((S (mdr_i_second_rankzeroevaluationmatrixnegative)) * mdr_vc_second_rankzeroevaluation)) /\ exists ff_q_mdr_second_rankzeroevaluationmatrixnegativeoutput. mdr_vb_second_rankzeroevaluation = ff_q_mdr_second_rankzeroevaluationmatrixnegativeoutput * S ((S (mdr_i_second_rankzeroevaluationmatrixnegative)) * mdr_vc_second_rankzeroevaluation) + (mdr_a_second_rankzeroevaluationmatrixnegative)))))))) /\ (exists mdr_b_second_rankzeroevaluationdeterminant mdr_c_second_rankzeroevaluationdeterminant mdr_l_second_rankzeroevaluationdeterminant mdr_i_second_rankzeroevaluationdeterminant. ((forall mdr_i_second_rankzeroevaluationdeterminanth. (exists mdr_gap_second_rankzeroevaluationdeterminanthi. mdr_gap_second_rankzeroevaluationdeterminanthi + S (mdr_i_second_rankzeroevaluationdeterminanth) = (mdr_l_second_rankzeroevaluationdeterminant)) -> exists mdr_d_second_rankzeroevaluationdeterminanth mdr_pb_second_rankzeroevaluationdeterminanth mdr_pc_second_rankzeroevaluationdeterminanth mdr_nb_second_rankzeroevaluationdeterminanth mdr_nc_second_rankzeroevaluationdeterminanth mdr_p_second_rankzeroevaluationdeterminanth mdr_n_second_rankzeroevaluationdeterminanth. ((exists mdr_z_second_rankzeroevaluationdeterminanthr. ((exists mdr_a_second_rankzeroevaluationdeterminanthrc mdr_b_second_rankzeroevaluationdeterminanthrc mdr_c_second_rankzeroevaluationdeterminanthrc mdr_e_second_rankzeroevaluationdeterminanthrc mdr_f_second_rankzeroevaluationdeterminanthrc. ((mdr_a_second_rankzeroevaluationdeterminanthrc = ((mdr_d_second_rankzeroevaluationdeterminanth) + (mdr_pb_second_rankzeroevaluationdeterminanth)) * S ((mdr_d_second_rankzeroevaluationdeterminanth) + (mdr_pb_second_rankzeroevaluationdeterminanth)) + ((mdr_pb_second_rankzeroevaluationdeterminanth) + (mdr_pb_second_rankzeroevaluationdeterminanth))) /\ ((mdr_b_second_rankzeroevaluationdeterminanthrc = ((mdr_pc_second_rankzeroevaluationdeterminanth) + (mdr_nb_second_rankzeroevaluationdeterminanth)) * S ((mdr_pc_second_rankzeroevaluationdeterminanth) + (mdr_nb_second_rankzeroevaluationdeterminanth)) + ((mdr_nb_second_rankzeroevaluationdeterminanth) + (mdr_nb_second_rankzeroevaluationdeterminanth))) /\ ((mdr_c_second_rankzeroevaluationdeterminanthrc = ((mdr_a_second_rankzeroevaluationdeterminanthrc) + (mdr_b_second_rankzeroevaluationdeterminanthrc)) * S ((mdr_a_second_rankzeroevaluationdeterminanthrc) + (mdr_b_second_rankzeroevaluationdeterminanthrc)) + ((mdr_b_second_rankzeroevaluationdeterminanthrc) + (mdr_b_second_rankzeroevaluationdeterminanthrc))) /\ ((mdr_e_second_rankzeroevaluationdeterminanthrc = ((mdr_p_second_rankzeroevaluationdeterminanth) + (mdr_n_second_rankzeroevaluationdeterminanth)) * S ((mdr_p_second_rankzeroevaluationdeterminanth) + (mdr_n_second_rankzeroevaluationdeterminanth)) + ((mdr_n_second_rankzeroevaluationdeterminanth) + (mdr_n_second_rankzeroevaluationdeterminanth))) /\ ((mdr_f_second_rankzeroevaluationdeterminanthrc = ((mdr_nc_second_rankzeroevaluationdeterminanth) + (mdr_e_second_rankzeroevaluationdeterminanthrc)) * S ((mdr_nc_second_rankzeroevaluationdeterminanth) + (mdr_e_second_rankzeroevaluationdeterminanthrc)) + ((mdr_e_second_rankzeroevaluationdeterminanthrc) + (mdr_e_second_rankzeroevaluationdeterminanthrc))) /\ ((mdr_z_second_rankzeroevaluationdeterminanthr) = ((mdr_c_second_rankzeroevaluationdeterminanthrc) + (mdr_f_second_rankzeroevaluationdeterminanthrc)) * S ((mdr_c_second_rankzeroevaluationdeterminanthrc) + (mdr_f_second_rankzeroevaluationdeterminanthrc)) + ((mdr_f_second_rankzeroevaluationdeterminanthrc) + (mdr_f_second_rankzeroevaluationdeterminanthrc))))))))) /\ (((exists ff_h_mdr_second_rankzeroevaluationdeterminanthrb. ff_h_mdr_second_rankzeroevaluationdeterminanthrb + S (mdr_z_second_rankzeroevaluationdeterminanthr) = S ((S (mdr_i_second_rankzeroevaluationdeterminanth)) * mdr_c_second_rankzeroevaluationdeterminant)) /\ exists ff_q_mdr_second_rankzeroevaluationdeterminanthrb. mdr_b_second_rankzeroevaluationdeterminant = ff_q_mdr_second_rankzeroevaluationdeterminanthrb * S ((S (mdr_i_second_rankzeroevaluationdeterminanth)) * mdr_c_second_rankzeroevaluationdeterminant) + (mdr_z_second_rankzeroevaluationdeterminanthr))))) /\ (((((mdr_d_second_rankzeroevaluationdeterminanth) = 0) /\ (((mdr_p_second_rankzeroevaluationdeterminanth) = 1) /\ ((mdr_n_second_rankzeroevaluationdeterminanth) = 0))) \/ exists mdr_q_second_rankzeroevaluationdeterminanths mdr_eb_second_rankzeroevaluationdeterminanths mdr_ec_second_rankzeroevaluationdeterminanths mdr_fb_second_rankzeroevaluationdeterminanths mdr_fc_second_rankzeroevaluationdeterminanths. (((mdr_d_second_rankzeroevaluationdeterminanth) = S (mdr_q_second_rankzeroevaluationdeterminanths)) /\ ((forall mdr_j_second_rankzeroevaluationdeterminanthsc. (exists mdr_gap_second_rankzeroevaluationdeterminanthscj. mdr_gap_second_rankzeroevaluationdeterminanthscj + S (mdr_j_second_rankzeroevaluationdeterminanthsc) = (S (mdr_q_second_rankzeroevaluationdeterminanths))) -> exists mdr_i_second_rankzeroevaluationdeterminanthsc mdr_up_second_rankzeroevaluationdeterminanthsc mdr_us_second_rankzeroevaluationdeterminanthsc mdr_un_second_rankzeroevaluationdeterminanthsc mdr_ut_second_rankzeroevaluationdeterminanthsc mdr_p_second_rankzeroevaluationdeterminanthsc mdr_n_second_rankzeroevaluationdeterminanthsc. ((exists mdr_gap_second_rankzeroevaluationdeterminanthsci. mdr_gap_second_rankzeroevaluationdeterminanthsci + S (mdr_i_second_rankzeroevaluationdeterminanthsc) = (mdr_i_second_rankzeroevaluationdeterminanth)) /\ ((exists mdr_z_second_rankzeroevaluationdeterminanthscr. ((exists mdr_a_second_rankzeroevaluationdeterminanthscrc mdr_b_second_rankzeroevaluationdeterminanthscrc mdr_c_second_rankzeroevaluationdeterminanthscrc mdr_e_second_rankzeroevaluationdeterminanthscrc mdr_f_second_rankzeroevaluationdeterminanthscrc. ((mdr_a_second_rankzeroevaluationdeterminanthscrc = ((mdr_q_second_rankzeroevaluationdeterminanths) + (mdr_up_second_rankzeroevaluationdeterminanthsc)) * S ((mdr_q_second_rankzeroevaluationdeterminanths) + (mdr_up_second_rankzeroevaluationdeterminanthsc)) + ((mdr_up_second_rankzeroevaluationdeterminanthsc) + (mdr_up_second_rankzeroevaluationdeterminanthsc))) /\ ((mdr_b_second_rankzeroevaluationdeterminanthscrc = ((mdr_us_second_rankzeroevaluationdeterminanthsc) + (mdr_un_second_rankzeroevaluationdeterminanthsc)) * S ((mdr_us_second_rankzeroevaluationdeterminanthsc) + (mdr_un_second_rankzeroevaluationdeterminanthsc)) + ((mdr_un_second_rankzeroevaluationdeterminanthsc) + (mdr_un_second_rankzeroevaluationdeterminanthsc))) /\ ((mdr_c_second_rankzeroevaluationdeterminanthscrc = ((mdr_a_second_rankzeroevaluationdeterminanthscrc) + (mdr_b_second_rankzeroevaluationdeterminanthscrc)) * S ((mdr_a_second_rankzeroevaluationdeterminanthscrc) + (mdr_b_second_rankzeroevaluationdeterminanthscrc)) + ((mdr_b_second_rankzeroevaluationdeterminanthscrc) + (mdr_b_second_rankzeroevaluationdeterminanthscrc))) /\ ((mdr_e_second_rankzeroevaluationdeterminanthscrc = ((mdr_p_second_rankzeroevaluationdeterminanthsc) + (mdr_n_second_rankzeroevaluationdeterminanthsc)) * S ((mdr_p_second_rankzeroevaluationdeterminanthsc) + (mdr_n_second_rankzeroevaluationdeterminanthsc)) + ((mdr_n_second_rankzeroevaluationdeterminanthsc) + (mdr_n_second_rankzeroevaluationdeterminanthsc))) /\ ((mdr_f_second_rankzeroevaluationdeterminanthscrc = ((mdr_ut_second_rankzeroevaluationdeterminanthsc) + (mdr_e_second_rankzeroevaluationdeterminanthscrc)) * S ((mdr_ut_second_rankzeroevaluationdeterminanthsc) + (mdr_e_second_rankzeroevaluationdeterminanthscrc)) + ((mdr_e_second_rankzeroevaluationdeterminanthscrc) + (mdr_e_second_rankzeroevaluationdeterminanthscrc))) /\ ((mdr_z_second_rankzeroevaluationdeterminanthscr) = ((mdr_c_second_rankzeroevaluationdeterminanthscrc) + (mdr_f_second_rankzeroevaluationdeterminanthscrc)) * S ((mdr_c_second_rankzeroevaluationdeterminanthscrc) + (mdr_f_second_rankzeroevaluationdeterminanthscrc)) + ((mdr_f_second_rankzeroevaluationdeterminanthscrc) + (mdr_f_second_rankzeroevaluationdeterminanthscrc))))))))) /\ (((exists ff_h_mdr_second_rankzeroevaluationdeterminanthscrb. ff_h_mdr_second_rankzeroevaluationdeterminanthscrb + S (mdr_z_second_rankzeroevaluationdeterminanthscr) = S ((S (mdr_i_second_rankzeroevaluationdeterminanthsc)) * mdr_c_second_rankzeroevaluationdeterminant)) /\ exists ff_q_mdr_second_rankzeroevaluationdeterminanthscrb. mdr_b_second_rankzeroevaluationdeterminant = ff_q_mdr_second_rankzeroevaluationdeterminanthscrb * S ((S (mdr_i_second_rankzeroevaluationdeterminanthsc)) * mdr_c_second_rankzeroevaluationdeterminant) + (mdr_z_second_rankzeroevaluationdeterminanthscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_second_rankzeroevaluationdeterminanthscm_positive. (exists ff_gap_mdm_lt_mdr_second_rankzeroevaluationdeterminanthscm_positive_index_bound. ff_gap_mdm_lt_mdr_second_rankzeroevaluationdeterminanthscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_second_rankzeroevaluationdeterminanthscm_positive) = ((mdr_q_second_rankzeroevaluationdeterminanths) * (mdr_q_second_rankzeroevaluationdeterminanths))) -> exists ff_row_mdm_prefix_mdr_second_rankzeroevaluationdeterminanthscm_positive ff_column_mdm_prefix_mdr_second_rankzeroevaluationdeterminanthscm_positive ff_value_mdm_prefix_mdr_second_rankzeroevaluationdeterminanthscm_positive. (ff_index_mdm_prefix_mdr_second_rankzeroevaluationdeterminanthscm_positive = (mdr_q_second_rankzeroevaluationdeterminanths) * ff_row_mdm_prefix_mdr_second_rankzeroevaluationdeterminanthscm_positive + ff_column_mdm_prefix_mdr_second_rankzeroevaluationdeterminanthscm_positive /\ ((exists ff_gap_mdm_lt_mdr_second_rankzeroevaluationdeterminanthscm_positive_column_bound. ff_gap_mdm_lt_mdr_second_rankzeroevaluationdeterminanthscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_second_rankzeroevaluationdeterminanthscm_positive) = (mdr_q_second_rankzeroevaluationdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_second_rankzeroevaluationdeterminanthscm_positive_cell ff_column_mdm_cell_mdr_second_rankzeroevaluationdeterminanthscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_second_rankzeroevaluationdeterminanthscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_second_rankzeroevaluationdeterminanthscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_second_rankzeroevaluationdeterminanthscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_second_rankzeroevaluationdeterminanthscm_positive_cell = ff_row_mdm_prefix_mdr_second_rankzeroevaluationdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_second_rankzeroevaluationdeterminanthscm_positive_cell_row_after. ff_gap_mdm_le_mdr_second_rankzeroevaluationdeterminanthscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_second_rankzeroevaluationdeterminanthscm_positive)) /\ ff_row_mdm_cell_mdr_second_rankzeroevaluationdeterminanthscm_positive_cell = S ff_row_mdm_prefix_mdr_second_rankzeroevaluationdeterminanthscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_second_rankzeroevaluationdeterminanthscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_second_rankzeroevaluationdeterminanthscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_second_rankzeroevaluationdeterminanthscm_positive) = (mdr_j_second_rankzeroevaluationdeterminanthsc)) /\ ff_column_mdm_cell_mdr_second_rankzeroevaluationdeterminanthscm_positive_cell = ff_column_mdm_prefix_mdr_second_rankzeroevaluationdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_second_rankzeroevaluationdeterminanthscm_positive_cell_column_after. ff_gap_mdm_le_mdr_second_rankzeroevaluationdeterminanthscm_positive_cell_column_after + (mdr_j_second_rankzeroevaluationdeterminanthsc) = (ff_column_mdm_prefix_mdr_second_rankzeroevaluationdeterminanthscm_positive)) /\ ff_column_mdm_cell_mdr_second_rankzeroevaluationdeterminanthscm_positive_cell = S ff_column_mdm_prefix_mdr_second_rankzeroevaluationdeterminanthscm_positive))) /\ (((exists ff_h_mdm_mdr_second_rankzeroevaluationdeterminanthscm_positive_cell_source. ff_h_mdm_mdr_second_rankzeroevaluationdeterminanthscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_second_rankzeroevaluationdeterminanthscm_positive) = S ((S ((ff_row_mdm_cell_mdr_second_rankzeroevaluationdeterminanthscm_positive_cell) * (S (mdr_q_second_rankzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_second_rankzeroevaluationdeterminanthscm_positive_cell))) * mdr_pc_second_rankzeroevaluationdeterminanth)) /\ exists ff_q_mdm_mdr_second_rankzeroevaluationdeterminanthscm_positive_cell_source. mdr_pb_second_rankzeroevaluationdeterminanth = ff_q_mdm_mdr_second_rankzeroevaluationdeterminanthscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_second_rankzeroevaluationdeterminanthscm_positive_cell) * (S (mdr_q_second_rankzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_second_rankzeroevaluationdeterminanthscm_positive_cell))) * mdr_pc_second_rankzeroevaluationdeterminanth) + (ff_value_mdm_prefix_mdr_second_rankzeroevaluationdeterminanthscm_positive)))))) /\ (((exists ff_h_mdm_mdr_second_rankzeroevaluationdeterminanthscm_positive_target. ff_h_mdm_mdr_second_rankzeroevaluationdeterminanthscm_positive_target + S (ff_value_mdm_prefix_mdr_second_rankzeroevaluationdeterminanthscm_positive) = S ((S (ff_index_mdm_prefix_mdr_second_rankzeroevaluationdeterminanthscm_positive)) * mdr_us_second_rankzeroevaluationdeterminanthsc)) /\ exists ff_q_mdm_mdr_second_rankzeroevaluationdeterminanthscm_positive_target. mdr_up_second_rankzeroevaluationdeterminanthsc = ff_q_mdm_mdr_second_rankzeroevaluationdeterminanthscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_second_rankzeroevaluationdeterminanthscm_positive)) * mdr_us_second_rankzeroevaluationdeterminanthsc) + (ff_value_mdm_prefix_mdr_second_rankzeroevaluationdeterminanthscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_second_rankzeroevaluationdeterminanthscm_negative. (exists ff_gap_mdm_lt_mdr_second_rankzeroevaluationdeterminanthscm_negative_index_bound. ff_gap_mdm_lt_mdr_second_rankzeroevaluationdeterminanthscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_second_rankzeroevaluationdeterminanthscm_negative) = ((mdr_q_second_rankzeroevaluationdeterminanths) * (mdr_q_second_rankzeroevaluationdeterminanths))) -> exists ff_row_mdm_prefix_mdr_second_rankzeroevaluationdeterminanthscm_negative ff_column_mdm_prefix_mdr_second_rankzeroevaluationdeterminanthscm_negative ff_value_mdm_prefix_mdr_second_rankzeroevaluationdeterminanthscm_negative. (ff_index_mdm_prefix_mdr_second_rankzeroevaluationdeterminanthscm_negative = (mdr_q_second_rankzeroevaluationdeterminanths) * ff_row_mdm_prefix_mdr_second_rankzeroevaluationdeterminanthscm_negative + ff_column_mdm_prefix_mdr_second_rankzeroevaluationdeterminanthscm_negative /\ ((exists ff_gap_mdm_lt_mdr_second_rankzeroevaluationdeterminanthscm_negative_column_bound. ff_gap_mdm_lt_mdr_second_rankzeroevaluationdeterminanthscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_second_rankzeroevaluationdeterminanthscm_negative) = (mdr_q_second_rankzeroevaluationdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_second_rankzeroevaluationdeterminanthscm_negative_cell ff_column_mdm_cell_mdr_second_rankzeroevaluationdeterminanthscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_second_rankzeroevaluationdeterminanthscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_second_rankzeroevaluationdeterminanthscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_second_rankzeroevaluationdeterminanthscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_second_rankzeroevaluationdeterminanthscm_negative_cell = ff_row_mdm_prefix_mdr_second_rankzeroevaluationdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_second_rankzeroevaluationdeterminanthscm_negative_cell_row_after. ff_gap_mdm_le_mdr_second_rankzeroevaluationdeterminanthscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_second_rankzeroevaluationdeterminanthscm_negative)) /\ ff_row_mdm_cell_mdr_second_rankzeroevaluationdeterminanthscm_negative_cell = S ff_row_mdm_prefix_mdr_second_rankzeroevaluationdeterminanthscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_second_rankzeroevaluationdeterminanthscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_second_rankzeroevaluationdeterminanthscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_second_rankzeroevaluationdeterminanthscm_negative) = (mdr_j_second_rankzeroevaluationdeterminanthsc)) /\ ff_column_mdm_cell_mdr_second_rankzeroevaluationdeterminanthscm_negative_cell = ff_column_mdm_prefix_mdr_second_rankzeroevaluationdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_second_rankzeroevaluationdeterminanthscm_negative_cell_column_after. ff_gap_mdm_le_mdr_second_rankzeroevaluationdeterminanthscm_negative_cell_column_after + (mdr_j_second_rankzeroevaluationdeterminanthsc) = (ff_column_mdm_prefix_mdr_second_rankzeroevaluationdeterminanthscm_negative)) /\ ff_column_mdm_cell_mdr_second_rankzeroevaluationdeterminanthscm_negative_cell = S ff_column_mdm_prefix_mdr_second_rankzeroevaluationdeterminanthscm_negative))) /\ (((exists ff_h_mdm_mdr_second_rankzeroevaluationdeterminanthscm_negative_cell_source. ff_h_mdm_mdr_second_rankzeroevaluationdeterminanthscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_second_rankzeroevaluationdeterminanthscm_negative) = S ((S ((ff_row_mdm_cell_mdr_second_rankzeroevaluationdeterminanthscm_negative_cell) * (S (mdr_q_second_rankzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_second_rankzeroevaluationdeterminanthscm_negative_cell))) * mdr_nc_second_rankzeroevaluationdeterminanth)) /\ exists ff_q_mdm_mdr_second_rankzeroevaluationdeterminanthscm_negative_cell_source. mdr_nb_second_rankzeroevaluationdeterminanth = ff_q_mdm_mdr_second_rankzeroevaluationdeterminanthscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_second_rankzeroevaluationdeterminanthscm_negative_cell) * (S (mdr_q_second_rankzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_second_rankzeroevaluationdeterminanthscm_negative_cell))) * mdr_nc_second_rankzeroevaluationdeterminanth) + (ff_value_mdm_prefix_mdr_second_rankzeroevaluationdeterminanthscm_negative)))))) /\ (((exists ff_h_mdm_mdr_second_rankzeroevaluationdeterminanthscm_negative_target. ff_h_mdm_mdr_second_rankzeroevaluationdeterminanthscm_negative_target + S (ff_value_mdm_prefix_mdr_second_rankzeroevaluationdeterminanthscm_negative) = S ((S (ff_index_mdm_prefix_mdr_second_rankzeroevaluationdeterminanthscm_negative)) * mdr_ut_second_rankzeroevaluationdeterminanthsc)) /\ exists ff_q_mdm_mdr_second_rankzeroevaluationdeterminanthscm_negative_target. mdr_un_second_rankzeroevaluationdeterminanthsc = ff_q_mdm_mdr_second_rankzeroevaluationdeterminanthscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_second_rankzeroevaluationdeterminanthscm_negative)) * mdr_ut_second_rankzeroevaluationdeterminanthsc) + (ff_value_mdm_prefix_mdr_second_rankzeroevaluationdeterminanthscm_negative))))))))) /\ ((((exists ff_h_mdr_second_rankzeroevaluationdeterminanthscp. ff_h_mdr_second_rankzeroevaluationdeterminanthscp + S (mdr_p_second_rankzeroevaluationdeterminanthsc) = S ((S (mdr_j_second_rankzeroevaluationdeterminanthsc)) * mdr_ec_second_rankzeroevaluationdeterminanths)) /\ exists ff_q_mdr_second_rankzeroevaluationdeterminanthscp. mdr_eb_second_rankzeroevaluationdeterminanths = ff_q_mdr_second_rankzeroevaluationdeterminanthscp * S ((S (mdr_j_second_rankzeroevaluationdeterminanthsc)) * mdr_ec_second_rankzeroevaluationdeterminanths) + (mdr_p_second_rankzeroevaluationdeterminanthsc))) /\ (((exists ff_h_mdr_second_rankzeroevaluationdeterminanthscn. ff_h_mdr_second_rankzeroevaluationdeterminanthscn + S (mdr_n_second_rankzeroevaluationdeterminanthsc) = S ((S (mdr_j_second_rankzeroevaluationdeterminanthsc)) * mdr_fc_second_rankzeroevaluationdeterminanths)) /\ exists ff_q_mdr_second_rankzeroevaluationdeterminanthscn. mdr_fb_second_rankzeroevaluationdeterminanths = ff_q_mdr_second_rankzeroevaluationdeterminanthscn * S ((S (mdr_j_second_rankzeroevaluationdeterminanthsc)) * mdr_fc_second_rankzeroevaluationdeterminanths) + (mdr_n_second_rankzeroevaluationdeterminanthsc)))))))) /\ (exists ff_ub_mce_fold_mdr_second_rankzeroevaluationdeterminanthsf ff_uc_mce_fold_mdr_second_rankzeroevaluationdeterminanthsf ff_vb_mce_fold_mdr_second_rankzeroevaluationdeterminanthsf ff_vc_mce_fold_mdr_second_rankzeroevaluationdeterminanthsf. ((forall ff_index_mce_alternating_mdr_second_rankzeroevaluationdeterminanthsf_prefix. (exists ff_gap_mce_mdr_second_rankzeroevaluationdeterminanthsf_prefix_index. ff_gap_mce_mdr_second_rankzeroevaluationdeterminanthsf_prefix_index + S (ff_index_mce_alternating_mdr_second_rankzeroevaluationdeterminanthsf_prefix) = (S (mdr_q_second_rankzeroevaluationdeterminanths))) -> exists ff_ap_mce_alternating_mdr_second_rankzeroevaluationdeterminanthsf_prefix ff_an_mce_alternating_mdr_second_rankzeroevaluationdeterminanthsf_prefix ff_bp_mce_alternating_mdr_second_rankzeroevaluationdeterminanthsf_prefix ff_bn_mce_alternating_mdr_second_rankzeroevaluationdeterminanthsf_prefix ff_p_mce_alternating_mdr_second_rankzeroevaluationdeterminanthsf_prefix ff_n_mce_alternating_mdr_second_rankzeroevaluationdeterminanthsf_prefix. ((((exists ff_h_mce_mdr_second_rankzeroevaluationdeterminanthsf_prefix_ap. ff_h_mce_mdr_second_rankzeroevaluationdeterminanthsf_prefix_ap + S (ff_ap_mce_alternating_mdr_second_rankzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_second_rankzeroevaluationdeterminanthsf_prefix)) * mdr_pc_second_rankzeroevaluationdeterminanth)) /\ exists ff_q_mce_mdr_second_rankzeroevaluationdeterminanthsf_prefix_ap. mdr_pb_second_rankzeroevaluationdeterminanth = ff_q_mce_mdr_second_rankzeroevaluationdeterminanthsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_second_rankzeroevaluationdeterminanthsf_prefix)) * mdr_pc_second_rankzeroevaluationdeterminanth) + (ff_ap_mce_alternating_mdr_second_rankzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_second_rankzeroevaluationdeterminanthsf_prefix_an. ff_h_mce_mdr_second_rankzeroevaluationdeterminanthsf_prefix_an + S (ff_an_mce_alternating_mdr_second_rankzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_second_rankzeroevaluationdeterminanthsf_prefix)) * mdr_nc_second_rankzeroevaluationdeterminanth)) /\ exists ff_q_mce_mdr_second_rankzeroevaluationdeterminanthsf_prefix_an. mdr_nb_second_rankzeroevaluationdeterminanth = ff_q_mce_mdr_second_rankzeroevaluationdeterminanthsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_second_rankzeroevaluationdeterminanthsf_prefix)) * mdr_nc_second_rankzeroevaluationdeterminanth) + (ff_an_mce_alternating_mdr_second_rankzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_second_rankzeroevaluationdeterminanthsf_prefix_bp. ff_h_mce_mdr_second_rankzeroevaluationdeterminanthsf_prefix_bp + S (ff_bp_mce_alternating_mdr_second_rankzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_second_rankzeroevaluationdeterminanthsf_prefix)) * mdr_ec_second_rankzeroevaluationdeterminanths)) /\ exists ff_q_mce_mdr_second_rankzeroevaluationdeterminanthsf_prefix_bp. mdr_eb_second_rankzeroevaluationdeterminanths = ff_q_mce_mdr_second_rankzeroevaluationdeterminanthsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_second_rankzeroevaluationdeterminanthsf_prefix)) * mdr_ec_second_rankzeroevaluationdeterminanths) + (ff_bp_mce_alternating_mdr_second_rankzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_second_rankzeroevaluationdeterminanthsf_prefix_bn. ff_h_mce_mdr_second_rankzeroevaluationdeterminanthsf_prefix_bn + S (ff_bn_mce_alternating_mdr_second_rankzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_second_rankzeroevaluationdeterminanthsf_prefix)) * mdr_fc_second_rankzeroevaluationdeterminanths)) /\ exists ff_q_mce_mdr_second_rankzeroevaluationdeterminanthsf_prefix_bn. mdr_fb_second_rankzeroevaluationdeterminanths = ff_q_mce_mdr_second_rankzeroevaluationdeterminanthsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_second_rankzeroevaluationdeterminanthsf_prefix)) * mdr_fc_second_rankzeroevaluationdeterminanths) + (ff_bn_mce_alternating_mdr_second_rankzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_second_rankzeroevaluationdeterminanthsf_prefix_positive. ff_h_mce_mdr_second_rankzeroevaluationdeterminanthsf_prefix_positive + S (ff_p_mce_alternating_mdr_second_rankzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_second_rankzeroevaluationdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_second_rankzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_second_rankzeroevaluationdeterminanthsf_prefix_positive. ff_ub_mce_fold_mdr_second_rankzeroevaluationdeterminanthsf = ff_q_mce_mdr_second_rankzeroevaluationdeterminanthsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_second_rankzeroevaluationdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_second_rankzeroevaluationdeterminanthsf) + (ff_p_mce_alternating_mdr_second_rankzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_second_rankzeroevaluationdeterminanthsf_prefix_negative. ff_h_mce_mdr_second_rankzeroevaluationdeterminanthsf_prefix_negative + S (ff_n_mce_alternating_mdr_second_rankzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_second_rankzeroevaluationdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_second_rankzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_second_rankzeroevaluationdeterminanthsf_prefix_negative. ff_vb_mce_fold_mdr_second_rankzeroevaluationdeterminanthsf = ff_q_mce_mdr_second_rankzeroevaluationdeterminanthsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_second_rankzeroevaluationdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_second_rankzeroevaluationdeterminanthsf) + (ff_n_mce_alternating_mdr_second_rankzeroevaluationdeterminanthsf_prefix))) /\ (((exists ff_even_mce_term_mdr_second_rankzeroevaluationdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_second_rankzeroevaluationdeterminanthsf_prefix = 2 * ff_even_mce_term_mdr_second_rankzeroevaluationdeterminanthsf_prefix_term) /\ (ff_p_mce_alternating_mdr_second_rankzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_second_rankzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_second_rankzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_second_rankzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_second_rankzeroevaluationdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_second_rankzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_second_rankzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_second_rankzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_second_rankzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_second_rankzeroevaluationdeterminanthsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_second_rankzeroevaluationdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_second_rankzeroevaluationdeterminanthsf_prefix = 2 * ff_odd_mce_term_mdr_second_rankzeroevaluationdeterminanthsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_second_rankzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_second_rankzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_second_rankzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_second_rankzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_second_rankzeroevaluationdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_second_rankzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_second_rankzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_second_rankzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_second_rankzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_second_rankzeroevaluationdeterminanthsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_second_rankzeroevaluationdeterminanthsf_positive ff_v_mce_mdr_second_rankzeroevaluationdeterminanthsf_positive. ((((exists ff_h_mce_mdr_second_rankzeroevaluationdeterminanthsf_positive_start. ff_h_mce_mdr_second_rankzeroevaluationdeterminanthsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_second_rankzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_second_rankzeroevaluationdeterminanthsf_positive_start. ff_u_mce_mdr_second_rankzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_second_rankzeroevaluationdeterminanthsf_positive_start * S ((S (0)) * ff_v_mce_mdr_second_rankzeroevaluationdeterminanthsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_second_rankzeroevaluationdeterminanthsf_positive_terminal. ff_h_mce_mdr_second_rankzeroevaluationdeterminanthsf_positive_terminal + S (mdr_p_second_rankzeroevaluationdeterminanth) = S ((S ((S (mdr_q_second_rankzeroevaluationdeterminanths)))) * ff_v_mce_mdr_second_rankzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_second_rankzeroevaluationdeterminanthsf_positive_terminal. ff_u_mce_mdr_second_rankzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_second_rankzeroevaluationdeterminanthsf_positive_terminal * S ((S ((S (mdr_q_second_rankzeroevaluationdeterminanths)))) * ff_v_mce_mdr_second_rankzeroevaluationdeterminanthsf_positive) + (mdr_p_second_rankzeroevaluationdeterminanth))) /\ forall ff_i_mce_mdr_second_rankzeroevaluationdeterminanthsf_positive. (exists ff_lt_mce_mdr_second_rankzeroevaluationdeterminanthsf_positive_bound. ff_lt_mce_mdr_second_rankzeroevaluationdeterminanthsf_positive_bound + S ff_i_mce_mdr_second_rankzeroevaluationdeterminanthsf_positive = (S (mdr_q_second_rankzeroevaluationdeterminanths))) -> exists ff_a_mce_mdr_second_rankzeroevaluationdeterminanthsf_positive ff_r_mce_mdr_second_rankzeroevaluationdeterminanthsf_positive ff_s_mce_mdr_second_rankzeroevaluationdeterminanthsf_positive. ((((exists ff_h_mce_mdr_second_rankzeroevaluationdeterminanthsf_positive_summand. ff_h_mce_mdr_second_rankzeroevaluationdeterminanthsf_positive_summand + S (ff_a_mce_mdr_second_rankzeroevaluationdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_second_rankzeroevaluationdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_second_rankzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_second_rankzeroevaluationdeterminanthsf_positive_summand. ff_ub_mce_fold_mdr_second_rankzeroevaluationdeterminanthsf = ff_q_mce_mdr_second_rankzeroevaluationdeterminanthsf_positive_summand * S ((S (ff_i_mce_mdr_second_rankzeroevaluationdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_second_rankzeroevaluationdeterminanthsf) + (ff_a_mce_mdr_second_rankzeroevaluationdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_second_rankzeroevaluationdeterminanthsf_positive_partial. ff_h_mce_mdr_second_rankzeroevaluationdeterminanthsf_positive_partial + S (ff_r_mce_mdr_second_rankzeroevaluationdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_second_rankzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_second_rankzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_second_rankzeroevaluationdeterminanthsf_positive_partial. ff_u_mce_mdr_second_rankzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_second_rankzeroevaluationdeterminanthsf_positive_partial * S ((S (ff_i_mce_mdr_second_rankzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_second_rankzeroevaluationdeterminanthsf_positive) + (ff_r_mce_mdr_second_rankzeroevaluationdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_second_rankzeroevaluationdeterminanthsf_positive_successor. ff_h_mce_mdr_second_rankzeroevaluationdeterminanthsf_positive_successor + S (ff_s_mce_mdr_second_rankzeroevaluationdeterminanthsf_positive) = S ((S (S ff_i_mce_mdr_second_rankzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_second_rankzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_second_rankzeroevaluationdeterminanthsf_positive_successor. ff_u_mce_mdr_second_rankzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_second_rankzeroevaluationdeterminanthsf_positive_successor * S ((S (S ff_i_mce_mdr_second_rankzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_second_rankzeroevaluationdeterminanthsf_positive) + (ff_s_mce_mdr_second_rankzeroevaluationdeterminanthsf_positive))) /\ ff_s_mce_mdr_second_rankzeroevaluationdeterminanthsf_positive = ff_r_mce_mdr_second_rankzeroevaluationdeterminanthsf_positive + ff_a_mce_mdr_second_rankzeroevaluationdeterminanthsf_positive)))))) /\ (exists ff_u_mce_mdr_second_rankzeroevaluationdeterminanthsf_negative ff_v_mce_mdr_second_rankzeroevaluationdeterminanthsf_negative. ((((exists ff_h_mce_mdr_second_rankzeroevaluationdeterminanthsf_negative_start. ff_h_mce_mdr_second_rankzeroevaluationdeterminanthsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_second_rankzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_second_rankzeroevaluationdeterminanthsf_negative_start. ff_u_mce_mdr_second_rankzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_second_rankzeroevaluationdeterminanthsf_negative_start * S ((S (0)) * ff_v_mce_mdr_second_rankzeroevaluationdeterminanthsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_second_rankzeroevaluationdeterminanthsf_negative_terminal. ff_h_mce_mdr_second_rankzeroevaluationdeterminanthsf_negative_terminal + S (mdr_n_second_rankzeroevaluationdeterminanth) = S ((S ((S (mdr_q_second_rankzeroevaluationdeterminanths)))) * ff_v_mce_mdr_second_rankzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_second_rankzeroevaluationdeterminanthsf_negative_terminal. ff_u_mce_mdr_second_rankzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_second_rankzeroevaluationdeterminanthsf_negative_terminal * S ((S ((S (mdr_q_second_rankzeroevaluationdeterminanths)))) * ff_v_mce_mdr_second_rankzeroevaluationdeterminanthsf_negative) + (mdr_n_second_rankzeroevaluationdeterminanth))) /\ forall ff_i_mce_mdr_second_rankzeroevaluationdeterminanthsf_negative. (exists ff_lt_mce_mdr_second_rankzeroevaluationdeterminanthsf_negative_bound. ff_lt_mce_mdr_second_rankzeroevaluationdeterminanthsf_negative_bound + S ff_i_mce_mdr_second_rankzeroevaluationdeterminanthsf_negative = (S (mdr_q_second_rankzeroevaluationdeterminanths))) -> exists ff_a_mce_mdr_second_rankzeroevaluationdeterminanthsf_negative ff_r_mce_mdr_second_rankzeroevaluationdeterminanthsf_negative ff_s_mce_mdr_second_rankzeroevaluationdeterminanthsf_negative. ((((exists ff_h_mce_mdr_second_rankzeroevaluationdeterminanthsf_negative_summand. ff_h_mce_mdr_second_rankzeroevaluationdeterminanthsf_negative_summand + S (ff_a_mce_mdr_second_rankzeroevaluationdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_second_rankzeroevaluationdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_second_rankzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_second_rankzeroevaluationdeterminanthsf_negative_summand. ff_vb_mce_fold_mdr_second_rankzeroevaluationdeterminanthsf = ff_q_mce_mdr_second_rankzeroevaluationdeterminanthsf_negative_summand * S ((S (ff_i_mce_mdr_second_rankzeroevaluationdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_second_rankzeroevaluationdeterminanthsf) + (ff_a_mce_mdr_second_rankzeroevaluationdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_second_rankzeroevaluationdeterminanthsf_negative_partial. ff_h_mce_mdr_second_rankzeroevaluationdeterminanthsf_negative_partial + S (ff_r_mce_mdr_second_rankzeroevaluationdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_second_rankzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_second_rankzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_second_rankzeroevaluationdeterminanthsf_negative_partial. ff_u_mce_mdr_second_rankzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_second_rankzeroevaluationdeterminanthsf_negative_partial * S ((S (ff_i_mce_mdr_second_rankzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_second_rankzeroevaluationdeterminanthsf_negative) + (ff_r_mce_mdr_second_rankzeroevaluationdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_second_rankzeroevaluationdeterminanthsf_negative_successor. ff_h_mce_mdr_second_rankzeroevaluationdeterminanthsf_negative_successor + S (ff_s_mce_mdr_second_rankzeroevaluationdeterminanthsf_negative) = S ((S (S ff_i_mce_mdr_second_rankzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_second_rankzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_second_rankzeroevaluationdeterminanthsf_negative_successor. ff_u_mce_mdr_second_rankzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_second_rankzeroevaluationdeterminanthsf_negative_successor * S ((S (S ff_i_mce_mdr_second_rankzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_second_rankzeroevaluationdeterminanthsf_negative) + (ff_s_mce_mdr_second_rankzeroevaluationdeterminanthsf_negative))) /\ ff_s_mce_mdr_second_rankzeroevaluationdeterminanthsf_negative = ff_r_mce_mdr_second_rankzeroevaluationdeterminanthsf_negative + ff_a_mce_mdr_second_rankzeroevaluationdeterminanthsf_negative))))))))))))))) /\ ((exists mdr_gap_second_rankzeroevaluationdeterminanti. mdr_gap_second_rankzeroevaluationdeterminanti + S (mdr_i_second_rankzeroevaluationdeterminant) = (mdr_l_second_rankzeroevaluationdeterminant)) /\ (exists mdr_z_second_rankzeroevaluationdeterminantr. ((exists mdr_a_second_rankzeroevaluationdeterminantrc mdr_b_second_rankzeroevaluationdeterminantrc mdr_c_second_rankzeroevaluationdeterminantrc mdr_e_second_rankzeroevaluationdeterminantrc mdr_f_second_rankzeroevaluationdeterminantrc. ((mdr_a_second_rankzeroevaluationdeterminantrc = ((mdr_q_second_rank) + (mdr_ub_second_rankzeroevaluation)) * S ((mdr_q_second_rank) + (mdr_ub_second_rankzeroevaluation)) + ((mdr_ub_second_rankzeroevaluation) + (mdr_ub_second_rankzeroevaluation))) /\ ((mdr_b_second_rankzeroevaluationdeterminantrc = ((mdr_uc_second_rankzeroevaluation) + (mdr_vb_second_rankzeroevaluation)) * S ((mdr_uc_second_rankzeroevaluation) + (mdr_vb_second_rankzeroevaluation)) + ((mdr_vb_second_rankzeroevaluation) + (mdr_vb_second_rankzeroevaluation))) /\ ((mdr_c_second_rankzeroevaluationdeterminantrc = ((mdr_a_second_rankzeroevaluationdeterminantrc) + (mdr_b_second_rankzeroevaluationdeterminantrc)) * S ((mdr_a_second_rankzeroevaluationdeterminantrc) + (mdr_b_second_rankzeroevaluationdeterminantrc)) + ((mdr_b_second_rankzeroevaluationdeterminantrc) + (mdr_b_second_rankzeroevaluationdeterminantrc))) /\ ((mdr_e_second_rankzeroevaluationdeterminantrc = ((mdr_p_second_rankzero) + (mdr_n_second_rankzero)) * S ((mdr_p_second_rankzero) + (mdr_n_second_rankzero)) + ((mdr_n_second_rankzero) + (mdr_n_second_rankzero))) /\ ((mdr_f_second_rankzeroevaluationdeterminantrc = ((mdr_vc_second_rankzeroevaluation) + (mdr_e_second_rankzeroevaluationdeterminantrc)) * S ((mdr_vc_second_rankzeroevaluation) + (mdr_e_second_rankzeroevaluationdeterminantrc)) + ((mdr_e_second_rankzeroevaluationdeterminantrc) + (mdr_e_second_rankzeroevaluationdeterminantrc))) /\ ((mdr_z_second_rankzeroevaluationdeterminantr) = ((mdr_c_second_rankzeroevaluationdeterminantrc) + (mdr_f_second_rankzeroevaluationdeterminantrc)) * S ((mdr_c_second_rankzeroevaluationdeterminantrc) + (mdr_f_second_rankzeroevaluationdeterminantrc)) + ((mdr_f_second_rankzeroevaluationdeterminantrc) + (mdr_f_second_rankzeroevaluationdeterminantrc))))))))) /\ (((exists ff_h_mdr_second_rankzeroevaluationdeterminantrb. ff_h_mdr_second_rankzeroevaluationdeterminantrb + S (mdr_z_second_rankzeroevaluationdeterminantr) = S ((S (mdr_i_second_rankzeroevaluationdeterminant)) * mdr_c_second_rankzeroevaluationdeterminant)) /\ exists ff_q_mdr_second_rankzeroevaluationdeterminantrb. mdr_b_second_rankzeroevaluationdeterminant = ff_q_mdr_second_rankzeroevaluationdeterminantrb * S ((S (mdr_i_second_rankzeroevaluationdeterminant)) * mdr_c_second_rankzeroevaluationdeterminant) + (mdr_z_second_rankzeroevaluationdeterminantr)))))))))) -> mdr_p_second_rankzero = mdr_n_second_rankzero)))))) -> rank = other