DL0092 — matrix_integer_cofactor_streams_from_recursion

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

∀ ab. ∀ ac. ∀ bb. ∀ bc. ∀ eb. ∀ ec. ∀ fb. ∀ fc. ∀ cb. ∀ cc. ∀ db. ∀ dc. ∀ gb. ∀ gc. ∀ hb. ∀ hc. ∀ q. (∀ x. ∀ y. ∀ z. ∀ n. ∀ m. ∀ k. ∀ i. ∀ j. ∀ u. ∀ v. ∀ w. ∀ x0. IntegerMatrixEntrywiseEqual(x,y,z,n,m,k,i,j,q,q) → SignedRecursiveDeterminant(x,y,z,n,q,u,v) → SignedRecursiveDeterminant(m,k,i,j,q,w,x0) → u + x0 = w + v) → IntegerMatrixEntrywiseEqual(ab,ac,bb,bc,eb,ec,fb,fc,S q,S q) → SignedEvaluatedCofactors(ab,ac,bb,bc,q,cb,cc,db,dc) → SignedEvaluatedCofactors(eb,ec,fb,fc,q,gb,gc,hb,hc) → IntegerVectorEqual(cb,cc,db,dc,gb,gc,hb,hc,S q)

Every linked abbreviation expands hygienically to the identical original native formula.

Definition DAG

SignedMatrixMinor(pb,pc,nb,nc,w,r,d,q,up,us,un,ut) · 2 SignedRecursiveDeterminant(pb,pc,nb,nc,d,p,n) · 4 SignedEvaluatedCofactors(pb,pc,nb,nc,q,eb,ec,fb,fc) · 2 IntegerVectorEqual(ab,ac,db,dc,eb,ec,fb,fc,l) · 1 IntegerMatrixEntrywiseEqual(ab,ac,bb,bc,eb,ec,fb,fc,r,w) · 2 BetaAt(b,c,i,x) · 4

Actual proof prerequisites

matrix_integer_signed_minor_balancebeta_at_unique · checked external prerequisite

Original expanded first-order statement

