signed_recursive_determinant_from_evaluated_cofactors

Exact expanded first-order arithmetic statement

forall pb pc nb nc q eb ec fb fc p n. (forall mdr_j_given_cofactors. (exists mdr_gap_given_cofactorsj. mdr_gap_given_cofactorsj + S (mdr_j_given_cofactors) = (S (q))) -> exists mdr_up_given_cofactors mdr_us_given_cofactors mdr_un_given_cofactors mdr_ut_given_cofactors mdr_p_given_cofactors mdr_n_given_cofactors. ((((forall ff_index_mdm_prefix_mdr_given_cofactorsm_positive. (exists ff_gap_mdm_lt_mdr_given_cofactorsm_positive_index_bound. ff_gap_mdm_lt_mdr_given_cofactorsm_positive_index_bound + S (ff_index_mdm_prefix_mdr_given_cofactorsm_positive) = ((q) * (q))) -> exists ff_row_mdm_prefix_mdr_given_cofactorsm_positive ff_column_mdm_prefix_mdr_given_cofactorsm_positive ff_value_mdm_prefix_mdr_given_cofactorsm_positive. (ff_index_mdm_prefix_mdr_given_cofactorsm_positive = (q) * ff_row_mdm_prefix_mdr_given_cofactorsm_positive + ff_column_mdm_prefix_mdr_given_cofactorsm_positive /\ ((exists ff_gap_mdm_lt_mdr_given_cofactorsm_positive_column_bound. ff_gap_mdm_lt_mdr_given_cofactorsm_positive_column_bound + S (ff_column_mdm_prefix_mdr_given_cofactorsm_positive) = (q)) /\ ((exists ff_row_mdm_cell_mdr_given_cofactorsm_positive_cell ff_column_mdm_cell_mdr_given_cofactorsm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_given_cofactorsm_positive_cell_row_before. ff_gap_mdm_lt_mdr_given_cofactorsm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_given_cofactorsm_positive) = (0)) /\ ff_row_mdm_cell_mdr_given_cofactorsm_positive_cell = ff_row_mdm_prefix_mdr_given_cofactorsm_positive) \/ ((exists ff_gap_mdm_le_mdr_given_cofactorsm_positive_cell_row_after. ff_gap_mdm_le_mdr_given_cofactorsm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_given_cofactorsm_positive)) /\ ff_row_mdm_cell_mdr_given_cofactorsm_positive_cell = S ff_row_mdm_prefix_mdr_given_cofactorsm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_given_cofactorsm_positive_cell_column_before. ff_gap_mdm_lt_mdr_given_cofactorsm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_given_cofactorsm_positive) = (mdr_j_given_cofactors)) /\ ff_column_mdm_cell_mdr_given_cofactorsm_positive_cell = ff_column_mdm_prefix_mdr_given_cofactorsm_positive) \/ ((exists ff_gap_mdm_le_mdr_given_cofactorsm_positive_cell_column_after. ff_gap_mdm_le_mdr_given_cofactorsm_positive_cell_column_after + (mdr_j_given_cofactors) = (ff_column_mdm_prefix_mdr_given_cofactorsm_positive)) /\ ff_column_mdm_cell_mdr_given_cofactorsm_positive_cell = S ff_column_mdm_prefix_mdr_given_cofactorsm_positive))) /\ (((exists ff_h_mdm_mdr_given_cofactorsm_positive_cell_source. ff_h_mdm_mdr_given_cofactorsm_positive_cell_source + S (ff_value_mdm_prefix_mdr_given_cofactorsm_positive) = S ((S ((ff_row_mdm_cell_mdr_given_cofactorsm_positive_cell) * (S (q)) + (ff_column_mdm_cell_mdr_given_cofactorsm_positive_cell))) * pc)) /\ exists ff_q_mdm_mdr_given_cofactorsm_positive_cell_source. pb = ff_q_mdm_mdr_given_cofactorsm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_given_cofactorsm_positive_cell) * (S (q)) + (ff_column_mdm_cell_mdr_given_cofactorsm_positive_cell))) * pc) + (ff_value_mdm_prefix_mdr_given_cofactorsm_positive)))))) /\ (((exists ff_h_mdm_mdr_given_cofactorsm_positive_target. ff_h_mdm_mdr_given_cofactorsm_positive_target + S (ff_value_mdm_prefix_mdr_given_cofactorsm_positive) = S ((S (ff_index_mdm_prefix_mdr_given_cofactorsm_positive)) * mdr_us_given_cofactors)) /\ exists ff_q_mdm_mdr_given_cofactorsm_positive_target. mdr_up_given_cofactors = ff_q_mdm_mdr_given_cofactorsm_positive_target * S ((S (ff_index_mdm_prefix_mdr_given_cofactorsm_positive)) * mdr_us_given_cofactors) + (ff_value_mdm_prefix_mdr_given_cofactorsm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_given_cofactorsm_negative. (exists ff_gap_mdm_lt_mdr_given_cofactorsm_negative_index_bound. ff_gap_mdm_lt_mdr_given_cofactorsm_negative_index_bound + S (ff_index_mdm_prefix_mdr_given_cofactorsm_negative) = ((q) * (q))) -> exists ff_row_mdm_prefix_mdr_given_cofactorsm_negative ff_column_mdm_prefix_mdr_given_cofactorsm_negative ff_value_mdm_prefix_mdr_given_cofactorsm_negative. (ff_index_mdm_prefix_mdr_given_cofactorsm_negative = (q) * ff_row_mdm_prefix_mdr_given_cofactorsm_negative + ff_column_mdm_prefix_mdr_given_cofactorsm_negative /\ ((exists ff_gap_mdm_lt_mdr_given_cofactorsm_negative_column_bound. ff_gap_mdm_lt_mdr_given_cofactorsm_negative_column_bound + S (ff_column_mdm_prefix_mdr_given_cofactorsm_negative) = (q)) /\ ((exists ff_row_mdm_cell_mdr_given_cofactorsm_negative_cell ff_column_mdm_cell_mdr_given_cofactorsm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_given_cofactorsm_negative_cell_row_before. ff_gap_mdm_lt_mdr_given_cofactorsm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_given_cofactorsm_negative) = (0)) /\ ff_row_mdm_cell_mdr_given_cofactorsm_negative_cell = ff_row_mdm_prefix_mdr_given_cofactorsm_negative) \/ ((exists ff_gap_mdm_le_mdr_given_cofactorsm_negative_cell_row_after. ff_gap_mdm_le_mdr_given_cofactorsm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_given_cofactorsm_negative)) /\ ff_row_mdm_cell_mdr_given_cofactorsm_negative_cell = S ff_row_mdm_prefix_mdr_given_cofactorsm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_given_cofactorsm_negative_cell_column_before. ff_gap_mdm_lt_mdr_given_cofactorsm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_given_cofactorsm_negative) = (mdr_j_given_cofactors)) /\ ff_column_mdm_cell_mdr_given_cofactorsm_negative_cell = ff_column_mdm_prefix_mdr_given_cofactorsm_negative) \/ ((exists ff_gap_mdm_le_mdr_given_cofactorsm_negative_cell_column_after. ff_gap_mdm_le_mdr_given_cofactorsm_negative_cell_column_after + (mdr_j_given_cofactors) = (ff_column_mdm_prefix_mdr_given_cofactorsm_negative)) /\ ff_column_mdm_cell_mdr_given_cofactorsm_negative_cell = S ff_column_mdm_prefix_mdr_given_cofactorsm_negative))) /\ (((exists ff_h_mdm_mdr_given_cofactorsm_negative_cell_source. ff_h_mdm_mdr_given_cofactorsm_negative_cell_source + S (ff_value_mdm_prefix_mdr_given_cofactorsm_negative) = S ((S ((ff_row_mdm_cell_mdr_given_cofactorsm_negative_cell) * (S (q)) + (ff_column_mdm_cell_mdr_given_cofactorsm_negative_cell))) * nc)) /\ exists ff_q_mdm_mdr_given_cofactorsm_negative_cell_source. nb = ff_q_mdm_mdr_given_cofactorsm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_given_cofactorsm_negative_cell) * (S (q)) + (ff_column_mdm_cell_mdr_given_cofactorsm_negative_cell))) * nc) + (ff_value_mdm_prefix_mdr_given_cofactorsm_negative)))))) /\ (((exists ff_h_mdm_mdr_given_cofactorsm_negative_target. ff_h_mdm_mdr_given_cofactorsm_negative_target + S (ff_value_mdm_prefix_mdr_given_cofactorsm_negative) = S ((S (ff_index_mdm_prefix_mdr_given_cofactorsm_negative)) * mdr_ut_given_cofactors)) /\ exists ff_q_mdm_mdr_given_cofactorsm_negative_target. mdr_un_given_cofactors = ff_q_mdm_mdr_given_cofactorsm_negative_target * S ((S (ff_index_mdm_prefix_mdr_given_cofactorsm_negative)) * mdr_ut_given_cofactors) + (ff_value_mdm_prefix_mdr_given_cofactorsm_negative))))))))) /\ ((exists mdr_b_given_cofactorsd mdr_c_given_cofactorsd mdr_l_given_cofactorsd mdr_i_given_cofactorsd. ((forall mdr_i_given_cofactorsdh. (exists mdr_gap_given_cofactorsdhi. mdr_gap_given_cofactorsdhi + S (mdr_i_given_cofactorsdh) = (mdr_l_given_cofactorsd)) -> exists mdr_d_given_cofactorsdh mdr_pb_given_cofactorsdh mdr_pc_given_cofactorsdh mdr_nb_given_cofactorsdh mdr_nc_given_cofactorsdh mdr_p_given_cofactorsdh mdr_n_given_cofactorsdh. ((exists mdr_z_given_cofactorsdhr. ((exists mdr_a_given_cofactorsdhrc mdr_b_given_cofactorsdhrc mdr_c_given_cofactorsdhrc mdr_e_given_cofactorsdhrc mdr_f_given_cofactorsdhrc. ((mdr_a_given_cofactorsdhrc = ((mdr_d_given_cofactorsdh) + (mdr_pb_given_cofactorsdh)) * S ((mdr_d_given_cofactorsdh) + (mdr_pb_given_cofactorsdh)) + ((mdr_pb_given_cofactorsdh) + (mdr_pb_given_cofactorsdh))) /\ ((mdr_b_given_cofactorsdhrc = ((mdr_pc_given_cofactorsdh) + (mdr_nb_given_cofactorsdh)) * S ((mdr_pc_given_cofactorsdh) + (mdr_nb_given_cofactorsdh)) + ((mdr_nb_given_cofactorsdh) + (mdr_nb_given_cofactorsdh))) /\ ((mdr_c_given_cofactorsdhrc = ((mdr_a_given_cofactorsdhrc) + (mdr_b_given_cofactorsdhrc)) * S ((mdr_a_given_cofactorsdhrc) + (mdr_b_given_cofactorsdhrc)) + ((mdr_b_given_cofactorsdhrc) + (mdr_b_given_cofactorsdhrc))) /\ ((mdr_e_given_cofactorsdhrc = ((mdr_p_given_cofactorsdh) + (mdr_n_given_cofactorsdh)) * S ((mdr_p_given_cofactorsdh) + (mdr_n_given_cofactorsdh)) + ((mdr_n_given_cofactorsdh) + (mdr_n_given_cofactorsdh))) /\ ((mdr_f_given_cofactorsdhrc = ((mdr_nc_given_cofactorsdh) + (mdr_e_given_cofactorsdhrc)) * S ((mdr_nc_given_cofactorsdh) + (mdr_e_given_cofactorsdhrc)) + ((mdr_e_given_cofactorsdhrc) + (mdr_e_given_cofactorsdhrc))) /\ ((mdr_z_given_cofactorsdhr) = ((mdr_c_given_cofactorsdhrc) + (mdr_f_given_cofactorsdhrc)) * S ((mdr_c_given_cofactorsdhrc) + (mdr_f_given_cofactorsdhrc)) + ((mdr_f_given_cofactorsdhrc) + (mdr_f_given_cofactorsdhrc))))))))) /\ (((exists ff_h_mdr_given_cofactorsdhrb. ff_h_mdr_given_cofactorsdhrb + S (mdr_z_given_cofactorsdhr) = S ((S (mdr_i_given_cofactorsdh)) * mdr_c_given_cofactorsd)) /\ exists ff_q_mdr_given_cofactorsdhrb. mdr_b_given_cofactorsd = ff_q_mdr_given_cofactorsdhrb * S ((S (mdr_i_given_cofactorsdh)) * mdr_c_given_cofactorsd) + (mdr_z_given_cofactorsdhr))))) /\ (((((mdr_d_given_cofactorsdh) = 0) /\ (((mdr_p_given_cofactorsdh) = 1) /\ ((mdr_n_given_cofactorsdh) = 0))) \/ exists mdr_q_given_cofactorsdhs mdr_eb_given_cofactorsdhs mdr_ec_given_cofactorsdhs mdr_fb_given_cofactorsdhs mdr_fc_given_cofactorsdhs. (((mdr_d_given_cofactorsdh) = S (mdr_q_given_cofactorsdhs)) /\ ((forall mdr_j_given_cofactorsdhsc. (exists mdr_gap_given_cofactorsdhscj. mdr_gap_given_cofactorsdhscj + S (mdr_j_given_cofactorsdhsc) = (S (mdr_q_given_cofactorsdhs))) -> exists mdr_i_given_cofactorsdhsc mdr_up_given_cofactorsdhsc mdr_us_given_cofactorsdhsc mdr_un_given_cofactorsdhsc mdr_ut_given_cofactorsdhsc mdr_p_given_cofactorsdhsc mdr_n_given_cofactorsdhsc. ((exists mdr_gap_given_cofactorsdhsci. mdr_gap_given_cofactorsdhsci + S (mdr_i_given_cofactorsdhsc) = (mdr_i_given_cofactorsdh)) /\ ((exists mdr_z_given_cofactorsdhscr. ((exists mdr_a_given_cofactorsdhscrc mdr_b_given_cofactorsdhscrc mdr_c_given_cofactorsdhscrc mdr_e_given_cofactorsdhscrc mdr_f_given_cofactorsdhscrc. ((mdr_a_given_cofactorsdhscrc = ((mdr_q_given_cofactorsdhs) + (mdr_up_given_cofactorsdhsc)) * S ((mdr_q_given_cofactorsdhs) + (mdr_up_given_cofactorsdhsc)) + ((mdr_up_given_cofactorsdhsc) + (mdr_up_given_cofactorsdhsc))) /\ ((mdr_b_given_cofactorsdhscrc = ((mdr_us_given_cofactorsdhsc) + (mdr_un_given_cofactorsdhsc)) * S ((mdr_us_given_cofactorsdhsc) + (mdr_un_given_cofactorsdhsc)) + ((mdr_un_given_cofactorsdhsc) + (mdr_un_given_cofactorsdhsc))) /\ ((mdr_c_given_cofactorsdhscrc = ((mdr_a_given_cofactorsdhscrc) + (mdr_b_given_cofactorsdhscrc)) * S ((mdr_a_given_cofactorsdhscrc) + (mdr_b_given_cofactorsdhscrc)) + ((mdr_b_given_cofactorsdhscrc) + (mdr_b_given_cofactorsdhscrc))) /\ ((mdr_e_given_cofactorsdhscrc = ((mdr_p_given_cofactorsdhsc) + (mdr_n_given_cofactorsdhsc)) * S ((mdr_p_given_cofactorsdhsc) + (mdr_n_given_cofactorsdhsc)) + ((mdr_n_given_cofactorsdhsc) + (mdr_n_given_cofactorsdhsc))) /\ ((mdr_f_given_cofactorsdhscrc = ((mdr_ut_given_cofactorsdhsc) + (mdr_e_given_cofactorsdhscrc)) * S ((mdr_ut_given_cofactorsdhsc) + (mdr_e_given_cofactorsdhscrc)) + ((mdr_e_given_cofactorsdhscrc) + (mdr_e_given_cofactorsdhscrc))) /\ ((mdr_z_given_cofactorsdhscr) = ((mdr_c_given_cofactorsdhscrc) + (mdr_f_given_cofactorsdhscrc)) * S ((mdr_c_given_cofactorsdhscrc) + (mdr_f_given_cofactorsdhscrc)) + ((mdr_f_given_cofactorsdhscrc) + (mdr_f_given_cofactorsdhscrc))))))))) /\ (((exists ff_h_mdr_given_cofactorsdhscrb. ff_h_mdr_given_cofactorsdhscrb + S (mdr_z_given_cofactorsdhscr) = S ((S (mdr_i_given_cofactorsdhsc)) * mdr_c_given_cofactorsd)) /\ exists ff_q_mdr_given_cofactorsdhscrb. mdr_b_given_cofactorsd = ff_q_mdr_given_cofactorsdhscrb * S ((S (mdr_i_given_cofactorsdhsc)) * mdr_c_given_cofactorsd) + (mdr_z_given_cofactorsdhscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_given_cofactorsdhscm_positive. (exists ff_gap_mdm_lt_mdr_given_cofactorsdhscm_positive_index_bound. ff_gap_mdm_lt_mdr_given_cofactorsdhscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_given_cofactorsdhscm_positive) = ((mdr_q_given_cofactorsdhs) * (mdr_q_given_cofactorsdhs))) -> exists ff_row_mdm_prefix_mdr_given_cofactorsdhscm_positive ff_column_mdm_prefix_mdr_given_cofactorsdhscm_positive ff_value_mdm_prefix_mdr_given_cofactorsdhscm_positive. (ff_index_mdm_prefix_mdr_given_cofactorsdhscm_positive = (mdr_q_given_cofactorsdhs) * ff_row_mdm_prefix_mdr_given_cofactorsdhscm_positive + ff_column_mdm_prefix_mdr_given_cofactorsdhscm_positive /\ ((exists ff_gap_mdm_lt_mdr_given_cofactorsdhscm_positive_column_bound. ff_gap_mdm_lt_mdr_given_cofactorsdhscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_given_cofactorsdhscm_positive) = (mdr_q_given_cofactorsdhs)) /\ ((exists ff_row_mdm_cell_mdr_given_cofactorsdhscm_positive_cell ff_column_mdm_cell_mdr_given_cofactorsdhscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_given_cofactorsdhscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_given_cofactorsdhscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_given_cofactorsdhscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_given_cofactorsdhscm_positive_cell = ff_row_mdm_prefix_mdr_given_cofactorsdhscm_positive) \/ ((exists ff_gap_mdm_le_mdr_given_cofactorsdhscm_positive_cell_row_after. ff_gap_mdm_le_mdr_given_cofactorsdhscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_given_cofactorsdhscm_positive)) /\ ff_row_mdm_cell_mdr_given_cofactorsdhscm_positive_cell = S ff_row_mdm_prefix_mdr_given_cofactorsdhscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_given_cofactorsdhscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_given_cofactorsdhscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_given_cofactorsdhscm_positive) = (mdr_j_given_cofactorsdhsc)) /\ ff_column_mdm_cell_mdr_given_cofactorsdhscm_positive_cell = ff_column_mdm_prefix_mdr_given_cofactorsdhscm_positive) \/ ((exists ff_gap_mdm_le_mdr_given_cofactorsdhscm_positive_cell_column_after. ff_gap_mdm_le_mdr_given_cofactorsdhscm_positive_cell_column_after + (mdr_j_given_cofactorsdhsc) = (ff_column_mdm_prefix_mdr_given_cofactorsdhscm_positive)) /\ ff_column_mdm_cell_mdr_given_cofactorsdhscm_positive_cell = S ff_column_mdm_prefix_mdr_given_cofactorsdhscm_positive))) /\ (((exists ff_h_mdm_mdr_given_cofactorsdhscm_positive_cell_source. ff_h_mdm_mdr_given_cofactorsdhscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_given_cofactorsdhscm_positive) = S ((S ((ff_row_mdm_cell_mdr_given_cofactorsdhscm_positive_cell) * (S (mdr_q_given_cofactorsdhs)) + (ff_column_mdm_cell_mdr_given_cofactorsdhscm_positive_cell))) * mdr_pc_given_cofactorsdh)) /\ exists ff_q_mdm_mdr_given_cofactorsdhscm_positive_cell_source. mdr_pb_given_cofactorsdh = ff_q_mdm_mdr_given_cofactorsdhscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_given_cofactorsdhscm_positive_cell) * (S (mdr_q_given_cofactorsdhs)) + (ff_column_mdm_cell_mdr_given_cofactorsdhscm_positive_cell))) * mdr_pc_given_cofactorsdh) + (ff_value_mdm_prefix_mdr_given_cofactorsdhscm_positive)))))) /\ (((exists ff_h_mdm_mdr_given_cofactorsdhscm_positive_target. ff_h_mdm_mdr_given_cofactorsdhscm_positive_target + S (ff_value_mdm_prefix_mdr_given_cofactorsdhscm_positive) = S ((S (ff_index_mdm_prefix_mdr_given_cofactorsdhscm_positive)) * mdr_us_given_cofactorsdhsc)) /\ exists ff_q_mdm_mdr_given_cofactorsdhscm_positive_target. mdr_up_given_cofactorsdhsc = ff_q_mdm_mdr_given_cofactorsdhscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_given_cofactorsdhscm_positive)) * mdr_us_given_cofactorsdhsc) + (ff_value_mdm_prefix_mdr_given_cofactorsdhscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_given_cofactorsdhscm_negative. (exists ff_gap_mdm_lt_mdr_given_cofactorsdhscm_negative_index_bound. ff_gap_mdm_lt_mdr_given_cofactorsdhscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_given_cofactorsdhscm_negative) = ((mdr_q_given_cofactorsdhs) * (mdr_q_given_cofactorsdhs))) -> exists ff_row_mdm_prefix_mdr_given_cofactorsdhscm_negative ff_column_mdm_prefix_mdr_given_cofactorsdhscm_negative ff_value_mdm_prefix_mdr_given_cofactorsdhscm_negative. (ff_index_mdm_prefix_mdr_given_cofactorsdhscm_negative = (mdr_q_given_cofactorsdhs) * ff_row_mdm_prefix_mdr_given_cofactorsdhscm_negative + ff_column_mdm_prefix_mdr_given_cofactorsdhscm_negative /\ ((exists ff_gap_mdm_lt_mdr_given_cofactorsdhscm_negative_column_bound. ff_gap_mdm_lt_mdr_given_cofactorsdhscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_given_cofactorsdhscm_negative) = (mdr_q_given_cofactorsdhs)) /\ ((exists ff_row_mdm_cell_mdr_given_cofactorsdhscm_negative_cell ff_column_mdm_cell_mdr_given_cofactorsdhscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_given_cofactorsdhscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_given_cofactorsdhscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_given_cofactorsdhscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_given_cofactorsdhscm_negative_cell = ff_row_mdm_prefix_mdr_given_cofactorsdhscm_negative) \/ ((exists ff_gap_mdm_le_mdr_given_cofactorsdhscm_negative_cell_row_after. ff_gap_mdm_le_mdr_given_cofactorsdhscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_given_cofactorsdhscm_negative)) /\ ff_row_mdm_cell_mdr_given_cofactorsdhscm_negative_cell = S ff_row_mdm_prefix_mdr_given_cofactorsdhscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_given_cofactorsdhscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_given_cofactorsdhscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_given_cofactorsdhscm_negative) = (mdr_j_given_cofactorsdhsc)) /\ ff_column_mdm_cell_mdr_given_cofactorsdhscm_negative_cell = ff_column_mdm_prefix_mdr_given_cofactorsdhscm_negative) \/ ((exists ff_gap_mdm_le_mdr_given_cofactorsdhscm_negative_cell_column_after. ff_gap_mdm_le_mdr_given_cofactorsdhscm_negative_cell_column_after + (mdr_j_given_cofactorsdhsc) = (ff_column_mdm_prefix_mdr_given_cofactorsdhscm_negative)) /\ ff_column_mdm_cell_mdr_given_cofactorsdhscm_negative_cell = S ff_column_mdm_prefix_mdr_given_cofactorsdhscm_negative))) /\ (((exists ff_h_mdm_mdr_given_cofactorsdhscm_negative_cell_source. ff_h_mdm_mdr_given_cofactorsdhscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_given_cofactorsdhscm_negative) = S ((S ((ff_row_mdm_cell_mdr_given_cofactorsdhscm_negative_cell) * (S (mdr_q_given_cofactorsdhs)) + (ff_column_mdm_cell_mdr_given_cofactorsdhscm_negative_cell))) * mdr_nc_given_cofactorsdh)) /\ exists ff_q_mdm_mdr_given_cofactorsdhscm_negative_cell_source. mdr_nb_given_cofactorsdh = ff_q_mdm_mdr_given_cofactorsdhscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_given_cofactorsdhscm_negative_cell) * (S (mdr_q_given_cofactorsdhs)) + (ff_column_mdm_cell_mdr_given_cofactorsdhscm_negative_cell))) * mdr_nc_given_cofactorsdh) + (ff_value_mdm_prefix_mdr_given_cofactorsdhscm_negative)))))) /\ (((exists ff_h_mdm_mdr_given_cofactorsdhscm_negative_target. ff_h_mdm_mdr_given_cofactorsdhscm_negative_target + S (ff_value_mdm_prefix_mdr_given_cofactorsdhscm_negative) = S ((S (ff_index_mdm_prefix_mdr_given_cofactorsdhscm_negative)) * mdr_ut_given_cofactorsdhsc)) /\ exists ff_q_mdm_mdr_given_cofactorsdhscm_negative_target. mdr_un_given_cofactorsdhsc = ff_q_mdm_mdr_given_cofactorsdhscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_given_cofactorsdhscm_negative)) * mdr_ut_given_cofactorsdhsc) + (ff_value_mdm_prefix_mdr_given_cofactorsdhscm_negative))))))))) /\ ((((exists ff_h_mdr_given_cofactorsdhscp. ff_h_mdr_given_cofactorsdhscp + S (mdr_p_given_cofactorsdhsc) = S ((S (mdr_j_given_cofactorsdhsc)) * mdr_ec_given_cofactorsdhs)) /\ exists ff_q_mdr_given_cofactorsdhscp. mdr_eb_given_cofactorsdhs = ff_q_mdr_given_cofactorsdhscp * S ((S (mdr_j_given_cofactorsdhsc)) * mdr_ec_given_cofactorsdhs) + (mdr_p_given_cofactorsdhsc))) /\ (((exists ff_h_mdr_given_cofactorsdhscn. ff_h_mdr_given_cofactorsdhscn + S (mdr_n_given_cofactorsdhsc) = S ((S (mdr_j_given_cofactorsdhsc)) * mdr_fc_given_cofactorsdhs)) /\ exists ff_q_mdr_given_cofactorsdhscn. mdr_fb_given_cofactorsdhs = ff_q_mdr_given_cofactorsdhscn * S ((S (mdr_j_given_cofactorsdhsc)) * mdr_fc_given_cofactorsdhs) + (mdr_n_given_cofactorsdhsc)))))))) /\ (exists ff_ub_mce_fold_mdr_given_cofactorsdhsf ff_uc_mce_fold_mdr_given_cofactorsdhsf ff_vb_mce_fold_mdr_given_cofactorsdhsf ff_vc_mce_fold_mdr_given_cofactorsdhsf. ((forall ff_index_mce_alternating_mdr_given_cofactorsdhsf_prefix. (exists ff_gap_mce_mdr_given_cofactorsdhsf_prefix_index. ff_gap_mce_mdr_given_cofactorsdhsf_prefix_index + S (ff_index_mce_alternating_mdr_given_cofactorsdhsf_prefix) = (S (mdr_q_given_cofactorsdhs))) -> exists ff_ap_mce_alternating_mdr_given_cofactorsdhsf_prefix ff_an_mce_alternating_mdr_given_cofactorsdhsf_prefix ff_bp_mce_alternating_mdr_given_cofactorsdhsf_prefix ff_bn_mce_alternating_mdr_given_cofactorsdhsf_prefix ff_p_mce_alternating_mdr_given_cofactorsdhsf_prefix ff_n_mce_alternating_mdr_given_cofactorsdhsf_prefix. ((((exists ff_h_mce_mdr_given_cofactorsdhsf_prefix_ap. ff_h_mce_mdr_given_cofactorsdhsf_prefix_ap + S (ff_ap_mce_alternating_mdr_given_cofactorsdhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_given_cofactorsdhsf_prefix)) * mdr_pc_given_cofactorsdh)) /\ exists ff_q_mce_mdr_given_cofactorsdhsf_prefix_ap. mdr_pb_given_cofactorsdh = ff_q_mce_mdr_given_cofactorsdhsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_given_cofactorsdhsf_prefix)) * mdr_pc_given_cofactorsdh) + (ff_ap_mce_alternating_mdr_given_cofactorsdhsf_prefix))) /\ ((((exists ff_h_mce_mdr_given_cofactorsdhsf_prefix_an. ff_h_mce_mdr_given_cofactorsdhsf_prefix_an + S (ff_an_mce_alternating_mdr_given_cofactorsdhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_given_cofactorsdhsf_prefix)) * mdr_nc_given_cofactorsdh)) /\ exists ff_q_mce_mdr_given_cofactorsdhsf_prefix_an. mdr_nb_given_cofactorsdh = ff_q_mce_mdr_given_cofactorsdhsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_given_cofactorsdhsf_prefix)) * mdr_nc_given_cofactorsdh) + (ff_an_mce_alternating_mdr_given_cofactorsdhsf_prefix))) /\ ((((exists ff_h_mce_mdr_given_cofactorsdhsf_prefix_bp. ff_h_mce_mdr_given_cofactorsdhsf_prefix_bp + S (ff_bp_mce_alternating_mdr_given_cofactorsdhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_given_cofactorsdhsf_prefix)) * mdr_ec_given_cofactorsdhs)) /\ exists ff_q_mce_mdr_given_cofactorsdhsf_prefix_bp. mdr_eb_given_cofactorsdhs = ff_q_mce_mdr_given_cofactorsdhsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_given_cofactorsdhsf_prefix)) * mdr_ec_given_cofactorsdhs) + (ff_bp_mce_alternating_mdr_given_cofactorsdhsf_prefix))) /\ ((((exists ff_h_mce_mdr_given_cofactorsdhsf_prefix_bn. ff_h_mce_mdr_given_cofactorsdhsf_prefix_bn + S (ff_bn_mce_alternating_mdr_given_cofactorsdhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_given_cofactorsdhsf_prefix)) * mdr_fc_given_cofactorsdhs)) /\ exists ff_q_mce_mdr_given_cofactorsdhsf_prefix_bn. mdr_fb_given_cofactorsdhs = ff_q_mce_mdr_given_cofactorsdhsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_given_cofactorsdhsf_prefix)) * mdr_fc_given_cofactorsdhs) + (ff_bn_mce_alternating_mdr_given_cofactorsdhsf_prefix))) /\ ((((exists ff_h_mce_mdr_given_cofactorsdhsf_prefix_positive. ff_h_mce_mdr_given_cofactorsdhsf_prefix_positive + S (ff_p_mce_alternating_mdr_given_cofactorsdhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_given_cofactorsdhsf_prefix)) * ff_uc_mce_fold_mdr_given_cofactorsdhsf)) /\ exists ff_q_mce_mdr_given_cofactorsdhsf_prefix_positive. ff_ub_mce_fold_mdr_given_cofactorsdhsf = ff_q_mce_mdr_given_cofactorsdhsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_given_cofactorsdhsf_prefix)) * ff_uc_mce_fold_mdr_given_cofactorsdhsf) + (ff_p_mce_alternating_mdr_given_cofactorsdhsf_prefix))) /\ ((((exists ff_h_mce_mdr_given_cofactorsdhsf_prefix_negative. ff_h_mce_mdr_given_cofactorsdhsf_prefix_negative + S (ff_n_mce_alternating_mdr_given_cofactorsdhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_given_cofactorsdhsf_prefix)) * ff_vc_mce_fold_mdr_given_cofactorsdhsf)) /\ exists ff_q_mce_mdr_given_cofactorsdhsf_prefix_negative. ff_vb_mce_fold_mdr_given_cofactorsdhsf = ff_q_mce_mdr_given_cofactorsdhsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_given_cofactorsdhsf_prefix)) * ff_vc_mce_fold_mdr_given_cofactorsdhsf) + (ff_n_mce_alternating_mdr_given_cofactorsdhsf_prefix))) /\ (((exists ff_even_mce_term_mdr_given_cofactorsdhsf_prefix_term. ff_index_mce_alternating_mdr_given_cofactorsdhsf_prefix = 2 * ff_even_mce_term_mdr_given_cofactorsdhsf_prefix_term) /\ (ff_p_mce_alternating_mdr_given_cofactorsdhsf_prefix = (ff_ap_mce_alternating_mdr_given_cofactorsdhsf_prefix) * (ff_bp_mce_alternating_mdr_given_cofactorsdhsf_prefix) + (ff_an_mce_alternating_mdr_given_cofactorsdhsf_prefix) * (ff_bn_mce_alternating_mdr_given_cofactorsdhsf_prefix) /\ ff_n_mce_alternating_mdr_given_cofactorsdhsf_prefix = (ff_ap_mce_alternating_mdr_given_cofactorsdhsf_prefix) * (ff_bn_mce_alternating_mdr_given_cofactorsdhsf_prefix) + (ff_an_mce_alternating_mdr_given_cofactorsdhsf_prefix) * (ff_bp_mce_alternating_mdr_given_cofactorsdhsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_given_cofactorsdhsf_prefix_term. ff_index_mce_alternating_mdr_given_cofactorsdhsf_prefix = 2 * ff_odd_mce_term_mdr_given_cofactorsdhsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_given_cofactorsdhsf_prefix = (ff_ap_mce_alternating_mdr_given_cofactorsdhsf_prefix) * (ff_bn_mce_alternating_mdr_given_cofactorsdhsf_prefix) + (ff_an_mce_alternating_mdr_given_cofactorsdhsf_prefix) * (ff_bp_mce_alternating_mdr_given_cofactorsdhsf_prefix) /\ ff_n_mce_alternating_mdr_given_cofactorsdhsf_prefix = (ff_ap_mce_alternating_mdr_given_cofactorsdhsf_prefix) * (ff_bp_mce_alternating_mdr_given_cofactorsdhsf_prefix) + (ff_an_mce_alternating_mdr_given_cofactorsdhsf_prefix) * (ff_bn_mce_alternating_mdr_given_cofactorsdhsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_given_cofactorsdhsf_positive ff_v_mce_mdr_given_cofactorsdhsf_positive. ((((exists ff_h_mce_mdr_given_cofactorsdhsf_positive_start. ff_h_mce_mdr_given_cofactorsdhsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_given_cofactorsdhsf_positive)) /\ exists ff_q_mce_mdr_given_cofactorsdhsf_positive_start. ff_u_mce_mdr_given_cofactorsdhsf_positive = ff_q_mce_mdr_given_cofactorsdhsf_positive_start * S ((S (0)) * ff_v_mce_mdr_given_cofactorsdhsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_given_cofactorsdhsf_positive_terminal. ff_h_mce_mdr_given_cofactorsdhsf_positive_terminal + S (mdr_p_given_cofactorsdh) = S ((S ((S (mdr_q_given_cofactorsdhs)))) * ff_v_mce_mdr_given_cofactorsdhsf_positive)) /\ exists ff_q_mce_mdr_given_cofactorsdhsf_positive_terminal. ff_u_mce_mdr_given_cofactorsdhsf_positive = ff_q_mce_mdr_given_cofactorsdhsf_positive_terminal * S ((S ((S (mdr_q_given_cofactorsdhs)))) * ff_v_mce_mdr_given_cofactorsdhsf_positive) + (mdr_p_given_cofactorsdh))) /\ forall ff_i_mce_mdr_given_cofactorsdhsf_positive. (exists ff_lt_mce_mdr_given_cofactorsdhsf_positive_bound. ff_lt_mce_mdr_given_cofactorsdhsf_positive_bound + S ff_i_mce_mdr_given_cofactorsdhsf_positive = (S (mdr_q_given_cofactorsdhs))) -> exists ff_a_mce_mdr_given_cofactorsdhsf_positive ff_r_mce_mdr_given_cofactorsdhsf_positive ff_s_mce_mdr_given_cofactorsdhsf_positive. ((((exists ff_h_mce_mdr_given_cofactorsdhsf_positive_summand. ff_h_mce_mdr_given_cofactorsdhsf_positive_summand + S (ff_a_mce_mdr_given_cofactorsdhsf_positive) = S ((S (ff_i_mce_mdr_given_cofactorsdhsf_positive)) * ff_uc_mce_fold_mdr_given_cofactorsdhsf)) /\ exists ff_q_mce_mdr_given_cofactorsdhsf_positive_summand. ff_ub_mce_fold_mdr_given_cofactorsdhsf = ff_q_mce_mdr_given_cofactorsdhsf_positive_summand * S ((S (ff_i_mce_mdr_given_cofactorsdhsf_positive)) * ff_uc_mce_fold_mdr_given_cofactorsdhsf) + (ff_a_mce_mdr_given_cofactorsdhsf_positive))) /\ ((((exists ff_h_mce_mdr_given_cofactorsdhsf_positive_partial. ff_h_mce_mdr_given_cofactorsdhsf_positive_partial + S (ff_r_mce_mdr_given_cofactorsdhsf_positive) = S ((S (ff_i_mce_mdr_given_cofactorsdhsf_positive)) * ff_v_mce_mdr_given_cofactorsdhsf_positive)) /\ exists ff_q_mce_mdr_given_cofactorsdhsf_positive_partial. ff_u_mce_mdr_given_cofactorsdhsf_positive = ff_q_mce_mdr_given_cofactorsdhsf_positive_partial * S ((S (ff_i_mce_mdr_given_cofactorsdhsf_positive)) * ff_v_mce_mdr_given_cofactorsdhsf_positive) + (ff_r_mce_mdr_given_cofactorsdhsf_positive))) /\ ((((exists ff_h_mce_mdr_given_cofactorsdhsf_positive_successor. ff_h_mce_mdr_given_cofactorsdhsf_positive_successor + S (ff_s_mce_mdr_given_cofactorsdhsf_positive) = S ((S (S ff_i_mce_mdr_given_cofactorsdhsf_positive)) * ff_v_mce_mdr_given_cofactorsdhsf_positive)) /\ exists ff_q_mce_mdr_given_cofactorsdhsf_positive_successor. ff_u_mce_mdr_given_cofactorsdhsf_positive = ff_q_mce_mdr_given_cofactorsdhsf_positive_successor * S ((S (S ff_i_mce_mdr_given_cofactorsdhsf_positive)) * ff_v_mce_mdr_given_cofactorsdhsf_positive) + (ff_s_mce_mdr_given_cofactorsdhsf_positive))) /\ ff_s_mce_mdr_given_cofactorsdhsf_positive = ff_r_mce_mdr_given_cofactorsdhsf_positive + ff_a_mce_mdr_given_cofactorsdhsf_positive)))))) /\ (exists ff_u_mce_mdr_given_cofactorsdhsf_negative ff_v_mce_mdr_given_cofactorsdhsf_negative. ((((exists ff_h_mce_mdr_given_cofactorsdhsf_negative_start. ff_h_mce_mdr_given_cofactorsdhsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_given_cofactorsdhsf_negative)) /\ exists ff_q_mce_mdr_given_cofactorsdhsf_negative_start. ff_u_mce_mdr_given_cofactorsdhsf_negative = ff_q_mce_mdr_given_cofactorsdhsf_negative_start * S ((S (0)) * ff_v_mce_mdr_given_cofactorsdhsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_given_cofactorsdhsf_negative_terminal. ff_h_mce_mdr_given_cofactorsdhsf_negative_terminal + S (mdr_n_given_cofactorsdh) = S ((S ((S (mdr_q_given_cofactorsdhs)))) * ff_v_mce_mdr_given_cofactorsdhsf_negative)) /\ exists ff_q_mce_mdr_given_cofactorsdhsf_negative_terminal. ff_u_mce_mdr_given_cofactorsdhsf_negative = ff_q_mce_mdr_given_cofactorsdhsf_negative_terminal * S ((S ((S (mdr_q_given_cofactorsdhs)))) * ff_v_mce_mdr_given_cofactorsdhsf_negative) + (mdr_n_given_cofactorsdh))) /\ forall ff_i_mce_mdr_given_cofactorsdhsf_negative. (exists ff_lt_mce_mdr_given_cofactorsdhsf_negative_bound. ff_lt_mce_mdr_given_cofactorsdhsf_negative_bound + S ff_i_mce_mdr_given_cofactorsdhsf_negative = (S (mdr_q_given_cofactorsdhs))) -> exists ff_a_mce_mdr_given_cofactorsdhsf_negative ff_r_mce_mdr_given_cofactorsdhsf_negative ff_s_mce_mdr_given_cofactorsdhsf_negative. ((((exists ff_h_mce_mdr_given_cofactorsdhsf_negative_summand. ff_h_mce_mdr_given_cofactorsdhsf_negative_summand + S (ff_a_mce_mdr_given_cofactorsdhsf_negative) = S ((S (ff_i_mce_mdr_given_cofactorsdhsf_negative)) * ff_vc_mce_fold_mdr_given_cofactorsdhsf)) /\ exists ff_q_mce_mdr_given_cofactorsdhsf_negative_summand. ff_vb_mce_fold_mdr_given_cofactorsdhsf = ff_q_mce_mdr_given_cofactorsdhsf_negative_summand * S ((S (ff_i_mce_mdr_given_cofactorsdhsf_negative)) * ff_vc_mce_fold_mdr_given_cofactorsdhsf) + (ff_a_mce_mdr_given_cofactorsdhsf_negative))) /\ ((((exists ff_h_mce_mdr_given_cofactorsdhsf_negative_partial. ff_h_mce_mdr_given_cofactorsdhsf_negative_partial + S (ff_r_mce_mdr_given_cofactorsdhsf_negative) = S ((S (ff_i_mce_mdr_given_cofactorsdhsf_negative)) * ff_v_mce_mdr_given_cofactorsdhsf_negative)) /\ exists ff_q_mce_mdr_given_cofactorsdhsf_negative_partial. ff_u_mce_mdr_given_cofactorsdhsf_negative = ff_q_mce_mdr_given_cofactorsdhsf_negative_partial * S ((S (ff_i_mce_mdr_given_cofactorsdhsf_negative)) * ff_v_mce_mdr_given_cofactorsdhsf_negative) + (ff_r_mce_mdr_given_cofactorsdhsf_negative))) /\ ((((exists ff_h_mce_mdr_given_cofactorsdhsf_negative_successor. ff_h_mce_mdr_given_cofactorsdhsf_negative_successor + S (ff_s_mce_mdr_given_cofactorsdhsf_negative) = S ((S (S ff_i_mce_mdr_given_cofactorsdhsf_negative)) * ff_v_mce_mdr_given_cofactorsdhsf_negative)) /\ exists ff_q_mce_mdr_given_cofactorsdhsf_negative_successor. ff_u_mce_mdr_given_cofactorsdhsf_negative = ff_q_mce_mdr_given_cofactorsdhsf_negative_successor * S ((S (S ff_i_mce_mdr_given_cofactorsdhsf_negative)) * ff_v_mce_mdr_given_cofactorsdhsf_negative) + (ff_s_mce_mdr_given_cofactorsdhsf_negative))) /\ ff_s_mce_mdr_given_cofactorsdhsf_negative = ff_r_mce_mdr_given_cofactorsdhsf_negative + ff_a_mce_mdr_given_cofactorsdhsf_negative))))))))))))))) /\ ((exists mdr_gap_given_cofactorsdi. mdr_gap_given_cofactorsdi + S (mdr_i_given_cofactorsd) = (mdr_l_given_cofactorsd)) /\ (exists mdr_z_given_cofactorsdr. ((exists mdr_a_given_cofactorsdrc mdr_b_given_cofactorsdrc mdr_c_given_cofactorsdrc mdr_e_given_cofactorsdrc mdr_f_given_cofactorsdrc. ((mdr_a_given_cofactorsdrc = ((q) + (mdr_up_given_cofactors)) * S ((q) + (mdr_up_given_cofactors)) + ((mdr_up_given_cofactors) + (mdr_up_given_cofactors))) /\ ((mdr_b_given_cofactorsdrc = ((mdr_us_given_cofactors) + (mdr_un_given_cofactors)) * S ((mdr_us_given_cofactors) + (mdr_un_given_cofactors)) + ((mdr_un_given_cofactors) + (mdr_un_given_cofactors))) /\ ((mdr_c_given_cofactorsdrc = ((mdr_a_given_cofactorsdrc) + (mdr_b_given_cofactorsdrc)) * S ((mdr_a_given_cofactorsdrc) + (mdr_b_given_cofactorsdrc)) + ((mdr_b_given_cofactorsdrc) + (mdr_b_given_cofactorsdrc))) /\ ((mdr_e_given_cofactorsdrc = ((mdr_p_given_cofactors) + (mdr_n_given_cofactors)) * S ((mdr_p_given_cofactors) + (mdr_n_given_cofactors)) + ((mdr_n_given_cofactors) + (mdr_n_given_cofactors))) /\ ((mdr_f_given_cofactorsdrc = ((mdr_ut_given_cofactors) + (mdr_e_given_cofactorsdrc)) * S ((mdr_ut_given_cofactors) + (mdr_e_given_cofactorsdrc)) + ((mdr_e_given_cofactorsdrc) + (mdr_e_given_cofactorsdrc))) /\ ((mdr_z_given_cofactorsdr) = ((mdr_c_given_cofactorsdrc) + (mdr_f_given_cofactorsdrc)) * S ((mdr_c_given_cofactorsdrc) + (mdr_f_given_cofactorsdrc)) + ((mdr_f_given_cofactorsdrc) + (mdr_f_given_cofactorsdrc))))))))) /\ (((exists ff_h_mdr_given_cofactorsdrb. ff_h_mdr_given_cofactorsdrb + S (mdr_z_given_cofactorsdr) = S ((S (mdr_i_given_cofactorsd)) * mdr_c_given_cofactorsd)) /\ exists ff_q_mdr_given_cofactorsdrb. mdr_b_given_cofactorsd = ff_q_mdr_given_cofactorsdrb * S ((S (mdr_i_given_cofactorsd)) * mdr_c_given_cofactorsd) + (mdr_z_given_cofactorsdr)))))))) /\ ((((exists ff_h_mdr_given_cofactorsp. ff_h_mdr_given_cofactorsp + S (mdr_p_given_cofactors) = S ((S (mdr_j_given_cofactors)) * ec)) /\ exists ff_q_mdr_given_cofactorsp. eb = ff_q_mdr_given_cofactorsp * S ((S (mdr_j_given_cofactors)) * ec) + (mdr_p_given_cofactors))) /\ (((exists ff_h_mdr_given_cofactorsn. ff_h_mdr_given_cofactorsn + S (mdr_n_given_cofactors) = S ((S (mdr_j_given_cofactors)) * fc)) /\ exists ff_q_mdr_given_cofactorsn. fb = ff_q_mdr_given_cofactorsn * S ((S (mdr_j_given_cofactors)) * fc) + (mdr_n_given_cofactors))))))) -> (exists ff_ub_mce_fold_mdre_given_fold ff_uc_mce_fold_mdre_given_fold ff_vb_mce_fold_mdre_given_fold ff_vc_mce_fold_mdre_given_fold. ((forall ff_index_mce_alternating_mdre_given_fold_prefix. (exists ff_gap_mce_mdre_given_fold_prefix_index. ff_gap_mce_mdre_given_fold_prefix_index + S (ff_index_mce_alternating_mdre_given_fold_prefix) = (S q)) -> exists ff_ap_mce_alternating_mdre_given_fold_prefix ff_an_mce_alternating_mdre_given_fold_prefix ff_bp_mce_alternating_mdre_given_fold_prefix ff_bn_mce_alternating_mdre_given_fold_prefix ff_p_mce_alternating_mdre_given_fold_prefix ff_n_mce_alternating_mdre_given_fold_prefix. ((((exists ff_h_mce_mdre_given_fold_prefix_ap. ff_h_mce_mdre_given_fold_prefix_ap + S (ff_ap_mce_alternating_mdre_given_fold_prefix) = S ((S (ff_index_mce_alternating_mdre_given_fold_prefix)) * pc)) /\ exists ff_q_mce_mdre_given_fold_prefix_ap. pb = ff_q_mce_mdre_given_fold_prefix_ap * S ((S (ff_index_mce_alternating_mdre_given_fold_prefix)) * pc) + (ff_ap_mce_alternating_mdre_given_fold_prefix))) /\ ((((exists ff_h_mce_mdre_given_fold_prefix_an. ff_h_mce_mdre_given_fold_prefix_an + S (ff_an_mce_alternating_mdre_given_fold_prefix) = S ((S (ff_index_mce_alternating_mdre_given_fold_prefix)) * nc)) /\ exists ff_q_mce_mdre_given_fold_prefix_an. nb = ff_q_mce_mdre_given_fold_prefix_an * S ((S (ff_index_mce_alternating_mdre_given_fold_prefix)) * nc) + (ff_an_mce_alternating_mdre_given_fold_prefix))) /\ ((((exists ff_h_mce_mdre_given_fold_prefix_bp. ff_h_mce_mdre_given_fold_prefix_bp + S (ff_bp_mce_alternating_mdre_given_fold_prefix) = S ((S (ff_index_mce_alternating_mdre_given_fold_prefix)) * ec)) /\ exists ff_q_mce_mdre_given_fold_prefix_bp. eb = ff_q_mce_mdre_given_fold_prefix_bp * S ((S (ff_index_mce_alternating_mdre_given_fold_prefix)) * ec) + (ff_bp_mce_alternating_mdre_given_fold_prefix))) /\ ((((exists ff_h_mce_mdre_given_fold_prefix_bn. ff_h_mce_mdre_given_fold_prefix_bn + S (ff_bn_mce_alternating_mdre_given_fold_prefix) = S ((S (ff_index_mce_alternating_mdre_given_fold_prefix)) * fc)) /\ exists ff_q_mce_mdre_given_fold_prefix_bn. fb = ff_q_mce_mdre_given_fold_prefix_bn * S ((S (ff_index_mce_alternating_mdre_given_fold_prefix)) * fc) + (ff_bn_mce_alternating_mdre_given_fold_prefix))) /\ ((((exists ff_h_mce_mdre_given_fold_prefix_positive. ff_h_mce_mdre_given_fold_prefix_positive + S (ff_p_mce_alternating_mdre_given_fold_prefix) = S ((S (ff_index_mce_alternating_mdre_given_fold_prefix)) * ff_uc_mce_fold_mdre_given_fold)) /\ exists ff_q_mce_mdre_given_fold_prefix_positive. ff_ub_mce_fold_mdre_given_fold = ff_q_mce_mdre_given_fold_prefix_positive * S ((S (ff_index_mce_alternating_mdre_given_fold_prefix)) * ff_uc_mce_fold_mdre_given_fold) + (ff_p_mce_alternating_mdre_given_fold_prefix))) /\ ((((exists ff_h_mce_mdre_given_fold_prefix_negative. ff_h_mce_mdre_given_fold_prefix_negative + S (ff_n_mce_alternating_mdre_given_fold_prefix) = S ((S (ff_index_mce_alternating_mdre_given_fold_prefix)) * ff_vc_mce_fold_mdre_given_fold)) /\ exists ff_q_mce_mdre_given_fold_prefix_negative. ff_vb_mce_fold_mdre_given_fold = ff_q_mce_mdre_given_fold_prefix_negative * S ((S (ff_index_mce_alternating_mdre_given_fold_prefix)) * ff_vc_mce_fold_mdre_given_fold) + (ff_n_mce_alternating_mdre_given_fold_prefix))) /\ (((exists ff_even_mce_term_mdre_given_fold_prefix_term. ff_index_mce_alternating_mdre_given_fold_prefix = 2 * ff_even_mce_term_mdre_given_fold_prefix_term) /\ (ff_p_mce_alternating_mdre_given_fold_prefix = (ff_ap_mce_alternating_mdre_given_fold_prefix) * (ff_bp_mce_alternating_mdre_given_fold_prefix) + (ff_an_mce_alternating_mdre_given_fold_prefix) * (ff_bn_mce_alternating_mdre_given_fold_prefix) /\ ff_n_mce_alternating_mdre_given_fold_prefix = (ff_ap_mce_alternating_mdre_given_fold_prefix) * (ff_bn_mce_alternating_mdre_given_fold_prefix) + (ff_an_mce_alternating_mdre_given_fold_prefix) * (ff_bp_mce_alternating_mdre_given_fold_prefix))) \/ ((exists ff_odd_mce_term_mdre_given_fold_prefix_term. ff_index_mce_alternating_mdre_given_fold_prefix = 2 * ff_odd_mce_term_mdre_given_fold_prefix_term + 1) /\ (ff_p_mce_alternating_mdre_given_fold_prefix = (ff_ap_mce_alternating_mdre_given_fold_prefix) * (ff_bn_mce_alternating_mdre_given_fold_prefix) + (ff_an_mce_alternating_mdre_given_fold_prefix) * (ff_bp_mce_alternating_mdre_given_fold_prefix) /\ ff_n_mce_alternating_mdre_given_fold_prefix = (ff_ap_mce_alternating_mdre_given_fold_prefix) * (ff_bp_mce_alternating_mdre_given_fold_prefix) + (ff_an_mce_alternating_mdre_given_fold_prefix) * (ff_bn_mce_alternating_mdre_given_fold_prefix))))))))))) /\ ((exists ff_u_mce_mdre_given_fold_positive ff_v_mce_mdre_given_fold_positive. ((((exists ff_h_mce_mdre_given_fold_positive_start. ff_h_mce_mdre_given_fold_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdre_given_fold_positive)) /\ exists ff_q_mce_mdre_given_fold_positive_start. ff_u_mce_mdre_given_fold_positive = ff_q_mce_mdre_given_fold_positive_start * S ((S (0)) * ff_v_mce_mdre_given_fold_positive) + (0))) /\ ((((exists ff_h_mce_mdre_given_fold_positive_terminal. ff_h_mce_mdre_given_fold_positive_terminal + S (p) = S ((S ((S q))) * ff_v_mce_mdre_given_fold_positive)) /\ exists ff_q_mce_mdre_given_fold_positive_terminal. ff_u_mce_mdre_given_fold_positive = ff_q_mce_mdre_given_fold_positive_terminal * S ((S ((S q))) * ff_v_mce_mdre_given_fold_positive) + (p))) /\ forall ff_i_mce_mdre_given_fold_positive. (exists ff_lt_mce_mdre_given_fold_positive_bound. ff_lt_mce_mdre_given_fold_positive_bound + S ff_i_mce_mdre_given_fold_positive = (S q)) -> exists ff_a_mce_mdre_given_fold_positive ff_r_mce_mdre_given_fold_positive ff_s_mce_mdre_given_fold_positive. ((((exists ff_h_mce_mdre_given_fold_positive_summand. ff_h_mce_mdre_given_fold_positive_summand + S (ff_a_mce_mdre_given_fold_positive) = S ((S (ff_i_mce_mdre_given_fold_positive)) * ff_uc_mce_fold_mdre_given_fold)) /\ exists ff_q_mce_mdre_given_fold_positive_summand. ff_ub_mce_fold_mdre_given_fold = ff_q_mce_mdre_given_fold_positive_summand * S ((S (ff_i_mce_mdre_given_fold_positive)) * ff_uc_mce_fold_mdre_given_fold) + (ff_a_mce_mdre_given_fold_positive))) /\ ((((exists ff_h_mce_mdre_given_fold_positive_partial. ff_h_mce_mdre_given_fold_positive_partial + S (ff_r_mce_mdre_given_fold_positive) = S ((S (ff_i_mce_mdre_given_fold_positive)) * ff_v_mce_mdre_given_fold_positive)) /\ exists ff_q_mce_mdre_given_fold_positive_partial. ff_u_mce_mdre_given_fold_positive = ff_q_mce_mdre_given_fold_positive_partial * S ((S (ff_i_mce_mdre_given_fold_positive)) * ff_v_mce_mdre_given_fold_positive) + (ff_r_mce_mdre_given_fold_positive))) /\ ((((exists ff_h_mce_mdre_given_fold_positive_successor. ff_h_mce_mdre_given_fold_positive_successor + S (ff_s_mce_mdre_given_fold_positive) = S ((S (S ff_i_mce_mdre_given_fold_positive)) * ff_v_mce_mdre_given_fold_positive)) /\ exists ff_q_mce_mdre_given_fold_positive_successor. ff_u_mce_mdre_given_fold_positive = ff_q_mce_mdre_given_fold_positive_successor * S ((S (S ff_i_mce_mdre_given_fold_positive)) * ff_v_mce_mdre_given_fold_positive) + (ff_s_mce_mdre_given_fold_positive))) /\ ff_s_mce_mdre_given_fold_positive = ff_r_mce_mdre_given_fold_positive + ff_a_mce_mdre_given_fold_positive)))))) /\ (exists ff_u_mce_mdre_given_fold_negative ff_v_mce_mdre_given_fold_negative. ((((exists ff_h_mce_mdre_given_fold_negative_start. ff_h_mce_mdre_given_fold_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdre_given_fold_negative)) /\ exists ff_q_mce_mdre_given_fold_negative_start. ff_u_mce_mdre_given_fold_negative = ff_q_mce_mdre_given_fold_negative_start * S ((S (0)) * ff_v_mce_mdre_given_fold_negative) + (0))) /\ ((((exists ff_h_mce_mdre_given_fold_negative_terminal. ff_h_mce_mdre_given_fold_negative_terminal + S (n) = S ((S ((S q))) * ff_v_mce_mdre_given_fold_negative)) /\ exists ff_q_mce_mdre_given_fold_negative_terminal. ff_u_mce_mdre_given_fold_negative = ff_q_mce_mdre_given_fold_negative_terminal * S ((S ((S q))) * ff_v_mce_mdre_given_fold_negative) + (n))) /\ forall ff_i_mce_mdre_given_fold_negative. (exists ff_lt_mce_mdre_given_fold_negative_bound. ff_lt_mce_mdre_given_fold_negative_bound + S ff_i_mce_mdre_given_fold_negative = (S q)) -> exists ff_a_mce_mdre_given_fold_negative ff_r_mce_mdre_given_fold_negative ff_s_mce_mdre_given_fold_negative. ((((exists ff_h_mce_mdre_given_fold_negative_summand. ff_h_mce_mdre_given_fold_negative_summand + S (ff_a_mce_mdre_given_fold_negative) = S ((S (ff_i_mce_mdre_given_fold_negative)) * ff_vc_mce_fold_mdre_given_fold)) /\ exists ff_q_mce_mdre_given_fold_negative_summand. ff_vb_mce_fold_mdre_given_fold = ff_q_mce_mdre_given_fold_negative_summand * S ((S (ff_i_mce_mdre_given_fold_negative)) * ff_vc_mce_fold_mdre_given_fold) + (ff_a_mce_mdre_given_fold_negative))) /\ ((((exists ff_h_mce_mdre_given_fold_negative_partial. ff_h_mce_mdre_given_fold_negative_partial + S (ff_r_mce_mdre_given_fold_negative) = S ((S (ff_i_mce_mdre_given_fold_negative)) * ff_v_mce_mdre_given_fold_negative)) /\ exists ff_q_mce_mdre_given_fold_negative_partial. ff_u_mce_mdre_given_fold_negative = ff_q_mce_mdre_given_fold_negative_partial * S ((S (ff_i_mce_mdre_given_fold_negative)) * ff_v_mce_mdre_given_fold_negative) + (ff_r_mce_mdre_given_fold_negative))) /\ ((((exists ff_h_mce_mdre_given_fold_negative_successor. ff_h_mce_mdre_given_fold_negative_successor + S (ff_s_mce_mdre_given_fold_negative) = S ((S (S ff_i_mce_mdre_given_fold_negative)) * ff_v_mce_mdre_given_fold_negative)) /\ exists ff_q_mce_mdre_given_fold_negative_successor. ff_u_mce_mdre_given_fold_negative = ff_q_mce_mdre_given_fold_negative_successor * S ((S (S ff_i_mce_mdre_given_fold_negative)) * ff_v_mce_mdre_given_fold_negative) + (ff_s_mce_mdre_given_fold_negative))) /\ ff_s_mce_mdre_given_fold_negative = ff_r_mce_mdre_given_fold_negative + ff_a_mce_mdre_given_fold_negative))))))))) -> (exists mdr_b_cofactor_equation mdr_c_cofactor_equation mdr_l_cofactor_equation mdr_i_cofactor_equation. ((forall mdr_i_cofactor_equationh. (exists mdr_gap_cofactor_equationhi. mdr_gap_cofactor_equationhi + S (mdr_i_cofactor_equationh) = (mdr_l_cofactor_equation)) -> exists mdr_d_cofactor_equationh mdr_pb_cofactor_equationh mdr_pc_cofactor_equationh mdr_nb_cofactor_equationh mdr_nc_cofactor_equationh mdr_p_cofactor_equationh mdr_n_cofactor_equationh. ((exists mdr_z_cofactor_equationhr. ((exists mdr_a_cofactor_equationhrc mdr_b_cofactor_equationhrc mdr_c_cofactor_equationhrc mdr_e_cofactor_equationhrc mdr_f_cofactor_equationhrc. ((mdr_a_cofactor_equationhrc = ((mdr_d_cofactor_equationh) + (mdr_pb_cofactor_equationh)) * S ((mdr_d_cofactor_equationh) + (mdr_pb_cofactor_equationh)) + ((mdr_pb_cofactor_equationh) + (mdr_pb_cofactor_equationh))) /\ ((mdr_b_cofactor_equationhrc = ((mdr_pc_cofactor_equationh) + (mdr_nb_cofactor_equationh)) * S ((mdr_pc_cofactor_equationh) + (mdr_nb_cofactor_equationh)) + ((mdr_nb_cofactor_equationh) + (mdr_nb_cofactor_equationh))) /\ ((mdr_c_cofactor_equationhrc = ((mdr_a_cofactor_equationhrc) + (mdr_b_cofactor_equationhrc)) * S ((mdr_a_cofactor_equationhrc) + (mdr_b_cofactor_equationhrc)) + ((mdr_b_cofactor_equationhrc) + (mdr_b_cofactor_equationhrc))) /\ ((mdr_e_cofactor_equationhrc = ((mdr_p_cofactor_equationh) + (mdr_n_cofactor_equationh)) * S ((mdr_p_cofactor_equationh) + (mdr_n_cofactor_equationh)) + ((mdr_n_cofactor_equationh) + (mdr_n_cofactor_equationh))) /\ ((mdr_f_cofactor_equationhrc = ((mdr_nc_cofactor_equationh) + (mdr_e_cofactor_equationhrc)) * S ((mdr_nc_cofactor_equationh) + (mdr_e_cofactor_equationhrc)) + ((mdr_e_cofactor_equationhrc) + (mdr_e_cofactor_equationhrc))) /\ ((mdr_z_cofactor_equationhr) = ((mdr_c_cofactor_equationhrc) + (mdr_f_cofactor_equationhrc)) * S ((mdr_c_cofactor_equationhrc) + (mdr_f_cofactor_equationhrc)) + ((mdr_f_cofactor_equationhrc) + (mdr_f_cofactor_equationhrc))))))))) /\ (((exists ff_h_mdr_cofactor_equationhrb. ff_h_mdr_cofactor_equationhrb + S (mdr_z_cofactor_equationhr) = S ((S (mdr_i_cofactor_equationh)) * mdr_c_cofactor_equation)) /\ exists ff_q_mdr_cofactor_equationhrb. mdr_b_cofactor_equation = ff_q_mdr_cofactor_equationhrb * S ((S (mdr_i_cofactor_equationh)) * mdr_c_cofactor_equation) + (mdr_z_cofactor_equationhr))))) /\ (((((mdr_d_cofactor_equationh) = 0) /\ (((mdr_p_cofactor_equationh) = 1) /\ ((mdr_n_cofactor_equationh) = 0))) \/ exists mdr_q_cofactor_equationhs mdr_eb_cofactor_equationhs mdr_ec_cofactor_equationhs mdr_fb_cofactor_equationhs mdr_fc_cofactor_equationhs. (((mdr_d_cofactor_equationh) = S (mdr_q_cofactor_equationhs)) /\ ((forall mdr_j_cofactor_equationhsc. (exists mdr_gap_cofactor_equationhscj. mdr_gap_cofactor_equationhscj + S (mdr_j_cofactor_equationhsc) = (S (mdr_q_cofactor_equationhs))) -> exists mdr_i_cofactor_equationhsc mdr_up_cofactor_equationhsc mdr_us_cofactor_equationhsc mdr_un_cofactor_equationhsc mdr_ut_cofactor_equationhsc mdr_p_cofactor_equationhsc mdr_n_cofactor_equationhsc. ((exists mdr_gap_cofactor_equationhsci. mdr_gap_cofactor_equationhsci + S (mdr_i_cofactor_equationhsc) = (mdr_i_cofactor_equationh)) /\ ((exists mdr_z_cofactor_equationhscr. ((exists mdr_a_cofactor_equationhscrc mdr_b_cofactor_equationhscrc mdr_c_cofactor_equationhscrc mdr_e_cofactor_equationhscrc mdr_f_cofactor_equationhscrc. ((mdr_a_cofactor_equationhscrc = ((mdr_q_cofactor_equationhs) + (mdr_up_cofactor_equationhsc)) * S ((mdr_q_cofactor_equationhs) + (mdr_up_cofactor_equationhsc)) + ((mdr_up_cofactor_equationhsc) + (mdr_up_cofactor_equationhsc))) /\ ((mdr_b_cofactor_equationhscrc = ((mdr_us_cofactor_equationhsc) + (mdr_un_cofactor_equationhsc)) * S ((mdr_us_cofactor_equationhsc) + (mdr_un_cofactor_equationhsc)) + ((mdr_un_cofactor_equationhsc) + (mdr_un_cofactor_equationhsc))) /\ ((mdr_c_cofactor_equationhscrc = ((mdr_a_cofactor_equationhscrc) + (mdr_b_cofactor_equationhscrc)) * S ((mdr_a_cofactor_equationhscrc) + (mdr_b_cofactor_equationhscrc)) + ((mdr_b_cofactor_equationhscrc) + (mdr_b_cofactor_equationhscrc))) /\ ((mdr_e_cofactor_equationhscrc = ((mdr_p_cofactor_equationhsc) + (mdr_n_cofactor_equationhsc)) * S ((mdr_p_cofactor_equationhsc) + (mdr_n_cofactor_equationhsc)) + ((mdr_n_cofactor_equationhsc) + (mdr_n_cofactor_equationhsc))) /\ ((mdr_f_cofactor_equationhscrc = ((mdr_ut_cofactor_equationhsc) + (mdr_e_cofactor_equationhscrc)) * S ((mdr_ut_cofactor_equationhsc) + (mdr_e_cofactor_equationhscrc)) + ((mdr_e_cofactor_equationhscrc) + (mdr_e_cofactor_equationhscrc))) /\ ((mdr_z_cofactor_equationhscr) = ((mdr_c_cofactor_equationhscrc) + (mdr_f_cofactor_equationhscrc)) * S ((mdr_c_cofactor_equationhscrc) + (mdr_f_cofactor_equationhscrc)) + ((mdr_f_cofactor_equationhscrc) + (mdr_f_cofactor_equationhscrc))))))))) /\ (((exists ff_h_mdr_cofactor_equationhscrb. ff_h_mdr_cofactor_equationhscrb + S (mdr_z_cofactor_equationhscr) = S ((S (mdr_i_cofactor_equationhsc)) * mdr_c_cofactor_equation)) /\ exists ff_q_mdr_cofactor_equationhscrb. mdr_b_cofactor_equation = ff_q_mdr_cofactor_equationhscrb * S ((S (mdr_i_cofactor_equationhsc)) * mdr_c_cofactor_equation) + (mdr_z_cofactor_equationhscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_cofactor_equationhscm_positive. (exists ff_gap_mdm_lt_mdr_cofactor_equationhscm_positive_index_bound. ff_gap_mdm_lt_mdr_cofactor_equationhscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_cofactor_equationhscm_positive) = ((mdr_q_cofactor_equationhs) * (mdr_q_cofactor_equationhs))) -> exists ff_row_mdm_prefix_mdr_cofactor_equationhscm_positive ff_column_mdm_prefix_mdr_cofactor_equationhscm_positive ff_value_mdm_prefix_mdr_cofactor_equationhscm_positive. (ff_index_mdm_prefix_mdr_cofactor_equationhscm_positive = (mdr_q_cofactor_equationhs) * ff_row_mdm_prefix_mdr_cofactor_equationhscm_positive + ff_column_mdm_prefix_mdr_cofactor_equationhscm_positive /\ ((exists ff_gap_mdm_lt_mdr_cofactor_equationhscm_positive_column_bound. ff_gap_mdm_lt_mdr_cofactor_equationhscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_cofactor_equationhscm_positive) = (mdr_q_cofactor_equationhs)) /\ ((exists ff_row_mdm_cell_mdr_cofactor_equationhscm_positive_cell ff_column_mdm_cell_mdr_cofactor_equationhscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_cofactor_equationhscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_cofactor_equationhscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_cofactor_equationhscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_cofactor_equationhscm_positive_cell = ff_row_mdm_prefix_mdr_cofactor_equationhscm_positive) \/ ((exists ff_gap_mdm_le_mdr_cofactor_equationhscm_positive_cell_row_after. ff_gap_mdm_le_mdr_cofactor_equationhscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_cofactor_equationhscm_positive)) /\ ff_row_mdm_cell_mdr_cofactor_equationhscm_positive_cell = S ff_row_mdm_prefix_mdr_cofactor_equationhscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_cofactor_equationhscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_cofactor_equationhscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_cofactor_equationhscm_positive) = (mdr_j_cofactor_equationhsc)) /\ ff_column_mdm_cell_mdr_cofactor_equationhscm_positive_cell = ff_column_mdm_prefix_mdr_cofactor_equationhscm_positive) \/ ((exists ff_gap_mdm_le_mdr_cofactor_equationhscm_positive_cell_column_after. ff_gap_mdm_le_mdr_cofactor_equationhscm_positive_cell_column_after + (mdr_j_cofactor_equationhsc) = (ff_column_mdm_prefix_mdr_cofactor_equationhscm_positive)) /\ ff_column_mdm_cell_mdr_cofactor_equationhscm_positive_cell = S ff_column_mdm_prefix_mdr_cofactor_equationhscm_positive))) /\ (((exists ff_h_mdm_mdr_cofactor_equationhscm_positive_cell_source. ff_h_mdm_mdr_cofactor_equationhscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_cofactor_equationhscm_positive) = S ((S ((ff_row_mdm_cell_mdr_cofactor_equationhscm_positive_cell) * (S (mdr_q_cofactor_equationhs)) + (ff_column_mdm_cell_mdr_cofactor_equationhscm_positive_cell))) * mdr_pc_cofactor_equationh)) /\ exists ff_q_mdm_mdr_cofactor_equationhscm_positive_cell_source. mdr_pb_cofactor_equationh = ff_q_mdm_mdr_cofactor_equationhscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_cofactor_equationhscm_positive_cell) * (S (mdr_q_cofactor_equationhs)) + (ff_column_mdm_cell_mdr_cofactor_equationhscm_positive_cell))) * mdr_pc_cofactor_equationh) + (ff_value_mdm_prefix_mdr_cofactor_equationhscm_positive)))))) /\ (((exists ff_h_mdm_mdr_cofactor_equationhscm_positive_target. ff_h_mdm_mdr_cofactor_equationhscm_positive_target + S (ff_value_mdm_prefix_mdr_cofactor_equationhscm_positive) = S ((S (ff_index_mdm_prefix_mdr_cofactor_equationhscm_positive)) * mdr_us_cofactor_equationhsc)) /\ exists ff_q_mdm_mdr_cofactor_equationhscm_positive_target. mdr_up_cofactor_equationhsc = ff_q_mdm_mdr_cofactor_equationhscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_cofactor_equationhscm_positive)) * mdr_us_cofactor_equationhsc) + (ff_value_mdm_prefix_mdr_cofactor_equationhscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_cofactor_equationhscm_negative. (exists ff_gap_mdm_lt_mdr_cofactor_equationhscm_negative_index_bound. ff_gap_mdm_lt_mdr_cofactor_equationhscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_cofactor_equationhscm_negative) = ((mdr_q_cofactor_equationhs) * (mdr_q_cofactor_equationhs))) -> exists ff_row_mdm_prefix_mdr_cofactor_equationhscm_negative ff_column_mdm_prefix_mdr_cofactor_equationhscm_negative ff_value_mdm_prefix_mdr_cofactor_equationhscm_negative. (ff_index_mdm_prefix_mdr_cofactor_equationhscm_negative = (mdr_q_cofactor_equationhs) * ff_row_mdm_prefix_mdr_cofactor_equationhscm_negative + ff_column_mdm_prefix_mdr_cofactor_equationhscm_negative /\ ((exists ff_gap_mdm_lt_mdr_cofactor_equationhscm_negative_column_bound. ff_gap_mdm_lt_mdr_cofactor_equationhscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_cofactor_equationhscm_negative) = (mdr_q_cofactor_equationhs)) /\ ((exists ff_row_mdm_cell_mdr_cofactor_equationhscm_negative_cell ff_column_mdm_cell_mdr_cofactor_equationhscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_cofactor_equationhscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_cofactor_equationhscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_cofactor_equationhscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_cofactor_equationhscm_negative_cell = ff_row_mdm_prefix_mdr_cofactor_equationhscm_negative) \/ ((exists ff_gap_mdm_le_mdr_cofactor_equationhscm_negative_cell_row_after. ff_gap_mdm_le_mdr_cofactor_equationhscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_cofactor_equationhscm_negative)) /\ ff_row_mdm_cell_mdr_cofactor_equationhscm_negative_cell = S ff_row_mdm_prefix_mdr_cofactor_equationhscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_cofactor_equationhscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_cofactor_equationhscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_cofactor_equationhscm_negative) = (mdr_j_cofactor_equationhsc)) /\ ff_column_mdm_cell_mdr_cofactor_equationhscm_negative_cell = ff_column_mdm_prefix_mdr_cofactor_equationhscm_negative) \/ ((exists ff_gap_mdm_le_mdr_cofactor_equationhscm_negative_cell_column_after. ff_gap_mdm_le_mdr_cofactor_equationhscm_negative_cell_column_after + (mdr_j_cofactor_equationhsc) = (ff_column_mdm_prefix_mdr_cofactor_equationhscm_negative)) /\ ff_column_mdm_cell_mdr_cofactor_equationhscm_negative_cell = S ff_column_mdm_prefix_mdr_cofactor_equationhscm_negative))) /\ (((exists ff_h_mdm_mdr_cofactor_equationhscm_negative_cell_source. ff_h_mdm_mdr_cofactor_equationhscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_cofactor_equationhscm_negative) = S ((S ((ff_row_mdm_cell_mdr_cofactor_equationhscm_negative_cell) * (S (mdr_q_cofactor_equationhs)) + (ff_column_mdm_cell_mdr_cofactor_equationhscm_negative_cell))) * mdr_nc_cofactor_equationh)) /\ exists ff_q_mdm_mdr_cofactor_equationhscm_negative_cell_source. mdr_nb_cofactor_equationh = ff_q_mdm_mdr_cofactor_equationhscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_cofactor_equationhscm_negative_cell) * (S (mdr_q_cofactor_equationhs)) + (ff_column_mdm_cell_mdr_cofactor_equationhscm_negative_cell))) * mdr_nc_cofactor_equationh) + (ff_value_mdm_prefix_mdr_cofactor_equationhscm_negative)))))) /\ (((exists ff_h_mdm_mdr_cofactor_equationhscm_negative_target. ff_h_mdm_mdr_cofactor_equationhscm_negative_target + S (ff_value_mdm_prefix_mdr_cofactor_equationhscm_negative) = S ((S (ff_index_mdm_prefix_mdr_cofactor_equationhscm_negative)) * mdr_ut_cofactor_equationhsc)) /\ exists ff_q_mdm_mdr_cofactor_equationhscm_negative_target. mdr_un_cofactor_equationhsc = ff_q_mdm_mdr_cofactor_equationhscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_cofactor_equationhscm_negative)) * mdr_ut_cofactor_equationhsc) + (ff_value_mdm_prefix_mdr_cofactor_equationhscm_negative))))))))) /\ ((((exists ff_h_mdr_cofactor_equationhscp. ff_h_mdr_cofactor_equationhscp + S (mdr_p_cofactor_equationhsc) = S ((S (mdr_j_cofactor_equationhsc)) * mdr_ec_cofactor_equationhs)) /\ exists ff_q_mdr_cofactor_equationhscp. mdr_eb_cofactor_equationhs = ff_q_mdr_cofactor_equationhscp * S ((S (mdr_j_cofactor_equationhsc)) * mdr_ec_cofactor_equationhs) + (mdr_p_cofactor_equationhsc))) /\ (((exists ff_h_mdr_cofactor_equationhscn. ff_h_mdr_cofactor_equationhscn + S (mdr_n_cofactor_equationhsc) = S ((S (mdr_j_cofactor_equationhsc)) * mdr_fc_cofactor_equationhs)) /\ exists ff_q_mdr_cofactor_equationhscn. mdr_fb_cofactor_equationhs = ff_q_mdr_cofactor_equationhscn * S ((S (mdr_j_cofactor_equationhsc)) * mdr_fc_cofactor_equationhs) + (mdr_n_cofactor_equationhsc)))))))) /\ (exists ff_ub_mce_fold_mdr_cofactor_equationhsf ff_uc_mce_fold_mdr_cofactor_equationhsf ff_vb_mce_fold_mdr_cofactor_equationhsf ff_vc_mce_fold_mdr_cofactor_equationhsf. ((forall ff_index_mce_alternating_mdr_cofactor_equationhsf_prefix. (exists ff_gap_mce_mdr_cofactor_equationhsf_prefix_index. ff_gap_mce_mdr_cofactor_equationhsf_prefix_index + S (ff_index_mce_alternating_mdr_cofactor_equationhsf_prefix) = (S (mdr_q_cofactor_equationhs))) -> exists ff_ap_mce_alternating_mdr_cofactor_equationhsf_prefix ff_an_mce_alternating_mdr_cofactor_equationhsf_prefix ff_bp_mce_alternating_mdr_cofactor_equationhsf_prefix ff_bn_mce_alternating_mdr_cofactor_equationhsf_prefix ff_p_mce_alternating_mdr_cofactor_equationhsf_prefix ff_n_mce_alternating_mdr_cofactor_equationhsf_prefix. ((((exists ff_h_mce_mdr_cofactor_equationhsf_prefix_ap. ff_h_mce_mdr_cofactor_equationhsf_prefix_ap + S (ff_ap_mce_alternating_mdr_cofactor_equationhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_cofactor_equationhsf_prefix)) * mdr_pc_cofactor_equationh)) /\ exists ff_q_mce_mdr_cofactor_equationhsf_prefix_ap. mdr_pb_cofactor_equationh = ff_q_mce_mdr_cofactor_equationhsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_cofactor_equationhsf_prefix)) * mdr_pc_cofactor_equationh) + (ff_ap_mce_alternating_mdr_cofactor_equationhsf_prefix))) /\ ((((exists ff_h_mce_mdr_cofactor_equationhsf_prefix_an. ff_h_mce_mdr_cofactor_equationhsf_prefix_an + S (ff_an_mce_alternating_mdr_cofactor_equationhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_cofactor_equationhsf_prefix)) * mdr_nc_cofactor_equationh)) /\ exists ff_q_mce_mdr_cofactor_equationhsf_prefix_an. mdr_nb_cofactor_equationh = ff_q_mce_mdr_cofactor_equationhsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_cofactor_equationhsf_prefix)) * mdr_nc_cofactor_equationh) + (ff_an_mce_alternating_mdr_cofactor_equationhsf_prefix))) /\ ((((exists ff_h_mce_mdr_cofactor_equationhsf_prefix_bp. ff_h_mce_mdr_cofactor_equationhsf_prefix_bp + S (ff_bp_mce_alternating_mdr_cofactor_equationhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_cofactor_equationhsf_prefix)) * mdr_ec_cofactor_equationhs)) /\ exists ff_q_mce_mdr_cofactor_equationhsf_prefix_bp. mdr_eb_cofactor_equationhs = ff_q_mce_mdr_cofactor_equationhsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_cofactor_equationhsf_prefix)) * mdr_ec_cofactor_equationhs) + (ff_bp_mce_alternating_mdr_cofactor_equationhsf_prefix))) /\ ((((exists ff_h_mce_mdr_cofactor_equationhsf_prefix_bn. ff_h_mce_mdr_cofactor_equationhsf_prefix_bn + S (ff_bn_mce_alternating_mdr_cofactor_equationhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_cofactor_equationhsf_prefix)) * mdr_fc_cofactor_equationhs)) /\ exists ff_q_mce_mdr_cofactor_equationhsf_prefix_bn. mdr_fb_cofactor_equationhs = ff_q_mce_mdr_cofactor_equationhsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_cofactor_equationhsf_prefix)) * mdr_fc_cofactor_equationhs) + (ff_bn_mce_alternating_mdr_cofactor_equationhsf_prefix))) /\ ((((exists ff_h_mce_mdr_cofactor_equationhsf_prefix_positive. ff_h_mce_mdr_cofactor_equationhsf_prefix_positive + S (ff_p_mce_alternating_mdr_cofactor_equationhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_cofactor_equationhsf_prefix)) * ff_uc_mce_fold_mdr_cofactor_equationhsf)) /\ exists ff_q_mce_mdr_cofactor_equationhsf_prefix_positive. ff_ub_mce_fold_mdr_cofactor_equationhsf = ff_q_mce_mdr_cofactor_equationhsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_cofactor_equationhsf_prefix)) * ff_uc_mce_fold_mdr_cofactor_equationhsf) + (ff_p_mce_alternating_mdr_cofactor_equationhsf_prefix))) /\ ((((exists ff_h_mce_mdr_cofactor_equationhsf_prefix_negative. ff_h_mce_mdr_cofactor_equationhsf_prefix_negative + S (ff_n_mce_alternating_mdr_cofactor_equationhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_cofactor_equationhsf_prefix)) * ff_vc_mce_fold_mdr_cofactor_equationhsf)) /\ exists ff_q_mce_mdr_cofactor_equationhsf_prefix_negative. ff_vb_mce_fold_mdr_cofactor_equationhsf = ff_q_mce_mdr_cofactor_equationhsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_cofactor_equationhsf_prefix)) * ff_vc_mce_fold_mdr_cofactor_equationhsf) + (ff_n_mce_alternating_mdr_cofactor_equationhsf_prefix))) /\ (((exists ff_even_mce_term_mdr_cofactor_equationhsf_prefix_term. ff_index_mce_alternating_mdr_cofactor_equationhsf_prefix = 2 * ff_even_mce_term_mdr_cofactor_equationhsf_prefix_term) /\ (ff_p_mce_alternating_mdr_cofactor_equationhsf_prefix = (ff_ap_mce_alternating_mdr_cofactor_equationhsf_prefix) * (ff_bp_mce_alternating_mdr_cofactor_equationhsf_prefix) + (ff_an_mce_alternating_mdr_cofactor_equationhsf_prefix) * (ff_bn_mce_alternating_mdr_cofactor_equationhsf_prefix) /\ ff_n_mce_alternating_mdr_cofactor_equationhsf_prefix = (ff_ap_mce_alternating_mdr_cofactor_equationhsf_prefix) * (ff_bn_mce_alternating_mdr_cofactor_equationhsf_prefix) + (ff_an_mce_alternating_mdr_cofactor_equationhsf_prefix) * (ff_bp_mce_alternating_mdr_cofactor_equationhsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_cofactor_equationhsf_prefix_term. ff_index_mce_alternating_mdr_cofactor_equationhsf_prefix = 2 * ff_odd_mce_term_mdr_cofactor_equationhsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_cofactor_equationhsf_prefix = (ff_ap_mce_alternating_mdr_cofactor_equationhsf_prefix) * (ff_bn_mce_alternating_mdr_cofactor_equationhsf_prefix) + (ff_an_mce_alternating_mdr_cofactor_equationhsf_prefix) * (ff_bp_mce_alternating_mdr_cofactor_equationhsf_prefix) /\ ff_n_mce_alternating_mdr_cofactor_equationhsf_prefix = (ff_ap_mce_alternating_mdr_cofactor_equationhsf_prefix) * (ff_bp_mce_alternating_mdr_cofactor_equationhsf_prefix) + (ff_an_mce_alternating_mdr_cofactor_equationhsf_prefix) * (ff_bn_mce_alternating_mdr_cofactor_equationhsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_cofactor_equationhsf_positive ff_v_mce_mdr_cofactor_equationhsf_positive. ((((exists ff_h_mce_mdr_cofactor_equationhsf_positive_start. ff_h_mce_mdr_cofactor_equationhsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_cofactor_equationhsf_positive)) /\ exists ff_q_mce_mdr_cofactor_equationhsf_positive_start. ff_u_mce_mdr_cofactor_equationhsf_positive = ff_q_mce_mdr_cofactor_equationhsf_positive_start * S ((S (0)) * ff_v_mce_mdr_cofactor_equationhsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_cofactor_equationhsf_positive_terminal. ff_h_mce_mdr_cofactor_equationhsf_positive_terminal + S (mdr_p_cofactor_equationh) = S ((S ((S (mdr_q_cofactor_equationhs)))) * ff_v_mce_mdr_cofactor_equationhsf_positive)) /\ exists ff_q_mce_mdr_cofactor_equationhsf_positive_terminal. ff_u_mce_mdr_cofactor_equationhsf_positive = ff_q_mce_mdr_cofactor_equationhsf_positive_terminal * S ((S ((S (mdr_q_cofactor_equationhs)))) * ff_v_mce_mdr_cofactor_equationhsf_positive) + (mdr_p_cofactor_equationh))) /\ forall ff_i_mce_mdr_cofactor_equationhsf_positive. (exists ff_lt_mce_mdr_cofactor_equationhsf_positive_bound. ff_lt_mce_mdr_cofactor_equationhsf_positive_bound + S ff_i_mce_mdr_cofactor_equationhsf_positive = (S (mdr_q_cofactor_equationhs))) -> exists ff_a_mce_mdr_cofactor_equationhsf_positive ff_r_mce_mdr_cofactor_equationhsf_positive ff_s_mce_mdr_cofactor_equationhsf_positive. ((((exists ff_h_mce_mdr_cofactor_equationhsf_positive_summand. ff_h_mce_mdr_cofactor_equationhsf_positive_summand + S (ff_a_mce_mdr_cofactor_equationhsf_positive) = S ((S (ff_i_mce_mdr_cofactor_equationhsf_positive)) * ff_uc_mce_fold_mdr_cofactor_equationhsf)) /\ exists ff_q_mce_mdr_cofactor_equationhsf_positive_summand. ff_ub_mce_fold_mdr_cofactor_equationhsf = ff_q_mce_mdr_cofactor_equationhsf_positive_summand * S ((S (ff_i_mce_mdr_cofactor_equationhsf_positive)) * ff_uc_mce_fold_mdr_cofactor_equationhsf) + (ff_a_mce_mdr_cofactor_equationhsf_positive))) /\ ((((exists ff_h_mce_mdr_cofactor_equationhsf_positive_partial. ff_h_mce_mdr_cofactor_equationhsf_positive_partial + S (ff_r_mce_mdr_cofactor_equationhsf_positive) = S ((S (ff_i_mce_mdr_cofactor_equationhsf_positive)) * ff_v_mce_mdr_cofactor_equationhsf_positive)) /\ exists ff_q_mce_mdr_cofactor_equationhsf_positive_partial. ff_u_mce_mdr_cofactor_equationhsf_positive = ff_q_mce_mdr_cofactor_equationhsf_positive_partial * S ((S (ff_i_mce_mdr_cofactor_equationhsf_positive)) * ff_v_mce_mdr_cofactor_equationhsf_positive) + (ff_r_mce_mdr_cofactor_equationhsf_positive))) /\ ((((exists ff_h_mce_mdr_cofactor_equationhsf_positive_successor. ff_h_mce_mdr_cofactor_equationhsf_positive_successor + S (ff_s_mce_mdr_cofactor_equationhsf_positive) = S ((S (S ff_i_mce_mdr_cofactor_equationhsf_positive)) * ff_v_mce_mdr_cofactor_equationhsf_positive)) /\ exists ff_q_mce_mdr_cofactor_equationhsf_positive_successor. ff_u_mce_mdr_cofactor_equationhsf_positive = ff_q_mce_mdr_cofactor_equationhsf_positive_successor * S ((S (S ff_i_mce_mdr_cofactor_equationhsf_positive)) * ff_v_mce_mdr_cofactor_equationhsf_positive) + (ff_s_mce_mdr_cofactor_equationhsf_positive))) /\ ff_s_mce_mdr_cofactor_equationhsf_positive = ff_r_mce_mdr_cofactor_equationhsf_positive + ff_a_mce_mdr_cofactor_equationhsf_positive)))))) /\ (exists ff_u_mce_mdr_cofactor_equationhsf_negative ff_v_mce_mdr_cofactor_equationhsf_negative. ((((exists ff_h_mce_mdr_cofactor_equationhsf_negative_start. ff_h_mce_mdr_cofactor_equationhsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_cofactor_equationhsf_negative)) /\ exists ff_q_mce_mdr_cofactor_equationhsf_negative_start. ff_u_mce_mdr_cofactor_equationhsf_negative = ff_q_mce_mdr_cofactor_equationhsf_negative_start * S ((S (0)) * ff_v_mce_mdr_cofactor_equationhsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_cofactor_equationhsf_negative_terminal. ff_h_mce_mdr_cofactor_equationhsf_negative_terminal + S (mdr_n_cofactor_equationh) = S ((S ((S (mdr_q_cofactor_equationhs)))) * ff_v_mce_mdr_cofactor_equationhsf_negative)) /\ exists ff_q_mce_mdr_cofactor_equationhsf_negative_terminal. ff_u_mce_mdr_cofactor_equationhsf_negative = ff_q_mce_mdr_cofactor_equationhsf_negative_terminal * S ((S ((S (mdr_q_cofactor_equationhs)))) * ff_v_mce_mdr_cofactor_equationhsf_negative) + (mdr_n_cofactor_equationh))) /\ forall ff_i_mce_mdr_cofactor_equationhsf_negative. (exists ff_lt_mce_mdr_cofactor_equationhsf_negative_bound. ff_lt_mce_mdr_cofactor_equationhsf_negative_bound + S ff_i_mce_mdr_cofactor_equationhsf_negative = (S (mdr_q_cofactor_equationhs))) -> exists ff_a_mce_mdr_cofactor_equationhsf_negative ff_r_mce_mdr_cofactor_equationhsf_negative ff_s_mce_mdr_cofactor_equationhsf_negative. ((((exists ff_h_mce_mdr_cofactor_equationhsf_negative_summand. ff_h_mce_mdr_cofactor_equationhsf_negative_summand + S (ff_a_mce_mdr_cofactor_equationhsf_negative) = S ((S (ff_i_mce_mdr_cofactor_equationhsf_negative)) * ff_vc_mce_fold_mdr_cofactor_equationhsf)) /\ exists ff_q_mce_mdr_cofactor_equationhsf_negative_summand. ff_vb_mce_fold_mdr_cofactor_equationhsf = ff_q_mce_mdr_cofactor_equationhsf_negative_summand * S ((S (ff_i_mce_mdr_cofactor_equationhsf_negative)) * ff_vc_mce_fold_mdr_cofactor_equationhsf) + (ff_a_mce_mdr_cofactor_equationhsf_negative))) /\ ((((exists ff_h_mce_mdr_cofactor_equationhsf_negative_partial. ff_h_mce_mdr_cofactor_equationhsf_negative_partial + S (ff_r_mce_mdr_cofactor_equationhsf_negative) = S ((S (ff_i_mce_mdr_cofactor_equationhsf_negative)) * ff_v_mce_mdr_cofactor_equationhsf_negative)) /\ exists ff_q_mce_mdr_cofactor_equationhsf_negative_partial. ff_u_mce_mdr_cofactor_equationhsf_negative = ff_q_mce_mdr_cofactor_equationhsf_negative_partial * S ((S (ff_i_mce_mdr_cofactor_equationhsf_negative)) * ff_v_mce_mdr_cofactor_equationhsf_negative) + (ff_r_mce_mdr_cofactor_equationhsf_negative))) /\ ((((exists ff_h_mce_mdr_cofactor_equationhsf_negative_successor. ff_h_mce_mdr_cofactor_equationhsf_negative_successor + S (ff_s_mce_mdr_cofactor_equationhsf_negative) = S ((S (S ff_i_mce_mdr_cofactor_equationhsf_negative)) * ff_v_mce_mdr_cofactor_equationhsf_negative)) /\ exists ff_q_mce_mdr_cofactor_equationhsf_negative_successor. ff_u_mce_mdr_cofactor_equationhsf_negative = ff_q_mce_mdr_cofactor_equationhsf_negative_successor * S ((S (S ff_i_mce_mdr_cofactor_equationhsf_negative)) * ff_v_mce_mdr_cofactor_equationhsf_negative) + (ff_s_mce_mdr_cofactor_equationhsf_negative))) /\ ff_s_mce_mdr_cofactor_equationhsf_negative = ff_r_mce_mdr_cofactor_equationhsf_negative + ff_a_mce_mdr_cofactor_equationhsf_negative))))))))))))))) /\ ((exists mdr_gap_cofactor_equationi. mdr_gap_cofactor_equationi + S (mdr_i_cofactor_equation) = (mdr_l_cofactor_equation)) /\ (exists mdr_z_cofactor_equationr. ((exists mdr_a_cofactor_equationrc mdr_b_cofactor_equationrc mdr_c_cofactor_equationrc mdr_e_cofactor_equationrc mdr_f_cofactor_equationrc. ((mdr_a_cofactor_equationrc = ((S q) + (pb)) * S ((S q) + (pb)) + ((pb) + (pb))) /\ ((mdr_b_cofactor_equationrc = ((pc) + (nb)) * S ((pc) + (nb)) + ((nb) + (nb))) /\ ((mdr_c_cofactor_equationrc = ((mdr_a_cofactor_equationrc) + (mdr_b_cofactor_equationrc)) * S ((mdr_a_cofactor_equationrc) + (mdr_b_cofactor_equationrc)) + ((mdr_b_cofactor_equationrc) + (mdr_b_cofactor_equationrc))) /\ ((mdr_e_cofactor_equationrc = ((p) + (n)) * S ((p) + (n)) + ((n) + (n))) /\ ((mdr_f_cofactor_equationrc = ((nc) + (mdr_e_cofactor_equationrc)) * S ((nc) + (mdr_e_cofactor_equationrc)) + ((mdr_e_cofactor_equationrc) + (mdr_e_cofactor_equationrc))) /\ ((mdr_z_cofactor_equationr) = ((mdr_c_cofactor_equationrc) + (mdr_f_cofactor_equationrc)) * S ((mdr_c_cofactor_equationrc) + (mdr_f_cofactor_equationrc)) + ((mdr_f_cofactor_equationrc) + (mdr_f_cofactor_equationrc))))))))) /\ (((exists ff_h_mdr_cofactor_equationrb. ff_h_mdr_cofactor_equationrb + S (mdr_z_cofactor_equationr) = S ((S (mdr_i_cofactor_equation)) * mdr_c_cofactor_equation)) /\ exists ff_q_mdr_cofactor_equationrb. mdr_b_cofactor_equation = ff_q_mdr_cofactor_equationrb * S ((S (mdr_i_cofactor_equation)) * mdr_c_cofactor_equation) + (mdr_z_cofactor_equationr))))))))