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. ∀ rc. ∀ cc. ∀ R. ∀ C. UniformBetaPrefixBox(rc,R,q,r) → UniformBetaPrefixBox(cc,C,q,w) → NonzeroMatrixMinor(pb,pc,nb,nc,r,w,q) → ∃ x. Lt(x,R) ∧ (∃ y. Lt(y,C) ∧ NonzeroSelectedMinor(pb,pc,nb,nc,r,w,q,x,rc,y,cc))Every linked abbreviation expands hygienically to the identical original native formula.
Definition DAG
Actual proof prerequisites
Original expanded first-order statement
forall pb pc nb nc r w q rc cc R C. (((~(R = 0)) /\ (forall mdr_b_rows_box mdr_e_rows_box. (forall fom_index_mrf_rows_boxsource. (exists fom_gap_mrf_rows_boxsource_index_bound. fom_gap_mrf_rows_boxsource_index_bound + S (fom_index_mrf_rows_boxsource) = q) -> exists fom_value_mrf_rows_boxsource. ((((exists fom_beta_height_mrf_rows_boxsource_entry. fom_beta_height_mrf_rows_boxsource_entry + S (fom_value_mrf_rows_boxsource) = S ((S (fom_index_mrf_rows_boxsource)) * mdr_e_rows_box)) /\ exists fom_beta_quotient_mrf_rows_boxsource_entry. mdr_b_rows_box = fom_beta_quotient_mrf_rows_boxsource_entry * S ((S (fom_index_mrf_rows_boxsource)) * mdr_e_rows_box) + (fom_value_mrf_rows_boxsource))) /\ (exists fom_gap_mrf_rows_boxsource_value_bound. fom_gap_mrf_rows_boxsource_value_bound + S (fom_value_mrf_rows_boxsource) = r))) -> exists mdr_z_rows_box. (((exists mdr_gap_rows_boxbound. mdr_gap_rows_boxbound + S (mdr_z_rows_box) = (R)) /\ (forall mdr_i_rows_boxprefix mdr_a_rows_boxprefix. (exists mdr_gap_rows_boxprefixb. mdr_gap_rows_boxprefixb + S (mdr_i_rows_boxprefix) = (q)) -> (((exists ff_h_mdr_rows_boxprefixo. ff_h_mdr_rows_boxprefixo + S (mdr_a_rows_boxprefix) = S ((S (mdr_i_rows_boxprefix)) * mdr_e_rows_box)) /\ exists ff_q_mdr_rows_boxprefixo. mdr_b_rows_box = ff_q_mdr_rows_boxprefixo * S ((S (mdr_i_rows_boxprefix)) * mdr_e_rows_box) + (mdr_a_rows_boxprefix))) -> (((exists ff_h_mdr_rows_boxprefixn. ff_h_mdr_rows_boxprefixn + S (mdr_a_rows_boxprefix) = S ((S (mdr_i_rows_boxprefix)) * rc)) /\ exists ff_q_mdr_rows_boxprefixn. mdr_z_rows_box = ff_q_mdr_rows_boxprefixn * S ((S (mdr_i_rows_boxprefix)) * rc) + (mdr_a_rows_boxprefix))))))))) -> (((~(C = 0)) /\ (forall mdr_b_columns_box mdr_e_columns_box. (forall fom_index_mrf_columns_boxsource. (exists fom_gap_mrf_columns_boxsource_index_bound. fom_gap_mrf_columns_boxsource_index_bound + S (fom_index_mrf_columns_boxsource) = q) -> exists fom_value_mrf_columns_boxsource. ((((exists fom_beta_height_mrf_columns_boxsource_entry. fom_beta_height_mrf_columns_boxsource_entry + S (fom_value_mrf_columns_boxsource) = S ((S (fom_index_mrf_columns_boxsource)) * mdr_e_columns_box)) /\ exists fom_beta_quotient_mrf_columns_boxsource_entry. mdr_b_columns_box = fom_beta_quotient_mrf_columns_boxsource_entry * S ((S (fom_index_mrf_columns_boxsource)) * mdr_e_columns_box) + (fom_value_mrf_columns_boxsource))) /\ (exists fom_gap_mrf_columns_boxsource_value_bound. fom_gap_mrf_columns_boxsource_value_bound + S (fom_value_mrf_columns_boxsource) = w))) -> exists mdr_z_columns_box. (((exists mdr_gap_columns_boxbound. mdr_gap_columns_boxbound + S (mdr_z_columns_box) = (C)) /\ (forall mdr_i_columns_boxprefix mdr_a_columns_boxprefix. (exists mdr_gap_columns_boxprefixb. mdr_gap_columns_boxprefixb + S (mdr_i_columns_boxprefix) = (q)) -> (((exists ff_h_mdr_columns_boxprefixo. ff_h_mdr_columns_boxprefixo + S (mdr_a_columns_boxprefix) = S ((S (mdr_i_columns_boxprefix)) * mdr_e_columns_box)) /\ exists ff_q_mdr_columns_boxprefixo. mdr_b_columns_box = ff_q_mdr_columns_boxprefixo * S ((S (mdr_i_columns_boxprefix)) * mdr_e_columns_box) + (mdr_a_columns_boxprefix))) -> (((exists ff_h_mdr_columns_boxprefixn. ff_h_mdr_columns_boxprefixn + S (mdr_a_columns_boxprefix) = S ((S (mdr_i_columns_boxprefix)) * cc)) /\ exists ff_q_mdr_columns_boxprefixn. mdr_z_columns_box = ff_q_mdr_columns_boxprefixn * S ((S (mdr_i_columns_boxprefix)) * cc) + (mdr_a_columns_boxprefix))))))))) -> (exists mdr_rb_unbounded_minor mdr_rc_unbounded_minor mdr_cb_unbounded_minor mdr_cc_unbounded_minor. (((((forall fom_index_mrf_unbounded_minorminorrowsbound. (exists fom_gap_mrf_unbounded_minorminorrowsbound_index_bound. fom_gap_mrf_unbounded_minorminorrowsbound_index_bound + S (fom_index_mrf_unbounded_minorminorrowsbound) = q) -> exists fom_value_mrf_unbounded_minorminorrowsbound. ((((exists fom_beta_height_mrf_unbounded_minorminorrowsbound_entry. fom_beta_height_mrf_unbounded_minorminorrowsbound_entry + S (fom_value_mrf_unbounded_minorminorrowsbound) = S ((S (fom_index_mrf_unbounded_minorminorrowsbound)) * mdr_rc_unbounded_minor)) /\ exists fom_beta_quotient_mrf_unbounded_minorminorrowsbound_entry. mdr_rb_unbounded_minor = fom_beta_quotient_mrf_unbounded_minorminorrowsbound_entry * S ((S (fom_index_mrf_unbounded_minorminorrowsbound)) * mdr_rc_unbounded_minor) + (fom_value_mrf_unbounded_minorminorrowsbound))) /\ (exists fom_gap_mrf_unbounded_minorminorrowsbound_value_bound. fom_gap_mrf_unbounded_minorminorrowsbound_value_bound + S (fom_value_mrf_unbounded_minorminorrowsbound) = r))) /\ (forall mdr_i_unbounded_minorminorrowsdistinct mdr_j_unbounded_minorminorrowsdistinct mdr_a_unbounded_minorminorrowsdistinct. (exists mdr_gap_unbounded_minorminorrowsdistincti. mdr_gap_unbounded_minorminorrowsdistincti + S (mdr_i_unbounded_minorminorrowsdistinct) = (q)) -> (exists mdr_gap_unbounded_minorminorrowsdistinctj. mdr_gap_unbounded_minorminorrowsdistinctj + S (mdr_j_unbounded_minorminorrowsdistinct) = (q)) -> (((exists ff_h_mdr_unbounded_minorminorrowsdistinctfirst. ff_h_mdr_unbounded_minorminorrowsdistinctfirst + S (mdr_a_unbounded_minorminorrowsdistinct) = S ((S (mdr_i_unbounded_minorminorrowsdistinct)) * mdr_rc_unbounded_minor)) /\ exists ff_q_mdr_unbounded_minorminorrowsdistinctfirst. mdr_rb_unbounded_minor = ff_q_mdr_unbounded_minorminorrowsdistinctfirst * S ((S (mdr_i_unbounded_minorminorrowsdistinct)) * mdr_rc_unbounded_minor) + (mdr_a_unbounded_minorminorrowsdistinct))) -> (((exists ff_h_mdr_unbounded_minorminorrowsdistinctsecond. ff_h_mdr_unbounded_minorminorrowsdistinctsecond + S (mdr_a_unbounded_minorminorrowsdistinct) = S ((S (mdr_j_unbounded_minorminorrowsdistinct)) * mdr_rc_unbounded_minor)) /\ exists ff_q_mdr_unbounded_minorminorrowsdistinctsecond. mdr_rb_unbounded_minor = ff_q_mdr_unbounded_minorminorrowsdistinctsecond * S ((S (mdr_j_unbounded_minorminorrowsdistinct)) * mdr_rc_unbounded_minor) + (mdr_a_unbounded_minorminorrowsdistinct))) -> mdr_i_unbounded_minorminorrowsdistinct = mdr_j_unbounded_minorminorrowsdistinct))) /\ ((((forall fom_index_mrf_unbounded_minorminorcolumnsbound. (exists fom_gap_mrf_unbounded_minorminorcolumnsbound_index_bound. fom_gap_mrf_unbounded_minorminorcolumnsbound_index_bound + S (fom_index_mrf_unbounded_minorminorcolumnsbound) = q) -> exists fom_value_mrf_unbounded_minorminorcolumnsbound. ((((exists fom_beta_height_mrf_unbounded_minorminorcolumnsbound_entry. fom_beta_height_mrf_unbounded_minorminorcolumnsbound_entry + S (fom_value_mrf_unbounded_minorminorcolumnsbound) = S ((S (fom_index_mrf_unbounded_minorminorcolumnsbound)) * mdr_cc_unbounded_minor)) /\ exists fom_beta_quotient_mrf_unbounded_minorminorcolumnsbound_entry. mdr_cb_unbounded_minor = fom_beta_quotient_mrf_unbounded_minorminorcolumnsbound_entry * S ((S (fom_index_mrf_unbounded_minorminorcolumnsbound)) * mdr_cc_unbounded_minor) + (fom_value_mrf_unbounded_minorminorcolumnsbound))) /\ (exists fom_gap_mrf_unbounded_minorminorcolumnsbound_value_bound. fom_gap_mrf_unbounded_minorminorcolumnsbound_value_bound + S (fom_value_mrf_unbounded_minorminorcolumnsbound) = w))) /\ (forall mdr_i_unbounded_minorminorcolumnsdistinct mdr_j_unbounded_minorminorcolumnsdistinct mdr_a_unbounded_minorminorcolumnsdistinct. (exists mdr_gap_unbounded_minorminorcolumnsdistincti. mdr_gap_unbounded_minorminorcolumnsdistincti + S (mdr_i_unbounded_minorminorcolumnsdistinct) = (q)) -> (exists mdr_gap_unbounded_minorminorcolumnsdistinctj. mdr_gap_unbounded_minorminorcolumnsdistinctj + S (mdr_j_unbounded_minorminorcolumnsdistinct) = (q)) -> (((exists ff_h_mdr_unbounded_minorminorcolumnsdistinctfirst. ff_h_mdr_unbounded_minorminorcolumnsdistinctfirst + S (mdr_a_unbounded_minorminorcolumnsdistinct) = S ((S (mdr_i_unbounded_minorminorcolumnsdistinct)) * mdr_cc_unbounded_minor)) /\ exists ff_q_mdr_unbounded_minorminorcolumnsdistinctfirst. mdr_cb_unbounded_minor = ff_q_mdr_unbounded_minorminorcolumnsdistinctfirst * S ((S (mdr_i_unbounded_minorminorcolumnsdistinct)) * mdr_cc_unbounded_minor) + (mdr_a_unbounded_minorminorcolumnsdistinct))) -> (((exists ff_h_mdr_unbounded_minorminorcolumnsdistinctsecond. ff_h_mdr_unbounded_minorminorcolumnsdistinctsecond + S (mdr_a_unbounded_minorminorcolumnsdistinct) = S ((S (mdr_j_unbounded_minorminorcolumnsdistinct)) * mdr_cc_unbounded_minor)) /\ exists ff_q_mdr_unbounded_minorminorcolumnsdistinctsecond. mdr_cb_unbounded_minor = ff_q_mdr_unbounded_minorminorcolumnsdistinctsecond * S ((S (mdr_j_unbounded_minorminorcolumnsdistinct)) * mdr_cc_unbounded_minor) + (mdr_a_unbounded_minorminorcolumnsdistinct))) -> mdr_i_unbounded_minorminorcolumnsdistinct = mdr_j_unbounded_minorminorcolumnsdistinct))) /\ (exists mdr_p_unbounded_minorminornonzero mdr_n_unbounded_minorminornonzero. ((exists mdr_ub_unbounded_minorminornonzeroevaluation mdr_uc_unbounded_minorminornonzeroevaluation mdr_vb_unbounded_minorminornonzeroevaluation mdr_vc_unbounded_minorminornonzeroevaluation. ((((forall mdr_i_unbounded_minorminornonzeroevaluationmatrixpositive. (exists mdr_gap_unbounded_minorminornonzeroevaluationmatrixpositivebound. mdr_gap_unbounded_minorminornonzeroevaluationmatrixpositivebound + S (mdr_i_unbounded_minorminornonzeroevaluationmatrixpositive) = ((q) * (q))) -> exists mdr_a_unbounded_minorminornonzeroevaluationmatrixpositive. (((exists mdr_r_unbounded_minorminornonzeroevaluationmatrixpositivepoint mdr_s_unbounded_minorminornonzeroevaluationmatrixpositivepoint mdr_u_unbounded_minorminornonzeroevaluationmatrixpositivepoint mdr_v_unbounded_minorminornonzeroevaluationmatrixpositivepoint. ((mdr_i_unbounded_minorminornonzeroevaluationmatrixpositive = (q) * mdr_r_unbounded_minorminornonzeroevaluationmatrixpositivepoint + mdr_s_unbounded_minorminornonzeroevaluationmatrixpositivepoint) /\ ((exists mdr_gap_unbounded_minorminornonzeroevaluationmatrixpositivepointcolumn. mdr_gap_unbounded_minorminornonzeroevaluationmatrixpositivepointcolumn + S (mdr_s_unbounded_minorminornonzeroevaluationmatrixpositivepoint) = (q)) /\ ((((exists ff_h_mdr_unbounded_minorminornonzeroevaluationmatrixpositivepointrow_index. ff_h_mdr_unbounded_minorminornonzeroevaluationmatrixpositivepointrow_index + S (mdr_u_unbounded_minorminornonzeroevaluationmatrixpositivepoint) = S ((S (mdr_r_unbounded_minorminornonzeroevaluationmatrixpositivepoint)) * mdr_rc_unbounded_minor)) /\ exists ff_q_mdr_unbounded_minorminornonzeroevaluationmatrixpositivepointrow_index. mdr_rb_unbounded_minor = ff_q_mdr_unbounded_minorminornonzeroevaluationmatrixpositivepointrow_index * S ((S (mdr_r_unbounded_minorminornonzeroevaluationmatrixpositivepoint)) * mdr_rc_unbounded_minor) + (mdr_u_unbounded_minorminornonzeroevaluationmatrixpositivepoint))) /\ ((((exists ff_h_mdr_unbounded_minorminornonzeroevaluationmatrixpositivepointcolumn_index. ff_h_mdr_unbounded_minorminornonzeroevaluationmatrixpositivepointcolumn_index + S (mdr_v_unbounded_minorminornonzeroevaluationmatrixpositivepoint) = S ((S (mdr_s_unbounded_minorminornonzeroevaluationmatrixpositivepoint)) * mdr_cc_unbounded_minor)) /\ exists ff_q_mdr_unbounded_minorminornonzeroevaluationmatrixpositivepointcolumn_index. mdr_cb_unbounded_minor = ff_q_mdr_unbounded_minorminornonzeroevaluationmatrixpositivepointcolumn_index * S ((S (mdr_s_unbounded_minorminornonzeroevaluationmatrixpositivepoint)) * mdr_cc_unbounded_minor) + (mdr_v_unbounded_minorminornonzeroevaluationmatrixpositivepoint))) /\ (((exists ff_h_mdr_unbounded_minorminornonzeroevaluationmatrixpositivepointsource. ff_h_mdr_unbounded_minorminornonzeroevaluationmatrixpositivepointsource + S (mdr_a_unbounded_minorminornonzeroevaluationmatrixpositive) = S ((S ((mdr_u_unbounded_minorminornonzeroevaluationmatrixpositivepoint) * (w) + (mdr_v_unbounded_minorminornonzeroevaluationmatrixpositivepoint))) * pc)) /\ exists ff_q_mdr_unbounded_minorminornonzeroevaluationmatrixpositivepointsource. pb = ff_q_mdr_unbounded_minorminornonzeroevaluationmatrixpositivepointsource * S ((S ((mdr_u_unbounded_minorminornonzeroevaluationmatrixpositivepoint) * (w) + (mdr_v_unbounded_minorminornonzeroevaluationmatrixpositivepoint))) * pc) + (mdr_a_unbounded_minorminornonzeroevaluationmatrixpositive)))))))) /\ (((exists ff_h_mdr_unbounded_minorminornonzeroevaluationmatrixpositiveoutput. ff_h_mdr_unbounded_minorminornonzeroevaluationmatrixpositiveoutput + S (mdr_a_unbounded_minorminornonzeroevaluationmatrixpositive) = S ((S (mdr_i_unbounded_minorminornonzeroevaluationmatrixpositive)) * mdr_uc_unbounded_minorminornonzeroevaluation)) /\ exists ff_q_mdr_unbounded_minorminornonzeroevaluationmatrixpositiveoutput. mdr_ub_unbounded_minorminornonzeroevaluation = ff_q_mdr_unbounded_minorminornonzeroevaluationmatrixpositiveoutput * S ((S (mdr_i_unbounded_minorminornonzeroevaluationmatrixpositive)) * mdr_uc_unbounded_minorminornonzeroevaluation) + (mdr_a_unbounded_minorminornonzeroevaluationmatrixpositive)))))) /\ (forall mdr_i_unbounded_minorminornonzeroevaluationmatrixnegative. (exists mdr_gap_unbounded_minorminornonzeroevaluationmatrixnegativebound. mdr_gap_unbounded_minorminornonzeroevaluationmatrixnegativebound + S (mdr_i_unbounded_minorminornonzeroevaluationmatrixnegative) = ((q) * (q))) -> exists mdr_a_unbounded_minorminornonzeroevaluationmatrixnegative. (((exists mdr_r_unbounded_minorminornonzeroevaluationmatrixnegativepoint mdr_s_unbounded_minorminornonzeroevaluationmatrixnegativepoint mdr_u_unbounded_minorminornonzeroevaluationmatrixnegativepoint mdr_v_unbounded_minorminornonzeroevaluationmatrixnegativepoint. ((mdr_i_unbounded_minorminornonzeroevaluationmatrixnegative = (q) * mdr_r_unbounded_minorminornonzeroevaluationmatrixnegativepoint + mdr_s_unbounded_minorminornonzeroevaluationmatrixnegativepoint) /\ ((exists mdr_gap_unbounded_minorminornonzeroevaluationmatrixnegativepointcolumn. mdr_gap_unbounded_minorminornonzeroevaluationmatrixnegativepointcolumn + S (mdr_s_unbounded_minorminornonzeroevaluationmatrixnegativepoint) = (q)) /\ ((((exists ff_h_mdr_unbounded_minorminornonzeroevaluationmatrixnegativepointrow_index. ff_h_mdr_unbounded_minorminornonzeroevaluationmatrixnegativepointrow_index + S (mdr_u_unbounded_minorminornonzeroevaluationmatrixnegativepoint) = S ((S (mdr_r_unbounded_minorminornonzeroevaluationmatrixnegativepoint)) * mdr_rc_unbounded_minor)) /\ exists ff_q_mdr_unbounded_minorminornonzeroevaluationmatrixnegativepointrow_index. mdr_rb_unbounded_minor = ff_q_mdr_unbounded_minorminornonzeroevaluationmatrixnegativepointrow_index * S ((S (mdr_r_unbounded_minorminornonzeroevaluationmatrixnegativepoint)) * mdr_rc_unbounded_minor) + (mdr_u_unbounded_minorminornonzeroevaluationmatrixnegativepoint))) /\ ((((exists ff_h_mdr_unbounded_minorminornonzeroevaluationmatrixnegativepointcolumn_index. ff_h_mdr_unbounded_minorminornonzeroevaluationmatrixnegativepointcolumn_index + S (mdr_v_unbounded_minorminornonzeroevaluationmatrixnegativepoint) = S ((S (mdr_s_unbounded_minorminornonzeroevaluationmatrixnegativepoint)) * mdr_cc_unbounded_minor)) /\ exists ff_q_mdr_unbounded_minorminornonzeroevaluationmatrixnegativepointcolumn_index. mdr_cb_unbounded_minor = ff_q_mdr_unbounded_minorminornonzeroevaluationmatrixnegativepointcolumn_index * S ((S (mdr_s_unbounded_minorminornonzeroevaluationmatrixnegativepoint)) * mdr_cc_unbounded_minor) + (mdr_v_unbounded_minorminornonzeroevaluationmatrixnegativepoint))) /\ (((exists ff_h_mdr_unbounded_minorminornonzeroevaluationmatrixnegativepointsource. ff_h_mdr_unbounded_minorminornonzeroevaluationmatrixnegativepointsource + S (mdr_a_unbounded_minorminornonzeroevaluationmatrixnegative) = S ((S ((mdr_u_unbounded_minorminornonzeroevaluationmatrixnegativepoint) * (w) + (mdr_v_unbounded_minorminornonzeroevaluationmatrixnegativepoint))) * nc)) /\ exists ff_q_mdr_unbounded_minorminornonzeroevaluationmatrixnegativepointsource. nb = ff_q_mdr_unbounded_minorminornonzeroevaluationmatrixnegativepointsource * S ((S ((mdr_u_unbounded_minorminornonzeroevaluationmatrixnegativepoint) * (w) + (mdr_v_unbounded_minorminornonzeroevaluationmatrixnegativepoint))) * nc) + (mdr_a_unbounded_minorminornonzeroevaluationmatrixnegative)))))))) /\ (((exists ff_h_mdr_unbounded_minorminornonzeroevaluationmatrixnegativeoutput. ff_h_mdr_unbounded_minorminornonzeroevaluationmatrixnegativeoutput + S (mdr_a_unbounded_minorminornonzeroevaluationmatrixnegative) = S ((S (mdr_i_unbounded_minorminornonzeroevaluationmatrixnegative)) * mdr_vc_unbounded_minorminornonzeroevaluation)) /\ exists ff_q_mdr_unbounded_minorminornonzeroevaluationmatrixnegativeoutput. mdr_vb_unbounded_minorminornonzeroevaluation = ff_q_mdr_unbounded_minorminornonzeroevaluationmatrixnegativeoutput * S ((S (mdr_i_unbounded_minorminornonzeroevaluationmatrixnegative)) * mdr_vc_unbounded_minorminornonzeroevaluation) + (mdr_a_unbounded_minorminornonzeroevaluationmatrixnegative)))))))) /\ (exists mdr_b_unbounded_minorminornonzeroevaluationdeterminant mdr_c_unbounded_minorminornonzeroevaluationdeterminant mdr_l_unbounded_minorminornonzeroevaluationdeterminant mdr_i_unbounded_minorminornonzeroevaluationdeterminant. ((forall mdr_i_unbounded_minorminornonzeroevaluationdeterminanth. (exists mdr_gap_unbounded_minorminornonzeroevaluationdeterminanthi. mdr_gap_unbounded_minorminornonzeroevaluationdeterminanthi + S (mdr_i_unbounded_minorminornonzeroevaluationdeterminanth) = (mdr_l_unbounded_minorminornonzeroevaluationdeterminant)) -> exists mdr_d_unbounded_minorminornonzeroevaluationdeterminanth mdr_pb_unbounded_minorminornonzeroevaluationdeterminanth mdr_pc_unbounded_minorminornonzeroevaluationdeterminanth mdr_nb_unbounded_minorminornonzeroevaluationdeterminanth mdr_nc_unbounded_minorminornonzeroevaluationdeterminanth mdr_p_unbounded_minorminornonzeroevaluationdeterminanth mdr_n_unbounded_minorminornonzeroevaluationdeterminanth. ((exists mdr_z_unbounded_minorminornonzeroevaluationdeterminanthr. ((exists mdr_a_unbounded_minorminornonzeroevaluationdeterminanthrc mdr_b_unbounded_minorminornonzeroevaluationdeterminanthrc mdr_c_unbounded_minorminornonzeroevaluationdeterminanthrc mdr_e_unbounded_minorminornonzeroevaluationdeterminanthrc mdr_f_unbounded_minorminornonzeroevaluationdeterminanthrc. ((mdr_a_unbounded_minorminornonzeroevaluationdeterminanthrc = ((mdr_d_unbounded_minorminornonzeroevaluationdeterminanth) + (mdr_pb_unbounded_minorminornonzeroevaluationdeterminanth)) * S ((mdr_d_unbounded_minorminornonzeroevaluationdeterminanth) + (mdr_pb_unbounded_minorminornonzeroevaluationdeterminanth)) + ((mdr_pb_unbounded_minorminornonzeroevaluationdeterminanth) + (mdr_pb_unbounded_minorminornonzeroevaluationdeterminanth))) /\ ((mdr_b_unbounded_minorminornonzeroevaluationdeterminanthrc = ((mdr_pc_unbounded_minorminornonzeroevaluationdeterminanth) + (mdr_nb_unbounded_minorminornonzeroevaluationdeterminanth)) * S ((mdr_pc_unbounded_minorminornonzeroevaluationdeterminanth) + (mdr_nb_unbounded_minorminornonzeroevaluationdeterminanth)) + ((mdr_nb_unbounded_minorminornonzeroevaluationdeterminanth) + (mdr_nb_unbounded_minorminornonzeroevaluationdeterminanth))) /\ ((mdr_c_unbounded_minorminornonzeroevaluationdeterminanthrc = ((mdr_a_unbounded_minorminornonzeroevaluationdeterminanthrc) + (mdr_b_unbounded_minorminornonzeroevaluationdeterminanthrc)) * S ((mdr_a_unbounded_minorminornonzeroevaluationdeterminanthrc) + (mdr_b_unbounded_minorminornonzeroevaluationdeterminanthrc)) + ((mdr_b_unbounded_minorminornonzeroevaluationdeterminanthrc) + (mdr_b_unbounded_minorminornonzeroevaluationdeterminanthrc))) /\ ((mdr_e_unbounded_minorminornonzeroevaluationdeterminanthrc = ((mdr_p_unbounded_minorminornonzeroevaluationdeterminanth) + (mdr_n_unbounded_minorminornonzeroevaluationdeterminanth)) * S ((mdr_p_unbounded_minorminornonzeroevaluationdeterminanth) + (mdr_n_unbounded_minorminornonzeroevaluationdeterminanth)) + ((mdr_n_unbounded_minorminornonzeroevaluationdeterminanth) + (mdr_n_unbounded_minorminornonzeroevaluationdeterminanth))) /\ ((mdr_f_unbounded_minorminornonzeroevaluationdeterminanthrc = ((mdr_nc_unbounded_minorminornonzeroevaluationdeterminanth) + (mdr_e_unbounded_minorminornonzeroevaluationdeterminanthrc)) * S ((mdr_nc_unbounded_minorminornonzeroevaluationdeterminanth) + (mdr_e_unbounded_minorminornonzeroevaluationdeterminanthrc)) + ((mdr_e_unbounded_minorminornonzeroevaluationdeterminanthrc) + (mdr_e_unbounded_minorminornonzeroevaluationdeterminanthrc))) /\ ((mdr_z_unbounded_minorminornonzeroevaluationdeterminanthr) = ((mdr_c_unbounded_minorminornonzeroevaluationdeterminanthrc) + (mdr_f_unbounded_minorminornonzeroevaluationdeterminanthrc)) * S ((mdr_c_unbounded_minorminornonzeroevaluationdeterminanthrc) + (mdr_f_unbounded_minorminornonzeroevaluationdeterminanthrc)) + ((mdr_f_unbounded_minorminornonzeroevaluationdeterminanthrc) + (mdr_f_unbounded_minorminornonzeroevaluationdeterminanthrc))))))))) /\ (((exists ff_h_mdr_unbounded_minorminornonzeroevaluationdeterminanthrb. ff_h_mdr_unbounded_minorminornonzeroevaluationdeterminanthrb + S (mdr_z_unbounded_minorminornonzeroevaluationdeterminanthr) = S ((S (mdr_i_unbounded_minorminornonzeroevaluationdeterminanth)) * mdr_c_unbounded_minorminornonzeroevaluationdeterminant)) /\ exists ff_q_mdr_unbounded_minorminornonzeroevaluationdeterminanthrb. mdr_b_unbounded_minorminornonzeroevaluationdeterminant = ff_q_mdr_unbounded_minorminornonzeroevaluationdeterminanthrb * S ((S (mdr_i_unbounded_minorminornonzeroevaluationdeterminanth)) * mdr_c_unbounded_minorminornonzeroevaluationdeterminant) + (mdr_z_unbounded_minorminornonzeroevaluationdeterminanthr))))) /\ (((((mdr_d_unbounded_minorminornonzeroevaluationdeterminanth) = 0) /\ (((mdr_p_unbounded_minorminornonzeroevaluationdeterminanth) = 1) /\ ((mdr_n_unbounded_minorminornonzeroevaluationdeterminanth) = 0))) \/ exists mdr_q_unbounded_minorminornonzeroevaluationdeterminanths mdr_eb_unbounded_minorminornonzeroevaluationdeterminanths mdr_ec_unbounded_minorminornonzeroevaluationdeterminanths mdr_fb_unbounded_minorminornonzeroevaluationdeterminanths mdr_fc_unbounded_minorminornonzeroevaluationdeterminanths. (((mdr_d_unbounded_minorminornonzeroevaluationdeterminanth) = S (mdr_q_unbounded_minorminornonzeroevaluationdeterminanths)) /\ ((forall mdr_j_unbounded_minorminornonzeroevaluationdeterminanthsc. (exists mdr_gap_unbounded_minorminornonzeroevaluationdeterminanthscj. mdr_gap_unbounded_minorminornonzeroevaluationdeterminanthscj + S (mdr_j_unbounded_minorminornonzeroevaluationdeterminanthsc) = (S (mdr_q_unbounded_minorminornonzeroevaluationdeterminanths))) -> exists mdr_i_unbounded_minorminornonzeroevaluationdeterminanthsc mdr_up_unbounded_minorminornonzeroevaluationdeterminanthsc mdr_us_unbounded_minorminornonzeroevaluationdeterminanthsc mdr_un_unbounded_minorminornonzeroevaluationdeterminanthsc mdr_ut_unbounded_minorminornonzeroevaluationdeterminanthsc mdr_p_unbounded_minorminornonzeroevaluationdeterminanthsc mdr_n_unbounded_minorminornonzeroevaluationdeterminanthsc. ((exists mdr_gap_unbounded_minorminornonzeroevaluationdeterminanthsci. mdr_gap_unbounded_minorminornonzeroevaluationdeterminanthsci + S (mdr_i_unbounded_minorminornonzeroevaluationdeterminanthsc) = (mdr_i_unbounded_minorminornonzeroevaluationdeterminanth)) /\ ((exists mdr_z_unbounded_minorminornonzeroevaluationdeterminanthscr. ((exists mdr_a_unbounded_minorminornonzeroevaluationdeterminanthscrc mdr_b_unbounded_minorminornonzeroevaluationdeterminanthscrc mdr_c_unbounded_minorminornonzeroevaluationdeterminanthscrc mdr_e_unbounded_minorminornonzeroevaluationdeterminanthscrc mdr_f_unbounded_minorminornonzeroevaluationdeterminanthscrc. ((mdr_a_unbounded_minorminornonzeroevaluationdeterminanthscrc = ((mdr_q_unbounded_minorminornonzeroevaluationdeterminanths) + (mdr_up_unbounded_minorminornonzeroevaluationdeterminanthsc)) * S ((mdr_q_unbounded_minorminornonzeroevaluationdeterminanths) + (mdr_up_unbounded_minorminornonzeroevaluationdeterminanthsc)) + ((mdr_up_unbounded_minorminornonzeroevaluationdeterminanthsc) + (mdr_up_unbounded_minorminornonzeroevaluationdeterminanthsc))) /\ ((mdr_b_unbounded_minorminornonzeroevaluationdeterminanthscrc = ((mdr_us_unbounded_minorminornonzeroevaluationdeterminanthsc) + (mdr_un_unbounded_minorminornonzeroevaluationdeterminanthsc)) * S ((mdr_us_unbounded_minorminornonzeroevaluationdeterminanthsc) + (mdr_un_unbounded_minorminornonzeroevaluationdeterminanthsc)) + ((mdr_un_unbounded_minorminornonzeroevaluationdeterminanthsc) + (mdr_un_unbounded_minorminornonzeroevaluationdeterminanthsc))) /\ ((mdr_c_unbounded_minorminornonzeroevaluationdeterminanthscrc = ((mdr_a_unbounded_minorminornonzeroevaluationdeterminanthscrc) + (mdr_b_unbounded_minorminornonzeroevaluationdeterminanthscrc)) * S ((mdr_a_unbounded_minorminornonzeroevaluationdeterminanthscrc) + (mdr_b_unbounded_minorminornonzeroevaluationdeterminanthscrc)) + ((mdr_b_unbounded_minorminornonzeroevaluationdeterminanthscrc) + (mdr_b_unbounded_minorminornonzeroevaluationdeterminanthscrc))) /\ ((mdr_e_unbounded_minorminornonzeroevaluationdeterminanthscrc = ((mdr_p_unbounded_minorminornonzeroevaluationdeterminanthsc) + (mdr_n_unbounded_minorminornonzeroevaluationdeterminanthsc)) * S ((mdr_p_unbounded_minorminornonzeroevaluationdeterminanthsc) + (mdr_n_unbounded_minorminornonzeroevaluationdeterminanthsc)) + ((mdr_n_unbounded_minorminornonzeroevaluationdeterminanthsc) + (mdr_n_unbounded_minorminornonzeroevaluationdeterminanthsc))) /\ ((mdr_f_unbounded_minorminornonzeroevaluationdeterminanthscrc = ((mdr_ut_unbounded_minorminornonzeroevaluationdeterminanthsc) + (mdr_e_unbounded_minorminornonzeroevaluationdeterminanthscrc)) * S ((mdr_ut_unbounded_minorminornonzeroevaluationdeterminanthsc) + (mdr_e_unbounded_minorminornonzeroevaluationdeterminanthscrc)) + ((mdr_e_unbounded_minorminornonzeroevaluationdeterminanthscrc) + (mdr_e_unbounded_minorminornonzeroevaluationdeterminanthscrc))) /\ ((mdr_z_unbounded_minorminornonzeroevaluationdeterminanthscr) = ((mdr_c_unbounded_minorminornonzeroevaluationdeterminanthscrc) + (mdr_f_unbounded_minorminornonzeroevaluationdeterminanthscrc)) * S ((mdr_c_unbounded_minorminornonzeroevaluationdeterminanthscrc) + (mdr_f_unbounded_minorminornonzeroevaluationdeterminanthscrc)) + ((mdr_f_unbounded_minorminornonzeroevaluationdeterminanthscrc) + (mdr_f_unbounded_minorminornonzeroevaluationdeterminanthscrc))))))))) /\ (((exists ff_h_mdr_unbounded_minorminornonzeroevaluationdeterminanthscrb. ff_h_mdr_unbounded_minorminornonzeroevaluationdeterminanthscrb + S (mdr_z_unbounded_minorminornonzeroevaluationdeterminanthscr) = S ((S (mdr_i_unbounded_minorminornonzeroevaluationdeterminanthsc)) * mdr_c_unbounded_minorminornonzeroevaluationdeterminant)) /\ exists ff_q_mdr_unbounded_minorminornonzeroevaluationdeterminanthscrb. mdr_b_unbounded_minorminornonzeroevaluationdeterminant = ff_q_mdr_unbounded_minorminornonzeroevaluationdeterminanthscrb * S ((S (mdr_i_unbounded_minorminornonzeroevaluationdeterminanthsc)) * mdr_c_unbounded_minorminornonzeroevaluationdeterminant) + (mdr_z_unbounded_minorminornonzeroevaluationdeterminanthscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_positive. (exists ff_gap_mdm_lt_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_positive_index_bound. ff_gap_mdm_lt_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_positive) = ((mdr_q_unbounded_minorminornonzeroevaluationdeterminanths) * (mdr_q_unbounded_minorminornonzeroevaluationdeterminanths))) -> exists ff_row_mdm_prefix_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_positive ff_column_mdm_prefix_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_positive ff_value_mdm_prefix_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_positive. (ff_index_mdm_prefix_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_positive = (mdr_q_unbounded_minorminornonzeroevaluationdeterminanths) * ff_row_mdm_prefix_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_positive + ff_column_mdm_prefix_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_positive /\ ((exists ff_gap_mdm_lt_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_positive_column_bound. ff_gap_mdm_lt_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_positive) = (mdr_q_unbounded_minorminornonzeroevaluationdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_positive_cell ff_column_mdm_cell_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_positive_cell = ff_row_mdm_prefix_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_positive_cell_row_after. ff_gap_mdm_le_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_positive)) /\ ff_row_mdm_cell_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_positive_cell = S ff_row_mdm_prefix_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_positive) = (mdr_j_unbounded_minorminornonzeroevaluationdeterminanthsc)) /\ ff_column_mdm_cell_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_positive_cell = ff_column_mdm_prefix_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_positive_cell_column_after. ff_gap_mdm_le_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_positive_cell_column_after + (mdr_j_unbounded_minorminornonzeroevaluationdeterminanthsc) = (ff_column_mdm_prefix_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_positive)) /\ ff_column_mdm_cell_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_positive_cell = S ff_column_mdm_prefix_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_positive))) /\ (((exists ff_h_mdm_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_positive_cell_source. ff_h_mdm_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_positive) = S ((S ((ff_row_mdm_cell_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_positive_cell) * (S (mdr_q_unbounded_minorminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_positive_cell))) * mdr_pc_unbounded_minorminornonzeroevaluationdeterminanth)) /\ exists ff_q_mdm_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_positive_cell_source. mdr_pb_unbounded_minorminornonzeroevaluationdeterminanth = ff_q_mdm_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_positive_cell) * (S (mdr_q_unbounded_minorminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_positive_cell))) * mdr_pc_unbounded_minorminornonzeroevaluationdeterminanth) + (ff_value_mdm_prefix_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_positive)))))) /\ (((exists ff_h_mdm_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_positive_target. ff_h_mdm_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_positive_target + S (ff_value_mdm_prefix_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_positive) = S ((S (ff_index_mdm_prefix_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_positive)) * mdr_us_unbounded_minorminornonzeroevaluationdeterminanthsc)) /\ exists ff_q_mdm_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_positive_target. mdr_up_unbounded_minorminornonzeroevaluationdeterminanthsc = ff_q_mdm_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_positive)) * mdr_us_unbounded_minorminornonzeroevaluationdeterminanthsc) + (ff_value_mdm_prefix_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_negative. (exists ff_gap_mdm_lt_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_negative_index_bound. ff_gap_mdm_lt_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_negative) = ((mdr_q_unbounded_minorminornonzeroevaluationdeterminanths) * (mdr_q_unbounded_minorminornonzeroevaluationdeterminanths))) -> exists ff_row_mdm_prefix_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_negative ff_column_mdm_prefix_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_negative ff_value_mdm_prefix_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_negative. (ff_index_mdm_prefix_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_negative = (mdr_q_unbounded_minorminornonzeroevaluationdeterminanths) * ff_row_mdm_prefix_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_negative + ff_column_mdm_prefix_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_negative /\ ((exists ff_gap_mdm_lt_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_negative_column_bound. ff_gap_mdm_lt_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_negative) = (mdr_q_unbounded_minorminornonzeroevaluationdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_negative_cell ff_column_mdm_cell_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_negative_cell = ff_row_mdm_prefix_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_negative_cell_row_after. ff_gap_mdm_le_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_negative)) /\ ff_row_mdm_cell_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_negative_cell = S ff_row_mdm_prefix_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_negative) = (mdr_j_unbounded_minorminornonzeroevaluationdeterminanthsc)) /\ ff_column_mdm_cell_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_negative_cell = ff_column_mdm_prefix_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_negative_cell_column_after. ff_gap_mdm_le_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_negative_cell_column_after + (mdr_j_unbounded_minorminornonzeroevaluationdeterminanthsc) = (ff_column_mdm_prefix_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_negative)) /\ ff_column_mdm_cell_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_negative_cell = S ff_column_mdm_prefix_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_negative))) /\ (((exists ff_h_mdm_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_negative_cell_source. ff_h_mdm_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_negative) = S ((S ((ff_row_mdm_cell_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_negative_cell) * (S (mdr_q_unbounded_minorminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_negative_cell))) * mdr_nc_unbounded_minorminornonzeroevaluationdeterminanth)) /\ exists ff_q_mdm_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_negative_cell_source. mdr_nb_unbounded_minorminornonzeroevaluationdeterminanth = ff_q_mdm_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_negative_cell) * (S (mdr_q_unbounded_minorminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_negative_cell))) * mdr_nc_unbounded_minorminornonzeroevaluationdeterminanth) + (ff_value_mdm_prefix_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_negative)))))) /\ (((exists ff_h_mdm_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_negative_target. ff_h_mdm_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_negative_target + S (ff_value_mdm_prefix_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_negative) = S ((S (ff_index_mdm_prefix_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_negative)) * mdr_ut_unbounded_minorminornonzeroevaluationdeterminanthsc)) /\ exists ff_q_mdm_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_negative_target. mdr_un_unbounded_minorminornonzeroevaluationdeterminanthsc = ff_q_mdm_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_negative)) * mdr_ut_unbounded_minorminornonzeroevaluationdeterminanthsc) + (ff_value_mdm_prefix_mdr_unbounded_minorminornonzeroevaluationdeterminanthscm_negative))))))))) /\ ((((exists ff_h_mdr_unbounded_minorminornonzeroevaluationdeterminanthscp. ff_h_mdr_unbounded_minorminornonzeroevaluationdeterminanthscp + S (mdr_p_unbounded_minorminornonzeroevaluationdeterminanthsc) = S ((S (mdr_j_unbounded_minorminornonzeroevaluationdeterminanthsc)) * mdr_ec_unbounded_minorminornonzeroevaluationdeterminanths)) /\ exists ff_q_mdr_unbounded_minorminornonzeroevaluationdeterminanthscp. mdr_eb_unbounded_minorminornonzeroevaluationdeterminanths = ff_q_mdr_unbounded_minorminornonzeroevaluationdeterminanthscp * S ((S (mdr_j_unbounded_minorminornonzeroevaluationdeterminanthsc)) * mdr_ec_unbounded_minorminornonzeroevaluationdeterminanths) + (mdr_p_unbounded_minorminornonzeroevaluationdeterminanthsc))) /\ (((exists ff_h_mdr_unbounded_minorminornonzeroevaluationdeterminanthscn. ff_h_mdr_unbounded_minorminornonzeroevaluationdeterminanthscn + S (mdr_n_unbounded_minorminornonzeroevaluationdeterminanthsc) = S ((S (mdr_j_unbounded_minorminornonzeroevaluationdeterminanthsc)) * mdr_fc_unbounded_minorminornonzeroevaluationdeterminanths)) /\ exists ff_q_mdr_unbounded_minorminornonzeroevaluationdeterminanthscn. mdr_fb_unbounded_minorminornonzeroevaluationdeterminanths = ff_q_mdr_unbounded_minorminornonzeroevaluationdeterminanthscn * S ((S (mdr_j_unbounded_minorminornonzeroevaluationdeterminanthsc)) * mdr_fc_unbounded_minorminornonzeroevaluationdeterminanths) + (mdr_n_unbounded_minorminornonzeroevaluationdeterminanthsc)))))))) /\ (exists ff_ub_mce_fold_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf ff_uc_mce_fold_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf ff_vb_mce_fold_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf ff_vc_mce_fold_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf. ((forall ff_index_mce_alternating_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix. (exists ff_gap_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix_index. ff_gap_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix_index + S (ff_index_mce_alternating_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix) = (S (mdr_q_unbounded_minorminornonzeroevaluationdeterminanths))) -> exists ff_ap_mce_alternating_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix ff_an_mce_alternating_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix ff_bp_mce_alternating_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix ff_bn_mce_alternating_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix ff_p_mce_alternating_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix ff_n_mce_alternating_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix. ((((exists ff_h_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix_ap. ff_h_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix_ap + S (ff_ap_mce_alternating_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix)) * mdr_pc_unbounded_minorminornonzeroevaluationdeterminanth)) /\ exists ff_q_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix_ap. mdr_pb_unbounded_minorminornonzeroevaluationdeterminanth = ff_q_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix)) * mdr_pc_unbounded_minorminornonzeroevaluationdeterminanth) + (ff_ap_mce_alternating_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix_an. ff_h_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix_an + S (ff_an_mce_alternating_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix)) * mdr_nc_unbounded_minorminornonzeroevaluationdeterminanth)) /\ exists ff_q_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix_an. mdr_nb_unbounded_minorminornonzeroevaluationdeterminanth = ff_q_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix)) * mdr_nc_unbounded_minorminornonzeroevaluationdeterminanth) + (ff_an_mce_alternating_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix_bp. ff_h_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix_bp + S (ff_bp_mce_alternating_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix)) * mdr_ec_unbounded_minorminornonzeroevaluationdeterminanths)) /\ exists ff_q_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix_bp. mdr_eb_unbounded_minorminornonzeroevaluationdeterminanths = ff_q_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix)) * mdr_ec_unbounded_minorminornonzeroevaluationdeterminanths) + (ff_bp_mce_alternating_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix_bn. ff_h_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix_bn + S (ff_bn_mce_alternating_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix)) * mdr_fc_unbounded_minorminornonzeroevaluationdeterminanths)) /\ exists ff_q_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix_bn. mdr_fb_unbounded_minorminornonzeroevaluationdeterminanths = ff_q_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix)) * mdr_fc_unbounded_minorminornonzeroevaluationdeterminanths) + (ff_bn_mce_alternating_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix_positive. ff_h_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix_positive + S (ff_p_mce_alternating_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix_positive. ff_ub_mce_fold_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf) + (ff_p_mce_alternating_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix_negative. ff_h_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix_negative + S (ff_n_mce_alternating_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix_negative. ff_vb_mce_fold_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf) + (ff_n_mce_alternating_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix))) /\ (((exists ff_even_mce_term_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix = 2 * ff_even_mce_term_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix_term) /\ (ff_p_mce_alternating_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix = 2 * ff_odd_mce_term_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_positive ff_v_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_positive. ((((exists ff_h_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_positive_start. ff_h_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_positive_start. ff_u_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_positive_start * S ((S (0)) * ff_v_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_positive_terminal. ff_h_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_positive_terminal + S (mdr_p_unbounded_minorminornonzeroevaluationdeterminanth) = S ((S ((S (mdr_q_unbounded_minorminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_positive_terminal. ff_u_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_positive_terminal * S ((S ((S (mdr_q_unbounded_minorminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_positive) + (mdr_p_unbounded_minorminornonzeroevaluationdeterminanth))) /\ forall ff_i_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_positive. (exists ff_lt_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_positive_bound. ff_lt_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_positive_bound + S ff_i_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_positive = (S (mdr_q_unbounded_minorminornonzeroevaluationdeterminanths))) -> exists ff_a_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_positive ff_r_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_positive ff_s_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_positive. ((((exists ff_h_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_positive_summand. ff_h_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_positive_summand + S (ff_a_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_positive_summand. ff_ub_mce_fold_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_positive_summand * S ((S (ff_i_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf) + (ff_a_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_positive_partial. ff_h_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_positive_partial + S (ff_r_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_positive_partial. ff_u_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_positive_partial * S ((S (ff_i_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_positive) + (ff_r_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_positive_successor. ff_h_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_positive_successor + S (ff_s_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_positive) = S ((S (S ff_i_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_positive_successor. ff_u_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_positive_successor * S ((S (S ff_i_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_positive) + (ff_s_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_positive))) /\ ff_s_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_positive = ff_r_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_positive + ff_a_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_positive)))))) /\ (exists ff_u_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_negative ff_v_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_negative. ((((exists ff_h_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_negative_start. ff_h_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_negative_start. ff_u_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_negative_start * S ((S (0)) * ff_v_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_negative_terminal. ff_h_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_negative_terminal + S (mdr_n_unbounded_minorminornonzeroevaluationdeterminanth) = S ((S ((S (mdr_q_unbounded_minorminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_negative_terminal. ff_u_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_negative_terminal * S ((S ((S (mdr_q_unbounded_minorminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_negative) + (mdr_n_unbounded_minorminornonzeroevaluationdeterminanth))) /\ forall ff_i_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_negative. (exists ff_lt_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_negative_bound. ff_lt_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_negative_bound + S ff_i_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_negative = (S (mdr_q_unbounded_minorminornonzeroevaluationdeterminanths))) -> exists ff_a_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_negative ff_r_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_negative ff_s_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_negative. ((((exists ff_h_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_negative_summand. ff_h_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_negative_summand + S (ff_a_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_negative_summand. ff_vb_mce_fold_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_negative_summand * S ((S (ff_i_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf) + (ff_a_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_negative_partial. ff_h_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_negative_partial + S (ff_r_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_negative_partial. ff_u_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_negative_partial * S ((S (ff_i_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_negative) + (ff_r_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_negative_successor. ff_h_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_negative_successor + S (ff_s_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_negative) = S ((S (S ff_i_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_negative_successor. ff_u_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_negative_successor * S ((S (S ff_i_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_negative) + (ff_s_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_negative))) /\ ff_s_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_negative = ff_r_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_negative + ff_a_mce_mdr_unbounded_minorminornonzeroevaluationdeterminanthsf_negative))))))))))))))) /\ ((exists mdr_gap_unbounded_minorminornonzeroevaluationdeterminanti. mdr_gap_unbounded_minorminornonzeroevaluationdeterminanti + S (mdr_i_unbounded_minorminornonzeroevaluationdeterminant) = (mdr_l_unbounded_minorminornonzeroevaluationdeterminant)) /\ (exists mdr_z_unbounded_minorminornonzeroevaluationdeterminantr. ((exists mdr_a_unbounded_minorminornonzeroevaluationdeterminantrc mdr_b_unbounded_minorminornonzeroevaluationdeterminantrc mdr_c_unbounded_minorminornonzeroevaluationdeterminantrc mdr_e_unbounded_minorminornonzeroevaluationdeterminantrc mdr_f_unbounded_minorminornonzeroevaluationdeterminantrc. ((mdr_a_unbounded_minorminornonzeroevaluationdeterminantrc = ((q) + (mdr_ub_unbounded_minorminornonzeroevaluation)) * S ((q) + (mdr_ub_unbounded_minorminornonzeroevaluation)) + ((mdr_ub_unbounded_minorminornonzeroevaluation) + (mdr_ub_unbounded_minorminornonzeroevaluation))) /\ ((mdr_b_unbounded_minorminornonzeroevaluationdeterminantrc = ((mdr_uc_unbounded_minorminornonzeroevaluation) + (mdr_vb_unbounded_minorminornonzeroevaluation)) * S ((mdr_uc_unbounded_minorminornonzeroevaluation) + (mdr_vb_unbounded_minorminornonzeroevaluation)) + ((mdr_vb_unbounded_minorminornonzeroevaluation) + (mdr_vb_unbounded_minorminornonzeroevaluation))) /\ ((mdr_c_unbounded_minorminornonzeroevaluationdeterminantrc = ((mdr_a_unbounded_minorminornonzeroevaluationdeterminantrc) + (mdr_b_unbounded_minorminornonzeroevaluationdeterminantrc)) * S ((mdr_a_unbounded_minorminornonzeroevaluationdeterminantrc) + (mdr_b_unbounded_minorminornonzeroevaluationdeterminantrc)) + ((mdr_b_unbounded_minorminornonzeroevaluationdeterminantrc) + (mdr_b_unbounded_minorminornonzeroevaluationdeterminantrc))) /\ ((mdr_e_unbounded_minorminornonzeroevaluationdeterminantrc = ((mdr_p_unbounded_minorminornonzero) + (mdr_n_unbounded_minorminornonzero)) * S ((mdr_p_unbounded_minorminornonzero) + (mdr_n_unbounded_minorminornonzero)) + ((mdr_n_unbounded_minorminornonzero) + (mdr_n_unbounded_minorminornonzero))) /\ ((mdr_f_unbounded_minorminornonzeroevaluationdeterminantrc = ((mdr_vc_unbounded_minorminornonzeroevaluation) + (mdr_e_unbounded_minorminornonzeroevaluationdeterminantrc)) * S ((mdr_vc_unbounded_minorminornonzeroevaluation) + (mdr_e_unbounded_minorminornonzeroevaluationdeterminantrc)) + ((mdr_e_unbounded_minorminornonzeroevaluationdeterminantrc) + (mdr_e_unbounded_minorminornonzeroevaluationdeterminantrc))) /\ ((mdr_z_unbounded_minorminornonzeroevaluationdeterminantr) = ((mdr_c_unbounded_minorminornonzeroevaluationdeterminantrc) + (mdr_f_unbounded_minorminornonzeroevaluationdeterminantrc)) * S ((mdr_c_unbounded_minorminornonzeroevaluationdeterminantrc) + (mdr_f_unbounded_minorminornonzeroevaluationdeterminantrc)) + ((mdr_f_unbounded_minorminornonzeroevaluationdeterminantrc) + (mdr_f_unbounded_minorminornonzeroevaluationdeterminantrc))))))))) /\ (((exists ff_h_mdr_unbounded_minorminornonzeroevaluationdeterminantrb. ff_h_mdr_unbounded_minorminornonzeroevaluationdeterminantrb + S (mdr_z_unbounded_minorminornonzeroevaluationdeterminantr) = S ((S (mdr_i_unbounded_minorminornonzeroevaluationdeterminant)) * mdr_c_unbounded_minorminornonzeroevaluationdeterminant)) /\ exists ff_q_mdr_unbounded_minorminornonzeroevaluationdeterminantrb. mdr_b_unbounded_minorminornonzeroevaluationdeterminant = ff_q_mdr_unbounded_minorminornonzeroevaluationdeterminantrb * S ((S (mdr_i_unbounded_minorminornonzeroevaluationdeterminant)) * mdr_c_unbounded_minorminornonzeroevaluationdeterminant) + (mdr_z_unbounded_minorminornonzeroevaluationdeterminantr)))))))))) /\ (~(mdr_p_unbounded_minorminornonzero = mdr_n_unbounded_minorminornonzero)))))))) -> (exists mdr_a_bounded_minorrows. (((exists mdr_gap_bounded_minorrowsbound. mdr_gap_bounded_minorrowsbound + S (mdr_a_bounded_minorrows) = (R)) /\ (exists mdr_a_bounded_minorrowcolumns. (((exists mdr_gap_bounded_minorrowcolumnsbound. mdr_gap_bounded_minorrowcolumnsbound + S (mdr_a_bounded_minorrowcolumns) = (C)) /\ (((((forall fom_index_mrf_bounded_minorrowminorrowsbound. (exists fom_gap_mrf_bounded_minorrowminorrowsbound_index_bound. fom_gap_mrf_bounded_minorrowminorrowsbound_index_bound + S (fom_index_mrf_bounded_minorrowminorrowsbound) = q) -> exists fom_value_mrf_bounded_minorrowminorrowsbound. ((((exists fom_beta_height_mrf_bounded_minorrowminorrowsbound_entry. fom_beta_height_mrf_bounded_minorrowminorrowsbound_entry + S (fom_value_mrf_bounded_minorrowminorrowsbound) = S ((S (fom_index_mrf_bounded_minorrowminorrowsbound)) * rc)) /\ exists fom_beta_quotient_mrf_bounded_minorrowminorrowsbound_entry. mdr_a_bounded_minorrows = fom_beta_quotient_mrf_bounded_minorrowminorrowsbound_entry * S ((S (fom_index_mrf_bounded_minorrowminorrowsbound)) * rc) + (fom_value_mrf_bounded_minorrowminorrowsbound))) /\ (exists fom_gap_mrf_bounded_minorrowminorrowsbound_value_bound. fom_gap_mrf_bounded_minorrowminorrowsbound_value_bound + S (fom_value_mrf_bounded_minorrowminorrowsbound) = r))) /\ (forall mdr_i_bounded_minorrowminorrowsdistinct mdr_j_bounded_minorrowminorrowsdistinct mdr_a_bounded_minorrowminorrowsdistinct. (exists mdr_gap_bounded_minorrowminorrowsdistincti. mdr_gap_bounded_minorrowminorrowsdistincti + S (mdr_i_bounded_minorrowminorrowsdistinct) = (q)) -> (exists mdr_gap_bounded_minorrowminorrowsdistinctj. mdr_gap_bounded_minorrowminorrowsdistinctj + S (mdr_j_bounded_minorrowminorrowsdistinct) = (q)) -> (((exists ff_h_mdr_bounded_minorrowminorrowsdistinctfirst. ff_h_mdr_bounded_minorrowminorrowsdistinctfirst + S (mdr_a_bounded_minorrowminorrowsdistinct) = S ((S (mdr_i_bounded_minorrowminorrowsdistinct)) * rc)) /\ exists ff_q_mdr_bounded_minorrowminorrowsdistinctfirst. mdr_a_bounded_minorrows = ff_q_mdr_bounded_minorrowminorrowsdistinctfirst * S ((S (mdr_i_bounded_minorrowminorrowsdistinct)) * rc) + (mdr_a_bounded_minorrowminorrowsdistinct))) -> (((exists ff_h_mdr_bounded_minorrowminorrowsdistinctsecond. ff_h_mdr_bounded_minorrowminorrowsdistinctsecond + S (mdr_a_bounded_minorrowminorrowsdistinct) = S ((S (mdr_j_bounded_minorrowminorrowsdistinct)) * rc)) /\ exists ff_q_mdr_bounded_minorrowminorrowsdistinctsecond. mdr_a_bounded_minorrows = ff_q_mdr_bounded_minorrowminorrowsdistinctsecond * S ((S (mdr_j_bounded_minorrowminorrowsdistinct)) * rc) + (mdr_a_bounded_minorrowminorrowsdistinct))) -> mdr_i_bounded_minorrowminorrowsdistinct = mdr_j_bounded_minorrowminorrowsdistinct))) /\ ((((forall fom_index_mrf_bounded_minorrowminorcolumnsbound. (exists fom_gap_mrf_bounded_minorrowminorcolumnsbound_index_bound. fom_gap_mrf_bounded_minorrowminorcolumnsbound_index_bound + S (fom_index_mrf_bounded_minorrowminorcolumnsbound) = q) -> exists fom_value_mrf_bounded_minorrowminorcolumnsbound. ((((exists fom_beta_height_mrf_bounded_minorrowminorcolumnsbound_entry. fom_beta_height_mrf_bounded_minorrowminorcolumnsbound_entry + S (fom_value_mrf_bounded_minorrowminorcolumnsbound) = S ((S (fom_index_mrf_bounded_minorrowminorcolumnsbound)) * cc)) /\ exists fom_beta_quotient_mrf_bounded_minorrowminorcolumnsbound_entry. mdr_a_bounded_minorrowcolumns = fom_beta_quotient_mrf_bounded_minorrowminorcolumnsbound_entry * S ((S (fom_index_mrf_bounded_minorrowminorcolumnsbound)) * cc) + (fom_value_mrf_bounded_minorrowminorcolumnsbound))) /\ (exists fom_gap_mrf_bounded_minorrowminorcolumnsbound_value_bound. fom_gap_mrf_bounded_minorrowminorcolumnsbound_value_bound + S (fom_value_mrf_bounded_minorrowminorcolumnsbound) = w))) /\ (forall mdr_i_bounded_minorrowminorcolumnsdistinct mdr_j_bounded_minorrowminorcolumnsdistinct mdr_a_bounded_minorrowminorcolumnsdistinct. (exists mdr_gap_bounded_minorrowminorcolumnsdistincti. mdr_gap_bounded_minorrowminorcolumnsdistincti + S (mdr_i_bounded_minorrowminorcolumnsdistinct) = (q)) -> (exists mdr_gap_bounded_minorrowminorcolumnsdistinctj. mdr_gap_bounded_minorrowminorcolumnsdistinctj + S (mdr_j_bounded_minorrowminorcolumnsdistinct) = (q)) -> (((exists ff_h_mdr_bounded_minorrowminorcolumnsdistinctfirst. ff_h_mdr_bounded_minorrowminorcolumnsdistinctfirst + S (mdr_a_bounded_minorrowminorcolumnsdistinct) = S ((S (mdr_i_bounded_minorrowminorcolumnsdistinct)) * cc)) /\ exists ff_q_mdr_bounded_minorrowminorcolumnsdistinctfirst. mdr_a_bounded_minorrowcolumns = ff_q_mdr_bounded_minorrowminorcolumnsdistinctfirst * S ((S (mdr_i_bounded_minorrowminorcolumnsdistinct)) * cc) + (mdr_a_bounded_minorrowminorcolumnsdistinct))) -> (((exists ff_h_mdr_bounded_minorrowminorcolumnsdistinctsecond. ff_h_mdr_bounded_minorrowminorcolumnsdistinctsecond + S (mdr_a_bounded_minorrowminorcolumnsdistinct) = S ((S (mdr_j_bounded_minorrowminorcolumnsdistinct)) * cc)) /\ exists ff_q_mdr_bounded_minorrowminorcolumnsdistinctsecond. mdr_a_bounded_minorrowcolumns = ff_q_mdr_bounded_minorrowminorcolumnsdistinctsecond * S ((S (mdr_j_bounded_minorrowminorcolumnsdistinct)) * cc) + (mdr_a_bounded_minorrowminorcolumnsdistinct))) -> mdr_i_bounded_minorrowminorcolumnsdistinct = mdr_j_bounded_minorrowminorcolumnsdistinct))) /\ (exists mdr_p_bounded_minorrowminornonzero mdr_n_bounded_minorrowminornonzero. ((exists mdr_ub_bounded_minorrowminornonzeroevaluation mdr_uc_bounded_minorrowminornonzeroevaluation mdr_vb_bounded_minorrowminornonzeroevaluation mdr_vc_bounded_minorrowminornonzeroevaluation. ((((forall mdr_i_bounded_minorrowminornonzeroevaluationmatrixpositive. (exists mdr_gap_bounded_minorrowminornonzeroevaluationmatrixpositivebound. mdr_gap_bounded_minorrowminornonzeroevaluationmatrixpositivebound + S (mdr_i_bounded_minorrowminornonzeroevaluationmatrixpositive) = ((q) * (q))) -> exists mdr_a_bounded_minorrowminornonzeroevaluationmatrixpositive. (((exists mdr_r_bounded_minorrowminornonzeroevaluationmatrixpositivepoint mdr_s_bounded_minorrowminornonzeroevaluationmatrixpositivepoint mdr_u_bounded_minorrowminornonzeroevaluationmatrixpositivepoint mdr_v_bounded_minorrowminornonzeroevaluationmatrixpositivepoint. ((mdr_i_bounded_minorrowminornonzeroevaluationmatrixpositive = (q) * mdr_r_bounded_minorrowminornonzeroevaluationmatrixpositivepoint + mdr_s_bounded_minorrowminornonzeroevaluationmatrixpositivepoint) /\ ((exists mdr_gap_bounded_minorrowminornonzeroevaluationmatrixpositivepointcolumn. mdr_gap_bounded_minorrowminornonzeroevaluationmatrixpositivepointcolumn + S (mdr_s_bounded_minorrowminornonzeroevaluationmatrixpositivepoint) = (q)) /\ ((((exists ff_h_mdr_bounded_minorrowminornonzeroevaluationmatrixpositivepointrow_index. ff_h_mdr_bounded_minorrowminornonzeroevaluationmatrixpositivepointrow_index + S (mdr_u_bounded_minorrowminornonzeroevaluationmatrixpositivepoint) = S ((S (mdr_r_bounded_minorrowminornonzeroevaluationmatrixpositivepoint)) * rc)) /\ exists ff_q_mdr_bounded_minorrowminornonzeroevaluationmatrixpositivepointrow_index. mdr_a_bounded_minorrows = ff_q_mdr_bounded_minorrowminornonzeroevaluationmatrixpositivepointrow_index * S ((S (mdr_r_bounded_minorrowminornonzeroevaluationmatrixpositivepoint)) * rc) + (mdr_u_bounded_minorrowminornonzeroevaluationmatrixpositivepoint))) /\ ((((exists ff_h_mdr_bounded_minorrowminornonzeroevaluationmatrixpositivepointcolumn_index. ff_h_mdr_bounded_minorrowminornonzeroevaluationmatrixpositivepointcolumn_index + S (mdr_v_bounded_minorrowminornonzeroevaluationmatrixpositivepoint) = S ((S (mdr_s_bounded_minorrowminornonzeroevaluationmatrixpositivepoint)) * cc)) /\ exists ff_q_mdr_bounded_minorrowminornonzeroevaluationmatrixpositivepointcolumn_index. mdr_a_bounded_minorrowcolumns = ff_q_mdr_bounded_minorrowminornonzeroevaluationmatrixpositivepointcolumn_index * S ((S (mdr_s_bounded_minorrowminornonzeroevaluationmatrixpositivepoint)) * cc) + (mdr_v_bounded_minorrowminornonzeroevaluationmatrixpositivepoint))) /\ (((exists ff_h_mdr_bounded_minorrowminornonzeroevaluationmatrixpositivepointsource. ff_h_mdr_bounded_minorrowminornonzeroevaluationmatrixpositivepointsource + S (mdr_a_bounded_minorrowminornonzeroevaluationmatrixpositive) = S ((S ((mdr_u_bounded_minorrowminornonzeroevaluationmatrixpositivepoint) * (w) + (mdr_v_bounded_minorrowminornonzeroevaluationmatrixpositivepoint))) * pc)) /\ exists ff_q_mdr_bounded_minorrowminornonzeroevaluationmatrixpositivepointsource. pb = ff_q_mdr_bounded_minorrowminornonzeroevaluationmatrixpositivepointsource * S ((S ((mdr_u_bounded_minorrowminornonzeroevaluationmatrixpositivepoint) * (w) + (mdr_v_bounded_minorrowminornonzeroevaluationmatrixpositivepoint))) * pc) + (mdr_a_bounded_minorrowminornonzeroevaluationmatrixpositive)))))))) /\ (((exists ff_h_mdr_bounded_minorrowminornonzeroevaluationmatrixpositiveoutput. ff_h_mdr_bounded_minorrowminornonzeroevaluationmatrixpositiveoutput + S (mdr_a_bounded_minorrowminornonzeroevaluationmatrixpositive) = S ((S (mdr_i_bounded_minorrowminornonzeroevaluationmatrixpositive)) * mdr_uc_bounded_minorrowminornonzeroevaluation)) /\ exists ff_q_mdr_bounded_minorrowminornonzeroevaluationmatrixpositiveoutput. mdr_ub_bounded_minorrowminornonzeroevaluation = ff_q_mdr_bounded_minorrowminornonzeroevaluationmatrixpositiveoutput * S ((S (mdr_i_bounded_minorrowminornonzeroevaluationmatrixpositive)) * mdr_uc_bounded_minorrowminornonzeroevaluation) + (mdr_a_bounded_minorrowminornonzeroevaluationmatrixpositive)))))) /\ (forall mdr_i_bounded_minorrowminornonzeroevaluationmatrixnegative. (exists mdr_gap_bounded_minorrowminornonzeroevaluationmatrixnegativebound. mdr_gap_bounded_minorrowminornonzeroevaluationmatrixnegativebound + S (mdr_i_bounded_minorrowminornonzeroevaluationmatrixnegative) = ((q) * (q))) -> exists mdr_a_bounded_minorrowminornonzeroevaluationmatrixnegative. (((exists mdr_r_bounded_minorrowminornonzeroevaluationmatrixnegativepoint mdr_s_bounded_minorrowminornonzeroevaluationmatrixnegativepoint mdr_u_bounded_minorrowminornonzeroevaluationmatrixnegativepoint mdr_v_bounded_minorrowminornonzeroevaluationmatrixnegativepoint. ((mdr_i_bounded_minorrowminornonzeroevaluationmatrixnegative = (q) * mdr_r_bounded_minorrowminornonzeroevaluationmatrixnegativepoint + mdr_s_bounded_minorrowminornonzeroevaluationmatrixnegativepoint) /\ ((exists mdr_gap_bounded_minorrowminornonzeroevaluationmatrixnegativepointcolumn. mdr_gap_bounded_minorrowminornonzeroevaluationmatrixnegativepointcolumn + S (mdr_s_bounded_minorrowminornonzeroevaluationmatrixnegativepoint) = (q)) /\ ((((exists ff_h_mdr_bounded_minorrowminornonzeroevaluationmatrixnegativepointrow_index. ff_h_mdr_bounded_minorrowminornonzeroevaluationmatrixnegativepointrow_index + S (mdr_u_bounded_minorrowminornonzeroevaluationmatrixnegativepoint) = S ((S (mdr_r_bounded_minorrowminornonzeroevaluationmatrixnegativepoint)) * rc)) /\ exists ff_q_mdr_bounded_minorrowminornonzeroevaluationmatrixnegativepointrow_index. mdr_a_bounded_minorrows = ff_q_mdr_bounded_minorrowminornonzeroevaluationmatrixnegativepointrow_index * S ((S (mdr_r_bounded_minorrowminornonzeroevaluationmatrixnegativepoint)) * rc) + (mdr_u_bounded_minorrowminornonzeroevaluationmatrixnegativepoint))) /\ ((((exists ff_h_mdr_bounded_minorrowminornonzeroevaluationmatrixnegativepointcolumn_index. ff_h_mdr_bounded_minorrowminornonzeroevaluationmatrixnegativepointcolumn_index + S (mdr_v_bounded_minorrowminornonzeroevaluationmatrixnegativepoint) = S ((S (mdr_s_bounded_minorrowminornonzeroevaluationmatrixnegativepoint)) * cc)) /\ exists ff_q_mdr_bounded_minorrowminornonzeroevaluationmatrixnegativepointcolumn_index. mdr_a_bounded_minorrowcolumns = ff_q_mdr_bounded_minorrowminornonzeroevaluationmatrixnegativepointcolumn_index * S ((S (mdr_s_bounded_minorrowminornonzeroevaluationmatrixnegativepoint)) * cc) + (mdr_v_bounded_minorrowminornonzeroevaluationmatrixnegativepoint))) /\ (((exists ff_h_mdr_bounded_minorrowminornonzeroevaluationmatrixnegativepointsource. ff_h_mdr_bounded_minorrowminornonzeroevaluationmatrixnegativepointsource + S (mdr_a_bounded_minorrowminornonzeroevaluationmatrixnegative) = S ((S ((mdr_u_bounded_minorrowminornonzeroevaluationmatrixnegativepoint) * (w) + (mdr_v_bounded_minorrowminornonzeroevaluationmatrixnegativepoint))) * nc)) /\ exists ff_q_mdr_bounded_minorrowminornonzeroevaluationmatrixnegativepointsource. nb = ff_q_mdr_bounded_minorrowminornonzeroevaluationmatrixnegativepointsource * S ((S ((mdr_u_bounded_minorrowminornonzeroevaluationmatrixnegativepoint) * (w) + (mdr_v_bounded_minorrowminornonzeroevaluationmatrixnegativepoint))) * nc) + (mdr_a_bounded_minorrowminornonzeroevaluationmatrixnegative)))))))) /\ (((exists ff_h_mdr_bounded_minorrowminornonzeroevaluationmatrixnegativeoutput. ff_h_mdr_bounded_minorrowminornonzeroevaluationmatrixnegativeoutput + S (mdr_a_bounded_minorrowminornonzeroevaluationmatrixnegative) = S ((S (mdr_i_bounded_minorrowminornonzeroevaluationmatrixnegative)) * mdr_vc_bounded_minorrowminornonzeroevaluation)) /\ exists ff_q_mdr_bounded_minorrowminornonzeroevaluationmatrixnegativeoutput. mdr_vb_bounded_minorrowminornonzeroevaluation = ff_q_mdr_bounded_minorrowminornonzeroevaluationmatrixnegativeoutput * S ((S (mdr_i_bounded_minorrowminornonzeroevaluationmatrixnegative)) * mdr_vc_bounded_minorrowminornonzeroevaluation) + (mdr_a_bounded_minorrowminornonzeroevaluationmatrixnegative)))))))) /\ (exists mdr_b_bounded_minorrowminornonzeroevaluationdeterminant mdr_c_bounded_minorrowminornonzeroevaluationdeterminant mdr_l_bounded_minorrowminornonzeroevaluationdeterminant mdr_i_bounded_minorrowminornonzeroevaluationdeterminant. ((forall mdr_i_bounded_minorrowminornonzeroevaluationdeterminanth. (exists mdr_gap_bounded_minorrowminornonzeroevaluationdeterminanthi. mdr_gap_bounded_minorrowminornonzeroevaluationdeterminanthi + S (mdr_i_bounded_minorrowminornonzeroevaluationdeterminanth) = (mdr_l_bounded_minorrowminornonzeroevaluationdeterminant)) -> exists mdr_d_bounded_minorrowminornonzeroevaluationdeterminanth mdr_pb_bounded_minorrowminornonzeroevaluationdeterminanth mdr_pc_bounded_minorrowminornonzeroevaluationdeterminanth mdr_nb_bounded_minorrowminornonzeroevaluationdeterminanth mdr_nc_bounded_minorrowminornonzeroevaluationdeterminanth mdr_p_bounded_minorrowminornonzeroevaluationdeterminanth mdr_n_bounded_minorrowminornonzeroevaluationdeterminanth. ((exists mdr_z_bounded_minorrowminornonzeroevaluationdeterminanthr. ((exists mdr_a_bounded_minorrowminornonzeroevaluationdeterminanthrc mdr_b_bounded_minorrowminornonzeroevaluationdeterminanthrc mdr_c_bounded_minorrowminornonzeroevaluationdeterminanthrc mdr_e_bounded_minorrowminornonzeroevaluationdeterminanthrc mdr_f_bounded_minorrowminornonzeroevaluationdeterminanthrc. ((mdr_a_bounded_minorrowminornonzeroevaluationdeterminanthrc = ((mdr_d_bounded_minorrowminornonzeroevaluationdeterminanth) + (mdr_pb_bounded_minorrowminornonzeroevaluationdeterminanth)) * S ((mdr_d_bounded_minorrowminornonzeroevaluationdeterminanth) + (mdr_pb_bounded_minorrowminornonzeroevaluationdeterminanth)) + ((mdr_pb_bounded_minorrowminornonzeroevaluationdeterminanth) + (mdr_pb_bounded_minorrowminornonzeroevaluationdeterminanth))) /\ ((mdr_b_bounded_minorrowminornonzeroevaluationdeterminanthrc = ((mdr_pc_bounded_minorrowminornonzeroevaluationdeterminanth) + (mdr_nb_bounded_minorrowminornonzeroevaluationdeterminanth)) * S ((mdr_pc_bounded_minorrowminornonzeroevaluationdeterminanth) + (mdr_nb_bounded_minorrowminornonzeroevaluationdeterminanth)) + ((mdr_nb_bounded_minorrowminornonzeroevaluationdeterminanth) + (mdr_nb_bounded_minorrowminornonzeroevaluationdeterminanth))) /\ ((mdr_c_bounded_minorrowminornonzeroevaluationdeterminanthrc = ((mdr_a_bounded_minorrowminornonzeroevaluationdeterminanthrc) + (mdr_b_bounded_minorrowminornonzeroevaluationdeterminanthrc)) * S ((mdr_a_bounded_minorrowminornonzeroevaluationdeterminanthrc) + (mdr_b_bounded_minorrowminornonzeroevaluationdeterminanthrc)) + ((mdr_b_bounded_minorrowminornonzeroevaluationdeterminanthrc) + (mdr_b_bounded_minorrowminornonzeroevaluationdeterminanthrc))) /\ ((mdr_e_bounded_minorrowminornonzeroevaluationdeterminanthrc = ((mdr_p_bounded_minorrowminornonzeroevaluationdeterminanth) + (mdr_n_bounded_minorrowminornonzeroevaluationdeterminanth)) * S ((mdr_p_bounded_minorrowminornonzeroevaluationdeterminanth) + (mdr_n_bounded_minorrowminornonzeroevaluationdeterminanth)) + ((mdr_n_bounded_minorrowminornonzeroevaluationdeterminanth) + (mdr_n_bounded_minorrowminornonzeroevaluationdeterminanth))) /\ ((mdr_f_bounded_minorrowminornonzeroevaluationdeterminanthrc = ((mdr_nc_bounded_minorrowminornonzeroevaluationdeterminanth) + (mdr_e_bounded_minorrowminornonzeroevaluationdeterminanthrc)) * S ((mdr_nc_bounded_minorrowminornonzeroevaluationdeterminanth) + (mdr_e_bounded_minorrowminornonzeroevaluationdeterminanthrc)) + ((mdr_e_bounded_minorrowminornonzeroevaluationdeterminanthrc) + (mdr_e_bounded_minorrowminornonzeroevaluationdeterminanthrc))) /\ ((mdr_z_bounded_minorrowminornonzeroevaluationdeterminanthr) = ((mdr_c_bounded_minorrowminornonzeroevaluationdeterminanthrc) + (mdr_f_bounded_minorrowminornonzeroevaluationdeterminanthrc)) * S ((mdr_c_bounded_minorrowminornonzeroevaluationdeterminanthrc) + (mdr_f_bounded_minorrowminornonzeroevaluationdeterminanthrc)) + ((mdr_f_bounded_minorrowminornonzeroevaluationdeterminanthrc) + (mdr_f_bounded_minorrowminornonzeroevaluationdeterminanthrc))))))))) /\ (((exists ff_h_mdr_bounded_minorrowminornonzeroevaluationdeterminanthrb. ff_h_mdr_bounded_minorrowminornonzeroevaluationdeterminanthrb + S (mdr_z_bounded_minorrowminornonzeroevaluationdeterminanthr) = S ((S (mdr_i_bounded_minorrowminornonzeroevaluationdeterminanth)) * mdr_c_bounded_minorrowminornonzeroevaluationdeterminant)) /\ exists ff_q_mdr_bounded_minorrowminornonzeroevaluationdeterminanthrb. mdr_b_bounded_minorrowminornonzeroevaluationdeterminant = ff_q_mdr_bounded_minorrowminornonzeroevaluationdeterminanthrb * S ((S (mdr_i_bounded_minorrowminornonzeroevaluationdeterminanth)) * mdr_c_bounded_minorrowminornonzeroevaluationdeterminant) + (mdr_z_bounded_minorrowminornonzeroevaluationdeterminanthr))))) /\ (((((mdr_d_bounded_minorrowminornonzeroevaluationdeterminanth) = 0) /\ (((mdr_p_bounded_minorrowminornonzeroevaluationdeterminanth) = 1) /\ ((mdr_n_bounded_minorrowminornonzeroevaluationdeterminanth) = 0))) \/ exists mdr_q_bounded_minorrowminornonzeroevaluationdeterminanths mdr_eb_bounded_minorrowminornonzeroevaluationdeterminanths mdr_ec_bounded_minorrowminornonzeroevaluationdeterminanths mdr_fb_bounded_minorrowminornonzeroevaluationdeterminanths mdr_fc_bounded_minorrowminornonzeroevaluationdeterminanths. (((mdr_d_bounded_minorrowminornonzeroevaluationdeterminanth) = S (mdr_q_bounded_minorrowminornonzeroevaluationdeterminanths)) /\ ((forall mdr_j_bounded_minorrowminornonzeroevaluationdeterminanthsc. (exists mdr_gap_bounded_minorrowminornonzeroevaluationdeterminanthscj. mdr_gap_bounded_minorrowminornonzeroevaluationdeterminanthscj + S (mdr_j_bounded_minorrowminornonzeroevaluationdeterminanthsc) = (S (mdr_q_bounded_minorrowminornonzeroevaluationdeterminanths))) -> exists mdr_i_bounded_minorrowminornonzeroevaluationdeterminanthsc mdr_up_bounded_minorrowminornonzeroevaluationdeterminanthsc mdr_us_bounded_minorrowminornonzeroevaluationdeterminanthsc mdr_un_bounded_minorrowminornonzeroevaluationdeterminanthsc mdr_ut_bounded_minorrowminornonzeroevaluationdeterminanthsc mdr_p_bounded_minorrowminornonzeroevaluationdeterminanthsc mdr_n_bounded_minorrowminornonzeroevaluationdeterminanthsc. ((exists mdr_gap_bounded_minorrowminornonzeroevaluationdeterminanthsci. mdr_gap_bounded_minorrowminornonzeroevaluationdeterminanthsci + S (mdr_i_bounded_minorrowminornonzeroevaluationdeterminanthsc) = (mdr_i_bounded_minorrowminornonzeroevaluationdeterminanth)) /\ ((exists mdr_z_bounded_minorrowminornonzeroevaluationdeterminanthscr. ((exists mdr_a_bounded_minorrowminornonzeroevaluationdeterminanthscrc mdr_b_bounded_minorrowminornonzeroevaluationdeterminanthscrc mdr_c_bounded_minorrowminornonzeroevaluationdeterminanthscrc mdr_e_bounded_minorrowminornonzeroevaluationdeterminanthscrc mdr_f_bounded_minorrowminornonzeroevaluationdeterminanthscrc. ((mdr_a_bounded_minorrowminornonzeroevaluationdeterminanthscrc = ((mdr_q_bounded_minorrowminornonzeroevaluationdeterminanths) + (mdr_up_bounded_minorrowminornonzeroevaluationdeterminanthsc)) * S ((mdr_q_bounded_minorrowminornonzeroevaluationdeterminanths) + (mdr_up_bounded_minorrowminornonzeroevaluationdeterminanthsc)) + ((mdr_up_bounded_minorrowminornonzeroevaluationdeterminanthsc) + (mdr_up_bounded_minorrowminornonzeroevaluationdeterminanthsc))) /\ ((mdr_b_bounded_minorrowminornonzeroevaluationdeterminanthscrc = ((mdr_us_bounded_minorrowminornonzeroevaluationdeterminanthsc) + (mdr_un_bounded_minorrowminornonzeroevaluationdeterminanthsc)) * S ((mdr_us_bounded_minorrowminornonzeroevaluationdeterminanthsc) + (mdr_un_bounded_minorrowminornonzeroevaluationdeterminanthsc)) + ((mdr_un_bounded_minorrowminornonzeroevaluationdeterminanthsc) + (mdr_un_bounded_minorrowminornonzeroevaluationdeterminanthsc))) /\ ((mdr_c_bounded_minorrowminornonzeroevaluationdeterminanthscrc = ((mdr_a_bounded_minorrowminornonzeroevaluationdeterminanthscrc) + (mdr_b_bounded_minorrowminornonzeroevaluationdeterminanthscrc)) * S ((mdr_a_bounded_minorrowminornonzeroevaluationdeterminanthscrc) + (mdr_b_bounded_minorrowminornonzeroevaluationdeterminanthscrc)) + ((mdr_b_bounded_minorrowminornonzeroevaluationdeterminanthscrc) + (mdr_b_bounded_minorrowminornonzeroevaluationdeterminanthscrc))) /\ ((mdr_e_bounded_minorrowminornonzeroevaluationdeterminanthscrc = ((mdr_p_bounded_minorrowminornonzeroevaluationdeterminanthsc) + (mdr_n_bounded_minorrowminornonzeroevaluationdeterminanthsc)) * S ((mdr_p_bounded_minorrowminornonzeroevaluationdeterminanthsc) + (mdr_n_bounded_minorrowminornonzeroevaluationdeterminanthsc)) + ((mdr_n_bounded_minorrowminornonzeroevaluationdeterminanthsc) + (mdr_n_bounded_minorrowminornonzeroevaluationdeterminanthsc))) /\ ((mdr_f_bounded_minorrowminornonzeroevaluationdeterminanthscrc = ((mdr_ut_bounded_minorrowminornonzeroevaluationdeterminanthsc) + (mdr_e_bounded_minorrowminornonzeroevaluationdeterminanthscrc)) * S ((mdr_ut_bounded_minorrowminornonzeroevaluationdeterminanthsc) + (mdr_e_bounded_minorrowminornonzeroevaluationdeterminanthscrc)) + ((mdr_e_bounded_minorrowminornonzeroevaluationdeterminanthscrc) + (mdr_e_bounded_minorrowminornonzeroevaluationdeterminanthscrc))) /\ ((mdr_z_bounded_minorrowminornonzeroevaluationdeterminanthscr) = ((mdr_c_bounded_minorrowminornonzeroevaluationdeterminanthscrc) + (mdr_f_bounded_minorrowminornonzeroevaluationdeterminanthscrc)) * S ((mdr_c_bounded_minorrowminornonzeroevaluationdeterminanthscrc) + (mdr_f_bounded_minorrowminornonzeroevaluationdeterminanthscrc)) + ((mdr_f_bounded_minorrowminornonzeroevaluationdeterminanthscrc) + (mdr_f_bounded_minorrowminornonzeroevaluationdeterminanthscrc))))))))) /\ (((exists ff_h_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscrb. ff_h_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscrb + S (mdr_z_bounded_minorrowminornonzeroevaluationdeterminanthscr) = S ((S (mdr_i_bounded_minorrowminornonzeroevaluationdeterminanthsc)) * mdr_c_bounded_minorrowminornonzeroevaluationdeterminant)) /\ exists ff_q_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscrb. mdr_b_bounded_minorrowminornonzeroevaluationdeterminant = ff_q_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscrb * S ((S (mdr_i_bounded_minorrowminornonzeroevaluationdeterminanthsc)) * mdr_c_bounded_minorrowminornonzeroevaluationdeterminant) + (mdr_z_bounded_minorrowminornonzeroevaluationdeterminanthscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_positive. (exists ff_gap_mdm_lt_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_positive_index_bound. ff_gap_mdm_lt_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_positive) = ((mdr_q_bounded_minorrowminornonzeroevaluationdeterminanths) * (mdr_q_bounded_minorrowminornonzeroevaluationdeterminanths))) -> exists ff_row_mdm_prefix_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_positive ff_column_mdm_prefix_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_positive ff_value_mdm_prefix_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_positive. (ff_index_mdm_prefix_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_positive = (mdr_q_bounded_minorrowminornonzeroevaluationdeterminanths) * ff_row_mdm_prefix_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_positive + ff_column_mdm_prefix_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_positive /\ ((exists ff_gap_mdm_lt_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_positive_column_bound. ff_gap_mdm_lt_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_positive) = (mdr_q_bounded_minorrowminornonzeroevaluationdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_positive_cell ff_column_mdm_cell_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_positive_cell = ff_row_mdm_prefix_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_positive_cell_row_after. ff_gap_mdm_le_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_positive)) /\ ff_row_mdm_cell_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_positive_cell = S ff_row_mdm_prefix_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_positive) = (mdr_j_bounded_minorrowminornonzeroevaluationdeterminanthsc)) /\ ff_column_mdm_cell_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_positive_cell = ff_column_mdm_prefix_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_positive_cell_column_after. ff_gap_mdm_le_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_positive_cell_column_after + (mdr_j_bounded_minorrowminornonzeroevaluationdeterminanthsc) = (ff_column_mdm_prefix_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_positive)) /\ ff_column_mdm_cell_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_positive_cell = S ff_column_mdm_prefix_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_positive))) /\ (((exists ff_h_mdm_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_positive_cell_source. ff_h_mdm_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_positive) = S ((S ((ff_row_mdm_cell_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_positive_cell) * (S (mdr_q_bounded_minorrowminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_positive_cell))) * mdr_pc_bounded_minorrowminornonzeroevaluationdeterminanth)) /\ exists ff_q_mdm_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_positive_cell_source. mdr_pb_bounded_minorrowminornonzeroevaluationdeterminanth = ff_q_mdm_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_positive_cell) * (S (mdr_q_bounded_minorrowminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_positive_cell))) * mdr_pc_bounded_minorrowminornonzeroevaluationdeterminanth) + (ff_value_mdm_prefix_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_positive)))))) /\ (((exists ff_h_mdm_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_positive_target. ff_h_mdm_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_positive_target + S (ff_value_mdm_prefix_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_positive) = S ((S (ff_index_mdm_prefix_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_positive)) * mdr_us_bounded_minorrowminornonzeroevaluationdeterminanthsc)) /\ exists ff_q_mdm_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_positive_target. mdr_up_bounded_minorrowminornonzeroevaluationdeterminanthsc = ff_q_mdm_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_positive)) * mdr_us_bounded_minorrowminornonzeroevaluationdeterminanthsc) + (ff_value_mdm_prefix_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_negative. (exists ff_gap_mdm_lt_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_negative_index_bound. ff_gap_mdm_lt_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_negative) = ((mdr_q_bounded_minorrowminornonzeroevaluationdeterminanths) * (mdr_q_bounded_minorrowminornonzeroevaluationdeterminanths))) -> exists ff_row_mdm_prefix_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_negative ff_column_mdm_prefix_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_negative ff_value_mdm_prefix_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_negative. (ff_index_mdm_prefix_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_negative = (mdr_q_bounded_minorrowminornonzeroevaluationdeterminanths) * ff_row_mdm_prefix_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_negative + ff_column_mdm_prefix_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_negative /\ ((exists ff_gap_mdm_lt_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_negative_column_bound. ff_gap_mdm_lt_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_negative) = (mdr_q_bounded_minorrowminornonzeroevaluationdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_negative_cell ff_column_mdm_cell_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_negative_cell = ff_row_mdm_prefix_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_negative_cell_row_after. ff_gap_mdm_le_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_negative)) /\ ff_row_mdm_cell_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_negative_cell = S ff_row_mdm_prefix_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_negative) = (mdr_j_bounded_minorrowminornonzeroevaluationdeterminanthsc)) /\ ff_column_mdm_cell_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_negative_cell = ff_column_mdm_prefix_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_negative_cell_column_after. ff_gap_mdm_le_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_negative_cell_column_after + (mdr_j_bounded_minorrowminornonzeroevaluationdeterminanthsc) = (ff_column_mdm_prefix_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_negative)) /\ ff_column_mdm_cell_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_negative_cell = S ff_column_mdm_prefix_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_negative))) /\ (((exists ff_h_mdm_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_negative_cell_source. ff_h_mdm_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_negative) = S ((S ((ff_row_mdm_cell_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_negative_cell) * (S (mdr_q_bounded_minorrowminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_negative_cell))) * mdr_nc_bounded_minorrowminornonzeroevaluationdeterminanth)) /\ exists ff_q_mdm_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_negative_cell_source. mdr_nb_bounded_minorrowminornonzeroevaluationdeterminanth = ff_q_mdm_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_negative_cell) * (S (mdr_q_bounded_minorrowminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_negative_cell))) * mdr_nc_bounded_minorrowminornonzeroevaluationdeterminanth) + (ff_value_mdm_prefix_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_negative)))))) /\ (((exists ff_h_mdm_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_negative_target. ff_h_mdm_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_negative_target + S (ff_value_mdm_prefix_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_negative) = S ((S (ff_index_mdm_prefix_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_negative)) * mdr_ut_bounded_minorrowminornonzeroevaluationdeterminanthsc)) /\ exists ff_q_mdm_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_negative_target. mdr_un_bounded_minorrowminornonzeroevaluationdeterminanthsc = ff_q_mdm_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_negative)) * mdr_ut_bounded_minorrowminornonzeroevaluationdeterminanthsc) + (ff_value_mdm_prefix_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscm_negative))))))))) /\ ((((exists ff_h_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscp. ff_h_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscp + S (mdr_p_bounded_minorrowminornonzeroevaluationdeterminanthsc) = S ((S (mdr_j_bounded_minorrowminornonzeroevaluationdeterminanthsc)) * mdr_ec_bounded_minorrowminornonzeroevaluationdeterminanths)) /\ exists ff_q_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscp. mdr_eb_bounded_minorrowminornonzeroevaluationdeterminanths = ff_q_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscp * S ((S (mdr_j_bounded_minorrowminornonzeroevaluationdeterminanthsc)) * mdr_ec_bounded_minorrowminornonzeroevaluationdeterminanths) + (mdr_p_bounded_minorrowminornonzeroevaluationdeterminanthsc))) /\ (((exists ff_h_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscn. ff_h_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscn + S (mdr_n_bounded_minorrowminornonzeroevaluationdeterminanthsc) = S ((S (mdr_j_bounded_minorrowminornonzeroevaluationdeterminanthsc)) * mdr_fc_bounded_minorrowminornonzeroevaluationdeterminanths)) /\ exists ff_q_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscn. mdr_fb_bounded_minorrowminornonzeroevaluationdeterminanths = ff_q_mdr_bounded_minorrowminornonzeroevaluationdeterminanthscn * S ((S (mdr_j_bounded_minorrowminornonzeroevaluationdeterminanthsc)) * mdr_fc_bounded_minorrowminornonzeroevaluationdeterminanths) + (mdr_n_bounded_minorrowminornonzeroevaluationdeterminanthsc)))))))) /\ (exists ff_ub_mce_fold_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf ff_uc_mce_fold_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf ff_vb_mce_fold_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf ff_vc_mce_fold_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf. ((forall ff_index_mce_alternating_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix. (exists ff_gap_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix_index. ff_gap_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix_index + S (ff_index_mce_alternating_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix) = (S (mdr_q_bounded_minorrowminornonzeroevaluationdeterminanths))) -> exists ff_ap_mce_alternating_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix ff_an_mce_alternating_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix ff_bp_mce_alternating_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix ff_bn_mce_alternating_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix ff_p_mce_alternating_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix ff_n_mce_alternating_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix. ((((exists ff_h_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix_ap. ff_h_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix_ap + S (ff_ap_mce_alternating_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix)) * mdr_pc_bounded_minorrowminornonzeroevaluationdeterminanth)) /\ exists ff_q_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix_ap. mdr_pb_bounded_minorrowminornonzeroevaluationdeterminanth = ff_q_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix)) * mdr_pc_bounded_minorrowminornonzeroevaluationdeterminanth) + (ff_ap_mce_alternating_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix_an. ff_h_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix_an + S (ff_an_mce_alternating_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix)) * mdr_nc_bounded_minorrowminornonzeroevaluationdeterminanth)) /\ exists ff_q_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix_an. mdr_nb_bounded_minorrowminornonzeroevaluationdeterminanth = ff_q_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix)) * mdr_nc_bounded_minorrowminornonzeroevaluationdeterminanth) + (ff_an_mce_alternating_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix_bp. ff_h_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix_bp + S (ff_bp_mce_alternating_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix)) * mdr_ec_bounded_minorrowminornonzeroevaluationdeterminanths)) /\ exists ff_q_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix_bp. mdr_eb_bounded_minorrowminornonzeroevaluationdeterminanths = ff_q_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix)) * mdr_ec_bounded_minorrowminornonzeroevaluationdeterminanths) + (ff_bp_mce_alternating_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix_bn. ff_h_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix_bn + S (ff_bn_mce_alternating_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix)) * mdr_fc_bounded_minorrowminornonzeroevaluationdeterminanths)) /\ exists ff_q_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix_bn. mdr_fb_bounded_minorrowminornonzeroevaluationdeterminanths = ff_q_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix)) * mdr_fc_bounded_minorrowminornonzeroevaluationdeterminanths) + (ff_bn_mce_alternating_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix_positive. ff_h_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix_positive + S (ff_p_mce_alternating_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix_positive. ff_ub_mce_fold_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf) + (ff_p_mce_alternating_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix_negative. ff_h_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix_negative + S (ff_n_mce_alternating_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix_negative. ff_vb_mce_fold_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf) + (ff_n_mce_alternating_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix))) /\ (((exists ff_even_mce_term_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix = 2 * ff_even_mce_term_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix_term) /\ (ff_p_mce_alternating_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix = 2 * ff_odd_mce_term_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_positive ff_v_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_positive. ((((exists ff_h_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_positive_start. ff_h_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_positive_start. ff_u_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_positive_start * S ((S (0)) * ff_v_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_positive_terminal. ff_h_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_positive_terminal + S (mdr_p_bounded_minorrowminornonzeroevaluationdeterminanth) = S ((S ((S (mdr_q_bounded_minorrowminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_positive_terminal. ff_u_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_positive_terminal * S ((S ((S (mdr_q_bounded_minorrowminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_positive) + (mdr_p_bounded_minorrowminornonzeroevaluationdeterminanth))) /\ forall ff_i_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_positive. (exists ff_lt_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_positive_bound. ff_lt_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_positive_bound + S ff_i_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_positive = (S (mdr_q_bounded_minorrowminornonzeroevaluationdeterminanths))) -> exists ff_a_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_positive ff_r_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_positive ff_s_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_positive. ((((exists ff_h_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_positive_summand. ff_h_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_positive_summand + S (ff_a_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_positive_summand. ff_ub_mce_fold_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_positive_summand * S ((S (ff_i_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf) + (ff_a_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_positive_partial. ff_h_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_positive_partial + S (ff_r_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_positive_partial. ff_u_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_positive_partial * S ((S (ff_i_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_positive) + (ff_r_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_positive_successor. ff_h_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_positive_successor + S (ff_s_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_positive) = S ((S (S ff_i_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_positive_successor. ff_u_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_positive_successor * S ((S (S ff_i_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_positive) + (ff_s_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_positive))) /\ ff_s_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_positive = ff_r_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_positive + ff_a_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_positive)))))) /\ (exists ff_u_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_negative ff_v_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_negative. ((((exists ff_h_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_negative_start. ff_h_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_negative_start. ff_u_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_negative_start * S ((S (0)) * ff_v_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_negative_terminal. ff_h_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_negative_terminal + S (mdr_n_bounded_minorrowminornonzeroevaluationdeterminanth) = S ((S ((S (mdr_q_bounded_minorrowminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_negative_terminal. ff_u_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_negative_terminal * S ((S ((S (mdr_q_bounded_minorrowminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_negative) + (mdr_n_bounded_minorrowminornonzeroevaluationdeterminanth))) /\ forall ff_i_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_negative. (exists ff_lt_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_negative_bound. ff_lt_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_negative_bound + S ff_i_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_negative = (S (mdr_q_bounded_minorrowminornonzeroevaluationdeterminanths))) -> exists ff_a_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_negative ff_r_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_negative ff_s_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_negative. ((((exists ff_h_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_negative_summand. ff_h_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_negative_summand + S (ff_a_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_negative_summand. ff_vb_mce_fold_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_negative_summand * S ((S (ff_i_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf) + (ff_a_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_negative_partial. ff_h_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_negative_partial + S (ff_r_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_negative_partial. ff_u_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_negative_partial * S ((S (ff_i_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_negative) + (ff_r_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_negative_successor. ff_h_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_negative_successor + S (ff_s_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_negative) = S ((S (S ff_i_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_negative_successor. ff_u_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_negative_successor * S ((S (S ff_i_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_negative) + (ff_s_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_negative))) /\ ff_s_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_negative = ff_r_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_negative + ff_a_mce_mdr_bounded_minorrowminornonzeroevaluationdeterminanthsf_negative))))))))))))))) /\ ((exists mdr_gap_bounded_minorrowminornonzeroevaluationdeterminanti. mdr_gap_bounded_minorrowminornonzeroevaluationdeterminanti + S (mdr_i_bounded_minorrowminornonzeroevaluationdeterminant) = (mdr_l_bounded_minorrowminornonzeroevaluationdeterminant)) /\ (exists mdr_z_bounded_minorrowminornonzeroevaluationdeterminantr. ((exists mdr_a_bounded_minorrowminornonzeroevaluationdeterminantrc mdr_b_bounded_minorrowminornonzeroevaluationdeterminantrc mdr_c_bounded_minorrowminornonzeroevaluationdeterminantrc mdr_e_bounded_minorrowminornonzeroevaluationdeterminantrc mdr_f_bounded_minorrowminornonzeroevaluationdeterminantrc. ((mdr_a_bounded_minorrowminornonzeroevaluationdeterminantrc = ((q) + (mdr_ub_bounded_minorrowminornonzeroevaluation)) * S ((q) + (mdr_ub_bounded_minorrowminornonzeroevaluation)) + ((mdr_ub_bounded_minorrowminornonzeroevaluation) + (mdr_ub_bounded_minorrowminornonzeroevaluation))) /\ ((mdr_b_bounded_minorrowminornonzeroevaluationdeterminantrc = ((mdr_uc_bounded_minorrowminornonzeroevaluation) + (mdr_vb_bounded_minorrowminornonzeroevaluation)) * S ((mdr_uc_bounded_minorrowminornonzeroevaluation) + (mdr_vb_bounded_minorrowminornonzeroevaluation)) + ((mdr_vb_bounded_minorrowminornonzeroevaluation) + (mdr_vb_bounded_minorrowminornonzeroevaluation))) /\ ((mdr_c_bounded_minorrowminornonzeroevaluationdeterminantrc = ((mdr_a_bounded_minorrowminornonzeroevaluationdeterminantrc) + (mdr_b_bounded_minorrowminornonzeroevaluationdeterminantrc)) * S ((mdr_a_bounded_minorrowminornonzeroevaluationdeterminantrc) + (mdr_b_bounded_minorrowminornonzeroevaluationdeterminantrc)) + ((mdr_b_bounded_minorrowminornonzeroevaluationdeterminantrc) + (mdr_b_bounded_minorrowminornonzeroevaluationdeterminantrc))) /\ ((mdr_e_bounded_minorrowminornonzeroevaluationdeterminantrc = ((mdr_p_bounded_minorrowminornonzero) + (mdr_n_bounded_minorrowminornonzero)) * S ((mdr_p_bounded_minorrowminornonzero) + (mdr_n_bounded_minorrowminornonzero)) + ((mdr_n_bounded_minorrowminornonzero) + (mdr_n_bounded_minorrowminornonzero))) /\ ((mdr_f_bounded_minorrowminornonzeroevaluationdeterminantrc = ((mdr_vc_bounded_minorrowminornonzeroevaluation) + (mdr_e_bounded_minorrowminornonzeroevaluationdeterminantrc)) * S ((mdr_vc_bounded_minorrowminornonzeroevaluation) + (mdr_e_bounded_minorrowminornonzeroevaluationdeterminantrc)) + ((mdr_e_bounded_minorrowminornonzeroevaluationdeterminantrc) + (mdr_e_bounded_minorrowminornonzeroevaluationdeterminantrc))) /\ ((mdr_z_bounded_minorrowminornonzeroevaluationdeterminantr) = ((mdr_c_bounded_minorrowminornonzeroevaluationdeterminantrc) + (mdr_f_bounded_minorrowminornonzeroevaluationdeterminantrc)) * S ((mdr_c_bounded_minorrowminornonzeroevaluationdeterminantrc) + (mdr_f_bounded_minorrowminornonzeroevaluationdeterminantrc)) + ((mdr_f_bounded_minorrowminornonzeroevaluationdeterminantrc) + (mdr_f_bounded_minorrowminornonzeroevaluationdeterminantrc))))))))) /\ (((exists ff_h_mdr_bounded_minorrowminornonzeroevaluationdeterminantrb. ff_h_mdr_bounded_minorrowminornonzeroevaluationdeterminantrb + S (mdr_z_bounded_minorrowminornonzeroevaluationdeterminantr) = S ((S (mdr_i_bounded_minorrowminornonzeroevaluationdeterminant)) * mdr_c_bounded_minorrowminornonzeroevaluationdeterminant)) /\ exists ff_q_mdr_bounded_minorrowminornonzeroevaluationdeterminantrb. mdr_b_bounded_minorrowminornonzeroevaluationdeterminant = ff_q_mdr_bounded_minorrowminornonzeroevaluationdeterminantrb * S ((S (mdr_i_bounded_minorrowminornonzeroevaluationdeterminant)) * mdr_c_bounded_minorrowminornonzeroevaluationdeterminant) + (mdr_z_bounded_minorrowminornonzeroevaluationdeterminantr)))))))))) /\ (~(mdr_p_bounded_minorrowminornonzero = mdr_n_bounded_minorrowminornonzero)))))))))))))Complete tactic proof in conservative notation
All 63 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
63 script commands · 14 reading checkpoints · 2 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.
Named ingredients (1)
01Fix variables and assumptionsL1–10
02Fix variables and assumptionsL11–14
03Separate the logical casesL15–24
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L15
cases hrowbox - L16
cases hcolbox - L17
cases hminor - L18
cases hminor_witness - L19
cases hminor_witness_witness - L20
cases hminor_witness_witness_witness - L21
cases hminor_witness_witness_witness_witness - L22
cases hminor_witness_witness_witness_witness_right - L23
cases hminor_witness_witness_witness_witness_left - L24
cases hminor_witness_witness_witness_witness_right_left
04Establish hrowL25–29
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hrowbox right.
- L25
have hrow : ∃ a. Lt(a,R) ∧ (∀ y. ∀ z. Lt(y,q) → BetaAt(x,x1,y,z) → BetaAt(a,rc,y,z))Definitions: Lt(a,R)Lt(y,q)BetaAt(x,x1,y,z)BetaAt(a,rc,y,z)Original native command in the exact edition - L26
specialize hrowbox_right (x) - L27
specialize hrowbox_right (x1) - L28
apply hrowbox_right - L29
exact hminor_witness_witness_witness_witness_left_left
05Separate the logical casesL30–31
06Establish hcolumnL32–36
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hcolbox right.
- L32
have hcolumn : ∃ a. Lt(a,C) ∧ (∀ x. ∀ y. Lt(x,q) → BetaAt(x2,x3,x,y) → BetaAt(a,cc,x,y))Definitions: Lt(a,C)Lt(x,q)BetaAt(x2,x3,x,y)BetaAt(a,cc,x,y)Original native command in the exact edition - L33
specialize hcolbox_right (x2) - L34
specialize hcolbox_right (x3) - L35
apply hcolbox_right - L36
exact hminor_witness_witness_witness_witness_right_left_left
07Separate the logical casesL37–38
08Construct an explicit witnessL39–39
Supply the displayed value, then prove that it has the required property.
- L39
exists x4
09Separate the logical casesL40–40
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L40
split
10Use earlier factsL41–41
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L41
exact hrow_witness_left
11Construct an explicit witnessL42–42
Supply the displayed value, then prove that it has the required property.
- L42
exists x5
12Separate the logical casesL43–43
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L43
split
13Use earlier factsL44–53
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L44
exact hcolumn_witness_left - L45
specialize matrix_rank_nonzero_selected_minor_transport (pb) - L46
specialize matrix_rank_nonzero_selected_minor_transport (pc) - L47
specialize matrix_rank_nonzero_selected_minor_transport (nb) - L48
specialize matrix_rank_nonzero_selected_minor_transport (nc) - L49
specialize matrix_rank_nonzero_selected_minor_transport (r) - L50
specialize matrix_rank_nonzero_selected_minor_transport (w) - L51
specialize matrix_rank_nonzero_selected_minor_transport (q) - L52
specialize matrix_rank_nonzero_selected_minor_transport (x) - L53
specialize matrix_rank_nonzero_selected_minor_transport (x1)
14Use earlier factsL54–63
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L54
specialize matrix_rank_nonzero_selected_minor_transport (x2) - L55
specialize matrix_rank_nonzero_selected_minor_transport (x3) - L56
specialize matrix_rank_nonzero_selected_minor_transport (x4) - L57
specialize matrix_rank_nonzero_selected_minor_transport (rc) - L58
specialize matrix_rank_nonzero_selected_minor_transport (x5) - L59
specialize matrix_rank_nonzero_selected_minor_transport (cc) - L60
apply matrix_rank_nonzero_selected_minor_transport - L61
exact hrow_witness_right - L62
exact hcolumn_witness_right - L63
exact hminor_witness_witness_witness_witness
Original defined command ledger · 63 lines
- 0001
intro pb - 0002
intro pc - 0003
intro nb - 0004
intro nc - 0005
intro r - 0006
intro w - 0007
intro q - 0008
intro rc - 0009
intro cc - 0010
intro R - 0011
intro C - 0012
intro hrowbox - 0013
intro hcolbox - 0014
intro hminor - 0015
cases hrowbox - 0016
cases hcolbox - 0017
cases hminor - 0018
cases hminor_witness - 0019
cases hminor_witness_witness - 0020
cases hminor_witness_witness_witness - 0021
cases hminor_witness_witness_witness_witness - 0022
cases hminor_witness_witness_witness_witness_right - 0023
cases hminor_witness_witness_witness_witness_left - 0024
cases hminor_witness_witness_witness_witness_right_left - 0025
have hrow : ∃ a. Lt(a,R) ∧ (∀ y. ∀ z. Lt(y,q) → BetaAt(x,x1,y,z) → BetaAt(a,rc,y,z)) - 0026
specialize hrowbox_right (x) - 0027
specialize hrowbox_right (x1) - 0028
apply hrowbox_right - 0029
exact hminor_witness_witness_witness_witness_left_left - 0030
cases hrow - 0031
cases hrow_witness - 0032
have hcolumn : ∃ a. Lt(a,C) ∧ (∀ x. ∀ y. Lt(x,q) → BetaAt(x2,x3,x,y) → BetaAt(a,cc,x,y)) - 0033
specialize hcolbox_right (x2) - 0034
specialize hcolbox_right (x3) - 0035
apply hcolbox_right - 0036
exact hminor_witness_witness_witness_witness_right_left_left - 0037
cases hcolumn - 0038
cases hcolumn_witness - 0039
exists x4 - 0040
split - 0041
exact hrow_witness_left - 0042
exists x5 - 0043
split - 0044
exact hcolumn_witness_left - 0045
specialize matrix_rank_nonzero_selected_minor_transport (pb) - 0046
specialize matrix_rank_nonzero_selected_minor_transport (pc) - 0047
specialize matrix_rank_nonzero_selected_minor_transport (nb) - 0048
specialize matrix_rank_nonzero_selected_minor_transport (nc) - 0049
specialize matrix_rank_nonzero_selected_minor_transport (r) - 0050
specialize matrix_rank_nonzero_selected_minor_transport (w) - 0051
specialize matrix_rank_nonzero_selected_minor_transport (q) - 0052
specialize matrix_rank_nonzero_selected_minor_transport (x) - 0053
specialize matrix_rank_nonzero_selected_minor_transport (x1) - 0054
specialize matrix_rank_nonzero_selected_minor_transport (x2) - 0055
specialize matrix_rank_nonzero_selected_minor_transport (x3) - 0056
specialize matrix_rank_nonzero_selected_minor_transport (x4) - 0057
specialize matrix_rank_nonzero_selected_minor_transport (rc) - 0058
specialize matrix_rank_nonzero_selected_minor_transport (x5) - 0059
specialize matrix_rank_nonzero_selected_minor_transport (cc) - 0060
apply matrix_rank_nonzero_selected_minor_transport - 0061
exact hrow_witness_right - 0062
exact hcolumn_witness_right - 0063
exact hminor_witness_witness_witness_witness