matrix_recursive_cofactor_streams_from_functionality

Exact expanded first-order arithmetic statement

forall pb pc nb nc qb qc rb rc q eb ec fb fc ub uc vb vc. (forall mdr_pb_cofactor_recursion mdr_pc_cofactor_recursion mdr_nb_cofactor_recursion mdr_nc_cofactor_recursion mdr_qb_cofactor_recursion mdr_qc_cofactor_recursion mdr_rb_cofactor_recursion mdr_rc_cofactor_recursion mdr_p_cofactor_recursion mdr_n_cofactor_recursion mdr_r_cofactor_recursion mdr_s_cofactor_recursion. (((forall mdr_i_cofactor_recursionmp mdr_a_cofactor_recursionmp. (exists mdr_gap_cofactor_recursionmpb. mdr_gap_cofactor_recursionmpb + S (mdr_i_cofactor_recursionmp) = ((q) * (q))) -> (((exists ff_h_mdr_cofactor_recursionmpo. ff_h_mdr_cofactor_recursionmpo + S (mdr_a_cofactor_recursionmp) = S ((S (mdr_i_cofactor_recursionmp)) * mdr_pc_cofactor_recursion)) /\ exists ff_q_mdr_cofactor_recursionmpo. mdr_pb_cofactor_recursion = ff_q_mdr_cofactor_recursionmpo * S ((S (mdr_i_cofactor_recursionmp)) * mdr_pc_cofactor_recursion) + (mdr_a_cofactor_recursionmp))) -> (((exists ff_h_mdr_cofactor_recursionmpn. ff_h_mdr_cofactor_recursionmpn + S (mdr_a_cofactor_recursionmp) = S ((S (mdr_i_cofactor_recursionmp)) * mdr_qc_cofactor_recursion)) /\ exists ff_q_mdr_cofactor_recursionmpn. mdr_qb_cofactor_recursion = ff_q_mdr_cofactor_recursionmpn * S ((S (mdr_i_cofactor_recursionmp)) * mdr_qc_cofactor_recursion) + (mdr_a_cofactor_recursionmp)))) /\ (forall mdr_i_cofactor_recursionmn mdr_a_cofactor_recursionmn. (exists mdr_gap_cofactor_recursionmnb. mdr_gap_cofactor_recursionmnb + S (mdr_i_cofactor_recursionmn) = ((q) * (q))) -> (((exists ff_h_mdr_cofactor_recursionmno. ff_h_mdr_cofactor_recursionmno + S (mdr_a_cofactor_recursionmn) = S ((S (mdr_i_cofactor_recursionmn)) * mdr_nc_cofactor_recursion)) /\ exists ff_q_mdr_cofactor_recursionmno. mdr_nb_cofactor_recursion = ff_q_mdr_cofactor_recursionmno * S ((S (mdr_i_cofactor_recursionmn)) * mdr_nc_cofactor_recursion) + (mdr_a_cofactor_recursionmn))) -> (((exists ff_h_mdr_cofactor_recursionmnn. ff_h_mdr_cofactor_recursionmnn + S (mdr_a_cofactor_recursionmn) = S ((S (mdr_i_cofactor_recursionmn)) * mdr_rc_cofactor_recursion)) /\ exists ff_q_mdr_cofactor_recursionmnn. mdr_rb_cofactor_recursion = ff_q_mdr_cofactor_recursionmnn * S ((S (mdr_i_cofactor_recursionmn)) * mdr_rc_cofactor_recursion) + (mdr_a_cofactor_recursionmn)))))) -> (exists mdr_b_cofactor_recursiona mdr_c_cofactor_recursiona mdr_l_cofactor_recursiona mdr_i_cofactor_recursiona. ((forall mdr_i_cofactor_recursionah. (exists mdr_gap_cofactor_recursionahi. mdr_gap_cofactor_recursionahi + S (mdr_i_cofactor_recursionah) = (mdr_l_cofactor_recursiona)) -> exists mdr_d_cofactor_recursionah mdr_pb_cofactor_recursionah mdr_pc_cofactor_recursionah mdr_nb_cofactor_recursionah mdr_nc_cofactor_recursionah mdr_p_cofactor_recursionah mdr_n_cofactor_recursionah. ((exists mdr_z_cofactor_recursionahr. ((exists mdr_a_cofactor_recursionahrc mdr_b_cofactor_recursionahrc mdr_c_cofactor_recursionahrc mdr_e_cofactor_recursionahrc mdr_f_cofactor_recursionahrc. ((mdr_a_cofactor_recursionahrc = ((mdr_d_cofactor_recursionah) + (mdr_pb_cofactor_recursionah)) * S ((mdr_d_cofactor_recursionah) + (mdr_pb_cofactor_recursionah)) + ((mdr_pb_cofactor_recursionah) + (mdr_pb_cofactor_recursionah))) /\ ((mdr_b_cofactor_recursionahrc = ((mdr_pc_cofactor_recursionah) + (mdr_nb_cofactor_recursionah)) * S ((mdr_pc_cofactor_recursionah) + (mdr_nb_cofactor_recursionah)) + ((mdr_nb_cofactor_recursionah) + (mdr_nb_cofactor_recursionah))) /\ ((mdr_c_cofactor_recursionahrc = ((mdr_a_cofactor_recursionahrc) + (mdr_b_cofactor_recursionahrc)) * S ((mdr_a_cofactor_recursionahrc) + (mdr_b_cofactor_recursionahrc)) + ((mdr_b_cofactor_recursionahrc) + (mdr_b_cofactor_recursionahrc))) /\ ((mdr_e_cofactor_recursionahrc = ((mdr_p_cofactor_recursionah) + (mdr_n_cofactor_recursionah)) * S ((mdr_p_cofactor_recursionah) + (mdr_n_cofactor_recursionah)) + ((mdr_n_cofactor_recursionah) + (mdr_n_cofactor_recursionah))) /\ ((mdr_f_cofactor_recursionahrc = ((mdr_nc_cofactor_recursionah) + (mdr_e_cofactor_recursionahrc)) * S ((mdr_nc_cofactor_recursionah) + (mdr_e_cofactor_recursionahrc)) + ((mdr_e_cofactor_recursionahrc) + (mdr_e_cofactor_recursionahrc))) /\ ((mdr_z_cofactor_recursionahr) = ((mdr_c_cofactor_recursionahrc) + (mdr_f_cofactor_recursionahrc)) * S ((mdr_c_cofactor_recursionahrc) + (mdr_f_cofactor_recursionahrc)) + ((mdr_f_cofactor_recursionahrc) + (mdr_f_cofactor_recursionahrc))))))))) /\ (((exists ff_h_mdr_cofactor_recursionahrb. ff_h_mdr_cofactor_recursionahrb + S (mdr_z_cofactor_recursionahr) = S ((S (mdr_i_cofactor_recursionah)) * mdr_c_cofactor_recursiona)) /\ exists ff_q_mdr_cofactor_recursionahrb. mdr_b_cofactor_recursiona = ff_q_mdr_cofactor_recursionahrb * S ((S (mdr_i_cofactor_recursionah)) * mdr_c_cofactor_recursiona) + (mdr_z_cofactor_recursionahr))))) /\ (((((mdr_d_cofactor_recursionah) = 0) /\ (((mdr_p_cofactor_recursionah) = 1) /\ ((mdr_n_cofactor_recursionah) = 0))) \/ exists mdr_q_cofactor_recursionahs mdr_eb_cofactor_recursionahs mdr_ec_cofactor_recursionahs mdr_fb_cofactor_recursionahs mdr_fc_cofactor_recursionahs. (((mdr_d_cofactor_recursionah) = S (mdr_q_cofactor_recursionahs)) /\ ((forall mdr_j_cofactor_recursionahsc. (exists mdr_gap_cofactor_recursionahscj. mdr_gap_cofactor_recursionahscj + S (mdr_j_cofactor_recursionahsc) = (S (mdr_q_cofactor_recursionahs))) -> exists mdr_i_cofactor_recursionahsc mdr_up_cofactor_recursionahsc mdr_us_cofactor_recursionahsc mdr_un_cofactor_recursionahsc mdr_ut_cofactor_recursionahsc mdr_p_cofactor_recursionahsc mdr_n_cofactor_recursionahsc. ((exists mdr_gap_cofactor_recursionahsci. mdr_gap_cofactor_recursionahsci + S (mdr_i_cofactor_recursionahsc) = (mdr_i_cofactor_recursionah)) /\ ((exists mdr_z_cofactor_recursionahscr. ((exists mdr_a_cofactor_recursionahscrc mdr_b_cofactor_recursionahscrc mdr_c_cofactor_recursionahscrc mdr_e_cofactor_recursionahscrc mdr_f_cofactor_recursionahscrc. ((mdr_a_cofactor_recursionahscrc = ((mdr_q_cofactor_recursionahs) + (mdr_up_cofactor_recursionahsc)) * S ((mdr_q_cofactor_recursionahs) + (mdr_up_cofactor_recursionahsc)) + ((mdr_up_cofactor_recursionahsc) + (mdr_up_cofactor_recursionahsc))) /\ ((mdr_b_cofactor_recursionahscrc = ((mdr_us_cofactor_recursionahsc) + (mdr_un_cofactor_recursionahsc)) * S ((mdr_us_cofactor_recursionahsc) + (mdr_un_cofactor_recursionahsc)) + ((mdr_un_cofactor_recursionahsc) + (mdr_un_cofactor_recursionahsc))) /\ ((mdr_c_cofactor_recursionahscrc = ((mdr_a_cofactor_recursionahscrc) + (mdr_b_cofactor_recursionahscrc)) * S ((mdr_a_cofactor_recursionahscrc) + (mdr_b_cofactor_recursionahscrc)) + ((mdr_b_cofactor_recursionahscrc) + (mdr_b_cofactor_recursionahscrc))) /\ ((mdr_e_cofactor_recursionahscrc = ((mdr_p_cofactor_recursionahsc) + (mdr_n_cofactor_recursionahsc)) * S ((mdr_p_cofactor_recursionahsc) + (mdr_n_cofactor_recursionahsc)) + ((mdr_n_cofactor_recursionahsc) + (mdr_n_cofactor_recursionahsc))) /\ ((mdr_f_cofactor_recursionahscrc = ((mdr_ut_cofactor_recursionahsc) + (mdr_e_cofactor_recursionahscrc)) * S ((mdr_ut_cofactor_recursionahsc) + (mdr_e_cofactor_recursionahscrc)) + ((mdr_e_cofactor_recursionahscrc) + (mdr_e_cofactor_recursionahscrc))) /\ ((mdr_z_cofactor_recursionahscr) = ((mdr_c_cofactor_recursionahscrc) + (mdr_f_cofactor_recursionahscrc)) * S ((mdr_c_cofactor_recursionahscrc) + (mdr_f_cofactor_recursionahscrc)) + ((mdr_f_cofactor_recursionahscrc) + (mdr_f_cofactor_recursionahscrc))))))))) /\ (((exists ff_h_mdr_cofactor_recursionahscrb. ff_h_mdr_cofactor_recursionahscrb + S (mdr_z_cofactor_recursionahscr) = S ((S (mdr_i_cofactor_recursionahsc)) * mdr_c_cofactor_recursiona)) /\ exists ff_q_mdr_cofactor_recursionahscrb. mdr_b_cofactor_recursiona = ff_q_mdr_cofactor_recursionahscrb * S ((S (mdr_i_cofactor_recursionahsc)) * mdr_c_cofactor_recursiona) + (mdr_z_cofactor_recursionahscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_cofactor_recursionahscm_positive. (exists ff_gap_mdm_lt_mdr_cofactor_recursionahscm_positive_index_bound. ff_gap_mdm_lt_mdr_cofactor_recursionahscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_cofactor_recursionahscm_positive) = ((mdr_q_cofactor_recursionahs) * (mdr_q_cofactor_recursionahs))) -> exists ff_row_mdm_prefix_mdr_cofactor_recursionahscm_positive ff_column_mdm_prefix_mdr_cofactor_recursionahscm_positive ff_value_mdm_prefix_mdr_cofactor_recursionahscm_positive. (ff_index_mdm_prefix_mdr_cofactor_recursionahscm_positive = (mdr_q_cofactor_recursionahs) * ff_row_mdm_prefix_mdr_cofactor_recursionahscm_positive + ff_column_mdm_prefix_mdr_cofactor_recursionahscm_positive /\ ((exists ff_gap_mdm_lt_mdr_cofactor_recursionahscm_positive_column_bound. ff_gap_mdm_lt_mdr_cofactor_recursionahscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_cofactor_recursionahscm_positive) = (mdr_q_cofactor_recursionahs)) /\ ((exists ff_row_mdm_cell_mdr_cofactor_recursionahscm_positive_cell ff_column_mdm_cell_mdr_cofactor_recursionahscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_cofactor_recursionahscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_cofactor_recursionahscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_cofactor_recursionahscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_cofactor_recursionahscm_positive_cell = ff_row_mdm_prefix_mdr_cofactor_recursionahscm_positive) \/ ((exists ff_gap_mdm_le_mdr_cofactor_recursionahscm_positive_cell_row_after. ff_gap_mdm_le_mdr_cofactor_recursionahscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_cofactor_recursionahscm_positive)) /\ ff_row_mdm_cell_mdr_cofactor_recursionahscm_positive_cell = S ff_row_mdm_prefix_mdr_cofactor_recursionahscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_cofactor_recursionahscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_cofactor_recursionahscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_cofactor_recursionahscm_positive) = (mdr_j_cofactor_recursionahsc)) /\ ff_column_mdm_cell_mdr_cofactor_recursionahscm_positive_cell = ff_column_mdm_prefix_mdr_cofactor_recursionahscm_positive) \/ ((exists ff_gap_mdm_le_mdr_cofactor_recursionahscm_positive_cell_column_after. ff_gap_mdm_le_mdr_cofactor_recursionahscm_positive_cell_column_after + (mdr_j_cofactor_recursionahsc) = (ff_column_mdm_prefix_mdr_cofactor_recursionahscm_positive)) /\ ff_column_mdm_cell_mdr_cofactor_recursionahscm_positive_cell = S ff_column_mdm_prefix_mdr_cofactor_recursionahscm_positive))) /\ (((exists ff_h_mdm_mdr_cofactor_recursionahscm_positive_cell_source. ff_h_mdm_mdr_cofactor_recursionahscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_cofactor_recursionahscm_positive) = S ((S ((ff_row_mdm_cell_mdr_cofactor_recursionahscm_positive_cell) * (S (mdr_q_cofactor_recursionahs)) + (ff_column_mdm_cell_mdr_cofactor_recursionahscm_positive_cell))) * mdr_pc_cofactor_recursionah)) /\ exists ff_q_mdm_mdr_cofactor_recursionahscm_positive_cell_source. mdr_pb_cofactor_recursionah = ff_q_mdm_mdr_cofactor_recursionahscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_cofactor_recursionahscm_positive_cell) * (S (mdr_q_cofactor_recursionahs)) + (ff_column_mdm_cell_mdr_cofactor_recursionahscm_positive_cell))) * mdr_pc_cofactor_recursionah) + (ff_value_mdm_prefix_mdr_cofactor_recursionahscm_positive)))))) /\ (((exists ff_h_mdm_mdr_cofactor_recursionahscm_positive_target. ff_h_mdm_mdr_cofactor_recursionahscm_positive_target + S (ff_value_mdm_prefix_mdr_cofactor_recursionahscm_positive) = S ((S (ff_index_mdm_prefix_mdr_cofactor_recursionahscm_positive)) * mdr_us_cofactor_recursionahsc)) /\ exists ff_q_mdm_mdr_cofactor_recursionahscm_positive_target. mdr_up_cofactor_recursionahsc = ff_q_mdm_mdr_cofactor_recursionahscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_cofactor_recursionahscm_positive)) * mdr_us_cofactor_recursionahsc) + (ff_value_mdm_prefix_mdr_cofactor_recursionahscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_cofactor_recursionahscm_negative. (exists ff_gap_mdm_lt_mdr_cofactor_recursionahscm_negative_index_bound. ff_gap_mdm_lt_mdr_cofactor_recursionahscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_cofactor_recursionahscm_negative) = ((mdr_q_cofactor_recursionahs) * (mdr_q_cofactor_recursionahs))) -> exists ff_row_mdm_prefix_mdr_cofactor_recursionahscm_negative ff_column_mdm_prefix_mdr_cofactor_recursionahscm_negative ff_value_mdm_prefix_mdr_cofactor_recursionahscm_negative. (ff_index_mdm_prefix_mdr_cofactor_recursionahscm_negative = (mdr_q_cofactor_recursionahs) * ff_row_mdm_prefix_mdr_cofactor_recursionahscm_negative + ff_column_mdm_prefix_mdr_cofactor_recursionahscm_negative /\ ((exists ff_gap_mdm_lt_mdr_cofactor_recursionahscm_negative_column_bound. ff_gap_mdm_lt_mdr_cofactor_recursionahscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_cofactor_recursionahscm_negative) = (mdr_q_cofactor_recursionahs)) /\ ((exists ff_row_mdm_cell_mdr_cofactor_recursionahscm_negative_cell ff_column_mdm_cell_mdr_cofactor_recursionahscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_cofactor_recursionahscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_cofactor_recursionahscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_cofactor_recursionahscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_cofactor_recursionahscm_negative_cell = ff_row_mdm_prefix_mdr_cofactor_recursionahscm_negative) \/ ((exists ff_gap_mdm_le_mdr_cofactor_recursionahscm_negative_cell_row_after. ff_gap_mdm_le_mdr_cofactor_recursionahscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_cofactor_recursionahscm_negative)) /\ ff_row_mdm_cell_mdr_cofactor_recursionahscm_negative_cell = S ff_row_mdm_prefix_mdr_cofactor_recursionahscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_cofactor_recursionahscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_cofactor_recursionahscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_cofactor_recursionahscm_negative) = (mdr_j_cofactor_recursionahsc)) /\ ff_column_mdm_cell_mdr_cofactor_recursionahscm_negative_cell = ff_column_mdm_prefix_mdr_cofactor_recursionahscm_negative) \/ ((exists ff_gap_mdm_le_mdr_cofactor_recursionahscm_negative_cell_column_after. ff_gap_mdm_le_mdr_cofactor_recursionahscm_negative_cell_column_after + (mdr_j_cofactor_recursionahsc) = (ff_column_mdm_prefix_mdr_cofactor_recursionahscm_negative)) /\ ff_column_mdm_cell_mdr_cofactor_recursionahscm_negative_cell = S ff_column_mdm_prefix_mdr_cofactor_recursionahscm_negative))) /\ (((exists ff_h_mdm_mdr_cofactor_recursionahscm_negative_cell_source. ff_h_mdm_mdr_cofactor_recursionahscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_cofactor_recursionahscm_negative) = S ((S ((ff_row_mdm_cell_mdr_cofactor_recursionahscm_negative_cell) * (S (mdr_q_cofactor_recursionahs)) + (ff_column_mdm_cell_mdr_cofactor_recursionahscm_negative_cell))) * mdr_nc_cofactor_recursionah)) /\ exists ff_q_mdm_mdr_cofactor_recursionahscm_negative_cell_source. mdr_nb_cofactor_recursionah = ff_q_mdm_mdr_cofactor_recursionahscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_cofactor_recursionahscm_negative_cell) * (S (mdr_q_cofactor_recursionahs)) + (ff_column_mdm_cell_mdr_cofactor_recursionahscm_negative_cell))) * mdr_nc_cofactor_recursionah) + (ff_value_mdm_prefix_mdr_cofactor_recursionahscm_negative)))))) /\ (((exists ff_h_mdm_mdr_cofactor_recursionahscm_negative_target. ff_h_mdm_mdr_cofactor_recursionahscm_negative_target + S (ff_value_mdm_prefix_mdr_cofactor_recursionahscm_negative) = S ((S (ff_index_mdm_prefix_mdr_cofactor_recursionahscm_negative)) * mdr_ut_cofactor_recursionahsc)) /\ exists ff_q_mdm_mdr_cofactor_recursionahscm_negative_target. mdr_un_cofactor_recursionahsc = ff_q_mdm_mdr_cofactor_recursionahscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_cofactor_recursionahscm_negative)) * mdr_ut_cofactor_recursionahsc) + (ff_value_mdm_prefix_mdr_cofactor_recursionahscm_negative))))))))) /\ ((((exists ff_h_mdr_cofactor_recursionahscp. ff_h_mdr_cofactor_recursionahscp + S (mdr_p_cofactor_recursionahsc) = S ((S (mdr_j_cofactor_recursionahsc)) * mdr_ec_cofactor_recursionahs)) /\ exists ff_q_mdr_cofactor_recursionahscp. mdr_eb_cofactor_recursionahs = ff_q_mdr_cofactor_recursionahscp * S ((S (mdr_j_cofactor_recursionahsc)) * mdr_ec_cofactor_recursionahs) + (mdr_p_cofactor_recursionahsc))) /\ (((exists ff_h_mdr_cofactor_recursionahscn. ff_h_mdr_cofactor_recursionahscn + S (mdr_n_cofactor_recursionahsc) = S ((S (mdr_j_cofactor_recursionahsc)) * mdr_fc_cofactor_recursionahs)) /\ exists ff_q_mdr_cofactor_recursionahscn. mdr_fb_cofactor_recursionahs = ff_q_mdr_cofactor_recursionahscn * S ((S (mdr_j_cofactor_recursionahsc)) * mdr_fc_cofactor_recursionahs) + (mdr_n_cofactor_recursionahsc)))))))) /\ (exists ff_ub_mce_fold_mdr_cofactor_recursionahsf ff_uc_mce_fold_mdr_cofactor_recursionahsf ff_vb_mce_fold_mdr_cofactor_recursionahsf ff_vc_mce_fold_mdr_cofactor_recursionahsf. ((forall ff_index_mce_alternating_mdr_cofactor_recursionahsf_prefix. (exists ff_gap_mce_mdr_cofactor_recursionahsf_prefix_index. ff_gap_mce_mdr_cofactor_recursionahsf_prefix_index + S (ff_index_mce_alternating_mdr_cofactor_recursionahsf_prefix) = (S (mdr_q_cofactor_recursionahs))) -> exists ff_ap_mce_alternating_mdr_cofactor_recursionahsf_prefix ff_an_mce_alternating_mdr_cofactor_recursionahsf_prefix ff_bp_mce_alternating_mdr_cofactor_recursionahsf_prefix ff_bn_mce_alternating_mdr_cofactor_recursionahsf_prefix ff_p_mce_alternating_mdr_cofactor_recursionahsf_prefix ff_n_mce_alternating_mdr_cofactor_recursionahsf_prefix. ((((exists ff_h_mce_mdr_cofactor_recursionahsf_prefix_ap. ff_h_mce_mdr_cofactor_recursionahsf_prefix_ap + S (ff_ap_mce_alternating_mdr_cofactor_recursionahsf_prefix) = S ((S (ff_index_mce_alternating_mdr_cofactor_recursionahsf_prefix)) * mdr_pc_cofactor_recursionah)) /\ exists ff_q_mce_mdr_cofactor_recursionahsf_prefix_ap. mdr_pb_cofactor_recursionah = ff_q_mce_mdr_cofactor_recursionahsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_cofactor_recursionahsf_prefix)) * mdr_pc_cofactor_recursionah) + (ff_ap_mce_alternating_mdr_cofactor_recursionahsf_prefix))) /\ ((((exists ff_h_mce_mdr_cofactor_recursionahsf_prefix_an. ff_h_mce_mdr_cofactor_recursionahsf_prefix_an + S (ff_an_mce_alternating_mdr_cofactor_recursionahsf_prefix) = S ((S (ff_index_mce_alternating_mdr_cofactor_recursionahsf_prefix)) * mdr_nc_cofactor_recursionah)) /\ exists ff_q_mce_mdr_cofactor_recursionahsf_prefix_an. mdr_nb_cofactor_recursionah = ff_q_mce_mdr_cofactor_recursionahsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_cofactor_recursionahsf_prefix)) * mdr_nc_cofactor_recursionah) + (ff_an_mce_alternating_mdr_cofactor_recursionahsf_prefix))) /\ ((((exists ff_h_mce_mdr_cofactor_recursionahsf_prefix_bp. ff_h_mce_mdr_cofactor_recursionahsf_prefix_bp + S (ff_bp_mce_alternating_mdr_cofactor_recursionahsf_prefix) = S ((S (ff_index_mce_alternating_mdr_cofactor_recursionahsf_prefix)) * mdr_ec_cofactor_recursionahs)) /\ exists ff_q_mce_mdr_cofactor_recursionahsf_prefix_bp. mdr_eb_cofactor_recursionahs = ff_q_mce_mdr_cofactor_recursionahsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_cofactor_recursionahsf_prefix)) * mdr_ec_cofactor_recursionahs) + (ff_bp_mce_alternating_mdr_cofactor_recursionahsf_prefix))) /\ ((((exists ff_h_mce_mdr_cofactor_recursionahsf_prefix_bn. ff_h_mce_mdr_cofactor_recursionahsf_prefix_bn + S (ff_bn_mce_alternating_mdr_cofactor_recursionahsf_prefix) = S ((S (ff_index_mce_alternating_mdr_cofactor_recursionahsf_prefix)) * mdr_fc_cofactor_recursionahs)) /\ exists ff_q_mce_mdr_cofactor_recursionahsf_prefix_bn. mdr_fb_cofactor_recursionahs = ff_q_mce_mdr_cofactor_recursionahsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_cofactor_recursionahsf_prefix)) * mdr_fc_cofactor_recursionahs) + (ff_bn_mce_alternating_mdr_cofactor_recursionahsf_prefix))) /\ ((((exists ff_h_mce_mdr_cofactor_recursionahsf_prefix_positive. ff_h_mce_mdr_cofactor_recursionahsf_prefix_positive + S (ff_p_mce_alternating_mdr_cofactor_recursionahsf_prefix) = S ((S (ff_index_mce_alternating_mdr_cofactor_recursionahsf_prefix)) * ff_uc_mce_fold_mdr_cofactor_recursionahsf)) /\ exists ff_q_mce_mdr_cofactor_recursionahsf_prefix_positive. ff_ub_mce_fold_mdr_cofactor_recursionahsf = ff_q_mce_mdr_cofactor_recursionahsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_cofactor_recursionahsf_prefix)) * ff_uc_mce_fold_mdr_cofactor_recursionahsf) + (ff_p_mce_alternating_mdr_cofactor_recursionahsf_prefix))) /\ ((((exists ff_h_mce_mdr_cofactor_recursionahsf_prefix_negative. ff_h_mce_mdr_cofactor_recursionahsf_prefix_negative + S (ff_n_mce_alternating_mdr_cofactor_recursionahsf_prefix) = S ((S (ff_index_mce_alternating_mdr_cofactor_recursionahsf_prefix)) * ff_vc_mce_fold_mdr_cofactor_recursionahsf)) /\ exists ff_q_mce_mdr_cofactor_recursionahsf_prefix_negative. ff_vb_mce_fold_mdr_cofactor_recursionahsf = ff_q_mce_mdr_cofactor_recursionahsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_cofactor_recursionahsf_prefix)) * ff_vc_mce_fold_mdr_cofactor_recursionahsf) + (ff_n_mce_alternating_mdr_cofactor_recursionahsf_prefix))) /\ (((exists ff_even_mce_term_mdr_cofactor_recursionahsf_prefix_term. ff_index_mce_alternating_mdr_cofactor_recursionahsf_prefix = 2 * ff_even_mce_term_mdr_cofactor_recursionahsf_prefix_term) /\ (ff_p_mce_alternating_mdr_cofactor_recursionahsf_prefix = (ff_ap_mce_alternating_mdr_cofactor_recursionahsf_prefix) * (ff_bp_mce_alternating_mdr_cofactor_recursionahsf_prefix) + (ff_an_mce_alternating_mdr_cofactor_recursionahsf_prefix) * (ff_bn_mce_alternating_mdr_cofactor_recursionahsf_prefix) /\ ff_n_mce_alternating_mdr_cofactor_recursionahsf_prefix = (ff_ap_mce_alternating_mdr_cofactor_recursionahsf_prefix) * (ff_bn_mce_alternating_mdr_cofactor_recursionahsf_prefix) + (ff_an_mce_alternating_mdr_cofactor_recursionahsf_prefix) * (ff_bp_mce_alternating_mdr_cofactor_recursionahsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_cofactor_recursionahsf_prefix_term. ff_index_mce_alternating_mdr_cofactor_recursionahsf_prefix = 2 * ff_odd_mce_term_mdr_cofactor_recursionahsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_cofactor_recursionahsf_prefix = (ff_ap_mce_alternating_mdr_cofactor_recursionahsf_prefix) * (ff_bn_mce_alternating_mdr_cofactor_recursionahsf_prefix) + (ff_an_mce_alternating_mdr_cofactor_recursionahsf_prefix) * (ff_bp_mce_alternating_mdr_cofactor_recursionahsf_prefix) /\ ff_n_mce_alternating_mdr_cofactor_recursionahsf_prefix = (ff_ap_mce_alternating_mdr_cofactor_recursionahsf_prefix) * (ff_bp_mce_alternating_mdr_cofactor_recursionahsf_prefix) + (ff_an_mce_alternating_mdr_cofactor_recursionahsf_prefix) * (ff_bn_mce_alternating_mdr_cofactor_recursionahsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_cofactor_recursionahsf_positive ff_v_mce_mdr_cofactor_recursionahsf_positive. ((((exists ff_h_mce_mdr_cofactor_recursionahsf_positive_start. ff_h_mce_mdr_cofactor_recursionahsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_cofactor_recursionahsf_positive)) /\ exists ff_q_mce_mdr_cofactor_recursionahsf_positive_start. ff_u_mce_mdr_cofactor_recursionahsf_positive = ff_q_mce_mdr_cofactor_recursionahsf_positive_start * S ((S (0)) * ff_v_mce_mdr_cofactor_recursionahsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_cofactor_recursionahsf_positive_terminal. ff_h_mce_mdr_cofactor_recursionahsf_positive_terminal + S (mdr_p_cofactor_recursionah) = S ((S ((S (mdr_q_cofactor_recursionahs)))) * ff_v_mce_mdr_cofactor_recursionahsf_positive)) /\ exists ff_q_mce_mdr_cofactor_recursionahsf_positive_terminal. ff_u_mce_mdr_cofactor_recursionahsf_positive = ff_q_mce_mdr_cofactor_recursionahsf_positive_terminal * S ((S ((S (mdr_q_cofactor_recursionahs)))) * ff_v_mce_mdr_cofactor_recursionahsf_positive) + (mdr_p_cofactor_recursionah))) /\ forall ff_i_mce_mdr_cofactor_recursionahsf_positive. (exists ff_lt_mce_mdr_cofactor_recursionahsf_positive_bound. ff_lt_mce_mdr_cofactor_recursionahsf_positive_bound + S ff_i_mce_mdr_cofactor_recursionahsf_positive = (S (mdr_q_cofactor_recursionahs))) -> exists ff_a_mce_mdr_cofactor_recursionahsf_positive ff_r_mce_mdr_cofactor_recursionahsf_positive ff_s_mce_mdr_cofactor_recursionahsf_positive. ((((exists ff_h_mce_mdr_cofactor_recursionahsf_positive_summand. ff_h_mce_mdr_cofactor_recursionahsf_positive_summand + S (ff_a_mce_mdr_cofactor_recursionahsf_positive) = S ((S (ff_i_mce_mdr_cofactor_recursionahsf_positive)) * ff_uc_mce_fold_mdr_cofactor_recursionahsf)) /\ exists ff_q_mce_mdr_cofactor_recursionahsf_positive_summand. ff_ub_mce_fold_mdr_cofactor_recursionahsf = ff_q_mce_mdr_cofactor_recursionahsf_positive_summand * S ((S (ff_i_mce_mdr_cofactor_recursionahsf_positive)) * ff_uc_mce_fold_mdr_cofactor_recursionahsf) + (ff_a_mce_mdr_cofactor_recursionahsf_positive))) /\ ((((exists ff_h_mce_mdr_cofactor_recursionahsf_positive_partial. ff_h_mce_mdr_cofactor_recursionahsf_positive_partial + S (ff_r_mce_mdr_cofactor_recursionahsf_positive) = S ((S (ff_i_mce_mdr_cofactor_recursionahsf_positive)) * ff_v_mce_mdr_cofactor_recursionahsf_positive)) /\ exists ff_q_mce_mdr_cofactor_recursionahsf_positive_partial. ff_u_mce_mdr_cofactor_recursionahsf_positive = ff_q_mce_mdr_cofactor_recursionahsf_positive_partial * S ((S (ff_i_mce_mdr_cofactor_recursionahsf_positive)) * ff_v_mce_mdr_cofactor_recursionahsf_positive) + (ff_r_mce_mdr_cofactor_recursionahsf_positive))) /\ ((((exists ff_h_mce_mdr_cofactor_recursionahsf_positive_successor. ff_h_mce_mdr_cofactor_recursionahsf_positive_successor + S (ff_s_mce_mdr_cofactor_recursionahsf_positive) = S ((S (S ff_i_mce_mdr_cofactor_recursionahsf_positive)) * ff_v_mce_mdr_cofactor_recursionahsf_positive)) /\ exists ff_q_mce_mdr_cofactor_recursionahsf_positive_successor. ff_u_mce_mdr_cofactor_recursionahsf_positive = ff_q_mce_mdr_cofactor_recursionahsf_positive_successor * S ((S (S ff_i_mce_mdr_cofactor_recursionahsf_positive)) * ff_v_mce_mdr_cofactor_recursionahsf_positive) + (ff_s_mce_mdr_cofactor_recursionahsf_positive))) /\ ff_s_mce_mdr_cofactor_recursionahsf_positive = ff_r_mce_mdr_cofactor_recursionahsf_positive + ff_a_mce_mdr_cofactor_recursionahsf_positive)))))) /\ (exists ff_u_mce_mdr_cofactor_recursionahsf_negative ff_v_mce_mdr_cofactor_recursionahsf_negative. ((((exists ff_h_mce_mdr_cofactor_recursionahsf_negative_start. ff_h_mce_mdr_cofactor_recursionahsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_cofactor_recursionahsf_negative)) /\ exists ff_q_mce_mdr_cofactor_recursionahsf_negative_start. ff_u_mce_mdr_cofactor_recursionahsf_negative = ff_q_mce_mdr_cofactor_recursionahsf_negative_start * S ((S (0)) * ff_v_mce_mdr_cofactor_recursionahsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_cofactor_recursionahsf_negative_terminal. ff_h_mce_mdr_cofactor_recursionahsf_negative_terminal + S (mdr_n_cofactor_recursionah) = S ((S ((S (mdr_q_cofactor_recursionahs)))) * ff_v_mce_mdr_cofactor_recursionahsf_negative)) /\ exists ff_q_mce_mdr_cofactor_recursionahsf_negative_terminal. ff_u_mce_mdr_cofactor_recursionahsf_negative = ff_q_mce_mdr_cofactor_recursionahsf_negative_terminal * S ((S ((S (mdr_q_cofactor_recursionahs)))) * ff_v_mce_mdr_cofactor_recursionahsf_negative) + (mdr_n_cofactor_recursionah))) /\ forall ff_i_mce_mdr_cofactor_recursionahsf_negative. (exists ff_lt_mce_mdr_cofactor_recursionahsf_negative_bound. ff_lt_mce_mdr_cofactor_recursionahsf_negative_bound + S ff_i_mce_mdr_cofactor_recursionahsf_negative = (S (mdr_q_cofactor_recursionahs))) -> exists ff_a_mce_mdr_cofactor_recursionahsf_negative ff_r_mce_mdr_cofactor_recursionahsf_negative ff_s_mce_mdr_cofactor_recursionahsf_negative. ((((exists ff_h_mce_mdr_cofactor_recursionahsf_negative_summand. ff_h_mce_mdr_cofactor_recursionahsf_negative_summand + S (ff_a_mce_mdr_cofactor_recursionahsf_negative) = S ((S (ff_i_mce_mdr_cofactor_recursionahsf_negative)) * ff_vc_mce_fold_mdr_cofactor_recursionahsf)) /\ exists ff_q_mce_mdr_cofactor_recursionahsf_negative_summand. ff_vb_mce_fold_mdr_cofactor_recursionahsf = ff_q_mce_mdr_cofactor_recursionahsf_negative_summand * S ((S (ff_i_mce_mdr_cofactor_recursionahsf_negative)) * ff_vc_mce_fold_mdr_cofactor_recursionahsf) + (ff_a_mce_mdr_cofactor_recursionahsf_negative))) /\ ((((exists ff_h_mce_mdr_cofactor_recursionahsf_negative_partial. ff_h_mce_mdr_cofactor_recursionahsf_negative_partial + S (ff_r_mce_mdr_cofactor_recursionahsf_negative) = S ((S (ff_i_mce_mdr_cofactor_recursionahsf_negative)) * ff_v_mce_mdr_cofactor_recursionahsf_negative)) /\ exists ff_q_mce_mdr_cofactor_recursionahsf_negative_partial. ff_u_mce_mdr_cofactor_recursionahsf_negative = ff_q_mce_mdr_cofactor_recursionahsf_negative_partial * S ((S (ff_i_mce_mdr_cofactor_recursionahsf_negative)) * ff_v_mce_mdr_cofactor_recursionahsf_negative) + (ff_r_mce_mdr_cofactor_recursionahsf_negative))) /\ ((((exists ff_h_mce_mdr_cofactor_recursionahsf_negative_successor. ff_h_mce_mdr_cofactor_recursionahsf_negative_successor + S (ff_s_mce_mdr_cofactor_recursionahsf_negative) = S ((S (S ff_i_mce_mdr_cofactor_recursionahsf_negative)) * ff_v_mce_mdr_cofactor_recursionahsf_negative)) /\ exists ff_q_mce_mdr_cofactor_recursionahsf_negative_successor. ff_u_mce_mdr_cofactor_recursionahsf_negative = ff_q_mce_mdr_cofactor_recursionahsf_negative_successor * S ((S (S ff_i_mce_mdr_cofactor_recursionahsf_negative)) * ff_v_mce_mdr_cofactor_recursionahsf_negative) + (ff_s_mce_mdr_cofactor_recursionahsf_negative))) /\ ff_s_mce_mdr_cofactor_recursionahsf_negative = ff_r_mce_mdr_cofactor_recursionahsf_negative + ff_a_mce_mdr_cofactor_recursionahsf_negative))))))))))))))) /\ ((exists mdr_gap_cofactor_recursionai. mdr_gap_cofactor_recursionai + S (mdr_i_cofactor_recursiona) = (mdr_l_cofactor_recursiona)) /\ (exists mdr_z_cofactor_recursionar. ((exists mdr_a_cofactor_recursionarc mdr_b_cofactor_recursionarc mdr_c_cofactor_recursionarc mdr_e_cofactor_recursionarc mdr_f_cofactor_recursionarc. ((mdr_a_cofactor_recursionarc = ((q) + (mdr_pb_cofactor_recursion)) * S ((q) + (mdr_pb_cofactor_recursion)) + ((mdr_pb_cofactor_recursion) + (mdr_pb_cofactor_recursion))) /\ ((mdr_b_cofactor_recursionarc = ((mdr_pc_cofactor_recursion) + (mdr_nb_cofactor_recursion)) * S ((mdr_pc_cofactor_recursion) + (mdr_nb_cofactor_recursion)) + ((mdr_nb_cofactor_recursion) + (mdr_nb_cofactor_recursion))) /\ ((mdr_c_cofactor_recursionarc = ((mdr_a_cofactor_recursionarc) + (mdr_b_cofactor_recursionarc)) * S ((mdr_a_cofactor_recursionarc) + (mdr_b_cofactor_recursionarc)) + ((mdr_b_cofactor_recursionarc) + (mdr_b_cofactor_recursionarc))) /\ ((mdr_e_cofactor_recursionarc = ((mdr_p_cofactor_recursion) + (mdr_n_cofactor_recursion)) * S ((mdr_p_cofactor_recursion) + (mdr_n_cofactor_recursion)) + ((mdr_n_cofactor_recursion) + (mdr_n_cofactor_recursion))) /\ ((mdr_f_cofactor_recursionarc = ((mdr_nc_cofactor_recursion) + (mdr_e_cofactor_recursionarc)) * S ((mdr_nc_cofactor_recursion) + (mdr_e_cofactor_recursionarc)) + ((mdr_e_cofactor_recursionarc) + (mdr_e_cofactor_recursionarc))) /\ ((mdr_z_cofactor_recursionar) = ((mdr_c_cofactor_recursionarc) + (mdr_f_cofactor_recursionarc)) * S ((mdr_c_cofactor_recursionarc) + (mdr_f_cofactor_recursionarc)) + ((mdr_f_cofactor_recursionarc) + (mdr_f_cofactor_recursionarc))))))))) /\ (((exists ff_h_mdr_cofactor_recursionarb. ff_h_mdr_cofactor_recursionarb + S (mdr_z_cofactor_recursionar) = S ((S (mdr_i_cofactor_recursiona)) * mdr_c_cofactor_recursiona)) /\ exists ff_q_mdr_cofactor_recursionarb. mdr_b_cofactor_recursiona = ff_q_mdr_cofactor_recursionarb * S ((S (mdr_i_cofactor_recursiona)) * mdr_c_cofactor_recursiona) + (mdr_z_cofactor_recursionar)))))))) -> (exists mdr_b_cofactor_recursionb mdr_c_cofactor_recursionb mdr_l_cofactor_recursionb mdr_i_cofactor_recursionb. ((forall mdr_i_cofactor_recursionbh. (exists mdr_gap_cofactor_recursionbhi. mdr_gap_cofactor_recursionbhi + S (mdr_i_cofactor_recursionbh) = (mdr_l_cofactor_recursionb)) -> exists mdr_d_cofactor_recursionbh mdr_pb_cofactor_recursionbh mdr_pc_cofactor_recursionbh mdr_nb_cofactor_recursionbh mdr_nc_cofactor_recursionbh mdr_p_cofactor_recursionbh mdr_n_cofactor_recursionbh. ((exists mdr_z_cofactor_recursionbhr. ((exists mdr_a_cofactor_recursionbhrc mdr_b_cofactor_recursionbhrc mdr_c_cofactor_recursionbhrc mdr_e_cofactor_recursionbhrc mdr_f_cofactor_recursionbhrc. ((mdr_a_cofactor_recursionbhrc = ((mdr_d_cofactor_recursionbh) + (mdr_pb_cofactor_recursionbh)) * S ((mdr_d_cofactor_recursionbh) + (mdr_pb_cofactor_recursionbh)) + ((mdr_pb_cofactor_recursionbh) + (mdr_pb_cofactor_recursionbh))) /\ ((mdr_b_cofactor_recursionbhrc = ((mdr_pc_cofactor_recursionbh) + (mdr_nb_cofactor_recursionbh)) * S ((mdr_pc_cofactor_recursionbh) + (mdr_nb_cofactor_recursionbh)) + ((mdr_nb_cofactor_recursionbh) + (mdr_nb_cofactor_recursionbh))) /\ ((mdr_c_cofactor_recursionbhrc = ((mdr_a_cofactor_recursionbhrc) + (mdr_b_cofactor_recursionbhrc)) * S ((mdr_a_cofactor_recursionbhrc) + (mdr_b_cofactor_recursionbhrc)) + ((mdr_b_cofactor_recursionbhrc) + (mdr_b_cofactor_recursionbhrc))) /\ ((mdr_e_cofactor_recursionbhrc = ((mdr_p_cofactor_recursionbh) + (mdr_n_cofactor_recursionbh)) * S ((mdr_p_cofactor_recursionbh) + (mdr_n_cofactor_recursionbh)) + ((mdr_n_cofactor_recursionbh) + (mdr_n_cofactor_recursionbh))) /\ ((mdr_f_cofactor_recursionbhrc = ((mdr_nc_cofactor_recursionbh) + (mdr_e_cofactor_recursionbhrc)) * S ((mdr_nc_cofactor_recursionbh) + (mdr_e_cofactor_recursionbhrc)) + ((mdr_e_cofactor_recursionbhrc) + (mdr_e_cofactor_recursionbhrc))) /\ ((mdr_z_cofactor_recursionbhr) = ((mdr_c_cofactor_recursionbhrc) + (mdr_f_cofactor_recursionbhrc)) * S ((mdr_c_cofactor_recursionbhrc) + (mdr_f_cofactor_recursionbhrc)) + ((mdr_f_cofactor_recursionbhrc) + (mdr_f_cofactor_recursionbhrc))))))))) /\ (((exists ff_h_mdr_cofactor_recursionbhrb. ff_h_mdr_cofactor_recursionbhrb + S (mdr_z_cofactor_recursionbhr) = S ((S (mdr_i_cofactor_recursionbh)) * mdr_c_cofactor_recursionb)) /\ exists ff_q_mdr_cofactor_recursionbhrb. mdr_b_cofactor_recursionb = ff_q_mdr_cofactor_recursionbhrb * S ((S (mdr_i_cofactor_recursionbh)) * mdr_c_cofactor_recursionb) + (mdr_z_cofactor_recursionbhr))))) /\ (((((mdr_d_cofactor_recursionbh) = 0) /\ (((mdr_p_cofactor_recursionbh) = 1) /\ ((mdr_n_cofactor_recursionbh) = 0))) \/ exists mdr_q_cofactor_recursionbhs mdr_eb_cofactor_recursionbhs mdr_ec_cofactor_recursionbhs mdr_fb_cofactor_recursionbhs mdr_fc_cofactor_recursionbhs. (((mdr_d_cofactor_recursionbh) = S (mdr_q_cofactor_recursionbhs)) /\ ((forall mdr_j_cofactor_recursionbhsc. (exists mdr_gap_cofactor_recursionbhscj. mdr_gap_cofactor_recursionbhscj + S (mdr_j_cofactor_recursionbhsc) = (S (mdr_q_cofactor_recursionbhs))) -> exists mdr_i_cofactor_recursionbhsc mdr_up_cofactor_recursionbhsc mdr_us_cofactor_recursionbhsc mdr_un_cofactor_recursionbhsc mdr_ut_cofactor_recursionbhsc mdr_p_cofactor_recursionbhsc mdr_n_cofactor_recursionbhsc. ((exists mdr_gap_cofactor_recursionbhsci. mdr_gap_cofactor_recursionbhsci + S (mdr_i_cofactor_recursionbhsc) = (mdr_i_cofactor_recursionbh)) /\ ((exists mdr_z_cofactor_recursionbhscr. ((exists mdr_a_cofactor_recursionbhscrc mdr_b_cofactor_recursionbhscrc mdr_c_cofactor_recursionbhscrc mdr_e_cofactor_recursionbhscrc mdr_f_cofactor_recursionbhscrc. ((mdr_a_cofactor_recursionbhscrc = ((mdr_q_cofactor_recursionbhs) + (mdr_up_cofactor_recursionbhsc)) * S ((mdr_q_cofactor_recursionbhs) + (mdr_up_cofactor_recursionbhsc)) + ((mdr_up_cofactor_recursionbhsc) + (mdr_up_cofactor_recursionbhsc))) /\ ((mdr_b_cofactor_recursionbhscrc = ((mdr_us_cofactor_recursionbhsc) + (mdr_un_cofactor_recursionbhsc)) * S ((mdr_us_cofactor_recursionbhsc) + (mdr_un_cofactor_recursionbhsc)) + ((mdr_un_cofactor_recursionbhsc) + (mdr_un_cofactor_recursionbhsc))) /\ ((mdr_c_cofactor_recursionbhscrc = ((mdr_a_cofactor_recursionbhscrc) + (mdr_b_cofactor_recursionbhscrc)) * S ((mdr_a_cofactor_recursionbhscrc) + (mdr_b_cofactor_recursionbhscrc)) + ((mdr_b_cofactor_recursionbhscrc) + (mdr_b_cofactor_recursionbhscrc))) /\ ((mdr_e_cofactor_recursionbhscrc = ((mdr_p_cofactor_recursionbhsc) + (mdr_n_cofactor_recursionbhsc)) * S ((mdr_p_cofactor_recursionbhsc) + (mdr_n_cofactor_recursionbhsc)) + ((mdr_n_cofactor_recursionbhsc) + (mdr_n_cofactor_recursionbhsc))) /\ ((mdr_f_cofactor_recursionbhscrc = ((mdr_ut_cofactor_recursionbhsc) + (mdr_e_cofactor_recursionbhscrc)) * S ((mdr_ut_cofactor_recursionbhsc) + (mdr_e_cofactor_recursionbhscrc)) + ((mdr_e_cofactor_recursionbhscrc) + (mdr_e_cofactor_recursionbhscrc))) /\ ((mdr_z_cofactor_recursionbhscr) = ((mdr_c_cofactor_recursionbhscrc) + (mdr_f_cofactor_recursionbhscrc)) * S ((mdr_c_cofactor_recursionbhscrc) + (mdr_f_cofactor_recursionbhscrc)) + ((mdr_f_cofactor_recursionbhscrc) + (mdr_f_cofactor_recursionbhscrc))))))))) /\ (((exists ff_h_mdr_cofactor_recursionbhscrb. ff_h_mdr_cofactor_recursionbhscrb + S (mdr_z_cofactor_recursionbhscr) = S ((S (mdr_i_cofactor_recursionbhsc)) * mdr_c_cofactor_recursionb)) /\ exists ff_q_mdr_cofactor_recursionbhscrb. mdr_b_cofactor_recursionb = ff_q_mdr_cofactor_recursionbhscrb * S ((S (mdr_i_cofactor_recursionbhsc)) * mdr_c_cofactor_recursionb) + (mdr_z_cofactor_recursionbhscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_cofactor_recursionbhscm_positive. (exists ff_gap_mdm_lt_mdr_cofactor_recursionbhscm_positive_index_bound. ff_gap_mdm_lt_mdr_cofactor_recursionbhscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_cofactor_recursionbhscm_positive) = ((mdr_q_cofactor_recursionbhs) * (mdr_q_cofactor_recursionbhs))) -> exists ff_row_mdm_prefix_mdr_cofactor_recursionbhscm_positive ff_column_mdm_prefix_mdr_cofactor_recursionbhscm_positive ff_value_mdm_prefix_mdr_cofactor_recursionbhscm_positive. (ff_index_mdm_prefix_mdr_cofactor_recursionbhscm_positive = (mdr_q_cofactor_recursionbhs) * ff_row_mdm_prefix_mdr_cofactor_recursionbhscm_positive + ff_column_mdm_prefix_mdr_cofactor_recursionbhscm_positive /\ ((exists ff_gap_mdm_lt_mdr_cofactor_recursionbhscm_positive_column_bound. ff_gap_mdm_lt_mdr_cofactor_recursionbhscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_cofactor_recursionbhscm_positive) = (mdr_q_cofactor_recursionbhs)) /\ ((exists ff_row_mdm_cell_mdr_cofactor_recursionbhscm_positive_cell ff_column_mdm_cell_mdr_cofactor_recursionbhscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_cofactor_recursionbhscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_cofactor_recursionbhscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_cofactor_recursionbhscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_cofactor_recursionbhscm_positive_cell = ff_row_mdm_prefix_mdr_cofactor_recursionbhscm_positive) \/ ((exists ff_gap_mdm_le_mdr_cofactor_recursionbhscm_positive_cell_row_after. ff_gap_mdm_le_mdr_cofactor_recursionbhscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_cofactor_recursionbhscm_positive)) /\ ff_row_mdm_cell_mdr_cofactor_recursionbhscm_positive_cell = S ff_row_mdm_prefix_mdr_cofactor_recursionbhscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_cofactor_recursionbhscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_cofactor_recursionbhscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_cofactor_recursionbhscm_positive) = (mdr_j_cofactor_recursionbhsc)) /\ ff_column_mdm_cell_mdr_cofactor_recursionbhscm_positive_cell = ff_column_mdm_prefix_mdr_cofactor_recursionbhscm_positive) \/ ((exists ff_gap_mdm_le_mdr_cofactor_recursionbhscm_positive_cell_column_after. ff_gap_mdm_le_mdr_cofactor_recursionbhscm_positive_cell_column_after + (mdr_j_cofactor_recursionbhsc) = (ff_column_mdm_prefix_mdr_cofactor_recursionbhscm_positive)) /\ ff_column_mdm_cell_mdr_cofactor_recursionbhscm_positive_cell = S ff_column_mdm_prefix_mdr_cofactor_recursionbhscm_positive))) /\ (((exists ff_h_mdm_mdr_cofactor_recursionbhscm_positive_cell_source. ff_h_mdm_mdr_cofactor_recursionbhscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_cofactor_recursionbhscm_positive) = S ((S ((ff_row_mdm_cell_mdr_cofactor_recursionbhscm_positive_cell) * (S (mdr_q_cofactor_recursionbhs)) + (ff_column_mdm_cell_mdr_cofactor_recursionbhscm_positive_cell))) * mdr_pc_cofactor_recursionbh)) /\ exists ff_q_mdm_mdr_cofactor_recursionbhscm_positive_cell_source. mdr_pb_cofactor_recursionbh = ff_q_mdm_mdr_cofactor_recursionbhscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_cofactor_recursionbhscm_positive_cell) * (S (mdr_q_cofactor_recursionbhs)) + (ff_column_mdm_cell_mdr_cofactor_recursionbhscm_positive_cell))) * mdr_pc_cofactor_recursionbh) + (ff_value_mdm_prefix_mdr_cofactor_recursionbhscm_positive)))))) /\ (((exists ff_h_mdm_mdr_cofactor_recursionbhscm_positive_target. ff_h_mdm_mdr_cofactor_recursionbhscm_positive_target + S (ff_value_mdm_prefix_mdr_cofactor_recursionbhscm_positive) = S ((S (ff_index_mdm_prefix_mdr_cofactor_recursionbhscm_positive)) * mdr_us_cofactor_recursionbhsc)) /\ exists ff_q_mdm_mdr_cofactor_recursionbhscm_positive_target. mdr_up_cofactor_recursionbhsc = ff_q_mdm_mdr_cofactor_recursionbhscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_cofactor_recursionbhscm_positive)) * mdr_us_cofactor_recursionbhsc) + (ff_value_mdm_prefix_mdr_cofactor_recursionbhscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_cofactor_recursionbhscm_negative. (exists ff_gap_mdm_lt_mdr_cofactor_recursionbhscm_negative_index_bound. ff_gap_mdm_lt_mdr_cofactor_recursionbhscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_cofactor_recursionbhscm_negative) = ((mdr_q_cofactor_recursionbhs) * (mdr_q_cofactor_recursionbhs))) -> exists ff_row_mdm_prefix_mdr_cofactor_recursionbhscm_negative ff_column_mdm_prefix_mdr_cofactor_recursionbhscm_negative ff_value_mdm_prefix_mdr_cofactor_recursionbhscm_negative. (ff_index_mdm_prefix_mdr_cofactor_recursionbhscm_negative = (mdr_q_cofactor_recursionbhs) * ff_row_mdm_prefix_mdr_cofactor_recursionbhscm_negative + ff_column_mdm_prefix_mdr_cofactor_recursionbhscm_negative /\ ((exists ff_gap_mdm_lt_mdr_cofactor_recursionbhscm_negative_column_bound. ff_gap_mdm_lt_mdr_cofactor_recursionbhscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_cofactor_recursionbhscm_negative) = (mdr_q_cofactor_recursionbhs)) /\ ((exists ff_row_mdm_cell_mdr_cofactor_recursionbhscm_negative_cell ff_column_mdm_cell_mdr_cofactor_recursionbhscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_cofactor_recursionbhscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_cofactor_recursionbhscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_cofactor_recursionbhscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_cofactor_recursionbhscm_negative_cell = ff_row_mdm_prefix_mdr_cofactor_recursionbhscm_negative) \/ ((exists ff_gap_mdm_le_mdr_cofactor_recursionbhscm_negative_cell_row_after. ff_gap_mdm_le_mdr_cofactor_recursionbhscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_cofactor_recursionbhscm_negative)) /\ ff_row_mdm_cell_mdr_cofactor_recursionbhscm_negative_cell = S ff_row_mdm_prefix_mdr_cofactor_recursionbhscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_cofactor_recursionbhscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_cofactor_recursionbhscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_cofactor_recursionbhscm_negative) = (mdr_j_cofactor_recursionbhsc)) /\ ff_column_mdm_cell_mdr_cofactor_recursionbhscm_negative_cell = ff_column_mdm_prefix_mdr_cofactor_recursionbhscm_negative) \/ ((exists ff_gap_mdm_le_mdr_cofactor_recursionbhscm_negative_cell_column_after. ff_gap_mdm_le_mdr_cofactor_recursionbhscm_negative_cell_column_after + (mdr_j_cofactor_recursionbhsc) = (ff_column_mdm_prefix_mdr_cofactor_recursionbhscm_negative)) /\ ff_column_mdm_cell_mdr_cofactor_recursionbhscm_negative_cell = S ff_column_mdm_prefix_mdr_cofactor_recursionbhscm_negative))) /\ (((exists ff_h_mdm_mdr_cofactor_recursionbhscm_negative_cell_source. ff_h_mdm_mdr_cofactor_recursionbhscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_cofactor_recursionbhscm_negative) = S ((S ((ff_row_mdm_cell_mdr_cofactor_recursionbhscm_negative_cell) * (S (mdr_q_cofactor_recursionbhs)) + (ff_column_mdm_cell_mdr_cofactor_recursionbhscm_negative_cell))) * mdr_nc_cofactor_recursionbh)) /\ exists ff_q_mdm_mdr_cofactor_recursionbhscm_negative_cell_source. mdr_nb_cofactor_recursionbh = ff_q_mdm_mdr_cofactor_recursionbhscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_cofactor_recursionbhscm_negative_cell) * (S (mdr_q_cofactor_recursionbhs)) + (ff_column_mdm_cell_mdr_cofactor_recursionbhscm_negative_cell))) * mdr_nc_cofactor_recursionbh) + (ff_value_mdm_prefix_mdr_cofactor_recursionbhscm_negative)))))) /\ (((exists ff_h_mdm_mdr_cofactor_recursionbhscm_negative_target. ff_h_mdm_mdr_cofactor_recursionbhscm_negative_target + S (ff_value_mdm_prefix_mdr_cofactor_recursionbhscm_negative) = S ((S (ff_index_mdm_prefix_mdr_cofactor_recursionbhscm_negative)) * mdr_ut_cofactor_recursionbhsc)) /\ exists ff_q_mdm_mdr_cofactor_recursionbhscm_negative_target. mdr_un_cofactor_recursionbhsc = ff_q_mdm_mdr_cofactor_recursionbhscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_cofactor_recursionbhscm_negative)) * mdr_ut_cofactor_recursionbhsc) + (ff_value_mdm_prefix_mdr_cofactor_recursionbhscm_negative))))))))) /\ ((((exists ff_h_mdr_cofactor_recursionbhscp. ff_h_mdr_cofactor_recursionbhscp + S (mdr_p_cofactor_recursionbhsc) = S ((S (mdr_j_cofactor_recursionbhsc)) * mdr_ec_cofactor_recursionbhs)) /\ exists ff_q_mdr_cofactor_recursionbhscp. mdr_eb_cofactor_recursionbhs = ff_q_mdr_cofactor_recursionbhscp * S ((S (mdr_j_cofactor_recursionbhsc)) * mdr_ec_cofactor_recursionbhs) + (mdr_p_cofactor_recursionbhsc))) /\ (((exists ff_h_mdr_cofactor_recursionbhscn. ff_h_mdr_cofactor_recursionbhscn + S (mdr_n_cofactor_recursionbhsc) = S ((S (mdr_j_cofactor_recursionbhsc)) * mdr_fc_cofactor_recursionbhs)) /\ exists ff_q_mdr_cofactor_recursionbhscn. mdr_fb_cofactor_recursionbhs = ff_q_mdr_cofactor_recursionbhscn * S ((S (mdr_j_cofactor_recursionbhsc)) * mdr_fc_cofactor_recursionbhs) + (mdr_n_cofactor_recursionbhsc)))))))) /\ (exists ff_ub_mce_fold_mdr_cofactor_recursionbhsf ff_uc_mce_fold_mdr_cofactor_recursionbhsf ff_vb_mce_fold_mdr_cofactor_recursionbhsf ff_vc_mce_fold_mdr_cofactor_recursionbhsf. ((forall ff_index_mce_alternating_mdr_cofactor_recursionbhsf_prefix. (exists ff_gap_mce_mdr_cofactor_recursionbhsf_prefix_index. ff_gap_mce_mdr_cofactor_recursionbhsf_prefix_index + S (ff_index_mce_alternating_mdr_cofactor_recursionbhsf_prefix) = (S (mdr_q_cofactor_recursionbhs))) -> exists ff_ap_mce_alternating_mdr_cofactor_recursionbhsf_prefix ff_an_mce_alternating_mdr_cofactor_recursionbhsf_prefix ff_bp_mce_alternating_mdr_cofactor_recursionbhsf_prefix ff_bn_mce_alternating_mdr_cofactor_recursionbhsf_prefix ff_p_mce_alternating_mdr_cofactor_recursionbhsf_prefix ff_n_mce_alternating_mdr_cofactor_recursionbhsf_prefix. ((((exists ff_h_mce_mdr_cofactor_recursionbhsf_prefix_ap. ff_h_mce_mdr_cofactor_recursionbhsf_prefix_ap + S (ff_ap_mce_alternating_mdr_cofactor_recursionbhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_cofactor_recursionbhsf_prefix)) * mdr_pc_cofactor_recursionbh)) /\ exists ff_q_mce_mdr_cofactor_recursionbhsf_prefix_ap. mdr_pb_cofactor_recursionbh = ff_q_mce_mdr_cofactor_recursionbhsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_cofactor_recursionbhsf_prefix)) * mdr_pc_cofactor_recursionbh) + (ff_ap_mce_alternating_mdr_cofactor_recursionbhsf_prefix))) /\ ((((exists ff_h_mce_mdr_cofactor_recursionbhsf_prefix_an. ff_h_mce_mdr_cofactor_recursionbhsf_prefix_an + S (ff_an_mce_alternating_mdr_cofactor_recursionbhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_cofactor_recursionbhsf_prefix)) * mdr_nc_cofactor_recursionbh)) /\ exists ff_q_mce_mdr_cofactor_recursionbhsf_prefix_an. mdr_nb_cofactor_recursionbh = ff_q_mce_mdr_cofactor_recursionbhsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_cofactor_recursionbhsf_prefix)) * mdr_nc_cofactor_recursionbh) + (ff_an_mce_alternating_mdr_cofactor_recursionbhsf_prefix))) /\ ((((exists ff_h_mce_mdr_cofactor_recursionbhsf_prefix_bp. ff_h_mce_mdr_cofactor_recursionbhsf_prefix_bp + S (ff_bp_mce_alternating_mdr_cofactor_recursionbhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_cofactor_recursionbhsf_prefix)) * mdr_ec_cofactor_recursionbhs)) /\ exists ff_q_mce_mdr_cofactor_recursionbhsf_prefix_bp. mdr_eb_cofactor_recursionbhs = ff_q_mce_mdr_cofactor_recursionbhsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_cofactor_recursionbhsf_prefix)) * mdr_ec_cofactor_recursionbhs) + (ff_bp_mce_alternating_mdr_cofactor_recursionbhsf_prefix))) /\ ((((exists ff_h_mce_mdr_cofactor_recursionbhsf_prefix_bn. ff_h_mce_mdr_cofactor_recursionbhsf_prefix_bn + S (ff_bn_mce_alternating_mdr_cofactor_recursionbhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_cofactor_recursionbhsf_prefix)) * mdr_fc_cofactor_recursionbhs)) /\ exists ff_q_mce_mdr_cofactor_recursionbhsf_prefix_bn. mdr_fb_cofactor_recursionbhs = ff_q_mce_mdr_cofactor_recursionbhsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_cofactor_recursionbhsf_prefix)) * mdr_fc_cofactor_recursionbhs) + (ff_bn_mce_alternating_mdr_cofactor_recursionbhsf_prefix))) /\ ((((exists ff_h_mce_mdr_cofactor_recursionbhsf_prefix_positive. ff_h_mce_mdr_cofactor_recursionbhsf_prefix_positive + S (ff_p_mce_alternating_mdr_cofactor_recursionbhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_cofactor_recursionbhsf_prefix)) * ff_uc_mce_fold_mdr_cofactor_recursionbhsf)) /\ exists ff_q_mce_mdr_cofactor_recursionbhsf_prefix_positive. ff_ub_mce_fold_mdr_cofactor_recursionbhsf = ff_q_mce_mdr_cofactor_recursionbhsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_cofactor_recursionbhsf_prefix)) * ff_uc_mce_fold_mdr_cofactor_recursionbhsf) + (ff_p_mce_alternating_mdr_cofactor_recursionbhsf_prefix))) /\ ((((exists ff_h_mce_mdr_cofactor_recursionbhsf_prefix_negative. ff_h_mce_mdr_cofactor_recursionbhsf_prefix_negative + S (ff_n_mce_alternating_mdr_cofactor_recursionbhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_cofactor_recursionbhsf_prefix)) * ff_vc_mce_fold_mdr_cofactor_recursionbhsf)) /\ exists ff_q_mce_mdr_cofactor_recursionbhsf_prefix_negative. ff_vb_mce_fold_mdr_cofactor_recursionbhsf = ff_q_mce_mdr_cofactor_recursionbhsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_cofactor_recursionbhsf_prefix)) * ff_vc_mce_fold_mdr_cofactor_recursionbhsf) + (ff_n_mce_alternating_mdr_cofactor_recursionbhsf_prefix))) /\ (((exists ff_even_mce_term_mdr_cofactor_recursionbhsf_prefix_term. ff_index_mce_alternating_mdr_cofactor_recursionbhsf_prefix = 2 * ff_even_mce_term_mdr_cofactor_recursionbhsf_prefix_term) /\ (ff_p_mce_alternating_mdr_cofactor_recursionbhsf_prefix = (ff_ap_mce_alternating_mdr_cofactor_recursionbhsf_prefix) * (ff_bp_mce_alternating_mdr_cofactor_recursionbhsf_prefix) + (ff_an_mce_alternating_mdr_cofactor_recursionbhsf_prefix) * (ff_bn_mce_alternating_mdr_cofactor_recursionbhsf_prefix) /\ ff_n_mce_alternating_mdr_cofactor_recursionbhsf_prefix = (ff_ap_mce_alternating_mdr_cofactor_recursionbhsf_prefix) * (ff_bn_mce_alternating_mdr_cofactor_recursionbhsf_prefix) + (ff_an_mce_alternating_mdr_cofactor_recursionbhsf_prefix) * (ff_bp_mce_alternating_mdr_cofactor_recursionbhsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_cofactor_recursionbhsf_prefix_term. ff_index_mce_alternating_mdr_cofactor_recursionbhsf_prefix = 2 * ff_odd_mce_term_mdr_cofactor_recursionbhsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_cofactor_recursionbhsf_prefix = (ff_ap_mce_alternating_mdr_cofactor_recursionbhsf_prefix) * (ff_bn_mce_alternating_mdr_cofactor_recursionbhsf_prefix) + (ff_an_mce_alternating_mdr_cofactor_recursionbhsf_prefix) * (ff_bp_mce_alternating_mdr_cofactor_recursionbhsf_prefix) /\ ff_n_mce_alternating_mdr_cofactor_recursionbhsf_prefix = (ff_ap_mce_alternating_mdr_cofactor_recursionbhsf_prefix) * (ff_bp_mce_alternating_mdr_cofactor_recursionbhsf_prefix) + (ff_an_mce_alternating_mdr_cofactor_recursionbhsf_prefix) * (ff_bn_mce_alternating_mdr_cofactor_recursionbhsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_cofactor_recursionbhsf_positive ff_v_mce_mdr_cofactor_recursionbhsf_positive. ((((exists ff_h_mce_mdr_cofactor_recursionbhsf_positive_start. ff_h_mce_mdr_cofactor_recursionbhsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_cofactor_recursionbhsf_positive)) /\ exists ff_q_mce_mdr_cofactor_recursionbhsf_positive_start. ff_u_mce_mdr_cofactor_recursionbhsf_positive = ff_q_mce_mdr_cofactor_recursionbhsf_positive_start * S ((S (0)) * ff_v_mce_mdr_cofactor_recursionbhsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_cofactor_recursionbhsf_positive_terminal. ff_h_mce_mdr_cofactor_recursionbhsf_positive_terminal + S (mdr_p_cofactor_recursionbh) = S ((S ((S (mdr_q_cofactor_recursionbhs)))) * ff_v_mce_mdr_cofactor_recursionbhsf_positive)) /\ exists ff_q_mce_mdr_cofactor_recursionbhsf_positive_terminal. ff_u_mce_mdr_cofactor_recursionbhsf_positive = ff_q_mce_mdr_cofactor_recursionbhsf_positive_terminal * S ((S ((S (mdr_q_cofactor_recursionbhs)))) * ff_v_mce_mdr_cofactor_recursionbhsf_positive) + (mdr_p_cofactor_recursionbh))) /\ forall ff_i_mce_mdr_cofactor_recursionbhsf_positive. (exists ff_lt_mce_mdr_cofactor_recursionbhsf_positive_bound. ff_lt_mce_mdr_cofactor_recursionbhsf_positive_bound + S ff_i_mce_mdr_cofactor_recursionbhsf_positive = (S (mdr_q_cofactor_recursionbhs))) -> exists ff_a_mce_mdr_cofactor_recursionbhsf_positive ff_r_mce_mdr_cofactor_recursionbhsf_positive ff_s_mce_mdr_cofactor_recursionbhsf_positive. ((((exists ff_h_mce_mdr_cofactor_recursionbhsf_positive_summand. ff_h_mce_mdr_cofactor_recursionbhsf_positive_summand + S (ff_a_mce_mdr_cofactor_recursionbhsf_positive) = S ((S (ff_i_mce_mdr_cofactor_recursionbhsf_positive)) * ff_uc_mce_fold_mdr_cofactor_recursionbhsf)) /\ exists ff_q_mce_mdr_cofactor_recursionbhsf_positive_summand. ff_ub_mce_fold_mdr_cofactor_recursionbhsf = ff_q_mce_mdr_cofactor_recursionbhsf_positive_summand * S ((S (ff_i_mce_mdr_cofactor_recursionbhsf_positive)) * ff_uc_mce_fold_mdr_cofactor_recursionbhsf) + (ff_a_mce_mdr_cofactor_recursionbhsf_positive))) /\ ((((exists ff_h_mce_mdr_cofactor_recursionbhsf_positive_partial. ff_h_mce_mdr_cofactor_recursionbhsf_positive_partial + S (ff_r_mce_mdr_cofactor_recursionbhsf_positive) = S ((S (ff_i_mce_mdr_cofactor_recursionbhsf_positive)) * ff_v_mce_mdr_cofactor_recursionbhsf_positive)) /\ exists ff_q_mce_mdr_cofactor_recursionbhsf_positive_partial. ff_u_mce_mdr_cofactor_recursionbhsf_positive = ff_q_mce_mdr_cofactor_recursionbhsf_positive_partial * S ((S (ff_i_mce_mdr_cofactor_recursionbhsf_positive)) * ff_v_mce_mdr_cofactor_recursionbhsf_positive) + (ff_r_mce_mdr_cofactor_recursionbhsf_positive))) /\ ((((exists ff_h_mce_mdr_cofactor_recursionbhsf_positive_successor. ff_h_mce_mdr_cofactor_recursionbhsf_positive_successor + S (ff_s_mce_mdr_cofactor_recursionbhsf_positive) = S ((S (S ff_i_mce_mdr_cofactor_recursionbhsf_positive)) * ff_v_mce_mdr_cofactor_recursionbhsf_positive)) /\ exists ff_q_mce_mdr_cofactor_recursionbhsf_positive_successor. ff_u_mce_mdr_cofactor_recursionbhsf_positive = ff_q_mce_mdr_cofactor_recursionbhsf_positive_successor * S ((S (S ff_i_mce_mdr_cofactor_recursionbhsf_positive)) * ff_v_mce_mdr_cofactor_recursionbhsf_positive) + (ff_s_mce_mdr_cofactor_recursionbhsf_positive))) /\ ff_s_mce_mdr_cofactor_recursionbhsf_positive = ff_r_mce_mdr_cofactor_recursionbhsf_positive + ff_a_mce_mdr_cofactor_recursionbhsf_positive)))))) /\ (exists ff_u_mce_mdr_cofactor_recursionbhsf_negative ff_v_mce_mdr_cofactor_recursionbhsf_negative. ((((exists ff_h_mce_mdr_cofactor_recursionbhsf_negative_start. ff_h_mce_mdr_cofactor_recursionbhsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_cofactor_recursionbhsf_negative)) /\ exists ff_q_mce_mdr_cofactor_recursionbhsf_negative_start. ff_u_mce_mdr_cofactor_recursionbhsf_negative = ff_q_mce_mdr_cofactor_recursionbhsf_negative_start * S ((S (0)) * ff_v_mce_mdr_cofactor_recursionbhsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_cofactor_recursionbhsf_negative_terminal. ff_h_mce_mdr_cofactor_recursionbhsf_negative_terminal + S (mdr_n_cofactor_recursionbh) = S ((S ((S (mdr_q_cofactor_recursionbhs)))) * ff_v_mce_mdr_cofactor_recursionbhsf_negative)) /\ exists ff_q_mce_mdr_cofactor_recursionbhsf_negative_terminal. ff_u_mce_mdr_cofactor_recursionbhsf_negative = ff_q_mce_mdr_cofactor_recursionbhsf_negative_terminal * S ((S ((S (mdr_q_cofactor_recursionbhs)))) * ff_v_mce_mdr_cofactor_recursionbhsf_negative) + (mdr_n_cofactor_recursionbh))) /\ forall ff_i_mce_mdr_cofactor_recursionbhsf_negative. (exists ff_lt_mce_mdr_cofactor_recursionbhsf_negative_bound. ff_lt_mce_mdr_cofactor_recursionbhsf_negative_bound + S ff_i_mce_mdr_cofactor_recursionbhsf_negative = (S (mdr_q_cofactor_recursionbhs))) -> exists ff_a_mce_mdr_cofactor_recursionbhsf_negative ff_r_mce_mdr_cofactor_recursionbhsf_negative ff_s_mce_mdr_cofactor_recursionbhsf_negative. ((((exists ff_h_mce_mdr_cofactor_recursionbhsf_negative_summand. ff_h_mce_mdr_cofactor_recursionbhsf_negative_summand + S (ff_a_mce_mdr_cofactor_recursionbhsf_negative) = S ((S (ff_i_mce_mdr_cofactor_recursionbhsf_negative)) * ff_vc_mce_fold_mdr_cofactor_recursionbhsf)) /\ exists ff_q_mce_mdr_cofactor_recursionbhsf_negative_summand. ff_vb_mce_fold_mdr_cofactor_recursionbhsf = ff_q_mce_mdr_cofactor_recursionbhsf_negative_summand * S ((S (ff_i_mce_mdr_cofactor_recursionbhsf_negative)) * ff_vc_mce_fold_mdr_cofactor_recursionbhsf) + (ff_a_mce_mdr_cofactor_recursionbhsf_negative))) /\ ((((exists ff_h_mce_mdr_cofactor_recursionbhsf_negative_partial. ff_h_mce_mdr_cofactor_recursionbhsf_negative_partial + S (ff_r_mce_mdr_cofactor_recursionbhsf_negative) = S ((S (ff_i_mce_mdr_cofactor_recursionbhsf_negative)) * ff_v_mce_mdr_cofactor_recursionbhsf_negative)) /\ exists ff_q_mce_mdr_cofactor_recursionbhsf_negative_partial. ff_u_mce_mdr_cofactor_recursionbhsf_negative = ff_q_mce_mdr_cofactor_recursionbhsf_negative_partial * S ((S (ff_i_mce_mdr_cofactor_recursionbhsf_negative)) * ff_v_mce_mdr_cofactor_recursionbhsf_negative) + (ff_r_mce_mdr_cofactor_recursionbhsf_negative))) /\ ((((exists ff_h_mce_mdr_cofactor_recursionbhsf_negative_successor. ff_h_mce_mdr_cofactor_recursionbhsf_negative_successor + S (ff_s_mce_mdr_cofactor_recursionbhsf_negative) = S ((S (S ff_i_mce_mdr_cofactor_recursionbhsf_negative)) * ff_v_mce_mdr_cofactor_recursionbhsf_negative)) /\ exists ff_q_mce_mdr_cofactor_recursionbhsf_negative_successor. ff_u_mce_mdr_cofactor_recursionbhsf_negative = ff_q_mce_mdr_cofactor_recursionbhsf_negative_successor * S ((S (S ff_i_mce_mdr_cofactor_recursionbhsf_negative)) * ff_v_mce_mdr_cofactor_recursionbhsf_negative) + (ff_s_mce_mdr_cofactor_recursionbhsf_negative))) /\ ff_s_mce_mdr_cofactor_recursionbhsf_negative = ff_r_mce_mdr_cofactor_recursionbhsf_negative + ff_a_mce_mdr_cofactor_recursionbhsf_negative))))))))))))))) /\ ((exists mdr_gap_cofactor_recursionbi. mdr_gap_cofactor_recursionbi + S (mdr_i_cofactor_recursionb) = (mdr_l_cofactor_recursionb)) /\ (exists mdr_z_cofactor_recursionbr. ((exists mdr_a_cofactor_recursionbrc mdr_b_cofactor_recursionbrc mdr_c_cofactor_recursionbrc mdr_e_cofactor_recursionbrc mdr_f_cofactor_recursionbrc. ((mdr_a_cofactor_recursionbrc = ((q) + (mdr_qb_cofactor_recursion)) * S ((q) + (mdr_qb_cofactor_recursion)) + ((mdr_qb_cofactor_recursion) + (mdr_qb_cofactor_recursion))) /\ ((mdr_b_cofactor_recursionbrc = ((mdr_qc_cofactor_recursion) + (mdr_rb_cofactor_recursion)) * S ((mdr_qc_cofactor_recursion) + (mdr_rb_cofactor_recursion)) + ((mdr_rb_cofactor_recursion) + (mdr_rb_cofactor_recursion))) /\ ((mdr_c_cofactor_recursionbrc = ((mdr_a_cofactor_recursionbrc) + (mdr_b_cofactor_recursionbrc)) * S ((mdr_a_cofactor_recursionbrc) + (mdr_b_cofactor_recursionbrc)) + ((mdr_b_cofactor_recursionbrc) + (mdr_b_cofactor_recursionbrc))) /\ ((mdr_e_cofactor_recursionbrc = ((mdr_r_cofactor_recursion) + (mdr_s_cofactor_recursion)) * S ((mdr_r_cofactor_recursion) + (mdr_s_cofactor_recursion)) + ((mdr_s_cofactor_recursion) + (mdr_s_cofactor_recursion))) /\ ((mdr_f_cofactor_recursionbrc = ((mdr_rc_cofactor_recursion) + (mdr_e_cofactor_recursionbrc)) * S ((mdr_rc_cofactor_recursion) + (mdr_e_cofactor_recursionbrc)) + ((mdr_e_cofactor_recursionbrc) + (mdr_e_cofactor_recursionbrc))) /\ ((mdr_z_cofactor_recursionbr) = ((mdr_c_cofactor_recursionbrc) + (mdr_f_cofactor_recursionbrc)) * S ((mdr_c_cofactor_recursionbrc) + (mdr_f_cofactor_recursionbrc)) + ((mdr_f_cofactor_recursionbrc) + (mdr_f_cofactor_recursionbrc))))))))) /\ (((exists ff_h_mdr_cofactor_recursionbrb. ff_h_mdr_cofactor_recursionbrb + S (mdr_z_cofactor_recursionbr) = S ((S (mdr_i_cofactor_recursionb)) * mdr_c_cofactor_recursionb)) /\ exists ff_q_mdr_cofactor_recursionbrb. mdr_b_cofactor_recursionb = ff_q_mdr_cofactor_recursionbrb * S ((S (mdr_i_cofactor_recursionb)) * mdr_c_cofactor_recursionb) + (mdr_z_cofactor_recursionbr)))))))) -> mdr_p_cofactor_recursion = mdr_r_cofactor_recursion /\ mdr_n_cofactor_recursion = mdr_s_cofactor_recursion) -> (((forall mdr_i_cofactor_parentsp mdr_a_cofactor_parentsp. (exists mdr_gap_cofactor_parentspb. mdr_gap_cofactor_parentspb + S (mdr_i_cofactor_parentsp) = ((S q) * (S q))) -> (((exists ff_h_mdr_cofactor_parentspo. ff_h_mdr_cofactor_parentspo + S (mdr_a_cofactor_parentsp) = S ((S (mdr_i_cofactor_parentsp)) * pc)) /\ exists ff_q_mdr_cofactor_parentspo. pb = ff_q_mdr_cofactor_parentspo * S ((S (mdr_i_cofactor_parentsp)) * pc) + (mdr_a_cofactor_parentsp))) -> (((exists ff_h_mdr_cofactor_parentspn. ff_h_mdr_cofactor_parentspn + S (mdr_a_cofactor_parentsp) = S ((S (mdr_i_cofactor_parentsp)) * qc)) /\ exists ff_q_mdr_cofactor_parentspn. qb = ff_q_mdr_cofactor_parentspn * S ((S (mdr_i_cofactor_parentsp)) * qc) + (mdr_a_cofactor_parentsp)))) /\ (forall mdr_i_cofactor_parentsn mdr_a_cofactor_parentsn. (exists mdr_gap_cofactor_parentsnb. mdr_gap_cofactor_parentsnb + S (mdr_i_cofactor_parentsn) = ((S q) * (S q))) -> (((exists ff_h_mdr_cofactor_parentsno. ff_h_mdr_cofactor_parentsno + S (mdr_a_cofactor_parentsn) = S ((S (mdr_i_cofactor_parentsn)) * nc)) /\ exists ff_q_mdr_cofactor_parentsno. nb = ff_q_mdr_cofactor_parentsno * S ((S (mdr_i_cofactor_parentsn)) * nc) + (mdr_a_cofactor_parentsn))) -> (((exists ff_h_mdr_cofactor_parentsnn. ff_h_mdr_cofactor_parentsnn + S (mdr_a_cofactor_parentsn) = S ((S (mdr_i_cofactor_parentsn)) * rc)) /\ exists ff_q_mdr_cofactor_parentsnn. rb = ff_q_mdr_cofactor_parentsnn * S ((S (mdr_i_cofactor_parentsn)) * rc) + (mdr_a_cofactor_parentsn)))))) -> (forall mdr_j_cofactor_left. (exists mdr_gap_cofactor_leftj. mdr_gap_cofactor_leftj + S (mdr_j_cofactor_left) = (S (q))) -> exists mdr_up_cofactor_left mdr_us_cofactor_left mdr_un_cofactor_left mdr_ut_cofactor_left mdr_p_cofactor_left mdr_n_cofactor_left. ((((forall ff_index_mdm_prefix_mdr_cofactor_leftm_positive. (exists ff_gap_mdm_lt_mdr_cofactor_leftm_positive_index_bound. ff_gap_mdm_lt_mdr_cofactor_leftm_positive_index_bound + S (ff_index_mdm_prefix_mdr_cofactor_leftm_positive) = ((q) * (q))) -> exists ff_row_mdm_prefix_mdr_cofactor_leftm_positive ff_column_mdm_prefix_mdr_cofactor_leftm_positive ff_value_mdm_prefix_mdr_cofactor_leftm_positive. (ff_index_mdm_prefix_mdr_cofactor_leftm_positive = (q) * ff_row_mdm_prefix_mdr_cofactor_leftm_positive + ff_column_mdm_prefix_mdr_cofactor_leftm_positive /\ ((exists ff_gap_mdm_lt_mdr_cofactor_leftm_positive_column_bound. ff_gap_mdm_lt_mdr_cofactor_leftm_positive_column_bound + S (ff_column_mdm_prefix_mdr_cofactor_leftm_positive) = (q)) /\ ((exists ff_row_mdm_cell_mdr_cofactor_leftm_positive_cell ff_column_mdm_cell_mdr_cofactor_leftm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_cofactor_leftm_positive_cell_row_before. ff_gap_mdm_lt_mdr_cofactor_leftm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_cofactor_leftm_positive) = (0)) /\ ff_row_mdm_cell_mdr_cofactor_leftm_positive_cell = ff_row_mdm_prefix_mdr_cofactor_leftm_positive) \/ ((exists ff_gap_mdm_le_mdr_cofactor_leftm_positive_cell_row_after. ff_gap_mdm_le_mdr_cofactor_leftm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_cofactor_leftm_positive)) /\ ff_row_mdm_cell_mdr_cofactor_leftm_positive_cell = S ff_row_mdm_prefix_mdr_cofactor_leftm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_cofactor_leftm_positive_cell_column_before. ff_gap_mdm_lt_mdr_cofactor_leftm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_cofactor_leftm_positive) = (mdr_j_cofactor_left)) /\ ff_column_mdm_cell_mdr_cofactor_leftm_positive_cell = ff_column_mdm_prefix_mdr_cofactor_leftm_positive) \/ ((exists ff_gap_mdm_le_mdr_cofactor_leftm_positive_cell_column_after. ff_gap_mdm_le_mdr_cofactor_leftm_positive_cell_column_after + (mdr_j_cofactor_left) = (ff_column_mdm_prefix_mdr_cofactor_leftm_positive)) /\ ff_column_mdm_cell_mdr_cofactor_leftm_positive_cell = S ff_column_mdm_prefix_mdr_cofactor_leftm_positive))) /\ (((exists ff_h_mdm_mdr_cofactor_leftm_positive_cell_source. ff_h_mdm_mdr_cofactor_leftm_positive_cell_source + S (ff_value_mdm_prefix_mdr_cofactor_leftm_positive) = S ((S ((ff_row_mdm_cell_mdr_cofactor_leftm_positive_cell) * (S (q)) + (ff_column_mdm_cell_mdr_cofactor_leftm_positive_cell))) * pc)) /\ exists ff_q_mdm_mdr_cofactor_leftm_positive_cell_source. pb = ff_q_mdm_mdr_cofactor_leftm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_cofactor_leftm_positive_cell) * (S (q)) + (ff_column_mdm_cell_mdr_cofactor_leftm_positive_cell))) * pc) + (ff_value_mdm_prefix_mdr_cofactor_leftm_positive)))))) /\ (((exists ff_h_mdm_mdr_cofactor_leftm_positive_target. ff_h_mdm_mdr_cofactor_leftm_positive_target + S (ff_value_mdm_prefix_mdr_cofactor_leftm_positive) = S ((S (ff_index_mdm_prefix_mdr_cofactor_leftm_positive)) * mdr_us_cofactor_left)) /\ exists ff_q_mdm_mdr_cofactor_leftm_positive_target. mdr_up_cofactor_left = ff_q_mdm_mdr_cofactor_leftm_positive_target * S ((S (ff_index_mdm_prefix_mdr_cofactor_leftm_positive)) * mdr_us_cofactor_left) + (ff_value_mdm_prefix_mdr_cofactor_leftm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_cofactor_leftm_negative. (exists ff_gap_mdm_lt_mdr_cofactor_leftm_negative_index_bound. ff_gap_mdm_lt_mdr_cofactor_leftm_negative_index_bound + S (ff_index_mdm_prefix_mdr_cofactor_leftm_negative) = ((q) * (q))) -> exists ff_row_mdm_prefix_mdr_cofactor_leftm_negative ff_column_mdm_prefix_mdr_cofactor_leftm_negative ff_value_mdm_prefix_mdr_cofactor_leftm_negative. (ff_index_mdm_prefix_mdr_cofactor_leftm_negative = (q) * ff_row_mdm_prefix_mdr_cofactor_leftm_negative + ff_column_mdm_prefix_mdr_cofactor_leftm_negative /\ ((exists ff_gap_mdm_lt_mdr_cofactor_leftm_negative_column_bound. ff_gap_mdm_lt_mdr_cofactor_leftm_negative_column_bound + S (ff_column_mdm_prefix_mdr_cofactor_leftm_negative) = (q)) /\ ((exists ff_row_mdm_cell_mdr_cofactor_leftm_negative_cell ff_column_mdm_cell_mdr_cofactor_leftm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_cofactor_leftm_negative_cell_row_before. ff_gap_mdm_lt_mdr_cofactor_leftm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_cofactor_leftm_negative) = (0)) /\ ff_row_mdm_cell_mdr_cofactor_leftm_negative_cell = ff_row_mdm_prefix_mdr_cofactor_leftm_negative) \/ ((exists ff_gap_mdm_le_mdr_cofactor_leftm_negative_cell_row_after. ff_gap_mdm_le_mdr_cofactor_leftm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_cofactor_leftm_negative)) /\ ff_row_mdm_cell_mdr_cofactor_leftm_negative_cell = S ff_row_mdm_prefix_mdr_cofactor_leftm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_cofactor_leftm_negative_cell_column_before. ff_gap_mdm_lt_mdr_cofactor_leftm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_cofactor_leftm_negative) = (mdr_j_cofactor_left)) /\ ff_column_mdm_cell_mdr_cofactor_leftm_negative_cell = ff_column_mdm_prefix_mdr_cofactor_leftm_negative) \/ ((exists ff_gap_mdm_le_mdr_cofactor_leftm_negative_cell_column_after. ff_gap_mdm_le_mdr_cofactor_leftm_negative_cell_column_after + (mdr_j_cofactor_left) = (ff_column_mdm_prefix_mdr_cofactor_leftm_negative)) /\ ff_column_mdm_cell_mdr_cofactor_leftm_negative_cell = S ff_column_mdm_prefix_mdr_cofactor_leftm_negative))) /\ (((exists ff_h_mdm_mdr_cofactor_leftm_negative_cell_source. ff_h_mdm_mdr_cofactor_leftm_negative_cell_source + S (ff_value_mdm_prefix_mdr_cofactor_leftm_negative) = S ((S ((ff_row_mdm_cell_mdr_cofactor_leftm_negative_cell) * (S (q)) + (ff_column_mdm_cell_mdr_cofactor_leftm_negative_cell))) * nc)) /\ exists ff_q_mdm_mdr_cofactor_leftm_negative_cell_source. nb = ff_q_mdm_mdr_cofactor_leftm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_cofactor_leftm_negative_cell) * (S (q)) + (ff_column_mdm_cell_mdr_cofactor_leftm_negative_cell))) * nc) + (ff_value_mdm_prefix_mdr_cofactor_leftm_negative)))))) /\ (((exists ff_h_mdm_mdr_cofactor_leftm_negative_target. ff_h_mdm_mdr_cofactor_leftm_negative_target + S (ff_value_mdm_prefix_mdr_cofactor_leftm_negative) = S ((S (ff_index_mdm_prefix_mdr_cofactor_leftm_negative)) * mdr_ut_cofactor_left)) /\ exists ff_q_mdm_mdr_cofactor_leftm_negative_target. mdr_un_cofactor_left = ff_q_mdm_mdr_cofactor_leftm_negative_target * S ((S (ff_index_mdm_prefix_mdr_cofactor_leftm_negative)) * mdr_ut_cofactor_left) + (ff_value_mdm_prefix_mdr_cofactor_leftm_negative))))))))) /\ ((exists mdr_b_cofactor_leftd mdr_c_cofactor_leftd mdr_l_cofactor_leftd mdr_i_cofactor_leftd. ((forall mdr_i_cofactor_leftdh. (exists mdr_gap_cofactor_leftdhi. mdr_gap_cofactor_leftdhi + S (mdr_i_cofactor_leftdh) = (mdr_l_cofactor_leftd)) -> exists mdr_d_cofactor_leftdh mdr_pb_cofactor_leftdh mdr_pc_cofactor_leftdh mdr_nb_cofactor_leftdh mdr_nc_cofactor_leftdh mdr_p_cofactor_leftdh mdr_n_cofactor_leftdh. ((exists mdr_z_cofactor_leftdhr. ((exists mdr_a_cofactor_leftdhrc mdr_b_cofactor_leftdhrc mdr_c_cofactor_leftdhrc mdr_e_cofactor_leftdhrc mdr_f_cofactor_leftdhrc. ((mdr_a_cofactor_leftdhrc = ((mdr_d_cofactor_leftdh) + (mdr_pb_cofactor_leftdh)) * S ((mdr_d_cofactor_leftdh) + (mdr_pb_cofactor_leftdh)) + ((mdr_pb_cofactor_leftdh) + (mdr_pb_cofactor_leftdh))) /\ ((mdr_b_cofactor_leftdhrc = ((mdr_pc_cofactor_leftdh) + (mdr_nb_cofactor_leftdh)) * S ((mdr_pc_cofactor_leftdh) + (mdr_nb_cofactor_leftdh)) + ((mdr_nb_cofactor_leftdh) + (mdr_nb_cofactor_leftdh))) /\ ((mdr_c_cofactor_leftdhrc = ((mdr_a_cofactor_leftdhrc) + (mdr_b_cofactor_leftdhrc)) * S ((mdr_a_cofactor_leftdhrc) + (mdr_b_cofactor_leftdhrc)) + ((mdr_b_cofactor_leftdhrc) + (mdr_b_cofactor_leftdhrc))) /\ ((mdr_e_cofactor_leftdhrc = ((mdr_p_cofactor_leftdh) + (mdr_n_cofactor_leftdh)) * S ((mdr_p_cofactor_leftdh) + (mdr_n_cofactor_leftdh)) + ((mdr_n_cofactor_leftdh) + (mdr_n_cofactor_leftdh))) /\ ((mdr_f_cofactor_leftdhrc = ((mdr_nc_cofactor_leftdh) + (mdr_e_cofactor_leftdhrc)) * S ((mdr_nc_cofactor_leftdh) + (mdr_e_cofactor_leftdhrc)) + ((mdr_e_cofactor_leftdhrc) + (mdr_e_cofactor_leftdhrc))) /\ ((mdr_z_cofactor_leftdhr) = ((mdr_c_cofactor_leftdhrc) + (mdr_f_cofactor_leftdhrc)) * S ((mdr_c_cofactor_leftdhrc) + (mdr_f_cofactor_leftdhrc)) + ((mdr_f_cofactor_leftdhrc) + (mdr_f_cofactor_leftdhrc))))))))) /\ (((exists ff_h_mdr_cofactor_leftdhrb. ff_h_mdr_cofactor_leftdhrb + S (mdr_z_cofactor_leftdhr) = S ((S (mdr_i_cofactor_leftdh)) * mdr_c_cofactor_leftd)) /\ exists ff_q_mdr_cofactor_leftdhrb. mdr_b_cofactor_leftd = ff_q_mdr_cofactor_leftdhrb * S ((S (mdr_i_cofactor_leftdh)) * mdr_c_cofactor_leftd) + (mdr_z_cofactor_leftdhr))))) /\ (((((mdr_d_cofactor_leftdh) = 0) /\ (((mdr_p_cofactor_leftdh) = 1) /\ ((mdr_n_cofactor_leftdh) = 0))) \/ exists mdr_q_cofactor_leftdhs mdr_eb_cofactor_leftdhs mdr_ec_cofactor_leftdhs mdr_fb_cofactor_leftdhs mdr_fc_cofactor_leftdhs. (((mdr_d_cofactor_leftdh) = S (mdr_q_cofactor_leftdhs)) /\ ((forall mdr_j_cofactor_leftdhsc. (exists mdr_gap_cofactor_leftdhscj. mdr_gap_cofactor_leftdhscj + S (mdr_j_cofactor_leftdhsc) = (S (mdr_q_cofactor_leftdhs))) -> exists mdr_i_cofactor_leftdhsc mdr_up_cofactor_leftdhsc mdr_us_cofactor_leftdhsc mdr_un_cofactor_leftdhsc mdr_ut_cofactor_leftdhsc mdr_p_cofactor_leftdhsc mdr_n_cofactor_leftdhsc. ((exists mdr_gap_cofactor_leftdhsci. mdr_gap_cofactor_leftdhsci + S (mdr_i_cofactor_leftdhsc) = (mdr_i_cofactor_leftdh)) /\ ((exists mdr_z_cofactor_leftdhscr. ((exists mdr_a_cofactor_leftdhscrc mdr_b_cofactor_leftdhscrc mdr_c_cofactor_leftdhscrc mdr_e_cofactor_leftdhscrc mdr_f_cofactor_leftdhscrc. ((mdr_a_cofactor_leftdhscrc = ((mdr_q_cofactor_leftdhs) + (mdr_up_cofactor_leftdhsc)) * S ((mdr_q_cofactor_leftdhs) + (mdr_up_cofactor_leftdhsc)) + ((mdr_up_cofactor_leftdhsc) + (mdr_up_cofactor_leftdhsc))) /\ ((mdr_b_cofactor_leftdhscrc = ((mdr_us_cofactor_leftdhsc) + (mdr_un_cofactor_leftdhsc)) * S ((mdr_us_cofactor_leftdhsc) + (mdr_un_cofactor_leftdhsc)) + ((mdr_un_cofactor_leftdhsc) + (mdr_un_cofactor_leftdhsc))) /\ ((mdr_c_cofactor_leftdhscrc = ((mdr_a_cofactor_leftdhscrc) + (mdr_b_cofactor_leftdhscrc)) * S ((mdr_a_cofactor_leftdhscrc) + (mdr_b_cofactor_leftdhscrc)) + ((mdr_b_cofactor_leftdhscrc) + (mdr_b_cofactor_leftdhscrc))) /\ ((mdr_e_cofactor_leftdhscrc = ((mdr_p_cofactor_leftdhsc) + (mdr_n_cofactor_leftdhsc)) * S ((mdr_p_cofactor_leftdhsc) + (mdr_n_cofactor_leftdhsc)) + ((mdr_n_cofactor_leftdhsc) + (mdr_n_cofactor_leftdhsc))) /\ ((mdr_f_cofactor_leftdhscrc = ((mdr_ut_cofactor_leftdhsc) + (mdr_e_cofactor_leftdhscrc)) * S ((mdr_ut_cofactor_leftdhsc) + (mdr_e_cofactor_leftdhscrc)) + ((mdr_e_cofactor_leftdhscrc) + (mdr_e_cofactor_leftdhscrc))) /\ ((mdr_z_cofactor_leftdhscr) = ((mdr_c_cofactor_leftdhscrc) + (mdr_f_cofactor_leftdhscrc)) * S ((mdr_c_cofactor_leftdhscrc) + (mdr_f_cofactor_leftdhscrc)) + ((mdr_f_cofactor_leftdhscrc) + (mdr_f_cofactor_leftdhscrc))))))))) /\ (((exists ff_h_mdr_cofactor_leftdhscrb. ff_h_mdr_cofactor_leftdhscrb + S (mdr_z_cofactor_leftdhscr) = S ((S (mdr_i_cofactor_leftdhsc)) * mdr_c_cofactor_leftd)) /\ exists ff_q_mdr_cofactor_leftdhscrb. mdr_b_cofactor_leftd = ff_q_mdr_cofactor_leftdhscrb * S ((S (mdr_i_cofactor_leftdhsc)) * mdr_c_cofactor_leftd) + (mdr_z_cofactor_leftdhscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_cofactor_leftdhscm_positive. (exists ff_gap_mdm_lt_mdr_cofactor_leftdhscm_positive_index_bound. ff_gap_mdm_lt_mdr_cofactor_leftdhscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_cofactor_leftdhscm_positive) = ((mdr_q_cofactor_leftdhs) * (mdr_q_cofactor_leftdhs))) -> exists ff_row_mdm_prefix_mdr_cofactor_leftdhscm_positive ff_column_mdm_prefix_mdr_cofactor_leftdhscm_positive ff_value_mdm_prefix_mdr_cofactor_leftdhscm_positive. (ff_index_mdm_prefix_mdr_cofactor_leftdhscm_positive = (mdr_q_cofactor_leftdhs) * ff_row_mdm_prefix_mdr_cofactor_leftdhscm_positive + ff_column_mdm_prefix_mdr_cofactor_leftdhscm_positive /\ ((exists ff_gap_mdm_lt_mdr_cofactor_leftdhscm_positive_column_bound. ff_gap_mdm_lt_mdr_cofactor_leftdhscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_cofactor_leftdhscm_positive) = (mdr_q_cofactor_leftdhs)) /\ ((exists ff_row_mdm_cell_mdr_cofactor_leftdhscm_positive_cell ff_column_mdm_cell_mdr_cofactor_leftdhscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_cofactor_leftdhscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_cofactor_leftdhscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_cofactor_leftdhscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_cofactor_leftdhscm_positive_cell = ff_row_mdm_prefix_mdr_cofactor_leftdhscm_positive) \/ ((exists ff_gap_mdm_le_mdr_cofactor_leftdhscm_positive_cell_row_after. ff_gap_mdm_le_mdr_cofactor_leftdhscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_cofactor_leftdhscm_positive)) /\ ff_row_mdm_cell_mdr_cofactor_leftdhscm_positive_cell = S ff_row_mdm_prefix_mdr_cofactor_leftdhscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_cofactor_leftdhscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_cofactor_leftdhscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_cofactor_leftdhscm_positive) = (mdr_j_cofactor_leftdhsc)) /\ ff_column_mdm_cell_mdr_cofactor_leftdhscm_positive_cell = ff_column_mdm_prefix_mdr_cofactor_leftdhscm_positive) \/ ((exists ff_gap_mdm_le_mdr_cofactor_leftdhscm_positive_cell_column_after. ff_gap_mdm_le_mdr_cofactor_leftdhscm_positive_cell_column_after + (mdr_j_cofactor_leftdhsc) = (ff_column_mdm_prefix_mdr_cofactor_leftdhscm_positive)) /\ ff_column_mdm_cell_mdr_cofactor_leftdhscm_positive_cell = S ff_column_mdm_prefix_mdr_cofactor_leftdhscm_positive))) /\ (((exists ff_h_mdm_mdr_cofactor_leftdhscm_positive_cell_source. ff_h_mdm_mdr_cofactor_leftdhscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_cofactor_leftdhscm_positive) = S ((S ((ff_row_mdm_cell_mdr_cofactor_leftdhscm_positive_cell) * (S (mdr_q_cofactor_leftdhs)) + (ff_column_mdm_cell_mdr_cofactor_leftdhscm_positive_cell))) * mdr_pc_cofactor_leftdh)) /\ exists ff_q_mdm_mdr_cofactor_leftdhscm_positive_cell_source. mdr_pb_cofactor_leftdh = ff_q_mdm_mdr_cofactor_leftdhscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_cofactor_leftdhscm_positive_cell) * (S (mdr_q_cofactor_leftdhs)) + (ff_column_mdm_cell_mdr_cofactor_leftdhscm_positive_cell))) * mdr_pc_cofactor_leftdh) + (ff_value_mdm_prefix_mdr_cofactor_leftdhscm_positive)))))) /\ (((exists ff_h_mdm_mdr_cofactor_leftdhscm_positive_target. ff_h_mdm_mdr_cofactor_leftdhscm_positive_target + S (ff_value_mdm_prefix_mdr_cofactor_leftdhscm_positive) = S ((S (ff_index_mdm_prefix_mdr_cofactor_leftdhscm_positive)) * mdr_us_cofactor_leftdhsc)) /\ exists ff_q_mdm_mdr_cofactor_leftdhscm_positive_target. mdr_up_cofactor_leftdhsc = ff_q_mdm_mdr_cofactor_leftdhscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_cofactor_leftdhscm_positive)) * mdr_us_cofactor_leftdhsc) + (ff_value_mdm_prefix_mdr_cofactor_leftdhscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_cofactor_leftdhscm_negative. (exists ff_gap_mdm_lt_mdr_cofactor_leftdhscm_negative_index_bound. ff_gap_mdm_lt_mdr_cofactor_leftdhscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_cofactor_leftdhscm_negative) = ((mdr_q_cofactor_leftdhs) * (mdr_q_cofactor_leftdhs))) -> exists ff_row_mdm_prefix_mdr_cofactor_leftdhscm_negative ff_column_mdm_prefix_mdr_cofactor_leftdhscm_negative ff_value_mdm_prefix_mdr_cofactor_leftdhscm_negative. (ff_index_mdm_prefix_mdr_cofactor_leftdhscm_negative = (mdr_q_cofactor_leftdhs) * ff_row_mdm_prefix_mdr_cofactor_leftdhscm_negative + ff_column_mdm_prefix_mdr_cofactor_leftdhscm_negative /\ ((exists ff_gap_mdm_lt_mdr_cofactor_leftdhscm_negative_column_bound. ff_gap_mdm_lt_mdr_cofactor_leftdhscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_cofactor_leftdhscm_negative) = (mdr_q_cofactor_leftdhs)) /\ ((exists ff_row_mdm_cell_mdr_cofactor_leftdhscm_negative_cell ff_column_mdm_cell_mdr_cofactor_leftdhscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_cofactor_leftdhscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_cofactor_leftdhscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_cofactor_leftdhscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_cofactor_leftdhscm_negative_cell = ff_row_mdm_prefix_mdr_cofactor_leftdhscm_negative) \/ ((exists ff_gap_mdm_le_mdr_cofactor_leftdhscm_negative_cell_row_after. ff_gap_mdm_le_mdr_cofactor_leftdhscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_cofactor_leftdhscm_negative)) /\ ff_row_mdm_cell_mdr_cofactor_leftdhscm_negative_cell = S ff_row_mdm_prefix_mdr_cofactor_leftdhscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_cofactor_leftdhscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_cofactor_leftdhscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_cofactor_leftdhscm_negative) = (mdr_j_cofactor_leftdhsc)) /\ ff_column_mdm_cell_mdr_cofactor_leftdhscm_negative_cell = ff_column_mdm_prefix_mdr_cofactor_leftdhscm_negative) \/ ((exists ff_gap_mdm_le_mdr_cofactor_leftdhscm_negative_cell_column_after. ff_gap_mdm_le_mdr_cofactor_leftdhscm_negative_cell_column_after + (mdr_j_cofactor_leftdhsc) = (ff_column_mdm_prefix_mdr_cofactor_leftdhscm_negative)) /\ ff_column_mdm_cell_mdr_cofactor_leftdhscm_negative_cell = S ff_column_mdm_prefix_mdr_cofactor_leftdhscm_negative))) /\ (((exists ff_h_mdm_mdr_cofactor_leftdhscm_negative_cell_source. ff_h_mdm_mdr_cofactor_leftdhscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_cofactor_leftdhscm_negative) = S ((S ((ff_row_mdm_cell_mdr_cofactor_leftdhscm_negative_cell) * (S (mdr_q_cofactor_leftdhs)) + (ff_column_mdm_cell_mdr_cofactor_leftdhscm_negative_cell))) * mdr_nc_cofactor_leftdh)) /\ exists ff_q_mdm_mdr_cofactor_leftdhscm_negative_cell_source. mdr_nb_cofactor_leftdh = ff_q_mdm_mdr_cofactor_leftdhscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_cofactor_leftdhscm_negative_cell) * (S (mdr_q_cofactor_leftdhs)) + (ff_column_mdm_cell_mdr_cofactor_leftdhscm_negative_cell))) * mdr_nc_cofactor_leftdh) + (ff_value_mdm_prefix_mdr_cofactor_leftdhscm_negative)))))) /\ (((exists ff_h_mdm_mdr_cofactor_leftdhscm_negative_target. ff_h_mdm_mdr_cofactor_leftdhscm_negative_target + S (ff_value_mdm_prefix_mdr_cofactor_leftdhscm_negative) = S ((S (ff_index_mdm_prefix_mdr_cofactor_leftdhscm_negative)) * mdr_ut_cofactor_leftdhsc)) /\ exists ff_q_mdm_mdr_cofactor_leftdhscm_negative_target. mdr_un_cofactor_leftdhsc = ff_q_mdm_mdr_cofactor_leftdhscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_cofactor_leftdhscm_negative)) * mdr_ut_cofactor_leftdhsc) + (ff_value_mdm_prefix_mdr_cofactor_leftdhscm_negative))))))))) /\ ((((exists ff_h_mdr_cofactor_leftdhscp. ff_h_mdr_cofactor_leftdhscp + S (mdr_p_cofactor_leftdhsc) = S ((S (mdr_j_cofactor_leftdhsc)) * mdr_ec_cofactor_leftdhs)) /\ exists ff_q_mdr_cofactor_leftdhscp. mdr_eb_cofactor_leftdhs = ff_q_mdr_cofactor_leftdhscp * S ((S (mdr_j_cofactor_leftdhsc)) * mdr_ec_cofactor_leftdhs) + (mdr_p_cofactor_leftdhsc))) /\ (((exists ff_h_mdr_cofactor_leftdhscn. ff_h_mdr_cofactor_leftdhscn + S (mdr_n_cofactor_leftdhsc) = S ((S (mdr_j_cofactor_leftdhsc)) * mdr_fc_cofactor_leftdhs)) /\ exists ff_q_mdr_cofactor_leftdhscn. mdr_fb_cofactor_leftdhs = ff_q_mdr_cofactor_leftdhscn * S ((S (mdr_j_cofactor_leftdhsc)) * mdr_fc_cofactor_leftdhs) + (mdr_n_cofactor_leftdhsc)))))))) /\ (exists ff_ub_mce_fold_mdr_cofactor_leftdhsf ff_uc_mce_fold_mdr_cofactor_leftdhsf ff_vb_mce_fold_mdr_cofactor_leftdhsf ff_vc_mce_fold_mdr_cofactor_leftdhsf. ((forall ff_index_mce_alternating_mdr_cofactor_leftdhsf_prefix. (exists ff_gap_mce_mdr_cofactor_leftdhsf_prefix_index. ff_gap_mce_mdr_cofactor_leftdhsf_prefix_index + S (ff_index_mce_alternating_mdr_cofactor_leftdhsf_prefix) = (S (mdr_q_cofactor_leftdhs))) -> exists ff_ap_mce_alternating_mdr_cofactor_leftdhsf_prefix ff_an_mce_alternating_mdr_cofactor_leftdhsf_prefix ff_bp_mce_alternating_mdr_cofactor_leftdhsf_prefix ff_bn_mce_alternating_mdr_cofactor_leftdhsf_prefix ff_p_mce_alternating_mdr_cofactor_leftdhsf_prefix ff_n_mce_alternating_mdr_cofactor_leftdhsf_prefix. ((((exists ff_h_mce_mdr_cofactor_leftdhsf_prefix_ap. ff_h_mce_mdr_cofactor_leftdhsf_prefix_ap + S (ff_ap_mce_alternating_mdr_cofactor_leftdhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_cofactor_leftdhsf_prefix)) * mdr_pc_cofactor_leftdh)) /\ exists ff_q_mce_mdr_cofactor_leftdhsf_prefix_ap. mdr_pb_cofactor_leftdh = ff_q_mce_mdr_cofactor_leftdhsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_cofactor_leftdhsf_prefix)) * mdr_pc_cofactor_leftdh) + (ff_ap_mce_alternating_mdr_cofactor_leftdhsf_prefix))) /\ ((((exists ff_h_mce_mdr_cofactor_leftdhsf_prefix_an. ff_h_mce_mdr_cofactor_leftdhsf_prefix_an + S (ff_an_mce_alternating_mdr_cofactor_leftdhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_cofactor_leftdhsf_prefix)) * mdr_nc_cofactor_leftdh)) /\ exists ff_q_mce_mdr_cofactor_leftdhsf_prefix_an. mdr_nb_cofactor_leftdh = ff_q_mce_mdr_cofactor_leftdhsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_cofactor_leftdhsf_prefix)) * mdr_nc_cofactor_leftdh) + (ff_an_mce_alternating_mdr_cofactor_leftdhsf_prefix))) /\ ((((exists ff_h_mce_mdr_cofactor_leftdhsf_prefix_bp. ff_h_mce_mdr_cofactor_leftdhsf_prefix_bp + S (ff_bp_mce_alternating_mdr_cofactor_leftdhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_cofactor_leftdhsf_prefix)) * mdr_ec_cofactor_leftdhs)) /\ exists ff_q_mce_mdr_cofactor_leftdhsf_prefix_bp. mdr_eb_cofactor_leftdhs = ff_q_mce_mdr_cofactor_leftdhsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_cofactor_leftdhsf_prefix)) * mdr_ec_cofactor_leftdhs) + (ff_bp_mce_alternating_mdr_cofactor_leftdhsf_prefix))) /\ ((((exists ff_h_mce_mdr_cofactor_leftdhsf_prefix_bn. ff_h_mce_mdr_cofactor_leftdhsf_prefix_bn + S (ff_bn_mce_alternating_mdr_cofactor_leftdhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_cofactor_leftdhsf_prefix)) * mdr_fc_cofactor_leftdhs)) /\ exists ff_q_mce_mdr_cofactor_leftdhsf_prefix_bn. mdr_fb_cofactor_leftdhs = ff_q_mce_mdr_cofactor_leftdhsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_cofactor_leftdhsf_prefix)) * mdr_fc_cofactor_leftdhs) + (ff_bn_mce_alternating_mdr_cofactor_leftdhsf_prefix))) /\ ((((exists ff_h_mce_mdr_cofactor_leftdhsf_prefix_positive. ff_h_mce_mdr_cofactor_leftdhsf_prefix_positive + S (ff_p_mce_alternating_mdr_cofactor_leftdhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_cofactor_leftdhsf_prefix)) * ff_uc_mce_fold_mdr_cofactor_leftdhsf)) /\ exists ff_q_mce_mdr_cofactor_leftdhsf_prefix_positive. ff_ub_mce_fold_mdr_cofactor_leftdhsf = ff_q_mce_mdr_cofactor_leftdhsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_cofactor_leftdhsf_prefix)) * ff_uc_mce_fold_mdr_cofactor_leftdhsf) + (ff_p_mce_alternating_mdr_cofactor_leftdhsf_prefix))) /\ ((((exists ff_h_mce_mdr_cofactor_leftdhsf_prefix_negative. ff_h_mce_mdr_cofactor_leftdhsf_prefix_negative + S (ff_n_mce_alternating_mdr_cofactor_leftdhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_cofactor_leftdhsf_prefix)) * ff_vc_mce_fold_mdr_cofactor_leftdhsf)) /\ exists ff_q_mce_mdr_cofactor_leftdhsf_prefix_negative. ff_vb_mce_fold_mdr_cofactor_leftdhsf = ff_q_mce_mdr_cofactor_leftdhsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_cofactor_leftdhsf_prefix)) * ff_vc_mce_fold_mdr_cofactor_leftdhsf) + (ff_n_mce_alternating_mdr_cofactor_leftdhsf_prefix))) /\ (((exists ff_even_mce_term_mdr_cofactor_leftdhsf_prefix_term. ff_index_mce_alternating_mdr_cofactor_leftdhsf_prefix = 2 * ff_even_mce_term_mdr_cofactor_leftdhsf_prefix_term) /\ (ff_p_mce_alternating_mdr_cofactor_leftdhsf_prefix = (ff_ap_mce_alternating_mdr_cofactor_leftdhsf_prefix) * (ff_bp_mce_alternating_mdr_cofactor_leftdhsf_prefix) + (ff_an_mce_alternating_mdr_cofactor_leftdhsf_prefix) * (ff_bn_mce_alternating_mdr_cofactor_leftdhsf_prefix) /\ ff_n_mce_alternating_mdr_cofactor_leftdhsf_prefix = (ff_ap_mce_alternating_mdr_cofactor_leftdhsf_prefix) * (ff_bn_mce_alternating_mdr_cofactor_leftdhsf_prefix) + (ff_an_mce_alternating_mdr_cofactor_leftdhsf_prefix) * (ff_bp_mce_alternating_mdr_cofactor_leftdhsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_cofactor_leftdhsf_prefix_term. ff_index_mce_alternating_mdr_cofactor_leftdhsf_prefix = 2 * ff_odd_mce_term_mdr_cofactor_leftdhsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_cofactor_leftdhsf_prefix = (ff_ap_mce_alternating_mdr_cofactor_leftdhsf_prefix) * (ff_bn_mce_alternating_mdr_cofactor_leftdhsf_prefix) + (ff_an_mce_alternating_mdr_cofactor_leftdhsf_prefix) * (ff_bp_mce_alternating_mdr_cofactor_leftdhsf_prefix) /\ ff_n_mce_alternating_mdr_cofactor_leftdhsf_prefix = (ff_ap_mce_alternating_mdr_cofactor_leftdhsf_prefix) * (ff_bp_mce_alternating_mdr_cofactor_leftdhsf_prefix) + (ff_an_mce_alternating_mdr_cofactor_leftdhsf_prefix) * (ff_bn_mce_alternating_mdr_cofactor_leftdhsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_cofactor_leftdhsf_positive ff_v_mce_mdr_cofactor_leftdhsf_positive. ((((exists ff_h_mce_mdr_cofactor_leftdhsf_positive_start. ff_h_mce_mdr_cofactor_leftdhsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_cofactor_leftdhsf_positive)) /\ exists ff_q_mce_mdr_cofactor_leftdhsf_positive_start. ff_u_mce_mdr_cofactor_leftdhsf_positive = ff_q_mce_mdr_cofactor_leftdhsf_positive_start * S ((S (0)) * ff_v_mce_mdr_cofactor_leftdhsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_cofactor_leftdhsf_positive_terminal. ff_h_mce_mdr_cofactor_leftdhsf_positive_terminal + S (mdr_p_cofactor_leftdh) = S ((S ((S (mdr_q_cofactor_leftdhs)))) * ff_v_mce_mdr_cofactor_leftdhsf_positive)) /\ exists ff_q_mce_mdr_cofactor_leftdhsf_positive_terminal. ff_u_mce_mdr_cofactor_leftdhsf_positive = ff_q_mce_mdr_cofactor_leftdhsf_positive_terminal * S ((S ((S (mdr_q_cofactor_leftdhs)))) * ff_v_mce_mdr_cofactor_leftdhsf_positive) + (mdr_p_cofactor_leftdh))) /\ forall ff_i_mce_mdr_cofactor_leftdhsf_positive. (exists ff_lt_mce_mdr_cofactor_leftdhsf_positive_bound. ff_lt_mce_mdr_cofactor_leftdhsf_positive_bound + S ff_i_mce_mdr_cofactor_leftdhsf_positive = (S (mdr_q_cofactor_leftdhs))) -> exists ff_a_mce_mdr_cofactor_leftdhsf_positive ff_r_mce_mdr_cofactor_leftdhsf_positive ff_s_mce_mdr_cofactor_leftdhsf_positive. ((((exists ff_h_mce_mdr_cofactor_leftdhsf_positive_summand. ff_h_mce_mdr_cofactor_leftdhsf_positive_summand + S (ff_a_mce_mdr_cofactor_leftdhsf_positive) = S ((S (ff_i_mce_mdr_cofactor_leftdhsf_positive)) * ff_uc_mce_fold_mdr_cofactor_leftdhsf)) /\ exists ff_q_mce_mdr_cofactor_leftdhsf_positive_summand. ff_ub_mce_fold_mdr_cofactor_leftdhsf = ff_q_mce_mdr_cofactor_leftdhsf_positive_summand * S ((S (ff_i_mce_mdr_cofactor_leftdhsf_positive)) * ff_uc_mce_fold_mdr_cofactor_leftdhsf) + (ff_a_mce_mdr_cofactor_leftdhsf_positive))) /\ ((((exists ff_h_mce_mdr_cofactor_leftdhsf_positive_partial. ff_h_mce_mdr_cofactor_leftdhsf_positive_partial + S (ff_r_mce_mdr_cofactor_leftdhsf_positive) = S ((S (ff_i_mce_mdr_cofactor_leftdhsf_positive)) * ff_v_mce_mdr_cofactor_leftdhsf_positive)) /\ exists ff_q_mce_mdr_cofactor_leftdhsf_positive_partial. ff_u_mce_mdr_cofactor_leftdhsf_positive = ff_q_mce_mdr_cofactor_leftdhsf_positive_partial * S ((S (ff_i_mce_mdr_cofactor_leftdhsf_positive)) * ff_v_mce_mdr_cofactor_leftdhsf_positive) + (ff_r_mce_mdr_cofactor_leftdhsf_positive))) /\ ((((exists ff_h_mce_mdr_cofactor_leftdhsf_positive_successor. ff_h_mce_mdr_cofactor_leftdhsf_positive_successor + S (ff_s_mce_mdr_cofactor_leftdhsf_positive) = S ((S (S ff_i_mce_mdr_cofactor_leftdhsf_positive)) * ff_v_mce_mdr_cofactor_leftdhsf_positive)) /\ exists ff_q_mce_mdr_cofactor_leftdhsf_positive_successor. ff_u_mce_mdr_cofactor_leftdhsf_positive = ff_q_mce_mdr_cofactor_leftdhsf_positive_successor * S ((S (S ff_i_mce_mdr_cofactor_leftdhsf_positive)) * ff_v_mce_mdr_cofactor_leftdhsf_positive) + (ff_s_mce_mdr_cofactor_leftdhsf_positive))) /\ ff_s_mce_mdr_cofactor_leftdhsf_positive = ff_r_mce_mdr_cofactor_leftdhsf_positive + ff_a_mce_mdr_cofactor_leftdhsf_positive)))))) /\ (exists ff_u_mce_mdr_cofactor_leftdhsf_negative ff_v_mce_mdr_cofactor_leftdhsf_negative. ((((exists ff_h_mce_mdr_cofactor_leftdhsf_negative_start. ff_h_mce_mdr_cofactor_leftdhsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_cofactor_leftdhsf_negative)) /\ exists ff_q_mce_mdr_cofactor_leftdhsf_negative_start. ff_u_mce_mdr_cofactor_leftdhsf_negative = ff_q_mce_mdr_cofactor_leftdhsf_negative_start * S ((S (0)) * ff_v_mce_mdr_cofactor_leftdhsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_cofactor_leftdhsf_negative_terminal. ff_h_mce_mdr_cofactor_leftdhsf_negative_terminal + S (mdr_n_cofactor_leftdh) = S ((S ((S (mdr_q_cofactor_leftdhs)))) * ff_v_mce_mdr_cofactor_leftdhsf_negative)) /\ exists ff_q_mce_mdr_cofactor_leftdhsf_negative_terminal. ff_u_mce_mdr_cofactor_leftdhsf_negative = ff_q_mce_mdr_cofactor_leftdhsf_negative_terminal * S ((S ((S (mdr_q_cofactor_leftdhs)))) * ff_v_mce_mdr_cofactor_leftdhsf_negative) + (mdr_n_cofactor_leftdh))) /\ forall ff_i_mce_mdr_cofactor_leftdhsf_negative. (exists ff_lt_mce_mdr_cofactor_leftdhsf_negative_bound. ff_lt_mce_mdr_cofactor_leftdhsf_negative_bound + S ff_i_mce_mdr_cofactor_leftdhsf_negative = (S (mdr_q_cofactor_leftdhs))) -> exists ff_a_mce_mdr_cofactor_leftdhsf_negative ff_r_mce_mdr_cofactor_leftdhsf_negative ff_s_mce_mdr_cofactor_leftdhsf_negative. ((((exists ff_h_mce_mdr_cofactor_leftdhsf_negative_summand. ff_h_mce_mdr_cofactor_leftdhsf_negative_summand + S (ff_a_mce_mdr_cofactor_leftdhsf_negative) = S ((S (ff_i_mce_mdr_cofactor_leftdhsf_negative)) * ff_vc_mce_fold_mdr_cofactor_leftdhsf)) /\ exists ff_q_mce_mdr_cofactor_leftdhsf_negative_summand. ff_vb_mce_fold_mdr_cofactor_leftdhsf = ff_q_mce_mdr_cofactor_leftdhsf_negative_summand * S ((S (ff_i_mce_mdr_cofactor_leftdhsf_negative)) * ff_vc_mce_fold_mdr_cofactor_leftdhsf) + (ff_a_mce_mdr_cofactor_leftdhsf_negative))) /\ ((((exists ff_h_mce_mdr_cofactor_leftdhsf_negative_partial. ff_h_mce_mdr_cofactor_leftdhsf_negative_partial + S (ff_r_mce_mdr_cofactor_leftdhsf_negative) = S ((S (ff_i_mce_mdr_cofactor_leftdhsf_negative)) * ff_v_mce_mdr_cofactor_leftdhsf_negative)) /\ exists ff_q_mce_mdr_cofactor_leftdhsf_negative_partial. ff_u_mce_mdr_cofactor_leftdhsf_negative = ff_q_mce_mdr_cofactor_leftdhsf_negative_partial * S ((S (ff_i_mce_mdr_cofactor_leftdhsf_negative)) * ff_v_mce_mdr_cofactor_leftdhsf_negative) + (ff_r_mce_mdr_cofactor_leftdhsf_negative))) /\ ((((exists ff_h_mce_mdr_cofactor_leftdhsf_negative_successor. ff_h_mce_mdr_cofactor_leftdhsf_negative_successor + S (ff_s_mce_mdr_cofactor_leftdhsf_negative) = S ((S (S ff_i_mce_mdr_cofactor_leftdhsf_negative)) * ff_v_mce_mdr_cofactor_leftdhsf_negative)) /\ exists ff_q_mce_mdr_cofactor_leftdhsf_negative_successor. ff_u_mce_mdr_cofactor_leftdhsf_negative = ff_q_mce_mdr_cofactor_leftdhsf_negative_successor * S ((S (S ff_i_mce_mdr_cofactor_leftdhsf_negative)) * ff_v_mce_mdr_cofactor_leftdhsf_negative) + (ff_s_mce_mdr_cofactor_leftdhsf_negative))) /\ ff_s_mce_mdr_cofactor_leftdhsf_negative = ff_r_mce_mdr_cofactor_leftdhsf_negative + ff_a_mce_mdr_cofactor_leftdhsf_negative))))))))))))))) /\ ((exists mdr_gap_cofactor_leftdi. mdr_gap_cofactor_leftdi + S (mdr_i_cofactor_leftd) = (mdr_l_cofactor_leftd)) /\ (exists mdr_z_cofactor_leftdr. ((exists mdr_a_cofactor_leftdrc mdr_b_cofactor_leftdrc mdr_c_cofactor_leftdrc mdr_e_cofactor_leftdrc mdr_f_cofactor_leftdrc. ((mdr_a_cofactor_leftdrc = ((q) + (mdr_up_cofactor_left)) * S ((q) + (mdr_up_cofactor_left)) + ((mdr_up_cofactor_left) + (mdr_up_cofactor_left))) /\ ((mdr_b_cofactor_leftdrc = ((mdr_us_cofactor_left) + (mdr_un_cofactor_left)) * S ((mdr_us_cofactor_left) + (mdr_un_cofactor_left)) + ((mdr_un_cofactor_left) + (mdr_un_cofactor_left))) /\ ((mdr_c_cofactor_leftdrc = ((mdr_a_cofactor_leftdrc) + (mdr_b_cofactor_leftdrc)) * S ((mdr_a_cofactor_leftdrc) + (mdr_b_cofactor_leftdrc)) + ((mdr_b_cofactor_leftdrc) + (mdr_b_cofactor_leftdrc))) /\ ((mdr_e_cofactor_leftdrc = ((mdr_p_cofactor_left) + (mdr_n_cofactor_left)) * S ((mdr_p_cofactor_left) + (mdr_n_cofactor_left)) + ((mdr_n_cofactor_left) + (mdr_n_cofactor_left))) /\ ((mdr_f_cofactor_leftdrc = ((mdr_ut_cofactor_left) + (mdr_e_cofactor_leftdrc)) * S ((mdr_ut_cofactor_left) + (mdr_e_cofactor_leftdrc)) + ((mdr_e_cofactor_leftdrc) + (mdr_e_cofactor_leftdrc))) /\ ((mdr_z_cofactor_leftdr) = ((mdr_c_cofactor_leftdrc) + (mdr_f_cofactor_leftdrc)) * S ((mdr_c_cofactor_leftdrc) + (mdr_f_cofactor_leftdrc)) + ((mdr_f_cofactor_leftdrc) + (mdr_f_cofactor_leftdrc))))))))) /\ (((exists ff_h_mdr_cofactor_leftdrb. ff_h_mdr_cofactor_leftdrb + S (mdr_z_cofactor_leftdr) = S ((S (mdr_i_cofactor_leftd)) * mdr_c_cofactor_leftd)) /\ exists ff_q_mdr_cofactor_leftdrb. mdr_b_cofactor_leftd = ff_q_mdr_cofactor_leftdrb * S ((S (mdr_i_cofactor_leftd)) * mdr_c_cofactor_leftd) + (mdr_z_cofactor_leftdr)))))))) /\ ((((exists ff_h_mdr_cofactor_leftp. ff_h_mdr_cofactor_leftp + S (mdr_p_cofactor_left) = S ((S (mdr_j_cofactor_left)) * ec)) /\ exists ff_q_mdr_cofactor_leftp. eb = ff_q_mdr_cofactor_leftp * S ((S (mdr_j_cofactor_left)) * ec) + (mdr_p_cofactor_left))) /\ (((exists ff_h_mdr_cofactor_leftn. ff_h_mdr_cofactor_leftn + S (mdr_n_cofactor_left) = S ((S (mdr_j_cofactor_left)) * fc)) /\ exists ff_q_mdr_cofactor_leftn. fb = ff_q_mdr_cofactor_leftn * S ((S (mdr_j_cofactor_left)) * fc) + (mdr_n_cofactor_left))))))) -> (forall mdr_j_cofactor_right. (exists mdr_gap_cofactor_rightj. mdr_gap_cofactor_rightj + S (mdr_j_cofactor_right) = (S (q))) -> exists mdr_up_cofactor_right mdr_us_cofactor_right mdr_un_cofactor_right mdr_ut_cofactor_right mdr_p_cofactor_right mdr_n_cofactor_right. ((((forall ff_index_mdm_prefix_mdr_cofactor_rightm_positive. (exists ff_gap_mdm_lt_mdr_cofactor_rightm_positive_index_bound. ff_gap_mdm_lt_mdr_cofactor_rightm_positive_index_bound + S (ff_index_mdm_prefix_mdr_cofactor_rightm_positive) = ((q) * (q))) -> exists ff_row_mdm_prefix_mdr_cofactor_rightm_positive ff_column_mdm_prefix_mdr_cofactor_rightm_positive ff_value_mdm_prefix_mdr_cofactor_rightm_positive. (ff_index_mdm_prefix_mdr_cofactor_rightm_positive = (q) * ff_row_mdm_prefix_mdr_cofactor_rightm_positive + ff_column_mdm_prefix_mdr_cofactor_rightm_positive /\ ((exists ff_gap_mdm_lt_mdr_cofactor_rightm_positive_column_bound. ff_gap_mdm_lt_mdr_cofactor_rightm_positive_column_bound + S (ff_column_mdm_prefix_mdr_cofactor_rightm_positive) = (q)) /\ ((exists ff_row_mdm_cell_mdr_cofactor_rightm_positive_cell ff_column_mdm_cell_mdr_cofactor_rightm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_cofactor_rightm_positive_cell_row_before. ff_gap_mdm_lt_mdr_cofactor_rightm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_cofactor_rightm_positive) = (0)) /\ ff_row_mdm_cell_mdr_cofactor_rightm_positive_cell = ff_row_mdm_prefix_mdr_cofactor_rightm_positive) \/ ((exists ff_gap_mdm_le_mdr_cofactor_rightm_positive_cell_row_after. ff_gap_mdm_le_mdr_cofactor_rightm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_cofactor_rightm_positive)) /\ ff_row_mdm_cell_mdr_cofactor_rightm_positive_cell = S ff_row_mdm_prefix_mdr_cofactor_rightm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_cofactor_rightm_positive_cell_column_before. ff_gap_mdm_lt_mdr_cofactor_rightm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_cofactor_rightm_positive) = (mdr_j_cofactor_right)) /\ ff_column_mdm_cell_mdr_cofactor_rightm_positive_cell = ff_column_mdm_prefix_mdr_cofactor_rightm_positive) \/ ((exists ff_gap_mdm_le_mdr_cofactor_rightm_positive_cell_column_after. ff_gap_mdm_le_mdr_cofactor_rightm_positive_cell_column_after + (mdr_j_cofactor_right) = (ff_column_mdm_prefix_mdr_cofactor_rightm_positive)) /\ ff_column_mdm_cell_mdr_cofactor_rightm_positive_cell = S ff_column_mdm_prefix_mdr_cofactor_rightm_positive))) /\ (((exists ff_h_mdm_mdr_cofactor_rightm_positive_cell_source. ff_h_mdm_mdr_cofactor_rightm_positive_cell_source + S (ff_value_mdm_prefix_mdr_cofactor_rightm_positive) = S ((S ((ff_row_mdm_cell_mdr_cofactor_rightm_positive_cell) * (S (q)) + (ff_column_mdm_cell_mdr_cofactor_rightm_positive_cell))) * qc)) /\ exists ff_q_mdm_mdr_cofactor_rightm_positive_cell_source. qb = ff_q_mdm_mdr_cofactor_rightm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_cofactor_rightm_positive_cell) * (S (q)) + (ff_column_mdm_cell_mdr_cofactor_rightm_positive_cell))) * qc) + (ff_value_mdm_prefix_mdr_cofactor_rightm_positive)))))) /\ (((exists ff_h_mdm_mdr_cofactor_rightm_positive_target. ff_h_mdm_mdr_cofactor_rightm_positive_target + S (ff_value_mdm_prefix_mdr_cofactor_rightm_positive) = S ((S (ff_index_mdm_prefix_mdr_cofactor_rightm_positive)) * mdr_us_cofactor_right)) /\ exists ff_q_mdm_mdr_cofactor_rightm_positive_target. mdr_up_cofactor_right = ff_q_mdm_mdr_cofactor_rightm_positive_target * S ((S (ff_index_mdm_prefix_mdr_cofactor_rightm_positive)) * mdr_us_cofactor_right) + (ff_value_mdm_prefix_mdr_cofactor_rightm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_cofactor_rightm_negative. (exists ff_gap_mdm_lt_mdr_cofactor_rightm_negative_index_bound. ff_gap_mdm_lt_mdr_cofactor_rightm_negative_index_bound + S (ff_index_mdm_prefix_mdr_cofactor_rightm_negative) = ((q) * (q))) -> exists ff_row_mdm_prefix_mdr_cofactor_rightm_negative ff_column_mdm_prefix_mdr_cofactor_rightm_negative ff_value_mdm_prefix_mdr_cofactor_rightm_negative. (ff_index_mdm_prefix_mdr_cofactor_rightm_negative = (q) * ff_row_mdm_prefix_mdr_cofactor_rightm_negative + ff_column_mdm_prefix_mdr_cofactor_rightm_negative /\ ((exists ff_gap_mdm_lt_mdr_cofactor_rightm_negative_column_bound. ff_gap_mdm_lt_mdr_cofactor_rightm_negative_column_bound + S (ff_column_mdm_prefix_mdr_cofactor_rightm_negative) = (q)) /\ ((exists ff_row_mdm_cell_mdr_cofactor_rightm_negative_cell ff_column_mdm_cell_mdr_cofactor_rightm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_cofactor_rightm_negative_cell_row_before. ff_gap_mdm_lt_mdr_cofactor_rightm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_cofactor_rightm_negative) = (0)) /\ ff_row_mdm_cell_mdr_cofactor_rightm_negative_cell = ff_row_mdm_prefix_mdr_cofactor_rightm_negative) \/ ((exists ff_gap_mdm_le_mdr_cofactor_rightm_negative_cell_row_after. ff_gap_mdm_le_mdr_cofactor_rightm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_cofactor_rightm_negative)) /\ ff_row_mdm_cell_mdr_cofactor_rightm_negative_cell = S ff_row_mdm_prefix_mdr_cofactor_rightm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_cofactor_rightm_negative_cell_column_before. ff_gap_mdm_lt_mdr_cofactor_rightm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_cofactor_rightm_negative) = (mdr_j_cofactor_right)) /\ ff_column_mdm_cell_mdr_cofactor_rightm_negative_cell = ff_column_mdm_prefix_mdr_cofactor_rightm_negative) \/ ((exists ff_gap_mdm_le_mdr_cofactor_rightm_negative_cell_column_after. ff_gap_mdm_le_mdr_cofactor_rightm_negative_cell_column_after + (mdr_j_cofactor_right) = (ff_column_mdm_prefix_mdr_cofactor_rightm_negative)) /\ ff_column_mdm_cell_mdr_cofactor_rightm_negative_cell = S ff_column_mdm_prefix_mdr_cofactor_rightm_negative))) /\ (((exists ff_h_mdm_mdr_cofactor_rightm_negative_cell_source. ff_h_mdm_mdr_cofactor_rightm_negative_cell_source + S (ff_value_mdm_prefix_mdr_cofactor_rightm_negative) = S ((S ((ff_row_mdm_cell_mdr_cofactor_rightm_negative_cell) * (S (q)) + (ff_column_mdm_cell_mdr_cofactor_rightm_negative_cell))) * rc)) /\ exists ff_q_mdm_mdr_cofactor_rightm_negative_cell_source. rb = ff_q_mdm_mdr_cofactor_rightm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_cofactor_rightm_negative_cell) * (S (q)) + (ff_column_mdm_cell_mdr_cofactor_rightm_negative_cell))) * rc) + (ff_value_mdm_prefix_mdr_cofactor_rightm_negative)))))) /\ (((exists ff_h_mdm_mdr_cofactor_rightm_negative_target. ff_h_mdm_mdr_cofactor_rightm_negative_target + S (ff_value_mdm_prefix_mdr_cofactor_rightm_negative) = S ((S (ff_index_mdm_prefix_mdr_cofactor_rightm_negative)) * mdr_ut_cofactor_right)) /\ exists ff_q_mdm_mdr_cofactor_rightm_negative_target. mdr_un_cofactor_right = ff_q_mdm_mdr_cofactor_rightm_negative_target * S ((S (ff_index_mdm_prefix_mdr_cofactor_rightm_negative)) * mdr_ut_cofactor_right) + (ff_value_mdm_prefix_mdr_cofactor_rightm_negative))))))))) /\ ((exists mdr_b_cofactor_rightd mdr_c_cofactor_rightd mdr_l_cofactor_rightd mdr_i_cofactor_rightd. ((forall mdr_i_cofactor_rightdh. (exists mdr_gap_cofactor_rightdhi. mdr_gap_cofactor_rightdhi + S (mdr_i_cofactor_rightdh) = (mdr_l_cofactor_rightd)) -> exists mdr_d_cofactor_rightdh mdr_pb_cofactor_rightdh mdr_pc_cofactor_rightdh mdr_nb_cofactor_rightdh mdr_nc_cofactor_rightdh mdr_p_cofactor_rightdh mdr_n_cofactor_rightdh. ((exists mdr_z_cofactor_rightdhr. ((exists mdr_a_cofactor_rightdhrc mdr_b_cofactor_rightdhrc mdr_c_cofactor_rightdhrc mdr_e_cofactor_rightdhrc mdr_f_cofactor_rightdhrc. ((mdr_a_cofactor_rightdhrc = ((mdr_d_cofactor_rightdh) + (mdr_pb_cofactor_rightdh)) * S ((mdr_d_cofactor_rightdh) + (mdr_pb_cofactor_rightdh)) + ((mdr_pb_cofactor_rightdh) + (mdr_pb_cofactor_rightdh))) /\ ((mdr_b_cofactor_rightdhrc = ((mdr_pc_cofactor_rightdh) + (mdr_nb_cofactor_rightdh)) * S ((mdr_pc_cofactor_rightdh) + (mdr_nb_cofactor_rightdh)) + ((mdr_nb_cofactor_rightdh) + (mdr_nb_cofactor_rightdh))) /\ ((mdr_c_cofactor_rightdhrc = ((mdr_a_cofactor_rightdhrc) + (mdr_b_cofactor_rightdhrc)) * S ((mdr_a_cofactor_rightdhrc) + (mdr_b_cofactor_rightdhrc)) + ((mdr_b_cofactor_rightdhrc) + (mdr_b_cofactor_rightdhrc))) /\ ((mdr_e_cofactor_rightdhrc = ((mdr_p_cofactor_rightdh) + (mdr_n_cofactor_rightdh)) * S ((mdr_p_cofactor_rightdh) + (mdr_n_cofactor_rightdh)) + ((mdr_n_cofactor_rightdh) + (mdr_n_cofactor_rightdh))) /\ ((mdr_f_cofactor_rightdhrc = ((mdr_nc_cofactor_rightdh) + (mdr_e_cofactor_rightdhrc)) * S ((mdr_nc_cofactor_rightdh) + (mdr_e_cofactor_rightdhrc)) + ((mdr_e_cofactor_rightdhrc) + (mdr_e_cofactor_rightdhrc))) /\ ((mdr_z_cofactor_rightdhr) = ((mdr_c_cofactor_rightdhrc) + (mdr_f_cofactor_rightdhrc)) * S ((mdr_c_cofactor_rightdhrc) + (mdr_f_cofactor_rightdhrc)) + ((mdr_f_cofactor_rightdhrc) + (mdr_f_cofactor_rightdhrc))))))))) /\ (((exists ff_h_mdr_cofactor_rightdhrb. ff_h_mdr_cofactor_rightdhrb + S (mdr_z_cofactor_rightdhr) = S ((S (mdr_i_cofactor_rightdh)) * mdr_c_cofactor_rightd)) /\ exists ff_q_mdr_cofactor_rightdhrb. mdr_b_cofactor_rightd = ff_q_mdr_cofactor_rightdhrb * S ((S (mdr_i_cofactor_rightdh)) * mdr_c_cofactor_rightd) + (mdr_z_cofactor_rightdhr))))) /\ (((((mdr_d_cofactor_rightdh) = 0) /\ (((mdr_p_cofactor_rightdh) = 1) /\ ((mdr_n_cofactor_rightdh) = 0))) \/ exists mdr_q_cofactor_rightdhs mdr_eb_cofactor_rightdhs mdr_ec_cofactor_rightdhs mdr_fb_cofactor_rightdhs mdr_fc_cofactor_rightdhs. (((mdr_d_cofactor_rightdh) = S (mdr_q_cofactor_rightdhs)) /\ ((forall mdr_j_cofactor_rightdhsc. (exists mdr_gap_cofactor_rightdhscj. mdr_gap_cofactor_rightdhscj + S (mdr_j_cofactor_rightdhsc) = (S (mdr_q_cofactor_rightdhs))) -> exists mdr_i_cofactor_rightdhsc mdr_up_cofactor_rightdhsc mdr_us_cofactor_rightdhsc mdr_un_cofactor_rightdhsc mdr_ut_cofactor_rightdhsc mdr_p_cofactor_rightdhsc mdr_n_cofactor_rightdhsc. ((exists mdr_gap_cofactor_rightdhsci. mdr_gap_cofactor_rightdhsci + S (mdr_i_cofactor_rightdhsc) = (mdr_i_cofactor_rightdh)) /\ ((exists mdr_z_cofactor_rightdhscr. ((exists mdr_a_cofactor_rightdhscrc mdr_b_cofactor_rightdhscrc mdr_c_cofactor_rightdhscrc mdr_e_cofactor_rightdhscrc mdr_f_cofactor_rightdhscrc. ((mdr_a_cofactor_rightdhscrc = ((mdr_q_cofactor_rightdhs) + (mdr_up_cofactor_rightdhsc)) * S ((mdr_q_cofactor_rightdhs) + (mdr_up_cofactor_rightdhsc)) + ((mdr_up_cofactor_rightdhsc) + (mdr_up_cofactor_rightdhsc))) /\ ((mdr_b_cofactor_rightdhscrc = ((mdr_us_cofactor_rightdhsc) + (mdr_un_cofactor_rightdhsc)) * S ((mdr_us_cofactor_rightdhsc) + (mdr_un_cofactor_rightdhsc)) + ((mdr_un_cofactor_rightdhsc) + (mdr_un_cofactor_rightdhsc))) /\ ((mdr_c_cofactor_rightdhscrc = ((mdr_a_cofactor_rightdhscrc) + (mdr_b_cofactor_rightdhscrc)) * S ((mdr_a_cofactor_rightdhscrc) + (mdr_b_cofactor_rightdhscrc)) + ((mdr_b_cofactor_rightdhscrc) + (mdr_b_cofactor_rightdhscrc))) /\ ((mdr_e_cofactor_rightdhscrc = ((mdr_p_cofactor_rightdhsc) + (mdr_n_cofactor_rightdhsc)) * S ((mdr_p_cofactor_rightdhsc) + (mdr_n_cofactor_rightdhsc)) + ((mdr_n_cofactor_rightdhsc) + (mdr_n_cofactor_rightdhsc))) /\ ((mdr_f_cofactor_rightdhscrc = ((mdr_ut_cofactor_rightdhsc) + (mdr_e_cofactor_rightdhscrc)) * S ((mdr_ut_cofactor_rightdhsc) + (mdr_e_cofactor_rightdhscrc)) + ((mdr_e_cofactor_rightdhscrc) + (mdr_e_cofactor_rightdhscrc))) /\ ((mdr_z_cofactor_rightdhscr) = ((mdr_c_cofactor_rightdhscrc) + (mdr_f_cofactor_rightdhscrc)) * S ((mdr_c_cofactor_rightdhscrc) + (mdr_f_cofactor_rightdhscrc)) + ((mdr_f_cofactor_rightdhscrc) + (mdr_f_cofactor_rightdhscrc))))))))) /\ (((exists ff_h_mdr_cofactor_rightdhscrb. ff_h_mdr_cofactor_rightdhscrb + S (mdr_z_cofactor_rightdhscr) = S ((S (mdr_i_cofactor_rightdhsc)) * mdr_c_cofactor_rightd)) /\ exists ff_q_mdr_cofactor_rightdhscrb. mdr_b_cofactor_rightd = ff_q_mdr_cofactor_rightdhscrb * S ((S (mdr_i_cofactor_rightdhsc)) * mdr_c_cofactor_rightd) + (mdr_z_cofactor_rightdhscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_cofactor_rightdhscm_positive. (exists ff_gap_mdm_lt_mdr_cofactor_rightdhscm_positive_index_bound. ff_gap_mdm_lt_mdr_cofactor_rightdhscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_cofactor_rightdhscm_positive) = ((mdr_q_cofactor_rightdhs) * (mdr_q_cofactor_rightdhs))) -> exists ff_row_mdm_prefix_mdr_cofactor_rightdhscm_positive ff_column_mdm_prefix_mdr_cofactor_rightdhscm_positive ff_value_mdm_prefix_mdr_cofactor_rightdhscm_positive. (ff_index_mdm_prefix_mdr_cofactor_rightdhscm_positive = (mdr_q_cofactor_rightdhs) * ff_row_mdm_prefix_mdr_cofactor_rightdhscm_positive + ff_column_mdm_prefix_mdr_cofactor_rightdhscm_positive /\ ((exists ff_gap_mdm_lt_mdr_cofactor_rightdhscm_positive_column_bound. ff_gap_mdm_lt_mdr_cofactor_rightdhscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_cofactor_rightdhscm_positive) = (mdr_q_cofactor_rightdhs)) /\ ((exists ff_row_mdm_cell_mdr_cofactor_rightdhscm_positive_cell ff_column_mdm_cell_mdr_cofactor_rightdhscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_cofactor_rightdhscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_cofactor_rightdhscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_cofactor_rightdhscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_cofactor_rightdhscm_positive_cell = ff_row_mdm_prefix_mdr_cofactor_rightdhscm_positive) \/ ((exists ff_gap_mdm_le_mdr_cofactor_rightdhscm_positive_cell_row_after. ff_gap_mdm_le_mdr_cofactor_rightdhscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_cofactor_rightdhscm_positive)) /\ ff_row_mdm_cell_mdr_cofactor_rightdhscm_positive_cell = S ff_row_mdm_prefix_mdr_cofactor_rightdhscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_cofactor_rightdhscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_cofactor_rightdhscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_cofactor_rightdhscm_positive) = (mdr_j_cofactor_rightdhsc)) /\ ff_column_mdm_cell_mdr_cofactor_rightdhscm_positive_cell = ff_column_mdm_prefix_mdr_cofactor_rightdhscm_positive) \/ ((exists ff_gap_mdm_le_mdr_cofactor_rightdhscm_positive_cell_column_after. ff_gap_mdm_le_mdr_cofactor_rightdhscm_positive_cell_column_after + (mdr_j_cofactor_rightdhsc) = (ff_column_mdm_prefix_mdr_cofactor_rightdhscm_positive)) /\ ff_column_mdm_cell_mdr_cofactor_rightdhscm_positive_cell = S ff_column_mdm_prefix_mdr_cofactor_rightdhscm_positive))) /\ (((exists ff_h_mdm_mdr_cofactor_rightdhscm_positive_cell_source. ff_h_mdm_mdr_cofactor_rightdhscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_cofactor_rightdhscm_positive) = S ((S ((ff_row_mdm_cell_mdr_cofactor_rightdhscm_positive_cell) * (S (mdr_q_cofactor_rightdhs)) + (ff_column_mdm_cell_mdr_cofactor_rightdhscm_positive_cell))) * mdr_pc_cofactor_rightdh)) /\ exists ff_q_mdm_mdr_cofactor_rightdhscm_positive_cell_source. mdr_pb_cofactor_rightdh = ff_q_mdm_mdr_cofactor_rightdhscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_cofactor_rightdhscm_positive_cell) * (S (mdr_q_cofactor_rightdhs)) + (ff_column_mdm_cell_mdr_cofactor_rightdhscm_positive_cell))) * mdr_pc_cofactor_rightdh) + (ff_value_mdm_prefix_mdr_cofactor_rightdhscm_positive)))))) /\ (((exists ff_h_mdm_mdr_cofactor_rightdhscm_positive_target. ff_h_mdm_mdr_cofactor_rightdhscm_positive_target + S (ff_value_mdm_prefix_mdr_cofactor_rightdhscm_positive) = S ((S (ff_index_mdm_prefix_mdr_cofactor_rightdhscm_positive)) * mdr_us_cofactor_rightdhsc)) /\ exists ff_q_mdm_mdr_cofactor_rightdhscm_positive_target. mdr_up_cofactor_rightdhsc = ff_q_mdm_mdr_cofactor_rightdhscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_cofactor_rightdhscm_positive)) * mdr_us_cofactor_rightdhsc) + (ff_value_mdm_prefix_mdr_cofactor_rightdhscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_cofactor_rightdhscm_negative. (exists ff_gap_mdm_lt_mdr_cofactor_rightdhscm_negative_index_bound. ff_gap_mdm_lt_mdr_cofactor_rightdhscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_cofactor_rightdhscm_negative) = ((mdr_q_cofactor_rightdhs) * (mdr_q_cofactor_rightdhs))) -> exists ff_row_mdm_prefix_mdr_cofactor_rightdhscm_negative ff_column_mdm_prefix_mdr_cofactor_rightdhscm_negative ff_value_mdm_prefix_mdr_cofactor_rightdhscm_negative. (ff_index_mdm_prefix_mdr_cofactor_rightdhscm_negative = (mdr_q_cofactor_rightdhs) * ff_row_mdm_prefix_mdr_cofactor_rightdhscm_negative + ff_column_mdm_prefix_mdr_cofactor_rightdhscm_negative /\ ((exists ff_gap_mdm_lt_mdr_cofactor_rightdhscm_negative_column_bound. ff_gap_mdm_lt_mdr_cofactor_rightdhscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_cofactor_rightdhscm_negative) = (mdr_q_cofactor_rightdhs)) /\ ((exists ff_row_mdm_cell_mdr_cofactor_rightdhscm_negative_cell ff_column_mdm_cell_mdr_cofactor_rightdhscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_cofactor_rightdhscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_cofactor_rightdhscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_cofactor_rightdhscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_cofactor_rightdhscm_negative_cell = ff_row_mdm_prefix_mdr_cofactor_rightdhscm_negative) \/ ((exists ff_gap_mdm_le_mdr_cofactor_rightdhscm_negative_cell_row_after. ff_gap_mdm_le_mdr_cofactor_rightdhscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_cofactor_rightdhscm_negative)) /\ ff_row_mdm_cell_mdr_cofactor_rightdhscm_negative_cell = S ff_row_mdm_prefix_mdr_cofactor_rightdhscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_cofactor_rightdhscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_cofactor_rightdhscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_cofactor_rightdhscm_negative) = (mdr_j_cofactor_rightdhsc)) /\ ff_column_mdm_cell_mdr_cofactor_rightdhscm_negative_cell = ff_column_mdm_prefix_mdr_cofactor_rightdhscm_negative) \/ ((exists ff_gap_mdm_le_mdr_cofactor_rightdhscm_negative_cell_column_after. ff_gap_mdm_le_mdr_cofactor_rightdhscm_negative_cell_column_after + (mdr_j_cofactor_rightdhsc) = (ff_column_mdm_prefix_mdr_cofactor_rightdhscm_negative)) /\ ff_column_mdm_cell_mdr_cofactor_rightdhscm_negative_cell = S ff_column_mdm_prefix_mdr_cofactor_rightdhscm_negative))) /\ (((exists ff_h_mdm_mdr_cofactor_rightdhscm_negative_cell_source. ff_h_mdm_mdr_cofactor_rightdhscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_cofactor_rightdhscm_negative) = S ((S ((ff_row_mdm_cell_mdr_cofactor_rightdhscm_negative_cell) * (S (mdr_q_cofactor_rightdhs)) + (ff_column_mdm_cell_mdr_cofactor_rightdhscm_negative_cell))) * mdr_nc_cofactor_rightdh)) /\ exists ff_q_mdm_mdr_cofactor_rightdhscm_negative_cell_source. mdr_nb_cofactor_rightdh = ff_q_mdm_mdr_cofactor_rightdhscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_cofactor_rightdhscm_negative_cell) * (S (mdr_q_cofactor_rightdhs)) + (ff_column_mdm_cell_mdr_cofactor_rightdhscm_negative_cell))) * mdr_nc_cofactor_rightdh) + (ff_value_mdm_prefix_mdr_cofactor_rightdhscm_negative)))))) /\ (((exists ff_h_mdm_mdr_cofactor_rightdhscm_negative_target. ff_h_mdm_mdr_cofactor_rightdhscm_negative_target + S (ff_value_mdm_prefix_mdr_cofactor_rightdhscm_negative) = S ((S (ff_index_mdm_prefix_mdr_cofactor_rightdhscm_negative)) * mdr_ut_cofactor_rightdhsc)) /\ exists ff_q_mdm_mdr_cofactor_rightdhscm_negative_target. mdr_un_cofactor_rightdhsc = ff_q_mdm_mdr_cofactor_rightdhscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_cofactor_rightdhscm_negative)) * mdr_ut_cofactor_rightdhsc) + (ff_value_mdm_prefix_mdr_cofactor_rightdhscm_negative))))))))) /\ ((((exists ff_h_mdr_cofactor_rightdhscp. ff_h_mdr_cofactor_rightdhscp + S (mdr_p_cofactor_rightdhsc) = S ((S (mdr_j_cofactor_rightdhsc)) * mdr_ec_cofactor_rightdhs)) /\ exists ff_q_mdr_cofactor_rightdhscp. mdr_eb_cofactor_rightdhs = ff_q_mdr_cofactor_rightdhscp * S ((S (mdr_j_cofactor_rightdhsc)) * mdr_ec_cofactor_rightdhs) + (mdr_p_cofactor_rightdhsc))) /\ (((exists ff_h_mdr_cofactor_rightdhscn. ff_h_mdr_cofactor_rightdhscn + S (mdr_n_cofactor_rightdhsc) = S ((S (mdr_j_cofactor_rightdhsc)) * mdr_fc_cofactor_rightdhs)) /\ exists ff_q_mdr_cofactor_rightdhscn. mdr_fb_cofactor_rightdhs = ff_q_mdr_cofactor_rightdhscn * S ((S (mdr_j_cofactor_rightdhsc)) * mdr_fc_cofactor_rightdhs) + (mdr_n_cofactor_rightdhsc)))))))) /\ (exists ff_ub_mce_fold_mdr_cofactor_rightdhsf ff_uc_mce_fold_mdr_cofactor_rightdhsf ff_vb_mce_fold_mdr_cofactor_rightdhsf ff_vc_mce_fold_mdr_cofactor_rightdhsf. ((forall ff_index_mce_alternating_mdr_cofactor_rightdhsf_prefix. (exists ff_gap_mce_mdr_cofactor_rightdhsf_prefix_index. ff_gap_mce_mdr_cofactor_rightdhsf_prefix_index + S (ff_index_mce_alternating_mdr_cofactor_rightdhsf_prefix) = (S (mdr_q_cofactor_rightdhs))) -> exists ff_ap_mce_alternating_mdr_cofactor_rightdhsf_prefix ff_an_mce_alternating_mdr_cofactor_rightdhsf_prefix ff_bp_mce_alternating_mdr_cofactor_rightdhsf_prefix ff_bn_mce_alternating_mdr_cofactor_rightdhsf_prefix ff_p_mce_alternating_mdr_cofactor_rightdhsf_prefix ff_n_mce_alternating_mdr_cofactor_rightdhsf_prefix. ((((exists ff_h_mce_mdr_cofactor_rightdhsf_prefix_ap. ff_h_mce_mdr_cofactor_rightdhsf_prefix_ap + S (ff_ap_mce_alternating_mdr_cofactor_rightdhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_cofactor_rightdhsf_prefix)) * mdr_pc_cofactor_rightdh)) /\ exists ff_q_mce_mdr_cofactor_rightdhsf_prefix_ap. mdr_pb_cofactor_rightdh = ff_q_mce_mdr_cofactor_rightdhsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_cofactor_rightdhsf_prefix)) * mdr_pc_cofactor_rightdh) + (ff_ap_mce_alternating_mdr_cofactor_rightdhsf_prefix))) /\ ((((exists ff_h_mce_mdr_cofactor_rightdhsf_prefix_an. ff_h_mce_mdr_cofactor_rightdhsf_prefix_an + S (ff_an_mce_alternating_mdr_cofactor_rightdhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_cofactor_rightdhsf_prefix)) * mdr_nc_cofactor_rightdh)) /\ exists ff_q_mce_mdr_cofactor_rightdhsf_prefix_an. mdr_nb_cofactor_rightdh = ff_q_mce_mdr_cofactor_rightdhsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_cofactor_rightdhsf_prefix)) * mdr_nc_cofactor_rightdh) + (ff_an_mce_alternating_mdr_cofactor_rightdhsf_prefix))) /\ ((((exists ff_h_mce_mdr_cofactor_rightdhsf_prefix_bp. ff_h_mce_mdr_cofactor_rightdhsf_prefix_bp + S (ff_bp_mce_alternating_mdr_cofactor_rightdhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_cofactor_rightdhsf_prefix)) * mdr_ec_cofactor_rightdhs)) /\ exists ff_q_mce_mdr_cofactor_rightdhsf_prefix_bp. mdr_eb_cofactor_rightdhs = ff_q_mce_mdr_cofactor_rightdhsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_cofactor_rightdhsf_prefix)) * mdr_ec_cofactor_rightdhs) + (ff_bp_mce_alternating_mdr_cofactor_rightdhsf_prefix))) /\ ((((exists ff_h_mce_mdr_cofactor_rightdhsf_prefix_bn. ff_h_mce_mdr_cofactor_rightdhsf_prefix_bn + S (ff_bn_mce_alternating_mdr_cofactor_rightdhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_cofactor_rightdhsf_prefix)) * mdr_fc_cofactor_rightdhs)) /\ exists ff_q_mce_mdr_cofactor_rightdhsf_prefix_bn. mdr_fb_cofactor_rightdhs = ff_q_mce_mdr_cofactor_rightdhsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_cofactor_rightdhsf_prefix)) * mdr_fc_cofactor_rightdhs) + (ff_bn_mce_alternating_mdr_cofactor_rightdhsf_prefix))) /\ ((((exists ff_h_mce_mdr_cofactor_rightdhsf_prefix_positive. ff_h_mce_mdr_cofactor_rightdhsf_prefix_positive + S (ff_p_mce_alternating_mdr_cofactor_rightdhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_cofactor_rightdhsf_prefix)) * ff_uc_mce_fold_mdr_cofactor_rightdhsf)) /\ exists ff_q_mce_mdr_cofactor_rightdhsf_prefix_positive. ff_ub_mce_fold_mdr_cofactor_rightdhsf = ff_q_mce_mdr_cofactor_rightdhsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_cofactor_rightdhsf_prefix)) * ff_uc_mce_fold_mdr_cofactor_rightdhsf) + (ff_p_mce_alternating_mdr_cofactor_rightdhsf_prefix))) /\ ((((exists ff_h_mce_mdr_cofactor_rightdhsf_prefix_negative. ff_h_mce_mdr_cofactor_rightdhsf_prefix_negative + S (ff_n_mce_alternating_mdr_cofactor_rightdhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_cofactor_rightdhsf_prefix)) * ff_vc_mce_fold_mdr_cofactor_rightdhsf)) /\ exists ff_q_mce_mdr_cofactor_rightdhsf_prefix_negative. ff_vb_mce_fold_mdr_cofactor_rightdhsf = ff_q_mce_mdr_cofactor_rightdhsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_cofactor_rightdhsf_prefix)) * ff_vc_mce_fold_mdr_cofactor_rightdhsf) + (ff_n_mce_alternating_mdr_cofactor_rightdhsf_prefix))) /\ (((exists ff_even_mce_term_mdr_cofactor_rightdhsf_prefix_term. ff_index_mce_alternating_mdr_cofactor_rightdhsf_prefix = 2 * ff_even_mce_term_mdr_cofactor_rightdhsf_prefix_term) /\ (ff_p_mce_alternating_mdr_cofactor_rightdhsf_prefix = (ff_ap_mce_alternating_mdr_cofactor_rightdhsf_prefix) * (ff_bp_mce_alternating_mdr_cofactor_rightdhsf_prefix) + (ff_an_mce_alternating_mdr_cofactor_rightdhsf_prefix) * (ff_bn_mce_alternating_mdr_cofactor_rightdhsf_prefix) /\ ff_n_mce_alternating_mdr_cofactor_rightdhsf_prefix = (ff_ap_mce_alternating_mdr_cofactor_rightdhsf_prefix) * (ff_bn_mce_alternating_mdr_cofactor_rightdhsf_prefix) + (ff_an_mce_alternating_mdr_cofactor_rightdhsf_prefix) * (ff_bp_mce_alternating_mdr_cofactor_rightdhsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_cofactor_rightdhsf_prefix_term. ff_index_mce_alternating_mdr_cofactor_rightdhsf_prefix = 2 * ff_odd_mce_term_mdr_cofactor_rightdhsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_cofactor_rightdhsf_prefix = (ff_ap_mce_alternating_mdr_cofactor_rightdhsf_prefix) * (ff_bn_mce_alternating_mdr_cofactor_rightdhsf_prefix) + (ff_an_mce_alternating_mdr_cofactor_rightdhsf_prefix) * (ff_bp_mce_alternating_mdr_cofactor_rightdhsf_prefix) /\ ff_n_mce_alternating_mdr_cofactor_rightdhsf_prefix = (ff_ap_mce_alternating_mdr_cofactor_rightdhsf_prefix) * (ff_bp_mce_alternating_mdr_cofactor_rightdhsf_prefix) + (ff_an_mce_alternating_mdr_cofactor_rightdhsf_prefix) * (ff_bn_mce_alternating_mdr_cofactor_rightdhsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_cofactor_rightdhsf_positive ff_v_mce_mdr_cofactor_rightdhsf_positive. ((((exists ff_h_mce_mdr_cofactor_rightdhsf_positive_start. ff_h_mce_mdr_cofactor_rightdhsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_cofactor_rightdhsf_positive)) /\ exists ff_q_mce_mdr_cofactor_rightdhsf_positive_start. ff_u_mce_mdr_cofactor_rightdhsf_positive = ff_q_mce_mdr_cofactor_rightdhsf_positive_start * S ((S (0)) * ff_v_mce_mdr_cofactor_rightdhsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_cofactor_rightdhsf_positive_terminal. ff_h_mce_mdr_cofactor_rightdhsf_positive_terminal + S (mdr_p_cofactor_rightdh) = S ((S ((S (mdr_q_cofactor_rightdhs)))) * ff_v_mce_mdr_cofactor_rightdhsf_positive)) /\ exists ff_q_mce_mdr_cofactor_rightdhsf_positive_terminal. ff_u_mce_mdr_cofactor_rightdhsf_positive = ff_q_mce_mdr_cofactor_rightdhsf_positive_terminal * S ((S ((S (mdr_q_cofactor_rightdhs)))) * ff_v_mce_mdr_cofactor_rightdhsf_positive) + (mdr_p_cofactor_rightdh))) /\ forall ff_i_mce_mdr_cofactor_rightdhsf_positive. (exists ff_lt_mce_mdr_cofactor_rightdhsf_positive_bound. ff_lt_mce_mdr_cofactor_rightdhsf_positive_bound + S ff_i_mce_mdr_cofactor_rightdhsf_positive = (S (mdr_q_cofactor_rightdhs))) -> exists ff_a_mce_mdr_cofactor_rightdhsf_positive ff_r_mce_mdr_cofactor_rightdhsf_positive ff_s_mce_mdr_cofactor_rightdhsf_positive. ((((exists ff_h_mce_mdr_cofactor_rightdhsf_positive_summand. ff_h_mce_mdr_cofactor_rightdhsf_positive_summand + S (ff_a_mce_mdr_cofactor_rightdhsf_positive) = S ((S (ff_i_mce_mdr_cofactor_rightdhsf_positive)) * ff_uc_mce_fold_mdr_cofactor_rightdhsf)) /\ exists ff_q_mce_mdr_cofactor_rightdhsf_positive_summand. ff_ub_mce_fold_mdr_cofactor_rightdhsf = ff_q_mce_mdr_cofactor_rightdhsf_positive_summand * S ((S (ff_i_mce_mdr_cofactor_rightdhsf_positive)) * ff_uc_mce_fold_mdr_cofactor_rightdhsf) + (ff_a_mce_mdr_cofactor_rightdhsf_positive))) /\ ((((exists ff_h_mce_mdr_cofactor_rightdhsf_positive_partial. ff_h_mce_mdr_cofactor_rightdhsf_positive_partial + S (ff_r_mce_mdr_cofactor_rightdhsf_positive) = S ((S (ff_i_mce_mdr_cofactor_rightdhsf_positive)) * ff_v_mce_mdr_cofactor_rightdhsf_positive)) /\ exists ff_q_mce_mdr_cofactor_rightdhsf_positive_partial. ff_u_mce_mdr_cofactor_rightdhsf_positive = ff_q_mce_mdr_cofactor_rightdhsf_positive_partial * S ((S (ff_i_mce_mdr_cofactor_rightdhsf_positive)) * ff_v_mce_mdr_cofactor_rightdhsf_positive) + (ff_r_mce_mdr_cofactor_rightdhsf_positive))) /\ ((((exists ff_h_mce_mdr_cofactor_rightdhsf_positive_successor. ff_h_mce_mdr_cofactor_rightdhsf_positive_successor + S (ff_s_mce_mdr_cofactor_rightdhsf_positive) = S ((S (S ff_i_mce_mdr_cofactor_rightdhsf_positive)) * ff_v_mce_mdr_cofactor_rightdhsf_positive)) /\ exists ff_q_mce_mdr_cofactor_rightdhsf_positive_successor. ff_u_mce_mdr_cofactor_rightdhsf_positive = ff_q_mce_mdr_cofactor_rightdhsf_positive_successor * S ((S (S ff_i_mce_mdr_cofactor_rightdhsf_positive)) * ff_v_mce_mdr_cofactor_rightdhsf_positive) + (ff_s_mce_mdr_cofactor_rightdhsf_positive))) /\ ff_s_mce_mdr_cofactor_rightdhsf_positive = ff_r_mce_mdr_cofactor_rightdhsf_positive + ff_a_mce_mdr_cofactor_rightdhsf_positive)))))) /\ (exists ff_u_mce_mdr_cofactor_rightdhsf_negative ff_v_mce_mdr_cofactor_rightdhsf_negative. ((((exists ff_h_mce_mdr_cofactor_rightdhsf_negative_start. ff_h_mce_mdr_cofactor_rightdhsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_cofactor_rightdhsf_negative)) /\ exists ff_q_mce_mdr_cofactor_rightdhsf_negative_start. ff_u_mce_mdr_cofactor_rightdhsf_negative = ff_q_mce_mdr_cofactor_rightdhsf_negative_start * S ((S (0)) * ff_v_mce_mdr_cofactor_rightdhsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_cofactor_rightdhsf_negative_terminal. ff_h_mce_mdr_cofactor_rightdhsf_negative_terminal + S (mdr_n_cofactor_rightdh) = S ((S ((S (mdr_q_cofactor_rightdhs)))) * ff_v_mce_mdr_cofactor_rightdhsf_negative)) /\ exists ff_q_mce_mdr_cofactor_rightdhsf_negative_terminal. ff_u_mce_mdr_cofactor_rightdhsf_negative = ff_q_mce_mdr_cofactor_rightdhsf_negative_terminal * S ((S ((S (mdr_q_cofactor_rightdhs)))) * ff_v_mce_mdr_cofactor_rightdhsf_negative) + (mdr_n_cofactor_rightdh))) /\ forall ff_i_mce_mdr_cofactor_rightdhsf_negative. (exists ff_lt_mce_mdr_cofactor_rightdhsf_negative_bound. ff_lt_mce_mdr_cofactor_rightdhsf_negative_bound + S ff_i_mce_mdr_cofactor_rightdhsf_negative = (S (mdr_q_cofactor_rightdhs))) -> exists ff_a_mce_mdr_cofactor_rightdhsf_negative ff_r_mce_mdr_cofactor_rightdhsf_negative ff_s_mce_mdr_cofactor_rightdhsf_negative. ((((exists ff_h_mce_mdr_cofactor_rightdhsf_negative_summand. ff_h_mce_mdr_cofactor_rightdhsf_negative_summand + S (ff_a_mce_mdr_cofactor_rightdhsf_negative) = S ((S (ff_i_mce_mdr_cofactor_rightdhsf_negative)) * ff_vc_mce_fold_mdr_cofactor_rightdhsf)) /\ exists ff_q_mce_mdr_cofactor_rightdhsf_negative_summand. ff_vb_mce_fold_mdr_cofactor_rightdhsf = ff_q_mce_mdr_cofactor_rightdhsf_negative_summand * S ((S (ff_i_mce_mdr_cofactor_rightdhsf_negative)) * ff_vc_mce_fold_mdr_cofactor_rightdhsf) + (ff_a_mce_mdr_cofactor_rightdhsf_negative))) /\ ((((exists ff_h_mce_mdr_cofactor_rightdhsf_negative_partial. ff_h_mce_mdr_cofactor_rightdhsf_negative_partial + S (ff_r_mce_mdr_cofactor_rightdhsf_negative) = S ((S (ff_i_mce_mdr_cofactor_rightdhsf_negative)) * ff_v_mce_mdr_cofactor_rightdhsf_negative)) /\ exists ff_q_mce_mdr_cofactor_rightdhsf_negative_partial. ff_u_mce_mdr_cofactor_rightdhsf_negative = ff_q_mce_mdr_cofactor_rightdhsf_negative_partial * S ((S (ff_i_mce_mdr_cofactor_rightdhsf_negative)) * ff_v_mce_mdr_cofactor_rightdhsf_negative) + (ff_r_mce_mdr_cofactor_rightdhsf_negative))) /\ ((((exists ff_h_mce_mdr_cofactor_rightdhsf_negative_successor. ff_h_mce_mdr_cofactor_rightdhsf_negative_successor + S (ff_s_mce_mdr_cofactor_rightdhsf_negative) = S ((S (S ff_i_mce_mdr_cofactor_rightdhsf_negative)) * ff_v_mce_mdr_cofactor_rightdhsf_negative)) /\ exists ff_q_mce_mdr_cofactor_rightdhsf_negative_successor. ff_u_mce_mdr_cofactor_rightdhsf_negative = ff_q_mce_mdr_cofactor_rightdhsf_negative_successor * S ((S (S ff_i_mce_mdr_cofactor_rightdhsf_negative)) * ff_v_mce_mdr_cofactor_rightdhsf_negative) + (ff_s_mce_mdr_cofactor_rightdhsf_negative))) /\ ff_s_mce_mdr_cofactor_rightdhsf_negative = ff_r_mce_mdr_cofactor_rightdhsf_negative + ff_a_mce_mdr_cofactor_rightdhsf_negative))))))))))))))) /\ ((exists mdr_gap_cofactor_rightdi. mdr_gap_cofactor_rightdi + S (mdr_i_cofactor_rightd) = (mdr_l_cofactor_rightd)) /\ (exists mdr_z_cofactor_rightdr. ((exists mdr_a_cofactor_rightdrc mdr_b_cofactor_rightdrc mdr_c_cofactor_rightdrc mdr_e_cofactor_rightdrc mdr_f_cofactor_rightdrc. ((mdr_a_cofactor_rightdrc = ((q) + (mdr_up_cofactor_right)) * S ((q) + (mdr_up_cofactor_right)) + ((mdr_up_cofactor_right) + (mdr_up_cofactor_right))) /\ ((mdr_b_cofactor_rightdrc = ((mdr_us_cofactor_right) + (mdr_un_cofactor_right)) * S ((mdr_us_cofactor_right) + (mdr_un_cofactor_right)) + ((mdr_un_cofactor_right) + (mdr_un_cofactor_right))) /\ ((mdr_c_cofactor_rightdrc = ((mdr_a_cofactor_rightdrc) + (mdr_b_cofactor_rightdrc)) * S ((mdr_a_cofactor_rightdrc) + (mdr_b_cofactor_rightdrc)) + ((mdr_b_cofactor_rightdrc) + (mdr_b_cofactor_rightdrc))) /\ ((mdr_e_cofactor_rightdrc = ((mdr_p_cofactor_right) + (mdr_n_cofactor_right)) * S ((mdr_p_cofactor_right) + (mdr_n_cofactor_right)) + ((mdr_n_cofactor_right) + (mdr_n_cofactor_right))) /\ ((mdr_f_cofactor_rightdrc = ((mdr_ut_cofactor_right) + (mdr_e_cofactor_rightdrc)) * S ((mdr_ut_cofactor_right) + (mdr_e_cofactor_rightdrc)) + ((mdr_e_cofactor_rightdrc) + (mdr_e_cofactor_rightdrc))) /\ ((mdr_z_cofactor_rightdr) = ((mdr_c_cofactor_rightdrc) + (mdr_f_cofactor_rightdrc)) * S ((mdr_c_cofactor_rightdrc) + (mdr_f_cofactor_rightdrc)) + ((mdr_f_cofactor_rightdrc) + (mdr_f_cofactor_rightdrc))))))))) /\ (((exists ff_h_mdr_cofactor_rightdrb. ff_h_mdr_cofactor_rightdrb + S (mdr_z_cofactor_rightdr) = S ((S (mdr_i_cofactor_rightd)) * mdr_c_cofactor_rightd)) /\ exists ff_q_mdr_cofactor_rightdrb. mdr_b_cofactor_rightd = ff_q_mdr_cofactor_rightdrb * S ((S (mdr_i_cofactor_rightd)) * mdr_c_cofactor_rightd) + (mdr_z_cofactor_rightdr)))))))) /\ ((((exists ff_h_mdr_cofactor_rightp. ff_h_mdr_cofactor_rightp + S (mdr_p_cofactor_right) = S ((S (mdr_j_cofactor_right)) * uc)) /\ exists ff_q_mdr_cofactor_rightp. ub = ff_q_mdr_cofactor_rightp * S ((S (mdr_j_cofactor_right)) * uc) + (mdr_p_cofactor_right))) /\ (((exists ff_h_mdr_cofactor_rightn. ff_h_mdr_cofactor_rightn + S (mdr_n_cofactor_right) = S ((S (mdr_j_cofactor_right)) * vc)) /\ exists ff_q_mdr_cofactor_rightn. vb = ff_q_mdr_cofactor_rightn * S ((S (mdr_j_cofactor_right)) * vc) + (mdr_n_cofactor_right))))))) -> ((forall mdr_i_cofactor_equal_positive mdr_a_cofactor_equal_positive. (exists mdr_gap_cofactor_equal_positiveb. mdr_gap_cofactor_equal_positiveb + S (mdr_i_cofactor_equal_positive) = (S q)) -> (((exists ff_h_mdr_cofactor_equal_positiveo. ff_h_mdr_cofactor_equal_positiveo + S (mdr_a_cofactor_equal_positive) = S ((S (mdr_i_cofactor_equal_positive)) * ec)) /\ exists ff_q_mdr_cofactor_equal_positiveo. eb = ff_q_mdr_cofactor_equal_positiveo * S ((S (mdr_i_cofactor_equal_positive)) * ec) + (mdr_a_cofactor_equal_positive))) -> (((exists ff_h_mdr_cofactor_equal_positiven. ff_h_mdr_cofactor_equal_positiven + S (mdr_a_cofactor_equal_positive) = S ((S (mdr_i_cofactor_equal_positive)) * uc)) /\ exists ff_q_mdr_cofactor_equal_positiven. ub = ff_q_mdr_cofactor_equal_positiven * S ((S (mdr_i_cofactor_equal_positive)) * uc) + (mdr_a_cofactor_equal_positive)))) /\ (forall mdr_i_cofactor_equal_negative mdr_a_cofactor_equal_negative. (exists mdr_gap_cofactor_equal_negativeb. mdr_gap_cofactor_equal_negativeb + S (mdr_i_cofactor_equal_negative) = (S q)) -> (((exists ff_h_mdr_cofactor_equal_negativeo. ff_h_mdr_cofactor_equal_negativeo + S (mdr_a_cofactor_equal_negative) = S ((S (mdr_i_cofactor_equal_negative)) * fc)) /\ exists ff_q_mdr_cofactor_equal_negativeo. fb = ff_q_mdr_cofactor_equal_negativeo * S ((S (mdr_i_cofactor_equal_negative)) * fc) + (mdr_a_cofactor_equal_negative))) -> (((exists ff_h_mdr_cofactor_equal_negativen. ff_h_mdr_cofactor_equal_negativen + S (mdr_a_cofactor_equal_negative) = S ((S (mdr_i_cofactor_equal_negative)) * vc)) /\ exists ff_q_mdr_cofactor_equal_negativen. vb = ff_q_mdr_cofactor_equal_negativen * S ((S (mdr_i_cofactor_equal_negative)) * vc) + (mdr_a_cofactor_equal_negative)))))