rectangular_matrix_rank_certificate_exists

forall pb pc nb nc r w. exists rank. (((exists mdr_gap_rank_existsrows_bound. mdr_gap_rank_existsrows_bound + (rank) = (r)) /\ ((exists mdr_gap_rank_existscolumns_bound. mdr_gap_rank_existscolumns_bound + (rank) = (w)) /\ ((exists mdr_rb_rank_existswitness mdr_rc_rank_existswitness mdr_cb_rank_existswitness mdr_cc_rank_existswitness. (((((forall fom_index_mrf_rank_existswitnessminorrowsbound. (exists fom_gap_mrf_rank_existswitnessminorrowsbound_index_bound. fom_gap_mrf_rank_existswitnessminorrowsbound_index_bound + S (fom_index_mrf_rank_existswitnessminorrowsbound) = rank) -> exists fom_value_mrf_rank_existswitnessminorrowsbound. ((((exists fom_beta_height_mrf_rank_existswitnessminorrowsbound_entry. fom_beta_height_mrf_rank_existswitnessminorrowsbound_entry + S (fom_value_mrf_rank_existswitnessminorrowsbound) = S ((S (fom_index_mrf_rank_existswitnessminorrowsbound)) * mdr_rc_rank_existswitness)) /\ exists fom_beta_quotient_mrf_rank_existswitnessminorrowsbound_entry. mdr_rb_rank_existswitness = fom_beta_quotient_mrf_rank_existswitnessminorrowsbound_entry * S ((S (fom_index_mrf_rank_existswitnessminorrowsbound)) * mdr_rc_rank_existswitness) + (fom_value_mrf_rank_existswitnessminorrowsbound))) /\ (exists fom_gap_mrf_rank_existswitnessminorrowsbound_value_bound. fom_gap_mrf_rank_existswitnessminorrowsbound_value_bound + S (fom_value_mrf_rank_existswitnessminorrowsbound) = r))) /\ (forall mdr_i_rank_existswitnessminorrowsdistinct mdr_j_rank_existswitnessminorrowsdistinct mdr_a_rank_existswitnessminorrowsdistinct. (exists mdr_gap_rank_existswitnessminorrowsdistincti. mdr_gap_rank_existswitnessminorrowsdistincti + S (mdr_i_rank_existswitnessminorrowsdistinct) = (rank)) -> (exists mdr_gap_rank_existswitnessminorrowsdistinctj. mdr_gap_rank_existswitnessminorrowsdistinctj + S (mdr_j_rank_existswitnessminorrowsdistinct) = (rank)) -> (((exists ff_h_mdr_rank_existswitnessminorrowsdistinctfirst. ff_h_mdr_rank_existswitnessminorrowsdistinctfirst + S (mdr_a_rank_existswitnessminorrowsdistinct) = S ((S (mdr_i_rank_existswitnessminorrowsdistinct)) * mdr_rc_rank_existswitness)) /\ exists ff_q_mdr_rank_existswitnessminorrowsdistinctfirst. mdr_rb_rank_existswitness = ff_q_mdr_rank_existswitnessminorrowsdistinctfirst * S ((S (mdr_i_rank_existswitnessminorrowsdistinct)) * mdr_rc_rank_existswitness) + (mdr_a_rank_existswitnessminorrowsdistinct))) -> (((exists ff_h_mdr_rank_existswitnessminorrowsdistinctsecond. ff_h_mdr_rank_existswitnessminorrowsdistinctsecond + S (mdr_a_rank_existswitnessminorrowsdistinct) = S ((S (mdr_j_rank_existswitnessminorrowsdistinct)) * mdr_rc_rank_existswitness)) /\ exists ff_q_mdr_rank_existswitnessminorrowsdistinctsecond. mdr_rb_rank_existswitness = ff_q_mdr_rank_existswitnessminorrowsdistinctsecond * S ((S (mdr_j_rank_existswitnessminorrowsdistinct)) * mdr_rc_rank_existswitness) + (mdr_a_rank_existswitnessminorrowsdistinct))) -> mdr_i_rank_existswitnessminorrowsdistinct = mdr_j_rank_existswitnessminorrowsdistinct))) /\ ((((forall fom_index_mrf_rank_existswitnessminorcolumnsbound. (exists fom_gap_mrf_rank_existswitnessminorcolumnsbound_index_bound. fom_gap_mrf_rank_existswitnessminorcolumnsbound_index_bound + S (fom_index_mrf_rank_existswitnessminorcolumnsbound) = rank) -> exists fom_value_mrf_rank_existswitnessminorcolumnsbound. ((((exists fom_beta_height_mrf_rank_existswitnessminorcolumnsbound_entry. fom_beta_height_mrf_rank_existswitnessminorcolumnsbound_entry + S (fom_value_mrf_rank_existswitnessminorcolumnsbound) = S ((S (fom_index_mrf_rank_existswitnessminorcolumnsbound)) * mdr_cc_rank_existswitness)) /\ exists fom_beta_quotient_mrf_rank_existswitnessminorcolumnsbound_entry. mdr_cb_rank_existswitness = fom_beta_quotient_mrf_rank_existswitnessminorcolumnsbound_entry * S ((S (fom_index_mrf_rank_existswitnessminorcolumnsbound)) * mdr_cc_rank_existswitness) + (fom_value_mrf_rank_existswitnessminorcolumnsbound))) /\ (exists fom_gap_mrf_rank_existswitnessminorcolumnsbound_value_bound. fom_gap_mrf_rank_existswitnessminorcolumnsbound_value_bound + S (fom_value_mrf_rank_existswitnessminorcolumnsbound) = w))) /\ (forall mdr_i_rank_existswitnessminorcolumnsdistinct mdr_j_rank_existswitnessminorcolumnsdistinct mdr_a_rank_existswitnessminorcolumnsdistinct. (exists mdr_gap_rank_existswitnessminorcolumnsdistincti. mdr_gap_rank_existswitnessminorcolumnsdistincti + S (mdr_i_rank_existswitnessminorcolumnsdistinct) = (rank)) -> (exists mdr_gap_rank_existswitnessminorcolumnsdistinctj. mdr_gap_rank_existswitnessminorcolumnsdistinctj + S (mdr_j_rank_existswitnessminorcolumnsdistinct) = (rank)) -> (((exists ff_h_mdr_rank_existswitnessminorcolumnsdistinctfirst. ff_h_mdr_rank_existswitnessminorcolumnsdistinctfirst + S (mdr_a_rank_existswitnessminorcolumnsdistinct) = S ((S (mdr_i_rank_existswitnessminorcolumnsdistinct)) * mdr_cc_rank_existswitness)) /\ exists ff_q_mdr_rank_existswitnessminorcolumnsdistinctfirst. mdr_cb_rank_existswitness = ff_q_mdr_rank_existswitnessminorcolumnsdistinctfirst * S ((S (mdr_i_rank_existswitnessminorcolumnsdistinct)) * mdr_cc_rank_existswitness) + (mdr_a_rank_existswitnessminorcolumnsdistinct))) -> (((exists ff_h_mdr_rank_existswitnessminorcolumnsdistinctsecond. ff_h_mdr_rank_existswitnessminorcolumnsdistinctsecond + S (mdr_a_rank_existswitnessminorcolumnsdistinct) = S ((S (mdr_j_rank_existswitnessminorcolumnsdistinct)) * mdr_cc_rank_existswitness)) /\ exists ff_q_mdr_rank_existswitnessminorcolumnsdistinctsecond. mdr_cb_rank_existswitness = ff_q_mdr_rank_existswitnessminorcolumnsdistinctsecond * S ((S (mdr_j_rank_existswitnessminorcolumnsdistinct)) * mdr_cc_rank_existswitness) + (mdr_a_rank_existswitnessminorcolumnsdistinct))) -> mdr_i_rank_existswitnessminorcolumnsdistinct = mdr_j_rank_existswitnessminorcolumnsdistinct))) /\ (exists mdr_p_rank_existswitnessminornonzero mdr_n_rank_existswitnessminornonzero. ((exists mdr_ub_rank_existswitnessminornonzeroevaluation mdr_uc_rank_existswitnessminornonzeroevaluation mdr_vb_rank_existswitnessminornonzeroevaluation mdr_vc_rank_existswitnessminornonzeroevaluation. ((((forall mdr_i_rank_existswitnessminornonzeroevaluationmatrixpositive. (exists mdr_gap_rank_existswitnessminornonzeroevaluationmatrixpositivebound. mdr_gap_rank_existswitnessminornonzeroevaluationmatrixpositivebound + S (mdr_i_rank_existswitnessminornonzeroevaluationmatrixpositive) = ((rank) * (rank))) -> exists mdr_a_rank_existswitnessminornonzeroevaluationmatrixpositive. (((exists mdr_r_rank_existswitnessminornonzeroevaluationmatrixpositivepoint mdr_s_rank_existswitnessminornonzeroevaluationmatrixpositivepoint mdr_u_rank_existswitnessminornonzeroevaluationmatrixpositivepoint mdr_v_rank_existswitnessminornonzeroevaluationmatrixpositivepoint. ((mdr_i_rank_existswitnessminornonzeroevaluationmatrixpositive = (rank) * mdr_r_rank_existswitnessminornonzeroevaluationmatrixpositivepoint + mdr_s_rank_existswitnessminornonzeroevaluationmatrixpositivepoint) /\ ((exists mdr_gap_rank_existswitnessminornonzeroevaluationmatrixpositivepointcolumn. mdr_gap_rank_existswitnessminornonzeroevaluationmatrixpositivepointcolumn + S (mdr_s_rank_existswitnessminornonzeroevaluationmatrixpositivepoint) = (rank)) /\ ((((exists ff_h_mdr_rank_existswitnessminornonzeroevaluationmatrixpositivepointrow_index. ff_h_mdr_rank_existswitnessminornonzeroevaluationmatrixpositivepointrow_index + S (mdr_u_rank_existswitnessminornonzeroevaluationmatrixpositivepoint) = S ((S (mdr_r_rank_existswitnessminornonzeroevaluationmatrixpositivepoint)) * mdr_rc_rank_existswitness)) /\ exists ff_q_mdr_rank_existswitnessminornonzeroevaluationmatrixpositivepointrow_index. mdr_rb_rank_existswitness = ff_q_mdr_rank_existswitnessminornonzeroevaluationmatrixpositivepointrow_index * S ((S (mdr_r_rank_existswitnessminornonzeroevaluationmatrixpositivepoint)) * mdr_rc_rank_existswitness) + (mdr_u_rank_existswitnessminornonzeroevaluationmatrixpositivepoint))) /\ ((((exists ff_h_mdr_rank_existswitnessminornonzeroevaluationmatrixpositivepointcolumn_index. ff_h_mdr_rank_existswitnessminornonzeroevaluationmatrixpositivepointcolumn_index + S (mdr_v_rank_existswitnessminornonzeroevaluationmatrixpositivepoint) = S ((S (mdr_s_rank_existswitnessminornonzeroevaluationmatrixpositivepoint)) * mdr_cc_rank_existswitness)) /\ exists ff_q_mdr_rank_existswitnessminornonzeroevaluationmatrixpositivepointcolumn_index. mdr_cb_rank_existswitness = ff_q_mdr_rank_existswitnessminornonzeroevaluationmatrixpositivepointcolumn_index * S ((S (mdr_s_rank_existswitnessminornonzeroevaluationmatrixpositivepoint)) * mdr_cc_rank_existswitness) + (mdr_v_rank_existswitnessminornonzeroevaluationmatrixpositivepoint))) /\ (((exists ff_h_mdr_rank_existswitnessminornonzeroevaluationmatrixpositivepointsource. ff_h_mdr_rank_existswitnessminornonzeroevaluationmatrixpositivepointsource + S (mdr_a_rank_existswitnessminornonzeroevaluationmatrixpositive) = S ((S ((mdr_u_rank_existswitnessminornonzeroevaluationmatrixpositivepoint) * (w) + (mdr_v_rank_existswitnessminornonzeroevaluationmatrixpositivepoint))) * pc)) /\ exists ff_q_mdr_rank_existswitnessminornonzeroevaluationmatrixpositivepointsource. pb = ff_q_mdr_rank_existswitnessminornonzeroevaluationmatrixpositivepointsource * S ((S ((mdr_u_rank_existswitnessminornonzeroevaluationmatrixpositivepoint) * (w) + (mdr_v_rank_existswitnessminornonzeroevaluationmatrixpositivepoint))) * pc) + (mdr_a_rank_existswitnessminornonzeroevaluationmatrixpositive)))))))) /\ (((exists ff_h_mdr_rank_existswitnessminornonzeroevaluationmatrixpositiveoutput. ff_h_mdr_rank_existswitnessminornonzeroevaluationmatrixpositiveoutput + S (mdr_a_rank_existswitnessminornonzeroevaluationmatrixpositive) = S ((S (mdr_i_rank_existswitnessminornonzeroevaluationmatrixpositive)) * mdr_uc_rank_existswitnessminornonzeroevaluation)) /\ exists ff_q_mdr_rank_existswitnessminornonzeroevaluationmatrixpositiveoutput. mdr_ub_rank_existswitnessminornonzeroevaluation = ff_q_mdr_rank_existswitnessminornonzeroevaluationmatrixpositiveoutput * S ((S (mdr_i_rank_existswitnessminornonzeroevaluationmatrixpositive)) * mdr_uc_rank_existswitnessminornonzeroevaluation) + (mdr_a_rank_existswitnessminornonzeroevaluationmatrixpositive)))))) /\ (forall mdr_i_rank_existswitnessminornonzeroevaluationmatrixnegative. (exists mdr_gap_rank_existswitnessminornonzeroevaluationmatrixnegativebound. mdr_gap_rank_existswitnessminornonzeroevaluationmatrixnegativebound + S (mdr_i_rank_existswitnessminornonzeroevaluationmatrixnegative) = ((rank) * (rank))) -> exists mdr_a_rank_existswitnessminornonzeroevaluationmatrixnegative. (((exists mdr_r_rank_existswitnessminornonzeroevaluationmatrixnegativepoint mdr_s_rank_existswitnessminornonzeroevaluationmatrixnegativepoint mdr_u_rank_existswitnessminornonzeroevaluationmatrixnegativepoint mdr_v_rank_existswitnessminornonzeroevaluationmatrixnegativepoint. ((mdr_i_rank_existswitnessminornonzeroevaluationmatrixnegative = (rank) * mdr_r_rank_existswitnessminornonzeroevaluationmatrixnegativepoint + mdr_s_rank_existswitnessminornonzeroevaluationmatrixnegativepoint) /\ ((exists mdr_gap_rank_existswitnessminornonzeroevaluationmatrixnegativepointcolumn. mdr_gap_rank_existswitnessminornonzeroevaluationmatrixnegativepointcolumn + S (mdr_s_rank_existswitnessminornonzeroevaluationmatrixnegativepoint) = (rank)) /\ ((((exists ff_h_mdr_rank_existswitnessminornonzeroevaluationmatrixnegativepointrow_index. ff_h_mdr_rank_existswitnessminornonzeroevaluationmatrixnegativepointrow_index + S (mdr_u_rank_existswitnessminornonzeroevaluationmatrixnegativepoint) = S ((S (mdr_r_rank_existswitnessminornonzeroevaluationmatrixnegativepoint)) * mdr_rc_rank_existswitness)) /\ exists ff_q_mdr_rank_existswitnessminornonzeroevaluationmatrixnegativepointrow_index. mdr_rb_rank_existswitness = ff_q_mdr_rank_existswitnessminornonzeroevaluationmatrixnegativepointrow_index * S ((S (mdr_r_rank_existswitnessminornonzeroevaluationmatrixnegativepoint)) * mdr_rc_rank_existswitness) + (mdr_u_rank_existswitnessminornonzeroevaluationmatrixnegativepoint))) /\ ((((exists ff_h_mdr_rank_existswitnessminornonzeroevaluationmatrixnegativepointcolumn_index. ff_h_mdr_rank_existswitnessminornonzeroevaluationmatrixnegativepointcolumn_index + S (mdr_v_rank_existswitnessminornonzeroevaluationmatrixnegativepoint) = S ((S (mdr_s_rank_existswitnessminornonzeroevaluationmatrixnegativepoint)) * mdr_cc_rank_existswitness)) /\ exists ff_q_mdr_rank_existswitnessminornonzeroevaluationmatrixnegativepointcolumn_index. mdr_cb_rank_existswitness = ff_q_mdr_rank_existswitnessminornonzeroevaluationmatrixnegativepointcolumn_index * S ((S (mdr_s_rank_existswitnessminornonzeroevaluationmatrixnegativepoint)) * mdr_cc_rank_existswitness) + (mdr_v_rank_existswitnessminornonzeroevaluationmatrixnegativepoint))) /\ (((exists ff_h_mdr_rank_existswitnessminornonzeroevaluationmatrixnegativepointsource. ff_h_mdr_rank_existswitnessminornonzeroevaluationmatrixnegativepointsource + S (mdr_a_rank_existswitnessminornonzeroevaluationmatrixnegative) = S ((S ((mdr_u_rank_existswitnessminornonzeroevaluationmatrixnegativepoint) * (w) + (mdr_v_rank_existswitnessminornonzeroevaluationmatrixnegativepoint))) * nc)) /\ exists ff_q_mdr_rank_existswitnessminornonzeroevaluationmatrixnegativepointsource. nb = ff_q_mdr_rank_existswitnessminornonzeroevaluationmatrixnegativepointsource * S ((S ((mdr_u_rank_existswitnessminornonzeroevaluationmatrixnegativepoint) * (w) + (mdr_v_rank_existswitnessminornonzeroevaluationmatrixnegativepoint))) * nc) + (mdr_a_rank_existswitnessminornonzeroevaluationmatrixnegative)))))))) /\ (((exists ff_h_mdr_rank_existswitnessminornonzeroevaluationmatrixnegativeoutput. ff_h_mdr_rank_existswitnessminornonzeroevaluationmatrixnegativeoutput + S (mdr_a_rank_existswitnessminornonzeroevaluationmatrixnegative) = S ((S (mdr_i_rank_existswitnessminornonzeroevaluationmatrixnegative)) * mdr_vc_rank_existswitnessminornonzeroevaluation)) /\ exists ff_q_mdr_rank_existswitnessminornonzeroevaluationmatrixnegativeoutput. mdr_vb_rank_existswitnessminornonzeroevaluation = ff_q_mdr_rank_existswitnessminornonzeroevaluationmatrixnegativeoutput * S ((S (mdr_i_rank_existswitnessminornonzeroevaluationmatrixnegative)) * mdr_vc_rank_existswitnessminornonzeroevaluation) + (mdr_a_rank_existswitnessminornonzeroevaluationmatrixnegative)))))))) /\ (exists mdr_b_rank_existswitnessminornonzeroevaluationdeterminant mdr_c_rank_existswitnessminornonzeroevaluationdeterminant mdr_l_rank_existswitnessminornonzeroevaluationdeterminant mdr_i_rank_existswitnessminornonzeroevaluationdeterminant. ((forall mdr_i_rank_existswitnessminornonzeroevaluationdeterminanth. (exists mdr_gap_rank_existswitnessminornonzeroevaluationdeterminanthi. mdr_gap_rank_existswitnessminornonzeroevaluationdeterminanthi + S (mdr_i_rank_existswitnessminornonzeroevaluationdeterminanth) = (mdr_l_rank_existswitnessminornonzeroevaluationdeterminant)) -> exists mdr_d_rank_existswitnessminornonzeroevaluationdeterminanth mdr_pb_rank_existswitnessminornonzeroevaluationdeterminanth mdr_pc_rank_existswitnessminornonzeroevaluationdeterminanth mdr_nb_rank_existswitnessminornonzeroevaluationdeterminanth mdr_nc_rank_existswitnessminornonzeroevaluationdeterminanth mdr_p_rank_existswitnessminornonzeroevaluationdeterminanth mdr_n_rank_existswitnessminornonzeroevaluationdeterminanth. ((exists mdr_z_rank_existswitnessminornonzeroevaluationdeterminanthr. ((exists mdr_a_rank_existswitnessminornonzeroevaluationdeterminanthrc mdr_b_rank_existswitnessminornonzeroevaluationdeterminanthrc mdr_c_rank_existswitnessminornonzeroevaluationdeterminanthrc mdr_e_rank_existswitnessminornonzeroevaluationdeterminanthrc mdr_f_rank_existswitnessminornonzeroevaluationdeterminanthrc. ((mdr_a_rank_existswitnessminornonzeroevaluationdeterminanthrc = ((mdr_d_rank_existswitnessminornonzeroevaluationdeterminanth) + (mdr_pb_rank_existswitnessminornonzeroevaluationdeterminanth)) * S ((mdr_d_rank_existswitnessminornonzeroevaluationdeterminanth) + (mdr_pb_rank_existswitnessminornonzeroevaluationdeterminanth)) + ((mdr_pb_rank_existswitnessminornonzeroevaluationdeterminanth) + (mdr_pb_rank_existswitnessminornonzeroevaluationdeterminanth))) /\ ((mdr_b_rank_existswitnessminornonzeroevaluationdeterminanthrc = ((mdr_pc_rank_existswitnessminornonzeroevaluationdeterminanth) + (mdr_nb_rank_existswitnessminornonzeroevaluationdeterminanth)) * S ((mdr_pc_rank_existswitnessminornonzeroevaluationdeterminanth) + (mdr_nb_rank_existswitnessminornonzeroevaluationdeterminanth)) + ((mdr_nb_rank_existswitnessminornonzeroevaluationdeterminanth) + (mdr_nb_rank_existswitnessminornonzeroevaluationdeterminanth))) /\ ((mdr_c_rank_existswitnessminornonzeroevaluationdeterminanthrc = ((mdr_a_rank_existswitnessminornonzeroevaluationdeterminanthrc) + (mdr_b_rank_existswitnessminornonzeroevaluationdeterminanthrc)) * S ((mdr_a_rank_existswitnessminornonzeroevaluationdeterminanthrc) + (mdr_b_rank_existswitnessminornonzeroevaluationdeterminanthrc)) + ((mdr_b_rank_existswitnessminornonzeroevaluationdeterminanthrc) + (mdr_b_rank_existswitnessminornonzeroevaluationdeterminanthrc))) /\ ((mdr_e_rank_existswitnessminornonzeroevaluationdeterminanthrc = ((mdr_p_rank_existswitnessminornonzeroevaluationdeterminanth) + (mdr_n_rank_existswitnessminornonzeroevaluationdeterminanth)) * S ((mdr_p_rank_existswitnessminornonzeroevaluationdeterminanth) + (mdr_n_rank_existswitnessminornonzeroevaluationdeterminanth)) + ((mdr_n_rank_existswitnessminornonzeroevaluationdeterminanth) + (mdr_n_rank_existswitnessminornonzeroevaluationdeterminanth))) /\ ((mdr_f_rank_existswitnessminornonzeroevaluationdeterminanthrc = ((mdr_nc_rank_existswitnessminornonzeroevaluationdeterminanth) + (mdr_e_rank_existswitnessminornonzeroevaluationdeterminanthrc)) * S ((mdr_nc_rank_existswitnessminornonzeroevaluationdeterminanth) + (mdr_e_rank_existswitnessminornonzeroevaluationdeterminanthrc)) + ((mdr_e_rank_existswitnessminornonzeroevaluationdeterminanthrc) + (mdr_e_rank_existswitnessminornonzeroevaluationdeterminanthrc))) /\ ((mdr_z_rank_existswitnessminornonzeroevaluationdeterminanthr) = ((mdr_c_rank_existswitnessminornonzeroevaluationdeterminanthrc) + (mdr_f_rank_existswitnessminornonzeroevaluationdeterminanthrc)) * S ((mdr_c_rank_existswitnessminornonzeroevaluationdeterminanthrc) + (mdr_f_rank_existswitnessminornonzeroevaluationdeterminanthrc)) + ((mdr_f_rank_existswitnessminornonzeroevaluationdeterminanthrc) + (mdr_f_rank_existswitnessminornonzeroevaluationdeterminanthrc))))))))) /\ (((exists ff_h_mdr_rank_existswitnessminornonzeroevaluationdeterminanthrb. ff_h_mdr_rank_existswitnessminornonzeroevaluationdeterminanthrb + S (mdr_z_rank_existswitnessminornonzeroevaluationdeterminanthr) = S ((S (mdr_i_rank_existswitnessminornonzeroevaluationdeterminanth)) * mdr_c_rank_existswitnessminornonzeroevaluationdeterminant)) /\ exists ff_q_mdr_rank_existswitnessminornonzeroevaluationdeterminanthrb. mdr_b_rank_existswitnessminornonzeroevaluationdeterminant = ff_q_mdr_rank_existswitnessminornonzeroevaluationdeterminanthrb * S ((S (mdr_i_rank_existswitnessminornonzeroevaluationdeterminanth)) * mdr_c_rank_existswitnessminornonzeroevaluationdeterminant) + (mdr_z_rank_existswitnessminornonzeroevaluationdeterminanthr))))) /\ (((((mdr_d_rank_existswitnessminornonzeroevaluationdeterminanth) = 0) /\ (((mdr_p_rank_existswitnessminornonzeroevaluationdeterminanth) = 1) /\ ((mdr_n_rank_existswitnessminornonzeroevaluationdeterminanth) = 0))) \/ exists mdr_q_rank_existswitnessminornonzeroevaluationdeterminanths mdr_eb_rank_existswitnessminornonzeroevaluationdeterminanths mdr_ec_rank_existswitnessminornonzeroevaluationdeterminanths mdr_fb_rank_existswitnessminornonzeroevaluationdeterminanths mdr_fc_rank_existswitnessminornonzeroevaluationdeterminanths. (((mdr_d_rank_existswitnessminornonzeroevaluationdeterminanth) = S (mdr_q_rank_existswitnessminornonzeroevaluationdeterminanths)) /\ ((forall mdr_j_rank_existswitnessminornonzeroevaluationdeterminanthsc. (exists mdr_gap_rank_existswitnessminornonzeroevaluationdeterminanthscj. mdr_gap_rank_existswitnessminornonzeroevaluationdeterminanthscj + S (mdr_j_rank_existswitnessminornonzeroevaluationdeterminanthsc) = (S (mdr_q_rank_existswitnessminornonzeroevaluationdeterminanths))) -> exists mdr_i_rank_existswitnessminornonzeroevaluationdeterminanthsc mdr_up_rank_existswitnessminornonzeroevaluationdeterminanthsc mdr_us_rank_existswitnessminornonzeroevaluationdeterminanthsc mdr_un_rank_existswitnessminornonzeroevaluationdeterminanthsc mdr_ut_rank_existswitnessminornonzeroevaluationdeterminanthsc mdr_p_rank_existswitnessminornonzeroevaluationdeterminanthsc mdr_n_rank_existswitnessminornonzeroevaluationdeterminanthsc. ((exists mdr_gap_rank_existswitnessminornonzeroevaluationdeterminanthsci. mdr_gap_rank_existswitnessminornonzeroevaluationdeterminanthsci + S (mdr_i_rank_existswitnessminornonzeroevaluationdeterminanthsc) = (mdr_i_rank_existswitnessminornonzeroevaluationdeterminanth)) /\ ((exists mdr_z_rank_existswitnessminornonzeroevaluationdeterminanthscr. ((exists mdr_a_rank_existswitnessminornonzeroevaluationdeterminanthscrc mdr_b_rank_existswitnessminornonzeroevaluationdeterminanthscrc mdr_c_rank_existswitnessminornonzeroevaluationdeterminanthscrc mdr_e_rank_existswitnessminornonzeroevaluationdeterminanthscrc mdr_f_rank_existswitnessminornonzeroevaluationdeterminanthscrc. ((mdr_a_rank_existswitnessminornonzeroevaluationdeterminanthscrc = ((mdr_q_rank_existswitnessminornonzeroevaluationdeterminanths) + (mdr_up_rank_existswitnessminornonzeroevaluationdeterminanthsc)) * S ((mdr_q_rank_existswitnessminornonzeroevaluationdeterminanths) + (mdr_up_rank_existswitnessminornonzeroevaluationdeterminanthsc)) + ((mdr_up_rank_existswitnessminornonzeroevaluationdeterminanthsc) + (mdr_up_rank_existswitnessminornonzeroevaluationdeterminanthsc))) /\ ((mdr_b_rank_existswitnessminornonzeroevaluationdeterminanthscrc = ((mdr_us_rank_existswitnessminornonzeroevaluationdeterminanthsc) + (mdr_un_rank_existswitnessminornonzeroevaluationdeterminanthsc)) * S ((mdr_us_rank_existswitnessminornonzeroevaluationdeterminanthsc) + (mdr_un_rank_existswitnessminornonzeroevaluationdeterminanthsc)) + ((mdr_un_rank_existswitnessminornonzeroevaluationdeterminanthsc) + (mdr_un_rank_existswitnessminornonzeroevaluationdeterminanthsc))) /\ ((mdr_c_rank_existswitnessminornonzeroevaluationdeterminanthscrc = ((mdr_a_rank_existswitnessminornonzeroevaluationdeterminanthscrc) + (mdr_b_rank_existswitnessminornonzeroevaluationdeterminanthscrc)) * S ((mdr_a_rank_existswitnessminornonzeroevaluationdeterminanthscrc) + (mdr_b_rank_existswitnessminornonzeroevaluationdeterminanthscrc)) + ((mdr_b_rank_existswitnessminornonzeroevaluationdeterminanthscrc) + (mdr_b_rank_existswitnessminornonzeroevaluationdeterminanthscrc))) /\ ((mdr_e_rank_existswitnessminornonzeroevaluationdeterminanthscrc = ((mdr_p_rank_existswitnessminornonzeroevaluationdeterminanthsc) + (mdr_n_rank_existswitnessminornonzeroevaluationdeterminanthsc)) * S ((mdr_p_rank_existswitnessminornonzeroevaluationdeterminanthsc) + (mdr_n_rank_existswitnessminornonzeroevaluationdeterminanthsc)) + ((mdr_n_rank_existswitnessminornonzeroevaluationdeterminanthsc) + (mdr_n_rank_existswitnessminornonzeroevaluationdeterminanthsc))) /\ ((mdr_f_rank_existswitnessminornonzeroevaluationdeterminanthscrc = ((mdr_ut_rank_existswitnessminornonzeroevaluationdeterminanthsc) + (mdr_e_rank_existswitnessminornonzeroevaluationdeterminanthscrc)) * S ((mdr_ut_rank_existswitnessminornonzeroevaluationdeterminanthsc) + (mdr_e_rank_existswitnessminornonzeroevaluationdeterminanthscrc)) + ((mdr_e_rank_existswitnessminornonzeroevaluationdeterminanthscrc) + (mdr_e_rank_existswitnessminornonzeroevaluationdeterminanthscrc))) /\ ((mdr_z_rank_existswitnessminornonzeroevaluationdeterminanthscr) = ((mdr_c_rank_existswitnessminornonzeroevaluationdeterminanthscrc) + (mdr_f_rank_existswitnessminornonzeroevaluationdeterminanthscrc)) * S ((mdr_c_rank_existswitnessminornonzeroevaluationdeterminanthscrc) + (mdr_f_rank_existswitnessminornonzeroevaluationdeterminanthscrc)) + ((mdr_f_rank_existswitnessminornonzeroevaluationdeterminanthscrc) + (mdr_f_rank_existswitnessminornonzeroevaluationdeterminanthscrc))))))))) /\ (((exists ff_h_mdr_rank_existswitnessminornonzeroevaluationdeterminanthscrb. ff_h_mdr_rank_existswitnessminornonzeroevaluationdeterminanthscrb + S (mdr_z_rank_existswitnessminornonzeroevaluationdeterminanthscr) = S ((S (mdr_i_rank_existswitnessminornonzeroevaluationdeterminanthsc)) * mdr_c_rank_existswitnessminornonzeroevaluationdeterminant)) /\ exists ff_q_mdr_rank_existswitnessminornonzeroevaluationdeterminanthscrb. mdr_b_rank_existswitnessminornonzeroevaluationdeterminant = ff_q_mdr_rank_existswitnessminornonzeroevaluationdeterminanthscrb * S ((S (mdr_i_rank_existswitnessminornonzeroevaluationdeterminanthsc)) * mdr_c_rank_existswitnessminornonzeroevaluationdeterminant) + (mdr_z_rank_existswitnessminornonzeroevaluationdeterminanthscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_rank_existswitnessminornonzeroevaluationdeterminanthscm_positive. (exists ff_gap_mdm_lt_mdr_rank_existswitnessminornonzeroevaluationdeterminanthscm_positive_index_bound. ff_gap_mdm_lt_mdr_rank_existswitnessminornonzeroevaluationdeterminanthscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_rank_existswitnessminornonzeroevaluationdeterminanthscm_positive) = ((mdr_q_rank_existswitnessminornonzeroevaluationdeterminanths) * (mdr_q_rank_existswitnessminornonzeroevaluationdeterminanths))) -> exists ff_row_mdm_prefix_mdr_rank_existswitnessminornonzeroevaluationdeterminanthscm_positive ff_column_mdm_prefix_mdr_rank_existswitnessminornonzeroevaluationdeterminanthscm_positive ff_value_mdm_prefix_mdr_rank_existswitnessminornonzeroevaluationdeterminanthscm_positive. (ff_index_mdm_prefix_mdr_rank_existswitnessminornonzeroevaluationdeterminanthscm_positive = (mdr_q_rank_existswitnessminornonzeroevaluationdeterminanths) * ff_row_mdm_prefix_mdr_rank_existswitnessminornonzeroevaluationdeterminanthscm_positive + ff_column_mdm_prefix_mdr_rank_existswitnessminornonzeroevaluationdeterminanthscm_positive /\ ((exists ff_gap_mdm_lt_mdr_rank_existswitnessminornonzeroevaluationdeterminanthscm_positive_column_bound. ff_gap_mdm_lt_mdr_rank_existswitnessminornonzeroevaluationdeterminanthscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_rank_existswitnessminornonzeroevaluationdeterminanthscm_positive) = (mdr_q_rank_existswitnessminornonzeroevaluationdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_rank_existswitnessminornonzeroevaluationdeterminanthscm_positive_cell ff_column_mdm_cell_mdr_rank_existswitnessminornonzeroevaluationdeterminanthscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_rank_existswitnessminornonzeroevaluationdeterminanthscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_rank_existswitnessminornonzeroevaluationdeterminanthscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_rank_existswitnessminornonzeroevaluationdeterminanthscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_rank_existswitnessminornonzeroevaluationdeterminanthscm_positive_cell = ff_row_mdm_prefix_mdr_rank_existswitnessminornonzeroevaluationdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_rank_existswitnessminornonzeroevaluationdeterminanthscm_positive_cell_row_after. ff_gap_mdm_le_mdr_rank_existswitnessminornonzeroevaluationdeterminanthscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_rank_existswitnessminornonzeroevaluationdeterminanthscm_positive)) /\ ff_row_mdm_cell_mdr_rank_existswitnessminornonzeroevaluationdeterminanthscm_positive_cell = S ff_row_mdm_prefix_mdr_rank_existswitnessminornonzeroevaluationdeterminanthscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_rank_existswitnessminornonzeroevaluationdeterminanthscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_rank_existswitnessminornonzeroevaluationdeterminanthscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_rank_existswitnessminornonzeroevaluationdeterminanthscm_positive) = (mdr_j_rank_existswitnessminornonzeroevaluationdeterminanthsc)) /\ ff_column_mdm_cell_mdr_rank_existswitnessminornonzeroevaluationdeterminanthscm_positive_cell = ff_column_mdm_prefix_mdr_rank_existswitnessminornonzeroevaluationdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_rank_existswitnessminornonzeroevaluationdeterminanthscm_positive_cell_column_after. ff_gap_mdm_le_mdr_rank_existswitnessminornonzeroevaluationdeterminanthscm_positive_cell_column_after + (mdr_j_rank_existswitnessminornonzeroevaluationdeterminanthsc) = (ff_column_mdm_prefix_mdr_rank_existswitnessminornonzeroevaluationdeterminanthscm_positive)) /\ ff_column_mdm_cell_mdr_rank_existswitnessminornonzeroevaluationdeterminanthscm_positive_cell = S ff_column_mdm_prefix_mdr_rank_existswitnessminornonzeroevaluationdeterminanthscm_positive))) /\ (((exists ff_h_mdm_mdr_rank_existswitnessminornonzeroevaluationdeterminanthscm_positive_cell_source. ff_h_mdm_mdr_rank_existswitnessminornonzeroevaluationdeterminanthscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_rank_existswitnessminornonzeroevaluationdeterminanthscm_positive) = S ((S ((ff_row_mdm_cell_mdr_rank_existswitnessminornonzeroevaluationdeterminanthscm_positive_cell) * (S (mdr_q_rank_existswitnessminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_rank_existswitnessminornonzeroevaluationdeterminanthscm_positive_cell))) * mdr_pc_rank_existswitnessminornonzeroevaluationdeterminanth)) /\ exists ff_q_mdm_mdr_rank_existswitnessminornonzeroevaluationdeterminanthscm_positive_cell_source. mdr_pb_rank_existswitnessminornonzeroevaluationdeterminanth = ff_q_mdm_mdr_rank_existswitnessminornonzeroevaluationdeterminanthscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_rank_existswitnessminornonzeroevaluationdeterminanthscm_positive_cell) * (S (mdr_q_rank_existswitnessminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_rank_existswitnessminornonzeroevaluationdeterminanthscm_positive_cell))) * mdr_pc_rank_existswitnessminornonzeroevaluationdeterminanth) + (ff_value_mdm_prefix_mdr_rank_existswitnessminornonzeroevaluationdeterminanthscm_positive)))))) /\ (((exists ff_h_mdm_mdr_rank_existswitnessminornonzeroevaluationdeterminanthscm_positive_target. ff_h_mdm_mdr_rank_existswitnessminornonzeroevaluationdeterminanthscm_positive_target + S (ff_value_mdm_prefix_mdr_rank_existswitnessminornonzeroevaluationdeterminanthscm_positive) = S ((S (ff_index_mdm_prefix_mdr_rank_existswitnessminornonzeroevaluationdeterminanthscm_positive)) * mdr_us_rank_existswitnessminornonzeroevaluationdeterminanthsc)) /\ exists ff_q_mdm_mdr_rank_existswitnessminornonzeroevaluationdeterminanthscm_positive_target. mdr_up_rank_existswitnessminornonzeroevaluationdeterminanthsc = ff_q_mdm_mdr_rank_existswitnessminornonzeroevaluationdeterminanthscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_rank_existswitnessminornonzeroevaluationdeterminanthscm_positive)) * mdr_us_rank_existswitnessminornonzeroevaluationdeterminanthsc) + (ff_value_mdm_prefix_mdr_rank_existswitnessminornonzeroevaluationdeterminanthscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_rank_existswitnessminornonzeroevaluationdeterminanthscm_negative. (exists ff_gap_mdm_lt_mdr_rank_existswitnessminornonzeroevaluationdeterminanthscm_negative_index_bound. ff_gap_mdm_lt_mdr_rank_existswitnessminornonzeroevaluationdeterminanthscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_rank_existswitnessminornonzeroevaluationdeterminanthscm_negative) = ((mdr_q_rank_existswitnessminornonzeroevaluationdeterminanths) * (mdr_q_rank_existswitnessminornonzeroevaluationdeterminanths))) -> exists ff_row_mdm_prefix_mdr_rank_existswitnessminornonzeroevaluationdeterminanthscm_negative ff_column_mdm_prefix_mdr_rank_existswitnessminornonzeroevaluationdeterminanthscm_negative ff_value_mdm_prefix_mdr_rank_existswitnessminornonzeroevaluationdeterminanthscm_negative. (ff_index_mdm_prefix_mdr_rank_existswitnessminornonzeroevaluationdeterminanthscm_negative = (mdr_q_rank_existswitnessminornonzeroevaluationdeterminanths) * ff_row_mdm_prefix_mdr_rank_existswitnessminornonzeroevaluationdeterminanthscm_negative + ff_column_mdm_prefix_mdr_rank_existswitnessminornonzeroevaluationdeterminanthscm_negative /\ ((exists ff_gap_mdm_lt_mdr_rank_existswitnessminornonzeroevaluationdeterminanthscm_negative_column_bound. ff_gap_mdm_lt_mdr_rank_existswitnessminornonzeroevaluationdeterminanthscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_rank_existswitnessminornonzeroevaluationdeterminanthscm_negative) = (mdr_q_rank_existswitnessminornonzeroevaluationdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_rank_existswitnessminornonzeroevaluationdeterminanthscm_negative_cell ff_column_mdm_cell_mdr_rank_existswitnessminornonzeroevaluationdeterminanthscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_rank_existswitnessminornonzeroevaluationdeterminanthscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_rank_existswitnessminornonzeroevaluationdeterminanthscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_rank_existswitnessminornonzeroevaluationdeterminanthscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_rank_existswitnessminornonzeroevaluationdeterminanthscm_negative_cell = ff_row_mdm_prefix_mdr_rank_existswitnessminornonzeroevaluationdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_rank_existswitnessminornonzeroevaluationdeterminanthscm_negative_cell_row_after. ff_gap_mdm_le_mdr_rank_existswitnessminornonzeroevaluationdeterminanthscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_rank_existswitnessminornonzeroevaluationdeterminanthscm_negative)) /\ ff_row_mdm_cell_mdr_rank_existswitnessminornonzeroevaluationdeterminanthscm_negative_cell = S ff_row_mdm_prefix_mdr_rank_existswitnessminornonzeroevaluationdeterminanthscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_rank_existswitnessminornonzeroevaluationdeterminanthscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_rank_existswitnessminornonzeroevaluationdeterminanthscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_rank_existswitnessminornonzeroevaluationdeterminanthscm_negative) = (mdr_j_rank_existswitnessminornonzeroevaluationdeterminanthsc)) /\ ff_column_mdm_cell_mdr_rank_existswitnessminornonzeroevaluationdeterminanthscm_negative_cell = ff_column_mdm_prefix_mdr_rank_existswitnessminornonzeroevaluationdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_rank_existswitnessminornonzeroevaluationdeterminanthscm_negative_cell_column_after. ff_gap_mdm_le_mdr_rank_existswitnessminornonzeroevaluationdeterminanthscm_negative_cell_column_after + (mdr_j_rank_existswitnessminornonzeroevaluationdeterminanthsc) = (ff_column_mdm_prefix_mdr_rank_existswitnessminornonzeroevaluationdeterminanthscm_negative)) /\ ff_column_mdm_cell_mdr_rank_existswitnessminornonzeroevaluationdeterminanthscm_negative_cell = S ff_column_mdm_prefix_mdr_rank_existswitnessminornonzeroevaluationdeterminanthscm_negative))) /\ (((exists ff_h_mdm_mdr_rank_existswitnessminornonzeroevaluationdeterminanthscm_negative_cell_source. ff_h_mdm_mdr_rank_existswitnessminornonzeroevaluationdeterminanthscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_rank_existswitnessminornonzeroevaluationdeterminanthscm_negative) = S ((S ((ff_row_mdm_cell_mdr_rank_existswitnessminornonzeroevaluationdeterminanthscm_negative_cell) * (S (mdr_q_rank_existswitnessminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_rank_existswitnessminornonzeroevaluationdeterminanthscm_negative_cell))) * mdr_nc_rank_existswitnessminornonzeroevaluationdeterminanth)) /\ exists ff_q_mdm_mdr_rank_existswitnessminornonzeroevaluationdeterminanthscm_negative_cell_source. mdr_nb_rank_existswitnessminornonzeroevaluationdeterminanth = ff_q_mdm_mdr_rank_existswitnessminornonzeroevaluationdeterminanthscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_rank_existswitnessminornonzeroevaluationdeterminanthscm_negative_cell) * (S (mdr_q_rank_existswitnessminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_rank_existswitnessminornonzeroevaluationdeterminanthscm_negative_cell))) * mdr_nc_rank_existswitnessminornonzeroevaluationdeterminanth) + (ff_value_mdm_prefix_mdr_rank_existswitnessminornonzeroevaluationdeterminanthscm_negative)))))) /\ (((exists ff_h_mdm_mdr_rank_existswitnessminornonzeroevaluationdeterminanthscm_negative_target. ff_h_mdm_mdr_rank_existswitnessminornonzeroevaluationdeterminanthscm_negative_target + S (ff_value_mdm_prefix_mdr_rank_existswitnessminornonzeroevaluationdeterminanthscm_negative) = S ((S (ff_index_mdm_prefix_mdr_rank_existswitnessminornonzeroevaluationdeterminanthscm_negative)) * mdr_ut_rank_existswitnessminornonzeroevaluationdeterminanthsc)) /\ exists ff_q_mdm_mdr_rank_existswitnessminornonzeroevaluationdeterminanthscm_negative_target. mdr_un_rank_existswitnessminornonzeroevaluationdeterminanthsc = ff_q_mdm_mdr_rank_existswitnessminornonzeroevaluationdeterminanthscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_rank_existswitnessminornonzeroevaluationdeterminanthscm_negative)) * mdr_ut_rank_existswitnessminornonzeroevaluationdeterminanthsc) + (ff_value_mdm_prefix_mdr_rank_existswitnessminornonzeroevaluationdeterminanthscm_negative))))))))) /\ ((((exists ff_h_mdr_rank_existswitnessminornonzeroevaluationdeterminanthscp. ff_h_mdr_rank_existswitnessminornonzeroevaluationdeterminanthscp + S (mdr_p_rank_existswitnessminornonzeroevaluationdeterminanthsc) = S ((S (mdr_j_rank_existswitnessminornonzeroevaluationdeterminanthsc)) * mdr_ec_rank_existswitnessminornonzeroevaluationdeterminanths)) /\ exists ff_q_mdr_rank_existswitnessminornonzeroevaluationdeterminanthscp. mdr_eb_rank_existswitnessminornonzeroevaluationdeterminanths = ff_q_mdr_rank_existswitnessminornonzeroevaluationdeterminanthscp * S ((S (mdr_j_rank_existswitnessminornonzeroevaluationdeterminanthsc)) * mdr_ec_rank_existswitnessminornonzeroevaluationdeterminanths) + (mdr_p_rank_existswitnessminornonzeroevaluationdeterminanthsc))) /\ (((exists ff_h_mdr_rank_existswitnessminornonzeroevaluationdeterminanthscn. ff_h_mdr_rank_existswitnessminornonzeroevaluationdeterminanthscn + S (mdr_n_rank_existswitnessminornonzeroevaluationdeterminanthsc) = S ((S (mdr_j_rank_existswitnessminornonzeroevaluationdeterminanthsc)) * mdr_fc_rank_existswitnessminornonzeroevaluationdeterminanths)) /\ exists ff_q_mdr_rank_existswitnessminornonzeroevaluationdeterminanthscn. mdr_fb_rank_existswitnessminornonzeroevaluationdeterminanths = ff_q_mdr_rank_existswitnessminornonzeroevaluationdeterminanthscn * S ((S (mdr_j_rank_existswitnessminornonzeroevaluationdeterminanthsc)) * mdr_fc_rank_existswitnessminornonzeroevaluationdeterminanths) + (mdr_n_rank_existswitnessminornonzeroevaluationdeterminanthsc)))))))) /\ (exists ff_ub_mce_fold_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf ff_uc_mce_fold_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf ff_vb_mce_fold_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf ff_vc_mce_fold_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf. ((forall ff_index_mce_alternating_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_prefix. (exists ff_gap_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_prefix_index. ff_gap_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_prefix_index + S (ff_index_mce_alternating_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_prefix) = (S (mdr_q_rank_existswitnessminornonzeroevaluationdeterminanths))) -> exists ff_ap_mce_alternating_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_prefix ff_an_mce_alternating_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_prefix ff_bp_mce_alternating_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_prefix ff_bn_mce_alternating_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_prefix ff_p_mce_alternating_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_prefix ff_n_mce_alternating_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_prefix. ((((exists ff_h_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_prefix_ap. ff_h_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_prefix_ap + S (ff_ap_mce_alternating_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_prefix)) * mdr_pc_rank_existswitnessminornonzeroevaluationdeterminanth)) /\ exists ff_q_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_prefix_ap. mdr_pb_rank_existswitnessminornonzeroevaluationdeterminanth = ff_q_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_prefix)) * mdr_pc_rank_existswitnessminornonzeroevaluationdeterminanth) + (ff_ap_mce_alternating_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_prefix_an. ff_h_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_prefix_an + S (ff_an_mce_alternating_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_prefix)) * mdr_nc_rank_existswitnessminornonzeroevaluationdeterminanth)) /\ exists ff_q_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_prefix_an. mdr_nb_rank_existswitnessminornonzeroevaluationdeterminanth = ff_q_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_prefix)) * mdr_nc_rank_existswitnessminornonzeroevaluationdeterminanth) + (ff_an_mce_alternating_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_prefix_bp. ff_h_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_prefix_bp + S (ff_bp_mce_alternating_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_prefix)) * mdr_ec_rank_existswitnessminornonzeroevaluationdeterminanths)) /\ exists ff_q_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_prefix_bp. mdr_eb_rank_existswitnessminornonzeroevaluationdeterminanths = ff_q_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_prefix)) * mdr_ec_rank_existswitnessminornonzeroevaluationdeterminanths) + (ff_bp_mce_alternating_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_prefix_bn. ff_h_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_prefix_bn + S (ff_bn_mce_alternating_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_prefix)) * mdr_fc_rank_existswitnessminornonzeroevaluationdeterminanths)) /\ exists ff_q_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_prefix_bn. mdr_fb_rank_existswitnessminornonzeroevaluationdeterminanths = ff_q_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_prefix)) * mdr_fc_rank_existswitnessminornonzeroevaluationdeterminanths) + (ff_bn_mce_alternating_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_prefix_positive. ff_h_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_prefix_positive + S (ff_p_mce_alternating_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_prefix_positive. ff_ub_mce_fold_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf) + (ff_p_mce_alternating_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_prefix_negative. ff_h_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_prefix_negative + S (ff_n_mce_alternating_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_prefix_negative. ff_vb_mce_fold_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf) + (ff_n_mce_alternating_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_prefix))) /\ (((exists ff_even_mce_term_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_prefix = 2 * ff_even_mce_term_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_prefix_term) /\ (ff_p_mce_alternating_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_prefix = 2 * ff_odd_mce_term_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_positive ff_v_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_positive. ((((exists ff_h_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_positive_start. ff_h_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_positive_start. ff_u_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_positive_start * S ((S (0)) * ff_v_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_positive_terminal. ff_h_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_positive_terminal + S (mdr_p_rank_existswitnessminornonzeroevaluationdeterminanth) = S ((S ((S (mdr_q_rank_existswitnessminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_positive_terminal. ff_u_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_positive_terminal * S ((S ((S (mdr_q_rank_existswitnessminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_positive) + (mdr_p_rank_existswitnessminornonzeroevaluationdeterminanth))) /\ forall ff_i_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_positive. (exists ff_lt_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_positive_bound. ff_lt_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_positive_bound + S ff_i_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_positive = (S (mdr_q_rank_existswitnessminornonzeroevaluationdeterminanths))) -> exists ff_a_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_positive ff_r_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_positive ff_s_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_positive. ((((exists ff_h_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_positive_summand. ff_h_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_positive_summand + S (ff_a_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_positive_summand. ff_ub_mce_fold_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_positive_summand * S ((S (ff_i_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf) + (ff_a_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_positive_partial. ff_h_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_positive_partial + S (ff_r_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_positive_partial. ff_u_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_positive_partial * S ((S (ff_i_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_positive) + (ff_r_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_positive_successor. ff_h_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_positive_successor + S (ff_s_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_positive) = S ((S (S ff_i_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_positive_successor. ff_u_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_positive_successor * S ((S (S ff_i_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_positive) + (ff_s_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_positive))) /\ ff_s_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_positive = ff_r_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_positive + ff_a_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_positive)))))) /\ (exists ff_u_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_negative ff_v_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_negative. ((((exists ff_h_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_negative_start. ff_h_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_negative_start. ff_u_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_negative_start * S ((S (0)) * ff_v_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_negative_terminal. ff_h_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_negative_terminal + S (mdr_n_rank_existswitnessminornonzeroevaluationdeterminanth) = S ((S ((S (mdr_q_rank_existswitnessminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_negative_terminal. ff_u_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_negative_terminal * S ((S ((S (mdr_q_rank_existswitnessminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_negative) + (mdr_n_rank_existswitnessminornonzeroevaluationdeterminanth))) /\ forall ff_i_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_negative. (exists ff_lt_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_negative_bound. ff_lt_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_negative_bound + S ff_i_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_negative = (S (mdr_q_rank_existswitnessminornonzeroevaluationdeterminanths))) -> exists ff_a_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_negative ff_r_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_negative ff_s_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_negative. ((((exists ff_h_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_negative_summand. ff_h_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_negative_summand + S (ff_a_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_negative_summand. ff_vb_mce_fold_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_negative_summand * S ((S (ff_i_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf) + (ff_a_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_negative_partial. ff_h_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_negative_partial + S (ff_r_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_negative_partial. ff_u_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_negative_partial * S ((S (ff_i_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_negative) + (ff_r_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_negative_successor. ff_h_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_negative_successor + S (ff_s_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_negative) = S ((S (S ff_i_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_negative_successor. ff_u_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_negative_successor * S ((S (S ff_i_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_negative) + (ff_s_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_negative))) /\ ff_s_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_negative = ff_r_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_negative + ff_a_mce_mdr_rank_existswitnessminornonzeroevaluationdeterminanthsf_negative))))))))))))))) /\ ((exists mdr_gap_rank_existswitnessminornonzeroevaluationdeterminanti. mdr_gap_rank_existswitnessminornonzeroevaluationdeterminanti + S (mdr_i_rank_existswitnessminornonzeroevaluationdeterminant) = (mdr_l_rank_existswitnessminornonzeroevaluationdeterminant)) /\ (exists mdr_z_rank_existswitnessminornonzeroevaluationdeterminantr. ((exists mdr_a_rank_existswitnessminornonzeroevaluationdeterminantrc mdr_b_rank_existswitnessminornonzeroevaluationdeterminantrc mdr_c_rank_existswitnessminornonzeroevaluationdeterminantrc mdr_e_rank_existswitnessminornonzeroevaluationdeterminantrc mdr_f_rank_existswitnessminornonzeroevaluationdeterminantrc. ((mdr_a_rank_existswitnessminornonzeroevaluationdeterminantrc = ((rank) + (mdr_ub_rank_existswitnessminornonzeroevaluation)) * S ((rank) + (mdr_ub_rank_existswitnessminornonzeroevaluation)) + ((mdr_ub_rank_existswitnessminornonzeroevaluation) + (mdr_ub_rank_existswitnessminornonzeroevaluation))) /\ ((mdr_b_rank_existswitnessminornonzeroevaluationdeterminantrc = ((mdr_uc_rank_existswitnessminornonzeroevaluation) + (mdr_vb_rank_existswitnessminornonzeroevaluation)) * S ((mdr_uc_rank_existswitnessminornonzeroevaluation) + (mdr_vb_rank_existswitnessminornonzeroevaluation)) + ((mdr_vb_rank_existswitnessminornonzeroevaluation) + (mdr_vb_rank_existswitnessminornonzeroevaluation))) /\ ((mdr_c_rank_existswitnessminornonzeroevaluationdeterminantrc = ((mdr_a_rank_existswitnessminornonzeroevaluationdeterminantrc) + (mdr_b_rank_existswitnessminornonzeroevaluationdeterminantrc)) * S ((mdr_a_rank_existswitnessminornonzeroevaluationdeterminantrc) + (mdr_b_rank_existswitnessminornonzeroevaluationdeterminantrc)) + ((mdr_b_rank_existswitnessminornonzeroevaluationdeterminantrc) + (mdr_b_rank_existswitnessminornonzeroevaluationdeterminantrc))) /\ ((mdr_e_rank_existswitnessminornonzeroevaluationdeterminantrc = ((mdr_p_rank_existswitnessminornonzero) + (mdr_n_rank_existswitnessminornonzero)) * S ((mdr_p_rank_existswitnessminornonzero) + (mdr_n_rank_existswitnessminornonzero)) + ((mdr_n_rank_existswitnessminornonzero) + (mdr_n_rank_existswitnessminornonzero))) /\ ((mdr_f_rank_existswitnessminornonzeroevaluationdeterminantrc = ((mdr_vc_rank_existswitnessminornonzeroevaluation) + (mdr_e_rank_existswitnessminornonzeroevaluationdeterminantrc)) * S ((mdr_vc_rank_existswitnessminornonzeroevaluation) + (mdr_e_rank_existswitnessminornonzeroevaluationdeterminantrc)) + ((mdr_e_rank_existswitnessminornonzeroevaluationdeterminantrc) + (mdr_e_rank_existswitnessminornonzeroevaluationdeterminantrc))) /\ ((mdr_z_rank_existswitnessminornonzeroevaluationdeterminantr) = ((mdr_c_rank_existswitnessminornonzeroevaluationdeterminantrc) + (mdr_f_rank_existswitnessminornonzeroevaluationdeterminantrc)) * S ((mdr_c_rank_existswitnessminornonzeroevaluationdeterminantrc) + (mdr_f_rank_existswitnessminornonzeroevaluationdeterminantrc)) + ((mdr_f_rank_existswitnessminornonzeroevaluationdeterminantrc) + (mdr_f_rank_existswitnessminornonzeroevaluationdeterminantrc))))))))) /\ (((exists ff_h_mdr_rank_existswitnessminornonzeroevaluationdeterminantrb. ff_h_mdr_rank_existswitnessminornonzeroevaluationdeterminantrb + S (mdr_z_rank_existswitnessminornonzeroevaluationdeterminantr) = S ((S (mdr_i_rank_existswitnessminornonzeroevaluationdeterminant)) * mdr_c_rank_existswitnessminornonzeroevaluationdeterminant)) /\ exists ff_q_mdr_rank_existswitnessminornonzeroevaluationdeterminantrb. mdr_b_rank_existswitnessminornonzeroevaluationdeterminant = ff_q_mdr_rank_existswitnessminornonzeroevaluationdeterminantrb * S ((S (mdr_i_rank_existswitnessminornonzeroevaluationdeterminant)) * mdr_c_rank_existswitnessminornonzeroevaluationdeterminant) + (mdr_z_rank_existswitnessminornonzeroevaluationdeterminantr)))))))))) /\ (~(mdr_p_rank_existswitnessminornonzero = mdr_n_rank_existswitnessminornonzero)))))))) /\ (forall mdr_q_rank_exists. (exists mdr_gap_rank_existshigher. mdr_gap_rank_existshigher + S (rank) = (mdr_q_rank_exists)) -> (forall mdr_rb_rank_existszero mdr_rc_rank_existszero mdr_cb_rank_existszero mdr_cc_rank_existszero mdr_p_rank_existszero mdr_n_rank_existszero. (((forall fom_index_mrf_rank_existszerorowsbound. (exists fom_gap_mrf_rank_existszerorowsbound_index_bound. fom_gap_mrf_rank_existszerorowsbound_index_bound + S (fom_index_mrf_rank_existszerorowsbound) = mdr_q_rank_exists) -> exists fom_value_mrf_rank_existszerorowsbound. ((((exists fom_beta_height_mrf_rank_existszerorowsbound_entry. fom_beta_height_mrf_rank_existszerorowsbound_entry + S (fom_value_mrf_rank_existszerorowsbound) = S ((S (fom_index_mrf_rank_existszerorowsbound)) * mdr_rc_rank_existszero)) /\ exists fom_beta_quotient_mrf_rank_existszerorowsbound_entry. mdr_rb_rank_existszero = fom_beta_quotient_mrf_rank_existszerorowsbound_entry * S ((S (fom_index_mrf_rank_existszerorowsbound)) * mdr_rc_rank_existszero) + (fom_value_mrf_rank_existszerorowsbound))) /\ (exists fom_gap_mrf_rank_existszerorowsbound_value_bound. fom_gap_mrf_rank_existszerorowsbound_value_bound + S (fom_value_mrf_rank_existszerorowsbound) = r))) /\ (forall mdr_i_rank_existszerorowsdistinct mdr_j_rank_existszerorowsdistinct mdr_a_rank_existszerorowsdistinct. (exists mdr_gap_rank_existszerorowsdistincti. mdr_gap_rank_existszerorowsdistincti + S (mdr_i_rank_existszerorowsdistinct) = (mdr_q_rank_exists)) -> (exists mdr_gap_rank_existszerorowsdistinctj. mdr_gap_rank_existszerorowsdistinctj + S (mdr_j_rank_existszerorowsdistinct) = (mdr_q_rank_exists)) -> (((exists ff_h_mdr_rank_existszerorowsdistinctfirst. ff_h_mdr_rank_existszerorowsdistinctfirst + S (mdr_a_rank_existszerorowsdistinct) = S ((S (mdr_i_rank_existszerorowsdistinct)) * mdr_rc_rank_existszero)) /\ exists ff_q_mdr_rank_existszerorowsdistinctfirst. mdr_rb_rank_existszero = ff_q_mdr_rank_existszerorowsdistinctfirst * S ((S (mdr_i_rank_existszerorowsdistinct)) * mdr_rc_rank_existszero) + (mdr_a_rank_existszerorowsdistinct))) -> (((exists ff_h_mdr_rank_existszerorowsdistinctsecond. ff_h_mdr_rank_existszerorowsdistinctsecond + S (mdr_a_rank_existszerorowsdistinct) = S ((S (mdr_j_rank_existszerorowsdistinct)) * mdr_rc_rank_existszero)) /\ exists ff_q_mdr_rank_existszerorowsdistinctsecond. mdr_rb_rank_existszero = ff_q_mdr_rank_existszerorowsdistinctsecond * S ((S (mdr_j_rank_existszerorowsdistinct)) * mdr_rc_rank_existszero) + (mdr_a_rank_existszerorowsdistinct))) -> mdr_i_rank_existszerorowsdistinct = mdr_j_rank_existszerorowsdistinct))) -> (((forall fom_index_mrf_rank_existszerocolumnsbound. (exists fom_gap_mrf_rank_existszerocolumnsbound_index_bound. fom_gap_mrf_rank_existszerocolumnsbound_index_bound + S (fom_index_mrf_rank_existszerocolumnsbound) = mdr_q_rank_exists) -> exists fom_value_mrf_rank_existszerocolumnsbound. ((((exists fom_beta_height_mrf_rank_existszerocolumnsbound_entry. fom_beta_height_mrf_rank_existszerocolumnsbound_entry + S (fom_value_mrf_rank_existszerocolumnsbound) = S ((S (fom_index_mrf_rank_existszerocolumnsbound)) * mdr_cc_rank_existszero)) /\ exists fom_beta_quotient_mrf_rank_existszerocolumnsbound_entry. mdr_cb_rank_existszero = fom_beta_quotient_mrf_rank_existszerocolumnsbound_entry * S ((S (fom_index_mrf_rank_existszerocolumnsbound)) * mdr_cc_rank_existszero) + (fom_value_mrf_rank_existszerocolumnsbound))) /\ (exists fom_gap_mrf_rank_existszerocolumnsbound_value_bound. fom_gap_mrf_rank_existszerocolumnsbound_value_bound + S (fom_value_mrf_rank_existszerocolumnsbound) = w))) /\ (forall mdr_i_rank_existszerocolumnsdistinct mdr_j_rank_existszerocolumnsdistinct mdr_a_rank_existszerocolumnsdistinct. (exists mdr_gap_rank_existszerocolumnsdistincti. mdr_gap_rank_existszerocolumnsdistincti + S (mdr_i_rank_existszerocolumnsdistinct) = (mdr_q_rank_exists)) -> (exists mdr_gap_rank_existszerocolumnsdistinctj. mdr_gap_rank_existszerocolumnsdistinctj + S (mdr_j_rank_existszerocolumnsdistinct) = (mdr_q_rank_exists)) -> (((exists ff_h_mdr_rank_existszerocolumnsdistinctfirst. ff_h_mdr_rank_existszerocolumnsdistinctfirst + S (mdr_a_rank_existszerocolumnsdistinct) = S ((S (mdr_i_rank_existszerocolumnsdistinct)) * mdr_cc_rank_existszero)) /\ exists ff_q_mdr_rank_existszerocolumnsdistinctfirst. mdr_cb_rank_existszero = ff_q_mdr_rank_existszerocolumnsdistinctfirst * S ((S (mdr_i_rank_existszerocolumnsdistinct)) * mdr_cc_rank_existszero) + (mdr_a_rank_existszerocolumnsdistinct))) -> (((exists ff_h_mdr_rank_existszerocolumnsdistinctsecond. ff_h_mdr_rank_existszerocolumnsdistinctsecond + S (mdr_a_rank_existszerocolumnsdistinct) = S ((S (mdr_j_rank_existszerocolumnsdistinct)) * mdr_cc_rank_existszero)) /\ exists ff_q_mdr_rank_existszerocolumnsdistinctsecond. mdr_cb_rank_existszero = ff_q_mdr_rank_existszerocolumnsdistinctsecond * S ((S (mdr_j_rank_existszerocolumnsdistinct)) * mdr_cc_rank_existszero) + (mdr_a_rank_existszerocolumnsdistinct))) -> mdr_i_rank_existszerocolumnsdistinct = mdr_j_rank_existszerocolumnsdistinct))) -> (exists mdr_ub_rank_existszeroevaluation mdr_uc_rank_existszeroevaluation mdr_vb_rank_existszeroevaluation mdr_vc_rank_existszeroevaluation. ((((forall mdr_i_rank_existszeroevaluationmatrixpositive. (exists mdr_gap_rank_existszeroevaluationmatrixpositivebound. mdr_gap_rank_existszeroevaluationmatrixpositivebound + S (mdr_i_rank_existszeroevaluationmatrixpositive) = ((mdr_q_rank_exists) * (mdr_q_rank_exists))) -> exists mdr_a_rank_existszeroevaluationmatrixpositive. (((exists mdr_r_rank_existszeroevaluationmatrixpositivepoint mdr_s_rank_existszeroevaluationmatrixpositivepoint mdr_u_rank_existszeroevaluationmatrixpositivepoint mdr_v_rank_existszeroevaluationmatrixpositivepoint. ((mdr_i_rank_existszeroevaluationmatrixpositive = (mdr_q_rank_exists) * mdr_r_rank_existszeroevaluationmatrixpositivepoint + mdr_s_rank_existszeroevaluationmatrixpositivepoint) /\ ((exists mdr_gap_rank_existszeroevaluationmatrixpositivepointcolumn. mdr_gap_rank_existszeroevaluationmatrixpositivepointcolumn + S (mdr_s_rank_existszeroevaluationmatrixpositivepoint) = (mdr_q_rank_exists)) /\ ((((exists ff_h_mdr_rank_existszeroevaluationmatrixpositivepointrow_index. ff_h_mdr_rank_existszeroevaluationmatrixpositivepointrow_index + S (mdr_u_rank_existszeroevaluationmatrixpositivepoint) = S ((S (mdr_r_rank_existszeroevaluationmatrixpositivepoint)) * mdr_rc_rank_existszero)) /\ exists ff_q_mdr_rank_existszeroevaluationmatrixpositivepointrow_index. mdr_rb_rank_existszero = ff_q_mdr_rank_existszeroevaluationmatrixpositivepointrow_index * S ((S (mdr_r_rank_existszeroevaluationmatrixpositivepoint)) * mdr_rc_rank_existszero) + (mdr_u_rank_existszeroevaluationmatrixpositivepoint))) /\ ((((exists ff_h_mdr_rank_existszeroevaluationmatrixpositivepointcolumn_index. ff_h_mdr_rank_existszeroevaluationmatrixpositivepointcolumn_index + S (mdr_v_rank_existszeroevaluationmatrixpositivepoint) = S ((S (mdr_s_rank_existszeroevaluationmatrixpositivepoint)) * mdr_cc_rank_existszero)) /\ exists ff_q_mdr_rank_existszeroevaluationmatrixpositivepointcolumn_index. mdr_cb_rank_existszero = ff_q_mdr_rank_existszeroevaluationmatrixpositivepointcolumn_index * S ((S (mdr_s_rank_existszeroevaluationmatrixpositivepoint)) * mdr_cc_rank_existszero) + (mdr_v_rank_existszeroevaluationmatrixpositivepoint))) /\ (((exists ff_h_mdr_rank_existszeroevaluationmatrixpositivepointsource. ff_h_mdr_rank_existszeroevaluationmatrixpositivepointsource + S (mdr_a_rank_existszeroevaluationmatrixpositive) = S ((S ((mdr_u_rank_existszeroevaluationmatrixpositivepoint) * (w) + (mdr_v_rank_existszeroevaluationmatrixpositivepoint))) * pc)) /\ exists ff_q_mdr_rank_existszeroevaluationmatrixpositivepointsource. pb = ff_q_mdr_rank_existszeroevaluationmatrixpositivepointsource * S ((S ((mdr_u_rank_existszeroevaluationmatrixpositivepoint) * (w) + (mdr_v_rank_existszeroevaluationmatrixpositivepoint))) * pc) + (mdr_a_rank_existszeroevaluationmatrixpositive)))))))) /\ (((exists ff_h_mdr_rank_existszeroevaluationmatrixpositiveoutput. ff_h_mdr_rank_existszeroevaluationmatrixpositiveoutput + S (mdr_a_rank_existszeroevaluationmatrixpositive) = S ((S (mdr_i_rank_existszeroevaluationmatrixpositive)) * mdr_uc_rank_existszeroevaluation)) /\ exists ff_q_mdr_rank_existszeroevaluationmatrixpositiveoutput. mdr_ub_rank_existszeroevaluation = ff_q_mdr_rank_existszeroevaluationmatrixpositiveoutput * S ((S (mdr_i_rank_existszeroevaluationmatrixpositive)) * mdr_uc_rank_existszeroevaluation) + (mdr_a_rank_existszeroevaluationmatrixpositive)))))) /\ (forall mdr_i_rank_existszeroevaluationmatrixnegative. (exists mdr_gap_rank_existszeroevaluationmatrixnegativebound. mdr_gap_rank_existszeroevaluationmatrixnegativebound + S (mdr_i_rank_existszeroevaluationmatrixnegative) = ((mdr_q_rank_exists) * (mdr_q_rank_exists))) -> exists mdr_a_rank_existszeroevaluationmatrixnegative. (((exists mdr_r_rank_existszeroevaluationmatrixnegativepoint mdr_s_rank_existszeroevaluationmatrixnegativepoint mdr_u_rank_existszeroevaluationmatrixnegativepoint mdr_v_rank_existszeroevaluationmatrixnegativepoint. ((mdr_i_rank_existszeroevaluationmatrixnegative = (mdr_q_rank_exists) * mdr_r_rank_existszeroevaluationmatrixnegativepoint + mdr_s_rank_existszeroevaluationmatrixnegativepoint) /\ ((exists mdr_gap_rank_existszeroevaluationmatrixnegativepointcolumn. mdr_gap_rank_existszeroevaluationmatrixnegativepointcolumn + S (mdr_s_rank_existszeroevaluationmatrixnegativepoint) = (mdr_q_rank_exists)) /\ ((((exists ff_h_mdr_rank_existszeroevaluationmatrixnegativepointrow_index. ff_h_mdr_rank_existszeroevaluationmatrixnegativepointrow_index + S (mdr_u_rank_existszeroevaluationmatrixnegativepoint) = S ((S (mdr_r_rank_existszeroevaluationmatrixnegativepoint)) * mdr_rc_rank_existszero)) /\ exists ff_q_mdr_rank_existszeroevaluationmatrixnegativepointrow_index. mdr_rb_rank_existszero = ff_q_mdr_rank_existszeroevaluationmatrixnegativepointrow_index * S ((S (mdr_r_rank_existszeroevaluationmatrixnegativepoint)) * mdr_rc_rank_existszero) + (mdr_u_rank_existszeroevaluationmatrixnegativepoint))) /\ ((((exists ff_h_mdr_rank_existszeroevaluationmatrixnegativepointcolumn_index. ff_h_mdr_rank_existszeroevaluationmatrixnegativepointcolumn_index + S (mdr_v_rank_existszeroevaluationmatrixnegativepoint) = S ((S (mdr_s_rank_existszeroevaluationmatrixnegativepoint)) * mdr_cc_rank_existszero)) /\ exists ff_q_mdr_rank_existszeroevaluationmatrixnegativepointcolumn_index. mdr_cb_rank_existszero = ff_q_mdr_rank_existszeroevaluationmatrixnegativepointcolumn_index * S ((S (mdr_s_rank_existszeroevaluationmatrixnegativepoint)) * mdr_cc_rank_existszero) + (mdr_v_rank_existszeroevaluationmatrixnegativepoint))) /\ (((exists ff_h_mdr_rank_existszeroevaluationmatrixnegativepointsource. ff_h_mdr_rank_existszeroevaluationmatrixnegativepointsource + S (mdr_a_rank_existszeroevaluationmatrixnegative) = S ((S ((mdr_u_rank_existszeroevaluationmatrixnegativepoint) * (w) + (mdr_v_rank_existszeroevaluationmatrixnegativepoint))) * nc)) /\ exists ff_q_mdr_rank_existszeroevaluationmatrixnegativepointsource. nb = ff_q_mdr_rank_existszeroevaluationmatrixnegativepointsource * S ((S ((mdr_u_rank_existszeroevaluationmatrixnegativepoint) * (w) + (mdr_v_rank_existszeroevaluationmatrixnegativepoint))) * nc) + (mdr_a_rank_existszeroevaluationmatrixnegative)))))))) /\ (((exists ff_h_mdr_rank_existszeroevaluationmatrixnegativeoutput. ff_h_mdr_rank_existszeroevaluationmatrixnegativeoutput + S (mdr_a_rank_existszeroevaluationmatrixnegative) = S ((S (mdr_i_rank_existszeroevaluationmatrixnegative)) * mdr_vc_rank_existszeroevaluation)) /\ exists ff_q_mdr_rank_existszeroevaluationmatrixnegativeoutput. mdr_vb_rank_existszeroevaluation = ff_q_mdr_rank_existszeroevaluationmatrixnegativeoutput * S ((S (mdr_i_rank_existszeroevaluationmatrixnegative)) * mdr_vc_rank_existszeroevaluation) + (mdr_a_rank_existszeroevaluationmatrixnegative)))))))) /\ (exists mdr_b_rank_existszeroevaluationdeterminant mdr_c_rank_existszeroevaluationdeterminant mdr_l_rank_existszeroevaluationdeterminant mdr_i_rank_existszeroevaluationdeterminant. ((forall mdr_i_rank_existszeroevaluationdeterminanth. (exists mdr_gap_rank_existszeroevaluationdeterminanthi. mdr_gap_rank_existszeroevaluationdeterminanthi + S (mdr_i_rank_existszeroevaluationdeterminanth) = (mdr_l_rank_existszeroevaluationdeterminant)) -> exists mdr_d_rank_existszeroevaluationdeterminanth mdr_pb_rank_existszeroevaluationdeterminanth mdr_pc_rank_existszeroevaluationdeterminanth mdr_nb_rank_existszeroevaluationdeterminanth mdr_nc_rank_existszeroevaluationdeterminanth mdr_p_rank_existszeroevaluationdeterminanth mdr_n_rank_existszeroevaluationdeterminanth. ((exists mdr_z_rank_existszeroevaluationdeterminanthr. ((exists mdr_a_rank_existszeroevaluationdeterminanthrc mdr_b_rank_existszeroevaluationdeterminanthrc mdr_c_rank_existszeroevaluationdeterminanthrc mdr_e_rank_existszeroevaluationdeterminanthrc mdr_f_rank_existszeroevaluationdeterminanthrc. ((mdr_a_rank_existszeroevaluationdeterminanthrc = ((mdr_d_rank_existszeroevaluationdeterminanth) + (mdr_pb_rank_existszeroevaluationdeterminanth)) * S ((mdr_d_rank_existszeroevaluationdeterminanth) + (mdr_pb_rank_existszeroevaluationdeterminanth)) + ((mdr_pb_rank_existszeroevaluationdeterminanth) + (mdr_pb_rank_existszeroevaluationdeterminanth))) /\ ((mdr_b_rank_existszeroevaluationdeterminanthrc = ((mdr_pc_rank_existszeroevaluationdeterminanth) + (mdr_nb_rank_existszeroevaluationdeterminanth)) * S ((mdr_pc_rank_existszeroevaluationdeterminanth) + (mdr_nb_rank_existszeroevaluationdeterminanth)) + ((mdr_nb_rank_existszeroevaluationdeterminanth) + (mdr_nb_rank_existszeroevaluationdeterminanth))) /\ ((mdr_c_rank_existszeroevaluationdeterminanthrc = ((mdr_a_rank_existszeroevaluationdeterminanthrc) + (mdr_b_rank_existszeroevaluationdeterminanthrc)) * S ((mdr_a_rank_existszeroevaluationdeterminanthrc) + (mdr_b_rank_existszeroevaluationdeterminanthrc)) + ((mdr_b_rank_existszeroevaluationdeterminanthrc) + (mdr_b_rank_existszeroevaluationdeterminanthrc))) /\ ((mdr_e_rank_existszeroevaluationdeterminanthrc = ((mdr_p_rank_existszeroevaluationdeterminanth) + (mdr_n_rank_existszeroevaluationdeterminanth)) * S ((mdr_p_rank_existszeroevaluationdeterminanth) + (mdr_n_rank_existszeroevaluationdeterminanth)) + ((mdr_n_rank_existszeroevaluationdeterminanth) + (mdr_n_rank_existszeroevaluationdeterminanth))) /\ ((mdr_f_rank_existszeroevaluationdeterminanthrc = ((mdr_nc_rank_existszeroevaluationdeterminanth) + (mdr_e_rank_existszeroevaluationdeterminanthrc)) * S ((mdr_nc_rank_existszeroevaluationdeterminanth) + (mdr_e_rank_existszeroevaluationdeterminanthrc)) + ((mdr_e_rank_existszeroevaluationdeterminanthrc) + (mdr_e_rank_existszeroevaluationdeterminanthrc))) /\ ((mdr_z_rank_existszeroevaluationdeterminanthr) = ((mdr_c_rank_existszeroevaluationdeterminanthrc) + (mdr_f_rank_existszeroevaluationdeterminanthrc)) * S ((mdr_c_rank_existszeroevaluationdeterminanthrc) + (mdr_f_rank_existszeroevaluationdeterminanthrc)) + ((mdr_f_rank_existszeroevaluationdeterminanthrc) + (mdr_f_rank_existszeroevaluationdeterminanthrc))))))))) /\ (((exists ff_h_mdr_rank_existszeroevaluationdeterminanthrb. ff_h_mdr_rank_existszeroevaluationdeterminanthrb + S (mdr_z_rank_existszeroevaluationdeterminanthr) = S ((S (mdr_i_rank_existszeroevaluationdeterminanth)) * mdr_c_rank_existszeroevaluationdeterminant)) /\ exists ff_q_mdr_rank_existszeroevaluationdeterminanthrb. mdr_b_rank_existszeroevaluationdeterminant = ff_q_mdr_rank_existszeroevaluationdeterminanthrb * S ((S (mdr_i_rank_existszeroevaluationdeterminanth)) * mdr_c_rank_existszeroevaluationdeterminant) + (mdr_z_rank_existszeroevaluationdeterminanthr))))) /\ (((((mdr_d_rank_existszeroevaluationdeterminanth) = 0) /\ (((mdr_p_rank_existszeroevaluationdeterminanth) = 1) /\ ((mdr_n_rank_existszeroevaluationdeterminanth) = 0))) \/ exists mdr_q_rank_existszeroevaluationdeterminanths mdr_eb_rank_existszeroevaluationdeterminanths mdr_ec_rank_existszeroevaluationdeterminanths mdr_fb_rank_existszeroevaluationdeterminanths mdr_fc_rank_existszeroevaluationdeterminanths. (((mdr_d_rank_existszeroevaluationdeterminanth) = S (mdr_q_rank_existszeroevaluationdeterminanths)) /\ ((forall mdr_j_rank_existszeroevaluationdeterminanthsc. (exists mdr_gap_rank_existszeroevaluationdeterminanthscj. mdr_gap_rank_existszeroevaluationdeterminanthscj + S (mdr_j_rank_existszeroevaluationdeterminanthsc) = (S (mdr_q_rank_existszeroevaluationdeterminanths))) -> exists mdr_i_rank_existszeroevaluationdeterminanthsc mdr_up_rank_existszeroevaluationdeterminanthsc mdr_us_rank_existszeroevaluationdeterminanthsc mdr_un_rank_existszeroevaluationdeterminanthsc mdr_ut_rank_existszeroevaluationdeterminanthsc mdr_p_rank_existszeroevaluationdeterminanthsc mdr_n_rank_existszeroevaluationdeterminanthsc. ((exists mdr_gap_rank_existszeroevaluationdeterminanthsci. mdr_gap_rank_existszeroevaluationdeterminanthsci + S (mdr_i_rank_existszeroevaluationdeterminanthsc) = (mdr_i_rank_existszeroevaluationdeterminanth)) /\ ((exists mdr_z_rank_existszeroevaluationdeterminanthscr. ((exists mdr_a_rank_existszeroevaluationdeterminanthscrc mdr_b_rank_existszeroevaluationdeterminanthscrc mdr_c_rank_existszeroevaluationdeterminanthscrc mdr_e_rank_existszeroevaluationdeterminanthscrc mdr_f_rank_existszeroevaluationdeterminanthscrc. ((mdr_a_rank_existszeroevaluationdeterminanthscrc = ((mdr_q_rank_existszeroevaluationdeterminanths) + (mdr_up_rank_existszeroevaluationdeterminanthsc)) * S ((mdr_q_rank_existszeroevaluationdeterminanths) + (mdr_up_rank_existszeroevaluationdeterminanthsc)) + ((mdr_up_rank_existszeroevaluationdeterminanthsc) + (mdr_up_rank_existszeroevaluationdeterminanthsc))) /\ ((mdr_b_rank_existszeroevaluationdeterminanthscrc = ((mdr_us_rank_existszeroevaluationdeterminanthsc) + (mdr_un_rank_existszeroevaluationdeterminanthsc)) * S ((mdr_us_rank_existszeroevaluationdeterminanthsc) + (mdr_un_rank_existszeroevaluationdeterminanthsc)) + ((mdr_un_rank_existszeroevaluationdeterminanthsc) + (mdr_un_rank_existszeroevaluationdeterminanthsc))) /\ ((mdr_c_rank_existszeroevaluationdeterminanthscrc = ((mdr_a_rank_existszeroevaluationdeterminanthscrc) + (mdr_b_rank_existszeroevaluationdeterminanthscrc)) * S ((mdr_a_rank_existszeroevaluationdeterminanthscrc) + (mdr_b_rank_existszeroevaluationdeterminanthscrc)) + ((mdr_b_rank_existszeroevaluationdeterminanthscrc) + (mdr_b_rank_existszeroevaluationdeterminanthscrc))) /\ ((mdr_e_rank_existszeroevaluationdeterminanthscrc = ((mdr_p_rank_existszeroevaluationdeterminanthsc) + (mdr_n_rank_existszeroevaluationdeterminanthsc)) * S ((mdr_p_rank_existszeroevaluationdeterminanthsc) + (mdr_n_rank_existszeroevaluationdeterminanthsc)) + ((mdr_n_rank_existszeroevaluationdeterminanthsc) + (mdr_n_rank_existszeroevaluationdeterminanthsc))) /\ ((mdr_f_rank_existszeroevaluationdeterminanthscrc = ((mdr_ut_rank_existszeroevaluationdeterminanthsc) + (mdr_e_rank_existszeroevaluationdeterminanthscrc)) * S ((mdr_ut_rank_existszeroevaluationdeterminanthsc) + (mdr_e_rank_existszeroevaluationdeterminanthscrc)) + ((mdr_e_rank_existszeroevaluationdeterminanthscrc) + (mdr_e_rank_existszeroevaluationdeterminanthscrc))) /\ ((mdr_z_rank_existszeroevaluationdeterminanthscr) = ((mdr_c_rank_existszeroevaluationdeterminanthscrc) + (mdr_f_rank_existszeroevaluationdeterminanthscrc)) * S ((mdr_c_rank_existszeroevaluationdeterminanthscrc) + (mdr_f_rank_existszeroevaluationdeterminanthscrc)) + ((mdr_f_rank_existszeroevaluationdeterminanthscrc) + (mdr_f_rank_existszeroevaluationdeterminanthscrc))))))))) /\ (((exists ff_h_mdr_rank_existszeroevaluationdeterminanthscrb. ff_h_mdr_rank_existszeroevaluationdeterminanthscrb + S (mdr_z_rank_existszeroevaluationdeterminanthscr) = S ((S (mdr_i_rank_existszeroevaluationdeterminanthsc)) * mdr_c_rank_existszeroevaluationdeterminant)) /\ exists ff_q_mdr_rank_existszeroevaluationdeterminanthscrb. mdr_b_rank_existszeroevaluationdeterminant = ff_q_mdr_rank_existszeroevaluationdeterminanthscrb * S ((S (mdr_i_rank_existszeroevaluationdeterminanthsc)) * mdr_c_rank_existszeroevaluationdeterminant) + (mdr_z_rank_existszeroevaluationdeterminanthscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_rank_existszeroevaluationdeterminanthscm_positive. (exists ff_gap_mdm_lt_mdr_rank_existszeroevaluationdeterminanthscm_positive_index_bound. ff_gap_mdm_lt_mdr_rank_existszeroevaluationdeterminanthscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_rank_existszeroevaluationdeterminanthscm_positive) = ((mdr_q_rank_existszeroevaluationdeterminanths) * (mdr_q_rank_existszeroevaluationdeterminanths))) -> exists ff_row_mdm_prefix_mdr_rank_existszeroevaluationdeterminanthscm_positive ff_column_mdm_prefix_mdr_rank_existszeroevaluationdeterminanthscm_positive ff_value_mdm_prefix_mdr_rank_existszeroevaluationdeterminanthscm_positive. (ff_index_mdm_prefix_mdr_rank_existszeroevaluationdeterminanthscm_positive = (mdr_q_rank_existszeroevaluationdeterminanths) * ff_row_mdm_prefix_mdr_rank_existszeroevaluationdeterminanthscm_positive + ff_column_mdm_prefix_mdr_rank_existszeroevaluationdeterminanthscm_positive /\ ((exists ff_gap_mdm_lt_mdr_rank_existszeroevaluationdeterminanthscm_positive_column_bound. ff_gap_mdm_lt_mdr_rank_existszeroevaluationdeterminanthscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_rank_existszeroevaluationdeterminanthscm_positive) = (mdr_q_rank_existszeroevaluationdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_rank_existszeroevaluationdeterminanthscm_positive_cell ff_column_mdm_cell_mdr_rank_existszeroevaluationdeterminanthscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_rank_existszeroevaluationdeterminanthscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_rank_existszeroevaluationdeterminanthscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_rank_existszeroevaluationdeterminanthscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_rank_existszeroevaluationdeterminanthscm_positive_cell = ff_row_mdm_prefix_mdr_rank_existszeroevaluationdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_rank_existszeroevaluationdeterminanthscm_positive_cell_row_after. ff_gap_mdm_le_mdr_rank_existszeroevaluationdeterminanthscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_rank_existszeroevaluationdeterminanthscm_positive)) /\ ff_row_mdm_cell_mdr_rank_existszeroevaluationdeterminanthscm_positive_cell = S ff_row_mdm_prefix_mdr_rank_existszeroevaluationdeterminanthscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_rank_existszeroevaluationdeterminanthscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_rank_existszeroevaluationdeterminanthscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_rank_existszeroevaluationdeterminanthscm_positive) = (mdr_j_rank_existszeroevaluationdeterminanthsc)) /\ ff_column_mdm_cell_mdr_rank_existszeroevaluationdeterminanthscm_positive_cell = ff_column_mdm_prefix_mdr_rank_existszeroevaluationdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_rank_existszeroevaluationdeterminanthscm_positive_cell_column_after. ff_gap_mdm_le_mdr_rank_existszeroevaluationdeterminanthscm_positive_cell_column_after + (mdr_j_rank_existszeroevaluationdeterminanthsc) = (ff_column_mdm_prefix_mdr_rank_existszeroevaluationdeterminanthscm_positive)) /\ ff_column_mdm_cell_mdr_rank_existszeroevaluationdeterminanthscm_positive_cell = S ff_column_mdm_prefix_mdr_rank_existszeroevaluationdeterminanthscm_positive))) /\ (((exists ff_h_mdm_mdr_rank_existszeroevaluationdeterminanthscm_positive_cell_source. ff_h_mdm_mdr_rank_existszeroevaluationdeterminanthscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_rank_existszeroevaluationdeterminanthscm_positive) = S ((S ((ff_row_mdm_cell_mdr_rank_existszeroevaluationdeterminanthscm_positive_cell) * (S (mdr_q_rank_existszeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_rank_existszeroevaluationdeterminanthscm_positive_cell))) * mdr_pc_rank_existszeroevaluationdeterminanth)) /\ exists ff_q_mdm_mdr_rank_existszeroevaluationdeterminanthscm_positive_cell_source. mdr_pb_rank_existszeroevaluationdeterminanth = ff_q_mdm_mdr_rank_existszeroevaluationdeterminanthscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_rank_existszeroevaluationdeterminanthscm_positive_cell) * (S (mdr_q_rank_existszeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_rank_existszeroevaluationdeterminanthscm_positive_cell))) * mdr_pc_rank_existszeroevaluationdeterminanth) + (ff_value_mdm_prefix_mdr_rank_existszeroevaluationdeterminanthscm_positive)))))) /\ (((exists ff_h_mdm_mdr_rank_existszeroevaluationdeterminanthscm_positive_target. ff_h_mdm_mdr_rank_existszeroevaluationdeterminanthscm_positive_target + S (ff_value_mdm_prefix_mdr_rank_existszeroevaluationdeterminanthscm_positive) = S ((S (ff_index_mdm_prefix_mdr_rank_existszeroevaluationdeterminanthscm_positive)) * mdr_us_rank_existszeroevaluationdeterminanthsc)) /\ exists ff_q_mdm_mdr_rank_existszeroevaluationdeterminanthscm_positive_target. mdr_up_rank_existszeroevaluationdeterminanthsc = ff_q_mdm_mdr_rank_existszeroevaluationdeterminanthscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_rank_existszeroevaluationdeterminanthscm_positive)) * mdr_us_rank_existszeroevaluationdeterminanthsc) + (ff_value_mdm_prefix_mdr_rank_existszeroevaluationdeterminanthscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_rank_existszeroevaluationdeterminanthscm_negative. (exists ff_gap_mdm_lt_mdr_rank_existszeroevaluationdeterminanthscm_negative_index_bound. ff_gap_mdm_lt_mdr_rank_existszeroevaluationdeterminanthscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_rank_existszeroevaluationdeterminanthscm_negative) = ((mdr_q_rank_existszeroevaluationdeterminanths) * (mdr_q_rank_existszeroevaluationdeterminanths))) -> exists ff_row_mdm_prefix_mdr_rank_existszeroevaluationdeterminanthscm_negative ff_column_mdm_prefix_mdr_rank_existszeroevaluationdeterminanthscm_negative ff_value_mdm_prefix_mdr_rank_existszeroevaluationdeterminanthscm_negative. (ff_index_mdm_prefix_mdr_rank_existszeroevaluationdeterminanthscm_negative = (mdr_q_rank_existszeroevaluationdeterminanths) * ff_row_mdm_prefix_mdr_rank_existszeroevaluationdeterminanthscm_negative + ff_column_mdm_prefix_mdr_rank_existszeroevaluationdeterminanthscm_negative /\ ((exists ff_gap_mdm_lt_mdr_rank_existszeroevaluationdeterminanthscm_negative_column_bound. ff_gap_mdm_lt_mdr_rank_existszeroevaluationdeterminanthscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_rank_existszeroevaluationdeterminanthscm_negative) = (mdr_q_rank_existszeroevaluationdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_rank_existszeroevaluationdeterminanthscm_negative_cell ff_column_mdm_cell_mdr_rank_existszeroevaluationdeterminanthscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_rank_existszeroevaluationdeterminanthscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_rank_existszeroevaluationdeterminanthscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_rank_existszeroevaluationdeterminanthscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_rank_existszeroevaluationdeterminanthscm_negative_cell = ff_row_mdm_prefix_mdr_rank_existszeroevaluationdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_rank_existszeroevaluationdeterminanthscm_negative_cell_row_after. ff_gap_mdm_le_mdr_rank_existszeroevaluationdeterminanthscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_rank_existszeroevaluationdeterminanthscm_negative)) /\ ff_row_mdm_cell_mdr_rank_existszeroevaluationdeterminanthscm_negative_cell = S ff_row_mdm_prefix_mdr_rank_existszeroevaluationdeterminanthscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_rank_existszeroevaluationdeterminanthscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_rank_existszeroevaluationdeterminanthscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_rank_existszeroevaluationdeterminanthscm_negative) = (mdr_j_rank_existszeroevaluationdeterminanthsc)) /\ ff_column_mdm_cell_mdr_rank_existszeroevaluationdeterminanthscm_negative_cell = ff_column_mdm_prefix_mdr_rank_existszeroevaluationdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_rank_existszeroevaluationdeterminanthscm_negative_cell_column_after. ff_gap_mdm_le_mdr_rank_existszeroevaluationdeterminanthscm_negative_cell_column_after + (mdr_j_rank_existszeroevaluationdeterminanthsc) = (ff_column_mdm_prefix_mdr_rank_existszeroevaluationdeterminanthscm_negative)) /\ ff_column_mdm_cell_mdr_rank_existszeroevaluationdeterminanthscm_negative_cell = S ff_column_mdm_prefix_mdr_rank_existszeroevaluationdeterminanthscm_negative))) /\ (((exists ff_h_mdm_mdr_rank_existszeroevaluationdeterminanthscm_negative_cell_source. ff_h_mdm_mdr_rank_existszeroevaluationdeterminanthscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_rank_existszeroevaluationdeterminanthscm_negative) = S ((S ((ff_row_mdm_cell_mdr_rank_existszeroevaluationdeterminanthscm_negative_cell) * (S (mdr_q_rank_existszeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_rank_existszeroevaluationdeterminanthscm_negative_cell))) * mdr_nc_rank_existszeroevaluationdeterminanth)) /\ exists ff_q_mdm_mdr_rank_existszeroevaluationdeterminanthscm_negative_cell_source. mdr_nb_rank_existszeroevaluationdeterminanth = ff_q_mdm_mdr_rank_existszeroevaluationdeterminanthscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_rank_existszeroevaluationdeterminanthscm_negative_cell) * (S (mdr_q_rank_existszeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_rank_existszeroevaluationdeterminanthscm_negative_cell))) * mdr_nc_rank_existszeroevaluationdeterminanth) + (ff_value_mdm_prefix_mdr_rank_existszeroevaluationdeterminanthscm_negative)))))) /\ (((exists ff_h_mdm_mdr_rank_existszeroevaluationdeterminanthscm_negative_target. ff_h_mdm_mdr_rank_existszeroevaluationdeterminanthscm_negative_target + S (ff_value_mdm_prefix_mdr_rank_existszeroevaluationdeterminanthscm_negative) = S ((S (ff_index_mdm_prefix_mdr_rank_existszeroevaluationdeterminanthscm_negative)) * mdr_ut_rank_existszeroevaluationdeterminanthsc)) /\ exists ff_q_mdm_mdr_rank_existszeroevaluationdeterminanthscm_negative_target. mdr_un_rank_existszeroevaluationdeterminanthsc = ff_q_mdm_mdr_rank_existszeroevaluationdeterminanthscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_rank_existszeroevaluationdeterminanthscm_negative)) * mdr_ut_rank_existszeroevaluationdeterminanthsc) + (ff_value_mdm_prefix_mdr_rank_existszeroevaluationdeterminanthscm_negative))))))))) /\ ((((exists ff_h_mdr_rank_existszeroevaluationdeterminanthscp. ff_h_mdr_rank_existszeroevaluationdeterminanthscp + S (mdr_p_rank_existszeroevaluationdeterminanthsc) = S ((S (mdr_j_rank_existszeroevaluationdeterminanthsc)) * mdr_ec_rank_existszeroevaluationdeterminanths)) /\ exists ff_q_mdr_rank_existszeroevaluationdeterminanthscp. mdr_eb_rank_existszeroevaluationdeterminanths = ff_q_mdr_rank_existszeroevaluationdeterminanthscp * S ((S (mdr_j_rank_existszeroevaluationdeterminanthsc)) * mdr_ec_rank_existszeroevaluationdeterminanths) + (mdr_p_rank_existszeroevaluationdeterminanthsc))) /\ (((exists ff_h_mdr_rank_existszeroevaluationdeterminanthscn. ff_h_mdr_rank_existszeroevaluationdeterminanthscn + S (mdr_n_rank_existszeroevaluationdeterminanthsc) = S ((S (mdr_j_rank_existszeroevaluationdeterminanthsc)) * mdr_fc_rank_existszeroevaluationdeterminanths)) /\ exists ff_q_mdr_rank_existszeroevaluationdeterminanthscn. mdr_fb_rank_existszeroevaluationdeterminanths = ff_q_mdr_rank_existszeroevaluationdeterminanthscn * S ((S (mdr_j_rank_existszeroevaluationdeterminanthsc)) * mdr_fc_rank_existszeroevaluationdeterminanths) + (mdr_n_rank_existszeroevaluationdeterminanthsc)))))))) /\ (exists ff_ub_mce_fold_mdr_rank_existszeroevaluationdeterminanthsf ff_uc_mce_fold_mdr_rank_existszeroevaluationdeterminanthsf ff_vb_mce_fold_mdr_rank_existszeroevaluationdeterminanthsf ff_vc_mce_fold_mdr_rank_existszeroevaluationdeterminanthsf. ((forall ff_index_mce_alternating_mdr_rank_existszeroevaluationdeterminanthsf_prefix. (exists ff_gap_mce_mdr_rank_existszeroevaluationdeterminanthsf_prefix_index. ff_gap_mce_mdr_rank_existszeroevaluationdeterminanthsf_prefix_index + S (ff_index_mce_alternating_mdr_rank_existszeroevaluationdeterminanthsf_prefix) = (S (mdr_q_rank_existszeroevaluationdeterminanths))) -> exists ff_ap_mce_alternating_mdr_rank_existszeroevaluationdeterminanthsf_prefix ff_an_mce_alternating_mdr_rank_existszeroevaluationdeterminanthsf_prefix ff_bp_mce_alternating_mdr_rank_existszeroevaluationdeterminanthsf_prefix ff_bn_mce_alternating_mdr_rank_existszeroevaluationdeterminanthsf_prefix ff_p_mce_alternating_mdr_rank_existszeroevaluationdeterminanthsf_prefix ff_n_mce_alternating_mdr_rank_existszeroevaluationdeterminanthsf_prefix. ((((exists ff_h_mce_mdr_rank_existszeroevaluationdeterminanthsf_prefix_ap. ff_h_mce_mdr_rank_existszeroevaluationdeterminanthsf_prefix_ap + S (ff_ap_mce_alternating_mdr_rank_existszeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_rank_existszeroevaluationdeterminanthsf_prefix)) * mdr_pc_rank_existszeroevaluationdeterminanth)) /\ exists ff_q_mce_mdr_rank_existszeroevaluationdeterminanthsf_prefix_ap. mdr_pb_rank_existszeroevaluationdeterminanth = ff_q_mce_mdr_rank_existszeroevaluationdeterminanthsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_rank_existszeroevaluationdeterminanthsf_prefix)) * mdr_pc_rank_existszeroevaluationdeterminanth) + (ff_ap_mce_alternating_mdr_rank_existszeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_rank_existszeroevaluationdeterminanthsf_prefix_an. ff_h_mce_mdr_rank_existszeroevaluationdeterminanthsf_prefix_an + S (ff_an_mce_alternating_mdr_rank_existszeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_rank_existszeroevaluationdeterminanthsf_prefix)) * mdr_nc_rank_existszeroevaluationdeterminanth)) /\ exists ff_q_mce_mdr_rank_existszeroevaluationdeterminanthsf_prefix_an. mdr_nb_rank_existszeroevaluationdeterminanth = ff_q_mce_mdr_rank_existszeroevaluationdeterminanthsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_rank_existszeroevaluationdeterminanthsf_prefix)) * mdr_nc_rank_existszeroevaluationdeterminanth) + (ff_an_mce_alternating_mdr_rank_existszeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_rank_existszeroevaluationdeterminanthsf_prefix_bp. ff_h_mce_mdr_rank_existszeroevaluationdeterminanthsf_prefix_bp + S (ff_bp_mce_alternating_mdr_rank_existszeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_rank_existszeroevaluationdeterminanthsf_prefix)) * mdr_ec_rank_existszeroevaluationdeterminanths)) /\ exists ff_q_mce_mdr_rank_existszeroevaluationdeterminanthsf_prefix_bp. mdr_eb_rank_existszeroevaluationdeterminanths = ff_q_mce_mdr_rank_existszeroevaluationdeterminanthsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_rank_existszeroevaluationdeterminanthsf_prefix)) * mdr_ec_rank_existszeroevaluationdeterminanths) + (ff_bp_mce_alternating_mdr_rank_existszeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_rank_existszeroevaluationdeterminanthsf_prefix_bn. ff_h_mce_mdr_rank_existszeroevaluationdeterminanthsf_prefix_bn + S (ff_bn_mce_alternating_mdr_rank_existszeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_rank_existszeroevaluationdeterminanthsf_prefix)) * mdr_fc_rank_existszeroevaluationdeterminanths)) /\ exists ff_q_mce_mdr_rank_existszeroevaluationdeterminanthsf_prefix_bn. mdr_fb_rank_existszeroevaluationdeterminanths = ff_q_mce_mdr_rank_existszeroevaluationdeterminanthsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_rank_existszeroevaluationdeterminanthsf_prefix)) * mdr_fc_rank_existszeroevaluationdeterminanths) + (ff_bn_mce_alternating_mdr_rank_existszeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_rank_existszeroevaluationdeterminanthsf_prefix_positive. ff_h_mce_mdr_rank_existszeroevaluationdeterminanthsf_prefix_positive + S (ff_p_mce_alternating_mdr_rank_existszeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_rank_existszeroevaluationdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_rank_existszeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_rank_existszeroevaluationdeterminanthsf_prefix_positive. ff_ub_mce_fold_mdr_rank_existszeroevaluationdeterminanthsf = ff_q_mce_mdr_rank_existszeroevaluationdeterminanthsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_rank_existszeroevaluationdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_rank_existszeroevaluationdeterminanthsf) + (ff_p_mce_alternating_mdr_rank_existszeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_rank_existszeroevaluationdeterminanthsf_prefix_negative. ff_h_mce_mdr_rank_existszeroevaluationdeterminanthsf_prefix_negative + S (ff_n_mce_alternating_mdr_rank_existszeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_rank_existszeroevaluationdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_rank_existszeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_rank_existszeroevaluationdeterminanthsf_prefix_negative. ff_vb_mce_fold_mdr_rank_existszeroevaluationdeterminanthsf = ff_q_mce_mdr_rank_existszeroevaluationdeterminanthsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_rank_existszeroevaluationdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_rank_existszeroevaluationdeterminanthsf) + (ff_n_mce_alternating_mdr_rank_existszeroevaluationdeterminanthsf_prefix))) /\ (((exists ff_even_mce_term_mdr_rank_existszeroevaluationdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_rank_existszeroevaluationdeterminanthsf_prefix = 2 * ff_even_mce_term_mdr_rank_existszeroevaluationdeterminanthsf_prefix_term) /\ (ff_p_mce_alternating_mdr_rank_existszeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_rank_existszeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_rank_existszeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_rank_existszeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_rank_existszeroevaluationdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_rank_existszeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_rank_existszeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_rank_existszeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_rank_existszeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_rank_existszeroevaluationdeterminanthsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_rank_existszeroevaluationdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_rank_existszeroevaluationdeterminanthsf_prefix = 2 * ff_odd_mce_term_mdr_rank_existszeroevaluationdeterminanthsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_rank_existszeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_rank_existszeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_rank_existszeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_rank_existszeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_rank_existszeroevaluationdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_rank_existszeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_rank_existszeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_rank_existszeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_rank_existszeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_rank_existszeroevaluationdeterminanthsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_rank_existszeroevaluationdeterminanthsf_positive ff_v_mce_mdr_rank_existszeroevaluationdeterminanthsf_positive. ((((exists ff_h_mce_mdr_rank_existszeroevaluationdeterminanthsf_positive_start. ff_h_mce_mdr_rank_existszeroevaluationdeterminanthsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_rank_existszeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_rank_existszeroevaluationdeterminanthsf_positive_start. ff_u_mce_mdr_rank_existszeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_rank_existszeroevaluationdeterminanthsf_positive_start * S ((S (0)) * ff_v_mce_mdr_rank_existszeroevaluationdeterminanthsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_rank_existszeroevaluationdeterminanthsf_positive_terminal. ff_h_mce_mdr_rank_existszeroevaluationdeterminanthsf_positive_terminal + S (mdr_p_rank_existszeroevaluationdeterminanth) = S ((S ((S (mdr_q_rank_existszeroevaluationdeterminanths)))) * ff_v_mce_mdr_rank_existszeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_rank_existszeroevaluationdeterminanthsf_positive_terminal. ff_u_mce_mdr_rank_existszeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_rank_existszeroevaluationdeterminanthsf_positive_terminal * S ((S ((S (mdr_q_rank_existszeroevaluationdeterminanths)))) * ff_v_mce_mdr_rank_existszeroevaluationdeterminanthsf_positive) + (mdr_p_rank_existszeroevaluationdeterminanth))) /\ forall ff_i_mce_mdr_rank_existszeroevaluationdeterminanthsf_positive. (exists ff_lt_mce_mdr_rank_existszeroevaluationdeterminanthsf_positive_bound. ff_lt_mce_mdr_rank_existszeroevaluationdeterminanthsf_positive_bound + S ff_i_mce_mdr_rank_existszeroevaluationdeterminanthsf_positive = (S (mdr_q_rank_existszeroevaluationdeterminanths))) -> exists ff_a_mce_mdr_rank_existszeroevaluationdeterminanthsf_positive ff_r_mce_mdr_rank_existszeroevaluationdeterminanthsf_positive ff_s_mce_mdr_rank_existszeroevaluationdeterminanthsf_positive. ((((exists ff_h_mce_mdr_rank_existszeroevaluationdeterminanthsf_positive_summand. ff_h_mce_mdr_rank_existszeroevaluationdeterminanthsf_positive_summand + S (ff_a_mce_mdr_rank_existszeroevaluationdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_rank_existszeroevaluationdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_rank_existszeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_rank_existszeroevaluationdeterminanthsf_positive_summand. ff_ub_mce_fold_mdr_rank_existszeroevaluationdeterminanthsf = ff_q_mce_mdr_rank_existszeroevaluationdeterminanthsf_positive_summand * S ((S (ff_i_mce_mdr_rank_existszeroevaluationdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_rank_existszeroevaluationdeterminanthsf) + (ff_a_mce_mdr_rank_existszeroevaluationdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_rank_existszeroevaluationdeterminanthsf_positive_partial. ff_h_mce_mdr_rank_existszeroevaluationdeterminanthsf_positive_partial + S (ff_r_mce_mdr_rank_existszeroevaluationdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_rank_existszeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_rank_existszeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_rank_existszeroevaluationdeterminanthsf_positive_partial. ff_u_mce_mdr_rank_existszeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_rank_existszeroevaluationdeterminanthsf_positive_partial * S ((S (ff_i_mce_mdr_rank_existszeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_rank_existszeroevaluationdeterminanthsf_positive) + (ff_r_mce_mdr_rank_existszeroevaluationdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_rank_existszeroevaluationdeterminanthsf_positive_successor. ff_h_mce_mdr_rank_existszeroevaluationdeterminanthsf_positive_successor + S (ff_s_mce_mdr_rank_existszeroevaluationdeterminanthsf_positive) = S ((S (S ff_i_mce_mdr_rank_existszeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_rank_existszeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_rank_existszeroevaluationdeterminanthsf_positive_successor. ff_u_mce_mdr_rank_existszeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_rank_existszeroevaluationdeterminanthsf_positive_successor * S ((S (S ff_i_mce_mdr_rank_existszeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_rank_existszeroevaluationdeterminanthsf_positive) + (ff_s_mce_mdr_rank_existszeroevaluationdeterminanthsf_positive))) /\ ff_s_mce_mdr_rank_existszeroevaluationdeterminanthsf_positive = ff_r_mce_mdr_rank_existszeroevaluationdeterminanthsf_positive + ff_a_mce_mdr_rank_existszeroevaluationdeterminanthsf_positive)))))) /\ (exists ff_u_mce_mdr_rank_existszeroevaluationdeterminanthsf_negative ff_v_mce_mdr_rank_existszeroevaluationdeterminanthsf_negative. ((((exists ff_h_mce_mdr_rank_existszeroevaluationdeterminanthsf_negative_start. ff_h_mce_mdr_rank_existszeroevaluationdeterminanthsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_rank_existszeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_rank_existszeroevaluationdeterminanthsf_negative_start. ff_u_mce_mdr_rank_existszeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_rank_existszeroevaluationdeterminanthsf_negative_start * S ((S (0)) * ff_v_mce_mdr_rank_existszeroevaluationdeterminanthsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_rank_existszeroevaluationdeterminanthsf_negative_terminal. ff_h_mce_mdr_rank_existszeroevaluationdeterminanthsf_negative_terminal + S (mdr_n_rank_existszeroevaluationdeterminanth) = S ((S ((S (mdr_q_rank_existszeroevaluationdeterminanths)))) * ff_v_mce_mdr_rank_existszeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_rank_existszeroevaluationdeterminanthsf_negative_terminal. ff_u_mce_mdr_rank_existszeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_rank_existszeroevaluationdeterminanthsf_negative_terminal * S ((S ((S (mdr_q_rank_existszeroevaluationdeterminanths)))) * ff_v_mce_mdr_rank_existszeroevaluationdeterminanthsf_negative) + (mdr_n_rank_existszeroevaluationdeterminanth))) /\ forall ff_i_mce_mdr_rank_existszeroevaluationdeterminanthsf_negative. (exists ff_lt_mce_mdr_rank_existszeroevaluationdeterminanthsf_negative_bound. ff_lt_mce_mdr_rank_existszeroevaluationdeterminanthsf_negative_bound + S ff_i_mce_mdr_rank_existszeroevaluationdeterminanthsf_negative = (S (mdr_q_rank_existszeroevaluationdeterminanths))) -> exists ff_a_mce_mdr_rank_existszeroevaluationdeterminanthsf_negative ff_r_mce_mdr_rank_existszeroevaluationdeterminanthsf_negative ff_s_mce_mdr_rank_existszeroevaluationdeterminanthsf_negative. ((((exists ff_h_mce_mdr_rank_existszeroevaluationdeterminanthsf_negative_summand. ff_h_mce_mdr_rank_existszeroevaluationdeterminanthsf_negative_summand + S (ff_a_mce_mdr_rank_existszeroevaluationdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_rank_existszeroevaluationdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_rank_existszeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_rank_existszeroevaluationdeterminanthsf_negative_summand. ff_vb_mce_fold_mdr_rank_existszeroevaluationdeterminanthsf = ff_q_mce_mdr_rank_existszeroevaluationdeterminanthsf_negative_summand * S ((S (ff_i_mce_mdr_rank_existszeroevaluationdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_rank_existszeroevaluationdeterminanthsf) + (ff_a_mce_mdr_rank_existszeroevaluationdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_rank_existszeroevaluationdeterminanthsf_negative_partial. ff_h_mce_mdr_rank_existszeroevaluationdeterminanthsf_negative_partial + S (ff_r_mce_mdr_rank_existszeroevaluationdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_rank_existszeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_rank_existszeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_rank_existszeroevaluationdeterminanthsf_negative_partial. ff_u_mce_mdr_rank_existszeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_rank_existszeroevaluationdeterminanthsf_negative_partial * S ((S (ff_i_mce_mdr_rank_existszeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_rank_existszeroevaluationdeterminanthsf_negative) + (ff_r_mce_mdr_rank_existszeroevaluationdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_rank_existszeroevaluationdeterminanthsf_negative_successor. ff_h_mce_mdr_rank_existszeroevaluationdeterminanthsf_negative_successor + S (ff_s_mce_mdr_rank_existszeroevaluationdeterminanthsf_negative) = S ((S (S ff_i_mce_mdr_rank_existszeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_rank_existszeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_rank_existszeroevaluationdeterminanthsf_negative_successor. ff_u_mce_mdr_rank_existszeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_rank_existszeroevaluationdeterminanthsf_negative_successor * S ((S (S ff_i_mce_mdr_rank_existszeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_rank_existszeroevaluationdeterminanthsf_negative) + (ff_s_mce_mdr_rank_existszeroevaluationdeterminanthsf_negative))) /\ ff_s_mce_mdr_rank_existszeroevaluationdeterminanthsf_negative = ff_r_mce_mdr_rank_existszeroevaluationdeterminanthsf_negative + ff_a_mce_mdr_rank_existszeroevaluationdeterminanthsf_negative))))))))))))))) /\ ((exists mdr_gap_rank_existszeroevaluationdeterminanti. mdr_gap_rank_existszeroevaluationdeterminanti + S (mdr_i_rank_existszeroevaluationdeterminant) = (mdr_l_rank_existszeroevaluationdeterminant)) /\ (exists mdr_z_rank_existszeroevaluationdeterminantr. ((exists mdr_a_rank_existszeroevaluationdeterminantrc mdr_b_rank_existszeroevaluationdeterminantrc mdr_c_rank_existszeroevaluationdeterminantrc mdr_e_rank_existszeroevaluationdeterminantrc mdr_f_rank_existszeroevaluationdeterminantrc. ((mdr_a_rank_existszeroevaluationdeterminantrc = ((mdr_q_rank_exists) + (mdr_ub_rank_existszeroevaluation)) * S ((mdr_q_rank_exists) + (mdr_ub_rank_existszeroevaluation)) + ((mdr_ub_rank_existszeroevaluation) + (mdr_ub_rank_existszeroevaluation))) /\ ((mdr_b_rank_existszeroevaluationdeterminantrc = ((mdr_uc_rank_existszeroevaluation) + (mdr_vb_rank_existszeroevaluation)) * S ((mdr_uc_rank_existszeroevaluation) + (mdr_vb_rank_existszeroevaluation)) + ((mdr_vb_rank_existszeroevaluation) + (mdr_vb_rank_existszeroevaluation))) /\ ((mdr_c_rank_existszeroevaluationdeterminantrc = ((mdr_a_rank_existszeroevaluationdeterminantrc) + (mdr_b_rank_existszeroevaluationdeterminantrc)) * S ((mdr_a_rank_existszeroevaluationdeterminantrc) + (mdr_b_rank_existszeroevaluationdeterminantrc)) + ((mdr_b_rank_existszeroevaluationdeterminantrc) + (mdr_b_rank_existszeroevaluationdeterminantrc))) /\ ((mdr_e_rank_existszeroevaluationdeterminantrc = ((mdr_p_rank_existszero) + (mdr_n_rank_existszero)) * S ((mdr_p_rank_existszero) + (mdr_n_rank_existszero)) + ((mdr_n_rank_existszero) + (mdr_n_rank_existszero))) /\ ((mdr_f_rank_existszeroevaluationdeterminantrc = ((mdr_vc_rank_existszeroevaluation) + (mdr_e_rank_existszeroevaluationdeterminantrc)) * S ((mdr_vc_rank_existszeroevaluation) + (mdr_e_rank_existszeroevaluationdeterminantrc)) + ((mdr_e_rank_existszeroevaluationdeterminantrc) + (mdr_e_rank_existszeroevaluationdeterminantrc))) /\ ((mdr_z_rank_existszeroevaluationdeterminantr) = ((mdr_c_rank_existszeroevaluationdeterminantrc) + (mdr_f_rank_existszeroevaluationdeterminantrc)) * S ((mdr_c_rank_existszeroevaluationdeterminantrc) + (mdr_f_rank_existszeroevaluationdeterminantrc)) + ((mdr_f_rank_existszeroevaluationdeterminantrc) + (mdr_f_rank_existszeroevaluationdeterminantrc))))))))) /\ (((exists ff_h_mdr_rank_existszeroevaluationdeterminantrb. ff_h_mdr_rank_existszeroevaluationdeterminantrb + S (mdr_z_rank_existszeroevaluationdeterminantr) = S ((S (mdr_i_rank_existszeroevaluationdeterminant)) * mdr_c_rank_existszeroevaluationdeterminant)) /\ exists ff_q_mdr_rank_existszeroevaluationdeterminantrb. mdr_b_rank_existszeroevaluationdeterminant = ff_q_mdr_rank_existszeroevaluationdeterminantrb * S ((S (mdr_i_rank_existszeroevaluationdeterminant)) * mdr_c_rank_existszeroevaluationdeterminant) + (mdr_z_rank_existszeroevaluationdeterminantr)))))))))) -> mdr_p_rank_existszero = mdr_n_rank_existszero))))))