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.
This branch proves the finite determinant/rank/span substrate. It does not claim Smith or Hermite normal form, lattice index equals determinant, determinant multiplicativity, lattice reduction, or geometry-of-numbers theorems.
Exact theorem in conservative defined notation
∀ q. (∀ x. ∀ y. ∀ z. ∀ n. ∀ m. ∀ k. ∀ i. SignedDeterminantHistory(m,k,i) → ∃ j. ∃ u. ∃ v. ∃ w. ∃ x0. (∀ x1. ∀ x2. Lt(x1,i) → BetaAt(m,k,x1,x2) → BetaAt(j,u,x1,x2)) ∧ (Le(i,v) ∧ (SignedDeterminantHistory(j,u,S v) ∧ SignedDeterminantNodeAt(j,u,v,q,x,y,z,n,w,x0)))) → ∀ x. ∀ y. ∀ z. ∀ n. ∀ m. ∀ k. ∀ i. SignedDeterminantHistory(m,k,i) → ∃ j. ∃ u. ∃ v. ∃ w. ∃ x0. (∀ x1. ∀ x2. Lt(x1,i) → BetaAt(m,k,x1,x2) → BetaAt(j,u,x1,x2)) ∧ (Le(i,v) ∧ (SignedDeterminantHistory(j,u,S v) ∧ SignedDeterminantNodeAt(j,u,v,S q,x,y,z,n,w,x0)))Every linked abbreviation expands hygienically to the identical original native formula.
Definition DAG
Actual proof prerequisites
le_refl · checked external prerequisitesigned_alternating_cofactor_fold_exists · checked external prerequisitematrix_recursive_cofactor_prefix_from_recursionmatrix_recursive_history_extendmatrix_recursive_prefix_transmatrix_recursive_prefix_restrict
Original expanded first-order statement
forall q. (forall mdr_pb_rec_source mdr_pc_rec_source mdr_nb_rec_source mdr_nc_rec_source mdr_b_rec_source mdr_c_rec_source mdr_l_rec_source. (forall mdr_i_rec_sourceh. (exists mdr_gap_rec_sourcehi. mdr_gap_rec_sourcehi + S (mdr_i_rec_sourceh) = (mdr_l_rec_source)) -> exists mdr_d_rec_sourceh mdr_pb_rec_sourceh mdr_pc_rec_sourceh mdr_nb_rec_sourceh mdr_nc_rec_sourceh mdr_p_rec_sourceh mdr_n_rec_sourceh. ((exists mdr_z_rec_sourcehr. ((exists mdr_a_rec_sourcehrc mdr_b_rec_sourcehrc mdr_c_rec_sourcehrc mdr_e_rec_sourcehrc mdr_f_rec_sourcehrc. ((mdr_a_rec_sourcehrc = ((mdr_d_rec_sourceh) + (mdr_pb_rec_sourceh)) * S ((mdr_d_rec_sourceh) + (mdr_pb_rec_sourceh)) + ((mdr_pb_rec_sourceh) + (mdr_pb_rec_sourceh))) /\ ((mdr_b_rec_sourcehrc = ((mdr_pc_rec_sourceh) + (mdr_nb_rec_sourceh)) * S ((mdr_pc_rec_sourceh) + (mdr_nb_rec_sourceh)) + ((mdr_nb_rec_sourceh) + (mdr_nb_rec_sourceh))) /\ ((mdr_c_rec_sourcehrc = ((mdr_a_rec_sourcehrc) + (mdr_b_rec_sourcehrc)) * S ((mdr_a_rec_sourcehrc) + (mdr_b_rec_sourcehrc)) + ((mdr_b_rec_sourcehrc) + (mdr_b_rec_sourcehrc))) /\ ((mdr_e_rec_sourcehrc = ((mdr_p_rec_sourceh) + (mdr_n_rec_sourceh)) * S ((mdr_p_rec_sourceh) + (mdr_n_rec_sourceh)) + ((mdr_n_rec_sourceh) + (mdr_n_rec_sourceh))) /\ ((mdr_f_rec_sourcehrc = ((mdr_nc_rec_sourceh) + (mdr_e_rec_sourcehrc)) * S ((mdr_nc_rec_sourceh) + (mdr_e_rec_sourcehrc)) + ((mdr_e_rec_sourcehrc) + (mdr_e_rec_sourcehrc))) /\ ((mdr_z_rec_sourcehr) = ((mdr_c_rec_sourcehrc) + (mdr_f_rec_sourcehrc)) * S ((mdr_c_rec_sourcehrc) + (mdr_f_rec_sourcehrc)) + ((mdr_f_rec_sourcehrc) + (mdr_f_rec_sourcehrc))))))))) /\ (((exists ff_h_mdr_rec_sourcehrb. ff_h_mdr_rec_sourcehrb + S (mdr_z_rec_sourcehr) = S ((S (mdr_i_rec_sourceh)) * mdr_c_rec_source)) /\ exists ff_q_mdr_rec_sourcehrb. mdr_b_rec_source = ff_q_mdr_rec_sourcehrb * S ((S (mdr_i_rec_sourceh)) * mdr_c_rec_source) + (mdr_z_rec_sourcehr))))) /\ (((((mdr_d_rec_sourceh) = 0) /\ (((mdr_p_rec_sourceh) = 1) /\ ((mdr_n_rec_sourceh) = 0))) \/ exists mdr_q_rec_sourcehs mdr_eb_rec_sourcehs mdr_ec_rec_sourcehs mdr_fb_rec_sourcehs mdr_fc_rec_sourcehs. (((mdr_d_rec_sourceh) = S (mdr_q_rec_sourcehs)) /\ ((forall mdr_j_rec_sourcehsc. (exists mdr_gap_rec_sourcehscj. mdr_gap_rec_sourcehscj + S (mdr_j_rec_sourcehsc) = (S (mdr_q_rec_sourcehs))) -> exists mdr_i_rec_sourcehsc mdr_up_rec_sourcehsc mdr_us_rec_sourcehsc mdr_un_rec_sourcehsc mdr_ut_rec_sourcehsc mdr_p_rec_sourcehsc mdr_n_rec_sourcehsc. ((exists mdr_gap_rec_sourcehsci. mdr_gap_rec_sourcehsci + S (mdr_i_rec_sourcehsc) = (mdr_i_rec_sourceh)) /\ ((exists mdr_z_rec_sourcehscr. ((exists mdr_a_rec_sourcehscrc mdr_b_rec_sourcehscrc mdr_c_rec_sourcehscrc mdr_e_rec_sourcehscrc mdr_f_rec_sourcehscrc. ((mdr_a_rec_sourcehscrc = ((mdr_q_rec_sourcehs) + (mdr_up_rec_sourcehsc)) * S ((mdr_q_rec_sourcehs) + (mdr_up_rec_sourcehsc)) + ((mdr_up_rec_sourcehsc) + (mdr_up_rec_sourcehsc))) /\ ((mdr_b_rec_sourcehscrc = ((mdr_us_rec_sourcehsc) + (mdr_un_rec_sourcehsc)) * S ((mdr_us_rec_sourcehsc) + (mdr_un_rec_sourcehsc)) + ((mdr_un_rec_sourcehsc) + (mdr_un_rec_sourcehsc))) /\ ((mdr_c_rec_sourcehscrc = ((mdr_a_rec_sourcehscrc) + (mdr_b_rec_sourcehscrc)) * S ((mdr_a_rec_sourcehscrc) + (mdr_b_rec_sourcehscrc)) + ((mdr_b_rec_sourcehscrc) + (mdr_b_rec_sourcehscrc))) /\ ((mdr_e_rec_sourcehscrc = ((mdr_p_rec_sourcehsc) + (mdr_n_rec_sourcehsc)) * S ((mdr_p_rec_sourcehsc) + (mdr_n_rec_sourcehsc)) + ((mdr_n_rec_sourcehsc) + (mdr_n_rec_sourcehsc))) /\ ((mdr_f_rec_sourcehscrc = ((mdr_ut_rec_sourcehsc) + (mdr_e_rec_sourcehscrc)) * S ((mdr_ut_rec_sourcehsc) + (mdr_e_rec_sourcehscrc)) + ((mdr_e_rec_sourcehscrc) + (mdr_e_rec_sourcehscrc))) /\ ((mdr_z_rec_sourcehscr) = ((mdr_c_rec_sourcehscrc) + (mdr_f_rec_sourcehscrc)) * S ((mdr_c_rec_sourcehscrc) + (mdr_f_rec_sourcehscrc)) + ((mdr_f_rec_sourcehscrc) + (mdr_f_rec_sourcehscrc))))))))) /\ (((exists ff_h_mdr_rec_sourcehscrb. ff_h_mdr_rec_sourcehscrb + S (mdr_z_rec_sourcehscr) = S ((S (mdr_i_rec_sourcehsc)) * mdr_c_rec_source)) /\ exists ff_q_mdr_rec_sourcehscrb. mdr_b_rec_source = ff_q_mdr_rec_sourcehscrb * S ((S (mdr_i_rec_sourcehsc)) * mdr_c_rec_source) + (mdr_z_rec_sourcehscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_rec_sourcehscm_positive. (exists ff_gap_mdm_lt_mdr_rec_sourcehscm_positive_index_bound. ff_gap_mdm_lt_mdr_rec_sourcehscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_rec_sourcehscm_positive) = ((mdr_q_rec_sourcehs) * (mdr_q_rec_sourcehs))) -> exists ff_row_mdm_prefix_mdr_rec_sourcehscm_positive ff_column_mdm_prefix_mdr_rec_sourcehscm_positive ff_value_mdm_prefix_mdr_rec_sourcehscm_positive. (ff_index_mdm_prefix_mdr_rec_sourcehscm_positive = (mdr_q_rec_sourcehs) * ff_row_mdm_prefix_mdr_rec_sourcehscm_positive + ff_column_mdm_prefix_mdr_rec_sourcehscm_positive /\ ((exists ff_gap_mdm_lt_mdr_rec_sourcehscm_positive_column_bound. ff_gap_mdm_lt_mdr_rec_sourcehscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_rec_sourcehscm_positive) = (mdr_q_rec_sourcehs)) /\ ((exists ff_row_mdm_cell_mdr_rec_sourcehscm_positive_cell ff_column_mdm_cell_mdr_rec_sourcehscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_rec_sourcehscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_rec_sourcehscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_rec_sourcehscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_rec_sourcehscm_positive_cell = ff_row_mdm_prefix_mdr_rec_sourcehscm_positive) \/ ((exists ff_gap_mdm_le_mdr_rec_sourcehscm_positive_cell_row_after. ff_gap_mdm_le_mdr_rec_sourcehscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_rec_sourcehscm_positive)) /\ ff_row_mdm_cell_mdr_rec_sourcehscm_positive_cell = S ff_row_mdm_prefix_mdr_rec_sourcehscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_rec_sourcehscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_rec_sourcehscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_rec_sourcehscm_positive) = (mdr_j_rec_sourcehsc)) /\ ff_column_mdm_cell_mdr_rec_sourcehscm_positive_cell = ff_column_mdm_prefix_mdr_rec_sourcehscm_positive) \/ ((exists ff_gap_mdm_le_mdr_rec_sourcehscm_positive_cell_column_after. ff_gap_mdm_le_mdr_rec_sourcehscm_positive_cell_column_after + (mdr_j_rec_sourcehsc) = (ff_column_mdm_prefix_mdr_rec_sourcehscm_positive)) /\ ff_column_mdm_cell_mdr_rec_sourcehscm_positive_cell = S ff_column_mdm_prefix_mdr_rec_sourcehscm_positive))) /\ (((exists ff_h_mdm_mdr_rec_sourcehscm_positive_cell_source. ff_h_mdm_mdr_rec_sourcehscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_rec_sourcehscm_positive) = S ((S ((ff_row_mdm_cell_mdr_rec_sourcehscm_positive_cell) * (S (mdr_q_rec_sourcehs)) + (ff_column_mdm_cell_mdr_rec_sourcehscm_positive_cell))) * mdr_pc_rec_sourceh)) /\ exists ff_q_mdm_mdr_rec_sourcehscm_positive_cell_source. mdr_pb_rec_sourceh = ff_q_mdm_mdr_rec_sourcehscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_rec_sourcehscm_positive_cell) * (S (mdr_q_rec_sourcehs)) + (ff_column_mdm_cell_mdr_rec_sourcehscm_positive_cell))) * mdr_pc_rec_sourceh) + (ff_value_mdm_prefix_mdr_rec_sourcehscm_positive)))))) /\ (((exists ff_h_mdm_mdr_rec_sourcehscm_positive_target. ff_h_mdm_mdr_rec_sourcehscm_positive_target + S (ff_value_mdm_prefix_mdr_rec_sourcehscm_positive) = S ((S (ff_index_mdm_prefix_mdr_rec_sourcehscm_positive)) * mdr_us_rec_sourcehsc)) /\ exists ff_q_mdm_mdr_rec_sourcehscm_positive_target. mdr_up_rec_sourcehsc = ff_q_mdm_mdr_rec_sourcehscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_rec_sourcehscm_positive)) * mdr_us_rec_sourcehsc) + (ff_value_mdm_prefix_mdr_rec_sourcehscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_rec_sourcehscm_negative. (exists ff_gap_mdm_lt_mdr_rec_sourcehscm_negative_index_bound. ff_gap_mdm_lt_mdr_rec_sourcehscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_rec_sourcehscm_negative) = ((mdr_q_rec_sourcehs) * (mdr_q_rec_sourcehs))) -> exists ff_row_mdm_prefix_mdr_rec_sourcehscm_negative ff_column_mdm_prefix_mdr_rec_sourcehscm_negative ff_value_mdm_prefix_mdr_rec_sourcehscm_negative. (ff_index_mdm_prefix_mdr_rec_sourcehscm_negative = (mdr_q_rec_sourcehs) * ff_row_mdm_prefix_mdr_rec_sourcehscm_negative + ff_column_mdm_prefix_mdr_rec_sourcehscm_negative /\ ((exists ff_gap_mdm_lt_mdr_rec_sourcehscm_negative_column_bound. ff_gap_mdm_lt_mdr_rec_sourcehscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_rec_sourcehscm_negative) = (mdr_q_rec_sourcehs)) /\ ((exists ff_row_mdm_cell_mdr_rec_sourcehscm_negative_cell ff_column_mdm_cell_mdr_rec_sourcehscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_rec_sourcehscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_rec_sourcehscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_rec_sourcehscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_rec_sourcehscm_negative_cell = ff_row_mdm_prefix_mdr_rec_sourcehscm_negative) \/ ((exists ff_gap_mdm_le_mdr_rec_sourcehscm_negative_cell_row_after. ff_gap_mdm_le_mdr_rec_sourcehscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_rec_sourcehscm_negative)) /\ ff_row_mdm_cell_mdr_rec_sourcehscm_negative_cell = S ff_row_mdm_prefix_mdr_rec_sourcehscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_rec_sourcehscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_rec_sourcehscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_rec_sourcehscm_negative) = (mdr_j_rec_sourcehsc)) /\ ff_column_mdm_cell_mdr_rec_sourcehscm_negative_cell = ff_column_mdm_prefix_mdr_rec_sourcehscm_negative) \/ ((exists ff_gap_mdm_le_mdr_rec_sourcehscm_negative_cell_column_after. ff_gap_mdm_le_mdr_rec_sourcehscm_negative_cell_column_after + (mdr_j_rec_sourcehsc) = (ff_column_mdm_prefix_mdr_rec_sourcehscm_negative)) /\ ff_column_mdm_cell_mdr_rec_sourcehscm_negative_cell = S ff_column_mdm_prefix_mdr_rec_sourcehscm_negative))) /\ (((exists ff_h_mdm_mdr_rec_sourcehscm_negative_cell_source. ff_h_mdm_mdr_rec_sourcehscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_rec_sourcehscm_negative) = S ((S ((ff_row_mdm_cell_mdr_rec_sourcehscm_negative_cell) * (S (mdr_q_rec_sourcehs)) + (ff_column_mdm_cell_mdr_rec_sourcehscm_negative_cell))) * mdr_nc_rec_sourceh)) /\ exists ff_q_mdm_mdr_rec_sourcehscm_negative_cell_source. mdr_nb_rec_sourceh = ff_q_mdm_mdr_rec_sourcehscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_rec_sourcehscm_negative_cell) * (S (mdr_q_rec_sourcehs)) + (ff_column_mdm_cell_mdr_rec_sourcehscm_negative_cell))) * mdr_nc_rec_sourceh) + (ff_value_mdm_prefix_mdr_rec_sourcehscm_negative)))))) /\ (((exists ff_h_mdm_mdr_rec_sourcehscm_negative_target. ff_h_mdm_mdr_rec_sourcehscm_negative_target + S (ff_value_mdm_prefix_mdr_rec_sourcehscm_negative) = S ((S (ff_index_mdm_prefix_mdr_rec_sourcehscm_negative)) * mdr_ut_rec_sourcehsc)) /\ exists ff_q_mdm_mdr_rec_sourcehscm_negative_target. mdr_un_rec_sourcehsc = ff_q_mdm_mdr_rec_sourcehscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_rec_sourcehscm_negative)) * mdr_ut_rec_sourcehsc) + (ff_value_mdm_prefix_mdr_rec_sourcehscm_negative))))))))) /\ ((((exists ff_h_mdr_rec_sourcehscp. ff_h_mdr_rec_sourcehscp + S (mdr_p_rec_sourcehsc) = S ((S (mdr_j_rec_sourcehsc)) * mdr_ec_rec_sourcehs)) /\ exists ff_q_mdr_rec_sourcehscp. mdr_eb_rec_sourcehs = ff_q_mdr_rec_sourcehscp * S ((S (mdr_j_rec_sourcehsc)) * mdr_ec_rec_sourcehs) + (mdr_p_rec_sourcehsc))) /\ (((exists ff_h_mdr_rec_sourcehscn. ff_h_mdr_rec_sourcehscn + S (mdr_n_rec_sourcehsc) = S ((S (mdr_j_rec_sourcehsc)) * mdr_fc_rec_sourcehs)) /\ exists ff_q_mdr_rec_sourcehscn. mdr_fb_rec_sourcehs = ff_q_mdr_rec_sourcehscn * S ((S (mdr_j_rec_sourcehsc)) * mdr_fc_rec_sourcehs) + (mdr_n_rec_sourcehsc)))))))) /\ (exists ff_ub_mce_fold_mdr_rec_sourcehsf ff_uc_mce_fold_mdr_rec_sourcehsf ff_vb_mce_fold_mdr_rec_sourcehsf ff_vc_mce_fold_mdr_rec_sourcehsf. ((forall ff_index_mce_alternating_mdr_rec_sourcehsf_prefix. (exists ff_gap_mce_mdr_rec_sourcehsf_prefix_index. ff_gap_mce_mdr_rec_sourcehsf_prefix_index + S (ff_index_mce_alternating_mdr_rec_sourcehsf_prefix) = (S (mdr_q_rec_sourcehs))) -> exists ff_ap_mce_alternating_mdr_rec_sourcehsf_prefix ff_an_mce_alternating_mdr_rec_sourcehsf_prefix ff_bp_mce_alternating_mdr_rec_sourcehsf_prefix ff_bn_mce_alternating_mdr_rec_sourcehsf_prefix ff_p_mce_alternating_mdr_rec_sourcehsf_prefix ff_n_mce_alternating_mdr_rec_sourcehsf_prefix. ((((exists ff_h_mce_mdr_rec_sourcehsf_prefix_ap. ff_h_mce_mdr_rec_sourcehsf_prefix_ap + S (ff_ap_mce_alternating_mdr_rec_sourcehsf_prefix) = S ((S (ff_index_mce_alternating_mdr_rec_sourcehsf_prefix)) * mdr_pc_rec_sourceh)) /\ exists ff_q_mce_mdr_rec_sourcehsf_prefix_ap. mdr_pb_rec_sourceh = ff_q_mce_mdr_rec_sourcehsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_rec_sourcehsf_prefix)) * mdr_pc_rec_sourceh) + (ff_ap_mce_alternating_mdr_rec_sourcehsf_prefix))) /\ ((((exists ff_h_mce_mdr_rec_sourcehsf_prefix_an. ff_h_mce_mdr_rec_sourcehsf_prefix_an + S (ff_an_mce_alternating_mdr_rec_sourcehsf_prefix) = S ((S (ff_index_mce_alternating_mdr_rec_sourcehsf_prefix)) * mdr_nc_rec_sourceh)) /\ exists ff_q_mce_mdr_rec_sourcehsf_prefix_an. mdr_nb_rec_sourceh = ff_q_mce_mdr_rec_sourcehsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_rec_sourcehsf_prefix)) * mdr_nc_rec_sourceh) + (ff_an_mce_alternating_mdr_rec_sourcehsf_prefix))) /\ ((((exists ff_h_mce_mdr_rec_sourcehsf_prefix_bp. ff_h_mce_mdr_rec_sourcehsf_prefix_bp + S (ff_bp_mce_alternating_mdr_rec_sourcehsf_prefix) = S ((S (ff_index_mce_alternating_mdr_rec_sourcehsf_prefix)) * mdr_ec_rec_sourcehs)) /\ exists ff_q_mce_mdr_rec_sourcehsf_prefix_bp. mdr_eb_rec_sourcehs = ff_q_mce_mdr_rec_sourcehsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_rec_sourcehsf_prefix)) * mdr_ec_rec_sourcehs) + (ff_bp_mce_alternating_mdr_rec_sourcehsf_prefix))) /\ ((((exists ff_h_mce_mdr_rec_sourcehsf_prefix_bn. ff_h_mce_mdr_rec_sourcehsf_prefix_bn + S (ff_bn_mce_alternating_mdr_rec_sourcehsf_prefix) = S ((S (ff_index_mce_alternating_mdr_rec_sourcehsf_prefix)) * mdr_fc_rec_sourcehs)) /\ exists ff_q_mce_mdr_rec_sourcehsf_prefix_bn. mdr_fb_rec_sourcehs = ff_q_mce_mdr_rec_sourcehsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_rec_sourcehsf_prefix)) * mdr_fc_rec_sourcehs) + (ff_bn_mce_alternating_mdr_rec_sourcehsf_prefix))) /\ ((((exists ff_h_mce_mdr_rec_sourcehsf_prefix_positive. ff_h_mce_mdr_rec_sourcehsf_prefix_positive + S (ff_p_mce_alternating_mdr_rec_sourcehsf_prefix) = S ((S (ff_index_mce_alternating_mdr_rec_sourcehsf_prefix)) * ff_uc_mce_fold_mdr_rec_sourcehsf)) /\ exists ff_q_mce_mdr_rec_sourcehsf_prefix_positive. ff_ub_mce_fold_mdr_rec_sourcehsf = ff_q_mce_mdr_rec_sourcehsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_rec_sourcehsf_prefix)) * ff_uc_mce_fold_mdr_rec_sourcehsf) + (ff_p_mce_alternating_mdr_rec_sourcehsf_prefix))) /\ ((((exists ff_h_mce_mdr_rec_sourcehsf_prefix_negative. ff_h_mce_mdr_rec_sourcehsf_prefix_negative + S (ff_n_mce_alternating_mdr_rec_sourcehsf_prefix) = S ((S (ff_index_mce_alternating_mdr_rec_sourcehsf_prefix)) * ff_vc_mce_fold_mdr_rec_sourcehsf)) /\ exists ff_q_mce_mdr_rec_sourcehsf_prefix_negative. ff_vb_mce_fold_mdr_rec_sourcehsf = ff_q_mce_mdr_rec_sourcehsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_rec_sourcehsf_prefix)) * ff_vc_mce_fold_mdr_rec_sourcehsf) + (ff_n_mce_alternating_mdr_rec_sourcehsf_prefix))) /\ (((exists ff_even_mce_term_mdr_rec_sourcehsf_prefix_term. ff_index_mce_alternating_mdr_rec_sourcehsf_prefix = 2 * ff_even_mce_term_mdr_rec_sourcehsf_prefix_term) /\ (ff_p_mce_alternating_mdr_rec_sourcehsf_prefix = (ff_ap_mce_alternating_mdr_rec_sourcehsf_prefix) * (ff_bp_mce_alternating_mdr_rec_sourcehsf_prefix) + (ff_an_mce_alternating_mdr_rec_sourcehsf_prefix) * (ff_bn_mce_alternating_mdr_rec_sourcehsf_prefix) /\ ff_n_mce_alternating_mdr_rec_sourcehsf_prefix = (ff_ap_mce_alternating_mdr_rec_sourcehsf_prefix) * (ff_bn_mce_alternating_mdr_rec_sourcehsf_prefix) + (ff_an_mce_alternating_mdr_rec_sourcehsf_prefix) * (ff_bp_mce_alternating_mdr_rec_sourcehsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_rec_sourcehsf_prefix_term. ff_index_mce_alternating_mdr_rec_sourcehsf_prefix = 2 * ff_odd_mce_term_mdr_rec_sourcehsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_rec_sourcehsf_prefix = (ff_ap_mce_alternating_mdr_rec_sourcehsf_prefix) * (ff_bn_mce_alternating_mdr_rec_sourcehsf_prefix) + (ff_an_mce_alternating_mdr_rec_sourcehsf_prefix) * (ff_bp_mce_alternating_mdr_rec_sourcehsf_prefix) /\ ff_n_mce_alternating_mdr_rec_sourcehsf_prefix = (ff_ap_mce_alternating_mdr_rec_sourcehsf_prefix) * (ff_bp_mce_alternating_mdr_rec_sourcehsf_prefix) + (ff_an_mce_alternating_mdr_rec_sourcehsf_prefix) * (ff_bn_mce_alternating_mdr_rec_sourcehsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_rec_sourcehsf_positive ff_v_mce_mdr_rec_sourcehsf_positive. ((((exists ff_h_mce_mdr_rec_sourcehsf_positive_start. ff_h_mce_mdr_rec_sourcehsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_rec_sourcehsf_positive)) /\ exists ff_q_mce_mdr_rec_sourcehsf_positive_start. ff_u_mce_mdr_rec_sourcehsf_positive = ff_q_mce_mdr_rec_sourcehsf_positive_start * S ((S (0)) * ff_v_mce_mdr_rec_sourcehsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_rec_sourcehsf_positive_terminal. ff_h_mce_mdr_rec_sourcehsf_positive_terminal + S (mdr_p_rec_sourceh) = S ((S ((S (mdr_q_rec_sourcehs)))) * ff_v_mce_mdr_rec_sourcehsf_positive)) /\ exists ff_q_mce_mdr_rec_sourcehsf_positive_terminal. ff_u_mce_mdr_rec_sourcehsf_positive = ff_q_mce_mdr_rec_sourcehsf_positive_terminal * S ((S ((S (mdr_q_rec_sourcehs)))) * ff_v_mce_mdr_rec_sourcehsf_positive) + (mdr_p_rec_sourceh))) /\ forall ff_i_mce_mdr_rec_sourcehsf_positive. (exists ff_lt_mce_mdr_rec_sourcehsf_positive_bound. ff_lt_mce_mdr_rec_sourcehsf_positive_bound + S ff_i_mce_mdr_rec_sourcehsf_positive = (S (mdr_q_rec_sourcehs))) -> exists ff_a_mce_mdr_rec_sourcehsf_positive ff_r_mce_mdr_rec_sourcehsf_positive ff_s_mce_mdr_rec_sourcehsf_positive. ((((exists ff_h_mce_mdr_rec_sourcehsf_positive_summand. ff_h_mce_mdr_rec_sourcehsf_positive_summand + S (ff_a_mce_mdr_rec_sourcehsf_positive) = S ((S (ff_i_mce_mdr_rec_sourcehsf_positive)) * ff_uc_mce_fold_mdr_rec_sourcehsf)) /\ exists ff_q_mce_mdr_rec_sourcehsf_positive_summand. ff_ub_mce_fold_mdr_rec_sourcehsf = ff_q_mce_mdr_rec_sourcehsf_positive_summand * S ((S (ff_i_mce_mdr_rec_sourcehsf_positive)) * ff_uc_mce_fold_mdr_rec_sourcehsf) + (ff_a_mce_mdr_rec_sourcehsf_positive))) /\ ((((exists ff_h_mce_mdr_rec_sourcehsf_positive_partial. ff_h_mce_mdr_rec_sourcehsf_positive_partial + S (ff_r_mce_mdr_rec_sourcehsf_positive) = S ((S (ff_i_mce_mdr_rec_sourcehsf_positive)) * ff_v_mce_mdr_rec_sourcehsf_positive)) /\ exists ff_q_mce_mdr_rec_sourcehsf_positive_partial. ff_u_mce_mdr_rec_sourcehsf_positive = ff_q_mce_mdr_rec_sourcehsf_positive_partial * S ((S (ff_i_mce_mdr_rec_sourcehsf_positive)) * ff_v_mce_mdr_rec_sourcehsf_positive) + (ff_r_mce_mdr_rec_sourcehsf_positive))) /\ ((((exists ff_h_mce_mdr_rec_sourcehsf_positive_successor. ff_h_mce_mdr_rec_sourcehsf_positive_successor + S (ff_s_mce_mdr_rec_sourcehsf_positive) = S ((S (S ff_i_mce_mdr_rec_sourcehsf_positive)) * ff_v_mce_mdr_rec_sourcehsf_positive)) /\ exists ff_q_mce_mdr_rec_sourcehsf_positive_successor. ff_u_mce_mdr_rec_sourcehsf_positive = ff_q_mce_mdr_rec_sourcehsf_positive_successor * S ((S (S ff_i_mce_mdr_rec_sourcehsf_positive)) * ff_v_mce_mdr_rec_sourcehsf_positive) + (ff_s_mce_mdr_rec_sourcehsf_positive))) /\ ff_s_mce_mdr_rec_sourcehsf_positive = ff_r_mce_mdr_rec_sourcehsf_positive + ff_a_mce_mdr_rec_sourcehsf_positive)))))) /\ (exists ff_u_mce_mdr_rec_sourcehsf_negative ff_v_mce_mdr_rec_sourcehsf_negative. ((((exists ff_h_mce_mdr_rec_sourcehsf_negative_start. ff_h_mce_mdr_rec_sourcehsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_rec_sourcehsf_negative)) /\ exists ff_q_mce_mdr_rec_sourcehsf_negative_start. ff_u_mce_mdr_rec_sourcehsf_negative = ff_q_mce_mdr_rec_sourcehsf_negative_start * S ((S (0)) * ff_v_mce_mdr_rec_sourcehsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_rec_sourcehsf_negative_terminal. ff_h_mce_mdr_rec_sourcehsf_negative_terminal + S (mdr_n_rec_sourceh) = S ((S ((S (mdr_q_rec_sourcehs)))) * ff_v_mce_mdr_rec_sourcehsf_negative)) /\ exists ff_q_mce_mdr_rec_sourcehsf_negative_terminal. ff_u_mce_mdr_rec_sourcehsf_negative = ff_q_mce_mdr_rec_sourcehsf_negative_terminal * S ((S ((S (mdr_q_rec_sourcehs)))) * ff_v_mce_mdr_rec_sourcehsf_negative) + (mdr_n_rec_sourceh))) /\ forall ff_i_mce_mdr_rec_sourcehsf_negative. (exists ff_lt_mce_mdr_rec_sourcehsf_negative_bound. ff_lt_mce_mdr_rec_sourcehsf_negative_bound + S ff_i_mce_mdr_rec_sourcehsf_negative = (S (mdr_q_rec_sourcehs))) -> exists ff_a_mce_mdr_rec_sourcehsf_negative ff_r_mce_mdr_rec_sourcehsf_negative ff_s_mce_mdr_rec_sourcehsf_negative. ((((exists ff_h_mce_mdr_rec_sourcehsf_negative_summand. ff_h_mce_mdr_rec_sourcehsf_negative_summand + S (ff_a_mce_mdr_rec_sourcehsf_negative) = S ((S (ff_i_mce_mdr_rec_sourcehsf_negative)) * ff_vc_mce_fold_mdr_rec_sourcehsf)) /\ exists ff_q_mce_mdr_rec_sourcehsf_negative_summand. ff_vb_mce_fold_mdr_rec_sourcehsf = ff_q_mce_mdr_rec_sourcehsf_negative_summand * S ((S (ff_i_mce_mdr_rec_sourcehsf_negative)) * ff_vc_mce_fold_mdr_rec_sourcehsf) + (ff_a_mce_mdr_rec_sourcehsf_negative))) /\ ((((exists ff_h_mce_mdr_rec_sourcehsf_negative_partial. ff_h_mce_mdr_rec_sourcehsf_negative_partial + S (ff_r_mce_mdr_rec_sourcehsf_negative) = S ((S (ff_i_mce_mdr_rec_sourcehsf_negative)) * ff_v_mce_mdr_rec_sourcehsf_negative)) /\ exists ff_q_mce_mdr_rec_sourcehsf_negative_partial. ff_u_mce_mdr_rec_sourcehsf_negative = ff_q_mce_mdr_rec_sourcehsf_negative_partial * S ((S (ff_i_mce_mdr_rec_sourcehsf_negative)) * ff_v_mce_mdr_rec_sourcehsf_negative) + (ff_r_mce_mdr_rec_sourcehsf_negative))) /\ ((((exists ff_h_mce_mdr_rec_sourcehsf_negative_successor. ff_h_mce_mdr_rec_sourcehsf_negative_successor + S (ff_s_mce_mdr_rec_sourcehsf_negative) = S ((S (S ff_i_mce_mdr_rec_sourcehsf_negative)) * ff_v_mce_mdr_rec_sourcehsf_negative)) /\ exists ff_q_mce_mdr_rec_sourcehsf_negative_successor. ff_u_mce_mdr_rec_sourcehsf_negative = ff_q_mce_mdr_rec_sourcehsf_negative_successor * S ((S (S ff_i_mce_mdr_rec_sourcehsf_negative)) * ff_v_mce_mdr_rec_sourcehsf_negative) + (ff_s_mce_mdr_rec_sourcehsf_negative))) /\ ff_s_mce_mdr_rec_sourcehsf_negative = ff_r_mce_mdr_rec_sourcehsf_negative + ff_a_mce_mdr_rec_sourcehsf_negative))))))))))))))) -> exists mdr_u_rec_source mdr_v_rec_source mdr_t_rec_source mdr_p_rec_source mdr_n_rec_source. ((forall mdr_i_rec_sourcerp mdr_a_rec_sourcerp. (exists mdr_gap_rec_sourcerpb. mdr_gap_rec_sourcerpb + S (mdr_i_rec_sourcerp) = (mdr_l_rec_source)) -> (((exists ff_h_mdr_rec_sourcerpo. ff_h_mdr_rec_sourcerpo + S (mdr_a_rec_sourcerp) = S ((S (mdr_i_rec_sourcerp)) * mdr_c_rec_source)) /\ exists ff_q_mdr_rec_sourcerpo. mdr_b_rec_source = ff_q_mdr_rec_sourcerpo * S ((S (mdr_i_rec_sourcerp)) * mdr_c_rec_source) + (mdr_a_rec_sourcerp))) -> (((exists ff_h_mdr_rec_sourcerpn. ff_h_mdr_rec_sourcerpn + S (mdr_a_rec_sourcerp) = S ((S (mdr_i_rec_sourcerp)) * mdr_v_rec_source)) /\ exists ff_q_mdr_rec_sourcerpn. mdr_u_rec_source = ff_q_mdr_rec_sourcerpn * S ((S (mdr_i_rec_sourcerp)) * mdr_v_rec_source) + (mdr_a_rec_sourcerp)))) /\ ((exists mdr_gap_rec_sourcerl. mdr_gap_rec_sourcerl + (mdr_l_rec_source) = (mdr_t_rec_source)) /\ ((forall mdr_i_rec_sourcerh. (exists mdr_gap_rec_sourcerhi. mdr_gap_rec_sourcerhi + S (mdr_i_rec_sourcerh) = (S (mdr_t_rec_source))) -> exists mdr_d_rec_sourcerh mdr_pb_rec_sourcerh mdr_pc_rec_sourcerh mdr_nb_rec_sourcerh mdr_nc_rec_sourcerh mdr_p_rec_sourcerh mdr_n_rec_sourcerh. ((exists mdr_z_rec_sourcerhr. ((exists mdr_a_rec_sourcerhrc mdr_b_rec_sourcerhrc mdr_c_rec_sourcerhrc mdr_e_rec_sourcerhrc mdr_f_rec_sourcerhrc. ((mdr_a_rec_sourcerhrc = ((mdr_d_rec_sourcerh) + (mdr_pb_rec_sourcerh)) * S ((mdr_d_rec_sourcerh) + (mdr_pb_rec_sourcerh)) + ((mdr_pb_rec_sourcerh) + (mdr_pb_rec_sourcerh))) /\ ((mdr_b_rec_sourcerhrc = ((mdr_pc_rec_sourcerh) + (mdr_nb_rec_sourcerh)) * S ((mdr_pc_rec_sourcerh) + (mdr_nb_rec_sourcerh)) + ((mdr_nb_rec_sourcerh) + (mdr_nb_rec_sourcerh))) /\ ((mdr_c_rec_sourcerhrc = ((mdr_a_rec_sourcerhrc) + (mdr_b_rec_sourcerhrc)) * S ((mdr_a_rec_sourcerhrc) + (mdr_b_rec_sourcerhrc)) + ((mdr_b_rec_sourcerhrc) + (mdr_b_rec_sourcerhrc))) /\ ((mdr_e_rec_sourcerhrc = ((mdr_p_rec_sourcerh) + (mdr_n_rec_sourcerh)) * S ((mdr_p_rec_sourcerh) + (mdr_n_rec_sourcerh)) + ((mdr_n_rec_sourcerh) + (mdr_n_rec_sourcerh))) /\ ((mdr_f_rec_sourcerhrc = ((mdr_nc_rec_sourcerh) + (mdr_e_rec_sourcerhrc)) * S ((mdr_nc_rec_sourcerh) + (mdr_e_rec_sourcerhrc)) + ((mdr_e_rec_sourcerhrc) + (mdr_e_rec_sourcerhrc))) /\ ((mdr_z_rec_sourcerhr) = ((mdr_c_rec_sourcerhrc) + (mdr_f_rec_sourcerhrc)) * S ((mdr_c_rec_sourcerhrc) + (mdr_f_rec_sourcerhrc)) + ((mdr_f_rec_sourcerhrc) + (mdr_f_rec_sourcerhrc))))))))) /\ (((exists ff_h_mdr_rec_sourcerhrb. ff_h_mdr_rec_sourcerhrb + S (mdr_z_rec_sourcerhr) = S ((S (mdr_i_rec_sourcerh)) * mdr_v_rec_source)) /\ exists ff_q_mdr_rec_sourcerhrb. mdr_u_rec_source = ff_q_mdr_rec_sourcerhrb * S ((S (mdr_i_rec_sourcerh)) * mdr_v_rec_source) + (mdr_z_rec_sourcerhr))))) /\ (((((mdr_d_rec_sourcerh) = 0) /\ (((mdr_p_rec_sourcerh) = 1) /\ ((mdr_n_rec_sourcerh) = 0))) \/ exists mdr_q_rec_sourcerhs mdr_eb_rec_sourcerhs mdr_ec_rec_sourcerhs mdr_fb_rec_sourcerhs mdr_fc_rec_sourcerhs. (((mdr_d_rec_sourcerh) = S (mdr_q_rec_sourcerhs)) /\ ((forall mdr_j_rec_sourcerhsc. (exists mdr_gap_rec_sourcerhscj. mdr_gap_rec_sourcerhscj + S (mdr_j_rec_sourcerhsc) = (S (mdr_q_rec_sourcerhs))) -> exists mdr_i_rec_sourcerhsc mdr_up_rec_sourcerhsc mdr_us_rec_sourcerhsc mdr_un_rec_sourcerhsc mdr_ut_rec_sourcerhsc mdr_p_rec_sourcerhsc mdr_n_rec_sourcerhsc. ((exists mdr_gap_rec_sourcerhsci. mdr_gap_rec_sourcerhsci + S (mdr_i_rec_sourcerhsc) = (mdr_i_rec_sourcerh)) /\ ((exists mdr_z_rec_sourcerhscr. ((exists mdr_a_rec_sourcerhscrc mdr_b_rec_sourcerhscrc mdr_c_rec_sourcerhscrc mdr_e_rec_sourcerhscrc mdr_f_rec_sourcerhscrc. ((mdr_a_rec_sourcerhscrc = ((mdr_q_rec_sourcerhs) + (mdr_up_rec_sourcerhsc)) * S ((mdr_q_rec_sourcerhs) + (mdr_up_rec_sourcerhsc)) + ((mdr_up_rec_sourcerhsc) + (mdr_up_rec_sourcerhsc))) /\ ((mdr_b_rec_sourcerhscrc = ((mdr_us_rec_sourcerhsc) + (mdr_un_rec_sourcerhsc)) * S ((mdr_us_rec_sourcerhsc) + (mdr_un_rec_sourcerhsc)) + ((mdr_un_rec_sourcerhsc) + (mdr_un_rec_sourcerhsc))) /\ ((mdr_c_rec_sourcerhscrc = ((mdr_a_rec_sourcerhscrc) + (mdr_b_rec_sourcerhscrc)) * S ((mdr_a_rec_sourcerhscrc) + (mdr_b_rec_sourcerhscrc)) + ((mdr_b_rec_sourcerhscrc) + (mdr_b_rec_sourcerhscrc))) /\ ((mdr_e_rec_sourcerhscrc = ((mdr_p_rec_sourcerhsc) + (mdr_n_rec_sourcerhsc)) * S ((mdr_p_rec_sourcerhsc) + (mdr_n_rec_sourcerhsc)) + ((mdr_n_rec_sourcerhsc) + (mdr_n_rec_sourcerhsc))) /\ ((mdr_f_rec_sourcerhscrc = ((mdr_ut_rec_sourcerhsc) + (mdr_e_rec_sourcerhscrc)) * S ((mdr_ut_rec_sourcerhsc) + (mdr_e_rec_sourcerhscrc)) + ((mdr_e_rec_sourcerhscrc) + (mdr_e_rec_sourcerhscrc))) /\ ((mdr_z_rec_sourcerhscr) = ((mdr_c_rec_sourcerhscrc) + (mdr_f_rec_sourcerhscrc)) * S ((mdr_c_rec_sourcerhscrc) + (mdr_f_rec_sourcerhscrc)) + ((mdr_f_rec_sourcerhscrc) + (mdr_f_rec_sourcerhscrc))))))))) /\ (((exists ff_h_mdr_rec_sourcerhscrb. ff_h_mdr_rec_sourcerhscrb + S (mdr_z_rec_sourcerhscr) = S ((S (mdr_i_rec_sourcerhsc)) * mdr_v_rec_source)) /\ exists ff_q_mdr_rec_sourcerhscrb. mdr_u_rec_source = ff_q_mdr_rec_sourcerhscrb * S ((S (mdr_i_rec_sourcerhsc)) * mdr_v_rec_source) + (mdr_z_rec_sourcerhscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_rec_sourcerhscm_positive. (exists ff_gap_mdm_lt_mdr_rec_sourcerhscm_positive_index_bound. ff_gap_mdm_lt_mdr_rec_sourcerhscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_rec_sourcerhscm_positive) = ((mdr_q_rec_sourcerhs) * (mdr_q_rec_sourcerhs))) -> exists ff_row_mdm_prefix_mdr_rec_sourcerhscm_positive ff_column_mdm_prefix_mdr_rec_sourcerhscm_positive ff_value_mdm_prefix_mdr_rec_sourcerhscm_positive. (ff_index_mdm_prefix_mdr_rec_sourcerhscm_positive = (mdr_q_rec_sourcerhs) * ff_row_mdm_prefix_mdr_rec_sourcerhscm_positive + ff_column_mdm_prefix_mdr_rec_sourcerhscm_positive /\ ((exists ff_gap_mdm_lt_mdr_rec_sourcerhscm_positive_column_bound. ff_gap_mdm_lt_mdr_rec_sourcerhscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_rec_sourcerhscm_positive) = (mdr_q_rec_sourcerhs)) /\ ((exists ff_row_mdm_cell_mdr_rec_sourcerhscm_positive_cell ff_column_mdm_cell_mdr_rec_sourcerhscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_rec_sourcerhscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_rec_sourcerhscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_rec_sourcerhscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_rec_sourcerhscm_positive_cell = ff_row_mdm_prefix_mdr_rec_sourcerhscm_positive) \/ ((exists ff_gap_mdm_le_mdr_rec_sourcerhscm_positive_cell_row_after. ff_gap_mdm_le_mdr_rec_sourcerhscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_rec_sourcerhscm_positive)) /\ ff_row_mdm_cell_mdr_rec_sourcerhscm_positive_cell = S ff_row_mdm_prefix_mdr_rec_sourcerhscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_rec_sourcerhscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_rec_sourcerhscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_rec_sourcerhscm_positive) = (mdr_j_rec_sourcerhsc)) /\ ff_column_mdm_cell_mdr_rec_sourcerhscm_positive_cell = ff_column_mdm_prefix_mdr_rec_sourcerhscm_positive) \/ ((exists ff_gap_mdm_le_mdr_rec_sourcerhscm_positive_cell_column_after. ff_gap_mdm_le_mdr_rec_sourcerhscm_positive_cell_column_after + (mdr_j_rec_sourcerhsc) = (ff_column_mdm_prefix_mdr_rec_sourcerhscm_positive)) /\ ff_column_mdm_cell_mdr_rec_sourcerhscm_positive_cell = S ff_column_mdm_prefix_mdr_rec_sourcerhscm_positive))) /\ (((exists ff_h_mdm_mdr_rec_sourcerhscm_positive_cell_source. ff_h_mdm_mdr_rec_sourcerhscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_rec_sourcerhscm_positive) = S ((S ((ff_row_mdm_cell_mdr_rec_sourcerhscm_positive_cell) * (S (mdr_q_rec_sourcerhs)) + (ff_column_mdm_cell_mdr_rec_sourcerhscm_positive_cell))) * mdr_pc_rec_sourcerh)) /\ exists ff_q_mdm_mdr_rec_sourcerhscm_positive_cell_source. mdr_pb_rec_sourcerh = ff_q_mdm_mdr_rec_sourcerhscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_rec_sourcerhscm_positive_cell) * (S (mdr_q_rec_sourcerhs)) + (ff_column_mdm_cell_mdr_rec_sourcerhscm_positive_cell))) * mdr_pc_rec_sourcerh) + (ff_value_mdm_prefix_mdr_rec_sourcerhscm_positive)))))) /\ (((exists ff_h_mdm_mdr_rec_sourcerhscm_positive_target. ff_h_mdm_mdr_rec_sourcerhscm_positive_target + S (ff_value_mdm_prefix_mdr_rec_sourcerhscm_positive) = S ((S (ff_index_mdm_prefix_mdr_rec_sourcerhscm_positive)) * mdr_us_rec_sourcerhsc)) /\ exists ff_q_mdm_mdr_rec_sourcerhscm_positive_target. mdr_up_rec_sourcerhsc = ff_q_mdm_mdr_rec_sourcerhscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_rec_sourcerhscm_positive)) * mdr_us_rec_sourcerhsc) + (ff_value_mdm_prefix_mdr_rec_sourcerhscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_rec_sourcerhscm_negative. (exists ff_gap_mdm_lt_mdr_rec_sourcerhscm_negative_index_bound. ff_gap_mdm_lt_mdr_rec_sourcerhscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_rec_sourcerhscm_negative) = ((mdr_q_rec_sourcerhs) * (mdr_q_rec_sourcerhs))) -> exists ff_row_mdm_prefix_mdr_rec_sourcerhscm_negative ff_column_mdm_prefix_mdr_rec_sourcerhscm_negative ff_value_mdm_prefix_mdr_rec_sourcerhscm_negative. (ff_index_mdm_prefix_mdr_rec_sourcerhscm_negative = (mdr_q_rec_sourcerhs) * ff_row_mdm_prefix_mdr_rec_sourcerhscm_negative + ff_column_mdm_prefix_mdr_rec_sourcerhscm_negative /\ ((exists ff_gap_mdm_lt_mdr_rec_sourcerhscm_negative_column_bound. ff_gap_mdm_lt_mdr_rec_sourcerhscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_rec_sourcerhscm_negative) = (mdr_q_rec_sourcerhs)) /\ ((exists ff_row_mdm_cell_mdr_rec_sourcerhscm_negative_cell ff_column_mdm_cell_mdr_rec_sourcerhscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_rec_sourcerhscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_rec_sourcerhscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_rec_sourcerhscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_rec_sourcerhscm_negative_cell = ff_row_mdm_prefix_mdr_rec_sourcerhscm_negative) \/ ((exists ff_gap_mdm_le_mdr_rec_sourcerhscm_negative_cell_row_after. ff_gap_mdm_le_mdr_rec_sourcerhscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_rec_sourcerhscm_negative)) /\ ff_row_mdm_cell_mdr_rec_sourcerhscm_negative_cell = S ff_row_mdm_prefix_mdr_rec_sourcerhscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_rec_sourcerhscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_rec_sourcerhscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_rec_sourcerhscm_negative) = (mdr_j_rec_sourcerhsc)) /\ ff_column_mdm_cell_mdr_rec_sourcerhscm_negative_cell = ff_column_mdm_prefix_mdr_rec_sourcerhscm_negative) \/ ((exists ff_gap_mdm_le_mdr_rec_sourcerhscm_negative_cell_column_after. ff_gap_mdm_le_mdr_rec_sourcerhscm_negative_cell_column_after + (mdr_j_rec_sourcerhsc) = (ff_column_mdm_prefix_mdr_rec_sourcerhscm_negative)) /\ ff_column_mdm_cell_mdr_rec_sourcerhscm_negative_cell = S ff_column_mdm_prefix_mdr_rec_sourcerhscm_negative))) /\ (((exists ff_h_mdm_mdr_rec_sourcerhscm_negative_cell_source. ff_h_mdm_mdr_rec_sourcerhscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_rec_sourcerhscm_negative) = S ((S ((ff_row_mdm_cell_mdr_rec_sourcerhscm_negative_cell) * (S (mdr_q_rec_sourcerhs)) + (ff_column_mdm_cell_mdr_rec_sourcerhscm_negative_cell))) * mdr_nc_rec_sourcerh)) /\ exists ff_q_mdm_mdr_rec_sourcerhscm_negative_cell_source. mdr_nb_rec_sourcerh = ff_q_mdm_mdr_rec_sourcerhscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_rec_sourcerhscm_negative_cell) * (S (mdr_q_rec_sourcerhs)) + (ff_column_mdm_cell_mdr_rec_sourcerhscm_negative_cell))) * mdr_nc_rec_sourcerh) + (ff_value_mdm_prefix_mdr_rec_sourcerhscm_negative)))))) /\ (((exists ff_h_mdm_mdr_rec_sourcerhscm_negative_target. ff_h_mdm_mdr_rec_sourcerhscm_negative_target + S (ff_value_mdm_prefix_mdr_rec_sourcerhscm_negative) = S ((S (ff_index_mdm_prefix_mdr_rec_sourcerhscm_negative)) * mdr_ut_rec_sourcerhsc)) /\ exists ff_q_mdm_mdr_rec_sourcerhscm_negative_target. mdr_un_rec_sourcerhsc = ff_q_mdm_mdr_rec_sourcerhscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_rec_sourcerhscm_negative)) * mdr_ut_rec_sourcerhsc) + (ff_value_mdm_prefix_mdr_rec_sourcerhscm_negative))))))))) /\ ((((exists ff_h_mdr_rec_sourcerhscp. ff_h_mdr_rec_sourcerhscp + S (mdr_p_rec_sourcerhsc) = S ((S (mdr_j_rec_sourcerhsc)) * mdr_ec_rec_sourcerhs)) /\ exists ff_q_mdr_rec_sourcerhscp. mdr_eb_rec_sourcerhs = ff_q_mdr_rec_sourcerhscp * S ((S (mdr_j_rec_sourcerhsc)) * mdr_ec_rec_sourcerhs) + (mdr_p_rec_sourcerhsc))) /\ (((exists ff_h_mdr_rec_sourcerhscn. ff_h_mdr_rec_sourcerhscn + S (mdr_n_rec_sourcerhsc) = S ((S (mdr_j_rec_sourcerhsc)) * mdr_fc_rec_sourcerhs)) /\ exists ff_q_mdr_rec_sourcerhscn. mdr_fb_rec_sourcerhs = ff_q_mdr_rec_sourcerhscn * S ((S (mdr_j_rec_sourcerhsc)) * mdr_fc_rec_sourcerhs) + (mdr_n_rec_sourcerhsc)))))))) /\ (exists ff_ub_mce_fold_mdr_rec_sourcerhsf ff_uc_mce_fold_mdr_rec_sourcerhsf ff_vb_mce_fold_mdr_rec_sourcerhsf ff_vc_mce_fold_mdr_rec_sourcerhsf. ((forall ff_index_mce_alternating_mdr_rec_sourcerhsf_prefix. (exists ff_gap_mce_mdr_rec_sourcerhsf_prefix_index. ff_gap_mce_mdr_rec_sourcerhsf_prefix_index + S (ff_index_mce_alternating_mdr_rec_sourcerhsf_prefix) = (S (mdr_q_rec_sourcerhs))) -> exists ff_ap_mce_alternating_mdr_rec_sourcerhsf_prefix ff_an_mce_alternating_mdr_rec_sourcerhsf_prefix ff_bp_mce_alternating_mdr_rec_sourcerhsf_prefix ff_bn_mce_alternating_mdr_rec_sourcerhsf_prefix ff_p_mce_alternating_mdr_rec_sourcerhsf_prefix ff_n_mce_alternating_mdr_rec_sourcerhsf_prefix. ((((exists ff_h_mce_mdr_rec_sourcerhsf_prefix_ap. ff_h_mce_mdr_rec_sourcerhsf_prefix_ap + S (ff_ap_mce_alternating_mdr_rec_sourcerhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_rec_sourcerhsf_prefix)) * mdr_pc_rec_sourcerh)) /\ exists ff_q_mce_mdr_rec_sourcerhsf_prefix_ap. mdr_pb_rec_sourcerh = ff_q_mce_mdr_rec_sourcerhsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_rec_sourcerhsf_prefix)) * mdr_pc_rec_sourcerh) + (ff_ap_mce_alternating_mdr_rec_sourcerhsf_prefix))) /\ ((((exists ff_h_mce_mdr_rec_sourcerhsf_prefix_an. ff_h_mce_mdr_rec_sourcerhsf_prefix_an + S (ff_an_mce_alternating_mdr_rec_sourcerhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_rec_sourcerhsf_prefix)) * mdr_nc_rec_sourcerh)) /\ exists ff_q_mce_mdr_rec_sourcerhsf_prefix_an. mdr_nb_rec_sourcerh = ff_q_mce_mdr_rec_sourcerhsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_rec_sourcerhsf_prefix)) * mdr_nc_rec_sourcerh) + (ff_an_mce_alternating_mdr_rec_sourcerhsf_prefix))) /\ ((((exists ff_h_mce_mdr_rec_sourcerhsf_prefix_bp. ff_h_mce_mdr_rec_sourcerhsf_prefix_bp + S (ff_bp_mce_alternating_mdr_rec_sourcerhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_rec_sourcerhsf_prefix)) * mdr_ec_rec_sourcerhs)) /\ exists ff_q_mce_mdr_rec_sourcerhsf_prefix_bp. mdr_eb_rec_sourcerhs = ff_q_mce_mdr_rec_sourcerhsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_rec_sourcerhsf_prefix)) * mdr_ec_rec_sourcerhs) + (ff_bp_mce_alternating_mdr_rec_sourcerhsf_prefix))) /\ ((((exists ff_h_mce_mdr_rec_sourcerhsf_prefix_bn. ff_h_mce_mdr_rec_sourcerhsf_prefix_bn + S (ff_bn_mce_alternating_mdr_rec_sourcerhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_rec_sourcerhsf_prefix)) * mdr_fc_rec_sourcerhs)) /\ exists ff_q_mce_mdr_rec_sourcerhsf_prefix_bn. mdr_fb_rec_sourcerhs = ff_q_mce_mdr_rec_sourcerhsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_rec_sourcerhsf_prefix)) * mdr_fc_rec_sourcerhs) + (ff_bn_mce_alternating_mdr_rec_sourcerhsf_prefix))) /\ ((((exists ff_h_mce_mdr_rec_sourcerhsf_prefix_positive. ff_h_mce_mdr_rec_sourcerhsf_prefix_positive + S (ff_p_mce_alternating_mdr_rec_sourcerhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_rec_sourcerhsf_prefix)) * ff_uc_mce_fold_mdr_rec_sourcerhsf)) /\ exists ff_q_mce_mdr_rec_sourcerhsf_prefix_positive. ff_ub_mce_fold_mdr_rec_sourcerhsf = ff_q_mce_mdr_rec_sourcerhsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_rec_sourcerhsf_prefix)) * ff_uc_mce_fold_mdr_rec_sourcerhsf) + (ff_p_mce_alternating_mdr_rec_sourcerhsf_prefix))) /\ ((((exists ff_h_mce_mdr_rec_sourcerhsf_prefix_negative. ff_h_mce_mdr_rec_sourcerhsf_prefix_negative + S (ff_n_mce_alternating_mdr_rec_sourcerhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_rec_sourcerhsf_prefix)) * ff_vc_mce_fold_mdr_rec_sourcerhsf)) /\ exists ff_q_mce_mdr_rec_sourcerhsf_prefix_negative. ff_vb_mce_fold_mdr_rec_sourcerhsf = ff_q_mce_mdr_rec_sourcerhsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_rec_sourcerhsf_prefix)) * ff_vc_mce_fold_mdr_rec_sourcerhsf) + (ff_n_mce_alternating_mdr_rec_sourcerhsf_prefix))) /\ (((exists ff_even_mce_term_mdr_rec_sourcerhsf_prefix_term. ff_index_mce_alternating_mdr_rec_sourcerhsf_prefix = 2 * ff_even_mce_term_mdr_rec_sourcerhsf_prefix_term) /\ (ff_p_mce_alternating_mdr_rec_sourcerhsf_prefix = (ff_ap_mce_alternating_mdr_rec_sourcerhsf_prefix) * (ff_bp_mce_alternating_mdr_rec_sourcerhsf_prefix) + (ff_an_mce_alternating_mdr_rec_sourcerhsf_prefix) * (ff_bn_mce_alternating_mdr_rec_sourcerhsf_prefix) /\ ff_n_mce_alternating_mdr_rec_sourcerhsf_prefix = (ff_ap_mce_alternating_mdr_rec_sourcerhsf_prefix) * (ff_bn_mce_alternating_mdr_rec_sourcerhsf_prefix) + (ff_an_mce_alternating_mdr_rec_sourcerhsf_prefix) * (ff_bp_mce_alternating_mdr_rec_sourcerhsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_rec_sourcerhsf_prefix_term. ff_index_mce_alternating_mdr_rec_sourcerhsf_prefix = 2 * ff_odd_mce_term_mdr_rec_sourcerhsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_rec_sourcerhsf_prefix = (ff_ap_mce_alternating_mdr_rec_sourcerhsf_prefix) * (ff_bn_mce_alternating_mdr_rec_sourcerhsf_prefix) + (ff_an_mce_alternating_mdr_rec_sourcerhsf_prefix) * (ff_bp_mce_alternating_mdr_rec_sourcerhsf_prefix) /\ ff_n_mce_alternating_mdr_rec_sourcerhsf_prefix = (ff_ap_mce_alternating_mdr_rec_sourcerhsf_prefix) * (ff_bp_mce_alternating_mdr_rec_sourcerhsf_prefix) + (ff_an_mce_alternating_mdr_rec_sourcerhsf_prefix) * (ff_bn_mce_alternating_mdr_rec_sourcerhsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_rec_sourcerhsf_positive ff_v_mce_mdr_rec_sourcerhsf_positive. ((((exists ff_h_mce_mdr_rec_sourcerhsf_positive_start. ff_h_mce_mdr_rec_sourcerhsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_rec_sourcerhsf_positive)) /\ exists ff_q_mce_mdr_rec_sourcerhsf_positive_start. ff_u_mce_mdr_rec_sourcerhsf_positive = ff_q_mce_mdr_rec_sourcerhsf_positive_start * S ((S (0)) * ff_v_mce_mdr_rec_sourcerhsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_rec_sourcerhsf_positive_terminal. ff_h_mce_mdr_rec_sourcerhsf_positive_terminal + S (mdr_p_rec_sourcerh) = S ((S ((S (mdr_q_rec_sourcerhs)))) * ff_v_mce_mdr_rec_sourcerhsf_positive)) /\ exists ff_q_mce_mdr_rec_sourcerhsf_positive_terminal. ff_u_mce_mdr_rec_sourcerhsf_positive = ff_q_mce_mdr_rec_sourcerhsf_positive_terminal * S ((S ((S (mdr_q_rec_sourcerhs)))) * ff_v_mce_mdr_rec_sourcerhsf_positive) + (mdr_p_rec_sourcerh))) /\ forall ff_i_mce_mdr_rec_sourcerhsf_positive. (exists ff_lt_mce_mdr_rec_sourcerhsf_positive_bound. ff_lt_mce_mdr_rec_sourcerhsf_positive_bound + S ff_i_mce_mdr_rec_sourcerhsf_positive = (S (mdr_q_rec_sourcerhs))) -> exists ff_a_mce_mdr_rec_sourcerhsf_positive ff_r_mce_mdr_rec_sourcerhsf_positive ff_s_mce_mdr_rec_sourcerhsf_positive. ((((exists ff_h_mce_mdr_rec_sourcerhsf_positive_summand. ff_h_mce_mdr_rec_sourcerhsf_positive_summand + S (ff_a_mce_mdr_rec_sourcerhsf_positive) = S ((S (ff_i_mce_mdr_rec_sourcerhsf_positive)) * ff_uc_mce_fold_mdr_rec_sourcerhsf)) /\ exists ff_q_mce_mdr_rec_sourcerhsf_positive_summand. ff_ub_mce_fold_mdr_rec_sourcerhsf = ff_q_mce_mdr_rec_sourcerhsf_positive_summand * S ((S (ff_i_mce_mdr_rec_sourcerhsf_positive)) * ff_uc_mce_fold_mdr_rec_sourcerhsf) + (ff_a_mce_mdr_rec_sourcerhsf_positive))) /\ ((((exists ff_h_mce_mdr_rec_sourcerhsf_positive_partial. ff_h_mce_mdr_rec_sourcerhsf_positive_partial + S (ff_r_mce_mdr_rec_sourcerhsf_positive) = S ((S (ff_i_mce_mdr_rec_sourcerhsf_positive)) * ff_v_mce_mdr_rec_sourcerhsf_positive)) /\ exists ff_q_mce_mdr_rec_sourcerhsf_positive_partial. ff_u_mce_mdr_rec_sourcerhsf_positive = ff_q_mce_mdr_rec_sourcerhsf_positive_partial * S ((S (ff_i_mce_mdr_rec_sourcerhsf_positive)) * ff_v_mce_mdr_rec_sourcerhsf_positive) + (ff_r_mce_mdr_rec_sourcerhsf_positive))) /\ ((((exists ff_h_mce_mdr_rec_sourcerhsf_positive_successor. ff_h_mce_mdr_rec_sourcerhsf_positive_successor + S (ff_s_mce_mdr_rec_sourcerhsf_positive) = S ((S (S ff_i_mce_mdr_rec_sourcerhsf_positive)) * ff_v_mce_mdr_rec_sourcerhsf_positive)) /\ exists ff_q_mce_mdr_rec_sourcerhsf_positive_successor. ff_u_mce_mdr_rec_sourcerhsf_positive = ff_q_mce_mdr_rec_sourcerhsf_positive_successor * S ((S (S ff_i_mce_mdr_rec_sourcerhsf_positive)) * ff_v_mce_mdr_rec_sourcerhsf_positive) + (ff_s_mce_mdr_rec_sourcerhsf_positive))) /\ ff_s_mce_mdr_rec_sourcerhsf_positive = ff_r_mce_mdr_rec_sourcerhsf_positive + ff_a_mce_mdr_rec_sourcerhsf_positive)))))) /\ (exists ff_u_mce_mdr_rec_sourcerhsf_negative ff_v_mce_mdr_rec_sourcerhsf_negative. ((((exists ff_h_mce_mdr_rec_sourcerhsf_negative_start. ff_h_mce_mdr_rec_sourcerhsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_rec_sourcerhsf_negative)) /\ exists ff_q_mce_mdr_rec_sourcerhsf_negative_start. ff_u_mce_mdr_rec_sourcerhsf_negative = ff_q_mce_mdr_rec_sourcerhsf_negative_start * S ((S (0)) * ff_v_mce_mdr_rec_sourcerhsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_rec_sourcerhsf_negative_terminal. ff_h_mce_mdr_rec_sourcerhsf_negative_terminal + S (mdr_n_rec_sourcerh) = S ((S ((S (mdr_q_rec_sourcerhs)))) * ff_v_mce_mdr_rec_sourcerhsf_negative)) /\ exists ff_q_mce_mdr_rec_sourcerhsf_negative_terminal. ff_u_mce_mdr_rec_sourcerhsf_negative = ff_q_mce_mdr_rec_sourcerhsf_negative_terminal * S ((S ((S (mdr_q_rec_sourcerhs)))) * ff_v_mce_mdr_rec_sourcerhsf_negative) + (mdr_n_rec_sourcerh))) /\ forall ff_i_mce_mdr_rec_sourcerhsf_negative. (exists ff_lt_mce_mdr_rec_sourcerhsf_negative_bound. ff_lt_mce_mdr_rec_sourcerhsf_negative_bound + S ff_i_mce_mdr_rec_sourcerhsf_negative = (S (mdr_q_rec_sourcerhs))) -> exists ff_a_mce_mdr_rec_sourcerhsf_negative ff_r_mce_mdr_rec_sourcerhsf_negative ff_s_mce_mdr_rec_sourcerhsf_negative. ((((exists ff_h_mce_mdr_rec_sourcerhsf_negative_summand. ff_h_mce_mdr_rec_sourcerhsf_negative_summand + S (ff_a_mce_mdr_rec_sourcerhsf_negative) = S ((S (ff_i_mce_mdr_rec_sourcerhsf_negative)) * ff_vc_mce_fold_mdr_rec_sourcerhsf)) /\ exists ff_q_mce_mdr_rec_sourcerhsf_negative_summand. ff_vb_mce_fold_mdr_rec_sourcerhsf = ff_q_mce_mdr_rec_sourcerhsf_negative_summand * S ((S (ff_i_mce_mdr_rec_sourcerhsf_negative)) * ff_vc_mce_fold_mdr_rec_sourcerhsf) + (ff_a_mce_mdr_rec_sourcerhsf_negative))) /\ ((((exists ff_h_mce_mdr_rec_sourcerhsf_negative_partial. ff_h_mce_mdr_rec_sourcerhsf_negative_partial + S (ff_r_mce_mdr_rec_sourcerhsf_negative) = S ((S (ff_i_mce_mdr_rec_sourcerhsf_negative)) * ff_v_mce_mdr_rec_sourcerhsf_negative)) /\ exists ff_q_mce_mdr_rec_sourcerhsf_negative_partial. ff_u_mce_mdr_rec_sourcerhsf_negative = ff_q_mce_mdr_rec_sourcerhsf_negative_partial * S ((S (ff_i_mce_mdr_rec_sourcerhsf_negative)) * ff_v_mce_mdr_rec_sourcerhsf_negative) + (ff_r_mce_mdr_rec_sourcerhsf_negative))) /\ ((((exists ff_h_mce_mdr_rec_sourcerhsf_negative_successor. ff_h_mce_mdr_rec_sourcerhsf_negative_successor + S (ff_s_mce_mdr_rec_sourcerhsf_negative) = S ((S (S ff_i_mce_mdr_rec_sourcerhsf_negative)) * ff_v_mce_mdr_rec_sourcerhsf_negative)) /\ exists ff_q_mce_mdr_rec_sourcerhsf_negative_successor. ff_u_mce_mdr_rec_sourcerhsf_negative = ff_q_mce_mdr_rec_sourcerhsf_negative_successor * S ((S (S ff_i_mce_mdr_rec_sourcerhsf_negative)) * ff_v_mce_mdr_rec_sourcerhsf_negative) + (ff_s_mce_mdr_rec_sourcerhsf_negative))) /\ ff_s_mce_mdr_rec_sourcerhsf_negative = ff_r_mce_mdr_rec_sourcerhsf_negative + ff_a_mce_mdr_rec_sourcerhsf_negative))))))))))))))) /\ (exists mdr_z_rec_sourcerr. ((exists mdr_a_rec_sourcerrc mdr_b_rec_sourcerrc mdr_c_rec_sourcerrc mdr_e_rec_sourcerrc mdr_f_rec_sourcerrc. ((mdr_a_rec_sourcerrc = ((q) + (mdr_pb_rec_source)) * S ((q) + (mdr_pb_rec_source)) + ((mdr_pb_rec_source) + (mdr_pb_rec_source))) /\ ((mdr_b_rec_sourcerrc = ((mdr_pc_rec_source) + (mdr_nb_rec_source)) * S ((mdr_pc_rec_source) + (mdr_nb_rec_source)) + ((mdr_nb_rec_source) + (mdr_nb_rec_source))) /\ ((mdr_c_rec_sourcerrc = ((mdr_a_rec_sourcerrc) + (mdr_b_rec_sourcerrc)) * S ((mdr_a_rec_sourcerrc) + (mdr_b_rec_sourcerrc)) + ((mdr_b_rec_sourcerrc) + (mdr_b_rec_sourcerrc))) /\ ((mdr_e_rec_sourcerrc = ((mdr_p_rec_source) + (mdr_n_rec_source)) * S ((mdr_p_rec_source) + (mdr_n_rec_source)) + ((mdr_n_rec_source) + (mdr_n_rec_source))) /\ ((mdr_f_rec_sourcerrc = ((mdr_nc_rec_source) + (mdr_e_rec_sourcerrc)) * S ((mdr_nc_rec_source) + (mdr_e_rec_sourcerrc)) + ((mdr_e_rec_sourcerrc) + (mdr_e_rec_sourcerrc))) /\ ((mdr_z_rec_sourcerr) = ((mdr_c_rec_sourcerrc) + (mdr_f_rec_sourcerrc)) * S ((mdr_c_rec_sourcerrc) + (mdr_f_rec_sourcerrc)) + ((mdr_f_rec_sourcerrc) + (mdr_f_rec_sourcerrc))))))))) /\ (((exists ff_h_mdr_rec_sourcerrb. ff_h_mdr_rec_sourcerrb + S (mdr_z_rec_sourcerr) = S ((S (mdr_t_rec_source)) * mdr_v_rec_source)) /\ exists ff_q_mdr_rec_sourcerrb. mdr_u_rec_source = ff_q_mdr_rec_sourcerrb * S ((S (mdr_t_rec_source)) * mdr_v_rec_source) + (mdr_z_rec_sourcerr))))))))) -> (forall mdr_pb_rec_result mdr_pc_rec_result mdr_nb_rec_result mdr_nc_rec_result mdr_b_rec_result mdr_c_rec_result mdr_l_rec_result. (forall mdr_i_rec_resulth. (exists mdr_gap_rec_resulthi. mdr_gap_rec_resulthi + S (mdr_i_rec_resulth) = (mdr_l_rec_result)) -> exists mdr_d_rec_resulth mdr_pb_rec_resulth mdr_pc_rec_resulth mdr_nb_rec_resulth mdr_nc_rec_resulth mdr_p_rec_resulth mdr_n_rec_resulth. ((exists mdr_z_rec_resulthr. ((exists mdr_a_rec_resulthrc mdr_b_rec_resulthrc mdr_c_rec_resulthrc mdr_e_rec_resulthrc mdr_f_rec_resulthrc. ((mdr_a_rec_resulthrc = ((mdr_d_rec_resulth) + (mdr_pb_rec_resulth)) * S ((mdr_d_rec_resulth) + (mdr_pb_rec_resulth)) + ((mdr_pb_rec_resulth) + (mdr_pb_rec_resulth))) /\ ((mdr_b_rec_resulthrc = ((mdr_pc_rec_resulth) + (mdr_nb_rec_resulth)) * S ((mdr_pc_rec_resulth) + (mdr_nb_rec_resulth)) + ((mdr_nb_rec_resulth) + (mdr_nb_rec_resulth))) /\ ((mdr_c_rec_resulthrc = ((mdr_a_rec_resulthrc) + (mdr_b_rec_resulthrc)) * S ((mdr_a_rec_resulthrc) + (mdr_b_rec_resulthrc)) + ((mdr_b_rec_resulthrc) + (mdr_b_rec_resulthrc))) /\ ((mdr_e_rec_resulthrc = ((mdr_p_rec_resulth) + (mdr_n_rec_resulth)) * S ((mdr_p_rec_resulth) + (mdr_n_rec_resulth)) + ((mdr_n_rec_resulth) + (mdr_n_rec_resulth))) /\ ((mdr_f_rec_resulthrc = ((mdr_nc_rec_resulth) + (mdr_e_rec_resulthrc)) * S ((mdr_nc_rec_resulth) + (mdr_e_rec_resulthrc)) + ((mdr_e_rec_resulthrc) + (mdr_e_rec_resulthrc))) /\ ((mdr_z_rec_resulthr) = ((mdr_c_rec_resulthrc) + (mdr_f_rec_resulthrc)) * S ((mdr_c_rec_resulthrc) + (mdr_f_rec_resulthrc)) + ((mdr_f_rec_resulthrc) + (mdr_f_rec_resulthrc))))))))) /\ (((exists ff_h_mdr_rec_resulthrb. ff_h_mdr_rec_resulthrb + S (mdr_z_rec_resulthr) = S ((S (mdr_i_rec_resulth)) * mdr_c_rec_result)) /\ exists ff_q_mdr_rec_resulthrb. mdr_b_rec_result = ff_q_mdr_rec_resulthrb * S ((S (mdr_i_rec_resulth)) * mdr_c_rec_result) + (mdr_z_rec_resulthr))))) /\ (((((mdr_d_rec_resulth) = 0) /\ (((mdr_p_rec_resulth) = 1) /\ ((mdr_n_rec_resulth) = 0))) \/ exists mdr_q_rec_resulths mdr_eb_rec_resulths mdr_ec_rec_resulths mdr_fb_rec_resulths mdr_fc_rec_resulths. (((mdr_d_rec_resulth) = S (mdr_q_rec_resulths)) /\ ((forall mdr_j_rec_resulthsc. (exists mdr_gap_rec_resulthscj. mdr_gap_rec_resulthscj + S (mdr_j_rec_resulthsc) = (S (mdr_q_rec_resulths))) -> exists mdr_i_rec_resulthsc mdr_up_rec_resulthsc mdr_us_rec_resulthsc mdr_un_rec_resulthsc mdr_ut_rec_resulthsc mdr_p_rec_resulthsc mdr_n_rec_resulthsc. ((exists mdr_gap_rec_resulthsci. mdr_gap_rec_resulthsci + S (mdr_i_rec_resulthsc) = (mdr_i_rec_resulth)) /\ ((exists mdr_z_rec_resulthscr. ((exists mdr_a_rec_resulthscrc mdr_b_rec_resulthscrc mdr_c_rec_resulthscrc mdr_e_rec_resulthscrc mdr_f_rec_resulthscrc. ((mdr_a_rec_resulthscrc = ((mdr_q_rec_resulths) + (mdr_up_rec_resulthsc)) * S ((mdr_q_rec_resulths) + (mdr_up_rec_resulthsc)) + ((mdr_up_rec_resulthsc) + (mdr_up_rec_resulthsc))) /\ ((mdr_b_rec_resulthscrc = ((mdr_us_rec_resulthsc) + (mdr_un_rec_resulthsc)) * S ((mdr_us_rec_resulthsc) + (mdr_un_rec_resulthsc)) + ((mdr_un_rec_resulthsc) + (mdr_un_rec_resulthsc))) /\ ((mdr_c_rec_resulthscrc = ((mdr_a_rec_resulthscrc) + (mdr_b_rec_resulthscrc)) * S ((mdr_a_rec_resulthscrc) + (mdr_b_rec_resulthscrc)) + ((mdr_b_rec_resulthscrc) + (mdr_b_rec_resulthscrc))) /\ ((mdr_e_rec_resulthscrc = ((mdr_p_rec_resulthsc) + (mdr_n_rec_resulthsc)) * S ((mdr_p_rec_resulthsc) + (mdr_n_rec_resulthsc)) + ((mdr_n_rec_resulthsc) + (mdr_n_rec_resulthsc))) /\ ((mdr_f_rec_resulthscrc = ((mdr_ut_rec_resulthsc) + (mdr_e_rec_resulthscrc)) * S ((mdr_ut_rec_resulthsc) + (mdr_e_rec_resulthscrc)) + ((mdr_e_rec_resulthscrc) + (mdr_e_rec_resulthscrc))) /\ ((mdr_z_rec_resulthscr) = ((mdr_c_rec_resulthscrc) + (mdr_f_rec_resulthscrc)) * S ((mdr_c_rec_resulthscrc) + (mdr_f_rec_resulthscrc)) + ((mdr_f_rec_resulthscrc) + (mdr_f_rec_resulthscrc))))))))) /\ (((exists ff_h_mdr_rec_resulthscrb. ff_h_mdr_rec_resulthscrb + S (mdr_z_rec_resulthscr) = S ((S (mdr_i_rec_resulthsc)) * mdr_c_rec_result)) /\ exists ff_q_mdr_rec_resulthscrb. mdr_b_rec_result = ff_q_mdr_rec_resulthscrb * S ((S (mdr_i_rec_resulthsc)) * mdr_c_rec_result) + (mdr_z_rec_resulthscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_rec_resulthscm_positive. (exists ff_gap_mdm_lt_mdr_rec_resulthscm_positive_index_bound. ff_gap_mdm_lt_mdr_rec_resulthscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_rec_resulthscm_positive) = ((mdr_q_rec_resulths) * (mdr_q_rec_resulths))) -> exists ff_row_mdm_prefix_mdr_rec_resulthscm_positive ff_column_mdm_prefix_mdr_rec_resulthscm_positive ff_value_mdm_prefix_mdr_rec_resulthscm_positive. (ff_index_mdm_prefix_mdr_rec_resulthscm_positive = (mdr_q_rec_resulths) * ff_row_mdm_prefix_mdr_rec_resulthscm_positive + ff_column_mdm_prefix_mdr_rec_resulthscm_positive /\ ((exists ff_gap_mdm_lt_mdr_rec_resulthscm_positive_column_bound. ff_gap_mdm_lt_mdr_rec_resulthscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_rec_resulthscm_positive) = (mdr_q_rec_resulths)) /\ ((exists ff_row_mdm_cell_mdr_rec_resulthscm_positive_cell ff_column_mdm_cell_mdr_rec_resulthscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_rec_resulthscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_rec_resulthscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_rec_resulthscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_rec_resulthscm_positive_cell = ff_row_mdm_prefix_mdr_rec_resulthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_rec_resulthscm_positive_cell_row_after. ff_gap_mdm_le_mdr_rec_resulthscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_rec_resulthscm_positive)) /\ ff_row_mdm_cell_mdr_rec_resulthscm_positive_cell = S ff_row_mdm_prefix_mdr_rec_resulthscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_rec_resulthscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_rec_resulthscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_rec_resulthscm_positive) = (mdr_j_rec_resulthsc)) /\ ff_column_mdm_cell_mdr_rec_resulthscm_positive_cell = ff_column_mdm_prefix_mdr_rec_resulthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_rec_resulthscm_positive_cell_column_after. ff_gap_mdm_le_mdr_rec_resulthscm_positive_cell_column_after + (mdr_j_rec_resulthsc) = (ff_column_mdm_prefix_mdr_rec_resulthscm_positive)) /\ ff_column_mdm_cell_mdr_rec_resulthscm_positive_cell = S ff_column_mdm_prefix_mdr_rec_resulthscm_positive))) /\ (((exists ff_h_mdm_mdr_rec_resulthscm_positive_cell_source. ff_h_mdm_mdr_rec_resulthscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_rec_resulthscm_positive) = S ((S ((ff_row_mdm_cell_mdr_rec_resulthscm_positive_cell) * (S (mdr_q_rec_resulths)) + (ff_column_mdm_cell_mdr_rec_resulthscm_positive_cell))) * mdr_pc_rec_resulth)) /\ exists ff_q_mdm_mdr_rec_resulthscm_positive_cell_source. mdr_pb_rec_resulth = ff_q_mdm_mdr_rec_resulthscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_rec_resulthscm_positive_cell) * (S (mdr_q_rec_resulths)) + (ff_column_mdm_cell_mdr_rec_resulthscm_positive_cell))) * mdr_pc_rec_resulth) + (ff_value_mdm_prefix_mdr_rec_resulthscm_positive)))))) /\ (((exists ff_h_mdm_mdr_rec_resulthscm_positive_target. ff_h_mdm_mdr_rec_resulthscm_positive_target + S (ff_value_mdm_prefix_mdr_rec_resulthscm_positive) = S ((S (ff_index_mdm_prefix_mdr_rec_resulthscm_positive)) * mdr_us_rec_resulthsc)) /\ exists ff_q_mdm_mdr_rec_resulthscm_positive_target. mdr_up_rec_resulthsc = ff_q_mdm_mdr_rec_resulthscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_rec_resulthscm_positive)) * mdr_us_rec_resulthsc) + (ff_value_mdm_prefix_mdr_rec_resulthscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_rec_resulthscm_negative. (exists ff_gap_mdm_lt_mdr_rec_resulthscm_negative_index_bound. ff_gap_mdm_lt_mdr_rec_resulthscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_rec_resulthscm_negative) = ((mdr_q_rec_resulths) * (mdr_q_rec_resulths))) -> exists ff_row_mdm_prefix_mdr_rec_resulthscm_negative ff_column_mdm_prefix_mdr_rec_resulthscm_negative ff_value_mdm_prefix_mdr_rec_resulthscm_negative. (ff_index_mdm_prefix_mdr_rec_resulthscm_negative = (mdr_q_rec_resulths) * ff_row_mdm_prefix_mdr_rec_resulthscm_negative + ff_column_mdm_prefix_mdr_rec_resulthscm_negative /\ ((exists ff_gap_mdm_lt_mdr_rec_resulthscm_negative_column_bound. ff_gap_mdm_lt_mdr_rec_resulthscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_rec_resulthscm_negative) = (mdr_q_rec_resulths)) /\ ((exists ff_row_mdm_cell_mdr_rec_resulthscm_negative_cell ff_column_mdm_cell_mdr_rec_resulthscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_rec_resulthscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_rec_resulthscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_rec_resulthscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_rec_resulthscm_negative_cell = ff_row_mdm_prefix_mdr_rec_resulthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_rec_resulthscm_negative_cell_row_after. ff_gap_mdm_le_mdr_rec_resulthscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_rec_resulthscm_negative)) /\ ff_row_mdm_cell_mdr_rec_resulthscm_negative_cell = S ff_row_mdm_prefix_mdr_rec_resulthscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_rec_resulthscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_rec_resulthscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_rec_resulthscm_negative) = (mdr_j_rec_resulthsc)) /\ ff_column_mdm_cell_mdr_rec_resulthscm_negative_cell = ff_column_mdm_prefix_mdr_rec_resulthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_rec_resulthscm_negative_cell_column_after. ff_gap_mdm_le_mdr_rec_resulthscm_negative_cell_column_after + (mdr_j_rec_resulthsc) = (ff_column_mdm_prefix_mdr_rec_resulthscm_negative)) /\ ff_column_mdm_cell_mdr_rec_resulthscm_negative_cell = S ff_column_mdm_prefix_mdr_rec_resulthscm_negative))) /\ (((exists ff_h_mdm_mdr_rec_resulthscm_negative_cell_source. ff_h_mdm_mdr_rec_resulthscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_rec_resulthscm_negative) = S ((S ((ff_row_mdm_cell_mdr_rec_resulthscm_negative_cell) * (S (mdr_q_rec_resulths)) + (ff_column_mdm_cell_mdr_rec_resulthscm_negative_cell))) * mdr_nc_rec_resulth)) /\ exists ff_q_mdm_mdr_rec_resulthscm_negative_cell_source. mdr_nb_rec_resulth = ff_q_mdm_mdr_rec_resulthscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_rec_resulthscm_negative_cell) * (S (mdr_q_rec_resulths)) + (ff_column_mdm_cell_mdr_rec_resulthscm_negative_cell))) * mdr_nc_rec_resulth) + (ff_value_mdm_prefix_mdr_rec_resulthscm_negative)))))) /\ (((exists ff_h_mdm_mdr_rec_resulthscm_negative_target. ff_h_mdm_mdr_rec_resulthscm_negative_target + S (ff_value_mdm_prefix_mdr_rec_resulthscm_negative) = S ((S (ff_index_mdm_prefix_mdr_rec_resulthscm_negative)) * mdr_ut_rec_resulthsc)) /\ exists ff_q_mdm_mdr_rec_resulthscm_negative_target. mdr_un_rec_resulthsc = ff_q_mdm_mdr_rec_resulthscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_rec_resulthscm_negative)) * mdr_ut_rec_resulthsc) + (ff_value_mdm_prefix_mdr_rec_resulthscm_negative))))))))) /\ ((((exists ff_h_mdr_rec_resulthscp. ff_h_mdr_rec_resulthscp + S (mdr_p_rec_resulthsc) = S ((S (mdr_j_rec_resulthsc)) * mdr_ec_rec_resulths)) /\ exists ff_q_mdr_rec_resulthscp. mdr_eb_rec_resulths = ff_q_mdr_rec_resulthscp * S ((S (mdr_j_rec_resulthsc)) * mdr_ec_rec_resulths) + (mdr_p_rec_resulthsc))) /\ (((exists ff_h_mdr_rec_resulthscn. ff_h_mdr_rec_resulthscn + S (mdr_n_rec_resulthsc) = S ((S (mdr_j_rec_resulthsc)) * mdr_fc_rec_resulths)) /\ exists ff_q_mdr_rec_resulthscn. mdr_fb_rec_resulths = ff_q_mdr_rec_resulthscn * S ((S (mdr_j_rec_resulthsc)) * mdr_fc_rec_resulths) + (mdr_n_rec_resulthsc)))))))) /\ (exists ff_ub_mce_fold_mdr_rec_resulthsf ff_uc_mce_fold_mdr_rec_resulthsf ff_vb_mce_fold_mdr_rec_resulthsf ff_vc_mce_fold_mdr_rec_resulthsf. ((forall ff_index_mce_alternating_mdr_rec_resulthsf_prefix. (exists ff_gap_mce_mdr_rec_resulthsf_prefix_index. ff_gap_mce_mdr_rec_resulthsf_prefix_index + S (ff_index_mce_alternating_mdr_rec_resulthsf_prefix) = (S (mdr_q_rec_resulths))) -> exists ff_ap_mce_alternating_mdr_rec_resulthsf_prefix ff_an_mce_alternating_mdr_rec_resulthsf_prefix ff_bp_mce_alternating_mdr_rec_resulthsf_prefix ff_bn_mce_alternating_mdr_rec_resulthsf_prefix ff_p_mce_alternating_mdr_rec_resulthsf_prefix ff_n_mce_alternating_mdr_rec_resulthsf_prefix. ((((exists ff_h_mce_mdr_rec_resulthsf_prefix_ap. ff_h_mce_mdr_rec_resulthsf_prefix_ap + S (ff_ap_mce_alternating_mdr_rec_resulthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_rec_resulthsf_prefix)) * mdr_pc_rec_resulth)) /\ exists ff_q_mce_mdr_rec_resulthsf_prefix_ap. mdr_pb_rec_resulth = ff_q_mce_mdr_rec_resulthsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_rec_resulthsf_prefix)) * mdr_pc_rec_resulth) + (ff_ap_mce_alternating_mdr_rec_resulthsf_prefix))) /\ ((((exists ff_h_mce_mdr_rec_resulthsf_prefix_an. ff_h_mce_mdr_rec_resulthsf_prefix_an + S (ff_an_mce_alternating_mdr_rec_resulthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_rec_resulthsf_prefix)) * mdr_nc_rec_resulth)) /\ exists ff_q_mce_mdr_rec_resulthsf_prefix_an. mdr_nb_rec_resulth = ff_q_mce_mdr_rec_resulthsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_rec_resulthsf_prefix)) * mdr_nc_rec_resulth) + (ff_an_mce_alternating_mdr_rec_resulthsf_prefix))) /\ ((((exists ff_h_mce_mdr_rec_resulthsf_prefix_bp. ff_h_mce_mdr_rec_resulthsf_prefix_bp + S (ff_bp_mce_alternating_mdr_rec_resulthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_rec_resulthsf_prefix)) * mdr_ec_rec_resulths)) /\ exists ff_q_mce_mdr_rec_resulthsf_prefix_bp. mdr_eb_rec_resulths = ff_q_mce_mdr_rec_resulthsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_rec_resulthsf_prefix)) * mdr_ec_rec_resulths) + (ff_bp_mce_alternating_mdr_rec_resulthsf_prefix))) /\ ((((exists ff_h_mce_mdr_rec_resulthsf_prefix_bn. ff_h_mce_mdr_rec_resulthsf_prefix_bn + S (ff_bn_mce_alternating_mdr_rec_resulthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_rec_resulthsf_prefix)) * mdr_fc_rec_resulths)) /\ exists ff_q_mce_mdr_rec_resulthsf_prefix_bn. mdr_fb_rec_resulths = ff_q_mce_mdr_rec_resulthsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_rec_resulthsf_prefix)) * mdr_fc_rec_resulths) + (ff_bn_mce_alternating_mdr_rec_resulthsf_prefix))) /\ ((((exists ff_h_mce_mdr_rec_resulthsf_prefix_positive. ff_h_mce_mdr_rec_resulthsf_prefix_positive + S (ff_p_mce_alternating_mdr_rec_resulthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_rec_resulthsf_prefix)) * ff_uc_mce_fold_mdr_rec_resulthsf)) /\ exists ff_q_mce_mdr_rec_resulthsf_prefix_positive. ff_ub_mce_fold_mdr_rec_resulthsf = ff_q_mce_mdr_rec_resulthsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_rec_resulthsf_prefix)) * ff_uc_mce_fold_mdr_rec_resulthsf) + (ff_p_mce_alternating_mdr_rec_resulthsf_prefix))) /\ ((((exists ff_h_mce_mdr_rec_resulthsf_prefix_negative. ff_h_mce_mdr_rec_resulthsf_prefix_negative + S (ff_n_mce_alternating_mdr_rec_resulthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_rec_resulthsf_prefix)) * ff_vc_mce_fold_mdr_rec_resulthsf)) /\ exists ff_q_mce_mdr_rec_resulthsf_prefix_negative. ff_vb_mce_fold_mdr_rec_resulthsf = ff_q_mce_mdr_rec_resulthsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_rec_resulthsf_prefix)) * ff_vc_mce_fold_mdr_rec_resulthsf) + (ff_n_mce_alternating_mdr_rec_resulthsf_prefix))) /\ (((exists ff_even_mce_term_mdr_rec_resulthsf_prefix_term. ff_index_mce_alternating_mdr_rec_resulthsf_prefix = 2 * ff_even_mce_term_mdr_rec_resulthsf_prefix_term) /\ (ff_p_mce_alternating_mdr_rec_resulthsf_prefix = (ff_ap_mce_alternating_mdr_rec_resulthsf_prefix) * (ff_bp_mce_alternating_mdr_rec_resulthsf_prefix) + (ff_an_mce_alternating_mdr_rec_resulthsf_prefix) * (ff_bn_mce_alternating_mdr_rec_resulthsf_prefix) /\ ff_n_mce_alternating_mdr_rec_resulthsf_prefix = (ff_ap_mce_alternating_mdr_rec_resulthsf_prefix) * (ff_bn_mce_alternating_mdr_rec_resulthsf_prefix) + (ff_an_mce_alternating_mdr_rec_resulthsf_prefix) * (ff_bp_mce_alternating_mdr_rec_resulthsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_rec_resulthsf_prefix_term. ff_index_mce_alternating_mdr_rec_resulthsf_prefix = 2 * ff_odd_mce_term_mdr_rec_resulthsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_rec_resulthsf_prefix = (ff_ap_mce_alternating_mdr_rec_resulthsf_prefix) * (ff_bn_mce_alternating_mdr_rec_resulthsf_prefix) + (ff_an_mce_alternating_mdr_rec_resulthsf_prefix) * (ff_bp_mce_alternating_mdr_rec_resulthsf_prefix) /\ ff_n_mce_alternating_mdr_rec_resulthsf_prefix = (ff_ap_mce_alternating_mdr_rec_resulthsf_prefix) * (ff_bp_mce_alternating_mdr_rec_resulthsf_prefix) + (ff_an_mce_alternating_mdr_rec_resulthsf_prefix) * (ff_bn_mce_alternating_mdr_rec_resulthsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_rec_resulthsf_positive ff_v_mce_mdr_rec_resulthsf_positive. ((((exists ff_h_mce_mdr_rec_resulthsf_positive_start. ff_h_mce_mdr_rec_resulthsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_rec_resulthsf_positive)) /\ exists ff_q_mce_mdr_rec_resulthsf_positive_start. ff_u_mce_mdr_rec_resulthsf_positive = ff_q_mce_mdr_rec_resulthsf_positive_start * S ((S (0)) * ff_v_mce_mdr_rec_resulthsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_rec_resulthsf_positive_terminal. ff_h_mce_mdr_rec_resulthsf_positive_terminal + S (mdr_p_rec_resulth) = S ((S ((S (mdr_q_rec_resulths)))) * ff_v_mce_mdr_rec_resulthsf_positive)) /\ exists ff_q_mce_mdr_rec_resulthsf_positive_terminal. ff_u_mce_mdr_rec_resulthsf_positive = ff_q_mce_mdr_rec_resulthsf_positive_terminal * S ((S ((S (mdr_q_rec_resulths)))) * ff_v_mce_mdr_rec_resulthsf_positive) + (mdr_p_rec_resulth))) /\ forall ff_i_mce_mdr_rec_resulthsf_positive. (exists ff_lt_mce_mdr_rec_resulthsf_positive_bound. ff_lt_mce_mdr_rec_resulthsf_positive_bound + S ff_i_mce_mdr_rec_resulthsf_positive = (S (mdr_q_rec_resulths))) -> exists ff_a_mce_mdr_rec_resulthsf_positive ff_r_mce_mdr_rec_resulthsf_positive ff_s_mce_mdr_rec_resulthsf_positive. ((((exists ff_h_mce_mdr_rec_resulthsf_positive_summand. ff_h_mce_mdr_rec_resulthsf_positive_summand + S (ff_a_mce_mdr_rec_resulthsf_positive) = S ((S (ff_i_mce_mdr_rec_resulthsf_positive)) * ff_uc_mce_fold_mdr_rec_resulthsf)) /\ exists ff_q_mce_mdr_rec_resulthsf_positive_summand. ff_ub_mce_fold_mdr_rec_resulthsf = ff_q_mce_mdr_rec_resulthsf_positive_summand * S ((S (ff_i_mce_mdr_rec_resulthsf_positive)) * ff_uc_mce_fold_mdr_rec_resulthsf) + (ff_a_mce_mdr_rec_resulthsf_positive))) /\ ((((exists ff_h_mce_mdr_rec_resulthsf_positive_partial. ff_h_mce_mdr_rec_resulthsf_positive_partial + S (ff_r_mce_mdr_rec_resulthsf_positive) = S ((S (ff_i_mce_mdr_rec_resulthsf_positive)) * ff_v_mce_mdr_rec_resulthsf_positive)) /\ exists ff_q_mce_mdr_rec_resulthsf_positive_partial. ff_u_mce_mdr_rec_resulthsf_positive = ff_q_mce_mdr_rec_resulthsf_positive_partial * S ((S (ff_i_mce_mdr_rec_resulthsf_positive)) * ff_v_mce_mdr_rec_resulthsf_positive) + (ff_r_mce_mdr_rec_resulthsf_positive))) /\ ((((exists ff_h_mce_mdr_rec_resulthsf_positive_successor. ff_h_mce_mdr_rec_resulthsf_positive_successor + S (ff_s_mce_mdr_rec_resulthsf_positive) = S ((S (S ff_i_mce_mdr_rec_resulthsf_positive)) * ff_v_mce_mdr_rec_resulthsf_positive)) /\ exists ff_q_mce_mdr_rec_resulthsf_positive_successor. ff_u_mce_mdr_rec_resulthsf_positive = ff_q_mce_mdr_rec_resulthsf_positive_successor * S ((S (S ff_i_mce_mdr_rec_resulthsf_positive)) * ff_v_mce_mdr_rec_resulthsf_positive) + (ff_s_mce_mdr_rec_resulthsf_positive))) /\ ff_s_mce_mdr_rec_resulthsf_positive = ff_r_mce_mdr_rec_resulthsf_positive + ff_a_mce_mdr_rec_resulthsf_positive)))))) /\ (exists ff_u_mce_mdr_rec_resulthsf_negative ff_v_mce_mdr_rec_resulthsf_negative. ((((exists ff_h_mce_mdr_rec_resulthsf_negative_start. ff_h_mce_mdr_rec_resulthsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_rec_resulthsf_negative)) /\ exists ff_q_mce_mdr_rec_resulthsf_negative_start. ff_u_mce_mdr_rec_resulthsf_negative = ff_q_mce_mdr_rec_resulthsf_negative_start * S ((S (0)) * ff_v_mce_mdr_rec_resulthsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_rec_resulthsf_negative_terminal. ff_h_mce_mdr_rec_resulthsf_negative_terminal + S (mdr_n_rec_resulth) = S ((S ((S (mdr_q_rec_resulths)))) * ff_v_mce_mdr_rec_resulthsf_negative)) /\ exists ff_q_mce_mdr_rec_resulthsf_negative_terminal. ff_u_mce_mdr_rec_resulthsf_negative = ff_q_mce_mdr_rec_resulthsf_negative_terminal * S ((S ((S (mdr_q_rec_resulths)))) * ff_v_mce_mdr_rec_resulthsf_negative) + (mdr_n_rec_resulth))) /\ forall ff_i_mce_mdr_rec_resulthsf_negative. (exists ff_lt_mce_mdr_rec_resulthsf_negative_bound. ff_lt_mce_mdr_rec_resulthsf_negative_bound + S ff_i_mce_mdr_rec_resulthsf_negative = (S (mdr_q_rec_resulths))) -> exists ff_a_mce_mdr_rec_resulthsf_negative ff_r_mce_mdr_rec_resulthsf_negative ff_s_mce_mdr_rec_resulthsf_negative. ((((exists ff_h_mce_mdr_rec_resulthsf_negative_summand. ff_h_mce_mdr_rec_resulthsf_negative_summand + S (ff_a_mce_mdr_rec_resulthsf_negative) = S ((S (ff_i_mce_mdr_rec_resulthsf_negative)) * ff_vc_mce_fold_mdr_rec_resulthsf)) /\ exists ff_q_mce_mdr_rec_resulthsf_negative_summand. ff_vb_mce_fold_mdr_rec_resulthsf = ff_q_mce_mdr_rec_resulthsf_negative_summand * S ((S (ff_i_mce_mdr_rec_resulthsf_negative)) * ff_vc_mce_fold_mdr_rec_resulthsf) + (ff_a_mce_mdr_rec_resulthsf_negative))) /\ ((((exists ff_h_mce_mdr_rec_resulthsf_negative_partial. ff_h_mce_mdr_rec_resulthsf_negative_partial + S (ff_r_mce_mdr_rec_resulthsf_negative) = S ((S (ff_i_mce_mdr_rec_resulthsf_negative)) * ff_v_mce_mdr_rec_resulthsf_negative)) /\ exists ff_q_mce_mdr_rec_resulthsf_negative_partial. ff_u_mce_mdr_rec_resulthsf_negative = ff_q_mce_mdr_rec_resulthsf_negative_partial * S ((S (ff_i_mce_mdr_rec_resulthsf_negative)) * ff_v_mce_mdr_rec_resulthsf_negative) + (ff_r_mce_mdr_rec_resulthsf_negative))) /\ ((((exists ff_h_mce_mdr_rec_resulthsf_negative_successor. ff_h_mce_mdr_rec_resulthsf_negative_successor + S (ff_s_mce_mdr_rec_resulthsf_negative) = S ((S (S ff_i_mce_mdr_rec_resulthsf_negative)) * ff_v_mce_mdr_rec_resulthsf_negative)) /\ exists ff_q_mce_mdr_rec_resulthsf_negative_successor. ff_u_mce_mdr_rec_resulthsf_negative = ff_q_mce_mdr_rec_resulthsf_negative_successor * S ((S (S ff_i_mce_mdr_rec_resulthsf_negative)) * ff_v_mce_mdr_rec_resulthsf_negative) + (ff_s_mce_mdr_rec_resulthsf_negative))) /\ ff_s_mce_mdr_rec_resulthsf_negative = ff_r_mce_mdr_rec_resulthsf_negative + ff_a_mce_mdr_rec_resulthsf_negative))))))))))))))) -> exists mdr_u_rec_result mdr_v_rec_result mdr_t_rec_result mdr_p_rec_result mdr_n_rec_result. ((forall mdr_i_rec_resultrp mdr_a_rec_resultrp. (exists mdr_gap_rec_resultrpb. mdr_gap_rec_resultrpb + S (mdr_i_rec_resultrp) = (mdr_l_rec_result)) -> (((exists ff_h_mdr_rec_resultrpo. ff_h_mdr_rec_resultrpo + S (mdr_a_rec_resultrp) = S ((S (mdr_i_rec_resultrp)) * mdr_c_rec_result)) /\ exists ff_q_mdr_rec_resultrpo. mdr_b_rec_result = ff_q_mdr_rec_resultrpo * S ((S (mdr_i_rec_resultrp)) * mdr_c_rec_result) + (mdr_a_rec_resultrp))) -> (((exists ff_h_mdr_rec_resultrpn. ff_h_mdr_rec_resultrpn + S (mdr_a_rec_resultrp) = S ((S (mdr_i_rec_resultrp)) * mdr_v_rec_result)) /\ exists ff_q_mdr_rec_resultrpn. mdr_u_rec_result = ff_q_mdr_rec_resultrpn * S ((S (mdr_i_rec_resultrp)) * mdr_v_rec_result) + (mdr_a_rec_resultrp)))) /\ ((exists mdr_gap_rec_resultrl. mdr_gap_rec_resultrl + (mdr_l_rec_result) = (mdr_t_rec_result)) /\ ((forall mdr_i_rec_resultrh. (exists mdr_gap_rec_resultrhi. mdr_gap_rec_resultrhi + S (mdr_i_rec_resultrh) = (S (mdr_t_rec_result))) -> exists mdr_d_rec_resultrh mdr_pb_rec_resultrh mdr_pc_rec_resultrh mdr_nb_rec_resultrh mdr_nc_rec_resultrh mdr_p_rec_resultrh mdr_n_rec_resultrh. ((exists mdr_z_rec_resultrhr. ((exists mdr_a_rec_resultrhrc mdr_b_rec_resultrhrc mdr_c_rec_resultrhrc mdr_e_rec_resultrhrc mdr_f_rec_resultrhrc. ((mdr_a_rec_resultrhrc = ((mdr_d_rec_resultrh) + (mdr_pb_rec_resultrh)) * S ((mdr_d_rec_resultrh) + (mdr_pb_rec_resultrh)) + ((mdr_pb_rec_resultrh) + (mdr_pb_rec_resultrh))) /\ ((mdr_b_rec_resultrhrc = ((mdr_pc_rec_resultrh) + (mdr_nb_rec_resultrh)) * S ((mdr_pc_rec_resultrh) + (mdr_nb_rec_resultrh)) + ((mdr_nb_rec_resultrh) + (mdr_nb_rec_resultrh))) /\ ((mdr_c_rec_resultrhrc = ((mdr_a_rec_resultrhrc) + (mdr_b_rec_resultrhrc)) * S ((mdr_a_rec_resultrhrc) + (mdr_b_rec_resultrhrc)) + ((mdr_b_rec_resultrhrc) + (mdr_b_rec_resultrhrc))) /\ ((mdr_e_rec_resultrhrc = ((mdr_p_rec_resultrh) + (mdr_n_rec_resultrh)) * S ((mdr_p_rec_resultrh) + (mdr_n_rec_resultrh)) + ((mdr_n_rec_resultrh) + (mdr_n_rec_resultrh))) /\ ((mdr_f_rec_resultrhrc = ((mdr_nc_rec_resultrh) + (mdr_e_rec_resultrhrc)) * S ((mdr_nc_rec_resultrh) + (mdr_e_rec_resultrhrc)) + ((mdr_e_rec_resultrhrc) + (mdr_e_rec_resultrhrc))) /\ ((mdr_z_rec_resultrhr) = ((mdr_c_rec_resultrhrc) + (mdr_f_rec_resultrhrc)) * S ((mdr_c_rec_resultrhrc) + (mdr_f_rec_resultrhrc)) + ((mdr_f_rec_resultrhrc) + (mdr_f_rec_resultrhrc))))))))) /\ (((exists ff_h_mdr_rec_resultrhrb. ff_h_mdr_rec_resultrhrb + S (mdr_z_rec_resultrhr) = S ((S (mdr_i_rec_resultrh)) * mdr_v_rec_result)) /\ exists ff_q_mdr_rec_resultrhrb. mdr_u_rec_result = ff_q_mdr_rec_resultrhrb * S ((S (mdr_i_rec_resultrh)) * mdr_v_rec_result) + (mdr_z_rec_resultrhr))))) /\ (((((mdr_d_rec_resultrh) = 0) /\ (((mdr_p_rec_resultrh) = 1) /\ ((mdr_n_rec_resultrh) = 0))) \/ exists mdr_q_rec_resultrhs mdr_eb_rec_resultrhs mdr_ec_rec_resultrhs mdr_fb_rec_resultrhs mdr_fc_rec_resultrhs. (((mdr_d_rec_resultrh) = S (mdr_q_rec_resultrhs)) /\ ((forall mdr_j_rec_resultrhsc. (exists mdr_gap_rec_resultrhscj. mdr_gap_rec_resultrhscj + S (mdr_j_rec_resultrhsc) = (S (mdr_q_rec_resultrhs))) -> exists mdr_i_rec_resultrhsc mdr_up_rec_resultrhsc mdr_us_rec_resultrhsc mdr_un_rec_resultrhsc mdr_ut_rec_resultrhsc mdr_p_rec_resultrhsc mdr_n_rec_resultrhsc. ((exists mdr_gap_rec_resultrhsci. mdr_gap_rec_resultrhsci + S (mdr_i_rec_resultrhsc) = (mdr_i_rec_resultrh)) /\ ((exists mdr_z_rec_resultrhscr. ((exists mdr_a_rec_resultrhscrc mdr_b_rec_resultrhscrc mdr_c_rec_resultrhscrc mdr_e_rec_resultrhscrc mdr_f_rec_resultrhscrc. ((mdr_a_rec_resultrhscrc = ((mdr_q_rec_resultrhs) + (mdr_up_rec_resultrhsc)) * S ((mdr_q_rec_resultrhs) + (mdr_up_rec_resultrhsc)) + ((mdr_up_rec_resultrhsc) + (mdr_up_rec_resultrhsc))) /\ ((mdr_b_rec_resultrhscrc = ((mdr_us_rec_resultrhsc) + (mdr_un_rec_resultrhsc)) * S ((mdr_us_rec_resultrhsc) + (mdr_un_rec_resultrhsc)) + ((mdr_un_rec_resultrhsc) + (mdr_un_rec_resultrhsc))) /\ ((mdr_c_rec_resultrhscrc = ((mdr_a_rec_resultrhscrc) + (mdr_b_rec_resultrhscrc)) * S ((mdr_a_rec_resultrhscrc) + (mdr_b_rec_resultrhscrc)) + ((mdr_b_rec_resultrhscrc) + (mdr_b_rec_resultrhscrc))) /\ ((mdr_e_rec_resultrhscrc = ((mdr_p_rec_resultrhsc) + (mdr_n_rec_resultrhsc)) * S ((mdr_p_rec_resultrhsc) + (mdr_n_rec_resultrhsc)) + ((mdr_n_rec_resultrhsc) + (mdr_n_rec_resultrhsc))) /\ ((mdr_f_rec_resultrhscrc = ((mdr_ut_rec_resultrhsc) + (mdr_e_rec_resultrhscrc)) * S ((mdr_ut_rec_resultrhsc) + (mdr_e_rec_resultrhscrc)) + ((mdr_e_rec_resultrhscrc) + (mdr_e_rec_resultrhscrc))) /\ ((mdr_z_rec_resultrhscr) = ((mdr_c_rec_resultrhscrc) + (mdr_f_rec_resultrhscrc)) * S ((mdr_c_rec_resultrhscrc) + (mdr_f_rec_resultrhscrc)) + ((mdr_f_rec_resultrhscrc) + (mdr_f_rec_resultrhscrc))))))))) /\ (((exists ff_h_mdr_rec_resultrhscrb. ff_h_mdr_rec_resultrhscrb + S (mdr_z_rec_resultrhscr) = S ((S (mdr_i_rec_resultrhsc)) * mdr_v_rec_result)) /\ exists ff_q_mdr_rec_resultrhscrb. mdr_u_rec_result = ff_q_mdr_rec_resultrhscrb * S ((S (mdr_i_rec_resultrhsc)) * mdr_v_rec_result) + (mdr_z_rec_resultrhscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_rec_resultrhscm_positive. (exists ff_gap_mdm_lt_mdr_rec_resultrhscm_positive_index_bound. ff_gap_mdm_lt_mdr_rec_resultrhscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_rec_resultrhscm_positive) = ((mdr_q_rec_resultrhs) * (mdr_q_rec_resultrhs))) -> exists ff_row_mdm_prefix_mdr_rec_resultrhscm_positive ff_column_mdm_prefix_mdr_rec_resultrhscm_positive ff_value_mdm_prefix_mdr_rec_resultrhscm_positive. (ff_index_mdm_prefix_mdr_rec_resultrhscm_positive = (mdr_q_rec_resultrhs) * ff_row_mdm_prefix_mdr_rec_resultrhscm_positive + ff_column_mdm_prefix_mdr_rec_resultrhscm_positive /\ ((exists ff_gap_mdm_lt_mdr_rec_resultrhscm_positive_column_bound. ff_gap_mdm_lt_mdr_rec_resultrhscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_rec_resultrhscm_positive) = (mdr_q_rec_resultrhs)) /\ ((exists ff_row_mdm_cell_mdr_rec_resultrhscm_positive_cell ff_column_mdm_cell_mdr_rec_resultrhscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_rec_resultrhscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_rec_resultrhscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_rec_resultrhscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_rec_resultrhscm_positive_cell = ff_row_mdm_prefix_mdr_rec_resultrhscm_positive) \/ ((exists ff_gap_mdm_le_mdr_rec_resultrhscm_positive_cell_row_after. ff_gap_mdm_le_mdr_rec_resultrhscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_rec_resultrhscm_positive)) /\ ff_row_mdm_cell_mdr_rec_resultrhscm_positive_cell = S ff_row_mdm_prefix_mdr_rec_resultrhscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_rec_resultrhscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_rec_resultrhscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_rec_resultrhscm_positive) = (mdr_j_rec_resultrhsc)) /\ ff_column_mdm_cell_mdr_rec_resultrhscm_positive_cell = ff_column_mdm_prefix_mdr_rec_resultrhscm_positive) \/ ((exists ff_gap_mdm_le_mdr_rec_resultrhscm_positive_cell_column_after. ff_gap_mdm_le_mdr_rec_resultrhscm_positive_cell_column_after + (mdr_j_rec_resultrhsc) = (ff_column_mdm_prefix_mdr_rec_resultrhscm_positive)) /\ ff_column_mdm_cell_mdr_rec_resultrhscm_positive_cell = S ff_column_mdm_prefix_mdr_rec_resultrhscm_positive))) /\ (((exists ff_h_mdm_mdr_rec_resultrhscm_positive_cell_source. ff_h_mdm_mdr_rec_resultrhscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_rec_resultrhscm_positive) = S ((S ((ff_row_mdm_cell_mdr_rec_resultrhscm_positive_cell) * (S (mdr_q_rec_resultrhs)) + (ff_column_mdm_cell_mdr_rec_resultrhscm_positive_cell))) * mdr_pc_rec_resultrh)) /\ exists ff_q_mdm_mdr_rec_resultrhscm_positive_cell_source. mdr_pb_rec_resultrh = ff_q_mdm_mdr_rec_resultrhscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_rec_resultrhscm_positive_cell) * (S (mdr_q_rec_resultrhs)) + (ff_column_mdm_cell_mdr_rec_resultrhscm_positive_cell))) * mdr_pc_rec_resultrh) + (ff_value_mdm_prefix_mdr_rec_resultrhscm_positive)))))) /\ (((exists ff_h_mdm_mdr_rec_resultrhscm_positive_target. ff_h_mdm_mdr_rec_resultrhscm_positive_target + S (ff_value_mdm_prefix_mdr_rec_resultrhscm_positive) = S ((S (ff_index_mdm_prefix_mdr_rec_resultrhscm_positive)) * mdr_us_rec_resultrhsc)) /\ exists ff_q_mdm_mdr_rec_resultrhscm_positive_target. mdr_up_rec_resultrhsc = ff_q_mdm_mdr_rec_resultrhscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_rec_resultrhscm_positive)) * mdr_us_rec_resultrhsc) + (ff_value_mdm_prefix_mdr_rec_resultrhscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_rec_resultrhscm_negative. (exists ff_gap_mdm_lt_mdr_rec_resultrhscm_negative_index_bound. ff_gap_mdm_lt_mdr_rec_resultrhscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_rec_resultrhscm_negative) = ((mdr_q_rec_resultrhs) * (mdr_q_rec_resultrhs))) -> exists ff_row_mdm_prefix_mdr_rec_resultrhscm_negative ff_column_mdm_prefix_mdr_rec_resultrhscm_negative ff_value_mdm_prefix_mdr_rec_resultrhscm_negative. (ff_index_mdm_prefix_mdr_rec_resultrhscm_negative = (mdr_q_rec_resultrhs) * ff_row_mdm_prefix_mdr_rec_resultrhscm_negative + ff_column_mdm_prefix_mdr_rec_resultrhscm_negative /\ ((exists ff_gap_mdm_lt_mdr_rec_resultrhscm_negative_column_bound. ff_gap_mdm_lt_mdr_rec_resultrhscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_rec_resultrhscm_negative) = (mdr_q_rec_resultrhs)) /\ ((exists ff_row_mdm_cell_mdr_rec_resultrhscm_negative_cell ff_column_mdm_cell_mdr_rec_resultrhscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_rec_resultrhscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_rec_resultrhscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_rec_resultrhscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_rec_resultrhscm_negative_cell = ff_row_mdm_prefix_mdr_rec_resultrhscm_negative) \/ ((exists ff_gap_mdm_le_mdr_rec_resultrhscm_negative_cell_row_after. ff_gap_mdm_le_mdr_rec_resultrhscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_rec_resultrhscm_negative)) /\ ff_row_mdm_cell_mdr_rec_resultrhscm_negative_cell = S ff_row_mdm_prefix_mdr_rec_resultrhscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_rec_resultrhscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_rec_resultrhscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_rec_resultrhscm_negative) = (mdr_j_rec_resultrhsc)) /\ ff_column_mdm_cell_mdr_rec_resultrhscm_negative_cell = ff_column_mdm_prefix_mdr_rec_resultrhscm_negative) \/ ((exists ff_gap_mdm_le_mdr_rec_resultrhscm_negative_cell_column_after. ff_gap_mdm_le_mdr_rec_resultrhscm_negative_cell_column_after + (mdr_j_rec_resultrhsc) = (ff_column_mdm_prefix_mdr_rec_resultrhscm_negative)) /\ ff_column_mdm_cell_mdr_rec_resultrhscm_negative_cell = S ff_column_mdm_prefix_mdr_rec_resultrhscm_negative))) /\ (((exists ff_h_mdm_mdr_rec_resultrhscm_negative_cell_source. ff_h_mdm_mdr_rec_resultrhscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_rec_resultrhscm_negative) = S ((S ((ff_row_mdm_cell_mdr_rec_resultrhscm_negative_cell) * (S (mdr_q_rec_resultrhs)) + (ff_column_mdm_cell_mdr_rec_resultrhscm_negative_cell))) * mdr_nc_rec_resultrh)) /\ exists ff_q_mdm_mdr_rec_resultrhscm_negative_cell_source. mdr_nb_rec_resultrh = ff_q_mdm_mdr_rec_resultrhscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_rec_resultrhscm_negative_cell) * (S (mdr_q_rec_resultrhs)) + (ff_column_mdm_cell_mdr_rec_resultrhscm_negative_cell))) * mdr_nc_rec_resultrh) + (ff_value_mdm_prefix_mdr_rec_resultrhscm_negative)))))) /\ (((exists ff_h_mdm_mdr_rec_resultrhscm_negative_target. ff_h_mdm_mdr_rec_resultrhscm_negative_target + S (ff_value_mdm_prefix_mdr_rec_resultrhscm_negative) = S ((S (ff_index_mdm_prefix_mdr_rec_resultrhscm_negative)) * mdr_ut_rec_resultrhsc)) /\ exists ff_q_mdm_mdr_rec_resultrhscm_negative_target. mdr_un_rec_resultrhsc = ff_q_mdm_mdr_rec_resultrhscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_rec_resultrhscm_negative)) * mdr_ut_rec_resultrhsc) + (ff_value_mdm_prefix_mdr_rec_resultrhscm_negative))))))))) /\ ((((exists ff_h_mdr_rec_resultrhscp. ff_h_mdr_rec_resultrhscp + S (mdr_p_rec_resultrhsc) = S ((S (mdr_j_rec_resultrhsc)) * mdr_ec_rec_resultrhs)) /\ exists ff_q_mdr_rec_resultrhscp. mdr_eb_rec_resultrhs = ff_q_mdr_rec_resultrhscp * S ((S (mdr_j_rec_resultrhsc)) * mdr_ec_rec_resultrhs) + (mdr_p_rec_resultrhsc))) /\ (((exists ff_h_mdr_rec_resultrhscn. ff_h_mdr_rec_resultrhscn + S (mdr_n_rec_resultrhsc) = S ((S (mdr_j_rec_resultrhsc)) * mdr_fc_rec_resultrhs)) /\ exists ff_q_mdr_rec_resultrhscn. mdr_fb_rec_resultrhs = ff_q_mdr_rec_resultrhscn * S ((S (mdr_j_rec_resultrhsc)) * mdr_fc_rec_resultrhs) + (mdr_n_rec_resultrhsc)))))))) /\ (exists ff_ub_mce_fold_mdr_rec_resultrhsf ff_uc_mce_fold_mdr_rec_resultrhsf ff_vb_mce_fold_mdr_rec_resultrhsf ff_vc_mce_fold_mdr_rec_resultrhsf. ((forall ff_index_mce_alternating_mdr_rec_resultrhsf_prefix. (exists ff_gap_mce_mdr_rec_resultrhsf_prefix_index. ff_gap_mce_mdr_rec_resultrhsf_prefix_index + S (ff_index_mce_alternating_mdr_rec_resultrhsf_prefix) = (S (mdr_q_rec_resultrhs))) -> exists ff_ap_mce_alternating_mdr_rec_resultrhsf_prefix ff_an_mce_alternating_mdr_rec_resultrhsf_prefix ff_bp_mce_alternating_mdr_rec_resultrhsf_prefix ff_bn_mce_alternating_mdr_rec_resultrhsf_prefix ff_p_mce_alternating_mdr_rec_resultrhsf_prefix ff_n_mce_alternating_mdr_rec_resultrhsf_prefix. ((((exists ff_h_mce_mdr_rec_resultrhsf_prefix_ap. ff_h_mce_mdr_rec_resultrhsf_prefix_ap + S (ff_ap_mce_alternating_mdr_rec_resultrhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_rec_resultrhsf_prefix)) * mdr_pc_rec_resultrh)) /\ exists ff_q_mce_mdr_rec_resultrhsf_prefix_ap. mdr_pb_rec_resultrh = ff_q_mce_mdr_rec_resultrhsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_rec_resultrhsf_prefix)) * mdr_pc_rec_resultrh) + (ff_ap_mce_alternating_mdr_rec_resultrhsf_prefix))) /\ ((((exists ff_h_mce_mdr_rec_resultrhsf_prefix_an. ff_h_mce_mdr_rec_resultrhsf_prefix_an + S (ff_an_mce_alternating_mdr_rec_resultrhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_rec_resultrhsf_prefix)) * mdr_nc_rec_resultrh)) /\ exists ff_q_mce_mdr_rec_resultrhsf_prefix_an. mdr_nb_rec_resultrh = ff_q_mce_mdr_rec_resultrhsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_rec_resultrhsf_prefix)) * mdr_nc_rec_resultrh) + (ff_an_mce_alternating_mdr_rec_resultrhsf_prefix))) /\ ((((exists ff_h_mce_mdr_rec_resultrhsf_prefix_bp. ff_h_mce_mdr_rec_resultrhsf_prefix_bp + S (ff_bp_mce_alternating_mdr_rec_resultrhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_rec_resultrhsf_prefix)) * mdr_ec_rec_resultrhs)) /\ exists ff_q_mce_mdr_rec_resultrhsf_prefix_bp. mdr_eb_rec_resultrhs = ff_q_mce_mdr_rec_resultrhsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_rec_resultrhsf_prefix)) * mdr_ec_rec_resultrhs) + (ff_bp_mce_alternating_mdr_rec_resultrhsf_prefix))) /\ ((((exists ff_h_mce_mdr_rec_resultrhsf_prefix_bn. ff_h_mce_mdr_rec_resultrhsf_prefix_bn + S (ff_bn_mce_alternating_mdr_rec_resultrhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_rec_resultrhsf_prefix)) * mdr_fc_rec_resultrhs)) /\ exists ff_q_mce_mdr_rec_resultrhsf_prefix_bn. mdr_fb_rec_resultrhs = ff_q_mce_mdr_rec_resultrhsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_rec_resultrhsf_prefix)) * mdr_fc_rec_resultrhs) + (ff_bn_mce_alternating_mdr_rec_resultrhsf_prefix))) /\ ((((exists ff_h_mce_mdr_rec_resultrhsf_prefix_positive. ff_h_mce_mdr_rec_resultrhsf_prefix_positive + S (ff_p_mce_alternating_mdr_rec_resultrhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_rec_resultrhsf_prefix)) * ff_uc_mce_fold_mdr_rec_resultrhsf)) /\ exists ff_q_mce_mdr_rec_resultrhsf_prefix_positive. ff_ub_mce_fold_mdr_rec_resultrhsf = ff_q_mce_mdr_rec_resultrhsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_rec_resultrhsf_prefix)) * ff_uc_mce_fold_mdr_rec_resultrhsf) + (ff_p_mce_alternating_mdr_rec_resultrhsf_prefix))) /\ ((((exists ff_h_mce_mdr_rec_resultrhsf_prefix_negative. ff_h_mce_mdr_rec_resultrhsf_prefix_negative + S (ff_n_mce_alternating_mdr_rec_resultrhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_rec_resultrhsf_prefix)) * ff_vc_mce_fold_mdr_rec_resultrhsf)) /\ exists ff_q_mce_mdr_rec_resultrhsf_prefix_negative. ff_vb_mce_fold_mdr_rec_resultrhsf = ff_q_mce_mdr_rec_resultrhsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_rec_resultrhsf_prefix)) * ff_vc_mce_fold_mdr_rec_resultrhsf) + (ff_n_mce_alternating_mdr_rec_resultrhsf_prefix))) /\ (((exists ff_even_mce_term_mdr_rec_resultrhsf_prefix_term. ff_index_mce_alternating_mdr_rec_resultrhsf_prefix = 2 * ff_even_mce_term_mdr_rec_resultrhsf_prefix_term) /\ (ff_p_mce_alternating_mdr_rec_resultrhsf_prefix = (ff_ap_mce_alternating_mdr_rec_resultrhsf_prefix) * (ff_bp_mce_alternating_mdr_rec_resultrhsf_prefix) + (ff_an_mce_alternating_mdr_rec_resultrhsf_prefix) * (ff_bn_mce_alternating_mdr_rec_resultrhsf_prefix) /\ ff_n_mce_alternating_mdr_rec_resultrhsf_prefix = (ff_ap_mce_alternating_mdr_rec_resultrhsf_prefix) * (ff_bn_mce_alternating_mdr_rec_resultrhsf_prefix) + (ff_an_mce_alternating_mdr_rec_resultrhsf_prefix) * (ff_bp_mce_alternating_mdr_rec_resultrhsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_rec_resultrhsf_prefix_term. ff_index_mce_alternating_mdr_rec_resultrhsf_prefix = 2 * ff_odd_mce_term_mdr_rec_resultrhsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_rec_resultrhsf_prefix = (ff_ap_mce_alternating_mdr_rec_resultrhsf_prefix) * (ff_bn_mce_alternating_mdr_rec_resultrhsf_prefix) + (ff_an_mce_alternating_mdr_rec_resultrhsf_prefix) * (ff_bp_mce_alternating_mdr_rec_resultrhsf_prefix) /\ ff_n_mce_alternating_mdr_rec_resultrhsf_prefix = (ff_ap_mce_alternating_mdr_rec_resultrhsf_prefix) * (ff_bp_mce_alternating_mdr_rec_resultrhsf_prefix) + (ff_an_mce_alternating_mdr_rec_resultrhsf_prefix) * (ff_bn_mce_alternating_mdr_rec_resultrhsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_rec_resultrhsf_positive ff_v_mce_mdr_rec_resultrhsf_positive. ((((exists ff_h_mce_mdr_rec_resultrhsf_positive_start. ff_h_mce_mdr_rec_resultrhsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_rec_resultrhsf_positive)) /\ exists ff_q_mce_mdr_rec_resultrhsf_positive_start. ff_u_mce_mdr_rec_resultrhsf_positive = ff_q_mce_mdr_rec_resultrhsf_positive_start * S ((S (0)) * ff_v_mce_mdr_rec_resultrhsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_rec_resultrhsf_positive_terminal. ff_h_mce_mdr_rec_resultrhsf_positive_terminal + S (mdr_p_rec_resultrh) = S ((S ((S (mdr_q_rec_resultrhs)))) * ff_v_mce_mdr_rec_resultrhsf_positive)) /\ exists ff_q_mce_mdr_rec_resultrhsf_positive_terminal. ff_u_mce_mdr_rec_resultrhsf_positive = ff_q_mce_mdr_rec_resultrhsf_positive_terminal * S ((S ((S (mdr_q_rec_resultrhs)))) * ff_v_mce_mdr_rec_resultrhsf_positive) + (mdr_p_rec_resultrh))) /\ forall ff_i_mce_mdr_rec_resultrhsf_positive. (exists ff_lt_mce_mdr_rec_resultrhsf_positive_bound. ff_lt_mce_mdr_rec_resultrhsf_positive_bound + S ff_i_mce_mdr_rec_resultrhsf_positive = (S (mdr_q_rec_resultrhs))) -> exists ff_a_mce_mdr_rec_resultrhsf_positive ff_r_mce_mdr_rec_resultrhsf_positive ff_s_mce_mdr_rec_resultrhsf_positive. ((((exists ff_h_mce_mdr_rec_resultrhsf_positive_summand. ff_h_mce_mdr_rec_resultrhsf_positive_summand + S (ff_a_mce_mdr_rec_resultrhsf_positive) = S ((S (ff_i_mce_mdr_rec_resultrhsf_positive)) * ff_uc_mce_fold_mdr_rec_resultrhsf)) /\ exists ff_q_mce_mdr_rec_resultrhsf_positive_summand. ff_ub_mce_fold_mdr_rec_resultrhsf = ff_q_mce_mdr_rec_resultrhsf_positive_summand * S ((S (ff_i_mce_mdr_rec_resultrhsf_positive)) * ff_uc_mce_fold_mdr_rec_resultrhsf) + (ff_a_mce_mdr_rec_resultrhsf_positive))) /\ ((((exists ff_h_mce_mdr_rec_resultrhsf_positive_partial. ff_h_mce_mdr_rec_resultrhsf_positive_partial + S (ff_r_mce_mdr_rec_resultrhsf_positive) = S ((S (ff_i_mce_mdr_rec_resultrhsf_positive)) * ff_v_mce_mdr_rec_resultrhsf_positive)) /\ exists ff_q_mce_mdr_rec_resultrhsf_positive_partial. ff_u_mce_mdr_rec_resultrhsf_positive = ff_q_mce_mdr_rec_resultrhsf_positive_partial * S ((S (ff_i_mce_mdr_rec_resultrhsf_positive)) * ff_v_mce_mdr_rec_resultrhsf_positive) + (ff_r_mce_mdr_rec_resultrhsf_positive))) /\ ((((exists ff_h_mce_mdr_rec_resultrhsf_positive_successor. ff_h_mce_mdr_rec_resultrhsf_positive_successor + S (ff_s_mce_mdr_rec_resultrhsf_positive) = S ((S (S ff_i_mce_mdr_rec_resultrhsf_positive)) * ff_v_mce_mdr_rec_resultrhsf_positive)) /\ exists ff_q_mce_mdr_rec_resultrhsf_positive_successor. ff_u_mce_mdr_rec_resultrhsf_positive = ff_q_mce_mdr_rec_resultrhsf_positive_successor * S ((S (S ff_i_mce_mdr_rec_resultrhsf_positive)) * ff_v_mce_mdr_rec_resultrhsf_positive) + (ff_s_mce_mdr_rec_resultrhsf_positive))) /\ ff_s_mce_mdr_rec_resultrhsf_positive = ff_r_mce_mdr_rec_resultrhsf_positive + ff_a_mce_mdr_rec_resultrhsf_positive)))))) /\ (exists ff_u_mce_mdr_rec_resultrhsf_negative ff_v_mce_mdr_rec_resultrhsf_negative. ((((exists ff_h_mce_mdr_rec_resultrhsf_negative_start. ff_h_mce_mdr_rec_resultrhsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_rec_resultrhsf_negative)) /\ exists ff_q_mce_mdr_rec_resultrhsf_negative_start. ff_u_mce_mdr_rec_resultrhsf_negative = ff_q_mce_mdr_rec_resultrhsf_negative_start * S ((S (0)) * ff_v_mce_mdr_rec_resultrhsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_rec_resultrhsf_negative_terminal. ff_h_mce_mdr_rec_resultrhsf_negative_terminal + S (mdr_n_rec_resultrh) = S ((S ((S (mdr_q_rec_resultrhs)))) * ff_v_mce_mdr_rec_resultrhsf_negative)) /\ exists ff_q_mce_mdr_rec_resultrhsf_negative_terminal. ff_u_mce_mdr_rec_resultrhsf_negative = ff_q_mce_mdr_rec_resultrhsf_negative_terminal * S ((S ((S (mdr_q_rec_resultrhs)))) * ff_v_mce_mdr_rec_resultrhsf_negative) + (mdr_n_rec_resultrh))) /\ forall ff_i_mce_mdr_rec_resultrhsf_negative. (exists ff_lt_mce_mdr_rec_resultrhsf_negative_bound. ff_lt_mce_mdr_rec_resultrhsf_negative_bound + S ff_i_mce_mdr_rec_resultrhsf_negative = (S (mdr_q_rec_resultrhs))) -> exists ff_a_mce_mdr_rec_resultrhsf_negative ff_r_mce_mdr_rec_resultrhsf_negative ff_s_mce_mdr_rec_resultrhsf_negative. ((((exists ff_h_mce_mdr_rec_resultrhsf_negative_summand. ff_h_mce_mdr_rec_resultrhsf_negative_summand + S (ff_a_mce_mdr_rec_resultrhsf_negative) = S ((S (ff_i_mce_mdr_rec_resultrhsf_negative)) * ff_vc_mce_fold_mdr_rec_resultrhsf)) /\ exists ff_q_mce_mdr_rec_resultrhsf_negative_summand. ff_vb_mce_fold_mdr_rec_resultrhsf = ff_q_mce_mdr_rec_resultrhsf_negative_summand * S ((S (ff_i_mce_mdr_rec_resultrhsf_negative)) * ff_vc_mce_fold_mdr_rec_resultrhsf) + (ff_a_mce_mdr_rec_resultrhsf_negative))) /\ ((((exists ff_h_mce_mdr_rec_resultrhsf_negative_partial. ff_h_mce_mdr_rec_resultrhsf_negative_partial + S (ff_r_mce_mdr_rec_resultrhsf_negative) = S ((S (ff_i_mce_mdr_rec_resultrhsf_negative)) * ff_v_mce_mdr_rec_resultrhsf_negative)) /\ exists ff_q_mce_mdr_rec_resultrhsf_negative_partial. ff_u_mce_mdr_rec_resultrhsf_negative = ff_q_mce_mdr_rec_resultrhsf_negative_partial * S ((S (ff_i_mce_mdr_rec_resultrhsf_negative)) * ff_v_mce_mdr_rec_resultrhsf_negative) + (ff_r_mce_mdr_rec_resultrhsf_negative))) /\ ((((exists ff_h_mce_mdr_rec_resultrhsf_negative_successor. ff_h_mce_mdr_rec_resultrhsf_negative_successor + S (ff_s_mce_mdr_rec_resultrhsf_negative) = S ((S (S ff_i_mce_mdr_rec_resultrhsf_negative)) * ff_v_mce_mdr_rec_resultrhsf_negative)) /\ exists ff_q_mce_mdr_rec_resultrhsf_negative_successor. ff_u_mce_mdr_rec_resultrhsf_negative = ff_q_mce_mdr_rec_resultrhsf_negative_successor * S ((S (S ff_i_mce_mdr_rec_resultrhsf_negative)) * ff_v_mce_mdr_rec_resultrhsf_negative) + (ff_s_mce_mdr_rec_resultrhsf_negative))) /\ ff_s_mce_mdr_rec_resultrhsf_negative = ff_r_mce_mdr_rec_resultrhsf_negative + ff_a_mce_mdr_rec_resultrhsf_negative))))))))))))))) /\ (exists mdr_z_rec_resultrr. ((exists mdr_a_rec_resultrrc mdr_b_rec_resultrrc mdr_c_rec_resultrrc mdr_e_rec_resultrrc mdr_f_rec_resultrrc. ((mdr_a_rec_resultrrc = ((S q) + (mdr_pb_rec_result)) * S ((S q) + (mdr_pb_rec_result)) + ((mdr_pb_rec_result) + (mdr_pb_rec_result))) /\ ((mdr_b_rec_resultrrc = ((mdr_pc_rec_result) + (mdr_nb_rec_result)) * S ((mdr_pc_rec_result) + (mdr_nb_rec_result)) + ((mdr_nb_rec_result) + (mdr_nb_rec_result))) /\ ((mdr_c_rec_resultrrc = ((mdr_a_rec_resultrrc) + (mdr_b_rec_resultrrc)) * S ((mdr_a_rec_resultrrc) + (mdr_b_rec_resultrrc)) + ((mdr_b_rec_resultrrc) + (mdr_b_rec_resultrrc))) /\ ((mdr_e_rec_resultrrc = ((mdr_p_rec_result) + (mdr_n_rec_result)) * S ((mdr_p_rec_result) + (mdr_n_rec_result)) + ((mdr_n_rec_result) + (mdr_n_rec_result))) /\ ((mdr_f_rec_resultrrc = ((mdr_nc_rec_result) + (mdr_e_rec_resultrrc)) * S ((mdr_nc_rec_result) + (mdr_e_rec_resultrrc)) + ((mdr_e_rec_resultrrc) + (mdr_e_rec_resultrrc))) /\ ((mdr_z_rec_resultrr) = ((mdr_c_rec_resultrrc) + (mdr_f_rec_resultrrc)) * S ((mdr_c_rec_resultrrc) + (mdr_f_rec_resultrrc)) + ((mdr_f_rec_resultrrc) + (mdr_f_rec_resultrrc))))))))) /\ (((exists ff_h_mdr_rec_resultrrb. ff_h_mdr_rec_resultrrb + S (mdr_z_rec_resultrr) = S ((S (mdr_t_rec_result)) * mdr_v_rec_result)) /\ exists ff_q_mdr_rec_resultrrb. mdr_u_rec_result = ff_q_mdr_rec_resultrrb * S ((S (mdr_t_rec_result)) * mdr_v_rec_result) + (mdr_z_rec_resultrr)))))))))Complete tactic proof in conservative notation
All 104 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.
Read the argument
Proof checkpoints
104 script commands · 24 reading checkpoints · 3 local claims
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.
Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.
Named ingredients (4)
01Fix variables and assumptionsL1–10
02Establish hfamilyL11–20
Establish this local claim before using it. It is not an additional assumption.
- L11
have hfamily : ∃ u. ∃ v. ∃ m. ∃ eb. ∃ ec. ∃ fb. ∃ fc. (∀ x. ∀ y. Lt(x,l) → BetaAt(b,c,x,y) → BetaAt(u,v,x,y)) ∧ (Le(l,m) ∧ (SignedDeterminantHistory(u,v,m) ∧ SignedDeterminantChildPrefix(u,v,m,pb,pc,nb,nc,q,eb,ec,fb,fc,S q)))Definitions: Lt(x,l)BetaAt(b,c,x,y)BetaAt(u,v,x,y)Le(l,m)SignedDeterminantHistory(u,v,m)SignedDeterminantChildPrefix(u,v,m,pb,pc,nb,nc,q,eb,ec,fb,fc,S q)Original native command in the exact edition - L12
specialize matrix_recursive_cofactor_prefix_from_recursion (q) - L13
specialize matrix_recursive_cofactor_prefix_from_recursion (pb) - L14
specialize matrix_recursive_cofactor_prefix_from_recursion (pc) - L15
specialize matrix_recursive_cofactor_prefix_from_recursion (nb) - L16
specialize matrix_recursive_cofactor_prefix_from_recursion (nc) - L17
specialize matrix_recursive_cofactor_prefix_from_recursion (b) - L18
specialize matrix_recursive_cofactor_prefix_from_recursion (c) - L19
specialize matrix_recursive_cofactor_prefix_from_recursion (l) - L20
specialize matrix_recursive_cofactor_prefix_from_recursion (S q)
03Use earlier factsL21–24
04Separate the logical casesL25–34
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L25
cases hfamily - L26
cases hfamily_witness - L27
cases hfamily_witness_witness - L28
cases hfamily_witness_witness_witness - L29
cases hfamily_witness_witness_witness_witness - L30
cases hfamily_witness_witness_witness_witness_witness - L31
cases hfamily_witness_witness_witness_witness_witness_witness - L32
cases hfamily_witness_witness_witness_witness_witness_witness_witness - L33
cases hfamily_witness_witness_witness_witness_witness_witness_witness_right - L34
cases hfamily_witness_witness_witness_witness_witness_witness_witness_right_right
05Establish hfoldL35–44
Establish this local claim before using it. It is not an additional assumption.
- L35
have hfold : ∃ p. ∃ n. SignedAlternatingCofactorFold(pb,pc,nb,nc,x3,x4,x5,x6,S q,p,n)Definitions: SignedAlternatingCofactorFold(pb,pc,nb,nc,x3,x4,x5,x6,S q,p,n)Original native command in the exact edition - L36
specialize signed_alternating_cofactor_fold_exists (pb) - L37
specialize signed_alternating_cofactor_fold_exists (pc) - L38
specialize signed_alternating_cofactor_fold_exists (nb) - L39
specialize signed_alternating_cofactor_fold_exists (nc) - L40
specialize signed_alternating_cofactor_fold_exists (x3) - L41
specialize signed_alternating_cofactor_fold_exists (x4) - L42
specialize signed_alternating_cofactor_fold_exists (x5) - L43
specialize signed_alternating_cofactor_fold_exists (x6) - L44
specialize signed_alternating_cofactor_fold_exists (S q)
06Use earlier factsL45–45
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L45
apply signed_alternating_cofactor_fold_exists
07Separate the logical casesL46–47
08Establish hextL48–57
Establish this local claim before using it. It is not an additional assumption.
- L48
have hext : ∃ u. ∃ v. (∀ y. ∀ z. Lt(y,x2) → BetaAt(x,x1,y,z) → BetaAt(u,v,y,z)) ∧ (SignedDeterminantHistory(u,v,S x2) ∧ SignedDeterminantNodeAt(u,v,x2,S q,pb,pc,nb,nc,x7,x8))Definitions: Lt(y,x2)BetaAt(x,x1,y,z)BetaAt(u,v,y,z)SignedDeterminantHistory(u,v,S x2)SignedDeterminantNodeAt(u,v,x2,S q,pb,pc,nb,nc,x7,x8)Original native command in the exact edition - L49
specialize matrix_recursive_history_extend (x) - L50
specialize matrix_recursive_history_extend (x1) - L51
specialize matrix_recursive_history_extend (x2) - L52
specialize matrix_recursive_history_extend (S q) - L53
specialize matrix_recursive_history_extend (pb) - L54
specialize matrix_recursive_history_extend (pc) - L55
specialize matrix_recursive_history_extend (nb) - L56
specialize matrix_recursive_history_extend (nc) - L57
specialize matrix_recursive_history_extend (x7)
09Use earlier factsL58–60
10Separate the logical casesL61–61
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L61
right
11Construct an explicit witnessL62–66
12Separate the logical casesL67–67
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L67
split
13Calculate and transport equalitiesL68–68
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L68
refl
14Separate the logical casesL69–69
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L69
split
15Use earlier factsL70–71
16Separate the logical casesL72–75
17Construct an explicit witnessL76–80
18Separate the logical casesL81–81
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L81
split
19Use earlier factsL82–91
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L82
specialize matrix_recursive_prefix_trans (b) - L83
specialize matrix_recursive_prefix_trans (c) - L84
specialize matrix_recursive_prefix_trans (x) - L85
specialize matrix_recursive_prefix_trans (x1) - L86
specialize matrix_recursive_prefix_trans (x9) - L87
specialize matrix_recursive_prefix_trans (x10) - L88
specialize matrix_recursive_prefix_trans (l) - L89
apply matrix_recursive_prefix_trans - L90
exact hfamily_witness_witness_witness_witness_witness_witness_witness_left - L91
specialize matrix_recursive_prefix_restrict (x)
20Use earlier factsL92–99
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L92
specialize matrix_recursive_prefix_restrict (x1) - L93
specialize matrix_recursive_prefix_restrict (x9) - L94
specialize matrix_recursive_prefix_restrict (x10) - L95
specialize matrix_recursive_prefix_restrict (x2) - L96
specialize matrix_recursive_prefix_restrict (l) - L97
apply matrix_recursive_prefix_restrict - L98
exact hfamily_witness_witness_witness_witness_witness_witness_witness_right_left - L99
exact hext_witness_witness_left
21Separate the logical casesL100–100
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L100
split
22Use earlier factsL101–101
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L101
exact hfamily_witness_witness_witness_witness_witness_witness_witness_right_left
23Separate the logical casesL102–102
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L102
split
Original defined command ledger · 104 lines
- 0001
intro q - 0002
intro hrecursion - 0003
intro pb - 0004
intro pc - 0005
intro nb - 0006
intro nc - 0007
intro b - 0008
intro c - 0009
intro l - 0010
intro hhistory - 0011
have hfamily : ∃ u. ∃ v. ∃ m. ∃ eb. ∃ ec. ∃ fb. ∃ fc. (∀ x. ∀ y. Lt(x,l) → BetaAt(b,c,x,y) → BetaAt(u,v,x,y)) ∧ (Le(l,m) ∧ (SignedDeterminantHistory(u,v,m) ∧ SignedDeterminantChildPrefix(u,v,m,pb,pc,nb,nc,q,eb,ec,fb,fc,S q))) - 0012
specialize matrix_recursive_cofactor_prefix_from_recursion (q) - 0013
specialize matrix_recursive_cofactor_prefix_from_recursion (pb) - 0014
specialize matrix_recursive_cofactor_prefix_from_recursion (pc) - 0015
specialize matrix_recursive_cofactor_prefix_from_recursion (nb) - 0016
specialize matrix_recursive_cofactor_prefix_from_recursion (nc) - 0017
specialize matrix_recursive_cofactor_prefix_from_recursion (b) - 0018
specialize matrix_recursive_cofactor_prefix_from_recursion (c) - 0019
specialize matrix_recursive_cofactor_prefix_from_recursion (l) - 0020
specialize matrix_recursive_cofactor_prefix_from_recursion (S q) - 0021
apply matrix_recursive_cofactor_prefix_from_recursion - 0022
exact hrecursion - 0023
apply le_refl - 0024
exact hhistory - 0025
cases hfamily - 0026
cases hfamily_witness - 0027
cases hfamily_witness_witness - 0028
cases hfamily_witness_witness_witness - 0029
cases hfamily_witness_witness_witness_witness - 0030
cases hfamily_witness_witness_witness_witness_witness - 0031
cases hfamily_witness_witness_witness_witness_witness_witness - 0032
cases hfamily_witness_witness_witness_witness_witness_witness_witness - 0033
cases hfamily_witness_witness_witness_witness_witness_witness_witness_right - 0034
cases hfamily_witness_witness_witness_witness_witness_witness_witness_right_right - 0035
have hfold : ∃ p. ∃ n. SignedAlternatingCofactorFold(pb,pc,nb,nc,x3,x4,x5,x6,S q,p,n) - 0036
specialize signed_alternating_cofactor_fold_exists (pb) - 0037
specialize signed_alternating_cofactor_fold_exists (pc) - 0038
specialize signed_alternating_cofactor_fold_exists (nb) - 0039
specialize signed_alternating_cofactor_fold_exists (nc) - 0040
specialize signed_alternating_cofactor_fold_exists (x3) - 0041
specialize signed_alternating_cofactor_fold_exists (x4) - 0042
specialize signed_alternating_cofactor_fold_exists (x5) - 0043
specialize signed_alternating_cofactor_fold_exists (x6) - 0044
specialize signed_alternating_cofactor_fold_exists (S q) - 0045
apply signed_alternating_cofactor_fold_exists - 0046
cases hfold - 0047
cases hfold_witness - 0048
have hext : ∃ u. ∃ v. (∀ y. ∀ z. Lt(y,x2) → BetaAt(x,x1,y,z) → BetaAt(u,v,y,z)) ∧ (SignedDeterminantHistory(u,v,S x2) ∧ SignedDeterminantNodeAt(u,v,x2,S q,pb,pc,nb,nc,x7,x8)) - 0049
specialize matrix_recursive_history_extend (x) - 0050
specialize matrix_recursive_history_extend (x1) - 0051
specialize matrix_recursive_history_extend (x2) - 0052
specialize matrix_recursive_history_extend (S q) - 0053
specialize matrix_recursive_history_extend (pb) - 0054
specialize matrix_recursive_history_extend (pc) - 0055
specialize matrix_recursive_history_extend (nb) - 0056
specialize matrix_recursive_history_extend (nc) - 0057
specialize matrix_recursive_history_extend (x7) - 0058
specialize matrix_recursive_history_extend (x8) - 0059
apply matrix_recursive_history_extend - 0060
exact hfamily_witness_witness_witness_witness_witness_witness_witness_right_right_left - 0061
right - 0062
exists q - 0063
exists x3 - 0064
exists x4 - 0065
exists x5 - 0066
exists x6 - 0067
split - 0068
refl - 0069
split - 0070
exact hfamily_witness_witness_witness_witness_witness_witness_witness_right_right_right - 0071
exact hfold_witness_witness - 0072
cases hext - 0073
cases hext_witness - 0074
cases hext_witness_witness - 0075
cases hext_witness_witness_right - 0076
exists x9 - 0077
exists x10 - 0078
exists x2 - 0079
exists x7 - 0080
exists x8 - 0081
split - 0082
specialize matrix_recursive_prefix_trans (b) - 0083
specialize matrix_recursive_prefix_trans (c) - 0084
specialize matrix_recursive_prefix_trans (x) - 0085
specialize matrix_recursive_prefix_trans (x1) - 0086
specialize matrix_recursive_prefix_trans (x9) - 0087
specialize matrix_recursive_prefix_trans (x10) - 0088
specialize matrix_recursive_prefix_trans (l) - 0089
apply matrix_recursive_prefix_trans - 0090
exact hfamily_witness_witness_witness_witness_witness_witness_witness_left - 0091
specialize matrix_recursive_prefix_restrict (x) - 0092
specialize matrix_recursive_prefix_restrict (x1) - 0093
specialize matrix_recursive_prefix_restrict (x9) - 0094
specialize matrix_recursive_prefix_restrict (x10) - 0095
specialize matrix_recursive_prefix_restrict (x2) - 0096
specialize matrix_recursive_prefix_restrict (l) - 0097
apply matrix_recursive_prefix_restrict - 0098
exact hfamily_witness_witness_witness_witness_witness_witness_witness_right_left - 0099
exact hext_witness_witness_left - 0100
split - 0101
exact hfamily_witness_witness_witness_witness_witness_witness_witness_right_left - 0102
split - 0103
exact hext_witness_witness_right_left - 0104
exact hext_witness_witness_right_right