matrix_integer_cofactor_streams_from_recursion

Exact expanded first-order arithmetic statement

forall ab ac bb bc eb ec fb fc cb cc db dc gb gc hb hc q. (forall mdr_ab_integer_recursion mdr_ac_integer_recursion mdr_bb_integer_recursion mdr_bc_integer_recursion mdr_eb_integer_recursion mdr_ec_integer_recursion mdr_fb_integer_recursion mdr_fc_integer_recursion mdr_p_integer_recursion mdr_n_integer_recursion mdr_P_integer_recursion mdr_N_integer_recursion. (forall ics_index_integer_recursionentries ics_value0_integer_recursionentries ics_value1_integer_recursionentries ics_value2_integer_recursionentries ics_value3_integer_recursionentries. (exists ics_gap_integer_recursionentries_bound. ics_gap_integer_recursionentries_bound + S (ics_index_integer_recursionentries) = ((q) * (q))) -> (((exists fs_h_ics_integer_recursionentries_at0. fs_h_ics_integer_recursionentries_at0 + S (ics_value0_integer_recursionentries) = S ((S (ics_index_integer_recursionentries)) * mdr_ac_integer_recursion)) /\ exists fs_q_ics_integer_recursionentries_at0. mdr_ab_integer_recursion = fs_q_ics_integer_recursionentries_at0 * S ((S (ics_index_integer_recursionentries)) * mdr_ac_integer_recursion) + (ics_value0_integer_recursionentries))) -> (((exists fs_h_ics_integer_recursionentries_at1. fs_h_ics_integer_recursionentries_at1 + S (ics_value1_integer_recursionentries) = S ((S (ics_index_integer_recursionentries)) * mdr_bc_integer_recursion)) /\ exists fs_q_ics_integer_recursionentries_at1. mdr_bb_integer_recursion = fs_q_ics_integer_recursionentries_at1 * S ((S (ics_index_integer_recursionentries)) * mdr_bc_integer_recursion) + (ics_value1_integer_recursionentries))) -> (((exists fs_h_ics_integer_recursionentries_at2. fs_h_ics_integer_recursionentries_at2 + S (ics_value2_integer_recursionentries) = S ((S (ics_index_integer_recursionentries)) * mdr_ec_integer_recursion)) /\ exists fs_q_ics_integer_recursionentries_at2. mdr_eb_integer_recursion = fs_q_ics_integer_recursionentries_at2 * S ((S (ics_index_integer_recursionentries)) * mdr_ec_integer_recursion) + (ics_value2_integer_recursionentries))) -> (((exists fs_h_ics_integer_recursionentries_at3. fs_h_ics_integer_recursionentries_at3 + S (ics_value3_integer_recursionentries) = S ((S (ics_index_integer_recursionentries)) * mdr_fc_integer_recursion)) /\ exists fs_q_ics_integer_recursionentries_at3. mdr_fb_integer_recursion = fs_q_ics_integer_recursionentries_at3 * S ((S (ics_index_integer_recursionentries)) * mdr_fc_integer_recursion) + (ics_value3_integer_recursionentries))) -> ics_value0_integer_recursionentries + ics_value3_integer_recursionentries = ics_value2_integer_recursionentries + ics_value1_integer_recursionentries) -> (exists mdr_b_integer_recursionfirst mdr_c_integer_recursionfirst mdr_l_integer_recursionfirst mdr_i_integer_recursionfirst. ((forall mdr_i_integer_recursionfirsth. (exists mdr_gap_integer_recursionfirsthi. mdr_gap_integer_recursionfirsthi + S (mdr_i_integer_recursionfirsth) = (mdr_l_integer_recursionfirst)) -> exists mdr_d_integer_recursionfirsth mdr_pb_integer_recursionfirsth mdr_pc_integer_recursionfirsth mdr_nb_integer_recursionfirsth mdr_nc_integer_recursionfirsth mdr_p_integer_recursionfirsth mdr_n_integer_recursionfirsth. ((exists mdr_z_integer_recursionfirsthr. ((exists mdr_a_integer_recursionfirsthrc mdr_b_integer_recursionfirsthrc mdr_c_integer_recursionfirsthrc mdr_e_integer_recursionfirsthrc mdr_f_integer_recursionfirsthrc. ((mdr_a_integer_recursionfirsthrc = ((mdr_d_integer_recursionfirsth) + (mdr_pb_integer_recursionfirsth)) * S ((mdr_d_integer_recursionfirsth) + (mdr_pb_integer_recursionfirsth)) + ((mdr_pb_integer_recursionfirsth) + (mdr_pb_integer_recursionfirsth))) /\ ((mdr_b_integer_recursionfirsthrc = ((mdr_pc_integer_recursionfirsth) + (mdr_nb_integer_recursionfirsth)) * S ((mdr_pc_integer_recursionfirsth) + (mdr_nb_integer_recursionfirsth)) + ((mdr_nb_integer_recursionfirsth) + (mdr_nb_integer_recursionfirsth))) /\ ((mdr_c_integer_recursionfirsthrc = ((mdr_a_integer_recursionfirsthrc) + (mdr_b_integer_recursionfirsthrc)) * S ((mdr_a_integer_recursionfirsthrc) + (mdr_b_integer_recursionfirsthrc)) + ((mdr_b_integer_recursionfirsthrc) + (mdr_b_integer_recursionfirsthrc))) /\ ((mdr_e_integer_recursionfirsthrc = ((mdr_p_integer_recursionfirsth) + (mdr_n_integer_recursionfirsth)) * S ((mdr_p_integer_recursionfirsth) + (mdr_n_integer_recursionfirsth)) + ((mdr_n_integer_recursionfirsth) + (mdr_n_integer_recursionfirsth))) /\ ((mdr_f_integer_recursionfirsthrc = ((mdr_nc_integer_recursionfirsth) + (mdr_e_integer_recursionfirsthrc)) * S ((mdr_nc_integer_recursionfirsth) + (mdr_e_integer_recursionfirsthrc)) + ((mdr_e_integer_recursionfirsthrc) + (mdr_e_integer_recursionfirsthrc))) /\ ((mdr_z_integer_recursionfirsthr) = ((mdr_c_integer_recursionfirsthrc) + (mdr_f_integer_recursionfirsthrc)) * S ((mdr_c_integer_recursionfirsthrc) + (mdr_f_integer_recursionfirsthrc)) + ((mdr_f_integer_recursionfirsthrc) + (mdr_f_integer_recursionfirsthrc))))))))) /\ (((exists ff_h_mdr_integer_recursionfirsthrb. ff_h_mdr_integer_recursionfirsthrb + S (mdr_z_integer_recursionfirsthr) = S ((S (mdr_i_integer_recursionfirsth)) * mdr_c_integer_recursionfirst)) /\ exists ff_q_mdr_integer_recursionfirsthrb. mdr_b_integer_recursionfirst = ff_q_mdr_integer_recursionfirsthrb * S ((S (mdr_i_integer_recursionfirsth)) * mdr_c_integer_recursionfirst) + (mdr_z_integer_recursionfirsthr))))) /\ (((((mdr_d_integer_recursionfirsth) = 0) /\ (((mdr_p_integer_recursionfirsth) = 1) /\ ((mdr_n_integer_recursionfirsth) = 0))) \/ exists mdr_q_integer_recursionfirsths mdr_eb_integer_recursionfirsths mdr_ec_integer_recursionfirsths mdr_fb_integer_recursionfirsths mdr_fc_integer_recursionfirsths. (((mdr_d_integer_recursionfirsth) = S (mdr_q_integer_recursionfirsths)) /\ ((forall mdr_j_integer_recursionfirsthsc. (exists mdr_gap_integer_recursionfirsthscj. mdr_gap_integer_recursionfirsthscj + S (mdr_j_integer_recursionfirsthsc) = (S (mdr_q_integer_recursionfirsths))) -> exists mdr_i_integer_recursionfirsthsc mdr_up_integer_recursionfirsthsc mdr_us_integer_recursionfirsthsc mdr_un_integer_recursionfirsthsc mdr_ut_integer_recursionfirsthsc mdr_p_integer_recursionfirsthsc mdr_n_integer_recursionfirsthsc. ((exists mdr_gap_integer_recursionfirsthsci. mdr_gap_integer_recursionfirsthsci + S (mdr_i_integer_recursionfirsthsc) = (mdr_i_integer_recursionfirsth)) /\ ((exists mdr_z_integer_recursionfirsthscr. ((exists mdr_a_integer_recursionfirsthscrc mdr_b_integer_recursionfirsthscrc mdr_c_integer_recursionfirsthscrc mdr_e_integer_recursionfirsthscrc mdr_f_integer_recursionfirsthscrc. ((mdr_a_integer_recursionfirsthscrc = ((mdr_q_integer_recursionfirsths) + (mdr_up_integer_recursionfirsthsc)) * S ((mdr_q_integer_recursionfirsths) + (mdr_up_integer_recursionfirsthsc)) + ((mdr_up_integer_recursionfirsthsc) + (mdr_up_integer_recursionfirsthsc))) /\ ((mdr_b_integer_recursionfirsthscrc = ((mdr_us_integer_recursionfirsthsc) + (mdr_un_integer_recursionfirsthsc)) * S ((mdr_us_integer_recursionfirsthsc) + (mdr_un_integer_recursionfirsthsc)) + ((mdr_un_integer_recursionfirsthsc) + (mdr_un_integer_recursionfirsthsc))) /\ ((mdr_c_integer_recursionfirsthscrc = ((mdr_a_integer_recursionfirsthscrc) + (mdr_b_integer_recursionfirsthscrc)) * S ((mdr_a_integer_recursionfirsthscrc) + (mdr_b_integer_recursionfirsthscrc)) + ((mdr_b_integer_recursionfirsthscrc) + (mdr_b_integer_recursionfirsthscrc))) /\ ((mdr_e_integer_recursionfirsthscrc = ((mdr_p_integer_recursionfirsthsc) + (mdr_n_integer_recursionfirsthsc)) * S ((mdr_p_integer_recursionfirsthsc) + (mdr_n_integer_recursionfirsthsc)) + ((mdr_n_integer_recursionfirsthsc) + (mdr_n_integer_recursionfirsthsc))) /\ ((mdr_f_integer_recursionfirsthscrc = ((mdr_ut_integer_recursionfirsthsc) + (mdr_e_integer_recursionfirsthscrc)) * S ((mdr_ut_integer_recursionfirsthsc) + (mdr_e_integer_recursionfirsthscrc)) + ((mdr_e_integer_recursionfirsthscrc) + (mdr_e_integer_recursionfirsthscrc))) /\ ((mdr_z_integer_recursionfirsthscr) = ((mdr_c_integer_recursionfirsthscrc) + (mdr_f_integer_recursionfirsthscrc)) * S ((mdr_c_integer_recursionfirsthscrc) + (mdr_f_integer_recursionfirsthscrc)) + ((mdr_f_integer_recursionfirsthscrc) + (mdr_f_integer_recursionfirsthscrc))))))))) /\ (((exists ff_h_mdr_integer_recursionfirsthscrb. ff_h_mdr_integer_recursionfirsthscrb + S (mdr_z_integer_recursionfirsthscr) = S ((S (mdr_i_integer_recursionfirsthsc)) * mdr_c_integer_recursionfirst)) /\ exists ff_q_mdr_integer_recursionfirsthscrb. mdr_b_integer_recursionfirst = ff_q_mdr_integer_recursionfirsthscrb * S ((S (mdr_i_integer_recursionfirsthsc)) * mdr_c_integer_recursionfirst) + (mdr_z_integer_recursionfirsthscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_integer_recursionfirsthscm_positive. (exists ff_gap_mdm_lt_mdr_integer_recursionfirsthscm_positive_index_bound. ff_gap_mdm_lt_mdr_integer_recursionfirsthscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_integer_recursionfirsthscm_positive) = ((mdr_q_integer_recursionfirsths) * (mdr_q_integer_recursionfirsths))) -> exists ff_row_mdm_prefix_mdr_integer_recursionfirsthscm_positive ff_column_mdm_prefix_mdr_integer_recursionfirsthscm_positive ff_value_mdm_prefix_mdr_integer_recursionfirsthscm_positive. (ff_index_mdm_prefix_mdr_integer_recursionfirsthscm_positive = (mdr_q_integer_recursionfirsths) * ff_row_mdm_prefix_mdr_integer_recursionfirsthscm_positive + ff_column_mdm_prefix_mdr_integer_recursionfirsthscm_positive /\ ((exists ff_gap_mdm_lt_mdr_integer_recursionfirsthscm_positive_column_bound. ff_gap_mdm_lt_mdr_integer_recursionfirsthscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_integer_recursionfirsthscm_positive) = (mdr_q_integer_recursionfirsths)) /\ ((exists ff_row_mdm_cell_mdr_integer_recursionfirsthscm_positive_cell ff_column_mdm_cell_mdr_integer_recursionfirsthscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_integer_recursionfirsthscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_integer_recursionfirsthscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_integer_recursionfirsthscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_integer_recursionfirsthscm_positive_cell = ff_row_mdm_prefix_mdr_integer_recursionfirsthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_integer_recursionfirsthscm_positive_cell_row_after. ff_gap_mdm_le_mdr_integer_recursionfirsthscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_integer_recursionfirsthscm_positive)) /\ ff_row_mdm_cell_mdr_integer_recursionfirsthscm_positive_cell = S ff_row_mdm_prefix_mdr_integer_recursionfirsthscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_integer_recursionfirsthscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_integer_recursionfirsthscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_integer_recursionfirsthscm_positive) = (mdr_j_integer_recursionfirsthsc)) /\ ff_column_mdm_cell_mdr_integer_recursionfirsthscm_positive_cell = ff_column_mdm_prefix_mdr_integer_recursionfirsthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_integer_recursionfirsthscm_positive_cell_column_after. ff_gap_mdm_le_mdr_integer_recursionfirsthscm_positive_cell_column_after + (mdr_j_integer_recursionfirsthsc) = (ff_column_mdm_prefix_mdr_integer_recursionfirsthscm_positive)) /\ ff_column_mdm_cell_mdr_integer_recursionfirsthscm_positive_cell = S ff_column_mdm_prefix_mdr_integer_recursionfirsthscm_positive))) /\ (((exists ff_h_mdm_mdr_integer_recursionfirsthscm_positive_cell_source. ff_h_mdm_mdr_integer_recursionfirsthscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_integer_recursionfirsthscm_positive) = S ((S ((ff_row_mdm_cell_mdr_integer_recursionfirsthscm_positive_cell) * (S (mdr_q_integer_recursionfirsths)) + (ff_column_mdm_cell_mdr_integer_recursionfirsthscm_positive_cell))) * mdr_pc_integer_recursionfirsth)) /\ exists ff_q_mdm_mdr_integer_recursionfirsthscm_positive_cell_source. mdr_pb_integer_recursionfirsth = ff_q_mdm_mdr_integer_recursionfirsthscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_integer_recursionfirsthscm_positive_cell) * (S (mdr_q_integer_recursionfirsths)) + (ff_column_mdm_cell_mdr_integer_recursionfirsthscm_positive_cell))) * mdr_pc_integer_recursionfirsth) + (ff_value_mdm_prefix_mdr_integer_recursionfirsthscm_positive)))))) /\ (((exists ff_h_mdm_mdr_integer_recursionfirsthscm_positive_target. ff_h_mdm_mdr_integer_recursionfirsthscm_positive_target + S (ff_value_mdm_prefix_mdr_integer_recursionfirsthscm_positive) = S ((S (ff_index_mdm_prefix_mdr_integer_recursionfirsthscm_positive)) * mdr_us_integer_recursionfirsthsc)) /\ exists ff_q_mdm_mdr_integer_recursionfirsthscm_positive_target. mdr_up_integer_recursionfirsthsc = ff_q_mdm_mdr_integer_recursionfirsthscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_integer_recursionfirsthscm_positive)) * mdr_us_integer_recursionfirsthsc) + (ff_value_mdm_prefix_mdr_integer_recursionfirsthscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_integer_recursionfirsthscm_negative. (exists ff_gap_mdm_lt_mdr_integer_recursionfirsthscm_negative_index_bound. ff_gap_mdm_lt_mdr_integer_recursionfirsthscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_integer_recursionfirsthscm_negative) = ((mdr_q_integer_recursionfirsths) * (mdr_q_integer_recursionfirsths))) -> exists ff_row_mdm_prefix_mdr_integer_recursionfirsthscm_negative ff_column_mdm_prefix_mdr_integer_recursionfirsthscm_negative ff_value_mdm_prefix_mdr_integer_recursionfirsthscm_negative. (ff_index_mdm_prefix_mdr_integer_recursionfirsthscm_negative = (mdr_q_integer_recursionfirsths) * ff_row_mdm_prefix_mdr_integer_recursionfirsthscm_negative + ff_column_mdm_prefix_mdr_integer_recursionfirsthscm_negative /\ ((exists ff_gap_mdm_lt_mdr_integer_recursionfirsthscm_negative_column_bound. ff_gap_mdm_lt_mdr_integer_recursionfirsthscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_integer_recursionfirsthscm_negative) = (mdr_q_integer_recursionfirsths)) /\ ((exists ff_row_mdm_cell_mdr_integer_recursionfirsthscm_negative_cell ff_column_mdm_cell_mdr_integer_recursionfirsthscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_integer_recursionfirsthscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_integer_recursionfirsthscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_integer_recursionfirsthscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_integer_recursionfirsthscm_negative_cell = ff_row_mdm_prefix_mdr_integer_recursionfirsthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_integer_recursionfirsthscm_negative_cell_row_after. ff_gap_mdm_le_mdr_integer_recursionfirsthscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_integer_recursionfirsthscm_negative)) /\ ff_row_mdm_cell_mdr_integer_recursionfirsthscm_negative_cell = S ff_row_mdm_prefix_mdr_integer_recursionfirsthscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_integer_recursionfirsthscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_integer_recursionfirsthscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_integer_recursionfirsthscm_negative) = (mdr_j_integer_recursionfirsthsc)) /\ ff_column_mdm_cell_mdr_integer_recursionfirsthscm_negative_cell = ff_column_mdm_prefix_mdr_integer_recursionfirsthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_integer_recursionfirsthscm_negative_cell_column_after. ff_gap_mdm_le_mdr_integer_recursionfirsthscm_negative_cell_column_after + (mdr_j_integer_recursionfirsthsc) = (ff_column_mdm_prefix_mdr_integer_recursionfirsthscm_negative)) /\ ff_column_mdm_cell_mdr_integer_recursionfirsthscm_negative_cell = S ff_column_mdm_prefix_mdr_integer_recursionfirsthscm_negative))) /\ (((exists ff_h_mdm_mdr_integer_recursionfirsthscm_negative_cell_source. ff_h_mdm_mdr_integer_recursionfirsthscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_integer_recursionfirsthscm_negative) = S ((S ((ff_row_mdm_cell_mdr_integer_recursionfirsthscm_negative_cell) * (S (mdr_q_integer_recursionfirsths)) + (ff_column_mdm_cell_mdr_integer_recursionfirsthscm_negative_cell))) * mdr_nc_integer_recursionfirsth)) /\ exists ff_q_mdm_mdr_integer_recursionfirsthscm_negative_cell_source. mdr_nb_integer_recursionfirsth = ff_q_mdm_mdr_integer_recursionfirsthscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_integer_recursionfirsthscm_negative_cell) * (S (mdr_q_integer_recursionfirsths)) + (ff_column_mdm_cell_mdr_integer_recursionfirsthscm_negative_cell))) * mdr_nc_integer_recursionfirsth) + (ff_value_mdm_prefix_mdr_integer_recursionfirsthscm_negative)))))) /\ (((exists ff_h_mdm_mdr_integer_recursionfirsthscm_negative_target. ff_h_mdm_mdr_integer_recursionfirsthscm_negative_target + S (ff_value_mdm_prefix_mdr_integer_recursionfirsthscm_negative) = S ((S (ff_index_mdm_prefix_mdr_integer_recursionfirsthscm_negative)) * mdr_ut_integer_recursionfirsthsc)) /\ exists ff_q_mdm_mdr_integer_recursionfirsthscm_negative_target. mdr_un_integer_recursionfirsthsc = ff_q_mdm_mdr_integer_recursionfirsthscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_integer_recursionfirsthscm_negative)) * mdr_ut_integer_recursionfirsthsc) + (ff_value_mdm_prefix_mdr_integer_recursionfirsthscm_negative))))))))) /\ ((((exists ff_h_mdr_integer_recursionfirsthscp. ff_h_mdr_integer_recursionfirsthscp + S (mdr_p_integer_recursionfirsthsc) = S ((S (mdr_j_integer_recursionfirsthsc)) * mdr_ec_integer_recursionfirsths)) /\ exists ff_q_mdr_integer_recursionfirsthscp. mdr_eb_integer_recursionfirsths = ff_q_mdr_integer_recursionfirsthscp * S ((S (mdr_j_integer_recursionfirsthsc)) * mdr_ec_integer_recursionfirsths) + (mdr_p_integer_recursionfirsthsc))) /\ (((exists ff_h_mdr_integer_recursionfirsthscn. ff_h_mdr_integer_recursionfirsthscn + S (mdr_n_integer_recursionfirsthsc) = S ((S (mdr_j_integer_recursionfirsthsc)) * mdr_fc_integer_recursionfirsths)) /\ exists ff_q_mdr_integer_recursionfirsthscn. mdr_fb_integer_recursionfirsths = ff_q_mdr_integer_recursionfirsthscn * S ((S (mdr_j_integer_recursionfirsthsc)) * mdr_fc_integer_recursionfirsths) + (mdr_n_integer_recursionfirsthsc)))))))) /\ (exists ff_ub_mce_fold_mdr_integer_recursionfirsthsf ff_uc_mce_fold_mdr_integer_recursionfirsthsf ff_vb_mce_fold_mdr_integer_recursionfirsthsf ff_vc_mce_fold_mdr_integer_recursionfirsthsf. ((forall ff_index_mce_alternating_mdr_integer_recursionfirsthsf_prefix. (exists ff_gap_mce_mdr_integer_recursionfirsthsf_prefix_index. ff_gap_mce_mdr_integer_recursionfirsthsf_prefix_index + S (ff_index_mce_alternating_mdr_integer_recursionfirsthsf_prefix) = (S (mdr_q_integer_recursionfirsths))) -> exists ff_ap_mce_alternating_mdr_integer_recursionfirsthsf_prefix ff_an_mce_alternating_mdr_integer_recursionfirsthsf_prefix ff_bp_mce_alternating_mdr_integer_recursionfirsthsf_prefix ff_bn_mce_alternating_mdr_integer_recursionfirsthsf_prefix ff_p_mce_alternating_mdr_integer_recursionfirsthsf_prefix ff_n_mce_alternating_mdr_integer_recursionfirsthsf_prefix. ((((exists ff_h_mce_mdr_integer_recursionfirsthsf_prefix_ap. ff_h_mce_mdr_integer_recursionfirsthsf_prefix_ap + S (ff_ap_mce_alternating_mdr_integer_recursionfirsthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_integer_recursionfirsthsf_prefix)) * mdr_pc_integer_recursionfirsth)) /\ exists ff_q_mce_mdr_integer_recursionfirsthsf_prefix_ap. mdr_pb_integer_recursionfirsth = ff_q_mce_mdr_integer_recursionfirsthsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_integer_recursionfirsthsf_prefix)) * mdr_pc_integer_recursionfirsth) + (ff_ap_mce_alternating_mdr_integer_recursionfirsthsf_prefix))) /\ ((((exists ff_h_mce_mdr_integer_recursionfirsthsf_prefix_an. ff_h_mce_mdr_integer_recursionfirsthsf_prefix_an + S (ff_an_mce_alternating_mdr_integer_recursionfirsthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_integer_recursionfirsthsf_prefix)) * mdr_nc_integer_recursionfirsth)) /\ exists ff_q_mce_mdr_integer_recursionfirsthsf_prefix_an. mdr_nb_integer_recursionfirsth = ff_q_mce_mdr_integer_recursionfirsthsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_integer_recursionfirsthsf_prefix)) * mdr_nc_integer_recursionfirsth) + (ff_an_mce_alternating_mdr_integer_recursionfirsthsf_prefix))) /\ ((((exists ff_h_mce_mdr_integer_recursionfirsthsf_prefix_bp. ff_h_mce_mdr_integer_recursionfirsthsf_prefix_bp + S (ff_bp_mce_alternating_mdr_integer_recursionfirsthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_integer_recursionfirsthsf_prefix)) * mdr_ec_integer_recursionfirsths)) /\ exists ff_q_mce_mdr_integer_recursionfirsthsf_prefix_bp. mdr_eb_integer_recursionfirsths = ff_q_mce_mdr_integer_recursionfirsthsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_integer_recursionfirsthsf_prefix)) * mdr_ec_integer_recursionfirsths) + (ff_bp_mce_alternating_mdr_integer_recursionfirsthsf_prefix))) /\ ((((exists ff_h_mce_mdr_integer_recursionfirsthsf_prefix_bn. ff_h_mce_mdr_integer_recursionfirsthsf_prefix_bn + S (ff_bn_mce_alternating_mdr_integer_recursionfirsthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_integer_recursionfirsthsf_prefix)) * mdr_fc_integer_recursionfirsths)) /\ exists ff_q_mce_mdr_integer_recursionfirsthsf_prefix_bn. mdr_fb_integer_recursionfirsths = ff_q_mce_mdr_integer_recursionfirsthsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_integer_recursionfirsthsf_prefix)) * mdr_fc_integer_recursionfirsths) + (ff_bn_mce_alternating_mdr_integer_recursionfirsthsf_prefix))) /\ ((((exists ff_h_mce_mdr_integer_recursionfirsthsf_prefix_positive. ff_h_mce_mdr_integer_recursionfirsthsf_prefix_positive + S (ff_p_mce_alternating_mdr_integer_recursionfirsthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_integer_recursionfirsthsf_prefix)) * ff_uc_mce_fold_mdr_integer_recursionfirsthsf)) /\ exists ff_q_mce_mdr_integer_recursionfirsthsf_prefix_positive. ff_ub_mce_fold_mdr_integer_recursionfirsthsf = ff_q_mce_mdr_integer_recursionfirsthsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_integer_recursionfirsthsf_prefix)) * ff_uc_mce_fold_mdr_integer_recursionfirsthsf) + (ff_p_mce_alternating_mdr_integer_recursionfirsthsf_prefix))) /\ ((((exists ff_h_mce_mdr_integer_recursionfirsthsf_prefix_negative. ff_h_mce_mdr_integer_recursionfirsthsf_prefix_negative + S (ff_n_mce_alternating_mdr_integer_recursionfirsthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_integer_recursionfirsthsf_prefix)) * ff_vc_mce_fold_mdr_integer_recursionfirsthsf)) /\ exists ff_q_mce_mdr_integer_recursionfirsthsf_prefix_negative. ff_vb_mce_fold_mdr_integer_recursionfirsthsf = ff_q_mce_mdr_integer_recursionfirsthsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_integer_recursionfirsthsf_prefix)) * ff_vc_mce_fold_mdr_integer_recursionfirsthsf) + (ff_n_mce_alternating_mdr_integer_recursionfirsthsf_prefix))) /\ (((exists ff_even_mce_term_mdr_integer_recursionfirsthsf_prefix_term. ff_index_mce_alternating_mdr_integer_recursionfirsthsf_prefix = 2 * ff_even_mce_term_mdr_integer_recursionfirsthsf_prefix_term) /\ (ff_p_mce_alternating_mdr_integer_recursionfirsthsf_prefix = (ff_ap_mce_alternating_mdr_integer_recursionfirsthsf_prefix) * (ff_bp_mce_alternating_mdr_integer_recursionfirsthsf_prefix) + (ff_an_mce_alternating_mdr_integer_recursionfirsthsf_prefix) * (ff_bn_mce_alternating_mdr_integer_recursionfirsthsf_prefix) /\ ff_n_mce_alternating_mdr_integer_recursionfirsthsf_prefix = (ff_ap_mce_alternating_mdr_integer_recursionfirsthsf_prefix) * (ff_bn_mce_alternating_mdr_integer_recursionfirsthsf_prefix) + (ff_an_mce_alternating_mdr_integer_recursionfirsthsf_prefix) * (ff_bp_mce_alternating_mdr_integer_recursionfirsthsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_integer_recursionfirsthsf_prefix_term. ff_index_mce_alternating_mdr_integer_recursionfirsthsf_prefix = 2 * ff_odd_mce_term_mdr_integer_recursionfirsthsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_integer_recursionfirsthsf_prefix = (ff_ap_mce_alternating_mdr_integer_recursionfirsthsf_prefix) * (ff_bn_mce_alternating_mdr_integer_recursionfirsthsf_prefix) + (ff_an_mce_alternating_mdr_integer_recursionfirsthsf_prefix) * (ff_bp_mce_alternating_mdr_integer_recursionfirsthsf_prefix) /\ ff_n_mce_alternating_mdr_integer_recursionfirsthsf_prefix = (ff_ap_mce_alternating_mdr_integer_recursionfirsthsf_prefix) * (ff_bp_mce_alternating_mdr_integer_recursionfirsthsf_prefix) + (ff_an_mce_alternating_mdr_integer_recursionfirsthsf_prefix) * (ff_bn_mce_alternating_mdr_integer_recursionfirsthsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_integer_recursionfirsthsf_positive ff_v_mce_mdr_integer_recursionfirsthsf_positive. ((((exists ff_h_mce_mdr_integer_recursionfirsthsf_positive_start. ff_h_mce_mdr_integer_recursionfirsthsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_integer_recursionfirsthsf_positive)) /\ exists ff_q_mce_mdr_integer_recursionfirsthsf_positive_start. ff_u_mce_mdr_integer_recursionfirsthsf_positive = ff_q_mce_mdr_integer_recursionfirsthsf_positive_start * S ((S (0)) * ff_v_mce_mdr_integer_recursionfirsthsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_integer_recursionfirsthsf_positive_terminal. ff_h_mce_mdr_integer_recursionfirsthsf_positive_terminal + S (mdr_p_integer_recursionfirsth) = S ((S ((S (mdr_q_integer_recursionfirsths)))) * ff_v_mce_mdr_integer_recursionfirsthsf_positive)) /\ exists ff_q_mce_mdr_integer_recursionfirsthsf_positive_terminal. ff_u_mce_mdr_integer_recursionfirsthsf_positive = ff_q_mce_mdr_integer_recursionfirsthsf_positive_terminal * S ((S ((S (mdr_q_integer_recursionfirsths)))) * ff_v_mce_mdr_integer_recursionfirsthsf_positive) + (mdr_p_integer_recursionfirsth))) /\ forall ff_i_mce_mdr_integer_recursionfirsthsf_positive. (exists ff_lt_mce_mdr_integer_recursionfirsthsf_positive_bound. ff_lt_mce_mdr_integer_recursionfirsthsf_positive_bound + S ff_i_mce_mdr_integer_recursionfirsthsf_positive = (S (mdr_q_integer_recursionfirsths))) -> exists ff_a_mce_mdr_integer_recursionfirsthsf_positive ff_r_mce_mdr_integer_recursionfirsthsf_positive ff_s_mce_mdr_integer_recursionfirsthsf_positive. ((((exists ff_h_mce_mdr_integer_recursionfirsthsf_positive_summand. ff_h_mce_mdr_integer_recursionfirsthsf_positive_summand + S (ff_a_mce_mdr_integer_recursionfirsthsf_positive) = S ((S (ff_i_mce_mdr_integer_recursionfirsthsf_positive)) * ff_uc_mce_fold_mdr_integer_recursionfirsthsf)) /\ exists ff_q_mce_mdr_integer_recursionfirsthsf_positive_summand. ff_ub_mce_fold_mdr_integer_recursionfirsthsf = ff_q_mce_mdr_integer_recursionfirsthsf_positive_summand * S ((S (ff_i_mce_mdr_integer_recursionfirsthsf_positive)) * ff_uc_mce_fold_mdr_integer_recursionfirsthsf) + (ff_a_mce_mdr_integer_recursionfirsthsf_positive))) /\ ((((exists ff_h_mce_mdr_integer_recursionfirsthsf_positive_partial. ff_h_mce_mdr_integer_recursionfirsthsf_positive_partial + S (ff_r_mce_mdr_integer_recursionfirsthsf_positive) = S ((S (ff_i_mce_mdr_integer_recursionfirsthsf_positive)) * ff_v_mce_mdr_integer_recursionfirsthsf_positive)) /\ exists ff_q_mce_mdr_integer_recursionfirsthsf_positive_partial. ff_u_mce_mdr_integer_recursionfirsthsf_positive = ff_q_mce_mdr_integer_recursionfirsthsf_positive_partial * S ((S (ff_i_mce_mdr_integer_recursionfirsthsf_positive)) * ff_v_mce_mdr_integer_recursionfirsthsf_positive) + (ff_r_mce_mdr_integer_recursionfirsthsf_positive))) /\ ((((exists ff_h_mce_mdr_integer_recursionfirsthsf_positive_successor. ff_h_mce_mdr_integer_recursionfirsthsf_positive_successor + S (ff_s_mce_mdr_integer_recursionfirsthsf_positive) = S ((S (S ff_i_mce_mdr_integer_recursionfirsthsf_positive)) * ff_v_mce_mdr_integer_recursionfirsthsf_positive)) /\ exists ff_q_mce_mdr_integer_recursionfirsthsf_positive_successor. ff_u_mce_mdr_integer_recursionfirsthsf_positive = ff_q_mce_mdr_integer_recursionfirsthsf_positive_successor * S ((S (S ff_i_mce_mdr_integer_recursionfirsthsf_positive)) * ff_v_mce_mdr_integer_recursionfirsthsf_positive) + (ff_s_mce_mdr_integer_recursionfirsthsf_positive))) /\ ff_s_mce_mdr_integer_recursionfirsthsf_positive = ff_r_mce_mdr_integer_recursionfirsthsf_positive + ff_a_mce_mdr_integer_recursionfirsthsf_positive)))))) /\ (exists ff_u_mce_mdr_integer_recursionfirsthsf_negative ff_v_mce_mdr_integer_recursionfirsthsf_negative. ((((exists ff_h_mce_mdr_integer_recursionfirsthsf_negative_start. ff_h_mce_mdr_integer_recursionfirsthsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_integer_recursionfirsthsf_negative)) /\ exists ff_q_mce_mdr_integer_recursionfirsthsf_negative_start. ff_u_mce_mdr_integer_recursionfirsthsf_negative = ff_q_mce_mdr_integer_recursionfirsthsf_negative_start * S ((S (0)) * ff_v_mce_mdr_integer_recursionfirsthsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_integer_recursionfirsthsf_negative_terminal. ff_h_mce_mdr_integer_recursionfirsthsf_negative_terminal + S (mdr_n_integer_recursionfirsth) = S ((S ((S (mdr_q_integer_recursionfirsths)))) * ff_v_mce_mdr_integer_recursionfirsthsf_negative)) /\ exists ff_q_mce_mdr_integer_recursionfirsthsf_negative_terminal. ff_u_mce_mdr_integer_recursionfirsthsf_negative = ff_q_mce_mdr_integer_recursionfirsthsf_negative_terminal * S ((S ((S (mdr_q_integer_recursionfirsths)))) * ff_v_mce_mdr_integer_recursionfirsthsf_negative) + (mdr_n_integer_recursionfirsth))) /\ forall ff_i_mce_mdr_integer_recursionfirsthsf_negative. (exists ff_lt_mce_mdr_integer_recursionfirsthsf_negative_bound. ff_lt_mce_mdr_integer_recursionfirsthsf_negative_bound + S ff_i_mce_mdr_integer_recursionfirsthsf_negative = (S (mdr_q_integer_recursionfirsths))) -> exists ff_a_mce_mdr_integer_recursionfirsthsf_negative ff_r_mce_mdr_integer_recursionfirsthsf_negative ff_s_mce_mdr_integer_recursionfirsthsf_negative. ((((exists ff_h_mce_mdr_integer_recursionfirsthsf_negative_summand. ff_h_mce_mdr_integer_recursionfirsthsf_negative_summand + S (ff_a_mce_mdr_integer_recursionfirsthsf_negative) = S ((S (ff_i_mce_mdr_integer_recursionfirsthsf_negative)) * ff_vc_mce_fold_mdr_integer_recursionfirsthsf)) /\ exists ff_q_mce_mdr_integer_recursionfirsthsf_negative_summand. ff_vb_mce_fold_mdr_integer_recursionfirsthsf = ff_q_mce_mdr_integer_recursionfirsthsf_negative_summand * S ((S (ff_i_mce_mdr_integer_recursionfirsthsf_negative)) * ff_vc_mce_fold_mdr_integer_recursionfirsthsf) + (ff_a_mce_mdr_integer_recursionfirsthsf_negative))) /\ ((((exists ff_h_mce_mdr_integer_recursionfirsthsf_negative_partial. ff_h_mce_mdr_integer_recursionfirsthsf_negative_partial + S (ff_r_mce_mdr_integer_recursionfirsthsf_negative) = S ((S (ff_i_mce_mdr_integer_recursionfirsthsf_negative)) * ff_v_mce_mdr_integer_recursionfirsthsf_negative)) /\ exists ff_q_mce_mdr_integer_recursionfirsthsf_negative_partial. ff_u_mce_mdr_integer_recursionfirsthsf_negative = ff_q_mce_mdr_integer_recursionfirsthsf_negative_partial * S ((S (ff_i_mce_mdr_integer_recursionfirsthsf_negative)) * ff_v_mce_mdr_integer_recursionfirsthsf_negative) + (ff_r_mce_mdr_integer_recursionfirsthsf_negative))) /\ ((((exists ff_h_mce_mdr_integer_recursionfirsthsf_negative_successor. ff_h_mce_mdr_integer_recursionfirsthsf_negative_successor + S (ff_s_mce_mdr_integer_recursionfirsthsf_negative) = S ((S (S ff_i_mce_mdr_integer_recursionfirsthsf_negative)) * ff_v_mce_mdr_integer_recursionfirsthsf_negative)) /\ exists ff_q_mce_mdr_integer_recursionfirsthsf_negative_successor. ff_u_mce_mdr_integer_recursionfirsthsf_negative = ff_q_mce_mdr_integer_recursionfirsthsf_negative_successor * S ((S (S ff_i_mce_mdr_integer_recursionfirsthsf_negative)) * ff_v_mce_mdr_integer_recursionfirsthsf_negative) + (ff_s_mce_mdr_integer_recursionfirsthsf_negative))) /\ ff_s_mce_mdr_integer_recursionfirsthsf_negative = ff_r_mce_mdr_integer_recursionfirsthsf_negative + ff_a_mce_mdr_integer_recursionfirsthsf_negative))))))))))))))) /\ ((exists mdr_gap_integer_recursionfirsti. mdr_gap_integer_recursionfirsti + S (mdr_i_integer_recursionfirst) = (mdr_l_integer_recursionfirst)) /\ (exists mdr_z_integer_recursionfirstr. ((exists mdr_a_integer_recursionfirstrc mdr_b_integer_recursionfirstrc mdr_c_integer_recursionfirstrc mdr_e_integer_recursionfirstrc mdr_f_integer_recursionfirstrc. ((mdr_a_integer_recursionfirstrc = ((q) + (mdr_ab_integer_recursion)) * S ((q) + (mdr_ab_integer_recursion)) + ((mdr_ab_integer_recursion) + (mdr_ab_integer_recursion))) /\ ((mdr_b_integer_recursionfirstrc = ((mdr_ac_integer_recursion) + (mdr_bb_integer_recursion)) * S ((mdr_ac_integer_recursion) + (mdr_bb_integer_recursion)) + ((mdr_bb_integer_recursion) + (mdr_bb_integer_recursion))) /\ ((mdr_c_integer_recursionfirstrc = ((mdr_a_integer_recursionfirstrc) + (mdr_b_integer_recursionfirstrc)) * S ((mdr_a_integer_recursionfirstrc) + (mdr_b_integer_recursionfirstrc)) + ((mdr_b_integer_recursionfirstrc) + (mdr_b_integer_recursionfirstrc))) /\ ((mdr_e_integer_recursionfirstrc = ((mdr_p_integer_recursion) + (mdr_n_integer_recursion)) * S ((mdr_p_integer_recursion) + (mdr_n_integer_recursion)) + ((mdr_n_integer_recursion) + (mdr_n_integer_recursion))) /\ ((mdr_f_integer_recursionfirstrc = ((mdr_bc_integer_recursion) + (mdr_e_integer_recursionfirstrc)) * S ((mdr_bc_integer_recursion) + (mdr_e_integer_recursionfirstrc)) + ((mdr_e_integer_recursionfirstrc) + (mdr_e_integer_recursionfirstrc))) /\ ((mdr_z_integer_recursionfirstr) = ((mdr_c_integer_recursionfirstrc) + (mdr_f_integer_recursionfirstrc)) * S ((mdr_c_integer_recursionfirstrc) + (mdr_f_integer_recursionfirstrc)) + ((mdr_f_integer_recursionfirstrc) + (mdr_f_integer_recursionfirstrc))))))))) /\ (((exists ff_h_mdr_integer_recursionfirstrb. ff_h_mdr_integer_recursionfirstrb + S (mdr_z_integer_recursionfirstr) = S ((S (mdr_i_integer_recursionfirst)) * mdr_c_integer_recursionfirst)) /\ exists ff_q_mdr_integer_recursionfirstrb. mdr_b_integer_recursionfirst = ff_q_mdr_integer_recursionfirstrb * S ((S (mdr_i_integer_recursionfirst)) * mdr_c_integer_recursionfirst) + (mdr_z_integer_recursionfirstr)))))))) -> (exists mdr_b_integer_recursionsecond mdr_c_integer_recursionsecond mdr_l_integer_recursionsecond mdr_i_integer_recursionsecond. ((forall mdr_i_integer_recursionsecondh. (exists mdr_gap_integer_recursionsecondhi. mdr_gap_integer_recursionsecondhi + S (mdr_i_integer_recursionsecondh) = (mdr_l_integer_recursionsecond)) -> exists mdr_d_integer_recursionsecondh mdr_pb_integer_recursionsecondh mdr_pc_integer_recursionsecondh mdr_nb_integer_recursionsecondh mdr_nc_integer_recursionsecondh mdr_p_integer_recursionsecondh mdr_n_integer_recursionsecondh. ((exists mdr_z_integer_recursionsecondhr. ((exists mdr_a_integer_recursionsecondhrc mdr_b_integer_recursionsecondhrc mdr_c_integer_recursionsecondhrc mdr_e_integer_recursionsecondhrc mdr_f_integer_recursionsecondhrc. ((mdr_a_integer_recursionsecondhrc = ((mdr_d_integer_recursionsecondh) + (mdr_pb_integer_recursionsecondh)) * S ((mdr_d_integer_recursionsecondh) + (mdr_pb_integer_recursionsecondh)) + ((mdr_pb_integer_recursionsecondh) + (mdr_pb_integer_recursionsecondh))) /\ ((mdr_b_integer_recursionsecondhrc = ((mdr_pc_integer_recursionsecondh) + (mdr_nb_integer_recursionsecondh)) * S ((mdr_pc_integer_recursionsecondh) + (mdr_nb_integer_recursionsecondh)) + ((mdr_nb_integer_recursionsecondh) + (mdr_nb_integer_recursionsecondh))) /\ ((mdr_c_integer_recursionsecondhrc = ((mdr_a_integer_recursionsecondhrc) + (mdr_b_integer_recursionsecondhrc)) * S ((mdr_a_integer_recursionsecondhrc) + (mdr_b_integer_recursionsecondhrc)) + ((mdr_b_integer_recursionsecondhrc) + (mdr_b_integer_recursionsecondhrc))) /\ ((mdr_e_integer_recursionsecondhrc = ((mdr_p_integer_recursionsecondh) + (mdr_n_integer_recursionsecondh)) * S ((mdr_p_integer_recursionsecondh) + (mdr_n_integer_recursionsecondh)) + ((mdr_n_integer_recursionsecondh) + (mdr_n_integer_recursionsecondh))) /\ ((mdr_f_integer_recursionsecondhrc = ((mdr_nc_integer_recursionsecondh) + (mdr_e_integer_recursionsecondhrc)) * S ((mdr_nc_integer_recursionsecondh) + (mdr_e_integer_recursionsecondhrc)) + ((mdr_e_integer_recursionsecondhrc) + (mdr_e_integer_recursionsecondhrc))) /\ ((mdr_z_integer_recursionsecondhr) = ((mdr_c_integer_recursionsecondhrc) + (mdr_f_integer_recursionsecondhrc)) * S ((mdr_c_integer_recursionsecondhrc) + (mdr_f_integer_recursionsecondhrc)) + ((mdr_f_integer_recursionsecondhrc) + (mdr_f_integer_recursionsecondhrc))))))))) /\ (((exists ff_h_mdr_integer_recursionsecondhrb. ff_h_mdr_integer_recursionsecondhrb + S (mdr_z_integer_recursionsecondhr) = S ((S (mdr_i_integer_recursionsecondh)) * mdr_c_integer_recursionsecond)) /\ exists ff_q_mdr_integer_recursionsecondhrb. mdr_b_integer_recursionsecond = ff_q_mdr_integer_recursionsecondhrb * S ((S (mdr_i_integer_recursionsecondh)) * mdr_c_integer_recursionsecond) + (mdr_z_integer_recursionsecondhr))))) /\ (((((mdr_d_integer_recursionsecondh) = 0) /\ (((mdr_p_integer_recursionsecondh) = 1) /\ ((mdr_n_integer_recursionsecondh) = 0))) \/ exists mdr_q_integer_recursionsecondhs mdr_eb_integer_recursionsecondhs mdr_ec_integer_recursionsecondhs mdr_fb_integer_recursionsecondhs mdr_fc_integer_recursionsecondhs. (((mdr_d_integer_recursionsecondh) = S (mdr_q_integer_recursionsecondhs)) /\ ((forall mdr_j_integer_recursionsecondhsc. (exists mdr_gap_integer_recursionsecondhscj. mdr_gap_integer_recursionsecondhscj + S (mdr_j_integer_recursionsecondhsc) = (S (mdr_q_integer_recursionsecondhs))) -> exists mdr_i_integer_recursionsecondhsc mdr_up_integer_recursionsecondhsc mdr_us_integer_recursionsecondhsc mdr_un_integer_recursionsecondhsc mdr_ut_integer_recursionsecondhsc mdr_p_integer_recursionsecondhsc mdr_n_integer_recursionsecondhsc. ((exists mdr_gap_integer_recursionsecondhsci. mdr_gap_integer_recursionsecondhsci + S (mdr_i_integer_recursionsecondhsc) = (mdr_i_integer_recursionsecondh)) /\ ((exists mdr_z_integer_recursionsecondhscr. ((exists mdr_a_integer_recursionsecondhscrc mdr_b_integer_recursionsecondhscrc mdr_c_integer_recursionsecondhscrc mdr_e_integer_recursionsecondhscrc mdr_f_integer_recursionsecondhscrc. ((mdr_a_integer_recursionsecondhscrc = ((mdr_q_integer_recursionsecondhs) + (mdr_up_integer_recursionsecondhsc)) * S ((mdr_q_integer_recursionsecondhs) + (mdr_up_integer_recursionsecondhsc)) + ((mdr_up_integer_recursionsecondhsc) + (mdr_up_integer_recursionsecondhsc))) /\ ((mdr_b_integer_recursionsecondhscrc = ((mdr_us_integer_recursionsecondhsc) + (mdr_un_integer_recursionsecondhsc)) * S ((mdr_us_integer_recursionsecondhsc) + (mdr_un_integer_recursionsecondhsc)) + ((mdr_un_integer_recursionsecondhsc) + (mdr_un_integer_recursionsecondhsc))) /\ ((mdr_c_integer_recursionsecondhscrc = ((mdr_a_integer_recursionsecondhscrc) + (mdr_b_integer_recursionsecondhscrc)) * S ((mdr_a_integer_recursionsecondhscrc) + (mdr_b_integer_recursionsecondhscrc)) + ((mdr_b_integer_recursionsecondhscrc) + (mdr_b_integer_recursionsecondhscrc))) /\ ((mdr_e_integer_recursionsecondhscrc = ((mdr_p_integer_recursionsecondhsc) + (mdr_n_integer_recursionsecondhsc)) * S ((mdr_p_integer_recursionsecondhsc) + (mdr_n_integer_recursionsecondhsc)) + ((mdr_n_integer_recursionsecondhsc) + (mdr_n_integer_recursionsecondhsc))) /\ ((mdr_f_integer_recursionsecondhscrc = ((mdr_ut_integer_recursionsecondhsc) + (mdr_e_integer_recursionsecondhscrc)) * S ((mdr_ut_integer_recursionsecondhsc) + (mdr_e_integer_recursionsecondhscrc)) + ((mdr_e_integer_recursionsecondhscrc) + (mdr_e_integer_recursionsecondhscrc))) /\ ((mdr_z_integer_recursionsecondhscr) = ((mdr_c_integer_recursionsecondhscrc) + (mdr_f_integer_recursionsecondhscrc)) * S ((mdr_c_integer_recursionsecondhscrc) + (mdr_f_integer_recursionsecondhscrc)) + ((mdr_f_integer_recursionsecondhscrc) + (mdr_f_integer_recursionsecondhscrc))))))))) /\ (((exists ff_h_mdr_integer_recursionsecondhscrb. ff_h_mdr_integer_recursionsecondhscrb + S (mdr_z_integer_recursionsecondhscr) = S ((S (mdr_i_integer_recursionsecondhsc)) * mdr_c_integer_recursionsecond)) /\ exists ff_q_mdr_integer_recursionsecondhscrb. mdr_b_integer_recursionsecond = ff_q_mdr_integer_recursionsecondhscrb * S ((S (mdr_i_integer_recursionsecondhsc)) * mdr_c_integer_recursionsecond) + (mdr_z_integer_recursionsecondhscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_integer_recursionsecondhscm_positive. (exists ff_gap_mdm_lt_mdr_integer_recursionsecondhscm_positive_index_bound. ff_gap_mdm_lt_mdr_integer_recursionsecondhscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_integer_recursionsecondhscm_positive) = ((mdr_q_integer_recursionsecondhs) * (mdr_q_integer_recursionsecondhs))) -> exists ff_row_mdm_prefix_mdr_integer_recursionsecondhscm_positive ff_column_mdm_prefix_mdr_integer_recursionsecondhscm_positive ff_value_mdm_prefix_mdr_integer_recursionsecondhscm_positive. (ff_index_mdm_prefix_mdr_integer_recursionsecondhscm_positive = (mdr_q_integer_recursionsecondhs) * ff_row_mdm_prefix_mdr_integer_recursionsecondhscm_positive + ff_column_mdm_prefix_mdr_integer_recursionsecondhscm_positive /\ ((exists ff_gap_mdm_lt_mdr_integer_recursionsecondhscm_positive_column_bound. ff_gap_mdm_lt_mdr_integer_recursionsecondhscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_integer_recursionsecondhscm_positive) = (mdr_q_integer_recursionsecondhs)) /\ ((exists ff_row_mdm_cell_mdr_integer_recursionsecondhscm_positive_cell ff_column_mdm_cell_mdr_integer_recursionsecondhscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_integer_recursionsecondhscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_integer_recursionsecondhscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_integer_recursionsecondhscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_integer_recursionsecondhscm_positive_cell = ff_row_mdm_prefix_mdr_integer_recursionsecondhscm_positive) \/ ((exists ff_gap_mdm_le_mdr_integer_recursionsecondhscm_positive_cell_row_after. ff_gap_mdm_le_mdr_integer_recursionsecondhscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_integer_recursionsecondhscm_positive)) /\ ff_row_mdm_cell_mdr_integer_recursionsecondhscm_positive_cell = S ff_row_mdm_prefix_mdr_integer_recursionsecondhscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_integer_recursionsecondhscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_integer_recursionsecondhscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_integer_recursionsecondhscm_positive) = (mdr_j_integer_recursionsecondhsc)) /\ ff_column_mdm_cell_mdr_integer_recursionsecondhscm_positive_cell = ff_column_mdm_prefix_mdr_integer_recursionsecondhscm_positive) \/ ((exists ff_gap_mdm_le_mdr_integer_recursionsecondhscm_positive_cell_column_after. ff_gap_mdm_le_mdr_integer_recursionsecondhscm_positive_cell_column_after + (mdr_j_integer_recursionsecondhsc) = (ff_column_mdm_prefix_mdr_integer_recursionsecondhscm_positive)) /\ ff_column_mdm_cell_mdr_integer_recursionsecondhscm_positive_cell = S ff_column_mdm_prefix_mdr_integer_recursionsecondhscm_positive))) /\ (((exists ff_h_mdm_mdr_integer_recursionsecondhscm_positive_cell_source. ff_h_mdm_mdr_integer_recursionsecondhscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_integer_recursionsecondhscm_positive) = S ((S ((ff_row_mdm_cell_mdr_integer_recursionsecondhscm_positive_cell) * (S (mdr_q_integer_recursionsecondhs)) + (ff_column_mdm_cell_mdr_integer_recursionsecondhscm_positive_cell))) * mdr_pc_integer_recursionsecondh)) /\ exists ff_q_mdm_mdr_integer_recursionsecondhscm_positive_cell_source. mdr_pb_integer_recursionsecondh = ff_q_mdm_mdr_integer_recursionsecondhscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_integer_recursionsecondhscm_positive_cell) * (S (mdr_q_integer_recursionsecondhs)) + (ff_column_mdm_cell_mdr_integer_recursionsecondhscm_positive_cell))) * mdr_pc_integer_recursionsecondh) + (ff_value_mdm_prefix_mdr_integer_recursionsecondhscm_positive)))))) /\ (((exists ff_h_mdm_mdr_integer_recursionsecondhscm_positive_target. ff_h_mdm_mdr_integer_recursionsecondhscm_positive_target + S (ff_value_mdm_prefix_mdr_integer_recursionsecondhscm_positive) = S ((S (ff_index_mdm_prefix_mdr_integer_recursionsecondhscm_positive)) * mdr_us_integer_recursionsecondhsc)) /\ exists ff_q_mdm_mdr_integer_recursionsecondhscm_positive_target. mdr_up_integer_recursionsecondhsc = ff_q_mdm_mdr_integer_recursionsecondhscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_integer_recursionsecondhscm_positive)) * mdr_us_integer_recursionsecondhsc) + (ff_value_mdm_prefix_mdr_integer_recursionsecondhscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_integer_recursionsecondhscm_negative. (exists ff_gap_mdm_lt_mdr_integer_recursionsecondhscm_negative_index_bound. ff_gap_mdm_lt_mdr_integer_recursionsecondhscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_integer_recursionsecondhscm_negative) = ((mdr_q_integer_recursionsecondhs) * (mdr_q_integer_recursionsecondhs))) -> exists ff_row_mdm_prefix_mdr_integer_recursionsecondhscm_negative ff_column_mdm_prefix_mdr_integer_recursionsecondhscm_negative ff_value_mdm_prefix_mdr_integer_recursionsecondhscm_negative. (ff_index_mdm_prefix_mdr_integer_recursionsecondhscm_negative = (mdr_q_integer_recursionsecondhs) * ff_row_mdm_prefix_mdr_integer_recursionsecondhscm_negative + ff_column_mdm_prefix_mdr_integer_recursionsecondhscm_negative /\ ((exists ff_gap_mdm_lt_mdr_integer_recursionsecondhscm_negative_column_bound. ff_gap_mdm_lt_mdr_integer_recursionsecondhscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_integer_recursionsecondhscm_negative) = (mdr_q_integer_recursionsecondhs)) /\ ((exists ff_row_mdm_cell_mdr_integer_recursionsecondhscm_negative_cell ff_column_mdm_cell_mdr_integer_recursionsecondhscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_integer_recursionsecondhscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_integer_recursionsecondhscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_integer_recursionsecondhscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_integer_recursionsecondhscm_negative_cell = ff_row_mdm_prefix_mdr_integer_recursionsecondhscm_negative) \/ ((exists ff_gap_mdm_le_mdr_integer_recursionsecondhscm_negative_cell_row_after. ff_gap_mdm_le_mdr_integer_recursionsecondhscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_integer_recursionsecondhscm_negative)) /\ ff_row_mdm_cell_mdr_integer_recursionsecondhscm_negative_cell = S ff_row_mdm_prefix_mdr_integer_recursionsecondhscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_integer_recursionsecondhscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_integer_recursionsecondhscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_integer_recursionsecondhscm_negative) = (mdr_j_integer_recursionsecondhsc)) /\ ff_column_mdm_cell_mdr_integer_recursionsecondhscm_negative_cell = ff_column_mdm_prefix_mdr_integer_recursionsecondhscm_negative) \/ ((exists ff_gap_mdm_le_mdr_integer_recursionsecondhscm_negative_cell_column_after. ff_gap_mdm_le_mdr_integer_recursionsecondhscm_negative_cell_column_after + (mdr_j_integer_recursionsecondhsc) = (ff_column_mdm_prefix_mdr_integer_recursionsecondhscm_negative)) /\ ff_column_mdm_cell_mdr_integer_recursionsecondhscm_negative_cell = S ff_column_mdm_prefix_mdr_integer_recursionsecondhscm_negative))) /\ (((exists ff_h_mdm_mdr_integer_recursionsecondhscm_negative_cell_source. ff_h_mdm_mdr_integer_recursionsecondhscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_integer_recursionsecondhscm_negative) = S ((S ((ff_row_mdm_cell_mdr_integer_recursionsecondhscm_negative_cell) * (S (mdr_q_integer_recursionsecondhs)) + (ff_column_mdm_cell_mdr_integer_recursionsecondhscm_negative_cell))) * mdr_nc_integer_recursionsecondh)) /\ exists ff_q_mdm_mdr_integer_recursionsecondhscm_negative_cell_source. mdr_nb_integer_recursionsecondh = ff_q_mdm_mdr_integer_recursionsecondhscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_integer_recursionsecondhscm_negative_cell) * (S (mdr_q_integer_recursionsecondhs)) + (ff_column_mdm_cell_mdr_integer_recursionsecondhscm_negative_cell))) * mdr_nc_integer_recursionsecondh) + (ff_value_mdm_prefix_mdr_integer_recursionsecondhscm_negative)))))) /\ (((exists ff_h_mdm_mdr_integer_recursionsecondhscm_negative_target. ff_h_mdm_mdr_integer_recursionsecondhscm_negative_target + S (ff_value_mdm_prefix_mdr_integer_recursionsecondhscm_negative) = S ((S (ff_index_mdm_prefix_mdr_integer_recursionsecondhscm_negative)) * mdr_ut_integer_recursionsecondhsc)) /\ exists ff_q_mdm_mdr_integer_recursionsecondhscm_negative_target. mdr_un_integer_recursionsecondhsc = ff_q_mdm_mdr_integer_recursionsecondhscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_integer_recursionsecondhscm_negative)) * mdr_ut_integer_recursionsecondhsc) + (ff_value_mdm_prefix_mdr_integer_recursionsecondhscm_negative))))))))) /\ ((((exists ff_h_mdr_integer_recursionsecondhscp. ff_h_mdr_integer_recursionsecondhscp + S (mdr_p_integer_recursionsecondhsc) = S ((S (mdr_j_integer_recursionsecondhsc)) * mdr_ec_integer_recursionsecondhs)) /\ exists ff_q_mdr_integer_recursionsecondhscp. mdr_eb_integer_recursionsecondhs = ff_q_mdr_integer_recursionsecondhscp * S ((S (mdr_j_integer_recursionsecondhsc)) * mdr_ec_integer_recursionsecondhs) + (mdr_p_integer_recursionsecondhsc))) /\ (((exists ff_h_mdr_integer_recursionsecondhscn. ff_h_mdr_integer_recursionsecondhscn + S (mdr_n_integer_recursionsecondhsc) = S ((S (mdr_j_integer_recursionsecondhsc)) * mdr_fc_integer_recursionsecondhs)) /\ exists ff_q_mdr_integer_recursionsecondhscn. mdr_fb_integer_recursionsecondhs = ff_q_mdr_integer_recursionsecondhscn * S ((S (mdr_j_integer_recursionsecondhsc)) * mdr_fc_integer_recursionsecondhs) + (mdr_n_integer_recursionsecondhsc)))))))) /\ (exists ff_ub_mce_fold_mdr_integer_recursionsecondhsf ff_uc_mce_fold_mdr_integer_recursionsecondhsf ff_vb_mce_fold_mdr_integer_recursionsecondhsf ff_vc_mce_fold_mdr_integer_recursionsecondhsf. ((forall ff_index_mce_alternating_mdr_integer_recursionsecondhsf_prefix. (exists ff_gap_mce_mdr_integer_recursionsecondhsf_prefix_index. ff_gap_mce_mdr_integer_recursionsecondhsf_prefix_index + S (ff_index_mce_alternating_mdr_integer_recursionsecondhsf_prefix) = (S (mdr_q_integer_recursionsecondhs))) -> exists ff_ap_mce_alternating_mdr_integer_recursionsecondhsf_prefix ff_an_mce_alternating_mdr_integer_recursionsecondhsf_prefix ff_bp_mce_alternating_mdr_integer_recursionsecondhsf_prefix ff_bn_mce_alternating_mdr_integer_recursionsecondhsf_prefix ff_p_mce_alternating_mdr_integer_recursionsecondhsf_prefix ff_n_mce_alternating_mdr_integer_recursionsecondhsf_prefix. ((((exists ff_h_mce_mdr_integer_recursionsecondhsf_prefix_ap. ff_h_mce_mdr_integer_recursionsecondhsf_prefix_ap + S (ff_ap_mce_alternating_mdr_integer_recursionsecondhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_integer_recursionsecondhsf_prefix)) * mdr_pc_integer_recursionsecondh)) /\ exists ff_q_mce_mdr_integer_recursionsecondhsf_prefix_ap. mdr_pb_integer_recursionsecondh = ff_q_mce_mdr_integer_recursionsecondhsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_integer_recursionsecondhsf_prefix)) * mdr_pc_integer_recursionsecondh) + (ff_ap_mce_alternating_mdr_integer_recursionsecondhsf_prefix))) /\ ((((exists ff_h_mce_mdr_integer_recursionsecondhsf_prefix_an. ff_h_mce_mdr_integer_recursionsecondhsf_prefix_an + S (ff_an_mce_alternating_mdr_integer_recursionsecondhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_integer_recursionsecondhsf_prefix)) * mdr_nc_integer_recursionsecondh)) /\ exists ff_q_mce_mdr_integer_recursionsecondhsf_prefix_an. mdr_nb_integer_recursionsecondh = ff_q_mce_mdr_integer_recursionsecondhsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_integer_recursionsecondhsf_prefix)) * mdr_nc_integer_recursionsecondh) + (ff_an_mce_alternating_mdr_integer_recursionsecondhsf_prefix))) /\ ((((exists ff_h_mce_mdr_integer_recursionsecondhsf_prefix_bp. ff_h_mce_mdr_integer_recursionsecondhsf_prefix_bp + S (ff_bp_mce_alternating_mdr_integer_recursionsecondhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_integer_recursionsecondhsf_prefix)) * mdr_ec_integer_recursionsecondhs)) /\ exists ff_q_mce_mdr_integer_recursionsecondhsf_prefix_bp. mdr_eb_integer_recursionsecondhs = ff_q_mce_mdr_integer_recursionsecondhsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_integer_recursionsecondhsf_prefix)) * mdr_ec_integer_recursionsecondhs) + (ff_bp_mce_alternating_mdr_integer_recursionsecondhsf_prefix))) /\ ((((exists ff_h_mce_mdr_integer_recursionsecondhsf_prefix_bn. ff_h_mce_mdr_integer_recursionsecondhsf_prefix_bn + S (ff_bn_mce_alternating_mdr_integer_recursionsecondhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_integer_recursionsecondhsf_prefix)) * mdr_fc_integer_recursionsecondhs)) /\ exists ff_q_mce_mdr_integer_recursionsecondhsf_prefix_bn. mdr_fb_integer_recursionsecondhs = ff_q_mce_mdr_integer_recursionsecondhsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_integer_recursionsecondhsf_prefix)) * mdr_fc_integer_recursionsecondhs) + (ff_bn_mce_alternating_mdr_integer_recursionsecondhsf_prefix))) /\ ((((exists ff_h_mce_mdr_integer_recursionsecondhsf_prefix_positive. ff_h_mce_mdr_integer_recursionsecondhsf_prefix_positive + S (ff_p_mce_alternating_mdr_integer_recursionsecondhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_integer_recursionsecondhsf_prefix)) * ff_uc_mce_fold_mdr_integer_recursionsecondhsf)) /\ exists ff_q_mce_mdr_integer_recursionsecondhsf_prefix_positive. ff_ub_mce_fold_mdr_integer_recursionsecondhsf = ff_q_mce_mdr_integer_recursionsecondhsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_integer_recursionsecondhsf_prefix)) * ff_uc_mce_fold_mdr_integer_recursionsecondhsf) + (ff_p_mce_alternating_mdr_integer_recursionsecondhsf_prefix))) /\ ((((exists ff_h_mce_mdr_integer_recursionsecondhsf_prefix_negative. ff_h_mce_mdr_integer_recursionsecondhsf_prefix_negative + S (ff_n_mce_alternating_mdr_integer_recursionsecondhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_integer_recursionsecondhsf_prefix)) * ff_vc_mce_fold_mdr_integer_recursionsecondhsf)) /\ exists ff_q_mce_mdr_integer_recursionsecondhsf_prefix_negative. ff_vb_mce_fold_mdr_integer_recursionsecondhsf = ff_q_mce_mdr_integer_recursionsecondhsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_integer_recursionsecondhsf_prefix)) * ff_vc_mce_fold_mdr_integer_recursionsecondhsf) + (ff_n_mce_alternating_mdr_integer_recursionsecondhsf_prefix))) /\ (((exists ff_even_mce_term_mdr_integer_recursionsecondhsf_prefix_term. ff_index_mce_alternating_mdr_integer_recursionsecondhsf_prefix = 2 * ff_even_mce_term_mdr_integer_recursionsecondhsf_prefix_term) /\ (ff_p_mce_alternating_mdr_integer_recursionsecondhsf_prefix = (ff_ap_mce_alternating_mdr_integer_recursionsecondhsf_prefix) * (ff_bp_mce_alternating_mdr_integer_recursionsecondhsf_prefix) + (ff_an_mce_alternating_mdr_integer_recursionsecondhsf_prefix) * (ff_bn_mce_alternating_mdr_integer_recursionsecondhsf_prefix) /\ ff_n_mce_alternating_mdr_integer_recursionsecondhsf_prefix = (ff_ap_mce_alternating_mdr_integer_recursionsecondhsf_prefix) * (ff_bn_mce_alternating_mdr_integer_recursionsecondhsf_prefix) + (ff_an_mce_alternating_mdr_integer_recursionsecondhsf_prefix) * (ff_bp_mce_alternating_mdr_integer_recursionsecondhsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_integer_recursionsecondhsf_prefix_term. ff_index_mce_alternating_mdr_integer_recursionsecondhsf_prefix = 2 * ff_odd_mce_term_mdr_integer_recursionsecondhsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_integer_recursionsecondhsf_prefix = (ff_ap_mce_alternating_mdr_integer_recursionsecondhsf_prefix) * (ff_bn_mce_alternating_mdr_integer_recursionsecondhsf_prefix) + (ff_an_mce_alternating_mdr_integer_recursionsecondhsf_prefix) * (ff_bp_mce_alternating_mdr_integer_recursionsecondhsf_prefix) /\ ff_n_mce_alternating_mdr_integer_recursionsecondhsf_prefix = (ff_ap_mce_alternating_mdr_integer_recursionsecondhsf_prefix) * (ff_bp_mce_alternating_mdr_integer_recursionsecondhsf_prefix) + (ff_an_mce_alternating_mdr_integer_recursionsecondhsf_prefix) * (ff_bn_mce_alternating_mdr_integer_recursionsecondhsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_integer_recursionsecondhsf_positive ff_v_mce_mdr_integer_recursionsecondhsf_positive. ((((exists ff_h_mce_mdr_integer_recursionsecondhsf_positive_start. ff_h_mce_mdr_integer_recursionsecondhsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_integer_recursionsecondhsf_positive)) /\ exists ff_q_mce_mdr_integer_recursionsecondhsf_positive_start. ff_u_mce_mdr_integer_recursionsecondhsf_positive = ff_q_mce_mdr_integer_recursionsecondhsf_positive_start * S ((S (0)) * ff_v_mce_mdr_integer_recursionsecondhsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_integer_recursionsecondhsf_positive_terminal. ff_h_mce_mdr_integer_recursionsecondhsf_positive_terminal + S (mdr_p_integer_recursionsecondh) = S ((S ((S (mdr_q_integer_recursionsecondhs)))) * ff_v_mce_mdr_integer_recursionsecondhsf_positive)) /\ exists ff_q_mce_mdr_integer_recursionsecondhsf_positive_terminal. ff_u_mce_mdr_integer_recursionsecondhsf_positive = ff_q_mce_mdr_integer_recursionsecondhsf_positive_terminal * S ((S ((S (mdr_q_integer_recursionsecondhs)))) * ff_v_mce_mdr_integer_recursionsecondhsf_positive) + (mdr_p_integer_recursionsecondh))) /\ forall ff_i_mce_mdr_integer_recursionsecondhsf_positive. (exists ff_lt_mce_mdr_integer_recursionsecondhsf_positive_bound. ff_lt_mce_mdr_integer_recursionsecondhsf_positive_bound + S ff_i_mce_mdr_integer_recursionsecondhsf_positive = (S (mdr_q_integer_recursionsecondhs))) -> exists ff_a_mce_mdr_integer_recursionsecondhsf_positive ff_r_mce_mdr_integer_recursionsecondhsf_positive ff_s_mce_mdr_integer_recursionsecondhsf_positive. ((((exists ff_h_mce_mdr_integer_recursionsecondhsf_positive_summand. ff_h_mce_mdr_integer_recursionsecondhsf_positive_summand + S (ff_a_mce_mdr_integer_recursionsecondhsf_positive) = S ((S (ff_i_mce_mdr_integer_recursionsecondhsf_positive)) * ff_uc_mce_fold_mdr_integer_recursionsecondhsf)) /\ exists ff_q_mce_mdr_integer_recursionsecondhsf_positive_summand. ff_ub_mce_fold_mdr_integer_recursionsecondhsf = ff_q_mce_mdr_integer_recursionsecondhsf_positive_summand * S ((S (ff_i_mce_mdr_integer_recursionsecondhsf_positive)) * ff_uc_mce_fold_mdr_integer_recursionsecondhsf) + (ff_a_mce_mdr_integer_recursionsecondhsf_positive))) /\ ((((exists ff_h_mce_mdr_integer_recursionsecondhsf_positive_partial. ff_h_mce_mdr_integer_recursionsecondhsf_positive_partial + S (ff_r_mce_mdr_integer_recursionsecondhsf_positive) = S ((S (ff_i_mce_mdr_integer_recursionsecondhsf_positive)) * ff_v_mce_mdr_integer_recursionsecondhsf_positive)) /\ exists ff_q_mce_mdr_integer_recursionsecondhsf_positive_partial. ff_u_mce_mdr_integer_recursionsecondhsf_positive = ff_q_mce_mdr_integer_recursionsecondhsf_positive_partial * S ((S (ff_i_mce_mdr_integer_recursionsecondhsf_positive)) * ff_v_mce_mdr_integer_recursionsecondhsf_positive) + (ff_r_mce_mdr_integer_recursionsecondhsf_positive))) /\ ((((exists ff_h_mce_mdr_integer_recursionsecondhsf_positive_successor. ff_h_mce_mdr_integer_recursionsecondhsf_positive_successor + S (ff_s_mce_mdr_integer_recursionsecondhsf_positive) = S ((S (S ff_i_mce_mdr_integer_recursionsecondhsf_positive)) * ff_v_mce_mdr_integer_recursionsecondhsf_positive)) /\ exists ff_q_mce_mdr_integer_recursionsecondhsf_positive_successor. ff_u_mce_mdr_integer_recursionsecondhsf_positive = ff_q_mce_mdr_integer_recursionsecondhsf_positive_successor * S ((S (S ff_i_mce_mdr_integer_recursionsecondhsf_positive)) * ff_v_mce_mdr_integer_recursionsecondhsf_positive) + (ff_s_mce_mdr_integer_recursionsecondhsf_positive))) /\ ff_s_mce_mdr_integer_recursionsecondhsf_positive = ff_r_mce_mdr_integer_recursionsecondhsf_positive + ff_a_mce_mdr_integer_recursionsecondhsf_positive)))))) /\ (exists ff_u_mce_mdr_integer_recursionsecondhsf_negative ff_v_mce_mdr_integer_recursionsecondhsf_negative. ((((exists ff_h_mce_mdr_integer_recursionsecondhsf_negative_start. ff_h_mce_mdr_integer_recursionsecondhsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_integer_recursionsecondhsf_negative)) /\ exists ff_q_mce_mdr_integer_recursionsecondhsf_negative_start. ff_u_mce_mdr_integer_recursionsecondhsf_negative = ff_q_mce_mdr_integer_recursionsecondhsf_negative_start * S ((S (0)) * ff_v_mce_mdr_integer_recursionsecondhsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_integer_recursionsecondhsf_negative_terminal. ff_h_mce_mdr_integer_recursionsecondhsf_negative_terminal + S (mdr_n_integer_recursionsecondh) = S ((S ((S (mdr_q_integer_recursionsecondhs)))) * ff_v_mce_mdr_integer_recursionsecondhsf_negative)) /\ exists ff_q_mce_mdr_integer_recursionsecondhsf_negative_terminal. ff_u_mce_mdr_integer_recursionsecondhsf_negative = ff_q_mce_mdr_integer_recursionsecondhsf_negative_terminal * S ((S ((S (mdr_q_integer_recursionsecondhs)))) * ff_v_mce_mdr_integer_recursionsecondhsf_negative) + (mdr_n_integer_recursionsecondh))) /\ forall ff_i_mce_mdr_integer_recursionsecondhsf_negative. (exists ff_lt_mce_mdr_integer_recursionsecondhsf_negative_bound. ff_lt_mce_mdr_integer_recursionsecondhsf_negative_bound + S ff_i_mce_mdr_integer_recursionsecondhsf_negative = (S (mdr_q_integer_recursionsecondhs))) -> exists ff_a_mce_mdr_integer_recursionsecondhsf_negative ff_r_mce_mdr_integer_recursionsecondhsf_negative ff_s_mce_mdr_integer_recursionsecondhsf_negative. ((((exists ff_h_mce_mdr_integer_recursionsecondhsf_negative_summand. ff_h_mce_mdr_integer_recursionsecondhsf_negative_summand + S (ff_a_mce_mdr_integer_recursionsecondhsf_negative) = S ((S (ff_i_mce_mdr_integer_recursionsecondhsf_negative)) * ff_vc_mce_fold_mdr_integer_recursionsecondhsf)) /\ exists ff_q_mce_mdr_integer_recursionsecondhsf_negative_summand. ff_vb_mce_fold_mdr_integer_recursionsecondhsf = ff_q_mce_mdr_integer_recursionsecondhsf_negative_summand * S ((S (ff_i_mce_mdr_integer_recursionsecondhsf_negative)) * ff_vc_mce_fold_mdr_integer_recursionsecondhsf) + (ff_a_mce_mdr_integer_recursionsecondhsf_negative))) /\ ((((exists ff_h_mce_mdr_integer_recursionsecondhsf_negative_partial. ff_h_mce_mdr_integer_recursionsecondhsf_negative_partial + S (ff_r_mce_mdr_integer_recursionsecondhsf_negative) = S ((S (ff_i_mce_mdr_integer_recursionsecondhsf_negative)) * ff_v_mce_mdr_integer_recursionsecondhsf_negative)) /\ exists ff_q_mce_mdr_integer_recursionsecondhsf_negative_partial. ff_u_mce_mdr_integer_recursionsecondhsf_negative = ff_q_mce_mdr_integer_recursionsecondhsf_negative_partial * S ((S (ff_i_mce_mdr_integer_recursionsecondhsf_negative)) * ff_v_mce_mdr_integer_recursionsecondhsf_negative) + (ff_r_mce_mdr_integer_recursionsecondhsf_negative))) /\ ((((exists ff_h_mce_mdr_integer_recursionsecondhsf_negative_successor. ff_h_mce_mdr_integer_recursionsecondhsf_negative_successor + S (ff_s_mce_mdr_integer_recursionsecondhsf_negative) = S ((S (S ff_i_mce_mdr_integer_recursionsecondhsf_negative)) * ff_v_mce_mdr_integer_recursionsecondhsf_negative)) /\ exists ff_q_mce_mdr_integer_recursionsecondhsf_negative_successor. ff_u_mce_mdr_integer_recursionsecondhsf_negative = ff_q_mce_mdr_integer_recursionsecondhsf_negative_successor * S ((S (S ff_i_mce_mdr_integer_recursionsecondhsf_negative)) * ff_v_mce_mdr_integer_recursionsecondhsf_negative) + (ff_s_mce_mdr_integer_recursionsecondhsf_negative))) /\ ff_s_mce_mdr_integer_recursionsecondhsf_negative = ff_r_mce_mdr_integer_recursionsecondhsf_negative + ff_a_mce_mdr_integer_recursionsecondhsf_negative))))))))))))))) /\ ((exists mdr_gap_integer_recursionsecondi. mdr_gap_integer_recursionsecondi + S (mdr_i_integer_recursionsecond) = (mdr_l_integer_recursionsecond)) /\ (exists mdr_z_integer_recursionsecondr. ((exists mdr_a_integer_recursionsecondrc mdr_b_integer_recursionsecondrc mdr_c_integer_recursionsecondrc mdr_e_integer_recursionsecondrc mdr_f_integer_recursionsecondrc. ((mdr_a_integer_recursionsecondrc = ((q) + (mdr_eb_integer_recursion)) * S ((q) + (mdr_eb_integer_recursion)) + ((mdr_eb_integer_recursion) + (mdr_eb_integer_recursion))) /\ ((mdr_b_integer_recursionsecondrc = ((mdr_ec_integer_recursion) + (mdr_fb_integer_recursion)) * S ((mdr_ec_integer_recursion) + (mdr_fb_integer_recursion)) + ((mdr_fb_integer_recursion) + (mdr_fb_integer_recursion))) /\ ((mdr_c_integer_recursionsecondrc = ((mdr_a_integer_recursionsecondrc) + (mdr_b_integer_recursionsecondrc)) * S ((mdr_a_integer_recursionsecondrc) + (mdr_b_integer_recursionsecondrc)) + ((mdr_b_integer_recursionsecondrc) + (mdr_b_integer_recursionsecondrc))) /\ ((mdr_e_integer_recursionsecondrc = ((mdr_P_integer_recursion) + (mdr_N_integer_recursion)) * S ((mdr_P_integer_recursion) + (mdr_N_integer_recursion)) + ((mdr_N_integer_recursion) + (mdr_N_integer_recursion))) /\ ((mdr_f_integer_recursionsecondrc = ((mdr_fc_integer_recursion) + (mdr_e_integer_recursionsecondrc)) * S ((mdr_fc_integer_recursion) + (mdr_e_integer_recursionsecondrc)) + ((mdr_e_integer_recursionsecondrc) + (mdr_e_integer_recursionsecondrc))) /\ ((mdr_z_integer_recursionsecondr) = ((mdr_c_integer_recursionsecondrc) + (mdr_f_integer_recursionsecondrc)) * S ((mdr_c_integer_recursionsecondrc) + (mdr_f_integer_recursionsecondrc)) + ((mdr_f_integer_recursionsecondrc) + (mdr_f_integer_recursionsecondrc))))))))) /\ (((exists ff_h_mdr_integer_recursionsecondrb. ff_h_mdr_integer_recursionsecondrb + S (mdr_z_integer_recursionsecondr) = S ((S (mdr_i_integer_recursionsecond)) * mdr_c_integer_recursionsecond)) /\ exists ff_q_mdr_integer_recursionsecondrb. mdr_b_integer_recursionsecond = ff_q_mdr_integer_recursionsecondrb * S ((S (mdr_i_integer_recursionsecond)) * mdr_c_integer_recursionsecond) + (mdr_z_integer_recursionsecondr)))))))) -> mdr_p_integer_recursion + mdr_N_integer_recursion = mdr_P_integer_recursion + mdr_n_integer_recursion) -> (forall ics_index_integer_cofactor_parents ics_value0_integer_cofactor_parents ics_value1_integer_cofactor_parents ics_value2_integer_cofactor_parents ics_value3_integer_cofactor_parents. (exists ics_gap_integer_cofactor_parents_bound. ics_gap_integer_cofactor_parents_bound + S (ics_index_integer_cofactor_parents) = ((S q) * (S q))) -> (((exists fs_h_ics_integer_cofactor_parents_at0. fs_h_ics_integer_cofactor_parents_at0 + S (ics_value0_integer_cofactor_parents) = S ((S (ics_index_integer_cofactor_parents)) * ac)) /\ exists fs_q_ics_integer_cofactor_parents_at0. ab = fs_q_ics_integer_cofactor_parents_at0 * S ((S (ics_index_integer_cofactor_parents)) * ac) + (ics_value0_integer_cofactor_parents))) -> (((exists fs_h_ics_integer_cofactor_parents_at1. fs_h_ics_integer_cofactor_parents_at1 + S (ics_value1_integer_cofactor_parents) = S ((S (ics_index_integer_cofactor_parents)) * bc)) /\ exists fs_q_ics_integer_cofactor_parents_at1. bb = fs_q_ics_integer_cofactor_parents_at1 * S ((S (ics_index_integer_cofactor_parents)) * bc) + (ics_value1_integer_cofactor_parents))) -> (((exists fs_h_ics_integer_cofactor_parents_at2. fs_h_ics_integer_cofactor_parents_at2 + S (ics_value2_integer_cofactor_parents) = S ((S (ics_index_integer_cofactor_parents)) * ec)) /\ exists fs_q_ics_integer_cofactor_parents_at2. eb = fs_q_ics_integer_cofactor_parents_at2 * S ((S (ics_index_integer_cofactor_parents)) * ec) + (ics_value2_integer_cofactor_parents))) -> (((exists fs_h_ics_integer_cofactor_parents_at3. fs_h_ics_integer_cofactor_parents_at3 + S (ics_value3_integer_cofactor_parents) = S ((S (ics_index_integer_cofactor_parents)) * fc)) /\ exists fs_q_ics_integer_cofactor_parents_at3. fb = fs_q_ics_integer_cofactor_parents_at3 * S ((S (ics_index_integer_cofactor_parents)) * fc) + (ics_value3_integer_cofactor_parents))) -> ics_value0_integer_cofactor_parents + ics_value3_integer_cofactor_parents = ics_value2_integer_cofactor_parents + ics_value1_integer_cofactor_parents) -> (forall mdr_j_integer_cofactor_first. (exists mdr_gap_integer_cofactor_firstj. mdr_gap_integer_cofactor_firstj + S (mdr_j_integer_cofactor_first) = (S (q))) -> exists mdr_up_integer_cofactor_first mdr_us_integer_cofactor_first mdr_un_integer_cofactor_first mdr_ut_integer_cofactor_first mdr_p_integer_cofactor_first mdr_n_integer_cofactor_first. ((((forall ff_index_mdm_prefix_mdr_integer_cofactor_firstm_positive. (exists ff_gap_mdm_lt_mdr_integer_cofactor_firstm_positive_index_bound. ff_gap_mdm_lt_mdr_integer_cofactor_firstm_positive_index_bound + S (ff_index_mdm_prefix_mdr_integer_cofactor_firstm_positive) = ((q) * (q))) -> exists ff_row_mdm_prefix_mdr_integer_cofactor_firstm_positive ff_column_mdm_prefix_mdr_integer_cofactor_firstm_positive ff_value_mdm_prefix_mdr_integer_cofactor_firstm_positive. (ff_index_mdm_prefix_mdr_integer_cofactor_firstm_positive = (q) * ff_row_mdm_prefix_mdr_integer_cofactor_firstm_positive + ff_column_mdm_prefix_mdr_integer_cofactor_firstm_positive /\ ((exists ff_gap_mdm_lt_mdr_integer_cofactor_firstm_positive_column_bound. ff_gap_mdm_lt_mdr_integer_cofactor_firstm_positive_column_bound + S (ff_column_mdm_prefix_mdr_integer_cofactor_firstm_positive) = (q)) /\ ((exists ff_row_mdm_cell_mdr_integer_cofactor_firstm_positive_cell ff_column_mdm_cell_mdr_integer_cofactor_firstm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_integer_cofactor_firstm_positive_cell_row_before. ff_gap_mdm_lt_mdr_integer_cofactor_firstm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_integer_cofactor_firstm_positive) = (0)) /\ ff_row_mdm_cell_mdr_integer_cofactor_firstm_positive_cell = ff_row_mdm_prefix_mdr_integer_cofactor_firstm_positive) \/ ((exists ff_gap_mdm_le_mdr_integer_cofactor_firstm_positive_cell_row_after. ff_gap_mdm_le_mdr_integer_cofactor_firstm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_integer_cofactor_firstm_positive)) /\ ff_row_mdm_cell_mdr_integer_cofactor_firstm_positive_cell = S ff_row_mdm_prefix_mdr_integer_cofactor_firstm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_integer_cofactor_firstm_positive_cell_column_before. ff_gap_mdm_lt_mdr_integer_cofactor_firstm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_integer_cofactor_firstm_positive) = (mdr_j_integer_cofactor_first)) /\ ff_column_mdm_cell_mdr_integer_cofactor_firstm_positive_cell = ff_column_mdm_prefix_mdr_integer_cofactor_firstm_positive) \/ ((exists ff_gap_mdm_le_mdr_integer_cofactor_firstm_positive_cell_column_after. ff_gap_mdm_le_mdr_integer_cofactor_firstm_positive_cell_column_after + (mdr_j_integer_cofactor_first) = (ff_column_mdm_prefix_mdr_integer_cofactor_firstm_positive)) /\ ff_column_mdm_cell_mdr_integer_cofactor_firstm_positive_cell = S ff_column_mdm_prefix_mdr_integer_cofactor_firstm_positive))) /\ (((exists ff_h_mdm_mdr_integer_cofactor_firstm_positive_cell_source. ff_h_mdm_mdr_integer_cofactor_firstm_positive_cell_source + S (ff_value_mdm_prefix_mdr_integer_cofactor_firstm_positive) = S ((S ((ff_row_mdm_cell_mdr_integer_cofactor_firstm_positive_cell) * (S (q)) + (ff_column_mdm_cell_mdr_integer_cofactor_firstm_positive_cell))) * ac)) /\ exists ff_q_mdm_mdr_integer_cofactor_firstm_positive_cell_source. ab = ff_q_mdm_mdr_integer_cofactor_firstm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_integer_cofactor_firstm_positive_cell) * (S (q)) + (ff_column_mdm_cell_mdr_integer_cofactor_firstm_positive_cell))) * ac) + (ff_value_mdm_prefix_mdr_integer_cofactor_firstm_positive)))))) /\ (((exists ff_h_mdm_mdr_integer_cofactor_firstm_positive_target. ff_h_mdm_mdr_integer_cofactor_firstm_positive_target + S (ff_value_mdm_prefix_mdr_integer_cofactor_firstm_positive) = S ((S (ff_index_mdm_prefix_mdr_integer_cofactor_firstm_positive)) * mdr_us_integer_cofactor_first)) /\ exists ff_q_mdm_mdr_integer_cofactor_firstm_positive_target. mdr_up_integer_cofactor_first = ff_q_mdm_mdr_integer_cofactor_firstm_positive_target * S ((S (ff_index_mdm_prefix_mdr_integer_cofactor_firstm_positive)) * mdr_us_integer_cofactor_first) + (ff_value_mdm_prefix_mdr_integer_cofactor_firstm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_integer_cofactor_firstm_negative. (exists ff_gap_mdm_lt_mdr_integer_cofactor_firstm_negative_index_bound. ff_gap_mdm_lt_mdr_integer_cofactor_firstm_negative_index_bound + S (ff_index_mdm_prefix_mdr_integer_cofactor_firstm_negative) = ((q) * (q))) -> exists ff_row_mdm_prefix_mdr_integer_cofactor_firstm_negative ff_column_mdm_prefix_mdr_integer_cofactor_firstm_negative ff_value_mdm_prefix_mdr_integer_cofactor_firstm_negative. (ff_index_mdm_prefix_mdr_integer_cofactor_firstm_negative = (q) * ff_row_mdm_prefix_mdr_integer_cofactor_firstm_negative + ff_column_mdm_prefix_mdr_integer_cofactor_firstm_negative /\ ((exists ff_gap_mdm_lt_mdr_integer_cofactor_firstm_negative_column_bound. ff_gap_mdm_lt_mdr_integer_cofactor_firstm_negative_column_bound + S (ff_column_mdm_prefix_mdr_integer_cofactor_firstm_negative) = (q)) /\ ((exists ff_row_mdm_cell_mdr_integer_cofactor_firstm_negative_cell ff_column_mdm_cell_mdr_integer_cofactor_firstm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_integer_cofactor_firstm_negative_cell_row_before. ff_gap_mdm_lt_mdr_integer_cofactor_firstm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_integer_cofactor_firstm_negative) = (0)) /\ ff_row_mdm_cell_mdr_integer_cofactor_firstm_negative_cell = ff_row_mdm_prefix_mdr_integer_cofactor_firstm_negative) \/ ((exists ff_gap_mdm_le_mdr_integer_cofactor_firstm_negative_cell_row_after. ff_gap_mdm_le_mdr_integer_cofactor_firstm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_integer_cofactor_firstm_negative)) /\ ff_row_mdm_cell_mdr_integer_cofactor_firstm_negative_cell = S ff_row_mdm_prefix_mdr_integer_cofactor_firstm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_integer_cofactor_firstm_negative_cell_column_before. ff_gap_mdm_lt_mdr_integer_cofactor_firstm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_integer_cofactor_firstm_negative) = (mdr_j_integer_cofactor_first)) /\ ff_column_mdm_cell_mdr_integer_cofactor_firstm_negative_cell = ff_column_mdm_prefix_mdr_integer_cofactor_firstm_negative) \/ ((exists ff_gap_mdm_le_mdr_integer_cofactor_firstm_negative_cell_column_after. ff_gap_mdm_le_mdr_integer_cofactor_firstm_negative_cell_column_after + (mdr_j_integer_cofactor_first) = (ff_column_mdm_prefix_mdr_integer_cofactor_firstm_negative)) /\ ff_column_mdm_cell_mdr_integer_cofactor_firstm_negative_cell = S ff_column_mdm_prefix_mdr_integer_cofactor_firstm_negative))) /\ (((exists ff_h_mdm_mdr_integer_cofactor_firstm_negative_cell_source. ff_h_mdm_mdr_integer_cofactor_firstm_negative_cell_source + S (ff_value_mdm_prefix_mdr_integer_cofactor_firstm_negative) = S ((S ((ff_row_mdm_cell_mdr_integer_cofactor_firstm_negative_cell) * (S (q)) + (ff_column_mdm_cell_mdr_integer_cofactor_firstm_negative_cell))) * bc)) /\ exists ff_q_mdm_mdr_integer_cofactor_firstm_negative_cell_source. bb = ff_q_mdm_mdr_integer_cofactor_firstm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_integer_cofactor_firstm_negative_cell) * (S (q)) + (ff_column_mdm_cell_mdr_integer_cofactor_firstm_negative_cell))) * bc) + (ff_value_mdm_prefix_mdr_integer_cofactor_firstm_negative)))))) /\ (((exists ff_h_mdm_mdr_integer_cofactor_firstm_negative_target. ff_h_mdm_mdr_integer_cofactor_firstm_negative_target + S (ff_value_mdm_prefix_mdr_integer_cofactor_firstm_negative) = S ((S (ff_index_mdm_prefix_mdr_integer_cofactor_firstm_negative)) * mdr_ut_integer_cofactor_first)) /\ exists ff_q_mdm_mdr_integer_cofactor_firstm_negative_target. mdr_un_integer_cofactor_first = ff_q_mdm_mdr_integer_cofactor_firstm_negative_target * S ((S (ff_index_mdm_prefix_mdr_integer_cofactor_firstm_negative)) * mdr_ut_integer_cofactor_first) + (ff_value_mdm_prefix_mdr_integer_cofactor_firstm_negative))))))))) /\ ((exists mdr_b_integer_cofactor_firstd mdr_c_integer_cofactor_firstd mdr_l_integer_cofactor_firstd mdr_i_integer_cofactor_firstd. ((forall mdr_i_integer_cofactor_firstdh. (exists mdr_gap_integer_cofactor_firstdhi. mdr_gap_integer_cofactor_firstdhi + S (mdr_i_integer_cofactor_firstdh) = (mdr_l_integer_cofactor_firstd)) -> exists mdr_d_integer_cofactor_firstdh mdr_pb_integer_cofactor_firstdh mdr_pc_integer_cofactor_firstdh mdr_nb_integer_cofactor_firstdh mdr_nc_integer_cofactor_firstdh mdr_p_integer_cofactor_firstdh mdr_n_integer_cofactor_firstdh. ((exists mdr_z_integer_cofactor_firstdhr. ((exists mdr_a_integer_cofactor_firstdhrc mdr_b_integer_cofactor_firstdhrc mdr_c_integer_cofactor_firstdhrc mdr_e_integer_cofactor_firstdhrc mdr_f_integer_cofactor_firstdhrc. ((mdr_a_integer_cofactor_firstdhrc = ((mdr_d_integer_cofactor_firstdh) + (mdr_pb_integer_cofactor_firstdh)) * S ((mdr_d_integer_cofactor_firstdh) + (mdr_pb_integer_cofactor_firstdh)) + ((mdr_pb_integer_cofactor_firstdh) + (mdr_pb_integer_cofactor_firstdh))) /\ ((mdr_b_integer_cofactor_firstdhrc = ((mdr_pc_integer_cofactor_firstdh) + (mdr_nb_integer_cofactor_firstdh)) * S ((mdr_pc_integer_cofactor_firstdh) + (mdr_nb_integer_cofactor_firstdh)) + ((mdr_nb_integer_cofactor_firstdh) + (mdr_nb_integer_cofactor_firstdh))) /\ ((mdr_c_integer_cofactor_firstdhrc = ((mdr_a_integer_cofactor_firstdhrc) + (mdr_b_integer_cofactor_firstdhrc)) * S ((mdr_a_integer_cofactor_firstdhrc) + (mdr_b_integer_cofactor_firstdhrc)) + ((mdr_b_integer_cofactor_firstdhrc) + (mdr_b_integer_cofactor_firstdhrc))) /\ ((mdr_e_integer_cofactor_firstdhrc = ((mdr_p_integer_cofactor_firstdh) + (mdr_n_integer_cofactor_firstdh)) * S ((mdr_p_integer_cofactor_firstdh) + (mdr_n_integer_cofactor_firstdh)) + ((mdr_n_integer_cofactor_firstdh) + (mdr_n_integer_cofactor_firstdh))) /\ ((mdr_f_integer_cofactor_firstdhrc = ((mdr_nc_integer_cofactor_firstdh) + (mdr_e_integer_cofactor_firstdhrc)) * S ((mdr_nc_integer_cofactor_firstdh) + (mdr_e_integer_cofactor_firstdhrc)) + ((mdr_e_integer_cofactor_firstdhrc) + (mdr_e_integer_cofactor_firstdhrc))) /\ ((mdr_z_integer_cofactor_firstdhr) = ((mdr_c_integer_cofactor_firstdhrc) + (mdr_f_integer_cofactor_firstdhrc)) * S ((mdr_c_integer_cofactor_firstdhrc) + (mdr_f_integer_cofactor_firstdhrc)) + ((mdr_f_integer_cofactor_firstdhrc) + (mdr_f_integer_cofactor_firstdhrc))))))))) /\ (((exists ff_h_mdr_integer_cofactor_firstdhrb. ff_h_mdr_integer_cofactor_firstdhrb + S (mdr_z_integer_cofactor_firstdhr) = S ((S (mdr_i_integer_cofactor_firstdh)) * mdr_c_integer_cofactor_firstd)) /\ exists ff_q_mdr_integer_cofactor_firstdhrb. mdr_b_integer_cofactor_firstd = ff_q_mdr_integer_cofactor_firstdhrb * S ((S (mdr_i_integer_cofactor_firstdh)) * mdr_c_integer_cofactor_firstd) + (mdr_z_integer_cofactor_firstdhr))))) /\ (((((mdr_d_integer_cofactor_firstdh) = 0) /\ (((mdr_p_integer_cofactor_firstdh) = 1) /\ ((mdr_n_integer_cofactor_firstdh) = 0))) \/ exists mdr_q_integer_cofactor_firstdhs mdr_eb_integer_cofactor_firstdhs mdr_ec_integer_cofactor_firstdhs mdr_fb_integer_cofactor_firstdhs mdr_fc_integer_cofactor_firstdhs. (((mdr_d_integer_cofactor_firstdh) = S (mdr_q_integer_cofactor_firstdhs)) /\ ((forall mdr_j_integer_cofactor_firstdhsc. (exists mdr_gap_integer_cofactor_firstdhscj. mdr_gap_integer_cofactor_firstdhscj + S (mdr_j_integer_cofactor_firstdhsc) = (S (mdr_q_integer_cofactor_firstdhs))) -> exists mdr_i_integer_cofactor_firstdhsc mdr_up_integer_cofactor_firstdhsc mdr_us_integer_cofactor_firstdhsc mdr_un_integer_cofactor_firstdhsc mdr_ut_integer_cofactor_firstdhsc mdr_p_integer_cofactor_firstdhsc mdr_n_integer_cofactor_firstdhsc. ((exists mdr_gap_integer_cofactor_firstdhsci. mdr_gap_integer_cofactor_firstdhsci + S (mdr_i_integer_cofactor_firstdhsc) = (mdr_i_integer_cofactor_firstdh)) /\ ((exists mdr_z_integer_cofactor_firstdhscr. ((exists mdr_a_integer_cofactor_firstdhscrc mdr_b_integer_cofactor_firstdhscrc mdr_c_integer_cofactor_firstdhscrc mdr_e_integer_cofactor_firstdhscrc mdr_f_integer_cofactor_firstdhscrc. ((mdr_a_integer_cofactor_firstdhscrc = ((mdr_q_integer_cofactor_firstdhs) + (mdr_up_integer_cofactor_firstdhsc)) * S ((mdr_q_integer_cofactor_firstdhs) + (mdr_up_integer_cofactor_firstdhsc)) + ((mdr_up_integer_cofactor_firstdhsc) + (mdr_up_integer_cofactor_firstdhsc))) /\ ((mdr_b_integer_cofactor_firstdhscrc = ((mdr_us_integer_cofactor_firstdhsc) + (mdr_un_integer_cofactor_firstdhsc)) * S ((mdr_us_integer_cofactor_firstdhsc) + (mdr_un_integer_cofactor_firstdhsc)) + ((mdr_un_integer_cofactor_firstdhsc) + (mdr_un_integer_cofactor_firstdhsc))) /\ ((mdr_c_integer_cofactor_firstdhscrc = ((mdr_a_integer_cofactor_firstdhscrc) + (mdr_b_integer_cofactor_firstdhscrc)) * S ((mdr_a_integer_cofactor_firstdhscrc) + (mdr_b_integer_cofactor_firstdhscrc)) + ((mdr_b_integer_cofactor_firstdhscrc) + (mdr_b_integer_cofactor_firstdhscrc))) /\ ((mdr_e_integer_cofactor_firstdhscrc = ((mdr_p_integer_cofactor_firstdhsc) + (mdr_n_integer_cofactor_firstdhsc)) * S ((mdr_p_integer_cofactor_firstdhsc) + (mdr_n_integer_cofactor_firstdhsc)) + ((mdr_n_integer_cofactor_firstdhsc) + (mdr_n_integer_cofactor_firstdhsc))) /\ ((mdr_f_integer_cofactor_firstdhscrc = ((mdr_ut_integer_cofactor_firstdhsc) + (mdr_e_integer_cofactor_firstdhscrc)) * S ((mdr_ut_integer_cofactor_firstdhsc) + (mdr_e_integer_cofactor_firstdhscrc)) + ((mdr_e_integer_cofactor_firstdhscrc) + (mdr_e_integer_cofactor_firstdhscrc))) /\ ((mdr_z_integer_cofactor_firstdhscr) = ((mdr_c_integer_cofactor_firstdhscrc) + (mdr_f_integer_cofactor_firstdhscrc)) * S ((mdr_c_integer_cofactor_firstdhscrc) + (mdr_f_integer_cofactor_firstdhscrc)) + ((mdr_f_integer_cofactor_firstdhscrc) + (mdr_f_integer_cofactor_firstdhscrc))))))))) /\ (((exists ff_h_mdr_integer_cofactor_firstdhscrb. ff_h_mdr_integer_cofactor_firstdhscrb + S (mdr_z_integer_cofactor_firstdhscr) = S ((S (mdr_i_integer_cofactor_firstdhsc)) * mdr_c_integer_cofactor_firstd)) /\ exists ff_q_mdr_integer_cofactor_firstdhscrb. mdr_b_integer_cofactor_firstd = ff_q_mdr_integer_cofactor_firstdhscrb * S ((S (mdr_i_integer_cofactor_firstdhsc)) * mdr_c_integer_cofactor_firstd) + (mdr_z_integer_cofactor_firstdhscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_integer_cofactor_firstdhscm_positive. (exists ff_gap_mdm_lt_mdr_integer_cofactor_firstdhscm_positive_index_bound. ff_gap_mdm_lt_mdr_integer_cofactor_firstdhscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_integer_cofactor_firstdhscm_positive) = ((mdr_q_integer_cofactor_firstdhs) * (mdr_q_integer_cofactor_firstdhs))) -> exists ff_row_mdm_prefix_mdr_integer_cofactor_firstdhscm_positive ff_column_mdm_prefix_mdr_integer_cofactor_firstdhscm_positive ff_value_mdm_prefix_mdr_integer_cofactor_firstdhscm_positive. (ff_index_mdm_prefix_mdr_integer_cofactor_firstdhscm_positive = (mdr_q_integer_cofactor_firstdhs) * ff_row_mdm_prefix_mdr_integer_cofactor_firstdhscm_positive + ff_column_mdm_prefix_mdr_integer_cofactor_firstdhscm_positive /\ ((exists ff_gap_mdm_lt_mdr_integer_cofactor_firstdhscm_positive_column_bound. ff_gap_mdm_lt_mdr_integer_cofactor_firstdhscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_integer_cofactor_firstdhscm_positive) = (mdr_q_integer_cofactor_firstdhs)) /\ ((exists ff_row_mdm_cell_mdr_integer_cofactor_firstdhscm_positive_cell ff_column_mdm_cell_mdr_integer_cofactor_firstdhscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_integer_cofactor_firstdhscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_integer_cofactor_firstdhscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_integer_cofactor_firstdhscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_integer_cofactor_firstdhscm_positive_cell = ff_row_mdm_prefix_mdr_integer_cofactor_firstdhscm_positive) \/ ((exists ff_gap_mdm_le_mdr_integer_cofactor_firstdhscm_positive_cell_row_after. ff_gap_mdm_le_mdr_integer_cofactor_firstdhscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_integer_cofactor_firstdhscm_positive)) /\ ff_row_mdm_cell_mdr_integer_cofactor_firstdhscm_positive_cell = S ff_row_mdm_prefix_mdr_integer_cofactor_firstdhscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_integer_cofactor_firstdhscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_integer_cofactor_firstdhscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_integer_cofactor_firstdhscm_positive) = (mdr_j_integer_cofactor_firstdhsc)) /\ ff_column_mdm_cell_mdr_integer_cofactor_firstdhscm_positive_cell = ff_column_mdm_prefix_mdr_integer_cofactor_firstdhscm_positive) \/ ((exists ff_gap_mdm_le_mdr_integer_cofactor_firstdhscm_positive_cell_column_after. ff_gap_mdm_le_mdr_integer_cofactor_firstdhscm_positive_cell_column_after + (mdr_j_integer_cofactor_firstdhsc) = (ff_column_mdm_prefix_mdr_integer_cofactor_firstdhscm_positive)) /\ ff_column_mdm_cell_mdr_integer_cofactor_firstdhscm_positive_cell = S ff_column_mdm_prefix_mdr_integer_cofactor_firstdhscm_positive))) /\ (((exists ff_h_mdm_mdr_integer_cofactor_firstdhscm_positive_cell_source. ff_h_mdm_mdr_integer_cofactor_firstdhscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_integer_cofactor_firstdhscm_positive) = S ((S ((ff_row_mdm_cell_mdr_integer_cofactor_firstdhscm_positive_cell) * (S (mdr_q_integer_cofactor_firstdhs)) + (ff_column_mdm_cell_mdr_integer_cofactor_firstdhscm_positive_cell))) * mdr_pc_integer_cofactor_firstdh)) /\ exists ff_q_mdm_mdr_integer_cofactor_firstdhscm_positive_cell_source. mdr_pb_integer_cofactor_firstdh = ff_q_mdm_mdr_integer_cofactor_firstdhscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_integer_cofactor_firstdhscm_positive_cell) * (S (mdr_q_integer_cofactor_firstdhs)) + (ff_column_mdm_cell_mdr_integer_cofactor_firstdhscm_positive_cell))) * mdr_pc_integer_cofactor_firstdh) + (ff_value_mdm_prefix_mdr_integer_cofactor_firstdhscm_positive)))))) /\ (((exists ff_h_mdm_mdr_integer_cofactor_firstdhscm_positive_target. ff_h_mdm_mdr_integer_cofactor_firstdhscm_positive_target + S (ff_value_mdm_prefix_mdr_integer_cofactor_firstdhscm_positive) = S ((S (ff_index_mdm_prefix_mdr_integer_cofactor_firstdhscm_positive)) * mdr_us_integer_cofactor_firstdhsc)) /\ exists ff_q_mdm_mdr_integer_cofactor_firstdhscm_positive_target. mdr_up_integer_cofactor_firstdhsc = ff_q_mdm_mdr_integer_cofactor_firstdhscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_integer_cofactor_firstdhscm_positive)) * mdr_us_integer_cofactor_firstdhsc) + (ff_value_mdm_prefix_mdr_integer_cofactor_firstdhscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_integer_cofactor_firstdhscm_negative. (exists ff_gap_mdm_lt_mdr_integer_cofactor_firstdhscm_negative_index_bound. ff_gap_mdm_lt_mdr_integer_cofactor_firstdhscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_integer_cofactor_firstdhscm_negative) = ((mdr_q_integer_cofactor_firstdhs) * (mdr_q_integer_cofactor_firstdhs))) -> exists ff_row_mdm_prefix_mdr_integer_cofactor_firstdhscm_negative ff_column_mdm_prefix_mdr_integer_cofactor_firstdhscm_negative ff_value_mdm_prefix_mdr_integer_cofactor_firstdhscm_negative. (ff_index_mdm_prefix_mdr_integer_cofactor_firstdhscm_negative = (mdr_q_integer_cofactor_firstdhs) * ff_row_mdm_prefix_mdr_integer_cofactor_firstdhscm_negative + ff_column_mdm_prefix_mdr_integer_cofactor_firstdhscm_negative /\ ((exists ff_gap_mdm_lt_mdr_integer_cofactor_firstdhscm_negative_column_bound. ff_gap_mdm_lt_mdr_integer_cofactor_firstdhscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_integer_cofactor_firstdhscm_negative) = (mdr_q_integer_cofactor_firstdhs)) /\ ((exists ff_row_mdm_cell_mdr_integer_cofactor_firstdhscm_negative_cell ff_column_mdm_cell_mdr_integer_cofactor_firstdhscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_integer_cofactor_firstdhscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_integer_cofactor_firstdhscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_integer_cofactor_firstdhscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_integer_cofactor_firstdhscm_negative_cell = ff_row_mdm_prefix_mdr_integer_cofactor_firstdhscm_negative) \/ ((exists ff_gap_mdm_le_mdr_integer_cofactor_firstdhscm_negative_cell_row_after. ff_gap_mdm_le_mdr_integer_cofactor_firstdhscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_integer_cofactor_firstdhscm_negative)) /\ ff_row_mdm_cell_mdr_integer_cofactor_firstdhscm_negative_cell = S ff_row_mdm_prefix_mdr_integer_cofactor_firstdhscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_integer_cofactor_firstdhscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_integer_cofactor_firstdhscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_integer_cofactor_firstdhscm_negative) = (mdr_j_integer_cofactor_firstdhsc)) /\ ff_column_mdm_cell_mdr_integer_cofactor_firstdhscm_negative_cell = ff_column_mdm_prefix_mdr_integer_cofactor_firstdhscm_negative) \/ ((exists ff_gap_mdm_le_mdr_integer_cofactor_firstdhscm_negative_cell_column_after. ff_gap_mdm_le_mdr_integer_cofactor_firstdhscm_negative_cell_column_after + (mdr_j_integer_cofactor_firstdhsc) = (ff_column_mdm_prefix_mdr_integer_cofactor_firstdhscm_negative)) /\ ff_column_mdm_cell_mdr_integer_cofactor_firstdhscm_negative_cell = S ff_column_mdm_prefix_mdr_integer_cofactor_firstdhscm_negative))) /\ (((exists ff_h_mdm_mdr_integer_cofactor_firstdhscm_negative_cell_source. ff_h_mdm_mdr_integer_cofactor_firstdhscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_integer_cofactor_firstdhscm_negative) = S ((S ((ff_row_mdm_cell_mdr_integer_cofactor_firstdhscm_negative_cell) * (S (mdr_q_integer_cofactor_firstdhs)) + (ff_column_mdm_cell_mdr_integer_cofactor_firstdhscm_negative_cell))) * mdr_nc_integer_cofactor_firstdh)) /\ exists ff_q_mdm_mdr_integer_cofactor_firstdhscm_negative_cell_source. mdr_nb_integer_cofactor_firstdh = ff_q_mdm_mdr_integer_cofactor_firstdhscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_integer_cofactor_firstdhscm_negative_cell) * (S (mdr_q_integer_cofactor_firstdhs)) + (ff_column_mdm_cell_mdr_integer_cofactor_firstdhscm_negative_cell))) * mdr_nc_integer_cofactor_firstdh) + (ff_value_mdm_prefix_mdr_integer_cofactor_firstdhscm_negative)))))) /\ (((exists ff_h_mdm_mdr_integer_cofactor_firstdhscm_negative_target. ff_h_mdm_mdr_integer_cofactor_firstdhscm_negative_target + S (ff_value_mdm_prefix_mdr_integer_cofactor_firstdhscm_negative) = S ((S (ff_index_mdm_prefix_mdr_integer_cofactor_firstdhscm_negative)) * mdr_ut_integer_cofactor_firstdhsc)) /\ exists ff_q_mdm_mdr_integer_cofactor_firstdhscm_negative_target. mdr_un_integer_cofactor_firstdhsc = ff_q_mdm_mdr_integer_cofactor_firstdhscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_integer_cofactor_firstdhscm_negative)) * mdr_ut_integer_cofactor_firstdhsc) + (ff_value_mdm_prefix_mdr_integer_cofactor_firstdhscm_negative))))))))) /\ ((((exists ff_h_mdr_integer_cofactor_firstdhscp. ff_h_mdr_integer_cofactor_firstdhscp + S (mdr_p_integer_cofactor_firstdhsc) = S ((S (mdr_j_integer_cofactor_firstdhsc)) * mdr_ec_integer_cofactor_firstdhs)) /\ exists ff_q_mdr_integer_cofactor_firstdhscp. mdr_eb_integer_cofactor_firstdhs = ff_q_mdr_integer_cofactor_firstdhscp * S ((S (mdr_j_integer_cofactor_firstdhsc)) * mdr_ec_integer_cofactor_firstdhs) + (mdr_p_integer_cofactor_firstdhsc))) /\ (((exists ff_h_mdr_integer_cofactor_firstdhscn. ff_h_mdr_integer_cofactor_firstdhscn + S (mdr_n_integer_cofactor_firstdhsc) = S ((S (mdr_j_integer_cofactor_firstdhsc)) * mdr_fc_integer_cofactor_firstdhs)) /\ exists ff_q_mdr_integer_cofactor_firstdhscn. mdr_fb_integer_cofactor_firstdhs = ff_q_mdr_integer_cofactor_firstdhscn * S ((S (mdr_j_integer_cofactor_firstdhsc)) * mdr_fc_integer_cofactor_firstdhs) + (mdr_n_integer_cofactor_firstdhsc)))))))) /\ (exists ff_ub_mce_fold_mdr_integer_cofactor_firstdhsf ff_uc_mce_fold_mdr_integer_cofactor_firstdhsf ff_vb_mce_fold_mdr_integer_cofactor_firstdhsf ff_vc_mce_fold_mdr_integer_cofactor_firstdhsf. ((forall ff_index_mce_alternating_mdr_integer_cofactor_firstdhsf_prefix. (exists ff_gap_mce_mdr_integer_cofactor_firstdhsf_prefix_index. ff_gap_mce_mdr_integer_cofactor_firstdhsf_prefix_index + S (ff_index_mce_alternating_mdr_integer_cofactor_firstdhsf_prefix) = (S (mdr_q_integer_cofactor_firstdhs))) -> exists ff_ap_mce_alternating_mdr_integer_cofactor_firstdhsf_prefix ff_an_mce_alternating_mdr_integer_cofactor_firstdhsf_prefix ff_bp_mce_alternating_mdr_integer_cofactor_firstdhsf_prefix ff_bn_mce_alternating_mdr_integer_cofactor_firstdhsf_prefix ff_p_mce_alternating_mdr_integer_cofactor_firstdhsf_prefix ff_n_mce_alternating_mdr_integer_cofactor_firstdhsf_prefix. ((((exists ff_h_mce_mdr_integer_cofactor_firstdhsf_prefix_ap. ff_h_mce_mdr_integer_cofactor_firstdhsf_prefix_ap + S (ff_ap_mce_alternating_mdr_integer_cofactor_firstdhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_integer_cofactor_firstdhsf_prefix)) * mdr_pc_integer_cofactor_firstdh)) /\ exists ff_q_mce_mdr_integer_cofactor_firstdhsf_prefix_ap. mdr_pb_integer_cofactor_firstdh = ff_q_mce_mdr_integer_cofactor_firstdhsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_integer_cofactor_firstdhsf_prefix)) * mdr_pc_integer_cofactor_firstdh) + (ff_ap_mce_alternating_mdr_integer_cofactor_firstdhsf_prefix))) /\ ((((exists ff_h_mce_mdr_integer_cofactor_firstdhsf_prefix_an. ff_h_mce_mdr_integer_cofactor_firstdhsf_prefix_an + S (ff_an_mce_alternating_mdr_integer_cofactor_firstdhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_integer_cofactor_firstdhsf_prefix)) * mdr_nc_integer_cofactor_firstdh)) /\ exists ff_q_mce_mdr_integer_cofactor_firstdhsf_prefix_an. mdr_nb_integer_cofactor_firstdh = ff_q_mce_mdr_integer_cofactor_firstdhsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_integer_cofactor_firstdhsf_prefix)) * mdr_nc_integer_cofactor_firstdh) + (ff_an_mce_alternating_mdr_integer_cofactor_firstdhsf_prefix))) /\ ((((exists ff_h_mce_mdr_integer_cofactor_firstdhsf_prefix_bp. ff_h_mce_mdr_integer_cofactor_firstdhsf_prefix_bp + S (ff_bp_mce_alternating_mdr_integer_cofactor_firstdhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_integer_cofactor_firstdhsf_prefix)) * mdr_ec_integer_cofactor_firstdhs)) /\ exists ff_q_mce_mdr_integer_cofactor_firstdhsf_prefix_bp. mdr_eb_integer_cofactor_firstdhs = ff_q_mce_mdr_integer_cofactor_firstdhsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_integer_cofactor_firstdhsf_prefix)) * mdr_ec_integer_cofactor_firstdhs) + (ff_bp_mce_alternating_mdr_integer_cofactor_firstdhsf_prefix))) /\ ((((exists ff_h_mce_mdr_integer_cofactor_firstdhsf_prefix_bn. ff_h_mce_mdr_integer_cofactor_firstdhsf_prefix_bn + S (ff_bn_mce_alternating_mdr_integer_cofactor_firstdhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_integer_cofactor_firstdhsf_prefix)) * mdr_fc_integer_cofactor_firstdhs)) /\ exists ff_q_mce_mdr_integer_cofactor_firstdhsf_prefix_bn. mdr_fb_integer_cofactor_firstdhs = ff_q_mce_mdr_integer_cofactor_firstdhsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_integer_cofactor_firstdhsf_prefix)) * mdr_fc_integer_cofactor_firstdhs) + (ff_bn_mce_alternating_mdr_integer_cofactor_firstdhsf_prefix))) /\ ((((exists ff_h_mce_mdr_integer_cofactor_firstdhsf_prefix_positive. ff_h_mce_mdr_integer_cofactor_firstdhsf_prefix_positive + S (ff_p_mce_alternating_mdr_integer_cofactor_firstdhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_integer_cofactor_firstdhsf_prefix)) * ff_uc_mce_fold_mdr_integer_cofactor_firstdhsf)) /\ exists ff_q_mce_mdr_integer_cofactor_firstdhsf_prefix_positive. ff_ub_mce_fold_mdr_integer_cofactor_firstdhsf = ff_q_mce_mdr_integer_cofactor_firstdhsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_integer_cofactor_firstdhsf_prefix)) * ff_uc_mce_fold_mdr_integer_cofactor_firstdhsf) + (ff_p_mce_alternating_mdr_integer_cofactor_firstdhsf_prefix))) /\ ((((exists ff_h_mce_mdr_integer_cofactor_firstdhsf_prefix_negative. ff_h_mce_mdr_integer_cofactor_firstdhsf_prefix_negative + S (ff_n_mce_alternating_mdr_integer_cofactor_firstdhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_integer_cofactor_firstdhsf_prefix)) * ff_vc_mce_fold_mdr_integer_cofactor_firstdhsf)) /\ exists ff_q_mce_mdr_integer_cofactor_firstdhsf_prefix_negative. ff_vb_mce_fold_mdr_integer_cofactor_firstdhsf = ff_q_mce_mdr_integer_cofactor_firstdhsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_integer_cofactor_firstdhsf_prefix)) * ff_vc_mce_fold_mdr_integer_cofactor_firstdhsf) + (ff_n_mce_alternating_mdr_integer_cofactor_firstdhsf_prefix))) /\ (((exists ff_even_mce_term_mdr_integer_cofactor_firstdhsf_prefix_term. ff_index_mce_alternating_mdr_integer_cofactor_firstdhsf_prefix = 2 * ff_even_mce_term_mdr_integer_cofactor_firstdhsf_prefix_term) /\ (ff_p_mce_alternating_mdr_integer_cofactor_firstdhsf_prefix = (ff_ap_mce_alternating_mdr_integer_cofactor_firstdhsf_prefix) * (ff_bp_mce_alternating_mdr_integer_cofactor_firstdhsf_prefix) + (ff_an_mce_alternating_mdr_integer_cofactor_firstdhsf_prefix) * (ff_bn_mce_alternating_mdr_integer_cofactor_firstdhsf_prefix) /\ ff_n_mce_alternating_mdr_integer_cofactor_firstdhsf_prefix = (ff_ap_mce_alternating_mdr_integer_cofactor_firstdhsf_prefix) * (ff_bn_mce_alternating_mdr_integer_cofactor_firstdhsf_prefix) + (ff_an_mce_alternating_mdr_integer_cofactor_firstdhsf_prefix) * (ff_bp_mce_alternating_mdr_integer_cofactor_firstdhsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_integer_cofactor_firstdhsf_prefix_term. ff_index_mce_alternating_mdr_integer_cofactor_firstdhsf_prefix = 2 * ff_odd_mce_term_mdr_integer_cofactor_firstdhsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_integer_cofactor_firstdhsf_prefix = (ff_ap_mce_alternating_mdr_integer_cofactor_firstdhsf_prefix) * (ff_bn_mce_alternating_mdr_integer_cofactor_firstdhsf_prefix) + (ff_an_mce_alternating_mdr_integer_cofactor_firstdhsf_prefix) * (ff_bp_mce_alternating_mdr_integer_cofactor_firstdhsf_prefix) /\ ff_n_mce_alternating_mdr_integer_cofactor_firstdhsf_prefix = (ff_ap_mce_alternating_mdr_integer_cofactor_firstdhsf_prefix) * (ff_bp_mce_alternating_mdr_integer_cofactor_firstdhsf_prefix) + (ff_an_mce_alternating_mdr_integer_cofactor_firstdhsf_prefix) * (ff_bn_mce_alternating_mdr_integer_cofactor_firstdhsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_integer_cofactor_firstdhsf_positive ff_v_mce_mdr_integer_cofactor_firstdhsf_positive. ((((exists ff_h_mce_mdr_integer_cofactor_firstdhsf_positive_start. ff_h_mce_mdr_integer_cofactor_firstdhsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_integer_cofactor_firstdhsf_positive)) /\ exists ff_q_mce_mdr_integer_cofactor_firstdhsf_positive_start. ff_u_mce_mdr_integer_cofactor_firstdhsf_positive = ff_q_mce_mdr_integer_cofactor_firstdhsf_positive_start * S ((S (0)) * ff_v_mce_mdr_integer_cofactor_firstdhsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_integer_cofactor_firstdhsf_positive_terminal. ff_h_mce_mdr_integer_cofactor_firstdhsf_positive_terminal + S (mdr_p_integer_cofactor_firstdh) = S ((S ((S (mdr_q_integer_cofactor_firstdhs)))) * ff_v_mce_mdr_integer_cofactor_firstdhsf_positive)) /\ exists ff_q_mce_mdr_integer_cofactor_firstdhsf_positive_terminal. ff_u_mce_mdr_integer_cofactor_firstdhsf_positive = ff_q_mce_mdr_integer_cofactor_firstdhsf_positive_terminal * S ((S ((S (mdr_q_integer_cofactor_firstdhs)))) * ff_v_mce_mdr_integer_cofactor_firstdhsf_positive) + (mdr_p_integer_cofactor_firstdh))) /\ forall ff_i_mce_mdr_integer_cofactor_firstdhsf_positive. (exists ff_lt_mce_mdr_integer_cofactor_firstdhsf_positive_bound. ff_lt_mce_mdr_integer_cofactor_firstdhsf_positive_bound + S ff_i_mce_mdr_integer_cofactor_firstdhsf_positive = (S (mdr_q_integer_cofactor_firstdhs))) -> exists ff_a_mce_mdr_integer_cofactor_firstdhsf_positive ff_r_mce_mdr_integer_cofactor_firstdhsf_positive ff_s_mce_mdr_integer_cofactor_firstdhsf_positive. ((((exists ff_h_mce_mdr_integer_cofactor_firstdhsf_positive_summand. ff_h_mce_mdr_integer_cofactor_firstdhsf_positive_summand + S (ff_a_mce_mdr_integer_cofactor_firstdhsf_positive) = S ((S (ff_i_mce_mdr_integer_cofactor_firstdhsf_positive)) * ff_uc_mce_fold_mdr_integer_cofactor_firstdhsf)) /\ exists ff_q_mce_mdr_integer_cofactor_firstdhsf_positive_summand. ff_ub_mce_fold_mdr_integer_cofactor_firstdhsf = ff_q_mce_mdr_integer_cofactor_firstdhsf_positive_summand * S ((S (ff_i_mce_mdr_integer_cofactor_firstdhsf_positive)) * ff_uc_mce_fold_mdr_integer_cofactor_firstdhsf) + (ff_a_mce_mdr_integer_cofactor_firstdhsf_positive))) /\ ((((exists ff_h_mce_mdr_integer_cofactor_firstdhsf_positive_partial. ff_h_mce_mdr_integer_cofactor_firstdhsf_positive_partial + S (ff_r_mce_mdr_integer_cofactor_firstdhsf_positive) = S ((S (ff_i_mce_mdr_integer_cofactor_firstdhsf_positive)) * ff_v_mce_mdr_integer_cofactor_firstdhsf_positive)) /\ exists ff_q_mce_mdr_integer_cofactor_firstdhsf_positive_partial. ff_u_mce_mdr_integer_cofactor_firstdhsf_positive = ff_q_mce_mdr_integer_cofactor_firstdhsf_positive_partial * S ((S (ff_i_mce_mdr_integer_cofactor_firstdhsf_positive)) * ff_v_mce_mdr_integer_cofactor_firstdhsf_positive) + (ff_r_mce_mdr_integer_cofactor_firstdhsf_positive))) /\ ((((exists ff_h_mce_mdr_integer_cofactor_firstdhsf_positive_successor. ff_h_mce_mdr_integer_cofactor_firstdhsf_positive_successor + S (ff_s_mce_mdr_integer_cofactor_firstdhsf_positive) = S ((S (S ff_i_mce_mdr_integer_cofactor_firstdhsf_positive)) * ff_v_mce_mdr_integer_cofactor_firstdhsf_positive)) /\ exists ff_q_mce_mdr_integer_cofactor_firstdhsf_positive_successor. ff_u_mce_mdr_integer_cofactor_firstdhsf_positive = ff_q_mce_mdr_integer_cofactor_firstdhsf_positive_successor * S ((S (S ff_i_mce_mdr_integer_cofactor_firstdhsf_positive)) * ff_v_mce_mdr_integer_cofactor_firstdhsf_positive) + (ff_s_mce_mdr_integer_cofactor_firstdhsf_positive))) /\ ff_s_mce_mdr_integer_cofactor_firstdhsf_positive = ff_r_mce_mdr_integer_cofactor_firstdhsf_positive + ff_a_mce_mdr_integer_cofactor_firstdhsf_positive)))))) /\ (exists ff_u_mce_mdr_integer_cofactor_firstdhsf_negative ff_v_mce_mdr_integer_cofactor_firstdhsf_negative. ((((exists ff_h_mce_mdr_integer_cofactor_firstdhsf_negative_start. ff_h_mce_mdr_integer_cofactor_firstdhsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_integer_cofactor_firstdhsf_negative)) /\ exists ff_q_mce_mdr_integer_cofactor_firstdhsf_negative_start. ff_u_mce_mdr_integer_cofactor_firstdhsf_negative = ff_q_mce_mdr_integer_cofactor_firstdhsf_negative_start * S ((S (0)) * ff_v_mce_mdr_integer_cofactor_firstdhsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_integer_cofactor_firstdhsf_negative_terminal. ff_h_mce_mdr_integer_cofactor_firstdhsf_negative_terminal + S (mdr_n_integer_cofactor_firstdh) = S ((S ((S (mdr_q_integer_cofactor_firstdhs)))) * ff_v_mce_mdr_integer_cofactor_firstdhsf_negative)) /\ exists ff_q_mce_mdr_integer_cofactor_firstdhsf_negative_terminal. ff_u_mce_mdr_integer_cofactor_firstdhsf_negative = ff_q_mce_mdr_integer_cofactor_firstdhsf_negative_terminal * S ((S ((S (mdr_q_integer_cofactor_firstdhs)))) * ff_v_mce_mdr_integer_cofactor_firstdhsf_negative) + (mdr_n_integer_cofactor_firstdh))) /\ forall ff_i_mce_mdr_integer_cofactor_firstdhsf_negative. (exists ff_lt_mce_mdr_integer_cofactor_firstdhsf_negative_bound. ff_lt_mce_mdr_integer_cofactor_firstdhsf_negative_bound + S ff_i_mce_mdr_integer_cofactor_firstdhsf_negative = (S (mdr_q_integer_cofactor_firstdhs))) -> exists ff_a_mce_mdr_integer_cofactor_firstdhsf_negative ff_r_mce_mdr_integer_cofactor_firstdhsf_negative ff_s_mce_mdr_integer_cofactor_firstdhsf_negative. ((((exists ff_h_mce_mdr_integer_cofactor_firstdhsf_negative_summand. ff_h_mce_mdr_integer_cofactor_firstdhsf_negative_summand + S (ff_a_mce_mdr_integer_cofactor_firstdhsf_negative) = S ((S (ff_i_mce_mdr_integer_cofactor_firstdhsf_negative)) * ff_vc_mce_fold_mdr_integer_cofactor_firstdhsf)) /\ exists ff_q_mce_mdr_integer_cofactor_firstdhsf_negative_summand. ff_vb_mce_fold_mdr_integer_cofactor_firstdhsf = ff_q_mce_mdr_integer_cofactor_firstdhsf_negative_summand * S ((S (ff_i_mce_mdr_integer_cofactor_firstdhsf_negative)) * ff_vc_mce_fold_mdr_integer_cofactor_firstdhsf) + (ff_a_mce_mdr_integer_cofactor_firstdhsf_negative))) /\ ((((exists ff_h_mce_mdr_integer_cofactor_firstdhsf_negative_partial. ff_h_mce_mdr_integer_cofactor_firstdhsf_negative_partial + S (ff_r_mce_mdr_integer_cofactor_firstdhsf_negative) = S ((S (ff_i_mce_mdr_integer_cofactor_firstdhsf_negative)) * ff_v_mce_mdr_integer_cofactor_firstdhsf_negative)) /\ exists ff_q_mce_mdr_integer_cofactor_firstdhsf_negative_partial. ff_u_mce_mdr_integer_cofactor_firstdhsf_negative = ff_q_mce_mdr_integer_cofactor_firstdhsf_negative_partial * S ((S (ff_i_mce_mdr_integer_cofactor_firstdhsf_negative)) * ff_v_mce_mdr_integer_cofactor_firstdhsf_negative) + (ff_r_mce_mdr_integer_cofactor_firstdhsf_negative))) /\ ((((exists ff_h_mce_mdr_integer_cofactor_firstdhsf_negative_successor. ff_h_mce_mdr_integer_cofactor_firstdhsf_negative_successor + S (ff_s_mce_mdr_integer_cofactor_firstdhsf_negative) = S ((S (S ff_i_mce_mdr_integer_cofactor_firstdhsf_negative)) * ff_v_mce_mdr_integer_cofactor_firstdhsf_negative)) /\ exists ff_q_mce_mdr_integer_cofactor_firstdhsf_negative_successor. ff_u_mce_mdr_integer_cofactor_firstdhsf_negative = ff_q_mce_mdr_integer_cofactor_firstdhsf_negative_successor * S ((S (S ff_i_mce_mdr_integer_cofactor_firstdhsf_negative)) * ff_v_mce_mdr_integer_cofactor_firstdhsf_negative) + (ff_s_mce_mdr_integer_cofactor_firstdhsf_negative))) /\ ff_s_mce_mdr_integer_cofactor_firstdhsf_negative = ff_r_mce_mdr_integer_cofactor_firstdhsf_negative + ff_a_mce_mdr_integer_cofactor_firstdhsf_negative))))))))))))))) /\ ((exists mdr_gap_integer_cofactor_firstdi. mdr_gap_integer_cofactor_firstdi + S (mdr_i_integer_cofactor_firstd) = (mdr_l_integer_cofactor_firstd)) /\ (exists mdr_z_integer_cofactor_firstdr. ((exists mdr_a_integer_cofactor_firstdrc mdr_b_integer_cofactor_firstdrc mdr_c_integer_cofactor_firstdrc mdr_e_integer_cofactor_firstdrc mdr_f_integer_cofactor_firstdrc. ((mdr_a_integer_cofactor_firstdrc = ((q) + (mdr_up_integer_cofactor_first)) * S ((q) + (mdr_up_integer_cofactor_first)) + ((mdr_up_integer_cofactor_first) + (mdr_up_integer_cofactor_first))) /\ ((mdr_b_integer_cofactor_firstdrc = ((mdr_us_integer_cofactor_first) + (mdr_un_integer_cofactor_first)) * S ((mdr_us_integer_cofactor_first) + (mdr_un_integer_cofactor_first)) + ((mdr_un_integer_cofactor_first) + (mdr_un_integer_cofactor_first))) /\ ((mdr_c_integer_cofactor_firstdrc = ((mdr_a_integer_cofactor_firstdrc) + (mdr_b_integer_cofactor_firstdrc)) * S ((mdr_a_integer_cofactor_firstdrc) + (mdr_b_integer_cofactor_firstdrc)) + ((mdr_b_integer_cofactor_firstdrc) + (mdr_b_integer_cofactor_firstdrc))) /\ ((mdr_e_integer_cofactor_firstdrc = ((mdr_p_integer_cofactor_first) + (mdr_n_integer_cofactor_first)) * S ((mdr_p_integer_cofactor_first) + (mdr_n_integer_cofactor_first)) + ((mdr_n_integer_cofactor_first) + (mdr_n_integer_cofactor_first))) /\ ((mdr_f_integer_cofactor_firstdrc = ((mdr_ut_integer_cofactor_first) + (mdr_e_integer_cofactor_firstdrc)) * S ((mdr_ut_integer_cofactor_first) + (mdr_e_integer_cofactor_firstdrc)) + ((mdr_e_integer_cofactor_firstdrc) + (mdr_e_integer_cofactor_firstdrc))) /\ ((mdr_z_integer_cofactor_firstdr) = ((mdr_c_integer_cofactor_firstdrc) + (mdr_f_integer_cofactor_firstdrc)) * S ((mdr_c_integer_cofactor_firstdrc) + (mdr_f_integer_cofactor_firstdrc)) + ((mdr_f_integer_cofactor_firstdrc) + (mdr_f_integer_cofactor_firstdrc))))))))) /\ (((exists ff_h_mdr_integer_cofactor_firstdrb. ff_h_mdr_integer_cofactor_firstdrb + S (mdr_z_integer_cofactor_firstdr) = S ((S (mdr_i_integer_cofactor_firstd)) * mdr_c_integer_cofactor_firstd)) /\ exists ff_q_mdr_integer_cofactor_firstdrb. mdr_b_integer_cofactor_firstd = ff_q_mdr_integer_cofactor_firstdrb * S ((S (mdr_i_integer_cofactor_firstd)) * mdr_c_integer_cofactor_firstd) + (mdr_z_integer_cofactor_firstdr)))))))) /\ ((((exists ff_h_mdr_integer_cofactor_firstp. ff_h_mdr_integer_cofactor_firstp + S (mdr_p_integer_cofactor_first) = S ((S (mdr_j_integer_cofactor_first)) * cc)) /\ exists ff_q_mdr_integer_cofactor_firstp. cb = ff_q_mdr_integer_cofactor_firstp * S ((S (mdr_j_integer_cofactor_first)) * cc) + (mdr_p_integer_cofactor_first))) /\ (((exists ff_h_mdr_integer_cofactor_firstn. ff_h_mdr_integer_cofactor_firstn + S (mdr_n_integer_cofactor_first) = S ((S (mdr_j_integer_cofactor_first)) * dc)) /\ exists ff_q_mdr_integer_cofactor_firstn. db = ff_q_mdr_integer_cofactor_firstn * S ((S (mdr_j_integer_cofactor_first)) * dc) + (mdr_n_integer_cofactor_first))))))) -> (forall mdr_j_integer_cofactor_second. (exists mdr_gap_integer_cofactor_secondj. mdr_gap_integer_cofactor_secondj + S (mdr_j_integer_cofactor_second) = (S (q))) -> exists mdr_up_integer_cofactor_second mdr_us_integer_cofactor_second mdr_un_integer_cofactor_second mdr_ut_integer_cofactor_second mdr_p_integer_cofactor_second mdr_n_integer_cofactor_second. ((((forall ff_index_mdm_prefix_mdr_integer_cofactor_secondm_positive. (exists ff_gap_mdm_lt_mdr_integer_cofactor_secondm_positive_index_bound. ff_gap_mdm_lt_mdr_integer_cofactor_secondm_positive_index_bound + S (ff_index_mdm_prefix_mdr_integer_cofactor_secondm_positive) = ((q) * (q))) -> exists ff_row_mdm_prefix_mdr_integer_cofactor_secondm_positive ff_column_mdm_prefix_mdr_integer_cofactor_secondm_positive ff_value_mdm_prefix_mdr_integer_cofactor_secondm_positive. (ff_index_mdm_prefix_mdr_integer_cofactor_secondm_positive = (q) * ff_row_mdm_prefix_mdr_integer_cofactor_secondm_positive + ff_column_mdm_prefix_mdr_integer_cofactor_secondm_positive /\ ((exists ff_gap_mdm_lt_mdr_integer_cofactor_secondm_positive_column_bound. ff_gap_mdm_lt_mdr_integer_cofactor_secondm_positive_column_bound + S (ff_column_mdm_prefix_mdr_integer_cofactor_secondm_positive) = (q)) /\ ((exists ff_row_mdm_cell_mdr_integer_cofactor_secondm_positive_cell ff_column_mdm_cell_mdr_integer_cofactor_secondm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_integer_cofactor_secondm_positive_cell_row_before. ff_gap_mdm_lt_mdr_integer_cofactor_secondm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_integer_cofactor_secondm_positive) = (0)) /\ ff_row_mdm_cell_mdr_integer_cofactor_secondm_positive_cell = ff_row_mdm_prefix_mdr_integer_cofactor_secondm_positive) \/ ((exists ff_gap_mdm_le_mdr_integer_cofactor_secondm_positive_cell_row_after. ff_gap_mdm_le_mdr_integer_cofactor_secondm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_integer_cofactor_secondm_positive)) /\ ff_row_mdm_cell_mdr_integer_cofactor_secondm_positive_cell = S ff_row_mdm_prefix_mdr_integer_cofactor_secondm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_integer_cofactor_secondm_positive_cell_column_before. ff_gap_mdm_lt_mdr_integer_cofactor_secondm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_integer_cofactor_secondm_positive) = (mdr_j_integer_cofactor_second)) /\ ff_column_mdm_cell_mdr_integer_cofactor_secondm_positive_cell = ff_column_mdm_prefix_mdr_integer_cofactor_secondm_positive) \/ ((exists ff_gap_mdm_le_mdr_integer_cofactor_secondm_positive_cell_column_after. ff_gap_mdm_le_mdr_integer_cofactor_secondm_positive_cell_column_after + (mdr_j_integer_cofactor_second) = (ff_column_mdm_prefix_mdr_integer_cofactor_secondm_positive)) /\ ff_column_mdm_cell_mdr_integer_cofactor_secondm_positive_cell = S ff_column_mdm_prefix_mdr_integer_cofactor_secondm_positive))) /\ (((exists ff_h_mdm_mdr_integer_cofactor_secondm_positive_cell_source. ff_h_mdm_mdr_integer_cofactor_secondm_positive_cell_source + S (ff_value_mdm_prefix_mdr_integer_cofactor_secondm_positive) = S ((S ((ff_row_mdm_cell_mdr_integer_cofactor_secondm_positive_cell) * (S (q)) + (ff_column_mdm_cell_mdr_integer_cofactor_secondm_positive_cell))) * ec)) /\ exists ff_q_mdm_mdr_integer_cofactor_secondm_positive_cell_source. eb = ff_q_mdm_mdr_integer_cofactor_secondm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_integer_cofactor_secondm_positive_cell) * (S (q)) + (ff_column_mdm_cell_mdr_integer_cofactor_secondm_positive_cell))) * ec) + (ff_value_mdm_prefix_mdr_integer_cofactor_secondm_positive)))))) /\ (((exists ff_h_mdm_mdr_integer_cofactor_secondm_positive_target. ff_h_mdm_mdr_integer_cofactor_secondm_positive_target + S (ff_value_mdm_prefix_mdr_integer_cofactor_secondm_positive) = S ((S (ff_index_mdm_prefix_mdr_integer_cofactor_secondm_positive)) * mdr_us_integer_cofactor_second)) /\ exists ff_q_mdm_mdr_integer_cofactor_secondm_positive_target. mdr_up_integer_cofactor_second = ff_q_mdm_mdr_integer_cofactor_secondm_positive_target * S ((S (ff_index_mdm_prefix_mdr_integer_cofactor_secondm_positive)) * mdr_us_integer_cofactor_second) + (ff_value_mdm_prefix_mdr_integer_cofactor_secondm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_integer_cofactor_secondm_negative. (exists ff_gap_mdm_lt_mdr_integer_cofactor_secondm_negative_index_bound. ff_gap_mdm_lt_mdr_integer_cofactor_secondm_negative_index_bound + S (ff_index_mdm_prefix_mdr_integer_cofactor_secondm_negative) = ((q) * (q))) -> exists ff_row_mdm_prefix_mdr_integer_cofactor_secondm_negative ff_column_mdm_prefix_mdr_integer_cofactor_secondm_negative ff_value_mdm_prefix_mdr_integer_cofactor_secondm_negative. (ff_index_mdm_prefix_mdr_integer_cofactor_secondm_negative = (q) * ff_row_mdm_prefix_mdr_integer_cofactor_secondm_negative + ff_column_mdm_prefix_mdr_integer_cofactor_secondm_negative /\ ((exists ff_gap_mdm_lt_mdr_integer_cofactor_secondm_negative_column_bound. ff_gap_mdm_lt_mdr_integer_cofactor_secondm_negative_column_bound + S (ff_column_mdm_prefix_mdr_integer_cofactor_secondm_negative) = (q)) /\ ((exists ff_row_mdm_cell_mdr_integer_cofactor_secondm_negative_cell ff_column_mdm_cell_mdr_integer_cofactor_secondm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_integer_cofactor_secondm_negative_cell_row_before. ff_gap_mdm_lt_mdr_integer_cofactor_secondm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_integer_cofactor_secondm_negative) = (0)) /\ ff_row_mdm_cell_mdr_integer_cofactor_secondm_negative_cell = ff_row_mdm_prefix_mdr_integer_cofactor_secondm_negative) \/ ((exists ff_gap_mdm_le_mdr_integer_cofactor_secondm_negative_cell_row_after. ff_gap_mdm_le_mdr_integer_cofactor_secondm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_integer_cofactor_secondm_negative)) /\ ff_row_mdm_cell_mdr_integer_cofactor_secondm_negative_cell = S ff_row_mdm_prefix_mdr_integer_cofactor_secondm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_integer_cofactor_secondm_negative_cell_column_before. ff_gap_mdm_lt_mdr_integer_cofactor_secondm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_integer_cofactor_secondm_negative) = (mdr_j_integer_cofactor_second)) /\ ff_column_mdm_cell_mdr_integer_cofactor_secondm_negative_cell = ff_column_mdm_prefix_mdr_integer_cofactor_secondm_negative) \/ ((exists ff_gap_mdm_le_mdr_integer_cofactor_secondm_negative_cell_column_after. ff_gap_mdm_le_mdr_integer_cofactor_secondm_negative_cell_column_after + (mdr_j_integer_cofactor_second) = (ff_column_mdm_prefix_mdr_integer_cofactor_secondm_negative)) /\ ff_column_mdm_cell_mdr_integer_cofactor_secondm_negative_cell = S ff_column_mdm_prefix_mdr_integer_cofactor_secondm_negative))) /\ (((exists ff_h_mdm_mdr_integer_cofactor_secondm_negative_cell_source. ff_h_mdm_mdr_integer_cofactor_secondm_negative_cell_source + S (ff_value_mdm_prefix_mdr_integer_cofactor_secondm_negative) = S ((S ((ff_row_mdm_cell_mdr_integer_cofactor_secondm_negative_cell) * (S (q)) + (ff_column_mdm_cell_mdr_integer_cofactor_secondm_negative_cell))) * fc)) /\ exists ff_q_mdm_mdr_integer_cofactor_secondm_negative_cell_source. fb = ff_q_mdm_mdr_integer_cofactor_secondm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_integer_cofactor_secondm_negative_cell) * (S (q)) + (ff_column_mdm_cell_mdr_integer_cofactor_secondm_negative_cell))) * fc) + (ff_value_mdm_prefix_mdr_integer_cofactor_secondm_negative)))))) /\ (((exists ff_h_mdm_mdr_integer_cofactor_secondm_negative_target. ff_h_mdm_mdr_integer_cofactor_secondm_negative_target + S (ff_value_mdm_prefix_mdr_integer_cofactor_secondm_negative) = S ((S (ff_index_mdm_prefix_mdr_integer_cofactor_secondm_negative)) * mdr_ut_integer_cofactor_second)) /\ exists ff_q_mdm_mdr_integer_cofactor_secondm_negative_target. mdr_un_integer_cofactor_second = ff_q_mdm_mdr_integer_cofactor_secondm_negative_target * S ((S (ff_index_mdm_prefix_mdr_integer_cofactor_secondm_negative)) * mdr_ut_integer_cofactor_second) + (ff_value_mdm_prefix_mdr_integer_cofactor_secondm_negative))))))))) /\ ((exists mdr_b_integer_cofactor_secondd mdr_c_integer_cofactor_secondd mdr_l_integer_cofactor_secondd mdr_i_integer_cofactor_secondd. ((forall mdr_i_integer_cofactor_seconddh. (exists mdr_gap_integer_cofactor_seconddhi. mdr_gap_integer_cofactor_seconddhi + S (mdr_i_integer_cofactor_seconddh) = (mdr_l_integer_cofactor_secondd)) -> exists mdr_d_integer_cofactor_seconddh mdr_pb_integer_cofactor_seconddh mdr_pc_integer_cofactor_seconddh mdr_nb_integer_cofactor_seconddh mdr_nc_integer_cofactor_seconddh mdr_p_integer_cofactor_seconddh mdr_n_integer_cofactor_seconddh. ((exists mdr_z_integer_cofactor_seconddhr. ((exists mdr_a_integer_cofactor_seconddhrc mdr_b_integer_cofactor_seconddhrc mdr_c_integer_cofactor_seconddhrc mdr_e_integer_cofactor_seconddhrc mdr_f_integer_cofactor_seconddhrc. ((mdr_a_integer_cofactor_seconddhrc = ((mdr_d_integer_cofactor_seconddh) + (mdr_pb_integer_cofactor_seconddh)) * S ((mdr_d_integer_cofactor_seconddh) + (mdr_pb_integer_cofactor_seconddh)) + ((mdr_pb_integer_cofactor_seconddh) + (mdr_pb_integer_cofactor_seconddh))) /\ ((mdr_b_integer_cofactor_seconddhrc = ((mdr_pc_integer_cofactor_seconddh) + (mdr_nb_integer_cofactor_seconddh)) * S ((mdr_pc_integer_cofactor_seconddh) + (mdr_nb_integer_cofactor_seconddh)) + ((mdr_nb_integer_cofactor_seconddh) + (mdr_nb_integer_cofactor_seconddh))) /\ ((mdr_c_integer_cofactor_seconddhrc = ((mdr_a_integer_cofactor_seconddhrc) + (mdr_b_integer_cofactor_seconddhrc)) * S ((mdr_a_integer_cofactor_seconddhrc) + (mdr_b_integer_cofactor_seconddhrc)) + ((mdr_b_integer_cofactor_seconddhrc) + (mdr_b_integer_cofactor_seconddhrc))) /\ ((mdr_e_integer_cofactor_seconddhrc = ((mdr_p_integer_cofactor_seconddh) + (mdr_n_integer_cofactor_seconddh)) * S ((mdr_p_integer_cofactor_seconddh) + (mdr_n_integer_cofactor_seconddh)) + ((mdr_n_integer_cofactor_seconddh) + (mdr_n_integer_cofactor_seconddh))) /\ ((mdr_f_integer_cofactor_seconddhrc = ((mdr_nc_integer_cofactor_seconddh) + (mdr_e_integer_cofactor_seconddhrc)) * S ((mdr_nc_integer_cofactor_seconddh) + (mdr_e_integer_cofactor_seconddhrc)) + ((mdr_e_integer_cofactor_seconddhrc) + (mdr_e_integer_cofactor_seconddhrc))) /\ ((mdr_z_integer_cofactor_seconddhr) = ((mdr_c_integer_cofactor_seconddhrc) + (mdr_f_integer_cofactor_seconddhrc)) * S ((mdr_c_integer_cofactor_seconddhrc) + (mdr_f_integer_cofactor_seconddhrc)) + ((mdr_f_integer_cofactor_seconddhrc) + (mdr_f_integer_cofactor_seconddhrc))))))))) /\ (((exists ff_h_mdr_integer_cofactor_seconddhrb. ff_h_mdr_integer_cofactor_seconddhrb + S (mdr_z_integer_cofactor_seconddhr) = S ((S (mdr_i_integer_cofactor_seconddh)) * mdr_c_integer_cofactor_secondd)) /\ exists ff_q_mdr_integer_cofactor_seconddhrb. mdr_b_integer_cofactor_secondd = ff_q_mdr_integer_cofactor_seconddhrb * S ((S (mdr_i_integer_cofactor_seconddh)) * mdr_c_integer_cofactor_secondd) + (mdr_z_integer_cofactor_seconddhr))))) /\ (((((mdr_d_integer_cofactor_seconddh) = 0) /\ (((mdr_p_integer_cofactor_seconddh) = 1) /\ ((mdr_n_integer_cofactor_seconddh) = 0))) \/ exists mdr_q_integer_cofactor_seconddhs mdr_eb_integer_cofactor_seconddhs mdr_ec_integer_cofactor_seconddhs mdr_fb_integer_cofactor_seconddhs mdr_fc_integer_cofactor_seconddhs. (((mdr_d_integer_cofactor_seconddh) = S (mdr_q_integer_cofactor_seconddhs)) /\ ((forall mdr_j_integer_cofactor_seconddhsc. (exists mdr_gap_integer_cofactor_seconddhscj. mdr_gap_integer_cofactor_seconddhscj + S (mdr_j_integer_cofactor_seconddhsc) = (S (mdr_q_integer_cofactor_seconddhs))) -> exists mdr_i_integer_cofactor_seconddhsc mdr_up_integer_cofactor_seconddhsc mdr_us_integer_cofactor_seconddhsc mdr_un_integer_cofactor_seconddhsc mdr_ut_integer_cofactor_seconddhsc mdr_p_integer_cofactor_seconddhsc mdr_n_integer_cofactor_seconddhsc. ((exists mdr_gap_integer_cofactor_seconddhsci. mdr_gap_integer_cofactor_seconddhsci + S (mdr_i_integer_cofactor_seconddhsc) = (mdr_i_integer_cofactor_seconddh)) /\ ((exists mdr_z_integer_cofactor_seconddhscr. ((exists mdr_a_integer_cofactor_seconddhscrc mdr_b_integer_cofactor_seconddhscrc mdr_c_integer_cofactor_seconddhscrc mdr_e_integer_cofactor_seconddhscrc mdr_f_integer_cofactor_seconddhscrc. ((mdr_a_integer_cofactor_seconddhscrc = ((mdr_q_integer_cofactor_seconddhs) + (mdr_up_integer_cofactor_seconddhsc)) * S ((mdr_q_integer_cofactor_seconddhs) + (mdr_up_integer_cofactor_seconddhsc)) + ((mdr_up_integer_cofactor_seconddhsc) + (mdr_up_integer_cofactor_seconddhsc))) /\ ((mdr_b_integer_cofactor_seconddhscrc = ((mdr_us_integer_cofactor_seconddhsc) + (mdr_un_integer_cofactor_seconddhsc)) * S ((mdr_us_integer_cofactor_seconddhsc) + (mdr_un_integer_cofactor_seconddhsc)) + ((mdr_un_integer_cofactor_seconddhsc) + (mdr_un_integer_cofactor_seconddhsc))) /\ ((mdr_c_integer_cofactor_seconddhscrc = ((mdr_a_integer_cofactor_seconddhscrc) + (mdr_b_integer_cofactor_seconddhscrc)) * S ((mdr_a_integer_cofactor_seconddhscrc) + (mdr_b_integer_cofactor_seconddhscrc)) + ((mdr_b_integer_cofactor_seconddhscrc) + (mdr_b_integer_cofactor_seconddhscrc))) /\ ((mdr_e_integer_cofactor_seconddhscrc = ((mdr_p_integer_cofactor_seconddhsc) + (mdr_n_integer_cofactor_seconddhsc)) * S ((mdr_p_integer_cofactor_seconddhsc) + (mdr_n_integer_cofactor_seconddhsc)) + ((mdr_n_integer_cofactor_seconddhsc) + (mdr_n_integer_cofactor_seconddhsc))) /\ ((mdr_f_integer_cofactor_seconddhscrc = ((mdr_ut_integer_cofactor_seconddhsc) + (mdr_e_integer_cofactor_seconddhscrc)) * S ((mdr_ut_integer_cofactor_seconddhsc) + (mdr_e_integer_cofactor_seconddhscrc)) + ((mdr_e_integer_cofactor_seconddhscrc) + (mdr_e_integer_cofactor_seconddhscrc))) /\ ((mdr_z_integer_cofactor_seconddhscr) = ((mdr_c_integer_cofactor_seconddhscrc) + (mdr_f_integer_cofactor_seconddhscrc)) * S ((mdr_c_integer_cofactor_seconddhscrc) + (mdr_f_integer_cofactor_seconddhscrc)) + ((mdr_f_integer_cofactor_seconddhscrc) + (mdr_f_integer_cofactor_seconddhscrc))))))))) /\ (((exists ff_h_mdr_integer_cofactor_seconddhscrb. ff_h_mdr_integer_cofactor_seconddhscrb + S (mdr_z_integer_cofactor_seconddhscr) = S ((S (mdr_i_integer_cofactor_seconddhsc)) * mdr_c_integer_cofactor_secondd)) /\ exists ff_q_mdr_integer_cofactor_seconddhscrb. mdr_b_integer_cofactor_secondd = ff_q_mdr_integer_cofactor_seconddhscrb * S ((S (mdr_i_integer_cofactor_seconddhsc)) * mdr_c_integer_cofactor_secondd) + (mdr_z_integer_cofactor_seconddhscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_integer_cofactor_seconddhscm_positive. (exists ff_gap_mdm_lt_mdr_integer_cofactor_seconddhscm_positive_index_bound. ff_gap_mdm_lt_mdr_integer_cofactor_seconddhscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_integer_cofactor_seconddhscm_positive) = ((mdr_q_integer_cofactor_seconddhs) * (mdr_q_integer_cofactor_seconddhs))) -> exists ff_row_mdm_prefix_mdr_integer_cofactor_seconddhscm_positive ff_column_mdm_prefix_mdr_integer_cofactor_seconddhscm_positive ff_value_mdm_prefix_mdr_integer_cofactor_seconddhscm_positive. (ff_index_mdm_prefix_mdr_integer_cofactor_seconddhscm_positive = (mdr_q_integer_cofactor_seconddhs) * ff_row_mdm_prefix_mdr_integer_cofactor_seconddhscm_positive + ff_column_mdm_prefix_mdr_integer_cofactor_seconddhscm_positive /\ ((exists ff_gap_mdm_lt_mdr_integer_cofactor_seconddhscm_positive_column_bound. ff_gap_mdm_lt_mdr_integer_cofactor_seconddhscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_integer_cofactor_seconddhscm_positive) = (mdr_q_integer_cofactor_seconddhs)) /\ ((exists ff_row_mdm_cell_mdr_integer_cofactor_seconddhscm_positive_cell ff_column_mdm_cell_mdr_integer_cofactor_seconddhscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_integer_cofactor_seconddhscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_integer_cofactor_seconddhscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_integer_cofactor_seconddhscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_integer_cofactor_seconddhscm_positive_cell = ff_row_mdm_prefix_mdr_integer_cofactor_seconddhscm_positive) \/ ((exists ff_gap_mdm_le_mdr_integer_cofactor_seconddhscm_positive_cell_row_after. ff_gap_mdm_le_mdr_integer_cofactor_seconddhscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_integer_cofactor_seconddhscm_positive)) /\ ff_row_mdm_cell_mdr_integer_cofactor_seconddhscm_positive_cell = S ff_row_mdm_prefix_mdr_integer_cofactor_seconddhscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_integer_cofactor_seconddhscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_integer_cofactor_seconddhscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_integer_cofactor_seconddhscm_positive) = (mdr_j_integer_cofactor_seconddhsc)) /\ ff_column_mdm_cell_mdr_integer_cofactor_seconddhscm_positive_cell = ff_column_mdm_prefix_mdr_integer_cofactor_seconddhscm_positive) \/ ((exists ff_gap_mdm_le_mdr_integer_cofactor_seconddhscm_positive_cell_column_after. ff_gap_mdm_le_mdr_integer_cofactor_seconddhscm_positive_cell_column_after + (mdr_j_integer_cofactor_seconddhsc) = (ff_column_mdm_prefix_mdr_integer_cofactor_seconddhscm_positive)) /\ ff_column_mdm_cell_mdr_integer_cofactor_seconddhscm_positive_cell = S ff_column_mdm_prefix_mdr_integer_cofactor_seconddhscm_positive))) /\ (((exists ff_h_mdm_mdr_integer_cofactor_seconddhscm_positive_cell_source. ff_h_mdm_mdr_integer_cofactor_seconddhscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_integer_cofactor_seconddhscm_positive) = S ((S ((ff_row_mdm_cell_mdr_integer_cofactor_seconddhscm_positive_cell) * (S (mdr_q_integer_cofactor_seconddhs)) + (ff_column_mdm_cell_mdr_integer_cofactor_seconddhscm_positive_cell))) * mdr_pc_integer_cofactor_seconddh)) /\ exists ff_q_mdm_mdr_integer_cofactor_seconddhscm_positive_cell_source. mdr_pb_integer_cofactor_seconddh = ff_q_mdm_mdr_integer_cofactor_seconddhscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_integer_cofactor_seconddhscm_positive_cell) * (S (mdr_q_integer_cofactor_seconddhs)) + (ff_column_mdm_cell_mdr_integer_cofactor_seconddhscm_positive_cell))) * mdr_pc_integer_cofactor_seconddh) + (ff_value_mdm_prefix_mdr_integer_cofactor_seconddhscm_positive)))))) /\ (((exists ff_h_mdm_mdr_integer_cofactor_seconddhscm_positive_target. ff_h_mdm_mdr_integer_cofactor_seconddhscm_positive_target + S (ff_value_mdm_prefix_mdr_integer_cofactor_seconddhscm_positive) = S ((S (ff_index_mdm_prefix_mdr_integer_cofactor_seconddhscm_positive)) * mdr_us_integer_cofactor_seconddhsc)) /\ exists ff_q_mdm_mdr_integer_cofactor_seconddhscm_positive_target. mdr_up_integer_cofactor_seconddhsc = ff_q_mdm_mdr_integer_cofactor_seconddhscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_integer_cofactor_seconddhscm_positive)) * mdr_us_integer_cofactor_seconddhsc) + (ff_value_mdm_prefix_mdr_integer_cofactor_seconddhscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_integer_cofactor_seconddhscm_negative. (exists ff_gap_mdm_lt_mdr_integer_cofactor_seconddhscm_negative_index_bound. ff_gap_mdm_lt_mdr_integer_cofactor_seconddhscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_integer_cofactor_seconddhscm_negative) = ((mdr_q_integer_cofactor_seconddhs) * (mdr_q_integer_cofactor_seconddhs))) -> exists ff_row_mdm_prefix_mdr_integer_cofactor_seconddhscm_negative ff_column_mdm_prefix_mdr_integer_cofactor_seconddhscm_negative ff_value_mdm_prefix_mdr_integer_cofactor_seconddhscm_negative. (ff_index_mdm_prefix_mdr_integer_cofactor_seconddhscm_negative = (mdr_q_integer_cofactor_seconddhs) * ff_row_mdm_prefix_mdr_integer_cofactor_seconddhscm_negative + ff_column_mdm_prefix_mdr_integer_cofactor_seconddhscm_negative /\ ((exists ff_gap_mdm_lt_mdr_integer_cofactor_seconddhscm_negative_column_bound. ff_gap_mdm_lt_mdr_integer_cofactor_seconddhscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_integer_cofactor_seconddhscm_negative) = (mdr_q_integer_cofactor_seconddhs)) /\ ((exists ff_row_mdm_cell_mdr_integer_cofactor_seconddhscm_negative_cell ff_column_mdm_cell_mdr_integer_cofactor_seconddhscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_integer_cofactor_seconddhscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_integer_cofactor_seconddhscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_integer_cofactor_seconddhscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_integer_cofactor_seconddhscm_negative_cell = ff_row_mdm_prefix_mdr_integer_cofactor_seconddhscm_negative) \/ ((exists ff_gap_mdm_le_mdr_integer_cofactor_seconddhscm_negative_cell_row_after. ff_gap_mdm_le_mdr_integer_cofactor_seconddhscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_integer_cofactor_seconddhscm_negative)) /\ ff_row_mdm_cell_mdr_integer_cofactor_seconddhscm_negative_cell = S ff_row_mdm_prefix_mdr_integer_cofactor_seconddhscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_integer_cofactor_seconddhscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_integer_cofactor_seconddhscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_integer_cofactor_seconddhscm_negative) = (mdr_j_integer_cofactor_seconddhsc)) /\ ff_column_mdm_cell_mdr_integer_cofactor_seconddhscm_negative_cell = ff_column_mdm_prefix_mdr_integer_cofactor_seconddhscm_negative) \/ ((exists ff_gap_mdm_le_mdr_integer_cofactor_seconddhscm_negative_cell_column_after. ff_gap_mdm_le_mdr_integer_cofactor_seconddhscm_negative_cell_column_after + (mdr_j_integer_cofactor_seconddhsc) = (ff_column_mdm_prefix_mdr_integer_cofactor_seconddhscm_negative)) /\ ff_column_mdm_cell_mdr_integer_cofactor_seconddhscm_negative_cell = S ff_column_mdm_prefix_mdr_integer_cofactor_seconddhscm_negative))) /\ (((exists ff_h_mdm_mdr_integer_cofactor_seconddhscm_negative_cell_source. ff_h_mdm_mdr_integer_cofactor_seconddhscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_integer_cofactor_seconddhscm_negative) = S ((S ((ff_row_mdm_cell_mdr_integer_cofactor_seconddhscm_negative_cell) * (S (mdr_q_integer_cofactor_seconddhs)) + (ff_column_mdm_cell_mdr_integer_cofactor_seconddhscm_negative_cell))) * mdr_nc_integer_cofactor_seconddh)) /\ exists ff_q_mdm_mdr_integer_cofactor_seconddhscm_negative_cell_source. mdr_nb_integer_cofactor_seconddh = ff_q_mdm_mdr_integer_cofactor_seconddhscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_integer_cofactor_seconddhscm_negative_cell) * (S (mdr_q_integer_cofactor_seconddhs)) + (ff_column_mdm_cell_mdr_integer_cofactor_seconddhscm_negative_cell))) * mdr_nc_integer_cofactor_seconddh) + (ff_value_mdm_prefix_mdr_integer_cofactor_seconddhscm_negative)))))) /\ (((exists ff_h_mdm_mdr_integer_cofactor_seconddhscm_negative_target. ff_h_mdm_mdr_integer_cofactor_seconddhscm_negative_target + S (ff_value_mdm_prefix_mdr_integer_cofactor_seconddhscm_negative) = S ((S (ff_index_mdm_prefix_mdr_integer_cofactor_seconddhscm_negative)) * mdr_ut_integer_cofactor_seconddhsc)) /\ exists ff_q_mdm_mdr_integer_cofactor_seconddhscm_negative_target. mdr_un_integer_cofactor_seconddhsc = ff_q_mdm_mdr_integer_cofactor_seconddhscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_integer_cofactor_seconddhscm_negative)) * mdr_ut_integer_cofactor_seconddhsc) + (ff_value_mdm_prefix_mdr_integer_cofactor_seconddhscm_negative))))))))) /\ ((((exists ff_h_mdr_integer_cofactor_seconddhscp. ff_h_mdr_integer_cofactor_seconddhscp + S (mdr_p_integer_cofactor_seconddhsc) = S ((S (mdr_j_integer_cofactor_seconddhsc)) * mdr_ec_integer_cofactor_seconddhs)) /\ exists ff_q_mdr_integer_cofactor_seconddhscp. mdr_eb_integer_cofactor_seconddhs = ff_q_mdr_integer_cofactor_seconddhscp * S ((S (mdr_j_integer_cofactor_seconddhsc)) * mdr_ec_integer_cofactor_seconddhs) + (mdr_p_integer_cofactor_seconddhsc))) /\ (((exists ff_h_mdr_integer_cofactor_seconddhscn. ff_h_mdr_integer_cofactor_seconddhscn + S (mdr_n_integer_cofactor_seconddhsc) = S ((S (mdr_j_integer_cofactor_seconddhsc)) * mdr_fc_integer_cofactor_seconddhs)) /\ exists ff_q_mdr_integer_cofactor_seconddhscn. mdr_fb_integer_cofactor_seconddhs = ff_q_mdr_integer_cofactor_seconddhscn * S ((S (mdr_j_integer_cofactor_seconddhsc)) * mdr_fc_integer_cofactor_seconddhs) + (mdr_n_integer_cofactor_seconddhsc)))))))) /\ (exists ff_ub_mce_fold_mdr_integer_cofactor_seconddhsf ff_uc_mce_fold_mdr_integer_cofactor_seconddhsf ff_vb_mce_fold_mdr_integer_cofactor_seconddhsf ff_vc_mce_fold_mdr_integer_cofactor_seconddhsf. ((forall ff_index_mce_alternating_mdr_integer_cofactor_seconddhsf_prefix. (exists ff_gap_mce_mdr_integer_cofactor_seconddhsf_prefix_index. ff_gap_mce_mdr_integer_cofactor_seconddhsf_prefix_index + S (ff_index_mce_alternating_mdr_integer_cofactor_seconddhsf_prefix) = (S (mdr_q_integer_cofactor_seconddhs))) -> exists ff_ap_mce_alternating_mdr_integer_cofactor_seconddhsf_prefix ff_an_mce_alternating_mdr_integer_cofactor_seconddhsf_prefix ff_bp_mce_alternating_mdr_integer_cofactor_seconddhsf_prefix ff_bn_mce_alternating_mdr_integer_cofactor_seconddhsf_prefix ff_p_mce_alternating_mdr_integer_cofactor_seconddhsf_prefix ff_n_mce_alternating_mdr_integer_cofactor_seconddhsf_prefix. ((((exists ff_h_mce_mdr_integer_cofactor_seconddhsf_prefix_ap. ff_h_mce_mdr_integer_cofactor_seconddhsf_prefix_ap + S (ff_ap_mce_alternating_mdr_integer_cofactor_seconddhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_integer_cofactor_seconddhsf_prefix)) * mdr_pc_integer_cofactor_seconddh)) /\ exists ff_q_mce_mdr_integer_cofactor_seconddhsf_prefix_ap. mdr_pb_integer_cofactor_seconddh = ff_q_mce_mdr_integer_cofactor_seconddhsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_integer_cofactor_seconddhsf_prefix)) * mdr_pc_integer_cofactor_seconddh) + (ff_ap_mce_alternating_mdr_integer_cofactor_seconddhsf_prefix))) /\ ((((exists ff_h_mce_mdr_integer_cofactor_seconddhsf_prefix_an. ff_h_mce_mdr_integer_cofactor_seconddhsf_prefix_an + S (ff_an_mce_alternating_mdr_integer_cofactor_seconddhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_integer_cofactor_seconddhsf_prefix)) * mdr_nc_integer_cofactor_seconddh)) /\ exists ff_q_mce_mdr_integer_cofactor_seconddhsf_prefix_an. mdr_nb_integer_cofactor_seconddh = ff_q_mce_mdr_integer_cofactor_seconddhsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_integer_cofactor_seconddhsf_prefix)) * mdr_nc_integer_cofactor_seconddh) + (ff_an_mce_alternating_mdr_integer_cofactor_seconddhsf_prefix))) /\ ((((exists ff_h_mce_mdr_integer_cofactor_seconddhsf_prefix_bp. ff_h_mce_mdr_integer_cofactor_seconddhsf_prefix_bp + S (ff_bp_mce_alternating_mdr_integer_cofactor_seconddhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_integer_cofactor_seconddhsf_prefix)) * mdr_ec_integer_cofactor_seconddhs)) /\ exists ff_q_mce_mdr_integer_cofactor_seconddhsf_prefix_bp. mdr_eb_integer_cofactor_seconddhs = ff_q_mce_mdr_integer_cofactor_seconddhsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_integer_cofactor_seconddhsf_prefix)) * mdr_ec_integer_cofactor_seconddhs) + (ff_bp_mce_alternating_mdr_integer_cofactor_seconddhsf_prefix))) /\ ((((exists ff_h_mce_mdr_integer_cofactor_seconddhsf_prefix_bn. ff_h_mce_mdr_integer_cofactor_seconddhsf_prefix_bn + S (ff_bn_mce_alternating_mdr_integer_cofactor_seconddhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_integer_cofactor_seconddhsf_prefix)) * mdr_fc_integer_cofactor_seconddhs)) /\ exists ff_q_mce_mdr_integer_cofactor_seconddhsf_prefix_bn. mdr_fb_integer_cofactor_seconddhs = ff_q_mce_mdr_integer_cofactor_seconddhsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_integer_cofactor_seconddhsf_prefix)) * mdr_fc_integer_cofactor_seconddhs) + (ff_bn_mce_alternating_mdr_integer_cofactor_seconddhsf_prefix))) /\ ((((exists ff_h_mce_mdr_integer_cofactor_seconddhsf_prefix_positive. ff_h_mce_mdr_integer_cofactor_seconddhsf_prefix_positive + S (ff_p_mce_alternating_mdr_integer_cofactor_seconddhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_integer_cofactor_seconddhsf_prefix)) * ff_uc_mce_fold_mdr_integer_cofactor_seconddhsf)) /\ exists ff_q_mce_mdr_integer_cofactor_seconddhsf_prefix_positive. ff_ub_mce_fold_mdr_integer_cofactor_seconddhsf = ff_q_mce_mdr_integer_cofactor_seconddhsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_integer_cofactor_seconddhsf_prefix)) * ff_uc_mce_fold_mdr_integer_cofactor_seconddhsf) + (ff_p_mce_alternating_mdr_integer_cofactor_seconddhsf_prefix))) /\ ((((exists ff_h_mce_mdr_integer_cofactor_seconddhsf_prefix_negative. ff_h_mce_mdr_integer_cofactor_seconddhsf_prefix_negative + S (ff_n_mce_alternating_mdr_integer_cofactor_seconddhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_integer_cofactor_seconddhsf_prefix)) * ff_vc_mce_fold_mdr_integer_cofactor_seconddhsf)) /\ exists ff_q_mce_mdr_integer_cofactor_seconddhsf_prefix_negative. ff_vb_mce_fold_mdr_integer_cofactor_seconddhsf = ff_q_mce_mdr_integer_cofactor_seconddhsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_integer_cofactor_seconddhsf_prefix)) * ff_vc_mce_fold_mdr_integer_cofactor_seconddhsf) + (ff_n_mce_alternating_mdr_integer_cofactor_seconddhsf_prefix))) /\ (((exists ff_even_mce_term_mdr_integer_cofactor_seconddhsf_prefix_term. ff_index_mce_alternating_mdr_integer_cofactor_seconddhsf_prefix = 2 * ff_even_mce_term_mdr_integer_cofactor_seconddhsf_prefix_term) /\ (ff_p_mce_alternating_mdr_integer_cofactor_seconddhsf_prefix = (ff_ap_mce_alternating_mdr_integer_cofactor_seconddhsf_prefix) * (ff_bp_mce_alternating_mdr_integer_cofactor_seconddhsf_prefix) + (ff_an_mce_alternating_mdr_integer_cofactor_seconddhsf_prefix) * (ff_bn_mce_alternating_mdr_integer_cofactor_seconddhsf_prefix) /\ ff_n_mce_alternating_mdr_integer_cofactor_seconddhsf_prefix = (ff_ap_mce_alternating_mdr_integer_cofactor_seconddhsf_prefix) * (ff_bn_mce_alternating_mdr_integer_cofactor_seconddhsf_prefix) + (ff_an_mce_alternating_mdr_integer_cofactor_seconddhsf_prefix) * (ff_bp_mce_alternating_mdr_integer_cofactor_seconddhsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_integer_cofactor_seconddhsf_prefix_term. ff_index_mce_alternating_mdr_integer_cofactor_seconddhsf_prefix = 2 * ff_odd_mce_term_mdr_integer_cofactor_seconddhsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_integer_cofactor_seconddhsf_prefix = (ff_ap_mce_alternating_mdr_integer_cofactor_seconddhsf_prefix) * (ff_bn_mce_alternating_mdr_integer_cofactor_seconddhsf_prefix) + (ff_an_mce_alternating_mdr_integer_cofactor_seconddhsf_prefix) * (ff_bp_mce_alternating_mdr_integer_cofactor_seconddhsf_prefix) /\ ff_n_mce_alternating_mdr_integer_cofactor_seconddhsf_prefix = (ff_ap_mce_alternating_mdr_integer_cofactor_seconddhsf_prefix) * (ff_bp_mce_alternating_mdr_integer_cofactor_seconddhsf_prefix) + (ff_an_mce_alternating_mdr_integer_cofactor_seconddhsf_prefix) * (ff_bn_mce_alternating_mdr_integer_cofactor_seconddhsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_integer_cofactor_seconddhsf_positive ff_v_mce_mdr_integer_cofactor_seconddhsf_positive. ((((exists ff_h_mce_mdr_integer_cofactor_seconddhsf_positive_start. ff_h_mce_mdr_integer_cofactor_seconddhsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_integer_cofactor_seconddhsf_positive)) /\ exists ff_q_mce_mdr_integer_cofactor_seconddhsf_positive_start. ff_u_mce_mdr_integer_cofactor_seconddhsf_positive = ff_q_mce_mdr_integer_cofactor_seconddhsf_positive_start * S ((S (0)) * ff_v_mce_mdr_integer_cofactor_seconddhsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_integer_cofactor_seconddhsf_positive_terminal. ff_h_mce_mdr_integer_cofactor_seconddhsf_positive_terminal + S (mdr_p_integer_cofactor_seconddh) = S ((S ((S (mdr_q_integer_cofactor_seconddhs)))) * ff_v_mce_mdr_integer_cofactor_seconddhsf_positive)) /\ exists ff_q_mce_mdr_integer_cofactor_seconddhsf_positive_terminal. ff_u_mce_mdr_integer_cofactor_seconddhsf_positive = ff_q_mce_mdr_integer_cofactor_seconddhsf_positive_terminal * S ((S ((S (mdr_q_integer_cofactor_seconddhs)))) * ff_v_mce_mdr_integer_cofactor_seconddhsf_positive) + (mdr_p_integer_cofactor_seconddh))) /\ forall ff_i_mce_mdr_integer_cofactor_seconddhsf_positive. (exists ff_lt_mce_mdr_integer_cofactor_seconddhsf_positive_bound. ff_lt_mce_mdr_integer_cofactor_seconddhsf_positive_bound + S ff_i_mce_mdr_integer_cofactor_seconddhsf_positive = (S (mdr_q_integer_cofactor_seconddhs))) -> exists ff_a_mce_mdr_integer_cofactor_seconddhsf_positive ff_r_mce_mdr_integer_cofactor_seconddhsf_positive ff_s_mce_mdr_integer_cofactor_seconddhsf_positive. ((((exists ff_h_mce_mdr_integer_cofactor_seconddhsf_positive_summand. ff_h_mce_mdr_integer_cofactor_seconddhsf_positive_summand + S (ff_a_mce_mdr_integer_cofactor_seconddhsf_positive) = S ((S (ff_i_mce_mdr_integer_cofactor_seconddhsf_positive)) * ff_uc_mce_fold_mdr_integer_cofactor_seconddhsf)) /\ exists ff_q_mce_mdr_integer_cofactor_seconddhsf_positive_summand. ff_ub_mce_fold_mdr_integer_cofactor_seconddhsf = ff_q_mce_mdr_integer_cofactor_seconddhsf_positive_summand * S ((S (ff_i_mce_mdr_integer_cofactor_seconddhsf_positive)) * ff_uc_mce_fold_mdr_integer_cofactor_seconddhsf) + (ff_a_mce_mdr_integer_cofactor_seconddhsf_positive))) /\ ((((exists ff_h_mce_mdr_integer_cofactor_seconddhsf_positive_partial. ff_h_mce_mdr_integer_cofactor_seconddhsf_positive_partial + S (ff_r_mce_mdr_integer_cofactor_seconddhsf_positive) = S ((S (ff_i_mce_mdr_integer_cofactor_seconddhsf_positive)) * ff_v_mce_mdr_integer_cofactor_seconddhsf_positive)) /\ exists ff_q_mce_mdr_integer_cofactor_seconddhsf_positive_partial. ff_u_mce_mdr_integer_cofactor_seconddhsf_positive = ff_q_mce_mdr_integer_cofactor_seconddhsf_positive_partial * S ((S (ff_i_mce_mdr_integer_cofactor_seconddhsf_positive)) * ff_v_mce_mdr_integer_cofactor_seconddhsf_positive) + (ff_r_mce_mdr_integer_cofactor_seconddhsf_positive))) /\ ((((exists ff_h_mce_mdr_integer_cofactor_seconddhsf_positive_successor. ff_h_mce_mdr_integer_cofactor_seconddhsf_positive_successor + S (ff_s_mce_mdr_integer_cofactor_seconddhsf_positive) = S ((S (S ff_i_mce_mdr_integer_cofactor_seconddhsf_positive)) * ff_v_mce_mdr_integer_cofactor_seconddhsf_positive)) /\ exists ff_q_mce_mdr_integer_cofactor_seconddhsf_positive_successor. ff_u_mce_mdr_integer_cofactor_seconddhsf_positive = ff_q_mce_mdr_integer_cofactor_seconddhsf_positive_successor * S ((S (S ff_i_mce_mdr_integer_cofactor_seconddhsf_positive)) * ff_v_mce_mdr_integer_cofactor_seconddhsf_positive) + (ff_s_mce_mdr_integer_cofactor_seconddhsf_positive))) /\ ff_s_mce_mdr_integer_cofactor_seconddhsf_positive = ff_r_mce_mdr_integer_cofactor_seconddhsf_positive + ff_a_mce_mdr_integer_cofactor_seconddhsf_positive)))))) /\ (exists ff_u_mce_mdr_integer_cofactor_seconddhsf_negative ff_v_mce_mdr_integer_cofactor_seconddhsf_negative. ((((exists ff_h_mce_mdr_integer_cofactor_seconddhsf_negative_start. ff_h_mce_mdr_integer_cofactor_seconddhsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_integer_cofactor_seconddhsf_negative)) /\ exists ff_q_mce_mdr_integer_cofactor_seconddhsf_negative_start. ff_u_mce_mdr_integer_cofactor_seconddhsf_negative = ff_q_mce_mdr_integer_cofactor_seconddhsf_negative_start * S ((S (0)) * ff_v_mce_mdr_integer_cofactor_seconddhsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_integer_cofactor_seconddhsf_negative_terminal. ff_h_mce_mdr_integer_cofactor_seconddhsf_negative_terminal + S (mdr_n_integer_cofactor_seconddh) = S ((S ((S (mdr_q_integer_cofactor_seconddhs)))) * ff_v_mce_mdr_integer_cofactor_seconddhsf_negative)) /\ exists ff_q_mce_mdr_integer_cofactor_seconddhsf_negative_terminal. ff_u_mce_mdr_integer_cofactor_seconddhsf_negative = ff_q_mce_mdr_integer_cofactor_seconddhsf_negative_terminal * S ((S ((S (mdr_q_integer_cofactor_seconddhs)))) * ff_v_mce_mdr_integer_cofactor_seconddhsf_negative) + (mdr_n_integer_cofactor_seconddh))) /\ forall ff_i_mce_mdr_integer_cofactor_seconddhsf_negative. (exists ff_lt_mce_mdr_integer_cofactor_seconddhsf_negative_bound. ff_lt_mce_mdr_integer_cofactor_seconddhsf_negative_bound + S ff_i_mce_mdr_integer_cofactor_seconddhsf_negative = (S (mdr_q_integer_cofactor_seconddhs))) -> exists ff_a_mce_mdr_integer_cofactor_seconddhsf_negative ff_r_mce_mdr_integer_cofactor_seconddhsf_negative ff_s_mce_mdr_integer_cofactor_seconddhsf_negative. ((((exists ff_h_mce_mdr_integer_cofactor_seconddhsf_negative_summand. ff_h_mce_mdr_integer_cofactor_seconddhsf_negative_summand + S (ff_a_mce_mdr_integer_cofactor_seconddhsf_negative) = S ((S (ff_i_mce_mdr_integer_cofactor_seconddhsf_negative)) * ff_vc_mce_fold_mdr_integer_cofactor_seconddhsf)) /\ exists ff_q_mce_mdr_integer_cofactor_seconddhsf_negative_summand. ff_vb_mce_fold_mdr_integer_cofactor_seconddhsf = ff_q_mce_mdr_integer_cofactor_seconddhsf_negative_summand * S ((S (ff_i_mce_mdr_integer_cofactor_seconddhsf_negative)) * ff_vc_mce_fold_mdr_integer_cofactor_seconddhsf) + (ff_a_mce_mdr_integer_cofactor_seconddhsf_negative))) /\ ((((exists ff_h_mce_mdr_integer_cofactor_seconddhsf_negative_partial. ff_h_mce_mdr_integer_cofactor_seconddhsf_negative_partial + S (ff_r_mce_mdr_integer_cofactor_seconddhsf_negative) = S ((S (ff_i_mce_mdr_integer_cofactor_seconddhsf_negative)) * ff_v_mce_mdr_integer_cofactor_seconddhsf_negative)) /\ exists ff_q_mce_mdr_integer_cofactor_seconddhsf_negative_partial. ff_u_mce_mdr_integer_cofactor_seconddhsf_negative = ff_q_mce_mdr_integer_cofactor_seconddhsf_negative_partial * S ((S (ff_i_mce_mdr_integer_cofactor_seconddhsf_negative)) * ff_v_mce_mdr_integer_cofactor_seconddhsf_negative) + (ff_r_mce_mdr_integer_cofactor_seconddhsf_negative))) /\ ((((exists ff_h_mce_mdr_integer_cofactor_seconddhsf_negative_successor. ff_h_mce_mdr_integer_cofactor_seconddhsf_negative_successor + S (ff_s_mce_mdr_integer_cofactor_seconddhsf_negative) = S ((S (S ff_i_mce_mdr_integer_cofactor_seconddhsf_negative)) * ff_v_mce_mdr_integer_cofactor_seconddhsf_negative)) /\ exists ff_q_mce_mdr_integer_cofactor_seconddhsf_negative_successor. ff_u_mce_mdr_integer_cofactor_seconddhsf_negative = ff_q_mce_mdr_integer_cofactor_seconddhsf_negative_successor * S ((S (S ff_i_mce_mdr_integer_cofactor_seconddhsf_negative)) * ff_v_mce_mdr_integer_cofactor_seconddhsf_negative) + (ff_s_mce_mdr_integer_cofactor_seconddhsf_negative))) /\ ff_s_mce_mdr_integer_cofactor_seconddhsf_negative = ff_r_mce_mdr_integer_cofactor_seconddhsf_negative + ff_a_mce_mdr_integer_cofactor_seconddhsf_negative))))))))))))))) /\ ((exists mdr_gap_integer_cofactor_seconddi. mdr_gap_integer_cofactor_seconddi + S (mdr_i_integer_cofactor_secondd) = (mdr_l_integer_cofactor_secondd)) /\ (exists mdr_z_integer_cofactor_seconddr. ((exists mdr_a_integer_cofactor_seconddrc mdr_b_integer_cofactor_seconddrc mdr_c_integer_cofactor_seconddrc mdr_e_integer_cofactor_seconddrc mdr_f_integer_cofactor_seconddrc. ((mdr_a_integer_cofactor_seconddrc = ((q) + (mdr_up_integer_cofactor_second)) * S ((q) + (mdr_up_integer_cofactor_second)) + ((mdr_up_integer_cofactor_second) + (mdr_up_integer_cofactor_second))) /\ ((mdr_b_integer_cofactor_seconddrc = ((mdr_us_integer_cofactor_second) + (mdr_un_integer_cofactor_second)) * S ((mdr_us_integer_cofactor_second) + (mdr_un_integer_cofactor_second)) + ((mdr_un_integer_cofactor_second) + (mdr_un_integer_cofactor_second))) /\ ((mdr_c_integer_cofactor_seconddrc = ((mdr_a_integer_cofactor_seconddrc) + (mdr_b_integer_cofactor_seconddrc)) * S ((mdr_a_integer_cofactor_seconddrc) + (mdr_b_integer_cofactor_seconddrc)) + ((mdr_b_integer_cofactor_seconddrc) + (mdr_b_integer_cofactor_seconddrc))) /\ ((mdr_e_integer_cofactor_seconddrc = ((mdr_p_integer_cofactor_second) + (mdr_n_integer_cofactor_second)) * S ((mdr_p_integer_cofactor_second) + (mdr_n_integer_cofactor_second)) + ((mdr_n_integer_cofactor_second) + (mdr_n_integer_cofactor_second))) /\ ((mdr_f_integer_cofactor_seconddrc = ((mdr_ut_integer_cofactor_second) + (mdr_e_integer_cofactor_seconddrc)) * S ((mdr_ut_integer_cofactor_second) + (mdr_e_integer_cofactor_seconddrc)) + ((mdr_e_integer_cofactor_seconddrc) + (mdr_e_integer_cofactor_seconddrc))) /\ ((mdr_z_integer_cofactor_seconddr) = ((mdr_c_integer_cofactor_seconddrc) + (mdr_f_integer_cofactor_seconddrc)) * S ((mdr_c_integer_cofactor_seconddrc) + (mdr_f_integer_cofactor_seconddrc)) + ((mdr_f_integer_cofactor_seconddrc) + (mdr_f_integer_cofactor_seconddrc))))))))) /\ (((exists ff_h_mdr_integer_cofactor_seconddrb. ff_h_mdr_integer_cofactor_seconddrb + S (mdr_z_integer_cofactor_seconddr) = S ((S (mdr_i_integer_cofactor_secondd)) * mdr_c_integer_cofactor_secondd)) /\ exists ff_q_mdr_integer_cofactor_seconddrb. mdr_b_integer_cofactor_secondd = ff_q_mdr_integer_cofactor_seconddrb * S ((S (mdr_i_integer_cofactor_secondd)) * mdr_c_integer_cofactor_secondd) + (mdr_z_integer_cofactor_seconddr)))))))) /\ ((((exists ff_h_mdr_integer_cofactor_secondp. ff_h_mdr_integer_cofactor_secondp + S (mdr_p_integer_cofactor_second) = S ((S (mdr_j_integer_cofactor_second)) * gc)) /\ exists ff_q_mdr_integer_cofactor_secondp. gb = ff_q_mdr_integer_cofactor_secondp * S ((S (mdr_j_integer_cofactor_second)) * gc) + (mdr_p_integer_cofactor_second))) /\ (((exists ff_h_mdr_integer_cofactor_secondn. ff_h_mdr_integer_cofactor_secondn + S (mdr_n_integer_cofactor_second) = S ((S (mdr_j_integer_cofactor_second)) * hc)) /\ exists ff_q_mdr_integer_cofactor_secondn. hb = ff_q_mdr_integer_cofactor_secondn * S ((S (mdr_j_integer_cofactor_second)) * hc) + (mdr_n_integer_cofactor_second))))))) -> (forall ics_index_integer_cofactor_streams ics_value0_integer_cofactor_streams ics_value1_integer_cofactor_streams ics_value2_integer_cofactor_streams ics_value3_integer_cofactor_streams. (exists ics_gap_integer_cofactor_streams_bound. ics_gap_integer_cofactor_streams_bound + S (ics_index_integer_cofactor_streams) = (S q)) -> (((exists fs_h_ics_integer_cofactor_streams_at0. fs_h_ics_integer_cofactor_streams_at0 + S (ics_value0_integer_cofactor_streams) = S ((S (ics_index_integer_cofactor_streams)) * cc)) /\ exists fs_q_ics_integer_cofactor_streams_at0. cb = fs_q_ics_integer_cofactor_streams_at0 * S ((S (ics_index_integer_cofactor_streams)) * cc) + (ics_value0_integer_cofactor_streams))) -> (((exists fs_h_ics_integer_cofactor_streams_at1. fs_h_ics_integer_cofactor_streams_at1 + S (ics_value1_integer_cofactor_streams) = S ((S (ics_index_integer_cofactor_streams)) * dc)) /\ exists fs_q_ics_integer_cofactor_streams_at1. db = fs_q_ics_integer_cofactor_streams_at1 * S ((S (ics_index_integer_cofactor_streams)) * dc) + (ics_value1_integer_cofactor_streams))) -> (((exists fs_h_ics_integer_cofactor_streams_at2. fs_h_ics_integer_cofactor_streams_at2 + S (ics_value2_integer_cofactor_streams) = S ((S (ics_index_integer_cofactor_streams)) * gc)) /\ exists fs_q_ics_integer_cofactor_streams_at2. gb = fs_q_ics_integer_cofactor_streams_at2 * S ((S (ics_index_integer_cofactor_streams)) * gc) + (ics_value2_integer_cofactor_streams))) -> (((exists fs_h_ics_integer_cofactor_streams_at3. fs_h_ics_integer_cofactor_streams_at3 + S (ics_value3_integer_cofactor_streams) = S ((S (ics_index_integer_cofactor_streams)) * hc)) /\ exists fs_q_ics_integer_cofactor_streams_at3. hb = fs_q_ics_integer_cofactor_streams_at3 * S ((S (ics_index_integer_cofactor_streams)) * hc) + (ics_value3_integer_cofactor_streams))) -> ics_value0_integer_cofactor_streams + ics_value3_integer_cofactor_streams = ics_value2_integer_cofactor_streams + ics_value1_integer_cofactor_streams)