rectangular_matrix_rank_zero_rows

forall pb pc nb nc w. (((exists mdr_gap_zero_rows_rankrows_bound. mdr_gap_zero_rows_rankrows_bound + (0) = (0)) /\ ((exists mdr_gap_zero_rows_rankcolumns_bound. mdr_gap_zero_rows_rankcolumns_bound + (0) = (w)) /\ ((exists mdr_rb_zero_rows_rankwitness mdr_rc_zero_rows_rankwitness mdr_cb_zero_rows_rankwitness mdr_cc_zero_rows_rankwitness. (((((forall fom_index_mrf_zero_rows_rankwitnessminorrowsbound. (exists fom_gap_mrf_zero_rows_rankwitnessminorrowsbound_index_bound. fom_gap_mrf_zero_rows_rankwitnessminorrowsbound_index_bound + S (fom_index_mrf_zero_rows_rankwitnessminorrowsbound) = 0) -> exists fom_value_mrf_zero_rows_rankwitnessminorrowsbound. ((((exists fom_beta_height_mrf_zero_rows_rankwitnessminorrowsbound_entry. fom_beta_height_mrf_zero_rows_rankwitnessminorrowsbound_entry + S (fom_value_mrf_zero_rows_rankwitnessminorrowsbound) = S ((S (fom_index_mrf_zero_rows_rankwitnessminorrowsbound)) * mdr_rc_zero_rows_rankwitness)) /\ exists fom_beta_quotient_mrf_zero_rows_rankwitnessminorrowsbound_entry. mdr_rb_zero_rows_rankwitness = fom_beta_quotient_mrf_zero_rows_rankwitnessminorrowsbound_entry * S ((S (fom_index_mrf_zero_rows_rankwitnessminorrowsbound)) * mdr_rc_zero_rows_rankwitness) + (fom_value_mrf_zero_rows_rankwitnessminorrowsbound))) /\ (exists fom_gap_mrf_zero_rows_rankwitnessminorrowsbound_value_bound. fom_gap_mrf_zero_rows_rankwitnessminorrowsbound_value_bound + S (fom_value_mrf_zero_rows_rankwitnessminorrowsbound) = 0))) /\ (forall mdr_i_zero_rows_rankwitnessminorrowsdistinct mdr_j_zero_rows_rankwitnessminorrowsdistinct mdr_a_zero_rows_rankwitnessminorrowsdistinct. (exists mdr_gap_zero_rows_rankwitnessminorrowsdistincti. mdr_gap_zero_rows_rankwitnessminorrowsdistincti + S (mdr_i_zero_rows_rankwitnessminorrowsdistinct) = (0)) -> (exists mdr_gap_zero_rows_rankwitnessminorrowsdistinctj. mdr_gap_zero_rows_rankwitnessminorrowsdistinctj + S (mdr_j_zero_rows_rankwitnessminorrowsdistinct) = (0)) -> (((exists ff_h_mdr_zero_rows_rankwitnessminorrowsdistinctfirst. ff_h_mdr_zero_rows_rankwitnessminorrowsdistinctfirst + S (mdr_a_zero_rows_rankwitnessminorrowsdistinct) = S ((S (mdr_i_zero_rows_rankwitnessminorrowsdistinct)) * mdr_rc_zero_rows_rankwitness)) /\ exists ff_q_mdr_zero_rows_rankwitnessminorrowsdistinctfirst. mdr_rb_zero_rows_rankwitness = ff_q_mdr_zero_rows_rankwitnessminorrowsdistinctfirst * S ((S (mdr_i_zero_rows_rankwitnessminorrowsdistinct)) * mdr_rc_zero_rows_rankwitness) + (mdr_a_zero_rows_rankwitnessminorrowsdistinct))) -> (((exists ff_h_mdr_zero_rows_rankwitnessminorrowsdistinctsecond. ff_h_mdr_zero_rows_rankwitnessminorrowsdistinctsecond + S (mdr_a_zero_rows_rankwitnessminorrowsdistinct) = S ((S (mdr_j_zero_rows_rankwitnessminorrowsdistinct)) * mdr_rc_zero_rows_rankwitness)) /\ exists ff_q_mdr_zero_rows_rankwitnessminorrowsdistinctsecond. mdr_rb_zero_rows_rankwitness = ff_q_mdr_zero_rows_rankwitnessminorrowsdistinctsecond * S ((S (mdr_j_zero_rows_rankwitnessminorrowsdistinct)) * mdr_rc_zero_rows_rankwitness) + (mdr_a_zero_rows_rankwitnessminorrowsdistinct))) -> mdr_i_zero_rows_rankwitnessminorrowsdistinct = mdr_j_zero_rows_rankwitnessminorrowsdistinct))) /\ ((((forall fom_index_mrf_zero_rows_rankwitnessminorcolumnsbound. (exists fom_gap_mrf_zero_rows_rankwitnessminorcolumnsbound_index_bound. fom_gap_mrf_zero_rows_rankwitnessminorcolumnsbound_index_bound + S (fom_index_mrf_zero_rows_rankwitnessminorcolumnsbound) = 0) -> exists fom_value_mrf_zero_rows_rankwitnessminorcolumnsbound. ((((exists fom_beta_height_mrf_zero_rows_rankwitnessminorcolumnsbound_entry. fom_beta_height_mrf_zero_rows_rankwitnessminorcolumnsbound_entry + S (fom_value_mrf_zero_rows_rankwitnessminorcolumnsbound) = S ((S (fom_index_mrf_zero_rows_rankwitnessminorcolumnsbound)) * mdr_cc_zero_rows_rankwitness)) /\ exists fom_beta_quotient_mrf_zero_rows_rankwitnessminorcolumnsbound_entry. mdr_cb_zero_rows_rankwitness = fom_beta_quotient_mrf_zero_rows_rankwitnessminorcolumnsbound_entry * S ((S (fom_index_mrf_zero_rows_rankwitnessminorcolumnsbound)) * mdr_cc_zero_rows_rankwitness) + (fom_value_mrf_zero_rows_rankwitnessminorcolumnsbound))) /\ (exists fom_gap_mrf_zero_rows_rankwitnessminorcolumnsbound_value_bound. fom_gap_mrf_zero_rows_rankwitnessminorcolumnsbound_value_bound + S (fom_value_mrf_zero_rows_rankwitnessminorcolumnsbound) = w))) /\ (forall mdr_i_zero_rows_rankwitnessminorcolumnsdistinct mdr_j_zero_rows_rankwitnessminorcolumnsdistinct mdr_a_zero_rows_rankwitnessminorcolumnsdistinct. (exists mdr_gap_zero_rows_rankwitnessminorcolumnsdistincti. mdr_gap_zero_rows_rankwitnessminorcolumnsdistincti + S (mdr_i_zero_rows_rankwitnessminorcolumnsdistinct) = (0)) -> (exists mdr_gap_zero_rows_rankwitnessminorcolumnsdistinctj. mdr_gap_zero_rows_rankwitnessminorcolumnsdistinctj + S (mdr_j_zero_rows_rankwitnessminorcolumnsdistinct) = (0)) -> (((exists ff_h_mdr_zero_rows_rankwitnessminorcolumnsdistinctfirst. ff_h_mdr_zero_rows_rankwitnessminorcolumnsdistinctfirst + S (mdr_a_zero_rows_rankwitnessminorcolumnsdistinct) = S ((S (mdr_i_zero_rows_rankwitnessminorcolumnsdistinct)) * mdr_cc_zero_rows_rankwitness)) /\ exists ff_q_mdr_zero_rows_rankwitnessminorcolumnsdistinctfirst. mdr_cb_zero_rows_rankwitness = ff_q_mdr_zero_rows_rankwitnessminorcolumnsdistinctfirst * S ((S (mdr_i_zero_rows_rankwitnessminorcolumnsdistinct)) * mdr_cc_zero_rows_rankwitness) + (mdr_a_zero_rows_rankwitnessminorcolumnsdistinct))) -> (((exists ff_h_mdr_zero_rows_rankwitnessminorcolumnsdistinctsecond. ff_h_mdr_zero_rows_rankwitnessminorcolumnsdistinctsecond + S (mdr_a_zero_rows_rankwitnessminorcolumnsdistinct) = S ((S (mdr_j_zero_rows_rankwitnessminorcolumnsdistinct)) * mdr_cc_zero_rows_rankwitness)) /\ exists ff_q_mdr_zero_rows_rankwitnessminorcolumnsdistinctsecond. mdr_cb_zero_rows_rankwitness = ff_q_mdr_zero_rows_rankwitnessminorcolumnsdistinctsecond * S ((S (mdr_j_zero_rows_rankwitnessminorcolumnsdistinct)) * mdr_cc_zero_rows_rankwitness) + (mdr_a_zero_rows_rankwitnessminorcolumnsdistinct))) -> mdr_i_zero_rows_rankwitnessminorcolumnsdistinct = mdr_j_zero_rows_rankwitnessminorcolumnsdistinct))) /\ (exists mdr_p_zero_rows_rankwitnessminornonzero mdr_n_zero_rows_rankwitnessminornonzero. ((exists mdr_ub_zero_rows_rankwitnessminornonzeroevaluation mdr_uc_zero_rows_rankwitnessminornonzeroevaluation mdr_vb_zero_rows_rankwitnessminornonzeroevaluation mdr_vc_zero_rows_rankwitnessminornonzeroevaluation. ((((forall mdr_i_zero_rows_rankwitnessminornonzeroevaluationmatrixpositive. (exists mdr_gap_zero_rows_rankwitnessminornonzeroevaluationmatrixpositivebound. mdr_gap_zero_rows_rankwitnessminornonzeroevaluationmatrixpositivebound + S (mdr_i_zero_rows_rankwitnessminornonzeroevaluationmatrixpositive) = ((0) * (0))) -> exists mdr_a_zero_rows_rankwitnessminornonzeroevaluationmatrixpositive. (((exists mdr_r_zero_rows_rankwitnessminornonzeroevaluationmatrixpositivepoint mdr_s_zero_rows_rankwitnessminornonzeroevaluationmatrixpositivepoint mdr_u_zero_rows_rankwitnessminornonzeroevaluationmatrixpositivepoint mdr_v_zero_rows_rankwitnessminornonzeroevaluationmatrixpositivepoint. ((mdr_i_zero_rows_rankwitnessminornonzeroevaluationmatrixpositive = (0) * mdr_r_zero_rows_rankwitnessminornonzeroevaluationmatrixpositivepoint + mdr_s_zero_rows_rankwitnessminornonzeroevaluationmatrixpositivepoint) /\ ((exists mdr_gap_zero_rows_rankwitnessminornonzeroevaluationmatrixpositivepointcolumn. mdr_gap_zero_rows_rankwitnessminornonzeroevaluationmatrixpositivepointcolumn + S (mdr_s_zero_rows_rankwitnessminornonzeroevaluationmatrixpositivepoint) = (0)) /\ ((((exists ff_h_mdr_zero_rows_rankwitnessminornonzeroevaluationmatrixpositivepointrow_index. ff_h_mdr_zero_rows_rankwitnessminornonzeroevaluationmatrixpositivepointrow_index + S (mdr_u_zero_rows_rankwitnessminornonzeroevaluationmatrixpositivepoint) = S ((S (mdr_r_zero_rows_rankwitnessminornonzeroevaluationmatrixpositivepoint)) * mdr_rc_zero_rows_rankwitness)) /\ exists ff_q_mdr_zero_rows_rankwitnessminornonzeroevaluationmatrixpositivepointrow_index. mdr_rb_zero_rows_rankwitness = ff_q_mdr_zero_rows_rankwitnessminornonzeroevaluationmatrixpositivepointrow_index * S ((S (mdr_r_zero_rows_rankwitnessminornonzeroevaluationmatrixpositivepoint)) * mdr_rc_zero_rows_rankwitness) + (mdr_u_zero_rows_rankwitnessminornonzeroevaluationmatrixpositivepoint))) /\ ((((exists ff_h_mdr_zero_rows_rankwitnessminornonzeroevaluationmatrixpositivepointcolumn_index. ff_h_mdr_zero_rows_rankwitnessminornonzeroevaluationmatrixpositivepointcolumn_index + S (mdr_v_zero_rows_rankwitnessminornonzeroevaluationmatrixpositivepoint) = S ((S (mdr_s_zero_rows_rankwitnessminornonzeroevaluationmatrixpositivepoint)) * mdr_cc_zero_rows_rankwitness)) /\ exists ff_q_mdr_zero_rows_rankwitnessminornonzeroevaluationmatrixpositivepointcolumn_index. mdr_cb_zero_rows_rankwitness = ff_q_mdr_zero_rows_rankwitnessminornonzeroevaluationmatrixpositivepointcolumn_index * S ((S (mdr_s_zero_rows_rankwitnessminornonzeroevaluationmatrixpositivepoint)) * mdr_cc_zero_rows_rankwitness) + (mdr_v_zero_rows_rankwitnessminornonzeroevaluationmatrixpositivepoint))) /\ (((exists ff_h_mdr_zero_rows_rankwitnessminornonzeroevaluationmatrixpositivepointsource. ff_h_mdr_zero_rows_rankwitnessminornonzeroevaluationmatrixpositivepointsource + S (mdr_a_zero_rows_rankwitnessminornonzeroevaluationmatrixpositive) = S ((S ((mdr_u_zero_rows_rankwitnessminornonzeroevaluationmatrixpositivepoint) * (w) + (mdr_v_zero_rows_rankwitnessminornonzeroevaluationmatrixpositivepoint))) * pc)) /\ exists ff_q_mdr_zero_rows_rankwitnessminornonzeroevaluationmatrixpositivepointsource. pb = ff_q_mdr_zero_rows_rankwitnessminornonzeroevaluationmatrixpositivepointsource * S ((S ((mdr_u_zero_rows_rankwitnessminornonzeroevaluationmatrixpositivepoint) * (w) + (mdr_v_zero_rows_rankwitnessminornonzeroevaluationmatrixpositivepoint))) * pc) + (mdr_a_zero_rows_rankwitnessminornonzeroevaluationmatrixpositive)))))))) /\ (((exists ff_h_mdr_zero_rows_rankwitnessminornonzeroevaluationmatrixpositiveoutput. ff_h_mdr_zero_rows_rankwitnessminornonzeroevaluationmatrixpositiveoutput + S (mdr_a_zero_rows_rankwitnessminornonzeroevaluationmatrixpositive) = S ((S (mdr_i_zero_rows_rankwitnessminornonzeroevaluationmatrixpositive)) * mdr_uc_zero_rows_rankwitnessminornonzeroevaluation)) /\ exists ff_q_mdr_zero_rows_rankwitnessminornonzeroevaluationmatrixpositiveoutput. mdr_ub_zero_rows_rankwitnessminornonzeroevaluation = ff_q_mdr_zero_rows_rankwitnessminornonzeroevaluationmatrixpositiveoutput * S ((S (mdr_i_zero_rows_rankwitnessminornonzeroevaluationmatrixpositive)) * mdr_uc_zero_rows_rankwitnessminornonzeroevaluation) + (mdr_a_zero_rows_rankwitnessminornonzeroevaluationmatrixpositive)))))) /\ (forall mdr_i_zero_rows_rankwitnessminornonzeroevaluationmatrixnegative. (exists mdr_gap_zero_rows_rankwitnessminornonzeroevaluationmatrixnegativebound. mdr_gap_zero_rows_rankwitnessminornonzeroevaluationmatrixnegativebound + S (mdr_i_zero_rows_rankwitnessminornonzeroevaluationmatrixnegative) = ((0) * (0))) -> exists mdr_a_zero_rows_rankwitnessminornonzeroevaluationmatrixnegative. (((exists mdr_r_zero_rows_rankwitnessminornonzeroevaluationmatrixnegativepoint mdr_s_zero_rows_rankwitnessminornonzeroevaluationmatrixnegativepoint mdr_u_zero_rows_rankwitnessminornonzeroevaluationmatrixnegativepoint mdr_v_zero_rows_rankwitnessminornonzeroevaluationmatrixnegativepoint. ((mdr_i_zero_rows_rankwitnessminornonzeroevaluationmatrixnegative = (0) * mdr_r_zero_rows_rankwitnessminornonzeroevaluationmatrixnegativepoint + mdr_s_zero_rows_rankwitnessminornonzeroevaluationmatrixnegativepoint) /\ ((exists mdr_gap_zero_rows_rankwitnessminornonzeroevaluationmatrixnegativepointcolumn. mdr_gap_zero_rows_rankwitnessminornonzeroevaluationmatrixnegativepointcolumn + S (mdr_s_zero_rows_rankwitnessminornonzeroevaluationmatrixnegativepoint) = (0)) /\ ((((exists ff_h_mdr_zero_rows_rankwitnessminornonzeroevaluationmatrixnegativepointrow_index. ff_h_mdr_zero_rows_rankwitnessminornonzeroevaluationmatrixnegativepointrow_index + S (mdr_u_zero_rows_rankwitnessminornonzeroevaluationmatrixnegativepoint) = S ((S (mdr_r_zero_rows_rankwitnessminornonzeroevaluationmatrixnegativepoint)) * mdr_rc_zero_rows_rankwitness)) /\ exists ff_q_mdr_zero_rows_rankwitnessminornonzeroevaluationmatrixnegativepointrow_index. mdr_rb_zero_rows_rankwitness = ff_q_mdr_zero_rows_rankwitnessminornonzeroevaluationmatrixnegativepointrow_index * S ((S (mdr_r_zero_rows_rankwitnessminornonzeroevaluationmatrixnegativepoint)) * mdr_rc_zero_rows_rankwitness) + (mdr_u_zero_rows_rankwitnessminornonzeroevaluationmatrixnegativepoint))) /\ ((((exists ff_h_mdr_zero_rows_rankwitnessminornonzeroevaluationmatrixnegativepointcolumn_index. ff_h_mdr_zero_rows_rankwitnessminornonzeroevaluationmatrixnegativepointcolumn_index + S (mdr_v_zero_rows_rankwitnessminornonzeroevaluationmatrixnegativepoint) = S ((S (mdr_s_zero_rows_rankwitnessminornonzeroevaluationmatrixnegativepoint)) * mdr_cc_zero_rows_rankwitness)) /\ exists ff_q_mdr_zero_rows_rankwitnessminornonzeroevaluationmatrixnegativepointcolumn_index. mdr_cb_zero_rows_rankwitness = ff_q_mdr_zero_rows_rankwitnessminornonzeroevaluationmatrixnegativepointcolumn_index * S ((S (mdr_s_zero_rows_rankwitnessminornonzeroevaluationmatrixnegativepoint)) * mdr_cc_zero_rows_rankwitness) + (mdr_v_zero_rows_rankwitnessminornonzeroevaluationmatrixnegativepoint))) /\ (((exists ff_h_mdr_zero_rows_rankwitnessminornonzeroevaluationmatrixnegativepointsource. ff_h_mdr_zero_rows_rankwitnessminornonzeroevaluationmatrixnegativepointsource + S (mdr_a_zero_rows_rankwitnessminornonzeroevaluationmatrixnegative) = S ((S ((mdr_u_zero_rows_rankwitnessminornonzeroevaluationmatrixnegativepoint) * (w) + (mdr_v_zero_rows_rankwitnessminornonzeroevaluationmatrixnegativepoint))) * nc)) /\ exists ff_q_mdr_zero_rows_rankwitnessminornonzeroevaluationmatrixnegativepointsource. nb = ff_q_mdr_zero_rows_rankwitnessminornonzeroevaluationmatrixnegativepointsource * S ((S ((mdr_u_zero_rows_rankwitnessminornonzeroevaluationmatrixnegativepoint) * (w) + (mdr_v_zero_rows_rankwitnessminornonzeroevaluationmatrixnegativepoint))) * nc) + (mdr_a_zero_rows_rankwitnessminornonzeroevaluationmatrixnegative)))))))) /\ (((exists ff_h_mdr_zero_rows_rankwitnessminornonzeroevaluationmatrixnegativeoutput. ff_h_mdr_zero_rows_rankwitnessminornonzeroevaluationmatrixnegativeoutput + S (mdr_a_zero_rows_rankwitnessminornonzeroevaluationmatrixnegative) = S ((S (mdr_i_zero_rows_rankwitnessminornonzeroevaluationmatrixnegative)) * mdr_vc_zero_rows_rankwitnessminornonzeroevaluation)) /\ exists ff_q_mdr_zero_rows_rankwitnessminornonzeroevaluationmatrixnegativeoutput. mdr_vb_zero_rows_rankwitnessminornonzeroevaluation = ff_q_mdr_zero_rows_rankwitnessminornonzeroevaluationmatrixnegativeoutput * S ((S (mdr_i_zero_rows_rankwitnessminornonzeroevaluationmatrixnegative)) * mdr_vc_zero_rows_rankwitnessminornonzeroevaluation) + (mdr_a_zero_rows_rankwitnessminornonzeroevaluationmatrixnegative)))))))) /\ (exists mdr_b_zero_rows_rankwitnessminornonzeroevaluationdeterminant mdr_c_zero_rows_rankwitnessminornonzeroevaluationdeterminant mdr_l_zero_rows_rankwitnessminornonzeroevaluationdeterminant mdr_i_zero_rows_rankwitnessminornonzeroevaluationdeterminant. ((forall mdr_i_zero_rows_rankwitnessminornonzeroevaluationdeterminanth. (exists mdr_gap_zero_rows_rankwitnessminornonzeroevaluationdeterminanthi. mdr_gap_zero_rows_rankwitnessminornonzeroevaluationdeterminanthi + S (mdr_i_zero_rows_rankwitnessminornonzeroevaluationdeterminanth) = (mdr_l_zero_rows_rankwitnessminornonzeroevaluationdeterminant)) -> exists mdr_d_zero_rows_rankwitnessminornonzeroevaluationdeterminanth mdr_pb_zero_rows_rankwitnessminornonzeroevaluationdeterminanth mdr_pc_zero_rows_rankwitnessminornonzeroevaluationdeterminanth mdr_nb_zero_rows_rankwitnessminornonzeroevaluationdeterminanth mdr_nc_zero_rows_rankwitnessminornonzeroevaluationdeterminanth mdr_p_zero_rows_rankwitnessminornonzeroevaluationdeterminanth mdr_n_zero_rows_rankwitnessminornonzeroevaluationdeterminanth. ((exists mdr_z_zero_rows_rankwitnessminornonzeroevaluationdeterminanthr. ((exists mdr_a_zero_rows_rankwitnessminornonzeroevaluationdeterminanthrc mdr_b_zero_rows_rankwitnessminornonzeroevaluationdeterminanthrc mdr_c_zero_rows_rankwitnessminornonzeroevaluationdeterminanthrc mdr_e_zero_rows_rankwitnessminornonzeroevaluationdeterminanthrc mdr_f_zero_rows_rankwitnessminornonzeroevaluationdeterminanthrc. ((mdr_a_zero_rows_rankwitnessminornonzeroevaluationdeterminanthrc = ((mdr_d_zero_rows_rankwitnessminornonzeroevaluationdeterminanth) + (mdr_pb_zero_rows_rankwitnessminornonzeroevaluationdeterminanth)) * S ((mdr_d_zero_rows_rankwitnessminornonzeroevaluationdeterminanth) + (mdr_pb_zero_rows_rankwitnessminornonzeroevaluationdeterminanth)) + ((mdr_pb_zero_rows_rankwitnessminornonzeroevaluationdeterminanth) + (mdr_pb_zero_rows_rankwitnessminornonzeroevaluationdeterminanth))) /\ ((mdr_b_zero_rows_rankwitnessminornonzeroevaluationdeterminanthrc = ((mdr_pc_zero_rows_rankwitnessminornonzeroevaluationdeterminanth) + (mdr_nb_zero_rows_rankwitnessminornonzeroevaluationdeterminanth)) * S ((mdr_pc_zero_rows_rankwitnessminornonzeroevaluationdeterminanth) + (mdr_nb_zero_rows_rankwitnessminornonzeroevaluationdeterminanth)) + ((mdr_nb_zero_rows_rankwitnessminornonzeroevaluationdeterminanth) + (mdr_nb_zero_rows_rankwitnessminornonzeroevaluationdeterminanth))) /\ ((mdr_c_zero_rows_rankwitnessminornonzeroevaluationdeterminanthrc = ((mdr_a_zero_rows_rankwitnessminornonzeroevaluationdeterminanthrc) + (mdr_b_zero_rows_rankwitnessminornonzeroevaluationdeterminanthrc)) * S ((mdr_a_zero_rows_rankwitnessminornonzeroevaluationdeterminanthrc) + (mdr_b_zero_rows_rankwitnessminornonzeroevaluationdeterminanthrc)) + ((mdr_b_zero_rows_rankwitnessminornonzeroevaluationdeterminanthrc) + (mdr_b_zero_rows_rankwitnessminornonzeroevaluationdeterminanthrc))) /\ ((mdr_e_zero_rows_rankwitnessminornonzeroevaluationdeterminanthrc = ((mdr_p_zero_rows_rankwitnessminornonzeroevaluationdeterminanth) + (mdr_n_zero_rows_rankwitnessminornonzeroevaluationdeterminanth)) * S ((mdr_p_zero_rows_rankwitnessminornonzeroevaluationdeterminanth) + (mdr_n_zero_rows_rankwitnessminornonzeroevaluationdeterminanth)) + ((mdr_n_zero_rows_rankwitnessminornonzeroevaluationdeterminanth) + (mdr_n_zero_rows_rankwitnessminornonzeroevaluationdeterminanth))) /\ ((mdr_f_zero_rows_rankwitnessminornonzeroevaluationdeterminanthrc = ((mdr_nc_zero_rows_rankwitnessminornonzeroevaluationdeterminanth) + (mdr_e_zero_rows_rankwitnessminornonzeroevaluationdeterminanthrc)) * S ((mdr_nc_zero_rows_rankwitnessminornonzeroevaluationdeterminanth) + (mdr_e_zero_rows_rankwitnessminornonzeroevaluationdeterminanthrc)) + ((mdr_e_zero_rows_rankwitnessminornonzeroevaluationdeterminanthrc) + (mdr_e_zero_rows_rankwitnessminornonzeroevaluationdeterminanthrc))) /\ ((mdr_z_zero_rows_rankwitnessminornonzeroevaluationdeterminanthr) = ((mdr_c_zero_rows_rankwitnessminornonzeroevaluationdeterminanthrc) + (mdr_f_zero_rows_rankwitnessminornonzeroevaluationdeterminanthrc)) * S ((mdr_c_zero_rows_rankwitnessminornonzeroevaluationdeterminanthrc) + (mdr_f_zero_rows_rankwitnessminornonzeroevaluationdeterminanthrc)) + ((mdr_f_zero_rows_rankwitnessminornonzeroevaluationdeterminanthrc) + (mdr_f_zero_rows_rankwitnessminornonzeroevaluationdeterminanthrc))))))))) /\ (((exists ff_h_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthrb. ff_h_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthrb + S (mdr_z_zero_rows_rankwitnessminornonzeroevaluationdeterminanthr) = S ((S (mdr_i_zero_rows_rankwitnessminornonzeroevaluationdeterminanth)) * mdr_c_zero_rows_rankwitnessminornonzeroevaluationdeterminant)) /\ exists ff_q_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthrb. mdr_b_zero_rows_rankwitnessminornonzeroevaluationdeterminant = ff_q_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthrb * S ((S (mdr_i_zero_rows_rankwitnessminornonzeroevaluationdeterminanth)) * mdr_c_zero_rows_rankwitnessminornonzeroevaluationdeterminant) + (mdr_z_zero_rows_rankwitnessminornonzeroevaluationdeterminanthr))))) /\ (((((mdr_d_zero_rows_rankwitnessminornonzeroevaluationdeterminanth) = 0) /\ (((mdr_p_zero_rows_rankwitnessminornonzeroevaluationdeterminanth) = 1) /\ ((mdr_n_zero_rows_rankwitnessminornonzeroevaluationdeterminanth) = 0))) \/ exists mdr_q_zero_rows_rankwitnessminornonzeroevaluationdeterminanths mdr_eb_zero_rows_rankwitnessminornonzeroevaluationdeterminanths mdr_ec_zero_rows_rankwitnessminornonzeroevaluationdeterminanths mdr_fb_zero_rows_rankwitnessminornonzeroevaluationdeterminanths mdr_fc_zero_rows_rankwitnessminornonzeroevaluationdeterminanths. (((mdr_d_zero_rows_rankwitnessminornonzeroevaluationdeterminanth) = S (mdr_q_zero_rows_rankwitnessminornonzeroevaluationdeterminanths)) /\ ((forall mdr_j_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsc. (exists mdr_gap_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscj. mdr_gap_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscj + S (mdr_j_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsc) = (S (mdr_q_zero_rows_rankwitnessminornonzeroevaluationdeterminanths))) -> exists mdr_i_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsc mdr_up_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsc mdr_us_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsc mdr_un_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsc mdr_ut_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsc mdr_p_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsc mdr_n_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsc. ((exists mdr_gap_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsci. mdr_gap_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsci + S (mdr_i_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsc) = (mdr_i_zero_rows_rankwitnessminornonzeroevaluationdeterminanth)) /\ ((exists mdr_z_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscr. ((exists mdr_a_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscrc mdr_b_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscrc mdr_c_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscrc mdr_e_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscrc mdr_f_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscrc. ((mdr_a_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscrc = ((mdr_q_zero_rows_rankwitnessminornonzeroevaluationdeterminanths) + (mdr_up_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsc)) * S ((mdr_q_zero_rows_rankwitnessminornonzeroevaluationdeterminanths) + (mdr_up_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsc)) + ((mdr_up_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsc) + (mdr_up_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsc))) /\ ((mdr_b_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscrc = ((mdr_us_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsc) + (mdr_un_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsc)) * S ((mdr_us_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsc) + (mdr_un_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsc)) + ((mdr_un_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsc) + (mdr_un_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsc))) /\ ((mdr_c_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscrc = ((mdr_a_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscrc) + (mdr_b_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscrc)) * S ((mdr_a_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscrc) + (mdr_b_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscrc)) + ((mdr_b_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscrc) + (mdr_b_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscrc))) /\ ((mdr_e_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscrc = ((mdr_p_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsc) + (mdr_n_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsc)) * S ((mdr_p_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsc) + (mdr_n_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsc)) + ((mdr_n_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsc) + (mdr_n_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsc))) /\ ((mdr_f_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscrc = ((mdr_ut_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsc) + (mdr_e_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscrc)) * S ((mdr_ut_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsc) + (mdr_e_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscrc)) + ((mdr_e_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscrc) + (mdr_e_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscrc))) /\ ((mdr_z_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscr) = ((mdr_c_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscrc) + (mdr_f_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscrc)) * S ((mdr_c_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscrc) + (mdr_f_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscrc)) + ((mdr_f_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscrc) + (mdr_f_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscrc))))))))) /\ (((exists ff_h_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscrb. ff_h_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscrb + S (mdr_z_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscr) = S ((S (mdr_i_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsc)) * mdr_c_zero_rows_rankwitnessminornonzeroevaluationdeterminant)) /\ exists ff_q_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscrb. mdr_b_zero_rows_rankwitnessminornonzeroevaluationdeterminant = ff_q_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscrb * S ((S (mdr_i_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsc)) * mdr_c_zero_rows_rankwitnessminornonzeroevaluationdeterminant) + (mdr_z_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscm_positive. (exists ff_gap_mdm_lt_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscm_positive_index_bound. ff_gap_mdm_lt_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscm_positive) = ((mdr_q_zero_rows_rankwitnessminornonzeroevaluationdeterminanths) * (mdr_q_zero_rows_rankwitnessminornonzeroevaluationdeterminanths))) -> exists ff_row_mdm_prefix_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscm_positive ff_column_mdm_prefix_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscm_positive ff_value_mdm_prefix_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscm_positive. (ff_index_mdm_prefix_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscm_positive = (mdr_q_zero_rows_rankwitnessminornonzeroevaluationdeterminanths) * ff_row_mdm_prefix_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscm_positive + ff_column_mdm_prefix_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscm_positive /\ ((exists ff_gap_mdm_lt_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscm_positive_column_bound. ff_gap_mdm_lt_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscm_positive) = (mdr_q_zero_rows_rankwitnessminornonzeroevaluationdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell ff_column_mdm_cell_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell = ff_row_mdm_prefix_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell_row_after. ff_gap_mdm_le_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscm_positive)) /\ ff_row_mdm_cell_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell = S ff_row_mdm_prefix_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscm_positive) = (mdr_j_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsc)) /\ ff_column_mdm_cell_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell = ff_column_mdm_prefix_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell_column_after. ff_gap_mdm_le_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell_column_after + (mdr_j_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsc) = (ff_column_mdm_prefix_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscm_positive)) /\ ff_column_mdm_cell_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell = S ff_column_mdm_prefix_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscm_positive))) /\ (((exists ff_h_mdm_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell_source. ff_h_mdm_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscm_positive) = S ((S ((ff_row_mdm_cell_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell) * (S (mdr_q_zero_rows_rankwitnessminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell))) * mdr_pc_zero_rows_rankwitnessminornonzeroevaluationdeterminanth)) /\ exists ff_q_mdm_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell_source. mdr_pb_zero_rows_rankwitnessminornonzeroevaluationdeterminanth = ff_q_mdm_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell) * (S (mdr_q_zero_rows_rankwitnessminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell))) * mdr_pc_zero_rows_rankwitnessminornonzeroevaluationdeterminanth) + (ff_value_mdm_prefix_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscm_positive)))))) /\ (((exists ff_h_mdm_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscm_positive_target. ff_h_mdm_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscm_positive_target + S (ff_value_mdm_prefix_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscm_positive) = S ((S (ff_index_mdm_prefix_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscm_positive)) * mdr_us_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsc)) /\ exists ff_q_mdm_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscm_positive_target. mdr_up_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsc = ff_q_mdm_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscm_positive)) * mdr_us_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsc) + (ff_value_mdm_prefix_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscm_negative. (exists ff_gap_mdm_lt_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscm_negative_index_bound. ff_gap_mdm_lt_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscm_negative) = ((mdr_q_zero_rows_rankwitnessminornonzeroevaluationdeterminanths) * (mdr_q_zero_rows_rankwitnessminornonzeroevaluationdeterminanths))) -> exists ff_row_mdm_prefix_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscm_negative ff_column_mdm_prefix_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscm_negative ff_value_mdm_prefix_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscm_negative. (ff_index_mdm_prefix_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscm_negative = (mdr_q_zero_rows_rankwitnessminornonzeroevaluationdeterminanths) * ff_row_mdm_prefix_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscm_negative + ff_column_mdm_prefix_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscm_negative /\ ((exists ff_gap_mdm_lt_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscm_negative_column_bound. ff_gap_mdm_lt_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscm_negative) = (mdr_q_zero_rows_rankwitnessminornonzeroevaluationdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell ff_column_mdm_cell_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell = ff_row_mdm_prefix_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell_row_after. ff_gap_mdm_le_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscm_negative)) /\ ff_row_mdm_cell_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell = S ff_row_mdm_prefix_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscm_negative) = (mdr_j_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsc)) /\ ff_column_mdm_cell_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell = ff_column_mdm_prefix_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell_column_after. ff_gap_mdm_le_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell_column_after + (mdr_j_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsc) = (ff_column_mdm_prefix_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscm_negative)) /\ ff_column_mdm_cell_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell = S ff_column_mdm_prefix_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscm_negative))) /\ (((exists ff_h_mdm_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell_source. ff_h_mdm_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscm_negative) = S ((S ((ff_row_mdm_cell_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell) * (S (mdr_q_zero_rows_rankwitnessminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell))) * mdr_nc_zero_rows_rankwitnessminornonzeroevaluationdeterminanth)) /\ exists ff_q_mdm_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell_source. mdr_nb_zero_rows_rankwitnessminornonzeroevaluationdeterminanth = ff_q_mdm_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell) * (S (mdr_q_zero_rows_rankwitnessminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell))) * mdr_nc_zero_rows_rankwitnessminornonzeroevaluationdeterminanth) + (ff_value_mdm_prefix_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscm_negative)))))) /\ (((exists ff_h_mdm_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscm_negative_target. ff_h_mdm_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscm_negative_target + S (ff_value_mdm_prefix_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscm_negative) = S ((S (ff_index_mdm_prefix_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscm_negative)) * mdr_ut_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsc)) /\ exists ff_q_mdm_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscm_negative_target. mdr_un_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsc = ff_q_mdm_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscm_negative)) * mdr_ut_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsc) + (ff_value_mdm_prefix_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscm_negative))))))))) /\ ((((exists ff_h_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscp. ff_h_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscp + S (mdr_p_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsc) = S ((S (mdr_j_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsc)) * mdr_ec_zero_rows_rankwitnessminornonzeroevaluationdeterminanths)) /\ exists ff_q_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscp. mdr_eb_zero_rows_rankwitnessminornonzeroevaluationdeterminanths = ff_q_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscp * S ((S (mdr_j_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsc)) * mdr_ec_zero_rows_rankwitnessminornonzeroevaluationdeterminanths) + (mdr_p_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsc))) /\ (((exists ff_h_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscn. ff_h_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscn + S (mdr_n_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsc) = S ((S (mdr_j_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsc)) * mdr_fc_zero_rows_rankwitnessminornonzeroevaluationdeterminanths)) /\ exists ff_q_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscn. mdr_fb_zero_rows_rankwitnessminornonzeroevaluationdeterminanths = ff_q_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthscn * S ((S (mdr_j_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsc)) * mdr_fc_zero_rows_rankwitnessminornonzeroevaluationdeterminanths) + (mdr_n_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsc)))))))) /\ (exists ff_ub_mce_fold_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf ff_uc_mce_fold_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf ff_vb_mce_fold_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf ff_vc_mce_fold_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf. ((forall ff_index_mce_alternating_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_prefix. (exists ff_gap_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_index. ff_gap_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_index + S (ff_index_mce_alternating_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) = (S (mdr_q_zero_rows_rankwitnessminornonzeroevaluationdeterminanths))) -> exists ff_ap_mce_alternating_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_prefix ff_an_mce_alternating_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_prefix ff_bp_mce_alternating_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_prefix ff_bn_mce_alternating_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_prefix ff_p_mce_alternating_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_prefix ff_n_mce_alternating_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_prefix. ((((exists ff_h_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_ap. ff_h_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_ap + S (ff_ap_mce_alternating_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_prefix)) * mdr_pc_zero_rows_rankwitnessminornonzeroevaluationdeterminanth)) /\ exists ff_q_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_ap. mdr_pb_zero_rows_rankwitnessminornonzeroevaluationdeterminanth = ff_q_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_prefix)) * mdr_pc_zero_rows_rankwitnessminornonzeroevaluationdeterminanth) + (ff_ap_mce_alternating_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_an. ff_h_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_an + S (ff_an_mce_alternating_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_prefix)) * mdr_nc_zero_rows_rankwitnessminornonzeroevaluationdeterminanth)) /\ exists ff_q_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_an. mdr_nb_zero_rows_rankwitnessminornonzeroevaluationdeterminanth = ff_q_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_prefix)) * mdr_nc_zero_rows_rankwitnessminornonzeroevaluationdeterminanth) + (ff_an_mce_alternating_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_bp. ff_h_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_bp + S (ff_bp_mce_alternating_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_prefix)) * mdr_ec_zero_rows_rankwitnessminornonzeroevaluationdeterminanths)) /\ exists ff_q_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_bp. mdr_eb_zero_rows_rankwitnessminornonzeroevaluationdeterminanths = ff_q_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_prefix)) * mdr_ec_zero_rows_rankwitnessminornonzeroevaluationdeterminanths) + (ff_bp_mce_alternating_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_bn. ff_h_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_bn + S (ff_bn_mce_alternating_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_prefix)) * mdr_fc_zero_rows_rankwitnessminornonzeroevaluationdeterminanths)) /\ exists ff_q_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_bn. mdr_fb_zero_rows_rankwitnessminornonzeroevaluationdeterminanths = ff_q_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_prefix)) * mdr_fc_zero_rows_rankwitnessminornonzeroevaluationdeterminanths) + (ff_bn_mce_alternating_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_positive. ff_h_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_positive + S (ff_p_mce_alternating_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_positive. ff_ub_mce_fold_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf) + (ff_p_mce_alternating_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_negative. ff_h_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_negative + S (ff_n_mce_alternating_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_negative. ff_vb_mce_fold_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf) + (ff_n_mce_alternating_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_prefix))) /\ (((exists ff_even_mce_term_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_prefix = 2 * ff_even_mce_term_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_term) /\ (ff_p_mce_alternating_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_prefix = 2 * ff_odd_mce_term_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_positive ff_v_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_positive. ((((exists ff_h_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_positive_start. ff_h_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_positive_start. ff_u_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_positive_start * S ((S (0)) * ff_v_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_positive_terminal. ff_h_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_positive_terminal + S (mdr_p_zero_rows_rankwitnessminornonzeroevaluationdeterminanth) = S ((S ((S (mdr_q_zero_rows_rankwitnessminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_positive_terminal. ff_u_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_positive_terminal * S ((S ((S (mdr_q_zero_rows_rankwitnessminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_positive) + (mdr_p_zero_rows_rankwitnessminornonzeroevaluationdeterminanth))) /\ forall ff_i_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_positive. (exists ff_lt_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_positive_bound. ff_lt_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_positive_bound + S ff_i_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_positive = (S (mdr_q_zero_rows_rankwitnessminornonzeroevaluationdeterminanths))) -> exists ff_a_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_positive ff_r_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_positive ff_s_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_positive. ((((exists ff_h_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_positive_summand. ff_h_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_positive_summand + S (ff_a_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_positive_summand. ff_ub_mce_fold_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_positive_summand * S ((S (ff_i_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf) + (ff_a_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_positive_partial. ff_h_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_positive_partial + S (ff_r_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_positive_partial. ff_u_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_positive_partial * S ((S (ff_i_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_positive) + (ff_r_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_positive_successor. ff_h_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_positive_successor + S (ff_s_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_positive) = S ((S (S ff_i_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_positive_successor. ff_u_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_positive_successor * S ((S (S ff_i_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_positive) + (ff_s_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_positive))) /\ ff_s_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_positive = ff_r_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_positive + ff_a_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_positive)))))) /\ (exists ff_u_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_negative ff_v_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_negative. ((((exists ff_h_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_negative_start. ff_h_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_negative_start. ff_u_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_negative_start * S ((S (0)) * ff_v_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_negative_terminal. ff_h_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_negative_terminal + S (mdr_n_zero_rows_rankwitnessminornonzeroevaluationdeterminanth) = S ((S ((S (mdr_q_zero_rows_rankwitnessminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_negative_terminal. ff_u_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_negative_terminal * S ((S ((S (mdr_q_zero_rows_rankwitnessminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_negative) + (mdr_n_zero_rows_rankwitnessminornonzeroevaluationdeterminanth))) /\ forall ff_i_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_negative. (exists ff_lt_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_negative_bound. ff_lt_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_negative_bound + S ff_i_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_negative = (S (mdr_q_zero_rows_rankwitnessminornonzeroevaluationdeterminanths))) -> exists ff_a_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_negative ff_r_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_negative ff_s_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_negative. ((((exists ff_h_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_negative_summand. ff_h_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_negative_summand + S (ff_a_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_negative_summand. ff_vb_mce_fold_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_negative_summand * S ((S (ff_i_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf) + (ff_a_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_negative_partial. ff_h_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_negative_partial + S (ff_r_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_negative_partial. ff_u_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_negative_partial * S ((S (ff_i_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_negative) + (ff_r_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_negative_successor. ff_h_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_negative_successor + S (ff_s_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_negative) = S ((S (S ff_i_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_negative_successor. ff_u_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_negative_successor * S ((S (S ff_i_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_negative) + (ff_s_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_negative))) /\ ff_s_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_negative = ff_r_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_negative + ff_a_mce_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminanthsf_negative))))))))))))))) /\ ((exists mdr_gap_zero_rows_rankwitnessminornonzeroevaluationdeterminanti. mdr_gap_zero_rows_rankwitnessminornonzeroevaluationdeterminanti + S (mdr_i_zero_rows_rankwitnessminornonzeroevaluationdeterminant) = (mdr_l_zero_rows_rankwitnessminornonzeroevaluationdeterminant)) /\ (exists mdr_z_zero_rows_rankwitnessminornonzeroevaluationdeterminantr. ((exists mdr_a_zero_rows_rankwitnessminornonzeroevaluationdeterminantrc mdr_b_zero_rows_rankwitnessminornonzeroevaluationdeterminantrc mdr_c_zero_rows_rankwitnessminornonzeroevaluationdeterminantrc mdr_e_zero_rows_rankwitnessminornonzeroevaluationdeterminantrc mdr_f_zero_rows_rankwitnessminornonzeroevaluationdeterminantrc. ((mdr_a_zero_rows_rankwitnessminornonzeroevaluationdeterminantrc = ((0) + (mdr_ub_zero_rows_rankwitnessminornonzeroevaluation)) * S ((0) + (mdr_ub_zero_rows_rankwitnessminornonzeroevaluation)) + ((mdr_ub_zero_rows_rankwitnessminornonzeroevaluation) + (mdr_ub_zero_rows_rankwitnessminornonzeroevaluation))) /\ ((mdr_b_zero_rows_rankwitnessminornonzeroevaluationdeterminantrc = ((mdr_uc_zero_rows_rankwitnessminornonzeroevaluation) + (mdr_vb_zero_rows_rankwitnessminornonzeroevaluation)) * S ((mdr_uc_zero_rows_rankwitnessminornonzeroevaluation) + (mdr_vb_zero_rows_rankwitnessminornonzeroevaluation)) + ((mdr_vb_zero_rows_rankwitnessminornonzeroevaluation) + (mdr_vb_zero_rows_rankwitnessminornonzeroevaluation))) /\ ((mdr_c_zero_rows_rankwitnessminornonzeroevaluationdeterminantrc = ((mdr_a_zero_rows_rankwitnessminornonzeroevaluationdeterminantrc) + (mdr_b_zero_rows_rankwitnessminornonzeroevaluationdeterminantrc)) * S ((mdr_a_zero_rows_rankwitnessminornonzeroevaluationdeterminantrc) + (mdr_b_zero_rows_rankwitnessminornonzeroevaluationdeterminantrc)) + ((mdr_b_zero_rows_rankwitnessminornonzeroevaluationdeterminantrc) + (mdr_b_zero_rows_rankwitnessminornonzeroevaluationdeterminantrc))) /\ ((mdr_e_zero_rows_rankwitnessminornonzeroevaluationdeterminantrc = ((mdr_p_zero_rows_rankwitnessminornonzero) + (mdr_n_zero_rows_rankwitnessminornonzero)) * S ((mdr_p_zero_rows_rankwitnessminornonzero) + (mdr_n_zero_rows_rankwitnessminornonzero)) + ((mdr_n_zero_rows_rankwitnessminornonzero) + (mdr_n_zero_rows_rankwitnessminornonzero))) /\ ((mdr_f_zero_rows_rankwitnessminornonzeroevaluationdeterminantrc = ((mdr_vc_zero_rows_rankwitnessminornonzeroevaluation) + (mdr_e_zero_rows_rankwitnessminornonzeroevaluationdeterminantrc)) * S ((mdr_vc_zero_rows_rankwitnessminornonzeroevaluation) + (mdr_e_zero_rows_rankwitnessminornonzeroevaluationdeterminantrc)) + ((mdr_e_zero_rows_rankwitnessminornonzeroevaluationdeterminantrc) + (mdr_e_zero_rows_rankwitnessminornonzeroevaluationdeterminantrc))) /\ ((mdr_z_zero_rows_rankwitnessminornonzeroevaluationdeterminantr) = ((mdr_c_zero_rows_rankwitnessminornonzeroevaluationdeterminantrc) + (mdr_f_zero_rows_rankwitnessminornonzeroevaluationdeterminantrc)) * S ((mdr_c_zero_rows_rankwitnessminornonzeroevaluationdeterminantrc) + (mdr_f_zero_rows_rankwitnessminornonzeroevaluationdeterminantrc)) + ((mdr_f_zero_rows_rankwitnessminornonzeroevaluationdeterminantrc) + (mdr_f_zero_rows_rankwitnessminornonzeroevaluationdeterminantrc))))))))) /\ (((exists ff_h_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminantrb. ff_h_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminantrb + S (mdr_z_zero_rows_rankwitnessminornonzeroevaluationdeterminantr) = S ((S (mdr_i_zero_rows_rankwitnessminornonzeroevaluationdeterminant)) * mdr_c_zero_rows_rankwitnessminornonzeroevaluationdeterminant)) /\ exists ff_q_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminantrb. mdr_b_zero_rows_rankwitnessminornonzeroevaluationdeterminant = ff_q_mdr_zero_rows_rankwitnessminornonzeroevaluationdeterminantrb * S ((S (mdr_i_zero_rows_rankwitnessminornonzeroevaluationdeterminant)) * mdr_c_zero_rows_rankwitnessminornonzeroevaluationdeterminant) + (mdr_z_zero_rows_rankwitnessminornonzeroevaluationdeterminantr)))))))))) /\ (~(mdr_p_zero_rows_rankwitnessminornonzero = mdr_n_zero_rows_rankwitnessminornonzero)))))))) /\ (forall mdr_q_zero_rows_rank. (exists mdr_gap_zero_rows_rankhigher. mdr_gap_zero_rows_rankhigher + S (0) = (mdr_q_zero_rows_rank)) -> (forall mdr_rb_zero_rows_rankzero mdr_rc_zero_rows_rankzero mdr_cb_zero_rows_rankzero mdr_cc_zero_rows_rankzero mdr_p_zero_rows_rankzero mdr_n_zero_rows_rankzero. (((forall fom_index_mrf_zero_rows_rankzerorowsbound. (exists fom_gap_mrf_zero_rows_rankzerorowsbound_index_bound. fom_gap_mrf_zero_rows_rankzerorowsbound_index_bound + S (fom_index_mrf_zero_rows_rankzerorowsbound) = mdr_q_zero_rows_rank) -> exists fom_value_mrf_zero_rows_rankzerorowsbound. ((((exists fom_beta_height_mrf_zero_rows_rankzerorowsbound_entry. fom_beta_height_mrf_zero_rows_rankzerorowsbound_entry + S (fom_value_mrf_zero_rows_rankzerorowsbound) = S ((S (fom_index_mrf_zero_rows_rankzerorowsbound)) * mdr_rc_zero_rows_rankzero)) /\ exists fom_beta_quotient_mrf_zero_rows_rankzerorowsbound_entry. mdr_rb_zero_rows_rankzero = fom_beta_quotient_mrf_zero_rows_rankzerorowsbound_entry * S ((S (fom_index_mrf_zero_rows_rankzerorowsbound)) * mdr_rc_zero_rows_rankzero) + (fom_value_mrf_zero_rows_rankzerorowsbound))) /\ (exists fom_gap_mrf_zero_rows_rankzerorowsbound_value_bound. fom_gap_mrf_zero_rows_rankzerorowsbound_value_bound + S (fom_value_mrf_zero_rows_rankzerorowsbound) = 0))) /\ (forall mdr_i_zero_rows_rankzerorowsdistinct mdr_j_zero_rows_rankzerorowsdistinct mdr_a_zero_rows_rankzerorowsdistinct. (exists mdr_gap_zero_rows_rankzerorowsdistincti. mdr_gap_zero_rows_rankzerorowsdistincti + S (mdr_i_zero_rows_rankzerorowsdistinct) = (mdr_q_zero_rows_rank)) -> (exists mdr_gap_zero_rows_rankzerorowsdistinctj. mdr_gap_zero_rows_rankzerorowsdistinctj + S (mdr_j_zero_rows_rankzerorowsdistinct) = (mdr_q_zero_rows_rank)) -> (((exists ff_h_mdr_zero_rows_rankzerorowsdistinctfirst. ff_h_mdr_zero_rows_rankzerorowsdistinctfirst + S (mdr_a_zero_rows_rankzerorowsdistinct) = S ((S (mdr_i_zero_rows_rankzerorowsdistinct)) * mdr_rc_zero_rows_rankzero)) /\ exists ff_q_mdr_zero_rows_rankzerorowsdistinctfirst. mdr_rb_zero_rows_rankzero = ff_q_mdr_zero_rows_rankzerorowsdistinctfirst * S ((S (mdr_i_zero_rows_rankzerorowsdistinct)) * mdr_rc_zero_rows_rankzero) + (mdr_a_zero_rows_rankzerorowsdistinct))) -> (((exists ff_h_mdr_zero_rows_rankzerorowsdistinctsecond. ff_h_mdr_zero_rows_rankzerorowsdistinctsecond + S (mdr_a_zero_rows_rankzerorowsdistinct) = S ((S (mdr_j_zero_rows_rankzerorowsdistinct)) * mdr_rc_zero_rows_rankzero)) /\ exists ff_q_mdr_zero_rows_rankzerorowsdistinctsecond. mdr_rb_zero_rows_rankzero = ff_q_mdr_zero_rows_rankzerorowsdistinctsecond * S ((S (mdr_j_zero_rows_rankzerorowsdistinct)) * mdr_rc_zero_rows_rankzero) + (mdr_a_zero_rows_rankzerorowsdistinct))) -> mdr_i_zero_rows_rankzerorowsdistinct = mdr_j_zero_rows_rankzerorowsdistinct))) -> (((forall fom_index_mrf_zero_rows_rankzerocolumnsbound. (exists fom_gap_mrf_zero_rows_rankzerocolumnsbound_index_bound. fom_gap_mrf_zero_rows_rankzerocolumnsbound_index_bound + S (fom_index_mrf_zero_rows_rankzerocolumnsbound) = mdr_q_zero_rows_rank) -> exists fom_value_mrf_zero_rows_rankzerocolumnsbound. ((((exists fom_beta_height_mrf_zero_rows_rankzerocolumnsbound_entry. fom_beta_height_mrf_zero_rows_rankzerocolumnsbound_entry + S (fom_value_mrf_zero_rows_rankzerocolumnsbound) = S ((S (fom_index_mrf_zero_rows_rankzerocolumnsbound)) * mdr_cc_zero_rows_rankzero)) /\ exists fom_beta_quotient_mrf_zero_rows_rankzerocolumnsbound_entry. mdr_cb_zero_rows_rankzero = fom_beta_quotient_mrf_zero_rows_rankzerocolumnsbound_entry * S ((S (fom_index_mrf_zero_rows_rankzerocolumnsbound)) * mdr_cc_zero_rows_rankzero) + (fom_value_mrf_zero_rows_rankzerocolumnsbound))) /\ (exists fom_gap_mrf_zero_rows_rankzerocolumnsbound_value_bound. fom_gap_mrf_zero_rows_rankzerocolumnsbound_value_bound + S (fom_value_mrf_zero_rows_rankzerocolumnsbound) = w))) /\ (forall mdr_i_zero_rows_rankzerocolumnsdistinct mdr_j_zero_rows_rankzerocolumnsdistinct mdr_a_zero_rows_rankzerocolumnsdistinct. (exists mdr_gap_zero_rows_rankzerocolumnsdistincti. mdr_gap_zero_rows_rankzerocolumnsdistincti + S (mdr_i_zero_rows_rankzerocolumnsdistinct) = (mdr_q_zero_rows_rank)) -> (exists mdr_gap_zero_rows_rankzerocolumnsdistinctj. mdr_gap_zero_rows_rankzerocolumnsdistinctj + S (mdr_j_zero_rows_rankzerocolumnsdistinct) = (mdr_q_zero_rows_rank)) -> (((exists ff_h_mdr_zero_rows_rankzerocolumnsdistinctfirst. ff_h_mdr_zero_rows_rankzerocolumnsdistinctfirst + S (mdr_a_zero_rows_rankzerocolumnsdistinct) = S ((S (mdr_i_zero_rows_rankzerocolumnsdistinct)) * mdr_cc_zero_rows_rankzero)) /\ exists ff_q_mdr_zero_rows_rankzerocolumnsdistinctfirst. mdr_cb_zero_rows_rankzero = ff_q_mdr_zero_rows_rankzerocolumnsdistinctfirst * S ((S (mdr_i_zero_rows_rankzerocolumnsdistinct)) * mdr_cc_zero_rows_rankzero) + (mdr_a_zero_rows_rankzerocolumnsdistinct))) -> (((exists ff_h_mdr_zero_rows_rankzerocolumnsdistinctsecond. ff_h_mdr_zero_rows_rankzerocolumnsdistinctsecond + S (mdr_a_zero_rows_rankzerocolumnsdistinct) = S ((S (mdr_j_zero_rows_rankzerocolumnsdistinct)) * mdr_cc_zero_rows_rankzero)) /\ exists ff_q_mdr_zero_rows_rankzerocolumnsdistinctsecond. mdr_cb_zero_rows_rankzero = ff_q_mdr_zero_rows_rankzerocolumnsdistinctsecond * S ((S (mdr_j_zero_rows_rankzerocolumnsdistinct)) * mdr_cc_zero_rows_rankzero) + (mdr_a_zero_rows_rankzerocolumnsdistinct))) -> mdr_i_zero_rows_rankzerocolumnsdistinct = mdr_j_zero_rows_rankzerocolumnsdistinct))) -> (exists mdr_ub_zero_rows_rankzeroevaluation mdr_uc_zero_rows_rankzeroevaluation mdr_vb_zero_rows_rankzeroevaluation mdr_vc_zero_rows_rankzeroevaluation. ((((forall mdr_i_zero_rows_rankzeroevaluationmatrixpositive. (exists mdr_gap_zero_rows_rankzeroevaluationmatrixpositivebound. mdr_gap_zero_rows_rankzeroevaluationmatrixpositivebound + S (mdr_i_zero_rows_rankzeroevaluationmatrixpositive) = ((mdr_q_zero_rows_rank) * (mdr_q_zero_rows_rank))) -> exists mdr_a_zero_rows_rankzeroevaluationmatrixpositive. (((exists mdr_r_zero_rows_rankzeroevaluationmatrixpositivepoint mdr_s_zero_rows_rankzeroevaluationmatrixpositivepoint mdr_u_zero_rows_rankzeroevaluationmatrixpositivepoint mdr_v_zero_rows_rankzeroevaluationmatrixpositivepoint. ((mdr_i_zero_rows_rankzeroevaluationmatrixpositive = (mdr_q_zero_rows_rank) * mdr_r_zero_rows_rankzeroevaluationmatrixpositivepoint + mdr_s_zero_rows_rankzeroevaluationmatrixpositivepoint) /\ ((exists mdr_gap_zero_rows_rankzeroevaluationmatrixpositivepointcolumn. mdr_gap_zero_rows_rankzeroevaluationmatrixpositivepointcolumn + S (mdr_s_zero_rows_rankzeroevaluationmatrixpositivepoint) = (mdr_q_zero_rows_rank)) /\ ((((exists ff_h_mdr_zero_rows_rankzeroevaluationmatrixpositivepointrow_index. ff_h_mdr_zero_rows_rankzeroevaluationmatrixpositivepointrow_index + S (mdr_u_zero_rows_rankzeroevaluationmatrixpositivepoint) = S ((S (mdr_r_zero_rows_rankzeroevaluationmatrixpositivepoint)) * mdr_rc_zero_rows_rankzero)) /\ exists ff_q_mdr_zero_rows_rankzeroevaluationmatrixpositivepointrow_index. mdr_rb_zero_rows_rankzero = ff_q_mdr_zero_rows_rankzeroevaluationmatrixpositivepointrow_index * S ((S (mdr_r_zero_rows_rankzeroevaluationmatrixpositivepoint)) * mdr_rc_zero_rows_rankzero) + (mdr_u_zero_rows_rankzeroevaluationmatrixpositivepoint))) /\ ((((exists ff_h_mdr_zero_rows_rankzeroevaluationmatrixpositivepointcolumn_index. ff_h_mdr_zero_rows_rankzeroevaluationmatrixpositivepointcolumn_index + S (mdr_v_zero_rows_rankzeroevaluationmatrixpositivepoint) = S ((S (mdr_s_zero_rows_rankzeroevaluationmatrixpositivepoint)) * mdr_cc_zero_rows_rankzero)) /\ exists ff_q_mdr_zero_rows_rankzeroevaluationmatrixpositivepointcolumn_index. mdr_cb_zero_rows_rankzero = ff_q_mdr_zero_rows_rankzeroevaluationmatrixpositivepointcolumn_index * S ((S (mdr_s_zero_rows_rankzeroevaluationmatrixpositivepoint)) * mdr_cc_zero_rows_rankzero) + (mdr_v_zero_rows_rankzeroevaluationmatrixpositivepoint))) /\ (((exists ff_h_mdr_zero_rows_rankzeroevaluationmatrixpositivepointsource. ff_h_mdr_zero_rows_rankzeroevaluationmatrixpositivepointsource + S (mdr_a_zero_rows_rankzeroevaluationmatrixpositive) = S ((S ((mdr_u_zero_rows_rankzeroevaluationmatrixpositivepoint) * (w) + (mdr_v_zero_rows_rankzeroevaluationmatrixpositivepoint))) * pc)) /\ exists ff_q_mdr_zero_rows_rankzeroevaluationmatrixpositivepointsource. pb = ff_q_mdr_zero_rows_rankzeroevaluationmatrixpositivepointsource * S ((S ((mdr_u_zero_rows_rankzeroevaluationmatrixpositivepoint) * (w) + (mdr_v_zero_rows_rankzeroevaluationmatrixpositivepoint))) * pc) + (mdr_a_zero_rows_rankzeroevaluationmatrixpositive)))))))) /\ (((exists ff_h_mdr_zero_rows_rankzeroevaluationmatrixpositiveoutput. ff_h_mdr_zero_rows_rankzeroevaluationmatrixpositiveoutput + S (mdr_a_zero_rows_rankzeroevaluationmatrixpositive) = S ((S (mdr_i_zero_rows_rankzeroevaluationmatrixpositive)) * mdr_uc_zero_rows_rankzeroevaluation)) /\ exists ff_q_mdr_zero_rows_rankzeroevaluationmatrixpositiveoutput. mdr_ub_zero_rows_rankzeroevaluation = ff_q_mdr_zero_rows_rankzeroevaluationmatrixpositiveoutput * S ((S (mdr_i_zero_rows_rankzeroevaluationmatrixpositive)) * mdr_uc_zero_rows_rankzeroevaluation) + (mdr_a_zero_rows_rankzeroevaluationmatrixpositive)))))) /\ (forall mdr_i_zero_rows_rankzeroevaluationmatrixnegative. (exists mdr_gap_zero_rows_rankzeroevaluationmatrixnegativebound. mdr_gap_zero_rows_rankzeroevaluationmatrixnegativebound + S (mdr_i_zero_rows_rankzeroevaluationmatrixnegative) = ((mdr_q_zero_rows_rank) * (mdr_q_zero_rows_rank))) -> exists mdr_a_zero_rows_rankzeroevaluationmatrixnegative. (((exists mdr_r_zero_rows_rankzeroevaluationmatrixnegativepoint mdr_s_zero_rows_rankzeroevaluationmatrixnegativepoint mdr_u_zero_rows_rankzeroevaluationmatrixnegativepoint mdr_v_zero_rows_rankzeroevaluationmatrixnegativepoint. ((mdr_i_zero_rows_rankzeroevaluationmatrixnegative = (mdr_q_zero_rows_rank) * mdr_r_zero_rows_rankzeroevaluationmatrixnegativepoint + mdr_s_zero_rows_rankzeroevaluationmatrixnegativepoint) /\ ((exists mdr_gap_zero_rows_rankzeroevaluationmatrixnegativepointcolumn. mdr_gap_zero_rows_rankzeroevaluationmatrixnegativepointcolumn + S (mdr_s_zero_rows_rankzeroevaluationmatrixnegativepoint) = (mdr_q_zero_rows_rank)) /\ ((((exists ff_h_mdr_zero_rows_rankzeroevaluationmatrixnegativepointrow_index. ff_h_mdr_zero_rows_rankzeroevaluationmatrixnegativepointrow_index + S (mdr_u_zero_rows_rankzeroevaluationmatrixnegativepoint) = S ((S (mdr_r_zero_rows_rankzeroevaluationmatrixnegativepoint)) * mdr_rc_zero_rows_rankzero)) /\ exists ff_q_mdr_zero_rows_rankzeroevaluationmatrixnegativepointrow_index. mdr_rb_zero_rows_rankzero = ff_q_mdr_zero_rows_rankzeroevaluationmatrixnegativepointrow_index * S ((S (mdr_r_zero_rows_rankzeroevaluationmatrixnegativepoint)) * mdr_rc_zero_rows_rankzero) + (mdr_u_zero_rows_rankzeroevaluationmatrixnegativepoint))) /\ ((((exists ff_h_mdr_zero_rows_rankzeroevaluationmatrixnegativepointcolumn_index. ff_h_mdr_zero_rows_rankzeroevaluationmatrixnegativepointcolumn_index + S (mdr_v_zero_rows_rankzeroevaluationmatrixnegativepoint) = S ((S (mdr_s_zero_rows_rankzeroevaluationmatrixnegativepoint)) * mdr_cc_zero_rows_rankzero)) /\ exists ff_q_mdr_zero_rows_rankzeroevaluationmatrixnegativepointcolumn_index. mdr_cb_zero_rows_rankzero = ff_q_mdr_zero_rows_rankzeroevaluationmatrixnegativepointcolumn_index * S ((S (mdr_s_zero_rows_rankzeroevaluationmatrixnegativepoint)) * mdr_cc_zero_rows_rankzero) + (mdr_v_zero_rows_rankzeroevaluationmatrixnegativepoint))) /\ (((exists ff_h_mdr_zero_rows_rankzeroevaluationmatrixnegativepointsource. ff_h_mdr_zero_rows_rankzeroevaluationmatrixnegativepointsource + S (mdr_a_zero_rows_rankzeroevaluationmatrixnegative) = S ((S ((mdr_u_zero_rows_rankzeroevaluationmatrixnegativepoint) * (w) + (mdr_v_zero_rows_rankzeroevaluationmatrixnegativepoint))) * nc)) /\ exists ff_q_mdr_zero_rows_rankzeroevaluationmatrixnegativepointsource. nb = ff_q_mdr_zero_rows_rankzeroevaluationmatrixnegativepointsource * S ((S ((mdr_u_zero_rows_rankzeroevaluationmatrixnegativepoint) * (w) + (mdr_v_zero_rows_rankzeroevaluationmatrixnegativepoint))) * nc) + (mdr_a_zero_rows_rankzeroevaluationmatrixnegative)))))))) /\ (((exists ff_h_mdr_zero_rows_rankzeroevaluationmatrixnegativeoutput. ff_h_mdr_zero_rows_rankzeroevaluationmatrixnegativeoutput + S (mdr_a_zero_rows_rankzeroevaluationmatrixnegative) = S ((S (mdr_i_zero_rows_rankzeroevaluationmatrixnegative)) * mdr_vc_zero_rows_rankzeroevaluation)) /\ exists ff_q_mdr_zero_rows_rankzeroevaluationmatrixnegativeoutput. mdr_vb_zero_rows_rankzeroevaluation = ff_q_mdr_zero_rows_rankzeroevaluationmatrixnegativeoutput * S ((S (mdr_i_zero_rows_rankzeroevaluationmatrixnegative)) * mdr_vc_zero_rows_rankzeroevaluation) + (mdr_a_zero_rows_rankzeroevaluationmatrixnegative)))))))) /\ (exists mdr_b_zero_rows_rankzeroevaluationdeterminant mdr_c_zero_rows_rankzeroevaluationdeterminant mdr_l_zero_rows_rankzeroevaluationdeterminant mdr_i_zero_rows_rankzeroevaluationdeterminant. ((forall mdr_i_zero_rows_rankzeroevaluationdeterminanth. (exists mdr_gap_zero_rows_rankzeroevaluationdeterminanthi. mdr_gap_zero_rows_rankzeroevaluationdeterminanthi + S (mdr_i_zero_rows_rankzeroevaluationdeterminanth) = (mdr_l_zero_rows_rankzeroevaluationdeterminant)) -> exists mdr_d_zero_rows_rankzeroevaluationdeterminanth mdr_pb_zero_rows_rankzeroevaluationdeterminanth mdr_pc_zero_rows_rankzeroevaluationdeterminanth mdr_nb_zero_rows_rankzeroevaluationdeterminanth mdr_nc_zero_rows_rankzeroevaluationdeterminanth mdr_p_zero_rows_rankzeroevaluationdeterminanth mdr_n_zero_rows_rankzeroevaluationdeterminanth. ((exists mdr_z_zero_rows_rankzeroevaluationdeterminanthr. ((exists mdr_a_zero_rows_rankzeroevaluationdeterminanthrc mdr_b_zero_rows_rankzeroevaluationdeterminanthrc mdr_c_zero_rows_rankzeroevaluationdeterminanthrc mdr_e_zero_rows_rankzeroevaluationdeterminanthrc mdr_f_zero_rows_rankzeroevaluationdeterminanthrc. ((mdr_a_zero_rows_rankzeroevaluationdeterminanthrc = ((mdr_d_zero_rows_rankzeroevaluationdeterminanth) + (mdr_pb_zero_rows_rankzeroevaluationdeterminanth)) * S ((mdr_d_zero_rows_rankzeroevaluationdeterminanth) + (mdr_pb_zero_rows_rankzeroevaluationdeterminanth)) + ((mdr_pb_zero_rows_rankzeroevaluationdeterminanth) + (mdr_pb_zero_rows_rankzeroevaluationdeterminanth))) /\ ((mdr_b_zero_rows_rankzeroevaluationdeterminanthrc = ((mdr_pc_zero_rows_rankzeroevaluationdeterminanth) + (mdr_nb_zero_rows_rankzeroevaluationdeterminanth)) * S ((mdr_pc_zero_rows_rankzeroevaluationdeterminanth) + (mdr_nb_zero_rows_rankzeroevaluationdeterminanth)) + ((mdr_nb_zero_rows_rankzeroevaluationdeterminanth) + (mdr_nb_zero_rows_rankzeroevaluationdeterminanth))) /\ ((mdr_c_zero_rows_rankzeroevaluationdeterminanthrc = ((mdr_a_zero_rows_rankzeroevaluationdeterminanthrc) + (mdr_b_zero_rows_rankzeroevaluationdeterminanthrc)) * S ((mdr_a_zero_rows_rankzeroevaluationdeterminanthrc) + (mdr_b_zero_rows_rankzeroevaluationdeterminanthrc)) + ((mdr_b_zero_rows_rankzeroevaluationdeterminanthrc) + (mdr_b_zero_rows_rankzeroevaluationdeterminanthrc))) /\ ((mdr_e_zero_rows_rankzeroevaluationdeterminanthrc = ((mdr_p_zero_rows_rankzeroevaluationdeterminanth) + (mdr_n_zero_rows_rankzeroevaluationdeterminanth)) * S ((mdr_p_zero_rows_rankzeroevaluationdeterminanth) + (mdr_n_zero_rows_rankzeroevaluationdeterminanth)) + ((mdr_n_zero_rows_rankzeroevaluationdeterminanth) + (mdr_n_zero_rows_rankzeroevaluationdeterminanth))) /\ ((mdr_f_zero_rows_rankzeroevaluationdeterminanthrc = ((mdr_nc_zero_rows_rankzeroevaluationdeterminanth) + (mdr_e_zero_rows_rankzeroevaluationdeterminanthrc)) * S ((mdr_nc_zero_rows_rankzeroevaluationdeterminanth) + (mdr_e_zero_rows_rankzeroevaluationdeterminanthrc)) + ((mdr_e_zero_rows_rankzeroevaluationdeterminanthrc) + (mdr_e_zero_rows_rankzeroevaluationdeterminanthrc))) /\ ((mdr_z_zero_rows_rankzeroevaluationdeterminanthr) = ((mdr_c_zero_rows_rankzeroevaluationdeterminanthrc) + (mdr_f_zero_rows_rankzeroevaluationdeterminanthrc)) * S ((mdr_c_zero_rows_rankzeroevaluationdeterminanthrc) + (mdr_f_zero_rows_rankzeroevaluationdeterminanthrc)) + ((mdr_f_zero_rows_rankzeroevaluationdeterminanthrc) + (mdr_f_zero_rows_rankzeroevaluationdeterminanthrc))))))))) /\ (((exists ff_h_mdr_zero_rows_rankzeroevaluationdeterminanthrb. ff_h_mdr_zero_rows_rankzeroevaluationdeterminanthrb + S (mdr_z_zero_rows_rankzeroevaluationdeterminanthr) = S ((S (mdr_i_zero_rows_rankzeroevaluationdeterminanth)) * mdr_c_zero_rows_rankzeroevaluationdeterminant)) /\ exists ff_q_mdr_zero_rows_rankzeroevaluationdeterminanthrb. mdr_b_zero_rows_rankzeroevaluationdeterminant = ff_q_mdr_zero_rows_rankzeroevaluationdeterminanthrb * S ((S (mdr_i_zero_rows_rankzeroevaluationdeterminanth)) * mdr_c_zero_rows_rankzeroevaluationdeterminant) + (mdr_z_zero_rows_rankzeroevaluationdeterminanthr))))) /\ (((((mdr_d_zero_rows_rankzeroevaluationdeterminanth) = 0) /\ (((mdr_p_zero_rows_rankzeroevaluationdeterminanth) = 1) /\ ((mdr_n_zero_rows_rankzeroevaluationdeterminanth) = 0))) \/ exists mdr_q_zero_rows_rankzeroevaluationdeterminanths mdr_eb_zero_rows_rankzeroevaluationdeterminanths mdr_ec_zero_rows_rankzeroevaluationdeterminanths mdr_fb_zero_rows_rankzeroevaluationdeterminanths mdr_fc_zero_rows_rankzeroevaluationdeterminanths. (((mdr_d_zero_rows_rankzeroevaluationdeterminanth) = S (mdr_q_zero_rows_rankzeroevaluationdeterminanths)) /\ ((forall mdr_j_zero_rows_rankzeroevaluationdeterminanthsc. (exists mdr_gap_zero_rows_rankzeroevaluationdeterminanthscj. mdr_gap_zero_rows_rankzeroevaluationdeterminanthscj + S (mdr_j_zero_rows_rankzeroevaluationdeterminanthsc) = (S (mdr_q_zero_rows_rankzeroevaluationdeterminanths))) -> exists mdr_i_zero_rows_rankzeroevaluationdeterminanthsc mdr_up_zero_rows_rankzeroevaluationdeterminanthsc mdr_us_zero_rows_rankzeroevaluationdeterminanthsc mdr_un_zero_rows_rankzeroevaluationdeterminanthsc mdr_ut_zero_rows_rankzeroevaluationdeterminanthsc mdr_p_zero_rows_rankzeroevaluationdeterminanthsc mdr_n_zero_rows_rankzeroevaluationdeterminanthsc. ((exists mdr_gap_zero_rows_rankzeroevaluationdeterminanthsci. mdr_gap_zero_rows_rankzeroevaluationdeterminanthsci + S (mdr_i_zero_rows_rankzeroevaluationdeterminanthsc) = (mdr_i_zero_rows_rankzeroevaluationdeterminanth)) /\ ((exists mdr_z_zero_rows_rankzeroevaluationdeterminanthscr. ((exists mdr_a_zero_rows_rankzeroevaluationdeterminanthscrc mdr_b_zero_rows_rankzeroevaluationdeterminanthscrc mdr_c_zero_rows_rankzeroevaluationdeterminanthscrc mdr_e_zero_rows_rankzeroevaluationdeterminanthscrc mdr_f_zero_rows_rankzeroevaluationdeterminanthscrc. ((mdr_a_zero_rows_rankzeroevaluationdeterminanthscrc = ((mdr_q_zero_rows_rankzeroevaluationdeterminanths) + (mdr_up_zero_rows_rankzeroevaluationdeterminanthsc)) * S ((mdr_q_zero_rows_rankzeroevaluationdeterminanths) + (mdr_up_zero_rows_rankzeroevaluationdeterminanthsc)) + ((mdr_up_zero_rows_rankzeroevaluationdeterminanthsc) + (mdr_up_zero_rows_rankzeroevaluationdeterminanthsc))) /\ ((mdr_b_zero_rows_rankzeroevaluationdeterminanthscrc = ((mdr_us_zero_rows_rankzeroevaluationdeterminanthsc) + (mdr_un_zero_rows_rankzeroevaluationdeterminanthsc)) * S ((mdr_us_zero_rows_rankzeroevaluationdeterminanthsc) + (mdr_un_zero_rows_rankzeroevaluationdeterminanthsc)) + ((mdr_un_zero_rows_rankzeroevaluationdeterminanthsc) + (mdr_un_zero_rows_rankzeroevaluationdeterminanthsc))) /\ ((mdr_c_zero_rows_rankzeroevaluationdeterminanthscrc = ((mdr_a_zero_rows_rankzeroevaluationdeterminanthscrc) + (mdr_b_zero_rows_rankzeroevaluationdeterminanthscrc)) * S ((mdr_a_zero_rows_rankzeroevaluationdeterminanthscrc) + (mdr_b_zero_rows_rankzeroevaluationdeterminanthscrc)) + ((mdr_b_zero_rows_rankzeroevaluationdeterminanthscrc) + (mdr_b_zero_rows_rankzeroevaluationdeterminanthscrc))) /\ ((mdr_e_zero_rows_rankzeroevaluationdeterminanthscrc = ((mdr_p_zero_rows_rankzeroevaluationdeterminanthsc) + (mdr_n_zero_rows_rankzeroevaluationdeterminanthsc)) * S ((mdr_p_zero_rows_rankzeroevaluationdeterminanthsc) + (mdr_n_zero_rows_rankzeroevaluationdeterminanthsc)) + ((mdr_n_zero_rows_rankzeroevaluationdeterminanthsc) + (mdr_n_zero_rows_rankzeroevaluationdeterminanthsc))) /\ ((mdr_f_zero_rows_rankzeroevaluationdeterminanthscrc = ((mdr_ut_zero_rows_rankzeroevaluationdeterminanthsc) + (mdr_e_zero_rows_rankzeroevaluationdeterminanthscrc)) * S ((mdr_ut_zero_rows_rankzeroevaluationdeterminanthsc) + (mdr_e_zero_rows_rankzeroevaluationdeterminanthscrc)) + ((mdr_e_zero_rows_rankzeroevaluationdeterminanthscrc) + (mdr_e_zero_rows_rankzeroevaluationdeterminanthscrc))) /\ ((mdr_z_zero_rows_rankzeroevaluationdeterminanthscr) = ((mdr_c_zero_rows_rankzeroevaluationdeterminanthscrc) + (mdr_f_zero_rows_rankzeroevaluationdeterminanthscrc)) * S ((mdr_c_zero_rows_rankzeroevaluationdeterminanthscrc) + (mdr_f_zero_rows_rankzeroevaluationdeterminanthscrc)) + ((mdr_f_zero_rows_rankzeroevaluationdeterminanthscrc) + (mdr_f_zero_rows_rankzeroevaluationdeterminanthscrc))))))))) /\ (((exists ff_h_mdr_zero_rows_rankzeroevaluationdeterminanthscrb. ff_h_mdr_zero_rows_rankzeroevaluationdeterminanthscrb + S (mdr_z_zero_rows_rankzeroevaluationdeterminanthscr) = S ((S (mdr_i_zero_rows_rankzeroevaluationdeterminanthsc)) * mdr_c_zero_rows_rankzeroevaluationdeterminant)) /\ exists ff_q_mdr_zero_rows_rankzeroevaluationdeterminanthscrb. mdr_b_zero_rows_rankzeroevaluationdeterminant = ff_q_mdr_zero_rows_rankzeroevaluationdeterminanthscrb * S ((S (mdr_i_zero_rows_rankzeroevaluationdeterminanthsc)) * mdr_c_zero_rows_rankzeroevaluationdeterminant) + (mdr_z_zero_rows_rankzeroevaluationdeterminanthscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_zero_rows_rankzeroevaluationdeterminanthscm_positive. (exists ff_gap_mdm_lt_mdr_zero_rows_rankzeroevaluationdeterminanthscm_positive_index_bound. ff_gap_mdm_lt_mdr_zero_rows_rankzeroevaluationdeterminanthscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_zero_rows_rankzeroevaluationdeterminanthscm_positive) = ((mdr_q_zero_rows_rankzeroevaluationdeterminanths) * (mdr_q_zero_rows_rankzeroevaluationdeterminanths))) -> exists ff_row_mdm_prefix_mdr_zero_rows_rankzeroevaluationdeterminanthscm_positive ff_column_mdm_prefix_mdr_zero_rows_rankzeroevaluationdeterminanthscm_positive ff_value_mdm_prefix_mdr_zero_rows_rankzeroevaluationdeterminanthscm_positive. (ff_index_mdm_prefix_mdr_zero_rows_rankzeroevaluationdeterminanthscm_positive = (mdr_q_zero_rows_rankzeroevaluationdeterminanths) * ff_row_mdm_prefix_mdr_zero_rows_rankzeroevaluationdeterminanthscm_positive + ff_column_mdm_prefix_mdr_zero_rows_rankzeroevaluationdeterminanthscm_positive /\ ((exists ff_gap_mdm_lt_mdr_zero_rows_rankzeroevaluationdeterminanthscm_positive_column_bound. ff_gap_mdm_lt_mdr_zero_rows_rankzeroevaluationdeterminanthscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_zero_rows_rankzeroevaluationdeterminanthscm_positive) = (mdr_q_zero_rows_rankzeroevaluationdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_zero_rows_rankzeroevaluationdeterminanthscm_positive_cell ff_column_mdm_cell_mdr_zero_rows_rankzeroevaluationdeterminanthscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_zero_rows_rankzeroevaluationdeterminanthscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_zero_rows_rankzeroevaluationdeterminanthscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_zero_rows_rankzeroevaluationdeterminanthscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_zero_rows_rankzeroevaluationdeterminanthscm_positive_cell = ff_row_mdm_prefix_mdr_zero_rows_rankzeroevaluationdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_zero_rows_rankzeroevaluationdeterminanthscm_positive_cell_row_after. ff_gap_mdm_le_mdr_zero_rows_rankzeroevaluationdeterminanthscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_zero_rows_rankzeroevaluationdeterminanthscm_positive)) /\ ff_row_mdm_cell_mdr_zero_rows_rankzeroevaluationdeterminanthscm_positive_cell = S ff_row_mdm_prefix_mdr_zero_rows_rankzeroevaluationdeterminanthscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_zero_rows_rankzeroevaluationdeterminanthscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_zero_rows_rankzeroevaluationdeterminanthscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_zero_rows_rankzeroevaluationdeterminanthscm_positive) = (mdr_j_zero_rows_rankzeroevaluationdeterminanthsc)) /\ ff_column_mdm_cell_mdr_zero_rows_rankzeroevaluationdeterminanthscm_positive_cell = ff_column_mdm_prefix_mdr_zero_rows_rankzeroevaluationdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_zero_rows_rankzeroevaluationdeterminanthscm_positive_cell_column_after. ff_gap_mdm_le_mdr_zero_rows_rankzeroevaluationdeterminanthscm_positive_cell_column_after + (mdr_j_zero_rows_rankzeroevaluationdeterminanthsc) = (ff_column_mdm_prefix_mdr_zero_rows_rankzeroevaluationdeterminanthscm_positive)) /\ ff_column_mdm_cell_mdr_zero_rows_rankzeroevaluationdeterminanthscm_positive_cell = S ff_column_mdm_prefix_mdr_zero_rows_rankzeroevaluationdeterminanthscm_positive))) /\ (((exists ff_h_mdm_mdr_zero_rows_rankzeroevaluationdeterminanthscm_positive_cell_source. ff_h_mdm_mdr_zero_rows_rankzeroevaluationdeterminanthscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_zero_rows_rankzeroevaluationdeterminanthscm_positive) = S ((S ((ff_row_mdm_cell_mdr_zero_rows_rankzeroevaluationdeterminanthscm_positive_cell) * (S (mdr_q_zero_rows_rankzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_zero_rows_rankzeroevaluationdeterminanthscm_positive_cell))) * mdr_pc_zero_rows_rankzeroevaluationdeterminanth)) /\ exists ff_q_mdm_mdr_zero_rows_rankzeroevaluationdeterminanthscm_positive_cell_source. mdr_pb_zero_rows_rankzeroevaluationdeterminanth = ff_q_mdm_mdr_zero_rows_rankzeroevaluationdeterminanthscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_zero_rows_rankzeroevaluationdeterminanthscm_positive_cell) * (S (mdr_q_zero_rows_rankzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_zero_rows_rankzeroevaluationdeterminanthscm_positive_cell))) * mdr_pc_zero_rows_rankzeroevaluationdeterminanth) + (ff_value_mdm_prefix_mdr_zero_rows_rankzeroevaluationdeterminanthscm_positive)))))) /\ (((exists ff_h_mdm_mdr_zero_rows_rankzeroevaluationdeterminanthscm_positive_target. ff_h_mdm_mdr_zero_rows_rankzeroevaluationdeterminanthscm_positive_target + S (ff_value_mdm_prefix_mdr_zero_rows_rankzeroevaluationdeterminanthscm_positive) = S ((S (ff_index_mdm_prefix_mdr_zero_rows_rankzeroevaluationdeterminanthscm_positive)) * mdr_us_zero_rows_rankzeroevaluationdeterminanthsc)) /\ exists ff_q_mdm_mdr_zero_rows_rankzeroevaluationdeterminanthscm_positive_target. mdr_up_zero_rows_rankzeroevaluationdeterminanthsc = ff_q_mdm_mdr_zero_rows_rankzeroevaluationdeterminanthscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_zero_rows_rankzeroevaluationdeterminanthscm_positive)) * mdr_us_zero_rows_rankzeroevaluationdeterminanthsc) + (ff_value_mdm_prefix_mdr_zero_rows_rankzeroevaluationdeterminanthscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_zero_rows_rankzeroevaluationdeterminanthscm_negative. (exists ff_gap_mdm_lt_mdr_zero_rows_rankzeroevaluationdeterminanthscm_negative_index_bound. ff_gap_mdm_lt_mdr_zero_rows_rankzeroevaluationdeterminanthscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_zero_rows_rankzeroevaluationdeterminanthscm_negative) = ((mdr_q_zero_rows_rankzeroevaluationdeterminanths) * (mdr_q_zero_rows_rankzeroevaluationdeterminanths))) -> exists ff_row_mdm_prefix_mdr_zero_rows_rankzeroevaluationdeterminanthscm_negative ff_column_mdm_prefix_mdr_zero_rows_rankzeroevaluationdeterminanthscm_negative ff_value_mdm_prefix_mdr_zero_rows_rankzeroevaluationdeterminanthscm_negative. (ff_index_mdm_prefix_mdr_zero_rows_rankzeroevaluationdeterminanthscm_negative = (mdr_q_zero_rows_rankzeroevaluationdeterminanths) * ff_row_mdm_prefix_mdr_zero_rows_rankzeroevaluationdeterminanthscm_negative + ff_column_mdm_prefix_mdr_zero_rows_rankzeroevaluationdeterminanthscm_negative /\ ((exists ff_gap_mdm_lt_mdr_zero_rows_rankzeroevaluationdeterminanthscm_negative_column_bound. ff_gap_mdm_lt_mdr_zero_rows_rankzeroevaluationdeterminanthscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_zero_rows_rankzeroevaluationdeterminanthscm_negative) = (mdr_q_zero_rows_rankzeroevaluationdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_zero_rows_rankzeroevaluationdeterminanthscm_negative_cell ff_column_mdm_cell_mdr_zero_rows_rankzeroevaluationdeterminanthscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_zero_rows_rankzeroevaluationdeterminanthscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_zero_rows_rankzeroevaluationdeterminanthscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_zero_rows_rankzeroevaluationdeterminanthscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_zero_rows_rankzeroevaluationdeterminanthscm_negative_cell = ff_row_mdm_prefix_mdr_zero_rows_rankzeroevaluationdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_zero_rows_rankzeroevaluationdeterminanthscm_negative_cell_row_after. ff_gap_mdm_le_mdr_zero_rows_rankzeroevaluationdeterminanthscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_zero_rows_rankzeroevaluationdeterminanthscm_negative)) /\ ff_row_mdm_cell_mdr_zero_rows_rankzeroevaluationdeterminanthscm_negative_cell = S ff_row_mdm_prefix_mdr_zero_rows_rankzeroevaluationdeterminanthscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_zero_rows_rankzeroevaluationdeterminanthscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_zero_rows_rankzeroevaluationdeterminanthscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_zero_rows_rankzeroevaluationdeterminanthscm_negative) = (mdr_j_zero_rows_rankzeroevaluationdeterminanthsc)) /\ ff_column_mdm_cell_mdr_zero_rows_rankzeroevaluationdeterminanthscm_negative_cell = ff_column_mdm_prefix_mdr_zero_rows_rankzeroevaluationdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_zero_rows_rankzeroevaluationdeterminanthscm_negative_cell_column_after. ff_gap_mdm_le_mdr_zero_rows_rankzeroevaluationdeterminanthscm_negative_cell_column_after + (mdr_j_zero_rows_rankzeroevaluationdeterminanthsc) = (ff_column_mdm_prefix_mdr_zero_rows_rankzeroevaluationdeterminanthscm_negative)) /\ ff_column_mdm_cell_mdr_zero_rows_rankzeroevaluationdeterminanthscm_negative_cell = S ff_column_mdm_prefix_mdr_zero_rows_rankzeroevaluationdeterminanthscm_negative))) /\ (((exists ff_h_mdm_mdr_zero_rows_rankzeroevaluationdeterminanthscm_negative_cell_source. ff_h_mdm_mdr_zero_rows_rankzeroevaluationdeterminanthscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_zero_rows_rankzeroevaluationdeterminanthscm_negative) = S ((S ((ff_row_mdm_cell_mdr_zero_rows_rankzeroevaluationdeterminanthscm_negative_cell) * (S (mdr_q_zero_rows_rankzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_zero_rows_rankzeroevaluationdeterminanthscm_negative_cell))) * mdr_nc_zero_rows_rankzeroevaluationdeterminanth)) /\ exists ff_q_mdm_mdr_zero_rows_rankzeroevaluationdeterminanthscm_negative_cell_source. mdr_nb_zero_rows_rankzeroevaluationdeterminanth = ff_q_mdm_mdr_zero_rows_rankzeroevaluationdeterminanthscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_zero_rows_rankzeroevaluationdeterminanthscm_negative_cell) * (S (mdr_q_zero_rows_rankzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_zero_rows_rankzeroevaluationdeterminanthscm_negative_cell))) * mdr_nc_zero_rows_rankzeroevaluationdeterminanth) + (ff_value_mdm_prefix_mdr_zero_rows_rankzeroevaluationdeterminanthscm_negative)))))) /\ (((exists ff_h_mdm_mdr_zero_rows_rankzeroevaluationdeterminanthscm_negative_target. ff_h_mdm_mdr_zero_rows_rankzeroevaluationdeterminanthscm_negative_target + S (ff_value_mdm_prefix_mdr_zero_rows_rankzeroevaluationdeterminanthscm_negative) = S ((S (ff_index_mdm_prefix_mdr_zero_rows_rankzeroevaluationdeterminanthscm_negative)) * mdr_ut_zero_rows_rankzeroevaluationdeterminanthsc)) /\ exists ff_q_mdm_mdr_zero_rows_rankzeroevaluationdeterminanthscm_negative_target. mdr_un_zero_rows_rankzeroevaluationdeterminanthsc = ff_q_mdm_mdr_zero_rows_rankzeroevaluationdeterminanthscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_zero_rows_rankzeroevaluationdeterminanthscm_negative)) * mdr_ut_zero_rows_rankzeroevaluationdeterminanthsc) + (ff_value_mdm_prefix_mdr_zero_rows_rankzeroevaluationdeterminanthscm_negative))))))))) /\ ((((exists ff_h_mdr_zero_rows_rankzeroevaluationdeterminanthscp. ff_h_mdr_zero_rows_rankzeroevaluationdeterminanthscp + S (mdr_p_zero_rows_rankzeroevaluationdeterminanthsc) = S ((S (mdr_j_zero_rows_rankzeroevaluationdeterminanthsc)) * mdr_ec_zero_rows_rankzeroevaluationdeterminanths)) /\ exists ff_q_mdr_zero_rows_rankzeroevaluationdeterminanthscp. mdr_eb_zero_rows_rankzeroevaluationdeterminanths = ff_q_mdr_zero_rows_rankzeroevaluationdeterminanthscp * S ((S (mdr_j_zero_rows_rankzeroevaluationdeterminanthsc)) * mdr_ec_zero_rows_rankzeroevaluationdeterminanths) + (mdr_p_zero_rows_rankzeroevaluationdeterminanthsc))) /\ (((exists ff_h_mdr_zero_rows_rankzeroevaluationdeterminanthscn. ff_h_mdr_zero_rows_rankzeroevaluationdeterminanthscn + S (mdr_n_zero_rows_rankzeroevaluationdeterminanthsc) = S ((S (mdr_j_zero_rows_rankzeroevaluationdeterminanthsc)) * mdr_fc_zero_rows_rankzeroevaluationdeterminanths)) /\ exists ff_q_mdr_zero_rows_rankzeroevaluationdeterminanthscn. mdr_fb_zero_rows_rankzeroevaluationdeterminanths = ff_q_mdr_zero_rows_rankzeroevaluationdeterminanthscn * S ((S (mdr_j_zero_rows_rankzeroevaluationdeterminanthsc)) * mdr_fc_zero_rows_rankzeroevaluationdeterminanths) + (mdr_n_zero_rows_rankzeroevaluationdeterminanthsc)))))))) /\ (exists ff_ub_mce_fold_mdr_zero_rows_rankzeroevaluationdeterminanthsf ff_uc_mce_fold_mdr_zero_rows_rankzeroevaluationdeterminanthsf ff_vb_mce_fold_mdr_zero_rows_rankzeroevaluationdeterminanthsf ff_vc_mce_fold_mdr_zero_rows_rankzeroevaluationdeterminanthsf. ((forall ff_index_mce_alternating_mdr_zero_rows_rankzeroevaluationdeterminanthsf_prefix. (exists ff_gap_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_prefix_index. ff_gap_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_prefix_index + S (ff_index_mce_alternating_mdr_zero_rows_rankzeroevaluationdeterminanthsf_prefix) = (S (mdr_q_zero_rows_rankzeroevaluationdeterminanths))) -> exists ff_ap_mce_alternating_mdr_zero_rows_rankzeroevaluationdeterminanthsf_prefix ff_an_mce_alternating_mdr_zero_rows_rankzeroevaluationdeterminanthsf_prefix ff_bp_mce_alternating_mdr_zero_rows_rankzeroevaluationdeterminanthsf_prefix ff_bn_mce_alternating_mdr_zero_rows_rankzeroevaluationdeterminanthsf_prefix ff_p_mce_alternating_mdr_zero_rows_rankzeroevaluationdeterminanthsf_prefix ff_n_mce_alternating_mdr_zero_rows_rankzeroevaluationdeterminanthsf_prefix. ((((exists ff_h_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_prefix_ap. ff_h_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_prefix_ap + S (ff_ap_mce_alternating_mdr_zero_rows_rankzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_zero_rows_rankzeroevaluationdeterminanthsf_prefix)) * mdr_pc_zero_rows_rankzeroevaluationdeterminanth)) /\ exists ff_q_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_prefix_ap. mdr_pb_zero_rows_rankzeroevaluationdeterminanth = ff_q_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_zero_rows_rankzeroevaluationdeterminanthsf_prefix)) * mdr_pc_zero_rows_rankzeroevaluationdeterminanth) + (ff_ap_mce_alternating_mdr_zero_rows_rankzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_prefix_an. ff_h_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_prefix_an + S (ff_an_mce_alternating_mdr_zero_rows_rankzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_zero_rows_rankzeroevaluationdeterminanthsf_prefix)) * mdr_nc_zero_rows_rankzeroevaluationdeterminanth)) /\ exists ff_q_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_prefix_an. mdr_nb_zero_rows_rankzeroevaluationdeterminanth = ff_q_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_zero_rows_rankzeroevaluationdeterminanthsf_prefix)) * mdr_nc_zero_rows_rankzeroevaluationdeterminanth) + (ff_an_mce_alternating_mdr_zero_rows_rankzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_prefix_bp. ff_h_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_prefix_bp + S (ff_bp_mce_alternating_mdr_zero_rows_rankzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_zero_rows_rankzeroevaluationdeterminanthsf_prefix)) * mdr_ec_zero_rows_rankzeroevaluationdeterminanths)) /\ exists ff_q_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_prefix_bp. mdr_eb_zero_rows_rankzeroevaluationdeterminanths = ff_q_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_zero_rows_rankzeroevaluationdeterminanthsf_prefix)) * mdr_ec_zero_rows_rankzeroevaluationdeterminanths) + (ff_bp_mce_alternating_mdr_zero_rows_rankzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_prefix_bn. ff_h_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_prefix_bn + S (ff_bn_mce_alternating_mdr_zero_rows_rankzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_zero_rows_rankzeroevaluationdeterminanthsf_prefix)) * mdr_fc_zero_rows_rankzeroevaluationdeterminanths)) /\ exists ff_q_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_prefix_bn. mdr_fb_zero_rows_rankzeroevaluationdeterminanths = ff_q_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_zero_rows_rankzeroevaluationdeterminanthsf_prefix)) * mdr_fc_zero_rows_rankzeroevaluationdeterminanths) + (ff_bn_mce_alternating_mdr_zero_rows_rankzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_prefix_positive. ff_h_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_prefix_positive + S (ff_p_mce_alternating_mdr_zero_rows_rankzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_zero_rows_rankzeroevaluationdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_zero_rows_rankzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_prefix_positive. ff_ub_mce_fold_mdr_zero_rows_rankzeroevaluationdeterminanthsf = ff_q_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_zero_rows_rankzeroevaluationdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_zero_rows_rankzeroevaluationdeterminanthsf) + (ff_p_mce_alternating_mdr_zero_rows_rankzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_prefix_negative. ff_h_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_prefix_negative + S (ff_n_mce_alternating_mdr_zero_rows_rankzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_zero_rows_rankzeroevaluationdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_zero_rows_rankzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_prefix_negative. ff_vb_mce_fold_mdr_zero_rows_rankzeroevaluationdeterminanthsf = ff_q_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_zero_rows_rankzeroevaluationdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_zero_rows_rankzeroevaluationdeterminanthsf) + (ff_n_mce_alternating_mdr_zero_rows_rankzeroevaluationdeterminanthsf_prefix))) /\ (((exists ff_even_mce_term_mdr_zero_rows_rankzeroevaluationdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_zero_rows_rankzeroevaluationdeterminanthsf_prefix = 2 * ff_even_mce_term_mdr_zero_rows_rankzeroevaluationdeterminanthsf_prefix_term) /\ (ff_p_mce_alternating_mdr_zero_rows_rankzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_zero_rows_rankzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_zero_rows_rankzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_zero_rows_rankzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_zero_rows_rankzeroevaluationdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_zero_rows_rankzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_zero_rows_rankzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_zero_rows_rankzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_zero_rows_rankzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_zero_rows_rankzeroevaluationdeterminanthsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_zero_rows_rankzeroevaluationdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_zero_rows_rankzeroevaluationdeterminanthsf_prefix = 2 * ff_odd_mce_term_mdr_zero_rows_rankzeroevaluationdeterminanthsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_zero_rows_rankzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_zero_rows_rankzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_zero_rows_rankzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_zero_rows_rankzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_zero_rows_rankzeroevaluationdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_zero_rows_rankzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_zero_rows_rankzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_zero_rows_rankzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_zero_rows_rankzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_zero_rows_rankzeroevaluationdeterminanthsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_positive ff_v_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_positive. ((((exists ff_h_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_positive_start. ff_h_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_positive_start. ff_u_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_positive_start * S ((S (0)) * ff_v_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_positive_terminal. ff_h_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_positive_terminal + S (mdr_p_zero_rows_rankzeroevaluationdeterminanth) = S ((S ((S (mdr_q_zero_rows_rankzeroevaluationdeterminanths)))) * ff_v_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_positive_terminal. ff_u_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_positive_terminal * S ((S ((S (mdr_q_zero_rows_rankzeroevaluationdeterminanths)))) * ff_v_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_positive) + (mdr_p_zero_rows_rankzeroevaluationdeterminanth))) /\ forall ff_i_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_positive. (exists ff_lt_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_positive_bound. ff_lt_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_positive_bound + S ff_i_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_positive = (S (mdr_q_zero_rows_rankzeroevaluationdeterminanths))) -> exists ff_a_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_positive ff_r_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_positive ff_s_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_positive. ((((exists ff_h_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_positive_summand. ff_h_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_positive_summand + S (ff_a_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_zero_rows_rankzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_positive_summand. ff_ub_mce_fold_mdr_zero_rows_rankzeroevaluationdeterminanthsf = ff_q_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_positive_summand * S ((S (ff_i_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_zero_rows_rankzeroevaluationdeterminanthsf) + (ff_a_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_positive_partial. ff_h_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_positive_partial + S (ff_r_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_positive_partial. ff_u_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_positive_partial * S ((S (ff_i_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_positive) + (ff_r_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_positive_successor. ff_h_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_positive_successor + S (ff_s_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_positive) = S ((S (S ff_i_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_positive_successor. ff_u_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_positive_successor * S ((S (S ff_i_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_positive) + (ff_s_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_positive))) /\ ff_s_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_positive = ff_r_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_positive + ff_a_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_positive)))))) /\ (exists ff_u_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_negative ff_v_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_negative. ((((exists ff_h_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_negative_start. ff_h_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_negative_start. ff_u_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_negative_start * S ((S (0)) * ff_v_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_negative_terminal. ff_h_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_negative_terminal + S (mdr_n_zero_rows_rankzeroevaluationdeterminanth) = S ((S ((S (mdr_q_zero_rows_rankzeroevaluationdeterminanths)))) * ff_v_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_negative_terminal. ff_u_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_negative_terminal * S ((S ((S (mdr_q_zero_rows_rankzeroevaluationdeterminanths)))) * ff_v_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_negative) + (mdr_n_zero_rows_rankzeroevaluationdeterminanth))) /\ forall ff_i_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_negative. (exists ff_lt_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_negative_bound. ff_lt_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_negative_bound + S ff_i_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_negative = (S (mdr_q_zero_rows_rankzeroevaluationdeterminanths))) -> exists ff_a_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_negative ff_r_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_negative ff_s_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_negative. ((((exists ff_h_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_negative_summand. ff_h_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_negative_summand + S (ff_a_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_zero_rows_rankzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_negative_summand. ff_vb_mce_fold_mdr_zero_rows_rankzeroevaluationdeterminanthsf = ff_q_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_negative_summand * S ((S (ff_i_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_zero_rows_rankzeroevaluationdeterminanthsf) + (ff_a_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_negative_partial. ff_h_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_negative_partial + S (ff_r_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_negative_partial. ff_u_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_negative_partial * S ((S (ff_i_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_negative) + (ff_r_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_negative_successor. ff_h_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_negative_successor + S (ff_s_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_negative) = S ((S (S ff_i_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_negative_successor. ff_u_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_negative_successor * S ((S (S ff_i_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_negative) + (ff_s_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_negative))) /\ ff_s_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_negative = ff_r_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_negative + ff_a_mce_mdr_zero_rows_rankzeroevaluationdeterminanthsf_negative))))))))))))))) /\ ((exists mdr_gap_zero_rows_rankzeroevaluationdeterminanti. mdr_gap_zero_rows_rankzeroevaluationdeterminanti + S (mdr_i_zero_rows_rankzeroevaluationdeterminant) = (mdr_l_zero_rows_rankzeroevaluationdeterminant)) /\ (exists mdr_z_zero_rows_rankzeroevaluationdeterminantr. ((exists mdr_a_zero_rows_rankzeroevaluationdeterminantrc mdr_b_zero_rows_rankzeroevaluationdeterminantrc mdr_c_zero_rows_rankzeroevaluationdeterminantrc mdr_e_zero_rows_rankzeroevaluationdeterminantrc mdr_f_zero_rows_rankzeroevaluationdeterminantrc. ((mdr_a_zero_rows_rankzeroevaluationdeterminantrc = ((mdr_q_zero_rows_rank) + (mdr_ub_zero_rows_rankzeroevaluation)) * S ((mdr_q_zero_rows_rank) + (mdr_ub_zero_rows_rankzeroevaluation)) + ((mdr_ub_zero_rows_rankzeroevaluation) + (mdr_ub_zero_rows_rankzeroevaluation))) /\ ((mdr_b_zero_rows_rankzeroevaluationdeterminantrc = ((mdr_uc_zero_rows_rankzeroevaluation) + (mdr_vb_zero_rows_rankzeroevaluation)) * S ((mdr_uc_zero_rows_rankzeroevaluation) + (mdr_vb_zero_rows_rankzeroevaluation)) + ((mdr_vb_zero_rows_rankzeroevaluation) + (mdr_vb_zero_rows_rankzeroevaluation))) /\ ((mdr_c_zero_rows_rankzeroevaluationdeterminantrc = ((mdr_a_zero_rows_rankzeroevaluationdeterminantrc) + (mdr_b_zero_rows_rankzeroevaluationdeterminantrc)) * S ((mdr_a_zero_rows_rankzeroevaluationdeterminantrc) + (mdr_b_zero_rows_rankzeroevaluationdeterminantrc)) + ((mdr_b_zero_rows_rankzeroevaluationdeterminantrc) + (mdr_b_zero_rows_rankzeroevaluationdeterminantrc))) /\ ((mdr_e_zero_rows_rankzeroevaluationdeterminantrc = ((mdr_p_zero_rows_rankzero) + (mdr_n_zero_rows_rankzero)) * S ((mdr_p_zero_rows_rankzero) + (mdr_n_zero_rows_rankzero)) + ((mdr_n_zero_rows_rankzero) + (mdr_n_zero_rows_rankzero))) /\ ((mdr_f_zero_rows_rankzeroevaluationdeterminantrc = ((mdr_vc_zero_rows_rankzeroevaluation) + (mdr_e_zero_rows_rankzeroevaluationdeterminantrc)) * S ((mdr_vc_zero_rows_rankzeroevaluation) + (mdr_e_zero_rows_rankzeroevaluationdeterminantrc)) + ((mdr_e_zero_rows_rankzeroevaluationdeterminantrc) + (mdr_e_zero_rows_rankzeroevaluationdeterminantrc))) /\ ((mdr_z_zero_rows_rankzeroevaluationdeterminantr) = ((mdr_c_zero_rows_rankzeroevaluationdeterminantrc) + (mdr_f_zero_rows_rankzeroevaluationdeterminantrc)) * S ((mdr_c_zero_rows_rankzeroevaluationdeterminantrc) + (mdr_f_zero_rows_rankzeroevaluationdeterminantrc)) + ((mdr_f_zero_rows_rankzeroevaluationdeterminantrc) + (mdr_f_zero_rows_rankzeroevaluationdeterminantrc))))))))) /\ (((exists ff_h_mdr_zero_rows_rankzeroevaluationdeterminantrb. ff_h_mdr_zero_rows_rankzeroevaluationdeterminantrb + S (mdr_z_zero_rows_rankzeroevaluationdeterminantr) = S ((S (mdr_i_zero_rows_rankzeroevaluationdeterminant)) * mdr_c_zero_rows_rankzeroevaluationdeterminant)) /\ exists ff_q_mdr_zero_rows_rankzeroevaluationdeterminantrb. mdr_b_zero_rows_rankzeroevaluationdeterminant = ff_q_mdr_zero_rows_rankzeroevaluationdeterminantrb * S ((S (mdr_i_zero_rows_rankzeroevaluationdeterminant)) * mdr_c_zero_rows_rankzeroevaluationdeterminant) + (mdr_z_zero_rows_rankzeroevaluationdeterminantr)))))))))) -> mdr_p_zero_rows_rankzero = mdr_n_zero_rows_rankzero))))))