matrix_rank_absence_from_all_minors_zero

Exact expanded first-order arithmetic statement

forall pb pc nb nc r w q. (forall mdr_rb_zero_minors mdr_rc_zero_minors mdr_cb_zero_minors mdr_cc_zero_minors mdr_p_zero_minors mdr_n_zero_minors. (((forall fom_index_mrf_zero_minorsrowsbound. (exists fom_gap_mrf_zero_minorsrowsbound_index_bound. fom_gap_mrf_zero_minorsrowsbound_index_bound + S (fom_index_mrf_zero_minorsrowsbound) = q) -> exists fom_value_mrf_zero_minorsrowsbound. ((((exists fom_beta_height_mrf_zero_minorsrowsbound_entry. fom_beta_height_mrf_zero_minorsrowsbound_entry + S (fom_value_mrf_zero_minorsrowsbound) = S ((S (fom_index_mrf_zero_minorsrowsbound)) * mdr_rc_zero_minors)) /\ exists fom_beta_quotient_mrf_zero_minorsrowsbound_entry. mdr_rb_zero_minors = fom_beta_quotient_mrf_zero_minorsrowsbound_entry * S ((S (fom_index_mrf_zero_minorsrowsbound)) * mdr_rc_zero_minors) + (fom_value_mrf_zero_minorsrowsbound))) /\ (exists fom_gap_mrf_zero_minorsrowsbound_value_bound. fom_gap_mrf_zero_minorsrowsbound_value_bound + S (fom_value_mrf_zero_minorsrowsbound) = r))) /\ (forall mdr_i_zero_minorsrowsdistinct mdr_j_zero_minorsrowsdistinct mdr_a_zero_minorsrowsdistinct. (exists mdr_gap_zero_minorsrowsdistincti. mdr_gap_zero_minorsrowsdistincti + S (mdr_i_zero_minorsrowsdistinct) = (q)) -> (exists mdr_gap_zero_minorsrowsdistinctj. mdr_gap_zero_minorsrowsdistinctj + S (mdr_j_zero_minorsrowsdistinct) = (q)) -> (((exists ff_h_mdr_zero_minorsrowsdistinctfirst. ff_h_mdr_zero_minorsrowsdistinctfirst + S (mdr_a_zero_minorsrowsdistinct) = S ((S (mdr_i_zero_minorsrowsdistinct)) * mdr_rc_zero_minors)) /\ exists ff_q_mdr_zero_minorsrowsdistinctfirst. mdr_rb_zero_minors = ff_q_mdr_zero_minorsrowsdistinctfirst * S ((S (mdr_i_zero_minorsrowsdistinct)) * mdr_rc_zero_minors) + (mdr_a_zero_minorsrowsdistinct))) -> (((exists ff_h_mdr_zero_minorsrowsdistinctsecond. ff_h_mdr_zero_minorsrowsdistinctsecond + S (mdr_a_zero_minorsrowsdistinct) = S ((S (mdr_j_zero_minorsrowsdistinct)) * mdr_rc_zero_minors)) /\ exists ff_q_mdr_zero_minorsrowsdistinctsecond. mdr_rb_zero_minors = ff_q_mdr_zero_minorsrowsdistinctsecond * S ((S (mdr_j_zero_minorsrowsdistinct)) * mdr_rc_zero_minors) + (mdr_a_zero_minorsrowsdistinct))) -> mdr_i_zero_minorsrowsdistinct = mdr_j_zero_minorsrowsdistinct))) -> (((forall fom_index_mrf_zero_minorscolumnsbound. (exists fom_gap_mrf_zero_minorscolumnsbound_index_bound. fom_gap_mrf_zero_minorscolumnsbound_index_bound + S (fom_index_mrf_zero_minorscolumnsbound) = q) -> exists fom_value_mrf_zero_minorscolumnsbound. ((((exists fom_beta_height_mrf_zero_minorscolumnsbound_entry. fom_beta_height_mrf_zero_minorscolumnsbound_entry + S (fom_value_mrf_zero_minorscolumnsbound) = S ((S (fom_index_mrf_zero_minorscolumnsbound)) * mdr_cc_zero_minors)) /\ exists fom_beta_quotient_mrf_zero_minorscolumnsbound_entry. mdr_cb_zero_minors = fom_beta_quotient_mrf_zero_minorscolumnsbound_entry * S ((S (fom_index_mrf_zero_minorscolumnsbound)) * mdr_cc_zero_minors) + (fom_value_mrf_zero_minorscolumnsbound))) /\ (exists fom_gap_mrf_zero_minorscolumnsbound_value_bound. fom_gap_mrf_zero_minorscolumnsbound_value_bound + S (fom_value_mrf_zero_minorscolumnsbound) = w))) /\ (forall mdr_i_zero_minorscolumnsdistinct mdr_j_zero_minorscolumnsdistinct mdr_a_zero_minorscolumnsdistinct. (exists mdr_gap_zero_minorscolumnsdistincti. mdr_gap_zero_minorscolumnsdistincti + S (mdr_i_zero_minorscolumnsdistinct) = (q)) -> (exists mdr_gap_zero_minorscolumnsdistinctj. mdr_gap_zero_minorscolumnsdistinctj + S (mdr_j_zero_minorscolumnsdistinct) = (q)) -> (((exists ff_h_mdr_zero_minorscolumnsdistinctfirst. ff_h_mdr_zero_minorscolumnsdistinctfirst + S (mdr_a_zero_minorscolumnsdistinct) = S ((S (mdr_i_zero_minorscolumnsdistinct)) * mdr_cc_zero_minors)) /\ exists ff_q_mdr_zero_minorscolumnsdistinctfirst. mdr_cb_zero_minors = ff_q_mdr_zero_minorscolumnsdistinctfirst * S ((S (mdr_i_zero_minorscolumnsdistinct)) * mdr_cc_zero_minors) + (mdr_a_zero_minorscolumnsdistinct))) -> (((exists ff_h_mdr_zero_minorscolumnsdistinctsecond. ff_h_mdr_zero_minorscolumnsdistinctsecond + S (mdr_a_zero_minorscolumnsdistinct) = S ((S (mdr_j_zero_minorscolumnsdistinct)) * mdr_cc_zero_minors)) /\ exists ff_q_mdr_zero_minorscolumnsdistinctsecond. mdr_cb_zero_minors = ff_q_mdr_zero_minorscolumnsdistinctsecond * S ((S (mdr_j_zero_minorscolumnsdistinct)) * mdr_cc_zero_minors) + (mdr_a_zero_minorscolumnsdistinct))) -> mdr_i_zero_minorscolumnsdistinct = mdr_j_zero_minorscolumnsdistinct))) -> (exists mdr_ub_zero_minorsevaluation mdr_uc_zero_minorsevaluation mdr_vb_zero_minorsevaluation mdr_vc_zero_minorsevaluation. ((((forall mdr_i_zero_minorsevaluationmatrixpositive. (exists mdr_gap_zero_minorsevaluationmatrixpositivebound. mdr_gap_zero_minorsevaluationmatrixpositivebound + S (mdr_i_zero_minorsevaluationmatrixpositive) = ((q) * (q))) -> exists mdr_a_zero_minorsevaluationmatrixpositive. (((exists mdr_r_zero_minorsevaluationmatrixpositivepoint mdr_s_zero_minorsevaluationmatrixpositivepoint mdr_u_zero_minorsevaluationmatrixpositivepoint mdr_v_zero_minorsevaluationmatrixpositivepoint. ((mdr_i_zero_minorsevaluationmatrixpositive = (q) * mdr_r_zero_minorsevaluationmatrixpositivepoint + mdr_s_zero_minorsevaluationmatrixpositivepoint) /\ ((exists mdr_gap_zero_minorsevaluationmatrixpositivepointcolumn. mdr_gap_zero_minorsevaluationmatrixpositivepointcolumn + S (mdr_s_zero_minorsevaluationmatrixpositivepoint) = (q)) /\ ((((exists ff_h_mdr_zero_minorsevaluationmatrixpositivepointrow_index. ff_h_mdr_zero_minorsevaluationmatrixpositivepointrow_index + S (mdr_u_zero_minorsevaluationmatrixpositivepoint) = S ((S (mdr_r_zero_minorsevaluationmatrixpositivepoint)) * mdr_rc_zero_minors)) /\ exists ff_q_mdr_zero_minorsevaluationmatrixpositivepointrow_index. mdr_rb_zero_minors = ff_q_mdr_zero_minorsevaluationmatrixpositivepointrow_index * S ((S (mdr_r_zero_minorsevaluationmatrixpositivepoint)) * mdr_rc_zero_minors) + (mdr_u_zero_minorsevaluationmatrixpositivepoint))) /\ ((((exists ff_h_mdr_zero_minorsevaluationmatrixpositivepointcolumn_index. ff_h_mdr_zero_minorsevaluationmatrixpositivepointcolumn_index + S (mdr_v_zero_minorsevaluationmatrixpositivepoint) = S ((S (mdr_s_zero_minorsevaluationmatrixpositivepoint)) * mdr_cc_zero_minors)) /\ exists ff_q_mdr_zero_minorsevaluationmatrixpositivepointcolumn_index. mdr_cb_zero_minors = ff_q_mdr_zero_minorsevaluationmatrixpositivepointcolumn_index * S ((S (mdr_s_zero_minorsevaluationmatrixpositivepoint)) * mdr_cc_zero_minors) + (mdr_v_zero_minorsevaluationmatrixpositivepoint))) /\ (((exists ff_h_mdr_zero_minorsevaluationmatrixpositivepointsource. ff_h_mdr_zero_minorsevaluationmatrixpositivepointsource + S (mdr_a_zero_minorsevaluationmatrixpositive) = S ((S ((mdr_u_zero_minorsevaluationmatrixpositivepoint) * (w) + (mdr_v_zero_minorsevaluationmatrixpositivepoint))) * pc)) /\ exists ff_q_mdr_zero_minorsevaluationmatrixpositivepointsource. pb = ff_q_mdr_zero_minorsevaluationmatrixpositivepointsource * S ((S ((mdr_u_zero_minorsevaluationmatrixpositivepoint) * (w) + (mdr_v_zero_minorsevaluationmatrixpositivepoint))) * pc) + (mdr_a_zero_minorsevaluationmatrixpositive)))))))) /\ (((exists ff_h_mdr_zero_minorsevaluationmatrixpositiveoutput. ff_h_mdr_zero_minorsevaluationmatrixpositiveoutput + S (mdr_a_zero_minorsevaluationmatrixpositive) = S ((S (mdr_i_zero_minorsevaluationmatrixpositive)) * mdr_uc_zero_minorsevaluation)) /\ exists ff_q_mdr_zero_minorsevaluationmatrixpositiveoutput. mdr_ub_zero_minorsevaluation = ff_q_mdr_zero_minorsevaluationmatrixpositiveoutput * S ((S (mdr_i_zero_minorsevaluationmatrixpositive)) * mdr_uc_zero_minorsevaluation) + (mdr_a_zero_minorsevaluationmatrixpositive)))))) /\ (forall mdr_i_zero_minorsevaluationmatrixnegative. (exists mdr_gap_zero_minorsevaluationmatrixnegativebound. mdr_gap_zero_minorsevaluationmatrixnegativebound + S (mdr_i_zero_minorsevaluationmatrixnegative) = ((q) * (q))) -> exists mdr_a_zero_minorsevaluationmatrixnegative. (((exists mdr_r_zero_minorsevaluationmatrixnegativepoint mdr_s_zero_minorsevaluationmatrixnegativepoint mdr_u_zero_minorsevaluationmatrixnegativepoint mdr_v_zero_minorsevaluationmatrixnegativepoint. ((mdr_i_zero_minorsevaluationmatrixnegative = (q) * mdr_r_zero_minorsevaluationmatrixnegativepoint + mdr_s_zero_minorsevaluationmatrixnegativepoint) /\ ((exists mdr_gap_zero_minorsevaluationmatrixnegativepointcolumn. mdr_gap_zero_minorsevaluationmatrixnegativepointcolumn + S (mdr_s_zero_minorsevaluationmatrixnegativepoint) = (q)) /\ ((((exists ff_h_mdr_zero_minorsevaluationmatrixnegativepointrow_index. ff_h_mdr_zero_minorsevaluationmatrixnegativepointrow_index + S (mdr_u_zero_minorsevaluationmatrixnegativepoint) = S ((S (mdr_r_zero_minorsevaluationmatrixnegativepoint)) * mdr_rc_zero_minors)) /\ exists ff_q_mdr_zero_minorsevaluationmatrixnegativepointrow_index. mdr_rb_zero_minors = ff_q_mdr_zero_minorsevaluationmatrixnegativepointrow_index * S ((S (mdr_r_zero_minorsevaluationmatrixnegativepoint)) * mdr_rc_zero_minors) + (mdr_u_zero_minorsevaluationmatrixnegativepoint))) /\ ((((exists ff_h_mdr_zero_minorsevaluationmatrixnegativepointcolumn_index. ff_h_mdr_zero_minorsevaluationmatrixnegativepointcolumn_index + S (mdr_v_zero_minorsevaluationmatrixnegativepoint) = S ((S (mdr_s_zero_minorsevaluationmatrixnegativepoint)) * mdr_cc_zero_minors)) /\ exists ff_q_mdr_zero_minorsevaluationmatrixnegativepointcolumn_index. mdr_cb_zero_minors = ff_q_mdr_zero_minorsevaluationmatrixnegativepointcolumn_index * S ((S (mdr_s_zero_minorsevaluationmatrixnegativepoint)) * mdr_cc_zero_minors) + (mdr_v_zero_minorsevaluationmatrixnegativepoint))) /\ (((exists ff_h_mdr_zero_minorsevaluationmatrixnegativepointsource. ff_h_mdr_zero_minorsevaluationmatrixnegativepointsource + S (mdr_a_zero_minorsevaluationmatrixnegative) = S ((S ((mdr_u_zero_minorsevaluationmatrixnegativepoint) * (w) + (mdr_v_zero_minorsevaluationmatrixnegativepoint))) * nc)) /\ exists ff_q_mdr_zero_minorsevaluationmatrixnegativepointsource. nb = ff_q_mdr_zero_minorsevaluationmatrixnegativepointsource * S ((S ((mdr_u_zero_minorsevaluationmatrixnegativepoint) * (w) + (mdr_v_zero_minorsevaluationmatrixnegativepoint))) * nc) + (mdr_a_zero_minorsevaluationmatrixnegative)))))))) /\ (((exists ff_h_mdr_zero_minorsevaluationmatrixnegativeoutput. ff_h_mdr_zero_minorsevaluationmatrixnegativeoutput + S (mdr_a_zero_minorsevaluationmatrixnegative) = S ((S (mdr_i_zero_minorsevaluationmatrixnegative)) * mdr_vc_zero_minorsevaluation)) /\ exists ff_q_mdr_zero_minorsevaluationmatrixnegativeoutput. mdr_vb_zero_minorsevaluation = ff_q_mdr_zero_minorsevaluationmatrixnegativeoutput * S ((S (mdr_i_zero_minorsevaluationmatrixnegative)) * mdr_vc_zero_minorsevaluation) + (mdr_a_zero_minorsevaluationmatrixnegative)))))))) /\ (exists mdr_b_zero_minorsevaluationdeterminant mdr_c_zero_minorsevaluationdeterminant mdr_l_zero_minorsevaluationdeterminant mdr_i_zero_minorsevaluationdeterminant. ((forall mdr_i_zero_minorsevaluationdeterminanth. (exists mdr_gap_zero_minorsevaluationdeterminanthi. mdr_gap_zero_minorsevaluationdeterminanthi + S (mdr_i_zero_minorsevaluationdeterminanth) = (mdr_l_zero_minorsevaluationdeterminant)) -> exists mdr_d_zero_minorsevaluationdeterminanth mdr_pb_zero_minorsevaluationdeterminanth mdr_pc_zero_minorsevaluationdeterminanth mdr_nb_zero_minorsevaluationdeterminanth mdr_nc_zero_minorsevaluationdeterminanth mdr_p_zero_minorsevaluationdeterminanth mdr_n_zero_minorsevaluationdeterminanth. ((exists mdr_z_zero_minorsevaluationdeterminanthr. ((exists mdr_a_zero_minorsevaluationdeterminanthrc mdr_b_zero_minorsevaluationdeterminanthrc mdr_c_zero_minorsevaluationdeterminanthrc mdr_e_zero_minorsevaluationdeterminanthrc mdr_f_zero_minorsevaluationdeterminanthrc. ((mdr_a_zero_minorsevaluationdeterminanthrc = ((mdr_d_zero_minorsevaluationdeterminanth) + (mdr_pb_zero_minorsevaluationdeterminanth)) * S ((mdr_d_zero_minorsevaluationdeterminanth) + (mdr_pb_zero_minorsevaluationdeterminanth)) + ((mdr_pb_zero_minorsevaluationdeterminanth) + (mdr_pb_zero_minorsevaluationdeterminanth))) /\ ((mdr_b_zero_minorsevaluationdeterminanthrc = ((mdr_pc_zero_minorsevaluationdeterminanth) + (mdr_nb_zero_minorsevaluationdeterminanth)) * S ((mdr_pc_zero_minorsevaluationdeterminanth) + (mdr_nb_zero_minorsevaluationdeterminanth)) + ((mdr_nb_zero_minorsevaluationdeterminanth) + (mdr_nb_zero_minorsevaluationdeterminanth))) /\ ((mdr_c_zero_minorsevaluationdeterminanthrc = ((mdr_a_zero_minorsevaluationdeterminanthrc) + (mdr_b_zero_minorsevaluationdeterminanthrc)) * S ((mdr_a_zero_minorsevaluationdeterminanthrc) + (mdr_b_zero_minorsevaluationdeterminanthrc)) + ((mdr_b_zero_minorsevaluationdeterminanthrc) + (mdr_b_zero_minorsevaluationdeterminanthrc))) /\ ((mdr_e_zero_minorsevaluationdeterminanthrc = ((mdr_p_zero_minorsevaluationdeterminanth) + (mdr_n_zero_minorsevaluationdeterminanth)) * S ((mdr_p_zero_minorsevaluationdeterminanth) + (mdr_n_zero_minorsevaluationdeterminanth)) + ((mdr_n_zero_minorsevaluationdeterminanth) + (mdr_n_zero_minorsevaluationdeterminanth))) /\ ((mdr_f_zero_minorsevaluationdeterminanthrc = ((mdr_nc_zero_minorsevaluationdeterminanth) + (mdr_e_zero_minorsevaluationdeterminanthrc)) * S ((mdr_nc_zero_minorsevaluationdeterminanth) + (mdr_e_zero_minorsevaluationdeterminanthrc)) + ((mdr_e_zero_minorsevaluationdeterminanthrc) + (mdr_e_zero_minorsevaluationdeterminanthrc))) /\ ((mdr_z_zero_minorsevaluationdeterminanthr) = ((mdr_c_zero_minorsevaluationdeterminanthrc) + (mdr_f_zero_minorsevaluationdeterminanthrc)) * S ((mdr_c_zero_minorsevaluationdeterminanthrc) + (mdr_f_zero_minorsevaluationdeterminanthrc)) + ((mdr_f_zero_minorsevaluationdeterminanthrc) + (mdr_f_zero_minorsevaluationdeterminanthrc))))))))) /\ (((exists ff_h_mdr_zero_minorsevaluationdeterminanthrb. ff_h_mdr_zero_minorsevaluationdeterminanthrb + S (mdr_z_zero_minorsevaluationdeterminanthr) = S ((S (mdr_i_zero_minorsevaluationdeterminanth)) * mdr_c_zero_minorsevaluationdeterminant)) /\ exists ff_q_mdr_zero_minorsevaluationdeterminanthrb. mdr_b_zero_minorsevaluationdeterminant = ff_q_mdr_zero_minorsevaluationdeterminanthrb * S ((S (mdr_i_zero_minorsevaluationdeterminanth)) * mdr_c_zero_minorsevaluationdeterminant) + (mdr_z_zero_minorsevaluationdeterminanthr))))) /\ (((((mdr_d_zero_minorsevaluationdeterminanth) = 0) /\ (((mdr_p_zero_minorsevaluationdeterminanth) = 1) /\ ((mdr_n_zero_minorsevaluationdeterminanth) = 0))) \/ exists mdr_q_zero_minorsevaluationdeterminanths mdr_eb_zero_minorsevaluationdeterminanths mdr_ec_zero_minorsevaluationdeterminanths mdr_fb_zero_minorsevaluationdeterminanths mdr_fc_zero_minorsevaluationdeterminanths. (((mdr_d_zero_minorsevaluationdeterminanth) = S (mdr_q_zero_minorsevaluationdeterminanths)) /\ ((forall mdr_j_zero_minorsevaluationdeterminanthsc. (exists mdr_gap_zero_minorsevaluationdeterminanthscj. mdr_gap_zero_minorsevaluationdeterminanthscj + S (mdr_j_zero_minorsevaluationdeterminanthsc) = (S (mdr_q_zero_minorsevaluationdeterminanths))) -> exists mdr_i_zero_minorsevaluationdeterminanthsc mdr_up_zero_minorsevaluationdeterminanthsc mdr_us_zero_minorsevaluationdeterminanthsc mdr_un_zero_minorsevaluationdeterminanthsc mdr_ut_zero_minorsevaluationdeterminanthsc mdr_p_zero_minorsevaluationdeterminanthsc mdr_n_zero_minorsevaluationdeterminanthsc. ((exists mdr_gap_zero_minorsevaluationdeterminanthsci. mdr_gap_zero_minorsevaluationdeterminanthsci + S (mdr_i_zero_minorsevaluationdeterminanthsc) = (mdr_i_zero_minorsevaluationdeterminanth)) /\ ((exists mdr_z_zero_minorsevaluationdeterminanthscr. ((exists mdr_a_zero_minorsevaluationdeterminanthscrc mdr_b_zero_minorsevaluationdeterminanthscrc mdr_c_zero_minorsevaluationdeterminanthscrc mdr_e_zero_minorsevaluationdeterminanthscrc mdr_f_zero_minorsevaluationdeterminanthscrc. ((mdr_a_zero_minorsevaluationdeterminanthscrc = ((mdr_q_zero_minorsevaluationdeterminanths) + (mdr_up_zero_minorsevaluationdeterminanthsc)) * S ((mdr_q_zero_minorsevaluationdeterminanths) + (mdr_up_zero_minorsevaluationdeterminanthsc)) + ((mdr_up_zero_minorsevaluationdeterminanthsc) + (mdr_up_zero_minorsevaluationdeterminanthsc))) /\ ((mdr_b_zero_minorsevaluationdeterminanthscrc = ((mdr_us_zero_minorsevaluationdeterminanthsc) + (mdr_un_zero_minorsevaluationdeterminanthsc)) * S ((mdr_us_zero_minorsevaluationdeterminanthsc) + (mdr_un_zero_minorsevaluationdeterminanthsc)) + ((mdr_un_zero_minorsevaluationdeterminanthsc) + (mdr_un_zero_minorsevaluationdeterminanthsc))) /\ ((mdr_c_zero_minorsevaluationdeterminanthscrc = ((mdr_a_zero_minorsevaluationdeterminanthscrc) + (mdr_b_zero_minorsevaluationdeterminanthscrc)) * S ((mdr_a_zero_minorsevaluationdeterminanthscrc) + (mdr_b_zero_minorsevaluationdeterminanthscrc)) + ((mdr_b_zero_minorsevaluationdeterminanthscrc) + (mdr_b_zero_minorsevaluationdeterminanthscrc))) /\ ((mdr_e_zero_minorsevaluationdeterminanthscrc = ((mdr_p_zero_minorsevaluationdeterminanthsc) + (mdr_n_zero_minorsevaluationdeterminanthsc)) * S ((mdr_p_zero_minorsevaluationdeterminanthsc) + (mdr_n_zero_minorsevaluationdeterminanthsc)) + ((mdr_n_zero_minorsevaluationdeterminanthsc) + (mdr_n_zero_minorsevaluationdeterminanthsc))) /\ ((mdr_f_zero_minorsevaluationdeterminanthscrc = ((mdr_ut_zero_minorsevaluationdeterminanthsc) + (mdr_e_zero_minorsevaluationdeterminanthscrc)) * S ((mdr_ut_zero_minorsevaluationdeterminanthsc) + (mdr_e_zero_minorsevaluationdeterminanthscrc)) + ((mdr_e_zero_minorsevaluationdeterminanthscrc) + (mdr_e_zero_minorsevaluationdeterminanthscrc))) /\ ((mdr_z_zero_minorsevaluationdeterminanthscr) = ((mdr_c_zero_minorsevaluationdeterminanthscrc) + (mdr_f_zero_minorsevaluationdeterminanthscrc)) * S ((mdr_c_zero_minorsevaluationdeterminanthscrc) + (mdr_f_zero_minorsevaluationdeterminanthscrc)) + ((mdr_f_zero_minorsevaluationdeterminanthscrc) + (mdr_f_zero_minorsevaluationdeterminanthscrc))))))))) /\ (((exists ff_h_mdr_zero_minorsevaluationdeterminanthscrb. ff_h_mdr_zero_minorsevaluationdeterminanthscrb + S (mdr_z_zero_minorsevaluationdeterminanthscr) = S ((S (mdr_i_zero_minorsevaluationdeterminanthsc)) * mdr_c_zero_minorsevaluationdeterminant)) /\ exists ff_q_mdr_zero_minorsevaluationdeterminanthscrb. mdr_b_zero_minorsevaluationdeterminant = ff_q_mdr_zero_minorsevaluationdeterminanthscrb * S ((S (mdr_i_zero_minorsevaluationdeterminanthsc)) * mdr_c_zero_minorsevaluationdeterminant) + (mdr_z_zero_minorsevaluationdeterminanthscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_zero_minorsevaluationdeterminanthscm_positive. (exists ff_gap_mdm_lt_mdr_zero_minorsevaluationdeterminanthscm_positive_index_bound. ff_gap_mdm_lt_mdr_zero_minorsevaluationdeterminanthscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_zero_minorsevaluationdeterminanthscm_positive) = ((mdr_q_zero_minorsevaluationdeterminanths) * (mdr_q_zero_minorsevaluationdeterminanths))) -> exists ff_row_mdm_prefix_mdr_zero_minorsevaluationdeterminanthscm_positive ff_column_mdm_prefix_mdr_zero_minorsevaluationdeterminanthscm_positive ff_value_mdm_prefix_mdr_zero_minorsevaluationdeterminanthscm_positive. (ff_index_mdm_prefix_mdr_zero_minorsevaluationdeterminanthscm_positive = (mdr_q_zero_minorsevaluationdeterminanths) * ff_row_mdm_prefix_mdr_zero_minorsevaluationdeterminanthscm_positive + ff_column_mdm_prefix_mdr_zero_minorsevaluationdeterminanthscm_positive /\ ((exists ff_gap_mdm_lt_mdr_zero_minorsevaluationdeterminanthscm_positive_column_bound. ff_gap_mdm_lt_mdr_zero_minorsevaluationdeterminanthscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_zero_minorsevaluationdeterminanthscm_positive) = (mdr_q_zero_minorsevaluationdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_zero_minorsevaluationdeterminanthscm_positive_cell ff_column_mdm_cell_mdr_zero_minorsevaluationdeterminanthscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_zero_minorsevaluationdeterminanthscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_zero_minorsevaluationdeterminanthscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_zero_minorsevaluationdeterminanthscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_zero_minorsevaluationdeterminanthscm_positive_cell = ff_row_mdm_prefix_mdr_zero_minorsevaluationdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_zero_minorsevaluationdeterminanthscm_positive_cell_row_after. ff_gap_mdm_le_mdr_zero_minorsevaluationdeterminanthscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_zero_minorsevaluationdeterminanthscm_positive)) /\ ff_row_mdm_cell_mdr_zero_minorsevaluationdeterminanthscm_positive_cell = S ff_row_mdm_prefix_mdr_zero_minorsevaluationdeterminanthscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_zero_minorsevaluationdeterminanthscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_zero_minorsevaluationdeterminanthscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_zero_minorsevaluationdeterminanthscm_positive) = (mdr_j_zero_minorsevaluationdeterminanthsc)) /\ ff_column_mdm_cell_mdr_zero_minorsevaluationdeterminanthscm_positive_cell = ff_column_mdm_prefix_mdr_zero_minorsevaluationdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_zero_minorsevaluationdeterminanthscm_positive_cell_column_after. ff_gap_mdm_le_mdr_zero_minorsevaluationdeterminanthscm_positive_cell_column_after + (mdr_j_zero_minorsevaluationdeterminanthsc) = (ff_column_mdm_prefix_mdr_zero_minorsevaluationdeterminanthscm_positive)) /\ ff_column_mdm_cell_mdr_zero_minorsevaluationdeterminanthscm_positive_cell = S ff_column_mdm_prefix_mdr_zero_minorsevaluationdeterminanthscm_positive))) /\ (((exists ff_h_mdm_mdr_zero_minorsevaluationdeterminanthscm_positive_cell_source. ff_h_mdm_mdr_zero_minorsevaluationdeterminanthscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_zero_minorsevaluationdeterminanthscm_positive) = S ((S ((ff_row_mdm_cell_mdr_zero_minorsevaluationdeterminanthscm_positive_cell) * (S (mdr_q_zero_minorsevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_zero_minorsevaluationdeterminanthscm_positive_cell))) * mdr_pc_zero_minorsevaluationdeterminanth)) /\ exists ff_q_mdm_mdr_zero_minorsevaluationdeterminanthscm_positive_cell_source. mdr_pb_zero_minorsevaluationdeterminanth = ff_q_mdm_mdr_zero_minorsevaluationdeterminanthscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_zero_minorsevaluationdeterminanthscm_positive_cell) * (S (mdr_q_zero_minorsevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_zero_minorsevaluationdeterminanthscm_positive_cell))) * mdr_pc_zero_minorsevaluationdeterminanth) + (ff_value_mdm_prefix_mdr_zero_minorsevaluationdeterminanthscm_positive)))))) /\ (((exists ff_h_mdm_mdr_zero_minorsevaluationdeterminanthscm_positive_target. ff_h_mdm_mdr_zero_minorsevaluationdeterminanthscm_positive_target + S (ff_value_mdm_prefix_mdr_zero_minorsevaluationdeterminanthscm_positive) = S ((S (ff_index_mdm_prefix_mdr_zero_minorsevaluationdeterminanthscm_positive)) * mdr_us_zero_minorsevaluationdeterminanthsc)) /\ exists ff_q_mdm_mdr_zero_minorsevaluationdeterminanthscm_positive_target. mdr_up_zero_minorsevaluationdeterminanthsc = ff_q_mdm_mdr_zero_minorsevaluationdeterminanthscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_zero_minorsevaluationdeterminanthscm_positive)) * mdr_us_zero_minorsevaluationdeterminanthsc) + (ff_value_mdm_prefix_mdr_zero_minorsevaluationdeterminanthscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_zero_minorsevaluationdeterminanthscm_negative. (exists ff_gap_mdm_lt_mdr_zero_minorsevaluationdeterminanthscm_negative_index_bound. ff_gap_mdm_lt_mdr_zero_minorsevaluationdeterminanthscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_zero_minorsevaluationdeterminanthscm_negative) = ((mdr_q_zero_minorsevaluationdeterminanths) * (mdr_q_zero_minorsevaluationdeterminanths))) -> exists ff_row_mdm_prefix_mdr_zero_minorsevaluationdeterminanthscm_negative ff_column_mdm_prefix_mdr_zero_minorsevaluationdeterminanthscm_negative ff_value_mdm_prefix_mdr_zero_minorsevaluationdeterminanthscm_negative. (ff_index_mdm_prefix_mdr_zero_minorsevaluationdeterminanthscm_negative = (mdr_q_zero_minorsevaluationdeterminanths) * ff_row_mdm_prefix_mdr_zero_minorsevaluationdeterminanthscm_negative + ff_column_mdm_prefix_mdr_zero_minorsevaluationdeterminanthscm_negative /\ ((exists ff_gap_mdm_lt_mdr_zero_minorsevaluationdeterminanthscm_negative_column_bound. ff_gap_mdm_lt_mdr_zero_minorsevaluationdeterminanthscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_zero_minorsevaluationdeterminanthscm_negative) = (mdr_q_zero_minorsevaluationdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_zero_minorsevaluationdeterminanthscm_negative_cell ff_column_mdm_cell_mdr_zero_minorsevaluationdeterminanthscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_zero_minorsevaluationdeterminanthscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_zero_minorsevaluationdeterminanthscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_zero_minorsevaluationdeterminanthscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_zero_minorsevaluationdeterminanthscm_negative_cell = ff_row_mdm_prefix_mdr_zero_minorsevaluationdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_zero_minorsevaluationdeterminanthscm_negative_cell_row_after. ff_gap_mdm_le_mdr_zero_minorsevaluationdeterminanthscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_zero_minorsevaluationdeterminanthscm_negative)) /\ ff_row_mdm_cell_mdr_zero_minorsevaluationdeterminanthscm_negative_cell = S ff_row_mdm_prefix_mdr_zero_minorsevaluationdeterminanthscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_zero_minorsevaluationdeterminanthscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_zero_minorsevaluationdeterminanthscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_zero_minorsevaluationdeterminanthscm_negative) = (mdr_j_zero_minorsevaluationdeterminanthsc)) /\ ff_column_mdm_cell_mdr_zero_minorsevaluationdeterminanthscm_negative_cell = ff_column_mdm_prefix_mdr_zero_minorsevaluationdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_zero_minorsevaluationdeterminanthscm_negative_cell_column_after. ff_gap_mdm_le_mdr_zero_minorsevaluationdeterminanthscm_negative_cell_column_after + (mdr_j_zero_minorsevaluationdeterminanthsc) = (ff_column_mdm_prefix_mdr_zero_minorsevaluationdeterminanthscm_negative)) /\ ff_column_mdm_cell_mdr_zero_minorsevaluationdeterminanthscm_negative_cell = S ff_column_mdm_prefix_mdr_zero_minorsevaluationdeterminanthscm_negative))) /\ (((exists ff_h_mdm_mdr_zero_minorsevaluationdeterminanthscm_negative_cell_source. ff_h_mdm_mdr_zero_minorsevaluationdeterminanthscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_zero_minorsevaluationdeterminanthscm_negative) = S ((S ((ff_row_mdm_cell_mdr_zero_minorsevaluationdeterminanthscm_negative_cell) * (S (mdr_q_zero_minorsevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_zero_minorsevaluationdeterminanthscm_negative_cell))) * mdr_nc_zero_minorsevaluationdeterminanth)) /\ exists ff_q_mdm_mdr_zero_minorsevaluationdeterminanthscm_negative_cell_source. mdr_nb_zero_minorsevaluationdeterminanth = ff_q_mdm_mdr_zero_minorsevaluationdeterminanthscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_zero_minorsevaluationdeterminanthscm_negative_cell) * (S (mdr_q_zero_minorsevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_zero_minorsevaluationdeterminanthscm_negative_cell))) * mdr_nc_zero_minorsevaluationdeterminanth) + (ff_value_mdm_prefix_mdr_zero_minorsevaluationdeterminanthscm_negative)))))) /\ (((exists ff_h_mdm_mdr_zero_minorsevaluationdeterminanthscm_negative_target. ff_h_mdm_mdr_zero_minorsevaluationdeterminanthscm_negative_target + S (ff_value_mdm_prefix_mdr_zero_minorsevaluationdeterminanthscm_negative) = S ((S (ff_index_mdm_prefix_mdr_zero_minorsevaluationdeterminanthscm_negative)) * mdr_ut_zero_minorsevaluationdeterminanthsc)) /\ exists ff_q_mdm_mdr_zero_minorsevaluationdeterminanthscm_negative_target. mdr_un_zero_minorsevaluationdeterminanthsc = ff_q_mdm_mdr_zero_minorsevaluationdeterminanthscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_zero_minorsevaluationdeterminanthscm_negative)) * mdr_ut_zero_minorsevaluationdeterminanthsc) + (ff_value_mdm_prefix_mdr_zero_minorsevaluationdeterminanthscm_negative))))))))) /\ ((((exists ff_h_mdr_zero_minorsevaluationdeterminanthscp. ff_h_mdr_zero_minorsevaluationdeterminanthscp + S (mdr_p_zero_minorsevaluationdeterminanthsc) = S ((S (mdr_j_zero_minorsevaluationdeterminanthsc)) * mdr_ec_zero_minorsevaluationdeterminanths)) /\ exists ff_q_mdr_zero_minorsevaluationdeterminanthscp. mdr_eb_zero_minorsevaluationdeterminanths = ff_q_mdr_zero_minorsevaluationdeterminanthscp * S ((S (mdr_j_zero_minorsevaluationdeterminanthsc)) * mdr_ec_zero_minorsevaluationdeterminanths) + (mdr_p_zero_minorsevaluationdeterminanthsc))) /\ (((exists ff_h_mdr_zero_minorsevaluationdeterminanthscn. ff_h_mdr_zero_minorsevaluationdeterminanthscn + S (mdr_n_zero_minorsevaluationdeterminanthsc) = S ((S (mdr_j_zero_minorsevaluationdeterminanthsc)) * mdr_fc_zero_minorsevaluationdeterminanths)) /\ exists ff_q_mdr_zero_minorsevaluationdeterminanthscn. mdr_fb_zero_minorsevaluationdeterminanths = ff_q_mdr_zero_minorsevaluationdeterminanthscn * S ((S (mdr_j_zero_minorsevaluationdeterminanthsc)) * mdr_fc_zero_minorsevaluationdeterminanths) + (mdr_n_zero_minorsevaluationdeterminanthsc)))))))) /\ (exists ff_ub_mce_fold_mdr_zero_minorsevaluationdeterminanthsf ff_uc_mce_fold_mdr_zero_minorsevaluationdeterminanthsf ff_vb_mce_fold_mdr_zero_minorsevaluationdeterminanthsf ff_vc_mce_fold_mdr_zero_minorsevaluationdeterminanthsf. ((forall ff_index_mce_alternating_mdr_zero_minorsevaluationdeterminanthsf_prefix. (exists ff_gap_mce_mdr_zero_minorsevaluationdeterminanthsf_prefix_index. ff_gap_mce_mdr_zero_minorsevaluationdeterminanthsf_prefix_index + S (ff_index_mce_alternating_mdr_zero_minorsevaluationdeterminanthsf_prefix) = (S (mdr_q_zero_minorsevaluationdeterminanths))) -> exists ff_ap_mce_alternating_mdr_zero_minorsevaluationdeterminanthsf_prefix ff_an_mce_alternating_mdr_zero_minorsevaluationdeterminanthsf_prefix ff_bp_mce_alternating_mdr_zero_minorsevaluationdeterminanthsf_prefix ff_bn_mce_alternating_mdr_zero_minorsevaluationdeterminanthsf_prefix ff_p_mce_alternating_mdr_zero_minorsevaluationdeterminanthsf_prefix ff_n_mce_alternating_mdr_zero_minorsevaluationdeterminanthsf_prefix. ((((exists ff_h_mce_mdr_zero_minorsevaluationdeterminanthsf_prefix_ap. ff_h_mce_mdr_zero_minorsevaluationdeterminanthsf_prefix_ap + S (ff_ap_mce_alternating_mdr_zero_minorsevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_zero_minorsevaluationdeterminanthsf_prefix)) * mdr_pc_zero_minorsevaluationdeterminanth)) /\ exists ff_q_mce_mdr_zero_minorsevaluationdeterminanthsf_prefix_ap. mdr_pb_zero_minorsevaluationdeterminanth = ff_q_mce_mdr_zero_minorsevaluationdeterminanthsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_zero_minorsevaluationdeterminanthsf_prefix)) * mdr_pc_zero_minorsevaluationdeterminanth) + (ff_ap_mce_alternating_mdr_zero_minorsevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_zero_minorsevaluationdeterminanthsf_prefix_an. ff_h_mce_mdr_zero_minorsevaluationdeterminanthsf_prefix_an + S (ff_an_mce_alternating_mdr_zero_minorsevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_zero_minorsevaluationdeterminanthsf_prefix)) * mdr_nc_zero_minorsevaluationdeterminanth)) /\ exists ff_q_mce_mdr_zero_minorsevaluationdeterminanthsf_prefix_an. mdr_nb_zero_minorsevaluationdeterminanth = ff_q_mce_mdr_zero_minorsevaluationdeterminanthsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_zero_minorsevaluationdeterminanthsf_prefix)) * mdr_nc_zero_minorsevaluationdeterminanth) + (ff_an_mce_alternating_mdr_zero_minorsevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_zero_minorsevaluationdeterminanthsf_prefix_bp. ff_h_mce_mdr_zero_minorsevaluationdeterminanthsf_prefix_bp + S (ff_bp_mce_alternating_mdr_zero_minorsevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_zero_minorsevaluationdeterminanthsf_prefix)) * mdr_ec_zero_minorsevaluationdeterminanths)) /\ exists ff_q_mce_mdr_zero_minorsevaluationdeterminanthsf_prefix_bp. mdr_eb_zero_minorsevaluationdeterminanths = ff_q_mce_mdr_zero_minorsevaluationdeterminanthsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_zero_minorsevaluationdeterminanthsf_prefix)) * mdr_ec_zero_minorsevaluationdeterminanths) + (ff_bp_mce_alternating_mdr_zero_minorsevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_zero_minorsevaluationdeterminanthsf_prefix_bn. ff_h_mce_mdr_zero_minorsevaluationdeterminanthsf_prefix_bn + S (ff_bn_mce_alternating_mdr_zero_minorsevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_zero_minorsevaluationdeterminanthsf_prefix)) * mdr_fc_zero_minorsevaluationdeterminanths)) /\ exists ff_q_mce_mdr_zero_minorsevaluationdeterminanthsf_prefix_bn. mdr_fb_zero_minorsevaluationdeterminanths = ff_q_mce_mdr_zero_minorsevaluationdeterminanthsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_zero_minorsevaluationdeterminanthsf_prefix)) * mdr_fc_zero_minorsevaluationdeterminanths) + (ff_bn_mce_alternating_mdr_zero_minorsevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_zero_minorsevaluationdeterminanthsf_prefix_positive. ff_h_mce_mdr_zero_minorsevaluationdeterminanthsf_prefix_positive + S (ff_p_mce_alternating_mdr_zero_minorsevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_zero_minorsevaluationdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_zero_minorsevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_zero_minorsevaluationdeterminanthsf_prefix_positive. ff_ub_mce_fold_mdr_zero_minorsevaluationdeterminanthsf = ff_q_mce_mdr_zero_minorsevaluationdeterminanthsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_zero_minorsevaluationdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_zero_minorsevaluationdeterminanthsf) + (ff_p_mce_alternating_mdr_zero_minorsevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_zero_minorsevaluationdeterminanthsf_prefix_negative. ff_h_mce_mdr_zero_minorsevaluationdeterminanthsf_prefix_negative + S (ff_n_mce_alternating_mdr_zero_minorsevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_zero_minorsevaluationdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_zero_minorsevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_zero_minorsevaluationdeterminanthsf_prefix_negative. ff_vb_mce_fold_mdr_zero_minorsevaluationdeterminanthsf = ff_q_mce_mdr_zero_minorsevaluationdeterminanthsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_zero_minorsevaluationdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_zero_minorsevaluationdeterminanthsf) + (ff_n_mce_alternating_mdr_zero_minorsevaluationdeterminanthsf_prefix))) /\ (((exists ff_even_mce_term_mdr_zero_minorsevaluationdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_zero_minorsevaluationdeterminanthsf_prefix = 2 * ff_even_mce_term_mdr_zero_minorsevaluationdeterminanthsf_prefix_term) /\ (ff_p_mce_alternating_mdr_zero_minorsevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_zero_minorsevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_zero_minorsevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_zero_minorsevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_zero_minorsevaluationdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_zero_minorsevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_zero_minorsevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_zero_minorsevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_zero_minorsevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_zero_minorsevaluationdeterminanthsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_zero_minorsevaluationdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_zero_minorsevaluationdeterminanthsf_prefix = 2 * ff_odd_mce_term_mdr_zero_minorsevaluationdeterminanthsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_zero_minorsevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_zero_minorsevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_zero_minorsevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_zero_minorsevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_zero_minorsevaluationdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_zero_minorsevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_zero_minorsevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_zero_minorsevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_zero_minorsevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_zero_minorsevaluationdeterminanthsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_zero_minorsevaluationdeterminanthsf_positive ff_v_mce_mdr_zero_minorsevaluationdeterminanthsf_positive. ((((exists ff_h_mce_mdr_zero_minorsevaluationdeterminanthsf_positive_start. ff_h_mce_mdr_zero_minorsevaluationdeterminanthsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_zero_minorsevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_zero_minorsevaluationdeterminanthsf_positive_start. ff_u_mce_mdr_zero_minorsevaluationdeterminanthsf_positive = ff_q_mce_mdr_zero_minorsevaluationdeterminanthsf_positive_start * S ((S (0)) * ff_v_mce_mdr_zero_minorsevaluationdeterminanthsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_zero_minorsevaluationdeterminanthsf_positive_terminal. ff_h_mce_mdr_zero_minorsevaluationdeterminanthsf_positive_terminal + S (mdr_p_zero_minorsevaluationdeterminanth) = S ((S ((S (mdr_q_zero_minorsevaluationdeterminanths)))) * ff_v_mce_mdr_zero_minorsevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_zero_minorsevaluationdeterminanthsf_positive_terminal. ff_u_mce_mdr_zero_minorsevaluationdeterminanthsf_positive = ff_q_mce_mdr_zero_minorsevaluationdeterminanthsf_positive_terminal * S ((S ((S (mdr_q_zero_minorsevaluationdeterminanths)))) * ff_v_mce_mdr_zero_minorsevaluationdeterminanthsf_positive) + (mdr_p_zero_minorsevaluationdeterminanth))) /\ forall ff_i_mce_mdr_zero_minorsevaluationdeterminanthsf_positive. (exists ff_lt_mce_mdr_zero_minorsevaluationdeterminanthsf_positive_bound. ff_lt_mce_mdr_zero_minorsevaluationdeterminanthsf_positive_bound + S ff_i_mce_mdr_zero_minorsevaluationdeterminanthsf_positive = (S (mdr_q_zero_minorsevaluationdeterminanths))) -> exists ff_a_mce_mdr_zero_minorsevaluationdeterminanthsf_positive ff_r_mce_mdr_zero_minorsevaluationdeterminanthsf_positive ff_s_mce_mdr_zero_minorsevaluationdeterminanthsf_positive. ((((exists ff_h_mce_mdr_zero_minorsevaluationdeterminanthsf_positive_summand. ff_h_mce_mdr_zero_minorsevaluationdeterminanthsf_positive_summand + S (ff_a_mce_mdr_zero_minorsevaluationdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_zero_minorsevaluationdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_zero_minorsevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_zero_minorsevaluationdeterminanthsf_positive_summand. ff_ub_mce_fold_mdr_zero_minorsevaluationdeterminanthsf = ff_q_mce_mdr_zero_minorsevaluationdeterminanthsf_positive_summand * S ((S (ff_i_mce_mdr_zero_minorsevaluationdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_zero_minorsevaluationdeterminanthsf) + (ff_a_mce_mdr_zero_minorsevaluationdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_zero_minorsevaluationdeterminanthsf_positive_partial. ff_h_mce_mdr_zero_minorsevaluationdeterminanthsf_positive_partial + S (ff_r_mce_mdr_zero_minorsevaluationdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_zero_minorsevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_zero_minorsevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_zero_minorsevaluationdeterminanthsf_positive_partial. ff_u_mce_mdr_zero_minorsevaluationdeterminanthsf_positive = ff_q_mce_mdr_zero_minorsevaluationdeterminanthsf_positive_partial * S ((S (ff_i_mce_mdr_zero_minorsevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_zero_minorsevaluationdeterminanthsf_positive) + (ff_r_mce_mdr_zero_minorsevaluationdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_zero_minorsevaluationdeterminanthsf_positive_successor. ff_h_mce_mdr_zero_minorsevaluationdeterminanthsf_positive_successor + S (ff_s_mce_mdr_zero_minorsevaluationdeterminanthsf_positive) = S ((S (S ff_i_mce_mdr_zero_minorsevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_zero_minorsevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_zero_minorsevaluationdeterminanthsf_positive_successor. ff_u_mce_mdr_zero_minorsevaluationdeterminanthsf_positive = ff_q_mce_mdr_zero_minorsevaluationdeterminanthsf_positive_successor * S ((S (S ff_i_mce_mdr_zero_minorsevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_zero_minorsevaluationdeterminanthsf_positive) + (ff_s_mce_mdr_zero_minorsevaluationdeterminanthsf_positive))) /\ ff_s_mce_mdr_zero_minorsevaluationdeterminanthsf_positive = ff_r_mce_mdr_zero_minorsevaluationdeterminanthsf_positive + ff_a_mce_mdr_zero_minorsevaluationdeterminanthsf_positive)))))) /\ (exists ff_u_mce_mdr_zero_minorsevaluationdeterminanthsf_negative ff_v_mce_mdr_zero_minorsevaluationdeterminanthsf_negative. ((((exists ff_h_mce_mdr_zero_minorsevaluationdeterminanthsf_negative_start. ff_h_mce_mdr_zero_minorsevaluationdeterminanthsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_zero_minorsevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_zero_minorsevaluationdeterminanthsf_negative_start. ff_u_mce_mdr_zero_minorsevaluationdeterminanthsf_negative = ff_q_mce_mdr_zero_minorsevaluationdeterminanthsf_negative_start * S ((S (0)) * ff_v_mce_mdr_zero_minorsevaluationdeterminanthsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_zero_minorsevaluationdeterminanthsf_negative_terminal. ff_h_mce_mdr_zero_minorsevaluationdeterminanthsf_negative_terminal + S (mdr_n_zero_minorsevaluationdeterminanth) = S ((S ((S (mdr_q_zero_minorsevaluationdeterminanths)))) * ff_v_mce_mdr_zero_minorsevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_zero_minorsevaluationdeterminanthsf_negative_terminal. ff_u_mce_mdr_zero_minorsevaluationdeterminanthsf_negative = ff_q_mce_mdr_zero_minorsevaluationdeterminanthsf_negative_terminal * S ((S ((S (mdr_q_zero_minorsevaluationdeterminanths)))) * ff_v_mce_mdr_zero_minorsevaluationdeterminanthsf_negative) + (mdr_n_zero_minorsevaluationdeterminanth))) /\ forall ff_i_mce_mdr_zero_minorsevaluationdeterminanthsf_negative. (exists ff_lt_mce_mdr_zero_minorsevaluationdeterminanthsf_negative_bound. ff_lt_mce_mdr_zero_minorsevaluationdeterminanthsf_negative_bound + S ff_i_mce_mdr_zero_minorsevaluationdeterminanthsf_negative = (S (mdr_q_zero_minorsevaluationdeterminanths))) -> exists ff_a_mce_mdr_zero_minorsevaluationdeterminanthsf_negative ff_r_mce_mdr_zero_minorsevaluationdeterminanthsf_negative ff_s_mce_mdr_zero_minorsevaluationdeterminanthsf_negative. ((((exists ff_h_mce_mdr_zero_minorsevaluationdeterminanthsf_negative_summand. ff_h_mce_mdr_zero_minorsevaluationdeterminanthsf_negative_summand + S (ff_a_mce_mdr_zero_minorsevaluationdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_zero_minorsevaluationdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_zero_minorsevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_zero_minorsevaluationdeterminanthsf_negative_summand. ff_vb_mce_fold_mdr_zero_minorsevaluationdeterminanthsf = ff_q_mce_mdr_zero_minorsevaluationdeterminanthsf_negative_summand * S ((S (ff_i_mce_mdr_zero_minorsevaluationdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_zero_minorsevaluationdeterminanthsf) + (ff_a_mce_mdr_zero_minorsevaluationdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_zero_minorsevaluationdeterminanthsf_negative_partial. ff_h_mce_mdr_zero_minorsevaluationdeterminanthsf_negative_partial + S (ff_r_mce_mdr_zero_minorsevaluationdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_zero_minorsevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_zero_minorsevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_zero_minorsevaluationdeterminanthsf_negative_partial. ff_u_mce_mdr_zero_minorsevaluationdeterminanthsf_negative = ff_q_mce_mdr_zero_minorsevaluationdeterminanthsf_negative_partial * S ((S (ff_i_mce_mdr_zero_minorsevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_zero_minorsevaluationdeterminanthsf_negative) + (ff_r_mce_mdr_zero_minorsevaluationdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_zero_minorsevaluationdeterminanthsf_negative_successor. ff_h_mce_mdr_zero_minorsevaluationdeterminanthsf_negative_successor + S (ff_s_mce_mdr_zero_minorsevaluationdeterminanthsf_negative) = S ((S (S ff_i_mce_mdr_zero_minorsevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_zero_minorsevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_zero_minorsevaluationdeterminanthsf_negative_successor. ff_u_mce_mdr_zero_minorsevaluationdeterminanthsf_negative = ff_q_mce_mdr_zero_minorsevaluationdeterminanthsf_negative_successor * S ((S (S ff_i_mce_mdr_zero_minorsevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_zero_minorsevaluationdeterminanthsf_negative) + (ff_s_mce_mdr_zero_minorsevaluationdeterminanthsf_negative))) /\ ff_s_mce_mdr_zero_minorsevaluationdeterminanthsf_negative = ff_r_mce_mdr_zero_minorsevaluationdeterminanthsf_negative + ff_a_mce_mdr_zero_minorsevaluationdeterminanthsf_negative))))))))))))))) /\ ((exists mdr_gap_zero_minorsevaluationdeterminanti. mdr_gap_zero_minorsevaluationdeterminanti + S (mdr_i_zero_minorsevaluationdeterminant) = (mdr_l_zero_minorsevaluationdeterminant)) /\ (exists mdr_z_zero_minorsevaluationdeterminantr. ((exists mdr_a_zero_minorsevaluationdeterminantrc mdr_b_zero_minorsevaluationdeterminantrc mdr_c_zero_minorsevaluationdeterminantrc mdr_e_zero_minorsevaluationdeterminantrc mdr_f_zero_minorsevaluationdeterminantrc. ((mdr_a_zero_minorsevaluationdeterminantrc = ((q) + (mdr_ub_zero_minorsevaluation)) * S ((q) + (mdr_ub_zero_minorsevaluation)) + ((mdr_ub_zero_minorsevaluation) + (mdr_ub_zero_minorsevaluation))) /\ ((mdr_b_zero_minorsevaluationdeterminantrc = ((mdr_uc_zero_minorsevaluation) + (mdr_vb_zero_minorsevaluation)) * S ((mdr_uc_zero_minorsevaluation) + (mdr_vb_zero_minorsevaluation)) + ((mdr_vb_zero_minorsevaluation) + (mdr_vb_zero_minorsevaluation))) /\ ((mdr_c_zero_minorsevaluationdeterminantrc = ((mdr_a_zero_minorsevaluationdeterminantrc) + (mdr_b_zero_minorsevaluationdeterminantrc)) * S ((mdr_a_zero_minorsevaluationdeterminantrc) + (mdr_b_zero_minorsevaluationdeterminantrc)) + ((mdr_b_zero_minorsevaluationdeterminantrc) + (mdr_b_zero_minorsevaluationdeterminantrc))) /\ ((mdr_e_zero_minorsevaluationdeterminantrc = ((mdr_p_zero_minors) + (mdr_n_zero_minors)) * S ((mdr_p_zero_minors) + (mdr_n_zero_minors)) + ((mdr_n_zero_minors) + (mdr_n_zero_minors))) /\ ((mdr_f_zero_minorsevaluationdeterminantrc = ((mdr_vc_zero_minorsevaluation) + (mdr_e_zero_minorsevaluationdeterminantrc)) * S ((mdr_vc_zero_minorsevaluation) + (mdr_e_zero_minorsevaluationdeterminantrc)) + ((mdr_e_zero_minorsevaluationdeterminantrc) + (mdr_e_zero_minorsevaluationdeterminantrc))) /\ ((mdr_z_zero_minorsevaluationdeterminantr) = ((mdr_c_zero_minorsevaluationdeterminantrc) + (mdr_f_zero_minorsevaluationdeterminantrc)) * S ((mdr_c_zero_minorsevaluationdeterminantrc) + (mdr_f_zero_minorsevaluationdeterminantrc)) + ((mdr_f_zero_minorsevaluationdeterminantrc) + (mdr_f_zero_minorsevaluationdeterminantrc))))))))) /\ (((exists ff_h_mdr_zero_minorsevaluationdeterminantrb. ff_h_mdr_zero_minorsevaluationdeterminantrb + S (mdr_z_zero_minorsevaluationdeterminantr) = S ((S (mdr_i_zero_minorsevaluationdeterminant)) * mdr_c_zero_minorsevaluationdeterminant)) /\ exists ff_q_mdr_zero_minorsevaluationdeterminantrb. mdr_b_zero_minorsevaluationdeterminant = ff_q_mdr_zero_minorsevaluationdeterminantrb * S ((S (mdr_i_zero_minorsevaluationdeterminant)) * mdr_c_zero_minorsevaluationdeterminant) + (mdr_z_zero_minorsevaluationdeterminantr)))))))))) -> mdr_p_zero_minors = mdr_n_zero_minors) -> ~(exists mdr_rb_forbidden_minor mdr_rc_forbidden_minor mdr_cb_forbidden_minor mdr_cc_forbidden_minor. (((((forall fom_index_mrf_forbidden_minorminorrowsbound. (exists fom_gap_mrf_forbidden_minorminorrowsbound_index_bound. fom_gap_mrf_forbidden_minorminorrowsbound_index_bound + S (fom_index_mrf_forbidden_minorminorrowsbound) = q) -> exists fom_value_mrf_forbidden_minorminorrowsbound. ((((exists fom_beta_height_mrf_forbidden_minorminorrowsbound_entry. fom_beta_height_mrf_forbidden_minorminorrowsbound_entry + S (fom_value_mrf_forbidden_minorminorrowsbound) = S ((S (fom_index_mrf_forbidden_minorminorrowsbound)) * mdr_rc_forbidden_minor)) /\ exists fom_beta_quotient_mrf_forbidden_minorminorrowsbound_entry. mdr_rb_forbidden_minor = fom_beta_quotient_mrf_forbidden_minorminorrowsbound_entry * S ((S (fom_index_mrf_forbidden_minorminorrowsbound)) * mdr_rc_forbidden_minor) + (fom_value_mrf_forbidden_minorminorrowsbound))) /\ (exists fom_gap_mrf_forbidden_minorminorrowsbound_value_bound. fom_gap_mrf_forbidden_minorminorrowsbound_value_bound + S (fom_value_mrf_forbidden_minorminorrowsbound) = r))) /\ (forall mdr_i_forbidden_minorminorrowsdistinct mdr_j_forbidden_minorminorrowsdistinct mdr_a_forbidden_minorminorrowsdistinct. (exists mdr_gap_forbidden_minorminorrowsdistincti. mdr_gap_forbidden_minorminorrowsdistincti + S (mdr_i_forbidden_minorminorrowsdistinct) = (q)) -> (exists mdr_gap_forbidden_minorminorrowsdistinctj. mdr_gap_forbidden_minorminorrowsdistinctj + S (mdr_j_forbidden_minorminorrowsdistinct) = (q)) -> (((exists ff_h_mdr_forbidden_minorminorrowsdistinctfirst. ff_h_mdr_forbidden_minorminorrowsdistinctfirst + S (mdr_a_forbidden_minorminorrowsdistinct) = S ((S (mdr_i_forbidden_minorminorrowsdistinct)) * mdr_rc_forbidden_minor)) /\ exists ff_q_mdr_forbidden_minorminorrowsdistinctfirst. mdr_rb_forbidden_minor = ff_q_mdr_forbidden_minorminorrowsdistinctfirst * S ((S (mdr_i_forbidden_minorminorrowsdistinct)) * mdr_rc_forbidden_minor) + (mdr_a_forbidden_minorminorrowsdistinct))) -> (((exists ff_h_mdr_forbidden_minorminorrowsdistinctsecond. ff_h_mdr_forbidden_minorminorrowsdistinctsecond + S (mdr_a_forbidden_minorminorrowsdistinct) = S ((S (mdr_j_forbidden_minorminorrowsdistinct)) * mdr_rc_forbidden_minor)) /\ exists ff_q_mdr_forbidden_minorminorrowsdistinctsecond. mdr_rb_forbidden_minor = ff_q_mdr_forbidden_minorminorrowsdistinctsecond * S ((S (mdr_j_forbidden_minorminorrowsdistinct)) * mdr_rc_forbidden_minor) + (mdr_a_forbidden_minorminorrowsdistinct))) -> mdr_i_forbidden_minorminorrowsdistinct = mdr_j_forbidden_minorminorrowsdistinct))) /\ ((((forall fom_index_mrf_forbidden_minorminorcolumnsbound. (exists fom_gap_mrf_forbidden_minorminorcolumnsbound_index_bound. fom_gap_mrf_forbidden_minorminorcolumnsbound_index_bound + S (fom_index_mrf_forbidden_minorminorcolumnsbound) = q) -> exists fom_value_mrf_forbidden_minorminorcolumnsbound. ((((exists fom_beta_height_mrf_forbidden_minorminorcolumnsbound_entry. fom_beta_height_mrf_forbidden_minorminorcolumnsbound_entry + S (fom_value_mrf_forbidden_minorminorcolumnsbound) = S ((S (fom_index_mrf_forbidden_minorminorcolumnsbound)) * mdr_cc_forbidden_minor)) /\ exists fom_beta_quotient_mrf_forbidden_minorminorcolumnsbound_entry. mdr_cb_forbidden_minor = fom_beta_quotient_mrf_forbidden_minorminorcolumnsbound_entry * S ((S (fom_index_mrf_forbidden_minorminorcolumnsbound)) * mdr_cc_forbidden_minor) + (fom_value_mrf_forbidden_minorminorcolumnsbound))) /\ (exists fom_gap_mrf_forbidden_minorminorcolumnsbound_value_bound. fom_gap_mrf_forbidden_minorminorcolumnsbound_value_bound + S (fom_value_mrf_forbidden_minorminorcolumnsbound) = w))) /\ (forall mdr_i_forbidden_minorminorcolumnsdistinct mdr_j_forbidden_minorminorcolumnsdistinct mdr_a_forbidden_minorminorcolumnsdistinct. (exists mdr_gap_forbidden_minorminorcolumnsdistincti. mdr_gap_forbidden_minorminorcolumnsdistincti + S (mdr_i_forbidden_minorminorcolumnsdistinct) = (q)) -> (exists mdr_gap_forbidden_minorminorcolumnsdistinctj. mdr_gap_forbidden_minorminorcolumnsdistinctj + S (mdr_j_forbidden_minorminorcolumnsdistinct) = (q)) -> (((exists ff_h_mdr_forbidden_minorminorcolumnsdistinctfirst. ff_h_mdr_forbidden_minorminorcolumnsdistinctfirst + S (mdr_a_forbidden_minorminorcolumnsdistinct) = S ((S (mdr_i_forbidden_minorminorcolumnsdistinct)) * mdr_cc_forbidden_minor)) /\ exists ff_q_mdr_forbidden_minorminorcolumnsdistinctfirst. mdr_cb_forbidden_minor = ff_q_mdr_forbidden_minorminorcolumnsdistinctfirst * S ((S (mdr_i_forbidden_minorminorcolumnsdistinct)) * mdr_cc_forbidden_minor) + (mdr_a_forbidden_minorminorcolumnsdistinct))) -> (((exists ff_h_mdr_forbidden_minorminorcolumnsdistinctsecond. ff_h_mdr_forbidden_minorminorcolumnsdistinctsecond + S (mdr_a_forbidden_minorminorcolumnsdistinct) = S ((S (mdr_j_forbidden_minorminorcolumnsdistinct)) * mdr_cc_forbidden_minor)) /\ exists ff_q_mdr_forbidden_minorminorcolumnsdistinctsecond. mdr_cb_forbidden_minor = ff_q_mdr_forbidden_minorminorcolumnsdistinctsecond * S ((S (mdr_j_forbidden_minorminorcolumnsdistinct)) * mdr_cc_forbidden_minor) + (mdr_a_forbidden_minorminorcolumnsdistinct))) -> mdr_i_forbidden_minorminorcolumnsdistinct = mdr_j_forbidden_minorminorcolumnsdistinct))) /\ (exists mdr_p_forbidden_minorminornonzero mdr_n_forbidden_minorminornonzero. ((exists mdr_ub_forbidden_minorminornonzeroevaluation mdr_uc_forbidden_minorminornonzeroevaluation mdr_vb_forbidden_minorminornonzeroevaluation mdr_vc_forbidden_minorminornonzeroevaluation. ((((forall mdr_i_forbidden_minorminornonzeroevaluationmatrixpositive. (exists mdr_gap_forbidden_minorminornonzeroevaluationmatrixpositivebound. mdr_gap_forbidden_minorminornonzeroevaluationmatrixpositivebound + S (mdr_i_forbidden_minorminornonzeroevaluationmatrixpositive) = ((q) * (q))) -> exists mdr_a_forbidden_minorminornonzeroevaluationmatrixpositive. (((exists mdr_r_forbidden_minorminornonzeroevaluationmatrixpositivepoint mdr_s_forbidden_minorminornonzeroevaluationmatrixpositivepoint mdr_u_forbidden_minorminornonzeroevaluationmatrixpositivepoint mdr_v_forbidden_minorminornonzeroevaluationmatrixpositivepoint. ((mdr_i_forbidden_minorminornonzeroevaluationmatrixpositive = (q) * mdr_r_forbidden_minorminornonzeroevaluationmatrixpositivepoint + mdr_s_forbidden_minorminornonzeroevaluationmatrixpositivepoint) /\ ((exists mdr_gap_forbidden_minorminornonzeroevaluationmatrixpositivepointcolumn. mdr_gap_forbidden_minorminornonzeroevaluationmatrixpositivepointcolumn + S (mdr_s_forbidden_minorminornonzeroevaluationmatrixpositivepoint) = (q)) /\ ((((exists ff_h_mdr_forbidden_minorminornonzeroevaluationmatrixpositivepointrow_index. ff_h_mdr_forbidden_minorminornonzeroevaluationmatrixpositivepointrow_index + S (mdr_u_forbidden_minorminornonzeroevaluationmatrixpositivepoint) = S ((S (mdr_r_forbidden_minorminornonzeroevaluationmatrixpositivepoint)) * mdr_rc_forbidden_minor)) /\ exists ff_q_mdr_forbidden_minorminornonzeroevaluationmatrixpositivepointrow_index. mdr_rb_forbidden_minor = ff_q_mdr_forbidden_minorminornonzeroevaluationmatrixpositivepointrow_index * S ((S (mdr_r_forbidden_minorminornonzeroevaluationmatrixpositivepoint)) * mdr_rc_forbidden_minor) + (mdr_u_forbidden_minorminornonzeroevaluationmatrixpositivepoint))) /\ ((((exists ff_h_mdr_forbidden_minorminornonzeroevaluationmatrixpositivepointcolumn_index. ff_h_mdr_forbidden_minorminornonzeroevaluationmatrixpositivepointcolumn_index + S (mdr_v_forbidden_minorminornonzeroevaluationmatrixpositivepoint) = S ((S (mdr_s_forbidden_minorminornonzeroevaluationmatrixpositivepoint)) * mdr_cc_forbidden_minor)) /\ exists ff_q_mdr_forbidden_minorminornonzeroevaluationmatrixpositivepointcolumn_index. mdr_cb_forbidden_minor = ff_q_mdr_forbidden_minorminornonzeroevaluationmatrixpositivepointcolumn_index * S ((S (mdr_s_forbidden_minorminornonzeroevaluationmatrixpositivepoint)) * mdr_cc_forbidden_minor) + (mdr_v_forbidden_minorminornonzeroevaluationmatrixpositivepoint))) /\ (((exists ff_h_mdr_forbidden_minorminornonzeroevaluationmatrixpositivepointsource. ff_h_mdr_forbidden_minorminornonzeroevaluationmatrixpositivepointsource + S (mdr_a_forbidden_minorminornonzeroevaluationmatrixpositive) = S ((S ((mdr_u_forbidden_minorminornonzeroevaluationmatrixpositivepoint) * (w) + (mdr_v_forbidden_minorminornonzeroevaluationmatrixpositivepoint))) * pc)) /\ exists ff_q_mdr_forbidden_minorminornonzeroevaluationmatrixpositivepointsource. pb = ff_q_mdr_forbidden_minorminornonzeroevaluationmatrixpositivepointsource * S ((S ((mdr_u_forbidden_minorminornonzeroevaluationmatrixpositivepoint) * (w) + (mdr_v_forbidden_minorminornonzeroevaluationmatrixpositivepoint))) * pc) + (mdr_a_forbidden_minorminornonzeroevaluationmatrixpositive)))))))) /\ (((exists ff_h_mdr_forbidden_minorminornonzeroevaluationmatrixpositiveoutput. ff_h_mdr_forbidden_minorminornonzeroevaluationmatrixpositiveoutput + S (mdr_a_forbidden_minorminornonzeroevaluationmatrixpositive) = S ((S (mdr_i_forbidden_minorminornonzeroevaluationmatrixpositive)) * mdr_uc_forbidden_minorminornonzeroevaluation)) /\ exists ff_q_mdr_forbidden_minorminornonzeroevaluationmatrixpositiveoutput. mdr_ub_forbidden_minorminornonzeroevaluation = ff_q_mdr_forbidden_minorminornonzeroevaluationmatrixpositiveoutput * S ((S (mdr_i_forbidden_minorminornonzeroevaluationmatrixpositive)) * mdr_uc_forbidden_minorminornonzeroevaluation) + (mdr_a_forbidden_minorminornonzeroevaluationmatrixpositive)))))) /\ (forall mdr_i_forbidden_minorminornonzeroevaluationmatrixnegative. (exists mdr_gap_forbidden_minorminornonzeroevaluationmatrixnegativebound. mdr_gap_forbidden_minorminornonzeroevaluationmatrixnegativebound + S (mdr_i_forbidden_minorminornonzeroevaluationmatrixnegative) = ((q) * (q))) -> exists mdr_a_forbidden_minorminornonzeroevaluationmatrixnegative. (((exists mdr_r_forbidden_minorminornonzeroevaluationmatrixnegativepoint mdr_s_forbidden_minorminornonzeroevaluationmatrixnegativepoint mdr_u_forbidden_minorminornonzeroevaluationmatrixnegativepoint mdr_v_forbidden_minorminornonzeroevaluationmatrixnegativepoint. ((mdr_i_forbidden_minorminornonzeroevaluationmatrixnegative = (q) * mdr_r_forbidden_minorminornonzeroevaluationmatrixnegativepoint + mdr_s_forbidden_minorminornonzeroevaluationmatrixnegativepoint) /\ ((exists mdr_gap_forbidden_minorminornonzeroevaluationmatrixnegativepointcolumn. mdr_gap_forbidden_minorminornonzeroevaluationmatrixnegativepointcolumn + S (mdr_s_forbidden_minorminornonzeroevaluationmatrixnegativepoint) = (q)) /\ ((((exists ff_h_mdr_forbidden_minorminornonzeroevaluationmatrixnegativepointrow_index. ff_h_mdr_forbidden_minorminornonzeroevaluationmatrixnegativepointrow_index + S (mdr_u_forbidden_minorminornonzeroevaluationmatrixnegativepoint) = S ((S (mdr_r_forbidden_minorminornonzeroevaluationmatrixnegativepoint)) * mdr_rc_forbidden_minor)) /\ exists ff_q_mdr_forbidden_minorminornonzeroevaluationmatrixnegativepointrow_index. mdr_rb_forbidden_minor = ff_q_mdr_forbidden_minorminornonzeroevaluationmatrixnegativepointrow_index * S ((S (mdr_r_forbidden_minorminornonzeroevaluationmatrixnegativepoint)) * mdr_rc_forbidden_minor) + (mdr_u_forbidden_minorminornonzeroevaluationmatrixnegativepoint))) /\ ((((exists ff_h_mdr_forbidden_minorminornonzeroevaluationmatrixnegativepointcolumn_index. ff_h_mdr_forbidden_minorminornonzeroevaluationmatrixnegativepointcolumn_index + S (mdr_v_forbidden_minorminornonzeroevaluationmatrixnegativepoint) = S ((S (mdr_s_forbidden_minorminornonzeroevaluationmatrixnegativepoint)) * mdr_cc_forbidden_minor)) /\ exists ff_q_mdr_forbidden_minorminornonzeroevaluationmatrixnegativepointcolumn_index. mdr_cb_forbidden_minor = ff_q_mdr_forbidden_minorminornonzeroevaluationmatrixnegativepointcolumn_index * S ((S (mdr_s_forbidden_minorminornonzeroevaluationmatrixnegativepoint)) * mdr_cc_forbidden_minor) + (mdr_v_forbidden_minorminornonzeroevaluationmatrixnegativepoint))) /\ (((exists ff_h_mdr_forbidden_minorminornonzeroevaluationmatrixnegativepointsource. ff_h_mdr_forbidden_minorminornonzeroevaluationmatrixnegativepointsource + S (mdr_a_forbidden_minorminornonzeroevaluationmatrixnegative) = S ((S ((mdr_u_forbidden_minorminornonzeroevaluationmatrixnegativepoint) * (w) + (mdr_v_forbidden_minorminornonzeroevaluationmatrixnegativepoint))) * nc)) /\ exists ff_q_mdr_forbidden_minorminornonzeroevaluationmatrixnegativepointsource. nb = ff_q_mdr_forbidden_minorminornonzeroevaluationmatrixnegativepointsource * S ((S ((mdr_u_forbidden_minorminornonzeroevaluationmatrixnegativepoint) * (w) + (mdr_v_forbidden_minorminornonzeroevaluationmatrixnegativepoint))) * nc) + (mdr_a_forbidden_minorminornonzeroevaluationmatrixnegative)))))))) /\ (((exists ff_h_mdr_forbidden_minorminornonzeroevaluationmatrixnegativeoutput. ff_h_mdr_forbidden_minorminornonzeroevaluationmatrixnegativeoutput + S (mdr_a_forbidden_minorminornonzeroevaluationmatrixnegative) = S ((S (mdr_i_forbidden_minorminornonzeroevaluationmatrixnegative)) * mdr_vc_forbidden_minorminornonzeroevaluation)) /\ exists ff_q_mdr_forbidden_minorminornonzeroevaluationmatrixnegativeoutput. mdr_vb_forbidden_minorminornonzeroevaluation = ff_q_mdr_forbidden_minorminornonzeroevaluationmatrixnegativeoutput * S ((S (mdr_i_forbidden_minorminornonzeroevaluationmatrixnegative)) * mdr_vc_forbidden_minorminornonzeroevaluation) + (mdr_a_forbidden_minorminornonzeroevaluationmatrixnegative)))))))) /\ (exists mdr_b_forbidden_minorminornonzeroevaluationdeterminant mdr_c_forbidden_minorminornonzeroevaluationdeterminant mdr_l_forbidden_minorminornonzeroevaluationdeterminant mdr_i_forbidden_minorminornonzeroevaluationdeterminant. ((forall mdr_i_forbidden_minorminornonzeroevaluationdeterminanth. (exists mdr_gap_forbidden_minorminornonzeroevaluationdeterminanthi. mdr_gap_forbidden_minorminornonzeroevaluationdeterminanthi + S (mdr_i_forbidden_minorminornonzeroevaluationdeterminanth) = (mdr_l_forbidden_minorminornonzeroevaluationdeterminant)) -> exists mdr_d_forbidden_minorminornonzeroevaluationdeterminanth mdr_pb_forbidden_minorminornonzeroevaluationdeterminanth mdr_pc_forbidden_minorminornonzeroevaluationdeterminanth mdr_nb_forbidden_minorminornonzeroevaluationdeterminanth mdr_nc_forbidden_minorminornonzeroevaluationdeterminanth mdr_p_forbidden_minorminornonzeroevaluationdeterminanth mdr_n_forbidden_minorminornonzeroevaluationdeterminanth. ((exists mdr_z_forbidden_minorminornonzeroevaluationdeterminanthr. ((exists mdr_a_forbidden_minorminornonzeroevaluationdeterminanthrc mdr_b_forbidden_minorminornonzeroevaluationdeterminanthrc mdr_c_forbidden_minorminornonzeroevaluationdeterminanthrc mdr_e_forbidden_minorminornonzeroevaluationdeterminanthrc mdr_f_forbidden_minorminornonzeroevaluationdeterminanthrc. ((mdr_a_forbidden_minorminornonzeroevaluationdeterminanthrc = ((mdr_d_forbidden_minorminornonzeroevaluationdeterminanth) + (mdr_pb_forbidden_minorminornonzeroevaluationdeterminanth)) * S ((mdr_d_forbidden_minorminornonzeroevaluationdeterminanth) + (mdr_pb_forbidden_minorminornonzeroevaluationdeterminanth)) + ((mdr_pb_forbidden_minorminornonzeroevaluationdeterminanth) + (mdr_pb_forbidden_minorminornonzeroevaluationdeterminanth))) /\ ((mdr_b_forbidden_minorminornonzeroevaluationdeterminanthrc = ((mdr_pc_forbidden_minorminornonzeroevaluationdeterminanth) + (mdr_nb_forbidden_minorminornonzeroevaluationdeterminanth)) * S ((mdr_pc_forbidden_minorminornonzeroevaluationdeterminanth) + (mdr_nb_forbidden_minorminornonzeroevaluationdeterminanth)) + ((mdr_nb_forbidden_minorminornonzeroevaluationdeterminanth) + (mdr_nb_forbidden_minorminornonzeroevaluationdeterminanth))) /\ ((mdr_c_forbidden_minorminornonzeroevaluationdeterminanthrc = ((mdr_a_forbidden_minorminornonzeroevaluationdeterminanthrc) + (mdr_b_forbidden_minorminornonzeroevaluationdeterminanthrc)) * S ((mdr_a_forbidden_minorminornonzeroevaluationdeterminanthrc) + (mdr_b_forbidden_minorminornonzeroevaluationdeterminanthrc)) + ((mdr_b_forbidden_minorminornonzeroevaluationdeterminanthrc) + (mdr_b_forbidden_minorminornonzeroevaluationdeterminanthrc))) /\ ((mdr_e_forbidden_minorminornonzeroevaluationdeterminanthrc = ((mdr_p_forbidden_minorminornonzeroevaluationdeterminanth) + (mdr_n_forbidden_minorminornonzeroevaluationdeterminanth)) * S ((mdr_p_forbidden_minorminornonzeroevaluationdeterminanth) + (mdr_n_forbidden_minorminornonzeroevaluationdeterminanth)) + ((mdr_n_forbidden_minorminornonzeroevaluationdeterminanth) + (mdr_n_forbidden_minorminornonzeroevaluationdeterminanth))) /\ ((mdr_f_forbidden_minorminornonzeroevaluationdeterminanthrc = ((mdr_nc_forbidden_minorminornonzeroevaluationdeterminanth) + (mdr_e_forbidden_minorminornonzeroevaluationdeterminanthrc)) * S ((mdr_nc_forbidden_minorminornonzeroevaluationdeterminanth) + (mdr_e_forbidden_minorminornonzeroevaluationdeterminanthrc)) + ((mdr_e_forbidden_minorminornonzeroevaluationdeterminanthrc) + (mdr_e_forbidden_minorminornonzeroevaluationdeterminanthrc))) /\ ((mdr_z_forbidden_minorminornonzeroevaluationdeterminanthr) = ((mdr_c_forbidden_minorminornonzeroevaluationdeterminanthrc) + (mdr_f_forbidden_minorminornonzeroevaluationdeterminanthrc)) * S ((mdr_c_forbidden_minorminornonzeroevaluationdeterminanthrc) + (mdr_f_forbidden_minorminornonzeroevaluationdeterminanthrc)) + ((mdr_f_forbidden_minorminornonzeroevaluationdeterminanthrc) + (mdr_f_forbidden_minorminornonzeroevaluationdeterminanthrc))))))))) /\ (((exists ff_h_mdr_forbidden_minorminornonzeroevaluationdeterminanthrb. ff_h_mdr_forbidden_minorminornonzeroevaluationdeterminanthrb + S (mdr_z_forbidden_minorminornonzeroevaluationdeterminanthr) = S ((S (mdr_i_forbidden_minorminornonzeroevaluationdeterminanth)) * mdr_c_forbidden_minorminornonzeroevaluationdeterminant)) /\ exists ff_q_mdr_forbidden_minorminornonzeroevaluationdeterminanthrb. mdr_b_forbidden_minorminornonzeroevaluationdeterminant = ff_q_mdr_forbidden_minorminornonzeroevaluationdeterminanthrb * S ((S (mdr_i_forbidden_minorminornonzeroevaluationdeterminanth)) * mdr_c_forbidden_minorminornonzeroevaluationdeterminant) + (mdr_z_forbidden_minorminornonzeroevaluationdeterminanthr))))) /\ (((((mdr_d_forbidden_minorminornonzeroevaluationdeterminanth) = 0) /\ (((mdr_p_forbidden_minorminornonzeroevaluationdeterminanth) = 1) /\ ((mdr_n_forbidden_minorminornonzeroevaluationdeterminanth) = 0))) \/ exists mdr_q_forbidden_minorminornonzeroevaluationdeterminanths mdr_eb_forbidden_minorminornonzeroevaluationdeterminanths mdr_ec_forbidden_minorminornonzeroevaluationdeterminanths mdr_fb_forbidden_minorminornonzeroevaluationdeterminanths mdr_fc_forbidden_minorminornonzeroevaluationdeterminanths. (((mdr_d_forbidden_minorminornonzeroevaluationdeterminanth) = S (mdr_q_forbidden_minorminornonzeroevaluationdeterminanths)) /\ ((forall mdr_j_forbidden_minorminornonzeroevaluationdeterminanthsc. (exists mdr_gap_forbidden_minorminornonzeroevaluationdeterminanthscj. mdr_gap_forbidden_minorminornonzeroevaluationdeterminanthscj + S (mdr_j_forbidden_minorminornonzeroevaluationdeterminanthsc) = (S (mdr_q_forbidden_minorminornonzeroevaluationdeterminanths))) -> exists mdr_i_forbidden_minorminornonzeroevaluationdeterminanthsc mdr_up_forbidden_minorminornonzeroevaluationdeterminanthsc mdr_us_forbidden_minorminornonzeroevaluationdeterminanthsc mdr_un_forbidden_minorminornonzeroevaluationdeterminanthsc mdr_ut_forbidden_minorminornonzeroevaluationdeterminanthsc mdr_p_forbidden_minorminornonzeroevaluationdeterminanthsc mdr_n_forbidden_minorminornonzeroevaluationdeterminanthsc. ((exists mdr_gap_forbidden_minorminornonzeroevaluationdeterminanthsci. mdr_gap_forbidden_minorminornonzeroevaluationdeterminanthsci + S (mdr_i_forbidden_minorminornonzeroevaluationdeterminanthsc) = (mdr_i_forbidden_minorminornonzeroevaluationdeterminanth)) /\ ((exists mdr_z_forbidden_minorminornonzeroevaluationdeterminanthscr. ((exists mdr_a_forbidden_minorminornonzeroevaluationdeterminanthscrc mdr_b_forbidden_minorminornonzeroevaluationdeterminanthscrc mdr_c_forbidden_minorminornonzeroevaluationdeterminanthscrc mdr_e_forbidden_minorminornonzeroevaluationdeterminanthscrc mdr_f_forbidden_minorminornonzeroevaluationdeterminanthscrc. ((mdr_a_forbidden_minorminornonzeroevaluationdeterminanthscrc = ((mdr_q_forbidden_minorminornonzeroevaluationdeterminanths) + (mdr_up_forbidden_minorminornonzeroevaluationdeterminanthsc)) * S ((mdr_q_forbidden_minorminornonzeroevaluationdeterminanths) + (mdr_up_forbidden_minorminornonzeroevaluationdeterminanthsc)) + ((mdr_up_forbidden_minorminornonzeroevaluationdeterminanthsc) + (mdr_up_forbidden_minorminornonzeroevaluationdeterminanthsc))) /\ ((mdr_b_forbidden_minorminornonzeroevaluationdeterminanthscrc = ((mdr_us_forbidden_minorminornonzeroevaluationdeterminanthsc) + (mdr_un_forbidden_minorminornonzeroevaluationdeterminanthsc)) * S ((mdr_us_forbidden_minorminornonzeroevaluationdeterminanthsc) + (mdr_un_forbidden_minorminornonzeroevaluationdeterminanthsc)) + ((mdr_un_forbidden_minorminornonzeroevaluationdeterminanthsc) + (mdr_un_forbidden_minorminornonzeroevaluationdeterminanthsc))) /\ ((mdr_c_forbidden_minorminornonzeroevaluationdeterminanthscrc = ((mdr_a_forbidden_minorminornonzeroevaluationdeterminanthscrc) + (mdr_b_forbidden_minorminornonzeroevaluationdeterminanthscrc)) * S ((mdr_a_forbidden_minorminornonzeroevaluationdeterminanthscrc) + (mdr_b_forbidden_minorminornonzeroevaluationdeterminanthscrc)) + ((mdr_b_forbidden_minorminornonzeroevaluationdeterminanthscrc) + (mdr_b_forbidden_minorminornonzeroevaluationdeterminanthscrc))) /\ ((mdr_e_forbidden_minorminornonzeroevaluationdeterminanthscrc = ((mdr_p_forbidden_minorminornonzeroevaluationdeterminanthsc) + (mdr_n_forbidden_minorminornonzeroevaluationdeterminanthsc)) * S ((mdr_p_forbidden_minorminornonzeroevaluationdeterminanthsc) + (mdr_n_forbidden_minorminornonzeroevaluationdeterminanthsc)) + ((mdr_n_forbidden_minorminornonzeroevaluationdeterminanthsc) + (mdr_n_forbidden_minorminornonzeroevaluationdeterminanthsc))) /\ ((mdr_f_forbidden_minorminornonzeroevaluationdeterminanthscrc = ((mdr_ut_forbidden_minorminornonzeroevaluationdeterminanthsc) + (mdr_e_forbidden_minorminornonzeroevaluationdeterminanthscrc)) * S ((mdr_ut_forbidden_minorminornonzeroevaluationdeterminanthsc) + (mdr_e_forbidden_minorminornonzeroevaluationdeterminanthscrc)) + ((mdr_e_forbidden_minorminornonzeroevaluationdeterminanthscrc) + (mdr_e_forbidden_minorminornonzeroevaluationdeterminanthscrc))) /\ ((mdr_z_forbidden_minorminornonzeroevaluationdeterminanthscr) = ((mdr_c_forbidden_minorminornonzeroevaluationdeterminanthscrc) + (mdr_f_forbidden_minorminornonzeroevaluationdeterminanthscrc)) * S ((mdr_c_forbidden_minorminornonzeroevaluationdeterminanthscrc) + (mdr_f_forbidden_minorminornonzeroevaluationdeterminanthscrc)) + ((mdr_f_forbidden_minorminornonzeroevaluationdeterminanthscrc) + (mdr_f_forbidden_minorminornonzeroevaluationdeterminanthscrc))))))))) /\ (((exists ff_h_mdr_forbidden_minorminornonzeroevaluationdeterminanthscrb. ff_h_mdr_forbidden_minorminornonzeroevaluationdeterminanthscrb + S (mdr_z_forbidden_minorminornonzeroevaluationdeterminanthscr) = S ((S (mdr_i_forbidden_minorminornonzeroevaluationdeterminanthsc)) * mdr_c_forbidden_minorminornonzeroevaluationdeterminant)) /\ exists ff_q_mdr_forbidden_minorminornonzeroevaluationdeterminanthscrb. mdr_b_forbidden_minorminornonzeroevaluationdeterminant = ff_q_mdr_forbidden_minorminornonzeroevaluationdeterminanthscrb * S ((S (mdr_i_forbidden_minorminornonzeroevaluationdeterminanthsc)) * mdr_c_forbidden_minorminornonzeroevaluationdeterminant) + (mdr_z_forbidden_minorminornonzeroevaluationdeterminanthscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_forbidden_minorminornonzeroevaluationdeterminanthscm_positive. (exists ff_gap_mdm_lt_mdr_forbidden_minorminornonzeroevaluationdeterminanthscm_positive_index_bound. ff_gap_mdm_lt_mdr_forbidden_minorminornonzeroevaluationdeterminanthscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_forbidden_minorminornonzeroevaluationdeterminanthscm_positive) = ((mdr_q_forbidden_minorminornonzeroevaluationdeterminanths) * (mdr_q_forbidden_minorminornonzeroevaluationdeterminanths))) -> exists ff_row_mdm_prefix_mdr_forbidden_minorminornonzeroevaluationdeterminanthscm_positive ff_column_mdm_prefix_mdr_forbidden_minorminornonzeroevaluationdeterminanthscm_positive ff_value_mdm_prefix_mdr_forbidden_minorminornonzeroevaluationdeterminanthscm_positive. (ff_index_mdm_prefix_mdr_forbidden_minorminornonzeroevaluationdeterminanthscm_positive = (mdr_q_forbidden_minorminornonzeroevaluationdeterminanths) * ff_row_mdm_prefix_mdr_forbidden_minorminornonzeroevaluationdeterminanthscm_positive + ff_column_mdm_prefix_mdr_forbidden_minorminornonzeroevaluationdeterminanthscm_positive /\ ((exists ff_gap_mdm_lt_mdr_forbidden_minorminornonzeroevaluationdeterminanthscm_positive_column_bound. ff_gap_mdm_lt_mdr_forbidden_minorminornonzeroevaluationdeterminanthscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_forbidden_minorminornonzeroevaluationdeterminanthscm_positive) = (mdr_q_forbidden_minorminornonzeroevaluationdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_forbidden_minorminornonzeroevaluationdeterminanthscm_positive_cell ff_column_mdm_cell_mdr_forbidden_minorminornonzeroevaluationdeterminanthscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_forbidden_minorminornonzeroevaluationdeterminanthscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_forbidden_minorminornonzeroevaluationdeterminanthscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_forbidden_minorminornonzeroevaluationdeterminanthscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_forbidden_minorminornonzeroevaluationdeterminanthscm_positive_cell = ff_row_mdm_prefix_mdr_forbidden_minorminornonzeroevaluationdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_forbidden_minorminornonzeroevaluationdeterminanthscm_positive_cell_row_after. ff_gap_mdm_le_mdr_forbidden_minorminornonzeroevaluationdeterminanthscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_forbidden_minorminornonzeroevaluationdeterminanthscm_positive)) /\ ff_row_mdm_cell_mdr_forbidden_minorminornonzeroevaluationdeterminanthscm_positive_cell = S ff_row_mdm_prefix_mdr_forbidden_minorminornonzeroevaluationdeterminanthscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_forbidden_minorminornonzeroevaluationdeterminanthscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_forbidden_minorminornonzeroevaluationdeterminanthscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_forbidden_minorminornonzeroevaluationdeterminanthscm_positive) = (mdr_j_forbidden_minorminornonzeroevaluationdeterminanthsc)) /\ ff_column_mdm_cell_mdr_forbidden_minorminornonzeroevaluationdeterminanthscm_positive_cell = ff_column_mdm_prefix_mdr_forbidden_minorminornonzeroevaluationdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_forbidden_minorminornonzeroevaluationdeterminanthscm_positive_cell_column_after. ff_gap_mdm_le_mdr_forbidden_minorminornonzeroevaluationdeterminanthscm_positive_cell_column_after + (mdr_j_forbidden_minorminornonzeroevaluationdeterminanthsc) = (ff_column_mdm_prefix_mdr_forbidden_minorminornonzeroevaluationdeterminanthscm_positive)) /\ ff_column_mdm_cell_mdr_forbidden_minorminornonzeroevaluationdeterminanthscm_positive_cell = S ff_column_mdm_prefix_mdr_forbidden_minorminornonzeroevaluationdeterminanthscm_positive))) /\ (((exists ff_h_mdm_mdr_forbidden_minorminornonzeroevaluationdeterminanthscm_positive_cell_source. ff_h_mdm_mdr_forbidden_minorminornonzeroevaluationdeterminanthscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_forbidden_minorminornonzeroevaluationdeterminanthscm_positive) = S ((S ((ff_row_mdm_cell_mdr_forbidden_minorminornonzeroevaluationdeterminanthscm_positive_cell) * (S (mdr_q_forbidden_minorminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_forbidden_minorminornonzeroevaluationdeterminanthscm_positive_cell))) * mdr_pc_forbidden_minorminornonzeroevaluationdeterminanth)) /\ exists ff_q_mdm_mdr_forbidden_minorminornonzeroevaluationdeterminanthscm_positive_cell_source. mdr_pb_forbidden_minorminornonzeroevaluationdeterminanth = ff_q_mdm_mdr_forbidden_minorminornonzeroevaluationdeterminanthscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_forbidden_minorminornonzeroevaluationdeterminanthscm_positive_cell) * (S (mdr_q_forbidden_minorminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_forbidden_minorminornonzeroevaluationdeterminanthscm_positive_cell))) * mdr_pc_forbidden_minorminornonzeroevaluationdeterminanth) + (ff_value_mdm_prefix_mdr_forbidden_minorminornonzeroevaluationdeterminanthscm_positive)))))) /\ (((exists ff_h_mdm_mdr_forbidden_minorminornonzeroevaluationdeterminanthscm_positive_target. ff_h_mdm_mdr_forbidden_minorminornonzeroevaluationdeterminanthscm_positive_target + S (ff_value_mdm_prefix_mdr_forbidden_minorminornonzeroevaluationdeterminanthscm_positive) = S ((S (ff_index_mdm_prefix_mdr_forbidden_minorminornonzeroevaluationdeterminanthscm_positive)) * mdr_us_forbidden_minorminornonzeroevaluationdeterminanthsc)) /\ exists ff_q_mdm_mdr_forbidden_minorminornonzeroevaluationdeterminanthscm_positive_target. mdr_up_forbidden_minorminornonzeroevaluationdeterminanthsc = ff_q_mdm_mdr_forbidden_minorminornonzeroevaluationdeterminanthscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_forbidden_minorminornonzeroevaluationdeterminanthscm_positive)) * mdr_us_forbidden_minorminornonzeroevaluationdeterminanthsc) + (ff_value_mdm_prefix_mdr_forbidden_minorminornonzeroevaluationdeterminanthscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_forbidden_minorminornonzeroevaluationdeterminanthscm_negative. (exists ff_gap_mdm_lt_mdr_forbidden_minorminornonzeroevaluationdeterminanthscm_negative_index_bound. ff_gap_mdm_lt_mdr_forbidden_minorminornonzeroevaluationdeterminanthscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_forbidden_minorminornonzeroevaluationdeterminanthscm_negative) = ((mdr_q_forbidden_minorminornonzeroevaluationdeterminanths) * (mdr_q_forbidden_minorminornonzeroevaluationdeterminanths))) -> exists ff_row_mdm_prefix_mdr_forbidden_minorminornonzeroevaluationdeterminanthscm_negative ff_column_mdm_prefix_mdr_forbidden_minorminornonzeroevaluationdeterminanthscm_negative ff_value_mdm_prefix_mdr_forbidden_minorminornonzeroevaluationdeterminanthscm_negative. (ff_index_mdm_prefix_mdr_forbidden_minorminornonzeroevaluationdeterminanthscm_negative = (mdr_q_forbidden_minorminornonzeroevaluationdeterminanths) * ff_row_mdm_prefix_mdr_forbidden_minorminornonzeroevaluationdeterminanthscm_negative + ff_column_mdm_prefix_mdr_forbidden_minorminornonzeroevaluationdeterminanthscm_negative /\ ((exists ff_gap_mdm_lt_mdr_forbidden_minorminornonzeroevaluationdeterminanthscm_negative_column_bound. ff_gap_mdm_lt_mdr_forbidden_minorminornonzeroevaluationdeterminanthscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_forbidden_minorminornonzeroevaluationdeterminanthscm_negative) = (mdr_q_forbidden_minorminornonzeroevaluationdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_forbidden_minorminornonzeroevaluationdeterminanthscm_negative_cell ff_column_mdm_cell_mdr_forbidden_minorminornonzeroevaluationdeterminanthscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_forbidden_minorminornonzeroevaluationdeterminanthscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_forbidden_minorminornonzeroevaluationdeterminanthscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_forbidden_minorminornonzeroevaluationdeterminanthscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_forbidden_minorminornonzeroevaluationdeterminanthscm_negative_cell = ff_row_mdm_prefix_mdr_forbidden_minorminornonzeroevaluationdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_forbidden_minorminornonzeroevaluationdeterminanthscm_negative_cell_row_after. ff_gap_mdm_le_mdr_forbidden_minorminornonzeroevaluationdeterminanthscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_forbidden_minorminornonzeroevaluationdeterminanthscm_negative)) /\ ff_row_mdm_cell_mdr_forbidden_minorminornonzeroevaluationdeterminanthscm_negative_cell = S ff_row_mdm_prefix_mdr_forbidden_minorminornonzeroevaluationdeterminanthscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_forbidden_minorminornonzeroevaluationdeterminanthscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_forbidden_minorminornonzeroevaluationdeterminanthscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_forbidden_minorminornonzeroevaluationdeterminanthscm_negative) = (mdr_j_forbidden_minorminornonzeroevaluationdeterminanthsc)) /\ ff_column_mdm_cell_mdr_forbidden_minorminornonzeroevaluationdeterminanthscm_negative_cell = ff_column_mdm_prefix_mdr_forbidden_minorminornonzeroevaluationdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_forbidden_minorminornonzeroevaluationdeterminanthscm_negative_cell_column_after. ff_gap_mdm_le_mdr_forbidden_minorminornonzeroevaluationdeterminanthscm_negative_cell_column_after + (mdr_j_forbidden_minorminornonzeroevaluationdeterminanthsc) = (ff_column_mdm_prefix_mdr_forbidden_minorminornonzeroevaluationdeterminanthscm_negative)) /\ ff_column_mdm_cell_mdr_forbidden_minorminornonzeroevaluationdeterminanthscm_negative_cell = S ff_column_mdm_prefix_mdr_forbidden_minorminornonzeroevaluationdeterminanthscm_negative))) /\ (((exists ff_h_mdm_mdr_forbidden_minorminornonzeroevaluationdeterminanthscm_negative_cell_source. ff_h_mdm_mdr_forbidden_minorminornonzeroevaluationdeterminanthscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_forbidden_minorminornonzeroevaluationdeterminanthscm_negative) = S ((S ((ff_row_mdm_cell_mdr_forbidden_minorminornonzeroevaluationdeterminanthscm_negative_cell) * (S (mdr_q_forbidden_minorminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_forbidden_minorminornonzeroevaluationdeterminanthscm_negative_cell))) * mdr_nc_forbidden_minorminornonzeroevaluationdeterminanth)) /\ exists ff_q_mdm_mdr_forbidden_minorminornonzeroevaluationdeterminanthscm_negative_cell_source. mdr_nb_forbidden_minorminornonzeroevaluationdeterminanth = ff_q_mdm_mdr_forbidden_minorminornonzeroevaluationdeterminanthscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_forbidden_minorminornonzeroevaluationdeterminanthscm_negative_cell) * (S (mdr_q_forbidden_minorminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_forbidden_minorminornonzeroevaluationdeterminanthscm_negative_cell))) * mdr_nc_forbidden_minorminornonzeroevaluationdeterminanth) + (ff_value_mdm_prefix_mdr_forbidden_minorminornonzeroevaluationdeterminanthscm_negative)))))) /\ (((exists ff_h_mdm_mdr_forbidden_minorminornonzeroevaluationdeterminanthscm_negative_target. ff_h_mdm_mdr_forbidden_minorminornonzeroevaluationdeterminanthscm_negative_target + S (ff_value_mdm_prefix_mdr_forbidden_minorminornonzeroevaluationdeterminanthscm_negative) = S ((S (ff_index_mdm_prefix_mdr_forbidden_minorminornonzeroevaluationdeterminanthscm_negative)) * mdr_ut_forbidden_minorminornonzeroevaluationdeterminanthsc)) /\ exists ff_q_mdm_mdr_forbidden_minorminornonzeroevaluationdeterminanthscm_negative_target. mdr_un_forbidden_minorminornonzeroevaluationdeterminanthsc = ff_q_mdm_mdr_forbidden_minorminornonzeroevaluationdeterminanthscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_forbidden_minorminornonzeroevaluationdeterminanthscm_negative)) * mdr_ut_forbidden_minorminornonzeroevaluationdeterminanthsc) + (ff_value_mdm_prefix_mdr_forbidden_minorminornonzeroevaluationdeterminanthscm_negative))))))))) /\ ((((exists ff_h_mdr_forbidden_minorminornonzeroevaluationdeterminanthscp. ff_h_mdr_forbidden_minorminornonzeroevaluationdeterminanthscp + S (mdr_p_forbidden_minorminornonzeroevaluationdeterminanthsc) = S ((S (mdr_j_forbidden_minorminornonzeroevaluationdeterminanthsc)) * mdr_ec_forbidden_minorminornonzeroevaluationdeterminanths)) /\ exists ff_q_mdr_forbidden_minorminornonzeroevaluationdeterminanthscp. mdr_eb_forbidden_minorminornonzeroevaluationdeterminanths = ff_q_mdr_forbidden_minorminornonzeroevaluationdeterminanthscp * S ((S (mdr_j_forbidden_minorminornonzeroevaluationdeterminanthsc)) * mdr_ec_forbidden_minorminornonzeroevaluationdeterminanths) + (mdr_p_forbidden_minorminornonzeroevaluationdeterminanthsc))) /\ (((exists ff_h_mdr_forbidden_minorminornonzeroevaluationdeterminanthscn. ff_h_mdr_forbidden_minorminornonzeroevaluationdeterminanthscn + S (mdr_n_forbidden_minorminornonzeroevaluationdeterminanthsc) = S ((S (mdr_j_forbidden_minorminornonzeroevaluationdeterminanthsc)) * mdr_fc_forbidden_minorminornonzeroevaluationdeterminanths)) /\ exists ff_q_mdr_forbidden_minorminornonzeroevaluationdeterminanthscn. mdr_fb_forbidden_minorminornonzeroevaluationdeterminanths = ff_q_mdr_forbidden_minorminornonzeroevaluationdeterminanthscn * S ((S (mdr_j_forbidden_minorminornonzeroevaluationdeterminanthsc)) * mdr_fc_forbidden_minorminornonzeroevaluationdeterminanths) + (mdr_n_forbidden_minorminornonzeroevaluationdeterminanthsc)))))))) /\ (exists ff_ub_mce_fold_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf ff_uc_mce_fold_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf ff_vb_mce_fold_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf ff_vc_mce_fold_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf. ((forall ff_index_mce_alternating_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_prefix. (exists ff_gap_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_prefix_index. ff_gap_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_prefix_index + S (ff_index_mce_alternating_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_prefix) = (S (mdr_q_forbidden_minorminornonzeroevaluationdeterminanths))) -> exists ff_ap_mce_alternating_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_prefix ff_an_mce_alternating_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_prefix ff_bp_mce_alternating_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_prefix ff_bn_mce_alternating_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_prefix ff_p_mce_alternating_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_prefix ff_n_mce_alternating_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_prefix. ((((exists ff_h_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_prefix_ap. ff_h_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_prefix_ap + S (ff_ap_mce_alternating_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_prefix)) * mdr_pc_forbidden_minorminornonzeroevaluationdeterminanth)) /\ exists ff_q_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_prefix_ap. mdr_pb_forbidden_minorminornonzeroevaluationdeterminanth = ff_q_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_prefix)) * mdr_pc_forbidden_minorminornonzeroevaluationdeterminanth) + (ff_ap_mce_alternating_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_prefix_an. ff_h_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_prefix_an + S (ff_an_mce_alternating_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_prefix)) * mdr_nc_forbidden_minorminornonzeroevaluationdeterminanth)) /\ exists ff_q_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_prefix_an. mdr_nb_forbidden_minorminornonzeroevaluationdeterminanth = ff_q_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_prefix)) * mdr_nc_forbidden_minorminornonzeroevaluationdeterminanth) + (ff_an_mce_alternating_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_prefix_bp. ff_h_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_prefix_bp + S (ff_bp_mce_alternating_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_prefix)) * mdr_ec_forbidden_minorminornonzeroevaluationdeterminanths)) /\ exists ff_q_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_prefix_bp. mdr_eb_forbidden_minorminornonzeroevaluationdeterminanths = ff_q_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_prefix)) * mdr_ec_forbidden_minorminornonzeroevaluationdeterminanths) + (ff_bp_mce_alternating_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_prefix_bn. ff_h_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_prefix_bn + S (ff_bn_mce_alternating_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_prefix)) * mdr_fc_forbidden_minorminornonzeroevaluationdeterminanths)) /\ exists ff_q_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_prefix_bn. mdr_fb_forbidden_minorminornonzeroevaluationdeterminanths = ff_q_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_prefix)) * mdr_fc_forbidden_minorminornonzeroevaluationdeterminanths) + (ff_bn_mce_alternating_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_prefix_positive. ff_h_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_prefix_positive + S (ff_p_mce_alternating_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_prefix_positive. ff_ub_mce_fold_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf) + (ff_p_mce_alternating_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_prefix_negative. ff_h_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_prefix_negative + S (ff_n_mce_alternating_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_prefix_negative. ff_vb_mce_fold_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf) + (ff_n_mce_alternating_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_prefix))) /\ (((exists ff_even_mce_term_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_prefix = 2 * ff_even_mce_term_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_prefix_term) /\ (ff_p_mce_alternating_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_prefix = 2 * ff_odd_mce_term_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_positive ff_v_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_positive. ((((exists ff_h_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_positive_start. ff_h_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_positive_start. ff_u_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_positive_start * S ((S (0)) * ff_v_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_positive_terminal. ff_h_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_positive_terminal + S (mdr_p_forbidden_minorminornonzeroevaluationdeterminanth) = S ((S ((S (mdr_q_forbidden_minorminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_positive_terminal. ff_u_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_positive_terminal * S ((S ((S (mdr_q_forbidden_minorminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_positive) + (mdr_p_forbidden_minorminornonzeroevaluationdeterminanth))) /\ forall ff_i_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_positive. (exists ff_lt_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_positive_bound. ff_lt_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_positive_bound + S ff_i_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_positive = (S (mdr_q_forbidden_minorminornonzeroevaluationdeterminanths))) -> exists ff_a_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_positive ff_r_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_positive ff_s_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_positive. ((((exists ff_h_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_positive_summand. ff_h_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_positive_summand + S (ff_a_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_positive_summand. ff_ub_mce_fold_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_positive_summand * S ((S (ff_i_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf) + (ff_a_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_positive_partial. ff_h_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_positive_partial + S (ff_r_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_positive_partial. ff_u_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_positive_partial * S ((S (ff_i_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_positive) + (ff_r_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_positive_successor. ff_h_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_positive_successor + S (ff_s_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_positive) = S ((S (S ff_i_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_positive_successor. ff_u_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_positive_successor * S ((S (S ff_i_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_positive) + (ff_s_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_positive))) /\ ff_s_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_positive = ff_r_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_positive + ff_a_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_positive)))))) /\ (exists ff_u_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_negative ff_v_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_negative. ((((exists ff_h_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_negative_start. ff_h_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_negative_start. ff_u_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_negative_start * S ((S (0)) * ff_v_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_negative_terminal. ff_h_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_negative_terminal + S (mdr_n_forbidden_minorminornonzeroevaluationdeterminanth) = S ((S ((S (mdr_q_forbidden_minorminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_negative_terminal. ff_u_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_negative_terminal * S ((S ((S (mdr_q_forbidden_minorminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_negative) + (mdr_n_forbidden_minorminornonzeroevaluationdeterminanth))) /\ forall ff_i_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_negative. (exists ff_lt_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_negative_bound. ff_lt_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_negative_bound + S ff_i_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_negative = (S (mdr_q_forbidden_minorminornonzeroevaluationdeterminanths))) -> exists ff_a_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_negative ff_r_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_negative ff_s_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_negative. ((((exists ff_h_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_negative_summand. ff_h_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_negative_summand + S (ff_a_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_negative_summand. ff_vb_mce_fold_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_negative_summand * S ((S (ff_i_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf) + (ff_a_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_negative_partial. ff_h_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_negative_partial + S (ff_r_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_negative_partial. ff_u_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_negative_partial * S ((S (ff_i_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_negative) + (ff_r_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_negative_successor. ff_h_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_negative_successor + S (ff_s_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_negative) = S ((S (S ff_i_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_negative_successor. ff_u_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_negative_successor * S ((S (S ff_i_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_negative) + (ff_s_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_negative))) /\ ff_s_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_negative = ff_r_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_negative + ff_a_mce_mdr_forbidden_minorminornonzeroevaluationdeterminanthsf_negative))))))))))))))) /\ ((exists mdr_gap_forbidden_minorminornonzeroevaluationdeterminanti. mdr_gap_forbidden_minorminornonzeroevaluationdeterminanti + S (mdr_i_forbidden_minorminornonzeroevaluationdeterminant) = (mdr_l_forbidden_minorminornonzeroevaluationdeterminant)) /\ (exists mdr_z_forbidden_minorminornonzeroevaluationdeterminantr. ((exists mdr_a_forbidden_minorminornonzeroevaluationdeterminantrc mdr_b_forbidden_minorminornonzeroevaluationdeterminantrc mdr_c_forbidden_minorminornonzeroevaluationdeterminantrc mdr_e_forbidden_minorminornonzeroevaluationdeterminantrc mdr_f_forbidden_minorminornonzeroevaluationdeterminantrc. ((mdr_a_forbidden_minorminornonzeroevaluationdeterminantrc = ((q) + (mdr_ub_forbidden_minorminornonzeroevaluation)) * S ((q) + (mdr_ub_forbidden_minorminornonzeroevaluation)) + ((mdr_ub_forbidden_minorminornonzeroevaluation) + (mdr_ub_forbidden_minorminornonzeroevaluation))) /\ ((mdr_b_forbidden_minorminornonzeroevaluationdeterminantrc = ((mdr_uc_forbidden_minorminornonzeroevaluation) + (mdr_vb_forbidden_minorminornonzeroevaluation)) * S ((mdr_uc_forbidden_minorminornonzeroevaluation) + (mdr_vb_forbidden_minorminornonzeroevaluation)) + ((mdr_vb_forbidden_minorminornonzeroevaluation) + (mdr_vb_forbidden_minorminornonzeroevaluation))) /\ ((mdr_c_forbidden_minorminornonzeroevaluationdeterminantrc = ((mdr_a_forbidden_minorminornonzeroevaluationdeterminantrc) + (mdr_b_forbidden_minorminornonzeroevaluationdeterminantrc)) * S ((mdr_a_forbidden_minorminornonzeroevaluationdeterminantrc) + (mdr_b_forbidden_minorminornonzeroevaluationdeterminantrc)) + ((mdr_b_forbidden_minorminornonzeroevaluationdeterminantrc) + (mdr_b_forbidden_minorminornonzeroevaluationdeterminantrc))) /\ ((mdr_e_forbidden_minorminornonzeroevaluationdeterminantrc = ((mdr_p_forbidden_minorminornonzero) + (mdr_n_forbidden_minorminornonzero)) * S ((mdr_p_forbidden_minorminornonzero) + (mdr_n_forbidden_minorminornonzero)) + ((mdr_n_forbidden_minorminornonzero) + (mdr_n_forbidden_minorminornonzero))) /\ ((mdr_f_forbidden_minorminornonzeroevaluationdeterminantrc = ((mdr_vc_forbidden_minorminornonzeroevaluation) + (mdr_e_forbidden_minorminornonzeroevaluationdeterminantrc)) * S ((mdr_vc_forbidden_minorminornonzeroevaluation) + (mdr_e_forbidden_minorminornonzeroevaluationdeterminantrc)) + ((mdr_e_forbidden_minorminornonzeroevaluationdeterminantrc) + (mdr_e_forbidden_minorminornonzeroevaluationdeterminantrc))) /\ ((mdr_z_forbidden_minorminornonzeroevaluationdeterminantr) = ((mdr_c_forbidden_minorminornonzeroevaluationdeterminantrc) + (mdr_f_forbidden_minorminornonzeroevaluationdeterminantrc)) * S ((mdr_c_forbidden_minorminornonzeroevaluationdeterminantrc) + (mdr_f_forbidden_minorminornonzeroevaluationdeterminantrc)) + ((mdr_f_forbidden_minorminornonzeroevaluationdeterminantrc) + (mdr_f_forbidden_minorminornonzeroevaluationdeterminantrc))))))))) /\ (((exists ff_h_mdr_forbidden_minorminornonzeroevaluationdeterminantrb. ff_h_mdr_forbidden_minorminornonzeroevaluationdeterminantrb + S (mdr_z_forbidden_minorminornonzeroevaluationdeterminantr) = S ((S (mdr_i_forbidden_minorminornonzeroevaluationdeterminant)) * mdr_c_forbidden_minorminornonzeroevaluationdeterminant)) /\ exists ff_q_mdr_forbidden_minorminornonzeroevaluationdeterminantrb. mdr_b_forbidden_minorminornonzeroevaluationdeterminant = ff_q_mdr_forbidden_minorminornonzeroevaluationdeterminantrb * S ((S (mdr_i_forbidden_minorminornonzeroevaluationdeterminant)) * mdr_c_forbidden_minorminornonzeroevaluationdeterminant) + (mdr_z_forbidden_minorminornonzeroevaluationdeterminantr)))))))))) /\ (~(mdr_p_forbidden_minorminornonzero = mdr_n_forbidden_minorminornonzero))))))))