signed_recursive_determinant_successor_decomposition

Exact expanded first-order arithmetic statement

forall pb pc nb nc q p n. (exists mdr_b_successor_source mdr_c_successor_source mdr_l_successor_source mdr_i_successor_source. ((forall mdr_i_successor_sourceh. (exists mdr_gap_successor_sourcehi. mdr_gap_successor_sourcehi + S (mdr_i_successor_sourceh) = (mdr_l_successor_source)) -> exists mdr_d_successor_sourceh mdr_pb_successor_sourceh mdr_pc_successor_sourceh mdr_nb_successor_sourceh mdr_nc_successor_sourceh mdr_p_successor_sourceh mdr_n_successor_sourceh. ((exists mdr_z_successor_sourcehr. ((exists mdr_a_successor_sourcehrc mdr_b_successor_sourcehrc mdr_c_successor_sourcehrc mdr_e_successor_sourcehrc mdr_f_successor_sourcehrc. ((mdr_a_successor_sourcehrc = ((mdr_d_successor_sourceh) + (mdr_pb_successor_sourceh)) * S ((mdr_d_successor_sourceh) + (mdr_pb_successor_sourceh)) + ((mdr_pb_successor_sourceh) + (mdr_pb_successor_sourceh))) /\ ((mdr_b_successor_sourcehrc = ((mdr_pc_successor_sourceh) + (mdr_nb_successor_sourceh)) * S ((mdr_pc_successor_sourceh) + (mdr_nb_successor_sourceh)) + ((mdr_nb_successor_sourceh) + (mdr_nb_successor_sourceh))) /\ ((mdr_c_successor_sourcehrc = ((mdr_a_successor_sourcehrc) + (mdr_b_successor_sourcehrc)) * S ((mdr_a_successor_sourcehrc) + (mdr_b_successor_sourcehrc)) + ((mdr_b_successor_sourcehrc) + (mdr_b_successor_sourcehrc))) /\ ((mdr_e_successor_sourcehrc = ((mdr_p_successor_sourceh) + (mdr_n_successor_sourceh)) * S ((mdr_p_successor_sourceh) + (mdr_n_successor_sourceh)) + ((mdr_n_successor_sourceh) + (mdr_n_successor_sourceh))) /\ ((mdr_f_successor_sourcehrc = ((mdr_nc_successor_sourceh) + (mdr_e_successor_sourcehrc)) * S ((mdr_nc_successor_sourceh) + (mdr_e_successor_sourcehrc)) + ((mdr_e_successor_sourcehrc) + (mdr_e_successor_sourcehrc))) /\ ((mdr_z_successor_sourcehr) = ((mdr_c_successor_sourcehrc) + (mdr_f_successor_sourcehrc)) * S ((mdr_c_successor_sourcehrc) + (mdr_f_successor_sourcehrc)) + ((mdr_f_successor_sourcehrc) + (mdr_f_successor_sourcehrc))))))))) /\ (((exists ff_h_mdr_successor_sourcehrb. ff_h_mdr_successor_sourcehrb + S (mdr_z_successor_sourcehr) = S ((S (mdr_i_successor_sourceh)) * mdr_c_successor_source)) /\ exists ff_q_mdr_successor_sourcehrb. mdr_b_successor_source = ff_q_mdr_successor_sourcehrb * S ((S (mdr_i_successor_sourceh)) * mdr_c_successor_source) + (mdr_z_successor_sourcehr))))) /\ (((((mdr_d_successor_sourceh) = 0) /\ (((mdr_p_successor_sourceh) = 1) /\ ((mdr_n_successor_sourceh) = 0))) \/ exists mdr_q_successor_sourcehs mdr_eb_successor_sourcehs mdr_ec_successor_sourcehs mdr_fb_successor_sourcehs mdr_fc_successor_sourcehs. (((mdr_d_successor_sourceh) = S (mdr_q_successor_sourcehs)) /\ ((forall mdr_j_successor_sourcehsc. (exists mdr_gap_successor_sourcehscj. mdr_gap_successor_sourcehscj + S (mdr_j_successor_sourcehsc) = (S (mdr_q_successor_sourcehs))) -> exists mdr_i_successor_sourcehsc mdr_up_successor_sourcehsc mdr_us_successor_sourcehsc mdr_un_successor_sourcehsc mdr_ut_successor_sourcehsc mdr_p_successor_sourcehsc mdr_n_successor_sourcehsc. ((exists mdr_gap_successor_sourcehsci. mdr_gap_successor_sourcehsci + S (mdr_i_successor_sourcehsc) = (mdr_i_successor_sourceh)) /\ ((exists mdr_z_successor_sourcehscr. ((exists mdr_a_successor_sourcehscrc mdr_b_successor_sourcehscrc mdr_c_successor_sourcehscrc mdr_e_successor_sourcehscrc mdr_f_successor_sourcehscrc. ((mdr_a_successor_sourcehscrc = ((mdr_q_successor_sourcehs) + (mdr_up_successor_sourcehsc)) * S ((mdr_q_successor_sourcehs) + (mdr_up_successor_sourcehsc)) + ((mdr_up_successor_sourcehsc) + (mdr_up_successor_sourcehsc))) /\ ((mdr_b_successor_sourcehscrc = ((mdr_us_successor_sourcehsc) + (mdr_un_successor_sourcehsc)) * S ((mdr_us_successor_sourcehsc) + (mdr_un_successor_sourcehsc)) + ((mdr_un_successor_sourcehsc) + (mdr_un_successor_sourcehsc))) /\ ((mdr_c_successor_sourcehscrc = ((mdr_a_successor_sourcehscrc) + (mdr_b_successor_sourcehscrc)) * S ((mdr_a_successor_sourcehscrc) + (mdr_b_successor_sourcehscrc)) + ((mdr_b_successor_sourcehscrc) + (mdr_b_successor_sourcehscrc))) /\ ((mdr_e_successor_sourcehscrc = ((mdr_p_successor_sourcehsc) + (mdr_n_successor_sourcehsc)) * S ((mdr_p_successor_sourcehsc) + (mdr_n_successor_sourcehsc)) + ((mdr_n_successor_sourcehsc) + (mdr_n_successor_sourcehsc))) /\ ((mdr_f_successor_sourcehscrc = ((mdr_ut_successor_sourcehsc) + (mdr_e_successor_sourcehscrc)) * S ((mdr_ut_successor_sourcehsc) + (mdr_e_successor_sourcehscrc)) + ((mdr_e_successor_sourcehscrc) + (mdr_e_successor_sourcehscrc))) /\ ((mdr_z_successor_sourcehscr) = ((mdr_c_successor_sourcehscrc) + (mdr_f_successor_sourcehscrc)) * S ((mdr_c_successor_sourcehscrc) + (mdr_f_successor_sourcehscrc)) + ((mdr_f_successor_sourcehscrc) + (mdr_f_successor_sourcehscrc))))))))) /\ (((exists ff_h_mdr_successor_sourcehscrb. ff_h_mdr_successor_sourcehscrb + S (mdr_z_successor_sourcehscr) = S ((S (mdr_i_successor_sourcehsc)) * mdr_c_successor_source)) /\ exists ff_q_mdr_successor_sourcehscrb. mdr_b_successor_source = ff_q_mdr_successor_sourcehscrb * S ((S (mdr_i_successor_sourcehsc)) * mdr_c_successor_source) + (mdr_z_successor_sourcehscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_successor_sourcehscm_positive. (exists ff_gap_mdm_lt_mdr_successor_sourcehscm_positive_index_bound. ff_gap_mdm_lt_mdr_successor_sourcehscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_successor_sourcehscm_positive) = ((mdr_q_successor_sourcehs) * (mdr_q_successor_sourcehs))) -> exists ff_row_mdm_prefix_mdr_successor_sourcehscm_positive ff_column_mdm_prefix_mdr_successor_sourcehscm_positive ff_value_mdm_prefix_mdr_successor_sourcehscm_positive. (ff_index_mdm_prefix_mdr_successor_sourcehscm_positive = (mdr_q_successor_sourcehs) * ff_row_mdm_prefix_mdr_successor_sourcehscm_positive + ff_column_mdm_prefix_mdr_successor_sourcehscm_positive /\ ((exists ff_gap_mdm_lt_mdr_successor_sourcehscm_positive_column_bound. ff_gap_mdm_lt_mdr_successor_sourcehscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_successor_sourcehscm_positive) = (mdr_q_successor_sourcehs)) /\ ((exists ff_row_mdm_cell_mdr_successor_sourcehscm_positive_cell ff_column_mdm_cell_mdr_successor_sourcehscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_successor_sourcehscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_successor_sourcehscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_successor_sourcehscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_successor_sourcehscm_positive_cell = ff_row_mdm_prefix_mdr_successor_sourcehscm_positive) \/ ((exists ff_gap_mdm_le_mdr_successor_sourcehscm_positive_cell_row_after. ff_gap_mdm_le_mdr_successor_sourcehscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_successor_sourcehscm_positive)) /\ ff_row_mdm_cell_mdr_successor_sourcehscm_positive_cell = S ff_row_mdm_prefix_mdr_successor_sourcehscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_successor_sourcehscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_successor_sourcehscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_successor_sourcehscm_positive) = (mdr_j_successor_sourcehsc)) /\ ff_column_mdm_cell_mdr_successor_sourcehscm_positive_cell = ff_column_mdm_prefix_mdr_successor_sourcehscm_positive) \/ ((exists ff_gap_mdm_le_mdr_successor_sourcehscm_positive_cell_column_after. ff_gap_mdm_le_mdr_successor_sourcehscm_positive_cell_column_after + (mdr_j_successor_sourcehsc) = (ff_column_mdm_prefix_mdr_successor_sourcehscm_positive)) /\ ff_column_mdm_cell_mdr_successor_sourcehscm_positive_cell = S ff_column_mdm_prefix_mdr_successor_sourcehscm_positive))) /\ (((exists ff_h_mdm_mdr_successor_sourcehscm_positive_cell_source. ff_h_mdm_mdr_successor_sourcehscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_successor_sourcehscm_positive) = S ((S ((ff_row_mdm_cell_mdr_successor_sourcehscm_positive_cell) * (S (mdr_q_successor_sourcehs)) + (ff_column_mdm_cell_mdr_successor_sourcehscm_positive_cell))) * mdr_pc_successor_sourceh)) /\ exists ff_q_mdm_mdr_successor_sourcehscm_positive_cell_source. mdr_pb_successor_sourceh = ff_q_mdm_mdr_successor_sourcehscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_successor_sourcehscm_positive_cell) * (S (mdr_q_successor_sourcehs)) + (ff_column_mdm_cell_mdr_successor_sourcehscm_positive_cell))) * mdr_pc_successor_sourceh) + (ff_value_mdm_prefix_mdr_successor_sourcehscm_positive)))))) /\ (((exists ff_h_mdm_mdr_successor_sourcehscm_positive_target. ff_h_mdm_mdr_successor_sourcehscm_positive_target + S (ff_value_mdm_prefix_mdr_successor_sourcehscm_positive) = S ((S (ff_index_mdm_prefix_mdr_successor_sourcehscm_positive)) * mdr_us_successor_sourcehsc)) /\ exists ff_q_mdm_mdr_successor_sourcehscm_positive_target. mdr_up_successor_sourcehsc = ff_q_mdm_mdr_successor_sourcehscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_successor_sourcehscm_positive)) * mdr_us_successor_sourcehsc) + (ff_value_mdm_prefix_mdr_successor_sourcehscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_successor_sourcehscm_negative. (exists ff_gap_mdm_lt_mdr_successor_sourcehscm_negative_index_bound. ff_gap_mdm_lt_mdr_successor_sourcehscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_successor_sourcehscm_negative) = ((mdr_q_successor_sourcehs) * (mdr_q_successor_sourcehs))) -> exists ff_row_mdm_prefix_mdr_successor_sourcehscm_negative ff_column_mdm_prefix_mdr_successor_sourcehscm_negative ff_value_mdm_prefix_mdr_successor_sourcehscm_negative. (ff_index_mdm_prefix_mdr_successor_sourcehscm_negative = (mdr_q_successor_sourcehs) * ff_row_mdm_prefix_mdr_successor_sourcehscm_negative + ff_column_mdm_prefix_mdr_successor_sourcehscm_negative /\ ((exists ff_gap_mdm_lt_mdr_successor_sourcehscm_negative_column_bound. ff_gap_mdm_lt_mdr_successor_sourcehscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_successor_sourcehscm_negative) = (mdr_q_successor_sourcehs)) /\ ((exists ff_row_mdm_cell_mdr_successor_sourcehscm_negative_cell ff_column_mdm_cell_mdr_successor_sourcehscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_successor_sourcehscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_successor_sourcehscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_successor_sourcehscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_successor_sourcehscm_negative_cell = ff_row_mdm_prefix_mdr_successor_sourcehscm_negative) \/ ((exists ff_gap_mdm_le_mdr_successor_sourcehscm_negative_cell_row_after. ff_gap_mdm_le_mdr_successor_sourcehscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_successor_sourcehscm_negative)) /\ ff_row_mdm_cell_mdr_successor_sourcehscm_negative_cell = S ff_row_mdm_prefix_mdr_successor_sourcehscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_successor_sourcehscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_successor_sourcehscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_successor_sourcehscm_negative) = (mdr_j_successor_sourcehsc)) /\ ff_column_mdm_cell_mdr_successor_sourcehscm_negative_cell = ff_column_mdm_prefix_mdr_successor_sourcehscm_negative) \/ ((exists ff_gap_mdm_le_mdr_successor_sourcehscm_negative_cell_column_after. ff_gap_mdm_le_mdr_successor_sourcehscm_negative_cell_column_after + (mdr_j_successor_sourcehsc) = (ff_column_mdm_prefix_mdr_successor_sourcehscm_negative)) /\ ff_column_mdm_cell_mdr_successor_sourcehscm_negative_cell = S ff_column_mdm_prefix_mdr_successor_sourcehscm_negative))) /\ (((exists ff_h_mdm_mdr_successor_sourcehscm_negative_cell_source. ff_h_mdm_mdr_successor_sourcehscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_successor_sourcehscm_negative) = S ((S ((ff_row_mdm_cell_mdr_successor_sourcehscm_negative_cell) * (S (mdr_q_successor_sourcehs)) + (ff_column_mdm_cell_mdr_successor_sourcehscm_negative_cell))) * mdr_nc_successor_sourceh)) /\ exists ff_q_mdm_mdr_successor_sourcehscm_negative_cell_source. mdr_nb_successor_sourceh = ff_q_mdm_mdr_successor_sourcehscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_successor_sourcehscm_negative_cell) * (S (mdr_q_successor_sourcehs)) + (ff_column_mdm_cell_mdr_successor_sourcehscm_negative_cell))) * mdr_nc_successor_sourceh) + (ff_value_mdm_prefix_mdr_successor_sourcehscm_negative)))))) /\ (((exists ff_h_mdm_mdr_successor_sourcehscm_negative_target. ff_h_mdm_mdr_successor_sourcehscm_negative_target + S (ff_value_mdm_prefix_mdr_successor_sourcehscm_negative) = S ((S (ff_index_mdm_prefix_mdr_successor_sourcehscm_negative)) * mdr_ut_successor_sourcehsc)) /\ exists ff_q_mdm_mdr_successor_sourcehscm_negative_target. mdr_un_successor_sourcehsc = ff_q_mdm_mdr_successor_sourcehscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_successor_sourcehscm_negative)) * mdr_ut_successor_sourcehsc) + (ff_value_mdm_prefix_mdr_successor_sourcehscm_negative))))))))) /\ ((((exists ff_h_mdr_successor_sourcehscp. ff_h_mdr_successor_sourcehscp + S (mdr_p_successor_sourcehsc) = S ((S (mdr_j_successor_sourcehsc)) * mdr_ec_successor_sourcehs)) /\ exists ff_q_mdr_successor_sourcehscp. mdr_eb_successor_sourcehs = ff_q_mdr_successor_sourcehscp * S ((S (mdr_j_successor_sourcehsc)) * mdr_ec_successor_sourcehs) + (mdr_p_successor_sourcehsc))) /\ (((exists ff_h_mdr_successor_sourcehscn. ff_h_mdr_successor_sourcehscn + S (mdr_n_successor_sourcehsc) = S ((S (mdr_j_successor_sourcehsc)) * mdr_fc_successor_sourcehs)) /\ exists ff_q_mdr_successor_sourcehscn. mdr_fb_successor_sourcehs = ff_q_mdr_successor_sourcehscn * S ((S (mdr_j_successor_sourcehsc)) * mdr_fc_successor_sourcehs) + (mdr_n_successor_sourcehsc)))))))) /\ (exists ff_ub_mce_fold_mdr_successor_sourcehsf ff_uc_mce_fold_mdr_successor_sourcehsf ff_vb_mce_fold_mdr_successor_sourcehsf ff_vc_mce_fold_mdr_successor_sourcehsf. ((forall ff_index_mce_alternating_mdr_successor_sourcehsf_prefix. (exists ff_gap_mce_mdr_successor_sourcehsf_prefix_index. ff_gap_mce_mdr_successor_sourcehsf_prefix_index + S (ff_index_mce_alternating_mdr_successor_sourcehsf_prefix) = (S (mdr_q_successor_sourcehs))) -> exists ff_ap_mce_alternating_mdr_successor_sourcehsf_prefix ff_an_mce_alternating_mdr_successor_sourcehsf_prefix ff_bp_mce_alternating_mdr_successor_sourcehsf_prefix ff_bn_mce_alternating_mdr_successor_sourcehsf_prefix ff_p_mce_alternating_mdr_successor_sourcehsf_prefix ff_n_mce_alternating_mdr_successor_sourcehsf_prefix. ((((exists ff_h_mce_mdr_successor_sourcehsf_prefix_ap. ff_h_mce_mdr_successor_sourcehsf_prefix_ap + S (ff_ap_mce_alternating_mdr_successor_sourcehsf_prefix) = S ((S (ff_index_mce_alternating_mdr_successor_sourcehsf_prefix)) * mdr_pc_successor_sourceh)) /\ exists ff_q_mce_mdr_successor_sourcehsf_prefix_ap. mdr_pb_successor_sourceh = ff_q_mce_mdr_successor_sourcehsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_successor_sourcehsf_prefix)) * mdr_pc_successor_sourceh) + (ff_ap_mce_alternating_mdr_successor_sourcehsf_prefix))) /\ ((((exists ff_h_mce_mdr_successor_sourcehsf_prefix_an. ff_h_mce_mdr_successor_sourcehsf_prefix_an + S (ff_an_mce_alternating_mdr_successor_sourcehsf_prefix) = S ((S (ff_index_mce_alternating_mdr_successor_sourcehsf_prefix)) * mdr_nc_successor_sourceh)) /\ exists ff_q_mce_mdr_successor_sourcehsf_prefix_an. mdr_nb_successor_sourceh = ff_q_mce_mdr_successor_sourcehsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_successor_sourcehsf_prefix)) * mdr_nc_successor_sourceh) + (ff_an_mce_alternating_mdr_successor_sourcehsf_prefix))) /\ ((((exists ff_h_mce_mdr_successor_sourcehsf_prefix_bp. ff_h_mce_mdr_successor_sourcehsf_prefix_bp + S (ff_bp_mce_alternating_mdr_successor_sourcehsf_prefix) = S ((S (ff_index_mce_alternating_mdr_successor_sourcehsf_prefix)) * mdr_ec_successor_sourcehs)) /\ exists ff_q_mce_mdr_successor_sourcehsf_prefix_bp. mdr_eb_successor_sourcehs = ff_q_mce_mdr_successor_sourcehsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_successor_sourcehsf_prefix)) * mdr_ec_successor_sourcehs) + (ff_bp_mce_alternating_mdr_successor_sourcehsf_prefix))) /\ ((((exists ff_h_mce_mdr_successor_sourcehsf_prefix_bn. ff_h_mce_mdr_successor_sourcehsf_prefix_bn + S (ff_bn_mce_alternating_mdr_successor_sourcehsf_prefix) = S ((S (ff_index_mce_alternating_mdr_successor_sourcehsf_prefix)) * mdr_fc_successor_sourcehs)) /\ exists ff_q_mce_mdr_successor_sourcehsf_prefix_bn. mdr_fb_successor_sourcehs = ff_q_mce_mdr_successor_sourcehsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_successor_sourcehsf_prefix)) * mdr_fc_successor_sourcehs) + (ff_bn_mce_alternating_mdr_successor_sourcehsf_prefix))) /\ ((((exists ff_h_mce_mdr_successor_sourcehsf_prefix_positive. ff_h_mce_mdr_successor_sourcehsf_prefix_positive + S (ff_p_mce_alternating_mdr_successor_sourcehsf_prefix) = S ((S (ff_index_mce_alternating_mdr_successor_sourcehsf_prefix)) * ff_uc_mce_fold_mdr_successor_sourcehsf)) /\ exists ff_q_mce_mdr_successor_sourcehsf_prefix_positive. ff_ub_mce_fold_mdr_successor_sourcehsf = ff_q_mce_mdr_successor_sourcehsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_successor_sourcehsf_prefix)) * ff_uc_mce_fold_mdr_successor_sourcehsf) + (ff_p_mce_alternating_mdr_successor_sourcehsf_prefix))) /\ ((((exists ff_h_mce_mdr_successor_sourcehsf_prefix_negative. ff_h_mce_mdr_successor_sourcehsf_prefix_negative + S (ff_n_mce_alternating_mdr_successor_sourcehsf_prefix) = S ((S (ff_index_mce_alternating_mdr_successor_sourcehsf_prefix)) * ff_vc_mce_fold_mdr_successor_sourcehsf)) /\ exists ff_q_mce_mdr_successor_sourcehsf_prefix_negative. ff_vb_mce_fold_mdr_successor_sourcehsf = ff_q_mce_mdr_successor_sourcehsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_successor_sourcehsf_prefix)) * ff_vc_mce_fold_mdr_successor_sourcehsf) + (ff_n_mce_alternating_mdr_successor_sourcehsf_prefix))) /\ (((exists ff_even_mce_term_mdr_successor_sourcehsf_prefix_term. ff_index_mce_alternating_mdr_successor_sourcehsf_prefix = 2 * ff_even_mce_term_mdr_successor_sourcehsf_prefix_term) /\ (ff_p_mce_alternating_mdr_successor_sourcehsf_prefix = (ff_ap_mce_alternating_mdr_successor_sourcehsf_prefix) * (ff_bp_mce_alternating_mdr_successor_sourcehsf_prefix) + (ff_an_mce_alternating_mdr_successor_sourcehsf_prefix) * (ff_bn_mce_alternating_mdr_successor_sourcehsf_prefix) /\ ff_n_mce_alternating_mdr_successor_sourcehsf_prefix = (ff_ap_mce_alternating_mdr_successor_sourcehsf_prefix) * (ff_bn_mce_alternating_mdr_successor_sourcehsf_prefix) + (ff_an_mce_alternating_mdr_successor_sourcehsf_prefix) * (ff_bp_mce_alternating_mdr_successor_sourcehsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_successor_sourcehsf_prefix_term. ff_index_mce_alternating_mdr_successor_sourcehsf_prefix = 2 * ff_odd_mce_term_mdr_successor_sourcehsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_successor_sourcehsf_prefix = (ff_ap_mce_alternating_mdr_successor_sourcehsf_prefix) * (ff_bn_mce_alternating_mdr_successor_sourcehsf_prefix) + (ff_an_mce_alternating_mdr_successor_sourcehsf_prefix) * (ff_bp_mce_alternating_mdr_successor_sourcehsf_prefix) /\ ff_n_mce_alternating_mdr_successor_sourcehsf_prefix = (ff_ap_mce_alternating_mdr_successor_sourcehsf_prefix) * (ff_bp_mce_alternating_mdr_successor_sourcehsf_prefix) + (ff_an_mce_alternating_mdr_successor_sourcehsf_prefix) * (ff_bn_mce_alternating_mdr_successor_sourcehsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_successor_sourcehsf_positive ff_v_mce_mdr_successor_sourcehsf_positive. ((((exists ff_h_mce_mdr_successor_sourcehsf_positive_start. ff_h_mce_mdr_successor_sourcehsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_successor_sourcehsf_positive)) /\ exists ff_q_mce_mdr_successor_sourcehsf_positive_start. ff_u_mce_mdr_successor_sourcehsf_positive = ff_q_mce_mdr_successor_sourcehsf_positive_start * S ((S (0)) * ff_v_mce_mdr_successor_sourcehsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_successor_sourcehsf_positive_terminal. ff_h_mce_mdr_successor_sourcehsf_positive_terminal + S (mdr_p_successor_sourceh) = S ((S ((S (mdr_q_successor_sourcehs)))) * ff_v_mce_mdr_successor_sourcehsf_positive)) /\ exists ff_q_mce_mdr_successor_sourcehsf_positive_terminal. ff_u_mce_mdr_successor_sourcehsf_positive = ff_q_mce_mdr_successor_sourcehsf_positive_terminal * S ((S ((S (mdr_q_successor_sourcehs)))) * ff_v_mce_mdr_successor_sourcehsf_positive) + (mdr_p_successor_sourceh))) /\ forall ff_i_mce_mdr_successor_sourcehsf_positive. (exists ff_lt_mce_mdr_successor_sourcehsf_positive_bound. ff_lt_mce_mdr_successor_sourcehsf_positive_bound + S ff_i_mce_mdr_successor_sourcehsf_positive = (S (mdr_q_successor_sourcehs))) -> exists ff_a_mce_mdr_successor_sourcehsf_positive ff_r_mce_mdr_successor_sourcehsf_positive ff_s_mce_mdr_successor_sourcehsf_positive. ((((exists ff_h_mce_mdr_successor_sourcehsf_positive_summand. ff_h_mce_mdr_successor_sourcehsf_positive_summand + S (ff_a_mce_mdr_successor_sourcehsf_positive) = S ((S (ff_i_mce_mdr_successor_sourcehsf_positive)) * ff_uc_mce_fold_mdr_successor_sourcehsf)) /\ exists ff_q_mce_mdr_successor_sourcehsf_positive_summand. ff_ub_mce_fold_mdr_successor_sourcehsf = ff_q_mce_mdr_successor_sourcehsf_positive_summand * S ((S (ff_i_mce_mdr_successor_sourcehsf_positive)) * ff_uc_mce_fold_mdr_successor_sourcehsf) + (ff_a_mce_mdr_successor_sourcehsf_positive))) /\ ((((exists ff_h_mce_mdr_successor_sourcehsf_positive_partial. ff_h_mce_mdr_successor_sourcehsf_positive_partial + S (ff_r_mce_mdr_successor_sourcehsf_positive) = S ((S (ff_i_mce_mdr_successor_sourcehsf_positive)) * ff_v_mce_mdr_successor_sourcehsf_positive)) /\ exists ff_q_mce_mdr_successor_sourcehsf_positive_partial. ff_u_mce_mdr_successor_sourcehsf_positive = ff_q_mce_mdr_successor_sourcehsf_positive_partial * S ((S (ff_i_mce_mdr_successor_sourcehsf_positive)) * ff_v_mce_mdr_successor_sourcehsf_positive) + (ff_r_mce_mdr_successor_sourcehsf_positive))) /\ ((((exists ff_h_mce_mdr_successor_sourcehsf_positive_successor. ff_h_mce_mdr_successor_sourcehsf_positive_successor + S (ff_s_mce_mdr_successor_sourcehsf_positive) = S ((S (S ff_i_mce_mdr_successor_sourcehsf_positive)) * ff_v_mce_mdr_successor_sourcehsf_positive)) /\ exists ff_q_mce_mdr_successor_sourcehsf_positive_successor. ff_u_mce_mdr_successor_sourcehsf_positive = ff_q_mce_mdr_successor_sourcehsf_positive_successor * S ((S (S ff_i_mce_mdr_successor_sourcehsf_positive)) * ff_v_mce_mdr_successor_sourcehsf_positive) + (ff_s_mce_mdr_successor_sourcehsf_positive))) /\ ff_s_mce_mdr_successor_sourcehsf_positive = ff_r_mce_mdr_successor_sourcehsf_positive + ff_a_mce_mdr_successor_sourcehsf_positive)))))) /\ (exists ff_u_mce_mdr_successor_sourcehsf_negative ff_v_mce_mdr_successor_sourcehsf_negative. ((((exists ff_h_mce_mdr_successor_sourcehsf_negative_start. ff_h_mce_mdr_successor_sourcehsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_successor_sourcehsf_negative)) /\ exists ff_q_mce_mdr_successor_sourcehsf_negative_start. ff_u_mce_mdr_successor_sourcehsf_negative = ff_q_mce_mdr_successor_sourcehsf_negative_start * S ((S (0)) * ff_v_mce_mdr_successor_sourcehsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_successor_sourcehsf_negative_terminal. ff_h_mce_mdr_successor_sourcehsf_negative_terminal + S (mdr_n_successor_sourceh) = S ((S ((S (mdr_q_successor_sourcehs)))) * ff_v_mce_mdr_successor_sourcehsf_negative)) /\ exists ff_q_mce_mdr_successor_sourcehsf_negative_terminal. ff_u_mce_mdr_successor_sourcehsf_negative = ff_q_mce_mdr_successor_sourcehsf_negative_terminal * S ((S ((S (mdr_q_successor_sourcehs)))) * ff_v_mce_mdr_successor_sourcehsf_negative) + (mdr_n_successor_sourceh))) /\ forall ff_i_mce_mdr_successor_sourcehsf_negative. (exists ff_lt_mce_mdr_successor_sourcehsf_negative_bound. ff_lt_mce_mdr_successor_sourcehsf_negative_bound + S ff_i_mce_mdr_successor_sourcehsf_negative = (S (mdr_q_successor_sourcehs))) -> exists ff_a_mce_mdr_successor_sourcehsf_negative ff_r_mce_mdr_successor_sourcehsf_negative ff_s_mce_mdr_successor_sourcehsf_negative. ((((exists ff_h_mce_mdr_successor_sourcehsf_negative_summand. ff_h_mce_mdr_successor_sourcehsf_negative_summand + S (ff_a_mce_mdr_successor_sourcehsf_negative) = S ((S (ff_i_mce_mdr_successor_sourcehsf_negative)) * ff_vc_mce_fold_mdr_successor_sourcehsf)) /\ exists ff_q_mce_mdr_successor_sourcehsf_negative_summand. ff_vb_mce_fold_mdr_successor_sourcehsf = ff_q_mce_mdr_successor_sourcehsf_negative_summand * S ((S (ff_i_mce_mdr_successor_sourcehsf_negative)) * ff_vc_mce_fold_mdr_successor_sourcehsf) + (ff_a_mce_mdr_successor_sourcehsf_negative))) /\ ((((exists ff_h_mce_mdr_successor_sourcehsf_negative_partial. ff_h_mce_mdr_successor_sourcehsf_negative_partial + S (ff_r_mce_mdr_successor_sourcehsf_negative) = S ((S (ff_i_mce_mdr_successor_sourcehsf_negative)) * ff_v_mce_mdr_successor_sourcehsf_negative)) /\ exists ff_q_mce_mdr_successor_sourcehsf_negative_partial. ff_u_mce_mdr_successor_sourcehsf_negative = ff_q_mce_mdr_successor_sourcehsf_negative_partial * S ((S (ff_i_mce_mdr_successor_sourcehsf_negative)) * ff_v_mce_mdr_successor_sourcehsf_negative) + (ff_r_mce_mdr_successor_sourcehsf_negative))) /\ ((((exists ff_h_mce_mdr_successor_sourcehsf_negative_successor. ff_h_mce_mdr_successor_sourcehsf_negative_successor + S (ff_s_mce_mdr_successor_sourcehsf_negative) = S ((S (S ff_i_mce_mdr_successor_sourcehsf_negative)) * ff_v_mce_mdr_successor_sourcehsf_negative)) /\ exists ff_q_mce_mdr_successor_sourcehsf_negative_successor. ff_u_mce_mdr_successor_sourcehsf_negative = ff_q_mce_mdr_successor_sourcehsf_negative_successor * S ((S (S ff_i_mce_mdr_successor_sourcehsf_negative)) * ff_v_mce_mdr_successor_sourcehsf_negative) + (ff_s_mce_mdr_successor_sourcehsf_negative))) /\ ff_s_mce_mdr_successor_sourcehsf_negative = ff_r_mce_mdr_successor_sourcehsf_negative + ff_a_mce_mdr_successor_sourcehsf_negative))))))))))))))) /\ ((exists mdr_gap_successor_sourcei. mdr_gap_successor_sourcei + S (mdr_i_successor_source) = (mdr_l_successor_source)) /\ (exists mdr_z_successor_sourcer. ((exists mdr_a_successor_sourcerc mdr_b_successor_sourcerc mdr_c_successor_sourcerc mdr_e_successor_sourcerc mdr_f_successor_sourcerc. ((mdr_a_successor_sourcerc = ((S q) + (pb)) * S ((S q) + (pb)) + ((pb) + (pb))) /\ ((mdr_b_successor_sourcerc = ((pc) + (nb)) * S ((pc) + (nb)) + ((nb) + (nb))) /\ ((mdr_c_successor_sourcerc = ((mdr_a_successor_sourcerc) + (mdr_b_successor_sourcerc)) * S ((mdr_a_successor_sourcerc) + (mdr_b_successor_sourcerc)) + ((mdr_b_successor_sourcerc) + (mdr_b_successor_sourcerc))) /\ ((mdr_e_successor_sourcerc = ((p) + (n)) * S ((p) + (n)) + ((n) + (n))) /\ ((mdr_f_successor_sourcerc = ((nc) + (mdr_e_successor_sourcerc)) * S ((nc) + (mdr_e_successor_sourcerc)) + ((mdr_e_successor_sourcerc) + (mdr_e_successor_sourcerc))) /\ ((mdr_z_successor_sourcer) = ((mdr_c_successor_sourcerc) + (mdr_f_successor_sourcerc)) * S ((mdr_c_successor_sourcerc) + (mdr_f_successor_sourcerc)) + ((mdr_f_successor_sourcerc) + (mdr_f_successor_sourcerc))))))))) /\ (((exists ff_h_mdr_successor_sourcerb. ff_h_mdr_successor_sourcerb + S (mdr_z_successor_sourcer) = S ((S (mdr_i_successor_source)) * mdr_c_successor_source)) /\ exists ff_q_mdr_successor_sourcerb. mdr_b_successor_source = ff_q_mdr_successor_sourcerb * S ((S (mdr_i_successor_source)) * mdr_c_successor_source) + (mdr_z_successor_sourcer)))))))) -> exists eb ec fb fc. ((forall mdr_j_cofactor_result. (exists mdr_gap_cofactor_resultj. mdr_gap_cofactor_resultj + S (mdr_j_cofactor_result) = (S (q))) -> exists mdr_up_cofactor_result mdr_us_cofactor_result mdr_un_cofactor_result mdr_ut_cofactor_result mdr_p_cofactor_result mdr_n_cofactor_result. ((((forall ff_index_mdm_prefix_mdr_cofactor_resultm_positive. (exists ff_gap_mdm_lt_mdr_cofactor_resultm_positive_index_bound. ff_gap_mdm_lt_mdr_cofactor_resultm_positive_index_bound + S (ff_index_mdm_prefix_mdr_cofactor_resultm_positive) = ((q) * (q))) -> exists ff_row_mdm_prefix_mdr_cofactor_resultm_positive ff_column_mdm_prefix_mdr_cofactor_resultm_positive ff_value_mdm_prefix_mdr_cofactor_resultm_positive. (ff_index_mdm_prefix_mdr_cofactor_resultm_positive = (q) * ff_row_mdm_prefix_mdr_cofactor_resultm_positive + ff_column_mdm_prefix_mdr_cofactor_resultm_positive /\ ((exists ff_gap_mdm_lt_mdr_cofactor_resultm_positive_column_bound. ff_gap_mdm_lt_mdr_cofactor_resultm_positive_column_bound + S (ff_column_mdm_prefix_mdr_cofactor_resultm_positive) = (q)) /\ ((exists ff_row_mdm_cell_mdr_cofactor_resultm_positive_cell ff_column_mdm_cell_mdr_cofactor_resultm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_cofactor_resultm_positive_cell_row_before. ff_gap_mdm_lt_mdr_cofactor_resultm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_cofactor_resultm_positive) = (0)) /\ ff_row_mdm_cell_mdr_cofactor_resultm_positive_cell = ff_row_mdm_prefix_mdr_cofactor_resultm_positive) \/ ((exists ff_gap_mdm_le_mdr_cofactor_resultm_positive_cell_row_after. ff_gap_mdm_le_mdr_cofactor_resultm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_cofactor_resultm_positive)) /\ ff_row_mdm_cell_mdr_cofactor_resultm_positive_cell = S ff_row_mdm_prefix_mdr_cofactor_resultm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_cofactor_resultm_positive_cell_column_before. ff_gap_mdm_lt_mdr_cofactor_resultm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_cofactor_resultm_positive) = (mdr_j_cofactor_result)) /\ ff_column_mdm_cell_mdr_cofactor_resultm_positive_cell = ff_column_mdm_prefix_mdr_cofactor_resultm_positive) \/ ((exists ff_gap_mdm_le_mdr_cofactor_resultm_positive_cell_column_after. ff_gap_mdm_le_mdr_cofactor_resultm_positive_cell_column_after + (mdr_j_cofactor_result) = (ff_column_mdm_prefix_mdr_cofactor_resultm_positive)) /\ ff_column_mdm_cell_mdr_cofactor_resultm_positive_cell = S ff_column_mdm_prefix_mdr_cofactor_resultm_positive))) /\ (((exists ff_h_mdm_mdr_cofactor_resultm_positive_cell_source. ff_h_mdm_mdr_cofactor_resultm_positive_cell_source + S (ff_value_mdm_prefix_mdr_cofactor_resultm_positive) = S ((S ((ff_row_mdm_cell_mdr_cofactor_resultm_positive_cell) * (S (q)) + (ff_column_mdm_cell_mdr_cofactor_resultm_positive_cell))) * pc)) /\ exists ff_q_mdm_mdr_cofactor_resultm_positive_cell_source. pb = ff_q_mdm_mdr_cofactor_resultm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_cofactor_resultm_positive_cell) * (S (q)) + (ff_column_mdm_cell_mdr_cofactor_resultm_positive_cell))) * pc) + (ff_value_mdm_prefix_mdr_cofactor_resultm_positive)))))) /\ (((exists ff_h_mdm_mdr_cofactor_resultm_positive_target. ff_h_mdm_mdr_cofactor_resultm_positive_target + S (ff_value_mdm_prefix_mdr_cofactor_resultm_positive) = S ((S (ff_index_mdm_prefix_mdr_cofactor_resultm_positive)) * mdr_us_cofactor_result)) /\ exists ff_q_mdm_mdr_cofactor_resultm_positive_target. mdr_up_cofactor_result = ff_q_mdm_mdr_cofactor_resultm_positive_target * S ((S (ff_index_mdm_prefix_mdr_cofactor_resultm_positive)) * mdr_us_cofactor_result) + (ff_value_mdm_prefix_mdr_cofactor_resultm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_cofactor_resultm_negative. (exists ff_gap_mdm_lt_mdr_cofactor_resultm_negative_index_bound. ff_gap_mdm_lt_mdr_cofactor_resultm_negative_index_bound + S (ff_index_mdm_prefix_mdr_cofactor_resultm_negative) = ((q) * (q))) -> exists ff_row_mdm_prefix_mdr_cofactor_resultm_negative ff_column_mdm_prefix_mdr_cofactor_resultm_negative ff_value_mdm_prefix_mdr_cofactor_resultm_negative. (ff_index_mdm_prefix_mdr_cofactor_resultm_negative = (q) * ff_row_mdm_prefix_mdr_cofactor_resultm_negative + ff_column_mdm_prefix_mdr_cofactor_resultm_negative /\ ((exists ff_gap_mdm_lt_mdr_cofactor_resultm_negative_column_bound. ff_gap_mdm_lt_mdr_cofactor_resultm_negative_column_bound + S (ff_column_mdm_prefix_mdr_cofactor_resultm_negative) = (q)) /\ ((exists ff_row_mdm_cell_mdr_cofactor_resultm_negative_cell ff_column_mdm_cell_mdr_cofactor_resultm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_cofactor_resultm_negative_cell_row_before. ff_gap_mdm_lt_mdr_cofactor_resultm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_cofactor_resultm_negative) = (0)) /\ ff_row_mdm_cell_mdr_cofactor_resultm_negative_cell = ff_row_mdm_prefix_mdr_cofactor_resultm_negative) \/ ((exists ff_gap_mdm_le_mdr_cofactor_resultm_negative_cell_row_after. ff_gap_mdm_le_mdr_cofactor_resultm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_cofactor_resultm_negative)) /\ ff_row_mdm_cell_mdr_cofactor_resultm_negative_cell = S ff_row_mdm_prefix_mdr_cofactor_resultm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_cofactor_resultm_negative_cell_column_before. ff_gap_mdm_lt_mdr_cofactor_resultm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_cofactor_resultm_negative) = (mdr_j_cofactor_result)) /\ ff_column_mdm_cell_mdr_cofactor_resultm_negative_cell = ff_column_mdm_prefix_mdr_cofactor_resultm_negative) \/ ((exists ff_gap_mdm_le_mdr_cofactor_resultm_negative_cell_column_after. ff_gap_mdm_le_mdr_cofactor_resultm_negative_cell_column_after + (mdr_j_cofactor_result) = (ff_column_mdm_prefix_mdr_cofactor_resultm_negative)) /\ ff_column_mdm_cell_mdr_cofactor_resultm_negative_cell = S ff_column_mdm_prefix_mdr_cofactor_resultm_negative))) /\ (((exists ff_h_mdm_mdr_cofactor_resultm_negative_cell_source. ff_h_mdm_mdr_cofactor_resultm_negative_cell_source + S (ff_value_mdm_prefix_mdr_cofactor_resultm_negative) = S ((S ((ff_row_mdm_cell_mdr_cofactor_resultm_negative_cell) * (S (q)) + (ff_column_mdm_cell_mdr_cofactor_resultm_negative_cell))) * nc)) /\ exists ff_q_mdm_mdr_cofactor_resultm_negative_cell_source. nb = ff_q_mdm_mdr_cofactor_resultm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_cofactor_resultm_negative_cell) * (S (q)) + (ff_column_mdm_cell_mdr_cofactor_resultm_negative_cell))) * nc) + (ff_value_mdm_prefix_mdr_cofactor_resultm_negative)))))) /\ (((exists ff_h_mdm_mdr_cofactor_resultm_negative_target. ff_h_mdm_mdr_cofactor_resultm_negative_target + S (ff_value_mdm_prefix_mdr_cofactor_resultm_negative) = S ((S (ff_index_mdm_prefix_mdr_cofactor_resultm_negative)) * mdr_ut_cofactor_result)) /\ exists ff_q_mdm_mdr_cofactor_resultm_negative_target. mdr_un_cofactor_result = ff_q_mdm_mdr_cofactor_resultm_negative_target * S ((S (ff_index_mdm_prefix_mdr_cofactor_resultm_negative)) * mdr_ut_cofactor_result) + (ff_value_mdm_prefix_mdr_cofactor_resultm_negative))))))))) /\ ((exists mdr_b_cofactor_resultd mdr_c_cofactor_resultd mdr_l_cofactor_resultd mdr_i_cofactor_resultd. ((forall mdr_i_cofactor_resultdh. (exists mdr_gap_cofactor_resultdhi. mdr_gap_cofactor_resultdhi + S (mdr_i_cofactor_resultdh) = (mdr_l_cofactor_resultd)) -> exists mdr_d_cofactor_resultdh mdr_pb_cofactor_resultdh mdr_pc_cofactor_resultdh mdr_nb_cofactor_resultdh mdr_nc_cofactor_resultdh mdr_p_cofactor_resultdh mdr_n_cofactor_resultdh. ((exists mdr_z_cofactor_resultdhr. ((exists mdr_a_cofactor_resultdhrc mdr_b_cofactor_resultdhrc mdr_c_cofactor_resultdhrc mdr_e_cofactor_resultdhrc mdr_f_cofactor_resultdhrc. ((mdr_a_cofactor_resultdhrc = ((mdr_d_cofactor_resultdh) + (mdr_pb_cofactor_resultdh)) * S ((mdr_d_cofactor_resultdh) + (mdr_pb_cofactor_resultdh)) + ((mdr_pb_cofactor_resultdh) + (mdr_pb_cofactor_resultdh))) /\ ((mdr_b_cofactor_resultdhrc = ((mdr_pc_cofactor_resultdh) + (mdr_nb_cofactor_resultdh)) * S ((mdr_pc_cofactor_resultdh) + (mdr_nb_cofactor_resultdh)) + ((mdr_nb_cofactor_resultdh) + (mdr_nb_cofactor_resultdh))) /\ ((mdr_c_cofactor_resultdhrc = ((mdr_a_cofactor_resultdhrc) + (mdr_b_cofactor_resultdhrc)) * S ((mdr_a_cofactor_resultdhrc) + (mdr_b_cofactor_resultdhrc)) + ((mdr_b_cofactor_resultdhrc) + (mdr_b_cofactor_resultdhrc))) /\ ((mdr_e_cofactor_resultdhrc = ((mdr_p_cofactor_resultdh) + (mdr_n_cofactor_resultdh)) * S ((mdr_p_cofactor_resultdh) + (mdr_n_cofactor_resultdh)) + ((mdr_n_cofactor_resultdh) + (mdr_n_cofactor_resultdh))) /\ ((mdr_f_cofactor_resultdhrc = ((mdr_nc_cofactor_resultdh) + (mdr_e_cofactor_resultdhrc)) * S ((mdr_nc_cofactor_resultdh) + (mdr_e_cofactor_resultdhrc)) + ((mdr_e_cofactor_resultdhrc) + (mdr_e_cofactor_resultdhrc))) /\ ((mdr_z_cofactor_resultdhr) = ((mdr_c_cofactor_resultdhrc) + (mdr_f_cofactor_resultdhrc)) * S ((mdr_c_cofactor_resultdhrc) + (mdr_f_cofactor_resultdhrc)) + ((mdr_f_cofactor_resultdhrc) + (mdr_f_cofactor_resultdhrc))))))))) /\ (((exists ff_h_mdr_cofactor_resultdhrb. ff_h_mdr_cofactor_resultdhrb + S (mdr_z_cofactor_resultdhr) = S ((S (mdr_i_cofactor_resultdh)) * mdr_c_cofactor_resultd)) /\ exists ff_q_mdr_cofactor_resultdhrb. mdr_b_cofactor_resultd = ff_q_mdr_cofactor_resultdhrb * S ((S (mdr_i_cofactor_resultdh)) * mdr_c_cofactor_resultd) + (mdr_z_cofactor_resultdhr))))) /\ (((((mdr_d_cofactor_resultdh) = 0) /\ (((mdr_p_cofactor_resultdh) = 1) /\ ((mdr_n_cofactor_resultdh) = 0))) \/ exists mdr_q_cofactor_resultdhs mdr_eb_cofactor_resultdhs mdr_ec_cofactor_resultdhs mdr_fb_cofactor_resultdhs mdr_fc_cofactor_resultdhs. (((mdr_d_cofactor_resultdh) = S (mdr_q_cofactor_resultdhs)) /\ ((forall mdr_j_cofactor_resultdhsc. (exists mdr_gap_cofactor_resultdhscj. mdr_gap_cofactor_resultdhscj + S (mdr_j_cofactor_resultdhsc) = (S (mdr_q_cofactor_resultdhs))) -> exists mdr_i_cofactor_resultdhsc mdr_up_cofactor_resultdhsc mdr_us_cofactor_resultdhsc mdr_un_cofactor_resultdhsc mdr_ut_cofactor_resultdhsc mdr_p_cofactor_resultdhsc mdr_n_cofactor_resultdhsc. ((exists mdr_gap_cofactor_resultdhsci. mdr_gap_cofactor_resultdhsci + S (mdr_i_cofactor_resultdhsc) = (mdr_i_cofactor_resultdh)) /\ ((exists mdr_z_cofactor_resultdhscr. ((exists mdr_a_cofactor_resultdhscrc mdr_b_cofactor_resultdhscrc mdr_c_cofactor_resultdhscrc mdr_e_cofactor_resultdhscrc mdr_f_cofactor_resultdhscrc. ((mdr_a_cofactor_resultdhscrc = ((mdr_q_cofactor_resultdhs) + (mdr_up_cofactor_resultdhsc)) * S ((mdr_q_cofactor_resultdhs) + (mdr_up_cofactor_resultdhsc)) + ((mdr_up_cofactor_resultdhsc) + (mdr_up_cofactor_resultdhsc))) /\ ((mdr_b_cofactor_resultdhscrc = ((mdr_us_cofactor_resultdhsc) + (mdr_un_cofactor_resultdhsc)) * S ((mdr_us_cofactor_resultdhsc) + (mdr_un_cofactor_resultdhsc)) + ((mdr_un_cofactor_resultdhsc) + (mdr_un_cofactor_resultdhsc))) /\ ((mdr_c_cofactor_resultdhscrc = ((mdr_a_cofactor_resultdhscrc) + (mdr_b_cofactor_resultdhscrc)) * S ((mdr_a_cofactor_resultdhscrc) + (mdr_b_cofactor_resultdhscrc)) + ((mdr_b_cofactor_resultdhscrc) + (mdr_b_cofactor_resultdhscrc))) /\ ((mdr_e_cofactor_resultdhscrc = ((mdr_p_cofactor_resultdhsc) + (mdr_n_cofactor_resultdhsc)) * S ((mdr_p_cofactor_resultdhsc) + (mdr_n_cofactor_resultdhsc)) + ((mdr_n_cofactor_resultdhsc) + (mdr_n_cofactor_resultdhsc))) /\ ((mdr_f_cofactor_resultdhscrc = ((mdr_ut_cofactor_resultdhsc) + (mdr_e_cofactor_resultdhscrc)) * S ((mdr_ut_cofactor_resultdhsc) + (mdr_e_cofactor_resultdhscrc)) + ((mdr_e_cofactor_resultdhscrc) + (mdr_e_cofactor_resultdhscrc))) /\ ((mdr_z_cofactor_resultdhscr) = ((mdr_c_cofactor_resultdhscrc) + (mdr_f_cofactor_resultdhscrc)) * S ((mdr_c_cofactor_resultdhscrc) + (mdr_f_cofactor_resultdhscrc)) + ((mdr_f_cofactor_resultdhscrc) + (mdr_f_cofactor_resultdhscrc))))))))) /\ (((exists ff_h_mdr_cofactor_resultdhscrb. ff_h_mdr_cofactor_resultdhscrb + S (mdr_z_cofactor_resultdhscr) = S ((S (mdr_i_cofactor_resultdhsc)) * mdr_c_cofactor_resultd)) /\ exists ff_q_mdr_cofactor_resultdhscrb. mdr_b_cofactor_resultd = ff_q_mdr_cofactor_resultdhscrb * S ((S (mdr_i_cofactor_resultdhsc)) * mdr_c_cofactor_resultd) + (mdr_z_cofactor_resultdhscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_cofactor_resultdhscm_positive. (exists ff_gap_mdm_lt_mdr_cofactor_resultdhscm_positive_index_bound. ff_gap_mdm_lt_mdr_cofactor_resultdhscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_cofactor_resultdhscm_positive) = ((mdr_q_cofactor_resultdhs) * (mdr_q_cofactor_resultdhs))) -> exists ff_row_mdm_prefix_mdr_cofactor_resultdhscm_positive ff_column_mdm_prefix_mdr_cofactor_resultdhscm_positive ff_value_mdm_prefix_mdr_cofactor_resultdhscm_positive. (ff_index_mdm_prefix_mdr_cofactor_resultdhscm_positive = (mdr_q_cofactor_resultdhs) * ff_row_mdm_prefix_mdr_cofactor_resultdhscm_positive + ff_column_mdm_prefix_mdr_cofactor_resultdhscm_positive /\ ((exists ff_gap_mdm_lt_mdr_cofactor_resultdhscm_positive_column_bound. ff_gap_mdm_lt_mdr_cofactor_resultdhscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_cofactor_resultdhscm_positive) = (mdr_q_cofactor_resultdhs)) /\ ((exists ff_row_mdm_cell_mdr_cofactor_resultdhscm_positive_cell ff_column_mdm_cell_mdr_cofactor_resultdhscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_cofactor_resultdhscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_cofactor_resultdhscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_cofactor_resultdhscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_cofactor_resultdhscm_positive_cell = ff_row_mdm_prefix_mdr_cofactor_resultdhscm_positive) \/ ((exists ff_gap_mdm_le_mdr_cofactor_resultdhscm_positive_cell_row_after. ff_gap_mdm_le_mdr_cofactor_resultdhscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_cofactor_resultdhscm_positive)) /\ ff_row_mdm_cell_mdr_cofactor_resultdhscm_positive_cell = S ff_row_mdm_prefix_mdr_cofactor_resultdhscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_cofactor_resultdhscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_cofactor_resultdhscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_cofactor_resultdhscm_positive) = (mdr_j_cofactor_resultdhsc)) /\ ff_column_mdm_cell_mdr_cofactor_resultdhscm_positive_cell = ff_column_mdm_prefix_mdr_cofactor_resultdhscm_positive) \/ ((exists ff_gap_mdm_le_mdr_cofactor_resultdhscm_positive_cell_column_after. ff_gap_mdm_le_mdr_cofactor_resultdhscm_positive_cell_column_after + (mdr_j_cofactor_resultdhsc) = (ff_column_mdm_prefix_mdr_cofactor_resultdhscm_positive)) /\ ff_column_mdm_cell_mdr_cofactor_resultdhscm_positive_cell = S ff_column_mdm_prefix_mdr_cofactor_resultdhscm_positive))) /\ (((exists ff_h_mdm_mdr_cofactor_resultdhscm_positive_cell_source. ff_h_mdm_mdr_cofactor_resultdhscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_cofactor_resultdhscm_positive) = S ((S ((ff_row_mdm_cell_mdr_cofactor_resultdhscm_positive_cell) * (S (mdr_q_cofactor_resultdhs)) + (ff_column_mdm_cell_mdr_cofactor_resultdhscm_positive_cell))) * mdr_pc_cofactor_resultdh)) /\ exists ff_q_mdm_mdr_cofactor_resultdhscm_positive_cell_source. mdr_pb_cofactor_resultdh = ff_q_mdm_mdr_cofactor_resultdhscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_cofactor_resultdhscm_positive_cell) * (S (mdr_q_cofactor_resultdhs)) + (ff_column_mdm_cell_mdr_cofactor_resultdhscm_positive_cell))) * mdr_pc_cofactor_resultdh) + (ff_value_mdm_prefix_mdr_cofactor_resultdhscm_positive)))))) /\ (((exists ff_h_mdm_mdr_cofactor_resultdhscm_positive_target. ff_h_mdm_mdr_cofactor_resultdhscm_positive_target + S (ff_value_mdm_prefix_mdr_cofactor_resultdhscm_positive) = S ((S (ff_index_mdm_prefix_mdr_cofactor_resultdhscm_positive)) * mdr_us_cofactor_resultdhsc)) /\ exists ff_q_mdm_mdr_cofactor_resultdhscm_positive_target. mdr_up_cofactor_resultdhsc = ff_q_mdm_mdr_cofactor_resultdhscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_cofactor_resultdhscm_positive)) * mdr_us_cofactor_resultdhsc) + (ff_value_mdm_prefix_mdr_cofactor_resultdhscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_cofactor_resultdhscm_negative. (exists ff_gap_mdm_lt_mdr_cofactor_resultdhscm_negative_index_bound. ff_gap_mdm_lt_mdr_cofactor_resultdhscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_cofactor_resultdhscm_negative) = ((mdr_q_cofactor_resultdhs) * (mdr_q_cofactor_resultdhs))) -> exists ff_row_mdm_prefix_mdr_cofactor_resultdhscm_negative ff_column_mdm_prefix_mdr_cofactor_resultdhscm_negative ff_value_mdm_prefix_mdr_cofactor_resultdhscm_negative. (ff_index_mdm_prefix_mdr_cofactor_resultdhscm_negative = (mdr_q_cofactor_resultdhs) * ff_row_mdm_prefix_mdr_cofactor_resultdhscm_negative + ff_column_mdm_prefix_mdr_cofactor_resultdhscm_negative /\ ((exists ff_gap_mdm_lt_mdr_cofactor_resultdhscm_negative_column_bound. ff_gap_mdm_lt_mdr_cofactor_resultdhscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_cofactor_resultdhscm_negative) = (mdr_q_cofactor_resultdhs)) /\ ((exists ff_row_mdm_cell_mdr_cofactor_resultdhscm_negative_cell ff_column_mdm_cell_mdr_cofactor_resultdhscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_cofactor_resultdhscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_cofactor_resultdhscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_cofactor_resultdhscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_cofactor_resultdhscm_negative_cell = ff_row_mdm_prefix_mdr_cofactor_resultdhscm_negative) \/ ((exists ff_gap_mdm_le_mdr_cofactor_resultdhscm_negative_cell_row_after. ff_gap_mdm_le_mdr_cofactor_resultdhscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_cofactor_resultdhscm_negative)) /\ ff_row_mdm_cell_mdr_cofactor_resultdhscm_negative_cell = S ff_row_mdm_prefix_mdr_cofactor_resultdhscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_cofactor_resultdhscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_cofactor_resultdhscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_cofactor_resultdhscm_negative) = (mdr_j_cofactor_resultdhsc)) /\ ff_column_mdm_cell_mdr_cofactor_resultdhscm_negative_cell = ff_column_mdm_prefix_mdr_cofactor_resultdhscm_negative) \/ ((exists ff_gap_mdm_le_mdr_cofactor_resultdhscm_negative_cell_column_after. ff_gap_mdm_le_mdr_cofactor_resultdhscm_negative_cell_column_after + (mdr_j_cofactor_resultdhsc) = (ff_column_mdm_prefix_mdr_cofactor_resultdhscm_negative)) /\ ff_column_mdm_cell_mdr_cofactor_resultdhscm_negative_cell = S ff_column_mdm_prefix_mdr_cofactor_resultdhscm_negative))) /\ (((exists ff_h_mdm_mdr_cofactor_resultdhscm_negative_cell_source. ff_h_mdm_mdr_cofactor_resultdhscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_cofactor_resultdhscm_negative) = S ((S ((ff_row_mdm_cell_mdr_cofactor_resultdhscm_negative_cell) * (S (mdr_q_cofactor_resultdhs)) + (ff_column_mdm_cell_mdr_cofactor_resultdhscm_negative_cell))) * mdr_nc_cofactor_resultdh)) /\ exists ff_q_mdm_mdr_cofactor_resultdhscm_negative_cell_source. mdr_nb_cofactor_resultdh = ff_q_mdm_mdr_cofactor_resultdhscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_cofactor_resultdhscm_negative_cell) * (S (mdr_q_cofactor_resultdhs)) + (ff_column_mdm_cell_mdr_cofactor_resultdhscm_negative_cell))) * mdr_nc_cofactor_resultdh) + (ff_value_mdm_prefix_mdr_cofactor_resultdhscm_negative)))))) /\ (((exists ff_h_mdm_mdr_cofactor_resultdhscm_negative_target. ff_h_mdm_mdr_cofactor_resultdhscm_negative_target + S (ff_value_mdm_prefix_mdr_cofactor_resultdhscm_negative) = S ((S (ff_index_mdm_prefix_mdr_cofactor_resultdhscm_negative)) * mdr_ut_cofactor_resultdhsc)) /\ exists ff_q_mdm_mdr_cofactor_resultdhscm_negative_target. mdr_un_cofactor_resultdhsc = ff_q_mdm_mdr_cofactor_resultdhscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_cofactor_resultdhscm_negative)) * mdr_ut_cofactor_resultdhsc) + (ff_value_mdm_prefix_mdr_cofactor_resultdhscm_negative))))))))) /\ ((((exists ff_h_mdr_cofactor_resultdhscp. ff_h_mdr_cofactor_resultdhscp + S (mdr_p_cofactor_resultdhsc) = S ((S (mdr_j_cofactor_resultdhsc)) * mdr_ec_cofactor_resultdhs)) /\ exists ff_q_mdr_cofactor_resultdhscp. mdr_eb_cofactor_resultdhs = ff_q_mdr_cofactor_resultdhscp * S ((S (mdr_j_cofactor_resultdhsc)) * mdr_ec_cofactor_resultdhs) + (mdr_p_cofactor_resultdhsc))) /\ (((exists ff_h_mdr_cofactor_resultdhscn. ff_h_mdr_cofactor_resultdhscn + S (mdr_n_cofactor_resultdhsc) = S ((S (mdr_j_cofactor_resultdhsc)) * mdr_fc_cofactor_resultdhs)) /\ exists ff_q_mdr_cofactor_resultdhscn. mdr_fb_cofactor_resultdhs = ff_q_mdr_cofactor_resultdhscn * S ((S (mdr_j_cofactor_resultdhsc)) * mdr_fc_cofactor_resultdhs) + (mdr_n_cofactor_resultdhsc)))))))) /\ (exists ff_ub_mce_fold_mdr_cofactor_resultdhsf ff_uc_mce_fold_mdr_cofactor_resultdhsf ff_vb_mce_fold_mdr_cofactor_resultdhsf ff_vc_mce_fold_mdr_cofactor_resultdhsf. ((forall ff_index_mce_alternating_mdr_cofactor_resultdhsf_prefix. (exists ff_gap_mce_mdr_cofactor_resultdhsf_prefix_index. ff_gap_mce_mdr_cofactor_resultdhsf_prefix_index + S (ff_index_mce_alternating_mdr_cofactor_resultdhsf_prefix) = (S (mdr_q_cofactor_resultdhs))) -> exists ff_ap_mce_alternating_mdr_cofactor_resultdhsf_prefix ff_an_mce_alternating_mdr_cofactor_resultdhsf_prefix ff_bp_mce_alternating_mdr_cofactor_resultdhsf_prefix ff_bn_mce_alternating_mdr_cofactor_resultdhsf_prefix ff_p_mce_alternating_mdr_cofactor_resultdhsf_prefix ff_n_mce_alternating_mdr_cofactor_resultdhsf_prefix. ((((exists ff_h_mce_mdr_cofactor_resultdhsf_prefix_ap. ff_h_mce_mdr_cofactor_resultdhsf_prefix_ap + S (ff_ap_mce_alternating_mdr_cofactor_resultdhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_cofactor_resultdhsf_prefix)) * mdr_pc_cofactor_resultdh)) /\ exists ff_q_mce_mdr_cofactor_resultdhsf_prefix_ap. mdr_pb_cofactor_resultdh = ff_q_mce_mdr_cofactor_resultdhsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_cofactor_resultdhsf_prefix)) * mdr_pc_cofactor_resultdh) + (ff_ap_mce_alternating_mdr_cofactor_resultdhsf_prefix))) /\ ((((exists ff_h_mce_mdr_cofactor_resultdhsf_prefix_an. ff_h_mce_mdr_cofactor_resultdhsf_prefix_an + S (ff_an_mce_alternating_mdr_cofactor_resultdhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_cofactor_resultdhsf_prefix)) * mdr_nc_cofactor_resultdh)) /\ exists ff_q_mce_mdr_cofactor_resultdhsf_prefix_an. mdr_nb_cofactor_resultdh = ff_q_mce_mdr_cofactor_resultdhsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_cofactor_resultdhsf_prefix)) * mdr_nc_cofactor_resultdh) + (ff_an_mce_alternating_mdr_cofactor_resultdhsf_prefix))) /\ ((((exists ff_h_mce_mdr_cofactor_resultdhsf_prefix_bp. ff_h_mce_mdr_cofactor_resultdhsf_prefix_bp + S (ff_bp_mce_alternating_mdr_cofactor_resultdhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_cofactor_resultdhsf_prefix)) * mdr_ec_cofactor_resultdhs)) /\ exists ff_q_mce_mdr_cofactor_resultdhsf_prefix_bp. mdr_eb_cofactor_resultdhs = ff_q_mce_mdr_cofactor_resultdhsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_cofactor_resultdhsf_prefix)) * mdr_ec_cofactor_resultdhs) + (ff_bp_mce_alternating_mdr_cofactor_resultdhsf_prefix))) /\ ((((exists ff_h_mce_mdr_cofactor_resultdhsf_prefix_bn. ff_h_mce_mdr_cofactor_resultdhsf_prefix_bn + S (ff_bn_mce_alternating_mdr_cofactor_resultdhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_cofactor_resultdhsf_prefix)) * mdr_fc_cofactor_resultdhs)) /\ exists ff_q_mce_mdr_cofactor_resultdhsf_prefix_bn. mdr_fb_cofactor_resultdhs = ff_q_mce_mdr_cofactor_resultdhsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_cofactor_resultdhsf_prefix)) * mdr_fc_cofactor_resultdhs) + (ff_bn_mce_alternating_mdr_cofactor_resultdhsf_prefix))) /\ ((((exists ff_h_mce_mdr_cofactor_resultdhsf_prefix_positive. ff_h_mce_mdr_cofactor_resultdhsf_prefix_positive + S (ff_p_mce_alternating_mdr_cofactor_resultdhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_cofactor_resultdhsf_prefix)) * ff_uc_mce_fold_mdr_cofactor_resultdhsf)) /\ exists ff_q_mce_mdr_cofactor_resultdhsf_prefix_positive. ff_ub_mce_fold_mdr_cofactor_resultdhsf = ff_q_mce_mdr_cofactor_resultdhsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_cofactor_resultdhsf_prefix)) * ff_uc_mce_fold_mdr_cofactor_resultdhsf) + (ff_p_mce_alternating_mdr_cofactor_resultdhsf_prefix))) /\ ((((exists ff_h_mce_mdr_cofactor_resultdhsf_prefix_negative. ff_h_mce_mdr_cofactor_resultdhsf_prefix_negative + S (ff_n_mce_alternating_mdr_cofactor_resultdhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_cofactor_resultdhsf_prefix)) * ff_vc_mce_fold_mdr_cofactor_resultdhsf)) /\ exists ff_q_mce_mdr_cofactor_resultdhsf_prefix_negative. ff_vb_mce_fold_mdr_cofactor_resultdhsf = ff_q_mce_mdr_cofactor_resultdhsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_cofactor_resultdhsf_prefix)) * ff_vc_mce_fold_mdr_cofactor_resultdhsf) + (ff_n_mce_alternating_mdr_cofactor_resultdhsf_prefix))) /\ (((exists ff_even_mce_term_mdr_cofactor_resultdhsf_prefix_term. ff_index_mce_alternating_mdr_cofactor_resultdhsf_prefix = 2 * ff_even_mce_term_mdr_cofactor_resultdhsf_prefix_term) /\ (ff_p_mce_alternating_mdr_cofactor_resultdhsf_prefix = (ff_ap_mce_alternating_mdr_cofactor_resultdhsf_prefix) * (ff_bp_mce_alternating_mdr_cofactor_resultdhsf_prefix) + (ff_an_mce_alternating_mdr_cofactor_resultdhsf_prefix) * (ff_bn_mce_alternating_mdr_cofactor_resultdhsf_prefix) /\ ff_n_mce_alternating_mdr_cofactor_resultdhsf_prefix = (ff_ap_mce_alternating_mdr_cofactor_resultdhsf_prefix) * (ff_bn_mce_alternating_mdr_cofactor_resultdhsf_prefix) + (ff_an_mce_alternating_mdr_cofactor_resultdhsf_prefix) * (ff_bp_mce_alternating_mdr_cofactor_resultdhsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_cofactor_resultdhsf_prefix_term. ff_index_mce_alternating_mdr_cofactor_resultdhsf_prefix = 2 * ff_odd_mce_term_mdr_cofactor_resultdhsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_cofactor_resultdhsf_prefix = (ff_ap_mce_alternating_mdr_cofactor_resultdhsf_prefix) * (ff_bn_mce_alternating_mdr_cofactor_resultdhsf_prefix) + (ff_an_mce_alternating_mdr_cofactor_resultdhsf_prefix) * (ff_bp_mce_alternating_mdr_cofactor_resultdhsf_prefix) /\ ff_n_mce_alternating_mdr_cofactor_resultdhsf_prefix = (ff_ap_mce_alternating_mdr_cofactor_resultdhsf_prefix) * (ff_bp_mce_alternating_mdr_cofactor_resultdhsf_prefix) + (ff_an_mce_alternating_mdr_cofactor_resultdhsf_prefix) * (ff_bn_mce_alternating_mdr_cofactor_resultdhsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_cofactor_resultdhsf_positive ff_v_mce_mdr_cofactor_resultdhsf_positive. ((((exists ff_h_mce_mdr_cofactor_resultdhsf_positive_start. ff_h_mce_mdr_cofactor_resultdhsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_cofactor_resultdhsf_positive)) /\ exists ff_q_mce_mdr_cofactor_resultdhsf_positive_start. ff_u_mce_mdr_cofactor_resultdhsf_positive = ff_q_mce_mdr_cofactor_resultdhsf_positive_start * S ((S (0)) * ff_v_mce_mdr_cofactor_resultdhsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_cofactor_resultdhsf_positive_terminal. ff_h_mce_mdr_cofactor_resultdhsf_positive_terminal + S (mdr_p_cofactor_resultdh) = S ((S ((S (mdr_q_cofactor_resultdhs)))) * ff_v_mce_mdr_cofactor_resultdhsf_positive)) /\ exists ff_q_mce_mdr_cofactor_resultdhsf_positive_terminal. ff_u_mce_mdr_cofactor_resultdhsf_positive = ff_q_mce_mdr_cofactor_resultdhsf_positive_terminal * S ((S ((S (mdr_q_cofactor_resultdhs)))) * ff_v_mce_mdr_cofactor_resultdhsf_positive) + (mdr_p_cofactor_resultdh))) /\ forall ff_i_mce_mdr_cofactor_resultdhsf_positive. (exists ff_lt_mce_mdr_cofactor_resultdhsf_positive_bound. ff_lt_mce_mdr_cofactor_resultdhsf_positive_bound + S ff_i_mce_mdr_cofactor_resultdhsf_positive = (S (mdr_q_cofactor_resultdhs))) -> exists ff_a_mce_mdr_cofactor_resultdhsf_positive ff_r_mce_mdr_cofactor_resultdhsf_positive ff_s_mce_mdr_cofactor_resultdhsf_positive. ((((exists ff_h_mce_mdr_cofactor_resultdhsf_positive_summand. ff_h_mce_mdr_cofactor_resultdhsf_positive_summand + S (ff_a_mce_mdr_cofactor_resultdhsf_positive) = S ((S (ff_i_mce_mdr_cofactor_resultdhsf_positive)) * ff_uc_mce_fold_mdr_cofactor_resultdhsf)) /\ exists ff_q_mce_mdr_cofactor_resultdhsf_positive_summand. ff_ub_mce_fold_mdr_cofactor_resultdhsf = ff_q_mce_mdr_cofactor_resultdhsf_positive_summand * S ((S (ff_i_mce_mdr_cofactor_resultdhsf_positive)) * ff_uc_mce_fold_mdr_cofactor_resultdhsf) + (ff_a_mce_mdr_cofactor_resultdhsf_positive))) /\ ((((exists ff_h_mce_mdr_cofactor_resultdhsf_positive_partial. ff_h_mce_mdr_cofactor_resultdhsf_positive_partial + S (ff_r_mce_mdr_cofactor_resultdhsf_positive) = S ((S (ff_i_mce_mdr_cofactor_resultdhsf_positive)) * ff_v_mce_mdr_cofactor_resultdhsf_positive)) /\ exists ff_q_mce_mdr_cofactor_resultdhsf_positive_partial. ff_u_mce_mdr_cofactor_resultdhsf_positive = ff_q_mce_mdr_cofactor_resultdhsf_positive_partial * S ((S (ff_i_mce_mdr_cofactor_resultdhsf_positive)) * ff_v_mce_mdr_cofactor_resultdhsf_positive) + (ff_r_mce_mdr_cofactor_resultdhsf_positive))) /\ ((((exists ff_h_mce_mdr_cofactor_resultdhsf_positive_successor. ff_h_mce_mdr_cofactor_resultdhsf_positive_successor + S (ff_s_mce_mdr_cofactor_resultdhsf_positive) = S ((S (S ff_i_mce_mdr_cofactor_resultdhsf_positive)) * ff_v_mce_mdr_cofactor_resultdhsf_positive)) /\ exists ff_q_mce_mdr_cofactor_resultdhsf_positive_successor. ff_u_mce_mdr_cofactor_resultdhsf_positive = ff_q_mce_mdr_cofactor_resultdhsf_positive_successor * S ((S (S ff_i_mce_mdr_cofactor_resultdhsf_positive)) * ff_v_mce_mdr_cofactor_resultdhsf_positive) + (ff_s_mce_mdr_cofactor_resultdhsf_positive))) /\ ff_s_mce_mdr_cofactor_resultdhsf_positive = ff_r_mce_mdr_cofactor_resultdhsf_positive + ff_a_mce_mdr_cofactor_resultdhsf_positive)))))) /\ (exists ff_u_mce_mdr_cofactor_resultdhsf_negative ff_v_mce_mdr_cofactor_resultdhsf_negative. ((((exists ff_h_mce_mdr_cofactor_resultdhsf_negative_start. ff_h_mce_mdr_cofactor_resultdhsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_cofactor_resultdhsf_negative)) /\ exists ff_q_mce_mdr_cofactor_resultdhsf_negative_start. ff_u_mce_mdr_cofactor_resultdhsf_negative = ff_q_mce_mdr_cofactor_resultdhsf_negative_start * S ((S (0)) * ff_v_mce_mdr_cofactor_resultdhsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_cofactor_resultdhsf_negative_terminal. ff_h_mce_mdr_cofactor_resultdhsf_negative_terminal + S (mdr_n_cofactor_resultdh) = S ((S ((S (mdr_q_cofactor_resultdhs)))) * ff_v_mce_mdr_cofactor_resultdhsf_negative)) /\ exists ff_q_mce_mdr_cofactor_resultdhsf_negative_terminal. ff_u_mce_mdr_cofactor_resultdhsf_negative = ff_q_mce_mdr_cofactor_resultdhsf_negative_terminal * S ((S ((S (mdr_q_cofactor_resultdhs)))) * ff_v_mce_mdr_cofactor_resultdhsf_negative) + (mdr_n_cofactor_resultdh))) /\ forall ff_i_mce_mdr_cofactor_resultdhsf_negative. (exists ff_lt_mce_mdr_cofactor_resultdhsf_negative_bound. ff_lt_mce_mdr_cofactor_resultdhsf_negative_bound + S ff_i_mce_mdr_cofactor_resultdhsf_negative = (S (mdr_q_cofactor_resultdhs))) -> exists ff_a_mce_mdr_cofactor_resultdhsf_negative ff_r_mce_mdr_cofactor_resultdhsf_negative ff_s_mce_mdr_cofactor_resultdhsf_negative. ((((exists ff_h_mce_mdr_cofactor_resultdhsf_negative_summand. ff_h_mce_mdr_cofactor_resultdhsf_negative_summand + S (ff_a_mce_mdr_cofactor_resultdhsf_negative) = S ((S (ff_i_mce_mdr_cofactor_resultdhsf_negative)) * ff_vc_mce_fold_mdr_cofactor_resultdhsf)) /\ exists ff_q_mce_mdr_cofactor_resultdhsf_negative_summand. ff_vb_mce_fold_mdr_cofactor_resultdhsf = ff_q_mce_mdr_cofactor_resultdhsf_negative_summand * S ((S (ff_i_mce_mdr_cofactor_resultdhsf_negative)) * ff_vc_mce_fold_mdr_cofactor_resultdhsf) + (ff_a_mce_mdr_cofactor_resultdhsf_negative))) /\ ((((exists ff_h_mce_mdr_cofactor_resultdhsf_negative_partial. ff_h_mce_mdr_cofactor_resultdhsf_negative_partial + S (ff_r_mce_mdr_cofactor_resultdhsf_negative) = S ((S (ff_i_mce_mdr_cofactor_resultdhsf_negative)) * ff_v_mce_mdr_cofactor_resultdhsf_negative)) /\ exists ff_q_mce_mdr_cofactor_resultdhsf_negative_partial. ff_u_mce_mdr_cofactor_resultdhsf_negative = ff_q_mce_mdr_cofactor_resultdhsf_negative_partial * S ((S (ff_i_mce_mdr_cofactor_resultdhsf_negative)) * ff_v_mce_mdr_cofactor_resultdhsf_negative) + (ff_r_mce_mdr_cofactor_resultdhsf_negative))) /\ ((((exists ff_h_mce_mdr_cofactor_resultdhsf_negative_successor. ff_h_mce_mdr_cofactor_resultdhsf_negative_successor + S (ff_s_mce_mdr_cofactor_resultdhsf_negative) = S ((S (S ff_i_mce_mdr_cofactor_resultdhsf_negative)) * ff_v_mce_mdr_cofactor_resultdhsf_negative)) /\ exists ff_q_mce_mdr_cofactor_resultdhsf_negative_successor. ff_u_mce_mdr_cofactor_resultdhsf_negative = ff_q_mce_mdr_cofactor_resultdhsf_negative_successor * S ((S (S ff_i_mce_mdr_cofactor_resultdhsf_negative)) * ff_v_mce_mdr_cofactor_resultdhsf_negative) + (ff_s_mce_mdr_cofactor_resultdhsf_negative))) /\ ff_s_mce_mdr_cofactor_resultdhsf_negative = ff_r_mce_mdr_cofactor_resultdhsf_negative + ff_a_mce_mdr_cofactor_resultdhsf_negative))))))))))))))) /\ ((exists mdr_gap_cofactor_resultdi. mdr_gap_cofactor_resultdi + S (mdr_i_cofactor_resultd) = (mdr_l_cofactor_resultd)) /\ (exists mdr_z_cofactor_resultdr. ((exists mdr_a_cofactor_resultdrc mdr_b_cofactor_resultdrc mdr_c_cofactor_resultdrc mdr_e_cofactor_resultdrc mdr_f_cofactor_resultdrc. ((mdr_a_cofactor_resultdrc = ((q) + (mdr_up_cofactor_result)) * S ((q) + (mdr_up_cofactor_result)) + ((mdr_up_cofactor_result) + (mdr_up_cofactor_result))) /\ ((mdr_b_cofactor_resultdrc = ((mdr_us_cofactor_result) + (mdr_un_cofactor_result)) * S ((mdr_us_cofactor_result) + (mdr_un_cofactor_result)) + ((mdr_un_cofactor_result) + (mdr_un_cofactor_result))) /\ ((mdr_c_cofactor_resultdrc = ((mdr_a_cofactor_resultdrc) + (mdr_b_cofactor_resultdrc)) * S ((mdr_a_cofactor_resultdrc) + (mdr_b_cofactor_resultdrc)) + ((mdr_b_cofactor_resultdrc) + (mdr_b_cofactor_resultdrc))) /\ ((mdr_e_cofactor_resultdrc = ((mdr_p_cofactor_result) + (mdr_n_cofactor_result)) * S ((mdr_p_cofactor_result) + (mdr_n_cofactor_result)) + ((mdr_n_cofactor_result) + (mdr_n_cofactor_result))) /\ ((mdr_f_cofactor_resultdrc = ((mdr_ut_cofactor_result) + (mdr_e_cofactor_resultdrc)) * S ((mdr_ut_cofactor_result) + (mdr_e_cofactor_resultdrc)) + ((mdr_e_cofactor_resultdrc) + (mdr_e_cofactor_resultdrc))) /\ ((mdr_z_cofactor_resultdr) = ((mdr_c_cofactor_resultdrc) + (mdr_f_cofactor_resultdrc)) * S ((mdr_c_cofactor_resultdrc) + (mdr_f_cofactor_resultdrc)) + ((mdr_f_cofactor_resultdrc) + (mdr_f_cofactor_resultdrc))))))))) /\ (((exists ff_h_mdr_cofactor_resultdrb. ff_h_mdr_cofactor_resultdrb + S (mdr_z_cofactor_resultdr) = S ((S (mdr_i_cofactor_resultd)) * mdr_c_cofactor_resultd)) /\ exists ff_q_mdr_cofactor_resultdrb. mdr_b_cofactor_resultd = ff_q_mdr_cofactor_resultdrb * S ((S (mdr_i_cofactor_resultd)) * mdr_c_cofactor_resultd) + (mdr_z_cofactor_resultdr)))))))) /\ ((((exists ff_h_mdr_cofactor_resultp. ff_h_mdr_cofactor_resultp + S (mdr_p_cofactor_result) = S ((S (mdr_j_cofactor_result)) * ec)) /\ exists ff_q_mdr_cofactor_resultp. eb = ff_q_mdr_cofactor_resultp * S ((S (mdr_j_cofactor_result)) * ec) + (mdr_p_cofactor_result))) /\ (((exists ff_h_mdr_cofactor_resultn. ff_h_mdr_cofactor_resultn + S (mdr_n_cofactor_result) = S ((S (mdr_j_cofactor_result)) * fc)) /\ exists ff_q_mdr_cofactor_resultn. fb = ff_q_mdr_cofactor_resultn * S ((S (mdr_j_cofactor_result)) * fc) + (mdr_n_cofactor_result))))))) /\ (exists ff_ub_mce_fold_mdr_cofactor_result ff_uc_mce_fold_mdr_cofactor_result ff_vb_mce_fold_mdr_cofactor_result ff_vc_mce_fold_mdr_cofactor_result. ((forall ff_index_mce_alternating_mdr_cofactor_result_prefix. (exists ff_gap_mce_mdr_cofactor_result_prefix_index. ff_gap_mce_mdr_cofactor_result_prefix_index + S (ff_index_mce_alternating_mdr_cofactor_result_prefix) = (S q)) -> exists ff_ap_mce_alternating_mdr_cofactor_result_prefix ff_an_mce_alternating_mdr_cofactor_result_prefix ff_bp_mce_alternating_mdr_cofactor_result_prefix ff_bn_mce_alternating_mdr_cofactor_result_prefix ff_p_mce_alternating_mdr_cofactor_result_prefix ff_n_mce_alternating_mdr_cofactor_result_prefix. ((((exists ff_h_mce_mdr_cofactor_result_prefix_ap. ff_h_mce_mdr_cofactor_result_prefix_ap + S (ff_ap_mce_alternating_mdr_cofactor_result_prefix) = S ((S (ff_index_mce_alternating_mdr_cofactor_result_prefix)) * pc)) /\ exists ff_q_mce_mdr_cofactor_result_prefix_ap. pb = ff_q_mce_mdr_cofactor_result_prefix_ap * S ((S (ff_index_mce_alternating_mdr_cofactor_result_prefix)) * pc) + (ff_ap_mce_alternating_mdr_cofactor_result_prefix))) /\ ((((exists ff_h_mce_mdr_cofactor_result_prefix_an. ff_h_mce_mdr_cofactor_result_prefix_an + S (ff_an_mce_alternating_mdr_cofactor_result_prefix) = S ((S (ff_index_mce_alternating_mdr_cofactor_result_prefix)) * nc)) /\ exists ff_q_mce_mdr_cofactor_result_prefix_an. nb = ff_q_mce_mdr_cofactor_result_prefix_an * S ((S (ff_index_mce_alternating_mdr_cofactor_result_prefix)) * nc) + (ff_an_mce_alternating_mdr_cofactor_result_prefix))) /\ ((((exists ff_h_mce_mdr_cofactor_result_prefix_bp. ff_h_mce_mdr_cofactor_result_prefix_bp + S (ff_bp_mce_alternating_mdr_cofactor_result_prefix) = S ((S (ff_index_mce_alternating_mdr_cofactor_result_prefix)) * ec)) /\ exists ff_q_mce_mdr_cofactor_result_prefix_bp. eb = ff_q_mce_mdr_cofactor_result_prefix_bp * S ((S (ff_index_mce_alternating_mdr_cofactor_result_prefix)) * ec) + (ff_bp_mce_alternating_mdr_cofactor_result_prefix))) /\ ((((exists ff_h_mce_mdr_cofactor_result_prefix_bn. ff_h_mce_mdr_cofactor_result_prefix_bn + S (ff_bn_mce_alternating_mdr_cofactor_result_prefix) = S ((S (ff_index_mce_alternating_mdr_cofactor_result_prefix)) * fc)) /\ exists ff_q_mce_mdr_cofactor_result_prefix_bn. fb = ff_q_mce_mdr_cofactor_result_prefix_bn * S ((S (ff_index_mce_alternating_mdr_cofactor_result_prefix)) * fc) + (ff_bn_mce_alternating_mdr_cofactor_result_prefix))) /\ ((((exists ff_h_mce_mdr_cofactor_result_prefix_positive. ff_h_mce_mdr_cofactor_result_prefix_positive + S (ff_p_mce_alternating_mdr_cofactor_result_prefix) = S ((S (ff_index_mce_alternating_mdr_cofactor_result_prefix)) * ff_uc_mce_fold_mdr_cofactor_result)) /\ exists ff_q_mce_mdr_cofactor_result_prefix_positive. ff_ub_mce_fold_mdr_cofactor_result = ff_q_mce_mdr_cofactor_result_prefix_positive * S ((S (ff_index_mce_alternating_mdr_cofactor_result_prefix)) * ff_uc_mce_fold_mdr_cofactor_result) + (ff_p_mce_alternating_mdr_cofactor_result_prefix))) /\ ((((exists ff_h_mce_mdr_cofactor_result_prefix_negative. ff_h_mce_mdr_cofactor_result_prefix_negative + S (ff_n_mce_alternating_mdr_cofactor_result_prefix) = S ((S (ff_index_mce_alternating_mdr_cofactor_result_prefix)) * ff_vc_mce_fold_mdr_cofactor_result)) /\ exists ff_q_mce_mdr_cofactor_result_prefix_negative. ff_vb_mce_fold_mdr_cofactor_result = ff_q_mce_mdr_cofactor_result_prefix_negative * S ((S (ff_index_mce_alternating_mdr_cofactor_result_prefix)) * ff_vc_mce_fold_mdr_cofactor_result) + (ff_n_mce_alternating_mdr_cofactor_result_prefix))) /\ (((exists ff_even_mce_term_mdr_cofactor_result_prefix_term. ff_index_mce_alternating_mdr_cofactor_result_prefix = 2 * ff_even_mce_term_mdr_cofactor_result_prefix_term) /\ (ff_p_mce_alternating_mdr_cofactor_result_prefix = (ff_ap_mce_alternating_mdr_cofactor_result_prefix) * (ff_bp_mce_alternating_mdr_cofactor_result_prefix) + (ff_an_mce_alternating_mdr_cofactor_result_prefix) * (ff_bn_mce_alternating_mdr_cofactor_result_prefix) /\ ff_n_mce_alternating_mdr_cofactor_result_prefix = (ff_ap_mce_alternating_mdr_cofactor_result_prefix) * (ff_bn_mce_alternating_mdr_cofactor_result_prefix) + (ff_an_mce_alternating_mdr_cofactor_result_prefix) * (ff_bp_mce_alternating_mdr_cofactor_result_prefix))) \/ ((exists ff_odd_mce_term_mdr_cofactor_result_prefix_term. ff_index_mce_alternating_mdr_cofactor_result_prefix = 2 * ff_odd_mce_term_mdr_cofactor_result_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_cofactor_result_prefix = (ff_ap_mce_alternating_mdr_cofactor_result_prefix) * (ff_bn_mce_alternating_mdr_cofactor_result_prefix) + (ff_an_mce_alternating_mdr_cofactor_result_prefix) * (ff_bp_mce_alternating_mdr_cofactor_result_prefix) /\ ff_n_mce_alternating_mdr_cofactor_result_prefix = (ff_ap_mce_alternating_mdr_cofactor_result_prefix) * (ff_bp_mce_alternating_mdr_cofactor_result_prefix) + (ff_an_mce_alternating_mdr_cofactor_result_prefix) * (ff_bn_mce_alternating_mdr_cofactor_result_prefix))))))))))) /\ ((exists ff_u_mce_mdr_cofactor_result_positive ff_v_mce_mdr_cofactor_result_positive. ((((exists ff_h_mce_mdr_cofactor_result_positive_start. ff_h_mce_mdr_cofactor_result_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_cofactor_result_positive)) /\ exists ff_q_mce_mdr_cofactor_result_positive_start. ff_u_mce_mdr_cofactor_result_positive = ff_q_mce_mdr_cofactor_result_positive_start * S ((S (0)) * ff_v_mce_mdr_cofactor_result_positive) + (0))) /\ ((((exists ff_h_mce_mdr_cofactor_result_positive_terminal. ff_h_mce_mdr_cofactor_result_positive_terminal + S (p) = S ((S ((S q))) * ff_v_mce_mdr_cofactor_result_positive)) /\ exists ff_q_mce_mdr_cofactor_result_positive_terminal. ff_u_mce_mdr_cofactor_result_positive = ff_q_mce_mdr_cofactor_result_positive_terminal * S ((S ((S q))) * ff_v_mce_mdr_cofactor_result_positive) + (p))) /\ forall ff_i_mce_mdr_cofactor_result_positive. (exists ff_lt_mce_mdr_cofactor_result_positive_bound. ff_lt_mce_mdr_cofactor_result_positive_bound + S ff_i_mce_mdr_cofactor_result_positive = (S q)) -> exists ff_a_mce_mdr_cofactor_result_positive ff_r_mce_mdr_cofactor_result_positive ff_s_mce_mdr_cofactor_result_positive. ((((exists ff_h_mce_mdr_cofactor_result_positive_summand. ff_h_mce_mdr_cofactor_result_positive_summand + S (ff_a_mce_mdr_cofactor_result_positive) = S ((S (ff_i_mce_mdr_cofactor_result_positive)) * ff_uc_mce_fold_mdr_cofactor_result)) /\ exists ff_q_mce_mdr_cofactor_result_positive_summand. ff_ub_mce_fold_mdr_cofactor_result = ff_q_mce_mdr_cofactor_result_positive_summand * S ((S (ff_i_mce_mdr_cofactor_result_positive)) * ff_uc_mce_fold_mdr_cofactor_result) + (ff_a_mce_mdr_cofactor_result_positive))) /\ ((((exists ff_h_mce_mdr_cofactor_result_positive_partial. ff_h_mce_mdr_cofactor_result_positive_partial + S (ff_r_mce_mdr_cofactor_result_positive) = S ((S (ff_i_mce_mdr_cofactor_result_positive)) * ff_v_mce_mdr_cofactor_result_positive)) /\ exists ff_q_mce_mdr_cofactor_result_positive_partial. ff_u_mce_mdr_cofactor_result_positive = ff_q_mce_mdr_cofactor_result_positive_partial * S ((S (ff_i_mce_mdr_cofactor_result_positive)) * ff_v_mce_mdr_cofactor_result_positive) + (ff_r_mce_mdr_cofactor_result_positive))) /\ ((((exists ff_h_mce_mdr_cofactor_result_positive_successor. ff_h_mce_mdr_cofactor_result_positive_successor + S (ff_s_mce_mdr_cofactor_result_positive) = S ((S (S ff_i_mce_mdr_cofactor_result_positive)) * ff_v_mce_mdr_cofactor_result_positive)) /\ exists ff_q_mce_mdr_cofactor_result_positive_successor. ff_u_mce_mdr_cofactor_result_positive = ff_q_mce_mdr_cofactor_result_positive_successor * S ((S (S ff_i_mce_mdr_cofactor_result_positive)) * ff_v_mce_mdr_cofactor_result_positive) + (ff_s_mce_mdr_cofactor_result_positive))) /\ ff_s_mce_mdr_cofactor_result_positive = ff_r_mce_mdr_cofactor_result_positive + ff_a_mce_mdr_cofactor_result_positive)))))) /\ (exists ff_u_mce_mdr_cofactor_result_negative ff_v_mce_mdr_cofactor_result_negative. ((((exists ff_h_mce_mdr_cofactor_result_negative_start. ff_h_mce_mdr_cofactor_result_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_cofactor_result_negative)) /\ exists ff_q_mce_mdr_cofactor_result_negative_start. ff_u_mce_mdr_cofactor_result_negative = ff_q_mce_mdr_cofactor_result_negative_start * S ((S (0)) * ff_v_mce_mdr_cofactor_result_negative) + (0))) /\ ((((exists ff_h_mce_mdr_cofactor_result_negative_terminal. ff_h_mce_mdr_cofactor_result_negative_terminal + S (n) = S ((S ((S q))) * ff_v_mce_mdr_cofactor_result_negative)) /\ exists ff_q_mce_mdr_cofactor_result_negative_terminal. ff_u_mce_mdr_cofactor_result_negative = ff_q_mce_mdr_cofactor_result_negative_terminal * S ((S ((S q))) * ff_v_mce_mdr_cofactor_result_negative) + (n))) /\ forall ff_i_mce_mdr_cofactor_result_negative. (exists ff_lt_mce_mdr_cofactor_result_negative_bound. ff_lt_mce_mdr_cofactor_result_negative_bound + S ff_i_mce_mdr_cofactor_result_negative = (S q)) -> exists ff_a_mce_mdr_cofactor_result_negative ff_r_mce_mdr_cofactor_result_negative ff_s_mce_mdr_cofactor_result_negative. ((((exists ff_h_mce_mdr_cofactor_result_negative_summand. ff_h_mce_mdr_cofactor_result_negative_summand + S (ff_a_mce_mdr_cofactor_result_negative) = S ((S (ff_i_mce_mdr_cofactor_result_negative)) * ff_vc_mce_fold_mdr_cofactor_result)) /\ exists ff_q_mce_mdr_cofactor_result_negative_summand. ff_vb_mce_fold_mdr_cofactor_result = ff_q_mce_mdr_cofactor_result_negative_summand * S ((S (ff_i_mce_mdr_cofactor_result_negative)) * ff_vc_mce_fold_mdr_cofactor_result) + (ff_a_mce_mdr_cofactor_result_negative))) /\ ((((exists ff_h_mce_mdr_cofactor_result_negative_partial. ff_h_mce_mdr_cofactor_result_negative_partial + S (ff_r_mce_mdr_cofactor_result_negative) = S ((S (ff_i_mce_mdr_cofactor_result_negative)) * ff_v_mce_mdr_cofactor_result_negative)) /\ exists ff_q_mce_mdr_cofactor_result_negative_partial. ff_u_mce_mdr_cofactor_result_negative = ff_q_mce_mdr_cofactor_result_negative_partial * S ((S (ff_i_mce_mdr_cofactor_result_negative)) * ff_v_mce_mdr_cofactor_result_negative) + (ff_r_mce_mdr_cofactor_result_negative))) /\ ((((exists ff_h_mce_mdr_cofactor_result_negative_successor. ff_h_mce_mdr_cofactor_result_negative_successor + S (ff_s_mce_mdr_cofactor_result_negative) = S ((S (S ff_i_mce_mdr_cofactor_result_negative)) * ff_v_mce_mdr_cofactor_result_negative)) /\ exists ff_q_mce_mdr_cofactor_result_negative_successor. ff_u_mce_mdr_cofactor_result_negative = ff_q_mce_mdr_cofactor_result_negative_successor * S ((S (S ff_i_mce_mdr_cofactor_result_negative)) * ff_v_mce_mdr_cofactor_result_negative) + (ff_s_mce_mdr_cofactor_result_negative))) /\ ff_s_mce_mdr_cofactor_result_negative = ff_r_mce_mdr_cofactor_result_negative + ff_a_mce_mdr_cofactor_result_negative))))))))))