Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.
This branch proves the finite determinant/rank/span substrate. It does not claim Smith or Hermite normal form, lattice index equals determinant, determinant multiplicativity, lattice reduction, or geometry-of-numbers theorems.
Exact theorem in conservative defined notation
∀ ab. ∀ ac. ∀ bb. ∀ bc. ∀ eb. ∀ ec. ∀ fb. ∀ fc. ∀ r. ∀ w. ∀ q. IntegerMatrixEntrywiseEqual(ab,ac,bb,bc,eb,ec,fb,fc,r,w) → AllSignedMinorsZero(ab,ac,bb,bc,r,w,q) → AllSignedMinorsZero(eb,ec,fb,fc,r,w,q)Every linked abbreviation expands hygienically to the identical original native formula.
Definition DAG
Actual proof prerequisites
Original expanded first-order 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)Complete tactic proof in conservative notation
All 55 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.
Read the argument
Proof checkpoints
55 script commands · 8 reading checkpoints · 0 local claims
This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.
Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.
Named ingredients (4)
01Fix variables and assumptionsL1–10
02Fix variables and assumptionsL11–13
03Use earlier factsL14–21
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L14
specialize matrix_rank_all_minors_zero_from_absence (eb) - L15
specialize matrix_rank_all_minors_zero_from_absence (ec) - L16
specialize matrix_rank_all_minors_zero_from_absence (fb) - L17
specialize matrix_rank_all_minors_zero_from_absence (fc) - L18
specialize matrix_rank_all_minors_zero_from_absence (r) - L19
specialize matrix_rank_all_minors_zero_from_absence (w) - L20
specialize matrix_rank_all_minors_zero_from_absence (q) - L21
apply matrix_rank_all_minors_zero_from_absence
04Fix variables and assumptionsL22–22
Work with arbitrary variables or the premises of the current implication.
- L22
intro hminor
05Use earlier factsL23–32
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L23
specialize matrix_rank_absence_from_all_minors_zero (ab) - L24
specialize matrix_rank_absence_from_all_minors_zero (ac) - L25
specialize matrix_rank_absence_from_all_minors_zero (bb) - L26
specialize matrix_rank_absence_from_all_minors_zero (bc) - L27
specialize matrix_rank_absence_from_all_minors_zero (r) - L28
specialize matrix_rank_absence_from_all_minors_zero (w) - L29
specialize matrix_rank_absence_from_all_minors_zero (q) - L30
apply matrix_rank_absence_from_all_minors_zero - L31
exact hzero - L32
specialize matrix_integer_nonzero_minor_transport (eb)
06Use earlier factsL33–42
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L33
specialize matrix_integer_nonzero_minor_transport (ec) - L34
specialize matrix_integer_nonzero_minor_transport (fb) - L35
specialize matrix_integer_nonzero_minor_transport (fc) - L36
specialize matrix_integer_nonzero_minor_transport (ab) - L37
specialize matrix_integer_nonzero_minor_transport (ac) - L38
specialize matrix_integer_nonzero_minor_transport (bb) - L39
specialize matrix_integer_nonzero_minor_transport (bc) - L40
specialize matrix_integer_nonzero_minor_transport (r) - L41
specialize matrix_integer_nonzero_minor_transport (w) - L42
specialize matrix_integer_nonzero_minor_transport (q)
07Use earlier factsL43–52
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L43
apply matrix_integer_nonzero_minor_transport - L44
specialize matrix_integer_vector_equality_symmetric (ab) - L45
specialize matrix_integer_vector_equality_symmetric (ac) - L46
specialize matrix_integer_vector_equality_symmetric (bb) - L47
specialize matrix_integer_vector_equality_symmetric (bc) - L48
specialize matrix_integer_vector_equality_symmetric (eb) - L49
specialize matrix_integer_vector_equality_symmetric (ec) - L50
specialize matrix_integer_vector_equality_symmetric (fb) - L51
specialize matrix_integer_vector_equality_symmetric (fc) - L52
specialize matrix_integer_vector_equality_symmetric (r * w)
Original defined command ledger · 55 lines
- 0001
intro ab - 0002
intro ac - 0003
intro bb - 0004
intro bc - 0005
intro eb - 0006
intro ec - 0007
intro fb - 0008
intro fc - 0009
intro r - 0010
intro w - 0011
intro q - 0012
intro hequal - 0013
intro hzero - 0014
specialize matrix_rank_all_minors_zero_from_absence (eb) - 0015
specialize matrix_rank_all_minors_zero_from_absence (ec) - 0016
specialize matrix_rank_all_minors_zero_from_absence (fb) - 0017
specialize matrix_rank_all_minors_zero_from_absence (fc) - 0018
specialize matrix_rank_all_minors_zero_from_absence (r) - 0019
specialize matrix_rank_all_minors_zero_from_absence (w) - 0020
specialize matrix_rank_all_minors_zero_from_absence (q) - 0021
apply matrix_rank_all_minors_zero_from_absence - 0022
intro hminor - 0023
specialize matrix_rank_absence_from_all_minors_zero (ab) - 0024
specialize matrix_rank_absence_from_all_minors_zero (ac) - 0025
specialize matrix_rank_absence_from_all_minors_zero (bb) - 0026
specialize matrix_rank_absence_from_all_minors_zero (bc) - 0027
specialize matrix_rank_absence_from_all_minors_zero (r) - 0028
specialize matrix_rank_absence_from_all_minors_zero (w) - 0029
specialize matrix_rank_absence_from_all_minors_zero (q) - 0030
apply matrix_rank_absence_from_all_minors_zero - 0031
exact hzero - 0032
specialize matrix_integer_nonzero_minor_transport (eb) - 0033
specialize matrix_integer_nonzero_minor_transport (ec) - 0034
specialize matrix_integer_nonzero_minor_transport (fb) - 0035
specialize matrix_integer_nonzero_minor_transport (fc) - 0036
specialize matrix_integer_nonzero_minor_transport (ab) - 0037
specialize matrix_integer_nonzero_minor_transport (ac) - 0038
specialize matrix_integer_nonzero_minor_transport (bb) - 0039
specialize matrix_integer_nonzero_minor_transport (bc) - 0040
specialize matrix_integer_nonzero_minor_transport (r) - 0041
specialize matrix_integer_nonzero_minor_transport (w) - 0042
specialize matrix_integer_nonzero_minor_transport (q) - 0043
apply matrix_integer_nonzero_minor_transport - 0044
specialize matrix_integer_vector_equality_symmetric (ab) - 0045
specialize matrix_integer_vector_equality_symmetric (ac) - 0046
specialize matrix_integer_vector_equality_symmetric (bb) - 0047
specialize matrix_integer_vector_equality_symmetric (bc) - 0048
specialize matrix_integer_vector_equality_symmetric (eb) - 0049
specialize matrix_integer_vector_equality_symmetric (ec) - 0050
specialize matrix_integer_vector_equality_symmetric (fb) - 0051
specialize matrix_integer_vector_equality_symmetric (fc) - 0052
specialize matrix_integer_vector_equality_symmetric (r * w) - 0053
apply matrix_integer_vector_equality_symmetric - 0054
exact hequal - 0055
exact hminor