forall ab ac bb bc eb ec fb fc cb cc db dc gb gc hb hc q. (forall mdr_ab_integer_recursion mdr_ac_integer_recursion mdr_bb_integer_recursion mdr_bc_integer_recursion mdr_eb_integer_recursion mdr_ec_integer_recursion mdr_fb_integer_recursion mdr_fc_integer_recursion mdr_p_integer_recursion mdr_n_integer_recursion mdr_P_integer_recursion mdr_N_integer_recursion. (forall ics_index_integer_recursionentries ics_value0_integer_recursionentries ics_value1_integer_recursionentries ics_value2_integer_recursionentries ics_value3_integer_recursionentries. (exists ics_gap_integer_recursionentries_bound. ics_gap_integer_recursionentries_bound + S (ics_index_integer_recursionentries) = ((q) * (q))) -> (((exists fs_h_ics_integer_recursionentries_at0. fs_h_ics_integer_recursionentries_at0 + S (ics_value0_integer_recursionentries) = S ((S (ics_index_integer_recursionentries)) * mdr_ac_integer_recursion)) /\ exists fs_q_ics_integer_recursionentries_at0. mdr_ab_integer_recursion = fs_q_ics_integer_recursionentries_at0 * S ((S (ics_index_integer_recursionentries)) * mdr_ac_integer_recursion) + (ics_value0_integer_recursionentries))) -> (((exists fs_h_ics_integer_recursionentries_at1. fs_h_ics_integer_recursionentries_at1 + S (ics_value1_integer_recursionentries) = S ((S (ics_index_integer_recursionentries)) * mdr_bc_integer_recursion)) /\ exists fs_q_ics_integer_recursionentries_at1. mdr_bb_integer_recursion = fs_q_ics_integer_recursionentries_at1 * S ((S (ics_index_integer_recursionentries)) * mdr_bc_integer_recursion) + (ics_value1_integer_recursionentries))) -> (((exists fs_h_ics_integer_recursionentries_at2. fs_h_ics_integer_recursionentries_at2 + S (ics_value2_integer_recursionentries) = S ((S (ics_index_integer_recursionentries)) * mdr_ec_integer_recursion)) /\ exists fs_q_ics_integer_recursionentries_at2. mdr_eb_integer_recursion = fs_q_ics_integer_recursionentries_at2 * S ((S (ics_index_integer_recursionentries)) * mdr_ec_integer_recursion) + (ics_value2_integer_recursionentries))) -> (((exists fs_h_ics_integer_recursionentries_at3. fs_h_ics_integer_recursionentries_at3 + S (ics_value3_integer_recursionentries) = S ((S (ics_index_integer_recursionentries)) * mdr_fc_integer_recursion)) /\ exists fs_q_ics_integer_recursionentries_at3. mdr_fb_integer_recursion = fs_q_ics_integer_recursionentries_at3 * S ((S (ics_index_integer_recursionentries)) * mdr_fc_integer_recursion) + (ics_value3_integer_recursionentries))) -> ics_value0_integer_recursionentries + ics_value3_integer_recursionentries = ics_value2_integer_recursionentries + ics_value1_integer_recursionentries) -> (exists mdr_b_integer_recursionfirst mdr_c_integer_recursionfirst mdr_l_integer_recursionfirst mdr_i_integer_recursionfirst. ((forall mdr_i_integer_recursionfirsth. (exists mdr_gap_integer_recursionfirsthi. mdr_gap_integer_recursionfirsthi + S (mdr_i_integer_recursionfirsth) = (mdr_l_integer_recursionfirst)) -> exists mdr_d_integer_recursionfirsth mdr_pb_integer_recursionfirsth mdr_pc_integer_recursionfirsth mdr_nb_integer_recursionfirsth mdr_nc_integer_recursionfirsth mdr_p_integer_recursionfirsth mdr_n_integer_recursionfirsth. ((exists mdr_z_integer_recursionfirsthr. ((exists mdr_a_integer_recursionfirsthrc mdr_b_integer_recursionfirsthrc mdr_c_integer_recursionfirsthrc mdr_e_integer_recursionfirsthrc mdr_f_integer_recursionfirsthrc. ((mdr_a_integer_recursionfirsthrc = ((mdr_d_integer_recursionfirsth) + (mdr_pb_integer_recursionfirsth)) * S ((mdr_d_integer_recursionfirsth) + (mdr_pb_integer_recursionfirsth)) + ((mdr_pb_integer_recursionfirsth) + (mdr_pb_integer_recursionfirsth))) /\ ((mdr_b_integer_recursionfirsthrc = ((mdr_pc_integer_recursionfirsth) + (mdr_nb_integer_recursionfirsth)) * S ((mdr_pc_integer_recursionfirsth) + (mdr_nb_integer_recursionfirsth)) + ((mdr_nb_integer_recursionfirsth) + (mdr_nb_integer_recursionfirsth))) /\ ((mdr_c_integer_recursionfirsthrc = ((mdr_a_integer_recursionfirsthrc) + (mdr_b_integer_recursionfirsthrc)) * S ((mdr_a_integer_recursionfirsthrc) + (mdr_b_integer_recursionfirsthrc)) + ((mdr_b_integer_recursionfirsthrc) + (mdr_b_integer_recursionfirsthrc))) /\ ((mdr_e_integer_recursionfirsthrc = ((mdr_p_integer_recursionfirsth) + (mdr_n_integer_recursionfirsth)) * S ((mdr_p_integer_recursionfirsth) + (mdr_n_integer_recursionfirsth)) + ((mdr_n_integer_recursionfirsth) + (mdr_n_integer_recursionfirsth))) /\ ((mdr_f_integer_recursionfirsthrc = ((mdr_nc_integer_recursionfirsth) + (mdr_e_integer_recursionfirsthrc)) * S ((mdr_nc_integer_recursionfirsth) + (mdr_e_integer_recursionfirsthrc)) + ((mdr_e_integer_recursionfirsthrc) + (mdr_e_integer_recursionfirsthrc))) /\ ((mdr_z_integer_recursionfirsthr) = ((mdr_c_integer_recursionfirsthrc) + (mdr_f_integer_recursionfirsthrc)) * S ((mdr_c_integer_recursionfirsthrc) + (mdr_f_integer_recursionfirsthrc)) + ((mdr_f_integer_recursionfirsthrc) + (mdr_f_integer_recursionfirsthrc))))))))) /\ (((exists ff_h_mdr_integer_recursionfirsthrb. ff_h_mdr_integer_recursionfirsthrb + S (mdr_z_integer_recursionfirsthr) = S ((S (mdr_i_integer_recursionfirsth)) * mdr_c_integer_recursionfirst)) /\ exists ff_q_mdr_integer_recursionfirsthrb. mdr_b_integer_recursionfirst = ff_q_mdr_integer_recursionfirsthrb * S ((S (mdr_i_integer_recursionfirsth)) * mdr_c_integer_recursionfirst) + (mdr_z_integer_recursionfirsthr))))) /\ (((((mdr_d_integer_recursionfirsth) = 0) /\ (((mdr_p_integer_recursionfirsth) = 1) /\ ((mdr_n_integer_recursionfirsth) = 0))) \/ exists mdr_q_integer_recursionfirsths mdr_eb_integer_recursionfirsths mdr_ec_integer_recursionfirsths mdr_fb_integer_recursionfirsths mdr_fc_integer_recursionfirsths. (((mdr_d_integer_recursionfirsth) = S (mdr_q_integer_recursionfirsths)) /\ ((forall mdr_j_integer_recursionfirsthsc. (exists mdr_gap_integer_recursionfirsthscj. mdr_gap_integer_recursionfirsthscj + S (mdr_j_integer_recursionfirsthsc) = (S (mdr_q_integer_recursionfirsths))) -> exists mdr_i_integer_recursionfirsthsc mdr_up_integer_recursionfirsthsc mdr_us_integer_recursionfirsthsc mdr_un_integer_recursionfirsthsc mdr_ut_integer_recursionfirsthsc mdr_p_integer_recursionfirsthsc mdr_n_integer_recursionfirsthsc. ((exists mdr_gap_integer_recursionfirsthsci. mdr_gap_integer_recursionfirsthsci + S (mdr_i_integer_recursionfirsthsc) = (mdr_i_integer_recursionfirsth)) /\ ((exists mdr_z_integer_recursionfirsthscr. ((exists mdr_a_integer_recursionfirsthscrc mdr_b_integer_recursionfirsthscrc mdr_c_integer_recursionfirsthscrc mdr_e_integer_recursionfirsthscrc mdr_f_integer_recursionfirsthscrc. ((mdr_a_integer_recursionfirsthscrc = ((mdr_q_integer_recursionfirsths) + (mdr_up_integer_recursionfirsthsc)) * S ((mdr_q_integer_recursionfirsths) + (mdr_up_integer_recursionfirsthsc)) + ((mdr_up_integer_recursionfirsthsc) + (mdr_up_integer_recursionfirsthsc))) /\ ((mdr_b_integer_recursionfirsthscrc = ((mdr_us_integer_recursionfirsthsc) + (mdr_un_integer_recursionfirsthsc)) * S ((mdr_us_integer_recursionfirsthsc) + (mdr_un_integer_recursionfirsthsc)) + ((mdr_un_integer_recursionfirsthsc) + (mdr_un_integer_recursionfirsthsc))) /\ ((mdr_c_integer_recursionfirsthscrc = ((mdr_a_integer_recursionfirsthscrc) + (mdr_b_integer_recursionfirsthscrc)) * S ((mdr_a_integer_recursionfirsthscrc) + (mdr_b_integer_recursionfirsthscrc)) + ((mdr_b_integer_recursionfirsthscrc) + (mdr_b_integer_recursionfirsthscrc))) /\ ((mdr_e_integer_recursionfirsthscrc = ((mdr_p_integer_recursionfirsthsc) + (mdr_n_integer_recursionfirsthsc)) * S ((mdr_p_integer_recursionfirsthsc) + (mdr_n_integer_recursionfirsthsc)) + ((mdr_n_integer_recursionfirsthsc) + (mdr_n_integer_recursionfirsthsc))) /\ ((mdr_f_integer_recursionfirsthscrc = ((mdr_ut_integer_recursionfirsthsc) + (mdr_e_integer_recursionfirsthscrc)) * S ((mdr_ut_integer_recursionfirsthsc) + (mdr_e_integer_recursionfirsthscrc)) + ((mdr_e_integer_recursionfirsthscrc) + (mdr_e_integer_recursionfirsthscrc))) /\ ((mdr_z_integer_recursionfirsthscr) = ((mdr_c_integer_recursionfirsthscrc) + (mdr_f_integer_recursionfirsthscrc)) * S ((mdr_c_integer_recursionfirsthscrc) + (mdr_f_integer_recursionfirsthscrc)) + ((mdr_f_integer_recursionfirsthscrc) + (mdr_f_integer_recursionfirsthscrc))))))))) /\ (((exists ff_h_mdr_integer_recursionfirsthscrb. ff_h_mdr_integer_recursionfirsthscrb + S (mdr_z_integer_recursionfirsthscr) = S ((S (mdr_i_integer_recursionfirsthsc)) * mdr_c_integer_recursionfirst)) /\ exists ff_q_mdr_integer_recursionfirsthscrb. mdr_b_integer_recursionfirst = ff_q_mdr_integer_recursionfirsthscrb * S ((S (mdr_i_integer_recursionfirsthsc)) * mdr_c_integer_recursionfirst) + (mdr_z_integer_recursionfirsthscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_integer_recursionfirsthscm_positive. (exists ff_gap_mdm_lt_mdr_integer_recursionfirsthscm_positive_index_bound. ff_gap_mdm_lt_mdr_integer_recursionfirsthscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_integer_recursionfirsthscm_positive) = ((mdr_q_integer_recursionfirsths) * (mdr_q_integer_recursionfirsths))) -> exists ff_row_mdm_prefix_mdr_integer_recursionfirsthscm_positive ff_column_mdm_prefix_mdr_integer_recursionfirsthscm_positive ff_value_mdm_prefix_mdr_integer_recursionfirsthscm_positive. (ff_index_mdm_prefix_mdr_integer_recursionfirsthscm_positive = (mdr_q_integer_recursionfirsths) * ff_row_mdm_prefix_mdr_integer_recursionfirsthscm_positive + ff_column_mdm_prefix_mdr_integer_recursionfirsthscm_positive /\ ((exists ff_gap_mdm_lt_mdr_integer_recursionfirsthscm_positive_column_bound. ff_gap_mdm_lt_mdr_integer_recursionfirsthscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_integer_recursionfirsthscm_positive) = (mdr_q_integer_recursionfirsths)) /\ ((exists ff_row_mdm_cell_mdr_integer_recursionfirsthscm_positive_cell ff_column_mdm_cell_mdr_integer_recursionfirsthscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_integer_recursionfirsthscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_integer_recursionfirsthscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_integer_recursionfirsthscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_integer_recursionfirsthscm_positive_cell = ff_row_mdm_prefix_mdr_integer_recursionfirsthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_integer_recursionfirsthscm_positive_cell_row_after. ff_gap_mdm_le_mdr_integer_recursionfirsthscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_integer_recursionfirsthscm_positive)) /\ ff_row_mdm_cell_mdr_integer_recursionfirsthscm_positive_cell = S ff_row_mdm_prefix_mdr_integer_recursionfirsthscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_integer_recursionfirsthscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_integer_recursionfirsthscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_integer_recursionfirsthscm_positive) = (mdr_j_integer_recursionfirsthsc)) /\ ff_column_mdm_cell_mdr_integer_recursionfirsthscm_positive_cell = ff_column_mdm_prefix_mdr_integer_recursionfirsthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_integer_recursionfirsthscm_positive_cell_column_after. ff_gap_mdm_le_mdr_integer_recursionfirsthscm_positive_cell_column_after + (mdr_j_integer_recursionfirsthsc) = (ff_column_mdm_prefix_mdr_integer_recursionfirsthscm_positive)) /\ ff_column_mdm_cell_mdr_integer_recursionfirsthscm_positive_cell = S ff_column_mdm_prefix_mdr_integer_recursionfirsthscm_positive))) /\ (((exists ff_h_mdm_mdr_integer_recursionfirsthscm_positive_cell_source. ff_h_mdm_mdr_integer_recursionfirsthscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_integer_recursionfirsthscm_positive) = S ((S ((ff_row_mdm_cell_mdr_integer_recursionfirsthscm_positive_cell) * (S (mdr_q_integer_recursionfirsths)) + (ff_column_mdm_cell_mdr_integer_recursionfirsthscm_positive_cell))) * mdr_pc_integer_recursionfirsth)) /\ exists ff_q_mdm_mdr_integer_recursionfirsthscm_positive_cell_source. mdr_pb_integer_recursionfirsth = ff_q_mdm_mdr_integer_recursionfirsthscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_integer_recursionfirsthscm_positive_cell) * (S (mdr_q_integer_recursionfirsths)) + (ff_column_mdm_cell_mdr_integer_recursionfirsthscm_positive_cell))) * mdr_pc_integer_recursionfirsth) + (ff_value_mdm_prefix_mdr_integer_recursionfirsthscm_positive)))))) /\ (((exists ff_h_mdm_mdr_integer_recursionfirsthscm_positive_target. ff_h_mdm_mdr_integer_recursionfirsthscm_positive_target + S (ff_value_mdm_prefix_mdr_integer_recursionfirsthscm_positive) = S ((S (ff_index_mdm_prefix_mdr_integer_recursionfirsthscm_positive)) * mdr_us_integer_recursionfirsthsc)) /\ exists ff_q_mdm_mdr_integer_recursionfirsthscm_positive_target. mdr_up_integer_recursionfirsthsc = ff_q_mdm_mdr_integer_recursionfirsthscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_integer_recursionfirsthscm_positive)) * mdr_us_integer_recursionfirsthsc) + (ff_value_mdm_prefix_mdr_integer_recursionfirsthscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_integer_recursionfirsthscm_negative. (exists ff_gap_mdm_lt_mdr_integer_recursionfirsthscm_negative_index_bound. ff_gap_mdm_lt_mdr_integer_recursionfirsthscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_integer_recursionfirsthscm_negative) = ((mdr_q_integer_recursionfirsths) * (mdr_q_integer_recursionfirsths))) -> exists ff_row_mdm_prefix_mdr_integer_recursionfirsthscm_negative ff_column_mdm_prefix_mdr_integer_recursionfirsthscm_negative ff_value_mdm_prefix_mdr_integer_recursionfirsthscm_negative. (ff_index_mdm_prefix_mdr_integer_recursionfirsthscm_negative = (mdr_q_integer_recursionfirsths) * ff_row_mdm_prefix_mdr_integer_recursionfirsthscm_negative + ff_column_mdm_prefix_mdr_integer_recursionfirsthscm_negative /\ ((exists ff_gap_mdm_lt_mdr_integer_recursionfirsthscm_negative_column_bound. ff_gap_mdm_lt_mdr_integer_recursionfirsthscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_integer_recursionfirsthscm_negative) = (mdr_q_integer_recursionfirsths)) /\ ((exists ff_row_mdm_cell_mdr_integer_recursionfirsthscm_negative_cell ff_column_mdm_cell_mdr_integer_recursionfirsthscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_integer_recursionfirsthscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_integer_recursionfirsthscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_integer_recursionfirsthscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_integer_recursionfirsthscm_negative_cell = ff_row_mdm_prefix_mdr_integer_recursionfirsthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_integer_recursionfirsthscm_negative_cell_row_after. ff_gap_mdm_le_mdr_integer_recursionfirsthscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_integer_recursionfirsthscm_negative)) /\ ff_row_mdm_cell_mdr_integer_recursionfirsthscm_negative_cell = S ff_row_mdm_prefix_mdr_integer_recursionfirsthscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_integer_recursionfirsthscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_integer_recursionfirsthscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_integer_recursionfirsthscm_negative) = (mdr_j_integer_recursionfirsthsc)) /\ ff_column_mdm_cell_mdr_integer_recursionfirsthscm_negative_cell = ff_column_mdm_prefix_mdr_integer_recursionfirsthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_integer_recursionfirsthscm_negative_cell_column_after. ff_gap_mdm_le_mdr_integer_recursionfirsthscm_negative_cell_column_after + (mdr_j_integer_recursionfirsthsc) = (ff_column_mdm_prefix_mdr_integer_recursionfirsthscm_negative)) /\ ff_column_mdm_cell_mdr_integer_recursionfirsthscm_negative_cell = S ff_column_mdm_prefix_mdr_integer_recursionfirsthscm_negative))) /\ (((exists ff_h_mdm_mdr_integer_recursionfirsthscm_negative_cell_source. ff_h_mdm_mdr_integer_recursionfirsthscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_integer_recursionfirsthscm_negative) = S ((S ((ff_row_mdm_cell_mdr_integer_recursionfirsthscm_negative_cell) * (S (mdr_q_integer_recursionfirsths)) + (ff_column_mdm_cell_mdr_integer_recursionfirsthscm_negative_cell))) * mdr_nc_integer_recursionfirsth)) /\ exists ff_q_mdm_mdr_integer_recursionfirsthscm_negative_cell_source. mdr_nb_integer_recursionfirsth = ff_q_mdm_mdr_integer_recursionfirsthscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_integer_recursionfirsthscm_negative_cell) * (S (mdr_q_integer_recursionfirsths)) + (ff_column_mdm_cell_mdr_integer_recursionfirsthscm_negative_cell))) * mdr_nc_integer_recursionfirsth) + (ff_value_mdm_prefix_mdr_integer_recursionfirsthscm_negative)))))) /\ (((exists ff_h_mdm_mdr_integer_recursionfirsthscm_negative_target. ff_h_mdm_mdr_integer_recursionfirsthscm_negative_target + S (ff_value_mdm_prefix_mdr_integer_recursionfirsthscm_negative) = S ((S (ff_index_mdm_prefix_mdr_integer_recursionfirsthscm_negative)) * mdr_ut_integer_recursionfirsthsc)) /\ exists ff_q_mdm_mdr_integer_recursionfirsthscm_negative_target. mdr_un_integer_recursionfirsthsc = ff_q_mdm_mdr_integer_recursionfirsthscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_integer_recursionfirsthscm_negative)) * mdr_ut_integer_recursionfirsthsc) + (ff_value_mdm_prefix_mdr_integer_recursionfirsthscm_negative))))))))) /\ ((((exists ff_h_mdr_integer_recursionfirsthscp. ff_h_mdr_integer_recursionfirsthscp + S (mdr_p_integer_recursionfirsthsc) = S ((S (mdr_j_integer_recursionfirsthsc)) * mdr_ec_integer_recursionfirsths)) /\ exists ff_q_mdr_integer_recursionfirsthscp. mdr_eb_integer_recursionfirsths = ff_q_mdr_integer_recursionfirsthscp * S ((S (mdr_j_integer_recursionfirsthsc)) * mdr_ec_integer_recursionfirsths) + (mdr_p_integer_recursionfirsthsc))) /\ (((exists ff_h_mdr_integer_recursionfirsthscn. ff_h_mdr_integer_recursionfirsthscn + S (mdr_n_integer_recursionfirsthsc) = S ((S (mdr_j_integer_recursionfirsthsc)) * mdr_fc_integer_recursionfirsths)) /\ exists ff_q_mdr_integer_recursionfirsthscn. mdr_fb_integer_recursionfirsths = ff_q_mdr_integer_recursionfirsthscn * S ((S (mdr_j_integer_recursionfirsthsc)) * mdr_fc_integer_recursionfirsths) + (mdr_n_integer_recursionfirsthsc)))))))) /\ (exists ff_ub_mce_fold_mdr_integer_recursionfirsthsf ff_uc_mce_fold_mdr_integer_recursionfirsthsf ff_vb_mce_fold_mdr_integer_recursionfirsthsf ff_vc_mce_fold_mdr_integer_recursionfirsthsf. ((forall ff_index_mce_alternating_mdr_integer_recursionfirsthsf_prefix. (exists ff_gap_mce_mdr_integer_recursionfirsthsf_prefix_index. ff_gap_mce_mdr_integer_recursionfirsthsf_prefix_index + S (ff_index_mce_alternating_mdr_integer_recursionfirsthsf_prefix) = (S (mdr_q_integer_recursionfirsths))) -> exists ff_ap_mce_alternating_mdr_integer_recursionfirsthsf_prefix ff_an_mce_alternating_mdr_integer_recursionfirsthsf_prefix ff_bp_mce_alternating_mdr_integer_recursionfirsthsf_prefix ff_bn_mce_alternating_mdr_integer_recursionfirsthsf_prefix ff_p_mce_alternating_mdr_integer_recursionfirsthsf_prefix ff_n_mce_alternating_mdr_integer_recursionfirsthsf_prefix. ((((exists ff_h_mce_mdr_integer_recursionfirsthsf_prefix_ap. ff_h_mce_mdr_integer_recursionfirsthsf_prefix_ap + S (ff_ap_mce_alternating_mdr_integer_recursionfirsthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_integer_recursionfirsthsf_prefix)) * mdr_pc_integer_recursionfirsth)) /\ exists ff_q_mce_mdr_integer_recursionfirsthsf_prefix_ap. mdr_pb_integer_recursionfirsth = ff_q_mce_mdr_integer_recursionfirsthsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_integer_recursionfirsthsf_prefix)) * mdr_pc_integer_recursionfirsth) + (ff_ap_mce_alternating_mdr_integer_recursionfirsthsf_prefix))) /\ ((((exists ff_h_mce_mdr_integer_recursionfirsthsf_prefix_an. ff_h_mce_mdr_integer_recursionfirsthsf_prefix_an + S (ff_an_mce_alternating_mdr_integer_recursionfirsthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_integer_recursionfirsthsf_prefix)) * mdr_nc_integer_recursionfirsth)) /\ exists ff_q_mce_mdr_integer_recursionfirsthsf_prefix_an. mdr_nb_integer_recursionfirsth = ff_q_mce_mdr_integer_recursionfirsthsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_integer_recursionfirsthsf_prefix)) * mdr_nc_integer_recursionfirsth) + (ff_an_mce_alternating_mdr_integer_recursionfirsthsf_prefix))) /\ ((((exists ff_h_mce_mdr_integer_recursionfirsthsf_prefix_bp. ff_h_mce_mdr_integer_recursionfirsthsf_prefix_bp + S (ff_bp_mce_alternating_mdr_integer_recursionfirsthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_integer_recursionfirsthsf_prefix)) * mdr_ec_integer_recursionfirsths)) /\ exists ff_q_mce_mdr_integer_recursionfirsthsf_prefix_bp. mdr_eb_integer_recursionfirsths = ff_q_mce_mdr_integer_recursionfirsthsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_integer_recursionfirsthsf_prefix)) * mdr_ec_integer_recursionfirsths) + (ff_bp_mce_alternating_mdr_integer_recursionfirsthsf_prefix))) /\ ((((exists ff_h_mce_mdr_integer_recursionfirsthsf_prefix_bn. ff_h_mce_mdr_integer_recursionfirsthsf_prefix_bn + S (ff_bn_mce_alternating_mdr_integer_recursionfirsthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_integer_recursionfirsthsf_prefix)) * mdr_fc_integer_recursionfirsths)) /\ exists ff_q_mce_mdr_integer_recursionfirsthsf_prefix_bn. mdr_fb_integer_recursionfirsths = ff_q_mce_mdr_integer_recursionfirsthsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_integer_recursionfirsthsf_prefix)) * mdr_fc_integer_recursionfirsths) + (ff_bn_mce_alternating_mdr_integer_recursionfirsthsf_prefix))) /\ ((((exists ff_h_mce_mdr_integer_recursionfirsthsf_prefix_positive. ff_h_mce_mdr_integer_recursionfirsthsf_prefix_positive + S (ff_p_mce_alternating_mdr_integer_recursionfirsthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_integer_recursionfirsthsf_prefix)) * ff_uc_mce_fold_mdr_integer_recursionfirsthsf)) /\ exists ff_q_mce_mdr_integer_recursionfirsthsf_prefix_positive. ff_ub_mce_fold_mdr_integer_recursionfirsthsf = ff_q_mce_mdr_integer_recursionfirsthsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_integer_recursionfirsthsf_prefix)) * ff_uc_mce_fold_mdr_integer_recursionfirsthsf) + (ff_p_mce_alternating_mdr_integer_recursionfirsthsf_prefix))) /\ ((((exists ff_h_mce_mdr_integer_recursionfirsthsf_prefix_negative. ff_h_mce_mdr_integer_recursionfirsthsf_prefix_negative + S (ff_n_mce_alternating_mdr_integer_recursionfirsthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_integer_recursionfirsthsf_prefix)) * ff_vc_mce_fold_mdr_integer_recursionfirsthsf)) /\ exists ff_q_mce_mdr_integer_recursionfirsthsf_prefix_negative. ff_vb_mce_fold_mdr_integer_recursionfirsthsf = ff_q_mce_mdr_integer_recursionfirsthsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_integer_recursionfirsthsf_prefix)) * ff_vc_mce_fold_mdr_integer_recursionfirsthsf) + (ff_n_mce_alternating_mdr_integer_recursionfirsthsf_prefix))) /\ (((exists ff_even_mce_term_mdr_integer_recursionfirsthsf_prefix_term. ff_index_mce_alternating_mdr_integer_recursionfirsthsf_prefix = 2 * ff_even_mce_term_mdr_integer_recursionfirsthsf_prefix_term) /\ (ff_p_mce_alternating_mdr_integer_recursionfirsthsf_prefix = (ff_ap_mce_alternating_mdr_integer_recursionfirsthsf_prefix) * (ff_bp_mce_alternating_mdr_integer_recursionfirsthsf_prefix) + (ff_an_mce_alternating_mdr_integer_recursionfirsthsf_prefix) * (ff_bn_mce_alternating_mdr_integer_recursionfirsthsf_prefix) /\ ff_n_mce_alternating_mdr_integer_recursionfirsthsf_prefix = (ff_ap_mce_alternating_mdr_integer_recursionfirsthsf_prefix) * (ff_bn_mce_alternating_mdr_integer_recursionfirsthsf_prefix) + (ff_an_mce_alternating_mdr_integer_recursionfirsthsf_prefix) * (ff_bp_mce_alternating_mdr_integer_recursionfirsthsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_integer_recursionfirsthsf_prefix_term. ff_index_mce_alternating_mdr_integer_recursionfirsthsf_prefix = 2 * ff_odd_mce_term_mdr_integer_recursionfirsthsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_integer_recursionfirsthsf_prefix = (ff_ap_mce_alternating_mdr_integer_recursionfirsthsf_prefix) * (ff_bn_mce_alternating_mdr_integer_recursionfirsthsf_prefix) + (ff_an_mce_alternating_mdr_integer_recursionfirsthsf_prefix) * (ff_bp_mce_alternating_mdr_integer_recursionfirsthsf_prefix) /\ ff_n_mce_alternating_mdr_integer_recursionfirsthsf_prefix = (ff_ap_mce_alternating_mdr_integer_recursionfirsthsf_prefix) * (ff_bp_mce_alternating_mdr_integer_recursionfirsthsf_prefix) + (ff_an_mce_alternating_mdr_integer_recursionfirsthsf_prefix) * (ff_bn_mce_alternating_mdr_integer_recursionfirsthsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_integer_recursionfirsthsf_positive ff_v_mce_mdr_integer_recursionfirsthsf_positive. ((((exists ff_h_mce_mdr_integer_recursionfirsthsf_positive_start. ff_h_mce_mdr_integer_recursionfirsthsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_integer_recursionfirsthsf_positive)) /\ exists ff_q_mce_mdr_integer_recursionfirsthsf_positive_start. ff_u_mce_mdr_integer_recursionfirsthsf_positive = ff_q_mce_mdr_integer_recursionfirsthsf_positive_start * S ((S (0)) * ff_v_mce_mdr_integer_recursionfirsthsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_integer_recursionfirsthsf_positive_terminal. ff_h_mce_mdr_integer_recursionfirsthsf_positive_terminal + S (mdr_p_integer_recursionfirsth) = S ((S ((S (mdr_q_integer_recursionfirsths)))) * ff_v_mce_mdr_integer_recursionfirsthsf_positive)) /\ exists ff_q_mce_mdr_integer_recursionfirsthsf_positive_terminal. ff_u_mce_mdr_integer_recursionfirsthsf_positive = ff_q_mce_mdr_integer_recursionfirsthsf_positive_terminal * S ((S ((S (mdr_q_integer_recursionfirsths)))) * ff_v_mce_mdr_integer_recursionfirsthsf_positive) + (mdr_p_integer_recursionfirsth))) /\ forall ff_i_mce_mdr_integer_recursionfirsthsf_positive. (exists ff_lt_mce_mdr_integer_recursionfirsthsf_positive_bound. ff_lt_mce_mdr_integer_recursionfirsthsf_positive_bound + S ff_i_mce_mdr_integer_recursionfirsthsf_positive = (S (mdr_q_integer_recursionfirsths))) -> exists ff_a_mce_mdr_integer_recursionfirsthsf_positive ff_r_mce_mdr_integer_recursionfirsthsf_positive ff_s_mce_mdr_integer_recursionfirsthsf_positive. ((((exists ff_h_mce_mdr_integer_recursionfirsthsf_positive_summand. ff_h_mce_mdr_integer_recursionfirsthsf_positive_summand + S (ff_a_mce_mdr_integer_recursionfirsthsf_positive) = S ((S (ff_i_mce_mdr_integer_recursionfirsthsf_positive)) * ff_uc_mce_fold_mdr_integer_recursionfirsthsf)) /\ exists ff_q_mce_mdr_integer_recursionfirsthsf_positive_summand. ff_ub_mce_fold_mdr_integer_recursionfirsthsf = ff_q_mce_mdr_integer_recursionfirsthsf_positive_summand * S ((S (ff_i_mce_mdr_integer_recursionfirsthsf_positive)) * ff_uc_mce_fold_mdr_integer_recursionfirsthsf) + (ff_a_mce_mdr_integer_recursionfirsthsf_positive))) /\ ((((exists ff_h_mce_mdr_integer_recursionfirsthsf_positive_partial. ff_h_mce_mdr_integer_recursionfirsthsf_positive_partial + S (ff_r_mce_mdr_integer_recursionfirsthsf_positive) = S ((S (ff_i_mce_mdr_integer_recursionfirsthsf_positive)) * ff_v_mce_mdr_integer_recursionfirsthsf_positive)) /\ exists ff_q_mce_mdr_integer_recursionfirsthsf_positive_partial. ff_u_mce_mdr_integer_recursionfirsthsf_positive = ff_q_mce_mdr_integer_recursionfirsthsf_positive_partial * S ((S (ff_i_mce_mdr_integer_recursionfirsthsf_positive)) * ff_v_mce_mdr_integer_recursionfirsthsf_positive) + (ff_r_mce_mdr_integer_recursionfirsthsf_positive))) /\ ((((exists ff_h_mce_mdr_integer_recursionfirsthsf_positive_successor. ff_h_mce_mdr_integer_recursionfirsthsf_positive_successor + S (ff_s_mce_mdr_integer_recursionfirsthsf_positive) = S ((S (S ff_i_mce_mdr_integer_recursionfirsthsf_positive)) * ff_v_mce_mdr_integer_recursionfirsthsf_positive)) /\ exists ff_q_mce_mdr_integer_recursionfirsthsf_positive_successor. ff_u_mce_mdr_integer_recursionfirsthsf_positive = ff_q_mce_mdr_integer_recursionfirsthsf_positive_successor * S ((S (S ff_i_mce_mdr_integer_recursionfirsthsf_positive)) * ff_v_mce_mdr_integer_recursionfirsthsf_positive) + (ff_s_mce_mdr_integer_recursionfirsthsf_positive))) /\ ff_s_mce_mdr_integer_recursionfirsthsf_positive = ff_r_mce_mdr_integer_recursionfirsthsf_positive + ff_a_mce_mdr_integer_recursionfirsthsf_positive)))))) /\ (exists ff_u_mce_mdr_integer_recursionfirsthsf_negative ff_v_mce_mdr_integer_recursionfirsthsf_negative. ((((exists ff_h_mce_mdr_integer_recursionfirsthsf_negative_start. ff_h_mce_mdr_integer_recursionfirsthsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_integer_recursionfirsthsf_negative)) /\ exists ff_q_mce_mdr_integer_recursionfirsthsf_negative_start. ff_u_mce_mdr_integer_recursionfirsthsf_negative = ff_q_mce_mdr_integer_recursionfirsthsf_negative_start * S ((S (0)) * ff_v_mce_mdr_integer_recursionfirsthsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_integer_recursionfirsthsf_negative_terminal. ff_h_mce_mdr_integer_recursionfirsthsf_negative_terminal + S (mdr_n_integer_recursionfirsth) = S ((S ((S (mdr_q_integer_recursionfirsths)))) * ff_v_mce_mdr_integer_recursionfirsthsf_negative)) /\ exists ff_q_mce_mdr_integer_recursionfirsthsf_negative_terminal. ff_u_mce_mdr_integer_recursionfirsthsf_negative = ff_q_mce_mdr_integer_recursionfirsthsf_negative_terminal * S ((S ((S (mdr_q_integer_recursionfirsths)))) * ff_v_mce_mdr_integer_recursionfirsthsf_negative) + (mdr_n_integer_recursionfirsth))) /\ forall ff_i_mce_mdr_integer_recursionfirsthsf_negative. (exists ff_lt_mce_mdr_integer_recursionfirsthsf_negative_bound. ff_lt_mce_mdr_integer_recursionfirsthsf_negative_bound + S ff_i_mce_mdr_integer_recursionfirsthsf_negative = (S (mdr_q_integer_recursionfirsths))) -> exists ff_a_mce_mdr_integer_recursionfirsthsf_negative ff_r_mce_mdr_integer_recursionfirsthsf_negative ff_s_mce_mdr_integer_recursionfirsthsf_negative. ((((exists ff_h_mce_mdr_integer_recursionfirsthsf_negative_summand. ff_h_mce_mdr_integer_recursionfirsthsf_negative_summand + S (ff_a_mce_mdr_integer_recursionfirsthsf_negative) = S ((S (ff_i_mce_mdr_integer_recursionfirsthsf_negative)) * ff_vc_mce_fold_mdr_integer_recursionfirsthsf)) /\ exists ff_q_mce_mdr_integer_recursionfirsthsf_negative_summand. ff_vb_mce_fold_mdr_integer_recursionfirsthsf = ff_q_mce_mdr_integer_recursionfirsthsf_negative_summand * S ((S (ff_i_mce_mdr_integer_recursionfirsthsf_negative)) * ff_vc_mce_fold_mdr_integer_recursionfirsthsf) + (ff_a_mce_mdr_integer_recursionfirsthsf_negative))) /\ ((((exists ff_h_mce_mdr_integer_recursionfirsthsf_negative_partial. ff_h_mce_mdr_integer_recursionfirsthsf_negative_partial + S (ff_r_mce_mdr_integer_recursionfirsthsf_negative) = S ((S (ff_i_mce_mdr_integer_recursionfirsthsf_negative)) * ff_v_mce_mdr_integer_recursionfirsthsf_negative)) /\ exists ff_q_mce_mdr_integer_recursionfirsthsf_negative_partial. ff_u_mce_mdr_integer_recursionfirsthsf_negative = ff_q_mce_mdr_integer_recursionfirsthsf_negative_partial * S ((S (ff_i_mce_mdr_integer_recursionfirsthsf_negative)) * ff_v_mce_mdr_integer_recursionfirsthsf_negative) + (ff_r_mce_mdr_integer_recursionfirsthsf_negative))) /\ ((((exists ff_h_mce_mdr_integer_recursionfirsthsf_negative_successor. ff_h_mce_mdr_integer_recursionfirsthsf_negative_successor + S (ff_s_mce_mdr_integer_recursionfirsthsf_negative) = S ((S (S ff_i_mce_mdr_integer_recursionfirsthsf_negative)) * ff_v_mce_mdr_integer_recursionfirsthsf_negative)) /\ exists ff_q_mce_mdr_integer_recursionfirsthsf_negative_successor. ff_u_mce_mdr_integer_recursionfirsthsf_negative = ff_q_mce_mdr_integer_recursionfirsthsf_negative_successor * S ((S (S ff_i_mce_mdr_integer_recursionfirsthsf_negative)) * ff_v_mce_mdr_integer_recursionfirsthsf_negative) + (ff_s_mce_mdr_integer_recursionfirsthsf_negative))) /\ ff_s_mce_mdr_integer_recursionfirsthsf_negative = ff_r_mce_mdr_integer_recursionfirsthsf_negative + ff_a_mce_mdr_integer_recursionfirsthsf_negative))))))))))))))) /\ ((exists mdr_gap_integer_recursionfirsti. mdr_gap_integer_recursionfirsti + S (mdr_i_integer_recursionfirst) = (mdr_l_integer_recursionfirst)) /\ (exists mdr_z_integer_recursionfirstr. ((exists mdr_a_integer_recursionfirstrc mdr_b_integer_recursionfirstrc mdr_c_integer_recursionfirstrc mdr_e_integer_recursionfirstrc mdr_f_integer_recursionfirstrc. ((mdr_a_integer_recursionfirstrc = ((q) + (mdr_ab_integer_recursion)) * S ((q) + (mdr_ab_integer_recursion)) + ((mdr_ab_integer_recursion) + (mdr_ab_integer_recursion))) /\ ((mdr_b_integer_recursionfirstrc = ((mdr_ac_integer_recursion) + (mdr_bb_integer_recursion)) * S ((mdr_ac_integer_recursion) + (mdr_bb_integer_recursion)) + ((mdr_bb_integer_recursion) + (mdr_bb_integer_recursion))) /\ ((mdr_c_integer_recursionfirstrc = ((mdr_a_integer_recursionfirstrc) + (mdr_b_integer_recursionfirstrc)) * S ((mdr_a_integer_recursionfirstrc) + (mdr_b_integer_recursionfirstrc)) + ((mdr_b_integer_recursionfirstrc) + (mdr_b_integer_recursionfirstrc))) /\ ((mdr_e_integer_recursionfirstrc = ((mdr_p_integer_recursion) + (mdr_n_integer_recursion)) * S ((mdr_p_integer_recursion) + (mdr_n_integer_recursion)) + ((mdr_n_integer_recursion) + (mdr_n_integer_recursion))) /\ ((mdr_f_integer_recursionfirstrc = ((mdr_bc_integer_recursion) + (mdr_e_integer_recursionfirstrc)) * S ((mdr_bc_integer_recursion) + (mdr_e_integer_recursionfirstrc)) + ((mdr_e_integer_recursionfirstrc) + (mdr_e_integer_recursionfirstrc))) /\ ((mdr_z_integer_recursionfirstr) = ((mdr_c_integer_recursionfirstrc) + (mdr_f_integer_recursionfirstrc)) * S ((mdr_c_integer_recursionfirstrc) + (mdr_f_integer_recursionfirstrc)) + ((mdr_f_integer_recursionfirstrc) + (mdr_f_integer_recursionfirstrc))))))))) /\ (((exists ff_h_mdr_integer_recursionfirstrb. ff_h_mdr_integer_recursionfirstrb + S (mdr_z_integer_recursionfirstr) = S ((S (mdr_i_integer_recursionfirst)) * mdr_c_integer_recursionfirst)) /\ exists ff_q_mdr_integer_recursionfirstrb. mdr_b_integer_recursionfirst = ff_q_mdr_integer_recursionfirstrb * S ((S (mdr_i_integer_recursionfirst)) * mdr_c_integer_recursionfirst) + (mdr_z_integer_recursionfirstr)))))))) -> (exists mdr_b_integer_recursionsecond mdr_c_integer_recursionsecond mdr_l_integer_recursionsecond mdr_i_integer_recursionsecond. ((forall mdr_i_integer_recursionsecondh. (exists mdr_gap_integer_recursionsecondhi. mdr_gap_integer_recursionsecondhi + S (mdr_i_integer_recursionsecondh) = (mdr_l_integer_recursionsecond)) -> exists mdr_d_integer_recursionsecondh mdr_pb_integer_recursionsecondh mdr_pc_integer_recursionsecondh mdr_nb_integer_recursionsecondh mdr_nc_integer_recursionsecondh mdr_p_integer_recursionsecondh mdr_n_integer_recursionsecondh. ((exists mdr_z_integer_recursionsecondhr. ((exists mdr_a_integer_recursionsecondhrc mdr_b_integer_recursionsecondhrc mdr_c_integer_recursionsecondhrc mdr_e_integer_recursionsecondhrc mdr_f_integer_recursionsecondhrc. ((mdr_a_integer_recursionsecondhrc = ((mdr_d_integer_recursionsecondh) + (mdr_pb_integer_recursionsecondh)) * S ((mdr_d_integer_recursionsecondh) + (mdr_pb_integer_recursionsecondh)) + ((mdr_pb_integer_recursionsecondh) + (mdr_pb_integer_recursionsecondh))) /\ ((mdr_b_integer_recursionsecondhrc = ((mdr_pc_integer_recursionsecondh) + (mdr_nb_integer_recursionsecondh)) * S ((mdr_pc_integer_recursionsecondh) + (mdr_nb_integer_recursionsecondh)) + ((mdr_nb_integer_recursionsecondh) + (mdr_nb_integer_recursionsecondh))) /\ ((mdr_c_integer_recursionsecondhrc = ((mdr_a_integer_recursionsecondhrc) + (mdr_b_integer_recursionsecondhrc)) * S ((mdr_a_integer_recursionsecondhrc) + (mdr_b_integer_recursionsecondhrc)) + ((mdr_b_integer_recursionsecondhrc) + (mdr_b_integer_recursionsecondhrc))) /\ ((mdr_e_integer_recursionsecondhrc = ((mdr_p_integer_recursionsecondh) + (mdr_n_integer_recursionsecondh)) * S ((mdr_p_integer_recursionsecondh) + (mdr_n_integer_recursionsecondh)) + ((mdr_n_integer_recursionsecondh) + (mdr_n_integer_recursionsecondh))) /\ ((mdr_f_integer_recursionsecondhrc = ((mdr_nc_integer_recursionsecondh) + (mdr_e_integer_recursionsecondhrc)) * S ((mdr_nc_integer_recursionsecondh) + (mdr_e_integer_recursionsecondhrc)) + ((mdr_e_integer_recursionsecondhrc) + (mdr_e_integer_recursionsecondhrc))) /\ ((mdr_z_integer_recursionsecondhr) = ((mdr_c_integer_recursionsecondhrc) + (mdr_f_integer_recursionsecondhrc)) * S ((mdr_c_integer_recursionsecondhrc) + (mdr_f_integer_recursionsecondhrc)) + ((mdr_f_integer_recursionsecondhrc) + (mdr_f_integer_recursionsecondhrc))))))))) /\ (((exists ff_h_mdr_integer_recursionsecondhrb. ff_h_mdr_integer_recursionsecondhrb + S (mdr_z_integer_recursionsecondhr) = S ((S (mdr_i_integer_recursionsecondh)) * mdr_c_integer_recursionsecond)) /\ exists ff_q_mdr_integer_recursionsecondhrb. mdr_b_integer_recursionsecond = ff_q_mdr_integer_recursionsecondhrb * S ((S (mdr_i_integer_recursionsecondh)) * mdr_c_integer_recursionsecond) + (mdr_z_integer_recursionsecondhr))))) /\ (((((mdr_d_integer_recursionsecondh) = 0) /\ (((mdr_p_integer_recursionsecondh) = 1) /\ ((mdr_n_integer_recursionsecondh) = 0))) \/ exists mdr_q_integer_recursionsecondhs mdr_eb_integer_recursionsecondhs mdr_ec_integer_recursionsecondhs mdr_fb_integer_recursionsecondhs mdr_fc_integer_recursionsecondhs. (((mdr_d_integer_recursionsecondh) = S (mdr_q_integer_recursionsecondhs)) /\ ((forall mdr_j_integer_recursionsecondhsc. (exists mdr_gap_integer_recursionsecondhscj. mdr_gap_integer_recursionsecondhscj + S (mdr_j_integer_recursionsecondhsc) = (S (mdr_q_integer_recursionsecondhs))) -> exists mdr_i_integer_recursionsecondhsc mdr_up_integer_recursionsecondhsc mdr_us_integer_recursionsecondhsc mdr_un_integer_recursionsecondhsc mdr_ut_integer_recursionsecondhsc mdr_p_integer_recursionsecondhsc mdr_n_integer_recursionsecondhsc. ((exists mdr_gap_integer_recursionsecondhsci. mdr_gap_integer_recursionsecondhsci + S (mdr_i_integer_recursionsecondhsc) = (mdr_i_integer_recursionsecondh)) /\ ((exists mdr_z_integer_recursionsecondhscr. ((exists mdr_a_integer_recursionsecondhscrc mdr_b_integer_recursionsecondhscrc mdr_c_integer_recursionsecondhscrc mdr_e_integer_recursionsecondhscrc mdr_f_integer_recursionsecondhscrc. ((mdr_a_integer_recursionsecondhscrc = ((mdr_q_integer_recursionsecondhs) + (mdr_up_integer_recursionsecondhsc)) * S ((mdr_q_integer_recursionsecondhs) + (mdr_up_integer_recursionsecondhsc)) + ((mdr_up_integer_recursionsecondhsc) + (mdr_up_integer_recursionsecondhsc))) /\ ((mdr_b_integer_recursionsecondhscrc = ((mdr_us_integer_recursionsecondhsc) + (mdr_un_integer_recursionsecondhsc)) * S ((mdr_us_integer_recursionsecondhsc) + (mdr_un_integer_recursionsecondhsc)) + ((mdr_un_integer_recursionsecondhsc) + (mdr_un_integer_recursionsecondhsc))) /\ ((mdr_c_integer_recursionsecondhscrc = ((mdr_a_integer_recursionsecondhscrc) + (mdr_b_integer_recursionsecondhscrc)) * S ((mdr_a_integer_recursionsecondhscrc) + (mdr_b_integer_recursionsecondhscrc)) + ((mdr_b_integer_recursionsecondhscrc) + (mdr_b_integer_recursionsecondhscrc))) /\ ((mdr_e_integer_recursionsecondhscrc = ((mdr_p_integer_recursionsecondhsc) + (mdr_n_integer_recursionsecondhsc)) * S ((mdr_p_integer_recursionsecondhsc) + (mdr_n_integer_recursionsecondhsc)) + ((mdr_n_integer_recursionsecondhsc) + (mdr_n_integer_recursionsecondhsc))) /\ ((mdr_f_integer_recursionsecondhscrc = ((mdr_ut_integer_recursionsecondhsc) + (mdr_e_integer_recursionsecondhscrc)) * S ((mdr_ut_integer_recursionsecondhsc) + (mdr_e_integer_recursionsecondhscrc)) + ((mdr_e_integer_recursionsecondhscrc) + (mdr_e_integer_recursionsecondhscrc))) /\ ((mdr_z_integer_recursionsecondhscr) = ((mdr_c_integer_recursionsecondhscrc) + (mdr_f_integer_recursionsecondhscrc)) * S ((mdr_c_integer_recursionsecondhscrc) + (mdr_f_integer_recursionsecondhscrc)) + ((mdr_f_integer_recursionsecondhscrc) + (mdr_f_integer_recursionsecondhscrc))))))))) /\ (((exists ff_h_mdr_integer_recursionsecondhscrb. ff_h_mdr_integer_recursionsecondhscrb + S (mdr_z_integer_recursionsecondhscr) = S ((S (mdr_i_integer_recursionsecondhsc)) * mdr_c_integer_recursionsecond)) /\ exists ff_q_mdr_integer_recursionsecondhscrb. mdr_b_integer_recursionsecond = ff_q_mdr_integer_recursionsecondhscrb * S ((S (mdr_i_integer_recursionsecondhsc)) * mdr_c_integer_recursionsecond) + (mdr_z_integer_recursionsecondhscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_integer_recursionsecondhscm_positive. (exists ff_gap_mdm_lt_mdr_integer_recursionsecondhscm_positive_index_bound. ff_gap_mdm_lt_mdr_integer_recursionsecondhscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_integer_recursionsecondhscm_positive) = ((mdr_q_integer_recursionsecondhs) * (mdr_q_integer_recursionsecondhs))) -> exists ff_row_mdm_prefix_mdr_integer_recursionsecondhscm_positive ff_column_mdm_prefix_mdr_integer_recursionsecondhscm_positive ff_value_mdm_prefix_mdr_integer_recursionsecondhscm_positive. (ff_index_mdm_prefix_mdr_integer_recursionsecondhscm_positive = (mdr_q_integer_recursionsecondhs) * ff_row_mdm_prefix_mdr_integer_recursionsecondhscm_positive + ff_column_mdm_prefix_mdr_integer_recursionsecondhscm_positive /\ ((exists ff_gap_mdm_lt_mdr_integer_recursionsecondhscm_positive_column_bound. ff_gap_mdm_lt_mdr_integer_recursionsecondhscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_integer_recursionsecondhscm_positive) = (mdr_q_integer_recursionsecondhs)) /\ ((exists ff_row_mdm_cell_mdr_integer_recursionsecondhscm_positive_cell ff_column_mdm_cell_mdr_integer_recursionsecondhscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_integer_recursionsecondhscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_integer_recursionsecondhscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_integer_recursionsecondhscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_integer_recursionsecondhscm_positive_cell = ff_row_mdm_prefix_mdr_integer_recursionsecondhscm_positive) \/ ((exists ff_gap_mdm_le_mdr_integer_recursionsecondhscm_positive_cell_row_after. ff_gap_mdm_le_mdr_integer_recursionsecondhscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_integer_recursionsecondhscm_positive)) /\ ff_row_mdm_cell_mdr_integer_recursionsecondhscm_positive_cell = S ff_row_mdm_prefix_mdr_integer_recursionsecondhscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_integer_recursionsecondhscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_integer_recursionsecondhscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_integer_recursionsecondhscm_positive) = (mdr_j_integer_recursionsecondhsc)) /\ ff_column_mdm_cell_mdr_integer_recursionsecondhscm_positive_cell = ff_column_mdm_prefix_mdr_integer_recursionsecondhscm_positive) \/ ((exists ff_gap_mdm_le_mdr_integer_recursionsecondhscm_positive_cell_column_after. ff_gap_mdm_le_mdr_integer_recursionsecondhscm_positive_cell_column_after + (mdr_j_integer_recursionsecondhsc) = (ff_column_mdm_prefix_mdr_integer_recursionsecondhscm_positive)) /\ ff_column_mdm_cell_mdr_integer_recursionsecondhscm_positive_cell = S ff_column_mdm_prefix_mdr_integer_recursionsecondhscm_positive))) /\ (((exists ff_h_mdm_mdr_integer_recursionsecondhscm_positive_cell_source. ff_h_mdm_mdr_integer_recursionsecondhscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_integer_recursionsecondhscm_positive) = S ((S ((ff_row_mdm_cell_mdr_integer_recursionsecondhscm_positive_cell) * (S (mdr_q_integer_recursionsecondhs)) + (ff_column_mdm_cell_mdr_integer_recursionsecondhscm_positive_cell))) * mdr_pc_integer_recursionsecondh)) /\ exists ff_q_mdm_mdr_integer_recursionsecondhscm_positive_cell_source. mdr_pb_integer_recursionsecondh = ff_q_mdm_mdr_integer_recursionsecondhscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_integer_recursionsecondhscm_positive_cell) * (S (mdr_q_integer_recursionsecondhs)) + (ff_column_mdm_cell_mdr_integer_recursionsecondhscm_positive_cell))) * mdr_pc_integer_recursionsecondh) + (ff_value_mdm_prefix_mdr_integer_recursionsecondhscm_positive)))))) /\ (((exists ff_h_mdm_mdr_integer_recursionsecondhscm_positive_target. ff_h_mdm_mdr_integer_recursionsecondhscm_positive_target + S (ff_value_mdm_prefix_mdr_integer_recursionsecondhscm_positive) = S ((S (ff_index_mdm_prefix_mdr_integer_recursionsecondhscm_positive)) * mdr_us_integer_recursionsecondhsc)) /\ exists ff_q_mdm_mdr_integer_recursionsecondhscm_positive_target. mdr_up_integer_recursionsecondhsc = ff_q_mdm_mdr_integer_recursionsecondhscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_integer_recursionsecondhscm_positive)) * mdr_us_integer_recursionsecondhsc) + (ff_value_mdm_prefix_mdr_integer_recursionsecondhscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_integer_recursionsecondhscm_negative. (exists ff_gap_mdm_lt_mdr_integer_recursionsecondhscm_negative_index_bound. ff_gap_mdm_lt_mdr_integer_recursionsecondhscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_integer_recursionsecondhscm_negative) = ((mdr_q_integer_recursionsecondhs) * (mdr_q_integer_recursionsecondhs))) -> exists ff_row_mdm_prefix_mdr_integer_recursionsecondhscm_negative ff_column_mdm_prefix_mdr_integer_recursionsecondhscm_negative ff_value_mdm_prefix_mdr_integer_recursionsecondhscm_negative. (ff_index_mdm_prefix_mdr_integer_recursionsecondhscm_negative = (mdr_q_integer_recursionsecondhs) * ff_row_mdm_prefix_mdr_integer_recursionsecondhscm_negative + ff_column_mdm_prefix_mdr_integer_recursionsecondhscm_negative /\ ((exists ff_gap_mdm_lt_mdr_integer_recursionsecondhscm_negative_column_bound. ff_gap_mdm_lt_mdr_integer_recursionsecondhscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_integer_recursionsecondhscm_negative) = (mdr_q_integer_recursionsecondhs)) /\ ((exists ff_row_mdm_cell_mdr_integer_recursionsecondhscm_negative_cell ff_column_mdm_cell_mdr_integer_recursionsecondhscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_integer_recursionsecondhscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_integer_recursionsecondhscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_integer_recursionsecondhscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_integer_recursionsecondhscm_negative_cell = ff_row_mdm_prefix_mdr_integer_recursionsecondhscm_negative) \/ ((exists ff_gap_mdm_le_mdr_integer_recursionsecondhscm_negative_cell_row_after. ff_gap_mdm_le_mdr_integer_recursionsecondhscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_integer_recursionsecondhscm_negative)) /\ ff_row_mdm_cell_mdr_integer_recursionsecondhscm_negative_cell = S ff_row_mdm_prefix_mdr_integer_recursionsecondhscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_integer_recursionsecondhscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_integer_recursionsecondhscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_integer_recursionsecondhscm_negative) = (mdr_j_integer_recursionsecondhsc)) /\ ff_column_mdm_cell_mdr_integer_recursionsecondhscm_negative_cell = ff_column_mdm_prefix_mdr_integer_recursionsecondhscm_negative) \/ ((exists ff_gap_mdm_le_mdr_integer_recursionsecondhscm_negative_cell_column_after. ff_gap_mdm_le_mdr_integer_recursionsecondhscm_negative_cell_column_after + (mdr_j_integer_recursionsecondhsc) = (ff_column_mdm_prefix_mdr_integer_recursionsecondhscm_negative)) /\ ff_column_mdm_cell_mdr_integer_recursionsecondhscm_negative_cell = S ff_column_mdm_prefix_mdr_integer_recursionsecondhscm_negative))) /\ (((exists ff_h_mdm_mdr_integer_recursionsecondhscm_negative_cell_source. ff_h_mdm_mdr_integer_recursionsecondhscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_integer_recursionsecondhscm_negative) = S ((S ((ff_row_mdm_cell_mdr_integer_recursionsecondhscm_negative_cell) * (S (mdr_q_integer_recursionsecondhs)) + (ff_column_mdm_cell_mdr_integer_recursionsecondhscm_negative_cell))) * mdr_nc_integer_recursionsecondh)) /\ exists ff_q_mdm_mdr_integer_recursionsecondhscm_negative_cell_source. mdr_nb_integer_recursionsecondh = ff_q_mdm_mdr_integer_recursionsecondhscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_integer_recursionsecondhscm_negative_cell) * (S (mdr_q_integer_recursionsecondhs)) + (ff_column_mdm_cell_mdr_integer_recursionsecondhscm_negative_cell))) * mdr_nc_integer_recursionsecondh) + (ff_value_mdm_prefix_mdr_integer_recursionsecondhscm_negative)))))) /\ (((exists ff_h_mdm_mdr_integer_recursionsecondhscm_negative_target. ff_h_mdm_mdr_integer_recursionsecondhscm_negative_target + S (ff_value_mdm_prefix_mdr_integer_recursionsecondhscm_negative) = S ((S (ff_index_mdm_prefix_mdr_integer_recursionsecondhscm_negative)) * mdr_ut_integer_recursionsecondhsc)) /\ exists ff_q_mdm_mdr_integer_recursionsecondhscm_negative_target. mdr_un_integer_recursionsecondhsc = ff_q_mdm_mdr_integer_recursionsecondhscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_integer_recursionsecondhscm_negative)) * mdr_ut_integer_recursionsecondhsc) + (ff_value_mdm_prefix_mdr_integer_recursionsecondhscm_negative))))))))) /\ ((((exists ff_h_mdr_integer_recursionsecondhscp. ff_h_mdr_integer_recursionsecondhscp + S (mdr_p_integer_recursionsecondhsc) = S ((S (mdr_j_integer_recursionsecondhsc)) * mdr_ec_integer_recursionsecondhs)) /\ exists ff_q_mdr_integer_recursionsecondhscp. mdr_eb_integer_recursionsecondhs = ff_q_mdr_integer_recursionsecondhscp * S ((S (mdr_j_integer_recursionsecondhsc)) * mdr_ec_integer_recursionsecondhs) + (mdr_p_integer_recursionsecondhsc))) /\ (((exists ff_h_mdr_integer_recursionsecondhscn. ff_h_mdr_integer_recursionsecondhscn + S (mdr_n_integer_recursionsecondhsc) = S ((S (mdr_j_integer_recursionsecondhsc)) * mdr_fc_integer_recursionsecondhs)) /\ exists ff_q_mdr_integer_recursionsecondhscn. mdr_fb_integer_recursionsecondhs = ff_q_mdr_integer_recursionsecondhscn * S ((S (mdr_j_integer_recursionsecondhsc)) * mdr_fc_integer_recursionsecondhs) + (mdr_n_integer_recursionsecondhsc)))))))) /\ (exists ff_ub_mce_fold_mdr_integer_recursionsecondhsf ff_uc_mce_fold_mdr_integer_recursionsecondhsf ff_vb_mce_fold_mdr_integer_recursionsecondhsf ff_vc_mce_fold_mdr_integer_recursionsecondhsf. ((forall ff_index_mce_alternating_mdr_integer_recursionsecondhsf_prefix. (exists ff_gap_mce_mdr_integer_recursionsecondhsf_prefix_index. ff_gap_mce_mdr_integer_recursionsecondhsf_prefix_index + S (ff_index_mce_alternating_mdr_integer_recursionsecondhsf_prefix) = (S (mdr_q_integer_recursionsecondhs))) -> exists ff_ap_mce_alternating_mdr_integer_recursionsecondhsf_prefix ff_an_mce_alternating_mdr_integer_recursionsecondhsf_prefix ff_bp_mce_alternating_mdr_integer_recursionsecondhsf_prefix ff_bn_mce_alternating_mdr_integer_recursionsecondhsf_prefix ff_p_mce_alternating_mdr_integer_recursionsecondhsf_prefix ff_n_mce_alternating_mdr_integer_recursionsecondhsf_prefix. ((((exists ff_h_mce_mdr_integer_recursionsecondhsf_prefix_ap. ff_h_mce_mdr_integer_recursionsecondhsf_prefix_ap + S (ff_ap_mce_alternating_mdr_integer_recursionsecondhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_integer_recursionsecondhsf_prefix)) * mdr_pc_integer_recursionsecondh)) /\ exists ff_q_mce_mdr_integer_recursionsecondhsf_prefix_ap. mdr_pb_integer_recursionsecondh = ff_q_mce_mdr_integer_recursionsecondhsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_integer_recursionsecondhsf_prefix)) * mdr_pc_integer_recursionsecondh) + (ff_ap_mce_alternating_mdr_integer_recursionsecondhsf_prefix))) /\ ((((exists ff_h_mce_mdr_integer_recursionsecondhsf_prefix_an. ff_h_mce_mdr_integer_recursionsecondhsf_prefix_an + S (ff_an_mce_alternating_mdr_integer_recursionsecondhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_integer_recursionsecondhsf_prefix)) * mdr_nc_integer_recursionsecondh)) /\ exists ff_q_mce_mdr_integer_recursionsecondhsf_prefix_an. mdr_nb_integer_recursionsecondh = ff_q_mce_mdr_integer_recursionsecondhsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_integer_recursionsecondhsf_prefix)) * mdr_nc_integer_recursionsecondh) + (ff_an_mce_alternating_mdr_integer_recursionsecondhsf_prefix))) /\ ((((exists ff_h_mce_mdr_integer_recursionsecondhsf_prefix_bp. ff_h_mce_mdr_integer_recursionsecondhsf_prefix_bp + S (ff_bp_mce_alternating_mdr_integer_recursionsecondhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_integer_recursionsecondhsf_prefix)) * mdr_ec_integer_recursionsecondhs)) /\ exists ff_q_mce_mdr_integer_recursionsecondhsf_prefix_bp. mdr_eb_integer_recursionsecondhs = ff_q_mce_mdr_integer_recursionsecondhsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_integer_recursionsecondhsf_prefix)) * mdr_ec_integer_recursionsecondhs) + (ff_bp_mce_alternating_mdr_integer_recursionsecondhsf_prefix))) /\ ((((exists ff_h_mce_mdr_integer_recursionsecondhsf_prefix_bn. ff_h_mce_mdr_integer_recursionsecondhsf_prefix_bn + S (ff_bn_mce_alternating_mdr_integer_recursionsecondhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_integer_recursionsecondhsf_prefix)) * mdr_fc_integer_recursionsecondhs)) /\ exists ff_q_mce_mdr_integer_recursionsecondhsf_prefix_bn. mdr_fb_integer_recursionsecondhs = ff_q_mce_mdr_integer_recursionsecondhsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_integer_recursionsecondhsf_prefix)) * mdr_fc_integer_recursionsecondhs) + (ff_bn_mce_alternating_mdr_integer_recursionsecondhsf_prefix))) /\ ((((exists ff_h_mce_mdr_integer_recursionsecondhsf_prefix_positive. ff_h_mce_mdr_integer_recursionsecondhsf_prefix_positive + S (ff_p_mce_alternating_mdr_integer_recursionsecondhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_integer_recursionsecondhsf_prefix)) * ff_uc_mce_fold_mdr_integer_recursionsecondhsf)) /\ exists ff_q_mce_mdr_integer_recursionsecondhsf_prefix_positive. ff_ub_mce_fold_mdr_integer_recursionsecondhsf = ff_q_mce_mdr_integer_recursionsecondhsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_integer_recursionsecondhsf_prefix)) * ff_uc_mce_fold_mdr_integer_recursionsecondhsf) + (ff_p_mce_alternating_mdr_integer_recursionsecondhsf_prefix))) /\ ((((exists ff_h_mce_mdr_integer_recursionsecondhsf_prefix_negative. ff_h_mce_mdr_integer_recursionsecondhsf_prefix_negative + S (ff_n_mce_alternating_mdr_integer_recursionsecondhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_integer_recursionsecondhsf_prefix)) * ff_vc_mce_fold_mdr_integer_recursionsecondhsf)) /\ exists ff_q_mce_mdr_integer_recursionsecondhsf_prefix_negative. ff_vb_mce_fold_mdr_integer_recursionsecondhsf = ff_q_mce_mdr_integer_recursionsecondhsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_integer_recursionsecondhsf_prefix)) * ff_vc_mce_fold_mdr_integer_recursionsecondhsf) + (ff_n_mce_alternating_mdr_integer_recursionsecondhsf_prefix))) /\ (((exists ff_even_mce_term_mdr_integer_recursionsecondhsf_prefix_term. ff_index_mce_alternating_mdr_integer_recursionsecondhsf_prefix = 2 * ff_even_mce_term_mdr_integer_recursionsecondhsf_prefix_term) /\ (ff_p_mce_alternating_mdr_integer_recursionsecondhsf_prefix = (ff_ap_mce_alternating_mdr_integer_recursionsecondhsf_prefix) * (ff_bp_mce_alternating_mdr_integer_recursionsecondhsf_prefix) + (ff_an_mce_alternating_mdr_integer_recursionsecondhsf_prefix) * (ff_bn_mce_alternating_mdr_integer_recursionsecondhsf_prefix) /\ ff_n_mce_alternating_mdr_integer_recursionsecondhsf_prefix = (ff_ap_mce_alternating_mdr_integer_recursionsecondhsf_prefix) * (ff_bn_mce_alternating_mdr_integer_recursionsecondhsf_prefix) + (ff_an_mce_alternating_mdr_integer_recursionsecondhsf_prefix) * (ff_bp_mce_alternating_mdr_integer_recursionsecondhsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_integer_recursionsecondhsf_prefix_term. ff_index_mce_alternating_mdr_integer_recursionsecondhsf_prefix = 2 * ff_odd_mce_term_mdr_integer_recursionsecondhsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_integer_recursionsecondhsf_prefix = (ff_ap_mce_alternating_mdr_integer_recursionsecondhsf_prefix) * (ff_bn_mce_alternating_mdr_integer_recursionsecondhsf_prefix) + (ff_an_mce_alternating_mdr_integer_recursionsecondhsf_prefix) * (ff_bp_mce_alternating_mdr_integer_recursionsecondhsf_prefix) /\ ff_n_mce_alternating_mdr_integer_recursionsecondhsf_prefix = (ff_ap_mce_alternating_mdr_integer_recursionsecondhsf_prefix) * (ff_bp_mce_alternating_mdr_integer_recursionsecondhsf_prefix) + (ff_an_mce_alternating_mdr_integer_recursionsecondhsf_prefix) * (ff_bn_mce_alternating_mdr_integer_recursionsecondhsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_integer_recursionsecondhsf_positive ff_v_mce_mdr_integer_recursionsecondhsf_positive. ((((exists ff_h_mce_mdr_integer_recursionsecondhsf_positive_start. ff_h_mce_mdr_integer_recursionsecondhsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_integer_recursionsecondhsf_positive)) /\ exists ff_q_mce_mdr_integer_recursionsecondhsf_positive_start. ff_u_mce_mdr_integer_recursionsecondhsf_positive = ff_q_mce_mdr_integer_recursionsecondhsf_positive_start * S ((S (0)) * ff_v_mce_mdr_integer_recursionsecondhsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_integer_recursionsecondhsf_positive_terminal. ff_h_mce_mdr_integer_recursionsecondhsf_positive_terminal + S (mdr_p_integer_recursionsecondh) = S ((S ((S (mdr_q_integer_recursionsecondhs)))) * ff_v_mce_mdr_integer_recursionsecondhsf_positive)) /\ exists ff_q_mce_mdr_integer_recursionsecondhsf_positive_terminal. ff_u_mce_mdr_integer_recursionsecondhsf_positive = ff_q_mce_mdr_integer_recursionsecondhsf_positive_terminal * S ((S ((S (mdr_q_integer_recursionsecondhs)))) * ff_v_mce_mdr_integer_recursionsecondhsf_positive) + (mdr_p_integer_recursionsecondh))) /\ forall ff_i_mce_mdr_integer_recursionsecondhsf_positive. (exists ff_lt_mce_mdr_integer_recursionsecondhsf_positive_bound. ff_lt_mce_mdr_integer_recursionsecondhsf_positive_bound + S ff_i_mce_mdr_integer_recursionsecondhsf_positive = (S (mdr_q_integer_recursionsecondhs))) -> exists ff_a_mce_mdr_integer_recursionsecondhsf_positive ff_r_mce_mdr_integer_recursionsecondhsf_positive ff_s_mce_mdr_integer_recursionsecondhsf_positive. ((((exists ff_h_mce_mdr_integer_recursionsecondhsf_positive_summand. ff_h_mce_mdr_integer_recursionsecondhsf_positive_summand + S (ff_a_mce_mdr_integer_recursionsecondhsf_positive) = S ((S (ff_i_mce_mdr_integer_recursionsecondhsf_positive)) * ff_uc_mce_fold_mdr_integer_recursionsecondhsf)) /\ exists ff_q_mce_mdr_integer_recursionsecondhsf_positive_summand. ff_ub_mce_fold_mdr_integer_recursionsecondhsf = ff_q_mce_mdr_integer_recursionsecondhsf_positive_summand * S ((S (ff_i_mce_mdr_integer_recursionsecondhsf_positive)) * ff_uc_mce_fold_mdr_integer_recursionsecondhsf) + (ff_a_mce_mdr_integer_recursionsecondhsf_positive))) /\ ((((exists ff_h_mce_mdr_integer_recursionsecondhsf_positive_partial. ff_h_mce_mdr_integer_recursionsecondhsf_positive_partial + S (ff_r_mce_mdr_integer_recursionsecondhsf_positive) = S ((S (ff_i_mce_mdr_integer_recursionsecondhsf_positive)) * ff_v_mce_mdr_integer_recursionsecondhsf_positive)) /\ exists ff_q_mce_mdr_integer_recursionsecondhsf_positive_partial. ff_u_mce_mdr_integer_recursionsecondhsf_positive = ff_q_mce_mdr_integer_recursionsecondhsf_positive_partial * S ((S (ff_i_mce_mdr_integer_recursionsecondhsf_positive)) * ff_v_mce_mdr_integer_recursionsecondhsf_positive) + (ff_r_mce_mdr_integer_recursionsecondhsf_positive))) /\ ((((exists ff_h_mce_mdr_integer_recursionsecondhsf_positive_successor. ff_h_mce_mdr_integer_recursionsecondhsf_positive_successor + S (ff_s_mce_mdr_integer_recursionsecondhsf_positive) = S ((S (S ff_i_mce_mdr_integer_recursionsecondhsf_positive)) * ff_v_mce_mdr_integer_recursionsecondhsf_positive)) /\ exists ff_q_mce_mdr_integer_recursionsecondhsf_positive_successor. ff_u_mce_mdr_integer_recursionsecondhsf_positive = ff_q_mce_mdr_integer_recursionsecondhsf_positive_successor * S ((S (S ff_i_mce_mdr_integer_recursionsecondhsf_positive)) * ff_v_mce_mdr_integer_recursionsecondhsf_positive) + (ff_s_mce_mdr_integer_recursionsecondhsf_positive))) /\ ff_s_mce_mdr_integer_recursionsecondhsf_positive = ff_r_mce_mdr_integer_recursionsecondhsf_positive + ff_a_mce_mdr_integer_recursionsecondhsf_positive)))))) /\ (exists ff_u_mce_mdr_integer_recursionsecondhsf_negative ff_v_mce_mdr_integer_recursionsecondhsf_negative. ((((exists ff_h_mce_mdr_integer_recursionsecondhsf_negative_start. ff_h_mce_mdr_integer_recursionsecondhsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_integer_recursionsecondhsf_negative)) /\ exists ff_q_mce_mdr_integer_recursionsecondhsf_negative_start. ff_u_mce_mdr_integer_recursionsecondhsf_negative = ff_q_mce_mdr_integer_recursionsecondhsf_negative_start * S ((S (0)) * ff_v_mce_mdr_integer_recursionsecondhsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_integer_recursionsecondhsf_negative_terminal. ff_h_mce_mdr_integer_recursionsecondhsf_negative_terminal + S (mdr_n_integer_recursionsecondh) = S ((S ((S (mdr_q_integer_recursionsecondhs)))) * ff_v_mce_mdr_integer_recursionsecondhsf_negative)) /\ exists ff_q_mce_mdr_integer_recursionsecondhsf_negative_terminal. ff_u_mce_mdr_integer_recursionsecondhsf_negative = ff_q_mce_mdr_integer_recursionsecondhsf_negative_terminal * S ((S ((S (mdr_q_integer_recursionsecondhs)))) * ff_v_mce_mdr_integer_recursionsecondhsf_negative) + (mdr_n_integer_recursionsecondh))) /\ forall ff_i_mce_mdr_integer_recursionsecondhsf_negative. (exists ff_lt_mce_mdr_integer_recursionsecondhsf_negative_bound. ff_lt_mce_mdr_integer_recursionsecondhsf_negative_bound + S ff_i_mce_mdr_integer_recursionsecondhsf_negative = (S (mdr_q_integer_recursionsecondhs))) -> exists ff_a_mce_mdr_integer_recursionsecondhsf_negative ff_r_mce_mdr_integer_recursionsecondhsf_negative ff_s_mce_mdr_integer_recursionsecondhsf_negative. ((((exists ff_h_mce_mdr_integer_recursionsecondhsf_negative_summand. ff_h_mce_mdr_integer_recursionsecondhsf_negative_summand + S (ff_a_mce_mdr_integer_recursionsecondhsf_negative) = S ((S (ff_i_mce_mdr_integer_recursionsecondhsf_negative)) * ff_vc_mce_fold_mdr_integer_recursionsecondhsf)) /\ exists ff_q_mce_mdr_integer_recursionsecondhsf_negative_summand. ff_vb_mce_fold_mdr_integer_recursionsecondhsf = ff_q_mce_mdr_integer_recursionsecondhsf_negative_summand * S ((S (ff_i_mce_mdr_integer_recursionsecondhsf_negative)) * ff_vc_mce_fold_mdr_integer_recursionsecondhsf) + (ff_a_mce_mdr_integer_recursionsecondhsf_negative))) /\ ((((exists ff_h_mce_mdr_integer_recursionsecondhsf_negative_partial. ff_h_mce_mdr_integer_recursionsecondhsf_negative_partial + S (ff_r_mce_mdr_integer_recursionsecondhsf_negative) = S ((S (ff_i_mce_mdr_integer_recursionsecondhsf_negative)) * ff_v_mce_mdr_integer_recursionsecondhsf_negative)) /\ exists ff_q_mce_mdr_integer_recursionsecondhsf_negative_partial. ff_u_mce_mdr_integer_recursionsecondhsf_negative = ff_q_mce_mdr_integer_recursionsecondhsf_negative_partial * S ((S (ff_i_mce_mdr_integer_recursionsecondhsf_negative)) * ff_v_mce_mdr_integer_recursionsecondhsf_negative) + (ff_r_mce_mdr_integer_recursionsecondhsf_negative))) /\ ((((exists ff_h_mce_mdr_integer_recursionsecondhsf_negative_successor. ff_h_mce_mdr_integer_recursionsecondhsf_negative_successor + S (ff_s_mce_mdr_integer_recursionsecondhsf_negative) = S ((S (S ff_i_mce_mdr_integer_recursionsecondhsf_negative)) * ff_v_mce_mdr_integer_recursionsecondhsf_negative)) /\ exists ff_q_mce_mdr_integer_recursionsecondhsf_negative_successor. ff_u_mce_mdr_integer_recursionsecondhsf_negative = ff_q_mce_mdr_integer_recursionsecondhsf_negative_successor * S ((S (S ff_i_mce_mdr_integer_recursionsecondhsf_negative)) * ff_v_mce_mdr_integer_recursionsecondhsf_negative) + (ff_s_mce_mdr_integer_recursionsecondhsf_negative))) /\ ff_s_mce_mdr_integer_recursionsecondhsf_negative = ff_r_mce_mdr_integer_recursionsecondhsf_negative + ff_a_mce_mdr_integer_recursionsecondhsf_negative))))))))))))))) /\ ((exists mdr_gap_integer_recursionsecondi. mdr_gap_integer_recursionsecondi + S (mdr_i_integer_recursionsecond) = (mdr_l_integer_recursionsecond)) /\ (exists mdr_z_integer_recursionsecondr. ((exists mdr_a_integer_recursionsecondrc mdr_b_integer_recursionsecondrc mdr_c_integer_recursionsecondrc mdr_e_integer_recursionsecondrc mdr_f_integer_recursionsecondrc. ((mdr_a_integer_recursionsecondrc = ((q) + (mdr_eb_integer_recursion)) * S ((q) + (mdr_eb_integer_recursion)) + ((mdr_eb_integer_recursion) + (mdr_eb_integer_recursion))) /\ ((mdr_b_integer_recursionsecondrc = ((mdr_ec_integer_recursion) + (mdr_fb_integer_recursion)) * S ((mdr_ec_integer_recursion) + (mdr_fb_integer_recursion)) + ((mdr_fb_integer_recursion) + (mdr_fb_integer_recursion))) /\ ((mdr_c_integer_recursionsecondrc = ((mdr_a_integer_recursionsecondrc) + (mdr_b_integer_recursionsecondrc)) * S ((mdr_a_integer_recursionsecondrc) + (mdr_b_integer_recursionsecondrc)) + ((mdr_b_integer_recursionsecondrc) + (mdr_b_integer_recursionsecondrc))) /\ ((mdr_e_integer_recursionsecondrc = ((mdr_P_integer_recursion) + (mdr_N_integer_recursion)) * S ((mdr_P_integer_recursion) + (mdr_N_integer_recursion)) + ((mdr_N_integer_recursion) + (mdr_N_integer_recursion))) /\ ((mdr_f_integer_recursionsecondrc = ((mdr_fc_integer_recursion) + (mdr_e_integer_recursionsecondrc)) * S ((mdr_fc_integer_recursion) + (mdr_e_integer_recursionsecondrc)) + ((mdr_e_integer_recursionsecondrc) + (mdr_e_integer_recursionsecondrc))) /\ ((mdr_z_integer_recursionsecondr) = ((mdr_c_integer_recursionsecondrc) + (mdr_f_integer_recursionsecondrc)) * S ((mdr_c_integer_recursionsecondrc) + (mdr_f_integer_recursionsecondrc)) + ((mdr_f_integer_recursionsecondrc) + (mdr_f_integer_recursionsecondrc))))))))) /\ (((exists ff_h_mdr_integer_recursionsecondrb. ff_h_mdr_integer_recursionsecondrb + S (mdr_z_integer_recursionsecondr) = S ((S (mdr_i_integer_recursionsecond)) * mdr_c_integer_recursionsecond)) /\ exists ff_q_mdr_integer_recursionsecondrb. mdr_b_integer_recursionsecond = ff_q_mdr_integer_recursionsecondrb * S ((S (mdr_i_integer_recursionsecond)) * mdr_c_integer_recursionsecond) + (mdr_z_integer_recursionsecondr)))))))) -> mdr_p_integer_recursion + mdr_N_integer_recursion = mdr_P_integer_recursion + mdr_n_integer_recursion) -> (forall ics_index_integer_cofactor_parents ics_value0_integer_cofactor_parents ics_value1_integer_cofactor_parents ics_value2_integer_cofactor_parents ics_value3_integer_cofactor_parents. (exists ics_gap_integer_cofactor_parents_bound. ics_gap_integer_cofactor_parents_bound + S (ics_index_integer_cofactor_parents) = ((S q) * (S q))) -> (((exists fs_h_ics_integer_cofactor_parents_at0. fs_h_ics_integer_cofactor_parents_at0 + S (ics_value0_integer_cofactor_parents) = S ((S (ics_index_integer_cofactor_parents)) * ac)) /\ exists fs_q_ics_integer_cofactor_parents_at0. ab = fs_q_ics_integer_cofactor_parents_at0 * S ((S (ics_index_integer_cofactor_parents)) * ac) + (ics_value0_integer_cofactor_parents))) -> (((exists fs_h_ics_integer_cofactor_parents_at1. fs_h_ics_integer_cofactor_parents_at1 + S (ics_value1_integer_cofactor_parents) = S ((S (ics_index_integer_cofactor_parents)) * bc)) /\ exists fs_q_ics_integer_cofactor_parents_at1. bb = fs_q_ics_integer_cofactor_parents_at1 * S ((S (ics_index_integer_cofactor_parents)) * bc) + (ics_value1_integer_cofactor_parents))) -> (((exists fs_h_ics_integer_cofactor_parents_at2. fs_h_ics_integer_cofactor_parents_at2 + S (ics_value2_integer_cofactor_parents) = S ((S (ics_index_integer_cofactor_parents)) * ec)) /\ exists fs_q_ics_integer_cofactor_parents_at2. eb = fs_q_ics_integer_cofactor_parents_at2 * S ((S (ics_index_integer_cofactor_parents)) * ec) + (ics_value2_integer_cofactor_parents))) -> (((exists fs_h_ics_integer_cofactor_parents_at3. fs_h_ics_integer_cofactor_parents_at3 + S (ics_value3_integer_cofactor_parents) = S ((S (ics_index_integer_cofactor_parents)) * fc)) /\ exists fs_q_ics_integer_cofactor_parents_at3. fb = fs_q_ics_integer_cofactor_parents_at3 * S ((S (ics_index_integer_cofactor_parents)) * fc) + (ics_value3_integer_cofactor_parents))) -> ics_value0_integer_cofactor_parents + ics_value3_integer_cofactor_parents = ics_value2_integer_cofactor_parents + ics_value1_integer_cofactor_parents) -> (forall mdr_j_integer_cofactor_first. (exists mdr_gap_integer_cofactor_firstj. mdr_gap_integer_cofactor_firstj + S (mdr_j_integer_cofactor_first) = (S (q))) -> exists mdr_up_integer_cofactor_first mdr_us_integer_cofactor_first mdr_un_integer_cofactor_first mdr_ut_integer_cofactor_first mdr_p_integer_cofactor_first mdr_n_integer_cofactor_first. ((((forall ff_index_mdm_prefix_mdr_integer_cofactor_firstm_positive. (exists ff_gap_mdm_lt_mdr_integer_cofactor_firstm_positive_index_bound. ff_gap_mdm_lt_mdr_integer_cofactor_firstm_positive_index_bound + S (ff_index_mdm_prefix_mdr_integer_cofactor_firstm_positive) = ((q) * (q))) -> exists ff_row_mdm_prefix_mdr_integer_cofactor_firstm_positive ff_column_mdm_prefix_mdr_integer_cofactor_firstm_positive ff_value_mdm_prefix_mdr_integer_cofactor_firstm_positive. (ff_index_mdm_prefix_mdr_integer_cofactor_firstm_positive = (q) * ff_row_mdm_prefix_mdr_integer_cofactor_firstm_positive + ff_column_mdm_prefix_mdr_integer_cofactor_firstm_positive /\ ((exists ff_gap_mdm_lt_mdr_integer_cofactor_firstm_positive_column_bound. ff_gap_mdm_lt_mdr_integer_cofactor_firstm_positive_column_bound + S (ff_column_mdm_prefix_mdr_integer_cofactor_firstm_positive) = (q)) /\ ((exists ff_row_mdm_cell_mdr_integer_cofactor_firstm_positive_cell ff_column_mdm_cell_mdr_integer_cofactor_firstm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_integer_cofactor_firstm_positive_cell_row_before. ff_gap_mdm_lt_mdr_integer_cofactor_firstm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_integer_cofactor_firstm_positive) = (0)) /\ ff_row_mdm_cell_mdr_integer_cofactor_firstm_positive_cell = ff_row_mdm_prefix_mdr_integer_cofactor_firstm_positive) \/ ((exists ff_gap_mdm_le_mdr_integer_cofactor_firstm_positive_cell_row_after. ff_gap_mdm_le_mdr_integer_cofactor_firstm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_integer_cofactor_firstm_positive)) /\ ff_row_mdm_cell_mdr_integer_cofactor_firstm_positive_cell = S ff_row_mdm_prefix_mdr_integer_cofactor_firstm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_integer_cofactor_firstm_positive_cell_column_before. ff_gap_mdm_lt_mdr_integer_cofactor_firstm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_integer_cofactor_firstm_positive) = (mdr_j_integer_cofactor_first)) /\ ff_column_mdm_cell_mdr_integer_cofactor_firstm_positive_cell = ff_column_mdm_prefix_mdr_integer_cofactor_firstm_positive) \/ ((exists ff_gap_mdm_le_mdr_integer_cofactor_firstm_positive_cell_column_after. ff_gap_mdm_le_mdr_integer_cofactor_firstm_positive_cell_column_after + (mdr_j_integer_cofactor_first) = (ff_column_mdm_prefix_mdr_integer_cofactor_firstm_positive)) /\ ff_column_mdm_cell_mdr_integer_cofactor_firstm_positive_cell = S ff_column_mdm_prefix_mdr_integer_cofactor_firstm_positive))) /\ (((exists ff_h_mdm_mdr_integer_cofactor_firstm_positive_cell_source. ff_h_mdm_mdr_integer_cofactor_firstm_positive_cell_source + S (ff_value_mdm_prefix_mdr_integer_cofactor_firstm_positive) = S ((S ((ff_row_mdm_cell_mdr_integer_cofactor_firstm_positive_cell) * (S (q)) + (ff_column_mdm_cell_mdr_integer_cofactor_firstm_positive_cell))) * ac)) /\ exists ff_q_mdm_mdr_integer_cofactor_firstm_positive_cell_source. ab = ff_q_mdm_mdr_integer_cofactor_firstm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_integer_cofactor_firstm_positive_cell) * (S (q)) + (ff_column_mdm_cell_mdr_integer_cofactor_firstm_positive_cell))) * ac) + (ff_value_mdm_prefix_mdr_integer_cofactor_firstm_positive)))))) /\ (((exists ff_h_mdm_mdr_integer_cofactor_firstm_positive_target. ff_h_mdm_mdr_integer_cofactor_firstm_positive_target + S (ff_value_mdm_prefix_mdr_integer_cofactor_firstm_positive) = S ((S (ff_index_mdm_prefix_mdr_integer_cofactor_firstm_positive)) * mdr_us_integer_cofactor_first)) /\ exists ff_q_mdm_mdr_integer_cofactor_firstm_positive_target. mdr_up_integer_cofactor_first = ff_q_mdm_mdr_integer_cofactor_firstm_positive_target * S ((S (ff_index_mdm_prefix_mdr_integer_cofactor_firstm_positive)) * mdr_us_integer_cofactor_first) + (ff_value_mdm_prefix_mdr_integer_cofactor_firstm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_integer_cofactor_firstm_negative. (exists ff_gap_mdm_lt_mdr_integer_cofactor_firstm_negative_index_bound. ff_gap_mdm_lt_mdr_integer_cofactor_firstm_negative_index_bound + S (ff_index_mdm_prefix_mdr_integer_cofactor_firstm_negative) = ((q) * (q))) -> exists ff_row_mdm_prefix_mdr_integer_cofactor_firstm_negative ff_column_mdm_prefix_mdr_integer_cofactor_firstm_negative ff_value_mdm_prefix_mdr_integer_cofactor_firstm_negative. (ff_index_mdm_prefix_mdr_integer_cofactor_firstm_negative = (q) * ff_row_mdm_prefix_mdr_integer_cofactor_firstm_negative + ff_column_mdm_prefix_mdr_integer_cofactor_firstm_negative /\ ((exists ff_gap_mdm_lt_mdr_integer_cofactor_firstm_negative_column_bound. ff_gap_mdm_lt_mdr_integer_cofactor_firstm_negative_column_bound + S (ff_column_mdm_prefix_mdr_integer_cofactor_firstm_negative) = (q)) /\ ((exists ff_row_mdm_cell_mdr_integer_cofactor_firstm_negative_cell ff_column_mdm_cell_mdr_integer_cofactor_firstm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_integer_cofactor_firstm_negative_cell_row_before. ff_gap_mdm_lt_mdr_integer_cofactor_firstm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_integer_cofactor_firstm_negative) = (0)) /\ ff_row_mdm_cell_mdr_integer_cofactor_firstm_negative_cell = ff_row_mdm_prefix_mdr_integer_cofactor_firstm_negative) \/ ((exists ff_gap_mdm_le_mdr_integer_cofactor_firstm_negative_cell_row_after. ff_gap_mdm_le_mdr_integer_cofactor_firstm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_integer_cofactor_firstm_negative)) /\ ff_row_mdm_cell_mdr_integer_cofactor_firstm_negative_cell = S ff_row_mdm_prefix_mdr_integer_cofactor_firstm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_integer_cofactor_firstm_negative_cell_column_before. ff_gap_mdm_lt_mdr_integer_cofactor_firstm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_integer_cofactor_firstm_negative) = (mdr_j_integer_cofactor_first)) /\ ff_column_mdm_cell_mdr_integer_cofactor_firstm_negative_cell = ff_column_mdm_prefix_mdr_integer_cofactor_firstm_negative) \/ ((exists ff_gap_mdm_le_mdr_integer_cofactor_firstm_negative_cell_column_after. ff_gap_mdm_le_mdr_integer_cofactor_firstm_negative_cell_column_after + (mdr_j_integer_cofactor_first) = (ff_column_mdm_prefix_mdr_integer_cofactor_firstm_negative)) /\ ff_column_mdm_cell_mdr_integer_cofactor_firstm_negative_cell = S ff_column_mdm_prefix_mdr_integer_cofactor_firstm_negative))) /\ (((exists ff_h_mdm_mdr_integer_cofactor_firstm_negative_cell_source. ff_h_mdm_mdr_integer_cofactor_firstm_negative_cell_source + S (ff_value_mdm_prefix_mdr_integer_cofactor_firstm_negative) = S ((S ((ff_row_mdm_cell_mdr_integer_cofactor_firstm_negative_cell) * (S (q)) + (ff_column_mdm_cell_mdr_integer_cofactor_firstm_negative_cell))) * bc)) /\ exists ff_q_mdm_mdr_integer_cofactor_firstm_negative_cell_source. bb = ff_q_mdm_mdr_integer_cofactor_firstm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_integer_cofactor_firstm_negative_cell) * (S (q)) + (ff_column_mdm_cell_mdr_integer_cofactor_firstm_negative_cell))) * bc) + (ff_value_mdm_prefix_mdr_integer_cofactor_firstm_negative)))))) /\ (((exists ff_h_mdm_mdr_integer_cofactor_firstm_negative_target. ff_h_mdm_mdr_integer_cofactor_firstm_negative_target + S (ff_value_mdm_prefix_mdr_integer_cofactor_firstm_negative) = S ((S (ff_index_mdm_prefix_mdr_integer_cofactor_firstm_negative)) * mdr_ut_integer_cofactor_first)) /\ exists ff_q_mdm_mdr_integer_cofactor_firstm_negative_target. mdr_un_integer_cofactor_first = ff_q_mdm_mdr_integer_cofactor_firstm_negative_target * S ((S (ff_index_mdm_prefix_mdr_integer_cofactor_firstm_negative)) * mdr_ut_integer_cofactor_first) + (ff_value_mdm_prefix_mdr_integer_cofactor_firstm_negative))))))))) /\ ((exists mdr_b_integer_cofactor_firstd mdr_c_integer_cofactor_firstd mdr_l_integer_cofactor_firstd mdr_i_integer_cofactor_firstd. ((forall mdr_i_integer_cofactor_firstdh. (exists mdr_gap_integer_cofactor_firstdhi. mdr_gap_integer_cofactor_firstdhi + S (mdr_i_integer_cofactor_firstdh) = (mdr_l_integer_cofactor_firstd)) -> exists mdr_d_integer_cofactor_firstdh mdr_pb_integer_cofactor_firstdh mdr_pc_integer_cofactor_firstdh mdr_nb_integer_cofactor_firstdh mdr_nc_integer_cofactor_firstdh mdr_p_integer_cofactor_firstdh mdr_n_integer_cofactor_firstdh. ((exists mdr_z_integer_cofactor_firstdhr. ((exists mdr_a_integer_cofactor_firstdhrc mdr_b_integer_cofactor_firstdhrc mdr_c_integer_cofactor_firstdhrc mdr_e_integer_cofactor_firstdhrc mdr_f_integer_cofactor_firstdhrc. ((mdr_a_integer_cofactor_firstdhrc = ((mdr_d_integer_cofactor_firstdh) + (mdr_pb_integer_cofactor_firstdh)) * S ((mdr_d_integer_cofactor_firstdh) + (mdr_pb_integer_cofactor_firstdh)) + ((mdr_pb_integer_cofactor_firstdh) + (mdr_pb_integer_cofactor_firstdh))) /\ ((mdr_b_integer_cofactor_firstdhrc = ((mdr_pc_integer_cofactor_firstdh) + (mdr_nb_integer_cofactor_firstdh)) * S ((mdr_pc_integer_cofactor_firstdh) + (mdr_nb_integer_cofactor_firstdh)) + ((mdr_nb_integer_cofactor_firstdh) + (mdr_nb_integer_cofactor_firstdh))) /\ ((mdr_c_integer_cofactor_firstdhrc = ((mdr_a_integer_cofactor_firstdhrc) + (mdr_b_integer_cofactor_firstdhrc)) * S ((mdr_a_integer_cofactor_firstdhrc) + (mdr_b_integer_cofactor_firstdhrc)) + ((mdr_b_integer_cofactor_firstdhrc) + (mdr_b_integer_cofactor_firstdhrc))) /\ ((mdr_e_integer_cofactor_firstdhrc = ((mdr_p_integer_cofactor_firstdh) + (mdr_n_integer_cofactor_firstdh)) * S ((mdr_p_integer_cofactor_firstdh) + (mdr_n_integer_cofactor_firstdh)) + ((mdr_n_integer_cofactor_firstdh) + (mdr_n_integer_cofactor_firstdh))) /\ ((mdr_f_integer_cofactor_firstdhrc = ((mdr_nc_integer_cofactor_firstdh) + (mdr_e_integer_cofactor_firstdhrc)) * S ((mdr_nc_integer_cofactor_firstdh) + (mdr_e_integer_cofactor_firstdhrc)) + ((mdr_e_integer_cofactor_firstdhrc) + (mdr_e_integer_cofactor_firstdhrc))) /\ ((mdr_z_integer_cofactor_firstdhr) = ((mdr_c_integer_cofactor_firstdhrc) + (mdr_f_integer_cofactor_firstdhrc)) * S ((mdr_c_integer_cofactor_firstdhrc) + (mdr_f_integer_cofactor_firstdhrc)) + ((mdr_f_integer_cofactor_firstdhrc) + (mdr_f_integer_cofactor_firstdhrc))))))))) /\ (((exists ff_h_mdr_integer_cofactor_firstdhrb. ff_h_mdr_integer_cofactor_firstdhrb + S (mdr_z_integer_cofactor_firstdhr) = S ((S (mdr_i_integer_cofactor_firstdh)) * mdr_c_integer_cofactor_firstd)) /\ exists ff_q_mdr_integer_cofactor_firstdhrb. mdr_b_integer_cofactor_firstd = ff_q_mdr_integer_cofactor_firstdhrb * S ((S (mdr_i_integer_cofactor_firstdh)) * mdr_c_integer_cofactor_firstd) + (mdr_z_integer_cofactor_firstdhr))))) /\ (((((mdr_d_integer_cofactor_firstdh) = 0) /\ (((mdr_p_integer_cofactor_firstdh) = 1) /\ ((mdr_n_integer_cofactor_firstdh) = 0))) \/ exists mdr_q_integer_cofactor_firstdhs mdr_eb_integer_cofactor_firstdhs mdr_ec_integer_cofactor_firstdhs mdr_fb_integer_cofactor_firstdhs mdr_fc_integer_cofactor_firstdhs. (((mdr_d_integer_cofactor_firstdh) = S (mdr_q_integer_cofactor_firstdhs)) /\ ((forall mdr_j_integer_cofactor_firstdhsc. (exists mdr_gap_integer_cofactor_firstdhscj. mdr_gap_integer_cofactor_firstdhscj + S (mdr_j_integer_cofactor_firstdhsc) = (S (mdr_q_integer_cofactor_firstdhs))) -> exists mdr_i_integer_cofactor_firstdhsc mdr_up_integer_cofactor_firstdhsc mdr_us_integer_cofactor_firstdhsc mdr_un_integer_cofactor_firstdhsc mdr_ut_integer_cofactor_firstdhsc mdr_p_integer_cofactor_firstdhsc mdr_n_integer_cofactor_firstdhsc. ((exists mdr_gap_integer_cofactor_firstdhsci. mdr_gap_integer_cofactor_firstdhsci + S (mdr_i_integer_cofactor_firstdhsc) = (mdr_i_integer_cofactor_firstdh)) /\ ((exists mdr_z_integer_cofactor_firstdhscr. ((exists mdr_a_integer_cofactor_firstdhscrc mdr_b_integer_cofactor_firstdhscrc mdr_c_integer_cofactor_firstdhscrc mdr_e_integer_cofactor_firstdhscrc mdr_f_integer_cofactor_firstdhscrc. ((mdr_a_integer_cofactor_firstdhscrc = ((mdr_q_integer_cofactor_firstdhs) + (mdr_up_integer_cofactor_firstdhsc)) * S ((mdr_q_integer_cofactor_firstdhs) + (mdr_up_integer_cofactor_firstdhsc)) + ((mdr_up_integer_cofactor_firstdhsc) + (mdr_up_integer_cofactor_firstdhsc))) /\ ((mdr_b_integer_cofactor_firstdhscrc = ((mdr_us_integer_cofactor_firstdhsc) + (mdr_un_integer_cofactor_firstdhsc)) * S ((mdr_us_integer_cofactor_firstdhsc) + (mdr_un_integer_cofactor_firstdhsc)) + ((mdr_un_integer_cofactor_firstdhsc) + (mdr_un_integer_cofactor_firstdhsc))) /\ ((mdr_c_integer_cofactor_firstdhscrc = ((mdr_a_integer_cofactor_firstdhscrc) + (mdr_b_integer_cofactor_firstdhscrc)) * S ((mdr_a_integer_cofactor_firstdhscrc) + (mdr_b_integer_cofactor_firstdhscrc)) + ((mdr_b_integer_cofactor_firstdhscrc) + (mdr_b_integer_cofactor_firstdhscrc))) /\ ((mdr_e_integer_cofactor_firstdhscrc = ((mdr_p_integer_cofactor_firstdhsc) + (mdr_n_integer_cofactor_firstdhsc)) * S ((mdr_p_integer_cofactor_firstdhsc) + (mdr_n_integer_cofactor_firstdhsc)) + ((mdr_n_integer_cofactor_firstdhsc) + (mdr_n_integer_cofactor_firstdhsc))) /\ ((mdr_f_integer_cofactor_firstdhscrc = ((mdr_ut_integer_cofactor_firstdhsc) + (mdr_e_integer_cofactor_firstdhscrc)) * S ((mdr_ut_integer_cofactor_firstdhsc) + (mdr_e_integer_cofactor_firstdhscrc)) + ((mdr_e_integer_cofactor_firstdhscrc) + (mdr_e_integer_cofactor_firstdhscrc))) /\ ((mdr_z_integer_cofactor_firstdhscr) = ((mdr_c_integer_cofactor_firstdhscrc) + (mdr_f_integer_cofactor_firstdhscrc)) * S ((mdr_c_integer_cofactor_firstdhscrc) + (mdr_f_integer_cofactor_firstdhscrc)) + ((mdr_f_integer_cofactor_firstdhscrc) + (mdr_f_integer_cofactor_firstdhscrc))))))))) /\ (((exists ff_h_mdr_integer_cofactor_firstdhscrb. ff_h_mdr_integer_cofactor_firstdhscrb + S (mdr_z_integer_cofactor_firstdhscr) = S ((S (mdr_i_integer_cofactor_firstdhsc)) * mdr_c_integer_cofactor_firstd)) /\ exists ff_q_mdr_integer_cofactor_firstdhscrb. mdr_b_integer_cofactor_firstd = ff_q_mdr_integer_cofactor_firstdhscrb * S ((S (mdr_i_integer_cofactor_firstdhsc)) * mdr_c_integer_cofactor_firstd) + (mdr_z_integer_cofactor_firstdhscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_integer_cofactor_firstdhscm_positive. (exists ff_gap_mdm_lt_mdr_integer_cofactor_firstdhscm_positive_index_bound. ff_gap_mdm_lt_mdr_integer_cofactor_firstdhscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_integer_cofactor_firstdhscm_positive) = ((mdr_q_integer_cofactor_firstdhs) * (mdr_q_integer_cofactor_firstdhs))) -> exists ff_row_mdm_prefix_mdr_integer_cofactor_firstdhscm_positive ff_column_mdm_prefix_mdr_integer_cofactor_firstdhscm_positive ff_value_mdm_prefix_mdr_integer_cofactor_firstdhscm_positive. (ff_index_mdm_prefix_mdr_integer_cofactor_firstdhscm_positive = (mdr_q_integer_cofactor_firstdhs) * ff_row_mdm_prefix_mdr_integer_cofactor_firstdhscm_positive + ff_column_mdm_prefix_mdr_integer_cofactor_firstdhscm_positive /\ ((exists ff_gap_mdm_lt_mdr_integer_cofactor_firstdhscm_positive_column_bound. ff_gap_mdm_lt_mdr_integer_cofactor_firstdhscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_integer_cofactor_firstdhscm_positive) = (mdr_q_integer_cofactor_firstdhs)) /\ ((exists ff_row_mdm_cell_mdr_integer_cofactor_firstdhscm_positive_cell ff_column_mdm_cell_mdr_integer_cofactor_firstdhscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_integer_cofactor_firstdhscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_integer_cofactor_firstdhscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_integer_cofactor_firstdhscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_integer_cofactor_firstdhscm_positive_cell = ff_row_mdm_prefix_mdr_integer_cofactor_firstdhscm_positive) \/ ((exists ff_gap_mdm_le_mdr_integer_cofactor_firstdhscm_positive_cell_row_after. ff_gap_mdm_le_mdr_integer_cofactor_firstdhscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_integer_cofactor_firstdhscm_positive)) /\ ff_row_mdm_cell_mdr_integer_cofactor_firstdhscm_positive_cell = S ff_row_mdm_prefix_mdr_integer_cofactor_firstdhscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_integer_cofactor_firstdhscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_integer_cofactor_firstdhscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_integer_cofactor_firstdhscm_positive) = (mdr_j_integer_cofactor_firstdhsc)) /\ ff_column_mdm_cell_mdr_integer_cofactor_firstdhscm_positive_cell = ff_column_mdm_prefix_mdr_integer_cofactor_firstdhscm_positive) \/ ((exists ff_gap_mdm_le_mdr_integer_cofactor_firstdhscm_positive_cell_column_after. ff_gap_mdm_le_mdr_integer_cofactor_firstdhscm_positive_cell_column_after + (mdr_j_integer_cofactor_firstdhsc) = (ff_column_mdm_prefix_mdr_integer_cofactor_firstdhscm_positive)) /\ ff_column_mdm_cell_mdr_integer_cofactor_firstdhscm_positive_cell = S ff_column_mdm_prefix_mdr_integer_cofactor_firstdhscm_positive))) /\ (((exists ff_h_mdm_mdr_integer_cofactor_firstdhscm_positive_cell_source. ff_h_mdm_mdr_integer_cofactor_firstdhscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_integer_cofactor_firstdhscm_positive) = S ((S ((ff_row_mdm_cell_mdr_integer_cofactor_firstdhscm_positive_cell) * (S (mdr_q_integer_cofactor_firstdhs)) + (ff_column_mdm_cell_mdr_integer_cofactor_firstdhscm_positive_cell))) * mdr_pc_integer_cofactor_firstdh)) /\ exists ff_q_mdm_mdr_integer_cofactor_firstdhscm_positive_cell_source. mdr_pb_integer_cofactor_firstdh = ff_q_mdm_mdr_integer_cofactor_firstdhscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_integer_cofactor_firstdhscm_positive_cell) * (S (mdr_q_integer_cofactor_firstdhs)) + (ff_column_mdm_cell_mdr_integer_cofactor_firstdhscm_positive_cell))) * mdr_pc_integer_cofactor_firstdh) + (ff_value_mdm_prefix_mdr_integer_cofactor_firstdhscm_positive)))))) /\ (((exists ff_h_mdm_mdr_integer_cofactor_firstdhscm_positive_target. ff_h_mdm_mdr_integer_cofactor_firstdhscm_positive_target + S (ff_value_mdm_prefix_mdr_integer_cofactor_firstdhscm_positive) = S ((S (ff_index_mdm_prefix_mdr_integer_cofactor_firstdhscm_positive)) * mdr_us_integer_cofactor_firstdhsc)) /\ exists ff_q_mdm_mdr_integer_cofactor_firstdhscm_positive_target. mdr_up_integer_cofactor_firstdhsc = ff_q_mdm_mdr_integer_cofactor_firstdhscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_integer_cofactor_firstdhscm_positive)) * mdr_us_integer_cofactor_firstdhsc) + (ff_value_mdm_prefix_mdr_integer_cofactor_firstdhscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_integer_cofactor_firstdhscm_negative. (exists ff_gap_mdm_lt_mdr_integer_cofactor_firstdhscm_negative_index_bound. ff_gap_mdm_lt_mdr_integer_cofactor_firstdhscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_integer_cofactor_firstdhscm_negative) = ((mdr_q_integer_cofactor_firstdhs) * (mdr_q_integer_cofactor_firstdhs))) -> exists ff_row_mdm_prefix_mdr_integer_cofactor_firstdhscm_negative ff_column_mdm_prefix_mdr_integer_cofactor_firstdhscm_negative ff_value_mdm_prefix_mdr_integer_cofactor_firstdhscm_negative. (ff_index_mdm_prefix_mdr_integer_cofactor_firstdhscm_negative = (mdr_q_integer_cofactor_firstdhs) * ff_row_mdm_prefix_mdr_integer_cofactor_firstdhscm_negative + ff_column_mdm_prefix_mdr_integer_cofactor_firstdhscm_negative /\ ((exists ff_gap_mdm_lt_mdr_integer_cofactor_firstdhscm_negative_column_bound. ff_gap_mdm_lt_mdr_integer_cofactor_firstdhscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_integer_cofactor_firstdhscm_negative) = (mdr_q_integer_cofactor_firstdhs)) /\ ((exists ff_row_mdm_cell_mdr_integer_cofactor_firstdhscm_negative_cell ff_column_mdm_cell_mdr_integer_cofactor_firstdhscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_integer_cofactor_firstdhscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_integer_cofactor_firstdhscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_integer_cofactor_firstdhscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_integer_cofactor_firstdhscm_negative_cell = ff_row_mdm_prefix_mdr_integer_cofactor_firstdhscm_negative) \/ ((exists ff_gap_mdm_le_mdr_integer_cofactor_firstdhscm_negative_cell_row_after. ff_gap_mdm_le_mdr_integer_cofactor_firstdhscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_integer_cofactor_firstdhscm_negative)) /\ ff_row_mdm_cell_mdr_integer_cofactor_firstdhscm_negative_cell = S ff_row_mdm_prefix_mdr_integer_cofactor_firstdhscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_integer_cofactor_firstdhscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_integer_cofactor_firstdhscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_integer_cofactor_firstdhscm_negative) = (mdr_j_integer_cofactor_firstdhsc)) /\ ff_column_mdm_cell_mdr_integer_cofactor_firstdhscm_negative_cell = ff_column_mdm_prefix_mdr_integer_cofactor_firstdhscm_negative) \/ ((exists ff_gap_mdm_le_mdr_integer_cofactor_firstdhscm_negative_cell_column_after. ff_gap_mdm_le_mdr_integer_cofactor_firstdhscm_negative_cell_column_after + (mdr_j_integer_cofactor_firstdhsc) = (ff_column_mdm_prefix_mdr_integer_cofactor_firstdhscm_negative)) /\ ff_column_mdm_cell_mdr_integer_cofactor_firstdhscm_negative_cell = S ff_column_mdm_prefix_mdr_integer_cofactor_firstdhscm_negative))) /\ (((exists ff_h_mdm_mdr_integer_cofactor_firstdhscm_negative_cell_source. ff_h_mdm_mdr_integer_cofactor_firstdhscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_integer_cofactor_firstdhscm_negative) = S ((S ((ff_row_mdm_cell_mdr_integer_cofactor_firstdhscm_negative_cell) * (S (mdr_q_integer_cofactor_firstdhs)) + (ff_column_mdm_cell_mdr_integer_cofactor_firstdhscm_negative_cell))) * mdr_nc_integer_cofactor_firstdh)) /\ exists ff_q_mdm_mdr_integer_cofactor_firstdhscm_negative_cell_source. mdr_nb_integer_cofactor_firstdh = ff_q_mdm_mdr_integer_cofactor_firstdhscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_integer_cofactor_firstdhscm_negative_cell) * (S (mdr_q_integer_cofactor_firstdhs)) + (ff_column_mdm_cell_mdr_integer_cofactor_firstdhscm_negative_cell))) * mdr_nc_integer_cofactor_firstdh) + (ff_value_mdm_prefix_mdr_integer_cofactor_firstdhscm_negative)))))) /\ (((exists ff_h_mdm_mdr_integer_cofactor_firstdhscm_negative_target. ff_h_mdm_mdr_integer_cofactor_firstdhscm_negative_target + S (ff_value_mdm_prefix_mdr_integer_cofactor_firstdhscm_negative) = S ((S (ff_index_mdm_prefix_mdr_integer_cofactor_firstdhscm_negative)) * mdr_ut_integer_cofactor_firstdhsc)) /\ exists ff_q_mdm_mdr_integer_cofactor_firstdhscm_negative_target. mdr_un_integer_cofactor_firstdhsc = ff_q_mdm_mdr_integer_cofactor_firstdhscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_integer_cofactor_firstdhscm_negative)) * mdr_ut_integer_cofactor_firstdhsc) + (ff_value_mdm_prefix_mdr_integer_cofactor_firstdhscm_negative))))))))) /\ ((((exists ff_h_mdr_integer_cofactor_firstdhscp. ff_h_mdr_integer_cofactor_firstdhscp + S (mdr_p_integer_cofactor_firstdhsc) = S ((S (mdr_j_integer_cofactor_firstdhsc)) * mdr_ec_integer_cofactor_firstdhs)) /\ exists ff_q_mdr_integer_cofactor_firstdhscp. mdr_eb_integer_cofactor_firstdhs = ff_q_mdr_integer_cofactor_firstdhscp * S ((S (mdr_j_integer_cofactor_firstdhsc)) * mdr_ec_integer_cofactor_firstdhs) + (mdr_p_integer_cofactor_firstdhsc))) /\ (((exists ff_h_mdr_integer_cofactor_firstdhscn. ff_h_mdr_integer_cofactor_firstdhscn + S (mdr_n_integer_cofactor_firstdhsc) = S ((S (mdr_j_integer_cofactor_firstdhsc)) * mdr_fc_integer_cofactor_firstdhs)) /\ exists ff_q_mdr_integer_cofactor_firstdhscn. mdr_fb_integer_cofactor_firstdhs = ff_q_mdr_integer_cofactor_firstdhscn * S ((S (mdr_j_integer_cofactor_firstdhsc)) * mdr_fc_integer_cofactor_firstdhs) + (mdr_n_integer_cofactor_firstdhsc)))))))) /\ (exists ff_ub_mce_fold_mdr_integer_cofactor_firstdhsf ff_uc_mce_fold_mdr_integer_cofactor_firstdhsf ff_vb_mce_fold_mdr_integer_cofactor_firstdhsf ff_vc_mce_fold_mdr_integer_cofactor_firstdhsf. ((forall ff_index_mce_alternating_mdr_integer_cofactor_firstdhsf_prefix. (exists ff_gap_mce_mdr_integer_cofactor_firstdhsf_prefix_index. ff_gap_mce_mdr_integer_cofactor_firstdhsf_prefix_index + S (ff_index_mce_alternating_mdr_integer_cofactor_firstdhsf_prefix) = (S (mdr_q_integer_cofactor_firstdhs))) -> exists ff_ap_mce_alternating_mdr_integer_cofactor_firstdhsf_prefix ff_an_mce_alternating_mdr_integer_cofactor_firstdhsf_prefix ff_bp_mce_alternating_mdr_integer_cofactor_firstdhsf_prefix ff_bn_mce_alternating_mdr_integer_cofactor_firstdhsf_prefix ff_p_mce_alternating_mdr_integer_cofactor_firstdhsf_prefix ff_n_mce_alternating_mdr_integer_cofactor_firstdhsf_prefix. ((((exists ff_h_mce_mdr_integer_cofactor_firstdhsf_prefix_ap. ff_h_mce_mdr_integer_cofactor_firstdhsf_prefix_ap + S (ff_ap_mce_alternating_mdr_integer_cofactor_firstdhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_integer_cofactor_firstdhsf_prefix)) * mdr_pc_integer_cofactor_firstdh)) /\ exists ff_q_mce_mdr_integer_cofactor_firstdhsf_prefix_ap. mdr_pb_integer_cofactor_firstdh = ff_q_mce_mdr_integer_cofactor_firstdhsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_integer_cofactor_firstdhsf_prefix)) * mdr_pc_integer_cofactor_firstdh) + (ff_ap_mce_alternating_mdr_integer_cofactor_firstdhsf_prefix))) /\ ((((exists ff_h_mce_mdr_integer_cofactor_firstdhsf_prefix_an. ff_h_mce_mdr_integer_cofactor_firstdhsf_prefix_an + S (ff_an_mce_alternating_mdr_integer_cofactor_firstdhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_integer_cofactor_firstdhsf_prefix)) * mdr_nc_integer_cofactor_firstdh)) /\ exists ff_q_mce_mdr_integer_cofactor_firstdhsf_prefix_an. mdr_nb_integer_cofactor_firstdh = ff_q_mce_mdr_integer_cofactor_firstdhsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_integer_cofactor_firstdhsf_prefix)) * mdr_nc_integer_cofactor_firstdh) + (ff_an_mce_alternating_mdr_integer_cofactor_firstdhsf_prefix))) /\ ((((exists ff_h_mce_mdr_integer_cofactor_firstdhsf_prefix_bp. ff_h_mce_mdr_integer_cofactor_firstdhsf_prefix_bp + S (ff_bp_mce_alternating_mdr_integer_cofactor_firstdhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_integer_cofactor_firstdhsf_prefix)) * mdr_ec_integer_cofactor_firstdhs)) /\ exists ff_q_mce_mdr_integer_cofactor_firstdhsf_prefix_bp. mdr_eb_integer_cofactor_firstdhs = ff_q_mce_mdr_integer_cofactor_firstdhsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_integer_cofactor_firstdhsf_prefix)) * mdr_ec_integer_cofactor_firstdhs) + (ff_bp_mce_alternating_mdr_integer_cofactor_firstdhsf_prefix))) /\ ((((exists ff_h_mce_mdr_integer_cofactor_firstdhsf_prefix_bn. ff_h_mce_mdr_integer_cofactor_firstdhsf_prefix_bn + S (ff_bn_mce_alternating_mdr_integer_cofactor_firstdhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_integer_cofactor_firstdhsf_prefix)) * mdr_fc_integer_cofactor_firstdhs)) /\ exists ff_q_mce_mdr_integer_cofactor_firstdhsf_prefix_bn. mdr_fb_integer_cofactor_firstdhs = ff_q_mce_mdr_integer_cofactor_firstdhsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_integer_cofactor_firstdhsf_prefix)) * mdr_fc_integer_cofactor_firstdhs) + (ff_bn_mce_alternating_mdr_integer_cofactor_firstdhsf_prefix))) /\ ((((exists ff_h_mce_mdr_integer_cofactor_firstdhsf_prefix_positive. ff_h_mce_mdr_integer_cofactor_firstdhsf_prefix_positive + S (ff_p_mce_alternating_mdr_integer_cofactor_firstdhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_integer_cofactor_firstdhsf_prefix)) * ff_uc_mce_fold_mdr_integer_cofactor_firstdhsf)) /\ exists ff_q_mce_mdr_integer_cofactor_firstdhsf_prefix_positive. ff_ub_mce_fold_mdr_integer_cofactor_firstdhsf = ff_q_mce_mdr_integer_cofactor_firstdhsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_integer_cofactor_firstdhsf_prefix)) * ff_uc_mce_fold_mdr_integer_cofactor_firstdhsf) + (ff_p_mce_alternating_mdr_integer_cofactor_firstdhsf_prefix))) /\ ((((exists ff_h_mce_mdr_integer_cofactor_firstdhsf_prefix_negative. ff_h_mce_mdr_integer_cofactor_firstdhsf_prefix_negative + S (ff_n_mce_alternating_mdr_integer_cofactor_firstdhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_integer_cofactor_firstdhsf_prefix)) * ff_vc_mce_fold_mdr_integer_cofactor_firstdhsf)) /\ exists ff_q_mce_mdr_integer_cofactor_firstdhsf_prefix_negative. ff_vb_mce_fold_mdr_integer_cofactor_firstdhsf = ff_q_mce_mdr_integer_cofactor_firstdhsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_integer_cofactor_firstdhsf_prefix)) * ff_vc_mce_fold_mdr_integer_cofactor_firstdhsf) + (ff_n_mce_alternating_mdr_integer_cofactor_firstdhsf_prefix))) /\ (((exists ff_even_mce_term_mdr_integer_cofactor_firstdhsf_prefix_term. ff_index_mce_alternating_mdr_integer_cofactor_firstdhsf_prefix = 2 * ff_even_mce_term_mdr_integer_cofactor_firstdhsf_prefix_term) /\ (ff_p_mce_alternating_mdr_integer_cofactor_firstdhsf_prefix = (ff_ap_mce_alternating_mdr_integer_cofactor_firstdhsf_prefix) * (ff_bp_mce_alternating_mdr_integer_cofactor_firstdhsf_prefix) + (ff_an_mce_alternating_mdr_integer_cofactor_firstdhsf_prefix) * (ff_bn_mce_alternating_mdr_integer_cofactor_firstdhsf_prefix) /\ ff_n_mce_alternating_mdr_integer_cofactor_firstdhsf_prefix = (ff_ap_mce_alternating_mdr_integer_cofactor_firstdhsf_prefix) * (ff_bn_mce_alternating_mdr_integer_cofactor_firstdhsf_prefix) + (ff_an_mce_alternating_mdr_integer_cofactor_firstdhsf_prefix) * (ff_bp_mce_alternating_mdr_integer_cofactor_firstdhsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_integer_cofactor_firstdhsf_prefix_term. ff_index_mce_alternating_mdr_integer_cofactor_firstdhsf_prefix = 2 * ff_odd_mce_term_mdr_integer_cofactor_firstdhsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_integer_cofactor_firstdhsf_prefix = (ff_ap_mce_alternating_mdr_integer_cofactor_firstdhsf_prefix) * (ff_bn_mce_alternating_mdr_integer_cofactor_firstdhsf_prefix) + (ff_an_mce_alternating_mdr_integer_cofactor_firstdhsf_prefix) * (ff_bp_mce_alternating_mdr_integer_cofactor_firstdhsf_prefix) /\ ff_n_mce_alternating_mdr_integer_cofactor_firstdhsf_prefix = (ff_ap_mce_alternating_mdr_integer_cofactor_firstdhsf_prefix) * (ff_bp_mce_alternating_mdr_integer_cofactor_firstdhsf_prefix) + (ff_an_mce_alternating_mdr_integer_cofactor_firstdhsf_prefix) * (ff_bn_mce_alternating_mdr_integer_cofactor_firstdhsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_integer_cofactor_firstdhsf_positive ff_v_mce_mdr_integer_cofactor_firstdhsf_positive. ((((exists ff_h_mce_mdr_integer_cofactor_firstdhsf_positive_start. ff_h_mce_mdr_integer_cofactor_firstdhsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_integer_cofactor_firstdhsf_positive)) /\ exists ff_q_mce_mdr_integer_cofactor_firstdhsf_positive_start. ff_u_mce_mdr_integer_cofactor_firstdhsf_positive = ff_q_mce_mdr_integer_cofactor_firstdhsf_positive_start * S ((S (0)) * ff_v_mce_mdr_integer_cofactor_firstdhsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_integer_cofactor_firstdhsf_positive_terminal. ff_h_mce_mdr_integer_cofactor_firstdhsf_positive_terminal + S (mdr_p_integer_cofactor_firstdh) = S ((S ((S (mdr_q_integer_cofactor_firstdhs)))) * ff_v_mce_mdr_integer_cofactor_firstdhsf_positive)) /\ exists ff_q_mce_mdr_integer_cofactor_firstdhsf_positive_terminal. ff_u_mce_mdr_integer_cofactor_firstdhsf_positive = ff_q_mce_mdr_integer_cofactor_firstdhsf_positive_terminal * S ((S ((S (mdr_q_integer_cofactor_firstdhs)))) * ff_v_mce_mdr_integer_cofactor_firstdhsf_positive) + (mdr_p_integer_cofactor_firstdh))) /\ forall ff_i_mce_mdr_integer_cofactor_firstdhsf_positive. (exists ff_lt_mce_mdr_integer_cofactor_firstdhsf_positive_bound. ff_lt_mce_mdr_integer_cofactor_firstdhsf_positive_bound + S ff_i_mce_mdr_integer_cofactor_firstdhsf_positive = (S (mdr_q_integer_cofactor_firstdhs))) -> exists ff_a_mce_mdr_integer_cofactor_firstdhsf_positive ff_r_mce_mdr_integer_cofactor_firstdhsf_positive ff_s_mce_mdr_integer_cofactor_firstdhsf_positive. ((((exists ff_h_mce_mdr_integer_cofactor_firstdhsf_positive_summand. ff_h_mce_mdr_integer_cofactor_firstdhsf_positive_summand + S (ff_a_mce_mdr_integer_cofactor_firstdhsf_positive) = S ((S (ff_i_mce_mdr_integer_cofactor_firstdhsf_positive)) * ff_uc_mce_fold_mdr_integer_cofactor_firstdhsf)) /\ exists ff_q_mce_mdr_integer_cofactor_firstdhsf_positive_summand. ff_ub_mce_fold_mdr_integer_cofactor_firstdhsf = ff_q_mce_mdr_integer_cofactor_firstdhsf_positive_summand * S ((S (ff_i_mce_mdr_integer_cofactor_firstdhsf_positive)) * ff_uc_mce_fold_mdr_integer_cofactor_firstdhsf) + (ff_a_mce_mdr_integer_cofactor_firstdhsf_positive))) /\ ((((exists ff_h_mce_mdr_integer_cofactor_firstdhsf_positive_partial. ff_h_mce_mdr_integer_cofactor_firstdhsf_positive_partial + S (ff_r_mce_mdr_integer_cofactor_firstdhsf_positive) = S ((S (ff_i_mce_mdr_integer_cofactor_firstdhsf_positive)) * ff_v_mce_mdr_integer_cofactor_firstdhsf_positive)) /\ exists ff_q_mce_mdr_integer_cofactor_firstdhsf_positive_partial. ff_u_mce_mdr_integer_cofactor_firstdhsf_positive = ff_q_mce_mdr_integer_cofactor_firstdhsf_positive_partial * S ((S (ff_i_mce_mdr_integer_cofactor_firstdhsf_positive)) * ff_v_mce_mdr_integer_cofactor_firstdhsf_positive) + (ff_r_mce_mdr_integer_cofactor_firstdhsf_positive))) /\ ((((exists ff_h_mce_mdr_integer_cofactor_firstdhsf_positive_successor. ff_h_mce_mdr_integer_cofactor_firstdhsf_positive_successor + S (ff_s_mce_mdr_integer_cofactor_firstdhsf_positive) = S ((S (S ff_i_mce_mdr_integer_cofactor_firstdhsf_positive)) * ff_v_mce_mdr_integer_cofactor_firstdhsf_positive)) /\ exists ff_q_mce_mdr_integer_cofactor_firstdhsf_positive_successor. ff_u_mce_mdr_integer_cofactor_firstdhsf_positive = ff_q_mce_mdr_integer_cofactor_firstdhsf_positive_successor * S ((S (S ff_i_mce_mdr_integer_cofactor_firstdhsf_positive)) * ff_v_mce_mdr_integer_cofactor_firstdhsf_positive) + (ff_s_mce_mdr_integer_cofactor_firstdhsf_positive))) /\ ff_s_mce_mdr_integer_cofactor_firstdhsf_positive = ff_r_mce_mdr_integer_cofactor_firstdhsf_positive + ff_a_mce_mdr_integer_cofactor_firstdhsf_positive)))))) /\ (exists ff_u_mce_mdr_integer_cofactor_firstdhsf_negative ff_v_mce_mdr_integer_cofactor_firstdhsf_negative. ((((exists ff_h_mce_mdr_integer_cofactor_firstdhsf_negative_start. ff_h_mce_mdr_integer_cofactor_firstdhsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_integer_cofactor_firstdhsf_negative)) /\ exists ff_q_mce_mdr_integer_cofactor_firstdhsf_negative_start. ff_u_mce_mdr_integer_cofactor_firstdhsf_negative = ff_q_mce_mdr_integer_cofactor_firstdhsf_negative_start * S ((S (0)) * ff_v_mce_mdr_integer_cofactor_firstdhsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_integer_cofactor_firstdhsf_negative_terminal. ff_h_mce_mdr_integer_cofactor_firstdhsf_negative_terminal + S (mdr_n_integer_cofactor_firstdh) = S ((S ((S (mdr_q_integer_cofactor_firstdhs)))) * ff_v_mce_mdr_integer_cofactor_firstdhsf_negative)) /\ exists ff_q_mce_mdr_integer_cofactor_firstdhsf_negative_terminal. ff_u_mce_mdr_integer_cofactor_firstdhsf_negative = ff_q_mce_mdr_integer_cofactor_firstdhsf_negative_terminal * S ((S ((S (mdr_q_integer_cofactor_firstdhs)))) * ff_v_mce_mdr_integer_cofactor_firstdhsf_negative) + (mdr_n_integer_cofactor_firstdh))) /\ forall ff_i_mce_mdr_integer_cofactor_firstdhsf_negative. (exists ff_lt_mce_mdr_integer_cofactor_firstdhsf_negative_bound. ff_lt_mce_mdr_integer_cofactor_firstdhsf_negative_bound + S ff_i_mce_mdr_integer_cofactor_firstdhsf_negative = (S (mdr_q_integer_cofactor_firstdhs))) -> exists ff_a_mce_mdr_integer_cofactor_firstdhsf_negative ff_r_mce_mdr_integer_cofactor_firstdhsf_negative ff_s_mce_mdr_integer_cofactor_firstdhsf_negative. ((((exists ff_h_mce_mdr_integer_cofactor_firstdhsf_negative_summand. ff_h_mce_mdr_integer_cofactor_firstdhsf_negative_summand + S (ff_a_mce_mdr_integer_cofactor_firstdhsf_negative) = S ((S (ff_i_mce_mdr_integer_cofactor_firstdhsf_negative)) * ff_vc_mce_fold_mdr_integer_cofactor_firstdhsf)) /\ exists ff_q_mce_mdr_integer_cofactor_firstdhsf_negative_summand. ff_vb_mce_fold_mdr_integer_cofactor_firstdhsf = ff_q_mce_mdr_integer_cofactor_firstdhsf_negative_summand * S ((S (ff_i_mce_mdr_integer_cofactor_firstdhsf_negative)) * ff_vc_mce_fold_mdr_integer_cofactor_firstdhsf) + (ff_a_mce_mdr_integer_cofactor_firstdhsf_negative))) /\ ((((exists ff_h_mce_mdr_integer_cofactor_firstdhsf_negative_partial. ff_h_mce_mdr_integer_cofactor_firstdhsf_negative_partial + S (ff_r_mce_mdr_integer_cofactor_firstdhsf_negative) = S ((S (ff_i_mce_mdr_integer_cofactor_firstdhsf_negative)) * ff_v_mce_mdr_integer_cofactor_firstdhsf_negative)) /\ exists ff_q_mce_mdr_integer_cofactor_firstdhsf_negative_partial. ff_u_mce_mdr_integer_cofactor_firstdhsf_negative = ff_q_mce_mdr_integer_cofactor_firstdhsf_negative_partial * S ((S (ff_i_mce_mdr_integer_cofactor_firstdhsf_negative)) * ff_v_mce_mdr_integer_cofactor_firstdhsf_negative) + (ff_r_mce_mdr_integer_cofactor_firstdhsf_negative))) /\ ((((exists ff_h_mce_mdr_integer_cofactor_firstdhsf_negative_successor. ff_h_mce_mdr_integer_cofactor_firstdhsf_negative_successor + S (ff_s_mce_mdr_integer_cofactor_firstdhsf_negative) = S ((S (S ff_i_mce_mdr_integer_cofactor_firstdhsf_negative)) * ff_v_mce_mdr_integer_cofactor_firstdhsf_negative)) /\ exists ff_q_mce_mdr_integer_cofactor_firstdhsf_negative_successor. ff_u_mce_mdr_integer_cofactor_firstdhsf_negative = ff_q_mce_mdr_integer_cofactor_firstdhsf_negative_successor * S ((S (S ff_i_mce_mdr_integer_cofactor_firstdhsf_negative)) * ff_v_mce_mdr_integer_cofactor_firstdhsf_negative) + (ff_s_mce_mdr_integer_cofactor_firstdhsf_negative))) /\ ff_s_mce_mdr_integer_cofactor_firstdhsf_negative = ff_r_mce_mdr_integer_cofactor_firstdhsf_negative + ff_a_mce_mdr_integer_cofactor_firstdhsf_negative))))))))))))))) /\ ((exists mdr_gap_integer_cofactor_firstdi. mdr_gap_integer_cofactor_firstdi + S (mdr_i_integer_cofactor_firstd) = (mdr_l_integer_cofactor_firstd)) /\ (exists mdr_z_integer_cofactor_firstdr. ((exists mdr_a_integer_cofactor_firstdrc mdr_b_integer_cofactor_firstdrc mdr_c_integer_cofactor_firstdrc mdr_e_integer_cofactor_firstdrc mdr_f_integer_cofactor_firstdrc. ((mdr_a_integer_cofactor_firstdrc = ((q) + (mdr_up_integer_cofactor_first)) * S ((q) + (mdr_up_integer_cofactor_first)) + ((mdr_up_integer_cofactor_first) + (mdr_up_integer_cofactor_first))) /\ ((mdr_b_integer_cofactor_firstdrc = ((mdr_us_integer_cofactor_first) + (mdr_un_integer_cofactor_first)) * S ((mdr_us_integer_cofactor_first) + (mdr_un_integer_cofactor_first)) + ((mdr_un_integer_cofactor_first) + (mdr_un_integer_cofactor_first))) /\ ((mdr_c_integer_cofactor_firstdrc = ((mdr_a_integer_cofactor_firstdrc) + (mdr_b_integer_cofactor_firstdrc)) * S ((mdr_a_integer_cofactor_firstdrc) + (mdr_b_integer_cofactor_firstdrc)) + ((mdr_b_integer_cofactor_firstdrc) + (mdr_b_integer_cofactor_firstdrc))) /\ ((mdr_e_integer_cofactor_firstdrc = ((mdr_p_integer_cofactor_first) + (mdr_n_integer_cofactor_first)) * S ((mdr_p_integer_cofactor_first) + (mdr_n_integer_cofactor_first)) + ((mdr_n_integer_cofactor_first) + (mdr_n_integer_cofactor_first))) /\ ((mdr_f_integer_cofactor_firstdrc = ((mdr_ut_integer_cofactor_first) + (mdr_e_integer_cofactor_firstdrc)) * S ((mdr_ut_integer_cofactor_first) + (mdr_e_integer_cofactor_firstdrc)) + ((mdr_e_integer_cofactor_firstdrc) + (mdr_e_integer_cofactor_firstdrc))) /\ ((mdr_z_integer_cofactor_firstdr) = ((mdr_c_integer_cofactor_firstdrc) + (mdr_f_integer_cofactor_firstdrc)) * S ((mdr_c_integer_cofactor_firstdrc) + (mdr_f_integer_cofactor_firstdrc)) + ((mdr_f_integer_cofactor_firstdrc) + (mdr_f_integer_cofactor_firstdrc))))))))) /\ (((exists ff_h_mdr_integer_cofactor_firstdrb. ff_h_mdr_integer_cofactor_firstdrb + S (mdr_z_integer_cofactor_firstdr) = S ((S (mdr_i_integer_cofactor_firstd)) * mdr_c_integer_cofactor_firstd)) /\ exists ff_q_mdr_integer_cofactor_firstdrb. mdr_b_integer_cofactor_firstd = ff_q_mdr_integer_cofactor_firstdrb * S ((S (mdr_i_integer_cofactor_firstd)) * mdr_c_integer_cofactor_firstd) + (mdr_z_integer_cofactor_firstdr)))))))) /\ ((((exists ff_h_mdr_integer_cofactor_firstp. ff_h_mdr_integer_cofactor_firstp + S (mdr_p_integer_cofactor_first) = S ((S (mdr_j_integer_cofactor_first)) * cc)) /\ exists ff_q_mdr_integer_cofactor_firstp. cb = ff_q_mdr_integer_cofactor_firstp * S ((S (mdr_j_integer_cofactor_first)) * cc) + (mdr_p_integer_cofactor_first))) /\ (((exists ff_h_mdr_integer_cofactor_firstn. ff_h_mdr_integer_cofactor_firstn + S (mdr_n_integer_cofactor_first) = S ((S (mdr_j_integer_cofactor_first)) * dc)) /\ exists ff_q_mdr_integer_cofactor_firstn. db = ff_q_mdr_integer_cofactor_firstn * S ((S (mdr_j_integer_cofactor_first)) * dc) + (mdr_n_integer_cofactor_first))))))) -> (forall mdr_j_integer_cofactor_second. (exists mdr_gap_integer_cofactor_secondj. mdr_gap_integer_cofactor_secondj + S (mdr_j_integer_cofactor_second) = (S (q))) -> exists mdr_up_integer_cofactor_second mdr_us_integer_cofactor_second mdr_un_integer_cofactor_second mdr_ut_integer_cofactor_second mdr_p_integer_cofactor_second mdr_n_integer_cofactor_second. ((((forall ff_index_mdm_prefix_mdr_integer_cofactor_secondm_positive. (exists ff_gap_mdm_lt_mdr_integer_cofactor_secondm_positive_index_bound. ff_gap_mdm_lt_mdr_integer_cofactor_secondm_positive_index_bound + S (ff_index_mdm_prefix_mdr_integer_cofactor_secondm_positive) = ((q) * (q))) -> exists ff_row_mdm_prefix_mdr_integer_cofactor_secondm_positive ff_column_mdm_prefix_mdr_integer_cofactor_secondm_positive ff_value_mdm_prefix_mdr_integer_cofactor_secondm_positive. (ff_index_mdm_prefix_mdr_integer_cofactor_secondm_positive = (q) * ff_row_mdm_prefix_mdr_integer_cofactor_secondm_positive + ff_column_mdm_prefix_mdr_integer_cofactor_secondm_positive /\ ((exists ff_gap_mdm_lt_mdr_integer_cofactor_secondm_positive_column_bound. ff_gap_mdm_lt_mdr_integer_cofactor_secondm_positive_column_bound + S (ff_column_mdm_prefix_mdr_integer_cofactor_secondm_positive) = (q)) /\ ((exists ff_row_mdm_cell_mdr_integer_cofactor_secondm_positive_cell ff_column_mdm_cell_mdr_integer_cofactor_secondm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_integer_cofactor_secondm_positive_cell_row_before. ff_gap_mdm_lt_mdr_integer_cofactor_secondm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_integer_cofactor_secondm_positive) = (0)) /\ ff_row_mdm_cell_mdr_integer_cofactor_secondm_positive_cell = ff_row_mdm_prefix_mdr_integer_cofactor_secondm_positive) \/ ((exists ff_gap_mdm_le_mdr_integer_cofactor_secondm_positive_cell_row_after. ff_gap_mdm_le_mdr_integer_cofactor_secondm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_integer_cofactor_secondm_positive)) /\ ff_row_mdm_cell_mdr_integer_cofactor_secondm_positive_cell = S ff_row_mdm_prefix_mdr_integer_cofactor_secondm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_integer_cofactor_secondm_positive_cell_column_before. ff_gap_mdm_lt_mdr_integer_cofactor_secondm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_integer_cofactor_secondm_positive) = (mdr_j_integer_cofactor_second)) /\ ff_column_mdm_cell_mdr_integer_cofactor_secondm_positive_cell = ff_column_mdm_prefix_mdr_integer_cofactor_secondm_positive) \/ ((exists ff_gap_mdm_le_mdr_integer_cofactor_secondm_positive_cell_column_after. ff_gap_mdm_le_mdr_integer_cofactor_secondm_positive_cell_column_after + (mdr_j_integer_cofactor_second) = (ff_column_mdm_prefix_mdr_integer_cofactor_secondm_positive)) /\ ff_column_mdm_cell_mdr_integer_cofactor_secondm_positive_cell = S ff_column_mdm_prefix_mdr_integer_cofactor_secondm_positive))) /\ (((exists ff_h_mdm_mdr_integer_cofactor_secondm_positive_cell_source. ff_h_mdm_mdr_integer_cofactor_secondm_positive_cell_source + S (ff_value_mdm_prefix_mdr_integer_cofactor_secondm_positive) = S ((S ((ff_row_mdm_cell_mdr_integer_cofactor_secondm_positive_cell) * (S (q)) + (ff_column_mdm_cell_mdr_integer_cofactor_secondm_positive_cell))) * ec)) /\ exists ff_q_mdm_mdr_integer_cofactor_secondm_positive_cell_source. eb = ff_q_mdm_mdr_integer_cofactor_secondm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_integer_cofactor_secondm_positive_cell) * (S (q)) + (ff_column_mdm_cell_mdr_integer_cofactor_secondm_positive_cell))) * ec) + (ff_value_mdm_prefix_mdr_integer_cofactor_secondm_positive)))))) /\ (((exists ff_h_mdm_mdr_integer_cofactor_secondm_positive_target. ff_h_mdm_mdr_integer_cofactor_secondm_positive_target + S (ff_value_mdm_prefix_mdr_integer_cofactor_secondm_positive) = S ((S (ff_index_mdm_prefix_mdr_integer_cofactor_secondm_positive)) * mdr_us_integer_cofactor_second)) /\ exists ff_q_mdm_mdr_integer_cofactor_secondm_positive_target. mdr_up_integer_cofactor_second = ff_q_mdm_mdr_integer_cofactor_secondm_positive_target * S ((S (ff_index_mdm_prefix_mdr_integer_cofactor_secondm_positive)) * mdr_us_integer_cofactor_second) + (ff_value_mdm_prefix_mdr_integer_cofactor_secondm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_integer_cofactor_secondm_negative. (exists ff_gap_mdm_lt_mdr_integer_cofactor_secondm_negative_index_bound. ff_gap_mdm_lt_mdr_integer_cofactor_secondm_negative_index_bound + S (ff_index_mdm_prefix_mdr_integer_cofactor_secondm_negative) = ((q) * (q))) -> exists ff_row_mdm_prefix_mdr_integer_cofactor_secondm_negative ff_column_mdm_prefix_mdr_integer_cofactor_secondm_negative ff_value_mdm_prefix_mdr_integer_cofactor_secondm_negative. (ff_index_mdm_prefix_mdr_integer_cofactor_secondm_negative = (q) * ff_row_mdm_prefix_mdr_integer_cofactor_secondm_negative + ff_column_mdm_prefix_mdr_integer_cofactor_secondm_negative /\ ((exists ff_gap_mdm_lt_mdr_integer_cofactor_secondm_negative_column_bound. ff_gap_mdm_lt_mdr_integer_cofactor_secondm_negative_column_bound + S (ff_column_mdm_prefix_mdr_integer_cofactor_secondm_negative) = (q)) /\ ((exists ff_row_mdm_cell_mdr_integer_cofactor_secondm_negative_cell ff_column_mdm_cell_mdr_integer_cofactor_secondm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_integer_cofactor_secondm_negative_cell_row_before. ff_gap_mdm_lt_mdr_integer_cofactor_secondm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_integer_cofactor_secondm_negative) = (0)) /\ ff_row_mdm_cell_mdr_integer_cofactor_secondm_negative_cell = ff_row_mdm_prefix_mdr_integer_cofactor_secondm_negative) \/ ((exists ff_gap_mdm_le_mdr_integer_cofactor_secondm_negative_cell_row_after. ff_gap_mdm_le_mdr_integer_cofactor_secondm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_integer_cofactor_secondm_negative)) /\ ff_row_mdm_cell_mdr_integer_cofactor_secondm_negative_cell = S ff_row_mdm_prefix_mdr_integer_cofactor_secondm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_integer_cofactor_secondm_negative_cell_column_before. ff_gap_mdm_lt_mdr_integer_cofactor_secondm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_integer_cofactor_secondm_negative) = (mdr_j_integer_cofactor_second)) /\ ff_column_mdm_cell_mdr_integer_cofactor_secondm_negative_cell = ff_column_mdm_prefix_mdr_integer_cofactor_secondm_negative) \/ ((exists ff_gap_mdm_le_mdr_integer_cofactor_secondm_negative_cell_column_after. ff_gap_mdm_le_mdr_integer_cofactor_secondm_negative_cell_column_after + (mdr_j_integer_cofactor_second) = (ff_column_mdm_prefix_mdr_integer_cofactor_secondm_negative)) /\ ff_column_mdm_cell_mdr_integer_cofactor_secondm_negative_cell = S ff_column_mdm_prefix_mdr_integer_cofactor_secondm_negative))) /\ (((exists ff_h_mdm_mdr_integer_cofactor_secondm_negative_cell_source. ff_h_mdm_mdr_integer_cofactor_secondm_negative_cell_source + S (ff_value_mdm_prefix_mdr_integer_cofactor_secondm_negative) = S ((S ((ff_row_mdm_cell_mdr_integer_cofactor_secondm_negative_cell) * (S (q)) + (ff_column_mdm_cell_mdr_integer_cofactor_secondm_negative_cell))) * fc)) /\ exists ff_q_mdm_mdr_integer_cofactor_secondm_negative_cell_source. fb = ff_q_mdm_mdr_integer_cofactor_secondm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_integer_cofactor_secondm_negative_cell) * (S (q)) + (ff_column_mdm_cell_mdr_integer_cofactor_secondm_negative_cell))) * fc) + (ff_value_mdm_prefix_mdr_integer_cofactor_secondm_negative)))))) /\ (((exists ff_h_mdm_mdr_integer_cofactor_secondm_negative_target. ff_h_mdm_mdr_integer_cofactor_secondm_negative_target + S (ff_value_mdm_prefix_mdr_integer_cofactor_secondm_negative) = S ((S (ff_index_mdm_prefix_mdr_integer_cofactor_secondm_negative)) * mdr_ut_integer_cofactor_second)) /\ exists ff_q_mdm_mdr_integer_cofactor_secondm_negative_target. mdr_un_integer_cofactor_second = ff_q_mdm_mdr_integer_cofactor_secondm_negative_target * S ((S (ff_index_mdm_prefix_mdr_integer_cofactor_secondm_negative)) * mdr_ut_integer_cofactor_second) + (ff_value_mdm_prefix_mdr_integer_cofactor_secondm_negative))))))))) /\ ((exists mdr_b_integer_cofactor_secondd mdr_c_integer_cofactor_secondd mdr_l_integer_cofactor_secondd mdr_i_integer_cofactor_secondd. ((forall mdr_i_integer_cofactor_seconddh. (exists mdr_gap_integer_cofactor_seconddhi. mdr_gap_integer_cofactor_seconddhi + S (mdr_i_integer_cofactor_seconddh) = (mdr_l_integer_cofactor_secondd)) -> exists mdr_d_integer_cofactor_seconddh mdr_pb_integer_cofactor_seconddh mdr_pc_integer_cofactor_seconddh mdr_nb_integer_cofactor_seconddh mdr_nc_integer_cofactor_seconddh mdr_p_integer_cofactor_seconddh mdr_n_integer_cofactor_seconddh. ((exists mdr_z_integer_cofactor_seconddhr. ((exists mdr_a_integer_cofactor_seconddhrc mdr_b_integer_cofactor_seconddhrc mdr_c_integer_cofactor_seconddhrc mdr_e_integer_cofactor_seconddhrc mdr_f_integer_cofactor_seconddhrc. ((mdr_a_integer_cofactor_seconddhrc = ((mdr_d_integer_cofactor_seconddh) + (mdr_pb_integer_cofactor_seconddh)) * S ((mdr_d_integer_cofactor_seconddh) + (mdr_pb_integer_cofactor_seconddh)) + ((mdr_pb_integer_cofactor_seconddh) + (mdr_pb_integer_cofactor_seconddh))) /\ ((mdr_b_integer_cofactor_seconddhrc = ((mdr_pc_integer_cofactor_seconddh) + (mdr_nb_integer_cofactor_seconddh)) * S ((mdr_pc_integer_cofactor_seconddh) + (mdr_nb_integer_cofactor_seconddh)) + ((mdr_nb_integer_cofactor_seconddh) + (mdr_nb_integer_cofactor_seconddh))) /\ ((mdr_c_integer_cofactor_seconddhrc = ((mdr_a_integer_cofactor_seconddhrc) + (mdr_b_integer_cofactor_seconddhrc)) * S ((mdr_a_integer_cofactor_seconddhrc) + (mdr_b_integer_cofactor_seconddhrc)) + ((mdr_b_integer_cofactor_seconddhrc) + (mdr_b_integer_cofactor_seconddhrc))) /\ ((mdr_e_integer_cofactor_seconddhrc = ((mdr_p_integer_cofactor_seconddh) + (mdr_n_integer_cofactor_seconddh)) * S ((mdr_p_integer_cofactor_seconddh) + (mdr_n_integer_cofactor_seconddh)) + ((mdr_n_integer_cofactor_seconddh) + (mdr_n_integer_cofactor_seconddh))) /\ ((mdr_f_integer_cofactor_seconddhrc = ((mdr_nc_integer_cofactor_seconddh) + (mdr_e_integer_cofactor_seconddhrc)) * S ((mdr_nc_integer_cofactor_seconddh) + (mdr_e_integer_cofactor_seconddhrc)) + ((mdr_e_integer_cofactor_seconddhrc) + (mdr_e_integer_cofactor_seconddhrc))) /\ ((mdr_z_integer_cofactor_seconddhr) = ((mdr_c_integer_cofactor_seconddhrc) + (mdr_f_integer_cofactor_seconddhrc)) * S ((mdr_c_integer_cofactor_seconddhrc) + (mdr_f_integer_cofactor_seconddhrc)) + ((mdr_f_integer_cofactor_seconddhrc) + (mdr_f_integer_cofactor_seconddhrc))))))))) /\ (((exists ff_h_mdr_integer_cofactor_seconddhrb. ff_h_mdr_integer_cofactor_seconddhrb + S (mdr_z_integer_cofactor_seconddhr) = S ((S (mdr_i_integer_cofactor_seconddh)) * mdr_c_integer_cofactor_secondd)) /\ exists ff_q_mdr_integer_cofactor_seconddhrb. mdr_b_integer_cofactor_secondd = ff_q_mdr_integer_cofactor_seconddhrb * S ((S (mdr_i_integer_cofactor_seconddh)) * mdr_c_integer_cofactor_secondd) + (mdr_z_integer_cofactor_seconddhr))))) /\ (((((mdr_d_integer_cofactor_seconddh) = 0) /\ (((mdr_p_integer_cofactor_seconddh) = 1) /\ ((mdr_n_integer_cofactor_seconddh) = 0))) \/ exists mdr_q_integer_cofactor_seconddhs mdr_eb_integer_cofactor_seconddhs mdr_ec_integer_cofactor_seconddhs mdr_fb_integer_cofactor_seconddhs mdr_fc_integer_cofactor_seconddhs. (((mdr_d_integer_cofactor_seconddh) = S (mdr_q_integer_cofactor_seconddhs)) /\ ((forall mdr_j_integer_cofactor_seconddhsc. (exists mdr_gap_integer_cofactor_seconddhscj. mdr_gap_integer_cofactor_seconddhscj + S (mdr_j_integer_cofactor_seconddhsc) = (S (mdr_q_integer_cofactor_seconddhs))) -> exists mdr_i_integer_cofactor_seconddhsc mdr_up_integer_cofactor_seconddhsc mdr_us_integer_cofactor_seconddhsc mdr_un_integer_cofactor_seconddhsc mdr_ut_integer_cofactor_seconddhsc mdr_p_integer_cofactor_seconddhsc mdr_n_integer_cofactor_seconddhsc. ((exists mdr_gap_integer_cofactor_seconddhsci. mdr_gap_integer_cofactor_seconddhsci + S (mdr_i_integer_cofactor_seconddhsc) = (mdr_i_integer_cofactor_seconddh)) /\ ((exists mdr_z_integer_cofactor_seconddhscr. ((exists mdr_a_integer_cofactor_seconddhscrc mdr_b_integer_cofactor_seconddhscrc mdr_c_integer_cofactor_seconddhscrc mdr_e_integer_cofactor_seconddhscrc mdr_f_integer_cofactor_seconddhscrc. ((mdr_a_integer_cofactor_seconddhscrc = ((mdr_q_integer_cofactor_seconddhs) + (mdr_up_integer_cofactor_seconddhsc)) * S ((mdr_q_integer_cofactor_seconddhs) + (mdr_up_integer_cofactor_seconddhsc)) + ((mdr_up_integer_cofactor_seconddhsc) + (mdr_up_integer_cofactor_seconddhsc))) /\ ((mdr_b_integer_cofactor_seconddhscrc = ((mdr_us_integer_cofactor_seconddhsc) + (mdr_un_integer_cofactor_seconddhsc)) * S ((mdr_us_integer_cofactor_seconddhsc) + (mdr_un_integer_cofactor_seconddhsc)) + ((mdr_un_integer_cofactor_seconddhsc) + (mdr_un_integer_cofactor_seconddhsc))) /\ ((mdr_c_integer_cofactor_seconddhscrc = ((mdr_a_integer_cofactor_seconddhscrc) + (mdr_b_integer_cofactor_seconddhscrc)) * S ((mdr_a_integer_cofactor_seconddhscrc) + (mdr_b_integer_cofactor_seconddhscrc)) + ((mdr_b_integer_cofactor_seconddhscrc) + (mdr_b_integer_cofactor_seconddhscrc))) /\ ((mdr_e_integer_cofactor_seconddhscrc = ((mdr_p_integer_cofactor_seconddhsc) + (mdr_n_integer_cofactor_seconddhsc)) * S ((mdr_p_integer_cofactor_seconddhsc) + (mdr_n_integer_cofactor_seconddhsc)) + ((mdr_n_integer_cofactor_seconddhsc) + (mdr_n_integer_cofactor_seconddhsc))) /\ ((mdr_f_integer_cofactor_seconddhscrc = ((mdr_ut_integer_cofactor_seconddhsc) + (mdr_e_integer_cofactor_seconddhscrc)) * S ((mdr_ut_integer_cofactor_seconddhsc) + (mdr_e_integer_cofactor_seconddhscrc)) + ((mdr_e_integer_cofactor_seconddhscrc) + (mdr_e_integer_cofactor_seconddhscrc))) /\ ((mdr_z_integer_cofactor_seconddhscr) = ((mdr_c_integer_cofactor_seconddhscrc) + (mdr_f_integer_cofactor_seconddhscrc)) * S ((mdr_c_integer_cofactor_seconddhscrc) + (mdr_f_integer_cofactor_seconddhscrc)) + ((mdr_f_integer_cofactor_seconddhscrc) + (mdr_f_integer_cofactor_seconddhscrc))))))))) /\ (((exists ff_h_mdr_integer_cofactor_seconddhscrb. ff_h_mdr_integer_cofactor_seconddhscrb + S (mdr_z_integer_cofactor_seconddhscr) = S ((S (mdr_i_integer_cofactor_seconddhsc)) * mdr_c_integer_cofactor_secondd)) /\ exists ff_q_mdr_integer_cofactor_seconddhscrb. mdr_b_integer_cofactor_secondd = ff_q_mdr_integer_cofactor_seconddhscrb * S ((S (mdr_i_integer_cofactor_seconddhsc)) * mdr_c_integer_cofactor_secondd) + (mdr_z_integer_cofactor_seconddhscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_integer_cofactor_seconddhscm_positive. (exists ff_gap_mdm_lt_mdr_integer_cofactor_seconddhscm_positive_index_bound. ff_gap_mdm_lt_mdr_integer_cofactor_seconddhscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_integer_cofactor_seconddhscm_positive) = ((mdr_q_integer_cofactor_seconddhs) * (mdr_q_integer_cofactor_seconddhs))) -> exists ff_row_mdm_prefix_mdr_integer_cofactor_seconddhscm_positive ff_column_mdm_prefix_mdr_integer_cofactor_seconddhscm_positive ff_value_mdm_prefix_mdr_integer_cofactor_seconddhscm_positive. (ff_index_mdm_prefix_mdr_integer_cofactor_seconddhscm_positive = (mdr_q_integer_cofactor_seconddhs) * ff_row_mdm_prefix_mdr_integer_cofactor_seconddhscm_positive + ff_column_mdm_prefix_mdr_integer_cofactor_seconddhscm_positive /\ ((exists ff_gap_mdm_lt_mdr_integer_cofactor_seconddhscm_positive_column_bound. ff_gap_mdm_lt_mdr_integer_cofactor_seconddhscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_integer_cofactor_seconddhscm_positive) = (mdr_q_integer_cofactor_seconddhs)) /\ ((exists ff_row_mdm_cell_mdr_integer_cofactor_seconddhscm_positive_cell ff_column_mdm_cell_mdr_integer_cofactor_seconddhscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_integer_cofactor_seconddhscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_integer_cofactor_seconddhscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_integer_cofactor_seconddhscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_integer_cofactor_seconddhscm_positive_cell = ff_row_mdm_prefix_mdr_integer_cofactor_seconddhscm_positive) \/ ((exists ff_gap_mdm_le_mdr_integer_cofactor_seconddhscm_positive_cell_row_after. ff_gap_mdm_le_mdr_integer_cofactor_seconddhscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_integer_cofactor_seconddhscm_positive)) /\ ff_row_mdm_cell_mdr_integer_cofactor_seconddhscm_positive_cell = S ff_row_mdm_prefix_mdr_integer_cofactor_seconddhscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_integer_cofactor_seconddhscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_integer_cofactor_seconddhscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_integer_cofactor_seconddhscm_positive) = (mdr_j_integer_cofactor_seconddhsc)) /\ ff_column_mdm_cell_mdr_integer_cofactor_seconddhscm_positive_cell = ff_column_mdm_prefix_mdr_integer_cofactor_seconddhscm_positive) \/ ((exists ff_gap_mdm_le_mdr_integer_cofactor_seconddhscm_positive_cell_column_after. ff_gap_mdm_le_mdr_integer_cofactor_seconddhscm_positive_cell_column_after + (mdr_j_integer_cofactor_seconddhsc) = (ff_column_mdm_prefix_mdr_integer_cofactor_seconddhscm_positive)) /\ ff_column_mdm_cell_mdr_integer_cofactor_seconddhscm_positive_cell = S ff_column_mdm_prefix_mdr_integer_cofactor_seconddhscm_positive))) /\ (((exists ff_h_mdm_mdr_integer_cofactor_seconddhscm_positive_cell_source. ff_h_mdm_mdr_integer_cofactor_seconddhscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_integer_cofactor_seconddhscm_positive) = S ((S ((ff_row_mdm_cell_mdr_integer_cofactor_seconddhscm_positive_cell) * (S (mdr_q_integer_cofactor_seconddhs)) + (ff_column_mdm_cell_mdr_integer_cofactor_seconddhscm_positive_cell))) * mdr_pc_integer_cofactor_seconddh)) /\ exists ff_q_mdm_mdr_integer_cofactor_seconddhscm_positive_cell_source. mdr_pb_integer_cofactor_seconddh = ff_q_mdm_mdr_integer_cofactor_seconddhscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_integer_cofactor_seconddhscm_positive_cell) * (S (mdr_q_integer_cofactor_seconddhs)) + (ff_column_mdm_cell_mdr_integer_cofactor_seconddhscm_positive_cell))) * mdr_pc_integer_cofactor_seconddh) + (ff_value_mdm_prefix_mdr_integer_cofactor_seconddhscm_positive)))))) /\ (((exists ff_h_mdm_mdr_integer_cofactor_seconddhscm_positive_target. ff_h_mdm_mdr_integer_cofactor_seconddhscm_positive_target + S (ff_value_mdm_prefix_mdr_integer_cofactor_seconddhscm_positive) = S ((S (ff_index_mdm_prefix_mdr_integer_cofactor_seconddhscm_positive)) * mdr_us_integer_cofactor_seconddhsc)) /\ exists ff_q_mdm_mdr_integer_cofactor_seconddhscm_positive_target. mdr_up_integer_cofactor_seconddhsc = ff_q_mdm_mdr_integer_cofactor_seconddhscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_integer_cofactor_seconddhscm_positive)) * mdr_us_integer_cofactor_seconddhsc) + (ff_value_mdm_prefix_mdr_integer_cofactor_seconddhscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_integer_cofactor_seconddhscm_negative. (exists ff_gap_mdm_lt_mdr_integer_cofactor_seconddhscm_negative_index_bound. ff_gap_mdm_lt_mdr_integer_cofactor_seconddhscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_integer_cofactor_seconddhscm_negative) = ((mdr_q_integer_cofactor_seconddhs) * (mdr_q_integer_cofactor_seconddhs))) -> exists ff_row_mdm_prefix_mdr_integer_cofactor_seconddhscm_negative ff_column_mdm_prefix_mdr_integer_cofactor_seconddhscm_negative ff_value_mdm_prefix_mdr_integer_cofactor_seconddhscm_negative. (ff_index_mdm_prefix_mdr_integer_cofactor_seconddhscm_negative = (mdr_q_integer_cofactor_seconddhs) * ff_row_mdm_prefix_mdr_integer_cofactor_seconddhscm_negative + ff_column_mdm_prefix_mdr_integer_cofactor_seconddhscm_negative /\ ((exists ff_gap_mdm_lt_mdr_integer_cofactor_seconddhscm_negative_column_bound. ff_gap_mdm_lt_mdr_integer_cofactor_seconddhscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_integer_cofactor_seconddhscm_negative) = (mdr_q_integer_cofactor_seconddhs)) /\ ((exists ff_row_mdm_cell_mdr_integer_cofactor_seconddhscm_negative_cell ff_column_mdm_cell_mdr_integer_cofactor_seconddhscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_integer_cofactor_seconddhscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_integer_cofactor_seconddhscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_integer_cofactor_seconddhscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_integer_cofactor_seconddhscm_negative_cell = ff_row_mdm_prefix_mdr_integer_cofactor_seconddhscm_negative) \/ ((exists ff_gap_mdm_le_mdr_integer_cofactor_seconddhscm_negative_cell_row_after. ff_gap_mdm_le_mdr_integer_cofactor_seconddhscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_integer_cofactor_seconddhscm_negative)) /\ ff_row_mdm_cell_mdr_integer_cofactor_seconddhscm_negative_cell = S ff_row_mdm_prefix_mdr_integer_cofactor_seconddhscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_integer_cofactor_seconddhscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_integer_cofactor_seconddhscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_integer_cofactor_seconddhscm_negative) = (mdr_j_integer_cofactor_seconddhsc)) /\ ff_column_mdm_cell_mdr_integer_cofactor_seconddhscm_negative_cell = ff_column_mdm_prefix_mdr_integer_cofactor_seconddhscm_negative) \/ ((exists ff_gap_mdm_le_mdr_integer_cofactor_seconddhscm_negative_cell_column_after. ff_gap_mdm_le_mdr_integer_cofactor_seconddhscm_negative_cell_column_after + (mdr_j_integer_cofactor_seconddhsc) = (ff_column_mdm_prefix_mdr_integer_cofactor_seconddhscm_negative)) /\ ff_column_mdm_cell_mdr_integer_cofactor_seconddhscm_negative_cell = S ff_column_mdm_prefix_mdr_integer_cofactor_seconddhscm_negative))) /\ (((exists ff_h_mdm_mdr_integer_cofactor_seconddhscm_negative_cell_source. ff_h_mdm_mdr_integer_cofactor_seconddhscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_integer_cofactor_seconddhscm_negative) = S ((S ((ff_row_mdm_cell_mdr_integer_cofactor_seconddhscm_negative_cell) * (S (mdr_q_integer_cofactor_seconddhs)) + (ff_column_mdm_cell_mdr_integer_cofactor_seconddhscm_negative_cell))) * mdr_nc_integer_cofactor_seconddh)) /\ exists ff_q_mdm_mdr_integer_cofactor_seconddhscm_negative_cell_source. mdr_nb_integer_cofactor_seconddh = ff_q_mdm_mdr_integer_cofactor_seconddhscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_integer_cofactor_seconddhscm_negative_cell) * (S (mdr_q_integer_cofactor_seconddhs)) + (ff_column_mdm_cell_mdr_integer_cofactor_seconddhscm_negative_cell))) * mdr_nc_integer_cofactor_seconddh) + (ff_value_mdm_prefix_mdr_integer_cofactor_seconddhscm_negative)))))) /\ (((exists ff_h_mdm_mdr_integer_cofactor_seconddhscm_negative_target. ff_h_mdm_mdr_integer_cofactor_seconddhscm_negative_target + S (ff_value_mdm_prefix_mdr_integer_cofactor_seconddhscm_negative) = S ((S (ff_index_mdm_prefix_mdr_integer_cofactor_seconddhscm_negative)) * mdr_ut_integer_cofactor_seconddhsc)) /\ exists ff_q_mdm_mdr_integer_cofactor_seconddhscm_negative_target. mdr_un_integer_cofactor_seconddhsc = ff_q_mdm_mdr_integer_cofactor_seconddhscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_integer_cofactor_seconddhscm_negative)) * mdr_ut_integer_cofactor_seconddhsc) + (ff_value_mdm_prefix_mdr_integer_cofactor_seconddhscm_negative))))))))) /\ ((((exists ff_h_mdr_integer_cofactor_seconddhscp. ff_h_mdr_integer_cofactor_seconddhscp + S (mdr_p_integer_cofactor_seconddhsc) = S ((S (mdr_j_integer_cofactor_seconddhsc)) * mdr_ec_integer_cofactor_seconddhs)) /\ exists ff_q_mdr_integer_cofactor_seconddhscp. mdr_eb_integer_cofactor_seconddhs = ff_q_mdr_integer_cofactor_seconddhscp * S ((S (mdr_j_integer_cofactor_seconddhsc)) * mdr_ec_integer_cofactor_seconddhs) + (mdr_p_integer_cofactor_seconddhsc))) /\ (((exists ff_h_mdr_integer_cofactor_seconddhscn. ff_h_mdr_integer_cofactor_seconddhscn + S (mdr_n_integer_cofactor_seconddhsc) = S ((S (mdr_j_integer_cofactor_seconddhsc)) * mdr_fc_integer_cofactor_seconddhs)) /\ exists ff_q_mdr_integer_cofactor_seconddhscn. mdr_fb_integer_cofactor_seconddhs = ff_q_mdr_integer_cofactor_seconddhscn * S ((S (mdr_j_integer_cofactor_seconddhsc)) * mdr_fc_integer_cofactor_seconddhs) + (mdr_n_integer_cofactor_seconddhsc)))))))) /\ (exists ff_ub_mce_fold_mdr_integer_cofactor_seconddhsf ff_uc_mce_fold_mdr_integer_cofactor_seconddhsf ff_vb_mce_fold_mdr_integer_cofactor_seconddhsf ff_vc_mce_fold_mdr_integer_cofactor_seconddhsf. ((forall ff_index_mce_alternating_mdr_integer_cofactor_seconddhsf_prefix. (exists ff_gap_mce_mdr_integer_cofactor_seconddhsf_prefix_index. ff_gap_mce_mdr_integer_cofactor_seconddhsf_prefix_index + S (ff_index_mce_alternating_mdr_integer_cofactor_seconddhsf_prefix) = (S (mdr_q_integer_cofactor_seconddhs))) -> exists ff_ap_mce_alternating_mdr_integer_cofactor_seconddhsf_prefix ff_an_mce_alternating_mdr_integer_cofactor_seconddhsf_prefix ff_bp_mce_alternating_mdr_integer_cofactor_seconddhsf_prefix ff_bn_mce_alternating_mdr_integer_cofactor_seconddhsf_prefix ff_p_mce_alternating_mdr_integer_cofactor_seconddhsf_prefix ff_n_mce_alternating_mdr_integer_cofactor_seconddhsf_prefix. ((((exists ff_h_mce_mdr_integer_cofactor_seconddhsf_prefix_ap. ff_h_mce_mdr_integer_cofactor_seconddhsf_prefix_ap + S (ff_ap_mce_alternating_mdr_integer_cofactor_seconddhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_integer_cofactor_seconddhsf_prefix)) * mdr_pc_integer_cofactor_seconddh)) /\ exists ff_q_mce_mdr_integer_cofactor_seconddhsf_prefix_ap. mdr_pb_integer_cofactor_seconddh = ff_q_mce_mdr_integer_cofactor_seconddhsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_integer_cofactor_seconddhsf_prefix)) * mdr_pc_integer_cofactor_seconddh) + (ff_ap_mce_alternating_mdr_integer_cofactor_seconddhsf_prefix))) /\ ((((exists ff_h_mce_mdr_integer_cofactor_seconddhsf_prefix_an. ff_h_mce_mdr_integer_cofactor_seconddhsf_prefix_an + S (ff_an_mce_alternating_mdr_integer_cofactor_seconddhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_integer_cofactor_seconddhsf_prefix)) * mdr_nc_integer_cofactor_seconddh)) /\ exists ff_q_mce_mdr_integer_cofactor_seconddhsf_prefix_an. mdr_nb_integer_cofactor_seconddh = ff_q_mce_mdr_integer_cofactor_seconddhsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_integer_cofactor_seconddhsf_prefix)) * mdr_nc_integer_cofactor_seconddh) + (ff_an_mce_alternating_mdr_integer_cofactor_seconddhsf_prefix))) /\ ((((exists ff_h_mce_mdr_integer_cofactor_seconddhsf_prefix_bp. ff_h_mce_mdr_integer_cofactor_seconddhsf_prefix_bp + S (ff_bp_mce_alternating_mdr_integer_cofactor_seconddhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_integer_cofactor_seconddhsf_prefix)) * mdr_ec_integer_cofactor_seconddhs)) /\ exists ff_q_mce_mdr_integer_cofactor_seconddhsf_prefix_bp. mdr_eb_integer_cofactor_seconddhs = ff_q_mce_mdr_integer_cofactor_seconddhsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_integer_cofactor_seconddhsf_prefix)) * mdr_ec_integer_cofactor_seconddhs) + (ff_bp_mce_alternating_mdr_integer_cofactor_seconddhsf_prefix))) /\ ((((exists ff_h_mce_mdr_integer_cofactor_seconddhsf_prefix_bn. ff_h_mce_mdr_integer_cofactor_seconddhsf_prefix_bn + S (ff_bn_mce_alternating_mdr_integer_cofactor_seconddhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_integer_cofactor_seconddhsf_prefix)) * mdr_fc_integer_cofactor_seconddhs)) /\ exists ff_q_mce_mdr_integer_cofactor_seconddhsf_prefix_bn. mdr_fb_integer_cofactor_seconddhs = ff_q_mce_mdr_integer_cofactor_seconddhsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_integer_cofactor_seconddhsf_prefix)) * mdr_fc_integer_cofactor_seconddhs) + (ff_bn_mce_alternating_mdr_integer_cofactor_seconddhsf_prefix))) /\ ((((exists ff_h_mce_mdr_integer_cofactor_seconddhsf_prefix_positive. ff_h_mce_mdr_integer_cofactor_seconddhsf_prefix_positive + S (ff_p_mce_alternating_mdr_integer_cofactor_seconddhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_integer_cofactor_seconddhsf_prefix)) * ff_uc_mce_fold_mdr_integer_cofactor_seconddhsf)) /\ exists ff_q_mce_mdr_integer_cofactor_seconddhsf_prefix_positive. ff_ub_mce_fold_mdr_integer_cofactor_seconddhsf = ff_q_mce_mdr_integer_cofactor_seconddhsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_integer_cofactor_seconddhsf_prefix)) * ff_uc_mce_fold_mdr_integer_cofactor_seconddhsf) + (ff_p_mce_alternating_mdr_integer_cofactor_seconddhsf_prefix))) /\ ((((exists ff_h_mce_mdr_integer_cofactor_seconddhsf_prefix_negative. ff_h_mce_mdr_integer_cofactor_seconddhsf_prefix_negative + S (ff_n_mce_alternating_mdr_integer_cofactor_seconddhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_integer_cofactor_seconddhsf_prefix)) * ff_vc_mce_fold_mdr_integer_cofactor_seconddhsf)) /\ exists ff_q_mce_mdr_integer_cofactor_seconddhsf_prefix_negative. ff_vb_mce_fold_mdr_integer_cofactor_seconddhsf = ff_q_mce_mdr_integer_cofactor_seconddhsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_integer_cofactor_seconddhsf_prefix)) * ff_vc_mce_fold_mdr_integer_cofactor_seconddhsf) + (ff_n_mce_alternating_mdr_integer_cofactor_seconddhsf_prefix))) /\ (((exists ff_even_mce_term_mdr_integer_cofactor_seconddhsf_prefix_term. ff_index_mce_alternating_mdr_integer_cofactor_seconddhsf_prefix = 2 * ff_even_mce_term_mdr_integer_cofactor_seconddhsf_prefix_term) /\ (ff_p_mce_alternating_mdr_integer_cofactor_seconddhsf_prefix = (ff_ap_mce_alternating_mdr_integer_cofactor_seconddhsf_prefix) * (ff_bp_mce_alternating_mdr_integer_cofactor_seconddhsf_prefix) + (ff_an_mce_alternating_mdr_integer_cofactor_seconddhsf_prefix) * (ff_bn_mce_alternating_mdr_integer_cofactor_seconddhsf_prefix) /\ ff_n_mce_alternating_mdr_integer_cofactor_seconddhsf_prefix = (ff_ap_mce_alternating_mdr_integer_cofactor_seconddhsf_prefix) * (ff_bn_mce_alternating_mdr_integer_cofactor_seconddhsf_prefix) + (ff_an_mce_alternating_mdr_integer_cofactor_seconddhsf_prefix) * (ff_bp_mce_alternating_mdr_integer_cofactor_seconddhsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_integer_cofactor_seconddhsf_prefix_term. ff_index_mce_alternating_mdr_integer_cofactor_seconddhsf_prefix = 2 * ff_odd_mce_term_mdr_integer_cofactor_seconddhsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_integer_cofactor_seconddhsf_prefix = (ff_ap_mce_alternating_mdr_integer_cofactor_seconddhsf_prefix) * (ff_bn_mce_alternating_mdr_integer_cofactor_seconddhsf_prefix) + (ff_an_mce_alternating_mdr_integer_cofactor_seconddhsf_prefix) * (ff_bp_mce_alternating_mdr_integer_cofactor_seconddhsf_prefix) /\ ff_n_mce_alternating_mdr_integer_cofactor_seconddhsf_prefix = (ff_ap_mce_alternating_mdr_integer_cofactor_seconddhsf_prefix) * (ff_bp_mce_alternating_mdr_integer_cofactor_seconddhsf_prefix) + (ff_an_mce_alternating_mdr_integer_cofactor_seconddhsf_prefix) * (ff_bn_mce_alternating_mdr_integer_cofactor_seconddhsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_integer_cofactor_seconddhsf_positive ff_v_mce_mdr_integer_cofactor_seconddhsf_positive. ((((exists ff_h_mce_mdr_integer_cofactor_seconddhsf_positive_start. ff_h_mce_mdr_integer_cofactor_seconddhsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_integer_cofactor_seconddhsf_positive)) /\ exists ff_q_mce_mdr_integer_cofactor_seconddhsf_positive_start. ff_u_mce_mdr_integer_cofactor_seconddhsf_positive = ff_q_mce_mdr_integer_cofactor_seconddhsf_positive_start * S ((S (0)) * ff_v_mce_mdr_integer_cofactor_seconddhsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_integer_cofactor_seconddhsf_positive_terminal. ff_h_mce_mdr_integer_cofactor_seconddhsf_positive_terminal + S (mdr_p_integer_cofactor_seconddh) = S ((S ((S (mdr_q_integer_cofactor_seconddhs)))) * ff_v_mce_mdr_integer_cofactor_seconddhsf_positive)) /\ exists ff_q_mce_mdr_integer_cofactor_seconddhsf_positive_terminal. ff_u_mce_mdr_integer_cofactor_seconddhsf_positive = ff_q_mce_mdr_integer_cofactor_seconddhsf_positive_terminal * S ((S ((S (mdr_q_integer_cofactor_seconddhs)))) * ff_v_mce_mdr_integer_cofactor_seconddhsf_positive) + (mdr_p_integer_cofactor_seconddh))) /\ forall ff_i_mce_mdr_integer_cofactor_seconddhsf_positive. (exists ff_lt_mce_mdr_integer_cofactor_seconddhsf_positive_bound. ff_lt_mce_mdr_integer_cofactor_seconddhsf_positive_bound + S ff_i_mce_mdr_integer_cofactor_seconddhsf_positive = (S (mdr_q_integer_cofactor_seconddhs))) -> exists ff_a_mce_mdr_integer_cofactor_seconddhsf_positive ff_r_mce_mdr_integer_cofactor_seconddhsf_positive ff_s_mce_mdr_integer_cofactor_seconddhsf_positive. ((((exists ff_h_mce_mdr_integer_cofactor_seconddhsf_positive_summand. ff_h_mce_mdr_integer_cofactor_seconddhsf_positive_summand + S (ff_a_mce_mdr_integer_cofactor_seconddhsf_positive) = S ((S (ff_i_mce_mdr_integer_cofactor_seconddhsf_positive)) * ff_uc_mce_fold_mdr_integer_cofactor_seconddhsf)) /\ exists ff_q_mce_mdr_integer_cofactor_seconddhsf_positive_summand. ff_ub_mce_fold_mdr_integer_cofactor_seconddhsf = ff_q_mce_mdr_integer_cofactor_seconddhsf_positive_summand * S ((S (ff_i_mce_mdr_integer_cofactor_seconddhsf_positive)) * ff_uc_mce_fold_mdr_integer_cofactor_seconddhsf) + (ff_a_mce_mdr_integer_cofactor_seconddhsf_positive))) /\ ((((exists ff_h_mce_mdr_integer_cofactor_seconddhsf_positive_partial. ff_h_mce_mdr_integer_cofactor_seconddhsf_positive_partial + S (ff_r_mce_mdr_integer_cofactor_seconddhsf_positive) = S ((S (ff_i_mce_mdr_integer_cofactor_seconddhsf_positive)) * ff_v_mce_mdr_integer_cofactor_seconddhsf_positive)) /\ exists ff_q_mce_mdr_integer_cofactor_seconddhsf_positive_partial. ff_u_mce_mdr_integer_cofactor_seconddhsf_positive = ff_q_mce_mdr_integer_cofactor_seconddhsf_positive_partial * S ((S (ff_i_mce_mdr_integer_cofactor_seconddhsf_positive)) * ff_v_mce_mdr_integer_cofactor_seconddhsf_positive) + (ff_r_mce_mdr_integer_cofactor_seconddhsf_positive))) /\ ((((exists ff_h_mce_mdr_integer_cofactor_seconddhsf_positive_successor. ff_h_mce_mdr_integer_cofactor_seconddhsf_positive_successor + S (ff_s_mce_mdr_integer_cofactor_seconddhsf_positive) = S ((S (S ff_i_mce_mdr_integer_cofactor_seconddhsf_positive)) * ff_v_mce_mdr_integer_cofactor_seconddhsf_positive)) /\ exists ff_q_mce_mdr_integer_cofactor_seconddhsf_positive_successor. ff_u_mce_mdr_integer_cofactor_seconddhsf_positive = ff_q_mce_mdr_integer_cofactor_seconddhsf_positive_successor * S ((S (S ff_i_mce_mdr_integer_cofactor_seconddhsf_positive)) * ff_v_mce_mdr_integer_cofactor_seconddhsf_positive) + (ff_s_mce_mdr_integer_cofactor_seconddhsf_positive))) /\ ff_s_mce_mdr_integer_cofactor_seconddhsf_positive = ff_r_mce_mdr_integer_cofactor_seconddhsf_positive + ff_a_mce_mdr_integer_cofactor_seconddhsf_positive)))))) /\ (exists ff_u_mce_mdr_integer_cofactor_seconddhsf_negative ff_v_mce_mdr_integer_cofactor_seconddhsf_negative. ((((exists ff_h_mce_mdr_integer_cofactor_seconddhsf_negative_start. ff_h_mce_mdr_integer_cofactor_seconddhsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_integer_cofactor_seconddhsf_negative)) /\ exists ff_q_mce_mdr_integer_cofactor_seconddhsf_negative_start. ff_u_mce_mdr_integer_cofactor_seconddhsf_negative = ff_q_mce_mdr_integer_cofactor_seconddhsf_negative_start * S ((S (0)) * ff_v_mce_mdr_integer_cofactor_seconddhsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_integer_cofactor_seconddhsf_negative_terminal. ff_h_mce_mdr_integer_cofactor_seconddhsf_negative_terminal + S (mdr_n_integer_cofactor_seconddh) = S ((S ((S (mdr_q_integer_cofactor_seconddhs)))) * ff_v_mce_mdr_integer_cofactor_seconddhsf_negative)) /\ exists ff_q_mce_mdr_integer_cofactor_seconddhsf_negative_terminal. ff_u_mce_mdr_integer_cofactor_seconddhsf_negative = ff_q_mce_mdr_integer_cofactor_seconddhsf_negative_terminal * S ((S ((S (mdr_q_integer_cofactor_seconddhs)))) * ff_v_mce_mdr_integer_cofactor_seconddhsf_negative) + (mdr_n_integer_cofactor_seconddh))) /\ forall ff_i_mce_mdr_integer_cofactor_seconddhsf_negative. (exists ff_lt_mce_mdr_integer_cofactor_seconddhsf_negative_bound. ff_lt_mce_mdr_integer_cofactor_seconddhsf_negative_bound + S ff_i_mce_mdr_integer_cofactor_seconddhsf_negative = (S (mdr_q_integer_cofactor_seconddhs))) -> exists ff_a_mce_mdr_integer_cofactor_seconddhsf_negative ff_r_mce_mdr_integer_cofactor_seconddhsf_negative ff_s_mce_mdr_integer_cofactor_seconddhsf_negative. ((((exists ff_h_mce_mdr_integer_cofactor_seconddhsf_negative_summand. ff_h_mce_mdr_integer_cofactor_seconddhsf_negative_summand + S (ff_a_mce_mdr_integer_cofactor_seconddhsf_negative) = S ((S (ff_i_mce_mdr_integer_cofactor_seconddhsf_negative)) * ff_vc_mce_fold_mdr_integer_cofactor_seconddhsf)) /\ exists ff_q_mce_mdr_integer_cofactor_seconddhsf_negative_summand. ff_vb_mce_fold_mdr_integer_cofactor_seconddhsf = ff_q_mce_mdr_integer_cofactor_seconddhsf_negative_summand * S ((S (ff_i_mce_mdr_integer_cofactor_seconddhsf_negative)) * ff_vc_mce_fold_mdr_integer_cofactor_seconddhsf) + (ff_a_mce_mdr_integer_cofactor_seconddhsf_negative))) /\ ((((exists ff_h_mce_mdr_integer_cofactor_seconddhsf_negative_partial. ff_h_mce_mdr_integer_cofactor_seconddhsf_negative_partial + S (ff_r_mce_mdr_integer_cofactor_seconddhsf_negative) = S ((S (ff_i_mce_mdr_integer_cofactor_seconddhsf_negative)) * ff_v_mce_mdr_integer_cofactor_seconddhsf_negative)) /\ exists ff_q_mce_mdr_integer_cofactor_seconddhsf_negative_partial. ff_u_mce_mdr_integer_cofactor_seconddhsf_negative = ff_q_mce_mdr_integer_cofactor_seconddhsf_negative_partial * S ((S (ff_i_mce_mdr_integer_cofactor_seconddhsf_negative)) * ff_v_mce_mdr_integer_cofactor_seconddhsf_negative) + (ff_r_mce_mdr_integer_cofactor_seconddhsf_negative))) /\ ((((exists ff_h_mce_mdr_integer_cofactor_seconddhsf_negative_successor. ff_h_mce_mdr_integer_cofactor_seconddhsf_negative_successor + S (ff_s_mce_mdr_integer_cofactor_seconddhsf_negative) = S ((S (S ff_i_mce_mdr_integer_cofactor_seconddhsf_negative)) * ff_v_mce_mdr_integer_cofactor_seconddhsf_negative)) /\ exists ff_q_mce_mdr_integer_cofactor_seconddhsf_negative_successor. ff_u_mce_mdr_integer_cofactor_seconddhsf_negative = ff_q_mce_mdr_integer_cofactor_seconddhsf_negative_successor * S ((S (S ff_i_mce_mdr_integer_cofactor_seconddhsf_negative)) * ff_v_mce_mdr_integer_cofactor_seconddhsf_negative) + (ff_s_mce_mdr_integer_cofactor_seconddhsf_negative))) /\ ff_s_mce_mdr_integer_cofactor_seconddhsf_negative = ff_r_mce_mdr_integer_cofactor_seconddhsf_negative + ff_a_mce_mdr_integer_cofactor_seconddhsf_negative))))))))))))))) /\ ((exists mdr_gap_integer_cofactor_seconddi. mdr_gap_integer_cofactor_seconddi + S (mdr_i_integer_cofactor_secondd) = (mdr_l_integer_cofactor_secondd)) /\ (exists mdr_z_integer_cofactor_seconddr. ((exists mdr_a_integer_cofactor_seconddrc mdr_b_integer_cofactor_seconddrc mdr_c_integer_cofactor_seconddrc mdr_e_integer_cofactor_seconddrc mdr_f_integer_cofactor_seconddrc. ((mdr_a_integer_cofactor_seconddrc = ((q) + (mdr_up_integer_cofactor_second)) * S ((q) + (mdr_up_integer_cofactor_second)) + ((mdr_up_integer_cofactor_second) + (mdr_up_integer_cofactor_second))) /\ ((mdr_b_integer_cofactor_seconddrc = ((mdr_us_integer_cofactor_second) + (mdr_un_integer_cofactor_second)) * S ((mdr_us_integer_cofactor_second) + (mdr_un_integer_cofactor_second)) + ((mdr_un_integer_cofactor_second) + (mdr_un_integer_cofactor_second))) /\ ((mdr_c_integer_cofactor_seconddrc = ((mdr_a_integer_cofactor_seconddrc) + (mdr_b_integer_cofactor_seconddrc)) * S ((mdr_a_integer_cofactor_seconddrc) + (mdr_b_integer_cofactor_seconddrc)) + ((mdr_b_integer_cofactor_seconddrc) + (mdr_b_integer_cofactor_seconddrc))) /\ ((mdr_e_integer_cofactor_seconddrc = ((mdr_p_integer_cofactor_second) + (mdr_n_integer_cofactor_second)) * S ((mdr_p_integer_cofactor_second) + (mdr_n_integer_cofactor_second)) + ((mdr_n_integer_cofactor_second) + (mdr_n_integer_cofactor_second))) /\ ((mdr_f_integer_cofactor_seconddrc = ((mdr_ut_integer_cofactor_second) + (mdr_e_integer_cofactor_seconddrc)) * S ((mdr_ut_integer_cofactor_second) + (mdr_e_integer_cofactor_seconddrc)) + ((mdr_e_integer_cofactor_seconddrc) + (mdr_e_integer_cofactor_seconddrc))) /\ ((mdr_z_integer_cofactor_seconddr) = ((mdr_c_integer_cofactor_seconddrc) + (mdr_f_integer_cofactor_seconddrc)) * S ((mdr_c_integer_cofactor_seconddrc) + (mdr_f_integer_cofactor_seconddrc)) + ((mdr_f_integer_cofactor_seconddrc) + (mdr_f_integer_cofactor_seconddrc))))))))) /\ (((exists ff_h_mdr_integer_cofactor_seconddrb. ff_h_mdr_integer_cofactor_seconddrb + S (mdr_z_integer_cofactor_seconddr) = S ((S (mdr_i_integer_cofactor_secondd)) * mdr_c_integer_cofactor_secondd)) /\ exists ff_q_mdr_integer_cofactor_seconddrb. mdr_b_integer_cofactor_secondd = ff_q_mdr_integer_cofactor_seconddrb * S ((S (mdr_i_integer_cofactor_secondd)) * mdr_c_integer_cofactor_secondd) + (mdr_z_integer_cofactor_seconddr)))))))) /\ ((((exists ff_h_mdr_integer_cofactor_secondp. ff_h_mdr_integer_cofactor_secondp + S (mdr_p_integer_cofactor_second) = S ((S (mdr_j_integer_cofactor_second)) * gc)) /\ exists ff_q_mdr_integer_cofactor_secondp. gb = ff_q_mdr_integer_cofactor_secondp * S ((S (mdr_j_integer_cofactor_second)) * gc) + (mdr_p_integer_cofactor_second))) /\ (((exists ff_h_mdr_integer_cofactor_secondn. ff_h_mdr_integer_cofactor_secondn + S (mdr_n_integer_cofactor_second) = S ((S (mdr_j_integer_cofactor_second)) * hc)) /\ exists ff_q_mdr_integer_cofactor_secondn. hb = ff_q_mdr_integer_cofactor_secondn * S ((S (mdr_j_integer_cofactor_second)) * hc) + (mdr_n_integer_cofactor_second))))))) -> (forall ics_index_integer_cofactor_streams ics_value0_integer_cofactor_streams ics_value1_integer_cofactor_streams ics_value2_integer_cofactor_streams ics_value3_integer_cofactor_streams. (exists ics_gap_integer_cofactor_streams_bound. ics_gap_integer_cofactor_streams_bound + S (ics_index_integer_cofactor_streams) = (S q)) -> (((exists fs_h_ics_integer_cofactor_streams_at0. fs_h_ics_integer_cofactor_streams_at0 + S (ics_value0_integer_cofactor_streams) = S ((S (ics_index_integer_cofactor_streams)) * cc)) /\ exists fs_q_ics_integer_cofactor_streams_at0. cb = fs_q_ics_integer_cofactor_streams_at0 * S ((S (ics_index_integer_cofactor_streams)) * cc) + (ics_value0_integer_cofactor_streams))) -> (((exists fs_h_ics_integer_cofactor_streams_at1. fs_h_ics_integer_cofactor_streams_at1 + S (ics_value1_integer_cofactor_streams) = S ((S (ics_index_integer_cofactor_streams)) * dc)) /\ exists fs_q_ics_integer_cofactor_streams_at1. db = fs_q_ics_integer_cofactor_streams_at1 * S ((S (ics_index_integer_cofactor_streams)) * dc) + (ics_value1_integer_cofactor_streams))) -> (((exists fs_h_ics_integer_cofactor_streams_at2. fs_h_ics_integer_cofactor_streams_at2 + S (ics_value2_integer_cofactor_streams) = S ((S (ics_index_integer_cofactor_streams)) * gc)) /\ exists fs_q_ics_integer_cofactor_streams_at2. gb = fs_q_ics_integer_cofactor_streams_at2 * S ((S (ics_index_integer_cofactor_streams)) * gc) + (ics_value2_integer_cofactor_streams))) -> (((exists fs_h_ics_integer_cofactor_streams_at3. fs_h_ics_integer_cofactor_streams_at3 + S (ics_value3_integer_cofactor_streams) = S ((S (ics_index_integer_cofactor_streams)) * hc)) /\ exists fs_q_ics_integer_cofactor_streams_at3. hb = fs_q_ics_integer_cofactor_streams_at3 * S ((S (ics_index_integer_cofactor_streams)) * hc) + (ics_value3_integer_cofactor_streams))) -> ics_value0_integer_cofactor_streams + ics_value3_integer_cofactor_streams = ics_value2_integer_cofactor_streams + ics_value1_integer_cofactor_streams)

