matrix_rank_nonzero_selected_minor_decidable

Exact expanded first-order arithmetic statement

forall pb pc nb nc r w q rb rc cb cc. (((((forall fom_index_mrf_minor_yesrowsbound. (exists fom_gap_mrf_minor_yesrowsbound_index_bound. fom_gap_mrf_minor_yesrowsbound_index_bound + S (fom_index_mrf_minor_yesrowsbound) = q) -> exists fom_value_mrf_minor_yesrowsbound. ((((exists fom_beta_height_mrf_minor_yesrowsbound_entry. fom_beta_height_mrf_minor_yesrowsbound_entry + S (fom_value_mrf_minor_yesrowsbound) = S ((S (fom_index_mrf_minor_yesrowsbound)) * rc)) /\ exists fom_beta_quotient_mrf_minor_yesrowsbound_entry. rb = fom_beta_quotient_mrf_minor_yesrowsbound_entry * S ((S (fom_index_mrf_minor_yesrowsbound)) * rc) + (fom_value_mrf_minor_yesrowsbound))) /\ (exists fom_gap_mrf_minor_yesrowsbound_value_bound. fom_gap_mrf_minor_yesrowsbound_value_bound + S (fom_value_mrf_minor_yesrowsbound) = r))) /\ (forall mdr_i_minor_yesrowsdistinct mdr_j_minor_yesrowsdistinct mdr_a_minor_yesrowsdistinct. (exists mdr_gap_minor_yesrowsdistincti. mdr_gap_minor_yesrowsdistincti + S (mdr_i_minor_yesrowsdistinct) = (q)) -> (exists mdr_gap_minor_yesrowsdistinctj. mdr_gap_minor_yesrowsdistinctj + S (mdr_j_minor_yesrowsdistinct) = (q)) -> (((exists ff_h_mdr_minor_yesrowsdistinctfirst. ff_h_mdr_minor_yesrowsdistinctfirst + S (mdr_a_minor_yesrowsdistinct) = S ((S (mdr_i_minor_yesrowsdistinct)) * rc)) /\ exists ff_q_mdr_minor_yesrowsdistinctfirst. rb = ff_q_mdr_minor_yesrowsdistinctfirst * S ((S (mdr_i_minor_yesrowsdistinct)) * rc) + (mdr_a_minor_yesrowsdistinct))) -> (((exists ff_h_mdr_minor_yesrowsdistinctsecond. ff_h_mdr_minor_yesrowsdistinctsecond + S (mdr_a_minor_yesrowsdistinct) = S ((S (mdr_j_minor_yesrowsdistinct)) * rc)) /\ exists ff_q_mdr_minor_yesrowsdistinctsecond. rb = ff_q_mdr_minor_yesrowsdistinctsecond * S ((S (mdr_j_minor_yesrowsdistinct)) * rc) + (mdr_a_minor_yesrowsdistinct))) -> mdr_i_minor_yesrowsdistinct = mdr_j_minor_yesrowsdistinct))) /\ ((((forall fom_index_mrf_minor_yescolumnsbound. (exists fom_gap_mrf_minor_yescolumnsbound_index_bound. fom_gap_mrf_minor_yescolumnsbound_index_bound + S (fom_index_mrf_minor_yescolumnsbound) = q) -> exists fom_value_mrf_minor_yescolumnsbound. ((((exists fom_beta_height_mrf_minor_yescolumnsbound_entry. fom_beta_height_mrf_minor_yescolumnsbound_entry + S (fom_value_mrf_minor_yescolumnsbound) = S ((S (fom_index_mrf_minor_yescolumnsbound)) * cc)) /\ exists fom_beta_quotient_mrf_minor_yescolumnsbound_entry. cb = fom_beta_quotient_mrf_minor_yescolumnsbound_entry * S ((S (fom_index_mrf_minor_yescolumnsbound)) * cc) + (fom_value_mrf_minor_yescolumnsbound))) /\ (exists fom_gap_mrf_minor_yescolumnsbound_value_bound. fom_gap_mrf_minor_yescolumnsbound_value_bound + S (fom_value_mrf_minor_yescolumnsbound) = w))) /\ (forall mdr_i_minor_yescolumnsdistinct mdr_j_minor_yescolumnsdistinct mdr_a_minor_yescolumnsdistinct. (exists mdr_gap_minor_yescolumnsdistincti. mdr_gap_minor_yescolumnsdistincti + S (mdr_i_minor_yescolumnsdistinct) = (q)) -> (exists mdr_gap_minor_yescolumnsdistinctj. mdr_gap_minor_yescolumnsdistinctj + S (mdr_j_minor_yescolumnsdistinct) = (q)) -> (((exists ff_h_mdr_minor_yescolumnsdistinctfirst. ff_h_mdr_minor_yescolumnsdistinctfirst + S (mdr_a_minor_yescolumnsdistinct) = S ((S (mdr_i_minor_yescolumnsdistinct)) * cc)) /\ exists ff_q_mdr_minor_yescolumnsdistinctfirst. cb = ff_q_mdr_minor_yescolumnsdistinctfirst * S ((S (mdr_i_minor_yescolumnsdistinct)) * cc) + (mdr_a_minor_yescolumnsdistinct))) -> (((exists ff_h_mdr_minor_yescolumnsdistinctsecond. ff_h_mdr_minor_yescolumnsdistinctsecond + S (mdr_a_minor_yescolumnsdistinct) = S ((S (mdr_j_minor_yescolumnsdistinct)) * cc)) /\ exists ff_q_mdr_minor_yescolumnsdistinctsecond. cb = ff_q_mdr_minor_yescolumnsdistinctsecond * S ((S (mdr_j_minor_yescolumnsdistinct)) * cc) + (mdr_a_minor_yescolumnsdistinct))) -> mdr_i_minor_yescolumnsdistinct = mdr_j_minor_yescolumnsdistinct))) /\ (exists mdr_p_minor_yesnonzero mdr_n_minor_yesnonzero. ((exists mdr_ub_minor_yesnonzeroevaluation mdr_uc_minor_yesnonzeroevaluation mdr_vb_minor_yesnonzeroevaluation mdr_vc_minor_yesnonzeroevaluation. ((((forall mdr_i_minor_yesnonzeroevaluationmatrixpositive. (exists mdr_gap_minor_yesnonzeroevaluationmatrixpositivebound. mdr_gap_minor_yesnonzeroevaluationmatrixpositivebound + S (mdr_i_minor_yesnonzeroevaluationmatrixpositive) = ((q) * (q))) -> exists mdr_a_minor_yesnonzeroevaluationmatrixpositive. (((exists mdr_r_minor_yesnonzeroevaluationmatrixpositivepoint mdr_s_minor_yesnonzeroevaluationmatrixpositivepoint mdr_u_minor_yesnonzeroevaluationmatrixpositivepoint mdr_v_minor_yesnonzeroevaluationmatrixpositivepoint. ((mdr_i_minor_yesnonzeroevaluationmatrixpositive = (q) * mdr_r_minor_yesnonzeroevaluationmatrixpositivepoint + mdr_s_minor_yesnonzeroevaluationmatrixpositivepoint) /\ ((exists mdr_gap_minor_yesnonzeroevaluationmatrixpositivepointcolumn. mdr_gap_minor_yesnonzeroevaluationmatrixpositivepointcolumn + S (mdr_s_minor_yesnonzeroevaluationmatrixpositivepoint) = (q)) /\ ((((exists ff_h_mdr_minor_yesnonzeroevaluationmatrixpositivepointrow_index. ff_h_mdr_minor_yesnonzeroevaluationmatrixpositivepointrow_index + S (mdr_u_minor_yesnonzeroevaluationmatrixpositivepoint) = S ((S (mdr_r_minor_yesnonzeroevaluationmatrixpositivepoint)) * rc)) /\ exists ff_q_mdr_minor_yesnonzeroevaluationmatrixpositivepointrow_index. rb = ff_q_mdr_minor_yesnonzeroevaluationmatrixpositivepointrow_index * S ((S (mdr_r_minor_yesnonzeroevaluationmatrixpositivepoint)) * rc) + (mdr_u_minor_yesnonzeroevaluationmatrixpositivepoint))) /\ ((((exists ff_h_mdr_minor_yesnonzeroevaluationmatrixpositivepointcolumn_index. ff_h_mdr_minor_yesnonzeroevaluationmatrixpositivepointcolumn_index + S (mdr_v_minor_yesnonzeroevaluationmatrixpositivepoint) = S ((S (mdr_s_minor_yesnonzeroevaluationmatrixpositivepoint)) * cc)) /\ exists ff_q_mdr_minor_yesnonzeroevaluationmatrixpositivepointcolumn_index. cb = ff_q_mdr_minor_yesnonzeroevaluationmatrixpositivepointcolumn_index * S ((S (mdr_s_minor_yesnonzeroevaluationmatrixpositivepoint)) * cc) + (mdr_v_minor_yesnonzeroevaluationmatrixpositivepoint))) /\ (((exists ff_h_mdr_minor_yesnonzeroevaluationmatrixpositivepointsource. ff_h_mdr_minor_yesnonzeroevaluationmatrixpositivepointsource + S (mdr_a_minor_yesnonzeroevaluationmatrixpositive) = S ((S ((mdr_u_minor_yesnonzeroevaluationmatrixpositivepoint) * (w) + (mdr_v_minor_yesnonzeroevaluationmatrixpositivepoint))) * pc)) /\ exists ff_q_mdr_minor_yesnonzeroevaluationmatrixpositivepointsource. pb = ff_q_mdr_minor_yesnonzeroevaluationmatrixpositivepointsource * S ((S ((mdr_u_minor_yesnonzeroevaluationmatrixpositivepoint) * (w) + (mdr_v_minor_yesnonzeroevaluationmatrixpositivepoint))) * pc) + (mdr_a_minor_yesnonzeroevaluationmatrixpositive)))))))) /\ (((exists ff_h_mdr_minor_yesnonzeroevaluationmatrixpositiveoutput. ff_h_mdr_minor_yesnonzeroevaluationmatrixpositiveoutput + S (mdr_a_minor_yesnonzeroevaluationmatrixpositive) = S ((S (mdr_i_minor_yesnonzeroevaluationmatrixpositive)) * mdr_uc_minor_yesnonzeroevaluation)) /\ exists ff_q_mdr_minor_yesnonzeroevaluationmatrixpositiveoutput. mdr_ub_minor_yesnonzeroevaluation = ff_q_mdr_minor_yesnonzeroevaluationmatrixpositiveoutput * S ((S (mdr_i_minor_yesnonzeroevaluationmatrixpositive)) * mdr_uc_minor_yesnonzeroevaluation) + (mdr_a_minor_yesnonzeroevaluationmatrixpositive)))))) /\ (forall mdr_i_minor_yesnonzeroevaluationmatrixnegative. (exists mdr_gap_minor_yesnonzeroevaluationmatrixnegativebound. mdr_gap_minor_yesnonzeroevaluationmatrixnegativebound + S (mdr_i_minor_yesnonzeroevaluationmatrixnegative) = ((q) * (q))) -> exists mdr_a_minor_yesnonzeroevaluationmatrixnegative. (((exists mdr_r_minor_yesnonzeroevaluationmatrixnegativepoint mdr_s_minor_yesnonzeroevaluationmatrixnegativepoint mdr_u_minor_yesnonzeroevaluationmatrixnegativepoint mdr_v_minor_yesnonzeroevaluationmatrixnegativepoint. ((mdr_i_minor_yesnonzeroevaluationmatrixnegative = (q) * mdr_r_minor_yesnonzeroevaluationmatrixnegativepoint + mdr_s_minor_yesnonzeroevaluationmatrixnegativepoint) /\ ((exists mdr_gap_minor_yesnonzeroevaluationmatrixnegativepointcolumn. mdr_gap_minor_yesnonzeroevaluationmatrixnegativepointcolumn + S (mdr_s_minor_yesnonzeroevaluationmatrixnegativepoint) = (q)) /\ ((((exists ff_h_mdr_minor_yesnonzeroevaluationmatrixnegativepointrow_index. ff_h_mdr_minor_yesnonzeroevaluationmatrixnegativepointrow_index + S (mdr_u_minor_yesnonzeroevaluationmatrixnegativepoint) = S ((S (mdr_r_minor_yesnonzeroevaluationmatrixnegativepoint)) * rc)) /\ exists ff_q_mdr_minor_yesnonzeroevaluationmatrixnegativepointrow_index. rb = ff_q_mdr_minor_yesnonzeroevaluationmatrixnegativepointrow_index * S ((S (mdr_r_minor_yesnonzeroevaluationmatrixnegativepoint)) * rc) + (mdr_u_minor_yesnonzeroevaluationmatrixnegativepoint))) /\ ((((exists ff_h_mdr_minor_yesnonzeroevaluationmatrixnegativepointcolumn_index. ff_h_mdr_minor_yesnonzeroevaluationmatrixnegativepointcolumn_index + S (mdr_v_minor_yesnonzeroevaluationmatrixnegativepoint) = S ((S (mdr_s_minor_yesnonzeroevaluationmatrixnegativepoint)) * cc)) /\ exists ff_q_mdr_minor_yesnonzeroevaluationmatrixnegativepointcolumn_index. cb = ff_q_mdr_minor_yesnonzeroevaluationmatrixnegativepointcolumn_index * S ((S (mdr_s_minor_yesnonzeroevaluationmatrixnegativepoint)) * cc) + (mdr_v_minor_yesnonzeroevaluationmatrixnegativepoint))) /\ (((exists ff_h_mdr_minor_yesnonzeroevaluationmatrixnegativepointsource. ff_h_mdr_minor_yesnonzeroevaluationmatrixnegativepointsource + S (mdr_a_minor_yesnonzeroevaluationmatrixnegative) = S ((S ((mdr_u_minor_yesnonzeroevaluationmatrixnegativepoint) * (w) + (mdr_v_minor_yesnonzeroevaluationmatrixnegativepoint))) * nc)) /\ exists ff_q_mdr_minor_yesnonzeroevaluationmatrixnegativepointsource. nb = ff_q_mdr_minor_yesnonzeroevaluationmatrixnegativepointsource * S ((S ((mdr_u_minor_yesnonzeroevaluationmatrixnegativepoint) * (w) + (mdr_v_minor_yesnonzeroevaluationmatrixnegativepoint))) * nc) + (mdr_a_minor_yesnonzeroevaluationmatrixnegative)))))))) /\ (((exists ff_h_mdr_minor_yesnonzeroevaluationmatrixnegativeoutput. ff_h_mdr_minor_yesnonzeroevaluationmatrixnegativeoutput + S (mdr_a_minor_yesnonzeroevaluationmatrixnegative) = S ((S (mdr_i_minor_yesnonzeroevaluationmatrixnegative)) * mdr_vc_minor_yesnonzeroevaluation)) /\ exists ff_q_mdr_minor_yesnonzeroevaluationmatrixnegativeoutput. mdr_vb_minor_yesnonzeroevaluation = ff_q_mdr_minor_yesnonzeroevaluationmatrixnegativeoutput * S ((S (mdr_i_minor_yesnonzeroevaluationmatrixnegative)) * mdr_vc_minor_yesnonzeroevaluation) + (mdr_a_minor_yesnonzeroevaluationmatrixnegative)))))))) /\ (exists mdr_b_minor_yesnonzeroevaluationdeterminant mdr_c_minor_yesnonzeroevaluationdeterminant mdr_l_minor_yesnonzeroevaluationdeterminant mdr_i_minor_yesnonzeroevaluationdeterminant. ((forall mdr_i_minor_yesnonzeroevaluationdeterminanth. (exists mdr_gap_minor_yesnonzeroevaluationdeterminanthi. mdr_gap_minor_yesnonzeroevaluationdeterminanthi + S (mdr_i_minor_yesnonzeroevaluationdeterminanth) = (mdr_l_minor_yesnonzeroevaluationdeterminant)) -> exists mdr_d_minor_yesnonzeroevaluationdeterminanth mdr_pb_minor_yesnonzeroevaluationdeterminanth mdr_pc_minor_yesnonzeroevaluationdeterminanth mdr_nb_minor_yesnonzeroevaluationdeterminanth mdr_nc_minor_yesnonzeroevaluationdeterminanth mdr_p_minor_yesnonzeroevaluationdeterminanth mdr_n_minor_yesnonzeroevaluationdeterminanth. ((exists mdr_z_minor_yesnonzeroevaluationdeterminanthr. ((exists mdr_a_minor_yesnonzeroevaluationdeterminanthrc mdr_b_minor_yesnonzeroevaluationdeterminanthrc mdr_c_minor_yesnonzeroevaluationdeterminanthrc mdr_e_minor_yesnonzeroevaluationdeterminanthrc mdr_f_minor_yesnonzeroevaluationdeterminanthrc. ((mdr_a_minor_yesnonzeroevaluationdeterminanthrc = ((mdr_d_minor_yesnonzeroevaluationdeterminanth) + (mdr_pb_minor_yesnonzeroevaluationdeterminanth)) * S ((mdr_d_minor_yesnonzeroevaluationdeterminanth) + (mdr_pb_minor_yesnonzeroevaluationdeterminanth)) + ((mdr_pb_minor_yesnonzeroevaluationdeterminanth) + (mdr_pb_minor_yesnonzeroevaluationdeterminanth))) /\ ((mdr_b_minor_yesnonzeroevaluationdeterminanthrc = ((mdr_pc_minor_yesnonzeroevaluationdeterminanth) + (mdr_nb_minor_yesnonzeroevaluationdeterminanth)) * S ((mdr_pc_minor_yesnonzeroevaluationdeterminanth) + (mdr_nb_minor_yesnonzeroevaluationdeterminanth)) + ((mdr_nb_minor_yesnonzeroevaluationdeterminanth) + (mdr_nb_minor_yesnonzeroevaluationdeterminanth))) /\ ((mdr_c_minor_yesnonzeroevaluationdeterminanthrc = ((mdr_a_minor_yesnonzeroevaluationdeterminanthrc) + (mdr_b_minor_yesnonzeroevaluationdeterminanthrc)) * S ((mdr_a_minor_yesnonzeroevaluationdeterminanthrc) + (mdr_b_minor_yesnonzeroevaluationdeterminanthrc)) + ((mdr_b_minor_yesnonzeroevaluationdeterminanthrc) + (mdr_b_minor_yesnonzeroevaluationdeterminanthrc))) /\ ((mdr_e_minor_yesnonzeroevaluationdeterminanthrc = ((mdr_p_minor_yesnonzeroevaluationdeterminanth) + (mdr_n_minor_yesnonzeroevaluationdeterminanth)) * S ((mdr_p_minor_yesnonzeroevaluationdeterminanth) + (mdr_n_minor_yesnonzeroevaluationdeterminanth)) + ((mdr_n_minor_yesnonzeroevaluationdeterminanth) + (mdr_n_minor_yesnonzeroevaluationdeterminanth))) /\ ((mdr_f_minor_yesnonzeroevaluationdeterminanthrc = ((mdr_nc_minor_yesnonzeroevaluationdeterminanth) + (mdr_e_minor_yesnonzeroevaluationdeterminanthrc)) * S ((mdr_nc_minor_yesnonzeroevaluationdeterminanth) + (mdr_e_minor_yesnonzeroevaluationdeterminanthrc)) + ((mdr_e_minor_yesnonzeroevaluationdeterminanthrc) + (mdr_e_minor_yesnonzeroevaluationdeterminanthrc))) /\ ((mdr_z_minor_yesnonzeroevaluationdeterminanthr) = ((mdr_c_minor_yesnonzeroevaluationdeterminanthrc) + (mdr_f_minor_yesnonzeroevaluationdeterminanthrc)) * S ((mdr_c_minor_yesnonzeroevaluationdeterminanthrc) + (mdr_f_minor_yesnonzeroevaluationdeterminanthrc)) + ((mdr_f_minor_yesnonzeroevaluationdeterminanthrc) + (mdr_f_minor_yesnonzeroevaluationdeterminanthrc))))))))) /\ (((exists ff_h_mdr_minor_yesnonzeroevaluationdeterminanthrb. ff_h_mdr_minor_yesnonzeroevaluationdeterminanthrb + S (mdr_z_minor_yesnonzeroevaluationdeterminanthr) = S ((S (mdr_i_minor_yesnonzeroevaluationdeterminanth)) * mdr_c_minor_yesnonzeroevaluationdeterminant)) /\ exists ff_q_mdr_minor_yesnonzeroevaluationdeterminanthrb. mdr_b_minor_yesnonzeroevaluationdeterminant = ff_q_mdr_minor_yesnonzeroevaluationdeterminanthrb * S ((S (mdr_i_minor_yesnonzeroevaluationdeterminanth)) * mdr_c_minor_yesnonzeroevaluationdeterminant) + (mdr_z_minor_yesnonzeroevaluationdeterminanthr))))) /\ (((((mdr_d_minor_yesnonzeroevaluationdeterminanth) = 0) /\ (((mdr_p_minor_yesnonzeroevaluationdeterminanth) = 1) /\ ((mdr_n_minor_yesnonzeroevaluationdeterminanth) = 0))) \/ exists mdr_q_minor_yesnonzeroevaluationdeterminanths mdr_eb_minor_yesnonzeroevaluationdeterminanths mdr_ec_minor_yesnonzeroevaluationdeterminanths mdr_fb_minor_yesnonzeroevaluationdeterminanths mdr_fc_minor_yesnonzeroevaluationdeterminanths. (((mdr_d_minor_yesnonzeroevaluationdeterminanth) = S (mdr_q_minor_yesnonzeroevaluationdeterminanths)) /\ ((forall mdr_j_minor_yesnonzeroevaluationdeterminanthsc. (exists mdr_gap_minor_yesnonzeroevaluationdeterminanthscj. mdr_gap_minor_yesnonzeroevaluationdeterminanthscj + S (mdr_j_minor_yesnonzeroevaluationdeterminanthsc) = (S (mdr_q_minor_yesnonzeroevaluationdeterminanths))) -> exists mdr_i_minor_yesnonzeroevaluationdeterminanthsc mdr_up_minor_yesnonzeroevaluationdeterminanthsc mdr_us_minor_yesnonzeroevaluationdeterminanthsc mdr_un_minor_yesnonzeroevaluationdeterminanthsc mdr_ut_minor_yesnonzeroevaluationdeterminanthsc mdr_p_minor_yesnonzeroevaluationdeterminanthsc mdr_n_minor_yesnonzeroevaluationdeterminanthsc. ((exists mdr_gap_minor_yesnonzeroevaluationdeterminanthsci. mdr_gap_minor_yesnonzeroevaluationdeterminanthsci + S (mdr_i_minor_yesnonzeroevaluationdeterminanthsc) = (mdr_i_minor_yesnonzeroevaluationdeterminanth)) /\ ((exists mdr_z_minor_yesnonzeroevaluationdeterminanthscr. ((exists mdr_a_minor_yesnonzeroevaluationdeterminanthscrc mdr_b_minor_yesnonzeroevaluationdeterminanthscrc mdr_c_minor_yesnonzeroevaluationdeterminanthscrc mdr_e_minor_yesnonzeroevaluationdeterminanthscrc mdr_f_minor_yesnonzeroevaluationdeterminanthscrc. ((mdr_a_minor_yesnonzeroevaluationdeterminanthscrc = ((mdr_q_minor_yesnonzeroevaluationdeterminanths) + (mdr_up_minor_yesnonzeroevaluationdeterminanthsc)) * S ((mdr_q_minor_yesnonzeroevaluationdeterminanths) + (mdr_up_minor_yesnonzeroevaluationdeterminanthsc)) + ((mdr_up_minor_yesnonzeroevaluationdeterminanthsc) + (mdr_up_minor_yesnonzeroevaluationdeterminanthsc))) /\ ((mdr_b_minor_yesnonzeroevaluationdeterminanthscrc = ((mdr_us_minor_yesnonzeroevaluationdeterminanthsc) + (mdr_un_minor_yesnonzeroevaluationdeterminanthsc)) * S ((mdr_us_minor_yesnonzeroevaluationdeterminanthsc) + (mdr_un_minor_yesnonzeroevaluationdeterminanthsc)) + ((mdr_un_minor_yesnonzeroevaluationdeterminanthsc) + (mdr_un_minor_yesnonzeroevaluationdeterminanthsc))) /\ ((mdr_c_minor_yesnonzeroevaluationdeterminanthscrc = ((mdr_a_minor_yesnonzeroevaluationdeterminanthscrc) + (mdr_b_minor_yesnonzeroevaluationdeterminanthscrc)) * S ((mdr_a_minor_yesnonzeroevaluationdeterminanthscrc) + (mdr_b_minor_yesnonzeroevaluationdeterminanthscrc)) + ((mdr_b_minor_yesnonzeroevaluationdeterminanthscrc) + (mdr_b_minor_yesnonzeroevaluationdeterminanthscrc))) /\ ((mdr_e_minor_yesnonzeroevaluationdeterminanthscrc = ((mdr_p_minor_yesnonzeroevaluationdeterminanthsc) + (mdr_n_minor_yesnonzeroevaluationdeterminanthsc)) * S ((mdr_p_minor_yesnonzeroevaluationdeterminanthsc) + (mdr_n_minor_yesnonzeroevaluationdeterminanthsc)) + ((mdr_n_minor_yesnonzeroevaluationdeterminanthsc) + (mdr_n_minor_yesnonzeroevaluationdeterminanthsc))) /\ ((mdr_f_minor_yesnonzeroevaluationdeterminanthscrc = ((mdr_ut_minor_yesnonzeroevaluationdeterminanthsc) + (mdr_e_minor_yesnonzeroevaluationdeterminanthscrc)) * S ((mdr_ut_minor_yesnonzeroevaluationdeterminanthsc) + (mdr_e_minor_yesnonzeroevaluationdeterminanthscrc)) + ((mdr_e_minor_yesnonzeroevaluationdeterminanthscrc) + (mdr_e_minor_yesnonzeroevaluationdeterminanthscrc))) /\ ((mdr_z_minor_yesnonzeroevaluationdeterminanthscr) = ((mdr_c_minor_yesnonzeroevaluationdeterminanthscrc) + (mdr_f_minor_yesnonzeroevaluationdeterminanthscrc)) * S ((mdr_c_minor_yesnonzeroevaluationdeterminanthscrc) + (mdr_f_minor_yesnonzeroevaluationdeterminanthscrc)) + ((mdr_f_minor_yesnonzeroevaluationdeterminanthscrc) + (mdr_f_minor_yesnonzeroevaluationdeterminanthscrc))))))))) /\ (((exists ff_h_mdr_minor_yesnonzeroevaluationdeterminanthscrb. ff_h_mdr_minor_yesnonzeroevaluationdeterminanthscrb + S (mdr_z_minor_yesnonzeroevaluationdeterminanthscr) = S ((S (mdr_i_minor_yesnonzeroevaluationdeterminanthsc)) * mdr_c_minor_yesnonzeroevaluationdeterminant)) /\ exists ff_q_mdr_minor_yesnonzeroevaluationdeterminanthscrb. mdr_b_minor_yesnonzeroevaluationdeterminant = ff_q_mdr_minor_yesnonzeroevaluationdeterminanthscrb * S ((S (mdr_i_minor_yesnonzeroevaluationdeterminanthsc)) * mdr_c_minor_yesnonzeroevaluationdeterminant) + (mdr_z_minor_yesnonzeroevaluationdeterminanthscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_minor_yesnonzeroevaluationdeterminanthscm_positive. (exists ff_gap_mdm_lt_mdr_minor_yesnonzeroevaluationdeterminanthscm_positive_index_bound. ff_gap_mdm_lt_mdr_minor_yesnonzeroevaluationdeterminanthscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_minor_yesnonzeroevaluationdeterminanthscm_positive) = ((mdr_q_minor_yesnonzeroevaluationdeterminanths) * (mdr_q_minor_yesnonzeroevaluationdeterminanths))) -> exists ff_row_mdm_prefix_mdr_minor_yesnonzeroevaluationdeterminanthscm_positive ff_column_mdm_prefix_mdr_minor_yesnonzeroevaluationdeterminanthscm_positive ff_value_mdm_prefix_mdr_minor_yesnonzeroevaluationdeterminanthscm_positive. (ff_index_mdm_prefix_mdr_minor_yesnonzeroevaluationdeterminanthscm_positive = (mdr_q_minor_yesnonzeroevaluationdeterminanths) * ff_row_mdm_prefix_mdr_minor_yesnonzeroevaluationdeterminanthscm_positive + ff_column_mdm_prefix_mdr_minor_yesnonzeroevaluationdeterminanthscm_positive /\ ((exists ff_gap_mdm_lt_mdr_minor_yesnonzeroevaluationdeterminanthscm_positive_column_bound. ff_gap_mdm_lt_mdr_minor_yesnonzeroevaluationdeterminanthscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_minor_yesnonzeroevaluationdeterminanthscm_positive) = (mdr_q_minor_yesnonzeroevaluationdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_minor_yesnonzeroevaluationdeterminanthscm_positive_cell ff_column_mdm_cell_mdr_minor_yesnonzeroevaluationdeterminanthscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_minor_yesnonzeroevaluationdeterminanthscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_minor_yesnonzeroevaluationdeterminanthscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_minor_yesnonzeroevaluationdeterminanthscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_minor_yesnonzeroevaluationdeterminanthscm_positive_cell = ff_row_mdm_prefix_mdr_minor_yesnonzeroevaluationdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_minor_yesnonzeroevaluationdeterminanthscm_positive_cell_row_after. ff_gap_mdm_le_mdr_minor_yesnonzeroevaluationdeterminanthscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_minor_yesnonzeroevaluationdeterminanthscm_positive)) /\ ff_row_mdm_cell_mdr_minor_yesnonzeroevaluationdeterminanthscm_positive_cell = S ff_row_mdm_prefix_mdr_minor_yesnonzeroevaluationdeterminanthscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_minor_yesnonzeroevaluationdeterminanthscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_minor_yesnonzeroevaluationdeterminanthscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_minor_yesnonzeroevaluationdeterminanthscm_positive) = (mdr_j_minor_yesnonzeroevaluationdeterminanthsc)) /\ ff_column_mdm_cell_mdr_minor_yesnonzeroevaluationdeterminanthscm_positive_cell = ff_column_mdm_prefix_mdr_minor_yesnonzeroevaluationdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_minor_yesnonzeroevaluationdeterminanthscm_positive_cell_column_after. ff_gap_mdm_le_mdr_minor_yesnonzeroevaluationdeterminanthscm_positive_cell_column_after + (mdr_j_minor_yesnonzeroevaluationdeterminanthsc) = (ff_column_mdm_prefix_mdr_minor_yesnonzeroevaluationdeterminanthscm_positive)) /\ ff_column_mdm_cell_mdr_minor_yesnonzeroevaluationdeterminanthscm_positive_cell = S ff_column_mdm_prefix_mdr_minor_yesnonzeroevaluationdeterminanthscm_positive))) /\ (((exists ff_h_mdm_mdr_minor_yesnonzeroevaluationdeterminanthscm_positive_cell_source. ff_h_mdm_mdr_minor_yesnonzeroevaluationdeterminanthscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_minor_yesnonzeroevaluationdeterminanthscm_positive) = S ((S ((ff_row_mdm_cell_mdr_minor_yesnonzeroevaluationdeterminanthscm_positive_cell) * (S (mdr_q_minor_yesnonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_minor_yesnonzeroevaluationdeterminanthscm_positive_cell))) * mdr_pc_minor_yesnonzeroevaluationdeterminanth)) /\ exists ff_q_mdm_mdr_minor_yesnonzeroevaluationdeterminanthscm_positive_cell_source. mdr_pb_minor_yesnonzeroevaluationdeterminanth = ff_q_mdm_mdr_minor_yesnonzeroevaluationdeterminanthscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_minor_yesnonzeroevaluationdeterminanthscm_positive_cell) * (S (mdr_q_minor_yesnonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_minor_yesnonzeroevaluationdeterminanthscm_positive_cell))) * mdr_pc_minor_yesnonzeroevaluationdeterminanth) + (ff_value_mdm_prefix_mdr_minor_yesnonzeroevaluationdeterminanthscm_positive)))))) /\ (((exists ff_h_mdm_mdr_minor_yesnonzeroevaluationdeterminanthscm_positive_target. ff_h_mdm_mdr_minor_yesnonzeroevaluationdeterminanthscm_positive_target + S (ff_value_mdm_prefix_mdr_minor_yesnonzeroevaluationdeterminanthscm_positive) = S ((S (ff_index_mdm_prefix_mdr_minor_yesnonzeroevaluationdeterminanthscm_positive)) * mdr_us_minor_yesnonzeroevaluationdeterminanthsc)) /\ exists ff_q_mdm_mdr_minor_yesnonzeroevaluationdeterminanthscm_positive_target. mdr_up_minor_yesnonzeroevaluationdeterminanthsc = ff_q_mdm_mdr_minor_yesnonzeroevaluationdeterminanthscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_minor_yesnonzeroevaluationdeterminanthscm_positive)) * mdr_us_minor_yesnonzeroevaluationdeterminanthsc) + (ff_value_mdm_prefix_mdr_minor_yesnonzeroevaluationdeterminanthscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_minor_yesnonzeroevaluationdeterminanthscm_negative. (exists ff_gap_mdm_lt_mdr_minor_yesnonzeroevaluationdeterminanthscm_negative_index_bound. ff_gap_mdm_lt_mdr_minor_yesnonzeroevaluationdeterminanthscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_minor_yesnonzeroevaluationdeterminanthscm_negative) = ((mdr_q_minor_yesnonzeroevaluationdeterminanths) * (mdr_q_minor_yesnonzeroevaluationdeterminanths))) -> exists ff_row_mdm_prefix_mdr_minor_yesnonzeroevaluationdeterminanthscm_negative ff_column_mdm_prefix_mdr_minor_yesnonzeroevaluationdeterminanthscm_negative ff_value_mdm_prefix_mdr_minor_yesnonzeroevaluationdeterminanthscm_negative. (ff_index_mdm_prefix_mdr_minor_yesnonzeroevaluationdeterminanthscm_negative = (mdr_q_minor_yesnonzeroevaluationdeterminanths) * ff_row_mdm_prefix_mdr_minor_yesnonzeroevaluationdeterminanthscm_negative + ff_column_mdm_prefix_mdr_minor_yesnonzeroevaluationdeterminanthscm_negative /\ ((exists ff_gap_mdm_lt_mdr_minor_yesnonzeroevaluationdeterminanthscm_negative_column_bound. ff_gap_mdm_lt_mdr_minor_yesnonzeroevaluationdeterminanthscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_minor_yesnonzeroevaluationdeterminanthscm_negative) = (mdr_q_minor_yesnonzeroevaluationdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_minor_yesnonzeroevaluationdeterminanthscm_negative_cell ff_column_mdm_cell_mdr_minor_yesnonzeroevaluationdeterminanthscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_minor_yesnonzeroevaluationdeterminanthscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_minor_yesnonzeroevaluationdeterminanthscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_minor_yesnonzeroevaluationdeterminanthscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_minor_yesnonzeroevaluationdeterminanthscm_negative_cell = ff_row_mdm_prefix_mdr_minor_yesnonzeroevaluationdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_minor_yesnonzeroevaluationdeterminanthscm_negative_cell_row_after. ff_gap_mdm_le_mdr_minor_yesnonzeroevaluationdeterminanthscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_minor_yesnonzeroevaluationdeterminanthscm_negative)) /\ ff_row_mdm_cell_mdr_minor_yesnonzeroevaluationdeterminanthscm_negative_cell = S ff_row_mdm_prefix_mdr_minor_yesnonzeroevaluationdeterminanthscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_minor_yesnonzeroevaluationdeterminanthscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_minor_yesnonzeroevaluationdeterminanthscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_minor_yesnonzeroevaluationdeterminanthscm_negative) = (mdr_j_minor_yesnonzeroevaluationdeterminanthsc)) /\ ff_column_mdm_cell_mdr_minor_yesnonzeroevaluationdeterminanthscm_negative_cell = ff_column_mdm_prefix_mdr_minor_yesnonzeroevaluationdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_minor_yesnonzeroevaluationdeterminanthscm_negative_cell_column_after. ff_gap_mdm_le_mdr_minor_yesnonzeroevaluationdeterminanthscm_negative_cell_column_after + (mdr_j_minor_yesnonzeroevaluationdeterminanthsc) = (ff_column_mdm_prefix_mdr_minor_yesnonzeroevaluationdeterminanthscm_negative)) /\ ff_column_mdm_cell_mdr_minor_yesnonzeroevaluationdeterminanthscm_negative_cell = S ff_column_mdm_prefix_mdr_minor_yesnonzeroevaluationdeterminanthscm_negative))) /\ (((exists ff_h_mdm_mdr_minor_yesnonzeroevaluationdeterminanthscm_negative_cell_source. ff_h_mdm_mdr_minor_yesnonzeroevaluationdeterminanthscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_minor_yesnonzeroevaluationdeterminanthscm_negative) = S ((S ((ff_row_mdm_cell_mdr_minor_yesnonzeroevaluationdeterminanthscm_negative_cell) * (S (mdr_q_minor_yesnonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_minor_yesnonzeroevaluationdeterminanthscm_negative_cell))) * mdr_nc_minor_yesnonzeroevaluationdeterminanth)) /\ exists ff_q_mdm_mdr_minor_yesnonzeroevaluationdeterminanthscm_negative_cell_source. mdr_nb_minor_yesnonzeroevaluationdeterminanth = ff_q_mdm_mdr_minor_yesnonzeroevaluationdeterminanthscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_minor_yesnonzeroevaluationdeterminanthscm_negative_cell) * (S (mdr_q_minor_yesnonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_minor_yesnonzeroevaluationdeterminanthscm_negative_cell))) * mdr_nc_minor_yesnonzeroevaluationdeterminanth) + (ff_value_mdm_prefix_mdr_minor_yesnonzeroevaluationdeterminanthscm_negative)))))) /\ (((exists ff_h_mdm_mdr_minor_yesnonzeroevaluationdeterminanthscm_negative_target. ff_h_mdm_mdr_minor_yesnonzeroevaluationdeterminanthscm_negative_target + S (ff_value_mdm_prefix_mdr_minor_yesnonzeroevaluationdeterminanthscm_negative) = S ((S (ff_index_mdm_prefix_mdr_minor_yesnonzeroevaluationdeterminanthscm_negative)) * mdr_ut_minor_yesnonzeroevaluationdeterminanthsc)) /\ exists ff_q_mdm_mdr_minor_yesnonzeroevaluationdeterminanthscm_negative_target. mdr_un_minor_yesnonzeroevaluationdeterminanthsc = ff_q_mdm_mdr_minor_yesnonzeroevaluationdeterminanthscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_minor_yesnonzeroevaluationdeterminanthscm_negative)) * mdr_ut_minor_yesnonzeroevaluationdeterminanthsc) + (ff_value_mdm_prefix_mdr_minor_yesnonzeroevaluationdeterminanthscm_negative))))))))) /\ ((((exists ff_h_mdr_minor_yesnonzeroevaluationdeterminanthscp. ff_h_mdr_minor_yesnonzeroevaluationdeterminanthscp + S (mdr_p_minor_yesnonzeroevaluationdeterminanthsc) = S ((S (mdr_j_minor_yesnonzeroevaluationdeterminanthsc)) * mdr_ec_minor_yesnonzeroevaluationdeterminanths)) /\ exists ff_q_mdr_minor_yesnonzeroevaluationdeterminanthscp. mdr_eb_minor_yesnonzeroevaluationdeterminanths = ff_q_mdr_minor_yesnonzeroevaluationdeterminanthscp * S ((S (mdr_j_minor_yesnonzeroevaluationdeterminanthsc)) * mdr_ec_minor_yesnonzeroevaluationdeterminanths) + (mdr_p_minor_yesnonzeroevaluationdeterminanthsc))) /\ (((exists ff_h_mdr_minor_yesnonzeroevaluationdeterminanthscn. ff_h_mdr_minor_yesnonzeroevaluationdeterminanthscn + S (mdr_n_minor_yesnonzeroevaluationdeterminanthsc) = S ((S (mdr_j_minor_yesnonzeroevaluationdeterminanthsc)) * mdr_fc_minor_yesnonzeroevaluationdeterminanths)) /\ exists ff_q_mdr_minor_yesnonzeroevaluationdeterminanthscn. mdr_fb_minor_yesnonzeroevaluationdeterminanths = ff_q_mdr_minor_yesnonzeroevaluationdeterminanthscn * S ((S (mdr_j_minor_yesnonzeroevaluationdeterminanthsc)) * mdr_fc_minor_yesnonzeroevaluationdeterminanths) + (mdr_n_minor_yesnonzeroevaluationdeterminanthsc)))))))) /\ (exists ff_ub_mce_fold_mdr_minor_yesnonzeroevaluationdeterminanthsf ff_uc_mce_fold_mdr_minor_yesnonzeroevaluationdeterminanthsf ff_vb_mce_fold_mdr_minor_yesnonzeroevaluationdeterminanthsf ff_vc_mce_fold_mdr_minor_yesnonzeroevaluationdeterminanthsf. ((forall ff_index_mce_alternating_mdr_minor_yesnonzeroevaluationdeterminanthsf_prefix. (exists ff_gap_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_prefix_index. ff_gap_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_prefix_index + S (ff_index_mce_alternating_mdr_minor_yesnonzeroevaluationdeterminanthsf_prefix) = (S (mdr_q_minor_yesnonzeroevaluationdeterminanths))) -> exists ff_ap_mce_alternating_mdr_minor_yesnonzeroevaluationdeterminanthsf_prefix ff_an_mce_alternating_mdr_minor_yesnonzeroevaluationdeterminanthsf_prefix ff_bp_mce_alternating_mdr_minor_yesnonzeroevaluationdeterminanthsf_prefix ff_bn_mce_alternating_mdr_minor_yesnonzeroevaluationdeterminanthsf_prefix ff_p_mce_alternating_mdr_minor_yesnonzeroevaluationdeterminanthsf_prefix ff_n_mce_alternating_mdr_minor_yesnonzeroevaluationdeterminanthsf_prefix. ((((exists ff_h_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_prefix_ap. ff_h_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_prefix_ap + S (ff_ap_mce_alternating_mdr_minor_yesnonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_minor_yesnonzeroevaluationdeterminanthsf_prefix)) * mdr_pc_minor_yesnonzeroevaluationdeterminanth)) /\ exists ff_q_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_prefix_ap. mdr_pb_minor_yesnonzeroevaluationdeterminanth = ff_q_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_minor_yesnonzeroevaluationdeterminanthsf_prefix)) * mdr_pc_minor_yesnonzeroevaluationdeterminanth) + (ff_ap_mce_alternating_mdr_minor_yesnonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_prefix_an. ff_h_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_prefix_an + S (ff_an_mce_alternating_mdr_minor_yesnonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_minor_yesnonzeroevaluationdeterminanthsf_prefix)) * mdr_nc_minor_yesnonzeroevaluationdeterminanth)) /\ exists ff_q_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_prefix_an. mdr_nb_minor_yesnonzeroevaluationdeterminanth = ff_q_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_minor_yesnonzeroevaluationdeterminanthsf_prefix)) * mdr_nc_minor_yesnonzeroevaluationdeterminanth) + (ff_an_mce_alternating_mdr_minor_yesnonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_prefix_bp. ff_h_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_prefix_bp + S (ff_bp_mce_alternating_mdr_minor_yesnonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_minor_yesnonzeroevaluationdeterminanthsf_prefix)) * mdr_ec_minor_yesnonzeroevaluationdeterminanths)) /\ exists ff_q_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_prefix_bp. mdr_eb_minor_yesnonzeroevaluationdeterminanths = ff_q_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_minor_yesnonzeroevaluationdeterminanthsf_prefix)) * mdr_ec_minor_yesnonzeroevaluationdeterminanths) + (ff_bp_mce_alternating_mdr_minor_yesnonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_prefix_bn. ff_h_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_prefix_bn + S (ff_bn_mce_alternating_mdr_minor_yesnonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_minor_yesnonzeroevaluationdeterminanthsf_prefix)) * mdr_fc_minor_yesnonzeroevaluationdeterminanths)) /\ exists ff_q_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_prefix_bn. mdr_fb_minor_yesnonzeroevaluationdeterminanths = ff_q_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_minor_yesnonzeroevaluationdeterminanthsf_prefix)) * mdr_fc_minor_yesnonzeroevaluationdeterminanths) + (ff_bn_mce_alternating_mdr_minor_yesnonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_prefix_positive. ff_h_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_prefix_positive + S (ff_p_mce_alternating_mdr_minor_yesnonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_minor_yesnonzeroevaluationdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_minor_yesnonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_prefix_positive. ff_ub_mce_fold_mdr_minor_yesnonzeroevaluationdeterminanthsf = ff_q_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_minor_yesnonzeroevaluationdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_minor_yesnonzeroevaluationdeterminanthsf) + (ff_p_mce_alternating_mdr_minor_yesnonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_prefix_negative. ff_h_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_prefix_negative + S (ff_n_mce_alternating_mdr_minor_yesnonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_minor_yesnonzeroevaluationdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_minor_yesnonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_prefix_negative. ff_vb_mce_fold_mdr_minor_yesnonzeroevaluationdeterminanthsf = ff_q_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_minor_yesnonzeroevaluationdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_minor_yesnonzeroevaluationdeterminanthsf) + (ff_n_mce_alternating_mdr_minor_yesnonzeroevaluationdeterminanthsf_prefix))) /\ (((exists ff_even_mce_term_mdr_minor_yesnonzeroevaluationdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_minor_yesnonzeroevaluationdeterminanthsf_prefix = 2 * ff_even_mce_term_mdr_minor_yesnonzeroevaluationdeterminanthsf_prefix_term) /\ (ff_p_mce_alternating_mdr_minor_yesnonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_minor_yesnonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_minor_yesnonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_minor_yesnonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_minor_yesnonzeroevaluationdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_minor_yesnonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_minor_yesnonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_minor_yesnonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_minor_yesnonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_minor_yesnonzeroevaluationdeterminanthsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_minor_yesnonzeroevaluationdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_minor_yesnonzeroevaluationdeterminanthsf_prefix = 2 * ff_odd_mce_term_mdr_minor_yesnonzeroevaluationdeterminanthsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_minor_yesnonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_minor_yesnonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_minor_yesnonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_minor_yesnonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_minor_yesnonzeroevaluationdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_minor_yesnonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_minor_yesnonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_minor_yesnonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_minor_yesnonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_minor_yesnonzeroevaluationdeterminanthsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_positive ff_v_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_positive. ((((exists ff_h_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_positive_start. ff_h_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_positive_start. ff_u_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_positive_start * S ((S (0)) * ff_v_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_positive_terminal. ff_h_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_positive_terminal + S (mdr_p_minor_yesnonzeroevaluationdeterminanth) = S ((S ((S (mdr_q_minor_yesnonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_positive_terminal. ff_u_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_positive_terminal * S ((S ((S (mdr_q_minor_yesnonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_positive) + (mdr_p_minor_yesnonzeroevaluationdeterminanth))) /\ forall ff_i_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_positive. (exists ff_lt_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_positive_bound. ff_lt_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_positive_bound + S ff_i_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_positive = (S (mdr_q_minor_yesnonzeroevaluationdeterminanths))) -> exists ff_a_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_positive ff_r_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_positive ff_s_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_positive. ((((exists ff_h_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_positive_summand. ff_h_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_positive_summand + S (ff_a_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_minor_yesnonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_positive_summand. ff_ub_mce_fold_mdr_minor_yesnonzeroevaluationdeterminanthsf = ff_q_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_positive_summand * S ((S (ff_i_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_minor_yesnonzeroevaluationdeterminanthsf) + (ff_a_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_positive_partial. ff_h_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_positive_partial + S (ff_r_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_positive_partial. ff_u_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_positive_partial * S ((S (ff_i_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_positive) + (ff_r_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_positive_successor. ff_h_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_positive_successor + S (ff_s_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_positive) = S ((S (S ff_i_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_positive_successor. ff_u_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_positive_successor * S ((S (S ff_i_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_positive) + (ff_s_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_positive))) /\ ff_s_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_positive = ff_r_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_positive + ff_a_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_positive)))))) /\ (exists ff_u_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_negative ff_v_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_negative. ((((exists ff_h_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_negative_start. ff_h_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_negative_start. ff_u_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_negative_start * S ((S (0)) * ff_v_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_negative_terminal. ff_h_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_negative_terminal + S (mdr_n_minor_yesnonzeroevaluationdeterminanth) = S ((S ((S (mdr_q_minor_yesnonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_negative_terminal. ff_u_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_negative_terminal * S ((S ((S (mdr_q_minor_yesnonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_negative) + (mdr_n_minor_yesnonzeroevaluationdeterminanth))) /\ forall ff_i_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_negative. (exists ff_lt_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_negative_bound. ff_lt_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_negative_bound + S ff_i_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_negative = (S (mdr_q_minor_yesnonzeroevaluationdeterminanths))) -> exists ff_a_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_negative ff_r_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_negative ff_s_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_negative. ((((exists ff_h_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_negative_summand. ff_h_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_negative_summand + S (ff_a_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_minor_yesnonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_negative_summand. ff_vb_mce_fold_mdr_minor_yesnonzeroevaluationdeterminanthsf = ff_q_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_negative_summand * S ((S (ff_i_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_minor_yesnonzeroevaluationdeterminanthsf) + (ff_a_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_negative_partial. ff_h_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_negative_partial + S (ff_r_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_negative_partial. ff_u_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_negative_partial * S ((S (ff_i_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_negative) + (ff_r_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_negative_successor. ff_h_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_negative_successor + S (ff_s_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_negative) = S ((S (S ff_i_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_negative_successor. ff_u_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_negative_successor * S ((S (S ff_i_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_negative) + (ff_s_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_negative))) /\ ff_s_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_negative = ff_r_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_negative + ff_a_mce_mdr_minor_yesnonzeroevaluationdeterminanthsf_negative))))))))))))))) /\ ((exists mdr_gap_minor_yesnonzeroevaluationdeterminanti. mdr_gap_minor_yesnonzeroevaluationdeterminanti + S (mdr_i_minor_yesnonzeroevaluationdeterminant) = (mdr_l_minor_yesnonzeroevaluationdeterminant)) /\ (exists mdr_z_minor_yesnonzeroevaluationdeterminantr. ((exists mdr_a_minor_yesnonzeroevaluationdeterminantrc mdr_b_minor_yesnonzeroevaluationdeterminantrc mdr_c_minor_yesnonzeroevaluationdeterminantrc mdr_e_minor_yesnonzeroevaluationdeterminantrc mdr_f_minor_yesnonzeroevaluationdeterminantrc. ((mdr_a_minor_yesnonzeroevaluationdeterminantrc = ((q) + (mdr_ub_minor_yesnonzeroevaluation)) * S ((q) + (mdr_ub_minor_yesnonzeroevaluation)) + ((mdr_ub_minor_yesnonzeroevaluation) + (mdr_ub_minor_yesnonzeroevaluation))) /\ ((mdr_b_minor_yesnonzeroevaluationdeterminantrc = ((mdr_uc_minor_yesnonzeroevaluation) + (mdr_vb_minor_yesnonzeroevaluation)) * S ((mdr_uc_minor_yesnonzeroevaluation) + (mdr_vb_minor_yesnonzeroevaluation)) + ((mdr_vb_minor_yesnonzeroevaluation) + (mdr_vb_minor_yesnonzeroevaluation))) /\ ((mdr_c_minor_yesnonzeroevaluationdeterminantrc = ((mdr_a_minor_yesnonzeroevaluationdeterminantrc) + (mdr_b_minor_yesnonzeroevaluationdeterminantrc)) * S ((mdr_a_minor_yesnonzeroevaluationdeterminantrc) + (mdr_b_minor_yesnonzeroevaluationdeterminantrc)) + ((mdr_b_minor_yesnonzeroevaluationdeterminantrc) + (mdr_b_minor_yesnonzeroevaluationdeterminantrc))) /\ ((mdr_e_minor_yesnonzeroevaluationdeterminantrc = ((mdr_p_minor_yesnonzero) + (mdr_n_minor_yesnonzero)) * S ((mdr_p_minor_yesnonzero) + (mdr_n_minor_yesnonzero)) + ((mdr_n_minor_yesnonzero) + (mdr_n_minor_yesnonzero))) /\ ((mdr_f_minor_yesnonzeroevaluationdeterminantrc = ((mdr_vc_minor_yesnonzeroevaluation) + (mdr_e_minor_yesnonzeroevaluationdeterminantrc)) * S ((mdr_vc_minor_yesnonzeroevaluation) + (mdr_e_minor_yesnonzeroevaluationdeterminantrc)) + ((mdr_e_minor_yesnonzeroevaluationdeterminantrc) + (mdr_e_minor_yesnonzeroevaluationdeterminantrc))) /\ ((mdr_z_minor_yesnonzeroevaluationdeterminantr) = ((mdr_c_minor_yesnonzeroevaluationdeterminantrc) + (mdr_f_minor_yesnonzeroevaluationdeterminantrc)) * S ((mdr_c_minor_yesnonzeroevaluationdeterminantrc) + (mdr_f_minor_yesnonzeroevaluationdeterminantrc)) + ((mdr_f_minor_yesnonzeroevaluationdeterminantrc) + (mdr_f_minor_yesnonzeroevaluationdeterminantrc))))))))) /\ (((exists ff_h_mdr_minor_yesnonzeroevaluationdeterminantrb. ff_h_mdr_minor_yesnonzeroevaluationdeterminantrb + S (mdr_z_minor_yesnonzeroevaluationdeterminantr) = S ((S (mdr_i_minor_yesnonzeroevaluationdeterminant)) * mdr_c_minor_yesnonzeroevaluationdeterminant)) /\ exists ff_q_mdr_minor_yesnonzeroevaluationdeterminantrb. mdr_b_minor_yesnonzeroevaluationdeterminant = ff_q_mdr_minor_yesnonzeroevaluationdeterminantrb * S ((S (mdr_i_minor_yesnonzeroevaluationdeterminant)) * mdr_c_minor_yesnonzeroevaluationdeterminant) + (mdr_z_minor_yesnonzeroevaluationdeterminantr)))))))))) /\ (~(mdr_p_minor_yesnonzero = mdr_n_minor_yesnonzero))))))) \/ ~(((((forall fom_index_mrf_minor_norowsbound. (exists fom_gap_mrf_minor_norowsbound_index_bound. fom_gap_mrf_minor_norowsbound_index_bound + S (fom_index_mrf_minor_norowsbound) = q) -> exists fom_value_mrf_minor_norowsbound. ((((exists fom_beta_height_mrf_minor_norowsbound_entry. fom_beta_height_mrf_minor_norowsbound_entry + S (fom_value_mrf_minor_norowsbound) = S ((S (fom_index_mrf_minor_norowsbound)) * rc)) /\ exists fom_beta_quotient_mrf_minor_norowsbound_entry. rb = fom_beta_quotient_mrf_minor_norowsbound_entry * S ((S (fom_index_mrf_minor_norowsbound)) * rc) + (fom_value_mrf_minor_norowsbound))) /\ (exists fom_gap_mrf_minor_norowsbound_value_bound. fom_gap_mrf_minor_norowsbound_value_bound + S (fom_value_mrf_minor_norowsbound) = r))) /\ (forall mdr_i_minor_norowsdistinct mdr_j_minor_norowsdistinct mdr_a_minor_norowsdistinct. (exists mdr_gap_minor_norowsdistincti. mdr_gap_minor_norowsdistincti + S (mdr_i_minor_norowsdistinct) = (q)) -> (exists mdr_gap_minor_norowsdistinctj. mdr_gap_minor_norowsdistinctj + S (mdr_j_minor_norowsdistinct) = (q)) -> (((exists ff_h_mdr_minor_norowsdistinctfirst. ff_h_mdr_minor_norowsdistinctfirst + S (mdr_a_minor_norowsdistinct) = S ((S (mdr_i_minor_norowsdistinct)) * rc)) /\ exists ff_q_mdr_minor_norowsdistinctfirst. rb = ff_q_mdr_minor_norowsdistinctfirst * S ((S (mdr_i_minor_norowsdistinct)) * rc) + (mdr_a_minor_norowsdistinct))) -> (((exists ff_h_mdr_minor_norowsdistinctsecond. ff_h_mdr_minor_norowsdistinctsecond + S (mdr_a_minor_norowsdistinct) = S ((S (mdr_j_minor_norowsdistinct)) * rc)) /\ exists ff_q_mdr_minor_norowsdistinctsecond. rb = ff_q_mdr_minor_norowsdistinctsecond * S ((S (mdr_j_minor_norowsdistinct)) * rc) + (mdr_a_minor_norowsdistinct))) -> mdr_i_minor_norowsdistinct = mdr_j_minor_norowsdistinct))) /\ ((((forall fom_index_mrf_minor_nocolumnsbound. (exists fom_gap_mrf_minor_nocolumnsbound_index_bound. fom_gap_mrf_minor_nocolumnsbound_index_bound + S (fom_index_mrf_minor_nocolumnsbound) = q) -> exists fom_value_mrf_minor_nocolumnsbound. ((((exists fom_beta_height_mrf_minor_nocolumnsbound_entry. fom_beta_height_mrf_minor_nocolumnsbound_entry + S (fom_value_mrf_minor_nocolumnsbound) = S ((S (fom_index_mrf_minor_nocolumnsbound)) * cc)) /\ exists fom_beta_quotient_mrf_minor_nocolumnsbound_entry. cb = fom_beta_quotient_mrf_minor_nocolumnsbound_entry * S ((S (fom_index_mrf_minor_nocolumnsbound)) * cc) + (fom_value_mrf_minor_nocolumnsbound))) /\ (exists fom_gap_mrf_minor_nocolumnsbound_value_bound. fom_gap_mrf_minor_nocolumnsbound_value_bound + S (fom_value_mrf_minor_nocolumnsbound) = w))) /\ (forall mdr_i_minor_nocolumnsdistinct mdr_j_minor_nocolumnsdistinct mdr_a_minor_nocolumnsdistinct. (exists mdr_gap_minor_nocolumnsdistincti. mdr_gap_minor_nocolumnsdistincti + S (mdr_i_minor_nocolumnsdistinct) = (q)) -> (exists mdr_gap_minor_nocolumnsdistinctj. mdr_gap_minor_nocolumnsdistinctj + S (mdr_j_minor_nocolumnsdistinct) = (q)) -> (((exists ff_h_mdr_minor_nocolumnsdistinctfirst. ff_h_mdr_minor_nocolumnsdistinctfirst + S (mdr_a_minor_nocolumnsdistinct) = S ((S (mdr_i_minor_nocolumnsdistinct)) * cc)) /\ exists ff_q_mdr_minor_nocolumnsdistinctfirst. cb = ff_q_mdr_minor_nocolumnsdistinctfirst * S ((S (mdr_i_minor_nocolumnsdistinct)) * cc) + (mdr_a_minor_nocolumnsdistinct))) -> (((exists ff_h_mdr_minor_nocolumnsdistinctsecond. ff_h_mdr_minor_nocolumnsdistinctsecond + S (mdr_a_minor_nocolumnsdistinct) = S ((S (mdr_j_minor_nocolumnsdistinct)) * cc)) /\ exists ff_q_mdr_minor_nocolumnsdistinctsecond. cb = ff_q_mdr_minor_nocolumnsdistinctsecond * S ((S (mdr_j_minor_nocolumnsdistinct)) * cc) + (mdr_a_minor_nocolumnsdistinct))) -> mdr_i_minor_nocolumnsdistinct = mdr_j_minor_nocolumnsdistinct))) /\ (exists mdr_p_minor_nononzero mdr_n_minor_nononzero. ((exists mdr_ub_minor_nononzeroevaluation mdr_uc_minor_nononzeroevaluation mdr_vb_minor_nononzeroevaluation mdr_vc_minor_nononzeroevaluation. ((((forall mdr_i_minor_nononzeroevaluationmatrixpositive. (exists mdr_gap_minor_nononzeroevaluationmatrixpositivebound. mdr_gap_minor_nononzeroevaluationmatrixpositivebound + S (mdr_i_minor_nononzeroevaluationmatrixpositive) = ((q) * (q))) -> exists mdr_a_minor_nononzeroevaluationmatrixpositive. (((exists mdr_r_minor_nononzeroevaluationmatrixpositivepoint mdr_s_minor_nononzeroevaluationmatrixpositivepoint mdr_u_minor_nononzeroevaluationmatrixpositivepoint mdr_v_minor_nononzeroevaluationmatrixpositivepoint. ((mdr_i_minor_nononzeroevaluationmatrixpositive = (q) * mdr_r_minor_nononzeroevaluationmatrixpositivepoint + mdr_s_minor_nononzeroevaluationmatrixpositivepoint) /\ ((exists mdr_gap_minor_nononzeroevaluationmatrixpositivepointcolumn. mdr_gap_minor_nononzeroevaluationmatrixpositivepointcolumn + S (mdr_s_minor_nononzeroevaluationmatrixpositivepoint) = (q)) /\ ((((exists ff_h_mdr_minor_nononzeroevaluationmatrixpositivepointrow_index. ff_h_mdr_minor_nononzeroevaluationmatrixpositivepointrow_index + S (mdr_u_minor_nononzeroevaluationmatrixpositivepoint) = S ((S (mdr_r_minor_nononzeroevaluationmatrixpositivepoint)) * rc)) /\ exists ff_q_mdr_minor_nononzeroevaluationmatrixpositivepointrow_index. rb = ff_q_mdr_minor_nononzeroevaluationmatrixpositivepointrow_index * S ((S (mdr_r_minor_nononzeroevaluationmatrixpositivepoint)) * rc) + (mdr_u_minor_nononzeroevaluationmatrixpositivepoint))) /\ ((((exists ff_h_mdr_minor_nononzeroevaluationmatrixpositivepointcolumn_index. ff_h_mdr_minor_nononzeroevaluationmatrixpositivepointcolumn_index + S (mdr_v_minor_nononzeroevaluationmatrixpositivepoint) = S ((S (mdr_s_minor_nononzeroevaluationmatrixpositivepoint)) * cc)) /\ exists ff_q_mdr_minor_nononzeroevaluationmatrixpositivepointcolumn_index. cb = ff_q_mdr_minor_nononzeroevaluationmatrixpositivepointcolumn_index * S ((S (mdr_s_minor_nononzeroevaluationmatrixpositivepoint)) * cc) + (mdr_v_minor_nononzeroevaluationmatrixpositivepoint))) /\ (((exists ff_h_mdr_minor_nononzeroevaluationmatrixpositivepointsource. ff_h_mdr_minor_nononzeroevaluationmatrixpositivepointsource + S (mdr_a_minor_nononzeroevaluationmatrixpositive) = S ((S ((mdr_u_minor_nononzeroevaluationmatrixpositivepoint) * (w) + (mdr_v_minor_nononzeroevaluationmatrixpositivepoint))) * pc)) /\ exists ff_q_mdr_minor_nononzeroevaluationmatrixpositivepointsource. pb = ff_q_mdr_minor_nononzeroevaluationmatrixpositivepointsource * S ((S ((mdr_u_minor_nononzeroevaluationmatrixpositivepoint) * (w) + (mdr_v_minor_nononzeroevaluationmatrixpositivepoint))) * pc) + (mdr_a_minor_nononzeroevaluationmatrixpositive)))))))) /\ (((exists ff_h_mdr_minor_nononzeroevaluationmatrixpositiveoutput. ff_h_mdr_minor_nononzeroevaluationmatrixpositiveoutput + S (mdr_a_minor_nononzeroevaluationmatrixpositive) = S ((S (mdr_i_minor_nononzeroevaluationmatrixpositive)) * mdr_uc_minor_nononzeroevaluation)) /\ exists ff_q_mdr_minor_nononzeroevaluationmatrixpositiveoutput. mdr_ub_minor_nononzeroevaluation = ff_q_mdr_minor_nononzeroevaluationmatrixpositiveoutput * S ((S (mdr_i_minor_nononzeroevaluationmatrixpositive)) * mdr_uc_minor_nononzeroevaluation) + (mdr_a_minor_nononzeroevaluationmatrixpositive)))))) /\ (forall mdr_i_minor_nononzeroevaluationmatrixnegative. (exists mdr_gap_minor_nononzeroevaluationmatrixnegativebound. mdr_gap_minor_nononzeroevaluationmatrixnegativebound + S (mdr_i_minor_nononzeroevaluationmatrixnegative) = ((q) * (q))) -> exists mdr_a_minor_nononzeroevaluationmatrixnegative. (((exists mdr_r_minor_nononzeroevaluationmatrixnegativepoint mdr_s_minor_nononzeroevaluationmatrixnegativepoint mdr_u_minor_nononzeroevaluationmatrixnegativepoint mdr_v_minor_nononzeroevaluationmatrixnegativepoint. ((mdr_i_minor_nononzeroevaluationmatrixnegative = (q) * mdr_r_minor_nononzeroevaluationmatrixnegativepoint + mdr_s_minor_nononzeroevaluationmatrixnegativepoint) /\ ((exists mdr_gap_minor_nononzeroevaluationmatrixnegativepointcolumn. mdr_gap_minor_nononzeroevaluationmatrixnegativepointcolumn + S (mdr_s_minor_nononzeroevaluationmatrixnegativepoint) = (q)) /\ ((((exists ff_h_mdr_minor_nononzeroevaluationmatrixnegativepointrow_index. ff_h_mdr_minor_nononzeroevaluationmatrixnegativepointrow_index + S (mdr_u_minor_nononzeroevaluationmatrixnegativepoint) = S ((S (mdr_r_minor_nononzeroevaluationmatrixnegativepoint)) * rc)) /\ exists ff_q_mdr_minor_nononzeroevaluationmatrixnegativepointrow_index. rb = ff_q_mdr_minor_nononzeroevaluationmatrixnegativepointrow_index * S ((S (mdr_r_minor_nononzeroevaluationmatrixnegativepoint)) * rc) + (mdr_u_minor_nononzeroevaluationmatrixnegativepoint))) /\ ((((exists ff_h_mdr_minor_nononzeroevaluationmatrixnegativepointcolumn_index. ff_h_mdr_minor_nononzeroevaluationmatrixnegativepointcolumn_index + S (mdr_v_minor_nononzeroevaluationmatrixnegativepoint) = S ((S (mdr_s_minor_nononzeroevaluationmatrixnegativepoint)) * cc)) /\ exists ff_q_mdr_minor_nononzeroevaluationmatrixnegativepointcolumn_index. cb = ff_q_mdr_minor_nononzeroevaluationmatrixnegativepointcolumn_index * S ((S (mdr_s_minor_nononzeroevaluationmatrixnegativepoint)) * cc) + (mdr_v_minor_nononzeroevaluationmatrixnegativepoint))) /\ (((exists ff_h_mdr_minor_nononzeroevaluationmatrixnegativepointsource. ff_h_mdr_minor_nononzeroevaluationmatrixnegativepointsource + S (mdr_a_minor_nononzeroevaluationmatrixnegative) = S ((S ((mdr_u_minor_nononzeroevaluationmatrixnegativepoint) * (w) + (mdr_v_minor_nononzeroevaluationmatrixnegativepoint))) * nc)) /\ exists ff_q_mdr_minor_nononzeroevaluationmatrixnegativepointsource. nb = ff_q_mdr_minor_nononzeroevaluationmatrixnegativepointsource * S ((S ((mdr_u_minor_nononzeroevaluationmatrixnegativepoint) * (w) + (mdr_v_minor_nononzeroevaluationmatrixnegativepoint))) * nc) + (mdr_a_minor_nononzeroevaluationmatrixnegative)))))))) /\ (((exists ff_h_mdr_minor_nononzeroevaluationmatrixnegativeoutput. ff_h_mdr_minor_nononzeroevaluationmatrixnegativeoutput + S (mdr_a_minor_nononzeroevaluationmatrixnegative) = S ((S (mdr_i_minor_nononzeroevaluationmatrixnegative)) * mdr_vc_minor_nononzeroevaluation)) /\ exists ff_q_mdr_minor_nononzeroevaluationmatrixnegativeoutput. mdr_vb_minor_nononzeroevaluation = ff_q_mdr_minor_nononzeroevaluationmatrixnegativeoutput * S ((S (mdr_i_minor_nononzeroevaluationmatrixnegative)) * mdr_vc_minor_nononzeroevaluation) + (mdr_a_minor_nononzeroevaluationmatrixnegative)))))))) /\ (exists mdr_b_minor_nononzeroevaluationdeterminant mdr_c_minor_nononzeroevaluationdeterminant mdr_l_minor_nononzeroevaluationdeterminant mdr_i_minor_nononzeroevaluationdeterminant. ((forall mdr_i_minor_nononzeroevaluationdeterminanth. (exists mdr_gap_minor_nononzeroevaluationdeterminanthi. mdr_gap_minor_nononzeroevaluationdeterminanthi + S (mdr_i_minor_nononzeroevaluationdeterminanth) = (mdr_l_minor_nononzeroevaluationdeterminant)) -> exists mdr_d_minor_nononzeroevaluationdeterminanth mdr_pb_minor_nononzeroevaluationdeterminanth mdr_pc_minor_nononzeroevaluationdeterminanth mdr_nb_minor_nononzeroevaluationdeterminanth mdr_nc_minor_nononzeroevaluationdeterminanth mdr_p_minor_nononzeroevaluationdeterminanth mdr_n_minor_nononzeroevaluationdeterminanth. ((exists mdr_z_minor_nononzeroevaluationdeterminanthr. ((exists mdr_a_minor_nononzeroevaluationdeterminanthrc mdr_b_minor_nononzeroevaluationdeterminanthrc mdr_c_minor_nononzeroevaluationdeterminanthrc mdr_e_minor_nononzeroevaluationdeterminanthrc mdr_f_minor_nononzeroevaluationdeterminanthrc. ((mdr_a_minor_nononzeroevaluationdeterminanthrc = ((mdr_d_minor_nononzeroevaluationdeterminanth) + (mdr_pb_minor_nononzeroevaluationdeterminanth)) * S ((mdr_d_minor_nononzeroevaluationdeterminanth) + (mdr_pb_minor_nononzeroevaluationdeterminanth)) + ((mdr_pb_minor_nononzeroevaluationdeterminanth) + (mdr_pb_minor_nononzeroevaluationdeterminanth))) /\ ((mdr_b_minor_nononzeroevaluationdeterminanthrc = ((mdr_pc_minor_nononzeroevaluationdeterminanth) + (mdr_nb_minor_nononzeroevaluationdeterminanth)) * S ((mdr_pc_minor_nononzeroevaluationdeterminanth) + (mdr_nb_minor_nononzeroevaluationdeterminanth)) + ((mdr_nb_minor_nononzeroevaluationdeterminanth) + (mdr_nb_minor_nononzeroevaluationdeterminanth))) /\ ((mdr_c_minor_nononzeroevaluationdeterminanthrc = ((mdr_a_minor_nononzeroevaluationdeterminanthrc) + (mdr_b_minor_nononzeroevaluationdeterminanthrc)) * S ((mdr_a_minor_nononzeroevaluationdeterminanthrc) + (mdr_b_minor_nononzeroevaluationdeterminanthrc)) + ((mdr_b_minor_nononzeroevaluationdeterminanthrc) + (mdr_b_minor_nononzeroevaluationdeterminanthrc))) /\ ((mdr_e_minor_nononzeroevaluationdeterminanthrc = ((mdr_p_minor_nononzeroevaluationdeterminanth) + (mdr_n_minor_nononzeroevaluationdeterminanth)) * S ((mdr_p_minor_nononzeroevaluationdeterminanth) + (mdr_n_minor_nononzeroevaluationdeterminanth)) + ((mdr_n_minor_nononzeroevaluationdeterminanth) + (mdr_n_minor_nononzeroevaluationdeterminanth))) /\ ((mdr_f_minor_nononzeroevaluationdeterminanthrc = ((mdr_nc_minor_nononzeroevaluationdeterminanth) + (mdr_e_minor_nononzeroevaluationdeterminanthrc)) * S ((mdr_nc_minor_nononzeroevaluationdeterminanth) + (mdr_e_minor_nononzeroevaluationdeterminanthrc)) + ((mdr_e_minor_nononzeroevaluationdeterminanthrc) + (mdr_e_minor_nononzeroevaluationdeterminanthrc))) /\ ((mdr_z_minor_nononzeroevaluationdeterminanthr) = ((mdr_c_minor_nononzeroevaluationdeterminanthrc) + (mdr_f_minor_nononzeroevaluationdeterminanthrc)) * S ((mdr_c_minor_nononzeroevaluationdeterminanthrc) + (mdr_f_minor_nononzeroevaluationdeterminanthrc)) + ((mdr_f_minor_nononzeroevaluationdeterminanthrc) + (mdr_f_minor_nononzeroevaluationdeterminanthrc))))))))) /\ (((exists ff_h_mdr_minor_nononzeroevaluationdeterminanthrb. ff_h_mdr_minor_nononzeroevaluationdeterminanthrb + S (mdr_z_minor_nononzeroevaluationdeterminanthr) = S ((S (mdr_i_minor_nononzeroevaluationdeterminanth)) * mdr_c_minor_nononzeroevaluationdeterminant)) /\ exists ff_q_mdr_minor_nononzeroevaluationdeterminanthrb. mdr_b_minor_nononzeroevaluationdeterminant = ff_q_mdr_minor_nononzeroevaluationdeterminanthrb * S ((S (mdr_i_minor_nononzeroevaluationdeterminanth)) * mdr_c_minor_nononzeroevaluationdeterminant) + (mdr_z_minor_nononzeroevaluationdeterminanthr))))) /\ (((((mdr_d_minor_nononzeroevaluationdeterminanth) = 0) /\ (((mdr_p_minor_nononzeroevaluationdeterminanth) = 1) /\ ((mdr_n_minor_nononzeroevaluationdeterminanth) = 0))) \/ exists mdr_q_minor_nononzeroevaluationdeterminanths mdr_eb_minor_nononzeroevaluationdeterminanths mdr_ec_minor_nononzeroevaluationdeterminanths mdr_fb_minor_nononzeroevaluationdeterminanths mdr_fc_minor_nononzeroevaluationdeterminanths. (((mdr_d_minor_nononzeroevaluationdeterminanth) = S (mdr_q_minor_nononzeroevaluationdeterminanths)) /\ ((forall mdr_j_minor_nononzeroevaluationdeterminanthsc. (exists mdr_gap_minor_nononzeroevaluationdeterminanthscj. mdr_gap_minor_nononzeroevaluationdeterminanthscj + S (mdr_j_minor_nononzeroevaluationdeterminanthsc) = (S (mdr_q_minor_nononzeroevaluationdeterminanths))) -> exists mdr_i_minor_nononzeroevaluationdeterminanthsc mdr_up_minor_nononzeroevaluationdeterminanthsc mdr_us_minor_nononzeroevaluationdeterminanthsc mdr_un_minor_nononzeroevaluationdeterminanthsc mdr_ut_minor_nononzeroevaluationdeterminanthsc mdr_p_minor_nononzeroevaluationdeterminanthsc mdr_n_minor_nononzeroevaluationdeterminanthsc. ((exists mdr_gap_minor_nononzeroevaluationdeterminanthsci. mdr_gap_minor_nononzeroevaluationdeterminanthsci + S (mdr_i_minor_nononzeroevaluationdeterminanthsc) = (mdr_i_minor_nononzeroevaluationdeterminanth)) /\ ((exists mdr_z_minor_nononzeroevaluationdeterminanthscr. ((exists mdr_a_minor_nononzeroevaluationdeterminanthscrc mdr_b_minor_nononzeroevaluationdeterminanthscrc mdr_c_minor_nononzeroevaluationdeterminanthscrc mdr_e_minor_nononzeroevaluationdeterminanthscrc mdr_f_minor_nononzeroevaluationdeterminanthscrc. ((mdr_a_minor_nononzeroevaluationdeterminanthscrc = ((mdr_q_minor_nononzeroevaluationdeterminanths) + (mdr_up_minor_nononzeroevaluationdeterminanthsc)) * S ((mdr_q_minor_nononzeroevaluationdeterminanths) + (mdr_up_minor_nononzeroevaluationdeterminanthsc)) + ((mdr_up_minor_nononzeroevaluationdeterminanthsc) + (mdr_up_minor_nononzeroevaluationdeterminanthsc))) /\ ((mdr_b_minor_nononzeroevaluationdeterminanthscrc = ((mdr_us_minor_nononzeroevaluationdeterminanthsc) + (mdr_un_minor_nononzeroevaluationdeterminanthsc)) * S ((mdr_us_minor_nononzeroevaluationdeterminanthsc) + (mdr_un_minor_nononzeroevaluationdeterminanthsc)) + ((mdr_un_minor_nononzeroevaluationdeterminanthsc) + (mdr_un_minor_nononzeroevaluationdeterminanthsc))) /\ ((mdr_c_minor_nononzeroevaluationdeterminanthscrc = ((mdr_a_minor_nononzeroevaluationdeterminanthscrc) + (mdr_b_minor_nononzeroevaluationdeterminanthscrc)) * S ((mdr_a_minor_nononzeroevaluationdeterminanthscrc) + (mdr_b_minor_nononzeroevaluationdeterminanthscrc)) + ((mdr_b_minor_nononzeroevaluationdeterminanthscrc) + (mdr_b_minor_nononzeroevaluationdeterminanthscrc))) /\ ((mdr_e_minor_nononzeroevaluationdeterminanthscrc = ((mdr_p_minor_nononzeroevaluationdeterminanthsc) + (mdr_n_minor_nononzeroevaluationdeterminanthsc)) * S ((mdr_p_minor_nononzeroevaluationdeterminanthsc) + (mdr_n_minor_nononzeroevaluationdeterminanthsc)) + ((mdr_n_minor_nononzeroevaluationdeterminanthsc) + (mdr_n_minor_nononzeroevaluationdeterminanthsc))) /\ ((mdr_f_minor_nononzeroevaluationdeterminanthscrc = ((mdr_ut_minor_nononzeroevaluationdeterminanthsc) + (mdr_e_minor_nononzeroevaluationdeterminanthscrc)) * S ((mdr_ut_minor_nononzeroevaluationdeterminanthsc) + (mdr_e_minor_nononzeroevaluationdeterminanthscrc)) + ((mdr_e_minor_nononzeroevaluationdeterminanthscrc) + (mdr_e_minor_nononzeroevaluationdeterminanthscrc))) /\ ((mdr_z_minor_nononzeroevaluationdeterminanthscr) = ((mdr_c_minor_nononzeroevaluationdeterminanthscrc) + (mdr_f_minor_nononzeroevaluationdeterminanthscrc)) * S ((mdr_c_minor_nononzeroevaluationdeterminanthscrc) + (mdr_f_minor_nononzeroevaluationdeterminanthscrc)) + ((mdr_f_minor_nononzeroevaluationdeterminanthscrc) + (mdr_f_minor_nononzeroevaluationdeterminanthscrc))))))))) /\ (((exists ff_h_mdr_minor_nononzeroevaluationdeterminanthscrb. ff_h_mdr_minor_nononzeroevaluationdeterminanthscrb + S (mdr_z_minor_nononzeroevaluationdeterminanthscr) = S ((S (mdr_i_minor_nononzeroevaluationdeterminanthsc)) * mdr_c_minor_nononzeroevaluationdeterminant)) /\ exists ff_q_mdr_minor_nononzeroevaluationdeterminanthscrb. mdr_b_minor_nononzeroevaluationdeterminant = ff_q_mdr_minor_nononzeroevaluationdeterminanthscrb * S ((S (mdr_i_minor_nononzeroevaluationdeterminanthsc)) * mdr_c_minor_nononzeroevaluationdeterminant) + (mdr_z_minor_nononzeroevaluationdeterminanthscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_minor_nononzeroevaluationdeterminanthscm_positive. (exists ff_gap_mdm_lt_mdr_minor_nononzeroevaluationdeterminanthscm_positive_index_bound. ff_gap_mdm_lt_mdr_minor_nononzeroevaluationdeterminanthscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_minor_nononzeroevaluationdeterminanthscm_positive) = ((mdr_q_minor_nononzeroevaluationdeterminanths) * (mdr_q_minor_nononzeroevaluationdeterminanths))) -> exists ff_row_mdm_prefix_mdr_minor_nononzeroevaluationdeterminanthscm_positive ff_column_mdm_prefix_mdr_minor_nononzeroevaluationdeterminanthscm_positive ff_value_mdm_prefix_mdr_minor_nononzeroevaluationdeterminanthscm_positive. (ff_index_mdm_prefix_mdr_minor_nononzeroevaluationdeterminanthscm_positive = (mdr_q_minor_nononzeroevaluationdeterminanths) * ff_row_mdm_prefix_mdr_minor_nononzeroevaluationdeterminanthscm_positive + ff_column_mdm_prefix_mdr_minor_nononzeroevaluationdeterminanthscm_positive /\ ((exists ff_gap_mdm_lt_mdr_minor_nononzeroevaluationdeterminanthscm_positive_column_bound. ff_gap_mdm_lt_mdr_minor_nononzeroevaluationdeterminanthscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_minor_nononzeroevaluationdeterminanthscm_positive) = (mdr_q_minor_nononzeroevaluationdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_minor_nononzeroevaluationdeterminanthscm_positive_cell ff_column_mdm_cell_mdr_minor_nononzeroevaluationdeterminanthscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_minor_nononzeroevaluationdeterminanthscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_minor_nononzeroevaluationdeterminanthscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_minor_nononzeroevaluationdeterminanthscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_minor_nononzeroevaluationdeterminanthscm_positive_cell = ff_row_mdm_prefix_mdr_minor_nononzeroevaluationdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_minor_nononzeroevaluationdeterminanthscm_positive_cell_row_after. ff_gap_mdm_le_mdr_minor_nononzeroevaluationdeterminanthscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_minor_nononzeroevaluationdeterminanthscm_positive)) /\ ff_row_mdm_cell_mdr_minor_nononzeroevaluationdeterminanthscm_positive_cell = S ff_row_mdm_prefix_mdr_minor_nononzeroevaluationdeterminanthscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_minor_nononzeroevaluationdeterminanthscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_minor_nononzeroevaluationdeterminanthscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_minor_nononzeroevaluationdeterminanthscm_positive) = (mdr_j_minor_nononzeroevaluationdeterminanthsc)) /\ ff_column_mdm_cell_mdr_minor_nononzeroevaluationdeterminanthscm_positive_cell = ff_column_mdm_prefix_mdr_minor_nononzeroevaluationdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_minor_nononzeroevaluationdeterminanthscm_positive_cell_column_after. ff_gap_mdm_le_mdr_minor_nononzeroevaluationdeterminanthscm_positive_cell_column_after + (mdr_j_minor_nononzeroevaluationdeterminanthsc) = (ff_column_mdm_prefix_mdr_minor_nononzeroevaluationdeterminanthscm_positive)) /\ ff_column_mdm_cell_mdr_minor_nononzeroevaluationdeterminanthscm_positive_cell = S ff_column_mdm_prefix_mdr_minor_nononzeroevaluationdeterminanthscm_positive))) /\ (((exists ff_h_mdm_mdr_minor_nononzeroevaluationdeterminanthscm_positive_cell_source. ff_h_mdm_mdr_minor_nononzeroevaluationdeterminanthscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_minor_nononzeroevaluationdeterminanthscm_positive) = S ((S ((ff_row_mdm_cell_mdr_minor_nononzeroevaluationdeterminanthscm_positive_cell) * (S (mdr_q_minor_nononzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_minor_nononzeroevaluationdeterminanthscm_positive_cell))) * mdr_pc_minor_nononzeroevaluationdeterminanth)) /\ exists ff_q_mdm_mdr_minor_nononzeroevaluationdeterminanthscm_positive_cell_source. mdr_pb_minor_nononzeroevaluationdeterminanth = ff_q_mdm_mdr_minor_nononzeroevaluationdeterminanthscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_minor_nononzeroevaluationdeterminanthscm_positive_cell) * (S (mdr_q_minor_nononzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_minor_nononzeroevaluationdeterminanthscm_positive_cell))) * mdr_pc_minor_nononzeroevaluationdeterminanth) + (ff_value_mdm_prefix_mdr_minor_nononzeroevaluationdeterminanthscm_positive)))))) /\ (((exists ff_h_mdm_mdr_minor_nononzeroevaluationdeterminanthscm_positive_target. ff_h_mdm_mdr_minor_nononzeroevaluationdeterminanthscm_positive_target + S (ff_value_mdm_prefix_mdr_minor_nononzeroevaluationdeterminanthscm_positive) = S ((S (ff_index_mdm_prefix_mdr_minor_nononzeroevaluationdeterminanthscm_positive)) * mdr_us_minor_nononzeroevaluationdeterminanthsc)) /\ exists ff_q_mdm_mdr_minor_nononzeroevaluationdeterminanthscm_positive_target. mdr_up_minor_nononzeroevaluationdeterminanthsc = ff_q_mdm_mdr_minor_nononzeroevaluationdeterminanthscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_minor_nononzeroevaluationdeterminanthscm_positive)) * mdr_us_minor_nononzeroevaluationdeterminanthsc) + (ff_value_mdm_prefix_mdr_minor_nononzeroevaluationdeterminanthscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_minor_nononzeroevaluationdeterminanthscm_negative. (exists ff_gap_mdm_lt_mdr_minor_nononzeroevaluationdeterminanthscm_negative_index_bound. ff_gap_mdm_lt_mdr_minor_nononzeroevaluationdeterminanthscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_minor_nononzeroevaluationdeterminanthscm_negative) = ((mdr_q_minor_nononzeroevaluationdeterminanths) * (mdr_q_minor_nononzeroevaluationdeterminanths))) -> exists ff_row_mdm_prefix_mdr_minor_nononzeroevaluationdeterminanthscm_negative ff_column_mdm_prefix_mdr_minor_nononzeroevaluationdeterminanthscm_negative ff_value_mdm_prefix_mdr_minor_nononzeroevaluationdeterminanthscm_negative. (ff_index_mdm_prefix_mdr_minor_nononzeroevaluationdeterminanthscm_negative = (mdr_q_minor_nononzeroevaluationdeterminanths) * ff_row_mdm_prefix_mdr_minor_nononzeroevaluationdeterminanthscm_negative + ff_column_mdm_prefix_mdr_minor_nononzeroevaluationdeterminanthscm_negative /\ ((exists ff_gap_mdm_lt_mdr_minor_nononzeroevaluationdeterminanthscm_negative_column_bound. ff_gap_mdm_lt_mdr_minor_nononzeroevaluationdeterminanthscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_minor_nononzeroevaluationdeterminanthscm_negative) = (mdr_q_minor_nononzeroevaluationdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_minor_nononzeroevaluationdeterminanthscm_negative_cell ff_column_mdm_cell_mdr_minor_nononzeroevaluationdeterminanthscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_minor_nononzeroevaluationdeterminanthscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_minor_nononzeroevaluationdeterminanthscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_minor_nononzeroevaluationdeterminanthscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_minor_nononzeroevaluationdeterminanthscm_negative_cell = ff_row_mdm_prefix_mdr_minor_nononzeroevaluationdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_minor_nononzeroevaluationdeterminanthscm_negative_cell_row_after. ff_gap_mdm_le_mdr_minor_nononzeroevaluationdeterminanthscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_minor_nononzeroevaluationdeterminanthscm_negative)) /\ ff_row_mdm_cell_mdr_minor_nononzeroevaluationdeterminanthscm_negative_cell = S ff_row_mdm_prefix_mdr_minor_nononzeroevaluationdeterminanthscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_minor_nononzeroevaluationdeterminanthscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_minor_nononzeroevaluationdeterminanthscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_minor_nononzeroevaluationdeterminanthscm_negative) = (mdr_j_minor_nononzeroevaluationdeterminanthsc)) /\ ff_column_mdm_cell_mdr_minor_nononzeroevaluationdeterminanthscm_negative_cell = ff_column_mdm_prefix_mdr_minor_nononzeroevaluationdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_minor_nononzeroevaluationdeterminanthscm_negative_cell_column_after. ff_gap_mdm_le_mdr_minor_nononzeroevaluationdeterminanthscm_negative_cell_column_after + (mdr_j_minor_nononzeroevaluationdeterminanthsc) = (ff_column_mdm_prefix_mdr_minor_nononzeroevaluationdeterminanthscm_negative)) /\ ff_column_mdm_cell_mdr_minor_nononzeroevaluationdeterminanthscm_negative_cell = S ff_column_mdm_prefix_mdr_minor_nononzeroevaluationdeterminanthscm_negative))) /\ (((exists ff_h_mdm_mdr_minor_nononzeroevaluationdeterminanthscm_negative_cell_source. ff_h_mdm_mdr_minor_nononzeroevaluationdeterminanthscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_minor_nononzeroevaluationdeterminanthscm_negative) = S ((S ((ff_row_mdm_cell_mdr_minor_nononzeroevaluationdeterminanthscm_negative_cell) * (S (mdr_q_minor_nononzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_minor_nononzeroevaluationdeterminanthscm_negative_cell))) * mdr_nc_minor_nononzeroevaluationdeterminanth)) /\ exists ff_q_mdm_mdr_minor_nononzeroevaluationdeterminanthscm_negative_cell_source. mdr_nb_minor_nononzeroevaluationdeterminanth = ff_q_mdm_mdr_minor_nononzeroevaluationdeterminanthscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_minor_nononzeroevaluationdeterminanthscm_negative_cell) * (S (mdr_q_minor_nononzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_minor_nononzeroevaluationdeterminanthscm_negative_cell))) * mdr_nc_minor_nononzeroevaluationdeterminanth) + (ff_value_mdm_prefix_mdr_minor_nononzeroevaluationdeterminanthscm_negative)))))) /\ (((exists ff_h_mdm_mdr_minor_nononzeroevaluationdeterminanthscm_negative_target. ff_h_mdm_mdr_minor_nononzeroevaluationdeterminanthscm_negative_target + S (ff_value_mdm_prefix_mdr_minor_nononzeroevaluationdeterminanthscm_negative) = S ((S (ff_index_mdm_prefix_mdr_minor_nononzeroevaluationdeterminanthscm_negative)) * mdr_ut_minor_nononzeroevaluationdeterminanthsc)) /\ exists ff_q_mdm_mdr_minor_nononzeroevaluationdeterminanthscm_negative_target. mdr_un_minor_nononzeroevaluationdeterminanthsc = ff_q_mdm_mdr_minor_nononzeroevaluationdeterminanthscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_minor_nononzeroevaluationdeterminanthscm_negative)) * mdr_ut_minor_nononzeroevaluationdeterminanthsc) + (ff_value_mdm_prefix_mdr_minor_nononzeroevaluationdeterminanthscm_negative))))))))) /\ ((((exists ff_h_mdr_minor_nononzeroevaluationdeterminanthscp. ff_h_mdr_minor_nononzeroevaluationdeterminanthscp + S (mdr_p_minor_nononzeroevaluationdeterminanthsc) = S ((S (mdr_j_minor_nononzeroevaluationdeterminanthsc)) * mdr_ec_minor_nononzeroevaluationdeterminanths)) /\ exists ff_q_mdr_minor_nononzeroevaluationdeterminanthscp. mdr_eb_minor_nononzeroevaluationdeterminanths = ff_q_mdr_minor_nononzeroevaluationdeterminanthscp * S ((S (mdr_j_minor_nononzeroevaluationdeterminanthsc)) * mdr_ec_minor_nononzeroevaluationdeterminanths) + (mdr_p_minor_nononzeroevaluationdeterminanthsc))) /\ (((exists ff_h_mdr_minor_nononzeroevaluationdeterminanthscn. ff_h_mdr_minor_nononzeroevaluationdeterminanthscn + S (mdr_n_minor_nononzeroevaluationdeterminanthsc) = S ((S (mdr_j_minor_nononzeroevaluationdeterminanthsc)) * mdr_fc_minor_nononzeroevaluationdeterminanths)) /\ exists ff_q_mdr_minor_nononzeroevaluationdeterminanthscn. mdr_fb_minor_nononzeroevaluationdeterminanths = ff_q_mdr_minor_nononzeroevaluationdeterminanthscn * S ((S (mdr_j_minor_nononzeroevaluationdeterminanthsc)) * mdr_fc_minor_nononzeroevaluationdeterminanths) + (mdr_n_minor_nononzeroevaluationdeterminanthsc)))))))) /\ (exists ff_ub_mce_fold_mdr_minor_nononzeroevaluationdeterminanthsf ff_uc_mce_fold_mdr_minor_nononzeroevaluationdeterminanthsf ff_vb_mce_fold_mdr_minor_nononzeroevaluationdeterminanthsf ff_vc_mce_fold_mdr_minor_nononzeroevaluationdeterminanthsf. ((forall ff_index_mce_alternating_mdr_minor_nononzeroevaluationdeterminanthsf_prefix. (exists ff_gap_mce_mdr_minor_nononzeroevaluationdeterminanthsf_prefix_index. ff_gap_mce_mdr_minor_nononzeroevaluationdeterminanthsf_prefix_index + S (ff_index_mce_alternating_mdr_minor_nononzeroevaluationdeterminanthsf_prefix) = (S (mdr_q_minor_nononzeroevaluationdeterminanths))) -> exists ff_ap_mce_alternating_mdr_minor_nononzeroevaluationdeterminanthsf_prefix ff_an_mce_alternating_mdr_minor_nononzeroevaluationdeterminanthsf_prefix ff_bp_mce_alternating_mdr_minor_nononzeroevaluationdeterminanthsf_prefix ff_bn_mce_alternating_mdr_minor_nononzeroevaluationdeterminanthsf_prefix ff_p_mce_alternating_mdr_minor_nononzeroevaluationdeterminanthsf_prefix ff_n_mce_alternating_mdr_minor_nononzeroevaluationdeterminanthsf_prefix. ((((exists ff_h_mce_mdr_minor_nononzeroevaluationdeterminanthsf_prefix_ap. ff_h_mce_mdr_minor_nononzeroevaluationdeterminanthsf_prefix_ap + S (ff_ap_mce_alternating_mdr_minor_nononzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_minor_nononzeroevaluationdeterminanthsf_prefix)) * mdr_pc_minor_nononzeroevaluationdeterminanth)) /\ exists ff_q_mce_mdr_minor_nononzeroevaluationdeterminanthsf_prefix_ap. mdr_pb_minor_nononzeroevaluationdeterminanth = ff_q_mce_mdr_minor_nononzeroevaluationdeterminanthsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_minor_nononzeroevaluationdeterminanthsf_prefix)) * mdr_pc_minor_nononzeroevaluationdeterminanth) + (ff_ap_mce_alternating_mdr_minor_nononzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_minor_nononzeroevaluationdeterminanthsf_prefix_an. ff_h_mce_mdr_minor_nononzeroevaluationdeterminanthsf_prefix_an + S (ff_an_mce_alternating_mdr_minor_nononzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_minor_nononzeroevaluationdeterminanthsf_prefix)) * mdr_nc_minor_nononzeroevaluationdeterminanth)) /\ exists ff_q_mce_mdr_minor_nononzeroevaluationdeterminanthsf_prefix_an. mdr_nb_minor_nononzeroevaluationdeterminanth = ff_q_mce_mdr_minor_nononzeroevaluationdeterminanthsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_minor_nononzeroevaluationdeterminanthsf_prefix)) * mdr_nc_minor_nononzeroevaluationdeterminanth) + (ff_an_mce_alternating_mdr_minor_nononzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_minor_nononzeroevaluationdeterminanthsf_prefix_bp. ff_h_mce_mdr_minor_nononzeroevaluationdeterminanthsf_prefix_bp + S (ff_bp_mce_alternating_mdr_minor_nononzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_minor_nononzeroevaluationdeterminanthsf_prefix)) * mdr_ec_minor_nononzeroevaluationdeterminanths)) /\ exists ff_q_mce_mdr_minor_nononzeroevaluationdeterminanthsf_prefix_bp. mdr_eb_minor_nononzeroevaluationdeterminanths = ff_q_mce_mdr_minor_nononzeroevaluationdeterminanthsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_minor_nononzeroevaluationdeterminanthsf_prefix)) * mdr_ec_minor_nononzeroevaluationdeterminanths) + (ff_bp_mce_alternating_mdr_minor_nononzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_minor_nononzeroevaluationdeterminanthsf_prefix_bn. ff_h_mce_mdr_minor_nononzeroevaluationdeterminanthsf_prefix_bn + S (ff_bn_mce_alternating_mdr_minor_nononzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_minor_nononzeroevaluationdeterminanthsf_prefix)) * mdr_fc_minor_nononzeroevaluationdeterminanths)) /\ exists ff_q_mce_mdr_minor_nononzeroevaluationdeterminanthsf_prefix_bn. mdr_fb_minor_nononzeroevaluationdeterminanths = ff_q_mce_mdr_minor_nononzeroevaluationdeterminanthsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_minor_nononzeroevaluationdeterminanthsf_prefix)) * mdr_fc_minor_nononzeroevaluationdeterminanths) + (ff_bn_mce_alternating_mdr_minor_nononzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_minor_nononzeroevaluationdeterminanthsf_prefix_positive. ff_h_mce_mdr_minor_nononzeroevaluationdeterminanthsf_prefix_positive + S (ff_p_mce_alternating_mdr_minor_nononzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_minor_nononzeroevaluationdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_minor_nononzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_minor_nononzeroevaluationdeterminanthsf_prefix_positive. ff_ub_mce_fold_mdr_minor_nononzeroevaluationdeterminanthsf = ff_q_mce_mdr_minor_nononzeroevaluationdeterminanthsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_minor_nononzeroevaluationdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_minor_nononzeroevaluationdeterminanthsf) + (ff_p_mce_alternating_mdr_minor_nononzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_minor_nononzeroevaluationdeterminanthsf_prefix_negative. ff_h_mce_mdr_minor_nononzeroevaluationdeterminanthsf_prefix_negative + S (ff_n_mce_alternating_mdr_minor_nononzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_minor_nononzeroevaluationdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_minor_nononzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_minor_nononzeroevaluationdeterminanthsf_prefix_negative. ff_vb_mce_fold_mdr_minor_nononzeroevaluationdeterminanthsf = ff_q_mce_mdr_minor_nononzeroevaluationdeterminanthsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_minor_nononzeroevaluationdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_minor_nononzeroevaluationdeterminanthsf) + (ff_n_mce_alternating_mdr_minor_nononzeroevaluationdeterminanthsf_prefix))) /\ (((exists ff_even_mce_term_mdr_minor_nononzeroevaluationdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_minor_nononzeroevaluationdeterminanthsf_prefix = 2 * ff_even_mce_term_mdr_minor_nononzeroevaluationdeterminanthsf_prefix_term) /\ (ff_p_mce_alternating_mdr_minor_nononzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_minor_nononzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_minor_nononzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_minor_nononzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_minor_nononzeroevaluationdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_minor_nononzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_minor_nononzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_minor_nononzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_minor_nononzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_minor_nononzeroevaluationdeterminanthsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_minor_nononzeroevaluationdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_minor_nononzeroevaluationdeterminanthsf_prefix = 2 * ff_odd_mce_term_mdr_minor_nononzeroevaluationdeterminanthsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_minor_nononzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_minor_nononzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_minor_nononzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_minor_nononzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_minor_nononzeroevaluationdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_minor_nononzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_minor_nononzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_minor_nononzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_minor_nononzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_minor_nononzeroevaluationdeterminanthsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_minor_nononzeroevaluationdeterminanthsf_positive ff_v_mce_mdr_minor_nononzeroevaluationdeterminanthsf_positive. ((((exists ff_h_mce_mdr_minor_nononzeroevaluationdeterminanthsf_positive_start. ff_h_mce_mdr_minor_nononzeroevaluationdeterminanthsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_minor_nononzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_minor_nononzeroevaluationdeterminanthsf_positive_start. ff_u_mce_mdr_minor_nononzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_minor_nononzeroevaluationdeterminanthsf_positive_start * S ((S (0)) * ff_v_mce_mdr_minor_nononzeroevaluationdeterminanthsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_minor_nononzeroevaluationdeterminanthsf_positive_terminal. ff_h_mce_mdr_minor_nononzeroevaluationdeterminanthsf_positive_terminal + S (mdr_p_minor_nononzeroevaluationdeterminanth) = S ((S ((S (mdr_q_minor_nononzeroevaluationdeterminanths)))) * ff_v_mce_mdr_minor_nononzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_minor_nononzeroevaluationdeterminanthsf_positive_terminal. ff_u_mce_mdr_minor_nononzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_minor_nononzeroevaluationdeterminanthsf_positive_terminal * S ((S ((S (mdr_q_minor_nononzeroevaluationdeterminanths)))) * ff_v_mce_mdr_minor_nononzeroevaluationdeterminanthsf_positive) + (mdr_p_minor_nononzeroevaluationdeterminanth))) /\ forall ff_i_mce_mdr_minor_nononzeroevaluationdeterminanthsf_positive. (exists ff_lt_mce_mdr_minor_nononzeroevaluationdeterminanthsf_positive_bound. ff_lt_mce_mdr_minor_nononzeroevaluationdeterminanthsf_positive_bound + S ff_i_mce_mdr_minor_nononzeroevaluationdeterminanthsf_positive = (S (mdr_q_minor_nononzeroevaluationdeterminanths))) -> exists ff_a_mce_mdr_minor_nononzeroevaluationdeterminanthsf_positive ff_r_mce_mdr_minor_nononzeroevaluationdeterminanthsf_positive ff_s_mce_mdr_minor_nononzeroevaluationdeterminanthsf_positive. ((((exists ff_h_mce_mdr_minor_nononzeroevaluationdeterminanthsf_positive_summand. ff_h_mce_mdr_minor_nononzeroevaluationdeterminanthsf_positive_summand + S (ff_a_mce_mdr_minor_nononzeroevaluationdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_minor_nononzeroevaluationdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_minor_nononzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_minor_nononzeroevaluationdeterminanthsf_positive_summand. ff_ub_mce_fold_mdr_minor_nononzeroevaluationdeterminanthsf = ff_q_mce_mdr_minor_nononzeroevaluationdeterminanthsf_positive_summand * S ((S (ff_i_mce_mdr_minor_nononzeroevaluationdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_minor_nononzeroevaluationdeterminanthsf) + (ff_a_mce_mdr_minor_nononzeroevaluationdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_minor_nononzeroevaluationdeterminanthsf_positive_partial. ff_h_mce_mdr_minor_nononzeroevaluationdeterminanthsf_positive_partial + S (ff_r_mce_mdr_minor_nononzeroevaluationdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_minor_nononzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_minor_nononzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_minor_nononzeroevaluationdeterminanthsf_positive_partial. ff_u_mce_mdr_minor_nononzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_minor_nononzeroevaluationdeterminanthsf_positive_partial * S ((S (ff_i_mce_mdr_minor_nononzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_minor_nononzeroevaluationdeterminanthsf_positive) + (ff_r_mce_mdr_minor_nononzeroevaluationdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_minor_nononzeroevaluationdeterminanthsf_positive_successor. ff_h_mce_mdr_minor_nononzeroevaluationdeterminanthsf_positive_successor + S (ff_s_mce_mdr_minor_nononzeroevaluationdeterminanthsf_positive) = S ((S (S ff_i_mce_mdr_minor_nononzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_minor_nononzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_minor_nononzeroevaluationdeterminanthsf_positive_successor. ff_u_mce_mdr_minor_nononzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_minor_nononzeroevaluationdeterminanthsf_positive_successor * S ((S (S ff_i_mce_mdr_minor_nononzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_minor_nononzeroevaluationdeterminanthsf_positive) + (ff_s_mce_mdr_minor_nononzeroevaluationdeterminanthsf_positive))) /\ ff_s_mce_mdr_minor_nononzeroevaluationdeterminanthsf_positive = ff_r_mce_mdr_minor_nononzeroevaluationdeterminanthsf_positive + ff_a_mce_mdr_minor_nononzeroevaluationdeterminanthsf_positive)))))) /\ (exists ff_u_mce_mdr_minor_nononzeroevaluationdeterminanthsf_negative ff_v_mce_mdr_minor_nononzeroevaluationdeterminanthsf_negative. ((((exists ff_h_mce_mdr_minor_nononzeroevaluationdeterminanthsf_negative_start. ff_h_mce_mdr_minor_nononzeroevaluationdeterminanthsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_minor_nononzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_minor_nononzeroevaluationdeterminanthsf_negative_start. ff_u_mce_mdr_minor_nononzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_minor_nononzeroevaluationdeterminanthsf_negative_start * S ((S (0)) * ff_v_mce_mdr_minor_nononzeroevaluationdeterminanthsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_minor_nononzeroevaluationdeterminanthsf_negative_terminal. ff_h_mce_mdr_minor_nononzeroevaluationdeterminanthsf_negative_terminal + S (mdr_n_minor_nononzeroevaluationdeterminanth) = S ((S ((S (mdr_q_minor_nononzeroevaluationdeterminanths)))) * ff_v_mce_mdr_minor_nononzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_minor_nononzeroevaluationdeterminanthsf_negative_terminal. ff_u_mce_mdr_minor_nononzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_minor_nononzeroevaluationdeterminanthsf_negative_terminal * S ((S ((S (mdr_q_minor_nononzeroevaluationdeterminanths)))) * ff_v_mce_mdr_minor_nononzeroevaluationdeterminanthsf_negative) + (mdr_n_minor_nononzeroevaluationdeterminanth))) /\ forall ff_i_mce_mdr_minor_nononzeroevaluationdeterminanthsf_negative. (exists ff_lt_mce_mdr_minor_nononzeroevaluationdeterminanthsf_negative_bound. ff_lt_mce_mdr_minor_nononzeroevaluationdeterminanthsf_negative_bound + S ff_i_mce_mdr_minor_nononzeroevaluationdeterminanthsf_negative = (S (mdr_q_minor_nononzeroevaluationdeterminanths))) -> exists ff_a_mce_mdr_minor_nononzeroevaluationdeterminanthsf_negative ff_r_mce_mdr_minor_nononzeroevaluationdeterminanthsf_negative ff_s_mce_mdr_minor_nononzeroevaluationdeterminanthsf_negative. ((((exists ff_h_mce_mdr_minor_nononzeroevaluationdeterminanthsf_negative_summand. ff_h_mce_mdr_minor_nononzeroevaluationdeterminanthsf_negative_summand + S (ff_a_mce_mdr_minor_nononzeroevaluationdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_minor_nononzeroevaluationdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_minor_nononzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_minor_nononzeroevaluationdeterminanthsf_negative_summand. ff_vb_mce_fold_mdr_minor_nononzeroevaluationdeterminanthsf = ff_q_mce_mdr_minor_nononzeroevaluationdeterminanthsf_negative_summand * S ((S (ff_i_mce_mdr_minor_nononzeroevaluationdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_minor_nononzeroevaluationdeterminanthsf) + (ff_a_mce_mdr_minor_nononzeroevaluationdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_minor_nononzeroevaluationdeterminanthsf_negative_partial. ff_h_mce_mdr_minor_nononzeroevaluationdeterminanthsf_negative_partial + S (ff_r_mce_mdr_minor_nononzeroevaluationdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_minor_nononzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_minor_nononzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_minor_nononzeroevaluationdeterminanthsf_negative_partial. ff_u_mce_mdr_minor_nononzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_minor_nononzeroevaluationdeterminanthsf_negative_partial * S ((S (ff_i_mce_mdr_minor_nononzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_minor_nononzeroevaluationdeterminanthsf_negative) + (ff_r_mce_mdr_minor_nononzeroevaluationdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_minor_nononzeroevaluationdeterminanthsf_negative_successor. ff_h_mce_mdr_minor_nononzeroevaluationdeterminanthsf_negative_successor + S (ff_s_mce_mdr_minor_nononzeroevaluationdeterminanthsf_negative) = S ((S (S ff_i_mce_mdr_minor_nononzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_minor_nononzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_minor_nononzeroevaluationdeterminanthsf_negative_successor. ff_u_mce_mdr_minor_nononzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_minor_nononzeroevaluationdeterminanthsf_negative_successor * S ((S (S ff_i_mce_mdr_minor_nononzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_minor_nononzeroevaluationdeterminanthsf_negative) + (ff_s_mce_mdr_minor_nononzeroevaluationdeterminanthsf_negative))) /\ ff_s_mce_mdr_minor_nononzeroevaluationdeterminanthsf_negative = ff_r_mce_mdr_minor_nononzeroevaluationdeterminanthsf_negative + ff_a_mce_mdr_minor_nononzeroevaluationdeterminanthsf_negative))))))))))))))) /\ ((exists mdr_gap_minor_nononzeroevaluationdeterminanti. mdr_gap_minor_nononzeroevaluationdeterminanti + S (mdr_i_minor_nononzeroevaluationdeterminant) = (mdr_l_minor_nononzeroevaluationdeterminant)) /\ (exists mdr_z_minor_nononzeroevaluationdeterminantr. ((exists mdr_a_minor_nononzeroevaluationdeterminantrc mdr_b_minor_nononzeroevaluationdeterminantrc mdr_c_minor_nononzeroevaluationdeterminantrc mdr_e_minor_nononzeroevaluationdeterminantrc mdr_f_minor_nononzeroevaluationdeterminantrc. ((mdr_a_minor_nononzeroevaluationdeterminantrc = ((q) + (mdr_ub_minor_nononzeroevaluation)) * S ((q) + (mdr_ub_minor_nononzeroevaluation)) + ((mdr_ub_minor_nononzeroevaluation) + (mdr_ub_minor_nononzeroevaluation))) /\ ((mdr_b_minor_nononzeroevaluationdeterminantrc = ((mdr_uc_minor_nononzeroevaluation) + (mdr_vb_minor_nononzeroevaluation)) * S ((mdr_uc_minor_nononzeroevaluation) + (mdr_vb_minor_nononzeroevaluation)) + ((mdr_vb_minor_nononzeroevaluation) + (mdr_vb_minor_nononzeroevaluation))) /\ ((mdr_c_minor_nononzeroevaluationdeterminantrc = ((mdr_a_minor_nononzeroevaluationdeterminantrc) + (mdr_b_minor_nononzeroevaluationdeterminantrc)) * S ((mdr_a_minor_nononzeroevaluationdeterminantrc) + (mdr_b_minor_nononzeroevaluationdeterminantrc)) + ((mdr_b_minor_nononzeroevaluationdeterminantrc) + (mdr_b_minor_nononzeroevaluationdeterminantrc))) /\ ((mdr_e_minor_nononzeroevaluationdeterminantrc = ((mdr_p_minor_nononzero) + (mdr_n_minor_nononzero)) * S ((mdr_p_minor_nononzero) + (mdr_n_minor_nononzero)) + ((mdr_n_minor_nononzero) + (mdr_n_minor_nononzero))) /\ ((mdr_f_minor_nononzeroevaluationdeterminantrc = ((mdr_vc_minor_nononzeroevaluation) + (mdr_e_minor_nononzeroevaluationdeterminantrc)) * S ((mdr_vc_minor_nononzeroevaluation) + (mdr_e_minor_nononzeroevaluationdeterminantrc)) + ((mdr_e_minor_nononzeroevaluationdeterminantrc) + (mdr_e_minor_nononzeroevaluationdeterminantrc))) /\ ((mdr_z_minor_nononzeroevaluationdeterminantr) = ((mdr_c_minor_nononzeroevaluationdeterminantrc) + (mdr_f_minor_nononzeroevaluationdeterminantrc)) * S ((mdr_c_minor_nononzeroevaluationdeterminantrc) + (mdr_f_minor_nononzeroevaluationdeterminantrc)) + ((mdr_f_minor_nononzeroevaluationdeterminantrc) + (mdr_f_minor_nononzeroevaluationdeterminantrc))))))))) /\ (((exists ff_h_mdr_minor_nononzeroevaluationdeterminantrb. ff_h_mdr_minor_nononzeroevaluationdeterminantrb + S (mdr_z_minor_nononzeroevaluationdeterminantr) = S ((S (mdr_i_minor_nononzeroevaluationdeterminant)) * mdr_c_minor_nononzeroevaluationdeterminant)) /\ exists ff_q_mdr_minor_nononzeroevaluationdeterminantrb. mdr_b_minor_nononzeroevaluationdeterminant = ff_q_mdr_minor_nononzeroevaluationdeterminantrb * S ((S (mdr_i_minor_nononzeroevaluationdeterminant)) * mdr_c_minor_nononzeroevaluationdeterminant) + (mdr_z_minor_nononzeroevaluationdeterminantr)))))))))) /\ (~(mdr_p_minor_nononzero = mdr_n_minor_nononzero)))))))