matrix_rank_all_minors_zero_from_absence

Exact expanded first-order arithmetic statement

forall pb pc nb nc r w q. ~(exists mdr_rb_absent_minor mdr_rc_absent_minor mdr_cb_absent_minor mdr_cc_absent_minor. (((((forall fom_index_mrf_absent_minorminorrowsbound. (exists fom_gap_mrf_absent_minorminorrowsbound_index_bound. fom_gap_mrf_absent_minorminorrowsbound_index_bound + S (fom_index_mrf_absent_minorminorrowsbound) = q) -> exists fom_value_mrf_absent_minorminorrowsbound. ((((exists fom_beta_height_mrf_absent_minorminorrowsbound_entry. fom_beta_height_mrf_absent_minorminorrowsbound_entry + S (fom_value_mrf_absent_minorminorrowsbound) = S ((S (fom_index_mrf_absent_minorminorrowsbound)) * mdr_rc_absent_minor)) /\ exists fom_beta_quotient_mrf_absent_minorminorrowsbound_entry. mdr_rb_absent_minor = fom_beta_quotient_mrf_absent_minorminorrowsbound_entry * S ((S (fom_index_mrf_absent_minorminorrowsbound)) * mdr_rc_absent_minor) + (fom_value_mrf_absent_minorminorrowsbound))) /\ (exists fom_gap_mrf_absent_minorminorrowsbound_value_bound. fom_gap_mrf_absent_minorminorrowsbound_value_bound + S (fom_value_mrf_absent_minorminorrowsbound) = r))) /\ (forall mdr_i_absent_minorminorrowsdistinct mdr_j_absent_minorminorrowsdistinct mdr_a_absent_minorminorrowsdistinct. (exists mdr_gap_absent_minorminorrowsdistincti. mdr_gap_absent_minorminorrowsdistincti + S (mdr_i_absent_minorminorrowsdistinct) = (q)) -> (exists mdr_gap_absent_minorminorrowsdistinctj. mdr_gap_absent_minorminorrowsdistinctj + S (mdr_j_absent_minorminorrowsdistinct) = (q)) -> (((exists ff_h_mdr_absent_minorminorrowsdistinctfirst. ff_h_mdr_absent_minorminorrowsdistinctfirst + S (mdr_a_absent_minorminorrowsdistinct) = S ((S (mdr_i_absent_minorminorrowsdistinct)) * mdr_rc_absent_minor)) /\ exists ff_q_mdr_absent_minorminorrowsdistinctfirst. mdr_rb_absent_minor = ff_q_mdr_absent_minorminorrowsdistinctfirst * S ((S (mdr_i_absent_minorminorrowsdistinct)) * mdr_rc_absent_minor) + (mdr_a_absent_minorminorrowsdistinct))) -> (((exists ff_h_mdr_absent_minorminorrowsdistinctsecond. ff_h_mdr_absent_minorminorrowsdistinctsecond + S (mdr_a_absent_minorminorrowsdistinct) = S ((S (mdr_j_absent_minorminorrowsdistinct)) * mdr_rc_absent_minor)) /\ exists ff_q_mdr_absent_minorminorrowsdistinctsecond. mdr_rb_absent_minor = ff_q_mdr_absent_minorminorrowsdistinctsecond * S ((S (mdr_j_absent_minorminorrowsdistinct)) * mdr_rc_absent_minor) + (mdr_a_absent_minorminorrowsdistinct))) -> mdr_i_absent_minorminorrowsdistinct = mdr_j_absent_minorminorrowsdistinct))) /\ ((((forall fom_index_mrf_absent_minorminorcolumnsbound. (exists fom_gap_mrf_absent_minorminorcolumnsbound_index_bound. fom_gap_mrf_absent_minorminorcolumnsbound_index_bound + S (fom_index_mrf_absent_minorminorcolumnsbound) = q) -> exists fom_value_mrf_absent_minorminorcolumnsbound. ((((exists fom_beta_height_mrf_absent_minorminorcolumnsbound_entry. fom_beta_height_mrf_absent_minorminorcolumnsbound_entry + S (fom_value_mrf_absent_minorminorcolumnsbound) = S ((S (fom_index_mrf_absent_minorminorcolumnsbound)) * mdr_cc_absent_minor)) /\ exists fom_beta_quotient_mrf_absent_minorminorcolumnsbound_entry. mdr_cb_absent_minor = fom_beta_quotient_mrf_absent_minorminorcolumnsbound_entry * S ((S (fom_index_mrf_absent_minorminorcolumnsbound)) * mdr_cc_absent_minor) + (fom_value_mrf_absent_minorminorcolumnsbound))) /\ (exists fom_gap_mrf_absent_minorminorcolumnsbound_value_bound. fom_gap_mrf_absent_minorminorcolumnsbound_value_bound + S (fom_value_mrf_absent_minorminorcolumnsbound) = w))) /\ (forall mdr_i_absent_minorminorcolumnsdistinct mdr_j_absent_minorminorcolumnsdistinct mdr_a_absent_minorminorcolumnsdistinct. (exists mdr_gap_absent_minorminorcolumnsdistincti. mdr_gap_absent_minorminorcolumnsdistincti + S (mdr_i_absent_minorminorcolumnsdistinct) = (q)) -> (exists mdr_gap_absent_minorminorcolumnsdistinctj. mdr_gap_absent_minorminorcolumnsdistinctj + S (mdr_j_absent_minorminorcolumnsdistinct) = (q)) -> (((exists ff_h_mdr_absent_minorminorcolumnsdistinctfirst. ff_h_mdr_absent_minorminorcolumnsdistinctfirst + S (mdr_a_absent_minorminorcolumnsdistinct) = S ((S (mdr_i_absent_minorminorcolumnsdistinct)) * mdr_cc_absent_minor)) /\ exists ff_q_mdr_absent_minorminorcolumnsdistinctfirst. mdr_cb_absent_minor = ff_q_mdr_absent_minorminorcolumnsdistinctfirst * S ((S (mdr_i_absent_minorminorcolumnsdistinct)) * mdr_cc_absent_minor) + (mdr_a_absent_minorminorcolumnsdistinct))) -> (((exists ff_h_mdr_absent_minorminorcolumnsdistinctsecond. ff_h_mdr_absent_minorminorcolumnsdistinctsecond + S (mdr_a_absent_minorminorcolumnsdistinct) = S ((S (mdr_j_absent_minorminorcolumnsdistinct)) * mdr_cc_absent_minor)) /\ exists ff_q_mdr_absent_minorminorcolumnsdistinctsecond. mdr_cb_absent_minor = ff_q_mdr_absent_minorminorcolumnsdistinctsecond * S ((S (mdr_j_absent_minorminorcolumnsdistinct)) * mdr_cc_absent_minor) + (mdr_a_absent_minorminorcolumnsdistinct))) -> mdr_i_absent_minorminorcolumnsdistinct = mdr_j_absent_minorminorcolumnsdistinct))) /\ (exists mdr_p_absent_minorminornonzero mdr_n_absent_minorminornonzero. ((exists mdr_ub_absent_minorminornonzeroevaluation mdr_uc_absent_minorminornonzeroevaluation mdr_vb_absent_minorminornonzeroevaluation mdr_vc_absent_minorminornonzeroevaluation. ((((forall mdr_i_absent_minorminornonzeroevaluationmatrixpositive. (exists mdr_gap_absent_minorminornonzeroevaluationmatrixpositivebound. mdr_gap_absent_minorminornonzeroevaluationmatrixpositivebound + S (mdr_i_absent_minorminornonzeroevaluationmatrixpositive) = ((q) * (q))) -> exists mdr_a_absent_minorminornonzeroevaluationmatrixpositive. (((exists mdr_r_absent_minorminornonzeroevaluationmatrixpositivepoint mdr_s_absent_minorminornonzeroevaluationmatrixpositivepoint mdr_u_absent_minorminornonzeroevaluationmatrixpositivepoint mdr_v_absent_minorminornonzeroevaluationmatrixpositivepoint. ((mdr_i_absent_minorminornonzeroevaluationmatrixpositive = (q) * mdr_r_absent_minorminornonzeroevaluationmatrixpositivepoint + mdr_s_absent_minorminornonzeroevaluationmatrixpositivepoint) /\ ((exists mdr_gap_absent_minorminornonzeroevaluationmatrixpositivepointcolumn. mdr_gap_absent_minorminornonzeroevaluationmatrixpositivepointcolumn + S (mdr_s_absent_minorminornonzeroevaluationmatrixpositivepoint) = (q)) /\ ((((exists ff_h_mdr_absent_minorminornonzeroevaluationmatrixpositivepointrow_index. ff_h_mdr_absent_minorminornonzeroevaluationmatrixpositivepointrow_index + S (mdr_u_absent_minorminornonzeroevaluationmatrixpositivepoint) = S ((S (mdr_r_absent_minorminornonzeroevaluationmatrixpositivepoint)) * mdr_rc_absent_minor)) /\ exists ff_q_mdr_absent_minorminornonzeroevaluationmatrixpositivepointrow_index. mdr_rb_absent_minor = ff_q_mdr_absent_minorminornonzeroevaluationmatrixpositivepointrow_index * S ((S (mdr_r_absent_minorminornonzeroevaluationmatrixpositivepoint)) * mdr_rc_absent_minor) + (mdr_u_absent_minorminornonzeroevaluationmatrixpositivepoint))) /\ ((((exists ff_h_mdr_absent_minorminornonzeroevaluationmatrixpositivepointcolumn_index. ff_h_mdr_absent_minorminornonzeroevaluationmatrixpositivepointcolumn_index + S (mdr_v_absent_minorminornonzeroevaluationmatrixpositivepoint) = S ((S (mdr_s_absent_minorminornonzeroevaluationmatrixpositivepoint)) * mdr_cc_absent_minor)) /\ exists ff_q_mdr_absent_minorminornonzeroevaluationmatrixpositivepointcolumn_index. mdr_cb_absent_minor = ff_q_mdr_absent_minorminornonzeroevaluationmatrixpositivepointcolumn_index * S ((S (mdr_s_absent_minorminornonzeroevaluationmatrixpositivepoint)) * mdr_cc_absent_minor) + (mdr_v_absent_minorminornonzeroevaluationmatrixpositivepoint))) /\ (((exists ff_h_mdr_absent_minorminornonzeroevaluationmatrixpositivepointsource. ff_h_mdr_absent_minorminornonzeroevaluationmatrixpositivepointsource + S (mdr_a_absent_minorminornonzeroevaluationmatrixpositive) = S ((S ((mdr_u_absent_minorminornonzeroevaluationmatrixpositivepoint) * (w) + (mdr_v_absent_minorminornonzeroevaluationmatrixpositivepoint))) * pc)) /\ exists ff_q_mdr_absent_minorminornonzeroevaluationmatrixpositivepointsource. pb = ff_q_mdr_absent_minorminornonzeroevaluationmatrixpositivepointsource * S ((S ((mdr_u_absent_minorminornonzeroevaluationmatrixpositivepoint) * (w) + (mdr_v_absent_minorminornonzeroevaluationmatrixpositivepoint))) * pc) + (mdr_a_absent_minorminornonzeroevaluationmatrixpositive)))))))) /\ (((exists ff_h_mdr_absent_minorminornonzeroevaluationmatrixpositiveoutput. ff_h_mdr_absent_minorminornonzeroevaluationmatrixpositiveoutput + S (mdr_a_absent_minorminornonzeroevaluationmatrixpositive) = S ((S (mdr_i_absent_minorminornonzeroevaluationmatrixpositive)) * mdr_uc_absent_minorminornonzeroevaluation)) /\ exists ff_q_mdr_absent_minorminornonzeroevaluationmatrixpositiveoutput. mdr_ub_absent_minorminornonzeroevaluation = ff_q_mdr_absent_minorminornonzeroevaluationmatrixpositiveoutput * S ((S (mdr_i_absent_minorminornonzeroevaluationmatrixpositive)) * mdr_uc_absent_minorminornonzeroevaluation) + (mdr_a_absent_minorminornonzeroevaluationmatrixpositive)))))) /\ (forall mdr_i_absent_minorminornonzeroevaluationmatrixnegative. (exists mdr_gap_absent_minorminornonzeroevaluationmatrixnegativebound. mdr_gap_absent_minorminornonzeroevaluationmatrixnegativebound + S (mdr_i_absent_minorminornonzeroevaluationmatrixnegative) = ((q) * (q))) -> exists mdr_a_absent_minorminornonzeroevaluationmatrixnegative. (((exists mdr_r_absent_minorminornonzeroevaluationmatrixnegativepoint mdr_s_absent_minorminornonzeroevaluationmatrixnegativepoint mdr_u_absent_minorminornonzeroevaluationmatrixnegativepoint mdr_v_absent_minorminornonzeroevaluationmatrixnegativepoint. ((mdr_i_absent_minorminornonzeroevaluationmatrixnegative = (q) * mdr_r_absent_minorminornonzeroevaluationmatrixnegativepoint + mdr_s_absent_minorminornonzeroevaluationmatrixnegativepoint) /\ ((exists mdr_gap_absent_minorminornonzeroevaluationmatrixnegativepointcolumn. mdr_gap_absent_minorminornonzeroevaluationmatrixnegativepointcolumn + S (mdr_s_absent_minorminornonzeroevaluationmatrixnegativepoint) = (q)) /\ ((((exists ff_h_mdr_absent_minorminornonzeroevaluationmatrixnegativepointrow_index. ff_h_mdr_absent_minorminornonzeroevaluationmatrixnegativepointrow_index + S (mdr_u_absent_minorminornonzeroevaluationmatrixnegativepoint) = S ((S (mdr_r_absent_minorminornonzeroevaluationmatrixnegativepoint)) * mdr_rc_absent_minor)) /\ exists ff_q_mdr_absent_minorminornonzeroevaluationmatrixnegativepointrow_index. mdr_rb_absent_minor = ff_q_mdr_absent_minorminornonzeroevaluationmatrixnegativepointrow_index * S ((S (mdr_r_absent_minorminornonzeroevaluationmatrixnegativepoint)) * mdr_rc_absent_minor) + (mdr_u_absent_minorminornonzeroevaluationmatrixnegativepoint))) /\ ((((exists ff_h_mdr_absent_minorminornonzeroevaluationmatrixnegativepointcolumn_index. ff_h_mdr_absent_minorminornonzeroevaluationmatrixnegativepointcolumn_index + S (mdr_v_absent_minorminornonzeroevaluationmatrixnegativepoint) = S ((S (mdr_s_absent_minorminornonzeroevaluationmatrixnegativepoint)) * mdr_cc_absent_minor)) /\ exists ff_q_mdr_absent_minorminornonzeroevaluationmatrixnegativepointcolumn_index. mdr_cb_absent_minor = ff_q_mdr_absent_minorminornonzeroevaluationmatrixnegativepointcolumn_index * S ((S (mdr_s_absent_minorminornonzeroevaluationmatrixnegativepoint)) * mdr_cc_absent_minor) + (mdr_v_absent_minorminornonzeroevaluationmatrixnegativepoint))) /\ (((exists ff_h_mdr_absent_minorminornonzeroevaluationmatrixnegativepointsource. ff_h_mdr_absent_minorminornonzeroevaluationmatrixnegativepointsource + S (mdr_a_absent_minorminornonzeroevaluationmatrixnegative) = S ((S ((mdr_u_absent_minorminornonzeroevaluationmatrixnegativepoint) * (w) + (mdr_v_absent_minorminornonzeroevaluationmatrixnegativepoint))) * nc)) /\ exists ff_q_mdr_absent_minorminornonzeroevaluationmatrixnegativepointsource. nb = ff_q_mdr_absent_minorminornonzeroevaluationmatrixnegativepointsource * S ((S ((mdr_u_absent_minorminornonzeroevaluationmatrixnegativepoint) * (w) + (mdr_v_absent_minorminornonzeroevaluationmatrixnegativepoint))) * nc) + (mdr_a_absent_minorminornonzeroevaluationmatrixnegative)))))))) /\ (((exists ff_h_mdr_absent_minorminornonzeroevaluationmatrixnegativeoutput. ff_h_mdr_absent_minorminornonzeroevaluationmatrixnegativeoutput + S (mdr_a_absent_minorminornonzeroevaluationmatrixnegative) = S ((S (mdr_i_absent_minorminornonzeroevaluationmatrixnegative)) * mdr_vc_absent_minorminornonzeroevaluation)) /\ exists ff_q_mdr_absent_minorminornonzeroevaluationmatrixnegativeoutput. mdr_vb_absent_minorminornonzeroevaluation = ff_q_mdr_absent_minorminornonzeroevaluationmatrixnegativeoutput * S ((S (mdr_i_absent_minorminornonzeroevaluationmatrixnegative)) * mdr_vc_absent_minorminornonzeroevaluation) + (mdr_a_absent_minorminornonzeroevaluationmatrixnegative)))))))) /\ (exists mdr_b_absent_minorminornonzeroevaluationdeterminant mdr_c_absent_minorminornonzeroevaluationdeterminant mdr_l_absent_minorminornonzeroevaluationdeterminant mdr_i_absent_minorminornonzeroevaluationdeterminant. ((forall mdr_i_absent_minorminornonzeroevaluationdeterminanth. (exists mdr_gap_absent_minorminornonzeroevaluationdeterminanthi. mdr_gap_absent_minorminornonzeroevaluationdeterminanthi + S (mdr_i_absent_minorminornonzeroevaluationdeterminanth) = (mdr_l_absent_minorminornonzeroevaluationdeterminant)) -> exists mdr_d_absent_minorminornonzeroevaluationdeterminanth mdr_pb_absent_minorminornonzeroevaluationdeterminanth mdr_pc_absent_minorminornonzeroevaluationdeterminanth mdr_nb_absent_minorminornonzeroevaluationdeterminanth mdr_nc_absent_minorminornonzeroevaluationdeterminanth mdr_p_absent_minorminornonzeroevaluationdeterminanth mdr_n_absent_minorminornonzeroevaluationdeterminanth. ((exists mdr_z_absent_minorminornonzeroevaluationdeterminanthr. ((exists mdr_a_absent_minorminornonzeroevaluationdeterminanthrc mdr_b_absent_minorminornonzeroevaluationdeterminanthrc mdr_c_absent_minorminornonzeroevaluationdeterminanthrc mdr_e_absent_minorminornonzeroevaluationdeterminanthrc mdr_f_absent_minorminornonzeroevaluationdeterminanthrc. ((mdr_a_absent_minorminornonzeroevaluationdeterminanthrc = ((mdr_d_absent_minorminornonzeroevaluationdeterminanth) + (mdr_pb_absent_minorminornonzeroevaluationdeterminanth)) * S ((mdr_d_absent_minorminornonzeroevaluationdeterminanth) + (mdr_pb_absent_minorminornonzeroevaluationdeterminanth)) + ((mdr_pb_absent_minorminornonzeroevaluationdeterminanth) + (mdr_pb_absent_minorminornonzeroevaluationdeterminanth))) /\ ((mdr_b_absent_minorminornonzeroevaluationdeterminanthrc = ((mdr_pc_absent_minorminornonzeroevaluationdeterminanth) + (mdr_nb_absent_minorminornonzeroevaluationdeterminanth)) * S ((mdr_pc_absent_minorminornonzeroevaluationdeterminanth) + (mdr_nb_absent_minorminornonzeroevaluationdeterminanth)) + ((mdr_nb_absent_minorminornonzeroevaluationdeterminanth) + (mdr_nb_absent_minorminornonzeroevaluationdeterminanth))) /\ ((mdr_c_absent_minorminornonzeroevaluationdeterminanthrc = ((mdr_a_absent_minorminornonzeroevaluationdeterminanthrc) + (mdr_b_absent_minorminornonzeroevaluationdeterminanthrc)) * S ((mdr_a_absent_minorminornonzeroevaluationdeterminanthrc) + (mdr_b_absent_minorminornonzeroevaluationdeterminanthrc)) + ((mdr_b_absent_minorminornonzeroevaluationdeterminanthrc) + (mdr_b_absent_minorminornonzeroevaluationdeterminanthrc))) /\ ((mdr_e_absent_minorminornonzeroevaluationdeterminanthrc = ((mdr_p_absent_minorminornonzeroevaluationdeterminanth) + (mdr_n_absent_minorminornonzeroevaluationdeterminanth)) * S ((mdr_p_absent_minorminornonzeroevaluationdeterminanth) + (mdr_n_absent_minorminornonzeroevaluationdeterminanth)) + ((mdr_n_absent_minorminornonzeroevaluationdeterminanth) + (mdr_n_absent_minorminornonzeroevaluationdeterminanth))) /\ ((mdr_f_absent_minorminornonzeroevaluationdeterminanthrc = ((mdr_nc_absent_minorminornonzeroevaluationdeterminanth) + (mdr_e_absent_minorminornonzeroevaluationdeterminanthrc)) * S ((mdr_nc_absent_minorminornonzeroevaluationdeterminanth) + (mdr_e_absent_minorminornonzeroevaluationdeterminanthrc)) + ((mdr_e_absent_minorminornonzeroevaluationdeterminanthrc) + (mdr_e_absent_minorminornonzeroevaluationdeterminanthrc))) /\ ((mdr_z_absent_minorminornonzeroevaluationdeterminanthr) = ((mdr_c_absent_minorminornonzeroevaluationdeterminanthrc) + (mdr_f_absent_minorminornonzeroevaluationdeterminanthrc)) * S ((mdr_c_absent_minorminornonzeroevaluationdeterminanthrc) + (mdr_f_absent_minorminornonzeroevaluationdeterminanthrc)) + ((mdr_f_absent_minorminornonzeroevaluationdeterminanthrc) + (mdr_f_absent_minorminornonzeroevaluationdeterminanthrc))))))))) /\ (((exists ff_h_mdr_absent_minorminornonzeroevaluationdeterminanthrb. ff_h_mdr_absent_minorminornonzeroevaluationdeterminanthrb + S (mdr_z_absent_minorminornonzeroevaluationdeterminanthr) = S ((S (mdr_i_absent_minorminornonzeroevaluationdeterminanth)) * mdr_c_absent_minorminornonzeroevaluationdeterminant)) /\ exists ff_q_mdr_absent_minorminornonzeroevaluationdeterminanthrb. mdr_b_absent_minorminornonzeroevaluationdeterminant = ff_q_mdr_absent_minorminornonzeroevaluationdeterminanthrb * S ((S (mdr_i_absent_minorminornonzeroevaluationdeterminanth)) * mdr_c_absent_minorminornonzeroevaluationdeterminant) + (mdr_z_absent_minorminornonzeroevaluationdeterminanthr))))) /\ (((((mdr_d_absent_minorminornonzeroevaluationdeterminanth) = 0) /\ (((mdr_p_absent_minorminornonzeroevaluationdeterminanth) = 1) /\ ((mdr_n_absent_minorminornonzeroevaluationdeterminanth) = 0))) \/ exists mdr_q_absent_minorminornonzeroevaluationdeterminanths mdr_eb_absent_minorminornonzeroevaluationdeterminanths mdr_ec_absent_minorminornonzeroevaluationdeterminanths mdr_fb_absent_minorminornonzeroevaluationdeterminanths mdr_fc_absent_minorminornonzeroevaluationdeterminanths. (((mdr_d_absent_minorminornonzeroevaluationdeterminanth) = S (mdr_q_absent_minorminornonzeroevaluationdeterminanths)) /\ ((forall mdr_j_absent_minorminornonzeroevaluationdeterminanthsc. (exists mdr_gap_absent_minorminornonzeroevaluationdeterminanthscj. mdr_gap_absent_minorminornonzeroevaluationdeterminanthscj + S (mdr_j_absent_minorminornonzeroevaluationdeterminanthsc) = (S (mdr_q_absent_minorminornonzeroevaluationdeterminanths))) -> exists mdr_i_absent_minorminornonzeroevaluationdeterminanthsc mdr_up_absent_minorminornonzeroevaluationdeterminanthsc mdr_us_absent_minorminornonzeroevaluationdeterminanthsc mdr_un_absent_minorminornonzeroevaluationdeterminanthsc mdr_ut_absent_minorminornonzeroevaluationdeterminanthsc mdr_p_absent_minorminornonzeroevaluationdeterminanthsc mdr_n_absent_minorminornonzeroevaluationdeterminanthsc. ((exists mdr_gap_absent_minorminornonzeroevaluationdeterminanthsci. mdr_gap_absent_minorminornonzeroevaluationdeterminanthsci + S (mdr_i_absent_minorminornonzeroevaluationdeterminanthsc) = (mdr_i_absent_minorminornonzeroevaluationdeterminanth)) /\ ((exists mdr_z_absent_minorminornonzeroevaluationdeterminanthscr. ((exists mdr_a_absent_minorminornonzeroevaluationdeterminanthscrc mdr_b_absent_minorminornonzeroevaluationdeterminanthscrc mdr_c_absent_minorminornonzeroevaluationdeterminanthscrc mdr_e_absent_minorminornonzeroevaluationdeterminanthscrc mdr_f_absent_minorminornonzeroevaluationdeterminanthscrc. ((mdr_a_absent_minorminornonzeroevaluationdeterminanthscrc = ((mdr_q_absent_minorminornonzeroevaluationdeterminanths) + (mdr_up_absent_minorminornonzeroevaluationdeterminanthsc)) * S ((mdr_q_absent_minorminornonzeroevaluationdeterminanths) + (mdr_up_absent_minorminornonzeroevaluationdeterminanthsc)) + ((mdr_up_absent_minorminornonzeroevaluationdeterminanthsc) + (mdr_up_absent_minorminornonzeroevaluationdeterminanthsc))) /\ ((mdr_b_absent_minorminornonzeroevaluationdeterminanthscrc = ((mdr_us_absent_minorminornonzeroevaluationdeterminanthsc) + (mdr_un_absent_minorminornonzeroevaluationdeterminanthsc)) * S ((mdr_us_absent_minorminornonzeroevaluationdeterminanthsc) + (mdr_un_absent_minorminornonzeroevaluationdeterminanthsc)) + ((mdr_un_absent_minorminornonzeroevaluationdeterminanthsc) + (mdr_un_absent_minorminornonzeroevaluationdeterminanthsc))) /\ ((mdr_c_absent_minorminornonzeroevaluationdeterminanthscrc = ((mdr_a_absent_minorminornonzeroevaluationdeterminanthscrc) + (mdr_b_absent_minorminornonzeroevaluationdeterminanthscrc)) * S ((mdr_a_absent_minorminornonzeroevaluationdeterminanthscrc) + (mdr_b_absent_minorminornonzeroevaluationdeterminanthscrc)) + ((mdr_b_absent_minorminornonzeroevaluationdeterminanthscrc) + (mdr_b_absent_minorminornonzeroevaluationdeterminanthscrc))) /\ ((mdr_e_absent_minorminornonzeroevaluationdeterminanthscrc = ((mdr_p_absent_minorminornonzeroevaluationdeterminanthsc) + (mdr_n_absent_minorminornonzeroevaluationdeterminanthsc)) * S ((mdr_p_absent_minorminornonzeroevaluationdeterminanthsc) + (mdr_n_absent_minorminornonzeroevaluationdeterminanthsc)) + ((mdr_n_absent_minorminornonzeroevaluationdeterminanthsc) + (mdr_n_absent_minorminornonzeroevaluationdeterminanthsc))) /\ ((mdr_f_absent_minorminornonzeroevaluationdeterminanthscrc = ((mdr_ut_absent_minorminornonzeroevaluationdeterminanthsc) + (mdr_e_absent_minorminornonzeroevaluationdeterminanthscrc)) * S ((mdr_ut_absent_minorminornonzeroevaluationdeterminanthsc) + (mdr_e_absent_minorminornonzeroevaluationdeterminanthscrc)) + ((mdr_e_absent_minorminornonzeroevaluationdeterminanthscrc) + (mdr_e_absent_minorminornonzeroevaluationdeterminanthscrc))) /\ ((mdr_z_absent_minorminornonzeroevaluationdeterminanthscr) = ((mdr_c_absent_minorminornonzeroevaluationdeterminanthscrc) + (mdr_f_absent_minorminornonzeroevaluationdeterminanthscrc)) * S ((mdr_c_absent_minorminornonzeroevaluationdeterminanthscrc) + (mdr_f_absent_minorminornonzeroevaluationdeterminanthscrc)) + ((mdr_f_absent_minorminornonzeroevaluationdeterminanthscrc) + (mdr_f_absent_minorminornonzeroevaluationdeterminanthscrc))))))))) /\ (((exists ff_h_mdr_absent_minorminornonzeroevaluationdeterminanthscrb. ff_h_mdr_absent_minorminornonzeroevaluationdeterminanthscrb + S (mdr_z_absent_minorminornonzeroevaluationdeterminanthscr) = S ((S (mdr_i_absent_minorminornonzeroevaluationdeterminanthsc)) * mdr_c_absent_minorminornonzeroevaluationdeterminant)) /\ exists ff_q_mdr_absent_minorminornonzeroevaluationdeterminanthscrb. mdr_b_absent_minorminornonzeroevaluationdeterminant = ff_q_mdr_absent_minorminornonzeroevaluationdeterminanthscrb * S ((S (mdr_i_absent_minorminornonzeroevaluationdeterminanthsc)) * mdr_c_absent_minorminornonzeroevaluationdeterminant) + (mdr_z_absent_minorminornonzeroevaluationdeterminanthscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_absent_minorminornonzeroevaluationdeterminanthscm_positive. (exists ff_gap_mdm_lt_mdr_absent_minorminornonzeroevaluationdeterminanthscm_positive_index_bound. ff_gap_mdm_lt_mdr_absent_minorminornonzeroevaluationdeterminanthscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_absent_minorminornonzeroevaluationdeterminanthscm_positive) = ((mdr_q_absent_minorminornonzeroevaluationdeterminanths) * (mdr_q_absent_minorminornonzeroevaluationdeterminanths))) -> exists ff_row_mdm_prefix_mdr_absent_minorminornonzeroevaluationdeterminanthscm_positive ff_column_mdm_prefix_mdr_absent_minorminornonzeroevaluationdeterminanthscm_positive ff_value_mdm_prefix_mdr_absent_minorminornonzeroevaluationdeterminanthscm_positive. (ff_index_mdm_prefix_mdr_absent_minorminornonzeroevaluationdeterminanthscm_positive = (mdr_q_absent_minorminornonzeroevaluationdeterminanths) * ff_row_mdm_prefix_mdr_absent_minorminornonzeroevaluationdeterminanthscm_positive + ff_column_mdm_prefix_mdr_absent_minorminornonzeroevaluationdeterminanthscm_positive /\ ((exists ff_gap_mdm_lt_mdr_absent_minorminornonzeroevaluationdeterminanthscm_positive_column_bound. ff_gap_mdm_lt_mdr_absent_minorminornonzeroevaluationdeterminanthscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_absent_minorminornonzeroevaluationdeterminanthscm_positive) = (mdr_q_absent_minorminornonzeroevaluationdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_absent_minorminornonzeroevaluationdeterminanthscm_positive_cell ff_column_mdm_cell_mdr_absent_minorminornonzeroevaluationdeterminanthscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_absent_minorminornonzeroevaluationdeterminanthscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_absent_minorminornonzeroevaluationdeterminanthscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_absent_minorminornonzeroevaluationdeterminanthscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_absent_minorminornonzeroevaluationdeterminanthscm_positive_cell = ff_row_mdm_prefix_mdr_absent_minorminornonzeroevaluationdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_absent_minorminornonzeroevaluationdeterminanthscm_positive_cell_row_after. ff_gap_mdm_le_mdr_absent_minorminornonzeroevaluationdeterminanthscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_absent_minorminornonzeroevaluationdeterminanthscm_positive)) /\ ff_row_mdm_cell_mdr_absent_minorminornonzeroevaluationdeterminanthscm_positive_cell = S ff_row_mdm_prefix_mdr_absent_minorminornonzeroevaluationdeterminanthscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_absent_minorminornonzeroevaluationdeterminanthscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_absent_minorminornonzeroevaluationdeterminanthscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_absent_minorminornonzeroevaluationdeterminanthscm_positive) = (mdr_j_absent_minorminornonzeroevaluationdeterminanthsc)) /\ ff_column_mdm_cell_mdr_absent_minorminornonzeroevaluationdeterminanthscm_positive_cell = ff_column_mdm_prefix_mdr_absent_minorminornonzeroevaluationdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_absent_minorminornonzeroevaluationdeterminanthscm_positive_cell_column_after. ff_gap_mdm_le_mdr_absent_minorminornonzeroevaluationdeterminanthscm_positive_cell_column_after + (mdr_j_absent_minorminornonzeroevaluationdeterminanthsc) = (ff_column_mdm_prefix_mdr_absent_minorminornonzeroevaluationdeterminanthscm_positive)) /\ ff_column_mdm_cell_mdr_absent_minorminornonzeroevaluationdeterminanthscm_positive_cell = S ff_column_mdm_prefix_mdr_absent_minorminornonzeroevaluationdeterminanthscm_positive))) /\ (((exists ff_h_mdm_mdr_absent_minorminornonzeroevaluationdeterminanthscm_positive_cell_source. ff_h_mdm_mdr_absent_minorminornonzeroevaluationdeterminanthscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_absent_minorminornonzeroevaluationdeterminanthscm_positive) = S ((S ((ff_row_mdm_cell_mdr_absent_minorminornonzeroevaluationdeterminanthscm_positive_cell) * (S (mdr_q_absent_minorminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_absent_minorminornonzeroevaluationdeterminanthscm_positive_cell))) * mdr_pc_absent_minorminornonzeroevaluationdeterminanth)) /\ exists ff_q_mdm_mdr_absent_minorminornonzeroevaluationdeterminanthscm_positive_cell_source. mdr_pb_absent_minorminornonzeroevaluationdeterminanth = ff_q_mdm_mdr_absent_minorminornonzeroevaluationdeterminanthscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_absent_minorminornonzeroevaluationdeterminanthscm_positive_cell) * (S (mdr_q_absent_minorminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_absent_minorminornonzeroevaluationdeterminanthscm_positive_cell))) * mdr_pc_absent_minorminornonzeroevaluationdeterminanth) + (ff_value_mdm_prefix_mdr_absent_minorminornonzeroevaluationdeterminanthscm_positive)))))) /\ (((exists ff_h_mdm_mdr_absent_minorminornonzeroevaluationdeterminanthscm_positive_target. ff_h_mdm_mdr_absent_minorminornonzeroevaluationdeterminanthscm_positive_target + S (ff_value_mdm_prefix_mdr_absent_minorminornonzeroevaluationdeterminanthscm_positive) = S ((S (ff_index_mdm_prefix_mdr_absent_minorminornonzeroevaluationdeterminanthscm_positive)) * mdr_us_absent_minorminornonzeroevaluationdeterminanthsc)) /\ exists ff_q_mdm_mdr_absent_minorminornonzeroevaluationdeterminanthscm_positive_target. mdr_up_absent_minorminornonzeroevaluationdeterminanthsc = ff_q_mdm_mdr_absent_minorminornonzeroevaluationdeterminanthscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_absent_minorminornonzeroevaluationdeterminanthscm_positive)) * mdr_us_absent_minorminornonzeroevaluationdeterminanthsc) + (ff_value_mdm_prefix_mdr_absent_minorminornonzeroevaluationdeterminanthscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_absent_minorminornonzeroevaluationdeterminanthscm_negative. (exists ff_gap_mdm_lt_mdr_absent_minorminornonzeroevaluationdeterminanthscm_negative_index_bound. ff_gap_mdm_lt_mdr_absent_minorminornonzeroevaluationdeterminanthscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_absent_minorminornonzeroevaluationdeterminanthscm_negative) = ((mdr_q_absent_minorminornonzeroevaluationdeterminanths) * (mdr_q_absent_minorminornonzeroevaluationdeterminanths))) -> exists ff_row_mdm_prefix_mdr_absent_minorminornonzeroevaluationdeterminanthscm_negative ff_column_mdm_prefix_mdr_absent_minorminornonzeroevaluationdeterminanthscm_negative ff_value_mdm_prefix_mdr_absent_minorminornonzeroevaluationdeterminanthscm_negative. (ff_index_mdm_prefix_mdr_absent_minorminornonzeroevaluationdeterminanthscm_negative = (mdr_q_absent_minorminornonzeroevaluationdeterminanths) * ff_row_mdm_prefix_mdr_absent_minorminornonzeroevaluationdeterminanthscm_negative + ff_column_mdm_prefix_mdr_absent_minorminornonzeroevaluationdeterminanthscm_negative /\ ((exists ff_gap_mdm_lt_mdr_absent_minorminornonzeroevaluationdeterminanthscm_negative_column_bound. ff_gap_mdm_lt_mdr_absent_minorminornonzeroevaluationdeterminanthscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_absent_minorminornonzeroevaluationdeterminanthscm_negative) = (mdr_q_absent_minorminornonzeroevaluationdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_absent_minorminornonzeroevaluationdeterminanthscm_negative_cell ff_column_mdm_cell_mdr_absent_minorminornonzeroevaluationdeterminanthscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_absent_minorminornonzeroevaluationdeterminanthscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_absent_minorminornonzeroevaluationdeterminanthscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_absent_minorminornonzeroevaluationdeterminanthscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_absent_minorminornonzeroevaluationdeterminanthscm_negative_cell = ff_row_mdm_prefix_mdr_absent_minorminornonzeroevaluationdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_absent_minorminornonzeroevaluationdeterminanthscm_negative_cell_row_after. ff_gap_mdm_le_mdr_absent_minorminornonzeroevaluationdeterminanthscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_absent_minorminornonzeroevaluationdeterminanthscm_negative)) /\ ff_row_mdm_cell_mdr_absent_minorminornonzeroevaluationdeterminanthscm_negative_cell = S ff_row_mdm_prefix_mdr_absent_minorminornonzeroevaluationdeterminanthscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_absent_minorminornonzeroevaluationdeterminanthscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_absent_minorminornonzeroevaluationdeterminanthscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_absent_minorminornonzeroevaluationdeterminanthscm_negative) = (mdr_j_absent_minorminornonzeroevaluationdeterminanthsc)) /\ ff_column_mdm_cell_mdr_absent_minorminornonzeroevaluationdeterminanthscm_negative_cell = ff_column_mdm_prefix_mdr_absent_minorminornonzeroevaluationdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_absent_minorminornonzeroevaluationdeterminanthscm_negative_cell_column_after. ff_gap_mdm_le_mdr_absent_minorminornonzeroevaluationdeterminanthscm_negative_cell_column_after + (mdr_j_absent_minorminornonzeroevaluationdeterminanthsc) = (ff_column_mdm_prefix_mdr_absent_minorminornonzeroevaluationdeterminanthscm_negative)) /\ ff_column_mdm_cell_mdr_absent_minorminornonzeroevaluationdeterminanthscm_negative_cell = S ff_column_mdm_prefix_mdr_absent_minorminornonzeroevaluationdeterminanthscm_negative))) /\ (((exists ff_h_mdm_mdr_absent_minorminornonzeroevaluationdeterminanthscm_negative_cell_source. ff_h_mdm_mdr_absent_minorminornonzeroevaluationdeterminanthscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_absent_minorminornonzeroevaluationdeterminanthscm_negative) = S ((S ((ff_row_mdm_cell_mdr_absent_minorminornonzeroevaluationdeterminanthscm_negative_cell) * (S (mdr_q_absent_minorminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_absent_minorminornonzeroevaluationdeterminanthscm_negative_cell))) * mdr_nc_absent_minorminornonzeroevaluationdeterminanth)) /\ exists ff_q_mdm_mdr_absent_minorminornonzeroevaluationdeterminanthscm_negative_cell_source. mdr_nb_absent_minorminornonzeroevaluationdeterminanth = ff_q_mdm_mdr_absent_minorminornonzeroevaluationdeterminanthscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_absent_minorminornonzeroevaluationdeterminanthscm_negative_cell) * (S (mdr_q_absent_minorminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_absent_minorminornonzeroevaluationdeterminanthscm_negative_cell))) * mdr_nc_absent_minorminornonzeroevaluationdeterminanth) + (ff_value_mdm_prefix_mdr_absent_minorminornonzeroevaluationdeterminanthscm_negative)))))) /\ (((exists ff_h_mdm_mdr_absent_minorminornonzeroevaluationdeterminanthscm_negative_target. ff_h_mdm_mdr_absent_minorminornonzeroevaluationdeterminanthscm_negative_target + S (ff_value_mdm_prefix_mdr_absent_minorminornonzeroevaluationdeterminanthscm_negative) = S ((S (ff_index_mdm_prefix_mdr_absent_minorminornonzeroevaluationdeterminanthscm_negative)) * mdr_ut_absent_minorminornonzeroevaluationdeterminanthsc)) /\ exists ff_q_mdm_mdr_absent_minorminornonzeroevaluationdeterminanthscm_negative_target. mdr_un_absent_minorminornonzeroevaluationdeterminanthsc = ff_q_mdm_mdr_absent_minorminornonzeroevaluationdeterminanthscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_absent_minorminornonzeroevaluationdeterminanthscm_negative)) * mdr_ut_absent_minorminornonzeroevaluationdeterminanthsc) + (ff_value_mdm_prefix_mdr_absent_minorminornonzeroevaluationdeterminanthscm_negative))))))))) /\ ((((exists ff_h_mdr_absent_minorminornonzeroevaluationdeterminanthscp. ff_h_mdr_absent_minorminornonzeroevaluationdeterminanthscp + S (mdr_p_absent_minorminornonzeroevaluationdeterminanthsc) = S ((S (mdr_j_absent_minorminornonzeroevaluationdeterminanthsc)) * mdr_ec_absent_minorminornonzeroevaluationdeterminanths)) /\ exists ff_q_mdr_absent_minorminornonzeroevaluationdeterminanthscp. mdr_eb_absent_minorminornonzeroevaluationdeterminanths = ff_q_mdr_absent_minorminornonzeroevaluationdeterminanthscp * S ((S (mdr_j_absent_minorminornonzeroevaluationdeterminanthsc)) * mdr_ec_absent_minorminornonzeroevaluationdeterminanths) + (mdr_p_absent_minorminornonzeroevaluationdeterminanthsc))) /\ (((exists ff_h_mdr_absent_minorminornonzeroevaluationdeterminanthscn. ff_h_mdr_absent_minorminornonzeroevaluationdeterminanthscn + S (mdr_n_absent_minorminornonzeroevaluationdeterminanthsc) = S ((S (mdr_j_absent_minorminornonzeroevaluationdeterminanthsc)) * mdr_fc_absent_minorminornonzeroevaluationdeterminanths)) /\ exists ff_q_mdr_absent_minorminornonzeroevaluationdeterminanthscn. mdr_fb_absent_minorminornonzeroevaluationdeterminanths = ff_q_mdr_absent_minorminornonzeroevaluationdeterminanthscn * S ((S (mdr_j_absent_minorminornonzeroevaluationdeterminanthsc)) * mdr_fc_absent_minorminornonzeroevaluationdeterminanths) + (mdr_n_absent_minorminornonzeroevaluationdeterminanthsc)))))))) /\ (exists ff_ub_mce_fold_mdr_absent_minorminornonzeroevaluationdeterminanthsf ff_uc_mce_fold_mdr_absent_minorminornonzeroevaluationdeterminanthsf ff_vb_mce_fold_mdr_absent_minorminornonzeroevaluationdeterminanthsf ff_vc_mce_fold_mdr_absent_minorminornonzeroevaluationdeterminanthsf. ((forall ff_index_mce_alternating_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix. (exists ff_gap_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix_index. ff_gap_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix_index + S (ff_index_mce_alternating_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix) = (S (mdr_q_absent_minorminornonzeroevaluationdeterminanths))) -> exists ff_ap_mce_alternating_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix ff_an_mce_alternating_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix ff_bp_mce_alternating_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix ff_bn_mce_alternating_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix ff_p_mce_alternating_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix ff_n_mce_alternating_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix. ((((exists ff_h_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix_ap. ff_h_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix_ap + S (ff_ap_mce_alternating_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix)) * mdr_pc_absent_minorminornonzeroevaluationdeterminanth)) /\ exists ff_q_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix_ap. mdr_pb_absent_minorminornonzeroevaluationdeterminanth = ff_q_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix)) * mdr_pc_absent_minorminornonzeroevaluationdeterminanth) + (ff_ap_mce_alternating_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix_an. ff_h_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix_an + S (ff_an_mce_alternating_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix)) * mdr_nc_absent_minorminornonzeroevaluationdeterminanth)) /\ exists ff_q_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix_an. mdr_nb_absent_minorminornonzeroevaluationdeterminanth = ff_q_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix)) * mdr_nc_absent_minorminornonzeroevaluationdeterminanth) + (ff_an_mce_alternating_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix_bp. ff_h_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix_bp + S (ff_bp_mce_alternating_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix)) * mdr_ec_absent_minorminornonzeroevaluationdeterminanths)) /\ exists ff_q_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix_bp. mdr_eb_absent_minorminornonzeroevaluationdeterminanths = ff_q_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix)) * mdr_ec_absent_minorminornonzeroevaluationdeterminanths) + (ff_bp_mce_alternating_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix_bn. ff_h_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix_bn + S (ff_bn_mce_alternating_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix)) * mdr_fc_absent_minorminornonzeroevaluationdeterminanths)) /\ exists ff_q_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix_bn. mdr_fb_absent_minorminornonzeroevaluationdeterminanths = ff_q_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix)) * mdr_fc_absent_minorminornonzeroevaluationdeterminanths) + (ff_bn_mce_alternating_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix_positive. ff_h_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix_positive + S (ff_p_mce_alternating_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_absent_minorminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix_positive. ff_ub_mce_fold_mdr_absent_minorminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_absent_minorminornonzeroevaluationdeterminanthsf) + (ff_p_mce_alternating_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix_negative. ff_h_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix_negative + S (ff_n_mce_alternating_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_absent_minorminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix_negative. ff_vb_mce_fold_mdr_absent_minorminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_absent_minorminornonzeroevaluationdeterminanthsf) + (ff_n_mce_alternating_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix))) /\ (((exists ff_even_mce_term_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix = 2 * ff_even_mce_term_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix_term) /\ (ff_p_mce_alternating_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix = 2 * ff_odd_mce_term_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_positive ff_v_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_positive. ((((exists ff_h_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_positive_start. ff_h_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_positive_start. ff_u_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_positive_start * S ((S (0)) * ff_v_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_positive_terminal. ff_h_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_positive_terminal + S (mdr_p_absent_minorminornonzeroevaluationdeterminanth) = S ((S ((S (mdr_q_absent_minorminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_positive_terminal. ff_u_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_positive_terminal * S ((S ((S (mdr_q_absent_minorminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_positive) + (mdr_p_absent_minorminornonzeroevaluationdeterminanth))) /\ forall ff_i_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_positive. (exists ff_lt_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_positive_bound. ff_lt_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_positive_bound + S ff_i_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_positive = (S (mdr_q_absent_minorminornonzeroevaluationdeterminanths))) -> exists ff_a_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_positive ff_r_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_positive ff_s_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_positive. ((((exists ff_h_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_positive_summand. ff_h_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_positive_summand + S (ff_a_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_absent_minorminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_positive_summand. ff_ub_mce_fold_mdr_absent_minorminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_positive_summand * S ((S (ff_i_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_absent_minorminornonzeroevaluationdeterminanthsf) + (ff_a_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_positive_partial. ff_h_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_positive_partial + S (ff_r_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_positive_partial. ff_u_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_positive_partial * S ((S (ff_i_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_positive) + (ff_r_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_positive_successor. ff_h_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_positive_successor + S (ff_s_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_positive) = S ((S (S ff_i_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_positive_successor. ff_u_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_positive_successor * S ((S (S ff_i_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_positive) + (ff_s_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_positive))) /\ ff_s_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_positive = ff_r_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_positive + ff_a_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_positive)))))) /\ (exists ff_u_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_negative ff_v_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_negative. ((((exists ff_h_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_negative_start. ff_h_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_negative_start. ff_u_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_negative_start * S ((S (0)) * ff_v_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_negative_terminal. ff_h_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_negative_terminal + S (mdr_n_absent_minorminornonzeroevaluationdeterminanth) = S ((S ((S (mdr_q_absent_minorminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_negative_terminal. ff_u_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_negative_terminal * S ((S ((S (mdr_q_absent_minorminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_negative) + (mdr_n_absent_minorminornonzeroevaluationdeterminanth))) /\ forall ff_i_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_negative. (exists ff_lt_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_negative_bound. ff_lt_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_negative_bound + S ff_i_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_negative = (S (mdr_q_absent_minorminornonzeroevaluationdeterminanths))) -> exists ff_a_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_negative ff_r_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_negative ff_s_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_negative. ((((exists ff_h_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_negative_summand. ff_h_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_negative_summand + S (ff_a_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_absent_minorminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_negative_summand. ff_vb_mce_fold_mdr_absent_minorminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_negative_summand * S ((S (ff_i_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_absent_minorminornonzeroevaluationdeterminanthsf) + (ff_a_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_negative_partial. ff_h_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_negative_partial + S (ff_r_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_negative_partial. ff_u_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_negative_partial * S ((S (ff_i_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_negative) + (ff_r_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_negative_successor. ff_h_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_negative_successor + S (ff_s_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_negative) = S ((S (S ff_i_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_negative_successor. ff_u_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_negative_successor * S ((S (S ff_i_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_negative) + (ff_s_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_negative))) /\ ff_s_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_negative = ff_r_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_negative + ff_a_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_negative))))))))))))))) /\ ((exists mdr_gap_absent_minorminornonzeroevaluationdeterminanti. mdr_gap_absent_minorminornonzeroevaluationdeterminanti + S (mdr_i_absent_minorminornonzeroevaluationdeterminant) = (mdr_l_absent_minorminornonzeroevaluationdeterminant)) /\ (exists mdr_z_absent_minorminornonzeroevaluationdeterminantr. ((exists mdr_a_absent_minorminornonzeroevaluationdeterminantrc mdr_b_absent_minorminornonzeroevaluationdeterminantrc mdr_c_absent_minorminornonzeroevaluationdeterminantrc mdr_e_absent_minorminornonzeroevaluationdeterminantrc mdr_f_absent_minorminornonzeroevaluationdeterminantrc. ((mdr_a_absent_minorminornonzeroevaluationdeterminantrc = ((q) + (mdr_ub_absent_minorminornonzeroevaluation)) * S ((q) + (mdr_ub_absent_minorminornonzeroevaluation)) + ((mdr_ub_absent_minorminornonzeroevaluation) + (mdr_ub_absent_minorminornonzeroevaluation))) /\ ((mdr_b_absent_minorminornonzeroevaluationdeterminantrc = ((mdr_uc_absent_minorminornonzeroevaluation) + (mdr_vb_absent_minorminornonzeroevaluation)) * S ((mdr_uc_absent_minorminornonzeroevaluation) + (mdr_vb_absent_minorminornonzeroevaluation)) + ((mdr_vb_absent_minorminornonzeroevaluation) + (mdr_vb_absent_minorminornonzeroevaluation))) /\ ((mdr_c_absent_minorminornonzeroevaluationdeterminantrc = ((mdr_a_absent_minorminornonzeroevaluationdeterminantrc) + (mdr_b_absent_minorminornonzeroevaluationdeterminantrc)) * S ((mdr_a_absent_minorminornonzeroevaluationdeterminantrc) + (mdr_b_absent_minorminornonzeroevaluationdeterminantrc)) + ((mdr_b_absent_minorminornonzeroevaluationdeterminantrc) + (mdr_b_absent_minorminornonzeroevaluationdeterminantrc))) /\ ((mdr_e_absent_minorminornonzeroevaluationdeterminantrc = ((mdr_p_absent_minorminornonzero) + (mdr_n_absent_minorminornonzero)) * S ((mdr_p_absent_minorminornonzero) + (mdr_n_absent_minorminornonzero)) + ((mdr_n_absent_minorminornonzero) + (mdr_n_absent_minorminornonzero))) /\ ((mdr_f_absent_minorminornonzeroevaluationdeterminantrc = ((mdr_vc_absent_minorminornonzeroevaluation) + (mdr_e_absent_minorminornonzeroevaluationdeterminantrc)) * S ((mdr_vc_absent_minorminornonzeroevaluation) + (mdr_e_absent_minorminornonzeroevaluationdeterminantrc)) + ((mdr_e_absent_minorminornonzeroevaluationdeterminantrc) + (mdr_e_absent_minorminornonzeroevaluationdeterminantrc))) /\ ((mdr_z_absent_minorminornonzeroevaluationdeterminantr) = ((mdr_c_absent_minorminornonzeroevaluationdeterminantrc) + (mdr_f_absent_minorminornonzeroevaluationdeterminantrc)) * S ((mdr_c_absent_minorminornonzeroevaluationdeterminantrc) + (mdr_f_absent_minorminornonzeroevaluationdeterminantrc)) + ((mdr_f_absent_minorminornonzeroevaluationdeterminantrc) + (mdr_f_absent_minorminornonzeroevaluationdeterminantrc))))))))) /\ (((exists ff_h_mdr_absent_minorminornonzeroevaluationdeterminantrb. ff_h_mdr_absent_minorminornonzeroevaluationdeterminantrb + S (mdr_z_absent_minorminornonzeroevaluationdeterminantr) = S ((S (mdr_i_absent_minorminornonzeroevaluationdeterminant)) * mdr_c_absent_minorminornonzeroevaluationdeterminant)) /\ exists ff_q_mdr_absent_minorminornonzeroevaluationdeterminantrb. mdr_b_absent_minorminornonzeroevaluationdeterminant = ff_q_mdr_absent_minorminornonzeroevaluationdeterminantrb * S ((S (mdr_i_absent_minorminornonzeroevaluationdeterminant)) * mdr_c_absent_minorminornonzeroevaluationdeterminant) + (mdr_z_absent_minorminornonzeroevaluationdeterminantr)))))))))) /\ (~(mdr_p_absent_minorminornonzero = mdr_n_absent_minorminornonzero)))))))) -> (forall mdr_rb_all_zero mdr_rc_all_zero mdr_cb_all_zero mdr_cc_all_zero mdr_p_all_zero mdr_n_all_zero. (((forall fom_index_mrf_all_zerorowsbound. (exists fom_gap_mrf_all_zerorowsbound_index_bound. fom_gap_mrf_all_zerorowsbound_index_bound + S (fom_index_mrf_all_zerorowsbound) = q) -> exists fom_value_mrf_all_zerorowsbound. ((((exists fom_beta_height_mrf_all_zerorowsbound_entry. fom_beta_height_mrf_all_zerorowsbound_entry + S (fom_value_mrf_all_zerorowsbound) = S ((S (fom_index_mrf_all_zerorowsbound)) * mdr_rc_all_zero)) /\ exists fom_beta_quotient_mrf_all_zerorowsbound_entry. mdr_rb_all_zero = fom_beta_quotient_mrf_all_zerorowsbound_entry * S ((S (fom_index_mrf_all_zerorowsbound)) * mdr_rc_all_zero) + (fom_value_mrf_all_zerorowsbound))) /\ (exists fom_gap_mrf_all_zerorowsbound_value_bound. fom_gap_mrf_all_zerorowsbound_value_bound + S (fom_value_mrf_all_zerorowsbound) = r))) /\ (forall mdr_i_all_zerorowsdistinct mdr_j_all_zerorowsdistinct mdr_a_all_zerorowsdistinct. (exists mdr_gap_all_zerorowsdistincti. mdr_gap_all_zerorowsdistincti + S (mdr_i_all_zerorowsdistinct) = (q)) -> (exists mdr_gap_all_zerorowsdistinctj. mdr_gap_all_zerorowsdistinctj + S (mdr_j_all_zerorowsdistinct) = (q)) -> (((exists ff_h_mdr_all_zerorowsdistinctfirst. ff_h_mdr_all_zerorowsdistinctfirst + S (mdr_a_all_zerorowsdistinct) = S ((S (mdr_i_all_zerorowsdistinct)) * mdr_rc_all_zero)) /\ exists ff_q_mdr_all_zerorowsdistinctfirst. mdr_rb_all_zero = ff_q_mdr_all_zerorowsdistinctfirst * S ((S (mdr_i_all_zerorowsdistinct)) * mdr_rc_all_zero) + (mdr_a_all_zerorowsdistinct))) -> (((exists ff_h_mdr_all_zerorowsdistinctsecond. ff_h_mdr_all_zerorowsdistinctsecond + S (mdr_a_all_zerorowsdistinct) = S ((S (mdr_j_all_zerorowsdistinct)) * mdr_rc_all_zero)) /\ exists ff_q_mdr_all_zerorowsdistinctsecond. mdr_rb_all_zero = ff_q_mdr_all_zerorowsdistinctsecond * S ((S (mdr_j_all_zerorowsdistinct)) * mdr_rc_all_zero) + (mdr_a_all_zerorowsdistinct))) -> mdr_i_all_zerorowsdistinct = mdr_j_all_zerorowsdistinct))) -> (((forall fom_index_mrf_all_zerocolumnsbound. (exists fom_gap_mrf_all_zerocolumnsbound_index_bound. fom_gap_mrf_all_zerocolumnsbound_index_bound + S (fom_index_mrf_all_zerocolumnsbound) = q) -> exists fom_value_mrf_all_zerocolumnsbound. ((((exists fom_beta_height_mrf_all_zerocolumnsbound_entry. fom_beta_height_mrf_all_zerocolumnsbound_entry + S (fom_value_mrf_all_zerocolumnsbound) = S ((S (fom_index_mrf_all_zerocolumnsbound)) * mdr_cc_all_zero)) /\ exists fom_beta_quotient_mrf_all_zerocolumnsbound_entry. mdr_cb_all_zero = fom_beta_quotient_mrf_all_zerocolumnsbound_entry * S ((S (fom_index_mrf_all_zerocolumnsbound)) * mdr_cc_all_zero) + (fom_value_mrf_all_zerocolumnsbound))) /\ (exists fom_gap_mrf_all_zerocolumnsbound_value_bound. fom_gap_mrf_all_zerocolumnsbound_value_bound + S (fom_value_mrf_all_zerocolumnsbound) = w))) /\ (forall mdr_i_all_zerocolumnsdistinct mdr_j_all_zerocolumnsdistinct mdr_a_all_zerocolumnsdistinct. (exists mdr_gap_all_zerocolumnsdistincti. mdr_gap_all_zerocolumnsdistincti + S (mdr_i_all_zerocolumnsdistinct) = (q)) -> (exists mdr_gap_all_zerocolumnsdistinctj. mdr_gap_all_zerocolumnsdistinctj + S (mdr_j_all_zerocolumnsdistinct) = (q)) -> (((exists ff_h_mdr_all_zerocolumnsdistinctfirst. ff_h_mdr_all_zerocolumnsdistinctfirst + S (mdr_a_all_zerocolumnsdistinct) = S ((S (mdr_i_all_zerocolumnsdistinct)) * mdr_cc_all_zero)) /\ exists ff_q_mdr_all_zerocolumnsdistinctfirst. mdr_cb_all_zero = ff_q_mdr_all_zerocolumnsdistinctfirst * S ((S (mdr_i_all_zerocolumnsdistinct)) * mdr_cc_all_zero) + (mdr_a_all_zerocolumnsdistinct))) -> (((exists ff_h_mdr_all_zerocolumnsdistinctsecond. ff_h_mdr_all_zerocolumnsdistinctsecond + S (mdr_a_all_zerocolumnsdistinct) = S ((S (mdr_j_all_zerocolumnsdistinct)) * mdr_cc_all_zero)) /\ exists ff_q_mdr_all_zerocolumnsdistinctsecond. mdr_cb_all_zero = ff_q_mdr_all_zerocolumnsdistinctsecond * S ((S (mdr_j_all_zerocolumnsdistinct)) * mdr_cc_all_zero) + (mdr_a_all_zerocolumnsdistinct))) -> mdr_i_all_zerocolumnsdistinct = mdr_j_all_zerocolumnsdistinct))) -> (exists mdr_ub_all_zeroevaluation mdr_uc_all_zeroevaluation mdr_vb_all_zeroevaluation mdr_vc_all_zeroevaluation. ((((forall mdr_i_all_zeroevaluationmatrixpositive. (exists mdr_gap_all_zeroevaluationmatrixpositivebound. mdr_gap_all_zeroevaluationmatrixpositivebound + S (mdr_i_all_zeroevaluationmatrixpositive) = ((q) * (q))) -> exists mdr_a_all_zeroevaluationmatrixpositive. (((exists mdr_r_all_zeroevaluationmatrixpositivepoint mdr_s_all_zeroevaluationmatrixpositivepoint mdr_u_all_zeroevaluationmatrixpositivepoint mdr_v_all_zeroevaluationmatrixpositivepoint. ((mdr_i_all_zeroevaluationmatrixpositive = (q) * mdr_r_all_zeroevaluationmatrixpositivepoint + mdr_s_all_zeroevaluationmatrixpositivepoint) /\ ((exists mdr_gap_all_zeroevaluationmatrixpositivepointcolumn. mdr_gap_all_zeroevaluationmatrixpositivepointcolumn + S (mdr_s_all_zeroevaluationmatrixpositivepoint) = (q)) /\ ((((exists ff_h_mdr_all_zeroevaluationmatrixpositivepointrow_index. ff_h_mdr_all_zeroevaluationmatrixpositivepointrow_index + S (mdr_u_all_zeroevaluationmatrixpositivepoint) = S ((S (mdr_r_all_zeroevaluationmatrixpositivepoint)) * mdr_rc_all_zero)) /\ exists ff_q_mdr_all_zeroevaluationmatrixpositivepointrow_index. mdr_rb_all_zero = ff_q_mdr_all_zeroevaluationmatrixpositivepointrow_index * S ((S (mdr_r_all_zeroevaluationmatrixpositivepoint)) * mdr_rc_all_zero) + (mdr_u_all_zeroevaluationmatrixpositivepoint))) /\ ((((exists ff_h_mdr_all_zeroevaluationmatrixpositivepointcolumn_index. ff_h_mdr_all_zeroevaluationmatrixpositivepointcolumn_index + S (mdr_v_all_zeroevaluationmatrixpositivepoint) = S ((S (mdr_s_all_zeroevaluationmatrixpositivepoint)) * mdr_cc_all_zero)) /\ exists ff_q_mdr_all_zeroevaluationmatrixpositivepointcolumn_index. mdr_cb_all_zero = ff_q_mdr_all_zeroevaluationmatrixpositivepointcolumn_index * S ((S (mdr_s_all_zeroevaluationmatrixpositivepoint)) * mdr_cc_all_zero) + (mdr_v_all_zeroevaluationmatrixpositivepoint))) /\ (((exists ff_h_mdr_all_zeroevaluationmatrixpositivepointsource. ff_h_mdr_all_zeroevaluationmatrixpositivepointsource + S (mdr_a_all_zeroevaluationmatrixpositive) = S ((S ((mdr_u_all_zeroevaluationmatrixpositivepoint) * (w) + (mdr_v_all_zeroevaluationmatrixpositivepoint))) * pc)) /\ exists ff_q_mdr_all_zeroevaluationmatrixpositivepointsource. pb = ff_q_mdr_all_zeroevaluationmatrixpositivepointsource * S ((S ((mdr_u_all_zeroevaluationmatrixpositivepoint) * (w) + (mdr_v_all_zeroevaluationmatrixpositivepoint))) * pc) + (mdr_a_all_zeroevaluationmatrixpositive)))))))) /\ (((exists ff_h_mdr_all_zeroevaluationmatrixpositiveoutput. ff_h_mdr_all_zeroevaluationmatrixpositiveoutput + S (mdr_a_all_zeroevaluationmatrixpositive) = S ((S (mdr_i_all_zeroevaluationmatrixpositive)) * mdr_uc_all_zeroevaluation)) /\ exists ff_q_mdr_all_zeroevaluationmatrixpositiveoutput. mdr_ub_all_zeroevaluation = ff_q_mdr_all_zeroevaluationmatrixpositiveoutput * S ((S (mdr_i_all_zeroevaluationmatrixpositive)) * mdr_uc_all_zeroevaluation) + (mdr_a_all_zeroevaluationmatrixpositive)))))) /\ (forall mdr_i_all_zeroevaluationmatrixnegative. (exists mdr_gap_all_zeroevaluationmatrixnegativebound. mdr_gap_all_zeroevaluationmatrixnegativebound + S (mdr_i_all_zeroevaluationmatrixnegative) = ((q) * (q))) -> exists mdr_a_all_zeroevaluationmatrixnegative. (((exists mdr_r_all_zeroevaluationmatrixnegativepoint mdr_s_all_zeroevaluationmatrixnegativepoint mdr_u_all_zeroevaluationmatrixnegativepoint mdr_v_all_zeroevaluationmatrixnegativepoint. ((mdr_i_all_zeroevaluationmatrixnegative = (q) * mdr_r_all_zeroevaluationmatrixnegativepoint + mdr_s_all_zeroevaluationmatrixnegativepoint) /\ ((exists mdr_gap_all_zeroevaluationmatrixnegativepointcolumn. mdr_gap_all_zeroevaluationmatrixnegativepointcolumn + S (mdr_s_all_zeroevaluationmatrixnegativepoint) = (q)) /\ ((((exists ff_h_mdr_all_zeroevaluationmatrixnegativepointrow_index. ff_h_mdr_all_zeroevaluationmatrixnegativepointrow_index + S (mdr_u_all_zeroevaluationmatrixnegativepoint) = S ((S (mdr_r_all_zeroevaluationmatrixnegativepoint)) * mdr_rc_all_zero)) /\ exists ff_q_mdr_all_zeroevaluationmatrixnegativepointrow_index. mdr_rb_all_zero = ff_q_mdr_all_zeroevaluationmatrixnegativepointrow_index * S ((S (mdr_r_all_zeroevaluationmatrixnegativepoint)) * mdr_rc_all_zero) + (mdr_u_all_zeroevaluationmatrixnegativepoint))) /\ ((((exists ff_h_mdr_all_zeroevaluationmatrixnegativepointcolumn_index. ff_h_mdr_all_zeroevaluationmatrixnegativepointcolumn_index + S (mdr_v_all_zeroevaluationmatrixnegativepoint) = S ((S (mdr_s_all_zeroevaluationmatrixnegativepoint)) * mdr_cc_all_zero)) /\ exists ff_q_mdr_all_zeroevaluationmatrixnegativepointcolumn_index. mdr_cb_all_zero = ff_q_mdr_all_zeroevaluationmatrixnegativepointcolumn_index * S ((S (mdr_s_all_zeroevaluationmatrixnegativepoint)) * mdr_cc_all_zero) + (mdr_v_all_zeroevaluationmatrixnegativepoint))) /\ (((exists ff_h_mdr_all_zeroevaluationmatrixnegativepointsource. ff_h_mdr_all_zeroevaluationmatrixnegativepointsource + S (mdr_a_all_zeroevaluationmatrixnegative) = S ((S ((mdr_u_all_zeroevaluationmatrixnegativepoint) * (w) + (mdr_v_all_zeroevaluationmatrixnegativepoint))) * nc)) /\ exists ff_q_mdr_all_zeroevaluationmatrixnegativepointsource. nb = ff_q_mdr_all_zeroevaluationmatrixnegativepointsource * S ((S ((mdr_u_all_zeroevaluationmatrixnegativepoint) * (w) + (mdr_v_all_zeroevaluationmatrixnegativepoint))) * nc) + (mdr_a_all_zeroevaluationmatrixnegative)))))))) /\ (((exists ff_h_mdr_all_zeroevaluationmatrixnegativeoutput. ff_h_mdr_all_zeroevaluationmatrixnegativeoutput + S (mdr_a_all_zeroevaluationmatrixnegative) = S ((S (mdr_i_all_zeroevaluationmatrixnegative)) * mdr_vc_all_zeroevaluation)) /\ exists ff_q_mdr_all_zeroevaluationmatrixnegativeoutput. mdr_vb_all_zeroevaluation = ff_q_mdr_all_zeroevaluationmatrixnegativeoutput * S ((S (mdr_i_all_zeroevaluationmatrixnegative)) * mdr_vc_all_zeroevaluation) + (mdr_a_all_zeroevaluationmatrixnegative)))))))) /\ (exists mdr_b_all_zeroevaluationdeterminant mdr_c_all_zeroevaluationdeterminant mdr_l_all_zeroevaluationdeterminant mdr_i_all_zeroevaluationdeterminant. ((forall mdr_i_all_zeroevaluationdeterminanth. (exists mdr_gap_all_zeroevaluationdeterminanthi. mdr_gap_all_zeroevaluationdeterminanthi + S (mdr_i_all_zeroevaluationdeterminanth) = (mdr_l_all_zeroevaluationdeterminant)) -> exists mdr_d_all_zeroevaluationdeterminanth mdr_pb_all_zeroevaluationdeterminanth mdr_pc_all_zeroevaluationdeterminanth mdr_nb_all_zeroevaluationdeterminanth mdr_nc_all_zeroevaluationdeterminanth mdr_p_all_zeroevaluationdeterminanth mdr_n_all_zeroevaluationdeterminanth. ((exists mdr_z_all_zeroevaluationdeterminanthr. ((exists mdr_a_all_zeroevaluationdeterminanthrc mdr_b_all_zeroevaluationdeterminanthrc mdr_c_all_zeroevaluationdeterminanthrc mdr_e_all_zeroevaluationdeterminanthrc mdr_f_all_zeroevaluationdeterminanthrc. ((mdr_a_all_zeroevaluationdeterminanthrc = ((mdr_d_all_zeroevaluationdeterminanth) + (mdr_pb_all_zeroevaluationdeterminanth)) * S ((mdr_d_all_zeroevaluationdeterminanth) + (mdr_pb_all_zeroevaluationdeterminanth)) + ((mdr_pb_all_zeroevaluationdeterminanth) + (mdr_pb_all_zeroevaluationdeterminanth))) /\ ((mdr_b_all_zeroevaluationdeterminanthrc = ((mdr_pc_all_zeroevaluationdeterminanth) + (mdr_nb_all_zeroevaluationdeterminanth)) * S ((mdr_pc_all_zeroevaluationdeterminanth) + (mdr_nb_all_zeroevaluationdeterminanth)) + ((mdr_nb_all_zeroevaluationdeterminanth) + (mdr_nb_all_zeroevaluationdeterminanth))) /\ ((mdr_c_all_zeroevaluationdeterminanthrc = ((mdr_a_all_zeroevaluationdeterminanthrc) + (mdr_b_all_zeroevaluationdeterminanthrc)) * S ((mdr_a_all_zeroevaluationdeterminanthrc) + (mdr_b_all_zeroevaluationdeterminanthrc)) + ((mdr_b_all_zeroevaluationdeterminanthrc) + (mdr_b_all_zeroevaluationdeterminanthrc))) /\ ((mdr_e_all_zeroevaluationdeterminanthrc = ((mdr_p_all_zeroevaluationdeterminanth) + (mdr_n_all_zeroevaluationdeterminanth)) * S ((mdr_p_all_zeroevaluationdeterminanth) + (mdr_n_all_zeroevaluationdeterminanth)) + ((mdr_n_all_zeroevaluationdeterminanth) + (mdr_n_all_zeroevaluationdeterminanth))) /\ ((mdr_f_all_zeroevaluationdeterminanthrc = ((mdr_nc_all_zeroevaluationdeterminanth) + (mdr_e_all_zeroevaluationdeterminanthrc)) * S ((mdr_nc_all_zeroevaluationdeterminanth) + (mdr_e_all_zeroevaluationdeterminanthrc)) + ((mdr_e_all_zeroevaluationdeterminanthrc) + (mdr_e_all_zeroevaluationdeterminanthrc))) /\ ((mdr_z_all_zeroevaluationdeterminanthr) = ((mdr_c_all_zeroevaluationdeterminanthrc) + (mdr_f_all_zeroevaluationdeterminanthrc)) * S ((mdr_c_all_zeroevaluationdeterminanthrc) + (mdr_f_all_zeroevaluationdeterminanthrc)) + ((mdr_f_all_zeroevaluationdeterminanthrc) + (mdr_f_all_zeroevaluationdeterminanthrc))))))))) /\ (((exists ff_h_mdr_all_zeroevaluationdeterminanthrb. ff_h_mdr_all_zeroevaluationdeterminanthrb + S (mdr_z_all_zeroevaluationdeterminanthr) = S ((S (mdr_i_all_zeroevaluationdeterminanth)) * mdr_c_all_zeroevaluationdeterminant)) /\ exists ff_q_mdr_all_zeroevaluationdeterminanthrb. mdr_b_all_zeroevaluationdeterminant = ff_q_mdr_all_zeroevaluationdeterminanthrb * S ((S (mdr_i_all_zeroevaluationdeterminanth)) * mdr_c_all_zeroevaluationdeterminant) + (mdr_z_all_zeroevaluationdeterminanthr))))) /\ (((((mdr_d_all_zeroevaluationdeterminanth) = 0) /\ (((mdr_p_all_zeroevaluationdeterminanth) = 1) /\ ((mdr_n_all_zeroevaluationdeterminanth) = 0))) \/ exists mdr_q_all_zeroevaluationdeterminanths mdr_eb_all_zeroevaluationdeterminanths mdr_ec_all_zeroevaluationdeterminanths mdr_fb_all_zeroevaluationdeterminanths mdr_fc_all_zeroevaluationdeterminanths. (((mdr_d_all_zeroevaluationdeterminanth) = S (mdr_q_all_zeroevaluationdeterminanths)) /\ ((forall mdr_j_all_zeroevaluationdeterminanthsc. (exists mdr_gap_all_zeroevaluationdeterminanthscj. mdr_gap_all_zeroevaluationdeterminanthscj + S (mdr_j_all_zeroevaluationdeterminanthsc) = (S (mdr_q_all_zeroevaluationdeterminanths))) -> exists mdr_i_all_zeroevaluationdeterminanthsc mdr_up_all_zeroevaluationdeterminanthsc mdr_us_all_zeroevaluationdeterminanthsc mdr_un_all_zeroevaluationdeterminanthsc mdr_ut_all_zeroevaluationdeterminanthsc mdr_p_all_zeroevaluationdeterminanthsc mdr_n_all_zeroevaluationdeterminanthsc. ((exists mdr_gap_all_zeroevaluationdeterminanthsci. mdr_gap_all_zeroevaluationdeterminanthsci + S (mdr_i_all_zeroevaluationdeterminanthsc) = (mdr_i_all_zeroevaluationdeterminanth)) /\ ((exists mdr_z_all_zeroevaluationdeterminanthscr. ((exists mdr_a_all_zeroevaluationdeterminanthscrc mdr_b_all_zeroevaluationdeterminanthscrc mdr_c_all_zeroevaluationdeterminanthscrc mdr_e_all_zeroevaluationdeterminanthscrc mdr_f_all_zeroevaluationdeterminanthscrc. ((mdr_a_all_zeroevaluationdeterminanthscrc = ((mdr_q_all_zeroevaluationdeterminanths) + (mdr_up_all_zeroevaluationdeterminanthsc)) * S ((mdr_q_all_zeroevaluationdeterminanths) + (mdr_up_all_zeroevaluationdeterminanthsc)) + ((mdr_up_all_zeroevaluationdeterminanthsc) + (mdr_up_all_zeroevaluationdeterminanthsc))) /\ ((mdr_b_all_zeroevaluationdeterminanthscrc = ((mdr_us_all_zeroevaluationdeterminanthsc) + (mdr_un_all_zeroevaluationdeterminanthsc)) * S ((mdr_us_all_zeroevaluationdeterminanthsc) + (mdr_un_all_zeroevaluationdeterminanthsc)) + ((mdr_un_all_zeroevaluationdeterminanthsc) + (mdr_un_all_zeroevaluationdeterminanthsc))) /\ ((mdr_c_all_zeroevaluationdeterminanthscrc = ((mdr_a_all_zeroevaluationdeterminanthscrc) + (mdr_b_all_zeroevaluationdeterminanthscrc)) * S ((mdr_a_all_zeroevaluationdeterminanthscrc) + (mdr_b_all_zeroevaluationdeterminanthscrc)) + ((mdr_b_all_zeroevaluationdeterminanthscrc) + (mdr_b_all_zeroevaluationdeterminanthscrc))) /\ ((mdr_e_all_zeroevaluationdeterminanthscrc = ((mdr_p_all_zeroevaluationdeterminanthsc) + (mdr_n_all_zeroevaluationdeterminanthsc)) * S ((mdr_p_all_zeroevaluationdeterminanthsc) + (mdr_n_all_zeroevaluationdeterminanthsc)) + ((mdr_n_all_zeroevaluationdeterminanthsc) + (mdr_n_all_zeroevaluationdeterminanthsc))) /\ ((mdr_f_all_zeroevaluationdeterminanthscrc = ((mdr_ut_all_zeroevaluationdeterminanthsc) + (mdr_e_all_zeroevaluationdeterminanthscrc)) * S ((mdr_ut_all_zeroevaluationdeterminanthsc) + (mdr_e_all_zeroevaluationdeterminanthscrc)) + ((mdr_e_all_zeroevaluationdeterminanthscrc) + (mdr_e_all_zeroevaluationdeterminanthscrc))) /\ ((mdr_z_all_zeroevaluationdeterminanthscr) = ((mdr_c_all_zeroevaluationdeterminanthscrc) + (mdr_f_all_zeroevaluationdeterminanthscrc)) * S ((mdr_c_all_zeroevaluationdeterminanthscrc) + (mdr_f_all_zeroevaluationdeterminanthscrc)) + ((mdr_f_all_zeroevaluationdeterminanthscrc) + (mdr_f_all_zeroevaluationdeterminanthscrc))))))))) /\ (((exists ff_h_mdr_all_zeroevaluationdeterminanthscrb. ff_h_mdr_all_zeroevaluationdeterminanthscrb + S (mdr_z_all_zeroevaluationdeterminanthscr) = S ((S (mdr_i_all_zeroevaluationdeterminanthsc)) * mdr_c_all_zeroevaluationdeterminant)) /\ exists ff_q_mdr_all_zeroevaluationdeterminanthscrb. mdr_b_all_zeroevaluationdeterminant = ff_q_mdr_all_zeroevaluationdeterminanthscrb * S ((S (mdr_i_all_zeroevaluationdeterminanthsc)) * mdr_c_all_zeroevaluationdeterminant) + (mdr_z_all_zeroevaluationdeterminanthscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_all_zeroevaluationdeterminanthscm_positive. (exists ff_gap_mdm_lt_mdr_all_zeroevaluationdeterminanthscm_positive_index_bound. ff_gap_mdm_lt_mdr_all_zeroevaluationdeterminanthscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_all_zeroevaluationdeterminanthscm_positive) = ((mdr_q_all_zeroevaluationdeterminanths) * (mdr_q_all_zeroevaluationdeterminanths))) -> exists ff_row_mdm_prefix_mdr_all_zeroevaluationdeterminanthscm_positive ff_column_mdm_prefix_mdr_all_zeroevaluationdeterminanthscm_positive ff_value_mdm_prefix_mdr_all_zeroevaluationdeterminanthscm_positive. (ff_index_mdm_prefix_mdr_all_zeroevaluationdeterminanthscm_positive = (mdr_q_all_zeroevaluationdeterminanths) * ff_row_mdm_prefix_mdr_all_zeroevaluationdeterminanthscm_positive + ff_column_mdm_prefix_mdr_all_zeroevaluationdeterminanthscm_positive /\ ((exists ff_gap_mdm_lt_mdr_all_zeroevaluationdeterminanthscm_positive_column_bound. ff_gap_mdm_lt_mdr_all_zeroevaluationdeterminanthscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_all_zeroevaluationdeterminanthscm_positive) = (mdr_q_all_zeroevaluationdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_all_zeroevaluationdeterminanthscm_positive_cell ff_column_mdm_cell_mdr_all_zeroevaluationdeterminanthscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_all_zeroevaluationdeterminanthscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_all_zeroevaluationdeterminanthscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_all_zeroevaluationdeterminanthscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_all_zeroevaluationdeterminanthscm_positive_cell = ff_row_mdm_prefix_mdr_all_zeroevaluationdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_all_zeroevaluationdeterminanthscm_positive_cell_row_after. ff_gap_mdm_le_mdr_all_zeroevaluationdeterminanthscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_all_zeroevaluationdeterminanthscm_positive)) /\ ff_row_mdm_cell_mdr_all_zeroevaluationdeterminanthscm_positive_cell = S ff_row_mdm_prefix_mdr_all_zeroevaluationdeterminanthscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_all_zeroevaluationdeterminanthscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_all_zeroevaluationdeterminanthscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_all_zeroevaluationdeterminanthscm_positive) = (mdr_j_all_zeroevaluationdeterminanthsc)) /\ ff_column_mdm_cell_mdr_all_zeroevaluationdeterminanthscm_positive_cell = ff_column_mdm_prefix_mdr_all_zeroevaluationdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_all_zeroevaluationdeterminanthscm_positive_cell_column_after. ff_gap_mdm_le_mdr_all_zeroevaluationdeterminanthscm_positive_cell_column_after + (mdr_j_all_zeroevaluationdeterminanthsc) = (ff_column_mdm_prefix_mdr_all_zeroevaluationdeterminanthscm_positive)) /\ ff_column_mdm_cell_mdr_all_zeroevaluationdeterminanthscm_positive_cell = S ff_column_mdm_prefix_mdr_all_zeroevaluationdeterminanthscm_positive))) /\ (((exists ff_h_mdm_mdr_all_zeroevaluationdeterminanthscm_positive_cell_source. ff_h_mdm_mdr_all_zeroevaluationdeterminanthscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_all_zeroevaluationdeterminanthscm_positive) = S ((S ((ff_row_mdm_cell_mdr_all_zeroevaluationdeterminanthscm_positive_cell) * (S (mdr_q_all_zeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_all_zeroevaluationdeterminanthscm_positive_cell))) * mdr_pc_all_zeroevaluationdeterminanth)) /\ exists ff_q_mdm_mdr_all_zeroevaluationdeterminanthscm_positive_cell_source. mdr_pb_all_zeroevaluationdeterminanth = ff_q_mdm_mdr_all_zeroevaluationdeterminanthscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_all_zeroevaluationdeterminanthscm_positive_cell) * (S (mdr_q_all_zeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_all_zeroevaluationdeterminanthscm_positive_cell))) * mdr_pc_all_zeroevaluationdeterminanth) + (ff_value_mdm_prefix_mdr_all_zeroevaluationdeterminanthscm_positive)))))) /\ (((exists ff_h_mdm_mdr_all_zeroevaluationdeterminanthscm_positive_target. ff_h_mdm_mdr_all_zeroevaluationdeterminanthscm_positive_target + S (ff_value_mdm_prefix_mdr_all_zeroevaluationdeterminanthscm_positive) = S ((S (ff_index_mdm_prefix_mdr_all_zeroevaluationdeterminanthscm_positive)) * mdr_us_all_zeroevaluationdeterminanthsc)) /\ exists ff_q_mdm_mdr_all_zeroevaluationdeterminanthscm_positive_target. mdr_up_all_zeroevaluationdeterminanthsc = ff_q_mdm_mdr_all_zeroevaluationdeterminanthscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_all_zeroevaluationdeterminanthscm_positive)) * mdr_us_all_zeroevaluationdeterminanthsc) + (ff_value_mdm_prefix_mdr_all_zeroevaluationdeterminanthscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_all_zeroevaluationdeterminanthscm_negative. (exists ff_gap_mdm_lt_mdr_all_zeroevaluationdeterminanthscm_negative_index_bound. ff_gap_mdm_lt_mdr_all_zeroevaluationdeterminanthscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_all_zeroevaluationdeterminanthscm_negative) = ((mdr_q_all_zeroevaluationdeterminanths) * (mdr_q_all_zeroevaluationdeterminanths))) -> exists ff_row_mdm_prefix_mdr_all_zeroevaluationdeterminanthscm_negative ff_column_mdm_prefix_mdr_all_zeroevaluationdeterminanthscm_negative ff_value_mdm_prefix_mdr_all_zeroevaluationdeterminanthscm_negative. (ff_index_mdm_prefix_mdr_all_zeroevaluationdeterminanthscm_negative = (mdr_q_all_zeroevaluationdeterminanths) * ff_row_mdm_prefix_mdr_all_zeroevaluationdeterminanthscm_negative + ff_column_mdm_prefix_mdr_all_zeroevaluationdeterminanthscm_negative /\ ((exists ff_gap_mdm_lt_mdr_all_zeroevaluationdeterminanthscm_negative_column_bound. ff_gap_mdm_lt_mdr_all_zeroevaluationdeterminanthscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_all_zeroevaluationdeterminanthscm_negative) = (mdr_q_all_zeroevaluationdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_all_zeroevaluationdeterminanthscm_negative_cell ff_column_mdm_cell_mdr_all_zeroevaluationdeterminanthscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_all_zeroevaluationdeterminanthscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_all_zeroevaluationdeterminanthscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_all_zeroevaluationdeterminanthscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_all_zeroevaluationdeterminanthscm_negative_cell = ff_row_mdm_prefix_mdr_all_zeroevaluationdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_all_zeroevaluationdeterminanthscm_negative_cell_row_after. ff_gap_mdm_le_mdr_all_zeroevaluationdeterminanthscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_all_zeroevaluationdeterminanthscm_negative)) /\ ff_row_mdm_cell_mdr_all_zeroevaluationdeterminanthscm_negative_cell = S ff_row_mdm_prefix_mdr_all_zeroevaluationdeterminanthscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_all_zeroevaluationdeterminanthscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_all_zeroevaluationdeterminanthscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_all_zeroevaluationdeterminanthscm_negative) = (mdr_j_all_zeroevaluationdeterminanthsc)) /\ ff_column_mdm_cell_mdr_all_zeroevaluationdeterminanthscm_negative_cell = ff_column_mdm_prefix_mdr_all_zeroevaluationdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_all_zeroevaluationdeterminanthscm_negative_cell_column_after. ff_gap_mdm_le_mdr_all_zeroevaluationdeterminanthscm_negative_cell_column_after + (mdr_j_all_zeroevaluationdeterminanthsc) = (ff_column_mdm_prefix_mdr_all_zeroevaluationdeterminanthscm_negative)) /\ ff_column_mdm_cell_mdr_all_zeroevaluationdeterminanthscm_negative_cell = S ff_column_mdm_prefix_mdr_all_zeroevaluationdeterminanthscm_negative))) /\ (((exists ff_h_mdm_mdr_all_zeroevaluationdeterminanthscm_negative_cell_source. ff_h_mdm_mdr_all_zeroevaluationdeterminanthscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_all_zeroevaluationdeterminanthscm_negative) = S ((S ((ff_row_mdm_cell_mdr_all_zeroevaluationdeterminanthscm_negative_cell) * (S (mdr_q_all_zeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_all_zeroevaluationdeterminanthscm_negative_cell))) * mdr_nc_all_zeroevaluationdeterminanth)) /\ exists ff_q_mdm_mdr_all_zeroevaluationdeterminanthscm_negative_cell_source. mdr_nb_all_zeroevaluationdeterminanth = ff_q_mdm_mdr_all_zeroevaluationdeterminanthscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_all_zeroevaluationdeterminanthscm_negative_cell) * (S (mdr_q_all_zeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_all_zeroevaluationdeterminanthscm_negative_cell))) * mdr_nc_all_zeroevaluationdeterminanth) + (ff_value_mdm_prefix_mdr_all_zeroevaluationdeterminanthscm_negative)))))) /\ (((exists ff_h_mdm_mdr_all_zeroevaluationdeterminanthscm_negative_target. ff_h_mdm_mdr_all_zeroevaluationdeterminanthscm_negative_target + S (ff_value_mdm_prefix_mdr_all_zeroevaluationdeterminanthscm_negative) = S ((S (ff_index_mdm_prefix_mdr_all_zeroevaluationdeterminanthscm_negative)) * mdr_ut_all_zeroevaluationdeterminanthsc)) /\ exists ff_q_mdm_mdr_all_zeroevaluationdeterminanthscm_negative_target. mdr_un_all_zeroevaluationdeterminanthsc = ff_q_mdm_mdr_all_zeroevaluationdeterminanthscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_all_zeroevaluationdeterminanthscm_negative)) * mdr_ut_all_zeroevaluationdeterminanthsc) + (ff_value_mdm_prefix_mdr_all_zeroevaluationdeterminanthscm_negative))))))))) /\ ((((exists ff_h_mdr_all_zeroevaluationdeterminanthscp. ff_h_mdr_all_zeroevaluationdeterminanthscp + S (mdr_p_all_zeroevaluationdeterminanthsc) = S ((S (mdr_j_all_zeroevaluationdeterminanthsc)) * mdr_ec_all_zeroevaluationdeterminanths)) /\ exists ff_q_mdr_all_zeroevaluationdeterminanthscp. mdr_eb_all_zeroevaluationdeterminanths = ff_q_mdr_all_zeroevaluationdeterminanthscp * S ((S (mdr_j_all_zeroevaluationdeterminanthsc)) * mdr_ec_all_zeroevaluationdeterminanths) + (mdr_p_all_zeroevaluationdeterminanthsc))) /\ (((exists ff_h_mdr_all_zeroevaluationdeterminanthscn. ff_h_mdr_all_zeroevaluationdeterminanthscn + S (mdr_n_all_zeroevaluationdeterminanthsc) = S ((S (mdr_j_all_zeroevaluationdeterminanthsc)) * mdr_fc_all_zeroevaluationdeterminanths)) /\ exists ff_q_mdr_all_zeroevaluationdeterminanthscn. mdr_fb_all_zeroevaluationdeterminanths = ff_q_mdr_all_zeroevaluationdeterminanthscn * S ((S (mdr_j_all_zeroevaluationdeterminanthsc)) * mdr_fc_all_zeroevaluationdeterminanths) + (mdr_n_all_zeroevaluationdeterminanthsc)))))))) /\ (exists ff_ub_mce_fold_mdr_all_zeroevaluationdeterminanthsf ff_uc_mce_fold_mdr_all_zeroevaluationdeterminanthsf ff_vb_mce_fold_mdr_all_zeroevaluationdeterminanthsf ff_vc_mce_fold_mdr_all_zeroevaluationdeterminanthsf. ((forall ff_index_mce_alternating_mdr_all_zeroevaluationdeterminanthsf_prefix. (exists ff_gap_mce_mdr_all_zeroevaluationdeterminanthsf_prefix_index. ff_gap_mce_mdr_all_zeroevaluationdeterminanthsf_prefix_index + S (ff_index_mce_alternating_mdr_all_zeroevaluationdeterminanthsf_prefix) = (S (mdr_q_all_zeroevaluationdeterminanths))) -> exists ff_ap_mce_alternating_mdr_all_zeroevaluationdeterminanthsf_prefix ff_an_mce_alternating_mdr_all_zeroevaluationdeterminanthsf_prefix ff_bp_mce_alternating_mdr_all_zeroevaluationdeterminanthsf_prefix ff_bn_mce_alternating_mdr_all_zeroevaluationdeterminanthsf_prefix ff_p_mce_alternating_mdr_all_zeroevaluationdeterminanthsf_prefix ff_n_mce_alternating_mdr_all_zeroevaluationdeterminanthsf_prefix. ((((exists ff_h_mce_mdr_all_zeroevaluationdeterminanthsf_prefix_ap. ff_h_mce_mdr_all_zeroevaluationdeterminanthsf_prefix_ap + S (ff_ap_mce_alternating_mdr_all_zeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_all_zeroevaluationdeterminanthsf_prefix)) * mdr_pc_all_zeroevaluationdeterminanth)) /\ exists ff_q_mce_mdr_all_zeroevaluationdeterminanthsf_prefix_ap. mdr_pb_all_zeroevaluationdeterminanth = ff_q_mce_mdr_all_zeroevaluationdeterminanthsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_all_zeroevaluationdeterminanthsf_prefix)) * mdr_pc_all_zeroevaluationdeterminanth) + (ff_ap_mce_alternating_mdr_all_zeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_all_zeroevaluationdeterminanthsf_prefix_an. ff_h_mce_mdr_all_zeroevaluationdeterminanthsf_prefix_an + S (ff_an_mce_alternating_mdr_all_zeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_all_zeroevaluationdeterminanthsf_prefix)) * mdr_nc_all_zeroevaluationdeterminanth)) /\ exists ff_q_mce_mdr_all_zeroevaluationdeterminanthsf_prefix_an. mdr_nb_all_zeroevaluationdeterminanth = ff_q_mce_mdr_all_zeroevaluationdeterminanthsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_all_zeroevaluationdeterminanthsf_prefix)) * mdr_nc_all_zeroevaluationdeterminanth) + (ff_an_mce_alternating_mdr_all_zeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_all_zeroevaluationdeterminanthsf_prefix_bp. ff_h_mce_mdr_all_zeroevaluationdeterminanthsf_prefix_bp + S (ff_bp_mce_alternating_mdr_all_zeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_all_zeroevaluationdeterminanthsf_prefix)) * mdr_ec_all_zeroevaluationdeterminanths)) /\ exists ff_q_mce_mdr_all_zeroevaluationdeterminanthsf_prefix_bp. mdr_eb_all_zeroevaluationdeterminanths = ff_q_mce_mdr_all_zeroevaluationdeterminanthsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_all_zeroevaluationdeterminanthsf_prefix)) * mdr_ec_all_zeroevaluationdeterminanths) + (ff_bp_mce_alternating_mdr_all_zeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_all_zeroevaluationdeterminanthsf_prefix_bn. ff_h_mce_mdr_all_zeroevaluationdeterminanthsf_prefix_bn + S (ff_bn_mce_alternating_mdr_all_zeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_all_zeroevaluationdeterminanthsf_prefix)) * mdr_fc_all_zeroevaluationdeterminanths)) /\ exists ff_q_mce_mdr_all_zeroevaluationdeterminanthsf_prefix_bn. mdr_fb_all_zeroevaluationdeterminanths = ff_q_mce_mdr_all_zeroevaluationdeterminanthsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_all_zeroevaluationdeterminanthsf_prefix)) * mdr_fc_all_zeroevaluationdeterminanths) + (ff_bn_mce_alternating_mdr_all_zeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_all_zeroevaluationdeterminanthsf_prefix_positive. ff_h_mce_mdr_all_zeroevaluationdeterminanthsf_prefix_positive + S (ff_p_mce_alternating_mdr_all_zeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_all_zeroevaluationdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_all_zeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_all_zeroevaluationdeterminanthsf_prefix_positive. ff_ub_mce_fold_mdr_all_zeroevaluationdeterminanthsf = ff_q_mce_mdr_all_zeroevaluationdeterminanthsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_all_zeroevaluationdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_all_zeroevaluationdeterminanthsf) + (ff_p_mce_alternating_mdr_all_zeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_all_zeroevaluationdeterminanthsf_prefix_negative. ff_h_mce_mdr_all_zeroevaluationdeterminanthsf_prefix_negative + S (ff_n_mce_alternating_mdr_all_zeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_all_zeroevaluationdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_all_zeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_all_zeroevaluationdeterminanthsf_prefix_negative. ff_vb_mce_fold_mdr_all_zeroevaluationdeterminanthsf = ff_q_mce_mdr_all_zeroevaluationdeterminanthsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_all_zeroevaluationdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_all_zeroevaluationdeterminanthsf) + (ff_n_mce_alternating_mdr_all_zeroevaluationdeterminanthsf_prefix))) /\ (((exists ff_even_mce_term_mdr_all_zeroevaluationdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_all_zeroevaluationdeterminanthsf_prefix = 2 * ff_even_mce_term_mdr_all_zeroevaluationdeterminanthsf_prefix_term) /\ (ff_p_mce_alternating_mdr_all_zeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_all_zeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_all_zeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_all_zeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_all_zeroevaluationdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_all_zeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_all_zeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_all_zeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_all_zeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_all_zeroevaluationdeterminanthsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_all_zeroevaluationdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_all_zeroevaluationdeterminanthsf_prefix = 2 * ff_odd_mce_term_mdr_all_zeroevaluationdeterminanthsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_all_zeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_all_zeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_all_zeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_all_zeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_all_zeroevaluationdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_all_zeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_all_zeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_all_zeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_all_zeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_all_zeroevaluationdeterminanthsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_all_zeroevaluationdeterminanthsf_positive ff_v_mce_mdr_all_zeroevaluationdeterminanthsf_positive. ((((exists ff_h_mce_mdr_all_zeroevaluationdeterminanthsf_positive_start. ff_h_mce_mdr_all_zeroevaluationdeterminanthsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_all_zeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_all_zeroevaluationdeterminanthsf_positive_start. ff_u_mce_mdr_all_zeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_all_zeroevaluationdeterminanthsf_positive_start * S ((S (0)) * ff_v_mce_mdr_all_zeroevaluationdeterminanthsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_all_zeroevaluationdeterminanthsf_positive_terminal. ff_h_mce_mdr_all_zeroevaluationdeterminanthsf_positive_terminal + S (mdr_p_all_zeroevaluationdeterminanth) = S ((S ((S (mdr_q_all_zeroevaluationdeterminanths)))) * ff_v_mce_mdr_all_zeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_all_zeroevaluationdeterminanthsf_positive_terminal. ff_u_mce_mdr_all_zeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_all_zeroevaluationdeterminanthsf_positive_terminal * S ((S ((S (mdr_q_all_zeroevaluationdeterminanths)))) * ff_v_mce_mdr_all_zeroevaluationdeterminanthsf_positive) + (mdr_p_all_zeroevaluationdeterminanth))) /\ forall ff_i_mce_mdr_all_zeroevaluationdeterminanthsf_positive. (exists ff_lt_mce_mdr_all_zeroevaluationdeterminanthsf_positive_bound. ff_lt_mce_mdr_all_zeroevaluationdeterminanthsf_positive_bound + S ff_i_mce_mdr_all_zeroevaluationdeterminanthsf_positive = (S (mdr_q_all_zeroevaluationdeterminanths))) -> exists ff_a_mce_mdr_all_zeroevaluationdeterminanthsf_positive ff_r_mce_mdr_all_zeroevaluationdeterminanthsf_positive ff_s_mce_mdr_all_zeroevaluationdeterminanthsf_positive. ((((exists ff_h_mce_mdr_all_zeroevaluationdeterminanthsf_positive_summand. ff_h_mce_mdr_all_zeroevaluationdeterminanthsf_positive_summand + S (ff_a_mce_mdr_all_zeroevaluationdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_all_zeroevaluationdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_all_zeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_all_zeroevaluationdeterminanthsf_positive_summand. ff_ub_mce_fold_mdr_all_zeroevaluationdeterminanthsf = ff_q_mce_mdr_all_zeroevaluationdeterminanthsf_positive_summand * S ((S (ff_i_mce_mdr_all_zeroevaluationdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_all_zeroevaluationdeterminanthsf) + (ff_a_mce_mdr_all_zeroevaluationdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_all_zeroevaluationdeterminanthsf_positive_partial. ff_h_mce_mdr_all_zeroevaluationdeterminanthsf_positive_partial + S (ff_r_mce_mdr_all_zeroevaluationdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_all_zeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_all_zeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_all_zeroevaluationdeterminanthsf_positive_partial. ff_u_mce_mdr_all_zeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_all_zeroevaluationdeterminanthsf_positive_partial * S ((S (ff_i_mce_mdr_all_zeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_all_zeroevaluationdeterminanthsf_positive) + (ff_r_mce_mdr_all_zeroevaluationdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_all_zeroevaluationdeterminanthsf_positive_successor. ff_h_mce_mdr_all_zeroevaluationdeterminanthsf_positive_successor + S (ff_s_mce_mdr_all_zeroevaluationdeterminanthsf_positive) = S ((S (S ff_i_mce_mdr_all_zeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_all_zeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_all_zeroevaluationdeterminanthsf_positive_successor. ff_u_mce_mdr_all_zeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_all_zeroevaluationdeterminanthsf_positive_successor * S ((S (S ff_i_mce_mdr_all_zeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_all_zeroevaluationdeterminanthsf_positive) + (ff_s_mce_mdr_all_zeroevaluationdeterminanthsf_positive))) /\ ff_s_mce_mdr_all_zeroevaluationdeterminanthsf_positive = ff_r_mce_mdr_all_zeroevaluationdeterminanthsf_positive + ff_a_mce_mdr_all_zeroevaluationdeterminanthsf_positive)))))) /\ (exists ff_u_mce_mdr_all_zeroevaluationdeterminanthsf_negative ff_v_mce_mdr_all_zeroevaluationdeterminanthsf_negative. ((((exists ff_h_mce_mdr_all_zeroevaluationdeterminanthsf_negative_start. ff_h_mce_mdr_all_zeroevaluationdeterminanthsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_all_zeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_all_zeroevaluationdeterminanthsf_negative_start. ff_u_mce_mdr_all_zeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_all_zeroevaluationdeterminanthsf_negative_start * S ((S (0)) * ff_v_mce_mdr_all_zeroevaluationdeterminanthsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_all_zeroevaluationdeterminanthsf_negative_terminal. ff_h_mce_mdr_all_zeroevaluationdeterminanthsf_negative_terminal + S (mdr_n_all_zeroevaluationdeterminanth) = S ((S ((S (mdr_q_all_zeroevaluationdeterminanths)))) * ff_v_mce_mdr_all_zeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_all_zeroevaluationdeterminanthsf_negative_terminal. ff_u_mce_mdr_all_zeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_all_zeroevaluationdeterminanthsf_negative_terminal * S ((S ((S (mdr_q_all_zeroevaluationdeterminanths)))) * ff_v_mce_mdr_all_zeroevaluationdeterminanthsf_negative) + (mdr_n_all_zeroevaluationdeterminanth))) /\ forall ff_i_mce_mdr_all_zeroevaluationdeterminanthsf_negative. (exists ff_lt_mce_mdr_all_zeroevaluationdeterminanthsf_negative_bound. ff_lt_mce_mdr_all_zeroevaluationdeterminanthsf_negative_bound + S ff_i_mce_mdr_all_zeroevaluationdeterminanthsf_negative = (S (mdr_q_all_zeroevaluationdeterminanths))) -> exists ff_a_mce_mdr_all_zeroevaluationdeterminanthsf_negative ff_r_mce_mdr_all_zeroevaluationdeterminanthsf_negative ff_s_mce_mdr_all_zeroevaluationdeterminanthsf_negative. ((((exists ff_h_mce_mdr_all_zeroevaluationdeterminanthsf_negative_summand. ff_h_mce_mdr_all_zeroevaluationdeterminanthsf_negative_summand + S (ff_a_mce_mdr_all_zeroevaluationdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_all_zeroevaluationdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_all_zeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_all_zeroevaluationdeterminanthsf_negative_summand. ff_vb_mce_fold_mdr_all_zeroevaluationdeterminanthsf = ff_q_mce_mdr_all_zeroevaluationdeterminanthsf_negative_summand * S ((S (ff_i_mce_mdr_all_zeroevaluationdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_all_zeroevaluationdeterminanthsf) + (ff_a_mce_mdr_all_zeroevaluationdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_all_zeroevaluationdeterminanthsf_negative_partial. ff_h_mce_mdr_all_zeroevaluationdeterminanthsf_negative_partial + S (ff_r_mce_mdr_all_zeroevaluationdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_all_zeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_all_zeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_all_zeroevaluationdeterminanthsf_negative_partial. ff_u_mce_mdr_all_zeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_all_zeroevaluationdeterminanthsf_negative_partial * S ((S (ff_i_mce_mdr_all_zeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_all_zeroevaluationdeterminanthsf_negative) + (ff_r_mce_mdr_all_zeroevaluationdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_all_zeroevaluationdeterminanthsf_negative_successor. ff_h_mce_mdr_all_zeroevaluationdeterminanthsf_negative_successor + S (ff_s_mce_mdr_all_zeroevaluationdeterminanthsf_negative) = S ((S (S ff_i_mce_mdr_all_zeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_all_zeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_all_zeroevaluationdeterminanthsf_negative_successor. ff_u_mce_mdr_all_zeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_all_zeroevaluationdeterminanthsf_negative_successor * S ((S (S ff_i_mce_mdr_all_zeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_all_zeroevaluationdeterminanthsf_negative) + (ff_s_mce_mdr_all_zeroevaluationdeterminanthsf_negative))) /\ ff_s_mce_mdr_all_zeroevaluationdeterminanthsf_negative = ff_r_mce_mdr_all_zeroevaluationdeterminanthsf_negative + ff_a_mce_mdr_all_zeroevaluationdeterminanthsf_negative))))))))))))))) /\ ((exists mdr_gap_all_zeroevaluationdeterminanti. mdr_gap_all_zeroevaluationdeterminanti + S (mdr_i_all_zeroevaluationdeterminant) = (mdr_l_all_zeroevaluationdeterminant)) /\ (exists mdr_z_all_zeroevaluationdeterminantr. ((exists mdr_a_all_zeroevaluationdeterminantrc mdr_b_all_zeroevaluationdeterminantrc mdr_c_all_zeroevaluationdeterminantrc mdr_e_all_zeroevaluationdeterminantrc mdr_f_all_zeroevaluationdeterminantrc. ((mdr_a_all_zeroevaluationdeterminantrc = ((q) + (mdr_ub_all_zeroevaluation)) * S ((q) + (mdr_ub_all_zeroevaluation)) + ((mdr_ub_all_zeroevaluation) + (mdr_ub_all_zeroevaluation))) /\ ((mdr_b_all_zeroevaluationdeterminantrc = ((mdr_uc_all_zeroevaluation) + (mdr_vb_all_zeroevaluation)) * S ((mdr_uc_all_zeroevaluation) + (mdr_vb_all_zeroevaluation)) + ((mdr_vb_all_zeroevaluation) + (mdr_vb_all_zeroevaluation))) /\ ((mdr_c_all_zeroevaluationdeterminantrc = ((mdr_a_all_zeroevaluationdeterminantrc) + (mdr_b_all_zeroevaluationdeterminantrc)) * S ((mdr_a_all_zeroevaluationdeterminantrc) + (mdr_b_all_zeroevaluationdeterminantrc)) + ((mdr_b_all_zeroevaluationdeterminantrc) + (mdr_b_all_zeroevaluationdeterminantrc))) /\ ((mdr_e_all_zeroevaluationdeterminantrc = ((mdr_p_all_zero) + (mdr_n_all_zero)) * S ((mdr_p_all_zero) + (mdr_n_all_zero)) + ((mdr_n_all_zero) + (mdr_n_all_zero))) /\ ((mdr_f_all_zeroevaluationdeterminantrc = ((mdr_vc_all_zeroevaluation) + (mdr_e_all_zeroevaluationdeterminantrc)) * S ((mdr_vc_all_zeroevaluation) + (mdr_e_all_zeroevaluationdeterminantrc)) + ((mdr_e_all_zeroevaluationdeterminantrc) + (mdr_e_all_zeroevaluationdeterminantrc))) /\ ((mdr_z_all_zeroevaluationdeterminantr) = ((mdr_c_all_zeroevaluationdeterminantrc) + (mdr_f_all_zeroevaluationdeterminantrc)) * S ((mdr_c_all_zeroevaluationdeterminantrc) + (mdr_f_all_zeroevaluationdeterminantrc)) + ((mdr_f_all_zeroevaluationdeterminantrc) + (mdr_f_all_zeroevaluationdeterminantrc))))))))) /\ (((exists ff_h_mdr_all_zeroevaluationdeterminantrb. ff_h_mdr_all_zeroevaluationdeterminantrb + S (mdr_z_all_zeroevaluationdeterminantr) = S ((S (mdr_i_all_zeroevaluationdeterminant)) * mdr_c_all_zeroevaluationdeterminant)) /\ exists ff_q_mdr_all_zeroevaluationdeterminantrb. mdr_b_all_zeroevaluationdeterminant = ff_q_mdr_all_zeroevaluationdeterminantrb * S ((S (mdr_i_all_zeroevaluationdeterminant)) * mdr_c_all_zeroevaluationdeterminant) + (mdr_z_all_zeroevaluationdeterminantr)))))))))) -> mdr_p_all_zero = mdr_n_all_zero)