Complete tactic proof in conservative notation

All 136 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

136 script commands · 18 reading checkpoints · 7 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 (1)

matrix integer signed minor balance

01Fix variables and assumptionsL1–10

Work with arbitrary variables or the premises of the current implication.

L1
intro ab
L2
intro ac
L3
intro bb
L4
intro bc
L5
intro eb
L6
intro ec
L7
intro fb
L8
intro fc
L9
intro cb
L10
intro cc

02Fix variables and assumptionsL11–20

Work with arbitrary variables or the premises of the current implication.

L11
intro db
L12
intro dc
L13
intro gb
L14
intro gc
L15
intro hb
L16
intro hc
L17
intro q
L18
intro hrecursion
L19
intro hequal
L20
intro hfirst

03Fix variables and assumptionsL21–30

Work with arbitrary variables or the premises of the current implication.

L21
intro hsecond
L22
intro i
L23
intro p
L24
intro n
L25
intro P
L26
intro N
L27
intro hi
L28
intro hp
L29
intro hn
L30
intro hP

04Fix variables and assumptionsL31–31

Work with arbitrary variables or the premises of the current implication.

L31
intro hN

05Establish hfirstcofactorL32–35

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hfirst.

L32
have hfirstcofactor : ∃ u. ∃ v. ∃ U. ∃ V. ∃ a. ∃ b. SignedMatrixMinor(ab,ac,bb,bc,S q,0,i,q,u,v,U,V) ∧ (SignedRecursiveDeterminant(u,v,U,V,q,a,b) ∧ (BetaAt(cb,cc,i,a) ∧ BetaAt(db,dc,i,b)))Definitions: SignedMatrixMinor(ab,ac,bb,bc,S q,0,i,q,u,v,U,V)SignedRecursiveDeterminant(u,v,U,V,q,a,b)BetaAt(cb,cc,i,a)BetaAt(db,dc,i,b)Original native command in the exact edition
L33
specialize hfirst (i)
L34
apply hfirst
L35
exact hi

