signed_recursive_determinant_exists

forall pb pc nb nc d. exists p n. (exists mdr_b_det_exists mdr_c_det_exists mdr_l_det_exists mdr_i_det_exists. ((forall mdr_i_det_existsh. (exists mdr_gap_det_existshi. mdr_gap_det_existshi + S (mdr_i_det_existsh) = (mdr_l_det_exists)) -> exists mdr_d_det_existsh mdr_pb_det_existsh mdr_pc_det_existsh mdr_nb_det_existsh mdr_nc_det_existsh mdr_p_det_existsh mdr_n_det_existsh. ((exists mdr_z_det_existshr. ((exists mdr_a_det_existshrc mdr_b_det_existshrc mdr_c_det_existshrc mdr_e_det_existshrc mdr_f_det_existshrc. ((mdr_a_det_existshrc = ((mdr_d_det_existsh) + (mdr_pb_det_existsh)) * S ((mdr_d_det_existsh) + (mdr_pb_det_existsh)) + ((mdr_pb_det_existsh) + (mdr_pb_det_existsh))) /\ ((mdr_b_det_existshrc = ((mdr_pc_det_existsh) + (mdr_nb_det_existsh)) * S ((mdr_pc_det_existsh) + (mdr_nb_det_existsh)) + ((mdr_nb_det_existsh) + (mdr_nb_det_existsh))) /\ ((mdr_c_det_existshrc = ((mdr_a_det_existshrc) + (mdr_b_det_existshrc)) * S ((mdr_a_det_existshrc) + (mdr_b_det_existshrc)) + ((mdr_b_det_existshrc) + (mdr_b_det_existshrc))) /\ ((mdr_e_det_existshrc = ((mdr_p_det_existsh) + (mdr_n_det_existsh)) * S ((mdr_p_det_existsh) + (mdr_n_det_existsh)) + ((mdr_n_det_existsh) + (mdr_n_det_existsh))) /\ ((mdr_f_det_existshrc = ((mdr_nc_det_existsh) + (mdr_e_det_existshrc)) * S ((mdr_nc_det_existsh) + (mdr_e_det_existshrc)) + ((mdr_e_det_existshrc) + (mdr_e_det_existshrc))) /\ ((mdr_z_det_existshr) = ((mdr_c_det_existshrc) + (mdr_f_det_existshrc)) * S ((mdr_c_det_existshrc) + (mdr_f_det_existshrc)) + ((mdr_f_det_existshrc) + (mdr_f_det_existshrc))))))))) /\ (((exists ff_h_mdr_det_existshrb. ff_h_mdr_det_existshrb + S (mdr_z_det_existshr) = S ((S (mdr_i_det_existsh)) * mdr_c_det_exists)) /\ exists ff_q_mdr_det_existshrb. mdr_b_det_exists = ff_q_mdr_det_existshrb * S ((S (mdr_i_det_existsh)) * mdr_c_det_exists) + (mdr_z_det_existshr))))) /\ (((((mdr_d_det_existsh) = 0) /\ (((mdr_p_det_existsh) = 1) /\ ((mdr_n_det_existsh) = 0))) \/ exists mdr_q_det_existshs mdr_eb_det_existshs mdr_ec_det_existshs mdr_fb_det_existshs mdr_fc_det_existshs. (((mdr_d_det_existsh) = S (mdr_q_det_existshs)) /\ ((forall mdr_j_det_existshsc. (exists mdr_gap_det_existshscj. mdr_gap_det_existshscj + S (mdr_j_det_existshsc) = (S (mdr_q_det_existshs))) -> exists mdr_i_det_existshsc mdr_up_det_existshsc mdr_us_det_existshsc mdr_un_det_existshsc mdr_ut_det_existshsc mdr_p_det_existshsc mdr_n_det_existshsc. ((exists mdr_gap_det_existshsci. mdr_gap_det_existshsci + S (mdr_i_det_existshsc) = (mdr_i_det_existsh)) /\ ((exists mdr_z_det_existshscr. ((exists mdr_a_det_existshscrc mdr_b_det_existshscrc mdr_c_det_existshscrc mdr_e_det_existshscrc mdr_f_det_existshscrc. ((mdr_a_det_existshscrc = ((mdr_q_det_existshs) + (mdr_up_det_existshsc)) * S ((mdr_q_det_existshs) + (mdr_up_det_existshsc)) + ((mdr_up_det_existshsc) + (mdr_up_det_existshsc))) /\ ((mdr_b_det_existshscrc = ((mdr_us_det_existshsc) + (mdr_un_det_existshsc)) * S ((mdr_us_det_existshsc) + (mdr_un_det_existshsc)) + ((mdr_un_det_existshsc) + (mdr_un_det_existshsc))) /\ ((mdr_c_det_existshscrc = ((mdr_a_det_existshscrc) + (mdr_b_det_existshscrc)) * S ((mdr_a_det_existshscrc) + (mdr_b_det_existshscrc)) + ((mdr_b_det_existshscrc) + (mdr_b_det_existshscrc))) /\ ((mdr_e_det_existshscrc = ((mdr_p_det_existshsc) + (mdr_n_det_existshsc)) * S ((mdr_p_det_existshsc) + (mdr_n_det_existshsc)) + ((mdr_n_det_existshsc) + (mdr_n_det_existshsc))) /\ ((mdr_f_det_existshscrc = ((mdr_ut_det_existshsc) + (mdr_e_det_existshscrc)) * S ((mdr_ut_det_existshsc) + (mdr_e_det_existshscrc)) + ((mdr_e_det_existshscrc) + (mdr_e_det_existshscrc))) /\ ((mdr_z_det_existshscr) = ((mdr_c_det_existshscrc) + (mdr_f_det_existshscrc)) * S ((mdr_c_det_existshscrc) + (mdr_f_det_existshscrc)) + ((mdr_f_det_existshscrc) + (mdr_f_det_existshscrc))))))))) /\ (((exists ff_h_mdr_det_existshscrb. ff_h_mdr_det_existshscrb + S (mdr_z_det_existshscr) = S ((S (mdr_i_det_existshsc)) * mdr_c_det_exists)) /\ exists ff_q_mdr_det_existshscrb. mdr_b_det_exists = ff_q_mdr_det_existshscrb * S ((S (mdr_i_det_existshsc)) * mdr_c_det_exists) + (mdr_z_det_existshscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_det_existshscm_positive. (exists ff_gap_mdm_lt_mdr_det_existshscm_positive_index_bound. ff_gap_mdm_lt_mdr_det_existshscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_det_existshscm_positive) = ((mdr_q_det_existshs) * (mdr_q_det_existshs))) -> exists ff_row_mdm_prefix_mdr_det_existshscm_positive ff_column_mdm_prefix_mdr_det_existshscm_positive ff_value_mdm_prefix_mdr_det_existshscm_positive. (ff_index_mdm_prefix_mdr_det_existshscm_positive = (mdr_q_det_existshs) * ff_row_mdm_prefix_mdr_det_existshscm_positive + ff_column_mdm_prefix_mdr_det_existshscm_positive /\ ((exists ff_gap_mdm_lt_mdr_det_existshscm_positive_column_bound. ff_gap_mdm_lt_mdr_det_existshscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_det_existshscm_positive) = (mdr_q_det_existshs)) /\ ((exists ff_row_mdm_cell_mdr_det_existshscm_positive_cell ff_column_mdm_cell_mdr_det_existshscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_det_existshscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_det_existshscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_det_existshscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_det_existshscm_positive_cell = ff_row_mdm_prefix_mdr_det_existshscm_positive) \/ ((exists ff_gap_mdm_le_mdr_det_existshscm_positive_cell_row_after. ff_gap_mdm_le_mdr_det_existshscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_det_existshscm_positive)) /\ ff_row_mdm_cell_mdr_det_existshscm_positive_cell = S ff_row_mdm_prefix_mdr_det_existshscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_det_existshscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_det_existshscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_det_existshscm_positive) = (mdr_j_det_existshsc)) /\ ff_column_mdm_cell_mdr_det_existshscm_positive_cell = ff_column_mdm_prefix_mdr_det_existshscm_positive) \/ ((exists ff_gap_mdm_le_mdr_det_existshscm_positive_cell_column_after. ff_gap_mdm_le_mdr_det_existshscm_positive_cell_column_after + (mdr_j_det_existshsc) = (ff_column_mdm_prefix_mdr_det_existshscm_positive)) /\ ff_column_mdm_cell_mdr_det_existshscm_positive_cell = S ff_column_mdm_prefix_mdr_det_existshscm_positive))) /\ (((exists ff_h_mdm_mdr_det_existshscm_positive_cell_source. ff_h_mdm_mdr_det_existshscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_det_existshscm_positive) = S ((S ((ff_row_mdm_cell_mdr_det_existshscm_positive_cell) * (S (mdr_q_det_existshs)) + (ff_column_mdm_cell_mdr_det_existshscm_positive_cell))) * mdr_pc_det_existsh)) /\ exists ff_q_mdm_mdr_det_existshscm_positive_cell_source. mdr_pb_det_existsh = ff_q_mdm_mdr_det_existshscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_det_existshscm_positive_cell) * (S (mdr_q_det_existshs)) + (ff_column_mdm_cell_mdr_det_existshscm_positive_cell))) * mdr_pc_det_existsh) + (ff_value_mdm_prefix_mdr_det_existshscm_positive)))))) /\ (((exists ff_h_mdm_mdr_det_existshscm_positive_target. ff_h_mdm_mdr_det_existshscm_positive_target + S (ff_value_mdm_prefix_mdr_det_existshscm_positive) = S ((S (ff_index_mdm_prefix_mdr_det_existshscm_positive)) * mdr_us_det_existshsc)) /\ exists ff_q_mdm_mdr_det_existshscm_positive_target. mdr_up_det_existshsc = ff_q_mdm_mdr_det_existshscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_det_existshscm_positive)) * mdr_us_det_existshsc) + (ff_value_mdm_prefix_mdr_det_existshscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_det_existshscm_negative. (exists ff_gap_mdm_lt_mdr_det_existshscm_negative_index_bound. ff_gap_mdm_lt_mdr_det_existshscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_det_existshscm_negative) = ((mdr_q_det_existshs) * (mdr_q_det_existshs))) -> exists ff_row_mdm_prefix_mdr_det_existshscm_negative ff_column_mdm_prefix_mdr_det_existshscm_negative ff_value_mdm_prefix_mdr_det_existshscm_negative. (ff_index_mdm_prefix_mdr_det_existshscm_negative = (mdr_q_det_existshs) * ff_row_mdm_prefix_mdr_det_existshscm_negative + ff_column_mdm_prefix_mdr_det_existshscm_negative /\ ((exists ff_gap_mdm_lt_mdr_det_existshscm_negative_column_bound. ff_gap_mdm_lt_mdr_det_existshscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_det_existshscm_negative) = (mdr_q_det_existshs)) /\ ((exists ff_row_mdm_cell_mdr_det_existshscm_negative_cell ff_column_mdm_cell_mdr_det_existshscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_det_existshscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_det_existshscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_det_existshscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_det_existshscm_negative_cell = ff_row_mdm_prefix_mdr_det_existshscm_negative) \/ ((exists ff_gap_mdm_le_mdr_det_existshscm_negative_cell_row_after. ff_gap_mdm_le_mdr_det_existshscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_det_existshscm_negative)) /\ ff_row_mdm_cell_mdr_det_existshscm_negative_cell = S ff_row_mdm_prefix_mdr_det_existshscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_det_existshscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_det_existshscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_det_existshscm_negative) = (mdr_j_det_existshsc)) /\ ff_column_mdm_cell_mdr_det_existshscm_negative_cell = ff_column_mdm_prefix_mdr_det_existshscm_negative) \/ ((exists ff_gap_mdm_le_mdr_det_existshscm_negative_cell_column_after. ff_gap_mdm_le_mdr_det_existshscm_negative_cell_column_after + (mdr_j_det_existshsc) = (ff_column_mdm_prefix_mdr_det_existshscm_negative)) /\ ff_column_mdm_cell_mdr_det_existshscm_negative_cell = S ff_column_mdm_prefix_mdr_det_existshscm_negative))) /\ (((exists ff_h_mdm_mdr_det_existshscm_negative_cell_source. ff_h_mdm_mdr_det_existshscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_det_existshscm_negative) = S ((S ((ff_row_mdm_cell_mdr_det_existshscm_negative_cell) * (S (mdr_q_det_existshs)) + (ff_column_mdm_cell_mdr_det_existshscm_negative_cell))) * mdr_nc_det_existsh)) /\ exists ff_q_mdm_mdr_det_existshscm_negative_cell_source. mdr_nb_det_existsh = ff_q_mdm_mdr_det_existshscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_det_existshscm_negative_cell) * (S (mdr_q_det_existshs)) + (ff_column_mdm_cell_mdr_det_existshscm_negative_cell))) * mdr_nc_det_existsh) + (ff_value_mdm_prefix_mdr_det_existshscm_negative)))))) /\ (((exists ff_h_mdm_mdr_det_existshscm_negative_target. ff_h_mdm_mdr_det_existshscm_negative_target + S (ff_value_mdm_prefix_mdr_det_existshscm_negative) = S ((S (ff_index_mdm_prefix_mdr_det_existshscm_negative)) * mdr_ut_det_existshsc)) /\ exists ff_q_mdm_mdr_det_existshscm_negative_target. mdr_un_det_existshsc = ff_q_mdm_mdr_det_existshscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_det_existshscm_negative)) * mdr_ut_det_existshsc) + (ff_value_mdm_prefix_mdr_det_existshscm_negative))))))))) /\ ((((exists ff_h_mdr_det_existshscp. ff_h_mdr_det_existshscp + S (mdr_p_det_existshsc) = S ((S (mdr_j_det_existshsc)) * mdr_ec_det_existshs)) /\ exists ff_q_mdr_det_existshscp. mdr_eb_det_existshs = ff_q_mdr_det_existshscp * S ((S (mdr_j_det_existshsc)) * mdr_ec_det_existshs) + (mdr_p_det_existshsc))) /\ (((exists ff_h_mdr_det_existshscn. ff_h_mdr_det_existshscn + S (mdr_n_det_existshsc) = S ((S (mdr_j_det_existshsc)) * mdr_fc_det_existshs)) /\ exists ff_q_mdr_det_existshscn. mdr_fb_det_existshs = ff_q_mdr_det_existshscn * S ((S (mdr_j_det_existshsc)) * mdr_fc_det_existshs) + (mdr_n_det_existshsc)))))))) /\ (exists ff_ub_mce_fold_mdr_det_existshsf ff_uc_mce_fold_mdr_det_existshsf ff_vb_mce_fold_mdr_det_existshsf ff_vc_mce_fold_mdr_det_existshsf. ((forall ff_index_mce_alternating_mdr_det_existshsf_prefix. (exists ff_gap_mce_mdr_det_existshsf_prefix_index. ff_gap_mce_mdr_det_existshsf_prefix_index + S (ff_index_mce_alternating_mdr_det_existshsf_prefix) = (S (mdr_q_det_existshs))) -> exists ff_ap_mce_alternating_mdr_det_existshsf_prefix ff_an_mce_alternating_mdr_det_existshsf_prefix ff_bp_mce_alternating_mdr_det_existshsf_prefix ff_bn_mce_alternating_mdr_det_existshsf_prefix ff_p_mce_alternating_mdr_det_existshsf_prefix ff_n_mce_alternating_mdr_det_existshsf_prefix. ((((exists ff_h_mce_mdr_det_existshsf_prefix_ap. ff_h_mce_mdr_det_existshsf_prefix_ap + S (ff_ap_mce_alternating_mdr_det_existshsf_prefix) = S ((S (ff_index_mce_alternating_mdr_det_existshsf_prefix)) * mdr_pc_det_existsh)) /\ exists ff_q_mce_mdr_det_existshsf_prefix_ap. mdr_pb_det_existsh = ff_q_mce_mdr_det_existshsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_det_existshsf_prefix)) * mdr_pc_det_existsh) + (ff_ap_mce_alternating_mdr_det_existshsf_prefix))) /\ ((((exists ff_h_mce_mdr_det_existshsf_prefix_an. ff_h_mce_mdr_det_existshsf_prefix_an + S (ff_an_mce_alternating_mdr_det_existshsf_prefix) = S ((S (ff_index_mce_alternating_mdr_det_existshsf_prefix)) * mdr_nc_det_existsh)) /\ exists ff_q_mce_mdr_det_existshsf_prefix_an. mdr_nb_det_existsh = ff_q_mce_mdr_det_existshsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_det_existshsf_prefix)) * mdr_nc_det_existsh) + (ff_an_mce_alternating_mdr_det_existshsf_prefix))) /\ ((((exists ff_h_mce_mdr_det_existshsf_prefix_bp. ff_h_mce_mdr_det_existshsf_prefix_bp + S (ff_bp_mce_alternating_mdr_det_existshsf_prefix) = S ((S (ff_index_mce_alternating_mdr_det_existshsf_prefix)) * mdr_ec_det_existshs)) /\ exists ff_q_mce_mdr_det_existshsf_prefix_bp. mdr_eb_det_existshs = ff_q_mce_mdr_det_existshsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_det_existshsf_prefix)) * mdr_ec_det_existshs) + (ff_bp_mce_alternating_mdr_det_existshsf_prefix))) /\ ((((exists ff_h_mce_mdr_det_existshsf_prefix_bn. ff_h_mce_mdr_det_existshsf_prefix_bn + S (ff_bn_mce_alternating_mdr_det_existshsf_prefix) = S ((S (ff_index_mce_alternating_mdr_det_existshsf_prefix)) * mdr_fc_det_existshs)) /\ exists ff_q_mce_mdr_det_existshsf_prefix_bn. mdr_fb_det_existshs = ff_q_mce_mdr_det_existshsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_det_existshsf_prefix)) * mdr_fc_det_existshs) + (ff_bn_mce_alternating_mdr_det_existshsf_prefix))) /\ ((((exists ff_h_mce_mdr_det_existshsf_prefix_positive. ff_h_mce_mdr_det_existshsf_prefix_positive + S (ff_p_mce_alternating_mdr_det_existshsf_prefix) = S ((S (ff_index_mce_alternating_mdr_det_existshsf_prefix)) * ff_uc_mce_fold_mdr_det_existshsf)) /\ exists ff_q_mce_mdr_det_existshsf_prefix_positive. ff_ub_mce_fold_mdr_det_existshsf = ff_q_mce_mdr_det_existshsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_det_existshsf_prefix)) * ff_uc_mce_fold_mdr_det_existshsf) + (ff_p_mce_alternating_mdr_det_existshsf_prefix))) /\ ((((exists ff_h_mce_mdr_det_existshsf_prefix_negative. ff_h_mce_mdr_det_existshsf_prefix_negative + S (ff_n_mce_alternating_mdr_det_existshsf_prefix) = S ((S (ff_index_mce_alternating_mdr_det_existshsf_prefix)) * ff_vc_mce_fold_mdr_det_existshsf)) /\ exists ff_q_mce_mdr_det_existshsf_prefix_negative. ff_vb_mce_fold_mdr_det_existshsf = ff_q_mce_mdr_det_existshsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_det_existshsf_prefix)) * ff_vc_mce_fold_mdr_det_existshsf) + (ff_n_mce_alternating_mdr_det_existshsf_prefix))) /\ (((exists ff_even_mce_term_mdr_det_existshsf_prefix_term. ff_index_mce_alternating_mdr_det_existshsf_prefix = 2 * ff_even_mce_term_mdr_det_existshsf_prefix_term) /\ (ff_p_mce_alternating_mdr_det_existshsf_prefix = (ff_ap_mce_alternating_mdr_det_existshsf_prefix) * (ff_bp_mce_alternating_mdr_det_existshsf_prefix) + (ff_an_mce_alternating_mdr_det_existshsf_prefix) * (ff_bn_mce_alternating_mdr_det_existshsf_prefix) /\ ff_n_mce_alternating_mdr_det_existshsf_prefix = (ff_ap_mce_alternating_mdr_det_existshsf_prefix) * (ff_bn_mce_alternating_mdr_det_existshsf_prefix) + (ff_an_mce_alternating_mdr_det_existshsf_prefix) * (ff_bp_mce_alternating_mdr_det_existshsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_det_existshsf_prefix_term. ff_index_mce_alternating_mdr_det_existshsf_prefix = 2 * ff_odd_mce_term_mdr_det_existshsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_det_existshsf_prefix = (ff_ap_mce_alternating_mdr_det_existshsf_prefix) * (ff_bn_mce_alternating_mdr_det_existshsf_prefix) + (ff_an_mce_alternating_mdr_det_existshsf_prefix) * (ff_bp_mce_alternating_mdr_det_existshsf_prefix) /\ ff_n_mce_alternating_mdr_det_existshsf_prefix = (ff_ap_mce_alternating_mdr_det_existshsf_prefix) * (ff_bp_mce_alternating_mdr_det_existshsf_prefix) + (ff_an_mce_alternating_mdr_det_existshsf_prefix) * (ff_bn_mce_alternating_mdr_det_existshsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_det_existshsf_positive ff_v_mce_mdr_det_existshsf_positive. ((((exists ff_h_mce_mdr_det_existshsf_positive_start. ff_h_mce_mdr_det_existshsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_det_existshsf_positive)) /\ exists ff_q_mce_mdr_det_existshsf_positive_start. ff_u_mce_mdr_det_existshsf_positive = ff_q_mce_mdr_det_existshsf_positive_start * S ((S (0)) * ff_v_mce_mdr_det_existshsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_det_existshsf_positive_terminal. ff_h_mce_mdr_det_existshsf_positive_terminal + S (mdr_p_det_existsh) = S ((S ((S (mdr_q_det_existshs)))) * ff_v_mce_mdr_det_existshsf_positive)) /\ exists ff_q_mce_mdr_det_existshsf_positive_terminal. ff_u_mce_mdr_det_existshsf_positive = ff_q_mce_mdr_det_existshsf_positive_terminal * S ((S ((S (mdr_q_det_existshs)))) * ff_v_mce_mdr_det_existshsf_positive) + (mdr_p_det_existsh))) /\ forall ff_i_mce_mdr_det_existshsf_positive. (exists ff_lt_mce_mdr_det_existshsf_positive_bound. ff_lt_mce_mdr_det_existshsf_positive_bound + S ff_i_mce_mdr_det_existshsf_positive = (S (mdr_q_det_existshs))) -> exists ff_a_mce_mdr_det_existshsf_positive ff_r_mce_mdr_det_existshsf_positive ff_s_mce_mdr_det_existshsf_positive. ((((exists ff_h_mce_mdr_det_existshsf_positive_summand. ff_h_mce_mdr_det_existshsf_positive_summand + S (ff_a_mce_mdr_det_existshsf_positive) = S ((S (ff_i_mce_mdr_det_existshsf_positive)) * ff_uc_mce_fold_mdr_det_existshsf)) /\ exists ff_q_mce_mdr_det_existshsf_positive_summand. ff_ub_mce_fold_mdr_det_existshsf = ff_q_mce_mdr_det_existshsf_positive_summand * S ((S (ff_i_mce_mdr_det_existshsf_positive)) * ff_uc_mce_fold_mdr_det_existshsf) + (ff_a_mce_mdr_det_existshsf_positive))) /\ ((((exists ff_h_mce_mdr_det_existshsf_positive_partial. ff_h_mce_mdr_det_existshsf_positive_partial + S (ff_r_mce_mdr_det_existshsf_positive) = S ((S (ff_i_mce_mdr_det_existshsf_positive)) * ff_v_mce_mdr_det_existshsf_positive)) /\ exists ff_q_mce_mdr_det_existshsf_positive_partial. ff_u_mce_mdr_det_existshsf_positive = ff_q_mce_mdr_det_existshsf_positive_partial * S ((S (ff_i_mce_mdr_det_existshsf_positive)) * ff_v_mce_mdr_det_existshsf_positive) + (ff_r_mce_mdr_det_existshsf_positive))) /\ ((((exists ff_h_mce_mdr_det_existshsf_positive_successor. ff_h_mce_mdr_det_existshsf_positive_successor + S (ff_s_mce_mdr_det_existshsf_positive) = S ((S (S ff_i_mce_mdr_det_existshsf_positive)) * ff_v_mce_mdr_det_existshsf_positive)) /\ exists ff_q_mce_mdr_det_existshsf_positive_successor. ff_u_mce_mdr_det_existshsf_positive = ff_q_mce_mdr_det_existshsf_positive_successor * S ((S (S ff_i_mce_mdr_det_existshsf_positive)) * ff_v_mce_mdr_det_existshsf_positive) + (ff_s_mce_mdr_det_existshsf_positive))) /\ ff_s_mce_mdr_det_existshsf_positive = ff_r_mce_mdr_det_existshsf_positive + ff_a_mce_mdr_det_existshsf_positive)))))) /\ (exists ff_u_mce_mdr_det_existshsf_negative ff_v_mce_mdr_det_existshsf_negative. ((((exists ff_h_mce_mdr_det_existshsf_negative_start. ff_h_mce_mdr_det_existshsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_det_existshsf_negative)) /\ exists ff_q_mce_mdr_det_existshsf_negative_start. ff_u_mce_mdr_det_existshsf_negative = ff_q_mce_mdr_det_existshsf_negative_start * S ((S (0)) * ff_v_mce_mdr_det_existshsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_det_existshsf_negative_terminal. ff_h_mce_mdr_det_existshsf_negative_terminal + S (mdr_n_det_existsh) = S ((S ((S (mdr_q_det_existshs)))) * ff_v_mce_mdr_det_existshsf_negative)) /\ exists ff_q_mce_mdr_det_existshsf_negative_terminal. ff_u_mce_mdr_det_existshsf_negative = ff_q_mce_mdr_det_existshsf_negative_terminal * S ((S ((S (mdr_q_det_existshs)))) * ff_v_mce_mdr_det_existshsf_negative) + (mdr_n_det_existsh))) /\ forall ff_i_mce_mdr_det_existshsf_negative. (exists ff_lt_mce_mdr_det_existshsf_negative_bound. ff_lt_mce_mdr_det_existshsf_negative_bound + S ff_i_mce_mdr_det_existshsf_negative = (S (mdr_q_det_existshs))) -> exists ff_a_mce_mdr_det_existshsf_negative ff_r_mce_mdr_det_existshsf_negative ff_s_mce_mdr_det_existshsf_negative. ((((exists ff_h_mce_mdr_det_existshsf_negative_summand. ff_h_mce_mdr_det_existshsf_negative_summand + S (ff_a_mce_mdr_det_existshsf_negative) = S ((S (ff_i_mce_mdr_det_existshsf_negative)) * ff_vc_mce_fold_mdr_det_existshsf)) /\ exists ff_q_mce_mdr_det_existshsf_negative_summand. ff_vb_mce_fold_mdr_det_existshsf = ff_q_mce_mdr_det_existshsf_negative_summand * S ((S (ff_i_mce_mdr_det_existshsf_negative)) * ff_vc_mce_fold_mdr_det_existshsf) + (ff_a_mce_mdr_det_existshsf_negative))) /\ ((((exists ff_h_mce_mdr_det_existshsf_negative_partial. ff_h_mce_mdr_det_existshsf_negative_partial + S (ff_r_mce_mdr_det_existshsf_negative) = S ((S (ff_i_mce_mdr_det_existshsf_negative)) * ff_v_mce_mdr_det_existshsf_negative)) /\ exists ff_q_mce_mdr_det_existshsf_negative_partial. ff_u_mce_mdr_det_existshsf_negative = ff_q_mce_mdr_det_existshsf_negative_partial * S ((S (ff_i_mce_mdr_det_existshsf_negative)) * ff_v_mce_mdr_det_existshsf_negative) + (ff_r_mce_mdr_det_existshsf_negative))) /\ ((((exists ff_h_mce_mdr_det_existshsf_negative_successor. ff_h_mce_mdr_det_existshsf_negative_successor + S (ff_s_mce_mdr_det_existshsf_negative) = S ((S (S ff_i_mce_mdr_det_existshsf_negative)) * ff_v_mce_mdr_det_existshsf_negative)) /\ exists ff_q_mce_mdr_det_existshsf_negative_successor. ff_u_mce_mdr_det_existshsf_negative = ff_q_mce_mdr_det_existshsf_negative_successor * S ((S (S ff_i_mce_mdr_det_existshsf_negative)) * ff_v_mce_mdr_det_existshsf_negative) + (ff_s_mce_mdr_det_existshsf_negative))) /\ ff_s_mce_mdr_det_existshsf_negative = ff_r_mce_mdr_det_existshsf_negative + ff_a_mce_mdr_det_existshsf_negative))))))))))))))) /\ ((exists mdr_gap_det_existsi. mdr_gap_det_existsi + S (mdr_i_det_exists) = (mdr_l_det_exists)) /\ (exists mdr_z_det_existsr. ((exists mdr_a_det_existsrc mdr_b_det_existsrc mdr_c_det_existsrc mdr_e_det_existsrc mdr_f_det_existsrc. ((mdr_a_det_existsrc = ((d) + (pb)) * S ((d) + (pb)) + ((pb) + (pb))) /\ ((mdr_b_det_existsrc = ((pc) + (nb)) * S ((pc) + (nb)) + ((nb) + (nb))) /\ ((mdr_c_det_existsrc = ((mdr_a_det_existsrc) + (mdr_b_det_existsrc)) * S ((mdr_a_det_existsrc) + (mdr_b_det_existsrc)) + ((mdr_b_det_existsrc) + (mdr_b_det_existsrc))) /\ ((mdr_e_det_existsrc = ((p) + (n)) * S ((p) + (n)) + ((n) + (n))) /\ ((mdr_f_det_existsrc = ((nc) + (mdr_e_det_existsrc)) * S ((nc) + (mdr_e_det_existsrc)) + ((mdr_e_det_existsrc) + (mdr_e_det_existsrc))) /\ ((mdr_z_det_existsr) = ((mdr_c_det_existsrc) + (mdr_f_det_existsrc)) * S ((mdr_c_det_existsrc) + (mdr_f_det_existsrc)) + ((mdr_f_det_existsrc) + (mdr_f_det_existsrc))))))))) /\ (((exists ff_h_mdr_det_existsrb. ff_h_mdr_det_existsrb + S (mdr_z_det_existsr) = S ((S (mdr_i_det_exists)) * mdr_c_det_exists)) /\ exists ff_q_mdr_det_existsrb. mdr_b_det_exists = ff_q_mdr_det_existsrb * S ((S (mdr_i_det_exists)) * mdr_c_det_exists) + (mdr_z_det_existsr))))))))