rectangular_matrix_rank_zero_columns

forall pb pc nb nc r. (((exists mdr_gap_zero_columns_rankrows_bound. mdr_gap_zero_columns_rankrows_bound + (0) = (r)) /\ ((exists mdr_gap_zero_columns_rankcolumns_bound. mdr_gap_zero_columns_rankcolumns_bound + (0) = (0)) /\ ((exists mdr_rb_zero_columns_rankwitness mdr_rc_zero_columns_rankwitness mdr_cb_zero_columns_rankwitness mdr_cc_zero_columns_rankwitness. (((((forall fom_index_mrf_zero_columns_rankwitnessminorrowsbound. (exists fom_gap_mrf_zero_columns_rankwitnessminorrowsbound_index_bound. fom_gap_mrf_zero_columns_rankwitnessminorrowsbound_index_bound + S (fom_index_mrf_zero_columns_rankwitnessminorrowsbound) = 0) -> exists fom_value_mrf_zero_columns_rankwitnessminorrowsbound. ((((exists fom_beta_height_mrf_zero_columns_rankwitnessminorrowsbound_entry. fom_beta_height_mrf_zero_columns_rankwitnessminorrowsbound_entry + S (fom_value_mrf_zero_columns_rankwitnessminorrowsbound) = S ((S (fom_index_mrf_zero_columns_rankwitnessminorrowsbound)) * mdr_rc_zero_columns_rankwitness)) /\ exists fom_beta_quotient_mrf_zero_columns_rankwitnessminorrowsbound_entry. mdr_rb_zero_columns_rankwitness = fom_beta_quotient_mrf_zero_columns_rankwitnessminorrowsbound_entry * S ((S (fom_index_mrf_zero_columns_rankwitnessminorrowsbound)) * mdr_rc_zero_columns_rankwitness) + (fom_value_mrf_zero_columns_rankwitnessminorrowsbound))) /\ (exists fom_gap_mrf_zero_columns_rankwitnessminorrowsbound_value_bound. fom_gap_mrf_zero_columns_rankwitnessminorrowsbound_value_bound + S (fom_value_mrf_zero_columns_rankwitnessminorrowsbound) = r))) /\ (forall mdr_i_zero_columns_rankwitnessminorrowsdistinct mdr_j_zero_columns_rankwitnessminorrowsdistinct mdr_a_zero_columns_rankwitnessminorrowsdistinct. (exists mdr_gap_zero_columns_rankwitnessminorrowsdistincti. mdr_gap_zero_columns_rankwitnessminorrowsdistincti + S (mdr_i_zero_columns_rankwitnessminorrowsdistinct) = (0)) -> (exists mdr_gap_zero_columns_rankwitnessminorrowsdistinctj. mdr_gap_zero_columns_rankwitnessminorrowsdistinctj + S (mdr_j_zero_columns_rankwitnessminorrowsdistinct) = (0)) -> (((exists ff_h_mdr_zero_columns_rankwitnessminorrowsdistinctfirst. ff_h_mdr_zero_columns_rankwitnessminorrowsdistinctfirst + S (mdr_a_zero_columns_rankwitnessminorrowsdistinct) = S ((S (mdr_i_zero_columns_rankwitnessminorrowsdistinct)) * mdr_rc_zero_columns_rankwitness)) /\ exists ff_q_mdr_zero_columns_rankwitnessminorrowsdistinctfirst. mdr_rb_zero_columns_rankwitness = ff_q_mdr_zero_columns_rankwitnessminorrowsdistinctfirst * S ((S (mdr_i_zero_columns_rankwitnessminorrowsdistinct)) * mdr_rc_zero_columns_rankwitness) + (mdr_a_zero_columns_rankwitnessminorrowsdistinct))) -> (((exists ff_h_mdr_zero_columns_rankwitnessminorrowsdistinctsecond. ff_h_mdr_zero_columns_rankwitnessminorrowsdistinctsecond + S (mdr_a_zero_columns_rankwitnessminorrowsdistinct) = S ((S (mdr_j_zero_columns_rankwitnessminorrowsdistinct)) * mdr_rc_zero_columns_rankwitness)) /\ exists ff_q_mdr_zero_columns_rankwitnessminorrowsdistinctsecond. mdr_rb_zero_columns_rankwitness = ff_q_mdr_zero_columns_rankwitnessminorrowsdistinctsecond * S ((S (mdr_j_zero_columns_rankwitnessminorrowsdistinct)) * mdr_rc_zero_columns_rankwitness) + (mdr_a_zero_columns_rankwitnessminorrowsdistinct))) -> mdr_i_zero_columns_rankwitnessminorrowsdistinct = mdr_j_zero_columns_rankwitnessminorrowsdistinct))) /\ ((((forall fom_index_mrf_zero_columns_rankwitnessminorcolumnsbound. (exists fom_gap_mrf_zero_columns_rankwitnessminorcolumnsbound_index_bound. fom_gap_mrf_zero_columns_rankwitnessminorcolumnsbound_index_bound + S (fom_index_mrf_zero_columns_rankwitnessminorcolumnsbound) = 0) -> exists fom_value_mrf_zero_columns_rankwitnessminorcolumnsbound. ((((exists fom_beta_height_mrf_zero_columns_rankwitnessminorcolumnsbound_entry. fom_beta_height_mrf_zero_columns_rankwitnessminorcolumnsbound_entry + S (fom_value_mrf_zero_columns_rankwitnessminorcolumnsbound) = S ((S (fom_index_mrf_zero_columns_rankwitnessminorcolumnsbound)) * mdr_cc_zero_columns_rankwitness)) /\ exists fom_beta_quotient_mrf_zero_columns_rankwitnessminorcolumnsbound_entry. mdr_cb_zero_columns_rankwitness = fom_beta_quotient_mrf_zero_columns_rankwitnessminorcolumnsbound_entry * S ((S (fom_index_mrf_zero_columns_rankwitnessminorcolumnsbound)) * mdr_cc_zero_columns_rankwitness) + (fom_value_mrf_zero_columns_rankwitnessminorcolumnsbound))) /\ (exists fom_gap_mrf_zero_columns_rankwitnessminorcolumnsbound_value_bound. fom_gap_mrf_zero_columns_rankwitnessminorcolumnsbound_value_bound + S (fom_value_mrf_zero_columns_rankwitnessminorcolumnsbound) = 0))) /\ (forall mdr_i_zero_columns_rankwitnessminorcolumnsdistinct mdr_j_zero_columns_rankwitnessminorcolumnsdistinct mdr_a_zero_columns_rankwitnessminorcolumnsdistinct. (exists mdr_gap_zero_columns_rankwitnessminorcolumnsdistincti. mdr_gap_zero_columns_rankwitnessminorcolumnsdistincti + S (mdr_i_zero_columns_rankwitnessminorcolumnsdistinct) = (0)) -> (exists mdr_gap_zero_columns_rankwitnessminorcolumnsdistinctj. mdr_gap_zero_columns_rankwitnessminorcolumnsdistinctj + S (mdr_j_zero_columns_rankwitnessminorcolumnsdistinct) = (0)) -> (((exists ff_h_mdr_zero_columns_rankwitnessminorcolumnsdistinctfirst. ff_h_mdr_zero_columns_rankwitnessminorcolumnsdistinctfirst + S (mdr_a_zero_columns_rankwitnessminorcolumnsdistinct) = S ((S (mdr_i_zero_columns_rankwitnessminorcolumnsdistinct)) * mdr_cc_zero_columns_rankwitness)) /\ exists ff_q_mdr_zero_columns_rankwitnessminorcolumnsdistinctfirst. mdr_cb_zero_columns_rankwitness = ff_q_mdr_zero_columns_rankwitnessminorcolumnsdistinctfirst * S ((S (mdr_i_zero_columns_rankwitnessminorcolumnsdistinct)) * mdr_cc_zero_columns_rankwitness) + (mdr_a_zero_columns_rankwitnessminorcolumnsdistinct))) -> (((exists ff_h_mdr_zero_columns_rankwitnessminorcolumnsdistinctsecond. ff_h_mdr_zero_columns_rankwitnessminorcolumnsdistinctsecond + S (mdr_a_zero_columns_rankwitnessminorcolumnsdistinct) = S ((S (mdr_j_zero_columns_rankwitnessminorcolumnsdistinct)) * mdr_cc_zero_columns_rankwitness)) /\ exists ff_q_mdr_zero_columns_rankwitnessminorcolumnsdistinctsecond. mdr_cb_zero_columns_rankwitness = ff_q_mdr_zero_columns_rankwitnessminorcolumnsdistinctsecond * S ((S (mdr_j_zero_columns_rankwitnessminorcolumnsdistinct)) * mdr_cc_zero_columns_rankwitness) + (mdr_a_zero_columns_rankwitnessminorcolumnsdistinct))) -> mdr_i_zero_columns_rankwitnessminorcolumnsdistinct = mdr_j_zero_columns_rankwitnessminorcolumnsdistinct))) /\ (exists mdr_p_zero_columns_rankwitnessminornonzero mdr_n_zero_columns_rankwitnessminornonzero. ((exists mdr_ub_zero_columns_rankwitnessminornonzeroevaluation mdr_uc_zero_columns_rankwitnessminornonzeroevaluation mdr_vb_zero_columns_rankwitnessminornonzeroevaluation mdr_vc_zero_columns_rankwitnessminornonzeroevaluation. ((((forall mdr_i_zero_columns_rankwitnessminornonzeroevaluationmatrixpositive. (exists mdr_gap_zero_columns_rankwitnessminornonzeroevaluationmatrixpositivebound. mdr_gap_zero_columns_rankwitnessminornonzeroevaluationmatrixpositivebound + S (mdr_i_zero_columns_rankwitnessminornonzeroevaluationmatrixpositive) = ((0) * (0))) -> exists mdr_a_zero_columns_rankwitnessminornonzeroevaluationmatrixpositive. (((exists mdr_r_zero_columns_rankwitnessminornonzeroevaluationmatrixpositivepoint mdr_s_zero_columns_rankwitnessminornonzeroevaluationmatrixpositivepoint mdr_u_zero_columns_rankwitnessminornonzeroevaluationmatrixpositivepoint mdr_v_zero_columns_rankwitnessminornonzeroevaluationmatrixpositivepoint. ((mdr_i_zero_columns_rankwitnessminornonzeroevaluationmatrixpositive = (0) * mdr_r_zero_columns_rankwitnessminornonzeroevaluationmatrixpositivepoint + mdr_s_zero_columns_rankwitnessminornonzeroevaluationmatrixpositivepoint) /\ ((exists mdr_gap_zero_columns_rankwitnessminornonzeroevaluationmatrixpositivepointcolumn. mdr_gap_zero_columns_rankwitnessminornonzeroevaluationmatrixpositivepointcolumn + S (mdr_s_zero_columns_rankwitnessminornonzeroevaluationmatrixpositivepoint) = (0)) /\ ((((exists ff_h_mdr_zero_columns_rankwitnessminornonzeroevaluationmatrixpositivepointrow_index. ff_h_mdr_zero_columns_rankwitnessminornonzeroevaluationmatrixpositivepointrow_index + S (mdr_u_zero_columns_rankwitnessminornonzeroevaluationmatrixpositivepoint) = S ((S (mdr_r_zero_columns_rankwitnessminornonzeroevaluationmatrixpositivepoint)) * mdr_rc_zero_columns_rankwitness)) /\ exists ff_q_mdr_zero_columns_rankwitnessminornonzeroevaluationmatrixpositivepointrow_index. mdr_rb_zero_columns_rankwitness = ff_q_mdr_zero_columns_rankwitnessminornonzeroevaluationmatrixpositivepointrow_index * S ((S (mdr_r_zero_columns_rankwitnessminornonzeroevaluationmatrixpositivepoint)) * mdr_rc_zero_columns_rankwitness) + (mdr_u_zero_columns_rankwitnessminornonzeroevaluationmatrixpositivepoint))) /\ ((((exists ff_h_mdr_zero_columns_rankwitnessminornonzeroevaluationmatrixpositivepointcolumn_index. ff_h_mdr_zero_columns_rankwitnessminornonzeroevaluationmatrixpositivepointcolumn_index + S (mdr_v_zero_columns_rankwitnessminornonzeroevaluationmatrixpositivepoint) = S ((S (mdr_s_zero_columns_rankwitnessminornonzeroevaluationmatrixpositivepoint)) * mdr_cc_zero_columns_rankwitness)) /\ exists ff_q_mdr_zero_columns_rankwitnessminornonzeroevaluationmatrixpositivepointcolumn_index. mdr_cb_zero_columns_rankwitness = ff_q_mdr_zero_columns_rankwitnessminornonzeroevaluationmatrixpositivepointcolumn_index * S ((S (mdr_s_zero_columns_rankwitnessminornonzeroevaluationmatrixpositivepoint)) * mdr_cc_zero_columns_rankwitness) + (mdr_v_zero_columns_rankwitnessminornonzeroevaluationmatrixpositivepoint))) /\ (((exists ff_h_mdr_zero_columns_rankwitnessminornonzeroevaluationmatrixpositivepointsource. ff_h_mdr_zero_columns_rankwitnessminornonzeroevaluationmatrixpositivepointsource + S (mdr_a_zero_columns_rankwitnessminornonzeroevaluationmatrixpositive) = S ((S ((mdr_u_zero_columns_rankwitnessminornonzeroevaluationmatrixpositivepoint) * (0) + (mdr_v_zero_columns_rankwitnessminornonzeroevaluationmatrixpositivepoint))) * pc)) /\ exists ff_q_mdr_zero_columns_rankwitnessminornonzeroevaluationmatrixpositivepointsource. pb = ff_q_mdr_zero_columns_rankwitnessminornonzeroevaluationmatrixpositivepointsource * S ((S ((mdr_u_zero_columns_rankwitnessminornonzeroevaluationmatrixpositivepoint) * (0) + (mdr_v_zero_columns_rankwitnessminornonzeroevaluationmatrixpositivepoint))) * pc) + (mdr_a_zero_columns_rankwitnessminornonzeroevaluationmatrixpositive)))))))) /\ (((exists ff_h_mdr_zero_columns_rankwitnessminornonzeroevaluationmatrixpositiveoutput. ff_h_mdr_zero_columns_rankwitnessminornonzeroevaluationmatrixpositiveoutput + S (mdr_a_zero_columns_rankwitnessminornonzeroevaluationmatrixpositive) = S ((S (mdr_i_zero_columns_rankwitnessminornonzeroevaluationmatrixpositive)) * mdr_uc_zero_columns_rankwitnessminornonzeroevaluation)) /\ exists ff_q_mdr_zero_columns_rankwitnessminornonzeroevaluationmatrixpositiveoutput. mdr_ub_zero_columns_rankwitnessminornonzeroevaluation = ff_q_mdr_zero_columns_rankwitnessminornonzeroevaluationmatrixpositiveoutput * S ((S (mdr_i_zero_columns_rankwitnessminornonzeroevaluationmatrixpositive)) * mdr_uc_zero_columns_rankwitnessminornonzeroevaluation) + (mdr_a_zero_columns_rankwitnessminornonzeroevaluationmatrixpositive)))))) /\ (forall mdr_i_zero_columns_rankwitnessminornonzeroevaluationmatrixnegative. (exists mdr_gap_zero_columns_rankwitnessminornonzeroevaluationmatrixnegativebound. mdr_gap_zero_columns_rankwitnessminornonzeroevaluationmatrixnegativebound + S (mdr_i_zero_columns_rankwitnessminornonzeroevaluationmatrixnegative) = ((0) * (0))) -> exists mdr_a_zero_columns_rankwitnessminornonzeroevaluationmatrixnegative. (((exists mdr_r_zero_columns_rankwitnessminornonzeroevaluationmatrixnegativepoint mdr_s_zero_columns_rankwitnessminornonzeroevaluationmatrixnegativepoint mdr_u_zero_columns_rankwitnessminornonzeroevaluationmatrixnegativepoint mdr_v_zero_columns_rankwitnessminornonzeroevaluationmatrixnegativepoint. ((mdr_i_zero_columns_rankwitnessminornonzeroevaluationmatrixnegative = (0) * mdr_r_zero_columns_rankwitnessminornonzeroevaluationmatrixnegativepoint + mdr_s_zero_columns_rankwitnessminornonzeroevaluationmatrixnegativepoint) /\ ((exists mdr_gap_zero_columns_rankwitnessminornonzeroevaluationmatrixnegativepointcolumn. mdr_gap_zero_columns_rankwitnessminornonzeroevaluationmatrixnegativepointcolumn + S (mdr_s_zero_columns_rankwitnessminornonzeroevaluationmatrixnegativepoint) = (0)) /\ ((((exists ff_h_mdr_zero_columns_rankwitnessminornonzeroevaluationmatrixnegativepointrow_index. ff_h_mdr_zero_columns_rankwitnessminornonzeroevaluationmatrixnegativepointrow_index + S (mdr_u_zero_columns_rankwitnessminornonzeroevaluationmatrixnegativepoint) = S ((S (mdr_r_zero_columns_rankwitnessminornonzeroevaluationmatrixnegativepoint)) * mdr_rc_zero_columns_rankwitness)) /\ exists ff_q_mdr_zero_columns_rankwitnessminornonzeroevaluationmatrixnegativepointrow_index. mdr_rb_zero_columns_rankwitness = ff_q_mdr_zero_columns_rankwitnessminornonzeroevaluationmatrixnegativepointrow_index * S ((S (mdr_r_zero_columns_rankwitnessminornonzeroevaluationmatrixnegativepoint)) * mdr_rc_zero_columns_rankwitness) + (mdr_u_zero_columns_rankwitnessminornonzeroevaluationmatrixnegativepoint))) /\ ((((exists ff_h_mdr_zero_columns_rankwitnessminornonzeroevaluationmatrixnegativepointcolumn_index. ff_h_mdr_zero_columns_rankwitnessminornonzeroevaluationmatrixnegativepointcolumn_index + S (mdr_v_zero_columns_rankwitnessminornonzeroevaluationmatrixnegativepoint) = S ((S (mdr_s_zero_columns_rankwitnessminornonzeroevaluationmatrixnegativepoint)) * mdr_cc_zero_columns_rankwitness)) /\ exists ff_q_mdr_zero_columns_rankwitnessminornonzeroevaluationmatrixnegativepointcolumn_index. mdr_cb_zero_columns_rankwitness = ff_q_mdr_zero_columns_rankwitnessminornonzeroevaluationmatrixnegativepointcolumn_index * S ((S (mdr_s_zero_columns_rankwitnessminornonzeroevaluationmatrixnegativepoint)) * mdr_cc_zero_columns_rankwitness) + (mdr_v_zero_columns_rankwitnessminornonzeroevaluationmatrixnegativepoint))) /\ (((exists ff_h_mdr_zero_columns_rankwitnessminornonzeroevaluationmatrixnegativepointsource. ff_h_mdr_zero_columns_rankwitnessminornonzeroevaluationmatrixnegativepointsource + S (mdr_a_zero_columns_rankwitnessminornonzeroevaluationmatrixnegative) = S ((S ((mdr_u_zero_columns_rankwitnessminornonzeroevaluationmatrixnegativepoint) * (0) + (mdr_v_zero_columns_rankwitnessminornonzeroevaluationmatrixnegativepoint))) * nc)) /\ exists ff_q_mdr_zero_columns_rankwitnessminornonzeroevaluationmatrixnegativepointsource. nb = ff_q_mdr_zero_columns_rankwitnessminornonzeroevaluationmatrixnegativepointsource * S ((S ((mdr_u_zero_columns_rankwitnessminornonzeroevaluationmatrixnegativepoint) * (0) + (mdr_v_zero_columns_rankwitnessminornonzeroevaluationmatrixnegativepoint))) * nc) + (mdr_a_zero_columns_rankwitnessminornonzeroevaluationmatrixnegative)))))))) /\ (((exists ff_h_mdr_zero_columns_rankwitnessminornonzeroevaluationmatrixnegativeoutput. ff_h_mdr_zero_columns_rankwitnessminornonzeroevaluationmatrixnegativeoutput + S (mdr_a_zero_columns_rankwitnessminornonzeroevaluationmatrixnegative) = S ((S (mdr_i_zero_columns_rankwitnessminornonzeroevaluationmatrixnegative)) * mdr_vc_zero_columns_rankwitnessminornonzeroevaluation)) /\ exists ff_q_mdr_zero_columns_rankwitnessminornonzeroevaluationmatrixnegativeoutput. mdr_vb_zero_columns_rankwitnessminornonzeroevaluation = ff_q_mdr_zero_columns_rankwitnessminornonzeroevaluationmatrixnegativeoutput * S ((S (mdr_i_zero_columns_rankwitnessminornonzeroevaluationmatrixnegative)) * mdr_vc_zero_columns_rankwitnessminornonzeroevaluation) + (mdr_a_zero_columns_rankwitnessminornonzeroevaluationmatrixnegative)))))))) /\ (exists mdr_b_zero_columns_rankwitnessminornonzeroevaluationdeterminant mdr_c_zero_columns_rankwitnessminornonzeroevaluationdeterminant mdr_l_zero_columns_rankwitnessminornonzeroevaluationdeterminant mdr_i_zero_columns_rankwitnessminornonzeroevaluationdeterminant. ((forall mdr_i_zero_columns_rankwitnessminornonzeroevaluationdeterminanth. (exists mdr_gap_zero_columns_rankwitnessminornonzeroevaluationdeterminanthi. mdr_gap_zero_columns_rankwitnessminornonzeroevaluationdeterminanthi + S (mdr_i_zero_columns_rankwitnessminornonzeroevaluationdeterminanth) = (mdr_l_zero_columns_rankwitnessminornonzeroevaluationdeterminant)) -> exists mdr_d_zero_columns_rankwitnessminornonzeroevaluationdeterminanth mdr_pb_zero_columns_rankwitnessminornonzeroevaluationdeterminanth mdr_pc_zero_columns_rankwitnessminornonzeroevaluationdeterminanth mdr_nb_zero_columns_rankwitnessminornonzeroevaluationdeterminanth mdr_nc_zero_columns_rankwitnessminornonzeroevaluationdeterminanth mdr_p_zero_columns_rankwitnessminornonzeroevaluationdeterminanth mdr_n_zero_columns_rankwitnessminornonzeroevaluationdeterminanth. ((exists mdr_z_zero_columns_rankwitnessminornonzeroevaluationdeterminanthr. ((exists mdr_a_zero_columns_rankwitnessminornonzeroevaluationdeterminanthrc mdr_b_zero_columns_rankwitnessminornonzeroevaluationdeterminanthrc mdr_c_zero_columns_rankwitnessminornonzeroevaluationdeterminanthrc mdr_e_zero_columns_rankwitnessminornonzeroevaluationdeterminanthrc mdr_f_zero_columns_rankwitnessminornonzeroevaluationdeterminanthrc. ((mdr_a_zero_columns_rankwitnessminornonzeroevaluationdeterminanthrc = ((mdr_d_zero_columns_rankwitnessminornonzeroevaluationdeterminanth) + (mdr_pb_zero_columns_rankwitnessminornonzeroevaluationdeterminanth)) * S ((mdr_d_zero_columns_rankwitnessminornonzeroevaluationdeterminanth) + (mdr_pb_zero_columns_rankwitnessminornonzeroevaluationdeterminanth)) + ((mdr_pb_zero_columns_rankwitnessminornonzeroevaluationdeterminanth) + (mdr_pb_zero_columns_rankwitnessminornonzeroevaluationdeterminanth))) /\ ((mdr_b_zero_columns_rankwitnessminornonzeroevaluationdeterminanthrc = ((mdr_pc_zero_columns_rankwitnessminornonzeroevaluationdeterminanth) + (mdr_nb_zero_columns_rankwitnessminornonzeroevaluationdeterminanth)) * S ((mdr_pc_zero_columns_rankwitnessminornonzeroevaluationdeterminanth) + (mdr_nb_zero_columns_rankwitnessminornonzeroevaluationdeterminanth)) + ((mdr_nb_zero_columns_rankwitnessminornonzeroevaluationdeterminanth) + (mdr_nb_zero_columns_rankwitnessminornonzeroevaluationdeterminanth))) /\ ((mdr_c_zero_columns_rankwitnessminornonzeroevaluationdeterminanthrc = ((mdr_a_zero_columns_rankwitnessminornonzeroevaluationdeterminanthrc) + (mdr_b_zero_columns_rankwitnessminornonzeroevaluationdeterminanthrc)) * S ((mdr_a_zero_columns_rankwitnessminornonzeroevaluationdeterminanthrc) + (mdr_b_zero_columns_rankwitnessminornonzeroevaluationdeterminanthrc)) + ((mdr_b_zero_columns_rankwitnessminornonzeroevaluationdeterminanthrc) + (mdr_b_zero_columns_rankwitnessminornonzeroevaluationdeterminanthrc))) /\ ((mdr_e_zero_columns_rankwitnessminornonzeroevaluationdeterminanthrc = ((mdr_p_zero_columns_rankwitnessminornonzeroevaluationdeterminanth) + (mdr_n_zero_columns_rankwitnessminornonzeroevaluationdeterminanth)) * S ((mdr_p_zero_columns_rankwitnessminornonzeroevaluationdeterminanth) + (mdr_n_zero_columns_rankwitnessminornonzeroevaluationdeterminanth)) + ((mdr_n_zero_columns_rankwitnessminornonzeroevaluationdeterminanth) + (mdr_n_zero_columns_rankwitnessminornonzeroevaluationdeterminanth))) /\ ((mdr_f_zero_columns_rankwitnessminornonzeroevaluationdeterminanthrc = ((mdr_nc_zero_columns_rankwitnessminornonzeroevaluationdeterminanth) + (mdr_e_zero_columns_rankwitnessminornonzeroevaluationdeterminanthrc)) * S ((mdr_nc_zero_columns_rankwitnessminornonzeroevaluationdeterminanth) + (mdr_e_zero_columns_rankwitnessminornonzeroevaluationdeterminanthrc)) + ((mdr_e_zero_columns_rankwitnessminornonzeroevaluationdeterminanthrc) + (mdr_e_zero_columns_rankwitnessminornonzeroevaluationdeterminanthrc))) /\ ((mdr_z_zero_columns_rankwitnessminornonzeroevaluationdeterminanthr) = ((mdr_c_zero_columns_rankwitnessminornonzeroevaluationdeterminanthrc) + (mdr_f_zero_columns_rankwitnessminornonzeroevaluationdeterminanthrc)) * S ((mdr_c_zero_columns_rankwitnessminornonzeroevaluationdeterminanthrc) + (mdr_f_zero_columns_rankwitnessminornonzeroevaluationdeterminanthrc)) + ((mdr_f_zero_columns_rankwitnessminornonzeroevaluationdeterminanthrc) + (mdr_f_zero_columns_rankwitnessminornonzeroevaluationdeterminanthrc))))))))) /\ (((exists ff_h_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthrb. ff_h_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthrb + S (mdr_z_zero_columns_rankwitnessminornonzeroevaluationdeterminanthr) = S ((S (mdr_i_zero_columns_rankwitnessminornonzeroevaluationdeterminanth)) * mdr_c_zero_columns_rankwitnessminornonzeroevaluationdeterminant)) /\ exists ff_q_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthrb. mdr_b_zero_columns_rankwitnessminornonzeroevaluationdeterminant = ff_q_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthrb * S ((S (mdr_i_zero_columns_rankwitnessminornonzeroevaluationdeterminanth)) * mdr_c_zero_columns_rankwitnessminornonzeroevaluationdeterminant) + (mdr_z_zero_columns_rankwitnessminornonzeroevaluationdeterminanthr))))) /\ (((((mdr_d_zero_columns_rankwitnessminornonzeroevaluationdeterminanth) = 0) /\ (((mdr_p_zero_columns_rankwitnessminornonzeroevaluationdeterminanth) = 1) /\ ((mdr_n_zero_columns_rankwitnessminornonzeroevaluationdeterminanth) = 0))) \/ exists mdr_q_zero_columns_rankwitnessminornonzeroevaluationdeterminanths mdr_eb_zero_columns_rankwitnessminornonzeroevaluationdeterminanths mdr_ec_zero_columns_rankwitnessminornonzeroevaluationdeterminanths mdr_fb_zero_columns_rankwitnessminornonzeroevaluationdeterminanths mdr_fc_zero_columns_rankwitnessminornonzeroevaluationdeterminanths. (((mdr_d_zero_columns_rankwitnessminornonzeroevaluationdeterminanth) = S (mdr_q_zero_columns_rankwitnessminornonzeroevaluationdeterminanths)) /\ ((forall mdr_j_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsc. (exists mdr_gap_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscj. mdr_gap_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscj + S (mdr_j_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsc) = (S (mdr_q_zero_columns_rankwitnessminornonzeroevaluationdeterminanths))) -> exists mdr_i_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsc mdr_up_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsc mdr_us_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsc mdr_un_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsc mdr_ut_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsc mdr_p_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsc mdr_n_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsc. ((exists mdr_gap_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsci. mdr_gap_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsci + S (mdr_i_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsc) = (mdr_i_zero_columns_rankwitnessminornonzeroevaluationdeterminanth)) /\ ((exists mdr_z_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscr. ((exists mdr_a_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscrc mdr_b_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscrc mdr_c_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscrc mdr_e_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscrc mdr_f_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscrc. ((mdr_a_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscrc = ((mdr_q_zero_columns_rankwitnessminornonzeroevaluationdeterminanths) + (mdr_up_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsc)) * S ((mdr_q_zero_columns_rankwitnessminornonzeroevaluationdeterminanths) + (mdr_up_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsc)) + ((mdr_up_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsc) + (mdr_up_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsc))) /\ ((mdr_b_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscrc = ((mdr_us_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsc) + (mdr_un_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsc)) * S ((mdr_us_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsc) + (mdr_un_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsc)) + ((mdr_un_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsc) + (mdr_un_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsc))) /\ ((mdr_c_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscrc = ((mdr_a_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscrc) + (mdr_b_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscrc)) * S ((mdr_a_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscrc) + (mdr_b_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscrc)) + ((mdr_b_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscrc) + (mdr_b_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscrc))) /\ ((mdr_e_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscrc = ((mdr_p_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsc) + (mdr_n_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsc)) * S ((mdr_p_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsc) + (mdr_n_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsc)) + ((mdr_n_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsc) + (mdr_n_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsc))) /\ ((mdr_f_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscrc = ((mdr_ut_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsc) + (mdr_e_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscrc)) * S ((mdr_ut_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsc) + (mdr_e_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscrc)) + ((mdr_e_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscrc) + (mdr_e_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscrc))) /\ ((mdr_z_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscr) = ((mdr_c_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscrc) + (mdr_f_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscrc)) * S ((mdr_c_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscrc) + (mdr_f_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscrc)) + ((mdr_f_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscrc) + (mdr_f_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscrc))))))))) /\ (((exists ff_h_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscrb. ff_h_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscrb + S (mdr_z_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscr) = S ((S (mdr_i_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsc)) * mdr_c_zero_columns_rankwitnessminornonzeroevaluationdeterminant)) /\ exists ff_q_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscrb. mdr_b_zero_columns_rankwitnessminornonzeroevaluationdeterminant = ff_q_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscrb * S ((S (mdr_i_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsc)) * mdr_c_zero_columns_rankwitnessminornonzeroevaluationdeterminant) + (mdr_z_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscm_positive. (exists ff_gap_mdm_lt_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscm_positive_index_bound. ff_gap_mdm_lt_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscm_positive) = ((mdr_q_zero_columns_rankwitnessminornonzeroevaluationdeterminanths) * (mdr_q_zero_columns_rankwitnessminornonzeroevaluationdeterminanths))) -> exists ff_row_mdm_prefix_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscm_positive ff_column_mdm_prefix_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscm_positive ff_value_mdm_prefix_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscm_positive. (ff_index_mdm_prefix_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscm_positive = (mdr_q_zero_columns_rankwitnessminornonzeroevaluationdeterminanths) * ff_row_mdm_prefix_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscm_positive + ff_column_mdm_prefix_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscm_positive /\ ((exists ff_gap_mdm_lt_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscm_positive_column_bound. ff_gap_mdm_lt_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscm_positive) = (mdr_q_zero_columns_rankwitnessminornonzeroevaluationdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell ff_column_mdm_cell_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell = ff_row_mdm_prefix_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell_row_after. ff_gap_mdm_le_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscm_positive)) /\ ff_row_mdm_cell_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell = S ff_row_mdm_prefix_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscm_positive) = (mdr_j_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsc)) /\ ff_column_mdm_cell_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell = ff_column_mdm_prefix_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell_column_after. ff_gap_mdm_le_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell_column_after + (mdr_j_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsc) = (ff_column_mdm_prefix_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscm_positive)) /\ ff_column_mdm_cell_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell = S ff_column_mdm_prefix_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscm_positive))) /\ (((exists ff_h_mdm_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell_source. ff_h_mdm_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscm_positive) = S ((S ((ff_row_mdm_cell_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell) * (S (mdr_q_zero_columns_rankwitnessminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell))) * mdr_pc_zero_columns_rankwitnessminornonzeroevaluationdeterminanth)) /\ exists ff_q_mdm_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell_source. mdr_pb_zero_columns_rankwitnessminornonzeroevaluationdeterminanth = ff_q_mdm_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell) * (S (mdr_q_zero_columns_rankwitnessminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell))) * mdr_pc_zero_columns_rankwitnessminornonzeroevaluationdeterminanth) + (ff_value_mdm_prefix_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscm_positive)))))) /\ (((exists ff_h_mdm_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscm_positive_target. ff_h_mdm_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscm_positive_target + S (ff_value_mdm_prefix_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscm_positive) = S ((S (ff_index_mdm_prefix_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscm_positive)) * mdr_us_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsc)) /\ exists ff_q_mdm_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscm_positive_target. mdr_up_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsc = ff_q_mdm_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscm_positive)) * mdr_us_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsc) + (ff_value_mdm_prefix_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscm_negative. (exists ff_gap_mdm_lt_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscm_negative_index_bound. ff_gap_mdm_lt_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscm_negative) = ((mdr_q_zero_columns_rankwitnessminornonzeroevaluationdeterminanths) * (mdr_q_zero_columns_rankwitnessminornonzeroevaluationdeterminanths))) -> exists ff_row_mdm_prefix_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscm_negative ff_column_mdm_prefix_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscm_negative ff_value_mdm_prefix_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscm_negative. (ff_index_mdm_prefix_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscm_negative = (mdr_q_zero_columns_rankwitnessminornonzeroevaluationdeterminanths) * ff_row_mdm_prefix_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscm_negative + ff_column_mdm_prefix_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscm_negative /\ ((exists ff_gap_mdm_lt_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscm_negative_column_bound. ff_gap_mdm_lt_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscm_negative) = (mdr_q_zero_columns_rankwitnessminornonzeroevaluationdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell ff_column_mdm_cell_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell = ff_row_mdm_prefix_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell_row_after. ff_gap_mdm_le_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscm_negative)) /\ ff_row_mdm_cell_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell = S ff_row_mdm_prefix_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscm_negative) = (mdr_j_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsc)) /\ ff_column_mdm_cell_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell = ff_column_mdm_prefix_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell_column_after. ff_gap_mdm_le_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell_column_after + (mdr_j_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsc) = (ff_column_mdm_prefix_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscm_negative)) /\ ff_column_mdm_cell_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell = S ff_column_mdm_prefix_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscm_negative))) /\ (((exists ff_h_mdm_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell_source. ff_h_mdm_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscm_negative) = S ((S ((ff_row_mdm_cell_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell) * (S (mdr_q_zero_columns_rankwitnessminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell))) * mdr_nc_zero_columns_rankwitnessminornonzeroevaluationdeterminanth)) /\ exists ff_q_mdm_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell_source. mdr_nb_zero_columns_rankwitnessminornonzeroevaluationdeterminanth = ff_q_mdm_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell) * (S (mdr_q_zero_columns_rankwitnessminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell))) * mdr_nc_zero_columns_rankwitnessminornonzeroevaluationdeterminanth) + (ff_value_mdm_prefix_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscm_negative)))))) /\ (((exists ff_h_mdm_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscm_negative_target. ff_h_mdm_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscm_negative_target + S (ff_value_mdm_prefix_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscm_negative) = S ((S (ff_index_mdm_prefix_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscm_negative)) * mdr_ut_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsc)) /\ exists ff_q_mdm_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscm_negative_target. mdr_un_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsc = ff_q_mdm_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscm_negative)) * mdr_ut_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsc) + (ff_value_mdm_prefix_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscm_negative))))))))) /\ ((((exists ff_h_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscp. ff_h_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscp + S (mdr_p_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsc) = S ((S (mdr_j_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsc)) * mdr_ec_zero_columns_rankwitnessminornonzeroevaluationdeterminanths)) /\ exists ff_q_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscp. mdr_eb_zero_columns_rankwitnessminornonzeroevaluationdeterminanths = ff_q_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscp * S ((S (mdr_j_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsc)) * mdr_ec_zero_columns_rankwitnessminornonzeroevaluationdeterminanths) + (mdr_p_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsc))) /\ (((exists ff_h_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscn. ff_h_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscn + S (mdr_n_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsc) = S ((S (mdr_j_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsc)) * mdr_fc_zero_columns_rankwitnessminornonzeroevaluationdeterminanths)) /\ exists ff_q_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscn. mdr_fb_zero_columns_rankwitnessminornonzeroevaluationdeterminanths = ff_q_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthscn * S ((S (mdr_j_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsc)) * mdr_fc_zero_columns_rankwitnessminornonzeroevaluationdeterminanths) + (mdr_n_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsc)))))))) /\ (exists ff_ub_mce_fold_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf ff_uc_mce_fold_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf ff_vb_mce_fold_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf ff_vc_mce_fold_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf. ((forall ff_index_mce_alternating_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_prefix. (exists ff_gap_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_index. ff_gap_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_index + S (ff_index_mce_alternating_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) = (S (mdr_q_zero_columns_rankwitnessminornonzeroevaluationdeterminanths))) -> exists ff_ap_mce_alternating_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_prefix ff_an_mce_alternating_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_prefix ff_bp_mce_alternating_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_prefix ff_bn_mce_alternating_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_prefix ff_p_mce_alternating_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_prefix ff_n_mce_alternating_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_prefix. ((((exists ff_h_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_ap. ff_h_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_ap + S (ff_ap_mce_alternating_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_prefix)) * mdr_pc_zero_columns_rankwitnessminornonzeroevaluationdeterminanth)) /\ exists ff_q_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_ap. mdr_pb_zero_columns_rankwitnessminornonzeroevaluationdeterminanth = ff_q_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_prefix)) * mdr_pc_zero_columns_rankwitnessminornonzeroevaluationdeterminanth) + (ff_ap_mce_alternating_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_an. ff_h_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_an + S (ff_an_mce_alternating_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_prefix)) * mdr_nc_zero_columns_rankwitnessminornonzeroevaluationdeterminanth)) /\ exists ff_q_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_an. mdr_nb_zero_columns_rankwitnessminornonzeroevaluationdeterminanth = ff_q_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_prefix)) * mdr_nc_zero_columns_rankwitnessminornonzeroevaluationdeterminanth) + (ff_an_mce_alternating_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_bp. ff_h_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_bp + S (ff_bp_mce_alternating_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_prefix)) * mdr_ec_zero_columns_rankwitnessminornonzeroevaluationdeterminanths)) /\ exists ff_q_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_bp. mdr_eb_zero_columns_rankwitnessminornonzeroevaluationdeterminanths = ff_q_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_prefix)) * mdr_ec_zero_columns_rankwitnessminornonzeroevaluationdeterminanths) + (ff_bp_mce_alternating_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_bn. ff_h_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_bn + S (ff_bn_mce_alternating_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_prefix)) * mdr_fc_zero_columns_rankwitnessminornonzeroevaluationdeterminanths)) /\ exists ff_q_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_bn. mdr_fb_zero_columns_rankwitnessminornonzeroevaluationdeterminanths = ff_q_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_prefix)) * mdr_fc_zero_columns_rankwitnessminornonzeroevaluationdeterminanths) + (ff_bn_mce_alternating_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_positive. ff_h_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_positive + S (ff_p_mce_alternating_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_positive. ff_ub_mce_fold_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf) + (ff_p_mce_alternating_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_negative. ff_h_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_negative + S (ff_n_mce_alternating_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_negative. ff_vb_mce_fold_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf) + (ff_n_mce_alternating_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_prefix))) /\ (((exists ff_even_mce_term_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_prefix = 2 * ff_even_mce_term_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_term) /\ (ff_p_mce_alternating_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_prefix = 2 * ff_odd_mce_term_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_positive ff_v_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_positive. ((((exists ff_h_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_positive_start. ff_h_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_positive_start. ff_u_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_positive_start * S ((S (0)) * ff_v_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_positive_terminal. ff_h_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_positive_terminal + S (mdr_p_zero_columns_rankwitnessminornonzeroevaluationdeterminanth) = S ((S ((S (mdr_q_zero_columns_rankwitnessminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_positive_terminal. ff_u_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_positive_terminal * S ((S ((S (mdr_q_zero_columns_rankwitnessminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_positive) + (mdr_p_zero_columns_rankwitnessminornonzeroevaluationdeterminanth))) /\ forall ff_i_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_positive. (exists ff_lt_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_positive_bound. ff_lt_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_positive_bound + S ff_i_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_positive = (S (mdr_q_zero_columns_rankwitnessminornonzeroevaluationdeterminanths))) -> exists ff_a_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_positive ff_r_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_positive ff_s_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_positive. ((((exists ff_h_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_positive_summand. ff_h_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_positive_summand + S (ff_a_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_positive_summand. ff_ub_mce_fold_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_positive_summand * S ((S (ff_i_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf) + (ff_a_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_positive_partial. ff_h_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_positive_partial + S (ff_r_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_positive_partial. ff_u_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_positive_partial * S ((S (ff_i_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_positive) + (ff_r_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_positive_successor. ff_h_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_positive_successor + S (ff_s_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_positive) = S ((S (S ff_i_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_positive_successor. ff_u_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_positive_successor * S ((S (S ff_i_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_positive) + (ff_s_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_positive))) /\ ff_s_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_positive = ff_r_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_positive + ff_a_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_positive)))))) /\ (exists ff_u_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_negative ff_v_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_negative. ((((exists ff_h_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_negative_start. ff_h_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_negative_start. ff_u_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_negative_start * S ((S (0)) * ff_v_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_negative_terminal. ff_h_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_negative_terminal + S (mdr_n_zero_columns_rankwitnessminornonzeroevaluationdeterminanth) = S ((S ((S (mdr_q_zero_columns_rankwitnessminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_negative_terminal. ff_u_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_negative_terminal * S ((S ((S (mdr_q_zero_columns_rankwitnessminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_negative) + (mdr_n_zero_columns_rankwitnessminornonzeroevaluationdeterminanth))) /\ forall ff_i_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_negative. (exists ff_lt_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_negative_bound. ff_lt_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_negative_bound + S ff_i_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_negative = (S (mdr_q_zero_columns_rankwitnessminornonzeroevaluationdeterminanths))) -> exists ff_a_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_negative ff_r_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_negative ff_s_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_negative. ((((exists ff_h_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_negative_summand. ff_h_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_negative_summand + S (ff_a_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_negative_summand. ff_vb_mce_fold_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_negative_summand * S ((S (ff_i_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf) + (ff_a_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_negative_partial. ff_h_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_negative_partial + S (ff_r_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_negative_partial. ff_u_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_negative_partial * S ((S (ff_i_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_negative) + (ff_r_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_negative_successor. ff_h_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_negative_successor + S (ff_s_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_negative) = S ((S (S ff_i_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_negative_successor. ff_u_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_negative_successor * S ((S (S ff_i_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_negative) + (ff_s_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_negative))) /\ ff_s_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_negative = ff_r_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_negative + ff_a_mce_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminanthsf_negative))))))))))))))) /\ ((exists mdr_gap_zero_columns_rankwitnessminornonzeroevaluationdeterminanti. mdr_gap_zero_columns_rankwitnessminornonzeroevaluationdeterminanti + S (mdr_i_zero_columns_rankwitnessminornonzeroevaluationdeterminant) = (mdr_l_zero_columns_rankwitnessminornonzeroevaluationdeterminant)) /\ (exists mdr_z_zero_columns_rankwitnessminornonzeroevaluationdeterminantr. ((exists mdr_a_zero_columns_rankwitnessminornonzeroevaluationdeterminantrc mdr_b_zero_columns_rankwitnessminornonzeroevaluationdeterminantrc mdr_c_zero_columns_rankwitnessminornonzeroevaluationdeterminantrc mdr_e_zero_columns_rankwitnessminornonzeroevaluationdeterminantrc mdr_f_zero_columns_rankwitnessminornonzeroevaluationdeterminantrc. ((mdr_a_zero_columns_rankwitnessminornonzeroevaluationdeterminantrc = ((0) + (mdr_ub_zero_columns_rankwitnessminornonzeroevaluation)) * S ((0) + (mdr_ub_zero_columns_rankwitnessminornonzeroevaluation)) + ((mdr_ub_zero_columns_rankwitnessminornonzeroevaluation) + (mdr_ub_zero_columns_rankwitnessminornonzeroevaluation))) /\ ((mdr_b_zero_columns_rankwitnessminornonzeroevaluationdeterminantrc = ((mdr_uc_zero_columns_rankwitnessminornonzeroevaluation) + (mdr_vb_zero_columns_rankwitnessminornonzeroevaluation)) * S ((mdr_uc_zero_columns_rankwitnessminornonzeroevaluation) + (mdr_vb_zero_columns_rankwitnessminornonzeroevaluation)) + ((mdr_vb_zero_columns_rankwitnessminornonzeroevaluation) + (mdr_vb_zero_columns_rankwitnessminornonzeroevaluation))) /\ ((mdr_c_zero_columns_rankwitnessminornonzeroevaluationdeterminantrc = ((mdr_a_zero_columns_rankwitnessminornonzeroevaluationdeterminantrc) + (mdr_b_zero_columns_rankwitnessminornonzeroevaluationdeterminantrc)) * S ((mdr_a_zero_columns_rankwitnessminornonzeroevaluationdeterminantrc) + (mdr_b_zero_columns_rankwitnessminornonzeroevaluationdeterminantrc)) + ((mdr_b_zero_columns_rankwitnessminornonzeroevaluationdeterminantrc) + (mdr_b_zero_columns_rankwitnessminornonzeroevaluationdeterminantrc))) /\ ((mdr_e_zero_columns_rankwitnessminornonzeroevaluationdeterminantrc = ((mdr_p_zero_columns_rankwitnessminornonzero) + (mdr_n_zero_columns_rankwitnessminornonzero)) * S ((mdr_p_zero_columns_rankwitnessminornonzero) + (mdr_n_zero_columns_rankwitnessminornonzero)) + ((mdr_n_zero_columns_rankwitnessminornonzero) + (mdr_n_zero_columns_rankwitnessminornonzero))) /\ ((mdr_f_zero_columns_rankwitnessminornonzeroevaluationdeterminantrc = ((mdr_vc_zero_columns_rankwitnessminornonzeroevaluation) + (mdr_e_zero_columns_rankwitnessminornonzeroevaluationdeterminantrc)) * S ((mdr_vc_zero_columns_rankwitnessminornonzeroevaluation) + (mdr_e_zero_columns_rankwitnessminornonzeroevaluationdeterminantrc)) + ((mdr_e_zero_columns_rankwitnessminornonzeroevaluationdeterminantrc) + (mdr_e_zero_columns_rankwitnessminornonzeroevaluationdeterminantrc))) /\ ((mdr_z_zero_columns_rankwitnessminornonzeroevaluationdeterminantr) = ((mdr_c_zero_columns_rankwitnessminornonzeroevaluationdeterminantrc) + (mdr_f_zero_columns_rankwitnessminornonzeroevaluationdeterminantrc)) * S ((mdr_c_zero_columns_rankwitnessminornonzeroevaluationdeterminantrc) + (mdr_f_zero_columns_rankwitnessminornonzeroevaluationdeterminantrc)) + ((mdr_f_zero_columns_rankwitnessminornonzeroevaluationdeterminantrc) + (mdr_f_zero_columns_rankwitnessminornonzeroevaluationdeterminantrc))))))))) /\ (((exists ff_h_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminantrb. ff_h_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminantrb + S (mdr_z_zero_columns_rankwitnessminornonzeroevaluationdeterminantr) = S ((S (mdr_i_zero_columns_rankwitnessminornonzeroevaluationdeterminant)) * mdr_c_zero_columns_rankwitnessminornonzeroevaluationdeterminant)) /\ exists ff_q_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminantrb. mdr_b_zero_columns_rankwitnessminornonzeroevaluationdeterminant = ff_q_mdr_zero_columns_rankwitnessminornonzeroevaluationdeterminantrb * S ((S (mdr_i_zero_columns_rankwitnessminornonzeroevaluationdeterminant)) * mdr_c_zero_columns_rankwitnessminornonzeroevaluationdeterminant) + (mdr_z_zero_columns_rankwitnessminornonzeroevaluationdeterminantr)))))))))) /\ (~(mdr_p_zero_columns_rankwitnessminornonzero = mdr_n_zero_columns_rankwitnessminornonzero)))))))) /\ (forall mdr_q_zero_columns_rank. (exists mdr_gap_zero_columns_rankhigher. mdr_gap_zero_columns_rankhigher + S (0) = (mdr_q_zero_columns_rank)) -> (forall mdr_rb_zero_columns_rankzero mdr_rc_zero_columns_rankzero mdr_cb_zero_columns_rankzero mdr_cc_zero_columns_rankzero mdr_p_zero_columns_rankzero mdr_n_zero_columns_rankzero. (((forall fom_index_mrf_zero_columns_rankzerorowsbound. (exists fom_gap_mrf_zero_columns_rankzerorowsbound_index_bound. fom_gap_mrf_zero_columns_rankzerorowsbound_index_bound + S (fom_index_mrf_zero_columns_rankzerorowsbound) = mdr_q_zero_columns_rank) -> exists fom_value_mrf_zero_columns_rankzerorowsbound. ((((exists fom_beta_height_mrf_zero_columns_rankzerorowsbound_entry. fom_beta_height_mrf_zero_columns_rankzerorowsbound_entry + S (fom_value_mrf_zero_columns_rankzerorowsbound) = S ((S (fom_index_mrf_zero_columns_rankzerorowsbound)) * mdr_rc_zero_columns_rankzero)) /\ exists fom_beta_quotient_mrf_zero_columns_rankzerorowsbound_entry. mdr_rb_zero_columns_rankzero = fom_beta_quotient_mrf_zero_columns_rankzerorowsbound_entry * S ((S (fom_index_mrf_zero_columns_rankzerorowsbound)) * mdr_rc_zero_columns_rankzero) + (fom_value_mrf_zero_columns_rankzerorowsbound))) /\ (exists fom_gap_mrf_zero_columns_rankzerorowsbound_value_bound. fom_gap_mrf_zero_columns_rankzerorowsbound_value_bound + S (fom_value_mrf_zero_columns_rankzerorowsbound) = r))) /\ (forall mdr_i_zero_columns_rankzerorowsdistinct mdr_j_zero_columns_rankzerorowsdistinct mdr_a_zero_columns_rankzerorowsdistinct. (exists mdr_gap_zero_columns_rankzerorowsdistincti. mdr_gap_zero_columns_rankzerorowsdistincti + S (mdr_i_zero_columns_rankzerorowsdistinct) = (mdr_q_zero_columns_rank)) -> (exists mdr_gap_zero_columns_rankzerorowsdistinctj. mdr_gap_zero_columns_rankzerorowsdistinctj + S (mdr_j_zero_columns_rankzerorowsdistinct) = (mdr_q_zero_columns_rank)) -> (((exists ff_h_mdr_zero_columns_rankzerorowsdistinctfirst. ff_h_mdr_zero_columns_rankzerorowsdistinctfirst + S (mdr_a_zero_columns_rankzerorowsdistinct) = S ((S (mdr_i_zero_columns_rankzerorowsdistinct)) * mdr_rc_zero_columns_rankzero)) /\ exists ff_q_mdr_zero_columns_rankzerorowsdistinctfirst. mdr_rb_zero_columns_rankzero = ff_q_mdr_zero_columns_rankzerorowsdistinctfirst * S ((S (mdr_i_zero_columns_rankzerorowsdistinct)) * mdr_rc_zero_columns_rankzero) + (mdr_a_zero_columns_rankzerorowsdistinct))) -> (((exists ff_h_mdr_zero_columns_rankzerorowsdistinctsecond. ff_h_mdr_zero_columns_rankzerorowsdistinctsecond + S (mdr_a_zero_columns_rankzerorowsdistinct) = S ((S (mdr_j_zero_columns_rankzerorowsdistinct)) * mdr_rc_zero_columns_rankzero)) /\ exists ff_q_mdr_zero_columns_rankzerorowsdistinctsecond. mdr_rb_zero_columns_rankzero = ff_q_mdr_zero_columns_rankzerorowsdistinctsecond * S ((S (mdr_j_zero_columns_rankzerorowsdistinct)) * mdr_rc_zero_columns_rankzero) + (mdr_a_zero_columns_rankzerorowsdistinct))) -> mdr_i_zero_columns_rankzerorowsdistinct = mdr_j_zero_columns_rankzerorowsdistinct))) -> (((forall fom_index_mrf_zero_columns_rankzerocolumnsbound. (exists fom_gap_mrf_zero_columns_rankzerocolumnsbound_index_bound. fom_gap_mrf_zero_columns_rankzerocolumnsbound_index_bound + S (fom_index_mrf_zero_columns_rankzerocolumnsbound) = mdr_q_zero_columns_rank) -> exists fom_value_mrf_zero_columns_rankzerocolumnsbound. ((((exists fom_beta_height_mrf_zero_columns_rankzerocolumnsbound_entry. fom_beta_height_mrf_zero_columns_rankzerocolumnsbound_entry + S (fom_value_mrf_zero_columns_rankzerocolumnsbound) = S ((S (fom_index_mrf_zero_columns_rankzerocolumnsbound)) * mdr_cc_zero_columns_rankzero)) /\ exists fom_beta_quotient_mrf_zero_columns_rankzerocolumnsbound_entry. mdr_cb_zero_columns_rankzero = fom_beta_quotient_mrf_zero_columns_rankzerocolumnsbound_entry * S ((S (fom_index_mrf_zero_columns_rankzerocolumnsbound)) * mdr_cc_zero_columns_rankzero) + (fom_value_mrf_zero_columns_rankzerocolumnsbound))) /\ (exists fom_gap_mrf_zero_columns_rankzerocolumnsbound_value_bound. fom_gap_mrf_zero_columns_rankzerocolumnsbound_value_bound + S (fom_value_mrf_zero_columns_rankzerocolumnsbound) = 0))) /\ (forall mdr_i_zero_columns_rankzerocolumnsdistinct mdr_j_zero_columns_rankzerocolumnsdistinct mdr_a_zero_columns_rankzerocolumnsdistinct. (exists mdr_gap_zero_columns_rankzerocolumnsdistincti. mdr_gap_zero_columns_rankzerocolumnsdistincti + S (mdr_i_zero_columns_rankzerocolumnsdistinct) = (mdr_q_zero_columns_rank)) -> (exists mdr_gap_zero_columns_rankzerocolumnsdistinctj. mdr_gap_zero_columns_rankzerocolumnsdistinctj + S (mdr_j_zero_columns_rankzerocolumnsdistinct) = (mdr_q_zero_columns_rank)) -> (((exists ff_h_mdr_zero_columns_rankzerocolumnsdistinctfirst. ff_h_mdr_zero_columns_rankzerocolumnsdistinctfirst + S (mdr_a_zero_columns_rankzerocolumnsdistinct) = S ((S (mdr_i_zero_columns_rankzerocolumnsdistinct)) * mdr_cc_zero_columns_rankzero)) /\ exists ff_q_mdr_zero_columns_rankzerocolumnsdistinctfirst. mdr_cb_zero_columns_rankzero = ff_q_mdr_zero_columns_rankzerocolumnsdistinctfirst * S ((S (mdr_i_zero_columns_rankzerocolumnsdistinct)) * mdr_cc_zero_columns_rankzero) + (mdr_a_zero_columns_rankzerocolumnsdistinct))) -> (((exists ff_h_mdr_zero_columns_rankzerocolumnsdistinctsecond. ff_h_mdr_zero_columns_rankzerocolumnsdistinctsecond + S (mdr_a_zero_columns_rankzerocolumnsdistinct) = S ((S (mdr_j_zero_columns_rankzerocolumnsdistinct)) * mdr_cc_zero_columns_rankzero)) /\ exists ff_q_mdr_zero_columns_rankzerocolumnsdistinctsecond. mdr_cb_zero_columns_rankzero = ff_q_mdr_zero_columns_rankzerocolumnsdistinctsecond * S ((S (mdr_j_zero_columns_rankzerocolumnsdistinct)) * mdr_cc_zero_columns_rankzero) + (mdr_a_zero_columns_rankzerocolumnsdistinct))) -> mdr_i_zero_columns_rankzerocolumnsdistinct = mdr_j_zero_columns_rankzerocolumnsdistinct))) -> (exists mdr_ub_zero_columns_rankzeroevaluation mdr_uc_zero_columns_rankzeroevaluation mdr_vb_zero_columns_rankzeroevaluation mdr_vc_zero_columns_rankzeroevaluation. ((((forall mdr_i_zero_columns_rankzeroevaluationmatrixpositive. (exists mdr_gap_zero_columns_rankzeroevaluationmatrixpositivebound. mdr_gap_zero_columns_rankzeroevaluationmatrixpositivebound + S (mdr_i_zero_columns_rankzeroevaluationmatrixpositive) = ((mdr_q_zero_columns_rank) * (mdr_q_zero_columns_rank))) -> exists mdr_a_zero_columns_rankzeroevaluationmatrixpositive. (((exists mdr_r_zero_columns_rankzeroevaluationmatrixpositivepoint mdr_s_zero_columns_rankzeroevaluationmatrixpositivepoint mdr_u_zero_columns_rankzeroevaluationmatrixpositivepoint mdr_v_zero_columns_rankzeroevaluationmatrixpositivepoint. ((mdr_i_zero_columns_rankzeroevaluationmatrixpositive = (mdr_q_zero_columns_rank) * mdr_r_zero_columns_rankzeroevaluationmatrixpositivepoint + mdr_s_zero_columns_rankzeroevaluationmatrixpositivepoint) /\ ((exists mdr_gap_zero_columns_rankzeroevaluationmatrixpositivepointcolumn. mdr_gap_zero_columns_rankzeroevaluationmatrixpositivepointcolumn + S (mdr_s_zero_columns_rankzeroevaluationmatrixpositivepoint) = (mdr_q_zero_columns_rank)) /\ ((((exists ff_h_mdr_zero_columns_rankzeroevaluationmatrixpositivepointrow_index. ff_h_mdr_zero_columns_rankzeroevaluationmatrixpositivepointrow_index + S (mdr_u_zero_columns_rankzeroevaluationmatrixpositivepoint) = S ((S (mdr_r_zero_columns_rankzeroevaluationmatrixpositivepoint)) * mdr_rc_zero_columns_rankzero)) /\ exists ff_q_mdr_zero_columns_rankzeroevaluationmatrixpositivepointrow_index. mdr_rb_zero_columns_rankzero = ff_q_mdr_zero_columns_rankzeroevaluationmatrixpositivepointrow_index * S ((S (mdr_r_zero_columns_rankzeroevaluationmatrixpositivepoint)) * mdr_rc_zero_columns_rankzero) + (mdr_u_zero_columns_rankzeroevaluationmatrixpositivepoint))) /\ ((((exists ff_h_mdr_zero_columns_rankzeroevaluationmatrixpositivepointcolumn_index. ff_h_mdr_zero_columns_rankzeroevaluationmatrixpositivepointcolumn_index + S (mdr_v_zero_columns_rankzeroevaluationmatrixpositivepoint) = S ((S (mdr_s_zero_columns_rankzeroevaluationmatrixpositivepoint)) * mdr_cc_zero_columns_rankzero)) /\ exists ff_q_mdr_zero_columns_rankzeroevaluationmatrixpositivepointcolumn_index. mdr_cb_zero_columns_rankzero = ff_q_mdr_zero_columns_rankzeroevaluationmatrixpositivepointcolumn_index * S ((S (mdr_s_zero_columns_rankzeroevaluationmatrixpositivepoint)) * mdr_cc_zero_columns_rankzero) + (mdr_v_zero_columns_rankzeroevaluationmatrixpositivepoint))) /\ (((exists ff_h_mdr_zero_columns_rankzeroevaluationmatrixpositivepointsource. ff_h_mdr_zero_columns_rankzeroevaluationmatrixpositivepointsource + S (mdr_a_zero_columns_rankzeroevaluationmatrixpositive) = S ((S ((mdr_u_zero_columns_rankzeroevaluationmatrixpositivepoint) * (0) + (mdr_v_zero_columns_rankzeroevaluationmatrixpositivepoint))) * pc)) /\ exists ff_q_mdr_zero_columns_rankzeroevaluationmatrixpositivepointsource. pb = ff_q_mdr_zero_columns_rankzeroevaluationmatrixpositivepointsource * S ((S ((mdr_u_zero_columns_rankzeroevaluationmatrixpositivepoint) * (0) + (mdr_v_zero_columns_rankzeroevaluationmatrixpositivepoint))) * pc) + (mdr_a_zero_columns_rankzeroevaluationmatrixpositive)))))))) /\ (((exists ff_h_mdr_zero_columns_rankzeroevaluationmatrixpositiveoutput. ff_h_mdr_zero_columns_rankzeroevaluationmatrixpositiveoutput + S (mdr_a_zero_columns_rankzeroevaluationmatrixpositive) = S ((S (mdr_i_zero_columns_rankzeroevaluationmatrixpositive)) * mdr_uc_zero_columns_rankzeroevaluation)) /\ exists ff_q_mdr_zero_columns_rankzeroevaluationmatrixpositiveoutput. mdr_ub_zero_columns_rankzeroevaluation = ff_q_mdr_zero_columns_rankzeroevaluationmatrixpositiveoutput * S ((S (mdr_i_zero_columns_rankzeroevaluationmatrixpositive)) * mdr_uc_zero_columns_rankzeroevaluation) + (mdr_a_zero_columns_rankzeroevaluationmatrixpositive)))))) /\ (forall mdr_i_zero_columns_rankzeroevaluationmatrixnegative. (exists mdr_gap_zero_columns_rankzeroevaluationmatrixnegativebound. mdr_gap_zero_columns_rankzeroevaluationmatrixnegativebound + S (mdr_i_zero_columns_rankzeroevaluationmatrixnegative) = ((mdr_q_zero_columns_rank) * (mdr_q_zero_columns_rank))) -> exists mdr_a_zero_columns_rankzeroevaluationmatrixnegative. (((exists mdr_r_zero_columns_rankzeroevaluationmatrixnegativepoint mdr_s_zero_columns_rankzeroevaluationmatrixnegativepoint mdr_u_zero_columns_rankzeroevaluationmatrixnegativepoint mdr_v_zero_columns_rankzeroevaluationmatrixnegativepoint. ((mdr_i_zero_columns_rankzeroevaluationmatrixnegative = (mdr_q_zero_columns_rank) * mdr_r_zero_columns_rankzeroevaluationmatrixnegativepoint + mdr_s_zero_columns_rankzeroevaluationmatrixnegativepoint) /\ ((exists mdr_gap_zero_columns_rankzeroevaluationmatrixnegativepointcolumn. mdr_gap_zero_columns_rankzeroevaluationmatrixnegativepointcolumn + S (mdr_s_zero_columns_rankzeroevaluationmatrixnegativepoint) = (mdr_q_zero_columns_rank)) /\ ((((exists ff_h_mdr_zero_columns_rankzeroevaluationmatrixnegativepointrow_index. ff_h_mdr_zero_columns_rankzeroevaluationmatrixnegativepointrow_index + S (mdr_u_zero_columns_rankzeroevaluationmatrixnegativepoint) = S ((S (mdr_r_zero_columns_rankzeroevaluationmatrixnegativepoint)) * mdr_rc_zero_columns_rankzero)) /\ exists ff_q_mdr_zero_columns_rankzeroevaluationmatrixnegativepointrow_index. mdr_rb_zero_columns_rankzero = ff_q_mdr_zero_columns_rankzeroevaluationmatrixnegativepointrow_index * S ((S (mdr_r_zero_columns_rankzeroevaluationmatrixnegativepoint)) * mdr_rc_zero_columns_rankzero) + (mdr_u_zero_columns_rankzeroevaluationmatrixnegativepoint))) /\ ((((exists ff_h_mdr_zero_columns_rankzeroevaluationmatrixnegativepointcolumn_index. ff_h_mdr_zero_columns_rankzeroevaluationmatrixnegativepointcolumn_index + S (mdr_v_zero_columns_rankzeroevaluationmatrixnegativepoint) = S ((S (mdr_s_zero_columns_rankzeroevaluationmatrixnegativepoint)) * mdr_cc_zero_columns_rankzero)) /\ exists ff_q_mdr_zero_columns_rankzeroevaluationmatrixnegativepointcolumn_index. mdr_cb_zero_columns_rankzero = ff_q_mdr_zero_columns_rankzeroevaluationmatrixnegativepointcolumn_index * S ((S (mdr_s_zero_columns_rankzeroevaluationmatrixnegativepoint)) * mdr_cc_zero_columns_rankzero) + (mdr_v_zero_columns_rankzeroevaluationmatrixnegativepoint))) /\ (((exists ff_h_mdr_zero_columns_rankzeroevaluationmatrixnegativepointsource. ff_h_mdr_zero_columns_rankzeroevaluationmatrixnegativepointsource + S (mdr_a_zero_columns_rankzeroevaluationmatrixnegative) = S ((S ((mdr_u_zero_columns_rankzeroevaluationmatrixnegativepoint) * (0) + (mdr_v_zero_columns_rankzeroevaluationmatrixnegativepoint))) * nc)) /\ exists ff_q_mdr_zero_columns_rankzeroevaluationmatrixnegativepointsource. nb = ff_q_mdr_zero_columns_rankzeroevaluationmatrixnegativepointsource * S ((S ((mdr_u_zero_columns_rankzeroevaluationmatrixnegativepoint) * (0) + (mdr_v_zero_columns_rankzeroevaluationmatrixnegativepoint))) * nc) + (mdr_a_zero_columns_rankzeroevaluationmatrixnegative)))))))) /\ (((exists ff_h_mdr_zero_columns_rankzeroevaluationmatrixnegativeoutput. ff_h_mdr_zero_columns_rankzeroevaluationmatrixnegativeoutput + S (mdr_a_zero_columns_rankzeroevaluationmatrixnegative) = S ((S (mdr_i_zero_columns_rankzeroevaluationmatrixnegative)) * mdr_vc_zero_columns_rankzeroevaluation)) /\ exists ff_q_mdr_zero_columns_rankzeroevaluationmatrixnegativeoutput. mdr_vb_zero_columns_rankzeroevaluation = ff_q_mdr_zero_columns_rankzeroevaluationmatrixnegativeoutput * S ((S (mdr_i_zero_columns_rankzeroevaluationmatrixnegative)) * mdr_vc_zero_columns_rankzeroevaluation) + (mdr_a_zero_columns_rankzeroevaluationmatrixnegative)))))))) /\ (exists mdr_b_zero_columns_rankzeroevaluationdeterminant mdr_c_zero_columns_rankzeroevaluationdeterminant mdr_l_zero_columns_rankzeroevaluationdeterminant mdr_i_zero_columns_rankzeroevaluationdeterminant. ((forall mdr_i_zero_columns_rankzeroevaluationdeterminanth. (exists mdr_gap_zero_columns_rankzeroevaluationdeterminanthi. mdr_gap_zero_columns_rankzeroevaluationdeterminanthi + S (mdr_i_zero_columns_rankzeroevaluationdeterminanth) = (mdr_l_zero_columns_rankzeroevaluationdeterminant)) -> exists mdr_d_zero_columns_rankzeroevaluationdeterminanth mdr_pb_zero_columns_rankzeroevaluationdeterminanth mdr_pc_zero_columns_rankzeroevaluationdeterminanth mdr_nb_zero_columns_rankzeroevaluationdeterminanth mdr_nc_zero_columns_rankzeroevaluationdeterminanth mdr_p_zero_columns_rankzeroevaluationdeterminanth mdr_n_zero_columns_rankzeroevaluationdeterminanth. ((exists mdr_z_zero_columns_rankzeroevaluationdeterminanthr. ((exists mdr_a_zero_columns_rankzeroevaluationdeterminanthrc mdr_b_zero_columns_rankzeroevaluationdeterminanthrc mdr_c_zero_columns_rankzeroevaluationdeterminanthrc mdr_e_zero_columns_rankzeroevaluationdeterminanthrc mdr_f_zero_columns_rankzeroevaluationdeterminanthrc. ((mdr_a_zero_columns_rankzeroevaluationdeterminanthrc = ((mdr_d_zero_columns_rankzeroevaluationdeterminanth) + (mdr_pb_zero_columns_rankzeroevaluationdeterminanth)) * S ((mdr_d_zero_columns_rankzeroevaluationdeterminanth) + (mdr_pb_zero_columns_rankzeroevaluationdeterminanth)) + ((mdr_pb_zero_columns_rankzeroevaluationdeterminanth) + (mdr_pb_zero_columns_rankzeroevaluationdeterminanth))) /\ ((mdr_b_zero_columns_rankzeroevaluationdeterminanthrc = ((mdr_pc_zero_columns_rankzeroevaluationdeterminanth) + (mdr_nb_zero_columns_rankzeroevaluationdeterminanth)) * S ((mdr_pc_zero_columns_rankzeroevaluationdeterminanth) + (mdr_nb_zero_columns_rankzeroevaluationdeterminanth)) + ((mdr_nb_zero_columns_rankzeroevaluationdeterminanth) + (mdr_nb_zero_columns_rankzeroevaluationdeterminanth))) /\ ((mdr_c_zero_columns_rankzeroevaluationdeterminanthrc = ((mdr_a_zero_columns_rankzeroevaluationdeterminanthrc) + (mdr_b_zero_columns_rankzeroevaluationdeterminanthrc)) * S ((mdr_a_zero_columns_rankzeroevaluationdeterminanthrc) + (mdr_b_zero_columns_rankzeroevaluationdeterminanthrc)) + ((mdr_b_zero_columns_rankzeroevaluationdeterminanthrc) + (mdr_b_zero_columns_rankzeroevaluationdeterminanthrc))) /\ ((mdr_e_zero_columns_rankzeroevaluationdeterminanthrc = ((mdr_p_zero_columns_rankzeroevaluationdeterminanth) + (mdr_n_zero_columns_rankzeroevaluationdeterminanth)) * S ((mdr_p_zero_columns_rankzeroevaluationdeterminanth) + (mdr_n_zero_columns_rankzeroevaluationdeterminanth)) + ((mdr_n_zero_columns_rankzeroevaluationdeterminanth) + (mdr_n_zero_columns_rankzeroevaluationdeterminanth))) /\ ((mdr_f_zero_columns_rankzeroevaluationdeterminanthrc = ((mdr_nc_zero_columns_rankzeroevaluationdeterminanth) + (mdr_e_zero_columns_rankzeroevaluationdeterminanthrc)) * S ((mdr_nc_zero_columns_rankzeroevaluationdeterminanth) + (mdr_e_zero_columns_rankzeroevaluationdeterminanthrc)) + ((mdr_e_zero_columns_rankzeroevaluationdeterminanthrc) + (mdr_e_zero_columns_rankzeroevaluationdeterminanthrc))) /\ ((mdr_z_zero_columns_rankzeroevaluationdeterminanthr) = ((mdr_c_zero_columns_rankzeroevaluationdeterminanthrc) + (mdr_f_zero_columns_rankzeroevaluationdeterminanthrc)) * S ((mdr_c_zero_columns_rankzeroevaluationdeterminanthrc) + (mdr_f_zero_columns_rankzeroevaluationdeterminanthrc)) + ((mdr_f_zero_columns_rankzeroevaluationdeterminanthrc) + (mdr_f_zero_columns_rankzeroevaluationdeterminanthrc))))))))) /\ (((exists ff_h_mdr_zero_columns_rankzeroevaluationdeterminanthrb. ff_h_mdr_zero_columns_rankzeroevaluationdeterminanthrb + S (mdr_z_zero_columns_rankzeroevaluationdeterminanthr) = S ((S (mdr_i_zero_columns_rankzeroevaluationdeterminanth)) * mdr_c_zero_columns_rankzeroevaluationdeterminant)) /\ exists ff_q_mdr_zero_columns_rankzeroevaluationdeterminanthrb. mdr_b_zero_columns_rankzeroevaluationdeterminant = ff_q_mdr_zero_columns_rankzeroevaluationdeterminanthrb * S ((S (mdr_i_zero_columns_rankzeroevaluationdeterminanth)) * mdr_c_zero_columns_rankzeroevaluationdeterminant) + (mdr_z_zero_columns_rankzeroevaluationdeterminanthr))))) /\ (((((mdr_d_zero_columns_rankzeroevaluationdeterminanth) = 0) /\ (((mdr_p_zero_columns_rankzeroevaluationdeterminanth) = 1) /\ ((mdr_n_zero_columns_rankzeroevaluationdeterminanth) = 0))) \/ exists mdr_q_zero_columns_rankzeroevaluationdeterminanths mdr_eb_zero_columns_rankzeroevaluationdeterminanths mdr_ec_zero_columns_rankzeroevaluationdeterminanths mdr_fb_zero_columns_rankzeroevaluationdeterminanths mdr_fc_zero_columns_rankzeroevaluationdeterminanths. (((mdr_d_zero_columns_rankzeroevaluationdeterminanth) = S (mdr_q_zero_columns_rankzeroevaluationdeterminanths)) /\ ((forall mdr_j_zero_columns_rankzeroevaluationdeterminanthsc. (exists mdr_gap_zero_columns_rankzeroevaluationdeterminanthscj. mdr_gap_zero_columns_rankzeroevaluationdeterminanthscj + S (mdr_j_zero_columns_rankzeroevaluationdeterminanthsc) = (S (mdr_q_zero_columns_rankzeroevaluationdeterminanths))) -> exists mdr_i_zero_columns_rankzeroevaluationdeterminanthsc mdr_up_zero_columns_rankzeroevaluationdeterminanthsc mdr_us_zero_columns_rankzeroevaluationdeterminanthsc mdr_un_zero_columns_rankzeroevaluationdeterminanthsc mdr_ut_zero_columns_rankzeroevaluationdeterminanthsc mdr_p_zero_columns_rankzeroevaluationdeterminanthsc mdr_n_zero_columns_rankzeroevaluationdeterminanthsc. ((exists mdr_gap_zero_columns_rankzeroevaluationdeterminanthsci. mdr_gap_zero_columns_rankzeroevaluationdeterminanthsci + S (mdr_i_zero_columns_rankzeroevaluationdeterminanthsc) = (mdr_i_zero_columns_rankzeroevaluationdeterminanth)) /\ ((exists mdr_z_zero_columns_rankzeroevaluationdeterminanthscr. ((exists mdr_a_zero_columns_rankzeroevaluationdeterminanthscrc mdr_b_zero_columns_rankzeroevaluationdeterminanthscrc mdr_c_zero_columns_rankzeroevaluationdeterminanthscrc mdr_e_zero_columns_rankzeroevaluationdeterminanthscrc mdr_f_zero_columns_rankzeroevaluationdeterminanthscrc. ((mdr_a_zero_columns_rankzeroevaluationdeterminanthscrc = ((mdr_q_zero_columns_rankzeroevaluationdeterminanths) + (mdr_up_zero_columns_rankzeroevaluationdeterminanthsc)) * S ((mdr_q_zero_columns_rankzeroevaluationdeterminanths) + (mdr_up_zero_columns_rankzeroevaluationdeterminanthsc)) + ((mdr_up_zero_columns_rankzeroevaluationdeterminanthsc) + (mdr_up_zero_columns_rankzeroevaluationdeterminanthsc))) /\ ((mdr_b_zero_columns_rankzeroevaluationdeterminanthscrc = ((mdr_us_zero_columns_rankzeroevaluationdeterminanthsc) + (mdr_un_zero_columns_rankzeroevaluationdeterminanthsc)) * S ((mdr_us_zero_columns_rankzeroevaluationdeterminanthsc) + (mdr_un_zero_columns_rankzeroevaluationdeterminanthsc)) + ((mdr_un_zero_columns_rankzeroevaluationdeterminanthsc) + (mdr_un_zero_columns_rankzeroevaluationdeterminanthsc))) /\ ((mdr_c_zero_columns_rankzeroevaluationdeterminanthscrc = ((mdr_a_zero_columns_rankzeroevaluationdeterminanthscrc) + (mdr_b_zero_columns_rankzeroevaluationdeterminanthscrc)) * S ((mdr_a_zero_columns_rankzeroevaluationdeterminanthscrc) + (mdr_b_zero_columns_rankzeroevaluationdeterminanthscrc)) + ((mdr_b_zero_columns_rankzeroevaluationdeterminanthscrc) + (mdr_b_zero_columns_rankzeroevaluationdeterminanthscrc))) /\ ((mdr_e_zero_columns_rankzeroevaluationdeterminanthscrc = ((mdr_p_zero_columns_rankzeroevaluationdeterminanthsc) + (mdr_n_zero_columns_rankzeroevaluationdeterminanthsc)) * S ((mdr_p_zero_columns_rankzeroevaluationdeterminanthsc) + (mdr_n_zero_columns_rankzeroevaluationdeterminanthsc)) + ((mdr_n_zero_columns_rankzeroevaluationdeterminanthsc) + (mdr_n_zero_columns_rankzeroevaluationdeterminanthsc))) /\ ((mdr_f_zero_columns_rankzeroevaluationdeterminanthscrc = ((mdr_ut_zero_columns_rankzeroevaluationdeterminanthsc) + (mdr_e_zero_columns_rankzeroevaluationdeterminanthscrc)) * S ((mdr_ut_zero_columns_rankzeroevaluationdeterminanthsc) + (mdr_e_zero_columns_rankzeroevaluationdeterminanthscrc)) + ((mdr_e_zero_columns_rankzeroevaluationdeterminanthscrc) + (mdr_e_zero_columns_rankzeroevaluationdeterminanthscrc))) /\ ((mdr_z_zero_columns_rankzeroevaluationdeterminanthscr) = ((mdr_c_zero_columns_rankzeroevaluationdeterminanthscrc) + (mdr_f_zero_columns_rankzeroevaluationdeterminanthscrc)) * S ((mdr_c_zero_columns_rankzeroevaluationdeterminanthscrc) + (mdr_f_zero_columns_rankzeroevaluationdeterminanthscrc)) + ((mdr_f_zero_columns_rankzeroevaluationdeterminanthscrc) + (mdr_f_zero_columns_rankzeroevaluationdeterminanthscrc))))))))) /\ (((exists ff_h_mdr_zero_columns_rankzeroevaluationdeterminanthscrb. ff_h_mdr_zero_columns_rankzeroevaluationdeterminanthscrb + S (mdr_z_zero_columns_rankzeroevaluationdeterminanthscr) = S ((S (mdr_i_zero_columns_rankzeroevaluationdeterminanthsc)) * mdr_c_zero_columns_rankzeroevaluationdeterminant)) /\ exists ff_q_mdr_zero_columns_rankzeroevaluationdeterminanthscrb. mdr_b_zero_columns_rankzeroevaluationdeterminant = ff_q_mdr_zero_columns_rankzeroevaluationdeterminanthscrb * S ((S (mdr_i_zero_columns_rankzeroevaluationdeterminanthsc)) * mdr_c_zero_columns_rankzeroevaluationdeterminant) + (mdr_z_zero_columns_rankzeroevaluationdeterminanthscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_zero_columns_rankzeroevaluationdeterminanthscm_positive. (exists ff_gap_mdm_lt_mdr_zero_columns_rankzeroevaluationdeterminanthscm_positive_index_bound. ff_gap_mdm_lt_mdr_zero_columns_rankzeroevaluationdeterminanthscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_zero_columns_rankzeroevaluationdeterminanthscm_positive) = ((mdr_q_zero_columns_rankzeroevaluationdeterminanths) * (mdr_q_zero_columns_rankzeroevaluationdeterminanths))) -> exists ff_row_mdm_prefix_mdr_zero_columns_rankzeroevaluationdeterminanthscm_positive ff_column_mdm_prefix_mdr_zero_columns_rankzeroevaluationdeterminanthscm_positive ff_value_mdm_prefix_mdr_zero_columns_rankzeroevaluationdeterminanthscm_positive. (ff_index_mdm_prefix_mdr_zero_columns_rankzeroevaluationdeterminanthscm_positive = (mdr_q_zero_columns_rankzeroevaluationdeterminanths) * ff_row_mdm_prefix_mdr_zero_columns_rankzeroevaluationdeterminanthscm_positive + ff_column_mdm_prefix_mdr_zero_columns_rankzeroevaluationdeterminanthscm_positive /\ ((exists ff_gap_mdm_lt_mdr_zero_columns_rankzeroevaluationdeterminanthscm_positive_column_bound. ff_gap_mdm_lt_mdr_zero_columns_rankzeroevaluationdeterminanthscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_zero_columns_rankzeroevaluationdeterminanthscm_positive) = (mdr_q_zero_columns_rankzeroevaluationdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_zero_columns_rankzeroevaluationdeterminanthscm_positive_cell ff_column_mdm_cell_mdr_zero_columns_rankzeroevaluationdeterminanthscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_zero_columns_rankzeroevaluationdeterminanthscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_zero_columns_rankzeroevaluationdeterminanthscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_zero_columns_rankzeroevaluationdeterminanthscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_zero_columns_rankzeroevaluationdeterminanthscm_positive_cell = ff_row_mdm_prefix_mdr_zero_columns_rankzeroevaluationdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_zero_columns_rankzeroevaluationdeterminanthscm_positive_cell_row_after. ff_gap_mdm_le_mdr_zero_columns_rankzeroevaluationdeterminanthscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_zero_columns_rankzeroevaluationdeterminanthscm_positive)) /\ ff_row_mdm_cell_mdr_zero_columns_rankzeroevaluationdeterminanthscm_positive_cell = S ff_row_mdm_prefix_mdr_zero_columns_rankzeroevaluationdeterminanthscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_zero_columns_rankzeroevaluationdeterminanthscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_zero_columns_rankzeroevaluationdeterminanthscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_zero_columns_rankzeroevaluationdeterminanthscm_positive) = (mdr_j_zero_columns_rankzeroevaluationdeterminanthsc)) /\ ff_column_mdm_cell_mdr_zero_columns_rankzeroevaluationdeterminanthscm_positive_cell = ff_column_mdm_prefix_mdr_zero_columns_rankzeroevaluationdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_zero_columns_rankzeroevaluationdeterminanthscm_positive_cell_column_after. ff_gap_mdm_le_mdr_zero_columns_rankzeroevaluationdeterminanthscm_positive_cell_column_after + (mdr_j_zero_columns_rankzeroevaluationdeterminanthsc) = (ff_column_mdm_prefix_mdr_zero_columns_rankzeroevaluationdeterminanthscm_positive)) /\ ff_column_mdm_cell_mdr_zero_columns_rankzeroevaluationdeterminanthscm_positive_cell = S ff_column_mdm_prefix_mdr_zero_columns_rankzeroevaluationdeterminanthscm_positive))) /\ (((exists ff_h_mdm_mdr_zero_columns_rankzeroevaluationdeterminanthscm_positive_cell_source. ff_h_mdm_mdr_zero_columns_rankzeroevaluationdeterminanthscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_zero_columns_rankzeroevaluationdeterminanthscm_positive) = S ((S ((ff_row_mdm_cell_mdr_zero_columns_rankzeroevaluationdeterminanthscm_positive_cell) * (S (mdr_q_zero_columns_rankzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_zero_columns_rankzeroevaluationdeterminanthscm_positive_cell))) * mdr_pc_zero_columns_rankzeroevaluationdeterminanth)) /\ exists ff_q_mdm_mdr_zero_columns_rankzeroevaluationdeterminanthscm_positive_cell_source. mdr_pb_zero_columns_rankzeroevaluationdeterminanth = ff_q_mdm_mdr_zero_columns_rankzeroevaluationdeterminanthscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_zero_columns_rankzeroevaluationdeterminanthscm_positive_cell) * (S (mdr_q_zero_columns_rankzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_zero_columns_rankzeroevaluationdeterminanthscm_positive_cell))) * mdr_pc_zero_columns_rankzeroevaluationdeterminanth) + (ff_value_mdm_prefix_mdr_zero_columns_rankzeroevaluationdeterminanthscm_positive)))))) /\ (((exists ff_h_mdm_mdr_zero_columns_rankzeroevaluationdeterminanthscm_positive_target. ff_h_mdm_mdr_zero_columns_rankzeroevaluationdeterminanthscm_positive_target + S (ff_value_mdm_prefix_mdr_zero_columns_rankzeroevaluationdeterminanthscm_positive) = S ((S (ff_index_mdm_prefix_mdr_zero_columns_rankzeroevaluationdeterminanthscm_positive)) * mdr_us_zero_columns_rankzeroevaluationdeterminanthsc)) /\ exists ff_q_mdm_mdr_zero_columns_rankzeroevaluationdeterminanthscm_positive_target. mdr_up_zero_columns_rankzeroevaluationdeterminanthsc = ff_q_mdm_mdr_zero_columns_rankzeroevaluationdeterminanthscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_zero_columns_rankzeroevaluationdeterminanthscm_positive)) * mdr_us_zero_columns_rankzeroevaluationdeterminanthsc) + (ff_value_mdm_prefix_mdr_zero_columns_rankzeroevaluationdeterminanthscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_zero_columns_rankzeroevaluationdeterminanthscm_negative. (exists ff_gap_mdm_lt_mdr_zero_columns_rankzeroevaluationdeterminanthscm_negative_index_bound. ff_gap_mdm_lt_mdr_zero_columns_rankzeroevaluationdeterminanthscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_zero_columns_rankzeroevaluationdeterminanthscm_negative) = ((mdr_q_zero_columns_rankzeroevaluationdeterminanths) * (mdr_q_zero_columns_rankzeroevaluationdeterminanths))) -> exists ff_row_mdm_prefix_mdr_zero_columns_rankzeroevaluationdeterminanthscm_negative ff_column_mdm_prefix_mdr_zero_columns_rankzeroevaluationdeterminanthscm_negative ff_value_mdm_prefix_mdr_zero_columns_rankzeroevaluationdeterminanthscm_negative. (ff_index_mdm_prefix_mdr_zero_columns_rankzeroevaluationdeterminanthscm_negative = (mdr_q_zero_columns_rankzeroevaluationdeterminanths) * ff_row_mdm_prefix_mdr_zero_columns_rankzeroevaluationdeterminanthscm_negative + ff_column_mdm_prefix_mdr_zero_columns_rankzeroevaluationdeterminanthscm_negative /\ ((exists ff_gap_mdm_lt_mdr_zero_columns_rankzeroevaluationdeterminanthscm_negative_column_bound. ff_gap_mdm_lt_mdr_zero_columns_rankzeroevaluationdeterminanthscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_zero_columns_rankzeroevaluationdeterminanthscm_negative) = (mdr_q_zero_columns_rankzeroevaluationdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_zero_columns_rankzeroevaluationdeterminanthscm_negative_cell ff_column_mdm_cell_mdr_zero_columns_rankzeroevaluationdeterminanthscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_zero_columns_rankzeroevaluationdeterminanthscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_zero_columns_rankzeroevaluationdeterminanthscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_zero_columns_rankzeroevaluationdeterminanthscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_zero_columns_rankzeroevaluationdeterminanthscm_negative_cell = ff_row_mdm_prefix_mdr_zero_columns_rankzeroevaluationdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_zero_columns_rankzeroevaluationdeterminanthscm_negative_cell_row_after. ff_gap_mdm_le_mdr_zero_columns_rankzeroevaluationdeterminanthscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_zero_columns_rankzeroevaluationdeterminanthscm_negative)) /\ ff_row_mdm_cell_mdr_zero_columns_rankzeroevaluationdeterminanthscm_negative_cell = S ff_row_mdm_prefix_mdr_zero_columns_rankzeroevaluationdeterminanthscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_zero_columns_rankzeroevaluationdeterminanthscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_zero_columns_rankzeroevaluationdeterminanthscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_zero_columns_rankzeroevaluationdeterminanthscm_negative) = (mdr_j_zero_columns_rankzeroevaluationdeterminanthsc)) /\ ff_column_mdm_cell_mdr_zero_columns_rankzeroevaluationdeterminanthscm_negative_cell = ff_column_mdm_prefix_mdr_zero_columns_rankzeroevaluationdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_zero_columns_rankzeroevaluationdeterminanthscm_negative_cell_column_after. ff_gap_mdm_le_mdr_zero_columns_rankzeroevaluationdeterminanthscm_negative_cell_column_after + (mdr_j_zero_columns_rankzeroevaluationdeterminanthsc) = (ff_column_mdm_prefix_mdr_zero_columns_rankzeroevaluationdeterminanthscm_negative)) /\ ff_column_mdm_cell_mdr_zero_columns_rankzeroevaluationdeterminanthscm_negative_cell = S ff_column_mdm_prefix_mdr_zero_columns_rankzeroevaluationdeterminanthscm_negative))) /\ (((exists ff_h_mdm_mdr_zero_columns_rankzeroevaluationdeterminanthscm_negative_cell_source. ff_h_mdm_mdr_zero_columns_rankzeroevaluationdeterminanthscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_zero_columns_rankzeroevaluationdeterminanthscm_negative) = S ((S ((ff_row_mdm_cell_mdr_zero_columns_rankzeroevaluationdeterminanthscm_negative_cell) * (S (mdr_q_zero_columns_rankzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_zero_columns_rankzeroevaluationdeterminanthscm_negative_cell))) * mdr_nc_zero_columns_rankzeroevaluationdeterminanth)) /\ exists ff_q_mdm_mdr_zero_columns_rankzeroevaluationdeterminanthscm_negative_cell_source. mdr_nb_zero_columns_rankzeroevaluationdeterminanth = ff_q_mdm_mdr_zero_columns_rankzeroevaluationdeterminanthscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_zero_columns_rankzeroevaluationdeterminanthscm_negative_cell) * (S (mdr_q_zero_columns_rankzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_zero_columns_rankzeroevaluationdeterminanthscm_negative_cell))) * mdr_nc_zero_columns_rankzeroevaluationdeterminanth) + (ff_value_mdm_prefix_mdr_zero_columns_rankzeroevaluationdeterminanthscm_negative)))))) /\ (((exists ff_h_mdm_mdr_zero_columns_rankzeroevaluationdeterminanthscm_negative_target. ff_h_mdm_mdr_zero_columns_rankzeroevaluationdeterminanthscm_negative_target + S (ff_value_mdm_prefix_mdr_zero_columns_rankzeroevaluationdeterminanthscm_negative) = S ((S (ff_index_mdm_prefix_mdr_zero_columns_rankzeroevaluationdeterminanthscm_negative)) * mdr_ut_zero_columns_rankzeroevaluationdeterminanthsc)) /\ exists ff_q_mdm_mdr_zero_columns_rankzeroevaluationdeterminanthscm_negative_target. mdr_un_zero_columns_rankzeroevaluationdeterminanthsc = ff_q_mdm_mdr_zero_columns_rankzeroevaluationdeterminanthscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_zero_columns_rankzeroevaluationdeterminanthscm_negative)) * mdr_ut_zero_columns_rankzeroevaluationdeterminanthsc) + (ff_value_mdm_prefix_mdr_zero_columns_rankzeroevaluationdeterminanthscm_negative))))))))) /\ ((((exists ff_h_mdr_zero_columns_rankzeroevaluationdeterminanthscp. ff_h_mdr_zero_columns_rankzeroevaluationdeterminanthscp + S (mdr_p_zero_columns_rankzeroevaluationdeterminanthsc) = S ((S (mdr_j_zero_columns_rankzeroevaluationdeterminanthsc)) * mdr_ec_zero_columns_rankzeroevaluationdeterminanths)) /\ exists ff_q_mdr_zero_columns_rankzeroevaluationdeterminanthscp. mdr_eb_zero_columns_rankzeroevaluationdeterminanths = ff_q_mdr_zero_columns_rankzeroevaluationdeterminanthscp * S ((S (mdr_j_zero_columns_rankzeroevaluationdeterminanthsc)) * mdr_ec_zero_columns_rankzeroevaluationdeterminanths) + (mdr_p_zero_columns_rankzeroevaluationdeterminanthsc))) /\ (((exists ff_h_mdr_zero_columns_rankzeroevaluationdeterminanthscn. ff_h_mdr_zero_columns_rankzeroevaluationdeterminanthscn + S (mdr_n_zero_columns_rankzeroevaluationdeterminanthsc) = S ((S (mdr_j_zero_columns_rankzeroevaluationdeterminanthsc)) * mdr_fc_zero_columns_rankzeroevaluationdeterminanths)) /\ exists ff_q_mdr_zero_columns_rankzeroevaluationdeterminanthscn. mdr_fb_zero_columns_rankzeroevaluationdeterminanths = ff_q_mdr_zero_columns_rankzeroevaluationdeterminanthscn * S ((S (mdr_j_zero_columns_rankzeroevaluationdeterminanthsc)) * mdr_fc_zero_columns_rankzeroevaluationdeterminanths) + (mdr_n_zero_columns_rankzeroevaluationdeterminanthsc)))))))) /\ (exists ff_ub_mce_fold_mdr_zero_columns_rankzeroevaluationdeterminanthsf ff_uc_mce_fold_mdr_zero_columns_rankzeroevaluationdeterminanthsf ff_vb_mce_fold_mdr_zero_columns_rankzeroevaluationdeterminanthsf ff_vc_mce_fold_mdr_zero_columns_rankzeroevaluationdeterminanthsf. ((forall ff_index_mce_alternating_mdr_zero_columns_rankzeroevaluationdeterminanthsf_prefix. (exists ff_gap_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_prefix_index. ff_gap_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_prefix_index + S (ff_index_mce_alternating_mdr_zero_columns_rankzeroevaluationdeterminanthsf_prefix) = (S (mdr_q_zero_columns_rankzeroevaluationdeterminanths))) -> exists ff_ap_mce_alternating_mdr_zero_columns_rankzeroevaluationdeterminanthsf_prefix ff_an_mce_alternating_mdr_zero_columns_rankzeroevaluationdeterminanthsf_prefix ff_bp_mce_alternating_mdr_zero_columns_rankzeroevaluationdeterminanthsf_prefix ff_bn_mce_alternating_mdr_zero_columns_rankzeroevaluationdeterminanthsf_prefix ff_p_mce_alternating_mdr_zero_columns_rankzeroevaluationdeterminanthsf_prefix ff_n_mce_alternating_mdr_zero_columns_rankzeroevaluationdeterminanthsf_prefix. ((((exists ff_h_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_prefix_ap. ff_h_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_prefix_ap + S (ff_ap_mce_alternating_mdr_zero_columns_rankzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_zero_columns_rankzeroevaluationdeterminanthsf_prefix)) * mdr_pc_zero_columns_rankzeroevaluationdeterminanth)) /\ exists ff_q_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_prefix_ap. mdr_pb_zero_columns_rankzeroevaluationdeterminanth = ff_q_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_zero_columns_rankzeroevaluationdeterminanthsf_prefix)) * mdr_pc_zero_columns_rankzeroevaluationdeterminanth) + (ff_ap_mce_alternating_mdr_zero_columns_rankzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_prefix_an. ff_h_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_prefix_an + S (ff_an_mce_alternating_mdr_zero_columns_rankzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_zero_columns_rankzeroevaluationdeterminanthsf_prefix)) * mdr_nc_zero_columns_rankzeroevaluationdeterminanth)) /\ exists ff_q_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_prefix_an. mdr_nb_zero_columns_rankzeroevaluationdeterminanth = ff_q_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_zero_columns_rankzeroevaluationdeterminanthsf_prefix)) * mdr_nc_zero_columns_rankzeroevaluationdeterminanth) + (ff_an_mce_alternating_mdr_zero_columns_rankzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_prefix_bp. ff_h_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_prefix_bp + S (ff_bp_mce_alternating_mdr_zero_columns_rankzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_zero_columns_rankzeroevaluationdeterminanthsf_prefix)) * mdr_ec_zero_columns_rankzeroevaluationdeterminanths)) /\ exists ff_q_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_prefix_bp. mdr_eb_zero_columns_rankzeroevaluationdeterminanths = ff_q_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_zero_columns_rankzeroevaluationdeterminanthsf_prefix)) * mdr_ec_zero_columns_rankzeroevaluationdeterminanths) + (ff_bp_mce_alternating_mdr_zero_columns_rankzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_prefix_bn. ff_h_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_prefix_bn + S (ff_bn_mce_alternating_mdr_zero_columns_rankzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_zero_columns_rankzeroevaluationdeterminanthsf_prefix)) * mdr_fc_zero_columns_rankzeroevaluationdeterminanths)) /\ exists ff_q_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_prefix_bn. mdr_fb_zero_columns_rankzeroevaluationdeterminanths = ff_q_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_zero_columns_rankzeroevaluationdeterminanthsf_prefix)) * mdr_fc_zero_columns_rankzeroevaluationdeterminanths) + (ff_bn_mce_alternating_mdr_zero_columns_rankzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_prefix_positive. ff_h_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_prefix_positive + S (ff_p_mce_alternating_mdr_zero_columns_rankzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_zero_columns_rankzeroevaluationdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_zero_columns_rankzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_prefix_positive. ff_ub_mce_fold_mdr_zero_columns_rankzeroevaluationdeterminanthsf = ff_q_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_zero_columns_rankzeroevaluationdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_zero_columns_rankzeroevaluationdeterminanthsf) + (ff_p_mce_alternating_mdr_zero_columns_rankzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_prefix_negative. ff_h_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_prefix_negative + S (ff_n_mce_alternating_mdr_zero_columns_rankzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_zero_columns_rankzeroevaluationdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_zero_columns_rankzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_prefix_negative. ff_vb_mce_fold_mdr_zero_columns_rankzeroevaluationdeterminanthsf = ff_q_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_zero_columns_rankzeroevaluationdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_zero_columns_rankzeroevaluationdeterminanthsf) + (ff_n_mce_alternating_mdr_zero_columns_rankzeroevaluationdeterminanthsf_prefix))) /\ (((exists ff_even_mce_term_mdr_zero_columns_rankzeroevaluationdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_zero_columns_rankzeroevaluationdeterminanthsf_prefix = 2 * ff_even_mce_term_mdr_zero_columns_rankzeroevaluationdeterminanthsf_prefix_term) /\ (ff_p_mce_alternating_mdr_zero_columns_rankzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_zero_columns_rankzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_zero_columns_rankzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_zero_columns_rankzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_zero_columns_rankzeroevaluationdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_zero_columns_rankzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_zero_columns_rankzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_zero_columns_rankzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_zero_columns_rankzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_zero_columns_rankzeroevaluationdeterminanthsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_zero_columns_rankzeroevaluationdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_zero_columns_rankzeroevaluationdeterminanthsf_prefix = 2 * ff_odd_mce_term_mdr_zero_columns_rankzeroevaluationdeterminanthsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_zero_columns_rankzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_zero_columns_rankzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_zero_columns_rankzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_zero_columns_rankzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_zero_columns_rankzeroevaluationdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_zero_columns_rankzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_zero_columns_rankzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_zero_columns_rankzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_zero_columns_rankzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_zero_columns_rankzeroevaluationdeterminanthsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_positive ff_v_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_positive. ((((exists ff_h_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_positive_start. ff_h_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_positive_start. ff_u_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_positive_start * S ((S (0)) * ff_v_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_positive_terminal. ff_h_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_positive_terminal + S (mdr_p_zero_columns_rankzeroevaluationdeterminanth) = S ((S ((S (mdr_q_zero_columns_rankzeroevaluationdeterminanths)))) * ff_v_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_positive_terminal. ff_u_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_positive_terminal * S ((S ((S (mdr_q_zero_columns_rankzeroevaluationdeterminanths)))) * ff_v_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_positive) + (mdr_p_zero_columns_rankzeroevaluationdeterminanth))) /\ forall ff_i_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_positive. (exists ff_lt_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_positive_bound. ff_lt_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_positive_bound + S ff_i_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_positive = (S (mdr_q_zero_columns_rankzeroevaluationdeterminanths))) -> exists ff_a_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_positive ff_r_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_positive ff_s_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_positive. ((((exists ff_h_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_positive_summand. ff_h_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_positive_summand + S (ff_a_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_zero_columns_rankzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_positive_summand. ff_ub_mce_fold_mdr_zero_columns_rankzeroevaluationdeterminanthsf = ff_q_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_positive_summand * S ((S (ff_i_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_zero_columns_rankzeroevaluationdeterminanthsf) + (ff_a_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_positive_partial. ff_h_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_positive_partial + S (ff_r_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_positive_partial. ff_u_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_positive_partial * S ((S (ff_i_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_positive) + (ff_r_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_positive_successor. ff_h_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_positive_successor + S (ff_s_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_positive) = S ((S (S ff_i_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_positive_successor. ff_u_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_positive_successor * S ((S (S ff_i_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_positive) + (ff_s_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_positive))) /\ ff_s_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_positive = ff_r_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_positive + ff_a_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_positive)))))) /\ (exists ff_u_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_negative ff_v_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_negative. ((((exists ff_h_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_negative_start. ff_h_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_negative_start. ff_u_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_negative_start * S ((S (0)) * ff_v_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_negative_terminal. ff_h_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_negative_terminal + S (mdr_n_zero_columns_rankzeroevaluationdeterminanth) = S ((S ((S (mdr_q_zero_columns_rankzeroevaluationdeterminanths)))) * ff_v_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_negative_terminal. ff_u_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_negative_terminal * S ((S ((S (mdr_q_zero_columns_rankzeroevaluationdeterminanths)))) * ff_v_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_negative) + (mdr_n_zero_columns_rankzeroevaluationdeterminanth))) /\ forall ff_i_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_negative. (exists ff_lt_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_negative_bound. ff_lt_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_negative_bound + S ff_i_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_negative = (S (mdr_q_zero_columns_rankzeroevaluationdeterminanths))) -> exists ff_a_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_negative ff_r_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_negative ff_s_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_negative. ((((exists ff_h_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_negative_summand. ff_h_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_negative_summand + S (ff_a_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_zero_columns_rankzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_negative_summand. ff_vb_mce_fold_mdr_zero_columns_rankzeroevaluationdeterminanthsf = ff_q_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_negative_summand * S ((S (ff_i_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_zero_columns_rankzeroevaluationdeterminanthsf) + (ff_a_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_negative_partial. ff_h_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_negative_partial + S (ff_r_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_negative_partial. ff_u_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_negative_partial * S ((S (ff_i_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_negative) + (ff_r_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_negative_successor. ff_h_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_negative_successor + S (ff_s_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_negative) = S ((S (S ff_i_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_negative_successor. ff_u_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_negative_successor * S ((S (S ff_i_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_negative) + (ff_s_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_negative))) /\ ff_s_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_negative = ff_r_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_negative + ff_a_mce_mdr_zero_columns_rankzeroevaluationdeterminanthsf_negative))))))))))))))) /\ ((exists mdr_gap_zero_columns_rankzeroevaluationdeterminanti. mdr_gap_zero_columns_rankzeroevaluationdeterminanti + S (mdr_i_zero_columns_rankzeroevaluationdeterminant) = (mdr_l_zero_columns_rankzeroevaluationdeterminant)) /\ (exists mdr_z_zero_columns_rankzeroevaluationdeterminantr. ((exists mdr_a_zero_columns_rankzeroevaluationdeterminantrc mdr_b_zero_columns_rankzeroevaluationdeterminantrc mdr_c_zero_columns_rankzeroevaluationdeterminantrc mdr_e_zero_columns_rankzeroevaluationdeterminantrc mdr_f_zero_columns_rankzeroevaluationdeterminantrc. ((mdr_a_zero_columns_rankzeroevaluationdeterminantrc = ((mdr_q_zero_columns_rank) + (mdr_ub_zero_columns_rankzeroevaluation)) * S ((mdr_q_zero_columns_rank) + (mdr_ub_zero_columns_rankzeroevaluation)) + ((mdr_ub_zero_columns_rankzeroevaluation) + (mdr_ub_zero_columns_rankzeroevaluation))) /\ ((mdr_b_zero_columns_rankzeroevaluationdeterminantrc = ((mdr_uc_zero_columns_rankzeroevaluation) + (mdr_vb_zero_columns_rankzeroevaluation)) * S ((mdr_uc_zero_columns_rankzeroevaluation) + (mdr_vb_zero_columns_rankzeroevaluation)) + ((mdr_vb_zero_columns_rankzeroevaluation) + (mdr_vb_zero_columns_rankzeroevaluation))) /\ ((mdr_c_zero_columns_rankzeroevaluationdeterminantrc = ((mdr_a_zero_columns_rankzeroevaluationdeterminantrc) + (mdr_b_zero_columns_rankzeroevaluationdeterminantrc)) * S ((mdr_a_zero_columns_rankzeroevaluationdeterminantrc) + (mdr_b_zero_columns_rankzeroevaluationdeterminantrc)) + ((mdr_b_zero_columns_rankzeroevaluationdeterminantrc) + (mdr_b_zero_columns_rankzeroevaluationdeterminantrc))) /\ ((mdr_e_zero_columns_rankzeroevaluationdeterminantrc = ((mdr_p_zero_columns_rankzero) + (mdr_n_zero_columns_rankzero)) * S ((mdr_p_zero_columns_rankzero) + (mdr_n_zero_columns_rankzero)) + ((mdr_n_zero_columns_rankzero) + (mdr_n_zero_columns_rankzero))) /\ ((mdr_f_zero_columns_rankzeroevaluationdeterminantrc = ((mdr_vc_zero_columns_rankzeroevaluation) + (mdr_e_zero_columns_rankzeroevaluationdeterminantrc)) * S ((mdr_vc_zero_columns_rankzeroevaluation) + (mdr_e_zero_columns_rankzeroevaluationdeterminantrc)) + ((mdr_e_zero_columns_rankzeroevaluationdeterminantrc) + (mdr_e_zero_columns_rankzeroevaluationdeterminantrc))) /\ ((mdr_z_zero_columns_rankzeroevaluationdeterminantr) = ((mdr_c_zero_columns_rankzeroevaluationdeterminantrc) + (mdr_f_zero_columns_rankzeroevaluationdeterminantrc)) * S ((mdr_c_zero_columns_rankzeroevaluationdeterminantrc) + (mdr_f_zero_columns_rankzeroevaluationdeterminantrc)) + ((mdr_f_zero_columns_rankzeroevaluationdeterminantrc) + (mdr_f_zero_columns_rankzeroevaluationdeterminantrc))))))))) /\ (((exists ff_h_mdr_zero_columns_rankzeroevaluationdeterminantrb. ff_h_mdr_zero_columns_rankzeroevaluationdeterminantrb + S (mdr_z_zero_columns_rankzeroevaluationdeterminantr) = S ((S (mdr_i_zero_columns_rankzeroevaluationdeterminant)) * mdr_c_zero_columns_rankzeroevaluationdeterminant)) /\ exists ff_q_mdr_zero_columns_rankzeroevaluationdeterminantrb. mdr_b_zero_columns_rankzeroevaluationdeterminant = ff_q_mdr_zero_columns_rankzeroevaluationdeterminantrb * S ((S (mdr_i_zero_columns_rankzeroevaluationdeterminant)) * mdr_c_zero_columns_rankzeroevaluationdeterminant) + (mdr_z_zero_columns_rankzeroevaluationdeterminantr)))))))))) -> mdr_p_zero_columns_rankzero = mdr_n_zero_columns_rankzero))))))