06Separate the logical casesL36–44

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

L36
cases hfirstcofactor
L37
cases hfirstcofactor_witness
L38
cases hfirstcofactor_witness_witness
L39
cases hfirstcofactor_witness_witness_witness
L40
cases hfirstcofactor_witness_witness_witness_witness
L41
cases hfirstcofactor_witness_witness_witness_witness_witness
L42
cases hfirstcofactor_witness_witness_witness_witness_witness_witness
L43
cases hfirstcofactor_witness_witness_witness_witness_witness_witness_right
L44
cases hfirstcofactor_witness_witness_witness_witness_witness_witness_right_right

07Establish hsecondcofactorL45–48

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hsecond.

L45
have hsecondcofactor : ∃ u. ∃ v. ∃ U. ∃ V. ∃ a. ∃ b. SignedMatrixMinor(eb,ec,fb,fc,S q,0,i,q,u,v,U,V) ∧ (SignedRecursiveDeterminant(u,v,U,V,q,a,b) ∧ (BetaAt(gb,gc,i,a) ∧ BetaAt(hb,hc,i,b)))Definitions: SignedMatrixMinor(eb,ec,fb,fc,S q,0,i,q,u,v,U,V)SignedRecursiveDeterminant(u,v,U,V,q,a,b)BetaAt(gb,gc,i,a)BetaAt(hb,hc,i,b)Original native command in the exact edition
L46
specialize hsecond (i)
L47
apply hsecond
L48
exact hi

