matrix_recursive_determinant_extensional

Exact expanded first-order arithmetic statement

forall d. (forall mdr_pb_all_extensional mdr_pc_all_extensional mdr_nb_all_extensional mdr_nc_all_extensional mdr_qb_all_extensional mdr_qc_all_extensional mdr_rb_all_extensional mdr_rc_all_extensional mdr_p_all_extensional mdr_n_all_extensional mdr_r_all_extensional mdr_s_all_extensional. (((forall mdr_i_all_extensionalmp mdr_a_all_extensionalmp. (exists mdr_gap_all_extensionalmpb. mdr_gap_all_extensionalmpb + S (mdr_i_all_extensionalmp) = ((d) * (d))) -> (((exists ff_h_mdr_all_extensionalmpo. ff_h_mdr_all_extensionalmpo + S (mdr_a_all_extensionalmp) = S ((S (mdr_i_all_extensionalmp)) * mdr_pc_all_extensional)) /\ exists ff_q_mdr_all_extensionalmpo. mdr_pb_all_extensional = ff_q_mdr_all_extensionalmpo * S ((S (mdr_i_all_extensionalmp)) * mdr_pc_all_extensional) + (mdr_a_all_extensionalmp))) -> (((exists ff_h_mdr_all_extensionalmpn. ff_h_mdr_all_extensionalmpn + S (mdr_a_all_extensionalmp) = S ((S (mdr_i_all_extensionalmp)) * mdr_qc_all_extensional)) /\ exists ff_q_mdr_all_extensionalmpn. mdr_qb_all_extensional = ff_q_mdr_all_extensionalmpn * S ((S (mdr_i_all_extensionalmp)) * mdr_qc_all_extensional) + (mdr_a_all_extensionalmp)))) /\ (forall mdr_i_all_extensionalmn mdr_a_all_extensionalmn. (exists mdr_gap_all_extensionalmnb. mdr_gap_all_extensionalmnb + S (mdr_i_all_extensionalmn) = ((d) * (d))) -> (((exists ff_h_mdr_all_extensionalmno. ff_h_mdr_all_extensionalmno + S (mdr_a_all_extensionalmn) = S ((S (mdr_i_all_extensionalmn)) * mdr_nc_all_extensional)) /\ exists ff_q_mdr_all_extensionalmno. mdr_nb_all_extensional = ff_q_mdr_all_extensionalmno * S ((S (mdr_i_all_extensionalmn)) * mdr_nc_all_extensional) + (mdr_a_all_extensionalmn))) -> (((exists ff_h_mdr_all_extensionalmnn. ff_h_mdr_all_extensionalmnn + S (mdr_a_all_extensionalmn) = S ((S (mdr_i_all_extensionalmn)) * mdr_rc_all_extensional)) /\ exists ff_q_mdr_all_extensionalmnn. mdr_rb_all_extensional = ff_q_mdr_all_extensionalmnn * S ((S (mdr_i_all_extensionalmn)) * mdr_rc_all_extensional) + (mdr_a_all_extensionalmn)))))) -> (exists mdr_b_all_extensionala mdr_c_all_extensionala mdr_l_all_extensionala mdr_i_all_extensionala. ((forall mdr_i_all_extensionalah. (exists mdr_gap_all_extensionalahi. mdr_gap_all_extensionalahi + S (mdr_i_all_extensionalah) = (mdr_l_all_extensionala)) -> exists mdr_d_all_extensionalah mdr_pb_all_extensionalah mdr_pc_all_extensionalah mdr_nb_all_extensionalah mdr_nc_all_extensionalah mdr_p_all_extensionalah mdr_n_all_extensionalah. ((exists mdr_z_all_extensionalahr. ((exists mdr_a_all_extensionalahrc mdr_b_all_extensionalahrc mdr_c_all_extensionalahrc mdr_e_all_extensionalahrc mdr_f_all_extensionalahrc. ((mdr_a_all_extensionalahrc = ((mdr_d_all_extensionalah) + (mdr_pb_all_extensionalah)) * S ((mdr_d_all_extensionalah) + (mdr_pb_all_extensionalah)) + ((mdr_pb_all_extensionalah) + (mdr_pb_all_extensionalah))) /\ ((mdr_b_all_extensionalahrc = ((mdr_pc_all_extensionalah) + (mdr_nb_all_extensionalah)) * S ((mdr_pc_all_extensionalah) + (mdr_nb_all_extensionalah)) + ((mdr_nb_all_extensionalah) + (mdr_nb_all_extensionalah))) /\ ((mdr_c_all_extensionalahrc = ((mdr_a_all_extensionalahrc) + (mdr_b_all_extensionalahrc)) * S ((mdr_a_all_extensionalahrc) + (mdr_b_all_extensionalahrc)) + ((mdr_b_all_extensionalahrc) + (mdr_b_all_extensionalahrc))) /\ ((mdr_e_all_extensionalahrc = ((mdr_p_all_extensionalah) + (mdr_n_all_extensionalah)) * S ((mdr_p_all_extensionalah) + (mdr_n_all_extensionalah)) + ((mdr_n_all_extensionalah) + (mdr_n_all_extensionalah))) /\ ((mdr_f_all_extensionalahrc = ((mdr_nc_all_extensionalah) + (mdr_e_all_extensionalahrc)) * S ((mdr_nc_all_extensionalah) + (mdr_e_all_extensionalahrc)) + ((mdr_e_all_extensionalahrc) + (mdr_e_all_extensionalahrc))) /\ ((mdr_z_all_extensionalahr) = ((mdr_c_all_extensionalahrc) + (mdr_f_all_extensionalahrc)) * S ((mdr_c_all_extensionalahrc) + (mdr_f_all_extensionalahrc)) + ((mdr_f_all_extensionalahrc) + (mdr_f_all_extensionalahrc))))))))) /\ (((exists ff_h_mdr_all_extensionalahrb. ff_h_mdr_all_extensionalahrb + S (mdr_z_all_extensionalahr) = S ((S (mdr_i_all_extensionalah)) * mdr_c_all_extensionala)) /\ exists ff_q_mdr_all_extensionalahrb. mdr_b_all_extensionala = ff_q_mdr_all_extensionalahrb * S ((S (mdr_i_all_extensionalah)) * mdr_c_all_extensionala) + (mdr_z_all_extensionalahr))))) /\ (((((mdr_d_all_extensionalah) = 0) /\ (((mdr_p_all_extensionalah) = 1) /\ ((mdr_n_all_extensionalah) = 0))) \/ exists mdr_q_all_extensionalahs mdr_eb_all_extensionalahs mdr_ec_all_extensionalahs mdr_fb_all_extensionalahs mdr_fc_all_extensionalahs. (((mdr_d_all_extensionalah) = S (mdr_q_all_extensionalahs)) /\ ((forall mdr_j_all_extensionalahsc. (exists mdr_gap_all_extensionalahscj. mdr_gap_all_extensionalahscj + S (mdr_j_all_extensionalahsc) = (S (mdr_q_all_extensionalahs))) -> exists mdr_i_all_extensionalahsc mdr_up_all_extensionalahsc mdr_us_all_extensionalahsc mdr_un_all_extensionalahsc mdr_ut_all_extensionalahsc mdr_p_all_extensionalahsc mdr_n_all_extensionalahsc. ((exists mdr_gap_all_extensionalahsci. mdr_gap_all_extensionalahsci + S (mdr_i_all_extensionalahsc) = (mdr_i_all_extensionalah)) /\ ((exists mdr_z_all_extensionalahscr. ((exists mdr_a_all_extensionalahscrc mdr_b_all_extensionalahscrc mdr_c_all_extensionalahscrc mdr_e_all_extensionalahscrc mdr_f_all_extensionalahscrc. ((mdr_a_all_extensionalahscrc = ((mdr_q_all_extensionalahs) + (mdr_up_all_extensionalahsc)) * S ((mdr_q_all_extensionalahs) + (mdr_up_all_extensionalahsc)) + ((mdr_up_all_extensionalahsc) + (mdr_up_all_extensionalahsc))) /\ ((mdr_b_all_extensionalahscrc = ((mdr_us_all_extensionalahsc) + (mdr_un_all_extensionalahsc)) * S ((mdr_us_all_extensionalahsc) + (mdr_un_all_extensionalahsc)) + ((mdr_un_all_extensionalahsc) + (mdr_un_all_extensionalahsc))) /\ ((mdr_c_all_extensionalahscrc = ((mdr_a_all_extensionalahscrc) + (mdr_b_all_extensionalahscrc)) * S ((mdr_a_all_extensionalahscrc) + (mdr_b_all_extensionalahscrc)) + ((mdr_b_all_extensionalahscrc) + (mdr_b_all_extensionalahscrc))) /\ ((mdr_e_all_extensionalahscrc = ((mdr_p_all_extensionalahsc) + (mdr_n_all_extensionalahsc)) * S ((mdr_p_all_extensionalahsc) + (mdr_n_all_extensionalahsc)) + ((mdr_n_all_extensionalahsc) + (mdr_n_all_extensionalahsc))) /\ ((mdr_f_all_extensionalahscrc = ((mdr_ut_all_extensionalahsc) + (mdr_e_all_extensionalahscrc)) * S ((mdr_ut_all_extensionalahsc) + (mdr_e_all_extensionalahscrc)) + ((mdr_e_all_extensionalahscrc) + (mdr_e_all_extensionalahscrc))) /\ ((mdr_z_all_extensionalahscr) = ((mdr_c_all_extensionalahscrc) + (mdr_f_all_extensionalahscrc)) * S ((mdr_c_all_extensionalahscrc) + (mdr_f_all_extensionalahscrc)) + ((mdr_f_all_extensionalahscrc) + (mdr_f_all_extensionalahscrc))))))))) /\ (((exists ff_h_mdr_all_extensionalahscrb. ff_h_mdr_all_extensionalahscrb + S (mdr_z_all_extensionalahscr) = S ((S (mdr_i_all_extensionalahsc)) * mdr_c_all_extensionala)) /\ exists ff_q_mdr_all_extensionalahscrb. mdr_b_all_extensionala = ff_q_mdr_all_extensionalahscrb * S ((S (mdr_i_all_extensionalahsc)) * mdr_c_all_extensionala) + (mdr_z_all_extensionalahscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_all_extensionalahscm_positive. (exists ff_gap_mdm_lt_mdr_all_extensionalahscm_positive_index_bound. ff_gap_mdm_lt_mdr_all_extensionalahscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_all_extensionalahscm_positive) = ((mdr_q_all_extensionalahs) * (mdr_q_all_extensionalahs))) -> exists ff_row_mdm_prefix_mdr_all_extensionalahscm_positive ff_column_mdm_prefix_mdr_all_extensionalahscm_positive ff_value_mdm_prefix_mdr_all_extensionalahscm_positive. (ff_index_mdm_prefix_mdr_all_extensionalahscm_positive = (mdr_q_all_extensionalahs) * ff_row_mdm_prefix_mdr_all_extensionalahscm_positive + ff_column_mdm_prefix_mdr_all_extensionalahscm_positive /\ ((exists ff_gap_mdm_lt_mdr_all_extensionalahscm_positive_column_bound. ff_gap_mdm_lt_mdr_all_extensionalahscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_all_extensionalahscm_positive) = (mdr_q_all_extensionalahs)) /\ ((exists ff_row_mdm_cell_mdr_all_extensionalahscm_positive_cell ff_column_mdm_cell_mdr_all_extensionalahscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_all_extensionalahscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_all_extensionalahscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_all_extensionalahscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_all_extensionalahscm_positive_cell = ff_row_mdm_prefix_mdr_all_extensionalahscm_positive) \/ ((exists ff_gap_mdm_le_mdr_all_extensionalahscm_positive_cell_row_after. ff_gap_mdm_le_mdr_all_extensionalahscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_all_extensionalahscm_positive)) /\ ff_row_mdm_cell_mdr_all_extensionalahscm_positive_cell = S ff_row_mdm_prefix_mdr_all_extensionalahscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_all_extensionalahscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_all_extensionalahscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_all_extensionalahscm_positive) = (mdr_j_all_extensionalahsc)) /\ ff_column_mdm_cell_mdr_all_extensionalahscm_positive_cell = ff_column_mdm_prefix_mdr_all_extensionalahscm_positive) \/ ((exists ff_gap_mdm_le_mdr_all_extensionalahscm_positive_cell_column_after. ff_gap_mdm_le_mdr_all_extensionalahscm_positive_cell_column_after + (mdr_j_all_extensionalahsc) = (ff_column_mdm_prefix_mdr_all_extensionalahscm_positive)) /\ ff_column_mdm_cell_mdr_all_extensionalahscm_positive_cell = S ff_column_mdm_prefix_mdr_all_extensionalahscm_positive))) /\ (((exists ff_h_mdm_mdr_all_extensionalahscm_positive_cell_source. ff_h_mdm_mdr_all_extensionalahscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_all_extensionalahscm_positive) = S ((S ((ff_row_mdm_cell_mdr_all_extensionalahscm_positive_cell) * (S (mdr_q_all_extensionalahs)) + (ff_column_mdm_cell_mdr_all_extensionalahscm_positive_cell))) * mdr_pc_all_extensionalah)) /\ exists ff_q_mdm_mdr_all_extensionalahscm_positive_cell_source. mdr_pb_all_extensionalah = ff_q_mdm_mdr_all_extensionalahscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_all_extensionalahscm_positive_cell) * (S (mdr_q_all_extensionalahs)) + (ff_column_mdm_cell_mdr_all_extensionalahscm_positive_cell))) * mdr_pc_all_extensionalah) + (ff_value_mdm_prefix_mdr_all_extensionalahscm_positive)))))) /\ (((exists ff_h_mdm_mdr_all_extensionalahscm_positive_target. ff_h_mdm_mdr_all_extensionalahscm_positive_target + S (ff_value_mdm_prefix_mdr_all_extensionalahscm_positive) = S ((S (ff_index_mdm_prefix_mdr_all_extensionalahscm_positive)) * mdr_us_all_extensionalahsc)) /\ exists ff_q_mdm_mdr_all_extensionalahscm_positive_target. mdr_up_all_extensionalahsc = ff_q_mdm_mdr_all_extensionalahscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_all_extensionalahscm_positive)) * mdr_us_all_extensionalahsc) + (ff_value_mdm_prefix_mdr_all_extensionalahscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_all_extensionalahscm_negative. (exists ff_gap_mdm_lt_mdr_all_extensionalahscm_negative_index_bound. ff_gap_mdm_lt_mdr_all_extensionalahscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_all_extensionalahscm_negative) = ((mdr_q_all_extensionalahs) * (mdr_q_all_extensionalahs))) -> exists ff_row_mdm_prefix_mdr_all_extensionalahscm_negative ff_column_mdm_prefix_mdr_all_extensionalahscm_negative ff_value_mdm_prefix_mdr_all_extensionalahscm_negative. (ff_index_mdm_prefix_mdr_all_extensionalahscm_negative = (mdr_q_all_extensionalahs) * ff_row_mdm_prefix_mdr_all_extensionalahscm_negative + ff_column_mdm_prefix_mdr_all_extensionalahscm_negative /\ ((exists ff_gap_mdm_lt_mdr_all_extensionalahscm_negative_column_bound. ff_gap_mdm_lt_mdr_all_extensionalahscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_all_extensionalahscm_negative) = (mdr_q_all_extensionalahs)) /\ ((exists ff_row_mdm_cell_mdr_all_extensionalahscm_negative_cell ff_column_mdm_cell_mdr_all_extensionalahscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_all_extensionalahscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_all_extensionalahscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_all_extensionalahscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_all_extensionalahscm_negative_cell = ff_row_mdm_prefix_mdr_all_extensionalahscm_negative) \/ ((exists ff_gap_mdm_le_mdr_all_extensionalahscm_negative_cell_row_after. ff_gap_mdm_le_mdr_all_extensionalahscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_all_extensionalahscm_negative)) /\ ff_row_mdm_cell_mdr_all_extensionalahscm_negative_cell = S ff_row_mdm_prefix_mdr_all_extensionalahscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_all_extensionalahscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_all_extensionalahscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_all_extensionalahscm_negative) = (mdr_j_all_extensionalahsc)) /\ ff_column_mdm_cell_mdr_all_extensionalahscm_negative_cell = ff_column_mdm_prefix_mdr_all_extensionalahscm_negative) \/ ((exists ff_gap_mdm_le_mdr_all_extensionalahscm_negative_cell_column_after. ff_gap_mdm_le_mdr_all_extensionalahscm_negative_cell_column_after + (mdr_j_all_extensionalahsc) = (ff_column_mdm_prefix_mdr_all_extensionalahscm_negative)) /\ ff_column_mdm_cell_mdr_all_extensionalahscm_negative_cell = S ff_column_mdm_prefix_mdr_all_extensionalahscm_negative))) /\ (((exists ff_h_mdm_mdr_all_extensionalahscm_negative_cell_source. ff_h_mdm_mdr_all_extensionalahscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_all_extensionalahscm_negative) = S ((S ((ff_row_mdm_cell_mdr_all_extensionalahscm_negative_cell) * (S (mdr_q_all_extensionalahs)) + (ff_column_mdm_cell_mdr_all_extensionalahscm_negative_cell))) * mdr_nc_all_extensionalah)) /\ exists ff_q_mdm_mdr_all_extensionalahscm_negative_cell_source. mdr_nb_all_extensionalah = ff_q_mdm_mdr_all_extensionalahscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_all_extensionalahscm_negative_cell) * (S (mdr_q_all_extensionalahs)) + (ff_column_mdm_cell_mdr_all_extensionalahscm_negative_cell))) * mdr_nc_all_extensionalah) + (ff_value_mdm_prefix_mdr_all_extensionalahscm_negative)))))) /\ (((exists ff_h_mdm_mdr_all_extensionalahscm_negative_target. ff_h_mdm_mdr_all_extensionalahscm_negative_target + S (ff_value_mdm_prefix_mdr_all_extensionalahscm_negative) = S ((S (ff_index_mdm_prefix_mdr_all_extensionalahscm_negative)) * mdr_ut_all_extensionalahsc)) /\ exists ff_q_mdm_mdr_all_extensionalahscm_negative_target. mdr_un_all_extensionalahsc = ff_q_mdm_mdr_all_extensionalahscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_all_extensionalahscm_negative)) * mdr_ut_all_extensionalahsc) + (ff_value_mdm_prefix_mdr_all_extensionalahscm_negative))))))))) /\ ((((exists ff_h_mdr_all_extensionalahscp. ff_h_mdr_all_extensionalahscp + S (mdr_p_all_extensionalahsc) = S ((S (mdr_j_all_extensionalahsc)) * mdr_ec_all_extensionalahs)) /\ exists ff_q_mdr_all_extensionalahscp. mdr_eb_all_extensionalahs = ff_q_mdr_all_extensionalahscp * S ((S (mdr_j_all_extensionalahsc)) * mdr_ec_all_extensionalahs) + (mdr_p_all_extensionalahsc))) /\ (((exists ff_h_mdr_all_extensionalahscn. ff_h_mdr_all_extensionalahscn + S (mdr_n_all_extensionalahsc) = S ((S (mdr_j_all_extensionalahsc)) * mdr_fc_all_extensionalahs)) /\ exists ff_q_mdr_all_extensionalahscn. mdr_fb_all_extensionalahs = ff_q_mdr_all_extensionalahscn * S ((S (mdr_j_all_extensionalahsc)) * mdr_fc_all_extensionalahs) + (mdr_n_all_extensionalahsc)))))))) /\ (exists ff_ub_mce_fold_mdr_all_extensionalahsf ff_uc_mce_fold_mdr_all_extensionalahsf ff_vb_mce_fold_mdr_all_extensionalahsf ff_vc_mce_fold_mdr_all_extensionalahsf. ((forall ff_index_mce_alternating_mdr_all_extensionalahsf_prefix. (exists ff_gap_mce_mdr_all_extensionalahsf_prefix_index. ff_gap_mce_mdr_all_extensionalahsf_prefix_index + S (ff_index_mce_alternating_mdr_all_extensionalahsf_prefix) = (S (mdr_q_all_extensionalahs))) -> exists ff_ap_mce_alternating_mdr_all_extensionalahsf_prefix ff_an_mce_alternating_mdr_all_extensionalahsf_prefix ff_bp_mce_alternating_mdr_all_extensionalahsf_prefix ff_bn_mce_alternating_mdr_all_extensionalahsf_prefix ff_p_mce_alternating_mdr_all_extensionalahsf_prefix ff_n_mce_alternating_mdr_all_extensionalahsf_prefix. ((((exists ff_h_mce_mdr_all_extensionalahsf_prefix_ap. ff_h_mce_mdr_all_extensionalahsf_prefix_ap + S (ff_ap_mce_alternating_mdr_all_extensionalahsf_prefix) = S ((S (ff_index_mce_alternating_mdr_all_extensionalahsf_prefix)) * mdr_pc_all_extensionalah)) /\ exists ff_q_mce_mdr_all_extensionalahsf_prefix_ap. mdr_pb_all_extensionalah = ff_q_mce_mdr_all_extensionalahsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_all_extensionalahsf_prefix)) * mdr_pc_all_extensionalah) + (ff_ap_mce_alternating_mdr_all_extensionalahsf_prefix))) /\ ((((exists ff_h_mce_mdr_all_extensionalahsf_prefix_an. ff_h_mce_mdr_all_extensionalahsf_prefix_an + S (ff_an_mce_alternating_mdr_all_extensionalahsf_prefix) = S ((S (ff_index_mce_alternating_mdr_all_extensionalahsf_prefix)) * mdr_nc_all_extensionalah)) /\ exists ff_q_mce_mdr_all_extensionalahsf_prefix_an. mdr_nb_all_extensionalah = ff_q_mce_mdr_all_extensionalahsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_all_extensionalahsf_prefix)) * mdr_nc_all_extensionalah) + (ff_an_mce_alternating_mdr_all_extensionalahsf_prefix))) /\ ((((exists ff_h_mce_mdr_all_extensionalahsf_prefix_bp. ff_h_mce_mdr_all_extensionalahsf_prefix_bp + S (ff_bp_mce_alternating_mdr_all_extensionalahsf_prefix) = S ((S (ff_index_mce_alternating_mdr_all_extensionalahsf_prefix)) * mdr_ec_all_extensionalahs)) /\ exists ff_q_mce_mdr_all_extensionalahsf_prefix_bp. mdr_eb_all_extensionalahs = ff_q_mce_mdr_all_extensionalahsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_all_extensionalahsf_prefix)) * mdr_ec_all_extensionalahs) + (ff_bp_mce_alternating_mdr_all_extensionalahsf_prefix))) /\ ((((exists ff_h_mce_mdr_all_extensionalahsf_prefix_bn. ff_h_mce_mdr_all_extensionalahsf_prefix_bn + S (ff_bn_mce_alternating_mdr_all_extensionalahsf_prefix) = S ((S (ff_index_mce_alternating_mdr_all_extensionalahsf_prefix)) * mdr_fc_all_extensionalahs)) /\ exists ff_q_mce_mdr_all_extensionalahsf_prefix_bn. mdr_fb_all_extensionalahs = ff_q_mce_mdr_all_extensionalahsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_all_extensionalahsf_prefix)) * mdr_fc_all_extensionalahs) + (ff_bn_mce_alternating_mdr_all_extensionalahsf_prefix))) /\ ((((exists ff_h_mce_mdr_all_extensionalahsf_prefix_positive. ff_h_mce_mdr_all_extensionalahsf_prefix_positive + S (ff_p_mce_alternating_mdr_all_extensionalahsf_prefix) = S ((S (ff_index_mce_alternating_mdr_all_extensionalahsf_prefix)) * ff_uc_mce_fold_mdr_all_extensionalahsf)) /\ exists ff_q_mce_mdr_all_extensionalahsf_prefix_positive. ff_ub_mce_fold_mdr_all_extensionalahsf = ff_q_mce_mdr_all_extensionalahsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_all_extensionalahsf_prefix)) * ff_uc_mce_fold_mdr_all_extensionalahsf) + (ff_p_mce_alternating_mdr_all_extensionalahsf_prefix))) /\ ((((exists ff_h_mce_mdr_all_extensionalahsf_prefix_negative. ff_h_mce_mdr_all_extensionalahsf_prefix_negative + S (ff_n_mce_alternating_mdr_all_extensionalahsf_prefix) = S ((S (ff_index_mce_alternating_mdr_all_extensionalahsf_prefix)) * ff_vc_mce_fold_mdr_all_extensionalahsf)) /\ exists ff_q_mce_mdr_all_extensionalahsf_prefix_negative. ff_vb_mce_fold_mdr_all_extensionalahsf = ff_q_mce_mdr_all_extensionalahsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_all_extensionalahsf_prefix)) * ff_vc_mce_fold_mdr_all_extensionalahsf) + (ff_n_mce_alternating_mdr_all_extensionalahsf_prefix))) /\ (((exists ff_even_mce_term_mdr_all_extensionalahsf_prefix_term. ff_index_mce_alternating_mdr_all_extensionalahsf_prefix = 2 * ff_even_mce_term_mdr_all_extensionalahsf_prefix_term) /\ (ff_p_mce_alternating_mdr_all_extensionalahsf_prefix = (ff_ap_mce_alternating_mdr_all_extensionalahsf_prefix) * (ff_bp_mce_alternating_mdr_all_extensionalahsf_prefix) + (ff_an_mce_alternating_mdr_all_extensionalahsf_prefix) * (ff_bn_mce_alternating_mdr_all_extensionalahsf_prefix) /\ ff_n_mce_alternating_mdr_all_extensionalahsf_prefix = (ff_ap_mce_alternating_mdr_all_extensionalahsf_prefix) * (ff_bn_mce_alternating_mdr_all_extensionalahsf_prefix) + (ff_an_mce_alternating_mdr_all_extensionalahsf_prefix) * (ff_bp_mce_alternating_mdr_all_extensionalahsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_all_extensionalahsf_prefix_term. ff_index_mce_alternating_mdr_all_extensionalahsf_prefix = 2 * ff_odd_mce_term_mdr_all_extensionalahsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_all_extensionalahsf_prefix = (ff_ap_mce_alternating_mdr_all_extensionalahsf_prefix) * (ff_bn_mce_alternating_mdr_all_extensionalahsf_prefix) + (ff_an_mce_alternating_mdr_all_extensionalahsf_prefix) * (ff_bp_mce_alternating_mdr_all_extensionalahsf_prefix) /\ ff_n_mce_alternating_mdr_all_extensionalahsf_prefix = (ff_ap_mce_alternating_mdr_all_extensionalahsf_prefix) * (ff_bp_mce_alternating_mdr_all_extensionalahsf_prefix) + (ff_an_mce_alternating_mdr_all_extensionalahsf_prefix) * (ff_bn_mce_alternating_mdr_all_extensionalahsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_all_extensionalahsf_positive ff_v_mce_mdr_all_extensionalahsf_positive. ((((exists ff_h_mce_mdr_all_extensionalahsf_positive_start. ff_h_mce_mdr_all_extensionalahsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_all_extensionalahsf_positive)) /\ exists ff_q_mce_mdr_all_extensionalahsf_positive_start. ff_u_mce_mdr_all_extensionalahsf_positive = ff_q_mce_mdr_all_extensionalahsf_positive_start * S ((S (0)) * ff_v_mce_mdr_all_extensionalahsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_all_extensionalahsf_positive_terminal. ff_h_mce_mdr_all_extensionalahsf_positive_terminal + S (mdr_p_all_extensionalah) = S ((S ((S (mdr_q_all_extensionalahs)))) * ff_v_mce_mdr_all_extensionalahsf_positive)) /\ exists ff_q_mce_mdr_all_extensionalahsf_positive_terminal. ff_u_mce_mdr_all_extensionalahsf_positive = ff_q_mce_mdr_all_extensionalahsf_positive_terminal * S ((S ((S (mdr_q_all_extensionalahs)))) * ff_v_mce_mdr_all_extensionalahsf_positive) + (mdr_p_all_extensionalah))) /\ forall ff_i_mce_mdr_all_extensionalahsf_positive. (exists ff_lt_mce_mdr_all_extensionalahsf_positive_bound. ff_lt_mce_mdr_all_extensionalahsf_positive_bound + S ff_i_mce_mdr_all_extensionalahsf_positive = (S (mdr_q_all_extensionalahs))) -> exists ff_a_mce_mdr_all_extensionalahsf_positive ff_r_mce_mdr_all_extensionalahsf_positive ff_s_mce_mdr_all_extensionalahsf_positive. ((((exists ff_h_mce_mdr_all_extensionalahsf_positive_summand. ff_h_mce_mdr_all_extensionalahsf_positive_summand + S (ff_a_mce_mdr_all_extensionalahsf_positive) = S ((S (ff_i_mce_mdr_all_extensionalahsf_positive)) * ff_uc_mce_fold_mdr_all_extensionalahsf)) /\ exists ff_q_mce_mdr_all_extensionalahsf_positive_summand. ff_ub_mce_fold_mdr_all_extensionalahsf = ff_q_mce_mdr_all_extensionalahsf_positive_summand * S ((S (ff_i_mce_mdr_all_extensionalahsf_positive)) * ff_uc_mce_fold_mdr_all_extensionalahsf) + (ff_a_mce_mdr_all_extensionalahsf_positive))) /\ ((((exists ff_h_mce_mdr_all_extensionalahsf_positive_partial. ff_h_mce_mdr_all_extensionalahsf_positive_partial + S (ff_r_mce_mdr_all_extensionalahsf_positive) = S ((S (ff_i_mce_mdr_all_extensionalahsf_positive)) * ff_v_mce_mdr_all_extensionalahsf_positive)) /\ exists ff_q_mce_mdr_all_extensionalahsf_positive_partial. ff_u_mce_mdr_all_extensionalahsf_positive = ff_q_mce_mdr_all_extensionalahsf_positive_partial * S ((S (ff_i_mce_mdr_all_extensionalahsf_positive)) * ff_v_mce_mdr_all_extensionalahsf_positive) + (ff_r_mce_mdr_all_extensionalahsf_positive))) /\ ((((exists ff_h_mce_mdr_all_extensionalahsf_positive_successor. ff_h_mce_mdr_all_extensionalahsf_positive_successor + S (ff_s_mce_mdr_all_extensionalahsf_positive) = S ((S (S ff_i_mce_mdr_all_extensionalahsf_positive)) * ff_v_mce_mdr_all_extensionalahsf_positive)) /\ exists ff_q_mce_mdr_all_extensionalahsf_positive_successor. ff_u_mce_mdr_all_extensionalahsf_positive = ff_q_mce_mdr_all_extensionalahsf_positive_successor * S ((S (S ff_i_mce_mdr_all_extensionalahsf_positive)) * ff_v_mce_mdr_all_extensionalahsf_positive) + (ff_s_mce_mdr_all_extensionalahsf_positive))) /\ ff_s_mce_mdr_all_extensionalahsf_positive = ff_r_mce_mdr_all_extensionalahsf_positive + ff_a_mce_mdr_all_extensionalahsf_positive)))))) /\ (exists ff_u_mce_mdr_all_extensionalahsf_negative ff_v_mce_mdr_all_extensionalahsf_negative. ((((exists ff_h_mce_mdr_all_extensionalahsf_negative_start. ff_h_mce_mdr_all_extensionalahsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_all_extensionalahsf_negative)) /\ exists ff_q_mce_mdr_all_extensionalahsf_negative_start. ff_u_mce_mdr_all_extensionalahsf_negative = ff_q_mce_mdr_all_extensionalahsf_negative_start * S ((S (0)) * ff_v_mce_mdr_all_extensionalahsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_all_extensionalahsf_negative_terminal. ff_h_mce_mdr_all_extensionalahsf_negative_terminal + S (mdr_n_all_extensionalah) = S ((S ((S (mdr_q_all_extensionalahs)))) * ff_v_mce_mdr_all_extensionalahsf_negative)) /\ exists ff_q_mce_mdr_all_extensionalahsf_negative_terminal. ff_u_mce_mdr_all_extensionalahsf_negative = ff_q_mce_mdr_all_extensionalahsf_negative_terminal * S ((S ((S (mdr_q_all_extensionalahs)))) * ff_v_mce_mdr_all_extensionalahsf_negative) + (mdr_n_all_extensionalah))) /\ forall ff_i_mce_mdr_all_extensionalahsf_negative. (exists ff_lt_mce_mdr_all_extensionalahsf_negative_bound. ff_lt_mce_mdr_all_extensionalahsf_negative_bound + S ff_i_mce_mdr_all_extensionalahsf_negative = (S (mdr_q_all_extensionalahs))) -> exists ff_a_mce_mdr_all_extensionalahsf_negative ff_r_mce_mdr_all_extensionalahsf_negative ff_s_mce_mdr_all_extensionalahsf_negative. ((((exists ff_h_mce_mdr_all_extensionalahsf_negative_summand. ff_h_mce_mdr_all_extensionalahsf_negative_summand + S (ff_a_mce_mdr_all_extensionalahsf_negative) = S ((S (ff_i_mce_mdr_all_extensionalahsf_negative)) * ff_vc_mce_fold_mdr_all_extensionalahsf)) /\ exists ff_q_mce_mdr_all_extensionalahsf_negative_summand. ff_vb_mce_fold_mdr_all_extensionalahsf = ff_q_mce_mdr_all_extensionalahsf_negative_summand * S ((S (ff_i_mce_mdr_all_extensionalahsf_negative)) * ff_vc_mce_fold_mdr_all_extensionalahsf) + (ff_a_mce_mdr_all_extensionalahsf_negative))) /\ ((((exists ff_h_mce_mdr_all_extensionalahsf_negative_partial. ff_h_mce_mdr_all_extensionalahsf_negative_partial + S (ff_r_mce_mdr_all_extensionalahsf_negative) = S ((S (ff_i_mce_mdr_all_extensionalahsf_negative)) * ff_v_mce_mdr_all_extensionalahsf_negative)) /\ exists ff_q_mce_mdr_all_extensionalahsf_negative_partial. ff_u_mce_mdr_all_extensionalahsf_negative = ff_q_mce_mdr_all_extensionalahsf_negative_partial * S ((S (ff_i_mce_mdr_all_extensionalahsf_negative)) * ff_v_mce_mdr_all_extensionalahsf_negative) + (ff_r_mce_mdr_all_extensionalahsf_negative))) /\ ((((exists ff_h_mce_mdr_all_extensionalahsf_negative_successor. ff_h_mce_mdr_all_extensionalahsf_negative_successor + S (ff_s_mce_mdr_all_extensionalahsf_negative) = S ((S (S ff_i_mce_mdr_all_extensionalahsf_negative)) * ff_v_mce_mdr_all_extensionalahsf_negative)) /\ exists ff_q_mce_mdr_all_extensionalahsf_negative_successor. ff_u_mce_mdr_all_extensionalahsf_negative = ff_q_mce_mdr_all_extensionalahsf_negative_successor * S ((S (S ff_i_mce_mdr_all_extensionalahsf_negative)) * ff_v_mce_mdr_all_extensionalahsf_negative) + (ff_s_mce_mdr_all_extensionalahsf_negative))) /\ ff_s_mce_mdr_all_extensionalahsf_negative = ff_r_mce_mdr_all_extensionalahsf_negative + ff_a_mce_mdr_all_extensionalahsf_negative))))))))))))))) /\ ((exists mdr_gap_all_extensionalai. mdr_gap_all_extensionalai + S (mdr_i_all_extensionala) = (mdr_l_all_extensionala)) /\ (exists mdr_z_all_extensionalar. ((exists mdr_a_all_extensionalarc mdr_b_all_extensionalarc mdr_c_all_extensionalarc mdr_e_all_extensionalarc mdr_f_all_extensionalarc. ((mdr_a_all_extensionalarc = ((d) + (mdr_pb_all_extensional)) * S ((d) + (mdr_pb_all_extensional)) + ((mdr_pb_all_extensional) + (mdr_pb_all_extensional))) /\ ((mdr_b_all_extensionalarc = ((mdr_pc_all_extensional) + (mdr_nb_all_extensional)) * S ((mdr_pc_all_extensional) + (mdr_nb_all_extensional)) + ((mdr_nb_all_extensional) + (mdr_nb_all_extensional))) /\ ((mdr_c_all_extensionalarc = ((mdr_a_all_extensionalarc) + (mdr_b_all_extensionalarc)) * S ((mdr_a_all_extensionalarc) + (mdr_b_all_extensionalarc)) + ((mdr_b_all_extensionalarc) + (mdr_b_all_extensionalarc))) /\ ((mdr_e_all_extensionalarc = ((mdr_p_all_extensional) + (mdr_n_all_extensional)) * S ((mdr_p_all_extensional) + (mdr_n_all_extensional)) + ((mdr_n_all_extensional) + (mdr_n_all_extensional))) /\ ((mdr_f_all_extensionalarc = ((mdr_nc_all_extensional) + (mdr_e_all_extensionalarc)) * S ((mdr_nc_all_extensional) + (mdr_e_all_extensionalarc)) + ((mdr_e_all_extensionalarc) + (mdr_e_all_extensionalarc))) /\ ((mdr_z_all_extensionalar) = ((mdr_c_all_extensionalarc) + (mdr_f_all_extensionalarc)) * S ((mdr_c_all_extensionalarc) + (mdr_f_all_extensionalarc)) + ((mdr_f_all_extensionalarc) + (mdr_f_all_extensionalarc))))))))) /\ (((exists ff_h_mdr_all_extensionalarb. ff_h_mdr_all_extensionalarb + S (mdr_z_all_extensionalar) = S ((S (mdr_i_all_extensionala)) * mdr_c_all_extensionala)) /\ exists ff_q_mdr_all_extensionalarb. mdr_b_all_extensionala = ff_q_mdr_all_extensionalarb * S ((S (mdr_i_all_extensionala)) * mdr_c_all_extensionala) + (mdr_z_all_extensionalar)))))))) -> (exists mdr_b_all_extensionalb mdr_c_all_extensionalb mdr_l_all_extensionalb mdr_i_all_extensionalb. ((forall mdr_i_all_extensionalbh. (exists mdr_gap_all_extensionalbhi. mdr_gap_all_extensionalbhi + S (mdr_i_all_extensionalbh) = (mdr_l_all_extensionalb)) -> exists mdr_d_all_extensionalbh mdr_pb_all_extensionalbh mdr_pc_all_extensionalbh mdr_nb_all_extensionalbh mdr_nc_all_extensionalbh mdr_p_all_extensionalbh mdr_n_all_extensionalbh. ((exists mdr_z_all_extensionalbhr. ((exists mdr_a_all_extensionalbhrc mdr_b_all_extensionalbhrc mdr_c_all_extensionalbhrc mdr_e_all_extensionalbhrc mdr_f_all_extensionalbhrc. ((mdr_a_all_extensionalbhrc = ((mdr_d_all_extensionalbh) + (mdr_pb_all_extensionalbh)) * S ((mdr_d_all_extensionalbh) + (mdr_pb_all_extensionalbh)) + ((mdr_pb_all_extensionalbh) + (mdr_pb_all_extensionalbh))) /\ ((mdr_b_all_extensionalbhrc = ((mdr_pc_all_extensionalbh) + (mdr_nb_all_extensionalbh)) * S ((mdr_pc_all_extensionalbh) + (mdr_nb_all_extensionalbh)) + ((mdr_nb_all_extensionalbh) + (mdr_nb_all_extensionalbh))) /\ ((mdr_c_all_extensionalbhrc = ((mdr_a_all_extensionalbhrc) + (mdr_b_all_extensionalbhrc)) * S ((mdr_a_all_extensionalbhrc) + (mdr_b_all_extensionalbhrc)) + ((mdr_b_all_extensionalbhrc) + (mdr_b_all_extensionalbhrc))) /\ ((mdr_e_all_extensionalbhrc = ((mdr_p_all_extensionalbh) + (mdr_n_all_extensionalbh)) * S ((mdr_p_all_extensionalbh) + (mdr_n_all_extensionalbh)) + ((mdr_n_all_extensionalbh) + (mdr_n_all_extensionalbh))) /\ ((mdr_f_all_extensionalbhrc = ((mdr_nc_all_extensionalbh) + (mdr_e_all_extensionalbhrc)) * S ((mdr_nc_all_extensionalbh) + (mdr_e_all_extensionalbhrc)) + ((mdr_e_all_extensionalbhrc) + (mdr_e_all_extensionalbhrc))) /\ ((mdr_z_all_extensionalbhr) = ((mdr_c_all_extensionalbhrc) + (mdr_f_all_extensionalbhrc)) * S ((mdr_c_all_extensionalbhrc) + (mdr_f_all_extensionalbhrc)) + ((mdr_f_all_extensionalbhrc) + (mdr_f_all_extensionalbhrc))))))))) /\ (((exists ff_h_mdr_all_extensionalbhrb. ff_h_mdr_all_extensionalbhrb + S (mdr_z_all_extensionalbhr) = S ((S (mdr_i_all_extensionalbh)) * mdr_c_all_extensionalb)) /\ exists ff_q_mdr_all_extensionalbhrb. mdr_b_all_extensionalb = ff_q_mdr_all_extensionalbhrb * S ((S (mdr_i_all_extensionalbh)) * mdr_c_all_extensionalb) + (mdr_z_all_extensionalbhr))))) /\ (((((mdr_d_all_extensionalbh) = 0) /\ (((mdr_p_all_extensionalbh) = 1) /\ ((mdr_n_all_extensionalbh) = 0))) \/ exists mdr_q_all_extensionalbhs mdr_eb_all_extensionalbhs mdr_ec_all_extensionalbhs mdr_fb_all_extensionalbhs mdr_fc_all_extensionalbhs. (((mdr_d_all_extensionalbh) = S (mdr_q_all_extensionalbhs)) /\ ((forall mdr_j_all_extensionalbhsc. (exists mdr_gap_all_extensionalbhscj. mdr_gap_all_extensionalbhscj + S (mdr_j_all_extensionalbhsc) = (S (mdr_q_all_extensionalbhs))) -> exists mdr_i_all_extensionalbhsc mdr_up_all_extensionalbhsc mdr_us_all_extensionalbhsc mdr_un_all_extensionalbhsc mdr_ut_all_extensionalbhsc mdr_p_all_extensionalbhsc mdr_n_all_extensionalbhsc. ((exists mdr_gap_all_extensionalbhsci. mdr_gap_all_extensionalbhsci + S (mdr_i_all_extensionalbhsc) = (mdr_i_all_extensionalbh)) /\ ((exists mdr_z_all_extensionalbhscr. ((exists mdr_a_all_extensionalbhscrc mdr_b_all_extensionalbhscrc mdr_c_all_extensionalbhscrc mdr_e_all_extensionalbhscrc mdr_f_all_extensionalbhscrc. ((mdr_a_all_extensionalbhscrc = ((mdr_q_all_extensionalbhs) + (mdr_up_all_extensionalbhsc)) * S ((mdr_q_all_extensionalbhs) + (mdr_up_all_extensionalbhsc)) + ((mdr_up_all_extensionalbhsc) + (mdr_up_all_extensionalbhsc))) /\ ((mdr_b_all_extensionalbhscrc = ((mdr_us_all_extensionalbhsc) + (mdr_un_all_extensionalbhsc)) * S ((mdr_us_all_extensionalbhsc) + (mdr_un_all_extensionalbhsc)) + ((mdr_un_all_extensionalbhsc) + (mdr_un_all_extensionalbhsc))) /\ ((mdr_c_all_extensionalbhscrc = ((mdr_a_all_extensionalbhscrc) + (mdr_b_all_extensionalbhscrc)) * S ((mdr_a_all_extensionalbhscrc) + (mdr_b_all_extensionalbhscrc)) + ((mdr_b_all_extensionalbhscrc) + (mdr_b_all_extensionalbhscrc))) /\ ((mdr_e_all_extensionalbhscrc = ((mdr_p_all_extensionalbhsc) + (mdr_n_all_extensionalbhsc)) * S ((mdr_p_all_extensionalbhsc) + (mdr_n_all_extensionalbhsc)) + ((mdr_n_all_extensionalbhsc) + (mdr_n_all_extensionalbhsc))) /\ ((mdr_f_all_extensionalbhscrc = ((mdr_ut_all_extensionalbhsc) + (mdr_e_all_extensionalbhscrc)) * S ((mdr_ut_all_extensionalbhsc) + (mdr_e_all_extensionalbhscrc)) + ((mdr_e_all_extensionalbhscrc) + (mdr_e_all_extensionalbhscrc))) /\ ((mdr_z_all_extensionalbhscr) = ((mdr_c_all_extensionalbhscrc) + (mdr_f_all_extensionalbhscrc)) * S ((mdr_c_all_extensionalbhscrc) + (mdr_f_all_extensionalbhscrc)) + ((mdr_f_all_extensionalbhscrc) + (mdr_f_all_extensionalbhscrc))))))))) /\ (((exists ff_h_mdr_all_extensionalbhscrb. ff_h_mdr_all_extensionalbhscrb + S (mdr_z_all_extensionalbhscr) = S ((S (mdr_i_all_extensionalbhsc)) * mdr_c_all_extensionalb)) /\ exists ff_q_mdr_all_extensionalbhscrb. mdr_b_all_extensionalb = ff_q_mdr_all_extensionalbhscrb * S ((S (mdr_i_all_extensionalbhsc)) * mdr_c_all_extensionalb) + (mdr_z_all_extensionalbhscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_all_extensionalbhscm_positive. (exists ff_gap_mdm_lt_mdr_all_extensionalbhscm_positive_index_bound. ff_gap_mdm_lt_mdr_all_extensionalbhscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_all_extensionalbhscm_positive) = ((mdr_q_all_extensionalbhs) * (mdr_q_all_extensionalbhs))) -> exists ff_row_mdm_prefix_mdr_all_extensionalbhscm_positive ff_column_mdm_prefix_mdr_all_extensionalbhscm_positive ff_value_mdm_prefix_mdr_all_extensionalbhscm_positive. (ff_index_mdm_prefix_mdr_all_extensionalbhscm_positive = (mdr_q_all_extensionalbhs) * ff_row_mdm_prefix_mdr_all_extensionalbhscm_positive + ff_column_mdm_prefix_mdr_all_extensionalbhscm_positive /\ ((exists ff_gap_mdm_lt_mdr_all_extensionalbhscm_positive_column_bound. ff_gap_mdm_lt_mdr_all_extensionalbhscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_all_extensionalbhscm_positive) = (mdr_q_all_extensionalbhs)) /\ ((exists ff_row_mdm_cell_mdr_all_extensionalbhscm_positive_cell ff_column_mdm_cell_mdr_all_extensionalbhscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_all_extensionalbhscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_all_extensionalbhscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_all_extensionalbhscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_all_extensionalbhscm_positive_cell = ff_row_mdm_prefix_mdr_all_extensionalbhscm_positive) \/ ((exists ff_gap_mdm_le_mdr_all_extensionalbhscm_positive_cell_row_after. ff_gap_mdm_le_mdr_all_extensionalbhscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_all_extensionalbhscm_positive)) /\ ff_row_mdm_cell_mdr_all_extensionalbhscm_positive_cell = S ff_row_mdm_prefix_mdr_all_extensionalbhscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_all_extensionalbhscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_all_extensionalbhscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_all_extensionalbhscm_positive) = (mdr_j_all_extensionalbhsc)) /\ ff_column_mdm_cell_mdr_all_extensionalbhscm_positive_cell = ff_column_mdm_prefix_mdr_all_extensionalbhscm_positive) \/ ((exists ff_gap_mdm_le_mdr_all_extensionalbhscm_positive_cell_column_after. ff_gap_mdm_le_mdr_all_extensionalbhscm_positive_cell_column_after + (mdr_j_all_extensionalbhsc) = (ff_column_mdm_prefix_mdr_all_extensionalbhscm_positive)) /\ ff_column_mdm_cell_mdr_all_extensionalbhscm_positive_cell = S ff_column_mdm_prefix_mdr_all_extensionalbhscm_positive))) /\ (((exists ff_h_mdm_mdr_all_extensionalbhscm_positive_cell_source. ff_h_mdm_mdr_all_extensionalbhscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_all_extensionalbhscm_positive) = S ((S ((ff_row_mdm_cell_mdr_all_extensionalbhscm_positive_cell) * (S (mdr_q_all_extensionalbhs)) + (ff_column_mdm_cell_mdr_all_extensionalbhscm_positive_cell))) * mdr_pc_all_extensionalbh)) /\ exists ff_q_mdm_mdr_all_extensionalbhscm_positive_cell_source. mdr_pb_all_extensionalbh = ff_q_mdm_mdr_all_extensionalbhscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_all_extensionalbhscm_positive_cell) * (S (mdr_q_all_extensionalbhs)) + (ff_column_mdm_cell_mdr_all_extensionalbhscm_positive_cell))) * mdr_pc_all_extensionalbh) + (ff_value_mdm_prefix_mdr_all_extensionalbhscm_positive)))))) /\ (((exists ff_h_mdm_mdr_all_extensionalbhscm_positive_target. ff_h_mdm_mdr_all_extensionalbhscm_positive_target + S (ff_value_mdm_prefix_mdr_all_extensionalbhscm_positive) = S ((S (ff_index_mdm_prefix_mdr_all_extensionalbhscm_positive)) * mdr_us_all_extensionalbhsc)) /\ exists ff_q_mdm_mdr_all_extensionalbhscm_positive_target. mdr_up_all_extensionalbhsc = ff_q_mdm_mdr_all_extensionalbhscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_all_extensionalbhscm_positive)) * mdr_us_all_extensionalbhsc) + (ff_value_mdm_prefix_mdr_all_extensionalbhscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_all_extensionalbhscm_negative. (exists ff_gap_mdm_lt_mdr_all_extensionalbhscm_negative_index_bound. ff_gap_mdm_lt_mdr_all_extensionalbhscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_all_extensionalbhscm_negative) = ((mdr_q_all_extensionalbhs) * (mdr_q_all_extensionalbhs))) -> exists ff_row_mdm_prefix_mdr_all_extensionalbhscm_negative ff_column_mdm_prefix_mdr_all_extensionalbhscm_negative ff_value_mdm_prefix_mdr_all_extensionalbhscm_negative. (ff_index_mdm_prefix_mdr_all_extensionalbhscm_negative = (mdr_q_all_extensionalbhs) * ff_row_mdm_prefix_mdr_all_extensionalbhscm_negative + ff_column_mdm_prefix_mdr_all_extensionalbhscm_negative /\ ((exists ff_gap_mdm_lt_mdr_all_extensionalbhscm_negative_column_bound. ff_gap_mdm_lt_mdr_all_extensionalbhscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_all_extensionalbhscm_negative) = (mdr_q_all_extensionalbhs)) /\ ((exists ff_row_mdm_cell_mdr_all_extensionalbhscm_negative_cell ff_column_mdm_cell_mdr_all_extensionalbhscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_all_extensionalbhscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_all_extensionalbhscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_all_extensionalbhscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_all_extensionalbhscm_negative_cell = ff_row_mdm_prefix_mdr_all_extensionalbhscm_negative) \/ ((exists ff_gap_mdm_le_mdr_all_extensionalbhscm_negative_cell_row_after. ff_gap_mdm_le_mdr_all_extensionalbhscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_all_extensionalbhscm_negative)) /\ ff_row_mdm_cell_mdr_all_extensionalbhscm_negative_cell = S ff_row_mdm_prefix_mdr_all_extensionalbhscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_all_extensionalbhscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_all_extensionalbhscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_all_extensionalbhscm_negative) = (mdr_j_all_extensionalbhsc)) /\ ff_column_mdm_cell_mdr_all_extensionalbhscm_negative_cell = ff_column_mdm_prefix_mdr_all_extensionalbhscm_negative) \/ ((exists ff_gap_mdm_le_mdr_all_extensionalbhscm_negative_cell_column_after. ff_gap_mdm_le_mdr_all_extensionalbhscm_negative_cell_column_after + (mdr_j_all_extensionalbhsc) = (ff_column_mdm_prefix_mdr_all_extensionalbhscm_negative)) /\ ff_column_mdm_cell_mdr_all_extensionalbhscm_negative_cell = S ff_column_mdm_prefix_mdr_all_extensionalbhscm_negative))) /\ (((exists ff_h_mdm_mdr_all_extensionalbhscm_negative_cell_source. ff_h_mdm_mdr_all_extensionalbhscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_all_extensionalbhscm_negative) = S ((S ((ff_row_mdm_cell_mdr_all_extensionalbhscm_negative_cell) * (S (mdr_q_all_extensionalbhs)) + (ff_column_mdm_cell_mdr_all_extensionalbhscm_negative_cell))) * mdr_nc_all_extensionalbh)) /\ exists ff_q_mdm_mdr_all_extensionalbhscm_negative_cell_source. mdr_nb_all_extensionalbh = ff_q_mdm_mdr_all_extensionalbhscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_all_extensionalbhscm_negative_cell) * (S (mdr_q_all_extensionalbhs)) + (ff_column_mdm_cell_mdr_all_extensionalbhscm_negative_cell))) * mdr_nc_all_extensionalbh) + (ff_value_mdm_prefix_mdr_all_extensionalbhscm_negative)))))) /\ (((exists ff_h_mdm_mdr_all_extensionalbhscm_negative_target. ff_h_mdm_mdr_all_extensionalbhscm_negative_target + S (ff_value_mdm_prefix_mdr_all_extensionalbhscm_negative) = S ((S (ff_index_mdm_prefix_mdr_all_extensionalbhscm_negative)) * mdr_ut_all_extensionalbhsc)) /\ exists ff_q_mdm_mdr_all_extensionalbhscm_negative_target. mdr_un_all_extensionalbhsc = ff_q_mdm_mdr_all_extensionalbhscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_all_extensionalbhscm_negative)) * mdr_ut_all_extensionalbhsc) + (ff_value_mdm_prefix_mdr_all_extensionalbhscm_negative))))))))) /\ ((((exists ff_h_mdr_all_extensionalbhscp. ff_h_mdr_all_extensionalbhscp + S (mdr_p_all_extensionalbhsc) = S ((S (mdr_j_all_extensionalbhsc)) * mdr_ec_all_extensionalbhs)) /\ exists ff_q_mdr_all_extensionalbhscp. mdr_eb_all_extensionalbhs = ff_q_mdr_all_extensionalbhscp * S ((S (mdr_j_all_extensionalbhsc)) * mdr_ec_all_extensionalbhs) + (mdr_p_all_extensionalbhsc))) /\ (((exists ff_h_mdr_all_extensionalbhscn. ff_h_mdr_all_extensionalbhscn + S (mdr_n_all_extensionalbhsc) = S ((S (mdr_j_all_extensionalbhsc)) * mdr_fc_all_extensionalbhs)) /\ exists ff_q_mdr_all_extensionalbhscn. mdr_fb_all_extensionalbhs = ff_q_mdr_all_extensionalbhscn * S ((S (mdr_j_all_extensionalbhsc)) * mdr_fc_all_extensionalbhs) + (mdr_n_all_extensionalbhsc)))))))) /\ (exists ff_ub_mce_fold_mdr_all_extensionalbhsf ff_uc_mce_fold_mdr_all_extensionalbhsf ff_vb_mce_fold_mdr_all_extensionalbhsf ff_vc_mce_fold_mdr_all_extensionalbhsf. ((forall ff_index_mce_alternating_mdr_all_extensionalbhsf_prefix. (exists ff_gap_mce_mdr_all_extensionalbhsf_prefix_index. ff_gap_mce_mdr_all_extensionalbhsf_prefix_index + S (ff_index_mce_alternating_mdr_all_extensionalbhsf_prefix) = (S (mdr_q_all_extensionalbhs))) -> exists ff_ap_mce_alternating_mdr_all_extensionalbhsf_prefix ff_an_mce_alternating_mdr_all_extensionalbhsf_prefix ff_bp_mce_alternating_mdr_all_extensionalbhsf_prefix ff_bn_mce_alternating_mdr_all_extensionalbhsf_prefix ff_p_mce_alternating_mdr_all_extensionalbhsf_prefix ff_n_mce_alternating_mdr_all_extensionalbhsf_prefix. ((((exists ff_h_mce_mdr_all_extensionalbhsf_prefix_ap. ff_h_mce_mdr_all_extensionalbhsf_prefix_ap + S (ff_ap_mce_alternating_mdr_all_extensionalbhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_all_extensionalbhsf_prefix)) * mdr_pc_all_extensionalbh)) /\ exists ff_q_mce_mdr_all_extensionalbhsf_prefix_ap. mdr_pb_all_extensionalbh = ff_q_mce_mdr_all_extensionalbhsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_all_extensionalbhsf_prefix)) * mdr_pc_all_extensionalbh) + (ff_ap_mce_alternating_mdr_all_extensionalbhsf_prefix))) /\ ((((exists ff_h_mce_mdr_all_extensionalbhsf_prefix_an. ff_h_mce_mdr_all_extensionalbhsf_prefix_an + S (ff_an_mce_alternating_mdr_all_extensionalbhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_all_extensionalbhsf_prefix)) * mdr_nc_all_extensionalbh)) /\ exists ff_q_mce_mdr_all_extensionalbhsf_prefix_an. mdr_nb_all_extensionalbh = ff_q_mce_mdr_all_extensionalbhsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_all_extensionalbhsf_prefix)) * mdr_nc_all_extensionalbh) + (ff_an_mce_alternating_mdr_all_extensionalbhsf_prefix))) /\ ((((exists ff_h_mce_mdr_all_extensionalbhsf_prefix_bp. ff_h_mce_mdr_all_extensionalbhsf_prefix_bp + S (ff_bp_mce_alternating_mdr_all_extensionalbhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_all_extensionalbhsf_prefix)) * mdr_ec_all_extensionalbhs)) /\ exists ff_q_mce_mdr_all_extensionalbhsf_prefix_bp. mdr_eb_all_extensionalbhs = ff_q_mce_mdr_all_extensionalbhsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_all_extensionalbhsf_prefix)) * mdr_ec_all_extensionalbhs) + (ff_bp_mce_alternating_mdr_all_extensionalbhsf_prefix))) /\ ((((exists ff_h_mce_mdr_all_extensionalbhsf_prefix_bn. ff_h_mce_mdr_all_extensionalbhsf_prefix_bn + S (ff_bn_mce_alternating_mdr_all_extensionalbhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_all_extensionalbhsf_prefix)) * mdr_fc_all_extensionalbhs)) /\ exists ff_q_mce_mdr_all_extensionalbhsf_prefix_bn. mdr_fb_all_extensionalbhs = ff_q_mce_mdr_all_extensionalbhsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_all_extensionalbhsf_prefix)) * mdr_fc_all_extensionalbhs) + (ff_bn_mce_alternating_mdr_all_extensionalbhsf_prefix))) /\ ((((exists ff_h_mce_mdr_all_extensionalbhsf_prefix_positive. ff_h_mce_mdr_all_extensionalbhsf_prefix_positive + S (ff_p_mce_alternating_mdr_all_extensionalbhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_all_extensionalbhsf_prefix)) * ff_uc_mce_fold_mdr_all_extensionalbhsf)) /\ exists ff_q_mce_mdr_all_extensionalbhsf_prefix_positive. ff_ub_mce_fold_mdr_all_extensionalbhsf = ff_q_mce_mdr_all_extensionalbhsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_all_extensionalbhsf_prefix)) * ff_uc_mce_fold_mdr_all_extensionalbhsf) + (ff_p_mce_alternating_mdr_all_extensionalbhsf_prefix))) /\ ((((exists ff_h_mce_mdr_all_extensionalbhsf_prefix_negative. ff_h_mce_mdr_all_extensionalbhsf_prefix_negative + S (ff_n_mce_alternating_mdr_all_extensionalbhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_all_extensionalbhsf_prefix)) * ff_vc_mce_fold_mdr_all_extensionalbhsf)) /\ exists ff_q_mce_mdr_all_extensionalbhsf_prefix_negative. ff_vb_mce_fold_mdr_all_extensionalbhsf = ff_q_mce_mdr_all_extensionalbhsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_all_extensionalbhsf_prefix)) * ff_vc_mce_fold_mdr_all_extensionalbhsf) + (ff_n_mce_alternating_mdr_all_extensionalbhsf_prefix))) /\ (((exists ff_even_mce_term_mdr_all_extensionalbhsf_prefix_term. ff_index_mce_alternating_mdr_all_extensionalbhsf_prefix = 2 * ff_even_mce_term_mdr_all_extensionalbhsf_prefix_term) /\ (ff_p_mce_alternating_mdr_all_extensionalbhsf_prefix = (ff_ap_mce_alternating_mdr_all_extensionalbhsf_prefix) * (ff_bp_mce_alternating_mdr_all_extensionalbhsf_prefix) + (ff_an_mce_alternating_mdr_all_extensionalbhsf_prefix) * (ff_bn_mce_alternating_mdr_all_extensionalbhsf_prefix) /\ ff_n_mce_alternating_mdr_all_extensionalbhsf_prefix = (ff_ap_mce_alternating_mdr_all_extensionalbhsf_prefix) * (ff_bn_mce_alternating_mdr_all_extensionalbhsf_prefix) + (ff_an_mce_alternating_mdr_all_extensionalbhsf_prefix) * (ff_bp_mce_alternating_mdr_all_extensionalbhsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_all_extensionalbhsf_prefix_term. ff_index_mce_alternating_mdr_all_extensionalbhsf_prefix = 2 * ff_odd_mce_term_mdr_all_extensionalbhsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_all_extensionalbhsf_prefix = (ff_ap_mce_alternating_mdr_all_extensionalbhsf_prefix) * (ff_bn_mce_alternating_mdr_all_extensionalbhsf_prefix) + (ff_an_mce_alternating_mdr_all_extensionalbhsf_prefix) * (ff_bp_mce_alternating_mdr_all_extensionalbhsf_prefix) /\ ff_n_mce_alternating_mdr_all_extensionalbhsf_prefix = (ff_ap_mce_alternating_mdr_all_extensionalbhsf_prefix) * (ff_bp_mce_alternating_mdr_all_extensionalbhsf_prefix) + (ff_an_mce_alternating_mdr_all_extensionalbhsf_prefix) * (ff_bn_mce_alternating_mdr_all_extensionalbhsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_all_extensionalbhsf_positive ff_v_mce_mdr_all_extensionalbhsf_positive. ((((exists ff_h_mce_mdr_all_extensionalbhsf_positive_start. ff_h_mce_mdr_all_extensionalbhsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_all_extensionalbhsf_positive)) /\ exists ff_q_mce_mdr_all_extensionalbhsf_positive_start. ff_u_mce_mdr_all_extensionalbhsf_positive = ff_q_mce_mdr_all_extensionalbhsf_positive_start * S ((S (0)) * ff_v_mce_mdr_all_extensionalbhsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_all_extensionalbhsf_positive_terminal. ff_h_mce_mdr_all_extensionalbhsf_positive_terminal + S (mdr_p_all_extensionalbh) = S ((S ((S (mdr_q_all_extensionalbhs)))) * ff_v_mce_mdr_all_extensionalbhsf_positive)) /\ exists ff_q_mce_mdr_all_extensionalbhsf_positive_terminal. ff_u_mce_mdr_all_extensionalbhsf_positive = ff_q_mce_mdr_all_extensionalbhsf_positive_terminal * S ((S ((S (mdr_q_all_extensionalbhs)))) * ff_v_mce_mdr_all_extensionalbhsf_positive) + (mdr_p_all_extensionalbh))) /\ forall ff_i_mce_mdr_all_extensionalbhsf_positive. (exists ff_lt_mce_mdr_all_extensionalbhsf_positive_bound. ff_lt_mce_mdr_all_extensionalbhsf_positive_bound + S ff_i_mce_mdr_all_extensionalbhsf_positive = (S (mdr_q_all_extensionalbhs))) -> exists ff_a_mce_mdr_all_extensionalbhsf_positive ff_r_mce_mdr_all_extensionalbhsf_positive ff_s_mce_mdr_all_extensionalbhsf_positive. ((((exists ff_h_mce_mdr_all_extensionalbhsf_positive_summand. ff_h_mce_mdr_all_extensionalbhsf_positive_summand + S (ff_a_mce_mdr_all_extensionalbhsf_positive) = S ((S (ff_i_mce_mdr_all_extensionalbhsf_positive)) * ff_uc_mce_fold_mdr_all_extensionalbhsf)) /\ exists ff_q_mce_mdr_all_extensionalbhsf_positive_summand. ff_ub_mce_fold_mdr_all_extensionalbhsf = ff_q_mce_mdr_all_extensionalbhsf_positive_summand * S ((S (ff_i_mce_mdr_all_extensionalbhsf_positive)) * ff_uc_mce_fold_mdr_all_extensionalbhsf) + (ff_a_mce_mdr_all_extensionalbhsf_positive))) /\ ((((exists ff_h_mce_mdr_all_extensionalbhsf_positive_partial. ff_h_mce_mdr_all_extensionalbhsf_positive_partial + S (ff_r_mce_mdr_all_extensionalbhsf_positive) = S ((S (ff_i_mce_mdr_all_extensionalbhsf_positive)) * ff_v_mce_mdr_all_extensionalbhsf_positive)) /\ exists ff_q_mce_mdr_all_extensionalbhsf_positive_partial. ff_u_mce_mdr_all_extensionalbhsf_positive = ff_q_mce_mdr_all_extensionalbhsf_positive_partial * S ((S (ff_i_mce_mdr_all_extensionalbhsf_positive)) * ff_v_mce_mdr_all_extensionalbhsf_positive) + (ff_r_mce_mdr_all_extensionalbhsf_positive))) /\ ((((exists ff_h_mce_mdr_all_extensionalbhsf_positive_successor. ff_h_mce_mdr_all_extensionalbhsf_positive_successor + S (ff_s_mce_mdr_all_extensionalbhsf_positive) = S ((S (S ff_i_mce_mdr_all_extensionalbhsf_positive)) * ff_v_mce_mdr_all_extensionalbhsf_positive)) /\ exists ff_q_mce_mdr_all_extensionalbhsf_positive_successor. ff_u_mce_mdr_all_extensionalbhsf_positive = ff_q_mce_mdr_all_extensionalbhsf_positive_successor * S ((S (S ff_i_mce_mdr_all_extensionalbhsf_positive)) * ff_v_mce_mdr_all_extensionalbhsf_positive) + (ff_s_mce_mdr_all_extensionalbhsf_positive))) /\ ff_s_mce_mdr_all_extensionalbhsf_positive = ff_r_mce_mdr_all_extensionalbhsf_positive + ff_a_mce_mdr_all_extensionalbhsf_positive)))))) /\ (exists ff_u_mce_mdr_all_extensionalbhsf_negative ff_v_mce_mdr_all_extensionalbhsf_negative. ((((exists ff_h_mce_mdr_all_extensionalbhsf_negative_start. ff_h_mce_mdr_all_extensionalbhsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_all_extensionalbhsf_negative)) /\ exists ff_q_mce_mdr_all_extensionalbhsf_negative_start. ff_u_mce_mdr_all_extensionalbhsf_negative = ff_q_mce_mdr_all_extensionalbhsf_negative_start * S ((S (0)) * ff_v_mce_mdr_all_extensionalbhsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_all_extensionalbhsf_negative_terminal. ff_h_mce_mdr_all_extensionalbhsf_negative_terminal + S (mdr_n_all_extensionalbh) = S ((S ((S (mdr_q_all_extensionalbhs)))) * ff_v_mce_mdr_all_extensionalbhsf_negative)) /\ exists ff_q_mce_mdr_all_extensionalbhsf_negative_terminal. ff_u_mce_mdr_all_extensionalbhsf_negative = ff_q_mce_mdr_all_extensionalbhsf_negative_terminal * S ((S ((S (mdr_q_all_extensionalbhs)))) * ff_v_mce_mdr_all_extensionalbhsf_negative) + (mdr_n_all_extensionalbh))) /\ forall ff_i_mce_mdr_all_extensionalbhsf_negative. (exists ff_lt_mce_mdr_all_extensionalbhsf_negative_bound. ff_lt_mce_mdr_all_extensionalbhsf_negative_bound + S ff_i_mce_mdr_all_extensionalbhsf_negative = (S (mdr_q_all_extensionalbhs))) -> exists ff_a_mce_mdr_all_extensionalbhsf_negative ff_r_mce_mdr_all_extensionalbhsf_negative ff_s_mce_mdr_all_extensionalbhsf_negative. ((((exists ff_h_mce_mdr_all_extensionalbhsf_negative_summand. ff_h_mce_mdr_all_extensionalbhsf_negative_summand + S (ff_a_mce_mdr_all_extensionalbhsf_negative) = S ((S (ff_i_mce_mdr_all_extensionalbhsf_negative)) * ff_vc_mce_fold_mdr_all_extensionalbhsf)) /\ exists ff_q_mce_mdr_all_extensionalbhsf_negative_summand. ff_vb_mce_fold_mdr_all_extensionalbhsf = ff_q_mce_mdr_all_extensionalbhsf_negative_summand * S ((S (ff_i_mce_mdr_all_extensionalbhsf_negative)) * ff_vc_mce_fold_mdr_all_extensionalbhsf) + (ff_a_mce_mdr_all_extensionalbhsf_negative))) /\ ((((exists ff_h_mce_mdr_all_extensionalbhsf_negative_partial. ff_h_mce_mdr_all_extensionalbhsf_negative_partial + S (ff_r_mce_mdr_all_extensionalbhsf_negative) = S ((S (ff_i_mce_mdr_all_extensionalbhsf_negative)) * ff_v_mce_mdr_all_extensionalbhsf_negative)) /\ exists ff_q_mce_mdr_all_extensionalbhsf_negative_partial. ff_u_mce_mdr_all_extensionalbhsf_negative = ff_q_mce_mdr_all_extensionalbhsf_negative_partial * S ((S (ff_i_mce_mdr_all_extensionalbhsf_negative)) * ff_v_mce_mdr_all_extensionalbhsf_negative) + (ff_r_mce_mdr_all_extensionalbhsf_negative))) /\ ((((exists ff_h_mce_mdr_all_extensionalbhsf_negative_successor. ff_h_mce_mdr_all_extensionalbhsf_negative_successor + S (ff_s_mce_mdr_all_extensionalbhsf_negative) = S ((S (S ff_i_mce_mdr_all_extensionalbhsf_negative)) * ff_v_mce_mdr_all_extensionalbhsf_negative)) /\ exists ff_q_mce_mdr_all_extensionalbhsf_negative_successor. ff_u_mce_mdr_all_extensionalbhsf_negative = ff_q_mce_mdr_all_extensionalbhsf_negative_successor * S ((S (S ff_i_mce_mdr_all_extensionalbhsf_negative)) * ff_v_mce_mdr_all_extensionalbhsf_negative) + (ff_s_mce_mdr_all_extensionalbhsf_negative))) /\ ff_s_mce_mdr_all_extensionalbhsf_negative = ff_r_mce_mdr_all_extensionalbhsf_negative + ff_a_mce_mdr_all_extensionalbhsf_negative))))))))))))))) /\ ((exists mdr_gap_all_extensionalbi. mdr_gap_all_extensionalbi + S (mdr_i_all_extensionalb) = (mdr_l_all_extensionalb)) /\ (exists mdr_z_all_extensionalbr. ((exists mdr_a_all_extensionalbrc mdr_b_all_extensionalbrc mdr_c_all_extensionalbrc mdr_e_all_extensionalbrc mdr_f_all_extensionalbrc. ((mdr_a_all_extensionalbrc = ((d) + (mdr_qb_all_extensional)) * S ((d) + (mdr_qb_all_extensional)) + ((mdr_qb_all_extensional) + (mdr_qb_all_extensional))) /\ ((mdr_b_all_extensionalbrc = ((mdr_qc_all_extensional) + (mdr_rb_all_extensional)) * S ((mdr_qc_all_extensional) + (mdr_rb_all_extensional)) + ((mdr_rb_all_extensional) + (mdr_rb_all_extensional))) /\ ((mdr_c_all_extensionalbrc = ((mdr_a_all_extensionalbrc) + (mdr_b_all_extensionalbrc)) * S ((mdr_a_all_extensionalbrc) + (mdr_b_all_extensionalbrc)) + ((mdr_b_all_extensionalbrc) + (mdr_b_all_extensionalbrc))) /\ ((mdr_e_all_extensionalbrc = ((mdr_r_all_extensional) + (mdr_s_all_extensional)) * S ((mdr_r_all_extensional) + (mdr_s_all_extensional)) + ((mdr_s_all_extensional) + (mdr_s_all_extensional))) /\ ((mdr_f_all_extensionalbrc = ((mdr_rc_all_extensional) + (mdr_e_all_extensionalbrc)) * S ((mdr_rc_all_extensional) + (mdr_e_all_extensionalbrc)) + ((mdr_e_all_extensionalbrc) + (mdr_e_all_extensionalbrc))) /\ ((mdr_z_all_extensionalbr) = ((mdr_c_all_extensionalbrc) + (mdr_f_all_extensionalbrc)) * S ((mdr_c_all_extensionalbrc) + (mdr_f_all_extensionalbrc)) + ((mdr_f_all_extensionalbrc) + (mdr_f_all_extensionalbrc))))))))) /\ (((exists ff_h_mdr_all_extensionalbrb. ff_h_mdr_all_extensionalbrb + S (mdr_z_all_extensionalbr) = S ((S (mdr_i_all_extensionalb)) * mdr_c_all_extensionalb)) /\ exists ff_q_mdr_all_extensionalbrb. mdr_b_all_extensionalb = ff_q_mdr_all_extensionalbrb * S ((S (mdr_i_all_extensionalb)) * mdr_c_all_extensionalb) + (mdr_z_all_extensionalbr)))))))) -> mdr_p_all_extensional = mdr_r_all_extensional /\ mdr_n_all_extensional = mdr_s_all_extensional)