Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.
This branch proves the finite determinant/rank/span substrate. It does not claim Smith or Hermite normal form, lattice index equals determinant, determinant multiplicativity, lattice reduction, or geometry-of-numbers theorems.
Exact theorem in conservative defined notation
∀ pb. ∀ pc. ∀ nb. ∀ nc. ∀ r. ∀ w. ∀ q. ¬NonzeroMatrixMinor(pb,pc,nb,nc,r,w,q) → AllSignedMinorsZero(pb,pc,nb,nc,r,w,q)Every linked abbreviation expands hygienically to the identical original native formula.
Definition DAG
Actual proof prerequisites
eq_decidable · checked external prerequisite
Original expanded first-order statement
forall pb pc nb nc r w q. ~(exists mdr_rb_absent_minor mdr_rc_absent_minor mdr_cb_absent_minor mdr_cc_absent_minor. (((((forall fom_index_mrf_absent_minorminorrowsbound. (exists fom_gap_mrf_absent_minorminorrowsbound_index_bound. fom_gap_mrf_absent_minorminorrowsbound_index_bound + S (fom_index_mrf_absent_minorminorrowsbound) = q) -> exists fom_value_mrf_absent_minorminorrowsbound. ((((exists fom_beta_height_mrf_absent_minorminorrowsbound_entry. fom_beta_height_mrf_absent_minorminorrowsbound_entry + S (fom_value_mrf_absent_minorminorrowsbound) = S ((S (fom_index_mrf_absent_minorminorrowsbound)) * mdr_rc_absent_minor)) /\ exists fom_beta_quotient_mrf_absent_minorminorrowsbound_entry. mdr_rb_absent_minor = fom_beta_quotient_mrf_absent_minorminorrowsbound_entry * S ((S (fom_index_mrf_absent_minorminorrowsbound)) * mdr_rc_absent_minor) + (fom_value_mrf_absent_minorminorrowsbound))) /\ (exists fom_gap_mrf_absent_minorminorrowsbound_value_bound. fom_gap_mrf_absent_minorminorrowsbound_value_bound + S (fom_value_mrf_absent_minorminorrowsbound) = r))) /\ (forall mdr_i_absent_minorminorrowsdistinct mdr_j_absent_minorminorrowsdistinct mdr_a_absent_minorminorrowsdistinct. (exists mdr_gap_absent_minorminorrowsdistincti. mdr_gap_absent_minorminorrowsdistincti + S (mdr_i_absent_minorminorrowsdistinct) = (q)) -> (exists mdr_gap_absent_minorminorrowsdistinctj. mdr_gap_absent_minorminorrowsdistinctj + S (mdr_j_absent_minorminorrowsdistinct) = (q)) -> (((exists ff_h_mdr_absent_minorminorrowsdistinctfirst. ff_h_mdr_absent_minorminorrowsdistinctfirst + S (mdr_a_absent_minorminorrowsdistinct) = S ((S (mdr_i_absent_minorminorrowsdistinct)) * mdr_rc_absent_minor)) /\ exists ff_q_mdr_absent_minorminorrowsdistinctfirst. mdr_rb_absent_minor = ff_q_mdr_absent_minorminorrowsdistinctfirst * S ((S (mdr_i_absent_minorminorrowsdistinct)) * mdr_rc_absent_minor) + (mdr_a_absent_minorminorrowsdistinct))) -> (((exists ff_h_mdr_absent_minorminorrowsdistinctsecond. ff_h_mdr_absent_minorminorrowsdistinctsecond + S (mdr_a_absent_minorminorrowsdistinct) = S ((S (mdr_j_absent_minorminorrowsdistinct)) * mdr_rc_absent_minor)) /\ exists ff_q_mdr_absent_minorminorrowsdistinctsecond. mdr_rb_absent_minor = ff_q_mdr_absent_minorminorrowsdistinctsecond * S ((S (mdr_j_absent_minorminorrowsdistinct)) * mdr_rc_absent_minor) + (mdr_a_absent_minorminorrowsdistinct))) -> mdr_i_absent_minorminorrowsdistinct = mdr_j_absent_minorminorrowsdistinct))) /\ ((((forall fom_index_mrf_absent_minorminorcolumnsbound. (exists fom_gap_mrf_absent_minorminorcolumnsbound_index_bound. fom_gap_mrf_absent_minorminorcolumnsbound_index_bound + S (fom_index_mrf_absent_minorminorcolumnsbound) = q) -> exists fom_value_mrf_absent_minorminorcolumnsbound. ((((exists fom_beta_height_mrf_absent_minorminorcolumnsbound_entry. fom_beta_height_mrf_absent_minorminorcolumnsbound_entry + S (fom_value_mrf_absent_minorminorcolumnsbound) = S ((S (fom_index_mrf_absent_minorminorcolumnsbound)) * mdr_cc_absent_minor)) /\ exists fom_beta_quotient_mrf_absent_minorminorcolumnsbound_entry. mdr_cb_absent_minor = fom_beta_quotient_mrf_absent_minorminorcolumnsbound_entry * S ((S (fom_index_mrf_absent_minorminorcolumnsbound)) * mdr_cc_absent_minor) + (fom_value_mrf_absent_minorminorcolumnsbound))) /\ (exists fom_gap_mrf_absent_minorminorcolumnsbound_value_bound. fom_gap_mrf_absent_minorminorcolumnsbound_value_bound + S (fom_value_mrf_absent_minorminorcolumnsbound) = w))) /\ (forall mdr_i_absent_minorminorcolumnsdistinct mdr_j_absent_minorminorcolumnsdistinct mdr_a_absent_minorminorcolumnsdistinct. (exists mdr_gap_absent_minorminorcolumnsdistincti. mdr_gap_absent_minorminorcolumnsdistincti + S (mdr_i_absent_minorminorcolumnsdistinct) = (q)) -> (exists mdr_gap_absent_minorminorcolumnsdistinctj. mdr_gap_absent_minorminorcolumnsdistinctj + S (mdr_j_absent_minorminorcolumnsdistinct) = (q)) -> (((exists ff_h_mdr_absent_minorminorcolumnsdistinctfirst. ff_h_mdr_absent_minorminorcolumnsdistinctfirst + S (mdr_a_absent_minorminorcolumnsdistinct) = S ((S (mdr_i_absent_minorminorcolumnsdistinct)) * mdr_cc_absent_minor)) /\ exists ff_q_mdr_absent_minorminorcolumnsdistinctfirst. mdr_cb_absent_minor = ff_q_mdr_absent_minorminorcolumnsdistinctfirst * S ((S (mdr_i_absent_minorminorcolumnsdistinct)) * mdr_cc_absent_minor) + (mdr_a_absent_minorminorcolumnsdistinct))) -> (((exists ff_h_mdr_absent_minorminorcolumnsdistinctsecond. ff_h_mdr_absent_minorminorcolumnsdistinctsecond + S (mdr_a_absent_minorminorcolumnsdistinct) = S ((S (mdr_j_absent_minorminorcolumnsdistinct)) * mdr_cc_absent_minor)) /\ exists ff_q_mdr_absent_minorminorcolumnsdistinctsecond. mdr_cb_absent_minor = ff_q_mdr_absent_minorminorcolumnsdistinctsecond * S ((S (mdr_j_absent_minorminorcolumnsdistinct)) * mdr_cc_absent_minor) + (mdr_a_absent_minorminorcolumnsdistinct))) -> mdr_i_absent_minorminorcolumnsdistinct = mdr_j_absent_minorminorcolumnsdistinct))) /\ (exists mdr_p_absent_minorminornonzero mdr_n_absent_minorminornonzero. ((exists mdr_ub_absent_minorminornonzeroevaluation mdr_uc_absent_minorminornonzeroevaluation mdr_vb_absent_minorminornonzeroevaluation mdr_vc_absent_minorminornonzeroevaluation. ((((forall mdr_i_absent_minorminornonzeroevaluationmatrixpositive. (exists mdr_gap_absent_minorminornonzeroevaluationmatrixpositivebound. mdr_gap_absent_minorminornonzeroevaluationmatrixpositivebound + S (mdr_i_absent_minorminornonzeroevaluationmatrixpositive) = ((q) * (q))) -> exists mdr_a_absent_minorminornonzeroevaluationmatrixpositive. (((exists mdr_r_absent_minorminornonzeroevaluationmatrixpositivepoint mdr_s_absent_minorminornonzeroevaluationmatrixpositivepoint mdr_u_absent_minorminornonzeroevaluationmatrixpositivepoint mdr_v_absent_minorminornonzeroevaluationmatrixpositivepoint. ((mdr_i_absent_minorminornonzeroevaluationmatrixpositive = (q) * mdr_r_absent_minorminornonzeroevaluationmatrixpositivepoint + mdr_s_absent_minorminornonzeroevaluationmatrixpositivepoint) /\ ((exists mdr_gap_absent_minorminornonzeroevaluationmatrixpositivepointcolumn. mdr_gap_absent_minorminornonzeroevaluationmatrixpositivepointcolumn + S (mdr_s_absent_minorminornonzeroevaluationmatrixpositivepoint) = (q)) /\ ((((exists ff_h_mdr_absent_minorminornonzeroevaluationmatrixpositivepointrow_index. ff_h_mdr_absent_minorminornonzeroevaluationmatrixpositivepointrow_index + S (mdr_u_absent_minorminornonzeroevaluationmatrixpositivepoint) = S ((S (mdr_r_absent_minorminornonzeroevaluationmatrixpositivepoint)) * mdr_rc_absent_minor)) /\ exists ff_q_mdr_absent_minorminornonzeroevaluationmatrixpositivepointrow_index. mdr_rb_absent_minor = ff_q_mdr_absent_minorminornonzeroevaluationmatrixpositivepointrow_index * S ((S (mdr_r_absent_minorminornonzeroevaluationmatrixpositivepoint)) * mdr_rc_absent_minor) + (mdr_u_absent_minorminornonzeroevaluationmatrixpositivepoint))) /\ ((((exists ff_h_mdr_absent_minorminornonzeroevaluationmatrixpositivepointcolumn_index. ff_h_mdr_absent_minorminornonzeroevaluationmatrixpositivepointcolumn_index + S (mdr_v_absent_minorminornonzeroevaluationmatrixpositivepoint) = S ((S (mdr_s_absent_minorminornonzeroevaluationmatrixpositivepoint)) * mdr_cc_absent_minor)) /\ exists ff_q_mdr_absent_minorminornonzeroevaluationmatrixpositivepointcolumn_index. mdr_cb_absent_minor = ff_q_mdr_absent_minorminornonzeroevaluationmatrixpositivepointcolumn_index * S ((S (mdr_s_absent_minorminornonzeroevaluationmatrixpositivepoint)) * mdr_cc_absent_minor) + (mdr_v_absent_minorminornonzeroevaluationmatrixpositivepoint))) /\ (((exists ff_h_mdr_absent_minorminornonzeroevaluationmatrixpositivepointsource. ff_h_mdr_absent_minorminornonzeroevaluationmatrixpositivepointsource + S (mdr_a_absent_minorminornonzeroevaluationmatrixpositive) = S ((S ((mdr_u_absent_minorminornonzeroevaluationmatrixpositivepoint) * (w) + (mdr_v_absent_minorminornonzeroevaluationmatrixpositivepoint))) * pc)) /\ exists ff_q_mdr_absent_minorminornonzeroevaluationmatrixpositivepointsource. pb = ff_q_mdr_absent_minorminornonzeroevaluationmatrixpositivepointsource * S ((S ((mdr_u_absent_minorminornonzeroevaluationmatrixpositivepoint) * (w) + (mdr_v_absent_minorminornonzeroevaluationmatrixpositivepoint))) * pc) + (mdr_a_absent_minorminornonzeroevaluationmatrixpositive)))))))) /\ (((exists ff_h_mdr_absent_minorminornonzeroevaluationmatrixpositiveoutput. ff_h_mdr_absent_minorminornonzeroevaluationmatrixpositiveoutput + S (mdr_a_absent_minorminornonzeroevaluationmatrixpositive) = S ((S (mdr_i_absent_minorminornonzeroevaluationmatrixpositive)) * mdr_uc_absent_minorminornonzeroevaluation)) /\ exists ff_q_mdr_absent_minorminornonzeroevaluationmatrixpositiveoutput. mdr_ub_absent_minorminornonzeroevaluation = ff_q_mdr_absent_minorminornonzeroevaluationmatrixpositiveoutput * S ((S (mdr_i_absent_minorminornonzeroevaluationmatrixpositive)) * mdr_uc_absent_minorminornonzeroevaluation) + (mdr_a_absent_minorminornonzeroevaluationmatrixpositive)))))) /\ (forall mdr_i_absent_minorminornonzeroevaluationmatrixnegative. (exists mdr_gap_absent_minorminornonzeroevaluationmatrixnegativebound. mdr_gap_absent_minorminornonzeroevaluationmatrixnegativebound + S (mdr_i_absent_minorminornonzeroevaluationmatrixnegative) = ((q) * (q))) -> exists mdr_a_absent_minorminornonzeroevaluationmatrixnegative. (((exists mdr_r_absent_minorminornonzeroevaluationmatrixnegativepoint mdr_s_absent_minorminornonzeroevaluationmatrixnegativepoint mdr_u_absent_minorminornonzeroevaluationmatrixnegativepoint mdr_v_absent_minorminornonzeroevaluationmatrixnegativepoint. ((mdr_i_absent_minorminornonzeroevaluationmatrixnegative = (q) * mdr_r_absent_minorminornonzeroevaluationmatrixnegativepoint + mdr_s_absent_minorminornonzeroevaluationmatrixnegativepoint) /\ ((exists mdr_gap_absent_minorminornonzeroevaluationmatrixnegativepointcolumn. mdr_gap_absent_minorminornonzeroevaluationmatrixnegativepointcolumn + S (mdr_s_absent_minorminornonzeroevaluationmatrixnegativepoint) = (q)) /\ ((((exists ff_h_mdr_absent_minorminornonzeroevaluationmatrixnegativepointrow_index. ff_h_mdr_absent_minorminornonzeroevaluationmatrixnegativepointrow_index + S (mdr_u_absent_minorminornonzeroevaluationmatrixnegativepoint) = S ((S (mdr_r_absent_minorminornonzeroevaluationmatrixnegativepoint)) * mdr_rc_absent_minor)) /\ exists ff_q_mdr_absent_minorminornonzeroevaluationmatrixnegativepointrow_index. mdr_rb_absent_minor = ff_q_mdr_absent_minorminornonzeroevaluationmatrixnegativepointrow_index * S ((S (mdr_r_absent_minorminornonzeroevaluationmatrixnegativepoint)) * mdr_rc_absent_minor) + (mdr_u_absent_minorminornonzeroevaluationmatrixnegativepoint))) /\ ((((exists ff_h_mdr_absent_minorminornonzeroevaluationmatrixnegativepointcolumn_index. ff_h_mdr_absent_minorminornonzeroevaluationmatrixnegativepointcolumn_index + S (mdr_v_absent_minorminornonzeroevaluationmatrixnegativepoint) = S ((S (mdr_s_absent_minorminornonzeroevaluationmatrixnegativepoint)) * mdr_cc_absent_minor)) /\ exists ff_q_mdr_absent_minorminornonzeroevaluationmatrixnegativepointcolumn_index. mdr_cb_absent_minor = ff_q_mdr_absent_minorminornonzeroevaluationmatrixnegativepointcolumn_index * S ((S (mdr_s_absent_minorminornonzeroevaluationmatrixnegativepoint)) * mdr_cc_absent_minor) + (mdr_v_absent_minorminornonzeroevaluationmatrixnegativepoint))) /\ (((exists ff_h_mdr_absent_minorminornonzeroevaluationmatrixnegativepointsource. ff_h_mdr_absent_minorminornonzeroevaluationmatrixnegativepointsource + S (mdr_a_absent_minorminornonzeroevaluationmatrixnegative) = S ((S ((mdr_u_absent_minorminornonzeroevaluationmatrixnegativepoint) * (w) + (mdr_v_absent_minorminornonzeroevaluationmatrixnegativepoint))) * nc)) /\ exists ff_q_mdr_absent_minorminornonzeroevaluationmatrixnegativepointsource. nb = ff_q_mdr_absent_minorminornonzeroevaluationmatrixnegativepointsource * S ((S ((mdr_u_absent_minorminornonzeroevaluationmatrixnegativepoint) * (w) + (mdr_v_absent_minorminornonzeroevaluationmatrixnegativepoint))) * nc) + (mdr_a_absent_minorminornonzeroevaluationmatrixnegative)))))))) /\ (((exists ff_h_mdr_absent_minorminornonzeroevaluationmatrixnegativeoutput. ff_h_mdr_absent_minorminornonzeroevaluationmatrixnegativeoutput + S (mdr_a_absent_minorminornonzeroevaluationmatrixnegative) = S ((S (mdr_i_absent_minorminornonzeroevaluationmatrixnegative)) * mdr_vc_absent_minorminornonzeroevaluation)) /\ exists ff_q_mdr_absent_minorminornonzeroevaluationmatrixnegativeoutput. mdr_vb_absent_minorminornonzeroevaluation = ff_q_mdr_absent_minorminornonzeroevaluationmatrixnegativeoutput * S ((S (mdr_i_absent_minorminornonzeroevaluationmatrixnegative)) * mdr_vc_absent_minorminornonzeroevaluation) + (mdr_a_absent_minorminornonzeroevaluationmatrixnegative)))))))) /\ (exists mdr_b_absent_minorminornonzeroevaluationdeterminant mdr_c_absent_minorminornonzeroevaluationdeterminant mdr_l_absent_minorminornonzeroevaluationdeterminant mdr_i_absent_minorminornonzeroevaluationdeterminant. ((forall mdr_i_absent_minorminornonzeroevaluationdeterminanth. (exists mdr_gap_absent_minorminornonzeroevaluationdeterminanthi. mdr_gap_absent_minorminornonzeroevaluationdeterminanthi + S (mdr_i_absent_minorminornonzeroevaluationdeterminanth) = (mdr_l_absent_minorminornonzeroevaluationdeterminant)) -> exists mdr_d_absent_minorminornonzeroevaluationdeterminanth mdr_pb_absent_minorminornonzeroevaluationdeterminanth mdr_pc_absent_minorminornonzeroevaluationdeterminanth mdr_nb_absent_minorminornonzeroevaluationdeterminanth mdr_nc_absent_minorminornonzeroevaluationdeterminanth mdr_p_absent_minorminornonzeroevaluationdeterminanth mdr_n_absent_minorminornonzeroevaluationdeterminanth. ((exists mdr_z_absent_minorminornonzeroevaluationdeterminanthr. ((exists mdr_a_absent_minorminornonzeroevaluationdeterminanthrc mdr_b_absent_minorminornonzeroevaluationdeterminanthrc mdr_c_absent_minorminornonzeroevaluationdeterminanthrc mdr_e_absent_minorminornonzeroevaluationdeterminanthrc mdr_f_absent_minorminornonzeroevaluationdeterminanthrc. ((mdr_a_absent_minorminornonzeroevaluationdeterminanthrc = ((mdr_d_absent_minorminornonzeroevaluationdeterminanth) + (mdr_pb_absent_minorminornonzeroevaluationdeterminanth)) * S ((mdr_d_absent_minorminornonzeroevaluationdeterminanth) + (mdr_pb_absent_minorminornonzeroevaluationdeterminanth)) + ((mdr_pb_absent_minorminornonzeroevaluationdeterminanth) + (mdr_pb_absent_minorminornonzeroevaluationdeterminanth))) /\ ((mdr_b_absent_minorminornonzeroevaluationdeterminanthrc = ((mdr_pc_absent_minorminornonzeroevaluationdeterminanth) + (mdr_nb_absent_minorminornonzeroevaluationdeterminanth)) * S ((mdr_pc_absent_minorminornonzeroevaluationdeterminanth) + (mdr_nb_absent_minorminornonzeroevaluationdeterminanth)) + ((mdr_nb_absent_minorminornonzeroevaluationdeterminanth) + (mdr_nb_absent_minorminornonzeroevaluationdeterminanth))) /\ ((mdr_c_absent_minorminornonzeroevaluationdeterminanthrc = ((mdr_a_absent_minorminornonzeroevaluationdeterminanthrc) + (mdr_b_absent_minorminornonzeroevaluationdeterminanthrc)) * S ((mdr_a_absent_minorminornonzeroevaluationdeterminanthrc) + (mdr_b_absent_minorminornonzeroevaluationdeterminanthrc)) + ((mdr_b_absent_minorminornonzeroevaluationdeterminanthrc) + (mdr_b_absent_minorminornonzeroevaluationdeterminanthrc))) /\ ((mdr_e_absent_minorminornonzeroevaluationdeterminanthrc = ((mdr_p_absent_minorminornonzeroevaluationdeterminanth) + (mdr_n_absent_minorminornonzeroevaluationdeterminanth)) * S ((mdr_p_absent_minorminornonzeroevaluationdeterminanth) + (mdr_n_absent_minorminornonzeroevaluationdeterminanth)) + ((mdr_n_absent_minorminornonzeroevaluationdeterminanth) + (mdr_n_absent_minorminornonzeroevaluationdeterminanth))) /\ ((mdr_f_absent_minorminornonzeroevaluationdeterminanthrc = ((mdr_nc_absent_minorminornonzeroevaluationdeterminanth) + (mdr_e_absent_minorminornonzeroevaluationdeterminanthrc)) * S ((mdr_nc_absent_minorminornonzeroevaluationdeterminanth) + (mdr_e_absent_minorminornonzeroevaluationdeterminanthrc)) + ((mdr_e_absent_minorminornonzeroevaluationdeterminanthrc) + (mdr_e_absent_minorminornonzeroevaluationdeterminanthrc))) /\ ((mdr_z_absent_minorminornonzeroevaluationdeterminanthr) = ((mdr_c_absent_minorminornonzeroevaluationdeterminanthrc) + (mdr_f_absent_minorminornonzeroevaluationdeterminanthrc)) * S ((mdr_c_absent_minorminornonzeroevaluationdeterminanthrc) + (mdr_f_absent_minorminornonzeroevaluationdeterminanthrc)) + ((mdr_f_absent_minorminornonzeroevaluationdeterminanthrc) + (mdr_f_absent_minorminornonzeroevaluationdeterminanthrc))))))))) /\ (((exists ff_h_mdr_absent_minorminornonzeroevaluationdeterminanthrb. ff_h_mdr_absent_minorminornonzeroevaluationdeterminanthrb + S (mdr_z_absent_minorminornonzeroevaluationdeterminanthr) = S ((S (mdr_i_absent_minorminornonzeroevaluationdeterminanth)) * mdr_c_absent_minorminornonzeroevaluationdeterminant)) /\ exists ff_q_mdr_absent_minorminornonzeroevaluationdeterminanthrb. mdr_b_absent_minorminornonzeroevaluationdeterminant = ff_q_mdr_absent_minorminornonzeroevaluationdeterminanthrb * S ((S (mdr_i_absent_minorminornonzeroevaluationdeterminanth)) * mdr_c_absent_minorminornonzeroevaluationdeterminant) + (mdr_z_absent_minorminornonzeroevaluationdeterminanthr))))) /\ (((((mdr_d_absent_minorminornonzeroevaluationdeterminanth) = 0) /\ (((mdr_p_absent_minorminornonzeroevaluationdeterminanth) = 1) /\ ((mdr_n_absent_minorminornonzeroevaluationdeterminanth) = 0))) \/ exists mdr_q_absent_minorminornonzeroevaluationdeterminanths mdr_eb_absent_minorminornonzeroevaluationdeterminanths mdr_ec_absent_minorminornonzeroevaluationdeterminanths mdr_fb_absent_minorminornonzeroevaluationdeterminanths mdr_fc_absent_minorminornonzeroevaluationdeterminanths. (((mdr_d_absent_minorminornonzeroevaluationdeterminanth) = S (mdr_q_absent_minorminornonzeroevaluationdeterminanths)) /\ ((forall mdr_j_absent_minorminornonzeroevaluationdeterminanthsc. (exists mdr_gap_absent_minorminornonzeroevaluationdeterminanthscj. mdr_gap_absent_minorminornonzeroevaluationdeterminanthscj + S (mdr_j_absent_minorminornonzeroevaluationdeterminanthsc) = (S (mdr_q_absent_minorminornonzeroevaluationdeterminanths))) -> exists mdr_i_absent_minorminornonzeroevaluationdeterminanthsc mdr_up_absent_minorminornonzeroevaluationdeterminanthsc mdr_us_absent_minorminornonzeroevaluationdeterminanthsc mdr_un_absent_minorminornonzeroevaluationdeterminanthsc mdr_ut_absent_minorminornonzeroevaluationdeterminanthsc mdr_p_absent_minorminornonzeroevaluationdeterminanthsc mdr_n_absent_minorminornonzeroevaluationdeterminanthsc. ((exists mdr_gap_absent_minorminornonzeroevaluationdeterminanthsci. mdr_gap_absent_minorminornonzeroevaluationdeterminanthsci + S (mdr_i_absent_minorminornonzeroevaluationdeterminanthsc) = (mdr_i_absent_minorminornonzeroevaluationdeterminanth)) /\ ((exists mdr_z_absent_minorminornonzeroevaluationdeterminanthscr. ((exists mdr_a_absent_minorminornonzeroevaluationdeterminanthscrc mdr_b_absent_minorminornonzeroevaluationdeterminanthscrc mdr_c_absent_minorminornonzeroevaluationdeterminanthscrc mdr_e_absent_minorminornonzeroevaluationdeterminanthscrc mdr_f_absent_minorminornonzeroevaluationdeterminanthscrc. ((mdr_a_absent_minorminornonzeroevaluationdeterminanthscrc = ((mdr_q_absent_minorminornonzeroevaluationdeterminanths) + (mdr_up_absent_minorminornonzeroevaluationdeterminanthsc)) * S ((mdr_q_absent_minorminornonzeroevaluationdeterminanths) + (mdr_up_absent_minorminornonzeroevaluationdeterminanthsc)) + ((mdr_up_absent_minorminornonzeroevaluationdeterminanthsc) + (mdr_up_absent_minorminornonzeroevaluationdeterminanthsc))) /\ ((mdr_b_absent_minorminornonzeroevaluationdeterminanthscrc = ((mdr_us_absent_minorminornonzeroevaluationdeterminanthsc) + (mdr_un_absent_minorminornonzeroevaluationdeterminanthsc)) * S ((mdr_us_absent_minorminornonzeroevaluationdeterminanthsc) + (mdr_un_absent_minorminornonzeroevaluationdeterminanthsc)) + ((mdr_un_absent_minorminornonzeroevaluationdeterminanthsc) + (mdr_un_absent_minorminornonzeroevaluationdeterminanthsc))) /\ ((mdr_c_absent_minorminornonzeroevaluationdeterminanthscrc = ((mdr_a_absent_minorminornonzeroevaluationdeterminanthscrc) + (mdr_b_absent_minorminornonzeroevaluationdeterminanthscrc)) * S ((mdr_a_absent_minorminornonzeroevaluationdeterminanthscrc) + (mdr_b_absent_minorminornonzeroevaluationdeterminanthscrc)) + ((mdr_b_absent_minorminornonzeroevaluationdeterminanthscrc) + (mdr_b_absent_minorminornonzeroevaluationdeterminanthscrc))) /\ ((mdr_e_absent_minorminornonzeroevaluationdeterminanthscrc = ((mdr_p_absent_minorminornonzeroevaluationdeterminanthsc) + (mdr_n_absent_minorminornonzeroevaluationdeterminanthsc)) * S ((mdr_p_absent_minorminornonzeroevaluationdeterminanthsc) + (mdr_n_absent_minorminornonzeroevaluationdeterminanthsc)) + ((mdr_n_absent_minorminornonzeroevaluationdeterminanthsc) + (mdr_n_absent_minorminornonzeroevaluationdeterminanthsc))) /\ ((mdr_f_absent_minorminornonzeroevaluationdeterminanthscrc = ((mdr_ut_absent_minorminornonzeroevaluationdeterminanthsc) + (mdr_e_absent_minorminornonzeroevaluationdeterminanthscrc)) * S ((mdr_ut_absent_minorminornonzeroevaluationdeterminanthsc) + (mdr_e_absent_minorminornonzeroevaluationdeterminanthscrc)) + ((mdr_e_absent_minorminornonzeroevaluationdeterminanthscrc) + (mdr_e_absent_minorminornonzeroevaluationdeterminanthscrc))) /\ ((mdr_z_absent_minorminornonzeroevaluationdeterminanthscr) = ((mdr_c_absent_minorminornonzeroevaluationdeterminanthscrc) + (mdr_f_absent_minorminornonzeroevaluationdeterminanthscrc)) * S ((mdr_c_absent_minorminornonzeroevaluationdeterminanthscrc) + (mdr_f_absent_minorminornonzeroevaluationdeterminanthscrc)) + ((mdr_f_absent_minorminornonzeroevaluationdeterminanthscrc) + (mdr_f_absent_minorminornonzeroevaluationdeterminanthscrc))))))))) /\ (((exists ff_h_mdr_absent_minorminornonzeroevaluationdeterminanthscrb. ff_h_mdr_absent_minorminornonzeroevaluationdeterminanthscrb + S (mdr_z_absent_minorminornonzeroevaluationdeterminanthscr) = S ((S (mdr_i_absent_minorminornonzeroevaluationdeterminanthsc)) * mdr_c_absent_minorminornonzeroevaluationdeterminant)) /\ exists ff_q_mdr_absent_minorminornonzeroevaluationdeterminanthscrb. mdr_b_absent_minorminornonzeroevaluationdeterminant = ff_q_mdr_absent_minorminornonzeroevaluationdeterminanthscrb * S ((S (mdr_i_absent_minorminornonzeroevaluationdeterminanthsc)) * mdr_c_absent_minorminornonzeroevaluationdeterminant) + (mdr_z_absent_minorminornonzeroevaluationdeterminanthscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_absent_minorminornonzeroevaluationdeterminanthscm_positive. (exists ff_gap_mdm_lt_mdr_absent_minorminornonzeroevaluationdeterminanthscm_positive_index_bound. ff_gap_mdm_lt_mdr_absent_minorminornonzeroevaluationdeterminanthscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_absent_minorminornonzeroevaluationdeterminanthscm_positive) = ((mdr_q_absent_minorminornonzeroevaluationdeterminanths) * (mdr_q_absent_minorminornonzeroevaluationdeterminanths))) -> exists ff_row_mdm_prefix_mdr_absent_minorminornonzeroevaluationdeterminanthscm_positive ff_column_mdm_prefix_mdr_absent_minorminornonzeroevaluationdeterminanthscm_positive ff_value_mdm_prefix_mdr_absent_minorminornonzeroevaluationdeterminanthscm_positive. (ff_index_mdm_prefix_mdr_absent_minorminornonzeroevaluationdeterminanthscm_positive = (mdr_q_absent_minorminornonzeroevaluationdeterminanths) * ff_row_mdm_prefix_mdr_absent_minorminornonzeroevaluationdeterminanthscm_positive + ff_column_mdm_prefix_mdr_absent_minorminornonzeroevaluationdeterminanthscm_positive /\ ((exists ff_gap_mdm_lt_mdr_absent_minorminornonzeroevaluationdeterminanthscm_positive_column_bound. ff_gap_mdm_lt_mdr_absent_minorminornonzeroevaluationdeterminanthscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_absent_minorminornonzeroevaluationdeterminanthscm_positive) = (mdr_q_absent_minorminornonzeroevaluationdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_absent_minorminornonzeroevaluationdeterminanthscm_positive_cell ff_column_mdm_cell_mdr_absent_minorminornonzeroevaluationdeterminanthscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_absent_minorminornonzeroevaluationdeterminanthscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_absent_minorminornonzeroevaluationdeterminanthscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_absent_minorminornonzeroevaluationdeterminanthscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_absent_minorminornonzeroevaluationdeterminanthscm_positive_cell = ff_row_mdm_prefix_mdr_absent_minorminornonzeroevaluationdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_absent_minorminornonzeroevaluationdeterminanthscm_positive_cell_row_after. ff_gap_mdm_le_mdr_absent_minorminornonzeroevaluationdeterminanthscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_absent_minorminornonzeroevaluationdeterminanthscm_positive)) /\ ff_row_mdm_cell_mdr_absent_minorminornonzeroevaluationdeterminanthscm_positive_cell = S ff_row_mdm_prefix_mdr_absent_minorminornonzeroevaluationdeterminanthscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_absent_minorminornonzeroevaluationdeterminanthscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_absent_minorminornonzeroevaluationdeterminanthscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_absent_minorminornonzeroevaluationdeterminanthscm_positive) = (mdr_j_absent_minorminornonzeroevaluationdeterminanthsc)) /\ ff_column_mdm_cell_mdr_absent_minorminornonzeroevaluationdeterminanthscm_positive_cell = ff_column_mdm_prefix_mdr_absent_minorminornonzeroevaluationdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_absent_minorminornonzeroevaluationdeterminanthscm_positive_cell_column_after. ff_gap_mdm_le_mdr_absent_minorminornonzeroevaluationdeterminanthscm_positive_cell_column_after + (mdr_j_absent_minorminornonzeroevaluationdeterminanthsc) = (ff_column_mdm_prefix_mdr_absent_minorminornonzeroevaluationdeterminanthscm_positive)) /\ ff_column_mdm_cell_mdr_absent_minorminornonzeroevaluationdeterminanthscm_positive_cell = S ff_column_mdm_prefix_mdr_absent_minorminornonzeroevaluationdeterminanthscm_positive))) /\ (((exists ff_h_mdm_mdr_absent_minorminornonzeroevaluationdeterminanthscm_positive_cell_source. ff_h_mdm_mdr_absent_minorminornonzeroevaluationdeterminanthscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_absent_minorminornonzeroevaluationdeterminanthscm_positive) = S ((S ((ff_row_mdm_cell_mdr_absent_minorminornonzeroevaluationdeterminanthscm_positive_cell) * (S (mdr_q_absent_minorminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_absent_minorminornonzeroevaluationdeterminanthscm_positive_cell))) * mdr_pc_absent_minorminornonzeroevaluationdeterminanth)) /\ exists ff_q_mdm_mdr_absent_minorminornonzeroevaluationdeterminanthscm_positive_cell_source. mdr_pb_absent_minorminornonzeroevaluationdeterminanth = ff_q_mdm_mdr_absent_minorminornonzeroevaluationdeterminanthscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_absent_minorminornonzeroevaluationdeterminanthscm_positive_cell) * (S (mdr_q_absent_minorminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_absent_minorminornonzeroevaluationdeterminanthscm_positive_cell))) * mdr_pc_absent_minorminornonzeroevaluationdeterminanth) + (ff_value_mdm_prefix_mdr_absent_minorminornonzeroevaluationdeterminanthscm_positive)))))) /\ (((exists ff_h_mdm_mdr_absent_minorminornonzeroevaluationdeterminanthscm_positive_target. ff_h_mdm_mdr_absent_minorminornonzeroevaluationdeterminanthscm_positive_target + S (ff_value_mdm_prefix_mdr_absent_minorminornonzeroevaluationdeterminanthscm_positive) = S ((S (ff_index_mdm_prefix_mdr_absent_minorminornonzeroevaluationdeterminanthscm_positive)) * mdr_us_absent_minorminornonzeroevaluationdeterminanthsc)) /\ exists ff_q_mdm_mdr_absent_minorminornonzeroevaluationdeterminanthscm_positive_target. mdr_up_absent_minorminornonzeroevaluationdeterminanthsc = ff_q_mdm_mdr_absent_minorminornonzeroevaluationdeterminanthscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_absent_minorminornonzeroevaluationdeterminanthscm_positive)) * mdr_us_absent_minorminornonzeroevaluationdeterminanthsc) + (ff_value_mdm_prefix_mdr_absent_minorminornonzeroevaluationdeterminanthscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_absent_minorminornonzeroevaluationdeterminanthscm_negative. (exists ff_gap_mdm_lt_mdr_absent_minorminornonzeroevaluationdeterminanthscm_negative_index_bound. ff_gap_mdm_lt_mdr_absent_minorminornonzeroevaluationdeterminanthscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_absent_minorminornonzeroevaluationdeterminanthscm_negative) = ((mdr_q_absent_minorminornonzeroevaluationdeterminanths) * (mdr_q_absent_minorminornonzeroevaluationdeterminanths))) -> exists ff_row_mdm_prefix_mdr_absent_minorminornonzeroevaluationdeterminanthscm_negative ff_column_mdm_prefix_mdr_absent_minorminornonzeroevaluationdeterminanthscm_negative ff_value_mdm_prefix_mdr_absent_minorminornonzeroevaluationdeterminanthscm_negative. (ff_index_mdm_prefix_mdr_absent_minorminornonzeroevaluationdeterminanthscm_negative = (mdr_q_absent_minorminornonzeroevaluationdeterminanths) * ff_row_mdm_prefix_mdr_absent_minorminornonzeroevaluationdeterminanthscm_negative + ff_column_mdm_prefix_mdr_absent_minorminornonzeroevaluationdeterminanthscm_negative /\ ((exists ff_gap_mdm_lt_mdr_absent_minorminornonzeroevaluationdeterminanthscm_negative_column_bound. ff_gap_mdm_lt_mdr_absent_minorminornonzeroevaluationdeterminanthscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_absent_minorminornonzeroevaluationdeterminanthscm_negative) = (mdr_q_absent_minorminornonzeroevaluationdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_absent_minorminornonzeroevaluationdeterminanthscm_negative_cell ff_column_mdm_cell_mdr_absent_minorminornonzeroevaluationdeterminanthscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_absent_minorminornonzeroevaluationdeterminanthscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_absent_minorminornonzeroevaluationdeterminanthscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_absent_minorminornonzeroevaluationdeterminanthscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_absent_minorminornonzeroevaluationdeterminanthscm_negative_cell = ff_row_mdm_prefix_mdr_absent_minorminornonzeroevaluationdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_absent_minorminornonzeroevaluationdeterminanthscm_negative_cell_row_after. ff_gap_mdm_le_mdr_absent_minorminornonzeroevaluationdeterminanthscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_absent_minorminornonzeroevaluationdeterminanthscm_negative)) /\ ff_row_mdm_cell_mdr_absent_minorminornonzeroevaluationdeterminanthscm_negative_cell = S ff_row_mdm_prefix_mdr_absent_minorminornonzeroevaluationdeterminanthscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_absent_minorminornonzeroevaluationdeterminanthscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_absent_minorminornonzeroevaluationdeterminanthscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_absent_minorminornonzeroevaluationdeterminanthscm_negative) = (mdr_j_absent_minorminornonzeroevaluationdeterminanthsc)) /\ ff_column_mdm_cell_mdr_absent_minorminornonzeroevaluationdeterminanthscm_negative_cell = ff_column_mdm_prefix_mdr_absent_minorminornonzeroevaluationdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_absent_minorminornonzeroevaluationdeterminanthscm_negative_cell_column_after. ff_gap_mdm_le_mdr_absent_minorminornonzeroevaluationdeterminanthscm_negative_cell_column_after + (mdr_j_absent_minorminornonzeroevaluationdeterminanthsc) = (ff_column_mdm_prefix_mdr_absent_minorminornonzeroevaluationdeterminanthscm_negative)) /\ ff_column_mdm_cell_mdr_absent_minorminornonzeroevaluationdeterminanthscm_negative_cell = S ff_column_mdm_prefix_mdr_absent_minorminornonzeroevaluationdeterminanthscm_negative))) /\ (((exists ff_h_mdm_mdr_absent_minorminornonzeroevaluationdeterminanthscm_negative_cell_source. ff_h_mdm_mdr_absent_minorminornonzeroevaluationdeterminanthscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_absent_minorminornonzeroevaluationdeterminanthscm_negative) = S ((S ((ff_row_mdm_cell_mdr_absent_minorminornonzeroevaluationdeterminanthscm_negative_cell) * (S (mdr_q_absent_minorminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_absent_minorminornonzeroevaluationdeterminanthscm_negative_cell))) * mdr_nc_absent_minorminornonzeroevaluationdeterminanth)) /\ exists ff_q_mdm_mdr_absent_minorminornonzeroevaluationdeterminanthscm_negative_cell_source. mdr_nb_absent_minorminornonzeroevaluationdeterminanth = ff_q_mdm_mdr_absent_minorminornonzeroevaluationdeterminanthscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_absent_minorminornonzeroevaluationdeterminanthscm_negative_cell) * (S (mdr_q_absent_minorminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_absent_minorminornonzeroevaluationdeterminanthscm_negative_cell))) * mdr_nc_absent_minorminornonzeroevaluationdeterminanth) + (ff_value_mdm_prefix_mdr_absent_minorminornonzeroevaluationdeterminanthscm_negative)))))) /\ (((exists ff_h_mdm_mdr_absent_minorminornonzeroevaluationdeterminanthscm_negative_target. ff_h_mdm_mdr_absent_minorminornonzeroevaluationdeterminanthscm_negative_target + S (ff_value_mdm_prefix_mdr_absent_minorminornonzeroevaluationdeterminanthscm_negative) = S ((S (ff_index_mdm_prefix_mdr_absent_minorminornonzeroevaluationdeterminanthscm_negative)) * mdr_ut_absent_minorminornonzeroevaluationdeterminanthsc)) /\ exists ff_q_mdm_mdr_absent_minorminornonzeroevaluationdeterminanthscm_negative_target. mdr_un_absent_minorminornonzeroevaluationdeterminanthsc = ff_q_mdm_mdr_absent_minorminornonzeroevaluationdeterminanthscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_absent_minorminornonzeroevaluationdeterminanthscm_negative)) * mdr_ut_absent_minorminornonzeroevaluationdeterminanthsc) + (ff_value_mdm_prefix_mdr_absent_minorminornonzeroevaluationdeterminanthscm_negative))))))))) /\ ((((exists ff_h_mdr_absent_minorminornonzeroevaluationdeterminanthscp. ff_h_mdr_absent_minorminornonzeroevaluationdeterminanthscp + S (mdr_p_absent_minorminornonzeroevaluationdeterminanthsc) = S ((S (mdr_j_absent_minorminornonzeroevaluationdeterminanthsc)) * mdr_ec_absent_minorminornonzeroevaluationdeterminanths)) /\ exists ff_q_mdr_absent_minorminornonzeroevaluationdeterminanthscp. mdr_eb_absent_minorminornonzeroevaluationdeterminanths = ff_q_mdr_absent_minorminornonzeroevaluationdeterminanthscp * S ((S (mdr_j_absent_minorminornonzeroevaluationdeterminanthsc)) * mdr_ec_absent_minorminornonzeroevaluationdeterminanths) + (mdr_p_absent_minorminornonzeroevaluationdeterminanthsc))) /\ (((exists ff_h_mdr_absent_minorminornonzeroevaluationdeterminanthscn. ff_h_mdr_absent_minorminornonzeroevaluationdeterminanthscn + S (mdr_n_absent_minorminornonzeroevaluationdeterminanthsc) = S ((S (mdr_j_absent_minorminornonzeroevaluationdeterminanthsc)) * mdr_fc_absent_minorminornonzeroevaluationdeterminanths)) /\ exists ff_q_mdr_absent_minorminornonzeroevaluationdeterminanthscn. mdr_fb_absent_minorminornonzeroevaluationdeterminanths = ff_q_mdr_absent_minorminornonzeroevaluationdeterminanthscn * S ((S (mdr_j_absent_minorminornonzeroevaluationdeterminanthsc)) * mdr_fc_absent_minorminornonzeroevaluationdeterminanths) + (mdr_n_absent_minorminornonzeroevaluationdeterminanthsc)))))))) /\ (exists ff_ub_mce_fold_mdr_absent_minorminornonzeroevaluationdeterminanthsf ff_uc_mce_fold_mdr_absent_minorminornonzeroevaluationdeterminanthsf ff_vb_mce_fold_mdr_absent_minorminornonzeroevaluationdeterminanthsf ff_vc_mce_fold_mdr_absent_minorminornonzeroevaluationdeterminanthsf. ((forall ff_index_mce_alternating_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix. (exists ff_gap_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix_index. ff_gap_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix_index + S (ff_index_mce_alternating_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix) = (S (mdr_q_absent_minorminornonzeroevaluationdeterminanths))) -> exists ff_ap_mce_alternating_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix ff_an_mce_alternating_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix ff_bp_mce_alternating_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix ff_bn_mce_alternating_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix ff_p_mce_alternating_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix ff_n_mce_alternating_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix. ((((exists ff_h_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix_ap. ff_h_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix_ap + S (ff_ap_mce_alternating_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix)) * mdr_pc_absent_minorminornonzeroevaluationdeterminanth)) /\ exists ff_q_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix_ap. mdr_pb_absent_minorminornonzeroevaluationdeterminanth = ff_q_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix)) * mdr_pc_absent_minorminornonzeroevaluationdeterminanth) + (ff_ap_mce_alternating_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix_an. ff_h_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix_an + S (ff_an_mce_alternating_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix)) * mdr_nc_absent_minorminornonzeroevaluationdeterminanth)) /\ exists ff_q_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix_an. mdr_nb_absent_minorminornonzeroevaluationdeterminanth = ff_q_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix)) * mdr_nc_absent_minorminornonzeroevaluationdeterminanth) + (ff_an_mce_alternating_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix_bp. ff_h_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix_bp + S (ff_bp_mce_alternating_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix)) * mdr_ec_absent_minorminornonzeroevaluationdeterminanths)) /\ exists ff_q_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix_bp. mdr_eb_absent_minorminornonzeroevaluationdeterminanths = ff_q_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix)) * mdr_ec_absent_minorminornonzeroevaluationdeterminanths) + (ff_bp_mce_alternating_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix_bn. ff_h_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix_bn + S (ff_bn_mce_alternating_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix)) * mdr_fc_absent_minorminornonzeroevaluationdeterminanths)) /\ exists ff_q_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix_bn. mdr_fb_absent_minorminornonzeroevaluationdeterminanths = ff_q_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix)) * mdr_fc_absent_minorminornonzeroevaluationdeterminanths) + (ff_bn_mce_alternating_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix_positive. ff_h_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix_positive + S (ff_p_mce_alternating_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_absent_minorminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix_positive. ff_ub_mce_fold_mdr_absent_minorminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_absent_minorminornonzeroevaluationdeterminanthsf) + (ff_p_mce_alternating_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix_negative. ff_h_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix_negative + S (ff_n_mce_alternating_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_absent_minorminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix_negative. ff_vb_mce_fold_mdr_absent_minorminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_absent_minorminornonzeroevaluationdeterminanthsf) + (ff_n_mce_alternating_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix))) /\ (((exists ff_even_mce_term_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix = 2 * ff_even_mce_term_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix_term) /\ (ff_p_mce_alternating_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix = 2 * ff_odd_mce_term_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_absent_minorminornonzeroevaluationdeterminanthsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_positive ff_v_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_positive. ((((exists ff_h_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_positive_start. ff_h_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_positive_start. ff_u_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_positive_start * S ((S (0)) * ff_v_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_positive_terminal. ff_h_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_positive_terminal + S (mdr_p_absent_minorminornonzeroevaluationdeterminanth) = S ((S ((S (mdr_q_absent_minorminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_positive_terminal. ff_u_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_positive_terminal * S ((S ((S (mdr_q_absent_minorminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_positive) + (mdr_p_absent_minorminornonzeroevaluationdeterminanth))) /\ forall ff_i_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_positive. (exists ff_lt_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_positive_bound. ff_lt_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_positive_bound + S ff_i_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_positive = (S (mdr_q_absent_minorminornonzeroevaluationdeterminanths))) -> exists ff_a_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_positive ff_r_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_positive ff_s_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_positive. ((((exists ff_h_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_positive_summand. ff_h_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_positive_summand + S (ff_a_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_absent_minorminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_positive_summand. ff_ub_mce_fold_mdr_absent_minorminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_positive_summand * S ((S (ff_i_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_absent_minorminornonzeroevaluationdeterminanthsf) + (ff_a_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_positive_partial. ff_h_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_positive_partial + S (ff_r_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_positive_partial. ff_u_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_positive_partial * S ((S (ff_i_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_positive) + (ff_r_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_positive_successor. ff_h_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_positive_successor + S (ff_s_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_positive) = S ((S (S ff_i_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_positive_successor. ff_u_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_positive_successor * S ((S (S ff_i_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_positive) + (ff_s_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_positive))) /\ ff_s_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_positive = ff_r_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_positive + ff_a_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_positive)))))) /\ (exists ff_u_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_negative ff_v_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_negative. ((((exists ff_h_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_negative_start. ff_h_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_negative_start. ff_u_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_negative_start * S ((S (0)) * ff_v_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_negative_terminal. ff_h_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_negative_terminal + S (mdr_n_absent_minorminornonzeroevaluationdeterminanth) = S ((S ((S (mdr_q_absent_minorminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_negative_terminal. ff_u_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_negative_terminal * S ((S ((S (mdr_q_absent_minorminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_negative) + (mdr_n_absent_minorminornonzeroevaluationdeterminanth))) /\ forall ff_i_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_negative. (exists ff_lt_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_negative_bound. ff_lt_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_negative_bound + S ff_i_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_negative = (S (mdr_q_absent_minorminornonzeroevaluationdeterminanths))) -> exists ff_a_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_negative ff_r_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_negative ff_s_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_negative. ((((exists ff_h_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_negative_summand. ff_h_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_negative_summand + S (ff_a_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_absent_minorminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_negative_summand. ff_vb_mce_fold_mdr_absent_minorminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_negative_summand * S ((S (ff_i_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_absent_minorminornonzeroevaluationdeterminanthsf) + (ff_a_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_negative_partial. ff_h_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_negative_partial + S (ff_r_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_negative_partial. ff_u_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_negative_partial * S ((S (ff_i_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_negative) + (ff_r_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_negative_successor. ff_h_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_negative_successor + S (ff_s_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_negative) = S ((S (S ff_i_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_negative_successor. ff_u_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_negative_successor * S ((S (S ff_i_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_negative) + (ff_s_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_negative))) /\ ff_s_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_negative = ff_r_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_negative + ff_a_mce_mdr_absent_minorminornonzeroevaluationdeterminanthsf_negative))))))))))))))) /\ ((exists mdr_gap_absent_minorminornonzeroevaluationdeterminanti. mdr_gap_absent_minorminornonzeroevaluationdeterminanti + S (mdr_i_absent_minorminornonzeroevaluationdeterminant) = (mdr_l_absent_minorminornonzeroevaluationdeterminant)) /\ (exists mdr_z_absent_minorminornonzeroevaluationdeterminantr. ((exists mdr_a_absent_minorminornonzeroevaluationdeterminantrc mdr_b_absent_minorminornonzeroevaluationdeterminantrc mdr_c_absent_minorminornonzeroevaluationdeterminantrc mdr_e_absent_minorminornonzeroevaluationdeterminantrc mdr_f_absent_minorminornonzeroevaluationdeterminantrc. ((mdr_a_absent_minorminornonzeroevaluationdeterminantrc = ((q) + (mdr_ub_absent_minorminornonzeroevaluation)) * S ((q) + (mdr_ub_absent_minorminornonzeroevaluation)) + ((mdr_ub_absent_minorminornonzeroevaluation) + (mdr_ub_absent_minorminornonzeroevaluation))) /\ ((mdr_b_absent_minorminornonzeroevaluationdeterminantrc = ((mdr_uc_absent_minorminornonzeroevaluation) + (mdr_vb_absent_minorminornonzeroevaluation)) * S ((mdr_uc_absent_minorminornonzeroevaluation) + (mdr_vb_absent_minorminornonzeroevaluation)) + ((mdr_vb_absent_minorminornonzeroevaluation) + (mdr_vb_absent_minorminornonzeroevaluation))) /\ ((mdr_c_absent_minorminornonzeroevaluationdeterminantrc = ((mdr_a_absent_minorminornonzeroevaluationdeterminantrc) + (mdr_b_absent_minorminornonzeroevaluationdeterminantrc)) * S ((mdr_a_absent_minorminornonzeroevaluationdeterminantrc) + (mdr_b_absent_minorminornonzeroevaluationdeterminantrc)) + ((mdr_b_absent_minorminornonzeroevaluationdeterminantrc) + (mdr_b_absent_minorminornonzeroevaluationdeterminantrc))) /\ ((mdr_e_absent_minorminornonzeroevaluationdeterminantrc = ((mdr_p_absent_minorminornonzero) + (mdr_n_absent_minorminornonzero)) * S ((mdr_p_absent_minorminornonzero) + (mdr_n_absent_minorminornonzero)) + ((mdr_n_absent_minorminornonzero) + (mdr_n_absent_minorminornonzero))) /\ ((mdr_f_absent_minorminornonzeroevaluationdeterminantrc = ((mdr_vc_absent_minorminornonzeroevaluation) + (mdr_e_absent_minorminornonzeroevaluationdeterminantrc)) * S ((mdr_vc_absent_minorminornonzeroevaluation) + (mdr_e_absent_minorminornonzeroevaluationdeterminantrc)) + ((mdr_e_absent_minorminornonzeroevaluationdeterminantrc) + (mdr_e_absent_minorminornonzeroevaluationdeterminantrc))) /\ ((mdr_z_absent_minorminornonzeroevaluationdeterminantr) = ((mdr_c_absent_minorminornonzeroevaluationdeterminantrc) + (mdr_f_absent_minorminornonzeroevaluationdeterminantrc)) * S ((mdr_c_absent_minorminornonzeroevaluationdeterminantrc) + (mdr_f_absent_minorminornonzeroevaluationdeterminantrc)) + ((mdr_f_absent_minorminornonzeroevaluationdeterminantrc) + (mdr_f_absent_minorminornonzeroevaluationdeterminantrc))))))))) /\ (((exists ff_h_mdr_absent_minorminornonzeroevaluationdeterminantrb. ff_h_mdr_absent_minorminornonzeroevaluationdeterminantrb + S (mdr_z_absent_minorminornonzeroevaluationdeterminantr) = S ((S (mdr_i_absent_minorminornonzeroevaluationdeterminant)) * mdr_c_absent_minorminornonzeroevaluationdeterminant)) /\ exists ff_q_mdr_absent_minorminornonzeroevaluationdeterminantrb. mdr_b_absent_minorminornonzeroevaluationdeterminant = ff_q_mdr_absent_minorminornonzeroevaluationdeterminantrb * S ((S (mdr_i_absent_minorminornonzeroevaluationdeterminant)) * mdr_c_absent_minorminornonzeroevaluationdeterminant) + (mdr_z_absent_minorminornonzeroevaluationdeterminantr)))))))))) /\ (~(mdr_p_absent_minorminornonzero = mdr_n_absent_minorminornonzero)))))))) -> (forall mdr_rb_all_zero mdr_rc_all_zero mdr_cb_all_zero mdr_cc_all_zero mdr_p_all_zero mdr_n_all_zero. (((forall fom_index_mrf_all_zerorowsbound. (exists fom_gap_mrf_all_zerorowsbound_index_bound. fom_gap_mrf_all_zerorowsbound_index_bound + S (fom_index_mrf_all_zerorowsbound) = q) -> exists fom_value_mrf_all_zerorowsbound. ((((exists fom_beta_height_mrf_all_zerorowsbound_entry. fom_beta_height_mrf_all_zerorowsbound_entry + S (fom_value_mrf_all_zerorowsbound) = S ((S (fom_index_mrf_all_zerorowsbound)) * mdr_rc_all_zero)) /\ exists fom_beta_quotient_mrf_all_zerorowsbound_entry. mdr_rb_all_zero = fom_beta_quotient_mrf_all_zerorowsbound_entry * S ((S (fom_index_mrf_all_zerorowsbound)) * mdr_rc_all_zero) + (fom_value_mrf_all_zerorowsbound))) /\ (exists fom_gap_mrf_all_zerorowsbound_value_bound. fom_gap_mrf_all_zerorowsbound_value_bound + S (fom_value_mrf_all_zerorowsbound) = r))) /\ (forall mdr_i_all_zerorowsdistinct mdr_j_all_zerorowsdistinct mdr_a_all_zerorowsdistinct. (exists mdr_gap_all_zerorowsdistincti. mdr_gap_all_zerorowsdistincti + S (mdr_i_all_zerorowsdistinct) = (q)) -> (exists mdr_gap_all_zerorowsdistinctj. mdr_gap_all_zerorowsdistinctj + S (mdr_j_all_zerorowsdistinct) = (q)) -> (((exists ff_h_mdr_all_zerorowsdistinctfirst. ff_h_mdr_all_zerorowsdistinctfirst + S (mdr_a_all_zerorowsdistinct) = S ((S (mdr_i_all_zerorowsdistinct)) * mdr_rc_all_zero)) /\ exists ff_q_mdr_all_zerorowsdistinctfirst. mdr_rb_all_zero = ff_q_mdr_all_zerorowsdistinctfirst * S ((S (mdr_i_all_zerorowsdistinct)) * mdr_rc_all_zero) + (mdr_a_all_zerorowsdistinct))) -> (((exists ff_h_mdr_all_zerorowsdistinctsecond. ff_h_mdr_all_zerorowsdistinctsecond + S (mdr_a_all_zerorowsdistinct) = S ((S (mdr_j_all_zerorowsdistinct)) * mdr_rc_all_zero)) /\ exists ff_q_mdr_all_zerorowsdistinctsecond. mdr_rb_all_zero = ff_q_mdr_all_zerorowsdistinctsecond * S ((S (mdr_j_all_zerorowsdistinct)) * mdr_rc_all_zero) + (mdr_a_all_zerorowsdistinct))) -> mdr_i_all_zerorowsdistinct = mdr_j_all_zerorowsdistinct))) -> (((forall fom_index_mrf_all_zerocolumnsbound. (exists fom_gap_mrf_all_zerocolumnsbound_index_bound. fom_gap_mrf_all_zerocolumnsbound_index_bound + S (fom_index_mrf_all_zerocolumnsbound) = q) -> exists fom_value_mrf_all_zerocolumnsbound. ((((exists fom_beta_height_mrf_all_zerocolumnsbound_entry. fom_beta_height_mrf_all_zerocolumnsbound_entry + S (fom_value_mrf_all_zerocolumnsbound) = S ((S (fom_index_mrf_all_zerocolumnsbound)) * mdr_cc_all_zero)) /\ exists fom_beta_quotient_mrf_all_zerocolumnsbound_entry. mdr_cb_all_zero = fom_beta_quotient_mrf_all_zerocolumnsbound_entry * S ((S (fom_index_mrf_all_zerocolumnsbound)) * mdr_cc_all_zero) + (fom_value_mrf_all_zerocolumnsbound))) /\ (exists fom_gap_mrf_all_zerocolumnsbound_value_bound. fom_gap_mrf_all_zerocolumnsbound_value_bound + S (fom_value_mrf_all_zerocolumnsbound) = w))) /\ (forall mdr_i_all_zerocolumnsdistinct mdr_j_all_zerocolumnsdistinct mdr_a_all_zerocolumnsdistinct. (exists mdr_gap_all_zerocolumnsdistincti. mdr_gap_all_zerocolumnsdistincti + S (mdr_i_all_zerocolumnsdistinct) = (q)) -> (exists mdr_gap_all_zerocolumnsdistinctj. mdr_gap_all_zerocolumnsdistinctj + S (mdr_j_all_zerocolumnsdistinct) = (q)) -> (((exists ff_h_mdr_all_zerocolumnsdistinctfirst. ff_h_mdr_all_zerocolumnsdistinctfirst + S (mdr_a_all_zerocolumnsdistinct) = S ((S (mdr_i_all_zerocolumnsdistinct)) * mdr_cc_all_zero)) /\ exists ff_q_mdr_all_zerocolumnsdistinctfirst. mdr_cb_all_zero = ff_q_mdr_all_zerocolumnsdistinctfirst * S ((S (mdr_i_all_zerocolumnsdistinct)) * mdr_cc_all_zero) + (mdr_a_all_zerocolumnsdistinct))) -> (((exists ff_h_mdr_all_zerocolumnsdistinctsecond. ff_h_mdr_all_zerocolumnsdistinctsecond + S (mdr_a_all_zerocolumnsdistinct) = S ((S (mdr_j_all_zerocolumnsdistinct)) * mdr_cc_all_zero)) /\ exists ff_q_mdr_all_zerocolumnsdistinctsecond. mdr_cb_all_zero = ff_q_mdr_all_zerocolumnsdistinctsecond * S ((S (mdr_j_all_zerocolumnsdistinct)) * mdr_cc_all_zero) + (mdr_a_all_zerocolumnsdistinct))) -> mdr_i_all_zerocolumnsdistinct = mdr_j_all_zerocolumnsdistinct))) -> (exists mdr_ub_all_zeroevaluation mdr_uc_all_zeroevaluation mdr_vb_all_zeroevaluation mdr_vc_all_zeroevaluation. ((((forall mdr_i_all_zeroevaluationmatrixpositive. (exists mdr_gap_all_zeroevaluationmatrixpositivebound. mdr_gap_all_zeroevaluationmatrixpositivebound + S (mdr_i_all_zeroevaluationmatrixpositive) = ((q) * (q))) -> exists mdr_a_all_zeroevaluationmatrixpositive. (((exists mdr_r_all_zeroevaluationmatrixpositivepoint mdr_s_all_zeroevaluationmatrixpositivepoint mdr_u_all_zeroevaluationmatrixpositivepoint mdr_v_all_zeroevaluationmatrixpositivepoint. ((mdr_i_all_zeroevaluationmatrixpositive = (q) * mdr_r_all_zeroevaluationmatrixpositivepoint + mdr_s_all_zeroevaluationmatrixpositivepoint) /\ ((exists mdr_gap_all_zeroevaluationmatrixpositivepointcolumn. mdr_gap_all_zeroevaluationmatrixpositivepointcolumn + S (mdr_s_all_zeroevaluationmatrixpositivepoint) = (q)) /\ ((((exists ff_h_mdr_all_zeroevaluationmatrixpositivepointrow_index. ff_h_mdr_all_zeroevaluationmatrixpositivepointrow_index + S (mdr_u_all_zeroevaluationmatrixpositivepoint) = S ((S (mdr_r_all_zeroevaluationmatrixpositivepoint)) * mdr_rc_all_zero)) /\ exists ff_q_mdr_all_zeroevaluationmatrixpositivepointrow_index. mdr_rb_all_zero = ff_q_mdr_all_zeroevaluationmatrixpositivepointrow_index * S ((S (mdr_r_all_zeroevaluationmatrixpositivepoint)) * mdr_rc_all_zero) + (mdr_u_all_zeroevaluationmatrixpositivepoint))) /\ ((((exists ff_h_mdr_all_zeroevaluationmatrixpositivepointcolumn_index. ff_h_mdr_all_zeroevaluationmatrixpositivepointcolumn_index + S (mdr_v_all_zeroevaluationmatrixpositivepoint) = S ((S (mdr_s_all_zeroevaluationmatrixpositivepoint)) * mdr_cc_all_zero)) /\ exists ff_q_mdr_all_zeroevaluationmatrixpositivepointcolumn_index. mdr_cb_all_zero = ff_q_mdr_all_zeroevaluationmatrixpositivepointcolumn_index * S ((S (mdr_s_all_zeroevaluationmatrixpositivepoint)) * mdr_cc_all_zero) + (mdr_v_all_zeroevaluationmatrixpositivepoint))) /\ (((exists ff_h_mdr_all_zeroevaluationmatrixpositivepointsource. ff_h_mdr_all_zeroevaluationmatrixpositivepointsource + S (mdr_a_all_zeroevaluationmatrixpositive) = S ((S ((mdr_u_all_zeroevaluationmatrixpositivepoint) * (w) + (mdr_v_all_zeroevaluationmatrixpositivepoint))) * pc)) /\ exists ff_q_mdr_all_zeroevaluationmatrixpositivepointsource. pb = ff_q_mdr_all_zeroevaluationmatrixpositivepointsource * S ((S ((mdr_u_all_zeroevaluationmatrixpositivepoint) * (w) + (mdr_v_all_zeroevaluationmatrixpositivepoint))) * pc) + (mdr_a_all_zeroevaluationmatrixpositive)))))))) /\ (((exists ff_h_mdr_all_zeroevaluationmatrixpositiveoutput. ff_h_mdr_all_zeroevaluationmatrixpositiveoutput + S (mdr_a_all_zeroevaluationmatrixpositive) = S ((S (mdr_i_all_zeroevaluationmatrixpositive)) * mdr_uc_all_zeroevaluation)) /\ exists ff_q_mdr_all_zeroevaluationmatrixpositiveoutput. mdr_ub_all_zeroevaluation = ff_q_mdr_all_zeroevaluationmatrixpositiveoutput * S ((S (mdr_i_all_zeroevaluationmatrixpositive)) * mdr_uc_all_zeroevaluation) + (mdr_a_all_zeroevaluationmatrixpositive)))))) /\ (forall mdr_i_all_zeroevaluationmatrixnegative. (exists mdr_gap_all_zeroevaluationmatrixnegativebound. mdr_gap_all_zeroevaluationmatrixnegativebound + S (mdr_i_all_zeroevaluationmatrixnegative) = ((q) * (q))) -> exists mdr_a_all_zeroevaluationmatrixnegative. (((exists mdr_r_all_zeroevaluationmatrixnegativepoint mdr_s_all_zeroevaluationmatrixnegativepoint mdr_u_all_zeroevaluationmatrixnegativepoint mdr_v_all_zeroevaluationmatrixnegativepoint. ((mdr_i_all_zeroevaluationmatrixnegative = (q) * mdr_r_all_zeroevaluationmatrixnegativepoint + mdr_s_all_zeroevaluationmatrixnegativepoint) /\ ((exists mdr_gap_all_zeroevaluationmatrixnegativepointcolumn. mdr_gap_all_zeroevaluationmatrixnegativepointcolumn + S (mdr_s_all_zeroevaluationmatrixnegativepoint) = (q)) /\ ((((exists ff_h_mdr_all_zeroevaluationmatrixnegativepointrow_index. ff_h_mdr_all_zeroevaluationmatrixnegativepointrow_index + S (mdr_u_all_zeroevaluationmatrixnegativepoint) = S ((S (mdr_r_all_zeroevaluationmatrixnegativepoint)) * mdr_rc_all_zero)) /\ exists ff_q_mdr_all_zeroevaluationmatrixnegativepointrow_index. mdr_rb_all_zero = ff_q_mdr_all_zeroevaluationmatrixnegativepointrow_index * S ((S (mdr_r_all_zeroevaluationmatrixnegativepoint)) * mdr_rc_all_zero) + (mdr_u_all_zeroevaluationmatrixnegativepoint))) /\ ((((exists ff_h_mdr_all_zeroevaluationmatrixnegativepointcolumn_index. ff_h_mdr_all_zeroevaluationmatrixnegativepointcolumn_index + S (mdr_v_all_zeroevaluationmatrixnegativepoint) = S ((S (mdr_s_all_zeroevaluationmatrixnegativepoint)) * mdr_cc_all_zero)) /\ exists ff_q_mdr_all_zeroevaluationmatrixnegativepointcolumn_index. mdr_cb_all_zero = ff_q_mdr_all_zeroevaluationmatrixnegativepointcolumn_index * S ((S (mdr_s_all_zeroevaluationmatrixnegativepoint)) * mdr_cc_all_zero) + (mdr_v_all_zeroevaluationmatrixnegativepoint))) /\ (((exists ff_h_mdr_all_zeroevaluationmatrixnegativepointsource. ff_h_mdr_all_zeroevaluationmatrixnegativepointsource + S (mdr_a_all_zeroevaluationmatrixnegative) = S ((S ((mdr_u_all_zeroevaluationmatrixnegativepoint) * (w) + (mdr_v_all_zeroevaluationmatrixnegativepoint))) * nc)) /\ exists ff_q_mdr_all_zeroevaluationmatrixnegativepointsource. nb = ff_q_mdr_all_zeroevaluationmatrixnegativepointsource * S ((S ((mdr_u_all_zeroevaluationmatrixnegativepoint) * (w) + (mdr_v_all_zeroevaluationmatrixnegativepoint))) * nc) + (mdr_a_all_zeroevaluationmatrixnegative)))))))) /\ (((exists ff_h_mdr_all_zeroevaluationmatrixnegativeoutput. ff_h_mdr_all_zeroevaluationmatrixnegativeoutput + S (mdr_a_all_zeroevaluationmatrixnegative) = S ((S (mdr_i_all_zeroevaluationmatrixnegative)) * mdr_vc_all_zeroevaluation)) /\ exists ff_q_mdr_all_zeroevaluationmatrixnegativeoutput. mdr_vb_all_zeroevaluation = ff_q_mdr_all_zeroevaluationmatrixnegativeoutput * S ((S (mdr_i_all_zeroevaluationmatrixnegative)) * mdr_vc_all_zeroevaluation) + (mdr_a_all_zeroevaluationmatrixnegative)))))))) /\ (exists mdr_b_all_zeroevaluationdeterminant mdr_c_all_zeroevaluationdeterminant mdr_l_all_zeroevaluationdeterminant mdr_i_all_zeroevaluationdeterminant. ((forall mdr_i_all_zeroevaluationdeterminanth. (exists mdr_gap_all_zeroevaluationdeterminanthi. mdr_gap_all_zeroevaluationdeterminanthi + S (mdr_i_all_zeroevaluationdeterminanth) = (mdr_l_all_zeroevaluationdeterminant)) -> exists mdr_d_all_zeroevaluationdeterminanth mdr_pb_all_zeroevaluationdeterminanth mdr_pc_all_zeroevaluationdeterminanth mdr_nb_all_zeroevaluationdeterminanth mdr_nc_all_zeroevaluationdeterminanth mdr_p_all_zeroevaluationdeterminanth mdr_n_all_zeroevaluationdeterminanth. ((exists mdr_z_all_zeroevaluationdeterminanthr. ((exists mdr_a_all_zeroevaluationdeterminanthrc mdr_b_all_zeroevaluationdeterminanthrc mdr_c_all_zeroevaluationdeterminanthrc mdr_e_all_zeroevaluationdeterminanthrc mdr_f_all_zeroevaluationdeterminanthrc. ((mdr_a_all_zeroevaluationdeterminanthrc = ((mdr_d_all_zeroevaluationdeterminanth) + (mdr_pb_all_zeroevaluationdeterminanth)) * S ((mdr_d_all_zeroevaluationdeterminanth) + (mdr_pb_all_zeroevaluationdeterminanth)) + ((mdr_pb_all_zeroevaluationdeterminanth) + (mdr_pb_all_zeroevaluationdeterminanth))) /\ ((mdr_b_all_zeroevaluationdeterminanthrc = ((mdr_pc_all_zeroevaluationdeterminanth) + (mdr_nb_all_zeroevaluationdeterminanth)) * S ((mdr_pc_all_zeroevaluationdeterminanth) + (mdr_nb_all_zeroevaluationdeterminanth)) + ((mdr_nb_all_zeroevaluationdeterminanth) + (mdr_nb_all_zeroevaluationdeterminanth))) /\ ((mdr_c_all_zeroevaluationdeterminanthrc = ((mdr_a_all_zeroevaluationdeterminanthrc) + (mdr_b_all_zeroevaluationdeterminanthrc)) * S ((mdr_a_all_zeroevaluationdeterminanthrc) + (mdr_b_all_zeroevaluationdeterminanthrc)) + ((mdr_b_all_zeroevaluationdeterminanthrc) + (mdr_b_all_zeroevaluationdeterminanthrc))) /\ ((mdr_e_all_zeroevaluationdeterminanthrc = ((mdr_p_all_zeroevaluationdeterminanth) + (mdr_n_all_zeroevaluationdeterminanth)) * S ((mdr_p_all_zeroevaluationdeterminanth) + (mdr_n_all_zeroevaluationdeterminanth)) + ((mdr_n_all_zeroevaluationdeterminanth) + (mdr_n_all_zeroevaluationdeterminanth))) /\ ((mdr_f_all_zeroevaluationdeterminanthrc = ((mdr_nc_all_zeroevaluationdeterminanth) + (mdr_e_all_zeroevaluationdeterminanthrc)) * S ((mdr_nc_all_zeroevaluationdeterminanth) + (mdr_e_all_zeroevaluationdeterminanthrc)) + ((mdr_e_all_zeroevaluationdeterminanthrc) + (mdr_e_all_zeroevaluationdeterminanthrc))) /\ ((mdr_z_all_zeroevaluationdeterminanthr) = ((mdr_c_all_zeroevaluationdeterminanthrc) + (mdr_f_all_zeroevaluationdeterminanthrc)) * S ((mdr_c_all_zeroevaluationdeterminanthrc) + (mdr_f_all_zeroevaluationdeterminanthrc)) + ((mdr_f_all_zeroevaluationdeterminanthrc) + (mdr_f_all_zeroevaluationdeterminanthrc))))))))) /\ (((exists ff_h_mdr_all_zeroevaluationdeterminanthrb. ff_h_mdr_all_zeroevaluationdeterminanthrb + S (mdr_z_all_zeroevaluationdeterminanthr) = S ((S (mdr_i_all_zeroevaluationdeterminanth)) * mdr_c_all_zeroevaluationdeterminant)) /\ exists ff_q_mdr_all_zeroevaluationdeterminanthrb. mdr_b_all_zeroevaluationdeterminant = ff_q_mdr_all_zeroevaluationdeterminanthrb * S ((S (mdr_i_all_zeroevaluationdeterminanth)) * mdr_c_all_zeroevaluationdeterminant) + (mdr_z_all_zeroevaluationdeterminanthr))))) /\ (((((mdr_d_all_zeroevaluationdeterminanth) = 0) /\ (((mdr_p_all_zeroevaluationdeterminanth) = 1) /\ ((mdr_n_all_zeroevaluationdeterminanth) = 0))) \/ exists mdr_q_all_zeroevaluationdeterminanths mdr_eb_all_zeroevaluationdeterminanths mdr_ec_all_zeroevaluationdeterminanths mdr_fb_all_zeroevaluationdeterminanths mdr_fc_all_zeroevaluationdeterminanths. (((mdr_d_all_zeroevaluationdeterminanth) = S (mdr_q_all_zeroevaluationdeterminanths)) /\ ((forall mdr_j_all_zeroevaluationdeterminanthsc. (exists mdr_gap_all_zeroevaluationdeterminanthscj. mdr_gap_all_zeroevaluationdeterminanthscj + S (mdr_j_all_zeroevaluationdeterminanthsc) = (S (mdr_q_all_zeroevaluationdeterminanths))) -> exists mdr_i_all_zeroevaluationdeterminanthsc mdr_up_all_zeroevaluationdeterminanthsc mdr_us_all_zeroevaluationdeterminanthsc mdr_un_all_zeroevaluationdeterminanthsc mdr_ut_all_zeroevaluationdeterminanthsc mdr_p_all_zeroevaluationdeterminanthsc mdr_n_all_zeroevaluationdeterminanthsc. ((exists mdr_gap_all_zeroevaluationdeterminanthsci. mdr_gap_all_zeroevaluationdeterminanthsci + S (mdr_i_all_zeroevaluationdeterminanthsc) = (mdr_i_all_zeroevaluationdeterminanth)) /\ ((exists mdr_z_all_zeroevaluationdeterminanthscr. ((exists mdr_a_all_zeroevaluationdeterminanthscrc mdr_b_all_zeroevaluationdeterminanthscrc mdr_c_all_zeroevaluationdeterminanthscrc mdr_e_all_zeroevaluationdeterminanthscrc mdr_f_all_zeroevaluationdeterminanthscrc. ((mdr_a_all_zeroevaluationdeterminanthscrc = ((mdr_q_all_zeroevaluationdeterminanths) + (mdr_up_all_zeroevaluationdeterminanthsc)) * S ((mdr_q_all_zeroevaluationdeterminanths) + (mdr_up_all_zeroevaluationdeterminanthsc)) + ((mdr_up_all_zeroevaluationdeterminanthsc) + (mdr_up_all_zeroevaluationdeterminanthsc))) /\ ((mdr_b_all_zeroevaluationdeterminanthscrc = ((mdr_us_all_zeroevaluationdeterminanthsc) + (mdr_un_all_zeroevaluationdeterminanthsc)) * S ((mdr_us_all_zeroevaluationdeterminanthsc) + (mdr_un_all_zeroevaluationdeterminanthsc)) + ((mdr_un_all_zeroevaluationdeterminanthsc) + (mdr_un_all_zeroevaluationdeterminanthsc))) /\ ((mdr_c_all_zeroevaluationdeterminanthscrc = ((mdr_a_all_zeroevaluationdeterminanthscrc) + (mdr_b_all_zeroevaluationdeterminanthscrc)) * S ((mdr_a_all_zeroevaluationdeterminanthscrc) + (mdr_b_all_zeroevaluationdeterminanthscrc)) + ((mdr_b_all_zeroevaluationdeterminanthscrc) + (mdr_b_all_zeroevaluationdeterminanthscrc))) /\ ((mdr_e_all_zeroevaluationdeterminanthscrc = ((mdr_p_all_zeroevaluationdeterminanthsc) + (mdr_n_all_zeroevaluationdeterminanthsc)) * S ((mdr_p_all_zeroevaluationdeterminanthsc) + (mdr_n_all_zeroevaluationdeterminanthsc)) + ((mdr_n_all_zeroevaluationdeterminanthsc) + (mdr_n_all_zeroevaluationdeterminanthsc))) /\ ((mdr_f_all_zeroevaluationdeterminanthscrc = ((mdr_ut_all_zeroevaluationdeterminanthsc) + (mdr_e_all_zeroevaluationdeterminanthscrc)) * S ((mdr_ut_all_zeroevaluationdeterminanthsc) + (mdr_e_all_zeroevaluationdeterminanthscrc)) + ((mdr_e_all_zeroevaluationdeterminanthscrc) + (mdr_e_all_zeroevaluationdeterminanthscrc))) /\ ((mdr_z_all_zeroevaluationdeterminanthscr) = ((mdr_c_all_zeroevaluationdeterminanthscrc) + (mdr_f_all_zeroevaluationdeterminanthscrc)) * S ((mdr_c_all_zeroevaluationdeterminanthscrc) + (mdr_f_all_zeroevaluationdeterminanthscrc)) + ((mdr_f_all_zeroevaluationdeterminanthscrc) + (mdr_f_all_zeroevaluationdeterminanthscrc))))))))) /\ (((exists ff_h_mdr_all_zeroevaluationdeterminanthscrb. ff_h_mdr_all_zeroevaluationdeterminanthscrb + S (mdr_z_all_zeroevaluationdeterminanthscr) = S ((S (mdr_i_all_zeroevaluationdeterminanthsc)) * mdr_c_all_zeroevaluationdeterminant)) /\ exists ff_q_mdr_all_zeroevaluationdeterminanthscrb. mdr_b_all_zeroevaluationdeterminant = ff_q_mdr_all_zeroevaluationdeterminanthscrb * S ((S (mdr_i_all_zeroevaluationdeterminanthsc)) * mdr_c_all_zeroevaluationdeterminant) + (mdr_z_all_zeroevaluationdeterminanthscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_all_zeroevaluationdeterminanthscm_positive. (exists ff_gap_mdm_lt_mdr_all_zeroevaluationdeterminanthscm_positive_index_bound. ff_gap_mdm_lt_mdr_all_zeroevaluationdeterminanthscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_all_zeroevaluationdeterminanthscm_positive) = ((mdr_q_all_zeroevaluationdeterminanths) * (mdr_q_all_zeroevaluationdeterminanths))) -> exists ff_row_mdm_prefix_mdr_all_zeroevaluationdeterminanthscm_positive ff_column_mdm_prefix_mdr_all_zeroevaluationdeterminanthscm_positive ff_value_mdm_prefix_mdr_all_zeroevaluationdeterminanthscm_positive. (ff_index_mdm_prefix_mdr_all_zeroevaluationdeterminanthscm_positive = (mdr_q_all_zeroevaluationdeterminanths) * ff_row_mdm_prefix_mdr_all_zeroevaluationdeterminanthscm_positive + ff_column_mdm_prefix_mdr_all_zeroevaluationdeterminanthscm_positive /\ ((exists ff_gap_mdm_lt_mdr_all_zeroevaluationdeterminanthscm_positive_column_bound. ff_gap_mdm_lt_mdr_all_zeroevaluationdeterminanthscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_all_zeroevaluationdeterminanthscm_positive) = (mdr_q_all_zeroevaluationdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_all_zeroevaluationdeterminanthscm_positive_cell ff_column_mdm_cell_mdr_all_zeroevaluationdeterminanthscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_all_zeroevaluationdeterminanthscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_all_zeroevaluationdeterminanthscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_all_zeroevaluationdeterminanthscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_all_zeroevaluationdeterminanthscm_positive_cell = ff_row_mdm_prefix_mdr_all_zeroevaluationdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_all_zeroevaluationdeterminanthscm_positive_cell_row_after. ff_gap_mdm_le_mdr_all_zeroevaluationdeterminanthscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_all_zeroevaluationdeterminanthscm_positive)) /\ ff_row_mdm_cell_mdr_all_zeroevaluationdeterminanthscm_positive_cell = S ff_row_mdm_prefix_mdr_all_zeroevaluationdeterminanthscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_all_zeroevaluationdeterminanthscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_all_zeroevaluationdeterminanthscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_all_zeroevaluationdeterminanthscm_positive) = (mdr_j_all_zeroevaluationdeterminanthsc)) /\ ff_column_mdm_cell_mdr_all_zeroevaluationdeterminanthscm_positive_cell = ff_column_mdm_prefix_mdr_all_zeroevaluationdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_all_zeroevaluationdeterminanthscm_positive_cell_column_after. ff_gap_mdm_le_mdr_all_zeroevaluationdeterminanthscm_positive_cell_column_after + (mdr_j_all_zeroevaluationdeterminanthsc) = (ff_column_mdm_prefix_mdr_all_zeroevaluationdeterminanthscm_positive)) /\ ff_column_mdm_cell_mdr_all_zeroevaluationdeterminanthscm_positive_cell = S ff_column_mdm_prefix_mdr_all_zeroevaluationdeterminanthscm_positive))) /\ (((exists ff_h_mdm_mdr_all_zeroevaluationdeterminanthscm_positive_cell_source. ff_h_mdm_mdr_all_zeroevaluationdeterminanthscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_all_zeroevaluationdeterminanthscm_positive) = S ((S ((ff_row_mdm_cell_mdr_all_zeroevaluationdeterminanthscm_positive_cell) * (S (mdr_q_all_zeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_all_zeroevaluationdeterminanthscm_positive_cell))) * mdr_pc_all_zeroevaluationdeterminanth)) /\ exists ff_q_mdm_mdr_all_zeroevaluationdeterminanthscm_positive_cell_source. mdr_pb_all_zeroevaluationdeterminanth = ff_q_mdm_mdr_all_zeroevaluationdeterminanthscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_all_zeroevaluationdeterminanthscm_positive_cell) * (S (mdr_q_all_zeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_all_zeroevaluationdeterminanthscm_positive_cell))) * mdr_pc_all_zeroevaluationdeterminanth) + (ff_value_mdm_prefix_mdr_all_zeroevaluationdeterminanthscm_positive)))))) /\ (((exists ff_h_mdm_mdr_all_zeroevaluationdeterminanthscm_positive_target. ff_h_mdm_mdr_all_zeroevaluationdeterminanthscm_positive_target + S (ff_value_mdm_prefix_mdr_all_zeroevaluationdeterminanthscm_positive) = S ((S (ff_index_mdm_prefix_mdr_all_zeroevaluationdeterminanthscm_positive)) * mdr_us_all_zeroevaluationdeterminanthsc)) /\ exists ff_q_mdm_mdr_all_zeroevaluationdeterminanthscm_positive_target. mdr_up_all_zeroevaluationdeterminanthsc = ff_q_mdm_mdr_all_zeroevaluationdeterminanthscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_all_zeroevaluationdeterminanthscm_positive)) * mdr_us_all_zeroevaluationdeterminanthsc) + (ff_value_mdm_prefix_mdr_all_zeroevaluationdeterminanthscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_all_zeroevaluationdeterminanthscm_negative. (exists ff_gap_mdm_lt_mdr_all_zeroevaluationdeterminanthscm_negative_index_bound. ff_gap_mdm_lt_mdr_all_zeroevaluationdeterminanthscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_all_zeroevaluationdeterminanthscm_negative) = ((mdr_q_all_zeroevaluationdeterminanths) * (mdr_q_all_zeroevaluationdeterminanths))) -> exists ff_row_mdm_prefix_mdr_all_zeroevaluationdeterminanthscm_negative ff_column_mdm_prefix_mdr_all_zeroevaluationdeterminanthscm_negative ff_value_mdm_prefix_mdr_all_zeroevaluationdeterminanthscm_negative. (ff_index_mdm_prefix_mdr_all_zeroevaluationdeterminanthscm_negative = (mdr_q_all_zeroevaluationdeterminanths) * ff_row_mdm_prefix_mdr_all_zeroevaluationdeterminanthscm_negative + ff_column_mdm_prefix_mdr_all_zeroevaluationdeterminanthscm_negative /\ ((exists ff_gap_mdm_lt_mdr_all_zeroevaluationdeterminanthscm_negative_column_bound. ff_gap_mdm_lt_mdr_all_zeroevaluationdeterminanthscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_all_zeroevaluationdeterminanthscm_negative) = (mdr_q_all_zeroevaluationdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_all_zeroevaluationdeterminanthscm_negative_cell ff_column_mdm_cell_mdr_all_zeroevaluationdeterminanthscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_all_zeroevaluationdeterminanthscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_all_zeroevaluationdeterminanthscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_all_zeroevaluationdeterminanthscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_all_zeroevaluationdeterminanthscm_negative_cell = ff_row_mdm_prefix_mdr_all_zeroevaluationdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_all_zeroevaluationdeterminanthscm_negative_cell_row_after. ff_gap_mdm_le_mdr_all_zeroevaluationdeterminanthscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_all_zeroevaluationdeterminanthscm_negative)) /\ ff_row_mdm_cell_mdr_all_zeroevaluationdeterminanthscm_negative_cell = S ff_row_mdm_prefix_mdr_all_zeroevaluationdeterminanthscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_all_zeroevaluationdeterminanthscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_all_zeroevaluationdeterminanthscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_all_zeroevaluationdeterminanthscm_negative) = (mdr_j_all_zeroevaluationdeterminanthsc)) /\ ff_column_mdm_cell_mdr_all_zeroevaluationdeterminanthscm_negative_cell = ff_column_mdm_prefix_mdr_all_zeroevaluationdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_all_zeroevaluationdeterminanthscm_negative_cell_column_after. ff_gap_mdm_le_mdr_all_zeroevaluationdeterminanthscm_negative_cell_column_after + (mdr_j_all_zeroevaluationdeterminanthsc) = (ff_column_mdm_prefix_mdr_all_zeroevaluationdeterminanthscm_negative)) /\ ff_column_mdm_cell_mdr_all_zeroevaluationdeterminanthscm_negative_cell = S ff_column_mdm_prefix_mdr_all_zeroevaluationdeterminanthscm_negative))) /\ (((exists ff_h_mdm_mdr_all_zeroevaluationdeterminanthscm_negative_cell_source. ff_h_mdm_mdr_all_zeroevaluationdeterminanthscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_all_zeroevaluationdeterminanthscm_negative) = S ((S ((ff_row_mdm_cell_mdr_all_zeroevaluationdeterminanthscm_negative_cell) * (S (mdr_q_all_zeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_all_zeroevaluationdeterminanthscm_negative_cell))) * mdr_nc_all_zeroevaluationdeterminanth)) /\ exists ff_q_mdm_mdr_all_zeroevaluationdeterminanthscm_negative_cell_source. mdr_nb_all_zeroevaluationdeterminanth = ff_q_mdm_mdr_all_zeroevaluationdeterminanthscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_all_zeroevaluationdeterminanthscm_negative_cell) * (S (mdr_q_all_zeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_all_zeroevaluationdeterminanthscm_negative_cell))) * mdr_nc_all_zeroevaluationdeterminanth) + (ff_value_mdm_prefix_mdr_all_zeroevaluationdeterminanthscm_negative)))))) /\ (((exists ff_h_mdm_mdr_all_zeroevaluationdeterminanthscm_negative_target. ff_h_mdm_mdr_all_zeroevaluationdeterminanthscm_negative_target + S (ff_value_mdm_prefix_mdr_all_zeroevaluationdeterminanthscm_negative) = S ((S (ff_index_mdm_prefix_mdr_all_zeroevaluationdeterminanthscm_negative)) * mdr_ut_all_zeroevaluationdeterminanthsc)) /\ exists ff_q_mdm_mdr_all_zeroevaluationdeterminanthscm_negative_target. mdr_un_all_zeroevaluationdeterminanthsc = ff_q_mdm_mdr_all_zeroevaluationdeterminanthscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_all_zeroevaluationdeterminanthscm_negative)) * mdr_ut_all_zeroevaluationdeterminanthsc) + (ff_value_mdm_prefix_mdr_all_zeroevaluationdeterminanthscm_negative))))))))) /\ ((((exists ff_h_mdr_all_zeroevaluationdeterminanthscp. ff_h_mdr_all_zeroevaluationdeterminanthscp + S (mdr_p_all_zeroevaluationdeterminanthsc) = S ((S (mdr_j_all_zeroevaluationdeterminanthsc)) * mdr_ec_all_zeroevaluationdeterminanths)) /\ exists ff_q_mdr_all_zeroevaluationdeterminanthscp. mdr_eb_all_zeroevaluationdeterminanths = ff_q_mdr_all_zeroevaluationdeterminanthscp * S ((S (mdr_j_all_zeroevaluationdeterminanthsc)) * mdr_ec_all_zeroevaluationdeterminanths) + (mdr_p_all_zeroevaluationdeterminanthsc))) /\ (((exists ff_h_mdr_all_zeroevaluationdeterminanthscn. ff_h_mdr_all_zeroevaluationdeterminanthscn + S (mdr_n_all_zeroevaluationdeterminanthsc) = S ((S (mdr_j_all_zeroevaluationdeterminanthsc)) * mdr_fc_all_zeroevaluationdeterminanths)) /\ exists ff_q_mdr_all_zeroevaluationdeterminanthscn. mdr_fb_all_zeroevaluationdeterminanths = ff_q_mdr_all_zeroevaluationdeterminanthscn * S ((S (mdr_j_all_zeroevaluationdeterminanthsc)) * mdr_fc_all_zeroevaluationdeterminanths) + (mdr_n_all_zeroevaluationdeterminanthsc)))))))) /\ (exists ff_ub_mce_fold_mdr_all_zeroevaluationdeterminanthsf ff_uc_mce_fold_mdr_all_zeroevaluationdeterminanthsf ff_vb_mce_fold_mdr_all_zeroevaluationdeterminanthsf ff_vc_mce_fold_mdr_all_zeroevaluationdeterminanthsf. ((forall ff_index_mce_alternating_mdr_all_zeroevaluationdeterminanthsf_prefix. (exists ff_gap_mce_mdr_all_zeroevaluationdeterminanthsf_prefix_index. ff_gap_mce_mdr_all_zeroevaluationdeterminanthsf_prefix_index + S (ff_index_mce_alternating_mdr_all_zeroevaluationdeterminanthsf_prefix) = (S (mdr_q_all_zeroevaluationdeterminanths))) -> exists ff_ap_mce_alternating_mdr_all_zeroevaluationdeterminanthsf_prefix ff_an_mce_alternating_mdr_all_zeroevaluationdeterminanthsf_prefix ff_bp_mce_alternating_mdr_all_zeroevaluationdeterminanthsf_prefix ff_bn_mce_alternating_mdr_all_zeroevaluationdeterminanthsf_prefix ff_p_mce_alternating_mdr_all_zeroevaluationdeterminanthsf_prefix ff_n_mce_alternating_mdr_all_zeroevaluationdeterminanthsf_prefix. ((((exists ff_h_mce_mdr_all_zeroevaluationdeterminanthsf_prefix_ap. ff_h_mce_mdr_all_zeroevaluationdeterminanthsf_prefix_ap + S (ff_ap_mce_alternating_mdr_all_zeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_all_zeroevaluationdeterminanthsf_prefix)) * mdr_pc_all_zeroevaluationdeterminanth)) /\ exists ff_q_mce_mdr_all_zeroevaluationdeterminanthsf_prefix_ap. mdr_pb_all_zeroevaluationdeterminanth = ff_q_mce_mdr_all_zeroevaluationdeterminanthsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_all_zeroevaluationdeterminanthsf_prefix)) * mdr_pc_all_zeroevaluationdeterminanth) + (ff_ap_mce_alternating_mdr_all_zeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_all_zeroevaluationdeterminanthsf_prefix_an. ff_h_mce_mdr_all_zeroevaluationdeterminanthsf_prefix_an + S (ff_an_mce_alternating_mdr_all_zeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_all_zeroevaluationdeterminanthsf_prefix)) * mdr_nc_all_zeroevaluationdeterminanth)) /\ exists ff_q_mce_mdr_all_zeroevaluationdeterminanthsf_prefix_an. mdr_nb_all_zeroevaluationdeterminanth = ff_q_mce_mdr_all_zeroevaluationdeterminanthsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_all_zeroevaluationdeterminanthsf_prefix)) * mdr_nc_all_zeroevaluationdeterminanth) + (ff_an_mce_alternating_mdr_all_zeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_all_zeroevaluationdeterminanthsf_prefix_bp. ff_h_mce_mdr_all_zeroevaluationdeterminanthsf_prefix_bp + S (ff_bp_mce_alternating_mdr_all_zeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_all_zeroevaluationdeterminanthsf_prefix)) * mdr_ec_all_zeroevaluationdeterminanths)) /\ exists ff_q_mce_mdr_all_zeroevaluationdeterminanthsf_prefix_bp. mdr_eb_all_zeroevaluationdeterminanths = ff_q_mce_mdr_all_zeroevaluationdeterminanthsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_all_zeroevaluationdeterminanthsf_prefix)) * mdr_ec_all_zeroevaluationdeterminanths) + (ff_bp_mce_alternating_mdr_all_zeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_all_zeroevaluationdeterminanthsf_prefix_bn. ff_h_mce_mdr_all_zeroevaluationdeterminanthsf_prefix_bn + S (ff_bn_mce_alternating_mdr_all_zeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_all_zeroevaluationdeterminanthsf_prefix)) * mdr_fc_all_zeroevaluationdeterminanths)) /\ exists ff_q_mce_mdr_all_zeroevaluationdeterminanthsf_prefix_bn. mdr_fb_all_zeroevaluationdeterminanths = ff_q_mce_mdr_all_zeroevaluationdeterminanthsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_all_zeroevaluationdeterminanthsf_prefix)) * mdr_fc_all_zeroevaluationdeterminanths) + (ff_bn_mce_alternating_mdr_all_zeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_all_zeroevaluationdeterminanthsf_prefix_positive. ff_h_mce_mdr_all_zeroevaluationdeterminanthsf_prefix_positive + S (ff_p_mce_alternating_mdr_all_zeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_all_zeroevaluationdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_all_zeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_all_zeroevaluationdeterminanthsf_prefix_positive. ff_ub_mce_fold_mdr_all_zeroevaluationdeterminanthsf = ff_q_mce_mdr_all_zeroevaluationdeterminanthsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_all_zeroevaluationdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_all_zeroevaluationdeterminanthsf) + (ff_p_mce_alternating_mdr_all_zeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_all_zeroevaluationdeterminanthsf_prefix_negative. ff_h_mce_mdr_all_zeroevaluationdeterminanthsf_prefix_negative + S (ff_n_mce_alternating_mdr_all_zeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_all_zeroevaluationdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_all_zeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_all_zeroevaluationdeterminanthsf_prefix_negative. ff_vb_mce_fold_mdr_all_zeroevaluationdeterminanthsf = ff_q_mce_mdr_all_zeroevaluationdeterminanthsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_all_zeroevaluationdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_all_zeroevaluationdeterminanthsf) + (ff_n_mce_alternating_mdr_all_zeroevaluationdeterminanthsf_prefix))) /\ (((exists ff_even_mce_term_mdr_all_zeroevaluationdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_all_zeroevaluationdeterminanthsf_prefix = 2 * ff_even_mce_term_mdr_all_zeroevaluationdeterminanthsf_prefix_term) /\ (ff_p_mce_alternating_mdr_all_zeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_all_zeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_all_zeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_all_zeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_all_zeroevaluationdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_all_zeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_all_zeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_all_zeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_all_zeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_all_zeroevaluationdeterminanthsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_all_zeroevaluationdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_all_zeroevaluationdeterminanthsf_prefix = 2 * ff_odd_mce_term_mdr_all_zeroevaluationdeterminanthsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_all_zeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_all_zeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_all_zeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_all_zeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_all_zeroevaluationdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_all_zeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_all_zeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_all_zeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_all_zeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_all_zeroevaluationdeterminanthsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_all_zeroevaluationdeterminanthsf_positive ff_v_mce_mdr_all_zeroevaluationdeterminanthsf_positive. ((((exists ff_h_mce_mdr_all_zeroevaluationdeterminanthsf_positive_start. ff_h_mce_mdr_all_zeroevaluationdeterminanthsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_all_zeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_all_zeroevaluationdeterminanthsf_positive_start. ff_u_mce_mdr_all_zeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_all_zeroevaluationdeterminanthsf_positive_start * S ((S (0)) * ff_v_mce_mdr_all_zeroevaluationdeterminanthsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_all_zeroevaluationdeterminanthsf_positive_terminal. ff_h_mce_mdr_all_zeroevaluationdeterminanthsf_positive_terminal + S (mdr_p_all_zeroevaluationdeterminanth) = S ((S ((S (mdr_q_all_zeroevaluationdeterminanths)))) * ff_v_mce_mdr_all_zeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_all_zeroevaluationdeterminanthsf_positive_terminal. ff_u_mce_mdr_all_zeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_all_zeroevaluationdeterminanthsf_positive_terminal * S ((S ((S (mdr_q_all_zeroevaluationdeterminanths)))) * ff_v_mce_mdr_all_zeroevaluationdeterminanthsf_positive) + (mdr_p_all_zeroevaluationdeterminanth))) /\ forall ff_i_mce_mdr_all_zeroevaluationdeterminanthsf_positive. (exists ff_lt_mce_mdr_all_zeroevaluationdeterminanthsf_positive_bound. ff_lt_mce_mdr_all_zeroevaluationdeterminanthsf_positive_bound + S ff_i_mce_mdr_all_zeroevaluationdeterminanthsf_positive = (S (mdr_q_all_zeroevaluationdeterminanths))) -> exists ff_a_mce_mdr_all_zeroevaluationdeterminanthsf_positive ff_r_mce_mdr_all_zeroevaluationdeterminanthsf_positive ff_s_mce_mdr_all_zeroevaluationdeterminanthsf_positive. ((((exists ff_h_mce_mdr_all_zeroevaluationdeterminanthsf_positive_summand. ff_h_mce_mdr_all_zeroevaluationdeterminanthsf_positive_summand + S (ff_a_mce_mdr_all_zeroevaluationdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_all_zeroevaluationdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_all_zeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_all_zeroevaluationdeterminanthsf_positive_summand. ff_ub_mce_fold_mdr_all_zeroevaluationdeterminanthsf = ff_q_mce_mdr_all_zeroevaluationdeterminanthsf_positive_summand * S ((S (ff_i_mce_mdr_all_zeroevaluationdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_all_zeroevaluationdeterminanthsf) + (ff_a_mce_mdr_all_zeroevaluationdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_all_zeroevaluationdeterminanthsf_positive_partial. ff_h_mce_mdr_all_zeroevaluationdeterminanthsf_positive_partial + S (ff_r_mce_mdr_all_zeroevaluationdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_all_zeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_all_zeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_all_zeroevaluationdeterminanthsf_positive_partial. ff_u_mce_mdr_all_zeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_all_zeroevaluationdeterminanthsf_positive_partial * S ((S (ff_i_mce_mdr_all_zeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_all_zeroevaluationdeterminanthsf_positive) + (ff_r_mce_mdr_all_zeroevaluationdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_all_zeroevaluationdeterminanthsf_positive_successor. ff_h_mce_mdr_all_zeroevaluationdeterminanthsf_positive_successor + S (ff_s_mce_mdr_all_zeroevaluationdeterminanthsf_positive) = S ((S (S ff_i_mce_mdr_all_zeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_all_zeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_all_zeroevaluationdeterminanthsf_positive_successor. ff_u_mce_mdr_all_zeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_all_zeroevaluationdeterminanthsf_positive_successor * S ((S (S ff_i_mce_mdr_all_zeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_all_zeroevaluationdeterminanthsf_positive) + (ff_s_mce_mdr_all_zeroevaluationdeterminanthsf_positive))) /\ ff_s_mce_mdr_all_zeroevaluationdeterminanthsf_positive = ff_r_mce_mdr_all_zeroevaluationdeterminanthsf_positive + ff_a_mce_mdr_all_zeroevaluationdeterminanthsf_positive)))))) /\ (exists ff_u_mce_mdr_all_zeroevaluationdeterminanthsf_negative ff_v_mce_mdr_all_zeroevaluationdeterminanthsf_negative. ((((exists ff_h_mce_mdr_all_zeroevaluationdeterminanthsf_negative_start. ff_h_mce_mdr_all_zeroevaluationdeterminanthsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_all_zeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_all_zeroevaluationdeterminanthsf_negative_start. ff_u_mce_mdr_all_zeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_all_zeroevaluationdeterminanthsf_negative_start * S ((S (0)) * ff_v_mce_mdr_all_zeroevaluationdeterminanthsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_all_zeroevaluationdeterminanthsf_negative_terminal. ff_h_mce_mdr_all_zeroevaluationdeterminanthsf_negative_terminal + S (mdr_n_all_zeroevaluationdeterminanth) = S ((S ((S (mdr_q_all_zeroevaluationdeterminanths)))) * ff_v_mce_mdr_all_zeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_all_zeroevaluationdeterminanthsf_negative_terminal. ff_u_mce_mdr_all_zeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_all_zeroevaluationdeterminanthsf_negative_terminal * S ((S ((S (mdr_q_all_zeroevaluationdeterminanths)))) * ff_v_mce_mdr_all_zeroevaluationdeterminanthsf_negative) + (mdr_n_all_zeroevaluationdeterminanth))) /\ forall ff_i_mce_mdr_all_zeroevaluationdeterminanthsf_negative. (exists ff_lt_mce_mdr_all_zeroevaluationdeterminanthsf_negative_bound. ff_lt_mce_mdr_all_zeroevaluationdeterminanthsf_negative_bound + S ff_i_mce_mdr_all_zeroevaluationdeterminanthsf_negative = (S (mdr_q_all_zeroevaluationdeterminanths))) -> exists ff_a_mce_mdr_all_zeroevaluationdeterminanthsf_negative ff_r_mce_mdr_all_zeroevaluationdeterminanthsf_negative ff_s_mce_mdr_all_zeroevaluationdeterminanthsf_negative. ((((exists ff_h_mce_mdr_all_zeroevaluationdeterminanthsf_negative_summand. ff_h_mce_mdr_all_zeroevaluationdeterminanthsf_negative_summand + S (ff_a_mce_mdr_all_zeroevaluationdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_all_zeroevaluationdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_all_zeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_all_zeroevaluationdeterminanthsf_negative_summand. ff_vb_mce_fold_mdr_all_zeroevaluationdeterminanthsf = ff_q_mce_mdr_all_zeroevaluationdeterminanthsf_negative_summand * S ((S (ff_i_mce_mdr_all_zeroevaluationdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_all_zeroevaluationdeterminanthsf) + (ff_a_mce_mdr_all_zeroevaluationdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_all_zeroevaluationdeterminanthsf_negative_partial. ff_h_mce_mdr_all_zeroevaluationdeterminanthsf_negative_partial + S (ff_r_mce_mdr_all_zeroevaluationdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_all_zeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_all_zeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_all_zeroevaluationdeterminanthsf_negative_partial. ff_u_mce_mdr_all_zeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_all_zeroevaluationdeterminanthsf_negative_partial * S ((S (ff_i_mce_mdr_all_zeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_all_zeroevaluationdeterminanthsf_negative) + (ff_r_mce_mdr_all_zeroevaluationdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_all_zeroevaluationdeterminanthsf_negative_successor. ff_h_mce_mdr_all_zeroevaluationdeterminanthsf_negative_successor + S (ff_s_mce_mdr_all_zeroevaluationdeterminanthsf_negative) = S ((S (S ff_i_mce_mdr_all_zeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_all_zeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_all_zeroevaluationdeterminanthsf_negative_successor. ff_u_mce_mdr_all_zeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_all_zeroevaluationdeterminanthsf_negative_successor * S ((S (S ff_i_mce_mdr_all_zeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_all_zeroevaluationdeterminanthsf_negative) + (ff_s_mce_mdr_all_zeroevaluationdeterminanthsf_negative))) /\ ff_s_mce_mdr_all_zeroevaluationdeterminanthsf_negative = ff_r_mce_mdr_all_zeroevaluationdeterminanthsf_negative + ff_a_mce_mdr_all_zeroevaluationdeterminanthsf_negative))))))))))))))) /\ ((exists mdr_gap_all_zeroevaluationdeterminanti. mdr_gap_all_zeroevaluationdeterminanti + S (mdr_i_all_zeroevaluationdeterminant) = (mdr_l_all_zeroevaluationdeterminant)) /\ (exists mdr_z_all_zeroevaluationdeterminantr. ((exists mdr_a_all_zeroevaluationdeterminantrc mdr_b_all_zeroevaluationdeterminantrc mdr_c_all_zeroevaluationdeterminantrc mdr_e_all_zeroevaluationdeterminantrc mdr_f_all_zeroevaluationdeterminantrc. ((mdr_a_all_zeroevaluationdeterminantrc = ((q) + (mdr_ub_all_zeroevaluation)) * S ((q) + (mdr_ub_all_zeroevaluation)) + ((mdr_ub_all_zeroevaluation) + (mdr_ub_all_zeroevaluation))) /\ ((mdr_b_all_zeroevaluationdeterminantrc = ((mdr_uc_all_zeroevaluation) + (mdr_vb_all_zeroevaluation)) * S ((mdr_uc_all_zeroevaluation) + (mdr_vb_all_zeroevaluation)) + ((mdr_vb_all_zeroevaluation) + (mdr_vb_all_zeroevaluation))) /\ ((mdr_c_all_zeroevaluationdeterminantrc = ((mdr_a_all_zeroevaluationdeterminantrc) + (mdr_b_all_zeroevaluationdeterminantrc)) * S ((mdr_a_all_zeroevaluationdeterminantrc) + (mdr_b_all_zeroevaluationdeterminantrc)) + ((mdr_b_all_zeroevaluationdeterminantrc) + (mdr_b_all_zeroevaluationdeterminantrc))) /\ ((mdr_e_all_zeroevaluationdeterminantrc = ((mdr_p_all_zero) + (mdr_n_all_zero)) * S ((mdr_p_all_zero) + (mdr_n_all_zero)) + ((mdr_n_all_zero) + (mdr_n_all_zero))) /\ ((mdr_f_all_zeroevaluationdeterminantrc = ((mdr_vc_all_zeroevaluation) + (mdr_e_all_zeroevaluationdeterminantrc)) * S ((mdr_vc_all_zeroevaluation) + (mdr_e_all_zeroevaluationdeterminantrc)) + ((mdr_e_all_zeroevaluationdeterminantrc) + (mdr_e_all_zeroevaluationdeterminantrc))) /\ ((mdr_z_all_zeroevaluationdeterminantr) = ((mdr_c_all_zeroevaluationdeterminantrc) + (mdr_f_all_zeroevaluationdeterminantrc)) * S ((mdr_c_all_zeroevaluationdeterminantrc) + (mdr_f_all_zeroevaluationdeterminantrc)) + ((mdr_f_all_zeroevaluationdeterminantrc) + (mdr_f_all_zeroevaluationdeterminantrc))))))))) /\ (((exists ff_h_mdr_all_zeroevaluationdeterminantrb. ff_h_mdr_all_zeroevaluationdeterminantrb + S (mdr_z_all_zeroevaluationdeterminantr) = S ((S (mdr_i_all_zeroevaluationdeterminant)) * mdr_c_all_zeroevaluationdeterminant)) /\ exists ff_q_mdr_all_zeroevaluationdeterminantrb. mdr_b_all_zeroevaluationdeterminant = ff_q_mdr_all_zeroevaluationdeterminantrb * S ((S (mdr_i_all_zeroevaluationdeterminant)) * mdr_c_all_zeroevaluationdeterminant) + (mdr_z_all_zeroevaluationdeterminantr)))))))))) -> mdr_p_all_zero = mdr_n_all_zero)Complete tactic proof in conservative notation
All 36 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.
Read the argument
Proof checkpoints
36 script commands · 15 reading checkpoints · 0 local claims
This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.
Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.
01Fix variables and assumptionsL1–10
02Fix variables and assumptionsL11–17
03Use earlier factsL18–19
04Separate the logical casesL20–20
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L20
cases eq_decidable
05Use earlier factsL21–21
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L21
exact eq_decidable_left
06Separate the logical casesL22–22
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L22
exfalso
07Use earlier factsL23–23
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L23
apply habsent
08Construct an explicit witnessL24–27
09Separate the logical casesL28–28
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L28
split
10Use earlier factsL29–29
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L29
exact hrows
11Separate the logical casesL30–30
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L30
split
12Use earlier factsL31–31
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L31
exact hcolumns
13Construct an explicit witnessL32–33
14Separate the logical casesL34–34
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L34
split
Original defined command ledger · 36 lines
- 0001
intro pb - 0002
intro pc - 0003
intro nb - 0004
intro nc - 0005
intro r - 0006
intro w - 0007
intro q - 0008
intro habsent - 0009
intro rb - 0010
intro rc - 0011
intro cb - 0012
intro cc - 0013
intro p - 0014
intro n - 0015
intro hrows - 0016
intro hcolumns - 0017
intro hvalue - 0018
specialize eq_decidable p - 0019
specialize eq_decidable n - 0020
cases eq_decidable - 0021
exact eq_decidable_left - 0022
exfalso - 0023
apply habsent - 0024
exists rb - 0025
exists rc - 0026
exists cb - 0027
exists cc - 0028
split - 0029
exact hrows - 0030
split - 0031
exact hcolumns - 0032
exists p - 0033
exists n - 0034
split - 0035
exact hvalue - 0036
exact eq_decidable_right