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. ∀ rb. ∀ rc. ∀ cb. ∀ cc. ∀ Rb. ∀ Rc. ∀ Cb. ∀ Cc. (∀ x. ∀ y. Lt(x,q) → BetaAt(rb,rc,x,y) → BetaAt(Rb,Rc,x,y)) → (∀ x. ∀ y. Lt(x,q) → BetaAt(cb,cc,x,y) → BetaAt(Cb,Cc,x,y)) → NonzeroSelectedMinor(pb,pc,nb,nc,r,w,q,rb,rc,cb,cc) → NonzeroSelectedMinor(pb,pc,nb,nc,r,w,q,Rb,Rc,Cb,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 rb rc cb cc Rb Rc Cb Cc. (forall mdr_i_nonzero_rows mdr_a_nonzero_rows. (exists mdr_gap_nonzero_rowsb. mdr_gap_nonzero_rowsb + S (mdr_i_nonzero_rows) = (q)) -> (((exists ff_h_mdr_nonzero_rowso. ff_h_mdr_nonzero_rowso + S (mdr_a_nonzero_rows) = S ((S (mdr_i_nonzero_rows)) * rc)) /\ exists ff_q_mdr_nonzero_rowso. rb = ff_q_mdr_nonzero_rowso * S ((S (mdr_i_nonzero_rows)) * rc) + (mdr_a_nonzero_rows))) -> (((exists ff_h_mdr_nonzero_rowsn. ff_h_mdr_nonzero_rowsn + S (mdr_a_nonzero_rows) = S ((S (mdr_i_nonzero_rows)) * Rc)) /\ exists ff_q_mdr_nonzero_rowsn. Rb = ff_q_mdr_nonzero_rowsn * S ((S (mdr_i_nonzero_rows)) * Rc) + (mdr_a_nonzero_rows)))) -> (forall mdr_i_nonzero_columns mdr_a_nonzero_columns. (exists mdr_gap_nonzero_columnsb. mdr_gap_nonzero_columnsb + S (mdr_i_nonzero_columns) = (q)) -> (((exists ff_h_mdr_nonzero_columnso. ff_h_mdr_nonzero_columnso + S (mdr_a_nonzero_columns) = S ((S (mdr_i_nonzero_columns)) * cc)) /\ exists ff_q_mdr_nonzero_columnso. cb = ff_q_mdr_nonzero_columnso * S ((S (mdr_i_nonzero_columns)) * cc) + (mdr_a_nonzero_columns))) -> (((exists ff_h_mdr_nonzero_columnsn. ff_h_mdr_nonzero_columnsn + S (mdr_a_nonzero_columns) = S ((S (mdr_i_nonzero_columns)) * Cc)) /\ exists ff_q_mdr_nonzero_columnsn. Cb = ff_q_mdr_nonzero_columnsn * S ((S (mdr_i_nonzero_columns)) * Cc) + (mdr_a_nonzero_columns)))) -> (((((forall fom_index_mrf_nonzero_sourcerowsbound. (exists fom_gap_mrf_nonzero_sourcerowsbound_index_bound. fom_gap_mrf_nonzero_sourcerowsbound_index_bound + S (fom_index_mrf_nonzero_sourcerowsbound) = q) -> exists fom_value_mrf_nonzero_sourcerowsbound. ((((exists fom_beta_height_mrf_nonzero_sourcerowsbound_entry. fom_beta_height_mrf_nonzero_sourcerowsbound_entry + S (fom_value_mrf_nonzero_sourcerowsbound) = S ((S (fom_index_mrf_nonzero_sourcerowsbound)) * rc)) /\ exists fom_beta_quotient_mrf_nonzero_sourcerowsbound_entry. rb = fom_beta_quotient_mrf_nonzero_sourcerowsbound_entry * S ((S (fom_index_mrf_nonzero_sourcerowsbound)) * rc) + (fom_value_mrf_nonzero_sourcerowsbound))) /\ (exists fom_gap_mrf_nonzero_sourcerowsbound_value_bound. fom_gap_mrf_nonzero_sourcerowsbound_value_bound + S (fom_value_mrf_nonzero_sourcerowsbound) = r))) /\ (forall mdr_i_nonzero_sourcerowsdistinct mdr_j_nonzero_sourcerowsdistinct mdr_a_nonzero_sourcerowsdistinct. (exists mdr_gap_nonzero_sourcerowsdistincti. mdr_gap_nonzero_sourcerowsdistincti + S (mdr_i_nonzero_sourcerowsdistinct) = (q)) -> (exists mdr_gap_nonzero_sourcerowsdistinctj. mdr_gap_nonzero_sourcerowsdistinctj + S (mdr_j_nonzero_sourcerowsdistinct) = (q)) -> (((exists ff_h_mdr_nonzero_sourcerowsdistinctfirst. ff_h_mdr_nonzero_sourcerowsdistinctfirst + S (mdr_a_nonzero_sourcerowsdistinct) = S ((S (mdr_i_nonzero_sourcerowsdistinct)) * rc)) /\ exists ff_q_mdr_nonzero_sourcerowsdistinctfirst. rb = ff_q_mdr_nonzero_sourcerowsdistinctfirst * S ((S (mdr_i_nonzero_sourcerowsdistinct)) * rc) + (mdr_a_nonzero_sourcerowsdistinct))) -> (((exists ff_h_mdr_nonzero_sourcerowsdistinctsecond. ff_h_mdr_nonzero_sourcerowsdistinctsecond + S (mdr_a_nonzero_sourcerowsdistinct) = S ((S (mdr_j_nonzero_sourcerowsdistinct)) * rc)) /\ exists ff_q_mdr_nonzero_sourcerowsdistinctsecond. rb = ff_q_mdr_nonzero_sourcerowsdistinctsecond * S ((S (mdr_j_nonzero_sourcerowsdistinct)) * rc) + (mdr_a_nonzero_sourcerowsdistinct))) -> mdr_i_nonzero_sourcerowsdistinct = mdr_j_nonzero_sourcerowsdistinct))) /\ ((((forall fom_index_mrf_nonzero_sourcecolumnsbound. (exists fom_gap_mrf_nonzero_sourcecolumnsbound_index_bound. fom_gap_mrf_nonzero_sourcecolumnsbound_index_bound + S (fom_index_mrf_nonzero_sourcecolumnsbound) = q) -> exists fom_value_mrf_nonzero_sourcecolumnsbound. ((((exists fom_beta_height_mrf_nonzero_sourcecolumnsbound_entry. fom_beta_height_mrf_nonzero_sourcecolumnsbound_entry + S (fom_value_mrf_nonzero_sourcecolumnsbound) = S ((S (fom_index_mrf_nonzero_sourcecolumnsbound)) * cc)) /\ exists fom_beta_quotient_mrf_nonzero_sourcecolumnsbound_entry. cb = fom_beta_quotient_mrf_nonzero_sourcecolumnsbound_entry * S ((S (fom_index_mrf_nonzero_sourcecolumnsbound)) * cc) + (fom_value_mrf_nonzero_sourcecolumnsbound))) /\ (exists fom_gap_mrf_nonzero_sourcecolumnsbound_value_bound. fom_gap_mrf_nonzero_sourcecolumnsbound_value_bound + S (fom_value_mrf_nonzero_sourcecolumnsbound) = w))) /\ (forall mdr_i_nonzero_sourcecolumnsdistinct mdr_j_nonzero_sourcecolumnsdistinct mdr_a_nonzero_sourcecolumnsdistinct. (exists mdr_gap_nonzero_sourcecolumnsdistincti. mdr_gap_nonzero_sourcecolumnsdistincti + S (mdr_i_nonzero_sourcecolumnsdistinct) = (q)) -> (exists mdr_gap_nonzero_sourcecolumnsdistinctj. mdr_gap_nonzero_sourcecolumnsdistinctj + S (mdr_j_nonzero_sourcecolumnsdistinct) = (q)) -> (((exists ff_h_mdr_nonzero_sourcecolumnsdistinctfirst. ff_h_mdr_nonzero_sourcecolumnsdistinctfirst + S (mdr_a_nonzero_sourcecolumnsdistinct) = S ((S (mdr_i_nonzero_sourcecolumnsdistinct)) * cc)) /\ exists ff_q_mdr_nonzero_sourcecolumnsdistinctfirst. cb = ff_q_mdr_nonzero_sourcecolumnsdistinctfirst * S ((S (mdr_i_nonzero_sourcecolumnsdistinct)) * cc) + (mdr_a_nonzero_sourcecolumnsdistinct))) -> (((exists ff_h_mdr_nonzero_sourcecolumnsdistinctsecond. ff_h_mdr_nonzero_sourcecolumnsdistinctsecond + S (mdr_a_nonzero_sourcecolumnsdistinct) = S ((S (mdr_j_nonzero_sourcecolumnsdistinct)) * cc)) /\ exists ff_q_mdr_nonzero_sourcecolumnsdistinctsecond. cb = ff_q_mdr_nonzero_sourcecolumnsdistinctsecond * S ((S (mdr_j_nonzero_sourcecolumnsdistinct)) * cc) + (mdr_a_nonzero_sourcecolumnsdistinct))) -> mdr_i_nonzero_sourcecolumnsdistinct = mdr_j_nonzero_sourcecolumnsdistinct))) /\ (exists mdr_p_nonzero_sourcenonzero mdr_n_nonzero_sourcenonzero. ((exists mdr_ub_nonzero_sourcenonzeroevaluation mdr_uc_nonzero_sourcenonzeroevaluation mdr_vb_nonzero_sourcenonzeroevaluation mdr_vc_nonzero_sourcenonzeroevaluation. ((((forall mdr_i_nonzero_sourcenonzeroevaluationmatrixpositive. (exists mdr_gap_nonzero_sourcenonzeroevaluationmatrixpositivebound. mdr_gap_nonzero_sourcenonzeroevaluationmatrixpositivebound + S (mdr_i_nonzero_sourcenonzeroevaluationmatrixpositive) = ((q) * (q))) -> exists mdr_a_nonzero_sourcenonzeroevaluationmatrixpositive. (((exists mdr_r_nonzero_sourcenonzeroevaluationmatrixpositivepoint mdr_s_nonzero_sourcenonzeroevaluationmatrixpositivepoint mdr_u_nonzero_sourcenonzeroevaluationmatrixpositivepoint mdr_v_nonzero_sourcenonzeroevaluationmatrixpositivepoint. ((mdr_i_nonzero_sourcenonzeroevaluationmatrixpositive = (q) * mdr_r_nonzero_sourcenonzeroevaluationmatrixpositivepoint + mdr_s_nonzero_sourcenonzeroevaluationmatrixpositivepoint) /\ ((exists mdr_gap_nonzero_sourcenonzeroevaluationmatrixpositivepointcolumn. mdr_gap_nonzero_sourcenonzeroevaluationmatrixpositivepointcolumn + S (mdr_s_nonzero_sourcenonzeroevaluationmatrixpositivepoint) = (q)) /\ ((((exists ff_h_mdr_nonzero_sourcenonzeroevaluationmatrixpositivepointrow_index. ff_h_mdr_nonzero_sourcenonzeroevaluationmatrixpositivepointrow_index + S (mdr_u_nonzero_sourcenonzeroevaluationmatrixpositivepoint) = S ((S (mdr_r_nonzero_sourcenonzeroevaluationmatrixpositivepoint)) * rc)) /\ exists ff_q_mdr_nonzero_sourcenonzeroevaluationmatrixpositivepointrow_index. rb = ff_q_mdr_nonzero_sourcenonzeroevaluationmatrixpositivepointrow_index * S ((S (mdr_r_nonzero_sourcenonzeroevaluationmatrixpositivepoint)) * rc) + (mdr_u_nonzero_sourcenonzeroevaluationmatrixpositivepoint))) /\ ((((exists ff_h_mdr_nonzero_sourcenonzeroevaluationmatrixpositivepointcolumn_index. ff_h_mdr_nonzero_sourcenonzeroevaluationmatrixpositivepointcolumn_index + S (mdr_v_nonzero_sourcenonzeroevaluationmatrixpositivepoint) = S ((S (mdr_s_nonzero_sourcenonzeroevaluationmatrixpositivepoint)) * cc)) /\ exists ff_q_mdr_nonzero_sourcenonzeroevaluationmatrixpositivepointcolumn_index. cb = ff_q_mdr_nonzero_sourcenonzeroevaluationmatrixpositivepointcolumn_index * S ((S (mdr_s_nonzero_sourcenonzeroevaluationmatrixpositivepoint)) * cc) + (mdr_v_nonzero_sourcenonzeroevaluationmatrixpositivepoint))) /\ (((exists ff_h_mdr_nonzero_sourcenonzeroevaluationmatrixpositivepointsource. ff_h_mdr_nonzero_sourcenonzeroevaluationmatrixpositivepointsource + S (mdr_a_nonzero_sourcenonzeroevaluationmatrixpositive) = S ((S ((mdr_u_nonzero_sourcenonzeroevaluationmatrixpositivepoint) * (w) + (mdr_v_nonzero_sourcenonzeroevaluationmatrixpositivepoint))) * pc)) /\ exists ff_q_mdr_nonzero_sourcenonzeroevaluationmatrixpositivepointsource. pb = ff_q_mdr_nonzero_sourcenonzeroevaluationmatrixpositivepointsource * S ((S ((mdr_u_nonzero_sourcenonzeroevaluationmatrixpositivepoint) * (w) + (mdr_v_nonzero_sourcenonzeroevaluationmatrixpositivepoint))) * pc) + (mdr_a_nonzero_sourcenonzeroevaluationmatrixpositive)))))))) /\ (((exists ff_h_mdr_nonzero_sourcenonzeroevaluationmatrixpositiveoutput. ff_h_mdr_nonzero_sourcenonzeroevaluationmatrixpositiveoutput + S (mdr_a_nonzero_sourcenonzeroevaluationmatrixpositive) = S ((S (mdr_i_nonzero_sourcenonzeroevaluationmatrixpositive)) * mdr_uc_nonzero_sourcenonzeroevaluation)) /\ exists ff_q_mdr_nonzero_sourcenonzeroevaluationmatrixpositiveoutput. mdr_ub_nonzero_sourcenonzeroevaluation = ff_q_mdr_nonzero_sourcenonzeroevaluationmatrixpositiveoutput * S ((S (mdr_i_nonzero_sourcenonzeroevaluationmatrixpositive)) * mdr_uc_nonzero_sourcenonzeroevaluation) + (mdr_a_nonzero_sourcenonzeroevaluationmatrixpositive)))))) /\ (forall mdr_i_nonzero_sourcenonzeroevaluationmatrixnegative. (exists mdr_gap_nonzero_sourcenonzeroevaluationmatrixnegativebound. mdr_gap_nonzero_sourcenonzeroevaluationmatrixnegativebound + S (mdr_i_nonzero_sourcenonzeroevaluationmatrixnegative) = ((q) * (q))) -> exists mdr_a_nonzero_sourcenonzeroevaluationmatrixnegative. (((exists mdr_r_nonzero_sourcenonzeroevaluationmatrixnegativepoint mdr_s_nonzero_sourcenonzeroevaluationmatrixnegativepoint mdr_u_nonzero_sourcenonzeroevaluationmatrixnegativepoint mdr_v_nonzero_sourcenonzeroevaluationmatrixnegativepoint. ((mdr_i_nonzero_sourcenonzeroevaluationmatrixnegative = (q) * mdr_r_nonzero_sourcenonzeroevaluationmatrixnegativepoint + mdr_s_nonzero_sourcenonzeroevaluationmatrixnegativepoint) /\ ((exists mdr_gap_nonzero_sourcenonzeroevaluationmatrixnegativepointcolumn. mdr_gap_nonzero_sourcenonzeroevaluationmatrixnegativepointcolumn + S (mdr_s_nonzero_sourcenonzeroevaluationmatrixnegativepoint) = (q)) /\ ((((exists ff_h_mdr_nonzero_sourcenonzeroevaluationmatrixnegativepointrow_index. ff_h_mdr_nonzero_sourcenonzeroevaluationmatrixnegativepointrow_index + S (mdr_u_nonzero_sourcenonzeroevaluationmatrixnegativepoint) = S ((S (mdr_r_nonzero_sourcenonzeroevaluationmatrixnegativepoint)) * rc)) /\ exists ff_q_mdr_nonzero_sourcenonzeroevaluationmatrixnegativepointrow_index. rb = ff_q_mdr_nonzero_sourcenonzeroevaluationmatrixnegativepointrow_index * S ((S (mdr_r_nonzero_sourcenonzeroevaluationmatrixnegativepoint)) * rc) + (mdr_u_nonzero_sourcenonzeroevaluationmatrixnegativepoint))) /\ ((((exists ff_h_mdr_nonzero_sourcenonzeroevaluationmatrixnegativepointcolumn_index. ff_h_mdr_nonzero_sourcenonzeroevaluationmatrixnegativepointcolumn_index + S (mdr_v_nonzero_sourcenonzeroevaluationmatrixnegativepoint) = S ((S (mdr_s_nonzero_sourcenonzeroevaluationmatrixnegativepoint)) * cc)) /\ exists ff_q_mdr_nonzero_sourcenonzeroevaluationmatrixnegativepointcolumn_index. cb = ff_q_mdr_nonzero_sourcenonzeroevaluationmatrixnegativepointcolumn_index * S ((S (mdr_s_nonzero_sourcenonzeroevaluationmatrixnegativepoint)) * cc) + (mdr_v_nonzero_sourcenonzeroevaluationmatrixnegativepoint))) /\ (((exists ff_h_mdr_nonzero_sourcenonzeroevaluationmatrixnegativepointsource. ff_h_mdr_nonzero_sourcenonzeroevaluationmatrixnegativepointsource + S (mdr_a_nonzero_sourcenonzeroevaluationmatrixnegative) = S ((S ((mdr_u_nonzero_sourcenonzeroevaluationmatrixnegativepoint) * (w) + (mdr_v_nonzero_sourcenonzeroevaluationmatrixnegativepoint))) * nc)) /\ exists ff_q_mdr_nonzero_sourcenonzeroevaluationmatrixnegativepointsource. nb = ff_q_mdr_nonzero_sourcenonzeroevaluationmatrixnegativepointsource * S ((S ((mdr_u_nonzero_sourcenonzeroevaluationmatrixnegativepoint) * (w) + (mdr_v_nonzero_sourcenonzeroevaluationmatrixnegativepoint))) * nc) + (mdr_a_nonzero_sourcenonzeroevaluationmatrixnegative)))))))) /\ (((exists ff_h_mdr_nonzero_sourcenonzeroevaluationmatrixnegativeoutput. ff_h_mdr_nonzero_sourcenonzeroevaluationmatrixnegativeoutput + S (mdr_a_nonzero_sourcenonzeroevaluationmatrixnegative) = S ((S (mdr_i_nonzero_sourcenonzeroevaluationmatrixnegative)) * mdr_vc_nonzero_sourcenonzeroevaluation)) /\ exists ff_q_mdr_nonzero_sourcenonzeroevaluationmatrixnegativeoutput. mdr_vb_nonzero_sourcenonzeroevaluation = ff_q_mdr_nonzero_sourcenonzeroevaluationmatrixnegativeoutput * S ((S (mdr_i_nonzero_sourcenonzeroevaluationmatrixnegative)) * mdr_vc_nonzero_sourcenonzeroevaluation) + (mdr_a_nonzero_sourcenonzeroevaluationmatrixnegative)))))))) /\ (exists mdr_b_nonzero_sourcenonzeroevaluationdeterminant mdr_c_nonzero_sourcenonzeroevaluationdeterminant mdr_l_nonzero_sourcenonzeroevaluationdeterminant mdr_i_nonzero_sourcenonzeroevaluationdeterminant. ((forall mdr_i_nonzero_sourcenonzeroevaluationdeterminanth. (exists mdr_gap_nonzero_sourcenonzeroevaluationdeterminanthi. mdr_gap_nonzero_sourcenonzeroevaluationdeterminanthi + S (mdr_i_nonzero_sourcenonzeroevaluationdeterminanth) = (mdr_l_nonzero_sourcenonzeroevaluationdeterminant)) -> exists mdr_d_nonzero_sourcenonzeroevaluationdeterminanth mdr_pb_nonzero_sourcenonzeroevaluationdeterminanth mdr_pc_nonzero_sourcenonzeroevaluationdeterminanth mdr_nb_nonzero_sourcenonzeroevaluationdeterminanth mdr_nc_nonzero_sourcenonzeroevaluationdeterminanth mdr_p_nonzero_sourcenonzeroevaluationdeterminanth mdr_n_nonzero_sourcenonzeroevaluationdeterminanth. ((exists mdr_z_nonzero_sourcenonzeroevaluationdeterminanthr. ((exists mdr_a_nonzero_sourcenonzeroevaluationdeterminanthrc mdr_b_nonzero_sourcenonzeroevaluationdeterminanthrc mdr_c_nonzero_sourcenonzeroevaluationdeterminanthrc mdr_e_nonzero_sourcenonzeroevaluationdeterminanthrc mdr_f_nonzero_sourcenonzeroevaluationdeterminanthrc. ((mdr_a_nonzero_sourcenonzeroevaluationdeterminanthrc = ((mdr_d_nonzero_sourcenonzeroevaluationdeterminanth) + (mdr_pb_nonzero_sourcenonzeroevaluationdeterminanth)) * S ((mdr_d_nonzero_sourcenonzeroevaluationdeterminanth) + (mdr_pb_nonzero_sourcenonzeroevaluationdeterminanth)) + ((mdr_pb_nonzero_sourcenonzeroevaluationdeterminanth) + (mdr_pb_nonzero_sourcenonzeroevaluationdeterminanth))) /\ ((mdr_b_nonzero_sourcenonzeroevaluationdeterminanthrc = ((mdr_pc_nonzero_sourcenonzeroevaluationdeterminanth) + (mdr_nb_nonzero_sourcenonzeroevaluationdeterminanth)) * S ((mdr_pc_nonzero_sourcenonzeroevaluationdeterminanth) + (mdr_nb_nonzero_sourcenonzeroevaluationdeterminanth)) + ((mdr_nb_nonzero_sourcenonzeroevaluationdeterminanth) + (mdr_nb_nonzero_sourcenonzeroevaluationdeterminanth))) /\ ((mdr_c_nonzero_sourcenonzeroevaluationdeterminanthrc = ((mdr_a_nonzero_sourcenonzeroevaluationdeterminanthrc) + (mdr_b_nonzero_sourcenonzeroevaluationdeterminanthrc)) * S ((mdr_a_nonzero_sourcenonzeroevaluationdeterminanthrc) + (mdr_b_nonzero_sourcenonzeroevaluationdeterminanthrc)) + ((mdr_b_nonzero_sourcenonzeroevaluationdeterminanthrc) + (mdr_b_nonzero_sourcenonzeroevaluationdeterminanthrc))) /\ ((mdr_e_nonzero_sourcenonzeroevaluationdeterminanthrc = ((mdr_p_nonzero_sourcenonzeroevaluationdeterminanth) + (mdr_n_nonzero_sourcenonzeroevaluationdeterminanth)) * S ((mdr_p_nonzero_sourcenonzeroevaluationdeterminanth) + (mdr_n_nonzero_sourcenonzeroevaluationdeterminanth)) + ((mdr_n_nonzero_sourcenonzeroevaluationdeterminanth) + (mdr_n_nonzero_sourcenonzeroevaluationdeterminanth))) /\ ((mdr_f_nonzero_sourcenonzeroevaluationdeterminanthrc = ((mdr_nc_nonzero_sourcenonzeroevaluationdeterminanth) + (mdr_e_nonzero_sourcenonzeroevaluationdeterminanthrc)) * S ((mdr_nc_nonzero_sourcenonzeroevaluationdeterminanth) + (mdr_e_nonzero_sourcenonzeroevaluationdeterminanthrc)) + ((mdr_e_nonzero_sourcenonzeroevaluationdeterminanthrc) + (mdr_e_nonzero_sourcenonzeroevaluationdeterminanthrc))) /\ ((mdr_z_nonzero_sourcenonzeroevaluationdeterminanthr) = ((mdr_c_nonzero_sourcenonzeroevaluationdeterminanthrc) + (mdr_f_nonzero_sourcenonzeroevaluationdeterminanthrc)) * S ((mdr_c_nonzero_sourcenonzeroevaluationdeterminanthrc) + (mdr_f_nonzero_sourcenonzeroevaluationdeterminanthrc)) + ((mdr_f_nonzero_sourcenonzeroevaluationdeterminanthrc) + (mdr_f_nonzero_sourcenonzeroevaluationdeterminanthrc))))))))) /\ (((exists ff_h_mdr_nonzero_sourcenonzeroevaluationdeterminanthrb. ff_h_mdr_nonzero_sourcenonzeroevaluationdeterminanthrb + S (mdr_z_nonzero_sourcenonzeroevaluationdeterminanthr) = S ((S (mdr_i_nonzero_sourcenonzeroevaluationdeterminanth)) * mdr_c_nonzero_sourcenonzeroevaluationdeterminant)) /\ exists ff_q_mdr_nonzero_sourcenonzeroevaluationdeterminanthrb. mdr_b_nonzero_sourcenonzeroevaluationdeterminant = ff_q_mdr_nonzero_sourcenonzeroevaluationdeterminanthrb * S ((S (mdr_i_nonzero_sourcenonzeroevaluationdeterminanth)) * mdr_c_nonzero_sourcenonzeroevaluationdeterminant) + (mdr_z_nonzero_sourcenonzeroevaluationdeterminanthr))))) /\ (((((mdr_d_nonzero_sourcenonzeroevaluationdeterminanth) = 0) /\ (((mdr_p_nonzero_sourcenonzeroevaluationdeterminanth) = 1) /\ ((mdr_n_nonzero_sourcenonzeroevaluationdeterminanth) = 0))) \/ exists mdr_q_nonzero_sourcenonzeroevaluationdeterminanths mdr_eb_nonzero_sourcenonzeroevaluationdeterminanths mdr_ec_nonzero_sourcenonzeroevaluationdeterminanths mdr_fb_nonzero_sourcenonzeroevaluationdeterminanths mdr_fc_nonzero_sourcenonzeroevaluationdeterminanths. (((mdr_d_nonzero_sourcenonzeroevaluationdeterminanth) = S (mdr_q_nonzero_sourcenonzeroevaluationdeterminanths)) /\ ((forall mdr_j_nonzero_sourcenonzeroevaluationdeterminanthsc. (exists mdr_gap_nonzero_sourcenonzeroevaluationdeterminanthscj. mdr_gap_nonzero_sourcenonzeroevaluationdeterminanthscj + S (mdr_j_nonzero_sourcenonzeroevaluationdeterminanthsc) = (S (mdr_q_nonzero_sourcenonzeroevaluationdeterminanths))) -> exists mdr_i_nonzero_sourcenonzeroevaluationdeterminanthsc mdr_up_nonzero_sourcenonzeroevaluationdeterminanthsc mdr_us_nonzero_sourcenonzeroevaluationdeterminanthsc mdr_un_nonzero_sourcenonzeroevaluationdeterminanthsc mdr_ut_nonzero_sourcenonzeroevaluationdeterminanthsc mdr_p_nonzero_sourcenonzeroevaluationdeterminanthsc mdr_n_nonzero_sourcenonzeroevaluationdeterminanthsc. ((exists mdr_gap_nonzero_sourcenonzeroevaluationdeterminanthsci. mdr_gap_nonzero_sourcenonzeroevaluationdeterminanthsci + S (mdr_i_nonzero_sourcenonzeroevaluationdeterminanthsc) = (mdr_i_nonzero_sourcenonzeroevaluationdeterminanth)) /\ ((exists mdr_z_nonzero_sourcenonzeroevaluationdeterminanthscr. ((exists mdr_a_nonzero_sourcenonzeroevaluationdeterminanthscrc mdr_b_nonzero_sourcenonzeroevaluationdeterminanthscrc mdr_c_nonzero_sourcenonzeroevaluationdeterminanthscrc mdr_e_nonzero_sourcenonzeroevaluationdeterminanthscrc mdr_f_nonzero_sourcenonzeroevaluationdeterminanthscrc. ((mdr_a_nonzero_sourcenonzeroevaluationdeterminanthscrc = ((mdr_q_nonzero_sourcenonzeroevaluationdeterminanths) + (mdr_up_nonzero_sourcenonzeroevaluationdeterminanthsc)) * S ((mdr_q_nonzero_sourcenonzeroevaluationdeterminanths) + (mdr_up_nonzero_sourcenonzeroevaluationdeterminanthsc)) + ((mdr_up_nonzero_sourcenonzeroevaluationdeterminanthsc) + (mdr_up_nonzero_sourcenonzeroevaluationdeterminanthsc))) /\ ((mdr_b_nonzero_sourcenonzeroevaluationdeterminanthscrc = ((mdr_us_nonzero_sourcenonzeroevaluationdeterminanthsc) + (mdr_un_nonzero_sourcenonzeroevaluationdeterminanthsc)) * S ((mdr_us_nonzero_sourcenonzeroevaluationdeterminanthsc) + (mdr_un_nonzero_sourcenonzeroevaluationdeterminanthsc)) + ((mdr_un_nonzero_sourcenonzeroevaluationdeterminanthsc) + (mdr_un_nonzero_sourcenonzeroevaluationdeterminanthsc))) /\ ((mdr_c_nonzero_sourcenonzeroevaluationdeterminanthscrc = ((mdr_a_nonzero_sourcenonzeroevaluationdeterminanthscrc) + (mdr_b_nonzero_sourcenonzeroevaluationdeterminanthscrc)) * S ((mdr_a_nonzero_sourcenonzeroevaluationdeterminanthscrc) + (mdr_b_nonzero_sourcenonzeroevaluationdeterminanthscrc)) + ((mdr_b_nonzero_sourcenonzeroevaluationdeterminanthscrc) + (mdr_b_nonzero_sourcenonzeroevaluationdeterminanthscrc))) /\ ((mdr_e_nonzero_sourcenonzeroevaluationdeterminanthscrc = ((mdr_p_nonzero_sourcenonzeroevaluationdeterminanthsc) + (mdr_n_nonzero_sourcenonzeroevaluationdeterminanthsc)) * S ((mdr_p_nonzero_sourcenonzeroevaluationdeterminanthsc) + (mdr_n_nonzero_sourcenonzeroevaluationdeterminanthsc)) + ((mdr_n_nonzero_sourcenonzeroevaluationdeterminanthsc) + (mdr_n_nonzero_sourcenonzeroevaluationdeterminanthsc))) /\ ((mdr_f_nonzero_sourcenonzeroevaluationdeterminanthscrc = ((mdr_ut_nonzero_sourcenonzeroevaluationdeterminanthsc) + (mdr_e_nonzero_sourcenonzeroevaluationdeterminanthscrc)) * S ((mdr_ut_nonzero_sourcenonzeroevaluationdeterminanthsc) + (mdr_e_nonzero_sourcenonzeroevaluationdeterminanthscrc)) + ((mdr_e_nonzero_sourcenonzeroevaluationdeterminanthscrc) + (mdr_e_nonzero_sourcenonzeroevaluationdeterminanthscrc))) /\ ((mdr_z_nonzero_sourcenonzeroevaluationdeterminanthscr) = ((mdr_c_nonzero_sourcenonzeroevaluationdeterminanthscrc) + (mdr_f_nonzero_sourcenonzeroevaluationdeterminanthscrc)) * S ((mdr_c_nonzero_sourcenonzeroevaluationdeterminanthscrc) + (mdr_f_nonzero_sourcenonzeroevaluationdeterminanthscrc)) + ((mdr_f_nonzero_sourcenonzeroevaluationdeterminanthscrc) + (mdr_f_nonzero_sourcenonzeroevaluationdeterminanthscrc))))))))) /\ (((exists ff_h_mdr_nonzero_sourcenonzeroevaluationdeterminanthscrb. ff_h_mdr_nonzero_sourcenonzeroevaluationdeterminanthscrb + S (mdr_z_nonzero_sourcenonzeroevaluationdeterminanthscr) = S ((S (mdr_i_nonzero_sourcenonzeroevaluationdeterminanthsc)) * mdr_c_nonzero_sourcenonzeroevaluationdeterminant)) /\ exists ff_q_mdr_nonzero_sourcenonzeroevaluationdeterminanthscrb. mdr_b_nonzero_sourcenonzeroevaluationdeterminant = ff_q_mdr_nonzero_sourcenonzeroevaluationdeterminanthscrb * S ((S (mdr_i_nonzero_sourcenonzeroevaluationdeterminanthsc)) * mdr_c_nonzero_sourcenonzeroevaluationdeterminant) + (mdr_z_nonzero_sourcenonzeroevaluationdeterminanthscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_nonzero_sourcenonzeroevaluationdeterminanthscm_positive. (exists ff_gap_mdm_lt_mdr_nonzero_sourcenonzeroevaluationdeterminanthscm_positive_index_bound. ff_gap_mdm_lt_mdr_nonzero_sourcenonzeroevaluationdeterminanthscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_nonzero_sourcenonzeroevaluationdeterminanthscm_positive) = ((mdr_q_nonzero_sourcenonzeroevaluationdeterminanths) * (mdr_q_nonzero_sourcenonzeroevaluationdeterminanths))) -> exists ff_row_mdm_prefix_mdr_nonzero_sourcenonzeroevaluationdeterminanthscm_positive ff_column_mdm_prefix_mdr_nonzero_sourcenonzeroevaluationdeterminanthscm_positive ff_value_mdm_prefix_mdr_nonzero_sourcenonzeroevaluationdeterminanthscm_positive. (ff_index_mdm_prefix_mdr_nonzero_sourcenonzeroevaluationdeterminanthscm_positive = (mdr_q_nonzero_sourcenonzeroevaluationdeterminanths) * ff_row_mdm_prefix_mdr_nonzero_sourcenonzeroevaluationdeterminanthscm_positive + ff_column_mdm_prefix_mdr_nonzero_sourcenonzeroevaluationdeterminanthscm_positive /\ ((exists ff_gap_mdm_lt_mdr_nonzero_sourcenonzeroevaluationdeterminanthscm_positive_column_bound. ff_gap_mdm_lt_mdr_nonzero_sourcenonzeroevaluationdeterminanthscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_nonzero_sourcenonzeroevaluationdeterminanthscm_positive) = (mdr_q_nonzero_sourcenonzeroevaluationdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_nonzero_sourcenonzeroevaluationdeterminanthscm_positive_cell ff_column_mdm_cell_mdr_nonzero_sourcenonzeroevaluationdeterminanthscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_nonzero_sourcenonzeroevaluationdeterminanthscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_nonzero_sourcenonzeroevaluationdeterminanthscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_nonzero_sourcenonzeroevaluationdeterminanthscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_nonzero_sourcenonzeroevaluationdeterminanthscm_positive_cell = ff_row_mdm_prefix_mdr_nonzero_sourcenonzeroevaluationdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_nonzero_sourcenonzeroevaluationdeterminanthscm_positive_cell_row_after. ff_gap_mdm_le_mdr_nonzero_sourcenonzeroevaluationdeterminanthscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_nonzero_sourcenonzeroevaluationdeterminanthscm_positive)) /\ ff_row_mdm_cell_mdr_nonzero_sourcenonzeroevaluationdeterminanthscm_positive_cell = S ff_row_mdm_prefix_mdr_nonzero_sourcenonzeroevaluationdeterminanthscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_nonzero_sourcenonzeroevaluationdeterminanthscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_nonzero_sourcenonzeroevaluationdeterminanthscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_nonzero_sourcenonzeroevaluationdeterminanthscm_positive) = (mdr_j_nonzero_sourcenonzeroevaluationdeterminanthsc)) /\ ff_column_mdm_cell_mdr_nonzero_sourcenonzeroevaluationdeterminanthscm_positive_cell = ff_column_mdm_prefix_mdr_nonzero_sourcenonzeroevaluationdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_nonzero_sourcenonzeroevaluationdeterminanthscm_positive_cell_column_after. ff_gap_mdm_le_mdr_nonzero_sourcenonzeroevaluationdeterminanthscm_positive_cell_column_after + (mdr_j_nonzero_sourcenonzeroevaluationdeterminanthsc) = (ff_column_mdm_prefix_mdr_nonzero_sourcenonzeroevaluationdeterminanthscm_positive)) /\ ff_column_mdm_cell_mdr_nonzero_sourcenonzeroevaluationdeterminanthscm_positive_cell = S ff_column_mdm_prefix_mdr_nonzero_sourcenonzeroevaluationdeterminanthscm_positive))) /\ (((exists ff_h_mdm_mdr_nonzero_sourcenonzeroevaluationdeterminanthscm_positive_cell_source. ff_h_mdm_mdr_nonzero_sourcenonzeroevaluationdeterminanthscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_nonzero_sourcenonzeroevaluationdeterminanthscm_positive) = S ((S ((ff_row_mdm_cell_mdr_nonzero_sourcenonzeroevaluationdeterminanthscm_positive_cell) * (S (mdr_q_nonzero_sourcenonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_nonzero_sourcenonzeroevaluationdeterminanthscm_positive_cell))) * mdr_pc_nonzero_sourcenonzeroevaluationdeterminanth)) /\ exists ff_q_mdm_mdr_nonzero_sourcenonzeroevaluationdeterminanthscm_positive_cell_source. mdr_pb_nonzero_sourcenonzeroevaluationdeterminanth = ff_q_mdm_mdr_nonzero_sourcenonzeroevaluationdeterminanthscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_nonzero_sourcenonzeroevaluationdeterminanthscm_positive_cell) * (S (mdr_q_nonzero_sourcenonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_nonzero_sourcenonzeroevaluationdeterminanthscm_positive_cell))) * mdr_pc_nonzero_sourcenonzeroevaluationdeterminanth) + (ff_value_mdm_prefix_mdr_nonzero_sourcenonzeroevaluationdeterminanthscm_positive)))))) /\ (((exists ff_h_mdm_mdr_nonzero_sourcenonzeroevaluationdeterminanthscm_positive_target. ff_h_mdm_mdr_nonzero_sourcenonzeroevaluationdeterminanthscm_positive_target + S (ff_value_mdm_prefix_mdr_nonzero_sourcenonzeroevaluationdeterminanthscm_positive) = S ((S (ff_index_mdm_prefix_mdr_nonzero_sourcenonzeroevaluationdeterminanthscm_positive)) * mdr_us_nonzero_sourcenonzeroevaluationdeterminanthsc)) /\ exists ff_q_mdm_mdr_nonzero_sourcenonzeroevaluationdeterminanthscm_positive_target. mdr_up_nonzero_sourcenonzeroevaluationdeterminanthsc = ff_q_mdm_mdr_nonzero_sourcenonzeroevaluationdeterminanthscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_nonzero_sourcenonzeroevaluationdeterminanthscm_positive)) * mdr_us_nonzero_sourcenonzeroevaluationdeterminanthsc) + (ff_value_mdm_prefix_mdr_nonzero_sourcenonzeroevaluationdeterminanthscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_nonzero_sourcenonzeroevaluationdeterminanthscm_negative. (exists ff_gap_mdm_lt_mdr_nonzero_sourcenonzeroevaluationdeterminanthscm_negative_index_bound. ff_gap_mdm_lt_mdr_nonzero_sourcenonzeroevaluationdeterminanthscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_nonzero_sourcenonzeroevaluationdeterminanthscm_negative) = ((mdr_q_nonzero_sourcenonzeroevaluationdeterminanths) * (mdr_q_nonzero_sourcenonzeroevaluationdeterminanths))) -> exists ff_row_mdm_prefix_mdr_nonzero_sourcenonzeroevaluationdeterminanthscm_negative ff_column_mdm_prefix_mdr_nonzero_sourcenonzeroevaluationdeterminanthscm_negative ff_value_mdm_prefix_mdr_nonzero_sourcenonzeroevaluationdeterminanthscm_negative. (ff_index_mdm_prefix_mdr_nonzero_sourcenonzeroevaluationdeterminanthscm_negative = (mdr_q_nonzero_sourcenonzeroevaluationdeterminanths) * ff_row_mdm_prefix_mdr_nonzero_sourcenonzeroevaluationdeterminanthscm_negative + ff_column_mdm_prefix_mdr_nonzero_sourcenonzeroevaluationdeterminanthscm_negative /\ ((exists ff_gap_mdm_lt_mdr_nonzero_sourcenonzeroevaluationdeterminanthscm_negative_column_bound. ff_gap_mdm_lt_mdr_nonzero_sourcenonzeroevaluationdeterminanthscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_nonzero_sourcenonzeroevaluationdeterminanthscm_negative) = (mdr_q_nonzero_sourcenonzeroevaluationdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_nonzero_sourcenonzeroevaluationdeterminanthscm_negative_cell ff_column_mdm_cell_mdr_nonzero_sourcenonzeroevaluationdeterminanthscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_nonzero_sourcenonzeroevaluationdeterminanthscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_nonzero_sourcenonzeroevaluationdeterminanthscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_nonzero_sourcenonzeroevaluationdeterminanthscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_nonzero_sourcenonzeroevaluationdeterminanthscm_negative_cell = ff_row_mdm_prefix_mdr_nonzero_sourcenonzeroevaluationdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_nonzero_sourcenonzeroevaluationdeterminanthscm_negative_cell_row_after. ff_gap_mdm_le_mdr_nonzero_sourcenonzeroevaluationdeterminanthscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_nonzero_sourcenonzeroevaluationdeterminanthscm_negative)) /\ ff_row_mdm_cell_mdr_nonzero_sourcenonzeroevaluationdeterminanthscm_negative_cell = S ff_row_mdm_prefix_mdr_nonzero_sourcenonzeroevaluationdeterminanthscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_nonzero_sourcenonzeroevaluationdeterminanthscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_nonzero_sourcenonzeroevaluationdeterminanthscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_nonzero_sourcenonzeroevaluationdeterminanthscm_negative) = (mdr_j_nonzero_sourcenonzeroevaluationdeterminanthsc)) /\ ff_column_mdm_cell_mdr_nonzero_sourcenonzeroevaluationdeterminanthscm_negative_cell = ff_column_mdm_prefix_mdr_nonzero_sourcenonzeroevaluationdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_nonzero_sourcenonzeroevaluationdeterminanthscm_negative_cell_column_after. ff_gap_mdm_le_mdr_nonzero_sourcenonzeroevaluationdeterminanthscm_negative_cell_column_after + (mdr_j_nonzero_sourcenonzeroevaluationdeterminanthsc) = (ff_column_mdm_prefix_mdr_nonzero_sourcenonzeroevaluationdeterminanthscm_negative)) /\ ff_column_mdm_cell_mdr_nonzero_sourcenonzeroevaluationdeterminanthscm_negative_cell = S ff_column_mdm_prefix_mdr_nonzero_sourcenonzeroevaluationdeterminanthscm_negative))) /\ (((exists ff_h_mdm_mdr_nonzero_sourcenonzeroevaluationdeterminanthscm_negative_cell_source. ff_h_mdm_mdr_nonzero_sourcenonzeroevaluationdeterminanthscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_nonzero_sourcenonzeroevaluationdeterminanthscm_negative) = S ((S ((ff_row_mdm_cell_mdr_nonzero_sourcenonzeroevaluationdeterminanthscm_negative_cell) * (S (mdr_q_nonzero_sourcenonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_nonzero_sourcenonzeroevaluationdeterminanthscm_negative_cell))) * mdr_nc_nonzero_sourcenonzeroevaluationdeterminanth)) /\ exists ff_q_mdm_mdr_nonzero_sourcenonzeroevaluationdeterminanthscm_negative_cell_source. mdr_nb_nonzero_sourcenonzeroevaluationdeterminanth = ff_q_mdm_mdr_nonzero_sourcenonzeroevaluationdeterminanthscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_nonzero_sourcenonzeroevaluationdeterminanthscm_negative_cell) * (S (mdr_q_nonzero_sourcenonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_nonzero_sourcenonzeroevaluationdeterminanthscm_negative_cell))) * mdr_nc_nonzero_sourcenonzeroevaluationdeterminanth) + (ff_value_mdm_prefix_mdr_nonzero_sourcenonzeroevaluationdeterminanthscm_negative)))))) /\ (((exists ff_h_mdm_mdr_nonzero_sourcenonzeroevaluationdeterminanthscm_negative_target. ff_h_mdm_mdr_nonzero_sourcenonzeroevaluationdeterminanthscm_negative_target + S (ff_value_mdm_prefix_mdr_nonzero_sourcenonzeroevaluationdeterminanthscm_negative) = S ((S (ff_index_mdm_prefix_mdr_nonzero_sourcenonzeroevaluationdeterminanthscm_negative)) * mdr_ut_nonzero_sourcenonzeroevaluationdeterminanthsc)) /\ exists ff_q_mdm_mdr_nonzero_sourcenonzeroevaluationdeterminanthscm_negative_target. mdr_un_nonzero_sourcenonzeroevaluationdeterminanthsc = ff_q_mdm_mdr_nonzero_sourcenonzeroevaluationdeterminanthscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_nonzero_sourcenonzeroevaluationdeterminanthscm_negative)) * mdr_ut_nonzero_sourcenonzeroevaluationdeterminanthsc) + (ff_value_mdm_prefix_mdr_nonzero_sourcenonzeroevaluationdeterminanthscm_negative))))))))) /\ ((((exists ff_h_mdr_nonzero_sourcenonzeroevaluationdeterminanthscp. ff_h_mdr_nonzero_sourcenonzeroevaluationdeterminanthscp + S (mdr_p_nonzero_sourcenonzeroevaluationdeterminanthsc) = S ((S (mdr_j_nonzero_sourcenonzeroevaluationdeterminanthsc)) * mdr_ec_nonzero_sourcenonzeroevaluationdeterminanths)) /\ exists ff_q_mdr_nonzero_sourcenonzeroevaluationdeterminanthscp. mdr_eb_nonzero_sourcenonzeroevaluationdeterminanths = ff_q_mdr_nonzero_sourcenonzeroevaluationdeterminanthscp * S ((S (mdr_j_nonzero_sourcenonzeroevaluationdeterminanthsc)) * mdr_ec_nonzero_sourcenonzeroevaluationdeterminanths) + (mdr_p_nonzero_sourcenonzeroevaluationdeterminanthsc))) /\ (((exists ff_h_mdr_nonzero_sourcenonzeroevaluationdeterminanthscn. ff_h_mdr_nonzero_sourcenonzeroevaluationdeterminanthscn + S (mdr_n_nonzero_sourcenonzeroevaluationdeterminanthsc) = S ((S (mdr_j_nonzero_sourcenonzeroevaluationdeterminanthsc)) * mdr_fc_nonzero_sourcenonzeroevaluationdeterminanths)) /\ exists ff_q_mdr_nonzero_sourcenonzeroevaluationdeterminanthscn. mdr_fb_nonzero_sourcenonzeroevaluationdeterminanths = ff_q_mdr_nonzero_sourcenonzeroevaluationdeterminanthscn * S ((S (mdr_j_nonzero_sourcenonzeroevaluationdeterminanthsc)) * mdr_fc_nonzero_sourcenonzeroevaluationdeterminanths) + (mdr_n_nonzero_sourcenonzeroevaluationdeterminanthsc)))))))) /\ (exists ff_ub_mce_fold_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf ff_uc_mce_fold_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf ff_vb_mce_fold_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf ff_vc_mce_fold_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf. ((forall ff_index_mce_alternating_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_prefix. (exists ff_gap_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_prefix_index. ff_gap_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_prefix_index + S (ff_index_mce_alternating_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_prefix) = (S (mdr_q_nonzero_sourcenonzeroevaluationdeterminanths))) -> exists ff_ap_mce_alternating_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_prefix ff_an_mce_alternating_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_prefix ff_bp_mce_alternating_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_prefix ff_bn_mce_alternating_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_prefix ff_p_mce_alternating_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_prefix ff_n_mce_alternating_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_prefix. ((((exists ff_h_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_prefix_ap. ff_h_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_prefix_ap + S (ff_ap_mce_alternating_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_prefix)) * mdr_pc_nonzero_sourcenonzeroevaluationdeterminanth)) /\ exists ff_q_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_prefix_ap. mdr_pb_nonzero_sourcenonzeroevaluationdeterminanth = ff_q_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_prefix)) * mdr_pc_nonzero_sourcenonzeroevaluationdeterminanth) + (ff_ap_mce_alternating_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_prefix_an. ff_h_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_prefix_an + S (ff_an_mce_alternating_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_prefix)) * mdr_nc_nonzero_sourcenonzeroevaluationdeterminanth)) /\ exists ff_q_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_prefix_an. mdr_nb_nonzero_sourcenonzeroevaluationdeterminanth = ff_q_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_prefix)) * mdr_nc_nonzero_sourcenonzeroevaluationdeterminanth) + (ff_an_mce_alternating_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_prefix_bp. ff_h_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_prefix_bp + S (ff_bp_mce_alternating_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_prefix)) * mdr_ec_nonzero_sourcenonzeroevaluationdeterminanths)) /\ exists ff_q_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_prefix_bp. mdr_eb_nonzero_sourcenonzeroevaluationdeterminanths = ff_q_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_prefix)) * mdr_ec_nonzero_sourcenonzeroevaluationdeterminanths) + (ff_bp_mce_alternating_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_prefix_bn. ff_h_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_prefix_bn + S (ff_bn_mce_alternating_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_prefix)) * mdr_fc_nonzero_sourcenonzeroevaluationdeterminanths)) /\ exists ff_q_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_prefix_bn. mdr_fb_nonzero_sourcenonzeroevaluationdeterminanths = ff_q_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_prefix)) * mdr_fc_nonzero_sourcenonzeroevaluationdeterminanths) + (ff_bn_mce_alternating_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_prefix_positive. ff_h_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_prefix_positive + S (ff_p_mce_alternating_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_prefix_positive. ff_ub_mce_fold_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf = ff_q_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf) + (ff_p_mce_alternating_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_prefix_negative. ff_h_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_prefix_negative + S (ff_n_mce_alternating_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_prefix_negative. ff_vb_mce_fold_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf = ff_q_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf) + (ff_n_mce_alternating_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_prefix))) /\ (((exists ff_even_mce_term_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_prefix = 2 * ff_even_mce_term_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_prefix_term) /\ (ff_p_mce_alternating_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_prefix = 2 * ff_odd_mce_term_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_positive ff_v_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_positive. ((((exists ff_h_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_positive_start. ff_h_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_positive_start. ff_u_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_positive_start * S ((S (0)) * ff_v_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_positive_terminal. ff_h_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_positive_terminal + S (mdr_p_nonzero_sourcenonzeroevaluationdeterminanth) = S ((S ((S (mdr_q_nonzero_sourcenonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_positive_terminal. ff_u_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_positive_terminal * S ((S ((S (mdr_q_nonzero_sourcenonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_positive) + (mdr_p_nonzero_sourcenonzeroevaluationdeterminanth))) /\ forall ff_i_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_positive. (exists ff_lt_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_positive_bound. ff_lt_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_positive_bound + S ff_i_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_positive = (S (mdr_q_nonzero_sourcenonzeroevaluationdeterminanths))) -> exists ff_a_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_positive ff_r_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_positive ff_s_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_positive. ((((exists ff_h_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_positive_summand. ff_h_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_positive_summand + S (ff_a_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_positive_summand. ff_ub_mce_fold_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf = ff_q_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_positive_summand * S ((S (ff_i_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf) + (ff_a_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_positive_partial. ff_h_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_positive_partial + S (ff_r_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_positive_partial. ff_u_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_positive_partial * S ((S (ff_i_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_positive) + (ff_r_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_positive_successor. ff_h_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_positive_successor + S (ff_s_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_positive) = S ((S (S ff_i_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_positive_successor. ff_u_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_positive_successor * S ((S (S ff_i_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_positive) + (ff_s_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_positive))) /\ ff_s_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_positive = ff_r_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_positive + ff_a_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_positive)))))) /\ (exists ff_u_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_negative ff_v_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_negative. ((((exists ff_h_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_negative_start. ff_h_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_negative_start. ff_u_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_negative_start * S ((S (0)) * ff_v_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_negative_terminal. ff_h_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_negative_terminal + S (mdr_n_nonzero_sourcenonzeroevaluationdeterminanth) = S ((S ((S (mdr_q_nonzero_sourcenonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_negative_terminal. ff_u_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_negative_terminal * S ((S ((S (mdr_q_nonzero_sourcenonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_negative) + (mdr_n_nonzero_sourcenonzeroevaluationdeterminanth))) /\ forall ff_i_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_negative. (exists ff_lt_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_negative_bound. ff_lt_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_negative_bound + S ff_i_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_negative = (S (mdr_q_nonzero_sourcenonzeroevaluationdeterminanths))) -> exists ff_a_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_negative ff_r_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_negative ff_s_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_negative. ((((exists ff_h_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_negative_summand. ff_h_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_negative_summand + S (ff_a_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_negative_summand. ff_vb_mce_fold_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf = ff_q_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_negative_summand * S ((S (ff_i_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf) + (ff_a_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_negative_partial. ff_h_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_negative_partial + S (ff_r_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_negative_partial. ff_u_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_negative_partial * S ((S (ff_i_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_negative) + (ff_r_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_negative_successor. ff_h_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_negative_successor + S (ff_s_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_negative) = S ((S (S ff_i_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_negative_successor. ff_u_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_negative_successor * S ((S (S ff_i_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_negative) + (ff_s_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_negative))) /\ ff_s_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_negative = ff_r_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_negative + ff_a_mce_mdr_nonzero_sourcenonzeroevaluationdeterminanthsf_negative))))))))))))))) /\ ((exists mdr_gap_nonzero_sourcenonzeroevaluationdeterminanti. mdr_gap_nonzero_sourcenonzeroevaluationdeterminanti + S (mdr_i_nonzero_sourcenonzeroevaluationdeterminant) = (mdr_l_nonzero_sourcenonzeroevaluationdeterminant)) /\ (exists mdr_z_nonzero_sourcenonzeroevaluationdeterminantr. ((exists mdr_a_nonzero_sourcenonzeroevaluationdeterminantrc mdr_b_nonzero_sourcenonzeroevaluationdeterminantrc mdr_c_nonzero_sourcenonzeroevaluationdeterminantrc mdr_e_nonzero_sourcenonzeroevaluationdeterminantrc mdr_f_nonzero_sourcenonzeroevaluationdeterminantrc. ((mdr_a_nonzero_sourcenonzeroevaluationdeterminantrc = ((q) + (mdr_ub_nonzero_sourcenonzeroevaluation)) * S ((q) + (mdr_ub_nonzero_sourcenonzeroevaluation)) + ((mdr_ub_nonzero_sourcenonzeroevaluation) + (mdr_ub_nonzero_sourcenonzeroevaluation))) /\ ((mdr_b_nonzero_sourcenonzeroevaluationdeterminantrc = ((mdr_uc_nonzero_sourcenonzeroevaluation) + (mdr_vb_nonzero_sourcenonzeroevaluation)) * S ((mdr_uc_nonzero_sourcenonzeroevaluation) + (mdr_vb_nonzero_sourcenonzeroevaluation)) + ((mdr_vb_nonzero_sourcenonzeroevaluation) + (mdr_vb_nonzero_sourcenonzeroevaluation))) /\ ((mdr_c_nonzero_sourcenonzeroevaluationdeterminantrc = ((mdr_a_nonzero_sourcenonzeroevaluationdeterminantrc) + (mdr_b_nonzero_sourcenonzeroevaluationdeterminantrc)) * S ((mdr_a_nonzero_sourcenonzeroevaluationdeterminantrc) + (mdr_b_nonzero_sourcenonzeroevaluationdeterminantrc)) + ((mdr_b_nonzero_sourcenonzeroevaluationdeterminantrc) + (mdr_b_nonzero_sourcenonzeroevaluationdeterminantrc))) /\ ((mdr_e_nonzero_sourcenonzeroevaluationdeterminantrc = ((mdr_p_nonzero_sourcenonzero) + (mdr_n_nonzero_sourcenonzero)) * S ((mdr_p_nonzero_sourcenonzero) + (mdr_n_nonzero_sourcenonzero)) + ((mdr_n_nonzero_sourcenonzero) + (mdr_n_nonzero_sourcenonzero))) /\ ((mdr_f_nonzero_sourcenonzeroevaluationdeterminantrc = ((mdr_vc_nonzero_sourcenonzeroevaluation) + (mdr_e_nonzero_sourcenonzeroevaluationdeterminantrc)) * S ((mdr_vc_nonzero_sourcenonzeroevaluation) + (mdr_e_nonzero_sourcenonzeroevaluationdeterminantrc)) + ((mdr_e_nonzero_sourcenonzeroevaluationdeterminantrc) + (mdr_e_nonzero_sourcenonzeroevaluationdeterminantrc))) /\ ((mdr_z_nonzero_sourcenonzeroevaluationdeterminantr) = ((mdr_c_nonzero_sourcenonzeroevaluationdeterminantrc) + (mdr_f_nonzero_sourcenonzeroevaluationdeterminantrc)) * S ((mdr_c_nonzero_sourcenonzeroevaluationdeterminantrc) + (mdr_f_nonzero_sourcenonzeroevaluationdeterminantrc)) + ((mdr_f_nonzero_sourcenonzeroevaluationdeterminantrc) + (mdr_f_nonzero_sourcenonzeroevaluationdeterminantrc))))))))) /\ (((exists ff_h_mdr_nonzero_sourcenonzeroevaluationdeterminantrb. ff_h_mdr_nonzero_sourcenonzeroevaluationdeterminantrb + S (mdr_z_nonzero_sourcenonzeroevaluationdeterminantr) = S ((S (mdr_i_nonzero_sourcenonzeroevaluationdeterminant)) * mdr_c_nonzero_sourcenonzeroevaluationdeterminant)) /\ exists ff_q_mdr_nonzero_sourcenonzeroevaluationdeterminantrb. mdr_b_nonzero_sourcenonzeroevaluationdeterminant = ff_q_mdr_nonzero_sourcenonzeroevaluationdeterminantrb * S ((S (mdr_i_nonzero_sourcenonzeroevaluationdeterminant)) * mdr_c_nonzero_sourcenonzeroevaluationdeterminant) + (mdr_z_nonzero_sourcenonzeroevaluationdeterminantr)))))))))) /\ (~(mdr_p_nonzero_sourcenonzero = mdr_n_nonzero_sourcenonzero))))))) -> (((((forall fom_index_mrf_nonzero_targetrowsbound. (exists fom_gap_mrf_nonzero_targetrowsbound_index_bound. fom_gap_mrf_nonzero_targetrowsbound_index_bound + S (fom_index_mrf_nonzero_targetrowsbound) = q) -> exists fom_value_mrf_nonzero_targetrowsbound. ((((exists fom_beta_height_mrf_nonzero_targetrowsbound_entry. fom_beta_height_mrf_nonzero_targetrowsbound_entry + S (fom_value_mrf_nonzero_targetrowsbound) = S ((S (fom_index_mrf_nonzero_targetrowsbound)) * Rc)) /\ exists fom_beta_quotient_mrf_nonzero_targetrowsbound_entry. Rb = fom_beta_quotient_mrf_nonzero_targetrowsbound_entry * S ((S (fom_index_mrf_nonzero_targetrowsbound)) * Rc) + (fom_value_mrf_nonzero_targetrowsbound))) /\ (exists fom_gap_mrf_nonzero_targetrowsbound_value_bound. fom_gap_mrf_nonzero_targetrowsbound_value_bound + S (fom_value_mrf_nonzero_targetrowsbound) = r))) /\ (forall mdr_i_nonzero_targetrowsdistinct mdr_j_nonzero_targetrowsdistinct mdr_a_nonzero_targetrowsdistinct. (exists mdr_gap_nonzero_targetrowsdistincti. mdr_gap_nonzero_targetrowsdistincti + S (mdr_i_nonzero_targetrowsdistinct) = (q)) -> (exists mdr_gap_nonzero_targetrowsdistinctj. mdr_gap_nonzero_targetrowsdistinctj + S (mdr_j_nonzero_targetrowsdistinct) = (q)) -> (((exists ff_h_mdr_nonzero_targetrowsdistinctfirst. ff_h_mdr_nonzero_targetrowsdistinctfirst + S (mdr_a_nonzero_targetrowsdistinct) = S ((S (mdr_i_nonzero_targetrowsdistinct)) * Rc)) /\ exists ff_q_mdr_nonzero_targetrowsdistinctfirst. Rb = ff_q_mdr_nonzero_targetrowsdistinctfirst * S ((S (mdr_i_nonzero_targetrowsdistinct)) * Rc) + (mdr_a_nonzero_targetrowsdistinct))) -> (((exists ff_h_mdr_nonzero_targetrowsdistinctsecond. ff_h_mdr_nonzero_targetrowsdistinctsecond + S (mdr_a_nonzero_targetrowsdistinct) = S ((S (mdr_j_nonzero_targetrowsdistinct)) * Rc)) /\ exists ff_q_mdr_nonzero_targetrowsdistinctsecond. Rb = ff_q_mdr_nonzero_targetrowsdistinctsecond * S ((S (mdr_j_nonzero_targetrowsdistinct)) * Rc) + (mdr_a_nonzero_targetrowsdistinct))) -> mdr_i_nonzero_targetrowsdistinct = mdr_j_nonzero_targetrowsdistinct))) /\ ((((forall fom_index_mrf_nonzero_targetcolumnsbound. (exists fom_gap_mrf_nonzero_targetcolumnsbound_index_bound. fom_gap_mrf_nonzero_targetcolumnsbound_index_bound + S (fom_index_mrf_nonzero_targetcolumnsbound) = q) -> exists fom_value_mrf_nonzero_targetcolumnsbound. ((((exists fom_beta_height_mrf_nonzero_targetcolumnsbound_entry. fom_beta_height_mrf_nonzero_targetcolumnsbound_entry + S (fom_value_mrf_nonzero_targetcolumnsbound) = S ((S (fom_index_mrf_nonzero_targetcolumnsbound)) * Cc)) /\ exists fom_beta_quotient_mrf_nonzero_targetcolumnsbound_entry. Cb = fom_beta_quotient_mrf_nonzero_targetcolumnsbound_entry * S ((S (fom_index_mrf_nonzero_targetcolumnsbound)) * Cc) + (fom_value_mrf_nonzero_targetcolumnsbound))) /\ (exists fom_gap_mrf_nonzero_targetcolumnsbound_value_bound. fom_gap_mrf_nonzero_targetcolumnsbound_value_bound + S (fom_value_mrf_nonzero_targetcolumnsbound) = w))) /\ (forall mdr_i_nonzero_targetcolumnsdistinct mdr_j_nonzero_targetcolumnsdistinct mdr_a_nonzero_targetcolumnsdistinct. (exists mdr_gap_nonzero_targetcolumnsdistincti. mdr_gap_nonzero_targetcolumnsdistincti + S (mdr_i_nonzero_targetcolumnsdistinct) = (q)) -> (exists mdr_gap_nonzero_targetcolumnsdistinctj. mdr_gap_nonzero_targetcolumnsdistinctj + S (mdr_j_nonzero_targetcolumnsdistinct) = (q)) -> (((exists ff_h_mdr_nonzero_targetcolumnsdistinctfirst. ff_h_mdr_nonzero_targetcolumnsdistinctfirst + S (mdr_a_nonzero_targetcolumnsdistinct) = S ((S (mdr_i_nonzero_targetcolumnsdistinct)) * Cc)) /\ exists ff_q_mdr_nonzero_targetcolumnsdistinctfirst. Cb = ff_q_mdr_nonzero_targetcolumnsdistinctfirst * S ((S (mdr_i_nonzero_targetcolumnsdistinct)) * Cc) + (mdr_a_nonzero_targetcolumnsdistinct))) -> (((exists ff_h_mdr_nonzero_targetcolumnsdistinctsecond. ff_h_mdr_nonzero_targetcolumnsdistinctsecond + S (mdr_a_nonzero_targetcolumnsdistinct) = S ((S (mdr_j_nonzero_targetcolumnsdistinct)) * Cc)) /\ exists ff_q_mdr_nonzero_targetcolumnsdistinctsecond. Cb = ff_q_mdr_nonzero_targetcolumnsdistinctsecond * S ((S (mdr_j_nonzero_targetcolumnsdistinct)) * Cc) + (mdr_a_nonzero_targetcolumnsdistinct))) -> mdr_i_nonzero_targetcolumnsdistinct = mdr_j_nonzero_targetcolumnsdistinct))) /\ (exists mdr_p_nonzero_targetnonzero mdr_n_nonzero_targetnonzero. ((exists mdr_ub_nonzero_targetnonzeroevaluation mdr_uc_nonzero_targetnonzeroevaluation mdr_vb_nonzero_targetnonzeroevaluation mdr_vc_nonzero_targetnonzeroevaluation. ((((forall mdr_i_nonzero_targetnonzeroevaluationmatrixpositive. (exists mdr_gap_nonzero_targetnonzeroevaluationmatrixpositivebound. mdr_gap_nonzero_targetnonzeroevaluationmatrixpositivebound + S (mdr_i_nonzero_targetnonzeroevaluationmatrixpositive) = ((q) * (q))) -> exists mdr_a_nonzero_targetnonzeroevaluationmatrixpositive. (((exists mdr_r_nonzero_targetnonzeroevaluationmatrixpositivepoint mdr_s_nonzero_targetnonzeroevaluationmatrixpositivepoint mdr_u_nonzero_targetnonzeroevaluationmatrixpositivepoint mdr_v_nonzero_targetnonzeroevaluationmatrixpositivepoint. ((mdr_i_nonzero_targetnonzeroevaluationmatrixpositive = (q) * mdr_r_nonzero_targetnonzeroevaluationmatrixpositivepoint + mdr_s_nonzero_targetnonzeroevaluationmatrixpositivepoint) /\ ((exists mdr_gap_nonzero_targetnonzeroevaluationmatrixpositivepointcolumn. mdr_gap_nonzero_targetnonzeroevaluationmatrixpositivepointcolumn + S (mdr_s_nonzero_targetnonzeroevaluationmatrixpositivepoint) = (q)) /\ ((((exists ff_h_mdr_nonzero_targetnonzeroevaluationmatrixpositivepointrow_index. ff_h_mdr_nonzero_targetnonzeroevaluationmatrixpositivepointrow_index + S (mdr_u_nonzero_targetnonzeroevaluationmatrixpositivepoint) = S ((S (mdr_r_nonzero_targetnonzeroevaluationmatrixpositivepoint)) * Rc)) /\ exists ff_q_mdr_nonzero_targetnonzeroevaluationmatrixpositivepointrow_index. Rb = ff_q_mdr_nonzero_targetnonzeroevaluationmatrixpositivepointrow_index * S ((S (mdr_r_nonzero_targetnonzeroevaluationmatrixpositivepoint)) * Rc) + (mdr_u_nonzero_targetnonzeroevaluationmatrixpositivepoint))) /\ ((((exists ff_h_mdr_nonzero_targetnonzeroevaluationmatrixpositivepointcolumn_index. ff_h_mdr_nonzero_targetnonzeroevaluationmatrixpositivepointcolumn_index + S (mdr_v_nonzero_targetnonzeroevaluationmatrixpositivepoint) = S ((S (mdr_s_nonzero_targetnonzeroevaluationmatrixpositivepoint)) * Cc)) /\ exists ff_q_mdr_nonzero_targetnonzeroevaluationmatrixpositivepointcolumn_index. Cb = ff_q_mdr_nonzero_targetnonzeroevaluationmatrixpositivepointcolumn_index * S ((S (mdr_s_nonzero_targetnonzeroevaluationmatrixpositivepoint)) * Cc) + (mdr_v_nonzero_targetnonzeroevaluationmatrixpositivepoint))) /\ (((exists ff_h_mdr_nonzero_targetnonzeroevaluationmatrixpositivepointsource. ff_h_mdr_nonzero_targetnonzeroevaluationmatrixpositivepointsource + S (mdr_a_nonzero_targetnonzeroevaluationmatrixpositive) = S ((S ((mdr_u_nonzero_targetnonzeroevaluationmatrixpositivepoint) * (w) + (mdr_v_nonzero_targetnonzeroevaluationmatrixpositivepoint))) * pc)) /\ exists ff_q_mdr_nonzero_targetnonzeroevaluationmatrixpositivepointsource. pb = ff_q_mdr_nonzero_targetnonzeroevaluationmatrixpositivepointsource * S ((S ((mdr_u_nonzero_targetnonzeroevaluationmatrixpositivepoint) * (w) + (mdr_v_nonzero_targetnonzeroevaluationmatrixpositivepoint))) * pc) + (mdr_a_nonzero_targetnonzeroevaluationmatrixpositive)))))))) /\ (((exists ff_h_mdr_nonzero_targetnonzeroevaluationmatrixpositiveoutput. ff_h_mdr_nonzero_targetnonzeroevaluationmatrixpositiveoutput + S (mdr_a_nonzero_targetnonzeroevaluationmatrixpositive) = S ((S (mdr_i_nonzero_targetnonzeroevaluationmatrixpositive)) * mdr_uc_nonzero_targetnonzeroevaluation)) /\ exists ff_q_mdr_nonzero_targetnonzeroevaluationmatrixpositiveoutput. mdr_ub_nonzero_targetnonzeroevaluation = ff_q_mdr_nonzero_targetnonzeroevaluationmatrixpositiveoutput * S ((S (mdr_i_nonzero_targetnonzeroevaluationmatrixpositive)) * mdr_uc_nonzero_targetnonzeroevaluation) + (mdr_a_nonzero_targetnonzeroevaluationmatrixpositive)))))) /\ (forall mdr_i_nonzero_targetnonzeroevaluationmatrixnegative. (exists mdr_gap_nonzero_targetnonzeroevaluationmatrixnegativebound. mdr_gap_nonzero_targetnonzeroevaluationmatrixnegativebound + S (mdr_i_nonzero_targetnonzeroevaluationmatrixnegative) = ((q) * (q))) -> exists mdr_a_nonzero_targetnonzeroevaluationmatrixnegative. (((exists mdr_r_nonzero_targetnonzeroevaluationmatrixnegativepoint mdr_s_nonzero_targetnonzeroevaluationmatrixnegativepoint mdr_u_nonzero_targetnonzeroevaluationmatrixnegativepoint mdr_v_nonzero_targetnonzeroevaluationmatrixnegativepoint. ((mdr_i_nonzero_targetnonzeroevaluationmatrixnegative = (q) * mdr_r_nonzero_targetnonzeroevaluationmatrixnegativepoint + mdr_s_nonzero_targetnonzeroevaluationmatrixnegativepoint) /\ ((exists mdr_gap_nonzero_targetnonzeroevaluationmatrixnegativepointcolumn. mdr_gap_nonzero_targetnonzeroevaluationmatrixnegativepointcolumn + S (mdr_s_nonzero_targetnonzeroevaluationmatrixnegativepoint) = (q)) /\ ((((exists ff_h_mdr_nonzero_targetnonzeroevaluationmatrixnegativepointrow_index. ff_h_mdr_nonzero_targetnonzeroevaluationmatrixnegativepointrow_index + S (mdr_u_nonzero_targetnonzeroevaluationmatrixnegativepoint) = S ((S (mdr_r_nonzero_targetnonzeroevaluationmatrixnegativepoint)) * Rc)) /\ exists ff_q_mdr_nonzero_targetnonzeroevaluationmatrixnegativepointrow_index. Rb = ff_q_mdr_nonzero_targetnonzeroevaluationmatrixnegativepointrow_index * S ((S (mdr_r_nonzero_targetnonzeroevaluationmatrixnegativepoint)) * Rc) + (mdr_u_nonzero_targetnonzeroevaluationmatrixnegativepoint))) /\ ((((exists ff_h_mdr_nonzero_targetnonzeroevaluationmatrixnegativepointcolumn_index. ff_h_mdr_nonzero_targetnonzeroevaluationmatrixnegativepointcolumn_index + S (mdr_v_nonzero_targetnonzeroevaluationmatrixnegativepoint) = S ((S (mdr_s_nonzero_targetnonzeroevaluationmatrixnegativepoint)) * Cc)) /\ exists ff_q_mdr_nonzero_targetnonzeroevaluationmatrixnegativepointcolumn_index. Cb = ff_q_mdr_nonzero_targetnonzeroevaluationmatrixnegativepointcolumn_index * S ((S (mdr_s_nonzero_targetnonzeroevaluationmatrixnegativepoint)) * Cc) + (mdr_v_nonzero_targetnonzeroevaluationmatrixnegativepoint))) /\ (((exists ff_h_mdr_nonzero_targetnonzeroevaluationmatrixnegativepointsource. ff_h_mdr_nonzero_targetnonzeroevaluationmatrixnegativepointsource + S (mdr_a_nonzero_targetnonzeroevaluationmatrixnegative) = S ((S ((mdr_u_nonzero_targetnonzeroevaluationmatrixnegativepoint) * (w) + (mdr_v_nonzero_targetnonzeroevaluationmatrixnegativepoint))) * nc)) /\ exists ff_q_mdr_nonzero_targetnonzeroevaluationmatrixnegativepointsource. nb = ff_q_mdr_nonzero_targetnonzeroevaluationmatrixnegativepointsource * S ((S ((mdr_u_nonzero_targetnonzeroevaluationmatrixnegativepoint) * (w) + (mdr_v_nonzero_targetnonzeroevaluationmatrixnegativepoint))) * nc) + (mdr_a_nonzero_targetnonzeroevaluationmatrixnegative)))))))) /\ (((exists ff_h_mdr_nonzero_targetnonzeroevaluationmatrixnegativeoutput. ff_h_mdr_nonzero_targetnonzeroevaluationmatrixnegativeoutput + S (mdr_a_nonzero_targetnonzeroevaluationmatrixnegative) = S ((S (mdr_i_nonzero_targetnonzeroevaluationmatrixnegative)) * mdr_vc_nonzero_targetnonzeroevaluation)) /\ exists ff_q_mdr_nonzero_targetnonzeroevaluationmatrixnegativeoutput. mdr_vb_nonzero_targetnonzeroevaluation = ff_q_mdr_nonzero_targetnonzeroevaluationmatrixnegativeoutput * S ((S (mdr_i_nonzero_targetnonzeroevaluationmatrixnegative)) * mdr_vc_nonzero_targetnonzeroevaluation) + (mdr_a_nonzero_targetnonzeroevaluationmatrixnegative)))))))) /\ (exists mdr_b_nonzero_targetnonzeroevaluationdeterminant mdr_c_nonzero_targetnonzeroevaluationdeterminant mdr_l_nonzero_targetnonzeroevaluationdeterminant mdr_i_nonzero_targetnonzeroevaluationdeterminant. ((forall mdr_i_nonzero_targetnonzeroevaluationdeterminanth. (exists mdr_gap_nonzero_targetnonzeroevaluationdeterminanthi. mdr_gap_nonzero_targetnonzeroevaluationdeterminanthi + S (mdr_i_nonzero_targetnonzeroevaluationdeterminanth) = (mdr_l_nonzero_targetnonzeroevaluationdeterminant)) -> exists mdr_d_nonzero_targetnonzeroevaluationdeterminanth mdr_pb_nonzero_targetnonzeroevaluationdeterminanth mdr_pc_nonzero_targetnonzeroevaluationdeterminanth mdr_nb_nonzero_targetnonzeroevaluationdeterminanth mdr_nc_nonzero_targetnonzeroevaluationdeterminanth mdr_p_nonzero_targetnonzeroevaluationdeterminanth mdr_n_nonzero_targetnonzeroevaluationdeterminanth. ((exists mdr_z_nonzero_targetnonzeroevaluationdeterminanthr. ((exists mdr_a_nonzero_targetnonzeroevaluationdeterminanthrc mdr_b_nonzero_targetnonzeroevaluationdeterminanthrc mdr_c_nonzero_targetnonzeroevaluationdeterminanthrc mdr_e_nonzero_targetnonzeroevaluationdeterminanthrc mdr_f_nonzero_targetnonzeroevaluationdeterminanthrc. ((mdr_a_nonzero_targetnonzeroevaluationdeterminanthrc = ((mdr_d_nonzero_targetnonzeroevaluationdeterminanth) + (mdr_pb_nonzero_targetnonzeroevaluationdeterminanth)) * S ((mdr_d_nonzero_targetnonzeroevaluationdeterminanth) + (mdr_pb_nonzero_targetnonzeroevaluationdeterminanth)) + ((mdr_pb_nonzero_targetnonzeroevaluationdeterminanth) + (mdr_pb_nonzero_targetnonzeroevaluationdeterminanth))) /\ ((mdr_b_nonzero_targetnonzeroevaluationdeterminanthrc = ((mdr_pc_nonzero_targetnonzeroevaluationdeterminanth) + (mdr_nb_nonzero_targetnonzeroevaluationdeterminanth)) * S ((mdr_pc_nonzero_targetnonzeroevaluationdeterminanth) + (mdr_nb_nonzero_targetnonzeroevaluationdeterminanth)) + ((mdr_nb_nonzero_targetnonzeroevaluationdeterminanth) + (mdr_nb_nonzero_targetnonzeroevaluationdeterminanth))) /\ ((mdr_c_nonzero_targetnonzeroevaluationdeterminanthrc = ((mdr_a_nonzero_targetnonzeroevaluationdeterminanthrc) + (mdr_b_nonzero_targetnonzeroevaluationdeterminanthrc)) * S ((mdr_a_nonzero_targetnonzeroevaluationdeterminanthrc) + (mdr_b_nonzero_targetnonzeroevaluationdeterminanthrc)) + ((mdr_b_nonzero_targetnonzeroevaluationdeterminanthrc) + (mdr_b_nonzero_targetnonzeroevaluationdeterminanthrc))) /\ ((mdr_e_nonzero_targetnonzeroevaluationdeterminanthrc = ((mdr_p_nonzero_targetnonzeroevaluationdeterminanth) + (mdr_n_nonzero_targetnonzeroevaluationdeterminanth)) * S ((mdr_p_nonzero_targetnonzeroevaluationdeterminanth) + (mdr_n_nonzero_targetnonzeroevaluationdeterminanth)) + ((mdr_n_nonzero_targetnonzeroevaluationdeterminanth) + (mdr_n_nonzero_targetnonzeroevaluationdeterminanth))) /\ ((mdr_f_nonzero_targetnonzeroevaluationdeterminanthrc = ((mdr_nc_nonzero_targetnonzeroevaluationdeterminanth) + (mdr_e_nonzero_targetnonzeroevaluationdeterminanthrc)) * S ((mdr_nc_nonzero_targetnonzeroevaluationdeterminanth) + (mdr_e_nonzero_targetnonzeroevaluationdeterminanthrc)) + ((mdr_e_nonzero_targetnonzeroevaluationdeterminanthrc) + (mdr_e_nonzero_targetnonzeroevaluationdeterminanthrc))) /\ ((mdr_z_nonzero_targetnonzeroevaluationdeterminanthr) = ((mdr_c_nonzero_targetnonzeroevaluationdeterminanthrc) + (mdr_f_nonzero_targetnonzeroevaluationdeterminanthrc)) * S ((mdr_c_nonzero_targetnonzeroevaluationdeterminanthrc) + (mdr_f_nonzero_targetnonzeroevaluationdeterminanthrc)) + ((mdr_f_nonzero_targetnonzeroevaluationdeterminanthrc) + (mdr_f_nonzero_targetnonzeroevaluationdeterminanthrc))))))))) /\ (((exists ff_h_mdr_nonzero_targetnonzeroevaluationdeterminanthrb. ff_h_mdr_nonzero_targetnonzeroevaluationdeterminanthrb + S (mdr_z_nonzero_targetnonzeroevaluationdeterminanthr) = S ((S (mdr_i_nonzero_targetnonzeroevaluationdeterminanth)) * mdr_c_nonzero_targetnonzeroevaluationdeterminant)) /\ exists ff_q_mdr_nonzero_targetnonzeroevaluationdeterminanthrb. mdr_b_nonzero_targetnonzeroevaluationdeterminant = ff_q_mdr_nonzero_targetnonzeroevaluationdeterminanthrb * S ((S (mdr_i_nonzero_targetnonzeroevaluationdeterminanth)) * mdr_c_nonzero_targetnonzeroevaluationdeterminant) + (mdr_z_nonzero_targetnonzeroevaluationdeterminanthr))))) /\ (((((mdr_d_nonzero_targetnonzeroevaluationdeterminanth) = 0) /\ (((mdr_p_nonzero_targetnonzeroevaluationdeterminanth) = 1) /\ ((mdr_n_nonzero_targetnonzeroevaluationdeterminanth) = 0))) \/ exists mdr_q_nonzero_targetnonzeroevaluationdeterminanths mdr_eb_nonzero_targetnonzeroevaluationdeterminanths mdr_ec_nonzero_targetnonzeroevaluationdeterminanths mdr_fb_nonzero_targetnonzeroevaluationdeterminanths mdr_fc_nonzero_targetnonzeroevaluationdeterminanths. (((mdr_d_nonzero_targetnonzeroevaluationdeterminanth) = S (mdr_q_nonzero_targetnonzeroevaluationdeterminanths)) /\ ((forall mdr_j_nonzero_targetnonzeroevaluationdeterminanthsc. (exists mdr_gap_nonzero_targetnonzeroevaluationdeterminanthscj. mdr_gap_nonzero_targetnonzeroevaluationdeterminanthscj + S (mdr_j_nonzero_targetnonzeroevaluationdeterminanthsc) = (S (mdr_q_nonzero_targetnonzeroevaluationdeterminanths))) -> exists mdr_i_nonzero_targetnonzeroevaluationdeterminanthsc mdr_up_nonzero_targetnonzeroevaluationdeterminanthsc mdr_us_nonzero_targetnonzeroevaluationdeterminanthsc mdr_un_nonzero_targetnonzeroevaluationdeterminanthsc mdr_ut_nonzero_targetnonzeroevaluationdeterminanthsc mdr_p_nonzero_targetnonzeroevaluationdeterminanthsc mdr_n_nonzero_targetnonzeroevaluationdeterminanthsc. ((exists mdr_gap_nonzero_targetnonzeroevaluationdeterminanthsci. mdr_gap_nonzero_targetnonzeroevaluationdeterminanthsci + S (mdr_i_nonzero_targetnonzeroevaluationdeterminanthsc) = (mdr_i_nonzero_targetnonzeroevaluationdeterminanth)) /\ ((exists mdr_z_nonzero_targetnonzeroevaluationdeterminanthscr. ((exists mdr_a_nonzero_targetnonzeroevaluationdeterminanthscrc mdr_b_nonzero_targetnonzeroevaluationdeterminanthscrc mdr_c_nonzero_targetnonzeroevaluationdeterminanthscrc mdr_e_nonzero_targetnonzeroevaluationdeterminanthscrc mdr_f_nonzero_targetnonzeroevaluationdeterminanthscrc. ((mdr_a_nonzero_targetnonzeroevaluationdeterminanthscrc = ((mdr_q_nonzero_targetnonzeroevaluationdeterminanths) + (mdr_up_nonzero_targetnonzeroevaluationdeterminanthsc)) * S ((mdr_q_nonzero_targetnonzeroevaluationdeterminanths) + (mdr_up_nonzero_targetnonzeroevaluationdeterminanthsc)) + ((mdr_up_nonzero_targetnonzeroevaluationdeterminanthsc) + (mdr_up_nonzero_targetnonzeroevaluationdeterminanthsc))) /\ ((mdr_b_nonzero_targetnonzeroevaluationdeterminanthscrc = ((mdr_us_nonzero_targetnonzeroevaluationdeterminanthsc) + (mdr_un_nonzero_targetnonzeroevaluationdeterminanthsc)) * S ((mdr_us_nonzero_targetnonzeroevaluationdeterminanthsc) + (mdr_un_nonzero_targetnonzeroevaluationdeterminanthsc)) + ((mdr_un_nonzero_targetnonzeroevaluationdeterminanthsc) + (mdr_un_nonzero_targetnonzeroevaluationdeterminanthsc))) /\ ((mdr_c_nonzero_targetnonzeroevaluationdeterminanthscrc = ((mdr_a_nonzero_targetnonzeroevaluationdeterminanthscrc) + (mdr_b_nonzero_targetnonzeroevaluationdeterminanthscrc)) * S ((mdr_a_nonzero_targetnonzeroevaluationdeterminanthscrc) + (mdr_b_nonzero_targetnonzeroevaluationdeterminanthscrc)) + ((mdr_b_nonzero_targetnonzeroevaluationdeterminanthscrc) + (mdr_b_nonzero_targetnonzeroevaluationdeterminanthscrc))) /\ ((mdr_e_nonzero_targetnonzeroevaluationdeterminanthscrc = ((mdr_p_nonzero_targetnonzeroevaluationdeterminanthsc) + (mdr_n_nonzero_targetnonzeroevaluationdeterminanthsc)) * S ((mdr_p_nonzero_targetnonzeroevaluationdeterminanthsc) + (mdr_n_nonzero_targetnonzeroevaluationdeterminanthsc)) + ((mdr_n_nonzero_targetnonzeroevaluationdeterminanthsc) + (mdr_n_nonzero_targetnonzeroevaluationdeterminanthsc))) /\ ((mdr_f_nonzero_targetnonzeroevaluationdeterminanthscrc = ((mdr_ut_nonzero_targetnonzeroevaluationdeterminanthsc) + (mdr_e_nonzero_targetnonzeroevaluationdeterminanthscrc)) * S ((mdr_ut_nonzero_targetnonzeroevaluationdeterminanthsc) + (mdr_e_nonzero_targetnonzeroevaluationdeterminanthscrc)) + ((mdr_e_nonzero_targetnonzeroevaluationdeterminanthscrc) + (mdr_e_nonzero_targetnonzeroevaluationdeterminanthscrc))) /\ ((mdr_z_nonzero_targetnonzeroevaluationdeterminanthscr) = ((mdr_c_nonzero_targetnonzeroevaluationdeterminanthscrc) + (mdr_f_nonzero_targetnonzeroevaluationdeterminanthscrc)) * S ((mdr_c_nonzero_targetnonzeroevaluationdeterminanthscrc) + (mdr_f_nonzero_targetnonzeroevaluationdeterminanthscrc)) + ((mdr_f_nonzero_targetnonzeroevaluationdeterminanthscrc) + (mdr_f_nonzero_targetnonzeroevaluationdeterminanthscrc))))))))) /\ (((exists ff_h_mdr_nonzero_targetnonzeroevaluationdeterminanthscrb. ff_h_mdr_nonzero_targetnonzeroevaluationdeterminanthscrb + S (mdr_z_nonzero_targetnonzeroevaluationdeterminanthscr) = S ((S (mdr_i_nonzero_targetnonzeroevaluationdeterminanthsc)) * mdr_c_nonzero_targetnonzeroevaluationdeterminant)) /\ exists ff_q_mdr_nonzero_targetnonzeroevaluationdeterminanthscrb. mdr_b_nonzero_targetnonzeroevaluationdeterminant = ff_q_mdr_nonzero_targetnonzeroevaluationdeterminanthscrb * S ((S (mdr_i_nonzero_targetnonzeroevaluationdeterminanthsc)) * mdr_c_nonzero_targetnonzeroevaluationdeterminant) + (mdr_z_nonzero_targetnonzeroevaluationdeterminanthscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_nonzero_targetnonzeroevaluationdeterminanthscm_positive. (exists ff_gap_mdm_lt_mdr_nonzero_targetnonzeroevaluationdeterminanthscm_positive_index_bound. ff_gap_mdm_lt_mdr_nonzero_targetnonzeroevaluationdeterminanthscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_nonzero_targetnonzeroevaluationdeterminanthscm_positive) = ((mdr_q_nonzero_targetnonzeroevaluationdeterminanths) * (mdr_q_nonzero_targetnonzeroevaluationdeterminanths))) -> exists ff_row_mdm_prefix_mdr_nonzero_targetnonzeroevaluationdeterminanthscm_positive ff_column_mdm_prefix_mdr_nonzero_targetnonzeroevaluationdeterminanthscm_positive ff_value_mdm_prefix_mdr_nonzero_targetnonzeroevaluationdeterminanthscm_positive. (ff_index_mdm_prefix_mdr_nonzero_targetnonzeroevaluationdeterminanthscm_positive = (mdr_q_nonzero_targetnonzeroevaluationdeterminanths) * ff_row_mdm_prefix_mdr_nonzero_targetnonzeroevaluationdeterminanthscm_positive + ff_column_mdm_prefix_mdr_nonzero_targetnonzeroevaluationdeterminanthscm_positive /\ ((exists ff_gap_mdm_lt_mdr_nonzero_targetnonzeroevaluationdeterminanthscm_positive_column_bound. ff_gap_mdm_lt_mdr_nonzero_targetnonzeroevaluationdeterminanthscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_nonzero_targetnonzeroevaluationdeterminanthscm_positive) = (mdr_q_nonzero_targetnonzeroevaluationdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_nonzero_targetnonzeroevaluationdeterminanthscm_positive_cell ff_column_mdm_cell_mdr_nonzero_targetnonzeroevaluationdeterminanthscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_nonzero_targetnonzeroevaluationdeterminanthscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_nonzero_targetnonzeroevaluationdeterminanthscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_nonzero_targetnonzeroevaluationdeterminanthscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_nonzero_targetnonzeroevaluationdeterminanthscm_positive_cell = ff_row_mdm_prefix_mdr_nonzero_targetnonzeroevaluationdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_nonzero_targetnonzeroevaluationdeterminanthscm_positive_cell_row_after. ff_gap_mdm_le_mdr_nonzero_targetnonzeroevaluationdeterminanthscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_nonzero_targetnonzeroevaluationdeterminanthscm_positive)) /\ ff_row_mdm_cell_mdr_nonzero_targetnonzeroevaluationdeterminanthscm_positive_cell = S ff_row_mdm_prefix_mdr_nonzero_targetnonzeroevaluationdeterminanthscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_nonzero_targetnonzeroevaluationdeterminanthscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_nonzero_targetnonzeroevaluationdeterminanthscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_nonzero_targetnonzeroevaluationdeterminanthscm_positive) = (mdr_j_nonzero_targetnonzeroevaluationdeterminanthsc)) /\ ff_column_mdm_cell_mdr_nonzero_targetnonzeroevaluationdeterminanthscm_positive_cell = ff_column_mdm_prefix_mdr_nonzero_targetnonzeroevaluationdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_nonzero_targetnonzeroevaluationdeterminanthscm_positive_cell_column_after. ff_gap_mdm_le_mdr_nonzero_targetnonzeroevaluationdeterminanthscm_positive_cell_column_after + (mdr_j_nonzero_targetnonzeroevaluationdeterminanthsc) = (ff_column_mdm_prefix_mdr_nonzero_targetnonzeroevaluationdeterminanthscm_positive)) /\ ff_column_mdm_cell_mdr_nonzero_targetnonzeroevaluationdeterminanthscm_positive_cell = S ff_column_mdm_prefix_mdr_nonzero_targetnonzeroevaluationdeterminanthscm_positive))) /\ (((exists ff_h_mdm_mdr_nonzero_targetnonzeroevaluationdeterminanthscm_positive_cell_source. ff_h_mdm_mdr_nonzero_targetnonzeroevaluationdeterminanthscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_nonzero_targetnonzeroevaluationdeterminanthscm_positive) = S ((S ((ff_row_mdm_cell_mdr_nonzero_targetnonzeroevaluationdeterminanthscm_positive_cell) * (S (mdr_q_nonzero_targetnonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_nonzero_targetnonzeroevaluationdeterminanthscm_positive_cell))) * mdr_pc_nonzero_targetnonzeroevaluationdeterminanth)) /\ exists ff_q_mdm_mdr_nonzero_targetnonzeroevaluationdeterminanthscm_positive_cell_source. mdr_pb_nonzero_targetnonzeroevaluationdeterminanth = ff_q_mdm_mdr_nonzero_targetnonzeroevaluationdeterminanthscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_nonzero_targetnonzeroevaluationdeterminanthscm_positive_cell) * (S (mdr_q_nonzero_targetnonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_nonzero_targetnonzeroevaluationdeterminanthscm_positive_cell))) * mdr_pc_nonzero_targetnonzeroevaluationdeterminanth) + (ff_value_mdm_prefix_mdr_nonzero_targetnonzeroevaluationdeterminanthscm_positive)))))) /\ (((exists ff_h_mdm_mdr_nonzero_targetnonzeroevaluationdeterminanthscm_positive_target. ff_h_mdm_mdr_nonzero_targetnonzeroevaluationdeterminanthscm_positive_target + S (ff_value_mdm_prefix_mdr_nonzero_targetnonzeroevaluationdeterminanthscm_positive) = S ((S (ff_index_mdm_prefix_mdr_nonzero_targetnonzeroevaluationdeterminanthscm_positive)) * mdr_us_nonzero_targetnonzeroevaluationdeterminanthsc)) /\ exists ff_q_mdm_mdr_nonzero_targetnonzeroevaluationdeterminanthscm_positive_target. mdr_up_nonzero_targetnonzeroevaluationdeterminanthsc = ff_q_mdm_mdr_nonzero_targetnonzeroevaluationdeterminanthscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_nonzero_targetnonzeroevaluationdeterminanthscm_positive)) * mdr_us_nonzero_targetnonzeroevaluationdeterminanthsc) + (ff_value_mdm_prefix_mdr_nonzero_targetnonzeroevaluationdeterminanthscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_nonzero_targetnonzeroevaluationdeterminanthscm_negative. (exists ff_gap_mdm_lt_mdr_nonzero_targetnonzeroevaluationdeterminanthscm_negative_index_bound. ff_gap_mdm_lt_mdr_nonzero_targetnonzeroevaluationdeterminanthscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_nonzero_targetnonzeroevaluationdeterminanthscm_negative) = ((mdr_q_nonzero_targetnonzeroevaluationdeterminanths) * (mdr_q_nonzero_targetnonzeroevaluationdeterminanths))) -> exists ff_row_mdm_prefix_mdr_nonzero_targetnonzeroevaluationdeterminanthscm_negative ff_column_mdm_prefix_mdr_nonzero_targetnonzeroevaluationdeterminanthscm_negative ff_value_mdm_prefix_mdr_nonzero_targetnonzeroevaluationdeterminanthscm_negative. (ff_index_mdm_prefix_mdr_nonzero_targetnonzeroevaluationdeterminanthscm_negative = (mdr_q_nonzero_targetnonzeroevaluationdeterminanths) * ff_row_mdm_prefix_mdr_nonzero_targetnonzeroevaluationdeterminanthscm_negative + ff_column_mdm_prefix_mdr_nonzero_targetnonzeroevaluationdeterminanthscm_negative /\ ((exists ff_gap_mdm_lt_mdr_nonzero_targetnonzeroevaluationdeterminanthscm_negative_column_bound. ff_gap_mdm_lt_mdr_nonzero_targetnonzeroevaluationdeterminanthscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_nonzero_targetnonzeroevaluationdeterminanthscm_negative) = (mdr_q_nonzero_targetnonzeroevaluationdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_nonzero_targetnonzeroevaluationdeterminanthscm_negative_cell ff_column_mdm_cell_mdr_nonzero_targetnonzeroevaluationdeterminanthscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_nonzero_targetnonzeroevaluationdeterminanthscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_nonzero_targetnonzeroevaluationdeterminanthscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_nonzero_targetnonzeroevaluationdeterminanthscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_nonzero_targetnonzeroevaluationdeterminanthscm_negative_cell = ff_row_mdm_prefix_mdr_nonzero_targetnonzeroevaluationdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_nonzero_targetnonzeroevaluationdeterminanthscm_negative_cell_row_after. ff_gap_mdm_le_mdr_nonzero_targetnonzeroevaluationdeterminanthscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_nonzero_targetnonzeroevaluationdeterminanthscm_negative)) /\ ff_row_mdm_cell_mdr_nonzero_targetnonzeroevaluationdeterminanthscm_negative_cell = S ff_row_mdm_prefix_mdr_nonzero_targetnonzeroevaluationdeterminanthscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_nonzero_targetnonzeroevaluationdeterminanthscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_nonzero_targetnonzeroevaluationdeterminanthscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_nonzero_targetnonzeroevaluationdeterminanthscm_negative) = (mdr_j_nonzero_targetnonzeroevaluationdeterminanthsc)) /\ ff_column_mdm_cell_mdr_nonzero_targetnonzeroevaluationdeterminanthscm_negative_cell = ff_column_mdm_prefix_mdr_nonzero_targetnonzeroevaluationdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_nonzero_targetnonzeroevaluationdeterminanthscm_negative_cell_column_after. ff_gap_mdm_le_mdr_nonzero_targetnonzeroevaluationdeterminanthscm_negative_cell_column_after + (mdr_j_nonzero_targetnonzeroevaluationdeterminanthsc) = (ff_column_mdm_prefix_mdr_nonzero_targetnonzeroevaluationdeterminanthscm_negative)) /\ ff_column_mdm_cell_mdr_nonzero_targetnonzeroevaluationdeterminanthscm_negative_cell = S ff_column_mdm_prefix_mdr_nonzero_targetnonzeroevaluationdeterminanthscm_negative))) /\ (((exists ff_h_mdm_mdr_nonzero_targetnonzeroevaluationdeterminanthscm_negative_cell_source. ff_h_mdm_mdr_nonzero_targetnonzeroevaluationdeterminanthscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_nonzero_targetnonzeroevaluationdeterminanthscm_negative) = S ((S ((ff_row_mdm_cell_mdr_nonzero_targetnonzeroevaluationdeterminanthscm_negative_cell) * (S (mdr_q_nonzero_targetnonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_nonzero_targetnonzeroevaluationdeterminanthscm_negative_cell))) * mdr_nc_nonzero_targetnonzeroevaluationdeterminanth)) /\ exists ff_q_mdm_mdr_nonzero_targetnonzeroevaluationdeterminanthscm_negative_cell_source. mdr_nb_nonzero_targetnonzeroevaluationdeterminanth = ff_q_mdm_mdr_nonzero_targetnonzeroevaluationdeterminanthscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_nonzero_targetnonzeroevaluationdeterminanthscm_negative_cell) * (S (mdr_q_nonzero_targetnonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_nonzero_targetnonzeroevaluationdeterminanthscm_negative_cell))) * mdr_nc_nonzero_targetnonzeroevaluationdeterminanth) + (ff_value_mdm_prefix_mdr_nonzero_targetnonzeroevaluationdeterminanthscm_negative)))))) /\ (((exists ff_h_mdm_mdr_nonzero_targetnonzeroevaluationdeterminanthscm_negative_target. ff_h_mdm_mdr_nonzero_targetnonzeroevaluationdeterminanthscm_negative_target + S (ff_value_mdm_prefix_mdr_nonzero_targetnonzeroevaluationdeterminanthscm_negative) = S ((S (ff_index_mdm_prefix_mdr_nonzero_targetnonzeroevaluationdeterminanthscm_negative)) * mdr_ut_nonzero_targetnonzeroevaluationdeterminanthsc)) /\ exists ff_q_mdm_mdr_nonzero_targetnonzeroevaluationdeterminanthscm_negative_target. mdr_un_nonzero_targetnonzeroevaluationdeterminanthsc = ff_q_mdm_mdr_nonzero_targetnonzeroevaluationdeterminanthscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_nonzero_targetnonzeroevaluationdeterminanthscm_negative)) * mdr_ut_nonzero_targetnonzeroevaluationdeterminanthsc) + (ff_value_mdm_prefix_mdr_nonzero_targetnonzeroevaluationdeterminanthscm_negative))))))))) /\ ((((exists ff_h_mdr_nonzero_targetnonzeroevaluationdeterminanthscp. ff_h_mdr_nonzero_targetnonzeroevaluationdeterminanthscp + S (mdr_p_nonzero_targetnonzeroevaluationdeterminanthsc) = S ((S (mdr_j_nonzero_targetnonzeroevaluationdeterminanthsc)) * mdr_ec_nonzero_targetnonzeroevaluationdeterminanths)) /\ exists ff_q_mdr_nonzero_targetnonzeroevaluationdeterminanthscp. mdr_eb_nonzero_targetnonzeroevaluationdeterminanths = ff_q_mdr_nonzero_targetnonzeroevaluationdeterminanthscp * S ((S (mdr_j_nonzero_targetnonzeroevaluationdeterminanthsc)) * mdr_ec_nonzero_targetnonzeroevaluationdeterminanths) + (mdr_p_nonzero_targetnonzeroevaluationdeterminanthsc))) /\ (((exists ff_h_mdr_nonzero_targetnonzeroevaluationdeterminanthscn. ff_h_mdr_nonzero_targetnonzeroevaluationdeterminanthscn + S (mdr_n_nonzero_targetnonzeroevaluationdeterminanthsc) = S ((S (mdr_j_nonzero_targetnonzeroevaluationdeterminanthsc)) * mdr_fc_nonzero_targetnonzeroevaluationdeterminanths)) /\ exists ff_q_mdr_nonzero_targetnonzeroevaluationdeterminanthscn. mdr_fb_nonzero_targetnonzeroevaluationdeterminanths = ff_q_mdr_nonzero_targetnonzeroevaluationdeterminanthscn * S ((S (mdr_j_nonzero_targetnonzeroevaluationdeterminanthsc)) * mdr_fc_nonzero_targetnonzeroevaluationdeterminanths) + (mdr_n_nonzero_targetnonzeroevaluationdeterminanthsc)))))))) /\ (exists ff_ub_mce_fold_mdr_nonzero_targetnonzeroevaluationdeterminanthsf ff_uc_mce_fold_mdr_nonzero_targetnonzeroevaluationdeterminanthsf ff_vb_mce_fold_mdr_nonzero_targetnonzeroevaluationdeterminanthsf ff_vc_mce_fold_mdr_nonzero_targetnonzeroevaluationdeterminanthsf. ((forall ff_index_mce_alternating_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_prefix. (exists ff_gap_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_prefix_index. ff_gap_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_prefix_index + S (ff_index_mce_alternating_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_prefix) = (S (mdr_q_nonzero_targetnonzeroevaluationdeterminanths))) -> exists ff_ap_mce_alternating_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_prefix ff_an_mce_alternating_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_prefix ff_bp_mce_alternating_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_prefix ff_bn_mce_alternating_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_prefix ff_p_mce_alternating_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_prefix ff_n_mce_alternating_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_prefix. ((((exists ff_h_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_prefix_ap. ff_h_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_prefix_ap + S (ff_ap_mce_alternating_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_prefix)) * mdr_pc_nonzero_targetnonzeroevaluationdeterminanth)) /\ exists ff_q_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_prefix_ap. mdr_pb_nonzero_targetnonzeroevaluationdeterminanth = ff_q_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_prefix)) * mdr_pc_nonzero_targetnonzeroevaluationdeterminanth) + (ff_ap_mce_alternating_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_prefix_an. ff_h_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_prefix_an + S (ff_an_mce_alternating_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_prefix)) * mdr_nc_nonzero_targetnonzeroevaluationdeterminanth)) /\ exists ff_q_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_prefix_an. mdr_nb_nonzero_targetnonzeroevaluationdeterminanth = ff_q_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_prefix)) * mdr_nc_nonzero_targetnonzeroevaluationdeterminanth) + (ff_an_mce_alternating_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_prefix_bp. ff_h_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_prefix_bp + S (ff_bp_mce_alternating_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_prefix)) * mdr_ec_nonzero_targetnonzeroevaluationdeterminanths)) /\ exists ff_q_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_prefix_bp. mdr_eb_nonzero_targetnonzeroevaluationdeterminanths = ff_q_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_prefix)) * mdr_ec_nonzero_targetnonzeroevaluationdeterminanths) + (ff_bp_mce_alternating_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_prefix_bn. ff_h_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_prefix_bn + S (ff_bn_mce_alternating_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_prefix)) * mdr_fc_nonzero_targetnonzeroevaluationdeterminanths)) /\ exists ff_q_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_prefix_bn. mdr_fb_nonzero_targetnonzeroevaluationdeterminanths = ff_q_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_prefix)) * mdr_fc_nonzero_targetnonzeroevaluationdeterminanths) + (ff_bn_mce_alternating_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_prefix_positive. ff_h_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_prefix_positive + S (ff_p_mce_alternating_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_nonzero_targetnonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_prefix_positive. ff_ub_mce_fold_mdr_nonzero_targetnonzeroevaluationdeterminanthsf = ff_q_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_nonzero_targetnonzeroevaluationdeterminanthsf) + (ff_p_mce_alternating_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_prefix_negative. ff_h_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_prefix_negative + S (ff_n_mce_alternating_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_nonzero_targetnonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_prefix_negative. ff_vb_mce_fold_mdr_nonzero_targetnonzeroevaluationdeterminanthsf = ff_q_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_nonzero_targetnonzeroevaluationdeterminanthsf) + (ff_n_mce_alternating_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_prefix))) /\ (((exists ff_even_mce_term_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_prefix = 2 * ff_even_mce_term_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_prefix_term) /\ (ff_p_mce_alternating_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_prefix = 2 * ff_odd_mce_term_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_positive ff_v_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_positive. ((((exists ff_h_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_positive_start. ff_h_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_positive_start. ff_u_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_positive_start * S ((S (0)) * ff_v_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_positive_terminal. ff_h_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_positive_terminal + S (mdr_p_nonzero_targetnonzeroevaluationdeterminanth) = S ((S ((S (mdr_q_nonzero_targetnonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_positive_terminal. ff_u_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_positive_terminal * S ((S ((S (mdr_q_nonzero_targetnonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_positive) + (mdr_p_nonzero_targetnonzeroevaluationdeterminanth))) /\ forall ff_i_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_positive. (exists ff_lt_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_positive_bound. ff_lt_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_positive_bound + S ff_i_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_positive = (S (mdr_q_nonzero_targetnonzeroevaluationdeterminanths))) -> exists ff_a_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_positive ff_r_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_positive ff_s_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_positive. ((((exists ff_h_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_positive_summand. ff_h_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_positive_summand + S (ff_a_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_nonzero_targetnonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_positive_summand. ff_ub_mce_fold_mdr_nonzero_targetnonzeroevaluationdeterminanthsf = ff_q_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_positive_summand * S ((S (ff_i_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_nonzero_targetnonzeroevaluationdeterminanthsf) + (ff_a_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_positive_partial. ff_h_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_positive_partial + S (ff_r_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_positive_partial. ff_u_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_positive_partial * S ((S (ff_i_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_positive) + (ff_r_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_positive_successor. ff_h_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_positive_successor + S (ff_s_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_positive) = S ((S (S ff_i_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_positive_successor. ff_u_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_positive_successor * S ((S (S ff_i_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_positive) + (ff_s_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_positive))) /\ ff_s_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_positive = ff_r_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_positive + ff_a_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_positive)))))) /\ (exists ff_u_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_negative ff_v_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_negative. ((((exists ff_h_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_negative_start. ff_h_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_negative_start. ff_u_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_negative_start * S ((S (0)) * ff_v_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_negative_terminal. ff_h_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_negative_terminal + S (mdr_n_nonzero_targetnonzeroevaluationdeterminanth) = S ((S ((S (mdr_q_nonzero_targetnonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_negative_terminal. ff_u_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_negative_terminal * S ((S ((S (mdr_q_nonzero_targetnonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_negative) + (mdr_n_nonzero_targetnonzeroevaluationdeterminanth))) /\ forall ff_i_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_negative. (exists ff_lt_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_negative_bound. ff_lt_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_negative_bound + S ff_i_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_negative = (S (mdr_q_nonzero_targetnonzeroevaluationdeterminanths))) -> exists ff_a_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_negative ff_r_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_negative ff_s_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_negative. ((((exists ff_h_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_negative_summand. ff_h_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_negative_summand + S (ff_a_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_nonzero_targetnonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_negative_summand. ff_vb_mce_fold_mdr_nonzero_targetnonzeroevaluationdeterminanthsf = ff_q_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_negative_summand * S ((S (ff_i_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_nonzero_targetnonzeroevaluationdeterminanthsf) + (ff_a_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_negative_partial. ff_h_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_negative_partial + S (ff_r_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_negative_partial. ff_u_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_negative_partial * S ((S (ff_i_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_negative) + (ff_r_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_negative_successor. ff_h_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_negative_successor + S (ff_s_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_negative) = S ((S (S ff_i_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_negative_successor. ff_u_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_negative_successor * S ((S (S ff_i_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_negative) + (ff_s_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_negative))) /\ ff_s_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_negative = ff_r_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_negative + ff_a_mce_mdr_nonzero_targetnonzeroevaluationdeterminanthsf_negative))))))))))))))) /\ ((exists mdr_gap_nonzero_targetnonzeroevaluationdeterminanti. mdr_gap_nonzero_targetnonzeroevaluationdeterminanti + S (mdr_i_nonzero_targetnonzeroevaluationdeterminant) = (mdr_l_nonzero_targetnonzeroevaluationdeterminant)) /\ (exists mdr_z_nonzero_targetnonzeroevaluationdeterminantr. ((exists mdr_a_nonzero_targetnonzeroevaluationdeterminantrc mdr_b_nonzero_targetnonzeroevaluationdeterminantrc mdr_c_nonzero_targetnonzeroevaluationdeterminantrc mdr_e_nonzero_targetnonzeroevaluationdeterminantrc mdr_f_nonzero_targetnonzeroevaluationdeterminantrc. ((mdr_a_nonzero_targetnonzeroevaluationdeterminantrc = ((q) + (mdr_ub_nonzero_targetnonzeroevaluation)) * S ((q) + (mdr_ub_nonzero_targetnonzeroevaluation)) + ((mdr_ub_nonzero_targetnonzeroevaluation) + (mdr_ub_nonzero_targetnonzeroevaluation))) /\ ((mdr_b_nonzero_targetnonzeroevaluationdeterminantrc = ((mdr_uc_nonzero_targetnonzeroevaluation) + (mdr_vb_nonzero_targetnonzeroevaluation)) * S ((mdr_uc_nonzero_targetnonzeroevaluation) + (mdr_vb_nonzero_targetnonzeroevaluation)) + ((mdr_vb_nonzero_targetnonzeroevaluation) + (mdr_vb_nonzero_targetnonzeroevaluation))) /\ ((mdr_c_nonzero_targetnonzeroevaluationdeterminantrc = ((mdr_a_nonzero_targetnonzeroevaluationdeterminantrc) + (mdr_b_nonzero_targetnonzeroevaluationdeterminantrc)) * S ((mdr_a_nonzero_targetnonzeroevaluationdeterminantrc) + (mdr_b_nonzero_targetnonzeroevaluationdeterminantrc)) + ((mdr_b_nonzero_targetnonzeroevaluationdeterminantrc) + (mdr_b_nonzero_targetnonzeroevaluationdeterminantrc))) /\ ((mdr_e_nonzero_targetnonzeroevaluationdeterminantrc = ((mdr_p_nonzero_targetnonzero) + (mdr_n_nonzero_targetnonzero)) * S ((mdr_p_nonzero_targetnonzero) + (mdr_n_nonzero_targetnonzero)) + ((mdr_n_nonzero_targetnonzero) + (mdr_n_nonzero_targetnonzero))) /\ ((mdr_f_nonzero_targetnonzeroevaluationdeterminantrc = ((mdr_vc_nonzero_targetnonzeroevaluation) + (mdr_e_nonzero_targetnonzeroevaluationdeterminantrc)) * S ((mdr_vc_nonzero_targetnonzeroevaluation) + (mdr_e_nonzero_targetnonzeroevaluationdeterminantrc)) + ((mdr_e_nonzero_targetnonzeroevaluationdeterminantrc) + (mdr_e_nonzero_targetnonzeroevaluationdeterminantrc))) /\ ((mdr_z_nonzero_targetnonzeroevaluationdeterminantr) = ((mdr_c_nonzero_targetnonzeroevaluationdeterminantrc) + (mdr_f_nonzero_targetnonzeroevaluationdeterminantrc)) * S ((mdr_c_nonzero_targetnonzeroevaluationdeterminantrc) + (mdr_f_nonzero_targetnonzeroevaluationdeterminantrc)) + ((mdr_f_nonzero_targetnonzeroevaluationdeterminantrc) + (mdr_f_nonzero_targetnonzeroevaluationdeterminantrc))))))))) /\ (((exists ff_h_mdr_nonzero_targetnonzeroevaluationdeterminantrb. ff_h_mdr_nonzero_targetnonzeroevaluationdeterminantrb + S (mdr_z_nonzero_targetnonzeroevaluationdeterminantr) = S ((S (mdr_i_nonzero_targetnonzeroevaluationdeterminant)) * mdr_c_nonzero_targetnonzeroevaluationdeterminant)) /\ exists ff_q_mdr_nonzero_targetnonzeroevaluationdeterminantrb. mdr_b_nonzero_targetnonzeroevaluationdeterminant = ff_q_mdr_nonzero_targetnonzeroevaluationdeterminantrb * S ((S (mdr_i_nonzero_targetnonzeroevaluationdeterminant)) * mdr_c_nonzero_targetnonzeroevaluationdeterminant) + (mdr_z_nonzero_targetnonzeroevaluationdeterminantr)))))))))) /\ (~(mdr_p_nonzero_targetnonzero = mdr_n_nonzero_targetnonzero)))))))Complete tactic proof in conservative notation
All 67 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
67 script commands · 12 reading checkpoints · 0 local claims
This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.
Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.
Named ingredients (2)
01Fix variables and assumptionsL1–10
02Fix variables and assumptionsL11–18
03Separate the logical casesL19–21
04Use earlier factsL22–30
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L22
specialize matrix_rank_selector_transport (rb) - L23
specialize matrix_rank_selector_transport (rc) - L24
specialize matrix_rank_selector_transport (Rb) - L25
specialize matrix_rank_selector_transport (Rc) - L26
specialize matrix_rank_selector_transport (q) - L27
specialize matrix_rank_selector_transport (r) - L28
apply matrix_rank_selector_transport - L29
exact hrows - L30
exact hminor_left
05Separate the logical casesL31–31
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L31
split
06Use earlier factsL32–40
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L32
specialize matrix_rank_selector_transport (cb) - L33
specialize matrix_rank_selector_transport (cc) - L34
specialize matrix_rank_selector_transport (Cb) - L35
specialize matrix_rank_selector_transport (Cc) - L36
specialize matrix_rank_selector_transport (q) - L37
specialize matrix_rank_selector_transport (w) - L38
apply matrix_rank_selector_transport - L39
exact hcolumns - L40
exact hminor_right_left
07Separate the logical casesL41–43
08Construct an explicit witnessL44–45
09Separate the logical casesL46–46
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L46
split
10Use earlier factsL47–56
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L47
specialize matrix_rank_selected_determinant_selector_transport (pb) - L48
specialize matrix_rank_selected_determinant_selector_transport (pc) - L49
specialize matrix_rank_selected_determinant_selector_transport (nb) - L50
specialize matrix_rank_selected_determinant_selector_transport (nc) - L51
specialize matrix_rank_selected_determinant_selector_transport (w) - L52
specialize matrix_rank_selected_determinant_selector_transport (rb) - L53
specialize matrix_rank_selected_determinant_selector_transport (rc) - L54
specialize matrix_rank_selected_determinant_selector_transport (cb) - L55
specialize matrix_rank_selected_determinant_selector_transport (cc) - L56
specialize matrix_rank_selected_determinant_selector_transport (q)
11Use earlier factsL57–66
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L57
specialize matrix_rank_selected_determinant_selector_transport (Rb) - L58
specialize matrix_rank_selected_determinant_selector_transport (Rc) - L59
specialize matrix_rank_selected_determinant_selector_transport (Cb) - L60
specialize matrix_rank_selected_determinant_selector_transport (Cc) - L61
specialize matrix_rank_selected_determinant_selector_transport (x) - L62
specialize matrix_rank_selected_determinant_selector_transport (x1) - L63
apply matrix_rank_selected_determinant_selector_transport - L64
exact hrows - L65
exact hcolumns - L66
exact hminor_right_right_witness_witness_left
12Use earlier factsL67–67
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L67
exact hminor_right_right_witness_witness_right
Original defined command ledger · 67 lines
- 0001
intro pb - 0002
intro pc - 0003
intro nb - 0004
intro nc - 0005
intro r - 0006
intro w - 0007
intro q - 0008
intro rb - 0009
intro rc - 0010
intro cb - 0011
intro cc - 0012
intro Rb - 0013
intro Rc - 0014
intro Cb - 0015
intro Cc - 0016
intro hrows - 0017
intro hcolumns - 0018
intro hminor - 0019
cases hminor - 0020
cases hminor_right - 0021
split - 0022
specialize matrix_rank_selector_transport (rb) - 0023
specialize matrix_rank_selector_transport (rc) - 0024
specialize matrix_rank_selector_transport (Rb) - 0025
specialize matrix_rank_selector_transport (Rc) - 0026
specialize matrix_rank_selector_transport (q) - 0027
specialize matrix_rank_selector_transport (r) - 0028
apply matrix_rank_selector_transport - 0029
exact hrows - 0030
exact hminor_left - 0031
split - 0032
specialize matrix_rank_selector_transport (cb) - 0033
specialize matrix_rank_selector_transport (cc) - 0034
specialize matrix_rank_selector_transport (Cb) - 0035
specialize matrix_rank_selector_transport (Cc) - 0036
specialize matrix_rank_selector_transport (q) - 0037
specialize matrix_rank_selector_transport (w) - 0038
apply matrix_rank_selector_transport - 0039
exact hcolumns - 0040
exact hminor_right_left - 0041
cases hminor_right_right - 0042
cases hminor_right_right_witness - 0043
cases hminor_right_right_witness_witness - 0044
exists x - 0045
exists x1 - 0046
split - 0047
specialize matrix_rank_selected_determinant_selector_transport (pb) - 0048
specialize matrix_rank_selected_determinant_selector_transport (pc) - 0049
specialize matrix_rank_selected_determinant_selector_transport (nb) - 0050
specialize matrix_rank_selected_determinant_selector_transport (nc) - 0051
specialize matrix_rank_selected_determinant_selector_transport (w) - 0052
specialize matrix_rank_selected_determinant_selector_transport (rb) - 0053
specialize matrix_rank_selected_determinant_selector_transport (rc) - 0054
specialize matrix_rank_selected_determinant_selector_transport (cb) - 0055
specialize matrix_rank_selected_determinant_selector_transport (cc) - 0056
specialize matrix_rank_selected_determinant_selector_transport (q) - 0057
specialize matrix_rank_selected_determinant_selector_transport (Rb) - 0058
specialize matrix_rank_selected_determinant_selector_transport (Rc) - 0059
specialize matrix_rank_selected_determinant_selector_transport (Cb) - 0060
specialize matrix_rank_selected_determinant_selector_transport (Cc) - 0061
specialize matrix_rank_selected_determinant_selector_transport (x) - 0062
specialize matrix_rank_selected_determinant_selector_transport (x1) - 0063
apply matrix_rank_selected_determinant_selector_transport - 0064
exact hrows - 0065
exact hcolumns - 0066
exact hminor_right_right_witness_witness_left - 0067
exact hminor_right_right_witness_witness_right