signed_recursive_determinant_functional

Exact expanded first-order arithmetic statement

forall pb pc nb nc d p n r s. (exists mdr_b_functional_first mdr_c_functional_first mdr_l_functional_first mdr_i_functional_first. ((forall mdr_i_functional_firsth. (exists mdr_gap_functional_firsthi. mdr_gap_functional_firsthi + S (mdr_i_functional_firsth) = (mdr_l_functional_first)) -> exists mdr_d_functional_firsth mdr_pb_functional_firsth mdr_pc_functional_firsth mdr_nb_functional_firsth mdr_nc_functional_firsth mdr_p_functional_firsth mdr_n_functional_firsth. ((exists mdr_z_functional_firsthr. ((exists mdr_a_functional_firsthrc mdr_b_functional_firsthrc mdr_c_functional_firsthrc mdr_e_functional_firsthrc mdr_f_functional_firsthrc. ((mdr_a_functional_firsthrc = ((mdr_d_functional_firsth) + (mdr_pb_functional_firsth)) * S ((mdr_d_functional_firsth) + (mdr_pb_functional_firsth)) + ((mdr_pb_functional_firsth) + (mdr_pb_functional_firsth))) /\ ((mdr_b_functional_firsthrc = ((mdr_pc_functional_firsth) + (mdr_nb_functional_firsth)) * S ((mdr_pc_functional_firsth) + (mdr_nb_functional_firsth)) + ((mdr_nb_functional_firsth) + (mdr_nb_functional_firsth))) /\ ((mdr_c_functional_firsthrc = ((mdr_a_functional_firsthrc) + (mdr_b_functional_firsthrc)) * S ((mdr_a_functional_firsthrc) + (mdr_b_functional_firsthrc)) + ((mdr_b_functional_firsthrc) + (mdr_b_functional_firsthrc))) /\ ((mdr_e_functional_firsthrc = ((mdr_p_functional_firsth) + (mdr_n_functional_firsth)) * S ((mdr_p_functional_firsth) + (mdr_n_functional_firsth)) + ((mdr_n_functional_firsth) + (mdr_n_functional_firsth))) /\ ((mdr_f_functional_firsthrc = ((mdr_nc_functional_firsth) + (mdr_e_functional_firsthrc)) * S ((mdr_nc_functional_firsth) + (mdr_e_functional_firsthrc)) + ((mdr_e_functional_firsthrc) + (mdr_e_functional_firsthrc))) /\ ((mdr_z_functional_firsthr) = ((mdr_c_functional_firsthrc) + (mdr_f_functional_firsthrc)) * S ((mdr_c_functional_firsthrc) + (mdr_f_functional_firsthrc)) + ((mdr_f_functional_firsthrc) + (mdr_f_functional_firsthrc))))))))) /\ (((exists ff_h_mdr_functional_firsthrb. ff_h_mdr_functional_firsthrb + S (mdr_z_functional_firsthr) = S ((S (mdr_i_functional_firsth)) * mdr_c_functional_first)) /\ exists ff_q_mdr_functional_firsthrb. mdr_b_functional_first = ff_q_mdr_functional_firsthrb * S ((S (mdr_i_functional_firsth)) * mdr_c_functional_first) + (mdr_z_functional_firsthr))))) /\ (((((mdr_d_functional_firsth) = 0) /\ (((mdr_p_functional_firsth) = 1) /\ ((mdr_n_functional_firsth) = 0))) \/ exists mdr_q_functional_firsths mdr_eb_functional_firsths mdr_ec_functional_firsths mdr_fb_functional_firsths mdr_fc_functional_firsths. (((mdr_d_functional_firsth) = S (mdr_q_functional_firsths)) /\ ((forall mdr_j_functional_firsthsc. (exists mdr_gap_functional_firsthscj. mdr_gap_functional_firsthscj + S (mdr_j_functional_firsthsc) = (S (mdr_q_functional_firsths))) -> exists mdr_i_functional_firsthsc mdr_up_functional_firsthsc mdr_us_functional_firsthsc mdr_un_functional_firsthsc mdr_ut_functional_firsthsc mdr_p_functional_firsthsc mdr_n_functional_firsthsc. ((exists mdr_gap_functional_firsthsci. mdr_gap_functional_firsthsci + S (mdr_i_functional_firsthsc) = (mdr_i_functional_firsth)) /\ ((exists mdr_z_functional_firsthscr. ((exists mdr_a_functional_firsthscrc mdr_b_functional_firsthscrc mdr_c_functional_firsthscrc mdr_e_functional_firsthscrc mdr_f_functional_firsthscrc. ((mdr_a_functional_firsthscrc = ((mdr_q_functional_firsths) + (mdr_up_functional_firsthsc)) * S ((mdr_q_functional_firsths) + (mdr_up_functional_firsthsc)) + ((mdr_up_functional_firsthsc) + (mdr_up_functional_firsthsc))) /\ ((mdr_b_functional_firsthscrc = ((mdr_us_functional_firsthsc) + (mdr_un_functional_firsthsc)) * S ((mdr_us_functional_firsthsc) + (mdr_un_functional_firsthsc)) + ((mdr_un_functional_firsthsc) + (mdr_un_functional_firsthsc))) /\ ((mdr_c_functional_firsthscrc = ((mdr_a_functional_firsthscrc) + (mdr_b_functional_firsthscrc)) * S ((mdr_a_functional_firsthscrc) + (mdr_b_functional_firsthscrc)) + ((mdr_b_functional_firsthscrc) + (mdr_b_functional_firsthscrc))) /\ ((mdr_e_functional_firsthscrc = ((mdr_p_functional_firsthsc) + (mdr_n_functional_firsthsc)) * S ((mdr_p_functional_firsthsc) + (mdr_n_functional_firsthsc)) + ((mdr_n_functional_firsthsc) + (mdr_n_functional_firsthsc))) /\ ((mdr_f_functional_firsthscrc = ((mdr_ut_functional_firsthsc) + (mdr_e_functional_firsthscrc)) * S ((mdr_ut_functional_firsthsc) + (mdr_e_functional_firsthscrc)) + ((mdr_e_functional_firsthscrc) + (mdr_e_functional_firsthscrc))) /\ ((mdr_z_functional_firsthscr) = ((mdr_c_functional_firsthscrc) + (mdr_f_functional_firsthscrc)) * S ((mdr_c_functional_firsthscrc) + (mdr_f_functional_firsthscrc)) + ((mdr_f_functional_firsthscrc) + (mdr_f_functional_firsthscrc))))))))) /\ (((exists ff_h_mdr_functional_firsthscrb. ff_h_mdr_functional_firsthscrb + S (mdr_z_functional_firsthscr) = S ((S (mdr_i_functional_firsthsc)) * mdr_c_functional_first)) /\ exists ff_q_mdr_functional_firsthscrb. mdr_b_functional_first = ff_q_mdr_functional_firsthscrb * S ((S (mdr_i_functional_firsthsc)) * mdr_c_functional_first) + (mdr_z_functional_firsthscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_functional_firsthscm_positive. (exists ff_gap_mdm_lt_mdr_functional_firsthscm_positive_index_bound. ff_gap_mdm_lt_mdr_functional_firsthscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_functional_firsthscm_positive) = ((mdr_q_functional_firsths) * (mdr_q_functional_firsths))) -> exists ff_row_mdm_prefix_mdr_functional_firsthscm_positive ff_column_mdm_prefix_mdr_functional_firsthscm_positive ff_value_mdm_prefix_mdr_functional_firsthscm_positive. (ff_index_mdm_prefix_mdr_functional_firsthscm_positive = (mdr_q_functional_firsths) * ff_row_mdm_prefix_mdr_functional_firsthscm_positive + ff_column_mdm_prefix_mdr_functional_firsthscm_positive /\ ((exists ff_gap_mdm_lt_mdr_functional_firsthscm_positive_column_bound. ff_gap_mdm_lt_mdr_functional_firsthscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_functional_firsthscm_positive) = (mdr_q_functional_firsths)) /\ ((exists ff_row_mdm_cell_mdr_functional_firsthscm_positive_cell ff_column_mdm_cell_mdr_functional_firsthscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_functional_firsthscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_functional_firsthscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_functional_firsthscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_functional_firsthscm_positive_cell = ff_row_mdm_prefix_mdr_functional_firsthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_functional_firsthscm_positive_cell_row_after. ff_gap_mdm_le_mdr_functional_firsthscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_functional_firsthscm_positive)) /\ ff_row_mdm_cell_mdr_functional_firsthscm_positive_cell = S ff_row_mdm_prefix_mdr_functional_firsthscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_functional_firsthscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_functional_firsthscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_functional_firsthscm_positive) = (mdr_j_functional_firsthsc)) /\ ff_column_mdm_cell_mdr_functional_firsthscm_positive_cell = ff_column_mdm_prefix_mdr_functional_firsthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_functional_firsthscm_positive_cell_column_after. ff_gap_mdm_le_mdr_functional_firsthscm_positive_cell_column_after + (mdr_j_functional_firsthsc) = (ff_column_mdm_prefix_mdr_functional_firsthscm_positive)) /\ ff_column_mdm_cell_mdr_functional_firsthscm_positive_cell = S ff_column_mdm_prefix_mdr_functional_firsthscm_positive))) /\ (((exists ff_h_mdm_mdr_functional_firsthscm_positive_cell_source. ff_h_mdm_mdr_functional_firsthscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_functional_firsthscm_positive) = S ((S ((ff_row_mdm_cell_mdr_functional_firsthscm_positive_cell) * (S (mdr_q_functional_firsths)) + (ff_column_mdm_cell_mdr_functional_firsthscm_positive_cell))) * mdr_pc_functional_firsth)) /\ exists ff_q_mdm_mdr_functional_firsthscm_positive_cell_source. mdr_pb_functional_firsth = ff_q_mdm_mdr_functional_firsthscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_functional_firsthscm_positive_cell) * (S (mdr_q_functional_firsths)) + (ff_column_mdm_cell_mdr_functional_firsthscm_positive_cell))) * mdr_pc_functional_firsth) + (ff_value_mdm_prefix_mdr_functional_firsthscm_positive)))))) /\ (((exists ff_h_mdm_mdr_functional_firsthscm_positive_target. ff_h_mdm_mdr_functional_firsthscm_positive_target + S (ff_value_mdm_prefix_mdr_functional_firsthscm_positive) = S ((S (ff_index_mdm_prefix_mdr_functional_firsthscm_positive)) * mdr_us_functional_firsthsc)) /\ exists ff_q_mdm_mdr_functional_firsthscm_positive_target. mdr_up_functional_firsthsc = ff_q_mdm_mdr_functional_firsthscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_functional_firsthscm_positive)) * mdr_us_functional_firsthsc) + (ff_value_mdm_prefix_mdr_functional_firsthscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_functional_firsthscm_negative. (exists ff_gap_mdm_lt_mdr_functional_firsthscm_negative_index_bound. ff_gap_mdm_lt_mdr_functional_firsthscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_functional_firsthscm_negative) = ((mdr_q_functional_firsths) * (mdr_q_functional_firsths))) -> exists ff_row_mdm_prefix_mdr_functional_firsthscm_negative ff_column_mdm_prefix_mdr_functional_firsthscm_negative ff_value_mdm_prefix_mdr_functional_firsthscm_negative. (ff_index_mdm_prefix_mdr_functional_firsthscm_negative = (mdr_q_functional_firsths) * ff_row_mdm_prefix_mdr_functional_firsthscm_negative + ff_column_mdm_prefix_mdr_functional_firsthscm_negative /\ ((exists ff_gap_mdm_lt_mdr_functional_firsthscm_negative_column_bound. ff_gap_mdm_lt_mdr_functional_firsthscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_functional_firsthscm_negative) = (mdr_q_functional_firsths)) /\ ((exists ff_row_mdm_cell_mdr_functional_firsthscm_negative_cell ff_column_mdm_cell_mdr_functional_firsthscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_functional_firsthscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_functional_firsthscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_functional_firsthscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_functional_firsthscm_negative_cell = ff_row_mdm_prefix_mdr_functional_firsthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_functional_firsthscm_negative_cell_row_after. ff_gap_mdm_le_mdr_functional_firsthscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_functional_firsthscm_negative)) /\ ff_row_mdm_cell_mdr_functional_firsthscm_negative_cell = S ff_row_mdm_prefix_mdr_functional_firsthscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_functional_firsthscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_functional_firsthscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_functional_firsthscm_negative) = (mdr_j_functional_firsthsc)) /\ ff_column_mdm_cell_mdr_functional_firsthscm_negative_cell = ff_column_mdm_prefix_mdr_functional_firsthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_functional_firsthscm_negative_cell_column_after. ff_gap_mdm_le_mdr_functional_firsthscm_negative_cell_column_after + (mdr_j_functional_firsthsc) = (ff_column_mdm_prefix_mdr_functional_firsthscm_negative)) /\ ff_column_mdm_cell_mdr_functional_firsthscm_negative_cell = S ff_column_mdm_prefix_mdr_functional_firsthscm_negative))) /\ (((exists ff_h_mdm_mdr_functional_firsthscm_negative_cell_source. ff_h_mdm_mdr_functional_firsthscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_functional_firsthscm_negative) = S ((S ((ff_row_mdm_cell_mdr_functional_firsthscm_negative_cell) * (S (mdr_q_functional_firsths)) + (ff_column_mdm_cell_mdr_functional_firsthscm_negative_cell))) * mdr_nc_functional_firsth)) /\ exists ff_q_mdm_mdr_functional_firsthscm_negative_cell_source. mdr_nb_functional_firsth = ff_q_mdm_mdr_functional_firsthscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_functional_firsthscm_negative_cell) * (S (mdr_q_functional_firsths)) + (ff_column_mdm_cell_mdr_functional_firsthscm_negative_cell))) * mdr_nc_functional_firsth) + (ff_value_mdm_prefix_mdr_functional_firsthscm_negative)))))) /\ (((exists ff_h_mdm_mdr_functional_firsthscm_negative_target. ff_h_mdm_mdr_functional_firsthscm_negative_target + S (ff_value_mdm_prefix_mdr_functional_firsthscm_negative) = S ((S (ff_index_mdm_prefix_mdr_functional_firsthscm_negative)) * mdr_ut_functional_firsthsc)) /\ exists ff_q_mdm_mdr_functional_firsthscm_negative_target. mdr_un_functional_firsthsc = ff_q_mdm_mdr_functional_firsthscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_functional_firsthscm_negative)) * mdr_ut_functional_firsthsc) + (ff_value_mdm_prefix_mdr_functional_firsthscm_negative))))))))) /\ ((((exists ff_h_mdr_functional_firsthscp. ff_h_mdr_functional_firsthscp + S (mdr_p_functional_firsthsc) = S ((S (mdr_j_functional_firsthsc)) * mdr_ec_functional_firsths)) /\ exists ff_q_mdr_functional_firsthscp. mdr_eb_functional_firsths = ff_q_mdr_functional_firsthscp * S ((S (mdr_j_functional_firsthsc)) * mdr_ec_functional_firsths) + (mdr_p_functional_firsthsc))) /\ (((exists ff_h_mdr_functional_firsthscn. ff_h_mdr_functional_firsthscn + S (mdr_n_functional_firsthsc) = S ((S (mdr_j_functional_firsthsc)) * mdr_fc_functional_firsths)) /\ exists ff_q_mdr_functional_firsthscn. mdr_fb_functional_firsths = ff_q_mdr_functional_firsthscn * S ((S (mdr_j_functional_firsthsc)) * mdr_fc_functional_firsths) + (mdr_n_functional_firsthsc)))))))) /\ (exists ff_ub_mce_fold_mdr_functional_firsthsf ff_uc_mce_fold_mdr_functional_firsthsf ff_vb_mce_fold_mdr_functional_firsthsf ff_vc_mce_fold_mdr_functional_firsthsf. ((forall ff_index_mce_alternating_mdr_functional_firsthsf_prefix. (exists ff_gap_mce_mdr_functional_firsthsf_prefix_index. ff_gap_mce_mdr_functional_firsthsf_prefix_index + S (ff_index_mce_alternating_mdr_functional_firsthsf_prefix) = (S (mdr_q_functional_firsths))) -> exists ff_ap_mce_alternating_mdr_functional_firsthsf_prefix ff_an_mce_alternating_mdr_functional_firsthsf_prefix ff_bp_mce_alternating_mdr_functional_firsthsf_prefix ff_bn_mce_alternating_mdr_functional_firsthsf_prefix ff_p_mce_alternating_mdr_functional_firsthsf_prefix ff_n_mce_alternating_mdr_functional_firsthsf_prefix. ((((exists ff_h_mce_mdr_functional_firsthsf_prefix_ap. ff_h_mce_mdr_functional_firsthsf_prefix_ap + S (ff_ap_mce_alternating_mdr_functional_firsthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_functional_firsthsf_prefix)) * mdr_pc_functional_firsth)) /\ exists ff_q_mce_mdr_functional_firsthsf_prefix_ap. mdr_pb_functional_firsth = ff_q_mce_mdr_functional_firsthsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_functional_firsthsf_prefix)) * mdr_pc_functional_firsth) + (ff_ap_mce_alternating_mdr_functional_firsthsf_prefix))) /\ ((((exists ff_h_mce_mdr_functional_firsthsf_prefix_an. ff_h_mce_mdr_functional_firsthsf_prefix_an + S (ff_an_mce_alternating_mdr_functional_firsthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_functional_firsthsf_prefix)) * mdr_nc_functional_firsth)) /\ exists ff_q_mce_mdr_functional_firsthsf_prefix_an. mdr_nb_functional_firsth = ff_q_mce_mdr_functional_firsthsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_functional_firsthsf_prefix)) * mdr_nc_functional_firsth) + (ff_an_mce_alternating_mdr_functional_firsthsf_prefix))) /\ ((((exists ff_h_mce_mdr_functional_firsthsf_prefix_bp. ff_h_mce_mdr_functional_firsthsf_prefix_bp + S (ff_bp_mce_alternating_mdr_functional_firsthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_functional_firsthsf_prefix)) * mdr_ec_functional_firsths)) /\ exists ff_q_mce_mdr_functional_firsthsf_prefix_bp. mdr_eb_functional_firsths = ff_q_mce_mdr_functional_firsthsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_functional_firsthsf_prefix)) * mdr_ec_functional_firsths) + (ff_bp_mce_alternating_mdr_functional_firsthsf_prefix))) /\ ((((exists ff_h_mce_mdr_functional_firsthsf_prefix_bn. ff_h_mce_mdr_functional_firsthsf_prefix_bn + S (ff_bn_mce_alternating_mdr_functional_firsthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_functional_firsthsf_prefix)) * mdr_fc_functional_firsths)) /\ exists ff_q_mce_mdr_functional_firsthsf_prefix_bn. mdr_fb_functional_firsths = ff_q_mce_mdr_functional_firsthsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_functional_firsthsf_prefix)) * mdr_fc_functional_firsths) + (ff_bn_mce_alternating_mdr_functional_firsthsf_prefix))) /\ ((((exists ff_h_mce_mdr_functional_firsthsf_prefix_positive. ff_h_mce_mdr_functional_firsthsf_prefix_positive + S (ff_p_mce_alternating_mdr_functional_firsthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_functional_firsthsf_prefix)) * ff_uc_mce_fold_mdr_functional_firsthsf)) /\ exists ff_q_mce_mdr_functional_firsthsf_prefix_positive. ff_ub_mce_fold_mdr_functional_firsthsf = ff_q_mce_mdr_functional_firsthsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_functional_firsthsf_prefix)) * ff_uc_mce_fold_mdr_functional_firsthsf) + (ff_p_mce_alternating_mdr_functional_firsthsf_prefix))) /\ ((((exists ff_h_mce_mdr_functional_firsthsf_prefix_negative. ff_h_mce_mdr_functional_firsthsf_prefix_negative + S (ff_n_mce_alternating_mdr_functional_firsthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_functional_firsthsf_prefix)) * ff_vc_mce_fold_mdr_functional_firsthsf)) /\ exists ff_q_mce_mdr_functional_firsthsf_prefix_negative. ff_vb_mce_fold_mdr_functional_firsthsf = ff_q_mce_mdr_functional_firsthsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_functional_firsthsf_prefix)) * ff_vc_mce_fold_mdr_functional_firsthsf) + (ff_n_mce_alternating_mdr_functional_firsthsf_prefix))) /\ (((exists ff_even_mce_term_mdr_functional_firsthsf_prefix_term. ff_index_mce_alternating_mdr_functional_firsthsf_prefix = 2 * ff_even_mce_term_mdr_functional_firsthsf_prefix_term) /\ (ff_p_mce_alternating_mdr_functional_firsthsf_prefix = (ff_ap_mce_alternating_mdr_functional_firsthsf_prefix) * (ff_bp_mce_alternating_mdr_functional_firsthsf_prefix) + (ff_an_mce_alternating_mdr_functional_firsthsf_prefix) * (ff_bn_mce_alternating_mdr_functional_firsthsf_prefix) /\ ff_n_mce_alternating_mdr_functional_firsthsf_prefix = (ff_ap_mce_alternating_mdr_functional_firsthsf_prefix) * (ff_bn_mce_alternating_mdr_functional_firsthsf_prefix) + (ff_an_mce_alternating_mdr_functional_firsthsf_prefix) * (ff_bp_mce_alternating_mdr_functional_firsthsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_functional_firsthsf_prefix_term. ff_index_mce_alternating_mdr_functional_firsthsf_prefix = 2 * ff_odd_mce_term_mdr_functional_firsthsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_functional_firsthsf_prefix = (ff_ap_mce_alternating_mdr_functional_firsthsf_prefix) * (ff_bn_mce_alternating_mdr_functional_firsthsf_prefix) + (ff_an_mce_alternating_mdr_functional_firsthsf_prefix) * (ff_bp_mce_alternating_mdr_functional_firsthsf_prefix) /\ ff_n_mce_alternating_mdr_functional_firsthsf_prefix = (ff_ap_mce_alternating_mdr_functional_firsthsf_prefix) * (ff_bp_mce_alternating_mdr_functional_firsthsf_prefix) + (ff_an_mce_alternating_mdr_functional_firsthsf_prefix) * (ff_bn_mce_alternating_mdr_functional_firsthsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_functional_firsthsf_positive ff_v_mce_mdr_functional_firsthsf_positive. ((((exists ff_h_mce_mdr_functional_firsthsf_positive_start. ff_h_mce_mdr_functional_firsthsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_functional_firsthsf_positive)) /\ exists ff_q_mce_mdr_functional_firsthsf_positive_start. ff_u_mce_mdr_functional_firsthsf_positive = ff_q_mce_mdr_functional_firsthsf_positive_start * S ((S (0)) * ff_v_mce_mdr_functional_firsthsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_functional_firsthsf_positive_terminal. ff_h_mce_mdr_functional_firsthsf_positive_terminal + S (mdr_p_functional_firsth) = S ((S ((S (mdr_q_functional_firsths)))) * ff_v_mce_mdr_functional_firsthsf_positive)) /\ exists ff_q_mce_mdr_functional_firsthsf_positive_terminal. ff_u_mce_mdr_functional_firsthsf_positive = ff_q_mce_mdr_functional_firsthsf_positive_terminal * S ((S ((S (mdr_q_functional_firsths)))) * ff_v_mce_mdr_functional_firsthsf_positive) + (mdr_p_functional_firsth))) /\ forall ff_i_mce_mdr_functional_firsthsf_positive. (exists ff_lt_mce_mdr_functional_firsthsf_positive_bound. ff_lt_mce_mdr_functional_firsthsf_positive_bound + S ff_i_mce_mdr_functional_firsthsf_positive = (S (mdr_q_functional_firsths))) -> exists ff_a_mce_mdr_functional_firsthsf_positive ff_r_mce_mdr_functional_firsthsf_positive ff_s_mce_mdr_functional_firsthsf_positive. ((((exists ff_h_mce_mdr_functional_firsthsf_positive_summand. ff_h_mce_mdr_functional_firsthsf_positive_summand + S (ff_a_mce_mdr_functional_firsthsf_positive) = S ((S (ff_i_mce_mdr_functional_firsthsf_positive)) * ff_uc_mce_fold_mdr_functional_firsthsf)) /\ exists ff_q_mce_mdr_functional_firsthsf_positive_summand. ff_ub_mce_fold_mdr_functional_firsthsf = ff_q_mce_mdr_functional_firsthsf_positive_summand * S ((S (ff_i_mce_mdr_functional_firsthsf_positive)) * ff_uc_mce_fold_mdr_functional_firsthsf) + (ff_a_mce_mdr_functional_firsthsf_positive))) /\ ((((exists ff_h_mce_mdr_functional_firsthsf_positive_partial. ff_h_mce_mdr_functional_firsthsf_positive_partial + S (ff_r_mce_mdr_functional_firsthsf_positive) = S ((S (ff_i_mce_mdr_functional_firsthsf_positive)) * ff_v_mce_mdr_functional_firsthsf_positive)) /\ exists ff_q_mce_mdr_functional_firsthsf_positive_partial. ff_u_mce_mdr_functional_firsthsf_positive = ff_q_mce_mdr_functional_firsthsf_positive_partial * S ((S (ff_i_mce_mdr_functional_firsthsf_positive)) * ff_v_mce_mdr_functional_firsthsf_positive) + (ff_r_mce_mdr_functional_firsthsf_positive))) /\ ((((exists ff_h_mce_mdr_functional_firsthsf_positive_successor. ff_h_mce_mdr_functional_firsthsf_positive_successor + S (ff_s_mce_mdr_functional_firsthsf_positive) = S ((S (S ff_i_mce_mdr_functional_firsthsf_positive)) * ff_v_mce_mdr_functional_firsthsf_positive)) /\ exists ff_q_mce_mdr_functional_firsthsf_positive_successor. ff_u_mce_mdr_functional_firsthsf_positive = ff_q_mce_mdr_functional_firsthsf_positive_successor * S ((S (S ff_i_mce_mdr_functional_firsthsf_positive)) * ff_v_mce_mdr_functional_firsthsf_positive) + (ff_s_mce_mdr_functional_firsthsf_positive))) /\ ff_s_mce_mdr_functional_firsthsf_positive = ff_r_mce_mdr_functional_firsthsf_positive + ff_a_mce_mdr_functional_firsthsf_positive)))))) /\ (exists ff_u_mce_mdr_functional_firsthsf_negative ff_v_mce_mdr_functional_firsthsf_negative. ((((exists ff_h_mce_mdr_functional_firsthsf_negative_start. ff_h_mce_mdr_functional_firsthsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_functional_firsthsf_negative)) /\ exists ff_q_mce_mdr_functional_firsthsf_negative_start. ff_u_mce_mdr_functional_firsthsf_negative = ff_q_mce_mdr_functional_firsthsf_negative_start * S ((S (0)) * ff_v_mce_mdr_functional_firsthsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_functional_firsthsf_negative_terminal. ff_h_mce_mdr_functional_firsthsf_negative_terminal + S (mdr_n_functional_firsth) = S ((S ((S (mdr_q_functional_firsths)))) * ff_v_mce_mdr_functional_firsthsf_negative)) /\ exists ff_q_mce_mdr_functional_firsthsf_negative_terminal. ff_u_mce_mdr_functional_firsthsf_negative = ff_q_mce_mdr_functional_firsthsf_negative_terminal * S ((S ((S (mdr_q_functional_firsths)))) * ff_v_mce_mdr_functional_firsthsf_negative) + (mdr_n_functional_firsth))) /\ forall ff_i_mce_mdr_functional_firsthsf_negative. (exists ff_lt_mce_mdr_functional_firsthsf_negative_bound. ff_lt_mce_mdr_functional_firsthsf_negative_bound + S ff_i_mce_mdr_functional_firsthsf_negative = (S (mdr_q_functional_firsths))) -> exists ff_a_mce_mdr_functional_firsthsf_negative ff_r_mce_mdr_functional_firsthsf_negative ff_s_mce_mdr_functional_firsthsf_negative. ((((exists ff_h_mce_mdr_functional_firsthsf_negative_summand. ff_h_mce_mdr_functional_firsthsf_negative_summand + S (ff_a_mce_mdr_functional_firsthsf_negative) = S ((S (ff_i_mce_mdr_functional_firsthsf_negative)) * ff_vc_mce_fold_mdr_functional_firsthsf)) /\ exists ff_q_mce_mdr_functional_firsthsf_negative_summand. ff_vb_mce_fold_mdr_functional_firsthsf = ff_q_mce_mdr_functional_firsthsf_negative_summand * S ((S (ff_i_mce_mdr_functional_firsthsf_negative)) * ff_vc_mce_fold_mdr_functional_firsthsf) + (ff_a_mce_mdr_functional_firsthsf_negative))) /\ ((((exists ff_h_mce_mdr_functional_firsthsf_negative_partial. ff_h_mce_mdr_functional_firsthsf_negative_partial + S (ff_r_mce_mdr_functional_firsthsf_negative) = S ((S (ff_i_mce_mdr_functional_firsthsf_negative)) * ff_v_mce_mdr_functional_firsthsf_negative)) /\ exists ff_q_mce_mdr_functional_firsthsf_negative_partial. ff_u_mce_mdr_functional_firsthsf_negative = ff_q_mce_mdr_functional_firsthsf_negative_partial * S ((S (ff_i_mce_mdr_functional_firsthsf_negative)) * ff_v_mce_mdr_functional_firsthsf_negative) + (ff_r_mce_mdr_functional_firsthsf_negative))) /\ ((((exists ff_h_mce_mdr_functional_firsthsf_negative_successor. ff_h_mce_mdr_functional_firsthsf_negative_successor + S (ff_s_mce_mdr_functional_firsthsf_negative) = S ((S (S ff_i_mce_mdr_functional_firsthsf_negative)) * ff_v_mce_mdr_functional_firsthsf_negative)) /\ exists ff_q_mce_mdr_functional_firsthsf_negative_successor. ff_u_mce_mdr_functional_firsthsf_negative = ff_q_mce_mdr_functional_firsthsf_negative_successor * S ((S (S ff_i_mce_mdr_functional_firsthsf_negative)) * ff_v_mce_mdr_functional_firsthsf_negative) + (ff_s_mce_mdr_functional_firsthsf_negative))) /\ ff_s_mce_mdr_functional_firsthsf_negative = ff_r_mce_mdr_functional_firsthsf_negative + ff_a_mce_mdr_functional_firsthsf_negative))))))))))))))) /\ ((exists mdr_gap_functional_firsti. mdr_gap_functional_firsti + S (mdr_i_functional_first) = (mdr_l_functional_first)) /\ (exists mdr_z_functional_firstr. ((exists mdr_a_functional_firstrc mdr_b_functional_firstrc mdr_c_functional_firstrc mdr_e_functional_firstrc mdr_f_functional_firstrc. ((mdr_a_functional_firstrc = ((d) + (pb)) * S ((d) + (pb)) + ((pb) + (pb))) /\ ((mdr_b_functional_firstrc = ((pc) + (nb)) * S ((pc) + (nb)) + ((nb) + (nb))) /\ ((mdr_c_functional_firstrc = ((mdr_a_functional_firstrc) + (mdr_b_functional_firstrc)) * S ((mdr_a_functional_firstrc) + (mdr_b_functional_firstrc)) + ((mdr_b_functional_firstrc) + (mdr_b_functional_firstrc))) /\ ((mdr_e_functional_firstrc = ((p) + (n)) * S ((p) + (n)) + ((n) + (n))) /\ ((mdr_f_functional_firstrc = ((nc) + (mdr_e_functional_firstrc)) * S ((nc) + (mdr_e_functional_firstrc)) + ((mdr_e_functional_firstrc) + (mdr_e_functional_firstrc))) /\ ((mdr_z_functional_firstr) = ((mdr_c_functional_firstrc) + (mdr_f_functional_firstrc)) * S ((mdr_c_functional_firstrc) + (mdr_f_functional_firstrc)) + ((mdr_f_functional_firstrc) + (mdr_f_functional_firstrc))))))))) /\ (((exists ff_h_mdr_functional_firstrb. ff_h_mdr_functional_firstrb + S (mdr_z_functional_firstr) = S ((S (mdr_i_functional_first)) * mdr_c_functional_first)) /\ exists ff_q_mdr_functional_firstrb. mdr_b_functional_first = ff_q_mdr_functional_firstrb * S ((S (mdr_i_functional_first)) * mdr_c_functional_first) + (mdr_z_functional_firstr)))))))) -> (exists mdr_b_functional_second mdr_c_functional_second mdr_l_functional_second mdr_i_functional_second. ((forall mdr_i_functional_secondh. (exists mdr_gap_functional_secondhi. mdr_gap_functional_secondhi + S (mdr_i_functional_secondh) = (mdr_l_functional_second)) -> exists mdr_d_functional_secondh mdr_pb_functional_secondh mdr_pc_functional_secondh mdr_nb_functional_secondh mdr_nc_functional_secondh mdr_p_functional_secondh mdr_n_functional_secondh. ((exists mdr_z_functional_secondhr. ((exists mdr_a_functional_secondhrc mdr_b_functional_secondhrc mdr_c_functional_secondhrc mdr_e_functional_secondhrc mdr_f_functional_secondhrc. ((mdr_a_functional_secondhrc = ((mdr_d_functional_secondh) + (mdr_pb_functional_secondh)) * S ((mdr_d_functional_secondh) + (mdr_pb_functional_secondh)) + ((mdr_pb_functional_secondh) + (mdr_pb_functional_secondh))) /\ ((mdr_b_functional_secondhrc = ((mdr_pc_functional_secondh) + (mdr_nb_functional_secondh)) * S ((mdr_pc_functional_secondh) + (mdr_nb_functional_secondh)) + ((mdr_nb_functional_secondh) + (mdr_nb_functional_secondh))) /\ ((mdr_c_functional_secondhrc = ((mdr_a_functional_secondhrc) + (mdr_b_functional_secondhrc)) * S ((mdr_a_functional_secondhrc) + (mdr_b_functional_secondhrc)) + ((mdr_b_functional_secondhrc) + (mdr_b_functional_secondhrc))) /\ ((mdr_e_functional_secondhrc = ((mdr_p_functional_secondh) + (mdr_n_functional_secondh)) * S ((mdr_p_functional_secondh) + (mdr_n_functional_secondh)) + ((mdr_n_functional_secondh) + (mdr_n_functional_secondh))) /\ ((mdr_f_functional_secondhrc = ((mdr_nc_functional_secondh) + (mdr_e_functional_secondhrc)) * S ((mdr_nc_functional_secondh) + (mdr_e_functional_secondhrc)) + ((mdr_e_functional_secondhrc) + (mdr_e_functional_secondhrc))) /\ ((mdr_z_functional_secondhr) = ((mdr_c_functional_secondhrc) + (mdr_f_functional_secondhrc)) * S ((mdr_c_functional_secondhrc) + (mdr_f_functional_secondhrc)) + ((mdr_f_functional_secondhrc) + (mdr_f_functional_secondhrc))))))))) /\ (((exists ff_h_mdr_functional_secondhrb. ff_h_mdr_functional_secondhrb + S (mdr_z_functional_secondhr) = S ((S (mdr_i_functional_secondh)) * mdr_c_functional_second)) /\ exists ff_q_mdr_functional_secondhrb. mdr_b_functional_second = ff_q_mdr_functional_secondhrb * S ((S (mdr_i_functional_secondh)) * mdr_c_functional_second) + (mdr_z_functional_secondhr))))) /\ (((((mdr_d_functional_secondh) = 0) /\ (((mdr_p_functional_secondh) = 1) /\ ((mdr_n_functional_secondh) = 0))) \/ exists mdr_q_functional_secondhs mdr_eb_functional_secondhs mdr_ec_functional_secondhs mdr_fb_functional_secondhs mdr_fc_functional_secondhs. (((mdr_d_functional_secondh) = S (mdr_q_functional_secondhs)) /\ ((forall mdr_j_functional_secondhsc. (exists mdr_gap_functional_secondhscj. mdr_gap_functional_secondhscj + S (mdr_j_functional_secondhsc) = (S (mdr_q_functional_secondhs))) -> exists mdr_i_functional_secondhsc mdr_up_functional_secondhsc mdr_us_functional_secondhsc mdr_un_functional_secondhsc mdr_ut_functional_secondhsc mdr_p_functional_secondhsc mdr_n_functional_secondhsc. ((exists mdr_gap_functional_secondhsci. mdr_gap_functional_secondhsci + S (mdr_i_functional_secondhsc) = (mdr_i_functional_secondh)) /\ ((exists mdr_z_functional_secondhscr. ((exists mdr_a_functional_secondhscrc mdr_b_functional_secondhscrc mdr_c_functional_secondhscrc mdr_e_functional_secondhscrc mdr_f_functional_secondhscrc. ((mdr_a_functional_secondhscrc = ((mdr_q_functional_secondhs) + (mdr_up_functional_secondhsc)) * S ((mdr_q_functional_secondhs) + (mdr_up_functional_secondhsc)) + ((mdr_up_functional_secondhsc) + (mdr_up_functional_secondhsc))) /\ ((mdr_b_functional_secondhscrc = ((mdr_us_functional_secondhsc) + (mdr_un_functional_secondhsc)) * S ((mdr_us_functional_secondhsc) + (mdr_un_functional_secondhsc)) + ((mdr_un_functional_secondhsc) + (mdr_un_functional_secondhsc))) /\ ((mdr_c_functional_secondhscrc = ((mdr_a_functional_secondhscrc) + (mdr_b_functional_secondhscrc)) * S ((mdr_a_functional_secondhscrc) + (mdr_b_functional_secondhscrc)) + ((mdr_b_functional_secondhscrc) + (mdr_b_functional_secondhscrc))) /\ ((mdr_e_functional_secondhscrc = ((mdr_p_functional_secondhsc) + (mdr_n_functional_secondhsc)) * S ((mdr_p_functional_secondhsc) + (mdr_n_functional_secondhsc)) + ((mdr_n_functional_secondhsc) + (mdr_n_functional_secondhsc))) /\ ((mdr_f_functional_secondhscrc = ((mdr_ut_functional_secondhsc) + (mdr_e_functional_secondhscrc)) * S ((mdr_ut_functional_secondhsc) + (mdr_e_functional_secondhscrc)) + ((mdr_e_functional_secondhscrc) + (mdr_e_functional_secondhscrc))) /\ ((mdr_z_functional_secondhscr) = ((mdr_c_functional_secondhscrc) + (mdr_f_functional_secondhscrc)) * S ((mdr_c_functional_secondhscrc) + (mdr_f_functional_secondhscrc)) + ((mdr_f_functional_secondhscrc) + (mdr_f_functional_secondhscrc))))))))) /\ (((exists ff_h_mdr_functional_secondhscrb. ff_h_mdr_functional_secondhscrb + S (mdr_z_functional_secondhscr) = S ((S (mdr_i_functional_secondhsc)) * mdr_c_functional_second)) /\ exists ff_q_mdr_functional_secondhscrb. mdr_b_functional_second = ff_q_mdr_functional_secondhscrb * S ((S (mdr_i_functional_secondhsc)) * mdr_c_functional_second) + (mdr_z_functional_secondhscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_functional_secondhscm_positive. (exists ff_gap_mdm_lt_mdr_functional_secondhscm_positive_index_bound. ff_gap_mdm_lt_mdr_functional_secondhscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_functional_secondhscm_positive) = ((mdr_q_functional_secondhs) * (mdr_q_functional_secondhs))) -> exists ff_row_mdm_prefix_mdr_functional_secondhscm_positive ff_column_mdm_prefix_mdr_functional_secondhscm_positive ff_value_mdm_prefix_mdr_functional_secondhscm_positive. (ff_index_mdm_prefix_mdr_functional_secondhscm_positive = (mdr_q_functional_secondhs) * ff_row_mdm_prefix_mdr_functional_secondhscm_positive + ff_column_mdm_prefix_mdr_functional_secondhscm_positive /\ ((exists ff_gap_mdm_lt_mdr_functional_secondhscm_positive_column_bound. ff_gap_mdm_lt_mdr_functional_secondhscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_functional_secondhscm_positive) = (mdr_q_functional_secondhs)) /\ ((exists ff_row_mdm_cell_mdr_functional_secondhscm_positive_cell ff_column_mdm_cell_mdr_functional_secondhscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_functional_secondhscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_functional_secondhscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_functional_secondhscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_functional_secondhscm_positive_cell = ff_row_mdm_prefix_mdr_functional_secondhscm_positive) \/ ((exists ff_gap_mdm_le_mdr_functional_secondhscm_positive_cell_row_after. ff_gap_mdm_le_mdr_functional_secondhscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_functional_secondhscm_positive)) /\ ff_row_mdm_cell_mdr_functional_secondhscm_positive_cell = S ff_row_mdm_prefix_mdr_functional_secondhscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_functional_secondhscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_functional_secondhscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_functional_secondhscm_positive) = (mdr_j_functional_secondhsc)) /\ ff_column_mdm_cell_mdr_functional_secondhscm_positive_cell = ff_column_mdm_prefix_mdr_functional_secondhscm_positive) \/ ((exists ff_gap_mdm_le_mdr_functional_secondhscm_positive_cell_column_after. ff_gap_mdm_le_mdr_functional_secondhscm_positive_cell_column_after + (mdr_j_functional_secondhsc) = (ff_column_mdm_prefix_mdr_functional_secondhscm_positive)) /\ ff_column_mdm_cell_mdr_functional_secondhscm_positive_cell = S ff_column_mdm_prefix_mdr_functional_secondhscm_positive))) /\ (((exists ff_h_mdm_mdr_functional_secondhscm_positive_cell_source. ff_h_mdm_mdr_functional_secondhscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_functional_secondhscm_positive) = S ((S ((ff_row_mdm_cell_mdr_functional_secondhscm_positive_cell) * (S (mdr_q_functional_secondhs)) + (ff_column_mdm_cell_mdr_functional_secondhscm_positive_cell))) * mdr_pc_functional_secondh)) /\ exists ff_q_mdm_mdr_functional_secondhscm_positive_cell_source. mdr_pb_functional_secondh = ff_q_mdm_mdr_functional_secondhscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_functional_secondhscm_positive_cell) * (S (mdr_q_functional_secondhs)) + (ff_column_mdm_cell_mdr_functional_secondhscm_positive_cell))) * mdr_pc_functional_secondh) + (ff_value_mdm_prefix_mdr_functional_secondhscm_positive)))))) /\ (((exists ff_h_mdm_mdr_functional_secondhscm_positive_target. ff_h_mdm_mdr_functional_secondhscm_positive_target + S (ff_value_mdm_prefix_mdr_functional_secondhscm_positive) = S ((S (ff_index_mdm_prefix_mdr_functional_secondhscm_positive)) * mdr_us_functional_secondhsc)) /\ exists ff_q_mdm_mdr_functional_secondhscm_positive_target. mdr_up_functional_secondhsc = ff_q_mdm_mdr_functional_secondhscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_functional_secondhscm_positive)) * mdr_us_functional_secondhsc) + (ff_value_mdm_prefix_mdr_functional_secondhscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_functional_secondhscm_negative. (exists ff_gap_mdm_lt_mdr_functional_secondhscm_negative_index_bound. ff_gap_mdm_lt_mdr_functional_secondhscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_functional_secondhscm_negative) = ((mdr_q_functional_secondhs) * (mdr_q_functional_secondhs))) -> exists ff_row_mdm_prefix_mdr_functional_secondhscm_negative ff_column_mdm_prefix_mdr_functional_secondhscm_negative ff_value_mdm_prefix_mdr_functional_secondhscm_negative. (ff_index_mdm_prefix_mdr_functional_secondhscm_negative = (mdr_q_functional_secondhs) * ff_row_mdm_prefix_mdr_functional_secondhscm_negative + ff_column_mdm_prefix_mdr_functional_secondhscm_negative /\ ((exists ff_gap_mdm_lt_mdr_functional_secondhscm_negative_column_bound. ff_gap_mdm_lt_mdr_functional_secondhscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_functional_secondhscm_negative) = (mdr_q_functional_secondhs)) /\ ((exists ff_row_mdm_cell_mdr_functional_secondhscm_negative_cell ff_column_mdm_cell_mdr_functional_secondhscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_functional_secondhscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_functional_secondhscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_functional_secondhscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_functional_secondhscm_negative_cell = ff_row_mdm_prefix_mdr_functional_secondhscm_negative) \/ ((exists ff_gap_mdm_le_mdr_functional_secondhscm_negative_cell_row_after. ff_gap_mdm_le_mdr_functional_secondhscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_functional_secondhscm_negative)) /\ ff_row_mdm_cell_mdr_functional_secondhscm_negative_cell = S ff_row_mdm_prefix_mdr_functional_secondhscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_functional_secondhscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_functional_secondhscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_functional_secondhscm_negative) = (mdr_j_functional_secondhsc)) /\ ff_column_mdm_cell_mdr_functional_secondhscm_negative_cell = ff_column_mdm_prefix_mdr_functional_secondhscm_negative) \/ ((exists ff_gap_mdm_le_mdr_functional_secondhscm_negative_cell_column_after. ff_gap_mdm_le_mdr_functional_secondhscm_negative_cell_column_after + (mdr_j_functional_secondhsc) = (ff_column_mdm_prefix_mdr_functional_secondhscm_negative)) /\ ff_column_mdm_cell_mdr_functional_secondhscm_negative_cell = S ff_column_mdm_prefix_mdr_functional_secondhscm_negative))) /\ (((exists ff_h_mdm_mdr_functional_secondhscm_negative_cell_source. ff_h_mdm_mdr_functional_secondhscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_functional_secondhscm_negative) = S ((S ((ff_row_mdm_cell_mdr_functional_secondhscm_negative_cell) * (S (mdr_q_functional_secondhs)) + (ff_column_mdm_cell_mdr_functional_secondhscm_negative_cell))) * mdr_nc_functional_secondh)) /\ exists ff_q_mdm_mdr_functional_secondhscm_negative_cell_source. mdr_nb_functional_secondh = ff_q_mdm_mdr_functional_secondhscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_functional_secondhscm_negative_cell) * (S (mdr_q_functional_secondhs)) + (ff_column_mdm_cell_mdr_functional_secondhscm_negative_cell))) * mdr_nc_functional_secondh) + (ff_value_mdm_prefix_mdr_functional_secondhscm_negative)))))) /\ (((exists ff_h_mdm_mdr_functional_secondhscm_negative_target. ff_h_mdm_mdr_functional_secondhscm_negative_target + S (ff_value_mdm_prefix_mdr_functional_secondhscm_negative) = S ((S (ff_index_mdm_prefix_mdr_functional_secondhscm_negative)) * mdr_ut_functional_secondhsc)) /\ exists ff_q_mdm_mdr_functional_secondhscm_negative_target. mdr_un_functional_secondhsc = ff_q_mdm_mdr_functional_secondhscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_functional_secondhscm_negative)) * mdr_ut_functional_secondhsc) + (ff_value_mdm_prefix_mdr_functional_secondhscm_negative))))))))) /\ ((((exists ff_h_mdr_functional_secondhscp. ff_h_mdr_functional_secondhscp + S (mdr_p_functional_secondhsc) = S ((S (mdr_j_functional_secondhsc)) * mdr_ec_functional_secondhs)) /\ exists ff_q_mdr_functional_secondhscp. mdr_eb_functional_secondhs = ff_q_mdr_functional_secondhscp * S ((S (mdr_j_functional_secondhsc)) * mdr_ec_functional_secondhs) + (mdr_p_functional_secondhsc))) /\ (((exists ff_h_mdr_functional_secondhscn. ff_h_mdr_functional_secondhscn + S (mdr_n_functional_secondhsc) = S ((S (mdr_j_functional_secondhsc)) * mdr_fc_functional_secondhs)) /\ exists ff_q_mdr_functional_secondhscn. mdr_fb_functional_secondhs = ff_q_mdr_functional_secondhscn * S ((S (mdr_j_functional_secondhsc)) * mdr_fc_functional_secondhs) + (mdr_n_functional_secondhsc)))))))) /\ (exists ff_ub_mce_fold_mdr_functional_secondhsf ff_uc_mce_fold_mdr_functional_secondhsf ff_vb_mce_fold_mdr_functional_secondhsf ff_vc_mce_fold_mdr_functional_secondhsf. ((forall ff_index_mce_alternating_mdr_functional_secondhsf_prefix. (exists ff_gap_mce_mdr_functional_secondhsf_prefix_index. ff_gap_mce_mdr_functional_secondhsf_prefix_index + S (ff_index_mce_alternating_mdr_functional_secondhsf_prefix) = (S (mdr_q_functional_secondhs))) -> exists ff_ap_mce_alternating_mdr_functional_secondhsf_prefix ff_an_mce_alternating_mdr_functional_secondhsf_prefix ff_bp_mce_alternating_mdr_functional_secondhsf_prefix ff_bn_mce_alternating_mdr_functional_secondhsf_prefix ff_p_mce_alternating_mdr_functional_secondhsf_prefix ff_n_mce_alternating_mdr_functional_secondhsf_prefix. ((((exists ff_h_mce_mdr_functional_secondhsf_prefix_ap. ff_h_mce_mdr_functional_secondhsf_prefix_ap + S (ff_ap_mce_alternating_mdr_functional_secondhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_functional_secondhsf_prefix)) * mdr_pc_functional_secondh)) /\ exists ff_q_mce_mdr_functional_secondhsf_prefix_ap. mdr_pb_functional_secondh = ff_q_mce_mdr_functional_secondhsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_functional_secondhsf_prefix)) * mdr_pc_functional_secondh) + (ff_ap_mce_alternating_mdr_functional_secondhsf_prefix))) /\ ((((exists ff_h_mce_mdr_functional_secondhsf_prefix_an. ff_h_mce_mdr_functional_secondhsf_prefix_an + S (ff_an_mce_alternating_mdr_functional_secondhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_functional_secondhsf_prefix)) * mdr_nc_functional_secondh)) /\ exists ff_q_mce_mdr_functional_secondhsf_prefix_an. mdr_nb_functional_secondh = ff_q_mce_mdr_functional_secondhsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_functional_secondhsf_prefix)) * mdr_nc_functional_secondh) + (ff_an_mce_alternating_mdr_functional_secondhsf_prefix))) /\ ((((exists ff_h_mce_mdr_functional_secondhsf_prefix_bp. ff_h_mce_mdr_functional_secondhsf_prefix_bp + S (ff_bp_mce_alternating_mdr_functional_secondhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_functional_secondhsf_prefix)) * mdr_ec_functional_secondhs)) /\ exists ff_q_mce_mdr_functional_secondhsf_prefix_bp. mdr_eb_functional_secondhs = ff_q_mce_mdr_functional_secondhsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_functional_secondhsf_prefix)) * mdr_ec_functional_secondhs) + (ff_bp_mce_alternating_mdr_functional_secondhsf_prefix))) /\ ((((exists ff_h_mce_mdr_functional_secondhsf_prefix_bn. ff_h_mce_mdr_functional_secondhsf_prefix_bn + S (ff_bn_mce_alternating_mdr_functional_secondhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_functional_secondhsf_prefix)) * mdr_fc_functional_secondhs)) /\ exists ff_q_mce_mdr_functional_secondhsf_prefix_bn. mdr_fb_functional_secondhs = ff_q_mce_mdr_functional_secondhsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_functional_secondhsf_prefix)) * mdr_fc_functional_secondhs) + (ff_bn_mce_alternating_mdr_functional_secondhsf_prefix))) /\ ((((exists ff_h_mce_mdr_functional_secondhsf_prefix_positive. ff_h_mce_mdr_functional_secondhsf_prefix_positive + S (ff_p_mce_alternating_mdr_functional_secondhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_functional_secondhsf_prefix)) * ff_uc_mce_fold_mdr_functional_secondhsf)) /\ exists ff_q_mce_mdr_functional_secondhsf_prefix_positive. ff_ub_mce_fold_mdr_functional_secondhsf = ff_q_mce_mdr_functional_secondhsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_functional_secondhsf_prefix)) * ff_uc_mce_fold_mdr_functional_secondhsf) + (ff_p_mce_alternating_mdr_functional_secondhsf_prefix))) /\ ((((exists ff_h_mce_mdr_functional_secondhsf_prefix_negative. ff_h_mce_mdr_functional_secondhsf_prefix_negative + S (ff_n_mce_alternating_mdr_functional_secondhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_functional_secondhsf_prefix)) * ff_vc_mce_fold_mdr_functional_secondhsf)) /\ exists ff_q_mce_mdr_functional_secondhsf_prefix_negative. ff_vb_mce_fold_mdr_functional_secondhsf = ff_q_mce_mdr_functional_secondhsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_functional_secondhsf_prefix)) * ff_vc_mce_fold_mdr_functional_secondhsf) + (ff_n_mce_alternating_mdr_functional_secondhsf_prefix))) /\ (((exists ff_even_mce_term_mdr_functional_secondhsf_prefix_term. ff_index_mce_alternating_mdr_functional_secondhsf_prefix = 2 * ff_even_mce_term_mdr_functional_secondhsf_prefix_term) /\ (ff_p_mce_alternating_mdr_functional_secondhsf_prefix = (ff_ap_mce_alternating_mdr_functional_secondhsf_prefix) * (ff_bp_mce_alternating_mdr_functional_secondhsf_prefix) + (ff_an_mce_alternating_mdr_functional_secondhsf_prefix) * (ff_bn_mce_alternating_mdr_functional_secondhsf_prefix) /\ ff_n_mce_alternating_mdr_functional_secondhsf_prefix = (ff_ap_mce_alternating_mdr_functional_secondhsf_prefix) * (ff_bn_mce_alternating_mdr_functional_secondhsf_prefix) + (ff_an_mce_alternating_mdr_functional_secondhsf_prefix) * (ff_bp_mce_alternating_mdr_functional_secondhsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_functional_secondhsf_prefix_term. ff_index_mce_alternating_mdr_functional_secondhsf_prefix = 2 * ff_odd_mce_term_mdr_functional_secondhsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_functional_secondhsf_prefix = (ff_ap_mce_alternating_mdr_functional_secondhsf_prefix) * (ff_bn_mce_alternating_mdr_functional_secondhsf_prefix) + (ff_an_mce_alternating_mdr_functional_secondhsf_prefix) * (ff_bp_mce_alternating_mdr_functional_secondhsf_prefix) /\ ff_n_mce_alternating_mdr_functional_secondhsf_prefix = (ff_ap_mce_alternating_mdr_functional_secondhsf_prefix) * (ff_bp_mce_alternating_mdr_functional_secondhsf_prefix) + (ff_an_mce_alternating_mdr_functional_secondhsf_prefix) * (ff_bn_mce_alternating_mdr_functional_secondhsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_functional_secondhsf_positive ff_v_mce_mdr_functional_secondhsf_positive. ((((exists ff_h_mce_mdr_functional_secondhsf_positive_start. ff_h_mce_mdr_functional_secondhsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_functional_secondhsf_positive)) /\ exists ff_q_mce_mdr_functional_secondhsf_positive_start. ff_u_mce_mdr_functional_secondhsf_positive = ff_q_mce_mdr_functional_secondhsf_positive_start * S ((S (0)) * ff_v_mce_mdr_functional_secondhsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_functional_secondhsf_positive_terminal. ff_h_mce_mdr_functional_secondhsf_positive_terminal + S (mdr_p_functional_secondh) = S ((S ((S (mdr_q_functional_secondhs)))) * ff_v_mce_mdr_functional_secondhsf_positive)) /\ exists ff_q_mce_mdr_functional_secondhsf_positive_terminal. ff_u_mce_mdr_functional_secondhsf_positive = ff_q_mce_mdr_functional_secondhsf_positive_terminal * S ((S ((S (mdr_q_functional_secondhs)))) * ff_v_mce_mdr_functional_secondhsf_positive) + (mdr_p_functional_secondh))) /\ forall ff_i_mce_mdr_functional_secondhsf_positive. (exists ff_lt_mce_mdr_functional_secondhsf_positive_bound. ff_lt_mce_mdr_functional_secondhsf_positive_bound + S ff_i_mce_mdr_functional_secondhsf_positive = (S (mdr_q_functional_secondhs))) -> exists ff_a_mce_mdr_functional_secondhsf_positive ff_r_mce_mdr_functional_secondhsf_positive ff_s_mce_mdr_functional_secondhsf_positive. ((((exists ff_h_mce_mdr_functional_secondhsf_positive_summand. ff_h_mce_mdr_functional_secondhsf_positive_summand + S (ff_a_mce_mdr_functional_secondhsf_positive) = S ((S (ff_i_mce_mdr_functional_secondhsf_positive)) * ff_uc_mce_fold_mdr_functional_secondhsf)) /\ exists ff_q_mce_mdr_functional_secondhsf_positive_summand. ff_ub_mce_fold_mdr_functional_secondhsf = ff_q_mce_mdr_functional_secondhsf_positive_summand * S ((S (ff_i_mce_mdr_functional_secondhsf_positive)) * ff_uc_mce_fold_mdr_functional_secondhsf) + (ff_a_mce_mdr_functional_secondhsf_positive))) /\ ((((exists ff_h_mce_mdr_functional_secondhsf_positive_partial. ff_h_mce_mdr_functional_secondhsf_positive_partial + S (ff_r_mce_mdr_functional_secondhsf_positive) = S ((S (ff_i_mce_mdr_functional_secondhsf_positive)) * ff_v_mce_mdr_functional_secondhsf_positive)) /\ exists ff_q_mce_mdr_functional_secondhsf_positive_partial. ff_u_mce_mdr_functional_secondhsf_positive = ff_q_mce_mdr_functional_secondhsf_positive_partial * S ((S (ff_i_mce_mdr_functional_secondhsf_positive)) * ff_v_mce_mdr_functional_secondhsf_positive) + (ff_r_mce_mdr_functional_secondhsf_positive))) /\ ((((exists ff_h_mce_mdr_functional_secondhsf_positive_successor. ff_h_mce_mdr_functional_secondhsf_positive_successor + S (ff_s_mce_mdr_functional_secondhsf_positive) = S ((S (S ff_i_mce_mdr_functional_secondhsf_positive)) * ff_v_mce_mdr_functional_secondhsf_positive)) /\ exists ff_q_mce_mdr_functional_secondhsf_positive_successor. ff_u_mce_mdr_functional_secondhsf_positive = ff_q_mce_mdr_functional_secondhsf_positive_successor * S ((S (S ff_i_mce_mdr_functional_secondhsf_positive)) * ff_v_mce_mdr_functional_secondhsf_positive) + (ff_s_mce_mdr_functional_secondhsf_positive))) /\ ff_s_mce_mdr_functional_secondhsf_positive = ff_r_mce_mdr_functional_secondhsf_positive + ff_a_mce_mdr_functional_secondhsf_positive)))))) /\ (exists ff_u_mce_mdr_functional_secondhsf_negative ff_v_mce_mdr_functional_secondhsf_negative. ((((exists ff_h_mce_mdr_functional_secondhsf_negative_start. ff_h_mce_mdr_functional_secondhsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_functional_secondhsf_negative)) /\ exists ff_q_mce_mdr_functional_secondhsf_negative_start. ff_u_mce_mdr_functional_secondhsf_negative = ff_q_mce_mdr_functional_secondhsf_negative_start * S ((S (0)) * ff_v_mce_mdr_functional_secondhsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_functional_secondhsf_negative_terminal. ff_h_mce_mdr_functional_secondhsf_negative_terminal + S (mdr_n_functional_secondh) = S ((S ((S (mdr_q_functional_secondhs)))) * ff_v_mce_mdr_functional_secondhsf_negative)) /\ exists ff_q_mce_mdr_functional_secondhsf_negative_terminal. ff_u_mce_mdr_functional_secondhsf_negative = ff_q_mce_mdr_functional_secondhsf_negative_terminal * S ((S ((S (mdr_q_functional_secondhs)))) * ff_v_mce_mdr_functional_secondhsf_negative) + (mdr_n_functional_secondh))) /\ forall ff_i_mce_mdr_functional_secondhsf_negative. (exists ff_lt_mce_mdr_functional_secondhsf_negative_bound. ff_lt_mce_mdr_functional_secondhsf_negative_bound + S ff_i_mce_mdr_functional_secondhsf_negative = (S (mdr_q_functional_secondhs))) -> exists ff_a_mce_mdr_functional_secondhsf_negative ff_r_mce_mdr_functional_secondhsf_negative ff_s_mce_mdr_functional_secondhsf_negative. ((((exists ff_h_mce_mdr_functional_secondhsf_negative_summand. ff_h_mce_mdr_functional_secondhsf_negative_summand + S (ff_a_mce_mdr_functional_secondhsf_negative) = S ((S (ff_i_mce_mdr_functional_secondhsf_negative)) * ff_vc_mce_fold_mdr_functional_secondhsf)) /\ exists ff_q_mce_mdr_functional_secondhsf_negative_summand. ff_vb_mce_fold_mdr_functional_secondhsf = ff_q_mce_mdr_functional_secondhsf_negative_summand * S ((S (ff_i_mce_mdr_functional_secondhsf_negative)) * ff_vc_mce_fold_mdr_functional_secondhsf) + (ff_a_mce_mdr_functional_secondhsf_negative))) /\ ((((exists ff_h_mce_mdr_functional_secondhsf_negative_partial. ff_h_mce_mdr_functional_secondhsf_negative_partial + S (ff_r_mce_mdr_functional_secondhsf_negative) = S ((S (ff_i_mce_mdr_functional_secondhsf_negative)) * ff_v_mce_mdr_functional_secondhsf_negative)) /\ exists ff_q_mce_mdr_functional_secondhsf_negative_partial. ff_u_mce_mdr_functional_secondhsf_negative = ff_q_mce_mdr_functional_secondhsf_negative_partial * S ((S (ff_i_mce_mdr_functional_secondhsf_negative)) * ff_v_mce_mdr_functional_secondhsf_negative) + (ff_r_mce_mdr_functional_secondhsf_negative))) /\ ((((exists ff_h_mce_mdr_functional_secondhsf_negative_successor. ff_h_mce_mdr_functional_secondhsf_negative_successor + S (ff_s_mce_mdr_functional_secondhsf_negative) = S ((S (S ff_i_mce_mdr_functional_secondhsf_negative)) * ff_v_mce_mdr_functional_secondhsf_negative)) /\ exists ff_q_mce_mdr_functional_secondhsf_negative_successor. ff_u_mce_mdr_functional_secondhsf_negative = ff_q_mce_mdr_functional_secondhsf_negative_successor * S ((S (S ff_i_mce_mdr_functional_secondhsf_negative)) * ff_v_mce_mdr_functional_secondhsf_negative) + (ff_s_mce_mdr_functional_secondhsf_negative))) /\ ff_s_mce_mdr_functional_secondhsf_negative = ff_r_mce_mdr_functional_secondhsf_negative + ff_a_mce_mdr_functional_secondhsf_negative))))))))))))))) /\ ((exists mdr_gap_functional_secondi. mdr_gap_functional_secondi + S (mdr_i_functional_second) = (mdr_l_functional_second)) /\ (exists mdr_z_functional_secondr. ((exists mdr_a_functional_secondrc mdr_b_functional_secondrc mdr_c_functional_secondrc mdr_e_functional_secondrc mdr_f_functional_secondrc. ((mdr_a_functional_secondrc = ((d) + (pb)) * S ((d) + (pb)) + ((pb) + (pb))) /\ ((mdr_b_functional_secondrc = ((pc) + (nb)) * S ((pc) + (nb)) + ((nb) + (nb))) /\ ((mdr_c_functional_secondrc = ((mdr_a_functional_secondrc) + (mdr_b_functional_secondrc)) * S ((mdr_a_functional_secondrc) + (mdr_b_functional_secondrc)) + ((mdr_b_functional_secondrc) + (mdr_b_functional_secondrc))) /\ ((mdr_e_functional_secondrc = ((r) + (s)) * S ((r) + (s)) + ((s) + (s))) /\ ((mdr_f_functional_secondrc = ((nc) + (mdr_e_functional_secondrc)) * S ((nc) + (mdr_e_functional_secondrc)) + ((mdr_e_functional_secondrc) + (mdr_e_functional_secondrc))) /\ ((mdr_z_functional_secondr) = ((mdr_c_functional_secondrc) + (mdr_f_functional_secondrc)) * S ((mdr_c_functional_secondrc) + (mdr_f_functional_secondrc)) + ((mdr_f_functional_secondrc) + (mdr_f_functional_secondrc))))))))) /\ (((exists ff_h_mdr_functional_secondrb. ff_h_mdr_functional_secondrb + S (mdr_z_functional_secondr) = S ((S (mdr_i_functional_second)) * mdr_c_functional_second)) /\ exists ff_q_mdr_functional_secondrb. mdr_b_functional_second = ff_q_mdr_functional_secondrb * S ((S (mdr_i_functional_second)) * mdr_c_functional_second) + (mdr_z_functional_secondr)))))))) -> p = r /\ n = s