Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.
Exact expanded first-order arithmetic statement
forall pb pc nb nc r w rank. (((exists mdr_gap_successor_rankrows_bound. mdr_gap_successor_rankrows_bound + (rank) = (r)) /\ ((exists mdr_gap_successor_rankcolumns_bound. mdr_gap_successor_rankcolumns_bound + (rank) = (w)) /\ ((exists mdr_rb_successor_rankwitness mdr_rc_successor_rankwitness mdr_cb_successor_rankwitness mdr_cc_successor_rankwitness. (((((forall fom_index_mrf_successor_rankwitnessminorrowsbound. (exists fom_gap_mrf_successor_rankwitnessminorrowsbound_index_bound. fom_gap_mrf_successor_rankwitnessminorrowsbound_index_bound + S (fom_index_mrf_successor_rankwitnessminorrowsbound) = rank) -> exists fom_value_mrf_successor_rankwitnessminorrowsbound. ((((exists fom_beta_height_mrf_successor_rankwitnessminorrowsbound_entry. fom_beta_height_mrf_successor_rankwitnessminorrowsbound_entry + S (fom_value_mrf_successor_rankwitnessminorrowsbound) = S ((S (fom_index_mrf_successor_rankwitnessminorrowsbound)) * mdr_rc_successor_rankwitness)) /\ exists fom_beta_quotient_mrf_successor_rankwitnessminorrowsbound_entry. mdr_rb_successor_rankwitness = fom_beta_quotient_mrf_successor_rankwitnessminorrowsbound_entry * S ((S (fom_index_mrf_successor_rankwitnessminorrowsbound)) * mdr_rc_successor_rankwitness) + (fom_value_mrf_successor_rankwitnessminorrowsbound))) /\ (exists fom_gap_mrf_successor_rankwitnessminorrowsbound_value_bound. fom_gap_mrf_successor_rankwitnessminorrowsbound_value_bound + S (fom_value_mrf_successor_rankwitnessminorrowsbound) = r))) /\ (forall mdr_i_successor_rankwitnessminorrowsdistinct mdr_j_successor_rankwitnessminorrowsdistinct mdr_a_successor_rankwitnessminorrowsdistinct. (exists mdr_gap_successor_rankwitnessminorrowsdistincti. mdr_gap_successor_rankwitnessminorrowsdistincti + S (mdr_i_successor_rankwitnessminorrowsdistinct) = (rank)) -> (exists mdr_gap_successor_rankwitnessminorrowsdistinctj. mdr_gap_successor_rankwitnessminorrowsdistinctj + S (mdr_j_successor_rankwitnessminorrowsdistinct) = (rank)) -> (((exists ff_h_mdr_successor_rankwitnessminorrowsdistinctfirst. ff_h_mdr_successor_rankwitnessminorrowsdistinctfirst + S (mdr_a_successor_rankwitnessminorrowsdistinct) = S ((S (mdr_i_successor_rankwitnessminorrowsdistinct)) * mdr_rc_successor_rankwitness)) /\ exists ff_q_mdr_successor_rankwitnessminorrowsdistinctfirst. mdr_rb_successor_rankwitness = ff_q_mdr_successor_rankwitnessminorrowsdistinctfirst * S ((S (mdr_i_successor_rankwitnessminorrowsdistinct)) * mdr_rc_successor_rankwitness) + (mdr_a_successor_rankwitnessminorrowsdistinct))) -> (((exists ff_h_mdr_successor_rankwitnessminorrowsdistinctsecond. ff_h_mdr_successor_rankwitnessminorrowsdistinctsecond + S (mdr_a_successor_rankwitnessminorrowsdistinct) = S ((S (mdr_j_successor_rankwitnessminorrowsdistinct)) * mdr_rc_successor_rankwitness)) /\ exists ff_q_mdr_successor_rankwitnessminorrowsdistinctsecond. mdr_rb_successor_rankwitness = ff_q_mdr_successor_rankwitnessminorrowsdistinctsecond * S ((S (mdr_j_successor_rankwitnessminorrowsdistinct)) * mdr_rc_successor_rankwitness) + (mdr_a_successor_rankwitnessminorrowsdistinct))) -> mdr_i_successor_rankwitnessminorrowsdistinct = mdr_j_successor_rankwitnessminorrowsdistinct))) /\ ((((forall fom_index_mrf_successor_rankwitnessminorcolumnsbound. (exists fom_gap_mrf_successor_rankwitnessminorcolumnsbound_index_bound. fom_gap_mrf_successor_rankwitnessminorcolumnsbound_index_bound + S (fom_index_mrf_successor_rankwitnessminorcolumnsbound) = rank) -> exists fom_value_mrf_successor_rankwitnessminorcolumnsbound. ((((exists fom_beta_height_mrf_successor_rankwitnessminorcolumnsbound_entry. fom_beta_height_mrf_successor_rankwitnessminorcolumnsbound_entry + S (fom_value_mrf_successor_rankwitnessminorcolumnsbound) = S ((S (fom_index_mrf_successor_rankwitnessminorcolumnsbound)) * mdr_cc_successor_rankwitness)) /\ exists fom_beta_quotient_mrf_successor_rankwitnessminorcolumnsbound_entry. mdr_cb_successor_rankwitness = fom_beta_quotient_mrf_successor_rankwitnessminorcolumnsbound_entry * S ((S (fom_index_mrf_successor_rankwitnessminorcolumnsbound)) * mdr_cc_successor_rankwitness) + (fom_value_mrf_successor_rankwitnessminorcolumnsbound))) /\ (exists fom_gap_mrf_successor_rankwitnessminorcolumnsbound_value_bound. fom_gap_mrf_successor_rankwitnessminorcolumnsbound_value_bound + S (fom_value_mrf_successor_rankwitnessminorcolumnsbound) = w))) /\ (forall mdr_i_successor_rankwitnessminorcolumnsdistinct mdr_j_successor_rankwitnessminorcolumnsdistinct mdr_a_successor_rankwitnessminorcolumnsdistinct. (exists mdr_gap_successor_rankwitnessminorcolumnsdistincti. mdr_gap_successor_rankwitnessminorcolumnsdistincti + S (mdr_i_successor_rankwitnessminorcolumnsdistinct) = (rank)) -> (exists mdr_gap_successor_rankwitnessminorcolumnsdistinctj. mdr_gap_successor_rankwitnessminorcolumnsdistinctj + S (mdr_j_successor_rankwitnessminorcolumnsdistinct) = (rank)) -> (((exists ff_h_mdr_successor_rankwitnessminorcolumnsdistinctfirst. ff_h_mdr_successor_rankwitnessminorcolumnsdistinctfirst + S (mdr_a_successor_rankwitnessminorcolumnsdistinct) = S ((S (mdr_i_successor_rankwitnessminorcolumnsdistinct)) * mdr_cc_successor_rankwitness)) /\ exists ff_q_mdr_successor_rankwitnessminorcolumnsdistinctfirst. mdr_cb_successor_rankwitness = ff_q_mdr_successor_rankwitnessminorcolumnsdistinctfirst * S ((S (mdr_i_successor_rankwitnessminorcolumnsdistinct)) * mdr_cc_successor_rankwitness) + (mdr_a_successor_rankwitnessminorcolumnsdistinct))) -> (((exists ff_h_mdr_successor_rankwitnessminorcolumnsdistinctsecond. ff_h_mdr_successor_rankwitnessminorcolumnsdistinctsecond + S (mdr_a_successor_rankwitnessminorcolumnsdistinct) = S ((S (mdr_j_successor_rankwitnessminorcolumnsdistinct)) * mdr_cc_successor_rankwitness)) /\ exists ff_q_mdr_successor_rankwitnessminorcolumnsdistinctsecond. mdr_cb_successor_rankwitness = ff_q_mdr_successor_rankwitnessminorcolumnsdistinctsecond * S ((S (mdr_j_successor_rankwitnessminorcolumnsdistinct)) * mdr_cc_successor_rankwitness) + (mdr_a_successor_rankwitnessminorcolumnsdistinct))) -> mdr_i_successor_rankwitnessminorcolumnsdistinct = mdr_j_successor_rankwitnessminorcolumnsdistinct))) /\ (exists mdr_p_successor_rankwitnessminornonzero mdr_n_successor_rankwitnessminornonzero. ((exists mdr_ub_successor_rankwitnessminornonzeroevaluation mdr_uc_successor_rankwitnessminornonzeroevaluation mdr_vb_successor_rankwitnessminornonzeroevaluation mdr_vc_successor_rankwitnessminornonzeroevaluation. ((((forall mdr_i_successor_rankwitnessminornonzeroevaluationmatrixpositive. (exists mdr_gap_successor_rankwitnessminornonzeroevaluationmatrixpositivebound. mdr_gap_successor_rankwitnessminornonzeroevaluationmatrixpositivebound + S (mdr_i_successor_rankwitnessminornonzeroevaluationmatrixpositive) = ((rank) * (rank))) -> exists mdr_a_successor_rankwitnessminornonzeroevaluationmatrixpositive. (((exists mdr_r_successor_rankwitnessminornonzeroevaluationmatrixpositivepoint mdr_s_successor_rankwitnessminornonzeroevaluationmatrixpositivepoint mdr_u_successor_rankwitnessminornonzeroevaluationmatrixpositivepoint mdr_v_successor_rankwitnessminornonzeroevaluationmatrixpositivepoint. ((mdr_i_successor_rankwitnessminornonzeroevaluationmatrixpositive = (rank) * mdr_r_successor_rankwitnessminornonzeroevaluationmatrixpositivepoint + mdr_s_successor_rankwitnessminornonzeroevaluationmatrixpositivepoint) /\ ((exists mdr_gap_successor_rankwitnessminornonzeroevaluationmatrixpositivepointcolumn. mdr_gap_successor_rankwitnessminornonzeroevaluationmatrixpositivepointcolumn + S (mdr_s_successor_rankwitnessminornonzeroevaluationmatrixpositivepoint) = (rank)) /\ ((((exists ff_h_mdr_successor_rankwitnessminornonzeroevaluationmatrixpositivepointrow_index. ff_h_mdr_successor_rankwitnessminornonzeroevaluationmatrixpositivepointrow_index + S (mdr_u_successor_rankwitnessminornonzeroevaluationmatrixpositivepoint) = S ((S (mdr_r_successor_rankwitnessminornonzeroevaluationmatrixpositivepoint)) * mdr_rc_successor_rankwitness)) /\ exists ff_q_mdr_successor_rankwitnessminornonzeroevaluationmatrixpositivepointrow_index. mdr_rb_successor_rankwitness = ff_q_mdr_successor_rankwitnessminornonzeroevaluationmatrixpositivepointrow_index * S ((S (mdr_r_successor_rankwitnessminornonzeroevaluationmatrixpositivepoint)) * mdr_rc_successor_rankwitness) + (mdr_u_successor_rankwitnessminornonzeroevaluationmatrixpositivepoint))) /\ ((((exists ff_h_mdr_successor_rankwitnessminornonzeroevaluationmatrixpositivepointcolumn_index. ff_h_mdr_successor_rankwitnessminornonzeroevaluationmatrixpositivepointcolumn_index + S (mdr_v_successor_rankwitnessminornonzeroevaluationmatrixpositivepoint) = S ((S (mdr_s_successor_rankwitnessminornonzeroevaluationmatrixpositivepoint)) * mdr_cc_successor_rankwitness)) /\ exists ff_q_mdr_successor_rankwitnessminornonzeroevaluationmatrixpositivepointcolumn_index. mdr_cb_successor_rankwitness = ff_q_mdr_successor_rankwitnessminornonzeroevaluationmatrixpositivepointcolumn_index * S ((S (mdr_s_successor_rankwitnessminornonzeroevaluationmatrixpositivepoint)) * mdr_cc_successor_rankwitness) + (mdr_v_successor_rankwitnessminornonzeroevaluationmatrixpositivepoint))) /\ (((exists ff_h_mdr_successor_rankwitnessminornonzeroevaluationmatrixpositivepointsource. ff_h_mdr_successor_rankwitnessminornonzeroevaluationmatrixpositivepointsource + S (mdr_a_successor_rankwitnessminornonzeroevaluationmatrixpositive) = S ((S ((mdr_u_successor_rankwitnessminornonzeroevaluationmatrixpositivepoint) * (w) + (mdr_v_successor_rankwitnessminornonzeroevaluationmatrixpositivepoint))) * pc)) /\ exists ff_q_mdr_successor_rankwitnessminornonzeroevaluationmatrixpositivepointsource. pb = ff_q_mdr_successor_rankwitnessminornonzeroevaluationmatrixpositivepointsource * S ((S ((mdr_u_successor_rankwitnessminornonzeroevaluationmatrixpositivepoint) * (w) + (mdr_v_successor_rankwitnessminornonzeroevaluationmatrixpositivepoint))) * pc) + (mdr_a_successor_rankwitnessminornonzeroevaluationmatrixpositive)))))))) /\ (((exists ff_h_mdr_successor_rankwitnessminornonzeroevaluationmatrixpositiveoutput. ff_h_mdr_successor_rankwitnessminornonzeroevaluationmatrixpositiveoutput + S (mdr_a_successor_rankwitnessminornonzeroevaluationmatrixpositive) = S ((S (mdr_i_successor_rankwitnessminornonzeroevaluationmatrixpositive)) * mdr_uc_successor_rankwitnessminornonzeroevaluation)) /\ exists ff_q_mdr_successor_rankwitnessminornonzeroevaluationmatrixpositiveoutput. mdr_ub_successor_rankwitnessminornonzeroevaluation = ff_q_mdr_successor_rankwitnessminornonzeroevaluationmatrixpositiveoutput * S ((S (mdr_i_successor_rankwitnessminornonzeroevaluationmatrixpositive)) * mdr_uc_successor_rankwitnessminornonzeroevaluation) + (mdr_a_successor_rankwitnessminornonzeroevaluationmatrixpositive)))))) /\ (forall mdr_i_successor_rankwitnessminornonzeroevaluationmatrixnegative. (exists mdr_gap_successor_rankwitnessminornonzeroevaluationmatrixnegativebound. mdr_gap_successor_rankwitnessminornonzeroevaluationmatrixnegativebound + S (mdr_i_successor_rankwitnessminornonzeroevaluationmatrixnegative) = ((rank) * (rank))) -> exists mdr_a_successor_rankwitnessminornonzeroevaluationmatrixnegative. (((exists mdr_r_successor_rankwitnessminornonzeroevaluationmatrixnegativepoint mdr_s_successor_rankwitnessminornonzeroevaluationmatrixnegativepoint mdr_u_successor_rankwitnessminornonzeroevaluationmatrixnegativepoint mdr_v_successor_rankwitnessminornonzeroevaluationmatrixnegativepoint. ((mdr_i_successor_rankwitnessminornonzeroevaluationmatrixnegative = (rank) * mdr_r_successor_rankwitnessminornonzeroevaluationmatrixnegativepoint + mdr_s_successor_rankwitnessminornonzeroevaluationmatrixnegativepoint) /\ ((exists mdr_gap_successor_rankwitnessminornonzeroevaluationmatrixnegativepointcolumn. mdr_gap_successor_rankwitnessminornonzeroevaluationmatrixnegativepointcolumn + S (mdr_s_successor_rankwitnessminornonzeroevaluationmatrixnegativepoint) = (rank)) /\ ((((exists ff_h_mdr_successor_rankwitnessminornonzeroevaluationmatrixnegativepointrow_index. ff_h_mdr_successor_rankwitnessminornonzeroevaluationmatrixnegativepointrow_index + S (mdr_u_successor_rankwitnessminornonzeroevaluationmatrixnegativepoint) = S ((S (mdr_r_successor_rankwitnessminornonzeroevaluationmatrixnegativepoint)) * mdr_rc_successor_rankwitness)) /\ exists ff_q_mdr_successor_rankwitnessminornonzeroevaluationmatrixnegativepointrow_index. mdr_rb_successor_rankwitness = ff_q_mdr_successor_rankwitnessminornonzeroevaluationmatrixnegativepointrow_index * S ((S (mdr_r_successor_rankwitnessminornonzeroevaluationmatrixnegativepoint)) * mdr_rc_successor_rankwitness) + (mdr_u_successor_rankwitnessminornonzeroevaluationmatrixnegativepoint))) /\ ((((exists ff_h_mdr_successor_rankwitnessminornonzeroevaluationmatrixnegativepointcolumn_index. ff_h_mdr_successor_rankwitnessminornonzeroevaluationmatrixnegativepointcolumn_index + S (mdr_v_successor_rankwitnessminornonzeroevaluationmatrixnegativepoint) = S ((S (mdr_s_successor_rankwitnessminornonzeroevaluationmatrixnegativepoint)) * mdr_cc_successor_rankwitness)) /\ exists ff_q_mdr_successor_rankwitnessminornonzeroevaluationmatrixnegativepointcolumn_index. mdr_cb_successor_rankwitness = ff_q_mdr_successor_rankwitnessminornonzeroevaluationmatrixnegativepointcolumn_index * S ((S (mdr_s_successor_rankwitnessminornonzeroevaluationmatrixnegativepoint)) * mdr_cc_successor_rankwitness) + (mdr_v_successor_rankwitnessminornonzeroevaluationmatrixnegativepoint))) /\ (((exists ff_h_mdr_successor_rankwitnessminornonzeroevaluationmatrixnegativepointsource. ff_h_mdr_successor_rankwitnessminornonzeroevaluationmatrixnegativepointsource + S (mdr_a_successor_rankwitnessminornonzeroevaluationmatrixnegative) = S ((S ((mdr_u_successor_rankwitnessminornonzeroevaluationmatrixnegativepoint) * (w) + (mdr_v_successor_rankwitnessminornonzeroevaluationmatrixnegativepoint))) * nc)) /\ exists ff_q_mdr_successor_rankwitnessminornonzeroevaluationmatrixnegativepointsource. nb = ff_q_mdr_successor_rankwitnessminornonzeroevaluationmatrixnegativepointsource * S ((S ((mdr_u_successor_rankwitnessminornonzeroevaluationmatrixnegativepoint) * (w) + (mdr_v_successor_rankwitnessminornonzeroevaluationmatrixnegativepoint))) * nc) + (mdr_a_successor_rankwitnessminornonzeroevaluationmatrixnegative)))))))) /\ (((exists ff_h_mdr_successor_rankwitnessminornonzeroevaluationmatrixnegativeoutput. ff_h_mdr_successor_rankwitnessminornonzeroevaluationmatrixnegativeoutput + S (mdr_a_successor_rankwitnessminornonzeroevaluationmatrixnegative) = S ((S (mdr_i_successor_rankwitnessminornonzeroevaluationmatrixnegative)) * mdr_vc_successor_rankwitnessminornonzeroevaluation)) /\ exists ff_q_mdr_successor_rankwitnessminornonzeroevaluationmatrixnegativeoutput. mdr_vb_successor_rankwitnessminornonzeroevaluation = ff_q_mdr_successor_rankwitnessminornonzeroevaluationmatrixnegativeoutput * S ((S (mdr_i_successor_rankwitnessminornonzeroevaluationmatrixnegative)) * mdr_vc_successor_rankwitnessminornonzeroevaluation) + (mdr_a_successor_rankwitnessminornonzeroevaluationmatrixnegative)))))))) /\ (exists mdr_b_successor_rankwitnessminornonzeroevaluationdeterminant mdr_c_successor_rankwitnessminornonzeroevaluationdeterminant mdr_l_successor_rankwitnessminornonzeroevaluationdeterminant mdr_i_successor_rankwitnessminornonzeroevaluationdeterminant. ((forall mdr_i_successor_rankwitnessminornonzeroevaluationdeterminanth. (exists mdr_gap_successor_rankwitnessminornonzeroevaluationdeterminanthi. mdr_gap_successor_rankwitnessminornonzeroevaluationdeterminanthi + S (mdr_i_successor_rankwitnessminornonzeroevaluationdeterminanth) = (mdr_l_successor_rankwitnessminornonzeroevaluationdeterminant)) -> exists mdr_d_successor_rankwitnessminornonzeroevaluationdeterminanth mdr_pb_successor_rankwitnessminornonzeroevaluationdeterminanth mdr_pc_successor_rankwitnessminornonzeroevaluationdeterminanth mdr_nb_successor_rankwitnessminornonzeroevaluationdeterminanth mdr_nc_successor_rankwitnessminornonzeroevaluationdeterminanth mdr_p_successor_rankwitnessminornonzeroevaluationdeterminanth mdr_n_successor_rankwitnessminornonzeroevaluationdeterminanth. ((exists mdr_z_successor_rankwitnessminornonzeroevaluationdeterminanthr. ((exists mdr_a_successor_rankwitnessminornonzeroevaluationdeterminanthrc mdr_b_successor_rankwitnessminornonzeroevaluationdeterminanthrc mdr_c_successor_rankwitnessminornonzeroevaluationdeterminanthrc mdr_e_successor_rankwitnessminornonzeroevaluationdeterminanthrc mdr_f_successor_rankwitnessminornonzeroevaluationdeterminanthrc. ((mdr_a_successor_rankwitnessminornonzeroevaluationdeterminanthrc = ((mdr_d_successor_rankwitnessminornonzeroevaluationdeterminanth) + (mdr_pb_successor_rankwitnessminornonzeroevaluationdeterminanth)) * S ((mdr_d_successor_rankwitnessminornonzeroevaluationdeterminanth) + (mdr_pb_successor_rankwitnessminornonzeroevaluationdeterminanth)) + ((mdr_pb_successor_rankwitnessminornonzeroevaluationdeterminanth) + (mdr_pb_successor_rankwitnessminornonzeroevaluationdeterminanth))) /\ ((mdr_b_successor_rankwitnessminornonzeroevaluationdeterminanthrc = ((mdr_pc_successor_rankwitnessminornonzeroevaluationdeterminanth) + (mdr_nb_successor_rankwitnessminornonzeroevaluationdeterminanth)) * S ((mdr_pc_successor_rankwitnessminornonzeroevaluationdeterminanth) + (mdr_nb_successor_rankwitnessminornonzeroevaluationdeterminanth)) + ((mdr_nb_successor_rankwitnessminornonzeroevaluationdeterminanth) + (mdr_nb_successor_rankwitnessminornonzeroevaluationdeterminanth))) /\ ((mdr_c_successor_rankwitnessminornonzeroevaluationdeterminanthrc = ((mdr_a_successor_rankwitnessminornonzeroevaluationdeterminanthrc) + (mdr_b_successor_rankwitnessminornonzeroevaluationdeterminanthrc)) * S ((mdr_a_successor_rankwitnessminornonzeroevaluationdeterminanthrc) + (mdr_b_successor_rankwitnessminornonzeroevaluationdeterminanthrc)) + ((mdr_b_successor_rankwitnessminornonzeroevaluationdeterminanthrc) + (mdr_b_successor_rankwitnessminornonzeroevaluationdeterminanthrc))) /\ ((mdr_e_successor_rankwitnessminornonzeroevaluationdeterminanthrc = ((mdr_p_successor_rankwitnessminornonzeroevaluationdeterminanth) + (mdr_n_successor_rankwitnessminornonzeroevaluationdeterminanth)) * S ((mdr_p_successor_rankwitnessminornonzeroevaluationdeterminanth) + (mdr_n_successor_rankwitnessminornonzeroevaluationdeterminanth)) + ((mdr_n_successor_rankwitnessminornonzeroevaluationdeterminanth) + (mdr_n_successor_rankwitnessminornonzeroevaluationdeterminanth))) /\ ((mdr_f_successor_rankwitnessminornonzeroevaluationdeterminanthrc = ((mdr_nc_successor_rankwitnessminornonzeroevaluationdeterminanth) + (mdr_e_successor_rankwitnessminornonzeroevaluationdeterminanthrc)) * S ((mdr_nc_successor_rankwitnessminornonzeroevaluationdeterminanth) + (mdr_e_successor_rankwitnessminornonzeroevaluationdeterminanthrc)) + ((mdr_e_successor_rankwitnessminornonzeroevaluationdeterminanthrc) + (mdr_e_successor_rankwitnessminornonzeroevaluationdeterminanthrc))) /\ ((mdr_z_successor_rankwitnessminornonzeroevaluationdeterminanthr) = ((mdr_c_successor_rankwitnessminornonzeroevaluationdeterminanthrc) + (mdr_f_successor_rankwitnessminornonzeroevaluationdeterminanthrc)) * S ((mdr_c_successor_rankwitnessminornonzeroevaluationdeterminanthrc) + (mdr_f_successor_rankwitnessminornonzeroevaluationdeterminanthrc)) + ((mdr_f_successor_rankwitnessminornonzeroevaluationdeterminanthrc) + (mdr_f_successor_rankwitnessminornonzeroevaluationdeterminanthrc))))))))) /\ (((exists ff_h_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthrb. ff_h_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthrb + S (mdr_z_successor_rankwitnessminornonzeroevaluationdeterminanthr) = S ((S (mdr_i_successor_rankwitnessminornonzeroevaluationdeterminanth)) * mdr_c_successor_rankwitnessminornonzeroevaluationdeterminant)) /\ exists ff_q_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthrb. mdr_b_successor_rankwitnessminornonzeroevaluationdeterminant = ff_q_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthrb * S ((S (mdr_i_successor_rankwitnessminornonzeroevaluationdeterminanth)) * mdr_c_successor_rankwitnessminornonzeroevaluationdeterminant) + (mdr_z_successor_rankwitnessminornonzeroevaluationdeterminanthr))))) /\ (((((mdr_d_successor_rankwitnessminornonzeroevaluationdeterminanth) = 0) /\ (((mdr_p_successor_rankwitnessminornonzeroevaluationdeterminanth) = 1) /\ ((mdr_n_successor_rankwitnessminornonzeroevaluationdeterminanth) = 0))) \/ exists mdr_q_successor_rankwitnessminornonzeroevaluationdeterminanths mdr_eb_successor_rankwitnessminornonzeroevaluationdeterminanths mdr_ec_successor_rankwitnessminornonzeroevaluationdeterminanths mdr_fb_successor_rankwitnessminornonzeroevaluationdeterminanths mdr_fc_successor_rankwitnessminornonzeroevaluationdeterminanths. (((mdr_d_successor_rankwitnessminornonzeroevaluationdeterminanth) = S (mdr_q_successor_rankwitnessminornonzeroevaluationdeterminanths)) /\ ((forall mdr_j_successor_rankwitnessminornonzeroevaluationdeterminanthsc. (exists mdr_gap_successor_rankwitnessminornonzeroevaluationdeterminanthscj. mdr_gap_successor_rankwitnessminornonzeroevaluationdeterminanthscj + S (mdr_j_successor_rankwitnessminornonzeroevaluationdeterminanthsc) = (S (mdr_q_successor_rankwitnessminornonzeroevaluationdeterminanths))) -> exists mdr_i_successor_rankwitnessminornonzeroevaluationdeterminanthsc mdr_up_successor_rankwitnessminornonzeroevaluationdeterminanthsc mdr_us_successor_rankwitnessminornonzeroevaluationdeterminanthsc mdr_un_successor_rankwitnessminornonzeroevaluationdeterminanthsc mdr_ut_successor_rankwitnessminornonzeroevaluationdeterminanthsc mdr_p_successor_rankwitnessminornonzeroevaluationdeterminanthsc mdr_n_successor_rankwitnessminornonzeroevaluationdeterminanthsc. ((exists mdr_gap_successor_rankwitnessminornonzeroevaluationdeterminanthsci. mdr_gap_successor_rankwitnessminornonzeroevaluationdeterminanthsci + S (mdr_i_successor_rankwitnessminornonzeroevaluationdeterminanthsc) = (mdr_i_successor_rankwitnessminornonzeroevaluationdeterminanth)) /\ ((exists mdr_z_successor_rankwitnessminornonzeroevaluationdeterminanthscr. ((exists mdr_a_successor_rankwitnessminornonzeroevaluationdeterminanthscrc mdr_b_successor_rankwitnessminornonzeroevaluationdeterminanthscrc mdr_c_successor_rankwitnessminornonzeroevaluationdeterminanthscrc mdr_e_successor_rankwitnessminornonzeroevaluationdeterminanthscrc mdr_f_successor_rankwitnessminornonzeroevaluationdeterminanthscrc. ((mdr_a_successor_rankwitnessminornonzeroevaluationdeterminanthscrc = ((mdr_q_successor_rankwitnessminornonzeroevaluationdeterminanths) + (mdr_up_successor_rankwitnessminornonzeroevaluationdeterminanthsc)) * S ((mdr_q_successor_rankwitnessminornonzeroevaluationdeterminanths) + (mdr_up_successor_rankwitnessminornonzeroevaluationdeterminanthsc)) + ((mdr_up_successor_rankwitnessminornonzeroevaluationdeterminanthsc) + (mdr_up_successor_rankwitnessminornonzeroevaluationdeterminanthsc))) /\ ((mdr_b_successor_rankwitnessminornonzeroevaluationdeterminanthscrc = ((mdr_us_successor_rankwitnessminornonzeroevaluationdeterminanthsc) + (mdr_un_successor_rankwitnessminornonzeroevaluationdeterminanthsc)) * S ((mdr_us_successor_rankwitnessminornonzeroevaluationdeterminanthsc) + (mdr_un_successor_rankwitnessminornonzeroevaluationdeterminanthsc)) + ((mdr_un_successor_rankwitnessminornonzeroevaluationdeterminanthsc) + (mdr_un_successor_rankwitnessminornonzeroevaluationdeterminanthsc))) /\ ((mdr_c_successor_rankwitnessminornonzeroevaluationdeterminanthscrc = ((mdr_a_successor_rankwitnessminornonzeroevaluationdeterminanthscrc) + (mdr_b_successor_rankwitnessminornonzeroevaluationdeterminanthscrc)) * S ((mdr_a_successor_rankwitnessminornonzeroevaluationdeterminanthscrc) + (mdr_b_successor_rankwitnessminornonzeroevaluationdeterminanthscrc)) + ((mdr_b_successor_rankwitnessminornonzeroevaluationdeterminanthscrc) + (mdr_b_successor_rankwitnessminornonzeroevaluationdeterminanthscrc))) /\ ((mdr_e_successor_rankwitnessminornonzeroevaluationdeterminanthscrc = ((mdr_p_successor_rankwitnessminornonzeroevaluationdeterminanthsc) + (mdr_n_successor_rankwitnessminornonzeroevaluationdeterminanthsc)) * S ((mdr_p_successor_rankwitnessminornonzeroevaluationdeterminanthsc) + (mdr_n_successor_rankwitnessminornonzeroevaluationdeterminanthsc)) + ((mdr_n_successor_rankwitnessminornonzeroevaluationdeterminanthsc) + (mdr_n_successor_rankwitnessminornonzeroevaluationdeterminanthsc))) /\ ((mdr_f_successor_rankwitnessminornonzeroevaluationdeterminanthscrc = ((mdr_ut_successor_rankwitnessminornonzeroevaluationdeterminanthsc) + (mdr_e_successor_rankwitnessminornonzeroevaluationdeterminanthscrc)) * S ((mdr_ut_successor_rankwitnessminornonzeroevaluationdeterminanthsc) + (mdr_e_successor_rankwitnessminornonzeroevaluationdeterminanthscrc)) + ((mdr_e_successor_rankwitnessminornonzeroevaluationdeterminanthscrc) + (mdr_e_successor_rankwitnessminornonzeroevaluationdeterminanthscrc))) /\ ((mdr_z_successor_rankwitnessminornonzeroevaluationdeterminanthscr) = ((mdr_c_successor_rankwitnessminornonzeroevaluationdeterminanthscrc) + (mdr_f_successor_rankwitnessminornonzeroevaluationdeterminanthscrc)) * S ((mdr_c_successor_rankwitnessminornonzeroevaluationdeterminanthscrc) + (mdr_f_successor_rankwitnessminornonzeroevaluationdeterminanthscrc)) + ((mdr_f_successor_rankwitnessminornonzeroevaluationdeterminanthscrc) + (mdr_f_successor_rankwitnessminornonzeroevaluationdeterminanthscrc))))))))) /\ (((exists ff_h_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthscrb. ff_h_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthscrb + S (mdr_z_successor_rankwitnessminornonzeroevaluationdeterminanthscr) = S ((S (mdr_i_successor_rankwitnessminornonzeroevaluationdeterminanthsc)) * mdr_c_successor_rankwitnessminornonzeroevaluationdeterminant)) /\ exists ff_q_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthscrb. mdr_b_successor_rankwitnessminornonzeroevaluationdeterminant = ff_q_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthscrb * S ((S (mdr_i_successor_rankwitnessminornonzeroevaluationdeterminanthsc)) * mdr_c_successor_rankwitnessminornonzeroevaluationdeterminant) + (mdr_z_successor_rankwitnessminornonzeroevaluationdeterminanthscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthscm_positive. (exists ff_gap_mdm_lt_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthscm_positive_index_bound. ff_gap_mdm_lt_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthscm_positive) = ((mdr_q_successor_rankwitnessminornonzeroevaluationdeterminanths) * (mdr_q_successor_rankwitnessminornonzeroevaluationdeterminanths))) -> exists ff_row_mdm_prefix_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthscm_positive ff_column_mdm_prefix_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthscm_positive ff_value_mdm_prefix_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthscm_positive. (ff_index_mdm_prefix_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthscm_positive = (mdr_q_successor_rankwitnessminornonzeroevaluationdeterminanths) * ff_row_mdm_prefix_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthscm_positive + ff_column_mdm_prefix_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthscm_positive /\ ((exists ff_gap_mdm_lt_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthscm_positive_column_bound. ff_gap_mdm_lt_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthscm_positive) = (mdr_q_successor_rankwitnessminornonzeroevaluationdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell ff_column_mdm_cell_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell = ff_row_mdm_prefix_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell_row_after. ff_gap_mdm_le_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthscm_positive)) /\ ff_row_mdm_cell_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell = S ff_row_mdm_prefix_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthscm_positive) = (mdr_j_successor_rankwitnessminornonzeroevaluationdeterminanthsc)) /\ ff_column_mdm_cell_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell = ff_column_mdm_prefix_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell_column_after. ff_gap_mdm_le_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell_column_after + (mdr_j_successor_rankwitnessminornonzeroevaluationdeterminanthsc) = (ff_column_mdm_prefix_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthscm_positive)) /\ ff_column_mdm_cell_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell = S ff_column_mdm_prefix_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthscm_positive))) /\ (((exists ff_h_mdm_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell_source. ff_h_mdm_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthscm_positive) = S ((S ((ff_row_mdm_cell_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell) * (S (mdr_q_successor_rankwitnessminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell))) * mdr_pc_successor_rankwitnessminornonzeroevaluationdeterminanth)) /\ exists ff_q_mdm_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell_source. mdr_pb_successor_rankwitnessminornonzeroevaluationdeterminanth = ff_q_mdm_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell) * (S (mdr_q_successor_rankwitnessminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell))) * mdr_pc_successor_rankwitnessminornonzeroevaluationdeterminanth) + (ff_value_mdm_prefix_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthscm_positive)))))) /\ (((exists ff_h_mdm_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthscm_positive_target. ff_h_mdm_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthscm_positive_target + S (ff_value_mdm_prefix_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthscm_positive) = S ((S (ff_index_mdm_prefix_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthscm_positive)) * mdr_us_successor_rankwitnessminornonzeroevaluationdeterminanthsc)) /\ exists ff_q_mdm_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthscm_positive_target. mdr_up_successor_rankwitnessminornonzeroevaluationdeterminanthsc = ff_q_mdm_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthscm_positive)) * mdr_us_successor_rankwitnessminornonzeroevaluationdeterminanthsc) + (ff_value_mdm_prefix_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthscm_negative. (exists ff_gap_mdm_lt_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthscm_negative_index_bound. ff_gap_mdm_lt_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthscm_negative) = ((mdr_q_successor_rankwitnessminornonzeroevaluationdeterminanths) * (mdr_q_successor_rankwitnessminornonzeroevaluationdeterminanths))) -> exists ff_row_mdm_prefix_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthscm_negative ff_column_mdm_prefix_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthscm_negative ff_value_mdm_prefix_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthscm_negative. (ff_index_mdm_prefix_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthscm_negative = (mdr_q_successor_rankwitnessminornonzeroevaluationdeterminanths) * ff_row_mdm_prefix_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthscm_negative + ff_column_mdm_prefix_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthscm_negative /\ ((exists ff_gap_mdm_lt_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthscm_negative_column_bound. ff_gap_mdm_lt_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthscm_negative) = (mdr_q_successor_rankwitnessminornonzeroevaluationdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell ff_column_mdm_cell_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell = ff_row_mdm_prefix_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell_row_after. ff_gap_mdm_le_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthscm_negative)) /\ ff_row_mdm_cell_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell = S ff_row_mdm_prefix_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthscm_negative) = (mdr_j_successor_rankwitnessminornonzeroevaluationdeterminanthsc)) /\ ff_column_mdm_cell_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell = ff_column_mdm_prefix_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell_column_after. ff_gap_mdm_le_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell_column_after + (mdr_j_successor_rankwitnessminornonzeroevaluationdeterminanthsc) = (ff_column_mdm_prefix_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthscm_negative)) /\ ff_column_mdm_cell_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell = S ff_column_mdm_prefix_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthscm_negative))) /\ (((exists ff_h_mdm_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell_source. ff_h_mdm_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthscm_negative) = S ((S ((ff_row_mdm_cell_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell) * (S (mdr_q_successor_rankwitnessminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell))) * mdr_nc_successor_rankwitnessminornonzeroevaluationdeterminanth)) /\ exists ff_q_mdm_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell_source. mdr_nb_successor_rankwitnessminornonzeroevaluationdeterminanth = ff_q_mdm_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell) * (S (mdr_q_successor_rankwitnessminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell))) * mdr_nc_successor_rankwitnessminornonzeroevaluationdeterminanth) + (ff_value_mdm_prefix_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthscm_negative)))))) /\ (((exists ff_h_mdm_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthscm_negative_target. ff_h_mdm_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthscm_negative_target + S (ff_value_mdm_prefix_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthscm_negative) = S ((S (ff_index_mdm_prefix_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthscm_negative)) * mdr_ut_successor_rankwitnessminornonzeroevaluationdeterminanthsc)) /\ exists ff_q_mdm_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthscm_negative_target. mdr_un_successor_rankwitnessminornonzeroevaluationdeterminanthsc = ff_q_mdm_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthscm_negative)) * mdr_ut_successor_rankwitnessminornonzeroevaluationdeterminanthsc) + (ff_value_mdm_prefix_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthscm_negative))))))))) /\ ((((exists ff_h_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthscp. ff_h_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthscp + S (mdr_p_successor_rankwitnessminornonzeroevaluationdeterminanthsc) = S ((S (mdr_j_successor_rankwitnessminornonzeroevaluationdeterminanthsc)) * mdr_ec_successor_rankwitnessminornonzeroevaluationdeterminanths)) /\ exists ff_q_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthscp. mdr_eb_successor_rankwitnessminornonzeroevaluationdeterminanths = ff_q_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthscp * S ((S (mdr_j_successor_rankwitnessminornonzeroevaluationdeterminanthsc)) * mdr_ec_successor_rankwitnessminornonzeroevaluationdeterminanths) + (mdr_p_successor_rankwitnessminornonzeroevaluationdeterminanthsc))) /\ (((exists ff_h_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthscn. ff_h_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthscn + S (mdr_n_successor_rankwitnessminornonzeroevaluationdeterminanthsc) = S ((S (mdr_j_successor_rankwitnessminornonzeroevaluationdeterminanthsc)) * mdr_fc_successor_rankwitnessminornonzeroevaluationdeterminanths)) /\ exists ff_q_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthscn. mdr_fb_successor_rankwitnessminornonzeroevaluationdeterminanths = ff_q_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthscn * S ((S (mdr_j_successor_rankwitnessminornonzeroevaluationdeterminanthsc)) * mdr_fc_successor_rankwitnessminornonzeroevaluationdeterminanths) + (mdr_n_successor_rankwitnessminornonzeroevaluationdeterminanthsc)))))))) /\ (exists ff_ub_mce_fold_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf ff_uc_mce_fold_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf ff_vb_mce_fold_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf ff_vc_mce_fold_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf. ((forall ff_index_mce_alternating_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_prefix. (exists ff_gap_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_index. ff_gap_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_index + S (ff_index_mce_alternating_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) = (S (mdr_q_successor_rankwitnessminornonzeroevaluationdeterminanths))) -> exists ff_ap_mce_alternating_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_prefix ff_an_mce_alternating_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_prefix ff_bp_mce_alternating_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_prefix ff_bn_mce_alternating_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_prefix ff_p_mce_alternating_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_prefix ff_n_mce_alternating_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_prefix. ((((exists ff_h_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_ap. ff_h_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_ap + S (ff_ap_mce_alternating_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_prefix)) * mdr_pc_successor_rankwitnessminornonzeroevaluationdeterminanth)) /\ exists ff_q_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_ap. mdr_pb_successor_rankwitnessminornonzeroevaluationdeterminanth = ff_q_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_prefix)) * mdr_pc_successor_rankwitnessminornonzeroevaluationdeterminanth) + (ff_ap_mce_alternating_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_an. ff_h_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_an + S (ff_an_mce_alternating_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_prefix)) * mdr_nc_successor_rankwitnessminornonzeroevaluationdeterminanth)) /\ exists ff_q_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_an. mdr_nb_successor_rankwitnessminornonzeroevaluationdeterminanth = ff_q_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_prefix)) * mdr_nc_successor_rankwitnessminornonzeroevaluationdeterminanth) + (ff_an_mce_alternating_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_bp. ff_h_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_bp + S (ff_bp_mce_alternating_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_prefix)) * mdr_ec_successor_rankwitnessminornonzeroevaluationdeterminanths)) /\ exists ff_q_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_bp. mdr_eb_successor_rankwitnessminornonzeroevaluationdeterminanths = ff_q_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_prefix)) * mdr_ec_successor_rankwitnessminornonzeroevaluationdeterminanths) + (ff_bp_mce_alternating_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_bn. ff_h_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_bn + S (ff_bn_mce_alternating_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_prefix)) * mdr_fc_successor_rankwitnessminornonzeroevaluationdeterminanths)) /\ exists ff_q_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_bn. mdr_fb_successor_rankwitnessminornonzeroevaluationdeterminanths = ff_q_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_prefix)) * mdr_fc_successor_rankwitnessminornonzeroevaluationdeterminanths) + (ff_bn_mce_alternating_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_positive. ff_h_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_positive + S (ff_p_mce_alternating_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_positive. ff_ub_mce_fold_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf) + (ff_p_mce_alternating_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_negative. ff_h_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_negative + S (ff_n_mce_alternating_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_negative. ff_vb_mce_fold_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf) + (ff_n_mce_alternating_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_prefix))) /\ (((exists ff_even_mce_term_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_prefix = 2 * ff_even_mce_term_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_term) /\ (ff_p_mce_alternating_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_prefix = 2 * ff_odd_mce_term_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_positive ff_v_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_positive. ((((exists ff_h_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_positive_start. ff_h_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_positive_start. ff_u_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_positive_start * S ((S (0)) * ff_v_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_positive_terminal. ff_h_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_positive_terminal + S (mdr_p_successor_rankwitnessminornonzeroevaluationdeterminanth) = S ((S ((S (mdr_q_successor_rankwitnessminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_positive_terminal. ff_u_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_positive_terminal * S ((S ((S (mdr_q_successor_rankwitnessminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_positive) + (mdr_p_successor_rankwitnessminornonzeroevaluationdeterminanth))) /\ forall ff_i_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_positive. (exists ff_lt_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_positive_bound. ff_lt_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_positive_bound + S ff_i_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_positive = (S (mdr_q_successor_rankwitnessminornonzeroevaluationdeterminanths))) -> exists ff_a_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_positive ff_r_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_positive ff_s_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_positive. ((((exists ff_h_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_positive_summand. ff_h_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_positive_summand + S (ff_a_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_positive_summand. ff_ub_mce_fold_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_positive_summand * S ((S (ff_i_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf) + (ff_a_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_positive_partial. ff_h_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_positive_partial + S (ff_r_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_positive_partial. ff_u_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_positive_partial * S ((S (ff_i_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_positive) + (ff_r_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_positive_successor. ff_h_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_positive_successor + S (ff_s_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_positive) = S ((S (S ff_i_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_positive_successor. ff_u_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_positive_successor * S ((S (S ff_i_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_positive) + (ff_s_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_positive))) /\ ff_s_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_positive = ff_r_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_positive + ff_a_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_positive)))))) /\ (exists ff_u_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_negative ff_v_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_negative. ((((exists ff_h_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_negative_start. ff_h_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_negative_start. ff_u_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_negative_start * S ((S (0)) * ff_v_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_negative_terminal. ff_h_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_negative_terminal + S (mdr_n_successor_rankwitnessminornonzeroevaluationdeterminanth) = S ((S ((S (mdr_q_successor_rankwitnessminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_negative_terminal. ff_u_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_negative_terminal * S ((S ((S (mdr_q_successor_rankwitnessminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_negative) + (mdr_n_successor_rankwitnessminornonzeroevaluationdeterminanth))) /\ forall ff_i_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_negative. (exists ff_lt_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_negative_bound. ff_lt_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_negative_bound + S ff_i_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_negative = (S (mdr_q_successor_rankwitnessminornonzeroevaluationdeterminanths))) -> exists ff_a_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_negative ff_r_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_negative ff_s_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_negative. ((((exists ff_h_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_negative_summand. ff_h_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_negative_summand + S (ff_a_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_negative_summand. ff_vb_mce_fold_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_negative_summand * S ((S (ff_i_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf) + (ff_a_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_negative_partial. ff_h_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_negative_partial + S (ff_r_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_negative_partial. ff_u_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_negative_partial * S ((S (ff_i_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_negative) + (ff_r_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_negative_successor. ff_h_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_negative_successor + S (ff_s_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_negative) = S ((S (S ff_i_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_negative_successor. ff_u_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_negative_successor * S ((S (S ff_i_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_negative) + (ff_s_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_negative))) /\ ff_s_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_negative = ff_r_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_negative + ff_a_mce_mdr_successor_rankwitnessminornonzeroevaluationdeterminanthsf_negative))))))))))))))) /\ ((exists mdr_gap_successor_rankwitnessminornonzeroevaluationdeterminanti. mdr_gap_successor_rankwitnessminornonzeroevaluationdeterminanti + S (mdr_i_successor_rankwitnessminornonzeroevaluationdeterminant) = (mdr_l_successor_rankwitnessminornonzeroevaluationdeterminant)) /\ (exists mdr_z_successor_rankwitnessminornonzeroevaluationdeterminantr. ((exists mdr_a_successor_rankwitnessminornonzeroevaluationdeterminantrc mdr_b_successor_rankwitnessminornonzeroevaluationdeterminantrc mdr_c_successor_rankwitnessminornonzeroevaluationdeterminantrc mdr_e_successor_rankwitnessminornonzeroevaluationdeterminantrc mdr_f_successor_rankwitnessminornonzeroevaluationdeterminantrc. ((mdr_a_successor_rankwitnessminornonzeroevaluationdeterminantrc = ((rank) + (mdr_ub_successor_rankwitnessminornonzeroevaluation)) * S ((rank) + (mdr_ub_successor_rankwitnessminornonzeroevaluation)) + ((mdr_ub_successor_rankwitnessminornonzeroevaluation) + (mdr_ub_successor_rankwitnessminornonzeroevaluation))) /\ ((mdr_b_successor_rankwitnessminornonzeroevaluationdeterminantrc = ((mdr_uc_successor_rankwitnessminornonzeroevaluation) + (mdr_vb_successor_rankwitnessminornonzeroevaluation)) * S ((mdr_uc_successor_rankwitnessminornonzeroevaluation) + (mdr_vb_successor_rankwitnessminornonzeroevaluation)) + ((mdr_vb_successor_rankwitnessminornonzeroevaluation) + (mdr_vb_successor_rankwitnessminornonzeroevaluation))) /\ ((mdr_c_successor_rankwitnessminornonzeroevaluationdeterminantrc = ((mdr_a_successor_rankwitnessminornonzeroevaluationdeterminantrc) + (mdr_b_successor_rankwitnessminornonzeroevaluationdeterminantrc)) * S ((mdr_a_successor_rankwitnessminornonzeroevaluationdeterminantrc) + (mdr_b_successor_rankwitnessminornonzeroevaluationdeterminantrc)) + ((mdr_b_successor_rankwitnessminornonzeroevaluationdeterminantrc) + (mdr_b_successor_rankwitnessminornonzeroevaluationdeterminantrc))) /\ ((mdr_e_successor_rankwitnessminornonzeroevaluationdeterminantrc = ((mdr_p_successor_rankwitnessminornonzero) + (mdr_n_successor_rankwitnessminornonzero)) * S ((mdr_p_successor_rankwitnessminornonzero) + (mdr_n_successor_rankwitnessminornonzero)) + ((mdr_n_successor_rankwitnessminornonzero) + (mdr_n_successor_rankwitnessminornonzero))) /\ ((mdr_f_successor_rankwitnessminornonzeroevaluationdeterminantrc = ((mdr_vc_successor_rankwitnessminornonzeroevaluation) + (mdr_e_successor_rankwitnessminornonzeroevaluationdeterminantrc)) * S ((mdr_vc_successor_rankwitnessminornonzeroevaluation) + (mdr_e_successor_rankwitnessminornonzeroevaluationdeterminantrc)) + ((mdr_e_successor_rankwitnessminornonzeroevaluationdeterminantrc) + (mdr_e_successor_rankwitnessminornonzeroevaluationdeterminantrc))) /\ ((mdr_z_successor_rankwitnessminornonzeroevaluationdeterminantr) = ((mdr_c_successor_rankwitnessminornonzeroevaluationdeterminantrc) + (mdr_f_successor_rankwitnessminornonzeroevaluationdeterminantrc)) * S ((mdr_c_successor_rankwitnessminornonzeroevaluationdeterminantrc) + (mdr_f_successor_rankwitnessminornonzeroevaluationdeterminantrc)) + ((mdr_f_successor_rankwitnessminornonzeroevaluationdeterminantrc) + (mdr_f_successor_rankwitnessminornonzeroevaluationdeterminantrc))))))))) /\ (((exists ff_h_mdr_successor_rankwitnessminornonzeroevaluationdeterminantrb. ff_h_mdr_successor_rankwitnessminornonzeroevaluationdeterminantrb + S (mdr_z_successor_rankwitnessminornonzeroevaluationdeterminantr) = S ((S (mdr_i_successor_rankwitnessminornonzeroevaluationdeterminant)) * mdr_c_successor_rankwitnessminornonzeroevaluationdeterminant)) /\ exists ff_q_mdr_successor_rankwitnessminornonzeroevaluationdeterminantrb. mdr_b_successor_rankwitnessminornonzeroevaluationdeterminant = ff_q_mdr_successor_rankwitnessminornonzeroevaluationdeterminantrb * S ((S (mdr_i_successor_rankwitnessminornonzeroevaluationdeterminant)) * mdr_c_successor_rankwitnessminornonzeroevaluationdeterminant) + (mdr_z_successor_rankwitnessminornonzeroevaluationdeterminantr)))))))))) /\ (~(mdr_p_successor_rankwitnessminornonzero = mdr_n_successor_rankwitnessminornonzero)))))))) /\ (forall mdr_q_successor_rank. (exists mdr_gap_successor_rankhigher. mdr_gap_successor_rankhigher + S (rank) = (mdr_q_successor_rank)) -> (forall mdr_rb_successor_rankzero mdr_rc_successor_rankzero mdr_cb_successor_rankzero mdr_cc_successor_rankzero mdr_p_successor_rankzero mdr_n_successor_rankzero. (((forall fom_index_mrf_successor_rankzerorowsbound. (exists fom_gap_mrf_successor_rankzerorowsbound_index_bound. fom_gap_mrf_successor_rankzerorowsbound_index_bound + S (fom_index_mrf_successor_rankzerorowsbound) = mdr_q_successor_rank) -> exists fom_value_mrf_successor_rankzerorowsbound. ((((exists fom_beta_height_mrf_successor_rankzerorowsbound_entry. fom_beta_height_mrf_successor_rankzerorowsbound_entry + S (fom_value_mrf_successor_rankzerorowsbound) = S ((S (fom_index_mrf_successor_rankzerorowsbound)) * mdr_rc_successor_rankzero)) /\ exists fom_beta_quotient_mrf_successor_rankzerorowsbound_entry. mdr_rb_successor_rankzero = fom_beta_quotient_mrf_successor_rankzerorowsbound_entry * S ((S (fom_index_mrf_successor_rankzerorowsbound)) * mdr_rc_successor_rankzero) + (fom_value_mrf_successor_rankzerorowsbound))) /\ (exists fom_gap_mrf_successor_rankzerorowsbound_value_bound. fom_gap_mrf_successor_rankzerorowsbound_value_bound + S (fom_value_mrf_successor_rankzerorowsbound) = r))) /\ (forall mdr_i_successor_rankzerorowsdistinct mdr_j_successor_rankzerorowsdistinct mdr_a_successor_rankzerorowsdistinct. (exists mdr_gap_successor_rankzerorowsdistincti. mdr_gap_successor_rankzerorowsdistincti + S (mdr_i_successor_rankzerorowsdistinct) = (mdr_q_successor_rank)) -> (exists mdr_gap_successor_rankzerorowsdistinctj. mdr_gap_successor_rankzerorowsdistinctj + S (mdr_j_successor_rankzerorowsdistinct) = (mdr_q_successor_rank)) -> (((exists ff_h_mdr_successor_rankzerorowsdistinctfirst. ff_h_mdr_successor_rankzerorowsdistinctfirst + S (mdr_a_successor_rankzerorowsdistinct) = S ((S (mdr_i_successor_rankzerorowsdistinct)) * mdr_rc_successor_rankzero)) /\ exists ff_q_mdr_successor_rankzerorowsdistinctfirst. mdr_rb_successor_rankzero = ff_q_mdr_successor_rankzerorowsdistinctfirst * S ((S (mdr_i_successor_rankzerorowsdistinct)) * mdr_rc_successor_rankzero) + (mdr_a_successor_rankzerorowsdistinct))) -> (((exists ff_h_mdr_successor_rankzerorowsdistinctsecond. ff_h_mdr_successor_rankzerorowsdistinctsecond + S (mdr_a_successor_rankzerorowsdistinct) = S ((S (mdr_j_successor_rankzerorowsdistinct)) * mdr_rc_successor_rankzero)) /\ exists ff_q_mdr_successor_rankzerorowsdistinctsecond. mdr_rb_successor_rankzero = ff_q_mdr_successor_rankzerorowsdistinctsecond * S ((S (mdr_j_successor_rankzerorowsdistinct)) * mdr_rc_successor_rankzero) + (mdr_a_successor_rankzerorowsdistinct))) -> mdr_i_successor_rankzerorowsdistinct = mdr_j_successor_rankzerorowsdistinct))) -> (((forall fom_index_mrf_successor_rankzerocolumnsbound. (exists fom_gap_mrf_successor_rankzerocolumnsbound_index_bound. fom_gap_mrf_successor_rankzerocolumnsbound_index_bound + S (fom_index_mrf_successor_rankzerocolumnsbound) = mdr_q_successor_rank) -> exists fom_value_mrf_successor_rankzerocolumnsbound. ((((exists fom_beta_height_mrf_successor_rankzerocolumnsbound_entry. fom_beta_height_mrf_successor_rankzerocolumnsbound_entry + S (fom_value_mrf_successor_rankzerocolumnsbound) = S ((S (fom_index_mrf_successor_rankzerocolumnsbound)) * mdr_cc_successor_rankzero)) /\ exists fom_beta_quotient_mrf_successor_rankzerocolumnsbound_entry. mdr_cb_successor_rankzero = fom_beta_quotient_mrf_successor_rankzerocolumnsbound_entry * S ((S (fom_index_mrf_successor_rankzerocolumnsbound)) * mdr_cc_successor_rankzero) + (fom_value_mrf_successor_rankzerocolumnsbound))) /\ (exists fom_gap_mrf_successor_rankzerocolumnsbound_value_bound. fom_gap_mrf_successor_rankzerocolumnsbound_value_bound + S (fom_value_mrf_successor_rankzerocolumnsbound) = w))) /\ (forall mdr_i_successor_rankzerocolumnsdistinct mdr_j_successor_rankzerocolumnsdistinct mdr_a_successor_rankzerocolumnsdistinct. (exists mdr_gap_successor_rankzerocolumnsdistincti. mdr_gap_successor_rankzerocolumnsdistincti + S (mdr_i_successor_rankzerocolumnsdistinct) = (mdr_q_successor_rank)) -> (exists mdr_gap_successor_rankzerocolumnsdistinctj. mdr_gap_successor_rankzerocolumnsdistinctj + S (mdr_j_successor_rankzerocolumnsdistinct) = (mdr_q_successor_rank)) -> (((exists ff_h_mdr_successor_rankzerocolumnsdistinctfirst. ff_h_mdr_successor_rankzerocolumnsdistinctfirst + S (mdr_a_successor_rankzerocolumnsdistinct) = S ((S (mdr_i_successor_rankzerocolumnsdistinct)) * mdr_cc_successor_rankzero)) /\ exists ff_q_mdr_successor_rankzerocolumnsdistinctfirst. mdr_cb_successor_rankzero = ff_q_mdr_successor_rankzerocolumnsdistinctfirst * S ((S (mdr_i_successor_rankzerocolumnsdistinct)) * mdr_cc_successor_rankzero) + (mdr_a_successor_rankzerocolumnsdistinct))) -> (((exists ff_h_mdr_successor_rankzerocolumnsdistinctsecond. ff_h_mdr_successor_rankzerocolumnsdistinctsecond + S (mdr_a_successor_rankzerocolumnsdistinct) = S ((S (mdr_j_successor_rankzerocolumnsdistinct)) * mdr_cc_successor_rankzero)) /\ exists ff_q_mdr_successor_rankzerocolumnsdistinctsecond. mdr_cb_successor_rankzero = ff_q_mdr_successor_rankzerocolumnsdistinctsecond * S ((S (mdr_j_successor_rankzerocolumnsdistinct)) * mdr_cc_successor_rankzero) + (mdr_a_successor_rankzerocolumnsdistinct))) -> mdr_i_successor_rankzerocolumnsdistinct = mdr_j_successor_rankzerocolumnsdistinct))) -> (exists mdr_ub_successor_rankzeroevaluation mdr_uc_successor_rankzeroevaluation mdr_vb_successor_rankzeroevaluation mdr_vc_successor_rankzeroevaluation. ((((forall mdr_i_successor_rankzeroevaluationmatrixpositive. (exists mdr_gap_successor_rankzeroevaluationmatrixpositivebound. mdr_gap_successor_rankzeroevaluationmatrixpositivebound + S (mdr_i_successor_rankzeroevaluationmatrixpositive) = ((mdr_q_successor_rank) * (mdr_q_successor_rank))) -> exists mdr_a_successor_rankzeroevaluationmatrixpositive. (((exists mdr_r_successor_rankzeroevaluationmatrixpositivepoint mdr_s_successor_rankzeroevaluationmatrixpositivepoint mdr_u_successor_rankzeroevaluationmatrixpositivepoint mdr_v_successor_rankzeroevaluationmatrixpositivepoint. ((mdr_i_successor_rankzeroevaluationmatrixpositive = (mdr_q_successor_rank) * mdr_r_successor_rankzeroevaluationmatrixpositivepoint + mdr_s_successor_rankzeroevaluationmatrixpositivepoint) /\ ((exists mdr_gap_successor_rankzeroevaluationmatrixpositivepointcolumn. mdr_gap_successor_rankzeroevaluationmatrixpositivepointcolumn + S (mdr_s_successor_rankzeroevaluationmatrixpositivepoint) = (mdr_q_successor_rank)) /\ ((((exists ff_h_mdr_successor_rankzeroevaluationmatrixpositivepointrow_index. ff_h_mdr_successor_rankzeroevaluationmatrixpositivepointrow_index + S (mdr_u_successor_rankzeroevaluationmatrixpositivepoint) = S ((S (mdr_r_successor_rankzeroevaluationmatrixpositivepoint)) * mdr_rc_successor_rankzero)) /\ exists ff_q_mdr_successor_rankzeroevaluationmatrixpositivepointrow_index. mdr_rb_successor_rankzero = ff_q_mdr_successor_rankzeroevaluationmatrixpositivepointrow_index * S ((S (mdr_r_successor_rankzeroevaluationmatrixpositivepoint)) * mdr_rc_successor_rankzero) + (mdr_u_successor_rankzeroevaluationmatrixpositivepoint))) /\ ((((exists ff_h_mdr_successor_rankzeroevaluationmatrixpositivepointcolumn_index. ff_h_mdr_successor_rankzeroevaluationmatrixpositivepointcolumn_index + S (mdr_v_successor_rankzeroevaluationmatrixpositivepoint) = S ((S (mdr_s_successor_rankzeroevaluationmatrixpositivepoint)) * mdr_cc_successor_rankzero)) /\ exists ff_q_mdr_successor_rankzeroevaluationmatrixpositivepointcolumn_index. mdr_cb_successor_rankzero = ff_q_mdr_successor_rankzeroevaluationmatrixpositivepointcolumn_index * S ((S (mdr_s_successor_rankzeroevaluationmatrixpositivepoint)) * mdr_cc_successor_rankzero) + (mdr_v_successor_rankzeroevaluationmatrixpositivepoint))) /\ (((exists ff_h_mdr_successor_rankzeroevaluationmatrixpositivepointsource. ff_h_mdr_successor_rankzeroevaluationmatrixpositivepointsource + S (mdr_a_successor_rankzeroevaluationmatrixpositive) = S ((S ((mdr_u_successor_rankzeroevaluationmatrixpositivepoint) * (w) + (mdr_v_successor_rankzeroevaluationmatrixpositivepoint))) * pc)) /\ exists ff_q_mdr_successor_rankzeroevaluationmatrixpositivepointsource. pb = ff_q_mdr_successor_rankzeroevaluationmatrixpositivepointsource * S ((S ((mdr_u_successor_rankzeroevaluationmatrixpositivepoint) * (w) + (mdr_v_successor_rankzeroevaluationmatrixpositivepoint))) * pc) + (mdr_a_successor_rankzeroevaluationmatrixpositive)))))))) /\ (((exists ff_h_mdr_successor_rankzeroevaluationmatrixpositiveoutput. ff_h_mdr_successor_rankzeroevaluationmatrixpositiveoutput + S (mdr_a_successor_rankzeroevaluationmatrixpositive) = S ((S (mdr_i_successor_rankzeroevaluationmatrixpositive)) * mdr_uc_successor_rankzeroevaluation)) /\ exists ff_q_mdr_successor_rankzeroevaluationmatrixpositiveoutput. mdr_ub_successor_rankzeroevaluation = ff_q_mdr_successor_rankzeroevaluationmatrixpositiveoutput * S ((S (mdr_i_successor_rankzeroevaluationmatrixpositive)) * mdr_uc_successor_rankzeroevaluation) + (mdr_a_successor_rankzeroevaluationmatrixpositive)))))) /\ (forall mdr_i_successor_rankzeroevaluationmatrixnegative. (exists mdr_gap_successor_rankzeroevaluationmatrixnegativebound. mdr_gap_successor_rankzeroevaluationmatrixnegativebound + S (mdr_i_successor_rankzeroevaluationmatrixnegative) = ((mdr_q_successor_rank) * (mdr_q_successor_rank))) -> exists mdr_a_successor_rankzeroevaluationmatrixnegative. (((exists mdr_r_successor_rankzeroevaluationmatrixnegativepoint mdr_s_successor_rankzeroevaluationmatrixnegativepoint mdr_u_successor_rankzeroevaluationmatrixnegativepoint mdr_v_successor_rankzeroevaluationmatrixnegativepoint. ((mdr_i_successor_rankzeroevaluationmatrixnegative = (mdr_q_successor_rank) * mdr_r_successor_rankzeroevaluationmatrixnegativepoint + mdr_s_successor_rankzeroevaluationmatrixnegativepoint) /\ ((exists mdr_gap_successor_rankzeroevaluationmatrixnegativepointcolumn. mdr_gap_successor_rankzeroevaluationmatrixnegativepointcolumn + S (mdr_s_successor_rankzeroevaluationmatrixnegativepoint) = (mdr_q_successor_rank)) /\ ((((exists ff_h_mdr_successor_rankzeroevaluationmatrixnegativepointrow_index. ff_h_mdr_successor_rankzeroevaluationmatrixnegativepointrow_index + S (mdr_u_successor_rankzeroevaluationmatrixnegativepoint) = S ((S (mdr_r_successor_rankzeroevaluationmatrixnegativepoint)) * mdr_rc_successor_rankzero)) /\ exists ff_q_mdr_successor_rankzeroevaluationmatrixnegativepointrow_index. mdr_rb_successor_rankzero = ff_q_mdr_successor_rankzeroevaluationmatrixnegativepointrow_index * S ((S (mdr_r_successor_rankzeroevaluationmatrixnegativepoint)) * mdr_rc_successor_rankzero) + (mdr_u_successor_rankzeroevaluationmatrixnegativepoint))) /\ ((((exists ff_h_mdr_successor_rankzeroevaluationmatrixnegativepointcolumn_index. ff_h_mdr_successor_rankzeroevaluationmatrixnegativepointcolumn_index + S (mdr_v_successor_rankzeroevaluationmatrixnegativepoint) = S ((S (mdr_s_successor_rankzeroevaluationmatrixnegativepoint)) * mdr_cc_successor_rankzero)) /\ exists ff_q_mdr_successor_rankzeroevaluationmatrixnegativepointcolumn_index. mdr_cb_successor_rankzero = ff_q_mdr_successor_rankzeroevaluationmatrixnegativepointcolumn_index * S ((S (mdr_s_successor_rankzeroevaluationmatrixnegativepoint)) * mdr_cc_successor_rankzero) + (mdr_v_successor_rankzeroevaluationmatrixnegativepoint))) /\ (((exists ff_h_mdr_successor_rankzeroevaluationmatrixnegativepointsource. ff_h_mdr_successor_rankzeroevaluationmatrixnegativepointsource + S (mdr_a_successor_rankzeroevaluationmatrixnegative) = S ((S ((mdr_u_successor_rankzeroevaluationmatrixnegativepoint) * (w) + (mdr_v_successor_rankzeroevaluationmatrixnegativepoint))) * nc)) /\ exists ff_q_mdr_successor_rankzeroevaluationmatrixnegativepointsource. nb = ff_q_mdr_successor_rankzeroevaluationmatrixnegativepointsource * S ((S ((mdr_u_successor_rankzeroevaluationmatrixnegativepoint) * (w) + (mdr_v_successor_rankzeroevaluationmatrixnegativepoint))) * nc) + (mdr_a_successor_rankzeroevaluationmatrixnegative)))))))) /\ (((exists ff_h_mdr_successor_rankzeroevaluationmatrixnegativeoutput. ff_h_mdr_successor_rankzeroevaluationmatrixnegativeoutput + S (mdr_a_successor_rankzeroevaluationmatrixnegative) = S ((S (mdr_i_successor_rankzeroevaluationmatrixnegative)) * mdr_vc_successor_rankzeroevaluation)) /\ exists ff_q_mdr_successor_rankzeroevaluationmatrixnegativeoutput. mdr_vb_successor_rankzeroevaluation = ff_q_mdr_successor_rankzeroevaluationmatrixnegativeoutput * S ((S (mdr_i_successor_rankzeroevaluationmatrixnegative)) * mdr_vc_successor_rankzeroevaluation) + (mdr_a_successor_rankzeroevaluationmatrixnegative)))))))) /\ (exists mdr_b_successor_rankzeroevaluationdeterminant mdr_c_successor_rankzeroevaluationdeterminant mdr_l_successor_rankzeroevaluationdeterminant mdr_i_successor_rankzeroevaluationdeterminant. ((forall mdr_i_successor_rankzeroevaluationdeterminanth. (exists mdr_gap_successor_rankzeroevaluationdeterminanthi. mdr_gap_successor_rankzeroevaluationdeterminanthi + S (mdr_i_successor_rankzeroevaluationdeterminanth) = (mdr_l_successor_rankzeroevaluationdeterminant)) -> exists mdr_d_successor_rankzeroevaluationdeterminanth mdr_pb_successor_rankzeroevaluationdeterminanth mdr_pc_successor_rankzeroevaluationdeterminanth mdr_nb_successor_rankzeroevaluationdeterminanth mdr_nc_successor_rankzeroevaluationdeterminanth mdr_p_successor_rankzeroevaluationdeterminanth mdr_n_successor_rankzeroevaluationdeterminanth. ((exists mdr_z_successor_rankzeroevaluationdeterminanthr. ((exists mdr_a_successor_rankzeroevaluationdeterminanthrc mdr_b_successor_rankzeroevaluationdeterminanthrc mdr_c_successor_rankzeroevaluationdeterminanthrc mdr_e_successor_rankzeroevaluationdeterminanthrc mdr_f_successor_rankzeroevaluationdeterminanthrc. ((mdr_a_successor_rankzeroevaluationdeterminanthrc = ((mdr_d_successor_rankzeroevaluationdeterminanth) + (mdr_pb_successor_rankzeroevaluationdeterminanth)) * S ((mdr_d_successor_rankzeroevaluationdeterminanth) + (mdr_pb_successor_rankzeroevaluationdeterminanth)) + ((mdr_pb_successor_rankzeroevaluationdeterminanth) + (mdr_pb_successor_rankzeroevaluationdeterminanth))) /\ ((mdr_b_successor_rankzeroevaluationdeterminanthrc = ((mdr_pc_successor_rankzeroevaluationdeterminanth) + (mdr_nb_successor_rankzeroevaluationdeterminanth)) * S ((mdr_pc_successor_rankzeroevaluationdeterminanth) + (mdr_nb_successor_rankzeroevaluationdeterminanth)) + ((mdr_nb_successor_rankzeroevaluationdeterminanth) + (mdr_nb_successor_rankzeroevaluationdeterminanth))) /\ ((mdr_c_successor_rankzeroevaluationdeterminanthrc = ((mdr_a_successor_rankzeroevaluationdeterminanthrc) + (mdr_b_successor_rankzeroevaluationdeterminanthrc)) * S ((mdr_a_successor_rankzeroevaluationdeterminanthrc) + (mdr_b_successor_rankzeroevaluationdeterminanthrc)) + ((mdr_b_successor_rankzeroevaluationdeterminanthrc) + (mdr_b_successor_rankzeroevaluationdeterminanthrc))) /\ ((mdr_e_successor_rankzeroevaluationdeterminanthrc = ((mdr_p_successor_rankzeroevaluationdeterminanth) + (mdr_n_successor_rankzeroevaluationdeterminanth)) * S ((mdr_p_successor_rankzeroevaluationdeterminanth) + (mdr_n_successor_rankzeroevaluationdeterminanth)) + ((mdr_n_successor_rankzeroevaluationdeterminanth) + (mdr_n_successor_rankzeroevaluationdeterminanth))) /\ ((mdr_f_successor_rankzeroevaluationdeterminanthrc = ((mdr_nc_successor_rankzeroevaluationdeterminanth) + (mdr_e_successor_rankzeroevaluationdeterminanthrc)) * S ((mdr_nc_successor_rankzeroevaluationdeterminanth) + (mdr_e_successor_rankzeroevaluationdeterminanthrc)) + ((mdr_e_successor_rankzeroevaluationdeterminanthrc) + (mdr_e_successor_rankzeroevaluationdeterminanthrc))) /\ ((mdr_z_successor_rankzeroevaluationdeterminanthr) = ((mdr_c_successor_rankzeroevaluationdeterminanthrc) + (mdr_f_successor_rankzeroevaluationdeterminanthrc)) * S ((mdr_c_successor_rankzeroevaluationdeterminanthrc) + (mdr_f_successor_rankzeroevaluationdeterminanthrc)) + ((mdr_f_successor_rankzeroevaluationdeterminanthrc) + (mdr_f_successor_rankzeroevaluationdeterminanthrc))))))))) /\ (((exists ff_h_mdr_successor_rankzeroevaluationdeterminanthrb. ff_h_mdr_successor_rankzeroevaluationdeterminanthrb + S (mdr_z_successor_rankzeroevaluationdeterminanthr) = S ((S (mdr_i_successor_rankzeroevaluationdeterminanth)) * mdr_c_successor_rankzeroevaluationdeterminant)) /\ exists ff_q_mdr_successor_rankzeroevaluationdeterminanthrb. mdr_b_successor_rankzeroevaluationdeterminant = ff_q_mdr_successor_rankzeroevaluationdeterminanthrb * S ((S (mdr_i_successor_rankzeroevaluationdeterminanth)) * mdr_c_successor_rankzeroevaluationdeterminant) + (mdr_z_successor_rankzeroevaluationdeterminanthr))))) /\ (((((mdr_d_successor_rankzeroevaluationdeterminanth) = 0) /\ (((mdr_p_successor_rankzeroevaluationdeterminanth) = 1) /\ ((mdr_n_successor_rankzeroevaluationdeterminanth) = 0))) \/ exists mdr_q_successor_rankzeroevaluationdeterminanths mdr_eb_successor_rankzeroevaluationdeterminanths mdr_ec_successor_rankzeroevaluationdeterminanths mdr_fb_successor_rankzeroevaluationdeterminanths mdr_fc_successor_rankzeroevaluationdeterminanths. (((mdr_d_successor_rankzeroevaluationdeterminanth) = S (mdr_q_successor_rankzeroevaluationdeterminanths)) /\ ((forall mdr_j_successor_rankzeroevaluationdeterminanthsc. (exists mdr_gap_successor_rankzeroevaluationdeterminanthscj. mdr_gap_successor_rankzeroevaluationdeterminanthscj + S (mdr_j_successor_rankzeroevaluationdeterminanthsc) = (S (mdr_q_successor_rankzeroevaluationdeterminanths))) -> exists mdr_i_successor_rankzeroevaluationdeterminanthsc mdr_up_successor_rankzeroevaluationdeterminanthsc mdr_us_successor_rankzeroevaluationdeterminanthsc mdr_un_successor_rankzeroevaluationdeterminanthsc mdr_ut_successor_rankzeroevaluationdeterminanthsc mdr_p_successor_rankzeroevaluationdeterminanthsc mdr_n_successor_rankzeroevaluationdeterminanthsc. ((exists mdr_gap_successor_rankzeroevaluationdeterminanthsci. mdr_gap_successor_rankzeroevaluationdeterminanthsci + S (mdr_i_successor_rankzeroevaluationdeterminanthsc) = (mdr_i_successor_rankzeroevaluationdeterminanth)) /\ ((exists mdr_z_successor_rankzeroevaluationdeterminanthscr. ((exists mdr_a_successor_rankzeroevaluationdeterminanthscrc mdr_b_successor_rankzeroevaluationdeterminanthscrc mdr_c_successor_rankzeroevaluationdeterminanthscrc mdr_e_successor_rankzeroevaluationdeterminanthscrc mdr_f_successor_rankzeroevaluationdeterminanthscrc. ((mdr_a_successor_rankzeroevaluationdeterminanthscrc = ((mdr_q_successor_rankzeroevaluationdeterminanths) + (mdr_up_successor_rankzeroevaluationdeterminanthsc)) * S ((mdr_q_successor_rankzeroevaluationdeterminanths) + (mdr_up_successor_rankzeroevaluationdeterminanthsc)) + ((mdr_up_successor_rankzeroevaluationdeterminanthsc) + (mdr_up_successor_rankzeroevaluationdeterminanthsc))) /\ ((mdr_b_successor_rankzeroevaluationdeterminanthscrc = ((mdr_us_successor_rankzeroevaluationdeterminanthsc) + (mdr_un_successor_rankzeroevaluationdeterminanthsc)) * S ((mdr_us_successor_rankzeroevaluationdeterminanthsc) + (mdr_un_successor_rankzeroevaluationdeterminanthsc)) + ((mdr_un_successor_rankzeroevaluationdeterminanthsc) + (mdr_un_successor_rankzeroevaluationdeterminanthsc))) /\ ((mdr_c_successor_rankzeroevaluationdeterminanthscrc = ((mdr_a_successor_rankzeroevaluationdeterminanthscrc) + (mdr_b_successor_rankzeroevaluationdeterminanthscrc)) * S ((mdr_a_successor_rankzeroevaluationdeterminanthscrc) + (mdr_b_successor_rankzeroevaluationdeterminanthscrc)) + ((mdr_b_successor_rankzeroevaluationdeterminanthscrc) + (mdr_b_successor_rankzeroevaluationdeterminanthscrc))) /\ ((mdr_e_successor_rankzeroevaluationdeterminanthscrc = ((mdr_p_successor_rankzeroevaluationdeterminanthsc) + (mdr_n_successor_rankzeroevaluationdeterminanthsc)) * S ((mdr_p_successor_rankzeroevaluationdeterminanthsc) + (mdr_n_successor_rankzeroevaluationdeterminanthsc)) + ((mdr_n_successor_rankzeroevaluationdeterminanthsc) + (mdr_n_successor_rankzeroevaluationdeterminanthsc))) /\ ((mdr_f_successor_rankzeroevaluationdeterminanthscrc = ((mdr_ut_successor_rankzeroevaluationdeterminanthsc) + (mdr_e_successor_rankzeroevaluationdeterminanthscrc)) * S ((mdr_ut_successor_rankzeroevaluationdeterminanthsc) + (mdr_e_successor_rankzeroevaluationdeterminanthscrc)) + ((mdr_e_successor_rankzeroevaluationdeterminanthscrc) + (mdr_e_successor_rankzeroevaluationdeterminanthscrc))) /\ ((mdr_z_successor_rankzeroevaluationdeterminanthscr) = ((mdr_c_successor_rankzeroevaluationdeterminanthscrc) + (mdr_f_successor_rankzeroevaluationdeterminanthscrc)) * S ((mdr_c_successor_rankzeroevaluationdeterminanthscrc) + (mdr_f_successor_rankzeroevaluationdeterminanthscrc)) + ((mdr_f_successor_rankzeroevaluationdeterminanthscrc) + (mdr_f_successor_rankzeroevaluationdeterminanthscrc))))))))) /\ (((exists ff_h_mdr_successor_rankzeroevaluationdeterminanthscrb. ff_h_mdr_successor_rankzeroevaluationdeterminanthscrb + S (mdr_z_successor_rankzeroevaluationdeterminanthscr) = S ((S (mdr_i_successor_rankzeroevaluationdeterminanthsc)) * mdr_c_successor_rankzeroevaluationdeterminant)) /\ exists ff_q_mdr_successor_rankzeroevaluationdeterminanthscrb. mdr_b_successor_rankzeroevaluationdeterminant = ff_q_mdr_successor_rankzeroevaluationdeterminanthscrb * S ((S (mdr_i_successor_rankzeroevaluationdeterminanthsc)) * mdr_c_successor_rankzeroevaluationdeterminant) + (mdr_z_successor_rankzeroevaluationdeterminanthscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_successor_rankzeroevaluationdeterminanthscm_positive. (exists ff_gap_mdm_lt_mdr_successor_rankzeroevaluationdeterminanthscm_positive_index_bound. ff_gap_mdm_lt_mdr_successor_rankzeroevaluationdeterminanthscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_successor_rankzeroevaluationdeterminanthscm_positive) = ((mdr_q_successor_rankzeroevaluationdeterminanths) * (mdr_q_successor_rankzeroevaluationdeterminanths))) -> exists ff_row_mdm_prefix_mdr_successor_rankzeroevaluationdeterminanthscm_positive ff_column_mdm_prefix_mdr_successor_rankzeroevaluationdeterminanthscm_positive ff_value_mdm_prefix_mdr_successor_rankzeroevaluationdeterminanthscm_positive. (ff_index_mdm_prefix_mdr_successor_rankzeroevaluationdeterminanthscm_positive = (mdr_q_successor_rankzeroevaluationdeterminanths) * ff_row_mdm_prefix_mdr_successor_rankzeroevaluationdeterminanthscm_positive + ff_column_mdm_prefix_mdr_successor_rankzeroevaluationdeterminanthscm_positive /\ ((exists ff_gap_mdm_lt_mdr_successor_rankzeroevaluationdeterminanthscm_positive_column_bound. ff_gap_mdm_lt_mdr_successor_rankzeroevaluationdeterminanthscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_successor_rankzeroevaluationdeterminanthscm_positive) = (mdr_q_successor_rankzeroevaluationdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_successor_rankzeroevaluationdeterminanthscm_positive_cell ff_column_mdm_cell_mdr_successor_rankzeroevaluationdeterminanthscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_successor_rankzeroevaluationdeterminanthscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_successor_rankzeroevaluationdeterminanthscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_successor_rankzeroevaluationdeterminanthscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_successor_rankzeroevaluationdeterminanthscm_positive_cell = ff_row_mdm_prefix_mdr_successor_rankzeroevaluationdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_successor_rankzeroevaluationdeterminanthscm_positive_cell_row_after. ff_gap_mdm_le_mdr_successor_rankzeroevaluationdeterminanthscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_successor_rankzeroevaluationdeterminanthscm_positive)) /\ ff_row_mdm_cell_mdr_successor_rankzeroevaluationdeterminanthscm_positive_cell = S ff_row_mdm_prefix_mdr_successor_rankzeroevaluationdeterminanthscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_successor_rankzeroevaluationdeterminanthscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_successor_rankzeroevaluationdeterminanthscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_successor_rankzeroevaluationdeterminanthscm_positive) = (mdr_j_successor_rankzeroevaluationdeterminanthsc)) /\ ff_column_mdm_cell_mdr_successor_rankzeroevaluationdeterminanthscm_positive_cell = ff_column_mdm_prefix_mdr_successor_rankzeroevaluationdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_successor_rankzeroevaluationdeterminanthscm_positive_cell_column_after. ff_gap_mdm_le_mdr_successor_rankzeroevaluationdeterminanthscm_positive_cell_column_after + (mdr_j_successor_rankzeroevaluationdeterminanthsc) = (ff_column_mdm_prefix_mdr_successor_rankzeroevaluationdeterminanthscm_positive)) /\ ff_column_mdm_cell_mdr_successor_rankzeroevaluationdeterminanthscm_positive_cell = S ff_column_mdm_prefix_mdr_successor_rankzeroevaluationdeterminanthscm_positive))) /\ (((exists ff_h_mdm_mdr_successor_rankzeroevaluationdeterminanthscm_positive_cell_source. ff_h_mdm_mdr_successor_rankzeroevaluationdeterminanthscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_successor_rankzeroevaluationdeterminanthscm_positive) = S ((S ((ff_row_mdm_cell_mdr_successor_rankzeroevaluationdeterminanthscm_positive_cell) * (S (mdr_q_successor_rankzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_successor_rankzeroevaluationdeterminanthscm_positive_cell))) * mdr_pc_successor_rankzeroevaluationdeterminanth)) /\ exists ff_q_mdm_mdr_successor_rankzeroevaluationdeterminanthscm_positive_cell_source. mdr_pb_successor_rankzeroevaluationdeterminanth = ff_q_mdm_mdr_successor_rankzeroevaluationdeterminanthscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_successor_rankzeroevaluationdeterminanthscm_positive_cell) * (S (mdr_q_successor_rankzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_successor_rankzeroevaluationdeterminanthscm_positive_cell))) * mdr_pc_successor_rankzeroevaluationdeterminanth) + (ff_value_mdm_prefix_mdr_successor_rankzeroevaluationdeterminanthscm_positive)))))) /\ (((exists ff_h_mdm_mdr_successor_rankzeroevaluationdeterminanthscm_positive_target. ff_h_mdm_mdr_successor_rankzeroevaluationdeterminanthscm_positive_target + S (ff_value_mdm_prefix_mdr_successor_rankzeroevaluationdeterminanthscm_positive) = S ((S (ff_index_mdm_prefix_mdr_successor_rankzeroevaluationdeterminanthscm_positive)) * mdr_us_successor_rankzeroevaluationdeterminanthsc)) /\ exists ff_q_mdm_mdr_successor_rankzeroevaluationdeterminanthscm_positive_target. mdr_up_successor_rankzeroevaluationdeterminanthsc = ff_q_mdm_mdr_successor_rankzeroevaluationdeterminanthscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_successor_rankzeroevaluationdeterminanthscm_positive)) * mdr_us_successor_rankzeroevaluationdeterminanthsc) + (ff_value_mdm_prefix_mdr_successor_rankzeroevaluationdeterminanthscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_successor_rankzeroevaluationdeterminanthscm_negative. (exists ff_gap_mdm_lt_mdr_successor_rankzeroevaluationdeterminanthscm_negative_index_bound. ff_gap_mdm_lt_mdr_successor_rankzeroevaluationdeterminanthscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_successor_rankzeroevaluationdeterminanthscm_negative) = ((mdr_q_successor_rankzeroevaluationdeterminanths) * (mdr_q_successor_rankzeroevaluationdeterminanths))) -> exists ff_row_mdm_prefix_mdr_successor_rankzeroevaluationdeterminanthscm_negative ff_column_mdm_prefix_mdr_successor_rankzeroevaluationdeterminanthscm_negative ff_value_mdm_prefix_mdr_successor_rankzeroevaluationdeterminanthscm_negative. (ff_index_mdm_prefix_mdr_successor_rankzeroevaluationdeterminanthscm_negative = (mdr_q_successor_rankzeroevaluationdeterminanths) * ff_row_mdm_prefix_mdr_successor_rankzeroevaluationdeterminanthscm_negative + ff_column_mdm_prefix_mdr_successor_rankzeroevaluationdeterminanthscm_negative /\ ((exists ff_gap_mdm_lt_mdr_successor_rankzeroevaluationdeterminanthscm_negative_column_bound. ff_gap_mdm_lt_mdr_successor_rankzeroevaluationdeterminanthscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_successor_rankzeroevaluationdeterminanthscm_negative) = (mdr_q_successor_rankzeroevaluationdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_successor_rankzeroevaluationdeterminanthscm_negative_cell ff_column_mdm_cell_mdr_successor_rankzeroevaluationdeterminanthscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_successor_rankzeroevaluationdeterminanthscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_successor_rankzeroevaluationdeterminanthscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_successor_rankzeroevaluationdeterminanthscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_successor_rankzeroevaluationdeterminanthscm_negative_cell = ff_row_mdm_prefix_mdr_successor_rankzeroevaluationdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_successor_rankzeroevaluationdeterminanthscm_negative_cell_row_after. ff_gap_mdm_le_mdr_successor_rankzeroevaluationdeterminanthscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_successor_rankzeroevaluationdeterminanthscm_negative)) /\ ff_row_mdm_cell_mdr_successor_rankzeroevaluationdeterminanthscm_negative_cell = S ff_row_mdm_prefix_mdr_successor_rankzeroevaluationdeterminanthscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_successor_rankzeroevaluationdeterminanthscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_successor_rankzeroevaluationdeterminanthscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_successor_rankzeroevaluationdeterminanthscm_negative) = (mdr_j_successor_rankzeroevaluationdeterminanthsc)) /\ ff_column_mdm_cell_mdr_successor_rankzeroevaluationdeterminanthscm_negative_cell = ff_column_mdm_prefix_mdr_successor_rankzeroevaluationdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_successor_rankzeroevaluationdeterminanthscm_negative_cell_column_after. ff_gap_mdm_le_mdr_successor_rankzeroevaluationdeterminanthscm_negative_cell_column_after + (mdr_j_successor_rankzeroevaluationdeterminanthsc) = (ff_column_mdm_prefix_mdr_successor_rankzeroevaluationdeterminanthscm_negative)) /\ ff_column_mdm_cell_mdr_successor_rankzeroevaluationdeterminanthscm_negative_cell = S ff_column_mdm_prefix_mdr_successor_rankzeroevaluationdeterminanthscm_negative))) /\ (((exists ff_h_mdm_mdr_successor_rankzeroevaluationdeterminanthscm_negative_cell_source. ff_h_mdm_mdr_successor_rankzeroevaluationdeterminanthscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_successor_rankzeroevaluationdeterminanthscm_negative) = S ((S ((ff_row_mdm_cell_mdr_successor_rankzeroevaluationdeterminanthscm_negative_cell) * (S (mdr_q_successor_rankzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_successor_rankzeroevaluationdeterminanthscm_negative_cell))) * mdr_nc_successor_rankzeroevaluationdeterminanth)) /\ exists ff_q_mdm_mdr_successor_rankzeroevaluationdeterminanthscm_negative_cell_source. mdr_nb_successor_rankzeroevaluationdeterminanth = ff_q_mdm_mdr_successor_rankzeroevaluationdeterminanthscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_successor_rankzeroevaluationdeterminanthscm_negative_cell) * (S (mdr_q_successor_rankzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_successor_rankzeroevaluationdeterminanthscm_negative_cell))) * mdr_nc_successor_rankzeroevaluationdeterminanth) + (ff_value_mdm_prefix_mdr_successor_rankzeroevaluationdeterminanthscm_negative)))))) /\ (((exists ff_h_mdm_mdr_successor_rankzeroevaluationdeterminanthscm_negative_target. ff_h_mdm_mdr_successor_rankzeroevaluationdeterminanthscm_negative_target + S (ff_value_mdm_prefix_mdr_successor_rankzeroevaluationdeterminanthscm_negative) = S ((S (ff_index_mdm_prefix_mdr_successor_rankzeroevaluationdeterminanthscm_negative)) * mdr_ut_successor_rankzeroevaluationdeterminanthsc)) /\ exists ff_q_mdm_mdr_successor_rankzeroevaluationdeterminanthscm_negative_target. mdr_un_successor_rankzeroevaluationdeterminanthsc = ff_q_mdm_mdr_successor_rankzeroevaluationdeterminanthscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_successor_rankzeroevaluationdeterminanthscm_negative)) * mdr_ut_successor_rankzeroevaluationdeterminanthsc) + (ff_value_mdm_prefix_mdr_successor_rankzeroevaluationdeterminanthscm_negative))))))))) /\ ((((exists ff_h_mdr_successor_rankzeroevaluationdeterminanthscp. ff_h_mdr_successor_rankzeroevaluationdeterminanthscp + S (mdr_p_successor_rankzeroevaluationdeterminanthsc) = S ((S (mdr_j_successor_rankzeroevaluationdeterminanthsc)) * mdr_ec_successor_rankzeroevaluationdeterminanths)) /\ exists ff_q_mdr_successor_rankzeroevaluationdeterminanthscp. mdr_eb_successor_rankzeroevaluationdeterminanths = ff_q_mdr_successor_rankzeroevaluationdeterminanthscp * S ((S (mdr_j_successor_rankzeroevaluationdeterminanthsc)) * mdr_ec_successor_rankzeroevaluationdeterminanths) + (mdr_p_successor_rankzeroevaluationdeterminanthsc))) /\ (((exists ff_h_mdr_successor_rankzeroevaluationdeterminanthscn. ff_h_mdr_successor_rankzeroevaluationdeterminanthscn + S (mdr_n_successor_rankzeroevaluationdeterminanthsc) = S ((S (mdr_j_successor_rankzeroevaluationdeterminanthsc)) * mdr_fc_successor_rankzeroevaluationdeterminanths)) /\ exists ff_q_mdr_successor_rankzeroevaluationdeterminanthscn. mdr_fb_successor_rankzeroevaluationdeterminanths = ff_q_mdr_successor_rankzeroevaluationdeterminanthscn * S ((S (mdr_j_successor_rankzeroevaluationdeterminanthsc)) * mdr_fc_successor_rankzeroevaluationdeterminanths) + (mdr_n_successor_rankzeroevaluationdeterminanthsc)))))))) /\ (exists ff_ub_mce_fold_mdr_successor_rankzeroevaluationdeterminanthsf ff_uc_mce_fold_mdr_successor_rankzeroevaluationdeterminanthsf ff_vb_mce_fold_mdr_successor_rankzeroevaluationdeterminanthsf ff_vc_mce_fold_mdr_successor_rankzeroevaluationdeterminanthsf. ((forall ff_index_mce_alternating_mdr_successor_rankzeroevaluationdeterminanthsf_prefix. (exists ff_gap_mce_mdr_successor_rankzeroevaluationdeterminanthsf_prefix_index. ff_gap_mce_mdr_successor_rankzeroevaluationdeterminanthsf_prefix_index + S (ff_index_mce_alternating_mdr_successor_rankzeroevaluationdeterminanthsf_prefix) = (S (mdr_q_successor_rankzeroevaluationdeterminanths))) -> exists ff_ap_mce_alternating_mdr_successor_rankzeroevaluationdeterminanthsf_prefix ff_an_mce_alternating_mdr_successor_rankzeroevaluationdeterminanthsf_prefix ff_bp_mce_alternating_mdr_successor_rankzeroevaluationdeterminanthsf_prefix ff_bn_mce_alternating_mdr_successor_rankzeroevaluationdeterminanthsf_prefix ff_p_mce_alternating_mdr_successor_rankzeroevaluationdeterminanthsf_prefix ff_n_mce_alternating_mdr_successor_rankzeroevaluationdeterminanthsf_prefix. ((((exists ff_h_mce_mdr_successor_rankzeroevaluationdeterminanthsf_prefix_ap. ff_h_mce_mdr_successor_rankzeroevaluationdeterminanthsf_prefix_ap + S (ff_ap_mce_alternating_mdr_successor_rankzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_successor_rankzeroevaluationdeterminanthsf_prefix)) * mdr_pc_successor_rankzeroevaluationdeterminanth)) /\ exists ff_q_mce_mdr_successor_rankzeroevaluationdeterminanthsf_prefix_ap. mdr_pb_successor_rankzeroevaluationdeterminanth = ff_q_mce_mdr_successor_rankzeroevaluationdeterminanthsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_successor_rankzeroevaluationdeterminanthsf_prefix)) * mdr_pc_successor_rankzeroevaluationdeterminanth) + (ff_ap_mce_alternating_mdr_successor_rankzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_successor_rankzeroevaluationdeterminanthsf_prefix_an. ff_h_mce_mdr_successor_rankzeroevaluationdeterminanthsf_prefix_an + S (ff_an_mce_alternating_mdr_successor_rankzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_successor_rankzeroevaluationdeterminanthsf_prefix)) * mdr_nc_successor_rankzeroevaluationdeterminanth)) /\ exists ff_q_mce_mdr_successor_rankzeroevaluationdeterminanthsf_prefix_an. mdr_nb_successor_rankzeroevaluationdeterminanth = ff_q_mce_mdr_successor_rankzeroevaluationdeterminanthsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_successor_rankzeroevaluationdeterminanthsf_prefix)) * mdr_nc_successor_rankzeroevaluationdeterminanth) + (ff_an_mce_alternating_mdr_successor_rankzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_successor_rankzeroevaluationdeterminanthsf_prefix_bp. ff_h_mce_mdr_successor_rankzeroevaluationdeterminanthsf_prefix_bp + S (ff_bp_mce_alternating_mdr_successor_rankzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_successor_rankzeroevaluationdeterminanthsf_prefix)) * mdr_ec_successor_rankzeroevaluationdeterminanths)) /\ exists ff_q_mce_mdr_successor_rankzeroevaluationdeterminanthsf_prefix_bp. mdr_eb_successor_rankzeroevaluationdeterminanths = ff_q_mce_mdr_successor_rankzeroevaluationdeterminanthsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_successor_rankzeroevaluationdeterminanthsf_prefix)) * mdr_ec_successor_rankzeroevaluationdeterminanths) + (ff_bp_mce_alternating_mdr_successor_rankzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_successor_rankzeroevaluationdeterminanthsf_prefix_bn. ff_h_mce_mdr_successor_rankzeroevaluationdeterminanthsf_prefix_bn + S (ff_bn_mce_alternating_mdr_successor_rankzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_successor_rankzeroevaluationdeterminanthsf_prefix)) * mdr_fc_successor_rankzeroevaluationdeterminanths)) /\ exists ff_q_mce_mdr_successor_rankzeroevaluationdeterminanthsf_prefix_bn. mdr_fb_successor_rankzeroevaluationdeterminanths = ff_q_mce_mdr_successor_rankzeroevaluationdeterminanthsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_successor_rankzeroevaluationdeterminanthsf_prefix)) * mdr_fc_successor_rankzeroevaluationdeterminanths) + (ff_bn_mce_alternating_mdr_successor_rankzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_successor_rankzeroevaluationdeterminanthsf_prefix_positive. ff_h_mce_mdr_successor_rankzeroevaluationdeterminanthsf_prefix_positive + S (ff_p_mce_alternating_mdr_successor_rankzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_successor_rankzeroevaluationdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_successor_rankzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_successor_rankzeroevaluationdeterminanthsf_prefix_positive. ff_ub_mce_fold_mdr_successor_rankzeroevaluationdeterminanthsf = ff_q_mce_mdr_successor_rankzeroevaluationdeterminanthsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_successor_rankzeroevaluationdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_successor_rankzeroevaluationdeterminanthsf) + (ff_p_mce_alternating_mdr_successor_rankzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_successor_rankzeroevaluationdeterminanthsf_prefix_negative. ff_h_mce_mdr_successor_rankzeroevaluationdeterminanthsf_prefix_negative + S (ff_n_mce_alternating_mdr_successor_rankzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_successor_rankzeroevaluationdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_successor_rankzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_successor_rankzeroevaluationdeterminanthsf_prefix_negative. ff_vb_mce_fold_mdr_successor_rankzeroevaluationdeterminanthsf = ff_q_mce_mdr_successor_rankzeroevaluationdeterminanthsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_successor_rankzeroevaluationdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_successor_rankzeroevaluationdeterminanthsf) + (ff_n_mce_alternating_mdr_successor_rankzeroevaluationdeterminanthsf_prefix))) /\ (((exists ff_even_mce_term_mdr_successor_rankzeroevaluationdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_successor_rankzeroevaluationdeterminanthsf_prefix = 2 * ff_even_mce_term_mdr_successor_rankzeroevaluationdeterminanthsf_prefix_term) /\ (ff_p_mce_alternating_mdr_successor_rankzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_successor_rankzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_successor_rankzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_successor_rankzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_successor_rankzeroevaluationdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_successor_rankzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_successor_rankzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_successor_rankzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_successor_rankzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_successor_rankzeroevaluationdeterminanthsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_successor_rankzeroevaluationdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_successor_rankzeroevaluationdeterminanthsf_prefix = 2 * ff_odd_mce_term_mdr_successor_rankzeroevaluationdeterminanthsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_successor_rankzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_successor_rankzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_successor_rankzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_successor_rankzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_successor_rankzeroevaluationdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_successor_rankzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_successor_rankzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_successor_rankzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_successor_rankzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_successor_rankzeroevaluationdeterminanthsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_successor_rankzeroevaluationdeterminanthsf_positive ff_v_mce_mdr_successor_rankzeroevaluationdeterminanthsf_positive. ((((exists ff_h_mce_mdr_successor_rankzeroevaluationdeterminanthsf_positive_start. ff_h_mce_mdr_successor_rankzeroevaluationdeterminanthsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_successor_rankzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_successor_rankzeroevaluationdeterminanthsf_positive_start. ff_u_mce_mdr_successor_rankzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_successor_rankzeroevaluationdeterminanthsf_positive_start * S ((S (0)) * ff_v_mce_mdr_successor_rankzeroevaluationdeterminanthsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_successor_rankzeroevaluationdeterminanthsf_positive_terminal. ff_h_mce_mdr_successor_rankzeroevaluationdeterminanthsf_positive_terminal + S (mdr_p_successor_rankzeroevaluationdeterminanth) = S ((S ((S (mdr_q_successor_rankzeroevaluationdeterminanths)))) * ff_v_mce_mdr_successor_rankzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_successor_rankzeroevaluationdeterminanthsf_positive_terminal. ff_u_mce_mdr_successor_rankzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_successor_rankzeroevaluationdeterminanthsf_positive_terminal * S ((S ((S (mdr_q_successor_rankzeroevaluationdeterminanths)))) * ff_v_mce_mdr_successor_rankzeroevaluationdeterminanthsf_positive) + (mdr_p_successor_rankzeroevaluationdeterminanth))) /\ forall ff_i_mce_mdr_successor_rankzeroevaluationdeterminanthsf_positive. (exists ff_lt_mce_mdr_successor_rankzeroevaluationdeterminanthsf_positive_bound. ff_lt_mce_mdr_successor_rankzeroevaluationdeterminanthsf_positive_bound + S ff_i_mce_mdr_successor_rankzeroevaluationdeterminanthsf_positive = (S (mdr_q_successor_rankzeroevaluationdeterminanths))) -> exists ff_a_mce_mdr_successor_rankzeroevaluationdeterminanthsf_positive ff_r_mce_mdr_successor_rankzeroevaluationdeterminanthsf_positive ff_s_mce_mdr_successor_rankzeroevaluationdeterminanthsf_positive. ((((exists ff_h_mce_mdr_successor_rankzeroevaluationdeterminanthsf_positive_summand. ff_h_mce_mdr_successor_rankzeroevaluationdeterminanthsf_positive_summand + S (ff_a_mce_mdr_successor_rankzeroevaluationdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_successor_rankzeroevaluationdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_successor_rankzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_successor_rankzeroevaluationdeterminanthsf_positive_summand. ff_ub_mce_fold_mdr_successor_rankzeroevaluationdeterminanthsf = ff_q_mce_mdr_successor_rankzeroevaluationdeterminanthsf_positive_summand * S ((S (ff_i_mce_mdr_successor_rankzeroevaluationdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_successor_rankzeroevaluationdeterminanthsf) + (ff_a_mce_mdr_successor_rankzeroevaluationdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_successor_rankzeroevaluationdeterminanthsf_positive_partial. ff_h_mce_mdr_successor_rankzeroevaluationdeterminanthsf_positive_partial + S (ff_r_mce_mdr_successor_rankzeroevaluationdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_successor_rankzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_successor_rankzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_successor_rankzeroevaluationdeterminanthsf_positive_partial. ff_u_mce_mdr_successor_rankzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_successor_rankzeroevaluationdeterminanthsf_positive_partial * S ((S (ff_i_mce_mdr_successor_rankzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_successor_rankzeroevaluationdeterminanthsf_positive) + (ff_r_mce_mdr_successor_rankzeroevaluationdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_successor_rankzeroevaluationdeterminanthsf_positive_successor. ff_h_mce_mdr_successor_rankzeroevaluationdeterminanthsf_positive_successor + S (ff_s_mce_mdr_successor_rankzeroevaluationdeterminanthsf_positive) = S ((S (S ff_i_mce_mdr_successor_rankzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_successor_rankzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_successor_rankzeroevaluationdeterminanthsf_positive_successor. ff_u_mce_mdr_successor_rankzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_successor_rankzeroevaluationdeterminanthsf_positive_successor * S ((S (S ff_i_mce_mdr_successor_rankzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_successor_rankzeroevaluationdeterminanthsf_positive) + (ff_s_mce_mdr_successor_rankzeroevaluationdeterminanthsf_positive))) /\ ff_s_mce_mdr_successor_rankzeroevaluationdeterminanthsf_positive = ff_r_mce_mdr_successor_rankzeroevaluationdeterminanthsf_positive + ff_a_mce_mdr_successor_rankzeroevaluationdeterminanthsf_positive)))))) /\ (exists ff_u_mce_mdr_successor_rankzeroevaluationdeterminanthsf_negative ff_v_mce_mdr_successor_rankzeroevaluationdeterminanthsf_negative. ((((exists ff_h_mce_mdr_successor_rankzeroevaluationdeterminanthsf_negative_start. ff_h_mce_mdr_successor_rankzeroevaluationdeterminanthsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_successor_rankzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_successor_rankzeroevaluationdeterminanthsf_negative_start. ff_u_mce_mdr_successor_rankzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_successor_rankzeroevaluationdeterminanthsf_negative_start * S ((S (0)) * ff_v_mce_mdr_successor_rankzeroevaluationdeterminanthsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_successor_rankzeroevaluationdeterminanthsf_negative_terminal. ff_h_mce_mdr_successor_rankzeroevaluationdeterminanthsf_negative_terminal + S (mdr_n_successor_rankzeroevaluationdeterminanth) = S ((S ((S (mdr_q_successor_rankzeroevaluationdeterminanths)))) * ff_v_mce_mdr_successor_rankzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_successor_rankzeroevaluationdeterminanthsf_negative_terminal. ff_u_mce_mdr_successor_rankzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_successor_rankzeroevaluationdeterminanthsf_negative_terminal * S ((S ((S (mdr_q_successor_rankzeroevaluationdeterminanths)))) * ff_v_mce_mdr_successor_rankzeroevaluationdeterminanthsf_negative) + (mdr_n_successor_rankzeroevaluationdeterminanth))) /\ forall ff_i_mce_mdr_successor_rankzeroevaluationdeterminanthsf_negative. (exists ff_lt_mce_mdr_successor_rankzeroevaluationdeterminanthsf_negative_bound. ff_lt_mce_mdr_successor_rankzeroevaluationdeterminanthsf_negative_bound + S ff_i_mce_mdr_successor_rankzeroevaluationdeterminanthsf_negative = (S (mdr_q_successor_rankzeroevaluationdeterminanths))) -> exists ff_a_mce_mdr_successor_rankzeroevaluationdeterminanthsf_negative ff_r_mce_mdr_successor_rankzeroevaluationdeterminanthsf_negative ff_s_mce_mdr_successor_rankzeroevaluationdeterminanthsf_negative. ((((exists ff_h_mce_mdr_successor_rankzeroevaluationdeterminanthsf_negative_summand. ff_h_mce_mdr_successor_rankzeroevaluationdeterminanthsf_negative_summand + S (ff_a_mce_mdr_successor_rankzeroevaluationdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_successor_rankzeroevaluationdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_successor_rankzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_successor_rankzeroevaluationdeterminanthsf_negative_summand. ff_vb_mce_fold_mdr_successor_rankzeroevaluationdeterminanthsf = ff_q_mce_mdr_successor_rankzeroevaluationdeterminanthsf_negative_summand * S ((S (ff_i_mce_mdr_successor_rankzeroevaluationdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_successor_rankzeroevaluationdeterminanthsf) + (ff_a_mce_mdr_successor_rankzeroevaluationdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_successor_rankzeroevaluationdeterminanthsf_negative_partial. ff_h_mce_mdr_successor_rankzeroevaluationdeterminanthsf_negative_partial + S (ff_r_mce_mdr_successor_rankzeroevaluationdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_successor_rankzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_successor_rankzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_successor_rankzeroevaluationdeterminanthsf_negative_partial. ff_u_mce_mdr_successor_rankzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_successor_rankzeroevaluationdeterminanthsf_negative_partial * S ((S (ff_i_mce_mdr_successor_rankzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_successor_rankzeroevaluationdeterminanthsf_negative) + (ff_r_mce_mdr_successor_rankzeroevaluationdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_successor_rankzeroevaluationdeterminanthsf_negative_successor. ff_h_mce_mdr_successor_rankzeroevaluationdeterminanthsf_negative_successor + S (ff_s_mce_mdr_successor_rankzeroevaluationdeterminanthsf_negative) = S ((S (S ff_i_mce_mdr_successor_rankzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_successor_rankzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_successor_rankzeroevaluationdeterminanthsf_negative_successor. ff_u_mce_mdr_successor_rankzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_successor_rankzeroevaluationdeterminanthsf_negative_successor * S ((S (S ff_i_mce_mdr_successor_rankzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_successor_rankzeroevaluationdeterminanthsf_negative) + (ff_s_mce_mdr_successor_rankzeroevaluationdeterminanthsf_negative))) /\ ff_s_mce_mdr_successor_rankzeroevaluationdeterminanthsf_negative = ff_r_mce_mdr_successor_rankzeroevaluationdeterminanthsf_negative + ff_a_mce_mdr_successor_rankzeroevaluationdeterminanthsf_negative))))))))))))))) /\ ((exists mdr_gap_successor_rankzeroevaluationdeterminanti. mdr_gap_successor_rankzeroevaluationdeterminanti + S (mdr_i_successor_rankzeroevaluationdeterminant) = (mdr_l_successor_rankzeroevaluationdeterminant)) /\ (exists mdr_z_successor_rankzeroevaluationdeterminantr. ((exists mdr_a_successor_rankzeroevaluationdeterminantrc mdr_b_successor_rankzeroevaluationdeterminantrc mdr_c_successor_rankzeroevaluationdeterminantrc mdr_e_successor_rankzeroevaluationdeterminantrc mdr_f_successor_rankzeroevaluationdeterminantrc. ((mdr_a_successor_rankzeroevaluationdeterminantrc = ((mdr_q_successor_rank) + (mdr_ub_successor_rankzeroevaluation)) * S ((mdr_q_successor_rank) + (mdr_ub_successor_rankzeroevaluation)) + ((mdr_ub_successor_rankzeroevaluation) + (mdr_ub_successor_rankzeroevaluation))) /\ ((mdr_b_successor_rankzeroevaluationdeterminantrc = ((mdr_uc_successor_rankzeroevaluation) + (mdr_vb_successor_rankzeroevaluation)) * S ((mdr_uc_successor_rankzeroevaluation) + (mdr_vb_successor_rankzeroevaluation)) + ((mdr_vb_successor_rankzeroevaluation) + (mdr_vb_successor_rankzeroevaluation))) /\ ((mdr_c_successor_rankzeroevaluationdeterminantrc = ((mdr_a_successor_rankzeroevaluationdeterminantrc) + (mdr_b_successor_rankzeroevaluationdeterminantrc)) * S ((mdr_a_successor_rankzeroevaluationdeterminantrc) + (mdr_b_successor_rankzeroevaluationdeterminantrc)) + ((mdr_b_successor_rankzeroevaluationdeterminantrc) + (mdr_b_successor_rankzeroevaluationdeterminantrc))) /\ ((mdr_e_successor_rankzeroevaluationdeterminantrc = ((mdr_p_successor_rankzero) + (mdr_n_successor_rankzero)) * S ((mdr_p_successor_rankzero) + (mdr_n_successor_rankzero)) + ((mdr_n_successor_rankzero) + (mdr_n_successor_rankzero))) /\ ((mdr_f_successor_rankzeroevaluationdeterminantrc = ((mdr_vc_successor_rankzeroevaluation) + (mdr_e_successor_rankzeroevaluationdeterminantrc)) * S ((mdr_vc_successor_rankzeroevaluation) + (mdr_e_successor_rankzeroevaluationdeterminantrc)) + ((mdr_e_successor_rankzeroevaluationdeterminantrc) + (mdr_e_successor_rankzeroevaluationdeterminantrc))) /\ ((mdr_z_successor_rankzeroevaluationdeterminantr) = ((mdr_c_successor_rankzeroevaluationdeterminantrc) + (mdr_f_successor_rankzeroevaluationdeterminantrc)) * S ((mdr_c_successor_rankzeroevaluationdeterminantrc) + (mdr_f_successor_rankzeroevaluationdeterminantrc)) + ((mdr_f_successor_rankzeroevaluationdeterminantrc) + (mdr_f_successor_rankzeroevaluationdeterminantrc))))))))) /\ (((exists ff_h_mdr_successor_rankzeroevaluationdeterminantrb. ff_h_mdr_successor_rankzeroevaluationdeterminantrb + S (mdr_z_successor_rankzeroevaluationdeterminantr) = S ((S (mdr_i_successor_rankzeroevaluationdeterminant)) * mdr_c_successor_rankzeroevaluationdeterminant)) /\ exists ff_q_mdr_successor_rankzeroevaluationdeterminantrb. mdr_b_successor_rankzeroevaluationdeterminant = ff_q_mdr_successor_rankzeroevaluationdeterminantrb * S ((S (mdr_i_successor_rankzeroevaluationdeterminant)) * mdr_c_successor_rankzeroevaluationdeterminant) + (mdr_z_successor_rankzeroevaluationdeterminantr)))))))))) -> mdr_p_successor_rankzero = mdr_n_successor_rankzero)))))) -> (forall mdr_rb_successor_minors mdr_rc_successor_minors mdr_cb_successor_minors mdr_cc_successor_minors mdr_p_successor_minors mdr_n_successor_minors. (((forall fom_index_mrf_successor_minorsrowsbound. (exists fom_gap_mrf_successor_minorsrowsbound_index_bound. fom_gap_mrf_successor_minorsrowsbound_index_bound + S (fom_index_mrf_successor_minorsrowsbound) = S rank) -> exists fom_value_mrf_successor_minorsrowsbound. ((((exists fom_beta_height_mrf_successor_minorsrowsbound_entry. fom_beta_height_mrf_successor_minorsrowsbound_entry + S (fom_value_mrf_successor_minorsrowsbound) = S ((S (fom_index_mrf_successor_minorsrowsbound)) * mdr_rc_successor_minors)) /\ exists fom_beta_quotient_mrf_successor_minorsrowsbound_entry. mdr_rb_successor_minors = fom_beta_quotient_mrf_successor_minorsrowsbound_entry * S ((S (fom_index_mrf_successor_minorsrowsbound)) * mdr_rc_successor_minors) + (fom_value_mrf_successor_minorsrowsbound))) /\ (exists fom_gap_mrf_successor_minorsrowsbound_value_bound. fom_gap_mrf_successor_minorsrowsbound_value_bound + S (fom_value_mrf_successor_minorsrowsbound) = r))) /\ (forall mdr_i_successor_minorsrowsdistinct mdr_j_successor_minorsrowsdistinct mdr_a_successor_minorsrowsdistinct. (exists mdr_gap_successor_minorsrowsdistincti. mdr_gap_successor_minorsrowsdistincti + S (mdr_i_successor_minorsrowsdistinct) = (S rank)) -> (exists mdr_gap_successor_minorsrowsdistinctj. mdr_gap_successor_minorsrowsdistinctj + S (mdr_j_successor_minorsrowsdistinct) = (S rank)) -> (((exists ff_h_mdr_successor_minorsrowsdistinctfirst. ff_h_mdr_successor_minorsrowsdistinctfirst + S (mdr_a_successor_minorsrowsdistinct) = S ((S (mdr_i_successor_minorsrowsdistinct)) * mdr_rc_successor_minors)) /\ exists ff_q_mdr_successor_minorsrowsdistinctfirst. mdr_rb_successor_minors = ff_q_mdr_successor_minorsrowsdistinctfirst * S ((S (mdr_i_successor_minorsrowsdistinct)) * mdr_rc_successor_minors) + (mdr_a_successor_minorsrowsdistinct))) -> (((exists ff_h_mdr_successor_minorsrowsdistinctsecond. ff_h_mdr_successor_minorsrowsdistinctsecond + S (mdr_a_successor_minorsrowsdistinct) = S ((S (mdr_j_successor_minorsrowsdistinct)) * mdr_rc_successor_minors)) /\ exists ff_q_mdr_successor_minorsrowsdistinctsecond. mdr_rb_successor_minors = ff_q_mdr_successor_minorsrowsdistinctsecond * S ((S (mdr_j_successor_minorsrowsdistinct)) * mdr_rc_successor_minors) + (mdr_a_successor_minorsrowsdistinct))) -> mdr_i_successor_minorsrowsdistinct = mdr_j_successor_minorsrowsdistinct))) -> (((forall fom_index_mrf_successor_minorscolumnsbound. (exists fom_gap_mrf_successor_minorscolumnsbound_index_bound. fom_gap_mrf_successor_minorscolumnsbound_index_bound + S (fom_index_mrf_successor_minorscolumnsbound) = S rank) -> exists fom_value_mrf_successor_minorscolumnsbound. ((((exists fom_beta_height_mrf_successor_minorscolumnsbound_entry. fom_beta_height_mrf_successor_minorscolumnsbound_entry + S (fom_value_mrf_successor_minorscolumnsbound) = S ((S (fom_index_mrf_successor_minorscolumnsbound)) * mdr_cc_successor_minors)) /\ exists fom_beta_quotient_mrf_successor_minorscolumnsbound_entry. mdr_cb_successor_minors = fom_beta_quotient_mrf_successor_minorscolumnsbound_entry * S ((S (fom_index_mrf_successor_minorscolumnsbound)) * mdr_cc_successor_minors) + (fom_value_mrf_successor_minorscolumnsbound))) /\ (exists fom_gap_mrf_successor_minorscolumnsbound_value_bound. fom_gap_mrf_successor_minorscolumnsbound_value_bound + S (fom_value_mrf_successor_minorscolumnsbound) = w))) /\ (forall mdr_i_successor_minorscolumnsdistinct mdr_j_successor_minorscolumnsdistinct mdr_a_successor_minorscolumnsdistinct. (exists mdr_gap_successor_minorscolumnsdistincti. mdr_gap_successor_minorscolumnsdistincti + S (mdr_i_successor_minorscolumnsdistinct) = (S rank)) -> (exists mdr_gap_successor_minorscolumnsdistinctj. mdr_gap_successor_minorscolumnsdistinctj + S (mdr_j_successor_minorscolumnsdistinct) = (S rank)) -> (((exists ff_h_mdr_successor_minorscolumnsdistinctfirst. ff_h_mdr_successor_minorscolumnsdistinctfirst + S (mdr_a_successor_minorscolumnsdistinct) = S ((S (mdr_i_successor_minorscolumnsdistinct)) * mdr_cc_successor_minors)) /\ exists ff_q_mdr_successor_minorscolumnsdistinctfirst. mdr_cb_successor_minors = ff_q_mdr_successor_minorscolumnsdistinctfirst * S ((S (mdr_i_successor_minorscolumnsdistinct)) * mdr_cc_successor_minors) + (mdr_a_successor_minorscolumnsdistinct))) -> (((exists ff_h_mdr_successor_minorscolumnsdistinctsecond. ff_h_mdr_successor_minorscolumnsdistinctsecond + S (mdr_a_successor_minorscolumnsdistinct) = S ((S (mdr_j_successor_minorscolumnsdistinct)) * mdr_cc_successor_minors)) /\ exists ff_q_mdr_successor_minorscolumnsdistinctsecond. mdr_cb_successor_minors = ff_q_mdr_successor_minorscolumnsdistinctsecond * S ((S (mdr_j_successor_minorscolumnsdistinct)) * mdr_cc_successor_minors) + (mdr_a_successor_minorscolumnsdistinct))) -> mdr_i_successor_minorscolumnsdistinct = mdr_j_successor_minorscolumnsdistinct))) -> (exists mdr_ub_successor_minorsevaluation mdr_uc_successor_minorsevaluation mdr_vb_successor_minorsevaluation mdr_vc_successor_minorsevaluation. ((((forall mdr_i_successor_minorsevaluationmatrixpositive. (exists mdr_gap_successor_minorsevaluationmatrixpositivebound. mdr_gap_successor_minorsevaluationmatrixpositivebound + S (mdr_i_successor_minorsevaluationmatrixpositive) = ((S rank) * (S rank))) -> exists mdr_a_successor_minorsevaluationmatrixpositive. (((exists mdr_r_successor_minorsevaluationmatrixpositivepoint mdr_s_successor_minorsevaluationmatrixpositivepoint mdr_u_successor_minorsevaluationmatrixpositivepoint mdr_v_successor_minorsevaluationmatrixpositivepoint. ((mdr_i_successor_minorsevaluationmatrixpositive = (S rank) * mdr_r_successor_minorsevaluationmatrixpositivepoint + mdr_s_successor_minorsevaluationmatrixpositivepoint) /\ ((exists mdr_gap_successor_minorsevaluationmatrixpositivepointcolumn. mdr_gap_successor_minorsevaluationmatrixpositivepointcolumn + S (mdr_s_successor_minorsevaluationmatrixpositivepoint) = (S rank)) /\ ((((exists ff_h_mdr_successor_minorsevaluationmatrixpositivepointrow_index. ff_h_mdr_successor_minorsevaluationmatrixpositivepointrow_index + S (mdr_u_successor_minorsevaluationmatrixpositivepoint) = S ((S (mdr_r_successor_minorsevaluationmatrixpositivepoint)) * mdr_rc_successor_minors)) /\ exists ff_q_mdr_successor_minorsevaluationmatrixpositivepointrow_index. mdr_rb_successor_minors = ff_q_mdr_successor_minorsevaluationmatrixpositivepointrow_index * S ((S (mdr_r_successor_minorsevaluationmatrixpositivepoint)) * mdr_rc_successor_minors) + (mdr_u_successor_minorsevaluationmatrixpositivepoint))) /\ ((((exists ff_h_mdr_successor_minorsevaluationmatrixpositivepointcolumn_index. ff_h_mdr_successor_minorsevaluationmatrixpositivepointcolumn_index + S (mdr_v_successor_minorsevaluationmatrixpositivepoint) = S ((S (mdr_s_successor_minorsevaluationmatrixpositivepoint)) * mdr_cc_successor_minors)) /\ exists ff_q_mdr_successor_minorsevaluationmatrixpositivepointcolumn_index. mdr_cb_successor_minors = ff_q_mdr_successor_minorsevaluationmatrixpositivepointcolumn_index * S ((S (mdr_s_successor_minorsevaluationmatrixpositivepoint)) * mdr_cc_successor_minors) + (mdr_v_successor_minorsevaluationmatrixpositivepoint))) /\ (((exists ff_h_mdr_successor_minorsevaluationmatrixpositivepointsource. ff_h_mdr_successor_minorsevaluationmatrixpositivepointsource + S (mdr_a_successor_minorsevaluationmatrixpositive) = S ((S ((mdr_u_successor_minorsevaluationmatrixpositivepoint) * (w) + (mdr_v_successor_minorsevaluationmatrixpositivepoint))) * pc)) /\ exists ff_q_mdr_successor_minorsevaluationmatrixpositivepointsource. pb = ff_q_mdr_successor_minorsevaluationmatrixpositivepointsource * S ((S ((mdr_u_successor_minorsevaluationmatrixpositivepoint) * (w) + (mdr_v_successor_minorsevaluationmatrixpositivepoint))) * pc) + (mdr_a_successor_minorsevaluationmatrixpositive)))))))) /\ (((exists ff_h_mdr_successor_minorsevaluationmatrixpositiveoutput. ff_h_mdr_successor_minorsevaluationmatrixpositiveoutput + S (mdr_a_successor_minorsevaluationmatrixpositive) = S ((S (mdr_i_successor_minorsevaluationmatrixpositive)) * mdr_uc_successor_minorsevaluation)) /\ exists ff_q_mdr_successor_minorsevaluationmatrixpositiveoutput. mdr_ub_successor_minorsevaluation = ff_q_mdr_successor_minorsevaluationmatrixpositiveoutput * S ((S (mdr_i_successor_minorsevaluationmatrixpositive)) * mdr_uc_successor_minorsevaluation) + (mdr_a_successor_minorsevaluationmatrixpositive)))))) /\ (forall mdr_i_successor_minorsevaluationmatrixnegative. (exists mdr_gap_successor_minorsevaluationmatrixnegativebound. mdr_gap_successor_minorsevaluationmatrixnegativebound + S (mdr_i_successor_minorsevaluationmatrixnegative) = ((S rank) * (S rank))) -> exists mdr_a_successor_minorsevaluationmatrixnegative. (((exists mdr_r_successor_minorsevaluationmatrixnegativepoint mdr_s_successor_minorsevaluationmatrixnegativepoint mdr_u_successor_minorsevaluationmatrixnegativepoint mdr_v_successor_minorsevaluationmatrixnegativepoint. ((mdr_i_successor_minorsevaluationmatrixnegative = (S rank) * mdr_r_successor_minorsevaluationmatrixnegativepoint + mdr_s_successor_minorsevaluationmatrixnegativepoint) /\ ((exists mdr_gap_successor_minorsevaluationmatrixnegativepointcolumn. mdr_gap_successor_minorsevaluationmatrixnegativepointcolumn + S (mdr_s_successor_minorsevaluationmatrixnegativepoint) = (S rank)) /\ ((((exists ff_h_mdr_successor_minorsevaluationmatrixnegativepointrow_index. ff_h_mdr_successor_minorsevaluationmatrixnegativepointrow_index + S (mdr_u_successor_minorsevaluationmatrixnegativepoint) = S ((S (mdr_r_successor_minorsevaluationmatrixnegativepoint)) * mdr_rc_successor_minors)) /\ exists ff_q_mdr_successor_minorsevaluationmatrixnegativepointrow_index. mdr_rb_successor_minors = ff_q_mdr_successor_minorsevaluationmatrixnegativepointrow_index * S ((S (mdr_r_successor_minorsevaluationmatrixnegativepoint)) * mdr_rc_successor_minors) + (mdr_u_successor_minorsevaluationmatrixnegativepoint))) /\ ((((exists ff_h_mdr_successor_minorsevaluationmatrixnegativepointcolumn_index. ff_h_mdr_successor_minorsevaluationmatrixnegativepointcolumn_index + S (mdr_v_successor_minorsevaluationmatrixnegativepoint) = S ((S (mdr_s_successor_minorsevaluationmatrixnegativepoint)) * mdr_cc_successor_minors)) /\ exists ff_q_mdr_successor_minorsevaluationmatrixnegativepointcolumn_index. mdr_cb_successor_minors = ff_q_mdr_successor_minorsevaluationmatrixnegativepointcolumn_index * S ((S (mdr_s_successor_minorsevaluationmatrixnegativepoint)) * mdr_cc_successor_minors) + (mdr_v_successor_minorsevaluationmatrixnegativepoint))) /\ (((exists ff_h_mdr_successor_minorsevaluationmatrixnegativepointsource. ff_h_mdr_successor_minorsevaluationmatrixnegativepointsource + S (mdr_a_successor_minorsevaluationmatrixnegative) = S ((S ((mdr_u_successor_minorsevaluationmatrixnegativepoint) * (w) + (mdr_v_successor_minorsevaluationmatrixnegativepoint))) * nc)) /\ exists ff_q_mdr_successor_minorsevaluationmatrixnegativepointsource. nb = ff_q_mdr_successor_minorsevaluationmatrixnegativepointsource * S ((S ((mdr_u_successor_minorsevaluationmatrixnegativepoint) * (w) + (mdr_v_successor_minorsevaluationmatrixnegativepoint))) * nc) + (mdr_a_successor_minorsevaluationmatrixnegative)))))))) /\ (((exists ff_h_mdr_successor_minorsevaluationmatrixnegativeoutput. ff_h_mdr_successor_minorsevaluationmatrixnegativeoutput + S (mdr_a_successor_minorsevaluationmatrixnegative) = S ((S (mdr_i_successor_minorsevaluationmatrixnegative)) * mdr_vc_successor_minorsevaluation)) /\ exists ff_q_mdr_successor_minorsevaluationmatrixnegativeoutput. mdr_vb_successor_minorsevaluation = ff_q_mdr_successor_minorsevaluationmatrixnegativeoutput * S ((S (mdr_i_successor_minorsevaluationmatrixnegative)) * mdr_vc_successor_minorsevaluation) + (mdr_a_successor_minorsevaluationmatrixnegative)))))))) /\ (exists mdr_b_successor_minorsevaluationdeterminant mdr_c_successor_minorsevaluationdeterminant mdr_l_successor_minorsevaluationdeterminant mdr_i_successor_minorsevaluationdeterminant. ((forall mdr_i_successor_minorsevaluationdeterminanth. (exists mdr_gap_successor_minorsevaluationdeterminanthi. mdr_gap_successor_minorsevaluationdeterminanthi + S (mdr_i_successor_minorsevaluationdeterminanth) = (mdr_l_successor_minorsevaluationdeterminant)) -> exists mdr_d_successor_minorsevaluationdeterminanth mdr_pb_successor_minorsevaluationdeterminanth mdr_pc_successor_minorsevaluationdeterminanth mdr_nb_successor_minorsevaluationdeterminanth mdr_nc_successor_minorsevaluationdeterminanth mdr_p_successor_minorsevaluationdeterminanth mdr_n_successor_minorsevaluationdeterminanth. ((exists mdr_z_successor_minorsevaluationdeterminanthr. ((exists mdr_a_successor_minorsevaluationdeterminanthrc mdr_b_successor_minorsevaluationdeterminanthrc mdr_c_successor_minorsevaluationdeterminanthrc mdr_e_successor_minorsevaluationdeterminanthrc mdr_f_successor_minorsevaluationdeterminanthrc. ((mdr_a_successor_minorsevaluationdeterminanthrc = ((mdr_d_successor_minorsevaluationdeterminanth) + (mdr_pb_successor_minorsevaluationdeterminanth)) * S ((mdr_d_successor_minorsevaluationdeterminanth) + (mdr_pb_successor_minorsevaluationdeterminanth)) + ((mdr_pb_successor_minorsevaluationdeterminanth) + (mdr_pb_successor_minorsevaluationdeterminanth))) /\ ((mdr_b_successor_minorsevaluationdeterminanthrc = ((mdr_pc_successor_minorsevaluationdeterminanth) + (mdr_nb_successor_minorsevaluationdeterminanth)) * S ((mdr_pc_successor_minorsevaluationdeterminanth) + (mdr_nb_successor_minorsevaluationdeterminanth)) + ((mdr_nb_successor_minorsevaluationdeterminanth) + (mdr_nb_successor_minorsevaluationdeterminanth))) /\ ((mdr_c_successor_minorsevaluationdeterminanthrc = ((mdr_a_successor_minorsevaluationdeterminanthrc) + (mdr_b_successor_minorsevaluationdeterminanthrc)) * S ((mdr_a_successor_minorsevaluationdeterminanthrc) + (mdr_b_successor_minorsevaluationdeterminanthrc)) + ((mdr_b_successor_minorsevaluationdeterminanthrc) + (mdr_b_successor_minorsevaluationdeterminanthrc))) /\ ((mdr_e_successor_minorsevaluationdeterminanthrc = ((mdr_p_successor_minorsevaluationdeterminanth) + (mdr_n_successor_minorsevaluationdeterminanth)) * S ((mdr_p_successor_minorsevaluationdeterminanth) + (mdr_n_successor_minorsevaluationdeterminanth)) + ((mdr_n_successor_minorsevaluationdeterminanth) + (mdr_n_successor_minorsevaluationdeterminanth))) /\ ((mdr_f_successor_minorsevaluationdeterminanthrc = ((mdr_nc_successor_minorsevaluationdeterminanth) + (mdr_e_successor_minorsevaluationdeterminanthrc)) * S ((mdr_nc_successor_minorsevaluationdeterminanth) + (mdr_e_successor_minorsevaluationdeterminanthrc)) + ((mdr_e_successor_minorsevaluationdeterminanthrc) + (mdr_e_successor_minorsevaluationdeterminanthrc))) /\ ((mdr_z_successor_minorsevaluationdeterminanthr) = ((mdr_c_successor_minorsevaluationdeterminanthrc) + (mdr_f_successor_minorsevaluationdeterminanthrc)) * S ((mdr_c_successor_minorsevaluationdeterminanthrc) + (mdr_f_successor_minorsevaluationdeterminanthrc)) + ((mdr_f_successor_minorsevaluationdeterminanthrc) + (mdr_f_successor_minorsevaluationdeterminanthrc))))))))) /\ (((exists ff_h_mdr_successor_minorsevaluationdeterminanthrb. ff_h_mdr_successor_minorsevaluationdeterminanthrb + S (mdr_z_successor_minorsevaluationdeterminanthr) = S ((S (mdr_i_successor_minorsevaluationdeterminanth)) * mdr_c_successor_minorsevaluationdeterminant)) /\ exists ff_q_mdr_successor_minorsevaluationdeterminanthrb. mdr_b_successor_minorsevaluationdeterminant = ff_q_mdr_successor_minorsevaluationdeterminanthrb * S ((S (mdr_i_successor_minorsevaluationdeterminanth)) * mdr_c_successor_minorsevaluationdeterminant) + (mdr_z_successor_minorsevaluationdeterminanthr))))) /\ (((((mdr_d_successor_minorsevaluationdeterminanth) = 0) /\ (((mdr_p_successor_minorsevaluationdeterminanth) = 1) /\ ((mdr_n_successor_minorsevaluationdeterminanth) = 0))) \/ exists mdr_q_successor_minorsevaluationdeterminanths mdr_eb_successor_minorsevaluationdeterminanths mdr_ec_successor_minorsevaluationdeterminanths mdr_fb_successor_minorsevaluationdeterminanths mdr_fc_successor_minorsevaluationdeterminanths. (((mdr_d_successor_minorsevaluationdeterminanth) = S (mdr_q_successor_minorsevaluationdeterminanths)) /\ ((forall mdr_j_successor_minorsevaluationdeterminanthsc. (exists mdr_gap_successor_minorsevaluationdeterminanthscj. mdr_gap_successor_minorsevaluationdeterminanthscj + S (mdr_j_successor_minorsevaluationdeterminanthsc) = (S (mdr_q_successor_minorsevaluationdeterminanths))) -> exists mdr_i_successor_minorsevaluationdeterminanthsc mdr_up_successor_minorsevaluationdeterminanthsc mdr_us_successor_minorsevaluationdeterminanthsc mdr_un_successor_minorsevaluationdeterminanthsc mdr_ut_successor_minorsevaluationdeterminanthsc mdr_p_successor_minorsevaluationdeterminanthsc mdr_n_successor_minorsevaluationdeterminanthsc. ((exists mdr_gap_successor_minorsevaluationdeterminanthsci. mdr_gap_successor_minorsevaluationdeterminanthsci + S (mdr_i_successor_minorsevaluationdeterminanthsc) = (mdr_i_successor_minorsevaluationdeterminanth)) /\ ((exists mdr_z_successor_minorsevaluationdeterminanthscr. ((exists mdr_a_successor_minorsevaluationdeterminanthscrc mdr_b_successor_minorsevaluationdeterminanthscrc mdr_c_successor_minorsevaluationdeterminanthscrc mdr_e_successor_minorsevaluationdeterminanthscrc mdr_f_successor_minorsevaluationdeterminanthscrc. ((mdr_a_successor_minorsevaluationdeterminanthscrc = ((mdr_q_successor_minorsevaluationdeterminanths) + (mdr_up_successor_minorsevaluationdeterminanthsc)) * S ((mdr_q_successor_minorsevaluationdeterminanths) + (mdr_up_successor_minorsevaluationdeterminanthsc)) + ((mdr_up_successor_minorsevaluationdeterminanthsc) + (mdr_up_successor_minorsevaluationdeterminanthsc))) /\ ((mdr_b_successor_minorsevaluationdeterminanthscrc = ((mdr_us_successor_minorsevaluationdeterminanthsc) + (mdr_un_successor_minorsevaluationdeterminanthsc)) * S ((mdr_us_successor_minorsevaluationdeterminanthsc) + (mdr_un_successor_minorsevaluationdeterminanthsc)) + ((mdr_un_successor_minorsevaluationdeterminanthsc) + (mdr_un_successor_minorsevaluationdeterminanthsc))) /\ ((mdr_c_successor_minorsevaluationdeterminanthscrc = ((mdr_a_successor_minorsevaluationdeterminanthscrc) + (mdr_b_successor_minorsevaluationdeterminanthscrc)) * S ((mdr_a_successor_minorsevaluationdeterminanthscrc) + (mdr_b_successor_minorsevaluationdeterminanthscrc)) + ((mdr_b_successor_minorsevaluationdeterminanthscrc) + (mdr_b_successor_minorsevaluationdeterminanthscrc))) /\ ((mdr_e_successor_minorsevaluationdeterminanthscrc = ((mdr_p_successor_minorsevaluationdeterminanthsc) + (mdr_n_successor_minorsevaluationdeterminanthsc)) * S ((mdr_p_successor_minorsevaluationdeterminanthsc) + (mdr_n_successor_minorsevaluationdeterminanthsc)) + ((mdr_n_successor_minorsevaluationdeterminanthsc) + (mdr_n_successor_minorsevaluationdeterminanthsc))) /\ ((mdr_f_successor_minorsevaluationdeterminanthscrc = ((mdr_ut_successor_minorsevaluationdeterminanthsc) + (mdr_e_successor_minorsevaluationdeterminanthscrc)) * S ((mdr_ut_successor_minorsevaluationdeterminanthsc) + (mdr_e_successor_minorsevaluationdeterminanthscrc)) + ((mdr_e_successor_minorsevaluationdeterminanthscrc) + (mdr_e_successor_minorsevaluationdeterminanthscrc))) /\ ((mdr_z_successor_minorsevaluationdeterminanthscr) = ((mdr_c_successor_minorsevaluationdeterminanthscrc) + (mdr_f_successor_minorsevaluationdeterminanthscrc)) * S ((mdr_c_successor_minorsevaluationdeterminanthscrc) + (mdr_f_successor_minorsevaluationdeterminanthscrc)) + ((mdr_f_successor_minorsevaluationdeterminanthscrc) + (mdr_f_successor_minorsevaluationdeterminanthscrc))))))))) /\ (((exists ff_h_mdr_successor_minorsevaluationdeterminanthscrb. ff_h_mdr_successor_minorsevaluationdeterminanthscrb + S (mdr_z_successor_minorsevaluationdeterminanthscr) = S ((S (mdr_i_successor_minorsevaluationdeterminanthsc)) * mdr_c_successor_minorsevaluationdeterminant)) /\ exists ff_q_mdr_successor_minorsevaluationdeterminanthscrb. mdr_b_successor_minorsevaluationdeterminant = ff_q_mdr_successor_minorsevaluationdeterminanthscrb * S ((S (mdr_i_successor_minorsevaluationdeterminanthsc)) * mdr_c_successor_minorsevaluationdeterminant) + (mdr_z_successor_minorsevaluationdeterminanthscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_successor_minorsevaluationdeterminanthscm_positive. (exists ff_gap_mdm_lt_mdr_successor_minorsevaluationdeterminanthscm_positive_index_bound. ff_gap_mdm_lt_mdr_successor_minorsevaluationdeterminanthscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_successor_minorsevaluationdeterminanthscm_positive) = ((mdr_q_successor_minorsevaluationdeterminanths) * (mdr_q_successor_minorsevaluationdeterminanths))) -> exists ff_row_mdm_prefix_mdr_successor_minorsevaluationdeterminanthscm_positive ff_column_mdm_prefix_mdr_successor_minorsevaluationdeterminanthscm_positive ff_value_mdm_prefix_mdr_successor_minorsevaluationdeterminanthscm_positive. (ff_index_mdm_prefix_mdr_successor_minorsevaluationdeterminanthscm_positive = (mdr_q_successor_minorsevaluationdeterminanths) * ff_row_mdm_prefix_mdr_successor_minorsevaluationdeterminanthscm_positive + ff_column_mdm_prefix_mdr_successor_minorsevaluationdeterminanthscm_positive /\ ((exists ff_gap_mdm_lt_mdr_successor_minorsevaluationdeterminanthscm_positive_column_bound. ff_gap_mdm_lt_mdr_successor_minorsevaluationdeterminanthscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_successor_minorsevaluationdeterminanthscm_positive) = (mdr_q_successor_minorsevaluationdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_successor_minorsevaluationdeterminanthscm_positive_cell ff_column_mdm_cell_mdr_successor_minorsevaluationdeterminanthscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_successor_minorsevaluationdeterminanthscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_successor_minorsevaluationdeterminanthscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_successor_minorsevaluationdeterminanthscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_successor_minorsevaluationdeterminanthscm_positive_cell = ff_row_mdm_prefix_mdr_successor_minorsevaluationdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_successor_minorsevaluationdeterminanthscm_positive_cell_row_after. ff_gap_mdm_le_mdr_successor_minorsevaluationdeterminanthscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_successor_minorsevaluationdeterminanthscm_positive)) /\ ff_row_mdm_cell_mdr_successor_minorsevaluationdeterminanthscm_positive_cell = S ff_row_mdm_prefix_mdr_successor_minorsevaluationdeterminanthscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_successor_minorsevaluationdeterminanthscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_successor_minorsevaluationdeterminanthscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_successor_minorsevaluationdeterminanthscm_positive) = (mdr_j_successor_minorsevaluationdeterminanthsc)) /\ ff_column_mdm_cell_mdr_successor_minorsevaluationdeterminanthscm_positive_cell = ff_column_mdm_prefix_mdr_successor_minorsevaluationdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_successor_minorsevaluationdeterminanthscm_positive_cell_column_after. ff_gap_mdm_le_mdr_successor_minorsevaluationdeterminanthscm_positive_cell_column_after + (mdr_j_successor_minorsevaluationdeterminanthsc) = (ff_column_mdm_prefix_mdr_successor_minorsevaluationdeterminanthscm_positive)) /\ ff_column_mdm_cell_mdr_successor_minorsevaluationdeterminanthscm_positive_cell = S ff_column_mdm_prefix_mdr_successor_minorsevaluationdeterminanthscm_positive))) /\ (((exists ff_h_mdm_mdr_successor_minorsevaluationdeterminanthscm_positive_cell_source. ff_h_mdm_mdr_successor_minorsevaluationdeterminanthscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_successor_minorsevaluationdeterminanthscm_positive) = S ((S ((ff_row_mdm_cell_mdr_successor_minorsevaluationdeterminanthscm_positive_cell) * (S (mdr_q_successor_minorsevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_successor_minorsevaluationdeterminanthscm_positive_cell))) * mdr_pc_successor_minorsevaluationdeterminanth)) /\ exists ff_q_mdm_mdr_successor_minorsevaluationdeterminanthscm_positive_cell_source. mdr_pb_successor_minorsevaluationdeterminanth = ff_q_mdm_mdr_successor_minorsevaluationdeterminanthscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_successor_minorsevaluationdeterminanthscm_positive_cell) * (S (mdr_q_successor_minorsevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_successor_minorsevaluationdeterminanthscm_positive_cell))) * mdr_pc_successor_minorsevaluationdeterminanth) + (ff_value_mdm_prefix_mdr_successor_minorsevaluationdeterminanthscm_positive)))))) /\ (((exists ff_h_mdm_mdr_successor_minorsevaluationdeterminanthscm_positive_target. ff_h_mdm_mdr_successor_minorsevaluationdeterminanthscm_positive_target + S (ff_value_mdm_prefix_mdr_successor_minorsevaluationdeterminanthscm_positive) = S ((S (ff_index_mdm_prefix_mdr_successor_minorsevaluationdeterminanthscm_positive)) * mdr_us_successor_minorsevaluationdeterminanthsc)) /\ exists ff_q_mdm_mdr_successor_minorsevaluationdeterminanthscm_positive_target. mdr_up_successor_minorsevaluationdeterminanthsc = ff_q_mdm_mdr_successor_minorsevaluationdeterminanthscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_successor_minorsevaluationdeterminanthscm_positive)) * mdr_us_successor_minorsevaluationdeterminanthsc) + (ff_value_mdm_prefix_mdr_successor_minorsevaluationdeterminanthscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_successor_minorsevaluationdeterminanthscm_negative. (exists ff_gap_mdm_lt_mdr_successor_minorsevaluationdeterminanthscm_negative_index_bound. ff_gap_mdm_lt_mdr_successor_minorsevaluationdeterminanthscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_successor_minorsevaluationdeterminanthscm_negative) = ((mdr_q_successor_minorsevaluationdeterminanths) * (mdr_q_successor_minorsevaluationdeterminanths))) -> exists ff_row_mdm_prefix_mdr_successor_minorsevaluationdeterminanthscm_negative ff_column_mdm_prefix_mdr_successor_minorsevaluationdeterminanthscm_negative ff_value_mdm_prefix_mdr_successor_minorsevaluationdeterminanthscm_negative. (ff_index_mdm_prefix_mdr_successor_minorsevaluationdeterminanthscm_negative = (mdr_q_successor_minorsevaluationdeterminanths) * ff_row_mdm_prefix_mdr_successor_minorsevaluationdeterminanthscm_negative + ff_column_mdm_prefix_mdr_successor_minorsevaluationdeterminanthscm_negative /\ ((exists ff_gap_mdm_lt_mdr_successor_minorsevaluationdeterminanthscm_negative_column_bound. ff_gap_mdm_lt_mdr_successor_minorsevaluationdeterminanthscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_successor_minorsevaluationdeterminanthscm_negative) = (mdr_q_successor_minorsevaluationdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_successor_minorsevaluationdeterminanthscm_negative_cell ff_column_mdm_cell_mdr_successor_minorsevaluationdeterminanthscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_successor_minorsevaluationdeterminanthscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_successor_minorsevaluationdeterminanthscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_successor_minorsevaluationdeterminanthscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_successor_minorsevaluationdeterminanthscm_negative_cell = ff_row_mdm_prefix_mdr_successor_minorsevaluationdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_successor_minorsevaluationdeterminanthscm_negative_cell_row_after. ff_gap_mdm_le_mdr_successor_minorsevaluationdeterminanthscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_successor_minorsevaluationdeterminanthscm_negative)) /\ ff_row_mdm_cell_mdr_successor_minorsevaluationdeterminanthscm_negative_cell = S ff_row_mdm_prefix_mdr_successor_minorsevaluationdeterminanthscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_successor_minorsevaluationdeterminanthscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_successor_minorsevaluationdeterminanthscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_successor_minorsevaluationdeterminanthscm_negative) = (mdr_j_successor_minorsevaluationdeterminanthsc)) /\ ff_column_mdm_cell_mdr_successor_minorsevaluationdeterminanthscm_negative_cell = ff_column_mdm_prefix_mdr_successor_minorsevaluationdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_successor_minorsevaluationdeterminanthscm_negative_cell_column_after. ff_gap_mdm_le_mdr_successor_minorsevaluationdeterminanthscm_negative_cell_column_after + (mdr_j_successor_minorsevaluationdeterminanthsc) = (ff_column_mdm_prefix_mdr_successor_minorsevaluationdeterminanthscm_negative)) /\ ff_column_mdm_cell_mdr_successor_minorsevaluationdeterminanthscm_negative_cell = S ff_column_mdm_prefix_mdr_successor_minorsevaluationdeterminanthscm_negative))) /\ (((exists ff_h_mdm_mdr_successor_minorsevaluationdeterminanthscm_negative_cell_source. ff_h_mdm_mdr_successor_minorsevaluationdeterminanthscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_successor_minorsevaluationdeterminanthscm_negative) = S ((S ((ff_row_mdm_cell_mdr_successor_minorsevaluationdeterminanthscm_negative_cell) * (S (mdr_q_successor_minorsevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_successor_minorsevaluationdeterminanthscm_negative_cell))) * mdr_nc_successor_minorsevaluationdeterminanth)) /\ exists ff_q_mdm_mdr_successor_minorsevaluationdeterminanthscm_negative_cell_source. mdr_nb_successor_minorsevaluationdeterminanth = ff_q_mdm_mdr_successor_minorsevaluationdeterminanthscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_successor_minorsevaluationdeterminanthscm_negative_cell) * (S (mdr_q_successor_minorsevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_successor_minorsevaluationdeterminanthscm_negative_cell))) * mdr_nc_successor_minorsevaluationdeterminanth) + (ff_value_mdm_prefix_mdr_successor_minorsevaluationdeterminanthscm_negative)))))) /\ (((exists ff_h_mdm_mdr_successor_minorsevaluationdeterminanthscm_negative_target. ff_h_mdm_mdr_successor_minorsevaluationdeterminanthscm_negative_target + S (ff_value_mdm_prefix_mdr_successor_minorsevaluationdeterminanthscm_negative) = S ((S (ff_index_mdm_prefix_mdr_successor_minorsevaluationdeterminanthscm_negative)) * mdr_ut_successor_minorsevaluationdeterminanthsc)) /\ exists ff_q_mdm_mdr_successor_minorsevaluationdeterminanthscm_negative_target. mdr_un_successor_minorsevaluationdeterminanthsc = ff_q_mdm_mdr_successor_minorsevaluationdeterminanthscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_successor_minorsevaluationdeterminanthscm_negative)) * mdr_ut_successor_minorsevaluationdeterminanthsc) + (ff_value_mdm_prefix_mdr_successor_minorsevaluationdeterminanthscm_negative))))))))) /\ ((((exists ff_h_mdr_successor_minorsevaluationdeterminanthscp. ff_h_mdr_successor_minorsevaluationdeterminanthscp + S (mdr_p_successor_minorsevaluationdeterminanthsc) = S ((S (mdr_j_successor_minorsevaluationdeterminanthsc)) * mdr_ec_successor_minorsevaluationdeterminanths)) /\ exists ff_q_mdr_successor_minorsevaluationdeterminanthscp. mdr_eb_successor_minorsevaluationdeterminanths = ff_q_mdr_successor_minorsevaluationdeterminanthscp * S ((S (mdr_j_successor_minorsevaluationdeterminanthsc)) * mdr_ec_successor_minorsevaluationdeterminanths) + (mdr_p_successor_minorsevaluationdeterminanthsc))) /\ (((exists ff_h_mdr_successor_minorsevaluationdeterminanthscn. ff_h_mdr_successor_minorsevaluationdeterminanthscn + S (mdr_n_successor_minorsevaluationdeterminanthsc) = S ((S (mdr_j_successor_minorsevaluationdeterminanthsc)) * mdr_fc_successor_minorsevaluationdeterminanths)) /\ exists ff_q_mdr_successor_minorsevaluationdeterminanthscn. mdr_fb_successor_minorsevaluationdeterminanths = ff_q_mdr_successor_minorsevaluationdeterminanthscn * S ((S (mdr_j_successor_minorsevaluationdeterminanthsc)) * mdr_fc_successor_minorsevaluationdeterminanths) + (mdr_n_successor_minorsevaluationdeterminanthsc)))))))) /\ (exists ff_ub_mce_fold_mdr_successor_minorsevaluationdeterminanthsf ff_uc_mce_fold_mdr_successor_minorsevaluationdeterminanthsf ff_vb_mce_fold_mdr_successor_minorsevaluationdeterminanthsf ff_vc_mce_fold_mdr_successor_minorsevaluationdeterminanthsf. ((forall ff_index_mce_alternating_mdr_successor_minorsevaluationdeterminanthsf_prefix. (exists ff_gap_mce_mdr_successor_minorsevaluationdeterminanthsf_prefix_index. ff_gap_mce_mdr_successor_minorsevaluationdeterminanthsf_prefix_index + S (ff_index_mce_alternating_mdr_successor_minorsevaluationdeterminanthsf_prefix) = (S (mdr_q_successor_minorsevaluationdeterminanths))) -> exists ff_ap_mce_alternating_mdr_successor_minorsevaluationdeterminanthsf_prefix ff_an_mce_alternating_mdr_successor_minorsevaluationdeterminanthsf_prefix ff_bp_mce_alternating_mdr_successor_minorsevaluationdeterminanthsf_prefix ff_bn_mce_alternating_mdr_successor_minorsevaluationdeterminanthsf_prefix ff_p_mce_alternating_mdr_successor_minorsevaluationdeterminanthsf_prefix ff_n_mce_alternating_mdr_successor_minorsevaluationdeterminanthsf_prefix. ((((exists ff_h_mce_mdr_successor_minorsevaluationdeterminanthsf_prefix_ap. ff_h_mce_mdr_successor_minorsevaluationdeterminanthsf_prefix_ap + S (ff_ap_mce_alternating_mdr_successor_minorsevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_successor_minorsevaluationdeterminanthsf_prefix)) * mdr_pc_successor_minorsevaluationdeterminanth)) /\ exists ff_q_mce_mdr_successor_minorsevaluationdeterminanthsf_prefix_ap. mdr_pb_successor_minorsevaluationdeterminanth = ff_q_mce_mdr_successor_minorsevaluationdeterminanthsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_successor_minorsevaluationdeterminanthsf_prefix)) * mdr_pc_successor_minorsevaluationdeterminanth) + (ff_ap_mce_alternating_mdr_successor_minorsevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_successor_minorsevaluationdeterminanthsf_prefix_an. ff_h_mce_mdr_successor_minorsevaluationdeterminanthsf_prefix_an + S (ff_an_mce_alternating_mdr_successor_minorsevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_successor_minorsevaluationdeterminanthsf_prefix)) * mdr_nc_successor_minorsevaluationdeterminanth)) /\ exists ff_q_mce_mdr_successor_minorsevaluationdeterminanthsf_prefix_an. mdr_nb_successor_minorsevaluationdeterminanth = ff_q_mce_mdr_successor_minorsevaluationdeterminanthsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_successor_minorsevaluationdeterminanthsf_prefix)) * mdr_nc_successor_minorsevaluationdeterminanth) + (ff_an_mce_alternating_mdr_successor_minorsevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_successor_minorsevaluationdeterminanthsf_prefix_bp. ff_h_mce_mdr_successor_minorsevaluationdeterminanthsf_prefix_bp + S (ff_bp_mce_alternating_mdr_successor_minorsevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_successor_minorsevaluationdeterminanthsf_prefix)) * mdr_ec_successor_minorsevaluationdeterminanths)) /\ exists ff_q_mce_mdr_successor_minorsevaluationdeterminanthsf_prefix_bp. mdr_eb_successor_minorsevaluationdeterminanths = ff_q_mce_mdr_successor_minorsevaluationdeterminanthsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_successor_minorsevaluationdeterminanthsf_prefix)) * mdr_ec_successor_minorsevaluationdeterminanths) + (ff_bp_mce_alternating_mdr_successor_minorsevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_successor_minorsevaluationdeterminanthsf_prefix_bn. ff_h_mce_mdr_successor_minorsevaluationdeterminanthsf_prefix_bn + S (ff_bn_mce_alternating_mdr_successor_minorsevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_successor_minorsevaluationdeterminanthsf_prefix)) * mdr_fc_successor_minorsevaluationdeterminanths)) /\ exists ff_q_mce_mdr_successor_minorsevaluationdeterminanthsf_prefix_bn. mdr_fb_successor_minorsevaluationdeterminanths = ff_q_mce_mdr_successor_minorsevaluationdeterminanthsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_successor_minorsevaluationdeterminanthsf_prefix)) * mdr_fc_successor_minorsevaluationdeterminanths) + (ff_bn_mce_alternating_mdr_successor_minorsevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_successor_minorsevaluationdeterminanthsf_prefix_positive. ff_h_mce_mdr_successor_minorsevaluationdeterminanthsf_prefix_positive + S (ff_p_mce_alternating_mdr_successor_minorsevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_successor_minorsevaluationdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_successor_minorsevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_successor_minorsevaluationdeterminanthsf_prefix_positive. ff_ub_mce_fold_mdr_successor_minorsevaluationdeterminanthsf = ff_q_mce_mdr_successor_minorsevaluationdeterminanthsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_successor_minorsevaluationdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_successor_minorsevaluationdeterminanthsf) + (ff_p_mce_alternating_mdr_successor_minorsevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_successor_minorsevaluationdeterminanthsf_prefix_negative. ff_h_mce_mdr_successor_minorsevaluationdeterminanthsf_prefix_negative + S (ff_n_mce_alternating_mdr_successor_minorsevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_successor_minorsevaluationdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_successor_minorsevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_successor_minorsevaluationdeterminanthsf_prefix_negative. ff_vb_mce_fold_mdr_successor_minorsevaluationdeterminanthsf = ff_q_mce_mdr_successor_minorsevaluationdeterminanthsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_successor_minorsevaluationdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_successor_minorsevaluationdeterminanthsf) + (ff_n_mce_alternating_mdr_successor_minorsevaluationdeterminanthsf_prefix))) /\ (((exists ff_even_mce_term_mdr_successor_minorsevaluationdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_successor_minorsevaluationdeterminanthsf_prefix = 2 * ff_even_mce_term_mdr_successor_minorsevaluationdeterminanthsf_prefix_term) /\ (ff_p_mce_alternating_mdr_successor_minorsevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_successor_minorsevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_successor_minorsevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_successor_minorsevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_successor_minorsevaluationdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_successor_minorsevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_successor_minorsevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_successor_minorsevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_successor_minorsevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_successor_minorsevaluationdeterminanthsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_successor_minorsevaluationdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_successor_minorsevaluationdeterminanthsf_prefix = 2 * ff_odd_mce_term_mdr_successor_minorsevaluationdeterminanthsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_successor_minorsevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_successor_minorsevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_successor_minorsevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_successor_minorsevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_successor_minorsevaluationdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_successor_minorsevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_successor_minorsevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_successor_minorsevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_successor_minorsevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_successor_minorsevaluationdeterminanthsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_successor_minorsevaluationdeterminanthsf_positive ff_v_mce_mdr_successor_minorsevaluationdeterminanthsf_positive. ((((exists ff_h_mce_mdr_successor_minorsevaluationdeterminanthsf_positive_start. ff_h_mce_mdr_successor_minorsevaluationdeterminanthsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_successor_minorsevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_successor_minorsevaluationdeterminanthsf_positive_start. ff_u_mce_mdr_successor_minorsevaluationdeterminanthsf_positive = ff_q_mce_mdr_successor_minorsevaluationdeterminanthsf_positive_start * S ((S (0)) * ff_v_mce_mdr_successor_minorsevaluationdeterminanthsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_successor_minorsevaluationdeterminanthsf_positive_terminal. ff_h_mce_mdr_successor_minorsevaluationdeterminanthsf_positive_terminal + S (mdr_p_successor_minorsevaluationdeterminanth) = S ((S ((S (mdr_q_successor_minorsevaluationdeterminanths)))) * ff_v_mce_mdr_successor_minorsevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_successor_minorsevaluationdeterminanthsf_positive_terminal. ff_u_mce_mdr_successor_minorsevaluationdeterminanthsf_positive = ff_q_mce_mdr_successor_minorsevaluationdeterminanthsf_positive_terminal * S ((S ((S (mdr_q_successor_minorsevaluationdeterminanths)))) * ff_v_mce_mdr_successor_minorsevaluationdeterminanthsf_positive) + (mdr_p_successor_minorsevaluationdeterminanth))) /\ forall ff_i_mce_mdr_successor_minorsevaluationdeterminanthsf_positive. (exists ff_lt_mce_mdr_successor_minorsevaluationdeterminanthsf_positive_bound. ff_lt_mce_mdr_successor_minorsevaluationdeterminanthsf_positive_bound + S ff_i_mce_mdr_successor_minorsevaluationdeterminanthsf_positive = (S (mdr_q_successor_minorsevaluationdeterminanths))) -> exists ff_a_mce_mdr_successor_minorsevaluationdeterminanthsf_positive ff_r_mce_mdr_successor_minorsevaluationdeterminanthsf_positive ff_s_mce_mdr_successor_minorsevaluationdeterminanthsf_positive. ((((exists ff_h_mce_mdr_successor_minorsevaluationdeterminanthsf_positive_summand. ff_h_mce_mdr_successor_minorsevaluationdeterminanthsf_positive_summand + S (ff_a_mce_mdr_successor_minorsevaluationdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_successor_minorsevaluationdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_successor_minorsevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_successor_minorsevaluationdeterminanthsf_positive_summand. ff_ub_mce_fold_mdr_successor_minorsevaluationdeterminanthsf = ff_q_mce_mdr_successor_minorsevaluationdeterminanthsf_positive_summand * S ((S (ff_i_mce_mdr_successor_minorsevaluationdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_successor_minorsevaluationdeterminanthsf) + (ff_a_mce_mdr_successor_minorsevaluationdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_successor_minorsevaluationdeterminanthsf_positive_partial. ff_h_mce_mdr_successor_minorsevaluationdeterminanthsf_positive_partial + S (ff_r_mce_mdr_successor_minorsevaluationdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_successor_minorsevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_successor_minorsevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_successor_minorsevaluationdeterminanthsf_positive_partial. ff_u_mce_mdr_successor_minorsevaluationdeterminanthsf_positive = ff_q_mce_mdr_successor_minorsevaluationdeterminanthsf_positive_partial * S ((S (ff_i_mce_mdr_successor_minorsevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_successor_minorsevaluationdeterminanthsf_positive) + (ff_r_mce_mdr_successor_minorsevaluationdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_successor_minorsevaluationdeterminanthsf_positive_successor. ff_h_mce_mdr_successor_minorsevaluationdeterminanthsf_positive_successor + S (ff_s_mce_mdr_successor_minorsevaluationdeterminanthsf_positive) = S ((S (S ff_i_mce_mdr_successor_minorsevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_successor_minorsevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_successor_minorsevaluationdeterminanthsf_positive_successor. ff_u_mce_mdr_successor_minorsevaluationdeterminanthsf_positive = ff_q_mce_mdr_successor_minorsevaluationdeterminanthsf_positive_successor * S ((S (S ff_i_mce_mdr_successor_minorsevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_successor_minorsevaluationdeterminanthsf_positive) + (ff_s_mce_mdr_successor_minorsevaluationdeterminanthsf_positive))) /\ ff_s_mce_mdr_successor_minorsevaluationdeterminanthsf_positive = ff_r_mce_mdr_successor_minorsevaluationdeterminanthsf_positive + ff_a_mce_mdr_successor_minorsevaluationdeterminanthsf_positive)))))) /\ (exists ff_u_mce_mdr_successor_minorsevaluationdeterminanthsf_negative ff_v_mce_mdr_successor_minorsevaluationdeterminanthsf_negative. ((((exists ff_h_mce_mdr_successor_minorsevaluationdeterminanthsf_negative_start. ff_h_mce_mdr_successor_minorsevaluationdeterminanthsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_successor_minorsevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_successor_minorsevaluationdeterminanthsf_negative_start. ff_u_mce_mdr_successor_minorsevaluationdeterminanthsf_negative = ff_q_mce_mdr_successor_minorsevaluationdeterminanthsf_negative_start * S ((S (0)) * ff_v_mce_mdr_successor_minorsevaluationdeterminanthsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_successor_minorsevaluationdeterminanthsf_negative_terminal. ff_h_mce_mdr_successor_minorsevaluationdeterminanthsf_negative_terminal + S (mdr_n_successor_minorsevaluationdeterminanth) = S ((S ((S (mdr_q_successor_minorsevaluationdeterminanths)))) * ff_v_mce_mdr_successor_minorsevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_successor_minorsevaluationdeterminanthsf_negative_terminal. ff_u_mce_mdr_successor_minorsevaluationdeterminanthsf_negative = ff_q_mce_mdr_successor_minorsevaluationdeterminanthsf_negative_terminal * S ((S ((S (mdr_q_successor_minorsevaluationdeterminanths)))) * ff_v_mce_mdr_successor_minorsevaluationdeterminanthsf_negative) + (mdr_n_successor_minorsevaluationdeterminanth))) /\ forall ff_i_mce_mdr_successor_minorsevaluationdeterminanthsf_negative. (exists ff_lt_mce_mdr_successor_minorsevaluationdeterminanthsf_negative_bound. ff_lt_mce_mdr_successor_minorsevaluationdeterminanthsf_negative_bound + S ff_i_mce_mdr_successor_minorsevaluationdeterminanthsf_negative = (S (mdr_q_successor_minorsevaluationdeterminanths))) -> exists ff_a_mce_mdr_successor_minorsevaluationdeterminanthsf_negative ff_r_mce_mdr_successor_minorsevaluationdeterminanthsf_negative ff_s_mce_mdr_successor_minorsevaluationdeterminanthsf_negative. ((((exists ff_h_mce_mdr_successor_minorsevaluationdeterminanthsf_negative_summand. ff_h_mce_mdr_successor_minorsevaluationdeterminanthsf_negative_summand + S (ff_a_mce_mdr_successor_minorsevaluationdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_successor_minorsevaluationdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_successor_minorsevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_successor_minorsevaluationdeterminanthsf_negative_summand. ff_vb_mce_fold_mdr_successor_minorsevaluationdeterminanthsf = ff_q_mce_mdr_successor_minorsevaluationdeterminanthsf_negative_summand * S ((S (ff_i_mce_mdr_successor_minorsevaluationdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_successor_minorsevaluationdeterminanthsf) + (ff_a_mce_mdr_successor_minorsevaluationdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_successor_minorsevaluationdeterminanthsf_negative_partial. ff_h_mce_mdr_successor_minorsevaluationdeterminanthsf_negative_partial + S (ff_r_mce_mdr_successor_minorsevaluationdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_successor_minorsevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_successor_minorsevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_successor_minorsevaluationdeterminanthsf_negative_partial. ff_u_mce_mdr_successor_minorsevaluationdeterminanthsf_negative = ff_q_mce_mdr_successor_minorsevaluationdeterminanthsf_negative_partial * S ((S (ff_i_mce_mdr_successor_minorsevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_successor_minorsevaluationdeterminanthsf_negative) + (ff_r_mce_mdr_successor_minorsevaluationdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_successor_minorsevaluationdeterminanthsf_negative_successor. ff_h_mce_mdr_successor_minorsevaluationdeterminanthsf_negative_successor + S (ff_s_mce_mdr_successor_minorsevaluationdeterminanthsf_negative) = S ((S (S ff_i_mce_mdr_successor_minorsevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_successor_minorsevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_successor_minorsevaluationdeterminanthsf_negative_successor. ff_u_mce_mdr_successor_minorsevaluationdeterminanthsf_negative = ff_q_mce_mdr_successor_minorsevaluationdeterminanthsf_negative_successor * S ((S (S ff_i_mce_mdr_successor_minorsevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_successor_minorsevaluationdeterminanthsf_negative) + (ff_s_mce_mdr_successor_minorsevaluationdeterminanthsf_negative))) /\ ff_s_mce_mdr_successor_minorsevaluationdeterminanthsf_negative = ff_r_mce_mdr_successor_minorsevaluationdeterminanthsf_negative + ff_a_mce_mdr_successor_minorsevaluationdeterminanthsf_negative))))))))))))))) /\ ((exists mdr_gap_successor_minorsevaluationdeterminanti. mdr_gap_successor_minorsevaluationdeterminanti + S (mdr_i_successor_minorsevaluationdeterminant) = (mdr_l_successor_minorsevaluationdeterminant)) /\ (exists mdr_z_successor_minorsevaluationdeterminantr. ((exists mdr_a_successor_minorsevaluationdeterminantrc mdr_b_successor_minorsevaluationdeterminantrc mdr_c_successor_minorsevaluationdeterminantrc mdr_e_successor_minorsevaluationdeterminantrc mdr_f_successor_minorsevaluationdeterminantrc. ((mdr_a_successor_minorsevaluationdeterminantrc = ((S rank) + (mdr_ub_successor_minorsevaluation)) * S ((S rank) + (mdr_ub_successor_minorsevaluation)) + ((mdr_ub_successor_minorsevaluation) + (mdr_ub_successor_minorsevaluation))) /\ ((mdr_b_successor_minorsevaluationdeterminantrc = ((mdr_uc_successor_minorsevaluation) + (mdr_vb_successor_minorsevaluation)) * S ((mdr_uc_successor_minorsevaluation) + (mdr_vb_successor_minorsevaluation)) + ((mdr_vb_successor_minorsevaluation) + (mdr_vb_successor_minorsevaluation))) /\ ((mdr_c_successor_minorsevaluationdeterminantrc = ((mdr_a_successor_minorsevaluationdeterminantrc) + (mdr_b_successor_minorsevaluationdeterminantrc)) * S ((mdr_a_successor_minorsevaluationdeterminantrc) + (mdr_b_successor_minorsevaluationdeterminantrc)) + ((mdr_b_successor_minorsevaluationdeterminantrc) + (mdr_b_successor_minorsevaluationdeterminantrc))) /\ ((mdr_e_successor_minorsevaluationdeterminantrc = ((mdr_p_successor_minors) + (mdr_n_successor_minors)) * S ((mdr_p_successor_minors) + (mdr_n_successor_minors)) + ((mdr_n_successor_minors) + (mdr_n_successor_minors))) /\ ((mdr_f_successor_minorsevaluationdeterminantrc = ((mdr_vc_successor_minorsevaluation) + (mdr_e_successor_minorsevaluationdeterminantrc)) * S ((mdr_vc_successor_minorsevaluation) + (mdr_e_successor_minorsevaluationdeterminantrc)) + ((mdr_e_successor_minorsevaluationdeterminantrc) + (mdr_e_successor_minorsevaluationdeterminantrc))) /\ ((mdr_z_successor_minorsevaluationdeterminantr) = ((mdr_c_successor_minorsevaluationdeterminantrc) + (mdr_f_successor_minorsevaluationdeterminantrc)) * S ((mdr_c_successor_minorsevaluationdeterminantrc) + (mdr_f_successor_minorsevaluationdeterminantrc)) + ((mdr_f_successor_minorsevaluationdeterminantrc) + (mdr_f_successor_minorsevaluationdeterminantrc))))))))) /\ (((exists ff_h_mdr_successor_minorsevaluationdeterminantrb. ff_h_mdr_successor_minorsevaluationdeterminantrb + S (mdr_z_successor_minorsevaluationdeterminantr) = S ((S (mdr_i_successor_minorsevaluationdeterminant)) * mdr_c_successor_minorsevaluationdeterminant)) /\ exists ff_q_mdr_successor_minorsevaluationdeterminantrb. mdr_b_successor_minorsevaluationdeterminant = ff_q_mdr_successor_minorsevaluationdeterminantrb * S ((S (mdr_i_successor_minorsevaluationdeterminant)) * mdr_c_successor_minorsevaluationdeterminant) + (mdr_z_successor_minorsevaluationdeterminantr)))))))))) -> mdr_p_successor_minors = mdr_n_successor_minors)Constructive proof overview
Generated structural guide
In particular, every actual minor of order rank plus one vanishes, with no choice of selector or determinant history left implicit.
The unchanged tactic script uses 1 declared prerequisite and contains 15 exact native proof lines.
Alpha v34 checked-use · first admitted v27 · independently kernel and Lean verified; not Stable
Proof neighborhood
Direct dependencies
le_refl Stable theorem; checked-use authorizedDirect dependents
none
Formal native tactic body
Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.
Read the argument
Proof checkpoints
This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.