matrix_rank_nonzero_minor_recode_in_box

Exact expanded first-order arithmetic statement

forall pb pc nb nc r w q rc cc R C. (((~(R = 0)) /\ (forall mdr_b_rows_box mdr_e_rows_box. (forall fom_index_mrf_rows_boxsource. (exists fom_gap_mrf_rows_boxsource_index_bound. fom_gap_mrf_rows_boxsource_index_bound + S (fom_index_mrf_rows_boxsource) = q) -> exists fom_value_mrf_rows_boxsource. ((((exists fom_beta_height_mrf_rows_boxsource_entry. fom_beta_height_mrf_rows_boxsource_entry + S (fom_value_mrf_rows_boxsource) = S ((S (fom_index_mrf_rows_boxsource)) * mdr_e_rows_box)) /\ exists fom_beta_quotient_mrf_rows_boxsource_entry. mdr_b_rows_box = fom_beta_quotient_mrf_rows_boxsource_entry * S ((S (fom_index_mrf_rows_boxsource)) * mdr_e_rows_box) + (fom_value_mrf_rows_boxsource))) /\ (exists fom_gap_mrf_rows_boxsource_value_bound. fom_gap_mrf_rows_boxsource_value_bound + S (fom_value_mrf_rows_boxsource) = r))) -> exists mdr_z_rows_box. (((exists mdr_gap_rows_boxbound. mdr_gap_rows_boxbound + S (mdr_z_rows_box) = (R)) /\ (forall mdr_i_rows_boxprefix mdr_a_rows_boxprefix. (exists mdr_gap_rows_boxprefixb. mdr_gap_rows_boxprefixb + S (mdr_i_rows_boxprefix) = (q)) -> (((exists ff_h_mdr_rows_boxprefixo. ff_h_mdr_rows_boxprefixo + S (mdr_a_rows_boxprefix) = S ((S (mdr_i_rows_boxprefix)) * mdr_e_rows_box)) /\ exists ff_q_mdr_rows_boxprefixo. mdr_b_rows_box = ff_q_mdr_rows_boxprefixo * S ((S (mdr_i_rows_boxprefix)) * mdr_e_rows_box) + (mdr_a_rows_boxprefix))) -> (((exists ff_h_mdr_rows_boxprefixn. ff_h_mdr_rows_boxprefixn + S (mdr_a_rows_boxprefix) = S ((S (mdr_i_rows_boxprefix)) * rc)) /\ exists ff_q_mdr_rows_boxprefixn. mdr_z_rows_box = ff_q_mdr_rows_boxprefixn * S ((S (mdr_i_rows_boxprefix)) * rc) + (mdr_a_rows_boxprefix))))))))) -> (((~(C = 0)) /\ (forall mdr_b_columns_box mdr_e_columns_box. (forall fom_index_mrf_columns_boxsource. (exists fom_gap_mrf_columns_boxsource_index_bound. fom_gap_mrf_columns_boxsource_index_bound + S (fom_index_mrf_columns_boxsource) = q) -> exists fom_value_mrf_columns_boxsource. ((((exists fom_beta_height_mrf_columns_boxsource_entry. fom_beta_height_mrf_columns_boxsource_entry + S (fom_value_mrf_columns_boxsource) = S ((S (fom_index_mrf_columns_boxsource)) * mdr_e_columns_box)) /\ exists fom_beta_quotient_mrf_columns_boxsource_entry. mdr_b_columns_box = fom_beta_quotient_mrf_columns_boxsource_entry * S ((S (fom_index_mrf_columns_boxsource)) * mdr_e_columns_box) + (fom_value_mrf_columns_boxsource))) /\ (exists fom_gap_mrf_columns_boxsource_value_bound. fom_gap_mrf_columns_boxsource_value_bound + S (fom_value_mrf_columns_boxsource) = w))) -> exists mdr_z_columns_box. (((exists mdr_gap_columns_boxbound. mdr_gap_columns_boxbound + S (mdr_z_columns_box) = (C)) /\ (forall mdr_i_columns_boxprefix mdr_a_columns_boxprefix. (exists mdr_gap_columns_boxprefixb. mdr_gap_columns_boxprefixb + S (mdr_i_columns_boxprefix) = (q)) -> (((exists ff_h_mdr_columns_boxprefixo. ff_h_mdr_columns_boxprefixo + S (mdr_a_columns_boxprefix) = S ((S (mdr_i_columns_boxprefix)) * mdr_e_columns_box)) /\ exists ff_q_mdr_columns_boxprefixo. mdr_b_columns_box = ff_q_mdr_columns_boxprefixo * S ((S (mdr_i_columns_boxprefix)) * mdr_e_columns_box) + (mdr_a_columns_boxprefix))) -> (((exists ff_h_mdr_columns_boxprefixn. ff_h_mdr_columns_boxprefixn + S (mdr_a_columns_boxprefix) = S ((S (mdr_i_columns_boxprefix)) * cc)) /\ exists ff_q_mdr_columns_boxprefixn. mdr_z_columns_box = ff_q_mdr_columns_boxprefixn * S ((S (mdr_i_columns_boxprefix)) * cc) + (mdr_a_columns_boxprefix))))))))) -> (exists mdr_rb_unbounded_minor mdr_rc_unbounded_minor mdr_cb_unbounded_minor mdr_cc_unbounded_minor. (((((forall fom_index_mrf_unbounded_minorminorrowsbound. (exists fom_gap_mrf_unbounded_minorminorrowsbound_index_bound. fom_gap_mrf_unbounded_minorminorrowsbound_index_bound + S (fom_index_mrf_unbounded_minorminorrowsbound) = q) -> exists fom_value_mrf_unbounded_minorminorrowsbound. ((((exists fom_beta_height_mrf_unbounded_minorminorrowsbound_entry. fom_beta_height_mrf_unbounded_minorminorrowsbound_entry + S (fom_value_mrf_unbounded_minorminorrowsbound) = S ((S (fom_index_mrf_unbounded_minorminorrowsbound)) * mdr_rc_unbounded_minor)) /\ exists fom_beta_quotient_mrf_unbounded_minorminorrowsbound_entry. mdr_rb_unbounded_minor = fom_beta_quotient_mrf_unbounded_minorminorrowsbound_entry * S ((S (fom_index_mrf_unbounded_minorminorrowsbound)) * mdr_rc_unbounded_minor) + (fom_value_mrf_unbounded_minorminorrowsbound))) /\ (exists fom_gap_mrf_unbounded_minorminorrowsbound_value_bound. fom_gap_mrf_unbounded_minorminorrowsbound_value_bound + S (fom_value_mrf_unbounded_minorminorrowsbound) = r))) /\ (forall mdr_i_unbounded_minorminorrowsdistinct mdr_j_unbounded_minorminorrowsdistinct mdr_a_unbounded_minorminorrowsdistinct. (exists mdr_gap_unbounded_minorminorrowsdistincti. mdr_gap_unbounded_minorminorrowsdistincti + S (mdr_i_unbounded_minorminorrowsdistinct) = (q)) -> (exists mdr_gap_unbounded_minorminorrowsdistinctj. mdr_gap_unbounded_minorminorrowsdistinctj + S (mdr_j_unbounded_minorminorrowsdistinct) = (q)) -> (((exists ff_h_mdr_unbounded_minorminorrowsdistinctfirst. ff_h_mdr_unbounded_minorminorrowsdistinctfirst + S (mdr_a_unbounded_minorminorrowsdistinct) = S ((S (mdr_i_unbounded_minorminorrowsdistinct)) * mdr_rc_unbounded_minor)) /\ exists ff_q_mdr_unbounded_minorminorrowsdistinctfirst. mdr_rb_unbounded_minor = ff_q_mdr_unbounded_minorminorrowsdistinctfirst * S ((S (mdr_i_unbounded_minorminorrowsdistinct)) * mdr_rc_unbounded_minor) + (mdr_a_unbounded_minorminorrowsdistinct))) -> (((exists ff_h_mdr_unbounded_minorminorrowsdistinctsecond. ff_h_mdr_unbounded_minorminorrowsdistinctsecond + S (mdr_a_unbounded_minorminorrowsdistinct) = S ((S (mdr_j_unbounded_minorminorrowsdistinct)) * mdr_rc_unbounded_minor)) /\ exists ff_q_mdr_unbounded_minorminorrowsdistinctsecond. mdr_rb_unbounded_minor = ff_q_mdr_unbounded_minorminorrowsdistinctsecond * S ((S (mdr_j_unbounded_minorminorrowsdistinct)) * mdr_rc_unbounded_minor) + (mdr_a_unbounded_minorminorrowsdistinct))) -> mdr_i_unbounded_minorminorrowsdistinct = mdr_j_unbounded_minorminorrowsdistinct))) /\ ((((forall fom_index_mrf_unbounded_minorminorcolumnsbound. (exists fom_gap_mrf_unbounded_minorminorcolumnsbound_index_bound. fom_gap_mrf_unbounded_minorminorcolumnsbound_index_bound + S (fom_index_mrf_unbounded_minorminorcolumnsbound) = q) -> exists fom_value_mrf_unbounded_minorminorcolumnsbound. ((((exists fom_beta_height_mrf_unbounded_minorminorcolumnsbound_entry. fom_beta_height_mrf_unbounded_minorminorcolumnsbound_entry + S (fom_value_mrf_unbounded_minorminorcolumnsbound) = S ((S (fom_index_mrf_unbounded_minorminorcolumnsbound)) * mdr_cc_unbounded_minor)) /\ exists fom_beta_quotient_mrf_unbounded_minorminorcolumnsbound_entry. mdr_cb_unbounded_minor = fom_beta_quotient_mrf_unbounded_minorminorcolumnsbound_entry * S ((S (fom_index_mrf_unbounded_minorminorcolumnsbound)) * mdr_cc_unbounded_minor) + (fom_value_mrf_unbounded_minorminorcolumnsbound))) /\ (exists fom_gap_mrf_unbounded_minorminorcolumnsbound_value_bound. fom_gap_mrf_unbounded_minorminorcolumnsbound_value_bound + S (fom_value_mrf_unbounded_minorminorcolumnsbound) = w))) /\ (forall mdr_i_unbounded_minorminorcolumnsdistinct mdr_j_unbounded_minorminorcolumnsdistinct mdr_a_unbounded_minorminorcolumnsdistinct. (exists mdr_gap_unbounded_minorminorcolumnsdistincti. mdr_gap_unbounded_minorminorcolumnsdistincti + S (mdr_i_unbounded_minorminorcolumnsdistinct) = (q)) -> (exists mdr_gap_unbounded_minorminorcolumnsdistinctj. mdr_gap_unbounded_minorminorcolumnsdistinctj + S (mdr_j_unbounded_minorminorcolumnsdistinct) = (q)) -> (((exists ff_h_mdr_unbounded_minorminorcolumnsdistinctfirst. ff_h_mdr_unbounded_minorminorcolumnsdistinctfirst + S (mdr_a_unbounded_minorminorcolumnsdistinct) = S ((S (mdr_i_unbounded_minorminorcolumnsdistinct)) * mdr_cc_unbounded_minor)) /\ exists ff_q_mdr_unbounded_minorminorcolumnsdistinctfirst. mdr_cb_unbounded_minor = ff_q_mdr_unbounded_minorminorcolumnsdistinctfirst * S ((S (mdr_i_unbounded_minorminorcolumnsdistinct)) * mdr_cc_unbounded_minor) + (mdr_a_unbounded_minorminorcolumnsdistinct))) -> (((exists ff_h_mdr_unbounded_minorminorcolumnsdistinctsecond. ff_h_mdr_unbounded_minorminorcolumnsdistinctsecond + S (mdr_a_unbounded_minorminorcolumnsdistinct) = S ((S (mdr_j_unbounded_minorminorcolumnsdistinct)) * mdr_cc_unbounded_minor)) /\ exists ff_q_mdr_unbounded_minorminorcolumnsdistinctsecond. mdr_cb_unbounded_minor = ff_q_mdr_unbounded_minorminorcolumnsdistinctsecond * S ((S (mdr_j_unbounded_minorminorcolumnsdistinct)) * mdr_cc_unbounded_minor) + (mdr_a_unbounded_minorminorcolumnsdistinct))) -> mdr_i_unbounded_minorminorcolumnsdistinct = mdr_j_unbounded_minorminorcolumnsdistinct))) /\ (exists mdr_p_unbounded_minorminornonzero mdr_n_unbounded_minorminornonzero. ((exists mdr_ub_unbounded_minorminornonzeroevaluation mdr_uc_unbounded_minorminornonzeroevaluation mdr_vb_unbounded_minorminornonzeroevaluation mdr_vc_unbounded_minorminornonzeroevaluation. ((((forall mdr_i_unbounded_minorminornonzeroevaluationmatrixpositive. (exists mdr_gap_unbounded_minorminornonzeroevaluationmatrixpositivebound. mdr_gap_unbounded_minorminornonzeroevaluationmatrixpositivebound + S (mdr_i_unbounded_minorminornonzeroevaluationmatrixpositive) = ((q) * (q))) -> exists mdr_a_unbounded_minorminornonzeroevaluationmatrixpositive. (((exists mdr_r_unbounded_minorminornonzeroevaluationmatrixpositivepoint mdr_s_unbounded_minorminornonzeroevaluationmatrixpositivepoint mdr_u_unbounded_minorminornonzeroevaluationmatrixpositivepoint mdr_v_unbounded_minorminornonzeroevaluationmatrixpositivepoint. ((mdr_i_unbounded_minorminornonzeroevaluationmatrixpositive = (q) * mdr_r_unbounded_minorminornonzeroevaluationmatrixpositivepoint + mdr_s_unbounded_minorminornonzeroevaluationmatrixpositivepoint) /\ ((exists mdr_gap_unbounded_minorminornonzeroevaluationmatrixpositivepointcolumn. mdr_gap_unbounded_minorminornonzeroevaluationmatrixpositivepointcolumn + S (mdr_s_unbounded_minorminornonzeroevaluationmatrixpositivepoint) = (q)) /\ ((((exists ff_h_mdr_unbounded_minorminornonzeroevaluationmatrixpositivepointrow_index. ff_h_mdr_unbounded_minorminornonzeroevaluationmatrixpositivepointrow_index + S (mdr_u_unbounded_minorminornonzeroevaluationmatrixpositivepoint) = S ((S (mdr_r_unbounded_minorminornonzeroevaluationmatrixpositivepoint)) * mdr_rc_unbounded_minor)) /\ exists ff_q_mdr_unbounded_minorminornonzeroevaluationmatrixpositivepointrow_index. mdr_rb_unbounded_minor = ff_q_mdr_unbounded_minorminornonzeroevaluationmatrixpositivepointrow_index * S ((S (mdr_r_unbounded_minorminornonzeroevaluationmatrixpositivepoint)) * mdr_rc_unbounded_minor) + (mdr_u_unbounded_minorminornonzeroevaluationmatrixpositivepoint))) /\ ((((exists ff_h_mdr_unbounded_minorminornonzeroevaluationmatrixpositivepointcolumn_index. ff_h_mdr_unbounded_minorminornonzeroevaluationmatrixpositivepointcolumn_index + S (mdr_v_unbounded_minorminornonzeroevaluationmatrixpositivepoint) = S ((S (mdr_s_unbounded_minorminornonzeroevaluationmatrixpositivepoint)) * mdr_cc_unbounded_minor)) /\ exists ff_q_mdr_unbounded_minorminornonzeroevaluationmatrixpositivepointcolumn_index. mdr_cb_unbounded_minor = ff_q_mdr_unbounded_minorminornonzeroevaluationmatrixpositivepointcolumn_index * S ((S (mdr_s_unbounded_minorminornonzeroevaluationmatrixpositivepoint)) * mdr_cc_unbounded_minor) + (mdr_v_unbounded_minorminornonzeroevaluationmatrixpositivepoint))) /\ (((exists ff_h_mdr_unbounded_minorminornonzeroevaluationmatrixpositivepointsource. ff_h_mdr_unbounded_minorminornonzeroevaluationmatrixpositivepointsource + S (mdr_a_unbounded_minorminornonzeroevaluationmatrixpositive) = S ((S ((mdr_u_unbounded_minorminornonzeroevaluationmatrixpositivepoint) * (w) + (mdr_v_unbounded_minorminornonzeroevaluationmatrixpositivepoint))) * pc)) /\ exists ff_q_mdr_unbounded_minorminornonzeroevaluationmatrixpositivepointsource. pb = ff_q_mdr_unbounded_minorminornonzeroevaluationmatrixpositivepointsource * S ((S ((mdr_u_unbounded_minorminornonzeroevaluationmatrixpositivepoint) * (w) + (mdr_v_unbounded_minorminornonzeroevaluationmatrixpositivepoint))) * pc) + (mdr_a_unbounded_minorminornonzeroevaluationmatrixpositive)))))))) /\ (((exists ff_h_mdr_unbounded_minorminornonzeroevaluationmatrixpositiveoutput. ff_h_mdr_unbounded_minorminornonzeroevaluationmatrixpositiveoutput + S (mdr_a_unbounded_minorminornonzeroevaluationmatrixpositive) = S ((S (mdr_i_unbounded_minorminornonzeroevaluationmatrixpositive)) * mdr_uc_unbounded_minorminornonzeroevaluation)) /\ exists ff_q_mdr_unbounded_minorminornonzeroevaluationmatrixpositiveoutput. mdr_ub_unbounded_minorminornonzeroevaluation = ff_q_mdr_unbounded_minorminornonzeroevaluationmatrixpositiveoutput * S ((S (mdr_i_unbounded_minorminornonzeroevaluationmatrixpositive)) * mdr_uc_unbounded_minorminornonzeroevaluation) + (mdr_a_unbounded_minorminornonzeroevaluationmatrixpositive)))))) /\ (forall mdr_i_unbounded_minorminornonzeroevaluationmatrixnegative. (exists mdr_gap_unbounded_minorminornonzeroevaluationmatrixnegativebound. mdr_gap_unbounded_minorminornonzeroevaluationmatrixnegativebound + S (mdr_i_unbounded_minorminornonzeroevaluationmatrixnegative) = ((q) * (q))) -> exists mdr_a_unbounded_minorminornonzeroevaluationmatrixnegative. (((exists mdr_r_unbounded_minorminornonzeroevaluationmatrixnegativepoint mdr_s_unbounded_minorminornonzeroevaluationmatrixnegativepoint mdr_u_unbounded_minorminornonzeroevaluationmatrixnegativepoint mdr_v_unbounded_minorminornonzeroevaluationmatrixnegativepoint. ((mdr_i_unbounded_minorminornonzeroevaluationmatrixnegative = (q) * mdr_r_unbounded_minorminornonzeroevaluationmatrixnegativepoint + mdr_s_unbounded_minorminornonzeroevaluationmatrixnegativepoint) /\ ((exists mdr_gap_unbounded_minorminornonzeroevaluationmatrixnegativepointcolumn. mdr_gap_unbounded_minorminornonzeroevaluationmatrixnegativepointcolumn + S (mdr_s_unbounded_minorminornonzeroevaluationmatrixnegativepoint) = (q)) /\ ((((exists ff_h_mdr_unbounded_minorminornonzeroevaluationmatrixnegativepointrow_index. ff_h_mdr_unbounded_minorminornonzeroevaluationmatrixnegativepointrow_index + S (mdr_u_unbounded_minorminornonzeroevaluationmatrixnegativepoint) = S ((S (mdr_r_unbounded_minorminornonzeroevaluationmatrixnegativepoint)) * mdr_rc_unbounded_minor)) /\ exists ff_q_mdr_unbounded_minorminornonzeroevaluationmatrixnegativepointrow_index. mdr_rb_unbounded_minor = ff_q_mdr_unbounded_minorminornonzeroevaluationmatrixnegativepointrow_index * S ((S (mdr_r_unbounded_minorminornonzeroevaluationmatrixnegativepoint)) * mdr_rc_unbounded_minor) + (mdr_u_unbounded_minorminornonzeroevaluationmatrixnegativepoint))) /\ ((((exists ff_h_mdr_unbounded_minorminornonzeroevaluationmatrixnegativepointcolumn_index. ff_h_mdr_unbounded_minorminornonzeroevaluationmatrixnegativepointcolumn_index + S (mdr_v_unbounded_minorminornonzeroevaluationmatrixnegativepoint) = S ((S (mdr_s_unbounded_minorminornonzeroevaluationmatrixnegativepoint)) * mdr_cc_unbounded_minor)) /\ exists ff_q_mdr_unbounded_minorminornonzeroevaluationmatrixnegativepointcolumn_index. mdr_cb_unbounded_minor = ff_q_mdr_unbounded_minorminornonzeroevaluationmatrixnegativepointcolumn_index * S ((S (mdr_s_unbounded_minorminornonzeroevaluationmatrixnegativepoint)) * mdr_cc_unbounded_minor) + (mdr_v_unbounded_minorminornonzeroevaluationmatrixnegativepoint))) /\ (((exists ff_h_mdr_unbounded_minorminornonzeroevaluationmatrixnegativepointsource. ff_h_mdr_unbounded_minorminornonzeroevaluationmatrixnegativepointsource + S (mdr_a_unbounded_minorminornonzeroevaluationmatrixnegative) = S ((S ((mdr_u_unbounded_minorminornonzeroevaluationmatrixnegativepoint) * (w) + (mdr_v_unbounded_minorminornonzeroevaluationmatrixnegativepoint))) * nc)) /\ exists ff_q_mdr_unbounded_minorminornonzeroevaluationmatrixnegativepointsource. nb = ff_q_mdr_unbounded_minorminornonzeroevaluationmatrixnegativepointsource * S ((S ((mdr_u_unbounded_minorminornonzeroevaluationmatrixnegativepoint) * (w) + (mdr_v_unbounded_minorminornonzeroevaluationmatrixnegativepoint))) * nc) + (mdr_a_unbounded_minorminornonzeroevaluationmatrixnegative)))))))) /\ (((exists ff_h_mdr_unbounded_minorminornonzeroevaluationmatrixnegativeoutput. ff_h_mdr_unbounded_minorminornonzeroevaluationmatrixnegativeoutput + S (mdr_a_unbounded_minorminornonzeroevaluationmatrixnegative) = S ((S (mdr_i_unbounded_minorminornonzeroevaluationmatrixnegative)) * mdr_vc_unbounded_minorminornonzeroevaluation)) /\ exists ff_q_mdr_unbounded_minorminornonzeroevaluationmatrixnegativeoutput. mdr_vb_unbounded_minorminornonzeroevaluation = ff_q_mdr_unbounded_minorminornonzeroevaluationmatrixnegativeoutput * S ((S (mdr_i_unbounded_minorminornonzeroevaluationmatrixnegative)) * mdr_vc_unbounded_minorminornonzeroevaluation) + (mdr_a_unbounded_minorminornonzeroevaluationmatrixnegative)))))))) /\ (exists mdr_b_unbounded_minorminornonzeroevaluationdeterminant mdr_c_unbounded_minorminornonzeroevaluationdeterminant mdr_l_unbounded_minorminornonzeroevaluationdeterminant mdr_i_unbounded_minorminornonzeroevaluationdeterminant. ((forall mdr_i_unbounded_minorminornonzeroevaluationdeterminanth. (exists mdr_gap_unbounded_minorminornonzeroevaluationdeterminanthi. mdr_gap_unbounded_minorminornonzeroevaluationdeterminanthi + S (mdr_i_unbounded_minorminornonzeroevaluationdeterminanth) = (mdr_l_unbounded_minorminornonzeroevaluationdeterminant)) -> exists mdr_d_unbounded_minorminornonzeroevaluationdeterminanth mdr_pb_unbounded_minorminornonzeroevaluationdeterminanth mdr_pc_unbounded_minorminornonzeroevaluationdeterminanth mdr_nb_unbounded_minorminornonzeroevaluationdeterminanth mdr_nc_unbounded_minorminornonzeroevaluationdeterminanth mdr_p_unbounded_minorminornonzeroevaluationdeterminanth mdr_n_unbounded_minorminornonzeroevaluationdeterminanth. ((exists mdr_z_unbounded_minorminornonzeroevaluationdeterminanthr. ((exists mdr_a_unbounded_minorminornonzeroevaluationdeterminanthrc mdr_b_unbounded_minorminornonzeroevaluationdeterminanthrc mdr_c_unbounded_minorminornonzeroevaluationdeterminanthrc mdr_e_unbounded_minorminornonzeroevaluationdeterminanthrc mdr_f_unbounded_minorminornonzeroevaluationdeterminanthrc. ((mdr_a_unbounded_minorminornonzeroevaluationdeterminanthrc = ((mdr_d_unbounded_minorminornonzeroevaluationdeterminanth) + (mdr_pb_unbounded_minorminornonzeroevaluationdeterminanth)) * S ((mdr_d_unbounded_minorminornonzeroevaluationdeterminanth) + (mdr_pb_unbounded_minorminornonzeroevaluationdeterminanth)) + ((mdr_pb_unbounded_minorminornonzeroevaluationdeterminanth) + (mdr_pb_unbounded_minorminornonzeroevaluationdeterminanth))) /\ ((mdr_b_unbounded_minorminornonzeroevaluationdeterminanthrc = ((mdr_pc_unbounded_minorminornonzeroevaluationdeterminanth) + (mdr_nb_unbounded_minorminornonzeroevaluationdeterminanth)) * S ((mdr_pc_unbounded_minorminornonzeroevaluationdeterminanth) + (mdr_nb_unbounded_minorminornonzeroevaluationdeterminanth)) + ((mdr_nb_unbounded_minorminornonzeroevaluationdeterminanth) + (mdr_nb_unbounded_minorminornonzeroevaluationdeterminanth))) /\ ((mdr_c_unbounded_minorminornonzeroevaluationdeterminanthrc = ((mdr_a_unbounded_minorminornonzeroevaluationdeterminanthrc) + (mdr_b_unbounded_minorminornonzeroevaluationdeterminanthrc)) * S ((mdr_a_unbounded_minorminornonzeroevaluationdeterminanthrc) + (mdr_b_unbounded_minorminornonzeroevaluationdeterminanthrc)) + ((mdr_b_unbounded_minorminornonzeroevaluationdeterminanthrc) + (mdr_b_unbounded_minorminornonzeroevaluationdeterminanthrc))) /\ ((mdr_e_unbounded_minorminornonzeroevaluationdeterminanthrc = ((mdr_p_unbounded_minorminornonzeroevaluationdeterminanth) + (mdr_n_unbounded_minorminornonzeroevaluationdeterminanth)) * S ((mdr_p_unbounded_minorminornonzeroevaluationdeterminanth) + (mdr_n_unbounded_minorminornonzeroevaluationdeterminanth)) + ((mdr_n_unbounded_minorminornonzeroevaluationdeterminanth) + (mdr_n_unbounded_minorminornonzeroevaluationdeterminanth))) /\ ((mdr_f_unbounded_minorminornonzeroevaluationdeterminanthrc = ((mdr_nc_unbounded_minorminornonzeroevaluationdeterminanth) + (mdr_e_unbounded_minorminornonzeroevaluationdeterminanthrc)) * S ((mdr_nc_unbounded_minorminornonzeroevaluationdeterminanth) + (mdr_e_unbounded_minorminornonzeroevaluationdeterminanthrc)) + ((mdr_e_unbounded_minorminornonzeroevaluationdeterminanthrc) + (mdr_e_unbounded_minorminornonzeroevaluationdeterminanthrc))) /\ ((mdr_z_unbounded_minorminornonzeroevaluationdeterminanthr) = ((mdr_c_unbounded_minorminornonzeroevaluationdeterminanthrc) + (mdr_f_unbounded_minorminornonzeroevaluationdeterminanthrc)) * S ((mdr_c_unbounded_minorminornonzeroevaluationdeterminanthrc) + (mdr_f_unbounded_minorminornonzeroevaluationdeterminanthrc)) + ((mdr_f_unbounded_minorminornonzeroevaluationdeterminanthrc) + (mdr_f_unbounded_minorminornonzeroevaluationdeterminanthrc))))))))) /\ (((exists ff_h_mdr_unbounded_minorminornonzeroevaluationdeterminanthrb. ff_h_mdr_unbounded_minorminornonzeroevaluationdeterminanthrb + S (mdr_z_unbounded_minorminornonzeroevaluationdeterminanthr) = S ((S (mdr_i_unbounded_minorminornonzeroevaluationdeterminanth)) * mdr_c_unbounded_minorminornonzeroevaluationdeterminant)) /\ exists ff_q_mdr_unbounded_minorminornonzeroevaluationdeterminanthrb. mdr_b_unbounded_minorminornonzeroevaluationdeterminant = ff_q_mdr_unbounded_minorminornonzeroevaluationdeterminanthrb * S ((S (mdr_i_unbounded_minorminornonzeroevaluationdeterminanth)) * mdr_c_unbounded_minorminornonzeroevaluationdeterminant) + (mdr_z_unbounded_minorminornonzeroevaluationdeterminanthr))))) /\ (((((mdr_d_unbounded_minorminornonzeroevaluationdeterminanth) = 0) /\ (((mdr_p_unbounded_minorminornonzeroevaluationdeterminanth) = 1) /\ ((mdr_n_unbounded_minorminornonzeroevaluationdeterminanth) = 0))) \/ exists mdr_q_unbounded_minorminornonzeroevaluationdeterminanths mdr_eb_unbounded_minorminornonzeroevaluationdeterminanths mdr_ec_unbounded_minorminornonzeroevaluationdeterminanths mdr_fb_unbounded_minorminornonzeroevaluationdeterminanths mdr_fc_unbounded_minorminornonzeroevaluationdeterminanths. (((mdr_d_unbounded_minorminornonzeroevaluationdeterminanth) = S (mdr_q_unbounded_minorminornonzeroevaluationdeterminanths)) /\ ((forall mdr_j_unbounded_minorminornonzeroevaluationdeterminanthsc. (exists mdr_gap_unbounded_minorminornonzeroevaluationdeterminanthscj. mdr_gap_unbounded_minorminornonzeroevaluationdeterminanthscj + S (mdr_j_unbounded_minorminornonzeroevaluationdeterminanthsc) = (S (mdr_q_unbounded_minorminornonzeroevaluationdeterminanths))) -> exists mdr_i_unbounded_minorminornonzeroevaluationdeterminanthsc mdr_up_unbounded_minorminornonzeroevaluationdeterminanthsc mdr_us_unbounded_minorminornonzeroevaluationdeterminanthsc mdr_un_unbounded_minorminornonzeroevaluationdeterminanthsc mdr_ut_unbounded_minorminornonzeroevaluationdeterminanthsc mdr_p_unbounded_minorminornonzeroevaluationdeterminanthsc mdr_n_unbounded_minorminornonzeroevaluationdeterminanthsc. ((exists mdr_gap_unbounded_minorminornonzeroevaluationdeterminanthsci. mdr_gap_unbounded_minorminornonzeroevaluationdeterminanthsci + S (mdr_i_unbounded_minorminornonzeroevaluationdeterminanthsc) = (mdr_i_unbounded_minorminornonzeroevaluationdeterminanth)) /\ ((exists mdr_z_unbounded_minorminornonzeroevaluationdeterminanthscr. ((exists mdr_a_unbounded_minorminornonzeroevaluationdeterminanthscrc mdr_b_unbounded_minorminornonzeroevaluationdeterminanthscrc mdr_c_unbounded_minorminornonzeroevaluationdeterminanthscrc mdr_e_unbounded_minorminornonzeroevaluationdeterminanthscrc mdr_f_unbounded_minorminornonzeroevaluationdeterminanthscrc. ((mdr_a_unbounded_minorminornonzeroevaluationdeterminanthscrc = ((mdr_q_unbounded_minorminornonzeroevaluationdeterminanths) + (mdr_up_unbounded_minorminornonzeroevaluationdeterminanthsc)) * S ((mdr_q_unbounded_minorminornonzeroevaluationdeterminanths) + (mdr_up_unbounded_minorminornonzeroevaluationdeterminanthsc)) + ((mdr_up_unbounded_minorminornonzeroevaluationdeterminanthsc) + (mdr_up_unbounded_minorminornonzeroevaluationdeterminanthsc))) /\ ((mdr_b_unbounded_minorminornonzeroevaluationdeterminanthscrc = ((mdr_us_unbounded_minorminornonzeroevaluationdeterminanthsc) + (mdr_un_unbounded_minorminornonzeroevaluationdeterminanthsc)) * S ((mdr_us_unbounded_minorminornonzeroevaluationdeterminanthsc) + (mdr_un_unbounded_minorminornonzeroevaluationdeterminanthsc)) + ((mdr_un_unbounded_minorminornonzeroevaluationdeterminanthsc) + (mdr_un_unbounded_minorminornonzeroevaluationdeterminanthsc))) /\ ((mdr_c_unbounded_minorminornonzeroevaluationdeterminanthscrc = ((mdr_a_unbounded_minorminornonzeroevaluationdeterminanthscrc) + (mdr_b_unbounded_minorminornonzeroevaluationdeterminanthscrc)) * S ((mdr_a_unbounded_minorminornonzeroevaluationdeterminanthscrc) + (mdr_b_unbounded_minorminornonzeroevaluationdeterminanthscrc)) + ((mdr_b_unbounded_minorminornonzeroevaluationdeterminanthscrc) + (mdr_b_unbounded_minorminornonzeroevaluationdeterminanthscrc))) /\ ((mdr_e_unbounded_minorminornonzeroevaluationdeterminanthscrc = ((mdr_p_unbounded_minorminornonzeroevaluationdeterminanthsc) + (mdr_n_unbounded_minorminornonzeroevaluationdeterminanthsc)) * S ((mdr_p_unbounded_minorminornonzeroevaluationdeterminanthsc) + (mdr_n_unbounded_minorminornonzeroevaluationdeterminanthsc)) + ((mdr_n_unbounded_minorminornonzeroevaluationdeterminanthsc) + (mdr_n_unbounded_minorminornonzeroevaluationdeterminanthsc))) /\ ((mdr_f_unbounded_minorminornonzeroevaluationdeterminanthscrc = ((mdr_ut_unbounded_minorminornonzeroevaluationdeterminanthsc) + (mdr_e_unbounded_minorminornonzeroevaluationdeterminanthscrc)) * S ((mdr_ut_unbounded_minorminornonzeroevaluationdeterminanthsc) + (mdr_e_unbounded_minorminornonzeroevaluationdeterminanthscrc)) + ((mdr_e_unbounded_minorminornonzeroevaluationdeterminanthscrc) + (mdr_e_unbounded_minorminornonzeroevaluationdeterminanthscrc))) /\ ((mdr_z_unbounded_minorminornonzeroevaluationdeterminanthscr) = ((mdr_c_unbounded_minorminornonzeroevaluationdeterminanthscrc) + (mdr_f_unbounded_minorminornonzeroevaluationdeterminanthscrc)) * S ((mdr_c_unbounded_minorminornonzeroevaluationdeterminanthscrc) + (mdr_f_unbounded_minorminornonzeroevaluationdeterminanthscrc)) + ((mdr_f_unbounded_minorminornonzeroevaluationdeterminanthscrc) + (mdr_f_unbounded_minorminornonzeroevaluationdeterminanthscrc))))))))) /\ (((exists ff_h_mdr_unbounded_minorminornonzeroevaluationdeterminanthscrb. ff_h_mdr_unbounded_minorminornonzeroevaluationdeterminanthscrb + S (mdr_z_unbounded_minorminornonzeroevaluationdeterminanthscr) = S ((S (mdr_i_unbounded_minorminornonzeroevaluationdeterminanthsc)) * mdr_c_unbounded_minorminornonzeroevaluationdeterminant)) /\ exists ff_q_mdr_unbounded_minorminornonzeroevaluationdeterminanthscrb. mdr_b_unbounded_minorminornonzeroevaluationdeterminant = ff_q_mdr_unbounded_minorminornonzeroevaluationdeterminanthscrb * S ((S (mdr_i_unbounded_minorminornonzeroevaluationdeterminanthsc)) * mdr_c_unbounded_minorminornonzeroevaluationdeterminant) + (mdr_z_unbounded_minorminornonzeroevaluationdeterminanthscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_positive. (exists ff_gap_mdm_lt_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_positive_index_bound. ff_gap_mdm_lt_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_positive) = ((mdr_q_unbounded_minorminornonzeroevaluationdeterminanths) * (mdr_q_unbounded_minorminornonzeroevaluationdeterminanths))) -> exists ff_row_mdm_prefix_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_positive ff_column_mdm_prefix_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_positive ff_value_mdm_prefix_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_positive. (ff_index_mdm_prefix_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_positive = (mdr_q_unbounded_minorminornonzeroevaluationdeterminanths) * ff_row_mdm_prefix_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_positive + ff_column_mdm_prefix_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_positive /\ ((exists ff_gap_mdm_lt_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_positive_column_bound. ff_gap_mdm_lt_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_positive) = (mdr_q_unbounded_minorminornonzeroevaluationdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_positive_cell ff_column_mdm_cell_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_positive_cell = ff_row_mdm_prefix_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_positive_cell_row_after. ff_gap_mdm_le_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_positive)) /\ ff_row_mdm_cell_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_positive_cell = S ff_row_mdm_prefix_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_positive) = (mdr_j_unbounded_minorminornonzeroevaluationdeterminanthsc)) /\ ff_column_mdm_cell_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_positive_cell = ff_column_mdm_prefix_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_positive_cell_column_after. ff_gap_mdm_le_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_positive_cell_column_after + (mdr_j_unbounded_minorminornonzeroevaluationdeterminanthsc) = (ff_column_mdm_prefix_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_positive)) /\ ff_column_mdm_cell_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_positive_cell = S ff_column_mdm_prefix_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_positive))) /\ (((exists ff_h_mdm_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_positive_cell_source. ff_h_mdm_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_positive) = S ((S ((ff_row_mdm_cell_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_positive_cell) * (S (mdr_q_unbounded_minorminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_positive_cell))) * mdr_pc_unbounded_minorminornonzeroevaluationdeterminanth)) /\ exists ff_q_mdm_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_positive_cell_source. mdr_pb_unbounded_minorminornonzeroevaluationdeterminanth = ff_q_mdm_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_positive_cell) * (S (mdr_q_unbounded_minorminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_positive_cell))) * mdr_pc_unbounded_minorminornonzeroevaluationdeterminanth) + (ff_value_mdm_prefix_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_positive)))))) /\ (((exists ff_h_mdm_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_positive_target. ff_h_mdm_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_positive_target + S (ff_value_mdm_prefix_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_positive) = S ((S (ff_index_mdm_prefix_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_positive)) * mdr_us_unbounded_minorminornonzeroevaluationdeterminanthsc)) /\ exists ff_q_mdm_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_positive_target. mdr_up_unbounded_minorminornonzeroevaluationdeterminanthsc = ff_q_mdm_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_positive)) * mdr_us_unbounded_minorminornonzeroevaluationdeterminanthsc) + (ff_value_mdm_prefix_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_negative. (exists ff_gap_mdm_lt_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_negative_index_bound. ff_gap_mdm_lt_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_negative) = ((mdr_q_unbounded_minorminornonzeroevaluationdeterminanths) * (mdr_q_unbounded_minorminornonzeroevaluationdeterminanths))) -> exists ff_row_mdm_prefix_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_negative ff_column_mdm_prefix_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_negative ff_value_mdm_prefix_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_negative. (ff_index_mdm_prefix_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_negative = (mdr_q_unbounded_minorminornonzeroevaluationdeterminanths) * ff_row_mdm_prefix_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_negative + ff_column_mdm_prefix_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_negative /\ ((exists ff_gap_mdm_lt_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_negative_column_bound. ff_gap_mdm_lt_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_negative) = (mdr_q_unbounded_minorminornonzeroevaluationdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_negative_cell ff_column_mdm_cell_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_negative_cell = ff_row_mdm_prefix_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_negative_cell_row_after. ff_gap_mdm_le_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_negative)) /\ ff_row_mdm_cell_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_negative_cell = S ff_row_mdm_prefix_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_negative) = (mdr_j_unbounded_minorminornonzeroevaluationdeterminanthsc)) /\ ff_column_mdm_cell_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_negative_cell = ff_column_mdm_prefix_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_negative_cell_column_after. ff_gap_mdm_le_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_negative_cell_column_after + (mdr_j_unbounded_minorminornonzeroevaluationdeterminanthsc) = (ff_column_mdm_prefix_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_negative)) /\ ff_column_mdm_cell_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_negative_cell = S ff_column_mdm_prefix_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_negative))) /\ (((exists ff_h_mdm_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_negative_cell_source. ff_h_mdm_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_negative) = S ((S ((ff_row_mdm_cell_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_negative_cell) * (S (mdr_q_unbounded_minorminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_negative_cell))) * mdr_nc_unbounded_minorminornonzeroevaluationdeterminanth)) /\ exists ff_q_mdm_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_negative_cell_source. mdr_nb_unbounded_minorminornonzeroevaluationdeterminanth = ff_q_mdm_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_negative_cell) * (S (mdr_q_unbounded_minorminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_negative_cell))) * mdr_nc_unbounded_minorminornonzeroevaluationdeterminanth) + (ff_value_mdm_prefix_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_negative)))))) /\ (((exists ff_h_mdm_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_negative_target. ff_h_mdm_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_negative_target + S (ff_value_mdm_prefix_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_negative) = S ((S (ff_index_mdm_prefix_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_negative)) * mdr_ut_unbounded_minorminornonzeroevaluationdeterminanthsc)) /\ exists ff_q_mdm_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_negative_target. mdr_un_unbounded_minorminornonzeroevaluationdeterminanthsc = ff_q_mdm_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_negative)) * mdr_ut_unbounded_minorminornonzeroevaluationdeterminanthsc) + (ff_value_mdm_prefix_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_negative))))))))) /\ ((((exists ff_h_mdr_unbounded_minorminornonzeroevaluationdeterminanthscp. ff_h_mdr_unbounded_minorminornonzeroevaluationdeterminanthscp + S (mdr_p_unbounded_minorminornonzeroevaluationdeterminanthsc) = S ((S (mdr_j_unbounded_minorminornonzeroevaluationdeterminanthsc)) * mdr_ec_unbounded_minorminornonzeroevaluationdeterminanths)) /\ exists ff_q_mdr_unbounded_minorminornonzeroevaluationdeterminanthscp. mdr_eb_unbounded_minorminornonzeroevaluationdeterminanths = ff_q_mdr_unbounded_minorminornonzeroevaluationdeterminanthscp * S ((S (mdr_j_unbounded_minorminornonzeroevaluationdeterminanthsc)) * mdr_ec_unbounded_minorminornonzeroevaluationdeterminanths) + (mdr_p_unbounded_minorminornonzeroevaluationdeterminanthsc))) /\ (((exists ff_h_mdr_unbounded_minorminornonzeroevaluationdeterminanthscn. ff_h_mdr_unbounded_minorminornonzeroevaluationdeterminanthscn + S (mdr_n_unbounded_minorminornonzeroevaluationdeterminanthsc) = S ((S (mdr_j_unbounded_minorminornonzeroevaluationdeterminanthsc)) * mdr_fc_unbounded_minorminornonzeroevaluationdeterminanths)) /\ exists ff_q_mdr_unbounded_minorminornonzeroevaluationdeterminanthscn. mdr_fb_unbounded_minorminornonzeroevaluationdeterminanths = ff_q_mdr_unbounded_minorminornonzeroevaluationdeterminanthscn * S ((S (mdr_j_unbounded_minorminornonzeroevaluationdeterminanthsc)) * mdr_fc_unbounded_minorminornonzeroevaluationdeterminanths) + (mdr_n_unbounded_minorminornonzeroevaluationdeterminanthsc)))))))) /\ (exists ff_ub_mce_fold_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf ff_uc_mce_fold_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf ff_vb_mce_fold_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf ff_vc_mce_fold_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf. ((forall ff_index_mce_alternating_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix. (exists ff_gap_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix_index. ff_gap_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix_index + S (ff_index_mce_alternating_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix) = (S (mdr_q_unbounded_minorminornonzeroevaluationdeterminanths))) -> exists ff_ap_mce_alternating_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix ff_an_mce_alternating_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix ff_bp_mce_alternating_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix ff_bn_mce_alternating_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix ff_p_mce_alternating_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix ff_n_mce_alternating_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix. ((((exists ff_h_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix_ap. ff_h_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix_ap + S (ff_ap_mce_alternating_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix)) * mdr_pc_unbounded_minorminornonzeroevaluationdeterminanth)) /\ exists ff_q_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix_ap. mdr_pb_unbounded_minorminornonzeroevaluationdeterminanth = ff_q_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix)) * mdr_pc_unbounded_minorminornonzeroevaluationdeterminanth) + (ff_ap_mce_alternating_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix_an. ff_h_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix_an + S (ff_an_mce_alternating_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix)) * mdr_nc_unbounded_minorminornonzeroevaluationdeterminanth)) /\ exists ff_q_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix_an. mdr_nb_unbounded_minorminornonzeroevaluationdeterminanth = ff_q_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix)) * mdr_nc_unbounded_minorminornonzeroevaluationdeterminanth) + (ff_an_mce_alternating_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix_bp. ff_h_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix_bp + S (ff_bp_mce_alternating_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix)) * mdr_ec_unbounded_minorminornonzeroevaluationdeterminanths)) /\ exists ff_q_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix_bp. mdr_eb_unbounded_minorminornonzeroevaluationdeterminanths = ff_q_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix)) * mdr_ec_unbounded_minorminornonzeroevaluationdeterminanths) + (ff_bp_mce_alternating_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix_bn. ff_h_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix_bn + S (ff_bn_mce_alternating_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix)) * mdr_fc_unbounded_minorminornonzeroevaluationdeterminanths)) /\ exists ff_q_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix_bn. mdr_fb_unbounded_minorminornonzeroevaluationdeterminanths = ff_q_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix)) * mdr_fc_unbounded_minorminornonzeroevaluationdeterminanths) + (ff_bn_mce_alternating_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix_positive. ff_h_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix_positive + S (ff_p_mce_alternating_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix_positive. ff_ub_mce_fold_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf) + (ff_p_mce_alternating_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix_negative. ff_h_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix_negative + S (ff_n_mce_alternating_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix_negative. ff_vb_mce_fold_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf) + (ff_n_mce_alternating_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix))) /\ (((exists ff_even_mce_term_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix = 2 * ff_even_mce_term_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix_term) /\ (ff_p_mce_alternating_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix = 2 * ff_odd_mce_term_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_positive ff_v_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_positive. ((((exists ff_h_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_positive_start. ff_h_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_positive_start. ff_u_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_positive_start * S ((S (0)) * ff_v_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_positive_terminal. ff_h_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_positive_terminal + S (mdr_p_unbounded_minorminornonzeroevaluationdeterminanth) = S ((S ((S (mdr_q_unbounded_minorminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_positive_terminal. ff_u_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_positive_terminal * S ((S ((S (mdr_q_unbounded_minorminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_positive) + (mdr_p_unbounded_minorminornonzeroevaluationdeterminanth))) /\ forall ff_i_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_positive. (exists ff_lt_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_positive_bound. ff_lt_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_positive_bound + S ff_i_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_positive = (S (mdr_q_unbounded_minorminornonzeroevaluationdeterminanths))) -> exists ff_a_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_positive ff_r_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_positive ff_s_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_positive. ((((exists ff_h_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_positive_summand. ff_h_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_positive_summand + S (ff_a_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_positive_summand. ff_ub_mce_fold_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_positive_summand * S ((S (ff_i_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf) + (ff_a_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_positive_partial. ff_h_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_positive_partial + S (ff_r_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_positive_partial. ff_u_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_positive_partial * S ((S (ff_i_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_positive) + (ff_r_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_positive_successor. ff_h_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_positive_successor + S (ff_s_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_positive) = S ((S (S ff_i_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_positive_successor. ff_u_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_positive_successor * S ((S (S ff_i_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_positive) + (ff_s_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_positive))) /\ ff_s_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_positive = ff_r_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_positive + ff_a_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_positive)))))) /\ (exists ff_u_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_negative ff_v_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_negative. ((((exists ff_h_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_negative_start. ff_h_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_negative_start. ff_u_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_negative_start * S ((S (0)) * ff_v_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_negative_terminal. ff_h_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_negative_terminal + S (mdr_n_unbounded_minorminornonzeroevaluationdeterminanth) = S ((S ((S (mdr_q_unbounded_minorminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_negative_terminal. ff_u_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_negative_terminal * S ((S ((S (mdr_q_unbounded_minorminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_negative) + (mdr_n_unbounded_minorminornonzeroevaluationdeterminanth))) /\ forall ff_i_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_negative. (exists ff_lt_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_negative_bound. ff_lt_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_negative_bound + S ff_i_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_negative = (S (mdr_q_unbounded_minorminornonzeroevaluationdeterminanths))) -> exists ff_a_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_negative ff_r_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_negative ff_s_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_negative. ((((exists ff_h_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_negative_summand. ff_h_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_negative_summand + S (ff_a_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_negative_summand. ff_vb_mce_fold_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_negative_summand * S ((S (ff_i_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf) + (ff_a_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_negative_partial. ff_h_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_negative_partial + S (ff_r_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_negative_partial. ff_u_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_negative_partial * S ((S (ff_i_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_negative) + (ff_r_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_negative_successor. ff_h_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_negative_successor + S (ff_s_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_negative) = S ((S (S ff_i_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_negative_successor. ff_u_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_negative_successor * S ((S (S ff_i_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_negative) + (ff_s_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_negative))) /\ ff_s_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_negative = ff_r_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_negative + ff_a_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_negative))))))))))))))) /\ ((exists mdr_gap_unbounded_minorminornonzeroevaluationdeterminanti. mdr_gap_unbounded_minorminornonzeroevaluationdeterminanti + S (mdr_i_unbounded_minorminornonzeroevaluationdeterminant) = (mdr_l_unbounded_minorminornonzeroevaluationdeterminant)) /\ (exists mdr_z_unbounded_minorminornonzeroevaluationdeterminantr. ((exists mdr_a_unbounded_minorminornonzeroevaluationdeterminantrc mdr_b_unbounded_minorminornonzeroevaluationdeterminantrc mdr_c_unbounded_minorminornonzeroevaluationdeterminantrc mdr_e_unbounded_minorminornonzeroevaluationdeterminantrc mdr_f_unbounded_minorminornonzeroevaluationdeterminantrc. ((mdr_a_unbounded_minorminornonzeroevaluationdeterminantrc = ((q) + (mdr_ub_unbounded_minorminornonzeroevaluation)) * S ((q) + (mdr_ub_unbounded_minorminornonzeroevaluation)) + ((mdr_ub_unbounded_minorminornonzeroevaluation) + (mdr_ub_unbounded_minorminornonzeroevaluation))) /\ ((mdr_b_unbounded_minorminornonzeroevaluationdeterminantrc = ((mdr_uc_unbounded_minorminornonzeroevaluation) + (mdr_vb_unbounded_minorminornonzeroevaluation)) * S ((mdr_uc_unbounded_minorminornonzeroevaluation) + (mdr_vb_unbounded_minorminornonzeroevaluation)) + ((mdr_vb_unbounded_minorminornonzeroevaluation) + (mdr_vb_unbounded_minorminornonzeroevaluation))) /\ ((mdr_c_unbounded_minorminornonzeroevaluationdeterminantrc = ((mdr_a_unbounded_minorminornonzeroevaluationdeterminantrc) + (mdr_b_unbounded_minorminornonzeroevaluationdeterminantrc)) * S ((mdr_a_unbounded_minorminornonzeroevaluationdeterminantrc) + (mdr_b_unbounded_minorminornonzeroevaluationdeterminantrc)) + ((mdr_b_unbounded_minorminornonzeroevaluationdeterminantrc) + (mdr_b_unbounded_minorminornonzeroevaluationdeterminantrc))) /\ ((mdr_e_unbounded_minorminornonzeroevaluationdeterminantrc = ((mdr_p_unbounded_minorminornonzero) + (mdr_n_unbounded_minorminornonzero)) * S ((mdr_p_unbounded_minorminornonzero) + (mdr_n_unbounded_minorminornonzero)) + ((mdr_n_unbounded_minorminornonzero) + (mdr_n_unbounded_minorminornonzero))) /\ ((mdr_f_unbounded_minorminornonzeroevaluationdeterminantrc = ((mdr_vc_unbounded_minorminornonzeroevaluation) + (mdr_e_unbounded_minorminornonzeroevaluationdeterminantrc)) * S ((mdr_vc_unbounded_minorminornonzeroevaluation) + (mdr_e_unbounded_minorminornonzeroevaluationdeterminantrc)) + ((mdr_e_unbounded_minorminornonzeroevaluationdeterminantrc) + (mdr_e_unbounded_minorminornonzeroevaluationdeterminantrc))) /\ ((mdr_z_unbounded_minorminornonzeroevaluationdeterminantr) = ((mdr_c_unbounded_minorminornonzeroevaluationdeterminantrc) + (mdr_f_unbounded_minorminornonzeroevaluationdeterminantrc)) * S ((mdr_c_unbounded_minorminornonzeroevaluationdeterminantrc) + (mdr_f_unbounded_minorminornonzeroevaluationdeterminantrc)) + ((mdr_f_unbounded_minorminornonzeroevaluationdeterminantrc) + (mdr_f_unbounded_minorminornonzeroevaluationdeterminantrc))))))))) /\ (((exists ff_h_mdr_unbounded_minorminornonzeroevaluationdeterminantrb. ff_h_mdr_unbounded_minorminornonzeroevaluationdeterminantrb + S (mdr_z_unbounded_minorminornonzeroevaluationdeterminantr) = S ((S (mdr_i_unbounded_minorminornonzeroevaluationdeterminant)) * mdr_c_unbounded_minorminornonzeroevaluationdeterminant)) /\ exists ff_q_mdr_unbounded_minorminornonzeroevaluationdeterminantrb. mdr_b_unbounded_minorminornonzeroevaluationdeterminant = ff_q_mdr_unbounded_minorminornonzeroevaluationdeterminantrb * S ((S (mdr_i_unbounded_minorminornonzeroevaluationdeterminant)) * mdr_c_unbounded_minorminornonzeroevaluationdeterminant) + (mdr_z_unbounded_minorminornonzeroevaluationdeterminantr)))))))))) /\ (~(mdr_p_unbounded_minorminornonzero = mdr_n_unbounded_minorminornonzero)))))))) -> (exists mdr_a_bounded_minorrows. (((exists mdr_gap_bounded_minorrowsbound. mdr_gap_bounded_minorrowsbound + S (mdr_a_bounded_minorrows) = (R)) /\ (exists mdr_a_bounded_minorrowcolumns. (((exists mdr_gap_bounded_minorrowcolumnsbound. mdr_gap_bounded_minorrowcolumnsbound + S (mdr_a_bounded_minorrowcolumns) = (C)) /\ (((((forall fom_index_mrf_bounded_minorrowminorrowsbound. (exists fom_gap_mrf_bounded_minorrowminorrowsbound_index_bound. fom_gap_mrf_bounded_minorrowminorrowsbound_index_bound + S (fom_index_mrf_bounded_minorrowminorrowsbound) = q) -> exists fom_value_mrf_bounded_minorrowminorrowsbound. ((((exists fom_beta_height_mrf_bounded_minorrowminorrowsbound_entry. fom_beta_height_mrf_bounded_minorrowminorrowsbound_entry + S (fom_value_mrf_bounded_minorrowminorrowsbound) = S ((S (fom_index_mrf_bounded_minorrowminorrowsbound)) * rc)) /\ exists fom_beta_quotient_mrf_bounded_minorrowminorrowsbound_entry. mdr_a_bounded_minorrows = fom_beta_quotient_mrf_bounded_minorrowminorrowsbound_entry * S ((S (fom_index_mrf_bounded_minorrowminorrowsbound)) * rc) + (fom_value_mrf_bounded_minorrowminorrowsbound))) /\ (exists fom_gap_mrf_bounded_minorrowminorrowsbound_value_bound. fom_gap_mrf_bounded_minorrowminorrowsbound_value_bound + S (fom_value_mrf_bounded_minorrowminorrowsbound) = r))) /\ (forall mdr_i_bounded_minorrowminorrowsdistinct mdr_j_bounded_minorrowminorrowsdistinct mdr_a_bounded_minorrowminorrowsdistinct. (exists mdr_gap_bounded_minorrowminorrowsdistincti. mdr_gap_bounded_minorrowminorrowsdistincti + S (mdr_i_bounded_minorrowminorrowsdistinct) = (q)) -> (exists mdr_gap_bounded_minorrowminorrowsdistinctj. mdr_gap_bounded_minorrowminorrowsdistinctj + S (mdr_j_bounded_minorrowminorrowsdistinct) = (q)) -> (((exists ff_h_mdr_bounded_minorrowminorrowsdistinctfirst. ff_h_mdr_bounded_minorrowminorrowsdistinctfirst + S (mdr_a_bounded_minorrowminorrowsdistinct) = S ((S (mdr_i_bounded_minorrowminorrowsdistinct)) * rc)) /\ exists ff_q_mdr_bounded_minorrowminorrowsdistinctfirst. mdr_a_bounded_minorrows = ff_q_mdr_bounded_minorrowminorrowsdistinctfirst * S ((S (mdr_i_bounded_minorrowminorrowsdistinct)) * rc) + (mdr_a_bounded_minorrowminorrowsdistinct))) -> (((exists ff_h_mdr_bounded_minorrowminorrowsdistinctsecond. ff_h_mdr_bounded_minorrowminorrowsdistinctsecond + S (mdr_a_bounded_minorrowminorrowsdistinct) = S ((S (mdr_j_bounded_minorrowminorrowsdistinct)) * rc)) /\ exists ff_q_mdr_bounded_minorrowminorrowsdistinctsecond. mdr_a_bounded_minorrows = ff_q_mdr_bounded_minorrowminorrowsdistinctsecond * S ((S (mdr_j_bounded_minorrowminorrowsdistinct)) * rc) + (mdr_a_bounded_minorrowminorrowsdistinct))) -> mdr_i_bounded_minorrowminorrowsdistinct = mdr_j_bounded_minorrowminorrowsdistinct))) /\ ((((forall fom_index_mrf_bounded_minorrowminorcolumnsbound. (exists fom_gap_mrf_bounded_minorrowminorcolumnsbound_index_bound. fom_gap_mrf_bounded_minorrowminorcolumnsbound_index_bound + S (fom_index_mrf_bounded_minorrowminorcolumnsbound) = q) -> exists fom_value_mrf_bounded_minorrowminorcolumnsbound. ((((exists fom_beta_height_mrf_bounded_minorrowminorcolumnsbound_entry. fom_beta_height_mrf_bounded_minorrowminorcolumnsbound_entry + S (fom_value_mrf_bounded_minorrowminorcolumnsbound) = S ((S (fom_index_mrf_bounded_minorrowminorcolumnsbound)) * cc)) /\ exists fom_beta_quotient_mrf_bounded_minorrowminorcolumnsbound_entry. mdr_a_bounded_minorrowcolumns = fom_beta_quotient_mrf_bounded_minorrowminorcolumnsbound_entry * S ((S (fom_index_mrf_bounded_minorrowminorcolumnsbound)) * cc) + (fom_value_mrf_bounded_minorrowminorcolumnsbound))) /\ (exists fom_gap_mrf_bounded_minorrowminorcolumnsbound_value_bound. fom_gap_mrf_bounded_minorrowminorcolumnsbound_value_bound + S (fom_value_mrf_bounded_minorrowminorcolumnsbound) = w))) /\ (forall mdr_i_bounded_minorrowminorcolumnsdistinct mdr_j_bounded_minorrowminorcolumnsdistinct mdr_a_bounded_minorrowminorcolumnsdistinct. (exists mdr_gap_bounded_minorrowminorcolumnsdistincti. mdr_gap_bounded_minorrowminorcolumnsdistincti + S (mdr_i_bounded_minorrowminorcolumnsdistinct) = (q)) -> (exists mdr_gap_bounded_minorrowminorcolumnsdistinctj. mdr_gap_bounded_minorrowminorcolumnsdistinctj + S (mdr_j_bounded_minorrowminorcolumnsdistinct) = (q)) -> (((exists ff_h_mdr_bounded_minorrowminorcolumnsdistinctfirst. ff_h_mdr_bounded_minorrowminorcolumnsdistinctfirst + S (mdr_a_bounded_minorrowminorcolumnsdistinct) = S ((S (mdr_i_bounded_minorrowminorcolumnsdistinct)) * cc)) /\ exists ff_q_mdr_bounded_minorrowminorcolumnsdistinctfirst. mdr_a_bounded_minorrowcolumns = ff_q_mdr_bounded_minorrowminorcolumnsdistinctfirst * S ((S (mdr_i_bounded_minorrowminorcolumnsdistinct)) * cc) + (mdr_a_bounded_minorrowminorcolumnsdistinct))) -> (((exists ff_h_mdr_bounded_minorrowminorcolumnsdistinctsecond. ff_h_mdr_bounded_minorrowminorcolumnsdistinctsecond + S (mdr_a_bounded_minorrowminorcolumnsdistinct) = S ((S (mdr_j_bounded_minorrowminorcolumnsdistinct)) * cc)) /\ exists ff_q_mdr_bounded_minorrowminorcolumnsdistinctsecond. mdr_a_bounded_minorrowcolumns = ff_q_mdr_bounded_minorrowminorcolumnsdistinctsecond * S ((S (mdr_j_bounded_minorrowminorcolumnsdistinct)) * cc) + (mdr_a_bounded_minorrowminorcolumnsdistinct))) -> mdr_i_bounded_minorrowminorcolumnsdistinct = mdr_j_bounded_minorrowminorcolumnsdistinct))) /\ (exists mdr_p_bounded_minorrowminornonzero mdr_n_bounded_minorrowminornonzero. ((exists mdr_ub_bounded_minorrowminornonzeroevaluation mdr_uc_bounded_minorrowminornonzeroevaluation mdr_vb_bounded_minorrowminornonzeroevaluation mdr_vc_bounded_minorrowminornonzeroevaluation. ((((forall mdr_i_bounded_minorrowminornonzeroevaluationmatrixpositive. (exists mdr_gap_bounded_minorrowminornonzeroevaluationmatrixpositivebound. mdr_gap_bounded_minorrowminornonzeroevaluationmatrixpositivebound + S (mdr_i_bounded_minorrowminornonzeroevaluationmatrixpositive) = ((q) * (q))) -> exists mdr_a_bounded_minorrowminornonzeroevaluationmatrixpositive. (((exists mdr_r_bounded_minorrowminornonzeroevaluationmatrixpositivepoint mdr_s_bounded_minorrowminornonzeroevaluationmatrixpositivepoint mdr_u_bounded_minorrowminornonzeroevaluationmatrixpositivepoint mdr_v_bounded_minorrowminornonzeroevaluationmatrixpositivepoint. ((mdr_i_bounded_minorrowminornonzeroevaluationmatrixpositive = (q) * mdr_r_bounded_minorrowminornonzeroevaluationmatrixpositivepoint + mdr_s_bounded_minorrowminornonzeroevaluationmatrixpositivepoint) /\ ((exists mdr_gap_bounded_minorrowminornonzeroevaluationmatrixpositivepointcolumn. mdr_gap_bounded_minorrowminornonzeroevaluationmatrixpositivepointcolumn + S (mdr_s_bounded_minorrowminornonzeroevaluationmatrixpositivepoint) = (q)) /\ ((((exists ff_h_mdr_bounded_minorrowminornonzeroevaluationmatrixpositivepointrow_index. ff_h_mdr_bounded_minorrowminornonzeroevaluationmatrixpositivepointrow_index + S (mdr_u_bounded_minorrowminornonzeroevaluationmatrixpositivepoint) = S ((S (mdr_r_bounded_minorrowminornonzeroevaluationmatrixpositivepoint)) * rc)) /\ exists ff_q_mdr_bounded_minorrowminornonzeroevaluationmatrixpositivepointrow_index. mdr_a_bounded_minorrows = ff_q_mdr_bounded_minorrowminornonzeroevaluationmatrixpositivepointrow_index * S ((S (mdr_r_bounded_minorrowminornonzeroevaluationmatrixpositivepoint)) * rc) + (mdr_u_bounded_minorrowminornonzeroevaluationmatrixpositivepoint))) /\ ((((exists ff_h_mdr_bounded_minorrowminornonzeroevaluationmatrixpositivepointcolumn_index. ff_h_mdr_bounded_minorrowminornonzeroevaluationmatrixpositivepointcolumn_index + S (mdr_v_bounded_minorrowminornonzeroevaluationmatrixpositivepoint) = S ((S (mdr_s_bounded_minorrowminornonzeroevaluationmatrixpositivepoint)) * cc)) /\ exists ff_q_mdr_bounded_minorrowminornonzeroevaluationmatrixpositivepointcolumn_index. mdr_a_bounded_minorrowcolumns = ff_q_mdr_bounded_minorrowminornonzeroevaluationmatrixpositivepointcolumn_index * S ((S (mdr_s_bounded_minorrowminornonzeroevaluationmatrixpositivepoint)) * cc) + (mdr_v_bounded_minorrowminornonzeroevaluationmatrixpositivepoint))) /\ (((exists ff_h_mdr_bounded_minorrowminornonzeroevaluationmatrixpositivepointsource. ff_h_mdr_bounded_minorrowminornonzeroevaluationmatrixpositivepointsource + S (mdr_a_bounded_minorrowminornonzeroevaluationmatrixpositive) = S ((S ((mdr_u_bounded_minorrowminornonzeroevaluationmatrixpositivepoint) * (w) + (mdr_v_bounded_minorrowminornonzeroevaluationmatrixpositivepoint))) * pc)) /\ exists ff_q_mdr_bounded_minorrowminornonzeroevaluationmatrixpositivepointsource. pb = ff_q_mdr_bounded_minorrowminornonzeroevaluationmatrixpositivepointsource * S ((S ((mdr_u_bounded_minorrowminornonzeroevaluationmatrixpositivepoint) * (w) + (mdr_v_bounded_minorrowminornonzeroevaluationmatrixpositivepoint))) * pc) + (mdr_a_bounded_minorrowminornonzeroevaluationmatrixpositive)))))))) /\ (((exists ff_h_mdr_bounded_minorrowminornonzeroevaluationmatrixpositiveoutput. ff_h_mdr_bounded_minorrowminornonzeroevaluationmatrixpositiveoutput + S (mdr_a_bounded_minorrowminornonzeroevaluationmatrixpositive) = S ((S (mdr_i_bounded_minorrowminornonzeroevaluationmatrixpositive)) * mdr_uc_bounded_minorrowminornonzeroevaluation)) /\ exists ff_q_mdr_bounded_minorrowminornonzeroevaluationmatrixpositiveoutput. mdr_ub_bounded_minorrowminornonzeroevaluation = ff_q_mdr_bounded_minorrowminornonzeroevaluationmatrixpositiveoutput * S ((S (mdr_i_bounded_minorrowminornonzeroevaluationmatrixpositive)) * mdr_uc_bounded_minorrowminornonzeroevaluation) + (mdr_a_bounded_minorrowminornonzeroevaluationmatrixpositive)))))) /\ (forall mdr_i_bounded_minorrowminornonzeroevaluationmatrixnegative. (exists mdr_gap_bounded_minorrowminornonzeroevaluationmatrixnegativebound. mdr_gap_bounded_minorrowminornonzeroevaluationmatrixnegativebound + S (mdr_i_bounded_minorrowminornonzeroevaluationmatrixnegative) = ((q) * (q))) -> exists mdr_a_bounded_minorrowminornonzeroevaluationmatrixnegative. (((exists mdr_r_bounded_minorrowminornonzeroevaluationmatrixnegativepoint mdr_s_bounded_minorrowminornonzeroevaluationmatrixnegativepoint mdr_u_bounded_minorrowminornonzeroevaluationmatrixnegativepoint mdr_v_bounded_minorrowminornonzeroevaluationmatrixnegativepoint. ((mdr_i_bounded_minorrowminornonzeroevaluationmatrixnegative = (q) * mdr_r_bounded_minorrowminornonzeroevaluationmatrixnegativepoint + mdr_s_bounded_minorrowminornonzeroevaluationmatrixnegativepoint) /\ ((exists mdr_gap_bounded_minorrowminornonzeroevaluationmatrixnegativepointcolumn. mdr_gap_bounded_minorrowminornonzeroevaluationmatrixnegativepointcolumn + S (mdr_s_bounded_minorrowminornonzeroevaluationmatrixnegativepoint) = (q)) /\ ((((exists ff_h_mdr_bounded_minorrowminornonzeroevaluationmatrixnegativepointrow_index. ff_h_mdr_bounded_minorrowminornonzeroevaluationmatrixnegativepointrow_index + S (mdr_u_bounded_minorrowminornonzeroevaluationmatrixnegativepoint) = S ((S (mdr_r_bounded_minorrowminornonzeroevaluationmatrixnegativepoint)) * rc)) /\ exists ff_q_mdr_bounded_minorrowminornonzeroevaluationmatrixnegativepointrow_index. mdr_a_bounded_minorrows = ff_q_mdr_bounded_minorrowminornonzeroevaluationmatrixnegativepointrow_index * S ((S (mdr_r_bounded_minorrowminornonzeroevaluationmatrixnegativepoint)) * rc) + (mdr_u_bounded_minorrowminornonzeroevaluationmatrixnegativepoint))) /\ ((((exists ff_h_mdr_bounded_minorrowminornonzeroevaluationmatrixnegativepointcolumn_index. ff_h_mdr_bounded_minorrowminornonzeroevaluationmatrixnegativepointcolumn_index + S (mdr_v_bounded_minorrowminornonzeroevaluationmatrixnegativepoint) = S ((S (mdr_s_bounded_minorrowminornonzeroevaluationmatrixnegativepoint)) * cc)) /\ exists ff_q_mdr_bounded_minorrowminornonzeroevaluationmatrixnegativepointcolumn_index. mdr_a_bounded_minorrowcolumns = ff_q_mdr_bounded_minorrowminornonzeroevaluationmatrixnegativepointcolumn_index * S ((S (mdr_s_bounded_minorrowminornonzeroevaluationmatrixnegativepoint)) * cc) + (mdr_v_bounded_minorrowminornonzeroevaluationmatrixnegativepoint))) /\ (((exists ff_h_mdr_bounded_minorrowminornonzeroevaluationmatrixnegativepointsource. ff_h_mdr_bounded_minorrowminornonzeroevaluationmatrixnegativepointsource + S (mdr_a_bounded_minorrowminornonzeroevaluationmatrixnegative) = S ((S ((mdr_u_bounded_minorrowminornonzeroevaluationmatrixnegativepoint) * (w) + (mdr_v_bounded_minorrowminornonzeroevaluationmatrixnegativepoint))) * nc)) /\ exists ff_q_mdr_bounded_minorrowminornonzeroevaluationmatrixnegativepointsource. nb = ff_q_mdr_bounded_minorrowminornonzeroevaluationmatrixnegativepointsource * S ((S ((mdr_u_bounded_minorrowminornonzeroevaluationmatrixnegativepoint) * (w) + (mdr_v_bounded_minorrowminornonzeroevaluationmatrixnegativepoint))) * nc) + (mdr_a_bounded_minorrowminornonzeroevaluationmatrixnegative)))))))) /\ (((exists ff_h_mdr_bounded_minorrowminornonzeroevaluationmatrixnegativeoutput. ff_h_mdr_bounded_minorrowminornonzeroevaluationmatrixnegativeoutput + S (mdr_a_bounded_minorrowminornonzeroevaluationmatrixnegative) = S ((S (mdr_i_bounded_minorrowminornonzeroevaluationmatrixnegative)) * mdr_vc_bounded_minorrowminornonzeroevaluation)) /\ exists ff_q_mdr_bounded_minorrowminornonzeroevaluationmatrixnegativeoutput. mdr_vb_bounded_minorrowminornonzeroevaluation = ff_q_mdr_bounded_minorrowminornonzeroevaluationmatrixnegativeoutput * S ((S (mdr_i_bounded_minorrowminornonzeroevaluationmatrixnegative)) * mdr_vc_bounded_minorrowminornonzeroevaluation) + (mdr_a_bounded_minorrowminornonzeroevaluationmatrixnegative)))))))) /\ (exists mdr_b_bounded_minorrowminornonzeroevaluationdeterminant mdr_c_bounded_minorrowminornonzeroevaluationdeterminant mdr_l_bounded_minorrowminornonzeroevaluationdeterminant mdr_i_bounded_minorrowminornonzeroevaluationdeterminant. ((forall mdr_i_bounded_minorrowminornonzeroevaluationdeterminanth. (exists mdr_gap_bounded_minorrowminornonzeroevaluationdeterminanthi. mdr_gap_bounded_minorrowminornonzeroevaluationdeterminanthi + S (mdr_i_bounded_minorrowminornonzeroevaluationdeterminanth) = (mdr_l_bounded_minorrowminornonzeroevaluationdeterminant)) -> exists mdr_d_bounded_minorrowminornonzeroevaluationdeterminanth mdr_pb_bounded_minorrowminornonzeroevaluationdeterminanth mdr_pc_bounded_minorrowminornonzeroevaluationdeterminanth mdr_nb_bounded_minorrowminornonzeroevaluationdeterminanth mdr_nc_bounded_minorrowminornonzeroevaluationdeterminanth mdr_p_bounded_minorrowminornonzeroevaluationdeterminanth mdr_n_bounded_minorrowminornonzeroevaluationdeterminanth. ((exists mdr_z_bounded_minorrowminornonzeroevaluationdeterminanthr. ((exists mdr_a_bounded_minorrowminornonzeroevaluationdeterminanthrc mdr_b_bounded_minorrowminornonzeroevaluationdeterminanthrc mdr_c_bounded_minorrowminornonzeroevaluationdeterminanthrc mdr_e_bounded_minorrowminornonzeroevaluationdeterminanthrc mdr_f_bounded_minorrowminornonzeroevaluationdeterminanthrc. ((mdr_a_bounded_minorrowminornonzeroevaluationdeterminanthrc = ((mdr_d_bounded_minorrowminornonzeroevaluationdeterminanth) + (mdr_pb_bounded_minorrowminornonzeroevaluationdeterminanth)) * S ((mdr_d_bounded_minorrowminornonzeroevaluationdeterminanth) + (mdr_pb_bounded_minorrowminornonzeroevaluationdeterminanth)) + ((mdr_pb_bounded_minorrowminornonzeroevaluationdeterminanth) + (mdr_pb_bounded_minorrowminornonzeroevaluationdeterminanth))) /\ ((mdr_b_bounded_minorrowminornonzeroevaluationdeterminanthrc = ((mdr_pc_bounded_minorrowminornonzeroevaluationdeterminanth) + (mdr_nb_bounded_minorrowminornonzeroevaluationdeterminanth)) * S ((mdr_pc_bounded_minorrowminornonzeroevaluationdeterminanth) + (mdr_nb_bounded_minorrowminornonzeroevaluationdeterminanth)) + ((mdr_nb_bounded_minorrowminornonzeroevaluationdeterminanth) + (mdr_nb_bounded_minorrowminornonzeroevaluationdeterminanth))) /\ ((mdr_c_bounded_minorrowminornonzeroevaluationdeterminanthrc = ((mdr_a_bounded_minorrowminornonzeroevaluationdeterminanthrc) + (mdr_b_bounded_minorrowminornonzeroevaluationdeterminanthrc)) * S ((mdr_a_bounded_minorrowminornonzeroevaluationdeterminanthrc) + (mdr_b_bounded_minorrowminornonzeroevaluationdeterminanthrc)) + ((mdr_b_bounded_minorrowminornonzeroevaluationdeterminanthrc) + (mdr_b_bounded_minorrowminornonzeroevaluationdeterminanthrc))) /\ ((mdr_e_bounded_minorrowminornonzeroevaluationdeterminanthrc = ((mdr_p_bounded_minorrowminornonzeroevaluationdeterminanth) + (mdr_n_bounded_minorrowminornonzeroevaluationdeterminanth)) * S ((mdr_p_bounded_minorrowminornonzeroevaluationdeterminanth) + (mdr_n_bounded_minorrowminornonzeroevaluationdeterminanth)) + ((mdr_n_bounded_minorrowminornonzeroevaluationdeterminanth) + (mdr_n_bounded_minorrowminornonzeroevaluationdeterminanth))) /\ ((mdr_f_bounded_minorrowminornonzeroevaluationdeterminanthrc = ((mdr_nc_bounded_minorrowminornonzeroevaluationdeterminanth) + (mdr_e_bounded_minorrowminornonzeroevaluationdeterminanthrc)) * S ((mdr_nc_bounded_minorrowminornonzeroevaluationdeterminanth) + (mdr_e_bounded_minorrowminornonzeroevaluationdeterminanthrc)) + ((mdr_e_bounded_minorrowminornonzeroevaluationdeterminanthrc) + (mdr_e_bounded_minorrowminornonzeroevaluationdeterminanthrc))) /\ ((mdr_z_bounded_minorrowminornonzeroevaluationdeterminanthr) = ((mdr_c_bounded_minorrowminornonzeroevaluationdeterminanthrc) + (mdr_f_bounded_minorrowminornonzeroevaluationdeterminanthrc)) * S ((mdr_c_bounded_minorrowminornonzeroevaluationdeterminanthrc) + (mdr_f_bounded_minorrowminornonzeroevaluationdeterminanthrc)) + ((mdr_f_bounded_minorrowminornonzeroevaluationdeterminanthrc) + (mdr_f_bounded_minorrowminornonzeroevaluationdeterminanthrc))))))))) /\ (((exists ff_h_mdr_bounded_minorrowminornonzeroevaluationdeterminanthrb. ff_h_mdr_bounded_minorrowminornonzeroevaluationdeterminanthrb + S (mdr_z_bounded_minorrowminornonzeroevaluationdeterminanthr) = S ((S (mdr_i_bounded_minorrowminornonzeroevaluationdeterminanth)) * mdr_c_bounded_minorrowminornonzeroevaluationdeterminant)) /\ exists ff_q_mdr_bounded_minorrowminornonzeroevaluationdeterminanthrb. mdr_b_bounded_minorrowminornonzeroevaluationdeterminant = ff_q_mdr_bounded_minorrowminornonzeroevaluationdeterminanthrb * S ((S (mdr_i_bounded_minorrowminornonzeroevaluationdeterminanth)) * mdr_c_bounded_minorrowminornonzeroevaluationdeterminant) + (mdr_z_bounded_minorrowminornonzeroevaluationdeterminanthr))))) /\ (((((mdr_d_bounded_minorrowminornonzeroevaluationdeterminanth) = 0) /\ (((mdr_p_bounded_minorrowminornonzeroevaluationdeterminanth) = 1) /\ ((mdr_n_bounded_minorrowminornonzeroevaluationdeterminanth) = 0))) \/ exists mdr_q_bounded_minorrowminornonzeroevaluationdeterminanths mdr_eb_bounded_minorrowminornonzeroevaluationdeterminanths mdr_ec_bounded_minorrowminornonzeroevaluationdeterminanths mdr_fb_bounded_minorrowminornonzeroevaluationdeterminanths mdr_fc_bounded_minorrowminornonzeroevaluationdeterminanths. (((mdr_d_bounded_minorrowminornonzeroevaluationdeterminanth) = S (mdr_q_bounded_minorrowminornonzeroevaluationdeterminanths)) /\ ((forall mdr_j_bounded_minorrowminornonzeroevaluationdeterminanthsc. (exists mdr_gap_bounded_minorrowminornonzeroevaluationdeterminanthscj. mdr_gap_bounded_minorrowminornonzeroevaluationdeterminanthscj + S (mdr_j_bounded_minorrowminornonzeroevaluationdeterminanthsc) = (S (mdr_q_bounded_minorrowminornonzeroevaluationdeterminanths))) -> exists mdr_i_bounded_minorrowminornonzeroevaluationdeterminanthsc mdr_up_bounded_minorrowminornonzeroevaluationdeterminanthsc mdr_us_bounded_minorrowminornonzeroevaluationdeterminanthsc mdr_un_bounded_minorrowminornonzeroevaluationdeterminanthsc mdr_ut_bounded_minorrowminornonzeroevaluationdeterminanthsc mdr_p_bounded_minorrowminornonzeroevaluationdeterminanthsc mdr_n_bounded_minorrowminornonzeroevaluationdeterminanthsc. ((exists mdr_gap_bounded_minorrowminornonzeroevaluationdeterminanthsci. mdr_gap_bounded_minorrowminornonzeroevaluationdeterminanthsci + S (mdr_i_bounded_minorrowminornonzeroevaluationdeterminanthsc) = (mdr_i_bounded_minorrowminornonzeroevaluationdeterminanth)) /\ ((exists mdr_z_bounded_minorrowminornonzeroevaluationdeterminanthscr. ((exists mdr_a_bounded_minorrowminornonzeroevaluationdeterminanthscrc mdr_b_bounded_minorrowminornonzeroevaluationdeterminanthscrc mdr_c_bounded_minorrowminornonzeroevaluationdeterminanthscrc mdr_e_bounded_minorrowminornonzeroevaluationdeterminanthscrc mdr_f_bounded_minorrowminornonzeroevaluationdeterminanthscrc. ((mdr_a_bounded_minorrowminornonzeroevaluationdeterminanthscrc = ((mdr_q_bounded_minorrowminornonzeroevaluationdeterminanths) + (mdr_up_bounded_minorrowminornonzeroevaluationdeterminanthsc)) * S ((mdr_q_bounded_minorrowminornonzeroevaluationdeterminanths) + (mdr_up_bounded_minorrowminornonzeroevaluationdeterminanthsc)) + ((mdr_up_bounded_minorrowminornonzeroevaluationdeterminanthsc) + (mdr_up_bounded_minorrowminornonzeroevaluationdeterminanthsc))) /\ ((mdr_b_bounded_minorrowminornonzeroevaluationdeterminanthscrc = ((mdr_us_bounded_minorrowminornonzeroevaluationdeterminanthsc) + (mdr_un_bounded_minorrowminornonzeroevaluationdeterminanthsc)) * S ((mdr_us_bounded_minorrowminornonzeroevaluationdeterminanthsc) + (mdr_un_bounded_minorrowminornonzeroevaluationdeterminanthsc)) + ((mdr_un_bounded_minorrowminornonzeroevaluationdeterminanthsc) + (mdr_un_bounded_minorrowminornonzeroevaluationdeterminanthsc))) /\ ((mdr_c_bounded_minorrowminornonzeroevaluationdeterminanthscrc = ((mdr_a_bounded_minorrowminornonzeroevaluationdeterminanthscrc) + (mdr_b_bounded_minorrowminornonzeroevaluationdeterminanthscrc)) * S ((mdr_a_bounded_minorrowminornonzeroevaluationdeterminanthscrc) + (mdr_b_bounded_minorrowminornonzeroevaluationdeterminanthscrc)) + ((mdr_b_bounded_minorrowminornonzeroevaluationdeterminanthscrc) + (mdr_b_bounded_minorrowminornonzeroevaluationdeterminanthscrc))) /\ ((mdr_e_bounded_minorrowminornonzeroevaluationdeterminanthscrc = ((mdr_p_bounded_minorrowminornonzeroevaluationdeterminanthsc) + (mdr_n_bounded_minorrowminornonzeroevaluationdeterminanthsc)) * S ((mdr_p_bounded_minorrowminornonzeroevaluationdeterminanthsc) + (mdr_n_bounded_minorrowminornonzeroevaluationdeterminanthsc)) + ((mdr_n_bounded_minorrowminornonzeroevaluationdeterminanthsc) + (mdr_n_bounded_minorrowminornonzeroevaluationdeterminanthsc))) /\ ((mdr_f_bounded_minorrowminornonzeroevaluationdeterminanthscrc = ((mdr_ut_bounded_minorrowminornonzeroevaluationdeterminanthsc) + (mdr_e_bounded_minorrowminornonzeroevaluationdeterminanthscrc)) * S ((mdr_ut_bounded_minorrowminornonzeroevaluationdeterminanthsc) + (mdr_e_bounded_minorrowminornonzeroevaluationdeterminanthscrc)) + ((mdr_e_bounded_minorrowminornonzeroevaluationdeterminanthscrc) + (mdr_e_bounded_minorrowminornonzeroevaluationdeterminanthscrc))) /\ ((mdr_z_bounded_minorrowminornonzeroevaluationdeterminanthscr) = ((mdr_c_bounded_minorrowminornonzeroevaluationdeterminanthscrc) + (mdr_f_bounded_minorrowminornonzeroevaluationdeterminanthscrc)) * S ((mdr_c_bounded_minorrowminornonzeroevaluationdeterminanthscrc) + (mdr_f_bounded_minorrowminornonzeroevaluationdeterminanthscrc)) + ((mdr_f_bounded_minorrowminornonzeroevaluationdeterminanthscrc) + (mdr_f_bounded_minorrowminornonzeroevaluationdeterminanthscrc))))))))) /\ (((exists ff_h_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscrb. ff_h_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscrb + S (mdr_z_bounded_minorrowminornonzeroevaluationdeterminanthscr) = S ((S (mdr_i_bounded_minorrowminornonzeroevaluationdeterminanthsc)) * mdr_c_bounded_minorrowminornonzeroevaluationdeterminant)) /\ exists ff_q_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscrb. mdr_b_bounded_minorrowminornonzeroevaluationdeterminant = ff_q_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscrb * S ((S (mdr_i_bounded_minorrowminornonzeroevaluationdeterminanthsc)) * mdr_c_bounded_minorrowminornonzeroevaluationdeterminant) + (mdr_z_bounded_minorrowminornonzeroevaluationdeterminanthscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_positive. (exists ff_gap_mdm_lt_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_positive_index_bound. ff_gap_mdm_lt_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_positive) = ((mdr_q_bounded_minorrowminornonzeroevaluationdeterminanths) * (mdr_q_bounded_minorrowminornonzeroevaluationdeterminanths))) -> exists ff_row_mdm_prefix_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_positive ff_column_mdm_prefix_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_positive ff_value_mdm_prefix_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_positive. (ff_index_mdm_prefix_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_positive = (mdr_q_bounded_minorrowminornonzeroevaluationdeterminanths) * ff_row_mdm_prefix_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_positive + ff_column_mdm_prefix_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_positive /\ ((exists ff_gap_mdm_lt_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_positive_column_bound. ff_gap_mdm_lt_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_positive) = (mdr_q_bounded_minorrowminornonzeroevaluationdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_positive_cell ff_column_mdm_cell_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_positive_cell = ff_row_mdm_prefix_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_positive_cell_row_after. ff_gap_mdm_le_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_positive)) /\ ff_row_mdm_cell_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_positive_cell = S ff_row_mdm_prefix_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_positive) = (mdr_j_bounded_minorrowminornonzeroevaluationdeterminanthsc)) /\ ff_column_mdm_cell_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_positive_cell = ff_column_mdm_prefix_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_positive_cell_column_after. ff_gap_mdm_le_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_positive_cell_column_after + (mdr_j_bounded_minorrowminornonzeroevaluationdeterminanthsc) = (ff_column_mdm_prefix_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_positive)) /\ ff_column_mdm_cell_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_positive_cell = S ff_column_mdm_prefix_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_positive))) /\ (((exists ff_h_mdm_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_positive_cell_source. ff_h_mdm_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_positive) = S ((S ((ff_row_mdm_cell_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_positive_cell) * (S (mdr_q_bounded_minorrowminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_positive_cell))) * mdr_pc_bounded_minorrowminornonzeroevaluationdeterminanth)) /\ exists ff_q_mdm_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_positive_cell_source. mdr_pb_bounded_minorrowminornonzeroevaluationdeterminanth = ff_q_mdm_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_positive_cell) * (S (mdr_q_bounded_minorrowminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_positive_cell))) * mdr_pc_bounded_minorrowminornonzeroevaluationdeterminanth) + (ff_value_mdm_prefix_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_positive)))))) /\ (((exists ff_h_mdm_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_positive_target. ff_h_mdm_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_positive_target + S (ff_value_mdm_prefix_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_positive) = S ((S (ff_index_mdm_prefix_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_positive)) * mdr_us_bounded_minorrowminornonzeroevaluationdeterminanthsc)) /\ exists ff_q_mdm_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_positive_target. mdr_up_bounded_minorrowminornonzeroevaluationdeterminanthsc = ff_q_mdm_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_positive)) * mdr_us_bounded_minorrowminornonzeroevaluationdeterminanthsc) + (ff_value_mdm_prefix_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_negative. (exists ff_gap_mdm_lt_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_negative_index_bound. ff_gap_mdm_lt_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_negative) = ((mdr_q_bounded_minorrowminornonzeroevaluationdeterminanths) * (mdr_q_bounded_minorrowminornonzeroevaluationdeterminanths))) -> exists ff_row_mdm_prefix_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_negative ff_column_mdm_prefix_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_negative ff_value_mdm_prefix_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_negative. (ff_index_mdm_prefix_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_negative = (mdr_q_bounded_minorrowminornonzeroevaluationdeterminanths) * ff_row_mdm_prefix_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_negative + ff_column_mdm_prefix_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_negative /\ ((exists ff_gap_mdm_lt_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_negative_column_bound. ff_gap_mdm_lt_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_negative) = (mdr_q_bounded_minorrowminornonzeroevaluationdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_negative_cell ff_column_mdm_cell_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_negative_cell = ff_row_mdm_prefix_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_negative_cell_row_after. ff_gap_mdm_le_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_negative)) /\ ff_row_mdm_cell_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_negative_cell = S ff_row_mdm_prefix_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_negative) = (mdr_j_bounded_minorrowminornonzeroevaluationdeterminanthsc)) /\ ff_column_mdm_cell_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_negative_cell = ff_column_mdm_prefix_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_negative_cell_column_after. ff_gap_mdm_le_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_negative_cell_column_after + (mdr_j_bounded_minorrowminornonzeroevaluationdeterminanthsc) = (ff_column_mdm_prefix_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_negative)) /\ ff_column_mdm_cell_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_negative_cell = S ff_column_mdm_prefix_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_negative))) /\ (((exists ff_h_mdm_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_negative_cell_source. ff_h_mdm_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_negative) = S ((S ((ff_row_mdm_cell_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_negative_cell) * (S (mdr_q_bounded_minorrowminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_negative_cell))) * mdr_nc_bounded_minorrowminornonzeroevaluationdeterminanth)) /\ exists ff_q_mdm_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_negative_cell_source. mdr_nb_bounded_minorrowminornonzeroevaluationdeterminanth = ff_q_mdm_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_negative_cell) * (S (mdr_q_bounded_minorrowminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_negative_cell))) * mdr_nc_bounded_minorrowminornonzeroevaluationdeterminanth) + (ff_value_mdm_prefix_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_negative)))))) /\ (((exists ff_h_mdm_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_negative_target. ff_h_mdm_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_negative_target + S (ff_value_mdm_prefix_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_negative) = S ((S (ff_index_mdm_prefix_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_negative)) * mdr_ut_bounded_minorrowminornonzeroevaluationdeterminanthsc)) /\ exists ff_q_mdm_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_negative_target. mdr_un_bounded_minorrowminornonzeroevaluationdeterminanthsc = ff_q_mdm_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_negative)) * mdr_ut_bounded_minorrowminornonzeroevaluationdeterminanthsc) + (ff_value_mdm_prefix_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_negative))))))))) /\ ((((exists ff_h_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscp. ff_h_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscp + S (mdr_p_bounded_minorrowminornonzeroevaluationdeterminanthsc) = S ((S (mdr_j_bounded_minorrowminornonzeroevaluationdeterminanthsc)) * mdr_ec_bounded_minorrowminornonzeroevaluationdeterminanths)) /\ exists ff_q_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscp. mdr_eb_bounded_minorrowminornonzeroevaluationdeterminanths = ff_q_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscp * S ((S (mdr_j_bounded_minorrowminornonzeroevaluationdeterminanthsc)) * mdr_ec_bounded_minorrowminornonzeroevaluationdeterminanths) + (mdr_p_bounded_minorrowminornonzeroevaluationdeterminanthsc))) /\ (((exists ff_h_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscn. ff_h_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscn + S (mdr_n_bounded_minorrowminornonzeroevaluationdeterminanthsc) = S ((S (mdr_j_bounded_minorrowminornonzeroevaluationdeterminanthsc)) * mdr_fc_bounded_minorrowminornonzeroevaluationdeterminanths)) /\ exists ff_q_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscn. mdr_fb_bounded_minorrowminornonzeroevaluationdeterminanths = ff_q_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscn * S ((S (mdr_j_bounded_minorrowminornonzeroevaluationdeterminanthsc)) * mdr_fc_bounded_minorrowminornonzeroevaluationdeterminanths) + (mdr_n_bounded_minorrowminornonzeroevaluationdeterminanthsc)))))))) /\ (exists ff_ub_mce_fold_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf ff_uc_mce_fold_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf ff_vb_mce_fold_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf ff_vc_mce_fold_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf. ((forall ff_index_mce_alternating_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix. (exists ff_gap_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix_index. ff_gap_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix_index + S (ff_index_mce_alternating_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix) = (S (mdr_q_bounded_minorrowminornonzeroevaluationdeterminanths))) -> exists ff_ap_mce_alternating_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix ff_an_mce_alternating_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix ff_bp_mce_alternating_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix ff_bn_mce_alternating_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix ff_p_mce_alternating_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix ff_n_mce_alternating_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix. ((((exists ff_h_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix_ap. ff_h_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix_ap + S (ff_ap_mce_alternating_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix)) * mdr_pc_bounded_minorrowminornonzeroevaluationdeterminanth)) /\ exists ff_q_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix_ap. mdr_pb_bounded_minorrowminornonzeroevaluationdeterminanth = ff_q_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix)) * mdr_pc_bounded_minorrowminornonzeroevaluationdeterminanth) + (ff_ap_mce_alternating_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix_an. ff_h_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix_an + S (ff_an_mce_alternating_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix)) * mdr_nc_bounded_minorrowminornonzeroevaluationdeterminanth)) /\ exists ff_q_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix_an. mdr_nb_bounded_minorrowminornonzeroevaluationdeterminanth = ff_q_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix)) * mdr_nc_bounded_minorrowminornonzeroevaluationdeterminanth) + (ff_an_mce_alternating_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix_bp. ff_h_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix_bp + S (ff_bp_mce_alternating_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix)) * mdr_ec_bounded_minorrowminornonzeroevaluationdeterminanths)) /\ exists ff_q_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix_bp. mdr_eb_bounded_minorrowminornonzeroevaluationdeterminanths = ff_q_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix)) * mdr_ec_bounded_minorrowminornonzeroevaluationdeterminanths) + (ff_bp_mce_alternating_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix_bn. ff_h_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix_bn + S (ff_bn_mce_alternating_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix)) * mdr_fc_bounded_minorrowminornonzeroevaluationdeterminanths)) /\ exists ff_q_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix_bn. mdr_fb_bounded_minorrowminornonzeroevaluationdeterminanths = ff_q_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix)) * mdr_fc_bounded_minorrowminornonzeroevaluationdeterminanths) + (ff_bn_mce_alternating_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix_positive. ff_h_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix_positive + S (ff_p_mce_alternating_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix_positive. ff_ub_mce_fold_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf) + (ff_p_mce_alternating_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix_negative. ff_h_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix_negative + S (ff_n_mce_alternating_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix_negative. ff_vb_mce_fold_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf) + (ff_n_mce_alternating_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix))) /\ (((exists ff_even_mce_term_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix = 2 * ff_even_mce_term_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix_term) /\ (ff_p_mce_alternating_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix = 2 * ff_odd_mce_term_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_positive ff_v_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_positive. ((((exists ff_h_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_positive_start. ff_h_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_positive_start. ff_u_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_positive_start * S ((S (0)) * ff_v_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_positive_terminal. ff_h_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_positive_terminal + S (mdr_p_bounded_minorrowminornonzeroevaluationdeterminanth) = S ((S ((S (mdr_q_bounded_minorrowminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_positive_terminal. ff_u_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_positive_terminal * S ((S ((S (mdr_q_bounded_minorrowminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_positive) + (mdr_p_bounded_minorrowminornonzeroevaluationdeterminanth))) /\ forall ff_i_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_positive. (exists ff_lt_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_positive_bound. ff_lt_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_positive_bound + S ff_i_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_positive = (S (mdr_q_bounded_minorrowminornonzeroevaluationdeterminanths))) -> exists ff_a_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_positive ff_r_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_positive ff_s_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_positive. ((((exists ff_h_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_positive_summand. ff_h_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_positive_summand + S (ff_a_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_positive_summand. ff_ub_mce_fold_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_positive_summand * S ((S (ff_i_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf) + (ff_a_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_positive_partial. ff_h_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_positive_partial + S (ff_r_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_positive_partial. ff_u_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_positive_partial * S ((S (ff_i_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_positive) + (ff_r_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_positive_successor. ff_h_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_positive_successor + S (ff_s_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_positive) = S ((S (S ff_i_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_positive_successor. ff_u_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_positive_successor * S ((S (S ff_i_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_positive) + (ff_s_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_positive))) /\ ff_s_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_positive = ff_r_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_positive + ff_a_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_positive)))))) /\ (exists ff_u_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_negative ff_v_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_negative. ((((exists ff_h_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_negative_start. ff_h_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_negative_start. ff_u_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_negative_start * S ((S (0)) * ff_v_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_negative_terminal. ff_h_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_negative_terminal + S (mdr_n_bounded_minorrowminornonzeroevaluationdeterminanth) = S ((S ((S (mdr_q_bounded_minorrowminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_negative_terminal. ff_u_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_negative_terminal * S ((S ((S (mdr_q_bounded_minorrowminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_negative) + (mdr_n_bounded_minorrowminornonzeroevaluationdeterminanth))) /\ forall ff_i_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_negative. (exists ff_lt_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_negative_bound. ff_lt_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_negative_bound + S ff_i_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_negative = (S (mdr_q_bounded_minorrowminornonzeroevaluationdeterminanths))) -> exists ff_a_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_negative ff_r_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_negative ff_s_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_negative. ((((exists ff_h_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_negative_summand. ff_h_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_negative_summand + S (ff_a_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_negative_summand. ff_vb_mce_fold_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_negative_summand * S ((S (ff_i_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf) + (ff_a_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_negative_partial. ff_h_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_negative_partial + S (ff_r_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_negative_partial. ff_u_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_negative_partial * S ((S (ff_i_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_negative) + (ff_r_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_negative_successor. ff_h_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_negative_successor + S (ff_s_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_negative) = S ((S (S ff_i_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_negative_successor. ff_u_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_negative_successor * S ((S (S ff_i_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_negative) + (ff_s_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_negative))) /\ ff_s_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_negative = ff_r_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_negative + ff_a_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_negative))))))))))))))) /\ ((exists mdr_gap_bounded_minorrowminornonzeroevaluationdeterminanti. mdr_gap_bounded_minorrowminornonzeroevaluationdeterminanti + S (mdr_i_bounded_minorrowminornonzeroevaluationdeterminant) = (mdr_l_bounded_minorrowminornonzeroevaluationdeterminant)) /\ (exists mdr_z_bounded_minorrowminornonzeroevaluationdeterminantr. ((exists mdr_a_bounded_minorrowminornonzeroevaluationdeterminantrc mdr_b_bounded_minorrowminornonzeroevaluationdeterminantrc mdr_c_bounded_minorrowminornonzeroevaluationdeterminantrc mdr_e_bounded_minorrowminornonzeroevaluationdeterminantrc mdr_f_bounded_minorrowminornonzeroevaluationdeterminantrc. ((mdr_a_bounded_minorrowminornonzeroevaluationdeterminantrc = ((q) + (mdr_ub_bounded_minorrowminornonzeroevaluation)) * S ((q) + (mdr_ub_bounded_minorrowminornonzeroevaluation)) + ((mdr_ub_bounded_minorrowminornonzeroevaluation) + (mdr_ub_bounded_minorrowminornonzeroevaluation))) /\ ((mdr_b_bounded_minorrowminornonzeroevaluationdeterminantrc = ((mdr_uc_bounded_minorrowminornonzeroevaluation) + (mdr_vb_bounded_minorrowminornonzeroevaluation)) * S ((mdr_uc_bounded_minorrowminornonzeroevaluation) + (mdr_vb_bounded_minorrowminornonzeroevaluation)) + ((mdr_vb_bounded_minorrowminornonzeroevaluation) + (mdr_vb_bounded_minorrowminornonzeroevaluation))) /\ ((mdr_c_bounded_minorrowminornonzeroevaluationdeterminantrc = ((mdr_a_bounded_minorrowminornonzeroevaluationdeterminantrc) + (mdr_b_bounded_minorrowminornonzeroevaluationdeterminantrc)) * S ((mdr_a_bounded_minorrowminornonzeroevaluationdeterminantrc) + (mdr_b_bounded_minorrowminornonzeroevaluationdeterminantrc)) + ((mdr_b_bounded_minorrowminornonzeroevaluationdeterminantrc) + (mdr_b_bounded_minorrowminornonzeroevaluationdeterminantrc))) /\ ((mdr_e_bounded_minorrowminornonzeroevaluationdeterminantrc = ((mdr_p_bounded_minorrowminornonzero) + (mdr_n_bounded_minorrowminornonzero)) * S ((mdr_p_bounded_minorrowminornonzero) + (mdr_n_bounded_minorrowminornonzero)) + ((mdr_n_bounded_minorrowminornonzero) + (mdr_n_bounded_minorrowminornonzero))) /\ ((mdr_f_bounded_minorrowminornonzeroevaluationdeterminantrc = ((mdr_vc_bounded_minorrowminornonzeroevaluation) + (mdr_e_bounded_minorrowminornonzeroevaluationdeterminantrc)) * S ((mdr_vc_bounded_minorrowminornonzeroevaluation) + (mdr_e_bounded_minorrowminornonzeroevaluationdeterminantrc)) + ((mdr_e_bounded_minorrowminornonzeroevaluationdeterminantrc) + (mdr_e_bounded_minorrowminornonzeroevaluationdeterminantrc))) /\ ((mdr_z_bounded_minorrowminornonzeroevaluationdeterminantr) = ((mdr_c_bounded_minorrowminornonzeroevaluationdeterminantrc) + (mdr_f_bounded_minorrowminornonzeroevaluationdeterminantrc)) * S ((mdr_c_bounded_minorrowminornonzeroevaluationdeterminantrc) + (mdr_f_bounded_minorrowminornonzeroevaluationdeterminantrc)) + ((mdr_f_bounded_minorrowminornonzeroevaluationdeterminantrc) + (mdr_f_bounded_minorrowminornonzeroevaluationdeterminantrc))))))))) /\ (((exists ff_h_mdr_bounded_minorrowminornonzeroevaluationdeterminantrb. ff_h_mdr_bounded_minorrowminornonzeroevaluationdeterminantrb + S (mdr_z_bounded_minorrowminornonzeroevaluationdeterminantr) = S ((S (mdr_i_bounded_minorrowminornonzeroevaluationdeterminant)) * mdr_c_bounded_minorrowminornonzeroevaluationdeterminant)) /\ exists ff_q_mdr_bounded_minorrowminornonzeroevaluationdeterminantrb. mdr_b_bounded_minorrowminornonzeroevaluationdeterminant = ff_q_mdr_bounded_minorrowminornonzeroevaluationdeterminantrb * S ((S (mdr_i_bounded_minorrowminornonzeroevaluationdeterminant)) * mdr_c_bounded_minorrowminornonzeroevaluationdeterminant) + (mdr_z_bounded_minorrowminornonzeroevaluationdeterminantr)))))))))) /\ (~(mdr_p_bounded_minorrowminornonzero = mdr_n_bounded_minorrowminornonzero)))))))))))))