matrix_rank_maximal_nonzero_prefix_exists

forall pb pc nb nc r w K. exists rank. (((exists mdr_gap_maximal_prefixbound. mdr_gap_maximal_prefixbound + (rank) = (K)) /\ ((exists mdr_rb_maximal_prefixwitness mdr_rc_maximal_prefixwitness mdr_cb_maximal_prefixwitness mdr_cc_maximal_prefixwitness. (((((forall fom_index_mrf_maximal_prefixwitnessminorrowsbound. (exists fom_gap_mrf_maximal_prefixwitnessminorrowsbound_index_bound. fom_gap_mrf_maximal_prefixwitnessminorrowsbound_index_bound + S (fom_index_mrf_maximal_prefixwitnessminorrowsbound) = rank) -> exists fom_value_mrf_maximal_prefixwitnessminorrowsbound. ((((exists fom_beta_height_mrf_maximal_prefixwitnessminorrowsbound_entry. fom_beta_height_mrf_maximal_prefixwitnessminorrowsbound_entry + S (fom_value_mrf_maximal_prefixwitnessminorrowsbound) = S ((S (fom_index_mrf_maximal_prefixwitnessminorrowsbound)) * mdr_rc_maximal_prefixwitness)) /\ exists fom_beta_quotient_mrf_maximal_prefixwitnessminorrowsbound_entry. mdr_rb_maximal_prefixwitness = fom_beta_quotient_mrf_maximal_prefixwitnessminorrowsbound_entry * S ((S (fom_index_mrf_maximal_prefixwitnessminorrowsbound)) * mdr_rc_maximal_prefixwitness) + (fom_value_mrf_maximal_prefixwitnessminorrowsbound))) /\ (exists fom_gap_mrf_maximal_prefixwitnessminorrowsbound_value_bound. fom_gap_mrf_maximal_prefixwitnessminorrowsbound_value_bound + S (fom_value_mrf_maximal_prefixwitnessminorrowsbound) = r))) /\ (forall mdr_i_maximal_prefixwitnessminorrowsdistinct mdr_j_maximal_prefixwitnessminorrowsdistinct mdr_a_maximal_prefixwitnessminorrowsdistinct. (exists mdr_gap_maximal_prefixwitnessminorrowsdistincti. mdr_gap_maximal_prefixwitnessminorrowsdistincti + S (mdr_i_maximal_prefixwitnessminorrowsdistinct) = (rank)) -> (exists mdr_gap_maximal_prefixwitnessminorrowsdistinctj. mdr_gap_maximal_prefixwitnessminorrowsdistinctj + S (mdr_j_maximal_prefixwitnessminorrowsdistinct) = (rank)) -> (((exists ff_h_mdr_maximal_prefixwitnessminorrowsdistinctfirst. ff_h_mdr_maximal_prefixwitnessminorrowsdistinctfirst + S (mdr_a_maximal_prefixwitnessminorrowsdistinct) = S ((S (mdr_i_maximal_prefixwitnessminorrowsdistinct)) * mdr_rc_maximal_prefixwitness)) /\ exists ff_q_mdr_maximal_prefixwitnessminorrowsdistinctfirst. mdr_rb_maximal_prefixwitness = ff_q_mdr_maximal_prefixwitnessminorrowsdistinctfirst * S ((S (mdr_i_maximal_prefixwitnessminorrowsdistinct)) * mdr_rc_maximal_prefixwitness) + (mdr_a_maximal_prefixwitnessminorrowsdistinct))) -> (((exists ff_h_mdr_maximal_prefixwitnessminorrowsdistinctsecond. ff_h_mdr_maximal_prefixwitnessminorrowsdistinctsecond + S (mdr_a_maximal_prefixwitnessminorrowsdistinct) = S ((S (mdr_j_maximal_prefixwitnessminorrowsdistinct)) * mdr_rc_maximal_prefixwitness)) /\ exists ff_q_mdr_maximal_prefixwitnessminorrowsdistinctsecond. mdr_rb_maximal_prefixwitness = ff_q_mdr_maximal_prefixwitnessminorrowsdistinctsecond * S ((S (mdr_j_maximal_prefixwitnessminorrowsdistinct)) * mdr_rc_maximal_prefixwitness) + (mdr_a_maximal_prefixwitnessminorrowsdistinct))) -> mdr_i_maximal_prefixwitnessminorrowsdistinct = mdr_j_maximal_prefixwitnessminorrowsdistinct))) /\ ((((forall fom_index_mrf_maximal_prefixwitnessminorcolumnsbound. (exists fom_gap_mrf_maximal_prefixwitnessminorcolumnsbound_index_bound. fom_gap_mrf_maximal_prefixwitnessminorcolumnsbound_index_bound + S (fom_index_mrf_maximal_prefixwitnessminorcolumnsbound) = rank) -> exists fom_value_mrf_maximal_prefixwitnessminorcolumnsbound. ((((exists fom_beta_height_mrf_maximal_prefixwitnessminorcolumnsbound_entry. fom_beta_height_mrf_maximal_prefixwitnessminorcolumnsbound_entry + S (fom_value_mrf_maximal_prefixwitnessminorcolumnsbound) = S ((S (fom_index_mrf_maximal_prefixwitnessminorcolumnsbound)) * mdr_cc_maximal_prefixwitness)) /\ exists fom_beta_quotient_mrf_maximal_prefixwitnessminorcolumnsbound_entry. mdr_cb_maximal_prefixwitness = fom_beta_quotient_mrf_maximal_prefixwitnessminorcolumnsbound_entry * S ((S (fom_index_mrf_maximal_prefixwitnessminorcolumnsbound)) * mdr_cc_maximal_prefixwitness) + (fom_value_mrf_maximal_prefixwitnessminorcolumnsbound))) /\ (exists fom_gap_mrf_maximal_prefixwitnessminorcolumnsbound_value_bound. fom_gap_mrf_maximal_prefixwitnessminorcolumnsbound_value_bound + S (fom_value_mrf_maximal_prefixwitnessminorcolumnsbound) = w))) /\ (forall mdr_i_maximal_prefixwitnessminorcolumnsdistinct mdr_j_maximal_prefixwitnessminorcolumnsdistinct mdr_a_maximal_prefixwitnessminorcolumnsdistinct. (exists mdr_gap_maximal_prefixwitnessminorcolumnsdistincti. mdr_gap_maximal_prefixwitnessminorcolumnsdistincti + S (mdr_i_maximal_prefixwitnessminorcolumnsdistinct) = (rank)) -> (exists mdr_gap_maximal_prefixwitnessminorcolumnsdistinctj. mdr_gap_maximal_prefixwitnessminorcolumnsdistinctj + S (mdr_j_maximal_prefixwitnessminorcolumnsdistinct) = (rank)) -> (((exists ff_h_mdr_maximal_prefixwitnessminorcolumnsdistinctfirst. ff_h_mdr_maximal_prefixwitnessminorcolumnsdistinctfirst + S (mdr_a_maximal_prefixwitnessminorcolumnsdistinct) = S ((S (mdr_i_maximal_prefixwitnessminorcolumnsdistinct)) * mdr_cc_maximal_prefixwitness)) /\ exists ff_q_mdr_maximal_prefixwitnessminorcolumnsdistinctfirst. mdr_cb_maximal_prefixwitness = ff_q_mdr_maximal_prefixwitnessminorcolumnsdistinctfirst * S ((S (mdr_i_maximal_prefixwitnessminorcolumnsdistinct)) * mdr_cc_maximal_prefixwitness) + (mdr_a_maximal_prefixwitnessminorcolumnsdistinct))) -> (((exists ff_h_mdr_maximal_prefixwitnessminorcolumnsdistinctsecond. ff_h_mdr_maximal_prefixwitnessminorcolumnsdistinctsecond + S (mdr_a_maximal_prefixwitnessminorcolumnsdistinct) = S ((S (mdr_j_maximal_prefixwitnessminorcolumnsdistinct)) * mdr_cc_maximal_prefixwitness)) /\ exists ff_q_mdr_maximal_prefixwitnessminorcolumnsdistinctsecond. mdr_cb_maximal_prefixwitness = ff_q_mdr_maximal_prefixwitnessminorcolumnsdistinctsecond * S ((S (mdr_j_maximal_prefixwitnessminorcolumnsdistinct)) * mdr_cc_maximal_prefixwitness) + (mdr_a_maximal_prefixwitnessminorcolumnsdistinct))) -> mdr_i_maximal_prefixwitnessminorcolumnsdistinct = mdr_j_maximal_prefixwitnessminorcolumnsdistinct))) /\ (exists mdr_p_maximal_prefixwitnessminornonzero mdr_n_maximal_prefixwitnessminornonzero. ((exists mdr_ub_maximal_prefixwitnessminornonzeroevaluation mdr_uc_maximal_prefixwitnessminornonzeroevaluation mdr_vb_maximal_prefixwitnessminornonzeroevaluation mdr_vc_maximal_prefixwitnessminornonzeroevaluation. ((((forall mdr_i_maximal_prefixwitnessminornonzeroevaluationmatrixpositive. (exists mdr_gap_maximal_prefixwitnessminornonzeroevaluationmatrixpositivebound. mdr_gap_maximal_prefixwitnessminornonzeroevaluationmatrixpositivebound + S (mdr_i_maximal_prefixwitnessminornonzeroevaluationmatrixpositive) = ((rank) * (rank))) -> exists mdr_a_maximal_prefixwitnessminornonzeroevaluationmatrixpositive. (((exists mdr_r_maximal_prefixwitnessminornonzeroevaluationmatrixpositivepoint mdr_s_maximal_prefixwitnessminornonzeroevaluationmatrixpositivepoint mdr_u_maximal_prefixwitnessminornonzeroevaluationmatrixpositivepoint mdr_v_maximal_prefixwitnessminornonzeroevaluationmatrixpositivepoint. ((mdr_i_maximal_prefixwitnessminornonzeroevaluationmatrixpositive = (rank) * mdr_r_maximal_prefixwitnessminornonzeroevaluationmatrixpositivepoint + mdr_s_maximal_prefixwitnessminornonzeroevaluationmatrixpositivepoint) /\ ((exists mdr_gap_maximal_prefixwitnessminornonzeroevaluationmatrixpositivepointcolumn. mdr_gap_maximal_prefixwitnessminornonzeroevaluationmatrixpositivepointcolumn + S (mdr_s_maximal_prefixwitnessminornonzeroevaluationmatrixpositivepoint) = (rank)) /\ ((((exists ff_h_mdr_maximal_prefixwitnessminornonzeroevaluationmatrixpositivepointrow_index. ff_h_mdr_maximal_prefixwitnessminornonzeroevaluationmatrixpositivepointrow_index + S (mdr_u_maximal_prefixwitnessminornonzeroevaluationmatrixpositivepoint) = S ((S (mdr_r_maximal_prefixwitnessminornonzeroevaluationmatrixpositivepoint)) * mdr_rc_maximal_prefixwitness)) /\ exists ff_q_mdr_maximal_prefixwitnessminornonzeroevaluationmatrixpositivepointrow_index. mdr_rb_maximal_prefixwitness = ff_q_mdr_maximal_prefixwitnessminornonzeroevaluationmatrixpositivepointrow_index * S ((S (mdr_r_maximal_prefixwitnessminornonzeroevaluationmatrixpositivepoint)) * mdr_rc_maximal_prefixwitness) + (mdr_u_maximal_prefixwitnessminornonzeroevaluationmatrixpositivepoint))) /\ ((((exists ff_h_mdr_maximal_prefixwitnessminornonzeroevaluationmatrixpositivepointcolumn_index. ff_h_mdr_maximal_prefixwitnessminornonzeroevaluationmatrixpositivepointcolumn_index + S (mdr_v_maximal_prefixwitnessminornonzeroevaluationmatrixpositivepoint) = S ((S (mdr_s_maximal_prefixwitnessminornonzeroevaluationmatrixpositivepoint)) * mdr_cc_maximal_prefixwitness)) /\ exists ff_q_mdr_maximal_prefixwitnessminornonzeroevaluationmatrixpositivepointcolumn_index. mdr_cb_maximal_prefixwitness = ff_q_mdr_maximal_prefixwitnessminornonzeroevaluationmatrixpositivepointcolumn_index * S ((S (mdr_s_maximal_prefixwitnessminornonzeroevaluationmatrixpositivepoint)) * mdr_cc_maximal_prefixwitness) + (mdr_v_maximal_prefixwitnessminornonzeroevaluationmatrixpositivepoint))) /\ (((exists ff_h_mdr_maximal_prefixwitnessminornonzeroevaluationmatrixpositivepointsource. ff_h_mdr_maximal_prefixwitnessminornonzeroevaluationmatrixpositivepointsource + S (mdr_a_maximal_prefixwitnessminornonzeroevaluationmatrixpositive) = S ((S ((mdr_u_maximal_prefixwitnessminornonzeroevaluationmatrixpositivepoint) * (w) + (mdr_v_maximal_prefixwitnessminornonzeroevaluationmatrixpositivepoint))) * pc)) /\ exists ff_q_mdr_maximal_prefixwitnessminornonzeroevaluationmatrixpositivepointsource. pb = ff_q_mdr_maximal_prefixwitnessminornonzeroevaluationmatrixpositivepointsource * S ((S ((mdr_u_maximal_prefixwitnessminornonzeroevaluationmatrixpositivepoint) * (w) + (mdr_v_maximal_prefixwitnessminornonzeroevaluationmatrixpositivepoint))) * pc) + (mdr_a_maximal_prefixwitnessminornonzeroevaluationmatrixpositive)))))))) /\ (((exists ff_h_mdr_maximal_prefixwitnessminornonzeroevaluationmatrixpositiveoutput. ff_h_mdr_maximal_prefixwitnessminornonzeroevaluationmatrixpositiveoutput + S (mdr_a_maximal_prefixwitnessminornonzeroevaluationmatrixpositive) = S ((S (mdr_i_maximal_prefixwitnessminornonzeroevaluationmatrixpositive)) * mdr_uc_maximal_prefixwitnessminornonzeroevaluation)) /\ exists ff_q_mdr_maximal_prefixwitnessminornonzeroevaluationmatrixpositiveoutput. mdr_ub_maximal_prefixwitnessminornonzeroevaluation = ff_q_mdr_maximal_prefixwitnessminornonzeroevaluationmatrixpositiveoutput * S ((S (mdr_i_maximal_prefixwitnessminornonzeroevaluationmatrixpositive)) * mdr_uc_maximal_prefixwitnessminornonzeroevaluation) + (mdr_a_maximal_prefixwitnessminornonzeroevaluationmatrixpositive)))))) /\ (forall mdr_i_maximal_prefixwitnessminornonzeroevaluationmatrixnegative. (exists mdr_gap_maximal_prefixwitnessminornonzeroevaluationmatrixnegativebound. mdr_gap_maximal_prefixwitnessminornonzeroevaluationmatrixnegativebound + S (mdr_i_maximal_prefixwitnessminornonzeroevaluationmatrixnegative) = ((rank) * (rank))) -> exists mdr_a_maximal_prefixwitnessminornonzeroevaluationmatrixnegative. (((exists mdr_r_maximal_prefixwitnessminornonzeroevaluationmatrixnegativepoint mdr_s_maximal_prefixwitnessminornonzeroevaluationmatrixnegativepoint mdr_u_maximal_prefixwitnessminornonzeroevaluationmatrixnegativepoint mdr_v_maximal_prefixwitnessminornonzeroevaluationmatrixnegativepoint. ((mdr_i_maximal_prefixwitnessminornonzeroevaluationmatrixnegative = (rank) * mdr_r_maximal_prefixwitnessminornonzeroevaluationmatrixnegativepoint + mdr_s_maximal_prefixwitnessminornonzeroevaluationmatrixnegativepoint) /\ ((exists mdr_gap_maximal_prefixwitnessminornonzeroevaluationmatrixnegativepointcolumn. mdr_gap_maximal_prefixwitnessminornonzeroevaluationmatrixnegativepointcolumn + S (mdr_s_maximal_prefixwitnessminornonzeroevaluationmatrixnegativepoint) = (rank)) /\ ((((exists ff_h_mdr_maximal_prefixwitnessminornonzeroevaluationmatrixnegativepointrow_index. ff_h_mdr_maximal_prefixwitnessminornonzeroevaluationmatrixnegativepointrow_index + S (mdr_u_maximal_prefixwitnessminornonzeroevaluationmatrixnegativepoint) = S ((S (mdr_r_maximal_prefixwitnessminornonzeroevaluationmatrixnegativepoint)) * mdr_rc_maximal_prefixwitness)) /\ exists ff_q_mdr_maximal_prefixwitnessminornonzeroevaluationmatrixnegativepointrow_index. mdr_rb_maximal_prefixwitness = ff_q_mdr_maximal_prefixwitnessminornonzeroevaluationmatrixnegativepointrow_index * S ((S (mdr_r_maximal_prefixwitnessminornonzeroevaluationmatrixnegativepoint)) * mdr_rc_maximal_prefixwitness) + (mdr_u_maximal_prefixwitnessminornonzeroevaluationmatrixnegativepoint))) /\ ((((exists ff_h_mdr_maximal_prefixwitnessminornonzeroevaluationmatrixnegativepointcolumn_index. ff_h_mdr_maximal_prefixwitnessminornonzeroevaluationmatrixnegativepointcolumn_index + S (mdr_v_maximal_prefixwitnessminornonzeroevaluationmatrixnegativepoint) = S ((S (mdr_s_maximal_prefixwitnessminornonzeroevaluationmatrixnegativepoint)) * mdr_cc_maximal_prefixwitness)) /\ exists ff_q_mdr_maximal_prefixwitnessminornonzeroevaluationmatrixnegativepointcolumn_index. mdr_cb_maximal_prefixwitness = ff_q_mdr_maximal_prefixwitnessminornonzeroevaluationmatrixnegativepointcolumn_index * S ((S (mdr_s_maximal_prefixwitnessminornonzeroevaluationmatrixnegativepoint)) * mdr_cc_maximal_prefixwitness) + (mdr_v_maximal_prefixwitnessminornonzeroevaluationmatrixnegativepoint))) /\ (((exists ff_h_mdr_maximal_prefixwitnessminornonzeroevaluationmatrixnegativepointsource. ff_h_mdr_maximal_prefixwitnessminornonzeroevaluationmatrixnegativepointsource + S (mdr_a_maximal_prefixwitnessminornonzeroevaluationmatrixnegative) = S ((S ((mdr_u_maximal_prefixwitnessminornonzeroevaluationmatrixnegativepoint) * (w) + (mdr_v_maximal_prefixwitnessminornonzeroevaluationmatrixnegativepoint))) * nc)) /\ exists ff_q_mdr_maximal_prefixwitnessminornonzeroevaluationmatrixnegativepointsource. nb = ff_q_mdr_maximal_prefixwitnessminornonzeroevaluationmatrixnegativepointsource * S ((S ((mdr_u_maximal_prefixwitnessminornonzeroevaluationmatrixnegativepoint) * (w) + (mdr_v_maximal_prefixwitnessminornonzeroevaluationmatrixnegativepoint))) * nc) + (mdr_a_maximal_prefixwitnessminornonzeroevaluationmatrixnegative)))))))) /\ (((exists ff_h_mdr_maximal_prefixwitnessminornonzeroevaluationmatrixnegativeoutput. ff_h_mdr_maximal_prefixwitnessminornonzeroevaluationmatrixnegativeoutput + S (mdr_a_maximal_prefixwitnessminornonzeroevaluationmatrixnegative) = S ((S (mdr_i_maximal_prefixwitnessminornonzeroevaluationmatrixnegative)) * mdr_vc_maximal_prefixwitnessminornonzeroevaluation)) /\ exists ff_q_mdr_maximal_prefixwitnessminornonzeroevaluationmatrixnegativeoutput. mdr_vb_maximal_prefixwitnessminornonzeroevaluation = ff_q_mdr_maximal_prefixwitnessminornonzeroevaluationmatrixnegativeoutput * S ((S (mdr_i_maximal_prefixwitnessminornonzeroevaluationmatrixnegative)) * mdr_vc_maximal_prefixwitnessminornonzeroevaluation) + (mdr_a_maximal_prefixwitnessminornonzeroevaluationmatrixnegative)))))))) /\ (exists mdr_b_maximal_prefixwitnessminornonzeroevaluationdeterminant mdr_c_maximal_prefixwitnessminornonzeroevaluationdeterminant mdr_l_maximal_prefixwitnessminornonzeroevaluationdeterminant mdr_i_maximal_prefixwitnessminornonzeroevaluationdeterminant. ((forall mdr_i_maximal_prefixwitnessminornonzeroevaluationdeterminanth. (exists mdr_gap_maximal_prefixwitnessminornonzeroevaluationdeterminanthi. mdr_gap_maximal_prefixwitnessminornonzeroevaluationdeterminanthi + S (mdr_i_maximal_prefixwitnessminornonzeroevaluationdeterminanth) = (mdr_l_maximal_prefixwitnessminornonzeroevaluationdeterminant)) -> exists mdr_d_maximal_prefixwitnessminornonzeroevaluationdeterminanth mdr_pb_maximal_prefixwitnessminornonzeroevaluationdeterminanth mdr_pc_maximal_prefixwitnessminornonzeroevaluationdeterminanth mdr_nb_maximal_prefixwitnessminornonzeroevaluationdeterminanth mdr_nc_maximal_prefixwitnessminornonzeroevaluationdeterminanth mdr_p_maximal_prefixwitnessminornonzeroevaluationdeterminanth mdr_n_maximal_prefixwitnessminornonzeroevaluationdeterminanth. ((exists mdr_z_maximal_prefixwitnessminornonzeroevaluationdeterminanthr. ((exists mdr_a_maximal_prefixwitnessminornonzeroevaluationdeterminanthrc mdr_b_maximal_prefixwitnessminornonzeroevaluationdeterminanthrc mdr_c_maximal_prefixwitnessminornonzeroevaluationdeterminanthrc mdr_e_maximal_prefixwitnessminornonzeroevaluationdeterminanthrc mdr_f_maximal_prefixwitnessminornonzeroevaluationdeterminanthrc. ((mdr_a_maximal_prefixwitnessminornonzeroevaluationdeterminanthrc = ((mdr_d_maximal_prefixwitnessminornonzeroevaluationdeterminanth) + (mdr_pb_maximal_prefixwitnessminornonzeroevaluationdeterminanth)) * S ((mdr_d_maximal_prefixwitnessminornonzeroevaluationdeterminanth) + (mdr_pb_maximal_prefixwitnessminornonzeroevaluationdeterminanth)) + ((mdr_pb_maximal_prefixwitnessminornonzeroevaluationdeterminanth) + (mdr_pb_maximal_prefixwitnessminornonzeroevaluationdeterminanth))) /\ ((mdr_b_maximal_prefixwitnessminornonzeroevaluationdeterminanthrc = ((mdr_pc_maximal_prefixwitnessminornonzeroevaluationdeterminanth) + (mdr_nb_maximal_prefixwitnessminornonzeroevaluationdeterminanth)) * S ((mdr_pc_maximal_prefixwitnessminornonzeroevaluationdeterminanth) + (mdr_nb_maximal_prefixwitnessminornonzeroevaluationdeterminanth)) + ((mdr_nb_maximal_prefixwitnessminornonzeroevaluationdeterminanth) + (mdr_nb_maximal_prefixwitnessminornonzeroevaluationdeterminanth))) /\ ((mdr_c_maximal_prefixwitnessminornonzeroevaluationdeterminanthrc = ((mdr_a_maximal_prefixwitnessminornonzeroevaluationdeterminanthrc) + (mdr_b_maximal_prefixwitnessminornonzeroevaluationdeterminanthrc)) * S ((mdr_a_maximal_prefixwitnessminornonzeroevaluationdeterminanthrc) + (mdr_b_maximal_prefixwitnessminornonzeroevaluationdeterminanthrc)) + ((mdr_b_maximal_prefixwitnessminornonzeroevaluationdeterminanthrc) + (mdr_b_maximal_prefixwitnessminornonzeroevaluationdeterminanthrc))) /\ ((mdr_e_maximal_prefixwitnessminornonzeroevaluationdeterminanthrc = ((mdr_p_maximal_prefixwitnessminornonzeroevaluationdeterminanth) + (mdr_n_maximal_prefixwitnessminornonzeroevaluationdeterminanth)) * S ((mdr_p_maximal_prefixwitnessminornonzeroevaluationdeterminanth) + (mdr_n_maximal_prefixwitnessminornonzeroevaluationdeterminanth)) + ((mdr_n_maximal_prefixwitnessminornonzeroevaluationdeterminanth) + (mdr_n_maximal_prefixwitnessminornonzeroevaluationdeterminanth))) /\ ((mdr_f_maximal_prefixwitnessminornonzeroevaluationdeterminanthrc = ((mdr_nc_maximal_prefixwitnessminornonzeroevaluationdeterminanth) + (mdr_e_maximal_prefixwitnessminornonzeroevaluationdeterminanthrc)) * S ((mdr_nc_maximal_prefixwitnessminornonzeroevaluationdeterminanth) + (mdr_e_maximal_prefixwitnessminornonzeroevaluationdeterminanthrc)) + ((mdr_e_maximal_prefixwitnessminornonzeroevaluationdeterminanthrc) + (mdr_e_maximal_prefixwitnessminornonzeroevaluationdeterminanthrc))) /\ ((mdr_z_maximal_prefixwitnessminornonzeroevaluationdeterminanthr) = ((mdr_c_maximal_prefixwitnessminornonzeroevaluationdeterminanthrc) + (mdr_f_maximal_prefixwitnessminornonzeroevaluationdeterminanthrc)) * S ((mdr_c_maximal_prefixwitnessminornonzeroevaluationdeterminanthrc) + (mdr_f_maximal_prefixwitnessminornonzeroevaluationdeterminanthrc)) + ((mdr_f_maximal_prefixwitnessminornonzeroevaluationdeterminanthrc) + (mdr_f_maximal_prefixwitnessminornonzeroevaluationdeterminanthrc))))))))) /\ (((exists ff_h_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthrb. ff_h_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthrb + S (mdr_z_maximal_prefixwitnessminornonzeroevaluationdeterminanthr) = S ((S (mdr_i_maximal_prefixwitnessminornonzeroevaluationdeterminanth)) * mdr_c_maximal_prefixwitnessminornonzeroevaluationdeterminant)) /\ exists ff_q_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthrb. mdr_b_maximal_prefixwitnessminornonzeroevaluationdeterminant = ff_q_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthrb * S ((S (mdr_i_maximal_prefixwitnessminornonzeroevaluationdeterminanth)) * mdr_c_maximal_prefixwitnessminornonzeroevaluationdeterminant) + (mdr_z_maximal_prefixwitnessminornonzeroevaluationdeterminanthr))))) /\ (((((mdr_d_maximal_prefixwitnessminornonzeroevaluationdeterminanth) = 0) /\ (((mdr_p_maximal_prefixwitnessminornonzeroevaluationdeterminanth) = 1) /\ ((mdr_n_maximal_prefixwitnessminornonzeroevaluationdeterminanth) = 0))) \/ exists mdr_q_maximal_prefixwitnessminornonzeroevaluationdeterminanths mdr_eb_maximal_prefixwitnessminornonzeroevaluationdeterminanths mdr_ec_maximal_prefixwitnessminornonzeroevaluationdeterminanths mdr_fb_maximal_prefixwitnessminornonzeroevaluationdeterminanths mdr_fc_maximal_prefixwitnessminornonzeroevaluationdeterminanths. (((mdr_d_maximal_prefixwitnessminornonzeroevaluationdeterminanth) = S (mdr_q_maximal_prefixwitnessminornonzeroevaluationdeterminanths)) /\ ((forall mdr_j_maximal_prefixwitnessminornonzeroevaluationdeterminanthsc. (exists mdr_gap_maximal_prefixwitnessminornonzeroevaluationdeterminanthscj. mdr_gap_maximal_prefixwitnessminornonzeroevaluationdeterminanthscj + S (mdr_j_maximal_prefixwitnessminornonzeroevaluationdeterminanthsc) = (S (mdr_q_maximal_prefixwitnessminornonzeroevaluationdeterminanths))) -> exists mdr_i_maximal_prefixwitnessminornonzeroevaluationdeterminanthsc mdr_up_maximal_prefixwitnessminornonzeroevaluationdeterminanthsc mdr_us_maximal_prefixwitnessminornonzeroevaluationdeterminanthsc mdr_un_maximal_prefixwitnessminornonzeroevaluationdeterminanthsc mdr_ut_maximal_prefixwitnessminornonzeroevaluationdeterminanthsc mdr_p_maximal_prefixwitnessminornonzeroevaluationdeterminanthsc mdr_n_maximal_prefixwitnessminornonzeroevaluationdeterminanthsc. ((exists mdr_gap_maximal_prefixwitnessminornonzeroevaluationdeterminanthsci. mdr_gap_maximal_prefixwitnessminornonzeroevaluationdeterminanthsci + S (mdr_i_maximal_prefixwitnessminornonzeroevaluationdeterminanthsc) = (mdr_i_maximal_prefixwitnessminornonzeroevaluationdeterminanth)) /\ ((exists mdr_z_maximal_prefixwitnessminornonzeroevaluationdeterminanthscr. ((exists mdr_a_maximal_prefixwitnessminornonzeroevaluationdeterminanthscrc mdr_b_maximal_prefixwitnessminornonzeroevaluationdeterminanthscrc mdr_c_maximal_prefixwitnessminornonzeroevaluationdeterminanthscrc mdr_e_maximal_prefixwitnessminornonzeroevaluationdeterminanthscrc mdr_f_maximal_prefixwitnessminornonzeroevaluationdeterminanthscrc. ((mdr_a_maximal_prefixwitnessminornonzeroevaluationdeterminanthscrc = ((mdr_q_maximal_prefixwitnessminornonzeroevaluationdeterminanths) + (mdr_up_maximal_prefixwitnessminornonzeroevaluationdeterminanthsc)) * S ((mdr_q_maximal_prefixwitnessminornonzeroevaluationdeterminanths) + (mdr_up_maximal_prefixwitnessminornonzeroevaluationdeterminanthsc)) + ((mdr_up_maximal_prefixwitnessminornonzeroevaluationdeterminanthsc) + (mdr_up_maximal_prefixwitnessminornonzeroevaluationdeterminanthsc))) /\ ((mdr_b_maximal_prefixwitnessminornonzeroevaluationdeterminanthscrc = ((mdr_us_maximal_prefixwitnessminornonzeroevaluationdeterminanthsc) + (mdr_un_maximal_prefixwitnessminornonzeroevaluationdeterminanthsc)) * S ((mdr_us_maximal_prefixwitnessminornonzeroevaluationdeterminanthsc) + (mdr_un_maximal_prefixwitnessminornonzeroevaluationdeterminanthsc)) + ((mdr_un_maximal_prefixwitnessminornonzeroevaluationdeterminanthsc) + (mdr_un_maximal_prefixwitnessminornonzeroevaluationdeterminanthsc))) /\ ((mdr_c_maximal_prefixwitnessminornonzeroevaluationdeterminanthscrc = ((mdr_a_maximal_prefixwitnessminornonzeroevaluationdeterminanthscrc) + (mdr_b_maximal_prefixwitnessminornonzeroevaluationdeterminanthscrc)) * S ((mdr_a_maximal_prefixwitnessminornonzeroevaluationdeterminanthscrc) + (mdr_b_maximal_prefixwitnessminornonzeroevaluationdeterminanthscrc)) + ((mdr_b_maximal_prefixwitnessminornonzeroevaluationdeterminanthscrc) + (mdr_b_maximal_prefixwitnessminornonzeroevaluationdeterminanthscrc))) /\ ((mdr_e_maximal_prefixwitnessminornonzeroevaluationdeterminanthscrc = ((mdr_p_maximal_prefixwitnessminornonzeroevaluationdeterminanthsc) + (mdr_n_maximal_prefixwitnessminornonzeroevaluationdeterminanthsc)) * S ((mdr_p_maximal_prefixwitnessminornonzeroevaluationdeterminanthsc) + (mdr_n_maximal_prefixwitnessminornonzeroevaluationdeterminanthsc)) + ((mdr_n_maximal_prefixwitnessminornonzeroevaluationdeterminanthsc) + (mdr_n_maximal_prefixwitnessminornonzeroevaluationdeterminanthsc))) /\ ((mdr_f_maximal_prefixwitnessminornonzeroevaluationdeterminanthscrc = ((mdr_ut_maximal_prefixwitnessminornonzeroevaluationdeterminanthsc) + (mdr_e_maximal_prefixwitnessminornonzeroevaluationdeterminanthscrc)) * S ((mdr_ut_maximal_prefixwitnessminornonzeroevaluationdeterminanthsc) + (mdr_e_maximal_prefixwitnessminornonzeroevaluationdeterminanthscrc)) + ((mdr_e_maximal_prefixwitnessminornonzeroevaluationdeterminanthscrc) + (mdr_e_maximal_prefixwitnessminornonzeroevaluationdeterminanthscrc))) /\ ((mdr_z_maximal_prefixwitnessminornonzeroevaluationdeterminanthscr) = ((mdr_c_maximal_prefixwitnessminornonzeroevaluationdeterminanthscrc) + (mdr_f_maximal_prefixwitnessminornonzeroevaluationdeterminanthscrc)) * S ((mdr_c_maximal_prefixwitnessminornonzeroevaluationdeterminanthscrc) + (mdr_f_maximal_prefixwitnessminornonzeroevaluationdeterminanthscrc)) + ((mdr_f_maximal_prefixwitnessminornonzeroevaluationdeterminanthscrc) + (mdr_f_maximal_prefixwitnessminornonzeroevaluationdeterminanthscrc))))))))) /\ (((exists ff_h_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthscrb. ff_h_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthscrb + S (mdr_z_maximal_prefixwitnessminornonzeroevaluationdeterminanthscr) = S ((S (mdr_i_maximal_prefixwitnessminornonzeroevaluationdeterminanthsc)) * mdr_c_maximal_prefixwitnessminornonzeroevaluationdeterminant)) /\ exists ff_q_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthscrb. mdr_b_maximal_prefixwitnessminornonzeroevaluationdeterminant = ff_q_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthscrb * S ((S (mdr_i_maximal_prefixwitnessminornonzeroevaluationdeterminanthsc)) * mdr_c_maximal_prefixwitnessminornonzeroevaluationdeterminant) + (mdr_z_maximal_prefixwitnessminornonzeroevaluationdeterminanthscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthscm_positive. (exists ff_gap_mdm_lt_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthscm_positive_index_bound. ff_gap_mdm_lt_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthscm_positive) = ((mdr_q_maximal_prefixwitnessminornonzeroevaluationdeterminanths) * (mdr_q_maximal_prefixwitnessminornonzeroevaluationdeterminanths))) -> exists ff_row_mdm_prefix_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthscm_positive ff_column_mdm_prefix_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthscm_positive ff_value_mdm_prefix_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthscm_positive. (ff_index_mdm_prefix_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthscm_positive = (mdr_q_maximal_prefixwitnessminornonzeroevaluationdeterminanths) * ff_row_mdm_prefix_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthscm_positive + ff_column_mdm_prefix_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthscm_positive /\ ((exists ff_gap_mdm_lt_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthscm_positive_column_bound. ff_gap_mdm_lt_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthscm_positive) = (mdr_q_maximal_prefixwitnessminornonzeroevaluationdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthscm_positive_cell ff_column_mdm_cell_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthscm_positive_cell = ff_row_mdm_prefix_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthscm_positive_cell_row_after. ff_gap_mdm_le_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthscm_positive)) /\ ff_row_mdm_cell_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthscm_positive_cell = S ff_row_mdm_prefix_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthscm_positive) = (mdr_j_maximal_prefixwitnessminornonzeroevaluationdeterminanthsc)) /\ ff_column_mdm_cell_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthscm_positive_cell = ff_column_mdm_prefix_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthscm_positive_cell_column_after. ff_gap_mdm_le_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthscm_positive_cell_column_after + (mdr_j_maximal_prefixwitnessminornonzeroevaluationdeterminanthsc) = (ff_column_mdm_prefix_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthscm_positive)) /\ ff_column_mdm_cell_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthscm_positive_cell = S ff_column_mdm_prefix_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthscm_positive))) /\ (((exists ff_h_mdm_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthscm_positive_cell_source. ff_h_mdm_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthscm_positive) = S ((S ((ff_row_mdm_cell_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthscm_positive_cell) * (S (mdr_q_maximal_prefixwitnessminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthscm_positive_cell))) * mdr_pc_maximal_prefixwitnessminornonzeroevaluationdeterminanth)) /\ exists ff_q_mdm_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthscm_positive_cell_source. mdr_pb_maximal_prefixwitnessminornonzeroevaluationdeterminanth = ff_q_mdm_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthscm_positive_cell) * (S (mdr_q_maximal_prefixwitnessminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthscm_positive_cell))) * mdr_pc_maximal_prefixwitnessminornonzeroevaluationdeterminanth) + (ff_value_mdm_prefix_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthscm_positive)))))) /\ (((exists ff_h_mdm_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthscm_positive_target. ff_h_mdm_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthscm_positive_target + S (ff_value_mdm_prefix_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthscm_positive) = S ((S (ff_index_mdm_prefix_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthscm_positive)) * mdr_us_maximal_prefixwitnessminornonzeroevaluationdeterminanthsc)) /\ exists ff_q_mdm_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthscm_positive_target. mdr_up_maximal_prefixwitnessminornonzeroevaluationdeterminanthsc = ff_q_mdm_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthscm_positive)) * mdr_us_maximal_prefixwitnessminornonzeroevaluationdeterminanthsc) + (ff_value_mdm_prefix_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthscm_negative. (exists ff_gap_mdm_lt_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthscm_negative_index_bound. ff_gap_mdm_lt_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthscm_negative) = ((mdr_q_maximal_prefixwitnessminornonzeroevaluationdeterminanths) * (mdr_q_maximal_prefixwitnessminornonzeroevaluationdeterminanths))) -> exists ff_row_mdm_prefix_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthscm_negative ff_column_mdm_prefix_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthscm_negative ff_value_mdm_prefix_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthscm_negative. (ff_index_mdm_prefix_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthscm_negative = (mdr_q_maximal_prefixwitnessminornonzeroevaluationdeterminanths) * ff_row_mdm_prefix_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthscm_negative + ff_column_mdm_prefix_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthscm_negative /\ ((exists ff_gap_mdm_lt_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthscm_negative_column_bound. ff_gap_mdm_lt_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthscm_negative) = (mdr_q_maximal_prefixwitnessminornonzeroevaluationdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthscm_negative_cell ff_column_mdm_cell_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthscm_negative_cell = ff_row_mdm_prefix_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthscm_negative_cell_row_after. ff_gap_mdm_le_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthscm_negative)) /\ ff_row_mdm_cell_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthscm_negative_cell = S ff_row_mdm_prefix_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthscm_negative) = (mdr_j_maximal_prefixwitnessminornonzeroevaluationdeterminanthsc)) /\ ff_column_mdm_cell_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthscm_negative_cell = ff_column_mdm_prefix_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthscm_negative_cell_column_after. ff_gap_mdm_le_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthscm_negative_cell_column_after + (mdr_j_maximal_prefixwitnessminornonzeroevaluationdeterminanthsc) = (ff_column_mdm_prefix_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthscm_negative)) /\ ff_column_mdm_cell_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthscm_negative_cell = S ff_column_mdm_prefix_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthscm_negative))) /\ (((exists ff_h_mdm_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthscm_negative_cell_source. ff_h_mdm_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthscm_negative) = S ((S ((ff_row_mdm_cell_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthscm_negative_cell) * (S (mdr_q_maximal_prefixwitnessminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthscm_negative_cell))) * mdr_nc_maximal_prefixwitnessminornonzeroevaluationdeterminanth)) /\ exists ff_q_mdm_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthscm_negative_cell_source. mdr_nb_maximal_prefixwitnessminornonzeroevaluationdeterminanth = ff_q_mdm_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthscm_negative_cell) * (S (mdr_q_maximal_prefixwitnessminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthscm_negative_cell))) * mdr_nc_maximal_prefixwitnessminornonzeroevaluationdeterminanth) + (ff_value_mdm_prefix_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthscm_negative)))))) /\ (((exists ff_h_mdm_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthscm_negative_target. ff_h_mdm_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthscm_negative_target + S (ff_value_mdm_prefix_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthscm_negative) = S ((S (ff_index_mdm_prefix_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthscm_negative)) * mdr_ut_maximal_prefixwitnessminornonzeroevaluationdeterminanthsc)) /\ exists ff_q_mdm_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthscm_negative_target. mdr_un_maximal_prefixwitnessminornonzeroevaluationdeterminanthsc = ff_q_mdm_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthscm_negative)) * mdr_ut_maximal_prefixwitnessminornonzeroevaluationdeterminanthsc) + (ff_value_mdm_prefix_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthscm_negative))))))))) /\ ((((exists ff_h_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthscp. ff_h_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthscp + S (mdr_p_maximal_prefixwitnessminornonzeroevaluationdeterminanthsc) = S ((S (mdr_j_maximal_prefixwitnessminornonzeroevaluationdeterminanthsc)) * mdr_ec_maximal_prefixwitnessminornonzeroevaluationdeterminanths)) /\ exists ff_q_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthscp. mdr_eb_maximal_prefixwitnessminornonzeroevaluationdeterminanths = ff_q_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthscp * S ((S (mdr_j_maximal_prefixwitnessminornonzeroevaluationdeterminanthsc)) * mdr_ec_maximal_prefixwitnessminornonzeroevaluationdeterminanths) + (mdr_p_maximal_prefixwitnessminornonzeroevaluationdeterminanthsc))) /\ (((exists ff_h_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthscn. ff_h_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthscn + S (mdr_n_maximal_prefixwitnessminornonzeroevaluationdeterminanthsc) = S ((S (mdr_j_maximal_prefixwitnessminornonzeroevaluationdeterminanthsc)) * mdr_fc_maximal_prefixwitnessminornonzeroevaluationdeterminanths)) /\ exists ff_q_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthscn. mdr_fb_maximal_prefixwitnessminornonzeroevaluationdeterminanths = ff_q_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthscn * S ((S (mdr_j_maximal_prefixwitnessminornonzeroevaluationdeterminanthsc)) * mdr_fc_maximal_prefixwitnessminornonzeroevaluationdeterminanths) + (mdr_n_maximal_prefixwitnessminornonzeroevaluationdeterminanthsc)))))))) /\ (exists ff_ub_mce_fold_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf ff_uc_mce_fold_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf ff_vb_mce_fold_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf ff_vc_mce_fold_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf. ((forall ff_index_mce_alternating_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_prefix. (exists ff_gap_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_prefix_index. ff_gap_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_prefix_index + S (ff_index_mce_alternating_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_prefix) = (S (mdr_q_maximal_prefixwitnessminornonzeroevaluationdeterminanths))) -> exists ff_ap_mce_alternating_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_prefix ff_an_mce_alternating_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_prefix ff_bp_mce_alternating_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_prefix ff_bn_mce_alternating_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_prefix ff_p_mce_alternating_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_prefix ff_n_mce_alternating_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_prefix. ((((exists ff_h_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_prefix_ap. ff_h_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_prefix_ap + S (ff_ap_mce_alternating_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_prefix)) * mdr_pc_maximal_prefixwitnessminornonzeroevaluationdeterminanth)) /\ exists ff_q_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_prefix_ap. mdr_pb_maximal_prefixwitnessminornonzeroevaluationdeterminanth = ff_q_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_prefix)) * mdr_pc_maximal_prefixwitnessminornonzeroevaluationdeterminanth) + (ff_ap_mce_alternating_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_prefix_an. ff_h_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_prefix_an + S (ff_an_mce_alternating_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_prefix)) * mdr_nc_maximal_prefixwitnessminornonzeroevaluationdeterminanth)) /\ exists ff_q_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_prefix_an. mdr_nb_maximal_prefixwitnessminornonzeroevaluationdeterminanth = ff_q_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_prefix)) * mdr_nc_maximal_prefixwitnessminornonzeroevaluationdeterminanth) + (ff_an_mce_alternating_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_prefix_bp. ff_h_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_prefix_bp + S (ff_bp_mce_alternating_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_prefix)) * mdr_ec_maximal_prefixwitnessminornonzeroevaluationdeterminanths)) /\ exists ff_q_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_prefix_bp. mdr_eb_maximal_prefixwitnessminornonzeroevaluationdeterminanths = ff_q_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_prefix)) * mdr_ec_maximal_prefixwitnessminornonzeroevaluationdeterminanths) + (ff_bp_mce_alternating_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_prefix_bn. ff_h_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_prefix_bn + S (ff_bn_mce_alternating_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_prefix)) * mdr_fc_maximal_prefixwitnessminornonzeroevaluationdeterminanths)) /\ exists ff_q_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_prefix_bn. mdr_fb_maximal_prefixwitnessminornonzeroevaluationdeterminanths = ff_q_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_prefix)) * mdr_fc_maximal_prefixwitnessminornonzeroevaluationdeterminanths) + (ff_bn_mce_alternating_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_prefix_positive. ff_h_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_prefix_positive + S (ff_p_mce_alternating_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_prefix_positive. ff_ub_mce_fold_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf) + (ff_p_mce_alternating_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_prefix_negative. ff_h_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_prefix_negative + S (ff_n_mce_alternating_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_prefix_negative. ff_vb_mce_fold_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf) + (ff_n_mce_alternating_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_prefix))) /\ (((exists ff_even_mce_term_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_prefix = 2 * ff_even_mce_term_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_prefix_term) /\ (ff_p_mce_alternating_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_prefix = 2 * ff_odd_mce_term_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_positive ff_v_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_positive. ((((exists ff_h_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_positive_start. ff_h_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_positive_start. ff_u_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_positive_start * S ((S (0)) * ff_v_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_positive_terminal. ff_h_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_positive_terminal + S (mdr_p_maximal_prefixwitnessminornonzeroevaluationdeterminanth) = S ((S ((S (mdr_q_maximal_prefixwitnessminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_positive_terminal. ff_u_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_positive_terminal * S ((S ((S (mdr_q_maximal_prefixwitnessminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_positive) + (mdr_p_maximal_prefixwitnessminornonzeroevaluationdeterminanth))) /\ forall ff_i_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_positive. (exists ff_lt_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_positive_bound. ff_lt_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_positive_bound + S ff_i_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_positive = (S (mdr_q_maximal_prefixwitnessminornonzeroevaluationdeterminanths))) -> exists ff_a_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_positive ff_r_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_positive ff_s_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_positive. ((((exists ff_h_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_positive_summand. ff_h_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_positive_summand + S (ff_a_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_positive_summand. ff_ub_mce_fold_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_positive_summand * S ((S (ff_i_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf) + (ff_a_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_positive_partial. ff_h_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_positive_partial + S (ff_r_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_positive_partial. ff_u_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_positive_partial * S ((S (ff_i_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_positive) + (ff_r_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_positive_successor. ff_h_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_positive_successor + S (ff_s_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_positive) = S ((S (S ff_i_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_positive_successor. ff_u_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_positive_successor * S ((S (S ff_i_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_positive) + (ff_s_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_positive))) /\ ff_s_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_positive = ff_r_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_positive + ff_a_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_positive)))))) /\ (exists ff_u_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_negative ff_v_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_negative. ((((exists ff_h_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_negative_start. ff_h_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_negative_start. ff_u_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_negative_start * S ((S (0)) * ff_v_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_negative_terminal. ff_h_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_negative_terminal + S (mdr_n_maximal_prefixwitnessminornonzeroevaluationdeterminanth) = S ((S ((S (mdr_q_maximal_prefixwitnessminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_negative_terminal. ff_u_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_negative_terminal * S ((S ((S (mdr_q_maximal_prefixwitnessminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_negative) + (mdr_n_maximal_prefixwitnessminornonzeroevaluationdeterminanth))) /\ forall ff_i_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_negative. (exists ff_lt_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_negative_bound. ff_lt_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_negative_bound + S ff_i_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_negative = (S (mdr_q_maximal_prefixwitnessminornonzeroevaluationdeterminanths))) -> exists ff_a_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_negative ff_r_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_negative ff_s_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_negative. ((((exists ff_h_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_negative_summand. ff_h_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_negative_summand + S (ff_a_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_negative_summand. ff_vb_mce_fold_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_negative_summand * S ((S (ff_i_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf) + (ff_a_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_negative_partial. ff_h_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_negative_partial + S (ff_r_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_negative_partial. ff_u_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_negative_partial * S ((S (ff_i_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_negative) + (ff_r_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_negative_successor. ff_h_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_negative_successor + S (ff_s_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_negative) = S ((S (S ff_i_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_negative_successor. ff_u_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_negative_successor * S ((S (S ff_i_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_negative) + (ff_s_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_negative))) /\ ff_s_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_negative = ff_r_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_negative + ff_a_mce_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminanthsf_negative))))))))))))))) /\ ((exists mdr_gap_maximal_prefixwitnessminornonzeroevaluationdeterminanti. mdr_gap_maximal_prefixwitnessminornonzeroevaluationdeterminanti + S (mdr_i_maximal_prefixwitnessminornonzeroevaluationdeterminant) = (mdr_l_maximal_prefixwitnessminornonzeroevaluationdeterminant)) /\ (exists mdr_z_maximal_prefixwitnessminornonzeroevaluationdeterminantr. ((exists mdr_a_maximal_prefixwitnessminornonzeroevaluationdeterminantrc mdr_b_maximal_prefixwitnessminornonzeroevaluationdeterminantrc mdr_c_maximal_prefixwitnessminornonzeroevaluationdeterminantrc mdr_e_maximal_prefixwitnessminornonzeroevaluationdeterminantrc mdr_f_maximal_prefixwitnessminornonzeroevaluationdeterminantrc. ((mdr_a_maximal_prefixwitnessminornonzeroevaluationdeterminantrc = ((rank) + (mdr_ub_maximal_prefixwitnessminornonzeroevaluation)) * S ((rank) + (mdr_ub_maximal_prefixwitnessminornonzeroevaluation)) + ((mdr_ub_maximal_prefixwitnessminornonzeroevaluation) + (mdr_ub_maximal_prefixwitnessminornonzeroevaluation))) /\ ((mdr_b_maximal_prefixwitnessminornonzeroevaluationdeterminantrc = ((mdr_uc_maximal_prefixwitnessminornonzeroevaluation) + (mdr_vb_maximal_prefixwitnessminornonzeroevaluation)) * S ((mdr_uc_maximal_prefixwitnessminornonzeroevaluation) + (mdr_vb_maximal_prefixwitnessminornonzeroevaluation)) + ((mdr_vb_maximal_prefixwitnessminornonzeroevaluation) + (mdr_vb_maximal_prefixwitnessminornonzeroevaluation))) /\ ((mdr_c_maximal_prefixwitnessminornonzeroevaluationdeterminantrc = ((mdr_a_maximal_prefixwitnessminornonzeroevaluationdeterminantrc) + (mdr_b_maximal_prefixwitnessminornonzeroevaluationdeterminantrc)) * S ((mdr_a_maximal_prefixwitnessminornonzeroevaluationdeterminantrc) + (mdr_b_maximal_prefixwitnessminornonzeroevaluationdeterminantrc)) + ((mdr_b_maximal_prefixwitnessminornonzeroevaluationdeterminantrc) + (mdr_b_maximal_prefixwitnessminornonzeroevaluationdeterminantrc))) /\ ((mdr_e_maximal_prefixwitnessminornonzeroevaluationdeterminantrc = ((mdr_p_maximal_prefixwitnessminornonzero) + (mdr_n_maximal_prefixwitnessminornonzero)) * S ((mdr_p_maximal_prefixwitnessminornonzero) + (mdr_n_maximal_prefixwitnessminornonzero)) + ((mdr_n_maximal_prefixwitnessminornonzero) + (mdr_n_maximal_prefixwitnessminornonzero))) /\ ((mdr_f_maximal_prefixwitnessminornonzeroevaluationdeterminantrc = ((mdr_vc_maximal_prefixwitnessminornonzeroevaluation) + (mdr_e_maximal_prefixwitnessminornonzeroevaluationdeterminantrc)) * S ((mdr_vc_maximal_prefixwitnessminornonzeroevaluation) + (mdr_e_maximal_prefixwitnessminornonzeroevaluationdeterminantrc)) + ((mdr_e_maximal_prefixwitnessminornonzeroevaluationdeterminantrc) + (mdr_e_maximal_prefixwitnessminornonzeroevaluationdeterminantrc))) /\ ((mdr_z_maximal_prefixwitnessminornonzeroevaluationdeterminantr) = ((mdr_c_maximal_prefixwitnessminornonzeroevaluationdeterminantrc) + (mdr_f_maximal_prefixwitnessminornonzeroevaluationdeterminantrc)) * S ((mdr_c_maximal_prefixwitnessminornonzeroevaluationdeterminantrc) + (mdr_f_maximal_prefixwitnessminornonzeroevaluationdeterminantrc)) + ((mdr_f_maximal_prefixwitnessminornonzeroevaluationdeterminantrc) + (mdr_f_maximal_prefixwitnessminornonzeroevaluationdeterminantrc))))))))) /\ (((exists ff_h_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminantrb. ff_h_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminantrb + S (mdr_z_maximal_prefixwitnessminornonzeroevaluationdeterminantr) = S ((S (mdr_i_maximal_prefixwitnessminornonzeroevaluationdeterminant)) * mdr_c_maximal_prefixwitnessminornonzeroevaluationdeterminant)) /\ exists ff_q_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminantrb. mdr_b_maximal_prefixwitnessminornonzeroevaluationdeterminant = ff_q_mdr_maximal_prefixwitnessminornonzeroevaluationdeterminantrb * S ((S (mdr_i_maximal_prefixwitnessminornonzeroevaluationdeterminant)) * mdr_c_maximal_prefixwitnessminornonzeroevaluationdeterminant) + (mdr_z_maximal_prefixwitnessminornonzeroevaluationdeterminantr)))))))))) /\ (~(mdr_p_maximal_prefixwitnessminornonzero = mdr_n_maximal_prefixwitnessminornonzero)))))))) /\ (forall mdr_j_maximal_prefixhigher. (exists mdr_gap_maximal_prefixhigherabove. mdr_gap_maximal_prefixhigherabove + S (rank) = (mdr_j_maximal_prefixhigher)) -> (exists mdr_gap_maximal_prefixhigherlimit. mdr_gap_maximal_prefixhigherlimit + (mdr_j_maximal_prefixhigher) = (K)) -> ~(exists mdr_rb_maximal_prefixhigherminor mdr_rc_maximal_prefixhigherminor mdr_cb_maximal_prefixhigherminor mdr_cc_maximal_prefixhigherminor. (((((forall fom_index_mrf_maximal_prefixhigherminorminorrowsbound. (exists fom_gap_mrf_maximal_prefixhigherminorminorrowsbound_index_bound. fom_gap_mrf_maximal_prefixhigherminorminorrowsbound_index_bound + S (fom_index_mrf_maximal_prefixhigherminorminorrowsbound) = mdr_j_maximal_prefixhigher) -> exists fom_value_mrf_maximal_prefixhigherminorminorrowsbound. ((((exists fom_beta_height_mrf_maximal_prefixhigherminorminorrowsbound_entry. fom_beta_height_mrf_maximal_prefixhigherminorminorrowsbound_entry + S (fom_value_mrf_maximal_prefixhigherminorminorrowsbound) = S ((S (fom_index_mrf_maximal_prefixhigherminorminorrowsbound)) * mdr_rc_maximal_prefixhigherminor)) /\ exists fom_beta_quotient_mrf_maximal_prefixhigherminorminorrowsbound_entry. mdr_rb_maximal_prefixhigherminor = fom_beta_quotient_mrf_maximal_prefixhigherminorminorrowsbound_entry * S ((S (fom_index_mrf_maximal_prefixhigherminorminorrowsbound)) * mdr_rc_maximal_prefixhigherminor) + (fom_value_mrf_maximal_prefixhigherminorminorrowsbound))) /\ (exists fom_gap_mrf_maximal_prefixhigherminorminorrowsbound_value_bound. fom_gap_mrf_maximal_prefixhigherminorminorrowsbound_value_bound + S (fom_value_mrf_maximal_prefixhigherminorminorrowsbound) = r))) /\ (forall mdr_i_maximal_prefixhigherminorminorrowsdistinct mdr_j_maximal_prefixhigherminorminorrowsdistinct mdr_a_maximal_prefixhigherminorminorrowsdistinct. (exists mdr_gap_maximal_prefixhigherminorminorrowsdistincti. mdr_gap_maximal_prefixhigherminorminorrowsdistincti + S (mdr_i_maximal_prefixhigherminorminorrowsdistinct) = (mdr_j_maximal_prefixhigher)) -> (exists mdr_gap_maximal_prefixhigherminorminorrowsdistinctj. mdr_gap_maximal_prefixhigherminorminorrowsdistinctj + S (mdr_j_maximal_prefixhigherminorminorrowsdistinct) = (mdr_j_maximal_prefixhigher)) -> (((exists ff_h_mdr_maximal_prefixhigherminorminorrowsdistinctfirst. ff_h_mdr_maximal_prefixhigherminorminorrowsdistinctfirst + S (mdr_a_maximal_prefixhigherminorminorrowsdistinct) = S ((S (mdr_i_maximal_prefixhigherminorminorrowsdistinct)) * mdr_rc_maximal_prefixhigherminor)) /\ exists ff_q_mdr_maximal_prefixhigherminorminorrowsdistinctfirst. mdr_rb_maximal_prefixhigherminor = ff_q_mdr_maximal_prefixhigherminorminorrowsdistinctfirst * S ((S (mdr_i_maximal_prefixhigherminorminorrowsdistinct)) * mdr_rc_maximal_prefixhigherminor) + (mdr_a_maximal_prefixhigherminorminorrowsdistinct))) -> (((exists ff_h_mdr_maximal_prefixhigherminorminorrowsdistinctsecond. ff_h_mdr_maximal_prefixhigherminorminorrowsdistinctsecond + S (mdr_a_maximal_prefixhigherminorminorrowsdistinct) = S ((S (mdr_j_maximal_prefixhigherminorminorrowsdistinct)) * mdr_rc_maximal_prefixhigherminor)) /\ exists ff_q_mdr_maximal_prefixhigherminorminorrowsdistinctsecond. mdr_rb_maximal_prefixhigherminor = ff_q_mdr_maximal_prefixhigherminorminorrowsdistinctsecond * S ((S (mdr_j_maximal_prefixhigherminorminorrowsdistinct)) * mdr_rc_maximal_prefixhigherminor) + (mdr_a_maximal_prefixhigherminorminorrowsdistinct))) -> mdr_i_maximal_prefixhigherminorminorrowsdistinct = mdr_j_maximal_prefixhigherminorminorrowsdistinct))) /\ ((((forall fom_index_mrf_maximal_prefixhigherminorminorcolumnsbound. (exists fom_gap_mrf_maximal_prefixhigherminorminorcolumnsbound_index_bound. fom_gap_mrf_maximal_prefixhigherminorminorcolumnsbound_index_bound + S (fom_index_mrf_maximal_prefixhigherminorminorcolumnsbound) = mdr_j_maximal_prefixhigher) -> exists fom_value_mrf_maximal_prefixhigherminorminorcolumnsbound. ((((exists fom_beta_height_mrf_maximal_prefixhigherminorminorcolumnsbound_entry. fom_beta_height_mrf_maximal_prefixhigherminorminorcolumnsbound_entry + S (fom_value_mrf_maximal_prefixhigherminorminorcolumnsbound) = S ((S (fom_index_mrf_maximal_prefixhigherminorminorcolumnsbound)) * mdr_cc_maximal_prefixhigherminor)) /\ exists fom_beta_quotient_mrf_maximal_prefixhigherminorminorcolumnsbound_entry. mdr_cb_maximal_prefixhigherminor = fom_beta_quotient_mrf_maximal_prefixhigherminorminorcolumnsbound_entry * S ((S (fom_index_mrf_maximal_prefixhigherminorminorcolumnsbound)) * mdr_cc_maximal_prefixhigherminor) + (fom_value_mrf_maximal_prefixhigherminorminorcolumnsbound))) /\ (exists fom_gap_mrf_maximal_prefixhigherminorminorcolumnsbound_value_bound. fom_gap_mrf_maximal_prefixhigherminorminorcolumnsbound_value_bound + S (fom_value_mrf_maximal_prefixhigherminorminorcolumnsbound) = w))) /\ (forall mdr_i_maximal_prefixhigherminorminorcolumnsdistinct mdr_j_maximal_prefixhigherminorminorcolumnsdistinct mdr_a_maximal_prefixhigherminorminorcolumnsdistinct. (exists mdr_gap_maximal_prefixhigherminorminorcolumnsdistincti. mdr_gap_maximal_prefixhigherminorminorcolumnsdistincti + S (mdr_i_maximal_prefixhigherminorminorcolumnsdistinct) = (mdr_j_maximal_prefixhigher)) -> (exists mdr_gap_maximal_prefixhigherminorminorcolumnsdistinctj. mdr_gap_maximal_prefixhigherminorminorcolumnsdistinctj + S (mdr_j_maximal_prefixhigherminorminorcolumnsdistinct) = (mdr_j_maximal_prefixhigher)) -> (((exists ff_h_mdr_maximal_prefixhigherminorminorcolumnsdistinctfirst. ff_h_mdr_maximal_prefixhigherminorminorcolumnsdistinctfirst + S (mdr_a_maximal_prefixhigherminorminorcolumnsdistinct) = S ((S (mdr_i_maximal_prefixhigherminorminorcolumnsdistinct)) * mdr_cc_maximal_prefixhigherminor)) /\ exists ff_q_mdr_maximal_prefixhigherminorminorcolumnsdistinctfirst. mdr_cb_maximal_prefixhigherminor = ff_q_mdr_maximal_prefixhigherminorminorcolumnsdistinctfirst * S ((S (mdr_i_maximal_prefixhigherminorminorcolumnsdistinct)) * mdr_cc_maximal_prefixhigherminor) + (mdr_a_maximal_prefixhigherminorminorcolumnsdistinct))) -> (((exists ff_h_mdr_maximal_prefixhigherminorminorcolumnsdistinctsecond. ff_h_mdr_maximal_prefixhigherminorminorcolumnsdistinctsecond + S (mdr_a_maximal_prefixhigherminorminorcolumnsdistinct) = S ((S (mdr_j_maximal_prefixhigherminorminorcolumnsdistinct)) * mdr_cc_maximal_prefixhigherminor)) /\ exists ff_q_mdr_maximal_prefixhigherminorminorcolumnsdistinctsecond. mdr_cb_maximal_prefixhigherminor = ff_q_mdr_maximal_prefixhigherminorminorcolumnsdistinctsecond * S ((S (mdr_j_maximal_prefixhigherminorminorcolumnsdistinct)) * mdr_cc_maximal_prefixhigherminor) + (mdr_a_maximal_prefixhigherminorminorcolumnsdistinct))) -> mdr_i_maximal_prefixhigherminorminorcolumnsdistinct = mdr_j_maximal_prefixhigherminorminorcolumnsdistinct))) /\ (exists mdr_p_maximal_prefixhigherminorminornonzero mdr_n_maximal_prefixhigherminorminornonzero. ((exists mdr_ub_maximal_prefixhigherminorminornonzeroevaluation mdr_uc_maximal_prefixhigherminorminornonzeroevaluation mdr_vb_maximal_prefixhigherminorminornonzeroevaluation mdr_vc_maximal_prefixhigherminorminornonzeroevaluation. ((((forall mdr_i_maximal_prefixhigherminorminornonzeroevaluationmatrixpositive. (exists mdr_gap_maximal_prefixhigherminorminornonzeroevaluationmatrixpositivebound. mdr_gap_maximal_prefixhigherminorminornonzeroevaluationmatrixpositivebound + S (mdr_i_maximal_prefixhigherminorminornonzeroevaluationmatrixpositive) = ((mdr_j_maximal_prefixhigher) * (mdr_j_maximal_prefixhigher))) -> exists mdr_a_maximal_prefixhigherminorminornonzeroevaluationmatrixpositive. (((exists mdr_r_maximal_prefixhigherminorminornonzeroevaluationmatrixpositivepoint mdr_s_maximal_prefixhigherminorminornonzeroevaluationmatrixpositivepoint mdr_u_maximal_prefixhigherminorminornonzeroevaluationmatrixpositivepoint mdr_v_maximal_prefixhigherminorminornonzeroevaluationmatrixpositivepoint. ((mdr_i_maximal_prefixhigherminorminornonzeroevaluationmatrixpositive = (mdr_j_maximal_prefixhigher) * mdr_r_maximal_prefixhigherminorminornonzeroevaluationmatrixpositivepoint + mdr_s_maximal_prefixhigherminorminornonzeroevaluationmatrixpositivepoint) /\ ((exists mdr_gap_maximal_prefixhigherminorminornonzeroevaluationmatrixpositivepointcolumn. mdr_gap_maximal_prefixhigherminorminornonzeroevaluationmatrixpositivepointcolumn + S (mdr_s_maximal_prefixhigherminorminornonzeroevaluationmatrixpositivepoint) = (mdr_j_maximal_prefixhigher)) /\ ((((exists ff_h_mdr_maximal_prefixhigherminorminornonzeroevaluationmatrixpositivepointrow_index. ff_h_mdr_maximal_prefixhigherminorminornonzeroevaluationmatrixpositivepointrow_index + S (mdr_u_maximal_prefixhigherminorminornonzeroevaluationmatrixpositivepoint) = S ((S (mdr_r_maximal_prefixhigherminorminornonzeroevaluationmatrixpositivepoint)) * mdr_rc_maximal_prefixhigherminor)) /\ exists ff_q_mdr_maximal_prefixhigherminorminornonzeroevaluationmatrixpositivepointrow_index. mdr_rb_maximal_prefixhigherminor = ff_q_mdr_maximal_prefixhigherminorminornonzeroevaluationmatrixpositivepointrow_index * S ((S (mdr_r_maximal_prefixhigherminorminornonzeroevaluationmatrixpositivepoint)) * mdr_rc_maximal_prefixhigherminor) + (mdr_u_maximal_prefixhigherminorminornonzeroevaluationmatrixpositivepoint))) /\ ((((exists ff_h_mdr_maximal_prefixhigherminorminornonzeroevaluationmatrixpositivepointcolumn_index. ff_h_mdr_maximal_prefixhigherminorminornonzeroevaluationmatrixpositivepointcolumn_index + S (mdr_v_maximal_prefixhigherminorminornonzeroevaluationmatrixpositivepoint) = S ((S (mdr_s_maximal_prefixhigherminorminornonzeroevaluationmatrixpositivepoint)) * mdr_cc_maximal_prefixhigherminor)) /\ exists ff_q_mdr_maximal_prefixhigherminorminornonzeroevaluationmatrixpositivepointcolumn_index. mdr_cb_maximal_prefixhigherminor = ff_q_mdr_maximal_prefixhigherminorminornonzeroevaluationmatrixpositivepointcolumn_index * S ((S (mdr_s_maximal_prefixhigherminorminornonzeroevaluationmatrixpositivepoint)) * mdr_cc_maximal_prefixhigherminor) + (mdr_v_maximal_prefixhigherminorminornonzeroevaluationmatrixpositivepoint))) /\ (((exists ff_h_mdr_maximal_prefixhigherminorminornonzeroevaluationmatrixpositivepointsource. ff_h_mdr_maximal_prefixhigherminorminornonzeroevaluationmatrixpositivepointsource + S (mdr_a_maximal_prefixhigherminorminornonzeroevaluationmatrixpositive) = S ((S ((mdr_u_maximal_prefixhigherminorminornonzeroevaluationmatrixpositivepoint) * (w) + (mdr_v_maximal_prefixhigherminorminornonzeroevaluationmatrixpositivepoint))) * pc)) /\ exists ff_q_mdr_maximal_prefixhigherminorminornonzeroevaluationmatrixpositivepointsource. pb = ff_q_mdr_maximal_prefixhigherminorminornonzeroevaluationmatrixpositivepointsource * S ((S ((mdr_u_maximal_prefixhigherminorminornonzeroevaluationmatrixpositivepoint) * (w) + (mdr_v_maximal_prefixhigherminorminornonzeroevaluationmatrixpositivepoint))) * pc) + (mdr_a_maximal_prefixhigherminorminornonzeroevaluationmatrixpositive)))))))) /\ (((exists ff_h_mdr_maximal_prefixhigherminorminornonzeroevaluationmatrixpositiveoutput. ff_h_mdr_maximal_prefixhigherminorminornonzeroevaluationmatrixpositiveoutput + S (mdr_a_maximal_prefixhigherminorminornonzeroevaluationmatrixpositive) = S ((S (mdr_i_maximal_prefixhigherminorminornonzeroevaluationmatrixpositive)) * mdr_uc_maximal_prefixhigherminorminornonzeroevaluation)) /\ exists ff_q_mdr_maximal_prefixhigherminorminornonzeroevaluationmatrixpositiveoutput. mdr_ub_maximal_prefixhigherminorminornonzeroevaluation = ff_q_mdr_maximal_prefixhigherminorminornonzeroevaluationmatrixpositiveoutput * S ((S (mdr_i_maximal_prefixhigherminorminornonzeroevaluationmatrixpositive)) * mdr_uc_maximal_prefixhigherminorminornonzeroevaluation) + (mdr_a_maximal_prefixhigherminorminornonzeroevaluationmatrixpositive)))))) /\ (forall mdr_i_maximal_prefixhigherminorminornonzeroevaluationmatrixnegative. (exists mdr_gap_maximal_prefixhigherminorminornonzeroevaluationmatrixnegativebound. mdr_gap_maximal_prefixhigherminorminornonzeroevaluationmatrixnegativebound + S (mdr_i_maximal_prefixhigherminorminornonzeroevaluationmatrixnegative) = ((mdr_j_maximal_prefixhigher) * (mdr_j_maximal_prefixhigher))) -> exists mdr_a_maximal_prefixhigherminorminornonzeroevaluationmatrixnegative. (((exists mdr_r_maximal_prefixhigherminorminornonzeroevaluationmatrixnegativepoint mdr_s_maximal_prefixhigherminorminornonzeroevaluationmatrixnegativepoint mdr_u_maximal_prefixhigherminorminornonzeroevaluationmatrixnegativepoint mdr_v_maximal_prefixhigherminorminornonzeroevaluationmatrixnegativepoint. ((mdr_i_maximal_prefixhigherminorminornonzeroevaluationmatrixnegative = (mdr_j_maximal_prefixhigher) * mdr_r_maximal_prefixhigherminorminornonzeroevaluationmatrixnegativepoint + mdr_s_maximal_prefixhigherminorminornonzeroevaluationmatrixnegativepoint) /\ ((exists mdr_gap_maximal_prefixhigherminorminornonzeroevaluationmatrixnegativepointcolumn. mdr_gap_maximal_prefixhigherminorminornonzeroevaluationmatrixnegativepointcolumn + S (mdr_s_maximal_prefixhigherminorminornonzeroevaluationmatrixnegativepoint) = (mdr_j_maximal_prefixhigher)) /\ ((((exists ff_h_mdr_maximal_prefixhigherminorminornonzeroevaluationmatrixnegativepointrow_index. ff_h_mdr_maximal_prefixhigherminorminornonzeroevaluationmatrixnegativepointrow_index + S (mdr_u_maximal_prefixhigherminorminornonzeroevaluationmatrixnegativepoint) = S ((S (mdr_r_maximal_prefixhigherminorminornonzeroevaluationmatrixnegativepoint)) * mdr_rc_maximal_prefixhigherminor)) /\ exists ff_q_mdr_maximal_prefixhigherminorminornonzeroevaluationmatrixnegativepointrow_index. mdr_rb_maximal_prefixhigherminor = ff_q_mdr_maximal_prefixhigherminorminornonzeroevaluationmatrixnegativepointrow_index * S ((S (mdr_r_maximal_prefixhigherminorminornonzeroevaluationmatrixnegativepoint)) * mdr_rc_maximal_prefixhigherminor) + (mdr_u_maximal_prefixhigherminorminornonzeroevaluationmatrixnegativepoint))) /\ ((((exists ff_h_mdr_maximal_prefixhigherminorminornonzeroevaluationmatrixnegativepointcolumn_index. ff_h_mdr_maximal_prefixhigherminorminornonzeroevaluationmatrixnegativepointcolumn_index + S (mdr_v_maximal_prefixhigherminorminornonzeroevaluationmatrixnegativepoint) = S ((S (mdr_s_maximal_prefixhigherminorminornonzeroevaluationmatrixnegativepoint)) * mdr_cc_maximal_prefixhigherminor)) /\ exists ff_q_mdr_maximal_prefixhigherminorminornonzeroevaluationmatrixnegativepointcolumn_index. mdr_cb_maximal_prefixhigherminor = ff_q_mdr_maximal_prefixhigherminorminornonzeroevaluationmatrixnegativepointcolumn_index * S ((S (mdr_s_maximal_prefixhigherminorminornonzeroevaluationmatrixnegativepoint)) * mdr_cc_maximal_prefixhigherminor) + (mdr_v_maximal_prefixhigherminorminornonzeroevaluationmatrixnegativepoint))) /\ (((exists ff_h_mdr_maximal_prefixhigherminorminornonzeroevaluationmatrixnegativepointsource. ff_h_mdr_maximal_prefixhigherminorminornonzeroevaluationmatrixnegativepointsource + S (mdr_a_maximal_prefixhigherminorminornonzeroevaluationmatrixnegative) = S ((S ((mdr_u_maximal_prefixhigherminorminornonzeroevaluationmatrixnegativepoint) * (w) + (mdr_v_maximal_prefixhigherminorminornonzeroevaluationmatrixnegativepoint))) * nc)) /\ exists ff_q_mdr_maximal_prefixhigherminorminornonzeroevaluationmatrixnegativepointsource. nb = ff_q_mdr_maximal_prefixhigherminorminornonzeroevaluationmatrixnegativepointsource * S ((S ((mdr_u_maximal_prefixhigherminorminornonzeroevaluationmatrixnegativepoint) * (w) + (mdr_v_maximal_prefixhigherminorminornonzeroevaluationmatrixnegativepoint))) * nc) + (mdr_a_maximal_prefixhigherminorminornonzeroevaluationmatrixnegative)))))))) /\ (((exists ff_h_mdr_maximal_prefixhigherminorminornonzeroevaluationmatrixnegativeoutput. ff_h_mdr_maximal_prefixhigherminorminornonzeroevaluationmatrixnegativeoutput + S (mdr_a_maximal_prefixhigherminorminornonzeroevaluationmatrixnegative) = S ((S (mdr_i_maximal_prefixhigherminorminornonzeroevaluationmatrixnegative)) * mdr_vc_maximal_prefixhigherminorminornonzeroevaluation)) /\ exists ff_q_mdr_maximal_prefixhigherminorminornonzeroevaluationmatrixnegativeoutput. mdr_vb_maximal_prefixhigherminorminornonzeroevaluation = ff_q_mdr_maximal_prefixhigherminorminornonzeroevaluationmatrixnegativeoutput * S ((S (mdr_i_maximal_prefixhigherminorminornonzeroevaluationmatrixnegative)) * mdr_vc_maximal_prefixhigherminorminornonzeroevaluation) + (mdr_a_maximal_prefixhigherminorminornonzeroevaluationmatrixnegative)))))))) /\ (exists mdr_b_maximal_prefixhigherminorminornonzeroevaluationdeterminant mdr_c_maximal_prefixhigherminorminornonzeroevaluationdeterminant mdr_l_maximal_prefixhigherminorminornonzeroevaluationdeterminant mdr_i_maximal_prefixhigherminorminornonzeroevaluationdeterminant. ((forall mdr_i_maximal_prefixhigherminorminornonzeroevaluationdeterminanth. (exists mdr_gap_maximal_prefixhigherminorminornonzeroevaluationdeterminanthi. mdr_gap_maximal_prefixhigherminorminornonzeroevaluationdeterminanthi + S (mdr_i_maximal_prefixhigherminorminornonzeroevaluationdeterminanth) = (mdr_l_maximal_prefixhigherminorminornonzeroevaluationdeterminant)) -> exists mdr_d_maximal_prefixhigherminorminornonzeroevaluationdeterminanth mdr_pb_maximal_prefixhigherminorminornonzeroevaluationdeterminanth mdr_pc_maximal_prefixhigherminorminornonzeroevaluationdeterminanth mdr_nb_maximal_prefixhigherminorminornonzeroevaluationdeterminanth mdr_nc_maximal_prefixhigherminorminornonzeroevaluationdeterminanth mdr_p_maximal_prefixhigherminorminornonzeroevaluationdeterminanth mdr_n_maximal_prefixhigherminorminornonzeroevaluationdeterminanth. ((exists mdr_z_maximal_prefixhigherminorminornonzeroevaluationdeterminanthr. ((exists mdr_a_maximal_prefixhigherminorminornonzeroevaluationdeterminanthrc mdr_b_maximal_prefixhigherminorminornonzeroevaluationdeterminanthrc mdr_c_maximal_prefixhigherminorminornonzeroevaluationdeterminanthrc mdr_e_maximal_prefixhigherminorminornonzeroevaluationdeterminanthrc mdr_f_maximal_prefixhigherminorminornonzeroevaluationdeterminanthrc. ((mdr_a_maximal_prefixhigherminorminornonzeroevaluationdeterminanthrc = ((mdr_d_maximal_prefixhigherminorminornonzeroevaluationdeterminanth) + (mdr_pb_maximal_prefixhigherminorminornonzeroevaluationdeterminanth)) * S ((mdr_d_maximal_prefixhigherminorminornonzeroevaluationdeterminanth) + (mdr_pb_maximal_prefixhigherminorminornonzeroevaluationdeterminanth)) + ((mdr_pb_maximal_prefixhigherminorminornonzeroevaluationdeterminanth) + (mdr_pb_maximal_prefixhigherminorminornonzeroevaluationdeterminanth))) /\ ((mdr_b_maximal_prefixhigherminorminornonzeroevaluationdeterminanthrc = ((mdr_pc_maximal_prefixhigherminorminornonzeroevaluationdeterminanth) + (mdr_nb_maximal_prefixhigherminorminornonzeroevaluationdeterminanth)) * S ((mdr_pc_maximal_prefixhigherminorminornonzeroevaluationdeterminanth) + (mdr_nb_maximal_prefixhigherminorminornonzeroevaluationdeterminanth)) + ((mdr_nb_maximal_prefixhigherminorminornonzeroevaluationdeterminanth) + (mdr_nb_maximal_prefixhigherminorminornonzeroevaluationdeterminanth))) /\ ((mdr_c_maximal_prefixhigherminorminornonzeroevaluationdeterminanthrc = ((mdr_a_maximal_prefixhigherminorminornonzeroevaluationdeterminanthrc) + (mdr_b_maximal_prefixhigherminorminornonzeroevaluationdeterminanthrc)) * S ((mdr_a_maximal_prefixhigherminorminornonzeroevaluationdeterminanthrc) + (mdr_b_maximal_prefixhigherminorminornonzeroevaluationdeterminanthrc)) + ((mdr_b_maximal_prefixhigherminorminornonzeroevaluationdeterminanthrc) + (mdr_b_maximal_prefixhigherminorminornonzeroevaluationdeterminanthrc))) /\ ((mdr_e_maximal_prefixhigherminorminornonzeroevaluationdeterminanthrc = ((mdr_p_maximal_prefixhigherminorminornonzeroevaluationdeterminanth) + (mdr_n_maximal_prefixhigherminorminornonzeroevaluationdeterminanth)) * S ((mdr_p_maximal_prefixhigherminorminornonzeroevaluationdeterminanth) + (mdr_n_maximal_prefixhigherminorminornonzeroevaluationdeterminanth)) + ((mdr_n_maximal_prefixhigherminorminornonzeroevaluationdeterminanth) + (mdr_n_maximal_prefixhigherminorminornonzeroevaluationdeterminanth))) /\ ((mdr_f_maximal_prefixhigherminorminornonzeroevaluationdeterminanthrc = ((mdr_nc_maximal_prefixhigherminorminornonzeroevaluationdeterminanth) + (mdr_e_maximal_prefixhigherminorminornonzeroevaluationdeterminanthrc)) * S ((mdr_nc_maximal_prefixhigherminorminornonzeroevaluationdeterminanth) + (mdr_e_maximal_prefixhigherminorminornonzeroevaluationdeterminanthrc)) + ((mdr_e_maximal_prefixhigherminorminornonzeroevaluationdeterminanthrc) + (mdr_e_maximal_prefixhigherminorminornonzeroevaluationdeterminanthrc))) /\ ((mdr_z_maximal_prefixhigherminorminornonzeroevaluationdeterminanthr) = ((mdr_c_maximal_prefixhigherminorminornonzeroevaluationdeterminanthrc) + (mdr_f_maximal_prefixhigherminorminornonzeroevaluationdeterminanthrc)) * S ((mdr_c_maximal_prefixhigherminorminornonzeroevaluationdeterminanthrc) + (mdr_f_maximal_prefixhigherminorminornonzeroevaluationdeterminanthrc)) + ((mdr_f_maximal_prefixhigherminorminornonzeroevaluationdeterminanthrc) + (mdr_f_maximal_prefixhigherminorminornonzeroevaluationdeterminanthrc))))))))) /\ (((exists ff_h_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthrb. ff_h_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthrb + S (mdr_z_maximal_prefixhigherminorminornonzeroevaluationdeterminanthr) = S ((S (mdr_i_maximal_prefixhigherminorminornonzeroevaluationdeterminanth)) * mdr_c_maximal_prefixhigherminorminornonzeroevaluationdeterminant)) /\ exists ff_q_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthrb. mdr_b_maximal_prefixhigherminorminornonzeroevaluationdeterminant = ff_q_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthrb * S ((S (mdr_i_maximal_prefixhigherminorminornonzeroevaluationdeterminanth)) * mdr_c_maximal_prefixhigherminorminornonzeroevaluationdeterminant) + (mdr_z_maximal_prefixhigherminorminornonzeroevaluationdeterminanthr))))) /\ (((((mdr_d_maximal_prefixhigherminorminornonzeroevaluationdeterminanth) = 0) /\ (((mdr_p_maximal_prefixhigherminorminornonzeroevaluationdeterminanth) = 1) /\ ((mdr_n_maximal_prefixhigherminorminornonzeroevaluationdeterminanth) = 0))) \/ exists mdr_q_maximal_prefixhigherminorminornonzeroevaluationdeterminanths mdr_eb_maximal_prefixhigherminorminornonzeroevaluationdeterminanths mdr_ec_maximal_prefixhigherminorminornonzeroevaluationdeterminanths mdr_fb_maximal_prefixhigherminorminornonzeroevaluationdeterminanths mdr_fc_maximal_prefixhigherminorminornonzeroevaluationdeterminanths. (((mdr_d_maximal_prefixhigherminorminornonzeroevaluationdeterminanth) = S (mdr_q_maximal_prefixhigherminorminornonzeroevaluationdeterminanths)) /\ ((forall mdr_j_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsc. (exists mdr_gap_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscj. mdr_gap_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscj + S (mdr_j_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsc) = (S (mdr_q_maximal_prefixhigherminorminornonzeroevaluationdeterminanths))) -> exists mdr_i_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsc mdr_up_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsc mdr_us_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsc mdr_un_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsc mdr_ut_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsc mdr_p_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsc mdr_n_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsc. ((exists mdr_gap_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsci. mdr_gap_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsci + S (mdr_i_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsc) = (mdr_i_maximal_prefixhigherminorminornonzeroevaluationdeterminanth)) /\ ((exists mdr_z_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscr. ((exists mdr_a_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscrc mdr_b_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscrc mdr_c_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscrc mdr_e_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscrc mdr_f_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscrc. ((mdr_a_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscrc = ((mdr_q_maximal_prefixhigherminorminornonzeroevaluationdeterminanths) + (mdr_up_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsc)) * S ((mdr_q_maximal_prefixhigherminorminornonzeroevaluationdeterminanths) + (mdr_up_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsc)) + ((mdr_up_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsc) + (mdr_up_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsc))) /\ ((mdr_b_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscrc = ((mdr_us_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsc) + (mdr_un_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsc)) * S ((mdr_us_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsc) + (mdr_un_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsc)) + ((mdr_un_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsc) + (mdr_un_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsc))) /\ ((mdr_c_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscrc = ((mdr_a_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscrc) + (mdr_b_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscrc)) * S ((mdr_a_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscrc) + (mdr_b_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscrc)) + ((mdr_b_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscrc) + (mdr_b_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscrc))) /\ ((mdr_e_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscrc = ((mdr_p_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsc) + (mdr_n_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsc)) * S ((mdr_p_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsc) + (mdr_n_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsc)) + ((mdr_n_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsc) + (mdr_n_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsc))) /\ ((mdr_f_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscrc = ((mdr_ut_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsc) + (mdr_e_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscrc)) * S ((mdr_ut_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsc) + (mdr_e_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscrc)) + ((mdr_e_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscrc) + (mdr_e_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscrc))) /\ ((mdr_z_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscr) = ((mdr_c_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscrc) + (mdr_f_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscrc)) * S ((mdr_c_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscrc) + (mdr_f_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscrc)) + ((mdr_f_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscrc) + (mdr_f_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscrc))))))))) /\ (((exists ff_h_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscrb. ff_h_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscrb + S (mdr_z_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscr) = S ((S (mdr_i_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsc)) * mdr_c_maximal_prefixhigherminorminornonzeroevaluationdeterminant)) /\ exists ff_q_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscrb. mdr_b_maximal_prefixhigherminorminornonzeroevaluationdeterminant = ff_q_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscrb * S ((S (mdr_i_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsc)) * mdr_c_maximal_prefixhigherminorminornonzeroevaluationdeterminant) + (mdr_z_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscm_positive. (exists ff_gap_mdm_lt_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscm_positive_index_bound. ff_gap_mdm_lt_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscm_positive) = ((mdr_q_maximal_prefixhigherminorminornonzeroevaluationdeterminanths) * (mdr_q_maximal_prefixhigherminorminornonzeroevaluationdeterminanths))) -> exists ff_row_mdm_prefix_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscm_positive ff_column_mdm_prefix_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscm_positive ff_value_mdm_prefix_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscm_positive. (ff_index_mdm_prefix_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscm_positive = (mdr_q_maximal_prefixhigherminorminornonzeroevaluationdeterminanths) * ff_row_mdm_prefix_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscm_positive + ff_column_mdm_prefix_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscm_positive /\ ((exists ff_gap_mdm_lt_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscm_positive_column_bound. ff_gap_mdm_lt_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscm_positive) = (mdr_q_maximal_prefixhigherminorminornonzeroevaluationdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscm_positive_cell ff_column_mdm_cell_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscm_positive_cell = ff_row_mdm_prefix_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscm_positive_cell_row_after. ff_gap_mdm_le_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscm_positive)) /\ ff_row_mdm_cell_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscm_positive_cell = S ff_row_mdm_prefix_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscm_positive) = (mdr_j_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsc)) /\ ff_column_mdm_cell_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscm_positive_cell = ff_column_mdm_prefix_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscm_positive_cell_column_after. ff_gap_mdm_le_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscm_positive_cell_column_after + (mdr_j_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsc) = (ff_column_mdm_prefix_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscm_positive)) /\ ff_column_mdm_cell_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscm_positive_cell = S ff_column_mdm_prefix_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscm_positive))) /\ (((exists ff_h_mdm_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscm_positive_cell_source. ff_h_mdm_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscm_positive) = S ((S ((ff_row_mdm_cell_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscm_positive_cell) * (S (mdr_q_maximal_prefixhigherminorminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscm_positive_cell))) * mdr_pc_maximal_prefixhigherminorminornonzeroevaluationdeterminanth)) /\ exists ff_q_mdm_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscm_positive_cell_source. mdr_pb_maximal_prefixhigherminorminornonzeroevaluationdeterminanth = ff_q_mdm_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscm_positive_cell) * (S (mdr_q_maximal_prefixhigherminorminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscm_positive_cell))) * mdr_pc_maximal_prefixhigherminorminornonzeroevaluationdeterminanth) + (ff_value_mdm_prefix_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscm_positive)))))) /\ (((exists ff_h_mdm_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscm_positive_target. ff_h_mdm_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscm_positive_target + S (ff_value_mdm_prefix_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscm_positive) = S ((S (ff_index_mdm_prefix_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscm_positive)) * mdr_us_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsc)) /\ exists ff_q_mdm_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscm_positive_target. mdr_up_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsc = ff_q_mdm_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscm_positive)) * mdr_us_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsc) + (ff_value_mdm_prefix_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscm_negative. (exists ff_gap_mdm_lt_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscm_negative_index_bound. ff_gap_mdm_lt_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscm_negative) = ((mdr_q_maximal_prefixhigherminorminornonzeroevaluationdeterminanths) * (mdr_q_maximal_prefixhigherminorminornonzeroevaluationdeterminanths))) -> exists ff_row_mdm_prefix_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscm_negative ff_column_mdm_prefix_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscm_negative ff_value_mdm_prefix_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscm_negative. (ff_index_mdm_prefix_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscm_negative = (mdr_q_maximal_prefixhigherminorminornonzeroevaluationdeterminanths) * ff_row_mdm_prefix_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscm_negative + ff_column_mdm_prefix_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscm_negative /\ ((exists ff_gap_mdm_lt_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscm_negative_column_bound. ff_gap_mdm_lt_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscm_negative) = (mdr_q_maximal_prefixhigherminorminornonzeroevaluationdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscm_negative_cell ff_column_mdm_cell_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscm_negative_cell = ff_row_mdm_prefix_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscm_negative_cell_row_after. ff_gap_mdm_le_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscm_negative)) /\ ff_row_mdm_cell_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscm_negative_cell = S ff_row_mdm_prefix_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscm_negative) = (mdr_j_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsc)) /\ ff_column_mdm_cell_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscm_negative_cell = ff_column_mdm_prefix_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscm_negative_cell_column_after. ff_gap_mdm_le_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscm_negative_cell_column_after + (mdr_j_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsc) = (ff_column_mdm_prefix_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscm_negative)) /\ ff_column_mdm_cell_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscm_negative_cell = S ff_column_mdm_prefix_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscm_negative))) /\ (((exists ff_h_mdm_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscm_negative_cell_source. ff_h_mdm_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscm_negative) = S ((S ((ff_row_mdm_cell_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscm_negative_cell) * (S (mdr_q_maximal_prefixhigherminorminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscm_negative_cell))) * mdr_nc_maximal_prefixhigherminorminornonzeroevaluationdeterminanth)) /\ exists ff_q_mdm_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscm_negative_cell_source. mdr_nb_maximal_prefixhigherminorminornonzeroevaluationdeterminanth = ff_q_mdm_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscm_negative_cell) * (S (mdr_q_maximal_prefixhigherminorminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscm_negative_cell))) * mdr_nc_maximal_prefixhigherminorminornonzeroevaluationdeterminanth) + (ff_value_mdm_prefix_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscm_negative)))))) /\ (((exists ff_h_mdm_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscm_negative_target. ff_h_mdm_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscm_negative_target + S (ff_value_mdm_prefix_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscm_negative) = S ((S (ff_index_mdm_prefix_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscm_negative)) * mdr_ut_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsc)) /\ exists ff_q_mdm_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscm_negative_target. mdr_un_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsc = ff_q_mdm_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscm_negative)) * mdr_ut_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsc) + (ff_value_mdm_prefix_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscm_negative))))))))) /\ ((((exists ff_h_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscp. ff_h_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscp + S (mdr_p_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsc) = S ((S (mdr_j_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsc)) * mdr_ec_maximal_prefixhigherminorminornonzeroevaluationdeterminanths)) /\ exists ff_q_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscp. mdr_eb_maximal_prefixhigherminorminornonzeroevaluationdeterminanths = ff_q_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscp * S ((S (mdr_j_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsc)) * mdr_ec_maximal_prefixhigherminorminornonzeroevaluationdeterminanths) + (mdr_p_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsc))) /\ (((exists ff_h_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscn. ff_h_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscn + S (mdr_n_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsc) = S ((S (mdr_j_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsc)) * mdr_fc_maximal_prefixhigherminorminornonzeroevaluationdeterminanths)) /\ exists ff_q_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscn. mdr_fb_maximal_prefixhigherminorminornonzeroevaluationdeterminanths = ff_q_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthscn * S ((S (mdr_j_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsc)) * mdr_fc_maximal_prefixhigherminorminornonzeroevaluationdeterminanths) + (mdr_n_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsc)))))))) /\ (exists ff_ub_mce_fold_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf ff_uc_mce_fold_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf ff_vb_mce_fold_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf ff_vc_mce_fold_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf. ((forall ff_index_mce_alternating_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_prefix. (exists ff_gap_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_prefix_index. ff_gap_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_prefix_index + S (ff_index_mce_alternating_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_prefix) = (S (mdr_q_maximal_prefixhigherminorminornonzeroevaluationdeterminanths))) -> exists ff_ap_mce_alternating_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_prefix ff_an_mce_alternating_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_prefix ff_bp_mce_alternating_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_prefix ff_bn_mce_alternating_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_prefix ff_p_mce_alternating_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_prefix ff_n_mce_alternating_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_prefix. ((((exists ff_h_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_prefix_ap. ff_h_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_prefix_ap + S (ff_ap_mce_alternating_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_prefix)) * mdr_pc_maximal_prefixhigherminorminornonzeroevaluationdeterminanth)) /\ exists ff_q_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_prefix_ap. mdr_pb_maximal_prefixhigherminorminornonzeroevaluationdeterminanth = ff_q_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_prefix)) * mdr_pc_maximal_prefixhigherminorminornonzeroevaluationdeterminanth) + (ff_ap_mce_alternating_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_prefix_an. ff_h_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_prefix_an + S (ff_an_mce_alternating_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_prefix)) * mdr_nc_maximal_prefixhigherminorminornonzeroevaluationdeterminanth)) /\ exists ff_q_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_prefix_an. mdr_nb_maximal_prefixhigherminorminornonzeroevaluationdeterminanth = ff_q_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_prefix)) * mdr_nc_maximal_prefixhigherminorminornonzeroevaluationdeterminanth) + (ff_an_mce_alternating_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_prefix_bp. ff_h_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_prefix_bp + S (ff_bp_mce_alternating_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_prefix)) * mdr_ec_maximal_prefixhigherminorminornonzeroevaluationdeterminanths)) /\ exists ff_q_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_prefix_bp. mdr_eb_maximal_prefixhigherminorminornonzeroevaluationdeterminanths = ff_q_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_prefix)) * mdr_ec_maximal_prefixhigherminorminornonzeroevaluationdeterminanths) + (ff_bp_mce_alternating_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_prefix_bn. ff_h_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_prefix_bn + S (ff_bn_mce_alternating_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_prefix)) * mdr_fc_maximal_prefixhigherminorminornonzeroevaluationdeterminanths)) /\ exists ff_q_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_prefix_bn. mdr_fb_maximal_prefixhigherminorminornonzeroevaluationdeterminanths = ff_q_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_prefix)) * mdr_fc_maximal_prefixhigherminorminornonzeroevaluationdeterminanths) + (ff_bn_mce_alternating_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_prefix_positive. ff_h_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_prefix_positive + S (ff_p_mce_alternating_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_prefix_positive. ff_ub_mce_fold_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf) + (ff_p_mce_alternating_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_prefix_negative. ff_h_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_prefix_negative + S (ff_n_mce_alternating_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_prefix_negative. ff_vb_mce_fold_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf) + (ff_n_mce_alternating_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_prefix))) /\ (((exists ff_even_mce_term_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_prefix = 2 * ff_even_mce_term_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_prefix_term) /\ (ff_p_mce_alternating_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_prefix = 2 * ff_odd_mce_term_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_positive ff_v_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_positive. ((((exists ff_h_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_positive_start. ff_h_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_positive_start. ff_u_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_positive_start * S ((S (0)) * ff_v_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_positive_terminal. ff_h_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_positive_terminal + S (mdr_p_maximal_prefixhigherminorminornonzeroevaluationdeterminanth) = S ((S ((S (mdr_q_maximal_prefixhigherminorminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_positive_terminal. ff_u_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_positive_terminal * S ((S ((S (mdr_q_maximal_prefixhigherminorminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_positive) + (mdr_p_maximal_prefixhigherminorminornonzeroevaluationdeterminanth))) /\ forall ff_i_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_positive. (exists ff_lt_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_positive_bound. ff_lt_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_positive_bound + S ff_i_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_positive = (S (mdr_q_maximal_prefixhigherminorminornonzeroevaluationdeterminanths))) -> exists ff_a_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_positive ff_r_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_positive ff_s_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_positive. ((((exists ff_h_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_positive_summand. ff_h_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_positive_summand + S (ff_a_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_positive_summand. ff_ub_mce_fold_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_positive_summand * S ((S (ff_i_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf) + (ff_a_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_positive_partial. ff_h_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_positive_partial + S (ff_r_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_positive_partial. ff_u_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_positive_partial * S ((S (ff_i_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_positive) + (ff_r_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_positive_successor. ff_h_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_positive_successor + S (ff_s_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_positive) = S ((S (S ff_i_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_positive_successor. ff_u_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_positive_successor * S ((S (S ff_i_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_positive) + (ff_s_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_positive))) /\ ff_s_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_positive = ff_r_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_positive + ff_a_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_positive)))))) /\ (exists ff_u_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_negative ff_v_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_negative. ((((exists ff_h_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_negative_start. ff_h_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_negative_start. ff_u_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_negative_start * S ((S (0)) * ff_v_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_negative_terminal. ff_h_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_negative_terminal + S (mdr_n_maximal_prefixhigherminorminornonzeroevaluationdeterminanth) = S ((S ((S (mdr_q_maximal_prefixhigherminorminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_negative_terminal. ff_u_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_negative_terminal * S ((S ((S (mdr_q_maximal_prefixhigherminorminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_negative) + (mdr_n_maximal_prefixhigherminorminornonzeroevaluationdeterminanth))) /\ forall ff_i_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_negative. (exists ff_lt_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_negative_bound. ff_lt_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_negative_bound + S ff_i_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_negative = (S (mdr_q_maximal_prefixhigherminorminornonzeroevaluationdeterminanths))) -> exists ff_a_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_negative ff_r_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_negative ff_s_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_negative. ((((exists ff_h_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_negative_summand. ff_h_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_negative_summand + S (ff_a_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_negative_summand. ff_vb_mce_fold_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_negative_summand * S ((S (ff_i_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf) + (ff_a_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_negative_partial. ff_h_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_negative_partial + S (ff_r_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_negative_partial. ff_u_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_negative_partial * S ((S (ff_i_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_negative) + (ff_r_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_negative_successor. ff_h_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_negative_successor + S (ff_s_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_negative) = S ((S (S ff_i_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_negative_successor. ff_u_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_negative_successor * S ((S (S ff_i_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_negative) + (ff_s_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_negative))) /\ ff_s_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_negative = ff_r_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_negative + ff_a_mce_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminanthsf_negative))))))))))))))) /\ ((exists mdr_gap_maximal_prefixhigherminorminornonzeroevaluationdeterminanti. mdr_gap_maximal_prefixhigherminorminornonzeroevaluationdeterminanti + S (mdr_i_maximal_prefixhigherminorminornonzeroevaluationdeterminant) = (mdr_l_maximal_prefixhigherminorminornonzeroevaluationdeterminant)) /\ (exists mdr_z_maximal_prefixhigherminorminornonzeroevaluationdeterminantr. ((exists mdr_a_maximal_prefixhigherminorminornonzeroevaluationdeterminantrc mdr_b_maximal_prefixhigherminorminornonzeroevaluationdeterminantrc mdr_c_maximal_prefixhigherminorminornonzeroevaluationdeterminantrc mdr_e_maximal_prefixhigherminorminornonzeroevaluationdeterminantrc mdr_f_maximal_prefixhigherminorminornonzeroevaluationdeterminantrc. ((mdr_a_maximal_prefixhigherminorminornonzeroevaluationdeterminantrc = ((mdr_j_maximal_prefixhigher) + (mdr_ub_maximal_prefixhigherminorminornonzeroevaluation)) * S ((mdr_j_maximal_prefixhigher) + (mdr_ub_maximal_prefixhigherminorminornonzeroevaluation)) + ((mdr_ub_maximal_prefixhigherminorminornonzeroevaluation) + (mdr_ub_maximal_prefixhigherminorminornonzeroevaluation))) /\ ((mdr_b_maximal_prefixhigherminorminornonzeroevaluationdeterminantrc = ((mdr_uc_maximal_prefixhigherminorminornonzeroevaluation) + (mdr_vb_maximal_prefixhigherminorminornonzeroevaluation)) * S ((mdr_uc_maximal_prefixhigherminorminornonzeroevaluation) + (mdr_vb_maximal_prefixhigherminorminornonzeroevaluation)) + ((mdr_vb_maximal_prefixhigherminorminornonzeroevaluation) + (mdr_vb_maximal_prefixhigherminorminornonzeroevaluation))) /\ ((mdr_c_maximal_prefixhigherminorminornonzeroevaluationdeterminantrc = ((mdr_a_maximal_prefixhigherminorminornonzeroevaluationdeterminantrc) + (mdr_b_maximal_prefixhigherminorminornonzeroevaluationdeterminantrc)) * S ((mdr_a_maximal_prefixhigherminorminornonzeroevaluationdeterminantrc) + (mdr_b_maximal_prefixhigherminorminornonzeroevaluationdeterminantrc)) + ((mdr_b_maximal_prefixhigherminorminornonzeroevaluationdeterminantrc) + (mdr_b_maximal_prefixhigherminorminornonzeroevaluationdeterminantrc))) /\ ((mdr_e_maximal_prefixhigherminorminornonzeroevaluationdeterminantrc = ((mdr_p_maximal_prefixhigherminorminornonzero) + (mdr_n_maximal_prefixhigherminorminornonzero)) * S ((mdr_p_maximal_prefixhigherminorminornonzero) + (mdr_n_maximal_prefixhigherminorminornonzero)) + ((mdr_n_maximal_prefixhigherminorminornonzero) + (mdr_n_maximal_prefixhigherminorminornonzero))) /\ ((mdr_f_maximal_prefixhigherminorminornonzeroevaluationdeterminantrc = ((mdr_vc_maximal_prefixhigherminorminornonzeroevaluation) + (mdr_e_maximal_prefixhigherminorminornonzeroevaluationdeterminantrc)) * S ((mdr_vc_maximal_prefixhigherminorminornonzeroevaluation) + (mdr_e_maximal_prefixhigherminorminornonzeroevaluationdeterminantrc)) + ((mdr_e_maximal_prefixhigherminorminornonzeroevaluationdeterminantrc) + (mdr_e_maximal_prefixhigherminorminornonzeroevaluationdeterminantrc))) /\ ((mdr_z_maximal_prefixhigherminorminornonzeroevaluationdeterminantr) = ((mdr_c_maximal_prefixhigherminorminornonzeroevaluationdeterminantrc) + (mdr_f_maximal_prefixhigherminorminornonzeroevaluationdeterminantrc)) * S ((mdr_c_maximal_prefixhigherminorminornonzeroevaluationdeterminantrc) + (mdr_f_maximal_prefixhigherminorminornonzeroevaluationdeterminantrc)) + ((mdr_f_maximal_prefixhigherminorminornonzeroevaluationdeterminantrc) + (mdr_f_maximal_prefixhigherminorminornonzeroevaluationdeterminantrc))))))))) /\ (((exists ff_h_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminantrb. ff_h_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminantrb + S (mdr_z_maximal_prefixhigherminorminornonzeroevaluationdeterminantr) = S ((S (mdr_i_maximal_prefixhigherminorminornonzeroevaluationdeterminant)) * mdr_c_maximal_prefixhigherminorminornonzeroevaluationdeterminant)) /\ exists ff_q_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminantrb. mdr_b_maximal_prefixhigherminorminornonzeroevaluationdeterminant = ff_q_mdr_maximal_prefixhigherminorminornonzeroevaluationdeterminantrb * S ((S (mdr_i_maximal_prefixhigherminorminornonzeroevaluationdeterminant)) * mdr_c_maximal_prefixhigherminorminornonzeroevaluationdeterminant) + (mdr_z_maximal_prefixhigherminorminornonzeroevaluationdeterminantr)))))))))) /\ (~(mdr_p_maximal_prefixhigherminorminornonzero = mdr_n_maximal_prefixhigherminorminornonzero))))))))))))