matrix_rank_nonzero_minor_dimension_bounds

forall pb pc nb nc r w q. (exists mdr_rb_minor_dimensions mdr_rc_minor_dimensions mdr_cb_minor_dimensions mdr_cc_minor_dimensions. (((((forall fom_index_mrf_minor_dimensionsminorrowsbound. (exists fom_gap_mrf_minor_dimensionsminorrowsbound_index_bound. fom_gap_mrf_minor_dimensionsminorrowsbound_index_bound + S (fom_index_mrf_minor_dimensionsminorrowsbound) = q) -> exists fom_value_mrf_minor_dimensionsminorrowsbound. ((((exists fom_beta_height_mrf_minor_dimensionsminorrowsbound_entry. fom_beta_height_mrf_minor_dimensionsminorrowsbound_entry + S (fom_value_mrf_minor_dimensionsminorrowsbound) = S ((S (fom_index_mrf_minor_dimensionsminorrowsbound)) * mdr_rc_minor_dimensions)) /\ exists fom_beta_quotient_mrf_minor_dimensionsminorrowsbound_entry. mdr_rb_minor_dimensions = fom_beta_quotient_mrf_minor_dimensionsminorrowsbound_entry * S ((S (fom_index_mrf_minor_dimensionsminorrowsbound)) * mdr_rc_minor_dimensions) + (fom_value_mrf_minor_dimensionsminorrowsbound))) /\ (exists fom_gap_mrf_minor_dimensionsminorrowsbound_value_bound. fom_gap_mrf_minor_dimensionsminorrowsbound_value_bound + S (fom_value_mrf_minor_dimensionsminorrowsbound) = r))) /\ (forall mdr_i_minor_dimensionsminorrowsdistinct mdr_j_minor_dimensionsminorrowsdistinct mdr_a_minor_dimensionsminorrowsdistinct. (exists mdr_gap_minor_dimensionsminorrowsdistincti. mdr_gap_minor_dimensionsminorrowsdistincti + S (mdr_i_minor_dimensionsminorrowsdistinct) = (q)) -> (exists mdr_gap_minor_dimensionsminorrowsdistinctj. mdr_gap_minor_dimensionsminorrowsdistinctj + S (mdr_j_minor_dimensionsminorrowsdistinct) = (q)) -> (((exists ff_h_mdr_minor_dimensionsminorrowsdistinctfirst. ff_h_mdr_minor_dimensionsminorrowsdistinctfirst + S (mdr_a_minor_dimensionsminorrowsdistinct) = S ((S (mdr_i_minor_dimensionsminorrowsdistinct)) * mdr_rc_minor_dimensions)) /\ exists ff_q_mdr_minor_dimensionsminorrowsdistinctfirst. mdr_rb_minor_dimensions = ff_q_mdr_minor_dimensionsminorrowsdistinctfirst * S ((S (mdr_i_minor_dimensionsminorrowsdistinct)) * mdr_rc_minor_dimensions) + (mdr_a_minor_dimensionsminorrowsdistinct))) -> (((exists ff_h_mdr_minor_dimensionsminorrowsdistinctsecond. ff_h_mdr_minor_dimensionsminorrowsdistinctsecond + S (mdr_a_minor_dimensionsminorrowsdistinct) = S ((S (mdr_j_minor_dimensionsminorrowsdistinct)) * mdr_rc_minor_dimensions)) /\ exists ff_q_mdr_minor_dimensionsminorrowsdistinctsecond. mdr_rb_minor_dimensions = ff_q_mdr_minor_dimensionsminorrowsdistinctsecond * S ((S (mdr_j_minor_dimensionsminorrowsdistinct)) * mdr_rc_minor_dimensions) + (mdr_a_minor_dimensionsminorrowsdistinct))) -> mdr_i_minor_dimensionsminorrowsdistinct = mdr_j_minor_dimensionsminorrowsdistinct))) /\ ((((forall fom_index_mrf_minor_dimensionsminorcolumnsbound. (exists fom_gap_mrf_minor_dimensionsminorcolumnsbound_index_bound. fom_gap_mrf_minor_dimensionsminorcolumnsbound_index_bound + S (fom_index_mrf_minor_dimensionsminorcolumnsbound) = q) -> exists fom_value_mrf_minor_dimensionsminorcolumnsbound. ((((exists fom_beta_height_mrf_minor_dimensionsminorcolumnsbound_entry. fom_beta_height_mrf_minor_dimensionsminorcolumnsbound_entry + S (fom_value_mrf_minor_dimensionsminorcolumnsbound) = S ((S (fom_index_mrf_minor_dimensionsminorcolumnsbound)) * mdr_cc_minor_dimensions)) /\ exists fom_beta_quotient_mrf_minor_dimensionsminorcolumnsbound_entry. mdr_cb_minor_dimensions = fom_beta_quotient_mrf_minor_dimensionsminorcolumnsbound_entry * S ((S (fom_index_mrf_minor_dimensionsminorcolumnsbound)) * mdr_cc_minor_dimensions) + (fom_value_mrf_minor_dimensionsminorcolumnsbound))) /\ (exists fom_gap_mrf_minor_dimensionsminorcolumnsbound_value_bound. fom_gap_mrf_minor_dimensionsminorcolumnsbound_value_bound + S (fom_value_mrf_minor_dimensionsminorcolumnsbound) = w))) /\ (forall mdr_i_minor_dimensionsminorcolumnsdistinct mdr_j_minor_dimensionsminorcolumnsdistinct mdr_a_minor_dimensionsminorcolumnsdistinct. (exists mdr_gap_minor_dimensionsminorcolumnsdistincti. mdr_gap_minor_dimensionsminorcolumnsdistincti + S (mdr_i_minor_dimensionsminorcolumnsdistinct) = (q)) -> (exists mdr_gap_minor_dimensionsminorcolumnsdistinctj. mdr_gap_minor_dimensionsminorcolumnsdistinctj + S (mdr_j_minor_dimensionsminorcolumnsdistinct) = (q)) -> (((exists ff_h_mdr_minor_dimensionsminorcolumnsdistinctfirst. ff_h_mdr_minor_dimensionsminorcolumnsdistinctfirst + S (mdr_a_minor_dimensionsminorcolumnsdistinct) = S ((S (mdr_i_minor_dimensionsminorcolumnsdistinct)) * mdr_cc_minor_dimensions)) /\ exists ff_q_mdr_minor_dimensionsminorcolumnsdistinctfirst. mdr_cb_minor_dimensions = ff_q_mdr_minor_dimensionsminorcolumnsdistinctfirst * S ((S (mdr_i_minor_dimensionsminorcolumnsdistinct)) * mdr_cc_minor_dimensions) + (mdr_a_minor_dimensionsminorcolumnsdistinct))) -> (((exists ff_h_mdr_minor_dimensionsminorcolumnsdistinctsecond. ff_h_mdr_minor_dimensionsminorcolumnsdistinctsecond + S (mdr_a_minor_dimensionsminorcolumnsdistinct) = S ((S (mdr_j_minor_dimensionsminorcolumnsdistinct)) * mdr_cc_minor_dimensions)) /\ exists ff_q_mdr_minor_dimensionsminorcolumnsdistinctsecond. mdr_cb_minor_dimensions = ff_q_mdr_minor_dimensionsminorcolumnsdistinctsecond * S ((S (mdr_j_minor_dimensionsminorcolumnsdistinct)) * mdr_cc_minor_dimensions) + (mdr_a_minor_dimensionsminorcolumnsdistinct))) -> mdr_i_minor_dimensionsminorcolumnsdistinct = mdr_j_minor_dimensionsminorcolumnsdistinct))) /\ (exists mdr_p_minor_dimensionsminornonzero mdr_n_minor_dimensionsminornonzero. ((exists mdr_ub_minor_dimensionsminornonzeroevaluation mdr_uc_minor_dimensionsminornonzeroevaluation mdr_vb_minor_dimensionsminornonzeroevaluation mdr_vc_minor_dimensionsminornonzeroevaluation. ((((forall mdr_i_minor_dimensionsminornonzeroevaluationmatrixpositive. (exists mdr_gap_minor_dimensionsminornonzeroevaluationmatrixpositivebound. mdr_gap_minor_dimensionsminornonzeroevaluationmatrixpositivebound + S (mdr_i_minor_dimensionsminornonzeroevaluationmatrixpositive) = ((q) * (q))) -> exists mdr_a_minor_dimensionsminornonzeroevaluationmatrixpositive. (((exists mdr_r_minor_dimensionsminornonzeroevaluationmatrixpositivepoint mdr_s_minor_dimensionsminornonzeroevaluationmatrixpositivepoint mdr_u_minor_dimensionsminornonzeroevaluationmatrixpositivepoint mdr_v_minor_dimensionsminornonzeroevaluationmatrixpositivepoint. ((mdr_i_minor_dimensionsminornonzeroevaluationmatrixpositive = (q) * mdr_r_minor_dimensionsminornonzeroevaluationmatrixpositivepoint + mdr_s_minor_dimensionsminornonzeroevaluationmatrixpositivepoint) /\ ((exists mdr_gap_minor_dimensionsminornonzeroevaluationmatrixpositivepointcolumn. mdr_gap_minor_dimensionsminornonzeroevaluationmatrixpositivepointcolumn + S (mdr_s_minor_dimensionsminornonzeroevaluationmatrixpositivepoint) = (q)) /\ ((((exists ff_h_mdr_minor_dimensionsminornonzeroevaluationmatrixpositivepointrow_index. ff_h_mdr_minor_dimensionsminornonzeroevaluationmatrixpositivepointrow_index + S (mdr_u_minor_dimensionsminornonzeroevaluationmatrixpositivepoint) = S ((S (mdr_r_minor_dimensionsminornonzeroevaluationmatrixpositivepoint)) * mdr_rc_minor_dimensions)) /\ exists ff_q_mdr_minor_dimensionsminornonzeroevaluationmatrixpositivepointrow_index. mdr_rb_minor_dimensions = ff_q_mdr_minor_dimensionsminornonzeroevaluationmatrixpositivepointrow_index * S ((S (mdr_r_minor_dimensionsminornonzeroevaluationmatrixpositivepoint)) * mdr_rc_minor_dimensions) + (mdr_u_minor_dimensionsminornonzeroevaluationmatrixpositivepoint))) /\ ((((exists ff_h_mdr_minor_dimensionsminornonzeroevaluationmatrixpositivepointcolumn_index. ff_h_mdr_minor_dimensionsminornonzeroevaluationmatrixpositivepointcolumn_index + S (mdr_v_minor_dimensionsminornonzeroevaluationmatrixpositivepoint) = S ((S (mdr_s_minor_dimensionsminornonzeroevaluationmatrixpositivepoint)) * mdr_cc_minor_dimensions)) /\ exists ff_q_mdr_minor_dimensionsminornonzeroevaluationmatrixpositivepointcolumn_index. mdr_cb_minor_dimensions = ff_q_mdr_minor_dimensionsminornonzeroevaluationmatrixpositivepointcolumn_index * S ((S (mdr_s_minor_dimensionsminornonzeroevaluationmatrixpositivepoint)) * mdr_cc_minor_dimensions) + (mdr_v_minor_dimensionsminornonzeroevaluationmatrixpositivepoint))) /\ (((exists ff_h_mdr_minor_dimensionsminornonzeroevaluationmatrixpositivepointsource. ff_h_mdr_minor_dimensionsminornonzeroevaluationmatrixpositivepointsource + S (mdr_a_minor_dimensionsminornonzeroevaluationmatrixpositive) = S ((S ((mdr_u_minor_dimensionsminornonzeroevaluationmatrixpositivepoint) * (w) + (mdr_v_minor_dimensionsminornonzeroevaluationmatrixpositivepoint))) * pc)) /\ exists ff_q_mdr_minor_dimensionsminornonzeroevaluationmatrixpositivepointsource. pb = ff_q_mdr_minor_dimensionsminornonzeroevaluationmatrixpositivepointsource * S ((S ((mdr_u_minor_dimensionsminornonzeroevaluationmatrixpositivepoint) * (w) + (mdr_v_minor_dimensionsminornonzeroevaluationmatrixpositivepoint))) * pc) + (mdr_a_minor_dimensionsminornonzeroevaluationmatrixpositive)))))))) /\ (((exists ff_h_mdr_minor_dimensionsminornonzeroevaluationmatrixpositiveoutput. ff_h_mdr_minor_dimensionsminornonzeroevaluationmatrixpositiveoutput + S (mdr_a_minor_dimensionsminornonzeroevaluationmatrixpositive) = S ((S (mdr_i_minor_dimensionsminornonzeroevaluationmatrixpositive)) * mdr_uc_minor_dimensionsminornonzeroevaluation)) /\ exists ff_q_mdr_minor_dimensionsminornonzeroevaluationmatrixpositiveoutput. mdr_ub_minor_dimensionsminornonzeroevaluation = ff_q_mdr_minor_dimensionsminornonzeroevaluationmatrixpositiveoutput * S ((S (mdr_i_minor_dimensionsminornonzeroevaluationmatrixpositive)) * mdr_uc_minor_dimensionsminornonzeroevaluation) + (mdr_a_minor_dimensionsminornonzeroevaluationmatrixpositive)))))) /\ (forall mdr_i_minor_dimensionsminornonzeroevaluationmatrixnegative. (exists mdr_gap_minor_dimensionsminornonzeroevaluationmatrixnegativebound. mdr_gap_minor_dimensionsminornonzeroevaluationmatrixnegativebound + S (mdr_i_minor_dimensionsminornonzeroevaluationmatrixnegative) = ((q) * (q))) -> exists mdr_a_minor_dimensionsminornonzeroevaluationmatrixnegative. (((exists mdr_r_minor_dimensionsminornonzeroevaluationmatrixnegativepoint mdr_s_minor_dimensionsminornonzeroevaluationmatrixnegativepoint mdr_u_minor_dimensionsminornonzeroevaluationmatrixnegativepoint mdr_v_minor_dimensionsminornonzeroevaluationmatrixnegativepoint. ((mdr_i_minor_dimensionsminornonzeroevaluationmatrixnegative = (q) * mdr_r_minor_dimensionsminornonzeroevaluationmatrixnegativepoint + mdr_s_minor_dimensionsminornonzeroevaluationmatrixnegativepoint) /\ ((exists mdr_gap_minor_dimensionsminornonzeroevaluationmatrixnegativepointcolumn. mdr_gap_minor_dimensionsminornonzeroevaluationmatrixnegativepointcolumn + S (mdr_s_minor_dimensionsminornonzeroevaluationmatrixnegativepoint) = (q)) /\ ((((exists ff_h_mdr_minor_dimensionsminornonzeroevaluationmatrixnegativepointrow_index. ff_h_mdr_minor_dimensionsminornonzeroevaluationmatrixnegativepointrow_index + S (mdr_u_minor_dimensionsminornonzeroevaluationmatrixnegativepoint) = S ((S (mdr_r_minor_dimensionsminornonzeroevaluationmatrixnegativepoint)) * mdr_rc_minor_dimensions)) /\ exists ff_q_mdr_minor_dimensionsminornonzeroevaluationmatrixnegativepointrow_index. mdr_rb_minor_dimensions = ff_q_mdr_minor_dimensionsminornonzeroevaluationmatrixnegativepointrow_index * S ((S (mdr_r_minor_dimensionsminornonzeroevaluationmatrixnegativepoint)) * mdr_rc_minor_dimensions) + (mdr_u_minor_dimensionsminornonzeroevaluationmatrixnegativepoint))) /\ ((((exists ff_h_mdr_minor_dimensionsminornonzeroevaluationmatrixnegativepointcolumn_index. ff_h_mdr_minor_dimensionsminornonzeroevaluationmatrixnegativepointcolumn_index + S (mdr_v_minor_dimensionsminornonzeroevaluationmatrixnegativepoint) = S ((S (mdr_s_minor_dimensionsminornonzeroevaluationmatrixnegativepoint)) * mdr_cc_minor_dimensions)) /\ exists ff_q_mdr_minor_dimensionsminornonzeroevaluationmatrixnegativepointcolumn_index. mdr_cb_minor_dimensions = ff_q_mdr_minor_dimensionsminornonzeroevaluationmatrixnegativepointcolumn_index * S ((S (mdr_s_minor_dimensionsminornonzeroevaluationmatrixnegativepoint)) * mdr_cc_minor_dimensions) + (mdr_v_minor_dimensionsminornonzeroevaluationmatrixnegativepoint))) /\ (((exists ff_h_mdr_minor_dimensionsminornonzeroevaluationmatrixnegativepointsource. ff_h_mdr_minor_dimensionsminornonzeroevaluationmatrixnegativepointsource + S (mdr_a_minor_dimensionsminornonzeroevaluationmatrixnegative) = S ((S ((mdr_u_minor_dimensionsminornonzeroevaluationmatrixnegativepoint) * (w) + (mdr_v_minor_dimensionsminornonzeroevaluationmatrixnegativepoint))) * nc)) /\ exists ff_q_mdr_minor_dimensionsminornonzeroevaluationmatrixnegativepointsource. nb = ff_q_mdr_minor_dimensionsminornonzeroevaluationmatrixnegativepointsource * S ((S ((mdr_u_minor_dimensionsminornonzeroevaluationmatrixnegativepoint) * (w) + (mdr_v_minor_dimensionsminornonzeroevaluationmatrixnegativepoint))) * nc) + (mdr_a_minor_dimensionsminornonzeroevaluationmatrixnegative)))))))) /\ (((exists ff_h_mdr_minor_dimensionsminornonzeroevaluationmatrixnegativeoutput. ff_h_mdr_minor_dimensionsminornonzeroevaluationmatrixnegativeoutput + S (mdr_a_minor_dimensionsminornonzeroevaluationmatrixnegative) = S ((S (mdr_i_minor_dimensionsminornonzeroevaluationmatrixnegative)) * mdr_vc_minor_dimensionsminornonzeroevaluation)) /\ exists ff_q_mdr_minor_dimensionsminornonzeroevaluationmatrixnegativeoutput. mdr_vb_minor_dimensionsminornonzeroevaluation = ff_q_mdr_minor_dimensionsminornonzeroevaluationmatrixnegativeoutput * S ((S (mdr_i_minor_dimensionsminornonzeroevaluationmatrixnegative)) * mdr_vc_minor_dimensionsminornonzeroevaluation) + (mdr_a_minor_dimensionsminornonzeroevaluationmatrixnegative)))))))) /\ (exists mdr_b_minor_dimensionsminornonzeroevaluationdeterminant mdr_c_minor_dimensionsminornonzeroevaluationdeterminant mdr_l_minor_dimensionsminornonzeroevaluationdeterminant mdr_i_minor_dimensionsminornonzeroevaluationdeterminant. ((forall mdr_i_minor_dimensionsminornonzeroevaluationdeterminanth. (exists mdr_gap_minor_dimensionsminornonzeroevaluationdeterminanthi. mdr_gap_minor_dimensionsminornonzeroevaluationdeterminanthi + S (mdr_i_minor_dimensionsminornonzeroevaluationdeterminanth) = (mdr_l_minor_dimensionsminornonzeroevaluationdeterminant)) -> exists mdr_d_minor_dimensionsminornonzeroevaluationdeterminanth mdr_pb_minor_dimensionsminornonzeroevaluationdeterminanth mdr_pc_minor_dimensionsminornonzeroevaluationdeterminanth mdr_nb_minor_dimensionsminornonzeroevaluationdeterminanth mdr_nc_minor_dimensionsminornonzeroevaluationdeterminanth mdr_p_minor_dimensionsminornonzeroevaluationdeterminanth mdr_n_minor_dimensionsminornonzeroevaluationdeterminanth. ((exists mdr_z_minor_dimensionsminornonzeroevaluationdeterminanthr. ((exists mdr_a_minor_dimensionsminornonzeroevaluationdeterminanthrc mdr_b_minor_dimensionsminornonzeroevaluationdeterminanthrc mdr_c_minor_dimensionsminornonzeroevaluationdeterminanthrc mdr_e_minor_dimensionsminornonzeroevaluationdeterminanthrc mdr_f_minor_dimensionsminornonzeroevaluationdeterminanthrc. ((mdr_a_minor_dimensionsminornonzeroevaluationdeterminanthrc = ((mdr_d_minor_dimensionsminornonzeroevaluationdeterminanth) + (mdr_pb_minor_dimensionsminornonzeroevaluationdeterminanth)) * S ((mdr_d_minor_dimensionsminornonzeroevaluationdeterminanth) + (mdr_pb_minor_dimensionsminornonzeroevaluationdeterminanth)) + ((mdr_pb_minor_dimensionsminornonzeroevaluationdeterminanth) + (mdr_pb_minor_dimensionsminornonzeroevaluationdeterminanth))) /\ ((mdr_b_minor_dimensionsminornonzeroevaluationdeterminanthrc = ((mdr_pc_minor_dimensionsminornonzeroevaluationdeterminanth) + (mdr_nb_minor_dimensionsminornonzeroevaluationdeterminanth)) * S ((mdr_pc_minor_dimensionsminornonzeroevaluationdeterminanth) + (mdr_nb_minor_dimensionsminornonzeroevaluationdeterminanth)) + ((mdr_nb_minor_dimensionsminornonzeroevaluationdeterminanth) + (mdr_nb_minor_dimensionsminornonzeroevaluationdeterminanth))) /\ ((mdr_c_minor_dimensionsminornonzeroevaluationdeterminanthrc = ((mdr_a_minor_dimensionsminornonzeroevaluationdeterminanthrc) + (mdr_b_minor_dimensionsminornonzeroevaluationdeterminanthrc)) * S ((mdr_a_minor_dimensionsminornonzeroevaluationdeterminanthrc) + (mdr_b_minor_dimensionsminornonzeroevaluationdeterminanthrc)) + ((mdr_b_minor_dimensionsminornonzeroevaluationdeterminanthrc) + (mdr_b_minor_dimensionsminornonzeroevaluationdeterminanthrc))) /\ ((mdr_e_minor_dimensionsminornonzeroevaluationdeterminanthrc = ((mdr_p_minor_dimensionsminornonzeroevaluationdeterminanth) + (mdr_n_minor_dimensionsminornonzeroevaluationdeterminanth)) * S ((mdr_p_minor_dimensionsminornonzeroevaluationdeterminanth) + (mdr_n_minor_dimensionsminornonzeroevaluationdeterminanth)) + ((mdr_n_minor_dimensionsminornonzeroevaluationdeterminanth) + (mdr_n_minor_dimensionsminornonzeroevaluationdeterminanth))) /\ ((mdr_f_minor_dimensionsminornonzeroevaluationdeterminanthrc = ((mdr_nc_minor_dimensionsminornonzeroevaluationdeterminanth) + (mdr_e_minor_dimensionsminornonzeroevaluationdeterminanthrc)) * S ((mdr_nc_minor_dimensionsminornonzeroevaluationdeterminanth) + (mdr_e_minor_dimensionsminornonzeroevaluationdeterminanthrc)) + ((mdr_e_minor_dimensionsminornonzeroevaluationdeterminanthrc) + (mdr_e_minor_dimensionsminornonzeroevaluationdeterminanthrc))) /\ ((mdr_z_minor_dimensionsminornonzeroevaluationdeterminanthr) = ((mdr_c_minor_dimensionsminornonzeroevaluationdeterminanthrc) + (mdr_f_minor_dimensionsminornonzeroevaluationdeterminanthrc)) * S ((mdr_c_minor_dimensionsminornonzeroevaluationdeterminanthrc) + (mdr_f_minor_dimensionsminornonzeroevaluationdeterminanthrc)) + ((mdr_f_minor_dimensionsminornonzeroevaluationdeterminanthrc) + (mdr_f_minor_dimensionsminornonzeroevaluationdeterminanthrc))))))))) /\ (((exists ff_h_mdr_minor_dimensionsminornonzeroevaluationdeterminanthrb. ff_h_mdr_minor_dimensionsminornonzeroevaluationdeterminanthrb + S (mdr_z_minor_dimensionsminornonzeroevaluationdeterminanthr) = S ((S (mdr_i_minor_dimensionsminornonzeroevaluationdeterminanth)) * mdr_c_minor_dimensionsminornonzeroevaluationdeterminant)) /\ exists ff_q_mdr_minor_dimensionsminornonzeroevaluationdeterminanthrb. mdr_b_minor_dimensionsminornonzeroevaluationdeterminant = ff_q_mdr_minor_dimensionsminornonzeroevaluationdeterminanthrb * S ((S (mdr_i_minor_dimensionsminornonzeroevaluationdeterminanth)) * mdr_c_minor_dimensionsminornonzeroevaluationdeterminant) + (mdr_z_minor_dimensionsminornonzeroevaluationdeterminanthr))))) /\ (((((mdr_d_minor_dimensionsminornonzeroevaluationdeterminanth) = 0) /\ (((mdr_p_minor_dimensionsminornonzeroevaluationdeterminanth) = 1) /\ ((mdr_n_minor_dimensionsminornonzeroevaluationdeterminanth) = 0))) \/ exists mdr_q_minor_dimensionsminornonzeroevaluationdeterminanths mdr_eb_minor_dimensionsminornonzeroevaluationdeterminanths mdr_ec_minor_dimensionsminornonzeroevaluationdeterminanths mdr_fb_minor_dimensionsminornonzeroevaluationdeterminanths mdr_fc_minor_dimensionsminornonzeroevaluationdeterminanths. (((mdr_d_minor_dimensionsminornonzeroevaluationdeterminanth) = S (mdr_q_minor_dimensionsminornonzeroevaluationdeterminanths)) /\ ((forall mdr_j_minor_dimensionsminornonzeroevaluationdeterminanthsc. (exists mdr_gap_minor_dimensionsminornonzeroevaluationdeterminanthscj. mdr_gap_minor_dimensionsminornonzeroevaluationdeterminanthscj + S (mdr_j_minor_dimensionsminornonzeroevaluationdeterminanthsc) = (S (mdr_q_minor_dimensionsminornonzeroevaluationdeterminanths))) -> exists mdr_i_minor_dimensionsminornonzeroevaluationdeterminanthsc mdr_up_minor_dimensionsminornonzeroevaluationdeterminanthsc mdr_us_minor_dimensionsminornonzeroevaluationdeterminanthsc mdr_un_minor_dimensionsminornonzeroevaluationdeterminanthsc mdr_ut_minor_dimensionsminornonzeroevaluationdeterminanthsc mdr_p_minor_dimensionsminornonzeroevaluationdeterminanthsc mdr_n_minor_dimensionsminornonzeroevaluationdeterminanthsc. ((exists mdr_gap_minor_dimensionsminornonzeroevaluationdeterminanthsci. mdr_gap_minor_dimensionsminornonzeroevaluationdeterminanthsci + S (mdr_i_minor_dimensionsminornonzeroevaluationdeterminanthsc) = (mdr_i_minor_dimensionsminornonzeroevaluationdeterminanth)) /\ ((exists mdr_z_minor_dimensionsminornonzeroevaluationdeterminanthscr. ((exists mdr_a_minor_dimensionsminornonzeroevaluationdeterminanthscrc mdr_b_minor_dimensionsminornonzeroevaluationdeterminanthscrc mdr_c_minor_dimensionsminornonzeroevaluationdeterminanthscrc mdr_e_minor_dimensionsminornonzeroevaluationdeterminanthscrc mdr_f_minor_dimensionsminornonzeroevaluationdeterminanthscrc. ((mdr_a_minor_dimensionsminornonzeroevaluationdeterminanthscrc = ((mdr_q_minor_dimensionsminornonzeroevaluationdeterminanths) + (mdr_up_minor_dimensionsminornonzeroevaluationdeterminanthsc)) * S ((mdr_q_minor_dimensionsminornonzeroevaluationdeterminanths) + (mdr_up_minor_dimensionsminornonzeroevaluationdeterminanthsc)) + ((mdr_up_minor_dimensionsminornonzeroevaluationdeterminanthsc) + (mdr_up_minor_dimensionsminornonzeroevaluationdeterminanthsc))) /\ ((mdr_b_minor_dimensionsminornonzeroevaluationdeterminanthscrc = ((mdr_us_minor_dimensionsminornonzeroevaluationdeterminanthsc) + (mdr_un_minor_dimensionsminornonzeroevaluationdeterminanthsc)) * S ((mdr_us_minor_dimensionsminornonzeroevaluationdeterminanthsc) + (mdr_un_minor_dimensionsminornonzeroevaluationdeterminanthsc)) + ((mdr_un_minor_dimensionsminornonzeroevaluationdeterminanthsc) + (mdr_un_minor_dimensionsminornonzeroevaluationdeterminanthsc))) /\ ((mdr_c_minor_dimensionsminornonzeroevaluationdeterminanthscrc = ((mdr_a_minor_dimensionsminornonzeroevaluationdeterminanthscrc) + (mdr_b_minor_dimensionsminornonzeroevaluationdeterminanthscrc)) * S ((mdr_a_minor_dimensionsminornonzeroevaluationdeterminanthscrc) + (mdr_b_minor_dimensionsminornonzeroevaluationdeterminanthscrc)) + ((mdr_b_minor_dimensionsminornonzeroevaluationdeterminanthscrc) + (mdr_b_minor_dimensionsminornonzeroevaluationdeterminanthscrc))) /\ ((mdr_e_minor_dimensionsminornonzeroevaluationdeterminanthscrc = ((mdr_p_minor_dimensionsminornonzeroevaluationdeterminanthsc) + (mdr_n_minor_dimensionsminornonzeroevaluationdeterminanthsc)) * S ((mdr_p_minor_dimensionsminornonzeroevaluationdeterminanthsc) + (mdr_n_minor_dimensionsminornonzeroevaluationdeterminanthsc)) + ((mdr_n_minor_dimensionsminornonzeroevaluationdeterminanthsc) + (mdr_n_minor_dimensionsminornonzeroevaluationdeterminanthsc))) /\ ((mdr_f_minor_dimensionsminornonzeroevaluationdeterminanthscrc = ((mdr_ut_minor_dimensionsminornonzeroevaluationdeterminanthsc) + (mdr_e_minor_dimensionsminornonzeroevaluationdeterminanthscrc)) * S ((mdr_ut_minor_dimensionsminornonzeroevaluationdeterminanthsc) + (mdr_e_minor_dimensionsminornonzeroevaluationdeterminanthscrc)) + ((mdr_e_minor_dimensionsminornonzeroevaluationdeterminanthscrc) + (mdr_e_minor_dimensionsminornonzeroevaluationdeterminanthscrc))) /\ ((mdr_z_minor_dimensionsminornonzeroevaluationdeterminanthscr) = ((mdr_c_minor_dimensionsminornonzeroevaluationdeterminanthscrc) + (mdr_f_minor_dimensionsminornonzeroevaluationdeterminanthscrc)) * S ((mdr_c_minor_dimensionsminornonzeroevaluationdeterminanthscrc) + (mdr_f_minor_dimensionsminornonzeroevaluationdeterminanthscrc)) + ((mdr_f_minor_dimensionsminornonzeroevaluationdeterminanthscrc) + (mdr_f_minor_dimensionsminornonzeroevaluationdeterminanthscrc))))))))) /\ (((exists ff_h_mdr_minor_dimensionsminornonzeroevaluationdeterminanthscrb. ff_h_mdr_minor_dimensionsminornonzeroevaluationdeterminanthscrb + S (mdr_z_minor_dimensionsminornonzeroevaluationdeterminanthscr) = S ((S (mdr_i_minor_dimensionsminornonzeroevaluationdeterminanthsc)) * mdr_c_minor_dimensionsminornonzeroevaluationdeterminant)) /\ exists ff_q_mdr_minor_dimensionsminornonzeroevaluationdeterminanthscrb. mdr_b_minor_dimensionsminornonzeroevaluationdeterminant = ff_q_mdr_minor_dimensionsminornonzeroevaluationdeterminanthscrb * S ((S (mdr_i_minor_dimensionsminornonzeroevaluationdeterminanthsc)) * mdr_c_minor_dimensionsminornonzeroevaluationdeterminant) + (mdr_z_minor_dimensionsminornonzeroevaluationdeterminanthscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_minor_dimensionsminornonzeroevaluationdeterminanthscm_positive. (exists ff_gap_mdm_lt_mdr_minor_dimensionsminornonzeroevaluationdeterminanthscm_positive_index_bound. ff_gap_mdm_lt_mdr_minor_dimensionsminornonzeroevaluationdeterminanthscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_minor_dimensionsminornonzeroevaluationdeterminanthscm_positive) = ((mdr_q_minor_dimensionsminornonzeroevaluationdeterminanths) * (mdr_q_minor_dimensionsminornonzeroevaluationdeterminanths))) -> exists ff_row_mdm_prefix_mdr_minor_dimensionsminornonzeroevaluationdeterminanthscm_positive ff_column_mdm_prefix_mdr_minor_dimensionsminornonzeroevaluationdeterminanthscm_positive ff_value_mdm_prefix_mdr_minor_dimensionsminornonzeroevaluationdeterminanthscm_positive. (ff_index_mdm_prefix_mdr_minor_dimensionsminornonzeroevaluationdeterminanthscm_positive = (mdr_q_minor_dimensionsminornonzeroevaluationdeterminanths) * ff_row_mdm_prefix_mdr_minor_dimensionsminornonzeroevaluationdeterminanthscm_positive + ff_column_mdm_prefix_mdr_minor_dimensionsminornonzeroevaluationdeterminanthscm_positive /\ ((exists ff_gap_mdm_lt_mdr_minor_dimensionsminornonzeroevaluationdeterminanthscm_positive_column_bound. ff_gap_mdm_lt_mdr_minor_dimensionsminornonzeroevaluationdeterminanthscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_minor_dimensionsminornonzeroevaluationdeterminanthscm_positive) = (mdr_q_minor_dimensionsminornonzeroevaluationdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_minor_dimensionsminornonzeroevaluationdeterminanthscm_positive_cell ff_column_mdm_cell_mdr_minor_dimensionsminornonzeroevaluationdeterminanthscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_minor_dimensionsminornonzeroevaluationdeterminanthscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_minor_dimensionsminornonzeroevaluationdeterminanthscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_minor_dimensionsminornonzeroevaluationdeterminanthscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_minor_dimensionsminornonzeroevaluationdeterminanthscm_positive_cell = ff_row_mdm_prefix_mdr_minor_dimensionsminornonzeroevaluationdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_minor_dimensionsminornonzeroevaluationdeterminanthscm_positive_cell_row_after. ff_gap_mdm_le_mdr_minor_dimensionsminornonzeroevaluationdeterminanthscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_minor_dimensionsminornonzeroevaluationdeterminanthscm_positive)) /\ ff_row_mdm_cell_mdr_minor_dimensionsminornonzeroevaluationdeterminanthscm_positive_cell = S ff_row_mdm_prefix_mdr_minor_dimensionsminornonzeroevaluationdeterminanthscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_minor_dimensionsminornonzeroevaluationdeterminanthscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_minor_dimensionsminornonzeroevaluationdeterminanthscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_minor_dimensionsminornonzeroevaluationdeterminanthscm_positive) = (mdr_j_minor_dimensionsminornonzeroevaluationdeterminanthsc)) /\ ff_column_mdm_cell_mdr_minor_dimensionsminornonzeroevaluationdeterminanthscm_positive_cell = ff_column_mdm_prefix_mdr_minor_dimensionsminornonzeroevaluationdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_minor_dimensionsminornonzeroevaluationdeterminanthscm_positive_cell_column_after. ff_gap_mdm_le_mdr_minor_dimensionsminornonzeroevaluationdeterminanthscm_positive_cell_column_after + (mdr_j_minor_dimensionsminornonzeroevaluationdeterminanthsc) = (ff_column_mdm_prefix_mdr_minor_dimensionsminornonzeroevaluationdeterminanthscm_positive)) /\ ff_column_mdm_cell_mdr_minor_dimensionsminornonzeroevaluationdeterminanthscm_positive_cell = S ff_column_mdm_prefix_mdr_minor_dimensionsminornonzeroevaluationdeterminanthscm_positive))) /\ (((exists ff_h_mdm_mdr_minor_dimensionsminornonzeroevaluationdeterminanthscm_positive_cell_source. ff_h_mdm_mdr_minor_dimensionsminornonzeroevaluationdeterminanthscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_minor_dimensionsminornonzeroevaluationdeterminanthscm_positive) = S ((S ((ff_row_mdm_cell_mdr_minor_dimensionsminornonzeroevaluationdeterminanthscm_positive_cell) * (S (mdr_q_minor_dimensionsminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_minor_dimensionsminornonzeroevaluationdeterminanthscm_positive_cell))) * mdr_pc_minor_dimensionsminornonzeroevaluationdeterminanth)) /\ exists ff_q_mdm_mdr_minor_dimensionsminornonzeroevaluationdeterminanthscm_positive_cell_source. mdr_pb_minor_dimensionsminornonzeroevaluationdeterminanth = ff_q_mdm_mdr_minor_dimensionsminornonzeroevaluationdeterminanthscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_minor_dimensionsminornonzeroevaluationdeterminanthscm_positive_cell) * (S (mdr_q_minor_dimensionsminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_minor_dimensionsminornonzeroevaluationdeterminanthscm_positive_cell))) * mdr_pc_minor_dimensionsminornonzeroevaluationdeterminanth) + (ff_value_mdm_prefix_mdr_minor_dimensionsminornonzeroevaluationdeterminanthscm_positive)))))) /\ (((exists ff_h_mdm_mdr_minor_dimensionsminornonzeroevaluationdeterminanthscm_positive_target. ff_h_mdm_mdr_minor_dimensionsminornonzeroevaluationdeterminanthscm_positive_target + S (ff_value_mdm_prefix_mdr_minor_dimensionsminornonzeroevaluationdeterminanthscm_positive) = S ((S (ff_index_mdm_prefix_mdr_minor_dimensionsminornonzeroevaluationdeterminanthscm_positive)) * mdr_us_minor_dimensionsminornonzeroevaluationdeterminanthsc)) /\ exists ff_q_mdm_mdr_minor_dimensionsminornonzeroevaluationdeterminanthscm_positive_target. mdr_up_minor_dimensionsminornonzeroevaluationdeterminanthsc = ff_q_mdm_mdr_minor_dimensionsminornonzeroevaluationdeterminanthscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_minor_dimensionsminornonzeroevaluationdeterminanthscm_positive)) * mdr_us_minor_dimensionsminornonzeroevaluationdeterminanthsc) + (ff_value_mdm_prefix_mdr_minor_dimensionsminornonzeroevaluationdeterminanthscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_minor_dimensionsminornonzeroevaluationdeterminanthscm_negative. (exists ff_gap_mdm_lt_mdr_minor_dimensionsminornonzeroevaluationdeterminanthscm_negative_index_bound. ff_gap_mdm_lt_mdr_minor_dimensionsminornonzeroevaluationdeterminanthscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_minor_dimensionsminornonzeroevaluationdeterminanthscm_negative) = ((mdr_q_minor_dimensionsminornonzeroevaluationdeterminanths) * (mdr_q_minor_dimensionsminornonzeroevaluationdeterminanths))) -> exists ff_row_mdm_prefix_mdr_minor_dimensionsminornonzeroevaluationdeterminanthscm_negative ff_column_mdm_prefix_mdr_minor_dimensionsminornonzeroevaluationdeterminanthscm_negative ff_value_mdm_prefix_mdr_minor_dimensionsminornonzeroevaluationdeterminanthscm_negative. (ff_index_mdm_prefix_mdr_minor_dimensionsminornonzeroevaluationdeterminanthscm_negative = (mdr_q_minor_dimensionsminornonzeroevaluationdeterminanths) * ff_row_mdm_prefix_mdr_minor_dimensionsminornonzeroevaluationdeterminanthscm_negative + ff_column_mdm_prefix_mdr_minor_dimensionsminornonzeroevaluationdeterminanthscm_negative /\ ((exists ff_gap_mdm_lt_mdr_minor_dimensionsminornonzeroevaluationdeterminanthscm_negative_column_bound. ff_gap_mdm_lt_mdr_minor_dimensionsminornonzeroevaluationdeterminanthscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_minor_dimensionsminornonzeroevaluationdeterminanthscm_negative) = (mdr_q_minor_dimensionsminornonzeroevaluationdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_minor_dimensionsminornonzeroevaluationdeterminanthscm_negative_cell ff_column_mdm_cell_mdr_minor_dimensionsminornonzeroevaluationdeterminanthscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_minor_dimensionsminornonzeroevaluationdeterminanthscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_minor_dimensionsminornonzeroevaluationdeterminanthscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_minor_dimensionsminornonzeroevaluationdeterminanthscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_minor_dimensionsminornonzeroevaluationdeterminanthscm_negative_cell = ff_row_mdm_prefix_mdr_minor_dimensionsminornonzeroevaluationdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_minor_dimensionsminornonzeroevaluationdeterminanthscm_negative_cell_row_after. ff_gap_mdm_le_mdr_minor_dimensionsminornonzeroevaluationdeterminanthscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_minor_dimensionsminornonzeroevaluationdeterminanthscm_negative)) /\ ff_row_mdm_cell_mdr_minor_dimensionsminornonzeroevaluationdeterminanthscm_negative_cell = S ff_row_mdm_prefix_mdr_minor_dimensionsminornonzeroevaluationdeterminanthscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_minor_dimensionsminornonzeroevaluationdeterminanthscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_minor_dimensionsminornonzeroevaluationdeterminanthscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_minor_dimensionsminornonzeroevaluationdeterminanthscm_negative) = (mdr_j_minor_dimensionsminornonzeroevaluationdeterminanthsc)) /\ ff_column_mdm_cell_mdr_minor_dimensionsminornonzeroevaluationdeterminanthscm_negative_cell = ff_column_mdm_prefix_mdr_minor_dimensionsminornonzeroevaluationdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_minor_dimensionsminornonzeroevaluationdeterminanthscm_negative_cell_column_after. ff_gap_mdm_le_mdr_minor_dimensionsminornonzeroevaluationdeterminanthscm_negative_cell_column_after + (mdr_j_minor_dimensionsminornonzeroevaluationdeterminanthsc) = (ff_column_mdm_prefix_mdr_minor_dimensionsminornonzeroevaluationdeterminanthscm_negative)) /\ ff_column_mdm_cell_mdr_minor_dimensionsminornonzeroevaluationdeterminanthscm_negative_cell = S ff_column_mdm_prefix_mdr_minor_dimensionsminornonzeroevaluationdeterminanthscm_negative))) /\ (((exists ff_h_mdm_mdr_minor_dimensionsminornonzeroevaluationdeterminanthscm_negative_cell_source. ff_h_mdm_mdr_minor_dimensionsminornonzeroevaluationdeterminanthscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_minor_dimensionsminornonzeroevaluationdeterminanthscm_negative) = S ((S ((ff_row_mdm_cell_mdr_minor_dimensionsminornonzeroevaluationdeterminanthscm_negative_cell) * (S (mdr_q_minor_dimensionsminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_minor_dimensionsminornonzeroevaluationdeterminanthscm_negative_cell))) * mdr_nc_minor_dimensionsminornonzeroevaluationdeterminanth)) /\ exists ff_q_mdm_mdr_minor_dimensionsminornonzeroevaluationdeterminanthscm_negative_cell_source. mdr_nb_minor_dimensionsminornonzeroevaluationdeterminanth = ff_q_mdm_mdr_minor_dimensionsminornonzeroevaluationdeterminanthscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_minor_dimensionsminornonzeroevaluationdeterminanthscm_negative_cell) * (S (mdr_q_minor_dimensionsminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_minor_dimensionsminornonzeroevaluationdeterminanthscm_negative_cell))) * mdr_nc_minor_dimensionsminornonzeroevaluationdeterminanth) + (ff_value_mdm_prefix_mdr_minor_dimensionsminornonzeroevaluationdeterminanthscm_negative)))))) /\ (((exists ff_h_mdm_mdr_minor_dimensionsminornonzeroevaluationdeterminanthscm_negative_target. ff_h_mdm_mdr_minor_dimensionsminornonzeroevaluationdeterminanthscm_negative_target + S (ff_value_mdm_prefix_mdr_minor_dimensionsminornonzeroevaluationdeterminanthscm_negative) = S ((S (ff_index_mdm_prefix_mdr_minor_dimensionsminornonzeroevaluationdeterminanthscm_negative)) * mdr_ut_minor_dimensionsminornonzeroevaluationdeterminanthsc)) /\ exists ff_q_mdm_mdr_minor_dimensionsminornonzeroevaluationdeterminanthscm_negative_target. mdr_un_minor_dimensionsminornonzeroevaluationdeterminanthsc = ff_q_mdm_mdr_minor_dimensionsminornonzeroevaluationdeterminanthscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_minor_dimensionsminornonzeroevaluationdeterminanthscm_negative)) * mdr_ut_minor_dimensionsminornonzeroevaluationdeterminanthsc) + (ff_value_mdm_prefix_mdr_minor_dimensionsminornonzeroevaluationdeterminanthscm_negative))))))))) /\ ((((exists ff_h_mdr_minor_dimensionsminornonzeroevaluationdeterminanthscp. ff_h_mdr_minor_dimensionsminornonzeroevaluationdeterminanthscp + S (mdr_p_minor_dimensionsminornonzeroevaluationdeterminanthsc) = S ((S (mdr_j_minor_dimensionsminornonzeroevaluationdeterminanthsc)) * mdr_ec_minor_dimensionsminornonzeroevaluationdeterminanths)) /\ exists ff_q_mdr_minor_dimensionsminornonzeroevaluationdeterminanthscp. mdr_eb_minor_dimensionsminornonzeroevaluationdeterminanths = ff_q_mdr_minor_dimensionsminornonzeroevaluationdeterminanthscp * S ((S (mdr_j_minor_dimensionsminornonzeroevaluationdeterminanthsc)) * mdr_ec_minor_dimensionsminornonzeroevaluationdeterminanths) + (mdr_p_minor_dimensionsminornonzeroevaluationdeterminanthsc))) /\ (((exists ff_h_mdr_minor_dimensionsminornonzeroevaluationdeterminanthscn. ff_h_mdr_minor_dimensionsminornonzeroevaluationdeterminanthscn + S (mdr_n_minor_dimensionsminornonzeroevaluationdeterminanthsc) = S ((S (mdr_j_minor_dimensionsminornonzeroevaluationdeterminanthsc)) * mdr_fc_minor_dimensionsminornonzeroevaluationdeterminanths)) /\ exists ff_q_mdr_minor_dimensionsminornonzeroevaluationdeterminanthscn. mdr_fb_minor_dimensionsminornonzeroevaluationdeterminanths = ff_q_mdr_minor_dimensionsminornonzeroevaluationdeterminanthscn * S ((S (mdr_j_minor_dimensionsminornonzeroevaluationdeterminanthsc)) * mdr_fc_minor_dimensionsminornonzeroevaluationdeterminanths) + (mdr_n_minor_dimensionsminornonzeroevaluationdeterminanthsc)))))))) /\ (exists ff_ub_mce_fold_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf ff_uc_mce_fold_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf ff_vb_mce_fold_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf ff_vc_mce_fold_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf. ((forall ff_index_mce_alternating_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_prefix. (exists ff_gap_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_prefix_index. ff_gap_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_prefix_index + S (ff_index_mce_alternating_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_prefix) = (S (mdr_q_minor_dimensionsminornonzeroevaluationdeterminanths))) -> exists ff_ap_mce_alternating_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_prefix ff_an_mce_alternating_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_prefix ff_bp_mce_alternating_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_prefix ff_bn_mce_alternating_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_prefix ff_p_mce_alternating_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_prefix ff_n_mce_alternating_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_prefix. ((((exists ff_h_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_prefix_ap. ff_h_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_prefix_ap + S (ff_ap_mce_alternating_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_prefix)) * mdr_pc_minor_dimensionsminornonzeroevaluationdeterminanth)) /\ exists ff_q_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_prefix_ap. mdr_pb_minor_dimensionsminornonzeroevaluationdeterminanth = ff_q_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_prefix)) * mdr_pc_minor_dimensionsminornonzeroevaluationdeterminanth) + (ff_ap_mce_alternating_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_prefix_an. ff_h_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_prefix_an + S (ff_an_mce_alternating_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_prefix)) * mdr_nc_minor_dimensionsminornonzeroevaluationdeterminanth)) /\ exists ff_q_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_prefix_an. mdr_nb_minor_dimensionsminornonzeroevaluationdeterminanth = ff_q_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_prefix)) * mdr_nc_minor_dimensionsminornonzeroevaluationdeterminanth) + (ff_an_mce_alternating_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_prefix_bp. ff_h_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_prefix_bp + S (ff_bp_mce_alternating_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_prefix)) * mdr_ec_minor_dimensionsminornonzeroevaluationdeterminanths)) /\ exists ff_q_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_prefix_bp. mdr_eb_minor_dimensionsminornonzeroevaluationdeterminanths = ff_q_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_prefix)) * mdr_ec_minor_dimensionsminornonzeroevaluationdeterminanths) + (ff_bp_mce_alternating_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_prefix_bn. ff_h_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_prefix_bn + S (ff_bn_mce_alternating_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_prefix)) * mdr_fc_minor_dimensionsminornonzeroevaluationdeterminanths)) /\ exists ff_q_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_prefix_bn. mdr_fb_minor_dimensionsminornonzeroevaluationdeterminanths = ff_q_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_prefix)) * mdr_fc_minor_dimensionsminornonzeroevaluationdeterminanths) + (ff_bn_mce_alternating_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_prefix_positive. ff_h_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_prefix_positive + S (ff_p_mce_alternating_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_prefix_positive. ff_ub_mce_fold_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf) + (ff_p_mce_alternating_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_prefix_negative. ff_h_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_prefix_negative + S (ff_n_mce_alternating_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_prefix_negative. ff_vb_mce_fold_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf) + (ff_n_mce_alternating_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_prefix))) /\ (((exists ff_even_mce_term_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_prefix = 2 * ff_even_mce_term_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_prefix_term) /\ (ff_p_mce_alternating_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_prefix = 2 * ff_odd_mce_term_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_positive ff_v_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_positive. ((((exists ff_h_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_positive_start. ff_h_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_positive_start. ff_u_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_positive_start * S ((S (0)) * ff_v_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_positive_terminal. ff_h_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_positive_terminal + S (mdr_p_minor_dimensionsminornonzeroevaluationdeterminanth) = S ((S ((S (mdr_q_minor_dimensionsminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_positive_terminal. ff_u_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_positive_terminal * S ((S ((S (mdr_q_minor_dimensionsminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_positive) + (mdr_p_minor_dimensionsminornonzeroevaluationdeterminanth))) /\ forall ff_i_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_positive. (exists ff_lt_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_positive_bound. ff_lt_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_positive_bound + S ff_i_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_positive = (S (mdr_q_minor_dimensionsminornonzeroevaluationdeterminanths))) -> exists ff_a_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_positive ff_r_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_positive ff_s_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_positive. ((((exists ff_h_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_positive_summand. ff_h_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_positive_summand + S (ff_a_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_positive_summand. ff_ub_mce_fold_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_positive_summand * S ((S (ff_i_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf) + (ff_a_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_positive_partial. ff_h_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_positive_partial + S (ff_r_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_positive_partial. ff_u_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_positive_partial * S ((S (ff_i_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_positive) + (ff_r_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_positive_successor. ff_h_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_positive_successor + S (ff_s_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_positive) = S ((S (S ff_i_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_positive_successor. ff_u_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_positive_successor * S ((S (S ff_i_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_positive) + (ff_s_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_positive))) /\ ff_s_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_positive = ff_r_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_positive + ff_a_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_positive)))))) /\ (exists ff_u_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_negative ff_v_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_negative. ((((exists ff_h_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_negative_start. ff_h_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_negative_start. ff_u_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_negative_start * S ((S (0)) * ff_v_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_negative_terminal. ff_h_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_negative_terminal + S (mdr_n_minor_dimensionsminornonzeroevaluationdeterminanth) = S ((S ((S (mdr_q_minor_dimensionsminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_negative_terminal. ff_u_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_negative_terminal * S ((S ((S (mdr_q_minor_dimensionsminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_negative) + (mdr_n_minor_dimensionsminornonzeroevaluationdeterminanth))) /\ forall ff_i_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_negative. (exists ff_lt_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_negative_bound. ff_lt_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_negative_bound + S ff_i_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_negative = (S (mdr_q_minor_dimensionsminornonzeroevaluationdeterminanths))) -> exists ff_a_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_negative ff_r_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_negative ff_s_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_negative. ((((exists ff_h_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_negative_summand. ff_h_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_negative_summand + S (ff_a_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_negative_summand. ff_vb_mce_fold_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_negative_summand * S ((S (ff_i_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf) + (ff_a_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_negative_partial. ff_h_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_negative_partial + S (ff_r_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_negative_partial. ff_u_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_negative_partial * S ((S (ff_i_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_negative) + (ff_r_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_negative_successor. ff_h_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_negative_successor + S (ff_s_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_negative) = S ((S (S ff_i_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_negative_successor. ff_u_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_negative_successor * S ((S (S ff_i_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_negative) + (ff_s_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_negative))) /\ ff_s_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_negative = ff_r_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_negative + ff_a_mce_mdr_minor_dimensionsminornonzeroevaluationdeterminanthsf_negative))))))))))))))) /\ ((exists mdr_gap_minor_dimensionsminornonzeroevaluationdeterminanti. mdr_gap_minor_dimensionsminornonzeroevaluationdeterminanti + S (mdr_i_minor_dimensionsminornonzeroevaluationdeterminant) = (mdr_l_minor_dimensionsminornonzeroevaluationdeterminant)) /\ (exists mdr_z_minor_dimensionsminornonzeroevaluationdeterminantr. ((exists mdr_a_minor_dimensionsminornonzeroevaluationdeterminantrc mdr_b_minor_dimensionsminornonzeroevaluationdeterminantrc mdr_c_minor_dimensionsminornonzeroevaluationdeterminantrc mdr_e_minor_dimensionsminornonzeroevaluationdeterminantrc mdr_f_minor_dimensionsminornonzeroevaluationdeterminantrc. ((mdr_a_minor_dimensionsminornonzeroevaluationdeterminantrc = ((q) + (mdr_ub_minor_dimensionsminornonzeroevaluation)) * S ((q) + (mdr_ub_minor_dimensionsminornonzeroevaluation)) + ((mdr_ub_minor_dimensionsminornonzeroevaluation) + (mdr_ub_minor_dimensionsminornonzeroevaluation))) /\ ((mdr_b_minor_dimensionsminornonzeroevaluationdeterminantrc = ((mdr_uc_minor_dimensionsminornonzeroevaluation) + (mdr_vb_minor_dimensionsminornonzeroevaluation)) * S ((mdr_uc_minor_dimensionsminornonzeroevaluation) + (mdr_vb_minor_dimensionsminornonzeroevaluation)) + ((mdr_vb_minor_dimensionsminornonzeroevaluation) + (mdr_vb_minor_dimensionsminornonzeroevaluation))) /\ ((mdr_c_minor_dimensionsminornonzeroevaluationdeterminantrc = ((mdr_a_minor_dimensionsminornonzeroevaluationdeterminantrc) + (mdr_b_minor_dimensionsminornonzeroevaluationdeterminantrc)) * S ((mdr_a_minor_dimensionsminornonzeroevaluationdeterminantrc) + (mdr_b_minor_dimensionsminornonzeroevaluationdeterminantrc)) + ((mdr_b_minor_dimensionsminornonzeroevaluationdeterminantrc) + (mdr_b_minor_dimensionsminornonzeroevaluationdeterminantrc))) /\ ((mdr_e_minor_dimensionsminornonzeroevaluationdeterminantrc = ((mdr_p_minor_dimensionsminornonzero) + (mdr_n_minor_dimensionsminornonzero)) * S ((mdr_p_minor_dimensionsminornonzero) + (mdr_n_minor_dimensionsminornonzero)) + ((mdr_n_minor_dimensionsminornonzero) + (mdr_n_minor_dimensionsminornonzero))) /\ ((mdr_f_minor_dimensionsminornonzeroevaluationdeterminantrc = ((mdr_vc_minor_dimensionsminornonzeroevaluation) + (mdr_e_minor_dimensionsminornonzeroevaluationdeterminantrc)) * S ((mdr_vc_minor_dimensionsminornonzeroevaluation) + (mdr_e_minor_dimensionsminornonzeroevaluationdeterminantrc)) + ((mdr_e_minor_dimensionsminornonzeroevaluationdeterminantrc) + (mdr_e_minor_dimensionsminornonzeroevaluationdeterminantrc))) /\ ((mdr_z_minor_dimensionsminornonzeroevaluationdeterminantr) = ((mdr_c_minor_dimensionsminornonzeroevaluationdeterminantrc) + (mdr_f_minor_dimensionsminornonzeroevaluationdeterminantrc)) * S ((mdr_c_minor_dimensionsminornonzeroevaluationdeterminantrc) + (mdr_f_minor_dimensionsminornonzeroevaluationdeterminantrc)) + ((mdr_f_minor_dimensionsminornonzeroevaluationdeterminantrc) + (mdr_f_minor_dimensionsminornonzeroevaluationdeterminantrc))))))))) /\ (((exists ff_h_mdr_minor_dimensionsminornonzeroevaluationdeterminantrb. ff_h_mdr_minor_dimensionsminornonzeroevaluationdeterminantrb + S (mdr_z_minor_dimensionsminornonzeroevaluationdeterminantr) = S ((S (mdr_i_minor_dimensionsminornonzeroevaluationdeterminant)) * mdr_c_minor_dimensionsminornonzeroevaluationdeterminant)) /\ exists ff_q_mdr_minor_dimensionsminornonzeroevaluationdeterminantrb. mdr_b_minor_dimensionsminornonzeroevaluationdeterminant = ff_q_mdr_minor_dimensionsminornonzeroevaluationdeterminantrb * S ((S (mdr_i_minor_dimensionsminornonzeroevaluationdeterminant)) * mdr_c_minor_dimensionsminornonzeroevaluationdeterminant) + (mdr_z_minor_dimensionsminornonzeroevaluationdeterminantr)))))))))) /\ (~(mdr_p_minor_dimensionsminornonzero = mdr_n_minor_dimensionsminornonzero)))))))) -> (((exists mdr_gap_minor_rows_bound. mdr_gap_minor_rows_bound + (q) = (r)) /\ (exists mdr_gap_minor_columns_bound. mdr_gap_minor_columns_bound + (q) = (w))))