08Separate the logical casesL49–57

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

L49
cases hsecondcofactor
L50
cases hsecondcofactor_witness
L51
cases hsecondcofactor_witness_witness
L52
cases hsecondcofactor_witness_witness_witness
L53
cases hsecondcofactor_witness_witness_witness_witness
L54
cases hsecondcofactor_witness_witness_witness_witness_witness
L55
cases hsecondcofactor_witness_witness_witness_witness_witness_witness
L56
cases hsecondcofactor_witness_witness_witness_witness_witness_witness_right
L57
cases hsecondcofactor_witness_witness_witness_witness_witness_witness_right_right

09Establish hbalanceL58–67

Establish this local claim before using it. It is not an additional assumption.

L58
have hbalance : x4 + x11 = x10 + x5
L59
specialize hrecursion (x)
L60
specialize hrecursion (x1)
L61
specialize hrecursion (x2)
L62
specialize hrecursion (x3)
L63
specialize hrecursion (x6)
L64
specialize hrecursion (x7)
L65
specialize hrecursion (x8)
L66
specialize hrecursion (x9)
L67
specialize hrecursion (x4)

10Use earlier factsL68–77

Instantiate or apply named facts and discharge the corresponding proof obligations.

L68
specialize hrecursion (x5)
L69
specialize hrecursion (x10)
L70
specialize hrecursion (x11)
L71
apply hrecursion
L72
specialize matrix_integer_signed_minor_balance (ab)
L73
specialize matrix_integer_signed_minor_balance (ac)
L74
specialize matrix_integer_signed_minor_balance (bb)
L75
specialize matrix_integer_signed_minor_balance (bc)
L76
specialize matrix_integer_signed_minor_balance (eb)
L77
specialize matrix_integer_signed_minor_balance (ec)

