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. ∀ d. ∀ p. ∀ n. SignedRecursiveDeterminant(ab,ac,bb,bc,d,p,n) → ¬p = n → NonzeroMatrixMinor(ab,ac,bb,bc,d,d,d)Every linked abbreviation expands hygienically to the identical original native formula.
Definition DAG
Actual proof prerequisites
eq_decidable · checked external prerequisitematrix_rank_nonzero_minor_emptymatrix_lattice_identity_selector_existsmatrix_lattice_identity_is_selectormatrix_lattice_identity_selected_signed
Original expanded first-order statement
forall ab ac bb bc d p n. (exists mdr_b_full_determinant mdr_c_full_determinant mdr_l_full_determinant mdr_i_full_determinant. ((forall mdr_i_full_determinanth. (exists mdr_gap_full_determinanthi. mdr_gap_full_determinanthi + S (mdr_i_full_determinanth) = (mdr_l_full_determinant)) -> exists mdr_d_full_determinanth mdr_pb_full_determinanth mdr_pc_full_determinanth mdr_nb_full_determinanth mdr_nc_full_determinanth mdr_p_full_determinanth mdr_n_full_determinanth. ((exists mdr_z_full_determinanthr. ((exists mdr_a_full_determinanthrc mdr_b_full_determinanthrc mdr_c_full_determinanthrc mdr_e_full_determinanthrc mdr_f_full_determinanthrc. ((mdr_a_full_determinanthrc = ((mdr_d_full_determinanth) + (mdr_pb_full_determinanth)) * S ((mdr_d_full_determinanth) + (mdr_pb_full_determinanth)) + ((mdr_pb_full_determinanth) + (mdr_pb_full_determinanth))) /\ ((mdr_b_full_determinanthrc = ((mdr_pc_full_determinanth) + (mdr_nb_full_determinanth)) * S ((mdr_pc_full_determinanth) + (mdr_nb_full_determinanth)) + ((mdr_nb_full_determinanth) + (mdr_nb_full_determinanth))) /\ ((mdr_c_full_determinanthrc = ((mdr_a_full_determinanthrc) + (mdr_b_full_determinanthrc)) * S ((mdr_a_full_determinanthrc) + (mdr_b_full_determinanthrc)) + ((mdr_b_full_determinanthrc) + (mdr_b_full_determinanthrc))) /\ ((mdr_e_full_determinanthrc = ((mdr_p_full_determinanth) + (mdr_n_full_determinanth)) * S ((mdr_p_full_determinanth) + (mdr_n_full_determinanth)) + ((mdr_n_full_determinanth) + (mdr_n_full_determinanth))) /\ ((mdr_f_full_determinanthrc = ((mdr_nc_full_determinanth) + (mdr_e_full_determinanthrc)) * S ((mdr_nc_full_determinanth) + (mdr_e_full_determinanthrc)) + ((mdr_e_full_determinanthrc) + (mdr_e_full_determinanthrc))) /\ ((mdr_z_full_determinanthr) = ((mdr_c_full_determinanthrc) + (mdr_f_full_determinanthrc)) * S ((mdr_c_full_determinanthrc) + (mdr_f_full_determinanthrc)) + ((mdr_f_full_determinanthrc) + (mdr_f_full_determinanthrc))))))))) /\ (((exists ff_h_mdr_full_determinanthrb. ff_h_mdr_full_determinanthrb + S (mdr_z_full_determinanthr) = S ((S (mdr_i_full_determinanth)) * mdr_c_full_determinant)) /\ exists ff_q_mdr_full_determinanthrb. mdr_b_full_determinant = ff_q_mdr_full_determinanthrb * S ((S (mdr_i_full_determinanth)) * mdr_c_full_determinant) + (mdr_z_full_determinanthr))))) /\ (((((mdr_d_full_determinanth) = 0) /\ (((mdr_p_full_determinanth) = 1) /\ ((mdr_n_full_determinanth) = 0))) \/ exists mdr_q_full_determinanths mdr_eb_full_determinanths mdr_ec_full_determinanths mdr_fb_full_determinanths mdr_fc_full_determinanths. (((mdr_d_full_determinanth) = S (mdr_q_full_determinanths)) /\ ((forall mdr_j_full_determinanthsc. (exists mdr_gap_full_determinanthscj. mdr_gap_full_determinanthscj + S (mdr_j_full_determinanthsc) = (S (mdr_q_full_determinanths))) -> exists mdr_i_full_determinanthsc mdr_up_full_determinanthsc mdr_us_full_determinanthsc mdr_un_full_determinanthsc mdr_ut_full_determinanthsc mdr_p_full_determinanthsc mdr_n_full_determinanthsc. ((exists mdr_gap_full_determinanthsci. mdr_gap_full_determinanthsci + S (mdr_i_full_determinanthsc) = (mdr_i_full_determinanth)) /\ ((exists mdr_z_full_determinanthscr. ((exists mdr_a_full_determinanthscrc mdr_b_full_determinanthscrc mdr_c_full_determinanthscrc mdr_e_full_determinanthscrc mdr_f_full_determinanthscrc. ((mdr_a_full_determinanthscrc = ((mdr_q_full_determinanths) + (mdr_up_full_determinanthsc)) * S ((mdr_q_full_determinanths) + (mdr_up_full_determinanthsc)) + ((mdr_up_full_determinanthsc) + (mdr_up_full_determinanthsc))) /\ ((mdr_b_full_determinanthscrc = ((mdr_us_full_determinanthsc) + (mdr_un_full_determinanthsc)) * S ((mdr_us_full_determinanthsc) + (mdr_un_full_determinanthsc)) + ((mdr_un_full_determinanthsc) + (mdr_un_full_determinanthsc))) /\ ((mdr_c_full_determinanthscrc = ((mdr_a_full_determinanthscrc) + (mdr_b_full_determinanthscrc)) * S ((mdr_a_full_determinanthscrc) + (mdr_b_full_determinanthscrc)) + ((mdr_b_full_determinanthscrc) + (mdr_b_full_determinanthscrc))) /\ ((mdr_e_full_determinanthscrc = ((mdr_p_full_determinanthsc) + (mdr_n_full_determinanthsc)) * S ((mdr_p_full_determinanthsc) + (mdr_n_full_determinanthsc)) + ((mdr_n_full_determinanthsc) + (mdr_n_full_determinanthsc))) /\ ((mdr_f_full_determinanthscrc = ((mdr_ut_full_determinanthsc) + (mdr_e_full_determinanthscrc)) * S ((mdr_ut_full_determinanthsc) + (mdr_e_full_determinanthscrc)) + ((mdr_e_full_determinanthscrc) + (mdr_e_full_determinanthscrc))) /\ ((mdr_z_full_determinanthscr) = ((mdr_c_full_determinanthscrc) + (mdr_f_full_determinanthscrc)) * S ((mdr_c_full_determinanthscrc) + (mdr_f_full_determinanthscrc)) + ((mdr_f_full_determinanthscrc) + (mdr_f_full_determinanthscrc))))))))) /\ (((exists ff_h_mdr_full_determinanthscrb. ff_h_mdr_full_determinanthscrb + S (mdr_z_full_determinanthscr) = S ((S (mdr_i_full_determinanthsc)) * mdr_c_full_determinant)) /\ exists ff_q_mdr_full_determinanthscrb. mdr_b_full_determinant = ff_q_mdr_full_determinanthscrb * S ((S (mdr_i_full_determinanthsc)) * mdr_c_full_determinant) + (mdr_z_full_determinanthscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_full_determinanthscm_positive. (exists ff_gap_mdm_lt_mdr_full_determinanthscm_positive_index_bound. ff_gap_mdm_lt_mdr_full_determinanthscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_full_determinanthscm_positive) = ((mdr_q_full_determinanths) * (mdr_q_full_determinanths))) -> exists ff_row_mdm_prefix_mdr_full_determinanthscm_positive ff_column_mdm_prefix_mdr_full_determinanthscm_positive ff_value_mdm_prefix_mdr_full_determinanthscm_positive. (ff_index_mdm_prefix_mdr_full_determinanthscm_positive = (mdr_q_full_determinanths) * ff_row_mdm_prefix_mdr_full_determinanthscm_positive + ff_column_mdm_prefix_mdr_full_determinanthscm_positive /\ ((exists ff_gap_mdm_lt_mdr_full_determinanthscm_positive_column_bound. ff_gap_mdm_lt_mdr_full_determinanthscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_full_determinanthscm_positive) = (mdr_q_full_determinanths)) /\ ((exists ff_row_mdm_cell_mdr_full_determinanthscm_positive_cell ff_column_mdm_cell_mdr_full_determinanthscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_full_determinanthscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_full_determinanthscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_full_determinanthscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_full_determinanthscm_positive_cell = ff_row_mdm_prefix_mdr_full_determinanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_full_determinanthscm_positive_cell_row_after. ff_gap_mdm_le_mdr_full_determinanthscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_full_determinanthscm_positive)) /\ ff_row_mdm_cell_mdr_full_determinanthscm_positive_cell = S ff_row_mdm_prefix_mdr_full_determinanthscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_full_determinanthscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_full_determinanthscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_full_determinanthscm_positive) = (mdr_j_full_determinanthsc)) /\ ff_column_mdm_cell_mdr_full_determinanthscm_positive_cell = ff_column_mdm_prefix_mdr_full_determinanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_full_determinanthscm_positive_cell_column_after. ff_gap_mdm_le_mdr_full_determinanthscm_positive_cell_column_after + (mdr_j_full_determinanthsc) = (ff_column_mdm_prefix_mdr_full_determinanthscm_positive)) /\ ff_column_mdm_cell_mdr_full_determinanthscm_positive_cell = S ff_column_mdm_prefix_mdr_full_determinanthscm_positive))) /\ (((exists ff_h_mdm_mdr_full_determinanthscm_positive_cell_source. ff_h_mdm_mdr_full_determinanthscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_full_determinanthscm_positive) = S ((S ((ff_row_mdm_cell_mdr_full_determinanthscm_positive_cell) * (S (mdr_q_full_determinanths)) + (ff_column_mdm_cell_mdr_full_determinanthscm_positive_cell))) * mdr_pc_full_determinanth)) /\ exists ff_q_mdm_mdr_full_determinanthscm_positive_cell_source. mdr_pb_full_determinanth = ff_q_mdm_mdr_full_determinanthscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_full_determinanthscm_positive_cell) * (S (mdr_q_full_determinanths)) + (ff_column_mdm_cell_mdr_full_determinanthscm_positive_cell))) * mdr_pc_full_determinanth) + (ff_value_mdm_prefix_mdr_full_determinanthscm_positive)))))) /\ (((exists ff_h_mdm_mdr_full_determinanthscm_positive_target. ff_h_mdm_mdr_full_determinanthscm_positive_target + S (ff_value_mdm_prefix_mdr_full_determinanthscm_positive) = S ((S (ff_index_mdm_prefix_mdr_full_determinanthscm_positive)) * mdr_us_full_determinanthsc)) /\ exists ff_q_mdm_mdr_full_determinanthscm_positive_target. mdr_up_full_determinanthsc = ff_q_mdm_mdr_full_determinanthscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_full_determinanthscm_positive)) * mdr_us_full_determinanthsc) + (ff_value_mdm_prefix_mdr_full_determinanthscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_full_determinanthscm_negative. (exists ff_gap_mdm_lt_mdr_full_determinanthscm_negative_index_bound. ff_gap_mdm_lt_mdr_full_determinanthscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_full_determinanthscm_negative) = ((mdr_q_full_determinanths) * (mdr_q_full_determinanths))) -> exists ff_row_mdm_prefix_mdr_full_determinanthscm_negative ff_column_mdm_prefix_mdr_full_determinanthscm_negative ff_value_mdm_prefix_mdr_full_determinanthscm_negative. (ff_index_mdm_prefix_mdr_full_determinanthscm_negative = (mdr_q_full_determinanths) * ff_row_mdm_prefix_mdr_full_determinanthscm_negative + ff_column_mdm_prefix_mdr_full_determinanthscm_negative /\ ((exists ff_gap_mdm_lt_mdr_full_determinanthscm_negative_column_bound. ff_gap_mdm_lt_mdr_full_determinanthscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_full_determinanthscm_negative) = (mdr_q_full_determinanths)) /\ ((exists ff_row_mdm_cell_mdr_full_determinanthscm_negative_cell ff_column_mdm_cell_mdr_full_determinanthscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_full_determinanthscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_full_determinanthscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_full_determinanthscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_full_determinanthscm_negative_cell = ff_row_mdm_prefix_mdr_full_determinanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_full_determinanthscm_negative_cell_row_after. ff_gap_mdm_le_mdr_full_determinanthscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_full_determinanthscm_negative)) /\ ff_row_mdm_cell_mdr_full_determinanthscm_negative_cell = S ff_row_mdm_prefix_mdr_full_determinanthscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_full_determinanthscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_full_determinanthscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_full_determinanthscm_negative) = (mdr_j_full_determinanthsc)) /\ ff_column_mdm_cell_mdr_full_determinanthscm_negative_cell = ff_column_mdm_prefix_mdr_full_determinanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_full_determinanthscm_negative_cell_column_after. ff_gap_mdm_le_mdr_full_determinanthscm_negative_cell_column_after + (mdr_j_full_determinanthsc) = (ff_column_mdm_prefix_mdr_full_determinanthscm_negative)) /\ ff_column_mdm_cell_mdr_full_determinanthscm_negative_cell = S ff_column_mdm_prefix_mdr_full_determinanthscm_negative))) /\ (((exists ff_h_mdm_mdr_full_determinanthscm_negative_cell_source. ff_h_mdm_mdr_full_determinanthscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_full_determinanthscm_negative) = S ((S ((ff_row_mdm_cell_mdr_full_determinanthscm_negative_cell) * (S (mdr_q_full_determinanths)) + (ff_column_mdm_cell_mdr_full_determinanthscm_negative_cell))) * mdr_nc_full_determinanth)) /\ exists ff_q_mdm_mdr_full_determinanthscm_negative_cell_source. mdr_nb_full_determinanth = ff_q_mdm_mdr_full_determinanthscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_full_determinanthscm_negative_cell) * (S (mdr_q_full_determinanths)) + (ff_column_mdm_cell_mdr_full_determinanthscm_negative_cell))) * mdr_nc_full_determinanth) + (ff_value_mdm_prefix_mdr_full_determinanthscm_negative)))))) /\ (((exists ff_h_mdm_mdr_full_determinanthscm_negative_target. ff_h_mdm_mdr_full_determinanthscm_negative_target + S (ff_value_mdm_prefix_mdr_full_determinanthscm_negative) = S ((S (ff_index_mdm_prefix_mdr_full_determinanthscm_negative)) * mdr_ut_full_determinanthsc)) /\ exists ff_q_mdm_mdr_full_determinanthscm_negative_target. mdr_un_full_determinanthsc = ff_q_mdm_mdr_full_determinanthscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_full_determinanthscm_negative)) * mdr_ut_full_determinanthsc) + (ff_value_mdm_prefix_mdr_full_determinanthscm_negative))))))))) /\ ((((exists ff_h_mdr_full_determinanthscp. ff_h_mdr_full_determinanthscp + S (mdr_p_full_determinanthsc) = S ((S (mdr_j_full_determinanthsc)) * mdr_ec_full_determinanths)) /\ exists ff_q_mdr_full_determinanthscp. mdr_eb_full_determinanths = ff_q_mdr_full_determinanthscp * S ((S (mdr_j_full_determinanthsc)) * mdr_ec_full_determinanths) + (mdr_p_full_determinanthsc))) /\ (((exists ff_h_mdr_full_determinanthscn. ff_h_mdr_full_determinanthscn + S (mdr_n_full_determinanthsc) = S ((S (mdr_j_full_determinanthsc)) * mdr_fc_full_determinanths)) /\ exists ff_q_mdr_full_determinanthscn. mdr_fb_full_determinanths = ff_q_mdr_full_determinanthscn * S ((S (mdr_j_full_determinanthsc)) * mdr_fc_full_determinanths) + (mdr_n_full_determinanthsc)))))))) /\ (exists ff_ub_mce_fold_mdr_full_determinanthsf ff_uc_mce_fold_mdr_full_determinanthsf ff_vb_mce_fold_mdr_full_determinanthsf ff_vc_mce_fold_mdr_full_determinanthsf. ((forall ff_index_mce_alternating_mdr_full_determinanthsf_prefix. (exists ff_gap_mce_mdr_full_determinanthsf_prefix_index. ff_gap_mce_mdr_full_determinanthsf_prefix_index + S (ff_index_mce_alternating_mdr_full_determinanthsf_prefix) = (S (mdr_q_full_determinanths))) -> exists ff_ap_mce_alternating_mdr_full_determinanthsf_prefix ff_an_mce_alternating_mdr_full_determinanthsf_prefix ff_bp_mce_alternating_mdr_full_determinanthsf_prefix ff_bn_mce_alternating_mdr_full_determinanthsf_prefix ff_p_mce_alternating_mdr_full_determinanthsf_prefix ff_n_mce_alternating_mdr_full_determinanthsf_prefix. ((((exists ff_h_mce_mdr_full_determinanthsf_prefix_ap. ff_h_mce_mdr_full_determinanthsf_prefix_ap + S (ff_ap_mce_alternating_mdr_full_determinanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_full_determinanthsf_prefix)) * mdr_pc_full_determinanth)) /\ exists ff_q_mce_mdr_full_determinanthsf_prefix_ap. mdr_pb_full_determinanth = ff_q_mce_mdr_full_determinanthsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_full_determinanthsf_prefix)) * mdr_pc_full_determinanth) + (ff_ap_mce_alternating_mdr_full_determinanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_full_determinanthsf_prefix_an. ff_h_mce_mdr_full_determinanthsf_prefix_an + S (ff_an_mce_alternating_mdr_full_determinanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_full_determinanthsf_prefix)) * mdr_nc_full_determinanth)) /\ exists ff_q_mce_mdr_full_determinanthsf_prefix_an. mdr_nb_full_determinanth = ff_q_mce_mdr_full_determinanthsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_full_determinanthsf_prefix)) * mdr_nc_full_determinanth) + (ff_an_mce_alternating_mdr_full_determinanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_full_determinanthsf_prefix_bp. ff_h_mce_mdr_full_determinanthsf_prefix_bp + S (ff_bp_mce_alternating_mdr_full_determinanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_full_determinanthsf_prefix)) * mdr_ec_full_determinanths)) /\ exists ff_q_mce_mdr_full_determinanthsf_prefix_bp. mdr_eb_full_determinanths = ff_q_mce_mdr_full_determinanthsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_full_determinanthsf_prefix)) * mdr_ec_full_determinanths) + (ff_bp_mce_alternating_mdr_full_determinanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_full_determinanthsf_prefix_bn. ff_h_mce_mdr_full_determinanthsf_prefix_bn + S (ff_bn_mce_alternating_mdr_full_determinanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_full_determinanthsf_prefix)) * mdr_fc_full_determinanths)) /\ exists ff_q_mce_mdr_full_determinanthsf_prefix_bn. mdr_fb_full_determinanths = ff_q_mce_mdr_full_determinanthsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_full_determinanthsf_prefix)) * mdr_fc_full_determinanths) + (ff_bn_mce_alternating_mdr_full_determinanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_full_determinanthsf_prefix_positive. ff_h_mce_mdr_full_determinanthsf_prefix_positive + S (ff_p_mce_alternating_mdr_full_determinanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_full_determinanthsf_prefix)) * ff_uc_mce_fold_mdr_full_determinanthsf)) /\ exists ff_q_mce_mdr_full_determinanthsf_prefix_positive. ff_ub_mce_fold_mdr_full_determinanthsf = ff_q_mce_mdr_full_determinanthsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_full_determinanthsf_prefix)) * ff_uc_mce_fold_mdr_full_determinanthsf) + (ff_p_mce_alternating_mdr_full_determinanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_full_determinanthsf_prefix_negative. ff_h_mce_mdr_full_determinanthsf_prefix_negative + S (ff_n_mce_alternating_mdr_full_determinanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_full_determinanthsf_prefix)) * ff_vc_mce_fold_mdr_full_determinanthsf)) /\ exists ff_q_mce_mdr_full_determinanthsf_prefix_negative. ff_vb_mce_fold_mdr_full_determinanthsf = ff_q_mce_mdr_full_determinanthsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_full_determinanthsf_prefix)) * ff_vc_mce_fold_mdr_full_determinanthsf) + (ff_n_mce_alternating_mdr_full_determinanthsf_prefix))) /\ (((exists ff_even_mce_term_mdr_full_determinanthsf_prefix_term. ff_index_mce_alternating_mdr_full_determinanthsf_prefix = 2 * ff_even_mce_term_mdr_full_determinanthsf_prefix_term) /\ (ff_p_mce_alternating_mdr_full_determinanthsf_prefix = (ff_ap_mce_alternating_mdr_full_determinanthsf_prefix) * (ff_bp_mce_alternating_mdr_full_determinanthsf_prefix) + (ff_an_mce_alternating_mdr_full_determinanthsf_prefix) * (ff_bn_mce_alternating_mdr_full_determinanthsf_prefix) /\ ff_n_mce_alternating_mdr_full_determinanthsf_prefix = (ff_ap_mce_alternating_mdr_full_determinanthsf_prefix) * (ff_bn_mce_alternating_mdr_full_determinanthsf_prefix) + (ff_an_mce_alternating_mdr_full_determinanthsf_prefix) * (ff_bp_mce_alternating_mdr_full_determinanthsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_full_determinanthsf_prefix_term. ff_index_mce_alternating_mdr_full_determinanthsf_prefix = 2 * ff_odd_mce_term_mdr_full_determinanthsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_full_determinanthsf_prefix = (ff_ap_mce_alternating_mdr_full_determinanthsf_prefix) * (ff_bn_mce_alternating_mdr_full_determinanthsf_prefix) + (ff_an_mce_alternating_mdr_full_determinanthsf_prefix) * (ff_bp_mce_alternating_mdr_full_determinanthsf_prefix) /\ ff_n_mce_alternating_mdr_full_determinanthsf_prefix = (ff_ap_mce_alternating_mdr_full_determinanthsf_prefix) * (ff_bp_mce_alternating_mdr_full_determinanthsf_prefix) + (ff_an_mce_alternating_mdr_full_determinanthsf_prefix) * (ff_bn_mce_alternating_mdr_full_determinanthsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_full_determinanthsf_positive ff_v_mce_mdr_full_determinanthsf_positive. ((((exists ff_h_mce_mdr_full_determinanthsf_positive_start. ff_h_mce_mdr_full_determinanthsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_full_determinanthsf_positive)) /\ exists ff_q_mce_mdr_full_determinanthsf_positive_start. ff_u_mce_mdr_full_determinanthsf_positive = ff_q_mce_mdr_full_determinanthsf_positive_start * S ((S (0)) * ff_v_mce_mdr_full_determinanthsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_full_determinanthsf_positive_terminal. ff_h_mce_mdr_full_determinanthsf_positive_terminal + S (mdr_p_full_determinanth) = S ((S ((S (mdr_q_full_determinanths)))) * ff_v_mce_mdr_full_determinanthsf_positive)) /\ exists ff_q_mce_mdr_full_determinanthsf_positive_terminal. ff_u_mce_mdr_full_determinanthsf_positive = ff_q_mce_mdr_full_determinanthsf_positive_terminal * S ((S ((S (mdr_q_full_determinanths)))) * ff_v_mce_mdr_full_determinanthsf_positive) + (mdr_p_full_determinanth))) /\ forall ff_i_mce_mdr_full_determinanthsf_positive. (exists ff_lt_mce_mdr_full_determinanthsf_positive_bound. ff_lt_mce_mdr_full_determinanthsf_positive_bound + S ff_i_mce_mdr_full_determinanthsf_positive = (S (mdr_q_full_determinanths))) -> exists ff_a_mce_mdr_full_determinanthsf_positive ff_r_mce_mdr_full_determinanthsf_positive ff_s_mce_mdr_full_determinanthsf_positive. ((((exists ff_h_mce_mdr_full_determinanthsf_positive_summand. ff_h_mce_mdr_full_determinanthsf_positive_summand + S (ff_a_mce_mdr_full_determinanthsf_positive) = S ((S (ff_i_mce_mdr_full_determinanthsf_positive)) * ff_uc_mce_fold_mdr_full_determinanthsf)) /\ exists ff_q_mce_mdr_full_determinanthsf_positive_summand. ff_ub_mce_fold_mdr_full_determinanthsf = ff_q_mce_mdr_full_determinanthsf_positive_summand * S ((S (ff_i_mce_mdr_full_determinanthsf_positive)) * ff_uc_mce_fold_mdr_full_determinanthsf) + (ff_a_mce_mdr_full_determinanthsf_positive))) /\ ((((exists ff_h_mce_mdr_full_determinanthsf_positive_partial. ff_h_mce_mdr_full_determinanthsf_positive_partial + S (ff_r_mce_mdr_full_determinanthsf_positive) = S ((S (ff_i_mce_mdr_full_determinanthsf_positive)) * ff_v_mce_mdr_full_determinanthsf_positive)) /\ exists ff_q_mce_mdr_full_determinanthsf_positive_partial. ff_u_mce_mdr_full_determinanthsf_positive = ff_q_mce_mdr_full_determinanthsf_positive_partial * S ((S (ff_i_mce_mdr_full_determinanthsf_positive)) * ff_v_mce_mdr_full_determinanthsf_positive) + (ff_r_mce_mdr_full_determinanthsf_positive))) /\ ((((exists ff_h_mce_mdr_full_determinanthsf_positive_successor. ff_h_mce_mdr_full_determinanthsf_positive_successor + S (ff_s_mce_mdr_full_determinanthsf_positive) = S ((S (S ff_i_mce_mdr_full_determinanthsf_positive)) * ff_v_mce_mdr_full_determinanthsf_positive)) /\ exists ff_q_mce_mdr_full_determinanthsf_positive_successor. ff_u_mce_mdr_full_determinanthsf_positive = ff_q_mce_mdr_full_determinanthsf_positive_successor * S ((S (S ff_i_mce_mdr_full_determinanthsf_positive)) * ff_v_mce_mdr_full_determinanthsf_positive) + (ff_s_mce_mdr_full_determinanthsf_positive))) /\ ff_s_mce_mdr_full_determinanthsf_positive = ff_r_mce_mdr_full_determinanthsf_positive + ff_a_mce_mdr_full_determinanthsf_positive)))))) /\ (exists ff_u_mce_mdr_full_determinanthsf_negative ff_v_mce_mdr_full_determinanthsf_negative. ((((exists ff_h_mce_mdr_full_determinanthsf_negative_start. ff_h_mce_mdr_full_determinanthsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_full_determinanthsf_negative)) /\ exists ff_q_mce_mdr_full_determinanthsf_negative_start. ff_u_mce_mdr_full_determinanthsf_negative = ff_q_mce_mdr_full_determinanthsf_negative_start * S ((S (0)) * ff_v_mce_mdr_full_determinanthsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_full_determinanthsf_negative_terminal. ff_h_mce_mdr_full_determinanthsf_negative_terminal + S (mdr_n_full_determinanth) = S ((S ((S (mdr_q_full_determinanths)))) * ff_v_mce_mdr_full_determinanthsf_negative)) /\ exists ff_q_mce_mdr_full_determinanthsf_negative_terminal. ff_u_mce_mdr_full_determinanthsf_negative = ff_q_mce_mdr_full_determinanthsf_negative_terminal * S ((S ((S (mdr_q_full_determinanths)))) * ff_v_mce_mdr_full_determinanthsf_negative) + (mdr_n_full_determinanth))) /\ forall ff_i_mce_mdr_full_determinanthsf_negative. (exists ff_lt_mce_mdr_full_determinanthsf_negative_bound. ff_lt_mce_mdr_full_determinanthsf_negative_bound + S ff_i_mce_mdr_full_determinanthsf_negative = (S (mdr_q_full_determinanths))) -> exists ff_a_mce_mdr_full_determinanthsf_negative ff_r_mce_mdr_full_determinanthsf_negative ff_s_mce_mdr_full_determinanthsf_negative. ((((exists ff_h_mce_mdr_full_determinanthsf_negative_summand. ff_h_mce_mdr_full_determinanthsf_negative_summand + S (ff_a_mce_mdr_full_determinanthsf_negative) = S ((S (ff_i_mce_mdr_full_determinanthsf_negative)) * ff_vc_mce_fold_mdr_full_determinanthsf)) /\ exists ff_q_mce_mdr_full_determinanthsf_negative_summand. ff_vb_mce_fold_mdr_full_determinanthsf = ff_q_mce_mdr_full_determinanthsf_negative_summand * S ((S (ff_i_mce_mdr_full_determinanthsf_negative)) * ff_vc_mce_fold_mdr_full_determinanthsf) + (ff_a_mce_mdr_full_determinanthsf_negative))) /\ ((((exists ff_h_mce_mdr_full_determinanthsf_negative_partial. ff_h_mce_mdr_full_determinanthsf_negative_partial + S (ff_r_mce_mdr_full_determinanthsf_negative) = S ((S (ff_i_mce_mdr_full_determinanthsf_negative)) * ff_v_mce_mdr_full_determinanthsf_negative)) /\ exists ff_q_mce_mdr_full_determinanthsf_negative_partial. ff_u_mce_mdr_full_determinanthsf_negative = ff_q_mce_mdr_full_determinanthsf_negative_partial * S ((S (ff_i_mce_mdr_full_determinanthsf_negative)) * ff_v_mce_mdr_full_determinanthsf_negative) + (ff_r_mce_mdr_full_determinanthsf_negative))) /\ ((((exists ff_h_mce_mdr_full_determinanthsf_negative_successor. ff_h_mce_mdr_full_determinanthsf_negative_successor + S (ff_s_mce_mdr_full_determinanthsf_negative) = S ((S (S ff_i_mce_mdr_full_determinanthsf_negative)) * ff_v_mce_mdr_full_determinanthsf_negative)) /\ exists ff_q_mce_mdr_full_determinanthsf_negative_successor. ff_u_mce_mdr_full_determinanthsf_negative = ff_q_mce_mdr_full_determinanthsf_negative_successor * S ((S (S ff_i_mce_mdr_full_determinanthsf_negative)) * ff_v_mce_mdr_full_determinanthsf_negative) + (ff_s_mce_mdr_full_determinanthsf_negative))) /\ ff_s_mce_mdr_full_determinanthsf_negative = ff_r_mce_mdr_full_determinanthsf_negative + ff_a_mce_mdr_full_determinanthsf_negative))))))))))))))) /\ ((exists mdr_gap_full_determinanti. mdr_gap_full_determinanti + S (mdr_i_full_determinant) = (mdr_l_full_determinant)) /\ (exists mdr_z_full_determinantr. ((exists mdr_a_full_determinantrc mdr_b_full_determinantrc mdr_c_full_determinantrc mdr_e_full_determinantrc mdr_f_full_determinantrc. ((mdr_a_full_determinantrc = ((d) + (ab)) * S ((d) + (ab)) + ((ab) + (ab))) /\ ((mdr_b_full_determinantrc = ((ac) + (bb)) * S ((ac) + (bb)) + ((bb) + (bb))) /\ ((mdr_c_full_determinantrc = ((mdr_a_full_determinantrc) + (mdr_b_full_determinantrc)) * S ((mdr_a_full_determinantrc) + (mdr_b_full_determinantrc)) + ((mdr_b_full_determinantrc) + (mdr_b_full_determinantrc))) /\ ((mdr_e_full_determinantrc = ((p) + (n)) * S ((p) + (n)) + ((n) + (n))) /\ ((mdr_f_full_determinantrc = ((bc) + (mdr_e_full_determinantrc)) * S ((bc) + (mdr_e_full_determinantrc)) + ((mdr_e_full_determinantrc) + (mdr_e_full_determinantrc))) /\ ((mdr_z_full_determinantr) = ((mdr_c_full_determinantrc) + (mdr_f_full_determinantrc)) * S ((mdr_c_full_determinantrc) + (mdr_f_full_determinantrc)) + ((mdr_f_full_determinantrc) + (mdr_f_full_determinantrc))))))))) /\ (((exists ff_h_mdr_full_determinantrb. ff_h_mdr_full_determinantrb + S (mdr_z_full_determinantr) = S ((S (mdr_i_full_determinant)) * mdr_c_full_determinant)) /\ exists ff_q_mdr_full_determinantrb. mdr_b_full_determinant = ff_q_mdr_full_determinantrb * S ((S (mdr_i_full_determinant)) * mdr_c_full_determinant) + (mdr_z_full_determinantr)))))))) -> ~(p = n) -> (exists mdr_rb_full_nonzero_minor mdr_rc_full_nonzero_minor mdr_cb_full_nonzero_minor mdr_cc_full_nonzero_minor. (((((forall fom_index_mrf_full_nonzero_minorminorrowsbound. (exists fom_gap_mrf_full_nonzero_minorminorrowsbound_index_bound. fom_gap_mrf_full_nonzero_minorminorrowsbound_index_bound + S (fom_index_mrf_full_nonzero_minorminorrowsbound) = d) -> exists fom_value_mrf_full_nonzero_minorminorrowsbound. ((((exists fom_beta_height_mrf_full_nonzero_minorminorrowsbound_entry. fom_beta_height_mrf_full_nonzero_minorminorrowsbound_entry + S (fom_value_mrf_full_nonzero_minorminorrowsbound) = S ((S (fom_index_mrf_full_nonzero_minorminorrowsbound)) * mdr_rc_full_nonzero_minor)) /\ exists fom_beta_quotient_mrf_full_nonzero_minorminorrowsbound_entry. mdr_rb_full_nonzero_minor = fom_beta_quotient_mrf_full_nonzero_minorminorrowsbound_entry * S ((S (fom_index_mrf_full_nonzero_minorminorrowsbound)) * mdr_rc_full_nonzero_minor) + (fom_value_mrf_full_nonzero_minorminorrowsbound))) /\ (exists fom_gap_mrf_full_nonzero_minorminorrowsbound_value_bound. fom_gap_mrf_full_nonzero_minorminorrowsbound_value_bound + S (fom_value_mrf_full_nonzero_minorminorrowsbound) = d))) /\ (forall mdr_i_full_nonzero_minorminorrowsdistinct mdr_j_full_nonzero_minorminorrowsdistinct mdr_a_full_nonzero_minorminorrowsdistinct. (exists mdr_gap_full_nonzero_minorminorrowsdistincti. mdr_gap_full_nonzero_minorminorrowsdistincti + S (mdr_i_full_nonzero_minorminorrowsdistinct) = (d)) -> (exists mdr_gap_full_nonzero_minorminorrowsdistinctj. mdr_gap_full_nonzero_minorminorrowsdistinctj + S (mdr_j_full_nonzero_minorminorrowsdistinct) = (d)) -> (((exists ff_h_mdr_full_nonzero_minorminorrowsdistinctfirst. ff_h_mdr_full_nonzero_minorminorrowsdistinctfirst + S (mdr_a_full_nonzero_minorminorrowsdistinct) = S ((S (mdr_i_full_nonzero_minorminorrowsdistinct)) * mdr_rc_full_nonzero_minor)) /\ exists ff_q_mdr_full_nonzero_minorminorrowsdistinctfirst. mdr_rb_full_nonzero_minor = ff_q_mdr_full_nonzero_minorminorrowsdistinctfirst * S ((S (mdr_i_full_nonzero_minorminorrowsdistinct)) * mdr_rc_full_nonzero_minor) + (mdr_a_full_nonzero_minorminorrowsdistinct))) -> (((exists ff_h_mdr_full_nonzero_minorminorrowsdistinctsecond. ff_h_mdr_full_nonzero_minorminorrowsdistinctsecond + S (mdr_a_full_nonzero_minorminorrowsdistinct) = S ((S (mdr_j_full_nonzero_minorminorrowsdistinct)) * mdr_rc_full_nonzero_minor)) /\ exists ff_q_mdr_full_nonzero_minorminorrowsdistinctsecond. mdr_rb_full_nonzero_minor = ff_q_mdr_full_nonzero_minorminorrowsdistinctsecond * S ((S (mdr_j_full_nonzero_minorminorrowsdistinct)) * mdr_rc_full_nonzero_minor) + (mdr_a_full_nonzero_minorminorrowsdistinct))) -> mdr_i_full_nonzero_minorminorrowsdistinct = mdr_j_full_nonzero_minorminorrowsdistinct))) /\ ((((forall fom_index_mrf_full_nonzero_minorminorcolumnsbound. (exists fom_gap_mrf_full_nonzero_minorminorcolumnsbound_index_bound. fom_gap_mrf_full_nonzero_minorminorcolumnsbound_index_bound + S (fom_index_mrf_full_nonzero_minorminorcolumnsbound) = d) -> exists fom_value_mrf_full_nonzero_minorminorcolumnsbound. ((((exists fom_beta_height_mrf_full_nonzero_minorminorcolumnsbound_entry. fom_beta_height_mrf_full_nonzero_minorminorcolumnsbound_entry + S (fom_value_mrf_full_nonzero_minorminorcolumnsbound) = S ((S (fom_index_mrf_full_nonzero_minorminorcolumnsbound)) * mdr_cc_full_nonzero_minor)) /\ exists fom_beta_quotient_mrf_full_nonzero_minorminorcolumnsbound_entry. mdr_cb_full_nonzero_minor = fom_beta_quotient_mrf_full_nonzero_minorminorcolumnsbound_entry * S ((S (fom_index_mrf_full_nonzero_minorminorcolumnsbound)) * mdr_cc_full_nonzero_minor) + (fom_value_mrf_full_nonzero_minorminorcolumnsbound))) /\ (exists fom_gap_mrf_full_nonzero_minorminorcolumnsbound_value_bound. fom_gap_mrf_full_nonzero_minorminorcolumnsbound_value_bound + S (fom_value_mrf_full_nonzero_minorminorcolumnsbound) = d))) /\ (forall mdr_i_full_nonzero_minorminorcolumnsdistinct mdr_j_full_nonzero_minorminorcolumnsdistinct mdr_a_full_nonzero_minorminorcolumnsdistinct. (exists mdr_gap_full_nonzero_minorminorcolumnsdistincti. mdr_gap_full_nonzero_minorminorcolumnsdistincti + S (mdr_i_full_nonzero_minorminorcolumnsdistinct) = (d)) -> (exists mdr_gap_full_nonzero_minorminorcolumnsdistinctj. mdr_gap_full_nonzero_minorminorcolumnsdistinctj + S (mdr_j_full_nonzero_minorminorcolumnsdistinct) = (d)) -> (((exists ff_h_mdr_full_nonzero_minorminorcolumnsdistinctfirst. ff_h_mdr_full_nonzero_minorminorcolumnsdistinctfirst + S (mdr_a_full_nonzero_minorminorcolumnsdistinct) = S ((S (mdr_i_full_nonzero_minorminorcolumnsdistinct)) * mdr_cc_full_nonzero_minor)) /\ exists ff_q_mdr_full_nonzero_minorminorcolumnsdistinctfirst. mdr_cb_full_nonzero_minor = ff_q_mdr_full_nonzero_minorminorcolumnsdistinctfirst * S ((S (mdr_i_full_nonzero_minorminorcolumnsdistinct)) * mdr_cc_full_nonzero_minor) + (mdr_a_full_nonzero_minorminorcolumnsdistinct))) -> (((exists ff_h_mdr_full_nonzero_minorminorcolumnsdistinctsecond. ff_h_mdr_full_nonzero_minorminorcolumnsdistinctsecond + S (mdr_a_full_nonzero_minorminorcolumnsdistinct) = S ((S (mdr_j_full_nonzero_minorminorcolumnsdistinct)) * mdr_cc_full_nonzero_minor)) /\ exists ff_q_mdr_full_nonzero_minorminorcolumnsdistinctsecond. mdr_cb_full_nonzero_minor = ff_q_mdr_full_nonzero_minorminorcolumnsdistinctsecond * S ((S (mdr_j_full_nonzero_minorminorcolumnsdistinct)) * mdr_cc_full_nonzero_minor) + (mdr_a_full_nonzero_minorminorcolumnsdistinct))) -> mdr_i_full_nonzero_minorminorcolumnsdistinct = mdr_j_full_nonzero_minorminorcolumnsdistinct))) /\ (exists mdr_p_full_nonzero_minorminornonzero mdr_n_full_nonzero_minorminornonzero. ((exists mdr_ub_full_nonzero_minorminornonzeroevaluation mdr_uc_full_nonzero_minorminornonzeroevaluation mdr_vb_full_nonzero_minorminornonzeroevaluation mdr_vc_full_nonzero_minorminornonzeroevaluation. ((((forall mdr_i_full_nonzero_minorminornonzeroevaluationmatrixpositive. (exists mdr_gap_full_nonzero_minorminornonzeroevaluationmatrixpositivebound. mdr_gap_full_nonzero_minorminornonzeroevaluationmatrixpositivebound + S (mdr_i_full_nonzero_minorminornonzeroevaluationmatrixpositive) = ((d) * (d))) -> exists mdr_a_full_nonzero_minorminornonzeroevaluationmatrixpositive. (((exists mdr_r_full_nonzero_minorminornonzeroevaluationmatrixpositivepoint mdr_s_full_nonzero_minorminornonzeroevaluationmatrixpositivepoint mdr_u_full_nonzero_minorminornonzeroevaluationmatrixpositivepoint mdr_v_full_nonzero_minorminornonzeroevaluationmatrixpositivepoint. ((mdr_i_full_nonzero_minorminornonzeroevaluationmatrixpositive = (d) * mdr_r_full_nonzero_minorminornonzeroevaluationmatrixpositivepoint + mdr_s_full_nonzero_minorminornonzeroevaluationmatrixpositivepoint) /\ ((exists mdr_gap_full_nonzero_minorminornonzeroevaluationmatrixpositivepointcolumn. mdr_gap_full_nonzero_minorminornonzeroevaluationmatrixpositivepointcolumn + S (mdr_s_full_nonzero_minorminornonzeroevaluationmatrixpositivepoint) = (d)) /\ ((((exists ff_h_mdr_full_nonzero_minorminornonzeroevaluationmatrixpositivepointrow_index. ff_h_mdr_full_nonzero_minorminornonzeroevaluationmatrixpositivepointrow_index + S (mdr_u_full_nonzero_minorminornonzeroevaluationmatrixpositivepoint) = S ((S (mdr_r_full_nonzero_minorminornonzeroevaluationmatrixpositivepoint)) * mdr_rc_full_nonzero_minor)) /\ exists ff_q_mdr_full_nonzero_minorminornonzeroevaluationmatrixpositivepointrow_index. mdr_rb_full_nonzero_minor = ff_q_mdr_full_nonzero_minorminornonzeroevaluationmatrixpositivepointrow_index * S ((S (mdr_r_full_nonzero_minorminornonzeroevaluationmatrixpositivepoint)) * mdr_rc_full_nonzero_minor) + (mdr_u_full_nonzero_minorminornonzeroevaluationmatrixpositivepoint))) /\ ((((exists ff_h_mdr_full_nonzero_minorminornonzeroevaluationmatrixpositivepointcolumn_index. ff_h_mdr_full_nonzero_minorminornonzeroevaluationmatrixpositivepointcolumn_index + S (mdr_v_full_nonzero_minorminornonzeroevaluationmatrixpositivepoint) = S ((S (mdr_s_full_nonzero_minorminornonzeroevaluationmatrixpositivepoint)) * mdr_cc_full_nonzero_minor)) /\ exists ff_q_mdr_full_nonzero_minorminornonzeroevaluationmatrixpositivepointcolumn_index. mdr_cb_full_nonzero_minor = ff_q_mdr_full_nonzero_minorminornonzeroevaluationmatrixpositivepointcolumn_index * S ((S (mdr_s_full_nonzero_minorminornonzeroevaluationmatrixpositivepoint)) * mdr_cc_full_nonzero_minor) + (mdr_v_full_nonzero_minorminornonzeroevaluationmatrixpositivepoint))) /\ (((exists ff_h_mdr_full_nonzero_minorminornonzeroevaluationmatrixpositivepointsource. ff_h_mdr_full_nonzero_minorminornonzeroevaluationmatrixpositivepointsource + S (mdr_a_full_nonzero_minorminornonzeroevaluationmatrixpositive) = S ((S ((mdr_u_full_nonzero_minorminornonzeroevaluationmatrixpositivepoint) * (d) + (mdr_v_full_nonzero_minorminornonzeroevaluationmatrixpositivepoint))) * ac)) /\ exists ff_q_mdr_full_nonzero_minorminornonzeroevaluationmatrixpositivepointsource. ab = ff_q_mdr_full_nonzero_minorminornonzeroevaluationmatrixpositivepointsource * S ((S ((mdr_u_full_nonzero_minorminornonzeroevaluationmatrixpositivepoint) * (d) + (mdr_v_full_nonzero_minorminornonzeroevaluationmatrixpositivepoint))) * ac) + (mdr_a_full_nonzero_minorminornonzeroevaluationmatrixpositive)))))))) /\ (((exists ff_h_mdr_full_nonzero_minorminornonzeroevaluationmatrixpositiveoutput. ff_h_mdr_full_nonzero_minorminornonzeroevaluationmatrixpositiveoutput + S (mdr_a_full_nonzero_minorminornonzeroevaluationmatrixpositive) = S ((S (mdr_i_full_nonzero_minorminornonzeroevaluationmatrixpositive)) * mdr_uc_full_nonzero_minorminornonzeroevaluation)) /\ exists ff_q_mdr_full_nonzero_minorminornonzeroevaluationmatrixpositiveoutput. mdr_ub_full_nonzero_minorminornonzeroevaluation = ff_q_mdr_full_nonzero_minorminornonzeroevaluationmatrixpositiveoutput * S ((S (mdr_i_full_nonzero_minorminornonzeroevaluationmatrixpositive)) * mdr_uc_full_nonzero_minorminornonzeroevaluation) + (mdr_a_full_nonzero_minorminornonzeroevaluationmatrixpositive)))))) /\ (forall mdr_i_full_nonzero_minorminornonzeroevaluationmatrixnegative. (exists mdr_gap_full_nonzero_minorminornonzeroevaluationmatrixnegativebound. mdr_gap_full_nonzero_minorminornonzeroevaluationmatrixnegativebound + S (mdr_i_full_nonzero_minorminornonzeroevaluationmatrixnegative) = ((d) * (d))) -> exists mdr_a_full_nonzero_minorminornonzeroevaluationmatrixnegative. (((exists mdr_r_full_nonzero_minorminornonzeroevaluationmatrixnegativepoint mdr_s_full_nonzero_minorminornonzeroevaluationmatrixnegativepoint mdr_u_full_nonzero_minorminornonzeroevaluationmatrixnegativepoint mdr_v_full_nonzero_minorminornonzeroevaluationmatrixnegativepoint. ((mdr_i_full_nonzero_minorminornonzeroevaluationmatrixnegative = (d) * mdr_r_full_nonzero_minorminornonzeroevaluationmatrixnegativepoint + mdr_s_full_nonzero_minorminornonzeroevaluationmatrixnegativepoint) /\ ((exists mdr_gap_full_nonzero_minorminornonzeroevaluationmatrixnegativepointcolumn. mdr_gap_full_nonzero_minorminornonzeroevaluationmatrixnegativepointcolumn + S (mdr_s_full_nonzero_minorminornonzeroevaluationmatrixnegativepoint) = (d)) /\ ((((exists ff_h_mdr_full_nonzero_minorminornonzeroevaluationmatrixnegativepointrow_index. ff_h_mdr_full_nonzero_minorminornonzeroevaluationmatrixnegativepointrow_index + S (mdr_u_full_nonzero_minorminornonzeroevaluationmatrixnegativepoint) = S ((S (mdr_r_full_nonzero_minorminornonzeroevaluationmatrixnegativepoint)) * mdr_rc_full_nonzero_minor)) /\ exists ff_q_mdr_full_nonzero_minorminornonzeroevaluationmatrixnegativepointrow_index. mdr_rb_full_nonzero_minor = ff_q_mdr_full_nonzero_minorminornonzeroevaluationmatrixnegativepointrow_index * S ((S (mdr_r_full_nonzero_minorminornonzeroevaluationmatrixnegativepoint)) * mdr_rc_full_nonzero_minor) + (mdr_u_full_nonzero_minorminornonzeroevaluationmatrixnegativepoint))) /\ ((((exists ff_h_mdr_full_nonzero_minorminornonzeroevaluationmatrixnegativepointcolumn_index. ff_h_mdr_full_nonzero_minorminornonzeroevaluationmatrixnegativepointcolumn_index + S (mdr_v_full_nonzero_minorminornonzeroevaluationmatrixnegativepoint) = S ((S (mdr_s_full_nonzero_minorminornonzeroevaluationmatrixnegativepoint)) * mdr_cc_full_nonzero_minor)) /\ exists ff_q_mdr_full_nonzero_minorminornonzeroevaluationmatrixnegativepointcolumn_index. mdr_cb_full_nonzero_minor = ff_q_mdr_full_nonzero_minorminornonzeroevaluationmatrixnegativepointcolumn_index * S ((S (mdr_s_full_nonzero_minorminornonzeroevaluationmatrixnegativepoint)) * mdr_cc_full_nonzero_minor) + (mdr_v_full_nonzero_minorminornonzeroevaluationmatrixnegativepoint))) /\ (((exists ff_h_mdr_full_nonzero_minorminornonzeroevaluationmatrixnegativepointsource. ff_h_mdr_full_nonzero_minorminornonzeroevaluationmatrixnegativepointsource + S (mdr_a_full_nonzero_minorminornonzeroevaluationmatrixnegative) = S ((S ((mdr_u_full_nonzero_minorminornonzeroevaluationmatrixnegativepoint) * (d) + (mdr_v_full_nonzero_minorminornonzeroevaluationmatrixnegativepoint))) * bc)) /\ exists ff_q_mdr_full_nonzero_minorminornonzeroevaluationmatrixnegativepointsource. bb = ff_q_mdr_full_nonzero_minorminornonzeroevaluationmatrixnegativepointsource * S ((S ((mdr_u_full_nonzero_minorminornonzeroevaluationmatrixnegativepoint) * (d) + (mdr_v_full_nonzero_minorminornonzeroevaluationmatrixnegativepoint))) * bc) + (mdr_a_full_nonzero_minorminornonzeroevaluationmatrixnegative)))))))) /\ (((exists ff_h_mdr_full_nonzero_minorminornonzeroevaluationmatrixnegativeoutput. ff_h_mdr_full_nonzero_minorminornonzeroevaluationmatrixnegativeoutput + S (mdr_a_full_nonzero_minorminornonzeroevaluationmatrixnegative) = S ((S (mdr_i_full_nonzero_minorminornonzeroevaluationmatrixnegative)) * mdr_vc_full_nonzero_minorminornonzeroevaluation)) /\ exists ff_q_mdr_full_nonzero_minorminornonzeroevaluationmatrixnegativeoutput. mdr_vb_full_nonzero_minorminornonzeroevaluation = ff_q_mdr_full_nonzero_minorminornonzeroevaluationmatrixnegativeoutput * S ((S (mdr_i_full_nonzero_minorminornonzeroevaluationmatrixnegative)) * mdr_vc_full_nonzero_minorminornonzeroevaluation) + (mdr_a_full_nonzero_minorminornonzeroevaluationmatrixnegative)))))))) /\ (exists mdr_b_full_nonzero_minorminornonzeroevaluationdeterminant mdr_c_full_nonzero_minorminornonzeroevaluationdeterminant mdr_l_full_nonzero_minorminornonzeroevaluationdeterminant mdr_i_full_nonzero_minorminornonzeroevaluationdeterminant. ((forall mdr_i_full_nonzero_minorminornonzeroevaluationdeterminanth. (exists mdr_gap_full_nonzero_minorminornonzeroevaluationdeterminanthi. mdr_gap_full_nonzero_minorminornonzeroevaluationdeterminanthi + S (mdr_i_full_nonzero_minorminornonzeroevaluationdeterminanth) = (mdr_l_full_nonzero_minorminornonzeroevaluationdeterminant)) -> exists mdr_d_full_nonzero_minorminornonzeroevaluationdeterminanth mdr_pb_full_nonzero_minorminornonzeroevaluationdeterminanth mdr_pc_full_nonzero_minorminornonzeroevaluationdeterminanth mdr_nb_full_nonzero_minorminornonzeroevaluationdeterminanth mdr_nc_full_nonzero_minorminornonzeroevaluationdeterminanth mdr_p_full_nonzero_minorminornonzeroevaluationdeterminanth mdr_n_full_nonzero_minorminornonzeroevaluationdeterminanth. ((exists mdr_z_full_nonzero_minorminornonzeroevaluationdeterminanthr. ((exists mdr_a_full_nonzero_minorminornonzeroevaluationdeterminanthrc mdr_b_full_nonzero_minorminornonzeroevaluationdeterminanthrc mdr_c_full_nonzero_minorminornonzeroevaluationdeterminanthrc mdr_e_full_nonzero_minorminornonzeroevaluationdeterminanthrc mdr_f_full_nonzero_minorminornonzeroevaluationdeterminanthrc. ((mdr_a_full_nonzero_minorminornonzeroevaluationdeterminanthrc = ((mdr_d_full_nonzero_minorminornonzeroevaluationdeterminanth) + (mdr_pb_full_nonzero_minorminornonzeroevaluationdeterminanth)) * S ((mdr_d_full_nonzero_minorminornonzeroevaluationdeterminanth) + (mdr_pb_full_nonzero_minorminornonzeroevaluationdeterminanth)) + ((mdr_pb_full_nonzero_minorminornonzeroevaluationdeterminanth) + (mdr_pb_full_nonzero_minorminornonzeroevaluationdeterminanth))) /\ ((mdr_b_full_nonzero_minorminornonzeroevaluationdeterminanthrc = ((mdr_pc_full_nonzero_minorminornonzeroevaluationdeterminanth) + (mdr_nb_full_nonzero_minorminornonzeroevaluationdeterminanth)) * S ((mdr_pc_full_nonzero_minorminornonzeroevaluationdeterminanth) + (mdr_nb_full_nonzero_minorminornonzeroevaluationdeterminanth)) + ((mdr_nb_full_nonzero_minorminornonzeroevaluationdeterminanth) + (mdr_nb_full_nonzero_minorminornonzeroevaluationdeterminanth))) /\ ((mdr_c_full_nonzero_minorminornonzeroevaluationdeterminanthrc = ((mdr_a_full_nonzero_minorminornonzeroevaluationdeterminanthrc) + (mdr_b_full_nonzero_minorminornonzeroevaluationdeterminanthrc)) * S ((mdr_a_full_nonzero_minorminornonzeroevaluationdeterminanthrc) + (mdr_b_full_nonzero_minorminornonzeroevaluationdeterminanthrc)) + ((mdr_b_full_nonzero_minorminornonzeroevaluationdeterminanthrc) + (mdr_b_full_nonzero_minorminornonzeroevaluationdeterminanthrc))) /\ ((mdr_e_full_nonzero_minorminornonzeroevaluationdeterminanthrc = ((mdr_p_full_nonzero_minorminornonzeroevaluationdeterminanth) + (mdr_n_full_nonzero_minorminornonzeroevaluationdeterminanth)) * S ((mdr_p_full_nonzero_minorminornonzeroevaluationdeterminanth) + (mdr_n_full_nonzero_minorminornonzeroevaluationdeterminanth)) + ((mdr_n_full_nonzero_minorminornonzeroevaluationdeterminanth) + (mdr_n_full_nonzero_minorminornonzeroevaluationdeterminanth))) /\ ((mdr_f_full_nonzero_minorminornonzeroevaluationdeterminanthrc = ((mdr_nc_full_nonzero_minorminornonzeroevaluationdeterminanth) + (mdr_e_full_nonzero_minorminornonzeroevaluationdeterminanthrc)) * S ((mdr_nc_full_nonzero_minorminornonzeroevaluationdeterminanth) + (mdr_e_full_nonzero_minorminornonzeroevaluationdeterminanthrc)) + ((mdr_e_full_nonzero_minorminornonzeroevaluationdeterminanthrc) + (mdr_e_full_nonzero_minorminornonzeroevaluationdeterminanthrc))) /\ ((mdr_z_full_nonzero_minorminornonzeroevaluationdeterminanthr) = ((mdr_c_full_nonzero_minorminornonzeroevaluationdeterminanthrc) + (mdr_f_full_nonzero_minorminornonzeroevaluationdeterminanthrc)) * S ((mdr_c_full_nonzero_minorminornonzeroevaluationdeterminanthrc) + (mdr_f_full_nonzero_minorminornonzeroevaluationdeterminanthrc)) + ((mdr_f_full_nonzero_minorminornonzeroevaluationdeterminanthrc) + (mdr_f_full_nonzero_minorminornonzeroevaluationdeterminanthrc))))))))) /\ (((exists ff_h_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthrb. ff_h_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthrb + S (mdr_z_full_nonzero_minorminornonzeroevaluationdeterminanthr) = S ((S (mdr_i_full_nonzero_minorminornonzeroevaluationdeterminanth)) * mdr_c_full_nonzero_minorminornonzeroevaluationdeterminant)) /\ exists ff_q_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthrb. mdr_b_full_nonzero_minorminornonzeroevaluationdeterminant = ff_q_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthrb * S ((S (mdr_i_full_nonzero_minorminornonzeroevaluationdeterminanth)) * mdr_c_full_nonzero_minorminornonzeroevaluationdeterminant) + (mdr_z_full_nonzero_minorminornonzeroevaluationdeterminanthr))))) /\ (((((mdr_d_full_nonzero_minorminornonzeroevaluationdeterminanth) = 0) /\ (((mdr_p_full_nonzero_minorminornonzeroevaluationdeterminanth) = 1) /\ ((mdr_n_full_nonzero_minorminornonzeroevaluationdeterminanth) = 0))) \/ exists mdr_q_full_nonzero_minorminornonzeroevaluationdeterminanths mdr_eb_full_nonzero_minorminornonzeroevaluationdeterminanths mdr_ec_full_nonzero_minorminornonzeroevaluationdeterminanths mdr_fb_full_nonzero_minorminornonzeroevaluationdeterminanths mdr_fc_full_nonzero_minorminornonzeroevaluationdeterminanths. (((mdr_d_full_nonzero_minorminornonzeroevaluationdeterminanth) = S (mdr_q_full_nonzero_minorminornonzeroevaluationdeterminanths)) /\ ((forall mdr_j_full_nonzero_minorminornonzeroevaluationdeterminanthsc. (exists mdr_gap_full_nonzero_minorminornonzeroevaluationdeterminanthscj. mdr_gap_full_nonzero_minorminornonzeroevaluationdeterminanthscj + S (mdr_j_full_nonzero_minorminornonzeroevaluationdeterminanthsc) = (S (mdr_q_full_nonzero_minorminornonzeroevaluationdeterminanths))) -> exists mdr_i_full_nonzero_minorminornonzeroevaluationdeterminanthsc mdr_up_full_nonzero_minorminornonzeroevaluationdeterminanthsc mdr_us_full_nonzero_minorminornonzeroevaluationdeterminanthsc mdr_un_full_nonzero_minorminornonzeroevaluationdeterminanthsc mdr_ut_full_nonzero_minorminornonzeroevaluationdeterminanthsc mdr_p_full_nonzero_minorminornonzeroevaluationdeterminanthsc mdr_n_full_nonzero_minorminornonzeroevaluationdeterminanthsc. ((exists mdr_gap_full_nonzero_minorminornonzeroevaluationdeterminanthsci. mdr_gap_full_nonzero_minorminornonzeroevaluationdeterminanthsci + S (mdr_i_full_nonzero_minorminornonzeroevaluationdeterminanthsc) = (mdr_i_full_nonzero_minorminornonzeroevaluationdeterminanth)) /\ ((exists mdr_z_full_nonzero_minorminornonzeroevaluationdeterminanthscr. ((exists mdr_a_full_nonzero_minorminornonzeroevaluationdeterminanthscrc mdr_b_full_nonzero_minorminornonzeroevaluationdeterminanthscrc mdr_c_full_nonzero_minorminornonzeroevaluationdeterminanthscrc mdr_e_full_nonzero_minorminornonzeroevaluationdeterminanthscrc mdr_f_full_nonzero_minorminornonzeroevaluationdeterminanthscrc. ((mdr_a_full_nonzero_minorminornonzeroevaluationdeterminanthscrc = ((mdr_q_full_nonzero_minorminornonzeroevaluationdeterminanths) + (mdr_up_full_nonzero_minorminornonzeroevaluationdeterminanthsc)) * S ((mdr_q_full_nonzero_minorminornonzeroevaluationdeterminanths) + (mdr_up_full_nonzero_minorminornonzeroevaluationdeterminanthsc)) + ((mdr_up_full_nonzero_minorminornonzeroevaluationdeterminanthsc) + (mdr_up_full_nonzero_minorminornonzeroevaluationdeterminanthsc))) /\ ((mdr_b_full_nonzero_minorminornonzeroevaluationdeterminanthscrc = ((mdr_us_full_nonzero_minorminornonzeroevaluationdeterminanthsc) + (mdr_un_full_nonzero_minorminornonzeroevaluationdeterminanthsc)) * S ((mdr_us_full_nonzero_minorminornonzeroevaluationdeterminanthsc) + (mdr_un_full_nonzero_minorminornonzeroevaluationdeterminanthsc)) + ((mdr_un_full_nonzero_minorminornonzeroevaluationdeterminanthsc) + (mdr_un_full_nonzero_minorminornonzeroevaluationdeterminanthsc))) /\ ((mdr_c_full_nonzero_minorminornonzeroevaluationdeterminanthscrc = ((mdr_a_full_nonzero_minorminornonzeroevaluationdeterminanthscrc) + (mdr_b_full_nonzero_minorminornonzeroevaluationdeterminanthscrc)) * S ((mdr_a_full_nonzero_minorminornonzeroevaluationdeterminanthscrc) + (mdr_b_full_nonzero_minorminornonzeroevaluationdeterminanthscrc)) + ((mdr_b_full_nonzero_minorminornonzeroevaluationdeterminanthscrc) + (mdr_b_full_nonzero_minorminornonzeroevaluationdeterminanthscrc))) /\ ((mdr_e_full_nonzero_minorminornonzeroevaluationdeterminanthscrc = ((mdr_p_full_nonzero_minorminornonzeroevaluationdeterminanthsc) + (mdr_n_full_nonzero_minorminornonzeroevaluationdeterminanthsc)) * S ((mdr_p_full_nonzero_minorminornonzeroevaluationdeterminanthsc) + (mdr_n_full_nonzero_minorminornonzeroevaluationdeterminanthsc)) + ((mdr_n_full_nonzero_minorminornonzeroevaluationdeterminanthsc) + (mdr_n_full_nonzero_minorminornonzeroevaluationdeterminanthsc))) /\ ((mdr_f_full_nonzero_minorminornonzeroevaluationdeterminanthscrc = ((mdr_ut_full_nonzero_minorminornonzeroevaluationdeterminanthsc) + (mdr_e_full_nonzero_minorminornonzeroevaluationdeterminanthscrc)) * S ((mdr_ut_full_nonzero_minorminornonzeroevaluationdeterminanthsc) + (mdr_e_full_nonzero_minorminornonzeroevaluationdeterminanthscrc)) + ((mdr_e_full_nonzero_minorminornonzeroevaluationdeterminanthscrc) + (mdr_e_full_nonzero_minorminornonzeroevaluationdeterminanthscrc))) /\ ((mdr_z_full_nonzero_minorminornonzeroevaluationdeterminanthscr) = ((mdr_c_full_nonzero_minorminornonzeroevaluationdeterminanthscrc) + (mdr_f_full_nonzero_minorminornonzeroevaluationdeterminanthscrc)) * S ((mdr_c_full_nonzero_minorminornonzeroevaluationdeterminanthscrc) + (mdr_f_full_nonzero_minorminornonzeroevaluationdeterminanthscrc)) + ((mdr_f_full_nonzero_minorminornonzeroevaluationdeterminanthscrc) + (mdr_f_full_nonzero_minorminornonzeroevaluationdeterminanthscrc))))))))) /\ (((exists ff_h_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthscrb. ff_h_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthscrb + S (mdr_z_full_nonzero_minorminornonzeroevaluationdeterminanthscr) = S ((S (mdr_i_full_nonzero_minorminornonzeroevaluationdeterminanthsc)) * mdr_c_full_nonzero_minorminornonzeroevaluationdeterminant)) /\ exists ff_q_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthscrb. mdr_b_full_nonzero_minorminornonzeroevaluationdeterminant = ff_q_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthscrb * S ((S (mdr_i_full_nonzero_minorminornonzeroevaluationdeterminanthsc)) * mdr_c_full_nonzero_minorminornonzeroevaluationdeterminant) + (mdr_z_full_nonzero_minorminornonzeroevaluationdeterminanthscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthscm_positive. (exists ff_gap_mdm_lt_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthscm_positive_index_bound. ff_gap_mdm_lt_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthscm_positive) = ((mdr_q_full_nonzero_minorminornonzeroevaluationdeterminanths) * (mdr_q_full_nonzero_minorminornonzeroevaluationdeterminanths))) -> exists ff_row_mdm_prefix_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthscm_positive ff_column_mdm_prefix_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthscm_positive ff_value_mdm_prefix_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthscm_positive. (ff_index_mdm_prefix_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthscm_positive = (mdr_q_full_nonzero_minorminornonzeroevaluationdeterminanths) * ff_row_mdm_prefix_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthscm_positive + ff_column_mdm_prefix_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthscm_positive /\ ((exists ff_gap_mdm_lt_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthscm_positive_column_bound. ff_gap_mdm_lt_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthscm_positive) = (mdr_q_full_nonzero_minorminornonzeroevaluationdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthscm_positive_cell ff_column_mdm_cell_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthscm_positive_cell = ff_row_mdm_prefix_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthscm_positive_cell_row_after. ff_gap_mdm_le_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthscm_positive)) /\ ff_row_mdm_cell_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthscm_positive_cell = S ff_row_mdm_prefix_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthscm_positive) = (mdr_j_full_nonzero_minorminornonzeroevaluationdeterminanthsc)) /\ ff_column_mdm_cell_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthscm_positive_cell = ff_column_mdm_prefix_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthscm_positive_cell_column_after. ff_gap_mdm_le_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthscm_positive_cell_column_after + (mdr_j_full_nonzero_minorminornonzeroevaluationdeterminanthsc) = (ff_column_mdm_prefix_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthscm_positive)) /\ ff_column_mdm_cell_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthscm_positive_cell = S ff_column_mdm_prefix_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthscm_positive))) /\ (((exists ff_h_mdm_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthscm_positive_cell_source. ff_h_mdm_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthscm_positive) = S ((S ((ff_row_mdm_cell_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthscm_positive_cell) * (S (mdr_q_full_nonzero_minorminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthscm_positive_cell))) * mdr_pc_full_nonzero_minorminornonzeroevaluationdeterminanth)) /\ exists ff_q_mdm_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthscm_positive_cell_source. mdr_pb_full_nonzero_minorminornonzeroevaluationdeterminanth = ff_q_mdm_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthscm_positive_cell) * (S (mdr_q_full_nonzero_minorminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthscm_positive_cell))) * mdr_pc_full_nonzero_minorminornonzeroevaluationdeterminanth) + (ff_value_mdm_prefix_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthscm_positive)))))) /\ (((exists ff_h_mdm_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthscm_positive_target. ff_h_mdm_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthscm_positive_target + S (ff_value_mdm_prefix_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthscm_positive) = S ((S (ff_index_mdm_prefix_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthscm_positive)) * mdr_us_full_nonzero_minorminornonzeroevaluationdeterminanthsc)) /\ exists ff_q_mdm_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthscm_positive_target. mdr_up_full_nonzero_minorminornonzeroevaluationdeterminanthsc = ff_q_mdm_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthscm_positive)) * mdr_us_full_nonzero_minorminornonzeroevaluationdeterminanthsc) + (ff_value_mdm_prefix_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthscm_negative. (exists ff_gap_mdm_lt_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthscm_negative_index_bound. ff_gap_mdm_lt_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthscm_negative) = ((mdr_q_full_nonzero_minorminornonzeroevaluationdeterminanths) * (mdr_q_full_nonzero_minorminornonzeroevaluationdeterminanths))) -> exists ff_row_mdm_prefix_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthscm_negative ff_column_mdm_prefix_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthscm_negative ff_value_mdm_prefix_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthscm_negative. (ff_index_mdm_prefix_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthscm_negative = (mdr_q_full_nonzero_minorminornonzeroevaluationdeterminanths) * ff_row_mdm_prefix_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthscm_negative + ff_column_mdm_prefix_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthscm_negative /\ ((exists ff_gap_mdm_lt_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthscm_negative_column_bound. ff_gap_mdm_lt_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthscm_negative) = (mdr_q_full_nonzero_minorminornonzeroevaluationdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthscm_negative_cell ff_column_mdm_cell_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthscm_negative_cell = ff_row_mdm_prefix_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthscm_negative_cell_row_after. ff_gap_mdm_le_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthscm_negative)) /\ ff_row_mdm_cell_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthscm_negative_cell = S ff_row_mdm_prefix_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthscm_negative) = (mdr_j_full_nonzero_minorminornonzeroevaluationdeterminanthsc)) /\ ff_column_mdm_cell_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthscm_negative_cell = ff_column_mdm_prefix_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthscm_negative_cell_column_after. ff_gap_mdm_le_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthscm_negative_cell_column_after + (mdr_j_full_nonzero_minorminornonzeroevaluationdeterminanthsc) = (ff_column_mdm_prefix_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthscm_negative)) /\ ff_column_mdm_cell_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthscm_negative_cell = S ff_column_mdm_prefix_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthscm_negative))) /\ (((exists ff_h_mdm_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthscm_negative_cell_source. ff_h_mdm_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthscm_negative) = S ((S ((ff_row_mdm_cell_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthscm_negative_cell) * (S (mdr_q_full_nonzero_minorminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthscm_negative_cell))) * mdr_nc_full_nonzero_minorminornonzeroevaluationdeterminanth)) /\ exists ff_q_mdm_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthscm_negative_cell_source. mdr_nb_full_nonzero_minorminornonzeroevaluationdeterminanth = ff_q_mdm_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthscm_negative_cell) * (S (mdr_q_full_nonzero_minorminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthscm_negative_cell))) * mdr_nc_full_nonzero_minorminornonzeroevaluationdeterminanth) + (ff_value_mdm_prefix_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthscm_negative)))))) /\ (((exists ff_h_mdm_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthscm_negative_target. ff_h_mdm_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthscm_negative_target + S (ff_value_mdm_prefix_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthscm_negative) = S ((S (ff_index_mdm_prefix_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthscm_negative)) * mdr_ut_full_nonzero_minorminornonzeroevaluationdeterminanthsc)) /\ exists ff_q_mdm_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthscm_negative_target. mdr_un_full_nonzero_minorminornonzeroevaluationdeterminanthsc = ff_q_mdm_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthscm_negative)) * mdr_ut_full_nonzero_minorminornonzeroevaluationdeterminanthsc) + (ff_value_mdm_prefix_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthscm_negative))))))))) /\ ((((exists ff_h_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthscp. ff_h_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthscp + S (mdr_p_full_nonzero_minorminornonzeroevaluationdeterminanthsc) = S ((S (mdr_j_full_nonzero_minorminornonzeroevaluationdeterminanthsc)) * mdr_ec_full_nonzero_minorminornonzeroevaluationdeterminanths)) /\ exists ff_q_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthscp. mdr_eb_full_nonzero_minorminornonzeroevaluationdeterminanths = ff_q_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthscp * S ((S (mdr_j_full_nonzero_minorminornonzeroevaluationdeterminanthsc)) * mdr_ec_full_nonzero_minorminornonzeroevaluationdeterminanths) + (mdr_p_full_nonzero_minorminornonzeroevaluationdeterminanthsc))) /\ (((exists ff_h_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthscn. ff_h_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthscn + S (mdr_n_full_nonzero_minorminornonzeroevaluationdeterminanthsc) = S ((S (mdr_j_full_nonzero_minorminornonzeroevaluationdeterminanthsc)) * mdr_fc_full_nonzero_minorminornonzeroevaluationdeterminanths)) /\ exists ff_q_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthscn. mdr_fb_full_nonzero_minorminornonzeroevaluationdeterminanths = ff_q_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthscn * S ((S (mdr_j_full_nonzero_minorminornonzeroevaluationdeterminanthsc)) * mdr_fc_full_nonzero_minorminornonzeroevaluationdeterminanths) + (mdr_n_full_nonzero_minorminornonzeroevaluationdeterminanthsc)))))))) /\ (exists ff_ub_mce_fold_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf ff_uc_mce_fold_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf ff_vb_mce_fold_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf ff_vc_mce_fold_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf. ((forall ff_index_mce_alternating_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix. (exists ff_gap_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix_index. ff_gap_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix_index + S (ff_index_mce_alternating_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix) = (S (mdr_q_full_nonzero_minorminornonzeroevaluationdeterminanths))) -> exists ff_ap_mce_alternating_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix ff_an_mce_alternating_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix ff_bp_mce_alternating_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix ff_bn_mce_alternating_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix ff_p_mce_alternating_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix ff_n_mce_alternating_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix. ((((exists ff_h_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix_ap. ff_h_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix_ap + S (ff_ap_mce_alternating_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix)) * mdr_pc_full_nonzero_minorminornonzeroevaluationdeterminanth)) /\ exists ff_q_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix_ap. mdr_pb_full_nonzero_minorminornonzeroevaluationdeterminanth = ff_q_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix)) * mdr_pc_full_nonzero_minorminornonzeroevaluationdeterminanth) + (ff_ap_mce_alternating_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix_an. ff_h_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix_an + S (ff_an_mce_alternating_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix)) * mdr_nc_full_nonzero_minorminornonzeroevaluationdeterminanth)) /\ exists ff_q_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix_an. mdr_nb_full_nonzero_minorminornonzeroevaluationdeterminanth = ff_q_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix)) * mdr_nc_full_nonzero_minorminornonzeroevaluationdeterminanth) + (ff_an_mce_alternating_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix_bp. ff_h_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix_bp + S (ff_bp_mce_alternating_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix)) * mdr_ec_full_nonzero_minorminornonzeroevaluationdeterminanths)) /\ exists ff_q_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix_bp. mdr_eb_full_nonzero_minorminornonzeroevaluationdeterminanths = ff_q_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix)) * mdr_ec_full_nonzero_minorminornonzeroevaluationdeterminanths) + (ff_bp_mce_alternating_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix_bn. ff_h_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix_bn + S (ff_bn_mce_alternating_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix)) * mdr_fc_full_nonzero_minorminornonzeroevaluationdeterminanths)) /\ exists ff_q_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix_bn. mdr_fb_full_nonzero_minorminornonzeroevaluationdeterminanths = ff_q_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix)) * mdr_fc_full_nonzero_minorminornonzeroevaluationdeterminanths) + (ff_bn_mce_alternating_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix_positive. ff_h_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix_positive + S (ff_p_mce_alternating_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix_positive. ff_ub_mce_fold_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf) + (ff_p_mce_alternating_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix_negative. ff_h_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix_negative + S (ff_n_mce_alternating_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix_negative. ff_vb_mce_fold_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf) + (ff_n_mce_alternating_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix))) /\ (((exists ff_even_mce_term_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix = 2 * ff_even_mce_term_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix_term) /\ (ff_p_mce_alternating_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix = 2 * ff_odd_mce_term_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_positive ff_v_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_positive. ((((exists ff_h_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_positive_start. ff_h_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_positive_start. ff_u_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_positive_start * S ((S (0)) * ff_v_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_positive_terminal. ff_h_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_positive_terminal + S (mdr_p_full_nonzero_minorminornonzeroevaluationdeterminanth) = S ((S ((S (mdr_q_full_nonzero_minorminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_positive_terminal. ff_u_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_positive_terminal * S ((S ((S (mdr_q_full_nonzero_minorminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_positive) + (mdr_p_full_nonzero_minorminornonzeroevaluationdeterminanth))) /\ forall ff_i_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_positive. (exists ff_lt_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_positive_bound. ff_lt_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_positive_bound + S ff_i_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_positive = (S (mdr_q_full_nonzero_minorminornonzeroevaluationdeterminanths))) -> exists ff_a_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_positive ff_r_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_positive ff_s_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_positive. ((((exists ff_h_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_positive_summand. ff_h_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_positive_summand + S (ff_a_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_positive_summand. ff_ub_mce_fold_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_positive_summand * S ((S (ff_i_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf) + (ff_a_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_positive_partial. ff_h_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_positive_partial + S (ff_r_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_positive_partial. ff_u_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_positive_partial * S ((S (ff_i_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_positive) + (ff_r_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_positive_successor. ff_h_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_positive_successor + S (ff_s_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_positive) = S ((S (S ff_i_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_positive_successor. ff_u_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_positive_successor * S ((S (S ff_i_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_positive) + (ff_s_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_positive))) /\ ff_s_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_positive = ff_r_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_positive + ff_a_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_positive)))))) /\ (exists ff_u_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_negative ff_v_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_negative. ((((exists ff_h_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_negative_start. ff_h_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_negative_start. ff_u_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_negative_start * S ((S (0)) * ff_v_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_negative_terminal. ff_h_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_negative_terminal + S (mdr_n_full_nonzero_minorminornonzeroevaluationdeterminanth) = S ((S ((S (mdr_q_full_nonzero_minorminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_negative_terminal. ff_u_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_negative_terminal * S ((S ((S (mdr_q_full_nonzero_minorminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_negative) + (mdr_n_full_nonzero_minorminornonzeroevaluationdeterminanth))) /\ forall ff_i_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_negative. (exists ff_lt_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_negative_bound. ff_lt_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_negative_bound + S ff_i_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_negative = (S (mdr_q_full_nonzero_minorminornonzeroevaluationdeterminanths))) -> exists ff_a_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_negative ff_r_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_negative ff_s_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_negative. ((((exists ff_h_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_negative_summand. ff_h_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_negative_summand + S (ff_a_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_negative_summand. ff_vb_mce_fold_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_negative_summand * S ((S (ff_i_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf) + (ff_a_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_negative_partial. ff_h_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_negative_partial + S (ff_r_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_negative_partial. ff_u_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_negative_partial * S ((S (ff_i_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_negative) + (ff_r_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_negative_successor. ff_h_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_negative_successor + S (ff_s_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_negative) = S ((S (S ff_i_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_negative_successor. ff_u_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_negative_successor * S ((S (S ff_i_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_negative) + (ff_s_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_negative))) /\ ff_s_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_negative = ff_r_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_negative + ff_a_mce_mdr_full_nonzero_minorminornonzeroevaluationdeterminanthsf_negative))))))))))))))) /\ ((exists mdr_gap_full_nonzero_minorminornonzeroevaluationdeterminanti. mdr_gap_full_nonzero_minorminornonzeroevaluationdeterminanti + S (mdr_i_full_nonzero_minorminornonzeroevaluationdeterminant) = (mdr_l_full_nonzero_minorminornonzeroevaluationdeterminant)) /\ (exists mdr_z_full_nonzero_minorminornonzeroevaluationdeterminantr. ((exists mdr_a_full_nonzero_minorminornonzeroevaluationdeterminantrc mdr_b_full_nonzero_minorminornonzeroevaluationdeterminantrc mdr_c_full_nonzero_minorminornonzeroevaluationdeterminantrc mdr_e_full_nonzero_minorminornonzeroevaluationdeterminantrc mdr_f_full_nonzero_minorminornonzeroevaluationdeterminantrc. ((mdr_a_full_nonzero_minorminornonzeroevaluationdeterminantrc = ((d) + (mdr_ub_full_nonzero_minorminornonzeroevaluation)) * S ((d) + (mdr_ub_full_nonzero_minorminornonzeroevaluation)) + ((mdr_ub_full_nonzero_minorminornonzeroevaluation) + (mdr_ub_full_nonzero_minorminornonzeroevaluation))) /\ ((mdr_b_full_nonzero_minorminornonzeroevaluationdeterminantrc = ((mdr_uc_full_nonzero_minorminornonzeroevaluation) + (mdr_vb_full_nonzero_minorminornonzeroevaluation)) * S ((mdr_uc_full_nonzero_minorminornonzeroevaluation) + (mdr_vb_full_nonzero_minorminornonzeroevaluation)) + ((mdr_vb_full_nonzero_minorminornonzeroevaluation) + (mdr_vb_full_nonzero_minorminornonzeroevaluation))) /\ ((mdr_c_full_nonzero_minorminornonzeroevaluationdeterminantrc = ((mdr_a_full_nonzero_minorminornonzeroevaluationdeterminantrc) + (mdr_b_full_nonzero_minorminornonzeroevaluationdeterminantrc)) * S ((mdr_a_full_nonzero_minorminornonzeroevaluationdeterminantrc) + (mdr_b_full_nonzero_minorminornonzeroevaluationdeterminantrc)) + ((mdr_b_full_nonzero_minorminornonzeroevaluationdeterminantrc) + (mdr_b_full_nonzero_minorminornonzeroevaluationdeterminantrc))) /\ ((mdr_e_full_nonzero_minorminornonzeroevaluationdeterminantrc = ((mdr_p_full_nonzero_minorminornonzero) + (mdr_n_full_nonzero_minorminornonzero)) * S ((mdr_p_full_nonzero_minorminornonzero) + (mdr_n_full_nonzero_minorminornonzero)) + ((mdr_n_full_nonzero_minorminornonzero) + (mdr_n_full_nonzero_minorminornonzero))) /\ ((mdr_f_full_nonzero_minorminornonzeroevaluationdeterminantrc = ((mdr_vc_full_nonzero_minorminornonzeroevaluation) + (mdr_e_full_nonzero_minorminornonzeroevaluationdeterminantrc)) * S ((mdr_vc_full_nonzero_minorminornonzeroevaluation) + (mdr_e_full_nonzero_minorminornonzeroevaluationdeterminantrc)) + ((mdr_e_full_nonzero_minorminornonzeroevaluationdeterminantrc) + (mdr_e_full_nonzero_minorminornonzeroevaluationdeterminantrc))) /\ ((mdr_z_full_nonzero_minorminornonzeroevaluationdeterminantr) = ((mdr_c_full_nonzero_minorminornonzeroevaluationdeterminantrc) + (mdr_f_full_nonzero_minorminornonzeroevaluationdeterminantrc)) * S ((mdr_c_full_nonzero_minorminornonzeroevaluationdeterminantrc) + (mdr_f_full_nonzero_minorminornonzeroevaluationdeterminantrc)) + ((mdr_f_full_nonzero_minorminornonzeroevaluationdeterminantrc) + (mdr_f_full_nonzero_minorminornonzeroevaluationdeterminantrc))))))))) /\ (((exists ff_h_mdr_full_nonzero_minorminornonzeroevaluationdeterminantrb. ff_h_mdr_full_nonzero_minorminornonzeroevaluationdeterminantrb + S (mdr_z_full_nonzero_minorminornonzeroevaluationdeterminantr) = S ((S (mdr_i_full_nonzero_minorminornonzeroevaluationdeterminant)) * mdr_c_full_nonzero_minorminornonzeroevaluationdeterminant)) /\ exists ff_q_mdr_full_nonzero_minorminornonzeroevaluationdeterminantrb. mdr_b_full_nonzero_minorminornonzeroevaluationdeterminant = ff_q_mdr_full_nonzero_minorminornonzeroevaluationdeterminantrb * S ((S (mdr_i_full_nonzero_minorminornonzeroevaluationdeterminant)) * mdr_c_full_nonzero_minorminornonzeroevaluationdeterminant) + (mdr_z_full_nonzero_minorminornonzeroevaluationdeterminantr)))))))))) /\ (~(mdr_p_full_nonzero_minorminornonzero = mdr_n_full_nonzero_minorminornonzero))))))))Complete tactic proof in conservative notation
All 82 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
82 script commands · 20 reading checkpoints · 1 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–9
02Use earlier factsL10–11
03Separate the logical casesL12–12
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L12
cases eq_decidable
04Calculate and transport equalitiesL13–22
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
05Calculate and transport equalitiesL23–32
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
06Calculate and transport equalitiesL33–34
07Use earlier factsL35–41
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L35
specialize matrix_rank_nonzero_minor_empty (ab) - L36
specialize matrix_rank_nonzero_minor_empty (ac) - L37
specialize matrix_rank_nonzero_minor_empty (bb) - L38
specialize matrix_rank_nonzero_minor_empty (bc) - L39
specialize matrix_rank_nonzero_minor_empty (0) - L40
specialize matrix_rank_nonzero_minor_empty (0) - L41
apply matrix_rank_nonzero_minor_empty
08Establish hidentityL42–44
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply matrix lattice identity selector exists.
- L42
have hidentity : ∃ b. ∃ c. IdentityMatrixSelector(b,c,d)Definitions: IdentityMatrixSelector(b,c,d)Original native command in the exact edition - L43
specialize matrix_lattice_identity_selector_exists (d) - L44
apply matrix_lattice_identity_selector_exists
09Separate the logical casesL45–46
10Construct an explicit witnessL47–50
11Separate the logical casesL51–51
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L51
split
12Use earlier factsL52–56
Instantiate or apply named facts and discharge the corresponding proof obligations.
13Separate the logical casesL57–57
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L57
split
14Use earlier factsL58–62
Instantiate or apply named facts and discharge the corresponding proof obligations.
15Construct an explicit witnessL63–64
16Separate the logical casesL65–65
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L65
split
17Construct an explicit witnessL66–69
18Separate the logical casesL70–70
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L70
split
19Use earlier factsL71–80
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L71
specialize matrix_lattice_identity_selected_signed (ab) - L72
specialize matrix_lattice_identity_selected_signed (ac) - L73
specialize matrix_lattice_identity_selected_signed (bb) - L74
specialize matrix_lattice_identity_selected_signed (bc) - L75
specialize matrix_lattice_identity_selected_signed (d) - L76
specialize matrix_lattice_identity_selected_signed (x) - L77
specialize matrix_lattice_identity_selected_signed (x1) - L78
apply matrix_lattice_identity_selected_signed - L79
exact eq_decidable_right - L80
exact hidentity_witness_witness
Original defined command ledger · 82 lines
- 0001
intro ab - 0002
intro ac - 0003
intro bb - 0004
intro bc - 0005
intro d - 0006
intro p - 0007
intro n - 0008
intro hdet - 0009
intro hnonzero - 0010
specialize eq_decidable d - 0011
specialize eq_decidable 0 - 0012
cases eq_decidable - 0013
rewrite eq_decidable_left - 0014
rewrite eq_decidable_left - 0015
rewrite eq_decidable_left - 0016
rewrite eq_decidable_left - 0017
rewrite eq_decidable_left - 0018
rewrite eq_decidable_left - 0019
rewrite eq_decidable_left - 0020
rewrite eq_decidable_left - 0021
rewrite eq_decidable_left - 0022
rewrite eq_decidable_left - 0023
rewrite eq_decidable_left - 0024
rewrite eq_decidable_left - 0025
rewrite eq_decidable_left - 0026
rewrite eq_decidable_left - 0027
rewrite eq_decidable_left - 0028
rewrite eq_decidable_left - 0029
rewrite eq_decidable_left - 0030
rewrite eq_decidable_left - 0031
rewrite eq_decidable_left - 0032
rewrite eq_decidable_left - 0033
rewrite eq_decidable_left - 0034
rewrite eq_decidable_left - 0035
specialize matrix_rank_nonzero_minor_empty (ab) - 0036
specialize matrix_rank_nonzero_minor_empty (ac) - 0037
specialize matrix_rank_nonzero_minor_empty (bb) - 0038
specialize matrix_rank_nonzero_minor_empty (bc) - 0039
specialize matrix_rank_nonzero_minor_empty (0) - 0040
specialize matrix_rank_nonzero_minor_empty (0) - 0041
apply matrix_rank_nonzero_minor_empty - 0042
have hidentity : ∃ b. ∃ c. IdentityMatrixSelector(b,c,d) - 0043
specialize matrix_lattice_identity_selector_exists (d) - 0044
apply matrix_lattice_identity_selector_exists - 0045
cases hidentity - 0046
cases hidentity_witness - 0047
exists x - 0048
exists x1 - 0049
exists x - 0050
exists x1 - 0051
split - 0052
specialize matrix_lattice_identity_is_selector (x) - 0053
specialize matrix_lattice_identity_is_selector (x1) - 0054
specialize matrix_lattice_identity_is_selector (d) - 0055
apply matrix_lattice_identity_is_selector - 0056
exact hidentity_witness_witness - 0057
split - 0058
specialize matrix_lattice_identity_is_selector (x) - 0059
specialize matrix_lattice_identity_is_selector (x1) - 0060
specialize matrix_lattice_identity_is_selector (d) - 0061
apply matrix_lattice_identity_is_selector - 0062
exact hidentity_witness_witness - 0063
exists p - 0064
exists n - 0065
split - 0066
exists ab - 0067
exists ac - 0068
exists bb - 0069
exists bc - 0070
split - 0071
specialize matrix_lattice_identity_selected_signed (ab) - 0072
specialize matrix_lattice_identity_selected_signed (ac) - 0073
specialize matrix_lattice_identity_selected_signed (bb) - 0074
specialize matrix_lattice_identity_selected_signed (bc) - 0075
specialize matrix_lattice_identity_selected_signed (d) - 0076
specialize matrix_lattice_identity_selected_signed (x) - 0077
specialize matrix_lattice_identity_selected_signed (x1) - 0078
apply matrix_lattice_identity_selected_signed - 0079
exact eq_decidable_right - 0080
exact hidentity_witness_witness - 0081
exact hdet - 0082
exact hnonzero