matrix_recursive_empty_history

Exact expanded first-order arithmetic statement

forall b c. (forall mdr_i_empty. (exists mdr_gap_emptyi. mdr_gap_emptyi + S (mdr_i_empty) = (0)) -> exists mdr_d_empty mdr_pb_empty mdr_pc_empty mdr_nb_empty mdr_nc_empty mdr_p_empty mdr_n_empty. ((exists mdr_z_emptyr. ((exists mdr_a_emptyrc mdr_b_emptyrc mdr_c_emptyrc mdr_e_emptyrc mdr_f_emptyrc. ((mdr_a_emptyrc = ((mdr_d_empty) + (mdr_pb_empty)) * S ((mdr_d_empty) + (mdr_pb_empty)) + ((mdr_pb_empty) + (mdr_pb_empty))) /\ ((mdr_b_emptyrc = ((mdr_pc_empty) + (mdr_nb_empty)) * S ((mdr_pc_empty) + (mdr_nb_empty)) + ((mdr_nb_empty) + (mdr_nb_empty))) /\ ((mdr_c_emptyrc = ((mdr_a_emptyrc) + (mdr_b_emptyrc)) * S ((mdr_a_emptyrc) + (mdr_b_emptyrc)) + ((mdr_b_emptyrc) + (mdr_b_emptyrc))) /\ ((mdr_e_emptyrc = ((mdr_p_empty) + (mdr_n_empty)) * S ((mdr_p_empty) + (mdr_n_empty)) + ((mdr_n_empty) + (mdr_n_empty))) /\ ((mdr_f_emptyrc = ((mdr_nc_empty) + (mdr_e_emptyrc)) * S ((mdr_nc_empty) + (mdr_e_emptyrc)) + ((mdr_e_emptyrc) + (mdr_e_emptyrc))) /\ ((mdr_z_emptyr) = ((mdr_c_emptyrc) + (mdr_f_emptyrc)) * S ((mdr_c_emptyrc) + (mdr_f_emptyrc)) + ((mdr_f_emptyrc) + (mdr_f_emptyrc))))))))) /\ (((exists ff_h_mdr_emptyrb. ff_h_mdr_emptyrb + S (mdr_z_emptyr) = S ((S (mdr_i_empty)) * c)) /\ exists ff_q_mdr_emptyrb. b = ff_q_mdr_emptyrb * S ((S (mdr_i_empty)) * c) + (mdr_z_emptyr))))) /\ (((((mdr_d_empty) = 0) /\ (((mdr_p_empty) = 1) /\ ((mdr_n_empty) = 0))) \/ exists mdr_q_emptys mdr_eb_emptys mdr_ec_emptys mdr_fb_emptys mdr_fc_emptys. (((mdr_d_empty) = S (mdr_q_emptys)) /\ ((forall mdr_j_emptysc. (exists mdr_gap_emptyscj. mdr_gap_emptyscj + S (mdr_j_emptysc) = (S (mdr_q_emptys))) -> exists mdr_i_emptysc mdr_up_emptysc mdr_us_emptysc mdr_un_emptysc mdr_ut_emptysc mdr_p_emptysc mdr_n_emptysc. ((exists mdr_gap_emptysci. mdr_gap_emptysci + S (mdr_i_emptysc) = (mdr_i_empty)) /\ ((exists mdr_z_emptyscr. ((exists mdr_a_emptyscrc mdr_b_emptyscrc mdr_c_emptyscrc mdr_e_emptyscrc mdr_f_emptyscrc. ((mdr_a_emptyscrc = ((mdr_q_emptys) + (mdr_up_emptysc)) * S ((mdr_q_emptys) + (mdr_up_emptysc)) + ((mdr_up_emptysc) + (mdr_up_emptysc))) /\ ((mdr_b_emptyscrc = ((mdr_us_emptysc) + (mdr_un_emptysc)) * S ((mdr_us_emptysc) + (mdr_un_emptysc)) + ((mdr_un_emptysc) + (mdr_un_emptysc))) /\ ((mdr_c_emptyscrc = ((mdr_a_emptyscrc) + (mdr_b_emptyscrc)) * S ((mdr_a_emptyscrc) + (mdr_b_emptyscrc)) + ((mdr_b_emptyscrc) + (mdr_b_emptyscrc))) /\ ((mdr_e_emptyscrc = ((mdr_p_emptysc) + (mdr_n_emptysc)) * S ((mdr_p_emptysc) + (mdr_n_emptysc)) + ((mdr_n_emptysc) + (mdr_n_emptysc))) /\ ((mdr_f_emptyscrc = ((mdr_ut_emptysc) + (mdr_e_emptyscrc)) * S ((mdr_ut_emptysc) + (mdr_e_emptyscrc)) + ((mdr_e_emptyscrc) + (mdr_e_emptyscrc))) /\ ((mdr_z_emptyscr) = ((mdr_c_emptyscrc) + (mdr_f_emptyscrc)) * S ((mdr_c_emptyscrc) + (mdr_f_emptyscrc)) + ((mdr_f_emptyscrc) + (mdr_f_emptyscrc))))))))) /\ (((exists ff_h_mdr_emptyscrb. ff_h_mdr_emptyscrb + S (mdr_z_emptyscr) = S ((S (mdr_i_emptysc)) * c)) /\ exists ff_q_mdr_emptyscrb. b = ff_q_mdr_emptyscrb * S ((S (mdr_i_emptysc)) * c) + (mdr_z_emptyscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_emptyscm_positive. (exists ff_gap_mdm_lt_mdr_emptyscm_positive_index_bound. ff_gap_mdm_lt_mdr_emptyscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_emptyscm_positive) = ((mdr_q_emptys) * (mdr_q_emptys))) -> exists ff_row_mdm_prefix_mdr_emptyscm_positive ff_column_mdm_prefix_mdr_emptyscm_positive ff_value_mdm_prefix_mdr_emptyscm_positive. (ff_index_mdm_prefix_mdr_emptyscm_positive = (mdr_q_emptys) * ff_row_mdm_prefix_mdr_emptyscm_positive + ff_column_mdm_prefix_mdr_emptyscm_positive /\ ((exists ff_gap_mdm_lt_mdr_emptyscm_positive_column_bound. ff_gap_mdm_lt_mdr_emptyscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_emptyscm_positive) = (mdr_q_emptys)) /\ ((exists ff_row_mdm_cell_mdr_emptyscm_positive_cell ff_column_mdm_cell_mdr_emptyscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_emptyscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_emptyscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_emptyscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_emptyscm_positive_cell = ff_row_mdm_prefix_mdr_emptyscm_positive) \/ ((exists ff_gap_mdm_le_mdr_emptyscm_positive_cell_row_after. ff_gap_mdm_le_mdr_emptyscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_emptyscm_positive)) /\ ff_row_mdm_cell_mdr_emptyscm_positive_cell = S ff_row_mdm_prefix_mdr_emptyscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_emptyscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_emptyscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_emptyscm_positive) = (mdr_j_emptysc)) /\ ff_column_mdm_cell_mdr_emptyscm_positive_cell = ff_column_mdm_prefix_mdr_emptyscm_positive) \/ ((exists ff_gap_mdm_le_mdr_emptyscm_positive_cell_column_after. ff_gap_mdm_le_mdr_emptyscm_positive_cell_column_after + (mdr_j_emptysc) = (ff_column_mdm_prefix_mdr_emptyscm_positive)) /\ ff_column_mdm_cell_mdr_emptyscm_positive_cell = S ff_column_mdm_prefix_mdr_emptyscm_positive))) /\ (((exists ff_h_mdm_mdr_emptyscm_positive_cell_source. ff_h_mdm_mdr_emptyscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_emptyscm_positive) = S ((S ((ff_row_mdm_cell_mdr_emptyscm_positive_cell) * (S (mdr_q_emptys)) + (ff_column_mdm_cell_mdr_emptyscm_positive_cell))) * mdr_pc_empty)) /\ exists ff_q_mdm_mdr_emptyscm_positive_cell_source. mdr_pb_empty = ff_q_mdm_mdr_emptyscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_emptyscm_positive_cell) * (S (mdr_q_emptys)) + (ff_column_mdm_cell_mdr_emptyscm_positive_cell))) * mdr_pc_empty) + (ff_value_mdm_prefix_mdr_emptyscm_positive)))))) /\ (((exists ff_h_mdm_mdr_emptyscm_positive_target. ff_h_mdm_mdr_emptyscm_positive_target + S (ff_value_mdm_prefix_mdr_emptyscm_positive) = S ((S (ff_index_mdm_prefix_mdr_emptyscm_positive)) * mdr_us_emptysc)) /\ exists ff_q_mdm_mdr_emptyscm_positive_target. mdr_up_emptysc = ff_q_mdm_mdr_emptyscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_emptyscm_positive)) * mdr_us_emptysc) + (ff_value_mdm_prefix_mdr_emptyscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_emptyscm_negative. (exists ff_gap_mdm_lt_mdr_emptyscm_negative_index_bound. ff_gap_mdm_lt_mdr_emptyscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_emptyscm_negative) = ((mdr_q_emptys) * (mdr_q_emptys))) -> exists ff_row_mdm_prefix_mdr_emptyscm_negative ff_column_mdm_prefix_mdr_emptyscm_negative ff_value_mdm_prefix_mdr_emptyscm_negative. (ff_index_mdm_prefix_mdr_emptyscm_negative = (mdr_q_emptys) * ff_row_mdm_prefix_mdr_emptyscm_negative + ff_column_mdm_prefix_mdr_emptyscm_negative /\ ((exists ff_gap_mdm_lt_mdr_emptyscm_negative_column_bound. ff_gap_mdm_lt_mdr_emptyscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_emptyscm_negative) = (mdr_q_emptys)) /\ ((exists ff_row_mdm_cell_mdr_emptyscm_negative_cell ff_column_mdm_cell_mdr_emptyscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_emptyscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_emptyscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_emptyscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_emptyscm_negative_cell = ff_row_mdm_prefix_mdr_emptyscm_negative) \/ ((exists ff_gap_mdm_le_mdr_emptyscm_negative_cell_row_after. ff_gap_mdm_le_mdr_emptyscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_emptyscm_negative)) /\ ff_row_mdm_cell_mdr_emptyscm_negative_cell = S ff_row_mdm_prefix_mdr_emptyscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_emptyscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_emptyscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_emptyscm_negative) = (mdr_j_emptysc)) /\ ff_column_mdm_cell_mdr_emptyscm_negative_cell = ff_column_mdm_prefix_mdr_emptyscm_negative) \/ ((exists ff_gap_mdm_le_mdr_emptyscm_negative_cell_column_after. ff_gap_mdm_le_mdr_emptyscm_negative_cell_column_after + (mdr_j_emptysc) = (ff_column_mdm_prefix_mdr_emptyscm_negative)) /\ ff_column_mdm_cell_mdr_emptyscm_negative_cell = S ff_column_mdm_prefix_mdr_emptyscm_negative))) /\ (((exists ff_h_mdm_mdr_emptyscm_negative_cell_source. ff_h_mdm_mdr_emptyscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_emptyscm_negative) = S ((S ((ff_row_mdm_cell_mdr_emptyscm_negative_cell) * (S (mdr_q_emptys)) + (ff_column_mdm_cell_mdr_emptyscm_negative_cell))) * mdr_nc_empty)) /\ exists ff_q_mdm_mdr_emptyscm_negative_cell_source. mdr_nb_empty = ff_q_mdm_mdr_emptyscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_emptyscm_negative_cell) * (S (mdr_q_emptys)) + (ff_column_mdm_cell_mdr_emptyscm_negative_cell))) * mdr_nc_empty) + (ff_value_mdm_prefix_mdr_emptyscm_negative)))))) /\ (((exists ff_h_mdm_mdr_emptyscm_negative_target. ff_h_mdm_mdr_emptyscm_negative_target + S (ff_value_mdm_prefix_mdr_emptyscm_negative) = S ((S (ff_index_mdm_prefix_mdr_emptyscm_negative)) * mdr_ut_emptysc)) /\ exists ff_q_mdm_mdr_emptyscm_negative_target. mdr_un_emptysc = ff_q_mdm_mdr_emptyscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_emptyscm_negative)) * mdr_ut_emptysc) + (ff_value_mdm_prefix_mdr_emptyscm_negative))))))))) /\ ((((exists ff_h_mdr_emptyscp. ff_h_mdr_emptyscp + S (mdr_p_emptysc) = S ((S (mdr_j_emptysc)) * mdr_ec_emptys)) /\ exists ff_q_mdr_emptyscp. mdr_eb_emptys = ff_q_mdr_emptyscp * S ((S (mdr_j_emptysc)) * mdr_ec_emptys) + (mdr_p_emptysc))) /\ (((exists ff_h_mdr_emptyscn. ff_h_mdr_emptyscn + S (mdr_n_emptysc) = S ((S (mdr_j_emptysc)) * mdr_fc_emptys)) /\ exists ff_q_mdr_emptyscn. mdr_fb_emptys = ff_q_mdr_emptyscn * S ((S (mdr_j_emptysc)) * mdr_fc_emptys) + (mdr_n_emptysc)))))))) /\ (exists ff_ub_mce_fold_mdr_emptysf ff_uc_mce_fold_mdr_emptysf ff_vb_mce_fold_mdr_emptysf ff_vc_mce_fold_mdr_emptysf. ((forall ff_index_mce_alternating_mdr_emptysf_prefix. (exists ff_gap_mce_mdr_emptysf_prefix_index. ff_gap_mce_mdr_emptysf_prefix_index + S (ff_index_mce_alternating_mdr_emptysf_prefix) = (S (mdr_q_emptys))) -> exists ff_ap_mce_alternating_mdr_emptysf_prefix ff_an_mce_alternating_mdr_emptysf_prefix ff_bp_mce_alternating_mdr_emptysf_prefix ff_bn_mce_alternating_mdr_emptysf_prefix ff_p_mce_alternating_mdr_emptysf_prefix ff_n_mce_alternating_mdr_emptysf_prefix. ((((exists ff_h_mce_mdr_emptysf_prefix_ap. ff_h_mce_mdr_emptysf_prefix_ap + S (ff_ap_mce_alternating_mdr_emptysf_prefix) = S ((S (ff_index_mce_alternating_mdr_emptysf_prefix)) * mdr_pc_empty)) /\ exists ff_q_mce_mdr_emptysf_prefix_ap. mdr_pb_empty = ff_q_mce_mdr_emptysf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_emptysf_prefix)) * mdr_pc_empty) + (ff_ap_mce_alternating_mdr_emptysf_prefix))) /\ ((((exists ff_h_mce_mdr_emptysf_prefix_an. ff_h_mce_mdr_emptysf_prefix_an + S (ff_an_mce_alternating_mdr_emptysf_prefix) = S ((S (ff_index_mce_alternating_mdr_emptysf_prefix)) * mdr_nc_empty)) /\ exists ff_q_mce_mdr_emptysf_prefix_an. mdr_nb_empty = ff_q_mce_mdr_emptysf_prefix_an * S ((S (ff_index_mce_alternating_mdr_emptysf_prefix)) * mdr_nc_empty) + (ff_an_mce_alternating_mdr_emptysf_prefix))) /\ ((((exists ff_h_mce_mdr_emptysf_prefix_bp. ff_h_mce_mdr_emptysf_prefix_bp + S (ff_bp_mce_alternating_mdr_emptysf_prefix) = S ((S (ff_index_mce_alternating_mdr_emptysf_prefix)) * mdr_ec_emptys)) /\ exists ff_q_mce_mdr_emptysf_prefix_bp. mdr_eb_emptys = ff_q_mce_mdr_emptysf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_emptysf_prefix)) * mdr_ec_emptys) + (ff_bp_mce_alternating_mdr_emptysf_prefix))) /\ ((((exists ff_h_mce_mdr_emptysf_prefix_bn. ff_h_mce_mdr_emptysf_prefix_bn + S (ff_bn_mce_alternating_mdr_emptysf_prefix) = S ((S (ff_index_mce_alternating_mdr_emptysf_prefix)) * mdr_fc_emptys)) /\ exists ff_q_mce_mdr_emptysf_prefix_bn. mdr_fb_emptys = ff_q_mce_mdr_emptysf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_emptysf_prefix)) * mdr_fc_emptys) + (ff_bn_mce_alternating_mdr_emptysf_prefix))) /\ ((((exists ff_h_mce_mdr_emptysf_prefix_positive. ff_h_mce_mdr_emptysf_prefix_positive + S (ff_p_mce_alternating_mdr_emptysf_prefix) = S ((S (ff_index_mce_alternating_mdr_emptysf_prefix)) * ff_uc_mce_fold_mdr_emptysf)) /\ exists ff_q_mce_mdr_emptysf_prefix_positive. ff_ub_mce_fold_mdr_emptysf = ff_q_mce_mdr_emptysf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_emptysf_prefix)) * ff_uc_mce_fold_mdr_emptysf) + (ff_p_mce_alternating_mdr_emptysf_prefix))) /\ ((((exists ff_h_mce_mdr_emptysf_prefix_negative. ff_h_mce_mdr_emptysf_prefix_negative + S (ff_n_mce_alternating_mdr_emptysf_prefix) = S ((S (ff_index_mce_alternating_mdr_emptysf_prefix)) * ff_vc_mce_fold_mdr_emptysf)) /\ exists ff_q_mce_mdr_emptysf_prefix_negative. ff_vb_mce_fold_mdr_emptysf = ff_q_mce_mdr_emptysf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_emptysf_prefix)) * ff_vc_mce_fold_mdr_emptysf) + (ff_n_mce_alternating_mdr_emptysf_prefix))) /\ (((exists ff_even_mce_term_mdr_emptysf_prefix_term. ff_index_mce_alternating_mdr_emptysf_prefix = 2 * ff_even_mce_term_mdr_emptysf_prefix_term) /\ (ff_p_mce_alternating_mdr_emptysf_prefix = (ff_ap_mce_alternating_mdr_emptysf_prefix) * (ff_bp_mce_alternating_mdr_emptysf_prefix) + (ff_an_mce_alternating_mdr_emptysf_prefix) * (ff_bn_mce_alternating_mdr_emptysf_prefix) /\ ff_n_mce_alternating_mdr_emptysf_prefix = (ff_ap_mce_alternating_mdr_emptysf_prefix) * (ff_bn_mce_alternating_mdr_emptysf_prefix) + (ff_an_mce_alternating_mdr_emptysf_prefix) * (ff_bp_mce_alternating_mdr_emptysf_prefix))) \/ ((exists ff_odd_mce_term_mdr_emptysf_prefix_term. ff_index_mce_alternating_mdr_emptysf_prefix = 2 * ff_odd_mce_term_mdr_emptysf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_emptysf_prefix = (ff_ap_mce_alternating_mdr_emptysf_prefix) * (ff_bn_mce_alternating_mdr_emptysf_prefix) + (ff_an_mce_alternating_mdr_emptysf_prefix) * (ff_bp_mce_alternating_mdr_emptysf_prefix) /\ ff_n_mce_alternating_mdr_emptysf_prefix = (ff_ap_mce_alternating_mdr_emptysf_prefix) * (ff_bp_mce_alternating_mdr_emptysf_prefix) + (ff_an_mce_alternating_mdr_emptysf_prefix) * (ff_bn_mce_alternating_mdr_emptysf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_emptysf_positive ff_v_mce_mdr_emptysf_positive. ((((exists ff_h_mce_mdr_emptysf_positive_start. ff_h_mce_mdr_emptysf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_emptysf_positive)) /\ exists ff_q_mce_mdr_emptysf_positive_start. ff_u_mce_mdr_emptysf_positive = ff_q_mce_mdr_emptysf_positive_start * S ((S (0)) * ff_v_mce_mdr_emptysf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_emptysf_positive_terminal. ff_h_mce_mdr_emptysf_positive_terminal + S (mdr_p_empty) = S ((S ((S (mdr_q_emptys)))) * ff_v_mce_mdr_emptysf_positive)) /\ exists ff_q_mce_mdr_emptysf_positive_terminal. ff_u_mce_mdr_emptysf_positive = ff_q_mce_mdr_emptysf_positive_terminal * S ((S ((S (mdr_q_emptys)))) * ff_v_mce_mdr_emptysf_positive) + (mdr_p_empty))) /\ forall ff_i_mce_mdr_emptysf_positive. (exists ff_lt_mce_mdr_emptysf_positive_bound. ff_lt_mce_mdr_emptysf_positive_bound + S ff_i_mce_mdr_emptysf_positive = (S (mdr_q_emptys))) -> exists ff_a_mce_mdr_emptysf_positive ff_r_mce_mdr_emptysf_positive ff_s_mce_mdr_emptysf_positive. ((((exists ff_h_mce_mdr_emptysf_positive_summand. ff_h_mce_mdr_emptysf_positive_summand + S (ff_a_mce_mdr_emptysf_positive) = S ((S (ff_i_mce_mdr_emptysf_positive)) * ff_uc_mce_fold_mdr_emptysf)) /\ exists ff_q_mce_mdr_emptysf_positive_summand. ff_ub_mce_fold_mdr_emptysf = ff_q_mce_mdr_emptysf_positive_summand * S ((S (ff_i_mce_mdr_emptysf_positive)) * ff_uc_mce_fold_mdr_emptysf) + (ff_a_mce_mdr_emptysf_positive))) /\ ((((exists ff_h_mce_mdr_emptysf_positive_partial. ff_h_mce_mdr_emptysf_positive_partial + S (ff_r_mce_mdr_emptysf_positive) = S ((S (ff_i_mce_mdr_emptysf_positive)) * ff_v_mce_mdr_emptysf_positive)) /\ exists ff_q_mce_mdr_emptysf_positive_partial. ff_u_mce_mdr_emptysf_positive = ff_q_mce_mdr_emptysf_positive_partial * S ((S (ff_i_mce_mdr_emptysf_positive)) * ff_v_mce_mdr_emptysf_positive) + (ff_r_mce_mdr_emptysf_positive))) /\ ((((exists ff_h_mce_mdr_emptysf_positive_successor. ff_h_mce_mdr_emptysf_positive_successor + S (ff_s_mce_mdr_emptysf_positive) = S ((S (S ff_i_mce_mdr_emptysf_positive)) * ff_v_mce_mdr_emptysf_positive)) /\ exists ff_q_mce_mdr_emptysf_positive_successor. ff_u_mce_mdr_emptysf_positive = ff_q_mce_mdr_emptysf_positive_successor * S ((S (S ff_i_mce_mdr_emptysf_positive)) * ff_v_mce_mdr_emptysf_positive) + (ff_s_mce_mdr_emptysf_positive))) /\ ff_s_mce_mdr_emptysf_positive = ff_r_mce_mdr_emptysf_positive + ff_a_mce_mdr_emptysf_positive)))))) /\ (exists ff_u_mce_mdr_emptysf_negative ff_v_mce_mdr_emptysf_negative. ((((exists ff_h_mce_mdr_emptysf_negative_start. ff_h_mce_mdr_emptysf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_emptysf_negative)) /\ exists ff_q_mce_mdr_emptysf_negative_start. ff_u_mce_mdr_emptysf_negative = ff_q_mce_mdr_emptysf_negative_start * S ((S (0)) * ff_v_mce_mdr_emptysf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_emptysf_negative_terminal. ff_h_mce_mdr_emptysf_negative_terminal + S (mdr_n_empty) = S ((S ((S (mdr_q_emptys)))) * ff_v_mce_mdr_emptysf_negative)) /\ exists ff_q_mce_mdr_emptysf_negative_terminal. ff_u_mce_mdr_emptysf_negative = ff_q_mce_mdr_emptysf_negative_terminal * S ((S ((S (mdr_q_emptys)))) * ff_v_mce_mdr_emptysf_negative) + (mdr_n_empty))) /\ forall ff_i_mce_mdr_emptysf_negative. (exists ff_lt_mce_mdr_emptysf_negative_bound. ff_lt_mce_mdr_emptysf_negative_bound + S ff_i_mce_mdr_emptysf_negative = (S (mdr_q_emptys))) -> exists ff_a_mce_mdr_emptysf_negative ff_r_mce_mdr_emptysf_negative ff_s_mce_mdr_emptysf_negative. ((((exists ff_h_mce_mdr_emptysf_negative_summand. ff_h_mce_mdr_emptysf_negative_summand + S (ff_a_mce_mdr_emptysf_negative) = S ((S (ff_i_mce_mdr_emptysf_negative)) * ff_vc_mce_fold_mdr_emptysf)) /\ exists ff_q_mce_mdr_emptysf_negative_summand. ff_vb_mce_fold_mdr_emptysf = ff_q_mce_mdr_emptysf_negative_summand * S ((S (ff_i_mce_mdr_emptysf_negative)) * ff_vc_mce_fold_mdr_emptysf) + (ff_a_mce_mdr_emptysf_negative))) /\ ((((exists ff_h_mce_mdr_emptysf_negative_partial. ff_h_mce_mdr_emptysf_negative_partial + S (ff_r_mce_mdr_emptysf_negative) = S ((S (ff_i_mce_mdr_emptysf_negative)) * ff_v_mce_mdr_emptysf_negative)) /\ exists ff_q_mce_mdr_emptysf_negative_partial. ff_u_mce_mdr_emptysf_negative = ff_q_mce_mdr_emptysf_negative_partial * S ((S (ff_i_mce_mdr_emptysf_negative)) * ff_v_mce_mdr_emptysf_negative) + (ff_r_mce_mdr_emptysf_negative))) /\ ((((exists ff_h_mce_mdr_emptysf_negative_successor. ff_h_mce_mdr_emptysf_negative_successor + S (ff_s_mce_mdr_emptysf_negative) = S ((S (S ff_i_mce_mdr_emptysf_negative)) * ff_v_mce_mdr_emptysf_negative)) /\ exists ff_q_mce_mdr_emptysf_negative_successor. ff_u_mce_mdr_emptysf_negative = ff_q_mce_mdr_emptysf_negative_successor * S ((S (S ff_i_mce_mdr_emptysf_negative)) * ff_v_mce_mdr_emptysf_negative) + (ff_s_mce_mdr_emptysf_negative))) /\ ff_s_mce_mdr_emptysf_negative = ff_r_mce_mdr_emptysf_negative + ff_a_mce_mdr_emptysf_negative)))))))))))))))