11Use earlier factsL78–87

Instantiate or apply named facts and discharge the corresponding proof obligations.

L78
specialize matrix_integer_signed_minor_balance (fb)
L79
specialize matrix_integer_signed_minor_balance (fc)
L80
specialize matrix_integer_signed_minor_balance (x)
L81
specialize matrix_integer_signed_minor_balance (x1)
L82
specialize matrix_integer_signed_minor_balance (x2)
L83
specialize matrix_integer_signed_minor_balance (x3)
L84
specialize matrix_integer_signed_minor_balance (x6)
L85
specialize matrix_integer_signed_minor_balance (x7)
L86
specialize matrix_integer_signed_minor_balance (x8)
L87
specialize matrix_integer_signed_minor_balance (x9)

12Use earlier factsL88–95

Instantiate or apply named facts and discharge the corresponding proof obligations.

L88
specialize matrix_integer_signed_minor_balance (q)
L89
specialize matrix_integer_signed_minor_balance (i)
L90
apply matrix_integer_signed_minor_balance
L91
exact hequal
L92
exact hfirstcofactor_witness_witness_witness_witness_witness_witness_left
L93
exact hsecondcofactor_witness_witness_witness_witness_witness_witness_left
L94
exact hfirstcofactor_witness_witness_witness_witness_witness_witness_right_left
L95
exact hsecondcofactor_witness_witness_witness_witness_witness_witness_right_left

