matrix_rank_nonzero_minor_decidable

forall pb pc nb nc r w q. (exists mdr_rb_exists_minor mdr_rc_exists_minor mdr_cb_exists_minor mdr_cc_exists_minor. (((((forall fom_index_mrf_exists_minorminorrowsbound. (exists fom_gap_mrf_exists_minorminorrowsbound_index_bound. fom_gap_mrf_exists_minorminorrowsbound_index_bound + S (fom_index_mrf_exists_minorminorrowsbound) = q) -> exists fom_value_mrf_exists_minorminorrowsbound. ((((exists fom_beta_height_mrf_exists_minorminorrowsbound_entry. fom_beta_height_mrf_exists_minorminorrowsbound_entry + S (fom_value_mrf_exists_minorminorrowsbound) = S ((S (fom_index_mrf_exists_minorminorrowsbound)) * mdr_rc_exists_minor)) /\ exists fom_beta_quotient_mrf_exists_minorminorrowsbound_entry. mdr_rb_exists_minor = fom_beta_quotient_mrf_exists_minorminorrowsbound_entry * S ((S (fom_index_mrf_exists_minorminorrowsbound)) * mdr_rc_exists_minor) + (fom_value_mrf_exists_minorminorrowsbound))) /\ (exists fom_gap_mrf_exists_minorminorrowsbound_value_bound. fom_gap_mrf_exists_minorminorrowsbound_value_bound + S (fom_value_mrf_exists_minorminorrowsbound) = r))) /\ (forall mdr_i_exists_minorminorrowsdistinct mdr_j_exists_minorminorrowsdistinct mdr_a_exists_minorminorrowsdistinct. (exists mdr_gap_exists_minorminorrowsdistincti. mdr_gap_exists_minorminorrowsdistincti + S (mdr_i_exists_minorminorrowsdistinct) = (q)) -> (exists mdr_gap_exists_minorminorrowsdistinctj. mdr_gap_exists_minorminorrowsdistinctj + S (mdr_j_exists_minorminorrowsdistinct) = (q)) -> (((exists ff_h_mdr_exists_minorminorrowsdistinctfirst. ff_h_mdr_exists_minorminorrowsdistinctfirst + S (mdr_a_exists_minorminorrowsdistinct) = S ((S (mdr_i_exists_minorminorrowsdistinct)) * mdr_rc_exists_minor)) /\ exists ff_q_mdr_exists_minorminorrowsdistinctfirst. mdr_rb_exists_minor = ff_q_mdr_exists_minorminorrowsdistinctfirst * S ((S (mdr_i_exists_minorminorrowsdistinct)) * mdr_rc_exists_minor) + (mdr_a_exists_minorminorrowsdistinct))) -> (((exists ff_h_mdr_exists_minorminorrowsdistinctsecond. ff_h_mdr_exists_minorminorrowsdistinctsecond + S (mdr_a_exists_minorminorrowsdistinct) = S ((S (mdr_j_exists_minorminorrowsdistinct)) * mdr_rc_exists_minor)) /\ exists ff_q_mdr_exists_minorminorrowsdistinctsecond. mdr_rb_exists_minor = ff_q_mdr_exists_minorminorrowsdistinctsecond * S ((S (mdr_j_exists_minorminorrowsdistinct)) * mdr_rc_exists_minor) + (mdr_a_exists_minorminorrowsdistinct))) -> mdr_i_exists_minorminorrowsdistinct = mdr_j_exists_minorminorrowsdistinct))) /\ ((((forall fom_index_mrf_exists_minorminorcolumnsbound. (exists fom_gap_mrf_exists_minorminorcolumnsbound_index_bound. fom_gap_mrf_exists_minorminorcolumnsbound_index_bound + S (fom_index_mrf_exists_minorminorcolumnsbound) = q) -> exists fom_value_mrf_exists_minorminorcolumnsbound. ((((exists fom_beta_height_mrf_exists_minorminorcolumnsbound_entry. fom_beta_height_mrf_exists_minorminorcolumnsbound_entry + S (fom_value_mrf_exists_minorminorcolumnsbound) = S ((S (fom_index_mrf_exists_minorminorcolumnsbound)) * mdr_cc_exists_minor)) /\ exists fom_beta_quotient_mrf_exists_minorminorcolumnsbound_entry. mdr_cb_exists_minor = fom_beta_quotient_mrf_exists_minorminorcolumnsbound_entry * S ((S (fom_index_mrf_exists_minorminorcolumnsbound)) * mdr_cc_exists_minor) + (fom_value_mrf_exists_minorminorcolumnsbound))) /\ (exists fom_gap_mrf_exists_minorminorcolumnsbound_value_bound. fom_gap_mrf_exists_minorminorcolumnsbound_value_bound + S (fom_value_mrf_exists_minorminorcolumnsbound) = w))) /\ (forall mdr_i_exists_minorminorcolumnsdistinct mdr_j_exists_minorminorcolumnsdistinct mdr_a_exists_minorminorcolumnsdistinct. (exists mdr_gap_exists_minorminorcolumnsdistincti. mdr_gap_exists_minorminorcolumnsdistincti + S (mdr_i_exists_minorminorcolumnsdistinct) = (q)) -> (exists mdr_gap_exists_minorminorcolumnsdistinctj. mdr_gap_exists_minorminorcolumnsdistinctj + S (mdr_j_exists_minorminorcolumnsdistinct) = (q)) -> (((exists ff_h_mdr_exists_minorminorcolumnsdistinctfirst. ff_h_mdr_exists_minorminorcolumnsdistinctfirst + S (mdr_a_exists_minorminorcolumnsdistinct) = S ((S (mdr_i_exists_minorminorcolumnsdistinct)) * mdr_cc_exists_minor)) /\ exists ff_q_mdr_exists_minorminorcolumnsdistinctfirst. mdr_cb_exists_minor = ff_q_mdr_exists_minorminorcolumnsdistinctfirst * S ((S (mdr_i_exists_minorminorcolumnsdistinct)) * mdr_cc_exists_minor) + (mdr_a_exists_minorminorcolumnsdistinct))) -> (((exists ff_h_mdr_exists_minorminorcolumnsdistinctsecond. ff_h_mdr_exists_minorminorcolumnsdistinctsecond + S (mdr_a_exists_minorminorcolumnsdistinct) = S ((S (mdr_j_exists_minorminorcolumnsdistinct)) * mdr_cc_exists_minor)) /\ exists ff_q_mdr_exists_minorminorcolumnsdistinctsecond. mdr_cb_exists_minor = ff_q_mdr_exists_minorminorcolumnsdistinctsecond * S ((S (mdr_j_exists_minorminorcolumnsdistinct)) * mdr_cc_exists_minor) + (mdr_a_exists_minorminorcolumnsdistinct))) -> mdr_i_exists_minorminorcolumnsdistinct = mdr_j_exists_minorminorcolumnsdistinct))) /\ (exists mdr_p_exists_minorminornonzero mdr_n_exists_minorminornonzero. ((exists mdr_ub_exists_minorminornonzeroevaluation mdr_uc_exists_minorminornonzeroevaluation mdr_vb_exists_minorminornonzeroevaluation mdr_vc_exists_minorminornonzeroevaluation. ((((forall mdr_i_exists_minorminornonzeroevaluationmatrixpositive. (exists mdr_gap_exists_minorminornonzeroevaluationmatrixpositivebound. mdr_gap_exists_minorminornonzeroevaluationmatrixpositivebound + S (mdr_i_exists_minorminornonzeroevaluationmatrixpositive) = ((q) * (q))) -> exists mdr_a_exists_minorminornonzeroevaluationmatrixpositive. (((exists mdr_r_exists_minorminornonzeroevaluationmatrixpositivepoint mdr_s_exists_minorminornonzeroevaluationmatrixpositivepoint mdr_u_exists_minorminornonzeroevaluationmatrixpositivepoint mdr_v_exists_minorminornonzeroevaluationmatrixpositivepoint. ((mdr_i_exists_minorminornonzeroevaluationmatrixpositive = (q) * mdr_r_exists_minorminornonzeroevaluationmatrixpositivepoint + mdr_s_exists_minorminornonzeroevaluationmatrixpositivepoint) /\ ((exists mdr_gap_exists_minorminornonzeroevaluationmatrixpositivepointcolumn. mdr_gap_exists_minorminornonzeroevaluationmatrixpositivepointcolumn + S (mdr_s_exists_minorminornonzeroevaluationmatrixpositivepoint) = (q)) /\ ((((exists ff_h_mdr_exists_minorminornonzeroevaluationmatrixpositivepointrow_index. ff_h_mdr_exists_minorminornonzeroevaluationmatrixpositivepointrow_index + S (mdr_u_exists_minorminornonzeroevaluationmatrixpositivepoint) = S ((S (mdr_r_exists_minorminornonzeroevaluationmatrixpositivepoint)) * mdr_rc_exists_minor)) /\ exists ff_q_mdr_exists_minorminornonzeroevaluationmatrixpositivepointrow_index. mdr_rb_exists_minor = ff_q_mdr_exists_minorminornonzeroevaluationmatrixpositivepointrow_index * S ((S (mdr_r_exists_minorminornonzeroevaluationmatrixpositivepoint)) * mdr_rc_exists_minor) + (mdr_u_exists_minorminornonzeroevaluationmatrixpositivepoint))) /\ ((((exists ff_h_mdr_exists_minorminornonzeroevaluationmatrixpositivepointcolumn_index. ff_h_mdr_exists_minorminornonzeroevaluationmatrixpositivepointcolumn_index + S (mdr_v_exists_minorminornonzeroevaluationmatrixpositivepoint) = S ((S (mdr_s_exists_minorminornonzeroevaluationmatrixpositivepoint)) * mdr_cc_exists_minor)) /\ exists ff_q_mdr_exists_minorminornonzeroevaluationmatrixpositivepointcolumn_index. mdr_cb_exists_minor = ff_q_mdr_exists_minorminornonzeroevaluationmatrixpositivepointcolumn_index * S ((S (mdr_s_exists_minorminornonzeroevaluationmatrixpositivepoint)) * mdr_cc_exists_minor) + (mdr_v_exists_minorminornonzeroevaluationmatrixpositivepoint))) /\ (((exists ff_h_mdr_exists_minorminornonzeroevaluationmatrixpositivepointsource. ff_h_mdr_exists_minorminornonzeroevaluationmatrixpositivepointsource + S (mdr_a_exists_minorminornonzeroevaluationmatrixpositive) = S ((S ((mdr_u_exists_minorminornonzeroevaluationmatrixpositivepoint) * (w) + (mdr_v_exists_minorminornonzeroevaluationmatrixpositivepoint))) * pc)) /\ exists ff_q_mdr_exists_minorminornonzeroevaluationmatrixpositivepointsource. pb = ff_q_mdr_exists_minorminornonzeroevaluationmatrixpositivepointsource * S ((S ((mdr_u_exists_minorminornonzeroevaluationmatrixpositivepoint) * (w) + (mdr_v_exists_minorminornonzeroevaluationmatrixpositivepoint))) * pc) + (mdr_a_exists_minorminornonzeroevaluationmatrixpositive)))))))) /\ (((exists ff_h_mdr_exists_minorminornonzeroevaluationmatrixpositiveoutput. ff_h_mdr_exists_minorminornonzeroevaluationmatrixpositiveoutput + S (mdr_a_exists_minorminornonzeroevaluationmatrixpositive) = S ((S (mdr_i_exists_minorminornonzeroevaluationmatrixpositive)) * mdr_uc_exists_minorminornonzeroevaluation)) /\ exists ff_q_mdr_exists_minorminornonzeroevaluationmatrixpositiveoutput. mdr_ub_exists_minorminornonzeroevaluation = ff_q_mdr_exists_minorminornonzeroevaluationmatrixpositiveoutput * S ((S (mdr_i_exists_minorminornonzeroevaluationmatrixpositive)) * mdr_uc_exists_minorminornonzeroevaluation) + (mdr_a_exists_minorminornonzeroevaluationmatrixpositive)))))) /\ (forall mdr_i_exists_minorminornonzeroevaluationmatrixnegative. (exists mdr_gap_exists_minorminornonzeroevaluationmatrixnegativebound. mdr_gap_exists_minorminornonzeroevaluationmatrixnegativebound + S (mdr_i_exists_minorminornonzeroevaluationmatrixnegative) = ((q) * (q))) -> exists mdr_a_exists_minorminornonzeroevaluationmatrixnegative. (((exists mdr_r_exists_minorminornonzeroevaluationmatrixnegativepoint mdr_s_exists_minorminornonzeroevaluationmatrixnegativepoint mdr_u_exists_minorminornonzeroevaluationmatrixnegativepoint mdr_v_exists_minorminornonzeroevaluationmatrixnegativepoint. ((mdr_i_exists_minorminornonzeroevaluationmatrixnegative = (q) * mdr_r_exists_minorminornonzeroevaluationmatrixnegativepoint + mdr_s_exists_minorminornonzeroevaluationmatrixnegativepoint) /\ ((exists mdr_gap_exists_minorminornonzeroevaluationmatrixnegativepointcolumn. mdr_gap_exists_minorminornonzeroevaluationmatrixnegativepointcolumn + S (mdr_s_exists_minorminornonzeroevaluationmatrixnegativepoint) = (q)) /\ ((((exists ff_h_mdr_exists_minorminornonzeroevaluationmatrixnegativepointrow_index. ff_h_mdr_exists_minorminornonzeroevaluationmatrixnegativepointrow_index + S (mdr_u_exists_minorminornonzeroevaluationmatrixnegativepoint) = S ((S (mdr_r_exists_minorminornonzeroevaluationmatrixnegativepoint)) * mdr_rc_exists_minor)) /\ exists ff_q_mdr_exists_minorminornonzeroevaluationmatrixnegativepointrow_index. mdr_rb_exists_minor = ff_q_mdr_exists_minorminornonzeroevaluationmatrixnegativepointrow_index * S ((S (mdr_r_exists_minorminornonzeroevaluationmatrixnegativepoint)) * mdr_rc_exists_minor) + (mdr_u_exists_minorminornonzeroevaluationmatrixnegativepoint))) /\ ((((exists ff_h_mdr_exists_minorminornonzeroevaluationmatrixnegativepointcolumn_index. ff_h_mdr_exists_minorminornonzeroevaluationmatrixnegativepointcolumn_index + S (mdr_v_exists_minorminornonzeroevaluationmatrixnegativepoint) = S ((S (mdr_s_exists_minorminornonzeroevaluationmatrixnegativepoint)) * mdr_cc_exists_minor)) /\ exists ff_q_mdr_exists_minorminornonzeroevaluationmatrixnegativepointcolumn_index. mdr_cb_exists_minor = ff_q_mdr_exists_minorminornonzeroevaluationmatrixnegativepointcolumn_index * S ((S (mdr_s_exists_minorminornonzeroevaluationmatrixnegativepoint)) * mdr_cc_exists_minor) + (mdr_v_exists_minorminornonzeroevaluationmatrixnegativepoint))) /\ (((exists ff_h_mdr_exists_minorminornonzeroevaluationmatrixnegativepointsource. ff_h_mdr_exists_minorminornonzeroevaluationmatrixnegativepointsource + S (mdr_a_exists_minorminornonzeroevaluationmatrixnegative) = S ((S ((mdr_u_exists_minorminornonzeroevaluationmatrixnegativepoint) * (w) + (mdr_v_exists_minorminornonzeroevaluationmatrixnegativepoint))) * nc)) /\ exists ff_q_mdr_exists_minorminornonzeroevaluationmatrixnegativepointsource. nb = ff_q_mdr_exists_minorminornonzeroevaluationmatrixnegativepointsource * S ((S ((mdr_u_exists_minorminornonzeroevaluationmatrixnegativepoint) * (w) + (mdr_v_exists_minorminornonzeroevaluationmatrixnegativepoint))) * nc) + (mdr_a_exists_minorminornonzeroevaluationmatrixnegative)))))))) /\ (((exists ff_h_mdr_exists_minorminornonzeroevaluationmatrixnegativeoutput. ff_h_mdr_exists_minorminornonzeroevaluationmatrixnegativeoutput + S (mdr_a_exists_minorminornonzeroevaluationmatrixnegative) = S ((S (mdr_i_exists_minorminornonzeroevaluationmatrixnegative)) * mdr_vc_exists_minorminornonzeroevaluation)) /\ exists ff_q_mdr_exists_minorminornonzeroevaluationmatrixnegativeoutput. mdr_vb_exists_minorminornonzeroevaluation = ff_q_mdr_exists_minorminornonzeroevaluationmatrixnegativeoutput * S ((S (mdr_i_exists_minorminornonzeroevaluationmatrixnegative)) * mdr_vc_exists_minorminornonzeroevaluation) + (mdr_a_exists_minorminornonzeroevaluationmatrixnegative)))))))) /\ (exists mdr_b_exists_minorminornonzeroevaluationdeterminant mdr_c_exists_minorminornonzeroevaluationdeterminant mdr_l_exists_minorminornonzeroevaluationdeterminant mdr_i_exists_minorminornonzeroevaluationdeterminant. ((forall mdr_i_exists_minorminornonzeroevaluationdeterminanth. (exists mdr_gap_exists_minorminornonzeroevaluationdeterminanthi. mdr_gap_exists_minorminornonzeroevaluationdeterminanthi + S (mdr_i_exists_minorminornonzeroevaluationdeterminanth) = (mdr_l_exists_minorminornonzeroevaluationdeterminant)) -> exists mdr_d_exists_minorminornonzeroevaluationdeterminanth mdr_pb_exists_minorminornonzeroevaluationdeterminanth mdr_pc_exists_minorminornonzeroevaluationdeterminanth mdr_nb_exists_minorminornonzeroevaluationdeterminanth mdr_nc_exists_minorminornonzeroevaluationdeterminanth mdr_p_exists_minorminornonzeroevaluationdeterminanth mdr_n_exists_minorminornonzeroevaluationdeterminanth. ((exists mdr_z_exists_minorminornonzeroevaluationdeterminanthr. ((exists mdr_a_exists_minorminornonzeroevaluationdeterminanthrc mdr_b_exists_minorminornonzeroevaluationdeterminanthrc mdr_c_exists_minorminornonzeroevaluationdeterminanthrc mdr_e_exists_minorminornonzeroevaluationdeterminanthrc mdr_f_exists_minorminornonzeroevaluationdeterminanthrc. ((mdr_a_exists_minorminornonzeroevaluationdeterminanthrc = ((mdr_d_exists_minorminornonzeroevaluationdeterminanth) + (mdr_pb_exists_minorminornonzeroevaluationdeterminanth)) * S ((mdr_d_exists_minorminornonzeroevaluationdeterminanth) + (mdr_pb_exists_minorminornonzeroevaluationdeterminanth)) + ((mdr_pb_exists_minorminornonzeroevaluationdeterminanth) + (mdr_pb_exists_minorminornonzeroevaluationdeterminanth))) /\ ((mdr_b_exists_minorminornonzeroevaluationdeterminanthrc = ((mdr_pc_exists_minorminornonzeroevaluationdeterminanth) + (mdr_nb_exists_minorminornonzeroevaluationdeterminanth)) * S ((mdr_pc_exists_minorminornonzeroevaluationdeterminanth) + (mdr_nb_exists_minorminornonzeroevaluationdeterminanth)) + ((mdr_nb_exists_minorminornonzeroevaluationdeterminanth) + (mdr_nb_exists_minorminornonzeroevaluationdeterminanth))) /\ ((mdr_c_exists_minorminornonzeroevaluationdeterminanthrc = ((mdr_a_exists_minorminornonzeroevaluationdeterminanthrc) + (mdr_b_exists_minorminornonzeroevaluationdeterminanthrc)) * S ((mdr_a_exists_minorminornonzeroevaluationdeterminanthrc) + (mdr_b_exists_minorminornonzeroevaluationdeterminanthrc)) + ((mdr_b_exists_minorminornonzeroevaluationdeterminanthrc) + (mdr_b_exists_minorminornonzeroevaluationdeterminanthrc))) /\ ((mdr_e_exists_minorminornonzeroevaluationdeterminanthrc = ((mdr_p_exists_minorminornonzeroevaluationdeterminanth) + (mdr_n_exists_minorminornonzeroevaluationdeterminanth)) * S ((mdr_p_exists_minorminornonzeroevaluationdeterminanth) + (mdr_n_exists_minorminornonzeroevaluationdeterminanth)) + ((mdr_n_exists_minorminornonzeroevaluationdeterminanth) + (mdr_n_exists_minorminornonzeroevaluationdeterminanth))) /\ ((mdr_f_exists_minorminornonzeroevaluationdeterminanthrc = ((mdr_nc_exists_minorminornonzeroevaluationdeterminanth) + (mdr_e_exists_minorminornonzeroevaluationdeterminanthrc)) * S ((mdr_nc_exists_minorminornonzeroevaluationdeterminanth) + (mdr_e_exists_minorminornonzeroevaluationdeterminanthrc)) + ((mdr_e_exists_minorminornonzeroevaluationdeterminanthrc) + (mdr_e_exists_minorminornonzeroevaluationdeterminanthrc))) /\ ((mdr_z_exists_minorminornonzeroevaluationdeterminanthr) = ((mdr_c_exists_minorminornonzeroevaluationdeterminanthrc) + (mdr_f_exists_minorminornonzeroevaluationdeterminanthrc)) * S ((mdr_c_exists_minorminornonzeroevaluationdeterminanthrc) + (mdr_f_exists_minorminornonzeroevaluationdeterminanthrc)) + ((mdr_f_exists_minorminornonzeroevaluationdeterminanthrc) + (mdr_f_exists_minorminornonzeroevaluationdeterminanthrc))))))))) /\ (((exists ff_h_mdr_exists_minorminornonzeroevaluationdeterminanthrb. ff_h_mdr_exists_minorminornonzeroevaluationdeterminanthrb + S (mdr_z_exists_minorminornonzeroevaluationdeterminanthr) = S ((S (mdr_i_exists_minorminornonzeroevaluationdeterminanth)) * mdr_c_exists_minorminornonzeroevaluationdeterminant)) /\ exists ff_q_mdr_exists_minorminornonzeroevaluationdeterminanthrb. mdr_b_exists_minorminornonzeroevaluationdeterminant = ff_q_mdr_exists_minorminornonzeroevaluationdeterminanthrb * S ((S (mdr_i_exists_minorminornonzeroevaluationdeterminanth)) * mdr_c_exists_minorminornonzeroevaluationdeterminant) + (mdr_z_exists_minorminornonzeroevaluationdeterminanthr))))) /\ (((((mdr_d_exists_minorminornonzeroevaluationdeterminanth) = 0) /\ (((mdr_p_exists_minorminornonzeroevaluationdeterminanth) = 1) /\ ((mdr_n_exists_minorminornonzeroevaluationdeterminanth) = 0))) \/ exists mdr_q_exists_minorminornonzeroevaluationdeterminanths mdr_eb_exists_minorminornonzeroevaluationdeterminanths mdr_ec_exists_minorminornonzeroevaluationdeterminanths mdr_fb_exists_minorminornonzeroevaluationdeterminanths mdr_fc_exists_minorminornonzeroevaluationdeterminanths. (((mdr_d_exists_minorminornonzeroevaluationdeterminanth) = S (mdr_q_exists_minorminornonzeroevaluationdeterminanths)) /\ ((forall mdr_j_exists_minorminornonzeroevaluationdeterminanthsc. (exists mdr_gap_exists_minorminornonzeroevaluationdeterminanthscj. mdr_gap_exists_minorminornonzeroevaluationdeterminanthscj + S (mdr_j_exists_minorminornonzeroevaluationdeterminanthsc) = (S (mdr_q_exists_minorminornonzeroevaluationdeterminanths))) -> exists mdr_i_exists_minorminornonzeroevaluationdeterminanthsc mdr_up_exists_minorminornonzeroevaluationdeterminanthsc mdr_us_exists_minorminornonzeroevaluationdeterminanthsc mdr_un_exists_minorminornonzeroevaluationdeterminanthsc mdr_ut_exists_minorminornonzeroevaluationdeterminanthsc mdr_p_exists_minorminornonzeroevaluationdeterminanthsc mdr_n_exists_minorminornonzeroevaluationdeterminanthsc. ((exists mdr_gap_exists_minorminornonzeroevaluationdeterminanthsci. mdr_gap_exists_minorminornonzeroevaluationdeterminanthsci + S (mdr_i_exists_minorminornonzeroevaluationdeterminanthsc) = (mdr_i_exists_minorminornonzeroevaluationdeterminanth)) /\ ((exists mdr_z_exists_minorminornonzeroevaluationdeterminanthscr. ((exists mdr_a_exists_minorminornonzeroevaluationdeterminanthscrc mdr_b_exists_minorminornonzeroevaluationdeterminanthscrc mdr_c_exists_minorminornonzeroevaluationdeterminanthscrc mdr_e_exists_minorminornonzeroevaluationdeterminanthscrc mdr_f_exists_minorminornonzeroevaluationdeterminanthscrc. ((mdr_a_exists_minorminornonzeroevaluationdeterminanthscrc = ((mdr_q_exists_minorminornonzeroevaluationdeterminanths) + (mdr_up_exists_minorminornonzeroevaluationdeterminanthsc)) * S ((mdr_q_exists_minorminornonzeroevaluationdeterminanths) + (mdr_up_exists_minorminornonzeroevaluationdeterminanthsc)) + ((mdr_up_exists_minorminornonzeroevaluationdeterminanthsc) + (mdr_up_exists_minorminornonzeroevaluationdeterminanthsc))) /\ ((mdr_b_exists_minorminornonzeroevaluationdeterminanthscrc = ((mdr_us_exists_minorminornonzeroevaluationdeterminanthsc) + (mdr_un_exists_minorminornonzeroevaluationdeterminanthsc)) * S ((mdr_us_exists_minorminornonzeroevaluationdeterminanthsc) + (mdr_un_exists_minorminornonzeroevaluationdeterminanthsc)) + ((mdr_un_exists_minorminornonzeroevaluationdeterminanthsc) + (mdr_un_exists_minorminornonzeroevaluationdeterminanthsc))) /\ ((mdr_c_exists_minorminornonzeroevaluationdeterminanthscrc = ((mdr_a_exists_minorminornonzeroevaluationdeterminanthscrc) + (mdr_b_exists_minorminornonzeroevaluationdeterminanthscrc)) * S ((mdr_a_exists_minorminornonzeroevaluationdeterminanthscrc) + (mdr_b_exists_minorminornonzeroevaluationdeterminanthscrc)) + ((mdr_b_exists_minorminornonzeroevaluationdeterminanthscrc) + (mdr_b_exists_minorminornonzeroevaluationdeterminanthscrc))) /\ ((mdr_e_exists_minorminornonzeroevaluationdeterminanthscrc = ((mdr_p_exists_minorminornonzeroevaluationdeterminanthsc) + (mdr_n_exists_minorminornonzeroevaluationdeterminanthsc)) * S ((mdr_p_exists_minorminornonzeroevaluationdeterminanthsc) + (mdr_n_exists_minorminornonzeroevaluationdeterminanthsc)) + ((mdr_n_exists_minorminornonzeroevaluationdeterminanthsc) + (mdr_n_exists_minorminornonzeroevaluationdeterminanthsc))) /\ ((mdr_f_exists_minorminornonzeroevaluationdeterminanthscrc = ((mdr_ut_exists_minorminornonzeroevaluationdeterminanthsc) + (mdr_e_exists_minorminornonzeroevaluationdeterminanthscrc)) * S ((mdr_ut_exists_minorminornonzeroevaluationdeterminanthsc) + (mdr_e_exists_minorminornonzeroevaluationdeterminanthscrc)) + ((mdr_e_exists_minorminornonzeroevaluationdeterminanthscrc) + (mdr_e_exists_minorminornonzeroevaluationdeterminanthscrc))) /\ ((mdr_z_exists_minorminornonzeroevaluationdeterminanthscr) = ((mdr_c_exists_minorminornonzeroevaluationdeterminanthscrc) + (mdr_f_exists_minorminornonzeroevaluationdeterminanthscrc)) * S ((mdr_c_exists_minorminornonzeroevaluationdeterminanthscrc) + (mdr_f_exists_minorminornonzeroevaluationdeterminanthscrc)) + ((mdr_f_exists_minorminornonzeroevaluationdeterminanthscrc) + (mdr_f_exists_minorminornonzeroevaluationdeterminanthscrc))))))))) /\ (((exists ff_h_mdr_exists_minorminornonzeroevaluationdeterminanthscrb. ff_h_mdr_exists_minorminornonzeroevaluationdeterminanthscrb + S (mdr_z_exists_minorminornonzeroevaluationdeterminanthscr) = S ((S (mdr_i_exists_minorminornonzeroevaluationdeterminanthsc)) * mdr_c_exists_minorminornonzeroevaluationdeterminant)) /\ exists ff_q_mdr_exists_minorminornonzeroevaluationdeterminanthscrb. mdr_b_exists_minorminornonzeroevaluationdeterminant = ff_q_mdr_exists_minorminornonzeroevaluationdeterminanthscrb * S ((S (mdr_i_exists_minorminornonzeroevaluationdeterminanthsc)) * mdr_c_exists_minorminornonzeroevaluationdeterminant) + (mdr_z_exists_minorminornonzeroevaluationdeterminanthscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_exists_minorminornonzeroevaluationdeterminanthscm_positive. (exists ff_gap_mdm_lt_mdr_exists_minorminornonzeroevaluationdeterminanthscm_positive_index_bound. ff_gap_mdm_lt_mdr_exists_minorminornonzeroevaluationdeterminanthscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_exists_minorminornonzeroevaluationdeterminanthscm_positive) = ((mdr_q_exists_minorminornonzeroevaluationdeterminanths) * (mdr_q_exists_minorminornonzeroevaluationdeterminanths))) -> exists ff_row_mdm_prefix_mdr_exists_minorminornonzeroevaluationdeterminanthscm_positive ff_column_mdm_prefix_mdr_exists_minorminornonzeroevaluationdeterminanthscm_positive ff_value_mdm_prefix_mdr_exists_minorminornonzeroevaluationdeterminanthscm_positive. (ff_index_mdm_prefix_mdr_exists_minorminornonzeroevaluationdeterminanthscm_positive = (mdr_q_exists_minorminornonzeroevaluationdeterminanths) * ff_row_mdm_prefix_mdr_exists_minorminornonzeroevaluationdeterminanthscm_positive + ff_column_mdm_prefix_mdr_exists_minorminornonzeroevaluationdeterminanthscm_positive /\ ((exists ff_gap_mdm_lt_mdr_exists_minorminornonzeroevaluationdeterminanthscm_positive_column_bound. ff_gap_mdm_lt_mdr_exists_minorminornonzeroevaluationdeterminanthscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_exists_minorminornonzeroevaluationdeterminanthscm_positive) = (mdr_q_exists_minorminornonzeroevaluationdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_exists_minorminornonzeroevaluationdeterminanthscm_positive_cell ff_column_mdm_cell_mdr_exists_minorminornonzeroevaluationdeterminanthscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_exists_minorminornonzeroevaluationdeterminanthscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_exists_minorminornonzeroevaluationdeterminanthscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_exists_minorminornonzeroevaluationdeterminanthscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_exists_minorminornonzeroevaluationdeterminanthscm_positive_cell = ff_row_mdm_prefix_mdr_exists_minorminornonzeroevaluationdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_exists_minorminornonzeroevaluationdeterminanthscm_positive_cell_row_after. ff_gap_mdm_le_mdr_exists_minorminornonzeroevaluationdeterminanthscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_exists_minorminornonzeroevaluationdeterminanthscm_positive)) /\ ff_row_mdm_cell_mdr_exists_minorminornonzeroevaluationdeterminanthscm_positive_cell = S ff_row_mdm_prefix_mdr_exists_minorminornonzeroevaluationdeterminanthscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_exists_minorminornonzeroevaluationdeterminanthscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_exists_minorminornonzeroevaluationdeterminanthscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_exists_minorminornonzeroevaluationdeterminanthscm_positive) = (mdr_j_exists_minorminornonzeroevaluationdeterminanthsc)) /\ ff_column_mdm_cell_mdr_exists_minorminornonzeroevaluationdeterminanthscm_positive_cell = ff_column_mdm_prefix_mdr_exists_minorminornonzeroevaluationdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_exists_minorminornonzeroevaluationdeterminanthscm_positive_cell_column_after. ff_gap_mdm_le_mdr_exists_minorminornonzeroevaluationdeterminanthscm_positive_cell_column_after + (mdr_j_exists_minorminornonzeroevaluationdeterminanthsc) = (ff_column_mdm_prefix_mdr_exists_minorminornonzeroevaluationdeterminanthscm_positive)) /\ ff_column_mdm_cell_mdr_exists_minorminornonzeroevaluationdeterminanthscm_positive_cell = S ff_column_mdm_prefix_mdr_exists_minorminornonzeroevaluationdeterminanthscm_positive))) /\ (((exists ff_h_mdm_mdr_exists_minorminornonzeroevaluationdeterminanthscm_positive_cell_source. ff_h_mdm_mdr_exists_minorminornonzeroevaluationdeterminanthscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_exists_minorminornonzeroevaluationdeterminanthscm_positive) = S ((S ((ff_row_mdm_cell_mdr_exists_minorminornonzeroevaluationdeterminanthscm_positive_cell) * (S (mdr_q_exists_minorminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_exists_minorminornonzeroevaluationdeterminanthscm_positive_cell))) * mdr_pc_exists_minorminornonzeroevaluationdeterminanth)) /\ exists ff_q_mdm_mdr_exists_minorminornonzeroevaluationdeterminanthscm_positive_cell_source. mdr_pb_exists_minorminornonzeroevaluationdeterminanth = ff_q_mdm_mdr_exists_minorminornonzeroevaluationdeterminanthscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_exists_minorminornonzeroevaluationdeterminanthscm_positive_cell) * (S (mdr_q_exists_minorminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_exists_minorminornonzeroevaluationdeterminanthscm_positive_cell))) * mdr_pc_exists_minorminornonzeroevaluationdeterminanth) + (ff_value_mdm_prefix_mdr_exists_minorminornonzeroevaluationdeterminanthscm_positive)))))) /\ (((exists ff_h_mdm_mdr_exists_minorminornonzeroevaluationdeterminanthscm_positive_target. ff_h_mdm_mdr_exists_minorminornonzeroevaluationdeterminanthscm_positive_target + S (ff_value_mdm_prefix_mdr_exists_minorminornonzeroevaluationdeterminanthscm_positive) = S ((S (ff_index_mdm_prefix_mdr_exists_minorminornonzeroevaluationdeterminanthscm_positive)) * mdr_us_exists_minorminornonzeroevaluationdeterminanthsc)) /\ exists ff_q_mdm_mdr_exists_minorminornonzeroevaluationdeterminanthscm_positive_target. mdr_up_exists_minorminornonzeroevaluationdeterminanthsc = ff_q_mdm_mdr_exists_minorminornonzeroevaluationdeterminanthscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_exists_minorminornonzeroevaluationdeterminanthscm_positive)) * mdr_us_exists_minorminornonzeroevaluationdeterminanthsc) + (ff_value_mdm_prefix_mdr_exists_minorminornonzeroevaluationdeterminanthscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_exists_minorminornonzeroevaluationdeterminanthscm_negative. (exists ff_gap_mdm_lt_mdr_exists_minorminornonzeroevaluationdeterminanthscm_negative_index_bound. ff_gap_mdm_lt_mdr_exists_minorminornonzeroevaluationdeterminanthscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_exists_minorminornonzeroevaluationdeterminanthscm_negative) = ((mdr_q_exists_minorminornonzeroevaluationdeterminanths) * (mdr_q_exists_minorminornonzeroevaluationdeterminanths))) -> exists ff_row_mdm_prefix_mdr_exists_minorminornonzeroevaluationdeterminanthscm_negative ff_column_mdm_prefix_mdr_exists_minorminornonzeroevaluationdeterminanthscm_negative ff_value_mdm_prefix_mdr_exists_minorminornonzeroevaluationdeterminanthscm_negative. (ff_index_mdm_prefix_mdr_exists_minorminornonzeroevaluationdeterminanthscm_negative = (mdr_q_exists_minorminornonzeroevaluationdeterminanths) * ff_row_mdm_prefix_mdr_exists_minorminornonzeroevaluationdeterminanthscm_negative + ff_column_mdm_prefix_mdr_exists_minorminornonzeroevaluationdeterminanthscm_negative /\ ((exists ff_gap_mdm_lt_mdr_exists_minorminornonzeroevaluationdeterminanthscm_negative_column_bound. ff_gap_mdm_lt_mdr_exists_minorminornonzeroevaluationdeterminanthscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_exists_minorminornonzeroevaluationdeterminanthscm_negative) = (mdr_q_exists_minorminornonzeroevaluationdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_exists_minorminornonzeroevaluationdeterminanthscm_negative_cell ff_column_mdm_cell_mdr_exists_minorminornonzeroevaluationdeterminanthscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_exists_minorminornonzeroevaluationdeterminanthscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_exists_minorminornonzeroevaluationdeterminanthscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_exists_minorminornonzeroevaluationdeterminanthscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_exists_minorminornonzeroevaluationdeterminanthscm_negative_cell = ff_row_mdm_prefix_mdr_exists_minorminornonzeroevaluationdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_exists_minorminornonzeroevaluationdeterminanthscm_negative_cell_row_after. ff_gap_mdm_le_mdr_exists_minorminornonzeroevaluationdeterminanthscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_exists_minorminornonzeroevaluationdeterminanthscm_negative)) /\ ff_row_mdm_cell_mdr_exists_minorminornonzeroevaluationdeterminanthscm_negative_cell = S ff_row_mdm_prefix_mdr_exists_minorminornonzeroevaluationdeterminanthscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_exists_minorminornonzeroevaluationdeterminanthscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_exists_minorminornonzeroevaluationdeterminanthscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_exists_minorminornonzeroevaluationdeterminanthscm_negative) = (mdr_j_exists_minorminornonzeroevaluationdeterminanthsc)) /\ ff_column_mdm_cell_mdr_exists_minorminornonzeroevaluationdeterminanthscm_negative_cell = ff_column_mdm_prefix_mdr_exists_minorminornonzeroevaluationdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_exists_minorminornonzeroevaluationdeterminanthscm_negative_cell_column_after. ff_gap_mdm_le_mdr_exists_minorminornonzeroevaluationdeterminanthscm_negative_cell_column_after + (mdr_j_exists_minorminornonzeroevaluationdeterminanthsc) = (ff_column_mdm_prefix_mdr_exists_minorminornonzeroevaluationdeterminanthscm_negative)) /\ ff_column_mdm_cell_mdr_exists_minorminornonzeroevaluationdeterminanthscm_negative_cell = S ff_column_mdm_prefix_mdr_exists_minorminornonzeroevaluationdeterminanthscm_negative))) /\ (((exists ff_h_mdm_mdr_exists_minorminornonzeroevaluationdeterminanthscm_negative_cell_source. ff_h_mdm_mdr_exists_minorminornonzeroevaluationdeterminanthscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_exists_minorminornonzeroevaluationdeterminanthscm_negative) = S ((S ((ff_row_mdm_cell_mdr_exists_minorminornonzeroevaluationdeterminanthscm_negative_cell) * (S (mdr_q_exists_minorminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_exists_minorminornonzeroevaluationdeterminanthscm_negative_cell))) * mdr_nc_exists_minorminornonzeroevaluationdeterminanth)) /\ exists ff_q_mdm_mdr_exists_minorminornonzeroevaluationdeterminanthscm_negative_cell_source. mdr_nb_exists_minorminornonzeroevaluationdeterminanth = ff_q_mdm_mdr_exists_minorminornonzeroevaluationdeterminanthscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_exists_minorminornonzeroevaluationdeterminanthscm_negative_cell) * (S (mdr_q_exists_minorminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_exists_minorminornonzeroevaluationdeterminanthscm_negative_cell))) * mdr_nc_exists_minorminornonzeroevaluationdeterminanth) + (ff_value_mdm_prefix_mdr_exists_minorminornonzeroevaluationdeterminanthscm_negative)))))) /\ (((exists ff_h_mdm_mdr_exists_minorminornonzeroevaluationdeterminanthscm_negative_target. ff_h_mdm_mdr_exists_minorminornonzeroevaluationdeterminanthscm_negative_target + S (ff_value_mdm_prefix_mdr_exists_minorminornonzeroevaluationdeterminanthscm_negative) = S ((S (ff_index_mdm_prefix_mdr_exists_minorminornonzeroevaluationdeterminanthscm_negative)) * mdr_ut_exists_minorminornonzeroevaluationdeterminanthsc)) /\ exists ff_q_mdm_mdr_exists_minorminornonzeroevaluationdeterminanthscm_negative_target. mdr_un_exists_minorminornonzeroevaluationdeterminanthsc = ff_q_mdm_mdr_exists_minorminornonzeroevaluationdeterminanthscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_exists_minorminornonzeroevaluationdeterminanthscm_negative)) * mdr_ut_exists_minorminornonzeroevaluationdeterminanthsc) + (ff_value_mdm_prefix_mdr_exists_minorminornonzeroevaluationdeterminanthscm_negative))))))))) /\ ((((exists ff_h_mdr_exists_minorminornonzeroevaluationdeterminanthscp. ff_h_mdr_exists_minorminornonzeroevaluationdeterminanthscp + S (mdr_p_exists_minorminornonzeroevaluationdeterminanthsc) = S ((S (mdr_j_exists_minorminornonzeroevaluationdeterminanthsc)) * mdr_ec_exists_minorminornonzeroevaluationdeterminanths)) /\ exists ff_q_mdr_exists_minorminornonzeroevaluationdeterminanthscp. mdr_eb_exists_minorminornonzeroevaluationdeterminanths = ff_q_mdr_exists_minorminornonzeroevaluationdeterminanthscp * S ((S (mdr_j_exists_minorminornonzeroevaluationdeterminanthsc)) * mdr_ec_exists_minorminornonzeroevaluationdeterminanths) + (mdr_p_exists_minorminornonzeroevaluationdeterminanthsc))) /\ (((exists ff_h_mdr_exists_minorminornonzeroevaluationdeterminanthscn. ff_h_mdr_exists_minorminornonzeroevaluationdeterminanthscn + S (mdr_n_exists_minorminornonzeroevaluationdeterminanthsc) = S ((S (mdr_j_exists_minorminornonzeroevaluationdeterminanthsc)) * mdr_fc_exists_minorminornonzeroevaluationdeterminanths)) /\ exists ff_q_mdr_exists_minorminornonzeroevaluationdeterminanthscn. mdr_fb_exists_minorminornonzeroevaluationdeterminanths = ff_q_mdr_exists_minorminornonzeroevaluationdeterminanthscn * S ((S (mdr_j_exists_minorminornonzeroevaluationdeterminanthsc)) * mdr_fc_exists_minorminornonzeroevaluationdeterminanths) + (mdr_n_exists_minorminornonzeroevaluationdeterminanthsc)))))))) /\ (exists ff_ub_mce_fold_mdr_exists_minorminornonzeroevaluationdeterminanthsf ff_uc_mce_fold_mdr_exists_minorminornonzeroevaluationdeterminanthsf ff_vb_mce_fold_mdr_exists_minorminornonzeroevaluationdeterminanthsf ff_vc_mce_fold_mdr_exists_minorminornonzeroevaluationdeterminanthsf. ((forall ff_index_mce_alternating_mdr_exists_minorminornonzeroevaluationdeterminanthsf_prefix. (exists ff_gap_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_prefix_index. ff_gap_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_prefix_index + S (ff_index_mce_alternating_mdr_exists_minorminornonzeroevaluationdeterminanthsf_prefix) = (S (mdr_q_exists_minorminornonzeroevaluationdeterminanths))) -> exists ff_ap_mce_alternating_mdr_exists_minorminornonzeroevaluationdeterminanthsf_prefix ff_an_mce_alternating_mdr_exists_minorminornonzeroevaluationdeterminanthsf_prefix ff_bp_mce_alternating_mdr_exists_minorminornonzeroevaluationdeterminanthsf_prefix ff_bn_mce_alternating_mdr_exists_minorminornonzeroevaluationdeterminanthsf_prefix ff_p_mce_alternating_mdr_exists_minorminornonzeroevaluationdeterminanthsf_prefix ff_n_mce_alternating_mdr_exists_minorminornonzeroevaluationdeterminanthsf_prefix. ((((exists ff_h_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_prefix_ap. ff_h_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_prefix_ap + S (ff_ap_mce_alternating_mdr_exists_minorminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_exists_minorminornonzeroevaluationdeterminanthsf_prefix)) * mdr_pc_exists_minorminornonzeroevaluationdeterminanth)) /\ exists ff_q_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_prefix_ap. mdr_pb_exists_minorminornonzeroevaluationdeterminanth = ff_q_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_exists_minorminornonzeroevaluationdeterminanthsf_prefix)) * mdr_pc_exists_minorminornonzeroevaluationdeterminanth) + (ff_ap_mce_alternating_mdr_exists_minorminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_prefix_an. ff_h_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_prefix_an + S (ff_an_mce_alternating_mdr_exists_minorminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_exists_minorminornonzeroevaluationdeterminanthsf_prefix)) * mdr_nc_exists_minorminornonzeroevaluationdeterminanth)) /\ exists ff_q_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_prefix_an. mdr_nb_exists_minorminornonzeroevaluationdeterminanth = ff_q_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_exists_minorminornonzeroevaluationdeterminanthsf_prefix)) * mdr_nc_exists_minorminornonzeroevaluationdeterminanth) + (ff_an_mce_alternating_mdr_exists_minorminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_prefix_bp. ff_h_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_prefix_bp + S (ff_bp_mce_alternating_mdr_exists_minorminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_exists_minorminornonzeroevaluationdeterminanthsf_prefix)) * mdr_ec_exists_minorminornonzeroevaluationdeterminanths)) /\ exists ff_q_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_prefix_bp. mdr_eb_exists_minorminornonzeroevaluationdeterminanths = ff_q_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_exists_minorminornonzeroevaluationdeterminanthsf_prefix)) * mdr_ec_exists_minorminornonzeroevaluationdeterminanths) + (ff_bp_mce_alternating_mdr_exists_minorminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_prefix_bn. ff_h_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_prefix_bn + S (ff_bn_mce_alternating_mdr_exists_minorminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_exists_minorminornonzeroevaluationdeterminanthsf_prefix)) * mdr_fc_exists_minorminornonzeroevaluationdeterminanths)) /\ exists ff_q_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_prefix_bn. mdr_fb_exists_minorminornonzeroevaluationdeterminanths = ff_q_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_exists_minorminornonzeroevaluationdeterminanthsf_prefix)) * mdr_fc_exists_minorminornonzeroevaluationdeterminanths) + (ff_bn_mce_alternating_mdr_exists_minorminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_prefix_positive. ff_h_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_prefix_positive + S (ff_p_mce_alternating_mdr_exists_minorminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_exists_minorminornonzeroevaluationdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_exists_minorminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_prefix_positive. ff_ub_mce_fold_mdr_exists_minorminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_exists_minorminornonzeroevaluationdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_exists_minorminornonzeroevaluationdeterminanthsf) + (ff_p_mce_alternating_mdr_exists_minorminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_prefix_negative. ff_h_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_prefix_negative + S (ff_n_mce_alternating_mdr_exists_minorminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_exists_minorminornonzeroevaluationdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_exists_minorminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_prefix_negative. ff_vb_mce_fold_mdr_exists_minorminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_exists_minorminornonzeroevaluationdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_exists_minorminornonzeroevaluationdeterminanthsf) + (ff_n_mce_alternating_mdr_exists_minorminornonzeroevaluationdeterminanthsf_prefix))) /\ (((exists ff_even_mce_term_mdr_exists_minorminornonzeroevaluationdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_exists_minorminornonzeroevaluationdeterminanthsf_prefix = 2 * ff_even_mce_term_mdr_exists_minorminornonzeroevaluationdeterminanthsf_prefix_term) /\ (ff_p_mce_alternating_mdr_exists_minorminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_exists_minorminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_exists_minorminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_exists_minorminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_exists_minorminornonzeroevaluationdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_exists_minorminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_exists_minorminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_exists_minorminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_exists_minorminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_exists_minorminornonzeroevaluationdeterminanthsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_exists_minorminornonzeroevaluationdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_exists_minorminornonzeroevaluationdeterminanthsf_prefix = 2 * ff_odd_mce_term_mdr_exists_minorminornonzeroevaluationdeterminanthsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_exists_minorminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_exists_minorminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_exists_minorminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_exists_minorminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_exists_minorminornonzeroevaluationdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_exists_minorminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_exists_minorminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_exists_minorminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_exists_minorminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_exists_minorminornonzeroevaluationdeterminanthsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_positive ff_v_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_positive. ((((exists ff_h_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_positive_start. ff_h_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_positive_start. ff_u_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_positive_start * S ((S (0)) * ff_v_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_positive_terminal. ff_h_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_positive_terminal + S (mdr_p_exists_minorminornonzeroevaluationdeterminanth) = S ((S ((S (mdr_q_exists_minorminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_positive_terminal. ff_u_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_positive_terminal * S ((S ((S (mdr_q_exists_minorminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_positive) + (mdr_p_exists_minorminornonzeroevaluationdeterminanth))) /\ forall ff_i_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_positive. (exists ff_lt_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_positive_bound. ff_lt_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_positive_bound + S ff_i_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_positive = (S (mdr_q_exists_minorminornonzeroevaluationdeterminanths))) -> exists ff_a_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_positive ff_r_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_positive ff_s_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_positive. ((((exists ff_h_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_positive_summand. ff_h_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_positive_summand + S (ff_a_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_exists_minorminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_positive_summand. ff_ub_mce_fold_mdr_exists_minorminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_positive_summand * S ((S (ff_i_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_exists_minorminornonzeroevaluationdeterminanthsf) + (ff_a_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_positive_partial. ff_h_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_positive_partial + S (ff_r_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_positive_partial. ff_u_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_positive_partial * S ((S (ff_i_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_positive) + (ff_r_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_positive_successor. ff_h_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_positive_successor + S (ff_s_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_positive) = S ((S (S ff_i_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_positive_successor. ff_u_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_positive_successor * S ((S (S ff_i_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_positive) + (ff_s_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_positive))) /\ ff_s_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_positive = ff_r_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_positive + ff_a_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_positive)))))) /\ (exists ff_u_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_negative ff_v_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_negative. ((((exists ff_h_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_negative_start. ff_h_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_negative_start. ff_u_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_negative_start * S ((S (0)) * ff_v_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_negative_terminal. ff_h_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_negative_terminal + S (mdr_n_exists_minorminornonzeroevaluationdeterminanth) = S ((S ((S (mdr_q_exists_minorminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_negative_terminal. ff_u_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_negative_terminal * S ((S ((S (mdr_q_exists_minorminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_negative) + (mdr_n_exists_minorminornonzeroevaluationdeterminanth))) /\ forall ff_i_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_negative. (exists ff_lt_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_negative_bound. ff_lt_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_negative_bound + S ff_i_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_negative = (S (mdr_q_exists_minorminornonzeroevaluationdeterminanths))) -> exists ff_a_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_negative ff_r_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_negative ff_s_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_negative. ((((exists ff_h_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_negative_summand. ff_h_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_negative_summand + S (ff_a_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_exists_minorminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_negative_summand. ff_vb_mce_fold_mdr_exists_minorminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_negative_summand * S ((S (ff_i_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_exists_minorminornonzeroevaluationdeterminanthsf) + (ff_a_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_negative_partial. ff_h_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_negative_partial + S (ff_r_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_negative_partial. ff_u_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_negative_partial * S ((S (ff_i_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_negative) + (ff_r_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_negative_successor. ff_h_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_negative_successor + S (ff_s_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_negative) = S ((S (S ff_i_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_negative_successor. ff_u_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_negative_successor * S ((S (S ff_i_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_negative) + (ff_s_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_negative))) /\ ff_s_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_negative = ff_r_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_negative + ff_a_mce_mdr_exists_minorminornonzeroevaluationdeterminanthsf_negative))))))))))))))) /\ ((exists mdr_gap_exists_minorminornonzeroevaluationdeterminanti. mdr_gap_exists_minorminornonzeroevaluationdeterminanti + S (mdr_i_exists_minorminornonzeroevaluationdeterminant) = (mdr_l_exists_minorminornonzeroevaluationdeterminant)) /\ (exists mdr_z_exists_minorminornonzeroevaluationdeterminantr. ((exists mdr_a_exists_minorminornonzeroevaluationdeterminantrc mdr_b_exists_minorminornonzeroevaluationdeterminantrc mdr_c_exists_minorminornonzeroevaluationdeterminantrc mdr_e_exists_minorminornonzeroevaluationdeterminantrc mdr_f_exists_minorminornonzeroevaluationdeterminantrc. ((mdr_a_exists_minorminornonzeroevaluationdeterminantrc = ((q) + (mdr_ub_exists_minorminornonzeroevaluation)) * S ((q) + (mdr_ub_exists_minorminornonzeroevaluation)) + ((mdr_ub_exists_minorminornonzeroevaluation) + (mdr_ub_exists_minorminornonzeroevaluation))) /\ ((mdr_b_exists_minorminornonzeroevaluationdeterminantrc = ((mdr_uc_exists_minorminornonzeroevaluation) + (mdr_vb_exists_minorminornonzeroevaluation)) * S ((mdr_uc_exists_minorminornonzeroevaluation) + (mdr_vb_exists_minorminornonzeroevaluation)) + ((mdr_vb_exists_minorminornonzeroevaluation) + (mdr_vb_exists_minorminornonzeroevaluation))) /\ ((mdr_c_exists_minorminornonzeroevaluationdeterminantrc = ((mdr_a_exists_minorminornonzeroevaluationdeterminantrc) + (mdr_b_exists_minorminornonzeroevaluationdeterminantrc)) * S ((mdr_a_exists_minorminornonzeroevaluationdeterminantrc) + (mdr_b_exists_minorminornonzeroevaluationdeterminantrc)) + ((mdr_b_exists_minorminornonzeroevaluationdeterminantrc) + (mdr_b_exists_minorminornonzeroevaluationdeterminantrc))) /\ ((mdr_e_exists_minorminornonzeroevaluationdeterminantrc = ((mdr_p_exists_minorminornonzero) + (mdr_n_exists_minorminornonzero)) * S ((mdr_p_exists_minorminornonzero) + (mdr_n_exists_minorminornonzero)) + ((mdr_n_exists_minorminornonzero) + (mdr_n_exists_minorminornonzero))) /\ ((mdr_f_exists_minorminornonzeroevaluationdeterminantrc = ((mdr_vc_exists_minorminornonzeroevaluation) + (mdr_e_exists_minorminornonzeroevaluationdeterminantrc)) * S ((mdr_vc_exists_minorminornonzeroevaluation) + (mdr_e_exists_minorminornonzeroevaluationdeterminantrc)) + ((mdr_e_exists_minorminornonzeroevaluationdeterminantrc) + (mdr_e_exists_minorminornonzeroevaluationdeterminantrc))) /\ ((mdr_z_exists_minorminornonzeroevaluationdeterminantr) = ((mdr_c_exists_minorminornonzeroevaluationdeterminantrc) + (mdr_f_exists_minorminornonzeroevaluationdeterminantrc)) * S ((mdr_c_exists_minorminornonzeroevaluationdeterminantrc) + (mdr_f_exists_minorminornonzeroevaluationdeterminantrc)) + ((mdr_f_exists_minorminornonzeroevaluationdeterminantrc) + (mdr_f_exists_minorminornonzeroevaluationdeterminantrc))))))))) /\ (((exists ff_h_mdr_exists_minorminornonzeroevaluationdeterminantrb. ff_h_mdr_exists_minorminornonzeroevaluationdeterminantrb + S (mdr_z_exists_minorminornonzeroevaluationdeterminantr) = S ((S (mdr_i_exists_minorminornonzeroevaluationdeterminant)) * mdr_c_exists_minorminornonzeroevaluationdeterminant)) /\ exists ff_q_mdr_exists_minorminornonzeroevaluationdeterminantrb. mdr_b_exists_minorminornonzeroevaluationdeterminant = ff_q_mdr_exists_minorminornonzeroevaluationdeterminantrb * S ((S (mdr_i_exists_minorminornonzeroevaluationdeterminant)) * mdr_c_exists_minorminornonzeroevaluationdeterminant) + (mdr_z_exists_minorminornonzeroevaluationdeterminantr)))))))))) /\ (~(mdr_p_exists_minorminornonzero = mdr_n_exists_minorminornonzero)))))))) \/ ~(exists mdr_rb_no_minor mdr_rc_no_minor mdr_cb_no_minor mdr_cc_no_minor. (((((forall fom_index_mrf_no_minorminorrowsbound. (exists fom_gap_mrf_no_minorminorrowsbound_index_bound. fom_gap_mrf_no_minorminorrowsbound_index_bound + S (fom_index_mrf_no_minorminorrowsbound) = q) -> exists fom_value_mrf_no_minorminorrowsbound. ((((exists fom_beta_height_mrf_no_minorminorrowsbound_entry. fom_beta_height_mrf_no_minorminorrowsbound_entry + S (fom_value_mrf_no_minorminorrowsbound) = S ((S (fom_index_mrf_no_minorminorrowsbound)) * mdr_rc_no_minor)) /\ exists fom_beta_quotient_mrf_no_minorminorrowsbound_entry. mdr_rb_no_minor = fom_beta_quotient_mrf_no_minorminorrowsbound_entry * S ((S (fom_index_mrf_no_minorminorrowsbound)) * mdr_rc_no_minor) + (fom_value_mrf_no_minorminorrowsbound))) /\ (exists fom_gap_mrf_no_minorminorrowsbound_value_bound. fom_gap_mrf_no_minorminorrowsbound_value_bound + S (fom_value_mrf_no_minorminorrowsbound) = r))) /\ (forall mdr_i_no_minorminorrowsdistinct mdr_j_no_minorminorrowsdistinct mdr_a_no_minorminorrowsdistinct. (exists mdr_gap_no_minorminorrowsdistincti. mdr_gap_no_minorminorrowsdistincti + S (mdr_i_no_minorminorrowsdistinct) = (q)) -> (exists mdr_gap_no_minorminorrowsdistinctj. mdr_gap_no_minorminorrowsdistinctj + S (mdr_j_no_minorminorrowsdistinct) = (q)) -> (((exists ff_h_mdr_no_minorminorrowsdistinctfirst. ff_h_mdr_no_minorminorrowsdistinctfirst + S (mdr_a_no_minorminorrowsdistinct) = S ((S (mdr_i_no_minorminorrowsdistinct)) * mdr_rc_no_minor)) /\ exists ff_q_mdr_no_minorminorrowsdistinctfirst. mdr_rb_no_minor = ff_q_mdr_no_minorminorrowsdistinctfirst * S ((S (mdr_i_no_minorminorrowsdistinct)) * mdr_rc_no_minor) + (mdr_a_no_minorminorrowsdistinct))) -> (((exists ff_h_mdr_no_minorminorrowsdistinctsecond. ff_h_mdr_no_minorminorrowsdistinctsecond + S (mdr_a_no_minorminorrowsdistinct) = S ((S (mdr_j_no_minorminorrowsdistinct)) * mdr_rc_no_minor)) /\ exists ff_q_mdr_no_minorminorrowsdistinctsecond. mdr_rb_no_minor = ff_q_mdr_no_minorminorrowsdistinctsecond * S ((S (mdr_j_no_minorminorrowsdistinct)) * mdr_rc_no_minor) + (mdr_a_no_minorminorrowsdistinct))) -> mdr_i_no_minorminorrowsdistinct = mdr_j_no_minorminorrowsdistinct))) /\ ((((forall fom_index_mrf_no_minorminorcolumnsbound. (exists fom_gap_mrf_no_minorminorcolumnsbound_index_bound. fom_gap_mrf_no_minorminorcolumnsbound_index_bound + S (fom_index_mrf_no_minorminorcolumnsbound) = q) -> exists fom_value_mrf_no_minorminorcolumnsbound. ((((exists fom_beta_height_mrf_no_minorminorcolumnsbound_entry. fom_beta_height_mrf_no_minorminorcolumnsbound_entry + S (fom_value_mrf_no_minorminorcolumnsbound) = S ((S (fom_index_mrf_no_minorminorcolumnsbound)) * mdr_cc_no_minor)) /\ exists fom_beta_quotient_mrf_no_minorminorcolumnsbound_entry. mdr_cb_no_minor = fom_beta_quotient_mrf_no_minorminorcolumnsbound_entry * S ((S (fom_index_mrf_no_minorminorcolumnsbound)) * mdr_cc_no_minor) + (fom_value_mrf_no_minorminorcolumnsbound))) /\ (exists fom_gap_mrf_no_minorminorcolumnsbound_value_bound. fom_gap_mrf_no_minorminorcolumnsbound_value_bound + S (fom_value_mrf_no_minorminorcolumnsbound) = w))) /\ (forall mdr_i_no_minorminorcolumnsdistinct mdr_j_no_minorminorcolumnsdistinct mdr_a_no_minorminorcolumnsdistinct. (exists mdr_gap_no_minorminorcolumnsdistincti. mdr_gap_no_minorminorcolumnsdistincti + S (mdr_i_no_minorminorcolumnsdistinct) = (q)) -> (exists mdr_gap_no_minorminorcolumnsdistinctj. mdr_gap_no_minorminorcolumnsdistinctj + S (mdr_j_no_minorminorcolumnsdistinct) = (q)) -> (((exists ff_h_mdr_no_minorminorcolumnsdistinctfirst. ff_h_mdr_no_minorminorcolumnsdistinctfirst + S (mdr_a_no_minorminorcolumnsdistinct) = S ((S (mdr_i_no_minorminorcolumnsdistinct)) * mdr_cc_no_minor)) /\ exists ff_q_mdr_no_minorminorcolumnsdistinctfirst. mdr_cb_no_minor = ff_q_mdr_no_minorminorcolumnsdistinctfirst * S ((S (mdr_i_no_minorminorcolumnsdistinct)) * mdr_cc_no_minor) + (mdr_a_no_minorminorcolumnsdistinct))) -> (((exists ff_h_mdr_no_minorminorcolumnsdistinctsecond. ff_h_mdr_no_minorminorcolumnsdistinctsecond + S (mdr_a_no_minorminorcolumnsdistinct) = S ((S (mdr_j_no_minorminorcolumnsdistinct)) * mdr_cc_no_minor)) /\ exists ff_q_mdr_no_minorminorcolumnsdistinctsecond. mdr_cb_no_minor = ff_q_mdr_no_minorminorcolumnsdistinctsecond * S ((S (mdr_j_no_minorminorcolumnsdistinct)) * mdr_cc_no_minor) + (mdr_a_no_minorminorcolumnsdistinct))) -> mdr_i_no_minorminorcolumnsdistinct = mdr_j_no_minorminorcolumnsdistinct))) /\ (exists mdr_p_no_minorminornonzero mdr_n_no_minorminornonzero. ((exists mdr_ub_no_minorminornonzeroevaluation mdr_uc_no_minorminornonzeroevaluation mdr_vb_no_minorminornonzeroevaluation mdr_vc_no_minorminornonzeroevaluation. ((((forall mdr_i_no_minorminornonzeroevaluationmatrixpositive. (exists mdr_gap_no_minorminornonzeroevaluationmatrixpositivebound. mdr_gap_no_minorminornonzeroevaluationmatrixpositivebound + S (mdr_i_no_minorminornonzeroevaluationmatrixpositive) = ((q) * (q))) -> exists mdr_a_no_minorminornonzeroevaluationmatrixpositive. (((exists mdr_r_no_minorminornonzeroevaluationmatrixpositivepoint mdr_s_no_minorminornonzeroevaluationmatrixpositivepoint mdr_u_no_minorminornonzeroevaluationmatrixpositivepoint mdr_v_no_minorminornonzeroevaluationmatrixpositivepoint. ((mdr_i_no_minorminornonzeroevaluationmatrixpositive = (q) * mdr_r_no_minorminornonzeroevaluationmatrixpositivepoint + mdr_s_no_minorminornonzeroevaluationmatrixpositivepoint) /\ ((exists mdr_gap_no_minorminornonzeroevaluationmatrixpositivepointcolumn. mdr_gap_no_minorminornonzeroevaluationmatrixpositivepointcolumn + S (mdr_s_no_minorminornonzeroevaluationmatrixpositivepoint) = (q)) /\ ((((exists ff_h_mdr_no_minorminornonzeroevaluationmatrixpositivepointrow_index. ff_h_mdr_no_minorminornonzeroevaluationmatrixpositivepointrow_index + S (mdr_u_no_minorminornonzeroevaluationmatrixpositivepoint) = S ((S (mdr_r_no_minorminornonzeroevaluationmatrixpositivepoint)) * mdr_rc_no_minor)) /\ exists ff_q_mdr_no_minorminornonzeroevaluationmatrixpositivepointrow_index. mdr_rb_no_minor = ff_q_mdr_no_minorminornonzeroevaluationmatrixpositivepointrow_index * S ((S (mdr_r_no_minorminornonzeroevaluationmatrixpositivepoint)) * mdr_rc_no_minor) + (mdr_u_no_minorminornonzeroevaluationmatrixpositivepoint))) /\ ((((exists ff_h_mdr_no_minorminornonzeroevaluationmatrixpositivepointcolumn_index. ff_h_mdr_no_minorminornonzeroevaluationmatrixpositivepointcolumn_index + S (mdr_v_no_minorminornonzeroevaluationmatrixpositivepoint) = S ((S (mdr_s_no_minorminornonzeroevaluationmatrixpositivepoint)) * mdr_cc_no_minor)) /\ exists ff_q_mdr_no_minorminornonzeroevaluationmatrixpositivepointcolumn_index. mdr_cb_no_minor = ff_q_mdr_no_minorminornonzeroevaluationmatrixpositivepointcolumn_index * S ((S (mdr_s_no_minorminornonzeroevaluationmatrixpositivepoint)) * mdr_cc_no_minor) + (mdr_v_no_minorminornonzeroevaluationmatrixpositivepoint))) /\ (((exists ff_h_mdr_no_minorminornonzeroevaluationmatrixpositivepointsource. ff_h_mdr_no_minorminornonzeroevaluationmatrixpositivepointsource + S (mdr_a_no_minorminornonzeroevaluationmatrixpositive) = S ((S ((mdr_u_no_minorminornonzeroevaluationmatrixpositivepoint) * (w) + (mdr_v_no_minorminornonzeroevaluationmatrixpositivepoint))) * pc)) /\ exists ff_q_mdr_no_minorminornonzeroevaluationmatrixpositivepointsource. pb = ff_q_mdr_no_minorminornonzeroevaluationmatrixpositivepointsource * S ((S ((mdr_u_no_minorminornonzeroevaluationmatrixpositivepoint) * (w) + (mdr_v_no_minorminornonzeroevaluationmatrixpositivepoint))) * pc) + (mdr_a_no_minorminornonzeroevaluationmatrixpositive)))))))) /\ (((exists ff_h_mdr_no_minorminornonzeroevaluationmatrixpositiveoutput. ff_h_mdr_no_minorminornonzeroevaluationmatrixpositiveoutput + S (mdr_a_no_minorminornonzeroevaluationmatrixpositive) = S ((S (mdr_i_no_minorminornonzeroevaluationmatrixpositive)) * mdr_uc_no_minorminornonzeroevaluation)) /\ exists ff_q_mdr_no_minorminornonzeroevaluationmatrixpositiveoutput. mdr_ub_no_minorminornonzeroevaluation = ff_q_mdr_no_minorminornonzeroevaluationmatrixpositiveoutput * S ((S (mdr_i_no_minorminornonzeroevaluationmatrixpositive)) * mdr_uc_no_minorminornonzeroevaluation) + (mdr_a_no_minorminornonzeroevaluationmatrixpositive)))))) /\ (forall mdr_i_no_minorminornonzeroevaluationmatrixnegative. (exists mdr_gap_no_minorminornonzeroevaluationmatrixnegativebound. mdr_gap_no_minorminornonzeroevaluationmatrixnegativebound + S (mdr_i_no_minorminornonzeroevaluationmatrixnegative) = ((q) * (q))) -> exists mdr_a_no_minorminornonzeroevaluationmatrixnegative. (((exists mdr_r_no_minorminornonzeroevaluationmatrixnegativepoint mdr_s_no_minorminornonzeroevaluationmatrixnegativepoint mdr_u_no_minorminornonzeroevaluationmatrixnegativepoint mdr_v_no_minorminornonzeroevaluationmatrixnegativepoint. ((mdr_i_no_minorminornonzeroevaluationmatrixnegative = (q) * mdr_r_no_minorminornonzeroevaluationmatrixnegativepoint + mdr_s_no_minorminornonzeroevaluationmatrixnegativepoint) /\ ((exists mdr_gap_no_minorminornonzeroevaluationmatrixnegativepointcolumn. mdr_gap_no_minorminornonzeroevaluationmatrixnegativepointcolumn + S (mdr_s_no_minorminornonzeroevaluationmatrixnegativepoint) = (q)) /\ ((((exists ff_h_mdr_no_minorminornonzeroevaluationmatrixnegativepointrow_index. ff_h_mdr_no_minorminornonzeroevaluationmatrixnegativepointrow_index + S (mdr_u_no_minorminornonzeroevaluationmatrixnegativepoint) = S ((S (mdr_r_no_minorminornonzeroevaluationmatrixnegativepoint)) * mdr_rc_no_minor)) /\ exists ff_q_mdr_no_minorminornonzeroevaluationmatrixnegativepointrow_index. mdr_rb_no_minor = ff_q_mdr_no_minorminornonzeroevaluationmatrixnegativepointrow_index * S ((S (mdr_r_no_minorminornonzeroevaluationmatrixnegativepoint)) * mdr_rc_no_minor) + (mdr_u_no_minorminornonzeroevaluationmatrixnegativepoint))) /\ ((((exists ff_h_mdr_no_minorminornonzeroevaluationmatrixnegativepointcolumn_index. ff_h_mdr_no_minorminornonzeroevaluationmatrixnegativepointcolumn_index + S (mdr_v_no_minorminornonzeroevaluationmatrixnegativepoint) = S ((S (mdr_s_no_minorminornonzeroevaluationmatrixnegativepoint)) * mdr_cc_no_minor)) /\ exists ff_q_mdr_no_minorminornonzeroevaluationmatrixnegativepointcolumn_index. mdr_cb_no_minor = ff_q_mdr_no_minorminornonzeroevaluationmatrixnegativepointcolumn_index * S ((S (mdr_s_no_minorminornonzeroevaluationmatrixnegativepoint)) * mdr_cc_no_minor) + (mdr_v_no_minorminornonzeroevaluationmatrixnegativepoint))) /\ (((exists ff_h_mdr_no_minorminornonzeroevaluationmatrixnegativepointsource. ff_h_mdr_no_minorminornonzeroevaluationmatrixnegativepointsource + S (mdr_a_no_minorminornonzeroevaluationmatrixnegative) = S ((S ((mdr_u_no_minorminornonzeroevaluationmatrixnegativepoint) * (w) + (mdr_v_no_minorminornonzeroevaluationmatrixnegativepoint))) * nc)) /\ exists ff_q_mdr_no_minorminornonzeroevaluationmatrixnegativepointsource. nb = ff_q_mdr_no_minorminornonzeroevaluationmatrixnegativepointsource * S ((S ((mdr_u_no_minorminornonzeroevaluationmatrixnegativepoint) * (w) + (mdr_v_no_minorminornonzeroevaluationmatrixnegativepoint))) * nc) + (mdr_a_no_minorminornonzeroevaluationmatrixnegative)))))))) /\ (((exists ff_h_mdr_no_minorminornonzeroevaluationmatrixnegativeoutput. ff_h_mdr_no_minorminornonzeroevaluationmatrixnegativeoutput + S (mdr_a_no_minorminornonzeroevaluationmatrixnegative) = S ((S (mdr_i_no_minorminornonzeroevaluationmatrixnegative)) * mdr_vc_no_minorminornonzeroevaluation)) /\ exists ff_q_mdr_no_minorminornonzeroevaluationmatrixnegativeoutput. mdr_vb_no_minorminornonzeroevaluation = ff_q_mdr_no_minorminornonzeroevaluationmatrixnegativeoutput * S ((S (mdr_i_no_minorminornonzeroevaluationmatrixnegative)) * mdr_vc_no_minorminornonzeroevaluation) + (mdr_a_no_minorminornonzeroevaluationmatrixnegative)))))))) /\ (exists mdr_b_no_minorminornonzeroevaluationdeterminant mdr_c_no_minorminornonzeroevaluationdeterminant mdr_l_no_minorminornonzeroevaluationdeterminant mdr_i_no_minorminornonzeroevaluationdeterminant. ((forall mdr_i_no_minorminornonzeroevaluationdeterminanth. (exists mdr_gap_no_minorminornonzeroevaluationdeterminanthi. mdr_gap_no_minorminornonzeroevaluationdeterminanthi + S (mdr_i_no_minorminornonzeroevaluationdeterminanth) = (mdr_l_no_minorminornonzeroevaluationdeterminant)) -> exists mdr_d_no_minorminornonzeroevaluationdeterminanth mdr_pb_no_minorminornonzeroevaluationdeterminanth mdr_pc_no_minorminornonzeroevaluationdeterminanth mdr_nb_no_minorminornonzeroevaluationdeterminanth mdr_nc_no_minorminornonzeroevaluationdeterminanth mdr_p_no_minorminornonzeroevaluationdeterminanth mdr_n_no_minorminornonzeroevaluationdeterminanth. ((exists mdr_z_no_minorminornonzeroevaluationdeterminanthr. ((exists mdr_a_no_minorminornonzeroevaluationdeterminanthrc mdr_b_no_minorminornonzeroevaluationdeterminanthrc mdr_c_no_minorminornonzeroevaluationdeterminanthrc mdr_e_no_minorminornonzeroevaluationdeterminanthrc mdr_f_no_minorminornonzeroevaluationdeterminanthrc. ((mdr_a_no_minorminornonzeroevaluationdeterminanthrc = ((mdr_d_no_minorminornonzeroevaluationdeterminanth) + (mdr_pb_no_minorminornonzeroevaluationdeterminanth)) * S ((mdr_d_no_minorminornonzeroevaluationdeterminanth) + (mdr_pb_no_minorminornonzeroevaluationdeterminanth)) + ((mdr_pb_no_minorminornonzeroevaluationdeterminanth) + (mdr_pb_no_minorminornonzeroevaluationdeterminanth))) /\ ((mdr_b_no_minorminornonzeroevaluationdeterminanthrc = ((mdr_pc_no_minorminornonzeroevaluationdeterminanth) + (mdr_nb_no_minorminornonzeroevaluationdeterminanth)) * S ((mdr_pc_no_minorminornonzeroevaluationdeterminanth) + (mdr_nb_no_minorminornonzeroevaluationdeterminanth)) + ((mdr_nb_no_minorminornonzeroevaluationdeterminanth) + (mdr_nb_no_minorminornonzeroevaluationdeterminanth))) /\ ((mdr_c_no_minorminornonzeroevaluationdeterminanthrc = ((mdr_a_no_minorminornonzeroevaluationdeterminanthrc) + (mdr_b_no_minorminornonzeroevaluationdeterminanthrc)) * S ((mdr_a_no_minorminornonzeroevaluationdeterminanthrc) + (mdr_b_no_minorminornonzeroevaluationdeterminanthrc)) + ((mdr_b_no_minorminornonzeroevaluationdeterminanthrc) + (mdr_b_no_minorminornonzeroevaluationdeterminanthrc))) /\ ((mdr_e_no_minorminornonzeroevaluationdeterminanthrc = ((mdr_p_no_minorminornonzeroevaluationdeterminanth) + (mdr_n_no_minorminornonzeroevaluationdeterminanth)) * S ((mdr_p_no_minorminornonzeroevaluationdeterminanth) + (mdr_n_no_minorminornonzeroevaluationdeterminanth)) + ((mdr_n_no_minorminornonzeroevaluationdeterminanth) + (mdr_n_no_minorminornonzeroevaluationdeterminanth))) /\ ((mdr_f_no_minorminornonzeroevaluationdeterminanthrc = ((mdr_nc_no_minorminornonzeroevaluationdeterminanth) + (mdr_e_no_minorminornonzeroevaluationdeterminanthrc)) * S ((mdr_nc_no_minorminornonzeroevaluationdeterminanth) + (mdr_e_no_minorminornonzeroevaluationdeterminanthrc)) + ((mdr_e_no_minorminornonzeroevaluationdeterminanthrc) + (mdr_e_no_minorminornonzeroevaluationdeterminanthrc))) /\ ((mdr_z_no_minorminornonzeroevaluationdeterminanthr) = ((mdr_c_no_minorminornonzeroevaluationdeterminanthrc) + (mdr_f_no_minorminornonzeroevaluationdeterminanthrc)) * S ((mdr_c_no_minorminornonzeroevaluationdeterminanthrc) + (mdr_f_no_minorminornonzeroevaluationdeterminanthrc)) + ((mdr_f_no_minorminornonzeroevaluationdeterminanthrc) + (mdr_f_no_minorminornonzeroevaluationdeterminanthrc))))))))) /\ (((exists ff_h_mdr_no_minorminornonzeroevaluationdeterminanthrb. ff_h_mdr_no_minorminornonzeroevaluationdeterminanthrb + S (mdr_z_no_minorminornonzeroevaluationdeterminanthr) = S ((S (mdr_i_no_minorminornonzeroevaluationdeterminanth)) * mdr_c_no_minorminornonzeroevaluationdeterminant)) /\ exists ff_q_mdr_no_minorminornonzeroevaluationdeterminanthrb. mdr_b_no_minorminornonzeroevaluationdeterminant = ff_q_mdr_no_minorminornonzeroevaluationdeterminanthrb * S ((S (mdr_i_no_minorminornonzeroevaluationdeterminanth)) * mdr_c_no_minorminornonzeroevaluationdeterminant) + (mdr_z_no_minorminornonzeroevaluationdeterminanthr))))) /\ (((((mdr_d_no_minorminornonzeroevaluationdeterminanth) = 0) /\ (((mdr_p_no_minorminornonzeroevaluationdeterminanth) = 1) /\ ((mdr_n_no_minorminornonzeroevaluationdeterminanth) = 0))) \/ exists mdr_q_no_minorminornonzeroevaluationdeterminanths mdr_eb_no_minorminornonzeroevaluationdeterminanths mdr_ec_no_minorminornonzeroevaluationdeterminanths mdr_fb_no_minorminornonzeroevaluationdeterminanths mdr_fc_no_minorminornonzeroevaluationdeterminanths. (((mdr_d_no_minorminornonzeroevaluationdeterminanth) = S (mdr_q_no_minorminornonzeroevaluationdeterminanths)) /\ ((forall mdr_j_no_minorminornonzeroevaluationdeterminanthsc. (exists mdr_gap_no_minorminornonzeroevaluationdeterminanthscj. mdr_gap_no_minorminornonzeroevaluationdeterminanthscj + S (mdr_j_no_minorminornonzeroevaluationdeterminanthsc) = (S (mdr_q_no_minorminornonzeroevaluationdeterminanths))) -> exists mdr_i_no_minorminornonzeroevaluationdeterminanthsc mdr_up_no_minorminornonzeroevaluationdeterminanthsc mdr_us_no_minorminornonzeroevaluationdeterminanthsc mdr_un_no_minorminornonzeroevaluationdeterminanthsc mdr_ut_no_minorminornonzeroevaluationdeterminanthsc mdr_p_no_minorminornonzeroevaluationdeterminanthsc mdr_n_no_minorminornonzeroevaluationdeterminanthsc. ((exists mdr_gap_no_minorminornonzeroevaluationdeterminanthsci. mdr_gap_no_minorminornonzeroevaluationdeterminanthsci + S (mdr_i_no_minorminornonzeroevaluationdeterminanthsc) = (mdr_i_no_minorminornonzeroevaluationdeterminanth)) /\ ((exists mdr_z_no_minorminornonzeroevaluationdeterminanthscr. ((exists mdr_a_no_minorminornonzeroevaluationdeterminanthscrc mdr_b_no_minorminornonzeroevaluationdeterminanthscrc mdr_c_no_minorminornonzeroevaluationdeterminanthscrc mdr_e_no_minorminornonzeroevaluationdeterminanthscrc mdr_f_no_minorminornonzeroevaluationdeterminanthscrc. ((mdr_a_no_minorminornonzeroevaluationdeterminanthscrc = ((mdr_q_no_minorminornonzeroevaluationdeterminanths) + (mdr_up_no_minorminornonzeroevaluationdeterminanthsc)) * S ((mdr_q_no_minorminornonzeroevaluationdeterminanths) + (mdr_up_no_minorminornonzeroevaluationdeterminanthsc)) + ((mdr_up_no_minorminornonzeroevaluationdeterminanthsc) + (mdr_up_no_minorminornonzeroevaluationdeterminanthsc))) /\ ((mdr_b_no_minorminornonzeroevaluationdeterminanthscrc = ((mdr_us_no_minorminornonzeroevaluationdeterminanthsc) + (mdr_un_no_minorminornonzeroevaluationdeterminanthsc)) * S ((mdr_us_no_minorminornonzeroevaluationdeterminanthsc) + (mdr_un_no_minorminornonzeroevaluationdeterminanthsc)) + ((mdr_un_no_minorminornonzeroevaluationdeterminanthsc) + (mdr_un_no_minorminornonzeroevaluationdeterminanthsc))) /\ ((mdr_c_no_minorminornonzeroevaluationdeterminanthscrc = ((mdr_a_no_minorminornonzeroevaluationdeterminanthscrc) + (mdr_b_no_minorminornonzeroevaluationdeterminanthscrc)) * S ((mdr_a_no_minorminornonzeroevaluationdeterminanthscrc) + (mdr_b_no_minorminornonzeroevaluationdeterminanthscrc)) + ((mdr_b_no_minorminornonzeroevaluationdeterminanthscrc) + (mdr_b_no_minorminornonzeroevaluationdeterminanthscrc))) /\ ((mdr_e_no_minorminornonzeroevaluationdeterminanthscrc = ((mdr_p_no_minorminornonzeroevaluationdeterminanthsc) + (mdr_n_no_minorminornonzeroevaluationdeterminanthsc)) * S ((mdr_p_no_minorminornonzeroevaluationdeterminanthsc) + (mdr_n_no_minorminornonzeroevaluationdeterminanthsc)) + ((mdr_n_no_minorminornonzeroevaluationdeterminanthsc) + (mdr_n_no_minorminornonzeroevaluationdeterminanthsc))) /\ ((mdr_f_no_minorminornonzeroevaluationdeterminanthscrc = ((mdr_ut_no_minorminornonzeroevaluationdeterminanthsc) + (mdr_e_no_minorminornonzeroevaluationdeterminanthscrc)) * S ((mdr_ut_no_minorminornonzeroevaluationdeterminanthsc) + (mdr_e_no_minorminornonzeroevaluationdeterminanthscrc)) + ((mdr_e_no_minorminornonzeroevaluationdeterminanthscrc) + (mdr_e_no_minorminornonzeroevaluationdeterminanthscrc))) /\ ((mdr_z_no_minorminornonzeroevaluationdeterminanthscr) = ((mdr_c_no_minorminornonzeroevaluationdeterminanthscrc) + (mdr_f_no_minorminornonzeroevaluationdeterminanthscrc)) * S ((mdr_c_no_minorminornonzeroevaluationdeterminanthscrc) + (mdr_f_no_minorminornonzeroevaluationdeterminanthscrc)) + ((mdr_f_no_minorminornonzeroevaluationdeterminanthscrc) + (mdr_f_no_minorminornonzeroevaluationdeterminanthscrc))))))))) /\ (((exists ff_h_mdr_no_minorminornonzeroevaluationdeterminanthscrb. ff_h_mdr_no_minorminornonzeroevaluationdeterminanthscrb + S (mdr_z_no_minorminornonzeroevaluationdeterminanthscr) = S ((S (mdr_i_no_minorminornonzeroevaluationdeterminanthsc)) * mdr_c_no_minorminornonzeroevaluationdeterminant)) /\ exists ff_q_mdr_no_minorminornonzeroevaluationdeterminanthscrb. mdr_b_no_minorminornonzeroevaluationdeterminant = ff_q_mdr_no_minorminornonzeroevaluationdeterminanthscrb * S ((S (mdr_i_no_minorminornonzeroevaluationdeterminanthsc)) * mdr_c_no_minorminornonzeroevaluationdeterminant) + (mdr_z_no_minorminornonzeroevaluationdeterminanthscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_no_minorminornonzeroevaluationdeterminanthscm_positive. (exists ff_gap_mdm_lt_mdr_no_minorminornonzeroevaluationdeterminanthscm_positive_index_bound. ff_gap_mdm_lt_mdr_no_minorminornonzeroevaluationdeterminanthscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_no_minorminornonzeroevaluationdeterminanthscm_positive) = ((mdr_q_no_minorminornonzeroevaluationdeterminanths) * (mdr_q_no_minorminornonzeroevaluationdeterminanths))) -> exists ff_row_mdm_prefix_mdr_no_minorminornonzeroevaluationdeterminanthscm_positive ff_column_mdm_prefix_mdr_no_minorminornonzeroevaluationdeterminanthscm_positive ff_value_mdm_prefix_mdr_no_minorminornonzeroevaluationdeterminanthscm_positive. (ff_index_mdm_prefix_mdr_no_minorminornonzeroevaluationdeterminanthscm_positive = (mdr_q_no_minorminornonzeroevaluationdeterminanths) * ff_row_mdm_prefix_mdr_no_minorminornonzeroevaluationdeterminanthscm_positive + ff_column_mdm_prefix_mdr_no_minorminornonzeroevaluationdeterminanthscm_positive /\ ((exists ff_gap_mdm_lt_mdr_no_minorminornonzeroevaluationdeterminanthscm_positive_column_bound. ff_gap_mdm_lt_mdr_no_minorminornonzeroevaluationdeterminanthscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_no_minorminornonzeroevaluationdeterminanthscm_positive) = (mdr_q_no_minorminornonzeroevaluationdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_no_minorminornonzeroevaluationdeterminanthscm_positive_cell ff_column_mdm_cell_mdr_no_minorminornonzeroevaluationdeterminanthscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_no_minorminornonzeroevaluationdeterminanthscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_no_minorminornonzeroevaluationdeterminanthscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_no_minorminornonzeroevaluationdeterminanthscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_no_minorminornonzeroevaluationdeterminanthscm_positive_cell = ff_row_mdm_prefix_mdr_no_minorminornonzeroevaluationdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_no_minorminornonzeroevaluationdeterminanthscm_positive_cell_row_after. ff_gap_mdm_le_mdr_no_minorminornonzeroevaluationdeterminanthscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_no_minorminornonzeroevaluationdeterminanthscm_positive)) /\ ff_row_mdm_cell_mdr_no_minorminornonzeroevaluationdeterminanthscm_positive_cell = S ff_row_mdm_prefix_mdr_no_minorminornonzeroevaluationdeterminanthscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_no_minorminornonzeroevaluationdeterminanthscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_no_minorminornonzeroevaluationdeterminanthscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_no_minorminornonzeroevaluationdeterminanthscm_positive) = (mdr_j_no_minorminornonzeroevaluationdeterminanthsc)) /\ ff_column_mdm_cell_mdr_no_minorminornonzeroevaluationdeterminanthscm_positive_cell = ff_column_mdm_prefix_mdr_no_minorminornonzeroevaluationdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_no_minorminornonzeroevaluationdeterminanthscm_positive_cell_column_after. ff_gap_mdm_le_mdr_no_minorminornonzeroevaluationdeterminanthscm_positive_cell_column_after + (mdr_j_no_minorminornonzeroevaluationdeterminanthsc) = (ff_column_mdm_prefix_mdr_no_minorminornonzeroevaluationdeterminanthscm_positive)) /\ ff_column_mdm_cell_mdr_no_minorminornonzeroevaluationdeterminanthscm_positive_cell = S ff_column_mdm_prefix_mdr_no_minorminornonzeroevaluationdeterminanthscm_positive))) /\ (((exists ff_h_mdm_mdr_no_minorminornonzeroevaluationdeterminanthscm_positive_cell_source. ff_h_mdm_mdr_no_minorminornonzeroevaluationdeterminanthscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_no_minorminornonzeroevaluationdeterminanthscm_positive) = S ((S ((ff_row_mdm_cell_mdr_no_minorminornonzeroevaluationdeterminanthscm_positive_cell) * (S (mdr_q_no_minorminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_no_minorminornonzeroevaluationdeterminanthscm_positive_cell))) * mdr_pc_no_minorminornonzeroevaluationdeterminanth)) /\ exists ff_q_mdm_mdr_no_minorminornonzeroevaluationdeterminanthscm_positive_cell_source. mdr_pb_no_minorminornonzeroevaluationdeterminanth = ff_q_mdm_mdr_no_minorminornonzeroevaluationdeterminanthscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_no_minorminornonzeroevaluationdeterminanthscm_positive_cell) * (S (mdr_q_no_minorminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_no_minorminornonzeroevaluationdeterminanthscm_positive_cell))) * mdr_pc_no_minorminornonzeroevaluationdeterminanth) + (ff_value_mdm_prefix_mdr_no_minorminornonzeroevaluationdeterminanthscm_positive)))))) /\ (((exists ff_h_mdm_mdr_no_minorminornonzeroevaluationdeterminanthscm_positive_target. ff_h_mdm_mdr_no_minorminornonzeroevaluationdeterminanthscm_positive_target + S (ff_value_mdm_prefix_mdr_no_minorminornonzeroevaluationdeterminanthscm_positive) = S ((S (ff_index_mdm_prefix_mdr_no_minorminornonzeroevaluationdeterminanthscm_positive)) * mdr_us_no_minorminornonzeroevaluationdeterminanthsc)) /\ exists ff_q_mdm_mdr_no_minorminornonzeroevaluationdeterminanthscm_positive_target. mdr_up_no_minorminornonzeroevaluationdeterminanthsc = ff_q_mdm_mdr_no_minorminornonzeroevaluationdeterminanthscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_no_minorminornonzeroevaluationdeterminanthscm_positive)) * mdr_us_no_minorminornonzeroevaluationdeterminanthsc) + (ff_value_mdm_prefix_mdr_no_minorminornonzeroevaluationdeterminanthscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_no_minorminornonzeroevaluationdeterminanthscm_negative. (exists ff_gap_mdm_lt_mdr_no_minorminornonzeroevaluationdeterminanthscm_negative_index_bound. ff_gap_mdm_lt_mdr_no_minorminornonzeroevaluationdeterminanthscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_no_minorminornonzeroevaluationdeterminanthscm_negative) = ((mdr_q_no_minorminornonzeroevaluationdeterminanths) * (mdr_q_no_minorminornonzeroevaluationdeterminanths))) -> exists ff_row_mdm_prefix_mdr_no_minorminornonzeroevaluationdeterminanthscm_negative ff_column_mdm_prefix_mdr_no_minorminornonzeroevaluationdeterminanthscm_negative ff_value_mdm_prefix_mdr_no_minorminornonzeroevaluationdeterminanthscm_negative. (ff_index_mdm_prefix_mdr_no_minorminornonzeroevaluationdeterminanthscm_negative = (mdr_q_no_minorminornonzeroevaluationdeterminanths) * ff_row_mdm_prefix_mdr_no_minorminornonzeroevaluationdeterminanthscm_negative + ff_column_mdm_prefix_mdr_no_minorminornonzeroevaluationdeterminanthscm_negative /\ ((exists ff_gap_mdm_lt_mdr_no_minorminornonzeroevaluationdeterminanthscm_negative_column_bound. ff_gap_mdm_lt_mdr_no_minorminornonzeroevaluationdeterminanthscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_no_minorminornonzeroevaluationdeterminanthscm_negative) = (mdr_q_no_minorminornonzeroevaluationdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_no_minorminornonzeroevaluationdeterminanthscm_negative_cell ff_column_mdm_cell_mdr_no_minorminornonzeroevaluationdeterminanthscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_no_minorminornonzeroevaluationdeterminanthscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_no_minorminornonzeroevaluationdeterminanthscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_no_minorminornonzeroevaluationdeterminanthscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_no_minorminornonzeroevaluationdeterminanthscm_negative_cell = ff_row_mdm_prefix_mdr_no_minorminornonzeroevaluationdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_no_minorminornonzeroevaluationdeterminanthscm_negative_cell_row_after. ff_gap_mdm_le_mdr_no_minorminornonzeroevaluationdeterminanthscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_no_minorminornonzeroevaluationdeterminanthscm_negative)) /\ ff_row_mdm_cell_mdr_no_minorminornonzeroevaluationdeterminanthscm_negative_cell = S ff_row_mdm_prefix_mdr_no_minorminornonzeroevaluationdeterminanthscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_no_minorminornonzeroevaluationdeterminanthscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_no_minorminornonzeroevaluationdeterminanthscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_no_minorminornonzeroevaluationdeterminanthscm_negative) = (mdr_j_no_minorminornonzeroevaluationdeterminanthsc)) /\ ff_column_mdm_cell_mdr_no_minorminornonzeroevaluationdeterminanthscm_negative_cell = ff_column_mdm_prefix_mdr_no_minorminornonzeroevaluationdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_no_minorminornonzeroevaluationdeterminanthscm_negative_cell_column_after. ff_gap_mdm_le_mdr_no_minorminornonzeroevaluationdeterminanthscm_negative_cell_column_after + (mdr_j_no_minorminornonzeroevaluationdeterminanthsc) = (ff_column_mdm_prefix_mdr_no_minorminornonzeroevaluationdeterminanthscm_negative)) /\ ff_column_mdm_cell_mdr_no_minorminornonzeroevaluationdeterminanthscm_negative_cell = S ff_column_mdm_prefix_mdr_no_minorminornonzeroevaluationdeterminanthscm_negative))) /\ (((exists ff_h_mdm_mdr_no_minorminornonzeroevaluationdeterminanthscm_negative_cell_source. ff_h_mdm_mdr_no_minorminornonzeroevaluationdeterminanthscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_no_minorminornonzeroevaluationdeterminanthscm_negative) = S ((S ((ff_row_mdm_cell_mdr_no_minorminornonzeroevaluationdeterminanthscm_negative_cell) * (S (mdr_q_no_minorminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_no_minorminornonzeroevaluationdeterminanthscm_negative_cell))) * mdr_nc_no_minorminornonzeroevaluationdeterminanth)) /\ exists ff_q_mdm_mdr_no_minorminornonzeroevaluationdeterminanthscm_negative_cell_source. mdr_nb_no_minorminornonzeroevaluationdeterminanth = ff_q_mdm_mdr_no_minorminornonzeroevaluationdeterminanthscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_no_minorminornonzeroevaluationdeterminanthscm_negative_cell) * (S (mdr_q_no_minorminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_no_minorminornonzeroevaluationdeterminanthscm_negative_cell))) * mdr_nc_no_minorminornonzeroevaluationdeterminanth) + (ff_value_mdm_prefix_mdr_no_minorminornonzeroevaluationdeterminanthscm_negative)))))) /\ (((exists ff_h_mdm_mdr_no_minorminornonzeroevaluationdeterminanthscm_negative_target. ff_h_mdm_mdr_no_minorminornonzeroevaluationdeterminanthscm_negative_target + S (ff_value_mdm_prefix_mdr_no_minorminornonzeroevaluationdeterminanthscm_negative) = S ((S (ff_index_mdm_prefix_mdr_no_minorminornonzeroevaluationdeterminanthscm_negative)) * mdr_ut_no_minorminornonzeroevaluationdeterminanthsc)) /\ exists ff_q_mdm_mdr_no_minorminornonzeroevaluationdeterminanthscm_negative_target. mdr_un_no_minorminornonzeroevaluationdeterminanthsc = ff_q_mdm_mdr_no_minorminornonzeroevaluationdeterminanthscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_no_minorminornonzeroevaluationdeterminanthscm_negative)) * mdr_ut_no_minorminornonzeroevaluationdeterminanthsc) + (ff_value_mdm_prefix_mdr_no_minorminornonzeroevaluationdeterminanthscm_negative))))))))) /\ ((((exists ff_h_mdr_no_minorminornonzeroevaluationdeterminanthscp. ff_h_mdr_no_minorminornonzeroevaluationdeterminanthscp + S (mdr_p_no_minorminornonzeroevaluationdeterminanthsc) = S ((S (mdr_j_no_minorminornonzeroevaluationdeterminanthsc)) * mdr_ec_no_minorminornonzeroevaluationdeterminanths)) /\ exists ff_q_mdr_no_minorminornonzeroevaluationdeterminanthscp. mdr_eb_no_minorminornonzeroevaluationdeterminanths = ff_q_mdr_no_minorminornonzeroevaluationdeterminanthscp * S ((S (mdr_j_no_minorminornonzeroevaluationdeterminanthsc)) * mdr_ec_no_minorminornonzeroevaluationdeterminanths) + (mdr_p_no_minorminornonzeroevaluationdeterminanthsc))) /\ (((exists ff_h_mdr_no_minorminornonzeroevaluationdeterminanthscn. ff_h_mdr_no_minorminornonzeroevaluationdeterminanthscn + S (mdr_n_no_minorminornonzeroevaluationdeterminanthsc) = S ((S (mdr_j_no_minorminornonzeroevaluationdeterminanthsc)) * mdr_fc_no_minorminornonzeroevaluationdeterminanths)) /\ exists ff_q_mdr_no_minorminornonzeroevaluationdeterminanthscn. mdr_fb_no_minorminornonzeroevaluationdeterminanths = ff_q_mdr_no_minorminornonzeroevaluationdeterminanthscn * S ((S (mdr_j_no_minorminornonzeroevaluationdeterminanthsc)) * mdr_fc_no_minorminornonzeroevaluationdeterminanths) + (mdr_n_no_minorminornonzeroevaluationdeterminanthsc)))))))) /\ (exists ff_ub_mce_fold_mdr_no_minorminornonzeroevaluationdeterminanthsf ff_uc_mce_fold_mdr_no_minorminornonzeroevaluationdeterminanthsf ff_vb_mce_fold_mdr_no_minorminornonzeroevaluationdeterminanthsf ff_vc_mce_fold_mdr_no_minorminornonzeroevaluationdeterminanthsf. ((forall ff_index_mce_alternating_mdr_no_minorminornonzeroevaluationdeterminanthsf_prefix. (exists ff_gap_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_prefix_index. ff_gap_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_prefix_index + S (ff_index_mce_alternating_mdr_no_minorminornonzeroevaluationdeterminanthsf_prefix) = (S (mdr_q_no_minorminornonzeroevaluationdeterminanths))) -> exists ff_ap_mce_alternating_mdr_no_minorminornonzeroevaluationdeterminanthsf_prefix ff_an_mce_alternating_mdr_no_minorminornonzeroevaluationdeterminanthsf_prefix ff_bp_mce_alternating_mdr_no_minorminornonzeroevaluationdeterminanthsf_prefix ff_bn_mce_alternating_mdr_no_minorminornonzeroevaluationdeterminanthsf_prefix ff_p_mce_alternating_mdr_no_minorminornonzeroevaluationdeterminanthsf_prefix ff_n_mce_alternating_mdr_no_minorminornonzeroevaluationdeterminanthsf_prefix. ((((exists ff_h_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_prefix_ap. ff_h_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_prefix_ap + S (ff_ap_mce_alternating_mdr_no_minorminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_no_minorminornonzeroevaluationdeterminanthsf_prefix)) * mdr_pc_no_minorminornonzeroevaluationdeterminanth)) /\ exists ff_q_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_prefix_ap. mdr_pb_no_minorminornonzeroevaluationdeterminanth = ff_q_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_no_minorminornonzeroevaluationdeterminanthsf_prefix)) * mdr_pc_no_minorminornonzeroevaluationdeterminanth) + (ff_ap_mce_alternating_mdr_no_minorminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_prefix_an. ff_h_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_prefix_an + S (ff_an_mce_alternating_mdr_no_minorminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_no_minorminornonzeroevaluationdeterminanthsf_prefix)) * mdr_nc_no_minorminornonzeroevaluationdeterminanth)) /\ exists ff_q_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_prefix_an. mdr_nb_no_minorminornonzeroevaluationdeterminanth = ff_q_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_no_minorminornonzeroevaluationdeterminanthsf_prefix)) * mdr_nc_no_minorminornonzeroevaluationdeterminanth) + (ff_an_mce_alternating_mdr_no_minorminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_prefix_bp. ff_h_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_prefix_bp + S (ff_bp_mce_alternating_mdr_no_minorminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_no_minorminornonzeroevaluationdeterminanthsf_prefix)) * mdr_ec_no_minorminornonzeroevaluationdeterminanths)) /\ exists ff_q_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_prefix_bp. mdr_eb_no_minorminornonzeroevaluationdeterminanths = ff_q_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_no_minorminornonzeroevaluationdeterminanthsf_prefix)) * mdr_ec_no_minorminornonzeroevaluationdeterminanths) + (ff_bp_mce_alternating_mdr_no_minorminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_prefix_bn. ff_h_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_prefix_bn + S (ff_bn_mce_alternating_mdr_no_minorminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_no_minorminornonzeroevaluationdeterminanthsf_prefix)) * mdr_fc_no_minorminornonzeroevaluationdeterminanths)) /\ exists ff_q_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_prefix_bn. mdr_fb_no_minorminornonzeroevaluationdeterminanths = ff_q_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_no_minorminornonzeroevaluationdeterminanthsf_prefix)) * mdr_fc_no_minorminornonzeroevaluationdeterminanths) + (ff_bn_mce_alternating_mdr_no_minorminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_prefix_positive. ff_h_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_prefix_positive + S (ff_p_mce_alternating_mdr_no_minorminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_no_minorminornonzeroevaluationdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_no_minorminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_prefix_positive. ff_ub_mce_fold_mdr_no_minorminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_no_minorminornonzeroevaluationdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_no_minorminornonzeroevaluationdeterminanthsf) + (ff_p_mce_alternating_mdr_no_minorminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_prefix_negative. ff_h_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_prefix_negative + S (ff_n_mce_alternating_mdr_no_minorminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_no_minorminornonzeroevaluationdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_no_minorminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_prefix_negative. ff_vb_mce_fold_mdr_no_minorminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_no_minorminornonzeroevaluationdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_no_minorminornonzeroevaluationdeterminanthsf) + (ff_n_mce_alternating_mdr_no_minorminornonzeroevaluationdeterminanthsf_prefix))) /\ (((exists ff_even_mce_term_mdr_no_minorminornonzeroevaluationdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_no_minorminornonzeroevaluationdeterminanthsf_prefix = 2 * ff_even_mce_term_mdr_no_minorminornonzeroevaluationdeterminanthsf_prefix_term) /\ (ff_p_mce_alternating_mdr_no_minorminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_no_minorminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_no_minorminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_no_minorminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_no_minorminornonzeroevaluationdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_no_minorminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_no_minorminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_no_minorminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_no_minorminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_no_minorminornonzeroevaluationdeterminanthsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_no_minorminornonzeroevaluationdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_no_minorminornonzeroevaluationdeterminanthsf_prefix = 2 * ff_odd_mce_term_mdr_no_minorminornonzeroevaluationdeterminanthsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_no_minorminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_no_minorminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_no_minorminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_no_minorminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_no_minorminornonzeroevaluationdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_no_minorminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_no_minorminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_no_minorminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_no_minorminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_no_minorminornonzeroevaluationdeterminanthsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_positive ff_v_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_positive. ((((exists ff_h_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_positive_start. ff_h_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_positive_start. ff_u_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_positive_start * S ((S (0)) * ff_v_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_positive_terminal. ff_h_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_positive_terminal + S (mdr_p_no_minorminornonzeroevaluationdeterminanth) = S ((S ((S (mdr_q_no_minorminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_positive_terminal. ff_u_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_positive_terminal * S ((S ((S (mdr_q_no_minorminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_positive) + (mdr_p_no_minorminornonzeroevaluationdeterminanth))) /\ forall ff_i_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_positive. (exists ff_lt_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_positive_bound. ff_lt_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_positive_bound + S ff_i_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_positive = (S (mdr_q_no_minorminornonzeroevaluationdeterminanths))) -> exists ff_a_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_positive ff_r_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_positive ff_s_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_positive. ((((exists ff_h_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_positive_summand. ff_h_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_positive_summand + S (ff_a_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_no_minorminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_positive_summand. ff_ub_mce_fold_mdr_no_minorminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_positive_summand * S ((S (ff_i_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_no_minorminornonzeroevaluationdeterminanthsf) + (ff_a_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_positive_partial. ff_h_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_positive_partial + S (ff_r_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_positive_partial. ff_u_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_positive_partial * S ((S (ff_i_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_positive) + (ff_r_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_positive_successor. ff_h_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_positive_successor + S (ff_s_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_positive) = S ((S (S ff_i_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_positive_successor. ff_u_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_positive_successor * S ((S (S ff_i_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_positive) + (ff_s_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_positive))) /\ ff_s_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_positive = ff_r_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_positive + ff_a_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_positive)))))) /\ (exists ff_u_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_negative ff_v_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_negative. ((((exists ff_h_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_negative_start. ff_h_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_negative_start. ff_u_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_negative_start * S ((S (0)) * ff_v_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_negative_terminal. ff_h_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_negative_terminal + S (mdr_n_no_minorminornonzeroevaluationdeterminanth) = S ((S ((S (mdr_q_no_minorminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_negative_terminal. ff_u_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_negative_terminal * S ((S ((S (mdr_q_no_minorminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_negative) + (mdr_n_no_minorminornonzeroevaluationdeterminanth))) /\ forall ff_i_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_negative. (exists ff_lt_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_negative_bound. ff_lt_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_negative_bound + S ff_i_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_negative = (S (mdr_q_no_minorminornonzeroevaluationdeterminanths))) -> exists ff_a_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_negative ff_r_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_negative ff_s_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_negative. ((((exists ff_h_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_negative_summand. ff_h_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_negative_summand + S (ff_a_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_no_minorminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_negative_summand. ff_vb_mce_fold_mdr_no_minorminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_negative_summand * S ((S (ff_i_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_no_minorminornonzeroevaluationdeterminanthsf) + (ff_a_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_negative_partial. ff_h_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_negative_partial + S (ff_r_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_negative_partial. ff_u_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_negative_partial * S ((S (ff_i_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_negative) + (ff_r_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_negative_successor. ff_h_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_negative_successor + S (ff_s_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_negative) = S ((S (S ff_i_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_negative_successor. ff_u_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_negative_successor * S ((S (S ff_i_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_negative) + (ff_s_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_negative))) /\ ff_s_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_negative = ff_r_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_negative + ff_a_mce_mdr_no_minorminornonzeroevaluationdeterminanthsf_negative))))))))))))))) /\ ((exists mdr_gap_no_minorminornonzeroevaluationdeterminanti. mdr_gap_no_minorminornonzeroevaluationdeterminanti + S (mdr_i_no_minorminornonzeroevaluationdeterminant) = (mdr_l_no_minorminornonzeroevaluationdeterminant)) /\ (exists mdr_z_no_minorminornonzeroevaluationdeterminantr. ((exists mdr_a_no_minorminornonzeroevaluationdeterminantrc mdr_b_no_minorminornonzeroevaluationdeterminantrc mdr_c_no_minorminornonzeroevaluationdeterminantrc mdr_e_no_minorminornonzeroevaluationdeterminantrc mdr_f_no_minorminornonzeroevaluationdeterminantrc. ((mdr_a_no_minorminornonzeroevaluationdeterminantrc = ((q) + (mdr_ub_no_minorminornonzeroevaluation)) * S ((q) + (mdr_ub_no_minorminornonzeroevaluation)) + ((mdr_ub_no_minorminornonzeroevaluation) + (mdr_ub_no_minorminornonzeroevaluation))) /\ ((mdr_b_no_minorminornonzeroevaluationdeterminantrc = ((mdr_uc_no_minorminornonzeroevaluation) + (mdr_vb_no_minorminornonzeroevaluation)) * S ((mdr_uc_no_minorminornonzeroevaluation) + (mdr_vb_no_minorminornonzeroevaluation)) + ((mdr_vb_no_minorminornonzeroevaluation) + (mdr_vb_no_minorminornonzeroevaluation))) /\ ((mdr_c_no_minorminornonzeroevaluationdeterminantrc = ((mdr_a_no_minorminornonzeroevaluationdeterminantrc) + (mdr_b_no_minorminornonzeroevaluationdeterminantrc)) * S ((mdr_a_no_minorminornonzeroevaluationdeterminantrc) + (mdr_b_no_minorminornonzeroevaluationdeterminantrc)) + ((mdr_b_no_minorminornonzeroevaluationdeterminantrc) + (mdr_b_no_minorminornonzeroevaluationdeterminantrc))) /\ ((mdr_e_no_minorminornonzeroevaluationdeterminantrc = ((mdr_p_no_minorminornonzero) + (mdr_n_no_minorminornonzero)) * S ((mdr_p_no_minorminornonzero) + (mdr_n_no_minorminornonzero)) + ((mdr_n_no_minorminornonzero) + (mdr_n_no_minorminornonzero))) /\ ((mdr_f_no_minorminornonzeroevaluationdeterminantrc = ((mdr_vc_no_minorminornonzeroevaluation) + (mdr_e_no_minorminornonzeroevaluationdeterminantrc)) * S ((mdr_vc_no_minorminornonzeroevaluation) + (mdr_e_no_minorminornonzeroevaluationdeterminantrc)) + ((mdr_e_no_minorminornonzeroevaluationdeterminantrc) + (mdr_e_no_minorminornonzeroevaluationdeterminantrc))) /\ ((mdr_z_no_minorminornonzeroevaluationdeterminantr) = ((mdr_c_no_minorminornonzeroevaluationdeterminantrc) + (mdr_f_no_minorminornonzeroevaluationdeterminantrc)) * S ((mdr_c_no_minorminornonzeroevaluationdeterminantrc) + (mdr_f_no_minorminornonzeroevaluationdeterminantrc)) + ((mdr_f_no_minorminornonzeroevaluationdeterminantrc) + (mdr_f_no_minorminornonzeroevaluationdeterminantrc))))))))) /\ (((exists ff_h_mdr_no_minorminornonzeroevaluationdeterminantrb. ff_h_mdr_no_minorminornonzeroevaluationdeterminantrb + S (mdr_z_no_minorminornonzeroevaluationdeterminantr) = S ((S (mdr_i_no_minorminornonzeroevaluationdeterminant)) * mdr_c_no_minorminornonzeroevaluationdeterminant)) /\ exists ff_q_mdr_no_minorminornonzeroevaluationdeterminantrb. mdr_b_no_minorminornonzeroevaluationdeterminant = ff_q_mdr_no_minorminornonzeroevaluationdeterminantrb * S ((S (mdr_i_no_minorminornonzeroevaluationdeterminant)) * mdr_c_no_minorminornonzeroevaluationdeterminant) + (mdr_z_no_minorminornonzeroevaluationdeterminantr)))))))))) /\ (~(mdr_p_no_minorminornonzero = mdr_n_no_minorminornonzero))))))))