matrix_integer_nonzero_minor_transport

forall ab ac bb bc eb ec fb fc r w q. (forall ics_index_minor_parent_equality ics_value0_minor_parent_equality ics_value1_minor_parent_equality ics_value2_minor_parent_equality ics_value3_minor_parent_equality. (exists ics_gap_minor_parent_equality_bound. ics_gap_minor_parent_equality_bound + S (ics_index_minor_parent_equality) = ((r) * (w))) -> (((exists fs_h_ics_minor_parent_equality_at0. fs_h_ics_minor_parent_equality_at0 + S (ics_value0_minor_parent_equality) = S ((S (ics_index_minor_parent_equality)) * ac)) /\ exists fs_q_ics_minor_parent_equality_at0. ab = fs_q_ics_minor_parent_equality_at0 * S ((S (ics_index_minor_parent_equality)) * ac) + (ics_value0_minor_parent_equality))) -> (((exists fs_h_ics_minor_parent_equality_at1. fs_h_ics_minor_parent_equality_at1 + S (ics_value1_minor_parent_equality) = S ((S (ics_index_minor_parent_equality)) * bc)) /\ exists fs_q_ics_minor_parent_equality_at1. bb = fs_q_ics_minor_parent_equality_at1 * S ((S (ics_index_minor_parent_equality)) * bc) + (ics_value1_minor_parent_equality))) -> (((exists fs_h_ics_minor_parent_equality_at2. fs_h_ics_minor_parent_equality_at2 + S (ics_value2_minor_parent_equality) = S ((S (ics_index_minor_parent_equality)) * ec)) /\ exists fs_q_ics_minor_parent_equality_at2. eb = fs_q_ics_minor_parent_equality_at2 * S ((S (ics_index_minor_parent_equality)) * ec) + (ics_value2_minor_parent_equality))) -> (((exists fs_h_ics_minor_parent_equality_at3. fs_h_ics_minor_parent_equality_at3 + S (ics_value3_minor_parent_equality) = S ((S (ics_index_minor_parent_equality)) * fc)) /\ exists fs_q_ics_minor_parent_equality_at3. fb = fs_q_ics_minor_parent_equality_at3 * S ((S (ics_index_minor_parent_equality)) * fc) + (ics_value3_minor_parent_equality))) -> ics_value0_minor_parent_equality + ics_value3_minor_parent_equality = ics_value2_minor_parent_equality + ics_value1_minor_parent_equality) -> (exists mdr_rb_first_nonzero_minor mdr_rc_first_nonzero_minor mdr_cb_first_nonzero_minor mdr_cc_first_nonzero_minor. (((((forall fom_index_mrf_first_nonzero_minorminorrowsbound. (exists fom_gap_mrf_first_nonzero_minorminorrowsbound_index_bound. fom_gap_mrf_first_nonzero_minorminorrowsbound_index_bound + S (fom_index_mrf_first_nonzero_minorminorrowsbound) = q) -> exists fom_value_mrf_first_nonzero_minorminorrowsbound. ((((exists fom_beta_height_mrf_first_nonzero_minorminorrowsbound_entry. fom_beta_height_mrf_first_nonzero_minorminorrowsbound_entry + S (fom_value_mrf_first_nonzero_minorminorrowsbound) = S ((S (fom_index_mrf_first_nonzero_minorminorrowsbound)) * mdr_rc_first_nonzero_minor)) /\ exists fom_beta_quotient_mrf_first_nonzero_minorminorrowsbound_entry. mdr_rb_first_nonzero_minor = fom_beta_quotient_mrf_first_nonzero_minorminorrowsbound_entry * S ((S (fom_index_mrf_first_nonzero_minorminorrowsbound)) * mdr_rc_first_nonzero_minor) + (fom_value_mrf_first_nonzero_minorminorrowsbound))) /\ (exists fom_gap_mrf_first_nonzero_minorminorrowsbound_value_bound. fom_gap_mrf_first_nonzero_minorminorrowsbound_value_bound + S (fom_value_mrf_first_nonzero_minorminorrowsbound) = r))) /\ (forall mdr_i_first_nonzero_minorminorrowsdistinct mdr_j_first_nonzero_minorminorrowsdistinct mdr_a_first_nonzero_minorminorrowsdistinct. (exists mdr_gap_first_nonzero_minorminorrowsdistincti. mdr_gap_first_nonzero_minorminorrowsdistincti + S (mdr_i_first_nonzero_minorminorrowsdistinct) = (q)) -> (exists mdr_gap_first_nonzero_minorminorrowsdistinctj. mdr_gap_first_nonzero_minorminorrowsdistinctj + S (mdr_j_first_nonzero_minorminorrowsdistinct) = (q)) -> (((exists ff_h_mdr_first_nonzero_minorminorrowsdistinctfirst. ff_h_mdr_first_nonzero_minorminorrowsdistinctfirst + S (mdr_a_first_nonzero_minorminorrowsdistinct) = S ((S (mdr_i_first_nonzero_minorminorrowsdistinct)) * mdr_rc_first_nonzero_minor)) /\ exists ff_q_mdr_first_nonzero_minorminorrowsdistinctfirst. mdr_rb_first_nonzero_minor = ff_q_mdr_first_nonzero_minorminorrowsdistinctfirst * S ((S (mdr_i_first_nonzero_minorminorrowsdistinct)) * mdr_rc_first_nonzero_minor) + (mdr_a_first_nonzero_minorminorrowsdistinct))) -> (((exists ff_h_mdr_first_nonzero_minorminorrowsdistinctsecond. ff_h_mdr_first_nonzero_minorminorrowsdistinctsecond + S (mdr_a_first_nonzero_minorminorrowsdistinct) = S ((S (mdr_j_first_nonzero_minorminorrowsdistinct)) * mdr_rc_first_nonzero_minor)) /\ exists ff_q_mdr_first_nonzero_minorminorrowsdistinctsecond. mdr_rb_first_nonzero_minor = ff_q_mdr_first_nonzero_minorminorrowsdistinctsecond * S ((S (mdr_j_first_nonzero_minorminorrowsdistinct)) * mdr_rc_first_nonzero_minor) + (mdr_a_first_nonzero_minorminorrowsdistinct))) -> mdr_i_first_nonzero_minorminorrowsdistinct = mdr_j_first_nonzero_minorminorrowsdistinct))) /\ ((((forall fom_index_mrf_first_nonzero_minorminorcolumnsbound. (exists fom_gap_mrf_first_nonzero_minorminorcolumnsbound_index_bound. fom_gap_mrf_first_nonzero_minorminorcolumnsbound_index_bound + S (fom_index_mrf_first_nonzero_minorminorcolumnsbound) = q) -> exists fom_value_mrf_first_nonzero_minorminorcolumnsbound. ((((exists fom_beta_height_mrf_first_nonzero_minorminorcolumnsbound_entry. fom_beta_height_mrf_first_nonzero_minorminorcolumnsbound_entry + S (fom_value_mrf_first_nonzero_minorminorcolumnsbound) = S ((S (fom_index_mrf_first_nonzero_minorminorcolumnsbound)) * mdr_cc_first_nonzero_minor)) /\ exists fom_beta_quotient_mrf_first_nonzero_minorminorcolumnsbound_entry. mdr_cb_first_nonzero_minor = fom_beta_quotient_mrf_first_nonzero_minorminorcolumnsbound_entry * S ((S (fom_index_mrf_first_nonzero_minorminorcolumnsbound)) * mdr_cc_first_nonzero_minor) + (fom_value_mrf_first_nonzero_minorminorcolumnsbound))) /\ (exists fom_gap_mrf_first_nonzero_minorminorcolumnsbound_value_bound. fom_gap_mrf_first_nonzero_minorminorcolumnsbound_value_bound + S (fom_value_mrf_first_nonzero_minorminorcolumnsbound) = w))) /\ (forall mdr_i_first_nonzero_minorminorcolumnsdistinct mdr_j_first_nonzero_minorminorcolumnsdistinct mdr_a_first_nonzero_minorminorcolumnsdistinct. (exists mdr_gap_first_nonzero_minorminorcolumnsdistincti. mdr_gap_first_nonzero_minorminorcolumnsdistincti + S (mdr_i_first_nonzero_minorminorcolumnsdistinct) = (q)) -> (exists mdr_gap_first_nonzero_minorminorcolumnsdistinctj. mdr_gap_first_nonzero_minorminorcolumnsdistinctj + S (mdr_j_first_nonzero_minorminorcolumnsdistinct) = (q)) -> (((exists ff_h_mdr_first_nonzero_minorminorcolumnsdistinctfirst. ff_h_mdr_first_nonzero_minorminorcolumnsdistinctfirst + S (mdr_a_first_nonzero_minorminorcolumnsdistinct) = S ((S (mdr_i_first_nonzero_minorminorcolumnsdistinct)) * mdr_cc_first_nonzero_minor)) /\ exists ff_q_mdr_first_nonzero_minorminorcolumnsdistinctfirst. mdr_cb_first_nonzero_minor = ff_q_mdr_first_nonzero_minorminorcolumnsdistinctfirst * S ((S (mdr_i_first_nonzero_minorminorcolumnsdistinct)) * mdr_cc_first_nonzero_minor) + (mdr_a_first_nonzero_minorminorcolumnsdistinct))) -> (((exists ff_h_mdr_first_nonzero_minorminorcolumnsdistinctsecond. ff_h_mdr_first_nonzero_minorminorcolumnsdistinctsecond + S (mdr_a_first_nonzero_minorminorcolumnsdistinct) = S ((S (mdr_j_first_nonzero_minorminorcolumnsdistinct)) * mdr_cc_first_nonzero_minor)) /\ exists ff_q_mdr_first_nonzero_minorminorcolumnsdistinctsecond. mdr_cb_first_nonzero_minor = ff_q_mdr_first_nonzero_minorminorcolumnsdistinctsecond * S ((S (mdr_j_first_nonzero_minorminorcolumnsdistinct)) * mdr_cc_first_nonzero_minor) + (mdr_a_first_nonzero_minorminorcolumnsdistinct))) -> mdr_i_first_nonzero_minorminorcolumnsdistinct = mdr_j_first_nonzero_minorminorcolumnsdistinct))) /\ (exists mdr_p_first_nonzero_minorminornonzero mdr_n_first_nonzero_minorminornonzero. ((exists mdr_ub_first_nonzero_minorminornonzeroevaluation mdr_uc_first_nonzero_minorminornonzeroevaluation mdr_vb_first_nonzero_minorminornonzeroevaluation mdr_vc_first_nonzero_minorminornonzeroevaluation. ((((forall mdr_i_first_nonzero_minorminornonzeroevaluationmatrixpositive. (exists mdr_gap_first_nonzero_minorminornonzeroevaluationmatrixpositivebound. mdr_gap_first_nonzero_minorminornonzeroevaluationmatrixpositivebound + S (mdr_i_first_nonzero_minorminornonzeroevaluationmatrixpositive) = ((q) * (q))) -> exists mdr_a_first_nonzero_minorminornonzeroevaluationmatrixpositive. (((exists mdr_r_first_nonzero_minorminornonzeroevaluationmatrixpositivepoint mdr_s_first_nonzero_minorminornonzeroevaluationmatrixpositivepoint mdr_u_first_nonzero_minorminornonzeroevaluationmatrixpositivepoint mdr_v_first_nonzero_minorminornonzeroevaluationmatrixpositivepoint. ((mdr_i_first_nonzero_minorminornonzeroevaluationmatrixpositive = (q) * mdr_r_first_nonzero_minorminornonzeroevaluationmatrixpositivepoint + mdr_s_first_nonzero_minorminornonzeroevaluationmatrixpositivepoint) /\ ((exists mdr_gap_first_nonzero_minorminornonzeroevaluationmatrixpositivepointcolumn. mdr_gap_first_nonzero_minorminornonzeroevaluationmatrixpositivepointcolumn + S (mdr_s_first_nonzero_minorminornonzeroevaluationmatrixpositivepoint) = (q)) /\ ((((exists ff_h_mdr_first_nonzero_minorminornonzeroevaluationmatrixpositivepointrow_index. ff_h_mdr_first_nonzero_minorminornonzeroevaluationmatrixpositivepointrow_index + S (mdr_u_first_nonzero_minorminornonzeroevaluationmatrixpositivepoint) = S ((S (mdr_r_first_nonzero_minorminornonzeroevaluationmatrixpositivepoint)) * mdr_rc_first_nonzero_minor)) /\ exists ff_q_mdr_first_nonzero_minorminornonzeroevaluationmatrixpositivepointrow_index. mdr_rb_first_nonzero_minor = ff_q_mdr_first_nonzero_minorminornonzeroevaluationmatrixpositivepointrow_index * S ((S (mdr_r_first_nonzero_minorminornonzeroevaluationmatrixpositivepoint)) * mdr_rc_first_nonzero_minor) + (mdr_u_first_nonzero_minorminornonzeroevaluationmatrixpositivepoint))) /\ ((((exists ff_h_mdr_first_nonzero_minorminornonzeroevaluationmatrixpositivepointcolumn_index. ff_h_mdr_first_nonzero_minorminornonzeroevaluationmatrixpositivepointcolumn_index + S (mdr_v_first_nonzero_minorminornonzeroevaluationmatrixpositivepoint) = S ((S (mdr_s_first_nonzero_minorminornonzeroevaluationmatrixpositivepoint)) * mdr_cc_first_nonzero_minor)) /\ exists ff_q_mdr_first_nonzero_minorminornonzeroevaluationmatrixpositivepointcolumn_index. mdr_cb_first_nonzero_minor = ff_q_mdr_first_nonzero_minorminornonzeroevaluationmatrixpositivepointcolumn_index * S ((S (mdr_s_first_nonzero_minorminornonzeroevaluationmatrixpositivepoint)) * mdr_cc_first_nonzero_minor) + (mdr_v_first_nonzero_minorminornonzeroevaluationmatrixpositivepoint))) /\ (((exists ff_h_mdr_first_nonzero_minorminornonzeroevaluationmatrixpositivepointsource. ff_h_mdr_first_nonzero_minorminornonzeroevaluationmatrixpositivepointsource + S (mdr_a_first_nonzero_minorminornonzeroevaluationmatrixpositive) = S ((S ((mdr_u_first_nonzero_minorminornonzeroevaluationmatrixpositivepoint) * (w) + (mdr_v_first_nonzero_minorminornonzeroevaluationmatrixpositivepoint))) * ac)) /\ exists ff_q_mdr_first_nonzero_minorminornonzeroevaluationmatrixpositivepointsource. ab = ff_q_mdr_first_nonzero_minorminornonzeroevaluationmatrixpositivepointsource * S ((S ((mdr_u_first_nonzero_minorminornonzeroevaluationmatrixpositivepoint) * (w) + (mdr_v_first_nonzero_minorminornonzeroevaluationmatrixpositivepoint))) * ac) + (mdr_a_first_nonzero_minorminornonzeroevaluationmatrixpositive)))))))) /\ (((exists ff_h_mdr_first_nonzero_minorminornonzeroevaluationmatrixpositiveoutput. ff_h_mdr_first_nonzero_minorminornonzeroevaluationmatrixpositiveoutput + S (mdr_a_first_nonzero_minorminornonzeroevaluationmatrixpositive) = S ((S (mdr_i_first_nonzero_minorminornonzeroevaluationmatrixpositive)) * mdr_uc_first_nonzero_minorminornonzeroevaluation)) /\ exists ff_q_mdr_first_nonzero_minorminornonzeroevaluationmatrixpositiveoutput. mdr_ub_first_nonzero_minorminornonzeroevaluation = ff_q_mdr_first_nonzero_minorminornonzeroevaluationmatrixpositiveoutput * S ((S (mdr_i_first_nonzero_minorminornonzeroevaluationmatrixpositive)) * mdr_uc_first_nonzero_minorminornonzeroevaluation) + (mdr_a_first_nonzero_minorminornonzeroevaluationmatrixpositive)))))) /\ (forall mdr_i_first_nonzero_minorminornonzeroevaluationmatrixnegative. (exists mdr_gap_first_nonzero_minorminornonzeroevaluationmatrixnegativebound. mdr_gap_first_nonzero_minorminornonzeroevaluationmatrixnegativebound + S (mdr_i_first_nonzero_minorminornonzeroevaluationmatrixnegative) = ((q) * (q))) -> exists mdr_a_first_nonzero_minorminornonzeroevaluationmatrixnegative. (((exists mdr_r_first_nonzero_minorminornonzeroevaluationmatrixnegativepoint mdr_s_first_nonzero_minorminornonzeroevaluationmatrixnegativepoint mdr_u_first_nonzero_minorminornonzeroevaluationmatrixnegativepoint mdr_v_first_nonzero_minorminornonzeroevaluationmatrixnegativepoint. ((mdr_i_first_nonzero_minorminornonzeroevaluationmatrixnegative = (q) * mdr_r_first_nonzero_minorminornonzeroevaluationmatrixnegativepoint + mdr_s_first_nonzero_minorminornonzeroevaluationmatrixnegativepoint) /\ ((exists mdr_gap_first_nonzero_minorminornonzeroevaluationmatrixnegativepointcolumn. mdr_gap_first_nonzero_minorminornonzeroevaluationmatrixnegativepointcolumn + S (mdr_s_first_nonzero_minorminornonzeroevaluationmatrixnegativepoint) = (q)) /\ ((((exists ff_h_mdr_first_nonzero_minorminornonzeroevaluationmatrixnegativepointrow_index. ff_h_mdr_first_nonzero_minorminornonzeroevaluationmatrixnegativepointrow_index + S (mdr_u_first_nonzero_minorminornonzeroevaluationmatrixnegativepoint) = S ((S (mdr_r_first_nonzero_minorminornonzeroevaluationmatrixnegativepoint)) * mdr_rc_first_nonzero_minor)) /\ exists ff_q_mdr_first_nonzero_minorminornonzeroevaluationmatrixnegativepointrow_index. mdr_rb_first_nonzero_minor = ff_q_mdr_first_nonzero_minorminornonzeroevaluationmatrixnegativepointrow_index * S ((S (mdr_r_first_nonzero_minorminornonzeroevaluationmatrixnegativepoint)) * mdr_rc_first_nonzero_minor) + (mdr_u_first_nonzero_minorminornonzeroevaluationmatrixnegativepoint))) /\ ((((exists ff_h_mdr_first_nonzero_minorminornonzeroevaluationmatrixnegativepointcolumn_index. ff_h_mdr_first_nonzero_minorminornonzeroevaluationmatrixnegativepointcolumn_index + S (mdr_v_first_nonzero_minorminornonzeroevaluationmatrixnegativepoint) = S ((S (mdr_s_first_nonzero_minorminornonzeroevaluationmatrixnegativepoint)) * mdr_cc_first_nonzero_minor)) /\ exists ff_q_mdr_first_nonzero_minorminornonzeroevaluationmatrixnegativepointcolumn_index. mdr_cb_first_nonzero_minor = ff_q_mdr_first_nonzero_minorminornonzeroevaluationmatrixnegativepointcolumn_index * S ((S (mdr_s_first_nonzero_minorminornonzeroevaluationmatrixnegativepoint)) * mdr_cc_first_nonzero_minor) + (mdr_v_first_nonzero_minorminornonzeroevaluationmatrixnegativepoint))) /\ (((exists ff_h_mdr_first_nonzero_minorminornonzeroevaluationmatrixnegativepointsource. ff_h_mdr_first_nonzero_minorminornonzeroevaluationmatrixnegativepointsource + S (mdr_a_first_nonzero_minorminornonzeroevaluationmatrixnegative) = S ((S ((mdr_u_first_nonzero_minorminornonzeroevaluationmatrixnegativepoint) * (w) + (mdr_v_first_nonzero_minorminornonzeroevaluationmatrixnegativepoint))) * bc)) /\ exists ff_q_mdr_first_nonzero_minorminornonzeroevaluationmatrixnegativepointsource. bb = ff_q_mdr_first_nonzero_minorminornonzeroevaluationmatrixnegativepointsource * S ((S ((mdr_u_first_nonzero_minorminornonzeroevaluationmatrixnegativepoint) * (w) + (mdr_v_first_nonzero_minorminornonzeroevaluationmatrixnegativepoint))) * bc) + (mdr_a_first_nonzero_minorminornonzeroevaluationmatrixnegative)))))))) /\ (((exists ff_h_mdr_first_nonzero_minorminornonzeroevaluationmatrixnegativeoutput. ff_h_mdr_first_nonzero_minorminornonzeroevaluationmatrixnegativeoutput + S (mdr_a_first_nonzero_minorminornonzeroevaluationmatrixnegative) = S ((S (mdr_i_first_nonzero_minorminornonzeroevaluationmatrixnegative)) * mdr_vc_first_nonzero_minorminornonzeroevaluation)) /\ exists ff_q_mdr_first_nonzero_minorminornonzeroevaluationmatrixnegativeoutput. mdr_vb_first_nonzero_minorminornonzeroevaluation = ff_q_mdr_first_nonzero_minorminornonzeroevaluationmatrixnegativeoutput * S ((S (mdr_i_first_nonzero_minorminornonzeroevaluationmatrixnegative)) * mdr_vc_first_nonzero_minorminornonzeroevaluation) + (mdr_a_first_nonzero_minorminornonzeroevaluationmatrixnegative)))))))) /\ (exists mdr_b_first_nonzero_minorminornonzeroevaluationdeterminant mdr_c_first_nonzero_minorminornonzeroevaluationdeterminant mdr_l_first_nonzero_minorminornonzeroevaluationdeterminant mdr_i_first_nonzero_minorminornonzeroevaluationdeterminant. ((forall mdr_i_first_nonzero_minorminornonzeroevaluationdeterminanth. (exists mdr_gap_first_nonzero_minorminornonzeroevaluationdeterminanthi. mdr_gap_first_nonzero_minorminornonzeroevaluationdeterminanthi + S (mdr_i_first_nonzero_minorminornonzeroevaluationdeterminanth) = (mdr_l_first_nonzero_minorminornonzeroevaluationdeterminant)) -> exists mdr_d_first_nonzero_minorminornonzeroevaluationdeterminanth mdr_pb_first_nonzero_minorminornonzeroevaluationdeterminanth mdr_pc_first_nonzero_minorminornonzeroevaluationdeterminanth mdr_nb_first_nonzero_minorminornonzeroevaluationdeterminanth mdr_nc_first_nonzero_minorminornonzeroevaluationdeterminanth mdr_p_first_nonzero_minorminornonzeroevaluationdeterminanth mdr_n_first_nonzero_minorminornonzeroevaluationdeterminanth. ((exists mdr_z_first_nonzero_minorminornonzeroevaluationdeterminanthr. ((exists mdr_a_first_nonzero_minorminornonzeroevaluationdeterminanthrc mdr_b_first_nonzero_minorminornonzeroevaluationdeterminanthrc mdr_c_first_nonzero_minorminornonzeroevaluationdeterminanthrc mdr_e_first_nonzero_minorminornonzeroevaluationdeterminanthrc mdr_f_first_nonzero_minorminornonzeroevaluationdeterminanthrc. ((mdr_a_first_nonzero_minorminornonzeroevaluationdeterminanthrc = ((mdr_d_first_nonzero_minorminornonzeroevaluationdeterminanth) + (mdr_pb_first_nonzero_minorminornonzeroevaluationdeterminanth)) * S ((mdr_d_first_nonzero_minorminornonzeroevaluationdeterminanth) + (mdr_pb_first_nonzero_minorminornonzeroevaluationdeterminanth)) + ((mdr_pb_first_nonzero_minorminornonzeroevaluationdeterminanth) + (mdr_pb_first_nonzero_minorminornonzeroevaluationdeterminanth))) /\ ((mdr_b_first_nonzero_minorminornonzeroevaluationdeterminanthrc = ((mdr_pc_first_nonzero_minorminornonzeroevaluationdeterminanth) + (mdr_nb_first_nonzero_minorminornonzeroevaluationdeterminanth)) * S ((mdr_pc_first_nonzero_minorminornonzeroevaluationdeterminanth) + (mdr_nb_first_nonzero_minorminornonzeroevaluationdeterminanth)) + ((mdr_nb_first_nonzero_minorminornonzeroevaluationdeterminanth) + (mdr_nb_first_nonzero_minorminornonzeroevaluationdeterminanth))) /\ ((mdr_c_first_nonzero_minorminornonzeroevaluationdeterminanthrc = ((mdr_a_first_nonzero_minorminornonzeroevaluationdeterminanthrc) + (mdr_b_first_nonzero_minorminornonzeroevaluationdeterminanthrc)) * S ((mdr_a_first_nonzero_minorminornonzeroevaluationdeterminanthrc) + (mdr_b_first_nonzero_minorminornonzeroevaluationdeterminanthrc)) + ((mdr_b_first_nonzero_minorminornonzeroevaluationdeterminanthrc) + (mdr_b_first_nonzero_minorminornonzeroevaluationdeterminanthrc))) /\ ((mdr_e_first_nonzero_minorminornonzeroevaluationdeterminanthrc = ((mdr_p_first_nonzero_minorminornonzeroevaluationdeterminanth) + (mdr_n_first_nonzero_minorminornonzeroevaluationdeterminanth)) * S ((mdr_p_first_nonzero_minorminornonzeroevaluationdeterminanth) + (mdr_n_first_nonzero_minorminornonzeroevaluationdeterminanth)) + ((mdr_n_first_nonzero_minorminornonzeroevaluationdeterminanth) + (mdr_n_first_nonzero_minorminornonzeroevaluationdeterminanth))) /\ ((mdr_f_first_nonzero_minorminornonzeroevaluationdeterminanthrc = ((mdr_nc_first_nonzero_minorminornonzeroevaluationdeterminanth) + (mdr_e_first_nonzero_minorminornonzeroevaluationdeterminanthrc)) * S ((mdr_nc_first_nonzero_minorminornonzeroevaluationdeterminanth) + (mdr_e_first_nonzero_minorminornonzeroevaluationdeterminanthrc)) + ((mdr_e_first_nonzero_minorminornonzeroevaluationdeterminanthrc) + (mdr_e_first_nonzero_minorminornonzeroevaluationdeterminanthrc))) /\ ((mdr_z_first_nonzero_minorminornonzeroevaluationdeterminanthr) = ((mdr_c_first_nonzero_minorminornonzeroevaluationdeterminanthrc) + (mdr_f_first_nonzero_minorminornonzeroevaluationdeterminanthrc)) * S ((mdr_c_first_nonzero_minorminornonzeroevaluationdeterminanthrc) + (mdr_f_first_nonzero_minorminornonzeroevaluationdeterminanthrc)) + ((mdr_f_first_nonzero_minorminornonzeroevaluationdeterminanthrc) + (mdr_f_first_nonzero_minorminornonzeroevaluationdeterminanthrc))))))))) /\ (((exists ff_h_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthrb. ff_h_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthrb + S (mdr_z_first_nonzero_minorminornonzeroevaluationdeterminanthr) = S ((S (mdr_i_first_nonzero_minorminornonzeroevaluationdeterminanth)) * mdr_c_first_nonzero_minorminornonzeroevaluationdeterminant)) /\ exists ff_q_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthrb. mdr_b_first_nonzero_minorminornonzeroevaluationdeterminant = ff_q_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthrb * S ((S (mdr_i_first_nonzero_minorminornonzeroevaluationdeterminanth)) * mdr_c_first_nonzero_minorminornonzeroevaluationdeterminant) + (mdr_z_first_nonzero_minorminornonzeroevaluationdeterminanthr))))) /\ (((((mdr_d_first_nonzero_minorminornonzeroevaluationdeterminanth) = 0) /\ (((mdr_p_first_nonzero_minorminornonzeroevaluationdeterminanth) = 1) /\ ((mdr_n_first_nonzero_minorminornonzeroevaluationdeterminanth) = 0))) \/ exists mdr_q_first_nonzero_minorminornonzeroevaluationdeterminanths mdr_eb_first_nonzero_minorminornonzeroevaluationdeterminanths mdr_ec_first_nonzero_minorminornonzeroevaluationdeterminanths mdr_fb_first_nonzero_minorminornonzeroevaluationdeterminanths mdr_fc_first_nonzero_minorminornonzeroevaluationdeterminanths. (((mdr_d_first_nonzero_minorminornonzeroevaluationdeterminanth) = S (mdr_q_first_nonzero_minorminornonzeroevaluationdeterminanths)) /\ ((forall mdr_j_first_nonzero_minorminornonzeroevaluationdeterminanthsc. (exists mdr_gap_first_nonzero_minorminornonzeroevaluationdeterminanthscj. mdr_gap_first_nonzero_minorminornonzeroevaluationdeterminanthscj + S (mdr_j_first_nonzero_minorminornonzeroevaluationdeterminanthsc) = (S (mdr_q_first_nonzero_minorminornonzeroevaluationdeterminanths))) -> exists mdr_i_first_nonzero_minorminornonzeroevaluationdeterminanthsc mdr_up_first_nonzero_minorminornonzeroevaluationdeterminanthsc mdr_us_first_nonzero_minorminornonzeroevaluationdeterminanthsc mdr_un_first_nonzero_minorminornonzeroevaluationdeterminanthsc mdr_ut_first_nonzero_minorminornonzeroevaluationdeterminanthsc mdr_p_first_nonzero_minorminornonzeroevaluationdeterminanthsc mdr_n_first_nonzero_minorminornonzeroevaluationdeterminanthsc. ((exists mdr_gap_first_nonzero_minorminornonzeroevaluationdeterminanthsci. mdr_gap_first_nonzero_minorminornonzeroevaluationdeterminanthsci + S (mdr_i_first_nonzero_minorminornonzeroevaluationdeterminanthsc) = (mdr_i_first_nonzero_minorminornonzeroevaluationdeterminanth)) /\ ((exists mdr_z_first_nonzero_minorminornonzeroevaluationdeterminanthscr. ((exists mdr_a_first_nonzero_minorminornonzeroevaluationdeterminanthscrc mdr_b_first_nonzero_minorminornonzeroevaluationdeterminanthscrc mdr_c_first_nonzero_minorminornonzeroevaluationdeterminanthscrc mdr_e_first_nonzero_minorminornonzeroevaluationdeterminanthscrc mdr_f_first_nonzero_minorminornonzeroevaluationdeterminanthscrc. ((mdr_a_first_nonzero_minorminornonzeroevaluationdeterminanthscrc = ((mdr_q_first_nonzero_minorminornonzeroevaluationdeterminanths) + (mdr_up_first_nonzero_minorminornonzeroevaluationdeterminanthsc)) * S ((mdr_q_first_nonzero_minorminornonzeroevaluationdeterminanths) + (mdr_up_first_nonzero_minorminornonzeroevaluationdeterminanthsc)) + ((mdr_up_first_nonzero_minorminornonzeroevaluationdeterminanthsc) + (mdr_up_first_nonzero_minorminornonzeroevaluationdeterminanthsc))) /\ ((mdr_b_first_nonzero_minorminornonzeroevaluationdeterminanthscrc = ((mdr_us_first_nonzero_minorminornonzeroevaluationdeterminanthsc) + (mdr_un_first_nonzero_minorminornonzeroevaluationdeterminanthsc)) * S ((mdr_us_first_nonzero_minorminornonzeroevaluationdeterminanthsc) + (mdr_un_first_nonzero_minorminornonzeroevaluationdeterminanthsc)) + ((mdr_un_first_nonzero_minorminornonzeroevaluationdeterminanthsc) + (mdr_un_first_nonzero_minorminornonzeroevaluationdeterminanthsc))) /\ ((mdr_c_first_nonzero_minorminornonzeroevaluationdeterminanthscrc = ((mdr_a_first_nonzero_minorminornonzeroevaluationdeterminanthscrc) + (mdr_b_first_nonzero_minorminornonzeroevaluationdeterminanthscrc)) * S ((mdr_a_first_nonzero_minorminornonzeroevaluationdeterminanthscrc) + (mdr_b_first_nonzero_minorminornonzeroevaluationdeterminanthscrc)) + ((mdr_b_first_nonzero_minorminornonzeroevaluationdeterminanthscrc) + (mdr_b_first_nonzero_minorminornonzeroevaluationdeterminanthscrc))) /\ ((mdr_e_first_nonzero_minorminornonzeroevaluationdeterminanthscrc = ((mdr_p_first_nonzero_minorminornonzeroevaluationdeterminanthsc) + (mdr_n_first_nonzero_minorminornonzeroevaluationdeterminanthsc)) * S ((mdr_p_first_nonzero_minorminornonzeroevaluationdeterminanthsc) + (mdr_n_first_nonzero_minorminornonzeroevaluationdeterminanthsc)) + ((mdr_n_first_nonzero_minorminornonzeroevaluationdeterminanthsc) + (mdr_n_first_nonzero_minorminornonzeroevaluationdeterminanthsc))) /\ ((mdr_f_first_nonzero_minorminornonzeroevaluationdeterminanthscrc = ((mdr_ut_first_nonzero_minorminornonzeroevaluationdeterminanthsc) + (mdr_e_first_nonzero_minorminornonzeroevaluationdeterminanthscrc)) * S ((mdr_ut_first_nonzero_minorminornonzeroevaluationdeterminanthsc) + (mdr_e_first_nonzero_minorminornonzeroevaluationdeterminanthscrc)) + ((mdr_e_first_nonzero_minorminornonzeroevaluationdeterminanthscrc) + (mdr_e_first_nonzero_minorminornonzeroevaluationdeterminanthscrc))) /\ ((mdr_z_first_nonzero_minorminornonzeroevaluationdeterminanthscr) = ((mdr_c_first_nonzero_minorminornonzeroevaluationdeterminanthscrc) + (mdr_f_first_nonzero_minorminornonzeroevaluationdeterminanthscrc)) * S ((mdr_c_first_nonzero_minorminornonzeroevaluationdeterminanthscrc) + (mdr_f_first_nonzero_minorminornonzeroevaluationdeterminanthscrc)) + ((mdr_f_first_nonzero_minorminornonzeroevaluationdeterminanthscrc) + (mdr_f_first_nonzero_minorminornonzeroevaluationdeterminanthscrc))))))))) /\ (((exists ff_h_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthscrb. ff_h_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthscrb + S (mdr_z_first_nonzero_minorminornonzeroevaluationdeterminanthscr) = S ((S (mdr_i_first_nonzero_minorminornonzeroevaluationdeterminanthsc)) * mdr_c_first_nonzero_minorminornonzeroevaluationdeterminant)) /\ exists ff_q_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthscrb. mdr_b_first_nonzero_minorminornonzeroevaluationdeterminant = ff_q_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthscrb * S ((S (mdr_i_first_nonzero_minorminornonzeroevaluationdeterminanthsc)) * mdr_c_first_nonzero_minorminornonzeroevaluationdeterminant) + (mdr_z_first_nonzero_minorminornonzeroevaluationdeterminanthscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthscm_positive. (exists ff_gap_mdm_lt_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthscm_positive_index_bound. ff_gap_mdm_lt_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthscm_positive) = ((mdr_q_first_nonzero_minorminornonzeroevaluationdeterminanths) * (mdr_q_first_nonzero_minorminornonzeroevaluationdeterminanths))) -> exists ff_row_mdm_prefix_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthscm_positive ff_column_mdm_prefix_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthscm_positive ff_value_mdm_prefix_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthscm_positive. (ff_index_mdm_prefix_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthscm_positive = (mdr_q_first_nonzero_minorminornonzeroevaluationdeterminanths) * ff_row_mdm_prefix_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthscm_positive + ff_column_mdm_prefix_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthscm_positive /\ ((exists ff_gap_mdm_lt_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthscm_positive_column_bound. ff_gap_mdm_lt_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthscm_positive) = (mdr_q_first_nonzero_minorminornonzeroevaluationdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthscm_positive_cell ff_column_mdm_cell_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthscm_positive_cell = ff_row_mdm_prefix_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthscm_positive_cell_row_after. ff_gap_mdm_le_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthscm_positive)) /\ ff_row_mdm_cell_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthscm_positive_cell = S ff_row_mdm_prefix_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthscm_positive) = (mdr_j_first_nonzero_minorminornonzeroevaluationdeterminanthsc)) /\ ff_column_mdm_cell_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthscm_positive_cell = ff_column_mdm_prefix_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthscm_positive_cell_column_after. ff_gap_mdm_le_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthscm_positive_cell_column_after + (mdr_j_first_nonzero_minorminornonzeroevaluationdeterminanthsc) = (ff_column_mdm_prefix_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthscm_positive)) /\ ff_column_mdm_cell_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthscm_positive_cell = S ff_column_mdm_prefix_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthscm_positive))) /\ (((exists ff_h_mdm_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthscm_positive_cell_source. ff_h_mdm_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthscm_positive) = S ((S ((ff_row_mdm_cell_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthscm_positive_cell) * (S (mdr_q_first_nonzero_minorminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthscm_positive_cell))) * mdr_pc_first_nonzero_minorminornonzeroevaluationdeterminanth)) /\ exists ff_q_mdm_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthscm_positive_cell_source. mdr_pb_first_nonzero_minorminornonzeroevaluationdeterminanth = ff_q_mdm_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthscm_positive_cell) * (S (mdr_q_first_nonzero_minorminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthscm_positive_cell))) * mdr_pc_first_nonzero_minorminornonzeroevaluationdeterminanth) + (ff_value_mdm_prefix_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthscm_positive)))))) /\ (((exists ff_h_mdm_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthscm_positive_target. ff_h_mdm_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthscm_positive_target + S (ff_value_mdm_prefix_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthscm_positive) = S ((S (ff_index_mdm_prefix_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthscm_positive)) * mdr_us_first_nonzero_minorminornonzeroevaluationdeterminanthsc)) /\ exists ff_q_mdm_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthscm_positive_target. mdr_up_first_nonzero_minorminornonzeroevaluationdeterminanthsc = ff_q_mdm_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthscm_positive)) * mdr_us_first_nonzero_minorminornonzeroevaluationdeterminanthsc) + (ff_value_mdm_prefix_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthscm_negative. (exists ff_gap_mdm_lt_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthscm_negative_index_bound. ff_gap_mdm_lt_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthscm_negative) = ((mdr_q_first_nonzero_minorminornonzeroevaluationdeterminanths) * (mdr_q_first_nonzero_minorminornonzeroevaluationdeterminanths))) -> exists ff_row_mdm_prefix_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthscm_negative ff_column_mdm_prefix_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthscm_negative ff_value_mdm_prefix_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthscm_negative. (ff_index_mdm_prefix_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthscm_negative = (mdr_q_first_nonzero_minorminornonzeroevaluationdeterminanths) * ff_row_mdm_prefix_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthscm_negative + ff_column_mdm_prefix_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthscm_negative /\ ((exists ff_gap_mdm_lt_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthscm_negative_column_bound. ff_gap_mdm_lt_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthscm_negative) = (mdr_q_first_nonzero_minorminornonzeroevaluationdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthscm_negative_cell ff_column_mdm_cell_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthscm_negative_cell = ff_row_mdm_prefix_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthscm_negative_cell_row_after. ff_gap_mdm_le_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthscm_negative)) /\ ff_row_mdm_cell_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthscm_negative_cell = S ff_row_mdm_prefix_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthscm_negative) = (mdr_j_first_nonzero_minorminornonzeroevaluationdeterminanthsc)) /\ ff_column_mdm_cell_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthscm_negative_cell = ff_column_mdm_prefix_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthscm_negative_cell_column_after. ff_gap_mdm_le_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthscm_negative_cell_column_after + (mdr_j_first_nonzero_minorminornonzeroevaluationdeterminanthsc) = (ff_column_mdm_prefix_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthscm_negative)) /\ ff_column_mdm_cell_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthscm_negative_cell = S ff_column_mdm_prefix_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthscm_negative))) /\ (((exists ff_h_mdm_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthscm_negative_cell_source. ff_h_mdm_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthscm_negative) = S ((S ((ff_row_mdm_cell_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthscm_negative_cell) * (S (mdr_q_first_nonzero_minorminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthscm_negative_cell))) * mdr_nc_first_nonzero_minorminornonzeroevaluationdeterminanth)) /\ exists ff_q_mdm_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthscm_negative_cell_source. mdr_nb_first_nonzero_minorminornonzeroevaluationdeterminanth = ff_q_mdm_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthscm_negative_cell) * (S (mdr_q_first_nonzero_minorminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthscm_negative_cell))) * mdr_nc_first_nonzero_minorminornonzeroevaluationdeterminanth) + (ff_value_mdm_prefix_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthscm_negative)))))) /\ (((exists ff_h_mdm_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthscm_negative_target. ff_h_mdm_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthscm_negative_target + S (ff_value_mdm_prefix_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthscm_negative) = S ((S (ff_index_mdm_prefix_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthscm_negative)) * mdr_ut_first_nonzero_minorminornonzeroevaluationdeterminanthsc)) /\ exists ff_q_mdm_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthscm_negative_target. mdr_un_first_nonzero_minorminornonzeroevaluationdeterminanthsc = ff_q_mdm_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthscm_negative)) * mdr_ut_first_nonzero_minorminornonzeroevaluationdeterminanthsc) + (ff_value_mdm_prefix_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthscm_negative))))))))) /\ ((((exists ff_h_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthscp. ff_h_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthscp + S (mdr_p_first_nonzero_minorminornonzeroevaluationdeterminanthsc) = S ((S (mdr_j_first_nonzero_minorminornonzeroevaluationdeterminanthsc)) * mdr_ec_first_nonzero_minorminornonzeroevaluationdeterminanths)) /\ exists ff_q_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthscp. mdr_eb_first_nonzero_minorminornonzeroevaluationdeterminanths = ff_q_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthscp * S ((S (mdr_j_first_nonzero_minorminornonzeroevaluationdeterminanthsc)) * mdr_ec_first_nonzero_minorminornonzeroevaluationdeterminanths) + (mdr_p_first_nonzero_minorminornonzeroevaluationdeterminanthsc))) /\ (((exists ff_h_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthscn. ff_h_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthscn + S (mdr_n_first_nonzero_minorminornonzeroevaluationdeterminanthsc) = S ((S (mdr_j_first_nonzero_minorminornonzeroevaluationdeterminanthsc)) * mdr_fc_first_nonzero_minorminornonzeroevaluationdeterminanths)) /\ exists ff_q_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthscn. mdr_fb_first_nonzero_minorminornonzeroevaluationdeterminanths = ff_q_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthscn * S ((S (mdr_j_first_nonzero_minorminornonzeroevaluationdeterminanthsc)) * mdr_fc_first_nonzero_minorminornonzeroevaluationdeterminanths) + (mdr_n_first_nonzero_minorminornonzeroevaluationdeterminanthsc)))))))) /\ (exists ff_ub_mce_fold_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf ff_uc_mce_fold_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf ff_vb_mce_fold_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf ff_vc_mce_fold_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf. ((forall ff_index_mce_alternating_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix. (exists ff_gap_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix_index. ff_gap_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix_index + S (ff_index_mce_alternating_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix) = (S (mdr_q_first_nonzero_minorminornonzeroevaluationdeterminanths))) -> exists ff_ap_mce_alternating_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix ff_an_mce_alternating_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix ff_bp_mce_alternating_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix ff_bn_mce_alternating_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix ff_p_mce_alternating_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix ff_n_mce_alternating_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix. ((((exists ff_h_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix_ap. ff_h_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix_ap + S (ff_ap_mce_alternating_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix)) * mdr_pc_first_nonzero_minorminornonzeroevaluationdeterminanth)) /\ exists ff_q_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix_ap. mdr_pb_first_nonzero_minorminornonzeroevaluationdeterminanth = ff_q_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix)) * mdr_pc_first_nonzero_minorminornonzeroevaluationdeterminanth) + (ff_ap_mce_alternating_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix_an. ff_h_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix_an + S (ff_an_mce_alternating_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix)) * mdr_nc_first_nonzero_minorminornonzeroevaluationdeterminanth)) /\ exists ff_q_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix_an. mdr_nb_first_nonzero_minorminornonzeroevaluationdeterminanth = ff_q_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix)) * mdr_nc_first_nonzero_minorminornonzeroevaluationdeterminanth) + (ff_an_mce_alternating_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix_bp. ff_h_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix_bp + S (ff_bp_mce_alternating_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix)) * mdr_ec_first_nonzero_minorminornonzeroevaluationdeterminanths)) /\ exists ff_q_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix_bp. mdr_eb_first_nonzero_minorminornonzeroevaluationdeterminanths = ff_q_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix)) * mdr_ec_first_nonzero_minorminornonzeroevaluationdeterminanths) + (ff_bp_mce_alternating_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix_bn. ff_h_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix_bn + S (ff_bn_mce_alternating_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix)) * mdr_fc_first_nonzero_minorminornonzeroevaluationdeterminanths)) /\ exists ff_q_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix_bn. mdr_fb_first_nonzero_minorminornonzeroevaluationdeterminanths = ff_q_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix)) * mdr_fc_first_nonzero_minorminornonzeroevaluationdeterminanths) + (ff_bn_mce_alternating_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix_positive. ff_h_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix_positive + S (ff_p_mce_alternating_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix_positive. ff_ub_mce_fold_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf) + (ff_p_mce_alternating_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix_negative. ff_h_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix_negative + S (ff_n_mce_alternating_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix_negative. ff_vb_mce_fold_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf) + (ff_n_mce_alternating_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix))) /\ (((exists ff_even_mce_term_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix = 2 * ff_even_mce_term_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix_term) /\ (ff_p_mce_alternating_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix = 2 * ff_odd_mce_term_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_positive ff_v_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_positive. ((((exists ff_h_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_positive_start. ff_h_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_positive_start. ff_u_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_positive_start * S ((S (0)) * ff_v_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_positive_terminal. ff_h_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_positive_terminal + S (mdr_p_first_nonzero_minorminornonzeroevaluationdeterminanth) = S ((S ((S (mdr_q_first_nonzero_minorminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_positive_terminal. ff_u_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_positive_terminal * S ((S ((S (mdr_q_first_nonzero_minorminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_positive) + (mdr_p_first_nonzero_minorminornonzeroevaluationdeterminanth))) /\ forall ff_i_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_positive. (exists ff_lt_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_positive_bound. ff_lt_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_positive_bound + S ff_i_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_positive = (S (mdr_q_first_nonzero_minorminornonzeroevaluationdeterminanths))) -> exists ff_a_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_positive ff_r_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_positive ff_s_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_positive. ((((exists ff_h_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_positive_summand. ff_h_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_positive_summand + S (ff_a_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_positive_summand. ff_ub_mce_fold_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_positive_summand * S ((S (ff_i_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf) + (ff_a_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_positive_partial. ff_h_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_positive_partial + S (ff_r_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_positive_partial. ff_u_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_positive_partial * S ((S (ff_i_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_positive) + (ff_r_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_positive_successor. ff_h_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_positive_successor + S (ff_s_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_positive) = S ((S (S ff_i_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_positive_successor. ff_u_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_positive_successor * S ((S (S ff_i_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_positive) + (ff_s_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_positive))) /\ ff_s_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_positive = ff_r_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_positive + ff_a_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_positive)))))) /\ (exists ff_u_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_negative ff_v_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_negative. ((((exists ff_h_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_negative_start. ff_h_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_negative_start. ff_u_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_negative_start * S ((S (0)) * ff_v_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_negative_terminal. ff_h_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_negative_terminal + S (mdr_n_first_nonzero_minorminornonzeroevaluationdeterminanth) = S ((S ((S (mdr_q_first_nonzero_minorminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_negative_terminal. ff_u_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_negative_terminal * S ((S ((S (mdr_q_first_nonzero_minorminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_negative) + (mdr_n_first_nonzero_minorminornonzeroevaluationdeterminanth))) /\ forall ff_i_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_negative. (exists ff_lt_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_negative_bound. ff_lt_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_negative_bound + S ff_i_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_negative = (S (mdr_q_first_nonzero_minorminornonzeroevaluationdeterminanths))) -> exists ff_a_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_negative ff_r_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_negative ff_s_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_negative. ((((exists ff_h_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_negative_summand. ff_h_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_negative_summand + S (ff_a_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_negative_summand. ff_vb_mce_fold_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_negative_summand * S ((S (ff_i_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf) + (ff_a_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_negative_partial. ff_h_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_negative_partial + S (ff_r_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_negative_partial. ff_u_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_negative_partial * S ((S (ff_i_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_negative) + (ff_r_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_negative_successor. ff_h_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_negative_successor + S (ff_s_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_negative) = S ((S (S ff_i_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_negative_successor. ff_u_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_negative_successor * S ((S (S ff_i_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_negative) + (ff_s_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_negative))) /\ ff_s_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_negative = ff_r_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_negative + ff_a_mce_mdr_first_nonzero_minorminornonzeroevaluationdeterminanthsf_negative))))))))))))))) /\ ((exists mdr_gap_first_nonzero_minorminornonzeroevaluationdeterminanti. mdr_gap_first_nonzero_minorminornonzeroevaluationdeterminanti + S (mdr_i_first_nonzero_minorminornonzeroevaluationdeterminant) = (mdr_l_first_nonzero_minorminornonzeroevaluationdeterminant)) /\ (exists mdr_z_first_nonzero_minorminornonzeroevaluationdeterminantr. ((exists mdr_a_first_nonzero_minorminornonzeroevaluationdeterminantrc mdr_b_first_nonzero_minorminornonzeroevaluationdeterminantrc mdr_c_first_nonzero_minorminornonzeroevaluationdeterminantrc mdr_e_first_nonzero_minorminornonzeroevaluationdeterminantrc mdr_f_first_nonzero_minorminornonzeroevaluationdeterminantrc. ((mdr_a_first_nonzero_minorminornonzeroevaluationdeterminantrc = ((q) + (mdr_ub_first_nonzero_minorminornonzeroevaluation)) * S ((q) + (mdr_ub_first_nonzero_minorminornonzeroevaluation)) + ((mdr_ub_first_nonzero_minorminornonzeroevaluation) + (mdr_ub_first_nonzero_minorminornonzeroevaluation))) /\ ((mdr_b_first_nonzero_minorminornonzeroevaluationdeterminantrc = ((mdr_uc_first_nonzero_minorminornonzeroevaluation) + (mdr_vb_first_nonzero_minorminornonzeroevaluation)) * S ((mdr_uc_first_nonzero_minorminornonzeroevaluation) + (mdr_vb_first_nonzero_minorminornonzeroevaluation)) + ((mdr_vb_first_nonzero_minorminornonzeroevaluation) + (mdr_vb_first_nonzero_minorminornonzeroevaluation))) /\ ((mdr_c_first_nonzero_minorminornonzeroevaluationdeterminantrc = ((mdr_a_first_nonzero_minorminornonzeroevaluationdeterminantrc) + (mdr_b_first_nonzero_minorminornonzeroevaluationdeterminantrc)) * S ((mdr_a_first_nonzero_minorminornonzeroevaluationdeterminantrc) + (mdr_b_first_nonzero_minorminornonzeroevaluationdeterminantrc)) + ((mdr_b_first_nonzero_minorminornonzeroevaluationdeterminantrc) + (mdr_b_first_nonzero_minorminornonzeroevaluationdeterminantrc))) /\ ((mdr_e_first_nonzero_minorminornonzeroevaluationdeterminantrc = ((mdr_p_first_nonzero_minorminornonzero) + (mdr_n_first_nonzero_minorminornonzero)) * S ((mdr_p_first_nonzero_minorminornonzero) + (mdr_n_first_nonzero_minorminornonzero)) + ((mdr_n_first_nonzero_minorminornonzero) + (mdr_n_first_nonzero_minorminornonzero))) /\ ((mdr_f_first_nonzero_minorminornonzeroevaluationdeterminantrc = ((mdr_vc_first_nonzero_minorminornonzeroevaluation) + (mdr_e_first_nonzero_minorminornonzeroevaluationdeterminantrc)) * S ((mdr_vc_first_nonzero_minorminornonzeroevaluation) + (mdr_e_first_nonzero_minorminornonzeroevaluationdeterminantrc)) + ((mdr_e_first_nonzero_minorminornonzeroevaluationdeterminantrc) + (mdr_e_first_nonzero_minorminornonzeroevaluationdeterminantrc))) /\ ((mdr_z_first_nonzero_minorminornonzeroevaluationdeterminantr) = ((mdr_c_first_nonzero_minorminornonzeroevaluationdeterminantrc) + (mdr_f_first_nonzero_minorminornonzeroevaluationdeterminantrc)) * S ((mdr_c_first_nonzero_minorminornonzeroevaluationdeterminantrc) + (mdr_f_first_nonzero_minorminornonzeroevaluationdeterminantrc)) + ((mdr_f_first_nonzero_minorminornonzeroevaluationdeterminantrc) + (mdr_f_first_nonzero_minorminornonzeroevaluationdeterminantrc))))))))) /\ (((exists ff_h_mdr_first_nonzero_minorminornonzeroevaluationdeterminantrb. ff_h_mdr_first_nonzero_minorminornonzeroevaluationdeterminantrb + S (mdr_z_first_nonzero_minorminornonzeroevaluationdeterminantr) = S ((S (mdr_i_first_nonzero_minorminornonzeroevaluationdeterminant)) * mdr_c_first_nonzero_minorminornonzeroevaluationdeterminant)) /\ exists ff_q_mdr_first_nonzero_minorminornonzeroevaluationdeterminantrb. mdr_b_first_nonzero_minorminornonzeroevaluationdeterminant = ff_q_mdr_first_nonzero_minorminornonzeroevaluationdeterminantrb * S ((S (mdr_i_first_nonzero_minorminornonzeroevaluationdeterminant)) * mdr_c_first_nonzero_minorminornonzeroevaluationdeterminant) + (mdr_z_first_nonzero_minorminornonzeroevaluationdeterminantr)))))))))) /\ (~(mdr_p_first_nonzero_minorminornonzero = mdr_n_first_nonzero_minorminornonzero)))))))) -> (exists mdr_rb_second_nonzero_minor mdr_rc_second_nonzero_minor mdr_cb_second_nonzero_minor mdr_cc_second_nonzero_minor. (((((forall fom_index_mrf_second_nonzero_minorminorrowsbound. (exists fom_gap_mrf_second_nonzero_minorminorrowsbound_index_bound. fom_gap_mrf_second_nonzero_minorminorrowsbound_index_bound + S (fom_index_mrf_second_nonzero_minorminorrowsbound) = q) -> exists fom_value_mrf_second_nonzero_minorminorrowsbound. ((((exists fom_beta_height_mrf_second_nonzero_minorminorrowsbound_entry. fom_beta_height_mrf_second_nonzero_minorminorrowsbound_entry + S (fom_value_mrf_second_nonzero_minorminorrowsbound) = S ((S (fom_index_mrf_second_nonzero_minorminorrowsbound)) * mdr_rc_second_nonzero_minor)) /\ exists fom_beta_quotient_mrf_second_nonzero_minorminorrowsbound_entry. mdr_rb_second_nonzero_minor = fom_beta_quotient_mrf_second_nonzero_minorminorrowsbound_entry * S ((S (fom_index_mrf_second_nonzero_minorminorrowsbound)) * mdr_rc_second_nonzero_minor) + (fom_value_mrf_second_nonzero_minorminorrowsbound))) /\ (exists fom_gap_mrf_second_nonzero_minorminorrowsbound_value_bound. fom_gap_mrf_second_nonzero_minorminorrowsbound_value_bound + S (fom_value_mrf_second_nonzero_minorminorrowsbound) = r))) /\ (forall mdr_i_second_nonzero_minorminorrowsdistinct mdr_j_second_nonzero_minorminorrowsdistinct mdr_a_second_nonzero_minorminorrowsdistinct. (exists mdr_gap_second_nonzero_minorminorrowsdistincti. mdr_gap_second_nonzero_minorminorrowsdistincti + S (mdr_i_second_nonzero_minorminorrowsdistinct) = (q)) -> (exists mdr_gap_second_nonzero_minorminorrowsdistinctj. mdr_gap_second_nonzero_minorminorrowsdistinctj + S (mdr_j_second_nonzero_minorminorrowsdistinct) = (q)) -> (((exists ff_h_mdr_second_nonzero_minorminorrowsdistinctfirst. ff_h_mdr_second_nonzero_minorminorrowsdistinctfirst + S (mdr_a_second_nonzero_minorminorrowsdistinct) = S ((S (mdr_i_second_nonzero_minorminorrowsdistinct)) * mdr_rc_second_nonzero_minor)) /\ exists ff_q_mdr_second_nonzero_minorminorrowsdistinctfirst. mdr_rb_second_nonzero_minor = ff_q_mdr_second_nonzero_minorminorrowsdistinctfirst * S ((S (mdr_i_second_nonzero_minorminorrowsdistinct)) * mdr_rc_second_nonzero_minor) + (mdr_a_second_nonzero_minorminorrowsdistinct))) -> (((exists ff_h_mdr_second_nonzero_minorminorrowsdistinctsecond. ff_h_mdr_second_nonzero_minorminorrowsdistinctsecond + S (mdr_a_second_nonzero_minorminorrowsdistinct) = S ((S (mdr_j_second_nonzero_minorminorrowsdistinct)) * mdr_rc_second_nonzero_minor)) /\ exists ff_q_mdr_second_nonzero_minorminorrowsdistinctsecond. mdr_rb_second_nonzero_minor = ff_q_mdr_second_nonzero_minorminorrowsdistinctsecond * S ((S (mdr_j_second_nonzero_minorminorrowsdistinct)) * mdr_rc_second_nonzero_minor) + (mdr_a_second_nonzero_minorminorrowsdistinct))) -> mdr_i_second_nonzero_minorminorrowsdistinct = mdr_j_second_nonzero_minorminorrowsdistinct))) /\ ((((forall fom_index_mrf_second_nonzero_minorminorcolumnsbound. (exists fom_gap_mrf_second_nonzero_minorminorcolumnsbound_index_bound. fom_gap_mrf_second_nonzero_minorminorcolumnsbound_index_bound + S (fom_index_mrf_second_nonzero_minorminorcolumnsbound) = q) -> exists fom_value_mrf_second_nonzero_minorminorcolumnsbound. ((((exists fom_beta_height_mrf_second_nonzero_minorminorcolumnsbound_entry. fom_beta_height_mrf_second_nonzero_minorminorcolumnsbound_entry + S (fom_value_mrf_second_nonzero_minorminorcolumnsbound) = S ((S (fom_index_mrf_second_nonzero_minorminorcolumnsbound)) * mdr_cc_second_nonzero_minor)) /\ exists fom_beta_quotient_mrf_second_nonzero_minorminorcolumnsbound_entry. mdr_cb_second_nonzero_minor = fom_beta_quotient_mrf_second_nonzero_minorminorcolumnsbound_entry * S ((S (fom_index_mrf_second_nonzero_minorminorcolumnsbound)) * mdr_cc_second_nonzero_minor) + (fom_value_mrf_second_nonzero_minorminorcolumnsbound))) /\ (exists fom_gap_mrf_second_nonzero_minorminorcolumnsbound_value_bound. fom_gap_mrf_second_nonzero_minorminorcolumnsbound_value_bound + S (fom_value_mrf_second_nonzero_minorminorcolumnsbound) = w))) /\ (forall mdr_i_second_nonzero_minorminorcolumnsdistinct mdr_j_second_nonzero_minorminorcolumnsdistinct mdr_a_second_nonzero_minorminorcolumnsdistinct. (exists mdr_gap_second_nonzero_minorminorcolumnsdistincti. mdr_gap_second_nonzero_minorminorcolumnsdistincti + S (mdr_i_second_nonzero_minorminorcolumnsdistinct) = (q)) -> (exists mdr_gap_second_nonzero_minorminorcolumnsdistinctj. mdr_gap_second_nonzero_minorminorcolumnsdistinctj + S (mdr_j_second_nonzero_minorminorcolumnsdistinct) = (q)) -> (((exists ff_h_mdr_second_nonzero_minorminorcolumnsdistinctfirst. ff_h_mdr_second_nonzero_minorminorcolumnsdistinctfirst + S (mdr_a_second_nonzero_minorminorcolumnsdistinct) = S ((S (mdr_i_second_nonzero_minorminorcolumnsdistinct)) * mdr_cc_second_nonzero_minor)) /\ exists ff_q_mdr_second_nonzero_minorminorcolumnsdistinctfirst. mdr_cb_second_nonzero_minor = ff_q_mdr_second_nonzero_minorminorcolumnsdistinctfirst * S ((S (mdr_i_second_nonzero_minorminorcolumnsdistinct)) * mdr_cc_second_nonzero_minor) + (mdr_a_second_nonzero_minorminorcolumnsdistinct))) -> (((exists ff_h_mdr_second_nonzero_minorminorcolumnsdistinctsecond. ff_h_mdr_second_nonzero_minorminorcolumnsdistinctsecond + S (mdr_a_second_nonzero_minorminorcolumnsdistinct) = S ((S (mdr_j_second_nonzero_minorminorcolumnsdistinct)) * mdr_cc_second_nonzero_minor)) /\ exists ff_q_mdr_second_nonzero_minorminorcolumnsdistinctsecond. mdr_cb_second_nonzero_minor = ff_q_mdr_second_nonzero_minorminorcolumnsdistinctsecond * S ((S (mdr_j_second_nonzero_minorminorcolumnsdistinct)) * mdr_cc_second_nonzero_minor) + (mdr_a_second_nonzero_minorminorcolumnsdistinct))) -> mdr_i_second_nonzero_minorminorcolumnsdistinct = mdr_j_second_nonzero_minorminorcolumnsdistinct))) /\ (exists mdr_p_second_nonzero_minorminornonzero mdr_n_second_nonzero_minorminornonzero. ((exists mdr_ub_second_nonzero_minorminornonzeroevaluation mdr_uc_second_nonzero_minorminornonzeroevaluation mdr_vb_second_nonzero_minorminornonzeroevaluation mdr_vc_second_nonzero_minorminornonzeroevaluation. ((((forall mdr_i_second_nonzero_minorminornonzeroevaluationmatrixpositive. (exists mdr_gap_second_nonzero_minorminornonzeroevaluationmatrixpositivebound. mdr_gap_second_nonzero_minorminornonzeroevaluationmatrixpositivebound + S (mdr_i_second_nonzero_minorminornonzeroevaluationmatrixpositive) = ((q) * (q))) -> exists mdr_a_second_nonzero_minorminornonzeroevaluationmatrixpositive. (((exists mdr_r_second_nonzero_minorminornonzeroevaluationmatrixpositivepoint mdr_s_second_nonzero_minorminornonzeroevaluationmatrixpositivepoint mdr_u_second_nonzero_minorminornonzeroevaluationmatrixpositivepoint mdr_v_second_nonzero_minorminornonzeroevaluationmatrixpositivepoint. ((mdr_i_second_nonzero_minorminornonzeroevaluationmatrixpositive = (q) * mdr_r_second_nonzero_minorminornonzeroevaluationmatrixpositivepoint + mdr_s_second_nonzero_minorminornonzeroevaluationmatrixpositivepoint) /\ ((exists mdr_gap_second_nonzero_minorminornonzeroevaluationmatrixpositivepointcolumn. mdr_gap_second_nonzero_minorminornonzeroevaluationmatrixpositivepointcolumn + S (mdr_s_second_nonzero_minorminornonzeroevaluationmatrixpositivepoint) = (q)) /\ ((((exists ff_h_mdr_second_nonzero_minorminornonzeroevaluationmatrixpositivepointrow_index. ff_h_mdr_second_nonzero_minorminornonzeroevaluationmatrixpositivepointrow_index + S (mdr_u_second_nonzero_minorminornonzeroevaluationmatrixpositivepoint) = S ((S (mdr_r_second_nonzero_minorminornonzeroevaluationmatrixpositivepoint)) * mdr_rc_second_nonzero_minor)) /\ exists ff_q_mdr_second_nonzero_minorminornonzeroevaluationmatrixpositivepointrow_index. mdr_rb_second_nonzero_minor = ff_q_mdr_second_nonzero_minorminornonzeroevaluationmatrixpositivepointrow_index * S ((S (mdr_r_second_nonzero_minorminornonzeroevaluationmatrixpositivepoint)) * mdr_rc_second_nonzero_minor) + (mdr_u_second_nonzero_minorminornonzeroevaluationmatrixpositivepoint))) /\ ((((exists ff_h_mdr_second_nonzero_minorminornonzeroevaluationmatrixpositivepointcolumn_index. ff_h_mdr_second_nonzero_minorminornonzeroevaluationmatrixpositivepointcolumn_index + S (mdr_v_second_nonzero_minorminornonzeroevaluationmatrixpositivepoint) = S ((S (mdr_s_second_nonzero_minorminornonzeroevaluationmatrixpositivepoint)) * mdr_cc_second_nonzero_minor)) /\ exists ff_q_mdr_second_nonzero_minorminornonzeroevaluationmatrixpositivepointcolumn_index. mdr_cb_second_nonzero_minor = ff_q_mdr_second_nonzero_minorminornonzeroevaluationmatrixpositivepointcolumn_index * S ((S (mdr_s_second_nonzero_minorminornonzeroevaluationmatrixpositivepoint)) * mdr_cc_second_nonzero_minor) + (mdr_v_second_nonzero_minorminornonzeroevaluationmatrixpositivepoint))) /\ (((exists ff_h_mdr_second_nonzero_minorminornonzeroevaluationmatrixpositivepointsource. ff_h_mdr_second_nonzero_minorminornonzeroevaluationmatrixpositivepointsource + S (mdr_a_second_nonzero_minorminornonzeroevaluationmatrixpositive) = S ((S ((mdr_u_second_nonzero_minorminornonzeroevaluationmatrixpositivepoint) * (w) + (mdr_v_second_nonzero_minorminornonzeroevaluationmatrixpositivepoint))) * ec)) /\ exists ff_q_mdr_second_nonzero_minorminornonzeroevaluationmatrixpositivepointsource. eb = ff_q_mdr_second_nonzero_minorminornonzeroevaluationmatrixpositivepointsource * S ((S ((mdr_u_second_nonzero_minorminornonzeroevaluationmatrixpositivepoint) * (w) + (mdr_v_second_nonzero_minorminornonzeroevaluationmatrixpositivepoint))) * ec) + (mdr_a_second_nonzero_minorminornonzeroevaluationmatrixpositive)))))))) /\ (((exists ff_h_mdr_second_nonzero_minorminornonzeroevaluationmatrixpositiveoutput. ff_h_mdr_second_nonzero_minorminornonzeroevaluationmatrixpositiveoutput + S (mdr_a_second_nonzero_minorminornonzeroevaluationmatrixpositive) = S ((S (mdr_i_second_nonzero_minorminornonzeroevaluationmatrixpositive)) * mdr_uc_second_nonzero_minorminornonzeroevaluation)) /\ exists ff_q_mdr_second_nonzero_minorminornonzeroevaluationmatrixpositiveoutput. mdr_ub_second_nonzero_minorminornonzeroevaluation = ff_q_mdr_second_nonzero_minorminornonzeroevaluationmatrixpositiveoutput * S ((S (mdr_i_second_nonzero_minorminornonzeroevaluationmatrixpositive)) * mdr_uc_second_nonzero_minorminornonzeroevaluation) + (mdr_a_second_nonzero_minorminornonzeroevaluationmatrixpositive)))))) /\ (forall mdr_i_second_nonzero_minorminornonzeroevaluationmatrixnegative. (exists mdr_gap_second_nonzero_minorminornonzeroevaluationmatrixnegativebound. mdr_gap_second_nonzero_minorminornonzeroevaluationmatrixnegativebound + S (mdr_i_second_nonzero_minorminornonzeroevaluationmatrixnegative) = ((q) * (q))) -> exists mdr_a_second_nonzero_minorminornonzeroevaluationmatrixnegative. (((exists mdr_r_second_nonzero_minorminornonzeroevaluationmatrixnegativepoint mdr_s_second_nonzero_minorminornonzeroevaluationmatrixnegativepoint mdr_u_second_nonzero_minorminornonzeroevaluationmatrixnegativepoint mdr_v_second_nonzero_minorminornonzeroevaluationmatrixnegativepoint. ((mdr_i_second_nonzero_minorminornonzeroevaluationmatrixnegative = (q) * mdr_r_second_nonzero_minorminornonzeroevaluationmatrixnegativepoint + mdr_s_second_nonzero_minorminornonzeroevaluationmatrixnegativepoint) /\ ((exists mdr_gap_second_nonzero_minorminornonzeroevaluationmatrixnegativepointcolumn. mdr_gap_second_nonzero_minorminornonzeroevaluationmatrixnegativepointcolumn + S (mdr_s_second_nonzero_minorminornonzeroevaluationmatrixnegativepoint) = (q)) /\ ((((exists ff_h_mdr_second_nonzero_minorminornonzeroevaluationmatrixnegativepointrow_index. ff_h_mdr_second_nonzero_minorminornonzeroevaluationmatrixnegativepointrow_index + S (mdr_u_second_nonzero_minorminornonzeroevaluationmatrixnegativepoint) = S ((S (mdr_r_second_nonzero_minorminornonzeroevaluationmatrixnegativepoint)) * mdr_rc_second_nonzero_minor)) /\ exists ff_q_mdr_second_nonzero_minorminornonzeroevaluationmatrixnegativepointrow_index. mdr_rb_second_nonzero_minor = ff_q_mdr_second_nonzero_minorminornonzeroevaluationmatrixnegativepointrow_index * S ((S (mdr_r_second_nonzero_minorminornonzeroevaluationmatrixnegativepoint)) * mdr_rc_second_nonzero_minor) + (mdr_u_second_nonzero_minorminornonzeroevaluationmatrixnegativepoint))) /\ ((((exists ff_h_mdr_second_nonzero_minorminornonzeroevaluationmatrixnegativepointcolumn_index. ff_h_mdr_second_nonzero_minorminornonzeroevaluationmatrixnegativepointcolumn_index + S (mdr_v_second_nonzero_minorminornonzeroevaluationmatrixnegativepoint) = S ((S (mdr_s_second_nonzero_minorminornonzeroevaluationmatrixnegativepoint)) * mdr_cc_second_nonzero_minor)) /\ exists ff_q_mdr_second_nonzero_minorminornonzeroevaluationmatrixnegativepointcolumn_index. mdr_cb_second_nonzero_minor = ff_q_mdr_second_nonzero_minorminornonzeroevaluationmatrixnegativepointcolumn_index * S ((S (mdr_s_second_nonzero_minorminornonzeroevaluationmatrixnegativepoint)) * mdr_cc_second_nonzero_minor) + (mdr_v_second_nonzero_minorminornonzeroevaluationmatrixnegativepoint))) /\ (((exists ff_h_mdr_second_nonzero_minorminornonzeroevaluationmatrixnegativepointsource. ff_h_mdr_second_nonzero_minorminornonzeroevaluationmatrixnegativepointsource + S (mdr_a_second_nonzero_minorminornonzeroevaluationmatrixnegative) = S ((S ((mdr_u_second_nonzero_minorminornonzeroevaluationmatrixnegativepoint) * (w) + (mdr_v_second_nonzero_minorminornonzeroevaluationmatrixnegativepoint))) * fc)) /\ exists ff_q_mdr_second_nonzero_minorminornonzeroevaluationmatrixnegativepointsource. fb = ff_q_mdr_second_nonzero_minorminornonzeroevaluationmatrixnegativepointsource * S ((S ((mdr_u_second_nonzero_minorminornonzeroevaluationmatrixnegativepoint) * (w) + (mdr_v_second_nonzero_minorminornonzeroevaluationmatrixnegativepoint))) * fc) + (mdr_a_second_nonzero_minorminornonzeroevaluationmatrixnegative)))))))) /\ (((exists ff_h_mdr_second_nonzero_minorminornonzeroevaluationmatrixnegativeoutput. ff_h_mdr_second_nonzero_minorminornonzeroevaluationmatrixnegativeoutput + S (mdr_a_second_nonzero_minorminornonzeroevaluationmatrixnegative) = S ((S (mdr_i_second_nonzero_minorminornonzeroevaluationmatrixnegative)) * mdr_vc_second_nonzero_minorminornonzeroevaluation)) /\ exists ff_q_mdr_second_nonzero_minorminornonzeroevaluationmatrixnegativeoutput. mdr_vb_second_nonzero_minorminornonzeroevaluation = ff_q_mdr_second_nonzero_minorminornonzeroevaluationmatrixnegativeoutput * S ((S (mdr_i_second_nonzero_minorminornonzeroevaluationmatrixnegative)) * mdr_vc_second_nonzero_minorminornonzeroevaluation) + (mdr_a_second_nonzero_minorminornonzeroevaluationmatrixnegative)))))))) /\ (exists mdr_b_second_nonzero_minorminornonzeroevaluationdeterminant mdr_c_second_nonzero_minorminornonzeroevaluationdeterminant mdr_l_second_nonzero_minorminornonzeroevaluationdeterminant mdr_i_second_nonzero_minorminornonzeroevaluationdeterminant. ((forall mdr_i_second_nonzero_minorminornonzeroevaluationdeterminanth. (exists mdr_gap_second_nonzero_minorminornonzeroevaluationdeterminanthi. mdr_gap_second_nonzero_minorminornonzeroevaluationdeterminanthi + S (mdr_i_second_nonzero_minorminornonzeroevaluationdeterminanth) = (mdr_l_second_nonzero_minorminornonzeroevaluationdeterminant)) -> exists mdr_d_second_nonzero_minorminornonzeroevaluationdeterminanth mdr_pb_second_nonzero_minorminornonzeroevaluationdeterminanth mdr_pc_second_nonzero_minorminornonzeroevaluationdeterminanth mdr_nb_second_nonzero_minorminornonzeroevaluationdeterminanth mdr_nc_second_nonzero_minorminornonzeroevaluationdeterminanth mdr_p_second_nonzero_minorminornonzeroevaluationdeterminanth mdr_n_second_nonzero_minorminornonzeroevaluationdeterminanth. ((exists mdr_z_second_nonzero_minorminornonzeroevaluationdeterminanthr. ((exists mdr_a_second_nonzero_minorminornonzeroevaluationdeterminanthrc mdr_b_second_nonzero_minorminornonzeroevaluationdeterminanthrc mdr_c_second_nonzero_minorminornonzeroevaluationdeterminanthrc mdr_e_second_nonzero_minorminornonzeroevaluationdeterminanthrc mdr_f_second_nonzero_minorminornonzeroevaluationdeterminanthrc. ((mdr_a_second_nonzero_minorminornonzeroevaluationdeterminanthrc = ((mdr_d_second_nonzero_minorminornonzeroevaluationdeterminanth) + (mdr_pb_second_nonzero_minorminornonzeroevaluationdeterminanth)) * S ((mdr_d_second_nonzero_minorminornonzeroevaluationdeterminanth) + (mdr_pb_second_nonzero_minorminornonzeroevaluationdeterminanth)) + ((mdr_pb_second_nonzero_minorminornonzeroevaluationdeterminanth) + (mdr_pb_second_nonzero_minorminornonzeroevaluationdeterminanth))) /\ ((mdr_b_second_nonzero_minorminornonzeroevaluationdeterminanthrc = ((mdr_pc_second_nonzero_minorminornonzeroevaluationdeterminanth) + (mdr_nb_second_nonzero_minorminornonzeroevaluationdeterminanth)) * S ((mdr_pc_second_nonzero_minorminornonzeroevaluationdeterminanth) + (mdr_nb_second_nonzero_minorminornonzeroevaluationdeterminanth)) + ((mdr_nb_second_nonzero_minorminornonzeroevaluationdeterminanth) + (mdr_nb_second_nonzero_minorminornonzeroevaluationdeterminanth))) /\ ((mdr_c_second_nonzero_minorminornonzeroevaluationdeterminanthrc = ((mdr_a_second_nonzero_minorminornonzeroevaluationdeterminanthrc) + (mdr_b_second_nonzero_minorminornonzeroevaluationdeterminanthrc)) * S ((mdr_a_second_nonzero_minorminornonzeroevaluationdeterminanthrc) + (mdr_b_second_nonzero_minorminornonzeroevaluationdeterminanthrc)) + ((mdr_b_second_nonzero_minorminornonzeroevaluationdeterminanthrc) + (mdr_b_second_nonzero_minorminornonzeroevaluationdeterminanthrc))) /\ ((mdr_e_second_nonzero_minorminornonzeroevaluationdeterminanthrc = ((mdr_p_second_nonzero_minorminornonzeroevaluationdeterminanth) + (mdr_n_second_nonzero_minorminornonzeroevaluationdeterminanth)) * S ((mdr_p_second_nonzero_minorminornonzeroevaluationdeterminanth) + (mdr_n_second_nonzero_minorminornonzeroevaluationdeterminanth)) + ((mdr_n_second_nonzero_minorminornonzeroevaluationdeterminanth) + (mdr_n_second_nonzero_minorminornonzeroevaluationdeterminanth))) /\ ((mdr_f_second_nonzero_minorminornonzeroevaluationdeterminanthrc = ((mdr_nc_second_nonzero_minorminornonzeroevaluationdeterminanth) + (mdr_e_second_nonzero_minorminornonzeroevaluationdeterminanthrc)) * S ((mdr_nc_second_nonzero_minorminornonzeroevaluationdeterminanth) + (mdr_e_second_nonzero_minorminornonzeroevaluationdeterminanthrc)) + ((mdr_e_second_nonzero_minorminornonzeroevaluationdeterminanthrc) + (mdr_e_second_nonzero_minorminornonzeroevaluationdeterminanthrc))) /\ ((mdr_z_second_nonzero_minorminornonzeroevaluationdeterminanthr) = ((mdr_c_second_nonzero_minorminornonzeroevaluationdeterminanthrc) + (mdr_f_second_nonzero_minorminornonzeroevaluationdeterminanthrc)) * S ((mdr_c_second_nonzero_minorminornonzeroevaluationdeterminanthrc) + (mdr_f_second_nonzero_minorminornonzeroevaluationdeterminanthrc)) + ((mdr_f_second_nonzero_minorminornonzeroevaluationdeterminanthrc) + (mdr_f_second_nonzero_minorminornonzeroevaluationdeterminanthrc))))))))) /\ (((exists ff_h_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthrb. ff_h_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthrb + S (mdr_z_second_nonzero_minorminornonzeroevaluationdeterminanthr) = S ((S (mdr_i_second_nonzero_minorminornonzeroevaluationdeterminanth)) * mdr_c_second_nonzero_minorminornonzeroevaluationdeterminant)) /\ exists ff_q_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthrb. mdr_b_second_nonzero_minorminornonzeroevaluationdeterminant = ff_q_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthrb * S ((S (mdr_i_second_nonzero_minorminornonzeroevaluationdeterminanth)) * mdr_c_second_nonzero_minorminornonzeroevaluationdeterminant) + (mdr_z_second_nonzero_minorminornonzeroevaluationdeterminanthr))))) /\ (((((mdr_d_second_nonzero_minorminornonzeroevaluationdeterminanth) = 0) /\ (((mdr_p_second_nonzero_minorminornonzeroevaluationdeterminanth) = 1) /\ ((mdr_n_second_nonzero_minorminornonzeroevaluationdeterminanth) = 0))) \/ exists mdr_q_second_nonzero_minorminornonzeroevaluationdeterminanths mdr_eb_second_nonzero_minorminornonzeroevaluationdeterminanths mdr_ec_second_nonzero_minorminornonzeroevaluationdeterminanths mdr_fb_second_nonzero_minorminornonzeroevaluationdeterminanths mdr_fc_second_nonzero_minorminornonzeroevaluationdeterminanths. (((mdr_d_second_nonzero_minorminornonzeroevaluationdeterminanth) = S (mdr_q_second_nonzero_minorminornonzeroevaluationdeterminanths)) /\ ((forall mdr_j_second_nonzero_minorminornonzeroevaluationdeterminanthsc. (exists mdr_gap_second_nonzero_minorminornonzeroevaluationdeterminanthscj. mdr_gap_second_nonzero_minorminornonzeroevaluationdeterminanthscj + S (mdr_j_second_nonzero_minorminornonzeroevaluationdeterminanthsc) = (S (mdr_q_second_nonzero_minorminornonzeroevaluationdeterminanths))) -> exists mdr_i_second_nonzero_minorminornonzeroevaluationdeterminanthsc mdr_up_second_nonzero_minorminornonzeroevaluationdeterminanthsc mdr_us_second_nonzero_minorminornonzeroevaluationdeterminanthsc mdr_un_second_nonzero_minorminornonzeroevaluationdeterminanthsc mdr_ut_second_nonzero_minorminornonzeroevaluationdeterminanthsc mdr_p_second_nonzero_minorminornonzeroevaluationdeterminanthsc mdr_n_second_nonzero_minorminornonzeroevaluationdeterminanthsc. ((exists mdr_gap_second_nonzero_minorminornonzeroevaluationdeterminanthsci. mdr_gap_second_nonzero_minorminornonzeroevaluationdeterminanthsci + S (mdr_i_second_nonzero_minorminornonzeroevaluationdeterminanthsc) = (mdr_i_second_nonzero_minorminornonzeroevaluationdeterminanth)) /\ ((exists mdr_z_second_nonzero_minorminornonzeroevaluationdeterminanthscr. ((exists mdr_a_second_nonzero_minorminornonzeroevaluationdeterminanthscrc mdr_b_second_nonzero_minorminornonzeroevaluationdeterminanthscrc mdr_c_second_nonzero_minorminornonzeroevaluationdeterminanthscrc mdr_e_second_nonzero_minorminornonzeroevaluationdeterminanthscrc mdr_f_second_nonzero_minorminornonzeroevaluationdeterminanthscrc. ((mdr_a_second_nonzero_minorminornonzeroevaluationdeterminanthscrc = ((mdr_q_second_nonzero_minorminornonzeroevaluationdeterminanths) + (mdr_up_second_nonzero_minorminornonzeroevaluationdeterminanthsc)) * S ((mdr_q_second_nonzero_minorminornonzeroevaluationdeterminanths) + (mdr_up_second_nonzero_minorminornonzeroevaluationdeterminanthsc)) + ((mdr_up_second_nonzero_minorminornonzeroevaluationdeterminanthsc) + (mdr_up_second_nonzero_minorminornonzeroevaluationdeterminanthsc))) /\ ((mdr_b_second_nonzero_minorminornonzeroevaluationdeterminanthscrc = ((mdr_us_second_nonzero_minorminornonzeroevaluationdeterminanthsc) + (mdr_un_second_nonzero_minorminornonzeroevaluationdeterminanthsc)) * S ((mdr_us_second_nonzero_minorminornonzeroevaluationdeterminanthsc) + (mdr_un_second_nonzero_minorminornonzeroevaluationdeterminanthsc)) + ((mdr_un_second_nonzero_minorminornonzeroevaluationdeterminanthsc) + (mdr_un_second_nonzero_minorminornonzeroevaluationdeterminanthsc))) /\ ((mdr_c_second_nonzero_minorminornonzeroevaluationdeterminanthscrc = ((mdr_a_second_nonzero_minorminornonzeroevaluationdeterminanthscrc) + (mdr_b_second_nonzero_minorminornonzeroevaluationdeterminanthscrc)) * S ((mdr_a_second_nonzero_minorminornonzeroevaluationdeterminanthscrc) + (mdr_b_second_nonzero_minorminornonzeroevaluationdeterminanthscrc)) + ((mdr_b_second_nonzero_minorminornonzeroevaluationdeterminanthscrc) + (mdr_b_second_nonzero_minorminornonzeroevaluationdeterminanthscrc))) /\ ((mdr_e_second_nonzero_minorminornonzeroevaluationdeterminanthscrc = ((mdr_p_second_nonzero_minorminornonzeroevaluationdeterminanthsc) + (mdr_n_second_nonzero_minorminornonzeroevaluationdeterminanthsc)) * S ((mdr_p_second_nonzero_minorminornonzeroevaluationdeterminanthsc) + (mdr_n_second_nonzero_minorminornonzeroevaluationdeterminanthsc)) + ((mdr_n_second_nonzero_minorminornonzeroevaluationdeterminanthsc) + (mdr_n_second_nonzero_minorminornonzeroevaluationdeterminanthsc))) /\ ((mdr_f_second_nonzero_minorminornonzeroevaluationdeterminanthscrc = ((mdr_ut_second_nonzero_minorminornonzeroevaluationdeterminanthsc) + (mdr_e_second_nonzero_minorminornonzeroevaluationdeterminanthscrc)) * S ((mdr_ut_second_nonzero_minorminornonzeroevaluationdeterminanthsc) + (mdr_e_second_nonzero_minorminornonzeroevaluationdeterminanthscrc)) + ((mdr_e_second_nonzero_minorminornonzeroevaluationdeterminanthscrc) + (mdr_e_second_nonzero_minorminornonzeroevaluationdeterminanthscrc))) /\ ((mdr_z_second_nonzero_minorminornonzeroevaluationdeterminanthscr) = ((mdr_c_second_nonzero_minorminornonzeroevaluationdeterminanthscrc) + (mdr_f_second_nonzero_minorminornonzeroevaluationdeterminanthscrc)) * S ((mdr_c_second_nonzero_minorminornonzeroevaluationdeterminanthscrc) + (mdr_f_second_nonzero_minorminornonzeroevaluationdeterminanthscrc)) + ((mdr_f_second_nonzero_minorminornonzeroevaluationdeterminanthscrc) + (mdr_f_second_nonzero_minorminornonzeroevaluationdeterminanthscrc))))))))) /\ (((exists ff_h_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthscrb. ff_h_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthscrb + S (mdr_z_second_nonzero_minorminornonzeroevaluationdeterminanthscr) = S ((S (mdr_i_second_nonzero_minorminornonzeroevaluationdeterminanthsc)) * mdr_c_second_nonzero_minorminornonzeroevaluationdeterminant)) /\ exists ff_q_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthscrb. mdr_b_second_nonzero_minorminornonzeroevaluationdeterminant = ff_q_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthscrb * S ((S (mdr_i_second_nonzero_minorminornonzeroevaluationdeterminanthsc)) * mdr_c_second_nonzero_minorminornonzeroevaluationdeterminant) + (mdr_z_second_nonzero_minorminornonzeroevaluationdeterminanthscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthscm_positive. (exists ff_gap_mdm_lt_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthscm_positive_index_bound. ff_gap_mdm_lt_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthscm_positive) = ((mdr_q_second_nonzero_minorminornonzeroevaluationdeterminanths) * (mdr_q_second_nonzero_minorminornonzeroevaluationdeterminanths))) -> exists ff_row_mdm_prefix_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthscm_positive ff_column_mdm_prefix_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthscm_positive ff_value_mdm_prefix_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthscm_positive. (ff_index_mdm_prefix_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthscm_positive = (mdr_q_second_nonzero_minorminornonzeroevaluationdeterminanths) * ff_row_mdm_prefix_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthscm_positive + ff_column_mdm_prefix_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthscm_positive /\ ((exists ff_gap_mdm_lt_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthscm_positive_column_bound. ff_gap_mdm_lt_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthscm_positive) = (mdr_q_second_nonzero_minorminornonzeroevaluationdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthscm_positive_cell ff_column_mdm_cell_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthscm_positive_cell = ff_row_mdm_prefix_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthscm_positive_cell_row_after. ff_gap_mdm_le_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthscm_positive)) /\ ff_row_mdm_cell_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthscm_positive_cell = S ff_row_mdm_prefix_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthscm_positive) = (mdr_j_second_nonzero_minorminornonzeroevaluationdeterminanthsc)) /\ ff_column_mdm_cell_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthscm_positive_cell = ff_column_mdm_prefix_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthscm_positive_cell_column_after. ff_gap_mdm_le_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthscm_positive_cell_column_after + (mdr_j_second_nonzero_minorminornonzeroevaluationdeterminanthsc) = (ff_column_mdm_prefix_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthscm_positive)) /\ ff_column_mdm_cell_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthscm_positive_cell = S ff_column_mdm_prefix_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthscm_positive))) /\ (((exists ff_h_mdm_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthscm_positive_cell_source. ff_h_mdm_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthscm_positive) = S ((S ((ff_row_mdm_cell_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthscm_positive_cell) * (S (mdr_q_second_nonzero_minorminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthscm_positive_cell))) * mdr_pc_second_nonzero_minorminornonzeroevaluationdeterminanth)) /\ exists ff_q_mdm_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthscm_positive_cell_source. mdr_pb_second_nonzero_minorminornonzeroevaluationdeterminanth = ff_q_mdm_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthscm_positive_cell) * (S (mdr_q_second_nonzero_minorminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthscm_positive_cell))) * mdr_pc_second_nonzero_minorminornonzeroevaluationdeterminanth) + (ff_value_mdm_prefix_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthscm_positive)))))) /\ (((exists ff_h_mdm_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthscm_positive_target. ff_h_mdm_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthscm_positive_target + S (ff_value_mdm_prefix_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthscm_positive) = S ((S (ff_index_mdm_prefix_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthscm_positive)) * mdr_us_second_nonzero_minorminornonzeroevaluationdeterminanthsc)) /\ exists ff_q_mdm_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthscm_positive_target. mdr_up_second_nonzero_minorminornonzeroevaluationdeterminanthsc = ff_q_mdm_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthscm_positive)) * mdr_us_second_nonzero_minorminornonzeroevaluationdeterminanthsc) + (ff_value_mdm_prefix_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthscm_negative. (exists ff_gap_mdm_lt_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthscm_negative_index_bound. ff_gap_mdm_lt_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthscm_negative) = ((mdr_q_second_nonzero_minorminornonzeroevaluationdeterminanths) * (mdr_q_second_nonzero_minorminornonzeroevaluationdeterminanths))) -> exists ff_row_mdm_prefix_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthscm_negative ff_column_mdm_prefix_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthscm_negative ff_value_mdm_prefix_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthscm_negative. (ff_index_mdm_prefix_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthscm_negative = (mdr_q_second_nonzero_minorminornonzeroevaluationdeterminanths) * ff_row_mdm_prefix_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthscm_negative + ff_column_mdm_prefix_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthscm_negative /\ ((exists ff_gap_mdm_lt_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthscm_negative_column_bound. ff_gap_mdm_lt_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthscm_negative) = (mdr_q_second_nonzero_minorminornonzeroevaluationdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthscm_negative_cell ff_column_mdm_cell_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthscm_negative_cell = ff_row_mdm_prefix_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthscm_negative_cell_row_after. ff_gap_mdm_le_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthscm_negative)) /\ ff_row_mdm_cell_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthscm_negative_cell = S ff_row_mdm_prefix_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthscm_negative) = (mdr_j_second_nonzero_minorminornonzeroevaluationdeterminanthsc)) /\ ff_column_mdm_cell_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthscm_negative_cell = ff_column_mdm_prefix_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthscm_negative_cell_column_after. ff_gap_mdm_le_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthscm_negative_cell_column_after + (mdr_j_second_nonzero_minorminornonzeroevaluationdeterminanthsc) = (ff_column_mdm_prefix_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthscm_negative)) /\ ff_column_mdm_cell_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthscm_negative_cell = S ff_column_mdm_prefix_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthscm_negative))) /\ (((exists ff_h_mdm_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthscm_negative_cell_source. ff_h_mdm_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthscm_negative) = S ((S ((ff_row_mdm_cell_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthscm_negative_cell) * (S (mdr_q_second_nonzero_minorminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthscm_negative_cell))) * mdr_nc_second_nonzero_minorminornonzeroevaluationdeterminanth)) /\ exists ff_q_mdm_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthscm_negative_cell_source. mdr_nb_second_nonzero_minorminornonzeroevaluationdeterminanth = ff_q_mdm_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthscm_negative_cell) * (S (mdr_q_second_nonzero_minorminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthscm_negative_cell))) * mdr_nc_second_nonzero_minorminornonzeroevaluationdeterminanth) + (ff_value_mdm_prefix_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthscm_negative)))))) /\ (((exists ff_h_mdm_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthscm_negative_target. ff_h_mdm_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthscm_negative_target + S (ff_value_mdm_prefix_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthscm_negative) = S ((S (ff_index_mdm_prefix_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthscm_negative)) * mdr_ut_second_nonzero_minorminornonzeroevaluationdeterminanthsc)) /\ exists ff_q_mdm_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthscm_negative_target. mdr_un_second_nonzero_minorminornonzeroevaluationdeterminanthsc = ff_q_mdm_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthscm_negative)) * mdr_ut_second_nonzero_minorminornonzeroevaluationdeterminanthsc) + (ff_value_mdm_prefix_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthscm_negative))))))))) /\ ((((exists ff_h_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthscp. ff_h_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthscp + S (mdr_p_second_nonzero_minorminornonzeroevaluationdeterminanthsc) = S ((S (mdr_j_second_nonzero_minorminornonzeroevaluationdeterminanthsc)) * mdr_ec_second_nonzero_minorminornonzeroevaluationdeterminanths)) /\ exists ff_q_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthscp. mdr_eb_second_nonzero_minorminornonzeroevaluationdeterminanths = ff_q_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthscp * S ((S (mdr_j_second_nonzero_minorminornonzeroevaluationdeterminanthsc)) * mdr_ec_second_nonzero_minorminornonzeroevaluationdeterminanths) + (mdr_p_second_nonzero_minorminornonzeroevaluationdeterminanthsc))) /\ (((exists ff_h_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthscn. ff_h_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthscn + S (mdr_n_second_nonzero_minorminornonzeroevaluationdeterminanthsc) = S ((S (mdr_j_second_nonzero_minorminornonzeroevaluationdeterminanthsc)) * mdr_fc_second_nonzero_minorminornonzeroevaluationdeterminanths)) /\ exists ff_q_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthscn. mdr_fb_second_nonzero_minorminornonzeroevaluationdeterminanths = ff_q_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthscn * S ((S (mdr_j_second_nonzero_minorminornonzeroevaluationdeterminanthsc)) * mdr_fc_second_nonzero_minorminornonzeroevaluationdeterminanths) + (mdr_n_second_nonzero_minorminornonzeroevaluationdeterminanthsc)))))))) /\ (exists ff_ub_mce_fold_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf ff_uc_mce_fold_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf ff_vb_mce_fold_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf ff_vc_mce_fold_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf. ((forall ff_index_mce_alternating_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix. (exists ff_gap_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix_index. ff_gap_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix_index + S (ff_index_mce_alternating_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix) = (S (mdr_q_second_nonzero_minorminornonzeroevaluationdeterminanths))) -> exists ff_ap_mce_alternating_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix ff_an_mce_alternating_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix ff_bp_mce_alternating_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix ff_bn_mce_alternating_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix ff_p_mce_alternating_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix ff_n_mce_alternating_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix. ((((exists ff_h_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix_ap. ff_h_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix_ap + S (ff_ap_mce_alternating_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix)) * mdr_pc_second_nonzero_minorminornonzeroevaluationdeterminanth)) /\ exists ff_q_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix_ap. mdr_pb_second_nonzero_minorminornonzeroevaluationdeterminanth = ff_q_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix)) * mdr_pc_second_nonzero_minorminornonzeroevaluationdeterminanth) + (ff_ap_mce_alternating_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix_an. ff_h_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix_an + S (ff_an_mce_alternating_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix)) * mdr_nc_second_nonzero_minorminornonzeroevaluationdeterminanth)) /\ exists ff_q_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix_an. mdr_nb_second_nonzero_minorminornonzeroevaluationdeterminanth = ff_q_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix)) * mdr_nc_second_nonzero_minorminornonzeroevaluationdeterminanth) + (ff_an_mce_alternating_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix_bp. ff_h_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix_bp + S (ff_bp_mce_alternating_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix)) * mdr_ec_second_nonzero_minorminornonzeroevaluationdeterminanths)) /\ exists ff_q_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix_bp. mdr_eb_second_nonzero_minorminornonzeroevaluationdeterminanths = ff_q_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix)) * mdr_ec_second_nonzero_minorminornonzeroevaluationdeterminanths) + (ff_bp_mce_alternating_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix_bn. ff_h_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix_bn + S (ff_bn_mce_alternating_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix)) * mdr_fc_second_nonzero_minorminornonzeroevaluationdeterminanths)) /\ exists ff_q_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix_bn. mdr_fb_second_nonzero_minorminornonzeroevaluationdeterminanths = ff_q_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix)) * mdr_fc_second_nonzero_minorminornonzeroevaluationdeterminanths) + (ff_bn_mce_alternating_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix_positive. ff_h_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix_positive + S (ff_p_mce_alternating_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix_positive. ff_ub_mce_fold_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf) + (ff_p_mce_alternating_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix_negative. ff_h_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix_negative + S (ff_n_mce_alternating_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix_negative. ff_vb_mce_fold_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf) + (ff_n_mce_alternating_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix))) /\ (((exists ff_even_mce_term_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix = 2 * ff_even_mce_term_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix_term) /\ (ff_p_mce_alternating_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix = 2 * ff_odd_mce_term_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_positive ff_v_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_positive. ((((exists ff_h_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_positive_start. ff_h_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_positive_start. ff_u_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_positive_start * S ((S (0)) * ff_v_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_positive_terminal. ff_h_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_positive_terminal + S (mdr_p_second_nonzero_minorminornonzeroevaluationdeterminanth) = S ((S ((S (mdr_q_second_nonzero_minorminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_positive_terminal. ff_u_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_positive_terminal * S ((S ((S (mdr_q_second_nonzero_minorminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_positive) + (mdr_p_second_nonzero_minorminornonzeroevaluationdeterminanth))) /\ forall ff_i_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_positive. (exists ff_lt_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_positive_bound. ff_lt_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_positive_bound + S ff_i_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_positive = (S (mdr_q_second_nonzero_minorminornonzeroevaluationdeterminanths))) -> exists ff_a_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_positive ff_r_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_positive ff_s_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_positive. ((((exists ff_h_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_positive_summand. ff_h_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_positive_summand + S (ff_a_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_positive_summand. ff_ub_mce_fold_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_positive_summand * S ((S (ff_i_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf) + (ff_a_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_positive_partial. ff_h_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_positive_partial + S (ff_r_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_positive_partial. ff_u_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_positive_partial * S ((S (ff_i_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_positive) + (ff_r_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_positive_successor. ff_h_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_positive_successor + S (ff_s_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_positive) = S ((S (S ff_i_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_positive_successor. ff_u_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_positive_successor * S ((S (S ff_i_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_positive) + (ff_s_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_positive))) /\ ff_s_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_positive = ff_r_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_positive + ff_a_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_positive)))))) /\ (exists ff_u_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_negative ff_v_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_negative. ((((exists ff_h_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_negative_start. ff_h_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_negative_start. ff_u_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_negative_start * S ((S (0)) * ff_v_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_negative_terminal. ff_h_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_negative_terminal + S (mdr_n_second_nonzero_minorminornonzeroevaluationdeterminanth) = S ((S ((S (mdr_q_second_nonzero_minorminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_negative_terminal. ff_u_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_negative_terminal * S ((S ((S (mdr_q_second_nonzero_minorminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_negative) + (mdr_n_second_nonzero_minorminornonzeroevaluationdeterminanth))) /\ forall ff_i_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_negative. (exists ff_lt_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_negative_bound. ff_lt_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_negative_bound + S ff_i_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_negative = (S (mdr_q_second_nonzero_minorminornonzeroevaluationdeterminanths))) -> exists ff_a_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_negative ff_r_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_negative ff_s_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_negative. ((((exists ff_h_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_negative_summand. ff_h_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_negative_summand + S (ff_a_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_negative_summand. ff_vb_mce_fold_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_negative_summand * S ((S (ff_i_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf) + (ff_a_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_negative_partial. ff_h_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_negative_partial + S (ff_r_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_negative_partial. ff_u_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_negative_partial * S ((S (ff_i_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_negative) + (ff_r_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_negative_successor. ff_h_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_negative_successor + S (ff_s_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_negative) = S ((S (S ff_i_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_negative_successor. ff_u_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_negative_successor * S ((S (S ff_i_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_negative) + (ff_s_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_negative))) /\ ff_s_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_negative = ff_r_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_negative + ff_a_mce_mdr_second_nonzero_minorminornonzeroevaluationdeterminanthsf_negative))))))))))))))) /\ ((exists mdr_gap_second_nonzero_minorminornonzeroevaluationdeterminanti. mdr_gap_second_nonzero_minorminornonzeroevaluationdeterminanti + S (mdr_i_second_nonzero_minorminornonzeroevaluationdeterminant) = (mdr_l_second_nonzero_minorminornonzeroevaluationdeterminant)) /\ (exists mdr_z_second_nonzero_minorminornonzeroevaluationdeterminantr. ((exists mdr_a_second_nonzero_minorminornonzeroevaluationdeterminantrc mdr_b_second_nonzero_minorminornonzeroevaluationdeterminantrc mdr_c_second_nonzero_minorminornonzeroevaluationdeterminantrc mdr_e_second_nonzero_minorminornonzeroevaluationdeterminantrc mdr_f_second_nonzero_minorminornonzeroevaluationdeterminantrc. ((mdr_a_second_nonzero_minorminornonzeroevaluationdeterminantrc = ((q) + (mdr_ub_second_nonzero_minorminornonzeroevaluation)) * S ((q) + (mdr_ub_second_nonzero_minorminornonzeroevaluation)) + ((mdr_ub_second_nonzero_minorminornonzeroevaluation) + (mdr_ub_second_nonzero_minorminornonzeroevaluation))) /\ ((mdr_b_second_nonzero_minorminornonzeroevaluationdeterminantrc = ((mdr_uc_second_nonzero_minorminornonzeroevaluation) + (mdr_vb_second_nonzero_minorminornonzeroevaluation)) * S ((mdr_uc_second_nonzero_minorminornonzeroevaluation) + (mdr_vb_second_nonzero_minorminornonzeroevaluation)) + ((mdr_vb_second_nonzero_minorminornonzeroevaluation) + (mdr_vb_second_nonzero_minorminornonzeroevaluation))) /\ ((mdr_c_second_nonzero_minorminornonzeroevaluationdeterminantrc = ((mdr_a_second_nonzero_minorminornonzeroevaluationdeterminantrc) + (mdr_b_second_nonzero_minorminornonzeroevaluationdeterminantrc)) * S ((mdr_a_second_nonzero_minorminornonzeroevaluationdeterminantrc) + (mdr_b_second_nonzero_minorminornonzeroevaluationdeterminantrc)) + ((mdr_b_second_nonzero_minorminornonzeroevaluationdeterminantrc) + (mdr_b_second_nonzero_minorminornonzeroevaluationdeterminantrc))) /\ ((mdr_e_second_nonzero_minorminornonzeroevaluationdeterminantrc = ((mdr_p_second_nonzero_minorminornonzero) + (mdr_n_second_nonzero_minorminornonzero)) * S ((mdr_p_second_nonzero_minorminornonzero) + (mdr_n_second_nonzero_minorminornonzero)) + ((mdr_n_second_nonzero_minorminornonzero) + (mdr_n_second_nonzero_minorminornonzero))) /\ ((mdr_f_second_nonzero_minorminornonzeroevaluationdeterminantrc = ((mdr_vc_second_nonzero_minorminornonzeroevaluation) + (mdr_e_second_nonzero_minorminornonzeroevaluationdeterminantrc)) * S ((mdr_vc_second_nonzero_minorminornonzeroevaluation) + (mdr_e_second_nonzero_minorminornonzeroevaluationdeterminantrc)) + ((mdr_e_second_nonzero_minorminornonzeroevaluationdeterminantrc) + (mdr_e_second_nonzero_minorminornonzeroevaluationdeterminantrc))) /\ ((mdr_z_second_nonzero_minorminornonzeroevaluationdeterminantr) = ((mdr_c_second_nonzero_minorminornonzeroevaluationdeterminantrc) + (mdr_f_second_nonzero_minorminornonzeroevaluationdeterminantrc)) * S ((mdr_c_second_nonzero_minorminornonzeroevaluationdeterminantrc) + (mdr_f_second_nonzero_minorminornonzeroevaluationdeterminantrc)) + ((mdr_f_second_nonzero_minorminornonzeroevaluationdeterminantrc) + (mdr_f_second_nonzero_minorminornonzeroevaluationdeterminantrc))))))))) /\ (((exists ff_h_mdr_second_nonzero_minorminornonzeroevaluationdeterminantrb. ff_h_mdr_second_nonzero_minorminornonzeroevaluationdeterminantrb + S (mdr_z_second_nonzero_minorminornonzeroevaluationdeterminantr) = S ((S (mdr_i_second_nonzero_minorminornonzeroevaluationdeterminant)) * mdr_c_second_nonzero_minorminornonzeroevaluationdeterminant)) /\ exists ff_q_mdr_second_nonzero_minorminornonzeroevaluationdeterminantrb. mdr_b_second_nonzero_minorminornonzeroevaluationdeterminant = ff_q_mdr_second_nonzero_minorminornonzeroevaluationdeterminantrb * S ((S (mdr_i_second_nonzero_minorminornonzeroevaluationdeterminant)) * mdr_c_second_nonzero_minorminornonzeroevaluationdeterminant) + (mdr_z_second_nonzero_minorminornonzeroevaluationdeterminantr)))))))))) /\ (~(mdr_p_second_nonzero_minorminornonzero = mdr_n_second_nonzero_minorminornonzero))))))))