matrix_integer_all_minors_zero_transport

Exact expanded first-order arithmetic statement

forall ab ac bb bc eb ec fb fc r w q. (forall ics_index_zero_parent_equality ics_value0_zero_parent_equality ics_value1_zero_parent_equality ics_value2_zero_parent_equality ics_value3_zero_parent_equality. (exists ics_gap_zero_parent_equality_bound. ics_gap_zero_parent_equality_bound + S (ics_index_zero_parent_equality) = ((r) * (w))) -> (((exists fs_h_ics_zero_parent_equality_at0. fs_h_ics_zero_parent_equality_at0 + S (ics_value0_zero_parent_equality) = S ((S (ics_index_zero_parent_equality)) * ac)) /\ exists fs_q_ics_zero_parent_equality_at0. ab = fs_q_ics_zero_parent_equality_at0 * S ((S (ics_index_zero_parent_equality)) * ac) + (ics_value0_zero_parent_equality))) -> (((exists fs_h_ics_zero_parent_equality_at1. fs_h_ics_zero_parent_equality_at1 + S (ics_value1_zero_parent_equality) = S ((S (ics_index_zero_parent_equality)) * bc)) /\ exists fs_q_ics_zero_parent_equality_at1. bb = fs_q_ics_zero_parent_equality_at1 * S ((S (ics_index_zero_parent_equality)) * bc) + (ics_value1_zero_parent_equality))) -> (((exists fs_h_ics_zero_parent_equality_at2. fs_h_ics_zero_parent_equality_at2 + S (ics_value2_zero_parent_equality) = S ((S (ics_index_zero_parent_equality)) * ec)) /\ exists fs_q_ics_zero_parent_equality_at2. eb = fs_q_ics_zero_parent_equality_at2 * S ((S (ics_index_zero_parent_equality)) * ec) + (ics_value2_zero_parent_equality))) -> (((exists fs_h_ics_zero_parent_equality_at3. fs_h_ics_zero_parent_equality_at3 + S (ics_value3_zero_parent_equality) = S ((S (ics_index_zero_parent_equality)) * fc)) /\ exists fs_q_ics_zero_parent_equality_at3. fb = fs_q_ics_zero_parent_equality_at3 * S ((S (ics_index_zero_parent_equality)) * fc) + (ics_value3_zero_parent_equality))) -> ics_value0_zero_parent_equality + ics_value3_zero_parent_equality = ics_value2_zero_parent_equality + ics_value1_zero_parent_equality) -> (forall mdr_rb_first_zero_minors mdr_rc_first_zero_minors mdr_cb_first_zero_minors mdr_cc_first_zero_minors mdr_p_first_zero_minors mdr_n_first_zero_minors. (((forall fom_index_mrf_first_zero_minorsrowsbound. (exists fom_gap_mrf_first_zero_minorsrowsbound_index_bound. fom_gap_mrf_first_zero_minorsrowsbound_index_bound + S (fom_index_mrf_first_zero_minorsrowsbound) = q) -> exists fom_value_mrf_first_zero_minorsrowsbound. ((((exists fom_beta_height_mrf_first_zero_minorsrowsbound_entry. fom_beta_height_mrf_first_zero_minorsrowsbound_entry + S (fom_value_mrf_first_zero_minorsrowsbound) = S ((S (fom_index_mrf_first_zero_minorsrowsbound)) * mdr_rc_first_zero_minors)) /\ exists fom_beta_quotient_mrf_first_zero_minorsrowsbound_entry. mdr_rb_first_zero_minors = fom_beta_quotient_mrf_first_zero_minorsrowsbound_entry * S ((S (fom_index_mrf_first_zero_minorsrowsbound)) * mdr_rc_first_zero_minors) + (fom_value_mrf_first_zero_minorsrowsbound))) /\ (exists fom_gap_mrf_first_zero_minorsrowsbound_value_bound. fom_gap_mrf_first_zero_minorsrowsbound_value_bound + S (fom_value_mrf_first_zero_minorsrowsbound) = r))) /\ (forall mdr_i_first_zero_minorsrowsdistinct mdr_j_first_zero_minorsrowsdistinct mdr_a_first_zero_minorsrowsdistinct. (exists mdr_gap_first_zero_minorsrowsdistincti. mdr_gap_first_zero_minorsrowsdistincti + S (mdr_i_first_zero_minorsrowsdistinct) = (q)) -> (exists mdr_gap_first_zero_minorsrowsdistinctj. mdr_gap_first_zero_minorsrowsdistinctj + S (mdr_j_first_zero_minorsrowsdistinct) = (q)) -> (((exists ff_h_mdr_first_zero_minorsrowsdistinctfirst. ff_h_mdr_first_zero_minorsrowsdistinctfirst + S (mdr_a_first_zero_minorsrowsdistinct) = S ((S (mdr_i_first_zero_minorsrowsdistinct)) * mdr_rc_first_zero_minors)) /\ exists ff_q_mdr_first_zero_minorsrowsdistinctfirst. mdr_rb_first_zero_minors = ff_q_mdr_first_zero_minorsrowsdistinctfirst * S ((S (mdr_i_first_zero_minorsrowsdistinct)) * mdr_rc_first_zero_minors) + (mdr_a_first_zero_minorsrowsdistinct))) -> (((exists ff_h_mdr_first_zero_minorsrowsdistinctsecond. ff_h_mdr_first_zero_minorsrowsdistinctsecond + S (mdr_a_first_zero_minorsrowsdistinct) = S ((S (mdr_j_first_zero_minorsrowsdistinct)) * mdr_rc_first_zero_minors)) /\ exists ff_q_mdr_first_zero_minorsrowsdistinctsecond. mdr_rb_first_zero_minors = ff_q_mdr_first_zero_minorsrowsdistinctsecond * S ((S (mdr_j_first_zero_minorsrowsdistinct)) * mdr_rc_first_zero_minors) + (mdr_a_first_zero_minorsrowsdistinct))) -> mdr_i_first_zero_minorsrowsdistinct = mdr_j_first_zero_minorsrowsdistinct))) -> (((forall fom_index_mrf_first_zero_minorscolumnsbound. (exists fom_gap_mrf_first_zero_minorscolumnsbound_index_bound. fom_gap_mrf_first_zero_minorscolumnsbound_index_bound + S (fom_index_mrf_first_zero_minorscolumnsbound) = q) -> exists fom_value_mrf_first_zero_minorscolumnsbound. ((((exists fom_beta_height_mrf_first_zero_minorscolumnsbound_entry. fom_beta_height_mrf_first_zero_minorscolumnsbound_entry + S (fom_value_mrf_first_zero_minorscolumnsbound) = S ((S (fom_index_mrf_first_zero_minorscolumnsbound)) * mdr_cc_first_zero_minors)) /\ exists fom_beta_quotient_mrf_first_zero_minorscolumnsbound_entry. mdr_cb_first_zero_minors = fom_beta_quotient_mrf_first_zero_minorscolumnsbound_entry * S ((S (fom_index_mrf_first_zero_minorscolumnsbound)) * mdr_cc_first_zero_minors) + (fom_value_mrf_first_zero_minorscolumnsbound))) /\ (exists fom_gap_mrf_first_zero_minorscolumnsbound_value_bound. fom_gap_mrf_first_zero_minorscolumnsbound_value_bound + S (fom_value_mrf_first_zero_minorscolumnsbound) = w))) /\ (forall mdr_i_first_zero_minorscolumnsdistinct mdr_j_first_zero_minorscolumnsdistinct mdr_a_first_zero_minorscolumnsdistinct. (exists mdr_gap_first_zero_minorscolumnsdistincti. mdr_gap_first_zero_minorscolumnsdistincti + S (mdr_i_first_zero_minorscolumnsdistinct) = (q)) -> (exists mdr_gap_first_zero_minorscolumnsdistinctj. mdr_gap_first_zero_minorscolumnsdistinctj + S (mdr_j_first_zero_minorscolumnsdistinct) = (q)) -> (((exists ff_h_mdr_first_zero_minorscolumnsdistinctfirst. ff_h_mdr_first_zero_minorscolumnsdistinctfirst + S (mdr_a_first_zero_minorscolumnsdistinct) = S ((S (mdr_i_first_zero_minorscolumnsdistinct)) * mdr_cc_first_zero_minors)) /\ exists ff_q_mdr_first_zero_minorscolumnsdistinctfirst. mdr_cb_first_zero_minors = ff_q_mdr_first_zero_minorscolumnsdistinctfirst * S ((S (mdr_i_first_zero_minorscolumnsdistinct)) * mdr_cc_first_zero_minors) + (mdr_a_first_zero_minorscolumnsdistinct))) -> (((exists ff_h_mdr_first_zero_minorscolumnsdistinctsecond. ff_h_mdr_first_zero_minorscolumnsdistinctsecond + S (mdr_a_first_zero_minorscolumnsdistinct) = S ((S (mdr_j_first_zero_minorscolumnsdistinct)) * mdr_cc_first_zero_minors)) /\ exists ff_q_mdr_first_zero_minorscolumnsdistinctsecond. mdr_cb_first_zero_minors = ff_q_mdr_first_zero_minorscolumnsdistinctsecond * S ((S (mdr_j_first_zero_minorscolumnsdistinct)) * mdr_cc_first_zero_minors) + (mdr_a_first_zero_minorscolumnsdistinct))) -> mdr_i_first_zero_minorscolumnsdistinct = mdr_j_first_zero_minorscolumnsdistinct))) -> (exists mdr_ub_first_zero_minorsevaluation mdr_uc_first_zero_minorsevaluation mdr_vb_first_zero_minorsevaluation mdr_vc_first_zero_minorsevaluation. ((((forall mdr_i_first_zero_minorsevaluationmatrixpositive. (exists mdr_gap_first_zero_minorsevaluationmatrixpositivebound. mdr_gap_first_zero_minorsevaluationmatrixpositivebound + S (mdr_i_first_zero_minorsevaluationmatrixpositive) = ((q) * (q))) -> exists mdr_a_first_zero_minorsevaluationmatrixpositive. (((exists mdr_r_first_zero_minorsevaluationmatrixpositivepoint mdr_s_first_zero_minorsevaluationmatrixpositivepoint mdr_u_first_zero_minorsevaluationmatrixpositivepoint mdr_v_first_zero_minorsevaluationmatrixpositivepoint. ((mdr_i_first_zero_minorsevaluationmatrixpositive = (q) * mdr_r_first_zero_minorsevaluationmatrixpositivepoint + mdr_s_first_zero_minorsevaluationmatrixpositivepoint) /\ ((exists mdr_gap_first_zero_minorsevaluationmatrixpositivepointcolumn. mdr_gap_first_zero_minorsevaluationmatrixpositivepointcolumn + S (mdr_s_first_zero_minorsevaluationmatrixpositivepoint) = (q)) /\ ((((exists ff_h_mdr_first_zero_minorsevaluationmatrixpositivepointrow_index. ff_h_mdr_first_zero_minorsevaluationmatrixpositivepointrow_index + S (mdr_u_first_zero_minorsevaluationmatrixpositivepoint) = S ((S (mdr_r_first_zero_minorsevaluationmatrixpositivepoint)) * mdr_rc_first_zero_minors)) /\ exists ff_q_mdr_first_zero_minorsevaluationmatrixpositivepointrow_index. mdr_rb_first_zero_minors = ff_q_mdr_first_zero_minorsevaluationmatrixpositivepointrow_index * S ((S (mdr_r_first_zero_minorsevaluationmatrixpositivepoint)) * mdr_rc_first_zero_minors) + (mdr_u_first_zero_minorsevaluationmatrixpositivepoint))) /\ ((((exists ff_h_mdr_first_zero_minorsevaluationmatrixpositivepointcolumn_index. ff_h_mdr_first_zero_minorsevaluationmatrixpositivepointcolumn_index + S (mdr_v_first_zero_minorsevaluationmatrixpositivepoint) = S ((S (mdr_s_first_zero_minorsevaluationmatrixpositivepoint)) * mdr_cc_first_zero_minors)) /\ exists ff_q_mdr_first_zero_minorsevaluationmatrixpositivepointcolumn_index. mdr_cb_first_zero_minors = ff_q_mdr_first_zero_minorsevaluationmatrixpositivepointcolumn_index * S ((S (mdr_s_first_zero_minorsevaluationmatrixpositivepoint)) * mdr_cc_first_zero_minors) + (mdr_v_first_zero_minorsevaluationmatrixpositivepoint))) /\ (((exists ff_h_mdr_first_zero_minorsevaluationmatrixpositivepointsource. ff_h_mdr_first_zero_minorsevaluationmatrixpositivepointsource + S (mdr_a_first_zero_minorsevaluationmatrixpositive) = S ((S ((mdr_u_first_zero_minorsevaluationmatrixpositivepoint) * (w) + (mdr_v_first_zero_minorsevaluationmatrixpositivepoint))) * ac)) /\ exists ff_q_mdr_first_zero_minorsevaluationmatrixpositivepointsource. ab = ff_q_mdr_first_zero_minorsevaluationmatrixpositivepointsource * S ((S ((mdr_u_first_zero_minorsevaluationmatrixpositivepoint) * (w) + (mdr_v_first_zero_minorsevaluationmatrixpositivepoint))) * ac) + (mdr_a_first_zero_minorsevaluationmatrixpositive)))))))) /\ (((exists ff_h_mdr_first_zero_minorsevaluationmatrixpositiveoutput. ff_h_mdr_first_zero_minorsevaluationmatrixpositiveoutput + S (mdr_a_first_zero_minorsevaluationmatrixpositive) = S ((S (mdr_i_first_zero_minorsevaluationmatrixpositive)) * mdr_uc_first_zero_minorsevaluation)) /\ exists ff_q_mdr_first_zero_minorsevaluationmatrixpositiveoutput. mdr_ub_first_zero_minorsevaluation = ff_q_mdr_first_zero_minorsevaluationmatrixpositiveoutput * S ((S (mdr_i_first_zero_minorsevaluationmatrixpositive)) * mdr_uc_first_zero_minorsevaluation) + (mdr_a_first_zero_minorsevaluationmatrixpositive)))))) /\ (forall mdr_i_first_zero_minorsevaluationmatrixnegative. (exists mdr_gap_first_zero_minorsevaluationmatrixnegativebound. mdr_gap_first_zero_minorsevaluationmatrixnegativebound + S (mdr_i_first_zero_minorsevaluationmatrixnegative) = ((q) * (q))) -> exists mdr_a_first_zero_minorsevaluationmatrixnegative. (((exists mdr_r_first_zero_minorsevaluationmatrixnegativepoint mdr_s_first_zero_minorsevaluationmatrixnegativepoint mdr_u_first_zero_minorsevaluationmatrixnegativepoint mdr_v_first_zero_minorsevaluationmatrixnegativepoint. ((mdr_i_first_zero_minorsevaluationmatrixnegative = (q) * mdr_r_first_zero_minorsevaluationmatrixnegativepoint + mdr_s_first_zero_minorsevaluationmatrixnegativepoint) /\ ((exists mdr_gap_first_zero_minorsevaluationmatrixnegativepointcolumn. mdr_gap_first_zero_minorsevaluationmatrixnegativepointcolumn + S (mdr_s_first_zero_minorsevaluationmatrixnegativepoint) = (q)) /\ ((((exists ff_h_mdr_first_zero_minorsevaluationmatrixnegativepointrow_index. ff_h_mdr_first_zero_minorsevaluationmatrixnegativepointrow_index + S (mdr_u_first_zero_minorsevaluationmatrixnegativepoint) = S ((S (mdr_r_first_zero_minorsevaluationmatrixnegativepoint)) * mdr_rc_first_zero_minors)) /\ exists ff_q_mdr_first_zero_minorsevaluationmatrixnegativepointrow_index. mdr_rb_first_zero_minors = ff_q_mdr_first_zero_minorsevaluationmatrixnegativepointrow_index * S ((S (mdr_r_first_zero_minorsevaluationmatrixnegativepoint)) * mdr_rc_first_zero_minors) + (mdr_u_first_zero_minorsevaluationmatrixnegativepoint))) /\ ((((exists ff_h_mdr_first_zero_minorsevaluationmatrixnegativepointcolumn_index. ff_h_mdr_first_zero_minorsevaluationmatrixnegativepointcolumn_index + S (mdr_v_first_zero_minorsevaluationmatrixnegativepoint) = S ((S (mdr_s_first_zero_minorsevaluationmatrixnegativepoint)) * mdr_cc_first_zero_minors)) /\ exists ff_q_mdr_first_zero_minorsevaluationmatrixnegativepointcolumn_index. mdr_cb_first_zero_minors = ff_q_mdr_first_zero_minorsevaluationmatrixnegativepointcolumn_index * S ((S (mdr_s_first_zero_minorsevaluationmatrixnegativepoint)) * mdr_cc_first_zero_minors) + (mdr_v_first_zero_minorsevaluationmatrixnegativepoint))) /\ (((exists ff_h_mdr_first_zero_minorsevaluationmatrixnegativepointsource. ff_h_mdr_first_zero_minorsevaluationmatrixnegativepointsource + S (mdr_a_first_zero_minorsevaluationmatrixnegative) = S ((S ((mdr_u_first_zero_minorsevaluationmatrixnegativepoint) * (w) + (mdr_v_first_zero_minorsevaluationmatrixnegativepoint))) * bc)) /\ exists ff_q_mdr_first_zero_minorsevaluationmatrixnegativepointsource. bb = ff_q_mdr_first_zero_minorsevaluationmatrixnegativepointsource * S ((S ((mdr_u_first_zero_minorsevaluationmatrixnegativepoint) * (w) + (mdr_v_first_zero_minorsevaluationmatrixnegativepoint))) * bc) + (mdr_a_first_zero_minorsevaluationmatrixnegative)))))))) /\ (((exists ff_h_mdr_first_zero_minorsevaluationmatrixnegativeoutput. ff_h_mdr_first_zero_minorsevaluationmatrixnegativeoutput + S (mdr_a_first_zero_minorsevaluationmatrixnegative) = S ((S (mdr_i_first_zero_minorsevaluationmatrixnegative)) * mdr_vc_first_zero_minorsevaluation)) /\ exists ff_q_mdr_first_zero_minorsevaluationmatrixnegativeoutput. mdr_vb_first_zero_minorsevaluation = ff_q_mdr_first_zero_minorsevaluationmatrixnegativeoutput * S ((S (mdr_i_first_zero_minorsevaluationmatrixnegative)) * mdr_vc_first_zero_minorsevaluation) + (mdr_a_first_zero_minorsevaluationmatrixnegative)))))))) /\ (exists mdr_b_first_zero_minorsevaluationdeterminant mdr_c_first_zero_minorsevaluationdeterminant mdr_l_first_zero_minorsevaluationdeterminant mdr_i_first_zero_minorsevaluationdeterminant. ((forall mdr_i_first_zero_minorsevaluationdeterminanth. (exists mdr_gap_first_zero_minorsevaluationdeterminanthi. mdr_gap_first_zero_minorsevaluationdeterminanthi + S (mdr_i_first_zero_minorsevaluationdeterminanth) = (mdr_l_first_zero_minorsevaluationdeterminant)) -> exists mdr_d_first_zero_minorsevaluationdeterminanth mdr_pb_first_zero_minorsevaluationdeterminanth mdr_pc_first_zero_minorsevaluationdeterminanth mdr_nb_first_zero_minorsevaluationdeterminanth mdr_nc_first_zero_minorsevaluationdeterminanth mdr_p_first_zero_minorsevaluationdeterminanth mdr_n_first_zero_minorsevaluationdeterminanth. ((exists mdr_z_first_zero_minorsevaluationdeterminanthr. ((exists mdr_a_first_zero_minorsevaluationdeterminanthrc mdr_b_first_zero_minorsevaluationdeterminanthrc mdr_c_first_zero_minorsevaluationdeterminanthrc mdr_e_first_zero_minorsevaluationdeterminanthrc mdr_f_first_zero_minorsevaluationdeterminanthrc. ((mdr_a_first_zero_minorsevaluationdeterminanthrc = ((mdr_d_first_zero_minorsevaluationdeterminanth) + (mdr_pb_first_zero_minorsevaluationdeterminanth)) * S ((mdr_d_first_zero_minorsevaluationdeterminanth) + (mdr_pb_first_zero_minorsevaluationdeterminanth)) + ((mdr_pb_first_zero_minorsevaluationdeterminanth) + (mdr_pb_first_zero_minorsevaluationdeterminanth))) /\ ((mdr_b_first_zero_minorsevaluationdeterminanthrc = ((mdr_pc_first_zero_minorsevaluationdeterminanth) + (mdr_nb_first_zero_minorsevaluationdeterminanth)) * S ((mdr_pc_first_zero_minorsevaluationdeterminanth) + (mdr_nb_first_zero_minorsevaluationdeterminanth)) + ((mdr_nb_first_zero_minorsevaluationdeterminanth) + (mdr_nb_first_zero_minorsevaluationdeterminanth))) /\ ((mdr_c_first_zero_minorsevaluationdeterminanthrc = ((mdr_a_first_zero_minorsevaluationdeterminanthrc) + (mdr_b_first_zero_minorsevaluationdeterminanthrc)) * S ((mdr_a_first_zero_minorsevaluationdeterminanthrc) + (mdr_b_first_zero_minorsevaluationdeterminanthrc)) + ((mdr_b_first_zero_minorsevaluationdeterminanthrc) + (mdr_b_first_zero_minorsevaluationdeterminanthrc))) /\ ((mdr_e_first_zero_minorsevaluationdeterminanthrc = ((mdr_p_first_zero_minorsevaluationdeterminanth) + (mdr_n_first_zero_minorsevaluationdeterminanth)) * S ((mdr_p_first_zero_minorsevaluationdeterminanth) + (mdr_n_first_zero_minorsevaluationdeterminanth)) + ((mdr_n_first_zero_minorsevaluationdeterminanth) + (mdr_n_first_zero_minorsevaluationdeterminanth))) /\ ((mdr_f_first_zero_minorsevaluationdeterminanthrc = ((mdr_nc_first_zero_minorsevaluationdeterminanth) + (mdr_e_first_zero_minorsevaluationdeterminanthrc)) * S ((mdr_nc_first_zero_minorsevaluationdeterminanth) + (mdr_e_first_zero_minorsevaluationdeterminanthrc)) + ((mdr_e_first_zero_minorsevaluationdeterminanthrc) + (mdr_e_first_zero_minorsevaluationdeterminanthrc))) /\ ((mdr_z_first_zero_minorsevaluationdeterminanthr) = ((mdr_c_first_zero_minorsevaluationdeterminanthrc) + (mdr_f_first_zero_minorsevaluationdeterminanthrc)) * S ((mdr_c_first_zero_minorsevaluationdeterminanthrc) + (mdr_f_first_zero_minorsevaluationdeterminanthrc)) + ((mdr_f_first_zero_minorsevaluationdeterminanthrc) + (mdr_f_first_zero_minorsevaluationdeterminanthrc))))))))) /\ (((exists ff_h_mdr_first_zero_minorsevaluationdeterminanthrb. ff_h_mdr_first_zero_minorsevaluationdeterminanthrb + S (mdr_z_first_zero_minorsevaluationdeterminanthr) = S ((S (mdr_i_first_zero_minorsevaluationdeterminanth)) * mdr_c_first_zero_minorsevaluationdeterminant)) /\ exists ff_q_mdr_first_zero_minorsevaluationdeterminanthrb. mdr_b_first_zero_minorsevaluationdeterminant = ff_q_mdr_first_zero_minorsevaluationdeterminanthrb * S ((S (mdr_i_first_zero_minorsevaluationdeterminanth)) * mdr_c_first_zero_minorsevaluationdeterminant) + (mdr_z_first_zero_minorsevaluationdeterminanthr))))) /\ (((((mdr_d_first_zero_minorsevaluationdeterminanth) = 0) /\ (((mdr_p_first_zero_minorsevaluationdeterminanth) = 1) /\ ((mdr_n_first_zero_minorsevaluationdeterminanth) = 0))) \/ exists mdr_q_first_zero_minorsevaluationdeterminanths mdr_eb_first_zero_minorsevaluationdeterminanths mdr_ec_first_zero_minorsevaluationdeterminanths mdr_fb_first_zero_minorsevaluationdeterminanths mdr_fc_first_zero_minorsevaluationdeterminanths. (((mdr_d_first_zero_minorsevaluationdeterminanth) = S (mdr_q_first_zero_minorsevaluationdeterminanths)) /\ ((forall mdr_j_first_zero_minorsevaluationdeterminanthsc. (exists mdr_gap_first_zero_minorsevaluationdeterminanthscj. mdr_gap_first_zero_minorsevaluationdeterminanthscj + S (mdr_j_first_zero_minorsevaluationdeterminanthsc) = (S (mdr_q_first_zero_minorsevaluationdeterminanths))) -> exists mdr_i_first_zero_minorsevaluationdeterminanthsc mdr_up_first_zero_minorsevaluationdeterminanthsc mdr_us_first_zero_minorsevaluationdeterminanthsc mdr_un_first_zero_minorsevaluationdeterminanthsc mdr_ut_first_zero_minorsevaluationdeterminanthsc mdr_p_first_zero_minorsevaluationdeterminanthsc mdr_n_first_zero_minorsevaluationdeterminanthsc. ((exists mdr_gap_first_zero_minorsevaluationdeterminanthsci. mdr_gap_first_zero_minorsevaluationdeterminanthsci + S (mdr_i_first_zero_minorsevaluationdeterminanthsc) = (mdr_i_first_zero_minorsevaluationdeterminanth)) /\ ((exists mdr_z_first_zero_minorsevaluationdeterminanthscr. ((exists mdr_a_first_zero_minorsevaluationdeterminanthscrc mdr_b_first_zero_minorsevaluationdeterminanthscrc mdr_c_first_zero_minorsevaluationdeterminanthscrc mdr_e_first_zero_minorsevaluationdeterminanthscrc mdr_f_first_zero_minorsevaluationdeterminanthscrc. ((mdr_a_first_zero_minorsevaluationdeterminanthscrc = ((mdr_q_first_zero_minorsevaluationdeterminanths) + (mdr_up_first_zero_minorsevaluationdeterminanthsc)) * S ((mdr_q_first_zero_minorsevaluationdeterminanths) + (mdr_up_first_zero_minorsevaluationdeterminanthsc)) + ((mdr_up_first_zero_minorsevaluationdeterminanthsc) + (mdr_up_first_zero_minorsevaluationdeterminanthsc))) /\ ((mdr_b_first_zero_minorsevaluationdeterminanthscrc = ((mdr_us_first_zero_minorsevaluationdeterminanthsc) + (mdr_un_first_zero_minorsevaluationdeterminanthsc)) * S ((mdr_us_first_zero_minorsevaluationdeterminanthsc) + (mdr_un_first_zero_minorsevaluationdeterminanthsc)) + ((mdr_un_first_zero_minorsevaluationdeterminanthsc) + (mdr_un_first_zero_minorsevaluationdeterminanthsc))) /\ ((mdr_c_first_zero_minorsevaluationdeterminanthscrc = ((mdr_a_first_zero_minorsevaluationdeterminanthscrc) + (mdr_b_first_zero_minorsevaluationdeterminanthscrc)) * S ((mdr_a_first_zero_minorsevaluationdeterminanthscrc) + (mdr_b_first_zero_minorsevaluationdeterminanthscrc)) + ((mdr_b_first_zero_minorsevaluationdeterminanthscrc) + (mdr_b_first_zero_minorsevaluationdeterminanthscrc))) /\ ((mdr_e_first_zero_minorsevaluationdeterminanthscrc = ((mdr_p_first_zero_minorsevaluationdeterminanthsc) + (mdr_n_first_zero_minorsevaluationdeterminanthsc)) * S ((mdr_p_first_zero_minorsevaluationdeterminanthsc) + (mdr_n_first_zero_minorsevaluationdeterminanthsc)) + ((mdr_n_first_zero_minorsevaluationdeterminanthsc) + (mdr_n_first_zero_minorsevaluationdeterminanthsc))) /\ ((mdr_f_first_zero_minorsevaluationdeterminanthscrc = ((mdr_ut_first_zero_minorsevaluationdeterminanthsc) + (mdr_e_first_zero_minorsevaluationdeterminanthscrc)) * S ((mdr_ut_first_zero_minorsevaluationdeterminanthsc) + (mdr_e_first_zero_minorsevaluationdeterminanthscrc)) + ((mdr_e_first_zero_minorsevaluationdeterminanthscrc) + (mdr_e_first_zero_minorsevaluationdeterminanthscrc))) /\ ((mdr_z_first_zero_minorsevaluationdeterminanthscr) = ((mdr_c_first_zero_minorsevaluationdeterminanthscrc) + (mdr_f_first_zero_minorsevaluationdeterminanthscrc)) * S ((mdr_c_first_zero_minorsevaluationdeterminanthscrc) + (mdr_f_first_zero_minorsevaluationdeterminanthscrc)) + ((mdr_f_first_zero_minorsevaluationdeterminanthscrc) + (mdr_f_first_zero_minorsevaluationdeterminanthscrc))))))))) /\ (((exists ff_h_mdr_first_zero_minorsevaluationdeterminanthscrb. ff_h_mdr_first_zero_minorsevaluationdeterminanthscrb + S (mdr_z_first_zero_minorsevaluationdeterminanthscr) = S ((S (mdr_i_first_zero_minorsevaluationdeterminanthsc)) * mdr_c_first_zero_minorsevaluationdeterminant)) /\ exists ff_q_mdr_first_zero_minorsevaluationdeterminanthscrb. mdr_b_first_zero_minorsevaluationdeterminant = ff_q_mdr_first_zero_minorsevaluationdeterminanthscrb * S ((S (mdr_i_first_zero_minorsevaluationdeterminanthsc)) * mdr_c_first_zero_minorsevaluationdeterminant) + (mdr_z_first_zero_minorsevaluationdeterminanthscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_first_zero_minorsevaluationdeterminanthscm_positive. (exists ff_gap_mdm_lt_mdr_first_zero_minorsevaluationdeterminanthscm_positive_index_bound. ff_gap_mdm_lt_mdr_first_zero_minorsevaluationdeterminanthscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_first_zero_minorsevaluationdeterminanthscm_positive) = ((mdr_q_first_zero_minorsevaluationdeterminanths) * (mdr_q_first_zero_minorsevaluationdeterminanths))) -> exists ff_row_mdm_prefix_mdr_first_zero_minorsevaluationdeterminanthscm_positive ff_column_mdm_prefix_mdr_first_zero_minorsevaluationdeterminanthscm_positive ff_value_mdm_prefix_mdr_first_zero_minorsevaluationdeterminanthscm_positive. (ff_index_mdm_prefix_mdr_first_zero_minorsevaluationdeterminanthscm_positive = (mdr_q_first_zero_minorsevaluationdeterminanths) * ff_row_mdm_prefix_mdr_first_zero_minorsevaluationdeterminanthscm_positive + ff_column_mdm_prefix_mdr_first_zero_minorsevaluationdeterminanthscm_positive /\ ((exists ff_gap_mdm_lt_mdr_first_zero_minorsevaluationdeterminanthscm_positive_column_bound. ff_gap_mdm_lt_mdr_first_zero_minorsevaluationdeterminanthscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_first_zero_minorsevaluationdeterminanthscm_positive) = (mdr_q_first_zero_minorsevaluationdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_first_zero_minorsevaluationdeterminanthscm_positive_cell ff_column_mdm_cell_mdr_first_zero_minorsevaluationdeterminanthscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_first_zero_minorsevaluationdeterminanthscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_first_zero_minorsevaluationdeterminanthscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_first_zero_minorsevaluationdeterminanthscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_first_zero_minorsevaluationdeterminanthscm_positive_cell = ff_row_mdm_prefix_mdr_first_zero_minorsevaluationdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_first_zero_minorsevaluationdeterminanthscm_positive_cell_row_after. ff_gap_mdm_le_mdr_first_zero_minorsevaluationdeterminanthscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_first_zero_minorsevaluationdeterminanthscm_positive)) /\ ff_row_mdm_cell_mdr_first_zero_minorsevaluationdeterminanthscm_positive_cell = S ff_row_mdm_prefix_mdr_first_zero_minorsevaluationdeterminanthscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_first_zero_minorsevaluationdeterminanthscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_first_zero_minorsevaluationdeterminanthscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_first_zero_minorsevaluationdeterminanthscm_positive) = (mdr_j_first_zero_minorsevaluationdeterminanthsc)) /\ ff_column_mdm_cell_mdr_first_zero_minorsevaluationdeterminanthscm_positive_cell = ff_column_mdm_prefix_mdr_first_zero_minorsevaluationdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_first_zero_minorsevaluationdeterminanthscm_positive_cell_column_after. ff_gap_mdm_le_mdr_first_zero_minorsevaluationdeterminanthscm_positive_cell_column_after + (mdr_j_first_zero_minorsevaluationdeterminanthsc) = (ff_column_mdm_prefix_mdr_first_zero_minorsevaluationdeterminanthscm_positive)) /\ ff_column_mdm_cell_mdr_first_zero_minorsevaluationdeterminanthscm_positive_cell = S ff_column_mdm_prefix_mdr_first_zero_minorsevaluationdeterminanthscm_positive))) /\ (((exists ff_h_mdm_mdr_first_zero_minorsevaluationdeterminanthscm_positive_cell_source. ff_h_mdm_mdr_first_zero_minorsevaluationdeterminanthscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_first_zero_minorsevaluationdeterminanthscm_positive) = S ((S ((ff_row_mdm_cell_mdr_first_zero_minorsevaluationdeterminanthscm_positive_cell) * (S (mdr_q_first_zero_minorsevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_first_zero_minorsevaluationdeterminanthscm_positive_cell))) * mdr_pc_first_zero_minorsevaluationdeterminanth)) /\ exists ff_q_mdm_mdr_first_zero_minorsevaluationdeterminanthscm_positive_cell_source. mdr_pb_first_zero_minorsevaluationdeterminanth = ff_q_mdm_mdr_first_zero_minorsevaluationdeterminanthscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_first_zero_minorsevaluationdeterminanthscm_positive_cell) * (S (mdr_q_first_zero_minorsevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_first_zero_minorsevaluationdeterminanthscm_positive_cell))) * mdr_pc_first_zero_minorsevaluationdeterminanth) + (ff_value_mdm_prefix_mdr_first_zero_minorsevaluationdeterminanthscm_positive)))))) /\ (((exists ff_h_mdm_mdr_first_zero_minorsevaluationdeterminanthscm_positive_target. ff_h_mdm_mdr_first_zero_minorsevaluationdeterminanthscm_positive_target + S (ff_value_mdm_prefix_mdr_first_zero_minorsevaluationdeterminanthscm_positive) = S ((S (ff_index_mdm_prefix_mdr_first_zero_minorsevaluationdeterminanthscm_positive)) * mdr_us_first_zero_minorsevaluationdeterminanthsc)) /\ exists ff_q_mdm_mdr_first_zero_minorsevaluationdeterminanthscm_positive_target. mdr_up_first_zero_minorsevaluationdeterminanthsc = ff_q_mdm_mdr_first_zero_minorsevaluationdeterminanthscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_first_zero_minorsevaluationdeterminanthscm_positive)) * mdr_us_first_zero_minorsevaluationdeterminanthsc) + (ff_value_mdm_prefix_mdr_first_zero_minorsevaluationdeterminanthscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_first_zero_minorsevaluationdeterminanthscm_negative. (exists ff_gap_mdm_lt_mdr_first_zero_minorsevaluationdeterminanthscm_negative_index_bound. ff_gap_mdm_lt_mdr_first_zero_minorsevaluationdeterminanthscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_first_zero_minorsevaluationdeterminanthscm_negative) = ((mdr_q_first_zero_minorsevaluationdeterminanths) * (mdr_q_first_zero_minorsevaluationdeterminanths))) -> exists ff_row_mdm_prefix_mdr_first_zero_minorsevaluationdeterminanthscm_negative ff_column_mdm_prefix_mdr_first_zero_minorsevaluationdeterminanthscm_negative ff_value_mdm_prefix_mdr_first_zero_minorsevaluationdeterminanthscm_negative. (ff_index_mdm_prefix_mdr_first_zero_minorsevaluationdeterminanthscm_negative = (mdr_q_first_zero_minorsevaluationdeterminanths) * ff_row_mdm_prefix_mdr_first_zero_minorsevaluationdeterminanthscm_negative + ff_column_mdm_prefix_mdr_first_zero_minorsevaluationdeterminanthscm_negative /\ ((exists ff_gap_mdm_lt_mdr_first_zero_minorsevaluationdeterminanthscm_negative_column_bound. ff_gap_mdm_lt_mdr_first_zero_minorsevaluationdeterminanthscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_first_zero_minorsevaluationdeterminanthscm_negative) = (mdr_q_first_zero_minorsevaluationdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_first_zero_minorsevaluationdeterminanthscm_negative_cell ff_column_mdm_cell_mdr_first_zero_minorsevaluationdeterminanthscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_first_zero_minorsevaluationdeterminanthscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_first_zero_minorsevaluationdeterminanthscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_first_zero_minorsevaluationdeterminanthscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_first_zero_minorsevaluationdeterminanthscm_negative_cell = ff_row_mdm_prefix_mdr_first_zero_minorsevaluationdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_first_zero_minorsevaluationdeterminanthscm_negative_cell_row_after. ff_gap_mdm_le_mdr_first_zero_minorsevaluationdeterminanthscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_first_zero_minorsevaluationdeterminanthscm_negative)) /\ ff_row_mdm_cell_mdr_first_zero_minorsevaluationdeterminanthscm_negative_cell = S ff_row_mdm_prefix_mdr_first_zero_minorsevaluationdeterminanthscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_first_zero_minorsevaluationdeterminanthscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_first_zero_minorsevaluationdeterminanthscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_first_zero_minorsevaluationdeterminanthscm_negative) = (mdr_j_first_zero_minorsevaluationdeterminanthsc)) /\ ff_column_mdm_cell_mdr_first_zero_minorsevaluationdeterminanthscm_negative_cell = ff_column_mdm_prefix_mdr_first_zero_minorsevaluationdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_first_zero_minorsevaluationdeterminanthscm_negative_cell_column_after. ff_gap_mdm_le_mdr_first_zero_minorsevaluationdeterminanthscm_negative_cell_column_after + (mdr_j_first_zero_minorsevaluationdeterminanthsc) = (ff_column_mdm_prefix_mdr_first_zero_minorsevaluationdeterminanthscm_negative)) /\ ff_column_mdm_cell_mdr_first_zero_minorsevaluationdeterminanthscm_negative_cell = S ff_column_mdm_prefix_mdr_first_zero_minorsevaluationdeterminanthscm_negative))) /\ (((exists ff_h_mdm_mdr_first_zero_minorsevaluationdeterminanthscm_negative_cell_source. ff_h_mdm_mdr_first_zero_minorsevaluationdeterminanthscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_first_zero_minorsevaluationdeterminanthscm_negative) = S ((S ((ff_row_mdm_cell_mdr_first_zero_minorsevaluationdeterminanthscm_negative_cell) * (S (mdr_q_first_zero_minorsevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_first_zero_minorsevaluationdeterminanthscm_negative_cell))) * mdr_nc_first_zero_minorsevaluationdeterminanth)) /\ exists ff_q_mdm_mdr_first_zero_minorsevaluationdeterminanthscm_negative_cell_source. mdr_nb_first_zero_minorsevaluationdeterminanth = ff_q_mdm_mdr_first_zero_minorsevaluationdeterminanthscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_first_zero_minorsevaluationdeterminanthscm_negative_cell) * (S (mdr_q_first_zero_minorsevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_first_zero_minorsevaluationdeterminanthscm_negative_cell))) * mdr_nc_first_zero_minorsevaluationdeterminanth) + (ff_value_mdm_prefix_mdr_first_zero_minorsevaluationdeterminanthscm_negative)))))) /\ (((exists ff_h_mdm_mdr_first_zero_minorsevaluationdeterminanthscm_negative_target. ff_h_mdm_mdr_first_zero_minorsevaluationdeterminanthscm_negative_target + S (ff_value_mdm_prefix_mdr_first_zero_minorsevaluationdeterminanthscm_negative) = S ((S (ff_index_mdm_prefix_mdr_first_zero_minorsevaluationdeterminanthscm_negative)) * mdr_ut_first_zero_minorsevaluationdeterminanthsc)) /\ exists ff_q_mdm_mdr_first_zero_minorsevaluationdeterminanthscm_negative_target. mdr_un_first_zero_minorsevaluationdeterminanthsc = ff_q_mdm_mdr_first_zero_minorsevaluationdeterminanthscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_first_zero_minorsevaluationdeterminanthscm_negative)) * mdr_ut_first_zero_minorsevaluationdeterminanthsc) + (ff_value_mdm_prefix_mdr_first_zero_minorsevaluationdeterminanthscm_negative))))))))) /\ ((((exists ff_h_mdr_first_zero_minorsevaluationdeterminanthscp. ff_h_mdr_first_zero_minorsevaluationdeterminanthscp + S (mdr_p_first_zero_minorsevaluationdeterminanthsc) = S ((S (mdr_j_first_zero_minorsevaluationdeterminanthsc)) * mdr_ec_first_zero_minorsevaluationdeterminanths)) /\ exists ff_q_mdr_first_zero_minorsevaluationdeterminanthscp. mdr_eb_first_zero_minorsevaluationdeterminanths = ff_q_mdr_first_zero_minorsevaluationdeterminanthscp * S ((S (mdr_j_first_zero_minorsevaluationdeterminanthsc)) * mdr_ec_first_zero_minorsevaluationdeterminanths) + (mdr_p_first_zero_minorsevaluationdeterminanthsc))) /\ (((exists ff_h_mdr_first_zero_minorsevaluationdeterminanthscn. ff_h_mdr_first_zero_minorsevaluationdeterminanthscn + S (mdr_n_first_zero_minorsevaluationdeterminanthsc) = S ((S (mdr_j_first_zero_minorsevaluationdeterminanthsc)) * mdr_fc_first_zero_minorsevaluationdeterminanths)) /\ exists ff_q_mdr_first_zero_minorsevaluationdeterminanthscn. mdr_fb_first_zero_minorsevaluationdeterminanths = ff_q_mdr_first_zero_minorsevaluationdeterminanthscn * S ((S (mdr_j_first_zero_minorsevaluationdeterminanthsc)) * mdr_fc_first_zero_minorsevaluationdeterminanths) + (mdr_n_first_zero_minorsevaluationdeterminanthsc)))))))) /\ (exists ff_ub_mce_fold_mdr_first_zero_minorsevaluationdeterminanthsf ff_uc_mce_fold_mdr_first_zero_minorsevaluationdeterminanthsf ff_vb_mce_fold_mdr_first_zero_minorsevaluationdeterminanthsf ff_vc_mce_fold_mdr_first_zero_minorsevaluationdeterminanthsf. ((forall ff_index_mce_alternating_mdr_first_zero_minorsevaluationdeterminanthsf_prefix. (exists ff_gap_mce_mdr_first_zero_minorsevaluationdeterminanthsf_prefix_index. ff_gap_mce_mdr_first_zero_minorsevaluationdeterminanthsf_prefix_index + S (ff_index_mce_alternating_mdr_first_zero_minorsevaluationdeterminanthsf_prefix) = (S (mdr_q_first_zero_minorsevaluationdeterminanths))) -> exists ff_ap_mce_alternating_mdr_first_zero_minorsevaluationdeterminanthsf_prefix ff_an_mce_alternating_mdr_first_zero_minorsevaluationdeterminanthsf_prefix ff_bp_mce_alternating_mdr_first_zero_minorsevaluationdeterminanthsf_prefix ff_bn_mce_alternating_mdr_first_zero_minorsevaluationdeterminanthsf_prefix ff_p_mce_alternating_mdr_first_zero_minorsevaluationdeterminanthsf_prefix ff_n_mce_alternating_mdr_first_zero_minorsevaluationdeterminanthsf_prefix. ((((exists ff_h_mce_mdr_first_zero_minorsevaluationdeterminanthsf_prefix_ap. ff_h_mce_mdr_first_zero_minorsevaluationdeterminanthsf_prefix_ap + S (ff_ap_mce_alternating_mdr_first_zero_minorsevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_first_zero_minorsevaluationdeterminanthsf_prefix)) * mdr_pc_first_zero_minorsevaluationdeterminanth)) /\ exists ff_q_mce_mdr_first_zero_minorsevaluationdeterminanthsf_prefix_ap. mdr_pb_first_zero_minorsevaluationdeterminanth = ff_q_mce_mdr_first_zero_minorsevaluationdeterminanthsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_first_zero_minorsevaluationdeterminanthsf_prefix)) * mdr_pc_first_zero_minorsevaluationdeterminanth) + (ff_ap_mce_alternating_mdr_first_zero_minorsevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_first_zero_minorsevaluationdeterminanthsf_prefix_an. ff_h_mce_mdr_first_zero_minorsevaluationdeterminanthsf_prefix_an + S (ff_an_mce_alternating_mdr_first_zero_minorsevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_first_zero_minorsevaluationdeterminanthsf_prefix)) * mdr_nc_first_zero_minorsevaluationdeterminanth)) /\ exists ff_q_mce_mdr_first_zero_minorsevaluationdeterminanthsf_prefix_an. mdr_nb_first_zero_minorsevaluationdeterminanth = ff_q_mce_mdr_first_zero_minorsevaluationdeterminanthsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_first_zero_minorsevaluationdeterminanthsf_prefix)) * mdr_nc_first_zero_minorsevaluationdeterminanth) + (ff_an_mce_alternating_mdr_first_zero_minorsevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_first_zero_minorsevaluationdeterminanthsf_prefix_bp. ff_h_mce_mdr_first_zero_minorsevaluationdeterminanthsf_prefix_bp + S (ff_bp_mce_alternating_mdr_first_zero_minorsevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_first_zero_minorsevaluationdeterminanthsf_prefix)) * mdr_ec_first_zero_minorsevaluationdeterminanths)) /\ exists ff_q_mce_mdr_first_zero_minorsevaluationdeterminanthsf_prefix_bp. mdr_eb_first_zero_minorsevaluationdeterminanths = ff_q_mce_mdr_first_zero_minorsevaluationdeterminanthsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_first_zero_minorsevaluationdeterminanthsf_prefix)) * mdr_ec_first_zero_minorsevaluationdeterminanths) + (ff_bp_mce_alternating_mdr_first_zero_minorsevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_first_zero_minorsevaluationdeterminanthsf_prefix_bn. ff_h_mce_mdr_first_zero_minorsevaluationdeterminanthsf_prefix_bn + S (ff_bn_mce_alternating_mdr_first_zero_minorsevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_first_zero_minorsevaluationdeterminanthsf_prefix)) * mdr_fc_first_zero_minorsevaluationdeterminanths)) /\ exists ff_q_mce_mdr_first_zero_minorsevaluationdeterminanthsf_prefix_bn. mdr_fb_first_zero_minorsevaluationdeterminanths = ff_q_mce_mdr_first_zero_minorsevaluationdeterminanthsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_first_zero_minorsevaluationdeterminanthsf_prefix)) * mdr_fc_first_zero_minorsevaluationdeterminanths) + (ff_bn_mce_alternating_mdr_first_zero_minorsevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_first_zero_minorsevaluationdeterminanthsf_prefix_positive. ff_h_mce_mdr_first_zero_minorsevaluationdeterminanthsf_prefix_positive + S (ff_p_mce_alternating_mdr_first_zero_minorsevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_first_zero_minorsevaluationdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_first_zero_minorsevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_first_zero_minorsevaluationdeterminanthsf_prefix_positive. ff_ub_mce_fold_mdr_first_zero_minorsevaluationdeterminanthsf = ff_q_mce_mdr_first_zero_minorsevaluationdeterminanthsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_first_zero_minorsevaluationdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_first_zero_minorsevaluationdeterminanthsf) + (ff_p_mce_alternating_mdr_first_zero_minorsevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_first_zero_minorsevaluationdeterminanthsf_prefix_negative. ff_h_mce_mdr_first_zero_minorsevaluationdeterminanthsf_prefix_negative + S (ff_n_mce_alternating_mdr_first_zero_minorsevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_first_zero_minorsevaluationdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_first_zero_minorsevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_first_zero_minorsevaluationdeterminanthsf_prefix_negative. ff_vb_mce_fold_mdr_first_zero_minorsevaluationdeterminanthsf = ff_q_mce_mdr_first_zero_minorsevaluationdeterminanthsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_first_zero_minorsevaluationdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_first_zero_minorsevaluationdeterminanthsf) + (ff_n_mce_alternating_mdr_first_zero_minorsevaluationdeterminanthsf_prefix))) /\ (((exists ff_even_mce_term_mdr_first_zero_minorsevaluationdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_first_zero_minorsevaluationdeterminanthsf_prefix = 2 * ff_even_mce_term_mdr_first_zero_minorsevaluationdeterminanthsf_prefix_term) /\ (ff_p_mce_alternating_mdr_first_zero_minorsevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_first_zero_minorsevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_first_zero_minorsevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_first_zero_minorsevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_first_zero_minorsevaluationdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_first_zero_minorsevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_first_zero_minorsevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_first_zero_minorsevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_first_zero_minorsevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_first_zero_minorsevaluationdeterminanthsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_first_zero_minorsevaluationdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_first_zero_minorsevaluationdeterminanthsf_prefix = 2 * ff_odd_mce_term_mdr_first_zero_minorsevaluationdeterminanthsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_first_zero_minorsevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_first_zero_minorsevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_first_zero_minorsevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_first_zero_minorsevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_first_zero_minorsevaluationdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_first_zero_minorsevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_first_zero_minorsevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_first_zero_minorsevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_first_zero_minorsevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_first_zero_minorsevaluationdeterminanthsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_first_zero_minorsevaluationdeterminanthsf_positive ff_v_mce_mdr_first_zero_minorsevaluationdeterminanthsf_positive. ((((exists ff_h_mce_mdr_first_zero_minorsevaluationdeterminanthsf_positive_start. ff_h_mce_mdr_first_zero_minorsevaluationdeterminanthsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_first_zero_minorsevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_first_zero_minorsevaluationdeterminanthsf_positive_start. ff_u_mce_mdr_first_zero_minorsevaluationdeterminanthsf_positive = ff_q_mce_mdr_first_zero_minorsevaluationdeterminanthsf_positive_start * S ((S (0)) * ff_v_mce_mdr_first_zero_minorsevaluationdeterminanthsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_first_zero_minorsevaluationdeterminanthsf_positive_terminal. ff_h_mce_mdr_first_zero_minorsevaluationdeterminanthsf_positive_terminal + S (mdr_p_first_zero_minorsevaluationdeterminanth) = S ((S ((S (mdr_q_first_zero_minorsevaluationdeterminanths)))) * ff_v_mce_mdr_first_zero_minorsevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_first_zero_minorsevaluationdeterminanthsf_positive_terminal. ff_u_mce_mdr_first_zero_minorsevaluationdeterminanthsf_positive = ff_q_mce_mdr_first_zero_minorsevaluationdeterminanthsf_positive_terminal * S ((S ((S (mdr_q_first_zero_minorsevaluationdeterminanths)))) * ff_v_mce_mdr_first_zero_minorsevaluationdeterminanthsf_positive) + (mdr_p_first_zero_minorsevaluationdeterminanth))) /\ forall ff_i_mce_mdr_first_zero_minorsevaluationdeterminanthsf_positive. (exists ff_lt_mce_mdr_first_zero_minorsevaluationdeterminanthsf_positive_bound. ff_lt_mce_mdr_first_zero_minorsevaluationdeterminanthsf_positive_bound + S ff_i_mce_mdr_first_zero_minorsevaluationdeterminanthsf_positive = (S (mdr_q_first_zero_minorsevaluationdeterminanths))) -> exists ff_a_mce_mdr_first_zero_minorsevaluationdeterminanthsf_positive ff_r_mce_mdr_first_zero_minorsevaluationdeterminanthsf_positive ff_s_mce_mdr_first_zero_minorsevaluationdeterminanthsf_positive. ((((exists ff_h_mce_mdr_first_zero_minorsevaluationdeterminanthsf_positive_summand. ff_h_mce_mdr_first_zero_minorsevaluationdeterminanthsf_positive_summand + S (ff_a_mce_mdr_first_zero_minorsevaluationdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_first_zero_minorsevaluationdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_first_zero_minorsevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_first_zero_minorsevaluationdeterminanthsf_positive_summand. ff_ub_mce_fold_mdr_first_zero_minorsevaluationdeterminanthsf = ff_q_mce_mdr_first_zero_minorsevaluationdeterminanthsf_positive_summand * S ((S (ff_i_mce_mdr_first_zero_minorsevaluationdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_first_zero_minorsevaluationdeterminanthsf) + (ff_a_mce_mdr_first_zero_minorsevaluationdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_first_zero_minorsevaluationdeterminanthsf_positive_partial. ff_h_mce_mdr_first_zero_minorsevaluationdeterminanthsf_positive_partial + S (ff_r_mce_mdr_first_zero_minorsevaluationdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_first_zero_minorsevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_first_zero_minorsevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_first_zero_minorsevaluationdeterminanthsf_positive_partial. ff_u_mce_mdr_first_zero_minorsevaluationdeterminanthsf_positive = ff_q_mce_mdr_first_zero_minorsevaluationdeterminanthsf_positive_partial * S ((S (ff_i_mce_mdr_first_zero_minorsevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_first_zero_minorsevaluationdeterminanthsf_positive) + (ff_r_mce_mdr_first_zero_minorsevaluationdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_first_zero_minorsevaluationdeterminanthsf_positive_successor. ff_h_mce_mdr_first_zero_minorsevaluationdeterminanthsf_positive_successor + S (ff_s_mce_mdr_first_zero_minorsevaluationdeterminanthsf_positive) = S ((S (S ff_i_mce_mdr_first_zero_minorsevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_first_zero_minorsevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_first_zero_minorsevaluationdeterminanthsf_positive_successor. ff_u_mce_mdr_first_zero_minorsevaluationdeterminanthsf_positive = ff_q_mce_mdr_first_zero_minorsevaluationdeterminanthsf_positive_successor * S ((S (S ff_i_mce_mdr_first_zero_minorsevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_first_zero_minorsevaluationdeterminanthsf_positive) + (ff_s_mce_mdr_first_zero_minorsevaluationdeterminanthsf_positive))) /\ ff_s_mce_mdr_first_zero_minorsevaluationdeterminanthsf_positive = ff_r_mce_mdr_first_zero_minorsevaluationdeterminanthsf_positive + ff_a_mce_mdr_first_zero_minorsevaluationdeterminanthsf_positive)))))) /\ (exists ff_u_mce_mdr_first_zero_minorsevaluationdeterminanthsf_negative ff_v_mce_mdr_first_zero_minorsevaluationdeterminanthsf_negative. ((((exists ff_h_mce_mdr_first_zero_minorsevaluationdeterminanthsf_negative_start. ff_h_mce_mdr_first_zero_minorsevaluationdeterminanthsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_first_zero_minorsevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_first_zero_minorsevaluationdeterminanthsf_negative_start. ff_u_mce_mdr_first_zero_minorsevaluationdeterminanthsf_negative = ff_q_mce_mdr_first_zero_minorsevaluationdeterminanthsf_negative_start * S ((S (0)) * ff_v_mce_mdr_first_zero_minorsevaluationdeterminanthsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_first_zero_minorsevaluationdeterminanthsf_negative_terminal. ff_h_mce_mdr_first_zero_minorsevaluationdeterminanthsf_negative_terminal + S (mdr_n_first_zero_minorsevaluationdeterminanth) = S ((S ((S (mdr_q_first_zero_minorsevaluationdeterminanths)))) * ff_v_mce_mdr_first_zero_minorsevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_first_zero_minorsevaluationdeterminanthsf_negative_terminal. ff_u_mce_mdr_first_zero_minorsevaluationdeterminanthsf_negative = ff_q_mce_mdr_first_zero_minorsevaluationdeterminanthsf_negative_terminal * S ((S ((S (mdr_q_first_zero_minorsevaluationdeterminanths)))) * ff_v_mce_mdr_first_zero_minorsevaluationdeterminanthsf_negative) + (mdr_n_first_zero_minorsevaluationdeterminanth))) /\ forall ff_i_mce_mdr_first_zero_minorsevaluationdeterminanthsf_negative. (exists ff_lt_mce_mdr_first_zero_minorsevaluationdeterminanthsf_negative_bound. ff_lt_mce_mdr_first_zero_minorsevaluationdeterminanthsf_negative_bound + S ff_i_mce_mdr_first_zero_minorsevaluationdeterminanthsf_negative = (S (mdr_q_first_zero_minorsevaluationdeterminanths))) -> exists ff_a_mce_mdr_first_zero_minorsevaluationdeterminanthsf_negative ff_r_mce_mdr_first_zero_minorsevaluationdeterminanthsf_negative ff_s_mce_mdr_first_zero_minorsevaluationdeterminanthsf_negative. ((((exists ff_h_mce_mdr_first_zero_minorsevaluationdeterminanthsf_negative_summand. ff_h_mce_mdr_first_zero_minorsevaluationdeterminanthsf_negative_summand + S (ff_a_mce_mdr_first_zero_minorsevaluationdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_first_zero_minorsevaluationdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_first_zero_minorsevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_first_zero_minorsevaluationdeterminanthsf_negative_summand. ff_vb_mce_fold_mdr_first_zero_minorsevaluationdeterminanthsf = ff_q_mce_mdr_first_zero_minorsevaluationdeterminanthsf_negative_summand * S ((S (ff_i_mce_mdr_first_zero_minorsevaluationdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_first_zero_minorsevaluationdeterminanthsf) + (ff_a_mce_mdr_first_zero_minorsevaluationdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_first_zero_minorsevaluationdeterminanthsf_negative_partial. ff_h_mce_mdr_first_zero_minorsevaluationdeterminanthsf_negative_partial + S (ff_r_mce_mdr_first_zero_minorsevaluationdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_first_zero_minorsevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_first_zero_minorsevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_first_zero_minorsevaluationdeterminanthsf_negative_partial. ff_u_mce_mdr_first_zero_minorsevaluationdeterminanthsf_negative = ff_q_mce_mdr_first_zero_minorsevaluationdeterminanthsf_negative_partial * S ((S (ff_i_mce_mdr_first_zero_minorsevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_first_zero_minorsevaluationdeterminanthsf_negative) + (ff_r_mce_mdr_first_zero_minorsevaluationdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_first_zero_minorsevaluationdeterminanthsf_negative_successor. ff_h_mce_mdr_first_zero_minorsevaluationdeterminanthsf_negative_successor + S (ff_s_mce_mdr_first_zero_minorsevaluationdeterminanthsf_negative) = S ((S (S ff_i_mce_mdr_first_zero_minorsevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_first_zero_minorsevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_first_zero_minorsevaluationdeterminanthsf_negative_successor. ff_u_mce_mdr_first_zero_minorsevaluationdeterminanthsf_negative = ff_q_mce_mdr_first_zero_minorsevaluationdeterminanthsf_negative_successor * S ((S (S ff_i_mce_mdr_first_zero_minorsevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_first_zero_minorsevaluationdeterminanthsf_negative) + (ff_s_mce_mdr_first_zero_minorsevaluationdeterminanthsf_negative))) /\ ff_s_mce_mdr_first_zero_minorsevaluationdeterminanthsf_negative = ff_r_mce_mdr_first_zero_minorsevaluationdeterminanthsf_negative + ff_a_mce_mdr_first_zero_minorsevaluationdeterminanthsf_negative))))))))))))))) /\ ((exists mdr_gap_first_zero_minorsevaluationdeterminanti. mdr_gap_first_zero_minorsevaluationdeterminanti + S (mdr_i_first_zero_minorsevaluationdeterminant) = (mdr_l_first_zero_minorsevaluationdeterminant)) /\ (exists mdr_z_first_zero_minorsevaluationdeterminantr. ((exists mdr_a_first_zero_minorsevaluationdeterminantrc mdr_b_first_zero_minorsevaluationdeterminantrc mdr_c_first_zero_minorsevaluationdeterminantrc mdr_e_first_zero_minorsevaluationdeterminantrc mdr_f_first_zero_minorsevaluationdeterminantrc. ((mdr_a_first_zero_minorsevaluationdeterminantrc = ((q) + (mdr_ub_first_zero_minorsevaluation)) * S ((q) + (mdr_ub_first_zero_minorsevaluation)) + ((mdr_ub_first_zero_minorsevaluation) + (mdr_ub_first_zero_minorsevaluation))) /\ ((mdr_b_first_zero_minorsevaluationdeterminantrc = ((mdr_uc_first_zero_minorsevaluation) + (mdr_vb_first_zero_minorsevaluation)) * S ((mdr_uc_first_zero_minorsevaluation) + (mdr_vb_first_zero_minorsevaluation)) + ((mdr_vb_first_zero_minorsevaluation) + (mdr_vb_first_zero_minorsevaluation))) /\ ((mdr_c_first_zero_minorsevaluationdeterminantrc = ((mdr_a_first_zero_minorsevaluationdeterminantrc) + (mdr_b_first_zero_minorsevaluationdeterminantrc)) * S ((mdr_a_first_zero_minorsevaluationdeterminantrc) + (mdr_b_first_zero_minorsevaluationdeterminantrc)) + ((mdr_b_first_zero_minorsevaluationdeterminantrc) + (mdr_b_first_zero_minorsevaluationdeterminantrc))) /\ ((mdr_e_first_zero_minorsevaluationdeterminantrc = ((mdr_p_first_zero_minors) + (mdr_n_first_zero_minors)) * S ((mdr_p_first_zero_minors) + (mdr_n_first_zero_minors)) + ((mdr_n_first_zero_minors) + (mdr_n_first_zero_minors))) /\ ((mdr_f_first_zero_minorsevaluationdeterminantrc = ((mdr_vc_first_zero_minorsevaluation) + (mdr_e_first_zero_minorsevaluationdeterminantrc)) * S ((mdr_vc_first_zero_minorsevaluation) + (mdr_e_first_zero_minorsevaluationdeterminantrc)) + ((mdr_e_first_zero_minorsevaluationdeterminantrc) + (mdr_e_first_zero_minorsevaluationdeterminantrc))) /\ ((mdr_z_first_zero_minorsevaluationdeterminantr) = ((mdr_c_first_zero_minorsevaluationdeterminantrc) + (mdr_f_first_zero_minorsevaluationdeterminantrc)) * S ((mdr_c_first_zero_minorsevaluationdeterminantrc) + (mdr_f_first_zero_minorsevaluationdeterminantrc)) + ((mdr_f_first_zero_minorsevaluationdeterminantrc) + (mdr_f_first_zero_minorsevaluationdeterminantrc))))))))) /\ (((exists ff_h_mdr_first_zero_minorsevaluationdeterminantrb. ff_h_mdr_first_zero_minorsevaluationdeterminantrb + S (mdr_z_first_zero_minorsevaluationdeterminantr) = S ((S (mdr_i_first_zero_minorsevaluationdeterminant)) * mdr_c_first_zero_minorsevaluationdeterminant)) /\ exists ff_q_mdr_first_zero_minorsevaluationdeterminantrb. mdr_b_first_zero_minorsevaluationdeterminant = ff_q_mdr_first_zero_minorsevaluationdeterminantrb * S ((S (mdr_i_first_zero_minorsevaluationdeterminant)) * mdr_c_first_zero_minorsevaluationdeterminant) + (mdr_z_first_zero_minorsevaluationdeterminantr)))))))))) -> mdr_p_first_zero_minors = mdr_n_first_zero_minors) -> (forall mdr_rb_second_zero_minors mdr_rc_second_zero_minors mdr_cb_second_zero_minors mdr_cc_second_zero_minors mdr_p_second_zero_minors mdr_n_second_zero_minors. (((forall fom_index_mrf_second_zero_minorsrowsbound. (exists fom_gap_mrf_second_zero_minorsrowsbound_index_bound. fom_gap_mrf_second_zero_minorsrowsbound_index_bound + S (fom_index_mrf_second_zero_minorsrowsbound) = q) -> exists fom_value_mrf_second_zero_minorsrowsbound. ((((exists fom_beta_height_mrf_second_zero_minorsrowsbound_entry. fom_beta_height_mrf_second_zero_minorsrowsbound_entry + S (fom_value_mrf_second_zero_minorsrowsbound) = S ((S (fom_index_mrf_second_zero_minorsrowsbound)) * mdr_rc_second_zero_minors)) /\ exists fom_beta_quotient_mrf_second_zero_minorsrowsbound_entry. mdr_rb_second_zero_minors = fom_beta_quotient_mrf_second_zero_minorsrowsbound_entry * S ((S (fom_index_mrf_second_zero_minorsrowsbound)) * mdr_rc_second_zero_minors) + (fom_value_mrf_second_zero_minorsrowsbound))) /\ (exists fom_gap_mrf_second_zero_minorsrowsbound_value_bound. fom_gap_mrf_second_zero_minorsrowsbound_value_bound + S (fom_value_mrf_second_zero_minorsrowsbound) = r))) /\ (forall mdr_i_second_zero_minorsrowsdistinct mdr_j_second_zero_minorsrowsdistinct mdr_a_second_zero_minorsrowsdistinct. (exists mdr_gap_second_zero_minorsrowsdistincti. mdr_gap_second_zero_minorsrowsdistincti + S (mdr_i_second_zero_minorsrowsdistinct) = (q)) -> (exists mdr_gap_second_zero_minorsrowsdistinctj. mdr_gap_second_zero_minorsrowsdistinctj + S (mdr_j_second_zero_minorsrowsdistinct) = (q)) -> (((exists ff_h_mdr_second_zero_minorsrowsdistinctfirst. ff_h_mdr_second_zero_minorsrowsdistinctfirst + S (mdr_a_second_zero_minorsrowsdistinct) = S ((S (mdr_i_second_zero_minorsrowsdistinct)) * mdr_rc_second_zero_minors)) /\ exists ff_q_mdr_second_zero_minorsrowsdistinctfirst. mdr_rb_second_zero_minors = ff_q_mdr_second_zero_minorsrowsdistinctfirst * S ((S (mdr_i_second_zero_minorsrowsdistinct)) * mdr_rc_second_zero_minors) + (mdr_a_second_zero_minorsrowsdistinct))) -> (((exists ff_h_mdr_second_zero_minorsrowsdistinctsecond. ff_h_mdr_second_zero_minorsrowsdistinctsecond + S (mdr_a_second_zero_minorsrowsdistinct) = S ((S (mdr_j_second_zero_minorsrowsdistinct)) * mdr_rc_second_zero_minors)) /\ exists ff_q_mdr_second_zero_minorsrowsdistinctsecond. mdr_rb_second_zero_minors = ff_q_mdr_second_zero_minorsrowsdistinctsecond * S ((S (mdr_j_second_zero_minorsrowsdistinct)) * mdr_rc_second_zero_minors) + (mdr_a_second_zero_minorsrowsdistinct))) -> mdr_i_second_zero_minorsrowsdistinct = mdr_j_second_zero_minorsrowsdistinct))) -> (((forall fom_index_mrf_second_zero_minorscolumnsbound. (exists fom_gap_mrf_second_zero_minorscolumnsbound_index_bound. fom_gap_mrf_second_zero_minorscolumnsbound_index_bound + S (fom_index_mrf_second_zero_minorscolumnsbound) = q) -> exists fom_value_mrf_second_zero_minorscolumnsbound. ((((exists fom_beta_height_mrf_second_zero_minorscolumnsbound_entry. fom_beta_height_mrf_second_zero_minorscolumnsbound_entry + S (fom_value_mrf_second_zero_minorscolumnsbound) = S ((S (fom_index_mrf_second_zero_minorscolumnsbound)) * mdr_cc_second_zero_minors)) /\ exists fom_beta_quotient_mrf_second_zero_minorscolumnsbound_entry. mdr_cb_second_zero_minors = fom_beta_quotient_mrf_second_zero_minorscolumnsbound_entry * S ((S (fom_index_mrf_second_zero_minorscolumnsbound)) * mdr_cc_second_zero_minors) + (fom_value_mrf_second_zero_minorscolumnsbound))) /\ (exists fom_gap_mrf_second_zero_minorscolumnsbound_value_bound. fom_gap_mrf_second_zero_minorscolumnsbound_value_bound + S (fom_value_mrf_second_zero_minorscolumnsbound) = w))) /\ (forall mdr_i_second_zero_minorscolumnsdistinct mdr_j_second_zero_minorscolumnsdistinct mdr_a_second_zero_minorscolumnsdistinct. (exists mdr_gap_second_zero_minorscolumnsdistincti. mdr_gap_second_zero_minorscolumnsdistincti + S (mdr_i_second_zero_minorscolumnsdistinct) = (q)) -> (exists mdr_gap_second_zero_minorscolumnsdistinctj. mdr_gap_second_zero_minorscolumnsdistinctj + S (mdr_j_second_zero_minorscolumnsdistinct) = (q)) -> (((exists ff_h_mdr_second_zero_minorscolumnsdistinctfirst. ff_h_mdr_second_zero_minorscolumnsdistinctfirst + S (mdr_a_second_zero_minorscolumnsdistinct) = S ((S (mdr_i_second_zero_minorscolumnsdistinct)) * mdr_cc_second_zero_minors)) /\ exists ff_q_mdr_second_zero_minorscolumnsdistinctfirst. mdr_cb_second_zero_minors = ff_q_mdr_second_zero_minorscolumnsdistinctfirst * S ((S (mdr_i_second_zero_minorscolumnsdistinct)) * mdr_cc_second_zero_minors) + (mdr_a_second_zero_minorscolumnsdistinct))) -> (((exists ff_h_mdr_second_zero_minorscolumnsdistinctsecond. ff_h_mdr_second_zero_minorscolumnsdistinctsecond + S (mdr_a_second_zero_minorscolumnsdistinct) = S ((S (mdr_j_second_zero_minorscolumnsdistinct)) * mdr_cc_second_zero_minors)) /\ exists ff_q_mdr_second_zero_minorscolumnsdistinctsecond. mdr_cb_second_zero_minors = ff_q_mdr_second_zero_minorscolumnsdistinctsecond * S ((S (mdr_j_second_zero_minorscolumnsdistinct)) * mdr_cc_second_zero_minors) + (mdr_a_second_zero_minorscolumnsdistinct))) -> mdr_i_second_zero_minorscolumnsdistinct = mdr_j_second_zero_minorscolumnsdistinct))) -> (exists mdr_ub_second_zero_minorsevaluation mdr_uc_second_zero_minorsevaluation mdr_vb_second_zero_minorsevaluation mdr_vc_second_zero_minorsevaluation. ((((forall mdr_i_second_zero_minorsevaluationmatrixpositive. (exists mdr_gap_second_zero_minorsevaluationmatrixpositivebound. mdr_gap_second_zero_minorsevaluationmatrixpositivebound + S (mdr_i_second_zero_minorsevaluationmatrixpositive) = ((q) * (q))) -> exists mdr_a_second_zero_minorsevaluationmatrixpositive. (((exists mdr_r_second_zero_minorsevaluationmatrixpositivepoint mdr_s_second_zero_minorsevaluationmatrixpositivepoint mdr_u_second_zero_minorsevaluationmatrixpositivepoint mdr_v_second_zero_minorsevaluationmatrixpositivepoint. ((mdr_i_second_zero_minorsevaluationmatrixpositive = (q) * mdr_r_second_zero_minorsevaluationmatrixpositivepoint + mdr_s_second_zero_minorsevaluationmatrixpositivepoint) /\ ((exists mdr_gap_second_zero_minorsevaluationmatrixpositivepointcolumn. mdr_gap_second_zero_minorsevaluationmatrixpositivepointcolumn + S (mdr_s_second_zero_minorsevaluationmatrixpositivepoint) = (q)) /\ ((((exists ff_h_mdr_second_zero_minorsevaluationmatrixpositivepointrow_index. ff_h_mdr_second_zero_minorsevaluationmatrixpositivepointrow_index + S (mdr_u_second_zero_minorsevaluationmatrixpositivepoint) = S ((S (mdr_r_second_zero_minorsevaluationmatrixpositivepoint)) * mdr_rc_second_zero_minors)) /\ exists ff_q_mdr_second_zero_minorsevaluationmatrixpositivepointrow_index. mdr_rb_second_zero_minors = ff_q_mdr_second_zero_minorsevaluationmatrixpositivepointrow_index * S ((S (mdr_r_second_zero_minorsevaluationmatrixpositivepoint)) * mdr_rc_second_zero_minors) + (mdr_u_second_zero_minorsevaluationmatrixpositivepoint))) /\ ((((exists ff_h_mdr_second_zero_minorsevaluationmatrixpositivepointcolumn_index. ff_h_mdr_second_zero_minorsevaluationmatrixpositivepointcolumn_index + S (mdr_v_second_zero_minorsevaluationmatrixpositivepoint) = S ((S (mdr_s_second_zero_minorsevaluationmatrixpositivepoint)) * mdr_cc_second_zero_minors)) /\ exists ff_q_mdr_second_zero_minorsevaluationmatrixpositivepointcolumn_index. mdr_cb_second_zero_minors = ff_q_mdr_second_zero_minorsevaluationmatrixpositivepointcolumn_index * S ((S (mdr_s_second_zero_minorsevaluationmatrixpositivepoint)) * mdr_cc_second_zero_minors) + (mdr_v_second_zero_minorsevaluationmatrixpositivepoint))) /\ (((exists ff_h_mdr_second_zero_minorsevaluationmatrixpositivepointsource. ff_h_mdr_second_zero_minorsevaluationmatrixpositivepointsource + S (mdr_a_second_zero_minorsevaluationmatrixpositive) = S ((S ((mdr_u_second_zero_minorsevaluationmatrixpositivepoint) * (w) + (mdr_v_second_zero_minorsevaluationmatrixpositivepoint))) * ec)) /\ exists ff_q_mdr_second_zero_minorsevaluationmatrixpositivepointsource. eb = ff_q_mdr_second_zero_minorsevaluationmatrixpositivepointsource * S ((S ((mdr_u_second_zero_minorsevaluationmatrixpositivepoint) * (w) + (mdr_v_second_zero_minorsevaluationmatrixpositivepoint))) * ec) + (mdr_a_second_zero_minorsevaluationmatrixpositive)))))))) /\ (((exists ff_h_mdr_second_zero_minorsevaluationmatrixpositiveoutput. ff_h_mdr_second_zero_minorsevaluationmatrixpositiveoutput + S (mdr_a_second_zero_minorsevaluationmatrixpositive) = S ((S (mdr_i_second_zero_minorsevaluationmatrixpositive)) * mdr_uc_second_zero_minorsevaluation)) /\ exists ff_q_mdr_second_zero_minorsevaluationmatrixpositiveoutput. mdr_ub_second_zero_minorsevaluation = ff_q_mdr_second_zero_minorsevaluationmatrixpositiveoutput * S ((S (mdr_i_second_zero_minorsevaluationmatrixpositive)) * mdr_uc_second_zero_minorsevaluation) + (mdr_a_second_zero_minorsevaluationmatrixpositive)))))) /\ (forall mdr_i_second_zero_minorsevaluationmatrixnegative. (exists mdr_gap_second_zero_minorsevaluationmatrixnegativebound. mdr_gap_second_zero_minorsevaluationmatrixnegativebound + S (mdr_i_second_zero_minorsevaluationmatrixnegative) = ((q) * (q))) -> exists mdr_a_second_zero_minorsevaluationmatrixnegative. (((exists mdr_r_second_zero_minorsevaluationmatrixnegativepoint mdr_s_second_zero_minorsevaluationmatrixnegativepoint mdr_u_second_zero_minorsevaluationmatrixnegativepoint mdr_v_second_zero_minorsevaluationmatrixnegativepoint. ((mdr_i_second_zero_minorsevaluationmatrixnegative = (q) * mdr_r_second_zero_minorsevaluationmatrixnegativepoint + mdr_s_second_zero_minorsevaluationmatrixnegativepoint) /\ ((exists mdr_gap_second_zero_minorsevaluationmatrixnegativepointcolumn. mdr_gap_second_zero_minorsevaluationmatrixnegativepointcolumn + S (mdr_s_second_zero_minorsevaluationmatrixnegativepoint) = (q)) /\ ((((exists ff_h_mdr_second_zero_minorsevaluationmatrixnegativepointrow_index. ff_h_mdr_second_zero_minorsevaluationmatrixnegativepointrow_index + S (mdr_u_second_zero_minorsevaluationmatrixnegativepoint) = S ((S (mdr_r_second_zero_minorsevaluationmatrixnegativepoint)) * mdr_rc_second_zero_minors)) /\ exists ff_q_mdr_second_zero_minorsevaluationmatrixnegativepointrow_index. mdr_rb_second_zero_minors = ff_q_mdr_second_zero_minorsevaluationmatrixnegativepointrow_index * S ((S (mdr_r_second_zero_minorsevaluationmatrixnegativepoint)) * mdr_rc_second_zero_minors) + (mdr_u_second_zero_minorsevaluationmatrixnegativepoint))) /\ ((((exists ff_h_mdr_second_zero_minorsevaluationmatrixnegativepointcolumn_index. ff_h_mdr_second_zero_minorsevaluationmatrixnegativepointcolumn_index + S (mdr_v_second_zero_minorsevaluationmatrixnegativepoint) = S ((S (mdr_s_second_zero_minorsevaluationmatrixnegativepoint)) * mdr_cc_second_zero_minors)) /\ exists ff_q_mdr_second_zero_minorsevaluationmatrixnegativepointcolumn_index. mdr_cb_second_zero_minors = ff_q_mdr_second_zero_minorsevaluationmatrixnegativepointcolumn_index * S ((S (mdr_s_second_zero_minorsevaluationmatrixnegativepoint)) * mdr_cc_second_zero_minors) + (mdr_v_second_zero_minorsevaluationmatrixnegativepoint))) /\ (((exists ff_h_mdr_second_zero_minorsevaluationmatrixnegativepointsource. ff_h_mdr_second_zero_minorsevaluationmatrixnegativepointsource + S (mdr_a_second_zero_minorsevaluationmatrixnegative) = S ((S ((mdr_u_second_zero_minorsevaluationmatrixnegativepoint) * (w) + (mdr_v_second_zero_minorsevaluationmatrixnegativepoint))) * fc)) /\ exists ff_q_mdr_second_zero_minorsevaluationmatrixnegativepointsource. fb = ff_q_mdr_second_zero_minorsevaluationmatrixnegativepointsource * S ((S ((mdr_u_second_zero_minorsevaluationmatrixnegativepoint) * (w) + (mdr_v_second_zero_minorsevaluationmatrixnegativepoint))) * fc) + (mdr_a_second_zero_minorsevaluationmatrixnegative)))))))) /\ (((exists ff_h_mdr_second_zero_minorsevaluationmatrixnegativeoutput. ff_h_mdr_second_zero_minorsevaluationmatrixnegativeoutput + S (mdr_a_second_zero_minorsevaluationmatrixnegative) = S ((S (mdr_i_second_zero_minorsevaluationmatrixnegative)) * mdr_vc_second_zero_minorsevaluation)) /\ exists ff_q_mdr_second_zero_minorsevaluationmatrixnegativeoutput. mdr_vb_second_zero_minorsevaluation = ff_q_mdr_second_zero_minorsevaluationmatrixnegativeoutput * S ((S (mdr_i_second_zero_minorsevaluationmatrixnegative)) * mdr_vc_second_zero_minorsevaluation) + (mdr_a_second_zero_minorsevaluationmatrixnegative)))))))) /\ (exists mdr_b_second_zero_minorsevaluationdeterminant mdr_c_second_zero_minorsevaluationdeterminant mdr_l_second_zero_minorsevaluationdeterminant mdr_i_second_zero_minorsevaluationdeterminant. ((forall mdr_i_second_zero_minorsevaluationdeterminanth. (exists mdr_gap_second_zero_minorsevaluationdeterminanthi. mdr_gap_second_zero_minorsevaluationdeterminanthi + S (mdr_i_second_zero_minorsevaluationdeterminanth) = (mdr_l_second_zero_minorsevaluationdeterminant)) -> exists mdr_d_second_zero_minorsevaluationdeterminanth mdr_pb_second_zero_minorsevaluationdeterminanth mdr_pc_second_zero_minorsevaluationdeterminanth mdr_nb_second_zero_minorsevaluationdeterminanth mdr_nc_second_zero_minorsevaluationdeterminanth mdr_p_second_zero_minorsevaluationdeterminanth mdr_n_second_zero_minorsevaluationdeterminanth. ((exists mdr_z_second_zero_minorsevaluationdeterminanthr. ((exists mdr_a_second_zero_minorsevaluationdeterminanthrc mdr_b_second_zero_minorsevaluationdeterminanthrc mdr_c_second_zero_minorsevaluationdeterminanthrc mdr_e_second_zero_minorsevaluationdeterminanthrc mdr_f_second_zero_minorsevaluationdeterminanthrc. ((mdr_a_second_zero_minorsevaluationdeterminanthrc = ((mdr_d_second_zero_minorsevaluationdeterminanth) + (mdr_pb_second_zero_minorsevaluationdeterminanth)) * S ((mdr_d_second_zero_minorsevaluationdeterminanth) + (mdr_pb_second_zero_minorsevaluationdeterminanth)) + ((mdr_pb_second_zero_minorsevaluationdeterminanth) + (mdr_pb_second_zero_minorsevaluationdeterminanth))) /\ ((mdr_b_second_zero_minorsevaluationdeterminanthrc = ((mdr_pc_second_zero_minorsevaluationdeterminanth) + (mdr_nb_second_zero_minorsevaluationdeterminanth)) * S ((mdr_pc_second_zero_minorsevaluationdeterminanth) + (mdr_nb_second_zero_minorsevaluationdeterminanth)) + ((mdr_nb_second_zero_minorsevaluationdeterminanth) + (mdr_nb_second_zero_minorsevaluationdeterminanth))) /\ ((mdr_c_second_zero_minorsevaluationdeterminanthrc = ((mdr_a_second_zero_minorsevaluationdeterminanthrc) + (mdr_b_second_zero_minorsevaluationdeterminanthrc)) * S ((mdr_a_second_zero_minorsevaluationdeterminanthrc) + (mdr_b_second_zero_minorsevaluationdeterminanthrc)) + ((mdr_b_second_zero_minorsevaluationdeterminanthrc) + (mdr_b_second_zero_minorsevaluationdeterminanthrc))) /\ ((mdr_e_second_zero_minorsevaluationdeterminanthrc = ((mdr_p_second_zero_minorsevaluationdeterminanth) + (mdr_n_second_zero_minorsevaluationdeterminanth)) * S ((mdr_p_second_zero_minorsevaluationdeterminanth) + (mdr_n_second_zero_minorsevaluationdeterminanth)) + ((mdr_n_second_zero_minorsevaluationdeterminanth) + (mdr_n_second_zero_minorsevaluationdeterminanth))) /\ ((mdr_f_second_zero_minorsevaluationdeterminanthrc = ((mdr_nc_second_zero_minorsevaluationdeterminanth) + (mdr_e_second_zero_minorsevaluationdeterminanthrc)) * S ((mdr_nc_second_zero_minorsevaluationdeterminanth) + (mdr_e_second_zero_minorsevaluationdeterminanthrc)) + ((mdr_e_second_zero_minorsevaluationdeterminanthrc) + (mdr_e_second_zero_minorsevaluationdeterminanthrc))) /\ ((mdr_z_second_zero_minorsevaluationdeterminanthr) = ((mdr_c_second_zero_minorsevaluationdeterminanthrc) + (mdr_f_second_zero_minorsevaluationdeterminanthrc)) * S ((mdr_c_second_zero_minorsevaluationdeterminanthrc) + (mdr_f_second_zero_minorsevaluationdeterminanthrc)) + ((mdr_f_second_zero_minorsevaluationdeterminanthrc) + (mdr_f_second_zero_minorsevaluationdeterminanthrc))))))))) /\ (((exists ff_h_mdr_second_zero_minorsevaluationdeterminanthrb. ff_h_mdr_second_zero_minorsevaluationdeterminanthrb + S (mdr_z_second_zero_minorsevaluationdeterminanthr) = S ((S (mdr_i_second_zero_minorsevaluationdeterminanth)) * mdr_c_second_zero_minorsevaluationdeterminant)) /\ exists ff_q_mdr_second_zero_minorsevaluationdeterminanthrb. mdr_b_second_zero_minorsevaluationdeterminant = ff_q_mdr_second_zero_minorsevaluationdeterminanthrb * S ((S (mdr_i_second_zero_minorsevaluationdeterminanth)) * mdr_c_second_zero_minorsevaluationdeterminant) + (mdr_z_second_zero_minorsevaluationdeterminanthr))))) /\ (((((mdr_d_second_zero_minorsevaluationdeterminanth) = 0) /\ (((mdr_p_second_zero_minorsevaluationdeterminanth) = 1) /\ ((mdr_n_second_zero_minorsevaluationdeterminanth) = 0))) \/ exists mdr_q_second_zero_minorsevaluationdeterminanths mdr_eb_second_zero_minorsevaluationdeterminanths mdr_ec_second_zero_minorsevaluationdeterminanths mdr_fb_second_zero_minorsevaluationdeterminanths mdr_fc_second_zero_minorsevaluationdeterminanths. (((mdr_d_second_zero_minorsevaluationdeterminanth) = S (mdr_q_second_zero_minorsevaluationdeterminanths)) /\ ((forall mdr_j_second_zero_minorsevaluationdeterminanthsc. (exists mdr_gap_second_zero_minorsevaluationdeterminanthscj. mdr_gap_second_zero_minorsevaluationdeterminanthscj + S (mdr_j_second_zero_minorsevaluationdeterminanthsc) = (S (mdr_q_second_zero_minorsevaluationdeterminanths))) -> exists mdr_i_second_zero_minorsevaluationdeterminanthsc mdr_up_second_zero_minorsevaluationdeterminanthsc mdr_us_second_zero_minorsevaluationdeterminanthsc mdr_un_second_zero_minorsevaluationdeterminanthsc mdr_ut_second_zero_minorsevaluationdeterminanthsc mdr_p_second_zero_minorsevaluationdeterminanthsc mdr_n_second_zero_minorsevaluationdeterminanthsc. ((exists mdr_gap_second_zero_minorsevaluationdeterminanthsci. mdr_gap_second_zero_minorsevaluationdeterminanthsci + S (mdr_i_second_zero_minorsevaluationdeterminanthsc) = (mdr_i_second_zero_minorsevaluationdeterminanth)) /\ ((exists mdr_z_second_zero_minorsevaluationdeterminanthscr. ((exists mdr_a_second_zero_minorsevaluationdeterminanthscrc mdr_b_second_zero_minorsevaluationdeterminanthscrc mdr_c_second_zero_minorsevaluationdeterminanthscrc mdr_e_second_zero_minorsevaluationdeterminanthscrc mdr_f_second_zero_minorsevaluationdeterminanthscrc. ((mdr_a_second_zero_minorsevaluationdeterminanthscrc = ((mdr_q_second_zero_minorsevaluationdeterminanths) + (mdr_up_second_zero_minorsevaluationdeterminanthsc)) * S ((mdr_q_second_zero_minorsevaluationdeterminanths) + (mdr_up_second_zero_minorsevaluationdeterminanthsc)) + ((mdr_up_second_zero_minorsevaluationdeterminanthsc) + (mdr_up_second_zero_minorsevaluationdeterminanthsc))) /\ ((mdr_b_second_zero_minorsevaluationdeterminanthscrc = ((mdr_us_second_zero_minorsevaluationdeterminanthsc) + (mdr_un_second_zero_minorsevaluationdeterminanthsc)) * S ((mdr_us_second_zero_minorsevaluationdeterminanthsc) + (mdr_un_second_zero_minorsevaluationdeterminanthsc)) + ((mdr_un_second_zero_minorsevaluationdeterminanthsc) + (mdr_un_second_zero_minorsevaluationdeterminanthsc))) /\ ((mdr_c_second_zero_minorsevaluationdeterminanthscrc = ((mdr_a_second_zero_minorsevaluationdeterminanthscrc) + (mdr_b_second_zero_minorsevaluationdeterminanthscrc)) * S ((mdr_a_second_zero_minorsevaluationdeterminanthscrc) + (mdr_b_second_zero_minorsevaluationdeterminanthscrc)) + ((mdr_b_second_zero_minorsevaluationdeterminanthscrc) + (mdr_b_second_zero_minorsevaluationdeterminanthscrc))) /\ ((mdr_e_second_zero_minorsevaluationdeterminanthscrc = ((mdr_p_second_zero_minorsevaluationdeterminanthsc) + (mdr_n_second_zero_minorsevaluationdeterminanthsc)) * S ((mdr_p_second_zero_minorsevaluationdeterminanthsc) + (mdr_n_second_zero_minorsevaluationdeterminanthsc)) + ((mdr_n_second_zero_minorsevaluationdeterminanthsc) + (mdr_n_second_zero_minorsevaluationdeterminanthsc))) /\ ((mdr_f_second_zero_minorsevaluationdeterminanthscrc = ((mdr_ut_second_zero_minorsevaluationdeterminanthsc) + (mdr_e_second_zero_minorsevaluationdeterminanthscrc)) * S ((mdr_ut_second_zero_minorsevaluationdeterminanthsc) + (mdr_e_second_zero_minorsevaluationdeterminanthscrc)) + ((mdr_e_second_zero_minorsevaluationdeterminanthscrc) + (mdr_e_second_zero_minorsevaluationdeterminanthscrc))) /\ ((mdr_z_second_zero_minorsevaluationdeterminanthscr) = ((mdr_c_second_zero_minorsevaluationdeterminanthscrc) + (mdr_f_second_zero_minorsevaluationdeterminanthscrc)) * S ((mdr_c_second_zero_minorsevaluationdeterminanthscrc) + (mdr_f_second_zero_minorsevaluationdeterminanthscrc)) + ((mdr_f_second_zero_minorsevaluationdeterminanthscrc) + (mdr_f_second_zero_minorsevaluationdeterminanthscrc))))))))) /\ (((exists ff_h_mdr_second_zero_minorsevaluationdeterminanthscrb. ff_h_mdr_second_zero_minorsevaluationdeterminanthscrb + S (mdr_z_second_zero_minorsevaluationdeterminanthscr) = S ((S (mdr_i_second_zero_minorsevaluationdeterminanthsc)) * mdr_c_second_zero_minorsevaluationdeterminant)) /\ exists ff_q_mdr_second_zero_minorsevaluationdeterminanthscrb. mdr_b_second_zero_minorsevaluationdeterminant = ff_q_mdr_second_zero_minorsevaluationdeterminanthscrb * S ((S (mdr_i_second_zero_minorsevaluationdeterminanthsc)) * mdr_c_second_zero_minorsevaluationdeterminant) + (mdr_z_second_zero_minorsevaluationdeterminanthscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_second_zero_minorsevaluationdeterminanthscm_positive. (exists ff_gap_mdm_lt_mdr_second_zero_minorsevaluationdeterminanthscm_positive_index_bound. ff_gap_mdm_lt_mdr_second_zero_minorsevaluationdeterminanthscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_second_zero_minorsevaluationdeterminanthscm_positive) = ((mdr_q_second_zero_minorsevaluationdeterminanths) * (mdr_q_second_zero_minorsevaluationdeterminanths))) -> exists ff_row_mdm_prefix_mdr_second_zero_minorsevaluationdeterminanthscm_positive ff_column_mdm_prefix_mdr_second_zero_minorsevaluationdeterminanthscm_positive ff_value_mdm_prefix_mdr_second_zero_minorsevaluationdeterminanthscm_positive. (ff_index_mdm_prefix_mdr_second_zero_minorsevaluationdeterminanthscm_positive = (mdr_q_second_zero_minorsevaluationdeterminanths) * ff_row_mdm_prefix_mdr_second_zero_minorsevaluationdeterminanthscm_positive + ff_column_mdm_prefix_mdr_second_zero_minorsevaluationdeterminanthscm_positive /\ ((exists ff_gap_mdm_lt_mdr_second_zero_minorsevaluationdeterminanthscm_positive_column_bound. ff_gap_mdm_lt_mdr_second_zero_minorsevaluationdeterminanthscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_second_zero_minorsevaluationdeterminanthscm_positive) = (mdr_q_second_zero_minorsevaluationdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_second_zero_minorsevaluationdeterminanthscm_positive_cell ff_column_mdm_cell_mdr_second_zero_minorsevaluationdeterminanthscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_second_zero_minorsevaluationdeterminanthscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_second_zero_minorsevaluationdeterminanthscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_second_zero_minorsevaluationdeterminanthscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_second_zero_minorsevaluationdeterminanthscm_positive_cell = ff_row_mdm_prefix_mdr_second_zero_minorsevaluationdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_second_zero_minorsevaluationdeterminanthscm_positive_cell_row_after. ff_gap_mdm_le_mdr_second_zero_minorsevaluationdeterminanthscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_second_zero_minorsevaluationdeterminanthscm_positive)) /\ ff_row_mdm_cell_mdr_second_zero_minorsevaluationdeterminanthscm_positive_cell = S ff_row_mdm_prefix_mdr_second_zero_minorsevaluationdeterminanthscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_second_zero_minorsevaluationdeterminanthscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_second_zero_minorsevaluationdeterminanthscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_second_zero_minorsevaluationdeterminanthscm_positive) = (mdr_j_second_zero_minorsevaluationdeterminanthsc)) /\ ff_column_mdm_cell_mdr_second_zero_minorsevaluationdeterminanthscm_positive_cell = ff_column_mdm_prefix_mdr_second_zero_minorsevaluationdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_second_zero_minorsevaluationdeterminanthscm_positive_cell_column_after. ff_gap_mdm_le_mdr_second_zero_minorsevaluationdeterminanthscm_positive_cell_column_after + (mdr_j_second_zero_minorsevaluationdeterminanthsc) = (ff_column_mdm_prefix_mdr_second_zero_minorsevaluationdeterminanthscm_positive)) /\ ff_column_mdm_cell_mdr_second_zero_minorsevaluationdeterminanthscm_positive_cell = S ff_column_mdm_prefix_mdr_second_zero_minorsevaluationdeterminanthscm_positive))) /\ (((exists ff_h_mdm_mdr_second_zero_minorsevaluationdeterminanthscm_positive_cell_source. ff_h_mdm_mdr_second_zero_minorsevaluationdeterminanthscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_second_zero_minorsevaluationdeterminanthscm_positive) = S ((S ((ff_row_mdm_cell_mdr_second_zero_minorsevaluationdeterminanthscm_positive_cell) * (S (mdr_q_second_zero_minorsevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_second_zero_minorsevaluationdeterminanthscm_positive_cell))) * mdr_pc_second_zero_minorsevaluationdeterminanth)) /\ exists ff_q_mdm_mdr_second_zero_minorsevaluationdeterminanthscm_positive_cell_source. mdr_pb_second_zero_minorsevaluationdeterminanth = ff_q_mdm_mdr_second_zero_minorsevaluationdeterminanthscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_second_zero_minorsevaluationdeterminanthscm_positive_cell) * (S (mdr_q_second_zero_minorsevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_second_zero_minorsevaluationdeterminanthscm_positive_cell))) * mdr_pc_second_zero_minorsevaluationdeterminanth) + (ff_value_mdm_prefix_mdr_second_zero_minorsevaluationdeterminanthscm_positive)))))) /\ (((exists ff_h_mdm_mdr_second_zero_minorsevaluationdeterminanthscm_positive_target. ff_h_mdm_mdr_second_zero_minorsevaluationdeterminanthscm_positive_target + S (ff_value_mdm_prefix_mdr_second_zero_minorsevaluationdeterminanthscm_positive) = S ((S (ff_index_mdm_prefix_mdr_second_zero_minorsevaluationdeterminanthscm_positive)) * mdr_us_second_zero_minorsevaluationdeterminanthsc)) /\ exists ff_q_mdm_mdr_second_zero_minorsevaluationdeterminanthscm_positive_target. mdr_up_second_zero_minorsevaluationdeterminanthsc = ff_q_mdm_mdr_second_zero_minorsevaluationdeterminanthscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_second_zero_minorsevaluationdeterminanthscm_positive)) * mdr_us_second_zero_minorsevaluationdeterminanthsc) + (ff_value_mdm_prefix_mdr_second_zero_minorsevaluationdeterminanthscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_second_zero_minorsevaluationdeterminanthscm_negative. (exists ff_gap_mdm_lt_mdr_second_zero_minorsevaluationdeterminanthscm_negative_index_bound. ff_gap_mdm_lt_mdr_second_zero_minorsevaluationdeterminanthscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_second_zero_minorsevaluationdeterminanthscm_negative) = ((mdr_q_second_zero_minorsevaluationdeterminanths) * (mdr_q_second_zero_minorsevaluationdeterminanths))) -> exists ff_row_mdm_prefix_mdr_second_zero_minorsevaluationdeterminanthscm_negative ff_column_mdm_prefix_mdr_second_zero_minorsevaluationdeterminanthscm_negative ff_value_mdm_prefix_mdr_second_zero_minorsevaluationdeterminanthscm_negative. (ff_index_mdm_prefix_mdr_second_zero_minorsevaluationdeterminanthscm_negative = (mdr_q_second_zero_minorsevaluationdeterminanths) * ff_row_mdm_prefix_mdr_second_zero_minorsevaluationdeterminanthscm_negative + ff_column_mdm_prefix_mdr_second_zero_minorsevaluationdeterminanthscm_negative /\ ((exists ff_gap_mdm_lt_mdr_second_zero_minorsevaluationdeterminanthscm_negative_column_bound. ff_gap_mdm_lt_mdr_second_zero_minorsevaluationdeterminanthscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_second_zero_minorsevaluationdeterminanthscm_negative) = (mdr_q_second_zero_minorsevaluationdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_second_zero_minorsevaluationdeterminanthscm_negative_cell ff_column_mdm_cell_mdr_second_zero_minorsevaluationdeterminanthscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_second_zero_minorsevaluationdeterminanthscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_second_zero_minorsevaluationdeterminanthscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_second_zero_minorsevaluationdeterminanthscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_second_zero_minorsevaluationdeterminanthscm_negative_cell = ff_row_mdm_prefix_mdr_second_zero_minorsevaluationdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_second_zero_minorsevaluationdeterminanthscm_negative_cell_row_after. ff_gap_mdm_le_mdr_second_zero_minorsevaluationdeterminanthscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_second_zero_minorsevaluationdeterminanthscm_negative)) /\ ff_row_mdm_cell_mdr_second_zero_minorsevaluationdeterminanthscm_negative_cell = S ff_row_mdm_prefix_mdr_second_zero_minorsevaluationdeterminanthscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_second_zero_minorsevaluationdeterminanthscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_second_zero_minorsevaluationdeterminanthscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_second_zero_minorsevaluationdeterminanthscm_negative) = (mdr_j_second_zero_minorsevaluationdeterminanthsc)) /\ ff_column_mdm_cell_mdr_second_zero_minorsevaluationdeterminanthscm_negative_cell = ff_column_mdm_prefix_mdr_second_zero_minorsevaluationdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_second_zero_minorsevaluationdeterminanthscm_negative_cell_column_after. ff_gap_mdm_le_mdr_second_zero_minorsevaluationdeterminanthscm_negative_cell_column_after + (mdr_j_second_zero_minorsevaluationdeterminanthsc) = (ff_column_mdm_prefix_mdr_second_zero_minorsevaluationdeterminanthscm_negative)) /\ ff_column_mdm_cell_mdr_second_zero_minorsevaluationdeterminanthscm_negative_cell = S ff_column_mdm_prefix_mdr_second_zero_minorsevaluationdeterminanthscm_negative))) /\ (((exists ff_h_mdm_mdr_second_zero_minorsevaluationdeterminanthscm_negative_cell_source. ff_h_mdm_mdr_second_zero_minorsevaluationdeterminanthscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_second_zero_minorsevaluationdeterminanthscm_negative) = S ((S ((ff_row_mdm_cell_mdr_second_zero_minorsevaluationdeterminanthscm_negative_cell) * (S (mdr_q_second_zero_minorsevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_second_zero_minorsevaluationdeterminanthscm_negative_cell))) * mdr_nc_second_zero_minorsevaluationdeterminanth)) /\ exists ff_q_mdm_mdr_second_zero_minorsevaluationdeterminanthscm_negative_cell_source. mdr_nb_second_zero_minorsevaluationdeterminanth = ff_q_mdm_mdr_second_zero_minorsevaluationdeterminanthscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_second_zero_minorsevaluationdeterminanthscm_negative_cell) * (S (mdr_q_second_zero_minorsevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_second_zero_minorsevaluationdeterminanthscm_negative_cell))) * mdr_nc_second_zero_minorsevaluationdeterminanth) + (ff_value_mdm_prefix_mdr_second_zero_minorsevaluationdeterminanthscm_negative)))))) /\ (((exists ff_h_mdm_mdr_second_zero_minorsevaluationdeterminanthscm_negative_target. ff_h_mdm_mdr_second_zero_minorsevaluationdeterminanthscm_negative_target + S (ff_value_mdm_prefix_mdr_second_zero_minorsevaluationdeterminanthscm_negative) = S ((S (ff_index_mdm_prefix_mdr_second_zero_minorsevaluationdeterminanthscm_negative)) * mdr_ut_second_zero_minorsevaluationdeterminanthsc)) /\ exists ff_q_mdm_mdr_second_zero_minorsevaluationdeterminanthscm_negative_target. mdr_un_second_zero_minorsevaluationdeterminanthsc = ff_q_mdm_mdr_second_zero_minorsevaluationdeterminanthscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_second_zero_minorsevaluationdeterminanthscm_negative)) * mdr_ut_second_zero_minorsevaluationdeterminanthsc) + (ff_value_mdm_prefix_mdr_second_zero_minorsevaluationdeterminanthscm_negative))))))))) /\ ((((exists ff_h_mdr_second_zero_minorsevaluationdeterminanthscp. ff_h_mdr_second_zero_minorsevaluationdeterminanthscp + S (mdr_p_second_zero_minorsevaluationdeterminanthsc) = S ((S (mdr_j_second_zero_minorsevaluationdeterminanthsc)) * mdr_ec_second_zero_minorsevaluationdeterminanths)) /\ exists ff_q_mdr_second_zero_minorsevaluationdeterminanthscp. mdr_eb_second_zero_minorsevaluationdeterminanths = ff_q_mdr_second_zero_minorsevaluationdeterminanthscp * S ((S (mdr_j_second_zero_minorsevaluationdeterminanthsc)) * mdr_ec_second_zero_minorsevaluationdeterminanths) + (mdr_p_second_zero_minorsevaluationdeterminanthsc))) /\ (((exists ff_h_mdr_second_zero_minorsevaluationdeterminanthscn. ff_h_mdr_second_zero_minorsevaluationdeterminanthscn + S (mdr_n_second_zero_minorsevaluationdeterminanthsc) = S ((S (mdr_j_second_zero_minorsevaluationdeterminanthsc)) * mdr_fc_second_zero_minorsevaluationdeterminanths)) /\ exists ff_q_mdr_second_zero_minorsevaluationdeterminanthscn. mdr_fb_second_zero_minorsevaluationdeterminanths = ff_q_mdr_second_zero_minorsevaluationdeterminanthscn * S ((S (mdr_j_second_zero_minorsevaluationdeterminanthsc)) * mdr_fc_second_zero_minorsevaluationdeterminanths) + (mdr_n_second_zero_minorsevaluationdeterminanthsc)))))))) /\ (exists ff_ub_mce_fold_mdr_second_zero_minorsevaluationdeterminanthsf ff_uc_mce_fold_mdr_second_zero_minorsevaluationdeterminanthsf ff_vb_mce_fold_mdr_second_zero_minorsevaluationdeterminanthsf ff_vc_mce_fold_mdr_second_zero_minorsevaluationdeterminanthsf. ((forall ff_index_mce_alternating_mdr_second_zero_minorsevaluationdeterminanthsf_prefix. (exists ff_gap_mce_mdr_second_zero_minorsevaluationdeterminanthsf_prefix_index. ff_gap_mce_mdr_second_zero_minorsevaluationdeterminanthsf_prefix_index + S (ff_index_mce_alternating_mdr_second_zero_minorsevaluationdeterminanthsf_prefix) = (S (mdr_q_second_zero_minorsevaluationdeterminanths))) -> exists ff_ap_mce_alternating_mdr_second_zero_minorsevaluationdeterminanthsf_prefix ff_an_mce_alternating_mdr_second_zero_minorsevaluationdeterminanthsf_prefix ff_bp_mce_alternating_mdr_second_zero_minorsevaluationdeterminanthsf_prefix ff_bn_mce_alternating_mdr_second_zero_minorsevaluationdeterminanthsf_prefix ff_p_mce_alternating_mdr_second_zero_minorsevaluationdeterminanthsf_prefix ff_n_mce_alternating_mdr_second_zero_minorsevaluationdeterminanthsf_prefix. ((((exists ff_h_mce_mdr_second_zero_minorsevaluationdeterminanthsf_prefix_ap. ff_h_mce_mdr_second_zero_minorsevaluationdeterminanthsf_prefix_ap + S (ff_ap_mce_alternating_mdr_second_zero_minorsevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_second_zero_minorsevaluationdeterminanthsf_prefix)) * mdr_pc_second_zero_minorsevaluationdeterminanth)) /\ exists ff_q_mce_mdr_second_zero_minorsevaluationdeterminanthsf_prefix_ap. mdr_pb_second_zero_minorsevaluationdeterminanth = ff_q_mce_mdr_second_zero_minorsevaluationdeterminanthsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_second_zero_minorsevaluationdeterminanthsf_prefix)) * mdr_pc_second_zero_minorsevaluationdeterminanth) + (ff_ap_mce_alternating_mdr_second_zero_minorsevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_second_zero_minorsevaluationdeterminanthsf_prefix_an. ff_h_mce_mdr_second_zero_minorsevaluationdeterminanthsf_prefix_an + S (ff_an_mce_alternating_mdr_second_zero_minorsevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_second_zero_minorsevaluationdeterminanthsf_prefix)) * mdr_nc_second_zero_minorsevaluationdeterminanth)) /\ exists ff_q_mce_mdr_second_zero_minorsevaluationdeterminanthsf_prefix_an. mdr_nb_second_zero_minorsevaluationdeterminanth = ff_q_mce_mdr_second_zero_minorsevaluationdeterminanthsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_second_zero_minorsevaluationdeterminanthsf_prefix)) * mdr_nc_second_zero_minorsevaluationdeterminanth) + (ff_an_mce_alternating_mdr_second_zero_minorsevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_second_zero_minorsevaluationdeterminanthsf_prefix_bp. ff_h_mce_mdr_second_zero_minorsevaluationdeterminanthsf_prefix_bp + S (ff_bp_mce_alternating_mdr_second_zero_minorsevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_second_zero_minorsevaluationdeterminanthsf_prefix)) * mdr_ec_second_zero_minorsevaluationdeterminanths)) /\ exists ff_q_mce_mdr_second_zero_minorsevaluationdeterminanthsf_prefix_bp. mdr_eb_second_zero_minorsevaluationdeterminanths = ff_q_mce_mdr_second_zero_minorsevaluationdeterminanthsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_second_zero_minorsevaluationdeterminanthsf_prefix)) * mdr_ec_second_zero_minorsevaluationdeterminanths) + (ff_bp_mce_alternating_mdr_second_zero_minorsevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_second_zero_minorsevaluationdeterminanthsf_prefix_bn. ff_h_mce_mdr_second_zero_minorsevaluationdeterminanthsf_prefix_bn + S (ff_bn_mce_alternating_mdr_second_zero_minorsevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_second_zero_minorsevaluationdeterminanthsf_prefix)) * mdr_fc_second_zero_minorsevaluationdeterminanths)) /\ exists ff_q_mce_mdr_second_zero_minorsevaluationdeterminanthsf_prefix_bn. mdr_fb_second_zero_minorsevaluationdeterminanths = ff_q_mce_mdr_second_zero_minorsevaluationdeterminanthsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_second_zero_minorsevaluationdeterminanthsf_prefix)) * mdr_fc_second_zero_minorsevaluationdeterminanths) + (ff_bn_mce_alternating_mdr_second_zero_minorsevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_second_zero_minorsevaluationdeterminanthsf_prefix_positive. ff_h_mce_mdr_second_zero_minorsevaluationdeterminanthsf_prefix_positive + S (ff_p_mce_alternating_mdr_second_zero_minorsevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_second_zero_minorsevaluationdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_second_zero_minorsevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_second_zero_minorsevaluationdeterminanthsf_prefix_positive. ff_ub_mce_fold_mdr_second_zero_minorsevaluationdeterminanthsf = ff_q_mce_mdr_second_zero_minorsevaluationdeterminanthsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_second_zero_minorsevaluationdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_second_zero_minorsevaluationdeterminanthsf) + (ff_p_mce_alternating_mdr_second_zero_minorsevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_second_zero_minorsevaluationdeterminanthsf_prefix_negative. ff_h_mce_mdr_second_zero_minorsevaluationdeterminanthsf_prefix_negative + S (ff_n_mce_alternating_mdr_second_zero_minorsevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_second_zero_minorsevaluationdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_second_zero_minorsevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_second_zero_minorsevaluationdeterminanthsf_prefix_negative. ff_vb_mce_fold_mdr_second_zero_minorsevaluationdeterminanthsf = ff_q_mce_mdr_second_zero_minorsevaluationdeterminanthsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_second_zero_minorsevaluationdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_second_zero_minorsevaluationdeterminanthsf) + (ff_n_mce_alternating_mdr_second_zero_minorsevaluationdeterminanthsf_prefix))) /\ (((exists ff_even_mce_term_mdr_second_zero_minorsevaluationdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_second_zero_minorsevaluationdeterminanthsf_prefix = 2 * ff_even_mce_term_mdr_second_zero_minorsevaluationdeterminanthsf_prefix_term) /\ (ff_p_mce_alternating_mdr_second_zero_minorsevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_second_zero_minorsevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_second_zero_minorsevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_second_zero_minorsevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_second_zero_minorsevaluationdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_second_zero_minorsevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_second_zero_minorsevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_second_zero_minorsevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_second_zero_minorsevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_second_zero_minorsevaluationdeterminanthsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_second_zero_minorsevaluationdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_second_zero_minorsevaluationdeterminanthsf_prefix = 2 * ff_odd_mce_term_mdr_second_zero_minorsevaluationdeterminanthsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_second_zero_minorsevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_second_zero_minorsevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_second_zero_minorsevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_second_zero_minorsevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_second_zero_minorsevaluationdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_second_zero_minorsevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_second_zero_minorsevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_second_zero_minorsevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_second_zero_minorsevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_second_zero_minorsevaluationdeterminanthsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_second_zero_minorsevaluationdeterminanthsf_positive ff_v_mce_mdr_second_zero_minorsevaluationdeterminanthsf_positive. ((((exists ff_h_mce_mdr_second_zero_minorsevaluationdeterminanthsf_positive_start. ff_h_mce_mdr_second_zero_minorsevaluationdeterminanthsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_second_zero_minorsevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_second_zero_minorsevaluationdeterminanthsf_positive_start. ff_u_mce_mdr_second_zero_minorsevaluationdeterminanthsf_positive = ff_q_mce_mdr_second_zero_minorsevaluationdeterminanthsf_positive_start * S ((S (0)) * ff_v_mce_mdr_second_zero_minorsevaluationdeterminanthsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_second_zero_minorsevaluationdeterminanthsf_positive_terminal. ff_h_mce_mdr_second_zero_minorsevaluationdeterminanthsf_positive_terminal + S (mdr_p_second_zero_minorsevaluationdeterminanth) = S ((S ((S (mdr_q_second_zero_minorsevaluationdeterminanths)))) * ff_v_mce_mdr_second_zero_minorsevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_second_zero_minorsevaluationdeterminanthsf_positive_terminal. ff_u_mce_mdr_second_zero_minorsevaluationdeterminanthsf_positive = ff_q_mce_mdr_second_zero_minorsevaluationdeterminanthsf_positive_terminal * S ((S ((S (mdr_q_second_zero_minorsevaluationdeterminanths)))) * ff_v_mce_mdr_second_zero_minorsevaluationdeterminanthsf_positive) + (mdr_p_second_zero_minorsevaluationdeterminanth))) /\ forall ff_i_mce_mdr_second_zero_minorsevaluationdeterminanthsf_positive. (exists ff_lt_mce_mdr_second_zero_minorsevaluationdeterminanthsf_positive_bound. ff_lt_mce_mdr_second_zero_minorsevaluationdeterminanthsf_positive_bound + S ff_i_mce_mdr_second_zero_minorsevaluationdeterminanthsf_positive = (S (mdr_q_second_zero_minorsevaluationdeterminanths))) -> exists ff_a_mce_mdr_second_zero_minorsevaluationdeterminanthsf_positive ff_r_mce_mdr_second_zero_minorsevaluationdeterminanthsf_positive ff_s_mce_mdr_second_zero_minorsevaluationdeterminanthsf_positive. ((((exists ff_h_mce_mdr_second_zero_minorsevaluationdeterminanthsf_positive_summand. ff_h_mce_mdr_second_zero_minorsevaluationdeterminanthsf_positive_summand + S (ff_a_mce_mdr_second_zero_minorsevaluationdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_second_zero_minorsevaluationdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_second_zero_minorsevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_second_zero_minorsevaluationdeterminanthsf_positive_summand. ff_ub_mce_fold_mdr_second_zero_minorsevaluationdeterminanthsf = ff_q_mce_mdr_second_zero_minorsevaluationdeterminanthsf_positive_summand * S ((S (ff_i_mce_mdr_second_zero_minorsevaluationdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_second_zero_minorsevaluationdeterminanthsf) + (ff_a_mce_mdr_second_zero_minorsevaluationdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_second_zero_minorsevaluationdeterminanthsf_positive_partial. ff_h_mce_mdr_second_zero_minorsevaluationdeterminanthsf_positive_partial + S (ff_r_mce_mdr_second_zero_minorsevaluationdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_second_zero_minorsevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_second_zero_minorsevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_second_zero_minorsevaluationdeterminanthsf_positive_partial. ff_u_mce_mdr_second_zero_minorsevaluationdeterminanthsf_positive = ff_q_mce_mdr_second_zero_minorsevaluationdeterminanthsf_positive_partial * S ((S (ff_i_mce_mdr_second_zero_minorsevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_second_zero_minorsevaluationdeterminanthsf_positive) + (ff_r_mce_mdr_second_zero_minorsevaluationdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_second_zero_minorsevaluationdeterminanthsf_positive_successor. ff_h_mce_mdr_second_zero_minorsevaluationdeterminanthsf_positive_successor + S (ff_s_mce_mdr_second_zero_minorsevaluationdeterminanthsf_positive) = S ((S (S ff_i_mce_mdr_second_zero_minorsevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_second_zero_minorsevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_second_zero_minorsevaluationdeterminanthsf_positive_successor. ff_u_mce_mdr_second_zero_minorsevaluationdeterminanthsf_positive = ff_q_mce_mdr_second_zero_minorsevaluationdeterminanthsf_positive_successor * S ((S (S ff_i_mce_mdr_second_zero_minorsevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_second_zero_minorsevaluationdeterminanthsf_positive) + (ff_s_mce_mdr_second_zero_minorsevaluationdeterminanthsf_positive))) /\ ff_s_mce_mdr_second_zero_minorsevaluationdeterminanthsf_positive = ff_r_mce_mdr_second_zero_minorsevaluationdeterminanthsf_positive + ff_a_mce_mdr_second_zero_minorsevaluationdeterminanthsf_positive)))))) /\ (exists ff_u_mce_mdr_second_zero_minorsevaluationdeterminanthsf_negative ff_v_mce_mdr_second_zero_minorsevaluationdeterminanthsf_negative. ((((exists ff_h_mce_mdr_second_zero_minorsevaluationdeterminanthsf_negative_start. ff_h_mce_mdr_second_zero_minorsevaluationdeterminanthsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_second_zero_minorsevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_second_zero_minorsevaluationdeterminanthsf_negative_start. ff_u_mce_mdr_second_zero_minorsevaluationdeterminanthsf_negative = ff_q_mce_mdr_second_zero_minorsevaluationdeterminanthsf_negative_start * S ((S (0)) * ff_v_mce_mdr_second_zero_minorsevaluationdeterminanthsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_second_zero_minorsevaluationdeterminanthsf_negative_terminal. ff_h_mce_mdr_second_zero_minorsevaluationdeterminanthsf_negative_terminal + S (mdr_n_second_zero_minorsevaluationdeterminanth) = S ((S ((S (mdr_q_second_zero_minorsevaluationdeterminanths)))) * ff_v_mce_mdr_second_zero_minorsevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_second_zero_minorsevaluationdeterminanthsf_negative_terminal. ff_u_mce_mdr_second_zero_minorsevaluationdeterminanthsf_negative = ff_q_mce_mdr_second_zero_minorsevaluationdeterminanthsf_negative_terminal * S ((S ((S (mdr_q_second_zero_minorsevaluationdeterminanths)))) * ff_v_mce_mdr_second_zero_minorsevaluationdeterminanthsf_negative) + (mdr_n_second_zero_minorsevaluationdeterminanth))) /\ forall ff_i_mce_mdr_second_zero_minorsevaluationdeterminanthsf_negative. (exists ff_lt_mce_mdr_second_zero_minorsevaluationdeterminanthsf_negative_bound. ff_lt_mce_mdr_second_zero_minorsevaluationdeterminanthsf_negative_bound + S ff_i_mce_mdr_second_zero_minorsevaluationdeterminanthsf_negative = (S (mdr_q_second_zero_minorsevaluationdeterminanths))) -> exists ff_a_mce_mdr_second_zero_minorsevaluationdeterminanthsf_negative ff_r_mce_mdr_second_zero_minorsevaluationdeterminanthsf_negative ff_s_mce_mdr_second_zero_minorsevaluationdeterminanthsf_negative. ((((exists ff_h_mce_mdr_second_zero_minorsevaluationdeterminanthsf_negative_summand. ff_h_mce_mdr_second_zero_minorsevaluationdeterminanthsf_negative_summand + S (ff_a_mce_mdr_second_zero_minorsevaluationdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_second_zero_minorsevaluationdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_second_zero_minorsevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_second_zero_minorsevaluationdeterminanthsf_negative_summand. ff_vb_mce_fold_mdr_second_zero_minorsevaluationdeterminanthsf = ff_q_mce_mdr_second_zero_minorsevaluationdeterminanthsf_negative_summand * S ((S (ff_i_mce_mdr_second_zero_minorsevaluationdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_second_zero_minorsevaluationdeterminanthsf) + (ff_a_mce_mdr_second_zero_minorsevaluationdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_second_zero_minorsevaluationdeterminanthsf_negative_partial. ff_h_mce_mdr_second_zero_minorsevaluationdeterminanthsf_negative_partial + S (ff_r_mce_mdr_second_zero_minorsevaluationdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_second_zero_minorsevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_second_zero_minorsevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_second_zero_minorsevaluationdeterminanthsf_negative_partial. ff_u_mce_mdr_second_zero_minorsevaluationdeterminanthsf_negative = ff_q_mce_mdr_second_zero_minorsevaluationdeterminanthsf_negative_partial * S ((S (ff_i_mce_mdr_second_zero_minorsevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_second_zero_minorsevaluationdeterminanthsf_negative) + (ff_r_mce_mdr_second_zero_minorsevaluationdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_second_zero_minorsevaluationdeterminanthsf_negative_successor. ff_h_mce_mdr_second_zero_minorsevaluationdeterminanthsf_negative_successor + S (ff_s_mce_mdr_second_zero_minorsevaluationdeterminanthsf_negative) = S ((S (S ff_i_mce_mdr_second_zero_minorsevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_second_zero_minorsevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_second_zero_minorsevaluationdeterminanthsf_negative_successor. ff_u_mce_mdr_second_zero_minorsevaluationdeterminanthsf_negative = ff_q_mce_mdr_second_zero_minorsevaluationdeterminanthsf_negative_successor * S ((S (S ff_i_mce_mdr_second_zero_minorsevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_second_zero_minorsevaluationdeterminanthsf_negative) + (ff_s_mce_mdr_second_zero_minorsevaluationdeterminanthsf_negative))) /\ ff_s_mce_mdr_second_zero_minorsevaluationdeterminanthsf_negative = ff_r_mce_mdr_second_zero_minorsevaluationdeterminanthsf_negative + ff_a_mce_mdr_second_zero_minorsevaluationdeterminanthsf_negative))))))))))))))) /\ ((exists mdr_gap_second_zero_minorsevaluationdeterminanti. mdr_gap_second_zero_minorsevaluationdeterminanti + S (mdr_i_second_zero_minorsevaluationdeterminant) = (mdr_l_second_zero_minorsevaluationdeterminant)) /\ (exists mdr_z_second_zero_minorsevaluationdeterminantr. ((exists mdr_a_second_zero_minorsevaluationdeterminantrc mdr_b_second_zero_minorsevaluationdeterminantrc mdr_c_second_zero_minorsevaluationdeterminantrc mdr_e_second_zero_minorsevaluationdeterminantrc mdr_f_second_zero_minorsevaluationdeterminantrc. ((mdr_a_second_zero_minorsevaluationdeterminantrc = ((q) + (mdr_ub_second_zero_minorsevaluation)) * S ((q) + (mdr_ub_second_zero_minorsevaluation)) + ((mdr_ub_second_zero_minorsevaluation) + (mdr_ub_second_zero_minorsevaluation))) /\ ((mdr_b_second_zero_minorsevaluationdeterminantrc = ((mdr_uc_second_zero_minorsevaluation) + (mdr_vb_second_zero_minorsevaluation)) * S ((mdr_uc_second_zero_minorsevaluation) + (mdr_vb_second_zero_minorsevaluation)) + ((mdr_vb_second_zero_minorsevaluation) + (mdr_vb_second_zero_minorsevaluation))) /\ ((mdr_c_second_zero_minorsevaluationdeterminantrc = ((mdr_a_second_zero_minorsevaluationdeterminantrc) + (mdr_b_second_zero_minorsevaluationdeterminantrc)) * S ((mdr_a_second_zero_minorsevaluationdeterminantrc) + (mdr_b_second_zero_minorsevaluationdeterminantrc)) + ((mdr_b_second_zero_minorsevaluationdeterminantrc) + (mdr_b_second_zero_minorsevaluationdeterminantrc))) /\ ((mdr_e_second_zero_minorsevaluationdeterminantrc = ((mdr_p_second_zero_minors) + (mdr_n_second_zero_minors)) * S ((mdr_p_second_zero_minors) + (mdr_n_second_zero_minors)) + ((mdr_n_second_zero_minors) + (mdr_n_second_zero_minors))) /\ ((mdr_f_second_zero_minorsevaluationdeterminantrc = ((mdr_vc_second_zero_minorsevaluation) + (mdr_e_second_zero_minorsevaluationdeterminantrc)) * S ((mdr_vc_second_zero_minorsevaluation) + (mdr_e_second_zero_minorsevaluationdeterminantrc)) + ((mdr_e_second_zero_minorsevaluationdeterminantrc) + (mdr_e_second_zero_minorsevaluationdeterminantrc))) /\ ((mdr_z_second_zero_minorsevaluationdeterminantr) = ((mdr_c_second_zero_minorsevaluationdeterminantrc) + (mdr_f_second_zero_minorsevaluationdeterminantrc)) * S ((mdr_c_second_zero_minorsevaluationdeterminantrc) + (mdr_f_second_zero_minorsevaluationdeterminantrc)) + ((mdr_f_second_zero_minorsevaluationdeterminantrc) + (mdr_f_second_zero_minorsevaluationdeterminantrc))))))))) /\ (((exists ff_h_mdr_second_zero_minorsevaluationdeterminantrb. ff_h_mdr_second_zero_minorsevaluationdeterminantrb + S (mdr_z_second_zero_minorsevaluationdeterminantr) = S ((S (mdr_i_second_zero_minorsevaluationdeterminant)) * mdr_c_second_zero_minorsevaluationdeterminant)) /\ exists ff_q_mdr_second_zero_minorsevaluationdeterminantrb. mdr_b_second_zero_minorsevaluationdeterminant = ff_q_mdr_second_zero_minorsevaluationdeterminantrb * S ((S (mdr_i_second_zero_minorsevaluationdeterminant)) * mdr_c_second_zero_minorsevaluationdeterminant) + (mdr_z_second_zero_minorsevaluationdeterminantr)))))))))) -> mdr_p_second_zero_minors = mdr_n_second_zero_minors)