matrix_integer_selected_determinant_balance

Exact expanded first-order arithmetic statement

forall ab ac bb bc eb ec fb fc r w q rb rc cb cc p n P N. (forall ics_index_selected_determinant_parents ics_value0_selected_determinant_parents ics_value1_selected_determinant_parents ics_value2_selected_determinant_parents ics_value3_selected_determinant_parents. (exists ics_gap_selected_determinant_parents_bound. ics_gap_selected_determinant_parents_bound + S (ics_index_selected_determinant_parents) = ((r) * (w))) -> (((exists fs_h_ics_selected_determinant_parents_at0. fs_h_ics_selected_determinant_parents_at0 + S (ics_value0_selected_determinant_parents) = S ((S (ics_index_selected_determinant_parents)) * ac)) /\ exists fs_q_ics_selected_determinant_parents_at0. ab = fs_q_ics_selected_determinant_parents_at0 * S ((S (ics_index_selected_determinant_parents)) * ac) + (ics_value0_selected_determinant_parents))) -> (((exists fs_h_ics_selected_determinant_parents_at1. fs_h_ics_selected_determinant_parents_at1 + S (ics_value1_selected_determinant_parents) = S ((S (ics_index_selected_determinant_parents)) * bc)) /\ exists fs_q_ics_selected_determinant_parents_at1. bb = fs_q_ics_selected_determinant_parents_at1 * S ((S (ics_index_selected_determinant_parents)) * bc) + (ics_value1_selected_determinant_parents))) -> (((exists fs_h_ics_selected_determinant_parents_at2. fs_h_ics_selected_determinant_parents_at2 + S (ics_value2_selected_determinant_parents) = S ((S (ics_index_selected_determinant_parents)) * ec)) /\ exists fs_q_ics_selected_determinant_parents_at2. eb = fs_q_ics_selected_determinant_parents_at2 * S ((S (ics_index_selected_determinant_parents)) * ec) + (ics_value2_selected_determinant_parents))) -> (((exists fs_h_ics_selected_determinant_parents_at3. fs_h_ics_selected_determinant_parents_at3 + S (ics_value3_selected_determinant_parents) = S ((S (ics_index_selected_determinant_parents)) * fc)) /\ exists fs_q_ics_selected_determinant_parents_at3. fb = fs_q_ics_selected_determinant_parents_at3 * S ((S (ics_index_selected_determinant_parents)) * fc) + (ics_value3_selected_determinant_parents))) -> ics_value0_selected_determinant_parents + ics_value3_selected_determinant_parents = ics_value2_selected_determinant_parents + ics_value1_selected_determinant_parents) -> (((forall fom_index_mrf_selected_determinant_rowsbound. (exists fom_gap_mrf_selected_determinant_rowsbound_index_bound. fom_gap_mrf_selected_determinant_rowsbound_index_bound + S (fom_index_mrf_selected_determinant_rowsbound) = q) -> exists fom_value_mrf_selected_determinant_rowsbound. ((((exists fom_beta_height_mrf_selected_determinant_rowsbound_entry. fom_beta_height_mrf_selected_determinant_rowsbound_entry + S (fom_value_mrf_selected_determinant_rowsbound) = S ((S (fom_index_mrf_selected_determinant_rowsbound)) * rc)) /\ exists fom_beta_quotient_mrf_selected_determinant_rowsbound_entry. rb = fom_beta_quotient_mrf_selected_determinant_rowsbound_entry * S ((S (fom_index_mrf_selected_determinant_rowsbound)) * rc) + (fom_value_mrf_selected_determinant_rowsbound))) /\ (exists fom_gap_mrf_selected_determinant_rowsbound_value_bound. fom_gap_mrf_selected_determinant_rowsbound_value_bound + S (fom_value_mrf_selected_determinant_rowsbound) = r))) /\ (forall mdr_i_selected_determinant_rowsdistinct mdr_j_selected_determinant_rowsdistinct mdr_a_selected_determinant_rowsdistinct. (exists mdr_gap_selected_determinant_rowsdistincti. mdr_gap_selected_determinant_rowsdistincti + S (mdr_i_selected_determinant_rowsdistinct) = (q)) -> (exists mdr_gap_selected_determinant_rowsdistinctj. mdr_gap_selected_determinant_rowsdistinctj + S (mdr_j_selected_determinant_rowsdistinct) = (q)) -> (((exists ff_h_mdr_selected_determinant_rowsdistinctfirst. ff_h_mdr_selected_determinant_rowsdistinctfirst + S (mdr_a_selected_determinant_rowsdistinct) = S ((S (mdr_i_selected_determinant_rowsdistinct)) * rc)) /\ exists ff_q_mdr_selected_determinant_rowsdistinctfirst. rb = ff_q_mdr_selected_determinant_rowsdistinctfirst * S ((S (mdr_i_selected_determinant_rowsdistinct)) * rc) + (mdr_a_selected_determinant_rowsdistinct))) -> (((exists ff_h_mdr_selected_determinant_rowsdistinctsecond. ff_h_mdr_selected_determinant_rowsdistinctsecond + S (mdr_a_selected_determinant_rowsdistinct) = S ((S (mdr_j_selected_determinant_rowsdistinct)) * rc)) /\ exists ff_q_mdr_selected_determinant_rowsdistinctsecond. rb = ff_q_mdr_selected_determinant_rowsdistinctsecond * S ((S (mdr_j_selected_determinant_rowsdistinct)) * rc) + (mdr_a_selected_determinant_rowsdistinct))) -> mdr_i_selected_determinant_rowsdistinct = mdr_j_selected_determinant_rowsdistinct))) -> (((forall fom_index_mrf_selected_determinant_columnsbound. (exists fom_gap_mrf_selected_determinant_columnsbound_index_bound. fom_gap_mrf_selected_determinant_columnsbound_index_bound + S (fom_index_mrf_selected_determinant_columnsbound) = q) -> exists fom_value_mrf_selected_determinant_columnsbound. ((((exists fom_beta_height_mrf_selected_determinant_columnsbound_entry. fom_beta_height_mrf_selected_determinant_columnsbound_entry + S (fom_value_mrf_selected_determinant_columnsbound) = S ((S (fom_index_mrf_selected_determinant_columnsbound)) * cc)) /\ exists fom_beta_quotient_mrf_selected_determinant_columnsbound_entry. cb = fom_beta_quotient_mrf_selected_determinant_columnsbound_entry * S ((S (fom_index_mrf_selected_determinant_columnsbound)) * cc) + (fom_value_mrf_selected_determinant_columnsbound))) /\ (exists fom_gap_mrf_selected_determinant_columnsbound_value_bound. fom_gap_mrf_selected_determinant_columnsbound_value_bound + S (fom_value_mrf_selected_determinant_columnsbound) = w))) /\ (forall mdr_i_selected_determinant_columnsdistinct mdr_j_selected_determinant_columnsdistinct mdr_a_selected_determinant_columnsdistinct. (exists mdr_gap_selected_determinant_columnsdistincti. mdr_gap_selected_determinant_columnsdistincti + S (mdr_i_selected_determinant_columnsdistinct) = (q)) -> (exists mdr_gap_selected_determinant_columnsdistinctj. mdr_gap_selected_determinant_columnsdistinctj + S (mdr_j_selected_determinant_columnsdistinct) = (q)) -> (((exists ff_h_mdr_selected_determinant_columnsdistinctfirst. ff_h_mdr_selected_determinant_columnsdistinctfirst + S (mdr_a_selected_determinant_columnsdistinct) = S ((S (mdr_i_selected_determinant_columnsdistinct)) * cc)) /\ exists ff_q_mdr_selected_determinant_columnsdistinctfirst. cb = ff_q_mdr_selected_determinant_columnsdistinctfirst * S ((S (mdr_i_selected_determinant_columnsdistinct)) * cc) + (mdr_a_selected_determinant_columnsdistinct))) -> (((exists ff_h_mdr_selected_determinant_columnsdistinctsecond. ff_h_mdr_selected_determinant_columnsdistinctsecond + S (mdr_a_selected_determinant_columnsdistinct) = S ((S (mdr_j_selected_determinant_columnsdistinct)) * cc)) /\ exists ff_q_mdr_selected_determinant_columnsdistinctsecond. cb = ff_q_mdr_selected_determinant_columnsdistinctsecond * S ((S (mdr_j_selected_determinant_columnsdistinct)) * cc) + (mdr_a_selected_determinant_columnsdistinct))) -> mdr_i_selected_determinant_columnsdistinct = mdr_j_selected_determinant_columnsdistinct))) -> (exists mdr_ub_first_selected_determinant mdr_uc_first_selected_determinant mdr_vb_first_selected_determinant mdr_vc_first_selected_determinant. ((((forall mdr_i_first_selected_determinantmatrixpositive. (exists mdr_gap_first_selected_determinantmatrixpositivebound. mdr_gap_first_selected_determinantmatrixpositivebound + S (mdr_i_first_selected_determinantmatrixpositive) = ((q) * (q))) -> exists mdr_a_first_selected_determinantmatrixpositive. (((exists mdr_r_first_selected_determinantmatrixpositivepoint mdr_s_first_selected_determinantmatrixpositivepoint mdr_u_first_selected_determinantmatrixpositivepoint mdr_v_first_selected_determinantmatrixpositivepoint. ((mdr_i_first_selected_determinantmatrixpositive = (q) * mdr_r_first_selected_determinantmatrixpositivepoint + mdr_s_first_selected_determinantmatrixpositivepoint) /\ ((exists mdr_gap_first_selected_determinantmatrixpositivepointcolumn. mdr_gap_first_selected_determinantmatrixpositivepointcolumn + S (mdr_s_first_selected_determinantmatrixpositivepoint) = (q)) /\ ((((exists ff_h_mdr_first_selected_determinantmatrixpositivepointrow_index. ff_h_mdr_first_selected_determinantmatrixpositivepointrow_index + S (mdr_u_first_selected_determinantmatrixpositivepoint) = S ((S (mdr_r_first_selected_determinantmatrixpositivepoint)) * rc)) /\ exists ff_q_mdr_first_selected_determinantmatrixpositivepointrow_index. rb = ff_q_mdr_first_selected_determinantmatrixpositivepointrow_index * S ((S (mdr_r_first_selected_determinantmatrixpositivepoint)) * rc) + (mdr_u_first_selected_determinantmatrixpositivepoint))) /\ ((((exists ff_h_mdr_first_selected_determinantmatrixpositivepointcolumn_index. ff_h_mdr_first_selected_determinantmatrixpositivepointcolumn_index + S (mdr_v_first_selected_determinantmatrixpositivepoint) = S ((S (mdr_s_first_selected_determinantmatrixpositivepoint)) * cc)) /\ exists ff_q_mdr_first_selected_determinantmatrixpositivepointcolumn_index. cb = ff_q_mdr_first_selected_determinantmatrixpositivepointcolumn_index * S ((S (mdr_s_first_selected_determinantmatrixpositivepoint)) * cc) + (mdr_v_first_selected_determinantmatrixpositivepoint))) /\ (((exists ff_h_mdr_first_selected_determinantmatrixpositivepointsource. ff_h_mdr_first_selected_determinantmatrixpositivepointsource + S (mdr_a_first_selected_determinantmatrixpositive) = S ((S ((mdr_u_first_selected_determinantmatrixpositivepoint) * (w) + (mdr_v_first_selected_determinantmatrixpositivepoint))) * ac)) /\ exists ff_q_mdr_first_selected_determinantmatrixpositivepointsource. ab = ff_q_mdr_first_selected_determinantmatrixpositivepointsource * S ((S ((mdr_u_first_selected_determinantmatrixpositivepoint) * (w) + (mdr_v_first_selected_determinantmatrixpositivepoint))) * ac) + (mdr_a_first_selected_determinantmatrixpositive)))))))) /\ (((exists ff_h_mdr_first_selected_determinantmatrixpositiveoutput. ff_h_mdr_first_selected_determinantmatrixpositiveoutput + S (mdr_a_first_selected_determinantmatrixpositive) = S ((S (mdr_i_first_selected_determinantmatrixpositive)) * mdr_uc_first_selected_determinant)) /\ exists ff_q_mdr_first_selected_determinantmatrixpositiveoutput. mdr_ub_first_selected_determinant = ff_q_mdr_first_selected_determinantmatrixpositiveoutput * S ((S (mdr_i_first_selected_determinantmatrixpositive)) * mdr_uc_first_selected_determinant) + (mdr_a_first_selected_determinantmatrixpositive)))))) /\ (forall mdr_i_first_selected_determinantmatrixnegative. (exists mdr_gap_first_selected_determinantmatrixnegativebound. mdr_gap_first_selected_determinantmatrixnegativebound + S (mdr_i_first_selected_determinantmatrixnegative) = ((q) * (q))) -> exists mdr_a_first_selected_determinantmatrixnegative. (((exists mdr_r_first_selected_determinantmatrixnegativepoint mdr_s_first_selected_determinantmatrixnegativepoint mdr_u_first_selected_determinantmatrixnegativepoint mdr_v_first_selected_determinantmatrixnegativepoint. ((mdr_i_first_selected_determinantmatrixnegative = (q) * mdr_r_first_selected_determinantmatrixnegativepoint + mdr_s_first_selected_determinantmatrixnegativepoint) /\ ((exists mdr_gap_first_selected_determinantmatrixnegativepointcolumn. mdr_gap_first_selected_determinantmatrixnegativepointcolumn + S (mdr_s_first_selected_determinantmatrixnegativepoint) = (q)) /\ ((((exists ff_h_mdr_first_selected_determinantmatrixnegativepointrow_index. ff_h_mdr_first_selected_determinantmatrixnegativepointrow_index + S (mdr_u_first_selected_determinantmatrixnegativepoint) = S ((S (mdr_r_first_selected_determinantmatrixnegativepoint)) * rc)) /\ exists ff_q_mdr_first_selected_determinantmatrixnegativepointrow_index. rb = ff_q_mdr_first_selected_determinantmatrixnegativepointrow_index * S ((S (mdr_r_first_selected_determinantmatrixnegativepoint)) * rc) + (mdr_u_first_selected_determinantmatrixnegativepoint))) /\ ((((exists ff_h_mdr_first_selected_determinantmatrixnegativepointcolumn_index. ff_h_mdr_first_selected_determinantmatrixnegativepointcolumn_index + S (mdr_v_first_selected_determinantmatrixnegativepoint) = S ((S (mdr_s_first_selected_determinantmatrixnegativepoint)) * cc)) /\ exists ff_q_mdr_first_selected_determinantmatrixnegativepointcolumn_index. cb = ff_q_mdr_first_selected_determinantmatrixnegativepointcolumn_index * S ((S (mdr_s_first_selected_determinantmatrixnegativepoint)) * cc) + (mdr_v_first_selected_determinantmatrixnegativepoint))) /\ (((exists ff_h_mdr_first_selected_determinantmatrixnegativepointsource. ff_h_mdr_first_selected_determinantmatrixnegativepointsource + S (mdr_a_first_selected_determinantmatrixnegative) = S ((S ((mdr_u_first_selected_determinantmatrixnegativepoint) * (w) + (mdr_v_first_selected_determinantmatrixnegativepoint))) * bc)) /\ exists ff_q_mdr_first_selected_determinantmatrixnegativepointsource. bb = ff_q_mdr_first_selected_determinantmatrixnegativepointsource * S ((S ((mdr_u_first_selected_determinantmatrixnegativepoint) * (w) + (mdr_v_first_selected_determinantmatrixnegativepoint))) * bc) + (mdr_a_first_selected_determinantmatrixnegative)))))))) /\ (((exists ff_h_mdr_first_selected_determinantmatrixnegativeoutput. ff_h_mdr_first_selected_determinantmatrixnegativeoutput + S (mdr_a_first_selected_determinantmatrixnegative) = S ((S (mdr_i_first_selected_determinantmatrixnegative)) * mdr_vc_first_selected_determinant)) /\ exists ff_q_mdr_first_selected_determinantmatrixnegativeoutput. mdr_vb_first_selected_determinant = ff_q_mdr_first_selected_determinantmatrixnegativeoutput * S ((S (mdr_i_first_selected_determinantmatrixnegative)) * mdr_vc_first_selected_determinant) + (mdr_a_first_selected_determinantmatrixnegative)))))))) /\ (exists mdr_b_first_selected_determinantdeterminant mdr_c_first_selected_determinantdeterminant mdr_l_first_selected_determinantdeterminant mdr_i_first_selected_determinantdeterminant. ((forall mdr_i_first_selected_determinantdeterminanth. (exists mdr_gap_first_selected_determinantdeterminanthi. mdr_gap_first_selected_determinantdeterminanthi + S (mdr_i_first_selected_determinantdeterminanth) = (mdr_l_first_selected_determinantdeterminant)) -> exists mdr_d_first_selected_determinantdeterminanth mdr_pb_first_selected_determinantdeterminanth mdr_pc_first_selected_determinantdeterminanth mdr_nb_first_selected_determinantdeterminanth mdr_nc_first_selected_determinantdeterminanth mdr_p_first_selected_determinantdeterminanth mdr_n_first_selected_determinantdeterminanth. ((exists mdr_z_first_selected_determinantdeterminanthr. ((exists mdr_a_first_selected_determinantdeterminanthrc mdr_b_first_selected_determinantdeterminanthrc mdr_c_first_selected_determinantdeterminanthrc mdr_e_first_selected_determinantdeterminanthrc mdr_f_first_selected_determinantdeterminanthrc. ((mdr_a_first_selected_determinantdeterminanthrc = ((mdr_d_first_selected_determinantdeterminanth) + (mdr_pb_first_selected_determinantdeterminanth)) * S ((mdr_d_first_selected_determinantdeterminanth) + (mdr_pb_first_selected_determinantdeterminanth)) + ((mdr_pb_first_selected_determinantdeterminanth) + (mdr_pb_first_selected_determinantdeterminanth))) /\ ((mdr_b_first_selected_determinantdeterminanthrc = ((mdr_pc_first_selected_determinantdeterminanth) + (mdr_nb_first_selected_determinantdeterminanth)) * S ((mdr_pc_first_selected_determinantdeterminanth) + (mdr_nb_first_selected_determinantdeterminanth)) + ((mdr_nb_first_selected_determinantdeterminanth) + (mdr_nb_first_selected_determinantdeterminanth))) /\ ((mdr_c_first_selected_determinantdeterminanthrc = ((mdr_a_first_selected_determinantdeterminanthrc) + (mdr_b_first_selected_determinantdeterminanthrc)) * S ((mdr_a_first_selected_determinantdeterminanthrc) + (mdr_b_first_selected_determinantdeterminanthrc)) + ((mdr_b_first_selected_determinantdeterminanthrc) + (mdr_b_first_selected_determinantdeterminanthrc))) /\ ((mdr_e_first_selected_determinantdeterminanthrc = ((mdr_p_first_selected_determinantdeterminanth) + (mdr_n_first_selected_determinantdeterminanth)) * S ((mdr_p_first_selected_determinantdeterminanth) + (mdr_n_first_selected_determinantdeterminanth)) + ((mdr_n_first_selected_determinantdeterminanth) + (mdr_n_first_selected_determinantdeterminanth))) /\ ((mdr_f_first_selected_determinantdeterminanthrc = ((mdr_nc_first_selected_determinantdeterminanth) + (mdr_e_first_selected_determinantdeterminanthrc)) * S ((mdr_nc_first_selected_determinantdeterminanth) + (mdr_e_first_selected_determinantdeterminanthrc)) + ((mdr_e_first_selected_determinantdeterminanthrc) + (mdr_e_first_selected_determinantdeterminanthrc))) /\ ((mdr_z_first_selected_determinantdeterminanthr) = ((mdr_c_first_selected_determinantdeterminanthrc) + (mdr_f_first_selected_determinantdeterminanthrc)) * S ((mdr_c_first_selected_determinantdeterminanthrc) + (mdr_f_first_selected_determinantdeterminanthrc)) + ((mdr_f_first_selected_determinantdeterminanthrc) + (mdr_f_first_selected_determinantdeterminanthrc))))))))) /\ (((exists ff_h_mdr_first_selected_determinantdeterminanthrb. ff_h_mdr_first_selected_determinantdeterminanthrb + S (mdr_z_first_selected_determinantdeterminanthr) = S ((S (mdr_i_first_selected_determinantdeterminanth)) * mdr_c_first_selected_determinantdeterminant)) /\ exists ff_q_mdr_first_selected_determinantdeterminanthrb. mdr_b_first_selected_determinantdeterminant = ff_q_mdr_first_selected_determinantdeterminanthrb * S ((S (mdr_i_first_selected_determinantdeterminanth)) * mdr_c_first_selected_determinantdeterminant) + (mdr_z_first_selected_determinantdeterminanthr))))) /\ (((((mdr_d_first_selected_determinantdeterminanth) = 0) /\ (((mdr_p_first_selected_determinantdeterminanth) = 1) /\ ((mdr_n_first_selected_determinantdeterminanth) = 0))) \/ exists mdr_q_first_selected_determinantdeterminanths mdr_eb_first_selected_determinantdeterminanths mdr_ec_first_selected_determinantdeterminanths mdr_fb_first_selected_determinantdeterminanths mdr_fc_first_selected_determinantdeterminanths. (((mdr_d_first_selected_determinantdeterminanth) = S (mdr_q_first_selected_determinantdeterminanths)) /\ ((forall mdr_j_first_selected_determinantdeterminanthsc. (exists mdr_gap_first_selected_determinantdeterminanthscj. mdr_gap_first_selected_determinantdeterminanthscj + S (mdr_j_first_selected_determinantdeterminanthsc) = (S (mdr_q_first_selected_determinantdeterminanths))) -> exists mdr_i_first_selected_determinantdeterminanthsc mdr_up_first_selected_determinantdeterminanthsc mdr_us_first_selected_determinantdeterminanthsc mdr_un_first_selected_determinantdeterminanthsc mdr_ut_first_selected_determinantdeterminanthsc mdr_p_first_selected_determinantdeterminanthsc mdr_n_first_selected_determinantdeterminanthsc. ((exists mdr_gap_first_selected_determinantdeterminanthsci. mdr_gap_first_selected_determinantdeterminanthsci + S (mdr_i_first_selected_determinantdeterminanthsc) = (mdr_i_first_selected_determinantdeterminanth)) /\ ((exists mdr_z_first_selected_determinantdeterminanthscr. ((exists mdr_a_first_selected_determinantdeterminanthscrc mdr_b_first_selected_determinantdeterminanthscrc mdr_c_first_selected_determinantdeterminanthscrc mdr_e_first_selected_determinantdeterminanthscrc mdr_f_first_selected_determinantdeterminanthscrc. ((mdr_a_first_selected_determinantdeterminanthscrc = ((mdr_q_first_selected_determinantdeterminanths) + (mdr_up_first_selected_determinantdeterminanthsc)) * S ((mdr_q_first_selected_determinantdeterminanths) + (mdr_up_first_selected_determinantdeterminanthsc)) + ((mdr_up_first_selected_determinantdeterminanthsc) + (mdr_up_first_selected_determinantdeterminanthsc))) /\ ((mdr_b_first_selected_determinantdeterminanthscrc = ((mdr_us_first_selected_determinantdeterminanthsc) + (mdr_un_first_selected_determinantdeterminanthsc)) * S ((mdr_us_first_selected_determinantdeterminanthsc) + (mdr_un_first_selected_determinantdeterminanthsc)) + ((mdr_un_first_selected_determinantdeterminanthsc) + (mdr_un_first_selected_determinantdeterminanthsc))) /\ ((mdr_c_first_selected_determinantdeterminanthscrc = ((mdr_a_first_selected_determinantdeterminanthscrc) + (mdr_b_first_selected_determinantdeterminanthscrc)) * S ((mdr_a_first_selected_determinantdeterminanthscrc) + (mdr_b_first_selected_determinantdeterminanthscrc)) + ((mdr_b_first_selected_determinantdeterminanthscrc) + (mdr_b_first_selected_determinantdeterminanthscrc))) /\ ((mdr_e_first_selected_determinantdeterminanthscrc = ((mdr_p_first_selected_determinantdeterminanthsc) + (mdr_n_first_selected_determinantdeterminanthsc)) * S ((mdr_p_first_selected_determinantdeterminanthsc) + (mdr_n_first_selected_determinantdeterminanthsc)) + ((mdr_n_first_selected_determinantdeterminanthsc) + (mdr_n_first_selected_determinantdeterminanthsc))) /\ ((mdr_f_first_selected_determinantdeterminanthscrc = ((mdr_ut_first_selected_determinantdeterminanthsc) + (mdr_e_first_selected_determinantdeterminanthscrc)) * S ((mdr_ut_first_selected_determinantdeterminanthsc) + (mdr_e_first_selected_determinantdeterminanthscrc)) + ((mdr_e_first_selected_determinantdeterminanthscrc) + (mdr_e_first_selected_determinantdeterminanthscrc))) /\ ((mdr_z_first_selected_determinantdeterminanthscr) = ((mdr_c_first_selected_determinantdeterminanthscrc) + (mdr_f_first_selected_determinantdeterminanthscrc)) * S ((mdr_c_first_selected_determinantdeterminanthscrc) + (mdr_f_first_selected_determinantdeterminanthscrc)) + ((mdr_f_first_selected_determinantdeterminanthscrc) + (mdr_f_first_selected_determinantdeterminanthscrc))))))))) /\ (((exists ff_h_mdr_first_selected_determinantdeterminanthscrb. ff_h_mdr_first_selected_determinantdeterminanthscrb + S (mdr_z_first_selected_determinantdeterminanthscr) = S ((S (mdr_i_first_selected_determinantdeterminanthsc)) * mdr_c_first_selected_determinantdeterminant)) /\ exists ff_q_mdr_first_selected_determinantdeterminanthscrb. mdr_b_first_selected_determinantdeterminant = ff_q_mdr_first_selected_determinantdeterminanthscrb * S ((S (mdr_i_first_selected_determinantdeterminanthsc)) * mdr_c_first_selected_determinantdeterminant) + (mdr_z_first_selected_determinantdeterminanthscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_first_selected_determinantdeterminanthscm_positive. (exists ff_gap_mdm_lt_mdr_first_selected_determinantdeterminanthscm_positive_index_bound. ff_gap_mdm_lt_mdr_first_selected_determinantdeterminanthscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_first_selected_determinantdeterminanthscm_positive) = ((mdr_q_first_selected_determinantdeterminanths) * (mdr_q_first_selected_determinantdeterminanths))) -> exists ff_row_mdm_prefix_mdr_first_selected_determinantdeterminanthscm_positive ff_column_mdm_prefix_mdr_first_selected_determinantdeterminanthscm_positive ff_value_mdm_prefix_mdr_first_selected_determinantdeterminanthscm_positive. (ff_index_mdm_prefix_mdr_first_selected_determinantdeterminanthscm_positive = (mdr_q_first_selected_determinantdeterminanths) * ff_row_mdm_prefix_mdr_first_selected_determinantdeterminanthscm_positive + ff_column_mdm_prefix_mdr_first_selected_determinantdeterminanthscm_positive /\ ((exists ff_gap_mdm_lt_mdr_first_selected_determinantdeterminanthscm_positive_column_bound. ff_gap_mdm_lt_mdr_first_selected_determinantdeterminanthscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_first_selected_determinantdeterminanthscm_positive) = (mdr_q_first_selected_determinantdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_first_selected_determinantdeterminanthscm_positive_cell ff_column_mdm_cell_mdr_first_selected_determinantdeterminanthscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_first_selected_determinantdeterminanthscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_first_selected_determinantdeterminanthscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_first_selected_determinantdeterminanthscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_first_selected_determinantdeterminanthscm_positive_cell = ff_row_mdm_prefix_mdr_first_selected_determinantdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_first_selected_determinantdeterminanthscm_positive_cell_row_after. ff_gap_mdm_le_mdr_first_selected_determinantdeterminanthscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_first_selected_determinantdeterminanthscm_positive)) /\ ff_row_mdm_cell_mdr_first_selected_determinantdeterminanthscm_positive_cell = S ff_row_mdm_prefix_mdr_first_selected_determinantdeterminanthscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_first_selected_determinantdeterminanthscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_first_selected_determinantdeterminanthscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_first_selected_determinantdeterminanthscm_positive) = (mdr_j_first_selected_determinantdeterminanthsc)) /\ ff_column_mdm_cell_mdr_first_selected_determinantdeterminanthscm_positive_cell = ff_column_mdm_prefix_mdr_first_selected_determinantdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_first_selected_determinantdeterminanthscm_positive_cell_column_after. ff_gap_mdm_le_mdr_first_selected_determinantdeterminanthscm_positive_cell_column_after + (mdr_j_first_selected_determinantdeterminanthsc) = (ff_column_mdm_prefix_mdr_first_selected_determinantdeterminanthscm_positive)) /\ ff_column_mdm_cell_mdr_first_selected_determinantdeterminanthscm_positive_cell = S ff_column_mdm_prefix_mdr_first_selected_determinantdeterminanthscm_positive))) /\ (((exists ff_h_mdm_mdr_first_selected_determinantdeterminanthscm_positive_cell_source. ff_h_mdm_mdr_first_selected_determinantdeterminanthscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_first_selected_determinantdeterminanthscm_positive) = S ((S ((ff_row_mdm_cell_mdr_first_selected_determinantdeterminanthscm_positive_cell) * (S (mdr_q_first_selected_determinantdeterminanths)) + (ff_column_mdm_cell_mdr_first_selected_determinantdeterminanthscm_positive_cell))) * mdr_pc_first_selected_determinantdeterminanth)) /\ exists ff_q_mdm_mdr_first_selected_determinantdeterminanthscm_positive_cell_source. mdr_pb_first_selected_determinantdeterminanth = ff_q_mdm_mdr_first_selected_determinantdeterminanthscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_first_selected_determinantdeterminanthscm_positive_cell) * (S (mdr_q_first_selected_determinantdeterminanths)) + (ff_column_mdm_cell_mdr_first_selected_determinantdeterminanthscm_positive_cell))) * mdr_pc_first_selected_determinantdeterminanth) + (ff_value_mdm_prefix_mdr_first_selected_determinantdeterminanthscm_positive)))))) /\ (((exists ff_h_mdm_mdr_first_selected_determinantdeterminanthscm_positive_target. ff_h_mdm_mdr_first_selected_determinantdeterminanthscm_positive_target + S (ff_value_mdm_prefix_mdr_first_selected_determinantdeterminanthscm_positive) = S ((S (ff_index_mdm_prefix_mdr_first_selected_determinantdeterminanthscm_positive)) * mdr_us_first_selected_determinantdeterminanthsc)) /\ exists ff_q_mdm_mdr_first_selected_determinantdeterminanthscm_positive_target. mdr_up_first_selected_determinantdeterminanthsc = ff_q_mdm_mdr_first_selected_determinantdeterminanthscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_first_selected_determinantdeterminanthscm_positive)) * mdr_us_first_selected_determinantdeterminanthsc) + (ff_value_mdm_prefix_mdr_first_selected_determinantdeterminanthscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_first_selected_determinantdeterminanthscm_negative. (exists ff_gap_mdm_lt_mdr_first_selected_determinantdeterminanthscm_negative_index_bound. ff_gap_mdm_lt_mdr_first_selected_determinantdeterminanthscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_first_selected_determinantdeterminanthscm_negative) = ((mdr_q_first_selected_determinantdeterminanths) * (mdr_q_first_selected_determinantdeterminanths))) -> exists ff_row_mdm_prefix_mdr_first_selected_determinantdeterminanthscm_negative ff_column_mdm_prefix_mdr_first_selected_determinantdeterminanthscm_negative ff_value_mdm_prefix_mdr_first_selected_determinantdeterminanthscm_negative. (ff_index_mdm_prefix_mdr_first_selected_determinantdeterminanthscm_negative = (mdr_q_first_selected_determinantdeterminanths) * ff_row_mdm_prefix_mdr_first_selected_determinantdeterminanthscm_negative + ff_column_mdm_prefix_mdr_first_selected_determinantdeterminanthscm_negative /\ ((exists ff_gap_mdm_lt_mdr_first_selected_determinantdeterminanthscm_negative_column_bound. ff_gap_mdm_lt_mdr_first_selected_determinantdeterminanthscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_first_selected_determinantdeterminanthscm_negative) = (mdr_q_first_selected_determinantdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_first_selected_determinantdeterminanthscm_negative_cell ff_column_mdm_cell_mdr_first_selected_determinantdeterminanthscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_first_selected_determinantdeterminanthscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_first_selected_determinantdeterminanthscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_first_selected_determinantdeterminanthscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_first_selected_determinantdeterminanthscm_negative_cell = ff_row_mdm_prefix_mdr_first_selected_determinantdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_first_selected_determinantdeterminanthscm_negative_cell_row_after. ff_gap_mdm_le_mdr_first_selected_determinantdeterminanthscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_first_selected_determinantdeterminanthscm_negative)) /\ ff_row_mdm_cell_mdr_first_selected_determinantdeterminanthscm_negative_cell = S ff_row_mdm_prefix_mdr_first_selected_determinantdeterminanthscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_first_selected_determinantdeterminanthscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_first_selected_determinantdeterminanthscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_first_selected_determinantdeterminanthscm_negative) = (mdr_j_first_selected_determinantdeterminanthsc)) /\ ff_column_mdm_cell_mdr_first_selected_determinantdeterminanthscm_negative_cell = ff_column_mdm_prefix_mdr_first_selected_determinantdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_first_selected_determinantdeterminanthscm_negative_cell_column_after. ff_gap_mdm_le_mdr_first_selected_determinantdeterminanthscm_negative_cell_column_after + (mdr_j_first_selected_determinantdeterminanthsc) = (ff_column_mdm_prefix_mdr_first_selected_determinantdeterminanthscm_negative)) /\ ff_column_mdm_cell_mdr_first_selected_determinantdeterminanthscm_negative_cell = S ff_column_mdm_prefix_mdr_first_selected_determinantdeterminanthscm_negative))) /\ (((exists ff_h_mdm_mdr_first_selected_determinantdeterminanthscm_negative_cell_source. ff_h_mdm_mdr_first_selected_determinantdeterminanthscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_first_selected_determinantdeterminanthscm_negative) = S ((S ((ff_row_mdm_cell_mdr_first_selected_determinantdeterminanthscm_negative_cell) * (S (mdr_q_first_selected_determinantdeterminanths)) + (ff_column_mdm_cell_mdr_first_selected_determinantdeterminanthscm_negative_cell))) * mdr_nc_first_selected_determinantdeterminanth)) /\ exists ff_q_mdm_mdr_first_selected_determinantdeterminanthscm_negative_cell_source. mdr_nb_first_selected_determinantdeterminanth = ff_q_mdm_mdr_first_selected_determinantdeterminanthscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_first_selected_determinantdeterminanthscm_negative_cell) * (S (mdr_q_first_selected_determinantdeterminanths)) + (ff_column_mdm_cell_mdr_first_selected_determinantdeterminanthscm_negative_cell))) * mdr_nc_first_selected_determinantdeterminanth) + (ff_value_mdm_prefix_mdr_first_selected_determinantdeterminanthscm_negative)))))) /\ (((exists ff_h_mdm_mdr_first_selected_determinantdeterminanthscm_negative_target. ff_h_mdm_mdr_first_selected_determinantdeterminanthscm_negative_target + S (ff_value_mdm_prefix_mdr_first_selected_determinantdeterminanthscm_negative) = S ((S (ff_index_mdm_prefix_mdr_first_selected_determinantdeterminanthscm_negative)) * mdr_ut_first_selected_determinantdeterminanthsc)) /\ exists ff_q_mdm_mdr_first_selected_determinantdeterminanthscm_negative_target. mdr_un_first_selected_determinantdeterminanthsc = ff_q_mdm_mdr_first_selected_determinantdeterminanthscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_first_selected_determinantdeterminanthscm_negative)) * mdr_ut_first_selected_determinantdeterminanthsc) + (ff_value_mdm_prefix_mdr_first_selected_determinantdeterminanthscm_negative))))))))) /\ ((((exists ff_h_mdr_first_selected_determinantdeterminanthscp. ff_h_mdr_first_selected_determinantdeterminanthscp + S (mdr_p_first_selected_determinantdeterminanthsc) = S ((S (mdr_j_first_selected_determinantdeterminanthsc)) * mdr_ec_first_selected_determinantdeterminanths)) /\ exists ff_q_mdr_first_selected_determinantdeterminanthscp. mdr_eb_first_selected_determinantdeterminanths = ff_q_mdr_first_selected_determinantdeterminanthscp * S ((S (mdr_j_first_selected_determinantdeterminanthsc)) * mdr_ec_first_selected_determinantdeterminanths) + (mdr_p_first_selected_determinantdeterminanthsc))) /\ (((exists ff_h_mdr_first_selected_determinantdeterminanthscn. ff_h_mdr_first_selected_determinantdeterminanthscn + S (mdr_n_first_selected_determinantdeterminanthsc) = S ((S (mdr_j_first_selected_determinantdeterminanthsc)) * mdr_fc_first_selected_determinantdeterminanths)) /\ exists ff_q_mdr_first_selected_determinantdeterminanthscn. mdr_fb_first_selected_determinantdeterminanths = ff_q_mdr_first_selected_determinantdeterminanthscn * S ((S (mdr_j_first_selected_determinantdeterminanthsc)) * mdr_fc_first_selected_determinantdeterminanths) + (mdr_n_first_selected_determinantdeterminanthsc)))))))) /\ (exists ff_ub_mce_fold_mdr_first_selected_determinantdeterminanthsf ff_uc_mce_fold_mdr_first_selected_determinantdeterminanthsf ff_vb_mce_fold_mdr_first_selected_determinantdeterminanthsf ff_vc_mce_fold_mdr_first_selected_determinantdeterminanthsf. ((forall ff_index_mce_alternating_mdr_first_selected_determinantdeterminanthsf_prefix. (exists ff_gap_mce_mdr_first_selected_determinantdeterminanthsf_prefix_index. ff_gap_mce_mdr_first_selected_determinantdeterminanthsf_prefix_index + S (ff_index_mce_alternating_mdr_first_selected_determinantdeterminanthsf_prefix) = (S (mdr_q_first_selected_determinantdeterminanths))) -> exists ff_ap_mce_alternating_mdr_first_selected_determinantdeterminanthsf_prefix ff_an_mce_alternating_mdr_first_selected_determinantdeterminanthsf_prefix ff_bp_mce_alternating_mdr_first_selected_determinantdeterminanthsf_prefix ff_bn_mce_alternating_mdr_first_selected_determinantdeterminanthsf_prefix ff_p_mce_alternating_mdr_first_selected_determinantdeterminanthsf_prefix ff_n_mce_alternating_mdr_first_selected_determinantdeterminanthsf_prefix. ((((exists ff_h_mce_mdr_first_selected_determinantdeterminanthsf_prefix_ap. ff_h_mce_mdr_first_selected_determinantdeterminanthsf_prefix_ap + S (ff_ap_mce_alternating_mdr_first_selected_determinantdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_first_selected_determinantdeterminanthsf_prefix)) * mdr_pc_first_selected_determinantdeterminanth)) /\ exists ff_q_mce_mdr_first_selected_determinantdeterminanthsf_prefix_ap. mdr_pb_first_selected_determinantdeterminanth = ff_q_mce_mdr_first_selected_determinantdeterminanthsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_first_selected_determinantdeterminanthsf_prefix)) * mdr_pc_first_selected_determinantdeterminanth) + (ff_ap_mce_alternating_mdr_first_selected_determinantdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_first_selected_determinantdeterminanthsf_prefix_an. ff_h_mce_mdr_first_selected_determinantdeterminanthsf_prefix_an + S (ff_an_mce_alternating_mdr_first_selected_determinantdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_first_selected_determinantdeterminanthsf_prefix)) * mdr_nc_first_selected_determinantdeterminanth)) /\ exists ff_q_mce_mdr_first_selected_determinantdeterminanthsf_prefix_an. mdr_nb_first_selected_determinantdeterminanth = ff_q_mce_mdr_first_selected_determinantdeterminanthsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_first_selected_determinantdeterminanthsf_prefix)) * mdr_nc_first_selected_determinantdeterminanth) + (ff_an_mce_alternating_mdr_first_selected_determinantdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_first_selected_determinantdeterminanthsf_prefix_bp. ff_h_mce_mdr_first_selected_determinantdeterminanthsf_prefix_bp + S (ff_bp_mce_alternating_mdr_first_selected_determinantdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_first_selected_determinantdeterminanthsf_prefix)) * mdr_ec_first_selected_determinantdeterminanths)) /\ exists ff_q_mce_mdr_first_selected_determinantdeterminanthsf_prefix_bp. mdr_eb_first_selected_determinantdeterminanths = ff_q_mce_mdr_first_selected_determinantdeterminanthsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_first_selected_determinantdeterminanthsf_prefix)) * mdr_ec_first_selected_determinantdeterminanths) + (ff_bp_mce_alternating_mdr_first_selected_determinantdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_first_selected_determinantdeterminanthsf_prefix_bn. ff_h_mce_mdr_first_selected_determinantdeterminanthsf_prefix_bn + S (ff_bn_mce_alternating_mdr_first_selected_determinantdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_first_selected_determinantdeterminanthsf_prefix)) * mdr_fc_first_selected_determinantdeterminanths)) /\ exists ff_q_mce_mdr_first_selected_determinantdeterminanthsf_prefix_bn. mdr_fb_first_selected_determinantdeterminanths = ff_q_mce_mdr_first_selected_determinantdeterminanthsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_first_selected_determinantdeterminanthsf_prefix)) * mdr_fc_first_selected_determinantdeterminanths) + (ff_bn_mce_alternating_mdr_first_selected_determinantdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_first_selected_determinantdeterminanthsf_prefix_positive. ff_h_mce_mdr_first_selected_determinantdeterminanthsf_prefix_positive + S (ff_p_mce_alternating_mdr_first_selected_determinantdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_first_selected_determinantdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_first_selected_determinantdeterminanthsf)) /\ exists ff_q_mce_mdr_first_selected_determinantdeterminanthsf_prefix_positive. ff_ub_mce_fold_mdr_first_selected_determinantdeterminanthsf = ff_q_mce_mdr_first_selected_determinantdeterminanthsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_first_selected_determinantdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_first_selected_determinantdeterminanthsf) + (ff_p_mce_alternating_mdr_first_selected_determinantdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_first_selected_determinantdeterminanthsf_prefix_negative. ff_h_mce_mdr_first_selected_determinantdeterminanthsf_prefix_negative + S (ff_n_mce_alternating_mdr_first_selected_determinantdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_first_selected_determinantdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_first_selected_determinantdeterminanthsf)) /\ exists ff_q_mce_mdr_first_selected_determinantdeterminanthsf_prefix_negative. ff_vb_mce_fold_mdr_first_selected_determinantdeterminanthsf = ff_q_mce_mdr_first_selected_determinantdeterminanthsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_first_selected_determinantdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_first_selected_determinantdeterminanthsf) + (ff_n_mce_alternating_mdr_first_selected_determinantdeterminanthsf_prefix))) /\ (((exists ff_even_mce_term_mdr_first_selected_determinantdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_first_selected_determinantdeterminanthsf_prefix = 2 * ff_even_mce_term_mdr_first_selected_determinantdeterminanthsf_prefix_term) /\ (ff_p_mce_alternating_mdr_first_selected_determinantdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_first_selected_determinantdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_first_selected_determinantdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_first_selected_determinantdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_first_selected_determinantdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_first_selected_determinantdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_first_selected_determinantdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_first_selected_determinantdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_first_selected_determinantdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_first_selected_determinantdeterminanthsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_first_selected_determinantdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_first_selected_determinantdeterminanthsf_prefix = 2 * ff_odd_mce_term_mdr_first_selected_determinantdeterminanthsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_first_selected_determinantdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_first_selected_determinantdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_first_selected_determinantdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_first_selected_determinantdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_first_selected_determinantdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_first_selected_determinantdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_first_selected_determinantdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_first_selected_determinantdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_first_selected_determinantdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_first_selected_determinantdeterminanthsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_first_selected_determinantdeterminanthsf_positive ff_v_mce_mdr_first_selected_determinantdeterminanthsf_positive. ((((exists ff_h_mce_mdr_first_selected_determinantdeterminanthsf_positive_start. ff_h_mce_mdr_first_selected_determinantdeterminanthsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_first_selected_determinantdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_first_selected_determinantdeterminanthsf_positive_start. ff_u_mce_mdr_first_selected_determinantdeterminanthsf_positive = ff_q_mce_mdr_first_selected_determinantdeterminanthsf_positive_start * S ((S (0)) * ff_v_mce_mdr_first_selected_determinantdeterminanthsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_first_selected_determinantdeterminanthsf_positive_terminal. ff_h_mce_mdr_first_selected_determinantdeterminanthsf_positive_terminal + S (mdr_p_first_selected_determinantdeterminanth) = S ((S ((S (mdr_q_first_selected_determinantdeterminanths)))) * ff_v_mce_mdr_first_selected_determinantdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_first_selected_determinantdeterminanthsf_positive_terminal. ff_u_mce_mdr_first_selected_determinantdeterminanthsf_positive = ff_q_mce_mdr_first_selected_determinantdeterminanthsf_positive_terminal * S ((S ((S (mdr_q_first_selected_determinantdeterminanths)))) * ff_v_mce_mdr_first_selected_determinantdeterminanthsf_positive) + (mdr_p_first_selected_determinantdeterminanth))) /\ forall ff_i_mce_mdr_first_selected_determinantdeterminanthsf_positive. (exists ff_lt_mce_mdr_first_selected_determinantdeterminanthsf_positive_bound. ff_lt_mce_mdr_first_selected_determinantdeterminanthsf_positive_bound + S ff_i_mce_mdr_first_selected_determinantdeterminanthsf_positive = (S (mdr_q_first_selected_determinantdeterminanths))) -> exists ff_a_mce_mdr_first_selected_determinantdeterminanthsf_positive ff_r_mce_mdr_first_selected_determinantdeterminanthsf_positive ff_s_mce_mdr_first_selected_determinantdeterminanthsf_positive. ((((exists ff_h_mce_mdr_first_selected_determinantdeterminanthsf_positive_summand. ff_h_mce_mdr_first_selected_determinantdeterminanthsf_positive_summand + S (ff_a_mce_mdr_first_selected_determinantdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_first_selected_determinantdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_first_selected_determinantdeterminanthsf)) /\ exists ff_q_mce_mdr_first_selected_determinantdeterminanthsf_positive_summand. ff_ub_mce_fold_mdr_first_selected_determinantdeterminanthsf = ff_q_mce_mdr_first_selected_determinantdeterminanthsf_positive_summand * S ((S (ff_i_mce_mdr_first_selected_determinantdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_first_selected_determinantdeterminanthsf) + (ff_a_mce_mdr_first_selected_determinantdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_first_selected_determinantdeterminanthsf_positive_partial. ff_h_mce_mdr_first_selected_determinantdeterminanthsf_positive_partial + S (ff_r_mce_mdr_first_selected_determinantdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_first_selected_determinantdeterminanthsf_positive)) * ff_v_mce_mdr_first_selected_determinantdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_first_selected_determinantdeterminanthsf_positive_partial. ff_u_mce_mdr_first_selected_determinantdeterminanthsf_positive = ff_q_mce_mdr_first_selected_determinantdeterminanthsf_positive_partial * S ((S (ff_i_mce_mdr_first_selected_determinantdeterminanthsf_positive)) * ff_v_mce_mdr_first_selected_determinantdeterminanthsf_positive) + (ff_r_mce_mdr_first_selected_determinantdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_first_selected_determinantdeterminanthsf_positive_successor. ff_h_mce_mdr_first_selected_determinantdeterminanthsf_positive_successor + S (ff_s_mce_mdr_first_selected_determinantdeterminanthsf_positive) = S ((S (S ff_i_mce_mdr_first_selected_determinantdeterminanthsf_positive)) * ff_v_mce_mdr_first_selected_determinantdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_first_selected_determinantdeterminanthsf_positive_successor. ff_u_mce_mdr_first_selected_determinantdeterminanthsf_positive = ff_q_mce_mdr_first_selected_determinantdeterminanthsf_positive_successor * S ((S (S ff_i_mce_mdr_first_selected_determinantdeterminanthsf_positive)) * ff_v_mce_mdr_first_selected_determinantdeterminanthsf_positive) + (ff_s_mce_mdr_first_selected_determinantdeterminanthsf_positive))) /\ ff_s_mce_mdr_first_selected_determinantdeterminanthsf_positive = ff_r_mce_mdr_first_selected_determinantdeterminanthsf_positive + ff_a_mce_mdr_first_selected_determinantdeterminanthsf_positive)))))) /\ (exists ff_u_mce_mdr_first_selected_determinantdeterminanthsf_negative ff_v_mce_mdr_first_selected_determinantdeterminanthsf_negative. ((((exists ff_h_mce_mdr_first_selected_determinantdeterminanthsf_negative_start. ff_h_mce_mdr_first_selected_determinantdeterminanthsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_first_selected_determinantdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_first_selected_determinantdeterminanthsf_negative_start. ff_u_mce_mdr_first_selected_determinantdeterminanthsf_negative = ff_q_mce_mdr_first_selected_determinantdeterminanthsf_negative_start * S ((S (0)) * ff_v_mce_mdr_first_selected_determinantdeterminanthsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_first_selected_determinantdeterminanthsf_negative_terminal. ff_h_mce_mdr_first_selected_determinantdeterminanthsf_negative_terminal + S (mdr_n_first_selected_determinantdeterminanth) = S ((S ((S (mdr_q_first_selected_determinantdeterminanths)))) * ff_v_mce_mdr_first_selected_determinantdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_first_selected_determinantdeterminanthsf_negative_terminal. ff_u_mce_mdr_first_selected_determinantdeterminanthsf_negative = ff_q_mce_mdr_first_selected_determinantdeterminanthsf_negative_terminal * S ((S ((S (mdr_q_first_selected_determinantdeterminanths)))) * ff_v_mce_mdr_first_selected_determinantdeterminanthsf_negative) + (mdr_n_first_selected_determinantdeterminanth))) /\ forall ff_i_mce_mdr_first_selected_determinantdeterminanthsf_negative. (exists ff_lt_mce_mdr_first_selected_determinantdeterminanthsf_negative_bound. ff_lt_mce_mdr_first_selected_determinantdeterminanthsf_negative_bound + S ff_i_mce_mdr_first_selected_determinantdeterminanthsf_negative = (S (mdr_q_first_selected_determinantdeterminanths))) -> exists ff_a_mce_mdr_first_selected_determinantdeterminanthsf_negative ff_r_mce_mdr_first_selected_determinantdeterminanthsf_negative ff_s_mce_mdr_first_selected_determinantdeterminanthsf_negative. ((((exists ff_h_mce_mdr_first_selected_determinantdeterminanthsf_negative_summand. ff_h_mce_mdr_first_selected_determinantdeterminanthsf_negative_summand + S (ff_a_mce_mdr_first_selected_determinantdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_first_selected_determinantdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_first_selected_determinantdeterminanthsf)) /\ exists ff_q_mce_mdr_first_selected_determinantdeterminanthsf_negative_summand. ff_vb_mce_fold_mdr_first_selected_determinantdeterminanthsf = ff_q_mce_mdr_first_selected_determinantdeterminanthsf_negative_summand * S ((S (ff_i_mce_mdr_first_selected_determinantdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_first_selected_determinantdeterminanthsf) + (ff_a_mce_mdr_first_selected_determinantdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_first_selected_determinantdeterminanthsf_negative_partial. ff_h_mce_mdr_first_selected_determinantdeterminanthsf_negative_partial + S (ff_r_mce_mdr_first_selected_determinantdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_first_selected_determinantdeterminanthsf_negative)) * ff_v_mce_mdr_first_selected_determinantdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_first_selected_determinantdeterminanthsf_negative_partial. ff_u_mce_mdr_first_selected_determinantdeterminanthsf_negative = ff_q_mce_mdr_first_selected_determinantdeterminanthsf_negative_partial * S ((S (ff_i_mce_mdr_first_selected_determinantdeterminanthsf_negative)) * ff_v_mce_mdr_first_selected_determinantdeterminanthsf_negative) + (ff_r_mce_mdr_first_selected_determinantdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_first_selected_determinantdeterminanthsf_negative_successor. ff_h_mce_mdr_first_selected_determinantdeterminanthsf_negative_successor + S (ff_s_mce_mdr_first_selected_determinantdeterminanthsf_negative) = S ((S (S ff_i_mce_mdr_first_selected_determinantdeterminanthsf_negative)) * ff_v_mce_mdr_first_selected_determinantdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_first_selected_determinantdeterminanthsf_negative_successor. ff_u_mce_mdr_first_selected_determinantdeterminanthsf_negative = ff_q_mce_mdr_first_selected_determinantdeterminanthsf_negative_successor * S ((S (S ff_i_mce_mdr_first_selected_determinantdeterminanthsf_negative)) * ff_v_mce_mdr_first_selected_determinantdeterminanthsf_negative) + (ff_s_mce_mdr_first_selected_determinantdeterminanthsf_negative))) /\ ff_s_mce_mdr_first_selected_determinantdeterminanthsf_negative = ff_r_mce_mdr_first_selected_determinantdeterminanthsf_negative + ff_a_mce_mdr_first_selected_determinantdeterminanthsf_negative))))))))))))))) /\ ((exists mdr_gap_first_selected_determinantdeterminanti. mdr_gap_first_selected_determinantdeterminanti + S (mdr_i_first_selected_determinantdeterminant) = (mdr_l_first_selected_determinantdeterminant)) /\ (exists mdr_z_first_selected_determinantdeterminantr. ((exists mdr_a_first_selected_determinantdeterminantrc mdr_b_first_selected_determinantdeterminantrc mdr_c_first_selected_determinantdeterminantrc mdr_e_first_selected_determinantdeterminantrc mdr_f_first_selected_determinantdeterminantrc. ((mdr_a_first_selected_determinantdeterminantrc = ((q) + (mdr_ub_first_selected_determinant)) * S ((q) + (mdr_ub_first_selected_determinant)) + ((mdr_ub_first_selected_determinant) + (mdr_ub_first_selected_determinant))) /\ ((mdr_b_first_selected_determinantdeterminantrc = ((mdr_uc_first_selected_determinant) + (mdr_vb_first_selected_determinant)) * S ((mdr_uc_first_selected_determinant) + (mdr_vb_first_selected_determinant)) + ((mdr_vb_first_selected_determinant) + (mdr_vb_first_selected_determinant))) /\ ((mdr_c_first_selected_determinantdeterminantrc = ((mdr_a_first_selected_determinantdeterminantrc) + (mdr_b_first_selected_determinantdeterminantrc)) * S ((mdr_a_first_selected_determinantdeterminantrc) + (mdr_b_first_selected_determinantdeterminantrc)) + ((mdr_b_first_selected_determinantdeterminantrc) + (mdr_b_first_selected_determinantdeterminantrc))) /\ ((mdr_e_first_selected_determinantdeterminantrc = ((p) + (n)) * S ((p) + (n)) + ((n) + (n))) /\ ((mdr_f_first_selected_determinantdeterminantrc = ((mdr_vc_first_selected_determinant) + (mdr_e_first_selected_determinantdeterminantrc)) * S ((mdr_vc_first_selected_determinant) + (mdr_e_first_selected_determinantdeterminantrc)) + ((mdr_e_first_selected_determinantdeterminantrc) + (mdr_e_first_selected_determinantdeterminantrc))) /\ ((mdr_z_first_selected_determinantdeterminantr) = ((mdr_c_first_selected_determinantdeterminantrc) + (mdr_f_first_selected_determinantdeterminantrc)) * S ((mdr_c_first_selected_determinantdeterminantrc) + (mdr_f_first_selected_determinantdeterminantrc)) + ((mdr_f_first_selected_determinantdeterminantrc) + (mdr_f_first_selected_determinantdeterminantrc))))))))) /\ (((exists ff_h_mdr_first_selected_determinantdeterminantrb. ff_h_mdr_first_selected_determinantdeterminantrb + S (mdr_z_first_selected_determinantdeterminantr) = S ((S (mdr_i_first_selected_determinantdeterminant)) * mdr_c_first_selected_determinantdeterminant)) /\ exists ff_q_mdr_first_selected_determinantdeterminantrb. mdr_b_first_selected_determinantdeterminant = ff_q_mdr_first_selected_determinantdeterminantrb * S ((S (mdr_i_first_selected_determinantdeterminant)) * mdr_c_first_selected_determinantdeterminant) + (mdr_z_first_selected_determinantdeterminantr)))))))))) -> (exists mdr_ub_second_selected_determinant mdr_uc_second_selected_determinant mdr_vb_second_selected_determinant mdr_vc_second_selected_determinant. ((((forall mdr_i_second_selected_determinantmatrixpositive. (exists mdr_gap_second_selected_determinantmatrixpositivebound. mdr_gap_second_selected_determinantmatrixpositivebound + S (mdr_i_second_selected_determinantmatrixpositive) = ((q) * (q))) -> exists mdr_a_second_selected_determinantmatrixpositive. (((exists mdr_r_second_selected_determinantmatrixpositivepoint mdr_s_second_selected_determinantmatrixpositivepoint mdr_u_second_selected_determinantmatrixpositivepoint mdr_v_second_selected_determinantmatrixpositivepoint. ((mdr_i_second_selected_determinantmatrixpositive = (q) * mdr_r_second_selected_determinantmatrixpositivepoint + mdr_s_second_selected_determinantmatrixpositivepoint) /\ ((exists mdr_gap_second_selected_determinantmatrixpositivepointcolumn. mdr_gap_second_selected_determinantmatrixpositivepointcolumn + S (mdr_s_second_selected_determinantmatrixpositivepoint) = (q)) /\ ((((exists ff_h_mdr_second_selected_determinantmatrixpositivepointrow_index. ff_h_mdr_second_selected_determinantmatrixpositivepointrow_index + S (mdr_u_second_selected_determinantmatrixpositivepoint) = S ((S (mdr_r_second_selected_determinantmatrixpositivepoint)) * rc)) /\ exists ff_q_mdr_second_selected_determinantmatrixpositivepointrow_index. rb = ff_q_mdr_second_selected_determinantmatrixpositivepointrow_index * S ((S (mdr_r_second_selected_determinantmatrixpositivepoint)) * rc) + (mdr_u_second_selected_determinantmatrixpositivepoint))) /\ ((((exists ff_h_mdr_second_selected_determinantmatrixpositivepointcolumn_index. ff_h_mdr_second_selected_determinantmatrixpositivepointcolumn_index + S (mdr_v_second_selected_determinantmatrixpositivepoint) = S ((S (mdr_s_second_selected_determinantmatrixpositivepoint)) * cc)) /\ exists ff_q_mdr_second_selected_determinantmatrixpositivepointcolumn_index. cb = ff_q_mdr_second_selected_determinantmatrixpositivepointcolumn_index * S ((S (mdr_s_second_selected_determinantmatrixpositivepoint)) * cc) + (mdr_v_second_selected_determinantmatrixpositivepoint))) /\ (((exists ff_h_mdr_second_selected_determinantmatrixpositivepointsource. ff_h_mdr_second_selected_determinantmatrixpositivepointsource + S (mdr_a_second_selected_determinantmatrixpositive) = S ((S ((mdr_u_second_selected_determinantmatrixpositivepoint) * (w) + (mdr_v_second_selected_determinantmatrixpositivepoint))) * ec)) /\ exists ff_q_mdr_second_selected_determinantmatrixpositivepointsource. eb = ff_q_mdr_second_selected_determinantmatrixpositivepointsource * S ((S ((mdr_u_second_selected_determinantmatrixpositivepoint) * (w) + (mdr_v_second_selected_determinantmatrixpositivepoint))) * ec) + (mdr_a_second_selected_determinantmatrixpositive)))))))) /\ (((exists ff_h_mdr_second_selected_determinantmatrixpositiveoutput. ff_h_mdr_second_selected_determinantmatrixpositiveoutput + S (mdr_a_second_selected_determinantmatrixpositive) = S ((S (mdr_i_second_selected_determinantmatrixpositive)) * mdr_uc_second_selected_determinant)) /\ exists ff_q_mdr_second_selected_determinantmatrixpositiveoutput. mdr_ub_second_selected_determinant = ff_q_mdr_second_selected_determinantmatrixpositiveoutput * S ((S (mdr_i_second_selected_determinantmatrixpositive)) * mdr_uc_second_selected_determinant) + (mdr_a_second_selected_determinantmatrixpositive)))))) /\ (forall mdr_i_second_selected_determinantmatrixnegative. (exists mdr_gap_second_selected_determinantmatrixnegativebound. mdr_gap_second_selected_determinantmatrixnegativebound + S (mdr_i_second_selected_determinantmatrixnegative) = ((q) * (q))) -> exists mdr_a_second_selected_determinantmatrixnegative. (((exists mdr_r_second_selected_determinantmatrixnegativepoint mdr_s_second_selected_determinantmatrixnegativepoint mdr_u_second_selected_determinantmatrixnegativepoint mdr_v_second_selected_determinantmatrixnegativepoint. ((mdr_i_second_selected_determinantmatrixnegative = (q) * mdr_r_second_selected_determinantmatrixnegativepoint + mdr_s_second_selected_determinantmatrixnegativepoint) /\ ((exists mdr_gap_second_selected_determinantmatrixnegativepointcolumn. mdr_gap_second_selected_determinantmatrixnegativepointcolumn + S (mdr_s_second_selected_determinantmatrixnegativepoint) = (q)) /\ ((((exists ff_h_mdr_second_selected_determinantmatrixnegativepointrow_index. ff_h_mdr_second_selected_determinantmatrixnegativepointrow_index + S (mdr_u_second_selected_determinantmatrixnegativepoint) = S ((S (mdr_r_second_selected_determinantmatrixnegativepoint)) * rc)) /\ exists ff_q_mdr_second_selected_determinantmatrixnegativepointrow_index. rb = ff_q_mdr_second_selected_determinantmatrixnegativepointrow_index * S ((S (mdr_r_second_selected_determinantmatrixnegativepoint)) * rc) + (mdr_u_second_selected_determinantmatrixnegativepoint))) /\ ((((exists ff_h_mdr_second_selected_determinantmatrixnegativepointcolumn_index. ff_h_mdr_second_selected_determinantmatrixnegativepointcolumn_index + S (mdr_v_second_selected_determinantmatrixnegativepoint) = S ((S (mdr_s_second_selected_determinantmatrixnegativepoint)) * cc)) /\ exists ff_q_mdr_second_selected_determinantmatrixnegativepointcolumn_index. cb = ff_q_mdr_second_selected_determinantmatrixnegativepointcolumn_index * S ((S (mdr_s_second_selected_determinantmatrixnegativepoint)) * cc) + (mdr_v_second_selected_determinantmatrixnegativepoint))) /\ (((exists ff_h_mdr_second_selected_determinantmatrixnegativepointsource. ff_h_mdr_second_selected_determinantmatrixnegativepointsource + S (mdr_a_second_selected_determinantmatrixnegative) = S ((S ((mdr_u_second_selected_determinantmatrixnegativepoint) * (w) + (mdr_v_second_selected_determinantmatrixnegativepoint))) * fc)) /\ exists ff_q_mdr_second_selected_determinantmatrixnegativepointsource. fb = ff_q_mdr_second_selected_determinantmatrixnegativepointsource * S ((S ((mdr_u_second_selected_determinantmatrixnegativepoint) * (w) + (mdr_v_second_selected_determinantmatrixnegativepoint))) * fc) + (mdr_a_second_selected_determinantmatrixnegative)))))))) /\ (((exists ff_h_mdr_second_selected_determinantmatrixnegativeoutput. ff_h_mdr_second_selected_determinantmatrixnegativeoutput + S (mdr_a_second_selected_determinantmatrixnegative) = S ((S (mdr_i_second_selected_determinantmatrixnegative)) * mdr_vc_second_selected_determinant)) /\ exists ff_q_mdr_second_selected_determinantmatrixnegativeoutput. mdr_vb_second_selected_determinant = ff_q_mdr_second_selected_determinantmatrixnegativeoutput * S ((S (mdr_i_second_selected_determinantmatrixnegative)) * mdr_vc_second_selected_determinant) + (mdr_a_second_selected_determinantmatrixnegative)))))))) /\ (exists mdr_b_second_selected_determinantdeterminant mdr_c_second_selected_determinantdeterminant mdr_l_second_selected_determinantdeterminant mdr_i_second_selected_determinantdeterminant. ((forall mdr_i_second_selected_determinantdeterminanth. (exists mdr_gap_second_selected_determinantdeterminanthi. mdr_gap_second_selected_determinantdeterminanthi + S (mdr_i_second_selected_determinantdeterminanth) = (mdr_l_second_selected_determinantdeterminant)) -> exists mdr_d_second_selected_determinantdeterminanth mdr_pb_second_selected_determinantdeterminanth mdr_pc_second_selected_determinantdeterminanth mdr_nb_second_selected_determinantdeterminanth mdr_nc_second_selected_determinantdeterminanth mdr_p_second_selected_determinantdeterminanth mdr_n_second_selected_determinantdeterminanth. ((exists mdr_z_second_selected_determinantdeterminanthr. ((exists mdr_a_second_selected_determinantdeterminanthrc mdr_b_second_selected_determinantdeterminanthrc mdr_c_second_selected_determinantdeterminanthrc mdr_e_second_selected_determinantdeterminanthrc mdr_f_second_selected_determinantdeterminanthrc. ((mdr_a_second_selected_determinantdeterminanthrc = ((mdr_d_second_selected_determinantdeterminanth) + (mdr_pb_second_selected_determinantdeterminanth)) * S ((mdr_d_second_selected_determinantdeterminanth) + (mdr_pb_second_selected_determinantdeterminanth)) + ((mdr_pb_second_selected_determinantdeterminanth) + (mdr_pb_second_selected_determinantdeterminanth))) /\ ((mdr_b_second_selected_determinantdeterminanthrc = ((mdr_pc_second_selected_determinantdeterminanth) + (mdr_nb_second_selected_determinantdeterminanth)) * S ((mdr_pc_second_selected_determinantdeterminanth) + (mdr_nb_second_selected_determinantdeterminanth)) + ((mdr_nb_second_selected_determinantdeterminanth) + (mdr_nb_second_selected_determinantdeterminanth))) /\ ((mdr_c_second_selected_determinantdeterminanthrc = ((mdr_a_second_selected_determinantdeterminanthrc) + (mdr_b_second_selected_determinantdeterminanthrc)) * S ((mdr_a_second_selected_determinantdeterminanthrc) + (mdr_b_second_selected_determinantdeterminanthrc)) + ((mdr_b_second_selected_determinantdeterminanthrc) + (mdr_b_second_selected_determinantdeterminanthrc))) /\ ((mdr_e_second_selected_determinantdeterminanthrc = ((mdr_p_second_selected_determinantdeterminanth) + (mdr_n_second_selected_determinantdeterminanth)) * S ((mdr_p_second_selected_determinantdeterminanth) + (mdr_n_second_selected_determinantdeterminanth)) + ((mdr_n_second_selected_determinantdeterminanth) + (mdr_n_second_selected_determinantdeterminanth))) /\ ((mdr_f_second_selected_determinantdeterminanthrc = ((mdr_nc_second_selected_determinantdeterminanth) + (mdr_e_second_selected_determinantdeterminanthrc)) * S ((mdr_nc_second_selected_determinantdeterminanth) + (mdr_e_second_selected_determinantdeterminanthrc)) + ((mdr_e_second_selected_determinantdeterminanthrc) + (mdr_e_second_selected_determinantdeterminanthrc))) /\ ((mdr_z_second_selected_determinantdeterminanthr) = ((mdr_c_second_selected_determinantdeterminanthrc) + (mdr_f_second_selected_determinantdeterminanthrc)) * S ((mdr_c_second_selected_determinantdeterminanthrc) + (mdr_f_second_selected_determinantdeterminanthrc)) + ((mdr_f_second_selected_determinantdeterminanthrc) + (mdr_f_second_selected_determinantdeterminanthrc))))))))) /\ (((exists ff_h_mdr_second_selected_determinantdeterminanthrb. ff_h_mdr_second_selected_determinantdeterminanthrb + S (mdr_z_second_selected_determinantdeterminanthr) = S ((S (mdr_i_second_selected_determinantdeterminanth)) * mdr_c_second_selected_determinantdeterminant)) /\ exists ff_q_mdr_second_selected_determinantdeterminanthrb. mdr_b_second_selected_determinantdeterminant = ff_q_mdr_second_selected_determinantdeterminanthrb * S ((S (mdr_i_second_selected_determinantdeterminanth)) * mdr_c_second_selected_determinantdeterminant) + (mdr_z_second_selected_determinantdeterminanthr))))) /\ (((((mdr_d_second_selected_determinantdeterminanth) = 0) /\ (((mdr_p_second_selected_determinantdeterminanth) = 1) /\ ((mdr_n_second_selected_determinantdeterminanth) = 0))) \/ exists mdr_q_second_selected_determinantdeterminanths mdr_eb_second_selected_determinantdeterminanths mdr_ec_second_selected_determinantdeterminanths mdr_fb_second_selected_determinantdeterminanths mdr_fc_second_selected_determinantdeterminanths. (((mdr_d_second_selected_determinantdeterminanth) = S (mdr_q_second_selected_determinantdeterminanths)) /\ ((forall mdr_j_second_selected_determinantdeterminanthsc. (exists mdr_gap_second_selected_determinantdeterminanthscj. mdr_gap_second_selected_determinantdeterminanthscj + S (mdr_j_second_selected_determinantdeterminanthsc) = (S (mdr_q_second_selected_determinantdeterminanths))) -> exists mdr_i_second_selected_determinantdeterminanthsc mdr_up_second_selected_determinantdeterminanthsc mdr_us_second_selected_determinantdeterminanthsc mdr_un_second_selected_determinantdeterminanthsc mdr_ut_second_selected_determinantdeterminanthsc mdr_p_second_selected_determinantdeterminanthsc mdr_n_second_selected_determinantdeterminanthsc. ((exists mdr_gap_second_selected_determinantdeterminanthsci. mdr_gap_second_selected_determinantdeterminanthsci + S (mdr_i_second_selected_determinantdeterminanthsc) = (mdr_i_second_selected_determinantdeterminanth)) /\ ((exists mdr_z_second_selected_determinantdeterminanthscr. ((exists mdr_a_second_selected_determinantdeterminanthscrc mdr_b_second_selected_determinantdeterminanthscrc mdr_c_second_selected_determinantdeterminanthscrc mdr_e_second_selected_determinantdeterminanthscrc mdr_f_second_selected_determinantdeterminanthscrc. ((mdr_a_second_selected_determinantdeterminanthscrc = ((mdr_q_second_selected_determinantdeterminanths) + (mdr_up_second_selected_determinantdeterminanthsc)) * S ((mdr_q_second_selected_determinantdeterminanths) + (mdr_up_second_selected_determinantdeterminanthsc)) + ((mdr_up_second_selected_determinantdeterminanthsc) + (mdr_up_second_selected_determinantdeterminanthsc))) /\ ((mdr_b_second_selected_determinantdeterminanthscrc = ((mdr_us_second_selected_determinantdeterminanthsc) + (mdr_un_second_selected_determinantdeterminanthsc)) * S ((mdr_us_second_selected_determinantdeterminanthsc) + (mdr_un_second_selected_determinantdeterminanthsc)) + ((mdr_un_second_selected_determinantdeterminanthsc) + (mdr_un_second_selected_determinantdeterminanthsc))) /\ ((mdr_c_second_selected_determinantdeterminanthscrc = ((mdr_a_second_selected_determinantdeterminanthscrc) + (mdr_b_second_selected_determinantdeterminanthscrc)) * S ((mdr_a_second_selected_determinantdeterminanthscrc) + (mdr_b_second_selected_determinantdeterminanthscrc)) + ((mdr_b_second_selected_determinantdeterminanthscrc) + (mdr_b_second_selected_determinantdeterminanthscrc))) /\ ((mdr_e_second_selected_determinantdeterminanthscrc = ((mdr_p_second_selected_determinantdeterminanthsc) + (mdr_n_second_selected_determinantdeterminanthsc)) * S ((mdr_p_second_selected_determinantdeterminanthsc) + (mdr_n_second_selected_determinantdeterminanthsc)) + ((mdr_n_second_selected_determinantdeterminanthsc) + (mdr_n_second_selected_determinantdeterminanthsc))) /\ ((mdr_f_second_selected_determinantdeterminanthscrc = ((mdr_ut_second_selected_determinantdeterminanthsc) + (mdr_e_second_selected_determinantdeterminanthscrc)) * S ((mdr_ut_second_selected_determinantdeterminanthsc) + (mdr_e_second_selected_determinantdeterminanthscrc)) + ((mdr_e_second_selected_determinantdeterminanthscrc) + (mdr_e_second_selected_determinantdeterminanthscrc))) /\ ((mdr_z_second_selected_determinantdeterminanthscr) = ((mdr_c_second_selected_determinantdeterminanthscrc) + (mdr_f_second_selected_determinantdeterminanthscrc)) * S ((mdr_c_second_selected_determinantdeterminanthscrc) + (mdr_f_second_selected_determinantdeterminanthscrc)) + ((mdr_f_second_selected_determinantdeterminanthscrc) + (mdr_f_second_selected_determinantdeterminanthscrc))))))))) /\ (((exists ff_h_mdr_second_selected_determinantdeterminanthscrb. ff_h_mdr_second_selected_determinantdeterminanthscrb + S (mdr_z_second_selected_determinantdeterminanthscr) = S ((S (mdr_i_second_selected_determinantdeterminanthsc)) * mdr_c_second_selected_determinantdeterminant)) /\ exists ff_q_mdr_second_selected_determinantdeterminanthscrb. mdr_b_second_selected_determinantdeterminant = ff_q_mdr_second_selected_determinantdeterminanthscrb * S ((S (mdr_i_second_selected_determinantdeterminanthsc)) * mdr_c_second_selected_determinantdeterminant) + (mdr_z_second_selected_determinantdeterminanthscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_second_selected_determinantdeterminanthscm_positive. (exists ff_gap_mdm_lt_mdr_second_selected_determinantdeterminanthscm_positive_index_bound. ff_gap_mdm_lt_mdr_second_selected_determinantdeterminanthscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_second_selected_determinantdeterminanthscm_positive) = ((mdr_q_second_selected_determinantdeterminanths) * (mdr_q_second_selected_determinantdeterminanths))) -> exists ff_row_mdm_prefix_mdr_second_selected_determinantdeterminanthscm_positive ff_column_mdm_prefix_mdr_second_selected_determinantdeterminanthscm_positive ff_value_mdm_prefix_mdr_second_selected_determinantdeterminanthscm_positive. (ff_index_mdm_prefix_mdr_second_selected_determinantdeterminanthscm_positive = (mdr_q_second_selected_determinantdeterminanths) * ff_row_mdm_prefix_mdr_second_selected_determinantdeterminanthscm_positive + ff_column_mdm_prefix_mdr_second_selected_determinantdeterminanthscm_positive /\ ((exists ff_gap_mdm_lt_mdr_second_selected_determinantdeterminanthscm_positive_column_bound. ff_gap_mdm_lt_mdr_second_selected_determinantdeterminanthscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_second_selected_determinantdeterminanthscm_positive) = (mdr_q_second_selected_determinantdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_second_selected_determinantdeterminanthscm_positive_cell ff_column_mdm_cell_mdr_second_selected_determinantdeterminanthscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_second_selected_determinantdeterminanthscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_second_selected_determinantdeterminanthscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_second_selected_determinantdeterminanthscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_second_selected_determinantdeterminanthscm_positive_cell = ff_row_mdm_prefix_mdr_second_selected_determinantdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_second_selected_determinantdeterminanthscm_positive_cell_row_after. ff_gap_mdm_le_mdr_second_selected_determinantdeterminanthscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_second_selected_determinantdeterminanthscm_positive)) /\ ff_row_mdm_cell_mdr_second_selected_determinantdeterminanthscm_positive_cell = S ff_row_mdm_prefix_mdr_second_selected_determinantdeterminanthscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_second_selected_determinantdeterminanthscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_second_selected_determinantdeterminanthscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_second_selected_determinantdeterminanthscm_positive) = (mdr_j_second_selected_determinantdeterminanthsc)) /\ ff_column_mdm_cell_mdr_second_selected_determinantdeterminanthscm_positive_cell = ff_column_mdm_prefix_mdr_second_selected_determinantdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_second_selected_determinantdeterminanthscm_positive_cell_column_after. ff_gap_mdm_le_mdr_second_selected_determinantdeterminanthscm_positive_cell_column_after + (mdr_j_second_selected_determinantdeterminanthsc) = (ff_column_mdm_prefix_mdr_second_selected_determinantdeterminanthscm_positive)) /\ ff_column_mdm_cell_mdr_second_selected_determinantdeterminanthscm_positive_cell = S ff_column_mdm_prefix_mdr_second_selected_determinantdeterminanthscm_positive))) /\ (((exists ff_h_mdm_mdr_second_selected_determinantdeterminanthscm_positive_cell_source. ff_h_mdm_mdr_second_selected_determinantdeterminanthscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_second_selected_determinantdeterminanthscm_positive) = S ((S ((ff_row_mdm_cell_mdr_second_selected_determinantdeterminanthscm_positive_cell) * (S (mdr_q_second_selected_determinantdeterminanths)) + (ff_column_mdm_cell_mdr_second_selected_determinantdeterminanthscm_positive_cell))) * mdr_pc_second_selected_determinantdeterminanth)) /\ exists ff_q_mdm_mdr_second_selected_determinantdeterminanthscm_positive_cell_source. mdr_pb_second_selected_determinantdeterminanth = ff_q_mdm_mdr_second_selected_determinantdeterminanthscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_second_selected_determinantdeterminanthscm_positive_cell) * (S (mdr_q_second_selected_determinantdeterminanths)) + (ff_column_mdm_cell_mdr_second_selected_determinantdeterminanthscm_positive_cell))) * mdr_pc_second_selected_determinantdeterminanth) + (ff_value_mdm_prefix_mdr_second_selected_determinantdeterminanthscm_positive)))))) /\ (((exists ff_h_mdm_mdr_second_selected_determinantdeterminanthscm_positive_target. ff_h_mdm_mdr_second_selected_determinantdeterminanthscm_positive_target + S (ff_value_mdm_prefix_mdr_second_selected_determinantdeterminanthscm_positive) = S ((S (ff_index_mdm_prefix_mdr_second_selected_determinantdeterminanthscm_positive)) * mdr_us_second_selected_determinantdeterminanthsc)) /\ exists ff_q_mdm_mdr_second_selected_determinantdeterminanthscm_positive_target. mdr_up_second_selected_determinantdeterminanthsc = ff_q_mdm_mdr_second_selected_determinantdeterminanthscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_second_selected_determinantdeterminanthscm_positive)) * mdr_us_second_selected_determinantdeterminanthsc) + (ff_value_mdm_prefix_mdr_second_selected_determinantdeterminanthscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_second_selected_determinantdeterminanthscm_negative. (exists ff_gap_mdm_lt_mdr_second_selected_determinantdeterminanthscm_negative_index_bound. ff_gap_mdm_lt_mdr_second_selected_determinantdeterminanthscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_second_selected_determinantdeterminanthscm_negative) = ((mdr_q_second_selected_determinantdeterminanths) * (mdr_q_second_selected_determinantdeterminanths))) -> exists ff_row_mdm_prefix_mdr_second_selected_determinantdeterminanthscm_negative ff_column_mdm_prefix_mdr_second_selected_determinantdeterminanthscm_negative ff_value_mdm_prefix_mdr_second_selected_determinantdeterminanthscm_negative. (ff_index_mdm_prefix_mdr_second_selected_determinantdeterminanthscm_negative = (mdr_q_second_selected_determinantdeterminanths) * ff_row_mdm_prefix_mdr_second_selected_determinantdeterminanthscm_negative + ff_column_mdm_prefix_mdr_second_selected_determinantdeterminanthscm_negative /\ ((exists ff_gap_mdm_lt_mdr_second_selected_determinantdeterminanthscm_negative_column_bound. ff_gap_mdm_lt_mdr_second_selected_determinantdeterminanthscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_second_selected_determinantdeterminanthscm_negative) = (mdr_q_second_selected_determinantdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_second_selected_determinantdeterminanthscm_negative_cell ff_column_mdm_cell_mdr_second_selected_determinantdeterminanthscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_second_selected_determinantdeterminanthscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_second_selected_determinantdeterminanthscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_second_selected_determinantdeterminanthscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_second_selected_determinantdeterminanthscm_negative_cell = ff_row_mdm_prefix_mdr_second_selected_determinantdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_second_selected_determinantdeterminanthscm_negative_cell_row_after. ff_gap_mdm_le_mdr_second_selected_determinantdeterminanthscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_second_selected_determinantdeterminanthscm_negative)) /\ ff_row_mdm_cell_mdr_second_selected_determinantdeterminanthscm_negative_cell = S ff_row_mdm_prefix_mdr_second_selected_determinantdeterminanthscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_second_selected_determinantdeterminanthscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_second_selected_determinantdeterminanthscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_second_selected_determinantdeterminanthscm_negative) = (mdr_j_second_selected_determinantdeterminanthsc)) /\ ff_column_mdm_cell_mdr_second_selected_determinantdeterminanthscm_negative_cell = ff_column_mdm_prefix_mdr_second_selected_determinantdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_second_selected_determinantdeterminanthscm_negative_cell_column_after. ff_gap_mdm_le_mdr_second_selected_determinantdeterminanthscm_negative_cell_column_after + (mdr_j_second_selected_determinantdeterminanthsc) = (ff_column_mdm_prefix_mdr_second_selected_determinantdeterminanthscm_negative)) /\ ff_column_mdm_cell_mdr_second_selected_determinantdeterminanthscm_negative_cell = S ff_column_mdm_prefix_mdr_second_selected_determinantdeterminanthscm_negative))) /\ (((exists ff_h_mdm_mdr_second_selected_determinantdeterminanthscm_negative_cell_source. ff_h_mdm_mdr_second_selected_determinantdeterminanthscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_second_selected_determinantdeterminanthscm_negative) = S ((S ((ff_row_mdm_cell_mdr_second_selected_determinantdeterminanthscm_negative_cell) * (S (mdr_q_second_selected_determinantdeterminanths)) + (ff_column_mdm_cell_mdr_second_selected_determinantdeterminanthscm_negative_cell))) * mdr_nc_second_selected_determinantdeterminanth)) /\ exists ff_q_mdm_mdr_second_selected_determinantdeterminanthscm_negative_cell_source. mdr_nb_second_selected_determinantdeterminanth = ff_q_mdm_mdr_second_selected_determinantdeterminanthscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_second_selected_determinantdeterminanthscm_negative_cell) * (S (mdr_q_second_selected_determinantdeterminanths)) + (ff_column_mdm_cell_mdr_second_selected_determinantdeterminanthscm_negative_cell))) * mdr_nc_second_selected_determinantdeterminanth) + (ff_value_mdm_prefix_mdr_second_selected_determinantdeterminanthscm_negative)))))) /\ (((exists ff_h_mdm_mdr_second_selected_determinantdeterminanthscm_negative_target. ff_h_mdm_mdr_second_selected_determinantdeterminanthscm_negative_target + S (ff_value_mdm_prefix_mdr_second_selected_determinantdeterminanthscm_negative) = S ((S (ff_index_mdm_prefix_mdr_second_selected_determinantdeterminanthscm_negative)) * mdr_ut_second_selected_determinantdeterminanthsc)) /\ exists ff_q_mdm_mdr_second_selected_determinantdeterminanthscm_negative_target. mdr_un_second_selected_determinantdeterminanthsc = ff_q_mdm_mdr_second_selected_determinantdeterminanthscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_second_selected_determinantdeterminanthscm_negative)) * mdr_ut_second_selected_determinantdeterminanthsc) + (ff_value_mdm_prefix_mdr_second_selected_determinantdeterminanthscm_negative))))))))) /\ ((((exists ff_h_mdr_second_selected_determinantdeterminanthscp. ff_h_mdr_second_selected_determinantdeterminanthscp + S (mdr_p_second_selected_determinantdeterminanthsc) = S ((S (mdr_j_second_selected_determinantdeterminanthsc)) * mdr_ec_second_selected_determinantdeterminanths)) /\ exists ff_q_mdr_second_selected_determinantdeterminanthscp. mdr_eb_second_selected_determinantdeterminanths = ff_q_mdr_second_selected_determinantdeterminanthscp * S ((S (mdr_j_second_selected_determinantdeterminanthsc)) * mdr_ec_second_selected_determinantdeterminanths) + (mdr_p_second_selected_determinantdeterminanthsc))) /\ (((exists ff_h_mdr_second_selected_determinantdeterminanthscn. ff_h_mdr_second_selected_determinantdeterminanthscn + S (mdr_n_second_selected_determinantdeterminanthsc) = S ((S (mdr_j_second_selected_determinantdeterminanthsc)) * mdr_fc_second_selected_determinantdeterminanths)) /\ exists ff_q_mdr_second_selected_determinantdeterminanthscn. mdr_fb_second_selected_determinantdeterminanths = ff_q_mdr_second_selected_determinantdeterminanthscn * S ((S (mdr_j_second_selected_determinantdeterminanthsc)) * mdr_fc_second_selected_determinantdeterminanths) + (mdr_n_second_selected_determinantdeterminanthsc)))))))) /\ (exists ff_ub_mce_fold_mdr_second_selected_determinantdeterminanthsf ff_uc_mce_fold_mdr_second_selected_determinantdeterminanthsf ff_vb_mce_fold_mdr_second_selected_determinantdeterminanthsf ff_vc_mce_fold_mdr_second_selected_determinantdeterminanthsf. ((forall ff_index_mce_alternating_mdr_second_selected_determinantdeterminanthsf_prefix. (exists ff_gap_mce_mdr_second_selected_determinantdeterminanthsf_prefix_index. ff_gap_mce_mdr_second_selected_determinantdeterminanthsf_prefix_index + S (ff_index_mce_alternating_mdr_second_selected_determinantdeterminanthsf_prefix) = (S (mdr_q_second_selected_determinantdeterminanths))) -> exists ff_ap_mce_alternating_mdr_second_selected_determinantdeterminanthsf_prefix ff_an_mce_alternating_mdr_second_selected_determinantdeterminanthsf_prefix ff_bp_mce_alternating_mdr_second_selected_determinantdeterminanthsf_prefix ff_bn_mce_alternating_mdr_second_selected_determinantdeterminanthsf_prefix ff_p_mce_alternating_mdr_second_selected_determinantdeterminanthsf_prefix ff_n_mce_alternating_mdr_second_selected_determinantdeterminanthsf_prefix. ((((exists ff_h_mce_mdr_second_selected_determinantdeterminanthsf_prefix_ap. ff_h_mce_mdr_second_selected_determinantdeterminanthsf_prefix_ap + S (ff_ap_mce_alternating_mdr_second_selected_determinantdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_second_selected_determinantdeterminanthsf_prefix)) * mdr_pc_second_selected_determinantdeterminanth)) /\ exists ff_q_mce_mdr_second_selected_determinantdeterminanthsf_prefix_ap. mdr_pb_second_selected_determinantdeterminanth = ff_q_mce_mdr_second_selected_determinantdeterminanthsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_second_selected_determinantdeterminanthsf_prefix)) * mdr_pc_second_selected_determinantdeterminanth) + (ff_ap_mce_alternating_mdr_second_selected_determinantdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_second_selected_determinantdeterminanthsf_prefix_an. ff_h_mce_mdr_second_selected_determinantdeterminanthsf_prefix_an + S (ff_an_mce_alternating_mdr_second_selected_determinantdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_second_selected_determinantdeterminanthsf_prefix)) * mdr_nc_second_selected_determinantdeterminanth)) /\ exists ff_q_mce_mdr_second_selected_determinantdeterminanthsf_prefix_an. mdr_nb_second_selected_determinantdeterminanth = ff_q_mce_mdr_second_selected_determinantdeterminanthsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_second_selected_determinantdeterminanthsf_prefix)) * mdr_nc_second_selected_determinantdeterminanth) + (ff_an_mce_alternating_mdr_second_selected_determinantdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_second_selected_determinantdeterminanthsf_prefix_bp. ff_h_mce_mdr_second_selected_determinantdeterminanthsf_prefix_bp + S (ff_bp_mce_alternating_mdr_second_selected_determinantdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_second_selected_determinantdeterminanthsf_prefix)) * mdr_ec_second_selected_determinantdeterminanths)) /\ exists ff_q_mce_mdr_second_selected_determinantdeterminanthsf_prefix_bp. mdr_eb_second_selected_determinantdeterminanths = ff_q_mce_mdr_second_selected_determinantdeterminanthsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_second_selected_determinantdeterminanthsf_prefix)) * mdr_ec_second_selected_determinantdeterminanths) + (ff_bp_mce_alternating_mdr_second_selected_determinantdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_second_selected_determinantdeterminanthsf_prefix_bn. ff_h_mce_mdr_second_selected_determinantdeterminanthsf_prefix_bn + S (ff_bn_mce_alternating_mdr_second_selected_determinantdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_second_selected_determinantdeterminanthsf_prefix)) * mdr_fc_second_selected_determinantdeterminanths)) /\ exists ff_q_mce_mdr_second_selected_determinantdeterminanthsf_prefix_bn. mdr_fb_second_selected_determinantdeterminanths = ff_q_mce_mdr_second_selected_determinantdeterminanthsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_second_selected_determinantdeterminanthsf_prefix)) * mdr_fc_second_selected_determinantdeterminanths) + (ff_bn_mce_alternating_mdr_second_selected_determinantdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_second_selected_determinantdeterminanthsf_prefix_positive. ff_h_mce_mdr_second_selected_determinantdeterminanthsf_prefix_positive + S (ff_p_mce_alternating_mdr_second_selected_determinantdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_second_selected_determinantdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_second_selected_determinantdeterminanthsf)) /\ exists ff_q_mce_mdr_second_selected_determinantdeterminanthsf_prefix_positive. ff_ub_mce_fold_mdr_second_selected_determinantdeterminanthsf = ff_q_mce_mdr_second_selected_determinantdeterminanthsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_second_selected_determinantdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_second_selected_determinantdeterminanthsf) + (ff_p_mce_alternating_mdr_second_selected_determinantdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_second_selected_determinantdeterminanthsf_prefix_negative. ff_h_mce_mdr_second_selected_determinantdeterminanthsf_prefix_negative + S (ff_n_mce_alternating_mdr_second_selected_determinantdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_second_selected_determinantdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_second_selected_determinantdeterminanthsf)) /\ exists ff_q_mce_mdr_second_selected_determinantdeterminanthsf_prefix_negative. ff_vb_mce_fold_mdr_second_selected_determinantdeterminanthsf = ff_q_mce_mdr_second_selected_determinantdeterminanthsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_second_selected_determinantdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_second_selected_determinantdeterminanthsf) + (ff_n_mce_alternating_mdr_second_selected_determinantdeterminanthsf_prefix))) /\ (((exists ff_even_mce_term_mdr_second_selected_determinantdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_second_selected_determinantdeterminanthsf_prefix = 2 * ff_even_mce_term_mdr_second_selected_determinantdeterminanthsf_prefix_term) /\ (ff_p_mce_alternating_mdr_second_selected_determinantdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_second_selected_determinantdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_second_selected_determinantdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_second_selected_determinantdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_second_selected_determinantdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_second_selected_determinantdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_second_selected_determinantdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_second_selected_determinantdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_second_selected_determinantdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_second_selected_determinantdeterminanthsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_second_selected_determinantdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_second_selected_determinantdeterminanthsf_prefix = 2 * ff_odd_mce_term_mdr_second_selected_determinantdeterminanthsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_second_selected_determinantdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_second_selected_determinantdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_second_selected_determinantdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_second_selected_determinantdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_second_selected_determinantdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_second_selected_determinantdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_second_selected_determinantdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_second_selected_determinantdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_second_selected_determinantdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_second_selected_determinantdeterminanthsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_second_selected_determinantdeterminanthsf_positive ff_v_mce_mdr_second_selected_determinantdeterminanthsf_positive. ((((exists ff_h_mce_mdr_second_selected_determinantdeterminanthsf_positive_start. ff_h_mce_mdr_second_selected_determinantdeterminanthsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_second_selected_determinantdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_second_selected_determinantdeterminanthsf_positive_start. ff_u_mce_mdr_second_selected_determinantdeterminanthsf_positive = ff_q_mce_mdr_second_selected_determinantdeterminanthsf_positive_start * S ((S (0)) * ff_v_mce_mdr_second_selected_determinantdeterminanthsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_second_selected_determinantdeterminanthsf_positive_terminal. ff_h_mce_mdr_second_selected_determinantdeterminanthsf_positive_terminal + S (mdr_p_second_selected_determinantdeterminanth) = S ((S ((S (mdr_q_second_selected_determinantdeterminanths)))) * ff_v_mce_mdr_second_selected_determinantdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_second_selected_determinantdeterminanthsf_positive_terminal. ff_u_mce_mdr_second_selected_determinantdeterminanthsf_positive = ff_q_mce_mdr_second_selected_determinantdeterminanthsf_positive_terminal * S ((S ((S (mdr_q_second_selected_determinantdeterminanths)))) * ff_v_mce_mdr_second_selected_determinantdeterminanthsf_positive) + (mdr_p_second_selected_determinantdeterminanth))) /\ forall ff_i_mce_mdr_second_selected_determinantdeterminanthsf_positive. (exists ff_lt_mce_mdr_second_selected_determinantdeterminanthsf_positive_bound. ff_lt_mce_mdr_second_selected_determinantdeterminanthsf_positive_bound + S ff_i_mce_mdr_second_selected_determinantdeterminanthsf_positive = (S (mdr_q_second_selected_determinantdeterminanths))) -> exists ff_a_mce_mdr_second_selected_determinantdeterminanthsf_positive ff_r_mce_mdr_second_selected_determinantdeterminanthsf_positive ff_s_mce_mdr_second_selected_determinantdeterminanthsf_positive. ((((exists ff_h_mce_mdr_second_selected_determinantdeterminanthsf_positive_summand. ff_h_mce_mdr_second_selected_determinantdeterminanthsf_positive_summand + S (ff_a_mce_mdr_second_selected_determinantdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_second_selected_determinantdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_second_selected_determinantdeterminanthsf)) /\ exists ff_q_mce_mdr_second_selected_determinantdeterminanthsf_positive_summand. ff_ub_mce_fold_mdr_second_selected_determinantdeterminanthsf = ff_q_mce_mdr_second_selected_determinantdeterminanthsf_positive_summand * S ((S (ff_i_mce_mdr_second_selected_determinantdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_second_selected_determinantdeterminanthsf) + (ff_a_mce_mdr_second_selected_determinantdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_second_selected_determinantdeterminanthsf_positive_partial. ff_h_mce_mdr_second_selected_determinantdeterminanthsf_positive_partial + S (ff_r_mce_mdr_second_selected_determinantdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_second_selected_determinantdeterminanthsf_positive)) * ff_v_mce_mdr_second_selected_determinantdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_second_selected_determinantdeterminanthsf_positive_partial. ff_u_mce_mdr_second_selected_determinantdeterminanthsf_positive = ff_q_mce_mdr_second_selected_determinantdeterminanthsf_positive_partial * S ((S (ff_i_mce_mdr_second_selected_determinantdeterminanthsf_positive)) * ff_v_mce_mdr_second_selected_determinantdeterminanthsf_positive) + (ff_r_mce_mdr_second_selected_determinantdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_second_selected_determinantdeterminanthsf_positive_successor. ff_h_mce_mdr_second_selected_determinantdeterminanthsf_positive_successor + S (ff_s_mce_mdr_second_selected_determinantdeterminanthsf_positive) = S ((S (S ff_i_mce_mdr_second_selected_determinantdeterminanthsf_positive)) * ff_v_mce_mdr_second_selected_determinantdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_second_selected_determinantdeterminanthsf_positive_successor. ff_u_mce_mdr_second_selected_determinantdeterminanthsf_positive = ff_q_mce_mdr_second_selected_determinantdeterminanthsf_positive_successor * S ((S (S ff_i_mce_mdr_second_selected_determinantdeterminanthsf_positive)) * ff_v_mce_mdr_second_selected_determinantdeterminanthsf_positive) + (ff_s_mce_mdr_second_selected_determinantdeterminanthsf_positive))) /\ ff_s_mce_mdr_second_selected_determinantdeterminanthsf_positive = ff_r_mce_mdr_second_selected_determinantdeterminanthsf_positive + ff_a_mce_mdr_second_selected_determinantdeterminanthsf_positive)))))) /\ (exists ff_u_mce_mdr_second_selected_determinantdeterminanthsf_negative ff_v_mce_mdr_second_selected_determinantdeterminanthsf_negative. ((((exists ff_h_mce_mdr_second_selected_determinantdeterminanthsf_negative_start. ff_h_mce_mdr_second_selected_determinantdeterminanthsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_second_selected_determinantdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_second_selected_determinantdeterminanthsf_negative_start. ff_u_mce_mdr_second_selected_determinantdeterminanthsf_negative = ff_q_mce_mdr_second_selected_determinantdeterminanthsf_negative_start * S ((S (0)) * ff_v_mce_mdr_second_selected_determinantdeterminanthsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_second_selected_determinantdeterminanthsf_negative_terminal. ff_h_mce_mdr_second_selected_determinantdeterminanthsf_negative_terminal + S (mdr_n_second_selected_determinantdeterminanth) = S ((S ((S (mdr_q_second_selected_determinantdeterminanths)))) * ff_v_mce_mdr_second_selected_determinantdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_second_selected_determinantdeterminanthsf_negative_terminal. ff_u_mce_mdr_second_selected_determinantdeterminanthsf_negative = ff_q_mce_mdr_second_selected_determinantdeterminanthsf_negative_terminal * S ((S ((S (mdr_q_second_selected_determinantdeterminanths)))) * ff_v_mce_mdr_second_selected_determinantdeterminanthsf_negative) + (mdr_n_second_selected_determinantdeterminanth))) /\ forall ff_i_mce_mdr_second_selected_determinantdeterminanthsf_negative. (exists ff_lt_mce_mdr_second_selected_determinantdeterminanthsf_negative_bound. ff_lt_mce_mdr_second_selected_determinantdeterminanthsf_negative_bound + S ff_i_mce_mdr_second_selected_determinantdeterminanthsf_negative = (S (mdr_q_second_selected_determinantdeterminanths))) -> exists ff_a_mce_mdr_second_selected_determinantdeterminanthsf_negative ff_r_mce_mdr_second_selected_determinantdeterminanthsf_negative ff_s_mce_mdr_second_selected_determinantdeterminanthsf_negative. ((((exists ff_h_mce_mdr_second_selected_determinantdeterminanthsf_negative_summand. ff_h_mce_mdr_second_selected_determinantdeterminanthsf_negative_summand + S (ff_a_mce_mdr_second_selected_determinantdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_second_selected_determinantdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_second_selected_determinantdeterminanthsf)) /\ exists ff_q_mce_mdr_second_selected_determinantdeterminanthsf_negative_summand. ff_vb_mce_fold_mdr_second_selected_determinantdeterminanthsf = ff_q_mce_mdr_second_selected_determinantdeterminanthsf_negative_summand * S ((S (ff_i_mce_mdr_second_selected_determinantdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_second_selected_determinantdeterminanthsf) + (ff_a_mce_mdr_second_selected_determinantdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_second_selected_determinantdeterminanthsf_negative_partial. ff_h_mce_mdr_second_selected_determinantdeterminanthsf_negative_partial + S (ff_r_mce_mdr_second_selected_determinantdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_second_selected_determinantdeterminanthsf_negative)) * ff_v_mce_mdr_second_selected_determinantdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_second_selected_determinantdeterminanthsf_negative_partial. ff_u_mce_mdr_second_selected_determinantdeterminanthsf_negative = ff_q_mce_mdr_second_selected_determinantdeterminanthsf_negative_partial * S ((S (ff_i_mce_mdr_second_selected_determinantdeterminanthsf_negative)) * ff_v_mce_mdr_second_selected_determinantdeterminanthsf_negative) + (ff_r_mce_mdr_second_selected_determinantdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_second_selected_determinantdeterminanthsf_negative_successor. ff_h_mce_mdr_second_selected_determinantdeterminanthsf_negative_successor + S (ff_s_mce_mdr_second_selected_determinantdeterminanthsf_negative) = S ((S (S ff_i_mce_mdr_second_selected_determinantdeterminanthsf_negative)) * ff_v_mce_mdr_second_selected_determinantdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_second_selected_determinantdeterminanthsf_negative_successor. ff_u_mce_mdr_second_selected_determinantdeterminanthsf_negative = ff_q_mce_mdr_second_selected_determinantdeterminanthsf_negative_successor * S ((S (S ff_i_mce_mdr_second_selected_determinantdeterminanthsf_negative)) * ff_v_mce_mdr_second_selected_determinantdeterminanthsf_negative) + (ff_s_mce_mdr_second_selected_determinantdeterminanthsf_negative))) /\ ff_s_mce_mdr_second_selected_determinantdeterminanthsf_negative = ff_r_mce_mdr_second_selected_determinantdeterminanthsf_negative + ff_a_mce_mdr_second_selected_determinantdeterminanthsf_negative))))))))))))))) /\ ((exists mdr_gap_second_selected_determinantdeterminanti. mdr_gap_second_selected_determinantdeterminanti + S (mdr_i_second_selected_determinantdeterminant) = (mdr_l_second_selected_determinantdeterminant)) /\ (exists mdr_z_second_selected_determinantdeterminantr. ((exists mdr_a_second_selected_determinantdeterminantrc mdr_b_second_selected_determinantdeterminantrc mdr_c_second_selected_determinantdeterminantrc mdr_e_second_selected_determinantdeterminantrc mdr_f_second_selected_determinantdeterminantrc. ((mdr_a_second_selected_determinantdeterminantrc = ((q) + (mdr_ub_second_selected_determinant)) * S ((q) + (mdr_ub_second_selected_determinant)) + ((mdr_ub_second_selected_determinant) + (mdr_ub_second_selected_determinant))) /\ ((mdr_b_second_selected_determinantdeterminantrc = ((mdr_uc_second_selected_determinant) + (mdr_vb_second_selected_determinant)) * S ((mdr_uc_second_selected_determinant) + (mdr_vb_second_selected_determinant)) + ((mdr_vb_second_selected_determinant) + (mdr_vb_second_selected_determinant))) /\ ((mdr_c_second_selected_determinantdeterminantrc = ((mdr_a_second_selected_determinantdeterminantrc) + (mdr_b_second_selected_determinantdeterminantrc)) * S ((mdr_a_second_selected_determinantdeterminantrc) + (mdr_b_second_selected_determinantdeterminantrc)) + ((mdr_b_second_selected_determinantdeterminantrc) + (mdr_b_second_selected_determinantdeterminantrc))) /\ ((mdr_e_second_selected_determinantdeterminantrc = ((P) + (N)) * S ((P) + (N)) + ((N) + (N))) /\ ((mdr_f_second_selected_determinantdeterminantrc = ((mdr_vc_second_selected_determinant) + (mdr_e_second_selected_determinantdeterminantrc)) * S ((mdr_vc_second_selected_determinant) + (mdr_e_second_selected_determinantdeterminantrc)) + ((mdr_e_second_selected_determinantdeterminantrc) + (mdr_e_second_selected_determinantdeterminantrc))) /\ ((mdr_z_second_selected_determinantdeterminantr) = ((mdr_c_second_selected_determinantdeterminantrc) + (mdr_f_second_selected_determinantdeterminantrc)) * S ((mdr_c_second_selected_determinantdeterminantrc) + (mdr_f_second_selected_determinantdeterminantrc)) + ((mdr_f_second_selected_determinantdeterminantrc) + (mdr_f_second_selected_determinantdeterminantrc))))))))) /\ (((exists ff_h_mdr_second_selected_determinantdeterminantrb. ff_h_mdr_second_selected_determinantdeterminantrb + S (mdr_z_second_selected_determinantdeterminantr) = S ((S (mdr_i_second_selected_determinantdeterminant)) * mdr_c_second_selected_determinantdeterminant)) /\ exists ff_q_mdr_second_selected_determinantdeterminantrb. mdr_b_second_selected_determinantdeterminant = ff_q_mdr_second_selected_determinantdeterminantrb * S ((S (mdr_i_second_selected_determinantdeterminant)) * mdr_c_second_selected_determinantdeterminant) + (mdr_z_second_selected_determinantdeterminantr)))))))))) -> p + N = P + n