13Establish hpositiveL96–104

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta at unique.

L96
have hpositive : p = x4
L97
specialize beta_at_unique (cb)
L98
specialize beta_at_unique (cc)
L99
specialize beta_at_unique (i)
L100
specialize beta_at_unique (p)
L101
specialize beta_at_unique (x4)
L102
apply beta_at_unique
L103
exact hp
L104
exact hfirstcofactor_witness_witness_witness_witness_witness_witness_right_right_left

14Establish hnegativeL105–113

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta at unique.

L105
have hnegative : n = x5
L106
specialize beta_at_unique (db)
L107
specialize beta_at_unique (dc)
L108
specialize beta_at_unique (i)
L109
specialize beta_at_unique (n)
L110
specialize beta_at_unique (x5)
L111
apply beta_at_unique
L112
exact hn
L113
exact hfirstcofactor_witness_witness_witness_witness_witness_witness_right_right_right

15Establish hotherpositiveL114–122

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta at unique.

L114
have hotherpositive : P = x10
L115
specialize beta_at_unique (gb)
L116
specialize beta_at_unique (gc)
L117
specialize beta_at_unique (i)
L118
specialize beta_at_unique (P)
L119
specialize beta_at_unique (x10)
L120
apply beta_at_unique
L121
exact hP
L122
exact hsecondcofactor_witness_witness_witness_witness_witness_witness_right_right_left

