matrix_rank_selected_determinant_functional

Exact expanded first-order arithmetic statement

forall pb pc nb nc w rb rc cb cc q p n P N. (exists mdr_ub_selected_det_first mdr_uc_selected_det_first mdr_vb_selected_det_first mdr_vc_selected_det_first. ((((forall mdr_i_selected_det_firstmatrixpositive. (exists mdr_gap_selected_det_firstmatrixpositivebound. mdr_gap_selected_det_firstmatrixpositivebound + S (mdr_i_selected_det_firstmatrixpositive) = ((q) * (q))) -> exists mdr_a_selected_det_firstmatrixpositive. (((exists mdr_r_selected_det_firstmatrixpositivepoint mdr_s_selected_det_firstmatrixpositivepoint mdr_u_selected_det_firstmatrixpositivepoint mdr_v_selected_det_firstmatrixpositivepoint. ((mdr_i_selected_det_firstmatrixpositive = (q) * mdr_r_selected_det_firstmatrixpositivepoint + mdr_s_selected_det_firstmatrixpositivepoint) /\ ((exists mdr_gap_selected_det_firstmatrixpositivepointcolumn. mdr_gap_selected_det_firstmatrixpositivepointcolumn + S (mdr_s_selected_det_firstmatrixpositivepoint) = (q)) /\ ((((exists ff_h_mdr_selected_det_firstmatrixpositivepointrow_index. ff_h_mdr_selected_det_firstmatrixpositivepointrow_index + S (mdr_u_selected_det_firstmatrixpositivepoint) = S ((S (mdr_r_selected_det_firstmatrixpositivepoint)) * rc)) /\ exists ff_q_mdr_selected_det_firstmatrixpositivepointrow_index. rb = ff_q_mdr_selected_det_firstmatrixpositivepointrow_index * S ((S (mdr_r_selected_det_firstmatrixpositivepoint)) * rc) + (mdr_u_selected_det_firstmatrixpositivepoint))) /\ ((((exists ff_h_mdr_selected_det_firstmatrixpositivepointcolumn_index. ff_h_mdr_selected_det_firstmatrixpositivepointcolumn_index + S (mdr_v_selected_det_firstmatrixpositivepoint) = S ((S (mdr_s_selected_det_firstmatrixpositivepoint)) * cc)) /\ exists ff_q_mdr_selected_det_firstmatrixpositivepointcolumn_index. cb = ff_q_mdr_selected_det_firstmatrixpositivepointcolumn_index * S ((S (mdr_s_selected_det_firstmatrixpositivepoint)) * cc) + (mdr_v_selected_det_firstmatrixpositivepoint))) /\ (((exists ff_h_mdr_selected_det_firstmatrixpositivepointsource. ff_h_mdr_selected_det_firstmatrixpositivepointsource + S (mdr_a_selected_det_firstmatrixpositive) = S ((S ((mdr_u_selected_det_firstmatrixpositivepoint) * (w) + (mdr_v_selected_det_firstmatrixpositivepoint))) * pc)) /\ exists ff_q_mdr_selected_det_firstmatrixpositivepointsource. pb = ff_q_mdr_selected_det_firstmatrixpositivepointsource * S ((S ((mdr_u_selected_det_firstmatrixpositivepoint) * (w) + (mdr_v_selected_det_firstmatrixpositivepoint))) * pc) + (mdr_a_selected_det_firstmatrixpositive)))))))) /\ (((exists ff_h_mdr_selected_det_firstmatrixpositiveoutput. ff_h_mdr_selected_det_firstmatrixpositiveoutput + S (mdr_a_selected_det_firstmatrixpositive) = S ((S (mdr_i_selected_det_firstmatrixpositive)) * mdr_uc_selected_det_first)) /\ exists ff_q_mdr_selected_det_firstmatrixpositiveoutput. mdr_ub_selected_det_first = ff_q_mdr_selected_det_firstmatrixpositiveoutput * S ((S (mdr_i_selected_det_firstmatrixpositive)) * mdr_uc_selected_det_first) + (mdr_a_selected_det_firstmatrixpositive)))))) /\ (forall mdr_i_selected_det_firstmatrixnegative. (exists mdr_gap_selected_det_firstmatrixnegativebound. mdr_gap_selected_det_firstmatrixnegativebound + S (mdr_i_selected_det_firstmatrixnegative) = ((q) * (q))) -> exists mdr_a_selected_det_firstmatrixnegative. (((exists mdr_r_selected_det_firstmatrixnegativepoint mdr_s_selected_det_firstmatrixnegativepoint mdr_u_selected_det_firstmatrixnegativepoint mdr_v_selected_det_firstmatrixnegativepoint. ((mdr_i_selected_det_firstmatrixnegative = (q) * mdr_r_selected_det_firstmatrixnegativepoint + mdr_s_selected_det_firstmatrixnegativepoint) /\ ((exists mdr_gap_selected_det_firstmatrixnegativepointcolumn. mdr_gap_selected_det_firstmatrixnegativepointcolumn + S (mdr_s_selected_det_firstmatrixnegativepoint) = (q)) /\ ((((exists ff_h_mdr_selected_det_firstmatrixnegativepointrow_index. ff_h_mdr_selected_det_firstmatrixnegativepointrow_index + S (mdr_u_selected_det_firstmatrixnegativepoint) = S ((S (mdr_r_selected_det_firstmatrixnegativepoint)) * rc)) /\ exists ff_q_mdr_selected_det_firstmatrixnegativepointrow_index. rb = ff_q_mdr_selected_det_firstmatrixnegativepointrow_index * S ((S (mdr_r_selected_det_firstmatrixnegativepoint)) * rc) + (mdr_u_selected_det_firstmatrixnegativepoint))) /\ ((((exists ff_h_mdr_selected_det_firstmatrixnegativepointcolumn_index. ff_h_mdr_selected_det_firstmatrixnegativepointcolumn_index + S (mdr_v_selected_det_firstmatrixnegativepoint) = S ((S (mdr_s_selected_det_firstmatrixnegativepoint)) * cc)) /\ exists ff_q_mdr_selected_det_firstmatrixnegativepointcolumn_index. cb = ff_q_mdr_selected_det_firstmatrixnegativepointcolumn_index * S ((S (mdr_s_selected_det_firstmatrixnegativepoint)) * cc) + (mdr_v_selected_det_firstmatrixnegativepoint))) /\ (((exists ff_h_mdr_selected_det_firstmatrixnegativepointsource. ff_h_mdr_selected_det_firstmatrixnegativepointsource + S (mdr_a_selected_det_firstmatrixnegative) = S ((S ((mdr_u_selected_det_firstmatrixnegativepoint) * (w) + (mdr_v_selected_det_firstmatrixnegativepoint))) * nc)) /\ exists ff_q_mdr_selected_det_firstmatrixnegativepointsource. nb = ff_q_mdr_selected_det_firstmatrixnegativepointsource * S ((S ((mdr_u_selected_det_firstmatrixnegativepoint) * (w) + (mdr_v_selected_det_firstmatrixnegativepoint))) * nc) + (mdr_a_selected_det_firstmatrixnegative)))))))) /\ (((exists ff_h_mdr_selected_det_firstmatrixnegativeoutput. ff_h_mdr_selected_det_firstmatrixnegativeoutput + S (mdr_a_selected_det_firstmatrixnegative) = S ((S (mdr_i_selected_det_firstmatrixnegative)) * mdr_vc_selected_det_first)) /\ exists ff_q_mdr_selected_det_firstmatrixnegativeoutput. mdr_vb_selected_det_first = ff_q_mdr_selected_det_firstmatrixnegativeoutput * S ((S (mdr_i_selected_det_firstmatrixnegative)) * mdr_vc_selected_det_first) + (mdr_a_selected_det_firstmatrixnegative)))))))) /\ (exists mdr_b_selected_det_firstdeterminant mdr_c_selected_det_firstdeterminant mdr_l_selected_det_firstdeterminant mdr_i_selected_det_firstdeterminant. ((forall mdr_i_selected_det_firstdeterminanth. (exists mdr_gap_selected_det_firstdeterminanthi. mdr_gap_selected_det_firstdeterminanthi + S (mdr_i_selected_det_firstdeterminanth) = (mdr_l_selected_det_firstdeterminant)) -> exists mdr_d_selected_det_firstdeterminanth mdr_pb_selected_det_firstdeterminanth mdr_pc_selected_det_firstdeterminanth mdr_nb_selected_det_firstdeterminanth mdr_nc_selected_det_firstdeterminanth mdr_p_selected_det_firstdeterminanth mdr_n_selected_det_firstdeterminanth. ((exists mdr_z_selected_det_firstdeterminanthr. ((exists mdr_a_selected_det_firstdeterminanthrc mdr_b_selected_det_firstdeterminanthrc mdr_c_selected_det_firstdeterminanthrc mdr_e_selected_det_firstdeterminanthrc mdr_f_selected_det_firstdeterminanthrc. ((mdr_a_selected_det_firstdeterminanthrc = ((mdr_d_selected_det_firstdeterminanth) + (mdr_pb_selected_det_firstdeterminanth)) * S ((mdr_d_selected_det_firstdeterminanth) + (mdr_pb_selected_det_firstdeterminanth)) + ((mdr_pb_selected_det_firstdeterminanth) + (mdr_pb_selected_det_firstdeterminanth))) /\ ((mdr_b_selected_det_firstdeterminanthrc = ((mdr_pc_selected_det_firstdeterminanth) + (mdr_nb_selected_det_firstdeterminanth)) * S ((mdr_pc_selected_det_firstdeterminanth) + (mdr_nb_selected_det_firstdeterminanth)) + ((mdr_nb_selected_det_firstdeterminanth) + (mdr_nb_selected_det_firstdeterminanth))) /\ ((mdr_c_selected_det_firstdeterminanthrc = ((mdr_a_selected_det_firstdeterminanthrc) + (mdr_b_selected_det_firstdeterminanthrc)) * S ((mdr_a_selected_det_firstdeterminanthrc) + (mdr_b_selected_det_firstdeterminanthrc)) + ((mdr_b_selected_det_firstdeterminanthrc) + (mdr_b_selected_det_firstdeterminanthrc))) /\ ((mdr_e_selected_det_firstdeterminanthrc = ((mdr_p_selected_det_firstdeterminanth) + (mdr_n_selected_det_firstdeterminanth)) * S ((mdr_p_selected_det_firstdeterminanth) + (mdr_n_selected_det_firstdeterminanth)) + ((mdr_n_selected_det_firstdeterminanth) + (mdr_n_selected_det_firstdeterminanth))) /\ ((mdr_f_selected_det_firstdeterminanthrc = ((mdr_nc_selected_det_firstdeterminanth) + (mdr_e_selected_det_firstdeterminanthrc)) * S ((mdr_nc_selected_det_firstdeterminanth) + (mdr_e_selected_det_firstdeterminanthrc)) + ((mdr_e_selected_det_firstdeterminanthrc) + (mdr_e_selected_det_firstdeterminanthrc))) /\ ((mdr_z_selected_det_firstdeterminanthr) = ((mdr_c_selected_det_firstdeterminanthrc) + (mdr_f_selected_det_firstdeterminanthrc)) * S ((mdr_c_selected_det_firstdeterminanthrc) + (mdr_f_selected_det_firstdeterminanthrc)) + ((mdr_f_selected_det_firstdeterminanthrc) + (mdr_f_selected_det_firstdeterminanthrc))))))))) /\ (((exists ff_h_mdr_selected_det_firstdeterminanthrb. ff_h_mdr_selected_det_firstdeterminanthrb + S (mdr_z_selected_det_firstdeterminanthr) = S ((S (mdr_i_selected_det_firstdeterminanth)) * mdr_c_selected_det_firstdeterminant)) /\ exists ff_q_mdr_selected_det_firstdeterminanthrb. mdr_b_selected_det_firstdeterminant = ff_q_mdr_selected_det_firstdeterminanthrb * S ((S (mdr_i_selected_det_firstdeterminanth)) * mdr_c_selected_det_firstdeterminant) + (mdr_z_selected_det_firstdeterminanthr))))) /\ (((((mdr_d_selected_det_firstdeterminanth) = 0) /\ (((mdr_p_selected_det_firstdeterminanth) = 1) /\ ((mdr_n_selected_det_firstdeterminanth) = 0))) \/ exists mdr_q_selected_det_firstdeterminanths mdr_eb_selected_det_firstdeterminanths mdr_ec_selected_det_firstdeterminanths mdr_fb_selected_det_firstdeterminanths mdr_fc_selected_det_firstdeterminanths. (((mdr_d_selected_det_firstdeterminanth) = S (mdr_q_selected_det_firstdeterminanths)) /\ ((forall mdr_j_selected_det_firstdeterminanthsc. (exists mdr_gap_selected_det_firstdeterminanthscj. mdr_gap_selected_det_firstdeterminanthscj + S (mdr_j_selected_det_firstdeterminanthsc) = (S (mdr_q_selected_det_firstdeterminanths))) -> exists mdr_i_selected_det_firstdeterminanthsc mdr_up_selected_det_firstdeterminanthsc mdr_us_selected_det_firstdeterminanthsc mdr_un_selected_det_firstdeterminanthsc mdr_ut_selected_det_firstdeterminanthsc mdr_p_selected_det_firstdeterminanthsc mdr_n_selected_det_firstdeterminanthsc. ((exists mdr_gap_selected_det_firstdeterminanthsci. mdr_gap_selected_det_firstdeterminanthsci + S (mdr_i_selected_det_firstdeterminanthsc) = (mdr_i_selected_det_firstdeterminanth)) /\ ((exists mdr_z_selected_det_firstdeterminanthscr. ((exists mdr_a_selected_det_firstdeterminanthscrc mdr_b_selected_det_firstdeterminanthscrc mdr_c_selected_det_firstdeterminanthscrc mdr_e_selected_det_firstdeterminanthscrc mdr_f_selected_det_firstdeterminanthscrc. ((mdr_a_selected_det_firstdeterminanthscrc = ((mdr_q_selected_det_firstdeterminanths) + (mdr_up_selected_det_firstdeterminanthsc)) * S ((mdr_q_selected_det_firstdeterminanths) + (mdr_up_selected_det_firstdeterminanthsc)) + ((mdr_up_selected_det_firstdeterminanthsc) + (mdr_up_selected_det_firstdeterminanthsc))) /\ ((mdr_b_selected_det_firstdeterminanthscrc = ((mdr_us_selected_det_firstdeterminanthsc) + (mdr_un_selected_det_firstdeterminanthsc)) * S ((mdr_us_selected_det_firstdeterminanthsc) + (mdr_un_selected_det_firstdeterminanthsc)) + ((mdr_un_selected_det_firstdeterminanthsc) + (mdr_un_selected_det_firstdeterminanthsc))) /\ ((mdr_c_selected_det_firstdeterminanthscrc = ((mdr_a_selected_det_firstdeterminanthscrc) + (mdr_b_selected_det_firstdeterminanthscrc)) * S ((mdr_a_selected_det_firstdeterminanthscrc) + (mdr_b_selected_det_firstdeterminanthscrc)) + ((mdr_b_selected_det_firstdeterminanthscrc) + (mdr_b_selected_det_firstdeterminanthscrc))) /\ ((mdr_e_selected_det_firstdeterminanthscrc = ((mdr_p_selected_det_firstdeterminanthsc) + (mdr_n_selected_det_firstdeterminanthsc)) * S ((mdr_p_selected_det_firstdeterminanthsc) + (mdr_n_selected_det_firstdeterminanthsc)) + ((mdr_n_selected_det_firstdeterminanthsc) + (mdr_n_selected_det_firstdeterminanthsc))) /\ ((mdr_f_selected_det_firstdeterminanthscrc = ((mdr_ut_selected_det_firstdeterminanthsc) + (mdr_e_selected_det_firstdeterminanthscrc)) * S ((mdr_ut_selected_det_firstdeterminanthsc) + (mdr_e_selected_det_firstdeterminanthscrc)) + ((mdr_e_selected_det_firstdeterminanthscrc) + (mdr_e_selected_det_firstdeterminanthscrc))) /\ ((mdr_z_selected_det_firstdeterminanthscr) = ((mdr_c_selected_det_firstdeterminanthscrc) + (mdr_f_selected_det_firstdeterminanthscrc)) * S ((mdr_c_selected_det_firstdeterminanthscrc) + (mdr_f_selected_det_firstdeterminanthscrc)) + ((mdr_f_selected_det_firstdeterminanthscrc) + (mdr_f_selected_det_firstdeterminanthscrc))))))))) /\ (((exists ff_h_mdr_selected_det_firstdeterminanthscrb. ff_h_mdr_selected_det_firstdeterminanthscrb + S (mdr_z_selected_det_firstdeterminanthscr) = S ((S (mdr_i_selected_det_firstdeterminanthsc)) * mdr_c_selected_det_firstdeterminant)) /\ exists ff_q_mdr_selected_det_firstdeterminanthscrb. mdr_b_selected_det_firstdeterminant = ff_q_mdr_selected_det_firstdeterminanthscrb * S ((S (mdr_i_selected_det_firstdeterminanthsc)) * mdr_c_selected_det_firstdeterminant) + (mdr_z_selected_det_firstdeterminanthscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_selected_det_firstdeterminanthscm_positive. (exists ff_gap_mdm_lt_mdr_selected_det_firstdeterminanthscm_positive_index_bound. ff_gap_mdm_lt_mdr_selected_det_firstdeterminanthscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_selected_det_firstdeterminanthscm_positive) = ((mdr_q_selected_det_firstdeterminanths) * (mdr_q_selected_det_firstdeterminanths))) -> exists ff_row_mdm_prefix_mdr_selected_det_firstdeterminanthscm_positive ff_column_mdm_prefix_mdr_selected_det_firstdeterminanthscm_positive ff_value_mdm_prefix_mdr_selected_det_firstdeterminanthscm_positive. (ff_index_mdm_prefix_mdr_selected_det_firstdeterminanthscm_positive = (mdr_q_selected_det_firstdeterminanths) * ff_row_mdm_prefix_mdr_selected_det_firstdeterminanthscm_positive + ff_column_mdm_prefix_mdr_selected_det_firstdeterminanthscm_positive /\ ((exists ff_gap_mdm_lt_mdr_selected_det_firstdeterminanthscm_positive_column_bound. ff_gap_mdm_lt_mdr_selected_det_firstdeterminanthscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_selected_det_firstdeterminanthscm_positive) = (mdr_q_selected_det_firstdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_selected_det_firstdeterminanthscm_positive_cell ff_column_mdm_cell_mdr_selected_det_firstdeterminanthscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_selected_det_firstdeterminanthscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_selected_det_firstdeterminanthscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_selected_det_firstdeterminanthscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_selected_det_firstdeterminanthscm_positive_cell = ff_row_mdm_prefix_mdr_selected_det_firstdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_selected_det_firstdeterminanthscm_positive_cell_row_after. ff_gap_mdm_le_mdr_selected_det_firstdeterminanthscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_selected_det_firstdeterminanthscm_positive)) /\ ff_row_mdm_cell_mdr_selected_det_firstdeterminanthscm_positive_cell = S ff_row_mdm_prefix_mdr_selected_det_firstdeterminanthscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_selected_det_firstdeterminanthscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_selected_det_firstdeterminanthscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_selected_det_firstdeterminanthscm_positive) = (mdr_j_selected_det_firstdeterminanthsc)) /\ ff_column_mdm_cell_mdr_selected_det_firstdeterminanthscm_positive_cell = ff_column_mdm_prefix_mdr_selected_det_firstdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_selected_det_firstdeterminanthscm_positive_cell_column_after. ff_gap_mdm_le_mdr_selected_det_firstdeterminanthscm_positive_cell_column_after + (mdr_j_selected_det_firstdeterminanthsc) = (ff_column_mdm_prefix_mdr_selected_det_firstdeterminanthscm_positive)) /\ ff_column_mdm_cell_mdr_selected_det_firstdeterminanthscm_positive_cell = S ff_column_mdm_prefix_mdr_selected_det_firstdeterminanthscm_positive))) /\ (((exists ff_h_mdm_mdr_selected_det_firstdeterminanthscm_positive_cell_source. ff_h_mdm_mdr_selected_det_firstdeterminanthscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_selected_det_firstdeterminanthscm_positive) = S ((S ((ff_row_mdm_cell_mdr_selected_det_firstdeterminanthscm_positive_cell) * (S (mdr_q_selected_det_firstdeterminanths)) + (ff_column_mdm_cell_mdr_selected_det_firstdeterminanthscm_positive_cell))) * mdr_pc_selected_det_firstdeterminanth)) /\ exists ff_q_mdm_mdr_selected_det_firstdeterminanthscm_positive_cell_source. mdr_pb_selected_det_firstdeterminanth = ff_q_mdm_mdr_selected_det_firstdeterminanthscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_selected_det_firstdeterminanthscm_positive_cell) * (S (mdr_q_selected_det_firstdeterminanths)) + (ff_column_mdm_cell_mdr_selected_det_firstdeterminanthscm_positive_cell))) * mdr_pc_selected_det_firstdeterminanth) + (ff_value_mdm_prefix_mdr_selected_det_firstdeterminanthscm_positive)))))) /\ (((exists ff_h_mdm_mdr_selected_det_firstdeterminanthscm_positive_target. ff_h_mdm_mdr_selected_det_firstdeterminanthscm_positive_target + S (ff_value_mdm_prefix_mdr_selected_det_firstdeterminanthscm_positive) = S ((S (ff_index_mdm_prefix_mdr_selected_det_firstdeterminanthscm_positive)) * mdr_us_selected_det_firstdeterminanthsc)) /\ exists ff_q_mdm_mdr_selected_det_firstdeterminanthscm_positive_target. mdr_up_selected_det_firstdeterminanthsc = ff_q_mdm_mdr_selected_det_firstdeterminanthscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_selected_det_firstdeterminanthscm_positive)) * mdr_us_selected_det_firstdeterminanthsc) + (ff_value_mdm_prefix_mdr_selected_det_firstdeterminanthscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_selected_det_firstdeterminanthscm_negative. (exists ff_gap_mdm_lt_mdr_selected_det_firstdeterminanthscm_negative_index_bound. ff_gap_mdm_lt_mdr_selected_det_firstdeterminanthscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_selected_det_firstdeterminanthscm_negative) = ((mdr_q_selected_det_firstdeterminanths) * (mdr_q_selected_det_firstdeterminanths))) -> exists ff_row_mdm_prefix_mdr_selected_det_firstdeterminanthscm_negative ff_column_mdm_prefix_mdr_selected_det_firstdeterminanthscm_negative ff_value_mdm_prefix_mdr_selected_det_firstdeterminanthscm_negative. (ff_index_mdm_prefix_mdr_selected_det_firstdeterminanthscm_negative = (mdr_q_selected_det_firstdeterminanths) * ff_row_mdm_prefix_mdr_selected_det_firstdeterminanthscm_negative + ff_column_mdm_prefix_mdr_selected_det_firstdeterminanthscm_negative /\ ((exists ff_gap_mdm_lt_mdr_selected_det_firstdeterminanthscm_negative_column_bound. ff_gap_mdm_lt_mdr_selected_det_firstdeterminanthscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_selected_det_firstdeterminanthscm_negative) = (mdr_q_selected_det_firstdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_selected_det_firstdeterminanthscm_negative_cell ff_column_mdm_cell_mdr_selected_det_firstdeterminanthscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_selected_det_firstdeterminanthscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_selected_det_firstdeterminanthscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_selected_det_firstdeterminanthscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_selected_det_firstdeterminanthscm_negative_cell = ff_row_mdm_prefix_mdr_selected_det_firstdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_selected_det_firstdeterminanthscm_negative_cell_row_after. ff_gap_mdm_le_mdr_selected_det_firstdeterminanthscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_selected_det_firstdeterminanthscm_negative)) /\ ff_row_mdm_cell_mdr_selected_det_firstdeterminanthscm_negative_cell = S ff_row_mdm_prefix_mdr_selected_det_firstdeterminanthscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_selected_det_firstdeterminanthscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_selected_det_firstdeterminanthscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_selected_det_firstdeterminanthscm_negative) = (mdr_j_selected_det_firstdeterminanthsc)) /\ ff_column_mdm_cell_mdr_selected_det_firstdeterminanthscm_negative_cell = ff_column_mdm_prefix_mdr_selected_det_firstdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_selected_det_firstdeterminanthscm_negative_cell_column_after. ff_gap_mdm_le_mdr_selected_det_firstdeterminanthscm_negative_cell_column_after + (mdr_j_selected_det_firstdeterminanthsc) = (ff_column_mdm_prefix_mdr_selected_det_firstdeterminanthscm_negative)) /\ ff_column_mdm_cell_mdr_selected_det_firstdeterminanthscm_negative_cell = S ff_column_mdm_prefix_mdr_selected_det_firstdeterminanthscm_negative))) /\ (((exists ff_h_mdm_mdr_selected_det_firstdeterminanthscm_negative_cell_source. ff_h_mdm_mdr_selected_det_firstdeterminanthscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_selected_det_firstdeterminanthscm_negative) = S ((S ((ff_row_mdm_cell_mdr_selected_det_firstdeterminanthscm_negative_cell) * (S (mdr_q_selected_det_firstdeterminanths)) + (ff_column_mdm_cell_mdr_selected_det_firstdeterminanthscm_negative_cell))) * mdr_nc_selected_det_firstdeterminanth)) /\ exists ff_q_mdm_mdr_selected_det_firstdeterminanthscm_negative_cell_source. mdr_nb_selected_det_firstdeterminanth = ff_q_mdm_mdr_selected_det_firstdeterminanthscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_selected_det_firstdeterminanthscm_negative_cell) * (S (mdr_q_selected_det_firstdeterminanths)) + (ff_column_mdm_cell_mdr_selected_det_firstdeterminanthscm_negative_cell))) * mdr_nc_selected_det_firstdeterminanth) + (ff_value_mdm_prefix_mdr_selected_det_firstdeterminanthscm_negative)))))) /\ (((exists ff_h_mdm_mdr_selected_det_firstdeterminanthscm_negative_target. ff_h_mdm_mdr_selected_det_firstdeterminanthscm_negative_target + S (ff_value_mdm_prefix_mdr_selected_det_firstdeterminanthscm_negative) = S ((S (ff_index_mdm_prefix_mdr_selected_det_firstdeterminanthscm_negative)) * mdr_ut_selected_det_firstdeterminanthsc)) /\ exists ff_q_mdm_mdr_selected_det_firstdeterminanthscm_negative_target. mdr_un_selected_det_firstdeterminanthsc = ff_q_mdm_mdr_selected_det_firstdeterminanthscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_selected_det_firstdeterminanthscm_negative)) * mdr_ut_selected_det_firstdeterminanthsc) + (ff_value_mdm_prefix_mdr_selected_det_firstdeterminanthscm_negative))))))))) /\ ((((exists ff_h_mdr_selected_det_firstdeterminanthscp. ff_h_mdr_selected_det_firstdeterminanthscp + S (mdr_p_selected_det_firstdeterminanthsc) = S ((S (mdr_j_selected_det_firstdeterminanthsc)) * mdr_ec_selected_det_firstdeterminanths)) /\ exists ff_q_mdr_selected_det_firstdeterminanthscp. mdr_eb_selected_det_firstdeterminanths = ff_q_mdr_selected_det_firstdeterminanthscp * S ((S (mdr_j_selected_det_firstdeterminanthsc)) * mdr_ec_selected_det_firstdeterminanths) + (mdr_p_selected_det_firstdeterminanthsc))) /\ (((exists ff_h_mdr_selected_det_firstdeterminanthscn. ff_h_mdr_selected_det_firstdeterminanthscn + S (mdr_n_selected_det_firstdeterminanthsc) = S ((S (mdr_j_selected_det_firstdeterminanthsc)) * mdr_fc_selected_det_firstdeterminanths)) /\ exists ff_q_mdr_selected_det_firstdeterminanthscn. mdr_fb_selected_det_firstdeterminanths = ff_q_mdr_selected_det_firstdeterminanthscn * S ((S (mdr_j_selected_det_firstdeterminanthsc)) * mdr_fc_selected_det_firstdeterminanths) + (mdr_n_selected_det_firstdeterminanthsc)))))))) /\ (exists ff_ub_mce_fold_mdr_selected_det_firstdeterminanthsf ff_uc_mce_fold_mdr_selected_det_firstdeterminanthsf ff_vb_mce_fold_mdr_selected_det_firstdeterminanthsf ff_vc_mce_fold_mdr_selected_det_firstdeterminanthsf. ((forall ff_index_mce_alternating_mdr_selected_det_firstdeterminanthsf_prefix. (exists ff_gap_mce_mdr_selected_det_firstdeterminanthsf_prefix_index. ff_gap_mce_mdr_selected_det_firstdeterminanthsf_prefix_index + S (ff_index_mce_alternating_mdr_selected_det_firstdeterminanthsf_prefix) = (S (mdr_q_selected_det_firstdeterminanths))) -> exists ff_ap_mce_alternating_mdr_selected_det_firstdeterminanthsf_prefix ff_an_mce_alternating_mdr_selected_det_firstdeterminanthsf_prefix ff_bp_mce_alternating_mdr_selected_det_firstdeterminanthsf_prefix ff_bn_mce_alternating_mdr_selected_det_firstdeterminanthsf_prefix ff_p_mce_alternating_mdr_selected_det_firstdeterminanthsf_prefix ff_n_mce_alternating_mdr_selected_det_firstdeterminanthsf_prefix. ((((exists ff_h_mce_mdr_selected_det_firstdeterminanthsf_prefix_ap. ff_h_mce_mdr_selected_det_firstdeterminanthsf_prefix_ap + S (ff_ap_mce_alternating_mdr_selected_det_firstdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_selected_det_firstdeterminanthsf_prefix)) * mdr_pc_selected_det_firstdeterminanth)) /\ exists ff_q_mce_mdr_selected_det_firstdeterminanthsf_prefix_ap. mdr_pb_selected_det_firstdeterminanth = ff_q_mce_mdr_selected_det_firstdeterminanthsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_selected_det_firstdeterminanthsf_prefix)) * mdr_pc_selected_det_firstdeterminanth) + (ff_ap_mce_alternating_mdr_selected_det_firstdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_selected_det_firstdeterminanthsf_prefix_an. ff_h_mce_mdr_selected_det_firstdeterminanthsf_prefix_an + S (ff_an_mce_alternating_mdr_selected_det_firstdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_selected_det_firstdeterminanthsf_prefix)) * mdr_nc_selected_det_firstdeterminanth)) /\ exists ff_q_mce_mdr_selected_det_firstdeterminanthsf_prefix_an. mdr_nb_selected_det_firstdeterminanth = ff_q_mce_mdr_selected_det_firstdeterminanthsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_selected_det_firstdeterminanthsf_prefix)) * mdr_nc_selected_det_firstdeterminanth) + (ff_an_mce_alternating_mdr_selected_det_firstdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_selected_det_firstdeterminanthsf_prefix_bp. ff_h_mce_mdr_selected_det_firstdeterminanthsf_prefix_bp + S (ff_bp_mce_alternating_mdr_selected_det_firstdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_selected_det_firstdeterminanthsf_prefix)) * mdr_ec_selected_det_firstdeterminanths)) /\ exists ff_q_mce_mdr_selected_det_firstdeterminanthsf_prefix_bp. mdr_eb_selected_det_firstdeterminanths = ff_q_mce_mdr_selected_det_firstdeterminanthsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_selected_det_firstdeterminanthsf_prefix)) * mdr_ec_selected_det_firstdeterminanths) + (ff_bp_mce_alternating_mdr_selected_det_firstdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_selected_det_firstdeterminanthsf_prefix_bn. ff_h_mce_mdr_selected_det_firstdeterminanthsf_prefix_bn + S (ff_bn_mce_alternating_mdr_selected_det_firstdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_selected_det_firstdeterminanthsf_prefix)) * mdr_fc_selected_det_firstdeterminanths)) /\ exists ff_q_mce_mdr_selected_det_firstdeterminanthsf_prefix_bn. mdr_fb_selected_det_firstdeterminanths = ff_q_mce_mdr_selected_det_firstdeterminanthsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_selected_det_firstdeterminanthsf_prefix)) * mdr_fc_selected_det_firstdeterminanths) + (ff_bn_mce_alternating_mdr_selected_det_firstdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_selected_det_firstdeterminanthsf_prefix_positive. ff_h_mce_mdr_selected_det_firstdeterminanthsf_prefix_positive + S (ff_p_mce_alternating_mdr_selected_det_firstdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_selected_det_firstdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_selected_det_firstdeterminanthsf)) /\ exists ff_q_mce_mdr_selected_det_firstdeterminanthsf_prefix_positive. ff_ub_mce_fold_mdr_selected_det_firstdeterminanthsf = ff_q_mce_mdr_selected_det_firstdeterminanthsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_selected_det_firstdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_selected_det_firstdeterminanthsf) + (ff_p_mce_alternating_mdr_selected_det_firstdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_selected_det_firstdeterminanthsf_prefix_negative. ff_h_mce_mdr_selected_det_firstdeterminanthsf_prefix_negative + S (ff_n_mce_alternating_mdr_selected_det_firstdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_selected_det_firstdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_selected_det_firstdeterminanthsf)) /\ exists ff_q_mce_mdr_selected_det_firstdeterminanthsf_prefix_negative. ff_vb_mce_fold_mdr_selected_det_firstdeterminanthsf = ff_q_mce_mdr_selected_det_firstdeterminanthsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_selected_det_firstdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_selected_det_firstdeterminanthsf) + (ff_n_mce_alternating_mdr_selected_det_firstdeterminanthsf_prefix))) /\ (((exists ff_even_mce_term_mdr_selected_det_firstdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_selected_det_firstdeterminanthsf_prefix = 2 * ff_even_mce_term_mdr_selected_det_firstdeterminanthsf_prefix_term) /\ (ff_p_mce_alternating_mdr_selected_det_firstdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_selected_det_firstdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_selected_det_firstdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_selected_det_firstdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_selected_det_firstdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_selected_det_firstdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_selected_det_firstdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_selected_det_firstdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_selected_det_firstdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_selected_det_firstdeterminanthsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_selected_det_firstdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_selected_det_firstdeterminanthsf_prefix = 2 * ff_odd_mce_term_mdr_selected_det_firstdeterminanthsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_selected_det_firstdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_selected_det_firstdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_selected_det_firstdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_selected_det_firstdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_selected_det_firstdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_selected_det_firstdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_selected_det_firstdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_selected_det_firstdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_selected_det_firstdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_selected_det_firstdeterminanthsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_selected_det_firstdeterminanthsf_positive ff_v_mce_mdr_selected_det_firstdeterminanthsf_positive. ((((exists ff_h_mce_mdr_selected_det_firstdeterminanthsf_positive_start. ff_h_mce_mdr_selected_det_firstdeterminanthsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_selected_det_firstdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_selected_det_firstdeterminanthsf_positive_start. ff_u_mce_mdr_selected_det_firstdeterminanthsf_positive = ff_q_mce_mdr_selected_det_firstdeterminanthsf_positive_start * S ((S (0)) * ff_v_mce_mdr_selected_det_firstdeterminanthsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_selected_det_firstdeterminanthsf_positive_terminal. ff_h_mce_mdr_selected_det_firstdeterminanthsf_positive_terminal + S (mdr_p_selected_det_firstdeterminanth) = S ((S ((S (mdr_q_selected_det_firstdeterminanths)))) * ff_v_mce_mdr_selected_det_firstdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_selected_det_firstdeterminanthsf_positive_terminal. ff_u_mce_mdr_selected_det_firstdeterminanthsf_positive = ff_q_mce_mdr_selected_det_firstdeterminanthsf_positive_terminal * S ((S ((S (mdr_q_selected_det_firstdeterminanths)))) * ff_v_mce_mdr_selected_det_firstdeterminanthsf_positive) + (mdr_p_selected_det_firstdeterminanth))) /\ forall ff_i_mce_mdr_selected_det_firstdeterminanthsf_positive. (exists ff_lt_mce_mdr_selected_det_firstdeterminanthsf_positive_bound. ff_lt_mce_mdr_selected_det_firstdeterminanthsf_positive_bound + S ff_i_mce_mdr_selected_det_firstdeterminanthsf_positive = (S (mdr_q_selected_det_firstdeterminanths))) -> exists ff_a_mce_mdr_selected_det_firstdeterminanthsf_positive ff_r_mce_mdr_selected_det_firstdeterminanthsf_positive ff_s_mce_mdr_selected_det_firstdeterminanthsf_positive. ((((exists ff_h_mce_mdr_selected_det_firstdeterminanthsf_positive_summand. ff_h_mce_mdr_selected_det_firstdeterminanthsf_positive_summand + S (ff_a_mce_mdr_selected_det_firstdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_selected_det_firstdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_selected_det_firstdeterminanthsf)) /\ exists ff_q_mce_mdr_selected_det_firstdeterminanthsf_positive_summand. ff_ub_mce_fold_mdr_selected_det_firstdeterminanthsf = ff_q_mce_mdr_selected_det_firstdeterminanthsf_positive_summand * S ((S (ff_i_mce_mdr_selected_det_firstdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_selected_det_firstdeterminanthsf) + (ff_a_mce_mdr_selected_det_firstdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_selected_det_firstdeterminanthsf_positive_partial. ff_h_mce_mdr_selected_det_firstdeterminanthsf_positive_partial + S (ff_r_mce_mdr_selected_det_firstdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_selected_det_firstdeterminanthsf_positive)) * ff_v_mce_mdr_selected_det_firstdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_selected_det_firstdeterminanthsf_positive_partial. ff_u_mce_mdr_selected_det_firstdeterminanthsf_positive = ff_q_mce_mdr_selected_det_firstdeterminanthsf_positive_partial * S ((S (ff_i_mce_mdr_selected_det_firstdeterminanthsf_positive)) * ff_v_mce_mdr_selected_det_firstdeterminanthsf_positive) + (ff_r_mce_mdr_selected_det_firstdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_selected_det_firstdeterminanthsf_positive_successor. ff_h_mce_mdr_selected_det_firstdeterminanthsf_positive_successor + S (ff_s_mce_mdr_selected_det_firstdeterminanthsf_positive) = S ((S (S ff_i_mce_mdr_selected_det_firstdeterminanthsf_positive)) * ff_v_mce_mdr_selected_det_firstdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_selected_det_firstdeterminanthsf_positive_successor. ff_u_mce_mdr_selected_det_firstdeterminanthsf_positive = ff_q_mce_mdr_selected_det_firstdeterminanthsf_positive_successor * S ((S (S ff_i_mce_mdr_selected_det_firstdeterminanthsf_positive)) * ff_v_mce_mdr_selected_det_firstdeterminanthsf_positive) + (ff_s_mce_mdr_selected_det_firstdeterminanthsf_positive))) /\ ff_s_mce_mdr_selected_det_firstdeterminanthsf_positive = ff_r_mce_mdr_selected_det_firstdeterminanthsf_positive + ff_a_mce_mdr_selected_det_firstdeterminanthsf_positive)))))) /\ (exists ff_u_mce_mdr_selected_det_firstdeterminanthsf_negative ff_v_mce_mdr_selected_det_firstdeterminanthsf_negative. ((((exists ff_h_mce_mdr_selected_det_firstdeterminanthsf_negative_start. ff_h_mce_mdr_selected_det_firstdeterminanthsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_selected_det_firstdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_selected_det_firstdeterminanthsf_negative_start. ff_u_mce_mdr_selected_det_firstdeterminanthsf_negative = ff_q_mce_mdr_selected_det_firstdeterminanthsf_negative_start * S ((S (0)) * ff_v_mce_mdr_selected_det_firstdeterminanthsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_selected_det_firstdeterminanthsf_negative_terminal. ff_h_mce_mdr_selected_det_firstdeterminanthsf_negative_terminal + S (mdr_n_selected_det_firstdeterminanth) = S ((S ((S (mdr_q_selected_det_firstdeterminanths)))) * ff_v_mce_mdr_selected_det_firstdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_selected_det_firstdeterminanthsf_negative_terminal. ff_u_mce_mdr_selected_det_firstdeterminanthsf_negative = ff_q_mce_mdr_selected_det_firstdeterminanthsf_negative_terminal * S ((S ((S (mdr_q_selected_det_firstdeterminanths)))) * ff_v_mce_mdr_selected_det_firstdeterminanthsf_negative) + (mdr_n_selected_det_firstdeterminanth))) /\ forall ff_i_mce_mdr_selected_det_firstdeterminanthsf_negative. (exists ff_lt_mce_mdr_selected_det_firstdeterminanthsf_negative_bound. ff_lt_mce_mdr_selected_det_firstdeterminanthsf_negative_bound + S ff_i_mce_mdr_selected_det_firstdeterminanthsf_negative = (S (mdr_q_selected_det_firstdeterminanths))) -> exists ff_a_mce_mdr_selected_det_firstdeterminanthsf_negative ff_r_mce_mdr_selected_det_firstdeterminanthsf_negative ff_s_mce_mdr_selected_det_firstdeterminanthsf_negative. ((((exists ff_h_mce_mdr_selected_det_firstdeterminanthsf_negative_summand. ff_h_mce_mdr_selected_det_firstdeterminanthsf_negative_summand + S (ff_a_mce_mdr_selected_det_firstdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_selected_det_firstdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_selected_det_firstdeterminanthsf)) /\ exists ff_q_mce_mdr_selected_det_firstdeterminanthsf_negative_summand. ff_vb_mce_fold_mdr_selected_det_firstdeterminanthsf = ff_q_mce_mdr_selected_det_firstdeterminanthsf_negative_summand * S ((S (ff_i_mce_mdr_selected_det_firstdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_selected_det_firstdeterminanthsf) + (ff_a_mce_mdr_selected_det_firstdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_selected_det_firstdeterminanthsf_negative_partial. ff_h_mce_mdr_selected_det_firstdeterminanthsf_negative_partial + S (ff_r_mce_mdr_selected_det_firstdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_selected_det_firstdeterminanthsf_negative)) * ff_v_mce_mdr_selected_det_firstdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_selected_det_firstdeterminanthsf_negative_partial. ff_u_mce_mdr_selected_det_firstdeterminanthsf_negative = ff_q_mce_mdr_selected_det_firstdeterminanthsf_negative_partial * S ((S (ff_i_mce_mdr_selected_det_firstdeterminanthsf_negative)) * ff_v_mce_mdr_selected_det_firstdeterminanthsf_negative) + (ff_r_mce_mdr_selected_det_firstdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_selected_det_firstdeterminanthsf_negative_successor. ff_h_mce_mdr_selected_det_firstdeterminanthsf_negative_successor + S (ff_s_mce_mdr_selected_det_firstdeterminanthsf_negative) = S ((S (S ff_i_mce_mdr_selected_det_firstdeterminanthsf_negative)) * ff_v_mce_mdr_selected_det_firstdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_selected_det_firstdeterminanthsf_negative_successor. ff_u_mce_mdr_selected_det_firstdeterminanthsf_negative = ff_q_mce_mdr_selected_det_firstdeterminanthsf_negative_successor * S ((S (S ff_i_mce_mdr_selected_det_firstdeterminanthsf_negative)) * ff_v_mce_mdr_selected_det_firstdeterminanthsf_negative) + (ff_s_mce_mdr_selected_det_firstdeterminanthsf_negative))) /\ ff_s_mce_mdr_selected_det_firstdeterminanthsf_negative = ff_r_mce_mdr_selected_det_firstdeterminanthsf_negative + ff_a_mce_mdr_selected_det_firstdeterminanthsf_negative))))))))))))))) /\ ((exists mdr_gap_selected_det_firstdeterminanti. mdr_gap_selected_det_firstdeterminanti + S (mdr_i_selected_det_firstdeterminant) = (mdr_l_selected_det_firstdeterminant)) /\ (exists mdr_z_selected_det_firstdeterminantr. ((exists mdr_a_selected_det_firstdeterminantrc mdr_b_selected_det_firstdeterminantrc mdr_c_selected_det_firstdeterminantrc mdr_e_selected_det_firstdeterminantrc mdr_f_selected_det_firstdeterminantrc. ((mdr_a_selected_det_firstdeterminantrc = ((q) + (mdr_ub_selected_det_first)) * S ((q) + (mdr_ub_selected_det_first)) + ((mdr_ub_selected_det_first) + (mdr_ub_selected_det_first))) /\ ((mdr_b_selected_det_firstdeterminantrc = ((mdr_uc_selected_det_first) + (mdr_vb_selected_det_first)) * S ((mdr_uc_selected_det_first) + (mdr_vb_selected_det_first)) + ((mdr_vb_selected_det_first) + (mdr_vb_selected_det_first))) /\ ((mdr_c_selected_det_firstdeterminantrc = ((mdr_a_selected_det_firstdeterminantrc) + (mdr_b_selected_det_firstdeterminantrc)) * S ((mdr_a_selected_det_firstdeterminantrc) + (mdr_b_selected_det_firstdeterminantrc)) + ((mdr_b_selected_det_firstdeterminantrc) + (mdr_b_selected_det_firstdeterminantrc))) /\ ((mdr_e_selected_det_firstdeterminantrc = ((p) + (n)) * S ((p) + (n)) + ((n) + (n))) /\ ((mdr_f_selected_det_firstdeterminantrc = ((mdr_vc_selected_det_first) + (mdr_e_selected_det_firstdeterminantrc)) * S ((mdr_vc_selected_det_first) + (mdr_e_selected_det_firstdeterminantrc)) + ((mdr_e_selected_det_firstdeterminantrc) + (mdr_e_selected_det_firstdeterminantrc))) /\ ((mdr_z_selected_det_firstdeterminantr) = ((mdr_c_selected_det_firstdeterminantrc) + (mdr_f_selected_det_firstdeterminantrc)) * S ((mdr_c_selected_det_firstdeterminantrc) + (mdr_f_selected_det_firstdeterminantrc)) + ((mdr_f_selected_det_firstdeterminantrc) + (mdr_f_selected_det_firstdeterminantrc))))))))) /\ (((exists ff_h_mdr_selected_det_firstdeterminantrb. ff_h_mdr_selected_det_firstdeterminantrb + S (mdr_z_selected_det_firstdeterminantr) = S ((S (mdr_i_selected_det_firstdeterminant)) * mdr_c_selected_det_firstdeterminant)) /\ exists ff_q_mdr_selected_det_firstdeterminantrb. mdr_b_selected_det_firstdeterminant = ff_q_mdr_selected_det_firstdeterminantrb * S ((S (mdr_i_selected_det_firstdeterminant)) * mdr_c_selected_det_firstdeterminant) + (mdr_z_selected_det_firstdeterminantr)))))))))) -> (exists mdr_ub_selected_det_second mdr_uc_selected_det_second mdr_vb_selected_det_second mdr_vc_selected_det_second. ((((forall mdr_i_selected_det_secondmatrixpositive. (exists mdr_gap_selected_det_secondmatrixpositivebound. mdr_gap_selected_det_secondmatrixpositivebound + S (mdr_i_selected_det_secondmatrixpositive) = ((q) * (q))) -> exists mdr_a_selected_det_secondmatrixpositive. (((exists mdr_r_selected_det_secondmatrixpositivepoint mdr_s_selected_det_secondmatrixpositivepoint mdr_u_selected_det_secondmatrixpositivepoint mdr_v_selected_det_secondmatrixpositivepoint. ((mdr_i_selected_det_secondmatrixpositive = (q) * mdr_r_selected_det_secondmatrixpositivepoint + mdr_s_selected_det_secondmatrixpositivepoint) /\ ((exists mdr_gap_selected_det_secondmatrixpositivepointcolumn. mdr_gap_selected_det_secondmatrixpositivepointcolumn + S (mdr_s_selected_det_secondmatrixpositivepoint) = (q)) /\ ((((exists ff_h_mdr_selected_det_secondmatrixpositivepointrow_index. ff_h_mdr_selected_det_secondmatrixpositivepointrow_index + S (mdr_u_selected_det_secondmatrixpositivepoint) = S ((S (mdr_r_selected_det_secondmatrixpositivepoint)) * rc)) /\ exists ff_q_mdr_selected_det_secondmatrixpositivepointrow_index. rb = ff_q_mdr_selected_det_secondmatrixpositivepointrow_index * S ((S (mdr_r_selected_det_secondmatrixpositivepoint)) * rc) + (mdr_u_selected_det_secondmatrixpositivepoint))) /\ ((((exists ff_h_mdr_selected_det_secondmatrixpositivepointcolumn_index. ff_h_mdr_selected_det_secondmatrixpositivepointcolumn_index + S (mdr_v_selected_det_secondmatrixpositivepoint) = S ((S (mdr_s_selected_det_secondmatrixpositivepoint)) * cc)) /\ exists ff_q_mdr_selected_det_secondmatrixpositivepointcolumn_index. cb = ff_q_mdr_selected_det_secondmatrixpositivepointcolumn_index * S ((S (mdr_s_selected_det_secondmatrixpositivepoint)) * cc) + (mdr_v_selected_det_secondmatrixpositivepoint))) /\ (((exists ff_h_mdr_selected_det_secondmatrixpositivepointsource. ff_h_mdr_selected_det_secondmatrixpositivepointsource + S (mdr_a_selected_det_secondmatrixpositive) = S ((S ((mdr_u_selected_det_secondmatrixpositivepoint) * (w) + (mdr_v_selected_det_secondmatrixpositivepoint))) * pc)) /\ exists ff_q_mdr_selected_det_secondmatrixpositivepointsource. pb = ff_q_mdr_selected_det_secondmatrixpositivepointsource * S ((S ((mdr_u_selected_det_secondmatrixpositivepoint) * (w) + (mdr_v_selected_det_secondmatrixpositivepoint))) * pc) + (mdr_a_selected_det_secondmatrixpositive)))))))) /\ (((exists ff_h_mdr_selected_det_secondmatrixpositiveoutput. ff_h_mdr_selected_det_secondmatrixpositiveoutput + S (mdr_a_selected_det_secondmatrixpositive) = S ((S (mdr_i_selected_det_secondmatrixpositive)) * mdr_uc_selected_det_second)) /\ exists ff_q_mdr_selected_det_secondmatrixpositiveoutput. mdr_ub_selected_det_second = ff_q_mdr_selected_det_secondmatrixpositiveoutput * S ((S (mdr_i_selected_det_secondmatrixpositive)) * mdr_uc_selected_det_second) + (mdr_a_selected_det_secondmatrixpositive)))))) /\ (forall mdr_i_selected_det_secondmatrixnegative. (exists mdr_gap_selected_det_secondmatrixnegativebound. mdr_gap_selected_det_secondmatrixnegativebound + S (mdr_i_selected_det_secondmatrixnegative) = ((q) * (q))) -> exists mdr_a_selected_det_secondmatrixnegative. (((exists mdr_r_selected_det_secondmatrixnegativepoint mdr_s_selected_det_secondmatrixnegativepoint mdr_u_selected_det_secondmatrixnegativepoint mdr_v_selected_det_secondmatrixnegativepoint. ((mdr_i_selected_det_secondmatrixnegative = (q) * mdr_r_selected_det_secondmatrixnegativepoint + mdr_s_selected_det_secondmatrixnegativepoint) /\ ((exists mdr_gap_selected_det_secondmatrixnegativepointcolumn. mdr_gap_selected_det_secondmatrixnegativepointcolumn + S (mdr_s_selected_det_secondmatrixnegativepoint) = (q)) /\ ((((exists ff_h_mdr_selected_det_secondmatrixnegativepointrow_index. ff_h_mdr_selected_det_secondmatrixnegativepointrow_index + S (mdr_u_selected_det_secondmatrixnegativepoint) = S ((S (mdr_r_selected_det_secondmatrixnegativepoint)) * rc)) /\ exists ff_q_mdr_selected_det_secondmatrixnegativepointrow_index. rb = ff_q_mdr_selected_det_secondmatrixnegativepointrow_index * S ((S (mdr_r_selected_det_secondmatrixnegativepoint)) * rc) + (mdr_u_selected_det_secondmatrixnegativepoint))) /\ ((((exists ff_h_mdr_selected_det_secondmatrixnegativepointcolumn_index. ff_h_mdr_selected_det_secondmatrixnegativepointcolumn_index + S (mdr_v_selected_det_secondmatrixnegativepoint) = S ((S (mdr_s_selected_det_secondmatrixnegativepoint)) * cc)) /\ exists ff_q_mdr_selected_det_secondmatrixnegativepointcolumn_index. cb = ff_q_mdr_selected_det_secondmatrixnegativepointcolumn_index * S ((S (mdr_s_selected_det_secondmatrixnegativepoint)) * cc) + (mdr_v_selected_det_secondmatrixnegativepoint))) /\ (((exists ff_h_mdr_selected_det_secondmatrixnegativepointsource. ff_h_mdr_selected_det_secondmatrixnegativepointsource + S (mdr_a_selected_det_secondmatrixnegative) = S ((S ((mdr_u_selected_det_secondmatrixnegativepoint) * (w) + (mdr_v_selected_det_secondmatrixnegativepoint))) * nc)) /\ exists ff_q_mdr_selected_det_secondmatrixnegativepointsource. nb = ff_q_mdr_selected_det_secondmatrixnegativepointsource * S ((S ((mdr_u_selected_det_secondmatrixnegativepoint) * (w) + (mdr_v_selected_det_secondmatrixnegativepoint))) * nc) + (mdr_a_selected_det_secondmatrixnegative)))))))) /\ (((exists ff_h_mdr_selected_det_secondmatrixnegativeoutput. ff_h_mdr_selected_det_secondmatrixnegativeoutput + S (mdr_a_selected_det_secondmatrixnegative) = S ((S (mdr_i_selected_det_secondmatrixnegative)) * mdr_vc_selected_det_second)) /\ exists ff_q_mdr_selected_det_secondmatrixnegativeoutput. mdr_vb_selected_det_second = ff_q_mdr_selected_det_secondmatrixnegativeoutput * S ((S (mdr_i_selected_det_secondmatrixnegative)) * mdr_vc_selected_det_second) + (mdr_a_selected_det_secondmatrixnegative)))))))) /\ (exists mdr_b_selected_det_seconddeterminant mdr_c_selected_det_seconddeterminant mdr_l_selected_det_seconddeterminant mdr_i_selected_det_seconddeterminant. ((forall mdr_i_selected_det_seconddeterminanth. (exists mdr_gap_selected_det_seconddeterminanthi. mdr_gap_selected_det_seconddeterminanthi + S (mdr_i_selected_det_seconddeterminanth) = (mdr_l_selected_det_seconddeterminant)) -> exists mdr_d_selected_det_seconddeterminanth mdr_pb_selected_det_seconddeterminanth mdr_pc_selected_det_seconddeterminanth mdr_nb_selected_det_seconddeterminanth mdr_nc_selected_det_seconddeterminanth mdr_p_selected_det_seconddeterminanth mdr_n_selected_det_seconddeterminanth. ((exists mdr_z_selected_det_seconddeterminanthr. ((exists mdr_a_selected_det_seconddeterminanthrc mdr_b_selected_det_seconddeterminanthrc mdr_c_selected_det_seconddeterminanthrc mdr_e_selected_det_seconddeterminanthrc mdr_f_selected_det_seconddeterminanthrc. ((mdr_a_selected_det_seconddeterminanthrc = ((mdr_d_selected_det_seconddeterminanth) + (mdr_pb_selected_det_seconddeterminanth)) * S ((mdr_d_selected_det_seconddeterminanth) + (mdr_pb_selected_det_seconddeterminanth)) + ((mdr_pb_selected_det_seconddeterminanth) + (mdr_pb_selected_det_seconddeterminanth))) /\ ((mdr_b_selected_det_seconddeterminanthrc = ((mdr_pc_selected_det_seconddeterminanth) + (mdr_nb_selected_det_seconddeterminanth)) * S ((mdr_pc_selected_det_seconddeterminanth) + (mdr_nb_selected_det_seconddeterminanth)) + ((mdr_nb_selected_det_seconddeterminanth) + (mdr_nb_selected_det_seconddeterminanth))) /\ ((mdr_c_selected_det_seconddeterminanthrc = ((mdr_a_selected_det_seconddeterminanthrc) + (mdr_b_selected_det_seconddeterminanthrc)) * S ((mdr_a_selected_det_seconddeterminanthrc) + (mdr_b_selected_det_seconddeterminanthrc)) + ((mdr_b_selected_det_seconddeterminanthrc) + (mdr_b_selected_det_seconddeterminanthrc))) /\ ((mdr_e_selected_det_seconddeterminanthrc = ((mdr_p_selected_det_seconddeterminanth) + (mdr_n_selected_det_seconddeterminanth)) * S ((mdr_p_selected_det_seconddeterminanth) + (mdr_n_selected_det_seconddeterminanth)) + ((mdr_n_selected_det_seconddeterminanth) + (mdr_n_selected_det_seconddeterminanth))) /\ ((mdr_f_selected_det_seconddeterminanthrc = ((mdr_nc_selected_det_seconddeterminanth) + (mdr_e_selected_det_seconddeterminanthrc)) * S ((mdr_nc_selected_det_seconddeterminanth) + (mdr_e_selected_det_seconddeterminanthrc)) + ((mdr_e_selected_det_seconddeterminanthrc) + (mdr_e_selected_det_seconddeterminanthrc))) /\ ((mdr_z_selected_det_seconddeterminanthr) = ((mdr_c_selected_det_seconddeterminanthrc) + (mdr_f_selected_det_seconddeterminanthrc)) * S ((mdr_c_selected_det_seconddeterminanthrc) + (mdr_f_selected_det_seconddeterminanthrc)) + ((mdr_f_selected_det_seconddeterminanthrc) + (mdr_f_selected_det_seconddeterminanthrc))))))))) /\ (((exists ff_h_mdr_selected_det_seconddeterminanthrb. ff_h_mdr_selected_det_seconddeterminanthrb + S (mdr_z_selected_det_seconddeterminanthr) = S ((S (mdr_i_selected_det_seconddeterminanth)) * mdr_c_selected_det_seconddeterminant)) /\ exists ff_q_mdr_selected_det_seconddeterminanthrb. mdr_b_selected_det_seconddeterminant = ff_q_mdr_selected_det_seconddeterminanthrb * S ((S (mdr_i_selected_det_seconddeterminanth)) * mdr_c_selected_det_seconddeterminant) + (mdr_z_selected_det_seconddeterminanthr))))) /\ (((((mdr_d_selected_det_seconddeterminanth) = 0) /\ (((mdr_p_selected_det_seconddeterminanth) = 1) /\ ((mdr_n_selected_det_seconddeterminanth) = 0))) \/ exists mdr_q_selected_det_seconddeterminanths mdr_eb_selected_det_seconddeterminanths mdr_ec_selected_det_seconddeterminanths mdr_fb_selected_det_seconddeterminanths mdr_fc_selected_det_seconddeterminanths. (((mdr_d_selected_det_seconddeterminanth) = S (mdr_q_selected_det_seconddeterminanths)) /\ ((forall mdr_j_selected_det_seconddeterminanthsc. (exists mdr_gap_selected_det_seconddeterminanthscj. mdr_gap_selected_det_seconddeterminanthscj + S (mdr_j_selected_det_seconddeterminanthsc) = (S (mdr_q_selected_det_seconddeterminanths))) -> exists mdr_i_selected_det_seconddeterminanthsc mdr_up_selected_det_seconddeterminanthsc mdr_us_selected_det_seconddeterminanthsc mdr_un_selected_det_seconddeterminanthsc mdr_ut_selected_det_seconddeterminanthsc mdr_p_selected_det_seconddeterminanthsc mdr_n_selected_det_seconddeterminanthsc. ((exists mdr_gap_selected_det_seconddeterminanthsci. mdr_gap_selected_det_seconddeterminanthsci + S (mdr_i_selected_det_seconddeterminanthsc) = (mdr_i_selected_det_seconddeterminanth)) /\ ((exists mdr_z_selected_det_seconddeterminanthscr. ((exists mdr_a_selected_det_seconddeterminanthscrc mdr_b_selected_det_seconddeterminanthscrc mdr_c_selected_det_seconddeterminanthscrc mdr_e_selected_det_seconddeterminanthscrc mdr_f_selected_det_seconddeterminanthscrc. ((mdr_a_selected_det_seconddeterminanthscrc = ((mdr_q_selected_det_seconddeterminanths) + (mdr_up_selected_det_seconddeterminanthsc)) * S ((mdr_q_selected_det_seconddeterminanths) + (mdr_up_selected_det_seconddeterminanthsc)) + ((mdr_up_selected_det_seconddeterminanthsc) + (mdr_up_selected_det_seconddeterminanthsc))) /\ ((mdr_b_selected_det_seconddeterminanthscrc = ((mdr_us_selected_det_seconddeterminanthsc) + (mdr_un_selected_det_seconddeterminanthsc)) * S ((mdr_us_selected_det_seconddeterminanthsc) + (mdr_un_selected_det_seconddeterminanthsc)) + ((mdr_un_selected_det_seconddeterminanthsc) + (mdr_un_selected_det_seconddeterminanthsc))) /\ ((mdr_c_selected_det_seconddeterminanthscrc = ((mdr_a_selected_det_seconddeterminanthscrc) + (mdr_b_selected_det_seconddeterminanthscrc)) * S ((mdr_a_selected_det_seconddeterminanthscrc) + (mdr_b_selected_det_seconddeterminanthscrc)) + ((mdr_b_selected_det_seconddeterminanthscrc) + (mdr_b_selected_det_seconddeterminanthscrc))) /\ ((mdr_e_selected_det_seconddeterminanthscrc = ((mdr_p_selected_det_seconddeterminanthsc) + (mdr_n_selected_det_seconddeterminanthsc)) * S ((mdr_p_selected_det_seconddeterminanthsc) + (mdr_n_selected_det_seconddeterminanthsc)) + ((mdr_n_selected_det_seconddeterminanthsc) + (mdr_n_selected_det_seconddeterminanthsc))) /\ ((mdr_f_selected_det_seconddeterminanthscrc = ((mdr_ut_selected_det_seconddeterminanthsc) + (mdr_e_selected_det_seconddeterminanthscrc)) * S ((mdr_ut_selected_det_seconddeterminanthsc) + (mdr_e_selected_det_seconddeterminanthscrc)) + ((mdr_e_selected_det_seconddeterminanthscrc) + (mdr_e_selected_det_seconddeterminanthscrc))) /\ ((mdr_z_selected_det_seconddeterminanthscr) = ((mdr_c_selected_det_seconddeterminanthscrc) + (mdr_f_selected_det_seconddeterminanthscrc)) * S ((mdr_c_selected_det_seconddeterminanthscrc) + (mdr_f_selected_det_seconddeterminanthscrc)) + ((mdr_f_selected_det_seconddeterminanthscrc) + (mdr_f_selected_det_seconddeterminanthscrc))))))))) /\ (((exists ff_h_mdr_selected_det_seconddeterminanthscrb. ff_h_mdr_selected_det_seconddeterminanthscrb + S (mdr_z_selected_det_seconddeterminanthscr) = S ((S (mdr_i_selected_det_seconddeterminanthsc)) * mdr_c_selected_det_seconddeterminant)) /\ exists ff_q_mdr_selected_det_seconddeterminanthscrb. mdr_b_selected_det_seconddeterminant = ff_q_mdr_selected_det_seconddeterminanthscrb * S ((S (mdr_i_selected_det_seconddeterminanthsc)) * mdr_c_selected_det_seconddeterminant) + (mdr_z_selected_det_seconddeterminanthscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_selected_det_seconddeterminanthscm_positive. (exists ff_gap_mdm_lt_mdr_selected_det_seconddeterminanthscm_positive_index_bound. ff_gap_mdm_lt_mdr_selected_det_seconddeterminanthscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_selected_det_seconddeterminanthscm_positive) = ((mdr_q_selected_det_seconddeterminanths) * (mdr_q_selected_det_seconddeterminanths))) -> exists ff_row_mdm_prefix_mdr_selected_det_seconddeterminanthscm_positive ff_column_mdm_prefix_mdr_selected_det_seconddeterminanthscm_positive ff_value_mdm_prefix_mdr_selected_det_seconddeterminanthscm_positive. (ff_index_mdm_prefix_mdr_selected_det_seconddeterminanthscm_positive = (mdr_q_selected_det_seconddeterminanths) * ff_row_mdm_prefix_mdr_selected_det_seconddeterminanthscm_positive + ff_column_mdm_prefix_mdr_selected_det_seconddeterminanthscm_positive /\ ((exists ff_gap_mdm_lt_mdr_selected_det_seconddeterminanthscm_positive_column_bound. ff_gap_mdm_lt_mdr_selected_det_seconddeterminanthscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_selected_det_seconddeterminanthscm_positive) = (mdr_q_selected_det_seconddeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_selected_det_seconddeterminanthscm_positive_cell ff_column_mdm_cell_mdr_selected_det_seconddeterminanthscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_selected_det_seconddeterminanthscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_selected_det_seconddeterminanthscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_selected_det_seconddeterminanthscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_selected_det_seconddeterminanthscm_positive_cell = ff_row_mdm_prefix_mdr_selected_det_seconddeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_selected_det_seconddeterminanthscm_positive_cell_row_after. ff_gap_mdm_le_mdr_selected_det_seconddeterminanthscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_selected_det_seconddeterminanthscm_positive)) /\ ff_row_mdm_cell_mdr_selected_det_seconddeterminanthscm_positive_cell = S ff_row_mdm_prefix_mdr_selected_det_seconddeterminanthscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_selected_det_seconddeterminanthscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_selected_det_seconddeterminanthscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_selected_det_seconddeterminanthscm_positive) = (mdr_j_selected_det_seconddeterminanthsc)) /\ ff_column_mdm_cell_mdr_selected_det_seconddeterminanthscm_positive_cell = ff_column_mdm_prefix_mdr_selected_det_seconddeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_selected_det_seconddeterminanthscm_positive_cell_column_after. ff_gap_mdm_le_mdr_selected_det_seconddeterminanthscm_positive_cell_column_after + (mdr_j_selected_det_seconddeterminanthsc) = (ff_column_mdm_prefix_mdr_selected_det_seconddeterminanthscm_positive)) /\ ff_column_mdm_cell_mdr_selected_det_seconddeterminanthscm_positive_cell = S ff_column_mdm_prefix_mdr_selected_det_seconddeterminanthscm_positive))) /\ (((exists ff_h_mdm_mdr_selected_det_seconddeterminanthscm_positive_cell_source. ff_h_mdm_mdr_selected_det_seconddeterminanthscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_selected_det_seconddeterminanthscm_positive) = S ((S ((ff_row_mdm_cell_mdr_selected_det_seconddeterminanthscm_positive_cell) * (S (mdr_q_selected_det_seconddeterminanths)) + (ff_column_mdm_cell_mdr_selected_det_seconddeterminanthscm_positive_cell))) * mdr_pc_selected_det_seconddeterminanth)) /\ exists ff_q_mdm_mdr_selected_det_seconddeterminanthscm_positive_cell_source. mdr_pb_selected_det_seconddeterminanth = ff_q_mdm_mdr_selected_det_seconddeterminanthscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_selected_det_seconddeterminanthscm_positive_cell) * (S (mdr_q_selected_det_seconddeterminanths)) + (ff_column_mdm_cell_mdr_selected_det_seconddeterminanthscm_positive_cell))) * mdr_pc_selected_det_seconddeterminanth) + (ff_value_mdm_prefix_mdr_selected_det_seconddeterminanthscm_positive)))))) /\ (((exists ff_h_mdm_mdr_selected_det_seconddeterminanthscm_positive_target. ff_h_mdm_mdr_selected_det_seconddeterminanthscm_positive_target + S (ff_value_mdm_prefix_mdr_selected_det_seconddeterminanthscm_positive) = S ((S (ff_index_mdm_prefix_mdr_selected_det_seconddeterminanthscm_positive)) * mdr_us_selected_det_seconddeterminanthsc)) /\ exists ff_q_mdm_mdr_selected_det_seconddeterminanthscm_positive_target. mdr_up_selected_det_seconddeterminanthsc = ff_q_mdm_mdr_selected_det_seconddeterminanthscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_selected_det_seconddeterminanthscm_positive)) * mdr_us_selected_det_seconddeterminanthsc) + (ff_value_mdm_prefix_mdr_selected_det_seconddeterminanthscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_selected_det_seconddeterminanthscm_negative. (exists ff_gap_mdm_lt_mdr_selected_det_seconddeterminanthscm_negative_index_bound. ff_gap_mdm_lt_mdr_selected_det_seconddeterminanthscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_selected_det_seconddeterminanthscm_negative) = ((mdr_q_selected_det_seconddeterminanths) * (mdr_q_selected_det_seconddeterminanths))) -> exists ff_row_mdm_prefix_mdr_selected_det_seconddeterminanthscm_negative ff_column_mdm_prefix_mdr_selected_det_seconddeterminanthscm_negative ff_value_mdm_prefix_mdr_selected_det_seconddeterminanthscm_negative. (ff_index_mdm_prefix_mdr_selected_det_seconddeterminanthscm_negative = (mdr_q_selected_det_seconddeterminanths) * ff_row_mdm_prefix_mdr_selected_det_seconddeterminanthscm_negative + ff_column_mdm_prefix_mdr_selected_det_seconddeterminanthscm_negative /\ ((exists ff_gap_mdm_lt_mdr_selected_det_seconddeterminanthscm_negative_column_bound. ff_gap_mdm_lt_mdr_selected_det_seconddeterminanthscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_selected_det_seconddeterminanthscm_negative) = (mdr_q_selected_det_seconddeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_selected_det_seconddeterminanthscm_negative_cell ff_column_mdm_cell_mdr_selected_det_seconddeterminanthscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_selected_det_seconddeterminanthscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_selected_det_seconddeterminanthscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_selected_det_seconddeterminanthscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_selected_det_seconddeterminanthscm_negative_cell = ff_row_mdm_prefix_mdr_selected_det_seconddeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_selected_det_seconddeterminanthscm_negative_cell_row_after. ff_gap_mdm_le_mdr_selected_det_seconddeterminanthscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_selected_det_seconddeterminanthscm_negative)) /\ ff_row_mdm_cell_mdr_selected_det_seconddeterminanthscm_negative_cell = S ff_row_mdm_prefix_mdr_selected_det_seconddeterminanthscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_selected_det_seconddeterminanthscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_selected_det_seconddeterminanthscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_selected_det_seconddeterminanthscm_negative) = (mdr_j_selected_det_seconddeterminanthsc)) /\ ff_column_mdm_cell_mdr_selected_det_seconddeterminanthscm_negative_cell = ff_column_mdm_prefix_mdr_selected_det_seconddeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_selected_det_seconddeterminanthscm_negative_cell_column_after. ff_gap_mdm_le_mdr_selected_det_seconddeterminanthscm_negative_cell_column_after + (mdr_j_selected_det_seconddeterminanthsc) = (ff_column_mdm_prefix_mdr_selected_det_seconddeterminanthscm_negative)) /\ ff_column_mdm_cell_mdr_selected_det_seconddeterminanthscm_negative_cell = S ff_column_mdm_prefix_mdr_selected_det_seconddeterminanthscm_negative))) /\ (((exists ff_h_mdm_mdr_selected_det_seconddeterminanthscm_negative_cell_source. ff_h_mdm_mdr_selected_det_seconddeterminanthscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_selected_det_seconddeterminanthscm_negative) = S ((S ((ff_row_mdm_cell_mdr_selected_det_seconddeterminanthscm_negative_cell) * (S (mdr_q_selected_det_seconddeterminanths)) + (ff_column_mdm_cell_mdr_selected_det_seconddeterminanthscm_negative_cell))) * mdr_nc_selected_det_seconddeterminanth)) /\ exists ff_q_mdm_mdr_selected_det_seconddeterminanthscm_negative_cell_source. mdr_nb_selected_det_seconddeterminanth = ff_q_mdm_mdr_selected_det_seconddeterminanthscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_selected_det_seconddeterminanthscm_negative_cell) * (S (mdr_q_selected_det_seconddeterminanths)) + (ff_column_mdm_cell_mdr_selected_det_seconddeterminanthscm_negative_cell))) * mdr_nc_selected_det_seconddeterminanth) + (ff_value_mdm_prefix_mdr_selected_det_seconddeterminanthscm_negative)))))) /\ (((exists ff_h_mdm_mdr_selected_det_seconddeterminanthscm_negative_target. ff_h_mdm_mdr_selected_det_seconddeterminanthscm_negative_target + S (ff_value_mdm_prefix_mdr_selected_det_seconddeterminanthscm_negative) = S ((S (ff_index_mdm_prefix_mdr_selected_det_seconddeterminanthscm_negative)) * mdr_ut_selected_det_seconddeterminanthsc)) /\ exists ff_q_mdm_mdr_selected_det_seconddeterminanthscm_negative_target. mdr_un_selected_det_seconddeterminanthsc = ff_q_mdm_mdr_selected_det_seconddeterminanthscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_selected_det_seconddeterminanthscm_negative)) * mdr_ut_selected_det_seconddeterminanthsc) + (ff_value_mdm_prefix_mdr_selected_det_seconddeterminanthscm_negative))))))))) /\ ((((exists ff_h_mdr_selected_det_seconddeterminanthscp. ff_h_mdr_selected_det_seconddeterminanthscp + S (mdr_p_selected_det_seconddeterminanthsc) = S ((S (mdr_j_selected_det_seconddeterminanthsc)) * mdr_ec_selected_det_seconddeterminanths)) /\ exists ff_q_mdr_selected_det_seconddeterminanthscp. mdr_eb_selected_det_seconddeterminanths = ff_q_mdr_selected_det_seconddeterminanthscp * S ((S (mdr_j_selected_det_seconddeterminanthsc)) * mdr_ec_selected_det_seconddeterminanths) + (mdr_p_selected_det_seconddeterminanthsc))) /\ (((exists ff_h_mdr_selected_det_seconddeterminanthscn. ff_h_mdr_selected_det_seconddeterminanthscn + S (mdr_n_selected_det_seconddeterminanthsc) = S ((S (mdr_j_selected_det_seconddeterminanthsc)) * mdr_fc_selected_det_seconddeterminanths)) /\ exists ff_q_mdr_selected_det_seconddeterminanthscn. mdr_fb_selected_det_seconddeterminanths = ff_q_mdr_selected_det_seconddeterminanthscn * S ((S (mdr_j_selected_det_seconddeterminanthsc)) * mdr_fc_selected_det_seconddeterminanths) + (mdr_n_selected_det_seconddeterminanthsc)))))))) /\ (exists ff_ub_mce_fold_mdr_selected_det_seconddeterminanthsf ff_uc_mce_fold_mdr_selected_det_seconddeterminanthsf ff_vb_mce_fold_mdr_selected_det_seconddeterminanthsf ff_vc_mce_fold_mdr_selected_det_seconddeterminanthsf. ((forall ff_index_mce_alternating_mdr_selected_det_seconddeterminanthsf_prefix. (exists ff_gap_mce_mdr_selected_det_seconddeterminanthsf_prefix_index. ff_gap_mce_mdr_selected_det_seconddeterminanthsf_prefix_index + S (ff_index_mce_alternating_mdr_selected_det_seconddeterminanthsf_prefix) = (S (mdr_q_selected_det_seconddeterminanths))) -> exists ff_ap_mce_alternating_mdr_selected_det_seconddeterminanthsf_prefix ff_an_mce_alternating_mdr_selected_det_seconddeterminanthsf_prefix ff_bp_mce_alternating_mdr_selected_det_seconddeterminanthsf_prefix ff_bn_mce_alternating_mdr_selected_det_seconddeterminanthsf_prefix ff_p_mce_alternating_mdr_selected_det_seconddeterminanthsf_prefix ff_n_mce_alternating_mdr_selected_det_seconddeterminanthsf_prefix. ((((exists ff_h_mce_mdr_selected_det_seconddeterminanthsf_prefix_ap. ff_h_mce_mdr_selected_det_seconddeterminanthsf_prefix_ap + S (ff_ap_mce_alternating_mdr_selected_det_seconddeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_selected_det_seconddeterminanthsf_prefix)) * mdr_pc_selected_det_seconddeterminanth)) /\ exists ff_q_mce_mdr_selected_det_seconddeterminanthsf_prefix_ap. mdr_pb_selected_det_seconddeterminanth = ff_q_mce_mdr_selected_det_seconddeterminanthsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_selected_det_seconddeterminanthsf_prefix)) * mdr_pc_selected_det_seconddeterminanth) + (ff_ap_mce_alternating_mdr_selected_det_seconddeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_selected_det_seconddeterminanthsf_prefix_an. ff_h_mce_mdr_selected_det_seconddeterminanthsf_prefix_an + S (ff_an_mce_alternating_mdr_selected_det_seconddeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_selected_det_seconddeterminanthsf_prefix)) * mdr_nc_selected_det_seconddeterminanth)) /\ exists ff_q_mce_mdr_selected_det_seconddeterminanthsf_prefix_an. mdr_nb_selected_det_seconddeterminanth = ff_q_mce_mdr_selected_det_seconddeterminanthsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_selected_det_seconddeterminanthsf_prefix)) * mdr_nc_selected_det_seconddeterminanth) + (ff_an_mce_alternating_mdr_selected_det_seconddeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_selected_det_seconddeterminanthsf_prefix_bp. ff_h_mce_mdr_selected_det_seconddeterminanthsf_prefix_bp + S (ff_bp_mce_alternating_mdr_selected_det_seconddeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_selected_det_seconddeterminanthsf_prefix)) * mdr_ec_selected_det_seconddeterminanths)) /\ exists ff_q_mce_mdr_selected_det_seconddeterminanthsf_prefix_bp. mdr_eb_selected_det_seconddeterminanths = ff_q_mce_mdr_selected_det_seconddeterminanthsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_selected_det_seconddeterminanthsf_prefix)) * mdr_ec_selected_det_seconddeterminanths) + (ff_bp_mce_alternating_mdr_selected_det_seconddeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_selected_det_seconddeterminanthsf_prefix_bn. ff_h_mce_mdr_selected_det_seconddeterminanthsf_prefix_bn + S (ff_bn_mce_alternating_mdr_selected_det_seconddeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_selected_det_seconddeterminanthsf_prefix)) * mdr_fc_selected_det_seconddeterminanths)) /\ exists ff_q_mce_mdr_selected_det_seconddeterminanthsf_prefix_bn. mdr_fb_selected_det_seconddeterminanths = ff_q_mce_mdr_selected_det_seconddeterminanthsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_selected_det_seconddeterminanthsf_prefix)) * mdr_fc_selected_det_seconddeterminanths) + (ff_bn_mce_alternating_mdr_selected_det_seconddeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_selected_det_seconddeterminanthsf_prefix_positive. ff_h_mce_mdr_selected_det_seconddeterminanthsf_prefix_positive + S (ff_p_mce_alternating_mdr_selected_det_seconddeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_selected_det_seconddeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_selected_det_seconddeterminanthsf)) /\ exists ff_q_mce_mdr_selected_det_seconddeterminanthsf_prefix_positive. ff_ub_mce_fold_mdr_selected_det_seconddeterminanthsf = ff_q_mce_mdr_selected_det_seconddeterminanthsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_selected_det_seconddeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_selected_det_seconddeterminanthsf) + (ff_p_mce_alternating_mdr_selected_det_seconddeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_selected_det_seconddeterminanthsf_prefix_negative. ff_h_mce_mdr_selected_det_seconddeterminanthsf_prefix_negative + S (ff_n_mce_alternating_mdr_selected_det_seconddeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_selected_det_seconddeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_selected_det_seconddeterminanthsf)) /\ exists ff_q_mce_mdr_selected_det_seconddeterminanthsf_prefix_negative. ff_vb_mce_fold_mdr_selected_det_seconddeterminanthsf = ff_q_mce_mdr_selected_det_seconddeterminanthsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_selected_det_seconddeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_selected_det_seconddeterminanthsf) + (ff_n_mce_alternating_mdr_selected_det_seconddeterminanthsf_prefix))) /\ (((exists ff_even_mce_term_mdr_selected_det_seconddeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_selected_det_seconddeterminanthsf_prefix = 2 * ff_even_mce_term_mdr_selected_det_seconddeterminanthsf_prefix_term) /\ (ff_p_mce_alternating_mdr_selected_det_seconddeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_selected_det_seconddeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_selected_det_seconddeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_selected_det_seconddeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_selected_det_seconddeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_selected_det_seconddeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_selected_det_seconddeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_selected_det_seconddeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_selected_det_seconddeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_selected_det_seconddeterminanthsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_selected_det_seconddeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_selected_det_seconddeterminanthsf_prefix = 2 * ff_odd_mce_term_mdr_selected_det_seconddeterminanthsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_selected_det_seconddeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_selected_det_seconddeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_selected_det_seconddeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_selected_det_seconddeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_selected_det_seconddeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_selected_det_seconddeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_selected_det_seconddeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_selected_det_seconddeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_selected_det_seconddeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_selected_det_seconddeterminanthsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_selected_det_seconddeterminanthsf_positive ff_v_mce_mdr_selected_det_seconddeterminanthsf_positive. ((((exists ff_h_mce_mdr_selected_det_seconddeterminanthsf_positive_start. ff_h_mce_mdr_selected_det_seconddeterminanthsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_selected_det_seconddeterminanthsf_positive)) /\ exists ff_q_mce_mdr_selected_det_seconddeterminanthsf_positive_start. ff_u_mce_mdr_selected_det_seconddeterminanthsf_positive = ff_q_mce_mdr_selected_det_seconddeterminanthsf_positive_start * S ((S (0)) * ff_v_mce_mdr_selected_det_seconddeterminanthsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_selected_det_seconddeterminanthsf_positive_terminal. ff_h_mce_mdr_selected_det_seconddeterminanthsf_positive_terminal + S (mdr_p_selected_det_seconddeterminanth) = S ((S ((S (mdr_q_selected_det_seconddeterminanths)))) * ff_v_mce_mdr_selected_det_seconddeterminanthsf_positive)) /\ exists ff_q_mce_mdr_selected_det_seconddeterminanthsf_positive_terminal. ff_u_mce_mdr_selected_det_seconddeterminanthsf_positive = ff_q_mce_mdr_selected_det_seconddeterminanthsf_positive_terminal * S ((S ((S (mdr_q_selected_det_seconddeterminanths)))) * ff_v_mce_mdr_selected_det_seconddeterminanthsf_positive) + (mdr_p_selected_det_seconddeterminanth))) /\ forall ff_i_mce_mdr_selected_det_seconddeterminanthsf_positive. (exists ff_lt_mce_mdr_selected_det_seconddeterminanthsf_positive_bound. ff_lt_mce_mdr_selected_det_seconddeterminanthsf_positive_bound + S ff_i_mce_mdr_selected_det_seconddeterminanthsf_positive = (S (mdr_q_selected_det_seconddeterminanths))) -> exists ff_a_mce_mdr_selected_det_seconddeterminanthsf_positive ff_r_mce_mdr_selected_det_seconddeterminanthsf_positive ff_s_mce_mdr_selected_det_seconddeterminanthsf_positive. ((((exists ff_h_mce_mdr_selected_det_seconddeterminanthsf_positive_summand. ff_h_mce_mdr_selected_det_seconddeterminanthsf_positive_summand + S (ff_a_mce_mdr_selected_det_seconddeterminanthsf_positive) = S ((S (ff_i_mce_mdr_selected_det_seconddeterminanthsf_positive)) * ff_uc_mce_fold_mdr_selected_det_seconddeterminanthsf)) /\ exists ff_q_mce_mdr_selected_det_seconddeterminanthsf_positive_summand. ff_ub_mce_fold_mdr_selected_det_seconddeterminanthsf = ff_q_mce_mdr_selected_det_seconddeterminanthsf_positive_summand * S ((S (ff_i_mce_mdr_selected_det_seconddeterminanthsf_positive)) * ff_uc_mce_fold_mdr_selected_det_seconddeterminanthsf) + (ff_a_mce_mdr_selected_det_seconddeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_selected_det_seconddeterminanthsf_positive_partial. ff_h_mce_mdr_selected_det_seconddeterminanthsf_positive_partial + S (ff_r_mce_mdr_selected_det_seconddeterminanthsf_positive) = S ((S (ff_i_mce_mdr_selected_det_seconddeterminanthsf_positive)) * ff_v_mce_mdr_selected_det_seconddeterminanthsf_positive)) /\ exists ff_q_mce_mdr_selected_det_seconddeterminanthsf_positive_partial. ff_u_mce_mdr_selected_det_seconddeterminanthsf_positive = ff_q_mce_mdr_selected_det_seconddeterminanthsf_positive_partial * S ((S (ff_i_mce_mdr_selected_det_seconddeterminanthsf_positive)) * ff_v_mce_mdr_selected_det_seconddeterminanthsf_positive) + (ff_r_mce_mdr_selected_det_seconddeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_selected_det_seconddeterminanthsf_positive_successor. ff_h_mce_mdr_selected_det_seconddeterminanthsf_positive_successor + S (ff_s_mce_mdr_selected_det_seconddeterminanthsf_positive) = S ((S (S ff_i_mce_mdr_selected_det_seconddeterminanthsf_positive)) * ff_v_mce_mdr_selected_det_seconddeterminanthsf_positive)) /\ exists ff_q_mce_mdr_selected_det_seconddeterminanthsf_positive_successor. ff_u_mce_mdr_selected_det_seconddeterminanthsf_positive = ff_q_mce_mdr_selected_det_seconddeterminanthsf_positive_successor * S ((S (S ff_i_mce_mdr_selected_det_seconddeterminanthsf_positive)) * ff_v_mce_mdr_selected_det_seconddeterminanthsf_positive) + (ff_s_mce_mdr_selected_det_seconddeterminanthsf_positive))) /\ ff_s_mce_mdr_selected_det_seconddeterminanthsf_positive = ff_r_mce_mdr_selected_det_seconddeterminanthsf_positive + ff_a_mce_mdr_selected_det_seconddeterminanthsf_positive)))))) /\ (exists ff_u_mce_mdr_selected_det_seconddeterminanthsf_negative ff_v_mce_mdr_selected_det_seconddeterminanthsf_negative. ((((exists ff_h_mce_mdr_selected_det_seconddeterminanthsf_negative_start. ff_h_mce_mdr_selected_det_seconddeterminanthsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_selected_det_seconddeterminanthsf_negative)) /\ exists ff_q_mce_mdr_selected_det_seconddeterminanthsf_negative_start. ff_u_mce_mdr_selected_det_seconddeterminanthsf_negative = ff_q_mce_mdr_selected_det_seconddeterminanthsf_negative_start * S ((S (0)) * ff_v_mce_mdr_selected_det_seconddeterminanthsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_selected_det_seconddeterminanthsf_negative_terminal. ff_h_mce_mdr_selected_det_seconddeterminanthsf_negative_terminal + S (mdr_n_selected_det_seconddeterminanth) = S ((S ((S (mdr_q_selected_det_seconddeterminanths)))) * ff_v_mce_mdr_selected_det_seconddeterminanthsf_negative)) /\ exists ff_q_mce_mdr_selected_det_seconddeterminanthsf_negative_terminal. ff_u_mce_mdr_selected_det_seconddeterminanthsf_negative = ff_q_mce_mdr_selected_det_seconddeterminanthsf_negative_terminal * S ((S ((S (mdr_q_selected_det_seconddeterminanths)))) * ff_v_mce_mdr_selected_det_seconddeterminanthsf_negative) + (mdr_n_selected_det_seconddeterminanth))) /\ forall ff_i_mce_mdr_selected_det_seconddeterminanthsf_negative. (exists ff_lt_mce_mdr_selected_det_seconddeterminanthsf_negative_bound. ff_lt_mce_mdr_selected_det_seconddeterminanthsf_negative_bound + S ff_i_mce_mdr_selected_det_seconddeterminanthsf_negative = (S (mdr_q_selected_det_seconddeterminanths))) -> exists ff_a_mce_mdr_selected_det_seconddeterminanthsf_negative ff_r_mce_mdr_selected_det_seconddeterminanthsf_negative ff_s_mce_mdr_selected_det_seconddeterminanthsf_negative. ((((exists ff_h_mce_mdr_selected_det_seconddeterminanthsf_negative_summand. ff_h_mce_mdr_selected_det_seconddeterminanthsf_negative_summand + S (ff_a_mce_mdr_selected_det_seconddeterminanthsf_negative) = S ((S (ff_i_mce_mdr_selected_det_seconddeterminanthsf_negative)) * ff_vc_mce_fold_mdr_selected_det_seconddeterminanthsf)) /\ exists ff_q_mce_mdr_selected_det_seconddeterminanthsf_negative_summand. ff_vb_mce_fold_mdr_selected_det_seconddeterminanthsf = ff_q_mce_mdr_selected_det_seconddeterminanthsf_negative_summand * S ((S (ff_i_mce_mdr_selected_det_seconddeterminanthsf_negative)) * ff_vc_mce_fold_mdr_selected_det_seconddeterminanthsf) + (ff_a_mce_mdr_selected_det_seconddeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_selected_det_seconddeterminanthsf_negative_partial. ff_h_mce_mdr_selected_det_seconddeterminanthsf_negative_partial + S (ff_r_mce_mdr_selected_det_seconddeterminanthsf_negative) = S ((S (ff_i_mce_mdr_selected_det_seconddeterminanthsf_negative)) * ff_v_mce_mdr_selected_det_seconddeterminanthsf_negative)) /\ exists ff_q_mce_mdr_selected_det_seconddeterminanthsf_negative_partial. ff_u_mce_mdr_selected_det_seconddeterminanthsf_negative = ff_q_mce_mdr_selected_det_seconddeterminanthsf_negative_partial * S ((S (ff_i_mce_mdr_selected_det_seconddeterminanthsf_negative)) * ff_v_mce_mdr_selected_det_seconddeterminanthsf_negative) + (ff_r_mce_mdr_selected_det_seconddeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_selected_det_seconddeterminanthsf_negative_successor. ff_h_mce_mdr_selected_det_seconddeterminanthsf_negative_successor + S (ff_s_mce_mdr_selected_det_seconddeterminanthsf_negative) = S ((S (S ff_i_mce_mdr_selected_det_seconddeterminanthsf_negative)) * ff_v_mce_mdr_selected_det_seconddeterminanthsf_negative)) /\ exists ff_q_mce_mdr_selected_det_seconddeterminanthsf_negative_successor. ff_u_mce_mdr_selected_det_seconddeterminanthsf_negative = ff_q_mce_mdr_selected_det_seconddeterminanthsf_negative_successor * S ((S (S ff_i_mce_mdr_selected_det_seconddeterminanthsf_negative)) * ff_v_mce_mdr_selected_det_seconddeterminanthsf_negative) + (ff_s_mce_mdr_selected_det_seconddeterminanthsf_negative))) /\ ff_s_mce_mdr_selected_det_seconddeterminanthsf_negative = ff_r_mce_mdr_selected_det_seconddeterminanthsf_negative + ff_a_mce_mdr_selected_det_seconddeterminanthsf_negative))))))))))))))) /\ ((exists mdr_gap_selected_det_seconddeterminanti. mdr_gap_selected_det_seconddeterminanti + S (mdr_i_selected_det_seconddeterminant) = (mdr_l_selected_det_seconddeterminant)) /\ (exists mdr_z_selected_det_seconddeterminantr. ((exists mdr_a_selected_det_seconddeterminantrc mdr_b_selected_det_seconddeterminantrc mdr_c_selected_det_seconddeterminantrc mdr_e_selected_det_seconddeterminantrc mdr_f_selected_det_seconddeterminantrc. ((mdr_a_selected_det_seconddeterminantrc = ((q) + (mdr_ub_selected_det_second)) * S ((q) + (mdr_ub_selected_det_second)) + ((mdr_ub_selected_det_second) + (mdr_ub_selected_det_second))) /\ ((mdr_b_selected_det_seconddeterminantrc = ((mdr_uc_selected_det_second) + (mdr_vb_selected_det_second)) * S ((mdr_uc_selected_det_second) + (mdr_vb_selected_det_second)) + ((mdr_vb_selected_det_second) + (mdr_vb_selected_det_second))) /\ ((mdr_c_selected_det_seconddeterminantrc = ((mdr_a_selected_det_seconddeterminantrc) + (mdr_b_selected_det_seconddeterminantrc)) * S ((mdr_a_selected_det_seconddeterminantrc) + (mdr_b_selected_det_seconddeterminantrc)) + ((mdr_b_selected_det_seconddeterminantrc) + (mdr_b_selected_det_seconddeterminantrc))) /\ ((mdr_e_selected_det_seconddeterminantrc = ((P) + (N)) * S ((P) + (N)) + ((N) + (N))) /\ ((mdr_f_selected_det_seconddeterminantrc = ((mdr_vc_selected_det_second) + (mdr_e_selected_det_seconddeterminantrc)) * S ((mdr_vc_selected_det_second) + (mdr_e_selected_det_seconddeterminantrc)) + ((mdr_e_selected_det_seconddeterminantrc) + (mdr_e_selected_det_seconddeterminantrc))) /\ ((mdr_z_selected_det_seconddeterminantr) = ((mdr_c_selected_det_seconddeterminantrc) + (mdr_f_selected_det_seconddeterminantrc)) * S ((mdr_c_selected_det_seconddeterminantrc) + (mdr_f_selected_det_seconddeterminantrc)) + ((mdr_f_selected_det_seconddeterminantrc) + (mdr_f_selected_det_seconddeterminantrc))))))))) /\ (((exists ff_h_mdr_selected_det_seconddeterminantrb. ff_h_mdr_selected_det_seconddeterminantrb + S (mdr_z_selected_det_seconddeterminantr) = S ((S (mdr_i_selected_det_seconddeterminant)) * mdr_c_selected_det_seconddeterminant)) /\ exists ff_q_mdr_selected_det_seconddeterminantrb. mdr_b_selected_det_seconddeterminant = ff_q_mdr_selected_det_seconddeterminantrb * S ((S (mdr_i_selected_det_seconddeterminant)) * mdr_c_selected_det_seconddeterminant) + (mdr_z_selected_det_seconddeterminantr)))))))))) -> p = P /\ n = N