Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.
Exact expanded first-order arithmetic statement
forall ab ac bb bc eb ec fb fc d D. (forall ics_index_data_integer_equal ics_value0_data_integer_equal ics_value1_data_integer_equal ics_value2_data_integer_equal ics_value3_data_integer_equal. (exists ics_gap_data_integer_equal_bound. ics_gap_data_integer_equal_bound + S (ics_index_data_integer_equal) = ((d) * (d))) -> (((exists fs_h_ics_data_integer_equal_at0. fs_h_ics_data_integer_equal_at0 + S (ics_value0_data_integer_equal) = S ((S (ics_index_data_integer_equal)) * ac)) /\ exists fs_q_ics_data_integer_equal_at0. ab = fs_q_ics_data_integer_equal_at0 * S ((S (ics_index_data_integer_equal)) * ac) + (ics_value0_data_integer_equal))) -> (((exists fs_h_ics_data_integer_equal_at1. fs_h_ics_data_integer_equal_at1 + S (ics_value1_data_integer_equal) = S ((S (ics_index_data_integer_equal)) * bc)) /\ exists fs_q_ics_data_integer_equal_at1. bb = fs_q_ics_data_integer_equal_at1 * S ((S (ics_index_data_integer_equal)) * bc) + (ics_value1_data_integer_equal))) -> (((exists fs_h_ics_data_integer_equal_at2. fs_h_ics_data_integer_equal_at2 + S (ics_value2_data_integer_equal) = S ((S (ics_index_data_integer_equal)) * ec)) /\ exists fs_q_ics_data_integer_equal_at2. eb = fs_q_ics_data_integer_equal_at2 * S ((S (ics_index_data_integer_equal)) * ec) + (ics_value2_data_integer_equal))) -> (((exists fs_h_ics_data_integer_equal_at3. fs_h_ics_data_integer_equal_at3 + S (ics_value3_data_integer_equal) = S ((S (ics_index_data_integer_equal)) * fc)) /\ exists fs_q_ics_data_integer_equal_at3. fb = fs_q_ics_data_integer_equal_at3 * S ((S (ics_index_data_integer_equal)) * fc) + (ics_value3_data_integer_equal))) -> ics_value0_data_integer_equal + ics_value3_data_integer_equal = ics_value2_data_integer_equal + ics_value1_data_integer_equal) -> (((~(d = 0)) /\ ((~(D = 0)) /\ (exists mdr_p_data_integer_firstabsolute mdr_n_data_integer_firstabsolute. ((exists mdr_b_data_integer_firstabsoluteevaluation mdr_c_data_integer_firstabsoluteevaluation mdr_l_data_integer_firstabsoluteevaluation mdr_i_data_integer_firstabsoluteevaluation. ((forall mdr_i_data_integer_firstabsoluteevaluationh. (exists mdr_gap_data_integer_firstabsoluteevaluationhi. mdr_gap_data_integer_firstabsoluteevaluationhi + S (mdr_i_data_integer_firstabsoluteevaluationh) = (mdr_l_data_integer_firstabsoluteevaluation)) -> exists mdr_d_data_integer_firstabsoluteevaluationh mdr_pb_data_integer_firstabsoluteevaluationh mdr_pc_data_integer_firstabsoluteevaluationh mdr_nb_data_integer_firstabsoluteevaluationh mdr_nc_data_integer_firstabsoluteevaluationh mdr_p_data_integer_firstabsoluteevaluationh mdr_n_data_integer_firstabsoluteevaluationh. ((exists mdr_z_data_integer_firstabsoluteevaluationhr. ((exists mdr_a_data_integer_firstabsoluteevaluationhrc mdr_b_data_integer_firstabsoluteevaluationhrc mdr_c_data_integer_firstabsoluteevaluationhrc mdr_e_data_integer_firstabsoluteevaluationhrc mdr_f_data_integer_firstabsoluteevaluationhrc. ((mdr_a_data_integer_firstabsoluteevaluationhrc = ((mdr_d_data_integer_firstabsoluteevaluationh) + (mdr_pb_data_integer_firstabsoluteevaluationh)) * S ((mdr_d_data_integer_firstabsoluteevaluationh) + (mdr_pb_data_integer_firstabsoluteevaluationh)) + ((mdr_pb_data_integer_firstabsoluteevaluationh) + (mdr_pb_data_integer_firstabsoluteevaluationh))) /\ ((mdr_b_data_integer_firstabsoluteevaluationhrc = ((mdr_pc_data_integer_firstabsoluteevaluationh) + (mdr_nb_data_integer_firstabsoluteevaluationh)) * S ((mdr_pc_data_integer_firstabsoluteevaluationh) + (mdr_nb_data_integer_firstabsoluteevaluationh)) + ((mdr_nb_data_integer_firstabsoluteevaluationh) + (mdr_nb_data_integer_firstabsoluteevaluationh))) /\ ((mdr_c_data_integer_firstabsoluteevaluationhrc = ((mdr_a_data_integer_firstabsoluteevaluationhrc) + (mdr_b_data_integer_firstabsoluteevaluationhrc)) * S ((mdr_a_data_integer_firstabsoluteevaluationhrc) + (mdr_b_data_integer_firstabsoluteevaluationhrc)) + ((mdr_b_data_integer_firstabsoluteevaluationhrc) + (mdr_b_data_integer_firstabsoluteevaluationhrc))) /\ ((mdr_e_data_integer_firstabsoluteevaluationhrc = ((mdr_p_data_integer_firstabsoluteevaluationh) + (mdr_n_data_integer_firstabsoluteevaluationh)) * S ((mdr_p_data_integer_firstabsoluteevaluationh) + (mdr_n_data_integer_firstabsoluteevaluationh)) + ((mdr_n_data_integer_firstabsoluteevaluationh) + (mdr_n_data_integer_firstabsoluteevaluationh))) /\ ((mdr_f_data_integer_firstabsoluteevaluationhrc = ((mdr_nc_data_integer_firstabsoluteevaluationh) + (mdr_e_data_integer_firstabsoluteevaluationhrc)) * S ((mdr_nc_data_integer_firstabsoluteevaluationh) + (mdr_e_data_integer_firstabsoluteevaluationhrc)) + ((mdr_e_data_integer_firstabsoluteevaluationhrc) + (mdr_e_data_integer_firstabsoluteevaluationhrc))) /\ ((mdr_z_data_integer_firstabsoluteevaluationhr) = ((mdr_c_data_integer_firstabsoluteevaluationhrc) + (mdr_f_data_integer_firstabsoluteevaluationhrc)) * S ((mdr_c_data_integer_firstabsoluteevaluationhrc) + (mdr_f_data_integer_firstabsoluteevaluationhrc)) + ((mdr_f_data_integer_firstabsoluteevaluationhrc) + (mdr_f_data_integer_firstabsoluteevaluationhrc))))))))) /\ (((exists ff_h_mdr_data_integer_firstabsoluteevaluationhrb. ff_h_mdr_data_integer_firstabsoluteevaluationhrb + S (mdr_z_data_integer_firstabsoluteevaluationhr) = S ((S (mdr_i_data_integer_firstabsoluteevaluationh)) * mdr_c_data_integer_firstabsoluteevaluation)) /\ exists ff_q_mdr_data_integer_firstabsoluteevaluationhrb. mdr_b_data_integer_firstabsoluteevaluation = ff_q_mdr_data_integer_firstabsoluteevaluationhrb * S ((S (mdr_i_data_integer_firstabsoluteevaluationh)) * mdr_c_data_integer_firstabsoluteevaluation) + (mdr_z_data_integer_firstabsoluteevaluationhr))))) /\ (((((mdr_d_data_integer_firstabsoluteevaluationh) = 0) /\ (((mdr_p_data_integer_firstabsoluteevaluationh) = 1) /\ ((mdr_n_data_integer_firstabsoluteevaluationh) = 0))) \/ exists mdr_q_data_integer_firstabsoluteevaluationhs mdr_eb_data_integer_firstabsoluteevaluationhs mdr_ec_data_integer_firstabsoluteevaluationhs mdr_fb_data_integer_firstabsoluteevaluationhs mdr_fc_data_integer_firstabsoluteevaluationhs. (((mdr_d_data_integer_firstabsoluteevaluationh) = S (mdr_q_data_integer_firstabsoluteevaluationhs)) /\ ((forall mdr_j_data_integer_firstabsoluteevaluationhsc. (exists mdr_gap_data_integer_firstabsoluteevaluationhscj. mdr_gap_data_integer_firstabsoluteevaluationhscj + S (mdr_j_data_integer_firstabsoluteevaluationhsc) = (S (mdr_q_data_integer_firstabsoluteevaluationhs))) -> exists mdr_i_data_integer_firstabsoluteevaluationhsc mdr_up_data_integer_firstabsoluteevaluationhsc mdr_us_data_integer_firstabsoluteevaluationhsc mdr_un_data_integer_firstabsoluteevaluationhsc mdr_ut_data_integer_firstabsoluteevaluationhsc mdr_p_data_integer_firstabsoluteevaluationhsc mdr_n_data_integer_firstabsoluteevaluationhsc. ((exists mdr_gap_data_integer_firstabsoluteevaluationhsci. mdr_gap_data_integer_firstabsoluteevaluationhsci + S (mdr_i_data_integer_firstabsoluteevaluationhsc) = (mdr_i_data_integer_firstabsoluteevaluationh)) /\ ((exists mdr_z_data_integer_firstabsoluteevaluationhscr. ((exists mdr_a_data_integer_firstabsoluteevaluationhscrc mdr_b_data_integer_firstabsoluteevaluationhscrc mdr_c_data_integer_firstabsoluteevaluationhscrc mdr_e_data_integer_firstabsoluteevaluationhscrc mdr_f_data_integer_firstabsoluteevaluationhscrc. ((mdr_a_data_integer_firstabsoluteevaluationhscrc = ((mdr_q_data_integer_firstabsoluteevaluationhs) + (mdr_up_data_integer_firstabsoluteevaluationhsc)) * S ((mdr_q_data_integer_firstabsoluteevaluationhs) + (mdr_up_data_integer_firstabsoluteevaluationhsc)) + ((mdr_up_data_integer_firstabsoluteevaluationhsc) + (mdr_up_data_integer_firstabsoluteevaluationhsc))) /\ ((mdr_b_data_integer_firstabsoluteevaluationhscrc = ((mdr_us_data_integer_firstabsoluteevaluationhsc) + (mdr_un_data_integer_firstabsoluteevaluationhsc)) * S ((mdr_us_data_integer_firstabsoluteevaluationhsc) + (mdr_un_data_integer_firstabsoluteevaluationhsc)) + ((mdr_un_data_integer_firstabsoluteevaluationhsc) + (mdr_un_data_integer_firstabsoluteevaluationhsc))) /\ ((mdr_c_data_integer_firstabsoluteevaluationhscrc = ((mdr_a_data_integer_firstabsoluteevaluationhscrc) + (mdr_b_data_integer_firstabsoluteevaluationhscrc)) * S ((mdr_a_data_integer_firstabsoluteevaluationhscrc) + (mdr_b_data_integer_firstabsoluteevaluationhscrc)) + ((mdr_b_data_integer_firstabsoluteevaluationhscrc) + (mdr_b_data_integer_firstabsoluteevaluationhscrc))) /\ ((mdr_e_data_integer_firstabsoluteevaluationhscrc = ((mdr_p_data_integer_firstabsoluteevaluationhsc) + (mdr_n_data_integer_firstabsoluteevaluationhsc)) * S ((mdr_p_data_integer_firstabsoluteevaluationhsc) + (mdr_n_data_integer_firstabsoluteevaluationhsc)) + ((mdr_n_data_integer_firstabsoluteevaluationhsc) + (mdr_n_data_integer_firstabsoluteevaluationhsc))) /\ ((mdr_f_data_integer_firstabsoluteevaluationhscrc = ((mdr_ut_data_integer_firstabsoluteevaluationhsc) + (mdr_e_data_integer_firstabsoluteevaluationhscrc)) * S ((mdr_ut_data_integer_firstabsoluteevaluationhsc) + (mdr_e_data_integer_firstabsoluteevaluationhscrc)) + ((mdr_e_data_integer_firstabsoluteevaluationhscrc) + (mdr_e_data_integer_firstabsoluteevaluationhscrc))) /\ ((mdr_z_data_integer_firstabsoluteevaluationhscr) = ((mdr_c_data_integer_firstabsoluteevaluationhscrc) + (mdr_f_data_integer_firstabsoluteevaluationhscrc)) * S ((mdr_c_data_integer_firstabsoluteevaluationhscrc) + (mdr_f_data_integer_firstabsoluteevaluationhscrc)) + ((mdr_f_data_integer_firstabsoluteevaluationhscrc) + (mdr_f_data_integer_firstabsoluteevaluationhscrc))))))))) /\ (((exists ff_h_mdr_data_integer_firstabsoluteevaluationhscrb. ff_h_mdr_data_integer_firstabsoluteevaluationhscrb + S (mdr_z_data_integer_firstabsoluteevaluationhscr) = S ((S (mdr_i_data_integer_firstabsoluteevaluationhsc)) * mdr_c_data_integer_firstabsoluteevaluation)) /\ exists ff_q_mdr_data_integer_firstabsoluteevaluationhscrb. mdr_b_data_integer_firstabsoluteevaluation = ff_q_mdr_data_integer_firstabsoluteevaluationhscrb * S ((S (mdr_i_data_integer_firstabsoluteevaluationhsc)) * mdr_c_data_integer_firstabsoluteevaluation) + (mdr_z_data_integer_firstabsoluteevaluationhscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_data_integer_firstabsoluteevaluationhscm_positive. (exists ff_gap_mdm_lt_mdr_data_integer_firstabsoluteevaluationhscm_positive_index_bound. ff_gap_mdm_lt_mdr_data_integer_firstabsoluteevaluationhscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_data_integer_firstabsoluteevaluationhscm_positive) = ((mdr_q_data_integer_firstabsoluteevaluationhs) * (mdr_q_data_integer_firstabsoluteevaluationhs))) -> exists ff_row_mdm_prefix_mdr_data_integer_firstabsoluteevaluationhscm_positive ff_column_mdm_prefix_mdr_data_integer_firstabsoluteevaluationhscm_positive ff_value_mdm_prefix_mdr_data_integer_firstabsoluteevaluationhscm_positive. (ff_index_mdm_prefix_mdr_data_integer_firstabsoluteevaluationhscm_positive = (mdr_q_data_integer_firstabsoluteevaluationhs) * ff_row_mdm_prefix_mdr_data_integer_firstabsoluteevaluationhscm_positive + ff_column_mdm_prefix_mdr_data_integer_firstabsoluteevaluationhscm_positive /\ ((exists ff_gap_mdm_lt_mdr_data_integer_firstabsoluteevaluationhscm_positive_column_bound. ff_gap_mdm_lt_mdr_data_integer_firstabsoluteevaluationhscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_data_integer_firstabsoluteevaluationhscm_positive) = (mdr_q_data_integer_firstabsoluteevaluationhs)) /\ ((exists ff_row_mdm_cell_mdr_data_integer_firstabsoluteevaluationhscm_positive_cell ff_column_mdm_cell_mdr_data_integer_firstabsoluteevaluationhscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_data_integer_firstabsoluteevaluationhscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_data_integer_firstabsoluteevaluationhscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_data_integer_firstabsoluteevaluationhscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_data_integer_firstabsoluteevaluationhscm_positive_cell = ff_row_mdm_prefix_mdr_data_integer_firstabsoluteevaluationhscm_positive) \/ ((exists ff_gap_mdm_le_mdr_data_integer_firstabsoluteevaluationhscm_positive_cell_row_after. ff_gap_mdm_le_mdr_data_integer_firstabsoluteevaluationhscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_data_integer_firstabsoluteevaluationhscm_positive)) /\ ff_row_mdm_cell_mdr_data_integer_firstabsoluteevaluationhscm_positive_cell = S ff_row_mdm_prefix_mdr_data_integer_firstabsoluteevaluationhscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_data_integer_firstabsoluteevaluationhscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_data_integer_firstabsoluteevaluationhscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_data_integer_firstabsoluteevaluationhscm_positive) = (mdr_j_data_integer_firstabsoluteevaluationhsc)) /\ ff_column_mdm_cell_mdr_data_integer_firstabsoluteevaluationhscm_positive_cell = ff_column_mdm_prefix_mdr_data_integer_firstabsoluteevaluationhscm_positive) \/ ((exists ff_gap_mdm_le_mdr_data_integer_firstabsoluteevaluationhscm_positive_cell_column_after. ff_gap_mdm_le_mdr_data_integer_firstabsoluteevaluationhscm_positive_cell_column_after + (mdr_j_data_integer_firstabsoluteevaluationhsc) = (ff_column_mdm_prefix_mdr_data_integer_firstabsoluteevaluationhscm_positive)) /\ ff_column_mdm_cell_mdr_data_integer_firstabsoluteevaluationhscm_positive_cell = S ff_column_mdm_prefix_mdr_data_integer_firstabsoluteevaluationhscm_positive))) /\ (((exists ff_h_mdm_mdr_data_integer_firstabsoluteevaluationhscm_positive_cell_source. ff_h_mdm_mdr_data_integer_firstabsoluteevaluationhscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_data_integer_firstabsoluteevaluationhscm_positive) = S ((S ((ff_row_mdm_cell_mdr_data_integer_firstabsoluteevaluationhscm_positive_cell) * (S (mdr_q_data_integer_firstabsoluteevaluationhs)) + (ff_column_mdm_cell_mdr_data_integer_firstabsoluteevaluationhscm_positive_cell))) * mdr_pc_data_integer_firstabsoluteevaluationh)) /\ exists ff_q_mdm_mdr_data_integer_firstabsoluteevaluationhscm_positive_cell_source. mdr_pb_data_integer_firstabsoluteevaluationh = ff_q_mdm_mdr_data_integer_firstabsoluteevaluationhscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_data_integer_firstabsoluteevaluationhscm_positive_cell) * (S (mdr_q_data_integer_firstabsoluteevaluationhs)) + (ff_column_mdm_cell_mdr_data_integer_firstabsoluteevaluationhscm_positive_cell))) * mdr_pc_data_integer_firstabsoluteevaluationh) + (ff_value_mdm_prefix_mdr_data_integer_firstabsoluteevaluationhscm_positive)))))) /\ (((exists ff_h_mdm_mdr_data_integer_firstabsoluteevaluationhscm_positive_target. ff_h_mdm_mdr_data_integer_firstabsoluteevaluationhscm_positive_target + S (ff_value_mdm_prefix_mdr_data_integer_firstabsoluteevaluationhscm_positive) = S ((S (ff_index_mdm_prefix_mdr_data_integer_firstabsoluteevaluationhscm_positive)) * mdr_us_data_integer_firstabsoluteevaluationhsc)) /\ exists ff_q_mdm_mdr_data_integer_firstabsoluteevaluationhscm_positive_target. mdr_up_data_integer_firstabsoluteevaluationhsc = ff_q_mdm_mdr_data_integer_firstabsoluteevaluationhscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_data_integer_firstabsoluteevaluationhscm_positive)) * mdr_us_data_integer_firstabsoluteevaluationhsc) + (ff_value_mdm_prefix_mdr_data_integer_firstabsoluteevaluationhscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_data_integer_firstabsoluteevaluationhscm_negative. (exists ff_gap_mdm_lt_mdr_data_integer_firstabsoluteevaluationhscm_negative_index_bound. ff_gap_mdm_lt_mdr_data_integer_firstabsoluteevaluationhscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_data_integer_firstabsoluteevaluationhscm_negative) = ((mdr_q_data_integer_firstabsoluteevaluationhs) * (mdr_q_data_integer_firstabsoluteevaluationhs))) -> exists ff_row_mdm_prefix_mdr_data_integer_firstabsoluteevaluationhscm_negative ff_column_mdm_prefix_mdr_data_integer_firstabsoluteevaluationhscm_negative ff_value_mdm_prefix_mdr_data_integer_firstabsoluteevaluationhscm_negative. (ff_index_mdm_prefix_mdr_data_integer_firstabsoluteevaluationhscm_negative = (mdr_q_data_integer_firstabsoluteevaluationhs) * ff_row_mdm_prefix_mdr_data_integer_firstabsoluteevaluationhscm_negative + ff_column_mdm_prefix_mdr_data_integer_firstabsoluteevaluationhscm_negative /\ ((exists ff_gap_mdm_lt_mdr_data_integer_firstabsoluteevaluationhscm_negative_column_bound. ff_gap_mdm_lt_mdr_data_integer_firstabsoluteevaluationhscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_data_integer_firstabsoluteevaluationhscm_negative) = (mdr_q_data_integer_firstabsoluteevaluationhs)) /\ ((exists ff_row_mdm_cell_mdr_data_integer_firstabsoluteevaluationhscm_negative_cell ff_column_mdm_cell_mdr_data_integer_firstabsoluteevaluationhscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_data_integer_firstabsoluteevaluationhscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_data_integer_firstabsoluteevaluationhscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_data_integer_firstabsoluteevaluationhscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_data_integer_firstabsoluteevaluationhscm_negative_cell = ff_row_mdm_prefix_mdr_data_integer_firstabsoluteevaluationhscm_negative) \/ ((exists ff_gap_mdm_le_mdr_data_integer_firstabsoluteevaluationhscm_negative_cell_row_after. ff_gap_mdm_le_mdr_data_integer_firstabsoluteevaluationhscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_data_integer_firstabsoluteevaluationhscm_negative)) /\ ff_row_mdm_cell_mdr_data_integer_firstabsoluteevaluationhscm_negative_cell = S ff_row_mdm_prefix_mdr_data_integer_firstabsoluteevaluationhscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_data_integer_firstabsoluteevaluationhscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_data_integer_firstabsoluteevaluationhscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_data_integer_firstabsoluteevaluationhscm_negative) = (mdr_j_data_integer_firstabsoluteevaluationhsc)) /\ ff_column_mdm_cell_mdr_data_integer_firstabsoluteevaluationhscm_negative_cell = ff_column_mdm_prefix_mdr_data_integer_firstabsoluteevaluationhscm_negative) \/ ((exists ff_gap_mdm_le_mdr_data_integer_firstabsoluteevaluationhscm_negative_cell_column_after. ff_gap_mdm_le_mdr_data_integer_firstabsoluteevaluationhscm_negative_cell_column_after + (mdr_j_data_integer_firstabsoluteevaluationhsc) = (ff_column_mdm_prefix_mdr_data_integer_firstabsoluteevaluationhscm_negative)) /\ ff_column_mdm_cell_mdr_data_integer_firstabsoluteevaluationhscm_negative_cell = S ff_column_mdm_prefix_mdr_data_integer_firstabsoluteevaluationhscm_negative))) /\ (((exists ff_h_mdm_mdr_data_integer_firstabsoluteevaluationhscm_negative_cell_source. ff_h_mdm_mdr_data_integer_firstabsoluteevaluationhscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_data_integer_firstabsoluteevaluationhscm_negative) = S ((S ((ff_row_mdm_cell_mdr_data_integer_firstabsoluteevaluationhscm_negative_cell) * (S (mdr_q_data_integer_firstabsoluteevaluationhs)) + (ff_column_mdm_cell_mdr_data_integer_firstabsoluteevaluationhscm_negative_cell))) * mdr_nc_data_integer_firstabsoluteevaluationh)) /\ exists ff_q_mdm_mdr_data_integer_firstabsoluteevaluationhscm_negative_cell_source. mdr_nb_data_integer_firstabsoluteevaluationh = ff_q_mdm_mdr_data_integer_firstabsoluteevaluationhscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_data_integer_firstabsoluteevaluationhscm_negative_cell) * (S (mdr_q_data_integer_firstabsoluteevaluationhs)) + (ff_column_mdm_cell_mdr_data_integer_firstabsoluteevaluationhscm_negative_cell))) * mdr_nc_data_integer_firstabsoluteevaluationh) + (ff_value_mdm_prefix_mdr_data_integer_firstabsoluteevaluationhscm_negative)))))) /\ (((exists ff_h_mdm_mdr_data_integer_firstabsoluteevaluationhscm_negative_target. ff_h_mdm_mdr_data_integer_firstabsoluteevaluationhscm_negative_target + S (ff_value_mdm_prefix_mdr_data_integer_firstabsoluteevaluationhscm_negative) = S ((S (ff_index_mdm_prefix_mdr_data_integer_firstabsoluteevaluationhscm_negative)) * mdr_ut_data_integer_firstabsoluteevaluationhsc)) /\ exists ff_q_mdm_mdr_data_integer_firstabsoluteevaluationhscm_negative_target. mdr_un_data_integer_firstabsoluteevaluationhsc = ff_q_mdm_mdr_data_integer_firstabsoluteevaluationhscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_data_integer_firstabsoluteevaluationhscm_negative)) * mdr_ut_data_integer_firstabsoluteevaluationhsc) + (ff_value_mdm_prefix_mdr_data_integer_firstabsoluteevaluationhscm_negative))))))))) /\ ((((exists ff_h_mdr_data_integer_firstabsoluteevaluationhscp. ff_h_mdr_data_integer_firstabsoluteevaluationhscp + S (mdr_p_data_integer_firstabsoluteevaluationhsc) = S ((S (mdr_j_data_integer_firstabsoluteevaluationhsc)) * mdr_ec_data_integer_firstabsoluteevaluationhs)) /\ exists ff_q_mdr_data_integer_firstabsoluteevaluationhscp. mdr_eb_data_integer_firstabsoluteevaluationhs = ff_q_mdr_data_integer_firstabsoluteevaluationhscp * S ((S (mdr_j_data_integer_firstabsoluteevaluationhsc)) * mdr_ec_data_integer_firstabsoluteevaluationhs) + (mdr_p_data_integer_firstabsoluteevaluationhsc))) /\ (((exists ff_h_mdr_data_integer_firstabsoluteevaluationhscn. ff_h_mdr_data_integer_firstabsoluteevaluationhscn + S (mdr_n_data_integer_firstabsoluteevaluationhsc) = S ((S (mdr_j_data_integer_firstabsoluteevaluationhsc)) * mdr_fc_data_integer_firstabsoluteevaluationhs)) /\ exists ff_q_mdr_data_integer_firstabsoluteevaluationhscn. mdr_fb_data_integer_firstabsoluteevaluationhs = ff_q_mdr_data_integer_firstabsoluteevaluationhscn * S ((S (mdr_j_data_integer_firstabsoluteevaluationhsc)) * mdr_fc_data_integer_firstabsoluteevaluationhs) + (mdr_n_data_integer_firstabsoluteevaluationhsc)))))))) /\ (exists ff_ub_mce_fold_mdr_data_integer_firstabsoluteevaluationhsf ff_uc_mce_fold_mdr_data_integer_firstabsoluteevaluationhsf ff_vb_mce_fold_mdr_data_integer_firstabsoluteevaluationhsf ff_vc_mce_fold_mdr_data_integer_firstabsoluteevaluationhsf. ((forall ff_index_mce_alternating_mdr_data_integer_firstabsoluteevaluationhsf_prefix. (exists ff_gap_mce_mdr_data_integer_firstabsoluteevaluationhsf_prefix_index. ff_gap_mce_mdr_data_integer_firstabsoluteevaluationhsf_prefix_index + S (ff_index_mce_alternating_mdr_data_integer_firstabsoluteevaluationhsf_prefix) = (S (mdr_q_data_integer_firstabsoluteevaluationhs))) -> exists ff_ap_mce_alternating_mdr_data_integer_firstabsoluteevaluationhsf_prefix ff_an_mce_alternating_mdr_data_integer_firstabsoluteevaluationhsf_prefix ff_bp_mce_alternating_mdr_data_integer_firstabsoluteevaluationhsf_prefix ff_bn_mce_alternating_mdr_data_integer_firstabsoluteevaluationhsf_prefix ff_p_mce_alternating_mdr_data_integer_firstabsoluteevaluationhsf_prefix ff_n_mce_alternating_mdr_data_integer_firstabsoluteevaluationhsf_prefix. ((((exists ff_h_mce_mdr_data_integer_firstabsoluteevaluationhsf_prefix_ap. ff_h_mce_mdr_data_integer_firstabsoluteevaluationhsf_prefix_ap + S (ff_ap_mce_alternating_mdr_data_integer_firstabsoluteevaluationhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_data_integer_firstabsoluteevaluationhsf_prefix)) * mdr_pc_data_integer_firstabsoluteevaluationh)) /\ exists ff_q_mce_mdr_data_integer_firstabsoluteevaluationhsf_prefix_ap. mdr_pb_data_integer_firstabsoluteevaluationh = ff_q_mce_mdr_data_integer_firstabsoluteevaluationhsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_data_integer_firstabsoluteevaluationhsf_prefix)) * mdr_pc_data_integer_firstabsoluteevaluationh) + (ff_ap_mce_alternating_mdr_data_integer_firstabsoluteevaluationhsf_prefix))) /\ ((((exists ff_h_mce_mdr_data_integer_firstabsoluteevaluationhsf_prefix_an. ff_h_mce_mdr_data_integer_firstabsoluteevaluationhsf_prefix_an + S (ff_an_mce_alternating_mdr_data_integer_firstabsoluteevaluationhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_data_integer_firstabsoluteevaluationhsf_prefix)) * mdr_nc_data_integer_firstabsoluteevaluationh)) /\ exists ff_q_mce_mdr_data_integer_firstabsoluteevaluationhsf_prefix_an. mdr_nb_data_integer_firstabsoluteevaluationh = ff_q_mce_mdr_data_integer_firstabsoluteevaluationhsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_data_integer_firstabsoluteevaluationhsf_prefix)) * mdr_nc_data_integer_firstabsoluteevaluationh) + (ff_an_mce_alternating_mdr_data_integer_firstabsoluteevaluationhsf_prefix))) /\ ((((exists ff_h_mce_mdr_data_integer_firstabsoluteevaluationhsf_prefix_bp. ff_h_mce_mdr_data_integer_firstabsoluteevaluationhsf_prefix_bp + S (ff_bp_mce_alternating_mdr_data_integer_firstabsoluteevaluationhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_data_integer_firstabsoluteevaluationhsf_prefix)) * mdr_ec_data_integer_firstabsoluteevaluationhs)) /\ exists ff_q_mce_mdr_data_integer_firstabsoluteevaluationhsf_prefix_bp. mdr_eb_data_integer_firstabsoluteevaluationhs = ff_q_mce_mdr_data_integer_firstabsoluteevaluationhsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_data_integer_firstabsoluteevaluationhsf_prefix)) * mdr_ec_data_integer_firstabsoluteevaluationhs) + (ff_bp_mce_alternating_mdr_data_integer_firstabsoluteevaluationhsf_prefix))) /\ ((((exists ff_h_mce_mdr_data_integer_firstabsoluteevaluationhsf_prefix_bn. ff_h_mce_mdr_data_integer_firstabsoluteevaluationhsf_prefix_bn + S (ff_bn_mce_alternating_mdr_data_integer_firstabsoluteevaluationhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_data_integer_firstabsoluteevaluationhsf_prefix)) * mdr_fc_data_integer_firstabsoluteevaluationhs)) /\ exists ff_q_mce_mdr_data_integer_firstabsoluteevaluationhsf_prefix_bn. mdr_fb_data_integer_firstabsoluteevaluationhs = ff_q_mce_mdr_data_integer_firstabsoluteevaluationhsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_data_integer_firstabsoluteevaluationhsf_prefix)) * mdr_fc_data_integer_firstabsoluteevaluationhs) + (ff_bn_mce_alternating_mdr_data_integer_firstabsoluteevaluationhsf_prefix))) /\ ((((exists ff_h_mce_mdr_data_integer_firstabsoluteevaluationhsf_prefix_positive. ff_h_mce_mdr_data_integer_firstabsoluteevaluationhsf_prefix_positive + S (ff_p_mce_alternating_mdr_data_integer_firstabsoluteevaluationhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_data_integer_firstabsoluteevaluationhsf_prefix)) * ff_uc_mce_fold_mdr_data_integer_firstabsoluteevaluationhsf)) /\ exists ff_q_mce_mdr_data_integer_firstabsoluteevaluationhsf_prefix_positive. ff_ub_mce_fold_mdr_data_integer_firstabsoluteevaluationhsf = ff_q_mce_mdr_data_integer_firstabsoluteevaluationhsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_data_integer_firstabsoluteevaluationhsf_prefix)) * ff_uc_mce_fold_mdr_data_integer_firstabsoluteevaluationhsf) + (ff_p_mce_alternating_mdr_data_integer_firstabsoluteevaluationhsf_prefix))) /\ ((((exists ff_h_mce_mdr_data_integer_firstabsoluteevaluationhsf_prefix_negative. ff_h_mce_mdr_data_integer_firstabsoluteevaluationhsf_prefix_negative + S (ff_n_mce_alternating_mdr_data_integer_firstabsoluteevaluationhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_data_integer_firstabsoluteevaluationhsf_prefix)) * ff_vc_mce_fold_mdr_data_integer_firstabsoluteevaluationhsf)) /\ exists ff_q_mce_mdr_data_integer_firstabsoluteevaluationhsf_prefix_negative. ff_vb_mce_fold_mdr_data_integer_firstabsoluteevaluationhsf = ff_q_mce_mdr_data_integer_firstabsoluteevaluationhsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_data_integer_firstabsoluteevaluationhsf_prefix)) * ff_vc_mce_fold_mdr_data_integer_firstabsoluteevaluationhsf) + (ff_n_mce_alternating_mdr_data_integer_firstabsoluteevaluationhsf_prefix))) /\ (((exists ff_even_mce_term_mdr_data_integer_firstabsoluteevaluationhsf_prefix_term. ff_index_mce_alternating_mdr_data_integer_firstabsoluteevaluationhsf_prefix = 2 * ff_even_mce_term_mdr_data_integer_firstabsoluteevaluationhsf_prefix_term) /\ (ff_p_mce_alternating_mdr_data_integer_firstabsoluteevaluationhsf_prefix = (ff_ap_mce_alternating_mdr_data_integer_firstabsoluteevaluationhsf_prefix) * (ff_bp_mce_alternating_mdr_data_integer_firstabsoluteevaluationhsf_prefix) + (ff_an_mce_alternating_mdr_data_integer_firstabsoluteevaluationhsf_prefix) * (ff_bn_mce_alternating_mdr_data_integer_firstabsoluteevaluationhsf_prefix) /\ ff_n_mce_alternating_mdr_data_integer_firstabsoluteevaluationhsf_prefix = (ff_ap_mce_alternating_mdr_data_integer_firstabsoluteevaluationhsf_prefix) * (ff_bn_mce_alternating_mdr_data_integer_firstabsoluteevaluationhsf_prefix) + (ff_an_mce_alternating_mdr_data_integer_firstabsoluteevaluationhsf_prefix) * (ff_bp_mce_alternating_mdr_data_integer_firstabsoluteevaluationhsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_data_integer_firstabsoluteevaluationhsf_prefix_term. ff_index_mce_alternating_mdr_data_integer_firstabsoluteevaluationhsf_prefix = 2 * ff_odd_mce_term_mdr_data_integer_firstabsoluteevaluationhsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_data_integer_firstabsoluteevaluationhsf_prefix = (ff_ap_mce_alternating_mdr_data_integer_firstabsoluteevaluationhsf_prefix) * (ff_bn_mce_alternating_mdr_data_integer_firstabsoluteevaluationhsf_prefix) + (ff_an_mce_alternating_mdr_data_integer_firstabsoluteevaluationhsf_prefix) * (ff_bp_mce_alternating_mdr_data_integer_firstabsoluteevaluationhsf_prefix) /\ ff_n_mce_alternating_mdr_data_integer_firstabsoluteevaluationhsf_prefix = (ff_ap_mce_alternating_mdr_data_integer_firstabsoluteevaluationhsf_prefix) * (ff_bp_mce_alternating_mdr_data_integer_firstabsoluteevaluationhsf_prefix) + (ff_an_mce_alternating_mdr_data_integer_firstabsoluteevaluationhsf_prefix) * (ff_bn_mce_alternating_mdr_data_integer_firstabsoluteevaluationhsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_data_integer_firstabsoluteevaluationhsf_positive ff_v_mce_mdr_data_integer_firstabsoluteevaluationhsf_positive. ((((exists ff_h_mce_mdr_data_integer_firstabsoluteevaluationhsf_positive_start. ff_h_mce_mdr_data_integer_firstabsoluteevaluationhsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_data_integer_firstabsoluteevaluationhsf_positive)) /\ exists ff_q_mce_mdr_data_integer_firstabsoluteevaluationhsf_positive_start. ff_u_mce_mdr_data_integer_firstabsoluteevaluationhsf_positive = ff_q_mce_mdr_data_integer_firstabsoluteevaluationhsf_positive_start * S ((S (0)) * ff_v_mce_mdr_data_integer_firstabsoluteevaluationhsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_data_integer_firstabsoluteevaluationhsf_positive_terminal. ff_h_mce_mdr_data_integer_firstabsoluteevaluationhsf_positive_terminal + S (mdr_p_data_integer_firstabsoluteevaluationh) = S ((S ((S (mdr_q_data_integer_firstabsoluteevaluationhs)))) * ff_v_mce_mdr_data_integer_firstabsoluteevaluationhsf_positive)) /\ exists ff_q_mce_mdr_data_integer_firstabsoluteevaluationhsf_positive_terminal. ff_u_mce_mdr_data_integer_firstabsoluteevaluationhsf_positive = ff_q_mce_mdr_data_integer_firstabsoluteevaluationhsf_positive_terminal * S ((S ((S (mdr_q_data_integer_firstabsoluteevaluationhs)))) * ff_v_mce_mdr_data_integer_firstabsoluteevaluationhsf_positive) + (mdr_p_data_integer_firstabsoluteevaluationh))) /\ forall ff_i_mce_mdr_data_integer_firstabsoluteevaluationhsf_positive. (exists ff_lt_mce_mdr_data_integer_firstabsoluteevaluationhsf_positive_bound. ff_lt_mce_mdr_data_integer_firstabsoluteevaluationhsf_positive_bound + S ff_i_mce_mdr_data_integer_firstabsoluteevaluationhsf_positive = (S (mdr_q_data_integer_firstabsoluteevaluationhs))) -> exists ff_a_mce_mdr_data_integer_firstabsoluteevaluationhsf_positive ff_r_mce_mdr_data_integer_firstabsoluteevaluationhsf_positive ff_s_mce_mdr_data_integer_firstabsoluteevaluationhsf_positive. ((((exists ff_h_mce_mdr_data_integer_firstabsoluteevaluationhsf_positive_summand. ff_h_mce_mdr_data_integer_firstabsoluteevaluationhsf_positive_summand + S (ff_a_mce_mdr_data_integer_firstabsoluteevaluationhsf_positive) = S ((S (ff_i_mce_mdr_data_integer_firstabsoluteevaluationhsf_positive)) * ff_uc_mce_fold_mdr_data_integer_firstabsoluteevaluationhsf)) /\ exists ff_q_mce_mdr_data_integer_firstabsoluteevaluationhsf_positive_summand. ff_ub_mce_fold_mdr_data_integer_firstabsoluteevaluationhsf = ff_q_mce_mdr_data_integer_firstabsoluteevaluationhsf_positive_summand * S ((S (ff_i_mce_mdr_data_integer_firstabsoluteevaluationhsf_positive)) * ff_uc_mce_fold_mdr_data_integer_firstabsoluteevaluationhsf) + (ff_a_mce_mdr_data_integer_firstabsoluteevaluationhsf_positive))) /\ ((((exists ff_h_mce_mdr_data_integer_firstabsoluteevaluationhsf_positive_partial. ff_h_mce_mdr_data_integer_firstabsoluteevaluationhsf_positive_partial + S (ff_r_mce_mdr_data_integer_firstabsoluteevaluationhsf_positive) = S ((S (ff_i_mce_mdr_data_integer_firstabsoluteevaluationhsf_positive)) * ff_v_mce_mdr_data_integer_firstabsoluteevaluationhsf_positive)) /\ exists ff_q_mce_mdr_data_integer_firstabsoluteevaluationhsf_positive_partial. ff_u_mce_mdr_data_integer_firstabsoluteevaluationhsf_positive = ff_q_mce_mdr_data_integer_firstabsoluteevaluationhsf_positive_partial * S ((S (ff_i_mce_mdr_data_integer_firstabsoluteevaluationhsf_positive)) * ff_v_mce_mdr_data_integer_firstabsoluteevaluationhsf_positive) + (ff_r_mce_mdr_data_integer_firstabsoluteevaluationhsf_positive))) /\ ((((exists ff_h_mce_mdr_data_integer_firstabsoluteevaluationhsf_positive_successor. ff_h_mce_mdr_data_integer_firstabsoluteevaluationhsf_positive_successor + S (ff_s_mce_mdr_data_integer_firstabsoluteevaluationhsf_positive) = S ((S (S ff_i_mce_mdr_data_integer_firstabsoluteevaluationhsf_positive)) * ff_v_mce_mdr_data_integer_firstabsoluteevaluationhsf_positive)) /\ exists ff_q_mce_mdr_data_integer_firstabsoluteevaluationhsf_positive_successor. ff_u_mce_mdr_data_integer_firstabsoluteevaluationhsf_positive = ff_q_mce_mdr_data_integer_firstabsoluteevaluationhsf_positive_successor * S ((S (S ff_i_mce_mdr_data_integer_firstabsoluteevaluationhsf_positive)) * ff_v_mce_mdr_data_integer_firstabsoluteevaluationhsf_positive) + (ff_s_mce_mdr_data_integer_firstabsoluteevaluationhsf_positive))) /\ ff_s_mce_mdr_data_integer_firstabsoluteevaluationhsf_positive = ff_r_mce_mdr_data_integer_firstabsoluteevaluationhsf_positive + ff_a_mce_mdr_data_integer_firstabsoluteevaluationhsf_positive)))))) /\ (exists ff_u_mce_mdr_data_integer_firstabsoluteevaluationhsf_negative ff_v_mce_mdr_data_integer_firstabsoluteevaluationhsf_negative. ((((exists ff_h_mce_mdr_data_integer_firstabsoluteevaluationhsf_negative_start. ff_h_mce_mdr_data_integer_firstabsoluteevaluationhsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_data_integer_firstabsoluteevaluationhsf_negative)) /\ exists ff_q_mce_mdr_data_integer_firstabsoluteevaluationhsf_negative_start. ff_u_mce_mdr_data_integer_firstabsoluteevaluationhsf_negative = ff_q_mce_mdr_data_integer_firstabsoluteevaluationhsf_negative_start * S ((S (0)) * ff_v_mce_mdr_data_integer_firstabsoluteevaluationhsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_data_integer_firstabsoluteevaluationhsf_negative_terminal. ff_h_mce_mdr_data_integer_firstabsoluteevaluationhsf_negative_terminal + S (mdr_n_data_integer_firstabsoluteevaluationh) = S ((S ((S (mdr_q_data_integer_firstabsoluteevaluationhs)))) * ff_v_mce_mdr_data_integer_firstabsoluteevaluationhsf_negative)) /\ exists ff_q_mce_mdr_data_integer_firstabsoluteevaluationhsf_negative_terminal. ff_u_mce_mdr_data_integer_firstabsoluteevaluationhsf_negative = ff_q_mce_mdr_data_integer_firstabsoluteevaluationhsf_negative_terminal * S ((S ((S (mdr_q_data_integer_firstabsoluteevaluationhs)))) * ff_v_mce_mdr_data_integer_firstabsoluteevaluationhsf_negative) + (mdr_n_data_integer_firstabsoluteevaluationh))) /\ forall ff_i_mce_mdr_data_integer_firstabsoluteevaluationhsf_negative. (exists ff_lt_mce_mdr_data_integer_firstabsoluteevaluationhsf_negative_bound. ff_lt_mce_mdr_data_integer_firstabsoluteevaluationhsf_negative_bound + S ff_i_mce_mdr_data_integer_firstabsoluteevaluationhsf_negative = (S (mdr_q_data_integer_firstabsoluteevaluationhs))) -> exists ff_a_mce_mdr_data_integer_firstabsoluteevaluationhsf_negative ff_r_mce_mdr_data_integer_firstabsoluteevaluationhsf_negative ff_s_mce_mdr_data_integer_firstabsoluteevaluationhsf_negative. ((((exists ff_h_mce_mdr_data_integer_firstabsoluteevaluationhsf_negative_summand. ff_h_mce_mdr_data_integer_firstabsoluteevaluationhsf_negative_summand + S (ff_a_mce_mdr_data_integer_firstabsoluteevaluationhsf_negative) = S ((S (ff_i_mce_mdr_data_integer_firstabsoluteevaluationhsf_negative)) * ff_vc_mce_fold_mdr_data_integer_firstabsoluteevaluationhsf)) /\ exists ff_q_mce_mdr_data_integer_firstabsoluteevaluationhsf_negative_summand. ff_vb_mce_fold_mdr_data_integer_firstabsoluteevaluationhsf = ff_q_mce_mdr_data_integer_firstabsoluteevaluationhsf_negative_summand * S ((S (ff_i_mce_mdr_data_integer_firstabsoluteevaluationhsf_negative)) * ff_vc_mce_fold_mdr_data_integer_firstabsoluteevaluationhsf) + (ff_a_mce_mdr_data_integer_firstabsoluteevaluationhsf_negative))) /\ ((((exists ff_h_mce_mdr_data_integer_firstabsoluteevaluationhsf_negative_partial. ff_h_mce_mdr_data_integer_firstabsoluteevaluationhsf_negative_partial + S (ff_r_mce_mdr_data_integer_firstabsoluteevaluationhsf_negative) = S ((S (ff_i_mce_mdr_data_integer_firstabsoluteevaluationhsf_negative)) * ff_v_mce_mdr_data_integer_firstabsoluteevaluationhsf_negative)) /\ exists ff_q_mce_mdr_data_integer_firstabsoluteevaluationhsf_negative_partial. ff_u_mce_mdr_data_integer_firstabsoluteevaluationhsf_negative = ff_q_mce_mdr_data_integer_firstabsoluteevaluationhsf_negative_partial * S ((S (ff_i_mce_mdr_data_integer_firstabsoluteevaluationhsf_negative)) * ff_v_mce_mdr_data_integer_firstabsoluteevaluationhsf_negative) + (ff_r_mce_mdr_data_integer_firstabsoluteevaluationhsf_negative))) /\ ((((exists ff_h_mce_mdr_data_integer_firstabsoluteevaluationhsf_negative_successor. ff_h_mce_mdr_data_integer_firstabsoluteevaluationhsf_negative_successor + S (ff_s_mce_mdr_data_integer_firstabsoluteevaluationhsf_negative) = S ((S (S ff_i_mce_mdr_data_integer_firstabsoluteevaluationhsf_negative)) * ff_v_mce_mdr_data_integer_firstabsoluteevaluationhsf_negative)) /\ exists ff_q_mce_mdr_data_integer_firstabsoluteevaluationhsf_negative_successor. ff_u_mce_mdr_data_integer_firstabsoluteevaluationhsf_negative = ff_q_mce_mdr_data_integer_firstabsoluteevaluationhsf_negative_successor * S ((S (S ff_i_mce_mdr_data_integer_firstabsoluteevaluationhsf_negative)) * ff_v_mce_mdr_data_integer_firstabsoluteevaluationhsf_negative) + (ff_s_mce_mdr_data_integer_firstabsoluteevaluationhsf_negative))) /\ ff_s_mce_mdr_data_integer_firstabsoluteevaluationhsf_negative = ff_r_mce_mdr_data_integer_firstabsoluteevaluationhsf_negative + ff_a_mce_mdr_data_integer_firstabsoluteevaluationhsf_negative))))))))))))))) /\ ((exists mdr_gap_data_integer_firstabsoluteevaluationi. mdr_gap_data_integer_firstabsoluteevaluationi + S (mdr_i_data_integer_firstabsoluteevaluation) = (mdr_l_data_integer_firstabsoluteevaluation)) /\ (exists mdr_z_data_integer_firstabsoluteevaluationr. ((exists mdr_a_data_integer_firstabsoluteevaluationrc mdr_b_data_integer_firstabsoluteevaluationrc mdr_c_data_integer_firstabsoluteevaluationrc mdr_e_data_integer_firstabsoluteevaluationrc mdr_f_data_integer_firstabsoluteevaluationrc. ((mdr_a_data_integer_firstabsoluteevaluationrc = ((d) + (ab)) * S ((d) + (ab)) + ((ab) + (ab))) /\ ((mdr_b_data_integer_firstabsoluteevaluationrc = ((ac) + (bb)) * S ((ac) + (bb)) + ((bb) + (bb))) /\ ((mdr_c_data_integer_firstabsoluteevaluationrc = ((mdr_a_data_integer_firstabsoluteevaluationrc) + (mdr_b_data_integer_firstabsoluteevaluationrc)) * S ((mdr_a_data_integer_firstabsoluteevaluationrc) + (mdr_b_data_integer_firstabsoluteevaluationrc)) + ((mdr_b_data_integer_firstabsoluteevaluationrc) + (mdr_b_data_integer_firstabsoluteevaluationrc))) /\ ((mdr_e_data_integer_firstabsoluteevaluationrc = ((mdr_p_data_integer_firstabsolute) + (mdr_n_data_integer_firstabsolute)) * S ((mdr_p_data_integer_firstabsolute) + (mdr_n_data_integer_firstabsolute)) + ((mdr_n_data_integer_firstabsolute) + (mdr_n_data_integer_firstabsolute))) /\ ((mdr_f_data_integer_firstabsoluteevaluationrc = ((bc) + (mdr_e_data_integer_firstabsoluteevaluationrc)) * S ((bc) + (mdr_e_data_integer_firstabsoluteevaluationrc)) + ((mdr_e_data_integer_firstabsoluteevaluationrc) + (mdr_e_data_integer_firstabsoluteevaluationrc))) /\ ((mdr_z_data_integer_firstabsoluteevaluationr) = ((mdr_c_data_integer_firstabsoluteevaluationrc) + (mdr_f_data_integer_firstabsoluteevaluationrc)) * S ((mdr_c_data_integer_firstabsoluteevaluationrc) + (mdr_f_data_integer_firstabsoluteevaluationrc)) + ((mdr_f_data_integer_firstabsoluteevaluationrc) + (mdr_f_data_integer_firstabsoluteevaluationrc))))))))) /\ (((exists ff_h_mdr_data_integer_firstabsoluteevaluationrb. ff_h_mdr_data_integer_firstabsoluteevaluationrb + S (mdr_z_data_integer_firstabsoluteevaluationr) = S ((S (mdr_i_data_integer_firstabsoluteevaluation)) * mdr_c_data_integer_firstabsoluteevaluation)) /\ exists ff_q_mdr_data_integer_firstabsoluteevaluationrb. mdr_b_data_integer_firstabsoluteevaluation = ff_q_mdr_data_integer_firstabsoluteevaluationrb * S ((S (mdr_i_data_integer_firstabsoluteevaluation)) * mdr_c_data_integer_firstabsoluteevaluation) + (mdr_z_data_integer_firstabsoluteevaluationr)))))))) /\ (((mdr_p_data_integer_firstabsolute) = (mdr_n_data_integer_firstabsolute) + (D)) \/ ((mdr_n_data_integer_firstabsolute) = (mdr_p_data_integer_firstabsolute) + (D)))))))) -> (((~(d = 0)) /\ ((~(D = 0)) /\ (exists mdr_p_data_integer_secondabsolute mdr_n_data_integer_secondabsolute. ((exists mdr_b_data_integer_secondabsoluteevaluation mdr_c_data_integer_secondabsoluteevaluation mdr_l_data_integer_secondabsoluteevaluation mdr_i_data_integer_secondabsoluteevaluation. ((forall mdr_i_data_integer_secondabsoluteevaluationh. (exists mdr_gap_data_integer_secondabsoluteevaluationhi. mdr_gap_data_integer_secondabsoluteevaluationhi + S (mdr_i_data_integer_secondabsoluteevaluationh) = (mdr_l_data_integer_secondabsoluteevaluation)) -> exists mdr_d_data_integer_secondabsoluteevaluationh mdr_pb_data_integer_secondabsoluteevaluationh mdr_pc_data_integer_secondabsoluteevaluationh mdr_nb_data_integer_secondabsoluteevaluationh mdr_nc_data_integer_secondabsoluteevaluationh mdr_p_data_integer_secondabsoluteevaluationh mdr_n_data_integer_secondabsoluteevaluationh. ((exists mdr_z_data_integer_secondabsoluteevaluationhr. ((exists mdr_a_data_integer_secondabsoluteevaluationhrc mdr_b_data_integer_secondabsoluteevaluationhrc mdr_c_data_integer_secondabsoluteevaluationhrc mdr_e_data_integer_secondabsoluteevaluationhrc mdr_f_data_integer_secondabsoluteevaluationhrc. ((mdr_a_data_integer_secondabsoluteevaluationhrc = ((mdr_d_data_integer_secondabsoluteevaluationh) + (mdr_pb_data_integer_secondabsoluteevaluationh)) * S ((mdr_d_data_integer_secondabsoluteevaluationh) + (mdr_pb_data_integer_secondabsoluteevaluationh)) + ((mdr_pb_data_integer_secondabsoluteevaluationh) + (mdr_pb_data_integer_secondabsoluteevaluationh))) /\ ((mdr_b_data_integer_secondabsoluteevaluationhrc = ((mdr_pc_data_integer_secondabsoluteevaluationh) + (mdr_nb_data_integer_secondabsoluteevaluationh)) * S ((mdr_pc_data_integer_secondabsoluteevaluationh) + (mdr_nb_data_integer_secondabsoluteevaluationh)) + ((mdr_nb_data_integer_secondabsoluteevaluationh) + (mdr_nb_data_integer_secondabsoluteevaluationh))) /\ ((mdr_c_data_integer_secondabsoluteevaluationhrc = ((mdr_a_data_integer_secondabsoluteevaluationhrc) + (mdr_b_data_integer_secondabsoluteevaluationhrc)) * S ((mdr_a_data_integer_secondabsoluteevaluationhrc) + (mdr_b_data_integer_secondabsoluteevaluationhrc)) + ((mdr_b_data_integer_secondabsoluteevaluationhrc) + (mdr_b_data_integer_secondabsoluteevaluationhrc))) /\ ((mdr_e_data_integer_secondabsoluteevaluationhrc = ((mdr_p_data_integer_secondabsoluteevaluationh) + (mdr_n_data_integer_secondabsoluteevaluationh)) * S ((mdr_p_data_integer_secondabsoluteevaluationh) + (mdr_n_data_integer_secondabsoluteevaluationh)) + ((mdr_n_data_integer_secondabsoluteevaluationh) + (mdr_n_data_integer_secondabsoluteevaluationh))) /\ ((mdr_f_data_integer_secondabsoluteevaluationhrc = ((mdr_nc_data_integer_secondabsoluteevaluationh) + (mdr_e_data_integer_secondabsoluteevaluationhrc)) * S ((mdr_nc_data_integer_secondabsoluteevaluationh) + (mdr_e_data_integer_secondabsoluteevaluationhrc)) + ((mdr_e_data_integer_secondabsoluteevaluationhrc) + (mdr_e_data_integer_secondabsoluteevaluationhrc))) /\ ((mdr_z_data_integer_secondabsoluteevaluationhr) = ((mdr_c_data_integer_secondabsoluteevaluationhrc) + (mdr_f_data_integer_secondabsoluteevaluationhrc)) * S ((mdr_c_data_integer_secondabsoluteevaluationhrc) + (mdr_f_data_integer_secondabsoluteevaluationhrc)) + ((mdr_f_data_integer_secondabsoluteevaluationhrc) + (mdr_f_data_integer_secondabsoluteevaluationhrc))))))))) /\ (((exists ff_h_mdr_data_integer_secondabsoluteevaluationhrb. ff_h_mdr_data_integer_secondabsoluteevaluationhrb + S (mdr_z_data_integer_secondabsoluteevaluationhr) = S ((S (mdr_i_data_integer_secondabsoluteevaluationh)) * mdr_c_data_integer_secondabsoluteevaluation)) /\ exists ff_q_mdr_data_integer_secondabsoluteevaluationhrb. mdr_b_data_integer_secondabsoluteevaluation = ff_q_mdr_data_integer_secondabsoluteevaluationhrb * S ((S (mdr_i_data_integer_secondabsoluteevaluationh)) * mdr_c_data_integer_secondabsoluteevaluation) + (mdr_z_data_integer_secondabsoluteevaluationhr))))) /\ (((((mdr_d_data_integer_secondabsoluteevaluationh) = 0) /\ (((mdr_p_data_integer_secondabsoluteevaluationh) = 1) /\ ((mdr_n_data_integer_secondabsoluteevaluationh) = 0))) \/ exists mdr_q_data_integer_secondabsoluteevaluationhs mdr_eb_data_integer_secondabsoluteevaluationhs mdr_ec_data_integer_secondabsoluteevaluationhs mdr_fb_data_integer_secondabsoluteevaluationhs mdr_fc_data_integer_secondabsoluteevaluationhs. (((mdr_d_data_integer_secondabsoluteevaluationh) = S (mdr_q_data_integer_secondabsoluteevaluationhs)) /\ ((forall mdr_j_data_integer_secondabsoluteevaluationhsc. (exists mdr_gap_data_integer_secondabsoluteevaluationhscj. mdr_gap_data_integer_secondabsoluteevaluationhscj + S (mdr_j_data_integer_secondabsoluteevaluationhsc) = (S (mdr_q_data_integer_secondabsoluteevaluationhs))) -> exists mdr_i_data_integer_secondabsoluteevaluationhsc mdr_up_data_integer_secondabsoluteevaluationhsc mdr_us_data_integer_secondabsoluteevaluationhsc mdr_un_data_integer_secondabsoluteevaluationhsc mdr_ut_data_integer_secondabsoluteevaluationhsc mdr_p_data_integer_secondabsoluteevaluationhsc mdr_n_data_integer_secondabsoluteevaluationhsc. ((exists mdr_gap_data_integer_secondabsoluteevaluationhsci. mdr_gap_data_integer_secondabsoluteevaluationhsci + S (mdr_i_data_integer_secondabsoluteevaluationhsc) = (mdr_i_data_integer_secondabsoluteevaluationh)) /\ ((exists mdr_z_data_integer_secondabsoluteevaluationhscr. ((exists mdr_a_data_integer_secondabsoluteevaluationhscrc mdr_b_data_integer_secondabsoluteevaluationhscrc mdr_c_data_integer_secondabsoluteevaluationhscrc mdr_e_data_integer_secondabsoluteevaluationhscrc mdr_f_data_integer_secondabsoluteevaluationhscrc. ((mdr_a_data_integer_secondabsoluteevaluationhscrc = ((mdr_q_data_integer_secondabsoluteevaluationhs) + (mdr_up_data_integer_secondabsoluteevaluationhsc)) * S ((mdr_q_data_integer_secondabsoluteevaluationhs) + (mdr_up_data_integer_secondabsoluteevaluationhsc)) + ((mdr_up_data_integer_secondabsoluteevaluationhsc) + (mdr_up_data_integer_secondabsoluteevaluationhsc))) /\ ((mdr_b_data_integer_secondabsoluteevaluationhscrc = ((mdr_us_data_integer_secondabsoluteevaluationhsc) + (mdr_un_data_integer_secondabsoluteevaluationhsc)) * S ((mdr_us_data_integer_secondabsoluteevaluationhsc) + (mdr_un_data_integer_secondabsoluteevaluationhsc)) + ((mdr_un_data_integer_secondabsoluteevaluationhsc) + (mdr_un_data_integer_secondabsoluteevaluationhsc))) /\ ((mdr_c_data_integer_secondabsoluteevaluationhscrc = ((mdr_a_data_integer_secondabsoluteevaluationhscrc) + (mdr_b_data_integer_secondabsoluteevaluationhscrc)) * S ((mdr_a_data_integer_secondabsoluteevaluationhscrc) + (mdr_b_data_integer_secondabsoluteevaluationhscrc)) + ((mdr_b_data_integer_secondabsoluteevaluationhscrc) + (mdr_b_data_integer_secondabsoluteevaluationhscrc))) /\ ((mdr_e_data_integer_secondabsoluteevaluationhscrc = ((mdr_p_data_integer_secondabsoluteevaluationhsc) + (mdr_n_data_integer_secondabsoluteevaluationhsc)) * S ((mdr_p_data_integer_secondabsoluteevaluationhsc) + (mdr_n_data_integer_secondabsoluteevaluationhsc)) + ((mdr_n_data_integer_secondabsoluteevaluationhsc) + (mdr_n_data_integer_secondabsoluteevaluationhsc))) /\ ((mdr_f_data_integer_secondabsoluteevaluationhscrc = ((mdr_ut_data_integer_secondabsoluteevaluationhsc) + (mdr_e_data_integer_secondabsoluteevaluationhscrc)) * S ((mdr_ut_data_integer_secondabsoluteevaluationhsc) + (mdr_e_data_integer_secondabsoluteevaluationhscrc)) + ((mdr_e_data_integer_secondabsoluteevaluationhscrc) + (mdr_e_data_integer_secondabsoluteevaluationhscrc))) /\ ((mdr_z_data_integer_secondabsoluteevaluationhscr) = ((mdr_c_data_integer_secondabsoluteevaluationhscrc) + (mdr_f_data_integer_secondabsoluteevaluationhscrc)) * S ((mdr_c_data_integer_secondabsoluteevaluationhscrc) + (mdr_f_data_integer_secondabsoluteevaluationhscrc)) + ((mdr_f_data_integer_secondabsoluteevaluationhscrc) + (mdr_f_data_integer_secondabsoluteevaluationhscrc))))))))) /\ (((exists ff_h_mdr_data_integer_secondabsoluteevaluationhscrb. ff_h_mdr_data_integer_secondabsoluteevaluationhscrb + S (mdr_z_data_integer_secondabsoluteevaluationhscr) = S ((S (mdr_i_data_integer_secondabsoluteevaluationhsc)) * mdr_c_data_integer_secondabsoluteevaluation)) /\ exists ff_q_mdr_data_integer_secondabsoluteevaluationhscrb. mdr_b_data_integer_secondabsoluteevaluation = ff_q_mdr_data_integer_secondabsoluteevaluationhscrb * S ((S (mdr_i_data_integer_secondabsoluteevaluationhsc)) * mdr_c_data_integer_secondabsoluteevaluation) + (mdr_z_data_integer_secondabsoluteevaluationhscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_data_integer_secondabsoluteevaluationhscm_positive. (exists ff_gap_mdm_lt_mdr_data_integer_secondabsoluteevaluationhscm_positive_index_bound. ff_gap_mdm_lt_mdr_data_integer_secondabsoluteevaluationhscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_data_integer_secondabsoluteevaluationhscm_positive) = ((mdr_q_data_integer_secondabsoluteevaluationhs) * (mdr_q_data_integer_secondabsoluteevaluationhs))) -> exists ff_row_mdm_prefix_mdr_data_integer_secondabsoluteevaluationhscm_positive ff_column_mdm_prefix_mdr_data_integer_secondabsoluteevaluationhscm_positive ff_value_mdm_prefix_mdr_data_integer_secondabsoluteevaluationhscm_positive. (ff_index_mdm_prefix_mdr_data_integer_secondabsoluteevaluationhscm_positive = (mdr_q_data_integer_secondabsoluteevaluationhs) * ff_row_mdm_prefix_mdr_data_integer_secondabsoluteevaluationhscm_positive + ff_column_mdm_prefix_mdr_data_integer_secondabsoluteevaluationhscm_positive /\ ((exists ff_gap_mdm_lt_mdr_data_integer_secondabsoluteevaluationhscm_positive_column_bound. ff_gap_mdm_lt_mdr_data_integer_secondabsoluteevaluationhscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_data_integer_secondabsoluteevaluationhscm_positive) = (mdr_q_data_integer_secondabsoluteevaluationhs)) /\ ((exists ff_row_mdm_cell_mdr_data_integer_secondabsoluteevaluationhscm_positive_cell ff_column_mdm_cell_mdr_data_integer_secondabsoluteevaluationhscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_data_integer_secondabsoluteevaluationhscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_data_integer_secondabsoluteevaluationhscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_data_integer_secondabsoluteevaluationhscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_data_integer_secondabsoluteevaluationhscm_positive_cell = ff_row_mdm_prefix_mdr_data_integer_secondabsoluteevaluationhscm_positive) \/ ((exists ff_gap_mdm_le_mdr_data_integer_secondabsoluteevaluationhscm_positive_cell_row_after. ff_gap_mdm_le_mdr_data_integer_secondabsoluteevaluationhscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_data_integer_secondabsoluteevaluationhscm_positive)) /\ ff_row_mdm_cell_mdr_data_integer_secondabsoluteevaluationhscm_positive_cell = S ff_row_mdm_prefix_mdr_data_integer_secondabsoluteevaluationhscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_data_integer_secondabsoluteevaluationhscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_data_integer_secondabsoluteevaluationhscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_data_integer_secondabsoluteevaluationhscm_positive) = (mdr_j_data_integer_secondabsoluteevaluationhsc)) /\ ff_column_mdm_cell_mdr_data_integer_secondabsoluteevaluationhscm_positive_cell = ff_column_mdm_prefix_mdr_data_integer_secondabsoluteevaluationhscm_positive) \/ ((exists ff_gap_mdm_le_mdr_data_integer_secondabsoluteevaluationhscm_positive_cell_column_after. ff_gap_mdm_le_mdr_data_integer_secondabsoluteevaluationhscm_positive_cell_column_after + (mdr_j_data_integer_secondabsoluteevaluationhsc) = (ff_column_mdm_prefix_mdr_data_integer_secondabsoluteevaluationhscm_positive)) /\ ff_column_mdm_cell_mdr_data_integer_secondabsoluteevaluationhscm_positive_cell = S ff_column_mdm_prefix_mdr_data_integer_secondabsoluteevaluationhscm_positive))) /\ (((exists ff_h_mdm_mdr_data_integer_secondabsoluteevaluationhscm_positive_cell_source. ff_h_mdm_mdr_data_integer_secondabsoluteevaluationhscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_data_integer_secondabsoluteevaluationhscm_positive) = S ((S ((ff_row_mdm_cell_mdr_data_integer_secondabsoluteevaluationhscm_positive_cell) * (S (mdr_q_data_integer_secondabsoluteevaluationhs)) + (ff_column_mdm_cell_mdr_data_integer_secondabsoluteevaluationhscm_positive_cell))) * mdr_pc_data_integer_secondabsoluteevaluationh)) /\ exists ff_q_mdm_mdr_data_integer_secondabsoluteevaluationhscm_positive_cell_source. mdr_pb_data_integer_secondabsoluteevaluationh = ff_q_mdm_mdr_data_integer_secondabsoluteevaluationhscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_data_integer_secondabsoluteevaluationhscm_positive_cell) * (S (mdr_q_data_integer_secondabsoluteevaluationhs)) + (ff_column_mdm_cell_mdr_data_integer_secondabsoluteevaluationhscm_positive_cell))) * mdr_pc_data_integer_secondabsoluteevaluationh) + (ff_value_mdm_prefix_mdr_data_integer_secondabsoluteevaluationhscm_positive)))))) /\ (((exists ff_h_mdm_mdr_data_integer_secondabsoluteevaluationhscm_positive_target. ff_h_mdm_mdr_data_integer_secondabsoluteevaluationhscm_positive_target + S (ff_value_mdm_prefix_mdr_data_integer_secondabsoluteevaluationhscm_positive) = S ((S (ff_index_mdm_prefix_mdr_data_integer_secondabsoluteevaluationhscm_positive)) * mdr_us_data_integer_secondabsoluteevaluationhsc)) /\ exists ff_q_mdm_mdr_data_integer_secondabsoluteevaluationhscm_positive_target. mdr_up_data_integer_secondabsoluteevaluationhsc = ff_q_mdm_mdr_data_integer_secondabsoluteevaluationhscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_data_integer_secondabsoluteevaluationhscm_positive)) * mdr_us_data_integer_secondabsoluteevaluationhsc) + (ff_value_mdm_prefix_mdr_data_integer_secondabsoluteevaluationhscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_data_integer_secondabsoluteevaluationhscm_negative. (exists ff_gap_mdm_lt_mdr_data_integer_secondabsoluteevaluationhscm_negative_index_bound. ff_gap_mdm_lt_mdr_data_integer_secondabsoluteevaluationhscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_data_integer_secondabsoluteevaluationhscm_negative) = ((mdr_q_data_integer_secondabsoluteevaluationhs) * (mdr_q_data_integer_secondabsoluteevaluationhs))) -> exists ff_row_mdm_prefix_mdr_data_integer_secondabsoluteevaluationhscm_negative ff_column_mdm_prefix_mdr_data_integer_secondabsoluteevaluationhscm_negative ff_value_mdm_prefix_mdr_data_integer_secondabsoluteevaluationhscm_negative. (ff_index_mdm_prefix_mdr_data_integer_secondabsoluteevaluationhscm_negative = (mdr_q_data_integer_secondabsoluteevaluationhs) * ff_row_mdm_prefix_mdr_data_integer_secondabsoluteevaluationhscm_negative + ff_column_mdm_prefix_mdr_data_integer_secondabsoluteevaluationhscm_negative /\ ((exists ff_gap_mdm_lt_mdr_data_integer_secondabsoluteevaluationhscm_negative_column_bound. ff_gap_mdm_lt_mdr_data_integer_secondabsoluteevaluationhscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_data_integer_secondabsoluteevaluationhscm_negative) = (mdr_q_data_integer_secondabsoluteevaluationhs)) /\ ((exists ff_row_mdm_cell_mdr_data_integer_secondabsoluteevaluationhscm_negative_cell ff_column_mdm_cell_mdr_data_integer_secondabsoluteevaluationhscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_data_integer_secondabsoluteevaluationhscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_data_integer_secondabsoluteevaluationhscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_data_integer_secondabsoluteevaluationhscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_data_integer_secondabsoluteevaluationhscm_negative_cell = ff_row_mdm_prefix_mdr_data_integer_secondabsoluteevaluationhscm_negative) \/ ((exists ff_gap_mdm_le_mdr_data_integer_secondabsoluteevaluationhscm_negative_cell_row_after. ff_gap_mdm_le_mdr_data_integer_secondabsoluteevaluationhscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_data_integer_secondabsoluteevaluationhscm_negative)) /\ ff_row_mdm_cell_mdr_data_integer_secondabsoluteevaluationhscm_negative_cell = S ff_row_mdm_prefix_mdr_data_integer_secondabsoluteevaluationhscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_data_integer_secondabsoluteevaluationhscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_data_integer_secondabsoluteevaluationhscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_data_integer_secondabsoluteevaluationhscm_negative) = (mdr_j_data_integer_secondabsoluteevaluationhsc)) /\ ff_column_mdm_cell_mdr_data_integer_secondabsoluteevaluationhscm_negative_cell = ff_column_mdm_prefix_mdr_data_integer_secondabsoluteevaluationhscm_negative) \/ ((exists ff_gap_mdm_le_mdr_data_integer_secondabsoluteevaluationhscm_negative_cell_column_after. ff_gap_mdm_le_mdr_data_integer_secondabsoluteevaluationhscm_negative_cell_column_after + (mdr_j_data_integer_secondabsoluteevaluationhsc) = (ff_column_mdm_prefix_mdr_data_integer_secondabsoluteevaluationhscm_negative)) /\ ff_column_mdm_cell_mdr_data_integer_secondabsoluteevaluationhscm_negative_cell = S ff_column_mdm_prefix_mdr_data_integer_secondabsoluteevaluationhscm_negative))) /\ (((exists ff_h_mdm_mdr_data_integer_secondabsoluteevaluationhscm_negative_cell_source. ff_h_mdm_mdr_data_integer_secondabsoluteevaluationhscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_data_integer_secondabsoluteevaluationhscm_negative) = S ((S ((ff_row_mdm_cell_mdr_data_integer_secondabsoluteevaluationhscm_negative_cell) * (S (mdr_q_data_integer_secondabsoluteevaluationhs)) + (ff_column_mdm_cell_mdr_data_integer_secondabsoluteevaluationhscm_negative_cell))) * mdr_nc_data_integer_secondabsoluteevaluationh)) /\ exists ff_q_mdm_mdr_data_integer_secondabsoluteevaluationhscm_negative_cell_source. mdr_nb_data_integer_secondabsoluteevaluationh = ff_q_mdm_mdr_data_integer_secondabsoluteevaluationhscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_data_integer_secondabsoluteevaluationhscm_negative_cell) * (S (mdr_q_data_integer_secondabsoluteevaluationhs)) + (ff_column_mdm_cell_mdr_data_integer_secondabsoluteevaluationhscm_negative_cell))) * mdr_nc_data_integer_secondabsoluteevaluationh) + (ff_value_mdm_prefix_mdr_data_integer_secondabsoluteevaluationhscm_negative)))))) /\ (((exists ff_h_mdm_mdr_data_integer_secondabsoluteevaluationhscm_negative_target. ff_h_mdm_mdr_data_integer_secondabsoluteevaluationhscm_negative_target + S (ff_value_mdm_prefix_mdr_data_integer_secondabsoluteevaluationhscm_negative) = S ((S (ff_index_mdm_prefix_mdr_data_integer_secondabsoluteevaluationhscm_negative)) * mdr_ut_data_integer_secondabsoluteevaluationhsc)) /\ exists ff_q_mdm_mdr_data_integer_secondabsoluteevaluationhscm_negative_target. mdr_un_data_integer_secondabsoluteevaluationhsc = ff_q_mdm_mdr_data_integer_secondabsoluteevaluationhscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_data_integer_secondabsoluteevaluationhscm_negative)) * mdr_ut_data_integer_secondabsoluteevaluationhsc) + (ff_value_mdm_prefix_mdr_data_integer_secondabsoluteevaluationhscm_negative))))))))) /\ ((((exists ff_h_mdr_data_integer_secondabsoluteevaluationhscp. ff_h_mdr_data_integer_secondabsoluteevaluationhscp + S (mdr_p_data_integer_secondabsoluteevaluationhsc) = S ((S (mdr_j_data_integer_secondabsoluteevaluationhsc)) * mdr_ec_data_integer_secondabsoluteevaluationhs)) /\ exists ff_q_mdr_data_integer_secondabsoluteevaluationhscp. mdr_eb_data_integer_secondabsoluteevaluationhs = ff_q_mdr_data_integer_secondabsoluteevaluationhscp * S ((S (mdr_j_data_integer_secondabsoluteevaluationhsc)) * mdr_ec_data_integer_secondabsoluteevaluationhs) + (mdr_p_data_integer_secondabsoluteevaluationhsc))) /\ (((exists ff_h_mdr_data_integer_secondabsoluteevaluationhscn. ff_h_mdr_data_integer_secondabsoluteevaluationhscn + S (mdr_n_data_integer_secondabsoluteevaluationhsc) = S ((S (mdr_j_data_integer_secondabsoluteevaluationhsc)) * mdr_fc_data_integer_secondabsoluteevaluationhs)) /\ exists ff_q_mdr_data_integer_secondabsoluteevaluationhscn. mdr_fb_data_integer_secondabsoluteevaluationhs = ff_q_mdr_data_integer_secondabsoluteevaluationhscn * S ((S (mdr_j_data_integer_secondabsoluteevaluationhsc)) * mdr_fc_data_integer_secondabsoluteevaluationhs) + (mdr_n_data_integer_secondabsoluteevaluationhsc)))))))) /\ (exists ff_ub_mce_fold_mdr_data_integer_secondabsoluteevaluationhsf ff_uc_mce_fold_mdr_data_integer_secondabsoluteevaluationhsf ff_vb_mce_fold_mdr_data_integer_secondabsoluteevaluationhsf ff_vc_mce_fold_mdr_data_integer_secondabsoluteevaluationhsf. ((forall ff_index_mce_alternating_mdr_data_integer_secondabsoluteevaluationhsf_prefix. (exists ff_gap_mce_mdr_data_integer_secondabsoluteevaluationhsf_prefix_index. ff_gap_mce_mdr_data_integer_secondabsoluteevaluationhsf_prefix_index + S (ff_index_mce_alternating_mdr_data_integer_secondabsoluteevaluationhsf_prefix) = (S (mdr_q_data_integer_secondabsoluteevaluationhs))) -> exists ff_ap_mce_alternating_mdr_data_integer_secondabsoluteevaluationhsf_prefix ff_an_mce_alternating_mdr_data_integer_secondabsoluteevaluationhsf_prefix ff_bp_mce_alternating_mdr_data_integer_secondabsoluteevaluationhsf_prefix ff_bn_mce_alternating_mdr_data_integer_secondabsoluteevaluationhsf_prefix ff_p_mce_alternating_mdr_data_integer_secondabsoluteevaluationhsf_prefix ff_n_mce_alternating_mdr_data_integer_secondabsoluteevaluationhsf_prefix. ((((exists ff_h_mce_mdr_data_integer_secondabsoluteevaluationhsf_prefix_ap. ff_h_mce_mdr_data_integer_secondabsoluteevaluationhsf_prefix_ap + S (ff_ap_mce_alternating_mdr_data_integer_secondabsoluteevaluationhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_data_integer_secondabsoluteevaluationhsf_prefix)) * mdr_pc_data_integer_secondabsoluteevaluationh)) /\ exists ff_q_mce_mdr_data_integer_secondabsoluteevaluationhsf_prefix_ap. mdr_pb_data_integer_secondabsoluteevaluationh = ff_q_mce_mdr_data_integer_secondabsoluteevaluationhsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_data_integer_secondabsoluteevaluationhsf_prefix)) * mdr_pc_data_integer_secondabsoluteevaluationh) + (ff_ap_mce_alternating_mdr_data_integer_secondabsoluteevaluationhsf_prefix))) /\ ((((exists ff_h_mce_mdr_data_integer_secondabsoluteevaluationhsf_prefix_an. ff_h_mce_mdr_data_integer_secondabsoluteevaluationhsf_prefix_an + S (ff_an_mce_alternating_mdr_data_integer_secondabsoluteevaluationhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_data_integer_secondabsoluteevaluationhsf_prefix)) * mdr_nc_data_integer_secondabsoluteevaluationh)) /\ exists ff_q_mce_mdr_data_integer_secondabsoluteevaluationhsf_prefix_an. mdr_nb_data_integer_secondabsoluteevaluationh = ff_q_mce_mdr_data_integer_secondabsoluteevaluationhsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_data_integer_secondabsoluteevaluationhsf_prefix)) * mdr_nc_data_integer_secondabsoluteevaluationh) + (ff_an_mce_alternating_mdr_data_integer_secondabsoluteevaluationhsf_prefix))) /\ ((((exists ff_h_mce_mdr_data_integer_secondabsoluteevaluationhsf_prefix_bp. ff_h_mce_mdr_data_integer_secondabsoluteevaluationhsf_prefix_bp + S (ff_bp_mce_alternating_mdr_data_integer_secondabsoluteevaluationhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_data_integer_secondabsoluteevaluationhsf_prefix)) * mdr_ec_data_integer_secondabsoluteevaluationhs)) /\ exists ff_q_mce_mdr_data_integer_secondabsoluteevaluationhsf_prefix_bp. mdr_eb_data_integer_secondabsoluteevaluationhs = ff_q_mce_mdr_data_integer_secondabsoluteevaluationhsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_data_integer_secondabsoluteevaluationhsf_prefix)) * mdr_ec_data_integer_secondabsoluteevaluationhs) + (ff_bp_mce_alternating_mdr_data_integer_secondabsoluteevaluationhsf_prefix))) /\ ((((exists ff_h_mce_mdr_data_integer_secondabsoluteevaluationhsf_prefix_bn. ff_h_mce_mdr_data_integer_secondabsoluteevaluationhsf_prefix_bn + S (ff_bn_mce_alternating_mdr_data_integer_secondabsoluteevaluationhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_data_integer_secondabsoluteevaluationhsf_prefix)) * mdr_fc_data_integer_secondabsoluteevaluationhs)) /\ exists ff_q_mce_mdr_data_integer_secondabsoluteevaluationhsf_prefix_bn. mdr_fb_data_integer_secondabsoluteevaluationhs = ff_q_mce_mdr_data_integer_secondabsoluteevaluationhsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_data_integer_secondabsoluteevaluationhsf_prefix)) * mdr_fc_data_integer_secondabsoluteevaluationhs) + (ff_bn_mce_alternating_mdr_data_integer_secondabsoluteevaluationhsf_prefix))) /\ ((((exists ff_h_mce_mdr_data_integer_secondabsoluteevaluationhsf_prefix_positive. ff_h_mce_mdr_data_integer_secondabsoluteevaluationhsf_prefix_positive + S (ff_p_mce_alternating_mdr_data_integer_secondabsoluteevaluationhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_data_integer_secondabsoluteevaluationhsf_prefix)) * ff_uc_mce_fold_mdr_data_integer_secondabsoluteevaluationhsf)) /\ exists ff_q_mce_mdr_data_integer_secondabsoluteevaluationhsf_prefix_positive. ff_ub_mce_fold_mdr_data_integer_secondabsoluteevaluationhsf = ff_q_mce_mdr_data_integer_secondabsoluteevaluationhsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_data_integer_secondabsoluteevaluationhsf_prefix)) * ff_uc_mce_fold_mdr_data_integer_secondabsoluteevaluationhsf) + (ff_p_mce_alternating_mdr_data_integer_secondabsoluteevaluationhsf_prefix))) /\ ((((exists ff_h_mce_mdr_data_integer_secondabsoluteevaluationhsf_prefix_negative. ff_h_mce_mdr_data_integer_secondabsoluteevaluationhsf_prefix_negative + S (ff_n_mce_alternating_mdr_data_integer_secondabsoluteevaluationhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_data_integer_secondabsoluteevaluationhsf_prefix)) * ff_vc_mce_fold_mdr_data_integer_secondabsoluteevaluationhsf)) /\ exists ff_q_mce_mdr_data_integer_secondabsoluteevaluationhsf_prefix_negative. ff_vb_mce_fold_mdr_data_integer_secondabsoluteevaluationhsf = ff_q_mce_mdr_data_integer_secondabsoluteevaluationhsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_data_integer_secondabsoluteevaluationhsf_prefix)) * ff_vc_mce_fold_mdr_data_integer_secondabsoluteevaluationhsf) + (ff_n_mce_alternating_mdr_data_integer_secondabsoluteevaluationhsf_prefix))) /\ (((exists ff_even_mce_term_mdr_data_integer_secondabsoluteevaluationhsf_prefix_term. ff_index_mce_alternating_mdr_data_integer_secondabsoluteevaluationhsf_prefix = 2 * ff_even_mce_term_mdr_data_integer_secondabsoluteevaluationhsf_prefix_term) /\ (ff_p_mce_alternating_mdr_data_integer_secondabsoluteevaluationhsf_prefix = (ff_ap_mce_alternating_mdr_data_integer_secondabsoluteevaluationhsf_prefix) * (ff_bp_mce_alternating_mdr_data_integer_secondabsoluteevaluationhsf_prefix) + (ff_an_mce_alternating_mdr_data_integer_secondabsoluteevaluationhsf_prefix) * (ff_bn_mce_alternating_mdr_data_integer_secondabsoluteevaluationhsf_prefix) /\ ff_n_mce_alternating_mdr_data_integer_secondabsoluteevaluationhsf_prefix = (ff_ap_mce_alternating_mdr_data_integer_secondabsoluteevaluationhsf_prefix) * (ff_bn_mce_alternating_mdr_data_integer_secondabsoluteevaluationhsf_prefix) + (ff_an_mce_alternating_mdr_data_integer_secondabsoluteevaluationhsf_prefix) * (ff_bp_mce_alternating_mdr_data_integer_secondabsoluteevaluationhsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_data_integer_secondabsoluteevaluationhsf_prefix_term. ff_index_mce_alternating_mdr_data_integer_secondabsoluteevaluationhsf_prefix = 2 * ff_odd_mce_term_mdr_data_integer_secondabsoluteevaluationhsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_data_integer_secondabsoluteevaluationhsf_prefix = (ff_ap_mce_alternating_mdr_data_integer_secondabsoluteevaluationhsf_prefix) * (ff_bn_mce_alternating_mdr_data_integer_secondabsoluteevaluationhsf_prefix) + (ff_an_mce_alternating_mdr_data_integer_secondabsoluteevaluationhsf_prefix) * (ff_bp_mce_alternating_mdr_data_integer_secondabsoluteevaluationhsf_prefix) /\ ff_n_mce_alternating_mdr_data_integer_secondabsoluteevaluationhsf_prefix = (ff_ap_mce_alternating_mdr_data_integer_secondabsoluteevaluationhsf_prefix) * (ff_bp_mce_alternating_mdr_data_integer_secondabsoluteevaluationhsf_prefix) + (ff_an_mce_alternating_mdr_data_integer_secondabsoluteevaluationhsf_prefix) * (ff_bn_mce_alternating_mdr_data_integer_secondabsoluteevaluationhsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_data_integer_secondabsoluteevaluationhsf_positive ff_v_mce_mdr_data_integer_secondabsoluteevaluationhsf_positive. ((((exists ff_h_mce_mdr_data_integer_secondabsoluteevaluationhsf_positive_start. ff_h_mce_mdr_data_integer_secondabsoluteevaluationhsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_data_integer_secondabsoluteevaluationhsf_positive)) /\ exists ff_q_mce_mdr_data_integer_secondabsoluteevaluationhsf_positive_start. ff_u_mce_mdr_data_integer_secondabsoluteevaluationhsf_positive = ff_q_mce_mdr_data_integer_secondabsoluteevaluationhsf_positive_start * S ((S (0)) * ff_v_mce_mdr_data_integer_secondabsoluteevaluationhsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_data_integer_secondabsoluteevaluationhsf_positive_terminal. ff_h_mce_mdr_data_integer_secondabsoluteevaluationhsf_positive_terminal + S (mdr_p_data_integer_secondabsoluteevaluationh) = S ((S ((S (mdr_q_data_integer_secondabsoluteevaluationhs)))) * ff_v_mce_mdr_data_integer_secondabsoluteevaluationhsf_positive)) /\ exists ff_q_mce_mdr_data_integer_secondabsoluteevaluationhsf_positive_terminal. ff_u_mce_mdr_data_integer_secondabsoluteevaluationhsf_positive = ff_q_mce_mdr_data_integer_secondabsoluteevaluationhsf_positive_terminal * S ((S ((S (mdr_q_data_integer_secondabsoluteevaluationhs)))) * ff_v_mce_mdr_data_integer_secondabsoluteevaluationhsf_positive) + (mdr_p_data_integer_secondabsoluteevaluationh))) /\ forall ff_i_mce_mdr_data_integer_secondabsoluteevaluationhsf_positive. (exists ff_lt_mce_mdr_data_integer_secondabsoluteevaluationhsf_positive_bound. ff_lt_mce_mdr_data_integer_secondabsoluteevaluationhsf_positive_bound + S ff_i_mce_mdr_data_integer_secondabsoluteevaluationhsf_positive = (S (mdr_q_data_integer_secondabsoluteevaluationhs))) -> exists ff_a_mce_mdr_data_integer_secondabsoluteevaluationhsf_positive ff_r_mce_mdr_data_integer_secondabsoluteevaluationhsf_positive ff_s_mce_mdr_data_integer_secondabsoluteevaluationhsf_positive. ((((exists ff_h_mce_mdr_data_integer_secondabsoluteevaluationhsf_positive_summand. ff_h_mce_mdr_data_integer_secondabsoluteevaluationhsf_positive_summand + S (ff_a_mce_mdr_data_integer_secondabsoluteevaluationhsf_positive) = S ((S (ff_i_mce_mdr_data_integer_secondabsoluteevaluationhsf_positive)) * ff_uc_mce_fold_mdr_data_integer_secondabsoluteevaluationhsf)) /\ exists ff_q_mce_mdr_data_integer_secondabsoluteevaluationhsf_positive_summand. ff_ub_mce_fold_mdr_data_integer_secondabsoluteevaluationhsf = ff_q_mce_mdr_data_integer_secondabsoluteevaluationhsf_positive_summand * S ((S (ff_i_mce_mdr_data_integer_secondabsoluteevaluationhsf_positive)) * ff_uc_mce_fold_mdr_data_integer_secondabsoluteevaluationhsf) + (ff_a_mce_mdr_data_integer_secondabsoluteevaluationhsf_positive))) /\ ((((exists ff_h_mce_mdr_data_integer_secondabsoluteevaluationhsf_positive_partial. ff_h_mce_mdr_data_integer_secondabsoluteevaluationhsf_positive_partial + S (ff_r_mce_mdr_data_integer_secondabsoluteevaluationhsf_positive) = S ((S (ff_i_mce_mdr_data_integer_secondabsoluteevaluationhsf_positive)) * ff_v_mce_mdr_data_integer_secondabsoluteevaluationhsf_positive)) /\ exists ff_q_mce_mdr_data_integer_secondabsoluteevaluationhsf_positive_partial. ff_u_mce_mdr_data_integer_secondabsoluteevaluationhsf_positive = ff_q_mce_mdr_data_integer_secondabsoluteevaluationhsf_positive_partial * S ((S (ff_i_mce_mdr_data_integer_secondabsoluteevaluationhsf_positive)) * ff_v_mce_mdr_data_integer_secondabsoluteevaluationhsf_positive) + (ff_r_mce_mdr_data_integer_secondabsoluteevaluationhsf_positive))) /\ ((((exists ff_h_mce_mdr_data_integer_secondabsoluteevaluationhsf_positive_successor. ff_h_mce_mdr_data_integer_secondabsoluteevaluationhsf_positive_successor + S (ff_s_mce_mdr_data_integer_secondabsoluteevaluationhsf_positive) = S ((S (S ff_i_mce_mdr_data_integer_secondabsoluteevaluationhsf_positive)) * ff_v_mce_mdr_data_integer_secondabsoluteevaluationhsf_positive)) /\ exists ff_q_mce_mdr_data_integer_secondabsoluteevaluationhsf_positive_successor. ff_u_mce_mdr_data_integer_secondabsoluteevaluationhsf_positive = ff_q_mce_mdr_data_integer_secondabsoluteevaluationhsf_positive_successor * S ((S (S ff_i_mce_mdr_data_integer_secondabsoluteevaluationhsf_positive)) * ff_v_mce_mdr_data_integer_secondabsoluteevaluationhsf_positive) + (ff_s_mce_mdr_data_integer_secondabsoluteevaluationhsf_positive))) /\ ff_s_mce_mdr_data_integer_secondabsoluteevaluationhsf_positive = ff_r_mce_mdr_data_integer_secondabsoluteevaluationhsf_positive + ff_a_mce_mdr_data_integer_secondabsoluteevaluationhsf_positive)))))) /\ (exists ff_u_mce_mdr_data_integer_secondabsoluteevaluationhsf_negative ff_v_mce_mdr_data_integer_secondabsoluteevaluationhsf_negative. ((((exists ff_h_mce_mdr_data_integer_secondabsoluteevaluationhsf_negative_start. ff_h_mce_mdr_data_integer_secondabsoluteevaluationhsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_data_integer_secondabsoluteevaluationhsf_negative)) /\ exists ff_q_mce_mdr_data_integer_secondabsoluteevaluationhsf_negative_start. ff_u_mce_mdr_data_integer_secondabsoluteevaluationhsf_negative = ff_q_mce_mdr_data_integer_secondabsoluteevaluationhsf_negative_start * S ((S (0)) * ff_v_mce_mdr_data_integer_secondabsoluteevaluationhsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_data_integer_secondabsoluteevaluationhsf_negative_terminal. ff_h_mce_mdr_data_integer_secondabsoluteevaluationhsf_negative_terminal + S (mdr_n_data_integer_secondabsoluteevaluationh) = S ((S ((S (mdr_q_data_integer_secondabsoluteevaluationhs)))) * ff_v_mce_mdr_data_integer_secondabsoluteevaluationhsf_negative)) /\ exists ff_q_mce_mdr_data_integer_secondabsoluteevaluationhsf_negative_terminal. ff_u_mce_mdr_data_integer_secondabsoluteevaluationhsf_negative = ff_q_mce_mdr_data_integer_secondabsoluteevaluationhsf_negative_terminal * S ((S ((S (mdr_q_data_integer_secondabsoluteevaluationhs)))) * ff_v_mce_mdr_data_integer_secondabsoluteevaluationhsf_negative) + (mdr_n_data_integer_secondabsoluteevaluationh))) /\ forall ff_i_mce_mdr_data_integer_secondabsoluteevaluationhsf_negative. (exists ff_lt_mce_mdr_data_integer_secondabsoluteevaluationhsf_negative_bound. ff_lt_mce_mdr_data_integer_secondabsoluteevaluationhsf_negative_bound + S ff_i_mce_mdr_data_integer_secondabsoluteevaluationhsf_negative = (S (mdr_q_data_integer_secondabsoluteevaluationhs))) -> exists ff_a_mce_mdr_data_integer_secondabsoluteevaluationhsf_negative ff_r_mce_mdr_data_integer_secondabsoluteevaluationhsf_negative ff_s_mce_mdr_data_integer_secondabsoluteevaluationhsf_negative. ((((exists ff_h_mce_mdr_data_integer_secondabsoluteevaluationhsf_negative_summand. ff_h_mce_mdr_data_integer_secondabsoluteevaluationhsf_negative_summand + S (ff_a_mce_mdr_data_integer_secondabsoluteevaluationhsf_negative) = S ((S (ff_i_mce_mdr_data_integer_secondabsoluteevaluationhsf_negative)) * ff_vc_mce_fold_mdr_data_integer_secondabsoluteevaluationhsf)) /\ exists ff_q_mce_mdr_data_integer_secondabsoluteevaluationhsf_negative_summand. ff_vb_mce_fold_mdr_data_integer_secondabsoluteevaluationhsf = ff_q_mce_mdr_data_integer_secondabsoluteevaluationhsf_negative_summand * S ((S (ff_i_mce_mdr_data_integer_secondabsoluteevaluationhsf_negative)) * ff_vc_mce_fold_mdr_data_integer_secondabsoluteevaluationhsf) + (ff_a_mce_mdr_data_integer_secondabsoluteevaluationhsf_negative))) /\ ((((exists ff_h_mce_mdr_data_integer_secondabsoluteevaluationhsf_negative_partial. ff_h_mce_mdr_data_integer_secondabsoluteevaluationhsf_negative_partial + S (ff_r_mce_mdr_data_integer_secondabsoluteevaluationhsf_negative) = S ((S (ff_i_mce_mdr_data_integer_secondabsoluteevaluationhsf_negative)) * ff_v_mce_mdr_data_integer_secondabsoluteevaluationhsf_negative)) /\ exists ff_q_mce_mdr_data_integer_secondabsoluteevaluationhsf_negative_partial. ff_u_mce_mdr_data_integer_secondabsoluteevaluationhsf_negative = ff_q_mce_mdr_data_integer_secondabsoluteevaluationhsf_negative_partial * S ((S (ff_i_mce_mdr_data_integer_secondabsoluteevaluationhsf_negative)) * ff_v_mce_mdr_data_integer_secondabsoluteevaluationhsf_negative) + (ff_r_mce_mdr_data_integer_secondabsoluteevaluationhsf_negative))) /\ ((((exists ff_h_mce_mdr_data_integer_secondabsoluteevaluationhsf_negative_successor. ff_h_mce_mdr_data_integer_secondabsoluteevaluationhsf_negative_successor + S (ff_s_mce_mdr_data_integer_secondabsoluteevaluationhsf_negative) = S ((S (S ff_i_mce_mdr_data_integer_secondabsoluteevaluationhsf_negative)) * ff_v_mce_mdr_data_integer_secondabsoluteevaluationhsf_negative)) /\ exists ff_q_mce_mdr_data_integer_secondabsoluteevaluationhsf_negative_successor. ff_u_mce_mdr_data_integer_secondabsoluteevaluationhsf_negative = ff_q_mce_mdr_data_integer_secondabsoluteevaluationhsf_negative_successor * S ((S (S ff_i_mce_mdr_data_integer_secondabsoluteevaluationhsf_negative)) * ff_v_mce_mdr_data_integer_secondabsoluteevaluationhsf_negative) + (ff_s_mce_mdr_data_integer_secondabsoluteevaluationhsf_negative))) /\ ff_s_mce_mdr_data_integer_secondabsoluteevaluationhsf_negative = ff_r_mce_mdr_data_integer_secondabsoluteevaluationhsf_negative + ff_a_mce_mdr_data_integer_secondabsoluteevaluationhsf_negative))))))))))))))) /\ ((exists mdr_gap_data_integer_secondabsoluteevaluationi. mdr_gap_data_integer_secondabsoluteevaluationi + S (mdr_i_data_integer_secondabsoluteevaluation) = (mdr_l_data_integer_secondabsoluteevaluation)) /\ (exists mdr_z_data_integer_secondabsoluteevaluationr. ((exists mdr_a_data_integer_secondabsoluteevaluationrc mdr_b_data_integer_secondabsoluteevaluationrc mdr_c_data_integer_secondabsoluteevaluationrc mdr_e_data_integer_secondabsoluteevaluationrc mdr_f_data_integer_secondabsoluteevaluationrc. ((mdr_a_data_integer_secondabsoluteevaluationrc = ((d) + (eb)) * S ((d) + (eb)) + ((eb) + (eb))) /\ ((mdr_b_data_integer_secondabsoluteevaluationrc = ((ec) + (fb)) * S ((ec) + (fb)) + ((fb) + (fb))) /\ ((mdr_c_data_integer_secondabsoluteevaluationrc = ((mdr_a_data_integer_secondabsoluteevaluationrc) + (mdr_b_data_integer_secondabsoluteevaluationrc)) * S ((mdr_a_data_integer_secondabsoluteevaluationrc) + (mdr_b_data_integer_secondabsoluteevaluationrc)) + ((mdr_b_data_integer_secondabsoluteevaluationrc) + (mdr_b_data_integer_secondabsoluteevaluationrc))) /\ ((mdr_e_data_integer_secondabsoluteevaluationrc = ((mdr_p_data_integer_secondabsolute) + (mdr_n_data_integer_secondabsolute)) * S ((mdr_p_data_integer_secondabsolute) + (mdr_n_data_integer_secondabsolute)) + ((mdr_n_data_integer_secondabsolute) + (mdr_n_data_integer_secondabsolute))) /\ ((mdr_f_data_integer_secondabsoluteevaluationrc = ((fc) + (mdr_e_data_integer_secondabsoluteevaluationrc)) * S ((fc) + (mdr_e_data_integer_secondabsoluteevaluationrc)) + ((mdr_e_data_integer_secondabsoluteevaluationrc) + (mdr_e_data_integer_secondabsoluteevaluationrc))) /\ ((mdr_z_data_integer_secondabsoluteevaluationr) = ((mdr_c_data_integer_secondabsoluteevaluationrc) + (mdr_f_data_integer_secondabsoluteevaluationrc)) * S ((mdr_c_data_integer_secondabsoluteevaluationrc) + (mdr_f_data_integer_secondabsoluteevaluationrc)) + ((mdr_f_data_integer_secondabsoluteevaluationrc) + (mdr_f_data_integer_secondabsoluteevaluationrc))))))))) /\ (((exists ff_h_mdr_data_integer_secondabsoluteevaluationrb. ff_h_mdr_data_integer_secondabsoluteevaluationrb + S (mdr_z_data_integer_secondabsoluteevaluationr) = S ((S (mdr_i_data_integer_secondabsoluteevaluation)) * mdr_c_data_integer_secondabsoluteevaluation)) /\ exists ff_q_mdr_data_integer_secondabsoluteevaluationrb. mdr_b_data_integer_secondabsoluteevaluation = ff_q_mdr_data_integer_secondabsoluteevaluationrb * S ((S (mdr_i_data_integer_secondabsoluteevaluation)) * mdr_c_data_integer_secondabsoluteevaluation) + (mdr_z_data_integer_secondabsoluteevaluationr)))))))) /\ (((mdr_p_data_integer_secondabsolute) = (mdr_n_data_integer_secondabsolute) + (D)) \/ ((mdr_n_data_integer_secondabsolute) = (mdr_p_data_integer_secondabsolute) + (D))))))))Constructive proof overview
Generated structural guide
Positive-dimensional absolute-determinant data respects the integer matrix itself, not arbitrary signed beta representatives.
The unchanged tactic script uses 1 declared prerequisite and contains 31 exact native proof lines.
Alpha v34 checked-use · first admitted v27 · independently kernel and Lean verified; not Stable
Proof neighborhood
Direct dependencies
Direct dependents
none
Formal native tactic body
Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.
Read the argument
Proof checkpoints
This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.
Named ingredients (1)
01Fix variables and assumptionsL1–10
02Fix variables and assumptionsL11–12
03Separate the logical casesL13–15
04Use earlier factsL16–16
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L16
exact hdata_left
05Separate the logical casesL17–17
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L17
split
06Use earlier factsL18–27
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L18
exact hdata_right_left - L19
specialize absolute_recursive_determinant_integer_transport (ab) - L20
specialize absolute_recursive_determinant_integer_transport (ac) - L21
specialize absolute_recursive_determinant_integer_transport (bb) - L22
specialize absolute_recursive_determinant_integer_transport (bc) - L23
specialize absolute_recursive_determinant_integer_transport (eb) - L24
specialize absolute_recursive_determinant_integer_transport (ec) - L25
specialize absolute_recursive_determinant_integer_transport (fb) - L26
specialize absolute_recursive_determinant_integer_transport (fc) - L27
specialize absolute_recursive_determinant_integer_transport (d)
Original exact command ledger · 31 lines
- 0001
intro ab - 0002
intro ac - 0003
intro bb - 0004
intro bc - 0005
intro eb - 0006
intro ec - 0007
intro fb - 0008
intro fc - 0009
intro d - 0010
intro D - 0011
intro hequal - 0012
intro hdata - 0013
cases hdata - 0014
cases hdata_right - 0015
split - 0016
exact hdata_left - 0017
split - 0018
exact hdata_right_left - 0019
specialize absolute_recursive_determinant_integer_transport (ab) - 0020
specialize absolute_recursive_determinant_integer_transport (ac) - 0021
specialize absolute_recursive_determinant_integer_transport (bb) - 0022
specialize absolute_recursive_determinant_integer_transport (bc) - 0023
specialize absolute_recursive_determinant_integer_transport (eb) - 0024
specialize absolute_recursive_determinant_integer_transport (ec) - 0025
specialize absolute_recursive_determinant_integer_transport (fb) - 0026
specialize absolute_recursive_determinant_integer_transport (fc) - 0027
specialize absolute_recursive_determinant_integer_transport (d) - 0028
specialize absolute_recursive_determinant_integer_transport (D) - 0029
apply absolute_recursive_determinant_integer_transport - 0030
exact hequal - 0031
exact hdata_right_right