16Establish hothernegativeL123–132

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta at unique.

L123
have hothernegative : N = x11
L124
specialize beta_at_unique (hb)
L125
specialize beta_at_unique (hc)
L126
specialize beta_at_unique (i)
L127
specialize beta_at_unique (N)
L128
specialize beta_at_unique (x11)
L129
apply beta_at_unique
L130
exact hN
L131
exact hsecondcofactor_witness_witness_witness_witness_witness_witness_right_right_right
L132
rewrite hpositive

17Calculate and transport equalitiesL133–135

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

L133
rewrite hnegative
L134
rewrite hotherpositive
L135
rewrite hothernegative

18Use earlier factsL136–136

Instantiate or apply named facts and discharge the corresponding proof obligations.

L136
exact hbalance

Library-wide reading audit

Original defined command ledger · 136 lines

0001intro ab
0002intro ac
0003intro bb
0004intro bc
0005intro eb
0006intro ec
0007intro fb
0008intro fc
0009intro cb
0010intro cc
0011intro db
0012intro dc
0013intro gb
0014intro gc
0015intro hb
0016intro hc
0017intro q
0018intro hrecursion
0019intro hequal
0020intro hfirst
0021intro hsecond
0022intro i
0023intro p
0024intro n
0025intro P
0026intro N
0027intro hi
0028intro hp
0029intro hn
0030intro hP
0031intro hN
0032have hfirstcofactor : ∃ u. ∃ v. ∃ U. ∃ V. ∃ a. ∃ b. SignedMatrixMinor(ab,ac,bb,bc,S q,0,i,q,u,v,U,V) ∧ (SignedRecursiveDeterminant(u,v,U,V,q,a,b) ∧ (BetaAt(cb,cc,i,a) ∧ BetaAt(db,dc,i,b)))
0033specialize hfirst (i)
0034apply hfirst
0035exact hi
0036cases hfirstcofactor
0037cases hfirstcofactor_witness
0038cases hfirstcofactor_witness_witness
0039cases hfirstcofactor_witness_witness_witness
0040cases hfirstcofactor_witness_witness_witness_witness
0041cases hfirstcofactor_witness_witness_witness_witness_witness
0042cases hfirstcofactor_witness_witness_witness_witness_witness_witness
0043cases hfirstcofactor_witness_witness_witness_witness_witness_witness_right
0044cases hfirstcofactor_witness_witness_witness_witness_witness_witness_right_right
0045have hsecondcofactor : ∃ u. ∃ v. ∃ U. ∃ V. ∃ a. ∃ b. SignedMatrixMinor(eb,ec,fb,fc,S q,0,i,q,u,v,U,V) ∧ (SignedRecursiveDeterminant(u,v,U,V,q,a,b) ∧ (BetaAt(gb,gc,i,a) ∧ BetaAt(hb,hc,i,b)))
0046specialize hsecond (i)
0047apply hsecond
0048exact hi
0049cases hsecondcofactor
0050cases hsecondcofactor_witness
0051cases hsecondcofactor_witness_witness
0052cases hsecondcofactor_witness_witness_witness
0053cases hsecondcofactor_witness_witness_witness_witness
0054cases hsecondcofactor_witness_witness_witness_witness_witness
0055cases hsecondcofactor_witness_witness_witness_witness_witness_witness
0056cases hsecondcofactor_witness_witness_witness_witness_witness_witness_right
0057cases hsecondcofactor_witness_witness_witness_witness_witness_witness_right_right
0058have hbalance : x4 + x11 = x10 + x5
0059specialize hrecursion (x)
0060specialize hrecursion (x1)
0061specialize hrecursion (x2)
0062specialize hrecursion (x3)
0063specialize hrecursion (x6)
0064specialize hrecursion (x7)
0065specialize hrecursion (x8)
0066specialize hrecursion (x9)
0067specialize hrecursion (x4)
0068specialize hrecursion (x5)
0069specialize hrecursion (x10)
0070specialize hrecursion (x11)
0071apply hrecursion
0072specialize matrix_integer_signed_minor_balance (ab)
0073specialize matrix_integer_signed_minor_balance (ac)
0074specialize matrix_integer_signed_minor_balance (bb)
0075specialize matrix_integer_signed_minor_balance (bc)
0076specialize matrix_integer_signed_minor_balance (eb)
0077specialize matrix_integer_signed_minor_balance (ec)
0078specialize matrix_integer_signed_minor_balance (fb)
0079specialize matrix_integer_signed_minor_balance (fc)
0080specialize matrix_integer_signed_minor_balance (x)
0081specialize matrix_integer_signed_minor_balance (x1)
0082specialize matrix_integer_signed_minor_balance (x2)
0083specialize matrix_integer_signed_minor_balance (x3)
0084specialize matrix_integer_signed_minor_balance (x6)
0085specialize matrix_integer_signed_minor_balance (x7)
0086specialize matrix_integer_signed_minor_balance (x8)
0087specialize matrix_integer_signed_minor_balance (x9)
0088specialize matrix_integer_signed_minor_balance (q)
0089specialize matrix_integer_signed_minor_balance (i)
0090apply matrix_integer_signed_minor_balance
0091exact hequal
0092exact hfirstcofactor_witness_witness_witness_witness_witness_witness_left
0093exact hsecondcofactor_witness_witness_witness_witness_witness_witness_left
0094exact hfirstcofactor_witness_witness_witness_witness_witness_witness_right_left
0095exact hsecondcofactor_witness_witness_witness_witness_witness_witness_right_left
0096have hpositive : p = x4
0097specialize beta_at_unique (cb)
0098specialize beta_at_unique (cc)
0099specialize beta_at_unique (i)
0100specialize beta_at_unique (p)
0101specialize beta_at_unique (x4)
0102apply beta_at_unique
0103exact hp
0104exact hfirstcofactor_witness_witness_witness_witness_witness_witness_right_right_left
0105have hnegative : n = x5
0106specialize beta_at_unique (db)
0107specialize beta_at_unique (dc)
0108specialize beta_at_unique (i)
0109specialize beta_at_unique (n)
0110specialize beta_at_unique (x5)
0111apply beta_at_unique
0112exact hn
0113exact hfirstcofactor_witness_witness_witness_witness_witness_witness_right_right_right
0114have hotherpositive : P = x10
0115specialize beta_at_unique (gb)
0116specialize beta_at_unique (gc)
0117specialize beta_at_unique (i)
0118specialize beta_at_unique (P)
0119specialize beta_at_unique (x10)
0120apply beta_at_unique
0121exact hP
0122exact hsecondcofactor_witness_witness_witness_witness_witness_witness_right_right_left
0123have hothernegative : N = x11
0124specialize beta_at_unique (hb)
0125specialize beta_at_unique (hc)
0126specialize beta_at_unique (i)
0127specialize beta_at_unique (N)
0128specialize beta_at_unique (x11)
0129apply beta_at_unique
0130exact hN
0131exact hsecondcofactor_witness_witness_witness_witness_witness_witness_right_right_right
0132rewrite hpositive
0133rewrite hnegative
0134rewrite hotherpositive
0135rewrite hothernegative
0136exact hbalance