square_matrix_full_rank_from_nonzero_determinant

Exact expanded first-order arithmetic statement

forall ab ac bb bc d p n. (exists mdr_b_nonsingular_determinant mdr_c_nonsingular_determinant mdr_l_nonsingular_determinant mdr_i_nonsingular_determinant. ((forall mdr_i_nonsingular_determinanth. (exists mdr_gap_nonsingular_determinanthi. mdr_gap_nonsingular_determinanthi + S (mdr_i_nonsingular_determinanth) = (mdr_l_nonsingular_determinant)) -> exists mdr_d_nonsingular_determinanth mdr_pb_nonsingular_determinanth mdr_pc_nonsingular_determinanth mdr_nb_nonsingular_determinanth mdr_nc_nonsingular_determinanth mdr_p_nonsingular_determinanth mdr_n_nonsingular_determinanth. ((exists mdr_z_nonsingular_determinanthr. ((exists mdr_a_nonsingular_determinanthrc mdr_b_nonsingular_determinanthrc mdr_c_nonsingular_determinanthrc mdr_e_nonsingular_determinanthrc mdr_f_nonsingular_determinanthrc. ((mdr_a_nonsingular_determinanthrc = ((mdr_d_nonsingular_determinanth) + (mdr_pb_nonsingular_determinanth)) * S ((mdr_d_nonsingular_determinanth) + (mdr_pb_nonsingular_determinanth)) + ((mdr_pb_nonsingular_determinanth) + (mdr_pb_nonsingular_determinanth))) /\ ((mdr_b_nonsingular_determinanthrc = ((mdr_pc_nonsingular_determinanth) + (mdr_nb_nonsingular_determinanth)) * S ((mdr_pc_nonsingular_determinanth) + (mdr_nb_nonsingular_determinanth)) + ((mdr_nb_nonsingular_determinanth) + (mdr_nb_nonsingular_determinanth))) /\ ((mdr_c_nonsingular_determinanthrc = ((mdr_a_nonsingular_determinanthrc) + (mdr_b_nonsingular_determinanthrc)) * S ((mdr_a_nonsingular_determinanthrc) + (mdr_b_nonsingular_determinanthrc)) + ((mdr_b_nonsingular_determinanthrc) + (mdr_b_nonsingular_determinanthrc))) /\ ((mdr_e_nonsingular_determinanthrc = ((mdr_p_nonsingular_determinanth) + (mdr_n_nonsingular_determinanth)) * S ((mdr_p_nonsingular_determinanth) + (mdr_n_nonsingular_determinanth)) + ((mdr_n_nonsingular_determinanth) + (mdr_n_nonsingular_determinanth))) /\ ((mdr_f_nonsingular_determinanthrc = ((mdr_nc_nonsingular_determinanth) + (mdr_e_nonsingular_determinanthrc)) * S ((mdr_nc_nonsingular_determinanth) + (mdr_e_nonsingular_determinanthrc)) + ((mdr_e_nonsingular_determinanthrc) + (mdr_e_nonsingular_determinanthrc))) /\ ((mdr_z_nonsingular_determinanthr) = ((mdr_c_nonsingular_determinanthrc) + (mdr_f_nonsingular_determinanthrc)) * S ((mdr_c_nonsingular_determinanthrc) + (mdr_f_nonsingular_determinanthrc)) + ((mdr_f_nonsingular_determinanthrc) + (mdr_f_nonsingular_determinanthrc))))))))) /\ (((exists ff_h_mdr_nonsingular_determinanthrb. ff_h_mdr_nonsingular_determinanthrb + S (mdr_z_nonsingular_determinanthr) = S ((S (mdr_i_nonsingular_determinanth)) * mdr_c_nonsingular_determinant)) /\ exists ff_q_mdr_nonsingular_determinanthrb. mdr_b_nonsingular_determinant = ff_q_mdr_nonsingular_determinanthrb * S ((S (mdr_i_nonsingular_determinanth)) * mdr_c_nonsingular_determinant) + (mdr_z_nonsingular_determinanthr))))) /\ (((((mdr_d_nonsingular_determinanth) = 0) /\ (((mdr_p_nonsingular_determinanth) = 1) /\ ((mdr_n_nonsingular_determinanth) = 0))) \/ exists mdr_q_nonsingular_determinanths mdr_eb_nonsingular_determinanths mdr_ec_nonsingular_determinanths mdr_fb_nonsingular_determinanths mdr_fc_nonsingular_determinanths. (((mdr_d_nonsingular_determinanth) = S (mdr_q_nonsingular_determinanths)) /\ ((forall mdr_j_nonsingular_determinanthsc. (exists mdr_gap_nonsingular_determinanthscj. mdr_gap_nonsingular_determinanthscj + S (mdr_j_nonsingular_determinanthsc) = (S (mdr_q_nonsingular_determinanths))) -> exists mdr_i_nonsingular_determinanthsc mdr_up_nonsingular_determinanthsc mdr_us_nonsingular_determinanthsc mdr_un_nonsingular_determinanthsc mdr_ut_nonsingular_determinanthsc mdr_p_nonsingular_determinanthsc mdr_n_nonsingular_determinanthsc. ((exists mdr_gap_nonsingular_determinanthsci. mdr_gap_nonsingular_determinanthsci + S (mdr_i_nonsingular_determinanthsc) = (mdr_i_nonsingular_determinanth)) /\ ((exists mdr_z_nonsingular_determinanthscr. ((exists mdr_a_nonsingular_determinanthscrc mdr_b_nonsingular_determinanthscrc mdr_c_nonsingular_determinanthscrc mdr_e_nonsingular_determinanthscrc mdr_f_nonsingular_determinanthscrc. ((mdr_a_nonsingular_determinanthscrc = ((mdr_q_nonsingular_determinanths) + (mdr_up_nonsingular_determinanthsc)) * S ((mdr_q_nonsingular_determinanths) + (mdr_up_nonsingular_determinanthsc)) + ((mdr_up_nonsingular_determinanthsc) + (mdr_up_nonsingular_determinanthsc))) /\ ((mdr_b_nonsingular_determinanthscrc = ((mdr_us_nonsingular_determinanthsc) + (mdr_un_nonsingular_determinanthsc)) * S ((mdr_us_nonsingular_determinanthsc) + (mdr_un_nonsingular_determinanthsc)) + ((mdr_un_nonsingular_determinanthsc) + (mdr_un_nonsingular_determinanthsc))) /\ ((mdr_c_nonsingular_determinanthscrc = ((mdr_a_nonsingular_determinanthscrc) + (mdr_b_nonsingular_determinanthscrc)) * S ((mdr_a_nonsingular_determinanthscrc) + (mdr_b_nonsingular_determinanthscrc)) + ((mdr_b_nonsingular_determinanthscrc) + (mdr_b_nonsingular_determinanthscrc))) /\ ((mdr_e_nonsingular_determinanthscrc = ((mdr_p_nonsingular_determinanthsc) + (mdr_n_nonsingular_determinanthsc)) * S ((mdr_p_nonsingular_determinanthsc) + (mdr_n_nonsingular_determinanthsc)) + ((mdr_n_nonsingular_determinanthsc) + (mdr_n_nonsingular_determinanthsc))) /\ ((mdr_f_nonsingular_determinanthscrc = ((mdr_ut_nonsingular_determinanthsc) + (mdr_e_nonsingular_determinanthscrc)) * S ((mdr_ut_nonsingular_determinanthsc) + (mdr_e_nonsingular_determinanthscrc)) + ((mdr_e_nonsingular_determinanthscrc) + (mdr_e_nonsingular_determinanthscrc))) /\ ((mdr_z_nonsingular_determinanthscr) = ((mdr_c_nonsingular_determinanthscrc) + (mdr_f_nonsingular_determinanthscrc)) * S ((mdr_c_nonsingular_determinanthscrc) + (mdr_f_nonsingular_determinanthscrc)) + ((mdr_f_nonsingular_determinanthscrc) + (mdr_f_nonsingular_determinanthscrc))))))))) /\ (((exists ff_h_mdr_nonsingular_determinanthscrb. ff_h_mdr_nonsingular_determinanthscrb + S (mdr_z_nonsingular_determinanthscr) = S ((S (mdr_i_nonsingular_determinanthsc)) * mdr_c_nonsingular_determinant)) /\ exists ff_q_mdr_nonsingular_determinanthscrb. mdr_b_nonsingular_determinant = ff_q_mdr_nonsingular_determinanthscrb * S ((S (mdr_i_nonsingular_determinanthsc)) * mdr_c_nonsingular_determinant) + (mdr_z_nonsingular_determinanthscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_nonsingular_determinanthscm_positive. (exists ff_gap_mdm_lt_mdr_nonsingular_determinanthscm_positive_index_bound. ff_gap_mdm_lt_mdr_nonsingular_determinanthscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_nonsingular_determinanthscm_positive) = ((mdr_q_nonsingular_determinanths) * (mdr_q_nonsingular_determinanths))) -> exists ff_row_mdm_prefix_mdr_nonsingular_determinanthscm_positive ff_column_mdm_prefix_mdr_nonsingular_determinanthscm_positive ff_value_mdm_prefix_mdr_nonsingular_determinanthscm_positive. (ff_index_mdm_prefix_mdr_nonsingular_determinanthscm_positive = (mdr_q_nonsingular_determinanths) * ff_row_mdm_prefix_mdr_nonsingular_determinanthscm_positive + ff_column_mdm_prefix_mdr_nonsingular_determinanthscm_positive /\ ((exists ff_gap_mdm_lt_mdr_nonsingular_determinanthscm_positive_column_bound. ff_gap_mdm_lt_mdr_nonsingular_determinanthscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_nonsingular_determinanthscm_positive) = (mdr_q_nonsingular_determinanths)) /\ ((exists ff_row_mdm_cell_mdr_nonsingular_determinanthscm_positive_cell ff_column_mdm_cell_mdr_nonsingular_determinanthscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_nonsingular_determinanthscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_nonsingular_determinanthscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_nonsingular_determinanthscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_nonsingular_determinanthscm_positive_cell = ff_row_mdm_prefix_mdr_nonsingular_determinanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_nonsingular_determinanthscm_positive_cell_row_after. ff_gap_mdm_le_mdr_nonsingular_determinanthscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_nonsingular_determinanthscm_positive)) /\ ff_row_mdm_cell_mdr_nonsingular_determinanthscm_positive_cell = S ff_row_mdm_prefix_mdr_nonsingular_determinanthscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_nonsingular_determinanthscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_nonsingular_determinanthscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_nonsingular_determinanthscm_positive) = (mdr_j_nonsingular_determinanthsc)) /\ ff_column_mdm_cell_mdr_nonsingular_determinanthscm_positive_cell = ff_column_mdm_prefix_mdr_nonsingular_determinanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_nonsingular_determinanthscm_positive_cell_column_after. ff_gap_mdm_le_mdr_nonsingular_determinanthscm_positive_cell_column_after + (mdr_j_nonsingular_determinanthsc) = (ff_column_mdm_prefix_mdr_nonsingular_determinanthscm_positive)) /\ ff_column_mdm_cell_mdr_nonsingular_determinanthscm_positive_cell = S ff_column_mdm_prefix_mdr_nonsingular_determinanthscm_positive))) /\ (((exists ff_h_mdm_mdr_nonsingular_determinanthscm_positive_cell_source. ff_h_mdm_mdr_nonsingular_determinanthscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_nonsingular_determinanthscm_positive) = S ((S ((ff_row_mdm_cell_mdr_nonsingular_determinanthscm_positive_cell) * (S (mdr_q_nonsingular_determinanths)) + (ff_column_mdm_cell_mdr_nonsingular_determinanthscm_positive_cell))) * mdr_pc_nonsingular_determinanth)) /\ exists ff_q_mdm_mdr_nonsingular_determinanthscm_positive_cell_source. mdr_pb_nonsingular_determinanth = ff_q_mdm_mdr_nonsingular_determinanthscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_nonsingular_determinanthscm_positive_cell) * (S (mdr_q_nonsingular_determinanths)) + (ff_column_mdm_cell_mdr_nonsingular_determinanthscm_positive_cell))) * mdr_pc_nonsingular_determinanth) + (ff_value_mdm_prefix_mdr_nonsingular_determinanthscm_positive)))))) /\ (((exists ff_h_mdm_mdr_nonsingular_determinanthscm_positive_target. ff_h_mdm_mdr_nonsingular_determinanthscm_positive_target + S (ff_value_mdm_prefix_mdr_nonsingular_determinanthscm_positive) = S ((S (ff_index_mdm_prefix_mdr_nonsingular_determinanthscm_positive)) * mdr_us_nonsingular_determinanthsc)) /\ exists ff_q_mdm_mdr_nonsingular_determinanthscm_positive_target. mdr_up_nonsingular_determinanthsc = ff_q_mdm_mdr_nonsingular_determinanthscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_nonsingular_determinanthscm_positive)) * mdr_us_nonsingular_determinanthsc) + (ff_value_mdm_prefix_mdr_nonsingular_determinanthscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_nonsingular_determinanthscm_negative. (exists ff_gap_mdm_lt_mdr_nonsingular_determinanthscm_negative_index_bound. ff_gap_mdm_lt_mdr_nonsingular_determinanthscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_nonsingular_determinanthscm_negative) = ((mdr_q_nonsingular_determinanths) * (mdr_q_nonsingular_determinanths))) -> exists ff_row_mdm_prefix_mdr_nonsingular_determinanthscm_negative ff_column_mdm_prefix_mdr_nonsingular_determinanthscm_negative ff_value_mdm_prefix_mdr_nonsingular_determinanthscm_negative. (ff_index_mdm_prefix_mdr_nonsingular_determinanthscm_negative = (mdr_q_nonsingular_determinanths) * ff_row_mdm_prefix_mdr_nonsingular_determinanthscm_negative + ff_column_mdm_prefix_mdr_nonsingular_determinanthscm_negative /\ ((exists ff_gap_mdm_lt_mdr_nonsingular_determinanthscm_negative_column_bound. ff_gap_mdm_lt_mdr_nonsingular_determinanthscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_nonsingular_determinanthscm_negative) = (mdr_q_nonsingular_determinanths)) /\ ((exists ff_row_mdm_cell_mdr_nonsingular_determinanthscm_negative_cell ff_column_mdm_cell_mdr_nonsingular_determinanthscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_nonsingular_determinanthscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_nonsingular_determinanthscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_nonsingular_determinanthscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_nonsingular_determinanthscm_negative_cell = ff_row_mdm_prefix_mdr_nonsingular_determinanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_nonsingular_determinanthscm_negative_cell_row_after. ff_gap_mdm_le_mdr_nonsingular_determinanthscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_nonsingular_determinanthscm_negative)) /\ ff_row_mdm_cell_mdr_nonsingular_determinanthscm_negative_cell = S ff_row_mdm_prefix_mdr_nonsingular_determinanthscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_nonsingular_determinanthscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_nonsingular_determinanthscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_nonsingular_determinanthscm_negative) = (mdr_j_nonsingular_determinanthsc)) /\ ff_column_mdm_cell_mdr_nonsingular_determinanthscm_negative_cell = ff_column_mdm_prefix_mdr_nonsingular_determinanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_nonsingular_determinanthscm_negative_cell_column_after. ff_gap_mdm_le_mdr_nonsingular_determinanthscm_negative_cell_column_after + (mdr_j_nonsingular_determinanthsc) = (ff_column_mdm_prefix_mdr_nonsingular_determinanthscm_negative)) /\ ff_column_mdm_cell_mdr_nonsingular_determinanthscm_negative_cell = S ff_column_mdm_prefix_mdr_nonsingular_determinanthscm_negative))) /\ (((exists ff_h_mdm_mdr_nonsingular_determinanthscm_negative_cell_source. ff_h_mdm_mdr_nonsingular_determinanthscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_nonsingular_determinanthscm_negative) = S ((S ((ff_row_mdm_cell_mdr_nonsingular_determinanthscm_negative_cell) * (S (mdr_q_nonsingular_determinanths)) + (ff_column_mdm_cell_mdr_nonsingular_determinanthscm_negative_cell))) * mdr_nc_nonsingular_determinanth)) /\ exists ff_q_mdm_mdr_nonsingular_determinanthscm_negative_cell_source. mdr_nb_nonsingular_determinanth = ff_q_mdm_mdr_nonsingular_determinanthscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_nonsingular_determinanthscm_negative_cell) * (S (mdr_q_nonsingular_determinanths)) + (ff_column_mdm_cell_mdr_nonsingular_determinanthscm_negative_cell))) * mdr_nc_nonsingular_determinanth) + (ff_value_mdm_prefix_mdr_nonsingular_determinanthscm_negative)))))) /\ (((exists ff_h_mdm_mdr_nonsingular_determinanthscm_negative_target. ff_h_mdm_mdr_nonsingular_determinanthscm_negative_target + S (ff_value_mdm_prefix_mdr_nonsingular_determinanthscm_negative) = S ((S (ff_index_mdm_prefix_mdr_nonsingular_determinanthscm_negative)) * mdr_ut_nonsingular_determinanthsc)) /\ exists ff_q_mdm_mdr_nonsingular_determinanthscm_negative_target. mdr_un_nonsingular_determinanthsc = ff_q_mdm_mdr_nonsingular_determinanthscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_nonsingular_determinanthscm_negative)) * mdr_ut_nonsingular_determinanthsc) + (ff_value_mdm_prefix_mdr_nonsingular_determinanthscm_negative))))))))) /\ ((((exists ff_h_mdr_nonsingular_determinanthscp. ff_h_mdr_nonsingular_determinanthscp + S (mdr_p_nonsingular_determinanthsc) = S ((S (mdr_j_nonsingular_determinanthsc)) * mdr_ec_nonsingular_determinanths)) /\ exists ff_q_mdr_nonsingular_determinanthscp. mdr_eb_nonsingular_determinanths = ff_q_mdr_nonsingular_determinanthscp * S ((S (mdr_j_nonsingular_determinanthsc)) * mdr_ec_nonsingular_determinanths) + (mdr_p_nonsingular_determinanthsc))) /\ (((exists ff_h_mdr_nonsingular_determinanthscn. ff_h_mdr_nonsingular_determinanthscn + S (mdr_n_nonsingular_determinanthsc) = S ((S (mdr_j_nonsingular_determinanthsc)) * mdr_fc_nonsingular_determinanths)) /\ exists ff_q_mdr_nonsingular_determinanthscn. mdr_fb_nonsingular_determinanths = ff_q_mdr_nonsingular_determinanthscn * S ((S (mdr_j_nonsingular_determinanthsc)) * mdr_fc_nonsingular_determinanths) + (mdr_n_nonsingular_determinanthsc)))))))) /\ (exists ff_ub_mce_fold_mdr_nonsingular_determinanthsf ff_uc_mce_fold_mdr_nonsingular_determinanthsf ff_vb_mce_fold_mdr_nonsingular_determinanthsf ff_vc_mce_fold_mdr_nonsingular_determinanthsf. ((forall ff_index_mce_alternating_mdr_nonsingular_determinanthsf_prefix. (exists ff_gap_mce_mdr_nonsingular_determinanthsf_prefix_index. ff_gap_mce_mdr_nonsingular_determinanthsf_prefix_index + S (ff_index_mce_alternating_mdr_nonsingular_determinanthsf_prefix) = (S (mdr_q_nonsingular_determinanths))) -> exists ff_ap_mce_alternating_mdr_nonsingular_determinanthsf_prefix ff_an_mce_alternating_mdr_nonsingular_determinanthsf_prefix ff_bp_mce_alternating_mdr_nonsingular_determinanthsf_prefix ff_bn_mce_alternating_mdr_nonsingular_determinanthsf_prefix ff_p_mce_alternating_mdr_nonsingular_determinanthsf_prefix ff_n_mce_alternating_mdr_nonsingular_determinanthsf_prefix. ((((exists ff_h_mce_mdr_nonsingular_determinanthsf_prefix_ap. ff_h_mce_mdr_nonsingular_determinanthsf_prefix_ap + S (ff_ap_mce_alternating_mdr_nonsingular_determinanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_nonsingular_determinanthsf_prefix)) * mdr_pc_nonsingular_determinanth)) /\ exists ff_q_mce_mdr_nonsingular_determinanthsf_prefix_ap. mdr_pb_nonsingular_determinanth = ff_q_mce_mdr_nonsingular_determinanthsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_nonsingular_determinanthsf_prefix)) * mdr_pc_nonsingular_determinanth) + (ff_ap_mce_alternating_mdr_nonsingular_determinanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_nonsingular_determinanthsf_prefix_an. ff_h_mce_mdr_nonsingular_determinanthsf_prefix_an + S (ff_an_mce_alternating_mdr_nonsingular_determinanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_nonsingular_determinanthsf_prefix)) * mdr_nc_nonsingular_determinanth)) /\ exists ff_q_mce_mdr_nonsingular_determinanthsf_prefix_an. mdr_nb_nonsingular_determinanth = ff_q_mce_mdr_nonsingular_determinanthsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_nonsingular_determinanthsf_prefix)) * mdr_nc_nonsingular_determinanth) + (ff_an_mce_alternating_mdr_nonsingular_determinanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_nonsingular_determinanthsf_prefix_bp. ff_h_mce_mdr_nonsingular_determinanthsf_prefix_bp + S (ff_bp_mce_alternating_mdr_nonsingular_determinanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_nonsingular_determinanthsf_prefix)) * mdr_ec_nonsingular_determinanths)) /\ exists ff_q_mce_mdr_nonsingular_determinanthsf_prefix_bp. mdr_eb_nonsingular_determinanths = ff_q_mce_mdr_nonsingular_determinanthsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_nonsingular_determinanthsf_prefix)) * mdr_ec_nonsingular_determinanths) + (ff_bp_mce_alternating_mdr_nonsingular_determinanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_nonsingular_determinanthsf_prefix_bn. ff_h_mce_mdr_nonsingular_determinanthsf_prefix_bn + S (ff_bn_mce_alternating_mdr_nonsingular_determinanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_nonsingular_determinanthsf_prefix)) * mdr_fc_nonsingular_determinanths)) /\ exists ff_q_mce_mdr_nonsingular_determinanthsf_prefix_bn. mdr_fb_nonsingular_determinanths = ff_q_mce_mdr_nonsingular_determinanthsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_nonsingular_determinanthsf_prefix)) * mdr_fc_nonsingular_determinanths) + (ff_bn_mce_alternating_mdr_nonsingular_determinanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_nonsingular_determinanthsf_prefix_positive. ff_h_mce_mdr_nonsingular_determinanthsf_prefix_positive + S (ff_p_mce_alternating_mdr_nonsingular_determinanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_nonsingular_determinanthsf_prefix)) * ff_uc_mce_fold_mdr_nonsingular_determinanthsf)) /\ exists ff_q_mce_mdr_nonsingular_determinanthsf_prefix_positive. ff_ub_mce_fold_mdr_nonsingular_determinanthsf = ff_q_mce_mdr_nonsingular_determinanthsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_nonsingular_determinanthsf_prefix)) * ff_uc_mce_fold_mdr_nonsingular_determinanthsf) + (ff_p_mce_alternating_mdr_nonsingular_determinanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_nonsingular_determinanthsf_prefix_negative. ff_h_mce_mdr_nonsingular_determinanthsf_prefix_negative + S (ff_n_mce_alternating_mdr_nonsingular_determinanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_nonsingular_determinanthsf_prefix)) * ff_vc_mce_fold_mdr_nonsingular_determinanthsf)) /\ exists ff_q_mce_mdr_nonsingular_determinanthsf_prefix_negative. ff_vb_mce_fold_mdr_nonsingular_determinanthsf = ff_q_mce_mdr_nonsingular_determinanthsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_nonsingular_determinanthsf_prefix)) * ff_vc_mce_fold_mdr_nonsingular_determinanthsf) + (ff_n_mce_alternating_mdr_nonsingular_determinanthsf_prefix))) /\ (((exists ff_even_mce_term_mdr_nonsingular_determinanthsf_prefix_term. ff_index_mce_alternating_mdr_nonsingular_determinanthsf_prefix = 2 * ff_even_mce_term_mdr_nonsingular_determinanthsf_prefix_term) /\ (ff_p_mce_alternating_mdr_nonsingular_determinanthsf_prefix = (ff_ap_mce_alternating_mdr_nonsingular_determinanthsf_prefix) * (ff_bp_mce_alternating_mdr_nonsingular_determinanthsf_prefix) + (ff_an_mce_alternating_mdr_nonsingular_determinanthsf_prefix) * (ff_bn_mce_alternating_mdr_nonsingular_determinanthsf_prefix) /\ ff_n_mce_alternating_mdr_nonsingular_determinanthsf_prefix = (ff_ap_mce_alternating_mdr_nonsingular_determinanthsf_prefix) * (ff_bn_mce_alternating_mdr_nonsingular_determinanthsf_prefix) + (ff_an_mce_alternating_mdr_nonsingular_determinanthsf_prefix) * (ff_bp_mce_alternating_mdr_nonsingular_determinanthsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_nonsingular_determinanthsf_prefix_term. ff_index_mce_alternating_mdr_nonsingular_determinanthsf_prefix = 2 * ff_odd_mce_term_mdr_nonsingular_determinanthsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_nonsingular_determinanthsf_prefix = (ff_ap_mce_alternating_mdr_nonsingular_determinanthsf_prefix) * (ff_bn_mce_alternating_mdr_nonsingular_determinanthsf_prefix) + (ff_an_mce_alternating_mdr_nonsingular_determinanthsf_prefix) * (ff_bp_mce_alternating_mdr_nonsingular_determinanthsf_prefix) /\ ff_n_mce_alternating_mdr_nonsingular_determinanthsf_prefix = (ff_ap_mce_alternating_mdr_nonsingular_determinanthsf_prefix) * (ff_bp_mce_alternating_mdr_nonsingular_determinanthsf_prefix) + (ff_an_mce_alternating_mdr_nonsingular_determinanthsf_prefix) * (ff_bn_mce_alternating_mdr_nonsingular_determinanthsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_nonsingular_determinanthsf_positive ff_v_mce_mdr_nonsingular_determinanthsf_positive. ((((exists ff_h_mce_mdr_nonsingular_determinanthsf_positive_start. ff_h_mce_mdr_nonsingular_determinanthsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_nonsingular_determinanthsf_positive)) /\ exists ff_q_mce_mdr_nonsingular_determinanthsf_positive_start. ff_u_mce_mdr_nonsingular_determinanthsf_positive = ff_q_mce_mdr_nonsingular_determinanthsf_positive_start * S ((S (0)) * ff_v_mce_mdr_nonsingular_determinanthsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_nonsingular_determinanthsf_positive_terminal. ff_h_mce_mdr_nonsingular_determinanthsf_positive_terminal + S (mdr_p_nonsingular_determinanth) = S ((S ((S (mdr_q_nonsingular_determinanths)))) * ff_v_mce_mdr_nonsingular_determinanthsf_positive)) /\ exists ff_q_mce_mdr_nonsingular_determinanthsf_positive_terminal. ff_u_mce_mdr_nonsingular_determinanthsf_positive = ff_q_mce_mdr_nonsingular_determinanthsf_positive_terminal * S ((S ((S (mdr_q_nonsingular_determinanths)))) * ff_v_mce_mdr_nonsingular_determinanthsf_positive) + (mdr_p_nonsingular_determinanth))) /\ forall ff_i_mce_mdr_nonsingular_determinanthsf_positive. (exists ff_lt_mce_mdr_nonsingular_determinanthsf_positive_bound. ff_lt_mce_mdr_nonsingular_determinanthsf_positive_bound + S ff_i_mce_mdr_nonsingular_determinanthsf_positive = (S (mdr_q_nonsingular_determinanths))) -> exists ff_a_mce_mdr_nonsingular_determinanthsf_positive ff_r_mce_mdr_nonsingular_determinanthsf_positive ff_s_mce_mdr_nonsingular_determinanthsf_positive. ((((exists ff_h_mce_mdr_nonsingular_determinanthsf_positive_summand. ff_h_mce_mdr_nonsingular_determinanthsf_positive_summand + S (ff_a_mce_mdr_nonsingular_determinanthsf_positive) = S ((S (ff_i_mce_mdr_nonsingular_determinanthsf_positive)) * ff_uc_mce_fold_mdr_nonsingular_determinanthsf)) /\ exists ff_q_mce_mdr_nonsingular_determinanthsf_positive_summand. ff_ub_mce_fold_mdr_nonsingular_determinanthsf = ff_q_mce_mdr_nonsingular_determinanthsf_positive_summand * S ((S (ff_i_mce_mdr_nonsingular_determinanthsf_positive)) * ff_uc_mce_fold_mdr_nonsingular_determinanthsf) + (ff_a_mce_mdr_nonsingular_determinanthsf_positive))) /\ ((((exists ff_h_mce_mdr_nonsingular_determinanthsf_positive_partial. ff_h_mce_mdr_nonsingular_determinanthsf_positive_partial + S (ff_r_mce_mdr_nonsingular_determinanthsf_positive) = S ((S (ff_i_mce_mdr_nonsingular_determinanthsf_positive)) * ff_v_mce_mdr_nonsingular_determinanthsf_positive)) /\ exists ff_q_mce_mdr_nonsingular_determinanthsf_positive_partial. ff_u_mce_mdr_nonsingular_determinanthsf_positive = ff_q_mce_mdr_nonsingular_determinanthsf_positive_partial * S ((S (ff_i_mce_mdr_nonsingular_determinanthsf_positive)) * ff_v_mce_mdr_nonsingular_determinanthsf_positive) + (ff_r_mce_mdr_nonsingular_determinanthsf_positive))) /\ ((((exists ff_h_mce_mdr_nonsingular_determinanthsf_positive_successor. ff_h_mce_mdr_nonsingular_determinanthsf_positive_successor + S (ff_s_mce_mdr_nonsingular_determinanthsf_positive) = S ((S (S ff_i_mce_mdr_nonsingular_determinanthsf_positive)) * ff_v_mce_mdr_nonsingular_determinanthsf_positive)) /\ exists ff_q_mce_mdr_nonsingular_determinanthsf_positive_successor. ff_u_mce_mdr_nonsingular_determinanthsf_positive = ff_q_mce_mdr_nonsingular_determinanthsf_positive_successor * S ((S (S ff_i_mce_mdr_nonsingular_determinanthsf_positive)) * ff_v_mce_mdr_nonsingular_determinanthsf_positive) + (ff_s_mce_mdr_nonsingular_determinanthsf_positive))) /\ ff_s_mce_mdr_nonsingular_determinanthsf_positive = ff_r_mce_mdr_nonsingular_determinanthsf_positive + ff_a_mce_mdr_nonsingular_determinanthsf_positive)))))) /\ (exists ff_u_mce_mdr_nonsingular_determinanthsf_negative ff_v_mce_mdr_nonsingular_determinanthsf_negative. ((((exists ff_h_mce_mdr_nonsingular_determinanthsf_negative_start. ff_h_mce_mdr_nonsingular_determinanthsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_nonsingular_determinanthsf_negative)) /\ exists ff_q_mce_mdr_nonsingular_determinanthsf_negative_start. ff_u_mce_mdr_nonsingular_determinanthsf_negative = ff_q_mce_mdr_nonsingular_determinanthsf_negative_start * S ((S (0)) * ff_v_mce_mdr_nonsingular_determinanthsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_nonsingular_determinanthsf_negative_terminal. ff_h_mce_mdr_nonsingular_determinanthsf_negative_terminal + S (mdr_n_nonsingular_determinanth) = S ((S ((S (mdr_q_nonsingular_determinanths)))) * ff_v_mce_mdr_nonsingular_determinanthsf_negative)) /\ exists ff_q_mce_mdr_nonsingular_determinanthsf_negative_terminal. ff_u_mce_mdr_nonsingular_determinanthsf_negative = ff_q_mce_mdr_nonsingular_determinanthsf_negative_terminal * S ((S ((S (mdr_q_nonsingular_determinanths)))) * ff_v_mce_mdr_nonsingular_determinanthsf_negative) + (mdr_n_nonsingular_determinanth))) /\ forall ff_i_mce_mdr_nonsingular_determinanthsf_negative. (exists ff_lt_mce_mdr_nonsingular_determinanthsf_negative_bound. ff_lt_mce_mdr_nonsingular_determinanthsf_negative_bound + S ff_i_mce_mdr_nonsingular_determinanthsf_negative = (S (mdr_q_nonsingular_determinanths))) -> exists ff_a_mce_mdr_nonsingular_determinanthsf_negative ff_r_mce_mdr_nonsingular_determinanthsf_negative ff_s_mce_mdr_nonsingular_determinanthsf_negative. ((((exists ff_h_mce_mdr_nonsingular_determinanthsf_negative_summand. ff_h_mce_mdr_nonsingular_determinanthsf_negative_summand + S (ff_a_mce_mdr_nonsingular_determinanthsf_negative) = S ((S (ff_i_mce_mdr_nonsingular_determinanthsf_negative)) * ff_vc_mce_fold_mdr_nonsingular_determinanthsf)) /\ exists ff_q_mce_mdr_nonsingular_determinanthsf_negative_summand. ff_vb_mce_fold_mdr_nonsingular_determinanthsf = ff_q_mce_mdr_nonsingular_determinanthsf_negative_summand * S ((S (ff_i_mce_mdr_nonsingular_determinanthsf_negative)) * ff_vc_mce_fold_mdr_nonsingular_determinanthsf) + (ff_a_mce_mdr_nonsingular_determinanthsf_negative))) /\ ((((exists ff_h_mce_mdr_nonsingular_determinanthsf_negative_partial. ff_h_mce_mdr_nonsingular_determinanthsf_negative_partial + S (ff_r_mce_mdr_nonsingular_determinanthsf_negative) = S ((S (ff_i_mce_mdr_nonsingular_determinanthsf_negative)) * ff_v_mce_mdr_nonsingular_determinanthsf_negative)) /\ exists ff_q_mce_mdr_nonsingular_determinanthsf_negative_partial. ff_u_mce_mdr_nonsingular_determinanthsf_negative = ff_q_mce_mdr_nonsingular_determinanthsf_negative_partial * S ((S (ff_i_mce_mdr_nonsingular_determinanthsf_negative)) * ff_v_mce_mdr_nonsingular_determinanthsf_negative) + (ff_r_mce_mdr_nonsingular_determinanthsf_negative))) /\ ((((exists ff_h_mce_mdr_nonsingular_determinanthsf_negative_successor. ff_h_mce_mdr_nonsingular_determinanthsf_negative_successor + S (ff_s_mce_mdr_nonsingular_determinanthsf_negative) = S ((S (S ff_i_mce_mdr_nonsingular_determinanthsf_negative)) * ff_v_mce_mdr_nonsingular_determinanthsf_negative)) /\ exists ff_q_mce_mdr_nonsingular_determinanthsf_negative_successor. ff_u_mce_mdr_nonsingular_determinanthsf_negative = ff_q_mce_mdr_nonsingular_determinanthsf_negative_successor * S ((S (S ff_i_mce_mdr_nonsingular_determinanthsf_negative)) * ff_v_mce_mdr_nonsingular_determinanthsf_negative) + (ff_s_mce_mdr_nonsingular_determinanthsf_negative))) /\ ff_s_mce_mdr_nonsingular_determinanthsf_negative = ff_r_mce_mdr_nonsingular_determinanthsf_negative + ff_a_mce_mdr_nonsingular_determinanthsf_negative))))))))))))))) /\ ((exists mdr_gap_nonsingular_determinanti. mdr_gap_nonsingular_determinanti + S (mdr_i_nonsingular_determinant) = (mdr_l_nonsingular_determinant)) /\ (exists mdr_z_nonsingular_determinantr. ((exists mdr_a_nonsingular_determinantrc mdr_b_nonsingular_determinantrc mdr_c_nonsingular_determinantrc mdr_e_nonsingular_determinantrc mdr_f_nonsingular_determinantrc. ((mdr_a_nonsingular_determinantrc = ((d) + (ab)) * S ((d) + (ab)) + ((ab) + (ab))) /\ ((mdr_b_nonsingular_determinantrc = ((ac) + (bb)) * S ((ac) + (bb)) + ((bb) + (bb))) /\ ((mdr_c_nonsingular_determinantrc = ((mdr_a_nonsingular_determinantrc) + (mdr_b_nonsingular_determinantrc)) * S ((mdr_a_nonsingular_determinantrc) + (mdr_b_nonsingular_determinantrc)) + ((mdr_b_nonsingular_determinantrc) + (mdr_b_nonsingular_determinantrc))) /\ ((mdr_e_nonsingular_determinantrc = ((p) + (n)) * S ((p) + (n)) + ((n) + (n))) /\ ((mdr_f_nonsingular_determinantrc = ((bc) + (mdr_e_nonsingular_determinantrc)) * S ((bc) + (mdr_e_nonsingular_determinantrc)) + ((mdr_e_nonsingular_determinantrc) + (mdr_e_nonsingular_determinantrc))) /\ ((mdr_z_nonsingular_determinantr) = ((mdr_c_nonsingular_determinantrc) + (mdr_f_nonsingular_determinantrc)) * S ((mdr_c_nonsingular_determinantrc) + (mdr_f_nonsingular_determinantrc)) + ((mdr_f_nonsingular_determinantrc) + (mdr_f_nonsingular_determinantrc))))))))) /\ (((exists ff_h_mdr_nonsingular_determinantrb. ff_h_mdr_nonsingular_determinantrb + S (mdr_z_nonsingular_determinantr) = S ((S (mdr_i_nonsingular_determinant)) * mdr_c_nonsingular_determinant)) /\ exists ff_q_mdr_nonsingular_determinantrb. mdr_b_nonsingular_determinant = ff_q_mdr_nonsingular_determinantrb * S ((S (mdr_i_nonsingular_determinant)) * mdr_c_nonsingular_determinant) + (mdr_z_nonsingular_determinantr)))))))) -> ~(p = n) -> (((exists mdr_gap_nonsingular_rankrows_bound. mdr_gap_nonsingular_rankrows_bound + (d) = (d)) /\ ((exists mdr_gap_nonsingular_rankcolumns_bound. mdr_gap_nonsingular_rankcolumns_bound + (d) = (d)) /\ ((exists mdr_rb_nonsingular_rankwitness mdr_rc_nonsingular_rankwitness mdr_cb_nonsingular_rankwitness mdr_cc_nonsingular_rankwitness. (((((forall fom_index_mrf_nonsingular_rankwitnessminorrowsbound. (exists fom_gap_mrf_nonsingular_rankwitnessminorrowsbound_index_bound. fom_gap_mrf_nonsingular_rankwitnessminorrowsbound_index_bound + S (fom_index_mrf_nonsingular_rankwitnessminorrowsbound) = d) -> exists fom_value_mrf_nonsingular_rankwitnessminorrowsbound. ((((exists fom_beta_height_mrf_nonsingular_rankwitnessminorrowsbound_entry. fom_beta_height_mrf_nonsingular_rankwitnessminorrowsbound_entry + S (fom_value_mrf_nonsingular_rankwitnessminorrowsbound) = S ((S (fom_index_mrf_nonsingular_rankwitnessminorrowsbound)) * mdr_rc_nonsingular_rankwitness)) /\ exists fom_beta_quotient_mrf_nonsingular_rankwitnessminorrowsbound_entry. mdr_rb_nonsingular_rankwitness = fom_beta_quotient_mrf_nonsingular_rankwitnessminorrowsbound_entry * S ((S (fom_index_mrf_nonsingular_rankwitnessminorrowsbound)) * mdr_rc_nonsingular_rankwitness) + (fom_value_mrf_nonsingular_rankwitnessminorrowsbound))) /\ (exists fom_gap_mrf_nonsingular_rankwitnessminorrowsbound_value_bound. fom_gap_mrf_nonsingular_rankwitnessminorrowsbound_value_bound + S (fom_value_mrf_nonsingular_rankwitnessminorrowsbound) = d))) /\ (forall mdr_i_nonsingular_rankwitnessminorrowsdistinct mdr_j_nonsingular_rankwitnessminorrowsdistinct mdr_a_nonsingular_rankwitnessminorrowsdistinct. (exists mdr_gap_nonsingular_rankwitnessminorrowsdistincti. mdr_gap_nonsingular_rankwitnessminorrowsdistincti + S (mdr_i_nonsingular_rankwitnessminorrowsdistinct) = (d)) -> (exists mdr_gap_nonsingular_rankwitnessminorrowsdistinctj. mdr_gap_nonsingular_rankwitnessminorrowsdistinctj + S (mdr_j_nonsingular_rankwitnessminorrowsdistinct) = (d)) -> (((exists ff_h_mdr_nonsingular_rankwitnessminorrowsdistinctfirst. ff_h_mdr_nonsingular_rankwitnessminorrowsdistinctfirst + S (mdr_a_nonsingular_rankwitnessminorrowsdistinct) = S ((S (mdr_i_nonsingular_rankwitnessminorrowsdistinct)) * mdr_rc_nonsingular_rankwitness)) /\ exists ff_q_mdr_nonsingular_rankwitnessminorrowsdistinctfirst. mdr_rb_nonsingular_rankwitness = ff_q_mdr_nonsingular_rankwitnessminorrowsdistinctfirst * S ((S (mdr_i_nonsingular_rankwitnessminorrowsdistinct)) * mdr_rc_nonsingular_rankwitness) + (mdr_a_nonsingular_rankwitnessminorrowsdistinct))) -> (((exists ff_h_mdr_nonsingular_rankwitnessminorrowsdistinctsecond. ff_h_mdr_nonsingular_rankwitnessminorrowsdistinctsecond + S (mdr_a_nonsingular_rankwitnessminorrowsdistinct) = S ((S (mdr_j_nonsingular_rankwitnessminorrowsdistinct)) * mdr_rc_nonsingular_rankwitness)) /\ exists ff_q_mdr_nonsingular_rankwitnessminorrowsdistinctsecond. mdr_rb_nonsingular_rankwitness = ff_q_mdr_nonsingular_rankwitnessminorrowsdistinctsecond * S ((S (mdr_j_nonsingular_rankwitnessminorrowsdistinct)) * mdr_rc_nonsingular_rankwitness) + (mdr_a_nonsingular_rankwitnessminorrowsdistinct))) -> mdr_i_nonsingular_rankwitnessminorrowsdistinct = mdr_j_nonsingular_rankwitnessminorrowsdistinct))) /\ ((((forall fom_index_mrf_nonsingular_rankwitnessminorcolumnsbound. (exists fom_gap_mrf_nonsingular_rankwitnessminorcolumnsbound_index_bound. fom_gap_mrf_nonsingular_rankwitnessminorcolumnsbound_index_bound + S (fom_index_mrf_nonsingular_rankwitnessminorcolumnsbound) = d) -> exists fom_value_mrf_nonsingular_rankwitnessminorcolumnsbound. ((((exists fom_beta_height_mrf_nonsingular_rankwitnessminorcolumnsbound_entry. fom_beta_height_mrf_nonsingular_rankwitnessminorcolumnsbound_entry + S (fom_value_mrf_nonsingular_rankwitnessminorcolumnsbound) = S ((S (fom_index_mrf_nonsingular_rankwitnessminorcolumnsbound)) * mdr_cc_nonsingular_rankwitness)) /\ exists fom_beta_quotient_mrf_nonsingular_rankwitnessminorcolumnsbound_entry. mdr_cb_nonsingular_rankwitness = fom_beta_quotient_mrf_nonsingular_rankwitnessminorcolumnsbound_entry * S ((S (fom_index_mrf_nonsingular_rankwitnessminorcolumnsbound)) * mdr_cc_nonsingular_rankwitness) + (fom_value_mrf_nonsingular_rankwitnessminorcolumnsbound))) /\ (exists fom_gap_mrf_nonsingular_rankwitnessminorcolumnsbound_value_bound. fom_gap_mrf_nonsingular_rankwitnessminorcolumnsbound_value_bound + S (fom_value_mrf_nonsingular_rankwitnessminorcolumnsbound) = d))) /\ (forall mdr_i_nonsingular_rankwitnessminorcolumnsdistinct mdr_j_nonsingular_rankwitnessminorcolumnsdistinct mdr_a_nonsingular_rankwitnessminorcolumnsdistinct. (exists mdr_gap_nonsingular_rankwitnessminorcolumnsdistincti. mdr_gap_nonsingular_rankwitnessminorcolumnsdistincti + S (mdr_i_nonsingular_rankwitnessminorcolumnsdistinct) = (d)) -> (exists mdr_gap_nonsingular_rankwitnessminorcolumnsdistinctj. mdr_gap_nonsingular_rankwitnessminorcolumnsdistinctj + S (mdr_j_nonsingular_rankwitnessminorcolumnsdistinct) = (d)) -> (((exists ff_h_mdr_nonsingular_rankwitnessminorcolumnsdistinctfirst. ff_h_mdr_nonsingular_rankwitnessminorcolumnsdistinctfirst + S (mdr_a_nonsingular_rankwitnessminorcolumnsdistinct) = S ((S (mdr_i_nonsingular_rankwitnessminorcolumnsdistinct)) * mdr_cc_nonsingular_rankwitness)) /\ exists ff_q_mdr_nonsingular_rankwitnessminorcolumnsdistinctfirst. mdr_cb_nonsingular_rankwitness = ff_q_mdr_nonsingular_rankwitnessminorcolumnsdistinctfirst * S ((S (mdr_i_nonsingular_rankwitnessminorcolumnsdistinct)) * mdr_cc_nonsingular_rankwitness) + (mdr_a_nonsingular_rankwitnessminorcolumnsdistinct))) -> (((exists ff_h_mdr_nonsingular_rankwitnessminorcolumnsdistinctsecond. ff_h_mdr_nonsingular_rankwitnessminorcolumnsdistinctsecond + S (mdr_a_nonsingular_rankwitnessminorcolumnsdistinct) = S ((S (mdr_j_nonsingular_rankwitnessminorcolumnsdistinct)) * mdr_cc_nonsingular_rankwitness)) /\ exists ff_q_mdr_nonsingular_rankwitnessminorcolumnsdistinctsecond. mdr_cb_nonsingular_rankwitness = ff_q_mdr_nonsingular_rankwitnessminorcolumnsdistinctsecond * S ((S (mdr_j_nonsingular_rankwitnessminorcolumnsdistinct)) * mdr_cc_nonsingular_rankwitness) + (mdr_a_nonsingular_rankwitnessminorcolumnsdistinct))) -> mdr_i_nonsingular_rankwitnessminorcolumnsdistinct = mdr_j_nonsingular_rankwitnessminorcolumnsdistinct))) /\ (exists mdr_p_nonsingular_rankwitnessminornonzero mdr_n_nonsingular_rankwitnessminornonzero. ((exists mdr_ub_nonsingular_rankwitnessminornonzeroevaluation mdr_uc_nonsingular_rankwitnessminornonzeroevaluation mdr_vb_nonsingular_rankwitnessminornonzeroevaluation mdr_vc_nonsingular_rankwitnessminornonzeroevaluation. ((((forall mdr_i_nonsingular_rankwitnessminornonzeroevaluationmatrixpositive. (exists mdr_gap_nonsingular_rankwitnessminornonzeroevaluationmatrixpositivebound. mdr_gap_nonsingular_rankwitnessminornonzeroevaluationmatrixpositivebound + S (mdr_i_nonsingular_rankwitnessminornonzeroevaluationmatrixpositive) = ((d) * (d))) -> exists mdr_a_nonsingular_rankwitnessminornonzeroevaluationmatrixpositive. (((exists mdr_r_nonsingular_rankwitnessminornonzeroevaluationmatrixpositivepoint mdr_s_nonsingular_rankwitnessminornonzeroevaluationmatrixpositivepoint mdr_u_nonsingular_rankwitnessminornonzeroevaluationmatrixpositivepoint mdr_v_nonsingular_rankwitnessminornonzeroevaluationmatrixpositivepoint. ((mdr_i_nonsingular_rankwitnessminornonzeroevaluationmatrixpositive = (d) * mdr_r_nonsingular_rankwitnessminornonzeroevaluationmatrixpositivepoint + mdr_s_nonsingular_rankwitnessminornonzeroevaluationmatrixpositivepoint) /\ ((exists mdr_gap_nonsingular_rankwitnessminornonzeroevaluationmatrixpositivepointcolumn. mdr_gap_nonsingular_rankwitnessminornonzeroevaluationmatrixpositivepointcolumn + S (mdr_s_nonsingular_rankwitnessminornonzeroevaluationmatrixpositivepoint) = (d)) /\ ((((exists ff_h_mdr_nonsingular_rankwitnessminornonzeroevaluationmatrixpositivepointrow_index. ff_h_mdr_nonsingular_rankwitnessminornonzeroevaluationmatrixpositivepointrow_index + S (mdr_u_nonsingular_rankwitnessminornonzeroevaluationmatrixpositivepoint) = S ((S (mdr_r_nonsingular_rankwitnessminornonzeroevaluationmatrixpositivepoint)) * mdr_rc_nonsingular_rankwitness)) /\ exists ff_q_mdr_nonsingular_rankwitnessminornonzeroevaluationmatrixpositivepointrow_index. mdr_rb_nonsingular_rankwitness = ff_q_mdr_nonsingular_rankwitnessminornonzeroevaluationmatrixpositivepointrow_index * S ((S (mdr_r_nonsingular_rankwitnessminornonzeroevaluationmatrixpositivepoint)) * mdr_rc_nonsingular_rankwitness) + (mdr_u_nonsingular_rankwitnessminornonzeroevaluationmatrixpositivepoint))) /\ ((((exists ff_h_mdr_nonsingular_rankwitnessminornonzeroevaluationmatrixpositivepointcolumn_index. ff_h_mdr_nonsingular_rankwitnessminornonzeroevaluationmatrixpositivepointcolumn_index + S (mdr_v_nonsingular_rankwitnessminornonzeroevaluationmatrixpositivepoint) = S ((S (mdr_s_nonsingular_rankwitnessminornonzeroevaluationmatrixpositivepoint)) * mdr_cc_nonsingular_rankwitness)) /\ exists ff_q_mdr_nonsingular_rankwitnessminornonzeroevaluationmatrixpositivepointcolumn_index. mdr_cb_nonsingular_rankwitness = ff_q_mdr_nonsingular_rankwitnessminornonzeroevaluationmatrixpositivepointcolumn_index * S ((S (mdr_s_nonsingular_rankwitnessminornonzeroevaluationmatrixpositivepoint)) * mdr_cc_nonsingular_rankwitness) + (mdr_v_nonsingular_rankwitnessminornonzeroevaluationmatrixpositivepoint))) /\ (((exists ff_h_mdr_nonsingular_rankwitnessminornonzeroevaluationmatrixpositivepointsource. ff_h_mdr_nonsingular_rankwitnessminornonzeroevaluationmatrixpositivepointsource + S (mdr_a_nonsingular_rankwitnessminornonzeroevaluationmatrixpositive) = S ((S ((mdr_u_nonsingular_rankwitnessminornonzeroevaluationmatrixpositivepoint) * (d) + (mdr_v_nonsingular_rankwitnessminornonzeroevaluationmatrixpositivepoint))) * ac)) /\ exists ff_q_mdr_nonsingular_rankwitnessminornonzeroevaluationmatrixpositivepointsource. ab = ff_q_mdr_nonsingular_rankwitnessminornonzeroevaluationmatrixpositivepointsource * S ((S ((mdr_u_nonsingular_rankwitnessminornonzeroevaluationmatrixpositivepoint) * (d) + (mdr_v_nonsingular_rankwitnessminornonzeroevaluationmatrixpositivepoint))) * ac) + (mdr_a_nonsingular_rankwitnessminornonzeroevaluationmatrixpositive)))))))) /\ (((exists ff_h_mdr_nonsingular_rankwitnessminornonzeroevaluationmatrixpositiveoutput. ff_h_mdr_nonsingular_rankwitnessminornonzeroevaluationmatrixpositiveoutput + S (mdr_a_nonsingular_rankwitnessminornonzeroevaluationmatrixpositive) = S ((S (mdr_i_nonsingular_rankwitnessminornonzeroevaluationmatrixpositive)) * mdr_uc_nonsingular_rankwitnessminornonzeroevaluation)) /\ exists ff_q_mdr_nonsingular_rankwitnessminornonzeroevaluationmatrixpositiveoutput. mdr_ub_nonsingular_rankwitnessminornonzeroevaluation = ff_q_mdr_nonsingular_rankwitnessminornonzeroevaluationmatrixpositiveoutput * S ((S (mdr_i_nonsingular_rankwitnessminornonzeroevaluationmatrixpositive)) * mdr_uc_nonsingular_rankwitnessminornonzeroevaluation) + (mdr_a_nonsingular_rankwitnessminornonzeroevaluationmatrixpositive)))))) /\ (forall mdr_i_nonsingular_rankwitnessminornonzeroevaluationmatrixnegative. (exists mdr_gap_nonsingular_rankwitnessminornonzeroevaluationmatrixnegativebound. mdr_gap_nonsingular_rankwitnessminornonzeroevaluationmatrixnegativebound + S (mdr_i_nonsingular_rankwitnessminornonzeroevaluationmatrixnegative) = ((d) * (d))) -> exists mdr_a_nonsingular_rankwitnessminornonzeroevaluationmatrixnegative. (((exists mdr_r_nonsingular_rankwitnessminornonzeroevaluationmatrixnegativepoint mdr_s_nonsingular_rankwitnessminornonzeroevaluationmatrixnegativepoint mdr_u_nonsingular_rankwitnessminornonzeroevaluationmatrixnegativepoint mdr_v_nonsingular_rankwitnessminornonzeroevaluationmatrixnegativepoint. ((mdr_i_nonsingular_rankwitnessminornonzeroevaluationmatrixnegative = (d) * mdr_r_nonsingular_rankwitnessminornonzeroevaluationmatrixnegativepoint + mdr_s_nonsingular_rankwitnessminornonzeroevaluationmatrixnegativepoint) /\ ((exists mdr_gap_nonsingular_rankwitnessminornonzeroevaluationmatrixnegativepointcolumn. mdr_gap_nonsingular_rankwitnessminornonzeroevaluationmatrixnegativepointcolumn + S (mdr_s_nonsingular_rankwitnessminornonzeroevaluationmatrixnegativepoint) = (d)) /\ ((((exists ff_h_mdr_nonsingular_rankwitnessminornonzeroevaluationmatrixnegativepointrow_index. ff_h_mdr_nonsingular_rankwitnessminornonzeroevaluationmatrixnegativepointrow_index + S (mdr_u_nonsingular_rankwitnessminornonzeroevaluationmatrixnegativepoint) = S ((S (mdr_r_nonsingular_rankwitnessminornonzeroevaluationmatrixnegativepoint)) * mdr_rc_nonsingular_rankwitness)) /\ exists ff_q_mdr_nonsingular_rankwitnessminornonzeroevaluationmatrixnegativepointrow_index. mdr_rb_nonsingular_rankwitness = ff_q_mdr_nonsingular_rankwitnessminornonzeroevaluationmatrixnegativepointrow_index * S ((S (mdr_r_nonsingular_rankwitnessminornonzeroevaluationmatrixnegativepoint)) * mdr_rc_nonsingular_rankwitness) + (mdr_u_nonsingular_rankwitnessminornonzeroevaluationmatrixnegativepoint))) /\ ((((exists ff_h_mdr_nonsingular_rankwitnessminornonzeroevaluationmatrixnegativepointcolumn_index. ff_h_mdr_nonsingular_rankwitnessminornonzeroevaluationmatrixnegativepointcolumn_index + S (mdr_v_nonsingular_rankwitnessminornonzeroevaluationmatrixnegativepoint) = S ((S (mdr_s_nonsingular_rankwitnessminornonzeroevaluationmatrixnegativepoint)) * mdr_cc_nonsingular_rankwitness)) /\ exists ff_q_mdr_nonsingular_rankwitnessminornonzeroevaluationmatrixnegativepointcolumn_index. mdr_cb_nonsingular_rankwitness = ff_q_mdr_nonsingular_rankwitnessminornonzeroevaluationmatrixnegativepointcolumn_index * S ((S (mdr_s_nonsingular_rankwitnessminornonzeroevaluationmatrixnegativepoint)) * mdr_cc_nonsingular_rankwitness) + (mdr_v_nonsingular_rankwitnessminornonzeroevaluationmatrixnegativepoint))) /\ (((exists ff_h_mdr_nonsingular_rankwitnessminornonzeroevaluationmatrixnegativepointsource. ff_h_mdr_nonsingular_rankwitnessminornonzeroevaluationmatrixnegativepointsource + S (mdr_a_nonsingular_rankwitnessminornonzeroevaluationmatrixnegative) = S ((S ((mdr_u_nonsingular_rankwitnessminornonzeroevaluationmatrixnegativepoint) * (d) + (mdr_v_nonsingular_rankwitnessminornonzeroevaluationmatrixnegativepoint))) * bc)) /\ exists ff_q_mdr_nonsingular_rankwitnessminornonzeroevaluationmatrixnegativepointsource. bb = ff_q_mdr_nonsingular_rankwitnessminornonzeroevaluationmatrixnegativepointsource * S ((S ((mdr_u_nonsingular_rankwitnessminornonzeroevaluationmatrixnegativepoint) * (d) + (mdr_v_nonsingular_rankwitnessminornonzeroevaluationmatrixnegativepoint))) * bc) + (mdr_a_nonsingular_rankwitnessminornonzeroevaluationmatrixnegative)))))))) /\ (((exists ff_h_mdr_nonsingular_rankwitnessminornonzeroevaluationmatrixnegativeoutput. ff_h_mdr_nonsingular_rankwitnessminornonzeroevaluationmatrixnegativeoutput + S (mdr_a_nonsingular_rankwitnessminornonzeroevaluationmatrixnegative) = S ((S (mdr_i_nonsingular_rankwitnessminornonzeroevaluationmatrixnegative)) * mdr_vc_nonsingular_rankwitnessminornonzeroevaluation)) /\ exists ff_q_mdr_nonsingular_rankwitnessminornonzeroevaluationmatrixnegativeoutput. mdr_vb_nonsingular_rankwitnessminornonzeroevaluation = ff_q_mdr_nonsingular_rankwitnessminornonzeroevaluationmatrixnegativeoutput * S ((S (mdr_i_nonsingular_rankwitnessminornonzeroevaluationmatrixnegative)) * mdr_vc_nonsingular_rankwitnessminornonzeroevaluation) + (mdr_a_nonsingular_rankwitnessminornonzeroevaluationmatrixnegative)))))))) /\ (exists mdr_b_nonsingular_rankwitnessminornonzeroevaluationdeterminant mdr_c_nonsingular_rankwitnessminornonzeroevaluationdeterminant mdr_l_nonsingular_rankwitnessminornonzeroevaluationdeterminant mdr_i_nonsingular_rankwitnessminornonzeroevaluationdeterminant. ((forall mdr_i_nonsingular_rankwitnessminornonzeroevaluationdeterminanth. (exists mdr_gap_nonsingular_rankwitnessminornonzeroevaluationdeterminanthi. mdr_gap_nonsingular_rankwitnessminornonzeroevaluationdeterminanthi + S (mdr_i_nonsingular_rankwitnessminornonzeroevaluationdeterminanth) = (mdr_l_nonsingular_rankwitnessminornonzeroevaluationdeterminant)) -> exists mdr_d_nonsingular_rankwitnessminornonzeroevaluationdeterminanth mdr_pb_nonsingular_rankwitnessminornonzeroevaluationdeterminanth mdr_pc_nonsingular_rankwitnessminornonzeroevaluationdeterminanth mdr_nb_nonsingular_rankwitnessminornonzeroevaluationdeterminanth mdr_nc_nonsingular_rankwitnessminornonzeroevaluationdeterminanth mdr_p_nonsingular_rankwitnessminornonzeroevaluationdeterminanth mdr_n_nonsingular_rankwitnessminornonzeroevaluationdeterminanth. ((exists mdr_z_nonsingular_rankwitnessminornonzeroevaluationdeterminanthr. ((exists mdr_a_nonsingular_rankwitnessminornonzeroevaluationdeterminanthrc mdr_b_nonsingular_rankwitnessminornonzeroevaluationdeterminanthrc mdr_c_nonsingular_rankwitnessminornonzeroevaluationdeterminanthrc mdr_e_nonsingular_rankwitnessminornonzeroevaluationdeterminanthrc mdr_f_nonsingular_rankwitnessminornonzeroevaluationdeterminanthrc. ((mdr_a_nonsingular_rankwitnessminornonzeroevaluationdeterminanthrc = ((mdr_d_nonsingular_rankwitnessminornonzeroevaluationdeterminanth) + (mdr_pb_nonsingular_rankwitnessminornonzeroevaluationdeterminanth)) * S ((mdr_d_nonsingular_rankwitnessminornonzeroevaluationdeterminanth) + (mdr_pb_nonsingular_rankwitnessminornonzeroevaluationdeterminanth)) + ((mdr_pb_nonsingular_rankwitnessminornonzeroevaluationdeterminanth) + (mdr_pb_nonsingular_rankwitnessminornonzeroevaluationdeterminanth))) /\ ((mdr_b_nonsingular_rankwitnessminornonzeroevaluationdeterminanthrc = ((mdr_pc_nonsingular_rankwitnessminornonzeroevaluationdeterminanth) + (mdr_nb_nonsingular_rankwitnessminornonzeroevaluationdeterminanth)) * S ((mdr_pc_nonsingular_rankwitnessminornonzeroevaluationdeterminanth) + (mdr_nb_nonsingular_rankwitnessminornonzeroevaluationdeterminanth)) + ((mdr_nb_nonsingular_rankwitnessminornonzeroevaluationdeterminanth) + (mdr_nb_nonsingular_rankwitnessminornonzeroevaluationdeterminanth))) /\ ((mdr_c_nonsingular_rankwitnessminornonzeroevaluationdeterminanthrc = ((mdr_a_nonsingular_rankwitnessminornonzeroevaluationdeterminanthrc) + (mdr_b_nonsingular_rankwitnessminornonzeroevaluationdeterminanthrc)) * S ((mdr_a_nonsingular_rankwitnessminornonzeroevaluationdeterminanthrc) + (mdr_b_nonsingular_rankwitnessminornonzeroevaluationdeterminanthrc)) + ((mdr_b_nonsingular_rankwitnessminornonzeroevaluationdeterminanthrc) + (mdr_b_nonsingular_rankwitnessminornonzeroevaluationdeterminanthrc))) /\ ((mdr_e_nonsingular_rankwitnessminornonzeroevaluationdeterminanthrc = ((mdr_p_nonsingular_rankwitnessminornonzeroevaluationdeterminanth) + (mdr_n_nonsingular_rankwitnessminornonzeroevaluationdeterminanth)) * S ((mdr_p_nonsingular_rankwitnessminornonzeroevaluationdeterminanth) + (mdr_n_nonsingular_rankwitnessminornonzeroevaluationdeterminanth)) + ((mdr_n_nonsingular_rankwitnessminornonzeroevaluationdeterminanth) + (mdr_n_nonsingular_rankwitnessminornonzeroevaluationdeterminanth))) /\ ((mdr_f_nonsingular_rankwitnessminornonzeroevaluationdeterminanthrc = ((mdr_nc_nonsingular_rankwitnessminornonzeroevaluationdeterminanth) + (mdr_e_nonsingular_rankwitnessminornonzeroevaluationdeterminanthrc)) * S ((mdr_nc_nonsingular_rankwitnessminornonzeroevaluationdeterminanth) + (mdr_e_nonsingular_rankwitnessminornonzeroevaluationdeterminanthrc)) + ((mdr_e_nonsingular_rankwitnessminornonzeroevaluationdeterminanthrc) + (mdr_e_nonsingular_rankwitnessminornonzeroevaluationdeterminanthrc))) /\ ((mdr_z_nonsingular_rankwitnessminornonzeroevaluationdeterminanthr) = ((mdr_c_nonsingular_rankwitnessminornonzeroevaluationdeterminanthrc) + (mdr_f_nonsingular_rankwitnessminornonzeroevaluationdeterminanthrc)) * S ((mdr_c_nonsingular_rankwitnessminornonzeroevaluationdeterminanthrc) + (mdr_f_nonsingular_rankwitnessminornonzeroevaluationdeterminanthrc)) + ((mdr_f_nonsingular_rankwitnessminornonzeroevaluationdeterminanthrc) + (mdr_f_nonsingular_rankwitnessminornonzeroevaluationdeterminanthrc))))))))) /\ (((exists ff_h_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthrb. ff_h_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthrb + S (mdr_z_nonsingular_rankwitnessminornonzeroevaluationdeterminanthr) = S ((S (mdr_i_nonsingular_rankwitnessminornonzeroevaluationdeterminanth)) * mdr_c_nonsingular_rankwitnessminornonzeroevaluationdeterminant)) /\ exists ff_q_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthrb. mdr_b_nonsingular_rankwitnessminornonzeroevaluationdeterminant = ff_q_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthrb * S ((S (mdr_i_nonsingular_rankwitnessminornonzeroevaluationdeterminanth)) * mdr_c_nonsingular_rankwitnessminornonzeroevaluationdeterminant) + (mdr_z_nonsingular_rankwitnessminornonzeroevaluationdeterminanthr))))) /\ (((((mdr_d_nonsingular_rankwitnessminornonzeroevaluationdeterminanth) = 0) /\ (((mdr_p_nonsingular_rankwitnessminornonzeroevaluationdeterminanth) = 1) /\ ((mdr_n_nonsingular_rankwitnessminornonzeroevaluationdeterminanth) = 0))) \/ exists mdr_q_nonsingular_rankwitnessminornonzeroevaluationdeterminanths mdr_eb_nonsingular_rankwitnessminornonzeroevaluationdeterminanths mdr_ec_nonsingular_rankwitnessminornonzeroevaluationdeterminanths mdr_fb_nonsingular_rankwitnessminornonzeroevaluationdeterminanths mdr_fc_nonsingular_rankwitnessminornonzeroevaluationdeterminanths. (((mdr_d_nonsingular_rankwitnessminornonzeroevaluationdeterminanth) = S (mdr_q_nonsingular_rankwitnessminornonzeroevaluationdeterminanths)) /\ ((forall mdr_j_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsc. (exists mdr_gap_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscj. mdr_gap_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscj + S (mdr_j_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsc) = (S (mdr_q_nonsingular_rankwitnessminornonzeroevaluationdeterminanths))) -> exists mdr_i_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsc mdr_up_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsc mdr_us_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsc mdr_un_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsc mdr_ut_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsc mdr_p_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsc mdr_n_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsc. ((exists mdr_gap_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsci. mdr_gap_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsci + S (mdr_i_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsc) = (mdr_i_nonsingular_rankwitnessminornonzeroevaluationdeterminanth)) /\ ((exists mdr_z_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscr. ((exists mdr_a_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscrc mdr_b_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscrc mdr_c_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscrc mdr_e_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscrc mdr_f_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscrc. ((mdr_a_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscrc = ((mdr_q_nonsingular_rankwitnessminornonzeroevaluationdeterminanths) + (mdr_up_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsc)) * S ((mdr_q_nonsingular_rankwitnessminornonzeroevaluationdeterminanths) + (mdr_up_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsc)) + ((mdr_up_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsc) + (mdr_up_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsc))) /\ ((mdr_b_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscrc = ((mdr_us_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsc) + (mdr_un_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsc)) * S ((mdr_us_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsc) + (mdr_un_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsc)) + ((mdr_un_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsc) + (mdr_un_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsc))) /\ ((mdr_c_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscrc = ((mdr_a_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscrc) + (mdr_b_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscrc)) * S ((mdr_a_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscrc) + (mdr_b_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscrc)) + ((mdr_b_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscrc) + (mdr_b_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscrc))) /\ ((mdr_e_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscrc = ((mdr_p_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsc) + (mdr_n_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsc)) * S ((mdr_p_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsc) + (mdr_n_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsc)) + ((mdr_n_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsc) + (mdr_n_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsc))) /\ ((mdr_f_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscrc = ((mdr_ut_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsc) + (mdr_e_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscrc)) * S ((mdr_ut_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsc) + (mdr_e_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscrc)) + ((mdr_e_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscrc) + (mdr_e_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscrc))) /\ ((mdr_z_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscr) = ((mdr_c_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscrc) + (mdr_f_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscrc)) * S ((mdr_c_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscrc) + (mdr_f_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscrc)) + ((mdr_f_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscrc) + (mdr_f_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscrc))))))))) /\ (((exists ff_h_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscrb. ff_h_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscrb + S (mdr_z_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscr) = S ((S (mdr_i_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsc)) * mdr_c_nonsingular_rankwitnessminornonzeroevaluationdeterminant)) /\ exists ff_q_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscrb. mdr_b_nonsingular_rankwitnessminornonzeroevaluationdeterminant = ff_q_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscrb * S ((S (mdr_i_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsc)) * mdr_c_nonsingular_rankwitnessminornonzeroevaluationdeterminant) + (mdr_z_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscm_positive. (exists ff_gap_mdm_lt_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscm_positive_index_bound. ff_gap_mdm_lt_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscm_positive) = ((mdr_q_nonsingular_rankwitnessminornonzeroevaluationdeterminanths) * (mdr_q_nonsingular_rankwitnessminornonzeroevaluationdeterminanths))) -> exists ff_row_mdm_prefix_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscm_positive ff_column_mdm_prefix_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscm_positive ff_value_mdm_prefix_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscm_positive. (ff_index_mdm_prefix_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscm_positive = (mdr_q_nonsingular_rankwitnessminornonzeroevaluationdeterminanths) * ff_row_mdm_prefix_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscm_positive + ff_column_mdm_prefix_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscm_positive /\ ((exists ff_gap_mdm_lt_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscm_positive_column_bound. ff_gap_mdm_lt_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscm_positive) = (mdr_q_nonsingular_rankwitnessminornonzeroevaluationdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell ff_column_mdm_cell_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell = ff_row_mdm_prefix_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell_row_after. ff_gap_mdm_le_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscm_positive)) /\ ff_row_mdm_cell_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell = S ff_row_mdm_prefix_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscm_positive) = (mdr_j_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsc)) /\ ff_column_mdm_cell_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell = ff_column_mdm_prefix_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell_column_after. ff_gap_mdm_le_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell_column_after + (mdr_j_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsc) = (ff_column_mdm_prefix_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscm_positive)) /\ ff_column_mdm_cell_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell = S ff_column_mdm_prefix_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscm_positive))) /\ (((exists ff_h_mdm_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell_source. ff_h_mdm_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscm_positive) = S ((S ((ff_row_mdm_cell_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell) * (S (mdr_q_nonsingular_rankwitnessminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell))) * mdr_pc_nonsingular_rankwitnessminornonzeroevaluationdeterminanth)) /\ exists ff_q_mdm_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell_source. mdr_pb_nonsingular_rankwitnessminornonzeroevaluationdeterminanth = ff_q_mdm_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell) * (S (mdr_q_nonsingular_rankwitnessminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell))) * mdr_pc_nonsingular_rankwitnessminornonzeroevaluationdeterminanth) + (ff_value_mdm_prefix_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscm_positive)))))) /\ (((exists ff_h_mdm_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscm_positive_target. ff_h_mdm_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscm_positive_target + S (ff_value_mdm_prefix_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscm_positive) = S ((S (ff_index_mdm_prefix_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscm_positive)) * mdr_us_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsc)) /\ exists ff_q_mdm_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscm_positive_target. mdr_up_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsc = ff_q_mdm_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscm_positive)) * mdr_us_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsc) + (ff_value_mdm_prefix_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscm_negative. (exists ff_gap_mdm_lt_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscm_negative_index_bound. ff_gap_mdm_lt_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscm_negative) = ((mdr_q_nonsingular_rankwitnessminornonzeroevaluationdeterminanths) * (mdr_q_nonsingular_rankwitnessminornonzeroevaluationdeterminanths))) -> exists ff_row_mdm_prefix_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscm_negative ff_column_mdm_prefix_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscm_negative ff_value_mdm_prefix_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscm_negative. (ff_index_mdm_prefix_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscm_negative = (mdr_q_nonsingular_rankwitnessminornonzeroevaluationdeterminanths) * ff_row_mdm_prefix_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscm_negative + ff_column_mdm_prefix_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscm_negative /\ ((exists ff_gap_mdm_lt_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscm_negative_column_bound. ff_gap_mdm_lt_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscm_negative) = (mdr_q_nonsingular_rankwitnessminornonzeroevaluationdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell ff_column_mdm_cell_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell = ff_row_mdm_prefix_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell_row_after. ff_gap_mdm_le_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscm_negative)) /\ ff_row_mdm_cell_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell = S ff_row_mdm_prefix_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscm_negative) = (mdr_j_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsc)) /\ ff_column_mdm_cell_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell = ff_column_mdm_prefix_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell_column_after. ff_gap_mdm_le_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell_column_after + (mdr_j_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsc) = (ff_column_mdm_prefix_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscm_negative)) /\ ff_column_mdm_cell_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell = S ff_column_mdm_prefix_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscm_negative))) /\ (((exists ff_h_mdm_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell_source. ff_h_mdm_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscm_negative) = S ((S ((ff_row_mdm_cell_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell) * (S (mdr_q_nonsingular_rankwitnessminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell))) * mdr_nc_nonsingular_rankwitnessminornonzeroevaluationdeterminanth)) /\ exists ff_q_mdm_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell_source. mdr_nb_nonsingular_rankwitnessminornonzeroevaluationdeterminanth = ff_q_mdm_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell) * (S (mdr_q_nonsingular_rankwitnessminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell))) * mdr_nc_nonsingular_rankwitnessminornonzeroevaluationdeterminanth) + (ff_value_mdm_prefix_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscm_negative)))))) /\ (((exists ff_h_mdm_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscm_negative_target. ff_h_mdm_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscm_negative_target + S (ff_value_mdm_prefix_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscm_negative) = S ((S (ff_index_mdm_prefix_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscm_negative)) * mdr_ut_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsc)) /\ exists ff_q_mdm_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscm_negative_target. mdr_un_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsc = ff_q_mdm_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscm_negative)) * mdr_ut_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsc) + (ff_value_mdm_prefix_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscm_negative))))))))) /\ ((((exists ff_h_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscp. ff_h_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscp + S (mdr_p_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsc) = S ((S (mdr_j_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsc)) * mdr_ec_nonsingular_rankwitnessminornonzeroevaluationdeterminanths)) /\ exists ff_q_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscp. mdr_eb_nonsingular_rankwitnessminornonzeroevaluationdeterminanths = ff_q_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscp * S ((S (mdr_j_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsc)) * mdr_ec_nonsingular_rankwitnessminornonzeroevaluationdeterminanths) + (mdr_p_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsc))) /\ (((exists ff_h_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscn. ff_h_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscn + S (mdr_n_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsc) = S ((S (mdr_j_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsc)) * mdr_fc_nonsingular_rankwitnessminornonzeroevaluationdeterminanths)) /\ exists ff_q_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscn. mdr_fb_nonsingular_rankwitnessminornonzeroevaluationdeterminanths = ff_q_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthscn * S ((S (mdr_j_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsc)) * mdr_fc_nonsingular_rankwitnessminornonzeroevaluationdeterminanths) + (mdr_n_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsc)))))))) /\ (exists ff_ub_mce_fold_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf ff_uc_mce_fold_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf ff_vb_mce_fold_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf ff_vc_mce_fold_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf. ((forall ff_index_mce_alternating_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_prefix. (exists ff_gap_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_index. ff_gap_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_index + S (ff_index_mce_alternating_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) = (S (mdr_q_nonsingular_rankwitnessminornonzeroevaluationdeterminanths))) -> exists ff_ap_mce_alternating_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_prefix ff_an_mce_alternating_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_prefix ff_bp_mce_alternating_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_prefix ff_bn_mce_alternating_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_prefix ff_p_mce_alternating_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_prefix ff_n_mce_alternating_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_prefix. ((((exists ff_h_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_ap. ff_h_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_ap + S (ff_ap_mce_alternating_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_prefix)) * mdr_pc_nonsingular_rankwitnessminornonzeroevaluationdeterminanth)) /\ exists ff_q_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_ap. mdr_pb_nonsingular_rankwitnessminornonzeroevaluationdeterminanth = ff_q_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_prefix)) * mdr_pc_nonsingular_rankwitnessminornonzeroevaluationdeterminanth) + (ff_ap_mce_alternating_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_an. ff_h_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_an + S (ff_an_mce_alternating_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_prefix)) * mdr_nc_nonsingular_rankwitnessminornonzeroevaluationdeterminanth)) /\ exists ff_q_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_an. mdr_nb_nonsingular_rankwitnessminornonzeroevaluationdeterminanth = ff_q_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_prefix)) * mdr_nc_nonsingular_rankwitnessminornonzeroevaluationdeterminanth) + (ff_an_mce_alternating_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_bp. ff_h_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_bp + S (ff_bp_mce_alternating_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_prefix)) * mdr_ec_nonsingular_rankwitnessminornonzeroevaluationdeterminanths)) /\ exists ff_q_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_bp. mdr_eb_nonsingular_rankwitnessminornonzeroevaluationdeterminanths = ff_q_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_prefix)) * mdr_ec_nonsingular_rankwitnessminornonzeroevaluationdeterminanths) + (ff_bp_mce_alternating_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_bn. ff_h_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_bn + S (ff_bn_mce_alternating_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_prefix)) * mdr_fc_nonsingular_rankwitnessminornonzeroevaluationdeterminanths)) /\ exists ff_q_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_bn. mdr_fb_nonsingular_rankwitnessminornonzeroevaluationdeterminanths = ff_q_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_prefix)) * mdr_fc_nonsingular_rankwitnessminornonzeroevaluationdeterminanths) + (ff_bn_mce_alternating_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_positive. ff_h_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_positive + S (ff_p_mce_alternating_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_positive. ff_ub_mce_fold_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf) + (ff_p_mce_alternating_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_negative. ff_h_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_negative + S (ff_n_mce_alternating_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_negative. ff_vb_mce_fold_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf) + (ff_n_mce_alternating_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_prefix))) /\ (((exists ff_even_mce_term_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_prefix = 2 * ff_even_mce_term_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_term) /\ (ff_p_mce_alternating_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_prefix = 2 * ff_odd_mce_term_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_positive ff_v_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_positive. ((((exists ff_h_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_positive_start. ff_h_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_positive_start. ff_u_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_positive_start * S ((S (0)) * ff_v_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_positive_terminal. ff_h_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_positive_terminal + S (mdr_p_nonsingular_rankwitnessminornonzeroevaluationdeterminanth) = S ((S ((S (mdr_q_nonsingular_rankwitnessminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_positive_terminal. ff_u_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_positive_terminal * S ((S ((S (mdr_q_nonsingular_rankwitnessminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_positive) + (mdr_p_nonsingular_rankwitnessminornonzeroevaluationdeterminanth))) /\ forall ff_i_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_positive. (exists ff_lt_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_positive_bound. ff_lt_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_positive_bound + S ff_i_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_positive = (S (mdr_q_nonsingular_rankwitnessminornonzeroevaluationdeterminanths))) -> exists ff_a_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_positive ff_r_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_positive ff_s_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_positive. ((((exists ff_h_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_positive_summand. ff_h_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_positive_summand + S (ff_a_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_positive_summand. ff_ub_mce_fold_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_positive_summand * S ((S (ff_i_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf) + (ff_a_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_positive_partial. ff_h_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_positive_partial + S (ff_r_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_positive_partial. ff_u_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_positive_partial * S ((S (ff_i_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_positive) + (ff_r_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_positive_successor. ff_h_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_positive_successor + S (ff_s_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_positive) = S ((S (S ff_i_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_positive_successor. ff_u_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_positive_successor * S ((S (S ff_i_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_positive) + (ff_s_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_positive))) /\ ff_s_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_positive = ff_r_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_positive + ff_a_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_positive)))))) /\ (exists ff_u_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_negative ff_v_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_negative. ((((exists ff_h_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_negative_start. ff_h_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_negative_start. ff_u_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_negative_start * S ((S (0)) * ff_v_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_negative_terminal. ff_h_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_negative_terminal + S (mdr_n_nonsingular_rankwitnessminornonzeroevaluationdeterminanth) = S ((S ((S (mdr_q_nonsingular_rankwitnessminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_negative_terminal. ff_u_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_negative_terminal * S ((S ((S (mdr_q_nonsingular_rankwitnessminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_negative) + (mdr_n_nonsingular_rankwitnessminornonzeroevaluationdeterminanth))) /\ forall ff_i_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_negative. (exists ff_lt_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_negative_bound. ff_lt_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_negative_bound + S ff_i_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_negative = (S (mdr_q_nonsingular_rankwitnessminornonzeroevaluationdeterminanths))) -> exists ff_a_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_negative ff_r_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_negative ff_s_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_negative. ((((exists ff_h_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_negative_summand. ff_h_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_negative_summand + S (ff_a_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_negative_summand. ff_vb_mce_fold_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_negative_summand * S ((S (ff_i_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf) + (ff_a_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_negative_partial. ff_h_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_negative_partial + S (ff_r_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_negative_partial. ff_u_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_negative_partial * S ((S (ff_i_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_negative) + (ff_r_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_negative_successor. ff_h_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_negative_successor + S (ff_s_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_negative) = S ((S (S ff_i_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_negative_successor. ff_u_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_negative_successor * S ((S (S ff_i_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_negative) + (ff_s_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_negative))) /\ ff_s_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_negative = ff_r_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_negative + ff_a_mce_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminanthsf_negative))))))))))))))) /\ ((exists mdr_gap_nonsingular_rankwitnessminornonzeroevaluationdeterminanti. mdr_gap_nonsingular_rankwitnessminornonzeroevaluationdeterminanti + S (mdr_i_nonsingular_rankwitnessminornonzeroevaluationdeterminant) = (mdr_l_nonsingular_rankwitnessminornonzeroevaluationdeterminant)) /\ (exists mdr_z_nonsingular_rankwitnessminornonzeroevaluationdeterminantr. ((exists mdr_a_nonsingular_rankwitnessminornonzeroevaluationdeterminantrc mdr_b_nonsingular_rankwitnessminornonzeroevaluationdeterminantrc mdr_c_nonsingular_rankwitnessminornonzeroevaluationdeterminantrc mdr_e_nonsingular_rankwitnessminornonzeroevaluationdeterminantrc mdr_f_nonsingular_rankwitnessminornonzeroevaluationdeterminantrc. ((mdr_a_nonsingular_rankwitnessminornonzeroevaluationdeterminantrc = ((d) + (mdr_ub_nonsingular_rankwitnessminornonzeroevaluation)) * S ((d) + (mdr_ub_nonsingular_rankwitnessminornonzeroevaluation)) + ((mdr_ub_nonsingular_rankwitnessminornonzeroevaluation) + (mdr_ub_nonsingular_rankwitnessminornonzeroevaluation))) /\ ((mdr_b_nonsingular_rankwitnessminornonzeroevaluationdeterminantrc = ((mdr_uc_nonsingular_rankwitnessminornonzeroevaluation) + (mdr_vb_nonsingular_rankwitnessminornonzeroevaluation)) * S ((mdr_uc_nonsingular_rankwitnessminornonzeroevaluation) + (mdr_vb_nonsingular_rankwitnessminornonzeroevaluation)) + ((mdr_vb_nonsingular_rankwitnessminornonzeroevaluation) + (mdr_vb_nonsingular_rankwitnessminornonzeroevaluation))) /\ ((mdr_c_nonsingular_rankwitnessminornonzeroevaluationdeterminantrc = ((mdr_a_nonsingular_rankwitnessminornonzeroevaluationdeterminantrc) + (mdr_b_nonsingular_rankwitnessminornonzeroevaluationdeterminantrc)) * S ((mdr_a_nonsingular_rankwitnessminornonzeroevaluationdeterminantrc) + (mdr_b_nonsingular_rankwitnessminornonzeroevaluationdeterminantrc)) + ((mdr_b_nonsingular_rankwitnessminornonzeroevaluationdeterminantrc) + (mdr_b_nonsingular_rankwitnessminornonzeroevaluationdeterminantrc))) /\ ((mdr_e_nonsingular_rankwitnessminornonzeroevaluationdeterminantrc = ((mdr_p_nonsingular_rankwitnessminornonzero) + (mdr_n_nonsingular_rankwitnessminornonzero)) * S ((mdr_p_nonsingular_rankwitnessminornonzero) + (mdr_n_nonsingular_rankwitnessminornonzero)) + ((mdr_n_nonsingular_rankwitnessminornonzero) + (mdr_n_nonsingular_rankwitnessminornonzero))) /\ ((mdr_f_nonsingular_rankwitnessminornonzeroevaluationdeterminantrc = ((mdr_vc_nonsingular_rankwitnessminornonzeroevaluation) + (mdr_e_nonsingular_rankwitnessminornonzeroevaluationdeterminantrc)) * S ((mdr_vc_nonsingular_rankwitnessminornonzeroevaluation) + (mdr_e_nonsingular_rankwitnessminornonzeroevaluationdeterminantrc)) + ((mdr_e_nonsingular_rankwitnessminornonzeroevaluationdeterminantrc) + (mdr_e_nonsingular_rankwitnessminornonzeroevaluationdeterminantrc))) /\ ((mdr_z_nonsingular_rankwitnessminornonzeroevaluationdeterminantr) = ((mdr_c_nonsingular_rankwitnessminornonzeroevaluationdeterminantrc) + (mdr_f_nonsingular_rankwitnessminornonzeroevaluationdeterminantrc)) * S ((mdr_c_nonsingular_rankwitnessminornonzeroevaluationdeterminantrc) + (mdr_f_nonsingular_rankwitnessminornonzeroevaluationdeterminantrc)) + ((mdr_f_nonsingular_rankwitnessminornonzeroevaluationdeterminantrc) + (mdr_f_nonsingular_rankwitnessminornonzeroevaluationdeterminantrc))))))))) /\ (((exists ff_h_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminantrb. ff_h_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminantrb + S (mdr_z_nonsingular_rankwitnessminornonzeroevaluationdeterminantr) = S ((S (mdr_i_nonsingular_rankwitnessminornonzeroevaluationdeterminant)) * mdr_c_nonsingular_rankwitnessminornonzeroevaluationdeterminant)) /\ exists ff_q_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminantrb. mdr_b_nonsingular_rankwitnessminornonzeroevaluationdeterminant = ff_q_mdr_nonsingular_rankwitnessminornonzeroevaluationdeterminantrb * S ((S (mdr_i_nonsingular_rankwitnessminornonzeroevaluationdeterminant)) * mdr_c_nonsingular_rankwitnessminornonzeroevaluationdeterminant) + (mdr_z_nonsingular_rankwitnessminornonzeroevaluationdeterminantr)))))))))) /\ (~(mdr_p_nonsingular_rankwitnessminornonzero = mdr_n_nonsingular_rankwitnessminornonzero)))))))) /\ (forall mdr_q_nonsingular_rank. (exists mdr_gap_nonsingular_rankhigher. mdr_gap_nonsingular_rankhigher + S (d) = (mdr_q_nonsingular_rank)) -> (forall mdr_rb_nonsingular_rankzero mdr_rc_nonsingular_rankzero mdr_cb_nonsingular_rankzero mdr_cc_nonsingular_rankzero mdr_p_nonsingular_rankzero mdr_n_nonsingular_rankzero. (((forall fom_index_mrf_nonsingular_rankzerorowsbound. (exists fom_gap_mrf_nonsingular_rankzerorowsbound_index_bound. fom_gap_mrf_nonsingular_rankzerorowsbound_index_bound + S (fom_index_mrf_nonsingular_rankzerorowsbound) = mdr_q_nonsingular_rank) -> exists fom_value_mrf_nonsingular_rankzerorowsbound. ((((exists fom_beta_height_mrf_nonsingular_rankzerorowsbound_entry. fom_beta_height_mrf_nonsingular_rankzerorowsbound_entry + S (fom_value_mrf_nonsingular_rankzerorowsbound) = S ((S (fom_index_mrf_nonsingular_rankzerorowsbound)) * mdr_rc_nonsingular_rankzero)) /\ exists fom_beta_quotient_mrf_nonsingular_rankzerorowsbound_entry. mdr_rb_nonsingular_rankzero = fom_beta_quotient_mrf_nonsingular_rankzerorowsbound_entry * S ((S (fom_index_mrf_nonsingular_rankzerorowsbound)) * mdr_rc_nonsingular_rankzero) + (fom_value_mrf_nonsingular_rankzerorowsbound))) /\ (exists fom_gap_mrf_nonsingular_rankzerorowsbound_value_bound. fom_gap_mrf_nonsingular_rankzerorowsbound_value_bound + S (fom_value_mrf_nonsingular_rankzerorowsbound) = d))) /\ (forall mdr_i_nonsingular_rankzerorowsdistinct mdr_j_nonsingular_rankzerorowsdistinct mdr_a_nonsingular_rankzerorowsdistinct. (exists mdr_gap_nonsingular_rankzerorowsdistincti. mdr_gap_nonsingular_rankzerorowsdistincti + S (mdr_i_nonsingular_rankzerorowsdistinct) = (mdr_q_nonsingular_rank)) -> (exists mdr_gap_nonsingular_rankzerorowsdistinctj. mdr_gap_nonsingular_rankzerorowsdistinctj + S (mdr_j_nonsingular_rankzerorowsdistinct) = (mdr_q_nonsingular_rank)) -> (((exists ff_h_mdr_nonsingular_rankzerorowsdistinctfirst. ff_h_mdr_nonsingular_rankzerorowsdistinctfirst + S (mdr_a_nonsingular_rankzerorowsdistinct) = S ((S (mdr_i_nonsingular_rankzerorowsdistinct)) * mdr_rc_nonsingular_rankzero)) /\ exists ff_q_mdr_nonsingular_rankzerorowsdistinctfirst. mdr_rb_nonsingular_rankzero = ff_q_mdr_nonsingular_rankzerorowsdistinctfirst * S ((S (mdr_i_nonsingular_rankzerorowsdistinct)) * mdr_rc_nonsingular_rankzero) + (mdr_a_nonsingular_rankzerorowsdistinct))) -> (((exists ff_h_mdr_nonsingular_rankzerorowsdistinctsecond. ff_h_mdr_nonsingular_rankzerorowsdistinctsecond + S (mdr_a_nonsingular_rankzerorowsdistinct) = S ((S (mdr_j_nonsingular_rankzerorowsdistinct)) * mdr_rc_nonsingular_rankzero)) /\ exists ff_q_mdr_nonsingular_rankzerorowsdistinctsecond. mdr_rb_nonsingular_rankzero = ff_q_mdr_nonsingular_rankzerorowsdistinctsecond * S ((S (mdr_j_nonsingular_rankzerorowsdistinct)) * mdr_rc_nonsingular_rankzero) + (mdr_a_nonsingular_rankzerorowsdistinct))) -> mdr_i_nonsingular_rankzerorowsdistinct = mdr_j_nonsingular_rankzerorowsdistinct))) -> (((forall fom_index_mrf_nonsingular_rankzerocolumnsbound. (exists fom_gap_mrf_nonsingular_rankzerocolumnsbound_index_bound. fom_gap_mrf_nonsingular_rankzerocolumnsbound_index_bound + S (fom_index_mrf_nonsingular_rankzerocolumnsbound) = mdr_q_nonsingular_rank) -> exists fom_value_mrf_nonsingular_rankzerocolumnsbound. ((((exists fom_beta_height_mrf_nonsingular_rankzerocolumnsbound_entry. fom_beta_height_mrf_nonsingular_rankzerocolumnsbound_entry + S (fom_value_mrf_nonsingular_rankzerocolumnsbound) = S ((S (fom_index_mrf_nonsingular_rankzerocolumnsbound)) * mdr_cc_nonsingular_rankzero)) /\ exists fom_beta_quotient_mrf_nonsingular_rankzerocolumnsbound_entry. mdr_cb_nonsingular_rankzero = fom_beta_quotient_mrf_nonsingular_rankzerocolumnsbound_entry * S ((S (fom_index_mrf_nonsingular_rankzerocolumnsbound)) * mdr_cc_nonsingular_rankzero) + (fom_value_mrf_nonsingular_rankzerocolumnsbound))) /\ (exists fom_gap_mrf_nonsingular_rankzerocolumnsbound_value_bound. fom_gap_mrf_nonsingular_rankzerocolumnsbound_value_bound + S (fom_value_mrf_nonsingular_rankzerocolumnsbound) = d))) /\ (forall mdr_i_nonsingular_rankzerocolumnsdistinct mdr_j_nonsingular_rankzerocolumnsdistinct mdr_a_nonsingular_rankzerocolumnsdistinct. (exists mdr_gap_nonsingular_rankzerocolumnsdistincti. mdr_gap_nonsingular_rankzerocolumnsdistincti + S (mdr_i_nonsingular_rankzerocolumnsdistinct) = (mdr_q_nonsingular_rank)) -> (exists mdr_gap_nonsingular_rankzerocolumnsdistinctj. mdr_gap_nonsingular_rankzerocolumnsdistinctj + S (mdr_j_nonsingular_rankzerocolumnsdistinct) = (mdr_q_nonsingular_rank)) -> (((exists ff_h_mdr_nonsingular_rankzerocolumnsdistinctfirst. ff_h_mdr_nonsingular_rankzerocolumnsdistinctfirst + S (mdr_a_nonsingular_rankzerocolumnsdistinct) = S ((S (mdr_i_nonsingular_rankzerocolumnsdistinct)) * mdr_cc_nonsingular_rankzero)) /\ exists ff_q_mdr_nonsingular_rankzerocolumnsdistinctfirst. mdr_cb_nonsingular_rankzero = ff_q_mdr_nonsingular_rankzerocolumnsdistinctfirst * S ((S (mdr_i_nonsingular_rankzerocolumnsdistinct)) * mdr_cc_nonsingular_rankzero) + (mdr_a_nonsingular_rankzerocolumnsdistinct))) -> (((exists ff_h_mdr_nonsingular_rankzerocolumnsdistinctsecond. ff_h_mdr_nonsingular_rankzerocolumnsdistinctsecond + S (mdr_a_nonsingular_rankzerocolumnsdistinct) = S ((S (mdr_j_nonsingular_rankzerocolumnsdistinct)) * mdr_cc_nonsingular_rankzero)) /\ exists ff_q_mdr_nonsingular_rankzerocolumnsdistinctsecond. mdr_cb_nonsingular_rankzero = ff_q_mdr_nonsingular_rankzerocolumnsdistinctsecond * S ((S (mdr_j_nonsingular_rankzerocolumnsdistinct)) * mdr_cc_nonsingular_rankzero) + (mdr_a_nonsingular_rankzerocolumnsdistinct))) -> mdr_i_nonsingular_rankzerocolumnsdistinct = mdr_j_nonsingular_rankzerocolumnsdistinct))) -> (exists mdr_ub_nonsingular_rankzeroevaluation mdr_uc_nonsingular_rankzeroevaluation mdr_vb_nonsingular_rankzeroevaluation mdr_vc_nonsingular_rankzeroevaluation. ((((forall mdr_i_nonsingular_rankzeroevaluationmatrixpositive. (exists mdr_gap_nonsingular_rankzeroevaluationmatrixpositivebound. mdr_gap_nonsingular_rankzeroevaluationmatrixpositivebound + S (mdr_i_nonsingular_rankzeroevaluationmatrixpositive) = ((mdr_q_nonsingular_rank) * (mdr_q_nonsingular_rank))) -> exists mdr_a_nonsingular_rankzeroevaluationmatrixpositive. (((exists mdr_r_nonsingular_rankzeroevaluationmatrixpositivepoint mdr_s_nonsingular_rankzeroevaluationmatrixpositivepoint mdr_u_nonsingular_rankzeroevaluationmatrixpositivepoint mdr_v_nonsingular_rankzeroevaluationmatrixpositivepoint. ((mdr_i_nonsingular_rankzeroevaluationmatrixpositive = (mdr_q_nonsingular_rank) * mdr_r_nonsingular_rankzeroevaluationmatrixpositivepoint + mdr_s_nonsingular_rankzeroevaluationmatrixpositivepoint) /\ ((exists mdr_gap_nonsingular_rankzeroevaluationmatrixpositivepointcolumn. mdr_gap_nonsingular_rankzeroevaluationmatrixpositivepointcolumn + S (mdr_s_nonsingular_rankzeroevaluationmatrixpositivepoint) = (mdr_q_nonsingular_rank)) /\ ((((exists ff_h_mdr_nonsingular_rankzeroevaluationmatrixpositivepointrow_index. ff_h_mdr_nonsingular_rankzeroevaluationmatrixpositivepointrow_index + S (mdr_u_nonsingular_rankzeroevaluationmatrixpositivepoint) = S ((S (mdr_r_nonsingular_rankzeroevaluationmatrixpositivepoint)) * mdr_rc_nonsingular_rankzero)) /\ exists ff_q_mdr_nonsingular_rankzeroevaluationmatrixpositivepointrow_index. mdr_rb_nonsingular_rankzero = ff_q_mdr_nonsingular_rankzeroevaluationmatrixpositivepointrow_index * S ((S (mdr_r_nonsingular_rankzeroevaluationmatrixpositivepoint)) * mdr_rc_nonsingular_rankzero) + (mdr_u_nonsingular_rankzeroevaluationmatrixpositivepoint))) /\ ((((exists ff_h_mdr_nonsingular_rankzeroevaluationmatrixpositivepointcolumn_index. ff_h_mdr_nonsingular_rankzeroevaluationmatrixpositivepointcolumn_index + S (mdr_v_nonsingular_rankzeroevaluationmatrixpositivepoint) = S ((S (mdr_s_nonsingular_rankzeroevaluationmatrixpositivepoint)) * mdr_cc_nonsingular_rankzero)) /\ exists ff_q_mdr_nonsingular_rankzeroevaluationmatrixpositivepointcolumn_index. mdr_cb_nonsingular_rankzero = ff_q_mdr_nonsingular_rankzeroevaluationmatrixpositivepointcolumn_index * S ((S (mdr_s_nonsingular_rankzeroevaluationmatrixpositivepoint)) * mdr_cc_nonsingular_rankzero) + (mdr_v_nonsingular_rankzeroevaluationmatrixpositivepoint))) /\ (((exists ff_h_mdr_nonsingular_rankzeroevaluationmatrixpositivepointsource. ff_h_mdr_nonsingular_rankzeroevaluationmatrixpositivepointsource + S (mdr_a_nonsingular_rankzeroevaluationmatrixpositive) = S ((S ((mdr_u_nonsingular_rankzeroevaluationmatrixpositivepoint) * (d) + (mdr_v_nonsingular_rankzeroevaluationmatrixpositivepoint))) * ac)) /\ exists ff_q_mdr_nonsingular_rankzeroevaluationmatrixpositivepointsource. ab = ff_q_mdr_nonsingular_rankzeroevaluationmatrixpositivepointsource * S ((S ((mdr_u_nonsingular_rankzeroevaluationmatrixpositivepoint) * (d) + (mdr_v_nonsingular_rankzeroevaluationmatrixpositivepoint))) * ac) + (mdr_a_nonsingular_rankzeroevaluationmatrixpositive)))))))) /\ (((exists ff_h_mdr_nonsingular_rankzeroevaluationmatrixpositiveoutput. ff_h_mdr_nonsingular_rankzeroevaluationmatrixpositiveoutput + S (mdr_a_nonsingular_rankzeroevaluationmatrixpositive) = S ((S (mdr_i_nonsingular_rankzeroevaluationmatrixpositive)) * mdr_uc_nonsingular_rankzeroevaluation)) /\ exists ff_q_mdr_nonsingular_rankzeroevaluationmatrixpositiveoutput. mdr_ub_nonsingular_rankzeroevaluation = ff_q_mdr_nonsingular_rankzeroevaluationmatrixpositiveoutput * S ((S (mdr_i_nonsingular_rankzeroevaluationmatrixpositive)) * mdr_uc_nonsingular_rankzeroevaluation) + (mdr_a_nonsingular_rankzeroevaluationmatrixpositive)))))) /\ (forall mdr_i_nonsingular_rankzeroevaluationmatrixnegative. (exists mdr_gap_nonsingular_rankzeroevaluationmatrixnegativebound. mdr_gap_nonsingular_rankzeroevaluationmatrixnegativebound + S (mdr_i_nonsingular_rankzeroevaluationmatrixnegative) = ((mdr_q_nonsingular_rank) * (mdr_q_nonsingular_rank))) -> exists mdr_a_nonsingular_rankzeroevaluationmatrixnegative. (((exists mdr_r_nonsingular_rankzeroevaluationmatrixnegativepoint mdr_s_nonsingular_rankzeroevaluationmatrixnegativepoint mdr_u_nonsingular_rankzeroevaluationmatrixnegativepoint mdr_v_nonsingular_rankzeroevaluationmatrixnegativepoint. ((mdr_i_nonsingular_rankzeroevaluationmatrixnegative = (mdr_q_nonsingular_rank) * mdr_r_nonsingular_rankzeroevaluationmatrixnegativepoint + mdr_s_nonsingular_rankzeroevaluationmatrixnegativepoint) /\ ((exists mdr_gap_nonsingular_rankzeroevaluationmatrixnegativepointcolumn. mdr_gap_nonsingular_rankzeroevaluationmatrixnegativepointcolumn + S (mdr_s_nonsingular_rankzeroevaluationmatrixnegativepoint) = (mdr_q_nonsingular_rank)) /\ ((((exists ff_h_mdr_nonsingular_rankzeroevaluationmatrixnegativepointrow_index. ff_h_mdr_nonsingular_rankzeroevaluationmatrixnegativepointrow_index + S (mdr_u_nonsingular_rankzeroevaluationmatrixnegativepoint) = S ((S (mdr_r_nonsingular_rankzeroevaluationmatrixnegativepoint)) * mdr_rc_nonsingular_rankzero)) /\ exists ff_q_mdr_nonsingular_rankzeroevaluationmatrixnegativepointrow_index. mdr_rb_nonsingular_rankzero = ff_q_mdr_nonsingular_rankzeroevaluationmatrixnegativepointrow_index * S ((S (mdr_r_nonsingular_rankzeroevaluationmatrixnegativepoint)) * mdr_rc_nonsingular_rankzero) + (mdr_u_nonsingular_rankzeroevaluationmatrixnegativepoint))) /\ ((((exists ff_h_mdr_nonsingular_rankzeroevaluationmatrixnegativepointcolumn_index. ff_h_mdr_nonsingular_rankzeroevaluationmatrixnegativepointcolumn_index + S (mdr_v_nonsingular_rankzeroevaluationmatrixnegativepoint) = S ((S (mdr_s_nonsingular_rankzeroevaluationmatrixnegativepoint)) * mdr_cc_nonsingular_rankzero)) /\ exists ff_q_mdr_nonsingular_rankzeroevaluationmatrixnegativepointcolumn_index. mdr_cb_nonsingular_rankzero = ff_q_mdr_nonsingular_rankzeroevaluationmatrixnegativepointcolumn_index * S ((S (mdr_s_nonsingular_rankzeroevaluationmatrixnegativepoint)) * mdr_cc_nonsingular_rankzero) + (mdr_v_nonsingular_rankzeroevaluationmatrixnegativepoint))) /\ (((exists ff_h_mdr_nonsingular_rankzeroevaluationmatrixnegativepointsource. ff_h_mdr_nonsingular_rankzeroevaluationmatrixnegativepointsource + S (mdr_a_nonsingular_rankzeroevaluationmatrixnegative) = S ((S ((mdr_u_nonsingular_rankzeroevaluationmatrixnegativepoint) * (d) + (mdr_v_nonsingular_rankzeroevaluationmatrixnegativepoint))) * bc)) /\ exists ff_q_mdr_nonsingular_rankzeroevaluationmatrixnegativepointsource. bb = ff_q_mdr_nonsingular_rankzeroevaluationmatrixnegativepointsource * S ((S ((mdr_u_nonsingular_rankzeroevaluationmatrixnegativepoint) * (d) + (mdr_v_nonsingular_rankzeroevaluationmatrixnegativepoint))) * bc) + (mdr_a_nonsingular_rankzeroevaluationmatrixnegative)))))))) /\ (((exists ff_h_mdr_nonsingular_rankzeroevaluationmatrixnegativeoutput. ff_h_mdr_nonsingular_rankzeroevaluationmatrixnegativeoutput + S (mdr_a_nonsingular_rankzeroevaluationmatrixnegative) = S ((S (mdr_i_nonsingular_rankzeroevaluationmatrixnegative)) * mdr_vc_nonsingular_rankzeroevaluation)) /\ exists ff_q_mdr_nonsingular_rankzeroevaluationmatrixnegativeoutput. mdr_vb_nonsingular_rankzeroevaluation = ff_q_mdr_nonsingular_rankzeroevaluationmatrixnegativeoutput * S ((S (mdr_i_nonsingular_rankzeroevaluationmatrixnegative)) * mdr_vc_nonsingular_rankzeroevaluation) + (mdr_a_nonsingular_rankzeroevaluationmatrixnegative)))))))) /\ (exists mdr_b_nonsingular_rankzeroevaluationdeterminant mdr_c_nonsingular_rankzeroevaluationdeterminant mdr_l_nonsingular_rankzeroevaluationdeterminant mdr_i_nonsingular_rankzeroevaluationdeterminant. ((forall mdr_i_nonsingular_rankzeroevaluationdeterminanth. (exists mdr_gap_nonsingular_rankzeroevaluationdeterminanthi. mdr_gap_nonsingular_rankzeroevaluationdeterminanthi + S (mdr_i_nonsingular_rankzeroevaluationdeterminanth) = (mdr_l_nonsingular_rankzeroevaluationdeterminant)) -> exists mdr_d_nonsingular_rankzeroevaluationdeterminanth mdr_pb_nonsingular_rankzeroevaluationdeterminanth mdr_pc_nonsingular_rankzeroevaluationdeterminanth mdr_nb_nonsingular_rankzeroevaluationdeterminanth mdr_nc_nonsingular_rankzeroevaluationdeterminanth mdr_p_nonsingular_rankzeroevaluationdeterminanth mdr_n_nonsingular_rankzeroevaluationdeterminanth. ((exists mdr_z_nonsingular_rankzeroevaluationdeterminanthr. ((exists mdr_a_nonsingular_rankzeroevaluationdeterminanthrc mdr_b_nonsingular_rankzeroevaluationdeterminanthrc mdr_c_nonsingular_rankzeroevaluationdeterminanthrc mdr_e_nonsingular_rankzeroevaluationdeterminanthrc mdr_f_nonsingular_rankzeroevaluationdeterminanthrc. ((mdr_a_nonsingular_rankzeroevaluationdeterminanthrc = ((mdr_d_nonsingular_rankzeroevaluationdeterminanth) + (mdr_pb_nonsingular_rankzeroevaluationdeterminanth)) * S ((mdr_d_nonsingular_rankzeroevaluationdeterminanth) + (mdr_pb_nonsingular_rankzeroevaluationdeterminanth)) + ((mdr_pb_nonsingular_rankzeroevaluationdeterminanth) + (mdr_pb_nonsingular_rankzeroevaluationdeterminanth))) /\ ((mdr_b_nonsingular_rankzeroevaluationdeterminanthrc = ((mdr_pc_nonsingular_rankzeroevaluationdeterminanth) + (mdr_nb_nonsingular_rankzeroevaluationdeterminanth)) * S ((mdr_pc_nonsingular_rankzeroevaluationdeterminanth) + (mdr_nb_nonsingular_rankzeroevaluationdeterminanth)) + ((mdr_nb_nonsingular_rankzeroevaluationdeterminanth) + (mdr_nb_nonsingular_rankzeroevaluationdeterminanth))) /\ ((mdr_c_nonsingular_rankzeroevaluationdeterminanthrc = ((mdr_a_nonsingular_rankzeroevaluationdeterminanthrc) + (mdr_b_nonsingular_rankzeroevaluationdeterminanthrc)) * S ((mdr_a_nonsingular_rankzeroevaluationdeterminanthrc) + (mdr_b_nonsingular_rankzeroevaluationdeterminanthrc)) + ((mdr_b_nonsingular_rankzeroevaluationdeterminanthrc) + (mdr_b_nonsingular_rankzeroevaluationdeterminanthrc))) /\ ((mdr_e_nonsingular_rankzeroevaluationdeterminanthrc = ((mdr_p_nonsingular_rankzeroevaluationdeterminanth) + (mdr_n_nonsingular_rankzeroevaluationdeterminanth)) * S ((mdr_p_nonsingular_rankzeroevaluationdeterminanth) + (mdr_n_nonsingular_rankzeroevaluationdeterminanth)) + ((mdr_n_nonsingular_rankzeroevaluationdeterminanth) + (mdr_n_nonsingular_rankzeroevaluationdeterminanth))) /\ ((mdr_f_nonsingular_rankzeroevaluationdeterminanthrc = ((mdr_nc_nonsingular_rankzeroevaluationdeterminanth) + (mdr_e_nonsingular_rankzeroevaluationdeterminanthrc)) * S ((mdr_nc_nonsingular_rankzeroevaluationdeterminanth) + (mdr_e_nonsingular_rankzeroevaluationdeterminanthrc)) + ((mdr_e_nonsingular_rankzeroevaluationdeterminanthrc) + (mdr_e_nonsingular_rankzeroevaluationdeterminanthrc))) /\ ((mdr_z_nonsingular_rankzeroevaluationdeterminanthr) = ((mdr_c_nonsingular_rankzeroevaluationdeterminanthrc) + (mdr_f_nonsingular_rankzeroevaluationdeterminanthrc)) * S ((mdr_c_nonsingular_rankzeroevaluationdeterminanthrc) + (mdr_f_nonsingular_rankzeroevaluationdeterminanthrc)) + ((mdr_f_nonsingular_rankzeroevaluationdeterminanthrc) + (mdr_f_nonsingular_rankzeroevaluationdeterminanthrc))))))))) /\ (((exists ff_h_mdr_nonsingular_rankzeroevaluationdeterminanthrb. ff_h_mdr_nonsingular_rankzeroevaluationdeterminanthrb + S (mdr_z_nonsingular_rankzeroevaluationdeterminanthr) = S ((S (mdr_i_nonsingular_rankzeroevaluationdeterminanth)) * mdr_c_nonsingular_rankzeroevaluationdeterminant)) /\ exists ff_q_mdr_nonsingular_rankzeroevaluationdeterminanthrb. mdr_b_nonsingular_rankzeroevaluationdeterminant = ff_q_mdr_nonsingular_rankzeroevaluationdeterminanthrb * S ((S (mdr_i_nonsingular_rankzeroevaluationdeterminanth)) * mdr_c_nonsingular_rankzeroevaluationdeterminant) + (mdr_z_nonsingular_rankzeroevaluationdeterminanthr))))) /\ (((((mdr_d_nonsingular_rankzeroevaluationdeterminanth) = 0) /\ (((mdr_p_nonsingular_rankzeroevaluationdeterminanth) = 1) /\ ((mdr_n_nonsingular_rankzeroevaluationdeterminanth) = 0))) \/ exists mdr_q_nonsingular_rankzeroevaluationdeterminanths mdr_eb_nonsingular_rankzeroevaluationdeterminanths mdr_ec_nonsingular_rankzeroevaluationdeterminanths mdr_fb_nonsingular_rankzeroevaluationdeterminanths mdr_fc_nonsingular_rankzeroevaluationdeterminanths. (((mdr_d_nonsingular_rankzeroevaluationdeterminanth) = S (mdr_q_nonsingular_rankzeroevaluationdeterminanths)) /\ ((forall mdr_j_nonsingular_rankzeroevaluationdeterminanthsc. (exists mdr_gap_nonsingular_rankzeroevaluationdeterminanthscj. mdr_gap_nonsingular_rankzeroevaluationdeterminanthscj + S (mdr_j_nonsingular_rankzeroevaluationdeterminanthsc) = (S (mdr_q_nonsingular_rankzeroevaluationdeterminanths))) -> exists mdr_i_nonsingular_rankzeroevaluationdeterminanthsc mdr_up_nonsingular_rankzeroevaluationdeterminanthsc mdr_us_nonsingular_rankzeroevaluationdeterminanthsc mdr_un_nonsingular_rankzeroevaluationdeterminanthsc mdr_ut_nonsingular_rankzeroevaluationdeterminanthsc mdr_p_nonsingular_rankzeroevaluationdeterminanthsc mdr_n_nonsingular_rankzeroevaluationdeterminanthsc. ((exists mdr_gap_nonsingular_rankzeroevaluationdeterminanthsci. mdr_gap_nonsingular_rankzeroevaluationdeterminanthsci + S (mdr_i_nonsingular_rankzeroevaluationdeterminanthsc) = (mdr_i_nonsingular_rankzeroevaluationdeterminanth)) /\ ((exists mdr_z_nonsingular_rankzeroevaluationdeterminanthscr. ((exists mdr_a_nonsingular_rankzeroevaluationdeterminanthscrc mdr_b_nonsingular_rankzeroevaluationdeterminanthscrc mdr_c_nonsingular_rankzeroevaluationdeterminanthscrc mdr_e_nonsingular_rankzeroevaluationdeterminanthscrc mdr_f_nonsingular_rankzeroevaluationdeterminanthscrc. ((mdr_a_nonsingular_rankzeroevaluationdeterminanthscrc = ((mdr_q_nonsingular_rankzeroevaluationdeterminanths) + (mdr_up_nonsingular_rankzeroevaluationdeterminanthsc)) * S ((mdr_q_nonsingular_rankzeroevaluationdeterminanths) + (mdr_up_nonsingular_rankzeroevaluationdeterminanthsc)) + ((mdr_up_nonsingular_rankzeroevaluationdeterminanthsc) + (mdr_up_nonsingular_rankzeroevaluationdeterminanthsc))) /\ ((mdr_b_nonsingular_rankzeroevaluationdeterminanthscrc = ((mdr_us_nonsingular_rankzeroevaluationdeterminanthsc) + (mdr_un_nonsingular_rankzeroevaluationdeterminanthsc)) * S ((mdr_us_nonsingular_rankzeroevaluationdeterminanthsc) + (mdr_un_nonsingular_rankzeroevaluationdeterminanthsc)) + ((mdr_un_nonsingular_rankzeroevaluationdeterminanthsc) + (mdr_un_nonsingular_rankzeroevaluationdeterminanthsc))) /\ ((mdr_c_nonsingular_rankzeroevaluationdeterminanthscrc = ((mdr_a_nonsingular_rankzeroevaluationdeterminanthscrc) + (mdr_b_nonsingular_rankzeroevaluationdeterminanthscrc)) * S ((mdr_a_nonsingular_rankzeroevaluationdeterminanthscrc) + (mdr_b_nonsingular_rankzeroevaluationdeterminanthscrc)) + ((mdr_b_nonsingular_rankzeroevaluationdeterminanthscrc) + (mdr_b_nonsingular_rankzeroevaluationdeterminanthscrc))) /\ ((mdr_e_nonsingular_rankzeroevaluationdeterminanthscrc = ((mdr_p_nonsingular_rankzeroevaluationdeterminanthsc) + (mdr_n_nonsingular_rankzeroevaluationdeterminanthsc)) * S ((mdr_p_nonsingular_rankzeroevaluationdeterminanthsc) + (mdr_n_nonsingular_rankzeroevaluationdeterminanthsc)) + ((mdr_n_nonsingular_rankzeroevaluationdeterminanthsc) + (mdr_n_nonsingular_rankzeroevaluationdeterminanthsc))) /\ ((mdr_f_nonsingular_rankzeroevaluationdeterminanthscrc = ((mdr_ut_nonsingular_rankzeroevaluationdeterminanthsc) + (mdr_e_nonsingular_rankzeroevaluationdeterminanthscrc)) * S ((mdr_ut_nonsingular_rankzeroevaluationdeterminanthsc) + (mdr_e_nonsingular_rankzeroevaluationdeterminanthscrc)) + ((mdr_e_nonsingular_rankzeroevaluationdeterminanthscrc) + (mdr_e_nonsingular_rankzeroevaluationdeterminanthscrc))) /\ ((mdr_z_nonsingular_rankzeroevaluationdeterminanthscr) = ((mdr_c_nonsingular_rankzeroevaluationdeterminanthscrc) + (mdr_f_nonsingular_rankzeroevaluationdeterminanthscrc)) * S ((mdr_c_nonsingular_rankzeroevaluationdeterminanthscrc) + (mdr_f_nonsingular_rankzeroevaluationdeterminanthscrc)) + ((mdr_f_nonsingular_rankzeroevaluationdeterminanthscrc) + (mdr_f_nonsingular_rankzeroevaluationdeterminanthscrc))))))))) /\ (((exists ff_h_mdr_nonsingular_rankzeroevaluationdeterminanthscrb. ff_h_mdr_nonsingular_rankzeroevaluationdeterminanthscrb + S (mdr_z_nonsingular_rankzeroevaluationdeterminanthscr) = S ((S (mdr_i_nonsingular_rankzeroevaluationdeterminanthsc)) * mdr_c_nonsingular_rankzeroevaluationdeterminant)) /\ exists ff_q_mdr_nonsingular_rankzeroevaluationdeterminanthscrb. mdr_b_nonsingular_rankzeroevaluationdeterminant = ff_q_mdr_nonsingular_rankzeroevaluationdeterminanthscrb * S ((S (mdr_i_nonsingular_rankzeroevaluationdeterminanthsc)) * mdr_c_nonsingular_rankzeroevaluationdeterminant) + (mdr_z_nonsingular_rankzeroevaluationdeterminanthscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_nonsingular_rankzeroevaluationdeterminanthscm_positive. (exists ff_gap_mdm_lt_mdr_nonsingular_rankzeroevaluationdeterminanthscm_positive_index_bound. ff_gap_mdm_lt_mdr_nonsingular_rankzeroevaluationdeterminanthscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_nonsingular_rankzeroevaluationdeterminanthscm_positive) = ((mdr_q_nonsingular_rankzeroevaluationdeterminanths) * (mdr_q_nonsingular_rankzeroevaluationdeterminanths))) -> exists ff_row_mdm_prefix_mdr_nonsingular_rankzeroevaluationdeterminanthscm_positive ff_column_mdm_prefix_mdr_nonsingular_rankzeroevaluationdeterminanthscm_positive ff_value_mdm_prefix_mdr_nonsingular_rankzeroevaluationdeterminanthscm_positive. (ff_index_mdm_prefix_mdr_nonsingular_rankzeroevaluationdeterminanthscm_positive = (mdr_q_nonsingular_rankzeroevaluationdeterminanths) * ff_row_mdm_prefix_mdr_nonsingular_rankzeroevaluationdeterminanthscm_positive + ff_column_mdm_prefix_mdr_nonsingular_rankzeroevaluationdeterminanthscm_positive /\ ((exists ff_gap_mdm_lt_mdr_nonsingular_rankzeroevaluationdeterminanthscm_positive_column_bound. ff_gap_mdm_lt_mdr_nonsingular_rankzeroevaluationdeterminanthscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_nonsingular_rankzeroevaluationdeterminanthscm_positive) = (mdr_q_nonsingular_rankzeroevaluationdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_nonsingular_rankzeroevaluationdeterminanthscm_positive_cell ff_column_mdm_cell_mdr_nonsingular_rankzeroevaluationdeterminanthscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_nonsingular_rankzeroevaluationdeterminanthscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_nonsingular_rankzeroevaluationdeterminanthscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_nonsingular_rankzeroevaluationdeterminanthscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_nonsingular_rankzeroevaluationdeterminanthscm_positive_cell = ff_row_mdm_prefix_mdr_nonsingular_rankzeroevaluationdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_nonsingular_rankzeroevaluationdeterminanthscm_positive_cell_row_after. ff_gap_mdm_le_mdr_nonsingular_rankzeroevaluationdeterminanthscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_nonsingular_rankzeroevaluationdeterminanthscm_positive)) /\ ff_row_mdm_cell_mdr_nonsingular_rankzeroevaluationdeterminanthscm_positive_cell = S ff_row_mdm_prefix_mdr_nonsingular_rankzeroevaluationdeterminanthscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_nonsingular_rankzeroevaluationdeterminanthscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_nonsingular_rankzeroevaluationdeterminanthscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_nonsingular_rankzeroevaluationdeterminanthscm_positive) = (mdr_j_nonsingular_rankzeroevaluationdeterminanthsc)) /\ ff_column_mdm_cell_mdr_nonsingular_rankzeroevaluationdeterminanthscm_positive_cell = ff_column_mdm_prefix_mdr_nonsingular_rankzeroevaluationdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_nonsingular_rankzeroevaluationdeterminanthscm_positive_cell_column_after. ff_gap_mdm_le_mdr_nonsingular_rankzeroevaluationdeterminanthscm_positive_cell_column_after + (mdr_j_nonsingular_rankzeroevaluationdeterminanthsc) = (ff_column_mdm_prefix_mdr_nonsingular_rankzeroevaluationdeterminanthscm_positive)) /\ ff_column_mdm_cell_mdr_nonsingular_rankzeroevaluationdeterminanthscm_positive_cell = S ff_column_mdm_prefix_mdr_nonsingular_rankzeroevaluationdeterminanthscm_positive))) /\ (((exists ff_h_mdm_mdr_nonsingular_rankzeroevaluationdeterminanthscm_positive_cell_source. ff_h_mdm_mdr_nonsingular_rankzeroevaluationdeterminanthscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_nonsingular_rankzeroevaluationdeterminanthscm_positive) = S ((S ((ff_row_mdm_cell_mdr_nonsingular_rankzeroevaluationdeterminanthscm_positive_cell) * (S (mdr_q_nonsingular_rankzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_nonsingular_rankzeroevaluationdeterminanthscm_positive_cell))) * mdr_pc_nonsingular_rankzeroevaluationdeterminanth)) /\ exists ff_q_mdm_mdr_nonsingular_rankzeroevaluationdeterminanthscm_positive_cell_source. mdr_pb_nonsingular_rankzeroevaluationdeterminanth = ff_q_mdm_mdr_nonsingular_rankzeroevaluationdeterminanthscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_nonsingular_rankzeroevaluationdeterminanthscm_positive_cell) * (S (mdr_q_nonsingular_rankzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_nonsingular_rankzeroevaluationdeterminanthscm_positive_cell))) * mdr_pc_nonsingular_rankzeroevaluationdeterminanth) + (ff_value_mdm_prefix_mdr_nonsingular_rankzeroevaluationdeterminanthscm_positive)))))) /\ (((exists ff_h_mdm_mdr_nonsingular_rankzeroevaluationdeterminanthscm_positive_target. ff_h_mdm_mdr_nonsingular_rankzeroevaluationdeterminanthscm_positive_target + S (ff_value_mdm_prefix_mdr_nonsingular_rankzeroevaluationdeterminanthscm_positive) = S ((S (ff_index_mdm_prefix_mdr_nonsingular_rankzeroevaluationdeterminanthscm_positive)) * mdr_us_nonsingular_rankzeroevaluationdeterminanthsc)) /\ exists ff_q_mdm_mdr_nonsingular_rankzeroevaluationdeterminanthscm_positive_target. mdr_up_nonsingular_rankzeroevaluationdeterminanthsc = ff_q_mdm_mdr_nonsingular_rankzeroevaluationdeterminanthscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_nonsingular_rankzeroevaluationdeterminanthscm_positive)) * mdr_us_nonsingular_rankzeroevaluationdeterminanthsc) + (ff_value_mdm_prefix_mdr_nonsingular_rankzeroevaluationdeterminanthscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_nonsingular_rankzeroevaluationdeterminanthscm_negative. (exists ff_gap_mdm_lt_mdr_nonsingular_rankzeroevaluationdeterminanthscm_negative_index_bound. ff_gap_mdm_lt_mdr_nonsingular_rankzeroevaluationdeterminanthscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_nonsingular_rankzeroevaluationdeterminanthscm_negative) = ((mdr_q_nonsingular_rankzeroevaluationdeterminanths) * (mdr_q_nonsingular_rankzeroevaluationdeterminanths))) -> exists ff_row_mdm_prefix_mdr_nonsingular_rankzeroevaluationdeterminanthscm_negative ff_column_mdm_prefix_mdr_nonsingular_rankzeroevaluationdeterminanthscm_negative ff_value_mdm_prefix_mdr_nonsingular_rankzeroevaluationdeterminanthscm_negative. (ff_index_mdm_prefix_mdr_nonsingular_rankzeroevaluationdeterminanthscm_negative = (mdr_q_nonsingular_rankzeroevaluationdeterminanths) * ff_row_mdm_prefix_mdr_nonsingular_rankzeroevaluationdeterminanthscm_negative + ff_column_mdm_prefix_mdr_nonsingular_rankzeroevaluationdeterminanthscm_negative /\ ((exists ff_gap_mdm_lt_mdr_nonsingular_rankzeroevaluationdeterminanthscm_negative_column_bound. ff_gap_mdm_lt_mdr_nonsingular_rankzeroevaluationdeterminanthscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_nonsingular_rankzeroevaluationdeterminanthscm_negative) = (mdr_q_nonsingular_rankzeroevaluationdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_nonsingular_rankzeroevaluationdeterminanthscm_negative_cell ff_column_mdm_cell_mdr_nonsingular_rankzeroevaluationdeterminanthscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_nonsingular_rankzeroevaluationdeterminanthscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_nonsingular_rankzeroevaluationdeterminanthscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_nonsingular_rankzeroevaluationdeterminanthscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_nonsingular_rankzeroevaluationdeterminanthscm_negative_cell = ff_row_mdm_prefix_mdr_nonsingular_rankzeroevaluationdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_nonsingular_rankzeroevaluationdeterminanthscm_negative_cell_row_after. ff_gap_mdm_le_mdr_nonsingular_rankzeroevaluationdeterminanthscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_nonsingular_rankzeroevaluationdeterminanthscm_negative)) /\ ff_row_mdm_cell_mdr_nonsingular_rankzeroevaluationdeterminanthscm_negative_cell = S ff_row_mdm_prefix_mdr_nonsingular_rankzeroevaluationdeterminanthscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_nonsingular_rankzeroevaluationdeterminanthscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_nonsingular_rankzeroevaluationdeterminanthscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_nonsingular_rankzeroevaluationdeterminanthscm_negative) = (mdr_j_nonsingular_rankzeroevaluationdeterminanthsc)) /\ ff_column_mdm_cell_mdr_nonsingular_rankzeroevaluationdeterminanthscm_negative_cell = ff_column_mdm_prefix_mdr_nonsingular_rankzeroevaluationdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_nonsingular_rankzeroevaluationdeterminanthscm_negative_cell_column_after. ff_gap_mdm_le_mdr_nonsingular_rankzeroevaluationdeterminanthscm_negative_cell_column_after + (mdr_j_nonsingular_rankzeroevaluationdeterminanthsc) = (ff_column_mdm_prefix_mdr_nonsingular_rankzeroevaluationdeterminanthscm_negative)) /\ ff_column_mdm_cell_mdr_nonsingular_rankzeroevaluationdeterminanthscm_negative_cell = S ff_column_mdm_prefix_mdr_nonsingular_rankzeroevaluationdeterminanthscm_negative))) /\ (((exists ff_h_mdm_mdr_nonsingular_rankzeroevaluationdeterminanthscm_negative_cell_source. ff_h_mdm_mdr_nonsingular_rankzeroevaluationdeterminanthscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_nonsingular_rankzeroevaluationdeterminanthscm_negative) = S ((S ((ff_row_mdm_cell_mdr_nonsingular_rankzeroevaluationdeterminanthscm_negative_cell) * (S (mdr_q_nonsingular_rankzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_nonsingular_rankzeroevaluationdeterminanthscm_negative_cell))) * mdr_nc_nonsingular_rankzeroevaluationdeterminanth)) /\ exists ff_q_mdm_mdr_nonsingular_rankzeroevaluationdeterminanthscm_negative_cell_source. mdr_nb_nonsingular_rankzeroevaluationdeterminanth = ff_q_mdm_mdr_nonsingular_rankzeroevaluationdeterminanthscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_nonsingular_rankzeroevaluationdeterminanthscm_negative_cell) * (S (mdr_q_nonsingular_rankzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_nonsingular_rankzeroevaluationdeterminanthscm_negative_cell))) * mdr_nc_nonsingular_rankzeroevaluationdeterminanth) + (ff_value_mdm_prefix_mdr_nonsingular_rankzeroevaluationdeterminanthscm_negative)))))) /\ (((exists ff_h_mdm_mdr_nonsingular_rankzeroevaluationdeterminanthscm_negative_target. ff_h_mdm_mdr_nonsingular_rankzeroevaluationdeterminanthscm_negative_target + S (ff_value_mdm_prefix_mdr_nonsingular_rankzeroevaluationdeterminanthscm_negative) = S ((S (ff_index_mdm_prefix_mdr_nonsingular_rankzeroevaluationdeterminanthscm_negative)) * mdr_ut_nonsingular_rankzeroevaluationdeterminanthsc)) /\ exists ff_q_mdm_mdr_nonsingular_rankzeroevaluationdeterminanthscm_negative_target. mdr_un_nonsingular_rankzeroevaluationdeterminanthsc = ff_q_mdm_mdr_nonsingular_rankzeroevaluationdeterminanthscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_nonsingular_rankzeroevaluationdeterminanthscm_negative)) * mdr_ut_nonsingular_rankzeroevaluationdeterminanthsc) + (ff_value_mdm_prefix_mdr_nonsingular_rankzeroevaluationdeterminanthscm_negative))))))))) /\ ((((exists ff_h_mdr_nonsingular_rankzeroevaluationdeterminanthscp. ff_h_mdr_nonsingular_rankzeroevaluationdeterminanthscp + S (mdr_p_nonsingular_rankzeroevaluationdeterminanthsc) = S ((S (mdr_j_nonsingular_rankzeroevaluationdeterminanthsc)) * mdr_ec_nonsingular_rankzeroevaluationdeterminanths)) /\ exists ff_q_mdr_nonsingular_rankzeroevaluationdeterminanthscp. mdr_eb_nonsingular_rankzeroevaluationdeterminanths = ff_q_mdr_nonsingular_rankzeroevaluationdeterminanthscp * S ((S (mdr_j_nonsingular_rankzeroevaluationdeterminanthsc)) * mdr_ec_nonsingular_rankzeroevaluationdeterminanths) + (mdr_p_nonsingular_rankzeroevaluationdeterminanthsc))) /\ (((exists ff_h_mdr_nonsingular_rankzeroevaluationdeterminanthscn. ff_h_mdr_nonsingular_rankzeroevaluationdeterminanthscn + S (mdr_n_nonsingular_rankzeroevaluationdeterminanthsc) = S ((S (mdr_j_nonsingular_rankzeroevaluationdeterminanthsc)) * mdr_fc_nonsingular_rankzeroevaluationdeterminanths)) /\ exists ff_q_mdr_nonsingular_rankzeroevaluationdeterminanthscn. mdr_fb_nonsingular_rankzeroevaluationdeterminanths = ff_q_mdr_nonsingular_rankzeroevaluationdeterminanthscn * S ((S (mdr_j_nonsingular_rankzeroevaluationdeterminanthsc)) * mdr_fc_nonsingular_rankzeroevaluationdeterminanths) + (mdr_n_nonsingular_rankzeroevaluationdeterminanthsc)))))))) /\ (exists ff_ub_mce_fold_mdr_nonsingular_rankzeroevaluationdeterminanthsf ff_uc_mce_fold_mdr_nonsingular_rankzeroevaluationdeterminanthsf ff_vb_mce_fold_mdr_nonsingular_rankzeroevaluationdeterminanthsf ff_vc_mce_fold_mdr_nonsingular_rankzeroevaluationdeterminanthsf. ((forall ff_index_mce_alternating_mdr_nonsingular_rankzeroevaluationdeterminanthsf_prefix. (exists ff_gap_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_prefix_index. ff_gap_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_prefix_index + S (ff_index_mce_alternating_mdr_nonsingular_rankzeroevaluationdeterminanthsf_prefix) = (S (mdr_q_nonsingular_rankzeroevaluationdeterminanths))) -> exists ff_ap_mce_alternating_mdr_nonsingular_rankzeroevaluationdeterminanthsf_prefix ff_an_mce_alternating_mdr_nonsingular_rankzeroevaluationdeterminanthsf_prefix ff_bp_mce_alternating_mdr_nonsingular_rankzeroevaluationdeterminanthsf_prefix ff_bn_mce_alternating_mdr_nonsingular_rankzeroevaluationdeterminanthsf_prefix ff_p_mce_alternating_mdr_nonsingular_rankzeroevaluationdeterminanthsf_prefix ff_n_mce_alternating_mdr_nonsingular_rankzeroevaluationdeterminanthsf_prefix. ((((exists ff_h_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_prefix_ap. ff_h_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_prefix_ap + S (ff_ap_mce_alternating_mdr_nonsingular_rankzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_nonsingular_rankzeroevaluationdeterminanthsf_prefix)) * mdr_pc_nonsingular_rankzeroevaluationdeterminanth)) /\ exists ff_q_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_prefix_ap. mdr_pb_nonsingular_rankzeroevaluationdeterminanth = ff_q_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_nonsingular_rankzeroevaluationdeterminanthsf_prefix)) * mdr_pc_nonsingular_rankzeroevaluationdeterminanth) + (ff_ap_mce_alternating_mdr_nonsingular_rankzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_prefix_an. ff_h_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_prefix_an + S (ff_an_mce_alternating_mdr_nonsingular_rankzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_nonsingular_rankzeroevaluationdeterminanthsf_prefix)) * mdr_nc_nonsingular_rankzeroevaluationdeterminanth)) /\ exists ff_q_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_prefix_an. mdr_nb_nonsingular_rankzeroevaluationdeterminanth = ff_q_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_nonsingular_rankzeroevaluationdeterminanthsf_prefix)) * mdr_nc_nonsingular_rankzeroevaluationdeterminanth) + (ff_an_mce_alternating_mdr_nonsingular_rankzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_prefix_bp. ff_h_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_prefix_bp + S (ff_bp_mce_alternating_mdr_nonsingular_rankzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_nonsingular_rankzeroevaluationdeterminanthsf_prefix)) * mdr_ec_nonsingular_rankzeroevaluationdeterminanths)) /\ exists ff_q_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_prefix_bp. mdr_eb_nonsingular_rankzeroevaluationdeterminanths = ff_q_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_nonsingular_rankzeroevaluationdeterminanthsf_prefix)) * mdr_ec_nonsingular_rankzeroevaluationdeterminanths) + (ff_bp_mce_alternating_mdr_nonsingular_rankzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_prefix_bn. ff_h_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_prefix_bn + S (ff_bn_mce_alternating_mdr_nonsingular_rankzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_nonsingular_rankzeroevaluationdeterminanthsf_prefix)) * mdr_fc_nonsingular_rankzeroevaluationdeterminanths)) /\ exists ff_q_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_prefix_bn. mdr_fb_nonsingular_rankzeroevaluationdeterminanths = ff_q_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_nonsingular_rankzeroevaluationdeterminanthsf_prefix)) * mdr_fc_nonsingular_rankzeroevaluationdeterminanths) + (ff_bn_mce_alternating_mdr_nonsingular_rankzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_prefix_positive. ff_h_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_prefix_positive + S (ff_p_mce_alternating_mdr_nonsingular_rankzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_nonsingular_rankzeroevaluationdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_nonsingular_rankzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_prefix_positive. ff_ub_mce_fold_mdr_nonsingular_rankzeroevaluationdeterminanthsf = ff_q_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_nonsingular_rankzeroevaluationdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_nonsingular_rankzeroevaluationdeterminanthsf) + (ff_p_mce_alternating_mdr_nonsingular_rankzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_prefix_negative. ff_h_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_prefix_negative + S (ff_n_mce_alternating_mdr_nonsingular_rankzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_nonsingular_rankzeroevaluationdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_nonsingular_rankzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_prefix_negative. ff_vb_mce_fold_mdr_nonsingular_rankzeroevaluationdeterminanthsf = ff_q_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_nonsingular_rankzeroevaluationdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_nonsingular_rankzeroevaluationdeterminanthsf) + (ff_n_mce_alternating_mdr_nonsingular_rankzeroevaluationdeterminanthsf_prefix))) /\ (((exists ff_even_mce_term_mdr_nonsingular_rankzeroevaluationdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_nonsingular_rankzeroevaluationdeterminanthsf_prefix = 2 * ff_even_mce_term_mdr_nonsingular_rankzeroevaluationdeterminanthsf_prefix_term) /\ (ff_p_mce_alternating_mdr_nonsingular_rankzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_nonsingular_rankzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_nonsingular_rankzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_nonsingular_rankzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_nonsingular_rankzeroevaluationdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_nonsingular_rankzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_nonsingular_rankzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_nonsingular_rankzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_nonsingular_rankzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_nonsingular_rankzeroevaluationdeterminanthsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_nonsingular_rankzeroevaluationdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_nonsingular_rankzeroevaluationdeterminanthsf_prefix = 2 * ff_odd_mce_term_mdr_nonsingular_rankzeroevaluationdeterminanthsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_nonsingular_rankzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_nonsingular_rankzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_nonsingular_rankzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_nonsingular_rankzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_nonsingular_rankzeroevaluationdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_nonsingular_rankzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_nonsingular_rankzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_nonsingular_rankzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_nonsingular_rankzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_nonsingular_rankzeroevaluationdeterminanthsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_positive ff_v_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_positive. ((((exists ff_h_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_positive_start. ff_h_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_positive_start. ff_u_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_positive_start * S ((S (0)) * ff_v_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_positive_terminal. ff_h_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_positive_terminal + S (mdr_p_nonsingular_rankzeroevaluationdeterminanth) = S ((S ((S (mdr_q_nonsingular_rankzeroevaluationdeterminanths)))) * ff_v_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_positive_terminal. ff_u_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_positive_terminal * S ((S ((S (mdr_q_nonsingular_rankzeroevaluationdeterminanths)))) * ff_v_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_positive) + (mdr_p_nonsingular_rankzeroevaluationdeterminanth))) /\ forall ff_i_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_positive. (exists ff_lt_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_positive_bound. ff_lt_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_positive_bound + S ff_i_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_positive = (S (mdr_q_nonsingular_rankzeroevaluationdeterminanths))) -> exists ff_a_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_positive ff_r_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_positive ff_s_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_positive. ((((exists ff_h_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_positive_summand. ff_h_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_positive_summand + S (ff_a_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_nonsingular_rankzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_positive_summand. ff_ub_mce_fold_mdr_nonsingular_rankzeroevaluationdeterminanthsf = ff_q_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_positive_summand * S ((S (ff_i_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_nonsingular_rankzeroevaluationdeterminanthsf) + (ff_a_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_positive_partial. ff_h_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_positive_partial + S (ff_r_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_positive_partial. ff_u_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_positive_partial * S ((S (ff_i_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_positive) + (ff_r_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_positive_successor. ff_h_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_positive_successor + S (ff_s_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_positive) = S ((S (S ff_i_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_positive_successor. ff_u_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_positive_successor * S ((S (S ff_i_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_positive) + (ff_s_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_positive))) /\ ff_s_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_positive = ff_r_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_positive + ff_a_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_positive)))))) /\ (exists ff_u_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_negative ff_v_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_negative. ((((exists ff_h_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_negative_start. ff_h_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_negative_start. ff_u_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_negative_start * S ((S (0)) * ff_v_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_negative_terminal. ff_h_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_negative_terminal + S (mdr_n_nonsingular_rankzeroevaluationdeterminanth) = S ((S ((S (mdr_q_nonsingular_rankzeroevaluationdeterminanths)))) * ff_v_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_negative_terminal. ff_u_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_negative_terminal * S ((S ((S (mdr_q_nonsingular_rankzeroevaluationdeterminanths)))) * ff_v_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_negative) + (mdr_n_nonsingular_rankzeroevaluationdeterminanth))) /\ forall ff_i_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_negative. (exists ff_lt_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_negative_bound. ff_lt_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_negative_bound + S ff_i_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_negative = (S (mdr_q_nonsingular_rankzeroevaluationdeterminanths))) -> exists ff_a_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_negative ff_r_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_negative ff_s_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_negative. ((((exists ff_h_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_negative_summand. ff_h_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_negative_summand + S (ff_a_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_nonsingular_rankzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_negative_summand. ff_vb_mce_fold_mdr_nonsingular_rankzeroevaluationdeterminanthsf = ff_q_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_negative_summand * S ((S (ff_i_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_nonsingular_rankzeroevaluationdeterminanthsf) + (ff_a_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_negative_partial. ff_h_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_negative_partial + S (ff_r_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_negative_partial. ff_u_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_negative_partial * S ((S (ff_i_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_negative) + (ff_r_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_negative_successor. ff_h_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_negative_successor + S (ff_s_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_negative) = S ((S (S ff_i_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_negative_successor. ff_u_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_negative_successor * S ((S (S ff_i_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_negative) + (ff_s_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_negative))) /\ ff_s_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_negative = ff_r_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_negative + ff_a_mce_mdr_nonsingular_rankzeroevaluationdeterminanthsf_negative))))))))))))))) /\ ((exists mdr_gap_nonsingular_rankzeroevaluationdeterminanti. mdr_gap_nonsingular_rankzeroevaluationdeterminanti + S (mdr_i_nonsingular_rankzeroevaluationdeterminant) = (mdr_l_nonsingular_rankzeroevaluationdeterminant)) /\ (exists mdr_z_nonsingular_rankzeroevaluationdeterminantr. ((exists mdr_a_nonsingular_rankzeroevaluationdeterminantrc mdr_b_nonsingular_rankzeroevaluationdeterminantrc mdr_c_nonsingular_rankzeroevaluationdeterminantrc mdr_e_nonsingular_rankzeroevaluationdeterminantrc mdr_f_nonsingular_rankzeroevaluationdeterminantrc. ((mdr_a_nonsingular_rankzeroevaluationdeterminantrc = ((mdr_q_nonsingular_rank) + (mdr_ub_nonsingular_rankzeroevaluation)) * S ((mdr_q_nonsingular_rank) + (mdr_ub_nonsingular_rankzeroevaluation)) + ((mdr_ub_nonsingular_rankzeroevaluation) + (mdr_ub_nonsingular_rankzeroevaluation))) /\ ((mdr_b_nonsingular_rankzeroevaluationdeterminantrc = ((mdr_uc_nonsingular_rankzeroevaluation) + (mdr_vb_nonsingular_rankzeroevaluation)) * S ((mdr_uc_nonsingular_rankzeroevaluation) + (mdr_vb_nonsingular_rankzeroevaluation)) + ((mdr_vb_nonsingular_rankzeroevaluation) + (mdr_vb_nonsingular_rankzeroevaluation))) /\ ((mdr_c_nonsingular_rankzeroevaluationdeterminantrc = ((mdr_a_nonsingular_rankzeroevaluationdeterminantrc) + (mdr_b_nonsingular_rankzeroevaluationdeterminantrc)) * S ((mdr_a_nonsingular_rankzeroevaluationdeterminantrc) + (mdr_b_nonsingular_rankzeroevaluationdeterminantrc)) + ((mdr_b_nonsingular_rankzeroevaluationdeterminantrc) + (mdr_b_nonsingular_rankzeroevaluationdeterminantrc))) /\ ((mdr_e_nonsingular_rankzeroevaluationdeterminantrc = ((mdr_p_nonsingular_rankzero) + (mdr_n_nonsingular_rankzero)) * S ((mdr_p_nonsingular_rankzero) + (mdr_n_nonsingular_rankzero)) + ((mdr_n_nonsingular_rankzero) + (mdr_n_nonsingular_rankzero))) /\ ((mdr_f_nonsingular_rankzeroevaluationdeterminantrc = ((mdr_vc_nonsingular_rankzeroevaluation) + (mdr_e_nonsingular_rankzeroevaluationdeterminantrc)) * S ((mdr_vc_nonsingular_rankzeroevaluation) + (mdr_e_nonsingular_rankzeroevaluationdeterminantrc)) + ((mdr_e_nonsingular_rankzeroevaluationdeterminantrc) + (mdr_e_nonsingular_rankzeroevaluationdeterminantrc))) /\ ((mdr_z_nonsingular_rankzeroevaluationdeterminantr) = ((mdr_c_nonsingular_rankzeroevaluationdeterminantrc) + (mdr_f_nonsingular_rankzeroevaluationdeterminantrc)) * S ((mdr_c_nonsingular_rankzeroevaluationdeterminantrc) + (mdr_f_nonsingular_rankzeroevaluationdeterminantrc)) + ((mdr_f_nonsingular_rankzeroevaluationdeterminantrc) + (mdr_f_nonsingular_rankzeroevaluationdeterminantrc))))))))) /\ (((exists ff_h_mdr_nonsingular_rankzeroevaluationdeterminantrb. ff_h_mdr_nonsingular_rankzeroevaluationdeterminantrb + S (mdr_z_nonsingular_rankzeroevaluationdeterminantr) = S ((S (mdr_i_nonsingular_rankzeroevaluationdeterminant)) * mdr_c_nonsingular_rankzeroevaluationdeterminant)) /\ exists ff_q_mdr_nonsingular_rankzeroevaluationdeterminantrb. mdr_b_nonsingular_rankzeroevaluationdeterminant = ff_q_mdr_nonsingular_rankzeroevaluationdeterminantrb * S ((S (mdr_i_nonsingular_rankzeroevaluationdeterminant)) * mdr_c_nonsingular_rankzeroevaluationdeterminant) + (mdr_z_nonsingular_rankzeroevaluationdeterminantr)))))))))) -> mdr_p_nonsingular_rankzero = mdr_n_nonsingular_rankzero))))))