matrix_rank_nonzero_minor_empty

Exact expanded first-order arithmetic statement

forall pb pc nb nc r w. (exists mdr_rb_minor_empty mdr_rc_minor_empty mdr_cb_minor_empty mdr_cc_minor_empty. (((((forall fom_index_mrf_minor_emptyminorrowsbound. (exists fom_gap_mrf_minor_emptyminorrowsbound_index_bound. fom_gap_mrf_minor_emptyminorrowsbound_index_bound + S (fom_index_mrf_minor_emptyminorrowsbound) = 0) -> exists fom_value_mrf_minor_emptyminorrowsbound. ((((exists fom_beta_height_mrf_minor_emptyminorrowsbound_entry. fom_beta_height_mrf_minor_emptyminorrowsbound_entry + S (fom_value_mrf_minor_emptyminorrowsbound) = S ((S (fom_index_mrf_minor_emptyminorrowsbound)) * mdr_rc_minor_empty)) /\ exists fom_beta_quotient_mrf_minor_emptyminorrowsbound_entry. mdr_rb_minor_empty = fom_beta_quotient_mrf_minor_emptyminorrowsbound_entry * S ((S (fom_index_mrf_minor_emptyminorrowsbound)) * mdr_rc_minor_empty) + (fom_value_mrf_minor_emptyminorrowsbound))) /\ (exists fom_gap_mrf_minor_emptyminorrowsbound_value_bound. fom_gap_mrf_minor_emptyminorrowsbound_value_bound + S (fom_value_mrf_minor_emptyminorrowsbound) = r))) /\ (forall mdr_i_minor_emptyminorrowsdistinct mdr_j_minor_emptyminorrowsdistinct mdr_a_minor_emptyminorrowsdistinct. (exists mdr_gap_minor_emptyminorrowsdistincti. mdr_gap_minor_emptyminorrowsdistincti + S (mdr_i_minor_emptyminorrowsdistinct) = (0)) -> (exists mdr_gap_minor_emptyminorrowsdistinctj. mdr_gap_minor_emptyminorrowsdistinctj + S (mdr_j_minor_emptyminorrowsdistinct) = (0)) -> (((exists ff_h_mdr_minor_emptyminorrowsdistinctfirst. ff_h_mdr_minor_emptyminorrowsdistinctfirst + S (mdr_a_minor_emptyminorrowsdistinct) = S ((S (mdr_i_minor_emptyminorrowsdistinct)) * mdr_rc_minor_empty)) /\ exists ff_q_mdr_minor_emptyminorrowsdistinctfirst. mdr_rb_minor_empty = ff_q_mdr_minor_emptyminorrowsdistinctfirst * S ((S (mdr_i_minor_emptyminorrowsdistinct)) * mdr_rc_minor_empty) + (mdr_a_minor_emptyminorrowsdistinct))) -> (((exists ff_h_mdr_minor_emptyminorrowsdistinctsecond. ff_h_mdr_minor_emptyminorrowsdistinctsecond + S (mdr_a_minor_emptyminorrowsdistinct) = S ((S (mdr_j_minor_emptyminorrowsdistinct)) * mdr_rc_minor_empty)) /\ exists ff_q_mdr_minor_emptyminorrowsdistinctsecond. mdr_rb_minor_empty = ff_q_mdr_minor_emptyminorrowsdistinctsecond * S ((S (mdr_j_minor_emptyminorrowsdistinct)) * mdr_rc_minor_empty) + (mdr_a_minor_emptyminorrowsdistinct))) -> mdr_i_minor_emptyminorrowsdistinct = mdr_j_minor_emptyminorrowsdistinct))) /\ ((((forall fom_index_mrf_minor_emptyminorcolumnsbound. (exists fom_gap_mrf_minor_emptyminorcolumnsbound_index_bound. fom_gap_mrf_minor_emptyminorcolumnsbound_index_bound + S (fom_index_mrf_minor_emptyminorcolumnsbound) = 0) -> exists fom_value_mrf_minor_emptyminorcolumnsbound. ((((exists fom_beta_height_mrf_minor_emptyminorcolumnsbound_entry. fom_beta_height_mrf_minor_emptyminorcolumnsbound_entry + S (fom_value_mrf_minor_emptyminorcolumnsbound) = S ((S (fom_index_mrf_minor_emptyminorcolumnsbound)) * mdr_cc_minor_empty)) /\ exists fom_beta_quotient_mrf_minor_emptyminorcolumnsbound_entry. mdr_cb_minor_empty = fom_beta_quotient_mrf_minor_emptyminorcolumnsbound_entry * S ((S (fom_index_mrf_minor_emptyminorcolumnsbound)) * mdr_cc_minor_empty) + (fom_value_mrf_minor_emptyminorcolumnsbound))) /\ (exists fom_gap_mrf_minor_emptyminorcolumnsbound_value_bound. fom_gap_mrf_minor_emptyminorcolumnsbound_value_bound + S (fom_value_mrf_minor_emptyminorcolumnsbound) = w))) /\ (forall mdr_i_minor_emptyminorcolumnsdistinct mdr_j_minor_emptyminorcolumnsdistinct mdr_a_minor_emptyminorcolumnsdistinct. (exists mdr_gap_minor_emptyminorcolumnsdistincti. mdr_gap_minor_emptyminorcolumnsdistincti + S (mdr_i_minor_emptyminorcolumnsdistinct) = (0)) -> (exists mdr_gap_minor_emptyminorcolumnsdistinctj. mdr_gap_minor_emptyminorcolumnsdistinctj + S (mdr_j_minor_emptyminorcolumnsdistinct) = (0)) -> (((exists ff_h_mdr_minor_emptyminorcolumnsdistinctfirst. ff_h_mdr_minor_emptyminorcolumnsdistinctfirst + S (mdr_a_minor_emptyminorcolumnsdistinct) = S ((S (mdr_i_minor_emptyminorcolumnsdistinct)) * mdr_cc_minor_empty)) /\ exists ff_q_mdr_minor_emptyminorcolumnsdistinctfirst. mdr_cb_minor_empty = ff_q_mdr_minor_emptyminorcolumnsdistinctfirst * S ((S (mdr_i_minor_emptyminorcolumnsdistinct)) * mdr_cc_minor_empty) + (mdr_a_minor_emptyminorcolumnsdistinct))) -> (((exists ff_h_mdr_minor_emptyminorcolumnsdistinctsecond. ff_h_mdr_minor_emptyminorcolumnsdistinctsecond + S (mdr_a_minor_emptyminorcolumnsdistinct) = S ((S (mdr_j_minor_emptyminorcolumnsdistinct)) * mdr_cc_minor_empty)) /\ exists ff_q_mdr_minor_emptyminorcolumnsdistinctsecond. mdr_cb_minor_empty = ff_q_mdr_minor_emptyminorcolumnsdistinctsecond * S ((S (mdr_j_minor_emptyminorcolumnsdistinct)) * mdr_cc_minor_empty) + (mdr_a_minor_emptyminorcolumnsdistinct))) -> mdr_i_minor_emptyminorcolumnsdistinct = mdr_j_minor_emptyminorcolumnsdistinct))) /\ (exists mdr_p_minor_emptyminornonzero mdr_n_minor_emptyminornonzero. ((exists mdr_ub_minor_emptyminornonzeroevaluation mdr_uc_minor_emptyminornonzeroevaluation mdr_vb_minor_emptyminornonzeroevaluation mdr_vc_minor_emptyminornonzeroevaluation. ((((forall mdr_i_minor_emptyminornonzeroevaluationmatrixpositive. (exists mdr_gap_minor_emptyminornonzeroevaluationmatrixpositivebound. mdr_gap_minor_emptyminornonzeroevaluationmatrixpositivebound + S (mdr_i_minor_emptyminornonzeroevaluationmatrixpositive) = ((0) * (0))) -> exists mdr_a_minor_emptyminornonzeroevaluationmatrixpositive. (((exists mdr_r_minor_emptyminornonzeroevaluationmatrixpositivepoint mdr_s_minor_emptyminornonzeroevaluationmatrixpositivepoint mdr_u_minor_emptyminornonzeroevaluationmatrixpositivepoint mdr_v_minor_emptyminornonzeroevaluationmatrixpositivepoint. ((mdr_i_minor_emptyminornonzeroevaluationmatrixpositive = (0) * mdr_r_minor_emptyminornonzeroevaluationmatrixpositivepoint + mdr_s_minor_emptyminornonzeroevaluationmatrixpositivepoint) /\ ((exists mdr_gap_minor_emptyminornonzeroevaluationmatrixpositivepointcolumn. mdr_gap_minor_emptyminornonzeroevaluationmatrixpositivepointcolumn + S (mdr_s_minor_emptyminornonzeroevaluationmatrixpositivepoint) = (0)) /\ ((((exists ff_h_mdr_minor_emptyminornonzeroevaluationmatrixpositivepointrow_index. ff_h_mdr_minor_emptyminornonzeroevaluationmatrixpositivepointrow_index + S (mdr_u_minor_emptyminornonzeroevaluationmatrixpositivepoint) = S ((S (mdr_r_minor_emptyminornonzeroevaluationmatrixpositivepoint)) * mdr_rc_minor_empty)) /\ exists ff_q_mdr_minor_emptyminornonzeroevaluationmatrixpositivepointrow_index. mdr_rb_minor_empty = ff_q_mdr_minor_emptyminornonzeroevaluationmatrixpositivepointrow_index * S ((S (mdr_r_minor_emptyminornonzeroevaluationmatrixpositivepoint)) * mdr_rc_minor_empty) + (mdr_u_minor_emptyminornonzeroevaluationmatrixpositivepoint))) /\ ((((exists ff_h_mdr_minor_emptyminornonzeroevaluationmatrixpositivepointcolumn_index. ff_h_mdr_minor_emptyminornonzeroevaluationmatrixpositivepointcolumn_index + S (mdr_v_minor_emptyminornonzeroevaluationmatrixpositivepoint) = S ((S (mdr_s_minor_emptyminornonzeroevaluationmatrixpositivepoint)) * mdr_cc_minor_empty)) /\ exists ff_q_mdr_minor_emptyminornonzeroevaluationmatrixpositivepointcolumn_index. mdr_cb_minor_empty = ff_q_mdr_minor_emptyminornonzeroevaluationmatrixpositivepointcolumn_index * S ((S (mdr_s_minor_emptyminornonzeroevaluationmatrixpositivepoint)) * mdr_cc_minor_empty) + (mdr_v_minor_emptyminornonzeroevaluationmatrixpositivepoint))) /\ (((exists ff_h_mdr_minor_emptyminornonzeroevaluationmatrixpositivepointsource. ff_h_mdr_minor_emptyminornonzeroevaluationmatrixpositivepointsource + S (mdr_a_minor_emptyminornonzeroevaluationmatrixpositive) = S ((S ((mdr_u_minor_emptyminornonzeroevaluationmatrixpositivepoint) * (w) + (mdr_v_minor_emptyminornonzeroevaluationmatrixpositivepoint))) * pc)) /\ exists ff_q_mdr_minor_emptyminornonzeroevaluationmatrixpositivepointsource. pb = ff_q_mdr_minor_emptyminornonzeroevaluationmatrixpositivepointsource * S ((S ((mdr_u_minor_emptyminornonzeroevaluationmatrixpositivepoint) * (w) + (mdr_v_minor_emptyminornonzeroevaluationmatrixpositivepoint))) * pc) + (mdr_a_minor_emptyminornonzeroevaluationmatrixpositive)))))))) /\ (((exists ff_h_mdr_minor_emptyminornonzeroevaluationmatrixpositiveoutput. ff_h_mdr_minor_emptyminornonzeroevaluationmatrixpositiveoutput + S (mdr_a_minor_emptyminornonzeroevaluationmatrixpositive) = S ((S (mdr_i_minor_emptyminornonzeroevaluationmatrixpositive)) * mdr_uc_minor_emptyminornonzeroevaluation)) /\ exists ff_q_mdr_minor_emptyminornonzeroevaluationmatrixpositiveoutput. mdr_ub_minor_emptyminornonzeroevaluation = ff_q_mdr_minor_emptyminornonzeroevaluationmatrixpositiveoutput * S ((S (mdr_i_minor_emptyminornonzeroevaluationmatrixpositive)) * mdr_uc_minor_emptyminornonzeroevaluation) + (mdr_a_minor_emptyminornonzeroevaluationmatrixpositive)))))) /\ (forall mdr_i_minor_emptyminornonzeroevaluationmatrixnegative. (exists mdr_gap_minor_emptyminornonzeroevaluationmatrixnegativebound. mdr_gap_minor_emptyminornonzeroevaluationmatrixnegativebound + S (mdr_i_minor_emptyminornonzeroevaluationmatrixnegative) = ((0) * (0))) -> exists mdr_a_minor_emptyminornonzeroevaluationmatrixnegative. (((exists mdr_r_minor_emptyminornonzeroevaluationmatrixnegativepoint mdr_s_minor_emptyminornonzeroevaluationmatrixnegativepoint mdr_u_minor_emptyminornonzeroevaluationmatrixnegativepoint mdr_v_minor_emptyminornonzeroevaluationmatrixnegativepoint. ((mdr_i_minor_emptyminornonzeroevaluationmatrixnegative = (0) * mdr_r_minor_emptyminornonzeroevaluationmatrixnegativepoint + mdr_s_minor_emptyminornonzeroevaluationmatrixnegativepoint) /\ ((exists mdr_gap_minor_emptyminornonzeroevaluationmatrixnegativepointcolumn. mdr_gap_minor_emptyminornonzeroevaluationmatrixnegativepointcolumn + S (mdr_s_minor_emptyminornonzeroevaluationmatrixnegativepoint) = (0)) /\ ((((exists ff_h_mdr_minor_emptyminornonzeroevaluationmatrixnegativepointrow_index. ff_h_mdr_minor_emptyminornonzeroevaluationmatrixnegativepointrow_index + S (mdr_u_minor_emptyminornonzeroevaluationmatrixnegativepoint) = S ((S (mdr_r_minor_emptyminornonzeroevaluationmatrixnegativepoint)) * mdr_rc_minor_empty)) /\ exists ff_q_mdr_minor_emptyminornonzeroevaluationmatrixnegativepointrow_index. mdr_rb_minor_empty = ff_q_mdr_minor_emptyminornonzeroevaluationmatrixnegativepointrow_index * S ((S (mdr_r_minor_emptyminornonzeroevaluationmatrixnegativepoint)) * mdr_rc_minor_empty) + (mdr_u_minor_emptyminornonzeroevaluationmatrixnegativepoint))) /\ ((((exists ff_h_mdr_minor_emptyminornonzeroevaluationmatrixnegativepointcolumn_index. ff_h_mdr_minor_emptyminornonzeroevaluationmatrixnegativepointcolumn_index + S (mdr_v_minor_emptyminornonzeroevaluationmatrixnegativepoint) = S ((S (mdr_s_minor_emptyminornonzeroevaluationmatrixnegativepoint)) * mdr_cc_minor_empty)) /\ exists ff_q_mdr_minor_emptyminornonzeroevaluationmatrixnegativepointcolumn_index. mdr_cb_minor_empty = ff_q_mdr_minor_emptyminornonzeroevaluationmatrixnegativepointcolumn_index * S ((S (mdr_s_minor_emptyminornonzeroevaluationmatrixnegativepoint)) * mdr_cc_minor_empty) + (mdr_v_minor_emptyminornonzeroevaluationmatrixnegativepoint))) /\ (((exists ff_h_mdr_minor_emptyminornonzeroevaluationmatrixnegativepointsource. ff_h_mdr_minor_emptyminornonzeroevaluationmatrixnegativepointsource + S (mdr_a_minor_emptyminornonzeroevaluationmatrixnegative) = S ((S ((mdr_u_minor_emptyminornonzeroevaluationmatrixnegativepoint) * (w) + (mdr_v_minor_emptyminornonzeroevaluationmatrixnegativepoint))) * nc)) /\ exists ff_q_mdr_minor_emptyminornonzeroevaluationmatrixnegativepointsource. nb = ff_q_mdr_minor_emptyminornonzeroevaluationmatrixnegativepointsource * S ((S ((mdr_u_minor_emptyminornonzeroevaluationmatrixnegativepoint) * (w) + (mdr_v_minor_emptyminornonzeroevaluationmatrixnegativepoint))) * nc) + (mdr_a_minor_emptyminornonzeroevaluationmatrixnegative)))))))) /\ (((exists ff_h_mdr_minor_emptyminornonzeroevaluationmatrixnegativeoutput. ff_h_mdr_minor_emptyminornonzeroevaluationmatrixnegativeoutput + S (mdr_a_minor_emptyminornonzeroevaluationmatrixnegative) = S ((S (mdr_i_minor_emptyminornonzeroevaluationmatrixnegative)) * mdr_vc_minor_emptyminornonzeroevaluation)) /\ exists ff_q_mdr_minor_emptyminornonzeroevaluationmatrixnegativeoutput. mdr_vb_minor_emptyminornonzeroevaluation = ff_q_mdr_minor_emptyminornonzeroevaluationmatrixnegativeoutput * S ((S (mdr_i_minor_emptyminornonzeroevaluationmatrixnegative)) * mdr_vc_minor_emptyminornonzeroevaluation) + (mdr_a_minor_emptyminornonzeroevaluationmatrixnegative)))))))) /\ (exists mdr_b_minor_emptyminornonzeroevaluationdeterminant mdr_c_minor_emptyminornonzeroevaluationdeterminant mdr_l_minor_emptyminornonzeroevaluationdeterminant mdr_i_minor_emptyminornonzeroevaluationdeterminant. ((forall mdr_i_minor_emptyminornonzeroevaluationdeterminanth. (exists mdr_gap_minor_emptyminornonzeroevaluationdeterminanthi. mdr_gap_minor_emptyminornonzeroevaluationdeterminanthi + S (mdr_i_minor_emptyminornonzeroevaluationdeterminanth) = (mdr_l_minor_emptyminornonzeroevaluationdeterminant)) -> exists mdr_d_minor_emptyminornonzeroevaluationdeterminanth mdr_pb_minor_emptyminornonzeroevaluationdeterminanth mdr_pc_minor_emptyminornonzeroevaluationdeterminanth mdr_nb_minor_emptyminornonzeroevaluationdeterminanth mdr_nc_minor_emptyminornonzeroevaluationdeterminanth mdr_p_minor_emptyminornonzeroevaluationdeterminanth mdr_n_minor_emptyminornonzeroevaluationdeterminanth. ((exists mdr_z_minor_emptyminornonzeroevaluationdeterminanthr. ((exists mdr_a_minor_emptyminornonzeroevaluationdeterminanthrc mdr_b_minor_emptyminornonzeroevaluationdeterminanthrc mdr_c_minor_emptyminornonzeroevaluationdeterminanthrc mdr_e_minor_emptyminornonzeroevaluationdeterminanthrc mdr_f_minor_emptyminornonzeroevaluationdeterminanthrc. ((mdr_a_minor_emptyminornonzeroevaluationdeterminanthrc = ((mdr_d_minor_emptyminornonzeroevaluationdeterminanth) + (mdr_pb_minor_emptyminornonzeroevaluationdeterminanth)) * S ((mdr_d_minor_emptyminornonzeroevaluationdeterminanth) + (mdr_pb_minor_emptyminornonzeroevaluationdeterminanth)) + ((mdr_pb_minor_emptyminornonzeroevaluationdeterminanth) + (mdr_pb_minor_emptyminornonzeroevaluationdeterminanth))) /\ ((mdr_b_minor_emptyminornonzeroevaluationdeterminanthrc = ((mdr_pc_minor_emptyminornonzeroevaluationdeterminanth) + (mdr_nb_minor_emptyminornonzeroevaluationdeterminanth)) * S ((mdr_pc_minor_emptyminornonzeroevaluationdeterminanth) + (mdr_nb_minor_emptyminornonzeroevaluationdeterminanth)) + ((mdr_nb_minor_emptyminornonzeroevaluationdeterminanth) + (mdr_nb_minor_emptyminornonzeroevaluationdeterminanth))) /\ ((mdr_c_minor_emptyminornonzeroevaluationdeterminanthrc = ((mdr_a_minor_emptyminornonzeroevaluationdeterminanthrc) + (mdr_b_minor_emptyminornonzeroevaluationdeterminanthrc)) * S ((mdr_a_minor_emptyminornonzeroevaluationdeterminanthrc) + (mdr_b_minor_emptyminornonzeroevaluationdeterminanthrc)) + ((mdr_b_minor_emptyminornonzeroevaluationdeterminanthrc) + (mdr_b_minor_emptyminornonzeroevaluationdeterminanthrc))) /\ ((mdr_e_minor_emptyminornonzeroevaluationdeterminanthrc = ((mdr_p_minor_emptyminornonzeroevaluationdeterminanth) + (mdr_n_minor_emptyminornonzeroevaluationdeterminanth)) * S ((mdr_p_minor_emptyminornonzeroevaluationdeterminanth) + (mdr_n_minor_emptyminornonzeroevaluationdeterminanth)) + ((mdr_n_minor_emptyminornonzeroevaluationdeterminanth) + (mdr_n_minor_emptyminornonzeroevaluationdeterminanth))) /\ ((mdr_f_minor_emptyminornonzeroevaluationdeterminanthrc = ((mdr_nc_minor_emptyminornonzeroevaluationdeterminanth) + (mdr_e_minor_emptyminornonzeroevaluationdeterminanthrc)) * S ((mdr_nc_minor_emptyminornonzeroevaluationdeterminanth) + (mdr_e_minor_emptyminornonzeroevaluationdeterminanthrc)) + ((mdr_e_minor_emptyminornonzeroevaluationdeterminanthrc) + (mdr_e_minor_emptyminornonzeroevaluationdeterminanthrc))) /\ ((mdr_z_minor_emptyminornonzeroevaluationdeterminanthr) = ((mdr_c_minor_emptyminornonzeroevaluationdeterminanthrc) + (mdr_f_minor_emptyminornonzeroevaluationdeterminanthrc)) * S ((mdr_c_minor_emptyminornonzeroevaluationdeterminanthrc) + (mdr_f_minor_emptyminornonzeroevaluationdeterminanthrc)) + ((mdr_f_minor_emptyminornonzeroevaluationdeterminanthrc) + (mdr_f_minor_emptyminornonzeroevaluationdeterminanthrc))))))))) /\ (((exists ff_h_mdr_minor_emptyminornonzeroevaluationdeterminanthrb. ff_h_mdr_minor_emptyminornonzeroevaluationdeterminanthrb + S (mdr_z_minor_emptyminornonzeroevaluationdeterminanthr) = S ((S (mdr_i_minor_emptyminornonzeroevaluationdeterminanth)) * mdr_c_minor_emptyminornonzeroevaluationdeterminant)) /\ exists ff_q_mdr_minor_emptyminornonzeroevaluationdeterminanthrb. mdr_b_minor_emptyminornonzeroevaluationdeterminant = ff_q_mdr_minor_emptyminornonzeroevaluationdeterminanthrb * S ((S (mdr_i_minor_emptyminornonzeroevaluationdeterminanth)) * mdr_c_minor_emptyminornonzeroevaluationdeterminant) + (mdr_z_minor_emptyminornonzeroevaluationdeterminanthr))))) /\ (((((mdr_d_minor_emptyminornonzeroevaluationdeterminanth) = 0) /\ (((mdr_p_minor_emptyminornonzeroevaluationdeterminanth) = 1) /\ ((mdr_n_minor_emptyminornonzeroevaluationdeterminanth) = 0))) \/ exists mdr_q_minor_emptyminornonzeroevaluationdeterminanths mdr_eb_minor_emptyminornonzeroevaluationdeterminanths mdr_ec_minor_emptyminornonzeroevaluationdeterminanths mdr_fb_minor_emptyminornonzeroevaluationdeterminanths mdr_fc_minor_emptyminornonzeroevaluationdeterminanths. (((mdr_d_minor_emptyminornonzeroevaluationdeterminanth) = S (mdr_q_minor_emptyminornonzeroevaluationdeterminanths)) /\ ((forall mdr_j_minor_emptyminornonzeroevaluationdeterminanthsc. (exists mdr_gap_minor_emptyminornonzeroevaluationdeterminanthscj. mdr_gap_minor_emptyminornonzeroevaluationdeterminanthscj + S (mdr_j_minor_emptyminornonzeroevaluationdeterminanthsc) = (S (mdr_q_minor_emptyminornonzeroevaluationdeterminanths))) -> exists mdr_i_minor_emptyminornonzeroevaluationdeterminanthsc mdr_up_minor_emptyminornonzeroevaluationdeterminanthsc mdr_us_minor_emptyminornonzeroevaluationdeterminanthsc mdr_un_minor_emptyminornonzeroevaluationdeterminanthsc mdr_ut_minor_emptyminornonzeroevaluationdeterminanthsc mdr_p_minor_emptyminornonzeroevaluationdeterminanthsc mdr_n_minor_emptyminornonzeroevaluationdeterminanthsc. ((exists mdr_gap_minor_emptyminornonzeroevaluationdeterminanthsci. mdr_gap_minor_emptyminornonzeroevaluationdeterminanthsci + S (mdr_i_minor_emptyminornonzeroevaluationdeterminanthsc) = (mdr_i_minor_emptyminornonzeroevaluationdeterminanth)) /\ ((exists mdr_z_minor_emptyminornonzeroevaluationdeterminanthscr. ((exists mdr_a_minor_emptyminornonzeroevaluationdeterminanthscrc mdr_b_minor_emptyminornonzeroevaluationdeterminanthscrc mdr_c_minor_emptyminornonzeroevaluationdeterminanthscrc mdr_e_minor_emptyminornonzeroevaluationdeterminanthscrc mdr_f_minor_emptyminornonzeroevaluationdeterminanthscrc. ((mdr_a_minor_emptyminornonzeroevaluationdeterminanthscrc = ((mdr_q_minor_emptyminornonzeroevaluationdeterminanths) + (mdr_up_minor_emptyminornonzeroevaluationdeterminanthsc)) * S ((mdr_q_minor_emptyminornonzeroevaluationdeterminanths) + (mdr_up_minor_emptyminornonzeroevaluationdeterminanthsc)) + ((mdr_up_minor_emptyminornonzeroevaluationdeterminanthsc) + (mdr_up_minor_emptyminornonzeroevaluationdeterminanthsc))) /\ ((mdr_b_minor_emptyminornonzeroevaluationdeterminanthscrc = ((mdr_us_minor_emptyminornonzeroevaluationdeterminanthsc) + (mdr_un_minor_emptyminornonzeroevaluationdeterminanthsc)) * S ((mdr_us_minor_emptyminornonzeroevaluationdeterminanthsc) + (mdr_un_minor_emptyminornonzeroevaluationdeterminanthsc)) + ((mdr_un_minor_emptyminornonzeroevaluationdeterminanthsc) + (mdr_un_minor_emptyminornonzeroevaluationdeterminanthsc))) /\ ((mdr_c_minor_emptyminornonzeroevaluationdeterminanthscrc = ((mdr_a_minor_emptyminornonzeroevaluationdeterminanthscrc) + (mdr_b_minor_emptyminornonzeroevaluationdeterminanthscrc)) * S ((mdr_a_minor_emptyminornonzeroevaluationdeterminanthscrc) + (mdr_b_minor_emptyminornonzeroevaluationdeterminanthscrc)) + ((mdr_b_minor_emptyminornonzeroevaluationdeterminanthscrc) + (mdr_b_minor_emptyminornonzeroevaluationdeterminanthscrc))) /\ ((mdr_e_minor_emptyminornonzeroevaluationdeterminanthscrc = ((mdr_p_minor_emptyminornonzeroevaluationdeterminanthsc) + (mdr_n_minor_emptyminornonzeroevaluationdeterminanthsc)) * S ((mdr_p_minor_emptyminornonzeroevaluationdeterminanthsc) + (mdr_n_minor_emptyminornonzeroevaluationdeterminanthsc)) + ((mdr_n_minor_emptyminornonzeroevaluationdeterminanthsc) + (mdr_n_minor_emptyminornonzeroevaluationdeterminanthsc))) /\ ((mdr_f_minor_emptyminornonzeroevaluationdeterminanthscrc = ((mdr_ut_minor_emptyminornonzeroevaluationdeterminanthsc) + (mdr_e_minor_emptyminornonzeroevaluationdeterminanthscrc)) * S ((mdr_ut_minor_emptyminornonzeroevaluationdeterminanthsc) + (mdr_e_minor_emptyminornonzeroevaluationdeterminanthscrc)) + ((mdr_e_minor_emptyminornonzeroevaluationdeterminanthscrc) + (mdr_e_minor_emptyminornonzeroevaluationdeterminanthscrc))) /\ ((mdr_z_minor_emptyminornonzeroevaluationdeterminanthscr) = ((mdr_c_minor_emptyminornonzeroevaluationdeterminanthscrc) + (mdr_f_minor_emptyminornonzeroevaluationdeterminanthscrc)) * S ((mdr_c_minor_emptyminornonzeroevaluationdeterminanthscrc) + (mdr_f_minor_emptyminornonzeroevaluationdeterminanthscrc)) + ((mdr_f_minor_emptyminornonzeroevaluationdeterminanthscrc) + (mdr_f_minor_emptyminornonzeroevaluationdeterminanthscrc))))))))) /\ (((exists ff_h_mdr_minor_emptyminornonzeroevaluationdeterminanthscrb. ff_h_mdr_minor_emptyminornonzeroevaluationdeterminanthscrb + S (mdr_z_minor_emptyminornonzeroevaluationdeterminanthscr) = S ((S (mdr_i_minor_emptyminornonzeroevaluationdeterminanthsc)) * mdr_c_minor_emptyminornonzeroevaluationdeterminant)) /\ exists ff_q_mdr_minor_emptyminornonzeroevaluationdeterminanthscrb. mdr_b_minor_emptyminornonzeroevaluationdeterminant = ff_q_mdr_minor_emptyminornonzeroevaluationdeterminanthscrb * S ((S (mdr_i_minor_emptyminornonzeroevaluationdeterminanthsc)) * mdr_c_minor_emptyminornonzeroevaluationdeterminant) + (mdr_z_minor_emptyminornonzeroevaluationdeterminanthscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_minor_emptyminornonzeroevaluationdeterminanthscm_positive. (exists ff_gap_mdm_lt_mdr_minor_emptyminornonzeroevaluationdeterminanthscm_positive_index_bound. ff_gap_mdm_lt_mdr_minor_emptyminornonzeroevaluationdeterminanthscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_minor_emptyminornonzeroevaluationdeterminanthscm_positive) = ((mdr_q_minor_emptyminornonzeroevaluationdeterminanths) * (mdr_q_minor_emptyminornonzeroevaluationdeterminanths))) -> exists ff_row_mdm_prefix_mdr_minor_emptyminornonzeroevaluationdeterminanthscm_positive ff_column_mdm_prefix_mdr_minor_emptyminornonzeroevaluationdeterminanthscm_positive ff_value_mdm_prefix_mdr_minor_emptyminornonzeroevaluationdeterminanthscm_positive. (ff_index_mdm_prefix_mdr_minor_emptyminornonzeroevaluationdeterminanthscm_positive = (mdr_q_minor_emptyminornonzeroevaluationdeterminanths) * ff_row_mdm_prefix_mdr_minor_emptyminornonzeroevaluationdeterminanthscm_positive + ff_column_mdm_prefix_mdr_minor_emptyminornonzeroevaluationdeterminanthscm_positive /\ ((exists ff_gap_mdm_lt_mdr_minor_emptyminornonzeroevaluationdeterminanthscm_positive_column_bound. ff_gap_mdm_lt_mdr_minor_emptyminornonzeroevaluationdeterminanthscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_minor_emptyminornonzeroevaluationdeterminanthscm_positive) = (mdr_q_minor_emptyminornonzeroevaluationdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_minor_emptyminornonzeroevaluationdeterminanthscm_positive_cell ff_column_mdm_cell_mdr_minor_emptyminornonzeroevaluationdeterminanthscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_minor_emptyminornonzeroevaluationdeterminanthscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_minor_emptyminornonzeroevaluationdeterminanthscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_minor_emptyminornonzeroevaluationdeterminanthscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_minor_emptyminornonzeroevaluationdeterminanthscm_positive_cell = ff_row_mdm_prefix_mdr_minor_emptyminornonzeroevaluationdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_minor_emptyminornonzeroevaluationdeterminanthscm_positive_cell_row_after. ff_gap_mdm_le_mdr_minor_emptyminornonzeroevaluationdeterminanthscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_minor_emptyminornonzeroevaluationdeterminanthscm_positive)) /\ ff_row_mdm_cell_mdr_minor_emptyminornonzeroevaluationdeterminanthscm_positive_cell = S ff_row_mdm_prefix_mdr_minor_emptyminornonzeroevaluationdeterminanthscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_minor_emptyminornonzeroevaluationdeterminanthscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_minor_emptyminornonzeroevaluationdeterminanthscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_minor_emptyminornonzeroevaluationdeterminanthscm_positive) = (mdr_j_minor_emptyminornonzeroevaluationdeterminanthsc)) /\ ff_column_mdm_cell_mdr_minor_emptyminornonzeroevaluationdeterminanthscm_positive_cell = ff_column_mdm_prefix_mdr_minor_emptyminornonzeroevaluationdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_minor_emptyminornonzeroevaluationdeterminanthscm_positive_cell_column_after. ff_gap_mdm_le_mdr_minor_emptyminornonzeroevaluationdeterminanthscm_positive_cell_column_after + (mdr_j_minor_emptyminornonzeroevaluationdeterminanthsc) = (ff_column_mdm_prefix_mdr_minor_emptyminornonzeroevaluationdeterminanthscm_positive)) /\ ff_column_mdm_cell_mdr_minor_emptyminornonzeroevaluationdeterminanthscm_positive_cell = S ff_column_mdm_prefix_mdr_minor_emptyminornonzeroevaluationdeterminanthscm_positive))) /\ (((exists ff_h_mdm_mdr_minor_emptyminornonzeroevaluationdeterminanthscm_positive_cell_source. ff_h_mdm_mdr_minor_emptyminornonzeroevaluationdeterminanthscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_minor_emptyminornonzeroevaluationdeterminanthscm_positive) = S ((S ((ff_row_mdm_cell_mdr_minor_emptyminornonzeroevaluationdeterminanthscm_positive_cell) * (S (mdr_q_minor_emptyminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_minor_emptyminornonzeroevaluationdeterminanthscm_positive_cell))) * mdr_pc_minor_emptyminornonzeroevaluationdeterminanth)) /\ exists ff_q_mdm_mdr_minor_emptyminornonzeroevaluationdeterminanthscm_positive_cell_source. mdr_pb_minor_emptyminornonzeroevaluationdeterminanth = ff_q_mdm_mdr_minor_emptyminornonzeroevaluationdeterminanthscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_minor_emptyminornonzeroevaluationdeterminanthscm_positive_cell) * (S (mdr_q_minor_emptyminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_minor_emptyminornonzeroevaluationdeterminanthscm_positive_cell))) * mdr_pc_minor_emptyminornonzeroevaluationdeterminanth) + (ff_value_mdm_prefix_mdr_minor_emptyminornonzeroevaluationdeterminanthscm_positive)))))) /\ (((exists ff_h_mdm_mdr_minor_emptyminornonzeroevaluationdeterminanthscm_positive_target. ff_h_mdm_mdr_minor_emptyminornonzeroevaluationdeterminanthscm_positive_target + S (ff_value_mdm_prefix_mdr_minor_emptyminornonzeroevaluationdeterminanthscm_positive) = S ((S (ff_index_mdm_prefix_mdr_minor_emptyminornonzeroevaluationdeterminanthscm_positive)) * mdr_us_minor_emptyminornonzeroevaluationdeterminanthsc)) /\ exists ff_q_mdm_mdr_minor_emptyminornonzeroevaluationdeterminanthscm_positive_target. mdr_up_minor_emptyminornonzeroevaluationdeterminanthsc = ff_q_mdm_mdr_minor_emptyminornonzeroevaluationdeterminanthscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_minor_emptyminornonzeroevaluationdeterminanthscm_positive)) * mdr_us_minor_emptyminornonzeroevaluationdeterminanthsc) + (ff_value_mdm_prefix_mdr_minor_emptyminornonzeroevaluationdeterminanthscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_minor_emptyminornonzeroevaluationdeterminanthscm_negative. (exists ff_gap_mdm_lt_mdr_minor_emptyminornonzeroevaluationdeterminanthscm_negative_index_bound. ff_gap_mdm_lt_mdr_minor_emptyminornonzeroevaluationdeterminanthscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_minor_emptyminornonzeroevaluationdeterminanthscm_negative) = ((mdr_q_minor_emptyminornonzeroevaluationdeterminanths) * (mdr_q_minor_emptyminornonzeroevaluationdeterminanths))) -> exists ff_row_mdm_prefix_mdr_minor_emptyminornonzeroevaluationdeterminanthscm_negative ff_column_mdm_prefix_mdr_minor_emptyminornonzeroevaluationdeterminanthscm_negative ff_value_mdm_prefix_mdr_minor_emptyminornonzeroevaluationdeterminanthscm_negative. (ff_index_mdm_prefix_mdr_minor_emptyminornonzeroevaluationdeterminanthscm_negative = (mdr_q_minor_emptyminornonzeroevaluationdeterminanths) * ff_row_mdm_prefix_mdr_minor_emptyminornonzeroevaluationdeterminanthscm_negative + ff_column_mdm_prefix_mdr_minor_emptyminornonzeroevaluationdeterminanthscm_negative /\ ((exists ff_gap_mdm_lt_mdr_minor_emptyminornonzeroevaluationdeterminanthscm_negative_column_bound. ff_gap_mdm_lt_mdr_minor_emptyminornonzeroevaluationdeterminanthscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_minor_emptyminornonzeroevaluationdeterminanthscm_negative) = (mdr_q_minor_emptyminornonzeroevaluationdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_minor_emptyminornonzeroevaluationdeterminanthscm_negative_cell ff_column_mdm_cell_mdr_minor_emptyminornonzeroevaluationdeterminanthscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_minor_emptyminornonzeroevaluationdeterminanthscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_minor_emptyminornonzeroevaluationdeterminanthscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_minor_emptyminornonzeroevaluationdeterminanthscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_minor_emptyminornonzeroevaluationdeterminanthscm_negative_cell = ff_row_mdm_prefix_mdr_minor_emptyminornonzeroevaluationdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_minor_emptyminornonzeroevaluationdeterminanthscm_negative_cell_row_after. ff_gap_mdm_le_mdr_minor_emptyminornonzeroevaluationdeterminanthscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_minor_emptyminornonzeroevaluationdeterminanthscm_negative)) /\ ff_row_mdm_cell_mdr_minor_emptyminornonzeroevaluationdeterminanthscm_negative_cell = S ff_row_mdm_prefix_mdr_minor_emptyminornonzeroevaluationdeterminanthscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_minor_emptyminornonzeroevaluationdeterminanthscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_minor_emptyminornonzeroevaluationdeterminanthscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_minor_emptyminornonzeroevaluationdeterminanthscm_negative) = (mdr_j_minor_emptyminornonzeroevaluationdeterminanthsc)) /\ ff_column_mdm_cell_mdr_minor_emptyminornonzeroevaluationdeterminanthscm_negative_cell = ff_column_mdm_prefix_mdr_minor_emptyminornonzeroevaluationdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_minor_emptyminornonzeroevaluationdeterminanthscm_negative_cell_column_after. ff_gap_mdm_le_mdr_minor_emptyminornonzeroevaluationdeterminanthscm_negative_cell_column_after + (mdr_j_minor_emptyminornonzeroevaluationdeterminanthsc) = (ff_column_mdm_prefix_mdr_minor_emptyminornonzeroevaluationdeterminanthscm_negative)) /\ ff_column_mdm_cell_mdr_minor_emptyminornonzeroevaluationdeterminanthscm_negative_cell = S ff_column_mdm_prefix_mdr_minor_emptyminornonzeroevaluationdeterminanthscm_negative))) /\ (((exists ff_h_mdm_mdr_minor_emptyminornonzeroevaluationdeterminanthscm_negative_cell_source. ff_h_mdm_mdr_minor_emptyminornonzeroevaluationdeterminanthscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_minor_emptyminornonzeroevaluationdeterminanthscm_negative) = S ((S ((ff_row_mdm_cell_mdr_minor_emptyminornonzeroevaluationdeterminanthscm_negative_cell) * (S (mdr_q_minor_emptyminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_minor_emptyminornonzeroevaluationdeterminanthscm_negative_cell))) * mdr_nc_minor_emptyminornonzeroevaluationdeterminanth)) /\ exists ff_q_mdm_mdr_minor_emptyminornonzeroevaluationdeterminanthscm_negative_cell_source. mdr_nb_minor_emptyminornonzeroevaluationdeterminanth = ff_q_mdm_mdr_minor_emptyminornonzeroevaluationdeterminanthscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_minor_emptyminornonzeroevaluationdeterminanthscm_negative_cell) * (S (mdr_q_minor_emptyminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_minor_emptyminornonzeroevaluationdeterminanthscm_negative_cell))) * mdr_nc_minor_emptyminornonzeroevaluationdeterminanth) + (ff_value_mdm_prefix_mdr_minor_emptyminornonzeroevaluationdeterminanthscm_negative)))))) /\ (((exists ff_h_mdm_mdr_minor_emptyminornonzeroevaluationdeterminanthscm_negative_target. ff_h_mdm_mdr_minor_emptyminornonzeroevaluationdeterminanthscm_negative_target + S (ff_value_mdm_prefix_mdr_minor_emptyminornonzeroevaluationdeterminanthscm_negative) = S ((S (ff_index_mdm_prefix_mdr_minor_emptyminornonzeroevaluationdeterminanthscm_negative)) * mdr_ut_minor_emptyminornonzeroevaluationdeterminanthsc)) /\ exists ff_q_mdm_mdr_minor_emptyminornonzeroevaluationdeterminanthscm_negative_target. mdr_un_minor_emptyminornonzeroevaluationdeterminanthsc = ff_q_mdm_mdr_minor_emptyminornonzeroevaluationdeterminanthscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_minor_emptyminornonzeroevaluationdeterminanthscm_negative)) * mdr_ut_minor_emptyminornonzeroevaluationdeterminanthsc) + (ff_value_mdm_prefix_mdr_minor_emptyminornonzeroevaluationdeterminanthscm_negative))))))))) /\ ((((exists ff_h_mdr_minor_emptyminornonzeroevaluationdeterminanthscp. ff_h_mdr_minor_emptyminornonzeroevaluationdeterminanthscp + S (mdr_p_minor_emptyminornonzeroevaluationdeterminanthsc) = S ((S (mdr_j_minor_emptyminornonzeroevaluationdeterminanthsc)) * mdr_ec_minor_emptyminornonzeroevaluationdeterminanths)) /\ exists ff_q_mdr_minor_emptyminornonzeroevaluationdeterminanthscp. mdr_eb_minor_emptyminornonzeroevaluationdeterminanths = ff_q_mdr_minor_emptyminornonzeroevaluationdeterminanthscp * S ((S (mdr_j_minor_emptyminornonzeroevaluationdeterminanthsc)) * mdr_ec_minor_emptyminornonzeroevaluationdeterminanths) + (mdr_p_minor_emptyminornonzeroevaluationdeterminanthsc))) /\ (((exists ff_h_mdr_minor_emptyminornonzeroevaluationdeterminanthscn. ff_h_mdr_minor_emptyminornonzeroevaluationdeterminanthscn + S (mdr_n_minor_emptyminornonzeroevaluationdeterminanthsc) = S ((S (mdr_j_minor_emptyminornonzeroevaluationdeterminanthsc)) * mdr_fc_minor_emptyminornonzeroevaluationdeterminanths)) /\ exists ff_q_mdr_minor_emptyminornonzeroevaluationdeterminanthscn. mdr_fb_minor_emptyminornonzeroevaluationdeterminanths = ff_q_mdr_minor_emptyminornonzeroevaluationdeterminanthscn * S ((S (mdr_j_minor_emptyminornonzeroevaluationdeterminanthsc)) * mdr_fc_minor_emptyminornonzeroevaluationdeterminanths) + (mdr_n_minor_emptyminornonzeroevaluationdeterminanthsc)))))))) /\ (exists ff_ub_mce_fold_mdr_minor_emptyminornonzeroevaluationdeterminanthsf ff_uc_mce_fold_mdr_minor_emptyminornonzeroevaluationdeterminanthsf ff_vb_mce_fold_mdr_minor_emptyminornonzeroevaluationdeterminanthsf ff_vc_mce_fold_mdr_minor_emptyminornonzeroevaluationdeterminanthsf. ((forall ff_index_mce_alternating_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_prefix. (exists ff_gap_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_prefix_index. ff_gap_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_prefix_index + S (ff_index_mce_alternating_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_prefix) = (S (mdr_q_minor_emptyminornonzeroevaluationdeterminanths))) -> exists ff_ap_mce_alternating_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_prefix ff_an_mce_alternating_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_prefix ff_bp_mce_alternating_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_prefix ff_bn_mce_alternating_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_prefix ff_p_mce_alternating_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_prefix ff_n_mce_alternating_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_prefix. ((((exists ff_h_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_prefix_ap. ff_h_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_prefix_ap + S (ff_ap_mce_alternating_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_prefix)) * mdr_pc_minor_emptyminornonzeroevaluationdeterminanth)) /\ exists ff_q_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_prefix_ap. mdr_pb_minor_emptyminornonzeroevaluationdeterminanth = ff_q_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_prefix)) * mdr_pc_minor_emptyminornonzeroevaluationdeterminanth) + (ff_ap_mce_alternating_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_prefix_an. ff_h_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_prefix_an + S (ff_an_mce_alternating_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_prefix)) * mdr_nc_minor_emptyminornonzeroevaluationdeterminanth)) /\ exists ff_q_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_prefix_an. mdr_nb_minor_emptyminornonzeroevaluationdeterminanth = ff_q_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_prefix)) * mdr_nc_minor_emptyminornonzeroevaluationdeterminanth) + (ff_an_mce_alternating_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_prefix_bp. ff_h_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_prefix_bp + S (ff_bp_mce_alternating_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_prefix)) * mdr_ec_minor_emptyminornonzeroevaluationdeterminanths)) /\ exists ff_q_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_prefix_bp. mdr_eb_minor_emptyminornonzeroevaluationdeterminanths = ff_q_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_prefix)) * mdr_ec_minor_emptyminornonzeroevaluationdeterminanths) + (ff_bp_mce_alternating_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_prefix_bn. ff_h_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_prefix_bn + S (ff_bn_mce_alternating_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_prefix)) * mdr_fc_minor_emptyminornonzeroevaluationdeterminanths)) /\ exists ff_q_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_prefix_bn. mdr_fb_minor_emptyminornonzeroevaluationdeterminanths = ff_q_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_prefix)) * mdr_fc_minor_emptyminornonzeroevaluationdeterminanths) + (ff_bn_mce_alternating_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_prefix_positive. ff_h_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_prefix_positive + S (ff_p_mce_alternating_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_minor_emptyminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_prefix_positive. ff_ub_mce_fold_mdr_minor_emptyminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_minor_emptyminornonzeroevaluationdeterminanthsf) + (ff_p_mce_alternating_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_prefix_negative. ff_h_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_prefix_negative + S (ff_n_mce_alternating_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_minor_emptyminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_prefix_negative. ff_vb_mce_fold_mdr_minor_emptyminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_minor_emptyminornonzeroevaluationdeterminanthsf) + (ff_n_mce_alternating_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_prefix))) /\ (((exists ff_even_mce_term_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_prefix = 2 * ff_even_mce_term_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_prefix_term) /\ (ff_p_mce_alternating_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_prefix = 2 * ff_odd_mce_term_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_positive ff_v_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_positive. ((((exists ff_h_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_positive_start. ff_h_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_positive_start. ff_u_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_positive_start * S ((S (0)) * ff_v_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_positive_terminal. ff_h_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_positive_terminal + S (mdr_p_minor_emptyminornonzeroevaluationdeterminanth) = S ((S ((S (mdr_q_minor_emptyminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_positive_terminal. ff_u_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_positive_terminal * S ((S ((S (mdr_q_minor_emptyminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_positive) + (mdr_p_minor_emptyminornonzeroevaluationdeterminanth))) /\ forall ff_i_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_positive. (exists ff_lt_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_positive_bound. ff_lt_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_positive_bound + S ff_i_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_positive = (S (mdr_q_minor_emptyminornonzeroevaluationdeterminanths))) -> exists ff_a_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_positive ff_r_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_positive ff_s_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_positive. ((((exists ff_h_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_positive_summand. ff_h_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_positive_summand + S (ff_a_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_minor_emptyminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_positive_summand. ff_ub_mce_fold_mdr_minor_emptyminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_positive_summand * S ((S (ff_i_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_minor_emptyminornonzeroevaluationdeterminanthsf) + (ff_a_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_positive_partial. ff_h_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_positive_partial + S (ff_r_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_positive_partial. ff_u_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_positive_partial * S ((S (ff_i_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_positive) + (ff_r_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_positive_successor. ff_h_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_positive_successor + S (ff_s_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_positive) = S ((S (S ff_i_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_positive_successor. ff_u_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_positive_successor * S ((S (S ff_i_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_positive) + (ff_s_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_positive))) /\ ff_s_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_positive = ff_r_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_positive + ff_a_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_positive)))))) /\ (exists ff_u_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_negative ff_v_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_negative. ((((exists ff_h_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_negative_start. ff_h_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_negative_start. ff_u_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_negative_start * S ((S (0)) * ff_v_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_negative_terminal. ff_h_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_negative_terminal + S (mdr_n_minor_emptyminornonzeroevaluationdeterminanth) = S ((S ((S (mdr_q_minor_emptyminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_negative_terminal. ff_u_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_negative_terminal * S ((S ((S (mdr_q_minor_emptyminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_negative) + (mdr_n_minor_emptyminornonzeroevaluationdeterminanth))) /\ forall ff_i_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_negative. (exists ff_lt_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_negative_bound. ff_lt_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_negative_bound + S ff_i_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_negative = (S (mdr_q_minor_emptyminornonzeroevaluationdeterminanths))) -> exists ff_a_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_negative ff_r_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_negative ff_s_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_negative. ((((exists ff_h_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_negative_summand. ff_h_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_negative_summand + S (ff_a_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_minor_emptyminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_negative_summand. ff_vb_mce_fold_mdr_minor_emptyminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_negative_summand * S ((S (ff_i_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_minor_emptyminornonzeroevaluationdeterminanthsf) + (ff_a_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_negative_partial. ff_h_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_negative_partial + S (ff_r_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_negative_partial. ff_u_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_negative_partial * S ((S (ff_i_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_negative) + (ff_r_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_negative_successor. ff_h_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_negative_successor + S (ff_s_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_negative) = S ((S (S ff_i_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_negative_successor. ff_u_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_negative_successor * S ((S (S ff_i_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_negative) + (ff_s_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_negative))) /\ ff_s_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_negative = ff_r_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_negative + ff_a_mce_mdr_minor_emptyminornonzeroevaluationdeterminanthsf_negative))))))))))))))) /\ ((exists mdr_gap_minor_emptyminornonzeroevaluationdeterminanti. mdr_gap_minor_emptyminornonzeroevaluationdeterminanti + S (mdr_i_minor_emptyminornonzeroevaluationdeterminant) = (mdr_l_minor_emptyminornonzeroevaluationdeterminant)) /\ (exists mdr_z_minor_emptyminornonzeroevaluationdeterminantr. ((exists mdr_a_minor_emptyminornonzeroevaluationdeterminantrc mdr_b_minor_emptyminornonzeroevaluationdeterminantrc mdr_c_minor_emptyminornonzeroevaluationdeterminantrc mdr_e_minor_emptyminornonzeroevaluationdeterminantrc mdr_f_minor_emptyminornonzeroevaluationdeterminantrc. ((mdr_a_minor_emptyminornonzeroevaluationdeterminantrc = ((0) + (mdr_ub_minor_emptyminornonzeroevaluation)) * S ((0) + (mdr_ub_minor_emptyminornonzeroevaluation)) + ((mdr_ub_minor_emptyminornonzeroevaluation) + (mdr_ub_minor_emptyminornonzeroevaluation))) /\ ((mdr_b_minor_emptyminornonzeroevaluationdeterminantrc = ((mdr_uc_minor_emptyminornonzeroevaluation) + (mdr_vb_minor_emptyminornonzeroevaluation)) * S ((mdr_uc_minor_emptyminornonzeroevaluation) + (mdr_vb_minor_emptyminornonzeroevaluation)) + ((mdr_vb_minor_emptyminornonzeroevaluation) + (mdr_vb_minor_emptyminornonzeroevaluation))) /\ ((mdr_c_minor_emptyminornonzeroevaluationdeterminantrc = ((mdr_a_minor_emptyminornonzeroevaluationdeterminantrc) + (mdr_b_minor_emptyminornonzeroevaluationdeterminantrc)) * S ((mdr_a_minor_emptyminornonzeroevaluationdeterminantrc) + (mdr_b_minor_emptyminornonzeroevaluationdeterminantrc)) + ((mdr_b_minor_emptyminornonzeroevaluationdeterminantrc) + (mdr_b_minor_emptyminornonzeroevaluationdeterminantrc))) /\ ((mdr_e_minor_emptyminornonzeroevaluationdeterminantrc = ((mdr_p_minor_emptyminornonzero) + (mdr_n_minor_emptyminornonzero)) * S ((mdr_p_minor_emptyminornonzero) + (mdr_n_minor_emptyminornonzero)) + ((mdr_n_minor_emptyminornonzero) + (mdr_n_minor_emptyminornonzero))) /\ ((mdr_f_minor_emptyminornonzeroevaluationdeterminantrc = ((mdr_vc_minor_emptyminornonzeroevaluation) + (mdr_e_minor_emptyminornonzeroevaluationdeterminantrc)) * S ((mdr_vc_minor_emptyminornonzeroevaluation) + (mdr_e_minor_emptyminornonzeroevaluationdeterminantrc)) + ((mdr_e_minor_emptyminornonzeroevaluationdeterminantrc) + (mdr_e_minor_emptyminornonzeroevaluationdeterminantrc))) /\ ((mdr_z_minor_emptyminornonzeroevaluationdeterminantr) = ((mdr_c_minor_emptyminornonzeroevaluationdeterminantrc) + (mdr_f_minor_emptyminornonzeroevaluationdeterminantrc)) * S ((mdr_c_minor_emptyminornonzeroevaluationdeterminantrc) + (mdr_f_minor_emptyminornonzeroevaluationdeterminantrc)) + ((mdr_f_minor_emptyminornonzeroevaluationdeterminantrc) + (mdr_f_minor_emptyminornonzeroevaluationdeterminantrc))))))))) /\ (((exists ff_h_mdr_minor_emptyminornonzeroevaluationdeterminantrb. ff_h_mdr_minor_emptyminornonzeroevaluationdeterminantrb + S (mdr_z_minor_emptyminornonzeroevaluationdeterminantr) = S ((S (mdr_i_minor_emptyminornonzeroevaluationdeterminant)) * mdr_c_minor_emptyminornonzeroevaluationdeterminant)) /\ exists ff_q_mdr_minor_emptyminornonzeroevaluationdeterminantrb. mdr_b_minor_emptyminornonzeroevaluationdeterminant = ff_q_mdr_minor_emptyminornonzeroevaluationdeterminantrb * S ((S (mdr_i_minor_emptyminornonzeroevaluationdeterminant)) * mdr_c_minor_emptyminornonzeroevaluationdeterminant) + (mdr_z_minor_emptyminornonzeroevaluationdeterminantr)))))))))) /\ (~(mdr_p_minor_emptyminornonzero = mdr_n_minor_emptyminornonzero))))))))