signed_recursive_determinant_exists_unique

Exact expanded first-order arithmetic statement

forall pb pc nb nc d. exists p n. ((exists mdr_b_unique_value mdr_c_unique_value mdr_l_unique_value mdr_i_unique_value. ((forall mdr_i_unique_valueh. (exists mdr_gap_unique_valuehi. mdr_gap_unique_valuehi + S (mdr_i_unique_valueh) = (mdr_l_unique_value)) -> exists mdr_d_unique_valueh mdr_pb_unique_valueh mdr_pc_unique_valueh mdr_nb_unique_valueh mdr_nc_unique_valueh mdr_p_unique_valueh mdr_n_unique_valueh. ((exists mdr_z_unique_valuehr. ((exists mdr_a_unique_valuehrc mdr_b_unique_valuehrc mdr_c_unique_valuehrc mdr_e_unique_valuehrc mdr_f_unique_valuehrc. ((mdr_a_unique_valuehrc = ((mdr_d_unique_valueh) + (mdr_pb_unique_valueh)) * S ((mdr_d_unique_valueh) + (mdr_pb_unique_valueh)) + ((mdr_pb_unique_valueh) + (mdr_pb_unique_valueh))) /\ ((mdr_b_unique_valuehrc = ((mdr_pc_unique_valueh) + (mdr_nb_unique_valueh)) * S ((mdr_pc_unique_valueh) + (mdr_nb_unique_valueh)) + ((mdr_nb_unique_valueh) + (mdr_nb_unique_valueh))) /\ ((mdr_c_unique_valuehrc = ((mdr_a_unique_valuehrc) + (mdr_b_unique_valuehrc)) * S ((mdr_a_unique_valuehrc) + (mdr_b_unique_valuehrc)) + ((mdr_b_unique_valuehrc) + (mdr_b_unique_valuehrc))) /\ ((mdr_e_unique_valuehrc = ((mdr_p_unique_valueh) + (mdr_n_unique_valueh)) * S ((mdr_p_unique_valueh) + (mdr_n_unique_valueh)) + ((mdr_n_unique_valueh) + (mdr_n_unique_valueh))) /\ ((mdr_f_unique_valuehrc = ((mdr_nc_unique_valueh) + (mdr_e_unique_valuehrc)) * S ((mdr_nc_unique_valueh) + (mdr_e_unique_valuehrc)) + ((mdr_e_unique_valuehrc) + (mdr_e_unique_valuehrc))) /\ ((mdr_z_unique_valuehr) = ((mdr_c_unique_valuehrc) + (mdr_f_unique_valuehrc)) * S ((mdr_c_unique_valuehrc) + (mdr_f_unique_valuehrc)) + ((mdr_f_unique_valuehrc) + (mdr_f_unique_valuehrc))))))))) /\ (((exists ff_h_mdr_unique_valuehrb. ff_h_mdr_unique_valuehrb + S (mdr_z_unique_valuehr) = S ((S (mdr_i_unique_valueh)) * mdr_c_unique_value)) /\ exists ff_q_mdr_unique_valuehrb. mdr_b_unique_value = ff_q_mdr_unique_valuehrb * S ((S (mdr_i_unique_valueh)) * mdr_c_unique_value) + (mdr_z_unique_valuehr))))) /\ (((((mdr_d_unique_valueh) = 0) /\ (((mdr_p_unique_valueh) = 1) /\ ((mdr_n_unique_valueh) = 0))) \/ exists mdr_q_unique_valuehs mdr_eb_unique_valuehs mdr_ec_unique_valuehs mdr_fb_unique_valuehs mdr_fc_unique_valuehs. (((mdr_d_unique_valueh) = S (mdr_q_unique_valuehs)) /\ ((forall mdr_j_unique_valuehsc. (exists mdr_gap_unique_valuehscj. mdr_gap_unique_valuehscj + S (mdr_j_unique_valuehsc) = (S (mdr_q_unique_valuehs))) -> exists mdr_i_unique_valuehsc mdr_up_unique_valuehsc mdr_us_unique_valuehsc mdr_un_unique_valuehsc mdr_ut_unique_valuehsc mdr_p_unique_valuehsc mdr_n_unique_valuehsc. ((exists mdr_gap_unique_valuehsci. mdr_gap_unique_valuehsci + S (mdr_i_unique_valuehsc) = (mdr_i_unique_valueh)) /\ ((exists mdr_z_unique_valuehscr. ((exists mdr_a_unique_valuehscrc mdr_b_unique_valuehscrc mdr_c_unique_valuehscrc mdr_e_unique_valuehscrc mdr_f_unique_valuehscrc. ((mdr_a_unique_valuehscrc = ((mdr_q_unique_valuehs) + (mdr_up_unique_valuehsc)) * S ((mdr_q_unique_valuehs) + (mdr_up_unique_valuehsc)) + ((mdr_up_unique_valuehsc) + (mdr_up_unique_valuehsc))) /\ ((mdr_b_unique_valuehscrc = ((mdr_us_unique_valuehsc) + (mdr_un_unique_valuehsc)) * S ((mdr_us_unique_valuehsc) + (mdr_un_unique_valuehsc)) + ((mdr_un_unique_valuehsc) + (mdr_un_unique_valuehsc))) /\ ((mdr_c_unique_valuehscrc = ((mdr_a_unique_valuehscrc) + (mdr_b_unique_valuehscrc)) * S ((mdr_a_unique_valuehscrc) + (mdr_b_unique_valuehscrc)) + ((mdr_b_unique_valuehscrc) + (mdr_b_unique_valuehscrc))) /\ ((mdr_e_unique_valuehscrc = ((mdr_p_unique_valuehsc) + (mdr_n_unique_valuehsc)) * S ((mdr_p_unique_valuehsc) + (mdr_n_unique_valuehsc)) + ((mdr_n_unique_valuehsc) + (mdr_n_unique_valuehsc))) /\ ((mdr_f_unique_valuehscrc = ((mdr_ut_unique_valuehsc) + (mdr_e_unique_valuehscrc)) * S ((mdr_ut_unique_valuehsc) + (mdr_e_unique_valuehscrc)) + ((mdr_e_unique_valuehscrc) + (mdr_e_unique_valuehscrc))) /\ ((mdr_z_unique_valuehscr) = ((mdr_c_unique_valuehscrc) + (mdr_f_unique_valuehscrc)) * S ((mdr_c_unique_valuehscrc) + (mdr_f_unique_valuehscrc)) + ((mdr_f_unique_valuehscrc) + (mdr_f_unique_valuehscrc))))))))) /\ (((exists ff_h_mdr_unique_valuehscrb. ff_h_mdr_unique_valuehscrb + S (mdr_z_unique_valuehscr) = S ((S (mdr_i_unique_valuehsc)) * mdr_c_unique_value)) /\ exists ff_q_mdr_unique_valuehscrb. mdr_b_unique_value = ff_q_mdr_unique_valuehscrb * S ((S (mdr_i_unique_valuehsc)) * mdr_c_unique_value) + (mdr_z_unique_valuehscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_unique_valuehscm_positive. (exists ff_gap_mdm_lt_mdr_unique_valuehscm_positive_index_bound. ff_gap_mdm_lt_mdr_unique_valuehscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_unique_valuehscm_positive) = ((mdr_q_unique_valuehs) * (mdr_q_unique_valuehs))) -> exists ff_row_mdm_prefix_mdr_unique_valuehscm_positive ff_column_mdm_prefix_mdr_unique_valuehscm_positive ff_value_mdm_prefix_mdr_unique_valuehscm_positive. (ff_index_mdm_prefix_mdr_unique_valuehscm_positive = (mdr_q_unique_valuehs) * ff_row_mdm_prefix_mdr_unique_valuehscm_positive + ff_column_mdm_prefix_mdr_unique_valuehscm_positive /\ ((exists ff_gap_mdm_lt_mdr_unique_valuehscm_positive_column_bound. ff_gap_mdm_lt_mdr_unique_valuehscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_unique_valuehscm_positive) = (mdr_q_unique_valuehs)) /\ ((exists ff_row_mdm_cell_mdr_unique_valuehscm_positive_cell ff_column_mdm_cell_mdr_unique_valuehscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_unique_valuehscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_unique_valuehscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_unique_valuehscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_unique_valuehscm_positive_cell = ff_row_mdm_prefix_mdr_unique_valuehscm_positive) \/ ((exists ff_gap_mdm_le_mdr_unique_valuehscm_positive_cell_row_after. ff_gap_mdm_le_mdr_unique_valuehscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_unique_valuehscm_positive)) /\ ff_row_mdm_cell_mdr_unique_valuehscm_positive_cell = S ff_row_mdm_prefix_mdr_unique_valuehscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_unique_valuehscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_unique_valuehscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_unique_valuehscm_positive) = (mdr_j_unique_valuehsc)) /\ ff_column_mdm_cell_mdr_unique_valuehscm_positive_cell = ff_column_mdm_prefix_mdr_unique_valuehscm_positive) \/ ((exists ff_gap_mdm_le_mdr_unique_valuehscm_positive_cell_column_after. ff_gap_mdm_le_mdr_unique_valuehscm_positive_cell_column_after + (mdr_j_unique_valuehsc) = (ff_column_mdm_prefix_mdr_unique_valuehscm_positive)) /\ ff_column_mdm_cell_mdr_unique_valuehscm_positive_cell = S ff_column_mdm_prefix_mdr_unique_valuehscm_positive))) /\ (((exists ff_h_mdm_mdr_unique_valuehscm_positive_cell_source. ff_h_mdm_mdr_unique_valuehscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_unique_valuehscm_positive) = S ((S ((ff_row_mdm_cell_mdr_unique_valuehscm_positive_cell) * (S (mdr_q_unique_valuehs)) + (ff_column_mdm_cell_mdr_unique_valuehscm_positive_cell))) * mdr_pc_unique_valueh)) /\ exists ff_q_mdm_mdr_unique_valuehscm_positive_cell_source. mdr_pb_unique_valueh = ff_q_mdm_mdr_unique_valuehscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_unique_valuehscm_positive_cell) * (S (mdr_q_unique_valuehs)) + (ff_column_mdm_cell_mdr_unique_valuehscm_positive_cell))) * mdr_pc_unique_valueh) + (ff_value_mdm_prefix_mdr_unique_valuehscm_positive)))))) /\ (((exists ff_h_mdm_mdr_unique_valuehscm_positive_target. ff_h_mdm_mdr_unique_valuehscm_positive_target + S (ff_value_mdm_prefix_mdr_unique_valuehscm_positive) = S ((S (ff_index_mdm_prefix_mdr_unique_valuehscm_positive)) * mdr_us_unique_valuehsc)) /\ exists ff_q_mdm_mdr_unique_valuehscm_positive_target. mdr_up_unique_valuehsc = ff_q_mdm_mdr_unique_valuehscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_unique_valuehscm_positive)) * mdr_us_unique_valuehsc) + (ff_value_mdm_prefix_mdr_unique_valuehscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_unique_valuehscm_negative. (exists ff_gap_mdm_lt_mdr_unique_valuehscm_negative_index_bound. ff_gap_mdm_lt_mdr_unique_valuehscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_unique_valuehscm_negative) = ((mdr_q_unique_valuehs) * (mdr_q_unique_valuehs))) -> exists ff_row_mdm_prefix_mdr_unique_valuehscm_negative ff_column_mdm_prefix_mdr_unique_valuehscm_negative ff_value_mdm_prefix_mdr_unique_valuehscm_negative. (ff_index_mdm_prefix_mdr_unique_valuehscm_negative = (mdr_q_unique_valuehs) * ff_row_mdm_prefix_mdr_unique_valuehscm_negative + ff_column_mdm_prefix_mdr_unique_valuehscm_negative /\ ((exists ff_gap_mdm_lt_mdr_unique_valuehscm_negative_column_bound. ff_gap_mdm_lt_mdr_unique_valuehscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_unique_valuehscm_negative) = (mdr_q_unique_valuehs)) /\ ((exists ff_row_mdm_cell_mdr_unique_valuehscm_negative_cell ff_column_mdm_cell_mdr_unique_valuehscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_unique_valuehscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_unique_valuehscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_unique_valuehscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_unique_valuehscm_negative_cell = ff_row_mdm_prefix_mdr_unique_valuehscm_negative) \/ ((exists ff_gap_mdm_le_mdr_unique_valuehscm_negative_cell_row_after. ff_gap_mdm_le_mdr_unique_valuehscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_unique_valuehscm_negative)) /\ ff_row_mdm_cell_mdr_unique_valuehscm_negative_cell = S ff_row_mdm_prefix_mdr_unique_valuehscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_unique_valuehscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_unique_valuehscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_unique_valuehscm_negative) = (mdr_j_unique_valuehsc)) /\ ff_column_mdm_cell_mdr_unique_valuehscm_negative_cell = ff_column_mdm_prefix_mdr_unique_valuehscm_negative) \/ ((exists ff_gap_mdm_le_mdr_unique_valuehscm_negative_cell_column_after. ff_gap_mdm_le_mdr_unique_valuehscm_negative_cell_column_after + (mdr_j_unique_valuehsc) = (ff_column_mdm_prefix_mdr_unique_valuehscm_negative)) /\ ff_column_mdm_cell_mdr_unique_valuehscm_negative_cell = S ff_column_mdm_prefix_mdr_unique_valuehscm_negative))) /\ (((exists ff_h_mdm_mdr_unique_valuehscm_negative_cell_source. ff_h_mdm_mdr_unique_valuehscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_unique_valuehscm_negative) = S ((S ((ff_row_mdm_cell_mdr_unique_valuehscm_negative_cell) * (S (mdr_q_unique_valuehs)) + (ff_column_mdm_cell_mdr_unique_valuehscm_negative_cell))) * mdr_nc_unique_valueh)) /\ exists ff_q_mdm_mdr_unique_valuehscm_negative_cell_source. mdr_nb_unique_valueh = ff_q_mdm_mdr_unique_valuehscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_unique_valuehscm_negative_cell) * (S (mdr_q_unique_valuehs)) + (ff_column_mdm_cell_mdr_unique_valuehscm_negative_cell))) * mdr_nc_unique_valueh) + (ff_value_mdm_prefix_mdr_unique_valuehscm_negative)))))) /\ (((exists ff_h_mdm_mdr_unique_valuehscm_negative_target. ff_h_mdm_mdr_unique_valuehscm_negative_target + S (ff_value_mdm_prefix_mdr_unique_valuehscm_negative) = S ((S (ff_index_mdm_prefix_mdr_unique_valuehscm_negative)) * mdr_ut_unique_valuehsc)) /\ exists ff_q_mdm_mdr_unique_valuehscm_negative_target. mdr_un_unique_valuehsc = ff_q_mdm_mdr_unique_valuehscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_unique_valuehscm_negative)) * mdr_ut_unique_valuehsc) + (ff_value_mdm_prefix_mdr_unique_valuehscm_negative))))))))) /\ ((((exists ff_h_mdr_unique_valuehscp. ff_h_mdr_unique_valuehscp + S (mdr_p_unique_valuehsc) = S ((S (mdr_j_unique_valuehsc)) * mdr_ec_unique_valuehs)) /\ exists ff_q_mdr_unique_valuehscp. mdr_eb_unique_valuehs = ff_q_mdr_unique_valuehscp * S ((S (mdr_j_unique_valuehsc)) * mdr_ec_unique_valuehs) + (mdr_p_unique_valuehsc))) /\ (((exists ff_h_mdr_unique_valuehscn. ff_h_mdr_unique_valuehscn + S (mdr_n_unique_valuehsc) = S ((S (mdr_j_unique_valuehsc)) * mdr_fc_unique_valuehs)) /\ exists ff_q_mdr_unique_valuehscn. mdr_fb_unique_valuehs = ff_q_mdr_unique_valuehscn * S ((S (mdr_j_unique_valuehsc)) * mdr_fc_unique_valuehs) + (mdr_n_unique_valuehsc)))))))) /\ (exists ff_ub_mce_fold_mdr_unique_valuehsf ff_uc_mce_fold_mdr_unique_valuehsf ff_vb_mce_fold_mdr_unique_valuehsf ff_vc_mce_fold_mdr_unique_valuehsf. ((forall ff_index_mce_alternating_mdr_unique_valuehsf_prefix. (exists ff_gap_mce_mdr_unique_valuehsf_prefix_index. ff_gap_mce_mdr_unique_valuehsf_prefix_index + S (ff_index_mce_alternating_mdr_unique_valuehsf_prefix) = (S (mdr_q_unique_valuehs))) -> exists ff_ap_mce_alternating_mdr_unique_valuehsf_prefix ff_an_mce_alternating_mdr_unique_valuehsf_prefix ff_bp_mce_alternating_mdr_unique_valuehsf_prefix ff_bn_mce_alternating_mdr_unique_valuehsf_prefix ff_p_mce_alternating_mdr_unique_valuehsf_prefix ff_n_mce_alternating_mdr_unique_valuehsf_prefix. ((((exists ff_h_mce_mdr_unique_valuehsf_prefix_ap. ff_h_mce_mdr_unique_valuehsf_prefix_ap + S (ff_ap_mce_alternating_mdr_unique_valuehsf_prefix) = S ((S (ff_index_mce_alternating_mdr_unique_valuehsf_prefix)) * mdr_pc_unique_valueh)) /\ exists ff_q_mce_mdr_unique_valuehsf_prefix_ap. mdr_pb_unique_valueh = ff_q_mce_mdr_unique_valuehsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_unique_valuehsf_prefix)) * mdr_pc_unique_valueh) + (ff_ap_mce_alternating_mdr_unique_valuehsf_prefix))) /\ ((((exists ff_h_mce_mdr_unique_valuehsf_prefix_an. ff_h_mce_mdr_unique_valuehsf_prefix_an + S (ff_an_mce_alternating_mdr_unique_valuehsf_prefix) = S ((S (ff_index_mce_alternating_mdr_unique_valuehsf_prefix)) * mdr_nc_unique_valueh)) /\ exists ff_q_mce_mdr_unique_valuehsf_prefix_an. mdr_nb_unique_valueh = ff_q_mce_mdr_unique_valuehsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_unique_valuehsf_prefix)) * mdr_nc_unique_valueh) + (ff_an_mce_alternating_mdr_unique_valuehsf_prefix))) /\ ((((exists ff_h_mce_mdr_unique_valuehsf_prefix_bp. ff_h_mce_mdr_unique_valuehsf_prefix_bp + S (ff_bp_mce_alternating_mdr_unique_valuehsf_prefix) = S ((S (ff_index_mce_alternating_mdr_unique_valuehsf_prefix)) * mdr_ec_unique_valuehs)) /\ exists ff_q_mce_mdr_unique_valuehsf_prefix_bp. mdr_eb_unique_valuehs = ff_q_mce_mdr_unique_valuehsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_unique_valuehsf_prefix)) * mdr_ec_unique_valuehs) + (ff_bp_mce_alternating_mdr_unique_valuehsf_prefix))) /\ ((((exists ff_h_mce_mdr_unique_valuehsf_prefix_bn. ff_h_mce_mdr_unique_valuehsf_prefix_bn + S (ff_bn_mce_alternating_mdr_unique_valuehsf_prefix) = S ((S (ff_index_mce_alternating_mdr_unique_valuehsf_prefix)) * mdr_fc_unique_valuehs)) /\ exists ff_q_mce_mdr_unique_valuehsf_prefix_bn. mdr_fb_unique_valuehs = ff_q_mce_mdr_unique_valuehsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_unique_valuehsf_prefix)) * mdr_fc_unique_valuehs) + (ff_bn_mce_alternating_mdr_unique_valuehsf_prefix))) /\ ((((exists ff_h_mce_mdr_unique_valuehsf_prefix_positive. ff_h_mce_mdr_unique_valuehsf_prefix_positive + S (ff_p_mce_alternating_mdr_unique_valuehsf_prefix) = S ((S (ff_index_mce_alternating_mdr_unique_valuehsf_prefix)) * ff_uc_mce_fold_mdr_unique_valuehsf)) /\ exists ff_q_mce_mdr_unique_valuehsf_prefix_positive. ff_ub_mce_fold_mdr_unique_valuehsf = ff_q_mce_mdr_unique_valuehsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_unique_valuehsf_prefix)) * ff_uc_mce_fold_mdr_unique_valuehsf) + (ff_p_mce_alternating_mdr_unique_valuehsf_prefix))) /\ ((((exists ff_h_mce_mdr_unique_valuehsf_prefix_negative. ff_h_mce_mdr_unique_valuehsf_prefix_negative + S (ff_n_mce_alternating_mdr_unique_valuehsf_prefix) = S ((S (ff_index_mce_alternating_mdr_unique_valuehsf_prefix)) * ff_vc_mce_fold_mdr_unique_valuehsf)) /\ exists ff_q_mce_mdr_unique_valuehsf_prefix_negative. ff_vb_mce_fold_mdr_unique_valuehsf = ff_q_mce_mdr_unique_valuehsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_unique_valuehsf_prefix)) * ff_vc_mce_fold_mdr_unique_valuehsf) + (ff_n_mce_alternating_mdr_unique_valuehsf_prefix))) /\ (((exists ff_even_mce_term_mdr_unique_valuehsf_prefix_term. ff_index_mce_alternating_mdr_unique_valuehsf_prefix = 2 * ff_even_mce_term_mdr_unique_valuehsf_prefix_term) /\ (ff_p_mce_alternating_mdr_unique_valuehsf_prefix = (ff_ap_mce_alternating_mdr_unique_valuehsf_prefix) * (ff_bp_mce_alternating_mdr_unique_valuehsf_prefix) + (ff_an_mce_alternating_mdr_unique_valuehsf_prefix) * (ff_bn_mce_alternating_mdr_unique_valuehsf_prefix) /\ ff_n_mce_alternating_mdr_unique_valuehsf_prefix = (ff_ap_mce_alternating_mdr_unique_valuehsf_prefix) * (ff_bn_mce_alternating_mdr_unique_valuehsf_prefix) + (ff_an_mce_alternating_mdr_unique_valuehsf_prefix) * (ff_bp_mce_alternating_mdr_unique_valuehsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_unique_valuehsf_prefix_term. ff_index_mce_alternating_mdr_unique_valuehsf_prefix = 2 * ff_odd_mce_term_mdr_unique_valuehsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_unique_valuehsf_prefix = (ff_ap_mce_alternating_mdr_unique_valuehsf_prefix) * (ff_bn_mce_alternating_mdr_unique_valuehsf_prefix) + (ff_an_mce_alternating_mdr_unique_valuehsf_prefix) * (ff_bp_mce_alternating_mdr_unique_valuehsf_prefix) /\ ff_n_mce_alternating_mdr_unique_valuehsf_prefix = (ff_ap_mce_alternating_mdr_unique_valuehsf_prefix) * (ff_bp_mce_alternating_mdr_unique_valuehsf_prefix) + (ff_an_mce_alternating_mdr_unique_valuehsf_prefix) * (ff_bn_mce_alternating_mdr_unique_valuehsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_unique_valuehsf_positive ff_v_mce_mdr_unique_valuehsf_positive. ((((exists ff_h_mce_mdr_unique_valuehsf_positive_start. ff_h_mce_mdr_unique_valuehsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_unique_valuehsf_positive)) /\ exists ff_q_mce_mdr_unique_valuehsf_positive_start. ff_u_mce_mdr_unique_valuehsf_positive = ff_q_mce_mdr_unique_valuehsf_positive_start * S ((S (0)) * ff_v_mce_mdr_unique_valuehsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_unique_valuehsf_positive_terminal. ff_h_mce_mdr_unique_valuehsf_positive_terminal + S (mdr_p_unique_valueh) = S ((S ((S (mdr_q_unique_valuehs)))) * ff_v_mce_mdr_unique_valuehsf_positive)) /\ exists ff_q_mce_mdr_unique_valuehsf_positive_terminal. ff_u_mce_mdr_unique_valuehsf_positive = ff_q_mce_mdr_unique_valuehsf_positive_terminal * S ((S ((S (mdr_q_unique_valuehs)))) * ff_v_mce_mdr_unique_valuehsf_positive) + (mdr_p_unique_valueh))) /\ forall ff_i_mce_mdr_unique_valuehsf_positive. (exists ff_lt_mce_mdr_unique_valuehsf_positive_bound. ff_lt_mce_mdr_unique_valuehsf_positive_bound + S ff_i_mce_mdr_unique_valuehsf_positive = (S (mdr_q_unique_valuehs))) -> exists ff_a_mce_mdr_unique_valuehsf_positive ff_r_mce_mdr_unique_valuehsf_positive ff_s_mce_mdr_unique_valuehsf_positive. ((((exists ff_h_mce_mdr_unique_valuehsf_positive_summand. ff_h_mce_mdr_unique_valuehsf_positive_summand + S (ff_a_mce_mdr_unique_valuehsf_positive) = S ((S (ff_i_mce_mdr_unique_valuehsf_positive)) * ff_uc_mce_fold_mdr_unique_valuehsf)) /\ exists ff_q_mce_mdr_unique_valuehsf_positive_summand. ff_ub_mce_fold_mdr_unique_valuehsf = ff_q_mce_mdr_unique_valuehsf_positive_summand * S ((S (ff_i_mce_mdr_unique_valuehsf_positive)) * ff_uc_mce_fold_mdr_unique_valuehsf) + (ff_a_mce_mdr_unique_valuehsf_positive))) /\ ((((exists ff_h_mce_mdr_unique_valuehsf_positive_partial. ff_h_mce_mdr_unique_valuehsf_positive_partial + S (ff_r_mce_mdr_unique_valuehsf_positive) = S ((S (ff_i_mce_mdr_unique_valuehsf_positive)) * ff_v_mce_mdr_unique_valuehsf_positive)) /\ exists ff_q_mce_mdr_unique_valuehsf_positive_partial. ff_u_mce_mdr_unique_valuehsf_positive = ff_q_mce_mdr_unique_valuehsf_positive_partial * S ((S (ff_i_mce_mdr_unique_valuehsf_positive)) * ff_v_mce_mdr_unique_valuehsf_positive) + (ff_r_mce_mdr_unique_valuehsf_positive))) /\ ((((exists ff_h_mce_mdr_unique_valuehsf_positive_successor. ff_h_mce_mdr_unique_valuehsf_positive_successor + S (ff_s_mce_mdr_unique_valuehsf_positive) = S ((S (S ff_i_mce_mdr_unique_valuehsf_positive)) * ff_v_mce_mdr_unique_valuehsf_positive)) /\ exists ff_q_mce_mdr_unique_valuehsf_positive_successor. ff_u_mce_mdr_unique_valuehsf_positive = ff_q_mce_mdr_unique_valuehsf_positive_successor * S ((S (S ff_i_mce_mdr_unique_valuehsf_positive)) * ff_v_mce_mdr_unique_valuehsf_positive) + (ff_s_mce_mdr_unique_valuehsf_positive))) /\ ff_s_mce_mdr_unique_valuehsf_positive = ff_r_mce_mdr_unique_valuehsf_positive + ff_a_mce_mdr_unique_valuehsf_positive)))))) /\ (exists ff_u_mce_mdr_unique_valuehsf_negative ff_v_mce_mdr_unique_valuehsf_negative. ((((exists ff_h_mce_mdr_unique_valuehsf_negative_start. ff_h_mce_mdr_unique_valuehsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_unique_valuehsf_negative)) /\ exists ff_q_mce_mdr_unique_valuehsf_negative_start. ff_u_mce_mdr_unique_valuehsf_negative = ff_q_mce_mdr_unique_valuehsf_negative_start * S ((S (0)) * ff_v_mce_mdr_unique_valuehsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_unique_valuehsf_negative_terminal. ff_h_mce_mdr_unique_valuehsf_negative_terminal + S (mdr_n_unique_valueh) = S ((S ((S (mdr_q_unique_valuehs)))) * ff_v_mce_mdr_unique_valuehsf_negative)) /\ exists ff_q_mce_mdr_unique_valuehsf_negative_terminal. ff_u_mce_mdr_unique_valuehsf_negative = ff_q_mce_mdr_unique_valuehsf_negative_terminal * S ((S ((S (mdr_q_unique_valuehs)))) * ff_v_mce_mdr_unique_valuehsf_negative) + (mdr_n_unique_valueh))) /\ forall ff_i_mce_mdr_unique_valuehsf_negative. (exists ff_lt_mce_mdr_unique_valuehsf_negative_bound. ff_lt_mce_mdr_unique_valuehsf_negative_bound + S ff_i_mce_mdr_unique_valuehsf_negative = (S (mdr_q_unique_valuehs))) -> exists ff_a_mce_mdr_unique_valuehsf_negative ff_r_mce_mdr_unique_valuehsf_negative ff_s_mce_mdr_unique_valuehsf_negative. ((((exists ff_h_mce_mdr_unique_valuehsf_negative_summand. ff_h_mce_mdr_unique_valuehsf_negative_summand + S (ff_a_mce_mdr_unique_valuehsf_negative) = S ((S (ff_i_mce_mdr_unique_valuehsf_negative)) * ff_vc_mce_fold_mdr_unique_valuehsf)) /\ exists ff_q_mce_mdr_unique_valuehsf_negative_summand. ff_vb_mce_fold_mdr_unique_valuehsf = ff_q_mce_mdr_unique_valuehsf_negative_summand * S ((S (ff_i_mce_mdr_unique_valuehsf_negative)) * ff_vc_mce_fold_mdr_unique_valuehsf) + (ff_a_mce_mdr_unique_valuehsf_negative))) /\ ((((exists ff_h_mce_mdr_unique_valuehsf_negative_partial. ff_h_mce_mdr_unique_valuehsf_negative_partial + S (ff_r_mce_mdr_unique_valuehsf_negative) = S ((S (ff_i_mce_mdr_unique_valuehsf_negative)) * ff_v_mce_mdr_unique_valuehsf_negative)) /\ exists ff_q_mce_mdr_unique_valuehsf_negative_partial. ff_u_mce_mdr_unique_valuehsf_negative = ff_q_mce_mdr_unique_valuehsf_negative_partial * S ((S (ff_i_mce_mdr_unique_valuehsf_negative)) * ff_v_mce_mdr_unique_valuehsf_negative) + (ff_r_mce_mdr_unique_valuehsf_negative))) /\ ((((exists ff_h_mce_mdr_unique_valuehsf_negative_successor. ff_h_mce_mdr_unique_valuehsf_negative_successor + S (ff_s_mce_mdr_unique_valuehsf_negative) = S ((S (S ff_i_mce_mdr_unique_valuehsf_negative)) * ff_v_mce_mdr_unique_valuehsf_negative)) /\ exists ff_q_mce_mdr_unique_valuehsf_negative_successor. ff_u_mce_mdr_unique_valuehsf_negative = ff_q_mce_mdr_unique_valuehsf_negative_successor * S ((S (S ff_i_mce_mdr_unique_valuehsf_negative)) * ff_v_mce_mdr_unique_valuehsf_negative) + (ff_s_mce_mdr_unique_valuehsf_negative))) /\ ff_s_mce_mdr_unique_valuehsf_negative = ff_r_mce_mdr_unique_valuehsf_negative + ff_a_mce_mdr_unique_valuehsf_negative))))))))))))))) /\ ((exists mdr_gap_unique_valuei. mdr_gap_unique_valuei + S (mdr_i_unique_value) = (mdr_l_unique_value)) /\ (exists mdr_z_unique_valuer. ((exists mdr_a_unique_valuerc mdr_b_unique_valuerc mdr_c_unique_valuerc mdr_e_unique_valuerc mdr_f_unique_valuerc. ((mdr_a_unique_valuerc = ((d) + (pb)) * S ((d) + (pb)) + ((pb) + (pb))) /\ ((mdr_b_unique_valuerc = ((pc) + (nb)) * S ((pc) + (nb)) + ((nb) + (nb))) /\ ((mdr_c_unique_valuerc = ((mdr_a_unique_valuerc) + (mdr_b_unique_valuerc)) * S ((mdr_a_unique_valuerc) + (mdr_b_unique_valuerc)) + ((mdr_b_unique_valuerc) + (mdr_b_unique_valuerc))) /\ ((mdr_e_unique_valuerc = ((p) + (n)) * S ((p) + (n)) + ((n) + (n))) /\ ((mdr_f_unique_valuerc = ((nc) + (mdr_e_unique_valuerc)) * S ((nc) + (mdr_e_unique_valuerc)) + ((mdr_e_unique_valuerc) + (mdr_e_unique_valuerc))) /\ ((mdr_z_unique_valuer) = ((mdr_c_unique_valuerc) + (mdr_f_unique_valuerc)) * S ((mdr_c_unique_valuerc) + (mdr_f_unique_valuerc)) + ((mdr_f_unique_valuerc) + (mdr_f_unique_valuerc))))))))) /\ (((exists ff_h_mdr_unique_valuerb. ff_h_mdr_unique_valuerb + S (mdr_z_unique_valuer) = S ((S (mdr_i_unique_value)) * mdr_c_unique_value)) /\ exists ff_q_mdr_unique_valuerb. mdr_b_unique_value = ff_q_mdr_unique_valuerb * S ((S (mdr_i_unique_value)) * mdr_c_unique_value) + (mdr_z_unique_valuer)))))))) /\ (forall r s. (exists mdr_b_unique_other mdr_c_unique_other mdr_l_unique_other mdr_i_unique_other. ((forall mdr_i_unique_otherh. (exists mdr_gap_unique_otherhi. mdr_gap_unique_otherhi + S (mdr_i_unique_otherh) = (mdr_l_unique_other)) -> exists mdr_d_unique_otherh mdr_pb_unique_otherh mdr_pc_unique_otherh mdr_nb_unique_otherh mdr_nc_unique_otherh mdr_p_unique_otherh mdr_n_unique_otherh. ((exists mdr_z_unique_otherhr. ((exists mdr_a_unique_otherhrc mdr_b_unique_otherhrc mdr_c_unique_otherhrc mdr_e_unique_otherhrc mdr_f_unique_otherhrc. ((mdr_a_unique_otherhrc = ((mdr_d_unique_otherh) + (mdr_pb_unique_otherh)) * S ((mdr_d_unique_otherh) + (mdr_pb_unique_otherh)) + ((mdr_pb_unique_otherh) + (mdr_pb_unique_otherh))) /\ ((mdr_b_unique_otherhrc = ((mdr_pc_unique_otherh) + (mdr_nb_unique_otherh)) * S ((mdr_pc_unique_otherh) + (mdr_nb_unique_otherh)) + ((mdr_nb_unique_otherh) + (mdr_nb_unique_otherh))) /\ ((mdr_c_unique_otherhrc = ((mdr_a_unique_otherhrc) + (mdr_b_unique_otherhrc)) * S ((mdr_a_unique_otherhrc) + (mdr_b_unique_otherhrc)) + ((mdr_b_unique_otherhrc) + (mdr_b_unique_otherhrc))) /\ ((mdr_e_unique_otherhrc = ((mdr_p_unique_otherh) + (mdr_n_unique_otherh)) * S ((mdr_p_unique_otherh) + (mdr_n_unique_otherh)) + ((mdr_n_unique_otherh) + (mdr_n_unique_otherh))) /\ ((mdr_f_unique_otherhrc = ((mdr_nc_unique_otherh) + (mdr_e_unique_otherhrc)) * S ((mdr_nc_unique_otherh) + (mdr_e_unique_otherhrc)) + ((mdr_e_unique_otherhrc) + (mdr_e_unique_otherhrc))) /\ ((mdr_z_unique_otherhr) = ((mdr_c_unique_otherhrc) + (mdr_f_unique_otherhrc)) * S ((mdr_c_unique_otherhrc) + (mdr_f_unique_otherhrc)) + ((mdr_f_unique_otherhrc) + (mdr_f_unique_otherhrc))))))))) /\ (((exists ff_h_mdr_unique_otherhrb. ff_h_mdr_unique_otherhrb + S (mdr_z_unique_otherhr) = S ((S (mdr_i_unique_otherh)) * mdr_c_unique_other)) /\ exists ff_q_mdr_unique_otherhrb. mdr_b_unique_other = ff_q_mdr_unique_otherhrb * S ((S (mdr_i_unique_otherh)) * mdr_c_unique_other) + (mdr_z_unique_otherhr))))) /\ (((((mdr_d_unique_otherh) = 0) /\ (((mdr_p_unique_otherh) = 1) /\ ((mdr_n_unique_otherh) = 0))) \/ exists mdr_q_unique_otherhs mdr_eb_unique_otherhs mdr_ec_unique_otherhs mdr_fb_unique_otherhs mdr_fc_unique_otherhs. (((mdr_d_unique_otherh) = S (mdr_q_unique_otherhs)) /\ ((forall mdr_j_unique_otherhsc. (exists mdr_gap_unique_otherhscj. mdr_gap_unique_otherhscj + S (mdr_j_unique_otherhsc) = (S (mdr_q_unique_otherhs))) -> exists mdr_i_unique_otherhsc mdr_up_unique_otherhsc mdr_us_unique_otherhsc mdr_un_unique_otherhsc mdr_ut_unique_otherhsc mdr_p_unique_otherhsc mdr_n_unique_otherhsc. ((exists mdr_gap_unique_otherhsci. mdr_gap_unique_otherhsci + S (mdr_i_unique_otherhsc) = (mdr_i_unique_otherh)) /\ ((exists mdr_z_unique_otherhscr. ((exists mdr_a_unique_otherhscrc mdr_b_unique_otherhscrc mdr_c_unique_otherhscrc mdr_e_unique_otherhscrc mdr_f_unique_otherhscrc. ((mdr_a_unique_otherhscrc = ((mdr_q_unique_otherhs) + (mdr_up_unique_otherhsc)) * S ((mdr_q_unique_otherhs) + (mdr_up_unique_otherhsc)) + ((mdr_up_unique_otherhsc) + (mdr_up_unique_otherhsc))) /\ ((mdr_b_unique_otherhscrc = ((mdr_us_unique_otherhsc) + (mdr_un_unique_otherhsc)) * S ((mdr_us_unique_otherhsc) + (mdr_un_unique_otherhsc)) + ((mdr_un_unique_otherhsc) + (mdr_un_unique_otherhsc))) /\ ((mdr_c_unique_otherhscrc = ((mdr_a_unique_otherhscrc) + (mdr_b_unique_otherhscrc)) * S ((mdr_a_unique_otherhscrc) + (mdr_b_unique_otherhscrc)) + ((mdr_b_unique_otherhscrc) + (mdr_b_unique_otherhscrc))) /\ ((mdr_e_unique_otherhscrc = ((mdr_p_unique_otherhsc) + (mdr_n_unique_otherhsc)) * S ((mdr_p_unique_otherhsc) + (mdr_n_unique_otherhsc)) + ((mdr_n_unique_otherhsc) + (mdr_n_unique_otherhsc))) /\ ((mdr_f_unique_otherhscrc = ((mdr_ut_unique_otherhsc) + (mdr_e_unique_otherhscrc)) * S ((mdr_ut_unique_otherhsc) + (mdr_e_unique_otherhscrc)) + ((mdr_e_unique_otherhscrc) + (mdr_e_unique_otherhscrc))) /\ ((mdr_z_unique_otherhscr) = ((mdr_c_unique_otherhscrc) + (mdr_f_unique_otherhscrc)) * S ((mdr_c_unique_otherhscrc) + (mdr_f_unique_otherhscrc)) + ((mdr_f_unique_otherhscrc) + (mdr_f_unique_otherhscrc))))))))) /\ (((exists ff_h_mdr_unique_otherhscrb. ff_h_mdr_unique_otherhscrb + S (mdr_z_unique_otherhscr) = S ((S (mdr_i_unique_otherhsc)) * mdr_c_unique_other)) /\ exists ff_q_mdr_unique_otherhscrb. mdr_b_unique_other = ff_q_mdr_unique_otherhscrb * S ((S (mdr_i_unique_otherhsc)) * mdr_c_unique_other) + (mdr_z_unique_otherhscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_unique_otherhscm_positive. (exists ff_gap_mdm_lt_mdr_unique_otherhscm_positive_index_bound. ff_gap_mdm_lt_mdr_unique_otherhscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_unique_otherhscm_positive) = ((mdr_q_unique_otherhs) * (mdr_q_unique_otherhs))) -> exists ff_row_mdm_prefix_mdr_unique_otherhscm_positive ff_column_mdm_prefix_mdr_unique_otherhscm_positive ff_value_mdm_prefix_mdr_unique_otherhscm_positive. (ff_index_mdm_prefix_mdr_unique_otherhscm_positive = (mdr_q_unique_otherhs) * ff_row_mdm_prefix_mdr_unique_otherhscm_positive + ff_column_mdm_prefix_mdr_unique_otherhscm_positive /\ ((exists ff_gap_mdm_lt_mdr_unique_otherhscm_positive_column_bound. ff_gap_mdm_lt_mdr_unique_otherhscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_unique_otherhscm_positive) = (mdr_q_unique_otherhs)) /\ ((exists ff_row_mdm_cell_mdr_unique_otherhscm_positive_cell ff_column_mdm_cell_mdr_unique_otherhscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_unique_otherhscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_unique_otherhscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_unique_otherhscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_unique_otherhscm_positive_cell = ff_row_mdm_prefix_mdr_unique_otherhscm_positive) \/ ((exists ff_gap_mdm_le_mdr_unique_otherhscm_positive_cell_row_after. ff_gap_mdm_le_mdr_unique_otherhscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_unique_otherhscm_positive)) /\ ff_row_mdm_cell_mdr_unique_otherhscm_positive_cell = S ff_row_mdm_prefix_mdr_unique_otherhscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_unique_otherhscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_unique_otherhscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_unique_otherhscm_positive) = (mdr_j_unique_otherhsc)) /\ ff_column_mdm_cell_mdr_unique_otherhscm_positive_cell = ff_column_mdm_prefix_mdr_unique_otherhscm_positive) \/ ((exists ff_gap_mdm_le_mdr_unique_otherhscm_positive_cell_column_after. ff_gap_mdm_le_mdr_unique_otherhscm_positive_cell_column_after + (mdr_j_unique_otherhsc) = (ff_column_mdm_prefix_mdr_unique_otherhscm_positive)) /\ ff_column_mdm_cell_mdr_unique_otherhscm_positive_cell = S ff_column_mdm_prefix_mdr_unique_otherhscm_positive))) /\ (((exists ff_h_mdm_mdr_unique_otherhscm_positive_cell_source. ff_h_mdm_mdr_unique_otherhscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_unique_otherhscm_positive) = S ((S ((ff_row_mdm_cell_mdr_unique_otherhscm_positive_cell) * (S (mdr_q_unique_otherhs)) + (ff_column_mdm_cell_mdr_unique_otherhscm_positive_cell))) * mdr_pc_unique_otherh)) /\ exists ff_q_mdm_mdr_unique_otherhscm_positive_cell_source. mdr_pb_unique_otherh = ff_q_mdm_mdr_unique_otherhscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_unique_otherhscm_positive_cell) * (S (mdr_q_unique_otherhs)) + (ff_column_mdm_cell_mdr_unique_otherhscm_positive_cell))) * mdr_pc_unique_otherh) + (ff_value_mdm_prefix_mdr_unique_otherhscm_positive)))))) /\ (((exists ff_h_mdm_mdr_unique_otherhscm_positive_target. ff_h_mdm_mdr_unique_otherhscm_positive_target + S (ff_value_mdm_prefix_mdr_unique_otherhscm_positive) = S ((S (ff_index_mdm_prefix_mdr_unique_otherhscm_positive)) * mdr_us_unique_otherhsc)) /\ exists ff_q_mdm_mdr_unique_otherhscm_positive_target. mdr_up_unique_otherhsc = ff_q_mdm_mdr_unique_otherhscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_unique_otherhscm_positive)) * mdr_us_unique_otherhsc) + (ff_value_mdm_prefix_mdr_unique_otherhscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_unique_otherhscm_negative. (exists ff_gap_mdm_lt_mdr_unique_otherhscm_negative_index_bound. ff_gap_mdm_lt_mdr_unique_otherhscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_unique_otherhscm_negative) = ((mdr_q_unique_otherhs) * (mdr_q_unique_otherhs))) -> exists ff_row_mdm_prefix_mdr_unique_otherhscm_negative ff_column_mdm_prefix_mdr_unique_otherhscm_negative ff_value_mdm_prefix_mdr_unique_otherhscm_negative. (ff_index_mdm_prefix_mdr_unique_otherhscm_negative = (mdr_q_unique_otherhs) * ff_row_mdm_prefix_mdr_unique_otherhscm_negative + ff_column_mdm_prefix_mdr_unique_otherhscm_negative /\ ((exists ff_gap_mdm_lt_mdr_unique_otherhscm_negative_column_bound. ff_gap_mdm_lt_mdr_unique_otherhscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_unique_otherhscm_negative) = (mdr_q_unique_otherhs)) /\ ((exists ff_row_mdm_cell_mdr_unique_otherhscm_negative_cell ff_column_mdm_cell_mdr_unique_otherhscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_unique_otherhscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_unique_otherhscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_unique_otherhscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_unique_otherhscm_negative_cell = ff_row_mdm_prefix_mdr_unique_otherhscm_negative) \/ ((exists ff_gap_mdm_le_mdr_unique_otherhscm_negative_cell_row_after. ff_gap_mdm_le_mdr_unique_otherhscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_unique_otherhscm_negative)) /\ ff_row_mdm_cell_mdr_unique_otherhscm_negative_cell = S ff_row_mdm_prefix_mdr_unique_otherhscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_unique_otherhscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_unique_otherhscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_unique_otherhscm_negative) = (mdr_j_unique_otherhsc)) /\ ff_column_mdm_cell_mdr_unique_otherhscm_negative_cell = ff_column_mdm_prefix_mdr_unique_otherhscm_negative) \/ ((exists ff_gap_mdm_le_mdr_unique_otherhscm_negative_cell_column_after. ff_gap_mdm_le_mdr_unique_otherhscm_negative_cell_column_after + (mdr_j_unique_otherhsc) = (ff_column_mdm_prefix_mdr_unique_otherhscm_negative)) /\ ff_column_mdm_cell_mdr_unique_otherhscm_negative_cell = S ff_column_mdm_prefix_mdr_unique_otherhscm_negative))) /\ (((exists ff_h_mdm_mdr_unique_otherhscm_negative_cell_source. ff_h_mdm_mdr_unique_otherhscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_unique_otherhscm_negative) = S ((S ((ff_row_mdm_cell_mdr_unique_otherhscm_negative_cell) * (S (mdr_q_unique_otherhs)) + (ff_column_mdm_cell_mdr_unique_otherhscm_negative_cell))) * mdr_nc_unique_otherh)) /\ exists ff_q_mdm_mdr_unique_otherhscm_negative_cell_source. mdr_nb_unique_otherh = ff_q_mdm_mdr_unique_otherhscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_unique_otherhscm_negative_cell) * (S (mdr_q_unique_otherhs)) + (ff_column_mdm_cell_mdr_unique_otherhscm_negative_cell))) * mdr_nc_unique_otherh) + (ff_value_mdm_prefix_mdr_unique_otherhscm_negative)))))) /\ (((exists ff_h_mdm_mdr_unique_otherhscm_negative_target. ff_h_mdm_mdr_unique_otherhscm_negative_target + S (ff_value_mdm_prefix_mdr_unique_otherhscm_negative) = S ((S (ff_index_mdm_prefix_mdr_unique_otherhscm_negative)) * mdr_ut_unique_otherhsc)) /\ exists ff_q_mdm_mdr_unique_otherhscm_negative_target. mdr_un_unique_otherhsc = ff_q_mdm_mdr_unique_otherhscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_unique_otherhscm_negative)) * mdr_ut_unique_otherhsc) + (ff_value_mdm_prefix_mdr_unique_otherhscm_negative))))))))) /\ ((((exists ff_h_mdr_unique_otherhscp. ff_h_mdr_unique_otherhscp + S (mdr_p_unique_otherhsc) = S ((S (mdr_j_unique_otherhsc)) * mdr_ec_unique_otherhs)) /\ exists ff_q_mdr_unique_otherhscp. mdr_eb_unique_otherhs = ff_q_mdr_unique_otherhscp * S ((S (mdr_j_unique_otherhsc)) * mdr_ec_unique_otherhs) + (mdr_p_unique_otherhsc))) /\ (((exists ff_h_mdr_unique_otherhscn. ff_h_mdr_unique_otherhscn + S (mdr_n_unique_otherhsc) = S ((S (mdr_j_unique_otherhsc)) * mdr_fc_unique_otherhs)) /\ exists ff_q_mdr_unique_otherhscn. mdr_fb_unique_otherhs = ff_q_mdr_unique_otherhscn * S ((S (mdr_j_unique_otherhsc)) * mdr_fc_unique_otherhs) + (mdr_n_unique_otherhsc)))))))) /\ (exists ff_ub_mce_fold_mdr_unique_otherhsf ff_uc_mce_fold_mdr_unique_otherhsf ff_vb_mce_fold_mdr_unique_otherhsf ff_vc_mce_fold_mdr_unique_otherhsf. ((forall ff_index_mce_alternating_mdr_unique_otherhsf_prefix. (exists ff_gap_mce_mdr_unique_otherhsf_prefix_index. ff_gap_mce_mdr_unique_otherhsf_prefix_index + S (ff_index_mce_alternating_mdr_unique_otherhsf_prefix) = (S (mdr_q_unique_otherhs))) -> exists ff_ap_mce_alternating_mdr_unique_otherhsf_prefix ff_an_mce_alternating_mdr_unique_otherhsf_prefix ff_bp_mce_alternating_mdr_unique_otherhsf_prefix ff_bn_mce_alternating_mdr_unique_otherhsf_prefix ff_p_mce_alternating_mdr_unique_otherhsf_prefix ff_n_mce_alternating_mdr_unique_otherhsf_prefix. ((((exists ff_h_mce_mdr_unique_otherhsf_prefix_ap. ff_h_mce_mdr_unique_otherhsf_prefix_ap + S (ff_ap_mce_alternating_mdr_unique_otherhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_unique_otherhsf_prefix)) * mdr_pc_unique_otherh)) /\ exists ff_q_mce_mdr_unique_otherhsf_prefix_ap. mdr_pb_unique_otherh = ff_q_mce_mdr_unique_otherhsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_unique_otherhsf_prefix)) * mdr_pc_unique_otherh) + (ff_ap_mce_alternating_mdr_unique_otherhsf_prefix))) /\ ((((exists ff_h_mce_mdr_unique_otherhsf_prefix_an. ff_h_mce_mdr_unique_otherhsf_prefix_an + S (ff_an_mce_alternating_mdr_unique_otherhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_unique_otherhsf_prefix)) * mdr_nc_unique_otherh)) /\ exists ff_q_mce_mdr_unique_otherhsf_prefix_an. mdr_nb_unique_otherh = ff_q_mce_mdr_unique_otherhsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_unique_otherhsf_prefix)) * mdr_nc_unique_otherh) + (ff_an_mce_alternating_mdr_unique_otherhsf_prefix))) /\ ((((exists ff_h_mce_mdr_unique_otherhsf_prefix_bp. ff_h_mce_mdr_unique_otherhsf_prefix_bp + S (ff_bp_mce_alternating_mdr_unique_otherhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_unique_otherhsf_prefix)) * mdr_ec_unique_otherhs)) /\ exists ff_q_mce_mdr_unique_otherhsf_prefix_bp. mdr_eb_unique_otherhs = ff_q_mce_mdr_unique_otherhsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_unique_otherhsf_prefix)) * mdr_ec_unique_otherhs) + (ff_bp_mce_alternating_mdr_unique_otherhsf_prefix))) /\ ((((exists ff_h_mce_mdr_unique_otherhsf_prefix_bn. ff_h_mce_mdr_unique_otherhsf_prefix_bn + S (ff_bn_mce_alternating_mdr_unique_otherhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_unique_otherhsf_prefix)) * mdr_fc_unique_otherhs)) /\ exists ff_q_mce_mdr_unique_otherhsf_prefix_bn. mdr_fb_unique_otherhs = ff_q_mce_mdr_unique_otherhsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_unique_otherhsf_prefix)) * mdr_fc_unique_otherhs) + (ff_bn_mce_alternating_mdr_unique_otherhsf_prefix))) /\ ((((exists ff_h_mce_mdr_unique_otherhsf_prefix_positive. ff_h_mce_mdr_unique_otherhsf_prefix_positive + S (ff_p_mce_alternating_mdr_unique_otherhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_unique_otherhsf_prefix)) * ff_uc_mce_fold_mdr_unique_otherhsf)) /\ exists ff_q_mce_mdr_unique_otherhsf_prefix_positive. ff_ub_mce_fold_mdr_unique_otherhsf = ff_q_mce_mdr_unique_otherhsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_unique_otherhsf_prefix)) * ff_uc_mce_fold_mdr_unique_otherhsf) + (ff_p_mce_alternating_mdr_unique_otherhsf_prefix))) /\ ((((exists ff_h_mce_mdr_unique_otherhsf_prefix_negative. ff_h_mce_mdr_unique_otherhsf_prefix_negative + S (ff_n_mce_alternating_mdr_unique_otherhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_unique_otherhsf_prefix)) * ff_vc_mce_fold_mdr_unique_otherhsf)) /\ exists ff_q_mce_mdr_unique_otherhsf_prefix_negative. ff_vb_mce_fold_mdr_unique_otherhsf = ff_q_mce_mdr_unique_otherhsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_unique_otherhsf_prefix)) * ff_vc_mce_fold_mdr_unique_otherhsf) + (ff_n_mce_alternating_mdr_unique_otherhsf_prefix))) /\ (((exists ff_even_mce_term_mdr_unique_otherhsf_prefix_term. ff_index_mce_alternating_mdr_unique_otherhsf_prefix = 2 * ff_even_mce_term_mdr_unique_otherhsf_prefix_term) /\ (ff_p_mce_alternating_mdr_unique_otherhsf_prefix = (ff_ap_mce_alternating_mdr_unique_otherhsf_prefix) * (ff_bp_mce_alternating_mdr_unique_otherhsf_prefix) + (ff_an_mce_alternating_mdr_unique_otherhsf_prefix) * (ff_bn_mce_alternating_mdr_unique_otherhsf_prefix) /\ ff_n_mce_alternating_mdr_unique_otherhsf_prefix = (ff_ap_mce_alternating_mdr_unique_otherhsf_prefix) * (ff_bn_mce_alternating_mdr_unique_otherhsf_prefix) + (ff_an_mce_alternating_mdr_unique_otherhsf_prefix) * (ff_bp_mce_alternating_mdr_unique_otherhsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_unique_otherhsf_prefix_term. ff_index_mce_alternating_mdr_unique_otherhsf_prefix = 2 * ff_odd_mce_term_mdr_unique_otherhsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_unique_otherhsf_prefix = (ff_ap_mce_alternating_mdr_unique_otherhsf_prefix) * (ff_bn_mce_alternating_mdr_unique_otherhsf_prefix) + (ff_an_mce_alternating_mdr_unique_otherhsf_prefix) * (ff_bp_mce_alternating_mdr_unique_otherhsf_prefix) /\ ff_n_mce_alternating_mdr_unique_otherhsf_prefix = (ff_ap_mce_alternating_mdr_unique_otherhsf_prefix) * (ff_bp_mce_alternating_mdr_unique_otherhsf_prefix) + (ff_an_mce_alternating_mdr_unique_otherhsf_prefix) * (ff_bn_mce_alternating_mdr_unique_otherhsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_unique_otherhsf_positive ff_v_mce_mdr_unique_otherhsf_positive. ((((exists ff_h_mce_mdr_unique_otherhsf_positive_start. ff_h_mce_mdr_unique_otherhsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_unique_otherhsf_positive)) /\ exists ff_q_mce_mdr_unique_otherhsf_positive_start. ff_u_mce_mdr_unique_otherhsf_positive = ff_q_mce_mdr_unique_otherhsf_positive_start * S ((S (0)) * ff_v_mce_mdr_unique_otherhsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_unique_otherhsf_positive_terminal. ff_h_mce_mdr_unique_otherhsf_positive_terminal + S (mdr_p_unique_otherh) = S ((S ((S (mdr_q_unique_otherhs)))) * ff_v_mce_mdr_unique_otherhsf_positive)) /\ exists ff_q_mce_mdr_unique_otherhsf_positive_terminal. ff_u_mce_mdr_unique_otherhsf_positive = ff_q_mce_mdr_unique_otherhsf_positive_terminal * S ((S ((S (mdr_q_unique_otherhs)))) * ff_v_mce_mdr_unique_otherhsf_positive) + (mdr_p_unique_otherh))) /\ forall ff_i_mce_mdr_unique_otherhsf_positive. (exists ff_lt_mce_mdr_unique_otherhsf_positive_bound. ff_lt_mce_mdr_unique_otherhsf_positive_bound + S ff_i_mce_mdr_unique_otherhsf_positive = (S (mdr_q_unique_otherhs))) -> exists ff_a_mce_mdr_unique_otherhsf_positive ff_r_mce_mdr_unique_otherhsf_positive ff_s_mce_mdr_unique_otherhsf_positive. ((((exists ff_h_mce_mdr_unique_otherhsf_positive_summand. ff_h_mce_mdr_unique_otherhsf_positive_summand + S (ff_a_mce_mdr_unique_otherhsf_positive) = S ((S (ff_i_mce_mdr_unique_otherhsf_positive)) * ff_uc_mce_fold_mdr_unique_otherhsf)) /\ exists ff_q_mce_mdr_unique_otherhsf_positive_summand. ff_ub_mce_fold_mdr_unique_otherhsf = ff_q_mce_mdr_unique_otherhsf_positive_summand * S ((S (ff_i_mce_mdr_unique_otherhsf_positive)) * ff_uc_mce_fold_mdr_unique_otherhsf) + (ff_a_mce_mdr_unique_otherhsf_positive))) /\ ((((exists ff_h_mce_mdr_unique_otherhsf_positive_partial. ff_h_mce_mdr_unique_otherhsf_positive_partial + S (ff_r_mce_mdr_unique_otherhsf_positive) = S ((S (ff_i_mce_mdr_unique_otherhsf_positive)) * ff_v_mce_mdr_unique_otherhsf_positive)) /\ exists ff_q_mce_mdr_unique_otherhsf_positive_partial. ff_u_mce_mdr_unique_otherhsf_positive = ff_q_mce_mdr_unique_otherhsf_positive_partial * S ((S (ff_i_mce_mdr_unique_otherhsf_positive)) * ff_v_mce_mdr_unique_otherhsf_positive) + (ff_r_mce_mdr_unique_otherhsf_positive))) /\ ((((exists ff_h_mce_mdr_unique_otherhsf_positive_successor. ff_h_mce_mdr_unique_otherhsf_positive_successor + S (ff_s_mce_mdr_unique_otherhsf_positive) = S ((S (S ff_i_mce_mdr_unique_otherhsf_positive)) * ff_v_mce_mdr_unique_otherhsf_positive)) /\ exists ff_q_mce_mdr_unique_otherhsf_positive_successor. ff_u_mce_mdr_unique_otherhsf_positive = ff_q_mce_mdr_unique_otherhsf_positive_successor * S ((S (S ff_i_mce_mdr_unique_otherhsf_positive)) * ff_v_mce_mdr_unique_otherhsf_positive) + (ff_s_mce_mdr_unique_otherhsf_positive))) /\ ff_s_mce_mdr_unique_otherhsf_positive = ff_r_mce_mdr_unique_otherhsf_positive + ff_a_mce_mdr_unique_otherhsf_positive)))))) /\ (exists ff_u_mce_mdr_unique_otherhsf_negative ff_v_mce_mdr_unique_otherhsf_negative. ((((exists ff_h_mce_mdr_unique_otherhsf_negative_start. ff_h_mce_mdr_unique_otherhsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_unique_otherhsf_negative)) /\ exists ff_q_mce_mdr_unique_otherhsf_negative_start. ff_u_mce_mdr_unique_otherhsf_negative = ff_q_mce_mdr_unique_otherhsf_negative_start * S ((S (0)) * ff_v_mce_mdr_unique_otherhsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_unique_otherhsf_negative_terminal. ff_h_mce_mdr_unique_otherhsf_negative_terminal + S (mdr_n_unique_otherh) = S ((S ((S (mdr_q_unique_otherhs)))) * ff_v_mce_mdr_unique_otherhsf_negative)) /\ exists ff_q_mce_mdr_unique_otherhsf_negative_terminal. ff_u_mce_mdr_unique_otherhsf_negative = ff_q_mce_mdr_unique_otherhsf_negative_terminal * S ((S ((S (mdr_q_unique_otherhs)))) * ff_v_mce_mdr_unique_otherhsf_negative) + (mdr_n_unique_otherh))) /\ forall ff_i_mce_mdr_unique_otherhsf_negative. (exists ff_lt_mce_mdr_unique_otherhsf_negative_bound. ff_lt_mce_mdr_unique_otherhsf_negative_bound + S ff_i_mce_mdr_unique_otherhsf_negative = (S (mdr_q_unique_otherhs))) -> exists ff_a_mce_mdr_unique_otherhsf_negative ff_r_mce_mdr_unique_otherhsf_negative ff_s_mce_mdr_unique_otherhsf_negative. ((((exists ff_h_mce_mdr_unique_otherhsf_negative_summand. ff_h_mce_mdr_unique_otherhsf_negative_summand + S (ff_a_mce_mdr_unique_otherhsf_negative) = S ((S (ff_i_mce_mdr_unique_otherhsf_negative)) * ff_vc_mce_fold_mdr_unique_otherhsf)) /\ exists ff_q_mce_mdr_unique_otherhsf_negative_summand. ff_vb_mce_fold_mdr_unique_otherhsf = ff_q_mce_mdr_unique_otherhsf_negative_summand * S ((S (ff_i_mce_mdr_unique_otherhsf_negative)) * ff_vc_mce_fold_mdr_unique_otherhsf) + (ff_a_mce_mdr_unique_otherhsf_negative))) /\ ((((exists ff_h_mce_mdr_unique_otherhsf_negative_partial. ff_h_mce_mdr_unique_otherhsf_negative_partial + S (ff_r_mce_mdr_unique_otherhsf_negative) = S ((S (ff_i_mce_mdr_unique_otherhsf_negative)) * ff_v_mce_mdr_unique_otherhsf_negative)) /\ exists ff_q_mce_mdr_unique_otherhsf_negative_partial. ff_u_mce_mdr_unique_otherhsf_negative = ff_q_mce_mdr_unique_otherhsf_negative_partial * S ((S (ff_i_mce_mdr_unique_otherhsf_negative)) * ff_v_mce_mdr_unique_otherhsf_negative) + (ff_r_mce_mdr_unique_otherhsf_negative))) /\ ((((exists ff_h_mce_mdr_unique_otherhsf_negative_successor. ff_h_mce_mdr_unique_otherhsf_negative_successor + S (ff_s_mce_mdr_unique_otherhsf_negative) = S ((S (S ff_i_mce_mdr_unique_otherhsf_negative)) * ff_v_mce_mdr_unique_otherhsf_negative)) /\ exists ff_q_mce_mdr_unique_otherhsf_negative_successor. ff_u_mce_mdr_unique_otherhsf_negative = ff_q_mce_mdr_unique_otherhsf_negative_successor * S ((S (S ff_i_mce_mdr_unique_otherhsf_negative)) * ff_v_mce_mdr_unique_otherhsf_negative) + (ff_s_mce_mdr_unique_otherhsf_negative))) /\ ff_s_mce_mdr_unique_otherhsf_negative = ff_r_mce_mdr_unique_otherhsf_negative + ff_a_mce_mdr_unique_otherhsf_negative))))))))))))))) /\ ((exists mdr_gap_unique_otheri. mdr_gap_unique_otheri + S (mdr_i_unique_other) = (mdr_l_unique_other)) /\ (exists mdr_z_unique_otherr. ((exists mdr_a_unique_otherrc mdr_b_unique_otherrc mdr_c_unique_otherrc mdr_e_unique_otherrc mdr_f_unique_otherrc. ((mdr_a_unique_otherrc = ((d) + (pb)) * S ((d) + (pb)) + ((pb) + (pb))) /\ ((mdr_b_unique_otherrc = ((pc) + (nb)) * S ((pc) + (nb)) + ((nb) + (nb))) /\ ((mdr_c_unique_otherrc = ((mdr_a_unique_otherrc) + (mdr_b_unique_otherrc)) * S ((mdr_a_unique_otherrc) + (mdr_b_unique_otherrc)) + ((mdr_b_unique_otherrc) + (mdr_b_unique_otherrc))) /\ ((mdr_e_unique_otherrc = ((r) + (s)) * S ((r) + (s)) + ((s) + (s))) /\ ((mdr_f_unique_otherrc = ((nc) + (mdr_e_unique_otherrc)) * S ((nc) + (mdr_e_unique_otherrc)) + ((mdr_e_unique_otherrc) + (mdr_e_unique_otherrc))) /\ ((mdr_z_unique_otherr) = ((mdr_c_unique_otherrc) + (mdr_f_unique_otherrc)) * S ((mdr_c_unique_otherrc) + (mdr_f_unique_otherrc)) + ((mdr_f_unique_otherrc) + (mdr_f_unique_otherrc))))))))) /\ (((exists ff_h_mdr_unique_otherrb. ff_h_mdr_unique_otherrb + S (mdr_z_unique_otherr) = S ((S (mdr_i_unique_other)) * mdr_c_unique_other)) /\ exists ff_q_mdr_unique_otherrb. mdr_b_unique_other = ff_q_mdr_unique_otherrb * S ((S (mdr_i_unique_other)) * mdr_c_unique_other) + (mdr_z_unique_otherr)))))))) -> r = p /\ s = n))